Simulation Semantics for Oracles in a Computation

def simulateQ {ι : Type u_1} {spec : OracleSpec ι} {r : Type u → Type u_2} [Monad r] (impl : QueryImpl spec r) {α : Type u} (mx : OracleComp spec α) : r α

Given an implementation of spec in the monad r, convert an OracleComp spec α to a implementation in r α by substituting impl t for query t throughout.

@[simp]

theorem simulateQ_pure {α : Type u} {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) (x : α) : simulateQ impl (pure x) = pure x

@[simp]

theorem simulateQ_bind {α β : Type u} {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) [LawfulMonad r] (mx : OracleComp spec α) (my : α → OracleComp spec β) : simulateQ impl (mx >>= my) = do let x ← simulateQ impl mx simulateQ impl (my x)

@[reducible]

def simulateQ' {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] [LawfulMonad r] (impl : QueryImpl spec r) : OracleComp spec →ᵐ r

Version of simulateQ that bundles into a monad hom.

@[simp]

theorem simulateQ_query {α : Type u} {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) [LawfulMonad r] (q : OracleQuery spec α) : simulateQ impl (liftM q) = q.cont <$> impl q.input

@[simp]

theorem simulateQ_spec_query {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) [LawfulMonad r] (t : spec.Domain) : simulateQ impl (liftM (OracleSpec.query t)) = impl t

Specialized form of simulateQ_query for the canonical spec.query t constructor: simulateQ impl (liftM (spec.query t)) = impl t.

The general simulateQ_query rewrite leaves an id <$> artifact when applied to spec.query t (because (spec.query t).cont = id). That artifact is harmless when spec.Range t is concrete (it disappears under definitional reduction), but in parametric sum-spec contexts ((E₁ + E₂).Range (Sum.inl t) vs E₁.Range t, both abstract atoms) the type annotations diverge and id_map no longer fires under simp only. This lemma sidesteps the artifact entirely and is the canonical entry point for simplifying simulateQ over an explicit spec.query t.

def evalWithAnswerFn {ι : Type u_4} {spec : OracleSpec ι} (f : QueryImpl spec Id) {α : Type u} (mx : OracleComp spec α) : α

Evaluate an oracle computation by answering each query with a total answer function.

This is the Id-valued specialization of simulateQ: each query in mx is replaced by the corresponding value returned by f.

@[simp]

theorem evalWithAnswerFn_pure {α : Type u} {ι : Type u_4} {spec : OracleSpec ι} (f : QueryImpl spec Id) (a : α) : evalWithAnswerFn f (pure a) = a

@[simp]

theorem evalWithAnswerFn_bind {α β : Type u} {ι : Type u_4} {spec : OracleSpec ι} (f : QueryImpl spec Id) (mx : OracleComp spec α) (my : α → OracleComp spec β) : evalWithAnswerFn f (mx >>= my) = evalWithAnswerFn f (my (evalWithAnswerFn f mx))

@[simp]

theorem evalWithAnswerFn_query {ι : Type u_4} {spec : OracleSpec ι} (f : QueryImpl spec Id) (t : spec.Domain) : evalWithAnswerFn f (query t) = f t

@[simp]

theorem simulateQ_query_bind {α β : Type u} {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) [LawfulMonad r] (q : OracleQuery spec α) (ou : α → OracleComp spec β) : simulateQ impl (liftM q >>= ou) = do let u ← liftM (impl q.input) simulateQ impl (ou (q.cont u))

@[simp]

theorem simulateQ_map {α β : Type u} {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) [LawfulMonad r] (mx : OracleComp spec α) (f : α → β) : simulateQ impl (f <$> mx) = f <$> simulateQ impl mx

@[simp]

theorem evalWithAnswerFn_map {α β : Type u} {ι : Type u_4} {spec : OracleSpec ι} (f : QueryImpl spec Id) (g : α → β) (mx : OracleComp spec α) : evalWithAnswerFn f (g <$> mx) = g (evalWithAnswerFn f mx)

@[simp]

theorem simulateQ_seq {α β : Type u} {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) [LawfulMonad r] (og : OracleComp spec (α → β)) (mx : OracleComp spec α) : simulateQ impl (og <*> mx) = simulateQ impl og <*> simulateQ impl mx

@[simp]

theorem simulateQ_seqLeft {α β : Type u} {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) [LawfulMonad r] (mx : OracleComp spec α) (my : OracleComp spec β) : simulateQ impl (mx <* my) = simulateQ impl mx <* simulateQ impl my

@[simp]

theorem simulateQ_seqRight {α β : Type u} {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) [LawfulMonad r] (mx : OracleComp spec α) (my : OracleComp spec β) : simulateQ impl (mx *> my) = simulateQ impl mx *> simulateQ impl my

@[simp]

theorem simulateQ_ite {α : Type u} {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) (p : Prop) [Decidable p] (mx mx' : OracleComp spec α) : simulateQ impl (if p then mx else mx') = if p then simulateQ impl mx else simulateQ impl mx'

@[simp]

theorem simulateQ_liftTarget {α : Type u} {ι : Type u_4} {spec : OracleSpec ι} {m : Type u → Type v} {n : Type u → Type w} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [MonadLiftT m n] [LawfulMonadLiftT m n] (impl : QueryImpl spec m) (comp : OracleComp spec α) : simulateQ (QueryImpl.liftTarget n impl) comp = liftM (simulateQ impl comp)

