Executable field arithmetic for the two PCP tests

The literal list contains pairs of claimed answer values and sign coordinates. The certificate list contains pairs of claimed certificate values and point coordinates. The surrounding verifier supplies their prescribed lengths.

def MIPRE.SAT.PcpFieldTests.literalProduct (p : Cost.BitStr) (l : List (Cost.BitStr × Cost.BitStr)) : Cost.BitStr

Equations

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

def MIPRE.SAT.PcpFieldTests.formulaValue (p φ : Cost.BitStr) (l : List (Cost.BitStr × Cost.BitStr)) : Cost.BitStr

Equations

• MIPRE.SAT.PcpFieldTests.formulaValue p φ l = MIPRE.LowDegree.BinaryPolynomial.mulReduce p φ (MIPRE.SAT.PcpFieldTests.literalProduct p l)

def MIPRE.SAT.PcpFieldTests.certificateTerm (p : Cost.BitStr) (a : Cost.BitStr × Cost.BitStr) : Cost.BitStr

Equations

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

def MIPRE.SAT.PcpFieldTests.certificateValue (p : Cost.BitStr) (l : List (Cost.BitStr × Cost.BitStr)) : Cost.BitStr

Equations

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

def MIPRE.SAT.PcpFieldTests.CorrectPairs (p : Cost.BitStr) (l : List (Cost.BitStr × Cost.BitStr)) : Prop

Equations

• MIPRE.SAT.PcpFieldTests.CorrectPairs p l = ∀ a ∈ l, List.length a.1 = List.length p ∧ List.length a.2 = List.length p

theorem MIPRE.SAT.PcpFieldTests.length_formulaValue (p φ : Cost.BitStr) (l : List (Cost.BitStr × Cost.BitStr)) (hφ : List.length φ = List.length p) : List.length (formulaValue p φ l) = List.length p

theorem MIPRE.SAT.PcpFieldTests.length_certificateTerm (p : Cost.BitStr) (a : Cost.BitStr × Cost.BitStr) (ha : List.length a.1 = List.length p) : List.length (certificateTerm p a) = List.length p

theorem MIPRE.SAT.PcpFieldTests.length_certificateValue (p : Cost.BitStr) (l : List (Cost.BitStr × Cost.BitStr)) (hl : CorrectPairs p l) : List.length (certificateValue p l) = List.length p

