The bespoke PCP for deciders: the statement

MIPRE.SAT.PcpDecider is blueprint thm:pcp-decider — the paper's theorem of the same name in answer_reduction.tex — the classical half of answer reduction: a verifier that, given a decider specification and a PCP view (a point z ∈ 𝔽_q^{m'} and a claimed evaluation of the proof at z), accepts an honest low-degree proof with probability 1 and forces any low-degree proof accepted with probability more than 1/2 to encode answers the decider accepts. It consumes lem:decoupled-5sat — the decoupled 5SAT description of the decider is what the proof's constraint polynomials arithmetize — and lem:schwartz-zippel.

Stated here, before anything is proved, so that the consumers in chapter 6 (ld_compiler.tex's typed PCP sampler, and thm:answer-reduction through it) can be written against it, exactly as SuccinctCookLevin and DecoupledDescriber were stated before being inhabited.

What the statement needs

• BinField k — a field of size 2^k with a fixed k-bit representation of its elements. The paper's admissible field size is q = 2^k with k odd and the representation is the one the self-dual normal basis of lem:self-dual-basis supplies; all the statement needs is the size and the representation. SAT.QuotientField.shoupAdmissibleField supplies this interface in the polynomial power basis, with uniform addition and multiplication programs. Consumers requiring a self-dual normal basis still need lem:self-dual-basis.
• PcpParams — def:pcpparams. Only k, m, s are data: d = 7 and m' = 5m + 5 + s are determined, and the paper's q is 2^k.
• PcpProof — def:pcp-proof: five m-variate polynomials and m' + 1 m'-variate ones, all of individual degree at most d.
• PcpProof.ev — def:pcp-eval, the evaluation (α₁ … α₅, β₀ … β_{m'}) at a point, with αᵢ = gᵢ(xᵢ) reading the i-th of the five m-coordinate blocks of z (PcpParams.block).
• ViewFormat — the format check item 1 requires the verifier to perform, and PcpProof.rawView the honest view in the verifier's bit-level input format.

Two things this statement carries, and one it does not

It carries the blueprint's repair of a confirmed source defect (rem:pcp-power-of-two): both m and m' are required to be powers of two dividing q, where the source's padding guarantees it only for the outer m'. Without the inner one the conditionally linear functions of the m-variate test's lines are ill defined.

It does not carry the source's lower bound on q (eq:pcp-q-choice, q ≥ (max\{Q,2\} · a'(d m'(m'+6))^{a'})^{1/b'}), which is stated in terms of the universal constants of thm:lidt-cl-soundness and is consumed not here but in ld_compiler.tex, where the answer-reduced verifier's soundness error is assembled. The blueprint's statement of thm:pcp-decider does not state it either; when the consumer is written it will need to be added here or re-derived there, and that is a deliberate gap rather than an oversight.

One convention fixed here

The paper identifies {0,1}^m with {1, …, M}, M = 2^m, "using, say, the lexicographic ordering on strings". Any fixed bijection will do, and the one fixed here is the repository's existing little-endian bitsVal/bitsOfNat convention (Cost.bitsVal (List.ofFn w)), so that the low-degree encoding of an answer block agrees with the tape indexing tapeBits that thm:succinct-sat and lem:decoupled-5sat already use. The choice is invisible to the statement's content, since the same bijection appears in the encoding and in the decoding.

Admissible fields with a bit representation

structure MIPRE.SAT.BinField (k : ℕ) : Type 1

A field of size 2^k together with a fixed k-bit representation of its elements.

• carrier : Type

  The field.

• instField : Field self.carrier

  Its field structure.

• instFintype : Fintype self.carrier

  It is finite.

• instDecidableEq : DecidableEq self.carrier

  Equality is decidable, so the decoding map Coded is defined.

• card_carrier : Fintype.card self.carrier = 2 ^ k

  It has 2^k elements.

• toBits : self.carrier → Cost.BitStr

  The representation of an element as k bits.

• ofBits : Cost.BitStr → self.carrier

  Reading a representation back.

• length_toBits (a : self.carrier) : List.length (self.toBits a) = k
• ofBits_toBits (a : self.carrier) : self.ofBits (self.toBits a) = a

def MIPRE.SAT.BinField.vecBits {k : ℕ} (E : BinField k) {n : ℕ} (v : Fin n → E.carrier) : List Cost.BitStr

A vector of field elements as a list of k-bit blocks.

Equations

• E.vecBits v = List.map E.toBits (List.ofFn v)

@[simp]

theorem MIPRE.SAT.BinField.length_vecBits {k : ℕ} (E : BinField k) {n : ℕ} (v : Fin n → E.carrier) : (E.vecBits v).length = n

theorem MIPRE.SAT.BinField.width_vecBits {k : ℕ} (E : BinField k) {n : ℕ} (v : Fin n → E.carrier) {b : Cost.BitStr} (hb : b ∈ E.vecBits v) : List.length b = k

The parameters

structure MIPRE.SAT.PcpParams : Type

The PCP parameters (q, m, d, m', s) = pcpparams(n, T, Q, σ) of def:pcpparams. Only k, m, s are data: q = 2^k, d = 7 and m' = 5m + 5 + s.

• k : ℕ

  q = 2^k, k odd for an admissible field size.

• m : ℕ

  The number of variables of the answer polynomials; M = 2^m ≥ 2T.

• s : ℕ

  The number of auxiliary variables supplied by the padded succinct describer.

def MIPRE.SAT.PcpParams.d : ℕ

The individual degree bound of the proof polynomials, d = 7.

Equations

• MIPRE.SAT.PcpParams.d = 7

def MIPRE.SAT.PcpParams.q (P : PcpParams) : ℕ

The field size q = 2^k.

Equations

• P.q = 2 ^ P.k

def MIPRE.SAT.PcpParams.m' (P : PcpParams) : ℕ

The number of variables of the constraint polynomials, m' = 5m + 5 + s.

Equations

• P.m' = 5 * P.m + 5 + P.s

theorem MIPRE.SAT.PcpParams.five_mul_m_le (P : PcpParams) : 5 * P.m ≤ P.m'

def MIPRE.SAT.PcpParams.block (P : PcpParams) {F : Type u_1} (i : Fin 5) (z : Fin P.m' → F) : Fin P.m → F

The i-th of the five m-coordinate blocks x₁, …, x₅ of a point of F^{m'}.

Equations

• P.block i z j = z ⟨↑i * P.m + ↑j, ⋯⟩

Proofs and views

structure MIPRE.SAT.PcpProof (P : PcpParams) (F : Type u_1) [CommRing F] : Type u_1

A low-degree PCP proof (def:pcp-proof): five m-variate polynomials g₁ … g₅ and m' + 1 m'-variate polynomials c₀ … c_{m'}, all of individual degree at most d.

• g : Fin 5 → MvPolynomial (Fin P.m) F

  The answer polynomials g₁, …, g₅.

• c : Fin (P.m' + 1) → MvPolynomial (Fin P.m') F

  The constraint polynomials c₀, …, c_{m'}.

• degreeOf_g (t : Fin 5) (i : Fin P.m) : MvPolynomial.degreeOf i (self.g t) ≤ PcpParams.d
• degreeOf_c (t : Fin (P.m' + 1)) (i : Fin P.m') : MvPolynomial.degreeOf i (self.c t) ≤ PcpParams.d

def MIPRE.SAT.PcpProof.ev {P : PcpParams} {F : Type u_1} [CommRing F] (pf : PcpProof P F) (z : Fin P.m' → F) : (Fin 5 → F) × (Fin (P.m' + 1) → F)

ev_z(Π) of def:pcp-eval: the five αᵢ = gᵢ(xᵢ) and the m' + 1 βⱼ = cⱼ(z).

Equations

• pf.ev z = (fun (i : Fin 5) => (MvPolynomial.eval (P.block i z)) (pf.g i), fun (j : Fin (P.m' + 1)) => (MvPolynomial.eval z) (pf.c j))

def MIPRE.SAT.PcpProof.rawView {P : PcpParams} {k : ℕ} (E : BinField k) (pf : PcpProof P E.carrier) (z : Fin P.m' → E.carrier) : List Cost.BitStr × List Cost.BitStr

The honest view at z in the verifier's input format: the bits of z, then the bits of ev_z(Π) with the five αᵢ before the m' + 1 βⱼ.

Equations

• MIPRE.SAT.PcpProof.rawView E pf z = (E.vecBits z, E.vecBits (pf.ev z).1 ++ E.vecBits (pf.ev z).2)

@[reducible, inline]

abbrev MIPRE.SAT.PcpInput : Type

The verifier's input: a decider specification (DescInput) together with a PCP view, the point and the claimed evaluation each a list of k-bit blocks.

Equations

• MIPRE.SAT.PcpInput = (MIPRE.SAT.DescInput × List MIPRE.Cost.BitStr × List MIPRE.Cost.BitStr)

def MIPRE.SAT.pcpInput (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (z ev : List Cost.BitStr) : PcpInput

The verifier's input, assembled.

Equations

• MIPRE.SAT.pcpInput D n T Q σ x y z ev = (((D, n, T, Q, σ), x, y), z, ev)

structure MIPRE.SAT.ViewFormat (P : PcpParams) (z ev : List Cost.BitStr) : Prop

The PCP view is formatted correctly: m' blocks for the point, 6 + m' for the claimed evaluation, each of k bits. Item 1 of the theorem asks the verifier to reject otherwise.

• length_z : z.length = P.m'
• length_ev : ev.length = 6 + P.m'
• width_z (b : Cost.BitStr) : b ∈ z → List.length b = P.k
• width_ev (b : Cost.BitStr) : b ∈ ev → List.length b = P.k

theorem MIPRE.SAT.viewFormat_rawView {P : PcpParams} {k : ℕ} (E : BinField k) (hk : P.k = k) (pf : PcpProof P E.carrier) (z : Fin P.m' → E.carrier) : ViewFormat P (PcpProof.rawView E pf z).1 (PcpProof.rawView E pf z).2

The answer blocks as subcube-indexed vectors

def MIPRE.SAT.answerVec (F : Type u_1) [CommRing F] (m : ℕ) (ap : Cost.BitStr) : (Fin m → Bool) → F

The answer block of a string ap, as a {0,1}^m-indexed vector of field elements: the tape encoding tapeBits read at the little-endian index of the subcube point. This is the paper's a = enc_Γ(a_prefix, ⊔^{M/2 - ℓ}), viewed in F^M through {0,1} ⊆ F.

Equations

• MIPRE.SAT.answerVec F m ap w = MIPRE.LowDegree.ofBool (MIPRE.SAT.tapeBits ap (MIPRE.Cost.bitsVal (List.ofFn w)))

The theorem

structure MIPRE.SAT.PcpDecider : Type 1

The bespoke PCP for deciders (blueprint thm:pcp-decider). An instance of this structure is the theorem.

• params : ℕ → ℕ → ℕ → ℕ → PcpParams

  pcpparams(n, T, Q, σ).

• fld (k : ℕ) : Odd k → BinField k

  The field of size q = 2^k with its k-bit representation, for each admissible (odd) extension degree. In particular this excludes k = 0, for which BinField k would require a one-element field.

• verify : Cost.PolyTimeFun PcpInput Bool

  The verifier.

• paramsProg : Cost.PolyTimeFun (ℕ × ℕ × ℕ × ℕ) (ℕ × ℕ × ℕ)

  The parameters, in polynomial time from (n, T, Q, σ).

• paramsProg_eq (n T Q σ : ℕ) : self.paramsProg.toFun (n, T, Q, σ) = ((self.params n T Q σ).k, (self.params n T Q σ).m, (self.params n T Q σ).s)
• odd_k (n T Q σ : ℕ) : Odd (self.params n T Q σ).k

  The field size is admissible: k is odd.

• two_mul_le (n T Q σ : ℕ) : 2 * T ≤ 2 ^ (self.params n T Q σ).m

  m is chosen so that M = 2^m ≥ 2T, as the padded succinct describer chooses it.

• m'_isPow (n T Q σ : ℕ) : ∃ (j : ℕ), (self.params n T Q σ).m' = 2 ^ j

  m' is a power of two: the padding step of the PCP, def:pcpparams.

• m'_dvd_q (n T Q σ : ℕ) : (self.params n T Q σ).m' ∣ (self.params n T Q σ).q

  m' ∣ q, which the m'-variate low-degree test's diagonal lines need.

• m_isPow (n T Q σ : ℕ) : ∃ (j : ℕ), (self.params n T Q σ).m = 2 ^ j

  m is a power of two as well. This is the blueprint's repair of a confirmed defect in the source (rem:pcp-power-of-two): the source's padding guarantees a power of two only for the outer count m', while the m-variate low-degree test applied to the answer polynomials needs m ∣ q for the inner m too.

• m_dvd_q (n T Q σ : ℕ) : (self.params n T Q σ).m ∣ (self.params n T Q σ).q

  m ∣ q, the hypothesis rem:pcp-power-of-two says a formalization must state.

• reject_invalid (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (z ev : List Cost.BitStr) : ¬Valid D n T Q σ x y ∨ ¬ViewFormat (self.params n T Q σ) z ev → self.verify.toFun (pcpInput D n T Q σ x y z ev) = false

  Item 1: the verifier rejects an invalid specification or a misformatted view.

• time_le : ∃ (R : Polynomial ℕ), ∀ (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (z ev : List Cost.BitStr), Valid D n T Q σ x y → ViewFormat (self.params n T Q σ) z ev → ∃ t ≤ Polynomial.eval (n.size + T.size + Q + σ) R, self.verify.code.Runs (Cost.encode (pcpInput D n T Q σ x y z ev)) (Cost.encode (self.verify.toFun (pcpInput D n T Q σ x y z ev))) t

  Item 2: the verifier runs in time poly(log T, log n, Q, σ) on formatted inputs.

• completeness (D : Decider) (n T Q σ : ℕ) (x y : Cost.BitStr) : Valid D.prog n T Q σ x y → ∀ (ap bp : Cost.BitStr), List.length ap ≤ T → List.length bp ≤ T → D.AcceptsWithin n x y ap bp T → ∃ (pf : PcpProof (self.params n T Q σ) (self.fld (self.params n T Q σ).k ⋯).carrier), pf.g 0 = LowDegree.ldEnc (answerVec (self.fld (self.params n T Q σ).k ⋯).carrier (self.params n T Q σ).m ap) ∧ pf.g 1 = LowDegree.ldEnc (answerVec (self.fld (self.params n T Q σ).k ⋯).carrier (self.params n T Q σ).m bp) ∧ ∀ (z : Fin (self.params n T Q σ).m' → (self.fld (self.params n T Q σ).k ⋯).carrier), self.verify.toFun (pcpInput D.prog n T Q σ x y (PcpProof.rawView (self.fld (self.params n T Q σ).k ⋯) pf z).1 (PcpProof.rawView (self.fld (self.params n T Q σ).k ⋯) pf z).2) = true

  Item 3 (completeness): if the decider accepts (n, x, y, ap, bp) within T, the low-degree proof whose first two answer polynomials are the low-degree encodings of the padded answers is accepted at every point.

• soundness (D : Decider) (n T Q σ : ℕ) (x y : Cost.BitStr) : Valid D.prog n T Q σ x y → ∀ (pf : PcpProof (self.params n T Q σ) (self.fld (self.params n T Q σ).k ⋯).carrier), (self.params n T Q σ).q ^ (self.params n T Q σ).m' < 2 * {z : Fin (self.params n T Q σ).m' → (self.fld (self.params n T Q σ).k ⋯).carrier | self.verify.toFun (pcpInput D.prog n T Q σ x y (PcpProof.rawView (self.fld (self.params n T Q σ).k ⋯) pf z).1 (PcpProof.rawView (self.fld (self.params n T Q σ).k ⋯) pf z).2) = true}.card → ∃ (ap : Cost.BitStr) (bp : Cost.BitStr), List.length ap ≤ T ∧ List.length bp ≤ T ∧ D.AcceptsWithin n x y ap bp T ∧ LowDegree.coded (pf.g 0) = answerVec (self.fld (self.params n T Q σ).k ⋯).carrier (self.params n T Q σ).m ap ∧ LowDegree.coded (pf.g 1) = answerVec (self.fld (self.params n T Q σ).k ⋯).carrier (self.params n T Q σ).m bp

  Item 4 (soundness): a low-degree proof accepted at more than half the points decodes to answers the decider accepts within T.