TM Subroutines: proof internals

Simulation lemmas and HoareTime proofs for the rewind, blank, clear, and copy subroutine machines defined in Complexitylib.Models.TuringMachine.Subroutines. Each subroutine gets a basic Hoare-style spec, and where needed a rich "frame" variant that threads an arbitrary predicate P on the untouched tapes through the run.

Main results

• writeTM_hoareTime — writes sym.toΓ to output cell 1
• rewindWorkTM_hoareTime — rewinds work tape idx to cell 1
• rewindWorkTM_hoareTime_frame — work-tape rewind preserving a predicate P
• rewindInputTM_hoareTime — rewinds the input tape to cell 1
• rewindInputTM_hoareTime_frame — input rewind preserving a predicate P
• rewindInputTM_toNTM_hoareTime — NTM-lifted input rewind spec
• rewindInputTM_toNTM_hoareTime_frame — NTM-lifted rich input rewind spec
• blankWorkTM_started_hoareTime — blank a started work tape in linear time
• blankWorkTM_hoareTime_frame_of_binaryString — frame-preserving blank
• clearWorkTM_hoareTime_frame_of_binaryString — blank then rewind to the started empty tape, preserving the frame
• copyInputToWorkTM_started_hoareTime — copy the Boolean input to a work tape
• copyWorkToWorkTM_started_hoareTime — copy one started work tape to another
• copyWorkToWorkTM_hoareTime_frame_of_binaryString — frame-preserving work-to-work copy

theorem Complexity.TM.writeTM_hoareTime {n : ℕ} (sym : Γw) (B : ℕ) : (writeTM sym).HoareTime (fun (x : Tape) (x_1 : Fin n → Tape) (out : Tape) => out.cells 0 = Γ.start ∧ (∀ j ≥ 1, out.cells j ≠ Γ.start) ∧ out.head ≤ B) (fun (x : Tape) (x_1 : Fin n → Tape) (out : Tape) => out.cells 1 = sym.toΓ) (B + 3)

writeTM sym writes sym.toΓ to output cell 1 and halts. Pre: output tape well-formed (cell 0 = ▷, cells ≥ 1 ≠ ▷), head ≤ B. Post: output cell 1 = sym.toΓ. Time: B + 3 steps.

theorem Complexity.TM.rewindWorkTM_hoareTime {n : ℕ} (idx : Fin n) (B : ℕ) : (rewindWorkTM idx).HoareTime (fun (x : Tape) (work : Fin n → Tape) (x_1 : Tape) => (work idx).cells 0 = Γ.start ∧ (∀ j ≥ 1, (work idx).cells j ≠ Γ.start) ∧ (work idx).head ≤ B) (fun (x : Tape) (work : Fin n → Tape) (x_1 : Tape) => (work idx).head = 1) (B + 2)

rewindWorkTM idx rewinds work tape idx to cell 1 and halts. Pre: work tape idx well-formed (cell 0 = ▷, cells ≥ 1 ≠ ▷), head ≤ B. Post: work tape idx head = 1. Time: B + 2 steps.

theorem Complexity.TM.rewindInputTM_hoareTime {n : ℕ} (B : ℕ) : rewindInputTM.HoareTime (fun (inp : Tape) (x : Fin n → Tape) (x_1 : Tape) => inp.cells 0 = Γ.start ∧ (∀ j ≥ 1, inp.cells j ≠ Γ.start) ∧ inp.head ≤ B) (fun (inp : Tape) (x : Fin n → Tape) (x_1 : Tape) => inp.head = 1) (B + 2)

rewindInputTM rewinds the input tape to cell 1 and halts. Pre: input tape well-formed (cell 0 = ▷, cells ≥ 1 ≠ ▷), head ≤ B. Post: input head = 1. Time: B + 2 steps.

theorem Complexity.TM.rewindInputTM_hoareTime_frame {n : ℕ} (B_input : ℕ) {P : Tape → (Fin n → Tape) → Tape → Prop} (hP_preserved : ∀ (inp : Tape) (work : Fin n → Tape) (out inp' : Tape) (work' : Fin n → Tape) (out' : Tape), P inp work out → inp'.cells = inp.cells → inp'.head = 1 → work' = work → out' = out → P inp' work' out') : rewindInputTM.HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp.cells 0 = Γ.start ∧ (∀ j ≥ 1, inp.cells j ≠ Γ.start) ∧ inp.head ≤ B_input ∧ out.read ≠ Γ.start ∧ out.head ≥ 1 ∧ (∀ (i : Fin n), (work i).read ≠ Γ.start ∧ (work i).head ≥ 1) ∧ P inp work out) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp.head = 1 ∧ P inp work out) (B_input + 2)

Rich HoareTime for rewindInputTM that preserves an arbitrary predicate P through the rewind, provided P is stable when the input cells are unchanged and the input head is reset to 1. Work and output tapes are preserved exactly under the usual non-start-under-head side conditions.

