Resetting a list of tapes to blank, content-agnostically

The full reset an opaque machine's scratch needs between calls: park everything (TM.parkAll_hoareTime), rewind every targeted tape to cell 1 (TM.rewindList_hoareTime), then wipe H cells forward from there (TM.wipeLoop_hoareTime). A fuel register disjoint from the targets drives the wipe and is left exactly as it started.

Main results

• TM.resetTapesTM — the composite reset machine
• TM.resetTapesTM_hoareTime / TM.resetTapesTM_hoareTime_of_bounds — its contract

theorem Complexity.TM.resetTapes_hoareTime {n : ℕ} (targets : List (Fin n)) (hnodup : targets.Nodup) (r : Fin n) (hr : r ∉ targets) (H : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hinpSI : inp₀.StartInvariant) (hinpP : Parked inp₀) (hout0 : out₀ = (Tape.init []).move Dir3.right) (hworkSI : ∀ (j : Fin n), j ≠ r → (work₀ j).StartInvariant) (htargetHead : ∀ j ∈ targets, (work₀ j).head ≤ H) (hworkR : work₀ r = regTape H) (hother : ∀ (j : Fin n), j ≠ r → j ∉ targets → Parked (work₀ j)) : ((skipTM.seqTM (bigSeqTM (List.map rewindWorkTM targets))).seqTM ((wipeStepTM targets).forRegTM r)).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ out = out₀ ∧ (∀ j ∈ targets, work j = wipedTape { head := 1, cells := (work₀ j).cells } H) ∧ work r = regTape H ∧ ∀ (j : Fin n), j ≠ r → j ∉ targets → work j = work₀ j) (targets.length * (H + 4) + H * 4 + 8)

Resetting a list of tapes. Regardless of their current content or head position (bounded by H), every tape in targets ends up blanked from cell 1 through cell H, with its tail beyond cell H untouched; the fuel register r (disjoint from targets) and every other tape are exactly as they were.

def Complexity.TM.resetTapesTM {n : ℕ} (targets : List (Fin n)) (r : Fin n) : TM n

The composite reset machine: park everything, rewind the targets, wipe H cells forward, then rewind the targets again.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.TM.resetTapesTM_hoareTime {n : ℕ} (targets : List (Fin n)) (hnodup : targets.Nodup) (r : Fin n) (hr : r ∉ targets) (H : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hinpSI : inp₀.StartInvariant) (hinpP : Parked inp₀) (hout0 : out₀ = (Tape.init []).move Dir3.right) (hworkSI : ∀ (j : Fin n), j ≠ r → (work₀ j).StartInvariant) (htargetHead : ∀ j ∈ targets, (work₀ j).head ≤ H) (htargetFar : ∀ j ∈ targets, ∀ (i : ℕ), H < i → (work₀ j).cells i = Γ.blank) (hworkR : work₀ r = regTape H) (hother : ∀ (j : Fin n), j ≠ r → j ∉ targets → Parked (work₀ j)) : (resetTapesTM targets r).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ out = out₀ ∧ (∀ j ∈ targets, work j = (Tape.init []).move Dir3.right) ∧ work r = regTape H ∧ ∀ (j : Fin n), j ≠ r → j ∉ targets → work j = work₀ j) (targets.length * (H + 4) + H * 4 + 8 + 1 + (targets.length * (H + 4) + 1))

The full reset. Every tape in targets whose content is confined to cells 1 … H — no matter where in that range, and no matter where its head currently sits — ends up literally blank and parked at cell 1. The fuel register r and all other tapes are returned exactly as they were.

theorem Complexity.TM.resetTapesTM_hoareTime_of_bounds {n : ℕ} (targets : List (Fin n)) (hnodup : targets.Nodup) (r : Fin n) (hr : r ∉ targets) (H : ℕ) (inp₀ : Tape) (extras : Fin n → Tape) (out₀ : Tape) (hinpSI : inp₀.StartInvariant) (hinpP : Parked inp₀) (hout0 : out₀ = (Tape.init []).move Dir3.right) (hextraP : ∀ (j : Fin n), j ≠ r → j ∉ targets → Parked (extras j)) : (resetTapesTM targets r).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ out = out₀ ∧ (∀ (j : Fin n), j ≠ r → (work j).StartInvariant) ∧ (∀ j ∈ targets, (work j).head ≤ H ∧ ∀ (i : ℕ), H < i → (work j).cells i = Γ.blank) ∧ work r = regTape H ∧ ∀ (j : Fin n), j ≠ r → j ∉ targets → work j = extras j) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ out = out₀ ∧ (∀ j ∈ targets, work j = (Tape.init []).move Dir3.right) ∧ work r = regTape H ∧ ∀ (j : Fin n), j ≠ r → j ∉ targets → work j = extras j) (targets.length * (H + 4) + H * 4 + 8 + 1 + (targets.length * (H + 4) + 1))

The reset, keyed on bounds rather than on a named tape family. The tapes an opaque machine leaves behind are only known through bounds, never as a closed form, so this is the shape the loop body actually needs: the exact starting family is instantiated inside the proof.