perf: index once in rewalk, bind.refresh and digest.laws_of (#228) - #231
Merged
Merged
Conversation
- rewalk: rate each site once (narrow over the piece) before reporting, so other_go, earlier and report compare ratings instead of walking the piece for every pair of twin sites. The proofs of rewalk_local_counts now go through Rewalk.rate; no law changed. - bind.refresh: read the annotated binders with a cursor (binders are in source order) instead of one full binder search per environment entry; a binder before the last one read starts the cursor over. - digest.laws_of: carry the outline items forward as a cursor instead of searching them from the start for each law. unused (reportable over the foreign header lines) is left as is: a faster lookup cannot be proved equal to the List.contains that unused_counts states. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01X7i62UAece6mwMRV3Y1b9B
The two new cursors wrapped their recursive step in Lazy.stop, the lone thunk AGENTS.md warns against for a search (thunk, U015). Carry the head's test as a Bool into the next call and match on it after the list, so the step stays a tail call. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01X7i62UAece6mwMRV3Y1b9B
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.
Fixes three of the four per-item scans in #228. No LAWS.bend changed, and bolt's lint output is byte-identical.
Changes
other_go,earlierandreportnow compare the stored flags, andother_full,earlier_oneandearlier_narare gone. The proofs ofrewalk_local_countsinsrc/rules/PROOF.bendnow go throughRewalk.rate.+aN = walk(xs)lets: 14.7 s → 0.14 s.bindersearch for each environment entry. The binders are in source order, whichBoundpromises. A binder earlier than the last one read restarts the cursor, so the result stays right whatever order the environment is in. Old and new gave the same result on all 20,461 scopes of 102 files in the tree.Lawlists were byte-identical on all 8 LAWS.bend files and on a synthetic file with 3,000 laws.seekandfrom_line, carry the stop test as a Bool instead of wrapping the recursive step in a thunk, as AGENTS.md asks.thunk(U015) reports none of the new code.Not changed: unused
unused_countsstates the foreign-line lookup asList.containsover anybinds. A faster exact lookup, such as a trie or a sorted cursor, would need a lemma thatU32.is_eq(a, b)meansa == b, and Base has none. That list is also empty in any file without foreign defs.With
scanturned on, the refresh, laws_of and rewalk per-site findings are gone. rewalk still has two scan findings: one walk per site, and the pairwise twin comparison that the law states.Gate
bend PROOF.bendprints ALL PROOFS CHECK in all 7 directories.bend main.bend -o bin/bolt.binbuilds.bolt --gpu offgives0 errors, 73 warnings, the baseline.🤖 Generated with Claude Code
https://claude.ai/code/session_01X7i62UAece6mwMRV3Y1b9B
Generated by Claude Code