WriterT ω Invariant Theory

Support-based invariant reasoning for query-implementations 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 ω).

These statements mirror QueryImpl.PreservesInv / OracleComp.simulateQ_run_preservesInv from SimSemantics/StateT/PreservesInv.lean, with the writer log playing the role of the threaded state.

Main definitions

• 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.WriterPreservesInv {ι : Type} {spec : OracleSpec ι} [spec.IsUniformSpec] {ω : 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 ι} [spec.IsUniformSpec] {ω : Type} [Monoid ω] (impl : QueryImpl spec (WriterT ω (OracleComp spec))) : impl.WriterPreservesInv fun (x : ω) => True

theorem QueryImpl.WriterPreservesInv.and {ι : Type} {spec : OracleSpec ι} [spec.IsUniformSpec] {ω : 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 ι} [spec.IsUniformSpec] {ω : 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 ι} [spec.IsUniformSpec] {ω : 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 ι} [spec.IsUniformSpec] {ω α : 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).