theorem Complexity.TM.rewindInputTM_toNTM_hoareTime {n : ℕ} (B : ℕ) : rewindInputTM.toNTM.HoareTime (fun (inp : Tape) (x : Fin n → Tape) (x_1 : Tape) => inp.cells 0 = Γ.start ∧ (∀ j ≥ 1, inp.cells j ≠ Γ.start) ∧ inp.head ≤ B) (fun (inp : Tape) (x : Fin n → Tape) (x_1 : Tape) => inp.head = 1) (B + 2)

Nondeterministic form of rewindInputTM_hoareTime, for phase compositions that run deterministic setup subroutines through TM.toNTM.

theorem Complexity.TM.rewindInputTM_toNTM_hoareTime_frame {n : ℕ} (B_input : ℕ) {P : Tape → (Fin n → Tape) → Tape → Prop} (hP_preserved : ∀ (inp : Tape) (work : Fin n → Tape) (out inp' : Tape) (work' : Fin n → Tape) (out' : Tape), P inp work out → inp'.cells = inp.cells → inp'.head = 1 → work' = work → out' = out → P inp' work' out') : rewindInputTM.toNTM.HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp.cells 0 = Γ.start ∧ (∀ j ≥ 1, inp.cells j ≠ Γ.start) ∧ inp.head ≤ B_input ∧ out.read ≠ Γ.start ∧ out.head ≥ 1 ∧ (∀ (i : Fin n), (work i).read ≠ Γ.start ∧ (work i).head ≥ 1) ∧ P inp work out) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp.head = 1 ∧ P inp work out) (B_input + 2)

Nondeterministic form of rewindInputTM_hoareTime_frame.

theorem Complexity.TM.rewindWorkTM_hoareTime_frame {n : ℕ} (idx : Fin n) (B_tape : ℕ) {P : Tape → (Fin n → Tape) → Tape → Prop} (hP_preserved : ∀ (inp : Tape) (work : Fin n → Tape) (out inp' : Tape) (work' : Fin n → Tape) (out' : Tape), P inp work out → (work' idx).cells = (work idx).cells → (work' idx).head = 1 → (∀ (i : Fin n), i ≠ idx → work' i = work i) → inp' = inp → out'.cells = out.cells → out'.head = out.head → P inp' work' out') : (rewindWorkTM idx).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => (work idx).cells 0 = Γ.start ∧ (∀ j ≥ 1, (work idx).cells j ≠ Γ.start) ∧ (work idx).head ≤ B_tape ∧ inp.read ≠ Γ.start ∧ out.read ≠ Γ.start ∧ out.head ≥ 1 ∧ (∀ (i : Fin n), i ≠ idx → (work i).read ≠ Γ.start ∧ (work i).head ≥ 1) ∧ P inp work out) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => (work idx).head = 1 ∧ P inp work out) (B_tape + 2)

Rich HoareTime for rewindWorkTM that preserves an arbitrary predicate P through the rewind, provided P depends on cells (not heads) of the target tape. This is the key tool for threading invariants (e.g., simulation state, encoded data) through rewind steps in seqTM compositions.

The caller provides hP_preserved showing that P is stable under:

• target tape cells unchanged, head set to 1
• all other work tapes unchanged
• input and output unchanged

theorem Complexity.TM.blankWorkTM_started_hoareTime {n : ℕ} (idx : Fin n) (x : List Bool) : (blankWorkTM idx).HoareTime (fun (_inp : Tape) (work : Fin n → Tape) (_out : Tape) => work idx = (Tape.init (List.map Γ.ofBool x)).move Dir3.right) (fun (_inp : Tape) (work : Fin n → Tape) (_out : Tape) => (work idx).head = x.length + 1 ∧ (work idx).cells 0 = Γ.start ∧ ∀ (i : ℕ), (work idx).cells (i + 1) = Γ.blank) (x.length + 1)

If work tape idx holds a started Boolean string x, then blankWorkTM idx clears that tape in |x| + 1 steps and leaves the head at the first blank cell after the erased string.

theorem Complexity.TM.blankWorkTM_hoareTime_frame_of_binaryString {n : ℕ} (idx : Fin n) (x : List Bool) {P : Tape → (Fin n → Tape) → Tape → Prop} (hP_preserved : ∀ (inp : Tape) (work : Fin n → Tape) (out inp' : Tape) (work' : Fin n → Tape) (out' : Tape), P inp work out → (work' idx).head = x.length + 1 → (work' idx).cells 0 = Γ.start → (∀ (i : ℕ), (work' idx).cells (i + 1) = Γ.blank) → inp' = inp → out' = out → (∀ (i : Fin n), i ≠ idx → work' i = work i) → P inp' work' out') : (blankWorkTM idx).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => work idx = (Tape.init (List.map Γ.ofBool x)).move Dir3.right ∧ inp.read ≠ Γ.start ∧ out.read ≠ Γ.start ∧ out.head ≥ 1 ∧ (∀ (i : Fin n), i ≠ idx → (work i).read ≠ Γ.start ∧ (work i).head ≥ 1) ∧ P inp work out) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => (work idx).head = x.length + 1 ∧ (work idx).cells 0 = Γ.start ∧ (∀ (i : ℕ), (work idx).cells (i + 1) = Γ.blank) ∧ P inp work out) (x.length + 1)

