The routines: specifications of the instructions #
Each instruction's specification is a reachability statement: from a configuration at
the instruction's first phase, with the tapes it reads in a stated shape, a bounded
number of steps leads to the configuration at the next instruction, with the stated
effect on the tapes it touches and none on the others (Untouched).
@[reducible, inline]
The control at (k, pc), first phase.
Equations
- MIPRE.TM.Interp.at_ k pc = some { k := k, pc := pc, ph := MIPRE.TM.Interp.Phase.p0 }
Instances For
def
MIPRE.TM.Interp.Untouched
{input : Fin 7 → List Sym}
(c c' : Cfg input)
(SI : List IT)
(SW : List WT)
:
c' agrees with c on the input heads outside SI and on the work tapes outside SW.
Equations
- MIPRE.TM.Interp.Untouched c c' SI SW = ((∀ j ∉ SI, c'.inputPos j = c.inputPos j) ∧ ∀ d ∉ SW, c'.workTapes d = c.workTapes d ∧ c'.workTapePos d = c.workTapePos d)
Instances For
One step of an instruction #
theorem
MIPRE.TM.Interp.step_instr
{input : Fin 7 → List Sym}
{c : Cfg input}
{k : ProgId}
{pc : Fin maxPc}
{ph : Phase}
(hq : c.state = some { k := k, pc := pc, ph := ph })
{ins : Instr}
(hins : instrAt k pc = ins)
:
have a := execInstr ins ph (Turing.MultiInputTM.Cfg.inputSymbols c) (Turing.MultiInputTM.Cfg.workTapeSymbols c);
Reach c 1 (applyAct a (resolve k pc a.next) c) a.out.toList
One step at (k, pc, ph) executing the instruction ins there.
write #
move #
toEnd #
theorem
MIPRE.TM.Interp.exec_toEnd
{input : Fin 7 → List Sym}
{k : ProgId}
{pc : Fin maxPc}
{t : WT}
(hins : instrAt k pc = Instr.toEnd t)
(hpc : ↑pc + 1 < maxPc)
(l : List Sym)
(c : Cfg input)
:
c.state = at_ k pc →
Holds (c.workTapes t) (c.workTapePos t) l →
c.workTapes t (c.workTapePos t + ↑l.length) = none →
∃ (c' : Cfg input),
Reach c (l.length + 1) c' [] ∧ c'.state = next_ k pc hpc ∧ Untouched c c' [] [t] ∧ c'.workTapes t = c.workTapes t ∧ c'.workTapePos t = c.workTapePos t + ↑l.length
rewind #
theorem
MIPRE.TM.Interp.scan_rewind
{input : Fin 7 → List Sym}
{k : ProgId}
{pc : Fin maxPc}
{t : WT}
(hins : instrAt k pc = Instr.rewind t)
(hpc : ↑pc + 1 < maxPc)
(n : ℕ)
(c : Cfg input)
:
c.state = some { k := k, pc := pc, ph := Phase.p1 } →
(∀ (q : ℤ), c.workTapePos t - ↑n < q → q ≤ c.workTapePos t → c.workTapes t q ≠ none) →
c.workTapes t (c.workTapePos t - ↑n) = none →
∃ (c' : Cfg input),
Reach c (n + 1) c' [] ∧ c'.state = next_ k pc hpc ∧ Untouched c c' [] [t] ∧ c'.workTapes t = c.workTapes t ∧ c'.workTapePos t = c.workTapePos t - ↑n + 1
The scan of rewind from p1: cells pos - n + 1 … pos not blank, pos - n blank.
theorem
MIPRE.TM.Interp.exec_rewind
{input : Fin 7 → List Sym}
{k : ProgId}
{pc : Fin maxPc}
{t : WT}
(hins : instrAt k pc = Instr.rewind t)
(hpc : ↑pc + 1 < maxPc)
(n : ℕ)
(c : Cfg input)
(hq : c.state = at_ k pc)
(hne : ∀ (q : ℤ), c.workTapePos t - ↑n ≤ q → q < c.workTapePos t → c.workTapes t q ≠ none)
(hbl : c.workTapes t (c.workTapePos t - ↑n - 1) = none)
:
From cell p + n with cells p … p + n - 1 not blank and p - 1 blank, rewind
reaches cell p (the head may start on the blank after the content).
eraseRight #
theorem
MIPRE.TM.Interp.scan_erase
{input : Fin 7 → List Sym}
{k : ProgId}
{pc : Fin maxPc}
{t : WT}
(hins : instrAt k pc = Instr.eraseRight t)
(l : List Sym)
(c : Cfg input)
:
c.state = some { k := k, pc := pc, ph := Phase.p1 } →
Holds (c.workTapes t) (c.workTapePos t) l →
c.workTapes t (c.workTapePos t + ↑l.length) = none →
∃ (c' : Cfg input),
Reach c (l.length + 1) c' [] ∧ c'.state = some { k := k, pc := pc, ph := Phase.p2 } ∧ Untouched c c' [] [t] ∧ (∀ (q : ℤ), q < c.workTapePos t ∨ c.workTapePos t + ↑l.length ≤ q → c'.workTapes t q = c.workTapes t q) ∧ BlankFrom (c'.workTapes t) (c.workTapePos t) l.length ∧ c'.workTapePos t = c.workTapePos t + ↑l.length - 1
The erasing scan of eraseRight (p1): erase the l held from the head, then one
left.
theorem
MIPRE.TM.Interp.scan_eraseBack
{input : Fin 7 → List Sym}
{k : ProgId}
{pc : Fin maxPc}
{t : WT}
(hins : instrAt k pc = Instr.eraseRight t)
(hpc : ↑pc + 1 < maxPc)
(n : ℕ)
(c : Cfg input)
:
c.state = some { k := k, pc := pc, ph := Phase.p2 } →
BlankFrom (c.workTapes t) (c.workTapePos t - ↑n + 1) n →
c.workTapes t (c.workTapePos t - ↑n) = some Sym.fr →
∃ (c' : Cfg input),
Reach c (n + 1) c' [] ∧ c'.state = next_ k pc hpc ∧ Untouched c c' [] [t] ∧ c'.workTapes t = Function.update (c.workTapes t) (c.workTapePos t - ↑n) none ∧ c'.workTapePos t = c.workTapePos t - ↑n
The return scan of eraseRight (p2): back over n blanks to the $, erase it.
theorem
MIPRE.TM.Interp.exec_eraseRight
{input : Fin 7 → List Sym}
{k : ProgId}
{pc : Fin maxPc}
{t : WT}
(hins : instrAt k pc = Instr.eraseRight t)
(hpc : ↑pc + 1 < maxPc)
(l : List Sym)
(c : Cfg input)
(hq : c.state = at_ k pc)
(hl : Holds (c.workTapes t) (c.workTapePos t) l)
(hend : c.workTapes t (c.workTapePos t + ↑l.length) = none)
:
∃ (c' : Cfg input),
Reach c (2 * l.length + 1) c' [] ∧ c'.state = next_ k pc hpc ∧ Untouched c c' [] [t] ∧ (∀ (q : ℤ), q < c.workTapePos t ∨ c.workTapePos t + ↑l.length ≤ q → c'.workTapes t q = c.workTapes t q) ∧ BlankFrom (c'.workTapes t) (c.workTapePos t) l.length ∧ c'.workTapePos t = c.workTapePos t
Erase the l held from the head (no $ among its symbols), ending where it started.
copyUntil #
theorem
MIPRE.TM.Interp.exec_copyUntil
{input : Fin 7 → List Sym}
{k : ProgId}
{pc : Fin maxPc}
{m : Option Sym}
{src dst : WT}
(hins : instrAt k pc = Instr.copyUntil m src dst)
(hpc : ↑pc + 1 < maxPc)
(hsd : src ≠ dst)
(l : List Sym)
(c : Cfg input)
:
c.state = at_ k pc →
Holds (c.workTapes src) (c.workTapePos src) l →
(∀ s ∈ l, some s ≠ m) →
c.workTapes src (c.workTapePos src + ↑l.length) = m →
∃ (c' : Cfg input),
Reach c (l.length + 1) c' [] ∧ c'.state = next_ k pc hpc ∧ Untouched c c' [] [src, dst] ∧ c'.workTapes src = c.workTapes src ∧ c'.workTapePos src = c.workTapePos src + ↑l.length ∧ Holds (c'.workTapes dst) (c.workTapePos dst) l ∧ (∀ (q : ℤ),
q < c.workTapePos dst ∨ c.workTapePos dst + ↑l.length ≤ q →
c'.workTapes dst q = c.workTapes dst q) ∧ c'.workTapePos dst = c.workTapePos dst + ↑l.length
Copy the l held from the head of src (none of whose symbols is m) onto dst,
stopping with the src head on the m after it.
branch, jump, emit, halt #
Scanning left #
theorem
MIPRE.TM.Interp.scan_leftToMarker
{input : Fin 7 → List Sym}
{k : ProgId}
{pc : Fin maxPc}
{m : Sym}
{t : WT}
(hins : instrAt k pc = Instr.leftToMarker m t)
(hpc : ↑pc + 1 < maxPc)
(l : List Sym)
(c : Cfg input)
:
c.state = some { k := k, pc := pc, ph := Phase.p1 } →
Holds (c.workTapes t) (c.workTapePos t + 1 - ↑l.length) l →
(∀ s ∈ l, s ≠ m) →
c.workTapes t (c.workTapePos t - ↑l.length) = some m ∨ c.workTapes t (c.workTapePos t - ↑l.length) = none →
∃ (c' : Cfg input),
Reach c (l.length + 1) c' [] ∧ c'.state = next_ k pc hpc ∧ Untouched c c' [] [t] ∧ c'.workTapes t = c.workTapes t ∧ c'.workTapePos t = c.workTapePos t - ↑l.length + 1
The scan of leftToMarker (phase p1): over the cells pos - n + 1 … pos, none holding
m, to the marker or blank at pos - n, then one right.
theorem
MIPRE.TM.Interp.exec_leftToMarker
{input : Fin 7 → List Sym}
{k : ProgId}
{pc : Fin maxPc}
{m : Sym}
{t : WT}
(hins : instrAt k pc = Instr.leftToMarker m t)
(hpc : ↑pc + 1 < maxPc)
(l : List Sym)
(c : Cfg input)
(hq : c.state = at_ k pc)
(hl : Holds (c.workTapes t) (c.workTapePos t - ↑l.length) l)
(hm : ∀ s ∈ l, s ≠ m)
(hend :
c.workTapes t (c.workTapePos t - ↑l.length - 1) = some m ∨ c.workTapes t (c.workTapePos t - ↑l.length - 1) = none)
:
leftToMarker: from pos, with l (no m) on pos - |l| … pos - 1 and the marker or a
blank at pos - |l| - 1, to pos - |l|.
popBack #
theorem
MIPRE.TM.Interp.scan_popBack
{input : Fin 7 → List Sym}
{k : ProgId}
{pc : Fin maxPc}
{m : Sym}
{t : WT}
(hins : instrAt k pc = Instr.popBack m t)
(hpc : ↑pc + 1 < maxPc)
(l : List Sym)
(c : Cfg input)
:
c.state = some { k := k, pc := pc, ph := Phase.p2 } →
Holds (c.workTapes t) (c.workTapePos t + 1 - ↑l.length) l →
(∀ s ∈ l, s ≠ m) →
c.workTapes t (c.workTapePos t - ↑l.length) = some m ∨ c.workTapes t (c.workTapePos t - ↑l.length) = none →
∃ (c' : Cfg input),
Reach c (l.length + 1) c' [] ∧ c'.state = next_ k pc hpc ∧ Untouched c c' [] [t] ∧ (∀ (q : ℤ),
q < c.workTapePos t + 1 - ↑l.length ∨ c.workTapePos t < q → c'.workTapes t q = c.workTapes t q) ∧ BlankFrom (c'.workTapes t) (c.workTapePos t + 1 - ↑l.length) l.length ∧ c'.workTapePos t = c.workTapePos t - ↑l.length + 1
The scan of popBack (phase p2): erase the cells pos - n + 1 … pos, none holding m,
to the marker or blank at pos - n, then one right.
theorem
MIPRE.TM.Interp.exec_popBack_empty
{input : Fin 7 → List Sym}
{k : ProgId}
{pc : Fin maxPc}
{m : Sym}
{t : WT}
(hins : instrAt k pc = Instr.popBack m t)
(hpc : ↑pc + 1 < maxPc)
(c : Cfg input)
(hq : c.state = at_ k pc)
(hbl : c.workTapes t (c.workTapePos t - 1) = none)
:
popBack on an empty tape: two steps, nothing.
theorem
MIPRE.TM.Interp.exec_popBack
{input : Fin 7 → List Sym}
{k : ProgId}
{pc : Fin maxPc}
{m : Sym}
{t : WT}
(hins : instrAt k pc = Instr.popBack m t)
(hpc : ↑pc + 1 < maxPc)
(l : List Sym)
(a : Sym)
(c : Cfg input)
(hq : c.state = at_ k pc)
(hl : Holds (c.workTapes t) (c.workTapePos t - ↑l.length - 1) (l ++ [a]))
(hm : ∀ s ∈ l, s ≠ m)
(hend :
c.workTapes t (c.workTapePos t - ↑l.length - 2) = some m ∨ c.workTapes t (c.workTapePos t - ↑l.length - 2) = none)
:
∃ (c' : Cfg input),
Reach c (l.length + 3) c' [] ∧ c'.state = next_ k pc hpc ∧ Untouched c c' [] [t] ∧ (∀ (q : ℤ), q < c.workTapePos t - ↑l.length - 1 ∨ c.workTapePos t ≤ q → c'.workTapes t q = c.workTapes t q) ∧ BlankFrom (c'.workTapes t) (c.workTapePos t - ↑l.length - 1) (l.length + 1) ∧ c'.workTapePos t = c.workTapePos t - ↑l.length - 1
popBack: from the end pos, with l ++ [a] on pos - |l| - 1 … pos - 1, l free of
m, and the marker or a blank before: erase them, ending at pos - |l| - 1.
The budget and the counter #
A unary tape: n ones from cell 0, blank elsewhere.
Equations
Instances For
theorem
MIPRE.TM.Interp.Unary.pop
{τ : Tape}
{n : ℕ}
(h : Unary τ (n + 1))
:
Unary (Function.update τ (↑n) none) n
theorem
MIPRE.TM.Interp.Unary.push
{τ : Tape}
{n : ℕ}
(h : Unary τ n)
:
Unary (Function.update τ (↑n) (some Sym.one)) (n + 1)
theorem
MIPRE.TM.Interp.exec_charge_one
{input : Fin 7 → List Sym}
{k : ProgId}
{pc : Fin maxPc}
(hins : instrAt k pc = Instr.charge false)
(hpc : ↑pc + 1 < maxPc)
(c : Cfg input)
(hq : c.state = at_ k pc)
{r : ℕ}
(hb : Unary (c.workTapes BUD) (r + 1))
(hpos : c.workTapePos BUD = ↑r + 1)
:
charge: one step left, then a pop per unit; halts on an exhausted budget.