Tape descriptions

A work tape is described by the list it holds from cell 0 (blank elsewhere) and its head position; a configuration by its control and the six descriptions (Desc). Every routine becomes a transformation of descriptions (D_write, D_copyTree, …), so that the correctness of a step of the evaluation machine is a chain of such transformations followed by list algebra (overwrite).

One tape

structure MIPRE.TM.Interp.TapeSt : Type

A tape holding exactly l from cell 0, its head at cell p.

• l : List Sym
• p : ℕ

theorem MIPRE.TM.Interp.TapeSt.ext {x y : TapeSt} (l : x.l = y.l) (p : x.p = y.p) : x = y

theorem MIPRE.TM.Interp.TapeSt.ext_iff {x y : TapeSt} : x = y ↔ x.l = y.l ∧ x.p = y.p

def MIPRE.TM.Interp.TapeIs (τ : Tape) (pos : ℤ) (s : TapeSt) : Prop

The tape τ with head pos is as described by s.

Equations

• MIPRE.TM.Interp.TapeIs τ pos s = (MIPRE.TM.Interp.Holds τ 0 s.l ∧ (∀ q < 0, τ q = none) ∧ (∀ (q : ℤ), ↑s.l.length ≤ q → τ q = none) ∧ pos = ↑s.p)

def MIPRE.TM.Interp.overwrite (l : List Sym) (p : ℕ) (w : List Sym) : List Sym

Writing w over l from position p (no gap: p ≤ l.length).

Equations

• MIPRE.TM.Interp.overwrite l p w = List.take p l ++ w ++ List.drop (p + w.length) l

@[simp]

theorem MIPRE.TM.Interp.overwrite_zero (l w : List Sym) : overwrite l 0 w = w ++ List.drop w.length l

theorem MIPRE.TM.Interp.overwrite_append (a l w : List Sym) : overwrite (a ++ l) a.length w = a ++ w ++ List.drop w.length l

theorem MIPRE.TM.Interp.overwrite_append' (a l w : List Sym) {p : ℕ} (hp : p = a.length) : overwrite (a ++ l) p w = a ++ w ++ List.drop w.length l

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.length_overwrite {l : List Sym} {p : ℕ} (hp : p ≤ l.length) (w : List Sym) : (overwrite l p w).length = max l.length (p + w.length)

@[simp]

theorem MIPRE.TM.Interp.overwrite_cons_succ (a : Sym) (l : List Sym) (p : ℕ) (w : List Sym) : overwrite (a :: l) (p + 1) w = a :: overwrite l p w

theorem MIPRE.TM.Interp.TapeIs.holds {τ : Tape} {pos : ℤ} {s : TapeSt} (h : TapeIs τ pos s) : Holds τ 0 s.l

theorem MIPRE.TM.Interp.TapeIs.before {τ : Tape} {pos : ℤ} {s : TapeSt} (h : TapeIs τ pos s) (q : ℤ) (hq : q < 0) : τ q = none

theorem MIPRE.TM.Interp.TapeIs.beyond {τ : Tape} {pos : ℤ} {s : TapeSt} (h : TapeIs τ pos s) (q : ℤ) (hq : ↑s.l.length ≤ q) : τ q = none

theorem MIPRE.TM.Interp.TapeIs.pos_eq {τ : Tape} {pos : ℤ} {s : TapeSt} (h : TapeIs τ pos s) : pos = ↑s.p

theorem MIPRE.TM.Interp.TapeIs.read {τ : Tape} {pos : ℤ} {s : TapeSt} (h : TapeIs τ pos s) (n : ℕ) : τ ↑n = s.l[n]?

The cell n.

theorem MIPRE.TM.Interp.TapeIs.read_pos {τ : Tape} {pos : ℤ} {s : TapeSt} (h : TapeIs τ pos s) : τ pos = s.l[s.p]?

The cell under the head.

