The class verifier of the polynomial-time halting reduction

The two programs of the PolyVerifier (def:mipstar) that puts an r.e. language L in the paper's class MIP*_{1,1/2}(2,1), for a polynomial-time reduction R of L to halting on the empty input (Cost.exists_polyTime_reduction): on input z they play the game of 𝒱^halt (R z) λ(z) at the fixed level C (Paper/Main.lean), with λ(z) = Λ₀ + 4|R z| the parameter of lem:lambda.

• The sampler sampProg, on (z, r), is the class sampler of Paper/ClassSampler.lean for the compressed samplers (GapCompression.samplerFamily) at the fixed level C: it computes M = R z, λ(z) and the compressed sampler's program S = ComputeSampler(λ(z)); asks S its dimension s = s(C) through the universal machine; takes the first s bits r' of the seed and asks S the two marginals at r'. Its output is the question pair of 𝒱^halt at the point r' (sampProg_runs), so that the uniform seed of length B ≥ s pushes forward to the compressed sampler's distribution.
• The decider decProg, on (z, x, y, a, b): computes M, λ(z) and the description of 𝒱^halt's decider (wrapCore around dec M λ(z), decBuild), rejects if a or b is longer than the cutoff 2 ^ (K + deg · |λ(z)|) (cutF, at least the compressor's answer bound poly(C, λ(z)) by exists_cut_ge), and otherwise runs the description on (C, x, y, a, b) through the universal machine. It accepts exactly when both answers are within the cutoff and 𝒱^halt's decider accepts (decProg_accepts).

The costs are bounded by explicit expressions in the total input length (sampB, decB), polynomially bounded (polyBounded_sampB, polyBounded_decB); Paper/ClassMain.lean chooses the verifier's polynomial above them and proves the game's value.

The sampler

@[reducible, inline]

noncomputable abbrev MIPRE.Halting.Sz (G : GapCompression) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z : Cost.BitStr) : CL.Sampler 7

The compressed sampler of the input z.

Equations

• MIPRE.Halting.Sz G Λ₀ R z = G.sampler (MIPRE.Halting.lamz Λ₀ R z)

@[reducible, inline]

noncomputable abbrev MIPRE.Halting.dimz (G : GapCompression) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z : Cost.BitStr) : ℕ

The dimension of its questions at the fixed level.

Equations

• MIPRE.Halting.dimz G Λ₀ R z = G.samplerFamily.dimz (MIPRE.Halting.C G) Λ₀ R z

@[reducible, inline]

noncomputable abbrev MIPRE.Halting.qOf (G : GapCompression) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (w : Player) (z r : Cost.BitStr) : Cost.BitStr

Player w's question on the seed r, on the input z: the marginal of the compressed sampler at the first dimz z bits of r.

Equations

• MIPRE.Halting.qOf G Λ₀ R w z r = G.samplerFamily.qOf (MIPRE.Halting.C G) Λ₀ R w z r

@[reducible, inline]

noncomputable abbrev MIPRE.Halting.sampProg (G : GapCompression) (U : Cost.UniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.Prog

The sampler of the class verifier: the class sampler of Paper/ClassSampler.lean for the compressed samplers at the fixed level C.

Equations

• MIPRE.Halting.sampProg G U Λ₀ R = G.samplerFamily.sampProg (MIPRE.Halting.C G) U Λ₀ R

theorem MIPRE.Halting.sampProg_wellScoped (G : GapCompression) (U : Cost.UniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.Prog.WellScoped 1 (sampProg G U Λ₀ R)

@[reducible, inline]

noncomputable abbrev MIPRE.Halting.dimB (G : GapCompression) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : ℕ

The compressor's bound poly(C, λ), in the total input length m: bounds the dimension and the times.

Equations

• MIPRE.Halting.dimB G Λ₀ R m = G.samplerFamily.dimB (MIPRE.Halting.C G) Λ₀ R m

@[reducible, inline]

noncomputable abbrev MIPRE.Halting.sampB (G : GapCompression) (U : Cost.UniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : ℕ

The sampler's cost, in the total input length.

Equations

• MIPRE.Halting.sampB G U Λ₀ R m = G.samplerFamily.sampB (MIPRE.Halting.C G) U Λ₀ R m

theorem MIPRE.Halting.dimz_le (G : GapCompression) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z : Cost.BitStr) (m : ℕ) (hm : List.length z ≤ m) : dimz G Λ₀ R z ≤ dimB G Λ₀ R m

theorem MIPRE.Halting.sampProg_runs (G : GapCompression) (U : Cost.UniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z r : Cost.BitStr) (hd : dimz G Λ₀ R z ≤ List.length r) : ∃ t ≤ sampB G U Λ₀ R (List.length z + List.length r), (sampProg G U Λ₀ R).Runs (Cost.encode (z, r)) (Cost.encode (qOf G Λ₀ R Player.alice z r, qOf G Λ₀ R Player.bob z r)) t

The sampler's run: on (z, r) with r at least dimz z long, it halts with the question pair of the seed within sampB (|z| + |r|).

The decider

noncomputable def MIPRE.Halting.MzF (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) Cost.Prog

q ↦ R z on the decider's input q = (z, x, y, a, b).

Equations

• MIPRE.Halting.MzF R = R.comp MIPRE.Cost.PolyTimeFun.fst

noncomputable def MIPRE.Halting.lamzF (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) ℕ

q ↦ λ(z).

Equations

• MIPRE.Halting.lamzF Λ₀ R = (MIPRE.Halting.lamF Λ₀).comp (MIPRE.Halting.MzF R)

def MIPRE.Halting.cutz (G : GapCompression) (Λ₀ K : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z : Cost.BitStr) : ℕ

The cutoff on the input z: 2 ^ (K + deg · |λ(z)|).

Equations

• MIPRE.Halting.cutz G Λ₀ K R z = 2 ^ (K + G.bound.natDegree * MIPRE.Cost.esize (MIPRE.Halting.lamz Λ₀ R z))

noncomputable def MIPRE.Halting.cutzF (G : GapCompression) (Λ₀ K : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) ℕ

q ↦ cutz z.

Equations

• MIPRE.Halting.cutzF G Λ₀ K R = (MIPRE.Halting.cutF K G.bound.natDegree).comp (MIPRE.Halting.lamzF Λ₀ R)

noncomputable def MIPRE.Halting.aF : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) Cost.BitStr

q ↦ a.

Equations

• MIPRE.Halting.aF = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd))

