The actual growing introspection clock

The closed clock program writes the exact repaired introspection budget in unary. Hardwiring the binary parameter has linear description overhead, and the compiler itself is an actual polynomial-time ambient program.

def MIPRE.Introspection.growingClock (k lam : ℕ) : CL.Detyping.ClockProgram

The executable polynomial-exponent clock, with the parameter stored in binary.

Equations

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

theorem MIPRE.Introspection.growingClock_budget (k lam n : ℕ) : (growingClock k lam).budget n = ansBound k lam n

theorem MIPRE.Introspection.growingClock_runs (k lam n : ℕ) : ∃ time ≤ ClockArithmetic.uniformCost k lam n + Cost.esize lam + Cost.esize n + 3, (growingClock k lam).prog.Runs (Cost.encode n) (Cost.Data.ofNat (ansBound k lam n)) time

theorem MIPRE.Introspection.growingClock_haltsWithin (k lam n : ℕ) : Cost.HaltsWithin (growingClock k lam).prog (Cost.encode n) (ClockArithmetic.uniformCost k lam n + Cost.esize lam + Cost.esize n + 3)

theorem MIPRE.Introspection.growingClock_size (k lam : ℕ) : Cost.esize (growingClock k lam).prog = Cost.esize (ClockArithmetic.uniformProg k) + Cost.esize lam + 35

No unary parameter or budget is embedded in the program description.

noncomputable def MIPRE.Introspection.growingClockCompiler (k : ℕ) : Cost.PolyTimeFun ℕ Cost.Prog

The actual uniform compiler for the parameterized clocks.

Equations

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

theorem MIPRE.Introspection.growingClockCompiler_apply (k lam : ℕ) : (growingClockCompiler k).toFun lam = (growingClock k lam).prog

theorem MIPRE.Introspection.growingClockCompiler_runs (k lam : ℕ) : ∃ time ≤ Polynomial.eval (Cost.esize lam) (growingClockCompiler k).timeBound, (growingClockCompiler k).code.Runs (Cost.encode lam) (Cost.encode (growingClock k lam).prog) time

Compiler execution takes polynomial time in the binary parameter length.