The charged copyTree #
copyTree src (some t) true copies S(v) and pops one budget cell per bit: with a budget
of at least |v| it succeeds (exec_copyTree_charge), otherwise it halts
(exec_copyTree_charge_fail).
theorem
MIPRE.TM.Interp.copyTree_scan_charge
{input : Fin 7 → List Sym}
{k : ProgId}
{pc : Fin maxPc}
{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)
(v : Cost.Data)
(c : Cfg input)
(d r : ℕ)
:
c.state = some { k := k, pc := pc, ph := Phase.p1 } →
1 ≤ d →
Unary (c.workTapes CNT) d →
c.workTapePos CNT = ↑d →
Unary (c.workTapes BUD) r →
c.workTapePos BUD = ↑r →
v.size ≤ r →
Holds (c.workTapes src) (c.workTapePos src) (S v) →
∃ n ≤ 4 * v.size,
∃ (c' : Cfg input),
Reach c n c' [] ∧ c'.state = scanExit k pc hpc d ∧ Untouched c c' [] [src, CNT, t, BUD] ∧ 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 ∧ Unary (c'.workTapes BUD) (r - v.size) ∧ c'.workTapePos BUD = ↑(r - v.size) ∧ DstEff t c c' (S v)
The scan of the charged copy over S(v) from d ≥ 1 pending subtrees and a budget of
r ≥ |v|.
theorem
MIPRE.TM.Interp.exec_copyTree_charge
{input : Fin 7 → List Sym}
{k : ProgId}
{pc : Fin maxPc}
{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)
(v : Cost.Data)
(c : Cfg input)
(hq : c.state = at_ k pc)
(hcnt : Unary (c.workTapes CNT) 0)
(hcp : c.workTapePos CNT = 0)
{r : ℕ}
(hbud : Unary (c.workTapes BUD) r)
(hbp : c.workTapePos BUD = ↑r)
(hr : v.size ≤ r)
(hsrc : Holds (c.workTapes src) (c.workTapePos src) (S v))
:
∃ n ≤ 4 * v.size + 1,
∃ (c' : Cfg input),
Reach c n c' [] ∧ c'.state = next_ k pc hpc ∧ Untouched c c' [] [src, CNT, t, BUD] ∧ c'.workTapes src = c.workTapes src ∧ c'.workTapePos src = c.workTapePos src + ↑v.size ∧ Unary (c'.workTapes CNT) 0 ∧ c'.workTapePos CNT = 0 ∧ Unary (c'.workTapes BUD) (r - v.size) ∧ c'.workTapePos BUD = ↑(r - v.size) ∧ DstEff t c c' (S v)
copyTree src (some t) true with a sufficient budget.
theorem
MIPRE.TM.Interp.copyTree_scan_fail
{input : Fin 7 → List Sym}
{k : ProgId}
{pc : Fin maxPc}
{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)
(v : Cost.Data)
(c : Cfg input)
(d r : ℕ)
:
The scan of the charged copy over S(v) with a budget r < |v| halts silently.
theorem
MIPRE.TM.Interp.exec_copyTree_charge_fail
{input : Fin 7 → List Sym}
{k : ProgId}
{pc : Fin maxPc}
{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)
(v : Cost.Data)
(c : Cfg input)
(hq : c.state = at_ k pc)
(hcnt : Unary (c.workTapes CNT) 0)
(hcp : c.workTapePos CNT = 0)
{r : ℕ}
(hbud : Unary (c.workTapes BUD) r)
(hbp : c.workTapePos BUD = ↑r)
(hr : r < v.size)
(hsrc : Holds (c.workTapes src) (c.workTapePos src) (S v))
:
copyTree src (some t) true with an insufficient budget halts silently.