From 07774bb68aba9e8ca858701ec89eae8679d1db4b Mon Sep 17 00:00:00 2001 From: Tanner Duve Date: Wed, 27 May 2026 19:51:12 -0700 Subject: [PATCH 1/2] feat(Control/Monad/Free): weakest preconditions for FreeM MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- Cslib.lean | 1 + Cslib/Foundations/Control/Monad/Free/WP.lean | 175 ++++++++++++++ CslibTests.lean | 1 + CslibTests/FreeMonadWP.lean | 230 +++++++++++++++++++ 4 files changed, 407 insertions(+) create mode 100644 Cslib/Foundations/Control/Monad/Free/WP.lean create mode 100644 CslibTests/FreeMonadWP.lean diff --git a/Cslib.lean b/Cslib.lean index b504973c3..113df9364 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -50,6 +50,7 @@ public import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey public import Cslib.Foundations.Control.Monad.Free public import Cslib.Foundations.Control.Monad.Free.Effects public import Cslib.Foundations.Control.Monad.Free.Fold +public import Cslib.Foundations.Control.Monad.Free.WP public import Cslib.Foundations.Data.BiTape public import Cslib.Foundations.Data.DecidableEqZero public import Cslib.Foundations.Data.FinFun.Basic diff --git a/Cslib/Foundations/Control/Monad/Free/WP.lean b/Cslib/Foundations/Control/Monad/Free/WP.lean new file mode 100644 index 000000000..d7711685c --- /dev/null +++ b/Cslib/Foundations/Control/Monad/Free/WP.lean @@ -0,0 +1,175 @@ +/- +Copyright (c) 2025 Tanner Duve (Logical Intelligence). All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Tanner Duve +-/ + +module + +public import Cslib.Foundations.Control.Monad.Free +public import Cslib.Foundations.Control.Monad.Free.Effects +public import Std.Do.PredTrans +public import Std.Do.WP.Basic +public import Std.Do.WP.Monad +public import Std.Do.Triple + +/-! +# Weakest preconditions for `FreeM` programs + +Weakest-precondition interpretation of `FreeM F` programs through `Std.Do`'s +predicate-transformer monad `PredTrans ps`. The universal property of `FreeM` lifts any +effect handler `F ι → PredTrans ps ι` to a unique monad morphism `wpH H = liftM H.run`, +so weakest preconditions are compositional in `FreeM`'s monadic structure. An +`[LHandler F ps]` instance plugs `FreeM F` into `Std.Do`'s `WP`/`WPMonad`/`Triple` +infrastructure. + +The WP's structural rules (`wpH_pure`, `wpH_bind`, …) are immediate from `liftM` being a monad +morphism; the adequacy theorem `wpH_ofInterp_eq_wp_liftM` — that WP-via-handler agrees with +`Std.Do`'s WP of the `liftM` interpretation — is the same statement of uniqueness. + +The design follows [Vistrup, Sammler, Jung. *Program Logics à la Carte.* POPL 2025], adapted +from coinductive ITrees to inductive `FreeM` and from Iris to `Std.Do`. +-/ + +@[expose] public section + +set_option mvcgen.warning false + +namespace Cslib + +open Std.Do + +namespace FreeM + +universe u v w + +variable {F G : Type u → Type v} {ps : PostShape.{u}} {α β : Type u} + +/-- A logical handler: an effect handler from `F` into the predicate-transformer monad +`PredTrans ps`. -/ +structure LHandler (F : Type u → Type v) (ps : PostShape.{u}) : Type (max (u + 1) v) where + /-- The assignment from operations to predicate transformers. -/ + run {ι : Type u} : F ι → PredTrans ps ι + +namespace LHandler + +/-- Sum of handlers; the counterpart of the paper's `H₁ ⊕ H₂`. -/ +def sum (H₁ : LHandler F ps) (H₂ : LHandler G ps) : + LHandler (fun α => F α ⊕ G α) ps where + run := Sum.elim H₁.run H₂.run + +@[simp] theorem sum_run_inl (H₁ : LHandler F ps) (H₂ : LHandler G ps) + {ι : Type u} (x : F ι) : + (LHandler.sum H₁ H₂).run (Sum.inl x : F ι ⊕ G ι) = H₁.run x := rfl + +@[simp] theorem sum_run_inr (H₁ : LHandler F ps) (H₂ : LHandler G ps) + {ι : Type u} (y : G ι) : + (LHandler.sum H₁ H₂).run (Sum.inr y : F ι ⊕ G ι) = H₂.run y := rfl + +/-- Derive a logical handler from an effect handler into any `[WP m ps]` monad, by composing +with `m`'s WP. -/ +def ofInterp {m : Type u → Type w} [WP m ps] + (interp : ∀ ι : Type u, F ι → m ι) : LHandler F ps where + run {ι} op := wp (interp ι op) + +@[simp] theorem ofInterp_run {m : Type u → Type w} [WP m ps] + (interp : ∀ ι : Type u, F ι → m ι) {ι : Type u} (op : F ι) : + (LHandler.ofInterp interp).run op = wp (interp ι op) := rfl + +end LHandler + +/-- Weakest-precondition interpretation of a `FreeM F α` program against a logical handler `H`. +Defined as `FreeM.liftM` instantiated at `PredTrans ps`, the unique monad morphism +`FreeM F → PredTrans ps` extending `H` per the universal property of `FreeM`. -/ +def wpH (H : LHandler F ps) (x : FreeM F α) : PredTrans ps α := + x.liftM (fun {_} => H.run) + +@[simp] theorem wpH_pure (H : LHandler F ps) (a : α) : + wpH H (pure a : FreeM F α) = Pure.pure a := rfl + +@[simp] theorem wpH_liftBind (H : LHandler F ps) {ι : Type u} + (op : F ι) (k : ι → FreeM F α) : + wpH H (lift op >>= k) = H.run op >>= fun x => wpH H (k x) := rfl + +@[simp] theorem wpH_lift (H : LHandler F ps) {ι : Type u} (op : F ι) : + wpH H (lift op : FreeM F ι) = H.run op := + liftM_lift _ op + +@[simp] theorem wpH_bind (H : LHandler F ps) (x : FreeM F α) (f : α → FreeM F β) : + wpH H (x >>= f) = wpH H x >>= fun a => wpH H (f a) := + liftM_bind _ x f + +/-- Adequacy theorem: WP via `FreeM` against an `ofInterp`-derived handler agrees with +`Std.Do`'s WP of the `liftM` interpretation. Equivalently, two monad morphisms +`FreeM F → PredTrans ps` extending the same handler are equal. -/ +theorem wpH_ofInterp_eq_wp_liftM + {m : Type u → Type w} [Monad m] [LawfulMonad m] [WPMonad m ps] + (interp : ∀ ι : Type u, F ι → m ι) (x : FreeM F α) : + wpH (LHandler.ofInterp interp) x = wp (x.liftM (fun {_} => interp _)) := by + induction x with + | pure a => simp [wpH, FreeM.liftM, WPMonad.wp_pure] + | lift_bind op k ih => + simp [WPMonad.wp_bind, ih] + +/-- Records a default logical handler for `F` at shape `ps`, enabling the global +`WP (FreeM F) ps` instance and any `Triple`/`mvcgen` reasoning over `FreeM F`. -/ +class HasHandler (F : Type u → Type v) (ps : outParam (PostShape.{u})) where + /-- The default logical handler for `F`. -/ + handler : LHandler F ps + +instance instWPFreeM [HasHandler F ps] : WP (FreeM F) ps where + wp := wpH HasHandler.handler + +instance instWPMonadFreeM [HasHandler F ps] : WPMonad (FreeM F) ps where + wp_pure _ := rfl + wp_bind x f := wpH_bind _ x f + +/-- Logical handler for the state effect, induced by `Std.Do`'s `WP (StateM σ)`. -/ +def StateF.handler {σ : Type u} : LHandler (StateF σ) (.arg σ .pure) := + LHandler.ofInterp (m := StateM σ) (fun _ op => FreeState.stateInterp op) + +instance StateF.instHasHandler {σ : Type u} : + HasHandler (StateF σ) (.arg σ .pure) where + handler := StateF.handler + +/-- WP of a `FreeState` program matches WP of its `StateM` interpretation. -/ +theorem StateF.wp_FreeState_eq_wp_toStateM {σ : Type u} (comp : FreeState σ α) : + wp comp = wp (FreeState.toStateM comp) := + wpH_ofInterp_eq_wp_liftM (m := StateM σ) + (fun _ op => FreeState.stateInterp op) comp + +/-- Hoare spec for `get` on `FreeState`. -/ +@[spec] +theorem Spec.get_FreeState {σ : Type u} {Q : PostCond σ (.arg σ .pure)} : + Triple (MonadStateOf.get : FreeState σ σ) (spred(fun s => Q.1 s s)) Q := by + mvcgen + +/-- Hoare spec for `set` on `FreeState`. -/ +@[spec] +theorem Spec.set_FreeState {σ : Type u} (s : σ) {Q : PostCond PUnit (.arg σ .pure)} : + Triple (MonadStateOf.set s : FreeState σ PUnit) (spred(fun _ => Q.1 ⟨⟩ s)) Q := by + mvcgen + +/-- Logical handler for the reader effect, induced by `Std.Do`'s `WP (ReaderM σ)`. -/ +def ReaderF.handler {σ : Type u} : LHandler (ReaderF σ) (.arg σ .pure) := + LHandler.ofInterp (m := ReaderM σ) (fun _ op => FreeReader.readInterp op) + +instance ReaderF.instHasHandler {σ : Type u} : + HasHandler (ReaderF σ) (.arg σ .pure) where + handler := ReaderF.handler + +/-- WP of a `FreeReader` program matches WP of its `ReaderM` interpretation. -/ +theorem ReaderF.wp_FreeReader_eq_wp_toReaderM {σ : Type u} (comp : FreeReader σ α) : + wp comp = wp (FreeReader.toReaderM comp) := + wpH_ofInterp_eq_wp_liftM (m := ReaderM σ) + (fun _ op => FreeReader.readInterp op) comp + +/-- Hoare spec for `read` on `FreeReader`. -/ +@[spec] +theorem Spec.read_FreeReader {ρ : Type u} {Q : PostCond ρ (.arg ρ .pure)} : + Triple (MonadReaderOf.read : FreeReader ρ ρ) (spred(fun r => Q.1 r r)) Q := by + mvcgen + +end FreeM + +end Cslib diff --git a/CslibTests.lean b/CslibTests.lean index 7b52a3a31..87709d818 100644 --- a/CslibTests.lean +++ b/CslibTests.lean @@ -5,6 +5,7 @@ public import CslibTests.CCS public import CslibTests.CLL public import CslibTests.DFA public import CslibTests.FreeMonad +public import CslibTests.FreeMonadWP public import CslibTests.GrindLint public import CslibTests.HML public import CslibTests.HasFresh diff --git a/CslibTests/FreeMonadWP.lean b/CslibTests/FreeMonadWP.lean new file mode 100644 index 000000000..0e6163dfe --- /dev/null +++ b/CslibTests/FreeMonadWP.lean @@ -0,0 +1,230 @@ +/- +Copyright (c) 2025 Tanner Duve (Logical Intelligence). All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Tanner Duve +-/ + +import Cslib.Foundations.Control.Monad.Free.WP +import Std.Tactic.Do + +/-! +Examples for WP in `Cslib.Foundations.Control.Monad.Free.WP`: instance resolution, +a `Triple` on a `FreeState` program discharged by `mvcgen`, and a custom `CounterF` effect with +its own logical handler. +-/ + +set_option mvcgen.warning false + +namespace CslibTests.FreeMonadWP + +open Cslib Cslib.FreeM Std.Do + +example : WP (FreeState Nat) (.arg Nat .pure) := inferInstance +example : WPMonad (FreeState Nat) (.arg Nat .pure) := inferInstance +example : WP (FreeReader Nat) (.arg Nat .pure) := inferInstance +example : HasHandler (StateF Nat) (.arg Nat .pure) := inferInstance + +/-- Increment the natural-number state by 1. -/ +def incr : FreeState Nat Unit := do + let n ← MonadStateOf.get + MonadStateOf.set (n + 1) + +example : wp incr = wp (FreeState.toStateM incr) := + StateF.wp_FreeState_eq_wp_toStateM incr + +/-- Starting in state `n`, `incr` ends in state `n + 1`. `mvcgen` picks up the `@[spec]` lemmas +for `MonadStateOf.get`/`set` on `FreeState` and discharges the resulting arithmetic VC. -/ +example (n : Nat) : + ⦃fun s => ⌜s = n⌝⦄ (incr : FreeState Nat Unit) ⦃⇓ _ s' => ⌜s' = n + 1⌝⦄ := by + mvcgen + intro s heq + subst heq + rfl + +/-- A counter effect with two operations. -/ +inductive CounterF : Type → Type where + /-- Increment the counter by one. -/ + | tick : CounterF Unit + /-- Read the counter's value. -/ + | read : CounterF Nat + +/-- Counter programs built from `CounterF`. -/ +abbrev FreeCounter := FreeM CounterF + +namespace CounterF + +/-- Effect handler for `CounterF` into `StateM Nat`, used to seed both the executable +semantics and the logical handler. -/ +def interp : ∀ ι : Type, CounterF ι → StateM Nat ι + | _, .tick => modify (· + 1) + | _, .read => MonadStateOf.get + +/-- Logical handler for `CounterF` induced by `interp` and `Std.Do`'s `WP (StateM Nat)` +instance. -/ +def handler : LHandler CounterF (.arg Nat .pure) := + LHandler.ofInterp CounterF.interp + +instance : HasHandler CounterF (.arg Nat .pure) where + handler := CounterF.handler + +/-- Interpret counter programs as `StateM Nat` programs. -/ +abbrev toStateM {α : Type} (comp : FreeCounter α) : StateM Nat α := + comp.liftM (fun {ι} => CounterF.interp ι) + +/-- Adequacy theorem specialized to `CounterF`. -/ +theorem wp_FreeCounter_eq_wp_toStateM {α : Type} (comp : FreeCounter α) : + wp comp = wp (CounterF.toStateM comp) := + wpH_ofInterp_eq_wp_liftM (m := StateM Nat) CounterF.interp comp + +end CounterF + +/-- Smart constructor: tick the counter as a `FreeCounter` action. -/ +abbrev tick : FreeCounter Unit := lift CounterF.tick + +/-- Smart constructor: read the counter as a `FreeCounter` action. -/ +abbrev readCounter : FreeCounter Nat := lift CounterF.read + +/-- Tick three times, then read out the counter. -/ +def threeTicks : FreeCounter Nat := do + tick; tick; tick + readCounter + +/-- +Triple about the counter program: starting at `0`, the final value is `3` and the final state +is `3`. Proven by the same bridge-then-`mvcgen` pattern as `incr`. +-/ +example : + ⦃fun s => ⌜s = 0⌝⦄ threeTicks ⦃⇓ v s => ⌜v = 3 ∧ s = 3⌝⦄ := by + mvcgen + intro s seq0 + subst seq0 + exact ⟨rfl, rfl⟩ + +/-- A failure effect with one operation `fail` of empty answer type. -/ +inductive FailF : Type → Type where + /-- Abort the computation. -/ + | fail : FailF PEmpty.{1} + +/-- Logical handler for `FailF`: `fail` has precondition `⌜False⌝`, so it is only provable in +unreachable branches. -/ +def FailF.handler {ps : PostShape} : LHandler FailF ps where + run {_} op := match op with + | .fail => PredTrans.const spred(⌜False⌝) + +/-- A combined state + failure signature, sequencing `StateF Nat` with `FailF`. -/ +abbrev StateFail := fun α => StateF Nat α ⊕ FailF α + +/-- Handler for the combined signature: the sum of the component handlers — the paper's +`H₁ ⊕ H₂` composition. -/ +instance : HasHandler StateFail (.arg Nat .pure) where + handler := StateF.handler.sum FailF.handler + +/-- Smart constructor for state-read in the combined signature. -/ +abbrev sfGet : FreeM StateFail Nat := lift (Sum.inl StateF.get) + +/-- Smart constructor for state-write in the combined signature. -/ +abbrev sfSet (n : Nat) : FreeM StateFail PUnit := lift (Sum.inl (StateF.set n)) + +/-- Smart constructor for failure in the combined signature, eliminated to any return type via +`PEmpty.elim`. -/ +abbrev sfFail {α : Type} : FreeM StateFail α := + lift (Sum.inr FailF.fail) >>= PEmpty.elim + +/-- Hoare spec for the sum-lifted state-read. -/ +@[spec] +theorem Spec.sfGet {Q : PostCond Nat (.arg Nat .pure)} : + Triple sfGet (spred(fun s => Q.1 s s)) Q := by + mvcgen + +/-- Hoare spec for the sum-lifted state-write. -/ +@[spec] +theorem Spec.sfSet (n : Nat) {Q : PostCond PUnit (.arg Nat .pure)} : + Triple (sfSet n) (spred(fun _ => Q.1 ⟨⟩ n)) Q := by + mvcgen + +/-- Hoare spec for sum-lifted failure: requires `False` to verify. -/ +@[spec] +theorem Spec.sfFail {α : Type} {Q : PostCond α (.arg Nat .pure)} : + Triple (sfFail : FreeM StateFail α) (spred(⌜False⌝)) Q := by + mvcgen + +/-- A non-branching program in the combined signature: read the state, then write +`state + 1`. Shows that the sum handler composes the StateF and FailF specs cleanly. -/ +def getAndBump : FreeM StateFail Unit := do + let n ← sfGet + sfSet (n + 1) + +/-- `getAndBump` advances the state by 1, proven through the sum handler. -/ +example (n : Nat) : + ⦃fun s => ⌜s = n⌝⦄ (getAndBump : FreeM StateFail Unit) + ⦃⇓ _ s => ⌜s = n + 1⌝⦄ := by + mvcgen + intro s a + subst a + rfl + +/-- Increment the state if it's strictly below `limit`, otherwise fail. Branches on the state's +value and uses `sfFail` in the else branch. -/ +def bumpUnder (limit : Nat) : FreeM StateFail Unit := do + let n ← sfGet + if n < limit then sfSet (n + 1) else sfFail + +/-- Starting in a state below `limit`, `bumpUnder` increments without failing — the failure +branch is unreachable because the precondition rules it out. -/ +example (limit n : Nat) (hlt : n < limit) : + ⦃fun s => ⌜s = n⌝⦄ (bumpUnder limit : FreeM StateFail Unit) + ⦃⇓ _ s => ⌜s = n + 1⌝⦄ := by + unfold bumpUnder + mvcgen <;> aesop + +/-- Demonic non-determinism: a single operation `choice α` that abstractly returns an arbitrary +`a : α`. Verification must consider all possible values of `a`. -/ +inductive DemonicF : Type → Type 1 where + /-- Choose an element of `α`. -/ + | choice (α : Type) : DemonicF α + +/-- Logical handler for `DemonicF`: the predicate transformer for `choice α` is universal +quantification over `α`. Conjunctivity of `∀` (i.e. `∀ a, P a ∧ Q a ⊣⊢ (∀ a, P a) ∧ (∀ a, Q a)`) +is what makes this admissible in `PredTrans`. -/ +def DemonicF.handler {ps : PostShape} : LHandler DemonicF ps where + run {_} op := match op with + | .choice _ => + { trans := fun Q => SPred.forall (fun a => Q.1 a) + conjunctiveRaw := by + intro Q₁ Q₂ + apply SPred.bientails.iff.mpr + refine ⟨?_, ?_⟩ + · apply SPred.and_intro + · apply SPred.forall_intro + intro a + exact (SPred.forall_elim a).trans SPred.and_elim_l + · apply SPred.forall_intro + intro a + exact (SPred.forall_elim a).trans SPred.and_elim_r + · apply SPred.forall_intro + intro a + apply SPred.and_intro + · exact SPred.and_elim_l.trans (SPred.forall_elim a) + · exact SPred.and_elim_r.trans (SPred.forall_elim a) } + +instance : HasHandler DemonicF .pure where + handler := DemonicF.handler + +/-- Smart constructor for demonic choice over `α`. -/ +abbrev demonic (α : Type) : FreeM DemonicF α := lift (DemonicF.choice α) + +/-- Triple for `demonic α`: the precondition must imply the postcondition for *every* `a : α`. -/ +@[spec] +theorem Spec.demonic {α : Type} {Q : PostCond α .pure} : + Triple (demonic α) (SPred.forall (fun a : α => Q.1 a)) Q := + Triple.iff.mpr SPred.entails.rfl + +/-- A demonic Bool: the precondition must hold for both `true` and `false`. -/ +example {Q : PostCond Bool .pure} : + Triple (demonic Bool) (SPred.and (Q.1 true) (Q.1 false)) Q := + fun ⟨ht, hf⟩ b => + match b with + | true => ht + | false => hf + +end CslibTests.FreeMonadWP From 25f5d807f8775c0d9604288100165b09839b0fa4 Mon Sep 17 00:00:00 2001 From: Tanner Duve Date: Wed, 27 May 2026 23:50:41 -0700 Subject: [PATCH 2/2] refactor(Free): move state/reader handlers to Effects.lean --- .../Control/Monad/Free/Effects.lean | 51 +++++++++++ Cslib/Foundations/Control/Monad/Free/WP.lean | 86 ++++--------------- CslibTests/FreeMonadWP.lean | 10 +-- 3 files changed, 75 insertions(+), 72 deletions(-) diff --git a/Cslib/Foundations/Control/Monad/Free/Effects.lean b/Cslib/Foundations/Control/Monad/Free/Effects.lean index 7c58bca5a..11dd9e6f3 100644 --- a/Cslib/Foundations/Control/Monad/Free/Effects.lean +++ b/Cslib/Foundations/Control/Monad/Free/Effects.lean @@ -7,6 +7,7 @@ Authors: Tanner Duve module public import Cslib.Foundations.Control.Monad.Free +public import Cslib.Foundations.Control.Monad.Free.WP public import Mathlib.Control.Monad.Cont /-! @@ -39,10 +40,14 @@ Free monad, state monad, writer monad, continuation monad @[expose] public section +set_option mvcgen.warning false + namespace Cslib namespace FreeM +open Std.Do + universe u v w w' w'' /-! ### State Monad via `FreeM` -/ @@ -157,6 +162,32 @@ lemma run'_bind (x : FreeState σ α) (f : α → FreeState σ β) (s₀ : σ) : end FreeState +/-- Logical handler for the state effect, induced by `Std.Do`'s `WP (StateM σ)`. -/ +def StateF.handler {σ : Type u} : LHandler (StateF σ) (.arg σ .pure) := + LHandler.ofInterp (m := StateM σ) (fun _ op => FreeState.stateInterp op) + +instance StateF.instHasHandler {σ : Type u} : + HasHandler (StateF σ) (.arg σ .pure) where + handler := StateF.handler + +/-- WP of a `FreeState` program matches WP of its `StateM` interpretation. -/ +theorem StateF.wp_FreeState_eq_wp_toStateM {σ α : Type u} (comp : FreeState σ α) : + wp comp = wp (FreeState.toStateM comp) := + wpH_ofInterp_eq_wp_liftM (m := StateM σ) + (fun _ op => FreeState.stateInterp op) comp + +/-- Hoare spec for `get` on `FreeState`. -/ +@[spec] +theorem Spec.get_FreeState {σ : Type u} {Q : PostCond σ (.arg σ .pure)} : + Triple (MonadStateOf.get : FreeState σ σ) (spred(fun s => Q.1 s s)) Q := by + mvcgen + +/-- Hoare spec for `set` on `FreeState`. -/ +@[spec] +theorem Spec.set_FreeState {σ : Type u} (s : σ) {Q : PostCond PUnit (.arg σ .pure)} : + Triple (MonadStateOf.set s : FreeState σ PUnit) (spred(fun _ => Q.1 ⟨⟩ s)) Q := by + mvcgen + /-! ### Writer Monad via `FreeM` -/ /-- @@ -453,6 +484,26 @@ instance instMonadWithReaderOf : MonadWithReaderOf σ (FreeReader σ) where end FreeReader +/-- Logical handler for the reader effect, induced by `Std.Do`'s `WP (ReaderM σ)`. -/ +def ReaderF.handler {σ : Type u} : LHandler (ReaderF σ) (.arg σ .pure) := + LHandler.ofInterp (m := ReaderM σ) (fun _ op => FreeReader.readInterp op) + +instance ReaderF.instHasHandler {σ : Type u} : + HasHandler (ReaderF σ) (.arg σ .pure) where + handler := ReaderF.handler + +/-- WP of a `FreeReader` program matches WP of its `ReaderM` interpretation. -/ +theorem ReaderF.wp_FreeReader_eq_wp_toReaderM {σ α : Type u} (comp : FreeReader σ α) : + wp comp = wp (FreeReader.toReaderM comp) := + wpH_ofInterp_eq_wp_liftM (m := ReaderM σ) + (fun _ op => FreeReader.readInterp op) comp + +/-- Hoare spec for `read` on `FreeReader`. -/ +@[spec] +theorem Spec.read_FreeReader {ρ : Type u} {Q : PostCond ρ (.arg ρ .pure)} : + Triple (MonadReaderOf.read : FreeReader ρ ρ) (spred(fun r => Q.1 r r)) Q := by + mvcgen + end FreeM end Cslib diff --git a/Cslib/Foundations/Control/Monad/Free/WP.lean b/Cslib/Foundations/Control/Monad/Free/WP.lean index d7711685c..6e667a6fc 100644 --- a/Cslib/Foundations/Control/Monad/Free/WP.lean +++ b/Cslib/Foundations/Control/Monad/Free/WP.lean @@ -7,7 +7,6 @@ Authors: Tanner Duve module public import Cslib.Foundations.Control.Monad.Free -public import Cslib.Foundations.Control.Monad.Free.Effects public import Std.Do.PredTrans public import Std.Do.WP.Basic public import Std.Do.WP.Monad @@ -18,9 +17,9 @@ public import Std.Do.Triple Weakest-precondition interpretation of `FreeM F` programs through `Std.Do`'s predicate-transformer monad `PredTrans ps`. The universal property of `FreeM` lifts any -effect handler `F ι → PredTrans ps ι` to a unique monad morphism `wpH H = liftM H.run`, -so weakest preconditions are compositional in `FreeM`'s monadic structure. An -`[LHandler F ps]` instance plugs `FreeM F` into `Std.Do`'s `WP`/`WPMonad`/`Triple` +effect handler `F ι → PredTrans ps ι` to a unique monad morphism `wpH H = liftM H`, +so weakest preconditions are compositional in `FreeM`'s monadic structure. A +`[HasHandler F ps]` instance plugs `FreeM F` into `Std.Do`'s `WP`/`WPMonad`/`Triple` infrastructure. The WP's structural rules (`wpH_pure`, `wpH_bind`, …) are immediate from `liftM` being a monad @@ -47,34 +46,33 @@ variable {F G : Type u → Type v} {ps : PostShape.{u}} {α β : Type u} /-- A logical handler: an effect handler from `F` into the predicate-transformer monad `PredTrans ps`. -/ -structure LHandler (F : Type u → Type v) (ps : PostShape.{u}) : Type (max (u + 1) v) where - /-- The assignment from operations to predicate transformers. -/ - run {ι : Type u} : F ι → PredTrans ps ι +abbrev LHandler (F : Type u → Type v) (ps : PostShape.{u}) : Type (max (u + 1) v) := + ∀ {ι : Type u}, F ι → PredTrans ps ι namespace LHandler /-- Sum of handlers; the counterpart of the paper's `H₁ ⊕ H₂`. -/ def sum (H₁ : LHandler F ps) (H₂ : LHandler G ps) : - LHandler (fun α => F α ⊕ G α) ps where - run := Sum.elim H₁.run H₂.run + LHandler (fun α => F α ⊕ G α) ps := + fun op => Sum.elim H₁ H₂ op -@[simp] theorem sum_run_inl (H₁ : LHandler F ps) (H₂ : LHandler G ps) +@[simp] theorem sum_inl (H₁ : LHandler F ps) (H₂ : LHandler G ps) {ι : Type u} (x : F ι) : - (LHandler.sum H₁ H₂).run (Sum.inl x : F ι ⊕ G ι) = H₁.run x := rfl + LHandler.sum H₁ H₂ (Sum.inl x : F ι ⊕ G ι) = H₁ x := rfl -@[simp] theorem sum_run_inr (H₁ : LHandler F ps) (H₂ : LHandler G ps) +@[simp] theorem sum_inr (H₁ : LHandler F ps) (H₂ : LHandler G ps) {ι : Type u} (y : G ι) : - (LHandler.sum H₁ H₂).run (Sum.inr y : F ι ⊕ G ι) = H₂.run y := rfl + LHandler.sum H₁ H₂ (Sum.inr y : F ι ⊕ G ι) = H₂ y := rfl /-- Derive a logical handler from an effect handler into any `[WP m ps]` monad, by composing with `m`'s WP. -/ def ofInterp {m : Type u → Type w} [WP m ps] - (interp : ∀ ι : Type u, F ι → m ι) : LHandler F ps where - run {ι} op := wp (interp ι op) + (interp : ∀ ι : Type u, F ι → m ι) : LHandler F ps := + fun {ι} op => wp (interp ι op) -@[simp] theorem ofInterp_run {m : Type u → Type w} [WP m ps] +@[simp] theorem ofInterp_apply {m : Type u → Type w} [WP m ps] (interp : ∀ ι : Type u, F ι → m ι) {ι : Type u} (op : F ι) : - (LHandler.ofInterp interp).run op = wp (interp ι op) := rfl + LHandler.ofInterp interp op = wp (interp ι op) := rfl end LHandler @@ -82,17 +80,17 @@ end LHandler Defined as `FreeM.liftM` instantiated at `PredTrans ps`, the unique monad morphism `FreeM F → PredTrans ps` extending `H` per the universal property of `FreeM`. -/ def wpH (H : LHandler F ps) (x : FreeM F α) : PredTrans ps α := - x.liftM (fun {_} => H.run) + x.liftM H @[simp] theorem wpH_pure (H : LHandler F ps) (a : α) : wpH H (pure a : FreeM F α) = Pure.pure a := rfl @[simp] theorem wpH_liftBind (H : LHandler F ps) {ι : Type u} (op : F ι) (k : ι → FreeM F α) : - wpH H (lift op >>= k) = H.run op >>= fun x => wpH H (k x) := rfl + wpH H (lift op >>= k) = H op >>= fun x => wpH H (k x) := rfl @[simp] theorem wpH_lift (H : LHandler F ps) {ι : Type u} (op : F ι) : - wpH H (lift op : FreeM F ι) = H.run op := + wpH H (lift op : FreeM F ι) = H op := liftM_lift _ op @[simp] theorem wpH_bind (H : LHandler F ps) (x : FreeM F α) (f : α → FreeM F β) : @@ -115,7 +113,7 @@ theorem wpH_ofInterp_eq_wp_liftM `WP (FreeM F) ps` instance and any `Triple`/`mvcgen` reasoning over `FreeM F`. -/ class HasHandler (F : Type u → Type v) (ps : outParam (PostShape.{u})) where /-- The default logical handler for `F`. -/ - handler : LHandler F ps + handler {ι : Type u} : F ι → PredTrans ps ι instance instWPFreeM [HasHandler F ps] : WP (FreeM F) ps where wp := wpH HasHandler.handler @@ -124,52 +122,6 @@ instance instWPMonadFreeM [HasHandler F ps] : WPMonad (FreeM F) ps where wp_pure _ := rfl wp_bind x f := wpH_bind _ x f -/-- Logical handler for the state effect, induced by `Std.Do`'s `WP (StateM σ)`. -/ -def StateF.handler {σ : Type u} : LHandler (StateF σ) (.arg σ .pure) := - LHandler.ofInterp (m := StateM σ) (fun _ op => FreeState.stateInterp op) - -instance StateF.instHasHandler {σ : Type u} : - HasHandler (StateF σ) (.arg σ .pure) where - handler := StateF.handler - -/-- WP of a `FreeState` program matches WP of its `StateM` interpretation. -/ -theorem StateF.wp_FreeState_eq_wp_toStateM {σ : Type u} (comp : FreeState σ α) : - wp comp = wp (FreeState.toStateM comp) := - wpH_ofInterp_eq_wp_liftM (m := StateM σ) - (fun _ op => FreeState.stateInterp op) comp - -/-- Hoare spec for `get` on `FreeState`. -/ -@[spec] -theorem Spec.get_FreeState {σ : Type u} {Q : PostCond σ (.arg σ .pure)} : - Triple (MonadStateOf.get : FreeState σ σ) (spred(fun s => Q.1 s s)) Q := by - mvcgen - -/-- Hoare spec for `set` on `FreeState`. -/ -@[spec] -theorem Spec.set_FreeState {σ : Type u} (s : σ) {Q : PostCond PUnit (.arg σ .pure)} : - Triple (MonadStateOf.set s : FreeState σ PUnit) (spred(fun _ => Q.1 ⟨⟩ s)) Q := by - mvcgen - -/-- Logical handler for the reader effect, induced by `Std.Do`'s `WP (ReaderM σ)`. -/ -def ReaderF.handler {σ : Type u} : LHandler (ReaderF σ) (.arg σ .pure) := - LHandler.ofInterp (m := ReaderM σ) (fun _ op => FreeReader.readInterp op) - -instance ReaderF.instHasHandler {σ : Type u} : - HasHandler (ReaderF σ) (.arg σ .pure) where - handler := ReaderF.handler - -/-- WP of a `FreeReader` program matches WP of its `ReaderM` interpretation. -/ -theorem ReaderF.wp_FreeReader_eq_wp_toReaderM {σ : Type u} (comp : FreeReader σ α) : - wp comp = wp (FreeReader.toReaderM comp) := - wpH_ofInterp_eq_wp_liftM (m := ReaderM σ) - (fun _ op => FreeReader.readInterp op) comp - -/-- Hoare spec for `read` on `FreeReader`. -/ -@[spec] -theorem Spec.read_FreeReader {ρ : Type u} {Q : PostCond ρ (.arg ρ .pure)} : - Triple (MonadReaderOf.read : FreeReader ρ ρ) (spred(fun r => Q.1 r r)) Q := by - mvcgen - end FreeM end Cslib diff --git a/CslibTests/FreeMonadWP.lean b/CslibTests/FreeMonadWP.lean index 0e6163dfe..69324cbf0 100644 --- a/CslibTests/FreeMonadWP.lean +++ b/CslibTests/FreeMonadWP.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Tanner Duve -/ -import Cslib.Foundations.Control.Monad.Free.WP +import Cslib.Foundations.Control.Monad.Free.Effects import Std.Tactic.Do /-! @@ -107,8 +107,8 @@ inductive FailF : Type → Type where /-- Logical handler for `FailF`: `fail` has precondition `⌜False⌝`, so it is only provable in unreachable branches. -/ -def FailF.handler {ps : PostShape} : LHandler FailF ps where - run {_} op := match op with +def FailF.handler {ps : PostShape} : LHandler FailF ps := + fun op => match op with | .fail => PredTrans.const spred(⌜False⌝) /-- A combined state + failure signature, sequencing `StateF Nat` with `FailF`. -/ @@ -186,8 +186,8 @@ inductive DemonicF : Type → Type 1 where /-- Logical handler for `DemonicF`: the predicate transformer for `choice α` is universal quantification over `α`. Conjunctivity of `∀` (i.e. `∀ a, P a ∧ Q a ⊣⊢ (∀ a, P a) ∧ (∀ a, Q a)`) is what makes this admissible in `PredTrans`. -/ -def DemonicF.handler {ps : PostShape} : LHandler DemonicF ps where - run {_} op := match op with +def DemonicF.handler {ps : PostShape} : LHandler DemonicF ps := + fun op => match op with | .choice _ => { trans := fun Q => SPred.forall (fun a => Q.1 a) conjunctiveRaw := by