Transcripts of randomized programs

The typed transcript of a program with private coins records only its external requests: private samples use the other component of ProbOracleComp.handler and do not enter the log. Forgetting the log recovers the original execution, and an existing log is an untouched suffix of the new one.

Main results

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

References

Adapts Languages/Probabilistic/Transcript.lean from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, reusing its typed log and the general simulation API.

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

Forgetting the external log preserves the joint result and complete oracle state.

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

Fresh external observations are prepended to an existing transcript. Private draws do not change either part of the log.