Skip to content

Commit a00790f

Browse files
tannerduvetannerduve
committed
feat(Control/Monad/Free): weakest preconditions for FreeM
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.
1 parent d780a2a commit a00790f

4 files changed

Lines changed: 410 additions & 0 deletions

File tree

‎Cslib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,7 @@ public import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey
5050
public import Cslib.Foundations.Control.Monad.Free
5151
public import Cslib.Foundations.Control.Monad.Free.Effects
5252
public import Cslib.Foundations.Control.Monad.Free.Fold
53+
public import Cslib.Foundations.Control.Monad.Free.WP
5354
public import Cslib.Foundations.Data.BiTape
5455
public import Cslib.Foundations.Data.DecidableEqZero
5556
public import Cslib.Foundations.Data.FinFun.Basic

‎Cslib/Foundations/Control/Monad/Free/WP.lean‎

Lines changed: 178 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,178 @@
1+
/-
2+
Copyright (c) 2025 Tanner Duve (Logical Intelligence). All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Tanner Duve
5+
-/
6+
7+
module
8+
9+
public import Cslib.Foundations.Control.Monad.Free
10+
public import Cslib.Foundations.Control.Monad.Free.Effects
11+
public import Std.Do.PredTrans
12+
public import Std.Do.WP.Basic
13+
public import Std.Do.WP.Monad
14+
public import Std.Do.Triple
15+
16+
/-!
17+
# Weakest preconditions for `FreeM` programs
18+
19+
Weakest-precondition interpretation of `FreeM F` programs through `Std.Do`'s
20+
predicate-transformer monad `PredTrans ps`. The universal property of `FreeM` lifts any
21+
effect handler `F ι → PredTrans ps ι` to a unique monad morphism `wpH H = liftM H.run`,
22+
so weakest preconditions are compositional in `FreeM`'s monadic structure. An
23+
`[LHandler F ps]` instance plugs `FreeM F` into `Std.Do`'s `WP`/`WPMonad`/`Triple`
24+
infrastructure.
25+
26+
The WP's structural rules (`wpH_pure`, `wpH_bind`, …) are immediate from `liftM` being a monad
27+
morphism; the adequacy theorem `wpH_ofInterp_eq_wp_liftM` — that WP-via-handler agrees with
28+
`Std.Do`'s WP of the `liftM` interpretation — is the same statement of uniqueness.
29+
30+
The design follows [Vistrup, Sammler, Jung. *Program Logics à la Carte.* POPL 2025], adapted
31+
from coinductive ITrees to inductive `FreeM` and from Iris to `Std.Do`.
32+
-/
33+
34+
@[expose] public section
35+
36+
set_option mvcgen.warning false
37+
38+
namespace Cslib
39+
40+
open Std.Do
41+
42+
namespace FreeM
43+
44+
universe u v w
45+
46+
variable {F G : Type u → Type v} {ps : PostShape.{u}} {α β : Type u}
47+
48+
/-- A logical effect handler: an effect handler from `F` into the predicate-transformer monad
49+
`PredTrans ps`. Wrapped in a structure to isolate the implicit `ι`-binder from class resolution
50+
at use sites. -/
51+
structure LHandler (F : Type u → Type v) (ps : PostShape.{u}) : Type (max (u + 1) v) where
52+
/-- The assignment from operations to predicate transformers. -/
53+
run {ι : Type u} : F ι → PredTrans ps ι
54+
55+
namespace LHandler
56+
57+
/-- Sum of handlers; the counterpart of the paper's `H₁ ⊕ H₂`. -/
58+
def sum (H₁ : LHandler F ps) (H₂ : LHandler G ps) :
59+
LHandler (fun α => F α ⊕ G α) ps where
60+
run op := match op with
61+
| .inl x => H₁.run x
62+
| .inr y => H₂.run y
63+
64+
@[simp] theorem sum_run_inl (H₁ : LHandler F ps) (H₂ : LHandler G ps)
65+
{ι : Type u} (x : F ι) :
66+
(LHandler.sum H₁ H₂).run (Sum.inl x : F ι ⊕ G ι) = H₁.run x := rfl
67+
68+
@[simp] theorem sum_run_inr (H₁ : LHandler F ps) (H₂ : LHandler G ps)
69+
{ι : Type u} (y : G ι) :
70+
(LHandler.sum H₁ H₂).run (Sum.inr y : F ι ⊕ G ι) = H₂.run y := rfl
71+
72+
/-- Derive a logical handler from an effect handler into any `[WP m ps]` monad, by composing
73+
with `m`'s WP. -/
74+
def ofInterp {m : Type u → Type w} [WP m ps]
75+
(interp : ∀ ι : Type u, F ι → m ι) : LHandler F ps where
76+
run {ι} op := wp (interp ι op)
77+
78+
@[simp] theorem ofInterp_run {m : Type u → Type w} [WP m ps]
79+
(interp : ∀ ι : Type u, F ι → m ι) {ι : Type u} (op : F ι) :
80+
(LHandler.ofInterp interp).run op = wp (interp ι op) := rfl
81+
82+
end LHandler
83+
84+
/-- Weakest-precondition interpretation of a `FreeM F α` program against a logical handler `H`.
85+
Defined as `FreeM.liftM` instantiated at `PredTrans ps`, the unique monad morphism
86+
`FreeM F → PredTrans ps` extending `H` per the universal property of `FreeM`. -/
87+
def wpH (H : LHandler F ps) (x : FreeM F α) : PredTrans ps α :=
88+
x.liftM (fun {_} => H.run)
89+
90+
@[simp] theorem wpH_pure (H : LHandler F ps) (a : α) :
91+
wpH H (pure a : FreeM F α) = Pure.pure a := rfl
92+
93+
@[simp] theorem wpH_liftBind (H : LHandler F ps) {ι : Type u}
94+
(op : F ι) (k : ι → FreeM F α) :
95+
wpH H (lift op >>= k) = H.run op >>= fun x => wpH H (k x) := rfl
96+
97+
@[simp] theorem wpH_lift (H : LHandler F ps) {ι : Type u} (op : F ι) :
98+
wpH H (lift op : FreeM F ι) = H.run op :=
99+
liftM_lift _ op
100+
101+
@[simp] theorem wpH_bind (H : LHandler F ps) (x : FreeM F α) (f : α → FreeM F β) :
102+
wpH H (x >>= f) = wpH H x >>= fun a => wpH H (f a) :=
103+
liftM_bind _ x f
104+
105+
/-- Adequacy theorem: WP via `FreeM` against an `ofInterp`-derived handler agrees with
106+
`Std.Do`'s WP of the `liftM` interpretation. Equivalently, two monad morphisms
107+
`FreeM F → PredTrans ps` extending the same handler are equal. -/
108+
theorem wpH_ofInterp_eq_wp_liftM
109+
{m : Type u → Type w} [Monad m] [LawfulMonad m] [WPMonad m ps]
110+
(interp : ∀ ι : Type u, F ι → m ι) (x : FreeM F α) :
111+
wpH (LHandler.ofInterp interp) x = wp (x.liftM (fun {_} => interp _)) := by
112+
induction x with
113+
| pure a => simp [wpH, FreeM.liftM, WPMonad.wp_pure]
114+
| lift_bind op k ih =>
115+
simp [WPMonad.wp_bind, ih]
116+
117+
/-- Records a default logical handler for `F` at shape `ps`, enabling the global
118+
`WP (FreeM F) ps` instance and any `Triple`/`mvcgen` reasoning over `FreeM F`. -/
119+
class HasHandler (F : Type u → Type v) (ps : outParam (PostShape.{u})) where
120+
/-- The default logical handler for `F`. -/
121+
handler : LHandler F ps
122+
123+
instance instWPFreeM [HasHandler F ps] : WP (FreeM F) ps where
124+
wp := wpH HasHandler.handler
125+
126+
instance instWPMonadFreeM [HasHandler F ps] : WPMonad (FreeM F) ps where
127+
wp_pure _ := rfl
128+
wp_bind x f := wpH_bind _ x f
129+
130+
/-- Logical handler for the state effect, induced by `Std.Do`'s `WP (StateM σ)`. -/
131+
def StateF.handler {σ : Type u} : LHandler (StateF σ) (.arg σ .pure) :=
132+
LHandler.ofInterp (m := StateM σ) (fun _ op => FreeState.stateInterp op)
133+
134+
instance StateF.instHasHandler {σ : Type u} :
135+
HasHandler (StateF σ) (.arg σ .pure) where
136+
handler := StateF.handler
137+
138+
/-- WP of a `FreeState` program matches WP of its `StateM` interpretation. -/
139+
theorem StateF.wp_FreeState_eq_wp_toStateM {σ : Type u} (comp : FreeState σ α) :
140+
wp comp = wp (FreeState.toStateM comp) :=
141+
wpH_ofInterp_eq_wp_liftM (m := StateM σ)
142+
(fun _ op => FreeState.stateInterp op) comp
143+
144+
/-- Hoare spec for `get` on `FreeState`. -/
145+
@[spec]
146+
theorem Spec.get_FreeState {σ : Type u} {Q : PostCond σ (.arg σ .pure)} :
147+
Triple (MonadStateOf.get : FreeState σ σ) (spred(fun s => Q.1 s s)) Q := by
148+
mvcgen
149+
150+
/-- Hoare spec for `set` on `FreeState`. -/
151+
@[spec]
152+
theorem Spec.set_FreeState {σ : Type u} (s : σ) {Q : PostCond PUnit (.arg σ .pure)} :
153+
Triple (MonadStateOf.set s : FreeState σ PUnit) (spred(fun _ => Q.1 ⟨⟩ s)) Q := by
154+
mvcgen
155+
156+
/-- Logical handler for the reader effect, induced by `Std.Do`'s `WP (ReaderM σ)`. -/
157+
def ReaderF.handler {σ : Type u} : LHandler (ReaderF σ) (.arg σ .pure) :=
158+
LHandler.ofInterp (m := ReaderM σ) (fun _ op => FreeReader.readInterp op)
159+
160+
instance ReaderF.instHasHandler {σ : Type u} :
161+
HasHandler (ReaderF σ) (.arg σ .pure) where
162+
handler := ReaderF.handler
163+
164+
/-- WP of a `FreeReader` program matches WP of its `ReaderM` interpretation. -/
165+
theorem ReaderF.wp_FreeReader_eq_wp_toReaderM {σ : Type u} (comp : FreeReader σ α) :
166+
wp comp = wp (FreeReader.toReaderM comp) :=
167+
wpH_ofInterp_eq_wp_liftM (m := ReaderM σ)
168+
(fun _ op => FreeReader.readInterp op) comp
169+
170+
/-- Hoare spec for `read` on `FreeReader`. -/
171+
@[spec]
172+
theorem Spec.read_FreeReader {ρ : Type u} {Q : PostCond ρ (.arg ρ .pure)} :
173+
Triple (MonadReaderOf.read : FreeReader ρ ρ) (spred(fun r => Q.1 r r)) Q := by
174+
mvcgen
175+
176+
end FreeM
177+
178+
end Cslib

‎CslibTests.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ public import CslibTests.CCS
55
public import CslibTests.CLL
66
public import CslibTests.DFA
77
public import CslibTests.FreeMonad
8+
public import CslibTests.FreeMonadWP
89
public import CslibTests.GrindLint
910
public import CslibTests.HML
1011
public import CslibTests.HasFresh

0 commit comments

Comments
 (0)