Observing oracle transcripts

withTranscript records each query and its answer while preserving the oracle's private state. Entries are stored newest first. Forgetting the transcript recovers the original execution, including its final private state.

Query budgets (Cslib.OracleComp.IsCostBounded) are properties of the program itself; every logged run respects them.

This is semantic instrumentation, not a claim that recording arbitrary replies is efficient. In particular, a machine's clock bounds its requests but need not bound the oracle's replies.

Main definitions

• Cslib.OracleComp.Transcript, .withTranscript: typed query logging with private state.

Main results

• Cslib.OracleComp.run_interpret_withTranscript: forgetting the log preserves full execution.
• Cslib.OracleComp.run_interpret_withTranscript_append: retain an existing transcript suffix.

References

Adapted from Languages/Probabilistic/Transcript.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the single OracleComp.interpret interface.

@[reducible, inline]

abbrev Cslib.OracleComp.Transcript {Query : Type u} (Response : Query → Type u) : Type u

Queries and their typed replies, stored in reverse chronological order.

noncomputable def Cslib.OracleComp.withTranscript {Query : Type u} {Response : Query → Type u} {State : Type u} (oracle : (q : Query) → StateT State PMF (Response q)) (q : Query) : StateT (State × Transcript Response) PMF (Response q)

Observe calls without changing the underlying oracle's replies or private state.

theorem Cslib.OracleComp.run_interpret_withTranscript {Query : Type u} {Response : Query → Type u} {State α : Type u} (oracle : (q : Query) → StateT State PMF (Response q)) (program : OracleComp Response α) (s : State) (transcript : Transcript Response) : PMF.map (fun (x : α × State × Transcript Response) => match x with | (result, state) => (result, state.1)) ((interpret (withTranscript oracle) program).run (s, transcript)) = (interpret oracle program).run s

Forgetting the transcript preserves the result and the oracle's complete final state.

theorem Cslib.OracleComp.run_interpret_withTranscript_append {Query : Type u} {Response : Query → Type u} {State α : Type u} (oracle : (q : Query) → StateT State PMF (Response q)) (program : OracleComp Response α) (s : State) (transcript : Transcript Response) : (interpret (withTranscript oracle) program).run (s, transcript) = PMF.map (fun (x : α × State × Transcript Response) => match x with | (result, state, fresh) => (result, state, fresh ++ transcript)) ((interpret (withTranscript oracle) program).run (s, []))

An existing transcript is an untouched suffix of the newly recorded interaction.