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, which gives FreeM programs a Std.Do.WP interpretation by lifting logical handlers into the predicate-transformer monad PredTrans.

A logical handler {ι : Type u} → F ι → PredTrans ps ι assigns each operation of the effect signature F a PredTrans ps specification. Since PredTrans ps is a monad and FreeM is free, FreeM.liftM extends such a handler to a monad morphism FreeM F → PredTrans ps; this is the weakest precondition and is compositional wrt the monadic structure.

A FreeM.WP 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. The main coherence lemma is FreeM.liftM_wp_eq_wp_liftM, and FreeM.wp_lift exposes the one-operation case.

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, custom effects, combined effects, and demonic choice.

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.

Address review feedback: - inline `wpH`, the `LHandler` abbrev/namespace, and `LHandler.ofInterp`; handlers are now plain `F ι → PredTrans ps ι` functions - rename the `HasHandler` class to `FreeM.WP` - restate the adequacy lemma directly on `liftM` as `liftM_wp_eq_wp_liftM`

…, naming - Make FreeM.WP a protected class so bare `WP` resolves to Std.Do.WP; rename instances to WP.toDoWP / anonymous WPMonad instance. - Add `wp_lift` and the adequacy lemma `ensures_liftM_of_wp`; reframe `liftM_wp_eq_wp_liftM` as the coherence/uniqueness lemma it is. - Inline StateF/ReaderF logical handlers into their WP instances. - Rename `wp_FreeState_eq_wp_toStateM` / `wp_FreeReader_eq_wp_toReaderM` to lowerCamel `wp_freeState_*` / `wp_freeReader_*`. - Use pattern-matching lambdas for FailF/DemonicF handlers in tests. - Add VistrupSammlerJung2025 to references.bib.

eric-wieser · 2026-06-18T20:51:51Z

Please update the PR description to reflect what's currently here.

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

Comment thread Cslib/Foundations/Control/Monad/Free/WP.lean Outdated

tannerduve force-pushed the feat/free-logic branch from d3b6959 to a00790f Compare May 28, 2026 06:13

eric-wieser reviewed May 28, 2026

View reviewed changes

Comment thread Cslib/Foundations/Control/Monad/Free/WP.lean Outdated

tannerduve force-pushed the feat/free-logic branch from a00790f to 07774bb Compare May 28, 2026 06:28

eric-wieser reviewed May 28, 2026

View reviewed changes

Comment thread Cslib/Foundations/Control/Monad/Free/WP.lean Outdated

eric-wieser reviewed May 28, 2026

View reviewed changes

Comment thread Cslib/Foundations/Control/Monad/Free/WP.lean Outdated

eric-wieser reviewed May 28, 2026

View reviewed changes

Comment thread Cslib/Foundations/Control/Monad/Free/WP.lean Outdated

tannerduve mentioned this pull request Jun 2, 2026

feat(FreeWP): weakest preconditions for FreeM via Std.Do Shreyas4991/Algolean#62

Merged

eric-wieser reviewed Jun 15, 2026

View reviewed changes