feat(control): bridge the program-logic kernel to core's lattice-generic WP stack

AGENTS.md

@@ -107,8 +107,11 @@ and depend on this library.
   algebra, monad iter / hom, lawful re-exports), plus the program-logic
   kernel: ordered monad algebras (`Monad/Algebra`, unary and relational),
   exact monadic support over core's `MonadAttach` with the
-  always/some/never judgments (`Monad/Support`), and the core-`Std.Do`
-  quarantine root (`Do/Basic`).
+  always/some/never judgments (`Monad/Support`), their bridges to core's
+  lattice-generic `Std.Internal.Do` weakest-precondition stack
+  (`Monad/{Algebra,Support,Hom}/WP`: `toWPMonad`, demonic and angelic
+  interpretations, `vcgen`-ready), and the core-`Std.Do` quarantine root
+  (`Do/Basic`).
 - `PolyFun/Control/LTS/Trace.lean`: generic finite visible traces over the
   silent/visible `Control.LTS` layer and preservation by weak simulation.
 - `PolyFun/Logic/`: small logic helpers (`HEq`).

PolyFun.lean

@@ -11,13 +11,16 @@ public import PolyFun.Control.Lawful.Basic
 public import PolyFun.Control.Monad.Algebra
 public import PolyFun.Control.Monad.Algebra.Relational
 public import PolyFun.Control.Monad.Algebra.Relational.Support
+public import PolyFun.Control.Monad.Algebra.WP
 public import PolyFun.Control.Monad.Free
 public import PolyFun.Control.Monad.FreeCont
 public import PolyFun.Control.Monad.Hom
+public import PolyFun.Control.Monad.Hom.WP
 public import PolyFun.Control.Monad.Hom.Writer
 public import PolyFun.Control.Monad.Indexed
 public import PolyFun.Control.Monad.Iter
 public import PolyFun.Control.Monad.Support
+public import PolyFun.Control.Monad.Support.WP
 public import PolyFun.Control.Trace
 public import PolyFun.IPFunctor.Basic
 public import PolyFun.IPFunctor.Chart.Basic

PolyFun/Control/Do/Basic.lean

@@ -20,15 +20,15 @@ evolving upstream API quarantined.
 It provides constructions — deliberately not instances — that transport core
 `Std.Do` structure onto PolyFun's monads:
 
-* `MonadHom.transportWP` / `MonadHom.transportWPMonad` pull a `WP`/`WPMonad`
+* `MonadHom.transportSPredWP` / `MonadHom.transportSPredWPMonad` pull a `WP`/`WPMonad`
   structure back along a monad morphism `F : m →ᵐ n`, so a monad that interprets
   into an `mvcgen`-ready stack inherits its predicate-transformer semantics.
 * `MonadAttach.toWP` / `MonadAttach.toWPMonad` give any monad with exact support
   the demonic (almost-sure) interpretation at the `.pure` post shape: `wp x Q`
   holds when every possible output of `x` satisfies `Q`. `MonadAttach.toWPSound`
   proves that interpretation sound in core's sense, with `attach` supplying the
   `Ensures` witness.
-* `MonadAttach.support_subset_of_wp` / `allOutputs_of_wp` go the other way: *any*
+* `MonadAttach.support_subset_of_wpSPred` / `allOutputs_of_wpSPred` go the other way: *any*
   `WPSound` predicate-transformer semantics bounds the support, so an
   `mvcgen`-discharged triple becomes a support fact in one step. These need only
   `LawfulMonadAttach`, so they also apply to `StateT`/`ReaderT`/`EStateM`, where
@@ -81,15 +81,15 @@ variable {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n]
 `x : m α` by the predicate transformer of its image `F x`. Not an instance —
 downstream registers it at chosen carriers. -/
 @[instance_reducible]
-def transportWP (F : m →ᵐ n) [WP n ps] : WP m ps where
+def transportSPredWP (F : m →ᵐ n) [WP n ps] : WP m ps where
   wp x := WP.wp (F x)
 
 /-- The transported structure is a `WPMonad` whenever the target is and the
 source is a lawful monad. Not an instance. -/
 @[instance_reducible]
