Oracle State Invariants for Shared-Oracle Simulations

This module provides minimal, model-agnostic infrastructure for reasoning about shared, stateful oracle simulations (ROM/AGM/hybrids) via a user-supplied invariant Inv : σ → Prop on oracle states.

We use support-based formulations (rather than Pr[ ...] = 1) to keep downstream proofs lightweight.

Main definitions

• InitSatisfiesInv — every sampled initial state satisfies the invariant
• QueryImpl.PreservesInv — every oracle query implementation step preserves Inv
• OracleComp.simulateQ_run_preservesInv — simulating any oracle computation with a preserving implementation preserves Inv on the final state
• StateT.StatePreserving — computation never changes the state
• StateT.PreservesInv — computation preserves an invariant on the state
• StateT.NeverFailsUnder — computation does not fail under an invariant
• StateT.OutputIndependent — output distribution is independent of the initial state under an invariant
• StateT.outputIndependent_after_preservesInv — non-interference: output-independent computation remains so after sequencing with an invariant-preserving computation
• QueryImpl.WriterPreservesInv — every oracle query implementation step preserves an invariant Inv : ω → Prop on the accumulated writer output (for WriterT ω handlers with [Monoid ω])
• OracleComp.simulateQ_run_writerPreservesInv — simulating any oracle computation with a writer-invariant-preserving implementation preserves Inv on the final accumulated writer value

def QueryImpl.PreservesInv {ι : Type} {spec : OracleSpec ι} {σ : Type} (impl : QueryImpl spec (StateT σ ProbComp)) (Inv : σ → Prop) : Prop

PreservesInv impl Inv means every oracle query implementation step preserves Inv on all reachable post-states (support-based).

theorem QueryImpl.PreservesInv.trivial {ι : Type} {spec : OracleSpec ι} {σ : Type} (impl : QueryImpl spec (StateT σ ProbComp)) : impl.PreservesInv fun (x : σ) => True

theorem QueryImpl.PreservesInv.and {ι : Type} {spec : OracleSpec ι} {σ : Type} {impl : QueryImpl spec (StateT σ ProbComp)} {P Q : σ → Prop} (hP : impl.PreservesInv P) (hQ : impl.PreservesInv Q) : impl.PreservesInv fun (s : σ) => P s ∧ Q s

theorem QueryImpl.PreservesInv.of_forall {ι : Type} {spec : OracleSpec ι} {σ : Type} {impl : QueryImpl spec (StateT σ ProbComp)} {Inv : σ → Prop} (h : ∀ (t : spec.Domain) (σ0 : σ), ∀ z ∈ support ((impl t).run σ0), Inv z.2) : impl.PreservesInv Inv

theorem OracleComp.simulateQ_run_preservesInv {ι : Type} {spec : OracleSpec ι} {σ α : Type} (impl : QueryImpl spec (StateT σ ProbComp)) (Inv : σ → Prop) (himpl : impl.PreservesInv Inv) (oa : OracleComp spec α) (σ0 : σ) : Inv σ0 → ∀ z ∈ support ((simulateQ impl oa).run σ0), Inv z.2

If impl preserves Inv, then simulating any oracle computation with simulateQ impl preserves Inv on the final state (support-wise).

theorem QueryImpl.PreservesInv.compose {ι ι' : Type} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {σ : Type} {so' : QueryImpl spec' (StateT σ ProbComp)} {so : QueryImpl spec (OracleComp spec')} {Inv : σ → Prop} (h : so'.PreservesInv Inv) : (so' ∘ₛ so).PreservesInv Inv

If so' preserves Inv, then so' ∘ₛ so also preserves Inv for any so.

def InitSatisfiesInv {σ : Type} (init : ProbComp σ) (Inv : σ → Prop) : Prop

InitSatisfiesInv init Inv means every possible initial state sampled by init satisfies Inv (support-based).

StateT invariant properties

These properties are useful for non-interference arguments in sequential composition proofs. They are stated for general StateT σ ProbComp computations.

def StateT.StatePreserving {σ α : Type} (mx : StateT σ ProbComp α) : Prop

StatePreserving mx means mx never changes the state: for every starting state σ0, every outcome in the support of mx.run σ0 has final state equal to σ0.

def StateT.PreservesInv {σ α : Type} (mx : StateT σ ProbComp α) (Inv : σ → Prop) : Prop

PreservesInv mx Inv means that starting from any state satisfying Inv, every reachable post-state (support-wise) also satisfies Inv.

def StateT.NeverFailsUnder {σ α : Type} (mx : StateT σ ProbComp α) (Inv : σ → Prop) : Prop

NeverFailsUnder mx Inv means that starting from any state satisfying Inv, the computation does not fail (its failure probability is 0).

def StateT.OutputIndependent {σ α : Type} (mx : StateT σ ProbComp α) (Inv : σ → Prop) : Prop

OutputIndependent mx Inv means the output distribution of mx does not depend on the initial state, as long as the initial state satisfies Inv.

This is distributional equality of run' (which discards the final state).

@[simp]

theorem StateT.statePreserving_pure {σ α : Type} (a : α) : (pure a).StatePreserving

@[simp]

theorem StateT.outputIndependent_pure {σ α : Type} (Inv : σ → Prop) (a : α) : (pure a).OutputIndependent Inv

