Compositional tape safety

Use the existing TM.HoareTime for endpoints and time. This module adds only state-independent safety and its sequential-composition rule, so resource predicates may include output and exclude an external witness stream.

theorem Complexity.TM.HoareSafety.consequence {n : ℕ} {M : TM n} {pre pre' safe safe' : TapePred n} (h : M.HoareSafety pre safe) (hpre : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), pre' inp work out → pre inp work out) (hsafe : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), safe inp work out → safe' inp work out) : M.HoareSafety pre' safe'

Strengthen the entry condition and weaken the safety conclusion.

theorem Complexity.TM.seqTM_hoareSafety {n : ℕ} (tm₁ tm₂ : TM n) {pre mid mid' post safe : TapePred n} {b₁ b₂ : ℕ} (h₁ : tm₁.HoareTime pre mid b₁) (htrans : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), mid inp work out → mid' (transitionInput inp) (fun (i : Fin n) => transitionTape (work i)) (transitionTape out)) (h₂ : tm₂.HoareTime mid' post b₂) (hs₁ : tm₁.HoareSafety pre safe) (hs₂ : tm₂.HoareSafety mid' safe) : (tm₁.seqTM tm₂).HoareSafety pre safe

A terminating sequential pipeline preserves a common safety predicate. The handoff is covered by the second phase's reflexive safety obligation.