Repository navigation
Focus value consistency - #163
luketpeterson wants to merge 13 commits into
Conversation
…e correct behavior has been settled for over a year and it was just cruft
Changing PathMap::restrict and WriteZipper::restrict to return None instead of Identity when the destination started empty
…nsistent behavior around zippers positioned at dangling paths #104
…ng out tests, and updating the API to match "blind zipper" patterns. Improving documentation and adding a diagram to illustrate behavior #104
Differential fuzz vs Lean model: successjob log · 2026-10-28 14:18:18 UTC WARNING: 147 new divergence(s) relative to base crate: 20000 inputs, seed 7agree = model and crate match; known = the divergence matches a classified bug in differential.py; new = it matches none. Only the new set is compared input by input below.
130 input(s) diverge on head but not on base; 8453 diverge on base but not on head. Known-class hits that changed
Newly diverging inputs (head only): 130 input(s), 1 kind(s)
Reproducers: first 1 distinct kind(s), shrunk
|
| side | agree | known | new divergences |
|---|---|---|---|
| head | 3502/5000 | 1432 | 66 |
| base | 1559/5000 | 1528 | 1913 |
17 input(s) diverge on head but not on base; 1864 diverge on base but not on head.
Known-class hits that changed
| known class | base | head |
|---|---|---|
| subtract_into() drops a value under a path present in the source [subtract_drops_value] | 400 | 0 |
| ACTZipper::val_count() counts from the zipper root, not the focus [act: val_count_ignores_focus] | 1093 | 1420 |
| which value survives a collision follows node layout rather than the left-biased spec (join/meet and | 35 | 12 |
Newly diverging inputs (head only): 17 input(s), 1 kind(s)
| first differs at | inputs | first example |
|---|---|---|
meet_k_path_into |
17 | random#00410: line 25 |
Reproducers: first 1 distinct kind(s), shrunk
random#00410: first differs at meet_k_path_into, 252 -> 22 bytes (act mode: the harness reads map1 through an ArenaCompactTree; the reproducer uses a PathMap read zipper)
line 25
lean: 25 meet_k_path_into ret=0 W=_ o0000 e1 v126 c0 n1 f? R=_ o_ e1 v- c1 n1 f?
crate: 25 meet_k_path_into ret=0 W=_ o0000 e1 v- c0 n0 f? R=_ o_ e1 v- c1 n1 f?
//! Generated by `pathmap_trace --repro`. Reproduces a fuzzer input as
//! plain `pathmap` API calls.
//!
//! `wz` writes into map0 and `rz` reads map1; they are separate maps so
//! both can be held at once. Values are `u64`.
use pathmap::PathMap;
use pathmap::utils::ByteMask;
use pathmap::zipper::*;
fn main() {
let mut map0 = PathMap::<u64>::new();
let mut map1 = PathMap::<u64>::new();
let mut wz = map0.write_zipper_at_path(&[]);
let mut rz = map1.read_zipper_at_path(&[]);
/* 0 */ wz.insert_prefix(&[0u8]);
/* 1 */ wz.get_val_or_set_mut(0);
/* 2 */ if 1 != 0 && wz.child_count() != 0 { wz.meet_k_path_into(1, false); }
drop(wz);
// What the maps hold at the end -- compare against the trace's MAP0/MAP1.
println!("MAP0 {:?}", map0.iter().collect::<Vec<_>>());
println!("MAP1 {:?}", map1.iter().collect::<Vec<_>>());
}1864 input(s) fixed on head
random#00000random#00008random#00013random#00015random#00016random#00017random#00020random#00027random#00030random#00035random#00038random#00041random#00043random#00044random#00048random#00051random#00052random#00054random#00060random#00064random#00068random#00070random#00072random#00076random#00077random#00086random#00087random#00088random#00092random#00093random#00094random#00096random#00098random#00099random#00100random#00103random#00106random#00107random#00108random#00110random#00111random#00113random#00114random#00121random#00122random#00124random#00127random#00130random#00134random#00135
Bench A/B vs base: donejob log · 2026-10-28 14:26:12 UTC base 91abaa8 → head 75cc482, 3 round(s), median of each run averaged; negative is faster
59 case(s) moved more than 5%
Full tables per bench are in the job log and the bench-out artifact. |
…s the purview of #117, so it doesn't appear as a new divergence
|
Full perf data attached. No detectable change in any recursive workloads (real-world cases). Degenerate cases with like joining two single-path tries together show the cost of checking the focus value (about 10%), but I don't think it's worth sacrificing to optimize for these degenerate cases, and the cost will actually be reversed (become a gain) when the new node contract is implemented. |
|
Can we hold off on merging this? This touches a ton of stuff there's no benchmark for here. I have two sets of benchmarks, but need some time to integrate them. |
imlvts
left a comment
There was a problem hiding this comment.
This is a bit more involved than I expected, but this certainly improves consistency.
If I'm not mistaken this also fixes one of the issues I encountered when doing algebraic equivalence, specifically because of the root/focus value.
Looks good.
I snuck in an API consistency fix and better documentation (both for remove_prefix). That's some of the extra bulk. I'm holding until we get the all-clear on real-world perf. |
…rune when a lredy empty and a zero-arg was passed, and an infinite loop when already empty
# Conflicts: # Cargo.toml # src/write_zipper.rs
|
🎉 |
This should be ready to go. Details about the changes in #104 issue.
Builds on #162
@imlvts Make sure I didn't screw the lean model. Changes seem like improvements / simplifications to me.