Canonical replay of oracle occurrence traces

Replay follows the existing native instructions and makes their actual buffered oracle calls. A fixed-length certificate contains one occurrence index per live instruction, followed only by zeros after the first halt. Those padding zeros are not recorded as transitions. Exhausting a certificate at a live configuration retains that configuration; terminal filtering is separate.

Main definitions

• Turing.MultiTapeMachine.indexWords: chronological fixed-length index enumeration.
• Turing.MultiTapeMachine.replayIndices: actual word-query replay with canonical padding.
• Turing.MultiTapeMachine.replayResult: retain successful replay and its final private state.
• Turing.MultiTapeMachine.replayTerminal: terminal observation, excluding live cutoffs.

Main results

• Turing.MultiTapeMachine.filterMap_replayResult: exact ordered enumeration of native runs.
• Turing.MultiTapeMachine.countP_replayResult_terminal: equality of terminal verdict counts.
• Turing.MultiTapeMachine.runOccurrenceTrace_empty: raw closed-run compatibility.
• Turing.MultiTapeMachine.replayTerminal_empty: the existing closed certificate decoder.

All replayed certificates start with the same external state. Different certificates may reach equal configurations, but distinct consumed indices and their List multiplicities are retained. The explicit positive arity bound concerns list lengths, not the number of distinct actions. No nonblocking, halting or encoded polynomial-time conclusion is implicit. This is a semantic replay program, not yet a certified efficient binary checker. The query and reply cost boundary are stated in MultiTape.Counting.Oracle.Program.

References

Reuses the existing occurrence certificates in MultiTape.Counting.Certificate and the native program and List interpretation in MultiTape.Counting.Oracle.Program; their formalization and mathematical source credits apply here. The stateful word interface is explicitly more general than the language-oracle interface in [For97], Section 2 and Definition 3.1.

def Turing.MultiTapeMachine.indexWords (bound : ℕ) : ℕ → List (List ℕ)

Enumerate fixed-width index words in chronological order: the current digit is outermost. Generating all bound ^ fuel words is not asserted to take polynomial time in fuel.

theorem Turing.MultiTapeMachine.mem_indexWords (bound fuel : ℕ) (word : List ℕ) : word ∈ indexWords bound fuel ↔ word.length = fuel ∧ ∀ index ∈ word, index < bound

The enumeration contains exactly the words of the required length and digit range.

theorem Turing.MultiTapeMachine.nodup_indexWords (bound fuel : ℕ) : (indexWords bound fuel).Nodup

Each fixed-length index word occurs once.

def Turing.MultiTapeMachine.replayIndicesFrom {k : ℕ} {Symbol Control Operation : Type} [DecidableEq Operation] {input : List Symbol} (machine : MultiTapeMachine k Symbol Control Operation List) : Config k Symbol Control Operation input → List ℕ → List ℕ → Cslib.OracleComp (fun (x : Operation × List Symbol) => List Symbol) (Option (List ℕ × Config k Symbol Control Operation input))

Replay after an already recorded trace; newly consumed indices are appended to it. The trace is an observer and does not alter the native machine configuration.

def Turing.MultiTapeMachine.replayIndices {k : ℕ} {Symbol Control Operation : Type} [DecidableEq Operation] {input : List Symbol} (machine : MultiTapeMachine k Symbol Control Operation List) (cfg : Config k Symbol Control Operation input) (word : List ℕ) : Cslib.OracleComp (fun (x : Operation × List Symbol) => List Symbol) (Option (List ℕ × Config k Symbol Control Operation input))

Replay real instructions, rejecting invalid indices and nonzero padding after halting. At exhaustion a live endpoint is retained. Only live instructions enter the consumed trace.

def Turing.MultiTapeMachine.replayResult {k : ℕ} {Symbol Control Operation : Type} [DecidableEq Operation] {input : List Symbol} (machine : MultiTapeMachine k Symbol Control Operation List) (cfg : Config k Symbol Control Operation input) (word : List ℕ) {S : Type} (oracle : Operation × List Symbol → S → List Symbol × S) (s : S) : Option ((List ℕ × Config k Symbol Control Operation input) × S)

Successful replay together with its final external state. Failed certificates are excluded, including any private-state effects before a late failure; sibling replays never share them.

theorem Turing.MultiTapeMachine.filterMap_replayResult {k : ℕ} {Symbol Control Operation : Type} [DecidableEq Operation] {input : List Symbol} (machine : MultiTapeMachine k Symbol Control Operation List) (bound : ℕ) (hpos : 0 < bound) (hbound : ∀ (state : Control) (symbol : Option Symbol) (work : Fin k → Option Symbol) (answers : Operation → Option Symbol), (machine.tr state symbol work answers).length ≤ bound) (fuel : ℕ) (cfg : Config k Symbol Control Operation input) {S : Type} (oracle : Operation × List Symbol → S → List Symbol × S) (s : S) : List.filterMap (fun (word : List ℕ) => machine.replayResult cfg word oracle s) (indexWords bound fuel) = machine.runOccurrenceTrace fuel cfg oracle s

Canonical fixed-clock certificates enumerate the exact ordered native run, retaining every consumed index, complete configuration and branch-local private state. Live cutoff endpoints are retained. This equality requires neither nonblocking nor a halting premise.

