The linear-constraints processor of the answer-reduced verifier

Slice P4h of planning/aldous-lyons-track.md: the linear-constraints processor of the output tailored verifier of the answer reduction, as a staged program. On (n, x, y, a^R, b^R), with the input verifier's programs and (λ, μ, σ) hardcoded, it runs

1. the routine's parameter program on ((λ, μ, σ), n) (ArRoutine.parCore);
2. to 5. the input sampler on the marginal queries of Alice and Bob at the seeds of x and of y, through the universal machine;
3. and 7. the routine's circuit function on the input's programs, the parameters and the two questions at each seed, on its encoding;
4. and 9. the proof check of each question, on its encoding, the circuit's gates spliced in;

and then the last stage lpFinal on what it read. No stage decodes a program: the circuit function and the proof check run on encodings assembled from the context.

• lpRuns: the run, and lpD_lpIs: the processor outputs the presented answer-reduced game's constraints at every pair of detyped questions.

Reading the context

noncomputable def MIPRE.Tailored.AnsRed.Typed.hdL (k : ℕ) : Cost.PolyTimeFun Cost.Data Cost.Data

The hardcoded data, (V.progs, λ, μ, σ), after k stages.

Equations

• MIPRE.Tailored.AnsRed.Typed.hdL k = MIPRE.Cost.PolyTimeFun.treeHead.comp (MIPRE.AnswerReduction.tails k)

noncomputable def MIPRE.Tailored.AnsRed.Typed.inL (k : ℕ) : Cost.PolyTimeFun Cost.Data Cost.Data

The input tuple (n, x, y, a^R, b^R), after k stages.

Equations

• MIPRE.Tailored.AnsRed.Typed.inL k = MIPRE.Cost.PolyTimeFun.treeTail.comp (MIPRE.AnswerReduction.tails k)

noncomputable def MIPRE.Tailored.AnsRed.Typed.nL (k : ℕ) : Cost.PolyTimeFun Cost.Data Cost.Data

The index.

Equations

• MIPRE.Tailored.AnsRed.Typed.nL k = MIPRE.Cost.PolyTimeFun.treeHead.comp (MIPRE.Tailored.AnsRed.Typed.inL k)

noncomputable def MIPRE.Tailored.AnsRed.Typed.xL (k : ℕ) : Cost.PolyTimeFun Cost.Data Cost.Data

The first question.

Equations

• MIPRE.Tailored.AnsRed.Typed.xL k = MIPRE.Cost.PolyTimeFun.treeHead.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp (MIPRE.Tailored.AnsRed.Typed.inL k))

noncomputable def MIPRE.Tailored.AnsRed.Typed.yL (k : ℕ) : Cost.PolyTimeFun Cost.Data Cost.Data

The second question.

Equations

• MIPRE.Tailored.AnsRed.Typed.yL k = MIPRE.Cost.PolyTimeFun.treeHead.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp (MIPRE.Tailored.AnsRed.Typed.inL k)))

noncomputable def MIPRE.Tailored.AnsRed.Typed.aL (k : ℕ) : Cost.PolyTimeFun Cost.Data Cost.Data

The first readable answer.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.bL (k : ℕ) : Cost.PolyTimeFun Cost.Data Cost.Data

The second readable answer.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.progsL (k : ℕ) : Cost.PolyTimeFun Cost.Data Cost.Data

The input verifier's programs.

Equations

• MIPRE.Tailored.AnsRed.Typed.progsL k = MIPRE.Cost.PolyTimeFun.treeHead.comp (MIPRE.Tailored.AnsRed.Typed.hdL k)

noncomputable def MIPRE.Tailored.AnsRed.Typed.lmsL (k : ℕ) : Cost.PolyTimeFun Cost.Data Cost.Data

(λ, μ, σ).

Equations

• MIPRE.Tailored.AnsRed.Typed.lmsL k = MIPRE.Cost.PolyTimeFun.treeTail.comp (MIPRE.Tailored.AnsRed.Typed.hdL k)

noncomputable def MIPRE.Tailored.AnsRed.Typed.parL (k : ℕ) : Cost.PolyTimeFun Cost.Data ArParams

