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.

theorem simulateQ_liftM_query {α : Type u} {ι : Type u_6} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) [LawfulMonad r] {ι' : Type u_4} {spec' : OracleSpec ι'} [MonadLiftT (OracleQuery spec') (OracleQuery spec)] (q : OracleQuery spec' α) : simulateQ impl (liftM q) = impl.mapQuery (liftM q)

Companion to simulateQ_query for a query entering the computation through a query-level lift chain: simulating a query lifted from a sub-spec spec' applies the implementation to the lifted query.

The (liftM q : OracleComp spec α) on the left elaborates through the canonical MonadLift (OracleQuery spec) (OracleComp spec) composed (via instMonadLiftTOfMonadLift) with the given MonadLiftT (OracleQuery spec') (OracleQuery spec) — e.g. a SubSpec embedding chain such as spec₂ ⊂ₒ spec₁ + spec₂ ⊂ₒ spec + (spec₁ + spec₂). This is the term shape produced by lifting a query helper (liftM (liftM (spec'.query t))) into a larger interface, as OracleSpec.SubSpec-based protocol verifiers do. simulateQ_query itself cannot match it: its query's spec is forced to equal the simulated spec, while here the query lives in spec'.

The right-hand side is deliberately mapQuery of the single term liftM q rather than the unbundled (liftM q).cont <$> impl (liftM q).input: the type of .cont depends on .input, so the unbundled form blocks all further simp rewriting of the lifted query (the dependent-motive trap). With mapQuery, the lifted query can then be normalized in place (everything in the SubSpec lift chain is definitional) and landed on the implementation with mapQuery_mk.

Not @[simp]: for the common sum-spec layouts the specialized routing lemmas (QueryImpl.simulateQ_add_add_liftM_query_left and friends in SimSemantics/Append.lean) resolve the routed query in one step; this general form would preempt them and strand the goal at an un-normalized mapQuery (liftM q). Use it manually for bespoke lift chains.

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)

theorem simulateQ_bind_map_eq_of_body {α β γ : Type u} {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) [LawfulMonad r] (oa : OracleComp spec α) (body₁ : α → OracleComp spec β) (body₂ : α → OracleComp spec γ) (f : γ → β) (hBody : ∀ (a : α), simulateQ impl (body₁ a) = f <$> simulateQ impl (body₂ a)) : simulateQ impl (oa >>= body₁) = f <$> simulateQ impl (oa >>= body₂)

Two simulateQ'd binds whose bodies agree up to a pure post-map f agree up to mapping f over the whole simulation. Companion to simulateQ_bind for establishing map-relations between two simulations without unfolding the shared leading computation oa.

@[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_dite {α : Type u} {ι : Type u_4} {spec : OracleSpec ι} {r : Type u → Type u_1} [Monad r] (impl : QueryImpl spec r) (p : Prop) [Decidable p] (mx : p → OracleComp spec α) (mx' : ¬p → OracleComp spec α) : simulateQ impl (dite p mx mx') = if h : p then simulateQ impl (mx h) else simulateQ impl (mx' h)

@[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 implementation 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.