Repository navigation
refactor: one file per guarantee under laws/ and proofs/ - #87
Merged
Merged
Conversation
SPEC.md, LAWS.bend and a 53k-line PROOF.bend had to be read side by side, matched up by ID tags. Each guarantee is now laws/<Name>.bend, its prose on top and its quantified laws under it, proved by proofs/<Name>.bend. LAWS.bend and PROOF.bend only import them. Definitions the laws share are under laws/defs/, lemmas several proofs use under proofs/lemmas/, each named for what it holds. Requirement IDs are gone: a file's name is its guarantee's. SPEC.md's definitions (well-formed, same, the number rule) head LAWS.bend, the fixed-decimal notes head laws/FixedWritesValidNumbers.bend, and the table itself is kept as docs/SPEC.md, which the RFCs' IDs point into. 16 proof helpers no proof reached are gone. Of the trust boundary, the checker's soundness and the gate runner hold for every Bend project and are dropped; F32.read is trusted on as_f32, and the cursor's memory on src/pull.bend. This needs a bolt that reads law and proof files by what LAWS.bend and PROOF.bend import, and no longer runs `trace`; bolt.bend drops `trace`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2 of 3 tasks
bolt v1.22.0 reads law and proof files by what LAWS.bend and PROOF.bend import, which this layout needs. Rules changed since the old pin, so some noqa comments no longer silence anything (S005); they are removed. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
ngngardner
marked this pull request as ready for review
November 1, 2026 03:39
ngngardner
enabled auto-merge (squash)
November 1, 2026 03:39
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.
Summary
laws/<Name>.bend(its prose, then its quantified laws), proved byproofs/<Name>.bend.LAWS.bendandPROOF.bendonly import them. That's 40 law files, 5 shared definition files and 28 lemma files, replacing the 53k-line PROOF.bend.LAWS.bend: well-formed,same, and where the number rule is written out.laws/FixedWritesValidNumbers.bend.docs/SPEC.md, since the RFCs cite its IDs.F32.readis now trusted in a comment onas_f32, and the cursor's memory in one onsrc/pull.bend.def trace().Depends on
Emerging-Patterns/bolt#257. The pinned bolt reads law files by name only and still runs
trace. This PR stays a draft until that release lands and the pin is bumped here.Test plan
bend PROOF.bend→ALL PROOFS CHECKS005stale# noqainscale/andbench/, which main also shows under that bolt (main has a C011 fordef trace()on top).nix flake check🤖 Generated with Claude Code