The answer-reduced decision predicate

Piece AR-3b of planning/answer-reduction.md: the decision procedure D̂^ar of the paper's fig:decider-pcp (ld_compiler.tex), on parsed answers, as a Boolean predicate.

A type of the answer-reduced verifier is a pair (r, t) of an oracularization role r and a PCP type t = (i, τ), a copy of the low-degree test and a test type. A question carries, besides the type, the oracle part x_Q (whatever the input sampler's seed space is: a type parameter X here) and the PCP part, a vector of V^pcp. An answer is an answer of the copy's low-degree test: of the m-variable test with one codeword for the first five copies, of the m'-variable test with m' + 6 codewords for the sixth (Ans). The oracle answers of the input verifier are never sent: that is the answer reduction.

The predicate (accepts) is the format preamble and then the five steps, each for both players:

1. equal types, equal answers;
2. the oracle's Point_6 answer against an isolated player v's Point_v answer, on the v-th component (α'_v = α_v), v = 1, 2 for Alice and Bob;
3. an isolated player's own input codeword, on copy v: the m-variable low-degree test;
4. between two oracles, on copies 3, 4, 5: the consistency α_i = α'_i against copy 6, and the individual m-variable low-degree test; on copy 6, the simultaneous m'-variable test with m' + 6 codewords;
5. the game check: an oracle's Point_6 answer, with the point, is a PCP view, and the PCP verifier (check, a parameter here) must accept it.

The format preamble checks every answer, including those no step reads (the paper's round-12 repair to its preamble): each answer must be of its copy's test and of the format its test type prescribes (ansFmt).

@[reducible, inline]

abbrev MIPRE.AnswerReduction.dPcp : ℕ

The individual degree bound of the PCP, d = 7.

Equations

• MIPRE.AnswerReduction.dPcp = MIPRE.SAT.PcpParams.d

@[reducible, inline]

abbrev MIPRE.AnswerReduction.Ans (P : SAT.PcpParams) (F : Type u_1) : Type u_1

Answers of the answer-reduced verifier: an answer of the m-variable test with one codeword (copies 1–5), or of the m'-variable test with m' + 6 codewords (copy 6).

Equations

• MIPRE.AnswerReduction.Ans P F = (MIPRE.LIDT.CL.Answer F P.m MIPRE.AnswerReduction.dPcp 1 ⊕ MIPRE.LIDT.CL.Answer F P.m' MIPRE.AnswerReduction.dPcp (P.m' + 6))

def MIPRE.AnswerReduction.tyFmt {F : Type u_1} {n d ldc : ℕ} : LIDT.CL.Ty → LIDT.CL.Answer F n d ldc → Bool

The format a test type prescribes, on an answer of any test.

Equations

• MIPRE.AnswerReduction.tyFmt MIPRE.LIDT.CL.Ty.point (MIPRE.LIDT.CL.Answer.values a) = true
• MIPRE.AnswerReduction.tyFmt MIPRE.LIDT.CL.Ty.aline (MIPRE.LIDT.CL.Answer.apolys f) = true
• MIPRE.AnswerReduction.tyFmt MIPRE.LIDT.CL.Ty.dline (MIPRE.LIDT.CL.Answer.dpolys f) = true
• MIPRE.AnswerReduction.tyFmt x✝¹ x✝ = false

def MIPRE.AnswerReduction.ansFmt {P : SAT.PcpParams} {F : Type u_1} (t : Pcp.PcpTy) : Ans P F → Bool

The format preamble for one answer: of its copy's test, in its type's format.

Equations

• MIPRE.AnswerReduction.ansFmt t (Sum.inl a) = (decide (↑t.1 < 5) && MIPRE.AnswerReduction.tyFmt t.2 a)
• MIPRE.AnswerReduction.ansFmt t (Sum.inr a) = (decide (↑t.1 = 5) && MIPRE.AnswerReduction.tyFmt t.2 a)

def MIPRE.AnswerReduction.val1 {P : SAT.PcpParams} {F : Type u_1} [Field F] : Ans P F → F

The single value of a point answer of copies 1–5, 0 otherwise.

Equations

• MIPRE.AnswerReduction.val1 (Sum.inl (MIPRE.LIDT.CL.Answer.values a)) = a 0
• MIPRE.AnswerReduction.val1 x✝ = 0

def MIPRE.AnswerReduction.val6 {P : SAT.PcpParams} {F : Type u_1} [Field F] (i : Fin (P.m' + 6)) : Ans P F → F

The i-th component of a Point_6 answer, 0 otherwise. The first five components are the α'_i, the rest the β_j of the constraint polynomials.

Equations

• MIPRE.AnswerReduction.val6 i (Sum.inr (MIPRE.LIDT.CL.Answer.values a)) = a i
• MIPRE.AnswerReduction.val6 i x✝ = 0

def MIPRE.AnswerReduction.vals6 {P : SAT.PcpParams} {F : Type u_1} [Field F] : Ans P F → Fin (P.m' + 6) → F

The point answer of copy 6 as a vector, 0 otherwise: the PCP view's evaluation part.

Equations

• MIPRE.AnswerReduction.vals6 (Sum.inr (MIPRE.LIDT.CL.Answer.values a)) = a
• MIPRE.AnswerReduction.vals6 x✝ = 0

def MIPRE.AnswerReduction.ans1 {P : SAT.PcpParams} {F : Type u_1} [Field F] : Ans P F → LIDT.CL.Answer F P.m dPcp 1

The m-variable test's answer, the zero point answer otherwise.

Equations

• MIPRE.AnswerReduction.ans1 (Sum.inl a) = a
• MIPRE.AnswerReduction.ans1 x✝ = MIPRE.LIDT.CL.Answer.values 0

def MIPRE.AnswerReduction.ans6 {P : SAT.PcpParams} {F : Type u_1} [Field F] : Ans P F → LIDT.CL.Answer F P.m' dPcp (P.m' + 6)

The m'-variable test's answer, the zero point answer otherwise.

Equations

• MIPRE.AnswerReduction.ans6 (Sum.inr a) = a
• MIPRE.AnswerReduction.ans6 x✝ = MIPRE.LIDT.CL.Answer.values 0

def MIPRE.AnswerReduction.roleIdx : Role → Option (Fin 5)

The index v - 1 of the input codeword an isolated player's role names: 0 for Alice, 1 for Bob.

Equations

• MIPRE.AnswerReduction.roleIdx MIPRE.Role.oracle = none
• MIPRE.AnswerReduction.roleIdx MIPRE.Role.alice = some 0
• MIPRE.AnswerReduction.roleIdx MIPRE.Role.bob = some 1

noncomputable def MIPRE.AnswerReduction.q6 {P : SAT.PcpParams} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {hm' : P.m' ∣ Fintype.card F} (S' : LIDT.CL.Sel F P.m' hm') (τ : LIDT.CL.Ty) (x : Pcp.Coord P → F) : LIDT.CL.Question F P.m'

The m'-variable test's question of copy 6 at a vector.

Equations

• MIPRE.AnswerReduction.q6 S' τ x = MIPRE.LIDT.CL.Sample.question hm' ((MIPRE.AnswerReduction.Pcp.regs6 P).sampleOf S' τ x) τ

noncomputable def MIPRE.AnswerReduction.q1 {P : SAT.PcpParams} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [NeZero P.m] {hm : P.m ∣ Fintype.card F} (S : LIDT.CL.Sel F P.m hm) (i : Fin 5) (τ : LIDT.CL.Ty) (x : Pcp.Coord P → F) : LIDT.CL.Question F P.m

The m-variable test's question of copy i ≤ 5 at a vector.

Equations

• MIPRE.AnswerReduction.q1 S i τ x = MIPRE.LIDT.CL.Sample.question hm ((MIPRE.AnswerReduction.Pcp.regs P i).sampleOf S τ x) τ

@[reducible, inline]

abbrev MIPRE.AnswerReduction.Q (P : SAT.PcpParams) (F : Type u_3) (X : Type u_4) : Type (max u_3 u_4)

A question of the answer-reduced verifier, decoded: the type, the oracle part and the PCP vector.

Equations

• MIPRE.AnswerReduction.Q P F X = ((MIPRE.Role × MIPRE.AnswerReduction.Pcp.PcpTy) × X × (MIPRE.AnswerReduction.Pcp.Coord P → F))

noncomputable def MIPRE.AnswerReduction.side {P : SAT.PcpParams} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [NeZero P.m] {hm : P.m ∣ Fintype.card F} {hm' : P.m' ∣ Fintype.card F} (S : LIDT.CL.Sel F P.m hm) (S' : LIDT.CL.Sel F P.m' hm') {X : Type u_2} (check : X → (Fin P.m' → F) → (Fin (P.m' + 6) → F) → Bool) (p q : Q P F X) (a b : Ans P F) : Bool

One side of the five steps, for the player asked p and answering a, against the other player asked q and answering b. check x z α is the PCP verifier's decision on the view (z, α) for the input question pair read off the oracle part x.

Equations

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

noncomputable def MIPRE.AnswerReduction.accepts {P : SAT.PcpParams} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [NeZero P.m] {hm : P.m ∣ Fintype.card F} {hm' : P.m' ∣ Fintype.card F} (S : LIDT.CL.Sel F P.m hm) (S' : LIDT.CL.Sel F P.m' hm') {X : Type u_2} (check : X → (Fin P.m' → F) → (Fin (P.m' + 6) → F) → Bool) (p q : Q P F X) (a b : Ans P F) : Bool

The answer-reduced decision predicate (fig:decider-pcp): the format preamble, the global consistency check, and the other four steps for both players.

Equations

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