Bundled Subprobability Semantics for Oracle Simulations

This file builds SPMFSemantics bundles for the common oracle-simulation pattern used throughout the crypto constructions in this repo:

1. a surface OracleComp program runs in a public-randomness world
2. selected oracle families are implemented by a StateT-based simulator over ProbComp
3. the final semantics is obtained by running the hidden state from a fixed initial cache and then observing the resulting ProbComp as an SPMF

noncomputable def SPMFSemantics.withStateOracle {ι : Type} {hashSpec : OracleSpec ι} {σ : Type} (hashImpl : QueryImpl hashSpec (StateT σ ProbComp)) (s : σ) : SPMFSemantics (OracleComp (unifSpec + hashSpec))

Bundled SPMF semantics for an oracle world consisting of public randomness plus a hidden stateful oracle implementation.

The surface monad is OracleComp (unifSpec + hashSpec). Internally, computations are interpreted by simulating the public-randomness queries with their identity implementation and the additional oracle family hashSpec with the supplied stateful simulator hashImpl. The hidden state is then initialized at s and discarded, leaving only the externally visible output subdistribution.

@[simp]

theorem SPMFSemantics.withStateOracle_evalDist_map {ι : Type} {hashSpec : OracleSpec ι} {σ : Type} (hashImpl : QueryImpl hashSpec (StateT σ ProbComp)) (s : σ) {α β : Type} (f : α → β) (mx : OracleComp (unifSpec + hashSpec) α) : (withStateOracle hashImpl s).evalDist (f <$> mx) = f <$> (withStateOracle hashImpl s).evalDist mx

withStateOracle commutes with <$>: mapping a function over the surface computation is the same as mapping it over the observed SPMF.

This holds because interpret is the bundled monad morphism simulateQ', and the StateT observer fun mx => toSPMF (StateT.run' mx s) preserves <$> even though it is not a full monad morphism: <$> does not thread state, so Prod.fst <$> (f <$> mx).run s factors as f <$> (Prod.fst <$> mx.run s) = f <$> StateT.run' mx s.

theorem SPMFSemantics.withStateOracle_evalDist_bind_pure {ι : Type} {hashSpec : OracleSpec ι} {σ : Type} (hashImpl : QueryImpl hashSpec (StateT σ ProbComp)) (s : σ) {α β : Type} (mx : OracleComp (unifSpec + hashSpec) α) (f : α → β) : ((withStateOracle hashImpl s).evalDist do let x ← mx pure (f x)) = f <$> (withStateOracle hashImpl s).evalDist mx

withStateOracle commutes with the specific >>= pure ∘ f pattern produced by a do-block returning a pure value at the end. A direct corollary of withStateOracle_evalDist_map.