diff --git a/AGENTS.md b/AGENTS.md index 250b633..becdf99 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -26,8 +26,8 @@ A `#|` equality for a proveable claim is a bug. A directory with - A `LAWS.bend` is human-owned: do not edit it to make a proof pass. Every law is quantified; `closed` reports one that is not. -- Every `PROOF.bend` in the tree is gated (`bend PROOF.bend` prints "All - terms check."), so a fixture holding a proof meant to fail cannot live here. +- Every `PROOF.bend` in the tree is gated (`bend PROOF.bend` prints `ALL + PROOFS CHECK`), so a fixture holding a proof meant to fail cannot live here. - Anything under a `tests/` directory is a test, and only the stay list may have one; `ez test` runs each on its own and caches none. Fixtures a test reads are not tests, so they live beside it -- `src/lsp/fixtures/`, not diff --git a/SPEC.md b/SPEC.md index 86ccf96..c713563 100644 --- a/SPEC.md +++ b/SPEC.md @@ -37,7 +37,7 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n | 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, in a call (not a self-call) to a def of the file, 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-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, 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. | 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 | @@ -59,7 +59,7 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n | :---- | :---- | :---- | :---- | :---- | | 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` reachable by relative imports from a law file in the run is a finding. | 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-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 ` `, 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 | ### Grading and config (BOLT-CFG) diff --git a/docs/rfc/bolt-spec.md b/docs/rfc/bolt-spec.md index 2116916..bf3784e 100644 --- a/docs/rfc/bolt-spec.md +++ b/docs/rfc/bolt-spec.md @@ -48,7 +48,7 @@ bolt has 271 laws, and 257 of them are closed: each pins one call on one input, | `#\|` test | A test written as a `#\|` trailer comment beside the code, which a test runner evaluates. bolt#10 moved most of bolt's into closed laws. | | Closed law | A law with no `for` or `exs` binder. It holds for one input, which makes it a unit test checked at compile time. | | Quantified law | A law with at least one binder. It holds for every input of that type. | -| Proof gate | For every PROOF.bend, `bend PROOF.bend` prints exactly `All terms check.` as its first line. | +| Proof gate | For every PROOF.bend, `bend PROOF.bend` prints exactly `ALL PROOFS CHECK` as its first line. | | Proved | A requirement backed by a quantified law tagged with its ID, passing the proof gate. | | Trusted | A requirement that is assumed, listed in the trust boundary, and checked by nothing in bolt. | | Pending | The status of a Proved requirement whose law has not landed. It is a status, not a level. | @@ -109,7 +109,7 @@ The proposal has five parts, four of them carried over from ez. A **specificatio | | |:---:| -| 
┌──────────┐     ┌───────────────┐          ┌────────────────┐     ┌────────────────┐
│ SPEC.md  │────▶│ Requirement   │──Proved─▶│ LAWS.bend      │────▶│ PROOF.bend     │
│ (IDs +   │     │ ID + level    │          │ (quantified,   │     │ (gate: "All    │
│  levels) │     │               │          │  # BOLT-X-N)   │     │  terms check.")│
└──────────┘     └───────┬───────┘          └────────────────┘     └────────────────┘
                         │                          ▲
                      Trusted                       │ checked by
                         ▼                          │
                 ┌───────────────┐          ┌────────────────┐
                 │ Trust boundary│          │ bolt: closed + │
                 │ (in SPEC.md)  │          │ traceability   │
                 └───────────────┘          └────────────────┘
| +| 
┌──────────┐     ┌───────────────┐          ┌────────────────┐     ┌────────────────┐
│ SPEC.md  │────▶│ Requirement   │──Proved─▶│ LAWS.bend      │────▶│ PROOF.bend     │
│ (IDs +   │     │ ID + level    │          │ (quantified,   │     │ (gate: "ALL    │
│  levels) │     │               │          │  # BOLT-X-N)   │     │  PROOFS CHECK")│
└──────────┘     └───────┬───────┘          └────────────────┘     └────────────────┘
                         │                          ▲
                      Trusted                       │ checked by
                         ▼                          │
                 ┌───────────────┐          ┌────────────────┐
                 │ Trust boundary│          │ bolt: closed + │
                 │ (in SPEC.md)  │          │ traceability   │
                 └───────────────┘          └────────────────┘
| | Caption: Every requirement ends in a tagged quantified law the proof gate checks, or in a named assumption. bolt's own rules check that the tags and binders are there. | ### Two levels, and the positions carried over from ez @@ -118,7 +118,7 @@ We take ez's positions as settled rather than re-argue them, since the two speci The other positions follow from keeping only those two levels. Closed laws have no standing, because a law about one input is a test, and tests and fixtures are never evidence for a requirement for the same reason. Untagged quantified laws are allowed, but nothing protects them, so a change may edit or delete them freely. A guarantee proved in a pinned dependency is Trusted from bolt's side, because bolt's gate does not re-check the dependency's proofs. -The proof gate is the one mechanical check the spec depends on: every PROOF.bend's first output line is exactly `All terms check.`, which rules out the `All terms check, but N defs rely on unsafe or foreign code:` form bend exits 0 with. bolt does not run that gate itself. `flake.nix` calls ez's `mkProofs`, which runs `ez test --unit-only` today and `ez prove` once ez ships it, and that runner's faithfulness is BOLT-TRUST-6. +The proof gate is the one mechanical check the spec depends on: every PROOF.bend's first output line is exactly `ALL PROOFS CHECK`, which rules out `SOME PROOFS FAIL` (bend 2.0.34 prints it, then the reason, `Error: N defs rely on unsafe or foreign code:` or `Error: N TODOs found.` among them, and exits 1; before 2.0.32 a proof leaning on unsafe or foreign code printed `All terms check, but N defs rely on unsafe or foreign code:` and exited 0). bolt does not run that gate itself. `flake.nix` calls ez's `mkProofs`, which runs `ez test --unit-only` today and `ez prove` once ez ships it, and that runner's faithfulness is BOLT-TRUST-6. ### Closed laws and the `closed` rule @@ -474,7 +474,7 @@ These assumptions sit outside the proofs. They are the complete list of Trusted | BOLT-TRUST-3 | The directory listing effect (`bolt/walk/dir.c`, `dir.js`) returns a directory's entries, marking directories with `/`, 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 (`bolt/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 --check-only` never runs `main`, and prints its report in the shape `bolt/lsp/report.bend` parses. | 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 terms check.` first line. | It is ez code run by `mkProofs` (`ez test --unit-only` today, `ez prove` when ez ships it). CI builds from a clean tree. | +| 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 ez code run by `mkProofs` (`ez test --unit-only` today, `ez prove` when ez ships it). CI builds from a clean tree. | | BOLT-TRUST-7 | Every commit on `main` passed `ci.yml`. | Holds only once the ruleset in REVIEW-8 exists. Today it does not hold. | | 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-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. | diff --git a/src/README.md b/src/README.md index 8665b0c..de41783 100644 --- a/src/README.md +++ b/src/README.md @@ -152,7 +152,8 @@ parameters and no `->`), which is how Bend fills the law named `f`. a law's `for` names, and every parameter of a foreign def, one whose body starts with `import` (its C and JS read them), however its header is wrapped. -- `hole` — a TODO hole left in code, the one bend counts in "N TODO found": +- `hole` — a TODO hole left in code, the one bend counts in "1 TODO found." / + "N TODOs found." (under `SOME PROOFS FAIL`, exit 1): `?` and then `TODO`, with spaces, newlines or comments allowed between (`?TODO`, `? TODO`). `?todo` and `?TODO_later` are other names, a type error to bend, and are not reported. LAWS.bend is exempt: its laws are open @@ -307,14 +308,17 @@ parameters and no `->`), which is how Bend fills the law named `f`. reverse: the missing lane cannot run it. A file headed `# lanes: native` needs no `.js`: that exact line must be one of the comment lines before the file's first non-comment line. -- `fuel` — a `Nat` literal (digits, then `n`) passed in a call, `name(..)`, - to a fuel parameter of a def of the same file. A fuel parameter is known by - its name alone, the one before its colon: `fuel`, `gas`, `steps` or - `budget`, or any name starting with `fuel`. Input past it is cut short - with no error: derive the fuel from the input. A literal of any size counts, - `3n` included. Only an argument that is one literal token alone counts, so - `U32.to_nat(1000)`, a let-bound literal and `(7n)` are not seen. A def's - own calls are exempt. +- `fuel` — a `Nat` literal (digits, then `n`), or `U32.to_nat` of a U32 + literal (`U32.to_nat(100000)`), passed in a call, `name(..)`, to a fuel + parameter of a def of the same file. A fuel parameter is known by its name + alone, the one before its colon: `fuel`, `gas`, `steps` or `budget`, or + any name starting with `fuel`. Input past it is cut short with no error: + derive the fuel from the input. In a law it is worse: a lemma proved over + every fuel, used at a big fixed one against a goal written another way, + overflows the checker's stack (bend 2.0.33/2.0.34). A literal of any size + counts, `3n` included. Only an argument that is the literal alone, or + `U32.to_nat(` it `)`, counts, so a let-bound literal and `(7n)` are not + seen. A def's own calls are exempt. - `tail` (pedantic) — a self-call that is not a tail call, in a def whose first live parameter is a `List` or a `String`. On a long one the JS lane overflows its stack (a 48 KB header crashed a server; ~4,900 entries and @@ -338,11 +342,16 @@ parameters and no `->`), which is how Bend fills the law named `f`. (proved or pending) ` ` entry that is missing, has no binder or lacks the tag, a Trusted row with no trust row, and a tag SPEC.md does not list as a Proved row, proved or pending. -- `unsafe` (project) — an `@unsafe def` that a LAWS.bend or PROOF.bend - reaches through its imports. There the checker prints "All terms check, - but N defs rely on unsafe or foreign code:" and a `- name` list (2.0.16 - counted marks: "with N unsafe annotations.") and exits 0, so a gate that - reads the exit status goes green on an unproven claim. +- `unsafe` (project) — an `@unsafe def` or a foreign def (a body of only + `import "./x.c"` / `import "./x.js"` lines) that a LAWS.bend or PROOF.bend + reaches through its relative imports, over the files bolt read. Since bend + 2.0.32 such a proof fails: bend prints `SOME PROOFS FAIL`, then `Error: N + defs rely on unsafe or foreign code:` and a `- name` list, and exits 1 + (2.0.34), every def of every imported module counted. That list names the + defs, not the import that brought the effect in; the finding names the + import path from the law file (`LAWS.bend -> mid.bend -> eff/io.bend`). Move + the effect into a sibling module no law file imports and pass it in as a + service. Hash imports (`import 0x.../path`) are not followed. - `coverage` (project) — in a project that states laws (a LAWS.bend among the files bolt read), a def or a type that no law reaches. It is `coverage`, not `law`, because `law` is a Bend keyword: `def law()` is no def, so a bolt.bend diff --git a/src/lsp/files/disk.bend b/src/lsp/files/disk.bend index 11cfb2a..c39e8b7 100644 --- a/src/lsp/files/disk.bend +++ b/src/lsp/files/disk.bend @@ -57,7 +57,7 @@ def read.opened(rr: Result<&1, &1, U32 & String, File>) -> IO(Maybe<&2, String>) case Fail{e}: IO.pure(Maybe<&2, String>, None{}) case Done{file}: - slurp(U32.to_nat(100000), file, []) + slurp(U32.to_nat(100000), file, []) # noqa: U006 100000 reads of 64 KiB, past any source # a file's text, or None when it cannot be opened def read(path: String) -> IO(Maybe<&2, String>): # noqa: L001 disk effect diff --git a/src/lsp/transport/stdio.bend b/src/lsp/transport/stdio.bend index 840163c..c154cab 100644 --- a/src/lsp/transport/stdio.bend +++ b/src/lsp/transport/stdio.bend @@ -71,7 +71,7 @@ def recv.loop(fuel: Nat, h2: Stdio) -> IO(Stdio & Maybe<&2, String>): # the fuel bounds the reads one message may take def recv(h2: Stdio) -> IO(Stdio & Maybe<&2, String>): # noqa: L001 transport effect - recv.loop(U32.to_nat(1000000), h2) + recv.loop(U32.to_nat(1000000), h2) # noqa: U006 a million reads for one message def send.done(ww: File & Result<&1, &1, U32 & String, Unit>, inp: File, buf: List<&2, U32>) -> IO(Stdio): (out, r) = ww diff --git a/src/rules/LAWS.bend b/src/rules/LAWS.bend index a9fe88a..cfe2ec4 100644 --- a/src/rules/LAWS.bend +++ b/src/rules/LAWS.bend @@ -1993,7 +1993,8 @@ law ring_counts: # then a `(` group, that is not a call of the statement's own name (a # self-call): for each fuel parameter of a def of that name, one finding when # the argument in its position (Calls.args, split at top-level commas) is one -# Nat literal token alone, digits then `n`. +# Nat literal token alone, digits then `n`, or the dotted name `U32.to_nat` +# then a `(` group holding one U32 literal token alone, digits only. # is the name a fuel parameter's: `fuel`, `gas`, `steps` or `budget`, or one # starting with `fuel`? @@ -2019,16 +2020,29 @@ def fuel.slots(ds: List<&2, Calls.Def>) -> List<&2, FuelRule.Fuel>: case Con{Calls.Def{name, sig, body}, rest}: List.append(&2, FuelRule.Fuel, fuel.slots.of(Calls.params(sig), name, 0n), fuel.slots(rest)) -# is the argument one Nat literal token alone, digits then `n`? +# does a call's group hold one number token alone, digits only (a U32 +# literal), when ok says the call is `U32.to_nat(`? +def fuel.conv(kids: Tree.Node, ok: Bool) -> Bool: + match kids: + case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TNum{}, +t, l, c}}, Tree.NNil{}}: + Bool.and(ok, T.digits_ok(String.to_list(t))) + case other: + False{} + +# is the argument one Nat literal token alone, digits then `n`, or the +# dotted name `U32.to_nat` then a `(` group holding one U32 literal alone? def fuel.lone(aa: Tree.Node) -> Bool: match aa: case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TNum{}, +t, l, c}}, Tree.NNil{}}: T.nat_ok(String.to_list(t)) + case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TDotted{}, +t, l, c}}, + Tree.NCons{Tree.Group{Lex.Tok{ok, +o, ol, oc}, kids, cl}, Tree.NNil{}}}: + fuel.conv(kids, Bool.and(String.eq(t, "U32.to_nat"), String.eq(o, "("))) case other: False{} # how many fuel parameters of defs named name a call with these arguments -# fills with a lone Nat literal +# fills with a fixed number (fuel.lone) def fuel.hits(fs: List<&2, FuelRule.Fuel>, +name: String, +as: List<&2, Tree.Node>) -> Nat: match fs: case Nil{}: @@ -2037,7 +2051,7 @@ def fuel.hits(fs: List<&2, FuelRule.Fuel>, +name: String, +as: List<&2, Tree.Nod +m = fuel.hits(rest, name, as) Bool.pick(Nat, Bool.and(String.eq(fn, name), fuel.lone(Calls.arg(as, at))), 1n+m, m) -# how many lone Nat literals the calls under the node pass for fuel, at any +# how many fixed numbers the calls under the node pass for fuel, at any # depth: a call is a name token then a `(` group, and a call of self is not # counted def fuel.count(nn: Tree.Node, +fs: List<&2, FuelRule.Fuel>, +self: String) -> Nat: @@ -2084,7 +2098,8 @@ law fuel_slots: {FuelRule.fuels(ds) == fuel.slots(ds) : List<&2, FuelRule.Fuel>} # LAW: over any chain, fuel reports one finding for each fuel parameter a -# call (not of self) fills with a lone Nat literal, and none for anything else +# call (not of self) fills with a lone Nat literal or `U32.to_nat` of a lone +# U32 literal, and none for anything else # BOLT-RULE-U006 law fuel_walk_counts: for nn: Tree.Node @@ -2660,15 +2675,23 @@ def coverage.lawful(ds: List<&2, Digest.Digest>) -> Bool: # unsafe (BOLT-LAW-3). Over every list of digests, as coverage's laws are. # A digest records a file's relative imports (normalized, `deps`) and its -# `@unsafe def`s; the import graph is theirs, and the closure a law file +# `@unsafe def`s and foreign defs (a def whose body is only imports of `.c` +# or `.js` files); the import graph is theirs, and the closure a law file # reaches over it is Imports.closure.go's, the walk every project rule -# shares. +# shares. A finding names the import path from the law file to the def's +# file, a shortest one, as Imports.trail walks it. # every file of the digests the file at from reaches by relative imports, # itself first, as the closure walk takes it def unsafe.closure(+all: List<&2, Digest.Digest>, from: String) -> List<&2, String>: Imports.closure.go(Digest.edges(all), Imports.paths(Digest.edges(all)), List.length(&2, Digest.Digest, all), from) +# the import path from the file at from to the file at to, over the digests, +# as the finding spells it: `a -> b -> c` +def unsafe.via(+all: List<&2, Digest.Digest>, +from: String, +to: String) -> String: + String.join(Imports.trail(Digest.edges(all), Imports.paths(Digest.edges(all)), List.length(&2, Digest.Digest, all), + from, to), " -> ") + # the path of the first law file among ls (a LAWS.bend or a PROOF.bend) # whose closure over all holds the path pp def unsafe.origin(ls: List<&2, Digest.Digest>, +all: List<&2, Digest.Digest>, +pp: String) -> Maybe<&2, String>: @@ -2679,35 +2702,55 @@ def unsafe.origin(ls: List<&2, Digest.Digest>, +all: List<&2, Digest.Digest>, +p +more = unsafe.origin(rest, all, pp) Bool.pick(Maybe<&2, String>, Bool.and(is_law_file, Imports.has(unsafe.closure(all, norm), pp)), Some{path}, more) -# one finding for each `@unsafe def`, at its `@`, naming the law file -def unsafe.each(us: List<&2, Digest.Unsafe>, +origin: String, +path: String) -> List<&2, F.Finding>: +# what the finding says of a foreign or an `@unsafe` def, reached from the +# law file at origin along the import path via +def unsafe.says(foreign: Bool, +name: String, +origin: String, +via: String) -> String: + match foreign: + case True{}: + "foreign def " ++ name ++ " is reachable from " ++ origin ++ " (" ++ via + ++ "), so bend fails that proof: SOME PROOFS FAIL, defs rely on unsafe or foreign code; move the effect into a sibling module no law file imports, and pass it in as a service." + case False{}: + "@unsafe def " ++ name ++ " is reachable from " ++ origin ++ " (" ++ via + ++ "), so bend fails that proof: SOME PROOFS FAIL, defs rely on unsafe or foreign code; recurse on a shrinking argument or on fuel and drop @unsafe, or move it into a sibling module no law file imports." + +# one finding for each def, at its `@` (7 wide) or, a foreign def, its +# header's start (3 wide), naming the law file and the import path +def unsafe.each(us: List<&2, Digest.Unsafe>, +origin: String, +via: String, +path: String) -> List<&2, F.Finding>: match us: case Nil{}: Nil{} - case Con{Digest.Unsafe{n, l, c}, rest}: - F.Finding{path, l, c, 7, "unsafe", "@unsafe def " ++ n ++ " is reachable from " ++ origin - ++ ", where the checker skips its termination check and still exits 0; recurse on a shrinking argument or on fuel, and drop @unsafe."} - <> unsafe.each(rest, origin, path) - -# a file's unsafe defs when a law file reaches it, else nothing -def unsafe.at(mm: Maybe<&2, String>, us: List<&2, Digest.Unsafe>, path: String) -> List<&2, F.Finding>: + case Con{Digest.Unsafe{n, l, c, +fo}, rest}: + F.Finding{path, l, c, Bool.pick(U32, fo, 3, 7), "unsafe", unsafe.says(fo, n, origin, via)} + <> unsafe.each(rest, origin, via, path) + +# a file's unsafe and foreign defs when a law file reaches it, else nothing; +# the path runs from that law file to the file at norm +def unsafe.at( + mm: Maybe<&2, String>, + us: List<&2, Digest.Unsafe>, + +path: String, + +norm: String, + +all: List<&2, Digest.Digest> +) -> List<&2, F.Finding>: match mm: case None{}: Nil{} - case Some{origin}: - unsafe.each(us, origin, path) + case Some{+origin}: + unsafe.each(us, origin, unsafe.via(all, Imports.norm(origin), norm), path) # the findings of every file of fs, in order, against the law files of all def unsafe.files(fs: List<&2, Digest.Digest>, +all: List<&2, Digest.Digest>) -> List<&2, F.Finding>: match fs: case Nil{}: Nil{} - case Con{Digest.Digest{path, norm, dir, is_laws, is_law_file, exempt, tops, says, deps, unsafes, laws}, rest}: - List.append(&2, F.Finding, unsafe.at(unsafe.origin(all, all, norm), unsafes, path), unsafe.files(rest, all)) + case Con{Digest.Digest{path, +norm, dir, is_laws, is_law_file, exempt, tops, says, deps, unsafes, laws}, rest}: + List.append(&2, F.Finding, unsafe.at(unsafe.origin(all, all, norm), unsafes, path, norm, all), + unsafe.files(rest, all)) # LAW: over every list of digests, unsafe reports exactly each `@unsafe def` -# of each file that the closure of some law file holds, in file order, and -# names the first such law file +# and each foreign def of each file that the closure of some law file holds, +# in file order, and names the first such law file and the import path from +# it to the file # BOLT-LAW-3 law unsafe_reports: for +ds: List<&2, Digest.Digest> diff --git a/src/rules/PROOF.bend b/src/rules/PROOF.bend index f228807..560d978 100644 --- a/src/rules/PROOF.bend +++ b/src/rules/PROOF.bend @@ -9000,7 +9000,101 @@ def Laws.fuel_slots(ds): Equal.cong(List<&2, FuelRule.Fuel>, List<&2, FuelRule.Fuel>, x => List.append(&2, FuelRule.Fuel, bb, x), FuelRule.fuels(rest), Laws.fuel.slots(rest), Laws.fuel_slots(rest))) -# a lone Nat literal argument is one finding, anything else none +# a `U32.to_nat(..)` group holding one U32 literal alone is one finding when +# the call is that one, anything else none +law fuel.conv: + for kids: Tree.Node + for ok: Bool + for +ll: U32 + for +cc: U32 + for +path: String + {List.length(&2, F.Finding, FuelRule.converted(kids, ok, ll, cc, path)) + == Bool.pick(Nat, Laws.fuel.conv(kids, ok), 1n, 0n) : Nat} + +def fuel.conv(kids, ok, ll, cc, path): + match kids: + case Tree.NCons{h, r}: + match h: + case Tree.Leaf{tok}: + match tok: + case Lex.Tok{k, +t, l, c}: + match k: + case Lex.TName{}: + {==} + case Lex.TUpper{}: + {==} + case Lex.TDotted{}: + {==} + case Lex.TWild{}: + {==} + case Lex.TKey{}: + {==} + case Lex.TNum{}: + match r: + case Tree.Leaf{x}: + {==} + case Tree.Group{x, y, z}: + {==} + case Tree.Stmt{x, y, z}: + {==} + case Tree.NNil{}: + chars.one(Bool.and(ok, T.digits_ok(String.to_list(t))), F.Finding{path, ll, cc, + U32.from_nat(Nat.add(String.length(t), 12n)), "fuel", + "The fuel is fixed at U32.to_nat(" ++ t + ++ "), so longer input is silently cut short; derive the fuel from the input size."}) + case Tree.NCons{x, y}: + {==} + case Lex.TStr{}: + {==} + case Lex.TChar{}: + {==} + case Lex.TComment{}: + {==} + case Lex.TSpace{}: + {==} + case Lex.TNewline{}: + {==} + case Lex.TOp{}: + {==} + case Lex.TColon{}: + {==} + case Lex.TEq{}: + {==} + case Lex.TBind{}: + {==} + case Lex.TArrow{}: + {==} + case Lex.TLam{}: + {==} + case Lex.TAll{}: + {==} + case Lex.TAmp{}: + {==} + case Lex.TOpen{}: + {==} + case Lex.TClose{}: + {==} + case Lex.TComma{}: + {==} + case Tree.Group{x, y, z}: + {==} + case Tree.Stmt{x, y, z}: + {==} + case Tree.NNil{}: + {==} + case Tree.NCons{x, y}: + {==} + case Tree.Leaf{x}: + {==} + case Tree.Group{x, y, z}: + {==} + case Tree.Stmt{x, y, z}: + {==} + case Tree.NNil{}: + {==} + +# a lone Nat literal argument, or U32.to_nat of a lone U32 literal, is one +# finding, anything else none law fuel.lit: for aa: Tree.Node for +path: String @@ -9019,7 +9113,39 @@ def fuel.lit(aa, path): case Lex.TUpper{}: {==} case Lex.TDotted{}: - {==} + match r: + case Tree.Leaf{x}: + {==} + case Tree.Group{x, y, z}: + {==} + case Tree.Stmt{x, y, z}: + {==} + case Tree.NNil{}: + {==} + case Tree.NCons{g, y}: + match g: + case Tree.Leaf{x}: + {==} + case Tree.Group{o, kids, cl}: + match o: + case Lex.Tok{ok, +ot, ol, oc}: + match y: + case Tree.Leaf{x}: + {==} + case Tree.Group{x, w, z}: + {==} + case Tree.Stmt{x, w, z}: + {==} + case Tree.NNil{}: + fuel.conv(kids, Bool.and(String.eq(t, "U32.to_nat"), String.eq(ot, "(")), l, c, path) + case Tree.NCons{x, w}: + {==} + case Tree.Stmt{x, w, z}: + {==} + case Tree.NNil{}: + {==} + case Tree.NCons{x, w}: + {==} case Lex.TWild{}: {==} case Lex.TKey{}: @@ -11042,39 +11168,59 @@ def unsafe.reacher(ls, all, pp): law unsafe.report: for us: List<&2, Digest.Unsafe> for +origin: String + for +via: String for +path: String - {Unsafe.report(us, origin, path) == Laws.unsafe.each(us, origin, path) : List<&2, F.Finding>} + {Unsafe.report(us, origin, via, path) == Laws.unsafe.each(us, origin, via, path) : List<&2, F.Finding>} -def unsafe.report(us, origin, path): +def unsafe.report(us, origin, via, path): match us: case Nil{}: {==} - case Con{Digest.Unsafe{+n, +l, +c}, rest}: - Equal.cong(List<&2, F.Finding>, List<&2, F.Finding>, - t => F.Finding{path, l, c, 7, "unsafe", "@unsafe def " ++ n ++ " is reachable from " ++ origin - ++ ", where the checker skips its termination check and still exits 0; recurse on a shrinking argument or on fuel, and drop @unsafe."} <> t, - Unsafe.report(rest, origin, path), Laws.unsafe.each(rest, origin, path), unsafe.report(rest, origin, path)) + case Con{Digest.Unsafe{+n, +l, +c, fo}, rest}: + match fo: + case True{}: + Equal.cong(List<&2, F.Finding>, List<&2, F.Finding>, + t => F.Finding{path, l, c, 3, "unsafe", Unsafe.say(True{}, n, origin, via)} <> t, + Unsafe.report(rest, origin, via, path), Laws.unsafe.each(rest, origin, via, path), + unsafe.report(rest, origin, via, path)) + case False{}: + Equal.cong(List<&2, F.Finding>, List<&2, F.Finding>, + t => F.Finding{path, l, c, 7, "unsafe", Unsafe.say(False{}, n, origin, via)} <> t, + Unsafe.report(rest, origin, via, path), Laws.unsafe.each(rest, origin, via, path), + unsafe.report(rest, origin, via, path)) # the rule's found is unsafe.at law unsafe.found: for mm: Maybe<&2, String> for us: List<&2, Digest.Unsafe> for +path: String - {Unsafe.found(mm, us, path) == Laws.unsafe.at(mm, us, path) : List<&2, F.Finding>} + for +norm: String + for +all: List<&2, Digest.Digest> + {Unsafe.found(mm, us, path, norm, Digest.edges(all), Imports.paths(Digest.edges(all)), + List.length(&2, Digest.Digest, all)) == Laws.unsafe.at(mm, us, path, norm, all) : List<&2, F.Finding>} -def unsafe.found(mm, us, path): +def unsafe.found(mm, us, path, norm, all): match mm: case None{}: {==} - case Some{origin}: - unsafe.report(us, origin, path) + case Some{+origin}: + match us: + case Nil{}: + {==} + case Con{u, rest}: + unsafe.report(u <> rest, origin, Laws.unsafe.via(all, Imports.norm(origin), norm), path) + +# the rule's walk over fs, against the law files of all, as its check runs it +def unsafe.run(fs: List<&2, Digest.Digest>, +all: List<&2, Digest.Digest>) -> List<&2, F.Finding>: + Unsafe.check.go(fs, Unsafe.reaches(all, Digest.edges(all), Imports.paths(Digest.edges(all)), + List.length(&2, Digest.Digest, all)), Digest.edges(all), Imports.paths(Digest.edges(all)), + List.length(&2, Digest.Digest, all)) # the rule's walk over the files is unsafe.files law unsafe.go: for fs: List<&2, Digest.Digest> for +all: List<&2, Digest.Digest> - {Unsafe.check.go(fs, Unsafe.reaches(all, Digest.edges(all), Imports.paths(Digest.edges(all)), - List.length(&2, Digest.Digest, all))) == Laws.unsafe.files(fs, all) : List<&2, F.Finding>} + {unsafe.run(fs, all) == Laws.unsafe.files(fs, all) : List<&2, F.Finding>} def unsafe.go(fs, all): match fs: @@ -11082,23 +11228,19 @@ def unsafe.go(fs, all): {==} case Con{Digest.Digest{+path, +norm, dir, is_laws, is_law_file, exempt, tops, says, deps, +unsafes, laws}, rest}: %unsafe.go(rest, all) : - {Unsafe.check.go(Digest.Digest{path, norm, dir, is_laws, is_law_file, exempt, tops, says, deps, unsafes, laws} - <> rest, Unsafe.reaches(all, Digest.edges(all), Imports.paths(Digest.edges(all)), - List.length(&2, Digest.Digest, all))) - == List.append(&2, F.Finding, Laws.unsafe.at(Laws.unsafe.origin(all, all, norm), unsafes, path), _) + {unsafe.run(Digest.Digest{path, norm, dir, is_laws, is_law_file, exempt, tops, says, deps, unsafes, laws} + <> rest, all) + == List.append(&2, F.Finding, Laws.unsafe.at(Laws.unsafe.origin(all, all, norm), unsafes, path, norm, all), _) : List<&2, F.Finding>} - %unsafe.found(Laws.unsafe.origin(all, all, norm), unsafes, path) : - {Unsafe.check.go(Digest.Digest{path, norm, dir, is_laws, is_law_file, exempt, tops, says, deps, unsafes, laws} - <> rest, Unsafe.reaches(all, Digest.edges(all), Imports.paths(Digest.edges(all)), - List.length(&2, Digest.Digest, all))) - == List.append(&2, F.Finding, _, Unsafe.check.go(rest, Unsafe.reaches(all, Digest.edges(all), - Imports.paths(Digest.edges(all)), List.length(&2, Digest.Digest, all)))) : List<&2, F.Finding>} + %unsafe.found(Laws.unsafe.origin(all, all, norm), unsafes, path, norm, all) : + {unsafe.run(Digest.Digest{path, norm, dir, is_laws, is_law_file, exempt, tops, says, deps, unsafes, laws} + <> rest, all) + == List.append(&2, F.Finding, _, unsafe.run(rest, all)) : List<&2, F.Finding>} %unsafe.reacher(all, all, norm) : - {Unsafe.check.go(Digest.Digest{path, norm, dir, is_laws, is_law_file, exempt, tops, says, deps, unsafes, laws} - <> rest, Unsafe.reaches(all, Digest.edges(all), Imports.paths(Digest.edges(all)), - List.length(&2, Digest.Digest, all))) - == List.append(&2, F.Finding, Unsafe.found(_, unsafes, path), Unsafe.check.go(rest, Unsafe.reaches(all, - Digest.edges(all), Imports.paths(Digest.edges(all)), List.length(&2, Digest.Digest, all)))) + {unsafe.run(Digest.Digest{path, norm, dir, is_laws, is_law_file, exempt, tops, says, deps, unsafes, laws} + <> rest, all) + == List.append(&2, F.Finding, Unsafe.found(_, unsafes, path, norm, Digest.edges(all), + Imports.paths(Digest.edges(all)), List.length(&2, Digest.Digest, all)), unsafe.run(rest, all)) : List<&2, F.Finding>} {==} @@ -24198,6 +24340,61 @@ def inert.fuel.fuels(ds): FuelRule.fuels(inert.defs(rest))) : List<&2, FuelRule.Fuel>} {==} +# a `U32.to_nat(..)` group read that way fixes the fuel it fixed +law inert.fuel.conv: + for kids: Tree.Node + for ok: Bool + for +ll: U32 + for +cc: U32 + for +path: String + {FuelRule.converted(Laws.inert.node(kids), ok, ll, cc, path) == FuelRule.converted(kids, ok, ll, cc, path) + : List<&2, F.Finding>} + +def inert.fuel.conv(kids, _ok, _ll, _cc, _path): + match kids: + case Tree.NCons{h, +r}: + match h: + case Tree.Leaf{tok}: + match tok: + case Lex.Tok{k, t, l, c}: + match k: + case Lex.TName{}: {==} + case Lex.TUpper{}: {==} + case Lex.TDotted{}: {==} + case Lex.TWild{}: {==} + case Lex.TKey{}: {==} + case Lex.TNum{}: + match r: + case Tree.NNil{}: {==} + case Tree.Leaf{x}: {==} + case Tree.Group{x, y, z}: {==} + case Tree.Stmt{x, y, z}: {==} + case Tree.NCons{x, y}: {==} + case Lex.TStr{}: {==} + case Lex.TChar{}: {==} + case Lex.TComment{}: {==} + case Lex.TSpace{}: {==} + case Lex.TNewline{}: {==} + case Lex.TOp{}: {==} + case Lex.TColon{}: {==} + case Lex.TEq{}: {==} + case Lex.TBind{}: {==} + case Lex.TArrow{}: {==} + case Lex.TLam{}: {==} + case Lex.TAll{}: {==} + case Lex.TAmp{}: {==} + case Lex.TOpen{}: {==} + case Lex.TClose{}: {==} + case Lex.TComma{}: {==} + case Tree.Group{o, gk, cl}: {==} + case Tree.Stmt{sk, sks, sb}: {==} + case Tree.NNil{}: {==} + case Tree.NCons{x, y}: {==} + case Tree.Leaf{tok}: {==} + case Tree.Group{o, gk, cl}: {==} + case Tree.Stmt{sk, sks, sb}: {==} + case Tree.NNil{}: {==} + # an argument read that way is the Nat literal it was: a number is never cut law inert.fuel.literal: for aa: Tree.Node @@ -24214,7 +24411,29 @@ def inert.fuel.literal(aa, _path): match k: case Lex.TName{}: {==} case Lex.TUpper{}: {==} - case Lex.TDotted{}: {==} + case Lex.TDotted{}: + match r: + case Tree.NCons{g, y}: + match g: + case Tree.Group{o, gk, cl}: + match o: + case Lex.Tok{ok, ot, ol, oc}: + match y: + case Tree.NNil{}: + inert.fuel.conv(gk, Bool.and(String.eq(t, "U32.to_nat"), String.eq(ot, "(")), l, c, + _path) + case Tree.Leaf{x}: {==} + case Tree.Group{x, w, z}: {==} + case Tree.Stmt{x, w, z}: {==} + case Tree.NCons{x, w}: {==} + case Tree.Leaf{x}: {==} + case Tree.Stmt{x, w, z}: {==} + case Tree.NNil{}: {==} + case Tree.NCons{x, w}: {==} + case Tree.NNil{}: {==} + case Tree.Leaf{x}: {==} + case Tree.Group{x, w, z}: {==} + case Tree.Stmt{x, w, z}: {==} case Lex.TWild{}: {==} case Lex.TKey{}: {==} case Lex.TNum{}: diff --git a/src/rules/correctness/hole.bend b/src/rules/correctness/hole.bend index 90510d2..17f72be 100644 --- a/src/rules/correctness/hole.bend +++ b/src/rules/correctness/hole.bend @@ -1,5 +1,6 @@ -# rule hole: a TODO hole left in code, the one bend counts in "N TODO found": -# a `?` and then the name `TODO`, with any spaces, newlines or comments +# rule hole: a TODO hole left in code, the one bend counts when it prints +# `SOME PROOFS FAIL` then "Error: 1 TODO found." or "Error: N TODOs found." +# and exits 1 (bend 2.0.34): a `?` and then the name `TODO`, with any spaces, newlines or comments # between them (`?TODO`, `? TODO`). `?todo`, `?TODO_later` and `?TODO.x` are # other names, which bend reports as a type error, not as a TODO, and they are # not reported here. The finding spans `?` through `TODO` when both sit on one diff --git a/src/rules/digest.bend b/src/rules/digest.bend index 9e9a2b2..2c6601f 100644 --- a/src/rules/digest.bend +++ b/src/rules/digest.bend @@ -5,7 +5,7 @@ # the file count (100 files cost 362 s that way). So each file is read down # once to what those rules ask of it -- its path, its top-level defs and types # by name and line, what its laws name, what it imports, and its `@unsafe` -# defs -- and the phases run over these, which are strings and cheap to copy. +# and foreign defs -- and the phases run over these, which are strings and cheap to copy. import Base import ../src.bend as Src import ../syntax/lex.bend as Lex @@ -16,6 +16,7 @@ import ../lazy/lazy.bend as Lazy import ./imports.bend as Imports import ./laws/closed.bend as Closed import ../paths.bend as Paths +import ./correctness/foreign.bend as Foreign # what a file holds # ----------------- @@ -31,9 +32,11 @@ type Mention is Data: type Top is Data: Top{kind: Outline.ItemKind, name: String, line: U32, ctors: List<&2, String>, calls: List<&2, Mention>} -# an `@unsafe def` and where its `@` is +# a def a proof may not reach (bend 2.0.32): an `@unsafe def`, where its +# `@` is, or a foreign def (its body only `import "./x.c"` / `import +# "./x.js"` lines), where its header starts; foreign says which type Unsafe is Data: - Unsafe{name: String, line: U32, col: U32} + Unsafe{name: String, line: U32, col: U32, foreign: Bool} # a law of a LAWS.bend: its name, the line it starts on, whether it binds # (a `for` or `exs` line), and the lines of its comment block, `# ` dropped @@ -43,7 +46,7 @@ type Law is Data: # one file as the project rules see it: its path as given and normalized, its # directory, whether it states laws (LAWS.bend) or proves them too # (PROOF.bend), whether the coverage rule lets it off, its top-level items, what -# its own laws name, the files it imports, and its `@unsafe` defs +# its own laws name, the files it imports, its `@unsafe` and foreign defs type Digest is Data: Digest{path: String, norm: String, dir: String, is_laws: Bool, is_law_file: Bool, exempt: Bool, tops: List<&2, Top>, says: List<&2, Mention>, deps: List<&2, String>, unsafes: List<&2, Unsafe>, @@ -254,7 +257,7 @@ def push(mm: Maybe<&2, String>, +ll: U32, +cc: U32, more: List<&2, Unsafe>) -> L case None{}: more case Some{n}: - Unsafe{n, ll, cc} <> more + Unsafe{n, ll, cc, False{}} <> more # every `@ unsafe def name` run of tokens, on one line or two def unsafe_defs(toks: List<&2, Lex.Tok>) -> List<&2, Unsafe>: @@ -265,6 +268,31 @@ def unsafe_defs(toks: List<&2, Lex.Tok>) -> List<&2, Unsafe>: +more = unsafe_defs(rest) Bool.pick(List<&2, Unsafe>, String.eq(at, "@"), push(unsafe_name(rest), l, c, more), more) +# a foreign def, when its body is one (Foreign.lanes), onto the others +def foreign.push( + mm: Maybe<&2, Foreign.Lanes>, + +name: String, + +ll: U32, + +cc: U32, + more: List<&2, Unsafe> +) -> List<&2, Unsafe>: + match mm: + case None{}: + more + case Some{_lanes}: + Unsafe{name, ll, cc, True{}} <> more + +# every top-level foreign def, where its header starts +def foreign_defs(root: Tree.Node) -> List<&2, Unsafe>: + match root: + case Tree.NCons{Tree.Stmt{Tree.SDef{}, +kids, body}, rest}: + foreign.push(Foreign.lanes(body), Foreign.name.of(Bind.declared(kids)), Tree.line(kids), Tree.col(kids), + foreign_defs(rest)) + case Tree.NCons{h, rest}: + foreign_defs(rest) + case other: + Nil{} + # the laws # -------- @@ -315,7 +343,8 @@ def of(s2: Src.Src) -> Digest: +as = aliases(items, p) Digest{path, p, Imports.dir_of(path), Paths.is_laws(path), Paths.is_law_file(path), is_exempt(p), ranged(items, uses.of(bound), as, p), stated(Paths.is_laws(path), tree, bound, as, p), Imports.targets(items, p), - unsafe_defs(significant(toks)), laws.in(Paths.is_laws(path), tree, items)} + List.append(&2, Unsafe, unsafe_defs(significant(toks)), foreign_defs(tree)), + laws.in(Paths.is_laws(path), tree, items)} # every file the linter read, in one pass, in order def all(ss: List<&2, Src.Src>) -> List<&2, Digest>: diff --git a/src/rules/imports.bend b/src/rules/imports.bend index 507e37d..cca9ec1 100644 --- a/src/rules/imports.bend +++ b/src/rules/imports.bend @@ -172,3 +172,43 @@ def walk( # the closure of the file at from, a path normalized already, over the graph def closure.go(es: List<&2, Edge>, +read: List<&2, String>, +fuel: Nat, +from: String) -> List<&2, String>: List.reverse(&2, String, walk(fuel, [from], [from], es, read)) + +# a file the trail's walk has queued, and the files it was reached through, +# itself first and the start last +type Step is Data: + Step{at: String, back: List<&2, String>} + +# each file queued, reached through back +def steps(ds: List<&2, String>, +back: List<&2, String>) -> List<&2, Step>: + match ds: + case Nil{}: + Nil{} + case Con{+d, rest}: + Step{d, d <> back} <> steps(rest, back) + +# the walk `walk` takes, breadth first, each queued file carrying how it was +# reached, until it takes the file at to: the files from the start to it, in +# order; none when the walk never takes it +def trail.go( + fuel: Nat, + todo: List<&2, Step>, + +seen: List<&2, String>, + +es: List<&2, Edge>, + +read: List<&2, String>, + +to: String +) -> List<&2, String>: + match fuel todo: + case 0n t: + Nil{} + case 1n+f Nil{}: + Nil{} + case 1n+f Con{Step{+at, +back}, rest}: + +found = fresh.fast(deps.first(es, at), seen, read) + Lazy.stop(List<&2, String>, String.eq(at, to), List.reverse(&2, String, back), + _u => trail.go(f, List.append(&2, Step, rest, steps(found, back)), + List.append(&2, String, List.reverse(&2, String, found), seen), es, read, to)) + +# a shortest chain of relative imports from the file at from to the file at +# to, both normalized: the files in order, from first and to last +def trail(es: List<&2, Edge>, +read: List<&2, String>, +fuel: Nat, +from: String, +to: String) -> List<&2, String>: + trail.go(fuel, [Step{from, [from]}], [from], es, read, to) diff --git a/src/rules/laws/unsafe.bend b/src/rules/laws/unsafe.bend index b1430ee..8b588fa 100644 --- a/src/rules/laws/unsafe.bend +++ b/src/rules/laws/unsafe.bend @@ -1,12 +1,22 @@ -# rule unsafe (project-wide): an `@unsafe def` that a LAWS.bend or PROOF.bend -# reaches by relative imports, over the files bolt read. The checker skips its -# termination check, prints "All terms check, but N defs rely on unsafe or -# foreign code:" (2.0.16: "with N unsafe annotation(s).") and exits 0, so a -# gate that only reads the exit status goes green on a proof that is not -# sound (a def that never returns proves anything). Recurse -# on a shrinking argument, or on a fuel, and drop the `@unsafe`; or keep the -# def out of what the laws import. An `@unsafe` def no law file reaches is -# not this rule's business. The rule reads each file's digest +# rule unsafe (project-wide): an `@unsafe def` or a foreign def (its body +# only `import "./x.c"` / `import "./x.js"` lines, what rule foreign reads) +# that a LAWS.bend or PROOF.bend reaches by relative imports, over the files +# bolt read. Since bend 2.0.32 a proof passes only when no def it loads, +# imports included, is `@unsafe` or foreign or names one that is: every def +# of every imported module counts, named by a law or not. Otherwise `bend` +# prints `SOME PROOFS FAIL`, then `Error: N defs rely on unsafe or foreign +# code:` and a `- name` list, and exits 1 (2.0.34; before 2.0.32 it printed +# "All terms check, but ..." and exited 0). So the gate is red, and the +# message names the defs that lean on the effect, not the import that +# brought it in: this rule names that path, law file first. `@unsafe` skips +# the termination check (a def that never returns proves anything): recurse +# on a shrinking argument or on fuel, and drop it. A foreign effect is fine +# in the program, never under a law: move it into a sibling module no law +# file imports, and hand the laws' code the effect as a service record +# (AGENTS.md; snap, ezhttp, bolt and ez were restructured that way). A def no +# law file reaches is not this rule's business. Hash imports (`import +# 0x.../path`, resolved through BEND_LIB) are not followed: bolt reads only +# the files of the run. The rule reads each file's digest # (src/rules/digest.bend), and takes every closure over one import graph. import Base import ../../finding.bend as F @@ -40,31 +50,81 @@ def reacher(rs: List<&2, Reach>, +pp: String) -> Maybe<&2, String>: +more = reacher(rest, pp) Bool.pick(Maybe<&2, String>, Imports.has(ps, pp), Some{origin}, more) -# each unsafe def as a finding, reached from the law file -def report(us: List<&2, Digest.Unsafe>, +origin: String, +path: String) -> List<&2, F.Finding>: +# what a def reached from a law file along the import path via is, and what +# to do about it +def say(foreign: Bool, +name: String, +origin: String, +via: String) -> String: + match foreign: + case True{}: + "foreign def " ++ name ++ " is reachable from " ++ origin ++ " (" ++ via + ++ "), so bend fails that proof: SOME PROOFS FAIL, defs rely on unsafe or foreign code; move the effect into a sibling module no law file imports, and pass it in as a service." + case False{}: + "@unsafe def " ++ name ++ " is reachable from " ++ origin ++ " (" ++ via + ++ "), so bend fails that proof: SOME PROOFS FAIL, defs rely on unsafe or foreign code; recurse on a shrinking argument or on fuel and drop @unsafe, or move it into a sibling module no law file imports." + +# each unsafe or foreign def as a finding, at its `@unsafe` or its `def`, +# reached from the law file along the import path via +def report(us: List<&2, Digest.Unsafe>, +origin: String, +via: String, +path: String) -> List<&2, F.Finding>: + match us: + case Nil{}: + Nil{} + case Con{Digest.Unsafe{n, l, c, +fo}, rest}: + F.Finding{path, l, c, Bool.pick(U32, fo, 3, 7), "unsafe", say(fo, n, origin, via)} <> report(rest, origin, via, path) + +# the import path from the file at from to the file at to, both normalized, +# as `a -> b -> c` +def via(es: List<&2, Imports.Edge>, +read: List<&2, String>, +fuel: Nat, +from: String, +to: String) -> String: + String.join(Imports.trail(es, read, fuel, from, to), " -> ") + +# the unsafe and foreign defs of the file at norm, reached from the law file +# at origin: the import path is looked for only when there is one +def found.some( + us: List<&2, Digest.Unsafe>, + +origin: String, + +path: String, + +norm: String, + +es: List<&2, Imports.Edge>, + +read: List<&2, String>, + +fuel: Nat +) -> List<&2, F.Finding>: match us: case Nil{}: Nil{} - case Con{Digest.Unsafe{n, l, c}, rest}: - F.Finding{path, l, c, 7, "unsafe", "@unsafe def " ++ n ++ " is reachable from " ++ origin - ++ ", where the checker skips its termination check and still exits 0; recurse on a shrinking argument or on fuel, and drop @unsafe."} <> report(rest, origin, path) + case Con{u, rest}: + report(u <> rest, origin, via(es, read, fuel, Imports.norm(origin), norm), path) -# the unsafe defs of a file, when a law file reaches it -def found(mm: Maybe<&2, String>, us: List<&2, Digest.Unsafe>, path: String) -> List<&2, F.Finding>: +# the unsafe and foreign defs of a file, when a law file reaches it +def found( + mm: Maybe<&2, String>, + us: List<&2, Digest.Unsafe>, + +path: String, + +norm: String, + +es: List<&2, Imports.Edge>, + +read: List<&2, String>, + +fuel: Nat +) -> List<&2, F.Finding>: match mm: case None{}: Nil{} case Some{origin}: - report(us, origin, path) + found.some(us, origin, path, norm, es, read, fuel) -def check.go(ds: List<&2, Digest.Digest>, +rs: List<&2, Reach>) -> List<&2, F.Finding>: +def check.go( + ds: List<&2, Digest.Digest>, + +rs: List<&2, Reach>, + +es: List<&2, Imports.Edge>, + +read: List<&2, String>, + +fuel: Nat +) -> List<&2, F.Finding>: match ds: case Nil{}: Nil{} - case Con{Digest.Digest{path, norm, dir, is_laws, is_law_file, exempt, tops, says, deps, unsafes, laws}, rest}: - List.append(&2, F.Finding, found(reacher(rs, norm), unsafes, path), check.go(rest, rs)) + case Con{Digest.Digest{path, +norm, dir, is_laws, is_law_file, exempt, tops, says, deps, unsafes, laws}, rest}: + List.append(&2, F.Finding, found(reacher(rs, norm), unsafes, path, norm, es, read, fuel), + check.go(rest, rs, es, read, fuel)) # the rule, over every file the linter read def check(+ds: List<&2, Digest.Digest>) -> List<&2, F.Finding>: +es = Digest.edges(ds) - check.go(ds, reaches(ds, es, Imports.paths(es), List.length(&2, Digest.Digest, ds))) + +read = Imports.paths(es) + +fuel = List.length(&2, Digest.Digest, ds) + check.go(ds, reaches(ds, es, read, fuel), es, read, fuel) diff --git a/src/rules/suspicious/fuel.bend b/src/rules/suspicious/fuel.bend index 995325a..b737574 100644 --- a/src/rules/suspicious/fuel.bend +++ b/src/rules/suspicious/fuel.bend @@ -1,15 +1,21 @@ -# rule fuel: a call to a def of the same file, its name then `(`, passes a Nat -# literal (`1000n`: digits, then `n`) where that def takes its fuel. A fuel -# parameter is known by its name alone (its first lowercase name before the -# colon): `fuel`, `gas`, `steps` or `budget`, or any name starting with -# `fuel`. The fuel-0 arm returns what it has, so input past the literal comes -# out cut short, with no error (a JSON printer that stopped at 1000 tasks). -# Inside a law, the checker unrolls the fixed fuel and hangs. Derive the fuel -# from the input's size (`Nat.mul(size, 4n)`) or take it as a parameter. A -# literal of any size counts, an exact repeat count such as `3n` included. -# Only an argument that is one literal token alone counts: `U32.to_nat(1000)`, -# a let-bound literal and a parenthesized `(7n)` are not seen. A def's own -# calls are exempt: its step passes `fuel - 1`, not a literal. +# rule fuel: a call to a def of the same file, its name then `(`, passes a +# fixed number where that def takes its fuel: a Nat literal (`1000n`: digits, +# then `n`), or `U32.to_nat` of a U32 literal (`U32.to_nat(100000)`: digits +# alone), the form a big fuel is written in. A fuel parameter is known by its +# name alone (its first lowercase name before the colon): `fuel`, `gas`, +# `steps` or `budget`, or any name starting with `fuel`. The fuel-0 arm +# returns what it has, so input past the number comes out cut short, with no +# error (a JSON printer that stopped at 1000 tasks). A law is no safer: a law +# proved over every fuel and then used at a big fixed one, against a goal +# written another way, overflows the checker ("the machine stack overflowed", +# bend 2.0.33 and 2.0.34; ez's lock walk at `U32.to_nat(100000)` did). Before +# 2.0.29 the checker unrolled the fixed fuel and hung; 2.0.29 made a checked +# recursion on a Nat literal linear. Derive the fuel from the input's size +# (`Nat.mul(size, 4n)`) or take it as a parameter. A number of any size +# counts, an exact repeat count such as `3n` included. Only an argument that +# is the literal alone, or `U32.to_nat(` the U32 literal alone `)`, counts: a +# let-bound literal and a parenthesized `(7n)` are not seen. A def's own calls +# are exempt: its step passes `fuel - 1`, not a literal. import Base import ../../src.bend as Src import ../../lazy/lazy.bend as Lazy @@ -46,7 +52,21 @@ def fuels(ds: List<&2, Calls.Def>) -> List<&2, Fuel>: case Con{Calls.Def{name, sig, body}, rest}: List.append(&2, Fuel, fuels.params(Calls.params(sig), name, 0n), fuels(rest)) -# an argument that is a Nat literal alone (digits, then `n`), as a finding +# the group of a call at line ll, column cc, as a finding when it holds one +# U32 literal alone (digits) and ok says the call is `U32.to_nat(` +def converted(kids: Tree.Node, ok: Bool, +ll: U32, +cc: U32, +path: String) -> List<&2, F.Finding>: + match kids: + case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TNum{}, +t, l, c}}, Tree.NNil{}}: + Bool.pick(List<&2, F.Finding>, Bool.and(ok, T.digits_ok(String.to_list(t))), + [F.Finding{path, ll, cc, U32.from_nat(Nat.add(String.length(t), 12n)), "fuel", + "The fuel is fixed at U32.to_nat(" ++ t + ++ "), so longer input is silently cut short; derive the fuel from the input size."}], + []) + case other: + Nil{} + +# an argument that is a Nat literal alone (digits, then `n`), or +# `U32.to_nat` of a U32 literal alone, as a finding def literal(aa: Tree.Node, +path: String) -> List<&2, F.Finding>: match aa: case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TNum{}, +t, l, c}}, Tree.NNil{}}: @@ -54,6 +74,9 @@ def literal(aa: Tree.Node, +path: String) -> List<&2, F.Finding>: [F.Finding{path, l, c, U32.from_nat(String.length(t)), "fuel", "The fuel is fixed at " ++ t ++ ", so longer input is silently cut short; derive the fuel from the input size."}], []) + case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TDotted{}, +t, l, c}}, + Tree.NCons{Tree.Group{Lex.Tok{ok, +o, ol, oc}, kids, cl}, Tree.NNil{}}}: + converted(kids, Bool.and(String.eq(t, "U32.to_nat"), String.eq(o, "(")), l, c, path) case other: Nil{} diff --git a/src/rules/tokens.bend b/src/rules/tokens.bend index 7cbaafd..7277778 100644 --- a/src/rules/tokens.bend +++ b/src/rules/tokens.bend @@ -64,6 +64,16 @@ def nat_ok(cs: List<&2, Char>) -> Bool: case Nil{}: False{} +# digits alone, one or more: a U32 literal's chars +def digits_ok(cs: List<&2, Char>) -> Bool: + match cs: + case Con{+c, Nil{}}: + Char.is_digit(c) + case Con{+c, t}: + Lazy.and_then(Char.is_digit(c), _u => digits_ok(t)) + case Nil{}: + False{} + # the text without its last char (a Nat literal's digits) def stem(+tt: String) -> String: String.take(tt, Nat.sub(String.length(tt), 1n))