Correctness of the executable circuit polynomial evaluator

def MIPRE.SAT.Circuit.fieldHistory (C : Circuit) (w : List Cost.BitStr) (k : ℕ) : List (Gate × Cost.BitStr)

Routing history at a prefix of the actual circuit.

Equations

• C.fieldHistory w k = List.map (fun (j : ℕ) => (C.gates.getD j (MIPRE.SAT.Gate.const false), w.getD j [])) (List.range k)

def MIPRE.SAT.Circuit.fieldPrefix (C : Circuit) (p : Cost.BitStr) (x w : List Cost.BitStr) (k : ℕ) : FieldState

Equations

• C.fieldPrefix p x w k = List.foldl MIPRE.SAT.Circuit.fieldStep ((p, x, w, []), MIPRE.SAT.Circuit.oneBits p) (C.fieldHistory w k)

theorem MIPRE.SAT.Circuit.fieldPrefix_env (C : Circuit) (p : Cost.BitStr) (x w : List Cost.BitStr) (k : ℕ) : (C.fieldPrefix p x w k).1 = (p, x, w, C.fieldHistory w k)

theorem MIPRE.SAT.Circuit.fieldPrefix_succ (C : Circuit) (p : Cost.BitStr) (x w : List Cost.BitStr) (k : ℕ) : C.fieldPrefix p x w (k + 1) = fieldStep (C.fieldPrefix p x w k) (C.gates.getD k (Gate.const false), w.getD k [])

theorem MIPRE.SAT.Circuit.fieldPrefix_width (C : Circuit) (p : Cost.BitStr) (x w : List Cost.BitStr) (k : ℕ) : List.length (C.fieldPrefix p x w k).2 = List.length p

theorem MIPRE.SAT.Circuit.readInput_fieldHistory (C : Circuit) (p : Cost.BitStr) (x w : List Cost.BitStr) (k i : ℕ) : readInput (p, x, w, C.fieldHistory w k) i = Sum.elim (fun (j : ℕ) => x.getD j []) (fun (j : ℕ) => w.getD j []) (C.inputRef k i)

theorem MIPRE.SAT.Circuit.width_getD (p : Cost.BitStr) (l : List Cost.BitStr) (h : ∀ b ∈ l, List.length b = List.length p) (i : ℕ) (hi : i < l.length) : List.length (l.getD i []) = List.length p

theorem MIPRE.SAT.Circuit.gate_ref_width (C : Circuit) (hC : C.WellFormed) (p : Cost.BitStr) (w : List Cost.BitStr) (hwlen : C.size ≤ w.length) (hw : ∀ b ∈ w, List.length b = List.length p) (k : ℕ) (hk : k < C.size) (j : ℕ) : j ∈ (C.gates.getD k (Gate.const false)).refs → List.length (w.getD j []) = List.length p

theorem MIPRE.SAT.Circuit.gate_input_width (C : Circuit) (hC : C.WellFormed) (p : Cost.BitStr) (x w : List Cost.BitStr) (hxlen : C.inputs ≤ x.length) (hwlen : C.size ≤ w.length) (hx : ∀ b ∈ x, List.length b = List.length p) (hw : ∀ b ∈ w, List.length b = List.length p) (k : ℕ) (hk : k < C.size) (i : ℕ) : C.gates.getD k (Gate.const false) = Gate.input i → List.length (readInput (p, x, w, C.fieldHistory w k) i) = List.length p

theorem MIPRE.SAT.Circuit.evalBits_factorBits {F : Type u_1} [Field F] [CharP F 2] (C : Circuit) (hC : C.WellFormed) (z : F) (p : Cost.BitStr) (hp : p ≠ []) (hroot : z ^ List.length p = LowDegree.BinaryPolynomial.evalBits z p) (x w : List Cost.BitStr) (hxlen : C.inputs ≤ x.length) (hwlen : C.size ≤ w.length) (hx : ∀ b ∈ x, List.length b = List.length p) (hw : ∀ b ∈ w, List.length b = List.length p) (k : ℕ) (hk : k < C.size) : LowDegree.BinaryPolynomial.evalBits z (factorBits (p, x, w, C.fieldHistory w k) (C.gates.getD k (Gate.const false), w.getD k [])) = (MvPolynomial.eval (Sum.elim (fun (i : ℕ) => LowDegree.BinaryPolynomial.evalBits z (x.getD i [])) fun (j : ℕ) => LowDegree.BinaryPolynomial.evalBits z (w.getD j []))) (C.consistencyFactor k)

