Lines read earlier wires

In the widened lines of a program (Program.lines), every gate wire that a line reads comes before the line's own gate (Program.lt_of_lines_wires_eq_gate), so facts about wires can be proved by induction along the program order (Program.wire_induction). Bounded fan-in is a bound on the arity of every line (Program.fanInAtMost_iff).

The value of a gate is its operation applied to the values of the wires it reads (Program.trace_gate, and Program.trace_gate_last for the last gate), and a valuation of the wires that reads the inputs and satisfies the equation of every gate is the trace (Program.eq_trace_of_forall_gate).

Main results

• Program.wire_induction: induction along the program order.
• Program.fanInAtMost_iff: bounded fan-in, gate by gate.
• Program.trace_gate, Program.trace_gate_last: the value of a gate.
• Program.trace_induction: propagate a semantic invariant from inputs through gates.
• Program.trace_rel, Program.eval_rel: lift a relation between two interpretations.
• Program.eq_trace_of_forall_gate: the trace is the unique solution of the gate equations.

theorem Cslib.Circuits.Program.lt_of_lines_wires_eq_gate {σ : Signature} {n g : ℕ} (p : Program σ n g) (k : Fin g) (s : Fin (σ.Arity (p.lines k).op)) (j : Fin g) (h : (p.lines k).wires s = Wire.gate j) : j < k

The gate wires read by a line come before its gate.

theorem Cslib.Circuits.Program.fanInAtMost_iff {σ : Signature} {n g : ℕ} {p : Program σ n g} {r : ℕ} : p.FanInAtMost r ↔ ∀ (k : Fin g), σ.Arity (p.lines k).op ≤ r

A program has fan-in at most r exactly when every gate reads at most r wires.

theorem Cslib.Circuits.Program.wire_induction {σ : Signature} {n g : ℕ} (p : Program σ n g) {P : Wire n g → Prop} (input : ∀ (i : Fin n), P (Wire.input i)) (gate : ∀ (k : Fin g), (∀ (s : Fin (σ.Arity (p.lines k).op)), P ((p.lines k).wires s)) → P (Wire.gate k)) (w : Wire n g) : P w

Induction along the program order: a property of wires that holds for the inputs, and for a gate whenever it holds for the wires the gate reads, holds for every wire.

theorem Cslib.Circuits.Program.trace_gate {σ : Signature} {n g : ℕ} {U : Type u_1} (p : Program σ n g) (I : Interpretation σ U) (x : Fin n → U) (k : Fin g) : p.trace I x (Wire.gate k) = I (p.lines k).op fun (a : Fin (σ.Arity (p.lines k).op)) => p.trace I x ((p.lines k).wires a)

The value of a gate is its operation applied to the values of the wires it reads.

theorem Cslib.Circuits.Program.trace_gate_last {σ : Signature} {n g : ℕ} {U : Type u_1} (p : Program σ n g) (line : Line σ n g) (I : Interpretation σ U) (x : Fin n → U) : (p.gate line).trace I x (Wire.gate (Fin.last g)) = I line.op fun (a : Fin (σ.Arity line.op)) => p.trace I x (line.wires a)

The value of the last gate of a program is its operation applied to the values of its arguments.

theorem Cslib.Circuits.Program.trace_induction {σ : Signature} {n g : ℕ} {U : Type u_1} (p : Program σ n g) (I : Interpretation σ U) (x : Fin n → U) {P : U → Prop} (input : ∀ (i : Fin n), P (x i)) (gate : ∀ (k : Fin g), (∀ (a : Fin (σ.Arity (p.lines k).op)), P (p.trace I x ((p.lines k).wires a))) → P (I (p.lines k).op (p.trace I x ∘ (p.lines k).wires))) (w : Wire n g) : P (p.trace I x w)

An invariant holding on the inputs and preserved by every evaluated gate holds on every wire. The preservation hypothesis is needed only for the arguments actually read by the gate.

theorem Cslib.Circuits.Program.eq_trace_of_forall_gate {σ : Signature} {n g : ℕ} {U : Type u_1} {p : Program σ n g} {I : Interpretation σ U} {v : Wire n g → U} {x : Fin n → U} (hin : ∀ (i : Fin n), v (Wire.input i) = x i) (hgate : ∀ (k : Fin g), v (Wire.gate k) = I (p.lines k).op fun (a : Fin (σ.Arity (p.lines k).op)) => v ((p.lines k).wires a)) : v = p.trace I x

A valuation of the wires is the trace of p when it reads the inputs and satisfies the equation of every gate.

theorem Cslib.Circuits.Program.trace_rel {σ : Signature} {n g : ℕ} {U : Type u_1} {V : Type u_2} (p : Program σ n g) {I : Interpretation σ U} {J : Interpretation σ V} {x : Fin n → U} {y : Fin n → V} (R : U → V → Prop) (input : ∀ (i : Fin n), R (x i) (y i)) (gate : ∀ (k : Fin g) (a : Fin (σ.Arity (p.lines k).op) → U) (b : Fin (σ.Arity (p.lines k).op) → V), (∀ (i : Fin (σ.Arity (p.lines k).op)), R (a i) (b i)) → R (I (p.lines k).op a) (J (p.lines k).op b)) (w : Wire n g) : R (p.trace I x w) (p.trace J y w)

Two interpretations preserve a relation on every wire if the inputs are related and the operations occurring in the program preserve it. No condition is imposed on unused operations.

theorem Cslib.Circuits.Program.eval_rel {σ : Signature} {n g : ℕ} {U : Type u_1} {V : Type u_2} (p : Program σ n g) {I : Interpretation σ U} {J : Interpretation σ V} {x : Fin n → U} {y : Fin n → V} (R : U → V → Prop) (input : ∀ (i : Fin n), R (x i) (y i)) (gate : ∀ (k : Fin g) (a : Fin (σ.Arity (p.lines k).op) → U) (b : Fin (σ.Arity (p.lines k).op) → V), (∀ (i : Fin (σ.Arity (p.lines k).op)), R (a i) (b i)) → R (I (p.lines k).op a) (J (p.lines k).op b)) (k : Fin g) : R (p.eval I x k) (p.eval J y k)

Related inputs and gate interpretations give related gate values.