Honest answers of the answer-reduced verifier

Piece AR-4 of planning/answer-reduction.md, the combinatorial half: the decision predicate accepts of fig:decider-pcp accepts the honest answers of two players who answer from polynomial data that is consistent in the ways the five steps check.

A player's data (HPolys) is five m-variate polynomials g₁ … g₅, one for each of the first five copies of the low-degree test, and m' + 6 m'-variate polynomials c, the codewords of the sixth copy. Its honest answer to a question of type (i, τ) (honestAns) is the honest answer (LIDT.CL.honest) of gᵢ, or of c for the sixth copy, to the seeded question the type's presentation computes. In the paper (ld_compiler.tex, the completeness part of thm:ar):

• an oracle's data is the PCP proof of its pair of answers: g₁, g₂ the low-degree encodings of the two answers, g₃ … g₅ the proof's other answer polynomials, and c the five gᵢ read on their blocks of F^{m'} followed by the constraint polynomials (HPolys.Oracle);
• an isolated player's data has for g_v the low-degree encoding of its own answer, v its role's index, and anything of low degree elsewhere (zero, in AR-4's instance).

accepts_honest is the statement: for two questions read off one PCP vector, players whose data is of individual degree at most d = 7 (HPolys.LowDeg), equal for equal roles, with the oracle's g_v the isolated player v's, and with an oracle's data passing its PCP check at every point, are accepted.

structure MIPRE.AnswerReduction.HPolys (P : SAT.PcpParams) (F : Type u_2) [Field F] : Type u_2

A player's polynomial data: the answer polynomials of the first five copies, and the codewords of the sixth.

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

  The polynomials of copies 1–5.

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

  The m' + 6 codewords of copy 6.

def MIPRE.AnswerReduction.HPolys.LowDeg {P : SAT.PcpParams} {F : Type u_1} [Field F] (H : HPolys P F) : Prop

Every polynomial has individual degree at most d = 7.

Equations

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

def MIPRE.AnswerReduction.HPolys.idx6 {P : SAT.PcpParams} (j : Fin 5) : Fin (P.m' + 6)

The index j ≤ 5 of a first-five copy among the sixth copy's codewords.

Equations

• MIPRE.AnswerReduction.HPolys.idx6 j = ⟨↑j, ⋯⟩

def MIPRE.AnswerReduction.HPolys.Oracle {P : SAT.PcpParams} {F : Type u_1} [Field F] (H : HPolys P F) (chk : (Fin P.m' → F) → (Fin (P.m' + 6) → F) → Bool) : Prop

An oracle's data: the sixth copy's first five codewords are the gⱼ read on their blocks, and every point's evaluations pass the check chk.

Equations

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

noncomputable def MIPRE.AnswerReduction.honestAns {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') (H : HPolys P F) (t : Pcp.PcpTy) (y : Pcp.Coord P → F) : Ans P F

The honest answer of a player with data H to the question of PCP type t read off y.

Equations

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

theorem MIPRE.AnswerReduction.honestAns_lt {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') (H : HPolys P F) {i : Fin 6} (τ : LIDT.CL.Ty) (y : Pcp.Coord P → F) (h : ↑i < 5) : honestAns S S' H (i, τ) y = Sum.inl (LIDT.CL.honest hm (fun (x : Fin 1) => H.g ⟨↑i, h⟩) (q1 S ⟨↑i, h⟩ τ y))

theorem MIPRE.AnswerReduction.honestAns_six {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') (H : HPolys P F) {i : Fin 6} (τ : LIDT.CL.Ty) (y : Pcp.Coord P → F) (h : ↑i = 5) : honestAns S S' H (i, τ) y = Sum.inr (LIDT.CL.honest hm' H.c (q6 S' τ y))

theorem MIPRE.AnswerReduction.ansFmt_honestAns {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') (H : HPolys P F) (t : Pcp.PcpTy) (y : Pcp.Coord P → F) : ansFmt t (honestAns S S' H t y) = true

The questions of one PCP vector

theorem MIPRE.AnswerReduction.ptOf_point_eval {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {ι : Type u_2} [DecidableEq ι] [Fintype ι] {n : ℕ} [NeZero n] {hn : n ∣ Fintype.card F} (R : LIDT.CL.Regs ι n) (Sn : LIDT.CL.Sel F n hn) (w : ι → F) : R.ptOf ((R.pres Sn LIDT.CL.Ty.point).eval w) = R.ptOf w

theorem MIPRE.AnswerReduction.pres_lt {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') (w : Pcp.Coord P → F) {i : Fin 6} (τ : LIDT.CL.Ty) (h : ↑i < 5) : (Pcp.pres P S S' (i, τ)).eval w = ((Pcp.regs P ⟨↑i, h⟩).pres S τ).eval w

theorem MIPRE.AnswerReduction.pres_six {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') (w : Pcp.Coord P → F) {i : Fin 6} (τ : LIDT.CL.Ty) (h : ↑i = 5) : (Pcp.pres P S S' (i, τ)).eval w = ((Pcp.regs6 P).pres S' τ).eval w

theorem MIPRE.AnswerReduction.ptOf_regs_point {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') (w : Pcp.Coord P → F) (v : Fin 5) : (Pcp.regs P v).ptOf ((Pcp.pres P S S' (v.castSucc, LIDT.CL.Ty.point)).eval w) = (Pcp.regs P v).ptOf w

The point of copy v's register, in the Point_v question.

theorem MIPRE.AnswerReduction.ptOf_regs_point6 {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') (w : Pcp.Coord P → F) (v : Fin 5) {i : Fin 6} (h : ↑i = 5) : (Pcp.regs P v).ptOf ((Pcp.pres P S S' (i, LIDT.CL.Ty.point)).eval w) = (Pcp.regs P v).ptOf w

The point of copy v's register, in the Point_6 question: the v-th block.

theorem MIPRE.AnswerReduction.q1_eval {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') (w : Pcp.Coord P → F) (v : Fin 5) (τ : LIDT.CL.Ty) : q1 S v τ ((Pcp.pres P S S' (v.castSucc, τ)).eval w) = LIDT.CL.Sample.question hm ((Pcp.regs P v).sampleOf S τ w) τ

theorem MIPRE.AnswerReduction.q6_eval {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') (w : Pcp.Coord P → F) {i : Fin 6} (τ : LIDT.CL.Ty) (h : ↑i = 5) : q6 S' τ ((Pcp.pres P S S' (i, τ)).eval w) = LIDT.CL.Sample.question hm' ((Pcp.regs6 P).sampleOf S' τ w) τ

Reading the honest answers

theorem MIPRE.AnswerReduction.val1_honest {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') (H : HPolys P F) (v : Fin 5) (y : Pcp.Coord P → F) : val1 (honestAns S S' H (v.castSucc, LIDT.CL.Ty.point) y) = (MvPolynomial.eval ((Pcp.regs P v).ptOf y)) (H.g v)

theorem MIPRE.AnswerReduction.val6_honest {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') (H : HPolys P F) {i : Fin 6} (h : ↑i = 5) (j : Fin (P.m' + 6)) (y : Pcp.Coord P → F) : val6 j (honestAns S S' H (i, LIDT.CL.Ty.point) y) = (MvPolynomial.eval ((Pcp.regs6 P).ptOf y)) (H.c j)

theorem MIPRE.AnswerReduction.vals6_honest {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') (H : HPolys P F) {i : Fin 6} (h : ↑i = 5) (y : Pcp.Coord P → F) : vals6 (honestAns S S' H (i, LIDT.CL.Ty.point) y) = fun (j : Fin (P.m' + 6)) => (MvPolynomial.eval ((Pcp.regs6 P).ptOf y)) (H.c j)

theorem MIPRE.AnswerReduction.ans1_honest {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') (H : HPolys P F) (v : Fin 5) (τ : LIDT.CL.Ty) (y : Pcp.Coord P → F) : ans1 (honestAns S S' H (v.castSucc, τ) y) = LIDT.CL.honest hm (fun (x : Fin 1) => H.g v) (q1 S v τ y)

theorem MIPRE.AnswerReduction.ans6_honest {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') (H : HPolys P F) {i : Fin 6} (h : ↑i = 5) (τ : LIDT.CL.Ty) (y : Pcp.Coord P → F) : ans6 (honestAns S S' H (i, τ) y) = LIDT.CL.honest hm' H.c (q6 S' τ y)

theorem MIPRE.AnswerReduction.accepts_q1_honest {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') {g : MvPolynomial (Fin P.m) F} (hg : ∀ (i : Fin P.m), MvPolynomial.degreeOf i g ≤ dPcp) (v : Fin 5) (τ τ' : LIDT.CL.Ty) (w : Pcp.Coord P → F) : LIDT.CL.accepts hm (q1 S v τ ((Pcp.pres P S S' (v.castSucc, τ)).eval w)) (q1 S v τ' ((Pcp.pres P S S' (v.castSucc, τ')).eval w)) (LIDT.CL.honest hm (fun (x : Fin 1) => g) (q1 S v τ ((Pcp.pres P S S' (v.castSucc, τ)).eval w))) (LIDT.CL.honest hm (fun (x : Fin 1) => g) (q1 S v τ' ((Pcp.pres P S S' (v.castSucc, τ')).eval w))) = true

The low-degree test of copy v ≤ 5 on honest answers to two questions of one PCP vector.

theorem MIPRE.AnswerReduction.accepts_q6_honest {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') {c : Fin (P.m' + 6) → MvPolynomial (Fin P.m') F} (hc : ∀ (j : Fin (P.m' + 6)) (i : Fin P.m'), MvPolynomial.degreeOf i (c j) ≤ dPcp) {i i' : Fin 6} (h : ↑i = 5) (h' : ↑i' = 5) (τ τ' : LIDT.CL.Ty) (w : Pcp.Coord P → F) : LIDT.CL.accepts hm' (q6 S' τ ((Pcp.pres P S S' (i, τ)).eval w)) (q6 S' τ' ((Pcp.pres P S S' (i', τ')).eval w)) (LIDT.CL.honest hm' c (q6 S' τ ((Pcp.pres P S S' (i, τ)).eval w))) (LIDT.CL.honest hm' c (q6 S' τ' ((Pcp.pres P S S' (i', τ')).eval w))) = true

The low-degree test of copy 6 on honest answers to two questions of one PCP vector.

The five steps

structure MIPRE.AnswerReduction.Consistent {P : SAT.PcpParams} {F : Type u_1} [Field F] (rp rq : Role) (Hp Hq : HPolys P F) : Prop

The consistency of two players' data that the five steps read: equal roles have equal data, and an isolated player v's g_v is an oracle's.

• same : rp = rq → Hp = Hq
• orc (v : Fin 5) : rp = Role.oracle → roleIdx rq = some v → Hq.g v = Hp.g v

theorem MIPRE.AnswerReduction.roleIdx_injective {r r' : Role} {v : Fin 5} (h : roleIdx r = some v) (h' : roleIdx r' = some v) : r = r'

theorem MIPRE.AnswerReduction.val6_eq_val1 {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') {chk : (Fin P.m' → F) → (Fin (P.m' + 6) → F) → Bool} (Hp Hq : HPolys P F) (ho : Hp.Oracle chk) (v : Fin 5) (hg : Hq.g v = Hp.g v) {i : Fin 6} (h5 : ↑i = 5) (w : Pcp.Coord P → F) : val6 (HPolys.idx6 v) (honestAns S S' Hp (i, LIDT.CL.Ty.point) ((Pcp.pres P S S' (i, LIDT.CL.Ty.point)).eval w)) = val1 (honestAns S S' Hq (v.castSucc, LIDT.CL.Ty.point) ((Pcp.pres P S S' (v.castSucc, LIDT.CL.Ty.point)).eval w))

Step 2's comparison, or step 4's: an oracle's Point_6 value on block v against a Point_v value of data with the same g_v.

theorem MIPRE.AnswerReduction.side_honest {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) (tp tq : Role × Pcp.PcpTy) (xp xq : X) (w : Pcp.Coord P → F) (Hp Hq : HPolys P F) (hp : Hp.LowDeg) (hpo : tp.1 = Role.oracle → Hp.Oracle (check xp)) (hc : Consistent tp.1 tq.1 Hp Hq) : side S S' check (tp, xp, (Pcp.pres P S S' tp.2).eval w) (tq, xq, (Pcp.pres P S S' tq.2).eval w) (honestAns S S' Hp tp.2 ((Pcp.pres P S S' tp.2).eval w)) (honestAns S S' Hq tq.2 ((Pcp.pres P S S' tq.2).eval w)) = true

theorem MIPRE.AnswerReduction.accepts_honestAns {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) (tp tq : Role × Pcp.PcpTy) (xp xq : X) (w : Pcp.Coord P → F) (Hp Hq : HPolys P F) (hp : Hp.LowDeg) (hq : Hq.LowDeg) (hpo : tp.1 = Role.oracle → Hp.Oracle (check xp)) (hqo : tq.1 = Role.oracle → Hq.Oracle (check xq)) (hc : Consistent tp.1 tq.1 Hp Hq) (hc' : Consistent tq.1 tp.1 Hq Hp) : accepts S S' check (tp, xp, (Pcp.pres P S S' tp.2).eval w) (tq, xq, (Pcp.pres P S S' tq.2).eval w) (honestAns S S' Hp tp.2 ((Pcp.pres P S S' tp.2).eval w)) (honestAns S S' Hq tq.2 ((Pcp.pres P S S' tq.2).eval w)) = true

The answer-reduced predicate accepts honest answers to two questions read off one PCP vector w, from data of low degree that is consistent both ways, an oracle's passing its PCP check.