Copying a value into virtual-input shape

TM.retargetInputStartedCfg expects the virtual-input work tape in the exact shape (Tape.init (y.map Γ.ofBool)).move Dir3.right — head parked at cell 1. A value produced elsewhere lands with its head past its content, so one more rewind closes the gap.

Main results

• TM.copyToVirtualInputTM — move a value into virtual-input position
• TM.copyToVirtualInputTM_hoareTime — its contract

theorem Complexity.TM.copyToVirtualInput_hoareTime {n : ℕ} (src dst : Fin n) (hne : src ≠ dst) (x : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hsrcHead : (work₀ src).head = 1) (hsrcOut : (work₀ src).HasOutput x) (hsrcParked : Parked (work₀ src)) (hdst : work₀ dst = (Tape.init []).move Dir3.right) (hinp : Parked inp₀) (hout : Parked out₀) (hother : ∀ (i : Fin n), i ≠ src → i ≠ dst → Parked (work₀ i)) : ((copyWorkToWorkTM src dst).seqTM (rewindWorkTM dst)).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₀ ∧ work dst = (Tape.init (List.map Γ.ofBool x)).move Dir3.right ∧ (work src).cells = (work₀ src).cells ∧ (work src).head = x.length + 1 ∧ ∀ (i : Fin n), i ≠ src → i ≠ dst → work i = work₀ i) (2 * x.length + 5)

Copy the value held at src into dst, then rewind dst to cell 1 — the exact shape retargetInputStartedCfg expects of a virtual input. Every tape besides src/dst, the real input, and the real output are held at fixed Parked values throughout.

def Complexity.TM.copyToVirtualInputTM {n : ℕ} (src dst : Fin n) : TM n

Copy a work tape's value into another and park the result at cell 1.

Equations

• Complexity.TM.copyToVirtualInputTM src dst = (Complexity.TM.copyWorkToWorkTM src dst).seqTM (Complexity.TM.rewindWorkTM dst)

theorem Complexity.TM.copyToVirtualInputTM_hoareTime {n : ℕ} (src dst : Fin n) (hne : src ≠ dst) (x : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hsrcHead : (work₀ src).head = 1) (hsrcOut : (work₀ src).HasOutput x) (hsrcParked : Parked (work₀ src)) (hdst : work₀ dst = (Tape.init []).move Dir3.right) (hinp : Parked inp₀) (hout : Parked out₀) (hother : ∀ (i : Fin n), i ≠ src → i ≠ dst → Parked (work₀ i)) : (copyToVirtualInputTM src dst).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₀ ∧ work = Function.update (Function.update work₀ dst ((Tape.init (List.map Γ.ofBool x)).move Dir3.right)) src { head := x.length + 1, cells := (work₀ src).cells } ∧ out = out₀) (2 * x.length + 5)

The copy, with the whole tape family pinned down. The source keeps its cells but ends with its head past the copied value; the destination holds the value parked at cell 1; nothing else moves. This determined form is what TM.seqTM_det chains.