Repository navigation
refactor: one file per guarantee under laws/ and proofs/ - #164
Merged
Merged
Conversation
SPEC.md and eighteen nested LAWS.bend/PROOF.bend pairs under src/ (about 49k 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. The root LAWS.bend and PROOF.bend only import them; no subdirectory keeps a pair. src/relock/PROOF.bend's lemmas went with the proofs that use them, and src/check/PROOF.bend's two imports moved to the root PROOF.bend. 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 preamble heads LAWS.bend, its notes on how each row was proved head the law files they concern, and the nested pairs' header prose went to the law and proof files it describes. The table itself is kept as docs/SPEC.md, which the RFCs' IDs point into. 79 proof helpers and 6 law definitions no law or proof reached are gone. Of the trust boundary, the checker's soundness is dropped. The rest is said on the code that assumes it, as `# Trusted, not proved:` comments: the interpreters on src/ez/app.bend, the words on src/share/args.bend, the gate runner on src/ez/prove.bend, the hub on src/hub/hub.bend, HTTP on src/hub/get.bend, stable names and the lock reading back on src/lock/lock.bend, command-line parsing on src/ez/line.bend (citing shake's law files), eztoml's round trip on src/toml/toml.bend, snap's answers on src/ez/ends.bend, git on src/git/git.bend, the 0x hash on src/pkg/pkg.bend, the narHash on src/sha/nar.bend and SHA-256 on src/share/sha.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>
The 113 law files the split named after their law's identifier (AddIdem, GapOfFullPin, UpsPlain) are renamed for what they guarantee (LedgerAddIdempotent, FullToolPinCopied, PlainPathHasNoClimbs), with their proof files, imports and cites. src/hub/get.bend cites ezhttp's law files in place of its HTTP- IDs, and a comment in laws/defs/LockInputs.bend no longer points at two laws that are gone. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
ngngardner
marked this pull request as ready for review
November 1, 2026 03:53
ngngardner
enabled auto-merge (squash)
November 1, 2026 03:55
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
One file per guarantee. Each guarantee is
laws/<Name>.bend(its prose, then its quantified laws), proved byproofs/<Name>.bend. The rootLAWS.bendandPROOF.bendonly import them. That's 211 law files (64 for SPEC.md's proved rows, 147 for laws no row tagged or several rows shared, each named for the behavior it states), 10 shared definition files and 26 lemma files.No nested pairs. The 18
LAWS.bend/PROOF.bendpairs undersrc/(about 49k lines) are folded into the root.src/relock/PROOF.bend's lemmas went with the proofs that use them.src/check/PROOF.bend's imports ofeq.bendandstr.bendmoved to the rootPROOF.bend. A few helper names two pairs both defined were renamed (lock'spermispacks.perm, pkg's isfiles.perm, and so on).No requirement IDs.
LAWS.bend.docs/SPEC.md, since the RFCs anddocs/guide.mdcite its IDs.Trust boundary.
# Trusted, not proved:comments on the code that assumes them:src/ez/app.bendsrc/share/args.bendez prove:src/ez/prove.bendsrc/hub/hub.bendsrc/hub/get.bend, citing ezhttp's law filessrc/lock/lock.bendsrc/ez/line.bend, citing shake's law filessrc/toml/toml.bend, citing eztoml's law filessrc/ez/ends.bendsrc/git/git.bendbend --publish:src/pkg/pkg.bendsrc/sha/nar.bendsrc/share/sha.bendHelpers: 79 proof helpers and 6 law definitions that no law or proof reached are gone.
bolt.bend drops
def trace(). AGENTS.md describes the new layout.bolt v1.22.0:
[tools.bolt]is bumped to the release with feat!: one guarantee per file under laws/ and proofs/; drop trace and SPEC.md bolt#257 (import-based law/proof roles, notrace), and the# noqacodes it finds silence nothing are dropped.Test plan
bend PROOF.bendprintsALL PROOFS CHECK.ez provefinds only the rootPROOF.bendnow.L001coverage). main under the same bolt has the same 320 warnings, plus 1 error (C011fordef trace()).ez doctor(ez 1.13.0, afterez fetch): ez.lock.toml is up to date, and every imported package is named in ez.toml.nix flake checkpasses🤖 Generated with Claude Code