From 7ab374154a7825aff714b6249bb34d7d10ebd8b4 Mon Sep 17 00:00:00 2001
From: anyingiit <49945850+anyingiit@users.noreply.github.com>
Date: Fri, 23 Oct 2026 02:36:03 +0800
Subject: [PATCH 1/2] Add to_prev_step and to_prev_val iteration methods

Add default implementations of ZipperMoving::to_prev_step and
ZipperIteration::to_prev_val (plus their _observed forms), which visit
positions / values in the exact reverse of to_next_step / to_next_val.
Called at the root they move to the last position / value in the trie,
and they return false once they are back at the root.

The new methods are forwarded through the zipper lens macro and
PathTracker, covered by the shared zipper_moving_tests and
zipper_iteration_tests suites, documented in the book, and benchmarked
in the binary_keys, sparse_keys and superdense_keys benches.

Closes #120
---
 benches/binary_keys.rs                  |  32 ++++
 benches/sparse_keys.rs                  |  40 +++++
 benches/superdense_keys.rs              |  32 ++++
 pathmap-book/src/1.02.05_zipper_iter.md |   2 +
 pathmap-book/src/api_links.md           |   2 +
 src/path_tracker.rs                     |   6 +
 src/zipper.rs                           | 196 ++++++++++++++++++++++++
 7 files changed, 310 insertions(+)

diff --git a/benches/binary_keys.rs b/benches/binary_keys.rs
index 664d2528..dbfd3e83 100644
--- a/benches/binary_keys.rs
+++ b/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) {
 
diff --git a/benches/sparse_keys.rs b/benches/sparse_keys.rs
index 5fe692ea..265f9d4a 100644
--- a/benches/sparse_keys.rs
+++ b/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) {
 
diff --git a/benches/superdense_keys.rs b/benches/superdense_keys.rs
index 7a56ffef..97d2ae48 100644
--- a/benches/superdense_keys.rs
+++ b/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;
diff --git a/pathmap-book/src/1.02.05_zipper_iter.md b/pathmap-book/src/1.02.05_zipper_iter.md
index 672ce55d..c5b28b16 100644
--- a/pathmap-book/src/1.02.05_zipper_iter.md
+++ b/pathmap-book/src/1.02.05_zipper_iter.md
@@ -8,10 +8,12 @@ The [`ZipperIteration`] trait extends [`ZipperMoving`] to provides methods for t
 ### Path-Byte Based Iteration
 
 - [`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
 
 - [`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.
diff --git a/pathmap-book/src/api_links.md b/pathmap-book/src/api_links.md
index 373c83d7..7b3fd37e 100644
--- a/pathmap-book/src/api_links.md
+++ b/pathmap-book/src/api_links.md
@@ -134,6 +134,8 @@
 [`to_next_step`]: https://docs.rs/pathmap/latest/pathmap/zipper/trait.ZipperIteration.html#tymethod.to_next_step
 [`to_next_val`]: https://docs.rs/pathmap/latest/pathmap/zipper/trait.ZipperIteration.html#tymethod.to_next_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
diff --git a/src/path_tracker.rs b/src/path_tracker.rs
index c646c31f..47486a7a 100644
--- a/src/path_tracker.rs
+++ b/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))
     }
diff --git a/src/zipper.rs b/src/zipper.rs
index d87d8395..aaffb376 100644
--- a/src/zipper.rs
+++ b/src/zipper.rs
@@ -508,6 +508,49 @@ pub trait ZipperMoving: Zipper {
         }
         true
     }
