Relational simulateQ Rules

This file provides the highest-leverage theorems for game-hopping proofs: relational coupling through oracle simulation, and the "identical until bad" lemma.

Main results

• relTriple_simulateQ_run: If two stateful oracle implementations are related by a state invariant and produce equal outputs, then simulating a computation with either implementation preserves the invariant and output equality.
• relTriple_simulateQ_run': Projection that only asserts output equality.
• tvDist_simulateQ_le_probEvent_bad: "Identical until bad" — if two oracle implementations agree whenever a "bad" flag is unset, the TV distance between their simulations is bounded by the probability of bad being set.

Relational simulateQ rules

theorem OracleComp.ProgramLogic.Relational.relTriple_simulateQ_run {ι : Type u} {spec : OracleSpec ι} {α : Type} {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {σ₁ σ₂ : Type} (impl₁ : QueryImpl spec (StateT σ₁ (OracleComp spec₁))) (impl₂ : QueryImpl spec (StateT σ₂ (OracleComp spec₂))) (R_state : σ₁ → σ₂ → Prop) (oa : OracleComp spec α) (himpl : ∀ (t : spec.Domain) (s₁ : σ₁) (s₂ : σ₂), R_state s₁ s₂ → RelTriple ((impl₁ t).run s₁) ((impl₂ t).run s₂) fun (p₁ : spec.Range t × σ₁) (p₂ : spec.Range t × σ₂) => p₁.1 = p₂.1 ∧ R_state p₁.2 p₂.2) (s₁ : σ₁) (s₂ : σ₂) (hs : R_state s₁ s₂) : RelTriple ((simulateQ impl₁ oa).run s₁) ((simulateQ impl₂ oa).run s₂) fun (p₁ : α × σ₁) (p₂ : α × σ₂) => p₁.1 = p₂.1 ∧ R_state p₁.2 p₂.2

Core relational simulateQ theorem with state invariant. If two oracle implementations produce equal outputs and preserve a state invariant R_state, then the full simulation also preserves the invariant and output equality.

theorem OracleComp.ProgramLogic.Relational.relTriple_simulateQ_run' {ι : Type u} {spec : OracleSpec ι} {α : Type} {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {σ₁ σ₂ : Type} (impl₁ : QueryImpl spec (StateT σ₁ (OracleComp spec₁))) (impl₂ : QueryImpl spec (StateT σ₂ (OracleComp spec₂))) (R_state : σ₁ → σ₂ → Prop) (oa : OracleComp spec α) (himpl : ∀ (t : spec.Domain) (s₁ : σ₁) (s₂ : σ₂), R_state s₁ s₂ → RelTriple ((impl₁ t).run s₁) ((impl₂ t).run s₂) fun (p₁ : spec.Range t × σ₁) (p₂ : spec.Range t × σ₂) => p₁.1 = p₂.1 ∧ R_state p₁.2 p₂.2) (s₁ : σ₁) (s₂ : σ₂) (hs : R_state s₁ s₂) : RelTriple ((simulateQ impl₁ oa).run' s₁) ((simulateQ impl₂ oa).run' s₂) (EqRel α)

Projection: relational simulateQ preserving only output equality.

theorem OracleComp.ProgramLogic.Relational.relTriple_simulateQ_run'_of_impl_evalDist_eq {ι : Type u} {spec : OracleSpec ι} {α : Type} {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {σ : Type} (impl₁ : QueryImpl spec (StateT σ (OracleComp spec₁))) (impl₂ : QueryImpl spec (StateT σ (OracleComp spec₂))) (oa : OracleComp spec α) (himpl : ∀ (t : spec.Domain) (s : σ), evalDist ((impl₁ t).run s) = evalDist ((impl₂ t).run s)) (s₁ s₂ : σ) (hs : s₁ = s₂) : RelTriple ((simulateQ impl₁ oa).run' s₁) ((simulateQ impl₂ oa).run' s₂) (EqRel α)

Exact-distribution specialization of relTriple_simulateQ_run'.

If corresponding oracle calls have identical full (output, state) distributions whenever the states are equal, then the simulated computations have identical output distributions. This packages the common pattern "prove per-query evalDist equality, then use Eq as the state invariant" into a single theorem.

WriterT analogue

theorem OracleComp.ProgramLogic.Relational.relTriple_simulateQ_run_writerT {ι : Type u} {spec : OracleSpec ι} {α : Type} {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {ω₁ ω₂ : Type} [Monoid ω₁] [Monoid ω₂] (impl₁ : QueryImpl spec (WriterT ω₁ (OracleComp spec₁))) (impl₂ : QueryImpl spec (WriterT ω₂ (OracleComp spec₂))) (R_writer : ω₁ → ω₂ → Prop) (hR_one : R_writer 1 1) (hR_mul : ∀ (w₁ w₁' : ω₁) (w₂ w₂' : ω₂), R_writer w₁ w₂ → R_writer w₁' w₂' → R_writer (w₁ * w₁') (w₂ * w₂')) (oa : OracleComp spec α) (himpl : ∀ (t : spec.Domain), RelTriple (impl₁ t).run (impl₂ t).run fun (p₁ : spec.Range t × ω₁) (p₂ : spec.Range t × ω₂) => p₁.1 = p₂.1 ∧ R_writer p₁.2 p₂.2) : RelTriple (simulateQ impl₁ oa).run (simulateQ impl₂ oa).run fun (p₁ : α × ω₁) (p₂ : α × ω₂) => p₁.1 = p₂.1 ∧ R_writer p₁.2 p₂.2

WriterT analogue of relTriple_simulateQ_run.

If two writer-transformed oracle implementations produce outputs related by a reflexive-and-closed relation R_writer on the accumulated logs, then the full simulation preserves output equality together with the accumulated-log relation.

hR_one witnesses reflexivity at the empty accumulator (the run-start value), and hR_mul closes R_writer under the monoid multiplication used by WriterT's bind. Together these make R_writer a monoid congruence on the two writer spaces, which is precisely the structural requirement for whole-program accumulation.

theorem OracleComp.ProgramLogic.Relational.relTriple_simulateQ_run_writerT_of_impl_eq {ι : Type u} {spec : OracleSpec ι} {α : Type} {ι₁ : Type u} {spec₁ : OracleSpec ι₁} [spec₁.Fintype] [spec₁.Inhabited] {ω : Type} [Monoid ω] (impl₁ impl₂ : QueryImpl spec (WriterT ω (OracleComp spec₁))) (himpl_eq : ∀ (t : spec.Domain), (impl₁ t).run = (impl₂ t).run) (oa : OracleComp spec α) : RelTriple (simulateQ impl₁ oa).run (simulateQ impl₂ oa).run (EqRel (α × ω))

WriterT analogue of relTriple_simulateQ_run_of_impl_eq_preservesInv.

If two writer-transformed oracle implementations agree pointwise on .run (i.e. every per-query increment is identical as an OracleComp), then the whole simulations yield identical (output, accumulator) distributions.

WriterT handlers are stateless (.run takes no argument), so the hypothesis is a plain equality rather than an invariant-gated implication. The postcondition is strict equality on α × ω.

theorem OracleComp.ProgramLogic.Relational.probOutput_simulateQ_run_writerT_eq_of_impl_eq {ι : Type u} {spec : OracleSpec ι} {α : Type} {ι₁ : Type u} {spec₁ : OracleSpec ι₁} [spec₁.Fintype] [spec₁.Inhabited] {ω : Type} [Monoid ω] (impl₁ impl₂ : QueryImpl spec (WriterT ω (OracleComp spec₁))) (himpl_eq : ∀ (t : spec.Domain), (impl₁ t).run = (impl₂ t).run) (oa : OracleComp spec α) (z : α × ω) : Pr[= z | (simulateQ impl₁ oa).run] = Pr[= z | (simulateQ impl₂ oa).run]

Output-probability projection of relTriple_simulateQ_run_writerT_of_impl_eq: two WriterT handlers with pointwise-equal .run yield identical (output, accumulator) probability distributions.

theorem OracleComp.ProgramLogic.Relational.evalDist_simulateQ_run_writerT_eq_of_impl_eq {ι : Type u} {spec : OracleSpec ι} {α : Type} {ι₁ : Type u} {spec₁ : OracleSpec ι₁} [spec₁.Fintype] [spec₁.Inhabited] {ω : Type} [Monoid ω] (impl₁ impl₂ : QueryImpl spec (WriterT ω (OracleComp spec₁))) (himpl_eq : ∀ (t : spec.Domain), (impl₁ t).run = (impl₂ t).run) (oa : OracleComp spec α) : evalDist (simulateQ impl₁ oa).run = evalDist (simulateQ impl₂ oa).run

evalDist equality projection of relTriple_simulateQ_run_writerT_of_impl_eq.

theorem OracleComp.ProgramLogic.Relational.relTriple_simulateQ_run_writerT' {ι : Type u} {spec : OracleSpec ι} {α : Type} {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {ω₁ ω₂ : Type} [Monoid ω₁] [Monoid ω₂] (impl₁ : QueryImpl spec (WriterT ω₁ (OracleComp spec₁))) (impl₂ : QueryImpl spec (WriterT ω₂ (OracleComp spec₂))) (R_writer : ω₁ → ω₂ → Prop) (hR_one : R_writer 1 1) (hR_mul : ∀ (w₁ w₁' : ω₁) (w₂ w₂' : ω₂), R_writer w₁ w₂ → R_writer w₁' w₂' → R_writer (w₁ * w₁') (w₂ * w₂')) (oa : OracleComp spec α) (himpl : ∀ (t : spec.Domain), RelTriple (impl₁ t).run (impl₂ t).run fun (p₁ : spec.Range t × ω₁) (p₂ : spec.Range t × ω₂) => p₁.1 = p₂.1 ∧ R_writer p₁.2 p₂.2) : RelTriple (Prod.fst <$> (simulateQ impl₁ oa).run) (Prod.fst <$> (simulateQ impl₂ oa).run) (EqRel α)

Projection of relTriple_simulateQ_run_writerT onto the output component.

theorem OracleComp.ProgramLogic.Relational.relTriple_simulateQ_run_of_impl_eq_preservesInv {α ι : Type} {spec : OracleSpec ι} {σ : Type} (impl₁ impl₂ : QueryImpl spec (StateT σ ProbComp)) (Inv : σ → Prop) (oa : OracleComp spec α) (himpl_eq : ∀ (t : spec.Domain) (s : σ), Inv s → (impl₁ t).run s = (impl₂ t).run s) (hpres₂ : ∀ (t : spec.Domain) (s : σ), Inv s → ∀ z ∈ support ((impl₂ t).run s), Inv z.2) (s : σ) (hs : Inv s) : RelTriple ((simulateQ impl₁ oa).run s) ((simulateQ impl₂ oa).run s) fun (p₁ p₂ : α × σ) => p₁ = p₂ ∧ Inv p₁.2

If two stateful oracle implementations agree on every query while Inv holds, and the second implementation preserves Inv, then the full simulations have identical (output, state) distributions from any invariant-satisfying initial state.

theorem OracleComp.ProgramLogic.Relational.relTriple_simulateQ_run_eqRel_of_impl_eq_preservesInv {α ι : Type} {spec : OracleSpec ι} {σ : Type} (impl₁ impl₂ : QueryImpl spec (StateT σ ProbComp)) (Inv : σ → Prop) (oa : OracleComp spec α) (himpl_eq : ∀ (t : spec.Domain) (s : σ), Inv s → (impl₁ t).run s = (impl₂ t).run s) (hpres₂ : ∀ (t : spec.Domain) (s : σ), Inv s → ∀ z ∈ support ((impl₂ t).run s), Inv z.2) (s : σ) (hs : Inv s) : RelTriple ((simulateQ impl₁ oa).run s) ((simulateQ impl₂ oa).run s) (EqRel (α × σ))

Exact-equality specialization of relTriple_simulateQ_run_of_impl_eq_preservesInv.

This weakens the stronger invariant-carrying postcondition to plain equality on (output, state), which is the shape consumed directly by probability-transport lemmas and theorem-driven rvcgen steps.

theorem OracleComp.ProgramLogic.Relational.probOutput_simulateQ_run_eq_of_impl_eq_preservesInv {α ι : Type} {spec : OracleSpec ι} {σ : Type} (impl₁ impl₂ : QueryImpl spec (StateT σ ProbComp)) (Inv : σ → Prop) (oa : OracleComp spec α) (himpl_eq : ∀ (t : spec.Domain) (s : σ), Inv s → (impl₁ t).run s = (impl₂ t).run s) (hpres₂ : ∀ (t : spec.Domain) (s : σ), Inv s → ∀ z ∈ support ((impl₂ t).run s), Inv z.2) (s : σ) (hs : Inv s) (z : α × σ) : Pr[= z | (simulateQ impl₁ oa).run s] = Pr[= z | (simulateQ impl₂ oa).run s]

Output-probability projection of relTriple_simulateQ_run_of_impl_eq_preservesInv.

theorem OracleComp.ProgramLogic.Relational.probOutput_simulateQ_run_eq_of_impl_eq_queryBound {α ι : Type} {spec : OracleSpec ι} {σ : Type} {B : Type u_1} (impl₁ impl₂ : QueryImpl spec (StateT σ ProbComp)) (Inv : σ → B → Prop) (canQuery : spec.Domain → B → Prop) (cost : spec.Domain → B → B) (oa : OracleComp spec α) (budget : B) (hbound : oa.IsQueryBound budget canQuery cost) (himpl_eq : ∀ (t : spec.Domain) (s : σ) (b : B), Inv s b → canQuery t b → (impl₁ t).run s = (impl₂ t).run s) (hpres₂ : ∀ (t : spec.Domain) (s : σ) (b : B), Inv s b → canQuery t b → ∀ z ∈ support ((impl₂ t).run s), Inv z.2 (cost t b)) (s : σ) (hs : Inv s budget) (z : α × σ) : Pr[= z | (simulateQ impl₁ oa).run s] = Pr[= z | (simulateQ impl₂ oa).run s]

Query-bounded exact-output transport for simulateQ.

If oa satisfies a structural query bound IsQueryBound budget canQuery cost, the two implementations agree on every query that the bound permits, and the second implementation preserves a budget-indexed invariant Inv, then the full simulated computations have identical output-state probabilities from any initial state satisfying Inv.

theorem OracleComp.ProgramLogic.Relational.map_run_simulateQ_eq_of_query_map_eq {α ι : Type} {spec : OracleSpec ι} {σ₁ σ₂ : Type} (impl₁ : QueryImpl spec (StateT σ₁ ProbComp)) (impl₂ : QueryImpl spec (StateT σ₂ ProbComp)) (proj : σ₁ → σ₂) (hproj : ∀ (t : spec.Domain) (s : σ₁), Prod.map id proj <$> (impl₁ t).run s = (impl₂ t).run (proj s)) (oa : OracleComp spec α) (s : σ₁) : Prod.map id proj <$> (simulateQ impl₁ oa).run s = (simulateQ impl₂ oa).run (proj s)

State-projection transport for simulateQ.run.

If each oracle call under impl₁ becomes the corresponding impl₂ call after mapping the state with proj, then the full simulated runs agree under the same projection.

theorem OracleComp.ProgramLogic.Relational.run'_simulateQ_eq_of_query_map_eq {α ι : Type} {spec : OracleSpec ι} {σ₁ σ₂ : Type} (impl₁ : QueryImpl spec (StateT σ₁ ProbComp)) (impl₂ : QueryImpl spec (StateT σ₂ ProbComp)) (proj : σ₁ → σ₂) (hproj : ∀ (t : spec.Domain) (s : σ₁), Prod.map id proj <$> (impl₁ t).run s = (impl₂ t).run (proj s)) (oa : OracleComp spec α) (s : σ₁) : (simulateQ impl₁ oa).run' s = (simulateQ impl₂ oa).run' (proj s)

run' projection corollary of map_run_simulateQ_eq_of_query_map_eq.

theorem OracleComp.ProgramLogic.Relational.relTriple_simulateQ_run'_of_query_map_eq {α ι : Type} {spec : OracleSpec ι} {σ₁ σ₂ : Type} (impl₁ : QueryImpl spec (StateT σ₁ ProbComp)) (impl₂ : QueryImpl spec (StateT σ₂ ProbComp)) (proj : σ₁ → σ₂) (hproj : ∀ (t : spec.Domain) (s : σ₁), Prod.map id proj <$> (impl₁ t).run s = (impl₂ t).run (proj s)) (oa : OracleComp spec α) (s : σ₁) : RelTriple ((simulateQ impl₁ oa).run' s) ((simulateQ impl₂ oa).run' (proj s)) (EqRel α)

Relational transport corollary of run'_simulateQ_eq_of_query_map_eq.

theorem OracleComp.ProgramLogic.Relational.map_run_simulateQ_eq_of_query_map_eq' {α ι ι' : Type} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {σ₁ σ₂ : Type} (impl₁ : QueryImpl spec (StateT σ₁ (OracleComp spec'))) (impl₂ : QueryImpl spec (StateT σ₂ (OracleComp spec'))) (proj : σ₁ → σ₂) (hproj : ∀ (t : spec.Domain) (s : σ₁), Prod.map id proj <$> (impl₁ t).run s = (impl₂ t).run (proj s)) (oa : OracleComp spec α) (s : σ₁) : Prod.map id proj <$> (simulateQ impl₁ oa).run s = (simulateQ impl₂ oa).run (proj s)

Generalized state-projection theorem: if applying proj to the state commutes with each oracle step, then it commutes with the full simulation. Generalizes the ProbComp version to any target spec.

theorem OracleComp.ProgramLogic.Relational.run'_simulateQ_eq_of_query_map_eq' {α ι ι' : Type} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {σ₁ σ₂ : Type} (impl₁ : QueryImpl spec (StateT σ₁ (OracleComp spec'))) (impl₂ : QueryImpl spec (StateT σ₂ (OracleComp spec'))) (proj : σ₁ → σ₂) (hproj : ∀ (t : spec.Domain) (s : σ₁), Prod.map id proj <$> (impl₁ t).run s = (impl₂ t).run (proj s)) (oa : OracleComp spec α) (s : σ₁) : (simulateQ impl₁ oa).run' s = (simulateQ impl₂ oa).run' (proj s)

run' projection corollary of map_run_simulateQ_eq_of_query_map_eq'.

"Identical until bad" fundamental lemma

theorem OracleComp.ProgramLogic.Relational.tvDist_simulateQ_le_probEvent_bad {ι : Type u} {spec : OracleSpec ι} {α : Type} [spec.Fintype] [spec.Inhabited] {σ : Type} (impl₁ impl₂ : QueryImpl spec (StateT σ (OracleComp spec))) (bad : σ → Prop) (oa : OracleComp spec α) (s₀ : σ) (h_init : ¬bad s₀) (h_agree : ∀ (t : spec.Domain) (s : σ), ¬bad s → (impl₁ t).run s = (impl₂ t).run s) (h_mono₁ : ∀ (t : spec.Domain) (s : σ), bad s → ∀ x ∈ support ((impl₁ t).run s), bad x.2) (h_mono₂ : ∀ (t : spec.Domain) (s : σ), bad s → ∀ x ∈ support ((impl₂ t).run s), bad x.2) : tvDist ((simulateQ impl₁ oa).run' s₀) ((simulateQ impl₂ oa).run' s₀) ≤ (probEvent ((simulateQ impl₁ oa).run s₀) (bad ∘ Prod.snd)).toReal

The fundamental lemma of game playing: if two oracle implementations agree whenever a "bad" flag is unset, then the total variation distance between the two simulations is bounded by the probability that bad gets set.

Both implementations must satisfy a monotonicity condition: once bad s holds, it must remain true in all reachable successor states. Without this, the theorem is false — an implementation could enter a bad state (where agreement is not required), diverge, and then return to a non-bad state, producing different outputs with Pr[bad] = 0. Monotonicity is needed on both sides because the proof establishes pointwise equality Pr[= (x,s) | sim₁] = Pr[= (x,s) | sim₂] for all ¬bad s, which requires ruling out bad-to-non-bad transitions in each implementation independently.

Distributional "identical until bad"

The _dist variant weakens the agreement hypothesis from definitional equality (impl₁ t).run s = (impl₂ t).run s) to distributional equality (∀ p, Pr[= p | (impl₁ t).run s] = Pr[= p | (impl₂ t).run s]). This is needed when the two implementations differ intensionally but agree on output probabilities.

theorem OracleComp.ProgramLogic.Relational.tvDist_simulateQ_le_probEvent_bad_dist {ι : Type u} {spec : OracleSpec ι} {α : Type} [spec.Fintype] [spec.Inhabited] {σ : Type} (impl₁ impl₂ : QueryImpl spec (StateT σ (OracleComp spec))) (bad : σ → Prop) (oa : OracleComp spec α) (s₀ : σ) : ¬bad s₀ → ∀ (h_agree_dist : ∀ (t : spec.Domain) (s : σ), ¬bad s → ∀ (p : spec.Range t × σ), Pr[= p | (impl₁ t).run s] = Pr[= p | (impl₂ t).run s]) (h_mono₁ : ∀ (t : spec.Domain) (s : σ), bad s → ∀ x ∈ support ((impl₁ t).run s), bad x.2) (h_mono₂ : ∀ (t : spec.Domain) (s : σ), bad s → ∀ x ∈ support ((impl₂ t).run s), bad x.2), tvDist ((simulateQ impl₁ oa).run' s₀) ((simulateQ impl₂ oa).run' s₀) ≤ (probEvent ((simulateQ impl₁ oa).run s₀) (bad ∘ Prod.snd)).toReal

Distributional variant of tvDist_simulateQ_le_probEvent_bad: weakens the agreement hypothesis from definitional equality to distributional equality (pointwise equal output probabilities).

def OracleComp.ProgramLogic.Relational.QueryImpl.fixSndStateT {ι : Type} {spec : OracleSpec ι} {σ Q : Type} (impl : QueryImpl spec (StateT (σ × Q) ProbComp)) (q₀ : Q) : QueryImpl spec (StateT σ ProbComp)

Given a StateT (σ × Q) ProbComp query implementation, fix the second state component at q₀ and project to StateT σ ProbComp.

theorem OracleComp.ProgramLogic.Relational.simulateQ_run_eq_of_snd_invariant {ι : Type} {spec : OracleSpec ι} {σ Q α : Type} (impl : QueryImpl spec (StateT (σ × Q) ProbComp)) (q₀ : Q) (h_inv : ∀ (t : spec.Domain) (s : σ), ∀ x ∈ support ((impl t).run (s, q₀)), x.2.2 = q₀) (oa : OracleComp spec α) (s : σ) : (simulateQ impl oa).run (s, q₀) = (fun (p : α × σ) => (p.1, p.2, q₀)) <$> (simulateQ (QueryImpl.fixSndStateT impl q₀) oa).run s

If the Q-component of product state (σ × Q) is invariant under all oracle queries starting from q₀, then the full simulateQ computation decomposes: running with (s, q₀) produces the same result as running the projected implementation on s alone, with q₀ appended back.

This generalizes map_run_simulateQ_eq_of_query_map_eq from all-states commutativity to support-based invariance.

theorem OracleComp.ProgramLogic.Relational.simulateQ_run'_eq_of_snd_invariant {ι : Type} {spec : OracleSpec ι} {σ Q α : Type} (impl : QueryImpl spec (StateT (σ × Q) ProbComp)) (q₀ : Q) (h_inv : ∀ (t : spec.Domain) (s : σ), ∀ x ∈ support ((impl t).run (s, q₀)), x.2.2 = q₀) (oa : OracleComp spec α) (s : σ) : (simulateQ impl oa).run' (s, q₀) = (simulateQ (QueryImpl.fixSndStateT impl q₀) oa).run' s

run' projection corollary of simulateQ_run_eq_of_snd_invariant.