Semantic circuit normalization

Merging gates that compute the same function preserves wire values and does not increase circuit size. A gate duplicating an earlier wire, or read by neither a gate nor the output, can be removed to obtain a strictly smaller single-output circuit.

def Cslib.Circuits.Program.Irredundant {σ : Signature} {n g : ℕ} {U : Type u_1} (p : Program σ n g) (i : Interpretation σ U) : Prop

Distinct gates compute distinct scalar functions. Gates may still duplicate input functions or be unused by the outputs.

Equations

• p.Irredundant i = Function.Injective (p.gateFunction i)

def Cslib.Circuits.Circuit.Irredundant {σ : Signature} {n m : ℕ} {U : Type u_1} (c : Circuit σ n m) (i : Interpretation σ U) : Prop

A circuit is irredundant when its internal gates compute pairwise distinct functions.

Equations

• c.Irredundant i = c.program.Irredundant i

theorem Cslib.Circuits.Program.exists_irredundant {σ : Signature} {n g : ℕ} {U : Type u_1} (p : Program σ n g) (i : Interpretation σ U) : ∃ k ≤ g, ∃ (q : Program σ n k) (ρ : Wire.Renaming n g k), (∀ (x : Fin n → U) (w : Wire n g), q.trace i x (ρ.apply w) = p.trace i x w) ∧ q.Irredundant i

A program can be rebuilt with distinct gate functions, preserving every wire's value.

theorem Cslib.Circuits.Circuit.exists_irredundant {σ : Signature} {n m : ℕ} {U : Type u_1} (c : Circuit σ n m) (i : Interpretation σ U) : ∃ (d : Circuit σ n m), d.eval i = c.eval i ∧ d.Irredundant i ∧ d.size ≤ c.size

Every circuit has an equivalent circuit with distinct gate functions and no more gates.

theorem Cslib.Circuits.Circuit.exists_smaller_of_equal {σ : Signature} {n : ℕ} {U : Type u_1} {I : Interpretation σ U} (c : Circuit σ n 1) (gate : Fin c.size) (wire : Wire n c.size) (hbefore : ↑wire.index < n + ↑gate) (heq : c.program.gateFunction I gate = c.program.wireFunction I wire) : ∃ (d : Circuit σ n 1), d.eval I = c.eval I ∧ d.size < c.size

A gate duplicating an earlier wire can be removed without changing the output.

theorem Cslib.Circuits.Circuit.exists_smaller_of_unused {σ : Signature} {n : ℕ} {U : Type u_1} {I : Interpretation σ U} (c : Circuit σ n 1) (input : Fin n) (gate : Fin c.size) (hread : ∀ (j : Fin c.size), ¬c.program.Reads j (Wire.gate gate)) (houtput : c.outputs 0 ≠ Wire.gate gate) : ∃ (d : Circuit σ n 1), d.eval I = c.eval I ∧ d.size < c.size

A gate read by no gate or designated output can be omitted. The given input supplies a zero-cost placeholder during reconstruction.