Read Bend 2 code, with a rule for its laws - #31
Merged
Merged
Conversation
…s say Bend 2 (bendlang/bend 2.0.x) files are parsed with tree-sitter-bend2: defs, types and laws are units, calls through import aliases reach the defs they name, and a test is a program ending in its expected output. Proofs and type-level defs are told from code; only defs with effects or built text get the security questions. Bend 1 files are skipped with their own reason, and a new rule, tests/laws, asks whether the comment above a law claims more than the law states, read in words. Parsing stops after 10 seconds, and outlines are budgeted as JSON.
…or size unsent A law whose first answer stays undecided is asked a Choice naming what its comment says beyond the law: nothing, context, a property, more inputs or a consequence under an unstated condition. A request the provider refuses as beyond the model's context no longer fails its file: the units it asked that no other request answered need context, as units the budget does not send.
…generalizes Of 29 laws still undecided after the relation Choice on thirteen Bend 2 projects, 11 checked one fixed key, an empty or one-entry object or one byte under a comment claiming the behavior in general. Asked directly, the 4 at 0.65 or more were all right.
…ling benchmarks apart A comment above a law also describes the laws right after it that have no comment of their own: "sound and complete" heads nfa_sound and nfa_complete. Copies in sibling benchmark programs, such as bendlang/bend's bench/runtime/*, are not compared, as sibling examples are not.
Hardcoded values: a case pattern's literal is not a candidate (Bend matches only literals and constructors), a Bool predicate that laws check and the defs only it calls hold samples, and the kind follow-up offers a bound that only needs to be large enough and an arbitrary mixing constant, and names a one-line def made to name its value. Function questions: the split note states Bend's shapes (one def per state machine, helper defs for computed matches, proofs following their definition), and flattening proposes nested patterns and a case _ fallback instead of guard clauses and early returns. On thirteen Bend 2 projects, labeled by hand: function-simplification findings from 24 right and 16 wrong to 19 and 3; hardcoded-value considers from 59 right and 144 wrong to 58 and 65.
A Bend 2 test is a whole program pinned to the output its run prints; the 4 shared-logic findings between two such tests on thirteen Bend 2 projects were all wrong.
A proof's steps follow the cases of what it proves, and its copies the rewrites each constructor needs, or a lemma a standalone demo or eval repeats. On 25 Bend 2 projects, the 4 function-simplification and 3 shared-logic findings on proofs were all wrong; a proof is a def of a PROOF.bend, one that fills a law, or one that returns an equality.
A Bend 2 test is a whole program, so a file on a test path that defines main is one test, whether its expected output ends the file or sits beside it, as bendc's tests/X.out. Asked their purpose, 48 of 85 such files stayed unresolved and were judged as application code, and a law of bendc's compiler feature test became a review.
A section's opening paragraph, above a blank line, speaks of the section's laws together: bulkhead's, which draws a restart claim from several laws, was read as the promise of the first one below it.
Bend 2 writes each match arm, binding and effect on a line of its own. On 25 Bend 2 projects, the 16 file-organization findings on files of fewer member lines were all labeled wrong, and the 13 right ones were on files of 313 member lines or more. The floor is min_bend_file_lines in the decision policy.
Function simplification and shared logic leave Bend 2 proofs out and word their questions for Bend 2; shared logic keeps sibling benchmarks and separate Bend 2 tests apart; file organization weighs a Bend 2 file only past its own floor; hardcoded values asks Bend 2 what kind of value it is.
The laws example was nfa_sound, whose comment also heads nfa_complete; it is body_after_blank of the HTTP client demo, whose law checks only texts that open with the blank line.
A PROOF.bend, a file named after what it proves (padding_proof.bend, BloomSafeProof.bend) or one under a proof or proofs directory holds proofs: its defs are not asked to be split nor about values, and its laws are lemmas whose comments say how a proof goes. On the 16 projects where such files were first judged, 12 of 14 function-simplification findings in them were wrong and the rest debatable, as were 14 of 15 law findings, and 36 of 40 hardcoded-value findings were wrong.
In a library of proofs, a derivation written out in several lemmas is one a shared lemma would serve: on the 16 projects where proofs were first compared, 32 of 41 shared-logic findings on files of proofs were right and 5 wrong. The three wrong ones this was tuned on were a lemma repeated in a standalone demo and an eval, and case arms of one proof. Function simplification still leaves proofs out: its 16 findings on them across 41 projects were all wrong (2 more debatable).
A benchmark's values are its workload: the sizes, seeds and ranges its C or TypeScript twin shares and its expected output pins. Of 82 hardcoded-value findings in the benchmark directories of Bend 2 projects, 70 were wrong.
An author who rules a Bend 2 file off into sections (# ----, # === Title) has laid it out as one module in parts, and the groups proposed from its calls rarely follow them: on 41 Bend 2 projects, 7 of 43 file-organization findings on files with two or more section rules were right, against 10 of 17 on files without.
Bend 2 writes each match arm, binding and effect on a line of its own and runs to long files, which the split question reads as several modules. On 64 Bend 2 projects, 14 of 43 file-organization reviews were right: 8 of 13 on the 41 the floor and sections were tuned on, and 6 of 30 on 23 projects never used for tuning.
Measured on 41 Bend 2 projects used for tuning and 23 never used for it, with every review and a sample of considers labeled by hand.
JevGate's own review of this branch read law_predicates as mixing separate jobs: collecting what laws and tests call, keeping the Bool predicates only other predicates call, and adding the defs only they call. Each step is its own function now; behavior is unchanged.
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
1 participant
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.
JevGate reads Bend 2 (bendlang/bend 2.0.x), with a new rule for its laws.
What changes
.bendfiles are parsed withtree-sitter-bend2(0.1.2, MIT). Defs, types and laws are units; calls through an import alias reach the def they name; imports link files by path, andimport Baselinks Base in the Bend repository. Every Bend request carries a short notation primer (file.notation), since a model may know Bend 1 or no Bend at all.++get the security questions.#|lines its run must print, or on a test path any file that definesmain(bendc keeps its outputs intests/X.out). It is judged whole.PROOF.bend,*_proof.bend, or anything underproof/orproofs/) holds proofs: its defs are not asked to be split or about values, and its laws are lemmas. Proof steps are still compared for copies, since a derivation repeated across lemmas is a real finding in a proof library.tests/laws(on by default, no--include-testsneeded). It asks whether the comment above a law claims more than the law states. The law is read in words, with the uncommented laws its comment heads, the file's header comment and the defs it names. An undecided law is asked what its comment adds, and whether it checks only particular inputs.casepattern's literal, a zero-argument def's number and a law predicate's samples are not value candidates. The function questions state Bend's shapes. Files under 300 member lines are not weighed for a split (min_bend_file_lines), a split of a Bend 2 file is at most a consider, and a note when the file is laid out in titled sections. A benchmark's values are not asked about. Copies between sibling benchmarks or separate Bend tests are not compared..bend. Any parse also stops after 10 s: Bend 2's grammar spent over ten minutes on a 1 MB Bend 1 file.Measured
Every review and consider on Bend code was labeled by hand from the code; debatable counts as not right.
Known limits
Failtext read as an exception's, a TLS library's documented opt-outs).letoutsidedo, a line continued inside parentheses, array literals with defaults (![0:1, _:7; 1]),~clauses in laws. 125 of 4,635.bendfiles in the 64 projects are skipped for it, 67 of them in one project that mixes dialects.