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

Simulating a plain ProbComp through unifFwdImpl and running it on cache s leaves the cache untouched, pairing each sampled output with the unchanged s.

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

Simulating a liftComp-embedded ProbComp through unifFwdImpl + ro discards the hash oracle, reducing to simulation through unifFwdImpl alone.

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

Running the unifFwdImpl + ro simulation of a lifted ProbComp on cache s leaves the cache untouched, pairing each sampled output with s.

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

The support of the unifFwdImpl + ro simulation of a lifted ProbComp run on cache s is the image of support oa under pairing each output with s.

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

Running the unifFwdImpl + ro simulation of a lifted ProbComp bound to a continuation, projected to its value via run', samples oa and then runs each continuation on cache 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

Simulating a hashSpec query through unifFwdImpl + ro dispatches it to the hash-oracle handler ro, since uniform forwarding leaves hash queries to ro.

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

Simulating a HasQuery.query hash query through unifFwdImpl + ro dispatches it to the hash-oracle handler ro, matching simulateQ_liftM_spec_query through the monad-lift form.

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.

theorem simulateQ_randomOracle_map_uniformFin {α : Type} (n : ℕ) (f : Fin (n + 1) → α) : (simulateQ OracleSpec.randomOracle (f <$> ($ᵗ Fin (n + 1)))).run' ∅ = f <$> ($ᵗ Fin (n + 1))

Simulating the random oracle leaves a mapped uniform Fin sample unchanged: the query is intercepted, but from the empty cache it misses and resamples uniformly, and the updated cache is then discarded by run', so the distribution over results is identical to the original sample.