Skip to content

Commit d3d44c8

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 d3d44c8

4 files changed

Lines changed: 418 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: 188 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,188 @@
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+
namespace Cslib
37+
38+
open Std.Do
39+
40+
namespace FreeM
41+
42+
universe u v w
43+
44+
variable {F G : Type u → Type v} {ps : PostShape.{u}} {α β : Type u}
45+
46+
/-- A logical effect handler: an effect handler from `F` into the predicate-transformer monad
47+
`PredTrans ps`. The "logical" qualifier distinguishes these from executable handlers into
48+
concrete computational monads. Wrapped in a structure to isolate the implicit `ι`-binder from
49+
class resolution at use sites. -/
50+
structure LHandler (F : Type u → Type v) (ps : PostShape.{u}) : Type (max (u + 1) v) where
51+
/-- The assignment from operations to predicate transformers. -/
52+
run {ι : Type u} : F ι → PredTrans ps ι
53+
54+
namespace LHandler
55+
56+
/-- Sum of handlers; the counterpart of the paper's `H₁ ⊕ H₂`. -/
57+
def sum (H₁ : LHandler F ps) (H₂ : LHandler G ps) :
58+
LHandler (fun α => F α ⊕ G α) ps where
59+
run op := match op with
60+
| .inl x => H₁.run x
61+
| .inr y => H₂.run y
62+
63+
@[simp] theorem sum_run_inl (H₁ : LHandler F ps) (H₂ : LHandler G ps)
64+
{ι : Type u} (x : F ι) :
65+
(LHandler.sum H₁ H₂).run (Sum.inl x : F ι ⊕ G ι) = H₁.run x := rfl
66+
67+
@[simp] theorem sum_run_inr (H₁ : LHandler F ps) (H₂ : LHandler G ps)
68+
{ι : Type u} (y : G ι) :
69+
(LHandler.sum H₁ H₂).run (Sum.inr y : F ι ⊕ G ι) = H₂.run y := rfl
70+
71+
/-- Derive a logical handler from an effect handler into any `[WP m ps]` monad, by composing
72+
with `m`'s WP. -/
73+
def ofInterp {m : Type u → Type w} [WP m ps]
74+
(interp : ∀ ι : Type u, F ι → m ι) : LHandler F ps where
75+
run {ι} op := wp (interp ι op)
76+
77+
@[simp] theorem ofInterp_run {m : Type u → Type w} [WP m ps]
78+
(interp : ∀ ι : Type u, F ι → m ι) {ι : Type u} (op : F ι) :
79+
(LHandler.ofInterp interp).run op = wp (interp ι op) := rfl
80+
81+
end LHandler
82+
83+
/-- Weakest-precondition interpretation of a `FreeM F α` program against a logical handler `H`.
84+
Defined as `FreeM.liftM` instantiated at `PredTrans ps`, the unique monad morphism
85+
`FreeM F → PredTrans ps` extending `H` per the universal property of `FreeM`. -/
86+
def wpH (H : LHandler F ps) (x : FreeM F α) : PredTrans ps α :=
87+
x.liftM (fun {_} => H.run)
88+
89+
@[simp] theorem wpH_pure (H : LHandler F ps) (a : α) :
90+
wpH H (.pure a : FreeM F α) = Pure.pure a := rfl
91+
92+
@[simp] theorem wpH_liftBind (H : LHandler F ps) {ι : Type u}
93+
(op : F ι) (k : ι → FreeM F α) :
94+
wpH H (.liftBind op k) = H.run op >>= fun x => wpH H (k x) := rfl
95+
96+
@[simp] theorem wpH_lift (H : LHandler F ps) {ι : Type u} (op : F ι) :
97+
wpH H (lift op : FreeM F ι) = H.run op :=
98+
liftM_lift _ op
99+
100+
@[simp] theorem wpH_bind (H : LHandler F ps) (x : FreeM F α) (f : α → FreeM F β) :
101+
wpH H (x >>= f) = wpH H x >>= fun a => wpH H (f a) :=
102+
liftM_bind _ x f
103+
104+
/-- Lift an `F`-operation through the sum handler reduces to running it under `H₁`. -/
105+
@[simp] theorem wpH_lift_sum_inl (H₁ : LHandler F ps) (H₂ : LHandler G ps)
106+
{ι : Type u} (op : F ι) :
107+
wpH (H₁.sum H₂) (lift (Sum.inl op : F ι ⊕ G ι)) = H₁.run op := by
108+
simp
109+
110+
/-- Lift a `G`-operation through the sum handler reduces to running it under `H₂`. -/
111+
@[simp] theorem wpH_lift_sum_inr (H₁ : LHandler F ps) (H₂ : LHandler G ps)
112+
{ι : Type u} (op : G ι) :
113+
wpH (H₁.sum H₂) (lift (Sum.inr op : F ι ⊕ G ι)) = H₂.run op := by
114+
simp
115+
116+
/-- Adequacy theorem: WP via `FreeM` against an `ofInterp`-derived handler agrees with
117+
`Std.Do`'s WP of the `liftM` interpretation. Equivalently, two monad morphisms
118+
`FreeM F → PredTrans ps` extending the same handler are equal. -/
119+
theorem wpH_ofInterp_eq_wp_liftM
120+
{m : Type u → Type w} [Monad m] [LawfulMonad m] [WPMonad m ps]
121+
(interp : ∀ ι : Type u, F ι → m ι) (x : FreeM F α) :
122+
wpH (LHandler.ofInterp interp) x = wp (x.liftM (fun {_} => interp _)) := by
123+
induction x with
124+
| pure a => simp [wpH, FreeM.liftM, WPMonad.wp_pure]
125+
| lift_bind op k ih =>
126+
simp [WPMonad.wp_bind, ih]
127+
128+
/-- Records a default logical handler for `F` at shape `ps`, enabling the global
129+
`WP (FreeM F) ps` instance and any `Triple`/`mvcgen` reasoning over `FreeM F`. -/
130+
class HasHandler (F : Type u → Type v) (ps : outParam (PostShape.{u})) where
131+
handler : LHandler F ps
132+
133+
instance instWPFreeM [HasHandler F ps] : WP (FreeM F) ps where
134+
wp := wpH HasHandler.handler
135+
136+
instance instWPMonadFreeM [HasHandler F ps] : WPMonad (FreeM F) ps where
137+
wp_pure _ := rfl
138+
wp_bind x f := wpH_bind _ x f
139+
140+
/-- Logical handler for the state effect, induced by `Std.Do`'s `WP (StateM σ)`. -/
141+
def StateF.handler {σ : Type u} : LHandler (StateF σ) (.arg σ .pure) :=
142+
LHandler.ofInterp (m := StateM σ) (fun _ op => FreeState.stateInterp op)
143+
144+
instance StateF.instHasHandler {σ : Type u} :
145+
HasHandler (StateF σ) (.arg σ .pure) where
146+
handler := StateF.handler
147+
148+
/-- WP of a `FreeState` program matches WP of its `StateM` interpretation. -/
149+
theorem StateF.wp_FreeState_eq_wp_toStateM {σ : Type u} (comp : FreeState σ α) :
150+
wp comp = wp (FreeState.toStateM comp) :=
151+
wpH_ofInterp_eq_wp_liftM (m := StateM σ)
152+
(fun _ op => FreeState.stateInterp op) comp
153+
154+
/-- Hoare spec for `get` on `FreeState`. -/
155+
@[spec]
156+
theorem Spec.get_FreeState {σ : Type u} {Q : PostCond σ (.arg σ .pure)} :
157+
Triple (MonadStateOf.get : FreeState σ σ) (spred(fun s => Q.1 s s)) Q := by
158+
mvcgen
159+
160+
/-- Hoare spec for `set` on `FreeState`. -/
161+
@[spec]
162+
theorem Spec.set_FreeState {σ : Type u} (s : σ) {Q : PostCond PUnit (.arg σ .pure)} :
163+
Triple (MonadStateOf.set s : FreeState σ PUnit) (spred(fun _ => Q.1 ⟨⟩ s)) Q := by
164+
mvcgen
165+
166+
/-- Logical handler for the reader effect, induced by `Std.Do`'s `WP (ReaderM σ)`. -/
167+
def ReaderF.handler {σ : Type u} : LHandler (ReaderF σ) (.arg σ .pure) :=
168+
LHandler.ofInterp (m := ReaderM σ) (fun _ op => FreeReader.readInterp op)
169+
170+
instance ReaderF.instHasHandler {σ : Type u} :
171+
HasHandler (ReaderF σ) (.arg σ .pure) where
172+
handler := ReaderF.handler
173+
174+
/-- WP of a `FreeReader` program matches WP of its `ReaderM` interpretation. -/
175+
theorem ReaderF.wp_FreeReader_eq_wp_toReaderM {σ : Type u} (comp : FreeReader σ α) :
176+
wp comp = wp (FreeReader.toReaderM comp) :=
177+
wpH_ofInterp_eq_wp_liftM (m := ReaderM σ)
178+
(fun _ op => FreeReader.readInterp op) comp
179+
180+
/-- Hoare spec for `read` on `FreeReader`. -/
181+
@[spec]
182+
theorem Spec.read_FreeReader {ρ : Type u} {Q : PostCond ρ (.arg ρ .pure)} :
183+
Triple (MonadReaderOf.read : FreeReader ρ ρ) (spred(fun r => Q.1 r r)) Q := by
184+
mvcgen
185+
186+
end FreeM
187+
188+
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)