theorem MIPRE.TM.Interp.TapeIs.holds_sub {τ : Tape} {pos : ℤ} {s : TapeSt} (h : TapeIs τ pos s) {l₁ l₂ l₃ : List Sym} (e : s.l = l₁ ++ l₂ ++ l₃) : Holds τ (↑l₁.length) l₂

A middle segment is held at its offset.

theorem MIPRE.TM.Interp.TapeIs.holds_drop {τ : Tape} {pos : ℤ} {s : TapeSt} (h : TapeIs τ pos s) (n : ℕ) : Holds τ (↑n) (List.drop n s.l)

The tail from n.

theorem MIPRE.TM.Interp.TapeIs.blank_after_drop {τ : Tape} {pos : ℤ} {s : TapeSt} (h : TapeIs τ pos s) (n : ℕ) : τ (↑n + ↑(List.drop n s.l).length) = none

theorem MIPRE.TM.Interp.TapeIs.of_same {τ : Tape} {pos : ℤ} {l : List Sym} {p : ℕ} (h : TapeIs τ pos { l := l, p := p }) {τ' : Tape} {pos' : ℤ} {p' : ℕ} (hτ : τ' = τ) (hpos : pos' = ↑p') : TapeIs τ' pos' { l := l, p := p' }

Same tape, another head position.

theorem MIPRE.TM.Interp.TapeIs.of_overwrite {τ : Tape} {pos : ℤ} {l : List Sym} {p : ℕ} (h : TapeIs τ pos { l := l, p := p }) (hp : p ≤ l.length) {τ' : Tape} {pos' : ℤ} {p' : ℕ} {w : List Sym} (hw : Holds τ' (↑p) w) (hout : ∀ (q : ℤ), q < ↑p ∨ ↑p + ↑w.length ≤ q → τ' q = τ q) (hpos : pos' = ↑p') : TapeIs τ' pos' { l := overwrite l p w, p := p' }

w written from p, the rest as before.

theorem MIPRE.TM.Interp.TapeIs.of_truncate {τ : Tape} {pos : ℤ} {l : List Sym} {p : ℕ} (h : TapeIs τ pos { l := l, p := p }) {n : ℕ} (hn : n ≤ l.length) {τ' : Tape} {pos' : ℤ} {p' : ℕ} (hout : ∀ (q : ℤ), q < ↑n ∨ ↑l.length ≤ q → τ' q = τ q) (hbl : BlankFrom τ' (↑n) (l.length - n)) (hpos : pos' = ↑p') : TapeIs τ' pos' { l := List.take n l, p := p' }

Erased from n to the end.

theorem MIPRE.TM.Interp.TapeIs.of_unary {τ : Tape} {pos : ℤ} {n : ℕ} (hu : Unary τ n) (hpos : pos = ↑n) : TapeIs τ pos { l := List.replicate n Sym.one, p := n }

theorem MIPRE.TM.Interp.TapeIs.unary {τ : Tape} {pos : ℤ} {n : ℕ} (h : TapeIs τ pos { l := List.replicate n Sym.one, p := n }) : Unary τ n

theorem MIPRE.TM.Interp.TapeIs.envTape {τ : Tape} {pos : ℤ} {env : Cost.Env} {p : ℕ} (h : TapeIs τ pos { l := envRepr env, p := p }) : EnvTape τ env

A configuration

def MIPRE.TM.Interp.Desc {input : Fin 7 → List Sym} (c : Cfg input) (q : Option Ctl) (ds : WT → TapeSt) : Prop

The configuration c has control q and its work tapes are as described by ds.

Equations

• MIPRE.TM.Interp.Desc c q ds = (c.state = q ∧ ∀ (t : Fin 6), MIPRE.TM.Interp.TapeIs (c.workTapes t) (c.workTapePos t) (ds t))

theorem MIPRE.TM.Interp.Desc.state {input : Fin 7 → List Sym} {c : Cfg input} {q : Option Ctl} {ds : WT → TapeSt} (h : Desc c q ds) : c.state = q

theorem MIPRE.TM.Interp.Desc.tape {input : Fin 7 → List Sym} {c : Cfg input} {q : Option Ctl} {ds : WT → TapeSt} (h : Desc c q ds) (t : WT) : TapeIs (c.workTapes t) (c.workTapePos t) (ds t)

theorem MIPRE.TM.Interp.Desc.pos {input : Fin 7 → List Sym} {c : Cfg input} {q : Option Ctl} {ds : WT → TapeSt} (h : Desc c q ds) (t : WT) : c.workTapePos t = ↑(ds t).p

theorem MIPRE.TM.Interp.Desc.read {input : Fin 7 → List Sym} {c : Cfg input} {q : Option Ctl} {ds : WT → TapeSt} (h : Desc c q ds) (t : WT) : c.workTapes t (c.workTapePos t) = (ds t).l[(ds t).p]?

theorem MIPRE.TM.Interp.Desc.cast {input : Fin 7 → List Sym} {c : Cfg input} {q : Option Ctl} {ds : WT → TapeSt} (h : Desc c q ds) {q' : Option Ctl} {ds' : WT → TapeSt} (hq : q = q') (hds : ds = ds') : Desc c q' ds'

theorem MIPRE.TM.Interp.Desc.of_untouched {input : Fin 7 → List Sym} {c : Cfg input} {q : Option Ctl} {ds : WT → TapeSt} (h : Desc c q ds) {c' : Cfg input} {SW : List WT} (hu : Untouched c c' [] SW) {q' : Option Ctl} (hq' : c'.state = q') {ds' : WT → TapeSt} (hT : ∀ t ∈ SW, TapeIs (c'.workTapes t) (c'.workTapePos t) (ds' t)) (hS : ∀ t ∉ SW, ds' t = ds t) : Desc c' q' ds'

A run touching only the tapes in SW, whose new descriptions are given.

The routines on descriptions

theorem MIPRE.TM.Interp.D_write {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {ds : WT → TapeSt} {t : WT} {s : Sym} (hins : instrAt k pc = Instr.write t s) (hpc : ↑pc + 1 < maxPc) (hd : Desc c (at_ k pc) ds) (hp : (ds t).p ≤ (ds t).l.length) : ∃ (c' : Cfg input), Reach c 1 c' [] ∧ Desc c' (next_ k pc hpc) (Function.update ds t { l := overwrite (ds t).l (ds t).p [s], p := (ds t).p + 1 })

theorem MIPRE.TM.Interp.D_move_right {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {ds : WT → TapeSt} {t : WT} (hins : instrAt k pc = Instr.move t true) (hpc : ↑pc + 1 < maxPc) (hd : Desc c (at_ k pc) ds) : ∃ (c' : Cfg input), Reach c 1 c' [] ∧ Desc c' (next_ k pc hpc) (Function.update ds t { l := (ds t).l, p := (ds t).p + 1 })

theorem MIPRE.TM.Interp.D_move_left {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {ds : WT → TapeSt} {t : WT} (hins : instrAt k pc = Instr.move t false) (hpc : ↑pc + 1 < maxPc) (hd : Desc c (at_ k pc) ds) (hp : 1 ≤ (ds t).p) : ∃ (c' : Cfg input), Reach c 1 c' [] ∧ Desc c' (next_ k pc hpc) (Function.update ds t { l := (ds t).l, p := (ds t).p - 1 })

theorem MIPRE.TM.Interp.D_rewind {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {ds : WT → TapeSt} {t : WT} (hins : instrAt k pc = Instr.rewind t) (hpc : ↑pc + 1 < maxPc) (hd : Desc c (at_ k pc) ds) (hp : (ds t).p ≤ (ds t).l.length) : ∃ (c' : Cfg input), Reach c ((ds t).p + 2) c' [] ∧ Desc c' (next_ k pc hpc) (Function.update ds t { l := (ds t).l, p := 0 })

theorem MIPRE.TM.Interp.D_toEnd {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {ds : WT → TapeSt} {t : WT} (hins : instrAt k pc = Instr.toEnd t) (hpc : ↑pc + 1 < maxPc) (hd : Desc c (at_ k pc) ds) (hp : (ds t).p ≤ (ds t).l.length) : ∃ (c' : Cfg input), Reach c ((ds t).l.length - (ds t).p + 1) c' [] ∧ Desc c' (next_ k pc hpc) (Function.update ds t { l := (ds t).l, p := (ds t).l.length })

theorem MIPRE.TM.Interp.D_eraseRight {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {ds : WT → TapeSt} {t : WT} (hins : instrAt k pc = Instr.eraseRight t) (hpc : ↑pc + 1 < maxPc) (hd : Desc c (at_ k pc) ds) (hp : (ds t).p ≤ (ds t).l.length) (hfr : ∀ s ∈ List.drop (ds t).p (ds t).l, s ≠ Sym.fr) : ∃ (c' : Cfg input), Reach c (2 * ((ds t).l.length - (ds t).p) + 1) c' [] ∧ Desc c' (next_ k pc hpc) (Function.update ds t { l := List.take (ds t).p (ds t).l, p := (ds t).p })

theorem MIPRE.TM.Interp.D_copyUntil {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {ds : WT → TapeSt} {m : Option Sym} {src dst : WT} (hins : instrAt k pc = Instr.copyUntil m src dst) (hpc : ↑pc + 1 < maxPc) (hsd : src ≠ dst) (hd : Desc c (at_ k pc) ds) {l₁ w l₂ : List Sym} (hsrc : (ds src).l = l₁ ++ w ++ l₂) (hsp : (ds src).p = l₁.length) (hm : ∀ s ∈ w, some s ≠ m) (hend : l₂[0]? = m) (hdp : (ds dst).p ≤ (ds dst).l.length) : ∃ (c' : Cfg input), Reach c (w.length + 1) c' [] ∧ Desc c' (next_ k pc hpc) (Function.update (Function.update ds src { l := (ds src).l, p := l₁.length + w.length }) dst { l := overwrite (ds dst).l (ds dst).p w, p := (ds dst).p + w.length })

theorem MIPRE.TM.Interp.D_branch_taken {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {ds : WT → TapeSt} {t : WT} {s : Option Sym} {target : ProgId} (hins : instrAt k pc = Instr.branch t s target) (hd : Desc c (at_ k pc) ds) (hs : (ds t).l[(ds t).p]? = s) : ∃ (c' : Cfg input), Reach c 1 c' [] ∧ Desc c' (at_ target ⟨0, D_branch_taken._proof_1⟩) ds

theorem MIPRE.TM.Interp.D_branch_not {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {ds : WT → TapeSt} {t : WT} {s : Option Sym} {target : ProgId} (hins : instrAt k pc = Instr.branch t s target) (hpc : ↑pc + 1 < maxPc) (hd : Desc c (at_ k pc) ds) (hs : (ds t).l[(ds t).p]? ≠ s) : ∃ (c' : Cfg input), Reach c 1 c' [] ∧ Desc c' (next_ k pc hpc) ds

theorem MIPRE.TM.Interp.D_jump {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {ds : WT → TapeSt} {target : ProgId} (hins : instrAt k pc = Instr.jump target) (hd : Desc c (at_ k pc) ds) : ∃ (c' : Cfg input), Reach c 1 c' [] ∧ Desc c' (at_ target ⟨0, D_branch_taken._proof_1⟩) ds

theorem MIPRE.TM.Interp.D_leftToMarker {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {ds : WT → TapeSt} {m : Sym} {t : WT} (hins : instrAt k pc = Instr.leftToMarker m t) (hpc : ↑pc + 1 < maxPc) (hd : Desc c (at_ k pc) ds) {l₁ w l₂ : List Sym} (hl : (ds t).l = l₁ ++ w ++ l₂) (hp : (ds t).p = l₁.length + w.length) (hm : ∀ s ∈ w, s ≠ m) (hl₁ : l₁ = [] ∨ ∃ (l₀ : List Sym), l₁ = l₀ ++ [m]) : ∃ (c' : Cfg input), Reach c (w.length + 2) c' [] ∧ Desc c' (next_ k pc hpc) (Function.update ds t { l := (ds t).l, p := l₁.length })

theorem MIPRE.TM.Interp.D_popBack {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {ds : WT → TapeSt} {m : Sym} {t : WT} (hins : instrAt k pc = Instr.popBack m t) (hpc : ↑pc + 1 < maxPc) (hd : Desc c (at_ k pc) ds) {l₁ w : List Sym} {a : Sym} (hl : (ds t).l = l₁ ++ w ++ [a]) (hp : (ds t).p = (ds t).l.length) (hm : ∀ s ∈ w, s ≠ m) (hl₁ : l₁ = [] ∨ ∃ (l₀ : List Sym), l₁ = l₀ ++ [m]) : ∃ (c' : Cfg input), Reach c (w.length + 3) c' [] ∧ Desc c' (next_ k pc hpc) (Function.update ds t { l := l₁, p := l₁.length })

theorem MIPRE.TM.Interp.D_popBack_empty {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {ds : WT → TapeSt} {m : Sym} {t : WT} (hins : instrAt k pc = Instr.popBack m t) (hpc : ↑pc + 1 < maxPc) (hd : Desc c (at_ k pc) ds) (hl : (ds t).l = []) (hp : (ds t).p = 0) : ∃ (c' : Cfg input), Reach c 2 c' [] ∧ Desc c' (next_ k pc hpc) ds

theorem MIPRE.TM.Interp.D_charge {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {ds : WT → TapeSt} (hins : instrAt k pc = Instr.charge false) (hpc : ↑pc + 1 < maxPc) (hd : Desc c (at_ k pc) ds) {r : ℕ} (hb : ds BUD = { l := List.replicate (r + 1) Sym.one, p := r + 1 }) : ∃ (c' : Cfg input), Reach c 2 c' [] ∧ Desc c' (next_ k pc hpc) (Function.update ds BUD { l := List.replicate r Sym.one, p := r })

theorem MIPRE.TM.Interp.D_charge_fail {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {ds : WT → TapeSt} (hins : instrAt k pc = Instr.charge false) (hd : Desc c (at_ k pc) ds) (hb : ds BUD = { l := [], p := 0 }) : HaltsIn c 2

theorem MIPRE.TM.Interp.D_getEnv {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {ds : WT → TapeSt} (hins : instrAt k pc = Instr.getEnv) (hpc : ↑pc + 1 < maxPc) (hd : Desc c (at_ k pc) ds) {env : Cost.Env} (hE : ds E = { l := envRepr env, p := (envRepr env).length }) {i : ℕ} {l₁ l₂ : List Sym} (hC : (ds C).l = l₁ ++ S (Cost.Data.ofNat i) ++ l₂) (hCp : (ds C).p = l₁.length) (hX : (ds X).p ≤ (ds X).l.length) : ∃ n ≤ 3 * i + 3 * (envRepr env).length + 9, ∃ (c' : Cfg input), Reach c n c' [] ∧ Desc c' (next_ k pc hpc) (Function.update (Function.update ds C { l := (ds C).l, p := l₁.length + (2 * i + 1) }) X { l := overwrite (ds X).l (ds X).p (S (env.get i)), p := (ds X).p + (S (env.get i)).length })

theorem MIPRE.TM.Interp.D_copyTree {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {ds : WT → TapeSt} {src t : WT} (hins : instrAt k pc = Instr.copyTree src (some t) false) (hpc : ↑pc + 1 < maxPc) (hst : src ≠ t) (hsc : src ≠ CNT) (htc : t ≠ CNT) (hd : Desc c (at_ k pc) ds) (hcnt : ds CNT = { l := [], p := 0 }) {v : Cost.Data} {l₁ l₂ : List Sym} (hsrc : (ds src).l = l₁ ++ S v ++ l₂) (hsp : (ds src).p = l₁.length) (htp : (ds t).p ≤ (ds t).l.length) : ∃ n ≤ 3 * v.size + 1, ∃ (c' : Cfg input), Reach c n c' [] ∧ Desc c' (next_ k pc hpc) (Function.update (Function.update ds src { l := (ds src).l, p := l₁.length + v.size }) t { l := overwrite (ds t).l (ds t).p (S v), p := (ds t).p + v.size })

theorem MIPRE.TM.Interp.D_skipTree {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {ds : WT → TapeSt} {src : WT} (hins : instrAt k pc = Instr.copyTree src none false) (hpc : ↑pc + 1 < maxPc) (hsc : src ≠ CNT) (hd : Desc c (at_ k pc) ds) (hcnt : ds CNT = { l := [], p := 0 }) {v : Cost.Data} {l₁ l₂ : List Sym} (hsrc : (ds src).l = l₁ ++ S v ++ l₂) (hsp : (ds src).p = l₁.length) : ∃ n ≤ 3 * v.size + 1, ∃ (c' : Cfg input), Reach c n c' [] ∧ Desc c' (next_ k pc hpc) (Function.update ds src { l := (ds src).l, p := l₁.length + v.size })

theorem MIPRE.TM.Interp.D_copyTree_charge {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {ds : WT → TapeSt} {src t : WT} (hins : instrAt k pc = Instr.copyTree src (some t) true) (hpc : ↑pc + 1 < maxPc) (hst : src ≠ t) (hsc : src ≠ CNT) (htc : t ≠ CNT) (hsb : src ≠ BUD) (htb : t ≠ BUD) (hd : Desc c (at_ k pc) ds) (hcnt : ds CNT = { l := [], p := 0 }) {r : ℕ} (hbud : ds BUD = { l := List.replicate r Sym.one, p := r }) {v : Cost.Data} {l₁ l₂ : List Sym} (hsrc : (ds src).l = l₁ ++ S v ++ l₂) (hsp : (ds src).p = l₁.length) (htp : (ds t).p ≤ (ds t).l.length) (hr : v.size ≤ r) : ∃ n ≤ 4 * v.size + 1, ∃ (c' : Cfg input), Reach c n c' [] ∧ Desc c' (next_ k pc hpc) (Function.update (Function.update (Function.update ds src { l := (ds src).l, p := l₁.length + v.size }) t { l := overwrite (ds t).l (ds t).p (S v), p := (ds t).p + v.size }) BUD { l := List.replicate (r - v.size) Sym.one, p := r - v.size })

theorem MIPRE.TM.Interp.D_copyTree_charge_fail {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {c : Cfg input} {ds : WT → TapeSt} {src t : WT} (hins : instrAt k pc = Instr.copyTree src (some t) true) (hpc : ↑pc + 1 < maxPc) (hst : src ≠ t) (hsc : src ≠ CNT) (htc : t ≠ CNT) (hsb : src ≠ BUD) (htb : t ≠ BUD) (hd : Desc c (at_ k pc) ds) (hcnt : ds CNT = { l := [], p := 0 }) {r : ℕ} (hbud : ds BUD = { l := List.replicate r Sym.one, p := r }) {v : Cost.Data} {l₁ l₂ : List Sym} (hsrc : (ds src).l = l₁ ++ S v ++ l₂) (hsp : (ds src).p = l₁.length) (hr : r < v.size) : HaltsIn c (4 * v.size + 1)