Private randomness with typed oracle calls

ProbOracleComp spec combines the existing finite-uniform sampling interface with spec by a disjoint sum of query types. It is still an OracleComp, interpreted by OracleComp.interpret. sample embeds a closed probabilistic program, and query calls the external oracle. A handler can therefore draw fresh private coins while caching only the external queries.

The finite-uniform interface specifies distributions, not their computational efficiency. Strict fair-coin realizability is certified separately; arbitrary exact finite-uniform sampling is not automatically a strict PPT operation.

Main definitions

• Cslib.probOracleSpec: the disjoint sum unifSpec ⊕ₒ spec of the finite-uniform sampling requests and the external queries of spec.
• Cslib.ProbOracleComp: the sum of the uniform sampling and external oracle interfaces.
• Cslib.ProbOracleComp.sample, .query: closed sampling and typed external calls.

The sampling and external interfaces form the sum unifSpec ⊕ₒ spec of CslibFrontier/Languages/Probabilistic/Sum.lean: sample is its left embedding (sample_eq_liftLeft), and a handler is the sum handler OracleComp.sumHandler random oracle, which answers private sampling requests with random and external queries with oracle. In particular, memoizing oracle does not memoize random. The rules of OracleComp.sumHandler apply directly.

Main results

• Cslib.ProbOracleComp.isMonadHom_sample: sample is a monad morphism from ProbComp.
• Cslib.ProbOracleComp.interpret_sample: embedded sampling uses only the sampling handler.
• Cslib.ProbOracleComp.run_interpret_sample: private sampling leaves oracle state unchanged.
• Cslib.ProbOracleComp.run_interpret_lift_sample: a stateful handler with external calls forwards private sampling unchanged.
• Cslib.ProbOracleComp.sample_run_interpret: sampling a closed stateful execution is the execution of the sampled handler.
• Cslib.ProbOracleComp.eval_interpret: closed handlers commute with probability interpretation.
• Cslib.ProbOracleComp.eval_run_interpret: closed handler programs preserve the joint state law.

References

Uses the typed interface of cslib PR #1129, by Samuel Schlesinger and Devon Tuma, based on the VCVio design credited in Languages.Probabilistic.Basic. This replaces the separate sampling constructor used by the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

@[reducible, inline]

abbrev Cslib.probOracleSpec {Query : Type} (spec : Query → Type) : OracleSpec (ℕ ⊕ Query)

A disjoint sum keeps fresh sampling requests separate from external oracle requests.

@[reducible, inline]

abbrev Cslib.ProbOracleComp {Query : Type} (spec : Query → Type) (α : Type) : Type

A program with separate finite-uniform samples and typed external queries.

def Cslib.ProbOracleComp.sample {Query α : Type} {spec : Query → Type} (program : ProbComp α) : ProbOracleComp spec α

Embed a closed probabilistic program; its calls remain separate from the external oracle.

theorem Cslib.ProbOracleComp.sample_eq_liftLeft {Query α : Type} {spec : Query → Type} (program : ProbComp α) : sample program = OracleComp.liftLeft program

Sampling is the left embedding into the sum unifSpec ⊕ₒ spec.

theorem Cslib.ProbOracleComp.isMonadHom_sample {Query : Type} {spec : Query → Type} : IsMonadHom ProbComp (ProbOracleComp spec) fun {α : Type} => sample

Lifting a closed sampler into ProbOracleComp spec is a monad morphism.

def Cslib.ProbOracleComp.query {Query : Type} {spec : Query → Type} (q : Query) : ProbOracleComp spec (spec q)

Make one external call, whose reply may determine later sampling or queries.

@[simp]

theorem Cslib.ProbOracleComp.interpret_query {Query : Type} {spec : Query → Type} {m : Type → Type v} [Monad m] [LawfulMonad m] (random : (n : ℕ) → m (Fin (n + 1))) (oracle : (q : Query) → m (spec q)) (q : Query) : OracleComp.interpret (OracleComp.sumHandler random oracle) (query q) = oracle q

The combined handler answers a single external query through its external component.

@[simp]

