Circuit arithmetization on exactly the input and gate variables

The first C.inputs coordinates are the inputs, followed by the C.size gate variables. No new variables are needed for routing repeated input reads.

def MIPRE.SAT.Circuit.wireEmbedding (C : Circuit) : Fin (C.inputs + C.size) → ℕ ⊕ ℕ

Embed the exact finite coordinate set into input and gate indices.

Equations

• C.wireEmbedding = Sum.map Fin.val Fin.val ∘ ⇑finSumFinEquiv.symm

theorem MIPRE.SAT.Circuit.wireEmbedding_injective (C : Circuit) : Function.Injective C.wireEmbedding

@[simp]

theorem MIPRE.SAT.Circuit.wireEmbedding_input (C : Circuit) (i : Fin C.inputs) : C.wireEmbedding (Fin.castAdd C.size i) = Sum.inl ↑i

@[simp]

theorem MIPRE.SAT.Circuit.wireEmbedding_gate (C : Circuit) (j : Fin C.size) : C.wireEmbedding (Fin.natAdd C.inputs j) = Sum.inr ↑j

noncomputable def MIPRE.SAT.Circuit.finiteArith {F : Type u_1} [Field F] (C : Circuit) : MvPolynomial (Fin (C.inputs + C.size)) F

The routed polynomial restricted to the exact finite coordinate set.

Equations

• C.finiteArith = (MvPolynomial.killCompl ⋯) C.routedArith

theorem MIPRE.SAT.Circuit.degreeOf_finiteArith_le {F : Type u_1} [Field F] (C : Circuit) (hC : C.WellFormed) (i : Fin (C.inputs + C.size)) : MvPolynomial.degreeOf i C.finiteArith ≤ 5

def MIPRE.SAT.Circuit.inputPart (C : Circuit) (z : Fin (C.inputs + C.size) → Bool) (i : ℕ) : Bool

Read the finite assignment's input part, with false outside the circuit.

Equations

• C.inputPart z i = if h : i < C.inputs then z (Fin.castAdd C.size ⟨i, h⟩) else false

def MIPRE.SAT.Circuit.gatePart (C : Circuit) (z : Fin (C.inputs + C.size) → Bool) (j : ℕ) : Bool

Read the finite assignment's gate part, with false outside the circuit.

Equations

• C.gatePart z j = if h : j < C.size then z (Fin.natAdd C.inputs ⟨j, h⟩) else false

theorem MIPRE.SAT.Circuit.eval_finiteArith {F : Type u_1} [Field F] (C : Circuit) (z : Fin (C.inputs + C.size) → Bool) : (MvPolynomial.eval fun (i : Fin (C.inputs + C.size)) => LowDegree.ofBool (z i)) C.finiteArith = (MvPolynomial.eval (Sum.elim (fun (i : ℕ) => LowDegree.ofBool (C.inputPart z i)) fun (j : ℕ) => LowDegree.ofBool (C.gatePart z j))) C.routedArith

theorem MIPRE.SAT.Circuit.eval_finiteArith_iff {F : Type u_1} [Field F] [CharP F 2] (C : Circuit) (hC : C.WellFormed) (z : Fin (C.inputs + C.size) → Bool) : (MvPolynomial.eval fun (i : Fin (C.inputs + C.size)) => LowDegree.ofBool (z i)) C.finiteArith = 1 ↔ C.RoutedConsistent (C.inputPart z) (C.gatePart z) ∧ C.gatePart z (C.size - 1) = true

The finite polynomial enforces all gate values and the output literal.

theorem MIPRE.SAT.Circuit.eval_finiteArith_bool {F : Type u_1} [Field F] [CharP F 2] (C : Circuit) (hC : C.WellFormed) (z : Fin (C.inputs + C.size) → Bool) : (MvPolynomial.eval fun (i : Fin (C.inputs + C.size)) => LowDegree.ofBool (z i)) C.finiteArith = 0 ∨ (MvPolynomial.eval fun (i : Fin (C.inputs + C.size)) => LowDegree.ofBool (z i)) C.finiteArith = 1

Boolean-valuedness is retained on the exact finite coordinate set.

theorem MIPRE.SAT.Circuit.inputPart_eq (C : Circuit) (x : ℕ → Bool) (z : Fin (C.inputs + C.size) → Bool) (h : ∀ (i : Fin C.inputs), z (Fin.castAdd C.size i) = x ↑i) (i : ℕ) : i < C.inputs → C.inputPart z i = x i

A finite assignment whose input coordinates equal x reads x on every input the circuit can use.

theorem MIPRE.SAT.Circuit.eval_iff_exists_finiteArith {F : Type u_1} [Field F] [CharP F 2] (C : Circuit) (hC : C.WellFormed) (x : ℕ → Bool) : C.eval x = true ↔ ∃ (z : Fin (C.inputs + C.size) → Bool), (∀ (i : Fin C.inputs), z (Fin.castAdd C.size i) = x ↑i) ∧ (MvPolynomial.eval fun (i : Fin (C.inputs + C.size)) => LowDegree.ofBool (z i)) C.finiteArith = 1

Exact-variable arithmetization of the accepting circuit relation.