feat(tocslib): stage the free-monad API, loop transport, and order bridge

AGENTS.md

@@ -112,10 +112,18 @@ and depend on this library.
 - `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`).
-- `ToCslib/`: a separate low-level Lake library of reusable extensions to the
-  pinned cslib machine API. It imports cslib and Mathlib but never PolyFun,
-  oracle semantics, probability, or cryptography. Concrete PolyFun backend
-  adapters may import it explicitly; the generated `PolyFun` umbrella does not.
+- `ToCslib/`: a separate Lake library that is the lowest layer under
+  PolyFun and stages what PolyFun will upstream: extensions of the pinned
+  cslib machine API (`Computability/`), additions to cslib's free monad
+  `PFunctor.FreeM` (`Data/PFunctor/Free/`: a normal-form case principle,
+  `map_pure` / `map_bind`, the catamorphism `foldFreeM`, handler fusion, and
+  commutation of `liftM` with loops), transport of loop combinators along
+  `pure`/`bind`-preserving functions plus effect-free loop instances for
+  `Option` and `Vector` (`Control/`), and the bridge from Mathlib's
+  `CompleteLattice` to core's `Lean.Order.CompleteLattice` (`Order/`). It
+  imports core, cslib, and Mathlib but never PolyFun, `Std.Do`, oracle
+  semantics, probability, or cryptography; PolyFun modules import it
+  directly. Its umbrella `ToCslib.lean` is generated like `PolyFun.lean`.
 - `PolyFunTest/`: separate test / worked-example library (glob
   `PolyFunTest.+`), built by `lake test` and kept out of the `lake lint`
   scope. Holds the dynamical / interaction worked examples and the
