Effective evaluation of the routed circuit polynomial

The evaluator multiplies the gate-consistency factors, retaining preceding input-copy values for routing. It works directly on coefficient vectors and never expands the polynomial into monomials.

def MIPRE.SAT.Circuit.factorBits (e : FieldEnv) (a : Gate × Cost.BitStr) : Cost.BitStr

One gate-consistency factor, with its claimed gate value.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev MIPRE.SAT.Circuit.FieldState : Type

Equations

• MIPRE.SAT.Circuit.FieldState = (MIPRE.SAT.Circuit.FieldEnv × MIPRE.Cost.BitStr)

def MIPRE.SAT.Circuit.fieldStep (s : FieldState) (a : Gate × Cost.BitStr) : FieldState

Append the gate to the routing history and multiply its consistency factor.

Equations

• MIPRE.SAT.Circuit.fieldStep s a = ((s.1.1, s.1.2.1, s.1.2.2.1, s.1.2.2.2 ++ [a]), MIPRE.LowDegree.BinaryPolynomial.mulReduce s.1.1 s.2 (MIPRE.SAT.Circuit.factorBits s.1 a))

theorem MIPRE.SAT.Circuit.fieldStep_width_le (s : FieldState) (a : Gate × Cost.BitStr) : List.length (fieldStep s a).2 ≤ List.length s.2

theorem MIPRE.SAT.Circuit.fold_fieldStep (l : List (Gate × Cost.BitStr)) (s : FieldState) : (List.foldl fieldStep s l).1 = (s.1.1, s.1.2.1, s.1.2.2.1, s.1.2.2.2 ++ l) ∧ List.length (List.foldl fieldStep s l).2 ≤ List.length s.2

The fold retains the modulus and coordinates, stores only the scanned history, and never increases its accumulator's coefficient width.

def MIPRE.SAT.Circuit.gatePairs (gs : List Gate) (w : List Cost.BitStr) : List (Gate × Cost.BitStr)

Pair each actual gate with its supplied coordinate; short malformed coordinate arrays use the empty vector.

Equations

• MIPRE.SAT.Circuit.gatePairs gs w = List.map (fun (j : ℕ) => (gs.getD j (MIPRE.SAT.Gate.const false), w.getD j [])) (List.range gs.length)

def MIPRE.SAT.Circuit.circuitBits (p : Cost.BitStr) (x w : List Cost.BitStr) (gs : List Gate) : Cost.BitStr

The complete circuit polynomial evaluator on coefficient vectors.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.SAT.Circuit.factorBitsProg : Cost.PolyTimeFun (FieldEnv × Gate × Cost.BitStr) Cost.BitStr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.SAT.Circuit.factorBitsProg_apply (e : FieldEnv) (a : Gate × Cost.BitStr) : factorBitsProg.toFun (e, a) = factorBits e a

noncomputable def MIPRE.SAT.Circuit.fieldStepProg : Cost.PolyTimeFun (FieldState × Gate × Cost.BitStr) FieldState

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.SAT.Circuit.fieldStepProg_apply (s : FieldState) (a : Gate × Cost.BitStr) : fieldStepProg.toFun (s, a) = fieldStep s a

theorem MIPRE.SAT.Circuit.fieldStep_bounded : fieldStepProg.FoldBounded (5 * Polynomial.X + 5)

noncomputable def MIPRE.SAT.Circuit.fieldScanProg : Cost.PolyTimeFun (List (Gate × Cost.BitStr) × FieldState) FieldState

The scan is an ambient polynomial-time program even on malformed inputs.

Equations

• MIPRE.SAT.Circuit.fieldScanProg = MIPRE.SAT.Circuit.fieldStepProg.foldl (5 * Polynomial.X + 5) MIPRE.SAT.Circuit.fieldStep_bounded

@[simp]

theorem MIPRE.SAT.Circuit.fieldScanProg_apply (l : List (Gate × Cost.BitStr)) (s : FieldState) : fieldScanProg.toFun (l, s) = List.foldl fieldStep s l

noncomputable def MIPRE.SAT.Circuit.gatePairsProg : Cost.PolyTimeFun (List Gate × List Cost.BitStr) (List (Gate × Cost.BitStr))

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.SAT.Circuit.gatePairsProg_apply (p : List Gate × List Cost.BitStr) : gatePairsProg.toFun p = gatePairs p.1 p.2

noncomputable def MIPRE.SAT.Circuit.circuitBitsProg : Cost.PolyTimeFun (Cost.BitStr × List Cost.BitStr × List Cost.BitStr × List Gate) Cost.BitStr

Uniform polynomial-time evaluation of the routed circuit polynomial. The input contains the modulus, external coordinates, gate coordinates, and gates.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.SAT.Circuit.circuitBitsProg_apply (p : Cost.BitStr) (x w : List Cost.BitStr) (gs : List Gate) : circuitBitsProg.toFun (p, x, w, gs) = circuitBits p x w gs