WriteZipper::insert_prefix (master code).
map = {aaa}
map.write_zipper().descend_to(b"a"); insert_prefix(b"b");
map.iter() -> ["abaa", "aaa"] // the stale path is still reachable
validate_node(root) -> "ambiguous path violation" // child at slot 0 with a key that prefixes slot 1'sSame invalid node shape that master's lean/FINDINGS.md §14 (PR #69) records for graft;
insert_prefix is another route to it (their §4 covers only insert_prefix("")). The PR's Case 3
debug_assert_eq!(key1.len(), 1) trips on such nodes — keep that assert — and in release the recursive
engine would misplace the value. Until fixed, path-sensitive cata results on maps mutated by
insert_prefix/graft cannot be trusted, and the randomized cata tests should avoid those operations
at mid-key foci.
WriteZipper::insert_prefix(master code).Same invalid node shape that master's
lean/FINDINGS.md§14 (PR #69) records forgraft;insert_prefixis another route to it (their §4 covers onlyinsert_prefix("")). The PR's Case 3debug_assert_eq!(key1.len(), 1)trips on such nodes — keep that assert — and in release the recursiveengine would misplace the value. Until fixed, path-sensitive cata results on maps mutated by
insert_prefix/graftcannot be trusted, and the randomized cata tests should avoid those operationsat mid-key foci.