From c133e2c62bd58f6de631eb33c3c51765a7f9dfb0 Mon Sep 17 00:00:00 2001 From: Devon Tuma Date: Thu, 3 Sep 2026 12:25:27 -0500 Subject: [PATCH] feat(control): bridge the program-logic kernel to core's lattice-generic WP stack Give every PolyFun judgment a core `Std.Internal.Do.WPMonad` interpretation (the stack that becomes public `Std.WP` in v4.35 and that `vcgen` drives), so that `vcgen` decomposes `do` programs through PolyFun's own semantics and core's `Spec.*` lemmas apply to them without re-proof: - `Control/Monad/Algebra/WP.lean`: `MAlgOrdered.toWP` / `toWPMonad` turn an ordered monad algebra over a Mathlib complete lattice into a `WPMonad m l EPost.Nil` through the `ToCslib.Order.LeanOrder` bridge; `wp` agrees with `MAlgOrdered.wp` by `rfl`, core's `Triple` is PolyFun's (`toWP_triple_iff`), `wpConjunctiveOf` derives conjunctivity from meet preservation, and `top_eq_top` / `meet_eq_inf` / `join_eq_sup` move between core's and Mathlib's lattice operations on a bridged carrier; - `Control/Monad/Support/WP.lean`: `MonadAttach.toWPMonadDemonic` and `toWPMonadAngelic` interpret exact support as `WPMonad m Prop EPost.Nil` (`wp x post = AllOutputs post x`, resp. `SomeOutput`); the angelic reading is expressible here because the laws are inequalities. The demonic reading is conjunctive and sound: `LawfulWPMonadAttach` mirrors, field for field, the soundness class on Lean master, declared in the `Std.Internal.Do` namespace so the v4.35 rename deletes it; `support_subset_of_wp` / `allOutputs_of_wp` turn any sound triple into a support fact; - `Control/Monad/Hom/WP.lean`: `MonadHom.transportWP` / `transportWPMonad` and the unbundled `transportWPMonadOf` pull an interpretation back along a monad morphism. None of these is a global instance; they are installed `local` or `scoped` at the carrier. The legacy `Std.Do` bridge keeps working under the names `MonadHom.transportSPredWP(Monad)` and `MonadAttach.support_subset_of_wpSPred` / `allOutputs_of_wpSPred`, freeing the canonical names. The bridge modules import the `Std.Internal.Do` root: `vcgen` consults the `@[spec]` database, whose `Spec.bind` lives in `Triple.SpecLemmas`, and importing only the `WP` submodules yields `No spec found` on every `do` block. `PolyFunTest/Do/Algebra.lean` and `PolyFunTest/Do/Support.lean` run `vcgen` through a Mathlib-carrier algebra and through the demonic reading of `SetM`, and convert the result back into an "always" judgment. Docs: the program-logic page now describes the lattice-generic stack as canonical, records the three practical rules (root import, binding a non-instance interpretation with `let` before projecting, keeping transfer lemmas out of the `Lean.Order` namespace) and the v4.35 rename table; the landscape memo, repo map, AGENTS.md, and two new gotchas follow. Validated with `./scripts/validate.sh --lint --test --axioms` (zero sorry/axiom taint). Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01Nb4g3Vxgjhnhsca7BzAsFc --- AGENTS.md | 7 +- PolyFun.lean | 3 + PolyFun/Control/Do/Basic.lean | 16 +-- PolyFun/Control/Monad/Algebra/WP.lean | 122 ++++++++++++++++++ PolyFun/Control/Monad/Hom/WP.lean | 84 +++++++++++++ PolyFun/Control/Monad/Support/WP.lean | 158 ++++++++++++++++++++++++ PolyFun/PFunctor/Free/Do.lean | 4 +- PolyFunTest/Do/Algebra.lean | 66 ++++++++++ PolyFunTest/Do/FreeM.lean | 2 +- PolyFunTest/Do/Support.lean | 68 ++++++++++ docs/reading/program-logic-landscape.md | 16 ++- docs/wiki/gotchas.md | 19 +++ docs/wiki/program-logic.md | 92 ++++++++------ docs/wiki/repo-map.md | 5 +- 14 files changed, 604 insertions(+), 58 deletions(-) create mode 100644 PolyFun/Control/Monad/Algebra/WP.lean create mode 100644 PolyFun/Control/Monad/Hom/WP.lean create mode 100644 PolyFun/Control/Monad/Support/WP.lean create mode 100644 PolyFunTest/Do/Algebra.lean create mode 100644 PolyFunTest/Do/Support.lean diff --git a/AGENTS.md b/AGENTS.md index f83dc2b3..1ad33be0 100644 --- a/AGENTS.md +++ b/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`). diff --git a/PolyFun.lean b/PolyFun.lean index 215568a0..6d4f7631 100644 --- a/PolyFun.lean +++ b/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 diff --git a/PolyFun/Control/Do/Basic.lean b/PolyFun/Control/Do/Basic.lean index be6d84b6..6818c4ed 100644 --- a/PolyFun/Control/Do/Basic.lean +++ b/PolyFun/Control/Do/Basic.lean @@ -20,7 +20,7 @@ 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 @@ -28,7 +28,7 @@ It provides constructions — deliberately not instances — that transport core 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 diff --git a/PolyFun/Control/Monad/Algebra/WP.lean b/PolyFun/Control/Monad/Algebra/WP.lean new file mode 100644 index 00000000..c19ee589 --- /dev/null +++ b/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 diff --git a/PolyFun/Control/Monad/Hom/WP.lean b/PolyFun/Control/Monad/Hom/WP.lean new file mode 100644 index 00000000..7128f549 --- /dev/null +++ b/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 diff --git a/PolyFun/Control/Monad/Support/WP.lean b/PolyFun/Control/Monad/Support/WP.lean new file mode 100644 index 00000000..39fb856a --- /dev/null +++ b/PolyFun/Control/Monad/Support/WP.lean @@ -0,0 +1,158 @@ +/- +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.Support +public import PolyFun.Control.Monad.Algebra.WP +public import Std.Internal.Do + +/-! +# Exact support as core weakest preconditions + +The always/some judgments of a monad with exact support are core `WPMonad` interpretations at +the `Prop` carrier with no exception layer: demonically, `wp x post` is `AllOutputs post x`; +angelically, it is `SomeOutput post x`. Both satisfy core's inequational laws — the angelic +reading has no counterpart on the older `Std.Do` stack, whose transformers carry conjunctivity +as a field. The demonic reading is conjunctive (`toWPMonadDemonic_wpConjunctive`); the angelic +one is not, and `PolyFunTest/Control/MonadAttach.lean` pins the counterexample. Neither is a +global instance: install them scoped or local where the support semantics is intended, exactly +as `mAlgOrderedPropDemonic` is. + +`LawfulWPMonadAttach` mirrors, field for field, the class Lean master ships in +`Std/WP/Monad/Sound.lean` (public from v4.35): a `wp`-provable postcondition holds at every +value the computation can return. It lives in the `Std.Internal.Do` namespace so that the v4.35 +rename of that namespace to `Std.WP` deletes it. `support_subset_of_wp` and `allOutputs_of_wp` +turn any sound triple — including one discharged by `vcgen` — into a support fact. +-/ + +public section + +universe u v w z + +open Std.Internal.Do +open scoped Lean.Order + +namespace Std.Internal.Do + +/-- Soundness of the weakest precondition interpretation of `m`: a postcondition that `wp` proves +holds of every value the program returns. Mirrors `Std.WP.LawfulWPMonadAttach` on Lean master. -/ +class LawfulWPMonadAttach (m : Type u → Type v) (Pred : outParam (Type w)) + (EPred : outParam (Type z)) [Monad m] [MonadAttach m] [LawfulMonadAttach m] + [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] where + /-- From a `wp`-provable postcondition and a `MonadAttach.CanReturn` witness, conclude `P` at + that value. -/ + of_canReturn_wp {α : Type u} {x : m α} {P : α → Prop} {a : α} : + MonadAttach.CanReturn x a → + (Lean.Order.top ⊑ wp x (fun a => ⌜P a⌝) Lean.Order.top) → P a + +end Std.Internal.Do + +namespace MonadAttach + +section Eliminations + +variable {m : Type u → Type v} [Monad m] [MonadAttach m] [LawfulMonadAttach m] + {Pred : Type w} {EPred : Type z} [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] + [LawfulWPMonadAttach m Pred EPred] + +/-- Any sound weakest-precondition proof bounds the support. -/ +theorem support_subset_of_wp {α : Type u} {x : m α} {P : α → Prop} + (h : Lean.Order.top ⊑ wp x (fun a => ⌜P a⌝) Lean.Order.top) : support x ⊆ {a | P a} := + fun _ hcan => LawfulWPMonadAttach.of_canReturn_wp hcan h + +/-- The "always" phrasing of `support_subset_of_wp`: a sound weakest-precondition proof +discharges the almost-sure judgment. Untagged: its antecedent has no first-order pattern for +`grind` to index. -/ +theorem allOutputs_of_wp {α : Type u} {x : m α} {P : α → Prop} + (h : Lean.Order.top ⊑ wp x (fun a => ⌜P a⌝) Lean.Order.top) : AllOutputs P x := + fun _ hcan => LawfulWPMonadAttach.of_canReturn_wp hcan h + +end Eliminations + +section Demonic + +variable {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] + +/-- The demonic (all-outputs) interpretation at the `Prop` carrier: `wp x post` holds when every +possible output of `x` satisfies `post`. Not an instance. -/ +@[expose, instance_reducible] +def toWPMonadDemonic : WPMonad m Prop EPost.Nil where + toLawfulMonad := inferInstance + toWP _ := + { wpTrans := fun x => ⟨fun post _ => AllOutputs post x⟩ + wp_trans_monotone := fun _ _ _ _ _ _ hpost => allOutputs_mono hpost } + pure_le_wp_pure a post _ := (allOutputs_pure post a).mpr + bind_le_wp_bind x f post _ := fun h => (allOutputs_bind post x f).mpr fun a ha => h a ha + +@[simp] +theorem toWPMonadDemonic_wp {α : Type u} (x : m α) (post : α → Prop) (epost : EPost.Nil) : + ((toWPMonadDemonic (m := m)).toWP α).wp x post epost = AllOutputs post x := + rfl + +/-- Core's triple under the demonic interpretation is the guarded "always" judgment. -/ +theorem toWPMonadDemonic_triple_iff {α : Type u} (x : m α) (pre : Prop) (post : α → Prop) + (epost : EPost.Nil) : + @Std.Internal.Do.Triple Prop EPost.Nil (m α) α _ _ x ((toWPMonadDemonic (m := m)).toWP α) + pre post epost ↔ + (pre → AllOutputs post x) := by + let inst := (toWPMonadDemonic (m := m)).toWP α + exact ⟨fun h => h.le_wp, fun h => ⟨h⟩⟩ + +/-- The demonic interpretation is conjunctive: "always" distributes over `∧`. -/ +theorem toWPMonadDemonic_wpConjunctive {α : Type u} (x : m α) : + @WPConjunctive (m α) α Prop EPost.Nil _ _ ((toWPMonadDemonic (m := m)).toWP α) x := by + let inst := (toWPMonadDemonic (m := m)).toWP α + refine ⟨fun Q₁ Q₂ _ _ => ?_⟩ + change Lean.Order.meet (AllOutputs Q₁ x) (AllOutputs Q₂ x) → + AllOutputs (Lean.Order.meet Q₁ Q₂) x + rw [Lean.Order.meet_prop_eq_and] + rintro ⟨h₁, h₂⟩ a ha + rw [Lean.Order.meet_apply, Lean.Order.meet_prop_eq_and] + exact ⟨h₁ a ha, h₂ a ha⟩ + +/-- The demonic interpretation is sound in core's sense: `CanReturn` is exactly the support. -/ +theorem toWPMonadDemonic_lawfulWPMonadAttach : + @LawfulWPMonadAttach m Prop EPost.Nil _ _ _ _ _ (toWPMonadDemonic (m := m)) := by + let inst := toWPMonadDemonic (m := m) + refine ⟨fun {α x P a} hcan hwp => ?_⟩ + have h : AllOutputs (fun a => ⌜P a⌝) x := Lean.Order.of_top_le_prop hwp + simpa only [Lean.Order.ofProp_prop_eq] using h a hcan + +end Demonic + +section Angelic + +variable {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] + +/-- The angelic (some-output) interpretation at the `Prop` carrier: `wp x post` holds when some +possible output of `x` satisfies `post`. Expressible only on the inequational stack; not an +instance. -/ +@[expose, instance_reducible] +def toWPMonadAngelic : WPMonad m Prop EPost.Nil where + toLawfulMonad := inferInstance + toWP _ := + { wpTrans := fun x => ⟨fun post _ => SomeOutput post x⟩ + wp_trans_monotone := fun _ _ _ _ _ _ hpost => someOutput_mono hpost } + pure_le_wp_pure a post _ := (someOutput_pure post a).mpr + bind_le_wp_bind x f post _ := fun h => (someOutput_bind post x f).mpr h + +@[simp] +theorem toWPMonadAngelic_wp {α : Type u} (x : m α) (post : α → Prop) (epost : EPost.Nil) : + ((toWPMonadAngelic (m := m)).toWP α).wp x post epost = SomeOutput post x := + rfl + +/-- Core's triple under the angelic interpretation is the guarded "sometimes" judgment. -/ +theorem toWPMonadAngelic_triple_iff {α : Type u} (x : m α) (pre : Prop) (post : α → Prop) + (epost : EPost.Nil) : + @Std.Internal.Do.Triple Prop EPost.Nil (m α) α _ _ x ((toWPMonadAngelic (m := m)).toWP α) + pre post epost ↔ + (pre → SomeOutput post x) := by + let inst := (toWPMonadAngelic (m := m)).toWP α + exact ⟨fun h => h.le_wp, fun h => ⟨h⟩⟩ + +end Angelic + +end MonadAttach diff --git a/PolyFun/PFunctor/Free/Do.lean b/PolyFun/PFunctor/Free/Do.lean index f097269c..c7288bf4 100644 --- a/PolyFun/PFunctor/Free/Do.lean +++ b/PolyFun/PFunctor/Free/Do.lean @@ -17,7 +17,7 @@ semantics in two ways: * **Through a handler**: `FreeM.wpMonadOfHandler s` interprets programs by `FreeM.liftM s` into any monad already carrying a `WPMonad` structure, via - `MonadHom.transportWPMonad`. Registration is left to the caller. + `MonadHom.transportSPredWPMonad`. Registration is left to the caller. * **Demonically, with operations uninterpreted**: the *scoped* instances `instWPAll` / `instWPMonadAll` interpret `wp⟦x⟧ Q` as "every possible output of `x` satisfies `Q`" (the `MonadAttach.toWP` structure at the `.pure` post @@ -46,7 +46,7 @@ structure. Not an instance — register it scoped or local downstream. -/ @[instance_reducible] def wpMonadOfHandler {n : Type uB → Type w} {ps : PostShape.{uB}} [Monad n] [WPMonad n ps] (s : Handler n P) : WPMonad (FreeM P) ps := - (FreeM.liftMHom s).transportWPMonad + (FreeM.liftMHom s).transportSPredWPMonad namespace DemonicWP diff --git a/PolyFunTest/Do/Algebra.lean b/PolyFunTest/Do/Algebra.lean new file mode 100644 index 00000000..c5a7a1fe --- /dev/null +++ b/PolyFunTest/Do/Algebra.lean @@ -0,0 +1,66 @@ +/- +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.WP +public import Std.Tactic.Do +public import Mathlib.Data.ENat.Lattice + +/-! +# Ordered monad algebras on core's `vcgen` + +An ordered monad algebra installed locally as a `WPMonad` drives core's `vcgen`: the generic +`Spec.pure` / `Spec.bind` rules apply, the derived `wp` is `MAlgOrdered.wp` by `rfl`, and +core's triple is PolyFun's. The base algebra below is the identity algebra on a deterministic +monad at the carrier `ℕ∞`, the shape a quantitative carrier takes; the `Prop` carrier is +exercised through the support layer instead. The monad is a fresh copy of `Id` so that no +global core instance competes with the locally installed one. +-/ + +public section + +set_option mvcgen.warning false + +open Std.Internal.Do + +/-- A deterministic monad with no global weakest-precondition instance. -/ +@[expose] +def Det (α : Type) : Type := α + +instance : Monad Det where + pure a := a + bind x f := f x + +instance : LawfulMonad Det := + LawfulMonad.mk' Det (fun _ => rfl) (fun _ _ => rfl) (fun _ _ _ => rfl) + +/-- The identity ordered algebra on `Det` at the extended naturals. -/ +noncomputable local instance instMAlgOrderedDetENat : MAlgOrdered Det ℕ∞ where + μ x := x + μ_pure _ := rfl + μ_bind_mono _ _ h x := h x + +/-- Its core interpretation, installed locally. -/ +noncomputable local instance instWPMonadDetENat : WPMonad Det ℕ∞ EPost.Nil := + MAlgOrdered.toWPMonad + +/-- Agreement with PolyFun's `wp` is definitional. -/ +example (x : Det Nat) (post : Nat → ℕ∞) (epost : EPost.Nil) : + wp x post epost = MAlgOrdered.wp x post := + rfl + +/-- `vcgen` decomposes a `do` block through the locally installed algebra. -/ +example (c : ℕ∞) : + ⦃ c ⦄ (do let x ← pure 1; pure (x + 1) : Det Nat) ⦃ fun r => if r = 2 then c else ⊥ ⦄ := by + vcgen + change c ≤ _ + simp + +/-- Core's triple through the derived interpretation is PolyFun's triple. -/ +example (x : Det Nat) (pre : ℕ∞) (post : Nat → ℕ∞) : + Triple x pre post Lean.Order.bot ↔ MAlgOrdered.Triple pre x post := + MAlgOrdered.toWP_triple_iff x pre post Lean.Order.bot diff --git a/PolyFunTest/Do/FreeM.lean b/PolyFunTest/Do/FreeM.lean index 0148fbe0..20227e3a 100644 --- a/PolyFunTest/Do/FreeM.lean +++ b/PolyFunTest/Do/FreeM.lean @@ -68,7 +68,7 @@ example (a : Bool) (h : MonadAttach.CanReturn flipTwo a) : a = true ∨ a = fals /-- The same, phrased as the "always" judgment over the support. -/ example : MonadAttach.AllOutputs (fun b => b = true ∨ b = false) flipTwo := by - refine MonadAttach.allOutputs_of_wp ?_ + refine MonadAttach.allOutputs_of_wpSPred ?_ mvcgen [flipTwo] intro x y cases x && y <;> simp diff --git a/PolyFunTest/Do/Support.lean b/PolyFunTest/Do/Support.lean new file mode 100644 index 00000000..e61d0da4 --- /dev/null +++ b/PolyFunTest/Do/Support.lean @@ -0,0 +1,68 @@ +/- +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.Support.WP +public import Std.Tactic.Do + +/-! +# Exact support on core's `vcgen` + +The demonic interpretation of a monad with exact support, installed locally, lets `vcgen` +decompose `do` blocks whose leaves are then discharged against the support: `wp` is the +"always" judgment by `rfl`, core's triple is the guarded judgment, and a sound triple converts +back into a support fact through `allOutputs_of_wp`. The angelic interpretation is checked to +compute the "sometimes" judgment. +-/ + +public section + +set_option mvcgen.warning false + +open Std.Internal.Do MonadAttach + +/-- The demonic interpretation of `SetM`, installed locally. -/ +local instance instWPMonadSetMDemonic : WPMonad SetM Prop EPost.Nil := + toWPMonadDemonic + +/-- A nondeterministic choice followed by a deterministic step. -/ +def choose12 : SetM Nat := do + let x ← (({1, 2} : Set Nat) : SetM Nat) + pure (x + 1) + +/-- `wp` is the "always" judgment. -/ +example (x : SetM Nat) (post : Nat → Prop) (epost : EPost.Nil) : + wp x post epost = AllOutputs post x := + rfl + +/-- `vcgen` decomposes the bind chain; the nondeterministic leaf has no registered +specification, so its verification condition is left as a support fact. -/ +theorem choose12_spec : ⦃ True ⦄ choose12 ⦃ fun r => r = 2 ∨ r = 3 ⦄ := by + vcgen -errorOnMissingSpec [choose12] + intro a ha + have ha' : a ∈ ({1, 2} : Set Nat) := SetM.canReturn_iff.mp ha + simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at ha' + change AllOutputs (fun r => r = 2 ∨ r = 3) (pure (a + 1) : SetM Nat) + rw [allOutputs_pure] + omega + +/-- A sound triple converts back into a support fact. -/ +example : AllOutputs (fun r => r = 2 ∨ r = 3) choose12 := by + have := toWPMonadDemonic_lawfulWPMonadAttach (m := SetM) + refine allOutputs_of_wp ?_ + intro _ + simpa only [Lean.Order.ofProp_prop_eq] using choose12_spec.le_wp trivial + +/-- The demonic interpretation is conjunctive. -/ +example (x : SetM Nat) : + @WPConjunctive (SetM Nat) Nat Prop EPost.Nil _ _ (instWPMonadSetMDemonic.toWP Nat) x := + toWPMonadDemonic_wpConjunctive x + +/-- The angelic interpretation computes the "sometimes" judgment. -/ +example (x : SetM Nat) (post : Nat → Prop) (epost : EPost.Nil) : + ((toWPMonadAngelic (m := SetM)).toWP Nat).wp x post epost = SomeOutput post x := + rfl diff --git a/docs/reading/program-logic-landscape.md b/docs/reading/program-logic-landscape.md index 8e5a9142..f9aaeba0 100644 --- a/docs/reading/program-logic-landscape.md +++ b/docs/reading/program-logic-landscape.md @@ -74,9 +74,18 @@ substrates; core `Std.Do` is used only behind a two-file quarantine. `Handler`; soundness `wpFold_le_wpVia` / `wpFold_eq_wpVia` (the generic engine behind VCVio's `HandlerSpecs` pattern); coherence of demonic/angelic folds with `AllOutputs`/`SomeOutput`. +- `Control/Monad/Algebra/WP.lean`, `Control/Monad/Support/WP.lean`, + `Control/Monad/Hom/WP.lean` — the bridges to core's lattice-generic stack + (`Std.Internal.Do`, public as `Std.WP` from v4.35, driven by `vcgen`): + `MAlgOrdered.toWPMonad` for Mathlib-lattice carriers, the demonic and angelic + `WPMonad` interpretations of exact support, conjunctivity of the demonic one, + a mirror of master's `LawfulWPMonadAttach` with `support_subset_of_wp` / + `allOutputs_of_wp`, and transport along monad morphisms. These are the + canonical interface; `PolyFunTest/Do/{Algebra,Support}.lean` run `vcgen` + through them. - `Control/Do/Basic.lean` + `PFunctor/Free/Do.lean` — the core-`Std.Do` - quarantine: `MonadHom.transportWP(Monad)`, `MonadAttach.toWP(Monad)`, - `toWPSound` plus `support_subset_of_wp`/`allOutputs_of_wp` (any `WPSound` + quarantine: `MonadHom.transportSPredWP(Monad)`, `MonadAttach.toWP(Monad)`, + `toWPSound` plus `support_subset_of_wpSPred`/`allOutputs_of_wpSPred` (any `WPSound` triple becomes a support fact), scoped demonic `WP (FreeM P) .pure` instances, and the `Spec.lift` `@[spec]` lemma; `mvcgen` decomposes `do`-programs over `FreeM` with uninterpreted @@ -132,7 +141,8 @@ implemented). invariant inside the state relation, since `ITree` has no possible-output predicate for a postcondition to range over. wp-congruence under `WeakBisim` remains open. -- The public angelic WP bridge is **blocked at the current Lean 4.34.0-rc2 pin**, not +- The angelic WP bridge exists on the lattice-generic stack + (`MonadAttach.toWPMonadAngelic`); on the older `Std.Do` stack it is **blocked**, not merely unwritten. `Std.Do.PredTrans` carries conjunctivity as a structure field, stated as a bi-entailment; `AllOutputs` distributes over `∧` both ways but `SomeOutput` only diff --git a/docs/wiki/gotchas.md b/docs/wiki/gotchas.md index 884cfb78..71839584 100644 --- a/docs/wiki/gotchas.md +++ b/docs/wiki/gotchas.md @@ -299,6 +299,25 @@ unused; the same statement over a `def` interface, or over a generic `P`, matche unaffected. State canaries and downstream lemmas over a generic or `def`-declared interface, or rewrite explicitly, rather than "fixing" the lemma. +### 11b. `vcgen` finds no spec unless the `Std.Internal.Do` root is imported + +`vcgen` consults the `@[spec]` database, and `Spec.bind` / `Spec.pure` live in +`Std.Internal.Do.Triple.SpecLemmas`. A file that imports only `Std.Internal.Do.WP.Basic` +(or reaches the stack through such a module) gets `No spec found for program …` on every +`do` block, with an empty candidate list. Import the root `Std.Internal.Do`; the bridge +modules under `PolyFun/Control/Monad/*/WP.lean` do so for this reason. A leaf with no +registered specification is left as a verification condition with +`vcgen -errorOnMissingSpec`. + +### 11c. Projections re-synthesize instance-implicit structure arguments + +`Triple`, `WPConjunctive`, and `LawfulWPMonadAttach` take their `WP` / `WPMonad` as +instance-implicit parameters. Projecting (`h.le_wp`) or constructing (`⟨h⟩`, `refine ⟨…⟩`) a +value whose interpretation is a *non-instance* construction (`MAlgOrdered.toWP α`, +`MonadAttach.toWPMonadDemonic`) makes Lean synthesize the instance afresh and fail. Bind the +construction first — `let inst := MAlgOrdered.toWP α` — so it is found as a local instance; +`let`, not `have`, so it stays definitionally the term in the statement. + ### 12. `Std.Do` imports are quarantined Only `PolyFun/Control/Do/Basic.lean`, `PolyFun/PFunctor/Free/Do.lean`, and diff --git a/docs/wiki/program-logic.md b/docs/wiki/program-logic.md index 42ff2573..832e947f 100644 --- a/docs/wiki/program-logic.md +++ b/docs/wiki/program-logic.md @@ -16,9 +16,12 @@ migration sketch live in | `PolyFun/Control/Monad/Support.lean` | `ExactMonadAttach m`: the introduction rules core omits for `MonadAttach.CanReturn`; `MonadAttach.support`; the `AllOutputs`/`SomeOutput`/`NoOutput` judgments and scoped `⊨ₐ`/`⊨ₛ`/`⊭` notation; the named demonic `MAlgOrdered m Prop` choice; instances for `Except`/`SetM` (absent upstream) and the `ExceptT` universe alias | | `PolyFun/PFunctor/Free/Support.lean` | `MonadAttach`/`ExactMonadAttach` for `FreeM P` with a computable, axiom-free `attach`; structural equations by `rfl`; coherence with `Free/Path.lean` (`support_eq_range_output`) and with the powerset fold (`support_eq_liftM_univ`) | | `PolyFun/PFunctor/Free/WP.lean` | `OpSpec P l` per-operation specs; syntactic `FreeM.wpFold` (with `demonic`/`angelic`); `OpSpec.toMAlgOrdered`; semantic `FreeM.wpVia` through a `Handler`; soundness `wpFold_le_wpVia`/`wpFold_eq_wpVia` | -| `PolyFun/Control/Do/Basic.lean` | Core-`Std.Do` transports: `MonadHom.transportWP(Monad)` along a monad morphism, `MonadAttach.toWP(Monad)` demonically at `.pure`, `toWPSound` for core-sense soundness, and `support_subset_of_wp`/`allOutputs_of_wp` turning any `WPSound` triple into a support fact | +| `PolyFun/Control/Do/Basic.lean` | Legacy core-`Std.Do` transports: `MonadHom.transportSPredWP(Monad)` along a monad morphism, `MonadAttach.toWP(Monad)` demonically at `.pure`, `toWPSound` for core-sense soundness, and `support_subset_of_wpSPred`/`allOutputs_of_wpSPred` turning any `WPSound` triple into a support fact | | `PolyFun/ITree/Do.lean` | Productive `while` for interaction trees: `forInLoop`, the scoped `ForIn` instance, and `forInLoop_weakBisim_of_invariant` — an invariant-scoped `WeakBisim` congruence because `iter` is lawful only up to weak bisimulation | | `PolyFun/PFunctor/Free/Do.lean` | Scoped demonic `WP (FreeM P) .pure` instances (`open scoped PFunctor.FreeM.DemonicWP`), `wpMonadOfHandler`, and the `Spec.lift` `@[spec]` lemma enabling `mvcgen` on free programs with uninterpreted operations | +| `PolyFun/Control/Monad/Algebra/WP.lean` | `MAlgOrdered.toWP` / `toWPMonad`: an ordered monad algebra as a core `Std.Internal.Do.WPMonad m l EPost.Nil` (through the `ToCslib.Order.LeanOrder` bridge), `wp` agreement by `rfl`, `toWP_triple_iff`, `wpConjunctiveOf`, and the transfer lemmas `top_eq_top` / `meet_eq_inf` / `join_eq_sup` between core's and Mathlib's lattice operations | +| `PolyFun/Control/Monad/Support/WP.lean` | `MonadAttach.toWPMonadDemonic` / `toWPMonadAngelic`: the always/some judgments as `WPMonad m Prop EPost.Nil`; conjunctivity of the demonic reading; the `LawfulWPMonadAttach` mirror of Lean master's soundness class with its demonic instance; `support_subset_of_wp` / `allOutputs_of_wp` | +| `PolyFun/Control/Monad/Hom/WP.lean` | `MonadHom.transportWP` / `transportWPMonad` / `transportWPMonadOf`: pulling a core `WPMonad` back along a (bundled or unbundled) monad morphism | Worked examples: `PolyFunTest/Control/MonadAttach.lean` (judgments, notation, `Iff.rfl` transfer contract) and `PolyFunTest/Do/FreeM.lean` (`mvcgen` smoke @@ -38,10 +41,11 @@ The support layer is a three-way split: core's implications into the equivalence support reasoning rewrites with. Extending `LawfulMonadAttach` rather than the weak class simultaneously excludes `MonadAttach.trivial` (`CanReturn := True`, i.e. `support = univ`). -- **`WPSound` is the bridge.** `MonadAttach.toWPSound` proves PolyFun's demonic - interpretation sound in core's sense, and `support_subset_of_wp` / - `allOutputs_of_wp` convert any `WPSound` weakest-precondition proof — including - an `mvcgen`-discharged one — into a support fact. +- **Soundness is the bridge.** On the canonical stack `LawfulWPMonadAttach` with + `support_subset_of_wp` / `allOutputs_of_wp` convert any sound weakest-precondition + proof — including a `vcgen`-discharged one — into a support fact; on the legacy + stack `MonadAttach.toWPSound` and `support_subset_of_wpSPred` / `allOutputs_of_wpSPred` + play the same role. Core supplies the instances for `Id`, `Option`, `OptionT`, `ExceptT`, `StateT`, and `ReaderT`; PolyFun adds `Except` and `SetM` (which core lacks), a @@ -130,43 +134,51 @@ reducible unfoldings such as VCVio's `OracleComp`. The demonic instances are ## The two upstream WP stacks -Core ships **two** complete weakest-precondition stacks at the v4.34.0-rc2 pin, and PolyFun -bridges the older one. Knowing which is which matters, because they differ on exactly the -property that decides what PolyFun can express. +Core ships **two** complete weakest-precondition stacks at the v4.34.0-rc2 pin. PolyFun's +canonical interface is the lattice-generic one; the older SPred one is bridged only for the +existing `mvcgen` smoke tests until the free-monad layer moves over. -| | `Std/Do/` (bridged here) | `Std/Internal/Do/` | +| | `Std/Internal/Do/` (canonical here) | `Std/Do/` (legacy bridge) | |---|---|---| -| Assertions | `SPred` / `PostShape` | any `Lean.Order.CompleteLattice` | -| `WPMonad` bind law | equational (`wp_bind : … = …`) | inequational (`bind_le_wp_bind`) | -| Conjunctivity | a **field of `PredTrans`**, bi-entailment | opt-in class `WPConjunctive`, one-directional | -| Soundness | `WPSound`, via `Internal.Ensures` | — | -| Also has | — | `WP.Frames`, `frameClosure`, `PreservesSup`, `RepeatInvariant` | -| Visibility | public | `Internal` | - -**The conjunctivity field is why the WP bridge is demonic-only.** `Std.Do.PredTrans` requires -`t (Q₁ ∧ₚ Q₂) ⊣⊢ₛ t Q₁ ∧ t Q₂`. `AllOutputs` distributes over `∧` in both directions, so -`MonadAttach.toWP` discharges it. `SomeOutput` distributes only left-to-right — two different -outputs may witness the two conjuncts separately — so there is no angelic `Std.Do.WP` at all. -That is a structural obstruction, not an unwritten lemma; -`PolyFunTest/Control/MonadAttach.lean` proves both directions and the failure. The angelic -reading therefore lives at the `MAlgOrdered` level, whose `μ_bind_mono` asks only for -monotonicity. - -**What changes upstream.** Beyond this pin, core promotes `Std.Internal.Do` verbatim to a -public `Std.WP`, replaces `WPSound` with `Std.WP.LawfulWPMonadAttach` — whose one field -concludes from a `MonadAttach.CanReturn` witness directly, dropping the `Ensures` -formulation — and deprecates `mvcgen` in favour of `vcgen`. All three ship in **v4.35**, not -v4.34. Two consequences for this layer: `support_subset_of_wp` / `allOutputs_of_wp` are -already stated against `CanReturn`, so they carry over as a rename; and `WPConjunctive` -being opt-in is what would unblock an angelic bridge. Its one law is exactly the reverse -conjunction direction refuted by the test, so that bridge would not provide the optional -class. - -`MAlgOrdered` is recognisably `Std.Internal.Do.WPMonad` minus exception postconditions — but -over Mathlib's `CompleteLattice`, while every piece of core WP machinery is over -`Lean.Order.CompleteLattice`, and the pinned Mathlib contains no bridge between the two -hierarchies. Adopting core's stack means porting `MAlgOrdered` off Mathlib's order hierarchy. -That cost is recorded here deliberately; it is not this layer's current direction. +| Assertions | any `Lean.Order.CompleteLattice` (`Assertion`) | `SPred` / `PostShape` | +| `WPMonad` bind law | inequational (`bind_le_wp_bind`) | equational (`wp_bind : … = …`) | +| Conjunctivity | opt-in, per program (`WPConjunctive x`) | a **field of `PredTrans`**, bi-entailment | +| Exceptions | `EPred` postconditions (`EPost.Nil`, `EPost.Cons`) | `ExceptConds` inside `PostCond` | +| Tactic | `vcgen` | `mvcgen` (deprecated on master) | +| Upstream fate | public `Std.WP` in v4.35 | retired | + +The inequational law is what lets *both* support readings instantiate the canonical stack: +`MonadAttach.toWPMonadDemonic` (`wp x post = AllOutputs post x`) and `toWPMonadAngelic` +(`wp x post = SomeOutput post x`). Only the demonic reading is conjunctive; the angelic one +distributes over `∧` in one direction only, which is exactly why it has no `Std.Do.WP` and no +`WPConjunctive` instance (`PolyFunTest/Control/MonadAttach.lean` proves the counterexample). +`MAlgOrdered.toWPMonad` gives every Mathlib-lattice carrier the same treatment through the +`ToCslib.Order.LeanOrder` bridge, and `MonadHom.transportWPMonad` pulls any of these back along +a monad morphism. None of them is a global instance; install them `local` or `scoped` at the +carrier (`PolyFunTest/Do/{Algebra,Support}.lean` show `vcgen` running through each). + +Three practical rules for writing against the canonical stack: + +- Import the `Std.Internal.Do` **root** wherever a `vcgen` proof is expected: the `@[spec]` + database (`Spec.bind`, `Spec.pure`, …) lives in `Std.Internal.Do.Triple.SpecLemmas`, and + importing only `WP.Basic` yields `No spec found for program …` on every `do` block. The bridge + modules import the root for this reason. +- A structure with an instance-implicit parameter re-synthesizes that instance on projection + and construction (`h.le_wp`, `⟨h⟩`, `refine ⟨…⟩` for `WPConjunctive`), so a proof about a + non-instance interpretation binds it first: `let inst := MAlgOrdered.toWP α`. +- Naming a theorem `Lean.Order.foo` elaborates it inside that namespace, activating core's + scoped `⊤` / `⊓` / `⊔` and shadowing Mathlib's `le_top` / `le_inf`; keep transfer lemmas in + a PolyFun namespace and qualify core's names. + +**Renames at the v4.35 bump** (recorded so the migration is mechanical): +`Std.Internal.Do` → `Std.WP`; `EPost.Nil` → `EStack⟨⟩` and `EPost.Cons eh et` → `eh × et`; +`Std.Internal.Do.Order.*` → `Std.Internal.Order.*`; the local `LawfulWPMonadAttach` is deleted +in favour of `Std.WP.LawfulWPMonadAttach` (same field); `ForIn.forInWithInvariant` → +`forInPureWithInvariant`; `mvcgen` is deprecated. + +`MAlgOrdered` stays: it is the Mathlib-lattice kernel VCVio's quantitative carrier bridges to +by `rfl`, and its `WriterT` lift has no core counterpart. The bridge, not a port, is what +connects it to core's order hierarchy. ## What stays downstream diff --git a/docs/wiki/repo-map.md b/docs/wiki/repo-map.md index 644d3014..140b1e4c 100644 --- a/docs/wiki/repo-map.md +++ b/docs/wiki/repo-map.md @@ -29,8 +29,9 @@ PolyFun/ Control/ monad/comonad and LTS infrastructure (Coalgebra, Comonad, Lawful, Free, Iter, Bisimulation, LTS/Trace), including the program-logic kernel - (Monad/{Algebra, Support}) and the core-Std.Do - quarantine root (Do/Basic) + (Monad/{Algebra, Support}), its bridges to core's + lattice-generic WP stack (Monad/{Algebra, Support, Hom}/WP) + and the core-Std.Do quarantine root (Do/Basic) Logic/ small logic helpers (HEq) ToCslib/ lowest production layer, staging what PolyFun upstreams: