The raw verifier and its fixed typed clause polynomial

noncomputable def MIPRE.TM.CookLevin.Pad.fixedCircuit (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) : SAT.Circuit

Equations

• MIPRE.TM.CookLevin.Pad.fixedCircuit D n T Q σ x y = MIPRE.TM.CookLevin.Pad.describeExact.toFun (((D, n, T, Q, σ), x, y), MIPRE.Cost.unary (MIPRE.TM.CookLevin.Pad.gateCount n T Q σ))

theorem MIPRE.TM.CookLevin.Pad.fixedCircuit_wellFormed (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) : (fixedCircuit D n T Q σ x y).WellFormed

theorem MIPRE.TM.CookLevin.Pad.fixedCircuit_inputs (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) : (fixedCircuit D n T Q σ x y).inputs = 5 * (pcpParams n T Q σ).m + 5

theorem MIPRE.TM.CookLevin.Pad.fixedCircuit_variables (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (hV : SAT.Valid D n T Q σ x y) : (fixedCircuit D n T Q σ x y).inputs + (fixedCircuit D n T Q σ x y).size = (pcpParams n T Q σ).m'

theorem MIPRE.TM.CookLevin.Pad.fixedCircuit_describes (D : Decider) (n T Q σ : ℕ) (x y : Cost.BitStr) (hV : SAT.Valid D.prog n T Q σ x y) : (fixedCircuit D.prog n T Q σ x y).DescribesDecider (pcpParams n T Q σ).m (pcpParams n T Q σ).m D n x y T

noncomputable def MIPRE.TM.CookLevin.Pad.clausePolynomial {F : Type u_1} [Field F] (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (hV : SAT.Valid D n T Q σ x y) : MvPolynomial (Fin (pcpParams n T Q σ).m') F

Equations

• MIPRE.TM.CookLevin.Pad.clausePolynomial D n T Q σ x y hV = (MIPRE.TM.CookLevin.Pad.pcpParams n T Q σ).circuitArith (MIPRE.TM.CookLevin.Pad.fixedCircuit D n T Q σ x y) ⋯

theorem MIPRE.TM.CookLevin.Pad.pcpParams_degree_pos (n T Q σ : ℕ) : 1 ≤ (pcpParams n T Q σ).k

noncomputable def MIPRE.TM.CookLevin.Pad.pcpModulus (n T Q σ : ℕ) : Cost.BitStr

Equations

• MIPRE.TM.CookLevin.Pad.pcpModulus n T Q σ = MIPRE.LowDegree.BinaryPolynomial.shoupLowerCoeffs.toFun (MIPRE.Cost.unary (MIPRE.TM.CookLevin.Pad.pcpParams n T Q σ).k)

theorem MIPRE.TM.CookLevin.Pad.pcpModulus_length (n T Q σ : ℕ) : List.length (pcpModulus n T Q σ) = (pcpParams n T Q σ).k

theorem MIPRE.TM.CookLevin.Pad.pcpModulus_ne_nil (n T Q σ : ℕ) : pcpModulus n T Q σ ≠ []

theorem MIPRE.TM.CookLevin.Pad.viewFormat_typed (P : SAT.PcpParams) (E : SAT.BinField P.k) (z : Fin P.m' → E.carrier) (α : Fin 5 → E.carrier) (β : Fin (P.m' + 1) → E.carrier) : SAT.ViewFormat P (E.vecBits z) (E.vecBits α ++ E.vecBits β)

theorem MIPRE.TM.CookLevin.Pad.verifierCircuitValue_typed (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (hV : SAT.Valid D n T Q σ x y) (E : SAT.BinField (pcpParams n T Q σ).k) [CharP E.carrier 2] (root : E.carrier) (hroot : root ^ List.length (pcpModulus n T Q σ) = LowDegree.BinaryPolynomial.evalBits root (pcpModulus n T Q σ)) (hencode : ∀ (a : E.carrier), LowDegree.BinaryPolynomial.evalBits root (E.toBits a) = a) (z : Fin (pcpParams n T Q σ).m' → E.carrier) (α : Fin 5 → E.carrier) (β : Fin ((pcpParams n T Q σ).m' + 1) → E.carrier) : LowDegree.BinaryPolynomial.evalBits root (verifierCircuitValue.toFun (SAT.pcpInput D n T Q σ x y (E.vecBits z) (E.vecBits α ++ E.vecBits β))) = (MvPolynomial.eval z) (clausePolynomial D n T Q σ x y hV)

The raw circuit value decodes to the fixed typed clause polynomial.

theorem MIPRE.TM.CookLevin.Pad.verifierTests_typed_iff (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (hV : SAT.Valid D n T Q σ x y) (E : SAT.BinField (pcpParams n T Q σ).k) [CharP E.carrier 2] (root : E.carrier) (hroot : root ^ List.length (pcpModulus n T Q σ) = LowDegree.BinaryPolynomial.evalBits root (pcpModulus n T Q σ)) (hencode : ∀ (a : E.carrier), LowDegree.BinaryPolynomial.evalBits root (E.toBits a) = a) (faithful : ∀ (a b : Cost.BitStr), List.length a = (pcpParams n T Q σ).k → List.length b = (pcpParams n T Q σ).k → (LowDegree.BinaryPolynomial.evalBits root a = LowDegree.BinaryPolynomial.evalBits root b ↔ a = b)) (z : Fin (pcpParams n T Q σ).m' → E.carrier) (α : Fin 5 → E.carrier) (β : Fin ((pcpParams n T Q σ).m' + 1) → E.carrier) : verifierTests.toFun (SAT.pcpInput D n T Q σ x y (E.vecBits z) (E.vecBits α ++ E.vecBits β)) = true ↔ SAT.PcpAlgebra.TypedAccepts (clausePolynomial D n T Q σ x y hV) z (α, β)

With faithful coefficient decoding, the executable field tests on a typed view are the algebraic PCP tests for its fixed clause polynomial.