Stateful oracle simulation

Local simulation identities lift to arbitrary adaptive programs, retaining both the result and the oracle's final private state. A simulation may randomly complete hidden state, as in the lazy-sampling proof for a random function. The local identity only needs to hold at states satisfying a preserved invariant.

These rules adapt Languages/Probabilistic/Simulation.lean from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8 to the common OracleComp.interpret interface. There is one oracle specification and one interpreter; stateful execution uses StateT.

Main results

• Cslib.OracleComp.induction: structural induction with the step case OracleComp.query q >>= cont.
• Cslib.OracleComp.run_interpret_pure, Cslib.OracleComp.run_interpret_bind, Cslib.OracleComp.run_interpret_map, Cslib.OracleComp.run_interpret_query: stateful interpretation of pure, >>=, <$>, and query.
• Cslib.OracleComp.run_interpret_invariant: invariants of each call hold after execution.
• Cslib.OracleComp.run_interpret_simulation_of_invariant: probabilistic state simulation.
• Cslib.OracleComp.run_interpret_map_state_of_invariant: deterministic state representation.
• Cslib.OracleComp.run_interpret_map_response_state: represent both replies and private state.
• Cslib.OracleComp.map_run_interpret: a monad morphism commutes with stateful interpretation.
• Cslib.OracleComp.run_interpret_lift: lifted effects preserve the complete private state.
• Cslib.OracleComp.run_interpret_run_interpret: a stateful handler whose effects are oracle calls, followed by a stateful oracle for those calls, is one handler on the joint state.
• Cslib.ProbComp.isMonadHom_eval: ProbComp.eval is a monad morphism into PMF.
• Cslib.ProbComp.eval_interpret: evaluating an interpreted oracle program interprets each call by its evaluated sampler.
• Cslib.ProbComp.mem_support_eval_pure_iff, Cslib.ProbComp.mem_support_eval_bind_iff, Cslib.ProbComp.mem_support_eval_map_iff, Cslib.ProbComp.mem_support_eval_uniform, Cslib.ProbComp.mem_support_eval_uniform_iff: support of evaluated closed probabilistic programs.

theorem Cslib.OracleComp.induction {ι : Type u} {spec : OracleSpec ι} {α : Type v} {motive : OracleComp spec α → Prop} (pure : ∀ (a : α), motive (pure a)) (query_bind : ∀ (q : ι) (cont : spec q → OracleComp spec α), (∀ (a : spec q), motive (cont a)) → motive (query q >>= cont)) (program : OracleComp spec α) : motive program

Structural induction on an oracle program, presenting the step case as OracleComp.query q >>= cont.

@[simp]

theorem Cslib.OracleComp.run_interpret_pure {ι : Type u} {spec : OracleSpec ι} {α State : Type v} {m : Type v → Type w} [Monad m] (oracle : (q : ι) → StateT State m (spec q)) (a : α) (s : State) : (interpret oracle (pure a)).run s = pure (a, s)

A pure program returns its value and leaves the state unchanged.

theorem Cslib.OracleComp.run_interpret_bind {ι : Type u} {spec : OracleSpec ι} {α State β : Type v} {m : Type v → Type w} [Monad m] [LawfulMonad m] (oracle : (q : ι) → StateT State m (spec q)) (program : OracleComp spec α) (next : α → OracleComp spec β) (s : State) : (interpret oracle (program >>= next)).run s = do let x ← (interpret oracle program).run s (interpret oracle (next x.1)).run x.2

Running program >>= next runs program, then runs next at its result from the state it reached.

theorem Cslib.OracleComp.run_interpret_map {ι : Type u} {spec : OracleSpec ι} {α State β : Type v} {m : Type v → Type w} [Monad m] [LawfulMonad m] (oracle : (q : ι) → StateT State m (spec q)) (f : α → β) (program : OracleComp spec α) (s : State) : (interpret oracle (f <$> program)).run s = Prod.map f id <$> (interpret oracle program).run s

Mapping f over a program maps it over the result and keeps the final state.

theorem Cslib.OracleComp.run_interpret_query {ι : Type u} {spec : OracleSpec ι} {State : Type v} {m : Type v → Type w} [Monad m] [LawfulMonad m] (oracle : (q : ι) → StateT State m (spec q)) (q : ι) (s : State) : (interpret oracle (query q)).run s = oracle q s

A single call is answered by the stateful oracle from the current state.

theorem Cslib.OracleComp.run_interpret_lift {ι : Type u} {spec : OracleSpec ι} {α State : Type v} {m : Type v → Type u_1} [Monad m] [LawfulMonad m] (oracle : (q : ι) → m (spec q)) (program : OracleComp spec α) (s : State) : (interpret (fun (q : ι) => StateT.lift (oracle q)) program).run s = (fun (a : α) => (a, s)) <$> interpret oracle program

