Carrying the left-marker invariant through a contract

⚠️ Unreviewed by Bolton

Every subroutine that rewinds, parks, or wipes asks its tapes for Tape.StartInvariant: the left marker at cell zero and nowhere else. A run cannot destroy it — TM.reachesIn_startInvariant — but a contract that does not mention it cannot pass it on, and a stage assembled from such contracts is stuck.

The rule below adds it: if a machine's precondition guarantees the invariant, its postcondition may be strengthened by it, for free.

Main results

• TM.HoareTime.startInvariant — a contract carries the left-marker invariant along
• TM.HoareTime.headBound — and a bound on how far its heads can have travelled

theorem Complexity.TM.HoareTime.startInvariant {n : ℕ} {tm : TM n} {pre post : TapePred n} {b : ℕ} (h : tm.HoareTime pre post b) (hpre : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), pre inp work out → inp.StartInvariant ∧ (∀ (i : Fin n), (work i).StartInvariant) ∧ out.StartInvariant) : tm.HoareTime pre (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => post inp work out ∧ inp.StartInvariant ∧ (∀ (i : Fin n), (work i).StartInvariant) ∧ out.StartInvariant) b

A contract carries the left-marker invariant. No machine can put a marker anywhere but cell zero, so a stage whose entry tapes are start-invariant leaves start-invariant tapes behind — which is what the rewinds and wipes downstream ask for.

theorem Complexity.TM.HoareTime.headBound {n : ℕ} {tm : TM n} {pre post : TapePred n} {b : ℕ} (h : tm.HoareTime pre post b) (h₀ : ℕ) (hpre : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), pre inp work out → (∀ (i : Fin n), (work i).head ≤ h₀) ∧ inp.head ≤ h₀ ∧ out.head ≤ h₀) : tm.HoareTime pre (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => post inp work out ∧ (∀ (i : Fin n), (work i).head ≤ h₀ + b) ∧ inp.head ≤ h₀ + b ∧ out.head ≤ h₀ + b) b

A contract bounds where its heads end up. A head moves at most one cell per step, so a stage that starts inside h₀ and runs for b steps ends inside h₀ + b — which is what the rewinds downstream need in order to know how far to scan.