The self-interpreter, II: the universal machines

The two universal machines of the toolkit (Cost/Toolkit.lean), built from the step program stepProg of Cost/Interpreter.lean:

• univProg runs the evaluation machine (Cost/Machine.lean) from the initial configuration of c on v until a final configuration, as a loop whose body tests finality (isFinalProg) and otherwise steps. A halting run of cost t takes at most 3 t machine steps (eval_steps_count), each on a configuration of size polynomial in esize c + v.size + t (eval_steps_bound_forever, size_toData_le), which gives the polynomial overhead (UniversalMachine.time_le); conversely a run of the loop is a machine run reaching a final configuration, hence a derivation (halts_iff).
• univTProg is the clocked variant: the loop additionally carries the remaining cost budget and a step budget 3 k + 1, both in unary, and a size guard Θ (a polynomial in k + esize c + v.size computed in unary). The step budget makes the loop terminate; the cost budget, decremented by the exact cost of each step (stepCostProg, matching stepCost), decides whether the simulated run halts within cost k; the size guard keeps the configurations handled by the loop polynomially bounded even when the simulated run does not halt — it never fires on a run that halts within the budget, whose configurations are bounded by Θ.

This discharges exists_efficient_universal and exists_clocked_universal (blueprint lem:universal-tm).

The final-configuration test

def MIPRE.Cost.Machine.isFinalProg : Prog

On the encoding of a configuration: cons nil r if it is final with value r, nil otherwise.

Equations

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

theorem MIPRE.Cost.Machine.isFinalProg_wellScoped : Prog.WellScoped 1 isFinalProg

theorem MIPRE.Cost.Machine.isFinalProg_final (r : Data) (e : Env) : ∃ t ≤ r.size + 8, isFinalProg.Runs { ctrl := Ctrl.ret r, env := e, kont := [] }.toData (Data.nil.cons r) t

theorem MIPRE.Cost.Machine.isFinalProg_nonfinal (c : Cfg) (h : ¬IsFinal c) : ∃ t ≤ 8, isFinalProg.Runs c.toData Data.nil t

The interpreter loop

def MIPRE.Cost.Machine.interpBody : Prog

Body of the interpreter loop: on a configuration, stop with its value if it is final, otherwise continue with the next configuration.

Equations

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

theorem MIPRE.Cost.Machine.interpBody_wellScoped : Prog.WellScoped 1 interpBody

def MIPRE.Cost.Machine.interpBodyBound (S : ℕ) : ℕ

Cost of one iteration of the interpreter loop on a configuration of size at most S.

Equations

• MIPRE.Cost.Machine.interpBodyBound S = MIPRE.Cost.Machine.stepBound S + 3 * S + 30

theorem MIPRE.Cost.Machine.stepBound_mono {S T : ℕ} (h : S ≤ T) : stepBound S ≤ stepBound T

theorem MIPRE.Cost.Machine.interpBodyBound_mono {S T : ℕ} (h : S ≤ T) : interpBodyBound S ≤ interpBodyBound T

theorem MIPRE.Cost.Machine.interpBody_final (r : Data) (e env : Env) : ∃ t ≤ 3 * { ctrl := Ctrl.ret r, env := e, kont := [] }.toData.size + 30, Eval ({ ctrl := Ctrl.ret r, env := e, kont := [] }.toData :: env) interpBody (Data.nil.cons r) t

theorem MIPRE.Cost.Machine.interpBody_step (c : Cfg) (h : ¬IsFinal c) (env : Env) : ∃ t ≤ interpBodyBound c.toData.size, Eval (c.toData :: env) interpBody ((Data.nil.cons Data.nil).cons (step c).toData) t

theorem MIPRE.Cost.Machine.interpLoop_runs (c₀ : Cfg) (S : ℕ) (hS : ∀ (n : ℕ), (step^[n] c₀).toData.size ≤ S) (r : Data) (e : Env) (N : ℕ) (hN : step^[N] c₀ = { ctrl := Ctrl.ret r, env := e, kont := [] }) (env : Env) (m n : ℕ) : n + m = N → ∃ t ≤ (m + 1) * (interpBodyBound S + 1), Eval ((step^[n] c₀).toData :: env) interpBody.loop r t

The interpreter loop, from the n-th configuration of a run that reaches a final configuration at step N, all of whose configurations have size at most S.

