feat(Control/Monad): Weakest preconditions and mcvgen for free monads by tannerduve · Pull Request #604 · leanprover/cslib

tannerduve · 2026-05-28T05:31:02Z

This PR adds Cslib/Foundations/Control/Monad/Free/WP.lean, equipping FreeM-based monads with a Std.Do.WP interpretation and hooking them into Std.Do.Triple and mvcgen.

A logical handler LHandler F ps assigns each operation of the effect signature F a PredTrans ps specification. Since PredTrans ps is a monad and FreeM is free, the universal property of FreeM extends a handler uniquely to a monad morphism FreeM F → PredTrans ps. This morphism, wpH H = liftM H.run, is the weakest precondition and is compositional wrt the monadic structure.

A HasHandler F ps typeclass selects a default handler for F and induces WP (FreeM F) ps and WPMonad (FreeM F) ps instances, so that Std.Do.Triple and mvcgen apply to FreeM F programs.

Handlers are provided for cslib's existing FreeState and FreeReader, along with @[spec] lemmas Spec.get_FreeState, Spec.set_FreeState, and Spec.read_FreeReader that let mvcgen step through state and reader programs.

CslibTests/FreeMonadWP.lean contains example Triples discharged by mvcgen, covering the supplied state and reader handlers, and multiple custom effects

The design follows Vistrup, Sammler, Jung, Program Logics à la Carte (POPL 2025), which uses coinductive free monads (ITrees) and Iris separation logic. Here we use inductive free monads and Std.Do program logic.

Add `Cslib.Foundations.Control.Monad.Free.WP`: a weakest-precondition framework for `FreeM`-based effectful programs via Std.Do's predicate-transformer monad `PredTrans ps`. A logical effect handler `LHandler F ps` lifts through the universal property of `FreeM` to a unique monad morphism `wpH H : FreeM F → PredTrans ps`. Structural rules (`wpH_pure`, `wpH_lift`, `wpH_bind`) follow from `liftM` being a monad morphism, and the adequacy theorem `wpH_ofInterp_eq_wp_liftM` identifies WP-via-handler with Std.Do's WP of the `liftM` interpretation. Handlers and @[spec] lemmas for the existing `StateF` and `ReaderF` effects let `mvcgen` step through `FreeState`/`FreeReader` programs. `CslibTests/FreeMonadWP` demonstrates: `FreeState` triples, a custom counter effect, `FailF` and `DemonicF` effect signatures with logical handlers, sum composition via `LHandler.sum`, and multi-effect triples discharged by `mvcgen`. Follows Vistrup–Sammler–Jung, *Program Logics à la Carte* (POPL 2025), adapted from coinductive ITrees to inductive `FreeM` and from Iris to Std.Do.

tannerduve requested review from chenson2018 and fmontesi as code owners May 28, 2026 05:31

tannerduve force-pushed the feat/free-logic branch 2 times, most recently from d3d44c8 to d3b6959 Compare May 28, 2026 06:01

eric-wieser reviewed May 28, 2026

View reviewed changes