Each computed factor evaluates to the corresponding polynomial factor.

theorem MIPRE.SAT.Circuit.evalBits_fieldPrefix {F : Type u_1} [Field F] [CharP F 2] (C : Circuit) (hC : C.WellFormed) (z : F) (p : Cost.BitStr) (hp : p ≠ []) (hroot : z ^ List.length p = LowDegree.BinaryPolynomial.evalBits z p) (x w : List Cost.BitStr) (hxlen : C.inputs ≤ x.length) (hwlen : C.size ≤ w.length) (hx : ∀ b ∈ x, List.length b = List.length p) (hw : ∀ b ∈ w, List.length b = List.length p) (k : ℕ) (hk : k ≤ C.size) : LowDegree.BinaryPolynomial.evalBits z (C.fieldPrefix p x w k).2 = ∏ j ∈ Finset.range k, (MvPolynomial.eval (Sum.elim (fun (i : ℕ) => LowDegree.BinaryPolynomial.evalBits z (x.getD i [])) fun (i : ℕ) => LowDegree.BinaryPolynomial.evalBits z (w.getD i []))) (C.consistencyFactor j)

The accumulator is precisely the product of the factors already scanned.

theorem MIPRE.SAT.Circuit.evalBits_circuitBits {F : Type u_1} [Field F] [CharP F 2] (C : Circuit) (hC : C.WellFormed) (z : F) (p : Cost.BitStr) (hp : p ≠ []) (hroot : z ^ List.length p = LowDegree.BinaryPolynomial.evalBits z p) (x w : List Cost.BitStr) (hxlen : C.inputs ≤ x.length) (hwlen : C.size ≤ w.length) (hx : ∀ b ∈ x, List.length b = List.length p) (hw : ∀ b ∈ w, List.length b = List.length p) : LowDegree.BinaryPolynomial.evalBits z (circuitBits p x w C.gates) = (MvPolynomial.eval (Sum.elim (fun (i : ℕ) => LowDegree.BinaryPolynomial.evalBits z (x.getD i [])) fun (j : ℕ) => LowDegree.BinaryPolynomial.evalBits z (w.getD j []))) C.routedArith

The executable coefficient-vector evaluator computes the complete routed circuit polynomial at every correctly sized field point.

theorem MIPRE.SAT.Circuit.length_circuitBits (C : Circuit) (p : Cost.BitStr) (x w : List Cost.BitStr) : List.length (circuitBits p x w C.gates) = List.length p

The evaluator always returns the supplied modulus width.

theorem MIPRE.SAT.Circuit.evalBits_circuitBits_finite {F : Type u_1} [Field F] [CharP F 2] (C : Circuit) (hC : C.WellFormed) (z : F) (p : Cost.BitStr) (hp : p ≠ []) (hroot : z ^ List.length p = LowDegree.BinaryPolynomial.evalBits z p) (x w : List Cost.BitStr) (hxlen : x.length = C.inputs) (hwlen : w.length = C.size) (hx : ∀ b ∈ x, List.length b = List.length p) (hw : ∀ b ∈ w, List.length b = List.length p) : LowDegree.BinaryPolynomial.evalBits z (circuitBits p x w C.gates) = (MvPolynomial.eval fun (i : Fin (C.inputs + C.size)) => Fin.addCases (fun (i : Fin C.inputs) => LowDegree.BinaryPolynomial.evalBits z (x.getD ↑i [])) (fun (j : Fin C.size) => LowDegree.BinaryPolynomial.evalBits z (w.getD ↑j [])) i) C.finiteArith

The same evaluator computes the polynomial on the exact finite coordinate set used by the PCP, with the inputs followed by the gate variables.