Clocked simulation as a polynomial-time predicate

Given a clocked universal machine UT, PolyTimeFun.haltsWithin UT : PolyTimeFun (Prog × ℕ) Bool decides whether e halts on the empty input within Nat.size n steps: it computes the budget in unary from the binary n (lenProg), assembles the machine's input (ofNat k, (encode e, nil)), runs UT.univT, and reads the halting flag of clockedResult. This is the "run e for log n steps" of [MNY, Lemma 5.1].

def MIPRE.Cost.Prog.haltsWithinProg (univT : Prog) : Prog

The program of PolyTimeFun.haltsWithin. Input: cons (encode e) (encode n).

Equations

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

theorem MIPRE.Cost.Prog.haltsWithinProg_wellScoped {univT : Prog} (hU : WellScoped 1 univT) : WellScoped 1 univT.haltsWithinProg

theorem MIPRE.Cost.Prog.haltsWithinProg_runs (UT : ClockedUniversalMachine) (e : Prog) (n : ℕ) : ∃ t ≤ Polynomial.eval (n.size + esize e + 1) UT.bound + (n.size + 1 + 1) * (esize n + 1 + 2 * n.size + 13) + 3 * esize e + 4 * n.size + 2 * esize n + 40, UT.univT.haltsWithinProg.Runs ((encode e).cons (encode n)) (encode (evalWithin e Data.nil n.size).isSome) t

The run of haltsWithinProg, in terms of the clocked machine's result.

noncomputable def MIPRE.Cost.PolyTimeFun.haltsWithin (UT : ClockedUniversalMachine) : PolyTimeFun (Prog × ℕ) Bool

Decides "e halts on the empty input within Nat.size n steps", in polynomial time, given a clocked universal machine.

Equations

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

@[simp]

theorem MIPRE.Cost.PolyTimeFun.haltsWithin_apply (UT : ClockedUniversalMachine) (e : Prog) (n : ℕ) : (haltsWithin UT).toFun (e, n) = (evalWithin e Data.nil n.size).isSome