Completeness of answer reduction

Piece AR-4 of planning/answer-reduction.md, concluded (lem:ar-completeness, with lem:oracle-timeout-pcc in the ambient form the contract uses): for λ, μ ≥ 1, an input within its budget whose decider has size at most σ and which has a value-1 PCC strategy at the answer bound 2^{(λn + 1)^μ} gives an answer-reduced verifier with a value-1 PCC strategy at the answer cut (arVerifier_hasPerfectPCC), hence at the output bound (arVerifier_completeness).

The typed game's completeness (exists_typedGame_perfectPCC) asks for good PCP proofs of the pairs the input decider accepts. They are the PCP decider's (SAT.PcpDecider.completeness), under three facts:

• the decider accepts within the PCP's time bound T = 2^{(Q + 5)(μ + 1)} (acceptsWithin_of_accepts): an input within its budget runs within 2^Q (|d| + 1)^μ on every input, and on answers of length at most 2^Q that is at most T — the timeout the paper's lem:oracle-timeout-pcc handles by truncation is here a consequence of determinism, since the answer alphabet is already cut at 2^Q;
• the PCP's input is valid (valid_of): Q ≤ T, 2 log n ≤ T, |𝒟| ≤ σ and questions of length at most Q. The second is where λ, μ ≥ 1 is needed (Q ≥ n + 1);
• the PCP's field is the Shoup field the answer-reduced sampler downsizes along (ShoupField, a hypothesis on the PCP decider like ParamsBound): the game check hands the PCP verifier the view in the Shoup representation, and the PCP's completeness is stated in its own.

Then the detyping compiler's completeness (CL.Detyping.DeciderProgram.verifier_hasPerfectPCC) carries the typed strategy to the output verifier, its typed predicate being the typed game's at the answer cut (typedDecider's accepts_iff).

def MIPRE.AnswerReduction.ShoupField (PD : SAT.PcpDecider) : Prop

The PCP's field is the Shoup field, for every admissible extension degree.

Equations

• MIPRE.AnswerReduction.ShoupField PD = ∀ (k : ℕ) (h : Odd k), PD.fld k h = MIPRE.SAT.shoupAdmissibleField k h

The view of a good proof

theorem MIPRE.AnswerReduction.vecBits_ofProof {P : SAT.PcpParams} (hk : 1 ≤ P.k) (pf : SAT.PcpProof P (Fq P hk)) (z : Fin P.m' → Fq P hk) : ((fld P hk).vecBits fun (j : Fin (P.m' + 6)) => (MvPolynomial.eval z) ((ofProof hk pf).c j)) = (fld P hk).vecBits (pf.ev z).1 ++ (fld P hk).vecBits (pf.ev z).2

The PCP's hypotheses

theorem MIPRE.AnswerReduction.pow_le_tPcp (lam mu n : ℕ) : 2 ^ arQ lam mu n * (2 ^ (arQ lam mu n + 5)) ^ mu ≤ tPcp lam mu n

theorem MIPRE.AnswerReduction.acceptsWithin_of_accepts {ℓ : ℕ} (V : Verifier (ℓ + 1)) (lam mu n : ℕ) (hV : V.Within n (inBudget lam mu n)) {x y a b : Cost.BitStr} (hx : List.length x ≤ arQ lam mu n) (hy : List.length y ≤ arQ lam mu n) (ha : List.length a ≤ inAns lam mu n) (hb : List.length b ≤ inAns lam mu n) (h : V.decider.Accepts n x y a b) : V.decider.AcceptsWithin n x y a b (tPcp lam mu n)

The input decider accepts within the PCP's time bound: an accepted input of questions at most Q long and answers at most 2^Q long is accepted within T = 2^{(Q + 5)(μ + 1)}, by determinism, when the decider is within its budget.

theorem MIPRE.AnswerReduction.valid_of {ℓ : ℕ} (V : Verifier (ℓ + 1)) (lam mu sigma n : ℕ) (hlam : 1 ≤ lam) (hmu : 1 ≤ mu) (hV : V.Within n (inBudget lam mu n)) (hsz : V.decider.size ≤ sigma) (x : Fin (V.sampler.dim n) → CL.𝔽₂) : SAT.Valid V.decider.prog n (tPcp lam mu n) (arQ lam mu n) sigma (CL.toBits ((V.sampler.cl n Player.alice).eval x)) (CL.toBits ((V.sampler.cl n Player.bob).eval x))

The PCP's input is valid, for λ, μ ≥ 1.

