The raw field tests on typed PCP views

def MIPRE.SAT.PcpViewTests.literals (P : PcpParams) (z ev : List Cost.BitStr) : List (Cost.BitStr × Cost.BitStr)

Equations

• MIPRE.SAT.PcpViewTests.literals P z ev = (List.take 5 ev).zip (List.take 5 (List.drop (5 * P.m) z))

def MIPRE.SAT.PcpViewTests.certificates (z ev : List Cost.BitStr) : List (Cost.BitStr × Cost.BitStr)

Equations

• MIPRE.SAT.PcpViewTests.certificates z ev = (List.drop 6 ev).zip z

theorem MIPRE.SAT.PcpViewTests.main_claim {k : ℕ} (E : BinField k) (P : PcpParams) (α : Fin 5 → E.carrier) (β : Fin (P.m' + 1) → E.carrier) : (E.vecBits α ++ E.vecBits β).getD 5 [] = E.toBits (β 0)

theorem MIPRE.SAT.PcpViewTests.tail_claims {k : ℕ} (E : BinField k) (P : PcpParams) (α : Fin 5 → E.carrier) (β : Fin (P.m' + 1) → E.carrier) : List.drop 6 (E.vecBits α ++ E.vecBits β) = E.vecBits fun (i : Fin P.m') => β i.succ

theorem MIPRE.SAT.PcpViewTests.literals_vecBits {k : ℕ} (E : BinField k) (P : PcpParams) (z : Fin P.m' → E.carrier) (α : Fin 5 → E.carrier) (β : Fin (P.m' + 1) → E.carrier) : literals P (E.vecBits z) (E.vecBits α ++ E.vecBits β) = List.ofFn fun (i : Fin 5) => (E.toBits (α i), E.toBits (z (P.signIndex i)))

theorem MIPRE.SAT.PcpViewTests.certificates_vecBits {k : ℕ} (E : BinField k) (P : PcpParams) (z : Fin P.m' → E.carrier) (α : Fin 5 → E.carrier) (β : Fin (P.m' + 1) → E.carrier) : certificates (E.vecBits z) (E.vecBits α ++ E.vecBits β) = List.ofFn fun (i : Fin P.m') => (E.toBits (β i.succ), E.toBits (z i))

theorem MIPRE.SAT.PcpViewTests.correctPairs_ofFn {k : ℕ} (E : BinField k) (p : Cost.BitStr) (hpk : List.length p = k) {n : ℕ} (a b : Fin n → E.carrier) : PcpFieldTests.CorrectPairs p (List.ofFn fun (i : Fin n) => (E.toBits (a i), E.toBits (b i)))

theorem MIPRE.SAT.PcpViewTests.checks_typed_iff {k : ℕ} (E : BinField k) (P : PcpParams) [CharP E.carrier 2] (root : E.carrier) (p : Cost.BitStr) (hp : p ≠ []) (hpk : List.length p = k) (hroot : root ^ List.length p = LowDegree.BinaryPolynomial.evalBits root p) (hencode : ∀ (a : E.carrier), LowDegree.BinaryPolynomial.evalBits root (E.toBits a) = a) (faithful : ∀ (a b : Cost.BitStr), List.length a = List.length p → List.length b = List.length p → (LowDegree.BinaryPolynomial.evalBits root a = LowDegree.BinaryPolynomial.evalBits root b ↔ a = b)) (Φ : MvPolynomial (Fin P.m') E.carrier) (z : Fin P.m' → E.carrier) (φ : Cost.BitStr) (hφ : List.length φ = List.length p) (hφeval : LowDegree.BinaryPolynomial.evalBits root φ = (MvPolynomial.eval z) Φ) (α : Fin 5 → E.carrier) (β : Fin (P.m' + 1) → E.carrier) : PcpFieldTests.checksProg.toFun (p, φ, (E.vecBits α ++ E.vecBits β).getD 5 [], literals P (E.vecBits z) (E.vecBits α ++ E.vecBits β), certificates (E.vecBits z) (E.vecBits α ++ E.vecBits β)) = true ↔ PcpAlgebra.TypedAccepts Φ z (α, β)

On a typed view with canonical coefficient decoding, the executable tests are exactly TypedAccepts, including the order of all certificate coordinates.