Space-aware Hoare specifications

TM.HoareSpace states the all-reachable auxiliary-space invariant required by TM.ComputesInSpace; TM.HoareTimeSpace pairs it with a terminating time-bounded Hoare triple. The public API includes structural rules, sequential composition, transducer closure, and a fresh-start computation bridge.

Main results

• TM.HoareTimeSpace.consequence — weaken/strengthen every contract component.
• TM.HoareSpace.weaken_pre, TM.HoareSpace.mono — structural space rules.
• Cfg.WithinAuxSpace.reachesIn — bound head growth along a concrete run.
• TM.HoareTime.and_hoareSpace — pair existing endpoint and safety proofs.
• TM.HoareTime.toHoareTimeSpace — derive all-reachable space from time and an initial head bound.
• TM.seqTM_hoareTimeSpace — compose two phases at one space budget.
• TM.IsTransducer.seqTM — sequential composition remains append-only.
• TM.computesInSpace_of_hoareTimeSpace — package per-input contracts.

theorem Complexity.Cfg.WithinAuxSpace.mono {n : ℕ} {Q : Type} {c : Cfg n Q} {inputLength inputLength' space space' : ℕ} (h : c.WithinAuxSpace inputLength space) (hinput : inputLength ≤ inputLength') (hspace : space ≤ space') : c.WithinAuxSpace inputLength' space'

Enlarging the logical input region and work-space budget preserves an auxiliary-space bound.

theorem Complexity.Cfg.WithinAuxSpace.transition {n : ℕ} {Q : Type} {c : Cfg n Q} {inputLength space : ℕ} (h : c.WithinAuxSpace inputLength space) : { state := c.state, input := TM.transitionInput c.input, work := fun (i : Fin n) => TM.transitionTape (c.work i), output := TM.transitionTape c.output }.WithinAuxSpace inputLength (space + 1)

The standard combinator phase transition moves input and work heads by at most one, so one additional auxiliary-space cell covers the seam.

theorem Complexity.Cfg.WithinAuxSpace.reachesIn {n : ℕ} {tm : TM n} {c c' : Cfg n tm.Q} {time inputLength space : ℕ} (h : c.WithinAuxSpace inputLength space) (hreach : tm.reachesIn time c c') : c'.WithinAuxSpace inputLength (space + time)

A time-step run can increase every charged head position by at most time, so adding that many cells preserves the auxiliary-space bound.

theorem Complexity.TM.HoareSpace.weaken_pre {n : ℕ} {tm : TM n} {pre pre' : TapePred n} {inputLength space : ℕ} (h : tm.HoareSpace pre inputLength space) (hpre : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), pre' inp work out → pre inp work out) : tm.HoareSpace pre' inputLength space

Strengthening the precondition preserves an all-reachable space contract.

theorem Complexity.TM.HoareSpace.mono {n : ℕ} {tm : TM n} {pre : TapePred n} {inputLength inputLength' space space' : ℕ} (h : tm.HoareSpace pre inputLength space) (hinput : inputLength ≤ inputLength') (hspace : space ≤ space') : tm.HoareSpace pre inputLength' space'

Enlarging the logical input region and auxiliary-space budget preserves a space contract.

theorem Complexity.TM.HoareTime.and_hoareSpace {n : ℕ} {tm : TM n} {pre post : TapePred n} {time inputLength space : ℕ} (htime : tm.HoareTime pre post time) (hspace : tm.HoareSpace pre inputLength space) : tm.HoareTimeSpace pre post time inputLength space

Pair an existing terminating Hoare proof with an all-reachable space proof. This is the main entry point for upgrading established subroutine contracts without reproving their endpoint behavior.

theorem Complexity.TM.HoareTime.toHoareTimeSpace {n : ℕ} {tm : TM n} {pre post : TapePred n} {time inputLength initialSpace : ℕ} (htime : tm.HoareTime pre post time) (hinitial : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), pre inp work out → { state := tm.qstart, input := inp, work := work, output := out }.WithinAuxSpace inputLength initialSpace) : tm.HoareTimeSpace pre post time inputLength (initialSpace + time)

Upgrade a terminating time-bounded Hoare triple to an all-reachable time-and-space contract. If every starting configuration fits in initialSpace, then at most one additional cell per machine step gives the uniform bound initialSpace + time.

theorem Complexity.TM.HoareTimeSpace.toHoareTime {n : ℕ} {tm : TM n} {pre post : TapePred n} {time inputLength space : ℕ} (h : tm.HoareTimeSpace pre post time inputLength space) : tm.HoareTime pre post time

A time-and-space contract exposes its ordinary time-bounded Hoare triple.

theorem Complexity.TM.HoareTimeSpace.toHoareSpace {n : ℕ} {tm : TM n} {pre post : TapePred n} {time inputLength space : ℕ} (h : tm.HoareTimeSpace pre post time inputLength space) : tm.HoareSpace pre inputLength space

A time-and-space contract exposes its all-reachable space component.

theorem Complexity.TM.HoareTimeSpace.consequence {n : ℕ} {tm : TM n} {pre pre' post post' : TapePred n} {time time' inputLength inputLength' space space' : ℕ} (h : tm.HoareTimeSpace pre post time inputLength space) (hpre : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), pre' inp work out → pre inp work out) (hpost : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), post inp work out → post' inp work out) (htime : time ≤ time') (hinput : inputLength ≤ inputLength') (hspace : space ≤ space') : tm.HoareTimeSpace pre' post' time' inputLength' space'

Consequence rule: strengthen the precondition, weaken the postcondition, and enlarge any of the three numerical bounds.

theorem Complexity.TM.IsTransducer.seqTM {n : ℕ} {tm₁ tm₂ : TM n} (h₁ : tm₁.IsTransducer) (h₂ : tm₂.IsTransducer) : (tm₁.seqTM tm₂).IsTransducer

Sequentially composing one-way-output machines preserves the transducer discipline.

theorem Complexity.TM.seqTM_hoareTimeSpace {n : ℕ} (tm₁ tm₂ : TM n) {pre mid mid' post : TapePred n} {b₁ b₂ inputLength space₁ space₂ : ℕ} (h₁ : tm₁.HoareTimeSpace pre mid b₁ inputLength space₁) (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₂.HoareTimeSpace mid' post b₂ inputLength space₂) : (tm₁.seqTM tm₂).HoareTimeSpace pre post (b₁ + 1 + b₂) inputLength (max space₁ space₂)

Sequential composition of time-and-space Hoare contracts.

theorem Complexity.TM.computesInSpace_of_hoareTimeSpace {n : ℕ} {tm : TM n} {f : List Bool → List Bool} {T S : ℕ → ℕ} (htrans : tm.IsTransducer) (h : ∀ (x : List Bool), tm.HoareTimeSpace (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = Tape.init (List.map Γ.ofBool x) ∧ (work = fun (x : Fin n) => Tape.init []) ∧ out = Tape.init []) (fun (x_1 : Tape) (x_2 : Fin n → Tape) (out : Tape) => out.HasOutput (f x)) (T x.length) x.length (S x.length)) : tm.ComputesInSpace f S

Per-input fresh-start time-and-space contracts package a total function transducer satisfying TM.ComputesInSpace.