theorem Turing.MultiTapeMachine.replayIndicesFrom_halted {k : ℕ} {Symbol Control Operation : Type} [DecidableEq Operation] {input : List Symbol} (machine : MultiTapeMachine k Symbol Control Operation List) (cfg : Config k Symbol Control Operation input) (h : cfg.tapes.state = none) (trace word : List ℕ) : machine.replayIndicesFrom cfg trace word = pure (if word = List.replicate word.length 0 then some (trace, cfg) else none)

A halted replay accepts exactly the all-zero suffix and makes no external call.

def Turing.MultiTapeMachine.replayTerminal {k : ℕ} {Symbol Control Operation : Type} [DecidableEq Operation] {input : List Symbol} (machine : MultiTapeMachine k Symbol Control Operation List) (cfg : Config k Symbol Control Operation input) (word : List ℕ) : Cslib.OracleComp (fun (x : Operation × List Symbol) => List Symbol) (Option (List ℕ × Config k Symbol Control Operation input))

Terminal observation is separate from raw replay. Live cutoff endpoints fail this check.

theorem Turing.MultiTapeMachine.filterMap_replayResult_terminal {k : ℕ} {Symbol Control Operation : Type} [DecidableEq Operation] {input : List Symbol} (machine : MultiTapeMachine k Symbol Control Operation List) (bound : ℕ) (hpos : 0 < bound) (hbound : ∀ (state : Control) (symbol : Option Symbol) (work : Fin k → Option Symbol) (answers : Operation → Option Symbol), (machine.tr state symbol work answers).length ≤ bound) (fuel : ℕ) (cfg : Config k Symbol Control Operation input) {S : Type} (oracle : Operation × List Symbol → S → List Symbol × S) (s : S) : List.filterMap (fun (word : List ℕ) => Option.filter (fun (result : (List ℕ × Config k Symbol Control Operation input) × S) => result.1.2.tapes.state.isNone) (machine.replayResult cfg word oracle s)) (indexWords bound fuel) = List.filter (fun (result : (List ℕ × Config k Symbol Control Operation input) × S) => result.1.2.tapes.state.isNone) (machine.runOccurrenceTrace fuel cfg oracle s)

Filtering canonical replay and filtering the native run give the same terminal occurrences.

theorem Turing.MultiTapeMachine.countP_replayResult_terminal {k : ℕ} {Symbol Control Operation : Type} [DecidableEq Operation] {input : List Symbol} (machine : MultiTapeMachine k Symbol Control Operation List) (bound : ℕ) (hpos : 0 < bound) (hbound : ∀ (state : Control) (symbol : Option Symbol) (work : Fin k → Option Symbol) (answers : Operation → Option Symbol), (machine.tr state symbol work answers).length ≤ bound) (fuel : ℕ) (cfg : Config k Symbol Control Operation input) {S : Type} (oracle : Operation × List Symbol → S → List Symbol × S) (s : S) (verdict : List Symbol → Bool) : List.countP (fun (word : List ℕ) => Option.any (fun (result : (List ℕ × Config k Symbol Control Operation input) × S) => result.1.2.tapes.state.isNone && verdict result.1.2.tapes.output) (machine.replayResult cfg word oracle s)) (indexWords bound fuel) = List.countP (fun (result : (List ℕ × Config k Symbol Control Operation input) × S) => result.1.2.tapes.state.isNone && verdict result.1.2.tapes.output) (machine.runOccurrenceTrace fuel cfg oracle s)

Both verdict counts require successful terminal replay; invalid and live certificates count for neither verdict, including when verdict is negated.

theorem Turing.MultiTapeMachine.runOccurrenceTrace_empty {k : ℕ} {Symbol Control : Type} {input : List Symbol} (machine : MultiTapeCTM k Symbol Control) (fuel : ℕ) (cfg : Cfg k Symbol Control input) {S : Type} (s : S) : List.map (fun (x : (List ℕ × Config k Symbol Control Empty input) × S) => match x with | ((fst, final), state) => (final.tapes, state)) (runOccurrenceTrace machine fuel (Config.emptyOracleEquiv.symm cfg) (fun (q : Empty × List Symbol) => q.1.elim) s) = List.map (fun (final : Cfg k Symbol Control input) => (final, s)) (machine.runList fuel cfg)

With no oracle channels, erasing the trace gives exactly the existing closed runList. Both sides retain live cutoff endpoints and preserve repeated final configurations.

theorem Turing.MultiTapeMachine.replayTerminal_empty {k : ℕ} {Symbol Control : Type} {input : List Symbol} (machine : MultiTapeCTM k Symbol Control) (cfg : Cfg k Symbol Control input) (word : List ℕ) : Option.map (fun (x : List ℕ × Config k Symbol Control Empty input) => match x with | (choices, final) => (choices, final.tapes)) (Cslib.OracleComp.interpret (fun (q : Empty × List Symbol) => q.1.elim) (replayTerminal machine (Config.emptyOracleEquiv.symm cfg) word)).run = machine.decodeCertificate cfg word

The terminal closed specialization is exactly the existing canonical decoder. Raw replay itself also retains live cutoffs, so the terminal observation in this statement is essential.