Random-Oracle Simulation Helpers

Generic lemmas for simulating OracleComp (unifSpec + hashSpec) computations via unifFwdImpl + ro in StateT hashSpec.QueryCache ProbComp, where unifFwdImpl forwards uniform-randomness queries and ro handles the hash oracle (typically randomOracle).

These lemmas factor out boilerplate shared by FiatShamir.perfectlyCorrect, FiatShamirWithAbort.correct, and other random-oracle-model proofs.

The typical usage pattern is:

let ro : QueryImpl hashSpec (StateT hashSpec.QueryCache ProbComp) := randomOracle
let impl := unifFwdImpl hashSpec + ro

Then the roSim namespace lemmas apply to simulateQ impl.

Main definitions

• unifFwdImpl: the identity forwarding implementation for unifSpec, lifted to StateT

noncomputable def unifFwdImpl {ι : Type} (hashSpec : OracleSpec ι) : QueryImpl unifSpec (StateT hashSpec.QueryCache ProbComp)

The identity forwarding implementation for unifSpec queries, lifted to StateT hashSpec.QueryCache ProbComp. Each uniform query passes through to the underlying ProbComp without touching the cache state.

theorem unifFwdImpl.simulateQ_run {ι : Type} {hashSpec : OracleSpec ι} {α : Type} (oa : ProbComp α) (s : hashSpec.QueryCache) : (simulateQ (unifFwdImpl hashSpec) oa).run s = (fun (x : α) => (x, s)) <$> oa

theorem roSim.simulateQ_liftComp {ι : Type} {hashSpec : OracleSpec ι} (ro : QueryImpl hashSpec (StateT hashSpec.QueryCache ProbComp)) {α : Type} (oa : ProbComp α) : simulateQ (unifFwdImpl hashSpec + ro) (OracleComp.liftComp oa (unifSpec + hashSpec)) = simulateQ (unifFwdImpl hashSpec) oa

theorem roSim.run_liftM {ι : Type} {hashSpec : OracleSpec ι} (ro : QueryImpl hashSpec (StateT hashSpec.QueryCache ProbComp)) {α : Type} (oa : ProbComp α) (s : hashSpec.QueryCache) : (simulateQ (unifFwdImpl hashSpec + ro) (liftM oa)).run s = (fun (x : α) => (x, s)) <$> oa

theorem roSim.run_liftM_support {ι : Type} {hashSpec : OracleSpec ι} (ro : QueryImpl hashSpec (StateT hashSpec.QueryCache ProbComp)) {α : Type} (oa : ProbComp α) (s : hashSpec.QueryCache) : support ((simulateQ (unifFwdImpl hashSpec + ro) (liftM oa)).run s) = (fun (x : α) => (x, s)) '' support oa

theorem roSim.run'_liftM_bind {ι : Type} {hashSpec : OracleSpec ι} (ro : QueryImpl hashSpec (StateT hashSpec.QueryCache ProbComp)) {α β : Type} (oa : ProbComp α) (rest : α → StateT hashSpec.QueryCache ProbComp β) (s : hashSpec.QueryCache) : (simulateQ (unifFwdImpl hashSpec + ro) (liftM oa) >>= rest).run' s = do let x ← oa (rest x).run' s

theorem roSim.simulateQ_HasQuery_query {ι : Type} {hashSpec : OracleSpec ι} (ro : QueryImpl hashSpec (StateT hashSpec.QueryCache ProbComp)) (q : hashSpec.Domain) : simulateQ (unifFwdImpl hashSpec + ro) (HasQuery.query q) = ro q