Evaluation of circuit codes

The signature and interpretation are arbitrary. Gate lists are evaluated in program order, appending one value per gate. Missing arguments and out-of-range wire indices read a supplied default. This total semantics agrees with typed circuit evaluation on actual circuit codes. Runtime certificates belong to the interpretation-specific modules.

Main definitions

• evalCode: total evaluation of a gate list.

Main results

• length_evalCode, prefix_evalCode: the evaluator appends one value per gate.
• getD_evalCode: gate equations on well-formed codes.
• Program.evalCode_code: the input values followed by the complete program trace.
• Circuit.eval_eq_getD: typed circuit outputs are lookups in that trace.

These are original implementation lemmas for the existing circuit semantics.

def Cslib.Circuits.evalCode {σ : Signature} {U : Type u} (I : Interpretation σ U) (d : U) (x : List U) (gates : List (σ.Op × List ℕ)) : List U

Evaluate the list of gates gates on the input values x: start from x and append the value of each gate in turn, reading wire i at position i of the values computed so far. An argument missing from a gate, or a wire not yet computed, reads d; on the code of a program neither happens (Program.evalCode_code).

@[simp]

theorem Cslib.Circuits.evalCode_nil {σ : Signature} {U : Type u} (I : Interpretation σ U) (d : U) (x : List U) : evalCode I d x [] = x

Evaluating an empty gate list returns the initial wire values unchanged.

theorem Cslib.Circuits.evalCode_append_singleton {σ : Signature} {U : Type u} (I : Interpretation σ U) (d : U) (x : List U) (gates : List (σ.Op × List ℕ)) (g : σ.Op × List ℕ) : evalCode I d x (gates ++ [g]) = evalCode I d x gates ++ [I g.1 fun (a : Fin (σ.Arity g.1)) => g.2[↑a]?.elim d fun (x_1 : ℕ) => (evalCode I d x gates).getD x_1 d]

Evaluating a gate list followed by one gate g appends g's evaluated output to the wire values computed by gates.

theorem Cslib.Circuits.evalCode_append {σ : Signature} {U : Type u} (I : Interpretation σ U) (d : U) (x : List U) (gates gates' : List (σ.Op × List ℕ)) : evalCode I d x (gates ++ gates') = evalCode I d (evalCode I d x gates) gates'

Evaluating a concatenation of gate lists evaluates the second list starting from the wire values produced by the first.

@[simp]

theorem Cslib.Circuits.length_evalCode {σ : Signature} {U : Type u} (I : Interpretation σ U) (d : U) (x : List U) (gates : List (σ.Op × List ℕ)) : (evalCode I d x gates).length = x.length + gates.length

Each gate adds one value.

theorem Cslib.Circuits.prefix_evalCode {σ : Signature} {U : Type u} (I : Interpretation σ U) (d : U) (x : List U) (gates : List (σ.Op × List ℕ)) : x <+: evalCode I d x gates

Evaluating a gate list only appends values.

theorem Cslib.Circuits.getD_evalCode {σ : Signature} {U : Type u} (I : Interpretation σ U) (d : U) (x : List U) {gates : List (σ.Op × List ℕ)} (h : Program.IsCodeFrom σ x.length 0 gates) {j : ℕ} {gate : σ.Op × List ℕ} (hg : gates[j]? = some gate) : (evalCode I d x gates).getD (x.length + j) d = I gate.1 fun (a : Fin (σ.Arity gate.1)) => gate.2[↑a]?.elim d fun (x_1 : ℕ) => (evalCode I d x gates).getD x_1 d

The value of a gate of a well-formed gate list is its operation applied to the values of its arguments.

theorem Cslib.Circuits.Wire.getD_append_toNat {U : Type u} {n k : ℕ} (x : Fin n → U) (y : Fin k → U) (d : U) (w : Wire n k) : (List.ofFn x ++ List.ofFn y).getD w.toNat d = elim x y w

Wire w is at position w.toNat of the inputs followed by the gates.

theorem Cslib.Circuits.Program.evalCode_code {σ : Signature} {U : Type u} {n k : ℕ} (p : Program σ n k) (I : Interpretation σ U) (d : U) (x : Fin n → U) : evalCode I d (List.ofFn x) p.code = List.ofFn x ++ List.ofFn (p.eval I x)

Evaluation through the code. On the code of a program, evalCode lists the inputs and then the values of the gates.

theorem Cslib.Circuits.Circuit.eval_eq_getD {σ : Signature} {U : Type u} {n m : ℕ} (c : Circuit σ n m) (I : Interpretation σ U) (d : U) (x : Fin n → U) (j : Fin m) : c.eval I x j = (evalCode I d (List.ofFn x) c.code.1).getD (c.outputs j).toNat d

Evaluation through the code. Output j of a circuit is the value at the number of its output wire after evaluating the gate list.