-def transportWPMonad (F : m →ᵐ n) [LawfulMonad m] [WPMonad n ps] : WPMonad m ps where
+def transportSPredWPMonad (F : m →ᵐ n) [LawfulMonad m] [WPMonad n ps] : WPMonad m ps where
   toLawfulMonad := inferInstance
-  toWP := F.transportWP
+  toWP := F.transportSPredWP
   wp_pure a := by
     change WP.wp (F (pure a)) = _
     rw [F.mmap_pure]
@@ -187,13 +187,13 @@ variable {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadAttach m]
   [LawfulMonadAttach m] {ps : PostShape.{u}} [WP m ps] [WPSound m ps]
 
 /-- Any `WPSound` predicate-transformer semantics bounds the support. -/
-theorem support_subset_of_wp {α : Type u} {x : m α} {P : α → Prop}
+theorem support_subset_of_wpSPred {α : Type u} {x : m α} {P : α → Prop}
     (h : ⊢ₛ wp⟦x⟧ (⇓?a => ⌜P a⌝)) : support x ⊆ {a | P a} :=
   fun _ hcan => WPSound.of_wp_canReturn (P := P) hcan h
 
-/-- The "always" phrasing of `support_subset_of_wp`: a weakest-precondition proof
+/-- The "always" phrasing of `support_subset_of_wpSPred`: a weakest-precondition proof
 discharges the almost-sure judgment. -/
-theorem allOutputs_of_wp {α : Type u} {x : m α} {P : α → Prop}
+theorem allOutputs_of_wpSPred {α : Type u} {x : m α} {P : α → Prop}
     (h : ⊢ₛ wp⟦x⟧ (⇓?a => ⌜P a⌝)) : AllOutputs P x :=
   fun _ hcan => WPSound.of_wp_canReturn (P := P) hcan h
 

PolyFun/Control/Monad/Algebra/WP.lean

