Add to_prev_step and to_prev_val iteration methods

benches/binary_keys.rs

@@ -306,6 +306,38 @@ fn binary_zipper_step_iter(bencher: Bencher, n: u64) {
     });
 }
 
+#[divan::bench(args = [50, 100, 200, 400, 800, 1600])]
+fn binary_zipper_prev_iter(bencher: Bencher, n: u64) {
+
+    let keys = make_keys(n as usize, 1);
+    let map: PathMap<usize> = keys.iter().enumerate().map(|(n, s)| (s, n)).collect();
+
+    //Benchmark iterating the values backwards
+    bencher.bench_local(|| {
+        let mut count = 0;
+        let mut zipper = map.read_zipper();
+        while zipper.to_prev_val() {
+            count += 1;
+        }
+        assert_eq!(count, n);
+    });
+}
+
+#[divan::bench(args = [50, 100, 200, 400, 800, 1600])]
+fn binary_zipper_prev_step_iter(bencher: Bencher, n: u64) {
+    let keys = make_keys(n as usize, 1);
+    let map: PathMap<usize> = keys.iter().enumerate().map(|(i, key)| (key, i)).collect();
+
+    bencher.bench_local(|| {
+        let mut steps = 0usize;
+        let mut zipper = map.read_zipper();
+        while zipper.to_prev_step() {
+            steps += 1;
+        }
+        black_box(steps);
+    });
+}
+
 #[divan::bench(sample_size = 1, args = [50, 100, 200, 400, 800, 1600])]
 fn binary_join(bencher: Bencher, n: u64) {
 

benches/sparse_keys.rs

@@ -344,6 +344,46 @@ fn sparse_zipper_step_iter(bencher: Bencher, n: u64) {
     });
 }
 
+#[divan::bench(args = [50, 100, 200, 400, 800, 1600])]
+fn sparse_zipper_prev_cursor(bencher: Bencher, n: u64) {
+
+    let mut r = StdRng::seed_from_u64(1);
+    let keys: Vec<Vec<u8>> = (0..n).into_iter().map(|_| {
+        let len = (r.random::<u8>() % 18) + 3; //length between 3 and 20 chars
+        (0..len).into_iter().map(|_| r.random::<u8>()).collect()
+    }).collect();
+    let map: PathMap<usize> = keys.iter().enumerate().map(|(n, s)| (s, n)).collect();
+
+    //Benchmark using the zipper as a cursor, moving backwards
+    bencher.bench_local(|| {
+        let mut count = 0;
+        let mut zipper = map.read_zipper();
+        while zipper.to_prev_val() {
+            count += 1;
+        }
+        assert_eq!(count, n);
+    });
+}
+
+#[divan::bench(args = [50, 100, 200, 400, 800, 1600])]
+fn sparse_zipper_prev_step_iter(bencher: Bencher, n: u64) {
+    let mut r = StdRng::seed_from_u64(1);
+    let keys: Vec<Vec<u8>> = (0..n).map(|_| {
+        let len = (r.random::<u8>() % 15) + 5;
+        (0..len).map(|_| r.random::<u8>()).collect()
+    }).collect();
+    let map: PathMap<usize> = keys.iter().enumerate().map(|(i, key)| (key, i)).collect();
+
+    bencher.bench_local(|| {
+        let mut steps = 0usize;
+        let mut zipper = map.read_zipper();
+        while zipper.to_prev_step() {
+            steps += 1;
+        }
+        black_box(steps);
+    });
+}
+
 #[divan::bench(args = [10, 20, 40, 80, 160, 320])]
 fn sparse_iter(bencher: Bencher, n: u64) {
 

benches/superdense_keys.rs

@@ -312,6 +312,38 @@ fn superdense_zipper_step_iter(bencher: Bencher, n: u64) {
     });
 }
 