The answer-reduced verifier

theorem MIPRE.AnswerReduction.exists_proofGood (PD : SAT.PcpDecider) (lam mu sigma : ℕ) {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (hF : ShoupField PD) (hlam : 1 ≤ lam) (hmu : 1 ≤ mu) (hV : V.Within n (inBudget lam mu n)) (hsz : V.decider.size ≤ sigma) (x : Fin (V.sampler.dim n) → CL.𝔽₂) (a b : Verifier.Answers (inAns lam mu n)) (h : (V.seeded n (inAns lam mu n)).D ((V.sampler.cl n Player.alice).eval x) ((V.sampler.cl n Player.bob).eval x) a b = true) : ∃ (pf : SAT.PcpProof ((family PD lam mu sigma).par n) (Fq ((family PD lam mu sigma).par n) ⋯)), ProofGood ⋯ (chk PD V lam mu sigma n) x (↑a) (↑b) pf

Good PCP proofs exist for the pairs the input decider accepts, by the PCP's completeness.

noncomputable def MIPRE.AnswerReduction.zeroProof (P : SAT.PcpParams) (hk : 1 ≤ P.k) : SAT.PcpProof P (Fq P hk)

The zero PCP proof.

Equations

• MIPRE.AnswerReduction.zeroProof P hk = { g := 0, c := 0, degreeOf_g := ⋯, degreeOf_c := ⋯ }

noncomputable def MIPRE.AnswerReduction.arPf (PD : SAT.PcpDecider) (lam mu sigma : ℕ) {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (x : Fin (V.sampler.dim n) → CL.𝔽₂) (a b : Cost.BitStr) : SAT.PcpProof ((family PD lam mu sigma).par n) (Fq ((family PD lam mu sigma).par n) ⋯)

The oracles' PCP proofs: a good proof where there is one.

Equations

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

theorem MIPRE.AnswerReduction.typedPredicate_eq (PD : SAT.PcpDecider) (lam mu sigma : ℕ) {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (p q : CL.Detyping.Question ArTy (Fin (dim V n ((family PD lam mu sigma).par n)))) (a b : Verifier.Answers (cutVal ((family PD lam mu sigma).par n))) : CL.Detyping.DeciderProgram.typedPredicate (typedSampler V.sampler PD lam mu sigma) (typedDecider PD V lam mu sigma) (arCut PD lam mu sigma) n p q a b = typedPred V n ((family PD lam mu sigma).par n) ⋯ ((family PD lam mu sigma).sel n) ((family PD lam mu sigma).sel' n) (chk PD V lam mu sigma n) (cutVal ((family PD lam mu sigma).par n)) p q a b

The typed decider's predicate, at the answer cut, is the typed game's.

theorem MIPRE.AnswerReduction.arVerifier_hasPerfectPCC (PD : SAT.PcpDecider) (lam mu sigma : ℕ) {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (hF : ShoupField PD) (hlam : 1 ≤ lam) (hmu : 1 ≤ mu) (hV : V.Within n (inBudget lam mu n)) (hsz : V.decider.size ≤ sigma) (h : V.HasPerfectPCC n (inAns lam mu n)) : (arVerifier PD lam mu sigma V).HasPerfectPCC n (cutVal (arPar PD lam mu sigma n))

Completeness of answer reduction, at the answer cut.

theorem MIPRE.AnswerReduction.arVerifier_completeness (PD : SAT.PcpDecider) {ℓ : ℕ} (R : Polynomial ℕ) (hF : ShoupField PD) (hR : ParamsBound PD R) : ∃ (bound : Polynomial ℕ) (deg : ℕ), (∀ (V : Verifier (ℓ + 1)) (lam mu sigma n : ℕ), V.Within n (inBudget lam mu n) → V.size ≤ sigma → (arVerifier PD lam mu sigma V).Within n (Budget.uniform (outBound bound lam mu sigma n) (outDegree deg mu))) ∧ ∀ (V : Verifier (ℓ + 1)) (lam mu sigma n : ℕ), 1 ≤ lam → 1 ≤ mu → V.Within n (inBudget lam mu n) → V.decider.size ≤ sigma → V.HasPerfectPCC n (inAns lam mu n) → (arVerifier PD lam mu sigma V).HasPerfectPCC n (outBound bound lam mu sigma n)

Completeness of answer reduction (lem:ar-completeness, the completeness clause of the AnswerReduction contract, at the output bound of arVerifier_bounds).