Replay verdicts as verifiers

Replaying a fixed fair-coin machine on an instance with a string of saved coins, and testing whether the output is [true], is a verifier on encoded pairs (a, w). It runs in linear time and linear space in the encoded pair, because replay itself does (Turing.MultiTapePTM.computableInDegree_runClosedCoins) and the replayed output is no longer than the replay time. Both readings of a time-bounded machine as a verifier use it: the certificate as a computation path of a nondeterministic machine (Cslib.Complexity.exists_verifier_of_mem_NTIME), and the random string of a probabilistic one (Cslib.Complexity.exists_verifier_of_mem_PromiseBPTIME).

Main results

• Turing.MultiTapePTM.computableInO_decide_runClosedCoins: the replay verdict is computable in linear time and space in the encoded pair.
• Turing.MultiTapePTM.computableInPolyTime_decide_runClosedCoins: the replay verdict is polynomial-time.

theorem Turing.MultiTapePTM.computableInO_decide_runClosedCoins {k : ℕ} {State : Type} [Finite State] {α : Type} {enc : α ↪ List Bool} (machine : MultiTapePTM k Bool State) : MultiTapeTM.ComputableInO (fun (p : α × List Bool) => decide (machine.runClosedCoins p.2 (enc p.1) = [true])) (MultiTapeTM.encPair enc MultiTapeTM.encBits) MultiTapeTM.encBool (fun (p : α × List Bool) => ((MultiTapeTM.encPair enc MultiTapeTM.encBits) p).length) fun (p : α × List Bool) => ((MultiTapeTM.encPair enc MultiTapeTM.encBits) p).length

Replay verdicts are linear-time verifiers. Replaying machine on enc a with the saved coins w, and testing whether the output is [true], is computable in linear time and linear space in the encoded pair (a, w).

theorem Turing.MultiTapePTM.computableInPolyTime_decide_runClosedCoins {k : ℕ} {State : Type} [Finite State] {α : Type} {enc : α ↪ List Bool} (machine : MultiTapePTM k Bool State) : MultiTapeTM.ComputableInPolyTime (fun (p : α × List Bool) => decide (machine.runClosedCoins p.2 (enc p.1) = [true])) (MultiTapeTM.encPair enc MultiTapeTM.encBits) MultiTapeTM.encBool

Replay verdicts are polynomial-time verifiers.