Fix ACTZipper::val_count counting from the zipper root, not the focus - #80
Open
imlvts wants to merge 1 commit into
Open
Fix ACTZipper::val_count counting from the zipper root, not the focus#80imlvts wants to merge 1 commit into
imlvts wants to merge 1 commit into
Conversation
`val_count` opened with `zipper.reset()`. `ZipperValues::val_count` counts the values at and below the *focus*, so this returned the count for the whole subtrie under the zipper's root wherever the focus was, and was right only when the focus happened to be at the root. Removing the reset is not quite enough: `to_next_val` walks the zipper's entire subtrie rather than the part below the focus, so the walk has to stop when it leaves. Depth-first order visits everything below the focus before anything outside it, so the first path that no longer starts with the focus ends the count. Regression test: `act_zipper_val_count_counts_from_the_focus`, against the PathMap zipper at six foci from the map root and three from a zipper rooted below it. Fails before this change. lean/FINDINGS.md ACT finding "val_count_ignores_focus" 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
Collaborator
|
The current val_count pathway is totally gone, once we merge the new catamorphism trait. So I'd rather not merge the behavior change because it'll just create a conflict. The test might be fine under the "low bar for a test" philosophy. Also I was thinking I ought to add val_count benchmarks for ACT. So I'll keep this PR open for the test and the yet-to-be-added benchmarks |
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
2 participants
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.
val_countopened withzipper.reset().ZipperValues::val_countcounts the values at and below the focus, so this returned the count for the whole subtrie under the zipper's root wherever the focus was, and was right only when the focus happened to be at the root.Removing the reset is not quite enough:
to_next_valwalks the zipper's entire subtrie rather than the part below the focus, so the walk has to stop when it leaves. Depth-first order visits everything below the focus before anything outside it, so the first path that no longer starts with the focus ends the count.Regression test:
act_zipper_val_count_counts_from_the_focus, against the PathMap zipper at six foci from the map root and three from a zipper rooted below it. Fails before this change.lean/FINDINGS.md ACT finding "val_count_ignores_focus" on the lean-fuzzer-restage branch.