theorem Cslib.ProbOracleComp.interpret_sample {Query α : Type} {spec : Query → Type} {m : Type → Type v} [Monad m] [LawfulMonad m] (random : (n : ℕ) → m (Fin (n + 1))) (oracle : (q : Query) → m (spec q)) (program : ProbComp α) : OracleComp.interpret (OracleComp.sumHandler random oracle) (sample program) = OracleComp.interpret random program

Embedded closed programs use only the sampling component of the combined handler.

@[simp]

theorem Cslib.ProbOracleComp.sample_bind {Query α β : Type} {spec : Query → Type} (program : ProbComp α) (next : α → ProbComp β) : sample (program >>= next) = do let a ← sample program sample (next a)

Sampling preserves ordinary functional sequencing before any interpretation.

@[simp]

theorem Cslib.ProbOracleComp.sample_pure {Query α : Type} {spec : Query → Type} (a : α) : sample (pure a) = pure a

Sampling a returned value makes no call.

@[simp]

theorem Cslib.ProbOracleComp.sample_map {Query α β : Type} {spec : Query → Type} (f : α → β) (program : ProbComp α) : sample (f <$> program) = f <$> sample program

Deterministic postprocessing stays inside the embedded closed program.

theorem Cslib.ProbOracleComp.run_interpret_sample {Query α State : Type} {spec : Query → Type} (oracle : (q : Query) → StateT State PMF (spec q)) (program : ProbComp α) (s : State) : (OracleComp.interpret (OracleComp.sumHandler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) oracle) (sample program)).run s = PMF.map (fun (x : α) => (x, s)) program.eval

Private sampling is fresh and leaves the complete external oracle state unchanged.

theorem Cslib.ProbOracleComp.run_interpret_lift_sample {Query α State : Type} {spec : Query → Type} {Query' : Type} {spec' : Query' → Type} (oracle : (q : Query) → StateT State (ProbOracleComp spec') (spec q)) (program : ProbComp α) (s : State) : (OracleComp.interpret (OracleComp.sumHandler (fun (n : ℕ) => StateT.lift (sample (ProbComp.unifFin n))) oracle) (sample program)).run s = (fun (x : α) => (x, s)) <$> sample program

A stateful handler that itself has private coins and external calls forwards every private draw as a fresh sample, leaving its own state unchanged.

theorem Cslib.ProbOracleComp.sample_run_interpret {Query α State : Type} {spec : Query → Type} {Query' : Type} {spec' : Query' → Type} (oracle : (q : Query) → StateT State ProbComp (spec q)) (program : ProbOracleComp spec α) (s : State) : sample ((OracleComp.interpret (OracleComp.sumHandler (fun (n : ℕ) => StateT.lift (ProbComp.unifFin n)) oracle) program).run s) = (OracleComp.interpret (OracleComp.sumHandler (fun (n : ℕ) => StateT.lift (sample (ProbComp.unifFin n))) fun (q : Query) (state : State) => sample (oracle q state)) program).run s

Sampling a closed stateful execution is the execution of the sampled handler: both make the same private draws and retain the same final handler state.

theorem Cslib.ProbOracleComp.eval_interpret {Query α : Type} {spec : Query → Type} (oracle : (q : Query) → ProbComp (spec q)) (program : ProbOracleComp spec α) : (OracleComp.interpret (OracleComp.sumHandler ProbComp.unifFin oracle) program).eval = OracleComp.interpret (OracleComp.sumHandler ProbComp.unifOracle fun (q : Query) => (oracle q).eval) program

Closed handlers have the same probability law when interpreted before or after evaluation.

theorem Cslib.ProbOracleComp.eval_run_interpret {Query α State : Type} {spec : Query → Type} (oracle : (q : Query) → StateT State ProbComp (spec q)) (program : ProbOracleComp spec α) (s : State) : ((OracleComp.interpret (OracleComp.sumHandler (fun (n : ℕ) => StateT.lift (ProbComp.unifFin n)) oracle) program).run s).eval = (OracleComp.interpret (OracleComp.sumHandler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) fun (q : Query) (state : State) => (oracle q state).eval) program).run s

Evaluating closed stateful handlers commutes with interpreting the whole oracle program. Private sampling stays independent, and the final state is retained beside the result.