diff --git a/AGENTS.md b/AGENTS.md
index 41281d69..f83dc2b3 100644
--- a/AGENTS.md
+++ b/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,17 +214,21 @@ 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
 
@@ -224,7 +236,8 @@ Structures use UpperCamelCase: `PFunctor`, `TypeTree`, `Decoration`,
 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.
diff --git a/PolyFun/PFunctor/Free/Basic.lean b/PolyFun/PFunctor/Free/Basic.lean
index 4afbe925..52daa6e3 100644
--- a/PolyFun/PFunctor/Free/Basic.lean
+++ b/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
diff --git a/PolyFun/PFunctor/Free/Cursor/Fork.lean b/PolyFun/PFunctor/Free/Cursor/Fork.lean
index 88b3fb2f..f53ce9ab 100644
--- a/PolyFun/PFunctor/Free/Cursor/Fork.lean
+++ b/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]
diff --git a/PolyFun/PFunctor/Free/Cursor/Occurrence.lean b/PolyFun/PFunctor/Free/Cursor/Occurrence.lean
index 72a307b2..2532ecde 100644
--- a/PolyFun/PFunctor/Free/Cursor/Occurrence.lean
+++ b/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
diff --git a/PolyFun/PFunctor/Free/Fold.lean b/PolyFun/PFunctor/Free/Fold.lean
index 8b189e8a..28b8a6f2 100644
--- a/PolyFun/PFunctor/Free/Fold.lean
+++ b/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
diff --git a/PolyFun/PFunctor/Free/Path.lean b/PolyFun/PFunctor/Free/Path.lean
index c8e8eb4f..9c313d6a 100644
--- a/PolyFun/PFunctor/Free/Path.lean
+++ b/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
diff --git a/PolyFun/PFunctor/Free/Universal.lean b/PolyFun/PFunctor/Free/Universal.lean
index 19fe95ed..a60c62a6 100644
--- a/PolyFun/PFunctor/Free/Universal.lean
+++ b/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
diff --git a/PolyFun/PFunctor/PatternRunsOnMatter/Operational.lean b/PolyFun/PFunctor/PatternRunsOnMatter/Operational.lean
index 0d068fcf..14995371 100644
--- a/PolyFun/PFunctor/PatternRunsOnMatter/Operational.lean
+++ b/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
diff --git a/PolyFunTest/Do/LeanOrder.lean b/PolyFunTest/Do/LeanOrder.lean
new file mode 100644
index 00000000..fb148c4f
--- /dev/null
+++ b/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
diff --git a/PolyFunTest/ModuleAPI/PFunctor.lean b/PolyFunTest/ModuleAPI/PFunctor.lean
index 153f82c1..8daea157 100644
--- a/PolyFunTest/ModuleAPI/PFunctor.lean
+++ b/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
diff --git a/PolyFunTest/ToCslib/Free.lean b/PolyFunTest/ToCslib/Free.lean
new file mode 100644
index 00000000..c8520705
--- /dev/null
+++ b/PolyFunTest/ToCslib/Free.lean
@@ -0,0 +1,79 @@
+/-
+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.Data.PFunctor.Free.Loops
+
+/-!
+# Canaries for the staged free-monad API
+
+These examples pin the behaviour of `ToCslib.Data.PFunctor.Free`: the opt-in case principle
+presents nodes in simp normal form, the functor equations fire on constructor-spelled goals
+without disabling `liftBind_eq`, the catamorphism is characterised by its universal property
+(interpretation *is* the fold), and interpretation commutes with list loops.
+-/
+
+public section
+
+open PFunctor
+
+/-- A single-position interface with boolean responses. -/
+abbrev coinP : PFunctor.{0, 0} := ⟨PUnit, fun _ => Bool⟩
+
+/-- `FreeM.cases` produces the `(lift a).bind cont` normal form, on which `simp` continues. -/
+example (x : FreeM coinP Nat) : FreeM.map id x = x := by
+  cases x using FreeM.cases with
+  | pure a => rfl
+  | lift_bind a cont => simp
+
+/-- The functor equation fires on a constructor-spelled goal. -/
+example (f : Nat → Nat) (cont : Bool → FreeM coinP Nat) :
+    FreeM.map f (FreeM.liftBind PUnit.unit cont) =
+      FreeM.liftBind PUnit.unit fun b => FreeM.map f (cont b) := by
+  simp
+
+/-- The fold equations fire under `simp`, in both the `.bind` and the `>>=` spelling. They are
+stated over a generic interface: on a reducible interface such as `coinP` the goal's implicit
+response type `coinP.B a` reduces to `Bool` in `simp`'s index while the lemmas keep the
+projection `P.B a`, so no lemma of this shape (cslib's `liftM_lift_bind` included) fires there;
+see `docs/wiki/gotchas.md`. -/
+example {P : PFunctor.{0, 0}} (onValue : Nat → Nat) (onEffect : (a : P.A) → (P.B a → Nat) → Nat)
+    (a : P.A) (cont : P.B a → FreeM P Nat) :
+    FreeM.foldFreeM onValue onEffect ((FreeM.lift a).bind cont) =
+      onEffect a fun b => FreeM.foldFreeM onValue onEffect (cont b) := by
+  simp
+
+example {P : PFunctor.{0, 0}} (onValue : Nat → Nat) (onEffect : (a : P.A) → (P.B a → Nat) → Nat)
+    (a : P.A) (cont : P.B a → FreeM P Nat) :
+    FreeM.foldFreeM onValue onEffect (FreeM.lift a >>= cont) =
+      onEffect a fun b => FreeM.foldFreeM onValue onEffect (cont b) := by
+  simp
+
+/-- Interpretation through a handler is the fold into the target monad's algebra. -/
+example (s : (a : coinP.A) → Option (coinP.B a)) :
+    (fun x : FreeM coinP Nat => x.liftM s) =
+      FreeM.foldFreeM pure fun a k => s a >>= k :=
+  FreeM.foldFreeM_unique _ _ _ (fun _ => rfl) fun a cont => FreeM.liftM_lift_bind s a cont
+
+/-- Interpretation is natural along any function preserving `pure` and `bind`. -/
+example (s : (a : coinP.A) → Id (coinP.B a)) (x : FreeM coinP Nat) :
+    (fun y : Id Nat => (pure y.run : Option Nat)) (FreeM.liftM s x) =
+      FreeM.liftM (fun a => (pure (s a).run : Option (coinP.B a))) x :=
+  FreeM.map_liftM (m := Id) (n := Option) (fun y => pure y.run) (fun _ => rfl) (fun _ _ => rfl)
+    s x
+
+/-- Interpretation commutes with a `for` loop over a list. -/
+example (s : (a : coinP.A) → Option (coinP.B a)) (l : List Nat) (init : Nat)
+    (f : Nat → Nat → FreeM coinP (ForInStep Nat)) :
+    FreeM.liftM s (forIn l init f) = forIn l init fun a b => FreeM.liftM s (f a b) :=
+  FreeM.liftM_forIn s l init f
+
+/-- Handler fusion. -/
+example (x : FreeM coinP Nat) (first : (a : coinP.A) → FreeM coinP (coinP.B a))
+    (second : (a : coinP.A) → Option (coinP.B a)) :
+    (x.liftM first).liftM second = x.liftM fun a => (first a).liftM second :=
+  FreeM.liftM_comp x first second
diff --git a/PolyFunTest/ToCslib/HomTransport.lean b/PolyFunTest/ToCslib/HomTransport.lean
new file mode 100644
index 00000000..a8e934fc
--- /dev/null
+++ b/PolyFunTest/ToCslib/HomTransport.lean
@@ -0,0 +1,54 @@
+/-
+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.Control.Monad.HomTransport
+public import ToCslib.Control.ForIn
+
+/-!
+# Canaries for loop transport and effect-free containers
+
+The transport lemmas are instantiated at a concrete `pure`/`bind`-preserving function, and the
+`Option` / `Vector` `PureForIn` instances are exercised through the generic container lemma.
+-/
+
+/-- Embedding `Id` into `Option` preserves `pure` and `bind`. -/
+example (l : List Nat) (init : Nat) (f : Nat → Nat → Id (ForInStep Nat)) :
+    (pure (forIn l init f).run : Option Nat) = forIn l init fun a b => pure (f a b).run :=
+  Cslib.map_listForIn (m := Id) (n := Option) (fun x => pure x.run) (fun _ => rfl) (fun _ _ => rfl) l init f
+
+example (l : List Nat) (f : Nat → Id PUnit) :
+    (pure (l.forM f).run : Option PUnit) = l.forM ((fun x => pure x.run) ∘ f) :=
+  Cslib.map_listForM (m := Id) (n := Option) (fun x => pure x.run) (fun _ => rfl) (fun _ _ => rfl) l f
+
+example (f : Nat → Nat → Id Nat) (init : Nat) (l : List Nat) :
+    (pure (l.foldlM f init).run : Option Nat) = l.foldlM (fun s a => pure (f s a).run) init :=
+  Cslib.map_listFoldlM (m := Id) (n := Option) (fun x => pure x.run) (fun _ => rfl) (fun _ _ => rfl) f init l
+
+example (f : Nat → Id Nat) (l : List Nat) :
+    (pure (l.mapM f).run : Option (List Nat)) = l.mapM ((fun x => pure x.run) ∘ f) :=
+  Cslib.map_listMapM (m := Id) (n := Option) (fun x => pure x.run) (fun _ => rfl) (fun _ _ => rfl) f l
+
+/-! ## Effect-free containers -/
+
+example : Std.Internal.PureForIn Id (Option Nat) Nat := inferInstance
+example : Std.Internal.PureForIn' Id (Option Nat) Nat := inferInstance
+example : Std.Internal.PureForIn Id (Vector Nat 3) Nat := inferInstance
+example : Std.Internal.PureForIn' Id (Vector Nat 3) Nat := inferInstance
+
+example (o : Option Nat) : ForIn.toList o = o.toList := by simp
+example (v : Vector Nat 3) : ForIn.toList v = v.toList := by simp
+
+/-- The generic container lemma reaches `Option` through its new instance. -/
+example (o : Option Nat) (init : Nat) (f : Nat → Nat → Id (ForInStep Nat)) :
+    (pure (forIn o init f).run : Option Nat) = forIn o init fun a b => pure (f a b).run :=
+  Cslib.map_forIn_of_pureForIn (m := Id) (n := Option) (fun x => pure x.run) (fun _ => rfl) (fun _ _ => rfl) o init f
+
+/-- … and `Vector` through its array. -/
+example (v : Vector Nat 3) (init : Nat) (f : Nat → Nat → Id (ForInStep Nat)) :
+    (pure (forIn v init f).run : Option Nat) = forIn v init fun a b => pure (f a b).run :=
+  Cslib.map_forIn_of_pureForIn (m := Id) (n := Option) (fun x => pure x.run) (fun _ => rfl) (fun _ _ => rfl) v init f
diff --git a/PolyFunTest/ToCslib/LeanOrder.lean b/PolyFunTest/ToCslib/LeanOrder.lean
new file mode 100644
index 00000000..0bd77201
--- /dev/null
+++ b/PolyFunTest/ToCslib/LeanOrder.lean
@@ -0,0 +1,30 @@
+/-
+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 Mathlib.Data.ENat.Lattice
+public import Mathlib.Data.Set.Lattice
+
+/-!
+# Canaries for the order bridge
+
+Mathlib complete lattices instantiate core's `Lean.Order.CompleteLattice`, the bridged relation
+is Mathlib's `≤` definitionally, and predicate-indexed suprema are `sSup` of the carved-out set.
+-/
+
+open Lean.Order
+
+example : Lean.Order.CompleteLattice (Set Nat) := inferInstance
+noncomputable example : Lean.Order.CompleteLattice ℕ∞ := inferInstance
+noncomputable example : Lean.Order.CompleteLattice (Nat → ℕ∞) := inferInstance
+
+example (a b : Set Nat) : (a ⊑ b) = (a ≤ b) := rfl
+example (a b : ℕ∞) : (a ⊑ b) = (a ≤ b) := rfl
+
+example (c : Set Nat → Prop) : Lean.Order.CompleteLattice.sup c = sSup {x | c x} :=
+  Lean.Order.sup_eq_sSup c
diff --git a/ToCslib.lean b/ToCslib.lean
index ff9ed687..7e95b396 100644
--- a/ToCslib.lean
+++ b/ToCslib.lean
@@ -1,21 +1,13 @@
-/-
-Copyright (c) 2026 PolyFun Contributors. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Devon Tuma, Elias Judin
--/
-
 module
 
 public import ToCslib.Computability.BitEncoding
+public import ToCslib.Computability.PolyTime
+public import ToCslib.Computability.SingleTape.BasicMachines
 public import ToCslib.Computability.SingleTape.Counting
 public import ToCslib.Computability.SingleTape.Snoc
+public import ToCslib.Control.ForIn
+public import ToCslib.Control.Monad.HomTransport
 public import ToCslib.Data.BitVec
-
-/-!
-# Extensions of the pinned cslib machine library
-
-This library contains reusable facts and constructions about cslib machines. It
-does not import PolyFun's realizability theory or any downstream oracle or
-cryptographic semantics. Optional backend libraries may import these modules
-explicitly without making cslib a dependency of generic PolyFun.
--/
+public import ToCslib.Data.PFunctor.Free.Basic
+public import ToCslib.Data.PFunctor.Free.Loops
+public import ToCslib.Order.LeanOrder
diff --git a/ToCslib/Control/ForIn.lean b/ToCslib/Control/ForIn.lean
new file mode 100644
index 00000000..cd22a80d
--- /dev/null
+++ b/ToCslib/Control/ForIn.lean
@@ -0,0 +1,102 @@
+/-
+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 Std.Internal.ForIn
+public import Init.Data.Vector.Lemmas
+
+/-!
+# Effect-free loops over `Option` and `Vector`
+
+Core's `Std.Internal.PureForIn` classes identify the containers whose `for` loop is the loop
+over the list `ForIn.toList` computes, which is what the loop specifications of the
+weakest-precondition layer and the transport of loops along monad morphisms reduce to. Core
+supplies instances for lists, arrays, ranges, slices, and iterators; this file adds `Option`
+(a loop of at most one iteration) and `Vector`, whose loop is its array's.
+-/
+
+public section
+
+universe u v u₁
+
+namespace Std.Internal
+
+/-- Transport a `forIn'` loop along an equation between its lists, re-typing the membership
+proofs of the body. -/
+private theorem forIn'_cast {γ : Type u₁} {δ : Type u} {n : Type u → Type v} [Monad n]
+    {l₁ l₂ : List γ} (h : l₁ = l₂) (init : δ) (f : (a : γ) → a ∈ l₂ → δ → n (ForInStep δ)) :
+    forIn' l₂ init f = forIn' l₁ init fun a ha b => f a (h ▸ ha) b := by
+  subst h; rfl
+
+/-! ## `Option` -/
+
+section Option
+
+variable {α : Type u₁}
+
+@[simp]
+theorem ForIn.toList_option (o : Option α) : ForIn.toList o = o.toList := by
+  apply ForIn.toList_eq_of_forIn_eq
+  intro init f
+  cases o with
+  | none => rfl
+  | some a =>
+    simp only [Option.toList, List.forIn_cons, List.forIn_nil]
+    exact bind_congr fun r => by cases r <;> rfl
+
+instance : LawfulMemForInId (Option α) α where
+  mem_toList_iff {a o} := by cases o <;> simp [Option.toList, eq_comm]
+
+instance {m : Type u → Type v} [Monad m] : PureForIn' m (Option α) α where
+  forIn'_eq o init f := by
+    cases o with
+    | none => rfl
+    | some a =>
+      rw [forIn'_cast (ForIn.toList_option (some a)).symm]
+      simp only [Option.toList, List.forIn'_cons, List.forIn'_nil]
+      exact bind_congr fun r => by cases r <;> rfl
+
+instance {m : Type u → Type v} [Monad m] : PureForIn m (Option α) α where
+  forIn_eq o init f := by
+    cases o with
+    | none => rfl
+    | some a =>
+      simp only [ForIn.toList_option, Option.toList, List.forIn_cons, List.forIn_nil]
+      exact bind_congr fun r => by cases r <;> rfl
+
+end Option
+
+/-! ## `Vector` -/
+
+section Vector
+
+variable {α : Type u₁} {n : Nat}
+
+@[simp]
+theorem ForIn.toList_vector (xs : Vector α n) : ForIn.toList xs = xs.toList := by
+  apply ForIn.toList_eq_of_forIn_eq
+  intro init f
+  cases xs with
+  | mk xs h => rw [Vector.forIn_mk, ← Array.forIn_toList]; rfl
+
+instance : LawfulMemForInId (Vector α n) α where
+  mem_toList_iff {a xs} := by rw [ForIn.toList_vector, Vector.mem_toList_iff]
+
+instance {m : Type u → Type v} [Monad m] : PureForIn' m (Vector α n) α where
+  forIn'_eq xs init f := by
+    cases xs with
+    | mk xs h =>
+      rw [Vector.forIn'_mk, forIn'_cast (l₁ := xs.toList) (ForIn.toList_vector (Vector.mk xs h)).symm,
+        Array.forIn'_toList]
+
+instance {m : Type u → Type v} [Monad m] : PureForIn m (Vector α n) α where
+  forIn_eq xs init f := by
+    cases xs with
+    | mk xs h => rw [Vector.forIn_mk, ← Array.forIn_toList, ForIn.toList_vector]; rfl
+
+end Vector
+
+end Std.Internal
diff --git a/ToCslib/Control/Monad/HomTransport.lean b/ToCslib/Control/Monad/HomTransport.lean
new file mode 100644
index 00000000..13f72126
--- /dev/null
+++ b/ToCslib/Control/Monad/HomTransport.lean
@@ -0,0 +1,123 @@
+/-
+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 Std.Internal.ForIn
+
+/-!
+# Transport of loops along monad morphisms
+
+A function `F : ∀ {β}, m β → n β` that preserves `pure` and `bind` commutes with every loop
+combinator that `do`-notation elaborates to: `forIn'` and `forIn` over lists, `forM`, `foldlM`,
+`mapM`, and `forIn` over any container whose `PureForIn` instance reduces its loop to the list
+`ForIn.toList` computes. The morphism hypotheses are stated inline, so a bundled monad
+homomorphism and cslib's unbundled `IsMonadHom` predicate instantiate the same lemmas.
+
+The list lemmas for `forM`, `foldlM`, and `mapM` follow the shapes of cslib's in-flight
+`IsMonadHom.map_list*` lemmas so that the restatement on that predicate is mechanical; the
+`forIn'` / `forIn` lemmas and the `PureForIn` transport are new.
+-/
+
+public section
+
+universe u v w u₁ w₁
+
+namespace Cslib
+
+variable {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n]
+  (F : ∀ {β : Type u}, m β → n β)
+  (hpure : ∀ {β : Type u} (b : β), F (pure b) = pure b)
+  (hbind : ∀ {β γ : Type u} (x : m β) (g : β → m γ), F (x >>= g) = F x >>= fun b => F (g b))
+
+include hpure hbind
+
+/-! ## Lists -/
+
+-- upstream candidate (complements cslib#856, which covers `mapM`, `forM`, and `foldlM`)
+theorem map_listForIn' {α : Type u₁} {β : Type u} (l : List α) (init : β)
+    (f : (a : α) → a ∈ l → β → m (ForInStep β)) :
+    F (forIn' l init f) = forIn' l init fun a h b => F (f a h b) := by
+  induction l generalizing init with
+  | nil => simp [hpure]
+  | cons a l ih =>
+    simp only [List.forIn'_cons, hbind]
+    congr 1
+    funext r
+    cases r <;> simp [hpure, ih]
+
+theorem map_listForIn {α : Type u₁} {β : Type u} (l : List α) (init : β)
+    (f : α → β → m (ForInStep β)) :
+    F (forIn l init f) = forIn l init fun a b => F (f a b) := by
+  induction l generalizing init with
+  | nil => simp [hpure]
+  | cons a l ih =>
+    simp only [List.forIn_cons, hbind]
+    congr 1
+    funext r
+    cases r <;> simp [hpure, ih]
+
+-- upstream: cslib#856 (`IsMonadHom.map_listForM`)
+theorem map_listForM {α : Type u₁} (l : List α) (f : α → m PUnit) :
+    F (l.forM f) = l.forM (F ∘ f) := by
+  induction l with
+  | nil => simp only [List.forM_eq_forM, List.forM_nil, hpure]
+  | cons a l ih =>
+    simp only [List.forM_eq_forM] at ih ⊢
+    simp only [List.forM_cons, hbind, ih, Function.comp_apply]
+
+-- upstream: cslib#856 (`IsMonadHom.map_listFoldlM`)
+theorem map_listFoldlM {s : Type u} {α : Type u₁} (f : s → α → m s) (init : s) (l : List α) :
+    F (l.foldlM f init) = l.foldlM (fun s a => F (f s a)) init := by
+  induction l generalizing init with
+  | nil => simp [hpure]
+  | cons a l ih => simp [hbind, ih]
+
+-- upstream: cslib#856 (`IsMonadHom.map_listMapM'`)
+theorem map_listMapM' {α : Type u₁} {β : Type u} (f : α → m β) (l : List α) :
+    F (l.mapM' f) = l.mapM' (F ∘ f) := by
+  induction l with
+  | nil => simp [hpure]
+  | cons a l ih => simp [hbind, hpure, ih]
+
+/-- A function preserving `pure` and `bind` preserves `Functor.map`. -/
+theorem map_functorMap [LawfulMonad m] [LawfulMonad n] {β γ : Type u} (g : β → γ) (x : m β) :
+    F (g <$> x) = g <$> F x := by
+  rw [← bind_pure_comp, hbind, ← bind_pure_comp]
+  simp only [hpure]
+
+-- upstream: cslib#856 (`IsMonadHom.map_listMapM`)
+theorem map_listMapM [LawfulMonad m] [LawfulMonad n] {α : Type u₁} {β : Type u}
+    (f : α → m β) (l : List α) :
+    F (l.mapM f) = l.mapM (F ∘ f) := by
+  induction l with
+  | nil => simp only [List.mapM_nil, hpure]
+  | cons a l ih => simp only [List.mapM_cons, hbind, hpure, ih, Function.comp_apply]
+
+/-! ## Containers iterating over a list
+
+`Std.Internal.PureForIn` identifies the containers (arrays, ranges, iterators, …) whose loop is
+the loop over the list `ForIn.toList` computes; transport then reduces to the list case. -/
+
+theorem map_forIn_of_pureForIn {ρ : Type w₁} {α : Type u₁} {β : Type u}
+    [ForIn m ρ α] [ForIn n ρ α] [ForIn Id ρ α]
+    [Std.Internal.PureForIn m ρ α] [Std.Internal.PureForIn n ρ α]
+    (xs : ρ) (init : β) (f : α → β → m (ForInStep β)) :
+    F (forIn xs init f) = forIn xs init fun a b => F (f a b) := by
+  rw [Std.Internal.PureForIn.forIn_eq (m := m) xs init f,
+    Std.Internal.PureForIn.forIn_eq (m := n) xs init]
+  exact map_listForIn F hpure hbind _ init f
+
+theorem map_forIn'_of_pureForIn' {ρ : Type w₁} {α : Type u₁} {β : Type u}
+    {d : Membership α ρ} [ForIn' m ρ α d] [ForIn' n ρ α d] [ForIn Id ρ α]
+    [Std.Internal.LawfulMemForInId ρ α]
+    [Std.Internal.PureForIn' m ρ α] [Std.Internal.PureForIn' n ρ α]
+    (xs : ρ) (init : β) (f : (a : α) → a ∈ xs → β → m (ForInStep β)) :
+    F (forIn' xs init f) = forIn' xs init fun a h b => F (f a h b) := by
+  rw [Std.Internal.PureForIn'.forIn'_eq (m := m) xs init f,
+    Std.Internal.PureForIn'.forIn'_eq (m := n) xs init]
+  exact map_listForIn' F hpure hbind _ init _
+
+end Cslib
diff --git a/ToCslib/Data/PFunctor/Free/Basic.lean b/ToCslib/Data/PFunctor/Free/Basic.lean
new file mode 100644
index 00000000..b0311d46
--- /dev/null
+++ b/ToCslib/Data/PFunctor/Free/Basic.lean
@@ -0,0 +1,174 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Devon Tuma, Quang Dao
+-/
+module
+
+public import Cslib.Foundations.Data.PFunctor.Free
+
+/-!
+# Extensions of the free monad on a polynomial functor
+
+Additions to cslib's `PFunctor.FreeM` API staged for upstreaming: a case-analysis principle in
+the same `(lift a).bind cont` normal form as cslib's induction principle, the functor equations
+`map_pure` / `map_bind` together with their constructor spellings, the catamorphism `foldFreeM`
+with its universal property (the polynomial counterpart of `Cslib.FreeM.foldFreeM`), handler
+fusion `liftM_comp`, the identity fold `liftM_lift_eq_self`, and naturality of `liftM` along any
+function that preserves `pure` and `bind` (`map_liftM`).
+
+Every declaration lives in the upstream namespace `PFunctor.FreeM` and uses no vocabulary beyond
+cslib's. A lemma that duplicates an open cslib pull request carries an `upstream:` comment naming
+it and is deleted when that request lands.
+-/
+
+public section
+
+universe u v w uA uB
+
+namespace PFunctor.FreeM
+
+variable {P : PFunctor.{uA, uB}} {α β γ : Type*}
+
+/-! ## Case analysis in simp normal form -/
+
+/-- Case analysis on a free polynomial tree, presenting the node case as `(lift a).bind cont`:
+the simp normal form that cslib's induction principle `FreeM.induction` also uses, so that
+`cases x using FreeM.cases with | pure a => _ | lift_bind a cont => _` produces goals `simp` can
+continue on without unfolding `liftBind`. -/
+-- upstream: cslib#731 supplies a `cases_eliminator` for the W-type presentation.
+protected def cases {motive : P.FreeM α → Sort u}
+    (pure : ∀ a, motive (pure a))
+    (lift_bind : ∀ (a : P.A) (cont : P.B a → P.FreeM α), motive ((FreeM.lift a).bind cont)) :
+    ∀ x, motive x
+  | .pure a => pure a
+  | .liftBind a cont => lift_bind a cont
+
+/-! ## Bind and functor equations -/
+
+/-- The monad `>>=` of `FreeM` is `FreeM.bind`, pointwise; the function-level form is
+`bind_eq_bind`. -/
+theorem bind_eq {α β : Type v} (x : P.FreeM α) (g : α → P.FreeM β) : x >>= g = x.bind g := rfl
+
+-- upstream: cslib#716
+@[simp]
+theorem map_pure (f : α → β) (x : α) : map f (pure x : P.FreeM α) = pure (f x) := rfl
+
+-- upstream: cslib#716
+@[simp]
+theorem map_bind (f : β → γ) (x : P.FreeM α) (cont : α → P.FreeM β) :
+    map f (x.bind cont) = x.bind fun a => (cont a).map f := by
+  simp_rw [← bind_pure_comp, FreeM.bind_assoc]
+
+/-- Mapping through a node maps every continuation, in constructor spelling. -/
+theorem map_liftBind (f : α → β) (a : P.A) (cont : P.B a → P.FreeM α) :
+    map f (FreeM.liftBind a cont) = FreeM.liftBind a fun b => map f (cont b) :=
+  rfl
+
+/-- Mapping through a node maps every continuation, in simp normal form. -/
+theorem map_lift_bind (f : α → β) (a : P.A) (cont : P.B a → P.FreeM α) :
+    map f ((FreeM.lift a).bind cont) = (FreeM.lift a).bind fun b => map f (cont b) :=
+  rfl
+
+/-! ## The catamorphism
+
+`FreeM P α` is the initial algebra of `β ↦ α ⊕ Σ a, (P.B a → β)`. An algebra is a value handler
+`onValue : α → β` together with a node handler `onEffect : (a : P.A) → (P.B a → β) → β`, and
+`foldFreeM` is the unique algebra morphism out of the free tree. -/
+
+/-- Fold a free polynomial tree into any algebra of its signature. -/
+@[expose]
+def foldFreeM (onValue : α → β) (onEffect : (a : P.A) → (P.B a → β) → β) : P.FreeM α → β
+  | .pure a => onValue a
+  | .liftBind a cont => onEffect a fun b => foldFreeM onValue onEffect (cont b)
+
+@[simp]
+theorem foldFreeM_pure (onValue : α → β) (onEffect : (a : P.A) → (P.B a → β) → β) (a : α) :
+    foldFreeM onValue onEffect (pure a) = onValue a :=
+  rfl
+
+@[simp]
+theorem foldFreeM_lift_bind (onValue : α → β) (onEffect : (a : P.A) → (P.B a → β) → β)
+    (a : P.A) (cont : P.B a → P.FreeM α) :
+    foldFreeM onValue onEffect ((FreeM.lift a).bind cont) =
+      onEffect a fun b => foldFreeM onValue onEffect (cont b) :=
+  rfl
+
+/-- `foldFreeM_lift_bind` with the node spelled through `>>=`, the form `simp` normalizes to
+when the leaf and response types share a universe. -/
+@[simp]
+theorem foldFreeM_lift_bind' {α : Type uB} {β : Type w} (onValue : α → β)
+    (onEffect : (a : P.A) → (P.B a → β) → β) (a : P.A) (cont : P.B a → P.FreeM α) :
+    foldFreeM onValue onEffect (FreeM.lift a >>= cont) =
+      onEffect a fun b => foldFreeM onValue onEffect (cont b) :=
+  rfl
+
+theorem foldFreeM_liftBind (onValue : α → β) (onEffect : (a : P.A) → (P.B a → β) → β)
+    (a : P.A) (cont : P.B a → P.FreeM α) :
+    foldFreeM onValue onEffect (FreeM.liftBind a cont) =
+      onEffect a fun b => foldFreeM onValue onEffect (cont b) :=
+  rfl
+
+@[simp]
+theorem foldFreeM_lift (a : P.A) (onValue : P.B a → β)
+    (onEffect : (a : P.A) → (P.B a → β) → β) :
+    foldFreeM onValue onEffect (FreeM.lift a) = onEffect a onValue :=
+  rfl
+
+/-- **Universal property of the fold**: a function agreeing with the algebra on leaves and on
+nodes is the fold. -/
+theorem foldFreeM_unique (onValue : α → β) (onEffect : (a : P.A) → (P.B a → β) → β)
+    (h : P.FreeM α → β) (h_pure : ∀ a, h (pure a) = onValue a)
+    (h_lift_bind : ∀ (a : P.A) (cont : P.B a → P.FreeM α),
+      h ((FreeM.lift a).bind cont) = onEffect a fun b => h (cont b)) :
+    h = foldFreeM onValue onEffect := by
+  funext x
+  induction x with
+  | pure a => rw [foldFreeM_pure, h_pure]
+  | lift_bind a cont ih => rw [foldFreeM_lift_bind, h_lift_bind]; simp only [ih]
+
+/-! ## Interpretation -/
+
+section liftM
+
+variable {m : Type uB → Type v} [Monad m]
+
+-- upstream: cslib#716
+/-- Folding a free polynomial tree by lifting each operation back into `FreeM` is the identity. -/
+@[simp]
+theorem liftM_lift_eq_self {α : Type uB} (x : P.FreeM α) : FreeM.liftM FreeM.lift x = x := by
+  induction x with
+  | pure _ => simp
+  | lift_bind _ _ ih => simp [ih]
+
+/-- **Naturality of interpretation**: a function `F` between monads that preserves `pure` and
+`bind` commutes with `liftM`, sending the interpretation through `s` to the interpretation
+through `F ∘ s`. The hypotheses are the fields of a monad-morphism predicate, stated inline so
+that both bundled and unbundled morphisms instantiate them. -/
+theorem map_liftM {n : Type uB → Type w} [Monad n]
+    (F : ∀ {β : Type uB}, m β → n β)
+    (hpure : ∀ {β : Type uB} (b : β), F (pure b) = pure b)
+    (hbind : ∀ {β γ : Type uB} (x : m β) (g : β → m γ),
+      F (x >>= g) = F x >>= fun b => F (g b))
+    (s : (a : P.A) → m (P.B a)) {α : Type uB} (x : P.FreeM α) :
+    F (FreeM.liftM s x) = FreeM.liftM (fun a => F (s a)) x := by
+  induction x with
+  | pure a => exact hpure a
+  | lift_bind a cont ih => simp only [bind_eq_bind, FreeM.liftM_lift_bind, hbind, ih]
+
+/-- **Handler fusion**: interpreting into a free monad and then into `m` is interpreting once
+through the pointwise Kleisli composite of the two handlers. -/
+theorem liftM_comp [LawfulMonad m] {Q : PFunctor.{u, uB}} {α : Type uB} (x : P.FreeM α)
+    (first : (a : P.A) → Q.FreeM (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 cont ih =>
+    change ((first a >>= fun b => (cont b).liftM first).liftM second) =
+      (first a).liftM second >>= fun b => (cont b).liftM fun a => (first a).liftM second
+    rw [FreeM.liftM_bind]
+    exact congrArg (fun k => (first a).liftM second >>= k) (funext ih)
+
+end liftM
+
+end PFunctor.FreeM
diff --git a/ToCslib/Data/PFunctor/Free/Loops.lean b/ToCslib/Data/PFunctor/Free/Loops.lean
new file mode 100644
index 00000000..655fa63a
--- /dev/null
+++ b/ToCslib/Data/PFunctor/Free/Loops.lean
@@ -0,0 +1,62 @@
+/-
+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.Data.PFunctor.Free.Basic
+public import ToCslib.Control.Monad.HomTransport
+
+/-!
+# Interpretation commutes with loops
+
+`FreeM.liftM s` preserves `pure` and `bind`, so the transport lemmas of
+`ToCslib.Control.Monad.HomTransport` specialise to it: interpreting a free program that loops
+over a list (or over any `PureForIn` container) is looping over the interpreted bodies.
+-/
+
+public section
+
+universe u v w u₁ w₁ uA uB
+
+namespace PFunctor.FreeM
+
+variable {P : PFunctor.{uA, uB}} {m : Type uB → Type v} [Monad m] [LawfulMonad m]
+  (s : (a : P.A) → m (P.B a))
+
+theorem liftM_forIn' {α : Type u₁} {β : Type uB} (l : List α) (init : β)
+    (f : (a : α) → a ∈ l → β → P.FreeM (ForInStep β)) :
+    FreeM.liftM s (forIn' l init f) = forIn' l init fun a h b => FreeM.liftM s (f a h b) :=
+  Cslib.map_listForIn' (fun x => FreeM.liftM s x) (FreeM.liftM_pure s) (FreeM.liftM_bind s)
+    l init f
+
+theorem liftM_forIn {α : Type u₁} {β : Type uB} (l : List α) (init : β)
+    (f : α → β → P.FreeM (ForInStep β)) :
+    FreeM.liftM s (forIn l init f) = forIn l init fun a b => FreeM.liftM s (f a b) :=
+  Cslib.map_listForIn (fun x => FreeM.liftM s x) (FreeM.liftM_pure s) (FreeM.liftM_bind s)
+    l init f
+
+theorem liftM_forM {α : Type u₁} (l : List α) (f : α → P.FreeM PUnit) :
+    FreeM.liftM s (l.forM f) = l.forM fun a => FreeM.liftM s (f a) :=
+  Cslib.map_listForM (fun x => FreeM.liftM s x) (FreeM.liftM_pure s) (FreeM.liftM_bind s) l f
+
+theorem liftM_foldlM {σ : Type uB} {α : Type u₁} (f : σ → α → P.FreeM σ) (init : σ)
+    (l : List α) :
+    FreeM.liftM s (l.foldlM f init) = l.foldlM (fun acc a => FreeM.liftM s (f acc a)) init :=
+  Cslib.map_listFoldlM (fun x => FreeM.liftM s x) (FreeM.liftM_pure s) (FreeM.liftM_bind s)
+    f init l
+
+theorem liftM_mapM {α : Type u₁} {β : Type uB} (f : α → P.FreeM β) (l : List α) :
+    FreeM.liftM s (l.mapM f) = l.mapM fun a => FreeM.liftM s (f a) :=
+  Cslib.map_listMapM (fun x => FreeM.liftM s x) (FreeM.liftM_pure s) (FreeM.liftM_bind s) f l
+
+theorem liftM_forIn_of_pureForIn {ρ : Type w₁} {α : Type u₁} {β : Type uB}
+    [ForIn (P.FreeM) ρ α] [ForIn m ρ α] [ForIn Id ρ α]
+    [Std.Internal.PureForIn (P.FreeM) ρ α] [Std.Internal.PureForIn m ρ α]
+    (xs : ρ) (init : β) (f : α → β → P.FreeM (ForInStep β)) :
+    FreeM.liftM s (forIn xs init f) = forIn xs init fun a b => FreeM.liftM s (f a b) :=
+  Cslib.map_forIn_of_pureForIn (fun x => FreeM.liftM s x) (FreeM.liftM_pure s)
+    (FreeM.liftM_bind s) xs init f
+
+end PFunctor.FreeM
diff --git a/ToCslib/Order/LeanOrder.lean b/ToCslib/Order/LeanOrder.lean
new file mode 100644
index 00000000..735fabdc
--- /dev/null
+++ b/ToCslib/Order/LeanOrder.lean
@@ -0,0 +1,62 @@
+/-
+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 Init.Internal.Order
+public import Mathlib.Order.CompleteLattice.Basic
+
+/-!
+# Core's order hierarchy from Mathlib's
+
+Core's weakest-precondition stack states assertions over `Lean.Order.CompleteLattice`, a
+lattice class whose order is a bare relation `⊑` and whose suprema are indexed by predicates,
+while Mathlib's program-logic carriers (`Prop`, `ℝ≥0∞`, function lattices) come with Mathlib's
+`CompleteLattice`. The pinned Mathlib has no bridge between the two hierarchies; this file
+supplies it. The instances are low priority so that core's own instances on `Prop` and on
+function types win where both apply; they agree with these definitionally on the order relation,
+and `Lean.Order.CompleteLattice` carries no further data, so the two routes to a lattice
+structure on the same type are propositionally interchangeable.
+-/
+
+public section
+
+namespace Lean.Order
+
+universe u
+
+variable {α : Type u}
+
+/-- Mathlib's `≤` as core's `⊑`. -/
+instance (priority := low) instPartialOrderOfMathlib [_root_.PartialOrder α] :
+    Lean.Order.PartialOrder α where
+  rel := (· ≤ ·)
+  rel_refl := le_refl _
+  rel_trans := le_trans
+  rel_antisymm := le_antisymm
+
+/-- The relation underlying the bridged order is Mathlib's `≤`. -/
+@[simp]
+theorem rel_eq_le [_root_.PartialOrder α] (x y : α) :
+    (@Lean.Order.PartialOrder.rel α instPartialOrderOfMathlib x y) = (x ≤ y) :=
+  rfl
+
+/-- Mathlib's complete lattice as core's, with `sSup` of the set a predicate carves out
+supplying every predicate-indexed supremum. -/
+instance (priority := low) instCompleteLatticeOfMathlib [_root_.CompleteLattice α] :
+    Lean.Order.CompleteLattice α where
+  toPartialOrder := instPartialOrderOfMathlib
+  has_sup c := ⟨sSup {x | c x}, fun _ =>
+    ⟨fun h y hy => le_trans (le_sSup (show y ∈ {x | c x} from hy)) h,
+      fun h => sSup_le fun y hy => h y hy⟩⟩
+
+/-- Core's predicate-indexed supremum is Mathlib's `sSup` of the carved-out set. -/
+theorem sup_eq_sSup [_root_.CompleteLattice α] (c : α → Prop) :
+    Lean.Order.CompleteLattice.sup c = sSup {x | c x} :=
+  is_sup_unique (CompleteLattice.sup_spec c) fun _ =>
+    ⟨fun h y hy => le_trans (le_sSup (show y ∈ {x | c x} from hy)) h,
+      fun h => sSup_le fun y hy => h y hy⟩
+
+end Lean.Order
diff --git a/docs/reading/upstream-alignment.md b/docs/reading/upstream-alignment.md
index 6bb1c015..6f5bd01c 100644
--- a/docs/reading/upstream-alignment.md
+++ b/docs/reading/upstream-alignment.md
@@ -194,7 +194,25 @@ should cite it alongside `LawfulMonadLift(T)` and Batteries' `LawfulAlternativeL
 ### Upstream — belongs elsewhere, PolyFun is the wrong home
 
 cslib is already PolyFun's upstreaming channel: the `PFunctor` basic API is being moved
-there, and cslib's `PFunctor.FreeM` is the free monad PolyFun builds on.
+there, and cslib's `PFunctor.FreeM` is the free monad PolyFun builds on. Material bound for
+cslib is staged in the `ToCslib/` library (see `docs/wiki/module-api.md`), which PolyFun imports
+as its lowest layer:
+
+| `ToCslib` module | Contents | Upstream target |
+|---|---|---|
+| `Data/PFunctor/Free/Basic.lean` | `map_pure`, `map_bind`, `liftM_lift_eq_self` | cslib#716 (open) |
+| `Data/PFunctor/Free/Basic.lean` | normal-form case principle `FreeM.cases` | cslib#731 (open) supplies a `cases_eliminator` |
+| `Data/PFunctor/Free/Basic.lean` | `bind_eq`, `map_liftBind`, `map_lift_bind`, `foldFreeM` + `foldFreeM_unique`, `liftM_comp`, `map_liftM` | new cslib PR |
+| `Data/PFunctor/Free/Loops.lean` | `liftM_forIn'` … `liftM_mapM` | new cslib PR |
+| `Control/Monad/HomTransport.lean` | hypothesis-form `map_listForM` / `map_listFoldlM` / `map_listMapM` | cslib#856 (open, as `IsMonadHom.map_list*`) |
+| `Control/Monad/HomTransport.lean` | `map_listForIn'`, `map_listForIn`, `map_forIn_of_pureForIn`, `map_functorMap` | new cslib PR alongside #856 |
+| `Control/ForIn.lean` | `PureForIn` / `PureForIn'` / `LawfulMemForInId` for `Option`, `Vector` | Lean core (`Std.Internal.ForIn`) |
+| `Order/LeanOrder.lean` | Mathlib `CompleteLattice` → `Lean.Order.CompleteLattice` | Mathlib or cslib |
+
+Not stageable downstream: the `liftBind` / `(lift a).bind` normal-form tax behind the seven
+`attribute [local implicit_reducible] PFunctor.FreeM.bind` sites needs `@[implicit_reducible]`
+at the definition in cslib, because Lean rejects global and `scoped` reducibility attributes on
+imported declarations (`Lean/ReducibilityAttrs.lean`). It rides on cslib#716 or #731.
 
 - **cslib**: delay bisimulation over `LTS` (see above). Also
   `Cslib.LTS.Bisimilarity.symm`, which is stated for a single state type while its
diff --git a/docs/wiki/generated-files.md b/docs/wiki/generated-files.md
index 172b9898..c3833fb5 100644
--- a/docs/wiki/generated-files.md
+++ b/docs/wiki/generated-files.md
@@ -6,12 +6,14 @@ Edit the source of truth, not the output.
 | --- | --- | --- | --- |
 | `CLAUDE.md` | compatibility symlink | No | Edit `AGENTS.md` |
 | `PolyFun.lean` | generated module with umbrella public imports | No | `./scripts/update-lib.sh` or `./scripts/check-imports.sh` |
+| `ToCslib.lean` | generated umbrella for the staging library | No | `./scripts/update-lib.sh ToCslib` or `./scripts/check-imports.sh` |
 | `.lake/` | build artifacts and cache | No | `lake build`, `lake exe cache get` |
 | `lake-manifest.json` | resolved dependency lockfile | Manual edits unsafe | Update `lean-toolchain` and both dependency pins in `lakefile.toml`, then run `lake update` |
 
 ## Important Notes
 
-- `./scripts/update-lib.sh` only uses tracked `PolyFun/**/*.lean` files and
+- `./scripts/update-lib.sh [ToCslib]` only uses tracked `PolyFun/**/*.lean` (or
+  `ToCslib/**/*.lean`) files and
   fails fast if untracked Lean files would be skipped. Stage new files
   first, then rerun. It emits a `module` command followed by sorted
   `public import` commands so importing `PolyFun` re-exports the library API.
diff --git a/docs/wiki/gotchas.md b/docs/wiki/gotchas.md
index b61f9ad3..884cfb78 100644
--- a/docs/wiki/gotchas.md
+++ b/docs/wiki/gotchas.md
@@ -288,6 +288,17 @@ path. Foundational citations live in
 those keys (`Hancock-Setzer`, `Spivak-Niu`, etc.) rather than copying
 prose.
 
+### 11a. `simp` lemmas over `FreeM` do not fire on reducible interfaces
+
+A lemma such as `PFunctor.FreeM.liftM_lift_bind` or `foldFreeM_lift_bind'` has the implicit
+response type `P.B a` inside its left-hand side (as the type argument of `>>=`), and `simp`'s
+discrimination tree indexes that argument as the projection `PFunctor.B`. On an interface declared
+with `abbrev` — `abbrev coinP : PFunctor := ⟨PUnit, fun _ => Bool⟩` — the goal's `coinP.B a`
+reduces to `Bool` while the tree is built, so the lemma is never retrieved and `simp` reports it
+unused; the same statement over a `def` interface, or over a generic `P`, matches. `rw` is
+unaffected. State canaries and downstream lemmas over a generic or `def`-declared interface, or
+rewrite explicitly, rather than "fixing" the lemma.
+
 ### 12. `Std.Do` imports are quarantined
 
 Only `PolyFun/Control/Do/Basic.lean`, `PolyFun/PFunctor/Free/Do.lean`, and
diff --git a/docs/wiki/module-api.md b/docs/wiki/module-api.md
index b6598778..093f3f70 100644
--- a/docs/wiki/module-api.md
+++ b/docs/wiki/module-api.md
@@ -85,3 +85,25 @@ A theorem belongs in PolyFun only when its statement can avoid `OracleSpec`,
 probability, and cryptographic policy; otherwise route it one dependency level
 at a time (VCVio candidates stay in VCVio), so "upstreamable" does not
 collapse everything to the lowest dependency.
+
+## The `ToCslib` staging layer
+
+`ToCslib/` is the lowest production library. It holds what PolyFun intends to upstream, written
+so that the upstream pull request is a move rather than a rewrite:
+
+- every declaration lives in the namespace it will have upstream (`PFunctor.FreeM`, `Cslib`,
+  `Lean.Order`, `Std.Internal`), so cslib's `topNamespace` linter and downstream call sites do
+  not change when it lands;
+- a lemma that duplicates an open upstream pull request carries an `-- upstream:` comment
+  naming it (for example `cslib#716`, `cslib#856`) and copies that request's statement shape;
+  it is deleted when the request lands and the pin moves;
+- a lemma with no upstream twin yet is marked `-- upstream candidate`;
+- `ToCslib` imports core, cslib, and Mathlib only — never PolyFun, and never `Std.Do`,
+  `Std.Internal.Do`, or `Std.Tactic.Do` (`scripts/check-modules.sh` enforces this);
+- PolyFun modules import `ToCslib` modules directly (`public import`) and keep no local copy of
+  a lemma that lives there; ordinary-import canaries for the moved lemmas stay in
+  `PolyFunTest/ModuleAPI/`, and behavioural canaries in `PolyFunTest/ToCslib/`;
+- headers say `PolyFun Contributors` here and are rewritten to the individual authors at
+  upstream pull-request time, when the file also gains `import Cslib.Init` and a
+  `CslibTests/` entry.
+
diff --git a/docs/wiki/pfunctor.md b/docs/wiki/pfunctor.md
index 4a5a5a07..a37bd1db 100644
--- a/docs/wiki/pfunctor.md
+++ b/docs/wiki/pfunctor.md
@@ -203,10 +203,17 @@ supplies the inductive type (constructors `pure` / `liftBind`), the `bind` / `ma
 / `Monad` / `LawfulMonad` / `MonadLift` instances, the `@[induction_eliminator]
 induction` principle (non-pure case `lift_bind`), the shape lift `lift : P.A →
 FreeM (P.B a)` and object lift `liftObj : P.Obj α → FreeM α`, and the `liftM`
-interpreter with its `Interprets` universal property. PolyFun layers its own API
-(`mapLens`, `liftM` monad-hom and naturality lemmas, `toW` / `equivWOfIsEmpty`, paths,
-displayed families, indexed-family packing, weakest preconditions, roll bounds)
-on top of the upstream type.
+interpreter with its `Interprets` universal property. Between cslib and PolyFun sits
+`ToCslib/Data/PFunctor/Free/`, the staging area for cslib-bound additions: the
+opt-in normal-form case principle `FreeM.cases`, `map_pure` / `map_bind` and their
+constructor spellings, `bind_eq`, the catamorphism `foldFreeM` with `foldFreeM_unique`,
+handler fusion `liftM_comp`, the identity fold `liftM_lift_eq_self`, naturality
+`map_liftM` along any `pure`/`bind`-preserving function, and commutation of `liftM`
+with list loops (`liftM_forIn'`, `liftM_forM`, `liftM_foldlM`, `liftM_mapM`).
+`PolyFun.PFunctor.Free.Basic` re-exports it and layers PolyFun's own API
+(`mapLens`, the bundled `liftMHom` monad-hom and its universal property,
+`toW` / `equivWOfIsEmpty`, paths, displayed families, indexed-family packing,
+weakest preconditions, roll bounds) on top.
 
 | File | Purpose |
 |------|---------|
diff --git a/docs/wiki/quickstart.md b/docs/wiki/quickstart.md
index 3665aa62..07b99978 100644
--- a/docs/wiki/quickstart.md
+++ b/docs/wiki/quickstart.md
@@ -48,7 +48,8 @@ git add path/to/newfile.lean
 ```
 
 `./scripts/update-lib.sh` only considers tracked files, and fails fast if
-untracked `PolyFun/**/*.lean` files are present.
+untracked `PolyFun/**/*.lean` files are present; `./scripts/update-lib.sh ToCslib`
+does the same for the staging library's umbrella `ToCslib.lean`.
 
 ### Lean-heavy refactors or cleanup
 
@@ -84,10 +85,11 @@ python3 ./scripts/test-docs-integrity.py
 python3 ./scripts/check-docs-integrity.py
 ```
 
-If you specifically need to regenerate `PolyFun.lean`, use:
+If you specifically need to regenerate `PolyFun.lean` or `ToCslib.lean`, use:
 
 ```bash
 ./scripts/update-lib.sh
+./scripts/update-lib.sh ToCslib
 ```
 
 To run the environment linters or the test library on their own:
diff --git a/docs/wiki/repo-map.md b/docs/wiki/repo-map.md
index a308a48e..644d3014 100644
--- a/docs/wiki/repo-map.md
+++ b/docs/wiki/repo-map.md
@@ -33,8 +33,12 @@ PolyFun/
                      quarantine root (Do/Basic)
   Logic/             small logic helpers (HEq)
 
-ToCslib/             separate low-level extensions to the pinned cslib machine
-                     API; imports cslib and Mathlib, never PolyFun
+ToCslib/             lowest production layer, staging what PolyFun upstreams:
+                     cslib machine-API extensions (Computability/), free-monad
+                     additions (Data/PFunctor/Free/), loop transport and
+                     effect-free loop instances (Control/), and the Mathlib →
+                     core order bridge (Order/); imports core, cslib and
+                     Mathlib, never PolyFun or Std.Do
 
 docs/wiki/           agent-facing notes (this directory)
 scripts/             repo utilities (validate, lint, update-lib, port helpers)
@@ -46,14 +50,17 @@ scripts/             repo utilities (validate, lint, update-lib, port helpers)
 Imports flow strictly downward, cycles are a build error. The DAG is also
 recorded in [`AGENTS.md`](../../AGENTS.md):
 
-`ToCslib` is a separate lower library rather than part of this DAG:
+`ToCslib` is the lowest layer of this DAG:
 
 ```text
-Cslib + Mathlib -> ToCslib -> optional PolyFun backend adapters
+Cslib + Mathlib + core Std.Internal -> ToCslib -> PolyFun
 ```
 
-It contains concrete machine constructions and lemmas, but no realizability,
-oracle, probability, or cryptographic policy.
+`PolyFun/PFunctor/Free/Basic.lean` imports `ToCslib.Data.PFunctor.Free.Basic`
+and backend adapters import the machine modules; `ToCslib.Order.LeanOrder`
+is where the program-logic kernel picks up core's order hierarchy. `ToCslib` contains staged upstream
+material only: no realizability, oracle, probability, or cryptographic policy,
+and no `Std.Do` / `Std.Internal.Do` imports.
 
 ```text
 PFunctor/{Basic, Bound, M, Equiv, Chart, Lens}
diff --git a/scripts/check-docs-integrity.py b/scripts/check-docs-integrity.py
index 7108ac3a..47264c32 100755
--- a/scripts/check-docs-integrity.py
+++ b/scripts/check-docs-integrity.py
@@ -167,7 +167,7 @@ def has_module_docstring(text: str) -> bool:
 
 def check_module_docstrings() -> list[str]:
     errors: list[str] = []
-    for source_root in (REPO_ROOT / "PolyFun", REPO_ROOT / "PolyFunTest"):
+    for source_root in (REPO_ROOT / "PolyFun", REPO_ROOT / "ToCslib", REPO_ROOT / "PolyFunTest"):
         for lean_file in source_root.rglob("*.lean"):
             if not has_module_docstring(lean_file.read_text()):
                 rel_path = lean_file.relative_to(REPO_ROOT)
diff --git a/scripts/check-imports.sh b/scripts/check-imports.sh
index 1bd75aeb..89273089 100755
--- a/scripts/check-imports.sh
+++ b/scripts/check-imports.sh
@@ -1,34 +1,35 @@
 #!/usr/bin/env bash
 
-# Check whether PolyFun.lean matches the tracked PolyFun/**/*.lean file set.
+# Check whether each umbrella module (PolyFun.lean, ToCslib.lean) matches the
+# tracked <Lib>/**/*.lean file set.
 
 set -euo pipefail
 
 REPO_ROOT="$(git rev-parse --show-toplevel)"
 cd "$REPO_ROOT"
 
-echo "Checking if all imports are up to date..."
+status=0
 
-backup_file="$(mktemp "${TMPDIR:-/tmp}/PolyFun.lean.backup.XXXXXX")"
-cp PolyFun.lean "$backup_file"
+for lib in PolyFun ToCslib; do
+  echo "Checking if all $lib imports are up to date..."
 
-restore_original() {
-  if [[ -f "$backup_file" ]]; then
-    mv "$backup_file" PolyFun.lean
+  backup_file="$(mktemp "${TMPDIR:-/tmp}/$lib.lean.backup.XXXXXX")"
+  cp "$lib.lean" "$backup_file"
+
+  ./scripts/update-lib.sh "$lib"
+
+  if cmp -s "$backup_file" "$lib.lean"; then
+    echo "✓ All $lib imports are up to date!"
+  else
+    echo "❌ $lib.lean is out of date!"
+    echo "Differences found:"
+    diff -u "$backup_file" "$lib.lean" || true
+    echo ""
+    echo "To fix this, run: ./scripts/update-lib.sh $lib"
+    status=1
   fi
-}
-trap restore_original EXIT
-
-./scripts/update-lib.sh
-
-if cmp -s "$backup_file" PolyFun.lean; then
-  echo "✓ All imports are up to date!"
-  exit 0
-fi
-
-echo "❌ Import file is out of date!"
-echo "Differences found:"
-diff -u "$backup_file" PolyFun.lean || true
-echo ""
-echo "To fix this, run: ./scripts/update-lib.sh"
-exit 1
+
+  mv "$backup_file" "$lib.lean"
+done
+
+exit "$status"
diff --git a/scripts/check-modules.sh b/scripts/check-modules.sh
index 11f8e062..5b494e3e 100755
--- a/scripts/check-modules.sh
+++ b/scripts/check-modules.sh
@@ -9,12 +9,16 @@ cd "$REPO_ROOT"
 
 status=0
 
+lean_sources() {
+  git ls-files -- 'PolyFun.lean' 'PolyFun/*.lean' 'ToCslib.lean' 'ToCslib/*.lean' 'PolyFunTest/*.lean'
+}
+
 while IFS= read -r file; do
   if ! grep -qx 'module' "$file"; then
     echo "ERROR: $file does not enable module mode with a 'module' command." >&2
     status=1
   fi
-done < <(git ls-files -- 'PolyFun.lean' 'PolyFun/*.lean' 'PolyFunTest/*.lean')
+done < <(lean_sources)
 
 while IFS= read -r file; do
   if ! grep -qx 'public section' "$file"; then
@@ -24,18 +28,35 @@ while IFS= read -r file; do
 done < <(git ls-files -- 'PolyFun/Interaction/*.lean')
 
 # The `Std.Do` quarantine (AGENTS.md gotcha 8, docs/wiki/program-logic.md): core's
-# weakest-precondition / `mvcgen` / `vcgen` API moves fast, so only the bridge modules may depend
-# on it. The fence covers both stacks core ships, `Std.Do` and `Std.Internal.Do`, and the tactic
-# layer `Std.Tactic.Do`. Everything the bridge modules export is a construction, never a global
-# instance.
-std_do_allowed() {
+# weakest-precondition API moves fast, so it is fenced in two tiers.
+#
+# * Definitions (`Std.Do` and `Std.Internal.Do`: `WP`, `WPMonad`, `Triple`, spec lemmas) may be
+#   imported by the program-logic kernel — `PolyFun/Control/Monad/`, `PolyFun/Control/Do/`,
+#   `PolyFun/PFunctor/Free/`, `PolyFun/ITree/Do.lean` — and by the `PolyFunTest/Do/` tests.
+# * Tactics (`Std.Tactic.Do`: `mvcgen`, `vcgen`, and the `@[spec]` attribute syntax) stay in
+#   `PolyFun/Control/Do/`, `PolyFun/PFunctor/Free/Do.lean`, and `PolyFunTest/Do/`.
+#
+# `ToCslib/` stages material for cslib, which uses neither stack, so it may import none of it.
+# Everything the fenced modules export is a construction or a scoped instance, never a global
+# `WP` instance.
+std_do_def_allowed() {
+  case "$1" in
+    PolyFun/Control/Monad/*|PolyFun/Control/Do/*|PolyFun/PFunctor/Free/*|PolyFun/ITree/Do.lean|PolyFunTest/Do/*)
+      return 0 ;;
+    *) return 1 ;;
+  esac
+}
+
+std_do_tactic_allowed() {
   case "$1" in
-    PolyFun/Control/Do/Basic.lean|PolyFun/PFunctor/Free/Do.lean|PolyFunTest/Do/*) return 0 ;;
+    PolyFun/Control/Do/*|PolyFun/PFunctor/Free/Do.lean|PolyFunTest/Do/*) return 0 ;;
     *) return 1 ;;
   esac
 }
 
-std_do_import_pattern='^[[:space:]]*(public[[:space:]]+)?(meta[[:space:]]+)?import([[:space:]]+all)?[[:space:]]+Std\.((Tactic|Internal)\.)?Do([[:space:]]*$|\.)'
+import_prefix='^[[:space:]]*(public[[:space:]]+)?(meta[[:space:]]+)?import([[:space:]]+all)?[[:space:]]+'
+std_do_def_pattern="${import_prefix}Std\.(Internal\.)?Do([[:space:]]*$|\.)"
+std_do_tactic_pattern="${import_prefix}Std\.Tactic\.Do([[:space:]]*$|\.)"
 
 # Keep every supported import modifier covered: otherwise a valid Lean import form can bypass
 # the quarantine while the repository's existing files still leave this check green.
@@ -43,29 +64,57 @@ for std_do_import in \
     'import Std.Do' \
     'import Std.Internal.Do' \
     'public import Std.Internal.Do.WP.Basic' \
+    'import all Std.Do.Triple' \
+    'public import all Std.Do' \
+    'meta import Std.Do' \
+    'public meta import Std.Internal.Do' \
+    'meta import all Std.Do' \
+    'public meta import all Std.Do'; do
+  if ! grep -qE "$std_do_def_pattern" <<< "$std_do_import"; then
+    echo "ERROR: Std.Do definition matcher does not recognize: $std_do_import" >&2
+    status=1
+  fi
+done
+
+for std_do_import in \
     'public import Std.Tactic.Do' \
+    'import Std.Tactic.Do.Syntax' \
     'import all Std.Tactic.Do' \
     'public import all Std.Tactic.Do' \
     'meta import Std.Tactic.Do' \
     'public meta import Std.Tactic.Do' \
     'meta import all Std.Tactic.Do' \
     'public meta import all Std.Tactic.Do'; do
-  if ! grep -qE "$std_do_import_pattern" <<< "$std_do_import"; then
-    echo "ERROR: Std.Do import matcher does not recognize: $std_do_import" >&2
+  if ! grep -qE "$std_do_tactic_pattern" <<< "$std_do_import"; then
+    echo "ERROR: Std.Tactic.Do matcher does not recognize: $std_do_import" >&2
     status=1
   fi
 done
 
+if grep -qE "$std_do_def_pattern" <<< 'import Std.Tactic.Do'; then
+  echo "ERROR: Std.Do definition matcher must not classify tactic imports." >&2
+  status=1
+fi
+if grep -qE "$std_do_tactic_pattern" <<< 'import Std.Internal.Do'; then
+  echo "ERROR: Std.Tactic.Do matcher must not classify definition imports." >&2
+  status=1
+fi
+
 while IFS= read -r file; do
-  if grep -qE "$std_do_import_pattern" "$file"; then
-    if ! std_do_allowed "$file"; then
-      echo "ERROR: $file imports core Std.Do / Std.Internal.Do outside the quarantine." >&2
-      echo "Only PolyFun/Control/Do/Basic.lean, PolyFun/PFunctor/Free/Do.lean, and" >&2
-      echo "PolyFunTest/Do/ may depend on it. See AGENTS.md gotcha 8." >&2
-      status=1
-    fi
+  if grep -qE "$std_do_def_pattern" "$file" && ! std_do_def_allowed "$file"; then
+    echo "ERROR: $file imports core Std.Do / Std.Internal.Do outside the quarantine." >&2
+    echo "Only the program-logic kernel (PolyFun/Control/Monad/, PolyFun/Control/Do/," >&2
+    echo "PolyFun/PFunctor/Free/, PolyFun/ITree/Do.lean) and PolyFunTest/Do/ may depend on" >&2
+    echo "it. See AGENTS.md gotcha 8." >&2
+    status=1
+  fi
+  if grep -qE "$std_do_tactic_pattern" "$file" && ! std_do_tactic_allowed "$file"; then
+    echo "ERROR: $file imports core Std.Tactic.Do outside the quarantine." >&2
+    echo "Only PolyFun/Control/Do/, PolyFun/PFunctor/Free/Do.lean, and PolyFunTest/Do/ may" >&2
+    echo "depend on it. See AGENTS.md gotcha 8." >&2
+    status=1
   fi
-done < <(git ls-files -- 'PolyFun.lean' 'PolyFun/*.lean' 'PolyFunTest/*.lean')
+done < <(lean_sources)
 
 if grep -rEn --include='*.lean' '@\[expose\][[:space:]]+public section' PolyFun/Interaction; then
   echo "ERROR: Broad exposed public sections are forbidden in PolyFun/Interaction." >&2
diff --git a/scripts/update-lib.sh b/scripts/update-lib.sh
index ccc8d9c2..5de18b3d 100755
--- a/scripts/update-lib.sh
+++ b/scripts/update-lib.sh
@@ -1,7 +1,11 @@
 #!/usr/bin/env bash
 
-# Update PolyFun.lean with all public imports.
-# This script only considers tracked files. New PolyFun/**/*.lean files
+# Update a library's umbrella module with all public imports.
+#
+#   ./scripts/update-lib.sh            # regenerates PolyFun.lean
+#   ./scripts/update-lib.sh ToCslib    # regenerates ToCslib.lean
+#
+# This script only considers tracked files. New <Lib>/**/*.lean files
 # must be staged first.
 
 set -euo pipefail
@@ -9,7 +13,16 @@ set -euo pipefail
 REPO_ROOT="$(git rev-parse --show-toplevel)"
 cd "$REPO_ROOT"
 
-if [[ ! -d "PolyFun" || ! -f "PolyFun.lean" ]]; then
+lib="${1:-PolyFun}"
+case "$lib" in
+  PolyFun|ToCslib) ;;
+  *)
+    echo "ERROR: unknown library '$lib' (expected PolyFun or ToCslib)." >&2
+    exit 1
+    ;;
+esac
+
+if [[ ! -d "$lib" || ! -f "$lib.lean" ]]; then
   echo "ERROR: Run this script from inside the PolyFun repository." >&2
   exit 1
 fi
@@ -19,16 +32,16 @@ while IFS= read -r file; do
   if [[ -n "$file" ]]; then
     untracked_lean_files+=("$file")
   fi
-done < <(git ls-files --others --exclude-standard -- 'PolyFun/*.lean')
+done < <(git ls-files --others --exclude-standard -- "$lib/*.lean")
 
 if (( ${#untracked_lean_files[@]} > 0 )); then
-  echo "ERROR: Untracked Lean files under PolyFun/ are not included in PolyFun.lean generation." >&2
+  echo "ERROR: Untracked Lean files under $lib/ are not included in $lib.lean generation." >&2
   echo "Stage them first, then rerun this script:" >&2
   printf '  git add %q\n' "${untracked_lean_files[@]}" >&2
   exit 1
 fi
 
-echo "Updating PolyFun.lean with all tracked imports..."
+echo "Updating $lib.lean with all tracked imports..."
 
 tmp_file="$(mktemp "${TMPDIR:-/tmp}/polyfun-imports.XXXXXX")"
 cleanup() {
@@ -39,13 +52,13 @@ trap cleanup EXIT
 {
   echo "module"
   echo ""
-  git ls-files -- 'PolyFun/*.lean' \
+  git ls-files -- "$lib/*.lean" \
     | LC_ALL=C sort \
     | sed 's/\.lean//;s,/,.,g;s/^/public import /'
 } > "$tmp_file"
 
-mv "$tmp_file" PolyFun.lean
+mv "$tmp_file" "$lib.lean"
 trap - EXIT
 
-import_count="$(grep -c '^public import ' PolyFun.lean)"
-echo "✓ PolyFun.lean updated with $import_count public imports"
+import_count="$(grep -c '^public import ' "$lib.lean")"
+echo "✓ $lib.lean updated with $import_count public imports"