Preparing saved coins and a buffered input

Both closed and external-oracle replay decode an encoded pair onto disjoint tapes. The first word supplies saved coins; the second becomes the virtual input, with a separate boundary marker. These helpers describe the same deterministic preparation independently of the replay controller.

Main definitions

• Turing.MultiTapeTM.ReplayInput.prepareTapes: reserve disjoint source and preparation tapes.
• Turing.MultiTapeTM.ReplayInput.words: prepared coins and input before marking the boundary.

Main results

• Turing.MultiTapeTM.ReplayInput.runFrom_prepare: the pair preparer's full machine execution.
• Turing.MultiTapeTM.ReplayInput.runFrom_mark: the two-step virtual-input boundary marker.

References

Extracted from MultiTape.Probabilistic.ReplayInput, adapted there from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

def Turing.MultiTapeTM.ReplayInput.prepareTapes (k r : ℕ) : Fin (r + 2) ↪ Fin (k + r + 3)

Reserve source tapes before pair preparation and a boundary-marker tape after it.

def Turing.MultiTapeTM.ReplayInput.words (k r : ℕ) (coins input : List Bool) : Fin (k + r + 3) → List Bool

The two prepared words, with blank source, scratch and boundary tapes.

def Turing.MultiTapeTM.ReplayInput.initial {Q : Type} (k r : ℕ) (coins input : List Bool) (q : Option Q) : Cfg (k + r + 1) Bool Q input

An initial source tape configuration with the saved coins on its last work tape.

theorem Turing.MultiTapeTM.ReplayInput.words_eq (k r : ℕ) (coins input : List Bool) : words k r coins input = Fin.append (Fin.snoc (fun (x : Fin (k + r)) => []) coins) ![input, []]

Separate the source and saved-coin tapes from the virtual input and boundary marker.

theorem Turing.MultiTapeTM.ReplayInput.runFrom_mark {k r : ℕ} (coins input outer : List Bool) : runFrom (wordsCfg outer (some (markWork Bool (some true)).q₀) (words k r coins input) []) 2 = inCfg true (initial k r coins input none) outer

Two instructions prepare the virtual-input boundary marker.

theorem Turing.MultiTapeTM.ReplayInput.runFrom_prepare {k r : ℕ} {PrepareState : Type} (prepare : MultiTapeTM (r + 2) Bool PrepareState) (coins input outer : List Bool) (t s : ℕ) (h : prepare.TransformsTapes (fun (inp : List Bool) (ws : Fin (r + 2) → List Bool) => inp = outer ∧ ws = fun (x : Fin (r + 2)) => []) (fun (x : List Bool) (x_1 ws' : Fin (r + 2) → List Bool) (emitted : List Bool) => ws' = Fin.append (fun (x : Fin r) => []) ![coins, input] ∧ emitted = []) t s) : runFrom ((prepare.extendTapes (prepareTapes k r)).initCfg outer) t = wordsCfg outer none (words k r coins input) []

Pair preparation reaches its exact output words on the reserved tapes.