Rich HoareTime for blankWorkTM: erase a started Boolean work tape while preserving arbitrary frame data on the input tape, output tape, and all other work tapes. This is the form needed to recycle a staged work tape inside a larger verifier pipeline.

theorem Complexity.TM.clearWorkTM_hoareTime_frame_of_binaryString {n : ℕ} (idx : Fin n) (x : List Bool) {P : Tape → (Fin n → Tape) → Tape → Prop} (hP_preserved : ∀ (inp : Tape) (work : Fin n → Tape) (out inp' : Tape) (work' : Fin n → Tape) (out' : Tape), P inp work out → work' idx = (Tape.init []).move Dir3.right → inp' = inp → out' = out → (∀ (i : Fin n), i ≠ idx → work' i = work i) → P inp' work' out') : (clearWorkTM idx).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => work idx = (Tape.init (List.map Γ.ofBool x)).move Dir3.right ∧ inp.read ≠ Γ.start ∧ out.read ≠ Γ.start ∧ out.head ≥ 1 ∧ (∀ (i : Fin n), i ≠ idx → (work i).read ≠ Γ.start ∧ (work i).head ≥ 1) ∧ P inp work out) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => work idx = (Tape.init []).move Dir3.right ∧ P inp work out) (x.length + 1 + 1 + (x.length + 1 + 2))

Rich HoareTime for clearWorkTM: erase a started Boolean work tape and rewind it to the standard started blank tape while preserving the external frame. The user predicate only needs to be stable once the target tape has reached the final started blank configuration.

theorem Complexity.TM.copyInputToWorkTM_started_hoareTime {n : ℕ} (idx : Fin n) (x : List Bool) : (copyInputToWorkTM idx).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (_out : Tape) => inp = (Tape.init (List.map Γ.ofBool x)).move Dir3.right ∧ (work idx).HasBinaryPrefix []) (fun (inp : Tape) (work : Fin n → Tape) (_out : Tape) => inp.cells = (Tape.init (List.map Γ.ofBool x)).cells ∧ inp.head = x.length + 1 ∧ (work idx).HasBinaryPrefix x) (x.length + 1)

copyInputToWorkTM idx can be started with the input and target work tape already positioned at cell 1: it copies the entire Boolean input to a binary prefix on work tape idx and halts within |x| + 1 steps.

theorem Complexity.TM.copyWorkToWorkTM_started_hoareTime {n : ℕ} (src dst : Fin n) (hne : src ≠ dst) (x : List Bool) : (copyWorkToWorkTM src dst).HoareTime (fun (_inp : Tape) (work : Fin n → Tape) (_out : Tape) => work src = (Tape.init (List.map Γ.ofBool x)).move Dir3.right ∧ (work dst).HasBinaryPrefix []) (fun (_inp : Tape) (work : Fin n → Tape) (_out : Tape) => (work src).cells = (Tape.init (List.map Γ.ofBool x)).cells ∧ (work src).head = x.length + 1 ∧ (work dst).HasBinaryPrefix x) (x.length + 1)

If src holds a started Boolean string x and dst is a started blank work tape, then copyWorkToWorkTM src dst copies x onto dst within |x| + 1 steps. The source contents are preserved, while its head advances to the first blank cell after the copied data.

theorem Complexity.TM.copyWorkToWorkTM_hoareTime_frame_of_binaryString {n : ℕ} (src dst : Fin n) (hne : src ≠ dst) (x : List Bool) {P : Tape → (Fin n → Tape) → Tape → Prop} (hP_preserved : ∀ (inp : Tape) (work : Fin n → Tape) (out inp' : Tape) (work' : Fin n → Tape) (out' : Tape), P inp work out → (work' src).cells = (Tape.init (List.map Γ.ofBool x)).cells → (work' src).head = x.length + 1 → (work' dst).HasBinaryPrefix x → (work' dst).cells 0 = Γ.start → inp' = inp → out' = out → (∀ (i : Fin n), i ≠ src → i ≠ dst → work' i = work i) → P inp' work' out') : (copyWorkToWorkTM src dst).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => work src = (Tape.init (List.map Γ.ofBool x)).move Dir3.right ∧ work dst = (Tape.init []).move Dir3.right ∧ inp.read ≠ Γ.start ∧ out.read ≠ Γ.start ∧ out.head ≥ 1 ∧ (∀ (i : Fin n), i ≠ src → i ≠ dst → (work i).read ≠ Γ.start ∧ (work i).head ≥ 1) ∧ P inp work out) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => (work src).cells = (Tape.init (List.map Γ.ofBool x)).cells ∧ (work src).head = x.length + 1 ∧ (work dst).HasBinaryPrefix x ∧ (work dst).cells 0 = Γ.start ∧ P inp work out) (x.length + 1)

Rich HoareTime for copyWorkToWorkTM: copy a started Boolean work tape to another started blank work tape while preserving arbitrary frame data on the input tape, output tape, and all unrelated work tapes. The source cells are preserved while its head advances to the first blank after the copied string, and the destination accumulates the copied prefix without losing its left-end marker.