Total clocking of arbitrary typed decision programs

An executable index clock writes a unary cost budget. The clocked universal machine simulates the arbitrary source program under that budget, and the wrapper accepts exactly an in-budget return of encode true. No termination or well-scopedness assumption is imposed on the source program.

structure MIPRE.CL.Detyping.ClockProgram : Type

An actual index routine that supplies a unary simulation budget.

• budget : ℕ → ℕ
• prog : Cost.Prog
• closed : Cost.Prog.WellScoped 1 self.prog
• runs (n : ℕ) : ∃ (time : ℕ), self.prog.Runs (Cost.encode n) (Cost.Data.ofNat (self.budget n)) time

def MIPRE.CL.Detyping.ClockProgram.constant (k : ℕ) : ClockProgram

A concrete executable clock, useful independently of any index-growth routine.

Equations

• MIPRE.CL.Detyping.ClockProgram.constant k = { budget := fun (x : ℕ) => k, prog := MIPRE.Cost.Prog.const (MIPRE.Cost.Data.ofNat k), closed := trivial, runs := ⋯ }

def MIPRE.CL.Detyping.ClockProgram.ofPolyTimeFun (f : Cost.PolyTimeFun ℕ Cost.Unary) : ClockProgram

Any polynomial-time unary index routine supplies an executable clock.

Equations

• MIPRE.CL.Detyping.ClockProgram.ofPolyTimeFun f = { budget := fun (n : ℕ) => List.length (f.toFun n), prog := f.code, closed := ⋯, runs := ⋯ }

theorem MIPRE.CL.Detyping.ClockProgram.evalWithin_eq_some_iff (c : Cost.Prog) (x r : Cost.Data) (k : ℕ) : Cost.evalWithin c x k = some r ↔ ∃ time ≤ k, c.Runs x r time

theorem MIPRE.CL.Detyping.ClockProgram.clockedResult_eq_iff (c : Cost.Prog) (x r : Cost.Data) (k : ℕ) : Cost.clockedResult c x k = (Cost.encode true).cons r ↔ ∃ time ≤ k, c.Runs x r time

The success tag carries precisely the source result of an in-budget run.

noncomputable def MIPRE.CL.Detyping.ClockProgram.clockRoute : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)

Equations

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

noncomputable def MIPRE.CL.Detyping.ClockProgram.clockPost (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.CL.Detyping.ClockProgram.checkResult : Cost.PolyTimeFun Cost.Data Bool

Equations

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

noncomputable def MIPRE.CL.Detyping.ClockProgram.clockStage (C : ClockProgram) (source : Cost.Prog) : Cost.Prog

Equations

• C.clockStage source = MIPRE.Cost.Prog.routeOneCall MIPRE.CL.Detyping.ClockProgram.clockRoute C.prog (MIPRE.CL.Detyping.ClockProgram.clockPost source)

theorem MIPRE.CL.Detyping.ClockProgram.clockStage_closed (C : ClockProgram) (source : Cost.Prog) : Cost.Prog.WellScoped 1 (C.clockStage source)

theorem MIPRE.CL.Detyping.ClockProgram.clockStage_runs (C : ClockProgram) (source : Cost.Prog) (x : Cost.Data) : ∃ (time : ℕ), (C.clockStage source).Runs x ((Cost.Data.ofNat (C.budget (Program.readNat.toFun (Cost.PolyTimeFun.treeHead.toFun x)))).cons ((Cost.encode source).cons x)) time

noncomputable def MIPRE.CL.Detyping.ClockProgram.wrapProg (C : ClockProgram) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog) : Cost.Prog

Equations

• C.wrapProg U source = (C.clockStage source).let_ (U.univT.let_ MIPRE.CL.Detyping.ClockProgram.checkResult.code)

theorem MIPRE.CL.Detyping.ClockProgram.wrapProg_closed (C : ClockProgram) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog) : Cost.Prog.WellScoped 1 (C.wrapProg U source)

theorem MIPRE.CL.Detyping.ClockProgram.wrapProg_runs (C : ClockProgram) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog) (x : Cost.Data) : ∃ (time : ℕ), (C.wrapProg U source).Runs x (Cost.encode (decide (Cost.clockedResult source x (C.budget (Program.readNat.toFun (Cost.PolyTimeFun.treeHead.toFun x))) = (Cost.encode true).cons (Cost.encode true)))) time

