Skip to content

Rounding out specification of prune behavior inside lean model #152

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
luketpeterson merged 2 commits into from
Oct 4, 2026
Merged

Rounding out specification of prune behavior inside lean model #152

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
961c7ad
Rounding out specification of prune behavior inside lean model
luketpeterson Oct 2, 2026
875564f
Removing references to reproduction cases, because they are out-of-sc…
luketpeterson Oct 4, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 3 additions & 5 deletions differential/src/bin/zipper_bug_repros.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"),
Expand Down Expand Up @@ -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] {
Expand Down
66 changes: 21 additions & 45 deletions differential/src/harness.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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?
Expand Down Expand Up @@ -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) => {
Expand Down Expand Up @@ -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 => {
Expand Down Expand Up @@ -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);
Expand All @@ -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 {
Expand All @@ -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"
Expand All @@ -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`.
Expand All @@ -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(),
)
}
}
Expand Down
24 changes: 12 additions & 12 deletions differential/src/repro.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
61 changes: 13 additions & 48 deletions lean/FINDINGS.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
31 changes: 23 additions & 8 deletions lean/PathMapModel/Check.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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. -/
Expand Down
Loading