Stop a read zipper from walking out of its own root - #77
Open
imlvts wants to merge 1 commit into
Open
Conversation
`to_next_sibling_byte` guarded with `prefix_buf.len() == 0`, which asks "am I at the *map* root". The question is "am I at *this zipper's* root", which `at_root()` answers. Rooted anywhere else, the sibling step rewrote the last byte of `prefix_buf`, and at the zipper's root that byte belongs to the root path, so the zipper's own root moved: `origin_path` changed while `root_key_start` and `focus_node` went on describing the old one. `to_sibling`, which `to_prev_sibling_byte` routes through, had no guard at all. `ZipperMoving` documents the answer here as "did not move", and `ZipperHead` depends on it: it hands out zippers on the promise that each stays inside its subtrie. It is worse than a containment violation. Once `origin_path` has moved, `reset()` truncates to it and pops the ancestor stack, leaving the zipper deregularized; `descend_to` asserts on that in a debug build and loops forever in a release one, and `move_to_path` is `reset` then `descend_to`. The differential fuzzer hit this as two hangs per 2000 inputs. A second, smaller fix in the same method: the re-descent after a sibling step tested `key_bytes.len() == 1`, which expresses "landed at the end of the path within the node" only when the node key is a single byte. `node_key.len()` is `fixed_len + 1`, so that is the test. Regression tests: `read_zipper_sibling_step_never_leaves_its_root` covers both entry points, for roots that exist and roots that do not, and fails before this change. `read_zipper_sibling_steps_when_rooted_inside_a_node` exercises sibling steps and subsequent movement from zippers rooted at every depth inside a shared prefix; it did not reach the second condition on the shapes tried and is a guard rather than a reproduction of that half. lean/FINDINGS.md finding 3 on the lean-fuzzer-restage branch. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BZmoASqM5FUuzvJeJaYQjR
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
to_next_sibling_byteguarded withprefix_buf.len() == 0, which asks "am I at the map root". The question is "am I at this zipper's root", whichat_root()answers. Rooted anywhere else, the sibling step rewrote the last byte ofprefix_buf, and at the zipper's root that byte belongs to the root path, so the zipper's own root moved:origin_pathchanged whileroot_key_startandfocus_nodewent on describing the old one.to_sibling, whichto_prev_sibling_byteroutes through, had no guard at all.ZipperMovingdocuments the answer here as "did not move", andZipperHeaddepends on it: it hands out zippers on the promise that each stays inside its subtrie.It is worse than a containment violation. Once
origin_pathhas moved,reset()truncates to it and pops the ancestor stack, leaving the zipper deregularized;descend_toasserts on that in a debug build and loops forever in a release one, andmove_to_pathisresetthendescend_to. The differential fuzzer hit this as two hangs per 2000 inputs.A second, smaller fix in the same method: the re-descent after a sibling step tested
key_bytes.len() == 1, which expresses "landed at the end of the path within the node" only when the node key is a single byte.node_key.len()isfixed_len + 1, so that is the test.Regression tests:
read_zipper_sibling_step_never_leaves_its_rootcovers both entry points, for roots that exist and roots that do not, and fails before this change.read_zipper_sibling_steps_when_rooted_inside_a_nodeexercises sibling steps and subsequent movement from zippers rooted at every depth inside a shared prefix; it did not reach the second condition on the shapes tried and is a guard rather than a reproduction of that half.lean/FINDINGS.md finding 3 on the lean-fuzzer-restage branch.