The parameters, the first stage's result, after k ≥ 1 stages.

Equations

• MIPRE.Tailored.AnsRed.Typed.parL k = MIPRE.Tailored.AnsRed.Typed.readParams.comp (MIPRE.AnswerReduction.res (k - 1))

noncomputable def MIPRE.Tailored.AnsRed.Typed.preL (k : ℕ) : Cost.PolyTimeFun Cost.Data LpIn

The typed view of the context after k ≥ 1 stages: the parameters, the questions and the readable answers, without input sampler questions or programs.

Equations

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

The stages' arguments

noncomputable def MIPRE.Tailored.AnsRed.Typed.argParL : Cost.PolyTimeFun Cost.Data Cost.Data

Stage 1's argument: ((λ, μ, σ), n).

Equations

• MIPRE.Tailored.AnsRed.Typed.argParL = MIPRE.Cost.PolyTimeFun.treePair.ap₂ (MIPRE.Tailored.AnsRed.Typed.lmsL 0) (MIPRE.Tailored.AnsRed.Typed.nL 0)

noncomputable def MIPRE.Tailored.AnsRed.Typed.seedL (k : ℕ) (q : ℕ → Cost.PolyTimeFun Cost.Data Cost.Data) : Cost.PolyTimeFun Cost.Data Cost.BitStr

The seed bits of a question, after k ≥ 1 stages: its vector part before the low-degree bits.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.argMgL (ℓ k : ℕ) (q : ℕ → Cost.PolyTimeFun Cost.Data Cost.Data) (w : Player) : Cost.PolyTimeFun Cost.Data Cost.Data

A marginal call's argument, after k stages: the input sampler's program and the query (n, marginal w (ℓ + 1) z) at the seed z of a question.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.argCircL (k rA rB : ℕ) : Cost.PolyTimeFun Cost.Data Cost.Data

A circuit stage's argument, after k stages: the encoding of the circuit function's input, from the input's programs, (λ, μ, σ), the index, the parameters and the input sampler's questions rA and rB stages back, read as bit strings — so that the argument is an encoding on every input, whatever the input sampler output.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.argPrfL (k rC : ℕ) (o : Cost.PolyTimeFun LpIn Cost.Unary) (q : Cost.PolyTimeFun LpIn Cost.BitStr) (a : ℕ → Cost.PolyTimeFun Cost.Data Cost.Data) : Cost.PolyTimeFun Cost.Data Cost.Data

A proof stage's argument, after k stages: the encoding of the proof check's input of a question at offset o, with readable answer a read as a bit string, the gates of the circuit rC stages back.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.readBL : Cost.PolyTimeFun Cost.Data (List Cost.BitStr)

A list of bit strings from its encoding.

Equations

• MIPRE.Tailored.AnsRed.Typed.readBL = MIPRE.CL.Detyping.Program.readBits.map.comp MIPRE.AnswerReduction.rawListP

noncomputable def MIPRE.Tailored.AnsRed.Typed.finRead : Cost.PolyTimeFun Cost.Data LpFin

The last stage's reader, after the nine stages.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArRoutine.lpCore (R : ArRoutine) (ℓ : ℕ) : Cost.Prog

The processor's core, on ((V.progs, λ, μ, σ), (n, x, y, a^R, b^R)), for an input sampler of level ℓ + 1.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.lpCore_closed (R : ArRoutine) (ℓ : ℕ) : Cost.Prog.WellScoped 1 (R.lpCore ℓ)

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArRoutine.lpD (R : ArRoutine) (ℓ : ℕ) (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam mu sigma : ℕ) : Decider

The linear-constraints processor, for the input programs V and (λ, μ, σ).

Equations

• R.lpD ℓ V lam mu sigma = { prog := MIPRE.Cost.hardcode (R.lpCore ℓ) (MIPRE.Cost.encode (V, lam, mu, sigma)), closed := ⋯ }

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArRoutine.lpPF (R : ArRoutine) (ℓ : ℕ) : Cost.PolyTimeFun ((Cost.Prog × Cost.Prog × Cost.Prog) × ℕ × ℕ × ℕ) Cost.Prog