@@ -129,7 +137,7 @@ dependency map lives in [`docs/wiki/repo-map.md`](docs/wiki/repo-map.md#conceptu
 Update that map when a change adds a module or changes an import boundary.
 
 New files must respect the documented DAG. Re-exports through
-`PolyFun.lean` are auto-generated; do not hand-edit.
+`PolyFun.lean` and `ToCslib.lean` are auto-generated; do not hand-edit.
 
 All Lean sources use module mode. In production files, make the intended API
 explicit with `public section` and expose individual reducer bodies only when
@@ -206,25 +214,30 @@ Structures use UpperCamelCase: `PFunctor`, `TypeTree`, `Decoration`,
    parameters are mathematically and compositionally intentional; explain
    that reason in an adjacent comment. This matches the treatment of
    universe-separated polynomial position/direction data upstream.
-6. **`PolyFun.lean` is generated.** Do not hand-edit it. After adding,
-   renaming, or deleting `.lean` files under `PolyFun/`, run
-   `./scripts/update-lib.sh`.
+6. **`PolyFun.lean` and `ToCslib.lean` are generated.** Do not hand-edit
+   them. After adding, renaming, or deleting `.lean` files under `PolyFun/`
+   run `./scripts/update-lib.sh`; under `ToCslib/`, run
+   `./scripts/update-lib.sh ToCslib`.
 7. **Do not introduce `sorry` or `admit` in finished work.** Use `stop`
    only when explicitly preserving partial proof work during a refactor.
-8. **`Std.Do` imports are quarantined.** Only
-   `PolyFun/Control/Do/Basic.lean`, `PolyFun/PFunctor/Free/Do.lean`, and
-   `PolyFunTest/Do/` may import core `Std.Do`, `Std.Internal.Do`, or
-   `Std.Tactic.Do` (`mvcgen` / `vcgen`), and they export constructions
-   (`def`s and `scoped` instances), never global `WP` instances. See
-   `docs/wiki/program-logic.md`.
+8. **`Std.Do` imports are quarantined, in two tiers.** The definitions
+   (`Std.Do`, `Std.Internal.Do`: `WP`, `WPMonad`, `Triple`, spec lemmas) may
+   be imported only by the program-logic kernel — `PolyFun/Control/Monad/`,
+   `PolyFun/Control/Do/`, `PolyFun/PFunctor/Free/`, `PolyFun/ITree/Do.lean` —
+   and by `PolyFunTest/Do/`. The tactics (`Std.Tactic.Do`: `mvcgen`,
+   `vcgen`, the `@[spec]` attribute syntax) stay in `PolyFun/Control/Do/`,
+   `PolyFun/PFunctor/Free/Do.lean`, and `PolyFunTest/Do/`. `ToCslib/` imports
+   neither. Fenced modules export constructions (`def`s and `scoped`
+   instances), never global `WP` instances. See `docs/wiki/program-logic.md`.
 
 ## Building
 
 ```bash
 lake exe cache get && lake build
 ```
 
-After adding new `.lean` files: `./scripts/update-lib.sh`.
+After adding new `.lean` files: `./scripts/update-lib.sh` (and
+`./scripts/update-lib.sh ToCslib` for the staging library).
 For routine local validation: `./scripts/validate.sh`.
 For anything that must stay axiom-clean, run `./scripts/validate.sh --axioms`.
 PolyFun has a zero-debt baseline: do not add `sorry` or non-standard axioms to it.

PolyFun/PFunctor/Free/Basic.lean

@@ -8,13 +8,16 @@ module
 public import PolyFun.Control.Monad.Hom
 public import PolyFun.PFunctor.Basic
 public import PolyFun.PFunctor.Lens.Basic
-public import Cslib.Foundations.Data.PFunctor.Free
+public import ToCslib.Data.PFunctor.Free.Basic
 
 /-!
 # Free Monad of a Polynomial Functor
 
-We define the free monad on a **polynomial functor** (`PFunctor`), and prove some basic properties.
-
+PolyFun's layer over cslib's free monad `PFunctor.FreeM`: the W-type presentations, root
+predicates, transport along lenses, and the bundled monad-homomorphism form of `FreeM.liftM`
+with its universal property and naturality. The purely free-monadic lemmas that used to live
+here (`map_pure`, `map_bind`, `foldFreeM`, `liftM_comp`, `liftM_lift_eq_self`, …) are staged for
+cslib in `ToCslib.Data.PFunctor.Free.Basic`, which this module re-exports.
 -/
 
 @[expose] public section
@@ -37,31 +40,6 @@ namespace FreeM
 
 variable {P : PFunctor.{uA, uB}} {α β γ : Type v}
 
-/-! ## Public constructor equations -/
-
-/-- Mapping a value through a leaf is visible through an ordinary module import,
-with the leaf written using the public `Pure` operation. -/
-@[simp]
-theorem map_pure {X : Type uβ} {Y : Type uγ} (f : X → Y) (x : X) :
-    FreeM.map (P := P) f (pure x : FreeM P X) = (pure (f x) : FreeM P Y) :=
-  rfl
-
-/-- Mapping a value through a query preserves its position and maps every
-continuation. -/
-theorem map_liftBind {X : Type uβ} {Y : Type uγ} (f : X → Y)
-    (a : P.A) (rest : P.B a → FreeM P X) :
-    FreeM.map f (FreeM.liftBind a rest) =
-      FreeM.liftBind a (fun direction ↦ FreeM.map f (rest direction)) :=
-  rfl
-
-/-- Mapping through a query written as `lift` followed by `bind` maps every
-continuation without requiring clients to expose `liftBind`. -/
-theorem map_lift_bind {X : Type uβ} {Y : Type uγ} (f : X → Y)
-    (a : P.A) (rest : P.B a → FreeM P X) :
-    FreeM.map f ((FreeM.lift a).bind rest) =
-      (FreeM.lift a).bind (fun direction ↦ FreeM.map f (rest direction)) :=
-  rfl
-
 /-! ## Fixed-point presentation -/
 
 /-- Reinterpret a finite free program as the W-type of query-or-return
@@ -171,24 +149,6 @@ def equivWOfIsEmpty [IsEmpty α] : FreeM P α ≃ P.W where
     induction w with
     | mk a f ih => exact congrArg (WType.mk a) (funext ih)
 
-lemma monad_bind_def (x : FreeM P α) (g : α → FreeM P β) :
-    x >>= g = FreeM.bind x g := rfl
-
-/-- Mapping after a free-monad bind can be moved into each continuation. -/
-theorem bind_map_right {δ : Type uδ} {β : Type uβ} {γ : Type uγ}
-    (mx : FreeM P δ) (g : δ → FreeM P β) (f : β → γ) :
-    FreeM.bind mx (fun x => FreeM.map f (g x)) =
-      FreeM.map f (FreeM.bind mx g) := by
-  simpa only [FreeM.bind_pure_comp] using
-    (FreeM.bind_assoc mx g (pure ∘ f)).symm
-
-/-- Mapping after a free-monad bind distributes through its continuation. -/
-theorem map_bind {δ : Type uδ} {β : Type uβ} {γ : Type uγ}
-    (f : β → γ) (mx : FreeM P δ) (g : δ → FreeM P β) :
-    FreeM.map f (FreeM.bind mx g) =
-      FreeM.bind mx (fun x ↦ FreeM.map f (g x)) :=
-  (bind_map_right mx g f).symm
-
 section mapLens
 
 variable {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}}
