Runs of the interpreter

Reach c n c' out: from the configuration c, n steps of U lead to c', emitting out. It composes (Reach.trans), and a single step is the action of the current instruction phase (step_eq, applyAct). The routine specifications (Routines.lean) are reachability statements with step bounds.

@[reducible, inline]

abbrev MIPRE.TM.Interp.Cfg (input : Fin 7 → List Sym) : Type

Configurations of the interpreter on the inputs input.

Equations

• MIPRE.TM.Interp.Cfg input = Turing.MultiInputTM.Cfg 7 6 MIPRE.TM.Interp.Sym MIPRE.TM.Interp.Ctl input

def MIPRE.TM.Interp.applyAct {input : Fin 7 → List Sym} (a : Act) (q' : Option Ctl) (c : Cfg input) : Cfg input

The configuration after the actions a, with the control q'.

Equations

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

def MIPRE.TM.Interp.actOf {input : Fin 7 → List Sym} (q : Ctl) (c : Cfg input) : Act

The action of the current instruction phase.

Equations

• MIPRE.TM.Interp.actOf q c = MIPRE.TM.Interp.execInstr (MIPRE.TM.Interp.instrAt q.k q.pc) q.ph (Turing.MultiInputTM.Cfg.inputSymbols c) (Turing.MultiInputTM.Cfg.workTapeSymbols c)

theorem MIPRE.TM.Interp.step_eq {input : Fin 7 → List Sym} (c : Cfg input) {q : Ctl} (hq : c.state = some q) : Turing.MultiInputTM.step c = applyAct (actOf q c) (resolve q.k q.pc (actOf q c).next) c

One step of U is the action of the current instruction phase.

theorem MIPRE.TM.Interp.outputSymbol_eq {input : Fin 7 → List Sym} (c : Cfg input) {q : Ctl} (hq : c.state = some q) : Turing.MultiInputTM.outputSymbol c = (actOf q c).out

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

n steps from c lead to c', emitting out.

Equations

• MIPRE.TM.Interp.Reach c n c' out = (Turing.MultiInputTM.configs c n = c' ∧ MIPRE.TM.Interp.U.outputString c n = out)

theorem MIPRE.TM.Interp.Reach.refl {input : Fin 7 → List Sym} (c : Cfg input) : Reach c 0 c []

