Evaluating circuits in polynomial time

evalCode evaluates a list of gates (Cslib.Circuits.Program.code) on a list of input values: starting from the inputs, it appends the value of each gate in turn, reading wire i at position i of the values computed so far. On the code of a program it returns the inputs followed by the values of the gates (Cslib.Circuits.Program.evalCode_code), so it evaluates circuits exactly as Cslib.Circuits.Circuit.eval does (Cslib.Circuits.Circuit.eval_eq_getD). It is total: an argument or a wire missing from a malformed list reads a default value.

For De Morgan circuits, evalCode is computable in polynomial time on the binary encoding of gate lists (Cslib.Circuits.Boolean.computableInPolyTime_evalCode), so is reading an output wire given by its binary number (Cslib.Circuits.Boolean.computableInPolyTime_evalOutput). These are certificates for the fun_prop calculus of tidy polynomial-time computations; the evaluators of Complexity.Computability.Circuit.Evaluation carry no runtime bound. Each gate is evaluated by two lookups at wire numbers, which are capped at the number of values computed so far before they are converted to unary, so wire numbers far beyond the circuit cost only their binary length.

The typed evaluation certificate accepts any bit list. It pads short lists with false and truncates long lists to the declared input arity before invoking the raw evaluator. Circuit generation, input preparation, binary wire lookup and evaluation are all included in its cost.

Main definitions

• Cslib.Circuits.evalCode: evaluation of a list of gates.
• Cslib.Circuits.Boolean.evalOutput: the value of a wire after evaluating a list of De Morgan gates.

Main results

• Cslib.Circuits.prefix_evalCode: evaluating a gate list preserves its input prefix.

• Cslib.Circuits.getD_evalCode: the value of a well-formed gate from its arguments.

• Cslib.Circuits.Program.evalCode_code: on the code of a program, evalCode lists the inputs and the gate values.

• Cslib.Circuits.Circuit.eval_eq_getD: circuit evaluation through the code.

• Cslib.Circuits.Circuit.eval_eq_evalOutput: the same for De Morgan circuits, through Cslib.Circuits.Boolean.evalOutput.

• Cslib.Circuits.Circuit.eval_ofList_eq_evalOutput: typed evaluation on an arbitrary input list uses the padded or truncated input word.

• Cslib.Circuits.Boolean.computableInPolyTime_evalCode, Cslib.Circuits.Boolean.computableInPolyTime_evalOutput: evaluation of De Morgan gate lists is polynomial-time.

• Cslib.Circuits.Boolean.computableInPolyTime_evalCircuit: evaluating an efficiently generated typed circuit on an efficiently generated input list is polynomial-time.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 6.1

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

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]

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'

@[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.

Polynomial time

theorem Cslib.Circuits.Boolean.computableInPolyTime_evalCode {γ : Type} {encIn : γ ↪ List Bool} {x : γ → List Bool} {gates : γ → List (Op × List ℕ)} (hx : Turing.MultiTapeTM.ComputableInPolyTime x encIn Turing.MultiTapeTM.encBits) (hgates : Turing.MultiTapeTM.ComputableInPolyTime gates encIn (Turing.MultiTapeTM.encList encGate)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ) => evalCode interpretation false (x a) (gates a)) encIn Turing.MultiTapeTM.encBits

Polynomial-time evaluation of De Morgan gate lists, for input bits and a gate list in the binary encoding encGate, both computed in polynomial time.

def Cslib.Circuits.Boolean.evalOutput (x : List Bool) (gates : List (Op × List ℕ)) (o : ℕ) : Bool

The value of wire o after evaluating the De Morgan gate list gates on the input bits x: on the code of a circuit and the number of an output wire, the value of that output (Circuit.eval_eq_getD).

theorem Cslib.Circuits.Circuit.eval_eq_evalOutput {n m : ℕ} (c : Circuit Boolean.signature n m) (x : Fin n → Bool) (j : Fin m) : c.eval Boolean.interpretation x j = Boolean.evalOutput (List.ofFn x) c.code.1 (c.outputs j).toNat

Output j of a De Morgan circuit is evalOutput at the number of its output wire.

theorem Cslib.Circuits.Boolean.computableInPolyTime_evalOutput {γ : Type} {encIn : γ ↪ List Bool} {x : γ → List Bool} {gates : γ → List (Op × List ℕ)} {o : γ → ℕ} (hx : Turing.MultiTapeTM.ComputableInPolyTime x encIn Turing.MultiTapeTM.encBits) (hgates : Turing.MultiTapeTM.ComputableInPolyTime gates encIn (Turing.MultiTapeTM.encList encGate)) (ho : Turing.MultiTapeTM.ComputableInPolyTime o encIn Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ) => evalOutput (x a) (gates a) (o a)) encIn Turing.MultiTapeTM.encBool

Polynomial-time evaluation of an output of a De Morgan gate list, for input bits, a gate list in the binary encoding encGate and a binary wire number, all computed in polynomial time.

theorem Cslib.Circuits.Circuit.eval_ofList_eq_evalOutput {n m : ℕ} (c : Circuit Boolean.signature n m) (x : List Bool) (j : Fin m) : c.eval Boolean.interpretation (BitString.ofList n x) j = Boolean.evalOutput (List.take n (x ++ List.replicate n false)) c.code.1 (c.code.2.getD (↑j) 0)

Evaluate a typed circuit on an arbitrary bit list by padding or truncating to its input arity. The output wire is read from the circuit's code at the specified output position.

theorem Cslib.Circuits.Boolean.computableInPolyTime_evalCircuit {γ : Type} {encIn : γ ↪ List Bool} {c : γ → (n : ℕ) × Circuit signature n 1} {x : γ → List Bool} (hc : Turing.MultiTapeTM.ComputableInPolyTime c encIn (encCircuit 1)) (hx : Turing.MultiTapeTM.ComputableInPolyTime x encIn Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ) => (c a).snd.eval interpretation (BitString.ofList (c a).fst (x a)) 0) encIn Turing.MultiTapeTM.encBool

Evaluate an efficiently computed typed circuit on any efficiently computed bit list. No length premise is needed: missing inputs are false, and inputs past the circuit's arity are ignored. The certificate charges circuit generation, input padding and all evaluation.