Completeness of the typed answer-reduced game

Piece AR-4 of planning/answer-reduction.md: a value-1 PCC strategy of the input verifier gives one of the (doubled) typed answer-reduced game (exists_typedGame_perfectPCC), for any PCP proofs of the accepted answer pairs — the paper's completeness argument for thm:ar (ld_compiler.tex), with the PCP's completeness left as a hypothesis (ProofGood), discharged in MIPRE/Background/AnswerReduction/Complete.

The strategy is the oracularized game's honest strategy (SeededGame.oracleStrategy, the oracularization's completeness), read through the question map that keeps a question's role and its oracle half (SyncStrategy.pushQ), and answered honestly (honestAns) from data computed from the role, the oracle half and the outcome (hdata):

• an oracle answering the pair (a, b) at seed x holds the PCP proof pfOf x a b (ofProof);
• an isolated player answering a holds the low-degree encoding of a at its own copy (ofAnswer), and zero elsewhere.

Two questions of positive weight are read off one seed; their oracle halves are then an oracularized question pair of positive weight, and their PCP halves questions of one PCP vector. There the oracularized predicate's checks are exactly the consistency accepts_honestAns needs.

The oracularized question distribution

theorem MIPRE.AnswerReduction.SeededGame.oDist_oquestion_pos {W : Type u_1} {A : Type u_2} [Fintype W] [DecidableEq W] (G : SeededGame W A) (r₁ r₂ : Role) (z : W) : 0 < G.oDist (G.oquestion r₁ z) (G.oquestion r₂ z)

theorem MIPRE.AnswerReduction.SampledGame.exists_of_dist_pos {Sd : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype Sd] [Fintype X] [Fintype Y] {qA : Sd → X} {qB : Sd → Y} {x : X} {y : Y} (h : 0 < SampledGame.dist qA qB x y) : ∃ (s : Sd), qA s = x ∧ qB s = y

The players' data

def MIPRE.AnswerReduction.blockEmb {P : SAT.PcpParams} (i : Fin 5) : Fin P.m → Fin P.m'

The embedding of the i-th block of m coordinates into the m' of the sixth copy.

Equations

• MIPRE.AnswerReduction.blockEmb i j = ⟨↑i * P.m + ↑j, ⋯⟩

theorem MIPRE.AnswerReduction.blockEmb_injective {P : SAT.PcpParams} (i : Fin 5) : Function.Injective (blockEmb i)

noncomputable def MIPRE.AnswerReduction.ofProof {P : SAT.PcpParams} (hk : 1 ≤ P.k) (pf : SAT.PcpProof P (Fq P hk)) : HPolys P (Fq P hk)

An oracle's data, from a PCP proof: the answer polynomials, and for the sixth copy the answer polynomials read on their blocks followed by the constraint polynomials.

Equations

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

noncomputable def MIPRE.AnswerReduction.ofAnswer {P : SAT.PcpParams} (hk : 1 ≤ P.k) (v : Fin 5) (a : Cost.BitStr) : HPolys P (Fq P hk)

An isolated player's data: the low-degree encoding of its answer at its own copy v.

Equations

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

def MIPRE.AnswerReduction.ProofGood {P : SAT.PcpParams} (hk : 1 ≤ P.k) {X : Type u_1} (check : X → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool) (x : X) (a b : Cost.BitStr) (pf : SAT.PcpProof P (Fq P hk)) : Prop

A PCP proof is good for the pair (a, b) at seed x: its first two answer polynomials encode a and b, and every point's evaluations pass the check.

Equations

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

theorem MIPRE.AnswerReduction.degreeOf_rename_le {P : SAT.PcpParams} (hk : 1 ≤ P.k) {m m' d : ℕ} {f : Fin m → Fin m'} (hf : Function.Injective f) {p : MvPolynomial (Fin m) (Fq P hk)} (hp : ∀ (i : Fin m), MvPolynomial.degreeOf i p ≤ d) (i' : Fin m') : MvPolynomial.degreeOf i' ((MvPolynomial.rename f) p) ≤ d

theorem MIPRE.AnswerReduction.lowDeg_ofProof {P : SAT.PcpParams} (hk : 1 ≤ P.k) (pf : SAT.PcpProof P (Fq P hk)) : (ofProof hk pf).LowDeg

theorem MIPRE.AnswerReduction.lowDeg_ofAnswer {P : SAT.PcpParams} (hk : 1 ≤ P.k) (v : Fin 5) (a : Cost.BitStr) : (ofAnswer hk v a).LowDeg

