From 287fefd0969f1401545079162874e00cb74e249c Mon Sep 17 00:00:00 2001 From: adamv-symbolica Date: Mon, 2 Nov 2026 18:09:39 +0000 Subject: [PATCH 1/2] Make set_val_at below a focus without a node step into existing children When the write zipper's focus has no child node of its own, `with_node_at_path` joined the focus key and the relative path and handed the whole key to the parent node's `node_set_val` / `node_set_branch`. Those expect a key that doesn't pass through a child, so a child further along the key (e.g. `xa` from earlier writes of `xab` and `xac`) was split around instead of entered. The write then landed beside the existing path, giving a duplicate value or a value the trie can't reach (#175). It now enters such a child, as the root case already does. The branch for a focus key plus path longer than a node key had the same defect inside the subtrie it takes from below the focus, and now walks it the same way. Co-Authored-By: Claude Opus 5.5 --- src/write_zipper.rs | 65 ++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 58 insertions(+), 7 deletions(-) diff --git a/src/write_zipper.rs b/src/write_zipper.rs index 7a5e1206..4ec477af 100644 --- a/src/write_zipper.rs +++ b/src/write_zipper.rs @@ -2626,6 +2626,11 @@ impl <'a, 'path, V: Clone + Send + Sync + Unpin, A: Allocator + 'a> WriteZipperC key_buf[..key.len()].copy_from_slice(key); key_buf[key.len()..key.len()+path.len()].copy_from_slice(path); let full_key = &key_buf[..key.len()+path.len()]; + // No child sits at the focus, but one further along `full_key` may already hold part + // of the path. The node ops expect a key that doesn't pass through a child, so step in. + if let Some((consumed, child_node)) = focus_node.node_get_child_mut(full_key) && consumed < full_key.len() { + return with_node_at_path_mut(child_node, &full_key[consumed..], node_f, retry_f) + } drop(focus_node); self.in_zipper_mut_static_result( |focus_node, _| node_f(focus_node, full_key), @@ -2641,13 +2646,7 @@ impl <'a, 'path, V: Clone + Send + Sync + Unpin, A: Allocator + 'a> WriteZipperC #[cfg(feature = "all_dense_nodes")] { TrieNodeODRc::new_in(crate::dense_byte_node::DenseByteNode::new_in(self.alloc.clone()), self.alloc.clone()) } }); - let result = match node_f(&mut child.make_mut(), path) { - Ok(result) => result, - Err(replacement_node) => { - child = replacement_node; - retry_f(&mut child.make_mut(), path) - }, - }; + let result = with_node_at_path_mut(&mut child, path, node_f, retry_f); drop(focus_node); self.in_zipper_mut_static_result( |node, key| node.node_set_branch(key, child), @@ -7017,6 +7016,58 @@ mod tests { } } + #[test] + fn set_val_at_through_child_below_focus() { + // https://github.com/Adam-Vandervorst/PathMap/issues/175 + let mut map = PathMap::<()>::new(); + { + let mut wz = map.write_zipper(); + wz.descend_to(b"x"); + assert_eq!(wz.set_val_at(b"ab", ()), None); + assert_eq!(wz.set_val_at(b"ac", ()), None); + assert_eq!(wz.set_val_at(b"ab", ()), Some(())); + } + assert_eq!(map.val_count(), 2); + assert_eq!(map.val_at(b"xab"), Some(&())); + assert_eq!(map.val_at(b"xac"), Some(&())); + + let mut map = PathMap::::new(); + { + let mut wz = map.write_zipper(); + wz.descend_to([1u8, 2]); + assert_eq!(wz.set_val_at([3u8, 2], 0), None); + assert_eq!(wz.set_val_at([3u8, 0, 3], 1), None); + assert_eq!(wz.set_val_at([3u8, 2], 2), Some(0)); + assert_eq!(wz.set_val_at([2u8], 3), None); + } + assert_eq!(map.val_count(), 3); + assert_eq!(map.val_at([1u8, 2, 3, 2]), Some(&2)); + assert_eq!(map.val_at([1u8, 2, 3, 0, 3]), Some(&1)); + assert_eq!(map.val_at([1u8, 2, 2]), Some(&3)); + } + + #[test] + fn set_val_at_through_child_below_long_focus() { + // As above, but the last path is long enough that the focus and path don't fit one node key + let focus = [0u8; 40]; + let long_path = b"ab12345678"; + let mut map = PathMap::::new(); + { + let mut wz = map.write_zipper(); + wz.descend_to(&focus); + assert_eq!(wz.set_val_at(b"ab", 0), None); + assert_eq!(wz.set_val_at(b"ac", 1), None); + assert_eq!(wz.set_val_at(long_path, 2), None); + assert_eq!(wz.set_val_at(long_path, 3), Some(2)); + } + assert_eq!(map.val_count(), 3); + for (path, val) in [(&b"ab"[..], 0), (b"ac", 1), (long_path, 3)] { + let mut full_path = focus.to_vec(); + full_path.extend_from_slice(path); + assert_eq!(map.val_at(&full_path), Some(&val)); + } + } + #[test] fn set_val_at_empty_path_sets_focus() { let mut map = PathMap::::new(); From 7f50816ef1751b1c642996d7bcdb13cf18f4d6d7 Mon Sep 17 00:00:00 2001 From: Luke Peterson Date: Mon, 2 Nov 2026 18:47:34 -0700 Subject: [PATCH 2/2] Adding some more tests to exercise edge cases (all pass) Adding set_val_at to lean model --- differential/src/harness.rs | 45 ++++++++++++++++++++++++++++- differential/src/repro.rs | 2 ++ lean/PathMapModel/Check.lean | 1 + lean/PathMapModel/Fuzz.lean | 15 ++++++---- lean/PathMapModel/Spec.lean | 12 ++++++++ lean/PathMapModel/Write.lean | 7 +++++ lean/README.md | 37 ++++++------------------ lean/input_format.py | 2 +- src/write_zipper.rs | 55 ++++++++++++++++++++++++++++++++++++ 9 files changed, 140 insertions(+), 36 deletions(-) diff --git a/differential/src/harness.rs b/differential/src/harness.rs index 39c1446a..c2863849 100644 --- a/differential/src/harness.rs +++ b/differential/src/harness.rs @@ -26,7 +26,7 @@ use core::fmt::Write as _; /// Selector count for newly generated inputs. Keep in sync with `lean/input_format.py`. /// Keep operation IDs permanently assigned. -pub const NOPS: usize = 60; +pub const NOPS: usize = 61; /// Unversioned inputs retain their original operation decoding. pub const LEGACY_NOPS: usize = 56; /// Input header marker, followed by a little-endian u16 selector count (1..=256). @@ -957,6 +957,11 @@ pub fn run_ops( let _t = get!(d.modn(2)); ("to_prev_val", show_bool(rz.to_prev_val()).to_string()) } + 60 => { + let p = get!(d.path(6)); + let v = get!(d.u8()) as u64; + ("set_val_at", show_val(wz.set_val_at(&p, v).as_ref())) + } 47 => { let t = get!(d.modn(2)); // The blind-zipper addition: `descend_until` reporting the @@ -1044,6 +1049,44 @@ mod input_format_tests { } } + #[test] + fn trace_and_reproducer_decode_relative_writes() { + let mut bytes = input_header(); + bytes.extend_from_slice(&[ + 0, 0, 0, 0, // Empty maps and zipper roots. + 0, 0, 1, 1, // Descend the write zipper to [1]. + 60, 2, 0, 1, 0, // [0,1] := 0. + 60, 2, 0, 2, 1, // [0,2] := 1. + 60, 2, 0, 1, 2, // [0,1] := 2, replacing 0 (issue #175). + 60, 0, 9, 60, 0, 10, // Empty path writes the focus, then replaces it. + 60, 2, 3, // Truncated path must not execute a write. + ]); + for trace in [run(&bytes, true), run_act(&bytes, false)] { + for expected in [ + "1 set_val_at ret=- W=01", + "2 set_val_at ret=- W=01", + "3 set_val_at ret=0 W=01", + "4 set_val_at ret=- W=01", + "5 set_val_at ret=9 W=01", + "MAP0 _:-,01:10,0100:-,010001:2,010002:1", + ] { + assert!(trace.contains(expected), "missing {expected}:\n{trace}"); + } + assert!(!trace.contains("6 set_val_at"), "{trace}"); + } + let repro = emit_repro(&bytes, 256); + assert!(repro.contains("wz.set_val_at(&[0u8, 1], 2);"), "{repro}"); + assert!(repro.contains("wz.set_val_at(&[], 10);"), "{repro}"); + + // With 60 selectors, byte 60 remains descend_to (op 0), not a write. + let mut old = WIRE_MAGIC.to_vec(); + old.extend_from_slice(&60u16.to_le_bytes()); + old.extend_from_slice(&[0, 0, 0, 0, 60, 0, 1, 2]); + let trace = run(&old, true); + assert!(trace.contains("0 descend_to"), "{trace}"); + assert!(!trace.contains("set_val_at"), "{trace}"); + } + #[test] fn trace_and_reproducer_decode_reverse_iteration() { let mut bytes = input_header(); diff --git a/differential/src/repro.rs b/differential/src/repro.rs index aaf31a32..98bc1fba 100644 --- a/differential/src/repro.rs +++ b/differential/src/repro.rs @@ -219,6 +219,8 @@ pub fn emit_repro(bytes: &[u8], upto: usize) -> String { 57 => { let _t = g!(d.modn(2)); "rz.descend_last_val();".to_string() } 58 => { let t = g!(d.modn(2)); format!("{}.to_prev_step();", z!(t)) } 59 => { let _t = g!(d.modn(2)); "rz.to_prev_val();".to_string() } + 60 => { let p = g!(d.path(6)); let v = g!(d.u8()) as u64; + format!("wz.set_val_at({}, {v});", rs_bytes(&p)) } _ => "// nop".to_string(), }; o.push_str(&format!(" /* {step:3} */ {line}\n")); diff --git a/lean/PathMapModel/Check.lean b/lean/PathMapModel/Check.lean index e1a6ef9e..d3213b0a 100644 --- a/lean/PathMapModel/Check.lean +++ b/lean/PathMapModel/Check.lean @@ -228,6 +228,7 @@ wraps from the root, and stays within a zipper rooted below the map root. -/ #guard ((zipAt fSide [] [3,3]).descendLastVal).2.path == [3,3] #guard allZips.all (fun z => probes.all (descendToExistingLands z)) #guard allZips.all (fun z => setValThenVal ops z 42) +#guard allZips.all (fun z => probes.all (fun p => setValAtAgrees ops z p 42)) #guard allZips.all (takeThenGraft ops) #guard allZips.all (joinEmptyIdentity ops) #guard allZips.all (joinSelfIdentity ops) diff --git a/lean/PathMapModel/Fuzz.lean b/lean/PathMapModel/Fuzz.lean index 4ed000e0..99091931 100644 --- a/lean/PathMapModel/Fuzz.lean +++ b/lean/PathMapModel/Fuzz.lean @@ -14,6 +14,10 @@ divergence shows up as a textual diff. The input is consumed one byte at a time; decoding stops (and the program ends) as soon as the input runs out. +Versioned inputs start with the eight bytes `PMFUZZ\x01\x00` and a +little-endian u16 selector count (1..=256). Headerless inputs use 56 selectors. +Both forms then decode the same map/zipper header and operations: + ``` header: n := u8 % 8 -- entries seeded into map0 (the write target) @@ -23,14 +27,9 @@ header: r0 := u8 % 4 ; r0 × pathbyte -- write zipper root r1 := u8 % 4 ; r1 × pathbyte -- read zipper root body: - repeated: op := u8 % 56 ; operands per op (see `step`) + repeated: op := u8 % selectors ; operands per op (see `step`) ``` -Inputs prefixed with `PMFUZZ\x01\x00` followed by a little-endian u16 selector -count (1..=256) use the same map/zipper header but decode operations modulo that -recorded count. Headerless inputs use 56. Operation 56 is `remove_subtrie`, -followed by a prune byte. - Every **path byte** is masked to `b % 4`, so the generated tries share prefixes heavily — that is where the interesting trie shapes (branch points, dangling chains, single-child runs) live. @@ -541,6 +540,10 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do | 59 => do let (_, d) ← d.mod 2 let (r, z) := s.rz.toPrevVal some (emit { s with rz := z } "to_prev_val" (showBool r), d) + | 60 => do let (p, d) ← d.path + let (v, d) ← d.u8 + let (old, z) := s.wz.setValAt p (UInt64.ofNat v.toNat) + some (emit { s with wz := z } "set_val_at" (showVal old), d) | _ => some (emit s "nop" "-", d) /-- Run operations until the input is exhausted or `fuel` runs out. -/ diff --git a/lean/PathMapModel/Spec.lean b/lean/PathMapModel/Spec.lean index 8e5294f8..b3a6d527 100644 --- a/lean/PathMapModel/Spec.lean +++ b/lean/PathMapModel/Spec.lean @@ -56,6 +56,14 @@ theorem descendTo_append (a b : Path) : theorem focus_descendTo (k : Path) : (z.descendTo k).focus = z.focus ++ k := by simp [focus, descendTo, List.append_assoc] +@[simp] theorem path_setValAt (p : Path) (v : V) : (z.setValAt p v).2.path = z.path := rfl + +@[simp] theorem root_setValAt (p : Path) (v : V) : (z.setValAt p v).2.root = z.root := rfl + +/-- Writing an empty relative path is exactly writing the focus. -/ +@[simp] theorem setValAt_nil (v : V) : z.setValAt [] v = z.setVal v := by + simp [setValAt, setVal] + /-- `origin_path = root_prefix_path ++ path`, as documented on `ZipperAbsolutePath`. -/ theorem origin_eq_root_append_path : z.rootPrefixPath ++ z.path = z.focus := rfl @@ -226,6 +234,10 @@ def setValThenVal (ops : ValOps V) (z : Zip V) (v : V) : Bool := | .valued w => ops.beq w v | .bare | .absent => false +/-- A relative write produces the same trie as descending and setting there. -/ +def setValAtAgrees (ops : ValOps V) (z : Zip V) (p : Path) (v : V) : Bool := + PathMap.beqT ops (z.setValAt p v).2.trie ((z.descendTo p).setVal v).2.trie + /-- `remove_val` clears the value but leaves the location dangling — which is to say the focus ends up exactly `.bare`. -/ def removeValLeavesPath (z : Zip V) : Bool := diff --git a/lean/PathMapModel/Write.lean b/lean/PathMapModel/Write.lean index 7f6f5ad4..b0f18952 100644 --- a/lean/PathMapModel/Write.lean +++ b/lean/PathMapModel/Write.lean @@ -41,6 +41,13 @@ def setVal (v : V) : Option V × Zip V := let (old, t) := z.trie.setVal z.focus v (old, z.withTrie t) +/-- `ZipperWriting::set_val_at`: set the value at a path relative to the focus, +creating it if absent and returning the replaced value. The cursor and zipper +root stay fixed; an empty path writes the focus itself. -/ +def setValAt (p : Path) (v : V) : Option V × Zip V := + let (old, t) := z.trie.setVal (z.focus ++ p) v + (old, z.withTrie t) + /-- Writing through the reference `get_val_mut` returns. Specified as: when there is a value, this is `set_val`; when there is not, it is diff --git a/lean/README.md b/lean/README.md index 39fc0868..e6827ae3 100644 --- a/lean/README.md +++ b/lean/README.md @@ -200,7 +200,10 @@ into a program over two maps and two zippers — `wz` writing into map 0, `rz` reading map 1, kept in separate maps so the real crate can hold both at once. ``` -header: +version header (new inputs only): + magic := "PMFUZZ\x01\x00" -- eight bytes + selectors := u16le -- 1 through 256 +map/zipper header: n := u8 % 8 -- entries seeded into map0 n × ( len := u8 % 6 ; len × pathbyte ; val := u8 ) n := u8 % 8 -- entries seeded into map1 @@ -208,29 +211,13 @@ header: r0 := u8 % 4 ; r0 × pathbyte -- write zipper root r1 := u8 % 4 ; r1 × pathbyte -- read zipper root body: - repeated: op := u8 % 56 ; operands per op + repeated: op := u8 % selectors ; operands per op ``` -This is the headerless format, whose selector count is permanently 56. New -inputs start with the eight bytes `PMFUZZ\x01\x00`, then a little-endian u16 -selector count (1 through 256), followed by the same map/zipper header. Operation -bytes are reduced modulo the recorded count, independently of the running -software's operation table. Truncated headers and invalid counts are rejected. -Readers auto-detect this format by the magic string; inputs without it use the -legacy selector count of 56. -Operation 56 is `remove_subtrie`, with one boolean prune operand. -Operation 57 is `descend_last_val`. It consumes a target byte and always uses -the read zipper, like `to_next_val`. -The model selects the greatest valued path in the starting subtree, including -the focus itself. Success means a value was found, even without movement; -failure leaves the focus unchanged. - -Operations 58 and 59 are `to_prev_step` and `to_prev_val`, each with a target -byte. Stepping can target either zipper; value iteration always uses the read -zipper, matching `to_next_val`. The model selects the greatest existing -non-root path (or valued path) strictly before the focus, wrapping from the -root to the last such location. Nonexistent starting paths are allowed; -exhaustion returns `false` at the zipper root, even when it holds a value. +Readers detect the version header by its magic bytes and reject truncated +headers or invalid selector counts. Headerless inputs use 56 selectors. +Each input's selector count controls decoding independently of the running +software's operation table. Generators always write the current header, using `NOPS` in `lean/input_format.py`, which must match `differential/src/harness.rs`. @@ -252,12 +239,6 @@ is a textual diff. The op table lives in `Fuzz.lean` (`PathMapModel.Fuzz.step`) and `differential/src/harness.rs`; **the two must be changed together.** -`Zip.removeSubtrie` clears the focus value and all descendants, then optionally -prunes. Its boolean result counts removal of a value or branch, including a -dangling descendant, but not pruning an already dangling focus. Build-time -checks cover removal, unrelated content, cursor stability, and the zipper-root -bound; differential operation 56 exercises the optimized Rust implementation. - ### Front ends | binary | drives | built with | diff --git a/lean/input_format.py b/lean/input_format.py index 32a928db..3333335f 100644 --- a/lean/input_format.py +++ b/lean/input_format.py @@ -3,7 +3,7 @@ WIRE_MAGIC = b"PMFUZZ\x01\x00" LEGACY_NOPS = 56 # Keep in sync with NOPS in differential/src/harness.rs. -NOPS = 60 +NOPS = 61 HEADER_SIZE = len(WIRE_MAGIC) + 2 diff --git a/src/write_zipper.rs b/src/write_zipper.rs index 4ec477af..bde799aa 100644 --- a/src/write_zipper.rs +++ b/src/write_zipper.rs @@ -7068,6 +7068,61 @@ mod tests { } } + #[test] + fn set_val_at_through_shared_child_keeps_clone_unchanged() { + let mut map = PathMap::::new(); + { + let mut wz = map.write_zipper(); + wz.descend_to(b"x"); + wz.set_val_at(b"ab", 0); + wz.set_val_at(b"ac", 1); + } + let snapshot = map.clone(); + { + let mut wz = map.write_zipper(); + wz.descend_to(b"x"); + assert_eq!(wz.set_val_at(b"ab", 2), Some(0)); + assert_eq!(wz.set_val_at(b"ad", 3), None); + assert_eq!(wz.path(), b"x"); + } + assert_eq!(map.val_count(), 3); + assert_eq!(map.val_at(b"xab"), Some(&2)); + assert_eq!(map.val_at(b"xac"), Some(&1)); + assert_eq!(map.val_at(b"xad"), Some(&3)); + assert_eq!(snapshot.val_count(), 2); + assert_eq!(snapshot.val_at(b"xab"), Some(&0)); + assert_eq!(snapshot.val_at(b"xac"), Some(&1)); + assert_eq!(snapshot.val_at(b"xad"), None); + } + + #[test] + fn set_val_at_through_child_at_node_key_length_boundary() { + let focus = [0u8; 40]; + for combined_len in [MAX_NODE_KEY_BYTES, MAX_NODE_KEY_BYTES + 1] { + let mut path = b"ab".to_vec(); + path.resize(combined_len - focus.len(), b'1'); + let mut map = PathMap::::new(); + { + let mut wz = map.write_zipper(); + wz.descend_to(&focus); + assert_eq!(wz.set_val_at(b"ab", 0), None); + assert_eq!(wz.set_val_at(b"ac", 1), None); + assert_eq!(wz.set_val_at(&path, 2), None); + assert_eq!(wz.set_val_at(&path, 3), Some(2)); + assert_eq!(wz.path(), focus); + assert_eq!(wz.val_at(b"ab"), Some(&0)); + assert_eq!(wz.val_at(b"ac"), Some(&1)); + assert_eq!(wz.val_at(&path), Some(&3)); + } + assert_eq!(map.val_count(), 3); + for (suffix, val) in [(&b"ab"[..], 0), (b"ac", 1), (&path, 3)] { + let mut full_path = focus.to_vec(); + full_path.extend_from_slice(suffix); + assert_eq!(map.val_at(&full_path), Some(&val)); + } + } + } + #[test] fn set_val_at_empty_path_sets_focus() { let mut map = PathMap::::new();