Frame rules for composite machines

Two things a machine built out of sub-machines needs to know: that a sub-machine's Hoare triple still holds once its tapes are embedded in a larger tape space (TM.placeWorkTM_hoareTime_frame), and that a run of bounded length cannot have touched cells far from where its heads started (TM.reachesIn_work_cells_far). The second is what lets a bounded wipe reset an opaque machine's scratch completely.

Main results

• TM.placeWorkTM_hoareTime_frame — a Hoare triple survives tape embedding
• TM.reachesIn_work_cells_far — a t-step run leaves cells beyond head + t alone
• TM.reachesIn_startInvariant — runs preserve Tape.StartInvariant
• TM.seqTM_det — sequential composition is deterministic on its components
• TM.IdlesInput — machines that never move their input head

def Complexity.TM.parkedBlank : Tape

The parked blank tape every scratch tape starts and ends at.

Equations

• Complexity.TM.parkedBlank = (Complexity.Tape.init []).move Complexity.Dir3.right

Embedding a Hoare triple in a larger tape space

A composite machine runs sub-machines that each own a fixed number of work tapes, while carrying persistent state (running values, fuel registers) on tapes those sub-machines never touch. TM.placeWorkTM already gives the exact frame-preserving simulation (placeWorkTM_reachesIn_placeWorkCfg_of_startInvariant); the lemma below turns that into a Hoare-triple-level tool, so each embedding is a single lemma application instead of a fresh reachesIn argument.

theorem Complexity.TM.placeWorkTM_hoareTime_frame {n pre post : ℕ} (tm : TM n) {preSmall postSmall : TapePred n} {b : ℕ} (h : tm.HoareTime preSmall postSmall b) (extras : Fin (pre + n + post) → Tape) (hinv : ∀ (i : Fin (pre + n + post)), ¬placeWorkInMiddle pre n i → (extras i).StartInvariant) (hhead : ∀ (i : Fin (pre + n + post)), ¬placeWorkInMiddle pre n i → 1 ≤ (extras i).head) : (placeWorkTM pre post tm).HoareTime (fun (inp : Tape) (work : Fin (pre + n + post) → Tape) (out : Tape) => preSmall inp (fun (i : Fin n) => work (placeWorkIdx pre post i)) out ∧ ∀ (i : Fin (pre + n + post)), ¬placeWorkInMiddle pre n i → work i = extras i) (fun (inp : Tape) (work : Fin (pre + n + post) → Tape) (out : Tape) => postSmall inp (fun (i : Fin n) => work (placeWorkIdx pre post i)) out ∧ ∀ (i : Fin (pre + n + post)), ¬placeWorkInMiddle pre n i → work i = extras i) b

Placing a Hoare triple. If tm : TM n satisfies a Hoare triple, then placeWorkTM pre post tm satisfies the triple obtained by reindexing tm's work-tape predicate through the middle block, with an arbitrary Parked-style frame (extras) held exactly fixed outside it.

What a bounded run can have disturbed

Resetting an opaque machine's scratch tapes between calls needs to know how far out the machine could possibly have written. Since each head moves by at most one cell per step and a machine only ever writes under its heads, a t-step run leaves every cell beyond head + t exactly as it found it. That is what makes the bounded wipe of TM.resetTapesTM complete rather than merely partial.

theorem Complexity.TM.work_cells_ne_of_step {n : ℕ} {tm : TM n} {c c' : Cfg n tm.Q} (hstep : tm.step c = some c') (i : Fin n) {j : ℕ} (hj : j ≠ (c.work i).head) : (c'.work i).cells j = (c.work i).cells j

One step leaves every work-tape cell other than that tape's own head unchanged: a machine writes only under its heads.

theorem Complexity.TM.reachesIn_work_cells_far {n : ℕ} {tm : TM n} {t : ℕ} {c c' : Cfg n tm.Q} : tm.reachesIn t c c' → ∀ (i : Fin n) (j : ℕ), (c.work i).head + t < j → (c'.work i).cells j = (c.work i).cells j

Cells beyond a work head's maximum reach are never touched.

theorem Complexity.TM.reachesIn_startInvariant {n : ℕ} {tm : TM n} {t : ℕ} {c c' : Cfg n tm.Q} : tm.reachesIn t c c' → c.input.StartInvariant → (∀ (i : Fin n), (c.work i).StartInvariant) → c.output.StartInvariant → c'.input.StartInvariant ∧ (∀ (i : Fin n), (c'.work i).StartInvariant) ∧ c'.output.StartInvariant

The standing left-marker invariant survives an entire run, on every tape.

theorem Complexity.TM.parked_transition {n : ℕ} {inp₀ out₀ : Tape} {W : Fin n → Tape} (hinp : Parked inp₀) (hW : ∀ (i : Fin n), Parked (W i)) (hout : Parked out₀) : transitionInput inp₀ = inp₀ ∧ (fun (i : Fin n) => transitionTape (W i)) = W ∧ transitionTape out₀ = out₀

A fully parked tape frame passes through a combinator seam unchanged — the boundary obligation of TM.seqTM_hoareTime in the common case where every tape is parked on both sides of the seam.

theorem Complexity.TM.seqTM_det {n : ℕ} (m₁ m₂ : TM n) {inp₀ out₀ : Tape} {W₀ W₁ W₂ : Fin n → Tape} {b₁ b₂ : ℕ} (hinp : Parked inp₀) (hout : Parked out₀) (hW₁ : ∀ (i : Fin n), Parked (W₁ i)) (h₁ : m₁.HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = W₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = W₁ ∧ out = out₀) b₁) (h₂ : m₂.HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = W₁ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = W₂ ∧ out = out₀) b₂) : (m₁.seqTM m₂).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = W₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = W₂ ∧ out = out₀) (b₁ + 1 + b₂)

Chaining two fully-determined phases. When each phase pins down the entire tape family and every intermediate tape is parked, sequential composition needs no boundary reasoning at all.

def Complexity.TM.IdlesInput {n : ℕ} (tm : TM n) : Prop

A machine that never moves its real input head off a parked position: its transition function always returns idleDir for the input tape. Machines that read their input from a work tape instead (TM.retargetInput and everything built on it) satisfy this.

Equations

• tm.IdlesInput = ∀ (q : tm.Q) (iHead : Complexity.Γ) (wHeads : Fin n → Complexity.Γ) (oHead : Complexity.Γ), (tm.δ q iHead wHeads oHead).2.2.2.1 = Complexity.TM.idleDir iHead

theorem Complexity.TM.reachesIn_input_eq_of_idlesInput {n : ℕ} {tm : TM n} (hidle : tm.IdlesInput) {t : ℕ} {c c' : Cfg n tm.Q} : tm.reachesIn t c c' → Parked c.input → c'.input = c.input

An input-idling machine preserves a parked real input tape exactly, for any number of steps.

theorem Complexity.TM.startInvariant_initNil : (Tape.init []).StartInvariant

The blank tape satisfies the left-marker invariant.

theorem Complexity.TM.startInvariant_initOfBool (y : List Bool) : (Tape.init (List.map Γ.ofBool y)).StartInvariant

A tape initialized with a Boolean string satisfies the left-marker invariant: Γ.ofBool never produces ▷.