@@ -307,10 +267,8 @@ omit [LawfulMonad m] [LawfulMonad n] in
 `FreeM.liftM s` is the fold of the post-composed handler `fun a => φ (s a)` — the value-level
 naturality square of the universal fold. -/
 @[simp] theorem liftM_natural (φ : m →ᵐ n) (x : FreeM P α) :
-    φ (FreeM.liftM s x) = FreeM.liftM (fun a => φ (s a)) x := by
-  induction x with
-  | pure x => exact φ.mmap_pure x
-  | lift_bind a r ih => simp [ih]
+    φ (FreeM.liftM s x) = FreeM.liftM (fun a => φ (s a)) x :=
+  FreeM.map_liftM (fun x => φ x) φ.mmap_pure φ.mmap_bind s x
 
 /-- Bundled form of `liftM_natural`: composing the fold monad-homomorphism `FreeM.liftMHom s` with
 a monad morphism `φ` is the fold of the post-composed handler. -/
@@ -342,39 +300,10 @@ section idFold
 
 variable {α : Type uB}
 
-/-- The fold with the canonical re-lifting handler `FreeM.lift` is the identity: interpreting each
-position back into the free monad recovers the tree (equivalently `FreeM.liftMHom FreeM.lift` is
-the identity homomorphism, `liftMHom_lift_eq_id`). The upstream form of `simulateQ` of the
-identity handler being the identity — a corollary of the universal property. -/
-@[simp] theorem liftM_lift_eq_self (x : FreeM P α) : FreeM.liftM FreeM.lift x = x := by
-  induction x with
-  | pure y => rfl
-  | lift_bind a r ih => simp [ih]
-
 theorem liftMHom_lift_eq_id :
     FreeM.liftMHom (P := P) (m := FreeM P) FreeM.lift = MonadHom.id (FreeM P) :=
   MonadHom.ext' fun _ x => by simp
 
-/-- Interpreting a free tree by a free handler and then interpreting the
-resulting free tree by an arbitrary monadic handler is the same as interpreting
-once by their pointwise Kleisli composite. -/
-theorem liftM_comp {Q : PFunctor.{uA₂, uB}} {m : Type uB → Type v}
-    [Monad m] [LawfulMonad m]
-    (x : FreeM P α)
-    (first : (a : P.A) → FreeM Q (P.B a))
-    (second : (a : Q.A) → m (Q.B a)) :
-    (x.liftM first).liftM second =
-      x.liftM (fun a => (first a).liftM second) := by
-  induction x with
-  | pure _ => rfl
-  | lift_bind a rest ih =>
-      change
-        ((first a >>= fun b => (rest b).liftM first).liftM second) =
-          (first a).liftM second >>= fun b =>
-            (rest b).liftM (fun a => (first a).liftM second)
-      rw [FreeM.liftM_bind]
-      exact congrArg (fun k => (first a).liftM second >>= k) (funext ih)
-
 end idFold
 
 end FreeM

PolyFun/PFunctor/Free/Cursor/Fork.lean

@@ -531,7 +531,7 @@ theorem filterMapLocateAndForkAt_eq_bind_complete [DecidableEq P.A]
               first := located.completion
               second := second }) located.occurrence.complete := by
   unfold filterMapLocateAndForkAt locateAndForkAt
-  rw [← bind_map_right]
+  rw [map_bind]
   apply congrArg (FreeM.bind (withPath program))
   funext path
   rcases hlocate : locateAt? target program path n with _ | located
@@ -570,7 +570,7 @@ theorem locateAndForkAt_liftBind_same_succ [DecidableEq P.A] (target : P.A)
   rw [withPath_liftBind_bind]
   apply congrArg (FreeM.liftBind target)
   funext answer
-  rw [← bind_map_right]
+  rw [map_bind]
   apply congrArg (FreeM.bind (withPath (next answer)))
   funext suffix
   rw [locateAt?_liftBind_same_succ]
@@ -590,7 +590,7 @@ theorem locateAndForkAt_liftBind_other [DecidableEq P.A] {target a : P.A}
   rw [withPath_liftBind_bind]
   apply congrArg (FreeM.liftBind a)
   funext answer
-  rw [← bind_map_right]
+  rw [map_bind]
   apply congrArg (FreeM.bind (withPath (next answer)))
   funext suffix
   rw [locateAt?_liftBind_other hne]

PolyFun/PFunctor/Free/Cursor/Occurrence.lean

@@ -324,7 +324,7 @@ theorem map_completeFork_found (occurrence : Occurrence target program n)
           first := first
           second := second })) occurrence.complete := by
   rw [completeFork_found]