Lifting every oracle action into state retains the original state beside its result.

theorem Cslib.OracleComp.run_interpret_invariant {ι : Type u} {spec : OracleSpec ι} {α State : Type v} (oracle : (q : ι) → StateT State PMF (spec q)) (invariant : State → Prop) (step : ∀ (q : ι) (s : State), invariant s → ∀ (a : spec q) (s' : State), (a, s') ∈ (oracle q s).support → invariant s') (program : OracleComp spec α) (s : State) (hs : invariant s) (result : α) (s' : State) (h : (result, s') ∈ ((interpret oracle program).run s).support) : invariant s'

An invariant preserved by supported oracle transitions holds after every adaptive program.

theorem Cslib.OracleComp.run_interpret_simulation_of_invariant {ι : Type u} {spec : OracleSpec ι} {α State State' : Type v} (oracle : (q : ι) → StateT State PMF (spec q)) (oracle' : (q : ι) → StateT State' PMF (spec q)) (relate : State → PMF State') (invariant : State → Prop) (preserve : ∀ (q : ι) (s : State), invariant s → ∀ (a : spec q) (s' : State), (a, s') ∈ (oracle q s).support → invariant s') (step : ∀ (q : ι) (s : State), invariant s → ((oracle q s).bind fun (x : spec q × State) => match x with | (a, s') => PMF.map (fun (x : State') => (a, x)) (relate s')) = (relate s).bind (oracle' q)) (program : OracleComp spec α) (s : State) (hs : invariant s) : (((interpret oracle program).run s).bind fun (x : α × State) => match x with | (a, s') => PMF.map (fun (x : State') => (a, x)) (relate s')) = (relate s).bind fun (t : State') => (interpret oracle' program).run t

A probabilistic change of private state that commutes with calls on invariant states commutes with an entire adaptive computation. Only supported transitions must preserve the invariant, and the equality retains the joint result and final state.

theorem Cslib.OracleComp.run_interpret_simulation {ι : Type u} {spec : OracleSpec ι} {α State State' : Type v} (oracle : (q : ι) → StateT State PMF (spec q)) (oracle' : (q : ι) → StateT State' PMF (spec q)) (relate : State → PMF State') (step : ∀ (q : ι) (s : State), ((oracle q s).bind fun (x : spec q × State) => match x with | (a, s') => PMF.map (fun (x : State') => (a, x)) (relate s')) = (relate s).bind (oracle' q)) (program : OracleComp spec α) (s : State) : (((interpret oracle program).run s).bind fun (x : α × State) => match x with | (a, s') => PMF.map (fun (x : State') => (a, x)) (relate s')) = (relate s).bind fun (t : State') => (interpret oracle' program).run t

A local probabilistic simulation lifts to every adaptive computation.

theorem Cslib.OracleComp.run_interpret_map_state_of_invariant {ι : Type u} {spec : OracleSpec ι} {α State State' : Type v} (oracle : (q : ι) → StateT State PMF (spec q)) (oracle' : (q : ι) → StateT State' PMF (spec q)) (represent : State → State') (invariant : State → Prop) (preserve : ∀ (q : ι) (s : State), invariant s → ∀ (a : spec q) (s' : State), (a, s') ∈ (oracle q s).support → invariant s') (step : ∀ (q : ι) (s : State), invariant s → PMF.map (fun (x : spec q × State) => match x with | (a, s') => (a, represent s')) (oracle q s) = oracle' q (represent s)) (program : OracleComp spec α) (s : State) (hs : invariant s) : PMF.map (fun (x : α × State) => match x with | (a, s') => (a, represent s')) ((interpret oracle program).run s) = (interpret oracle' program).run (represent s)

Re-encoding private state preserves adaptive execution when calls agree on invariant states.

theorem Cslib.OracleComp.run_interpret_map_state {ι : Type u} {spec : OracleSpec ι} {α State State' : Type v} (oracle : (q : ι) → StateT State PMF (spec q)) (oracle' : (q : ι) → StateT State' PMF (spec q)) (represent : State → State') (step : ∀ (q : ι) (s : State), PMF.map (fun (x : spec q × State) => match x with | (a, s') => (a, represent s')) (oracle q s) = oracle' q (represent s)) (program : OracleComp spec α) (s : State) : PMF.map (fun (x : α × State) => match x with | (a, s') => (a, represent s')) ((interpret oracle program).run s) = (interpret oracle' program).run (represent s)

A deterministic representation commuting with each call preserves the complete execution.

theorem Cslib.OracleComp.run_interpret_map_response_state {ι : Type u} {spec : OracleSpec ι} {α State State' : Type v} {spec' : OracleSpec ι} (response : (q : ι) → spec q → spec' q) (oracle : (q : ι) → StateT State PMF (spec q)) (oracle' : (q : ι) → StateT State' PMF (spec' q)) (represent : State → State') (step : ∀ (q : ι) (s : State), PMF.map (fun (x : spec q × State) => match x with | (a, s') => (response q a, represent s')) (oracle q s) = oracle' q (represent s)) (program : OracleComp spec' α) (s : State) : PMF.map (fun (x : α × State) => match x with | (a, s') => (a, represent s')) ((interpret oracle (interpret (fun (q : ι) => response q <$> query q) program)).run s) = (interpret oracle' program).run (represent s)

Representing replies and private state commutes with adaptive execution. Oracle substitution supplies each target reply by mapping a source reply, including to adaptive continuations. This corollary of state simulation retains the joint result and represented final state.

theorem Cslib.OracleComp.map_run_interpret {ι : Type u} {spec : OracleSpec ι} {α State : Type v} {m : Type v → Type u_1} {n : Type v → Type u_2} [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n] {f : {β : Type v} → m β → n β} (hf : IsMonadHom m n fun {α : Type v} => f) (oracle : (q : ι) → StateT State m (spec q)) (program : OracleComp spec α) (s : State) : f ((interpret oracle program).run s) = (interpret (fun (q : ι) (state : State) => f (oracle q state)) program).run s

Transforming the underlying monad commutes with stateful program interpretation, retaining the joint result and private state.

theorem Cslib.OracleComp.run_interpret_run_interpret {ι : Type u} {spec : OracleSpec ι} {α : Type v} {κ : Type w} {target : OracleSpec κ} {Hidden External : Type v} {m : Type v → Type u_1} [Monad m] [LawfulMonad m] (handler : (q : ι) → StateT Hidden (OracleComp target) (spec q)) (oracle : (q : κ) → StateT External m (target q)) (program : OracleComp spec α) (hidden : Hidden) (external : External) : (interpret oracle ((interpret handler program).run hidden)).run external = (fun (result : α × Hidden × External) => ((result.1, result.2.1), result.2.2)) <$> (interpret (fun (q : ι) (state : Hidden × External) => (fun (result : (spec q × Hidden) × External) => (result.1.1, result.1.2, result.2)) <$> (interpret oracle ((handler q).run state.1)).run state.2) program).run (hidden, external)

Running a program against a stateful handler whose own effects are oracle calls, and then running those calls against a stateful oracle, is one stateful execution on the joint state. The result, the handler's final state and the oracle's final state are retained jointly.

theorem Cslib.ProbComp.isMonadHom_eval : IsMonadHom ProbComp PMF @eval

Evaluating a closed probabilistic program is a monad morphism into PMF.

theorem Cslib.ProbComp.eval_interpret {α ι : Type} {spec : ι → Type} (handler : (q : ι) → ProbComp (spec q)) (program : OracleComp spec α) : (OracleComp.interpret handler program).eval = OracleComp.interpret (fun (q : ι) => (handler q).eval) program

Evaluating an interpreted oracle program is interpreting each call by its evaluated sampler.

theorem Cslib.ProbComp.mem_support_eval_pure_iff {α : Type} {a x : α} : x ∈ (pure a).eval.support ↔ x = a

A returned value is the only supported outcome of pure a.

theorem Cslib.ProbComp.mem_support_eval_bind_iff {α β : Type} {program : ProbComp α} {next : α → ProbComp β} {b : β} : b ∈ (program >>= next).eval.support ↔ ∃ a ∈ program.eval.support, b ∈ (next a).eval.support

An outcome is supported by program >>= next iff it is supported by next a for some supported outcome a of program.

theorem Cslib.ProbComp.mem_support_eval_map_iff {α β : Type} {f : α → β} {program : ProbComp α} {b : β} : b ∈ (f <$> program).eval.support ↔ ∃ a ∈ program.eval.support, f a = b

An outcome is supported by f <$> program iff it is the image under f of a supported outcome of program.

theorem Cslib.ProbComp.mem_support_eval_uniform {α : Type} [Fintype α] [Nonempty α] (a : α) : a ∈ (uniform α).eval.support

Every element of a nonempty finite type is in the support of uniform α.

theorem Cslib.ProbComp.mem_support_eval_uniform_iff {α : Type} [Fintype α] [Nonempty α] {a : α} : a ∈ (uniform α).eval.support ↔ True

Membership in the support of uniform α is unconditionally true.