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.
• Cslib.ProbOracleComp.handler: the sum handler of sampling and external queries.

The sampling and external interfaces form the sum unifSpec ⊕ₒ spec of Complexity/Languages/Probabilistic/Sum.lean: sample is its left embedding (sample_eq_liftLeft) and handler its sum handler (handler_eq_sumHandler).

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.

def Cslib.ProbOracleComp.handler {Query : Type} {spec : Query → Type} {m : Type → Type v} (random : (n : ℕ) → m (Fin (n + 1))) (oracle : (q : Query) → m (spec q)) (q : ℕ ⊕ Query) : m (probOracleSpec spec q)

Combine the two handlers. In particular, memoizing oracle does not memoize random. This is the sum handler of unifSpec ⊕ₒ spec (handler_eq_sumHandler), with its own case equations.

theorem Cslib.ProbOracleComp.handler_eq_sumHandler {Query : Type} {spec : Query → Type} {m : Type → Type v} (random : (n : ℕ) → m (Fin (n + 1))) (oracle : (q : Query) → m (spec q)) : handler random oracle = OracleComp.sumHandler random oracle

The combined handler is the sum handler of the sampling and external interfaces.

theorem Cslib.ProbOracleComp.interpret_handler {Query : Type} {spec : Query → Type} {Query' : Type} {spec' : Query' → Type} {m : Type → Type v} [Monad m] (target : (q : Query') → m (spec' q)) (random : (k : ℕ) → OracleComp spec' (Fin (k + 1))) (oracle : (q : Query) → OracleComp spec' (spec q)) : (fun (q : ℕ ⊕ Query) => OracleComp.interpret target (handler random oracle q)) = handler (fun (k : ℕ) => OracleComp.interpret target (random k)) fun (q : Query) => OracleComp.interpret target (oracle q)

Interpretation distributes over the sampling and external components of a program handler.

@[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 (handler 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 (handler 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 (handler (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 (handler (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 (handler (fun (n : ℕ) => StateT.lift (ProbComp.unifFin n)) oracle) program).run s) = (OracleComp.interpret (handler (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 (handler ProbComp.unifFin oracle) program).eval = OracleComp.interpret (handler 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 (handler (fun (n : ℕ) => StateT.lift (ProbComp.unifFin n)) oracle) program).run s).eval = (OracleComp.interpret (handler (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.