The input-tape routines

copyUnary, copyInputBits, checkLen and buildAnswer read an input tape from its head to the blank after the input, writing on a work tape; their specifications are by induction on the remaining suffix of the input.

structure MIPRE.TM.Interp.WEff {input : Fin 7 → List Sym} (t : WT) (c c' : Cfg input) (l : List Sym) : Prop

The effect of writing l at the head of t (as in CopyTree.lean).

• holds : Holds (c'.workTapes t) (c.workTapePos t) l
• outside (q : ℤ) : q < c.workTapePos t ∨ c.workTapePos t + ↑l.length ≤ q → c'.workTapes t q = c.workTapes t q
• pos : c'.workTapePos t = c.workTapePos t + ↑l.length

theorem MIPRE.TM.Interp.WEff.trans {input : Fin 7 → List Sym} {t : WT} {c c' c'' : Cfg input} {l l' : List Sym} (h : WEff t c c' l) (h' : WEff t c' c'' l') : WEff t c c'' (l ++ l')

theorem MIPRE.TM.Interp.WEff.cast {input : Fin 7 → List Sym} {t : WT} {c c' : Cfg input} {l l' : List Sym} (h : WEff t c c' l) (e : l = l') : WEff t c c' l'

theorem MIPRE.TM.Interp.moveInputPos_val_one {n : ℕ} (p : Fin (n + 2)) (h : ↑p < n + 1) : ↑(Turing.MultiTapeTM.moveInputPos p 1) = ↑p + 1

theorem MIPRE.TM.Interp.WEff.nil {input : Fin 7 → List Sym} {t : WT} {c c' : Cfg input} (htape : c'.workTapes t = c.workTapes t) (hpos : c'.workTapePos t = c.workTapePos t) : WEff t c c' []

theorem MIPRE.TM.Interp.WEff.single {input : Fin 7 → List Sym} {t : WT} {c c' : Cfg input} {s : Sym} (htape : c'.workTapes t = Function.update (c.workTapes t) (c.workTapePos t) (some s)) (hpos : c'.workTapePos t = c.workTapePos t + 1) : WEff t c c' [s]

copyUnary

theorem MIPRE.TM.Interp.exec_copyUnary {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {j : IT} {dst : WT} (hins : instrAt k pc = Instr.copyUnary j dst) (hpc : ↑pc + 1 < maxPc) (m : ℕ) (c : Cfg input) (q : ℕ) : c.state = at_ k pc → ↑(c.inputPos j) = q + 1 → (input j).length = q + m → ∃ (c' : Cfg input), Reach c (m + 1) c' [] ∧ c'.state = next_ k pc hpc ∧ Untouched c c' [j] [dst] ∧ ↑(c'.inputPos j) = (input j).length + 1 ∧ WEff dst c c' (List.replicate m Sym.one)

From position q + 1 of input j: one 1 per remaining symbol.

copyInputBits

theorem MIPRE.TM.Interp.exec_copyInputBits {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {j : IT} {dst : WT} (hins : instrAt k pc = Instr.copyInputBits j dst) (hpc : ↑pc + 1 < maxPc) (m : ℕ) (c : Cfg input) (q : ℕ) : c.state = at_ k pc → ↑(c.inputPos j) = q + 1 → (input j).length = q + m → ∃ (c' : Cfg input), Reach c (m + 1) c' [] ∧ c'.state = next_ k pc hpc ∧ Untouched c c' [j] [dst] ∧ ↑(c'.inputPos j) = (input j).length + 1 ∧ WEff dst c c' (List.drop q (input j))

From position q + 1 of input j: the remaining symbols.

checkLen

theorem MIPRE.TM.Interp.exec_checkLen {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {j ref : IT} (hins : instrAt k pc = Instr.checkLen j ref) (hpc : ↑pc + 1 < maxPc) (hjr : j ≠ ref) (m : ℕ) (c : Cfg input) (q : ℕ) : c.state = at_ k pc → ↑(c.inputPos j) = q + 1 → ↑(c.inputPos ref) = q + 1 → (input j).length = q + m → q + m ≤ (input ref).length → ∃ (c' : Cfg input), Reach c (m + 1) c' [] ∧ c'.state = next_ k pc hpc ∧ Untouched c c' [j, ref] [] ∧ ↑(c'.inputPos j) = (input j).length + 1 ∧ ↑(c'.inputPos ref) = (input j).length + 1

From position q + 1 on both j and ref, with |j| - q ≤ |ref| - q: both heads advance to the end of j.

buildAnswer

def MIPRE.TM.Interp.boolOf : Sym → Bool

The bit of an input symbol.

Equations

• MIPRE.TM.Interp.boolOf MIPRE.TM.Interp.Sym.one = true
• MIPRE.TM.Interp.boolOf x✝ = false

def MIPRE.TM.Interp.answerBits (l : List Sym) : List Sym

The written form of an answer suffix: S(encode (l.map boolOf)).

Equations

• MIPRE.TM.Interp.answerBits l = MIPRE.TM.Interp.S (MIPRE.Cost.Data.ofList MIPRE.Cost.Data.ofBool (List.map MIPRE.TM.Interp.boolOf l))

theorem MIPRE.TM.Interp.answerBits_nil : answerBits [] = [Sym.zero]

theorem MIPRE.TM.Interp.answerBits_zero (l : List Sym) : answerBits (Sym.zero :: l) = Sym.one :: Sym.zero :: answerBits l

theorem MIPRE.TM.Interp.answerBits_one (l : List Sym) : answerBits (Sym.one :: l) = Sym.one :: Sym.one :: Sym.zero :: Sym.zero :: answerBits l

theorem MIPRE.TM.Interp.exec_buildAnswer {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {j : IT} {dst : WT} (hins : instrAt k pc = Instr.buildAnswer j dst) (hpc : ↑pc + 1 < maxPc) (hbits : ∀ s ∈ input j, s = Sym.zero ∨ s = Sym.one) (m : ℕ) (c : Cfg input) (q : ℕ) : c.state = at_ k pc → ↑(c.inputPos j) = q + 1 → (input j).length = q + m → ∃ n ≤ 4 * m + 1, ∃ (c' : Cfg input), Reach c n c' [] ∧ c'.state = next_ k pc hpc ∧ Untouched c c' [j] [dst] ∧ ↑(c'.inputPos j) = (input j).length + 1 ∧ WEff dst c c' (answerBits (List.drop q (input j)))

From position q + 1 of a bit input j: S(encode) of the remaining bits.