Stateful simulation with private randomness

An external oracle's invariant or state simulation remains valid when clients also draw private randomness. Private draws leave oracle state untouched, and independent sampling commutes with the distribution relating two state representations. These are specializations of the existing OracleComp rules to the disjoint-sum interface, with no additional program induction.

Main results

• Cslib.ProbOracleComp.run_interpret_invariant: external invariants survive private sampling.
• Cslib.ProbOracleComp.run_interpret_simulation: local joint-state simulation suffices.
• Cslib.ProbOracleComp.run_interpret_map_state_of_invariant: state representation on an invariant.
• Cslib.ProbOracleComp.run_interpret_map_state: deterministic representation of oracle state.
• Cslib.ProbOracleComp.run_interpret_map_response_state: represent replies and oracle state, leaving private samples unchanged.
• Cslib.ProbOracleComp.run_interpret_readOnly: preserve a fixed external environment.
• Cslib.ProbOracleComp.run_interpret_run_interpret: a handler with private coins and external calls, followed by the external oracle, is one stateful handler on the joint state.

References

Adapts the cslib crypto branch's state simulation API at 5ff69ca93402e7c947208dc56396d6d86203ccd8 to the typed sum of sampling and external calls.

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

Reading a fixed external environment retains it, independently of the client's private draws.

theorem Cslib.ProbOracleComp.run_interpret_invariant {Query α State : Type} {spec : Query → Type} (oracle : (q : Query) → StateT State PMF (spec q)) (invariant : State → Prop) (step : ∀ (q : Query) (s : State), invariant s → ∀ (a : spec q) (s' : State), (a, s') ∈ (oracle q s).support → invariant s') (program : ProbOracleComp spec α) (s : State) (hs : invariant s) (result : α) (s' : State) (h : (result, s') ∈ ((OracleComp.interpret (handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) oracle) program).run s).support) : invariant s'

An external oracle's invariant is unaffected by the client's private sampling.

theorem Cslib.ProbOracleComp.run_interpret_simulation {Query α State State' : Type} {spec : Query → Type} (oracle : (q : Query) → StateT State PMF (spec q)) (oracle' : (q : Query) → StateT State' PMF (spec q)) (relate : State → PMF State') (step : ∀ (q : Query) (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 : ProbOracleComp spec α) (s : State) : (((OracleComp.interpret (handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) 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 (state : State') => (OracleComp.interpret (handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) oracle') program).run state

A local probabilistic state simulation extends to clients with fresh private samples.

theorem Cslib.ProbOracleComp.run_interpret_map_state_of_invariant {Query α State State' : Type} {spec : Query → Type} (oracle : (q : Query) → StateT State PMF (spec q)) (oracle' : (q : Query) → StateT State' PMF (spec q)) (represent : State → State') (invariant : State → Prop) (preserve : ∀ (q : Query) (s : State), invariant s → ∀ (a : spec q) (s' : State), (a, s') ∈ (oracle q s).support → invariant s') (step : ∀ (q : Query) (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 : ProbOracleComp spec α) (s : State) (hs : invariant s) : PMF.map (fun (x : α × State) => match x with | (a, s') => (a, represent s')) ((OracleComp.interpret (handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) oracle) program).run s) = (OracleComp.interpret (handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) oracle') program).run (represent s)

Re-encode private state on invariant states while retaining independent private samples.

theorem Cslib.ProbOracleComp.run_interpret_map_state {Query α State State' : Type} {spec : Query → Type} (oracle : (q : Query) → StateT State PMF (spec q)) (oracle' : (q : Query) → StateT State' PMF (spec q)) (represent : State → State') (step : ∀ (q : Query) (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 : ProbOracleComp spec α) (s : State) : PMF.map (fun (x : α × State) => match x with | (a, s') => (a, represent s')) ((OracleComp.interpret (handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) oracle) program).run s) = (OracleComp.interpret (handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) oracle') program).run (represent s)

A deterministic state representation commuting with external calls commutes with the whole randomized adaptive program, retaining the result and represented private state.

theorem Cslib.ProbOracleComp.run_interpret_map_response_state {Query α State State' : Type} {spec spec' : Query → Type} (response : (q : Query) → spec q → spec' q) (oracle : (q : Query) → StateT State PMF (spec q)) (oracle' : (q : Query) → StateT State' PMF (spec' q)) (represent : State → State') (step : ∀ (q : Query) (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 : ProbOracleComp spec' α) (s : State) : PMF.map (fun (x : α × State) => match x with | (a, s') => (a, represent s')) ((OracleComp.interpret (handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) oracle) (OracleComp.interpret (handler (fun (n : ℕ) => sample (ProbComp.unifFin n)) fun (q : Query) => response q <$> query q) program)).run s) = (OracleComp.interpret (handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) oracle') program).run (represent s)

Reply and state representations preserve randomized adaptive execution. Private samples are forwarded unchanged; only external replies and the oracle's state are represented.

theorem Cslib.ProbOracleComp.run_interpret_run_interpret {Query α : Type} {spec : Query → Type} {Query' : Type} {spec' : Query' → Type} {Hidden External : Type} (inner : (q : Query) → StateT Hidden (ProbOracleComp spec') (spec q)) (oracle : (q : Query') → StateT External PMF (spec' q)) (program : ProbOracleComp spec α) (hidden : Hidden) (external : External) : (OracleComp.interpret (handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) oracle) ((OracleComp.interpret (handler (fun (n : ℕ) => StateT.lift (sample (ProbComp.unifFin n))) inner) program).run hidden)).run external = PMF.map (fun (result : α × Hidden × External) => ((result.1, result.2.1), result.2.2)) ((OracleComp.interpret (handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) fun (q : Query) (state : Hidden × External) => PMF.map (fun (result : (spec q × Hidden) × External) => (result.1.1, result.1.2, result.2)) ((OracleComp.interpret (handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) oracle) ((inner q).run state.1)).run state.2)) program).run (hidden, external))

A stateful handler that draws private coins and calls an external oracle, followed by that oracle, is one stateful handler on the joint state. Private draws stay fresh, and the result, the handler's state and the external oracle's state are retained jointly.