Saved samples in adaptive oracle interactions

An external handler can consume one saved sample per call while the client continues drawing independent private randomness. For a program making at most n external queries, n independent samples drawn in advance give exactly the online joint law of the result and the handler's state (ProbOracleComp.IsQueryBounded.run_interpret_presample). Unused samples are discarded in this equality; they need not be independent of the final state or the client's stopping time. The handler's fallback value is never used, so a run on a sufficient list of samples is a function of those samples.

This is the library's presampling theorem. A program without private coins is the special case OracleComp.IsQueryBounded.run_interpret_presample, and closed ProbComp handlers the special case ProbOracleComp.IsQueryBounded.eval_presample.

Main definitions

• Cslib.OracleComp.withSampleList: supply a list's head to a handler and retain its tail.

Main results

• Cslib.ProbOracleComp.IsQueryBounded.run_interpret_presample: presampling preserves the joint law of result and state.
• Cslib.ProbOracleComp.IsQueryBounded.eval_presample: the same for closed probabilistic handlers.
• Cslib.OracleComp.IsQueryBounded.run_interpret_presample: the same without private coins.

References

Adapted from Languages/Probabilistic/Presample.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the typed sum of private and external calls.

def Cslib.OracleComp.withSampleList {Query : Type u} {spec : Query → Type v} {State Value : Type v} {m : Type v → Type w} [Functor m] (fallback : Value) (oracle : Value → (q : Query) → StateT State m (spec q)) (q : Query) : StateT (State × List Value) m (spec q)

Supply the next saved sample to a stateful handler. The fallback makes short lists total; the ordinary state and unused suffix are retained.

theorem Cslib.ProbOracleComp.IsQueryBounded.run_interpret_presample {Query α State Value : Type} {spec : Query → Type} {program : ProbOracleComp spec α} {n : ℕ} (h : program.IsQueryBounded n) (source : PMF Value) (fallback : Value) (oracle : Value → (q : Query) → StateT State PMF (spec q)) (s : State) : ((PMF.map List.ofFn (Probability.PMF.iid source n)).bind fun (values : List Value) => PMF.map (fun (result : α × State × List Value) => (result.1, result.2.1)) ((OracleComp.interpret (handler (fun (k : ℕ) => StateT.lift (ProbComp.unifOracle k)) (OracleComp.withSampleList fallback oracle)) program).run (s, values))) = (OracleComp.interpret (handler (fun (k : ℕ) => StateT.lift (ProbComp.unifOracle k)) fun (q : Query) (state : State) => source.bind fun (value : Value) => oracle value q state) program).run s

Presampling. A program makes at most n external queries, and a handler draws one sample from source per external query. Answering from n independent samples drawn in advance instead gives the same joint law of the result and the handler's state. Private samples are drawn online in both runs. The statement is exact and independent of the efficiency of the program, the handler and the source.

theorem Cslib.ProbOracleComp.IsQueryBounded.eval_presample {Query α State Value : Type} {spec : Query → Type} {program : ProbOracleComp spec α} {count : ℕ} (h : program.IsQueryBounded count) (source : ProbComp Value) (fallback : Value) (oracle : Value → (q : Query) → StateT State ProbComp (spec q)) (s : State) : (do let values ← OracleComp.replicate count source (fun (x : α × State × List Value) => match x with | (result, next, snd) => (result, next)) <$> (OracleComp.interpret (handler (fun (n : ℕ) => StateT.lift (ProbComp.unifFin n)) (OracleComp.withSampleList fallback oracle)) program).run (s, values)).eval = ((OracleComp.interpret (handler (fun (n : ℕ) => StateT.lift (ProbComp.unifFin n)) fun (q : Query) (s : State) => do let value ← source oracle value q s) program).run s).eval

Presampling with closed probabilistic handlers. The ProbComp form of IsQueryBounded.run_interpret_presample: n saved samples from source give the online joint law of the result and the handler's state.

theorem Cslib.OracleComp.IsQueryBounded.run_interpret_presample {Query State Value γ : Type} {spec : Query → Type} {program : OracleComp spec γ} {n : ℕ} (h : program.IsQueryBounded n) (source : PMF Value) (fallback : Value) (oracle : Value → (q : Query) → StateT State PMF (spec q)) (s : State) : ((PMF.map List.ofFn (Probability.PMF.iid source n)).bind fun (values : List Value) => PMF.map (fun (result : γ × State × List Value) => (result.1, result.2.1)) ((interpret (withSampleList fallback oracle) program).run (s, values))) = (interpret (fun (q : Query) (state : State) => source.bind fun (value : Value) => oracle value q state) program).run s

Presampling without private coins. A program makes at most n calls, and a handler draws one sample from source per call. Answering from n independent samples drawn in advance gives the same joint law of the result and the handler's state.