State-Projection Lemmas for simulateQ

This file collects the equational state-projection theorems for simulateQ over StateT-valued query implementations. They are pure equalities on distributions, with no relational, coupling, or TV-distance content, and so live at the SimSemantics layer alongside StateT.lean rather than in ProgramLogic.

Main results

• OracleComp.map_run_simulateQ_eq_of_query_map_eq (and its _inv' variant): if every oracle step of impl₁ becomes the corresponding impl₂ step after mapping the state by proj, then the full simulation does too.
• OracleComp.run'_simulateQ_eq_of_query_map_eq (and variants): the run' (output-only) projection corollaries.
• QueryImpl.StateOrnament: a package for the recurring pattern where one stateful handler refines another by carrying extra bookkeeping state.
• QueryImpl.fixSndStateT + OracleComp.simulateQ_run_eq_of_snd_invariant: support-based decomposition for product state spaces where one component is invariant.
• QueryImpl.extendState + OracleComp.extendState_run_proj_eq: auxiliary-state lift, the inverse direction of fixSndStateT.

Layering

This file is below ProgramLogic and is depended on by both ProgramLogic/Relational/SimulateQ (which proves the genuinely relational corollaries) and OracleComp/QueryTracking/* files that need to project away bookkeeping state from cached / programmed / seeded oracles.

State-projection: all states

theorem OracleComp.map_run_simulateQ_eq_of_query_map_eq {α ι : Type u} {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] [LawfulMonad m] {σ₁ σ₂ : Type u} (impl₁ : QueryImpl spec (StateT σ₁ m)) (impl₂ : QueryImpl spec (StateT σ₂ m)) (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.run'_simulateQ_eq_of_query_map_eq {α ι : Type u} {spec : OracleSpec ι} {m : Type u → Type v} [Monad m] [LawfulMonad m] {σ₁ σ₂ : Type u} (impl₁ : QueryImpl spec (StateT σ₁ m)) (impl₂ : QueryImpl spec (StateT σ₂ m)) (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.

State-projection: invariant-gated

theorem OracleComp.map_run_simulateQ_eq_of_query_map_eq_inv' {α : Type u} {ι ι' : Type} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {σ₁ σ₂ : Type u} (impl₁ : QueryImpl spec (StateT σ₁ (OracleComp spec'))) (impl₂ : QueryImpl spec (StateT σ₂ (OracleComp spec'))) (inv : σ₁ → Prop) (proj : σ₁ → σ₂) (hinv : ∀ (t : spec.Domain) (s : σ₁), inv s → ∀ y ∈ support ((impl₁ t).run s), inv y.2) (hproj : ∀ (t : spec.Domain) (s : σ₁), inv s → Prod.map id proj <$> (impl₁ t).run s = (impl₂ t).run (proj s)) (oa : OracleComp spec α) (s : σ₁) (hs : inv s) : Prod.map id proj <$> (simulateQ impl₁ oa).run s = (simulateQ impl₂ oa).run (proj s)

Invariant-gated state-projection theorem: if proj commutes with each oracle step under a state invariant inv that is preserved by every step, then it commutes with the full simulation starting from any state satisfying inv. This is the natural strengthening of map_run_simulateQ_eq_of_query_map_eq for projections that only agree on a reachable subset of states.

theorem OracleComp.simulateQ_run_preserves_inv_of_query {α : Type u} {ι ι' : Type} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {σ : Type u} (impl : QueryImpl spec (StateT σ (OracleComp spec'))) (inv : σ → Prop) (hinv : ∀ (t : spec.Domain) (s : σ), inv s → ∀ y ∈ support ((impl t).run s), inv y.2) (oa : OracleComp spec α) (s : σ) (hs : inv s) (y : α × σ) : y ∈ support ((simulateQ impl oa).run s) → inv y.2

Query-step invariant preservation lifts to any full simulation. This is the support-preservation half of map_run_simulateQ_eq_of_query_map_eq_inv', exposed separately for projected continuations after a simulated prefix.

theorem OracleComp.map_run_simulateQ_bind_eq_of_query_map_eq_inv' {α : Type u} {ι ι' : Type} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {σ₁ σ₂ β : Type u} (impl₁ : QueryImpl spec (StateT σ₁ (OracleComp spec'))) (impl₂ : QueryImpl spec (StateT σ₂ (OracleComp spec'))) (inv : σ₁ → Prop) (proj : σ₁ → σ₂) (hinv : ∀ (t : spec.Domain) (s : σ₁), inv s → ∀ y ∈ support ((impl₁ t).run s), inv y.2) (hproj : ∀ (t : spec.Domain) (s : σ₁), inv s → Prod.map id proj <$> (impl₁ t).run s = (impl₂ t).run (proj s)) (oa : OracleComp spec α) (k₁ : α → StateT σ₁ (OracleComp spec') β) (k₂ : α → StateT σ₂ (OracleComp spec') β) (hk : ∀ (x : α) (s : σ₁), inv s → Prod.map id proj <$> (k₁ x).run s = (k₂ x).run (proj s)) (s : σ₁) (hs : inv s) : Prod.map id proj <$> (simulateQ impl₁ oa >>= k₁).run s = (simulateQ impl₂ oa >>= k₂).run (proj s)

Invariant-gated state-projection theorem for a simulated prefix followed by a stateful continuation.

theorem OracleComp.run'_simulateQ_eq_of_query_map_eq_inv' {α : Type u} {ι ι' : Type} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {σ₁ σ₂ : Type u} (impl₁ : QueryImpl spec (StateT σ₁ (OracleComp spec'))) (impl₂ : QueryImpl spec (StateT σ₂ (OracleComp spec'))) (inv : σ₁ → Prop) (proj : σ₁ → σ₂) (hinv : ∀ (t : spec.Domain) (s : σ₁), inv s → ∀ y ∈ support ((impl₁ t).run s), inv y.2) (hproj : ∀ (t : spec.Domain) (s : σ₁), inv s → Prod.map id proj <$> (impl₁ t).run s = (impl₂ t).run (proj s)) (oa : OracleComp spec α) (s : σ₁) (hs : inv s) : (simulateQ impl₁ oa).run' s = (simulateQ impl₂ oa).run' (proj s)

run' projection corollary of map_run_simulateQ_eq_of_query_map_eq_inv'.

structure QueryImpl.StateOrnament {ι ι' : Type} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {σ τ : Type u_1} (decorated : QueryImpl spec (StateT σ (OracleComp spec'))) (base : QueryImpl spec (StateT τ (OracleComp spec'))) : Type u_1

A state ornament packages the data needed to project a decorated stateful query implementation onto a base implementation.

The decorated implementation may carry extra bookkeeping state. The projection only needs to commute with each query on states satisfying inv, and inv must be preserved by each query step.

• inv : σ → Prop
• proj : σ → τ
• preserves_inv (t : spec.Domain) (s : σ) : self.inv s → ∀ y ∈ support ((decorated t).run s), self.inv y.2
• project_step (t : spec.Domain) (s : σ) : self.inv s → Prod.map id self.proj <$> (decorated t).run s = (base t).run (self.proj s)

theorem QueryImpl.StateOrnament.run_eq {ι ι' : Type} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {σ τ : Type} {decorated : QueryImpl spec (StateT σ (OracleComp spec'))} {base : QueryImpl spec (StateT τ (OracleComp spec'))} {α : Type} (orn : decorated.StateOrnament base) (oa : OracleComp spec α) (s : σ) (hs : orn.inv s) : Prod.map id orn.proj <$> (simulateQ decorated oa).run s = (simulateQ base oa).run (orn.proj s)

A state ornament projects full simulations of the decorated implementation onto simulations of the base implementation.

theorem QueryImpl.StateOrnament.run'_eq {ι ι' : Type} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {σ τ : Type} {decorated : QueryImpl spec (StateT σ (OracleComp spec'))} {base : QueryImpl spec (StateT τ (OracleComp spec'))} {α : Type} (orn : decorated.StateOrnament base) (oa : OracleComp spec α) (s : σ) (hs : orn.inv s) : (simulateQ decorated oa).run' s = (simulateQ base oa).run' (orn.proj s)

Output-only corollary of QueryImpl.StateOrnament.run_eq.

Fixing one component of a product state

def 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.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 (impl.fixSndStateT 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.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 (impl.fixSndStateT q₀) oa).run' s

run' projection corollary of simulateQ_run_eq_of_snd_invariant.

Extending state with an auxiliary component

def QueryImpl.extendState {ι : Type u} {spec : OracleSpec ι} {σ Q : Type u} {m : Type u → Type v} [Monad m] (so : QueryImpl spec (StateT σ m)) (aux : (t : spec.Domain) → σ → spec.Range t → σ → Q → Q) : QueryImpl spec (StateT (σ × Q) m)

Extend a stateful query implementation with an auxiliary state component Q. The base implementation runs on the σ component. The auxiliary update may inspect the query input, the pre-state, the produced output, the post-state, and the old auxiliary value.

Inverse direction of QueryImpl.fixSndStateT: extendState adds a passive auxiliary, while fixSndStateT projects one away. Together they witness the universal property of the product state space.

@[simp]

theorem QueryImpl.extendState_apply {ι : Type u} {spec : OracleSpec ι} {σ Q : Type u} {m : Type u → Type v} [Monad m] (so : QueryImpl spec (StateT σ m)) (aux : (t : spec.Domain) → σ → spec.Range t → σ → Q → Q) (t : spec.Domain) (s : σ × Q) : (so.extendState aux t).run s = do let p ← (so t).run s.1 pure (p.1, p.2, aux t s.1 p.1 p.2 s.2)

def QueryImpl.extendStateLeft {ι : Type u} {spec : OracleSpec ι} {σ Q : Type u} {m : Type u → Type v} [Monad m] (so : QueryImpl spec (StateT σ m)) (aux : (t : spec.Domain) → σ → spec.Range t → σ → Q → Q) : QueryImpl spec (StateT (Q × σ) m)

Extend a stateful query implementation with an auxiliary component on the left of the product state. This is the same construction as extendState, but it matches handlers whose state is ordered as (auxiliary, baseState).

@[simp]

theorem QueryImpl.extendStateLeft_apply {ι : Type u} {spec : OracleSpec ι} {σ Q : Type u} {m : Type u → Type v} [Monad m] (so : QueryImpl spec (StateT σ m)) (aux : (t : spec.Domain) → σ → spec.Range t → σ → Q → Q) (t : spec.Domain) (s : Q × σ) : (so.extendStateLeft aux t).run s = do let p ← (so t).run s.2 pure (p.1, aux t s.2 p.1 p.2 s.1, p.2)

theorem OracleComp.extendState_run_proj_eq {α ι : Type u} {spec : OracleSpec ι} {σ Q : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (so : QueryImpl spec (StateT σ m)) (aux : (t : spec.Domain) → σ → spec.Range t → σ → Q → Q) (oa : OracleComp spec α) (s : σ) (q : Q) : Prod.map id Prod.fst <$> (simulateQ (so.extendState aux) oa).run (s, q) = (simulateQ so oa).run s

Forgetting the auxiliary Q component commutes with the full simulation. Running so.extendState aux and projecting away the Q component agrees with running so directly on the σ component, irrespective of the initial Q value or the auxiliary update.

This is the universal-property statement: the Q component is genuinely passive in the sense that it does not influence the σ-side of the simulation.

theorem OracleComp.extendState_run'_eq {α ι : Type u} {spec : OracleSpec ι} {σ Q : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (so : QueryImpl spec (StateT σ m)) (aux : (t : spec.Domain) → σ → spec.Range t → σ → Q → Q) (oa : OracleComp spec α) (s : σ) (q : Q) : (simulateQ (so.extendState aux) oa).run' (s, q) = (simulateQ so oa).run' s

run' projection corollary of extendState_run_proj_eq: dropping both the auxiliary Q and the σ state of the extended simulation gives the same output distribution as the base simulation.

theorem OracleComp.extendStateLeft_run_proj_eq {α ι : Type u} {spec : OracleSpec ι} {σ Q : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (so : QueryImpl spec (StateT σ m)) (aux : (t : spec.Domain) → σ → spec.Range t → σ → Q → Q) (oa : OracleComp spec α) (s : σ) (q : Q) : Prod.map id Prod.snd <$> (simulateQ (so.extendStateLeft aux) oa).run (q, s) = (simulateQ so oa).run s

Forgetting the left auxiliary Q component commutes with the full simulation. This is the left-product analogue of extendState_run_proj_eq.

theorem OracleComp.extendStateLeft_run'_eq {α ι : Type u} {spec : OracleSpec ι} {σ Q : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (so : QueryImpl spec (StateT σ m)) (aux : (t : spec.Domain) → σ → spec.Range t → σ → Q → Q) (oa : OracleComp spec α) (s : σ) (q : Q) : (simulateQ (so.extendStateLeft aux) oa).run' (q, s) = (simulateQ so oa).run' s

run' projection corollary of extendStateLeft_run_proj_eq.