theorem MIPRE.Cost.Machine.interpLoop_rev (t : ℕ) (c : Cfg) (env : Env) (r : Data) : Eval (c.toData :: env) interpBody.loop r t → ∃ (N : ℕ) (e : Env), step^[N] c = { ctrl := Ctrl.ret r, env := e, kont := [] }

The loop, backwards: a run of the interpreter loop from a configuration reaches a final configuration with the same value.

The universal program

def MIPRE.Cost.Machine.univPrelude : Prog

On cons c v: the initial configuration of c on v, as data.

Equations

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

theorem MIPRE.Cost.Machine.univPrelude_runs (c v : Data) : ∃ t ≤ c.size + v.size + 10, Eval [c.cons v] univPrelude (initData c v) t

def MIPRE.Cost.Machine.univProg : Prog

The universal program: on cons (encode c) v, build the initial configuration of c on v and run the interpreter loop.

Equations

• MIPRE.Cost.Machine.univProg = MIPRE.Cost.Machine.univPrelude.let_ MIPRE.Cost.Machine.interpBody.loop

theorem MIPRE.Cost.Machine.univProg_wellScoped : Prog.WellScoped 1 univProg

def MIPRE.Cost.Machine.sigmaFun (X : ℕ) : ℕ

The size bound on the configurations of a halting run, in terms of X = esize c + v.size + t.

Equations

• MIPRE.Cost.Machine.sigmaFun X = MIPRE.Cost.Machine.cfgSizeBound X (3 * X) X (2 * X)

def MIPRE.Cost.Machine.univBoundFun (X : ℕ) : ℕ

The time bound of the universal program, in terms of X = esize c + v.size + t.

Equations

• MIPRE.Cost.Machine.univBoundFun X = (3 * X + 1) * (MIPRE.Cost.Machine.interpBodyBound (MIPRE.Cost.Machine.sigmaFun X) + 1) + 2 * X + 11

theorem MIPRE.Cost.Machine.univProg_time_le (c : Prog) (v r : Data) (t : ℕ) (h : c.Runs v r t) : ∃ t' ≤ univBoundFun (esize c + v.size + t), univProg.Runs ((encode c).cons v) r t'

theorem MIPRE.Cost.Machine.univProg_halts_of (c : Prog) (v r : Data) (t' : ℕ) (h : univProg.Runs ((encode c).cons v) r t') : ∃ (t : ℕ), c.Runs v r t

Unary arithmetic for the clock

def MIPRE.Cost.Machine.subBody : Prog

Loop body of subProg: on cons a b (unary), stop with the flagged difference cons (cons nil nil) (b - a) if a ≤ b, with nil otherwise.

Equations

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

def MIPRE.Cost.Machine.subProg : Prog

Unary subtraction with comparison: subProg on cons (ofNat a) (ofNat b) computes subResult a b.

Equations

• MIPRE.Cost.Machine.subProg = MIPRE.Cost.Machine.subBody.loop

theorem MIPRE.Cost.Machine.subBody_wellScoped : Prog.WellScoped 1 subBody

theorem MIPRE.Cost.Machine.subProg_wellScoped : Prog.WellScoped 1 subProg

def MIPRE.Cost.Machine.subResult (a b : ℕ) : Data

The value of subProg: the flagged difference, or nil when b < a.

Equations

• MIPRE.Cost.Machine.subResult a b = if a ≤ b then (MIPRE.Cost.Data.nil.cons MIPRE.Cost.Data.nil).cons (MIPRE.Cost.Data.ofNat (b - a)) else MIPRE.Cost.Data.nil

def MIPRE.Cost.Machine.subBound (a b : ℕ) : ℕ

Cost bound of subProg on cons (ofNat a) (ofNat b).

Equations

• MIPRE.Cost.Machine.subBound a b = (a + 1) * (2 * a + 2 * b + 14)

theorem MIPRE.Cost.Machine.subBound_mono {a b a' b' : ℕ} (ha : a ≤ a') (hb : b ≤ b') : subBound a b ≤ subBound a' b'

theorem MIPRE.Cost.Machine.subProg_runs (a b : ℕ) (env : Env) : ∃ t ≤ subBound a b, Eval ((Data.ofNat a).cons (Data.ofNat b) :: env) subProg (subResult a b) t

def MIPRE.Cost.Machine.tripleBody : Prog

Loop body of tripleProg: on cons (ofNat n) (ofNat m), ofNat (3 n + m).

