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.computableInLinearTimeAndSpace_runClosedCoins: deterministic replay is linear-time and linear-work-space in the encoded coins/input pair.
• Turing.MultiTapePTM.computableInPolyTime_runClosedCoins: deterministic replay is polynomial-time.

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.computableInLinearTimeAndSpace_runClosedCoins {k : ℕ} {State : Type} [Finite State] (machine : MultiTapePTM k Bool State) : MultiTapeTM.ComputableInLinearTimeAndSpace (fun (p : List Bool × List Bool) => machine.runClosedCoins p.1 p.2) (MultiTapeTM.encPair MultiTapeTM.encBits MultiTapeTM.encBits) MultiTapeTM.encBits

Saved-coin replay retains linear time and linear workspace in the encoded coins/input pair.

theorem Turing.MultiTapePTM.computableInPolyTime_runClosedCoins {k : ℕ} {State : Type} [Finite State] (machine : MultiTapePTM k Bool State) : MultiTapeTM.ComputableInPolyTime (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 computable in polynomial time.