Documentation

MIPRE.TM.Interp.Step

One step of the evaluation machine #

The representation of a configuration of the CEK machine on the tapes (RepOf), the dispatcher, and, for each case of Machine.step, the run of the case program from the representation of m to that of step m, charging stepCost m (StepTo), or halting silently when the budget is short.

instance MIPRE.TM.Interp.instNeZeroNatMaxPc :

The tape names are distinct #

@[simp]

theorem MIPRE.TM.Interp.C_ne_E :

@[simp]

theorem MIPRE.TM.Interp.C_ne_K :

@[simp]

theorem MIPRE.TM.Interp.C_ne_X :

@[simp]

theorem MIPRE.TM.Interp.C_ne_CNT :

@[simp]

theorem MIPRE.TM.Interp.C_ne_BUD :

@[simp]

theorem MIPRE.TM.Interp.E_ne_C :

@[simp]

theorem MIPRE.TM.Interp.E_ne_K :

@[simp]

theorem MIPRE.TM.Interp.E_ne_X :

@[simp]

theorem MIPRE.TM.Interp.E_ne_CNT :

@[simp]

theorem MIPRE.TM.Interp.E_ne_BUD :

@[simp]

theorem MIPRE.TM.Interp.K_ne_C :

@[simp]

theorem MIPRE.TM.Interp.K_ne_E :

@[simp]

theorem MIPRE.TM.Interp.K_ne_X :

@[simp]

theorem MIPRE.TM.Interp.K_ne_CNT :

@[simp]

theorem MIPRE.TM.Interp.K_ne_BUD :

@[simp]

theorem MIPRE.TM.Interp.X_ne_C :

@[simp]

theorem MIPRE.TM.Interp.X_ne_E :

@[simp]

theorem MIPRE.TM.Interp.X_ne_K :

@[simp]

theorem MIPRE.TM.Interp.X_ne_CNT :

@[simp]

theorem MIPRE.TM.Interp.X_ne_BUD :

@[simp]

theorem MIPRE.TM.Interp.CNT_ne_C :

@[simp]

theorem MIPRE.TM.Interp.CNT_ne_E :

@[simp]

theorem MIPRE.TM.Interp.CNT_ne_K :

@[simp]

theorem MIPRE.TM.Interp.CNT_ne_X :

@[simp]

theorem MIPRE.TM.Interp.CNT_ne_BUD :

@[simp]

theorem MIPRE.TM.Interp.BUD_ne_C :

@[simp]

theorem MIPRE.TM.Interp.BUD_ne_E :

@[simp]

theorem MIPRE.TM.Interp.BUD_ne_K :

@[simp]

theorem MIPRE.TM.Interp.BUD_ne_X :

@[simp]

theorem MIPRE.TM.Interp.BUD_ne_CNT :

The representation #

structure MIPRE.TM.Interp.RepOf (ds : WT → TapeSt) (m : Cost.Machine.Cfg) (r pC pK : ℕ) :

The descriptions representing the machine configuration m with budget r: the control followed by garbage g (its head at pC), the environment and the stack exactly (the stack head at pK), a scratch tape with its head inside its content, an empty counter, a unary budget.

ctrl : ∃ (g : List Sym), ds C = { l := ctrlRepr m.ctrl ++ g, p := pC }
env : ds E = { l := envRepr m.env, p := (envRepr m.env).length }
kont : ds K = { l := kontRepr m.kont, p := pK }
scratch : (ds X).p ≤ (ds X).l.length
cnt : ds CNT = { l := [], p := 0 }
bud : ds BUD = { l := List.replicate r Sym.one, p := r }

Instances For

theorem MIPRE.TM.Interp.RepOf.eq {ds : WT → TapeSt} {m : Cost.Machine.Cfg} {r pC pK : ℕ} (h : RepOf ds m r pC pK) :

∃ (g : List Sym), ds = Function.update (Function.update (Function.update (Function.update (Function.update ds C { l := ctrlRepr m.ctrl ++ g, p := pC }) E { l := envRepr m.env, p := (envRepr m.env).length }) K { l := kontRepr m.kont, p := pK }) CNT { l := [], p := 0 }) BUD { l := List.replicate r Sym.one, p := r }

The representation, as an explicit description (the scratch tape as it is).

def MIPRE.TM.Interp.sz (m : Cost.Machine.Cfg) :

The size of the representation of m.

Equations

MIPRE.TM.Interp.sz m = (MIPRE.TM.Interp.ctrlRepr m.ctrl).length + (MIPRE.TM.Interp.envRepr m.env).length + (MIPRE.TM.Interp.kontRepr m.kont).length + 1

Instances For

@[reducible, inline]

abbrev MIPRE.TM.Interp.PreTo {input : Fin 7 → List Sym} (c : Cfg input) (B : ℕ) (q : Option Ctl) (m' : Cost.Machine.Cfg) (r' pC pK xl : ℕ) :

c reaches, within B silent steps, the control q with tapes representing m' (budget r', heads of C and K at pC, pK), its scratch tape of length at most xl.

Equations

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

Instances For

@[reducible, inline]

abbrev MIPRE.TM.Interp.StepTo {input : Fin 7 → List Sym} (c : Cfg input) (B : ℕ) (m' : Cost.Machine.Cfg) (r' xl : ℕ) :

c reaches, within B silent steps, the dispatcher representing m' with budget r', its scratch tape of length at most xl.

Equations

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

Instances For