Equations

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

def MIPRE.Cost.Machine.tripleProg : Prog

tripleProg on cons (ofNat n) (ofNat m) computes ofNat (3 n + m).

Equations

• MIPRE.Cost.Machine.tripleProg = MIPRE.Cost.Machine.tripleBody.loop

theorem MIPRE.Cost.Machine.tripleBody_wellScoped : Prog.WellScoped 1 tripleBody

theorem MIPRE.Cost.Machine.tripleProg_wellScoped : Prog.WellScoped 1 tripleProg

theorem MIPRE.Cost.Machine.tripleProg_runs (n m : ℕ) (env : Env) : ∃ t ≤ (n + 1) * (8 * n + 2 * m + 30), Eval ((Data.ofNat n).cons (Data.ofNat m) :: env) tripleProg (Data.ofNat (3 * n + m)) t

def MIPRE.Cost.Machine.repBody : Prog

Loop body of repProg: on cons (ofNat n) (cons d acc), n copies of d consed onto acc.

Equations

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

def MIPRE.Cost.Machine.repProg : Prog

repProg on cons (ofNat n) (cons d (list acc)) computes list (replicate n d ++ acc).

Equations

• MIPRE.Cost.Machine.repProg = MIPRE.Cost.Machine.repBody.loop

theorem MIPRE.Cost.Machine.repBody_wellScoped : Prog.WellScoped 1 repBody

theorem MIPRE.Cost.Machine.repProg_wellScoped : Prog.WellScoped 1 repProg

def MIPRE.Cost.Machine.repBound (n d a : ℕ) : ℕ

Cost bound of repProg for n copies of a value of size d onto an accumulator of size a.

Equations

• MIPRE.Cost.Machine.repBound n d a = (n + 1) * (4 * n + 4 * d + 2 * a + 30) + n * (n + 1) * (d + 1)

theorem MIPRE.Cost.Machine.repProg_runs (n : ℕ) (d : Data) (acc : List Data) (env : Env) : ∃ t ≤ repBound n d.size (Data.list acc).size, Eval ((Data.ofNat n).cons (d.cons (Data.list acc)) :: env) repProg (Data.list (List.replicate n d ++ acc)) t

theorem MIPRE.Cost.Machine.size_list_replicate (n : ℕ) (d : Data) : (Data.list (List.replicate n d)).size = n * (d.size + 1) + 1

The cost of a step, as a program

def MIPRE.Cost.Machine.costVar : Prog

Cost of a var step: cons body env ↦ ofNat ((getList env body).size + 1).

Equations

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

def MIPRE.Cost.Machine.costConst : Prog

Cost of a const step: cons d env ↦ ofNat d.size.

Equations

• MIPRE.Cost.Machine.costConst = MIPRE.Cost.Prog.elim 0 MIPRE.Cost.Prog.nil (MIPRE.Cost.Prog.callVar 0 MIPRE.Cost.Prog.sizeProg)

def MIPRE.Cost.Machine.costCases : List Prog

The case programs of the cost of an "evaluate" step, indexed by the tag.

Equations

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

theorem MIPRE.Cost.Machine.costVar_wellScoped : Prog.WellScoped 1 costVar

theorem MIPRE.Cost.Machine.costConst_wellScoped : Prog.WellScoped 1 costConst

theorem MIPRE.Cost.Machine.costCases_wellScoped (c : Prog) : c ∈ costCases → Prog.WellScoped 1 c

def MIPRE.Cost.Machine.stepCostEv : Prog

The cost of an "evaluate" step; environment [tag, payload, ctrl, rest, d].

Equations

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

def MIPRE.Cost.Machine.stepCostRet : Prog

The cost of a "return" step: 1 at a loop1 frame, 0 otherwise; environment [t₁, t₂, tag, payload, ctrl, rest, d].

Equations

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

def MIPRE.Cost.Machine.stepCostProg : Prog

On the encoding of a configuration c: ofNat (stepCost c).

Equations

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

theorem MIPRE.Cost.Machine.stepCostRet_wellScoped : Prog.WellScoped 7 stepCostRet

theorem MIPRE.Cost.Machine.stepCostEv_wellScoped : Prog.WellScoped 5 stepCostEv

theorem MIPRE.Cost.Machine.stepCostProg_wellScoped : Prog.WellScoped 1 stepCostProg