-  rw [← bind_map_right]
+  rw [map_bind]
   apply congrArg (FreeM.bind occurrence.complete)
   funext first
   rw [← FreeM.comp_map]
@@ -376,7 +376,7 @@ theorem completeFork_prependSame {next : P.B target → FreeM P α} (answer : P.
       simp only [Occurrence.resume, FreeM.map]
       apply congrArg (FreeM.liftBind target)
       funext firstAnswer
-      rw [← bind_map_right]
+      rw [map_bind]
       apply congrArg (FreeM.bind (withPath (occurrence.resume firstAnswer)))
       funext firstSuffix
       apply congrArg (FreeM.liftBind target)
@@ -398,7 +398,7 @@ theorem completeFork_prependOther {a : P.A} {next : P.B a → FreeM P α} (hne :
       simp only [Occurrence.resume, FreeM.map]
       apply congrArg (FreeM.liftBind target)
       funext firstAnswer
-      rw [← bind_map_right]
+      rw [map_bind]
       apply congrArg (FreeM.bind (withPath (occurrence.resume firstAnswer)))
       funext firstSuffix
       apply congrArg (FreeM.liftBind target)
@@ -572,7 +572,7 @@ theorem splitAt_bind_complete [DecidableEq P.A] (target : P.A) : (program : Free
             change FreeM.bind (splitAt a (next answer) n)
                 (fun result => FreeM.map addPrefix (Split.complete result)) =
               FreeM.map addPrefix (withPath (next answer))
-            rw [bind_map_right, ih answer n]
+            rw [← map_bind, ih answer n]
       · simp only [splitAt, dite_eq_right h, withPath]
         apply congrArg (FreeM.liftBind a)
         funext answer
@@ -588,7 +588,7 @@ theorem splitAt_bind_complete [DecidableEq P.A] (target : P.A) : (program : Free
         change FreeM.bind (splitAt target (next answer) n)
             (fun result => FreeM.map addPrefix (Split.complete result)) =
           FreeM.map addPrefix (withPath (next answer))
-        rw [bind_map_right, ih answer n]
+        rw [← map_bind, ih answer n]
 
 /-- Erasing validity certificates from `splitAtValid` recovers `splitAt`. -/
 theorem map_val_splitAtValid [DecidableEq P.A] (target : P.A) : (program : FreeM P α) → (n : Nat) →
@@ -683,7 +683,7 @@ theorem forkAt_liftBind_same_succ [DecidableEq P.A] (target : P.A)
       rw [← FreeM.bind_pure_comp, FreeM.bind_assoc]
       rfl]
   simp_rw [Split.completeFork_prependSame]
-  rw [bind_map_right]
+  rw [← map_bind]
 
 theorem forkAt_liftBind_other [DecidableEq P.A] {target a : P.A}
     (hne : a ≠ target) (next : P.B a → FreeM P α) (n : Nat) :
@@ -702,7 +702,7 @@ theorem forkAt_liftBind_other [DecidableEq P.A] {target a : P.A}
       rw [← FreeM.bind_pure_comp, FreeM.bind_assoc]
       rfl]
   simp_rw [Split.completeFork_prependOther]
-  rw [bind_map_right]
+  rw [← map_bind]
 
 
 end PFunctor.FreeM.Cursor

PolyFun/PFunctor/Free/Fold.lean

@@ -65,7 +65,7 @@ theorem foldl_succ (position : P.A) (step : state → Nat → P.B position → s
           readout rounds (step accumulator 0 answer) := by
   rw [foldl, Fin.foldlM_succ]
   simp only [Fin.val_zero]
-  rw [FreeM.monad_bind_def, FreeM.map_bind]
+  rw [FreeM.bind_eq, FreeM.map_bind]
   simp only [FreeM.liftBind_bind, FreeM.pure_bind]
   apply congrArg (fun next => (FreeM.lift position).bind next)
   funext answer
@@ -108,7 +108,7 @@ theorem foldr_succ (position : P.A) (step : state → Nat → P.B position → s
         foldr position step readout rounds (step accumulator rounds answer) := by
   rw [foldr, Fin.foldrM_succ_last]
   simp only [Fin.val_last]
-  rw [FreeM.monad_bind_def, FreeM.map_bind]
+  rw [FreeM.bind_eq, FreeM.map_bind]
   simp only [FreeM.liftBind_bind, FreeM.pure_bind]
   apply congrArg (fun next => (FreeM.lift position).bind next)
   funext answer

PolyFun/PFunctor/Free/Path.lean

@@ -425,7 +425,7 @@ the entire path; this theorem identifies their exact overlap. -/
   induction s with
   | pure x => rfl
   | lift_bind a rest ih =>
-      simp only [monad_bind_def, liftBind_bind]
+      simp only [bind_eq, liftBind_bind]
       exact congrArg (FreeM.liftBind a) (funext ih)
 
 namespace Path

PolyFun/PFunctor/Free/Universal.lean

@@ -156,7 +156,7 @@ theorem foldObjAt_append_split {α : Type uB}
       foldObjAt M l s id >>= fun path =>
         foldObjAt M l (next path) (fun inner => label ⟨path, inner⟩) := by
   unfold foldObjAt
-  rw [decodeAt_append_split, ← FreeM.monad_bind_def, FreeM.liftM_bind]
+  rw [decodeAt_append_split, ← FreeM.bind_eq, FreeM.liftM_bind]
 
 /-- Pointwise container form of multiplication preservation by `foldLens`.
 Both the evaluated position and the reconstructed pair of source paths are

PolyFun/PFunctor/PatternRunsOnMatter/Operational.lean

@@ -102,7 +102,7 @@ theorem runTree_append
       change P.B a × Q.B (M.head matter) at direction
       rw [freeM_bind_map_left,
         ih direction.1 (fun path => next ⟨direction.1, path⟩)
-          (M.children matter direction.2), ← FreeM.bind_map_right]
+          (M.children matter direction.2), FreeM.map_bind]
       apply congrArg (FreeM.bind
         (runTree (rest direction.1) (M.children matter direction.2)))
       funext pulled
@@ -176,7 +176,7 @@ theorem runWithHandler_append [LawfulMonad m]
               (FreeM.Path.append pattern next pulled.1 inner.1,
                 M.Vertex.append pulled.2 inner.2) := by
   unfold runWithHandler
-  rw [runTree_append, ← FreeM.monad_bind_def, FreeM.liftM_bind]
+  rw [runTree_append, ← FreeM.bind_eq, FreeM.liftM_bind]
   apply bind_congr
   intro pulled
   change FreeM.liftM handler

PolyFunTest/Do/LeanOrder.lean

@@ -0,0 +1,34 @@
+/-
+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 ToCslib.Order.LeanOrder
+public import Std.Internal.Do.Order.Basic
+
+/-!
+# Diamond canaries for the order bridge
+
+Core ships its own `Lean.Order.CompleteLattice` instances on `Prop` and on function types in
+`Std.Internal.Do.Order.Basic`; the bridged Mathlib instances of `ToCslib.Order.LeanOrder` must
+compute the same order relation definitionally, so that lemmas stated over either route apply
+to goals stated over the other.
+-/
+
+open Lean.Order
+
+/-- Core's `Prop` instance is implication. -/
+example (p q : Prop) : (p ⊑ q) = (p → q) := rfl
+
+/-- The bridged Mathlib instance on `Prop` is implication too. -/
+example (p q : Prop) : (@PartialOrder.rel Prop instPartialOrderOfMathlib p q) = (p → q) := rfl
+
+/-- Core's function-space instance is the pointwise order. -/
+example (f g : Nat → Prop) : (f ⊑ g) = ∀ n, f n → g n := rfl
+
+/-- The bridged Mathlib instance on functions is the pointwise order too. -/
+example (f g : Nat → Prop) :
+    (@PartialOrder.rel (Nat → Prop) instPartialOrderOfMathlib f g) = ∀ n, f n → g n := rfl

PolyFunTest/ModuleAPI/PFunctor.lean

@@ -73,4 +73,16 @@ example {P : PFunctor.{uA, uB}} {m : Type uB → Type v}
       program.liftM (fun position => hom (handler position)) :=
   FreeM.liftM_natural handler hom program
 
+/-- Lemmas staged in `ToCslib` reach PolyFun consumers through the ordinary re-export. -/
+example {P : PFunctor.{uA, uB}} {α : Type uα} {β : Type uβ} {γ : Type w}
+    (f : β → γ) (x : FreeM P α) (cont : α → FreeM P β) :
+    FreeM.map f (x.bind cont) = x.bind fun a => (cont a).map f :=
+  FreeM.map_bind f x cont
+
+example {P : PFunctor.{uA, uB}} {α : Type uα} {β : Type uβ} (onValue : α → β)
+    (onEffect : (a : P.A) → (P.B a → β) → β) (a : P.A) (cont : P.B a → FreeM P α) :
+    FreeM.foldFreeM onValue onEffect ((FreeM.lift a).bind cont) =
+      onEffect a fun b => FreeM.foldFreeM onValue onEffect (cont b) :=
+  FreeM.foldFreeM_lift_bind onValue onEffect a cont
+
 end PolyFunTest.ModuleAPI.PFunctor