+
+    /// Convenience form of [`ZipperMoving::to_prev_step_observed`] that does not observe path movement.
+    fn to_prev_step(&mut self) -> bool {
+        self.to_prev_step_observed(&mut ())
+    }
+
+    /// Moves the zipper to the previous existing path within the trie, visiting every path in the exact
+    /// reverse of the order used by [`to_next_step`](ZipperMoving::to_next_step), and reporting movement to `obs`.
+    ///
+    /// Returns `true` if the position of the zipper has moved, or `false` if the zipper has returned
+    /// to the root.  Called at the root, this method moves to the last path in the trie (the end of
+    /// the path found by [`descend_last_byte`](ZipperMoving::descend_last_byte) repeatedly), so calling
+    /// it repeatedly cycles through all existing positions, like `to_next_step`.
+    ///
+    /// If the focus has a previous sibling, this method moves to that sibling and then descends its last
+    /// child at each level until it reaches a leaf.  Otherwise it ascends one byte.
+    ///
+    /// `obs` is notified of every movement made, so a caller can track the zipper's location without
+    /// the zipper needing to maintain a path buffer of its own.  Pass `&mut ()` to discard them.
+    fn to_prev_step_observed<Obs: PathObserver>(&mut self, obs: &mut Obs) -> bool {
+        if !self.at_root() {
+            match self.to_prev_sibling_byte() {
+                Some(byte) => {
+                    //A sibling step replaces the last byte rather than adding one, so the
+                    //observer sees the old byte retracted before the new one arrives.
+                    obs.ascend(1);
+                    obs.descend_to_byte(byte);
+                },
+                None => {
+                    self.ascend_byte();
+                    obs.ascend(1);
+                    return !self.at_root()
+                }
+            }
+        } else if self.child_count() == 0 {
+            return false
+        }
+        //Descend to the last leaf below the focus, which is the predecessor in depth-first order
+        while let Some(byte) = self.descend_last_byte() {
+            obs.descend_to_byte(byte);
+        }
+        true
+    }
 }
 
 /// Receives notifications about the movements a [Zipper] makes, so a caller can track the
@@ -974,6 +1017,56 @@ pub trait ZipperIteration: ZipperMoving {
         }
     }
 