+#[divan::bench(args = [100, 200, 400, 800, 1600, 3200])]
+fn superdense_zipper_prev_cursor(bencher: Bencher, n: u64) {
+
+    let mut map: PathMap<u64> = PathMap::new();
+    for i in 0..n { map.set_val_at(prefix_key(&i), i); }
+
+    //Benchmark using the the zipper as a cursor, moving backwards
+    bencher.bench_local(|| {
+        let mut count = 0;
+        let mut zipper = map.read_zipper();
+        while zipper.to_prev_val() {
+            count += 1;
+        }
+        assert_eq!(count, n);
+    });
+}
+
+#[divan::bench(args = [100, 200, 400, 800, 1600, 3200])]
+fn superdense_zipper_prev_step_iter(bencher: Bencher, n: u64) {
+    let mut map: PathMap<u64> = PathMap::new();
+    for i in 0..n { map.set_val_at(prefix_key(&i), i); }
+
+    bencher.bench_local(|| {
+        let mut steps = 0usize;
+        let mut zipper = map.read_zipper();
+        while zipper.to_prev_step() {
+            steps += 1;
+        }
+        black_box(steps);
+    });
+}
+
 fn prefix_key(k: &u64) -> &[u8] {
     let bs = (8 - k.leading_zeros()/8) as u8;
     let kp: *const u64 = k;

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 = 58;
+pub const NOPS: usize = 60;
 /// 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).
@@ -948,6 +948,15 @@ pub fn run_ops<R: ReadSource>(
                     let _t = get!(d.modn(2));
                     ("descend_last_val", show_bool(rz.descend_last_val()).to_string())
                 }
+                58 => {
+                    let t = get!(d.modn(2));
+                    let r = tgt!(t, wz, *rz, z, z.to_prev_step());
+                    ("to_prev_step", show_bool(r).to_string())
+                }
+                59 => {
+                    let _t = get!(d.modn(2));
+                    ("to_prev_val", show_bool(rz.to_prev_val()).to_string())
+                }
                 47 => {
                     let t = get!(d.modn(2));
                     // The blind-zipper addition: `descend_until` reporting the
@@ -1035,6 +1044,40 @@ mod input_format_tests {
         }
     }
 
+    #[test]
+    fn trace_and_reproducer_decode_reverse_iteration() {
+        let mut bytes = input_header();
+        bytes.extend_from_slice(&[
+            2, 1, 0, 10, 1, 2, 20, // map0: [0], [2].
+            4, 0, 9, 1, 0, 11, 2, 0, 1, 12, 1, 2, 13, // map1: [], [0], [0,1], [2].
+            0, 0, // Zipper roots.
+            0, 0, 3, 3, 3, 3, // Missing write focus [3,3,3].
+            58, 0, 58, 0, 58, 0, 58, 0, // Step backward, exhaust, wrap.
+            57, 1, // Initialize reverse value iteration at [2].
+            59, 1, 59, 1, 59, 1, 59, 1, // Iterate, exhaust at the valued root, wrap.
+        ]);
+        // ACT's known val_count defect prevents --check at a missing focus.
+        for trace in [run(&bytes, true), run_act(&bytes, false)] {
+            for expected in [
+                "1 to_prev_step ret=1 W=02",
+                "2 to_prev_step ret=1 W=00",
+                "3 to_prev_step ret=0 W=_",
+                "4 to_prev_step ret=1 W=02",
+                "5 descend_last_val ret=1",
+                "6 to_prev_val ret=1",
+                "7 to_prev_val ret=1",
+                "8 to_prev_val ret=0",
+                "9 to_prev_val ret=1",
+            ] {
+                assert!(trace.contains(expected), "missing {expected}:\n{trace}");
+            }
+        }
+        let repro = emit_repro(&bytes, 256);
+        assert!(repro.contains("wz.to_prev_step();"));
+        assert!(repro.contains("rz.to_prev_val();"));
+        assert!(repro.contains("rz.descend_last_val();"));
+    }
+
     #[test]
     fn trace_and_reproducer_decode_last_value_descent() {
         let mut bytes = input_header();

differential/src/repro.rs

@@ -217,6 +217,8 @@ pub fn emit_repro(bytes: &[u8], upto: usize) -> String {
                             rs_bytes(&r1), rs_bytes(&p)) }
             56 => { let pr = g!(d.boolean()); format!("wz.remove_subtrie({pr});") }
             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() }
             _ => "// nop".to_string(),
         };
         o.push_str(&format!("    /* {step:3} */ {line}\n"));

