descend_first_k_path(0) compliance fixes

differential/src/harness.rs

@@ -147,7 +147,7 @@ pub fn fingerprint<Z: ZipperMoving + ZipperPath + ZipperValues<u64> + ZipperAbso
 ///   implement the trait the op needs.
 /// * `skip:at-root` — `to_next`/`to_prev_sibling_byte` at the zipper root,
 ///   where the native read zipper escapes its own root.
-/// * `skip:k0` — a degenerate `k = 0`.
+/// * `skip:k0` — a degenerate `k = 0` on `join`/`meet_k_path_into`.
 /// * `skip:empty-focus` — the focus has nothing below it, where the op's
 ///   behaviour is a function of node materialisation rather than trie state.
 /// * `skip:empty-path` — `insert_prefix("")`, which destroys the subtrie.
@@ -583,13 +583,9 @@ pub fn run_ops<R: ReadSource>(
                 15 => {
                     let _t = get!(d.modn(2));
                     let k = get!(d.modn(4));
-                    // k == 0 is degenerate; see Fuzz.lean.
-                    if k == 0 {
-                        ("descend_first_k_path", SKIP_K0.to_string())
-                    } else {
-                        let r = (*rz).descend_first_k_path(k);
-                        ("descend_first_k_path", show_bool(r).to_string())
-                    }
+                    // k == 0 is specified as an unsuccessful descent; see Fuzz.lean.
+                    let r = (*rz).descend_first_k_path(k);
+                    ("descend_first_k_path", show_bool(r).to_string())
                 }
                 16 => {
                     let _t = get!(d.modn(2));
@@ -598,13 +594,7 @@ pub fn run_ops<R: ReadSource>(
                     // unspecified (it continues state left by
                     // `descend_first_k_path`).
                     let mut v: Vec<String> = Vec::new();
-                    if k == 0 {
-                        let _ = writeln!(out, 
-                            "{step} k_path_walk ret={SKIP_K0} W={} R={}",
-                            fingerprint(&wz, root0), fingerprint(rz, root1));
-                        step += 1;
-                        continue;
-                    }
+                    // With k == 0 the descent fails and the walk is empty.
                     if rz.descend_first_k_path(k) {
                         v.push(hex_path(rz.path()));
                         while v.len() < 32 && rz.to_next_k_path(k) {

lean/PathMapModel/Fuzz.lean

@@ -62,7 +62,7 @@ agree exactly or every input with a skip diverges.
   the trait the op needs.
 * `skip:at-root` — `to_next`/`to_prev_sibling_byte` at the zipper root, where
   the native read zipper escapes its own root.
-* `skip:k0` — a degenerate `k = 0`.
+* `skip:k0` — a degenerate `k = 0` on `join`/`meet_k_path_into`.
 * `skip:empty-focus` — the focus has nothing below it, where the op's behaviour
   is a function of node materialisation rather than trie state.
 * `skip:empty-path` — `insert_prefix("")`, which destroys the subtrie.
@@ -310,23 +310,21 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do
              let (r, z) := s.rz.toNextVal
              some (emit { s with rz := z } "to_next_val" (showBool r), d)
   | 15 => do let (_t, d) ← d.mod 2; let (k, d) ← d.mod 4
-             -- `k = 0` is degenerate: `k_path_internal` treats "already at depth
-             -- base+0" as a hit and reports success without moving, then
-             -- `to_next_k_path(0)` reports success forever.  Skipped.
-             if k == 0 then some (emit s "descend_first_k_path" skipK0, d)
-             else
-               let (r, z) := s.rz.descendFirstKPath k
-               some (emit { s with rz := z } "descend_first_k_path" (showBool r), d)
+             -- `k = 0` is specified: `false`, focus untouched.  `kPathFrom` gives
+             -- that with no special case, since it wants a location strictly after
+             -- the focus and the only one at depth base+0 is the focus itself.
+             let (r, z) := s.rz.descendFirstKPath k
+             some (emit { s with rz := z } "descend_first_k_path" (showBool r), d)
   | 16 => do let (_t, d) ← d.mod 2; let (k, d) ← d.mod 4
              -- `to_next_k_path` is only meaningful as the continuation of a
              -- `descend_first_k_path` iteration -- `k_path_internal` carries
              -- iteration state, and calling it cold is flagged by pathmap's own
              -- debug assertions.  So the op is the whole walk, not one step.
-             if k == 0 then some (emit s "k_path_walk" skipK0, d)
-             else
-               let (ps, z) := kWalk s.rz k
-               some (emit { s with rz := z } "k_path_walk"
-                 (String.intercalate "," (ps.map hexPath)), d)
+             -- With `k = 0` the descent fails, so the walk is empty and the
+             -- never-ending `to_next_k_path(0)` is not reached.
+             let (ps, z) := kWalk s.rz k
+             some (emit { s with rz := z } "k_path_walk"
+               (String.intercalate "," (ps.map hexPath)), d)
   | 17 => do let (_t, d) ← d.mod 2
              -- `ZipperIteration` is read-only: the target byte is still consumed,
              -- but the operation always applies to the read zipper.

lean/README.md

@@ -329,7 +329,7 @@ skips diverges:
 
 | token | what it means |
 |---|---|
-| `skip:k0` | `meet_k_path_into(0)`, `join_k_path_into(0)`, `descend_first_k_path(0)` / `to_next_k_path(0)` — degenerate; the first two should be the identity and destroy the subtrie, the last reports success without moving, forever. |
+| `skip:k0` | `meet_k_path_into(0)`, `join_k_path_into(0)` — degenerate; they should be the identity and destroy the subtrie. (`descend_first_k_path(0)` is specified as `false` without moving and is no longer skipped.) |
 | `skip:empty-focus` | `meet_k_path_into` with no children (it does not terminate), and `restricting` when either side has nothing below its focus (the two branches differ in *effect*, not just in the reported bool). |
 | `skip:empty-path` | `insert_prefix("")` — should be the identity, destroys the subtrie. |
 | `skip:at-root` | `to_next_sibling_byte` / `to_prev_sibling_byte` at the zipper root — the native read zipper leaves its own root there. |

lean/differential.py

@@ -266,12 +266,6 @@ def run(self, blob):
      "copy-on-write cannot make a shared dangling path unique (finding 16) "
      "[shared_dangling_cow]"),
     # ArenaCompactTree read source (differential.py --act).
-    (["k_path_walk"],
-     "ACTZipper::descend_first_k_path() only walks the leftmost chain "
-     "[act: first_k_path_no_backtrack]"),
-    (["descend_first_k_path"],
-     "ACTZipper::descend_first_k_path() only walks the leftmost chain "
-     "[act: first_k_path_no_backtrack]"),
     (["descend_last_path"],
      "ACTZipper::descend_last_path() runs one byte past the end of the trie "
      "[act: last_path_overshoots]"),

src/arena_compact.rs

@@ -3255,7 +3255,7 @@ where Storage: AsRef<[u8]>
     fn descend_first_k_path_observed<Obs: PathObserver>(&mut self, k: usize, obs: &mut Obs) -> bool {
         timed_span!(DescendFirstKPath, COUNTERS);
         if k == 0 {
-            return true;
+            return false;
         }
         //This used to follow the first byte `k` times and give up if it ran out, which finds a
         //path of length `k` only when the leftmost chain happens to be that long -- so a trie

src/prefix_zipper.rs

@@ -558,6 +558,9 @@ impl<'prefix, Z> ZipperIteration for PrefixZipper<'prefix, Z>
     }
 
     fn descend_first_k_path_observed<Obs: PathObserver>(&mut self, k: usize, obs: &mut Obs) -> bool {
+        if k == 0 {
+            return false;
+        }
         if self.position.is_invalid() {
             return false;
         }

src/zipper.rs

@@ -1051,6 +1051,9 @@ pub trait ZipperIteration: ZipperMoving {
     ///
     /// See: [to_next_k_path](ZipperIteration::to_next_k_path)
     fn descend_first_k_path_observed<Obs: PathObserver>(&mut self, k: usize, obs: &mut Obs) -> bool {
+        if k == 0 {
+            return false;
+        }
         k_path_default_internal(self, k, self.depth(), obs)
     }
 
@@ -2664,6 +2667,9 @@ pub(crate) mod read_zipper_core {
         }
         fn descend_first_k_path_observed<Obs: PathObserver>(&mut self, k: usize, obs: &mut Obs) -> bool {
             timed_span!(DescendFirstKPath, COUNTERS);
+            if k == 0 {
+                return false;
+            }
             self.prepare_buffers();
             debug_assert!(self.is_regularized());
 
@@ -4639,6 +4645,12 @@ pub(crate) mod zipper_iteration_tests {
                     crate::zipper::zipper_iteration_tests::run_test(&mut temp_store, $make_z, b":", crate::zipper::zipper_iteration_tests::k_path_test1)
                 }
 
+                #[test]
+                fn [<$z_name _k_path_zero>]() {
+                    let mut temp_store = $read_keys(crate::zipper::zipper_iteration_tests::K_PATH_ZERO_KEYS);
+                    crate::zipper::zipper_iteration_tests::run_test(&mut temp_store, $make_z, b"", crate::zipper::zipper_iteration_tests::k_path_zero)
+                }
+
                 #[test]
                 fn [<$z_name _k_path_test2>]() {
                     let paths = crate::zipper::zipper_iteration_tests::k_path_test2_paths();
@@ -4750,6 +4762,20 @@ pub(crate) mod zipper_iteration_tests {
         assert_eq!(count, ZIPPER_ITER_TEST2_COUNT);
     }
 
+    pub const K_PATH_ZERO_KEYS: &[&[u8]] = &[b"a", b"b"];
+
+    /// The contract explicitly defines `k == 0` as unsuccessful and requires an unsuccessful
+    /// descent to leave the zipper at its original focus.
+    pub fn k_path_zero<Z: ZipperIteration + ZipperPath>(mut zipper: Z) {
+        //At a branching focus, where the native zipper used to report success
+        assert!(!zipper.descend_first_k_path(0));
+        assert_eq!(zipper.path(), b"");
+        assert!(zipper.descend_first_byte().is_some());
+        assert_eq!(zipper.path(), b"a");
+        assert!(!zipper.descend_first_k_path(0));
+        assert_eq!(zipper.path(), b"a");
+    }
+
     /// This is a toy encoding where `:n:` precedes a symbol `n` characters long
     pub const K_PATH_TEST1_KEYS: &[&[u8]] = &[
         b":5:above:3:the:4:fray:",