theorem MIPRE.SAT.PcpFieldTests.eval_literalProduct {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (p : Cost.BitStr) (hp : p ≠ []) (hroot : z ^ List.length p = LowDegree.BinaryPolynomial.evalBits z p) (l : List (Cost.BitStr × Cost.BitStr)) (hl : CorrectPairs p l) : LowDegree.BinaryPolynomial.evalBits z (literalProduct p l) = (List.map (fun (a : Cost.BitStr × Cost.BitStr) => LowDegree.BinaryPolynomial.evalBits z a.1 - LowDegree.BinaryPolynomial.evalBits z a.2) l).prod

theorem MIPRE.SAT.PcpFieldTests.eval_formulaValue {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (p : Cost.BitStr) (hp : p ≠ []) (hroot : z ^ List.length p = LowDegree.BinaryPolynomial.evalBits z p) (φ : Cost.BitStr) (hφ : List.length φ = List.length p) (l : List (Cost.BitStr × Cost.BitStr)) (hl : CorrectPairs p l) : LowDegree.BinaryPolynomial.evalBits z (formulaValue p φ l) = LowDegree.BinaryPolynomial.evalBits z φ * (List.map (fun (a : Cost.BitStr × Cost.BitStr) => LowDegree.BinaryPolynomial.evalBits z a.1 - LowDegree.BinaryPolynomial.evalBits z a.2) l).prod

theorem MIPRE.SAT.PcpFieldTests.eval_certificateTerm {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (p : Cost.BitStr) (hp : p ≠ []) (hroot : z ^ List.length p = LowDegree.BinaryPolynomial.evalBits z p) (a : Cost.BitStr × Cost.BitStr) (ha : List.length a.1 = List.length p) (hb : List.length a.2 = List.length p) : LowDegree.BinaryPolynomial.evalBits z (certificateTerm p a) = LowDegree.BinaryPolynomial.evalBits z a.1 * (LowDegree.BinaryPolynomial.evalBits z a.2 * (1 - LowDegree.BinaryPolynomial.evalBits z a.2))

theorem MIPRE.SAT.PcpFieldTests.eval_certificateValue {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (p : Cost.BitStr) (hp : p ≠ []) (hroot : z ^ List.length p = LowDegree.BinaryPolynomial.evalBits z p) (l : List (Cost.BitStr × Cost.BitStr)) (hl : CorrectPairs p l) : LowDegree.BinaryPolynomial.evalBits z (certificateValue p l) = (List.map (fun (a : Cost.BitStr × Cost.BitStr) => LowDegree.BinaryPolynomial.evalBits z a.1 * (LowDegree.BinaryPolynomial.evalBits z a.2 * (1 - LowDegree.BinaryPolynomial.evalBits z a.2))) l).sum

noncomputable def MIPRE.SAT.PcpFieldTests.literalProductProg : Cost.PolyTimeFun (Cost.BitStr × List (Cost.BitStr × Cost.BitStr)) Cost.BitStr

Equations

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

@[simp]

theorem MIPRE.SAT.PcpFieldTests.literalProductProg_apply (p : Cost.BitStr) (l : List (Cost.BitStr × Cost.BitStr)) : literalProductProg.toFun (p, l) = literalProduct p l

noncomputable def MIPRE.SAT.PcpFieldTests.formulaValueProg : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr × List (Cost.BitStr × Cost.BitStr)) Cost.BitStr

Equations

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

@[simp]

theorem MIPRE.SAT.PcpFieldTests.formulaValueProg_apply (p φ : Cost.BitStr) (l : List (Cost.BitStr × Cost.BitStr)) : formulaValueProg.toFun (p, φ, l) = formulaValue p φ l

noncomputable def MIPRE.SAT.PcpFieldTests.certificateTermProg : Cost.PolyTimeFun ((Cost.BitStr × Cost.BitStr) × Cost.BitStr) Cost.BitStr

Equations

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

@[simp]

theorem MIPRE.SAT.PcpFieldTests.certificateTermProg_apply (a : Cost.BitStr × Cost.BitStr) (p : Cost.BitStr) : certificateTermProg.toFun (a, p) = certificateTerm p a

noncomputable def MIPRE.SAT.PcpFieldTests.certificateValueProg : Cost.PolyTimeFun (Cost.BitStr × List (Cost.BitStr × Cost.BitStr)) Cost.BitStr

Equations

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

@[simp]

theorem MIPRE.SAT.PcpFieldTests.certificateValueProg_apply (p : Cost.BitStr) (l : List (Cost.BitStr × Cost.BitStr)) : certificateValueProg.toFun (p, l) = certificateValue p l

@[reducible, inline]

abbrev MIPRE.SAT.PcpFieldTests.TestInput : Type

Modulus, circuit value, claimed main certificate, literals, and zero terms.

Equations

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

def MIPRE.SAT.PcpFieldTests.checks (a : TestInput) : Bool

Equations

• MIPRE.SAT.PcpFieldTests.checks a = (decide (a.2.2.1 = MIPRE.SAT.PcpFieldTests.formulaValue a.1 a.2.1 a.2.2.2.1) && decide (a.2.2.1 = MIPRE.SAT.PcpFieldTests.certificateValue a.1 a.2.2.2.2))

noncomputable def MIPRE.SAT.PcpFieldTests.checksProg : Cost.PolyTimeFun TestInput Bool

Both raw coefficient-vector equality tests, as one uniform ambient program.

Equations

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

@[simp]

theorem MIPRE.SAT.PcpFieldTests.checksProg_apply (a : TestInput) : checksProg.toFun a = checks a

theorem MIPRE.SAT.PcpFieldTests.checksProg_true_iff {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (p : Cost.BitStr) (hp : p ≠ []) (hroot : z ^ List.length p = LowDegree.BinaryPolynomial.evalBits z p) (faithful : ∀ (a b : Cost.BitStr), List.length a = List.length p → List.length b = List.length p → (LowDegree.BinaryPolynomial.evalBits z a = LowDegree.BinaryPolynomial.evalBits z b ↔ a = b)) (φ β : Cost.BitStr) (hφ : List.length φ = List.length p) (hβ : List.length β = List.length p) (lits certs : List (Cost.BitStr × Cost.BitStr)) (hl : CorrectPairs p lits) (hc : CorrectPairs p certs) : checksProg.toFun (p, φ, β, lits, certs) = true ↔ LowDegree.BinaryPolynomial.evalBits z β = LowDegree.BinaryPolynomial.evalBits z φ * (List.map (fun (a : Cost.BitStr × Cost.BitStr) => LowDegree.BinaryPolynomial.evalBits z a.1 - LowDegree.BinaryPolynomial.evalBits z a.2) lits).prod ∧ LowDegree.BinaryPolynomial.evalBits z β = (List.map (fun (a : Cost.BitStr × Cost.BitStr) => LowDegree.BinaryPolynomial.evalBits z a.1 * (LowDegree.BinaryPolynomial.evalBits z a.2 * (1 - LowDegree.BinaryPolynomial.evalBits z a.2))) certs).sum

Faithful coefficient decoding converts the two executable equality checks into precisely the two algebraic field identities.