A deterministic controller for saved-coin replay

The controller reads the supplied coins from a fresh last work tape. Each stored bit supplies one source instruction. After the source halts, only the coin head continues moving; the first blank coin cell halts the controller. Thus a tape of t coins takes exactly t + 1 transitions, even if the source does not halt within its supplied clock.

This module accounts for execution from preloaded tapes. Writing the coins and preparing the input are separate machine computations, not free initial data in a complexity certificate.

Main definitions

• Turing.MultiTapePTM.replay: deterministic replay with one additional read-only work tape.

Main results

• Turing.MultiTapePTM.runFrom_replay: agreement with fixed-coin execution and actual halting.

References

Adapted from the cslib crypto branch's Oracle/Replay.lean at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the common closed machine directly.

def Turing.MultiTapePTM.Replay.config {k : ℕ} {State : Type} {input : List Bool} (cfg : MultiTapeMachine.Config k Bool State Empty input) (tape : ℤ → Option Bool) (position : ℤ) : Cfg (k + 1) Bool (Option State) input

Add a read-only coin tape, keeping the source's possibly halted state in live control.

def Turing.MultiTapePTM.Replay.idle {k : ℕ} {State : Type} (next : Option (Option State)) (move : SignType) : Action (k + 1) Bool (Option State)

Move only the coin head and update the controller.

def Turing.MultiTapePTM.Replay.liftAction {k : ℕ} {State : Type} (action : Action k Bool State) : Action (k + 1) Bool (Option State)

Simulate an ordinary source action while advancing the coin head.

def Turing.MultiTapePTM.Replay.stopped {k : ℕ} {State : Type} {input : List Bool} (cfg : MultiTapeMachine.Config k Bool State Empty input) (tape : ℤ → Option Bool) (position : ℤ) : Cfg (k + 1) Bool (Option State) input

Stop the controller without changing any tape or head.

theorem Turing.MultiTapePTM.Replay.apply_liftAction {k : ℕ} {State : Type} {input : List Bool} (cfg : MultiTapeMachine.Config k Bool State Empty input) (tape : ℤ → Option Bool) (position : ℤ) (action : Action k Bool State) (symbol : Empty → Option Bool) (move : Empty → SignType) : (liftAction action).apply (config cfg tape position) = config (cfg.step action symbol move) tape (position + 1)

A lifted action updates the source tapes and consumes one stored coin.

theorem Turing.MultiTapePTM.Replay.apply_tick {k : ℕ} {State : Type} {input : List Bool} (cfg : MultiTapeMachine.Config k Bool State Empty input) (tape : ℤ → Option Bool) (position : ℤ) : (idle (some cfg.tapes.state) 1).apply (config cfg tape position) = config cfg tape (position + 1)

Once the source halts, only the saved-coin head moves.

theorem Turing.MultiTapePTM.Replay.apply_stop {k : ℕ} {State : Type} {input : List Bool} (cfg : MultiTapeMachine.Config k Bool State Empty input) (tape : ℤ → Option Bool) (position : ℤ) : (idle none 0).apply (config cfg tape position) = stopped cfg tape position

Halting preserves every tape and head position.

@[simp]

theorem Turing.MultiTapePTM.Replay.config_inputSymbol {k : ℕ} {State : Type} {input : List Bool} (cfg : MultiTapeMachine.Config k Bool State Empty input) (tape : ℤ → Option Bool) (position : ℤ) : (config cfg tape position).inputSymbol = cfg.tapes.inputSymbol

@[simp]

theorem Turing.MultiTapePTM.Replay.config_workTapeSymbols_castSucc {k : ℕ} {State : Type} {input : List Bool} (cfg : MultiTapeMachine.Config k Bool State Empty input) (tape : ℤ → Option Bool) (position : ℤ) (i : Fin k) : (config cfg tape position).workTapeSymbols i.castSucc = cfg.tapes.workTapeSymbols i

@[simp]

theorem Turing.MultiTapePTM.Replay.config_workTapeSymbols_last {k : ℕ} {State : Type} {input : List Bool} (cfg : MultiTapeMachine.Config k Bool State Empty input) (tape : ℤ → Option Bool) (position : ℤ) : (config cfg tape position).workTapeSymbols (Fin.last k) = tape position

def Turing.MultiTapePTM.replay {k : ℕ} {State : Type} (machine : MultiTapePTM k Bool State) : MultiTapeTM (k + 1) Bool (Option State)

A deterministic replay controller. Its control is finite whenever the source control is.

theorem Turing.MultiTapePTM.Replay.step_some {k : ℕ} {State : Type} {input : List Bool} (machine : MultiTapePTM k Bool State) (cfg : MultiTapeMachine.Config k Bool State Empty input) (tape : ℤ → Option Bool) (position : ℤ) (bit : Bool) (hcell : tape position = some bit) : MultiTapeTM.step (config cfg tape position) = config ((machine.withCoin bit).step cfg) tape (position + 1)

An available coin supplies exactly one deterministic source transition.

theorem Turing.MultiTapePTM.Replay.step_none {k : ℕ} {State : Type} {input : List Bool} (machine : MultiTapePTM k Bool State) (cfg : MultiTapeMachine.Config k Bool State Empty input) (tape : ℤ → Option Bool) (position : ℤ) (hcell : tape position = none) : MultiTapeTM.step (config cfg tape position) = stopped cfg tape position

The first blank saved-coin cell halts the controller.

theorem Turing.MultiTapePTM.Replay.runFrom_coins {k : ℕ} {State : Type} {input : List Bool} (machine : MultiTapePTM k Bool State) (cfg : MultiTapeMachine.Config k Bool State Empty input) (coins : List Bool) (tape : ℤ → Option Bool) (position : ℤ) (hcoins : ∀ i < coins.length, tape (position + ↑i) = coins[i]?) (hstop : tape (position + ↑coins.length) = none) : MultiTapeTM.runFrom (config cfg tape position) (coins.length + 1) = stopped (machine.runClosedConfigFromCoins coins cfg) tape (position + ↑coins.length)

Replay a stored sequence starting at any coin position. The source may halt early or remain live when the supplied sequence ends; the controller reaches the following blank in either case.

theorem Turing.MultiTapePTM.runFrom_replay {k : ℕ} {State : Type} (machine : MultiTapePTM k Bool State) (coins input : List Bool) : MultiTapeTM.runFrom (Replay.config (MultiTapeMachine.initialConfig machine input) (tapeOfList coins) 0) (coins.length + 1) = Replay.stopped (machine.runClosedConfigFromCoins coins (MultiTapeMachine.initialConfig machine input)) (tapeOfList coins) ↑coins.length

From preloaded coins and blank source tapes, replay agrees with the fixed-coin interpreter and halts in the number of coins plus one transitions.