The exact Boolean returned by the executable clock wrapper on every raw input.

theorem MIPRE.CL.Detyping.ClockProgram.wrapProg_halts (C : ClockProgram) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog) (x : Cost.Data) : Cost.Halts (C.wrapProg U source) x

noncomputable def MIPRE.CL.Detyping.ClockProgram.wrapCost (C : ClockProgram) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog) (x : Cost.Data) (clockTime : ℕ) : ℕ

The explicit wrapper cost, including clock generation and universal simulation.

Equations

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

theorem MIPRE.CL.Detyping.ClockProgram.wrapProg_haltsWithin (C : ClockProgram) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog) (x : Cost.Data) (clockTime : ℕ) (hC : Cost.HaltsWithin C.prog (Cost.encode (Program.readNat.toFun (Cost.PolyTimeFun.treeHead.toFun x))) clockTime) : Cost.HaltsWithin (C.wrapProg U source) x (C.wrapCost U source x clockTime)

Runtime overhead is explicit once the executable clock's own runtime is bounded.

theorem MIPRE.CL.Detyping.ClockProgram.wrapProg_accepts_iff (C : ClockProgram) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog) (x : Cost.Data) : (∃ (time : ℕ), (C.wrapProg U source).Runs x (Cost.encode true) time) ↔ ∃ time ≤ C.budget (Program.readNat.toFun (Cost.PolyTimeFun.treeHead.toFun x)), source.Runs x (Cost.encode true) time

Acceptance is exactly acceptance of the source within the computed cost budget.

noncomputable def MIPRE.CL.Detyping.ClockProgram.wrap {T : Type u_1} [Cost.SizedEncoding T] (C : ClockProgram) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog) : TypedDecider T

The genuine typed decider obtained by clocking arbitrary source code.

Equations

• C.wrap U source = { prog := C.wrapProg U source, closed := ⋯ }

theorem MIPRE.CL.Detyping.ClockProgram.wrap_total {T : Type u_1} [Cost.SizedEncoding T] (C : ClockProgram) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog) : (C.wrap U source).Total

theorem MIPRE.CL.Detyping.ClockProgram.wrap_accepts_iff {T : Type u_1} [Cost.SizedEncoding T] (C : ClockProgram) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog) (n : ℕ) (u : T) (x : Cost.BitStr) (v : T) (y a b : Cost.BitStr) : (C.wrap U source).Accepts n u x v y a b ↔ ∃ time ≤ C.budget n, source.Runs (Cost.encode (n, u, x, v, y, a, b)) (Cost.encode true) time

theorem MIPRE.CL.Detyping.ClockProgram.wrap_accepts_iff_of_bounded {T : Type u_1} [Cost.SizedEncoding T] (C : ClockProgram) (U : Cost.ClockedUniversalMachine) (D : TypedDecider T) (n : ℕ) (u : T) (x : Cost.BitStr) (v : T) (y a b : Cost.BitStr) (h : Cost.HaltsWithin D.prog (Cost.encode (n, u, x, v, y, a, b)) (C.budget n)) : (C.wrap U D.prog).Accepts n u x v y a b ↔ D.Accepts n u x v y a b

Whenever a source run is known to fit, clocking preserves its acceptance predicate.

noncomputable def MIPRE.CL.Detyping.ClockProgram.decider {T : Type u_1} [Cost.SizedEncoding T] (C : ClockProgram) (source : Cost.Prog) : TypedDecider T

The wrapper instantiated with the proved clocked self-interpreter.

Equations

• C.decider source = C.wrap MIPRE.Cost.selfClockedUniversal source

theorem MIPRE.CL.Detyping.ClockProgram.decider_total {T : Type u_1} [Cost.SizedEncoding T] (C : ClockProgram) (source : Cost.Prog) : (C.decider source).Total

theorem MIPRE.CL.Detyping.ClockProgram.decider_accepts_iff {T : Type u_1} [Cost.SizedEncoding T] (C : ClockProgram) (source : Cost.Prog) (n : ℕ) (u : T) (x : Cost.BitStr) (v : T) (y a b : Cost.BitStr) : (C.decider source).Accepts n u x v y a b ↔ ∃ time ≤ C.budget n, source.Runs (Cost.encode (n, u, x, v, y, a, b)) (Cost.encode true) time