Runtime of the complete clocked exponential-index simulation

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

Equations

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

theorem MIPRE.Introspection.ClockSimulation.reindexProg_runs_cost (x : Cost.Data) : ∃ time ≤ reindexCost x, reindexProg.Runs x (reindexed x) time

noncomputable def MIPRE.Introspection.ClockSimulation.clockStageCost (k lam : ℕ) (x : Cost.Data) : ℕ

Equations

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

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

noncomputable def MIPRE.Introspection.ClockSimulation.reindexStageCost (source : Cost.Prog) (x : Cost.Data) (B : ℕ) : ℕ

Equations

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

theorem MIPRE.Introspection.ClockSimulation.reindexStage_runs_cost (source : Cost.Prog) (x : Cost.Data) (B : ℕ) : ∃ time ≤ reindexStageCost source x B, (reindexStage source).Runs (x.cons (Cost.Data.ofNat B)) ((Cost.Data.ofNat B).cons ((Cost.encode source).cons (reindexed x))) time

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

Equations

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

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

An explicit bound for every input, including malformed indices and queries.

noncomputable def MIPRE.Introspection.ClockSimulation.reindexCostPoly : Polynomial ℕ

Equations

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

noncomputable def MIPRE.Introspection.ClockSimulation.clockStageCostPoly (k : ℕ) : Polynomial ℕ

Equations

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

noncomputable def MIPRE.Introspection.ClockSimulation.reindexStageCostPoly : Polynomial ℕ

Equations

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

noncomputable def MIPRE.Introspection.ClockSimulation.simulationCostPoly (k : ℕ) (U : Cost.ClockedUniversalMachine) : Polynomial ℕ

Equations

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

theorem MIPRE.Introspection.ClockSimulation.reindexCost_le {x : Cost.Data} {B : ℕ} (hn : indexReader.toFun x ≤ B) (hx : x.size ≤ 64 * B) (hout : (reindexed x).size ≤ 64 * B) : reindexCost x ≤ Polynomial.eval B reindexCostPoly

theorem MIPRE.Introspection.ClockSimulation.clockStageCost_le {k lam : ℕ} {x : Cost.Data} (hk : 1 ≤ k) (hl : 1 ≤ lam) (hn : 1 ≤ indexReader.toFun x) (hx : x.size ≤ 64 * ansBound k lam (indexReader.toFun x)) : clockStageCost k lam x ≤ Polynomial.eval (ansBound k lam (indexReader.toFun x)) (clockStageCostPoly k)

theorem MIPRE.Introspection.ClockSimulation.simulationCost_le {k lam : ℕ} (U : Cost.ClockedUniversalMachine) (source : Cost.Prog) (x : Cost.Data) (hk : 1 ≤ k) (hl : 1 ≤ lam) (hn : 1 ≤ indexReader.toFun x) (hcode : Cost.esize source ≤ ansBound k lam (indexReader.toFun x)) (hx : x.size ≤ 64 * ansBound k lam (indexReader.toFun x)) (hout : (reindexed x).size ≤ 64 * ansBound k lam (indexReader.toFun x)) : simulationCost k lam U source x ≤ Polynomial.eval (ansBound k lam (indexReader.toFun x)) (simulationCostPoly k U)

Uniform polynomial overhead in the budget, once it dominates the source and inputs.

theorem MIPRE.Introspection.ClockSimulation.legal_input_sizes {k lam n : ℕ} (hk : 1 ≤ k) (hl : 1 ≤ 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) : Cost.esize (n, x, y, a, b) ≤ 64 * ansBound k lam n ∧ Cost.esize (2 ^ n, x, y, a, b) ≤ 64 * ansBound k lam n

theorem MIPRE.Introspection.ClockSimulation.decider_ansBound_time (k : ℕ) (hk : 1 ≤ k) (U : Cost.ClockedUniversalMachine) : ∃ (C : ℕ), ∀ (lam n : ℕ) (source : Cost.Prog), 1 ≤ lam → 1 ≤ n → Cost.esize source ≤ lam → ∀ (x y a b : Cost.BitStr), List.length x ≤ (2 ^ n) ^ lam → List.length y ≤ (2 ^ n) ^ lam → List.length a ≤ (2 ^ n) ^ lam → List.length b ≤ (2 ^ n) ^ lam → Cost.HaltsWithin (decider k lam U source).prog (Cost.encode (n, x, y, a, b)) (ansBound C lam n)

A uniform absolute runtime for the entire compiled clocked decider, including clock generation, index conversion, simulation and the final result check.

theorem MIPRE.Introspection.ClockSimulation.original_decider_ansBound_time (U : Cost.ClockedUniversalMachine) : ∃ (C : ℕ), ∀ {ℓ lam n : ℕ} (V : Verifier ℓ), V.IsBounded lam → 1 ≤ n → ∀ (x y a b : Cost.BitStr), List.length x ≤ (2 ^ n) ^ lam → List.length y ≤ (2 ^ n) ^ lam → List.length a ≤ (2 ^ n) ^ lam → List.length b ≤ (2 ^ n) ^ lam → Cost.HaltsWithin (decider 5 lam U V.decider.prog).prog (Cost.encode (n, x, y, a, b)) (ansBound C lam n)