theorem StateT.statePreserving_bind {σ α β : Type} (mx : StateT σ ProbComp α) (my : α → StateT σ ProbComp β) (h₁ : mx.StatePreserving) (h₂ : ∀ (a : α), (my a).StatePreserving) : (mx >>= my).StatePreserving

theorem StateT.preservesInv_of_statePreserving {σ α : Type} (mx : StateT σ ProbComp α) (Inv : σ → Prop) (h : mx.StatePreserving) : mx.PreservesInv Inv

theorem StateT.preservesInv_bind {σ α β : Type} (mx : StateT σ ProbComp α) (my : α → StateT σ ProbComp β) (Inv : σ → Prop) (h₁ : mx.PreservesInv Inv) (h₂ : ∀ (a : α), (my a).PreservesInv Inv) : (mx >>= my).PreservesInv Inv

theorem StateT.outputIndependent_after_preservesInv {σ α β : Type} (mx : StateT σ ProbComp α) (my : StateT σ ProbComp β) (Inv : σ → Prop) (hmx : mx.OutputIndependent Inv) (hmyInv : my.PreservesInv Inv) (σ0 : σ) : Inv σ0 → (evalDist do let us ← my.run σ0 mx.run' us.2) = evalDist (mx.run' σ0)

If mx is output-independent on Inv, and my preserves Inv and never fails, then the output distribution of mx is unchanged by running my first and then running mx on the resulting state.

WriterT invariant properties

These properties mirror QueryImpl.PreservesInv / OracleComp.simulateQ_run_preservesInv for handlers that accumulate a writer log in a monoid ω (as opposed to threading state through StateT). Typical use-cases include countingOracle (with ω = QueryCount ι) and costOracle (with an arbitrary Monoid ω).

def QueryImpl.WriterPreservesInv {ι : Type} {spec : OracleSpec ι} {ω : Type} [Monoid ω] (impl : QueryImpl spec (WriterT ω (OracleComp spec))) (Inv : ω → Prop) : Prop

WriterPreservesInv impl Inv means every oracle query implementation step preserves Inv on the accumulated writer: starting from any s₀ satisfying Inv, every reachable post-writer s₀ * w (for (a, w) in the support of (impl t).run) also satisfies Inv.

theorem QueryImpl.WriterPreservesInv.trivial {ι : Type} {spec : OracleSpec ι} {ω : Type} [Monoid ω] (impl : QueryImpl spec (WriterT ω (OracleComp spec))) : impl.WriterPreservesInv fun (x : ω) => True

theorem QueryImpl.WriterPreservesInv.and {ι : Type} {spec : OracleSpec ι} {ω : Type} [Monoid ω] {impl : QueryImpl spec (WriterT ω (OracleComp spec))} {P Q : ω → Prop} (hP : impl.WriterPreservesInv P) (hQ : impl.WriterPreservesInv Q) : impl.WriterPreservesInv fun (s : ω) => P s ∧ Q s

theorem QueryImpl.WriterPreservesInv.of_forall {ι : Type} {spec : OracleSpec ι} {ω : Type} [Monoid ω] {impl : QueryImpl spec (WriterT ω (OracleComp spec))} {Inv : ω → Prop} (h : ∀ (t : spec.Domain) (s₀ : ω), ∀ z ∈ support (impl t).run, Inv (s₀ * z.2)) : impl.WriterPreservesInv Inv

WriterPreservesInv from an unconditional per-query witness. Analogous to PreservesInv.of_forall: if every reachable increment z.2 satisfies Inv (s₀ * z.2) for any starting s₀ regardless of whether Inv s₀ holds, then Inv is preserved.

theorem QueryImpl.WriterPreservesInv.of_mul_closed {ι : Type} {spec : OracleSpec ι} {ω : Type} [Monoid ω] {impl : QueryImpl spec (WriterT ω (OracleComp spec))} {Inv : ω → Prop} (hClosed : ∀ (a b : ω), Inv a → Inv b → Inv (a * b)) (hPerQuery : ∀ (t : spec.Domain), ∀ z ∈ support (impl t).run, Inv z.2) : impl.WriterPreservesInv Inv

WriterPreservesInv from a multiplicatively-closed predicate.

If Inv holds on every writer increment w produced by a single query (hPerQuery) and is closed under * (hClosed), then Inv is preserved across the whole simulation. This is the canonical builder for writer invariants: pick a submonoid-like predicate, show every per-query increment lands in it, and you're done.

Note on composition. Unlike PreservesInv.compose, we do not provide a compose analogue for WriterPreservesInv: the definition is keyed to a single spec appearing both as the source of queries and as the inner OracleComp spec monad of the writer. Composition via ∘ₛ changes the query spec but not the inner writer monad, so the composite signature no longer matches WriterPreservesInv's. The intended idiom is to compose on the underlying OracleComp layer (e.g. via simulateQ_compose) and then apply simulateQ_run_writerPreservesInv to the composite computation.

theorem OracleComp.simulateQ_run_writerPreservesInv {ι : Type} {spec : OracleSpec ι} {ω α : Type} [Monoid ω] (impl : QueryImpl spec (WriterT ω (OracleComp spec))) (Inv : ω → Prop) (himpl : impl.WriterPreservesInv Inv) (oa : OracleComp spec α) (s₀ : ω) : Inv s₀ → ∀ z ∈ support (simulateQ impl oa).run, Inv (s₀ * z.2)

If impl preserves the writer invariant Inv, then simulating any oracle computation with simulateQ impl preserves Inv on the final accumulated writer (support-wise).