Executable clocked simulation at the original exponential index

The clock is computed at index n; the source program receives index 2^n. Both transformations are actual programs. The repaired exponent-five bound preserves the original bounded decider on its legal question and answer cut.

noncomputable def MIPRE.Introspection.ClockSimulation.indexReader : Cost.PolyTimeFun Cost.Data ℕ

Equations

• MIPRE.Introspection.ClockSimulation.indexReader = MIPRE.CL.Detyping.Program.readNat.comp MIPRE.Cost.PolyTimeFun.treeHead

noncomputable def MIPRE.Introspection.ClockSimulation.reindexed (x : Cost.Data) : Cost.Data

Equations

• MIPRE.Introspection.ClockSimulation.reindexed x = (MIPRE.Cost.encode (2 ^ MIPRE.Introspection.ClockSimulation.indexReader.toFun x)).cons (MIPRE.Cost.PolyTimeFun.treeTail.toFun x)

noncomputable def MIPRE.Introspection.ClockSimulation.reindexProg : Cost.Prog

Equations

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

theorem MIPRE.Introspection.ClockSimulation.reindexProg_closed : Cost.Prog.WellScoped 1 reindexProg

theorem MIPRE.Introspection.ClockSimulation.reindexProg_runs (x : Cost.Data) : ∃ (time : ℕ), reindexProg.Runs x (reindexed x) time

The source-index adapter is total even when the incoming index is malformed.

theorem MIPRE.Introspection.ClockSimulation.reindexed_cons (n : ℕ) (d : Cost.Data) : reindexed ((Cost.encode n).cons d) = (Cost.encode (2 ^ n)).cons d

noncomputable def MIPRE.Introspection.ClockSimulation.clockStage (k lam : ℕ) : Cost.Prog

Equations

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

theorem MIPRE.Introspection.ClockSimulation.clockStage_closed (k lam : ℕ) : Cost.Prog.WellScoped 1 (clockStage k lam)

theorem MIPRE.Introspection.ClockSimulation.clockStage_runs (k lam : ℕ) (x : Cost.Data) : ∃ (time : ℕ), (clockStage k lam).Runs x (x.cons (Cost.Data.ofNat (ansBound k lam (indexReader.toFun x)))) time

noncomputable def MIPRE.Introspection.ClockSimulation.simulationInput (source : Cost.Prog) : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data

Equations

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

noncomputable def MIPRE.Introspection.ClockSimulation.reindexStage (source : Cost.Prog) : Cost.Prog

Equations

• MIPRE.Introspection.ClockSimulation.reindexStage source = MIPRE.Introspection.ClockSimulation.reindexProg.callWithContext (MIPRE.Introspection.ClockSimulation.simulationInput source)

theorem MIPRE.Introspection.ClockSimulation.reindexStage_closed (source : Cost.Prog) : Cost.Prog.WellScoped 1 (reindexStage source)

theorem MIPRE.Introspection.ClockSimulation.reindexStage_runs (source : Cost.Prog) (x : Cost.Data) (budget : ℕ) : ∃ (time : ℕ), (reindexStage source).Runs (x.cons (Cost.Data.ofNat budget)) ((Cost.Data.ofNat budget).cons ((Cost.encode source).cons (reindexed x))) time

noncomputable def MIPRE.Introspection.ClockSimulation.prog (k lam : ℕ) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog) : Cost.Prog

This program computes the growing budget, changes the source index, and simulates.

Equations

• MIPRE.Introspection.ClockSimulation.prog k lam U source = (MIPRE.Introspection.ClockSimulation.clockStage k lam).let_ ((MIPRE.Introspection.ClockSimulation.reindexStage source).let_ U.univT)

theorem MIPRE.Introspection.ClockSimulation.prog_closed (k lam : ℕ) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog) : Cost.Prog.WellScoped 1 (prog k lam U source)

theorem MIPRE.Introspection.ClockSimulation.prog_runs (k lam : ℕ) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog) (x : Cost.Data) : ∃ (time : ℕ), (prog k lam U source).Runs x (Cost.clockedResult source (reindexed x) (ansBound k lam (indexReader.toFun x))) time

theorem MIPRE.Introspection.ClockSimulation.prog_halts (k lam : ℕ) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog) (x : Cost.Data) : Cost.Halts (prog k lam U source) x

noncomputable def MIPRE.Introspection.ClockSimulation.decider (k lam : ℕ) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog) : Decider

The resulting ordinary decider rejects timeouts and all nonaccepting results.

Equations

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

theorem MIPRE.Introspection.ClockSimulation.decider_runs (k lam : ℕ) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog) (x : Cost.Data) : ∃ (time : ℕ), (decider k lam U source).prog.Runs x (Cost.encode (decide (Cost.clockedResult source (reindexed x) (ansBound k lam (indexReader.toFun x)) = (Cost.encode true).cons (Cost.encode true)))) time

theorem MIPRE.Introspection.ClockSimulation.decider_halts (k lam : ℕ) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog) (x : Cost.Data) : Cost.Halts (decider k lam U source).prog x

theorem MIPRE.Introspection.ClockSimulation.decider_accepts_iff (k lam : ℕ) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog) (n : ℕ) (x y a b : Cost.BitStr) : (decider k lam U source).Accepts n x y a b ↔ ∃ time ≤ ansBound k lam n, source.Runs (Cost.encode (2 ^ n, x, y, a, b)) (Cost.encode true) time

theorem MIPRE.Introspection.ClockSimulation.original_decider_preserved {ℓ lam n : ℕ} (U : Cost.ClockedUniversalMachine) (V : Verifier ℓ) (hV : V.IsBounded lam) (hn : 1 ≤ n) (x y a b : Cost.BitStr) (hx : List.length x ≤ (2 ^ n) ^ lam) (hy : List.length y ≤ (2 ^ n) ^ lam) (ha : List.length a ≤ (2 ^ n) ^ lam) (hb : List.length b ≤ (2 ^ n) ^ lam) : (decider 5 lam U V.decider.prog).Accepts n x y a b ↔ V.decider.Accepts (2 ^ n) x y a b

The concrete exponent-five clock preserves the original bounded verifier on the original legal answer alphabet, without enlarging that alphabet.