lean/PathMapModel/Check.lean

@@ -190,6 +190,28 @@ pruning an already dangling focus does not count as removing content. -/
 #guard allZips.all descendIndexedLands
 #guard allZips.all siblingRoundTrip
 #guard allZips.all toNextValMonotone
+#guard allZips.all toPrevStepMonotone
+#guard allZips.all toPrevValMonotone
+#guard allZips.all stepRoundTrip
+#guard allZips.all valRoundTrip
+
+/-! Reverse traversal skips missing ancestors, stops at existing parents,
+wraps from the root, and stays within a zipper rooted below the map root. -/
+#guard ((zipAt fSide [] [3,3,3]).toPrevStep).2.path == [2]
+#guard ((zipAt fSide [] [0,0,3,3]).toPrevStep).2.path == [0,0]
+#guard ((zipAt fSide [] [0,1,3]).toPrevStep).2.path == [0,0]
+#guard ((zipAt fSide [] []).toPrevStep).2.path == [2]
+#guard !((zipAt fSide [] [0]).toPrevStep).1
+#guard !((zipAt fSide [0,0] [3,3]).toPrevStep).1
+#guard ((zipAt fSide [0] []).toPrevVal).2.path == [2]
+#guard ((zipAt fBranch [] [0,1]).toPrevVal).2.path == [0,0]
+#guard ((zipAt fBranch [] [0,0]).toPrevVal).2.path == [0]
+#guard !((zipAt fBranch [] [0]).toPrevVal).1
+#guard !((zipAt (mk [([], 9)]) [] []).toPrevVal).1
+#guard !((zipAt fEmpty [] []).toPrevStep).1
+#guard !((zipAt fEmpty [] [3,3]).toPrevVal).1
+#guard ((zipAt fDangle [] []).toPrevVal).2.path == [0]
+
 #guard allZips.all descendLastValLands
 
 /-! Last-value descent includes the focus and skips dangling suffixes. -/

lean/PathMapModel/Fuzz.lean

@@ -535,6 +535,12 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do
   | 57 => do let (_, d) ← d.mod 2
              let (r, z) := s.rz.descendLastVal
              some (emit { s with rz := z } "descend_last_val" (showBool r), d)
+  | 58 => do let (t, d) ← d.mod 2
+             let (r, s) := onTarget s t (fun z => z.toPrevStep)
+             some (emit s "to_prev_step" (showBool r), d)
+  | 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)
   | _ => some (emit s "nop" "-", d)
 
 /-- Run operations until the input is exhausted or `fuel` runs out. -/

lean/PathMapModel/Spec.lean