Its program, from the input programs and (λ, μ, σ), in polynomial time.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.lpPF_eq (R : ArRoutine) (ℓ : ℕ) (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam mu sigma : ℕ) : (R.lpPF ℓ).toFun (V, lam, mu, sigma) = (R.lpD ℓ V lam mu sigma).prog

The run

theorem MIPRE.Tailored.AnsRed.Typed.readBL_encode (l : List Cost.BitStr) : readBL.toFun (Cost.encode l) = l

theorem MIPRE.Tailored.AnsRed.Typed.leftBP_rolePart {t j rV : ℕ} (y : Fin (rV + D j * t) → CL.𝔽₂) : AnswerReduction.leftBP.toFun (CL.toBits y, Cost.unary (D j * t)) = CL.toBits (rolePart t j rV y)

The seed bits of a question's bits are its role part's.

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.ArRoutine.lpX0 (R : ArRoutine) (lam mu sigma n : ℕ) {ℓ : ℕ} (V : TailoredVerifier (ℓ + 1)) (qx qy : CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin (V.sampler.dim n + D ((R.fam lam mu sigma).j n) * (R.fam lam mu sigma).t n)) → CL.𝔽₂) (aR bR : Cost.BitStr) : Cost.Data

The core's input.

Equations

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

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Typed.ArRoutine.seedOf (R : ArRoutine) (lam mu sigma n : ℕ) {ℓ : ℕ} (V : TailoredVerifier (ℓ + 1)) (q : CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin (V.sampler.dim n + D ((R.fam lam mu sigma).j n) * (R.fam lam mu sigma).t n)) → CL.𝔽₂) : V.Questions n

A question's seed, as a question of the input verifier.

Equations

• R.seedOf lam mu sigma n V q = MIPRE.Tailored.AnsRed.Typed.rolePart ((R.fam lam mu sigma).t n) ((R.fam lam mu sigma).j n) (V.sampler.dim n) (MIPRE.CL.pull Function.Embedding.inr q)

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Typed.ArRoutine.margD (R : ArRoutine) (lam mu sigma n : ℕ) {ℓ : ℕ} (V : TailoredVerifier (ℓ + 1)) (w : Player) (q : CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin (V.sampler.dim n + D ((R.fam lam mu sigma).j n) * (R.fam lam mu sigma).t n)) → CL.𝔽₂) : Cost.Data

The input sampler's question of player w at a question's seed, as data.

Equations

• R.margD lam mu sigma n V w q = MIPRE.Cost.encode (MIPRE.CL.toBits ((V.sampler.cl n w).eval (R.seedOf lam mu sigma n V q)))

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.seedL_eq (R : ArRoutine) (lam mu sigma n : ℕ) {ℓ : ℕ} (V : TailoredVerifier (ℓ + 1)) (k : ℕ) (X : Cost.Data) (q : ℕ → Cost.PolyTimeFun Cost.Data Cost.Data) (z : CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin (V.sampler.dim n + D ((R.fam lam mu sigma).j n) * (R.fam lam mu sigma).t n)) → CL.𝔽₂) (hp : (AnswerReduction.res (k - 1)).toFun X = Cost.encode (R.params lam mu sigma n)) (hq : (q k).toFun X = Cost.encode (CL.toBits ((CL.Detyping.DeciderProgram.vectorEquiv (V.sampler.dim n + D ((R.fam lam mu sigma).j n) * (R.fam lam mu sigma).t n)) z))) : (seedL k q).toFun X = CL.toBits (R.seedOf lam mu sigma n V z)

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.argMgL_eq (R : ArRoutine) (lam mu sigma n : ℕ) {ℓ : ℕ} (V : TailoredVerifier (ℓ + 1)) (k : ℕ) (X : Cost.Data) (q : ℕ → Cost.PolyTimeFun Cost.Data Cost.Data) (w : Player) (z : CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin (V.sampler.dim n + D ((R.fam lam mu sigma).j n) * (R.fam lam mu sigma).t n)) → CL.𝔽₂) (hp : (AnswerReduction.res (k - 1)).toFun X = Cost.encode (R.params lam mu sigma n)) (hq : (q k).toFun X = Cost.encode (CL.toBits ((CL.Detyping.DeciderProgram.vectorEquiv (V.sampler.dim n + D ((R.fam lam mu sigma).j n) * (R.fam lam mu sigma).t n)) z))) (hs : Cost.PolyTimeFun.treeHead.toFun ((progsL k).toFun X) = Cost.encode V.sampler.prog) (hn : (nL k).toFun X = Cost.encode n) : (argMgL ℓ k q w).toFun X = (Cost.encode V.sampler.prog).cons (Cost.encode (n, CL.Sampler.Query.marginal w (ℓ + 1) (CL.toBits (R.seedOf lam mu sigma n V z))))

