Fix set_val_at #175

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<R: ReadSource>(
                     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();

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"));

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)

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. -/

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 :=

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

lean/README.md

@@ -200,37 +200,24 @@ 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
   n × ( len := u8 % 6 ; len × pathbyte ; val := u8 )
   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 |

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
 
 

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,113 @@ 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::<u64>::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::<u64>::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_through_shared_child_keeps_clone_unchanged() {
+        let mut map = PathMap::<u64>::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::<u64>::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::<u64>::new();