def MIPRE.TM.Interp.PreTo1 {input : Fin 7 → List Sym} (c : Cfg input) (B : ℕ) (q : Option Ctl) (m' : Cost.Machine.Cfg) (r' pC pK xl : ℕ) :

PreTo with at least one step.

Equations

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

Instances For

@[reducible, inline]

abbrev MIPRE.TM.Interp.RunTo {input : Fin 7 → List Sym} (c : Cfg input) (B : ℕ) (m' : Cost.Machine.Cfg) (r' xl : ℕ) :

StepTo with at least one step.

Equations

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

Instances For

theorem MIPRE.TM.Interp.PreTo1.mono {input : Fin 7 → List Sym} {c : Cfg input} {B B' : ℕ} {q : Option Ctl} {m' : Cost.Machine.Cfg} {r' pC pK xl xl' : ℕ} (h : PreTo1 c B q m' r' pC pK xl) (hB : B ≤ B') (hx : xl ≤ xl') :

PreTo1 c B' q m' r' pC pK xl'

The control words #

theorem MIPRE.TM.Interp.ctrlRepr_var (i : ℕ) :

ctrlRepr (Cost.Machine.Ctrl.ev (Cost.Prog.var i)) = Sym.zero :: Sym.one :: Sym.zero :: S (Cost.Data.ofNat i)

theorem MIPRE.TM.Interp.ctrlRepr_nil :

ctrlRepr (Cost.Machine.Ctrl.ev Cost.Prog.nil) = [Sym.zero , Sym.one , Sym.one , Sym.zero , Sym.zero , Sym.zero ]

theorem MIPRE.TM.Interp.ctrlRepr_cons (h t : Cost.Prog) :

ctrlRepr (Cost.Machine.Ctrl.ev (h.cons t)) = Sym.zero :: Sym.one :: Sym.one :: Sym.zero :: Sym.one :: Sym.zero :: Sym.zero :: Sym.one :: (S h.toData ++ S t.toData)

theorem MIPRE.TM.Interp.ctrlRepr_elim (i : ℕ) (n c : Cost.Prog) :

ctrlRepr (Cost.Machine.Ctrl.ev (Cost.Prog.elim i n c)) = Sym.zero :: Sym.one :: Sym.one :: Sym.zero :: Sym.one :: Sym.zero :: Sym.one :: Sym.zero :: Sym.zero :: Sym.one :: (S (Cost.Data.ofNat i) ++ Sym.one :: (S n.toData ++ S c.toData))

theorem MIPRE.TM.Interp.ctrlRepr_let (e b : Cost.Prog) :

ctrlRepr (Cost.Machine.Ctrl.ev (e.let_ b)) = Sym.zero :: Sym.one :: Sym.one :: Sym.zero :: Sym.one :: Sym.zero :: Sym.one :: Sym.zero :: Sym.one :: Sym.zero :: Sym.zero :: Sym.one :: (S e.toData ++ S b.toData)

theorem MIPRE.TM.Interp.ctrlRepr_loop (b : Cost.Prog) :

theorem MIPRE.TM.Interp.ctrlRepr_const (d : Cost.Data) :

theorem MIPRE.TM.Interp.ctrlRepr_ret (v : Cost.Data) :

ctrlRepr (Cost.Machine.Ctrl.ret v) = Sym.one :: S v

List facts #

theorem MIPRE.TM.Interp.overwrite_cons_one_add (a : Sym) (l : List Sym) (p : ℕ) (w : List Sym) :

overwrite (a :: l) (1 + p) w = a :: overwrite l p w

theorem MIPRE.TM.Interp.overwrite_append_nil' (a w : List Sym) {p : ℕ} (hp : p = a.length) :

overwrite a p w = a ++ w

theorem MIPRE.TM.Interp.kontRepr_nil_or_fr (k : List Cost.Machine.Frame) :

kontRepr k = [] ∨ ∃ (l₀ : List Sym), kontRepr k = l₀ ++ [Sym.fr ]

theorem MIPRE.TM.Interp.envRepr_nil_or_sep (env : Cost.Env) :

envRepr env = [] ∨ ∃ (l₀ : List Sym), envRepr env = l₀ ++ [Sym.sep ]

theorem MIPRE.TM.Interp.mem_envRepr_ne_fr (env : Cost.Env) (s : Sym) :

s ∈ envRepr env → some s ≠ some Sym.fr

theorem MIPRE.TM.Interp.mem_envRepr_ne_en (env : Cost.Env) (s : Sym) :

s ∈ envRepr env → s ≠ Sym.en

theorem MIPRE.TM.Interp.mem_envRepr_ne_none (env : Cost.Env) (s : Sym) :

s ∈ envRepr env → some s ≠ none

theorem MIPRE.TM.Interp.size_get_le (env : Cost.Env) (i : ℕ) :

(env.get i).size ≤ (envRepr env).length + 1

theorem MIPRE.TM.Interp.frameBody_ne_fr (f : Cost.Machine.Frame) (s : Sym) :

s ∈ frameBody f → s ≠ Sym.fr

def MIPRE.TM.Interp.tacticNorm_dsAt___ :

Lean.ParserDescr

Normalize a description after a routine.

Equations

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

Instances For

def MIPRE.TM.Interp.tacticNorm_ds_goal :

Lean.ParserDescr

Equations