A marginal call's argument is the query at the question's seed.

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.marg_runs (R : ArRoutine) (lam mu sigma n : ℕ) {ℓ : ℕ} (V : TailoredVerifier (ℓ + 1)) (w : Player) (z : CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin (V.sampler.dim n + D ((R.fam lam mu sigma).j n) * (R.fam lam mu sigma).t n)) → CL.𝔽₂) : ∃ (t : ℕ), Cost.selfUniversal.univ.Runs ((Cost.encode V.sampler.prog).cons (Cost.encode (n, CL.Sampler.Query.marginal w (ℓ + 1) (CL.toBits (R.seedOf lam mu sigma n V z))))) (R.margD lam mu sigma n V w z) t

The input sampler's run on a marginal query at a question's seed.

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.lpCore_runs (R : ArRoutine) (lam mu sigma n : ℕ) {ℓ : ℕ} (V : TailoredVerifier (ℓ + 1)) (qx qy : CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin (V.sampler.dim n + D ((R.fam lam mu sigma).j n) * (R.fam lam mu sigma).t n)) → CL.𝔽₂) (aR bR : Cost.BitStr) {ℓ' : ℕ} (P : Bool → Role × LIDT.CL.Ty → CL.CLFun (ZMod 2) (Fin (V.sampler.dim n + D ((R.fam lam mu sigma).j n) * (R.fam lam mu sigma).t n)) ℓ') (B : ℕ) : ∃ (t : ℕ), (R.lpCore ℓ).Runs (R.lpX0 lam mu sigma n V qx qy aR bR) (Cost.encode ((arPresented (R.d lam mu sigma n) ⋯ ((R.fam lam mu sigma).sel n) (R.L lam mu sigma n) ⋯ V n (R.circ lam mu sigma n V) ⋯ P B).cons qx qy aR bR)) t

The core's run: it outputs the presented answer-reduced game's constraints.

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.lpD_lpIs (R : ArRoutine) (lam mu sigma n : ℕ) {ℓ : ℕ} (V : TailoredVerifier (ℓ + 1)) (qx qy : CL.Detyping.Coord (Role × LIDT.CL.Ty) (Fin (V.sampler.dim n + D ((R.fam lam mu sigma).j n) * (R.fam lam mu sigma).t n)) → CL.𝔽₂) (aR bR : Cost.BitStr) {ℓ' : ℕ} (P : Bool → Role × LIDT.CL.Ty → CL.CLFun (ZMod 2) (Fin (V.sampler.dim n + D ((R.fam lam mu sigma).j n) * (R.fam lam mu sigma).t n)) ℓ') (B : ℕ) : LpIs (R.lpD ℓ V.progs lam mu sigma) n (CL.toBits ((CL.Detyping.DeciderProgram.vectorEquiv (V.sampler.dim n + D ((R.fam lam mu sigma).j n) * (R.fam lam mu sigma).t n)) qx)) (CL.toBits ((CL.Detyping.DeciderProgram.vectorEquiv (V.sampler.dim n + D ((R.fam lam mu sigma).j n) * (R.fam lam mu sigma).t n)) qy)) aR bR ((arPresented (R.d lam mu sigma n) ⋯ ((R.fam lam mu sigma).sel n) (R.L lam mu sigma n) ⋯ V n (R.circ lam mu sigma n V) ⋯ P B).cons qx qy aR bR)