def MIPRE.Cost.Machine.stepCostBound (S : ℕ) : ℕ

Cost bound of stepCostProg on a configuration of size S.

Equations

• MIPRE.Cost.Machine.stepCostBound S = (S + 1) * (7 * S + 32) + 13 * S + 50

theorem MIPRE.Cost.Machine.stepCostBound_mono {S T : ℕ} (h : S ≤ T) : stepCostBound S ≤ stepCostBound T

theorem MIPRE.Cost.Machine.stepCostProg_ev (k : ℕ) (body env kont r : Data) {t : ℕ} (hk : k < costCases.length) (h : Eval [body.cons env] (costCases.getD k Prog.nil) r t) : ∃ s ≤ t + 2 * body.size + 2 * env.size + kont.size + k + 14, Eval [(Data.nil.cons ((Data.ofNat k).cons body)).cons (env.cons kont)] stepCostProg r s

The prefix of stepCostProg on an "evaluate" configuration, up to the dispatch.

theorem MIPRE.Cost.Machine.stepCost_le_size (c : Cfg) : stepCost c ≤ c.toData.size

theorem MIPRE.Cost.Machine.stepCostProg_runs (c : Cfg) : ∃ t ≤ stepCostBound c.toData.size, stepCostProg.Runs c.toData (Data.ofNat (stepCost c)) t

stepCostProg computes the cost of a step, at a cost quadratic in the size of the configuration.

The clocked interpreter loop

def MIPRE.Cost.Machine.clockState (d rem budget theta : Data) : Data

The state of the clocked loop: the configuration, the remaining cost budget, the remaining step budget and the size guard (the last three in unary).

Equations

• MIPRE.Cost.Machine.clockState d rem budget theta = d.cons (rem.cons (budget.cons theta))

def MIPRE.Cost.Machine.clockRest : Prog

Second half of a step of the clocked loop, after the cost subtraction succeeded: step, then check the size of the new configuration against the guard; environment [cons nil nil, rem', sub, cr, nil, budget', nil, budget, theta, rem, r₂, d, r₁, s].

Equations

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

def MIPRE.Cost.Machine.clockStep : Prog

The step of the clocked loop on a non-final configuration; environment [flag, budget, theta, rem, r₂, d, r₁, s] with flag = nil: stop with nil if the step budget is exhausted or the cost of the step exceeds the remaining cost budget, else clockRest.

Equations

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

def MIPRE.Cost.Machine.clockBody : Prog

Body of the clocked loop: stop with the flagged value of a final configuration, otherwise clockStep.

Equations

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

theorem MIPRE.Cost.Machine.clockRest_wellScoped : Prog.WellScoped 14 clockRest

theorem MIPRE.Cost.Machine.clockStep_wellScoped : Prog.WellScoped 8 clockStep

theorem MIPRE.Cost.Machine.clockBody_wellScoped : Prog.WellScoped 1 clockBody

def MIPRE.Cost.Machine.sizeBound (s : ℕ) : ℕ

Cost bound of sizeProg on a value of size s (as in sizeProg_runs).

Equations

• MIPRE.Cost.Machine.sizeBound s = (s + 1) * (5 * s + 20) + s + 6

theorem MIPRE.Cost.Machine.sizeBound_mono {s t : ℕ} (h : s ≤ t) : sizeBound s ≤ sizeBound t

def MIPRE.Cost.Machine.clockRestBound (S Θ rem b : ℕ) : ℕ

Bound on the second half of a step of the clocked loop, in terms of the configuration size S, the guard Θ, the remaining cost rem and the step budget b.

Equations

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

def MIPRE.Cost.Machine.clockBodyBound (Θ k : ℕ) : ℕ

Bound of one iteration of the clocked loop, on configurations of size at most Θ, with cost budget at most k (and step budget at most 3 k + 1).

Equations

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

theorem MIPRE.Cost.Machine.clockBody_final (r : Data) (e : Env) (rem budget theta : Data) (env : Env) : ∃ t ≤ 3 * { ctrl := Ctrl.ret r, env := e, kont := [] }.toData.size + 30, Eval (clockState { ctrl := Ctrl.ret r, env := e, kont := [] }.toData rem budget theta :: env) clockBody (Data.nil.cons ((Data.nil.cons Data.nil).cons r)) t

