Efficient replay from an encoded input and saved coins

Replay receives an ordinary encoded pair of coins and input. A pair preparer writes both words, a marker enables virtual input, and the saved-coin controller executes the supplied transitions. The final tidy normalization clears the working storage and restores all heads.

Main results

• Turing.MultiTapePTM.computableTidilyInLinearTimeAndSpace_runClosedCoins: deterministic replay has a uniform linear time and space bound in the encoded pair length.

References

Adapted from the cslib crypto branch's MultiTape/Oracle/ReplayInput.lean at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the common machine and the tidy pair calculus.

theorem Turing.MultiTapePTM.computableTidilyInLinearTimeAndSpace_runClosedCoins {k : ℕ} {State : Type} [Finite State] (machine : MultiTapePTM k Bool State) : MultiTapeTM.ComputableTidilyInLinearTimeAndSpace (fun (p : List Bool × List Bool) => machine.runClosedCoins p.1 p.2) (MultiTapeTM.encPair MultiTapeTM.encBits MultiTapeTM.encBits) MultiTapeTM.encBits

Running a fixed machine on a supplied pair of coins and input is tidily computable in linear time and space. The bound charges input preparation, every supplied coin, and final cleanup; it does not assume that the source machine halts.

theorem Turing.MultiTapePTM.computableTidilyInPolyTime_runClosedCoins {k : ℕ} {State : Type} [Finite State] (machine : MultiTapePTM k Bool State) : MultiTapeTM.ComputableTidilyInPolyTime (fun (p : List Bool × List Bool) => machine.runClosedCoins p.1 p.2) (MultiTapeTM.encPair MultiTapeTM.encBits MultiTapeTM.encBits) MultiTapeTM.encBits

The ordinary functional polynomial-time API can invoke saved-coin replay directly.