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.

Each rule is stated twice: for the spelled-out interpretation of the sum handler, and for its name Cslib.ProbOracleComp.runWith (runWith_invariant, runWith_simulation, …). The two statements are definitionally equal.

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.
• Cslib.ProbOracleComp.runWith_readOnly, Cslib.ProbOracleComp.runWith_invariant, Cslib.ProbOracleComp.runWith_simulation, Cslib.ProbOracleComp.runWith_map_state_of_invariant, Cslib.ProbOracleComp.runWith_map_state, Cslib.ProbOracleComp.runWith_map_response_state, Cslib.ProbOracleComp.runWith_run_interpret: the same rules for Cslib.ProbOracleComp.runWith.

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 (OracleComp.sumHandler (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 (OracleComp.sumHandler 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.runWith_readOnly {Query α State : Type} {spec : Query → Type} (oracle : (q : Query) → State → PMF (spec q)) (program : ProbOracleComp spec α) (s : State) : runWith (fun (q : Query) (state : State) => PMF.map (fun (x : spec q) => (x, state)) (oracle q state)) program s = PMF.map (fun (x : α) => (x, s)) (OracleComp.evalWith (OracleComp.sumHandler ProbComp.unifOracle fun (q : Query) => oracle q s) program)

Reading a fixed external environment retains it, independently of the client's private draws: the run evaluates the program against the environment at the starting state.

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 (OracleComp.sumHandler (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.runWith_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') ∈ (runWith oracle program s).support) : invariant s'

An external oracle's invariant holds at every final state of runWith.

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 (OracleComp.sumHandler (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 (OracleComp.sumHandler (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.runWith_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) : ((runWith oracle program s).bind fun (x : α × State) => match x with | (a, s') => PMF.map (fun (x : State') => (a, x)) (relate s')) = (relate s).bind (runWith oracle' program)

A local probabilistic state simulation extends to runWith.

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 (OracleComp.sumHandler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) oracle) program).run s) = (OracleComp.interpret (OracleComp.sumHandler (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.runWith_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')) (runWith oracle program s) = runWith oracle' program (represent s)

A state representation commuting with external calls on invariant states commutes with runWith.

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 (OracleComp.sumHandler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) oracle) program).run s) = (OracleComp.interpret (OracleComp.sumHandler (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.runWith_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')) (runWith oracle program s) = runWith oracle' program (represent s)

A deterministic state representation commuting with external calls commutes with runWith.

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 (OracleComp.sumHandler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) oracle) (OracleComp.interpret (OracleComp.sumHandler (fun (n : ℕ) => sample (ProbComp.unifFin n)) fun (q : Query) => response q <$> query q) program)).run s) = (OracleComp.interpret (OracleComp.sumHandler (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.runWith_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')) (runWith oracle (OracleComp.interpret (OracleComp.sumHandler (fun (n : ℕ) => sample (ProbComp.unifFin n)) fun (q : Query) => response q <$> query q) program) s) = runWith oracle' program (represent s)

Reply and state representations commute with runWith; private samples are forwarded unchanged.

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 (OracleComp.sumHandler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) oracle) ((OracleComp.interpret (OracleComp.sumHandler (fun (n : ℕ) => StateT.lift (sample (ProbComp.unifFin n))) inner) program).run hidden)).run external = PMF.map (fun (x : α × Hidden × External) => match x with | (a, b, c) => ((a, b), c)) ((OracleComp.interpret (OracleComp.sumHandler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) fun (q : Query) (state : Hidden × External) => PMF.map (fun (x : (spec q × Hidden) × External) => match x with | ((a, b), c) => (a, b, c)) ((OracleComp.interpret (OracleComp.sumHandler (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.

theorem Cslib.ProbOracleComp.runWith_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) : runWith oracle ((OracleComp.interpret (OracleComp.sumHandler (fun (n : ℕ) => StateT.lift (sample (ProbComp.unifFin n))) inner) program).run hidden) external = PMF.map (fun (x : α × Hidden × External) => match x with | (a, b, c) => ((a, b), c)) (runWith (fun (q : Query) (state : Hidden × External) => PMF.map (fun (x : (spec q × Hidden) × External) => match x with | ((a, b), c) => (a, b, c)) (runWith oracle ((inner q).run state.1) state.2)) program (hidden, external))

A stateful handler that draws private coins and calls an external oracle, run against that oracle by runWith, is one runWith on the joint state of the handler and the oracle.