@@ -0,0 +1,122 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Devon Tuma
+-/
+module
+
+public import PolyFun.Control.Monad.Algebra
+public import ToCslib.Order.LeanOrder
+public import Std.Internal.Do
+
+/-!
+# Ordered monad algebras as core weakest-precondition monads
+
+Core's lattice-generic program logic (`Std.Internal.Do`, public as `Std.WP` from Lean v4.35)
+interprets a monad through `WPMonad m Pred EPred`: a monotone predicate transformer per program,
+sound for `pure` and `bind` up to `⊑`. An ordered monad algebra `MAlgOrdered m l` carries exactly
+that data, with equations in place of the inequalities and no exception layer, so it yields a
+`WPMonad m l EPost.Nil` once `ToCslib.Order.LeanOrder` makes Mathlib's `CompleteLattice l` an
+`Assertion`. The construction is deliberately not an instance: install it at the base monad
+(`letI` / `local instance`) and let core's `StateT`, `ReaderT`, `ExceptT`, and `OptionT`
+instances lift it, which supplies honest exception postconditions where PolyFun's own
+transformer lifts collapse failures to `⊥`.
+
+Agreement is definitional: `wp` computed through the derived interpretation *is*
+`MAlgOrdered.wp`, and core's `Triple` unfolds to `MAlgOrdered.Triple`. The module imports the
+`Std.Internal.Do` root rather than its `WP` submodules so that the `@[spec]` database `vcgen`
+consults — `Spec.bind` in particular, which lives in `Std.Internal.Do.Triple.SpecLemmas` — is
+loaded wherever an instance built here is installed. The lattice operations
+core's lemmas are stated with (`⊤`, `⊥`, `⊓`, `⊔` of `Lean.Order`) are Mathlib's on a bridged
+carrier; the transfer lemmas below let `simp` move between the two spellings.
+-/
+
+public section
+
+universe u v w
+
+/-! ## Lattice operations across the bridge
+
+`Std.Internal.Do.Order.Basic` defines `Lean.Order.top`, `meet`, and `join` from predicate-indexed
+suprema; on a carrier whose `Lean.Order.CompleteLattice` comes from Mathlib they are Mathlib's
+`⊤`, `⊓`, and `⊔`. -/
+
+namespace MAlgOrdered
+
+section LatticeTransfer
+
+variable {α : Type u} [CompleteLattice α]
+
+@[simp]
+theorem top_eq_top : (Lean.Order.top : α) = ⊤ :=
+  le_antisymm le_top (Lean.Order.le_top (⊤ : α))
+
+@[simp]
+theorem meet_eq_inf (x y : α) : Lean.Order.meet x y = x ⊓ y :=
+  le_antisymm (le_inf (Lean.Order.meet_le_left x y) (Lean.Order.meet_le_right x y))
+    (Lean.Order.le_meet _ x y inf_le_left inf_le_right)
+
+@[simp]
+theorem join_eq_sup (x y : α) : Lean.Order.join x y = x ⊔ y :=
+  le_antisymm (Lean.Order.join_le x y _ le_sup_left le_sup_right)
+    (sup_le (Lean.Order.left_le_join x y) (Lean.Order.right_le_join x y))
+
+end LatticeTransfer
+
+end MAlgOrdered
+
+open Std.Internal.Do
+
+namespace MAlgOrdered
+
+variable {m : Type u → Type v} {l : Type u} [Monad m] [_root_.CompleteLattice l] [MAlgOrdered m l]
+
+/-- The predicate-transformer interpretation of `m α` induced by an ordered monad algebra:
+`MAlgOrdered.wp x post`, ignoring the empty exception postcondition. -/
+@[expose, instance_reducible]
+def toWP (α : Type u) : WP (m α) α l EPost.Nil where
+  wpTrans x := ⟨fun post _ => MAlgOrdered.wp x post⟩
+  wp_trans_monotone x _ _ _ _ _ hpost := wp_mono x hpost
+
+@[simp]
+theorem toWP_wp {α : Type u} (x : m α) (post : α → l) (epost : EPost.Nil) :
+    (toWP (m := m) (l := l) α).wp x post epost = MAlgOrdered.wp x post :=
+  rfl
+
+/-- Core's triple through the derived interpretation is PolyFun's triple. -/
+theorem toWP_triple_iff {α : Type u} (x : m α) (pre : l) (post : α → l) (epost : EPost.Nil) :
+    @Std.Internal.Do.Triple l EPost.Nil (m α) α _ _ x (toWP α) pre post epost ↔
+      MAlgOrdered.Triple pre x post := by
+  let inst := toWP (m := m) (l := l) α
+  exact ⟨fun h => h.le_wp, fun h => ⟨h⟩⟩
+
+/-- An ordered monad algebra is a core weakest-precondition monad: its laws are the equations
+`wp_pure` and `wp_bind` read as inequalities. Not an instance. -/
+@[expose, instance_reducible]
+def toWPMonad [LawfulMonad m] : WPMonad m l EPost.Nil where
+  toLawfulMonad := inferInstance
+  toWP := toWP
+  pure_le_wp_pure x post _ := Lean.Order.PartialOrder.rel_of_eq (wp_pure x post).symm
+  bind_le_wp_bind x f post _ := Lean.Order.PartialOrder.rel_of_eq (wp_bind x f post).symm
+
+@[simp]
+theorem toWPMonad_wp [LawfulMonad m] {α : Type u} (x : m α) (post : α → l) (epost : EPost.Nil) :
+    (letI := toWPMonad (m := m) (l := l); Std.Internal.Do.wp x post epost) =
+      MAlgOrdered.wp x post :=
+  rfl
+
+/-- The derived interpretation is conjunctive at `x` whenever the algebra's `wp x` preserves
+binary meets of postconditions. -/
+theorem wpConjunctiveOf {α : Type u} (x : m α)
+    (h : ∀ Q₁ Q₂ : α → l,
+      MAlgOrdered.wp x Q₁ ⊓ MAlgOrdered.wp x Q₂ ≤ MAlgOrdered.wp x fun a => Q₁ a ⊓ Q₂ a) :
+    @WPConjunctive (m α) α l EPost.Nil _ _ (toWP α) x := by
+  let inst := toWP (m := m) (l := l) α
+  refine ⟨fun Q₁ Q₂ _ _ => ?_⟩
+  change Lean.Order.meet (MAlgOrdered.wp x Q₁) (MAlgOrdered.wp x Q₂) ≤
+    MAlgOrdered.wp x (Lean.Order.meet Q₁ Q₂)
+  rw [meet_eq_inf]
+  refine _root_.le_trans (h Q₁ Q₂) (wp_mono x fun a => ?_)
+  rw [Lean.Order.meet_apply, meet_eq_inf]
+
+end MAlgOrdered

