diff --git a/differential/src/harness.rs b/differential/src/harness.rs index 0b0d72d9..3ac19648 100644 --- a/differential/src/harness.rs +++ b/differential/src/harness.rs @@ -147,7 +147,7 @@ pub fn fingerprint + 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( 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( // unspecified (it continues state left by // `descend_first_k_path`). let mut v: Vec = 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) { diff --git a/lean/PathMapModel/Fuzz.lean b/lean/PathMapModel/Fuzz.lean index de6c88e7..977325d0 100644 --- a/lean/PathMapModel/Fuzz.lean +++ b/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. diff --git a/lean/README.md b/lean/README.md index f3a0cb43..60696f91 100644 --- a/lean/README.md +++ b/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. | diff --git a/lean/differential.py b/lean/differential.py index 47b593dd..0e91a522 100755 --- a/lean/differential.py +++ b/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]"), diff --git a/src/arena_compact.rs b/src/arena_compact.rs index 183b7bc1..c05f9af5 100644 --- a/src/arena_compact.rs +++ b/src/arena_compact.rs @@ -3255,7 +3255,7 @@ where Storage: AsRef<[u8]> fn descend_first_k_path_observed(&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 diff --git a/src/prefix_zipper.rs b/src/prefix_zipper.rs index 14823612..efb0c65b 100644 --- a/src/prefix_zipper.rs +++ b/src/prefix_zipper.rs @@ -558,6 +558,9 @@ impl<'prefix, Z> ZipperIteration for PrefixZipper<'prefix, Z> } fn descend_first_k_path_observed(&mut self, k: usize, obs: &mut Obs) -> bool { + if k == 0 { + return false; + } if self.position.is_invalid() { return false; } diff --git a/src/zipper.rs b/src/zipper.rs index ba96c579..61a173ae 100644 --- a/src/zipper.rs +++ b/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(&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(&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(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:",