diff --git a/differential/src/bin/zipper_bug_repros.rs b/differential/src/bin/zipper_bug_repros.rs
index c7a0dbe4..2275f609 100644
--- a/differential/src/bin/zipper_bug_repros.rs
+++ b/differential/src/bin/zipper_bug_repros.rs
@@ -38,7 +38,7 @@ const CASES: &[(&str, &str)] = &[
     ("root_escape", "a read zipper whose root does not exist walks out of its own root"),
     ("insert_prefix_empty", "insert_prefix(b\"\") destroys the subtrie instead of doing nothing"),
     ("drop_head_zero", "join_k_path_into(0) destroys the subtrie instead of doing nothing"),
-    ("prune_reach", "prune_path's depth and reported byte count depend on internal node layout"),
+    ("prune_reach", "historical prune_path root-boundary bug (fixed in current pathmap)"),
     ("empty_node_leak", "remove_branches / take_map report on node materialisation, not trie state"),
     ("ascend_until_wz", "ascend_until corrupts a write zipper rooted at a node boundary"),
     ("to_next_k_path_borrowed", "to_next_k_path underflows path_len on a borrowed-path zipper"),
@@ -200,10 +200,8 @@ fn run(name: &str) {
             println!("  join_k_path_into(0)->{r}; after: {}   <-- expected unchanged", vals(&map));
         }
 
-        // `prune_path` is documented not to prune above the zipper's root, and to
-        // return the number of bytes removed.  It does prune above the root, and
-        // the count it returns switches between absolute and relative depending
-        // on where the internal node holding the focus begins.
+        // Historical reproducer: the current implementation stays within the
+        // zipper root and returns the relative number of bytes removed.
         "prune_reach" => {
             for len in [8usize, 100] {
                 for rootlen in [0usize, 5] {
diff --git a/differential/src/harness.rs b/differential/src/harness.rs
index 3ac19648..e822db99 100644
--- a/differential/src/harness.rs
+++ b/differential/src/harness.rs
@@ -151,8 +151,6 @@ pub fn fingerprint<Z: ZipperMoving + ZipperPath + ZipperValues<u64> + ZipperAbso
 /// * `skip:empty-focus` — the focus has nothing below it, where the op's
 ///   behaviour is a function of node materialisation rather than trie state.
 /// * `skip:empty-path` — `insert_prefix("")`, which destroys the subtrie.
-/// * `skip:off-root-prune` — a prune on a write zipper not rooted at the map
-///   root, where the depth pruned is a function of internal node layout.
 /// * `skip:quarantined` — the op is disabled outright (op 54).
 ///
 /// Each is recorded in lean/FINDINGS.md and commented at its site.
@@ -161,7 +159,6 @@ pub const SKIP_AT_ROOT: &str = "skip:at-root";
 pub const SKIP_K0: &str = "skip:k0";
 pub const SKIP_EMPTY_FOCUS: &str = "skip:empty-focus";
 pub const SKIP_EMPTY_PATH: &str = "skip:empty-path";
-pub const SKIP_OFF_ROOT_PRUNE: &str = "skip:off-root-prune";
 pub const SKIP_QUARANTINED: &str = "skip:quarantined";
 
 /// Does the focus have no descendants at all?
@@ -465,14 +462,8 @@ pub fn run_ops<R: ReadSource>(
     {
         let mut wz = map0.write_zipper_at_path(root0);
         let mut step = 0usize;
-        // Explicit pruning is only well-defined for a zipper at the map root;
-        // off it the depth pruned depends on internal node layout.
-        let pruneable = root0.is_empty();
-        // The `prune` flag on the other operations is passed straight to
-        // `node_remove_*`, which prunes within the node even when it finds
-        // nothing and reports `None` -- so its effect is a function of node
-        // layout, not of the trie.  Always false.  See lean/FINDINGS.md #7.
-        let no_prune = false;
+        // Run pruning at every zipper root so layout-dependent defects remain
+        // visible to the differential comparison.
 
         macro_rules! get {
             ($e:expr) => {
@@ -676,40 +667,28 @@ pub fn run_ops<R: ReadSource>(
                     ("set_val", show_val(wz.set_val(v).as_ref()))
                 }
                 28 => {
-                    let _pr = get!(d.boolean()); // decoded for stream alignment; see `no_prune`
-                    ("remove_val", show_val(wz.remove_val(no_prune).as_ref()))
+                    let pr = get!(d.boolean());
+                    ("remove_val", show_val(wz.remove_val(pr).as_ref()))
                 }
                 29 => ("create_path", show_bool(wz.create_path()).to_string()),
-                30 => {
-                    if pruneable {
-                        ("prune_path", format!("{}", wz.prune_path()))
-                    } else {
-                        ("prune_path", SKIP_OFF_ROOT_PRUNE.to_string())
-                    }
-                }
-                31 => {
-                    if pruneable {
-                        ("prune_ascend", format!("{}", wz.prune_ascend()))
-                    } else {
-                        ("prune_ascend", SKIP_OFF_ROOT_PRUNE.to_string())
-                    }
-                }
+                30 => ("prune_path", format!("{}", wz.prune_path())),
+                31 => ("prune_ascend", format!("{}", wz.prune_ascend())),
                 32 => {
-                    let _pr = get!(d.boolean()); // decoded for stream alignment; see `no_prune`
+                    let pr = get!(d.boolean());
                     let leaky = focus_node_empty(&wz);
-                    let r = wz.remove_branches(no_prune);
+                    let r = wz.remove_branches(pr);
                     let s = if leaky { "?".to_string() } else { show_bool(r).to_string() };
                     ("remove_branches", s)
                 }
                 33 => {
                     let n = get!(d.modn(4));
                     let m = get!(d.path_n(n));
-                    let _pr = get!(d.boolean()); // decoded for stream alignment; see `no_prune`
-                    let mask = ByteMask::from_iter(m.iter().copied());
-                    wz.remove_unmasked_branches(mask, no_prune);
+                    let pr = get!(d.boolean());
                     let mut canon: Vec<u8> = m.clone();
                     canon.sort_unstable();
                     canon.dedup();
+                    let mask = ByteMask::from_iter(m.iter().copied());
+                    wz.remove_unmasked_branches(mask, pr);
                     ("remove_unmasked_branches", hex_path(&canon))
                 }
                 34 => {
@@ -737,15 +716,12 @@ pub fn run_ops<R: ReadSource>(
                     ("join_map_into", s)
                 }
                 38 => {
-                    let _pr = get!(d.boolean()); // decoded for stream alignment; see `no_prune`
-                    ("meet_into", show_status_opt((*rz).do_meet_into(&mut wz, no_prune)))
+                    let pr = get!(d.boolean());
+                    ("meet_into", show_status_opt((*rz).do_meet_into(&mut wz, pr)))
                 }
                 39 => {
-                    let _pr = get!(d.boolean()); // decoded for stream alignment; see `no_prune`
-                    (
-                        "subtract_into",
-                        show_status_opt((*rz).do_subtract_into(&mut wz, no_prune)),
-                    )
+                    let pr = get!(d.boolean());
+                    ("subtract_into", show_status_opt((*rz).do_subtract_into(&mut wz, pr)))
                 }
                 40 => {
                     let leaky = focus_node_empty(&wz);
@@ -771,13 +747,13 @@ pub fn run_ops<R: ReadSource>(
                 }
                 42 => {
                     let k = get!(d.modn(4));
-                    let _pr = get!(d.boolean()); // decoded for stream alignment; see `no_prune`
+                    let pr = get!(d.boolean());
                     // `join_k_path_into(0)` destroys the subtrie in pathmap 0.3.1.
                     if k == 0 {
                         ("join_k_path_into", SKIP_K0.to_string())
                     } else {
                         // The bool leaks node materialisation; see FINDINGS.md #8.
-                        let r = wz.join_k_path_into(k, no_prune);
+                        let r = wz.join_k_path_into(k, pr);
                         let s = if focus_node_empty(&wz) {
                             "?".to_string()
                         } else {
@@ -800,9 +776,9 @@ pub fn run_ops<R: ReadSource>(
                     ("remove_prefix", show_bool(wz.remove_prefix(n)).to_string())
                 }
                 45 => {
-                    let _pr = get!(d.boolean()); // decoded for stream alignment; see `no_prune`
+                    let pr = get!(d.boolean());
                     let leaky = focus_node_empty(&wz) && wz.val().is_none();
-                    let r = match wz.take_map(no_prune) {
+                    let r = match wz.take_map(pr) {
                         Some(m) => {
                             wz.graft_map(m);
                             "1"
@@ -813,7 +789,7 @@ pub fn run_ops<R: ReadSource>(
                 }
                 46 => {
                     let k = get!(d.modn(4));
-                    let _pr = get!(d.boolean()); // decoded for stream alignment; see `no_prune`
+                    let pr = get!(d.boolean());
                     // `meet_k_path_into` spins forever when the focus has no
                     // children, and escapes the focus subtree when k == 0.
                     // See `Zip.meetKPathUnspecified`.
@@ -824,7 +800,7 @@ pub fn run_ops<R: ReadSource>(
                     } else {
                         (
                             "meet_k_path_into",
-                            show_bool(wz.meet_k_path_into(k, no_prune)).to_string(),
+                            show_bool(wz.meet_k_path_into(k, pr)).to_string(),
                         )
                     }
                 }
diff --git a/differential/src/repro.rs b/differential/src/repro.rs
index 6d2c06f4..105638ee 100644
--- a/differential/src/repro.rs
+++ b/differential/src/repro.rs
@@ -170,33 +170,33 @@ pub fn emit_repro(bytes: &[u8], upto: usize) -> String {
                     else { "rz.make_map().val_count();".to_string() } }
             26 => { let t = g!(d.modn(2)); format!("{}.fork_read_zipper();", z!(t)) }
             27 => { let v = g!(d.u8()) as u64; format!("wz.set_val({v});") }
-            28 => { let _pr = g!(d.boolean()); "wz.remove_val(false);".to_string() }
+            28 => { let pr = g!(d.boolean()); format!("wz.remove_val({pr});") }
             29 => "wz.create_path();".to_string(),
             30 => "wz.prune_path();".to_string(),
             31 => "wz.prune_ascend();".to_string(),
-            32 => { let _pr = g!(d.boolean()); "wz.remove_branches(false);".to_string() }
-            33 => { let n = g!(d.modn(4)); let m = g!(d.path_n(n)); let _pr = g!(d.boolean());
-                    format!("wz.remove_unmasked_branches(ByteMask::from_iter({}.iter().copied()), false);", rs_mask(&m)) }
+            32 => { let pr = g!(d.boolean()); format!("wz.remove_branches({pr});") }
+            33 => { let n = g!(d.modn(4)); let m = g!(d.path_n(n)); let pr = g!(d.boolean());
+                    format!("wz.remove_unmasked_branches(ByteMask::from_iter({}.iter().copied()), {pr});", rs_mask(&m)) }
             34 => "wz.graft(&rz);".to_string(),
             35 => { let p = g!(d.path(6));
                     format!("wz.graft_src_at(&rz, {});", rs_bytes(&p)) }
             36 => "wz.join_into(&rz);".to_string(),
             37 => "wz.join_map_into(rz.make_map());".to_string(),
-            38 => { let _pr = g!(d.boolean()); "wz.meet_into(&rz, false);".to_string() }
-            39 => { let _pr = g!(d.boolean()); "wz.subtract_into(&rz, false);".to_string() }
+            38 => { let pr = g!(d.boolean()); format!("wz.meet_into(&rz, {pr});") }
+            39 => { let pr = g!(d.boolean()); format!("wz.subtract_into(&rz, {pr});") }
             40 => "wz.restrict(&rz);".to_string(),
             41 => "wz.restricting(&rz);".to_string(),
-            42 => { let k = g!(d.modn(4)); let _pr = g!(d.boolean());
+            42 => { let k = g!(d.modn(4)); let pr = g!(d.boolean());
                     if k == 0 { "// join_k_path_into(0): skipped by the harness".to_string() }
-                    else { format!("wz.join_k_path_into({k}, false);") } }
+                    else { format!("wz.join_k_path_into({k}, {pr});") } }
             43 => { let p = g!(d.path(6));
                     if p.is_empty() { "// insert_prefix(\"\"): skipped by the harness".to_string() }
                     else { format!("wz.insert_prefix({});", rs_bytes(&p)) } }
             44 => { let n = g!(d.modn(6)); format!("wz.remove_prefix({n});") }
-            45 => { let _pr = g!(d.boolean());
-                    "if let Some(m) = wz.take_map(false) { wz.graft_map(m); }".to_string() }
-            46 => { let k = g!(d.modn(4)); let _pr = g!(d.boolean());
-                    format!("if {k} != 0 && wz.child_count() != 0 {{ wz.meet_k_path_into({k}, false); }}") }
+            45 => { let pr = g!(d.boolean());
+                    format!("if let Some(m) = wz.take_map({pr}) {{ wz.graft_map(m); }}") }
+            46 => { let k = g!(d.modn(4)); let pr = g!(d.boolean());
+                    format!("if {k} != 0 && wz.child_count() != 0 {{ wz.meet_k_path_into({k}, {pr}); }}") }
             47 => { let t = g!(d.modn(2));
                     format!("{{ let mut obs = Vec::new(); {}.descend_until_observed(&mut obs); }}", z!(t)) }
             48 => { let v = g!(d.u8()) as u64;
diff --git a/lean/FINDINGS.md b/lean/FINDINGS.md
index 4d98c548..3ce6d531 100644
--- a/lean/FINDINGS.md
+++ b/lean/FINDINGS.md
@@ -187,54 +187,19 @@ The native `ReadZipper` overrides these with a token-based iterator that does
 terminate, so the hang is reachable through `meet_k_path_into` and through any
 zipper type that inherits the default `ZipperIteration` implementation.
 
-## 7. `prune_path` prunes above the zipper's root, and its count is unspecifiable
-
-`case: prune_reach` — **documentation is wrong; return value is unspecifiable**
-
-`ZipperWriting::prune_path` says "This method cannot prune the trie above the
-zipper's root."  It can and does:
-
-```rust
-map.insert(b"abcd", 1);
-let mut wz = map.write_zipper_at_path(b"ab");   // root at depth 2
-wz.descend_to(b"cd");
-wz.remove_val(false);
-wz.prune_path();                                // -> 4; the map is now empty
-```
-
-Worse, the number returned is `max(node_pruned_bytes, trie_pruned_bytes)`, and
-`node_pruned_bytes` depends on where the internal node holding the focus begins:
-
-| dangling chain | zipper root depth | returned | absolute | relative |
-| --- | --- | --- | --- | --- |
-| 8 bytes | 0 | 8 | 8 | 8 |
-| 8 bytes | 5 | 8 | 8 | 3 |
-| 100 bytes | 0 | 100 | 100 | 100 |
-| 100 bytes | 5 | **95** | 100 | 95 |
-
-The *effect* is the same in every row (the map ends up empty); only the reported
-count changes, switching between absolute and relative purely on node layout.
-The reach of the effect is layout-dependent too, in other shapes — a
-`remove_val(true)` under a zipper rooted at depth 3 was observed leaving one byte
-of a dangling chain behind where the same operation at the map root removes it.
-
-The `prune` **flag** on the other operations is worse than the explicit call.
-It is handed straight to `node_remove_val` / `node_remove_all_branches`, which
-prune within the node whether or not they found anything to remove:
-
-```rust
-// map = { [0] = 0 }, plus a dangling [1]
-let mut wz = map.write_zipper();
-wz.descend_to(&[1]);
-wz.remove_val(true);      // -> None, and yet [1] is gone
-```
-
-So `remove_val(true)` can delete a location while reporting that it removed
-nothing, and whether it does depends on where the node boundary falls.
-
-Consequence for anyone specifying this API: pruning is only well-defined for the
-explicit `prune_path` on a zipper rooted at the map root.  The harness passes
-`prune = false` everywhere else.
+## 7. Pruning contract
+
+The original `prune_reach` case described an older implementation where
+`prune_path` crossed the zipper root and returned a node-layout-dependent
+count.  It is fixed in the current checkout.  Current Rust tests
+`prune_should_not_cross_zipper_root`,
+`prune_should_not_cross_zipper_root_across_nodes`, and
+`prune_flags_preserve_zipper_root` cover that boundary.  The differential
+harness exercises explicit pruning at every zipper root.
+
+The model specifies the prune flag as `operation(false)` followed by
+`prune_path`, even after a no-op.  Lean guards in `PathMapModel/Check.lean` and
+Rust tests in `src/write_zipper.rs` cover pruning at and below the zipper root.
 
 ## 8. Several return values report on node materialisation, not on trie state
 
diff --git a/lean/PathMapModel/Check.lean b/lean/PathMapModel/Check.lean
index ea252df0..0e3b5dab 100644
--- a/lean/PathMapModel/Check.lean
+++ b/lean/PathMapModel/Check.lean
@@ -75,14 +75,29 @@ and below it (the location does not exist). -/
 #guard ((zipAt pruneT2b [] [0,0,0,1,2,3]).prunePath).1 == 0
 #guard ((zipAt pruneT2b [] [0,0,0,1,2,3,4,5]).prunePath).1 == 0
 
-/-! Pruning *does* rise above the zipper's root, contradicting the doc comment
-on `ZipperWriting::prune_path`.  A zipper rooted at `[0,0]` looking at the
-dangling tip of the same chain prunes all 7 bytes, back to the map root — not
-the 5 that lie below its own root.  Verified against pathmap 0.3.1; see
-`Zip.prunePath`. -/
-
-#guard ((zipAt pruneT2b [0,0] [0,1,2,3,4]).prunePath).1 == 7
-#guard ((zipAt pruneT2b [0,0] [0,1,2,3,4]).prunePath).2.trie.isEmptyMap
+/-! The zipper root bounds pruning, even for a dangling chain continuing above it. -/
+
+#guard ((zipAt pruneT2b [0,0] [0,1,2,3,4]).prunePath).1 == 5
+#guard ((zipAt pruneT2b [0,0] [0,1,2,3,4]).prunePath).2.trie.pathExists [0,0]
+#guard !((zipAt pruneT2b [0,0] [0,1,2,3,4]).prunePath).2.trie.pathExists [0,0,0]
+
+/-! The flag is an explicit prune after the operation, including a no-op.
+`false` preserves a dangling path. -/
+
+#guard (((zipAt pruneT2 [] [0,0,1,0,0]).removeVal true).2.trie.pathExists [0,0,1]) == false
+#guard (((zipAt pruneT2 [] [0,0,1,0,0]).removeVal false).2.trie.pathExists [0,0,1,0,0])
+#guard !(((zipAt pruneT2b [] [0,0,0,1,2,3,4]).removeVal true).2.trie.pathExists [0,0,0,1,2,3,4])
+#guard !(((zipAt pruneT2b [] []).removeBranches true).2.trie.pathExists [0])
+#guard (((zipAt pruneT2b [] []).removeBranches false).2.trie.pathExists [])
+#guard (((zipAt pruneT2b [] [0,0,0,1,2,3,4]).removeUnmaskedBranches
+  (ByteMask.ofList []) true).trie.pathExists [0,0,0,1,2,3,4]) == false
+#guard !(((zipAt pruneT2b [] [0,0,0,1,2,3,4]).takeMap true).2.trie.pathExists
+  [0,0,0,1,2,3,4])
+#guard !(((zipAt pruneT2b [] [0,0,0,1,2,3,4]).joinKPathInto ops 1 true).2.trie.pathExists
+  [0,0,0,1,2,3,4])
+#guard (((zipAt pruneT2b [0,0] [0,1,2,3,4]).removeVal true).2.trie.pathExists [0,0])
+#guard !(((zipAt pruneT2b [0,0] [0,1,2,3,4]).removeVal true).2.trie.pathExists
+  [0,0,0])
 
 /-! `write_zipper_drop_head_test3`: `[[0,0],[0,1],[1,0],[1,1]]` with
 `join_k_path_into(1)` collapses to 2 values. -/
diff --git a/lean/PathMapModel/Fuzz.lean b/lean/PathMapModel/Fuzz.lean
index 977325d0..9175ec6b 100644
--- a/lean/PathMapModel/Fuzz.lean
+++ b/lean/PathMapModel/Fuzz.lean
@@ -66,8 +66,6 @@ agree exactly or every input with a skip diverges.
 * `skip:empty-focus` — the focus has nothing below it, where the op's behaviour
   is a function of node materialisation rather than trie state.
 * `skip:empty-path` — `insert_prefix("")`, which destroys the subtrie.
-* `skip:off-root-prune` — a prune on a write zipper not rooted at the map root,
-  where the depth pruned is a function of internal node layout.
 * `skip:quarantined` — the op is disabled outright (op 54).
 
 Each is recorded in FINDINGS.md and commented at its site. -/
@@ -77,7 +75,6 @@ def skipAtRoot : String := "skip:at-root"
 def skipK0 : String := "skip:k0"
 def skipEmptyFocus : String := "skip:empty-focus"
 def skipEmptyPath : String := "skip:empty-path"
-def skipOffRootPrune : String := "skip:off-root-prune"
 def skipQuarantined : String := "skip:quarantined"
 
 /-! ## Rendering -/
@@ -189,35 +186,9 @@ def emit (s : St) (name : String) (ret : String) : St :=
 def showBool (b : Bool) : String := if b then "1" else "0"
 
 
-/-- Is the *explicit* `prune_path` / `prune_ascend` well-defined for this state?
-
-Only for a write zipper rooted at the map root.  Pruning happens in two places:
-`node_remove_*` prunes within the internal node holding the focus, and
-`prune_path_internal` prunes the trie above it but stops at the zipper's origin.
-With a non-empty zipper root the two disagree and the depth pruned becomes a
-function of node layout rather than of the logical trie — a 40-byte dangling
-chain under a zipper rooted at depth 5 prunes to the map root, a 100-byte one
-stops at the zipper root.
-
-The `prune` *flag* on the other operations is worse: it is passed straight to
-`node_remove_val` / `node_remove_all_branches`, which prune within the node even
-when they find nothing to remove and report `None`.  So `remove_val(true)` can
-delete a dangling location while returning `None`, and whether it does depends on
-where the node boundary falls.  The harness therefore always passes
-`prune = false` to those operations (see `noPrune`) and gates the explicit prune
-operations on this predicate. -/
-def pruneable (s : St) : Bool := s.wz.root.isEmpty
-
-/-- The `prune` flag the harness passes to operations that take one.
-
-Always `false`: the flag's effect is a function of internal node layout rather
-than of the logical trie, so there is nothing for a model to agree with.  See
-`pruneable` and lean/FINDINGS.md finding 7. -/
-def noPrune : Bool := false
-
 /-! ## The operation table
 
-`op % 47` selects the operation.  Ops `0`–`26` act on a target zipper chosen by
+`op % 56` selects the operation.  Ops `0`–`26` act on a target zipper chosen by
 a following `u8 % 2` byte (`0` = write zipper, `1` = read zipper); ops `27`–`46`
 are write-zipper operations. -/
 
@@ -362,26 +333,22 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do
   | 27 => do let (v, d) ← d.u8
              let (old, z) := s.wz.setVal (UInt64.ofNat v.toNat)
              some (emit { s with wz := z } "set_val" (showVal old), d)
-  | 28 => do let (_pr, d) ← d.bool
-             let (old, z) := s.wz.removeVal noPrune
+  | 28 => do let (pr, d) ← d.bool
+             let (old, z) := s.wz.removeVal pr
              some (emit { s with wz := z } "remove_val" (showVal old), d)
   | 29 => do let (r, z) := s.wz.createPath
              some (emit { s with wz := z } "create_path" (showBool r), d)
-  | 30 => do if pruneable s then
-               let (n, z) := s.wz.prunePath
-               some (emit { s with wz := z } "prune_path" (toString n), d)
-             else some (emit s "prune_path" skipOffRootPrune, d)
-  | 31 => do if pruneable s then
-               let (n, z) := s.wz.pruneAscend
-               some (emit { s with wz := z } "prune_ascend" (toString n), d)
-             else some (emit s "prune_ascend" skipOffRootPrune, d)
-  | 32 => do let (_pr, d) ← d.bool
+  | 30 => do let (n, z) := s.wz.prunePath
+             some (emit { s with wz := z } "prune_path" (toString n), d)
+  | 31 => do let (n, z) := s.wz.pruneAscend
+             some (emit { s with wz := z } "prune_ascend" (toString n), d)
+  | 32 => do let (pr, d) ← d.bool
              let leaky := s.wz.focusNodeIsEmpty
-             let (r, z) := s.wz.removeBranches noPrune
+             let (r, z) := s.wz.removeBranches pr
              some (emit { s with wz := z } "remove_branches"
                (if leaky then "?" else showBool r), d)
-  | 33 => do let (n, d) ← d.mod 4; let (m, d) ← d.pathN n; let (_pr, d) ← d.bool
-             let z := s.wz.removeUnmaskedBranches (ByteMask.ofList m) noPrune
+  | 33 => do let (n, d) ← d.mod 4; let (m, d) ← d.pathN n; let (pr, d) ← d.bool
+             let z := s.wz.removeUnmaskedBranches (ByteMask.ofList m) pr
              some (emit { s with wz := z } "remove_unmasked_branches" (hexPath (ByteMask.ofList m)), d)
   | 34 => do if s.act then some (emit s "graft" skipAct, d) else
              do
@@ -402,15 +369,15 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do
                let (st, z) := s.wz.joinMapInto ops s.rz.makeMap
                some (emit { s with wz := z } "join_map_into"
                  (if leaky then "?" else toString st), d)
-  | 38 => do let (_pr, d) ← d.bool
+  | 38 => do let (pr, d) ← d.bool
              if s.act then some (emit s "meet_into" skipAct, d)
              else
-               let (st, z) := s.wz.meetInto ops s.rz noPrune
+               let (st, z) := s.wz.meetInto ops s.rz pr
                some (emit { s with wz := z } "meet_into" (toString st), d)
-  | 39 => do let (_pr, d) ← d.bool
+  | 39 => do let (pr, d) ← d.bool
              if s.act then some (emit s "subtract_into" skipAct, d)
              else
-               let (st, z) := s.wz.subtractInto ops s.rz noPrune
+               let (st, z) := s.wz.subtractInto ops s.rz pr
                some (emit { s with wz := z } "subtract_into" (toString st), d)
   | 40 => do if s.act then some (emit s "restrict" skipAct, d) else
              do
@@ -432,7 +399,7 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do
              else
                let (r, z) := s.wz.restricting s.rz
                some (emit { s with wz := z } "restricting" (showBool r), d)
-  | 42 => do let (k, d) ← d.mod 4; let (_pr, d) ← d.bool
+  | 42 => do let (k, d) ← d.mod 4; let (pr, d) ← d.bool
              -- `join_k_path_into(0)` should be the identity but destroys the
              -- subtrie in pathmap 0.3.1; see `Zip.joinKPathInto`.
              if k == 0 then some (emit s "join_k_path_into" skipK0, d)
@@ -442,7 +409,7 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do
                -- representations, so `true` gets reported for a collapse that
                -- produced nothing.  Compared only when something survived.
                -- See FINDINGS.md #8.
-               let (r, z) := s.wz.joinKPathInto ops k noPrune
+               let (r, z) := s.wz.joinKPathInto ops k pr
                some (emit { s with wz := z } "join_k_path_into"
                  (if z.focusNodeIsEmpty then "?" else showBool r), d)
   | 43 => do let (p, d) ← d.path
@@ -456,9 +423,9 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do
   | 44 => do let (n, d) ← d.mod 6
              let (r, z) := s.wz.removePrefix n
              some (emit { s with wz := z } "remove_prefix" (showBool r), d)
-  | 45 => do let (_pr, d) ← d.bool
+  | 45 => do let (pr, d) ← d.bool
              let leaky := s.wz.focusNodeIsEmpty && s.wz.val.isNone
-             let (m, z) := s.wz.takeMap noPrune
+             let (m, z) := s.wz.takeMap pr
              if leaky then
                some (emit { s with wz := (z.graftMap (m.getD PathMap.empty)) }
                  "take_map_restore" "?", d)
@@ -466,7 +433,7 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do
              match m with
              | some mm => some (emit { s with wz := z.graftMap mm } "take_map_restore" "1", d)
              | none => some (emit { s with wz := z } "take_map_restore" "0", d)
-  | 46 => do let (k, d) ← d.mod 4; let (_pr, d) ← d.bool
+  | 46 => do let (k, d) ← d.mod 4; let (pr, d) ← d.bool
              -- `meet_k_path_into` is not implementable for these arguments; see
              -- `Zip.meetKPathUnspecified`, whose two disjuncts are split out here
              -- so the skip names which one fired.  The Rust side matches.
@@ -474,7 +441,7 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do
              else if s.wz.focusNodeIsEmpty then
                some (emit s "meet_k_path_into" skipEmptyFocus, d)
              else
-               let (r, z) := s.wz.meetKPathInto ops k noPrune
+               let (r, z) := s.wz.meetKPathInto ops k pr
                some (emit { s with wz := z } "meet_k_path_into" (showBool r), d)
   | 47 => do let (t, d) ← d.mod 2
              -- The blind-zipper addition: `descend_until` reporting the bytes it
diff --git a/lean/PathMapModel/PathMap.lean b/lean/PathMapModel/PathMap.lean
index 2054dfd9..e07c3157 100644
--- a/lean/PathMapModel/PathMap.lean
+++ b/lean/PathMapModel/PathMap.lean
@@ -271,8 +271,8 @@ def addPath (t : PathMap V) (p : Path) : PathMap V := mk' t.vals (p :: t.paths)
 
 `prune_path` deletes the dangling chain ending at the focus, stopping at the
 first location above it that carries a value, that branches, or that is the
-zipper's root.  It is a no-op unless the focus is a *dangling tip*: it exists,
-has no value, and has no children. -/
+zipper's root.  The root itself is retained.  It is a no-op unless the focus is
+a *dangling tip* below that root: it exists, has no value, and has no children. -/
 
 /-- Is `p` a dangling tip — an existing location with neither value nor children? -/
 def isDanglingTip (t : PathMap V) (p : Path) : Bool :=
diff --git a/lean/PathMapModel/Write.lean b/lean/PathMapModel/Write.lean
index 6ee3a84e..c5e43eed 100644
--- a/lean/PathMapModel/Write.lean
+++ b/lean/PathMapModel/Write.lean
@@ -15,9 +15,9 @@ invariants shape the whole API and are worth stating up front:
    the model assumes throughout.  Note the resulting asymmetry: `graft` adopts
    the source's focus value but `join_into` does **not** join focus values.
 
-2. **Pruning is opt-in and local.**  A write leaves dangling paths behind unless
-   `prune` is passed, and even then `prune_path` only fires when the focus is a
-   dangling tip.  Pruning stops at the zipper's root and never rises above it.
+2. **Pruning is opt-in and root-bounded.**  A write leaves dangling paths behind
+   unless `prune` is passed.  Passing `true` means running the operation with
+   `false`, then calling `prunePath` at the resulting focus, even after a no-op.
 -/
 
 namespace PathMapModel
@@ -71,28 +71,12 @@ def getValOrSetMutWith (d : V) : V × Bool × Zip V :=
   | some v => (v, false, z)
   | none => (d, true, (z.setVal d).2)
 
-/-- `ZipperWriting::prune_path`: delete the dangling chain ending at the focus,
-stopping at the first location above it that carries a value or branches.  The
-focus does **not** move.
-
-Two things about this differ from the doc comment on `ZipperWriting::prune_path`,
-both verified against `pathmap` 0.3.1:
-
-* **It prunes above the zipper's root.**  The doc says "This method cannot prune
-  the trie above the zipper's root", but a write zipper rooted at `ab` whose
-  focus is a dangling tip deletes `a` and `ab` too, right up to the nearest
-  branch or value in the *whole map*.  The model therefore passes `0`, not
-  `z.root.length`, as the stop depth.
-* **The returned count is not well-defined** when the zipper's root is non-empty.
-  `prune_path` returns `max(node_pruned_bytes, trie_pruned_bytes)`, and
-  `node_pruned_bytes` depends on where the internal node holding the focus
-  happens to begin.  Empirically, a 40-byte dangling chain under a zipper rooted
-  at depth 5 reports 40 (absolute) while a 100-byte one reports 95 (relative).
-  The *effect* is the same in both cases; only the number differs.  The model
-  reports the absolute count, and the differential harness compares the count
-  only for zippers rooted at the map root. -/
+/-- `ZipperWriting::prune_path`: remove the dangling suffix ending at the focus.
+The first valued or branching ancestor survives; the zipper root is also a hard
+stop.  Return the number of bytes removed, relative to the focus, without moving
+the cursor.  An absent, valued, or branching focus returns zero. -/
 def prunePath : Nat × Zip V :=
-  let (n, t) := z.trie.prunePath 0 z.focus
+  let (n, t) := z.trie.prunePath z.root.length z.focus
   (n, z.withTrie t)
 
 /-- `ZipperWriting::prune_ascend`: `prune_path` followed by ascending that far. -/
@@ -100,20 +84,11 @@ def pruneAscend : Nat × Zip V :=
   let (n, z') := z.prunePath
   (n, (z'.ascend n).2)
 
-/-- `ZipperWriting::remove_val`: removes the value, leaving the location as a
-dangling path unless `prune` reclaims it.
-
-Pruning only happens when a value was actually removed: `remove_val` returns
-early on the `None` branch, so `remove_val(true)` at a location with no value
-leaves any dangling path in place. -/
+/-- `ZipperWriting::remove_val`: remove the value, then optionally prune. -/
 def removeVal (prune : Bool) : Option V × Zip V :=
-  match z.entry with
-  -- Nothing to remove.  Note the `prune` flag does not fire here: `remove_val`
-  -- returns early on this branch, so a dangling path is left in place.
-  | .absent | .bare => (none, z)
-  | .valued v =>
-    let z' := z.withTrie (z.trie.removeVal z.focus).2
-    (some v, if prune then (z'.prunePath).2 else z')
+  let (old, t) := z.trie.removeVal z.focus
+  let z' := z.withTrie t
+  (old, if prune then (z'.prunePath).2 else z')
 
 /-- `ZipperWriting::create_path`: make the focus exist as a dangling path.
 Returns whether new bytes were created.
@@ -208,17 +183,15 @@ def graftChildMaps (maps : List (ByteMask × PathMap V)) (removeUnset : Bool) :
 /-- `ZipperWriting::take_map`: remove the subtrie at the focus (value included)
 and return it as a `PathMap`.  Returns `none` when there was nothing to take. -/
 def takeMap (prune : Bool) : Option (PathMap V) × Zip V :=
-  let rv := z.entry.val
-  let z1 := z.withTrie (z.trie.removeVal z.focus).2
-  let z2 := if prune then (z1.prunePath).2 else z1
-  let below := z2.focusNode
-  let z3 := z2.withTrie (z2.trie.removeBelow z2.focus)
-  let z4 := if prune then (z3.prunePath).2 else z3
+  let (rv, z1) := z.removeVal false
+  let below := z1.focusNode
+  let (_, z2) := z1.removeBranches false
   let taken :=
     match rv with
     | some v => (below.setVal [] v).2
     | none => below
-  (if below.isEmptyMap && rv.isNone then none else some taken, z4)
+  (if below.isEmptyMap && rv.isNone then none else some taken,
+    if prune then (z2.prunePath).2 else z2)
 
 /-! ## Path surgery -/
 
@@ -331,7 +304,7 @@ def joinIntoTake (src : Zip V) (prune : Bool) : AlgStatus × Zip V × Zip V :=
 The value step runs first and can prune the focus out from under the node step.
 A meet drops every dangling path, since a location only survives if it leads to
 a surviving value. -/
-def meetInto (src : Zip V) (prune : Bool) : AlgStatus × Zip V :=
+def meetIntoWithoutPrune (src : Zip V) : AlgStatus × Zip V :=
   let (valStatus, valWasNone, z1) :=
     match z.val, src.val with
     | some sv, some ov =>
@@ -339,9 +312,9 @@ def meetInto (src : Zip V) (prune : Bool) : AlgStatus × Zip V :=
         (AlgStatus.ofValRes r, false,
           match r.resolve sv ov with
           | some v => (z.setVal v).2
-          | none => (z.removeVal prune).2)
+          | none => (z.removeVal false).2)
     | none, some _ => (AlgStatus.none, true, z)
-    | some _, none => (AlgStatus.none, false, (z.removeVal prune).2)
+    | some _, none => (AlgStatus.none, false, (z.removeVal false).2)
     | none, none => (AlgStatus.none, true, z)
   let selfB := z1.focusNode
   let srcB := src.focusNode
@@ -349,8 +322,7 @@ def meetInto (src : Zip V) (prune : Bool) : AlgStatus × Zip V :=
     (AlgStatus.merge .none valStatus true valWasNone, z1)
   else if srcB.isEmptyMap then
     let z2 := z1.withTrie (z1.trie.removeBelow z1.focus)
-    let z3 := if prune then (z2.prunePath).2 else z2
-    (AlgStatus.merge .none valStatus false valWasNone, z3)
+    (AlgStatus.merge .none valStatus false valWasNone, z2)
   else
     let r := PathMap.meet ops selfB srcB
     let st := nodeStatus ops selfB r
@@ -358,15 +330,20 @@ def meetInto (src : Zip V) (prune : Bool) : AlgStatus × Zip V :=
       if st == .identity then z1
       else
         let zg := z1.withTrie (z1.trie.graftBelow z1.focus r)
-        if st == .none && prune then (zg.prunePath).2 else zg
+        zg
     (AlgStatus.merge st valStatus false valWasNone, z2)
 
+/-- A true flag is exactly an explicit prune after the meet. -/
+def meetInto (src : Zip V) (prune : Bool) : AlgStatus × Zip V :=
+  let (st, z') := z.meetIntoWithoutPrune ops src
+  (st, if prune then (z'.prunePath).2 else z')
+
 /-- `ZipperWriting::subtract_into`: remove the source's subtrie from the focus's.
 
 Where the source has no node at all, `self`'s subtree survives untouched —
 dangling paths included.  Where it does, only locations leading to a surviving
 value are kept. -/
-def subtractInto (src : Zip V) (prune : Bool) : AlgStatus × Zip V :=
+def subtractIntoWithoutPrune (src : Zip V) : AlgStatus × Zip V :=
   let (valStatus, valWasNone, z1) :=
     match z.val, src.val with
     | some sv, some ov =>
@@ -374,7 +351,7 @@ def subtractInto (src : Zip V) (prune : Bool) : AlgStatus × Zip V :=
         (AlgStatus.ofValRes r, false,
           match r.resolve sv ov with
           | some v => (z.setVal v).2
-          | none => (z.removeVal prune).2)
+          | none => (z.removeVal false).2)
     | none, some _ => (AlgStatus.none, true, z)
     | some _, none => (AlgStatus.identity, false, z)
     | none, none => (AlgStatus.none, true, z)
@@ -392,9 +369,14 @@ def subtractInto (src : Zip V) (prune : Bool) : AlgStatus × Zip V :=
       if st == .identity then z1
       else
         let zg := z1.withTrie (z1.trie.graftBelow z1.focus r)
-        if st == .none && prune then (zg.prunePath).2 else zg
+        zg
     (AlgStatus.merge st valStatus false valWasNone, z2)
 
+/-- A true flag is exactly an explicit prune after the subtraction. -/
+def subtractInto (src : Zip V) (prune : Bool) : AlgStatus × Zip V :=
+  let (st, z') := z.subtractIntoWithoutPrune ops src
+  (st, if prune then (z'.prunePath).2 else z')
+
 /-- `ZipperWriting::meet_2`: meet two *source* subtries and write the result at
 the focus.
 
@@ -463,7 +445,7 @@ def joinKPathInto (k : Nat) (prune : Bool) : Bool × Zip V :=
     else
       let r := PathMap.dropHead ops below k
       (!r.isEmptyMap, z.withTrie (z.trie.graftBelow z.focus r))
-  (res, if prune && !res then (z1.prunePath).2 else z1)
+  (res, if prune then (z1.prunePath).2 else z1)
 
 /-- `meet_k_path_into` is **not implementable** for these arguments: its
 provisional implementation drives `descend_first_k_path` through the
@@ -486,9 +468,11 @@ def meetKPathInto (k : Nat) (prune : Bool) : Bool × Zip V :=
       match acc with
       | none => some m
       | some a => some (PathMap.meet ops a m)) none
-  match result with
-  | some m => if m.isEmptyMap then (false, (z.removeBranches prune).2) else (true, z.graftMap m)
-  | none => (false, (z.removeBranches prune).2)
+  let (b, z') :=
+    match result with
+    | some m => if m.isEmptyMap then (false, (z.removeBranches false).2) else (true, z.graftMap m)
+    | none => (false, (z.removeBranches false).2)
+  (b, if prune then (z'.prunePath).2 else z')
 
 end Zip
 end PathMapModel
diff --git a/lean/README.md b/lean/README.md
index 60696f91..7d39c2c8 100644
--- a/lean/README.md
+++ b/lean/README.md
@@ -168,9 +168,9 @@ Honest accounting, because it matters for how much the model is worth:
   separate the focus from its stop depth.
 * **Machine-checked on fixtures** (`Check.lean`): the metamorphic laws in
   `Spec.lean` §2, evaluated at build time over six trie shapes crossed with
-  eight focus positions — plus regression fixtures whose expected values are
+  eight focus positions — plus pruning contract checks, regression fixtures
   transcribed from `pathmap`'s own unit tests (`write_zipper_prune_path_test2`,
-  `write_zipper_drop_head_test1/3/6`) and the `restrict` oracle from
+  `write_zipper_drop_head_test1/3/6`), and the `restrict` oracle from
   `tests/pathmap_algebra_differential.rs`.
 * **Checked against the crate** (`differential.py`): everything else, on every
   generated program.
@@ -178,6 +178,21 @@ Honest accounting, because it matters for how much the model is worth:
 The definitions themselves are the specification.  They are total and executable,
 so "the spec" and "the oracle" cannot drift apart.
 
+### Pruning contract
+
+`Zip.prunePath` removes a dangling suffix only when the focus exists and has
+neither a value nor children.  It stops at the closest valued or branching
+ancestor, or at the write zipper's root, whichever comes first.  It leaves the
+cursor at the focus and returns the number of removed path bytes;
+`Zip.pruneAscend` then ascends by that count.  The root itself survives.
+
+A `prune` flag means running the operation with `false`, then calling
+`prune_path` at the resulting focus.  This applies even when the operation
+returns `None` or otherwise changes nothing.  These rules are encoded in
+`PathMap.lean` and `Write.lean` and checked with fixtures in `Check.lean`.
+The harness runs pruning at every zipper root and reports disagreements with
+the Rust implementation.
+
 ## The differential harness
 
 A fuzzer input is a byte string.  Lean and Rust decode it with identical rules
@@ -333,7 +348,6 @@ skips diverges:
 | `skip:empty-focus` | `meet_k_path_into` with no children (it does not terminate), and `restricting` when either side has nothing below its focus (the two branches differ in *effect*, not just in the reported bool). |
 | `skip:empty-path` | `insert_prefix("")` — should be the identity, destroys the subtrie. |
 | `skip:at-root` | `to_next_sibling_byte` / `to_prev_sibling_byte` at the zipper root — the native read zipper leaves its own root there. |
-| `skip:off-root-prune` | `prune_path` / `prune_ascend`, and the `prune` flag on every other operation, for a write zipper not rooted at the map root — the depth pruned is a function of internal node layout, so there is nothing to specify. |
 | `skip:quarantined` | `graft_child_maps` (op 54), disabled outright: it is broken three ways (FINDINGS.md #15) and the node representations it leaves behind degrade the `AlgebraicStatus` that *later* operations report. |
 | `skip:act` | ACT mode only — the read source cannot be a merge source (`ZipperInfallibleSubtries` is not implemented for it) or does not implement the trait the op needs. |
 
@@ -400,7 +414,7 @@ observed behaviour rather than intent, and are the places to distrust:
 | --- | --- |
 | `AlgStatus.merge` | transcribed line-for-line from `src/ring.rs` |
 | `joinVal` / `meetVal` / `subVal` | follow `Option<V>`'s impls in `src/ring.rs` |
-| `Zip.prunePath` | stop depth determined empirically; the doc comment is wrong |
+| `Zip.prunePath` | specifies the documented zipper-root bound and the count of removed bytes |
 | `Zip.toNextKPath` | deliberately follows the native `ReadZipper` over the trait default |
 | `PathMap.dropHead` | "values at depth exactly `k` are lost" is observed, not documented |
 | `Zip.joinMapInto` | the short-circuit asymmetry with `join_into` is observed |
@@ -512,9 +526,8 @@ happens to read the damaged location -- value bias, for instance, is reported by
 `meet_into` where it is introduced but by `dump`, `val_at` or the final map dump
 wherever it is later observed.  `divergence_shape` in `differential.py` decides
 those, and returning "no familiar shape" is its important case: it is what keeps
-a genuinely new defect out of the known buckets.  A shrunk reproducer for each
-class is in `lean/corpus/`, and `./lean/differential.py lean/corpus/*.bin`
-replays them all.
+a genuinely new defect out of the known buckets.  The remaining corpus inputs
+can be replayed with `./lean/differential.py lean/corpus/*.bin`.
 
 `differential.py` prints the breakdown itself, so new divergences stay visible as
 the known ones are fixed.
diff --git a/lean/differential.py b/lean/differential.py
index 0e91a522..cf5f6160 100755
--- a/lean/differential.py
+++ b/lean/differential.py
@@ -271,7 +271,7 @@ def run(self, blob):
      "[act: last_path_overshoots]"),
     # Shape classes, from `divergence_shape`.  Last on purpose: every entry
     # above is more specific, and these are meant to catch only what none of
-    # them explain.  Reproducers for each are in lean/corpus/.
+    # them explain.
     (["STATUS-ONLY"],
      "AlgebraicStatus::Identity is not returned reliably when nothing changed "
      "(finding 8); meet_into/subtract_into, status only, effects agree "
@@ -280,6 +280,9 @@ def run(self, blob):
      "an algebraic op keeps a dangling child the spec drops: an empty child "
      "node meets/subtracts to itself rather than disappearing "
      "[meet_keeps_dangling]"),
+    (["DANGLING-FOCUS-KEPT"],
+     "meet_into() keeps an empty materialized focus that the spec removes "
+     "[meet_keeps_dangling]"),
     (["CONTENT-DROPPED"],
      "subtract_into() drops a value under a path present in the source "
      "[subtract_drops_value]"),
@@ -371,6 +374,10 @@ def divergence_shape(a, b):
         if all(x[1:].isdigit() and y[1:].isdigit() for x, y in diff):
             return "VALUE-ONLY"
         return None
+    if (keys == {"e"} and len(diff) == 1 and len(ta) > 2
+            and ta[1] == "meet_into" and "ret=None" in ta
+            and diff[0] == ("e0", "e1")):
+        return "DANGLING-FOCUS-KEPT"
     if keys <= {"ret", "c", "n"} and ({"c", "n"} & keys):
         # `c` (child_count) when it moved, else `n` (val_count): a dangling
         # child adds a child without adding a value, a dropped value the
diff --git a/lean/shrink.py b/lean/shrink.py
index 65f23f64..76e0c782 100755
--- a/lean/shrink.py
+++ b/lean/shrink.py
@@ -56,7 +56,11 @@ def signature(blob):
             strip = lambda t: re.sub(r" n\d+", " n?", t)
             vc = (len(pa) == 2 and len(pb) == 2 and pa[0] == pb[0]
                   and strip(pa[1]) == strip(pb[1]))
-            return "DIFF %s%s" % ("valcount-only " if vc else "", a.split()[1])
+            fields = a.split()
+            op = fields[1] if len(fields) > 1 and fields[0].isdigit() else (fields[0] if fields else "blank")
+            if op == "remove_val" and any(t.startswith("ret=") and t != "ret=-" for t in fields):
+                op += " valued"
+            return "DIFF %s%s" % ("valcount-only " if vc else "", op)
     if len(ml) != len(cl):
         return "DIFF length"
     return None