@@ -299,6 +299,35 @@ def toNextValMonotone (z : Zip V) : Bool :=
   let (moved, z') := z.toNextVal
   if moved then Path.lt z.path z'.path && z'.isVal else z'.atRoot
 
+/-- Reverse stepping lands on an existing non-root predecessor, except for
+the initial wrap from the root. Exhaustion returns to the root. -/
+def toPrevStepMonotone (z : Zip V) : Bool :=
+  let (moved, z') := z.toPrevStep
+  if moved then z'.pathExists && !z'.atRoot && (z.atRoot || Path.lt z'.path z.path)
+  else z'.atRoot
+
+/-- Reverse value iteration has the same ordering and boundary as stepping. -/
+def toPrevValMonotone (z : Zip V) : Bool :=
+  let (moved, z') := z.toPrevVal
+  if moved then z'.isVal && !z'.atRoot && (z.atRoot || Path.lt z'.path z.path)
+  else z'.atRoot
+
+/-- Forward then backward returns to an existing non-root starting position. -/
+def stepRoundTrip (z : Zip V) : Bool :=
+  if !z.pathExists || z.atRoot then true
+  else
+    let (moved, next) := z.toNextStep
+    let (back, prev) := next.toPrevStep
+    !moved || (back && prev.path == z.path)
+
+/-- Forward then backward returns to a non-root starting value. -/
+def valRoundTrip (z : Zip V) : Bool :=
+  if !z.isVal || z.atRoot then true
+  else
+    let (moved, next) := z.toNextVal
+    let (back, prev) := next.toPrevVal
+    !moved || (back && prev.path == z.path)
+
 /-- Last-value descent stays within the starting subtree, includes the focus,
 and leaves it unchanged when no value is found. Repeating success is stable. -/
 def descendLastValLands (z : Zip V) : Bool :=

lean/PathMapModel/Zipper.lean

@@ -341,6 +341,14 @@ def toNextStep : Bool × Zip V :=
   | some q => (true, { z with path := q })
   | none => (false, z.reset)
 
+/-- `ZipperMoving::to_prev_step`: the greatest non-root existing location
+strictly before the focus. At the root, wrap to the last non-root location.
+Missing focus paths are allowed; they are never returned as predecessors. -/
+def toPrevStep : Bool × Zip V :=
+  match (z.subPaths.filter (fun q => !q.isEmpty && (z.atRoot || Path.lt q z.path))).getLast? with
+  | some q => (true, { z with path := q })
+  | none => (false, z.reset)
+
 /-! ## `trait ZipperIteration` -/
 
 /-- `ZipperIteration::to_next_val`: the next existing location carrying a value,
@@ -351,6 +359,15 @@ def toNextVal : Bool × Zip V :=
   | some q => (true, { z with path := q })
   | none => (false, z.reset)
 
+/-- `ZipperIteration::to_prev_val`: the greatest non-root valued location
+strictly before the focus, wrapping to the last such value from the root.
+The zipper-root value is excluded, as in `toNextVal`. -/
+def toPrevVal : Bool × Zip V :=
+  match (z.subPaths.filter (fun q => !q.isEmpty && (z.atRoot || Path.lt q z.path) &&
+      (z.trie.valAt (z.root ++ q)).isSome)).getLast? with
+  | some q => (true, { z with path := q })
+  | none => (false, z.reset)
+
 /-- `ZipperReadOnlyIteration::to_next_get_val`. -/
 def toNextGetVal : Option V × Zip V :=
   let (moved, z') := z.toNextVal

lean/README.md

@@ -225,6 +225,13 @@ 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.
+
 Generators always write the current header, using `NOPS` in
 `lean/input_format.py`, which must match `differential/src/harness.rs`.
 Saved failures and shrunken inputs also carry a header, preserving the original

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 = 58
+NOPS = 60
 HEADER_SIZE = len(WIRE_MAGIC) + 2
 
 

pathmap-book/src/1.02.05_zipper_iter.md

@@ -9,11 +9,13 @@ The [`ZipperIteration`] trait extends [`ZipperMoving`] with methods for traversa
 
 - [`descend_last_path`] descends to the last existing path by sort order in the current subtree, whether or not it holds a value. It returns `true` if the focus moved.
 - [`to_next_step`] moves the zipper to the next existing position in the trie structure, regardless of whether it contains a value. Calling this method repeatedly will cycle through through all existing positions in the trie, visiting each position once before visiting any position twice.  If the focus is not at a leaf, this method descends.  If it is at a leaf, it ascends repeatedly until finding a sibling, then moves to that sibling.
+- [`to_prev_step`] moves the zipper to the previous existing position, visiting positions in the exact reverse of the [`to_next_step`] order.  Called at the root, it moves to the last position in the trie.
 
 ### Value Based Iteration
 
 - [`descend_last_val`] moves directly to the position containing the last value, in path sort order, at or below the zipper’s current focus.
 - [`to_next_val`] advances the zipper to the next position containing a value, using depth-first traversal.  Calling this method repeatedly will visit each position containing a value once, before visiting any position twice.
+- [`to_prev_val`] moves the zipper to the previous position containing a value, visiting values in the exact reverse of the [`to_next_val`] order.
 
 ### K-Path Iteration
 The `k_path` methods allow iterating over children at depth `k` relative to the focus (or starting focus).  This enables efficiently visiting all paths at a specific distances from a common root, which is useful for certain algorithmic patterns.  For example, if your trie contains a number of 4-byte data types (e.g. record IDs, etc.), you can visit the subtrie below each one using a `k_path` iteration.

pathmap-book/src/api_links.md

@@ -138,6 +138,8 @@
 [`to_next_val`]: https://docs.rs/pathmap/latest/pathmap/zipper/trait.ZipperIteration.html#tymethod.to_next_val
 [`descend_last_val`]: https://docs.rs/pathmap/latest/pathmap/zipper/trait.ZipperIteration.html#method.descend_last_val
 [`to_prev_sibling_byte`]: https://docs.rs/pathmap/latest/pathmap/zipper/trait.ZipperMoving.html#tymethod.to_prev_sibling_byte
+[`to_prev_step`]: https://docs.rs/pathmap/latest/pathmap/zipper/trait.ZipperMoving.html#method.to_prev_step
+[`to_prev_val`]: https://docs.rs/pathmap/latest/pathmap/zipper/trait.ZipperIteration.html#method.to_prev_val
 [`trie_ref_at_path`]: https://docs.rs/pathmap/latest/pathmap/zipper/trait.ZipperReadOnlySubtries.html#tymethod.trie_ref_at_path
 [`val`]: https://docs.rs/pathmap/latest/pathmap/zipper/trait.ZipperValues.html#tymethod.val
 [`val_at`]: https://docs.rs/pathmap/latest/pathmap/zipper/trait.ZipperValuesAt.html#tymethod.val_at

src/path_tracker.rs

@@ -142,6 +142,9 @@ impl<Z: ZipperMoving> ZipperMoving for PathTracker<Z> {
     fn to_next_step_observed<Obs: PathObserver>(&mut self, obs: &mut Obs) -> bool {
         self.zipper.to_next_step_observed(&mut (&mut self.path, &mut *obs))
     }
+    fn to_prev_step_observed<Obs: PathObserver>(&mut self, obs: &mut Obs) -> bool {
+        self.zipper.to_prev_step_observed(&mut (&mut self.path, &mut *obs))
+    }
     fn to_next_sibling_byte(&mut self) -> Option<u8> {
         let byte = self.zipper.to_next_sibling_byte()?;
         *self.path.last_mut().expect("path must not be empty") = byte;
@@ -161,6 +164,9 @@ impl<Z: ZipperIteration> ZipperIteration for PathTracker<Z> {
     fn to_next_val_observed<Obs: PathObserver>(&mut self, obs: &mut Obs) -> bool {
         self.zipper.to_next_val_observed(&mut (&mut self.path, &mut *obs))
     }
+    fn to_prev_val_observed<Obs: PathObserver>(&mut self, obs: &mut Obs) -> bool {
+        self.zipper.to_prev_val_observed(&mut (&mut self.path, &mut *obs))
+    }
     fn descend_last_path_observed<Obs: PathObserver>(&mut self, obs: &mut Obs) -> bool {
         self.zipper.descend_last_path_observed(&mut (&mut self.path, &mut *obs))
     }