Repository navigation
refactor: one file per guarantee under laws/ and proofs/ - #71
Merged
Merged
Conversation
SPEC.md, src/LAWS.bend (4k lines) and src/PROOF.bend (11.5k lines) 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. One LAWS.bend and PROOF.bend at the root only import them; the pair under src/ is gone, and the gate is `bend PROOF.bend`. A law that proves part of several guarantees has its own file, and each guarantee that rests on it says so. 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 with SPEC.md: a file's name is its guarantee's. SPEC.md's definitions (well-formed, plain word, current command, selected path, env value) head LAWS.bend. Of the trust boundary, the checker's soundness and the gate runner hold for every Bend project and are dropped; what IO.args and IO.get_env hand on, and that argv and env_vars pass it through, is said on src/args.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 tasks done
The requirement table the law files replaced stays as a record: the RFCs name guarantees by its IDs. LAWS.bend points to it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
bolt v1.22.0 reads law and proof files by what LAWS.bend and PROOF.bend import, which this layout needs. The rules changed since the v1.19.0 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:33
ngngardner
enabled auto-merge (squash)
November 1, 2026 03:33
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(prose, then its quantified laws), proved byproofs/<Name>.bend. A singleLAWS.bend/PROOF.bendpair at the root only imports them. The oldsrc/LAWS.bend(4k lines) andsrc/PROOF.bend(11.5k lines) are gone, and the gate is nowbend PROOF.bend.laws/defs/, and lemmas several proofs use live inproofs/lemmas/. Each is named for what it holds. A law that several guarantees rest on has its own file.LAWS.bend.src/args.bend: whatIO.argsandIO.get_envhand on, and thatargvandenv_varspass it through.def trace().Depends on
Emerging-Patterns/bolt#257. The pinned bolt (v1.19.0) 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# noqainsrc/eq.bend,src/grow.bend,src/walk.bendandexamples/demo. Main shows the same 36 under that bolt, plus a C011 fordef trace(). They need cleaning when the pin is bumped.nix flake check🤖 Generated with Claude Code