The copyTree routine

Copying (or skipping) a preorder-serialized value: a scan with a unary counter of the pending subtrees on CNT, one more per 1 (a node with two children, itself consumed) and one fewer per 0 (a leaf), finishing when none is pending. The scan from d ≥ 1 pending subtrees over S(v) leaves d - 1 pending (copyTree_scan), finishing when d = 1; the instruction starts with one (exec_copyTree).

def MIPRE.TM.Interp.scanExit (k : ProgId) (pc : Fin maxPc) (hpc : ↑pc + 1 < maxPc) (d : ℕ) : Option Ctl

The control at (k, pc, p1) if d ≠ 1, else at the next instruction.

Equations

• MIPRE.TM.Interp.scanExit k pc hpc d = if d = 1 then MIPRE.TM.Interp.next_ k pc hpc else some { k := k, pc := pc, ph := MIPRE.TM.Interp.Phase.p1 }

structure MIPRE.TM.Interp.DstEff {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: l held from the old head, the rest of the tape kept, the head past l.

• 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.DstEff.trans {input : Fin 7 → List Sym} {t : WT} {c c' c'' : Cfg input} {l l' : List Sym} (h : DstEff t c c' l) (h' : DstEff t c' c'' l') : DstEff t c c'' (l ++ l')

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

theorem MIPRE.TM.Interp.DstEff.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) : DstEff t c c' []

theorem MIPRE.TM.Interp.DstEff.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) : DstEff t c c' [s]

One written symbol.

theorem MIPRE.TM.Interp.copyTree_scan {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {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) (v : Cost.Data) (c : Cfg input) (d : ℕ) : c.state = some { k := k, pc := pc, ph := Phase.p1 } → 1 ≤ d → Unary (c.workTapes CNT) d → c.workTapePos CNT = ↑d → Holds (c.workTapes src) (c.workTapePos src) (S v) → ∃ n ≤ 3 * v.size, ∃ (c' : Cfg input), Reach c n c' [] ∧ c'.state = scanExit k pc hpc d ∧ Untouched c c' [] [src, CNT, t] ∧ c'.workTapes src = c.workTapes src ∧ c'.workTapePos src = c.workTapePos src + ↑v.size ∧ Unary (c'.workTapes CNT) (d - 1) ∧ c'.workTapePos CNT = ↑d - 1 ∧ DstEff t c c' (S v)

The scan of copyTree src (some t) false over S(v) from d ≥ 1 pending subtrees.

theorem MIPRE.TM.Interp.skipTree_scan {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {src : WT} (hins : instrAt k pc = Instr.copyTree src none false) (hpc : ↑pc + 1 < maxPc) (hsc : src ≠ CNT) (v : Cost.Data) (c : Cfg input) (d : ℕ) : c.state = some { k := k, pc := pc, ph := Phase.p1 } → 1 ≤ d → Unary (c.workTapes CNT) d → c.workTapePos CNT = ↑d → Holds (c.workTapes src) (c.workTapePos src) (S v) → ∃ n ≤ 3 * v.size, ∃ (c' : Cfg input), Reach c n c' [] ∧ c'.state = scanExit k pc hpc d ∧ Untouched c c' [] [src, CNT] ∧ c'.workTapes src = c.workTapes src ∧ c'.workTapePos src = c.workTapePos src + ↑v.size ∧ Unary (c'.workTapes CNT) (d - 1) ∧ c'.workTapePos CNT = ↑d - 1

The scan of copyTree src none false (a skip) over S(v) from d ≥ 1 pending subtrees.

theorem MIPRE.TM.Interp.copyTree_start {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {src : WT} {dst : Option WT} {ch : Bool} (hins : instrAt k pc = Instr.copyTree src dst ch) (c : Cfg input) (hq : c.state = at_ k pc) (hcnt : Unary (c.workTapes CNT) 0) (hcp : c.workTapePos CNT = 0) : ∃ (c' : Cfg input), Reach c 1 c' [] ∧ c'.state = some { k := k, pc := pc, ph := Phase.p1 } ∧ Untouched c c' [] [CNT] ∧ Unary (c'.workTapes CNT) 1 ∧ c'.workTapePos CNT = 1

The first phase of copyTree: one pending subtree.

theorem MIPRE.TM.Interp.exec_copyTree {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {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) (v : Cost.Data) (c : Cfg input) (hq : c.state = at_ k pc) (hcnt : Unary (c.workTapes CNT) 0) (hcp : c.workTapePos CNT = 0) (hsrc : Holds (c.workTapes src) (c.workTapePos src) (S v)) : ∃ n ≤ 3 * v.size + 1, ∃ (c' : Cfg input), Reach c n c' [] ∧ c'.state = next_ k pc hpc ∧ Untouched c c' [] [src, CNT, t] ∧ c'.workTapes src = c.workTapes src ∧ c'.workTapePos src = c.workTapePos src + ↑v.size ∧ Unary (c'.workTapes CNT) 0 ∧ c'.workTapePos CNT = 0 ∧ DstEff t c c' (S v)

copyTree src (some t) false: copy S(v) from the head of src to the head of t, in at most 3 |v| + 1 steps.

theorem MIPRE.TM.Interp.exec_skipTree {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} {src : WT} (hins : instrAt k pc = Instr.copyTree src none false) (hpc : ↑pc + 1 < maxPc) (hsc : src ≠ CNT) (v : Cost.Data) (c : Cfg input) (hq : c.state = at_ k pc) (hcnt : Unary (c.workTapes CNT) 0) (hcp : c.workTapePos CNT = 0) (hsrc : Holds (c.workTapes src) (c.workTapePos src) (S v)) : ∃ n ≤ 3 * v.size + 1, ∃ (c' : Cfg input), Reach c n c' [] ∧ c'.state = next_ k pc hpc ∧ Untouched c c' [] [src, CNT] ∧ c'.workTapes src = c.workTapes src ∧ c'.workTapePos src = c.workTapePos src + ↑v.size ∧ Unary (c'.workTapes CNT) 0 ∧ c'.workTapePos CNT = 0

copyTree src none false: skip S(v) on src, in at most 3 |v| + 1 steps.