This is the list of every behavior bolt guarantees, each under a stable requirement ID. Every requirement has one of two levels. A Proved requirement holds for every input, and is backed by a quantified law (a for or exs binder) in a LAWS.bend that passes the proof gate. A Trusted requirement is an assumption bolt cannot check from inside its own gate, and it is listed in the trust boundary below. A Proved requirement whose law has not landed yet has status pending: we intend to prove it, and until then it is not guaranteed. The proof gate is this check: for every PROOF.bend in the tree, the first line bend PROOF.bend prints is exactly ALL PROOFS CHECK (bend 2.0.32's verdict, which fails a proof that loads @unsafe or foreign code, imports included, so no PROOF.bend imports a module holding a foreign effect: those take the effect as a service). Tests and fixtures are never evidence for a requirement.
The reasoning behind each requirement, the verdict of each against the code at a38e87a, and the decisions that shaped them are in docs/rfc/bolt-spec.md. Every law as it stood then is in docs/rfc/bolt-law-inventory.md.
A requirement table is any table whose header row is exactly | ID | Requirement | Level | Status | Law |. An ID is uppercase segments joined by hyphens, at least two ([A-Z][A-Z0-9]*(-[A-Z0-9]+)+), unique within the requirement tables, and never reused once released. Level is Proved or Trusted. Status is proved or pending for a Proved row and empty for a Trusted row. A Law cell holds <path> <law> entries, paths relative to this file, separated by ; . A proved row names one or more laws, and together they prove it. A pending row may name laws that each prove part of it; the row stays pending until its requirement is proved in full, and its entries are checked as a proved row's are. A Trusted row names none.
A law proves a requirement when a comment line # <ID>, alone on its line, sits in the unbroken comment block directly above its law line. A law may carry several tags, one per line:
# LAW: a thunk that ignores its argument makes stop Bool.pick
# BOLT-LIB-1
law stop_is_pick:
A tag may name a proved or a pending requirement, never a Trusted one or an ID no requirement table lists. A Trusted requirement's ID appears once in a requirement table and once in the trust boundary table. Untagged quantified laws are allowed; they pass the gate like any law, but nothing here protects them. A law with no binder is a closed finding.
| ID | Requirement | Level | Status | Law |
|---|---|---|---|---|
| BOLT-RULE-C002 | hole reports exactly a TODO hole bend counts, a ? then TODO with only spaces, newlines or comments between, outside a LAWS.bend, and nothing else. |
Proved | proved | src/rules/LAWS.bend hole_counts |
| BOLT-RULE-C003 | pick reports exactly a self-call in one or both branches of Bool.pick, and does not report again a nested pick in a branch it reported. |
Proved | proved | src/rules/LAWS.bend pick_walk_counts; src/rules/LAWS.bend pick_picks_counts; src/rules/LAWS.bend pick_counts; src/rules/LAWS.bend pick_mute; src/rules/LAWS.bend pick_next |
| BOLT-RULE-C004 | put reports exactly one finding for each Map.put token with a ( token right after it among the significant tokens, and none in a file where a def keyword has a Map.put token right after it. |
Proved | proved | src/rules/LAWS.bend put_counts |
| BOLT-RULE-C005 | arms reports exactly, in a single-scrutinee match, a Nat arm already covered by an earlier kn+p, Succ{p} or Succ{_} arm. |
Proved | proved | src/rules/LAWS.bend arms_counts |
| BOLT-RULE-C006 | escape reports exactly one finding for each \0 followed by a digit in a string or char literal, its escapes read as a backslash and the one char after it, and none for anything else. |
Proved | proved | src/rules/LAWS.bend escape_counts; src/rules/LAWS.bend escape_scan_counts |
| BOLT-RULE-C007 | twice reports exactly, in a def that calls itself, a list pattern in a case's first match column opening with the same literal twice. |
Proved | proved | src/rules/LAWS.bend twice_counts |
| BOLT-RULE-C008 | strings reports exactly a match whose closed string-literal arms, read in the first match column, total over 64 characters. |
Proved | proved | src/rules/LAWS.bend strings_counts |
| BOLT-RULE-C009 | chars reports exactly a match with more than eight arms whose first match column opens with a char literal. |
Proved | proved | src/rules/LAWS.bend chars_counts |
| BOLT-RULE-C010 | foreign reports exactly a foreign def with a .c body and no .js or the reverse, where a file whose leading comment lines include the exact line # lanes: native needs no .js. |
Proved | proved | src/rules/LAWS.bend foreign_native; src/rules/LAWS.bend foreign_walk_counts; src/rules/LAWS.bend foreign_counts |
| BOLT-RULE-C011 | setting reports exactly, for each bolt.bend that grades a directory the run grades (a source's or SPEC.md's; the first of its candidates the World read, BOLT-CFG-4), each bolt.bend once in the order its directories come, one finding for each setting unknown holds (BOLT-CFG-7), at that bolt.bend's path and the line of the setting's def, in file order, and nothing else. It runs in the CLI lint only. |
Proved | proved | src/LAWS.bend unknown_exact; src/LAWS.bend setting_reports |
| BOLT-RULE-U001 | unused reports exactly an unused let, do-bind, lambda binder or parameter, with the header's exemptions: a foreign def, whose parameters are exempt, is one whose body's first statement is import, wherever its header's -> and return type fall. |
Proved | proved | src/rules/LAWS.bend unused_counts |
| BOLT-RULE-U002 | strict reports exactly a self-call inside Bool.and or Bool.or, or in a comma-separated stretch holding && or || (matched by that exact text), where a => ends the stretch on its left and a lambda body counts only by its own && or ||. |
Proved | proved | src/rules/LAWS.bend strict_walk_counts; src/rules/LAWS.bend strict_counts |
| BOLT-RULE-U003 | eager reports exactly a looping def of the file called in a Bool.pick branch. |
Proved | proved | src/rules/LAWS.bend eager_counts; src/rules/LAWS.bend eager_lambda; src/rules/LAWS.bend eager_comma; src/rules/LAWS.bend eager_plain |
| BOLT-RULE-U004 | concat reports exactly a self-call argument that appends onto the parameter in its own position: the append written as the argument, inside any number of parentheses, or a lone name whose nearest q = .. or +q = .. let before the call, in its statement chain or an enclosing one, has such an append as its right side. |
Proved | proved | src/rules/LAWS.bend concat_counts; src/rules/LAWS.bend concat_paren; src/rules/LAWS.bend concat_in_place; src/rules/LAWS.bend concat_via; src/rules/LAWS.bend concat_nearest; src/rules/LAWS.bend concat_other; src/rules/LAWS.bend concat_scope; src/rules/LAWS.bend concat_bound; src/rules/LAWS.bend concat_bound_plus |
| BOLT-RULE-U006 | fuel reports exactly an argument that is one Nat literal token alone, or the dotted name U32.to_nat then a ( group holding one U32 literal token (digits) alone, in a call (not a self-call) to a def of the file that returns no effect (its header holds no top-level -> token followed right away by the capitalized name token IO, nor ends in a -> whose first statement under the def starts with that token), at a parameter named fuel, gas, steps or budget or starting with fuel. |
Proved | proved | src/rules/LAWS.bend fuel_slots; src/rules/LAWS.bend fuel_walk_counts; src/rules/LAWS.bend fuel_counts |
| BOLT-RULE-U007 | index reports exactly a List.get or String.get at a non-literal index anywhere in a recursive def, except a List.get on a fixed table that table reports and a get that is the def's own self-call (the def is named List.get or String.get). |
Proved | proved | src/rules/LAWS.bend index_counts |
| BOLT-RULE-U008 | table reports exactly, in a def that calls itself, a List.get or List.set call whose index is not one number token and whose list is a fixed table: a list literal, a number-sized array, or List.replicate / Array.new / List.range with a number count, written inline, as a table def of the file, or held by the let of that name in scope. |
Proved | proved | src/rules/LAWS.bend table_walk_counts; src/rules/LAWS.bend table_counts |
| BOLT-RULE-U009 | hoist reports exactly, in a def that calls itself and is not a law or a proof, outside a lambda's body (the rest of a chain after =>), a case pattern, and a case arm that does not call the def: a List.get, List.set, String.get, Array.get or Array.set call whose collection is a table, and a let of one plain name to a table that a later get, set or name[..] in its block or the statements after it indexes; where a table is a list literal with eight or more top-level commas, an array literal of more than eight slots ([v : T*n] with n not a literal 0 to 8, [v : T^d] with d not a literal 0 to 3), a List.replicate, Array.new or List.range whose count is not a literal 0 to 8, a List.map or Array.map, or a call to a def of the file, other than an undotted self-call, whose body is a single statement that is a list literal, or an array literal, List.replicate, Array.new or List.range sized by a number literal, of more than eight cells by those measures; and every value name in the table (a callee or a ~ template aside) is a parameter that each self-call passes back unchanged in its own position. |
Proved | proved | src/rules/LAWS.bend hoist_counts |
| BOLT-RULE-U010 | ring reports exactly, in a def that calls itself, a self-call argument that appends onto a drop by a number literal, or a tail, of the parameter in its own position, when no match of the def has that parameter as a scrutinee. |
Proved | proved | src/rules/LAWS.bend ring_walk_counts; src/rules/LAWS.bend ring_counts |
| BOLT-RULE-U011 | rewalk reports exactly, in each straight piece of a def that is not a law or a proof (its body outside case arms, or one case arm's body), each call of a walk (a looping def of the file other than the def itself, or a listed Base walk) whose result is read for a single value (indexed on the spot, an accessor's collection argument, or alone the right of an = let of one name that is a record field or is read at least once and only indexed or as an accessor's collection argument) and follows no twin so read, when a twin keeps its result whole: another call in the piece, at another position, of the same walk on the same argument (the same text, and the same number of lets before it of each name in it). |
Proved | proved | src/rules/LAWS.bend rewalk_local_counts; src/rules/LAWS.bend rewalk_visit_counts; src/rules/LAWS.bend rewalk_counts |
| BOLT-RULE-U012 | unit reports exactly a multiply or divide by one on a recursive step. |
Proved | proved | src/rules/LAWS.bend unit_walk_counts; src/rules/LAWS.bend unit_counts |
| BOLT-RULE-U013 | scan reports exactly, outside a LAWS.bend or a PROOF.bend, in a def that calls itself and is not a proof, outside a lambda's body (the rest of a chain after =>), a case pattern, and a case arm that does not call the def: each call, a plain or dotted name token then a ( group, of a callee other than the def, one of whose walked arguments is exactly the lone name of a parameter that every self-call passes back as that same lone name in its own position (carried). A callee walks argument 2 of List.contains, List.find, List.filter and List.length, 3 of List.any and List.all, and 4 of List.foldl and List.foldr (the Base list searches); a def of the file walks, when it calls itself, its first live parameter that some self-call does not pass back unchanged, unless that parameter's type is Nat or String, and each parameter its body passes, anywhere, as the lone name of an argument a call of a Base search or of a def listed before it walks. One finding per call. |
Proved | proved | src/rules/LAWS.bend scan_counts; src/rules/LAWS.bend scan_quiet; src/rules/LAWS.bend scan_slots |
| BOLT-RULE-U015 | thunk (opt-in) reports exactly, in a def, a lambda whose body is exactly a self-call and whose parameter that call does not read, passed as the one lambda of a call: in the kids of a group opened by ( (its arguments: the kids split at their comma leaves), exactly one argument holding, among its own nodes and not inside a group, a leaf whose text is =>, four nodes in a row of those kids, a leaf of a name kind (the parameter), a leaf whose text is =>, a leaf whose text is the def's name, and a ( group, the kids ending right after the group or going on with a comma, and no name leaf in the group, at any depth, spelling the parameter or the parameter then a dot; such groups found at any depth; one finding for each, on the def's name, and nothing else. A call given two or more lambdas (a dispatch) gets none. |
Proved | proved | src/rules/LAWS.bend thunk_walk_counts; src/rules/LAWS.bend thunk_counts |
| BOLT-RULE-U016 | fromrev reports exactly, outside a LAWS.bend or a PROOF.bend, one finding (on the first) for each run of four tokens right after one another among the significant tokens (spaces, newlines and comments dropped) whose texts are String.from_list, (, List.reverse and (, and nothing else: anything between them, another ( included, is not the shape, and neither is List.reverse.go. |
Proved | proved | src/rules/LAWS.bend fromrev_counts; src/rules/LAWS.bend fromrev_exempt; src/rules/LAWS.bend inert_fromrev |
| BOLT-RULE-S001 | doc reports exactly a top-level def, type or law with no comment block right above it, or right above a run of @ lines (attributes such as @unsafe) right above it, with the header's exemptions. |
Proved | proved | src/rules/LAWS.bend doc_walk_counts; src/rules/LAWS.bend doc_counts |
| BOLT-RULE-S002 | space reports exactly trailing whitespace or a tab on any line, string literals and #| lines included, or a line over 120 columns with string literals counted as two, comments at full width, and #| lines not counted. |
Proved | proved | src/rules/LAWS.bend space_counts; src/rules/LAWS.bend space_line_counts; src/rules/LAWS.bend space_width_counts |
| BOLT-RULE-S003 | wrap reports exactly one finding for each def header that breaks its shape and none otherwise: a one-line header wider than 120 columns through its last : (the whole header when it has none), counted as space counts a line except that a comment counts zero, or a header across lines (one holding a newline token; a line break inside a string literal does not count) whose parameter list (opened by the first ( with no bracket open, split by the commas at its own depth) holds a parameter that spans lines, starts on the ( line, or starts on the line a later parameter starts on, or holds no parameter at all, or closes with its ) not on a line below the last parameter's last line, or with no -> (or, with no return type, the header's :) right after its ) on the ) line. |
Proved | proved | src/rules/LAWS.bend wrap_width; src/rules/LAWS.bend wrap_shape_counts; src/rules/LAWS.bend wrap_counts |
| BOLT-RULE-S004 | param reports exactly one finding for each parameter binder whose name is shorter than two characters, unless the name is one capital letter (a type parameter) or the parameter is bare or typed : Quant (a quantity), none for any other binder, and none at all in a PROOF.bend. |
Proved | proved | src/rules/LAWS.bend param_counts |
| BOLT-RULE-S005 | noqa reports exactly, at each noqa comment's line and column (BOLT-OUT-7), one finding for a bare one (#, any spaces, then noqa at the comment's end or before a space) and one for each code it names that no graded finding of its file on its line has, a code that is no rule's included, where a project rule's code (coverage, unsafe, trace) is judged only when the run is the whole tree and never in the editor, and nothing else. It runs after the filter, over the findings of every other rule, so its findings come last (BOLT-OUT-3) and no noqa comment silences them: a # noqa: S005 silences nothing and is itself reported. |
Proved | proved | src/LAWS.bend noqa_counts; src/LAWS.bend noqa_bare; src/LAWS.bend noqa_bare_text |
| BOLT-RULE-P001 | tail reports exactly a non-tail self-call outside any Bool.pick(..) in a def whose first live parameter's type is a List or String, whether or not the call shrinks it. |
Proved | proved | src/rules/LAWS.bend tail_walk_counts; src/rules/LAWS.bend tail_counts |
| BOLT-RULE-EXEMPT | For every text, a per-file rule's check on a path its header exempts returns no findings. The cost rules (pick, strict, eager, tail, concat, index, table, hoist, ring, rewalk, unit, scan, thunk) also skip, wherever it is, every def that is a proof: one whose signature returns a proof (-> {a == b : T}), or one written with no type at all (no : among its parameters and no ->, as def f(x, y):), which is how Bend fills the law named f; their "reports exactly" rows are read with that skip. |
Proved | proved | src/rules/LAWS.bend untyped_exempt; src/rules/LAWS.bend hole_exempt; src/rules/LAWS.bend doc_exempt; src/rules/LAWS.bend param_exempt; src/rules/LAWS.bend pick_exempt; src/rules/LAWS.bend tail_exempt; src/rules/LAWS.bend concat_exempt; src/rules/LAWS.bend eager_exempt; src/rules/LAWS.bend rewalk_exempt; src/rules/LAWS.bend strict_exempt; src/rules/LAWS.bend hoist_exempt; src/rules/LAWS.bend index_exempt; src/rules/LAWS.bend ring_exempt; src/rules/LAWS.bend table_exempt; src/rules/LAWS.bend unit_exempt; src/rules/LAWS.bend scan_exempt; src/rules/LAWS.bend thunk_exempt; src/rules/LAWS.bend fromrev_exempt |
| BOLT-RULE-INERT | For every rule whose pattern is code (all but escape, strings, chars, space, twice, foreign, noqa and rewalk), changing the contents of a comment or string literal does not change the findings. |
Proved | proved | src/rules/LAWS.bend inert_hole; src/rules/LAWS.bend inert_put; src/rules/LAWS.bend inert_tail; src/rules/LAWS.bend inert_pick; src/rules/LAWS.bend inert_strict; src/rules/LAWS.bend inert_doc; src/rules/LAWS.bend inert_param; src/rules/LAWS.bend inert_table; src/rules/LAWS.bend inert_index; src/rules/LAWS.bend inert_concat; src/rules/LAWS.bend inert_unit; src/rules/LAWS.bend inert_eager; src/rules/LAWS.bend inert_fuel; src/rules/LAWS.bend inert_ring; src/rules/LAWS.bend inert_arms; src/rules/LAWS.bend inert_unused; src/rules/LAWS.bend inert_hoist; src/rules/LAWS.bend inert_wrap; src/rules/LAWS.bend inert_scan; src/rules/LAWS.bend inert_thunk; src/rules/LAWS.bend inert_fromrev |
| ID | Requirement | Level | Status | Law |
|---|---|---|---|---|
| BOLT-LAW-1 | In every file under a law directory, except helpers, law files and tests, every def and type is named by a quantified law in a LAWS.bend or reached from one through calls. A quantified law names an item by a use in its statement that the binder (BOLT-SYN-5) resolves to that item, through an import alias or in the same file; a def calls an item by such a use on its own lines. A def is covered when such a law names it or a covered def calls it, in its own file or in another file of the run; a type is covered when such a law or a covered def names it or one of its constructors. | Proved | proved | src/rules/LAWS.bend coverage_reach; src/rules/LAWS.bend reach_from; src/rules/LAWS.bend reach_shut; src/rules/LAWS.bend reach_least; src/rules/LAWS.bend reach_digest; src/rules/LAWS.bend reach_binder |
| BOLT-LAW-2 | closed reports any law in a LAWS.bend with no binder. |
Proved | proved | src/rules/LAWS.bend closed_walk_counts; src/rules/LAWS.bend closed_counts |
| BOLT-LAW-3 | An @unsafe def or a foreign def (a def whose body is only imports of .c or .js files) reachable by relative imports from a law file in the run is a finding, at the def, that names the first such law file and the import path from it to the def's file. |
Proved | proved | src/rules/LAWS.bend unsafe_reports; src/rules/LAWS.bend unsafe_from; src/rules/LAWS.bend unsafe_shut; src/rules/LAWS.bend unsafe_least |
| BOLT-LAW-5 | Run over the whole tree, the traceability rule reports exactly one finding for each defect of SPEC.md, in the format stated under "Tagging and traceability", against the laws read, and nothing else: a table row with the wrong number of cells; a row whose ID does not match the pattern; a requirement or trust row whose ID another row of its table kind also has; a requirement row that is neither Proved with status proved or pending nor Trusted with an empty status, a proved row that names no law, and a Trusted row that names one; a Trusted row with no trust row; for each Law entry of a Proved row, proved or pending, an entry that is not <path> <law>, a path no LAWS.bend read has, or a law it lacks, else one for no for/exs binder and one for no tag of the row; and a tag naming an ID no Proved row, proved or pending, lists. A pending row may name laws that prove part of it and a tag may name a pending row. With no SPEC.md it reports that once; over files named on the line, nothing. |
Proved | proved | src/rules/LAWS.bend trace_pending_judged; src/rules/LAWS.bend trace_pending_shape; src/rules/LAWS.bend trace_proved_shape; src/rules/LAWS.bend trace_trusted_shape; src/rules/LAWS.bend trace_pending_claimed; src/rules/LAWS.bend trace_trusted_unclaimed; src/rules/LAWS.bend trace_unlisted_unclaimed; src/rules/LAWS.bend trace_counts; src/rules/LAWS.bend trace_unread; src/rules/LAWS.bend trace_named |
| ID | Requirement | Level | Status | Law |
|---|---|---|---|---|
| BOLT-CFG-1 | A rule's level is its own setting, else its group's setting, else its group's default. | Proved | proved | src/LAWS.bend set_level_none; src/LAWS.bend set_level_first; src/LAWS.bend set_level_skip; src/LAWS.bend level_own; src/LAWS.bend level_group; src/LAWS.bend level_default |
| BOLT-CFG-2 | Grading drops a finding at off and attaches the level to every other. |
Proved | proved | src/LAWS.bend graded_keeps |
| BOLT-CFG-3 | A level word that is not off or warn grades as error. |
Proved | proved | src/LAWS.bend word_error |
| BOLT-CFG-4 | A finding is graded by the nearest readable bolt.bend in its file's directory, then each parent, and only that one applies. | Proved | proved | src/LAWS.bend absolute_root; src/LAWS.bend absolute_under; src/LAWS.bend home_empty; src/LAWS.bend home_here; src/LAWS.bend home_up; src/LAWS.bend home_down; src/LAWS.bend chain_parent; src/LAWS.bend nearest_grades |
| BOLT-CFG-5 | Group defaults are correctness at error, pedantic off, and the rest at warn. | Proved | proved | src/LAWS.bend default_correctness; src/LAWS.bend default_pedantic; src/LAWS.bend default_rest |
| BOLT-CFG-6 | An opt-in rule is off unless its own setting names it. | Proved | proved | src/LAWS.bend level_own; src/LAWS.bend opt_in_off |
| BOLT-CFG-7 | A setting in a bolt.bend whose name is no rule or group is a finding: of the settings grading reads from a bolt.bend (each def whose body holds a string), unknown holds exactly those whose name is neither the slug nor the group of any row of the code table, in file order, one each. |
Proved | proved | src/LAWS.bend unknown_exact; src/LAWS.bend settings_graded |
| ID | Requirement | Level | Status | Law |
|---|---|---|---|---|
| BOLT-SCOPE-1 | With no files named, bolt lints every .bend file under . found within the first 100000 directories the walk reads, not descending into hidden directories or node_modules, sorted by code point; past that bound the walk stops silently. |
Proved | proved | src/LAWS.bend walk_files |
| BOLT-SCOPE-2 | A per-file rule sees one file's Src; a project rule sees the digests of every file in the run; setting sees the text of each bolt.bend grading reads; and nothing else. |
Proved | proved | src/LAWS.bend scope_findings |
| BOLT-SCOPE-3 | When the files in the run include a LAWS.bend, every file in the run that is not exempt is under law; otherwise none is. | Proved | proved | src/LAWS.bend under_law_all |
| BOLT-SCOPE-4 | Path exemptions are decided by the path alone, never by content: two files at one path are exempt from law alike whatever each holds, and on a path a per-file rule's header exempts (a LAWS.bend, a PROOF.bend, a file under a tests directory, and for closed any file but a LAWS.bend) that rule's findings are the same for every source. What a rule reads from content to skip a def, a line or a file (a def that is a proof, returning one or written with no type, a file that defines Map.put, # lanes: native, main and dotted names) is that rule's behavior, not a path exemption. |
Proved | proved | src/rules/LAWS.bend scope_digest_exempt; src/rules/LAWS.bend scope_hole; src/rules/LAWS.bend scope_doc; src/rules/LAWS.bend scope_param; src/rules/LAWS.bend scope_law_file; src/rules/LAWS.bend scope_closed |
| BOLT-SCOPE-5 | A bolt.bend is read, never linted, even when named. | Proved | proved | src/LAWS.bend no_config_linted |
| ID | Requirement | Level | Status | Law |
|---|---|---|---|---|
| BOLT-OUT-1 | The code table maps each rule slug to exactly one code and each code to exactly one slug. | Proved | proved | src/LAWS.bend slug_finds_row; src/LAWS.bend code_finds_row |
| BOLT-OUT-6 | A released code is never renumbered or reused. | Trusted | ||
| BOLT-OUT-2 | A finding prints as path:line:col: level: CODE: message, 1-based. |
Proved | proved | src/LAWS.bend shown |
| BOLT-OUT-3 | Output order is read failures, then per-file findings in file-list order and Rules.on order, then setting's findings (C011), then coverage, unsafe and trace, less the findings a noqa comment silences (BOLT-OUT-7), then noqa's findings (S005) in file-list order. |
Proved | proved | src/LAWS.bend lines_in_order |
| BOLT-OUT-4 | The last line is clean or N errors, M warnings, and the exit status is 1 exactly when some graded finding is an error, counting the findings BOLT-OUT-3 prints. |
Proved | proved | src/LAWS.bend last_line_summary; src/LAWS.bend exit_on_error |
| BOLT-OUT-5 | A path that cannot be read is a read finding graded with correctness. |
Proved | proved | src/LAWS.bend unread_one_finding; src/LAWS.bend directory_one_finding; src/LAWS.bend read_is_correctness |
| BOLT-OUT-7 | A finding whose line carries a # noqa: comment naming its code is not reported and not counted: a comment token whose text is #, any spaces, noqa: and then codes (runs of ASCII letters and digits, case-sensitive, split by commas with spaces around them allowed, any text after) silences every graded finding of its own file on its own line whose code it names, once every rule has run, the project rules included, and the summary and the exit status count only what remains. The filter reads comment tokens only, so a noqa inside a string literal is never one and no rule's findings change. |
Proved | proved | src/LAWS.bend noqa_comments; src/LAWS.bend noqa_codes; src/LAWS.bend noqa_bare; src/LAWS.bend noqa_bare_text; src/LAWS.bend noqa_keeps; src/LAWS.bend lines_in_order; src/LAWS.bend last_line_summary; src/LAWS.bend exit_on_error |
| ID | Requirement | Level | Status | Law |
|---|---|---|---|---|
| BOLT-CLI-1 | bolt accepts bolt [lint] [files], bolt check files, bolt lsp, bolt help [cmd], --help and --; an argv parse error exits 1, and help, --help and --version exit 0. What shake answers for each argv is BOLT-TRUST-8; the laws prove what bolt does with that answer. |
Proved | proved | src/LAWS.bend cli_bare; src/LAWS.bend cli_bare_raw; src/LAWS.bend cli_lint; src/LAWS.bend cli_lint_raw; src/LAWS.bend cli_check; src/LAWS.bend cli_check_raw; src/LAWS.bend cli_lsp; src/LAWS.bend cli_lsp_word; src/LAWS.bend cli_help; src/LAWS.bend cli_dash_help; src/LAWS.bend cli_version; src/LAWS.bend cli_error_exits; src/LAWS.bend cli_help_exits; src/LAWS.bend cli_version_exits; src/LAWS.bend cli_runs; src/LAWS.bend cli_files |
| BOLT-CLI-2 | --version prints the release and, when the build has one, the short commit in parentheses. |
Proved | proved | src/LAWS.bend cli_version; src/LAWS.bend cli_version_exits; src/LAWS.bend version_release; src/LAWS.bend version_commit |
| BOLT-CLI-3 | bolt reads the arguments after the program, which IO.args names first (bend 2.0.32). --help before the line's first -- asks for the page bolt help prints, for the subcommand named first when there is one, else the root's; after -- it is a file, and a line with no such --help is parsed as it is. |
Proved | proved | src/LAWS.bend cli_args_program; src/LAWS.bend cli_line_plain; src/LAWS.bend cli_help_flag; src/LAWS.bend cli_help_dashes; src/LAWS.bend cli_help_flag_path; src/LAWS.bend cli_help_cmd; src/LAWS.bend cli_dash_help |
| ID | Requirement | Level | Status | Law |
|---|---|---|---|---|
| BOLT-CHK-1 | bolt check prints one path:line:1: error: line per error bend reports, on the line bend marks, then a count; it exits 1 when there is any, and treats a failure to run bend as an error. |
Proved | proved | src/LAWS.bend check_lines; src/LAWS.bend check_one_each; src/LAWS.bend check_clean; src/LAWS.bend check_one; src/LAWS.bend check_many; src/LAWS.bend check_unrun_error; src/LAWS.bend check_run_of; src/LAWS.bend check_run_unrun; src/LAWS.bend check_exec_ran; src/LAWS.bend check_exec_unrun; src/LAWS.bend check_exec_died; src/LAWS.bend check_exec_died_reported; src/LAWS.bend check_exec_untagged; src/LAWS.bend check_proof_unrun; src/LAWS.bend check_marked; src/LAWS.bend check_marked_line; src/LAWS.bend check_import_first; src/LAWS.bend check_own_marked |
| ID | Requirement | Level | Status | Law |
|---|---|---|---|---|
| BOLT-SYN-1 | Lex.text(Lex.tokens(s)) == s for every s. |
Proved | proved | src/syntax/LAWS.bend lossless |
| BOLT-SYN-2 | A token's line and column are those of its first character, 0-based, in code points. | Proved | proved | src/syntax/LAWS.bend positions |
| BOLT-SYN-3 | The tree drops no token: its leaves are the significant tokens in order, except that each token that is a run of > (a close of angle groups or an operator such as >>) becomes one > leaf per character at consecutive columns. |
Proved | proved | src/syntax/LAWS.bend leaves |
| BOLT-SYN-4 | The outline lists every column-0 import, def, type, law and @unsafe def. |
Proved | proved | src/syntax/LAWS.bend outline |
| BOLT-SYN-5 | The binder resolves a use to the innermost binder, then a file item, then an alias qualifier, else free. | Proved | proved | src/syntax/LAWS.bend resolves; src/syntax/LAWS.bend uses; src/syntax/LAWS.bend extends; src/syntax/LAWS.bend shadows; src/syntax/LAWS.bend restores; src/syntax/LAWS.bend lets; src/syntax/LAWS.bend groups |
| BOLT-SYN-6 | Every function in src/syntax/ terminates on every input without fuel. |
Trusted |
| ID | Requirement | Level | Status | Law |
|---|---|---|---|---|
| BOLT-LSP-1 | Content-Length counts UTF-8 bytes; a partial header or body waits; cut of wrap(s) gives s. |
Proved | proved | src/lsp/LAWS.bend frame_counts; src/lsp/LAWS.bend frame_round; src/lsp/LAWS.bend frame_waits |
| BOLT-LSP-2 | Diagnostics for an open document equal the CLI's per-file findings for that file and text under the same bolt.bend, less what its noqa comments silence (BOLT-OUT-7), then noqa's findings on them, which judge no project rule's code. |
Proved | proved | src/lsp/LAWS.bend lint_is_cli |
| BOLT-LSP-3 | Each request gets exactly one response with the same id, in order; an unknown request gets -32601; an unknown notification gets nothing. | Proved | proved | src/lsp/LAWS.bend replies_pair; src/lsp/LAWS.bend unknown_refused |
| BOLT-LSP-4 | Open and save publish checker plus lint; change publishes lint plus the last checker result; close publishes an empty list; an open bolt.bend gets no lint. | Proved | proved | src/lsp/LAWS.bend open_publishes; src/lsp/LAWS.bend save_publishes; src/lsp/LAWS.bend change_publishes; src/lsp/LAWS.bend open_keeps; src/lsp/LAWS.bend save_keeps; src/lsp/LAWS.bend change_keeps; src/lsp/LAWS.bend close_publishes; src/lsp/LAWS.bend config_unlinted |
| BOLT-LSP-5 | The checker never runs main. |
Proved | proved | src/lsp/LAWS.bend check_only; src/lsp/LAWS.bend followup_check_only |
| BOLT-LSP-6 | Hover, definition, references and completion answer from the binder (BOLT-SYN-5) over the open text and its relative imports. | Proved | proved | src/lsp/LAWS.bend nav_open_text; src/lsp/LAWS.bend nav_definition_binder; src/lsp/LAWS.bend nav_definition_local; src/lsp/LAWS.bend nav_definition_item; src/lsp/LAWS.bend nav_definition_import; src/lsp/LAWS.bend nav_definition_free; src/lsp/LAWS.bend nav_import_open; src/lsp/LAWS.bend nav_hover_use; src/lsp/LAWS.bend nav_hover_binder; src/lsp/LAWS.bend nav_hover_item; src/lsp/LAWS.bend nav_hover_own; src/lsp/LAWS.bend nav_references; src/lsp/LAWS.bend nav_completion; src/lsp/LAWS.bend nav_completion_import |
| BOLT-LSP-7 | Positions are in the encoding the client negotiated. | Proved | proved | src/lsp/LAWS.bend enc_negotiated; src/lsp/LAWS.bend enc_advertised; src/lsp/LAWS.bend enc_kept; src/lsp/LAWS.bend enc_round; src/lsp/LAWS.bend enc_sent; src/lsp/LAWS.bend enc_read; src/lsp/LAWS.bend enc_tokens; src/lsp/LAWS.bend enc_utf32 |
| BOLT-LSP-8 | On a line with no character past U+FFFF, a column counted in UTF-16 units equals the column counted in characters, both sent and read. | Proved | proved | src/lsp/LAWS.bend enc_narrow |
| ID | Requirement | Level | Status | Law |
|---|---|---|---|---|
| BOLT-LIB-1 | Lazy.stop(c, a, _ => b) == Bool.pick(c, a, b), Lazy.or_else(a, _ => b) == Bool.or(a, b) and Lazy.and_then(a, _ => b) == Bool.and(a, b) for all inputs. |
Proved | proved | src/lazy/LAWS.bend stop_is_pick; src/lazy/LAWS.bend or_else_is_or; src/lazy/LAWS.bend and_then_is_and |
| BOLT-LIB-2 | Lazy.stop, Lazy.or_else and Lazy.and_then apply their thunk only on the branch that needs it. |
Trusted |
These assumptions sit outside the proofs. They are the complete list of Trusted requirements, and a passing proof gate says nothing about them.
| ID | Assumption | Why it is trusted |
|---|---|---|
| BOLT-TRUST-1 | The Bend checker is sound. | It cannot be checked from inside Bend; this is EZ-TRUST-1. bolt pins bend through the flake. |
| BOLT-TRUST-2 | bolt's lexer, tree and outline read a file as the program bend reads, for the constructs the rules depend on. | bolt cannot call bend's parser from Bend. Checked against bend 2.0.25: a string literal runs across newlines to its closing quote, and the outline reads no line that starts inside one; a > inside (..), [..] or {..} within <..> is an operator and does not close the angle group; names are ASCII in both, since bend rejects a non-ASCII letter in a def name, a parameter or a let binder. One divergence remains: bend accepts a char literal holding a raw newline, which bolt's lexer ends at the end of its line. One is a decided difference: a line indented deeper, outside brackets, is a child statement in bolt's tree ("a" then ++ "b" is ["a" {[++ "b"]}]), where bend reads one expression. The rules that read statements from the tree could be affected (tail, unused, table, rewalk, wrap); run on a continued ++, <> or boolean or, a continued let value, a lambda body and a call argument, tail, strict, concat, unused and param report what they report on one line, and wrap reports a header whose -> T: sits on the next line, which its requirement makes a finding. |
| BOLT-TRUST-3 | The directory listing effect (src/walk/dir.c, dir.js) returns a directory's entries, marking directories with /, the OS tells the truth when the directory probe (src/walk/disk.bend is_dir) asks whether a path is a folder, and the file read effect returns a file's text. |
The walk and the reads are foreign code; the planner takes their answers as given. |
| BOLT-TRUST-4 | The LSP transport (src/lsp/transport/fd.c, fd.js) delivers stdin bytes in order and writes stdout bytes whole. |
Foreign code over descriptors 0 and 1. |
| BOLT-TRUST-5 | bend <file> --check-only never runs main, and prints its report in the shape src/lsp/report.bend parses, naming a def in Location: the way src/lsp/checker/names.bend builds its names. |
bend is a separate program, and the report format has already drifted once (report_import). |
| BOLT-TRUST-6 | The proof gate runner runs bend on every PROOF.bend and accepts only an exact ALL PROOFS CHECK first line. |
It is the flake's proofs check, a shell loop over every PROOF.bend on the flake's bend (2.0.35), until ez's mkProofs runs on that bend. CI builds from a clean tree. |
| BOLT-TRUST-7 | Every commit on main passed ci.yml. |
The repository ruleset "main: require ci" requires the check / check job on main (since 2026-09-22). release-please PRs, which get no CI run, merge through an admin pull-request bypass. |
| BOLT-TRUST-8 | shake v0.2.0 (0x085b03c84ca37125e38dddede7b91e55) parses argv as its proved rows say: SHAKE-TOK-1, SHAKE-TOK-3, SHAKE-TOK-4, SHAKE-PARSE-2, SHAKE-PARSE-3, SHAKE-PARSE-4, SHAKE-PARSE-8, SHAKE-GET-1, SHAKE-GET-2 and SHAKE-ERR-1; ezjson v1.1.0 (0x81c67699424929b5c44cd8577e18117f) parses and prints JSON correctly. |
Pinned dependencies, by ez.toml hash, each proving its own rows in its own gate at the pinned tag. bolt reads shake through main.bend only and never unfolds its parser: the BOLT-CLI laws that name an argv take the answer those rows guarantee as premises, each citing its row, and prove what bolt does with it. |
| BOLT-TRUST-9 | Each interpreter answers the World's questions and executes plans faithfully. | It makes no decisions and is kept small enough to review line by line. The listing and read effects it calls are BOLT-TRUST-3. |
| BOLT-OUT-6 | A released code is never renumbered or reused. | A property across versions, enforced by review of the SPEC row that lists the table. |
| BOLT-SYN-6 | Every function in src/syntax/ terminates on every input without fuel. |
Termination is what the Bend checker's structural-recursion check establishes, so this rests on BOLT-TRUST-1 and needs no law of its own. |
| BOLT-LIB-2 | The lazy branches apply their thunk only on the branch that needs it. | A law states what a term equals, not what evaluation skipped, so Bend cannot state it. src/lazy/lazy.bend matches on the Bool before it applies the thunk, and BOLT-LIB-1 proves the values agree with the strict forms. |