theorem MIPRE.Cost.Machine.clockBody_budget0 (c : Cfg) (hc : ¬IsFinal c) (rem theta : Data) (env : Env) : ∃ t ≤ c.toData.size + 20, Eval (clockState c.toData rem (Data.ofNat 0) theta :: env) clockBody (Data.nil.cons Data.nil) t

def MIPRE.Cost.Machine.clockEnv (c : Cfg) (rem b Θ : ℕ) (env : Env) : Env

The environment of clockStep after the cost subtraction, on a configuration c with remaining cost rem, step budget b + 1 and guard Θ.

Equations

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

theorem MIPRE.Cost.Machine.clockBody_prefix (c : Cfg) (hc : ¬IsFinal c) (rem b Θ : ℕ) (env : Env) (r : Data) {t : ℕ} (hrest : Eval (clockEnv c rem b Θ env) (Prog.elim 0 (Prog.nil.cons Prog.nil) clockRest) r t) : ∃ s ≤ t + stepCostBound c.toData.size + subBound (stepCost c) rem + 4 * c.toData.size + 4 * rem + 30, Eval (clockState c.toData (Data.ofNat rem) (Data.ofNat (b + 1)) (Data.ofNat Θ) :: env) clockBody r s

The first half of a step of the clocked loop on a non-final configuration with a positive step budget: the finality test, the cost of the step and its subtraction.

theorem MIPRE.Cost.Machine.clockRest_stop (c : Cfg) (rem b Θ : ℕ) (env : Env) (hle : stepCost c ≤ rem) (hΘ : Θ < (step c).toData.size) : ∃ t ≤ clockRestBound c.toData.size Θ rem b, Eval (clockEnv c rem b Θ env) (Prog.elim 0 (Prog.nil.cons Prog.nil) clockRest) (Data.nil.cons Data.nil) t

theorem MIPRE.Cost.Machine.clockRest_continue (c : Cfg) (rem b Θ : ℕ) (env : Env) (hle : stepCost c ≤ rem) (hΘ : (step c).toData.size ≤ Θ) : ∃ t ≤ clockRestBound c.toData.size Θ rem b, Eval (clockEnv c rem b Θ env) (Prog.elim 0 (Prog.nil.cons Prog.nil) clockRest) ((Data.nil.cons Data.nil).cons (clockState (step c).toData (Data.ofNat (rem - stepCost c)) (Data.ofNat b) (Data.ofNat Θ))) t

theorem MIPRE.Cost.Machine.clockBody_cost_le {S Θ k rem b cost t₂ t₁ : ℕ} (hS : S ≤ Θ) (hrem : rem ≤ k) (hb : b ≤ 3 * k) (hcost : cost ≤ S) (ht₂ : t₂ ≤ clockRestBound S Θ rem b) (ht₁ : t₁ ≤ t₂ + stepCostBound S + subBound cost rem + 4 * S + 4 * rem + 30) : t₁ ≤ clockBodyBound Θ k

The cost of one non-final iteration is at most clockBodyBound Θ k.

The semantics of the clocked loop

def MIPRE.Cost.Machine.Cfg.val : Cfg → Data

The value of a configuration: the returned value, nil on an "evaluate" control.

Equations

• { ctrl := MIPRE.Cost.Machine.Ctrl.ret v, env := env, kont := kont }.val = v
• { ctrl := MIPRE.Cost.Machine.Ctrl.ev p, env := env, kont := kont }.val = MIPRE.Cost.Data.nil

noncomputable def MIPRE.Cost.Machine.clockRun (c₀ : Cfg) (k Θ : ℕ) : ℕ → ℕ → Data

The result of the clocked loop from the n-th configuration of the run of c₀, with step budget b, cost budget k and size guard Θ.

Equations

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

theorem MIPRE.Cost.Machine.clockBodyBound_ge (Θ k : ℕ) : 12 * Θ + 200 ≤ clockBodyBound Θ k

theorem MIPRE.Cost.Machine.clockLoop_runs (c₀ : Cfg) (k Θ : ℕ) (env : Env) (b n : ℕ) : b ≤ 3 * k + 1 → costSum c₀ n ≤ k → (step^[n] c₀).toData.size ≤ Θ → ∃ t ≤ (b + 1) * (clockBodyBound Θ k + 1), Eval (clockState (step^[n] c₀).toData (Data.ofNat (k - costSum c₀ n)) (Data.ofNat b) (Data.ofNat Θ) :: env) clockBody.loop (clockRun c₀ k Θ b n) t