PolyFun/Control/Monad/Hom/WP.lean

@@ -0,0 +1,84 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Devon Tuma
+-/
+module
+
+public import PolyFun.Control.Monad.Hom
+public import Std.Internal.Do
+
+/-!
+# Transport of weakest preconditions along monad morphisms
+
+A monad morphism `F : m →ᵐ n` pulls a `WPMonad` interpretation of `n` back to `m`: a program is
+interpreted by the transformer of its image. Because `F` preserves `pure` and `bind`, the
+soundness inequalities transfer verbatim. This is how a free program acquires the semantics of a
+handler (`FreeM.wpMonadOfHandler`), and how any monad interpreting into a `vcgen`-ready stack
+inherits that stack's specifications. The unbundled form takes the two preservation equations
+inline, so cslib's `IsMonadHom` predicate instantiates it once it lands.
+
+Nothing here is an instance: register the transported structure scoped or local at the
+carrier where it is intended.
+-/
+
+public section
+
+universe u v w w' z
+
+open Std.Internal.Do Lean.Order
+
+namespace MonadHom
+
+variable {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n]
+  {Pred : Type w'} {EPred : Type z} [Assertion Pred] [Assertion EPred]
+
+/-- Pull back the interpretation of `n α` along a monad morphism. -/
+@[expose, instance_reducible]
+def transportWP (F : m →ᵐ n) (α : Type u) [WP (n α) α Pred EPred] : WP (m α) α Pred EPred where
+  wpTrans x := WP.wpTrans (F x)
+  wp_trans_monotone x := WP.wp_trans_monotone (F x)
+
+@[simp]
+theorem transportWP_wp (F : m →ᵐ n) {α : Type u} [WP (n α) α Pred EPred] (x : m α)
+    (post : α → Pred) (epost : EPred) :
+    (F.transportWP α).wp x post epost = wp (F x) post epost :=
+  rfl
+
+/-- The transported interpretation is a weakest-precondition monad whenever the target is and
+the source is lawful. -/
+@[expose, instance_reducible]
+def transportWPMonad (F : m →ᵐ n) [LawfulMonad m] [WPMonad n Pred EPred] :
+    WPMonad m Pred EPred where
+  toLawfulMonad := inferInstance
+  toWP α := F.transportWP α
+  pure_le_wp_pure a post epost := by
+    change post a ⊑ wp (F (pure a)) post epost
+    rw [F.mmap_pure]
+    exact WPMonad.pure_le_wp_pure a post epost
+  bind_le_wp_bind x f post epost := by
+    change wp (F x) (fun a => wp (F (f a)) post epost) epost ⊑ wp (F (x >>= f)) post epost
+    rw [F.mmap_bind]
+    exact WPMonad.bind_le_wp_bind (F x) (fun a => F (f a)) post epost
+
+/-- Transport along a function preserving `pure` and `bind`, with the two equations supplied
+inline rather than bundled. -/
+@[expose, instance_reducible]
+def transportWPMonadOf (F : ∀ {α : Type u}, m α → n α)
+    (hpure : ∀ {α : Type u} (a : α), F (pure a) = pure a)
+    (hbind : ∀ {α β : Type u} (x : m α) (f : α → m β), F (x >>= f) = F x >>= fun a => F (f a))
+    [LawfulMonad m] [WPMonad n Pred EPred] : WPMonad m Pred EPred where
+  toLawfulMonad := inferInstance
+  toWP α :=
+    { wpTrans := fun x => WP.wpTrans (F x)
+      wp_trans_monotone := fun x => WP.wp_trans_monotone (F x) }
+  pure_le_wp_pure a post epost := by
+    change post a ⊑ wp (F (pure a)) post epost
+    rw [hpure]
+    exact WPMonad.pure_le_wp_pure a post epost
+  bind_le_wp_bind x f post epost := by
+    change wp (F x) (fun a => wp (F (f a)) post epost) epost ⊑ wp (F (x >>= f)) post epost
+    rw [hbind]
+    exact WPMonad.bind_le_wp_bind (F x) (fun a => F (f a)) post epost
+
+end MonadHom