The self-interpreter, I: the step function as a program

Programs of the ambient model implementing the step function of the evaluation machine on data (Machine.stepData, Cost/MachineData.lean): stepEvProg for "evaluate" controls, stepRetProg for "return" controls, and stepProg combining them. Each is proved to compute stepData on encoded configurations, at a cost quadratic in the size of the configuration (the only non-constant work is the walk getListProg along the environment, which copies the remaining environment at each of its steps).

Conventions: every sub-program is closed and receives its input, a tuple built with cons, at variable 0; tuples are taken apart with elim (free), and the pieces are read back with var (paid by size). Tag dispatch on a unary numeral is a chain of elims; the case programs are called through callVar on a packaged tuple whose index grows by two per level of the chain.

def MIPRE.Cost.Machine.tacticSize_omega : Lean.ParserDescr

Discharge a linear inequality between costs and sizes, after expanding the sizes of constructors and of encoded configurations.

Equations

• MIPRE.Cost.Machine.tacticSize_omega = Lean.ParserDescr.node `MIPRE.Cost.Machine.tacticSize_omega 1024 (Lean.ParserDescr.nonReservedSymbol "size_omega" false)

Projections at an arbitrary index

def MIPRE.Cost.Machine.projLeft (i : ℕ) : Prog

left of the value of variable i.

Equations

• MIPRE.Cost.Machine.projLeft i = MIPRE.Cost.Prog.elim i MIPRE.Cost.Prog.nil (MIPRE.Cost.Prog.var 0)

def MIPRE.Cost.Machine.projRight (i : ℕ) : Prog

right of the value of variable i.

Equations

• MIPRE.Cost.Machine.projRight i = MIPRE.Cost.Prog.elim i MIPRE.Cost.Prog.nil (MIPRE.Cost.Prog.var 1)

theorem MIPRE.Cost.Machine.projLeft_runs {E : Env} {i : ℕ} {d : Data} (h : E.get i = d) : ∃ s ≤ d.size + 2, Eval E (projLeft i) d.left s

theorem MIPRE.Cost.Machine.projRight_runs {E : Env} {i : ℕ} {d : Data} (h : E.get i = d) : ∃ s ≤ d.size + 2, Eval E (projRight i) d.right s

theorem MIPRE.Cost.Machine.size_left_le (d : Data) : d.left.size ≤ d.size

theorem MIPRE.Cost.Machine.size_right_le (d : Data) : d.right.size ≤ d.size

theorem MIPRE.Cost.Machine.size_getList_le (env : Data) (n : ℕ) : (env.getList n).size ≤ env.size

The environment walk

def MIPRE.Cost.Machine.getListBody : Prog

Body of getListProg: on the state cons env idx, stop with left env if idx is exhausted, else continue with cons (right env) idx'.

Equations

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

def MIPRE.Cost.Machine.getListProg : Prog

getListProg on cons env idx computes getList env (unaryToNat idx).

Equations

• MIPRE.Cost.Machine.getListProg = MIPRE.Cost.Machine.getListBody.loop

theorem MIPRE.Cost.Machine.getListBody_wellScoped : Prog.WellScoped 1 getListBody

theorem MIPRE.Cost.Machine.getListProg_wellScoped : Prog.WellScoped 1 getListProg

theorem MIPRE.Cost.Machine.getListProg_runs (idx env : Data) (rest : Env) : ∃ t ≤ (idx.size + 1) * (env.size + idx.size + 12), Eval (env.cons idx :: rest) getListProg (env.getList idx.unaryToNat) t

The "evaluate" cases

def MIPRE.Cost.Machine.evVar : Prog

Cases of stepEvProg; input cons body (cons env kont). After the two elims the environment is [env, kont, body, cons env kont, input].

Equations

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

def MIPRE.Cost.Machine.evNil : Prog

Equations

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

def MIPRE.Cost.Machine.evCons : Prog

Equations

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

def MIPRE.Cost.Machine.evElim : Prog

Equations

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

def MIPRE.Cost.Machine.evLet : Prog

Equations

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

def MIPRE.Cost.Machine.evLoop : Prog

Equations

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

def MIPRE.Cost.Machine.evConst : Prog

Equations

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

theorem MIPRE.Cost.Machine.evVar_wellScoped : Prog.WellScoped 1 evVar

theorem MIPRE.Cost.Machine.evNil_wellScoped : Prog.WellScoped 1 evNil

theorem MIPRE.Cost.Machine.evCons_wellScoped : Prog.WellScoped 1 evCons

theorem MIPRE.Cost.Machine.evLet_wellScoped : Prog.WellScoped 1 evLet

theorem MIPRE.Cost.Machine.evLoop_wellScoped : Prog.WellScoped 1 evLoop

theorem MIPRE.Cost.Machine.evConst_wellScoped : Prog.WellScoped 1 evConst

theorem MIPRE.Cost.Machine.evElim_wellScoped : Prog.WellScoped 1 evElim

theorem MIPRE.Cost.Machine.evVar_runs (body env kont : Data) : ∃ s ≤ (body.size + 1) * (env.size + body.size + 12) + 4 * env.size + 3 * body.size + 2 * kont.size + 20, Eval [body.cons (env.cons kont)] evVar ((retD (env.getList body.unaryToNat)).cons (env.cons kont)) s

theorem MIPRE.Cost.Machine.evNil_runs (body env kont : Data) : ∃ s ≤ env.size + kont.size + 12, Eval [body.cons (env.cons kont)] evNil ((retD Data.nil).cons (env.cons kont)) s

theorem MIPRE.Cost.Machine.evCons_runs (h t env kont : Data) : ∃ s ≤ h.size + t.size + 2 * env.size + kont.size + 20, Eval [(h.cons t).cons (env.cons kont)] evCons ((evD h).cons (env.cons (((Data.ofNat 0).cons (t.cons env)).cons kont))) s

theorem MIPRE.Cost.Machine.evLet_runs (e b env kont : Data) : ∃ s ≤ e.size + b.size + 2 * env.size + kont.size + 24, Eval [(e.cons b).cons (env.cons kont)] evLet ((evD e).cons (env.cons (((Data.ofNat 2).cons (b.cons env)).cons kont))) s

theorem MIPRE.Cost.Machine.evLoop_runs (b env kont : Data) : ∃ s ≤ 2 * b.size + 2 * env.size + kont.size + 26, Eval [b.cons (env.cons kont)] evLoop ((evD b).cons (env.cons (((Data.ofNat 3).cons (b.cons env)).cons kont))) s

theorem MIPRE.Cost.Machine.evConst_runs (d env kont : Data) : ∃ s ≤ d.size + env.size + kont.size + 12, Eval [d.cons (env.cons kont)] evConst ((retD d).cons (env.cons kont)) s

theorem MIPRE.Cost.Machine.evElim_runs (i n c env kont : Data) : ∃ s ≤ (i.size + 1) * (env.size + i.size + 12) + 5 * env.size + 3 * i.size + n.size + c.size + 2 * kont.size + 40, Eval [(i.cons (n.cons c)).cons (env.cons kont)] evElim (if env.getList i.unaryToNat = Data.nil then (evD n).cons (env.cons kont) else (evD c).cons (((env.getList i.unaryToNat).left.cons ((env.getList i.unaryToNat).right.cons env)).cons kont)) s

Tag dispatch

def MIPRE.Cost.Machine.dispatch : List Prog → ℕ → ℕ → Prog

dispatch cs i idx: case analysis on the unary numeral at variable i, calling the k-th program of cs on the tuple at variable idx + 2 k (each level of the chain binds two more variables).

Equations

• MIPRE.Cost.Machine.dispatch [] x✝¹ x✝ = MIPRE.Cost.Prog.nil
• MIPRE.Cost.Machine.dispatch [c] x✝¹ x✝ = MIPRE.Cost.Prog.callVar x✝ c
• MIPRE.Cost.Machine.dispatch (c :: c' :: cs) x✝¹ x✝ = MIPRE.Cost.Prog.elim x✝¹ (MIPRE.Cost.Prog.callVar x✝ c) (MIPRE.Cost.Machine.dispatch (c' :: cs) 1 (x✝ + 2))

theorem MIPRE.Cost.Machine.dispatch_wellScoped (cs : List Prog) (i idx n : ℕ) : i < n → idx < n → (∀ c ∈ cs, Prog.WellScoped 1 c) → Prog.WellScoped n (dispatch cs i idx)

theorem MIPRE.Cost.Machine.dispatch_runs (cs : List Prog) (k i idx : ℕ) (E : Env) (pk r : Data) (t : ℕ) : k < cs.length → (∀ c ∈ cs, Prog.WellScoped 1 c) → E.get i = Data.ofNat k → E.get idx = pk → Eval [pk] (cs.getD k Prog.nil) r t → ∃ s ≤ t + pk.size + k + 3, Eval E (dispatch cs i idx) r s

The "evaluate" step

def MIPRE.Cost.Machine.evCases : List Prog

The case programs of stepEvProg, indexed by the tag of the program.

Equations

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

theorem MIPRE.Cost.Machine.evCases_wellScoped (c : Prog) : c ∈ evCases → Prog.WellScoped 1 c

def MIPRE.Cost.Machine.stepEvProg : Prog

The step on "evaluate p"; input cons (toData p) (cons env kont).

Equations

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

theorem MIPRE.Cost.Machine.stepEvProg_wellScoped : Prog.WellScoped 1 stepEvProg

def MIPRE.Cost.Machine.dispEnv (k : ℕ) (body env kont : Data) : Env

The environment in which the dispatch of stepEvProg runs, for a program with tag k and body body.

Equations

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

theorem MIPRE.Cost.Machine.stepEvProg_prefix (k : ℕ) (body env kont r : Data) {s : ℕ} (hd : Eval (dispEnv k body env kont) (dispatch evCases 0 1) r s) : ∃ c ≤ s + body.size + env.size + kont.size + (Data.ofNat k).size + 12, Eval [((Data.ofNat k).cons body).cons (env.cons kont)] stepEvProg r c

The prefix of stepEvProg up to the dispatch.

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

Bound of one "evaluate" step in terms of S = esize p + env.size + kont.size.

Equations

• MIPRE.Cost.Machine.stepEvBound S = (S + 1) * (S + 30) + 100

theorem MIPRE.Cost.Machine.stepEvProg_runs (p : Prog) (env kont : Data) : ∃ s ≤ stepEvBound (esize p + env.size + kont.size), stepEvProg.Runs (p.toData.cons (env.cons kont)) (stepEv p.toData env kont) s

The "return" cases

def MIPRE.Cost.Machine.retCons1 : Prog

Cases of stepRetProg; input cons v (cons env (cons fb k)) with fb the payload of the top frame. After the three elims the environment is [fb, k, env, cons fb k, v, cons env (cons fb k), input].

Equations

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

def MIPRE.Cost.Machine.retCons2 : Prog

Equations

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

def MIPRE.Cost.Machine.retLet1 : Prog

Equations

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

def MIPRE.Cost.Machine.retLoop1 : Prog

Equations

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

theorem MIPRE.Cost.Machine.retCons1_wellScoped : Prog.WellScoped 1 retCons1

theorem MIPRE.Cost.Machine.retCons2_wellScoped : Prog.WellScoped 1 retCons2

theorem MIPRE.Cost.Machine.retLet1_wellScoped : Prog.WellScoped 1 retLet1

theorem MIPRE.Cost.Machine.retLoop1_wellScoped : Prog.WellScoped 1 retLoop1

theorem MIPRE.Cost.Machine.retCons1_runs (t' env' v env k : Data) : ∃ s ≤ t'.size + env'.size + v.size + k.size + 20, Eval [v.cons (env.cons ((t'.cons env').cons k))] retCons1 ((evD t').cons (env'.cons (((Data.ofNat 1).cons v).cons k))) s

theorem MIPRE.Cost.Machine.retCons2_runs (a v env k : Data) : ∃ s ≤ a.size + v.size + env.size + k.size + 16, Eval [v.cons (env.cons (a.cons k))] retCons2 ((retD (a.cons v)).cons (env.cons k)) s

theorem MIPRE.Cost.Machine.retLet1_runs (b env' v env k : Data) : ∃ s ≤ b.size + v.size + env'.size + k.size + 16, Eval [v.cons (env.cons ((b.cons env').cons k))] retLet1 ((evD b).cons ((v.cons env').cons k)) s

theorem MIPRE.Cost.Machine.retLoop1_runs_nil (b env' env k : Data) : ∃ s ≤ env'.size + k.size + 16, Eval [Data.nil.cons (env.cons ((b.cons env').cons k))] retLoop1 ((retD Data.nil).cons (env'.cons k)) s

theorem MIPRE.Cost.Machine.retLoop1_runs_stop (b env' c env k : Data) : ∃ s ≤ c.size + env'.size + k.size + 18, Eval [(Data.nil.cons c).cons (env.cons ((b.cons env').cons k))] retLoop1 ((retD c).cons (env'.cons k)) s

theorem MIPRE.Cost.Machine.retLoop1_runs_step (b env' a₁ a₂ c env k : Data) : ∃ s ≤ 2 * b.size + 2 * c.size + 2 * env'.size + k.size + 40, Eval [((a₁.cons a₂).cons c).cons (env.cons ((b.cons env').cons k))] retLoop1 ((evD b).cons ((c.cons env'.right).cons (((Data.ofNat 3).cons (b.cons (c.cons env'.right))).cons k))) s

The "return" step

def MIPRE.Cost.Machine.retCases : List Prog

The case programs of stepRetProg, indexed by the tag of the top frame.

Equations

• MIPRE.Cost.Machine.retCases = [MIPRE.Cost.Machine.retCons1, MIPRE.Cost.Machine.retCons2, MIPRE.Cost.Machine.retLet1, MIPRE.Cost.Machine.retLoop1]

theorem MIPRE.Cost.Machine.retCases_wellScoped (c : Prog) : c ∈ retCases → Prog.WellScoped 1 c

def MIPRE.Cost.Machine.stepRetProg : Prog

The step on "return v"; input cons v (cons env kont).

Equations

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

theorem MIPRE.Cost.Machine.stepRetProg_wellScoped : Prog.WellScoped 1 stepRetProg

theorem MIPRE.Cost.Machine.stepRetProg_runs_nil (v env : Data) : ∃ s ≤ v.size + env.size + 12, stepRetProg.Runs (v.cons (env.cons Data.nil)) (stepRet v env Data.nil) s

def MIPRE.Cost.Machine.retDispEnv (ftag : ℕ) (fb v env k : Data) : Env

The environment in which the dispatch of stepRetProg runs, for a top frame with tag ftag and payload fb.

Equations

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

theorem MIPRE.Cost.Machine.stepRetProg_prefix (ftag : ℕ) (fb v env k r : Data) {s : ℕ} (hd : Eval (retDispEnv ftag fb v env k) (dispatch retCases 0 1) r s) : ∃ c ≤ s + v.size + env.size + fb.size + k.size + (Data.ofNat ftag).size + 16, Eval [v.cons (env.cons (((Data.ofNat ftag).cons fb).cons k))] stepRetProg r c

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

Bound of one "return" step in terms of S = v.size + env.size + kont.size.

Equations

• MIPRE.Cost.Machine.stepRetBound S = 8 * S + 120

theorem MIPRE.Cost.Machine.stepRetProg_runs_cons (v env : Data) (f : Frame) (k : Data) : ∃ s ≤ stepRetBound (v.size + env.size + f.toData.size + k.size), stepRetProg.Runs (v.cons (env.cons (f.toData.cons k))) (stepRet v env (f.toData.cons k)) s

The step

def MIPRE.Cost.Machine.stepProg : Prog

The step function as a program: on the encoding of a configuration, the encoding of the next configuration.

Equations

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

theorem MIPRE.Cost.Machine.stepProg_wellScoped : Prog.WellScoped 1 stepProg

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

Bound of one step of the interpreter in terms of the size of the configuration.

Equations

• MIPRE.Cost.Machine.stepBound S = (S + 1) * (S + 40) + 200

theorem MIPRE.Cost.Machine.le_stepBound_of_le {c S T : ℕ} (hc : c ≤ 41 * S + 240) (hS : S ≤ T) : c ≤ stepBound T

theorem MIPRE.Cost.Machine.le_stepBound_of_quad {c S T : ℕ} (hc : c ≤ (S + 1) * (S + 30) + 100 + 3 * S + 60) (hS : S + 4 ≤ T) : c ≤ stepBound T

theorem MIPRE.Cost.Machine.stepProg_runs (c : Cfg) : ∃ s ≤ stepBound c.toData.size, stepProg.Runs c.toData (step c).toData s

stepProg computes the step of the machine on encoded configurations, at a cost quadratic in the size of the configuration.