noncomputable def MIPRE.Halting.bF : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) Cost.BitStr

q ↦ b.

Equations

• MIPRE.Halting.bF = MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd))

noncomputable def MIPRE.Halting.wF (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) Cost.Prog

q ↦ wrapCore univ (ComputeSampler λ(z)) (dec (R z) λ(z)), the decider of 𝒱^halt.

Equations

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

noncomputable def MIPRE.Halting.wdec (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z : Cost.BitStr) : Cost.Prog

The decider of 𝒱^halt (R z) λ(z), wrapped.

Equations

• MIPRE.Halting.wdec G U UT Λ₀ R z = (MIPRE.Halting.Vpaper G U UT (R.toFun z) (MIPRE.Halting.lamz Λ₀ R z)).decider.prog

theorem MIPRE.Halting.wF_apply (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z x y a b : Cost.BitStr) : (wF G U UT Λ₀ R).toFun (z, x, y, a, b) = wdec G U UT Λ₀ R z

noncomputable def MIPRE.Halting.inputF (G : GapCompression) : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) Cost.Data

q ↦ encode (C, x, y, a, b), the decider's input at the fixed level.

Equations

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

noncomputable def MIPRE.Halting.rejF : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) (Cost.Prog × Cost.Data)

The rejecting branch: the constant-false program on the empty input.

Equations

• MIPRE.Halting.rejF = MIPRE.Cost.PolyTimeFun.const (MIPRE.Halting.falseProg, MIPRE.Cost.Data.nil)

noncomputable def MIPRE.Halting.D1 (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ K : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) (Cost.Prog × Cost.Data)

The preparation of the class decider: the program to run and its input — the constant-false program if a or b exceeds the cutoff, else 𝒱^halt's decider on (C, x, y, a, b).

Equations

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

theorem MIPRE.Halting.D1_apply (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ K : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z x y a b : Cost.BitStr) : (D1 G U UT Λ₀ K R).toFun (z, x, y, a, b) = if List.length a ≤ cutz G Λ₀ K R z then if List.length b ≤ cutz G Λ₀ K R z then (wdec G U UT Λ₀ R z, Cost.encode (C G, x, y, a, b)) else (falseProg, Cost.Data.nil) else (falseProg, Cost.Data.nil)

noncomputable def MIPRE.Halting.decProg (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ K : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.Prog

The decider of the class verifier: the preparation, then the universal machine.

Equations

• MIPRE.Halting.decProg G U UT Λ₀ K R = (MIPRE.Halting.D1 G U UT Λ₀ K R).code.seq U.univ

theorem MIPRE.Halting.decProg_wellScoped (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ K : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.Prog.WellScoped 1 (decProg G U UT Λ₀ K R)

theorem MIPRE.Halting.decProg_accepts (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ K : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z x y a b : Cost.BitStr) : (∃ (t : ℕ), (decProg G U UT Λ₀ K R).Runs (Cost.encode (z, x, y, a, b)) (Cost.encode true) t) ↔ List.length a ≤ cutz G Λ₀ K R z ∧ List.length b ≤ cutz G Λ₀ K R z ∧ (Vpaper G U UT (R.toFun z) (lamz Λ₀ R z)).decider.Accepts (C G) x y a b

Acceptance of the class decider: both answers within the cutoff, and 𝒱^halt's decider accepts at the fixed level.

noncomputable def MIPRE.Halting.TDB (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ K : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : ℕ

The preparation's cost, in the total input length.

Equations

• MIPRE.Halting.TDB G U UT Λ₀ K R m = Polynomial.eval (4 * m + 9) (MIPRE.Halting.D1 G U UT Λ₀ K R).timeBound

noncomputable def MIPRE.Halting.zB (G : GapCompression) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : ℕ

A common bound on the atoms of the wrapped decider's cost, in m.

Equations

• MIPRE.Halting.zB G Λ₀ R m = Polynomial.eval (4 * m + 1) R.timeBound + MIPRE.Halting.C G + MIPRE.Halting.lamB Λ₀ R m + (4 * m + 7)

noncomputable def MIPRE.Halting.decB (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ K : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : ℕ

The class decider's cost, in the total input length.

Equations

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

theorem MIPRE.Halting.decProg_runs (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (Λ₀ K : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z x y a b : Cost.BitStr) : ∃ (r : Cost.Data), ∃ t ≤ decB G U UT Λ₀ K R (List.length z + List.length x + List.length y + List.length a + List.length b), (decProg G U UT Λ₀ K R).Runs (Cost.encode (z, x, y, a, b)) r t

The class decider halts on every input within decB (|z| + |x| + |y| + |a| + |b|).