theorem simulateQ_def {α : Type u} {ι : Type u_1} {spec : OracleSpec ι} {n : Type u → Type v} [Monad n] [LawfulMonad n] (impl : QueryImpl spec n) (mx : OracleComp spec α) : simulateQ impl mx = (fun {α : Type u} (x : spec.toPFunctor.FreeM α) => (PFunctor.FreeM.mapMHom impl).toFun α x) mx

@[simp]

theorem simulateQ_id' {α : Type u} {ι : Type u_1} {spec : OracleSpec ι} (mx : OracleComp spec α) : simulateQ (QueryImpl.id' spec) mx = mx

QueryImpl.id' is an identity for simulateQ with implementaiton in OracleComp spec.

theorem simulateQ_ofLift_eq_self {ι : Type u_1} {spec : OracleSpec ι} {α : Type u} (mx : OracleComp spec α) : simulateQ (QueryImpl.ofLift spec (OracleComp spec)) mx = mx

Lifting queries to their original implementation has no effect on a computation.

List / ForM distributivity

@[simp]

theorem simulateQ_list_mapM {α β : Type u} {ι : Type u_1} {spec : OracleSpec ι} {n : Type u → Type v} [Monad n] [LawfulMonad n] (impl : QueryImpl spec n) (f : α → OracleComp spec β) (xs : List α) : simulateQ impl (List.mapM f xs) = List.mapM (fun (a : α) => simulateQ impl (f a)) xs

simulateQ distributes over List.mapM: simulating a mapped list is the same as mapping the simulated function over the list.

@[simp]

theorem simulateQ_list_forM {α : Type u} {ι : Type u_1} {spec : OracleSpec ι} {n : Type u → Type v} [Monad n] [LawfulMonad n] (impl : QueryImpl spec n) (f : α → OracleComp spec PUnit.{u + 1}) (xs : List α) : simulateQ impl (xs.forM f) = xs.forM fun (a : α) => simulateQ impl (f a)

simulateQ distributes over List.forM.

@[simp]

theorem simulateQ_list_forIn {α : Type u} {ι : Type u_1} {spec : OracleSpec ι} {n : Type u → Type v} [Monad n] [LawfulMonad n] (impl : QueryImpl spec n) {β : Type u} (xs : List α) (init : β) (f : α → β → OracleComp spec (ForInStep β)) : simulateQ impl (forIn xs init f) = forIn xs init fun (a : α) (b : β) => simulateQ impl (f a b)

simulateQ distributes over forIn on a list: a monad morphism commutes with forIn.

This is the forIn (early-exit / accumulating loop) sibling of simulateQ_list_mapM and simulateQ_list_forM. It lets a simulateQ pushed in front of a verifier-style loop forIn (List.finRange t) init (fun j acc => …) be moved inside the loop body, after which the individual simulated query steps can be discharged.

Composition of simulations via a per-query bridge

theorem simulateQ_StateT_compose {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {σ : Type u'} {n : Type u' → Type v'} [Monad n] [LawfulMonad n] (red : QueryImpl spec₁ (StateT σ (OracleComp spec₂))) (impl : QueryImpl spec₂ n) (game : QueryImpl spec₁ (StateT σ n)) (bridge : ∀ (q : spec₁.Domain) (s : σ), simulateQ impl ((red q).run s) = (game q).run s) {α : Type u'} (oa : OracleComp spec₁ α) (s : σ) : simulateQ impl ((simulateQ red oa).run s) = (simulateQ game oa).run s

Two-stage simulation: if a "reduction" red : QueryImpl spec₁ (StateT σ (OracleComp spec₂)) followed by an inner impl : QueryImpl spec₂ n agrees per-query with a "combined" handler game : QueryImpl spec₁ (StateT σ n), then the agreement extends to every outer computation by structural induction. This packages the boilerplate induction reused across PRF-style reductions.

theorem simulateQ_StateT_StateT_compose {ι₁ : Type u_1} {ι₂ : Type u_2} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {σ τ : Type u'} {n : Type u' → Type v'} [Monad n] [LawfulMonad n] (red : QueryImpl spec₁ (StateT σ (OracleComp spec₂))) (impl : QueryImpl spec₂ (StateT τ n)) (combined : QueryImpl spec₁ (StateT (σ × τ) n)) (bridge : ∀ (q : spec₁.Domain) (s : σ) (c : τ), (simulateQ impl ((red q).run s)).run c = (fun (r : spec₁.Range q × σ × τ) => ((r.1, r.2.1), r.2.2)) <$> combined q (s, c)) {α : Type u'} (oa : OracleComp spec₁ α) (s : σ) (c : τ) : (simulateQ impl ((simulateQ red oa).run s)).run c = (fun (r : α × σ × τ) => ((r.1, r.2.1), r.2.2)) <$> (simulateQ combined oa).run (s, c)

Three-layer simulation collapse: if a "reduction" red : QueryImpl spec₁ (StateT σ (OracleComp spec₂)) followed by an inner cached impl : QueryImpl spec₂ (StateT τ n) agrees per-query with a single "combined" handler combined : QueryImpl spec₁ (StateT (σ × τ) n) up to the natural reassociation α × σ × τ ≃ (α × σ) × τ, then the agreement extends to every outer computation. This packages the boilerplate induction used by lazy-random-oracle / cached-PRF collapses.