The clocked loop computes clockRun.

theorem MIPRE.Cost.Machine.clockRun_of_final (c₀ : Cfg) (k Θ N : ℕ) (r : Data) (e : Env) (hN : step^[N] c₀ = { ctrl := Ctrl.ret r, env := e, kont := [] }) (hcost : costSum c₀ N ≤ k) (hΘ : ∀ (n : ℕ), (step^[n] c₀).toData.size ≤ Θ) (b n : ℕ) : n ≤ N → N ≤ n + b → clockRun c₀ k Θ b n = (Data.nil.cons Data.nil).cons r

On a run reaching a final configuration at step N within the cost budget, whose configurations are all within the guard, the clocked loop returns the flagged value.

theorem MIPRE.Cost.Machine.clockRun_of_not (c : Prog) (v : Data) (k Θ : ℕ) (hno : ¬∃ (r : Data), ∃ t ≤ k, c.Runs v r t) (b n : ℕ) : costSum { ctrl := Ctrl.ev c, env := [v], kont := [] } n ≤ k → clockRun { ctrl := Ctrl.ev c, env := [v], kont := [] } k Θ b n = Data.nil

If c does not halt on v within cost k, the clocked loop returns nil.

theorem MIPRE.Cost.Machine.clockRun_eq (c : Prog) (v : Data) (k Θ : ℕ) (hΘ : ∀ (r : Data), ∀ t ≤ k, c.Runs v r t → ∀ (n : ℕ), (step^[n] { ctrl := Ctrl.ev c, env := [v], kont := [] }).toData.size ≤ Θ) : clockRun { ctrl := Ctrl.ev c, env := [v], kont := [] } k Θ (3 * k + 1) 0 = clockedResult c v k

The clocked loop from the initial configuration, with step budget 3 k + 1, computes clockedResult c v k, provided the guard Θ bounds the configurations of any run of c on v of cost at most k.

The clocked universal program

def MIPRE.Cost.Machine.guardFun (X : ℕ) : ℕ

The size guard of the clocked simulation, as a function of X = k + esize c + v.size: Y = 9 X + 4 (two applications of tripleProg)...

Equations

• MIPRE.Cost.Machine.guardFun X = 3 * (3 * X + 1) + 1

def MIPRE.Cost.Machine.t1Fun (X : ℕ) : ℕ

...the size of Y copies of ofNat Y...

Equations

• MIPRE.Cost.Machine.t1Fun X = MIPRE.Cost.Machine.guardFun X * (2 * MIPRE.Cost.Machine.guardFun X + 1 + 1) + 1

def MIPRE.Cost.Machine.thetaFun (X : ℕ) : ℕ

...and the size of Y copies of that list: the guard Θ.

Equations

• MIPRE.Cost.Machine.thetaFun X = MIPRE.Cost.Machine.guardFun X * (MIPRE.Cost.Machine.t1Fun X + 1) + 1

theorem MIPRE.Cost.Machine.guardFun_le_thetaFun (X : ℕ) : guardFun X ≤ thetaFun X

theorem MIPRE.Cost.Machine.sigmaFun_le_thetaFun (X : ℕ) : sigmaFun X ≤ thetaFun X

The guard dominates the size bound of the configurations of a run of cost at most k.

def MIPRE.Cost.Machine.univTProg : Prog

The clocked universal program: on cons (ofNat k) (cons (encode c) v), compute X = k + esize c + v.size and the guard Θ in unary, build the initial configuration and the state of the clocked loop, and run it with step budget 3 k + 1.

Equations

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

theorem MIPRE.Cost.Machine.univTProg_wellScoped : Prog.WellScoped 1 univTProg

def MIPRE.Cost.Machine.addBound (a b : ℕ) : ℕ

Cost bound of addProg (as in addProg_runs).

Equations

• MIPRE.Cost.Machine.addBound a b = (a + 1) * (4 * a + 2 * b + 15)

theorem MIPRE.Cost.Machine.addBound_mono {a b a' b' : ℕ} (ha : a ≤ a') (hb : b ≤ b') : addBound a b ≤ addBound a' b'

def MIPRE.Cost.Machine.tripleBound (n m : ℕ) : ℕ

Cost bound of tripleProg (as in tripleProg_runs).

Equations

• MIPRE.Cost.Machine.tripleBound n m = (n + 1) * (8 * n + 2 * m + 30)