theorem MIPRE.AnswerReduction.oracle_ofProof {P : SAT.PcpParams} (hk : 1 ≤ P.k) {X : Type u_1} {check : X → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool} {x : X} {a b : Cost.BitStr} {pf : SAT.PcpProof P (Fq P hk)} (h : ProofGood hk check x a b pf) : (ofProof hk pf).Oracle (check x)

The answer length

theorem MIPRE.AnswerReduction.cnt_le {P : SAT.PcpParams} (t : Pcp.PcpTy) : cnt P t ≤ (P.m' + 6) * (P.m' * 7 + 1)

theorem MIPRE.AnswerReduction.length_enc_honestAns_le {P : SAT.PcpParams} (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (H : HPolys P (Fq P hk)) (t : Pcp.PcpTy) (y : Pcp.Coord P → Fq P hk) : List.length (enc (fld P hk) (honestAns S S' H t y)) ≤ 32 * ((P.k + 1) * (P.m' + 7) * (P.m' + 7))

Honest answers fit the answer cut 32 (k + 1)(m' + 7)^2.

The players' data, from the oracularized strategy's outcomes

noncomputable def MIPRE.AnswerReduction.hdata {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) {B : ℕ} (pfOf : (Fin (V.sampler.dim n) → CL.𝔽₂) → Cost.BitStr → Cost.BitStr → SAT.PcpProof P (Fq P hk)) : Role → (Fin (V.sampler.dim n) → CL.𝔽₂) → OAns (Verifier.Answers B) → HPolys P (Fq P hk)

A player's data, from its role, the oracle half of its question and the oracularized strategy's outcome.

Equations

• MIPRE.AnswerReduction.hdata V n P hk pfOf MIPRE.Role.oracle x✝ (MIPRE.OAns.pair a b) = MIPRE.AnswerReduction.ofProof hk (pfOf x✝ ↑a ↑b)
• MIPRE.AnswerReduction.hdata V n P hk pfOf MIPRE.Role.alice x✝ (MIPRE.OAns.single a) = MIPRE.AnswerReduction.ofAnswer hk 0 ↑a
• MIPRE.AnswerReduction.hdata V n P hk pfOf MIPRE.Role.bob x✝ (MIPRE.OAns.single b) = MIPRE.AnswerReduction.ofAnswer hk 1 ↑b
• MIPRE.AnswerReduction.hdata V n P hk pfOf x✝² x✝¹ x✝ = { g := 0, c := 0 }

theorem MIPRE.AnswerReduction.lowDeg_hdata {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) {B : ℕ} (pfOf : (Fin (V.sampler.dim n) → CL.𝔽₂) → Cost.BitStr → Cost.BitStr → SAT.PcpProof P (Fq P hk)) (r : Role) (x : Fin (V.sampler.dim n) → CL.𝔽₂) (u : OAns (Verifier.Answers B)) : (hdata V n P hk pfOf r x u).LowDeg

theorem MIPRE.AnswerReduction.consistent_of_oaccepts {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) {B : ℕ} (pfOf : (Fin (V.sampler.dim n) → CL.𝔽₂) → Cost.BitStr → Cost.BitStr → SAT.PcpProof P (Fq P hk)) {check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool} (hpf : ∀ (x : Fin (V.sampler.dim n) → CL.𝔽₂) (a b : Verifier.Answers B), (V.seeded n B).D ((V.sampler.cl n Player.alice).eval x) ((V.sampler.cl n Player.bob).eval x) a b = true → ProofGood hk check x (↑a) (↑b) (pfOf x ↑a ↑b)) (r₁ r₂ : Role) (x₀ : Fin (V.sampler.dim n) → CL.𝔽₂) {u v : OAns (Verifier.Answers B)} (h : (V.seeded n B).oaccepts ((V.seeded n B).oquestion r₁ x₀) ((V.seeded n B).oquestion r₂ x₀) u v = true) : Consistent r₁ r₂ (hdata V n P hk pfOf r₁ ((V.seeded n B).oquestion r₁ x₀).2 u) (hdata V n P hk pfOf r₂ ((V.seeded n B).oquestion r₂ x₀).2 v)

The oracularized predicate's checks are the consistency of the data, on a question pair read off one seed, when every accepted pair's proof is good.

theorem MIPRE.AnswerReduction.oracle_hdata {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) {B : ℕ} (pfOf : (Fin (V.sampler.dim n) → CL.𝔽₂) → Cost.BitStr → Cost.BitStr → SAT.PcpProof P (Fq P hk)) {check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool} (hpf : ∀ (x : Fin (V.sampler.dim n) → CL.𝔽₂) (a b : Verifier.Answers B), (V.seeded n B).D ((V.sampler.cl n Player.alice).eval x) ((V.sampler.cl n Player.bob).eval x) a b = true → ProofGood hk check x (↑a) (↑b) (pfOf x ↑a ↑b)) (r₂ : Role) (x₀ : Fin (V.sampler.dim n) → CL.𝔽₂) {u v : OAns (Verifier.Answers B)} (h : (V.seeded n B).oaccepts ((V.seeded n B).oquestion Role.oracle x₀) ((V.seeded n B).oquestion r₂ x₀) u v = true) : (hdata V n P hk pfOf Role.oracle x₀ u).Oracle (check x₀)

An oracle's data passes its PCP check, at a question pair the oracularized predicate accepts.

theorem MIPRE.AnswerReduction.SeededGame.oaccepts_comm {W : Type u_1} {A : Type u_2} [Fintype W] [DecidableEq W] [Fintype A] [DecidableEq A] (G : SeededGame W A) (p q : Role × W) (u v : OAns A) : G.oaccepts p q u v = G.oaccepts q p v u

noncomputable def MIPRE.AnswerReduction.honestQ {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) {B : ℕ} (pfOf : (Fin (V.sampler.dim n) → CL.𝔽₂) → Cost.BitStr → Cost.BitStr → SAT.PcpProof P (Fq P hk)) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') (p : CL.Detyping.Question ArTy (Fin (dim V n P))) (u : OAns (Verifier.Answers B)) : Ans P (Fq P hk)

The honest answer to a typed question, from the oracularized strategy's outcome.

Equations

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

theorem MIPRE.AnswerReduction.exists_of_typedGame_mu_pos {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') {check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool} {Bout : ℕ} {p q : CL.Detyping.Question ArTy (Fin (dim V n P))} (h : 0 < (typedGame V n P hk S S' check Bout).μ p q) : ∃ (t₁ : Role × Pcp.PcpTy) (t₂ : Role × Pcp.PcpTy) (z : Fin (dim V n P) → CL.𝔽₂), p = (t₁, (cl V n P hk S S' t₁).eval z) ∧ q = (t₂, (cl V n P hk S S' t₂).eval z)

Two typed questions of positive weight are read off one seed.

theorem MIPRE.AnswerReduction.oraclePart_cl {ℓ : ℕ} {V : Verifier (ℓ + 1)} {n : ℕ} {P : SAT.PcpParams} {hk : 1 ≤ P.k} {B : ℕ} [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} {S : LIDT.CL.Sel (Fq P hk) P.m hm} {S' : LIDT.CL.Sel (Fq P hk) P.m' hm'} (t : ArTy) (z : Fin (dim V n P) → CL.𝔽₂) : oraclePart V n P ((cl V n P hk S S' t).eval z) = ((V.seeded n B).oquestion t.1 (oraclePart V n P z)).2

theorem MIPRE.AnswerReduction.exists_typedGame_perfectPCC {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (P : SAT.PcpParams) (hk : 1 ≤ P.k) {B : ℕ} (pfOf : (Fin (V.sampler.dim n) → CL.𝔽₂) → Cost.BitStr → Cost.BitStr → SAT.PcpProof P (Fq P hk)) [NeZero P.m] {hm : P.m ∣ Fintype.card (Fq P hk)} {hm' : P.m' ∣ Fintype.card (Fq P hk)} (S : LIDT.CL.Sel (Fq P hk) P.m hm) (S' : LIDT.CL.Sel (Fq P hk) P.m' hm') {check : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin P.m' → Fq P hk) → (Fin (P.m' + 6) → Fq P hk) → Bool} (Bout : ℕ) (hBout : 32 * ((P.k + 1) * (P.m' + 7) * (P.m' + 7)) ≤ Bout) (hV : V.HasPerfectPCC n B) (hpf : ∀ (x : Fin (V.sampler.dim n) → CL.𝔽₂) (a b : Verifier.Answers B), (V.seeded n B).D ((V.sampler.cl n Player.alice).eval x) ((V.sampler.cl n Player.bob).eval x) a b = true → ProofGood hk check x (↑a) (↑b) (pfOf x ↑a ↑b)) : ∃ (R : SyncStrategy (typedGame V n P hk S S' check Bout).doubled), R.IsPCC ∧ R.value = 1

Completeness of the typed answer-reduced game: a value-1 PCC strategy of 𝒱_n, and good PCP proofs of the pairs it accepts, give a value-1 PCC strategy of the doubled typed game at any answer cut above 32 (k + 1)(m' + 7)^2.