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

@[simp]

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

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

theorem OracleComp.neverFail_simulateQ_randomOracle_run {ι : Type} {spec : OracleSpec ι} {α : Type} [DecidableEq ι] [spec.Inhabited] [(t : spec.Domain) → SampleableType (spec.Range t)] (oa : OracleComp spec α) (cache : spec.QueryCache) : NeverFail ((simulateQ OracleSpec.randomOracle oa).run cache)

The random-oracle simulation of a plain OracleComp never fails on any starting cache.

theorem OracleComp.exists_agreesWithFn_evalWithAnswerFn_eq_iff_mem_support {ι : Type} {spec : OracleSpec ι} {α : Type} [DecidableEq ι] [spec.Inhabited] [(t : spec.Domain) → SampleableType (spec.Range t)] (oa : OracleComp spec α) (cache : spec.QueryCache) (a : α) : (∃ (f : QueryImpl spec Id), OracleSpec.QueryCache.AgreesWithFn f cache ∧ evalWithAnswerFn f oa = a) ↔ ∃ (cache' : spec.QueryCache), (a, cache') ∈ support ((simulateQ OracleSpec.randomOracle oa).run cache)

Support characterization for lazy random-oracle simulation.

A value a can appear as the output of the random-oracle simulation from cache iff some total answer function agreeing with cache evaluates the computation to a. The final cache produced by the simulation is existentially quantified away.

theorem OracleComp.probEvent_eq_one_simulateQ_randomOracle_run_iff {ι : Type} {spec : OracleSpec ι} {α : Type} [DecidableEq ι] [spec.Inhabited] [(t : spec.Domain) → SampleableType (spec.Range t)] (oa : OracleComp spec α) (preexisting_cache : spec.QueryCache) (p : α → Prop) : (probEvent ((simulateQ OracleSpec.randomOracle oa).run preexisting_cache) fun (v : α × spec.QueryCache) => p v.1) = 1 ↔ ∀ (f : QueryImpl spec Id), OracleSpec.QueryCache.AgreesWithFn f preexisting_cache → p (evalWithAnswerFn f oa)

Probability-one form of the random-oracle support characterization.

A predicate on the result value holds with probability one under lazy random-oracle simulation from preexisting_cache iff it holds for every total answer function agreeing with that cache.