theorem MIPRE.Cost.Machine.clockBodyBound_mono_right {Θ k k' : ℕ} (h : k ≤ k') : clockBodyBound Θ k ≤ clockBodyBound Θ k'

def MIPRE.Cost.Machine.univTBoundFun (X : ℕ) : ℕ

The time bound of the clocked universal program, as a function of X = k + esize c + v.size.

Equations

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

theorem MIPRE.Cost.Machine.univTProg_runs (c : Prog) (v : Data) (k : ℕ) : ∃ t ≤ univTBoundFun (k + esize c + v.size), univTProg.Runs ((Data.ofNat k).cons ((encode c).cons v)) (clockedResult c v k) t

Polynomial packaging

noncomputable def MIPRE.Cost.Machine.stepPoly : Polynomial ℕ

stepBound as a polynomial.

Equations

• MIPRE.Cost.Machine.stepPoly = (Polynomial.X + Polynomial.C 1) * (Polynomial.X + Polynomial.C 40) + Polynomial.C 200

theorem MIPRE.Cost.Machine.stepPoly_eval (x : ℕ) : Polynomial.eval x stepPoly = stepBound x

noncomputable def MIPRE.Cost.Machine.interpBodyPoly : Polynomial ℕ

interpBodyBound as a polynomial.

Equations

• MIPRE.Cost.Machine.interpBodyPoly = MIPRE.Cost.Machine.stepPoly + Polynomial.C 3 * Polynomial.X + Polynomial.C 30

theorem MIPRE.Cost.Machine.interpBodyPoly_eval (x : ℕ) : Polynomial.eval x interpBodyPoly = interpBodyBound x

noncomputable def MIPRE.Cost.Machine.sigmaPoly : Polynomial ℕ

sigmaFun as a polynomial.

Equations

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

theorem MIPRE.Cost.Machine.sigmaPoly_eval (x : ℕ) : Polynomial.eval x sigmaPoly = sigmaFun x

noncomputable def MIPRE.Cost.Machine.univPoly : Polynomial ℕ

univBoundFun as a polynomial.

Equations

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

theorem MIPRE.Cost.Machine.univPoly_eval (x : ℕ) : Polynomial.eval x univPoly = univBoundFun x

noncomputable def MIPRE.Cost.Machine.sizePoly (p : Polynomial ℕ) : Polynomial ℕ

sizeBound of a polynomial.

Equations

• MIPRE.Cost.Machine.sizePoly p = (p + Polynomial.C 1) * (Polynomial.C 5 * p + Polynomial.C 20) + p + Polynomial.C 6

theorem MIPRE.Cost.Machine.sizePoly_eval (p : Polynomial ℕ) (x : ℕ) : Polynomial.eval x (sizePoly p) = sizeBound (Polynomial.eval x p)

noncomputable def MIPRE.Cost.Machine.addPoly (p q : Polynomial ℕ) : Polynomial ℕ

addBound of polynomials.

Equations

• MIPRE.Cost.Machine.addPoly p q = (p + Polynomial.C 1) * (Polynomial.C 4 * p + Polynomial.C 2 * q + Polynomial.C 15)

theorem MIPRE.Cost.Machine.addPoly_eval (p q : Polynomial ℕ) (x : ℕ) : Polynomial.eval x (addPoly p q) = addBound (Polynomial.eval x p) (Polynomial.eval x q)

noncomputable def MIPRE.Cost.Machine.triplePoly (p q : Polynomial ℕ) : Polynomial ℕ

tripleBound of polynomials.

Equations

• MIPRE.Cost.Machine.triplePoly p q = (p + Polynomial.C 1) * (Polynomial.C 8 * p + Polynomial.C 2 * q + Polynomial.C 30)

theorem MIPRE.Cost.Machine.triplePoly_eval (p q : Polynomial ℕ) (x : ℕ) : Polynomial.eval x (triplePoly p q) = tripleBound (Polynomial.eval x p) (Polynomial.eval x q)

noncomputable def MIPRE.Cost.Machine.repPoly (p q r : Polynomial ℕ) : Polynomial ℕ

repBound of polynomials.

Equations

• MIPRE.Cost.Machine.repPoly p q r = (p + Polynomial.C 1) * (Polynomial.C 4 * p + Polynomial.C 4 * q + Polynomial.C 2 * r + Polynomial.C 30) + p * (p + Polynomial.C 1) * (q + Polynomial.C 1)