MIPRE.TM.Interp.tacticNorm_ds_goal = Lean.ParserDescr.node `MIPRE.TM.Interp.tacticNorm_ds_goal 1024 (Lean.ParserDescr.nonReservedSymbol "norm_ds_goal" false)

Instances For

The dispatcher on `ev` #

theorem MIPRE.TM.Interp.evDispatch_round {input : Fin 7 → List Sym} {pc : Fin maxPc} {tgt : ProgId} (h1 : instrAt ProgId.evDispatch pc = Instr.move C true) (h2 : ↑pc + 1 < maxPc) (h2' : instrAt ProgId.evDispatch ⟨↑pc + 1, h2⟩ = Instr.move C true) (h3 : ↑pc + 2 < maxPc) (h3' : instrAt ProgId.evDispatch ⟨↑pc + 2, h3⟩ = Instr.branch C (some Sym.zero) tgt) {c : Cfg input} {ds : WT → TapeSt} (hd : Desc c (at_ ProgId.evDispatch pc) ds) :

((ds C).l[(ds C).p + 2]? = some Sym.zero → ∃ (c' : Cfg input), Reach c 3 c' [] ∧ Desc c' (at_ tgt 0) (Function.update ds C { l := (ds C).l, p := (ds C).p + 2 })) ∧ ((ds C).l[(ds C).p + 2]? ≠ some Sym.zero → ∀ (h4 : ↑pc + 2 + 1 < maxPc), ∃ (c' : Cfg input), Reach c 3 c' [] ∧ Desc c' (next_ ProgId.evDispatch ⟨↑pc + 2, h3⟩ h4) (Function.update ds C { l := (ds C).l, p := (ds C).p + 2 }))

One round of evDispatch: two moves and a branch on the bit two cells right.

def MIPRE.TM.Interp.evTarget :

Cost.Prog → ProgId

The case program of a control to evaluate, and the position of the final 0 of its tag.

Equations

Instances For

def MIPRE.TM.Interp.evHead :

Cost.Prog → ℕ

Equations

MIPRE.TM.Interp.evHead (MIPRE.Cost.Prog.var i) = 2
MIPRE.TM.Interp.evHead MIPRE.Cost.Prog.nil = 4
MIPRE.TM.Interp.evHead (h.cons t) = 6
MIPRE.TM.Interp.evHead (MIPRE.Cost.Prog.elim i n c) = 8
MIPRE.TM.Interp.evHead (e.let_ b) = 10
MIPRE.TM.Interp.evHead b.loop = 12
MIPRE.TM.Interp.evHead (MIPRE.Cost.Prog.const d) = 14

Instances For

theorem MIPRE.TM.Interp.dispatch_ev {input : Fin 7 → List Sym} {c : Cfg input} {ds : WT → TapeSt} (hd : Desc c (at_ ProgId.dispatch 0) ds) {p : Cost.Prog} {env : Cost.Env} {k : List Cost.Machine.Frame} {r : ℕ} (hr : RepOf ds { ctrl := Cost.Machine.Ctrl.ev p, env := env, kont := k } r (ctrlRepr (Cost.Machine.Ctrl.ev p)).length (kontRepr k).length) :

PreTo1 c ((ctrlRepr (Cost.Machine.Ctrl.ev p)).length + 26) (at_ (evTarget p) 0) { ctrl := Cost.Machine.Ctrl.ev p, env := env, kont := k } r (evHead p) (kontRepr k).length (ds X).l.length

From the dispatcher, a control ev p reaches its case program with the head of C on the final 0 of the tag.

The cases: `ev` #

def MIPRE.TM.Interp.caseBound (m : Cost.Machine.Cfg) (xl : ℕ) :

The bound on the steps of a case program.

Equations

MIPRE.TM.Interp.caseBound m xl = 100 * (MIPRE.TM.Interp.sz m + xl + 1)

Instances For

theorem MIPRE.TM.Interp.case_evNil {input : Fin 7 → List Sym} {c : Cfg input} {ds : WT → TapeSt} (hd : Desc c (at_ ProgId.evNil 0) ds) {env : Cost.Env} {k : List Cost.Machine.Frame} {r : ℕ} (hr : RepOf ds { ctrl := Cost.Machine.Ctrl.ev Cost.Prog.nil, env := env, kont := k } (r + 1) 4 (kontRepr k).length) :

StepTo c (caseBound { ctrl := Cost.Machine.Ctrl.ev Cost.Prog.nil, env := env, kont := k } (ds X).l.length) { ctrl := Cost.Machine.Ctrl.ret Cost.Data.nil, env := env, kont := k } r ((ds X).l.length + sz { ctrl := Cost.Machine.Ctrl.ev Cost.Prog.nil, env := env, kont := k })

theorem MIPRE.TM.Interp.case_evNil_fail {input : Fin 7 → List Sym} {c : Cfg input} {ds : WT → TapeSt} (hd : Desc c (at_ ProgId.evNil 0) ds) {env : Cost.Env} {k : List Cost.Machine.Frame} (hr : RepOf ds { ctrl := Cost.Machine.Ctrl.ev Cost.Prog.nil, env := env, kont := k } 0 4 (kontRepr k).length) :

HaltsIn c (caseBound { ctrl := Cost.Machine.Ctrl.ev Cost.Prog.nil, env := env, kont := k } (ds X).l.length)

theorem MIPRE.TM.Interp.case_evVar {input : Fin 7 → List Sym} {c : Cfg input} {ds : WT → TapeSt} (hd : Desc c (at_ ProgId.evVar 0) ds) {i : ℕ} {env : Cost.Env} {k : List Cost.Machine.Frame} {r : ℕ} (hr : RepOf ds { ctrl := Cost.Machine.Ctrl.ev (Cost.Prog.var i), env := env, kont := k } (r + ((env.get i).size + 1)) 2 (kontRepr k).length) :

StepTo c (caseBound { ctrl := Cost.Machine.Ctrl.ev (Cost.Prog.var i), env := env, kont := k } (ds X).l.length) { ctrl := Cost.Machine.Ctrl.ret (env.get i), env := env, kont := k } r ((ds X).l.length + sz { ctrl := Cost.Machine.Ctrl.ev (Cost.Prog.var i), env := env, kont := k })

theorem MIPRE.TM.Interp.case_evVar_fail {input : Fin 7 → List Sym} {c : Cfg input} {ds : WT → TapeSt} (hd : Desc c (at_ ProgId.evVar 0) ds) {i : ℕ} {env : Cost.Env} {k : List Cost.Machine.Frame} {r : ℕ} (hr : RepOf ds { ctrl := Cost.Machine.Ctrl.ev (Cost.Prog.var i), env := env, kont := k } r 2 (kontRepr k).length) (hlt : r < (env.get i).size + 1) :

HaltsIn c (caseBound { ctrl := Cost.Machine.Ctrl.ev (Cost.Prog.var i), env := env, kont := k } (ds X).l.length)

theorem MIPRE.TM.Interp.case_evConst {input : Fin 7 → List Sym} {c : Cfg input} {ds : WT → TapeSt} (hd : Desc c (at_ ProgId.evConst 0) ds) {d : Cost.Data} {env : Cost.Env} {k : List Cost.Machine.Frame} {r : ℕ} (hr : RepOf ds { ctrl := Cost.Machine.Ctrl.ev (Cost.Prog.const d), env := env, kont := k } (r + d.size) 14 (kontRepr k).length) :

StepTo c (caseBound { ctrl := Cost.Machine.Ctrl.ev (Cost.Prog.const d), env := env, kont := k } (ds X).l.length) { ctrl := Cost.Machine.Ctrl.ret d, env := env, kont := k } r ((ds X).l.length + sz { ctrl := Cost.Machine.Ctrl.ev (Cost.Prog.const d), env := env, kont := k })

theorem MIPRE.TM.Interp.case_evConst_fail {input : Fin 7 → List Sym} {c : Cfg input} {ds : WT → TapeSt} (hd : Desc c (at_ ProgId.evConst 0) ds) {d : Cost.Data} {env : Cost.Env} {k : List Cost.Machine.Frame} {r : ℕ} (hr : RepOf ds { ctrl := Cost.Machine.Ctrl.ev (Cost.Prog.const d), env := env, kont := k } r 14 (kontRepr k).length) (hlt : r < d.size) :

HaltsIn c (caseBound { ctrl := Cost.Machine.Ctrl.ev (Cost.Prog.const d), env := env, kont := k } (ds X).l.length)

theorem MIPRE.TM.Interp.case_evCons {input : Fin 7 → List Sym} {c : Cfg input} {ds : WT → TapeSt} (hd : Desc c (at_ ProgId.evCons 0) ds) {h t : Cost.Prog} {env : Cost.Env} {k : List Cost.Machine.Frame} {r : ℕ} (hr : RepOf ds { ctrl := Cost.Machine.Ctrl.ev (h.cons t), env := env, kont := k } r 6 (kontRepr k).length) :

PreTo c (caseBound { ctrl := Cost.Machine.Ctrl.ev (h.cons t), env := env, kont := k } (ds X).l.length) (at_ ProgId.evCons 15) { ctrl := Cost.Machine.Ctrl.ev h, env := env, kont := Cost.Machine.Frame.cons1 t env :: k } r (ctrlRepr (Cost.Machine.Ctrl.ev h)).length (kontRepr (Cost.Machine.Frame.cons1 t env :: k)).length ((ds X).l.length + sz { ctrl := Cost.Machine.Ctrl.ev (h.cons t), env := env, kont := k })

The common tail of evCons and evLet: after the frame is pushed, rebuild the control from the scratch tape and charge. Stated inline in each case.

Finishing a case: the charge and the jump #

theorem MIPRE.TM.Interp.PreTo.charge_jump {input : Fin 7 → List Sym} {c : Cfg input} {B : ℕ} {k : ProgId} {pc : Fin maxPc} {m' : Cost.Machine.Cfg} {r xl : ℕ} (h : PreTo c B (at_ k pc) m' (r + 1) (ctrlRepr m'.ctrl).length (kontRepr m'.kont).length xl) (hins : instrAt k pc = Instr.charge false) (hpc : ↑pc + 1 < maxPc) (hins' : instrAt k ⟨↑pc + 1, hpc⟩ = Instr.jump ProgId.dispatch) :

StepTo c (B + 3) m' r xl

theorem MIPRE.TM.Interp.PreTo.charge_fail {input : Fin 7 → List Sym} {c : Cfg input} {B : ℕ} {k : ProgId} {pc : Fin maxPc} {m' : Cost.Machine.Cfg} {pC pK xl : ℕ} (h : PreTo c B (at_ k pc) m' 0 pC pK xl) (hins : instrAt k pc = Instr.charge false) :

HaltsIn c (B + 2)

`ev elim` #

theorem MIPRE.TM.Interp.case_evElim_nil {input : Fin 7 → List Sym} {c : Cfg input} {ds : WT → TapeSt} (hd : Desc c (at_ ProgId.evElim 0) ds) {i : ℕ} {n cc : Cost.Prog} {env : Cost.Env} {k : List Cost.Machine.Frame} {r : ℕ} (hr : RepOf ds { ctrl := Cost.Machine.Ctrl.ev (Cost.Prog.elim i n cc), env := env, kont := k } r 8 (kontRepr k).length) (hv : env.get i = Cost.Data.nil) :

PreTo c (caseBound { ctrl := Cost.Machine.Ctrl.ev (Cost.Prog.elim i n cc), env := env, kont := k } (ds X).l.length) (at_ ProgId.evElimNil 6) { ctrl := Cost.Machine.Ctrl.ev n, env := env, kont := k } r (ctrlRepr (Cost.Machine.Ctrl.ev n)).length (kontRepr k).length ((ds X).l.length + sz { ctrl := Cost.Machine.Ctrl.ev (Cost.Prog.elim i n cc), env := env, kont := k })

elim when the value is nil: evaluate n.

theorem MIPRE.TM.Interp.case_evElim_cons {input : Fin 7 → List Sym} {c : Cfg input} {ds : WT → TapeSt} (hd : Desc c (at_ ProgId.evElim 0) ds) {i : ℕ} {n cc : Cost.Prog} {env : Cost.Env} {k : List Cost.Machine.Frame} {r : ℕ} (hr : RepOf ds { ctrl := Cost.Machine.Ctrl.ev (Cost.Prog.elim i n cc), env := env, kont := k } r 8 (kontRepr k).length) {a b : Cost.Data} (hv : env.get i = a.cons b) :

PreTo c (caseBound { ctrl := Cost.Machine.Ctrl.ev (Cost.Prog.elim i n cc), env := env, kont := k } (ds X).l.length) (at_ ProgId.evElimCons 15) { ctrl := Cost.Machine.Ctrl.ev cc, env := a :: b :: env, kont := k } r (ctrlRepr (Cost.Machine.Ctrl.ev cc)).length (kontRepr k).length ((ds X).l.length + sz { ctrl := Cost.Machine.Ctrl.ev (Cost.Prog.elim i n cc), env := env, kont := k })

elim when the value is a pair: push its components, evaluate cc.

`ev let` and `ev loop` #

theorem MIPRE.TM.Interp.case_evLet {input : Fin 7 → List Sym} {c : Cfg input} {ds : WT → TapeSt} (hd : Desc c (at_ ProgId.evLet 0) ds) {e b : Cost.Prog} {env : Cost.Env} {k : List Cost.Machine.Frame} {r : ℕ} (hr : RepOf ds { ctrl := Cost.Machine.Ctrl.ev (e.let_ b), env := env, kont := k } r 10 (kontRepr k).length) :

PreTo c (caseBound { ctrl := Cost.Machine.Ctrl.ev (e.let_ b), env := env, kont := k } (ds X).l.length) (at_ ProgId.evLet 15) { ctrl := Cost.Machine.Ctrl.ev e, env := env, kont := Cost.Machine.Frame.let1 b env :: k } r (ctrlRepr (Cost.Machine.Ctrl.ev e)).length (kontRepr (Cost.Machine.Frame.let1 b env :: k)).length ((ds X).l.length + sz { ctrl := Cost.Machine.Ctrl.ev (e.let_ b), env := env, kont := k })

theorem MIPRE.TM.Interp.case_evLoop {input : Fin 7 → List Sym} {c : Cfg input} {ds : WT → TapeSt} (hd : Desc c (at_ ProgId.evLoop 0) ds) {b : Cost.Prog} {env : Cost.Env} {k : List Cost.Machine.Frame} {r : ℕ} (hr : RepOf ds { ctrl := Cost.Machine.Ctrl.ev b.loop, env := env, kont := k } r 12 (kontRepr k).length) :

StepTo c (caseBound { ctrl := Cost.Machine.Ctrl.ev b.loop, env := env, kont := k } (ds X).l.length) { ctrl := Cost.Machine.Ctrl.ev b, env := env, kont := Cost.Machine.Frame.loop1 b env :: k } r ((ds X).l.length + sz { ctrl := Cost.Machine.Ctrl.ev b.loop, env := env, kont := k })

The dispatcher on `ret` #

def MIPRE.TM.Interp.retTarget :

Cost.Machine.Frame → ProgId

The case program of a return to a frame.

Equations

Instances For

theorem MIPRE.TM.Interp.frameBody_cons1 (t : Cost.Prog) (env : Cost.Env) :

frameBody (Cost.Machine.Frame.cons1 t env) = Sym.zero :: Sym.zero :: (S t.toData ++ [Sym.en ] ++ envRepr env)

theorem MIPRE.TM.Interp.frameBody_cons2 (a : Cost.Data) :

frameBody (Cost.Machine.Frame.cons2 a) = Sym.zero :: Sym.one :: S a

theorem MIPRE.TM.Interp.frameBody_let1 (b : Cost.Prog) (env : Cost.Env) :

frameBody (Cost.Machine.Frame.let1 b env) = Sym.one :: Sym.zero :: (S b.toData ++ [Sym.en ] ++ envRepr env)

theorem MIPRE.TM.Interp.frameBody_loop1 (b : Cost.Prog) (env : Cost.Env) :

frameBody (Cost.Machine.Frame.loop1 b env) = Sym.one :: Sym.one :: (S b.toData ++ [Sym.en ] ++ envRepr env)

theorem MIPRE.TM.Interp.kontRepr_cons' (f : Cost.Machine.Frame) (k : List Cost.Machine.Frame) :

kontRepr (f :: k) = kontRepr k ++ frameBody f ++ [Sym.fr ]

theorem MIPRE.TM.Interp.getElem?_append_right' (l₁ l₂ : List Sym) {i j : ℕ} (h : i = l₁.length + j) :

(l₁ ++ l₂)[i]? = l₂[j]?

theorem MIPRE.TM.Interp.read_tag (k : List Cost.Machine.Frame) (f : Cost.Machine.Frame) (j : ℕ) (hj : j < 2) :

(kontRepr k ++ frameBody f ++ [Sym.fr ])[(kontRepr k).length + j]? = (frameTag f)[j]?

The two tag bits of a frame, read off the stack.

theorem MIPRE.TM.Interp.read_tag0 (k : List Cost.Machine.Frame) (f : Cost.Machine.Frame) :

(kontRepr k ++ frameBody f ++ [Sym.fr ])[(kontRepr k).length]? = (frameTag f)[0]?

theorem MIPRE.TM.Interp.read_tag1 (k : List Cost.Machine.Frame) (f : Cost.Machine.Frame) :

(kontRepr k ++ frameBody f ++ [Sym.fr ])[(kontRepr k).length + 1]? = (frameTag f)[1]?

theorem MIPRE.TM.Interp.read_end (k : List Cost.Machine.Frame) (f : Cost.Machine.Frame) :

(kontRepr k ++ frameBody f ++ [Sym.fr ])[(kontRepr k).length + (frameBody f).length]? = some Sym.fr

theorem MIPRE.TM.Interp.dispatch_ret {input : Fin 7 → List Sym} {c : Cfg input} {ds : WT → TapeSt} (hd : Desc c (at_ ProgId.dispatch 0) ds) {v : Cost.Data} {env : Cost.Env} {f : Cost.Machine.Frame} {k : List Cost.Machine.Frame} {r : ℕ} (hr : RepOf ds { ctrl := Cost.Machine.Ctrl.ret v, env := env, kont := f :: k } r (ctrlRepr (Cost.Machine.Ctrl.ret v)).length (kontRepr (f :: k)).length) :

PreTo1 c (v.size + (frameBody f).length + 20) (at_ (retTarget f) 0) { ctrl := Cost.Machine.Ctrl.ret v, env := env, kont := f :: k } r 1 ((kontRepr k).length + 1) (ds X).l.length

From the dispatcher, a return to a frame reaches its case program with the head of C on the value and the head of K on the second tag bit.

Popping the innermost environment entry #

theorem MIPRE.TM.Interp.D_popEnv {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {ds : WT → TapeSt} (hins : instrAt k pc = Instr.popBack Sym.sep E) (hpc : ↑pc + 1 < maxPc) (hd : Desc c (at_ k pc) ds) {env' : Cost.Env} (hE : ds E = { l := envRepr env', p := (envRepr env').length }) :

∃ n ≤ (envRepr env').length + 3, ∃ (c' : Cfg input), Reach c n c' [] ∧ Desc c' (next_ k pc hpc) (Function.update ds E { l := envRepr (List.tail env'), p := (envRepr (List.tail env')).length })

theorem MIPRE.TM.Interp.drop_env_ne_fr (env : Cost.Env) (n : ℕ) (s : Sym) :

s ∈ List.drop n (envRepr env) → s ≠ Sym.fr

The cases: `ret` #

theorem MIPRE.TM.Interp.case_retCons1 {input : Fin 7 → List Sym} {c : Cfg input} {ds : WT → TapeSt} (hd : Desc c (at_ ProgId.retCons1 0) ds) {v : Cost.Data} {t : Cost.Prog} {env env' : Cost.Env} {k : List Cost.Machine.Frame} {r : ℕ} (hr : RepOf ds { ctrl := Cost.Machine.Ctrl.ret v, env := env, kont := Cost.Machine.Frame.cons1 t env' :: k } r 1 ((kontRepr k).length + 1)) :

StepTo c (caseBound { ctrl := Cost.Machine.Ctrl.ret v, env := env, kont := Cost.Machine.Frame.cons1 t env' :: k } (ds X).l.length) { ctrl := Cost.Machine.Ctrl.ev t, env := env', kont := Cost.Machine.Frame.cons2 v :: k } r ((ds X).l.length + sz { ctrl := Cost.Machine.Ctrl.ret v, env := env, kont := Cost.Machine.Frame.cons1 t env' :: k })

theorem MIPRE.TM.Interp.case_retCons2 {input : Fin 7 → List Sym} {c : Cfg input} {ds : WT → TapeSt} (hd : Desc c (at_ ProgId.retCons2 0) ds) {v a : Cost.Data} {env : Cost.Env} {k : List Cost.Machine.Frame} {r : ℕ} (hr : RepOf ds { ctrl := Cost.Machine.Ctrl.ret v, env := env, kont := Cost.Machine.Frame.cons2 a :: k } r 1 ((kontRepr k).length + 1)) :

StepTo c (caseBound { ctrl := Cost.Machine.Ctrl.ret v, env := env, kont := Cost.Machine.Frame.cons2 a :: k } (ds X).l.length) { ctrl := Cost.Machine.Ctrl.ret (a.cons v), env := env, kont := k } r ((ds X).l.length + sz { ctrl := Cost.Machine.Ctrl.ret v, env := env, kont := Cost.Machine.Frame.cons2 a :: k })

theorem MIPRE.TM.Interp.case_retLet1 {input : Fin 7 → List Sym} {c : Cfg input} {ds : WT → TapeSt} (hd : Desc c (at_ ProgId.retLet1 0) ds) {v : Cost.Data} {b : Cost.Prog} {env env' : Cost.Env} {k : List Cost.Machine.Frame} {r : ℕ} (hr : RepOf ds { ctrl := Cost.Machine.Ctrl.ret v, env := env, kont := Cost.Machine.Frame.let1 b env' :: k } r 1 ((kontRepr k).length + 1)) :

StepTo c (caseBound { ctrl := Cost.Machine.Ctrl.ret v, env := env, kont := Cost.Machine.Frame.let1 b env' :: k } (ds X).l.length) { ctrl := Cost.Machine.Ctrl.ev b, env := v :: env', kont := k } r ((ds X).l.length + sz { ctrl := Cost.Machine.Ctrl.ret v, env := env, kont := Cost.Machine.Frame.let1 b env' :: k })

`ret` to a `loop1` frame #

theorem MIPRE.TM.Interp.case_retLoopNil {input : Fin 7 → List Sym} {c : Cfg input} {ds : WT → TapeSt} (hd : Desc c (at_ ProgId.retLoop1 0) ds) {b : Cost.Prog} {env env' : Cost.Env} {k : List Cost.Machine.Frame} {r : ℕ} (hr : RepOf ds { ctrl := Cost.Machine.Ctrl.ret Cost.Data.nil, env := env, kont := Cost.Machine.Frame.loop1 b env' :: k } r 1 ((kontRepr k).length + 1)) :

PreTo c (caseBound { ctrl := Cost.Machine.Ctrl.ret Cost.Data.nil, env := env, kont := Cost.Machine.Frame.loop1 b env' :: k } (ds X).l.length) (at_ ProgId.retLoopNil 11) { ctrl := Cost.Machine.Ctrl.ret Cost.Data.nil, env := env', kont := k } r (ctrlRepr (Cost.Machine.Ctrl.ret Cost.Data.nil)).length (kontRepr k).length ((ds X).l.length + sz { ctrl := Cost.Machine.Ctrl.ret Cost.Data.nil, env := env, kont := Cost.Machine.Frame.loop1 b env' :: k })

theorem MIPRE.TM.Interp.case_retLoopStop {input : Fin 7 → List Sym} {c : Cfg input} {ds : WT → TapeSt} (hd : Desc c (at_ ProgId.retLoop1 0) ds) {r' : Cost.Data} {b : Cost.Prog} {env env' : Cost.Env} {k : List Cost.Machine.Frame} {r : ℕ} (hr : RepOf ds { ctrl := Cost.Machine.Ctrl.ret (Cost.Data.nil.cons r'), env := env, kont := Cost.Machine.Frame.loop1 b env' :: k } r 1 ((kontRepr k).length + 1)) :

PreTo c (caseBound { ctrl := Cost.Machine.Ctrl.ret (Cost.Data.nil.cons r'), env := env, kont := Cost.Machine.Frame.loop1 b env' :: k } (ds X).l.length) (at_ ProgId.retLoopStop 15) { ctrl := Cost.Machine.Ctrl.ret r', env := env', kont := k } r (ctrlRepr (Cost.Machine.Ctrl.ret r')).length (kontRepr k).length ((ds X).l.length + sz { ctrl := Cost.Machine.Ctrl.ret (Cost.Data.nil.cons r'), env := env, kont := Cost.Machine.Frame.loop1 b env' :: k })

theorem MIPRE.TM.Interp.case_retLoopCont {input : Fin 7 → List Sym} {c : Cfg input} {ds : WT → TapeSt} (hd : Desc c (at_ ProgId.retLoop1 0) ds) {y z v' : Cost.Data} {b : Cost.Prog} {env env' : Cost.Env} {k : List Cost.Machine.Frame} {r : ℕ} (hr : RepOf ds { ctrl := Cost.Machine.Ctrl.ret ((y.cons z).cons v'), env := env, kont := Cost.Machine.Frame.loop1 b env' :: k } r 1 ((kontRepr k).length + 1)) :

PreTo c (caseBound { ctrl := Cost.Machine.Ctrl.ret ((y.cons z).cons v'), env := env, kont := Cost.Machine.Frame.loop1 b env' :: k } (ds X).l.length) (at_ ProgId.retLoopCont 29) { ctrl := Cost.Machine.Ctrl.ev b, env := v' :: List.tail env', kont := Cost.Machine.Frame.loop1 b (v' :: List.tail env') :: k } r (ctrlRepr (Cost.Machine.Ctrl.ev b)).length (kontRepr (Cost.Machine.Frame.loop1 b (v' :: List.tail env') :: k)).length ((ds X).l.length + sz { ctrl := Cost.Machine.Ctrl.ret ((y.cons z).cons v'), env := env, kont := Cost.Machine.Frame.loop1 b env' :: k })

The final check #

def MIPRE.TM.Interp.CDesc {input : Fin 7 → List Sym} (c : Cfg input) (q : Option Ctl) (s : TapeSt) :

The control and the tape C alone (the stack head may sit before the tape).

Equations

MIPRE.TM.Interp.CDesc c q s = (c.state = q ∧ MIPRE.TM.Interp.TapeIs (c.workTapes MIPRE.TM.Interp.C) (c.workTapePos MIPRE.TM.Interp.C) s)

Instances For

theorem MIPRE.TM.Interp.F_move_right {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {l : List Sym} {p : ℕ} (hins : instrAt k pc = Instr.move C true) (hpc : ↑pc + 1 < maxPc) (h : CDesc c (at_ k pc) { l := l, p := p }) :

∃ (c' : Cfg input), Reach c 1 c' [] ∧ CDesc c' (next_ k pc hpc) { l := l, p := p + 1 }

theorem MIPRE.TM.Interp.F_branch_taken {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {l : List Sym} {p : ℕ} {s : Option Sym} {target : ProgId} (hins : instrAt k pc = Instr.branch C s target) (h : CDesc c (at_ k pc) { l := l, p := p }) (hs : l[p]? = s) :

∃ (c' : Cfg input), Reach c 1 c' [] ∧ CDesc c' (at_ target ⟨0, F_branch_taken._proof_1 ⟩) { l := l, p := p }

theorem MIPRE.TM.Interp.F_branch_not {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {l : List Sym} {p : ℕ} {s : Option Sym} {target : ProgId} (hins : instrAt k pc = Instr.branch C s target) (hpc : ↑pc + 1 < maxPc) (h : CDesc c (at_ k pc) { l := l, p := p }) (hs : l[p]? ≠ s) :

∃ (c' : Cfg input), Reach c 1 c' [] ∧ CDesc c' (next_ k pc hpc) { l := l, p := p }

theorem MIPRE.TM.Interp.F_emit {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {l : List Sym} {p : ℕ} {s : Sym} (hins : instrAt k pc = Instr.emit s) (hpc : ↑pc + 1 < maxPc) (h : CDesc c (at_ k pc) { l := l, p := p }) :

∃ (c' : Cfg input), Reach c 1 c' [s] ∧ CDesc c' (next_ k pc hpc) { l := l, p := p }

theorem MIPRE.TM.Interp.F_halt {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {s : TapeSt} (hins : instrAt k pc = Instr.halt) (h : CDesc c (at_ k pc) s) :

∃ (c' : Cfg input), Reach c 1 c' [] ∧ c'.state = none

def MIPRE.TM.Interp.AcceptsFrom {input : Fin 7 → List Sym} (c : Cfg input) (n : ℕ) :

U accepts from c within n silent steps followed by the output 1.

Equations

MIPRE.TM.Interp.AcceptsFrom c n = ∃ (c' : MIPRE.TM.Interp.Cfg input), MIPRE.TM.Interp.Reach c n c' [MIPRE.TM.Interp.Sym.one ] ∧ c'.state = none

Instances For

theorem MIPRE.TM.Interp.final_run {input : Fin 7 → List Sym} {c : Cfg input} {ds : WT → TapeSt} (hd : Desc c (at_ ProgId.dispatch 0) ds) {v : Cost.Data} {env : Cost.Env} {r : ℕ} (hr : RepOf ds { ctrl := Cost.Machine.Ctrl.ret v, env := env, kont := [] } r (ctrlRepr (Cost.Machine.Ctrl.ret v)).length (kontRepr []).length) :

(v = Cost.Data.ofBool true → ∃ n ≤ v.size + 16, AcceptsFrom c n) ∧ (v ≠ Cost.Data.ofBool true → HaltsIn c (v.size + 16))

The final check on ret v with an empty stack: accept iff v = encode true.

The step #

def MIPRE.TM.Interp.stepBound (m : Cost.Machine.Cfg) (xl : ℕ) :

The bound on the steps of U simulating one step of the machine from a representation with a scratch tape of length xl.

Equations

MIPRE.TM.Interp.stepBound m xl = MIPRE.TM.Interp.caseBound m xl + MIPRE.TM.Interp.sz m + 30

Instances For

theorem MIPRE.TM.Interp.PreTo.after_dispatch {input : Fin 7 → List Sym} {c c₁ : Cfg input} {n₁ B₁ : ℕ} (hr₁ : Reach c n₁ c₁ []) (h1 : 1 ≤ n₁) (hn₁ : n₁ ≤ B₁) {B : ℕ} {q : Option Ctl} {m' : Cost.Machine.Cfg} {r pC pK xl : ℕ} (h : PreTo c₁ B q m' r pC pK xl) :

PreTo1 c (B₁ + B) q m' r pC pK xl

theorem MIPRE.TM.Interp.step_run {input : Fin 7 → List Sym} {c : Cfg input} {ds : WT → TapeSt} (hd : Desc c (at_ ProgId.dispatch 0) ds) {m : Cost.Machine.Cfg} {r : ℕ} (hr : RepOf ds m r (ctrlRepr m.ctrl).length (kontRepr m.kont).length) (hnf : ∀ (v : Cost.Data), m.ctrl = Cost.Machine.Ctrl.ret v → m.kont ≠ []) (hcost : Cost.Machine.stepCost m ≤ r) :

RunTo c (stepBound m (ds X).l.length) (Cost.Machine.step m) (r - Cost.Machine.stepCost m) ((ds X).l.length + sz m)

One step of the machine, when the budget covers its cost: from the dispatcher representing m, U reaches the dispatcher representing step m with the cost charged.

theorem MIPRE.TM.Interp.step_fail {input : Fin 7 → List Sym} {c : Cfg input} {ds : WT → TapeSt} (hd : Desc c (at_ ProgId.dispatch 0) ds) {m : Cost.Machine.Cfg} {r : ℕ} (hr : RepOf ds m r (ctrlRepr m.ctrl).length (kontRepr m.kont).length) (hnf : ∀ (v : Cost.Data), m.ctrl = Cost.Machine.Ctrl.ret v → m.kont ≠ []) (hcost : r < Cost.Machine.stepCost m) :

HaltsIn c (stepBound m (ds X).l.length)

One step of the machine, when the budget is short: U halts silently.