The processor outputs the presented answer-reduced game's constraints at every pair of detyped questions.

The output verifier

noncomputable def MIPRE.Tailored.AnsRed.Typed.ArRoutine.output (R : ArRoutine) {ℓ : ℕ} (V : TailoredVerifier (ℓ + 1)) (lam mu sigma : ℕ) : TailoredVerifier (max (ℓ + 1) 3 + 2)

The output tailored verifier of the answer reduction: the answer-reduced sampler, the answer-length calculator and the linear-constraints processor.

Equations

• R.output V lam mu sigma = { sampler := R.toLd.arSampler lam mu sigma V.sampler, len := R.lenD lam mu sigma, lp := R.lpD ℓ V.progs lam mu sigma }

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.arMeets_output (R : ArRoutine) {ℓ : ℕ} (V : TailoredVerifier (ℓ + 1)) (lam mu sigma n B : ℕ) : ArMeets (R.d lam mu sigma n) ⋯ ((R.fam lam mu sigma).sel n) (R.L lam mu sigma n) ⋯ V n (R.circ lam mu sigma n V) ⋯ (fun (x : Bool) (u : Role × LIDT.CL.Ty) => arCl ((R.fam lam mu sigma).sel n) n V u) B (R.output V lam mu sigma) (R.toLd.qe lam mu sigma V.sampler n)

The output verifier meets the presented answer-reduced game at every index, along the numbering of the detyped questions.

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.hasPerfectZPC_output (R : ArRoutine) {ℓ : ℕ} (V : TailoredVerifier (ℓ + 1)) (lam mu sigma n B : ℕ) {prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)} {Tt : ℕ} (H : HonestHyp (R.L lam mu sigma n) V n prm (R.circ lam mu sigma n V) Tt) (hd : 17 ≤ R.d lam mu sigma n) (hB : ∀ (u : Role × LIDT.CL.Ty), len ((R.fam lam mu sigma).t n) ((R.fam lam mu sigma).j n) (R.d lam mu sigma n) (R.L lam mu sigma n) u ≤ B) (hV : V.HasPerfectZPC n) : (R.output V lam mu sigma).HasPerfectZPC n

Completeness of the output verifier, under the honest PCPs' hypotheses, for a degree d ≥ 17 and an answer bound at least the types' lengths.

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.valStar_sound_output (R : ArRoutine) {ℓ : ℕ} (V : TailoredVerifier (ℓ + 1)) (lam mu sigma n B : ℕ) {prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)} {Tt : ℕ} (H : HonestHyp (R.L lam mu sigma n) V n prm (R.circ lam mu sigma n V) Tt) (hd : 1 ≤ R.d lam mu sigma n) (hB : ∀ (u : Role × LIDT.CL.Ty), len ((R.fam lam mu sigma).t n) ((R.fam lam mu sigma).j n) (R.d lam mu sigma n) (R.L lam mu sigma n) u ≤ B) (hq : 2 * ((2 ^ (R.fam lam mu sigma).j n + 1) * R.d lam mu sigma n) ≤ Fintype.card (Fq ((R.fam lam mu sigma).t n) ⋯)) (hτ : 2 * ((R.L lam mu sigma n).m * chkDeg 5 (R.d lam mu sigma n)) ≤ Fintype.card (Fq ((R.fam lam mu sigma).t n) ⋯)) {ε : ℝ} (hε : 0 < ε) (hv : 1 - ε < (R.output V lam mu sigma).valStar n) : 1 - 24 * √(errAR ((R.fam lam mu sigma).t n) ⋯ ((R.fam lam mu sigma).j n) (R.d lam mu sigma n) (R.L lam mu sigma n) (16 ^ 9 * ε)) ≤ V.valStar n

Soundness of the output verifier: if its n-th game has val* > 1 - ε, then val*(𝒱_n) ≥ 1 - 24 √(errAR (16⁹ ε)), once the field is large enough.