StateT σ ProbComp Invariant Theory

Support-based invariant reasoning for shared, stateful oracle simulations (ROM/AGM/hybrids) whose handlers live in StateT σ ProbComp. A user-supplied predicate Inv : σ → Prop is preserved by an implementation when every reachable post-state satisfies it.

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

The WriterT analogue of this theory lives in SimSemantics/WriterT/PreservesInv.lean.

Main definitions

• 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
• InitSatisfiesInv — every sampled initial state satisfies the invariant
• 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

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) (hmyNoFail : my.NeverFailsUnder Inv) (σ0 : σ) : Inv σ0 → 𝒟[do let us ← my.run σ0 mx.run' us.2] = 𝒟[mx.run' σ0]

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