theorem MIPRE.TM.Interp.Reach.trans {input : Fin 7 → List Sym} {c c' c'' : Cfg input} {n m : ℕ} {out out' : List Sym} (h : Reach c n c' out) (h' : Reach c' m c'' out') : Reach c (n + m) c'' (out ++ out')

theorem MIPRE.TM.Interp.Reach.single {input : Fin 7 → List Sym} (c : Cfg input) : Reach c 1 (Turing.MultiInputTM.step c) (Turing.MultiInputTM.outputSymbol c).toList

theorem MIPRE.TM.Interp.Reach.cast_n {input : Fin 7 → List Sym} {c c' : Cfg input} {n n' : ℕ} {out : List Sym} (h : Reach c n c' out) (e : n = n') : Reach c n' c' out

theorem MIPRE.TM.Interp.Reach.cast_out {input : Fin 7 → List Sym} {c c' : Cfg input} {n : ℕ} {out out' : List Sym} (h : Reach c n c' out) (e : out = out') : Reach c n c' out'

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

Halting silently: the state is none after n steps, and nothing was emitted.

Equations

• MIPRE.TM.Interp.HaltsIn c n = ((Turing.MultiInputTM.configs c n).state = none ∧ MIPRE.TM.Interp.U.outputString c n = [])

theorem MIPRE.TM.Interp.HaltsIn.of_reach {input : Fin 7 → List Sym} {c c' : Cfg input} {n : ℕ} (h : Reach c n c' []) (h' : c'.state = none) : HaltsIn c n

theorem MIPRE.TM.Interp.HaltsIn.mono {input : Fin 7 → List Sym} {c : Cfg input} {n m : ℕ} (h : HaltsIn c n) (hnm : n ≤ m) : HaltsIn c m

theorem MIPRE.TM.Interp.HaltsIn.after {input : Fin 7 → List Sym} {c c' : Cfg input} {n m : ℕ} (h : Reach c n c' []) (h' : HaltsIn c' m) : HaltsIn c (n + m)

A silent run followed by a silent halt.

Reading and writing under applyAct

@[simp]

theorem MIPRE.TM.Interp.applyAct_state {input : Fin 7 → List Sym} (a : Act) (q' : Option Ctl) (c : Cfg input) : (applyAct a q' c).state = q'

@[simp]

theorem MIPRE.TM.Interp.applyAct_inputPos {input : Fin 7 → List Sym} (a : Act) (q' : Option Ctl) (c : Cfg input) (j : IT) : (applyAct a q' c).inputPos j = Turing.MultiTapeTM.moveInputPos (c.inputPos j) (a.inMoves j)

@[simp]

theorem MIPRE.TM.Interp.applyAct_workTapePos {input : Fin 7 → List Sym} (a : Act) (q' : Option Ctl) (c : Cfg input) (d : WT) : (applyAct a q' c).workTapePos d = c.workTapePos d + ↑(a.works d).2

theorem MIPRE.TM.Interp.applyAct_workTapes_of_none {input : Fin 7 → List Sym} (a : Act) (q' : Option Ctl) (c : Cfg input) (d : WT) (h : (a.works d).1 = none) : (applyAct a q' c).workTapes d = c.workTapes d

theorem MIPRE.TM.Interp.applyAct_workTapes_of_some {input : Fin 7 → List Sym} (a : Act) (q' : Option Ctl) (c : Cfg input) (d : WT) {s : Option Sym} (h : (a.works d).1 = some s) : (applyAct a q' c).workTapes d = Function.update (c.workTapes d) (c.workTapePos d) s

Evaluating actions

@[simp]

theorem MIPRE.TM.Interp.Act.base_inMoves (n : Next) (j : IT) : (base n).inMoves j = 0

@[simp]

theorem MIPRE.TM.Interp.Act.base_works (n : Next) (d : WT) : (base n).works d = (none, 0)

@[simp]

theorem MIPRE.TM.Interp.Act.base_out (n : Next) : (base n).out = none

@[simp]

theorem MIPRE.TM.Interp.Act.base_next (n : Next) : (base n).next = n

@[simp]

theorem MIPRE.TM.Interp.Act.mw_next (a : Act) (t : WT) (m : SignType) : (a.mw t m).next = a.next

@[simp]

theorem MIPRE.TM.Interp.Act.ww_next (a : Act) (t : WT) (s : Option Sym) : (a.ww t s).next = a.next

@[simp]

theorem MIPRE.TM.Interp.Act.mi_next (a : Act) (j : IT) (m : SignType) : (a.mi j m).next = a.next

@[simp]

theorem MIPRE.TM.Interp.Act.emit_next (a : Act) (s : Sym) : (a.emit s).next = a.next

@[simp]

theorem MIPRE.TM.Interp.Act.mw_out (a : Act) (t : WT) (m : SignType) : (a.mw t m).out = a.out

@[simp]

theorem MIPRE.TM.Interp.Act.ww_out (a : Act) (t : WT) (s : Option Sym) : (a.ww t s).out = a.out

@[simp]

theorem MIPRE.TM.Interp.Act.mi_out (a : Act) (j : IT) (m : SignType) : (a.mi j m).out = a.out

@[simp]

theorem MIPRE.TM.Interp.Act.emit_out (a : Act) (s : Sym) : (a.emit s).out = some s

@[simp]

theorem MIPRE.TM.Interp.Act.mw_inMoves (a : Act) (t : WT) (m : SignType) : (a.mw t m).inMoves = a.inMoves

@[simp]

theorem MIPRE.TM.Interp.Act.ww_inMoves (a : Act) (t : WT) (s : Option Sym) : (a.ww t s).inMoves = a.inMoves

@[simp]

theorem MIPRE.TM.Interp.Act.emit_inMoves (a : Act) (s : Sym) : (a.emit s).inMoves = a.inMoves

@[simp]

theorem MIPRE.TM.Interp.Act.mi_inMoves (a : Act) (j : IT) (m : SignType) : (a.mi j m).inMoves = Function.update a.inMoves j m

@[simp]

theorem MIPRE.TM.Interp.Act.mi_works (a : Act) (j : IT) (m : SignType) : (a.mi j m).works = a.works

@[simp]

theorem MIPRE.TM.Interp.Act.emit_works (a : Act) (s : Sym) : (a.emit s).works = a.works

@[simp]

theorem MIPRE.TM.Interp.Act.mw_works_self (a : Act) (t : WT) (m : SignType) : (a.mw t m).works t = ((a.works t).1, m)

theorem MIPRE.TM.Interp.Act.mw_works_of_ne (a : Act) {t t' : WT} (h : t' ≠ t) (m : SignType) : (a.mw t m).works t' = a.works t'

@[simp]

theorem MIPRE.TM.Interp.Act.ww_works_self (a : Act) (t : WT) (s : Option Sym) : (a.ww t s).works t = (some s, (a.works t).2)

theorem MIPRE.TM.Interp.Act.ww_works_of_ne (a : Act) {t t' : WT} (h : t' ≠ t) (s : Option Sym) : (a.ww t s).works t' = a.works t'