+    /// Convenience form of [`ZipperIteration::to_prev_val_observed`] that does not observe path movement.
+    fn to_prev_val(&mut self) -> bool {
+        self.to_prev_val_observed(&mut ())
+    }
+
+    /// Systematically moves to the previous value accessible from the zipper, visiting values in the
+    /// exact reverse of the order used by [`to_next_val`](ZipperIteration::to_next_val), and reporting
+    /// movement to `obs`.
+    ///
+    /// Returns `true` if the zipper is positioned at the previous value, or `false` if the zipper has
+    /// encountered the root.  Called at the root, this method moves to the last value in the trie.
+    ///
+    /// `obs` is notified of every movement made, so a caller can track the zipper's location without
+    /// the zipper needing to maintain a path buffer of its own.  Pass `&mut ()` to discard them.
+    fn to_prev_val_observed<Obs: PathObserver>(&mut self, obs: &mut Obs) -> bool {
+        //This walks the same positions as repeated calls to `to_prev_step`, but uses
+        //`descend_last_path` to reach the last leaf below a subtrie in one call
+        if self.at_root() {
+            if !self.descend_last_path_observed(obs) {
+                return false
+            }
+            if self.is_val() {
+                return true
+            }
+        }
+        loop {
+            match self.to_prev_sibling_byte() {
+                Some(byte) => {
+                    //A sibling step replaces the last byte rather than adding one, so the
+                    //observer sees the old byte retracted before the new one arrives.
+                    obs.ascend(1);
+                    obs.descend_to_byte(byte);
+                    self.descend_last_path_observed(obs);
+                },
+                None => {
+                    if !self.ascend_byte() {
+                        return false
+                    }
+                    obs.ascend(1);
+                    if self.at_root() {
+                        return false
+                    }
+                }
+            }
+            if self.is_val() {
+                return true
+            }
+        }
+    }
+
     /// Convenience form of [`ZipperIteration::descend_last_path_observed`] that does not observe path movement.
     fn descend_last_path(&mut self) -> bool {
         self.descend_last_path_observed(&mut ())
@@ -1285,6 +1378,7 @@ use zipper_priv::*;
 macro_rules! zipper_impl_lens {
     (ZipperIteration $s: ident => $e:expr) => {
         fn to_next_val_observed<Obs: PathObserver>(&mut $s, obs: &mut Obs) -> bool { $e.to_next_val_observed(obs) }
+        fn to_prev_val_observed<Obs: PathObserver>(&mut $s, obs: &mut Obs) -> bool { $e.to_prev_val_observed(obs) }
         fn descend_last_path_observed<Obs: PathObserver>(&mut $s, obs: &mut Obs) -> bool { $e.descend_last_path_observed(obs) }
         fn descend_first_k_path_observed<Obs: PathObserver>(&mut $s, k: usize, obs: &mut Obs) -> bool { $e.descend_first_k_path_observed(k, obs) }
         fn to_next_k_path_observed<Obs: PathObserver>(&mut $s, k: usize, obs: &mut Obs) -> bool { $e.to_next_k_path_observed(k, obs) }
@@ -1341,6 +1435,7 @@ macro_rules! zipper_impl_lens {
         fn ascend_until(&mut $s) -> usize { $e.ascend_until() }
         fn ascend_until_branch(&mut $s) -> usize { $e.ascend_until_branch() }
         fn to_next_step_observed<Obs: PathObserver>(&mut $s, obs: &mut Obs) -> bool { $e.to_next_step_observed(obs) }
+        fn to_prev_step_observed<Obs: PathObserver>(&mut $s, obs: &mut Obs) -> bool { $e.to_prev_step_observed(obs) }
     };
     (ZipperInfallibleSubtries $s: ident => $e:expr) => {
         fn make_map(&$s) -> crate::PathMap<V, A> { $e.make_map() }
@@ -3840,6 +3935,12 @@ pub(crate) mod zipper_moving_tests {
                     crate::zipper::zipper_moving_tests::run_test(&mut temp_store, $make_z, &[], crate::zipper::zipper_moving_tests::to_next_step_test1)
                 }
 
+                #[test]
+                fn [<$z_name _to_prev_step_test1>]() {
+                    let mut temp_store = $read_keys(crate::zipper::zipper_moving_tests::ZIPPER_TO_NEXT_STEP_TEST1_KEYS);
+                    crate::zipper::zipper_moving_tests::run_test(&mut temp_store, $make_z, &[], crate::zipper::zipper_moving_tests::to_prev_step_test1)
+                }
+
                 #[test]
                 fn [<$z_name _zipper_byte_iter_test1>]() {
                     let mut temp_store = $read_keys(crate::zipper::zipper_moving_tests::ZIPPER_BYTES_ITER_TEST1_KEYS);
@@ -4660,6 +4761,43 @@ pub(crate) mod zipper_moving_tests {
         }
     }
 
+    /// `to_prev_step` must visit exactly the positions `to_next_step` visits, in reverse order, and
+    /// return `false` once it is back at the root
+    pub fn to_prev_step_test1<Z: ZipperMoving + ZipperPath>(mut zipper: Z) {
+        let mut forward = vec![];
+        while zipper.to_next_step() {
+            forward.push(zipper.path().to_vec());
+        }
+        assert!(zipper.at_root());
+        assert_eq!(forward.len(), 43);
+
+        let mut backward = vec![];
+        let mut observed = Vec::<u8>::new();
+        while zipper.to_prev_step_observed(&mut observed) {
+            assert_eq!(&observed[..], zipper.path(), "observer disagreed with path at step {}", backward.len());
+            backward.push(zipper.path().to_vec());
+        }
+        assert!(zipper.at_root());
+        assert_eq!(observed.len(), 0);
+        backward.reverse();
+        assert_eq!(forward, backward);
+
+        //Stepping back from the middle of a traversal
+        zipper.descend_to(b"romu");
+        assert!(zipper.to_prev_step());
+        assert_eq!(zipper.path(), b"romanus");
+        assert!(zipper.to_prev_step());
+        assert_eq!(zipper.path(), b"romanu");
+        zipper.reset();
+        zipper.descend_to(b"rom");
+        assert!(zipper.to_prev_step());
+        assert_eq!(zipper.path(), b"ro");
+        zipper.reset();
+        zipper.descend_to(b"a");
+        assert!(!zipper.to_prev_step());
+        assert!(zipper.at_root());
+    }
+
     pub const ZIPPER_BYTES_ITER_TEST1_KEYS: &[&[u8]] = &[b"ABCDEFGHIJKLMNOPQRSTUVWXYZ", b"ab",];
 
     pub fn zipper_byte_iter_test1<Z: ZipperMoving + ZipperPath>(mut zipper: Z) {
@@ -4824,6 +4962,20 @@ pub(crate) mod zipper_iteration_tests {
                     crate::zipper::zipper_iteration_tests::run_test(&mut temp_store, $make_z, &[], crate::zipper::zipper_iteration_tests::zipper_iter_test1)
                 }
 
+                #[test]
+                fn [<$z_name _zipper_prev_iter_test1>]() {
+                    let mut temp_store = $read_keys(crate::zipper::zipper_iteration_tests::ZIPPER_ITER_TEST1_KEYS);
+                    crate::zipper::zipper_iteration_tests::run_test(&mut temp_store, $make_z, &[], crate::zipper::zipper_iteration_tests::zipper_prev_iter_test1)
+                }
+
+                #[test]
+                fn [<$z_name _zipper_prev_iter_test2>]() {
+                    let paths = crate::zipper::zipper_iteration_tests::zipper_iter_test2_paths();
+                    let path_refs: Vec<&[u8]> = paths.iter().map(|path| &path[..]).collect();
+                    let mut temp_store = $read_keys(&path_refs[..]);
+                    crate::zipper::zipper_iteration_tests::run_test(&mut temp_store, $make_z, b"in", crate::zipper::zipper_iteration_tests::zipper_prev_iter_test2)
+                }
+
                 #[test]
                 fn [<$z_name _zipper_iter_test2>]() {
                     let paths = crate::zipper::zipper_iteration_tests::zipper_iter_test2_paths();
@@ -4950,6 +5102,50 @@ pub(crate) mod zipper_iteration_tests {
         assert_eq!(idx, keys.len());
     }
 
+    /// Calls `to_prev_val` over the whole trie, ensuring all paths are visited exactly once, in the
+    /// reverse of the `to_next_val` order
+    pub fn zipper_prev_iter_test1<'a, Z: ZipperIteration + ZipperPath>(mut zipper: Z) {
+        let keys = ZIPPER_ITER_TEST1_KEYS;
+
+        let mut idx = keys.len();
+        let mut observed = Vec::<u8>::new();
+        while zipper.to_prev_val_observed(&mut observed) {
+            assert!(idx > 0, "to_prev_val visited more values than exist");
+            idx -= 1;
+            assert_eq!(keys[idx], zipper.path());
+            assert_eq!(&observed[..], zipper.path(), "observer disagreed with path at value {idx}");
+        }
+        assert_eq!(idx, 0);
+        assert!(zipper.at_root());
+
+        //A value that has descendants ("roman") comes before them, so stepping back from one of them
+        //lands on it, and stepping back from it lands on the previous sibling subtree's last value
+        zipper.descend_to(b"romane");
+        assert!(zipper.to_prev_val());
+        assert_eq!(zipper.path(), b"roman");
+        assert!(zipper.to_prev_val());
+        assert_eq!(zipper.path(), b"rom'i");
+
+        //Alternating directions returns to the same value
+        assert!(zipper.to_next_val());
+        assert_eq!(zipper.path(), b"roman");
+        assert!(zipper.to_prev_val());
+        assert_eq!(zipper.path(), b"rom'i");
+    }
+
+    pub fn zipper_prev_iter_test2<'a, Z: ZipperIteration + ZipperPath>(mut zipper: Z) {
+        //Iterating backwards using a zipper that has a root that is not the map root
+        let mut count: usize = ZIPPER_ITER_TEST2_COUNT;
+        let mut observed = Vec::<u8>::new();
+        while zipper.to_prev_val_observed(&mut observed) {
+            assert_eq!(zipper.is_val(), true);
+            count -= 1;
+            assert_eq!(zipper.path(), count.to_be_bytes());
+            assert_eq!(&observed[..], zipper.path(), "observer disagreed with path at value {count}");
+        }
+        assert_eq!(count, 0);
+    }
+
     const ZIPPER_ITER_TEST2_COUNT: usize = 32;
     pub fn zipper_iter_test2_paths() -> Vec<Vec<u8>> {
         (0usize..ZIPPER_ITER_TEST2_COUNT).into_iter().map(|i| {

From 76a744e2077f2c709209e54f8d20b872dfdec0f4 Mon Sep 17 00:00:00 2001
From: Luke Peterson <luke@infoplatter.com>
Date: Thu, 22 Oct 2026 21:29:41 -0600
Subject: [PATCH 2/2] Fixing the way non-existent starting paths are handled by
 to_prev_step Adding lean descriptions and harness entries for the methods

---
 differential/src/harness.rs   | 45 +++++++++++++++++-
 differential/src/repro.rs     |  2 +
 lean/PathMapModel/Check.lean  | 22 +++++++++
 lean/PathMapModel/Fuzz.lean   |  6 +++
 lean/PathMapModel/Spec.lean   | 29 ++++++++++++
 lean/PathMapModel/Zipper.lean | 17 +++++++
 lean/README.md                |  7 +++
 lean/input_format.py          |  2 +-
 src/zipper.rs                 | 88 ++++++++++++++++++++++++++---------
 9 files changed, 194 insertions(+), 24 deletions(-)

diff --git a/differential/src/harness.rs b/differential/src/harness.rs
index 796b1740..39c1446a 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 = 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();
diff --git a/differential/src/repro.rs b/differential/src/repro.rs
index 5fa6ca2e..aaf31a32 100644
--- a/differential/src/repro.rs
+++ b/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"));
diff --git a/lean/PathMapModel/Check.lean b/lean/PathMapModel/Check.lean
index ef528266..e1a6ef9e 100644
--- a/lean/PathMapModel/Check.lean
+++ b/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. -/
diff --git a/lean/PathMapModel/Fuzz.lean b/lean/PathMapModel/Fuzz.lean
index 7b10f38c..4ed000e0 100644
--- a/lean/PathMapModel/Fuzz.lean
+++ b/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. -/
diff --git a/lean/PathMapModel/Spec.lean b/lean/PathMapModel/Spec.lean
index 7084f8eb..8e5294f8 100644
--- a/lean/PathMapModel/Spec.lean
+++ b/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 :=
diff --git a/lean/PathMapModel/Zipper.lean b/lean/PathMapModel/Zipper.lean
index 6317c5c5..d6d2799f 100644
--- a/lean/PathMapModel/Zipper.lean
+++ b/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
diff --git a/lean/README.md b/lean/README.md
index ba303a31..39fc0868 100644
--- a/lean/README.md
+++ b/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
diff --git a/lean/input_format.py b/lean/input_format.py
index 92af37ec..32a928db 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 = 58
+NOPS = 60
 HEADER_SIZE = len(WIRE_MAGIC) + 2
 
 
diff --git a/src/zipper.rs b/src/zipper.rs
index 4087319b..8e60216f 100644
--- a/src/zipper.rs
+++ b/src/zipper.rs
@@ -471,8 +471,10 @@ pub trait ZipperMoving: Zipper {
     /// Advances the zipper to visit every existing path within the trie in a depth-first order,
     /// reporting movement to `obs`.
     ///
-    /// Returns `true` if the position of the zipper has moved, or `false` if the zipper has returned
-    /// to the root
+    /// Returns `false` when zipper has returned to the zipper’s root, otherwise `true`. If the zipper's
+    /// focus is on a non-existent path, this method moves to the next existing path in the sequence of
+    /// existing paths.
+    ///
     /// `obs` is notified of every movement made, so a caller can track the zipper's location without
     /// the zipper needing to maintain a path buffer of its own.  Pass `&mut ()` to discard them.
     fn to_next_step_observed<Obs: PathObserver>(&mut self, obs: &mut Obs) -> bool {
@@ -517,33 +519,43 @@ pub trait ZipperMoving: Zipper {
     /// Moves the zipper to the previous existing path within the trie, visiting every path in the exact
     /// reverse of the order used by [`to_next_step`](ZipperMoving::to_next_step), and reporting movement to `obs`.
     ///
-    /// Returns `true` if the position of the zipper has moved, or `false` if the zipper has returned
-    /// to the root.  Called at the root, this method moves to the last path in the trie (the end of
-    /// the path found by [`descend_last_byte`](ZipperMoving::descend_last_byte) repeatedly), so calling
-    /// it repeatedly cycles through all existing positions, like `to_next_step`.
+    /// Returns `false` when traversal ends at the zipper's root, otherwise `true`.
+    /// Called at the root, this method moves to the last existing path by sort order.
     ///
-    /// If the focus has a previous sibling, this method moves to that sibling and then descends its last
-    /// child at each level until it reaches a leaf.  Otherwise it ascends one byte.
+    /// If the zipper's focus is on a non-existent path, this method moves to the existing path immediately
+    /// before the focus path in the sequence of existing paths.
     ///
     /// `obs` is notified of every movement made, so a caller can track the zipper's location without
     /// the zipper needing to maintain a path buffer of its own.  Pass `&mut ()` to discard them.
     fn to_prev_step_observed<Obs: PathObserver>(&mut self, obs: &mut Obs) -> bool {
-        if !self.at_root() {
-            match self.to_prev_sibling_byte() {
-                Some(byte) => {
-                    //A sibling step replaces the last byte rather than adding one, so the
-                    //observer sees the old byte retracted before the new one arrives.
-                    obs.ascend(1);
-                    obs.descend_to_byte(byte);
-                },
-                None => {
-                    self.ascend_byte();
-                    obs.ascend(1);
-                    return !self.at_root()
+        if self.at_root() {
+            if self.child_count() == 0 {
+                return false
+            }
+        } else {
+            loop {
+                match self.to_prev_sibling_byte() {
+                    Some(byte) => {
+                        //A sibling step replaces the last byte rather than adding one, so the
+                        //observer sees the old byte retracted before the new one arrives.
+                        obs.ascend(1);
+                        obs.descend_to_byte(byte);
+                        break
+                    },
+                    None => {
+                        if !self.ascend_byte() {
+                            return false
+                        }
+                        obs.ascend(1);
+                        if self.at_root() {
+                            return false
+                        }
+                        if self.path_exists() {
+                            return true
+                        }
+                    }
                 }
             }
-        } else if self.child_count() == 0 {
-            return false
         }
         //Descend to the last leaf below the focus, which is the predecessor in depth-first order
         while let Some(byte) = self.descend_last_byte() {
@@ -3980,6 +3992,14 @@ pub(crate) mod zipper_moving_tests {
                     crate::zipper::zipper_moving_tests::run_test(&mut temp_store, $make_z, &[], crate::zipper::zipper_moving_tests::to_prev_step_test1)
                 }
 
+                #[test]
+                fn [<$z_name _to_prev_step_from_missing_path>]() {
+                    for root in [b"".as_slice(), b"rom".as_slice()] {
+                        let mut temp_store = $read_keys(crate::zipper::zipper_moving_tests::ZIPPER_TO_NEXT_STEP_TEST1_KEYS);
+                        crate::zipper::zipper_moving_tests::run_test(&mut temp_store, $make_z, root, crate::zipper::zipper_moving_tests::to_prev_step_from_missing_path)
+                    }
+                }
+
                 #[test]
                 fn [<$z_name _zipper_byte_iter_test1>]() {
                     let mut temp_store = $read_keys(crate::zipper::zipper_moving_tests::ZIPPER_BYTES_ITER_TEST1_KEYS);
@@ -4837,6 +4857,30 @@ pub(crate) mod zipper_moving_tests {
         assert!(zipper.at_root());
     }
 
+    /// Missing suffixes must be skipped without skipping an existing parent or predecessor subtree.
+    pub fn to_prev_step_from_missing_path<Z: ZipperMoving + ZipperPath>(mut zipper: Z) {
+        let mut paths = vec![];
+        while zipper.to_next_step() {
+            paths.push(zipper.path().to_vec());
+        }
+        for start in [b"zzzz".as_slice(), b"0zzz", b"romanusZZ", b"romzzz", b"aaaa"] {
+            zipper.reset();
+            zipper.descend_to(start);
+            assert!(!zipper.path_exists(), "test focus must be missing: {start:?}");
+            let expected = paths.iter().rev().find(|path| path.as_slice() < start);
+            let mut observed = start.to_vec();
+            assert_eq!(zipper.to_prev_step_observed(&mut observed), expected.is_some(), "from {start:?}");
+            assert_eq!(zipper.path(), expected.map_or(b"".as_slice(), |path| path.as_slice()), "from {start:?}");
+            assert_eq!(observed, zipper.path(), "observer from {start:?}");
+            assert!(zipper.at_root() || zipper.path_exists());
+
+            zipper.reset();
+            zipper.descend_to(start);
+            assert_eq!(zipper.to_prev_step(), expected.is_some());
+            assert_eq!(zipper.path(), observed);
+        }
+    }
+
     pub const ZIPPER_BYTES_ITER_TEST1_KEYS: &[&[u8]] = &[b"ABCDEFGHIJKLMNOPQRSTUVWXYZ", b"ab",];
 
     pub fn zipper_byte_iter_test1<Z: ZipperMoving + ZipperPath>(mut zipper: Z) {