Exact acceptance of the cross-introspection compiler

For a bounded original verifier the actual dimension query fits the clock. Acceptance is precisely the complete format/cutoff/projection guard followed by acceptance of the original decider at the exponential index.

noncomputable def MIPRE.Introspection.SourceCompiler.preparedData (c k lam : ℕ) (S : Cost.Prog) (x : Cost.Data) : Cost.Data

Equations

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

theorem MIPRE.Introspection.SourceCompiler.crossProg_run_final (c k lam : ℕ) (U : Cost.ClockedUniversalMachine) (S D : Cost.Prog) (x r : Cost.Data) (t : ℕ) (hr : (finalStage k lam U D).Runs (preparedData c k lam S x) r t) : ∃ (time : ℕ), (crossProg c k lam U S D).Runs x r time

theorem MIPRE.Introspection.SourceCompiler.crossProg_accepts_final (c k lam : ℕ) (U : Cost.ClockedUniversalMachine) (S D : Cost.Prog) (x : Cost.Data) : (∃ (t : ℕ), (crossProg c k lam U S D).Runs x (Cost.encode true) t) ↔ ∃ (t : ℕ), (finalStage k lam U D).Runs (preparedData c k lam S x) (Cost.encode true) t

theorem MIPRE.Introspection.SourceCompiler.finalStage_accepts_iff (k lam : ℕ) (U : Cost.ClockedUniversalMachine) (D : Cost.Prog) (x : Cost.Data) : (∃ (t : ℕ), (finalStage k lam U D).Runs x (Cost.encode true) t) ↔ Prepared x ∧ GuardReady (finalInput.toFun x) ∧ ∃ (t : ℕ), (ClockSimulation.decider k lam U D).prog.Runs (projectedCall.toFun (finalInput.toFun x)) (Cost.encode true) t

theorem MIPRE.Introspection.SourceCompiler.bounded_dimensionResult {ℓ lam n : ℕ} (V : Verifier ℓ) (hV : V.IsBounded lam) (hn : 1 ≤ n) : dimensionResult 5 lam V.sampler.prog n = (Cost.encode true).cons (Cost.encode (V.sampler.dim (2 ^ n)))

The actual sampler query, rather than an assumed dimension subroutine, fits exponent five.

theorem MIPRE.Introspection.SourceCompiler.finalInput_canonical (n Q R s : ℕ) (a b : Cost.BitStr) : finalInput.toFun (((Cost.encode (n, a, b)).cons (Cost.encode (Q, R))).cons ((Cost.encode true).cons (Cost.encode s))) = (n, Q, R, s, a, b)

theorem MIPRE.Introspection.SourceCompiler.prepared_canonical (n Q R s : ℕ) (a b : Cost.BitStr) : Prepared (((Cost.encode (n, a, b)).cons (Cost.encode (Q, R))).cons ((Cost.encode true).cons (Cost.encode s)))

theorem MIPRE.Introspection.SourceCompiler.crossProg_original_iff {ℓ lam n : ℕ} (c : ℕ) (U : Cost.ClockedUniversalMachine) (V : Verifier ℓ) (hV : V.IsBounded lam) (hn : 1 ≤ n) (a b : Cost.BitStr) : (∃ (t : ℕ), (crossProg c 5 lam U V.sampler.prog V.decider.prog).Runs (Cost.encode (n, a, b)) (Cost.encode true) t) ↔ have x := (n, registerBits c lam n, originalBound lam n, V.sampler.dim (2 ^ n), a, b); GuardReady x ∧ V.decider.Accepts (2 ^ n) (List.take (inputDim.toFun x) (leftParts.toFun x).1) (List.take (inputDim.toFun x) (rightParts.toFun x).1) (leftParts.toFun x).2 (rightParts.toFun x).2

Exact source-game interpretation, including the internal original-answer cutoff. The sole verifier hypothesis is its existing boundedness definition.