theorem MIPRE.Cost.Machine.repPoly_eval (p q r : Polynomial ℕ) (x : ℕ) : Polynomial.eval x (repPoly p q r) = repBound (Polynomial.eval x p) (Polynomial.eval x q) (Polynomial.eval x r)

noncomputable def MIPRE.Cost.Machine.subPoly (p q : Polynomial ℕ) : Polynomial ℕ

subBound of polynomials.

Equations

• MIPRE.Cost.Machine.subPoly p q = (p + Polynomial.C 1) * (Polynomial.C 2 * p + Polynomial.C 2 * q + Polynomial.C 14)

theorem MIPRE.Cost.Machine.subPoly_eval (p q : Polynomial ℕ) (x : ℕ) : Polynomial.eval x (subPoly p q) = subBound (Polynomial.eval x p) (Polynomial.eval x q)

noncomputable def MIPRE.Cost.Machine.stepCostPoly (p : Polynomial ℕ) : Polynomial ℕ

stepCostBound of a polynomial.

Equations

• MIPRE.Cost.Machine.stepCostPoly p = (p + Polynomial.C 1) * (Polynomial.C 7 * p + Polynomial.C 32) + Polynomial.C 13 * p + Polynomial.C 50

theorem MIPRE.Cost.Machine.stepCostPoly_eval (p : Polynomial ℕ) (x : ℕ) : Polynomial.eval x (stepCostPoly p) = stepCostBound (Polynomial.eval x p)

noncomputable def MIPRE.Cost.Machine.clockBodyPoly (p q : Polynomial ℕ) : Polynomial ℕ

clockBodyBound of polynomials.

Equations

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

theorem MIPRE.Cost.Machine.clockBodyPoly_eval (p q : Polynomial ℕ) (x : ℕ) : Polynomial.eval x (clockBodyPoly p q) = clockBodyBound (Polynomial.eval x p) (Polynomial.eval x q)

noncomputable def MIPRE.Cost.Machine.guardPoly : Polynomial ℕ

guardFun, t1Fun, thetaFun as polynomials.

Equations

• MIPRE.Cost.Machine.guardPoly = Polynomial.C 3 * (Polynomial.C 3 * Polynomial.X + Polynomial.C 1) + Polynomial.C 1

theorem MIPRE.Cost.Machine.guardPoly_eval (x : ℕ) : Polynomial.eval x guardPoly = guardFun x

noncomputable def MIPRE.Cost.Machine.t1Poly : Polynomial ℕ

Equations

• MIPRE.Cost.Machine.t1Poly = MIPRE.Cost.Machine.guardPoly * (Polynomial.C 2 * MIPRE.Cost.Machine.guardPoly + Polynomial.C 1 + Polynomial.C 1) + Polynomial.C 1

theorem MIPRE.Cost.Machine.t1Poly_eval (x : ℕ) : Polynomial.eval x t1Poly = t1Fun x

noncomputable def MIPRE.Cost.Machine.thetaPoly : Polynomial ℕ

Equations

• MIPRE.Cost.Machine.thetaPoly = MIPRE.Cost.Machine.guardPoly * (MIPRE.Cost.Machine.t1Poly + Polynomial.C 1) + Polynomial.C 1

theorem MIPRE.Cost.Machine.thetaPoly_eval (x : ℕ) : Polynomial.eval x thetaPoly = thetaFun x

noncomputable def MIPRE.Cost.Machine.univTPoly : Polynomial ℕ

univTBoundFun as a polynomial.

Equations

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

theorem MIPRE.Cost.Machine.univTPoly_eval (x : ℕ) : Polynomial.eval x univTPoly = univTBoundFun x

noncomputable def MIPRE.Cost.selfUniversal : UniversalMachine

The universal machine given by the self-interpreter.

Equations

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

theorem MIPRE.Cost.exists_efficient_universal : Nonempty UniversalMachine

Existence of an efficient universal machine (blueprint lem:universal-tm).

noncomputable def MIPRE.Cost.selfClockedUniversal : ClockedUniversalMachine

The clocked universal machine given by the self-interpreter.

Equations

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

theorem MIPRE.Cost.exists_clocked_universal : Nonempty ClockedUniversalMachine

Existence of a clocked universal machine (blueprint lem:universal-tm).