Explicit runtime of canonical parameter generation

def MIPRE.Introspection.SourceCompiler.exponentBitsCost (j : ℕ) : ℕ

Equations

• MIPRE.Introspection.SourceCompiler.exponentBitsCost j = (j + 2) * (4 * j + 20)

def MIPRE.Introspection.SourceCompiler.powerUnaryCost (j : ℕ) : ℕ

Equations

• MIPRE.Introspection.SourceCompiler.powerUnaryCost j = MIPRE.Introspection.SourceCompiler.exponentBitsCost j + MIPRE.Introspection.ClockArithmetic.unaryCost (2 ^ j) + 1

theorem MIPRE.Introspection.SourceCompiler.powerUnaryProg_runs_cost (j : ℕ) : ∃ t ≤ powerUnaryCost j, powerUnaryProg.Runs (Cost.Data.ofNat j) (Cost.Data.ofNat (2 ^ j)) t

def MIPRE.Introspection.SourceCompiler.contextCost (post : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data) (a ctx r : Cost.Data) (t : ℕ) : ℕ

Equations

• MIPRE.Introspection.SourceCompiler.contextCost post a ctx r t = 2 * a.size + 2 * ctx.size + r.size + t + Polynomial.eval (ctx.size + r.size + 1) post.timeBound + 12

noncomputable def MIPRE.Introspection.SourceCompiler.boundsCost (c lam n : ℕ) : ℕ

Equations

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

theorem MIPRE.Introspection.SourceCompiler.boundsProg_runs_cost (c lam n : ℕ) : ∃ time ≤ boundsCost c lam n, (boundsProg c).Runs (Cost.encode (lam, n)) (Cost.encode (registerBits c lam n, originalBound lam n)) time