diff --git a/SPEC.md b/SPEC.md index eb1f8f3..289c612 100644 --- a/SPEC.md +++ b/SPEC.md @@ -8,7 +8,7 @@ A spec is **well-formed** when `check` reports nothing for it (SHAKE-SPEC-1). Th The words `parse` receives are what the program passes it. In a compiled program they come from `argv`, after the runtime has taken its own flags and the first `--` (SHAKE-TRUST-2). -The reasoning behind each requirement, the verdict of each against the code at `b93357a`, and the decisions that shaped them are in [docs/rfc/shake-spec.md](docs/rfc/shake-spec.md). Every law as it stood then, and the progress of the rollout, is in [docs/rfc/shake-law-inventory.md](docs/rfc/shake-law-inventory.md). +The reasoning behind each requirement, the verdict of each against the code at `b93357a`, and the decisions that shaped them are in [docs/rfc/shake-spec.md](docs/rfc/shake-spec.md). The RFC also records the audit behind them and the rollout that proved every row. ## Format diff --git a/bolt.bend b/bolt.bend index 0a24721..f8db8b6 100644 --- a/bolt.bend +++ b/bolt.bend @@ -1,5 +1,5 @@ -# bolt.bend: how bolt lints this repo. Every rule is an error except -# `coverage`, which warns until the laws exist: the gate must see no errors. +# bolt.bend: how bolt lints this repo. Every rule is an error: the gate must +# see no errors. # See bolt/config.bend for the groups and levels. import Base @@ -15,11 +15,11 @@ def suspicious() -> String: def style() -> String: "error" -# a pure def named by no quantified law: advice while the laws of -# docs/rfc/shake-spec.md are pending. That rule is `coverage` (L001). IO, -# which no law can reach, says so with `# noqa: L001` on its def line. +# a pure def named by no quantified law. That rule is `coverage` (L001). A +# def no law applies to (IO, a builder, a type alias, proof machinery, the +# example program) says so with `# noqa: L001 ` on its def line. def laws() -> String: - "warn" + "error" # a law with no binder def closed() -> String: diff --git a/docs/rfc/shake-law-inventory.md b/docs/rfc/shake-law-inventory.md deleted file mode 100644 index c57d5d9..0000000 --- a/docs/rfc/shake-law-inventory.md +++ /dev/null @@ -1,262 +0,0 @@ -# shake law inventory - -Read at `b93357a` on `main` ("chore: bump Bend to 2.0.26 (#13)"), with bend 2.0.26 (the release `flake.lock` pins through `bendlang/bend` at `6a77e12`), bolt v0.4.0 (`flake.lock` pins `Emerging-Patterns/bolt` at `24b497e`) and ez at `13e86ea`. - -This is the companion to [shake-spec.md](shake-spec.md). Since it was read, the code has moved: `shake/main.bend` is `src/cli.bend` (its one-letter parameters doubled and its headers rewrapped for bolt's style rules, with no other change), `shake/args.bend`, `LAWS.bend`, `PROOF.bend` and `sample.bend` are under `src/`, and `main.bend` at the root is the interface. Paths and line numbers below are as read. It records what `shake/LAWS.bend` states today, maps each law to the requirement it points toward, and records what we found by reading the code and running a binary built from this tree. It follows the shape of bolt's [bolt-law-inventory.md](https://github.com/Emerging-Patterns/bolt/blob/v1.6.2/docs/rfc/bolt-law-inventory.md) and takes the positions ez's and bolt's specifications reached: exactly two assurance levels, Proved and Trusted; pending is a status, not a level; a closed law has no standing; a test or fixture is never evidence for a requirement. - -## How we ran things - -The proof gate is `bend shake/PROOF.bend` from the repository root, the same check `ez test --unit-only` makes in CI through ez's `mkProofs` (ez's runner compares the first line with `All terms check.`, so a proof that leans on unsafe code fails it). The linter is the pinned bolt, built with `bend bolt/main.bend -o bin/bolt.bin` at `24b497e` and run with no arguments at the root. We also built bolt v1.6.2, the current release, to see what the rollout's first lint bump will report; its hub dependencies were filled into a local `BEND_LIB` from the git revisions in bolt's `ez.toml`, because this environment cannot reach `hub.bend-lang.com`. The demo binary was built from a fresh copy of the tracked files (`git archive HEAD`), following the README. - -## How to read the tables - -**Kind** is `Q` for a quantified law whose binders the statement uses, and `C` for a closed law. shake writes no law without a binder: each of its 53 closed laws has exactly one binder, `for u: Unit`, that the statement never mentions. We count those as `C`, because they state one fixed input, and the table marks them `C (u)` so the disguise is visible. - -**Proof** is `{==}` when the whole proof in PROOF.bend is `{==}`: the two sides reduce to the same term with no case split. Every one of shake's 79 proofs is `{==}`. For a closed law that is what a closed law is. For a quantified law it means the binders are never inspected, so the law restates how a definition unfolds on its first step. - -**Claim** is what the law states, in one line, about the input it is really about. - -**Points toward** names the requirement in the RFC the law illustrates. For a law we propose to delete, it records where the replacing quantified law belongs. `none` has a reason in parentheses: `definitional` restates a definition, `wiring` restates how two defs compose, `helper pin` is one private helper on one input, `wording` pins text nobody depends on, `fixture` is a law about test scaffolding, `dead code` is about a def nothing calls. - -## Proposed requirement IDs - -These are the IDs the RFC proposes. They are listed here so the tables can point at them; their wording and verdicts are in the RFC. - -| ID | Short name | -| :---- | :---- | -| SHAKE-TOK-1 | A word starting `--` is a long option: the spelling up to the first `=`, and the rest after it as a value, verbatim. | -| SHAKE-TOK-2 | A word starting with one `-` (not `-` alone) is a short option: one char of spelling, the rest as a glued value. | -| SHAKE-TOK-3 | `-` alone, and every word not starting with `-`, is a plain word. | -| SHAKE-TOK-4 | After a word exactly `--` reaches `parse`, every later word is a positional value, verbatim. | -| SHAKE-TOK-5 | A flag given a value is refused. | -| SHAKE-TOK-6 | An option with no glued value takes the next word, unless that word is flag-shaped or there is none. | -| SHAKE-TOK-7 | A spelling no argument of the current command has is refused as unknown. | -| SHAKE-PARSE-1 | Value fidelity, the headline guarantee: every bound value is a word of argv, verbatim, or a default. | -| SHAKE-PARSE-2 | Plain words bind the current command's positionals in spec order. | -| SHAKE-PARSE-3 | A rest positional binds every remaining plain word, in order. | -| SHAKE-PARSE-4 | A plain word naming a subcommand selects it. | -| SHAKE-PARSE-5 | A value outside an argument's nonempty choices is refused. | -| SHAKE-PARSE-6 | Defaults fill exactly the unbound arguments that have one. | -| SHAKE-PARSE-7 | A successful parse binds every required argument on the selected path. | -| SHAKE-PARSE-8 | `help` in command position asks for help on the words after it. | -| SHAKE-PARSE-9 | The first error wins. | -| SHAKE-PARSE-10 | A repeated option (decided behavior change). | -| SHAKE-SPEC-1 | `check` reports exactly the ways a Cli is ill-formed (new). | -| SHAKE-GET-1 | `get`, `get_all`, `on` and `path_of` read the Matched as stated. | -| SHAKE-HELP-1 | `help` shows the page of the command its path names. | -| SHAKE-HELP-2 | A page lists every subcommand and every option once, in spec order, and the usage line every positional. | -| SHAKE-ERR-1 | `err_text` is empty exactly for NeedHelp. | -| SHAKE-ARGS-1 | `argv` is the runtime's argument list, word for word. | -| SHAKE-TRUST-1 | The Bend checker is sound. | -| SHAKE-TRUST-2 | The compiled runtime's argument handling, as bend 2.0.26 does it. | -| SHAKE-TRUST-3 | The proof-gate runner reads the first line. | - -## The gate and the linter on shake itself - -| Check | Result | Time | -| :---- | :---- | :---- | -| `bend shake/PROOF.bend` | first line `All terms check.`, exit 0 | 1.1 s | -| pinned bolt v0.4.0, whole tree | `clean`, exit 0 | 0.7 s | -| bolt v1.6.2, whole tree, shake's bolt.bend | 140 errors: 82 S004 (`param`, one-letter parameters), 51 S003 (`wrap`, wrapped headers), 7 L001 (`coverage`, every def of `examples/demo/main.bend`); 0 L002 (`closed`) | 0.8 s | -| bolt v1.6.2 `trace` | not run: shake has no SPEC.md | | - -Both green results mean less than they sound, for the same reason. bolt's `closed` rule (L002 in v1.6.2, `closed` in v0.4.0) reports a law with no `for` or `exs` line, and every closed law in shake has one: `for u: Unit`, which nothing uses. So the rule that exists to reject closed laws accepts all 53, in the pinned bolt and in the current one. `coverage` is satisfied the same way: every def in `shake/main.bend` is named by some law, and for most of them that law is one computed case. bolt's own inventory warned that a `for` binder the statement never uses makes a closed law look quantified; shake is the case at scale. - -We checked the gate directly by planting a bug. Changing `parse.put` to bind `String.take(val, 6n)` instead of `val` truncates every bound value to six characters. The gate still printed `All terms check.`, and the demo built from that tree printed `hello Alexan` for `greet --name Alexandra`. Every fixture value in LAWS.bend is six characters or fewer. We restored the file before going on. - -## Summary - -| File | Laws | Quantified | Closed | Quantified proved by `{==}` | Pin wording | -| :---- | :---- | :---- | :---- | :---- | :---- | -| `shake/LAWS.bend` | 79 | 26 | 53 | 26 | 6 | - -"Pin wording" counts closed laws whose expected value is help or error text (`help_root`, `help_greet`, `help_add`, `help_rest`, `help_rest_req`, `err_text_unknown`). A further 21 compare `show`'s one-line rendering of a fixture parse, and `show` exists only for the laws. - -**What shake proves today.** Nothing about parsing. Of the 26 quantified laws, 20 restate a definition's first unfolding, how two defs are wired, or `show`'s format (a builder is its constructor, `parse` is `finish` of `walk`, a lookup in an empty list is `None`), 5 are small lemmas that are true and could serve a requirement (`looks_flag_long`, `allowed_any`, `get_nil`, `on_nil`, `err_text_help`), and 1 is one step of a copy (`copy_one`). No law quantifies over an argv and a spec together, which is where every behavior a caller relies on lives. The 53 closed laws check that about thirty fixed command lines still parse and render as they did. The quantified content about shake's parser that does exist lives in bolt: bolt's `bolt/PROOF.bend` proves `cli.word_step` and `cli.walk_plain`, that a plain word binds the next positional and that plain words fill a rest positional in order, by unfolding shake's private walker. bolt's SPEC.md lists shake as BOLT-TRUST-8, "shake v0.1.1 parses argv as its spec says", and shake has no spec. - -## Inventory - -| Law | Kind | Proof | Claim | Points toward | -| :---- | :---- | :---- | :---- | :---- | -| `app_is_cli` | Q | `{==}` | `app` builds the Cli of its fields | none (definitional) | -| `sub_is_sub` | Q | `{==}` | `sub` builds the Sub of its fields | none (definitional) | -| `flag_is_arg` | Q | `{==}` | `flag` builds a Flag Arg, not required, no default, no choices | none (definitional) | -| `opt_is_arg` | Q | `{==}` | `opt` builds an Opt Arg of its fields | none (definitional) | -| `pos_is_arg` | Q | `{==}` | `pos` builds a Pos Arg with no spellings | none (definitional) | -| `rest_is_arg` | Q | `{==}` | `rest` builds a Rest Arg with no spellings | none (definitional) | -| `looks_flag_is_dash` | Q | `{==}` | `looks_flag` is its body | none (definitional) | -| `looks_flag_long` | Q | `{==}` | every word starting `--` is flag-shaped | SHAKE-TOK-6 (lemma) | -| `looks_flag_alone` | C (u) | `{==}` | `-` is not flag-shaped | SHAKE-TOK-6 | -| `cut_eq_is_go` | Q | `{==}` | `cut_eq` is its body | none (definitional) | -| `cut_eq_plain` | C (u) | `{==}` | `cut_eq("name")` has no value | SHAKE-TOK-1 | -| `cut_eq_value` | C (u) | `{==}` | `cut_eq("name=Ada")` splits at `=` | SHAKE-TOK-1 | -| `short_of_is_take` | Q | `{==}` | `short_of` is its body | none (definitional) | -| `short_of_glued` | C (u) | `{==}` | `short_of("nAda")` is `n` and `Ada` | SHAKE-TOK-2 | -| `short_of_one` | C (u) | `{==}` | `short_of("n")` has no value | SHAKE-TOK-2 | -| `by_long_nil` | Q | `{==}` | no long spelling in an empty list | none (definitional) | -| `by_long_flag` | C (u) | `{==}` | one fixed flag is found by `verbose` | SHAKE-TOK-1 | -| `by_short_nil` | Q | `{==}` | no short spelling in an empty list | none (definitional) | -| `by_short_flag` | C (u) | `{==}` | one fixed flag is found by `v` | SHAKE-TOK-2 | -| `by_name_nil` | Q | `{==}` | no name in an empty list | none (definitional) | -| `by_name_flag` | C (u) | `{==}` | one fixed flag is found by `verbose` | none (helper pin) | -| `find_sub_nil` | Q | `{==}` | no Sub in an empty list | none (definitional) | -| `find_sub_head` | C (u) | `{==}` | one fixed Sub is found by name | SHAKE-PARSE-4 | -| `pos_of_nil` | C (u) | `{==}` | an empty spec has no positionals | none (helper pin) | -| `pos_of_keeps` | C (u) | `{==}` | one fixed spec keeps its positional and drops its flag | SHAKE-PARSE-2 | -| `pos_of_rest` | C (u) | `{==}` | one fixed spec keeps its rest positional | SHAKE-PARSE-3 | -| `rest_last_none` | C (u) | `{==}` | `rest.last` of one positional | none (dead code) | -| `rest_last_ok` | C (u) | `{==}` | `rest.last` with rest at the end | none (dead code) | -| `rest_last_mid` | C (u) | `{==}` | `rest.last` with rest in the middle | none (dead code); SHAKE-SPEC-1 | -| `allowed_any` | Q | `{==}` | empty choices accept every value | SHAKE-PARSE-5 (lemma) | -| `allowed_listed` | C (u) | `{==}` | `red` is among `red, green` | SHAKE-PARSE-5 | -| `allowed_other` | C (u) | `{==}` | `blue` is not among `red, green` | SHAKE-PARSE-5 | -| `bound_nil` | Q | `{==}` | nothing is bound in an empty list | none (definitional) | -| `bound_head` | C (u) | `{==}` | one fixed bind is bound | none (helper pin) | -| `get_nil` | Q | `{==}` | `get` on an empty Matched is `""` | SHAKE-GET-1 (lemma) | -| `get_head` | C (u) | `{==}` | `get` reads one fixed bind | SHAKE-GET-1 | -| `get_all_nil` | Q | `{==}` | `get_all` on an empty Matched is empty | none (definitional) | -| `get_all_two` | C (u) | `{==}` | `get_all` of two fixed binds | SHAKE-GET-1 | -| `on_nil` | Q | `{==}` | no flag is on in an empty Matched | SHAKE-GET-1 (lemma) | -| `on_true` | C (u) | `{==}` | one fixed flag bound to `true` is on | SHAKE-GET-1 | -| `path_of_keeps` | Q | `{==}` | `path_of` returns the path field | none (definitional) | -| `parse_is_walk` | Q | `{==}` | `parse` is `finish` of `walk` of `start` | none (wiring) | -| `show_done` | Q | `{==}` | `show` of a Done is `ok` and the match | none (wording) | -| `show_fail` | Q | `{==}` | `show` of a Fail is `err` and the tag | none (wording) | -| `help_is_go` | Q | `{==}` | `help` is `help.go` from the root page | none (wiring) | -| `err_text_help` | Q | `{==}` | NeedHelp's error text is empty for every Cli and path | SHAKE-ERR-1 | -| `parse_flag_long` | C (u) | `{==}` | `--verbose greet` on the fixture | SHAKE-TOK-1 | -| `parse_flag_short` | C (u) | `{==}` | `-v greet` on the fixture | SHAKE-TOK-2 | -| `parse_opt_long` | C (u) | `{==}` | `greet --name Ada` on the fixture | SHAKE-TOK-6 | -| `parse_opt_eq` | C (u) | `{==}` | `greet --name=Ada` on the fixture | SHAKE-TOK-1 | -| `parse_opt_short` | C (u) | `{==}` | `greet -n Ada` on the fixture | SHAKE-TOK-6 | -| `parse_opt_glued` | C (u) | `{==}` | `greet -nAda` on the fixture | SHAKE-TOK-2 | -| `parse_pos` | C (u) | `{==}` | `greet Ada` on the fixture | SHAKE-PARSE-2 | -| `parse_default` | C (u) | `{==}` | `greet` fills `name=world` | SHAKE-PARSE-6 | -| `parse_add` | C (u) | `{==}` | `add 2 3` on the fixture | SHAKE-PARSE-2 | -| `parse_nested` | C (u) | `{==}` | `add 2 3 more` selects `add/more` | SHAKE-PARSE-4 | -| `parse_dash` | C (u) | `{==}` | `greet -- --name` binds `who=--name` | SHAKE-TOK-4 | -| `err_missing` | C (u) | `{==}` | `add 2` is missing `b` | SHAKE-PARSE-7 | -| `err_choice` | C (u) | `{==}` | `--color purple` is refused | SHAKE-PARSE-5 | -| `err_unknown_long` | C (u) | `{==}` | `--nope` is unknown | SHAKE-TOK-7 | -| `err_unknown_short` | C (u) | `{==}` | `-z` is unknown | SHAKE-TOK-7 | -| `err_help_root` | C (u) | `{==}` | `help` is NeedHelp at the root | SHAKE-PARSE-8 | -| `err_help_greet` | C (u) | `{==}` | `help greet` is NeedHelp at `greet` | SHAKE-PARSE-8 | -| `err_unexpected` | C (u) | `{==}` | `greet Ada extra` is unexpected `extra` | SHAKE-PARSE-2 | -| `parse_rest_none` | C (u) | `{==}` | no words bind no files | SHAKE-PARSE-3 | -| `parse_rest_one` | C (u) | `{==}` | one word binds one file | SHAKE-PARSE-3 | -| `parse_rest_many` | C (u) | `{==}` | two words bind two files in order | SHAKE-PARSE-3 | -| `parse_rest_dash` | C (u) | `{==}` | `-- --name a.bend` binds both as files | SHAKE-TOK-4 | -| `err_rest_missing` | C (u) | `{==}` | a required rest with no words is missing | SHAKE-PARSE-7 | -| `show_rest_many` | C (u) | `{==}` | `show` of a two-file parse | none (wording) | -| `help_root` | C (u) | `{==}` | the fixture's root page, byte for byte | SHAKE-HELP-2 (wording) | -| `help_greet` | C (u) | `{==}` | the fixture's `greet` page, byte for byte | SHAKE-HELP-2 (wording) | -| `help_add` | C (u) | `{==}` | the fixture's `add` page, byte for byte | SHAKE-HELP-2 (wording) | -| `help_rest` | C (u) | `{==}` | the rest fixture's page, byte for byte | SHAKE-HELP-2 (wording) | -| `help_rest_req` | C (u) | `{==}` | one required rest renders `...` | SHAKE-HELP-2 | -| `err_text_unknown` | C (u) | `{==}` | the text for `--nope`, byte for byte | SHAKE-ERR-1 (wording) | -| `copy_nil` | C (u) | `{==}` | `copy` of the empty list | SHAKE-ARGS-1 | -| `copy_one` | Q | `{==}` | `copy` of a one-word list | SHAKE-ARGS-1 | -| `argv_is_copy` | C (u) | `{==}` | `argv` is its body | none (definitional) | - -## Coverage by requirement - -| Requirement | Laws pointing toward it | Quantified among them | -| :---- | :---- | :---- | -| SHAKE-TOK-1 | `cut_eq_plain`, `cut_eq_value`, `by_long_flag`, `parse_flag_long`, `parse_opt_eq` | none | -| SHAKE-TOK-2 | `short_of_glued`, `short_of_one`, `by_short_flag`, `parse_flag_short`, `parse_opt_glued` | none | -| SHAKE-TOK-3 | none | none | -| SHAKE-TOK-4 | `parse_dash`, `parse_rest_dash` | none | -| SHAKE-TOK-5 | none | none | -| SHAKE-TOK-6 | `looks_flag_long`, `looks_flag_alone`, `parse_opt_long`, `parse_opt_short` | `looks_flag_long` (a lemma) | -| SHAKE-TOK-7 | `err_unknown_long`, `err_unknown_short` | none | -| SHAKE-PARSE-1 | none | none | -| SHAKE-PARSE-2 | `pos_of_keeps`, `parse_pos`, `parse_add`, `err_unexpected` | none (bolt's `cli.word_step` is the only one, in bolt) | -| SHAKE-PARSE-3 | `pos_of_rest`, `parse_rest_none`, `parse_rest_one`, `parse_rest_many` | none (bolt's `cli.walk_plain`, in bolt) | -| SHAKE-PARSE-4 | `find_sub_head`, `parse_nested` | none | -| SHAKE-PARSE-5 | `allowed_any`, `allowed_listed`, `allowed_other`, `err_choice` | `allowed_any` (a lemma) | -| SHAKE-PARSE-6 | `parse_default` | none | -| SHAKE-PARSE-7 | `err_missing`, `err_rest_missing` | none | -| SHAKE-PARSE-8 | `err_help_root`, `err_help_greet` | none | -| SHAKE-PARSE-9 | none | none | -| SHAKE-PARSE-10 | none | none | -| SHAKE-SPEC-1 | `rest_last_mid` | none | -| SHAKE-GET-1 | `get_nil`, `get_head`, `get_all_two`, `on_nil`, `on_true` | `get_nil`, `on_nil` (lemmas) | -| SHAKE-HELP-1 | none | none | -| SHAKE-HELP-2 | `help_root`, `help_greet`, `help_add`, `help_rest`, `help_rest_req` | none | -| SHAKE-ERR-1 | `err_text_help`, `err_text_unknown` | `err_text_help` (half of the row) | -| SHAKE-ARGS-1 | `copy_nil`, `copy_one` | `copy_one` (one step) | - -## Requirements against code - -The draft requirements come from the README and the header comment of `shake/main.bend`, since shake has no other statement of what it does. "Confirmed" means we ran the demo binary built from this tree; "by reading" means we read the code and did not run it. - -| Requirement | Verdict | Evidence | -| :---- | :---- | :---- | -| README: "`parse` binds flags, options, positionals, and nested commands" | holds | `main.bend:751-851`. Confirmed with `greet --name Ada -v`, `add 2 3 --times 2`, `add 2 3 more` (fixture). | -| README and `main.bend:4`: "A `--` ends option parsing: every word after it is a positional" | holds for `parse`; fails for the program a user runs | `parse.step.raw` (`main.bend:714-722`) does what the README says. The compiled runtime of bend 2.0.26 consumes the first `--` itself and passes the words after it unexamined, so `parse` never sees it. Confirmed: `demo greet -- --name` fails with "the following required argument was not provided: name", while LAWS.bend's `parse_dash` proves `who=--name` for the same words. `demo greet -- -- --name` prints `hello --name`. See finding F1. | -| README: "the runtime also strips `--threads`, `--gpu`, and `--gpu-build`" | partly | `--threads` and `--gpu` are stripped together with the word after them, and the runtime exits 1 when that word is not a count or `on`, `off` or a size. `--gpu-build` is not stripped: the runtime runs the GPU build step and exits 0 without running `main`. Confirmed: `demo greet --gpu-build` prints nothing, exit 0; `demo greet --threads x` prints `bend: expected a thread count of 1 or more after --threads`, exit 1. | -| README: "`--help` is consumed by the Bend runtime of a compiled binary and never reaches the program" | holds, before the first `--` | Confirmed: `demo greet --help` prints the runtime's usage. After a `--` it reaches `parse`: `demo greet -- --help` reports an unknown `--help`. | -| README: "A rest positional keeps every leftover word under one name; `get_all` reads that list" | holds | `parse.take_pos.keep` (`main.bend:563-568`) keeps a rest positional in the pending list; `get_all.bind` (`main.bend:405-410`) collects in bind order, and `parse.finish.miss` reverses binds into argv order. By reading. | -| README: "`get` still reads one value" | holds; which value is unstated | `get.bind` returns the first bind by that name after the reverse, so the first given wins. Confirmed: `demo greet --name Ada --name Bob` prints `hello Ada`. See F3. | -| README: "Print usage with `tool help` or `tool help `" | holds, with an accident | `parse.step.help` (`main.bend:693-700`). An unknown name in the path is skipped: `demo help nope` prints the root page and exits 0; `demo help nope greet` prints `greet`'s page. Confirmed. See F5. | -| `main.bend:2`: "`help` writes usage for a command path" | holds | `help.go` (`main.bend:1098-1105`). | -| `main.bend:145`: "`-` alone is not" a flag token | holds | Confirmed: `demo greet -` binds `who=-`. | -| `main.bend:330`: rest positionals are last and at most one | fails: nothing checks it | `rest.last` (`main.bend:323-328`) is called by no code, only by three closed laws. A spec with a rest positional before a plain one parses: the rest swallows every word and the later positional is never bound. By reading. See F6. | -| bolt's BOLT-TRUST-8: "shake v0.1.1 parses argv as its spec says" | as trusted, with nothing to trust | shake has no spec. See F12. | - -## What each entry point reads - -shake is a library. Its one IO entry point is `argv` in `shake/args.bend`; everything else is a pure function of its arguments, so the World and planner split that ez and bolt needed is already true of `parse`, `help` and `err_text`. - -| Entry point | Reads | Source | -| :---- | :---- | :---- | -| `parse(app, argv)` | the Cli and the word list, nothing else | `main.bend:850-851` | -| `help(app, path)` | the Cli and the path | `main.bend:1108-1110` | -| `err_text(app, e)` | the Cli's name, args and subs, and the error | `main.bend:1113-1131` | -| `argv()` | `IO.args()`, which is what the Bend runtime left of the process's argv | `args.bend:15-17` | - -What the runtime leaves is decided outside shake, in the C `main` bend 2.0.26 emits (read out of the bend binary with `strings`): it walks `argv[1..]`; on `--` it copies every later word through and stops looking; on `--help` it prints its own usage and exits 0; on `--gpu-build` it builds the GPU image and exits 0; on `--threads` and `--gpu` it consumes the next word as their value and exits 1 if that value is malformed; every other word is passed on. That is SHAKE-TRUST-2. - -No decision is made inside IO and no read falls back to a default, so the tracing found no bug of the ez kind. What it found is that the runtime's rules and shake's rules both claim `--`, and the runtime's run first. - -## Findings - -Every finding is recorded, not resolved. The RFC carries a REVIEW item for each one a requirement depends on. - -### Bugs - -- **F1. `--` never reaches `parse` in a compiled binary.** Confirmed. The README, `main.bend:4`, `parse_dash` and `parse_rest_dash` all describe `--` as shake's end of options, and in a compiled binary the runtime takes the first `--` for itself. A user who types `tool add -- -5 3` to pass a negative number gets "unexpected argument '-5'"; they must type `tool add -- -- -5 3`. The code is right about the words it is given; the documentation and the laws describe words no user can give with one `--`. -- **F2. The README build fails on a fresh clone.** Confirmed: `bend examples/demo/main.bend -o bin/demo.bin` fails with "cannot open output file bin/demo.bin" because `bin/` is not tracked. This is the bug ez's README had. -- **F3. The gate does not protect parsing.** Confirmed by the planted truncation bug above: every closed law passes on a parser that drops the seventh character of every value. - -### Behavior that looks accidental - -- **F4. A repeated option keeps its first value.** Confirmed: `greet --name Ada --name Bob` prints `hello Ada`. `get_all` returns both. clap 4 refuses a repeated single-valued option; getopt-style tools usually keep the last. -- **F5. `help` skips unknown names.** Confirmed: `help nope` prints the root page and exits 0. clap reports an unrecognized subcommand. -- **F6. No spec is ever checked.** By reading. `rest.last` is dead code. Nothing refuses two arguments with one spelling or one name (the first wins at lookup), a subcommand named `help` (it can never be selected), a default outside its own choices (it is bound without the choices test), or a required positional after an optional one. -- **F7. `-n=Ada` binds `=Ada`.** Confirmed. clap binds `Ada` for `-n=Ada`. -- **F8. Error text always shows the root usage line.** Confirmed: an unknown flag inside `greet` shows `Usage: demo [OPTIONS] [COMMAND]`. `err_text` has no path to show another. -- **F9. A missing option value and a missing required argument are one error.** Confirmed: `greet --name` reports "the following required argument was not provided: name". Both are `Missing{name}`. -- **F10. An empty value and no value read the same.** By reading: `get` returns `""` for an unbound name and for `--name=`. `on` is `get == "true"`, so an option given the value `true` is also on. -- **F11. A subcommand name always selects the subcommand.** By reading and confirmed on the fixture: before `--`, a word equal to a subcommand's name is never a positional value. clap does the same by default. We list it because a row needs to say so. - -### Behavior no requirement mentions, and other programs - -- **F12. bolt depends on shake's internals, and trusts a spec that does not exist.** bolt v1.6.2 pins shake v0.1.1 (`cb02b47`, whose `shake/` tree matches this one), lists it as BOLT-TRUST-8, and proves its own CLI laws by unfolding eight walker defs (`Shake.parse.step`, `Shake.parse.step.end`, `Shake.parse.step.help`, `Shake.parse.step.kind.go`, `Shake.parse.word.go`, `Shake.parse.take_pos`, `Shake.parse.walk`, `Shake.parse.finish`), two accessor helpers (`Shake.get.bind`, `Shake.get_all.bind`), and the walker's `St` and `Mode` types (`bolt/PROOF.bend`, `cli.word_step` and `cli.walk_plain`). Any rename or restructuring of shake's walker breaks bolt's proofs the day bolt bumps its pin, and nothing in shake says which names are its interface. ez uses only the public surface (`app`, `sub`, `flag`, `opt`, `pos`, `parse`, `help`, `err_text`, `get`, `on`, `path_of`). -- **F13. The pinned bolt cannot enforce the model.** shake pins bolt v0.4.0, which has no `trace` rule; v1.6.2 has `trace`, but its `closed` rule accepts `for u: Unit` just as v0.4.0 does. - -### Requirements with no code - -- The README says a rest positional is "every leftover word", and nothing checks that the rest is the last positional (F6). - -## Rollout progress - -| Phase | State | What landed | -| :---- | :---- | :---- | -| Preliminary | done | This inventory and the RFC; the RFC accepted with every review item resolved; the README builds from a fresh clone (`mkdir -p bin`) and, with `main.bend` and `src/cli.bend`, says what a compiled program's runtime takes before shake (F1, F2). | -| Zero | done | The code moved to `src/` behind `main.bend`; ez at `df6d616`; bolt at `ada294e` as a `[tools.bolt]` pin in the lock; the newer style rules' findings fixed; `coverage` at warn, IO marked `# noqa: L001`. | -| One | done | SPEC.md; 73 laws and `src/sample.bend` deleted (every closed law, and every quantified law marked definitional, wiring or wording above); `err_text_help` restated over `main.bend` and tagged SHAKE-ERR-1 as a partial law; `looks_flag_long`, `allowed_any`, `get_nil`, `on_nil` and `copy_one` kept untagged as lemmas; `trace` at error. `coverage` now reports 41 defs no quantified law reaches, the map of what the rows below must reach. | -| Two | done (PARSE-5, TOK-3, TOK-5 and TOK-7 moved to phase three, since each needs a walker step law) | SHAKE-ERR-1 proved (`err_text_iff`, with `err_text_help`). The last-value change for `get` (REVIEW-4) landed on its own, then SHAKE-GET-1 proved by seven laws over `main.bend`, with `hit_append`, `bind_values_append` and `last_snoc` as untagged lemmas and `src/eq.bend` (string equality is reflexive, from ez's `check/eq.bend`); `get_last` is also a partial law of SHAKE-PARSE-10. Each new proof fails when replaced by `{==}`, and `get_last` fails against the old first-value `get`. SHAKE-ARGS-1 proved by `copy_keeps` (the copy read back is the list; it fails against a `copy` that drops words), which replaces the `copy_one` lemma; `argv`'s IO wiring became SHAKE-TRUST-4. SHAKE-PARSE-9 proved by `fail_stays` (frame law, over `parse` with the walker's failure as premise; lemmas `walk_append`, `dead_walk`, `fail_from`); it fails against a walker that recovers after an error. The `help` change (REVIEW-6) landed on its own: `parse` refuses a word after `help` that is not a subcommand where it stands (SHAKE-PARSE-8 stays pending until its law lands). `check` (REVIEW-7) landed on its own: `src/check.bend`, exported from `main.bend` with `SpecErr` and `spec_err_text`, not called by `parse`; `rest.last` deleted (F6). SHAKE-SPEC-1 stays pending until its count and frame laws land. Every decided behavior change has now landed. | -| Three | done | The design, [shake-walker-proofs.md](shake-walker-proofs.md), with its spike: bolt's 18 walker lemmas check against today's walker unchanged. WP0 started: `src/walk.bend`, general over any rest positional. WP1 started: SHAKE-TOK-7's refusals, `unknown_long` and `unknown_short`, over `parse` from any walker state reached by the words before (REVIEW-W1's premise form), through step lemmas and `fail_stays`; lemmas `prefix_empty`, `drop_zero`. Each fails as `{==}`, and against a walker that skips an unknown option. The design changes of REVIEW-4, 5 and 11 to 14 landed one PR each, then WP1's refusals on the new shapes, all through the general `refused` lemma: `long_no_name` (TOK-1), `flag_long_valued` (TOK-5, with the not-yet-given premise REVIEW-4 needs), `value_flag_shaped` and `value_absent` (TOK-6, now `NoValue`), `no_pos_left` (PARSE-2), `choice_refused` (PARSE-5), `help_unknown` (PARSE-8), and `repeated_long_flag` and `repeated_long_opt` (PARSE-10, through `once_dead`). Each is caught by a walker mutant that accepts what it refuses. WP2 started: `binds_grow` in `src/grow.bend` (a walker only ever puts bindings in front of those it holds, one lemma per arm of `step`, shaped like bolt's `extends`) and `kept_all` and `kept`, the binding counterparts of `refused`: a binding a step makes is read back by `get_all` of the successful parse, after the values bound before it. Through them: `value_binds` (TOK-6, now proved), `pos_next` and `pos_binds` (PARSE-2), `dd_step`, `raw_next`, `raw_binds`, `raw_no_pos` and `raw_refused` (TOK-4, now proved), `long_binds` (TOK-1, and PARSE-10's `many` half for long spellings), and `value_refused` and `long_refused` (PARSE-5). Stating PARSE-5 found a bug, fixed first: an option's value was checked against a parent's argument of the same name. Walker mutants that drop or replace bindings, bind the name for the value, keep `--` from switching to positionals, or refuse a repeated `many` option each fail the gate. REVIEW-16 then made bindings per command: `binds_grow` became `gw.reach` (a word stays in the current command, putting bindings in front, or enters a subcommand, which keeps the command it leaves above it, or leaves the walker stuck in help or failed), and `kept_all` and `kept` now conclude over `get_all` of the command at the walker's path in the result (`all_at`), through `gw.finished`, `gw.at_build` and the depth invariant `gw.depth`. SHAKE-GET-1 is restated over the new `Matched` and SHAKE-GET-2 proves its navigation. Walker mutants that let a subcommand inherit its parent's bindings, drop a command's bindings from its Matched, build the levels leaf first, forget the parent on entering, or let `at` ignore names each fail the gate. Then `cut_first_eq` and `cut_no_eq`: the `=` cut of a long option's body splits at its first `=`, the value verbatim, which discharges `long_binds`' cut premise, so SHAKE-TOK-1 is proved; a cut that ignores `=`, or loses a char of the value, fails the gate. SHAKE-PARSE-3 is proved by `rest_next` and `rest_binds` (before `--`) and `rest_raw_next` and `rest_raw_binds` (after it), general over a rest with choices, not only bolt's `files`: each word binds the rest and leaves it pending, and `get_all` of its command's Matched reads the words in order; a walker that consumes a rest like a plain positional fails the gate. SHAKE-PARSE-6 and PARSE-7 are proved per command over the finished walker's frame (`fin.at`: the Matched of the command at a path is its level, defaults filled): `default_filled`, `bound_kept`, `no_default` and `no_argument` for defaults, and `required_present` and `required_missing` for required arguments; a fill that overwrites a bound value, a missing default that binds the empty string, a required check that never fires, or parents left without their defaults each fail the gate. SHAKE-PARSE-4 is proved by `enter_step` (entering a subcommand: its arguments current, its positionals pending, no bindings of its own, the command left above it; also SHAKE-TOK-7's half about the current argument list), `enter_missing`, `none_blocking` and `first_blocking`; the row now says what blocks a subcommand as the code does: a pending positional that is required, has no default and is not a rest. SHAKE-PARSE-8 is proved by `help_step` (`help` starts a help path), `help_walk` (each word naming a subcommand under the one before extends it), `help_path` (the words ending there fail with NeedHelp of the whole path) and WP1's `help_unknown`; a help path that does not grow, or a `help` never recognized, fails the gate. SHAKE-PARSE-2 is proved with `start_state` (the root's positionals pending at the start), `pos_of_app`, `pos_of_pos` and `pos_of_opt` (the pending list is exactly the positional arguments, in spec order), `enter_step` (a subcommand's own on entry), and `help_word_next` and `help_word_binds` (a word `help` once a positional is bound binds like any other); positionals pending out of order, or `help` read as a request after a positional, fail the gate. The short clusters: `short_step` (a word `-...` is read as a cluster from the walker as it stood) and one law per kind of letter over the cluster function, `letter_flag`, `letter_flag_eq`, `letter_flag_again`, `letter_opt_again`, `letter_unknown`, `letter_value`, `letter_value_eq`, `letter_value_next` and `letter_value_bad`, with `cluster_dead` (a letter after a failed one changes nothing, which stating PARSE-10 found broken and was fixed first); and `plain_word_step` and `dash_word_step` for TOK-3. With them SHAKE-TOK-2, TOK-3, TOK-5, TOK-7, PARSE-5 and PARSE-10 are proved, and no pending row has partial laws left. Mutants that keep the `=` of `-n=Ada`, end a cluster at a flag, or drop a char of a glued value fail the gate. SHAKE-HELP-1 is proved by `help_page` (the help text for a path is the page of the command the path reaches), `reach_child` and `reach_skip` (a name found under the current command moves to it, an unknown one stays put), stated over law-side `reach` and `page` helpers in `src/LAWS.bend`; SHAKE-ERR-2 by `err_path_at` (each error names the command path it arose at) and `err_text_usage` (an error's text shows that command's usage line), with the refusal laws tagged too, since each names the path its error carries. An error text that shows the root's usage, or a help walk that loses the subcommands on an unknown name, fails the gate. SHAKE-HELP-2 is proved by `cmds_listed` (a page's Commands block is one line per subcommand, in spec order, then `help`'s), `opts_listed` (its Options block is one line per flag and option, from Base's `List.filter`, in spec order) and `usage_listed` (the usage line names the positionals, filtered the same way, each as a law-side `mark`: `` or `[NAME]`, then `...` for a rest); commands out of order, no `help` line, a dropped option line, swapped brackets, a positional named twice, or `...` after every positional each fail the gate. SHAKE-SPEC-1 is proved by `check_listed` (WP6): rather than the counts and frame law the design planned, it states the whole report list, which fixes both at once. `check` of a Cli is its root's reports, then each subcommand's at its own path, depth first; a command's reports are each argument's against the arguments before it (a name or spelling they have, a default outside nonempty choices), then each positional's against those before it (a rest with one after it, a required one after an optional one), then each subcommand's against its earlier siblings (a name they have, the name `help`); all stated in `src/LAWS.bend` over the arguments before, not `check`'s accumulators. A `check` that skips nested commands, gives them reversed paths, compares long spellings with short ones, refuses a default when there are no choices, forgets an optional positional, forgets a subcommand's name, or allows a subcommand named `help` fails the gate. SHAKE-PARSE-1 (WP5) has its first law, `values_given`: when the parse succeeds, every binding in the Matched of a command on the selected path is `true`, a piece of one of the words, verbatim (what is left of a word once some chars are dropped from its front), or the default of one of that command's arguments. It is proved by a walker invariant, `gv.good` (every value a walker holds, at every level, is `true` or a piece of one of the words), kept by every arm of `step` (`gv.step`), so by every walk from the start (`gv.walk`), then read through the finished frame (`fin.at`) and the fill, which adds only the command's own defaults. Stating it found the row wrong about flags, which bind `true`, not a piece of a word; the row now says so. A walker that truncates or reverses values, binds a flag to anything but `true`, fills a default with the argument's name, or binds an option's name for its value fails the gate in `values_given`'s own proof, each also isolated from the earlier laws. Then `values_here`: each binding of a command is named after one of that command's own arguments, and each piece comes from the words read while that command was current (`mid`, between the word that selected it, or the start, and the word that selects a subcommand under it, or the end). It is proved by a second walker invariant, `gn.good`: every binding of the current command is named after one of its arguments and is `true` or a piece of the words, and the option waiting for a value and the pending positionals are its own; entering a subcommand empties the bindings, so a walk over `mid` from the command's first word keeps them within `mid`. The fill adds only the command's own defaults (`gn.dsub`). A walker whose subcommand inherits its parent's bindings, binds a positional or a flag under another name, or truncates values fails the gate in `values_here`'s own proof, each isolated from the earlier laws. Which argument each kind of word binds is proved per word shape by the TOK and PARSE-2/3 laws. Last, the row's count sentence, reworded (the maintainer's decision) to the two per-word laws it was there for, since a count over the words would need a second parser: `one_value_per_word` (from any walker, a word adds at most one binding other than `true`: flags add only `true`, and the first letter of a cluster that takes a value ends it; `nd.*`) and `word_used` (a word read by a walker that can still succeed always changes it; `nu.*`, with a cluster invariant `nu.J`). For `word_used`, `-` alone is now told apart by what follows the dash (`String.is_empty(String.drop(tok, 1n))`) rather than by comparing the word with `"-"`: the same for every word that starts with `-`, and a proof needs no char equality; the demo answers 48 cases the same before and after. A word bound twice, a cluster that goes on after an option letter, an ignored `--`, an ignored flag, or an ignored extra word each fails the gate in the new laws' own proofs. SHAKE-PARSE-1 is proved, and no row is pending. | - -The planted truncation bug (F3) is caught: a walker that drops the seventh char of every value fails the gate at the value laws of phase three (`wk.walk_plain` first) and, with those set aside, at PARSE-1's `values_given` (`gv.put`). diff --git a/docs/rfc/shake-spec.md b/docs/rfc/shake-spec.md index 0d462f7..b8ee5af 100644 --- a/docs/rfc/shake-spec.md +++ b/docs/rfc/shake-spec.md @@ -4,15 +4,15 @@ Read at `b93357a` on `main` ("chore: bump Bend to 2.0.26 (#13)"), bend 2.0.26, b ## Draft Status -**State:** Accepted. Every review item below is resolved: the maintainer accepted each recommendation. +**State:** Accepted and implemented. Every review item below is resolved, and every row of SPEC.md is proved (see [Rollout](#rollout)). -This draft was written from the code at `b93357a`, from the evidence in [shake-law-inventory.md](shake-law-inventory.md), and from the positions reached by the specifications of ez ([ez-spec.md](https://github.com/Emerging-Patterns/ez/blob/master/docs/rfc/ez-spec.md)) and bolt ([bolt-spec.md](https://github.com/Emerging-Patterns/bolt/blob/v1.6.2/docs/rfc/bolt-spec.md)). Every verdict was checked against the code, and most were confirmed by running the demo binary built from a fresh copy of this tree. The items below are decisions this draft makes and asks a maintainer to confirm. Each one also appears inline where the decision lives. The first two come first because the rest depend on them. REVIEW-2, REVIEW-9 and REVIEW-10 were resolved by the change that moved the code into `src/` behind `main.bend`; the paths below that say `shake/main.bend` are as read at `b93357a` and now live in `src/cli.bend`. +This draft was written from the code at `b93357a`, from the audit in [Appendix: the audit](#appendix-the-audit) (its law-by-law tables were `docs/rfc/shake-law-inventory.md`, folded into this RFC and deleted once the rollout finished; they are in git at `72fd9a5`), and from the positions reached by the specifications of ez ([ez-spec.md](https://github.com/Emerging-Patterns/ez/blob/master/docs/rfc/ez-spec.md)) and bolt ([bolt-spec.md](https://github.com/Emerging-Patterns/bolt/blob/v1.6.2/docs/rfc/bolt-spec.md)). Every verdict was checked against the code, and most were confirmed by running the demo binary built from a fresh copy of this tree. The items below are decisions this draft makes and asks a maintainer to confirm. Each one also appears inline where the decision lives. The first two come first because the rest depend on them. REVIEW-2, REVIEW-9 and REVIEW-10 were resolved by the change that moved the code into `src/` behind `main.bend`; the paths below that say `shake/main.bend` are as read at `b93357a` and now live in `src/cli.bend`. **Items for review:** - [x] - [x] -- [x] +- [x] - [x] - [x] - [x] @@ -60,7 +60,7 @@ shake is a command-line argument parser for Bend 2, about 1100 lines in `shake/m ### How shake proves things today -shake has one LAWS.bend with 79 laws and one PROOF.bend in which every proof is `{==}`. The gate passes in about a second, and the pinned bolt reports `clean`. The inventory shows why neither means much. 53 laws state one fixed call: 25 parse a fixed command line against the fixtures in `shake/sample.bend` (21 of them through `show`'s one-line rendering), 6 compare help or error pages byte for byte, and the other 22 pin one helper on one input. Each carries `for u: Unit`, a binder its statement never uses, and that is enough for the `closed` rule of both the pinned bolt and the current one to accept it. Of the 26 laws that really quantify, 20 say that a definition unfolds to its body or how two defs are wired, and the other 6 are small true lemmas. None quantifies over an argv and a spec together. +shake has one LAWS.bend with 79 laws and one PROOF.bend in which every proof is `{==}`. The gate passes in about a second, and the pinned bolt reports `clean`. The audit showed why neither meant much. 53 laws state one fixed call: 25 parse a fixed command line against the fixtures in `shake/sample.bend` (21 of them through `show`'s one-line rendering), 6 compare help or error pages byte for byte, and the other 22 pin one helper on one input. Each carries `for u: Unit`, a binder its statement never uses, and that is enough for the `closed` rule of both the pinned bolt and the current one to accept it. Of the 26 laws that really quantify, 20 say that a definition unfolds to its body or how two defs are wired, and the other 6 are small true lemmas. None quantifies over an argv and a spec together. The consequence is measurable. We changed `parse.put` to keep only the first six characters of every value. The gate printed `All terms check.`, bolt printed `clean`, and the demo printed `hello Alexan` for `greet --name Alexandra`. @@ -246,15 +246,15 @@ Not changed: the wording of each message, which no row promises. ### How we will know it worked -The gate passing will mean something: the truncation bug from the inventory, and any bug that binds a value the user did not type or to a name it was not given for, fails PARSE-1's proof. bolt's `trace` reports nothing at error, and `closed` reports nothing because no closed law is left. bolt's BOLT-TRUST-8 names SHAKE rows, and bolt's CLI proofs cite shake's laws instead of shake's walker. +The gate passing will mean something: the truncation bug from the audit, and any bug that binds a value the user did not type or to a name it was not given for, fails PARSE-1's proof. bolt's `trace` reports nothing at error, and `closed` reports nothing because no closed law is left. bolt's BOLT-TRUST-8 names SHAKE rows, and bolt's CLI proofs cite shake's laws instead of shake's walker. ## Abandoned Ideas -**Keep the closed laws as `# toward` trails.** ez did this for a while under bolt v0.9.0. It kept ez on an old bolt, and ez deleted the trails once the replacing laws were written down. shake's closed laws encode one accident each (the fixture parse through `show`, pages byte for byte), and the inventory keeps the map, so the trails would tell nobody anything. +**Keep the closed laws as `# toward` trails.** ez did this for a while under bolt v0.9.0. It kept ez on an old bolt, and ez deleted the trails once the replacing laws were written down. shake's closed laws encode one accident each (the fixture parse through `show`, pages byte for byte), and the audit kept the map, so the trails would tell nobody anything. **Prove each fixture command line.** Stating `parse(Sample.spec(), ["greet", "--name", "Ada"])` for more command lines is the same closed law at a larger count. It is what we have, and the planted bug shows what it misses. -**Prove shake equal to a reference parser.** A second implementation shares the first's reading of the corner cases, which is where every accident in the inventory lives. bolt and ez both deleted their refactor-equivalence laws for this reason. +**Prove shake equal to a reference parser.** A second implementation shares the first's reading of the corner cases, which is where every accident the audit found lives. bolt and ez both deleted their refactor-equivalence laws for this reason. **Make help and error wording contractual.** It is what users see, which argues for it. But no program depends on the bytes, a wording change would break every such law, and the six page laws show the cost. The rows state structure (every subcommand listed once, in order) instead. @@ -280,14 +280,24 @@ Each phase leaves the gate green, bolt clean at the pinned version, and SPEC.md | Phase | What lands | What is true after | | :---- | :---- | :---- | -| Preliminary | this RFC and the inventory (no code change); the two docs changes | the README builds from a fresh clone and describes `--` as users meet it | +| Preliminary (done) | this RFC and the audit (no code change); the two docs changes | the README builds from a fresh clone and describes `--` as users meet it | | Zero (done) | the code moved to `src/` behind `main.bend`; ez at `df6d616`; bolt at `ada294e` as a `[tools.bolt]` pin, its style findings fixed, `coverage` at warn with `# noqa: L001` on IO | the tree is clean under a bolt that has `trace` and `noqa` | -| One | SPEC.md from this RFC; 73 laws, `sample.bend` and `show` deleted; `err_text_help` tagged; `trace` at error; `closed` at error | every row is pending or trusted, and the gate stops pretending | -| Two | the cheap rows: PARSE-9 (frame), ERR-1, GET-1 (after REVIEW-4's change), ARGS-1, PARSE-5, TOK-3, TOK-5, TOK-7 | the first proved rows | -| Three | the spike, then PARSE-2 and PARSE-3; bolt bumps shake and cites them; then TOK-1, TOK-2, TOK-4, TOK-6, PARSE-4, PARSE-6, PARSE-7, PARSE-8 | BOLT-TRUST-8 names SHAKE rows | -| Four | `check` and SPEC-1; then PARSE-1; then HELP-1 and HELP-2; `coverage` back at error | no pending rows; the inventory is folded into this RFC and deleted | +| One (done) | SPEC.md from this RFC; 73 laws, `sample.bend` and `show` deleted; `err_text_help` tagged; `trace` at error; `closed` at error | every row is pending or trusted, and the gate stops pretending | +| Two (done) | the cheap rows: PARSE-9 (frame), ERR-1, GET-1 (after REVIEW-4's change), ARGS-1, PARSE-5, TOK-3, TOK-5, TOK-7 | the first proved rows | +| Three (done) | the spike, then PARSE-2 and PARSE-3; bolt bumps shake and cites them; then TOK-1, TOK-2, TOK-4, TOK-6, PARSE-4, PARSE-6, PARSE-7, PARSE-8 | BOLT-TRUST-8 names SHAKE rows | +| Four (done) | `check` and SPEC-1; then PARSE-1; then HELP-1 and HELP-2; `coverage` back at error | no pending rows; the inventory is folded into this RFC and deleted | -The finish line: no pending rows, every closed law deleted, `trace`, `closed` and `coverage` at error, and bolt citing shake's laws rather than its walker. +The finish line: no pending rows, every closed law deleted, `trace`, `closed` and `coverage` at error, and bolt citing shake's laws rather than its walker. All of it but the last holds; bolt's side is bolt#193 and bolt#194. + +### Rollout record + +- **Preliminary and Zero.** The README builds from a fresh clone (`mkdir -p bin`) and says what the runtime takes before shake (F1, F2). The code moved to `src/` behind `main.bend`; ez and bolt are pinned in the lock (`[tools.bolt]`); IO is marked `# noqa: L001`. +- **One.** SPEC.md. 73 laws, `src/sample.bend` deleted; `trace` and `closed` at error. +- **Two.** SHAKE-ERR-1, GET-1 (after REVIEW-4 made `get` read the last value), ARGS-1, PARSE-9 (a failed walk stays failed). The decided changes of REVIEW-6 (`help` refuses an unknown name) and REVIEW-7 (`check`) landed on their own. +- **Three.** The walker proofs of [shake-walker-proofs.md](shake-walker-proofs.md): refusals through one `refused` lemma; bindings through `kept_all` and `kept` over the invariant `gw.reach`; per-command readers after REVIEW-16 (clap's model: each command keeps its own bindings). SHAKE-TOK-1 to TOK-7, PARSE-2 to PARSE-8 and PARSE-10, GET-2. Stating PARSE-5 found an option's value checked against a parent's choices, and stating PARSE-10 found a failed cluster letter revived by the next one; both were fixed first. +- **Four.** SHAKE-HELP-1, HELP-2, ERR-2, SPEC-1 (`check`'s whole report list as one law), then PARSE-1 in four laws: `values_given` (every value is `true`, a verbatim piece of a word, or a default), `values_here` (named after the command's own arguments, from its own words), and, replacing the count sentence by the maintainer's decision, `one_value_per_word` and `word_used` (a word binds at most one value and is never ignored). `-` alone is recognized by what follows the dash, unchanged in behavior. `show` was deleted (nothing used it), and `coverage` is at error: each def no law applies to (IO, the builders, type aliases, proof machinery, the example) says why with `# noqa: L001`, and `spec_err_where` covers the report texts of `check`. + +Each proof in phases Two to Four was checked by planting the bug it is meant to catch; the PRs name each mutant and where the gate failed. ## Future Steps @@ -296,3 +306,31 @@ The finish line: no pending rows, every closed law deleted, `trace`, `closed` an **Ask bend to pass `--` through.** If the runtime left `--` in the list when it follows the program's own words, shake's `--` would work with one dash-dash. That is a change to bend's runtime and to every compiled Bend program, so we record it rather than depend on it. **Siblings.** ez's CLI would gain the same guarantees by citing SHAKE rows in its own spec, and a strict `closed` that sees through unused binders (REVIEW-9) protects every repository in the family from shake's pattern. + +## Appendix: the audit + +Read at `b93357a` with bend 2.0.26, bolt v0.4.0 (pinned) and bolt v1.6.2 (current). The proof gate was `bend shake/PROOF.bend`; the linter the pinned bolt over the whole tree; the demo binary was built from a fresh copy of the tracked files, following the README. + +| File | Laws | Quantified | Closed | Quantified proved by `{==}` | +| :---- | :---- | :---- | :---- | :---- | +| `shake/LAWS.bend` | 79 | 26 | 53 | 26 | + +Each closed law carried `for u: Unit`, a binder its statement never used, which let both bolts' `closed` rule accept it. Of the quantified laws, 20 restated a definition's unfolding, wiring or `show`'s format; 5 were small true lemmas (`looks_flag_long`, `allowed_any`, `get_nil`, `on_nil`, `err_text_help`) and one was a step of `copy`. No law quantified over an argv and a spec together. Planting a bug that truncated every value to six characters left the gate green. + +### Findings and what became of them + +| | Finding | Outcome | +| :-- | :-- | :-- | +| F1 | `--` never reaches `parse` in a compiled binary: the runtime takes the first one | SHAKE-TRUST-2; the README's `-- --` note | +| F2 | the README build failed on a fresh clone (`bin/` untracked) | `mkdir -p bin` in the README | +| F3 | the gate did not protect parsing: a truncating parser passed | caught by the value laws of phase Three and by `values_given` | +| F4 | a repeated option kept its first value | REVIEW-4: `get` reads the last value; a flag or single-valued option given twice is refused (PARSE-10) | +| F5 | `help` skipped unknown names | REVIEW-6: refused (PARSE-8) | +| F6 | no spec was ever checked | REVIEW-7: `check` (SPEC-1) | +| F7 | `-n=Ada` bound `=Ada` | REVIEW-5: binds `Ada` (TOK-2) | +| F8 | error text always showed the root's usage | REVIEW-13: errors carry their path (ERR-2) | +| F9 | a missing option value and a missing argument were one error | `NoValue` (TOK-6) | +| F10 | an empty value and no value read the same | unchanged; [Future Steps](#future-steps) | +| F11 | a subcommand's name always selects it | kept, as clap reads it ([Risks](#risks)) | +| F12 | bolt proves its CLI by unfolding shake's private walker, and trusts a spec that did not exist | SPEC.md now exists; bolt#193 (the proofs bolt can delete) and bolt#194 (citing shake's rows) | +| F13 | the pinned bolt could not enforce the model (no `trace`; `closed` accepted unused binders) | bolt pinned at `ada294e`, which has `trace`; every closed law is deleted, so `closed` has none left to miss | diff --git a/examples/demo/main.bend b/examples/demo/main.bend index 3488c87..2b87a33 100644 --- a/examples/demo/main.bend +++ b/examples/demo/main.bend @@ -3,7 +3,7 @@ import Base import ../../main.bend as Shake # the program spec -def spec() -> Shake.Cli: +def spec() -> Shake.Cli: # noqa: L001 the example program, not the library Shake.app("demo", "A tiny command-line program.", Some{"0.1.0"}, [Shake.flag("verbose", Some{"v"}, Some{"verbose"}, "More output")], [ @@ -44,7 +44,7 @@ def greet.tags(tags: List<&2, String>) -> IO(Unit): IO.print("tags: " ++ String.join(hh <> tt, " ")) # the value bound to `name`, or "" when nothing bound it -def text(+mm: Shake.Matched, +name: String) -> String: +def text(+mm: Shake.Matched, +name: String) -> String: # noqa: L001 the example program, not the library Maybe.default(&2, String, Shake.get(mm, name), "") # a successful greet: `who` when given, else `--name`, which has a default; diff --git a/main.bend b/main.bend index cdc3452..40fe17a 100644 --- a/main.bend +++ b/main.bend @@ -18,11 +18,11 @@ def Cli() -> Data: S.Cli # a nested command -def Sub() -> Data: +def Sub() -> Data: # noqa: L001 a type alias of the interface S.Sub # one argument: a flag, an option, a positional or a rest positional -def Arg() -> Data: +def Arg() -> Data: # noqa: L001 a type alias of the interface S.Arg # a successful parse, one command at a time: the bindings the command made, @@ -35,7 +35,7 @@ def ParseErr() -> Data: S.ParseErr # one way a spec contradicts itself -def SpecErr() -> Data: +def SpecErr() -> Data: # noqa: L001 a type alias of the interface K.SpecErr # a program: name, about, optional version, top-level args and commands @@ -49,7 +49,7 @@ def app( S.app(name, about, version, args, subs) # a nested command -def sub( +def sub( # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state +name: String, +about: String, args: List<&2, S.Arg>, @@ -58,7 +58,7 @@ def sub( S.sub(name, about, args, subs) # a boolean flag -def flag( +def flag( # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state +name: String, short: Maybe<&2, String>, long: Maybe<&2, String>, @@ -67,7 +67,7 @@ def flag( S.flag(name, short, long, help) # a valued option -def opt( +def opt( # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state +name: String, short: Maybe<&2, String>, long: Maybe<&2, String>, @@ -80,7 +80,7 @@ def opt( # an option that may be given more than once; `get_all` reads every value, in # order, and `get` the last -def many( +def many( # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state +name: String, short: Maybe<&2, String>, long: Maybe<&2, String>, @@ -92,7 +92,7 @@ def many( S.many(name, short, long, help, required, default, choices) # a positional -def pos( +def pos( # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state +name: String, +help: String, required: Bool, @@ -102,7 +102,7 @@ def pos( S.pos(name, help, required, default, choices) # a rest positional: every leftover word, as one name -def rest( +def rest( # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state +name: String, +help: String, required: Bool, diff --git a/src/LAWS.bend b/src/LAWS.bend index 42a5133..a7a70df 100644 --- a/src/LAWS.bend +++ b/src/LAWS.bend @@ -2765,3 +2765,30 @@ law word_used: for h_live: {Grow.gw.live(st) == True{} : Bool} for h_same: {S.parse.step(tok, st) == st : S.St} Empty + +# the command path a report of `check` is at +def spec_path(err: K.SpecErr) -> List<&2, String>: + match err: + case K.RestNotLast{path, _n}: + path + case K.SameName{path, _n}: + path + case K.SameShort{path, _s}: + path + case K.SameLong{path, _l}: + path + case K.SameSub{path, _n}: + path + case K.HelpSub{path}: + path + case K.DefaultNotChoice{path, _n, _v}: + path + case K.RequiredAfterOptional{path, _n}: + path + +# LAW: the text of every report of `check` says first where it is: `spec: ` +# at the root, else the command's path (a lemma for SHAKE-SPEC-1's reports) +law spec_err_where: + for +err: K.SpecErr + exs msg: String + {Shake.spec_err_text(err) == K.at(spec_path(err)) ++ msg : String} diff --git a/src/PROOF.bend b/src/PROOF.bend index a3b9b98..3e22d1b 100644 --- a/src/PROOF.bend +++ b/src/PROOF.bend @@ -9652,3 +9652,22 @@ def Laws.word_used(tok, st, h_live, h_same): nu.need_w(S.looks_flag(tok), nn, tok, args, up, subs, path, binds, pos, raw, seen, S.Need{nn}, {==}, h_same) case S.Free{}: nu.rawf(raw, tok, args, up, subs, path, binds, pos, seen, S.Free{}, {==}, {==}, {==}, h_same) + +def Laws.spec_err_where(err): + match err: + case K.RestNotLast{+path, +name}: + ("rest positional '" ++ name ++ "' is not the last positional", {==}) + case K.SameName{+path, +name}: + ("two arguments are named '" ++ name ++ "'", {==}) + case K.SameShort{+path, +short}: + ("two arguments are spelled '-" ++ short ++ "'", {==}) + case K.SameLong{+path, +long}: + ("two arguments are spelled '--" ++ long ++ "'", {==}) + case K.SameSub{+path, +name}: + ("two subcommands are named '" ++ name ++ "'", {==}) + case K.HelpSub{+path}: + ("a subcommand is named 'help', which `parse` keeps for help", {==}) + case K.DefaultNotChoice{+path, +name, +value}: + ("the default '" ++ value ++ "' of '" ++ name ++ "' is not one of its choices", {==}) + case K.RequiredAfterOptional{+path, +name}: + ("required positional '" ++ name ++ "' follows an optional one", {==}) diff --git a/src/cli.bend b/src/cli.bend index a553408..d561bc5 100644 --- a/src/cli.bend +++ b/src/cli.bend @@ -118,7 +118,7 @@ def app( Cli{name, about, version, args, subs} # a nested command -def sub( +def sub( # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state +name: String, +about: String, args: List<&2, Arg>, @@ -127,7 +127,7 @@ def sub( Sub{name, about, args, subs} # a boolean flag -def flag( +def flag( # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state +name: String, short: Maybe<&2, String>, long: Maybe<&2, String>, @@ -136,7 +136,7 @@ def flag( Arg{name, short, long, Flag{}, help, False{}, None{}, []} # a valued option -def opt( +def opt( # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state +name: String, short: Maybe<&2, String>, long: Maybe<&2, String>, @@ -148,7 +148,7 @@ def opt( Arg{name, short, long, Opt{}, help, required, default, choices} # an option that may be given more than once; `get_all` reads every value -def many( +def many( # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state +name: String, short: Maybe<&2, String>, long: Maybe<&2, String>, @@ -160,7 +160,7 @@ def many( Arg{name, short, long, Many{}, help, required, default, choices} # a positional -def pos( +def pos( # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state +name: String, +help: String, required: Bool, @@ -170,7 +170,7 @@ def pos( Arg{name, None{}, None{}, Pos{}, help, required, default, choices} # a rest positional: every leftover word, as one name -def rest( +def rest( # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state +name: String, +help: String, required: Bool, @@ -1393,57 +1393,6 @@ def parse.finish(st: St) -> Result<&2, &2, ParseErr, Matched>: def parse(app: Cli, argv: List<&2, String>) -> Result<&2, &2, ParseErr, Matched>: parse.finish(parse.walk(argv, parse.start(app))) -# a ParseErr as a short tag -def show.err(ee: ParseErr) -> String: - match ee: - case UnknownFlag{_at, word}: - "unknown " ++ word - case Missing{_at, name}: - "missing " ++ name - case NoValue{_at, name}: - "novalue " ++ name - case BadValue{_at, name, value}: - "bad " ++ name ++ " " ++ value - case NeedHelp{path}: - "help " ++ String.join(path, " ") - case Unexpected{_at, arg}: - "unexpected " ++ arg - case Repeated{_at, name}: - "repeated " ++ name - -# one bind as `name=value` -def show.bind(bb: Bind, +rest: String) -> String: - Bind{n, v} = bb - n ++ "=" ++ v ++ Bool.pick(String, String.is_empty(rest), "", " " ++ rest) - -# the bindings as `name=value` words -def show.binds(bs: List<&2, Bind>) -> String: - match bs: - case Nil{}: - "" - case Con{+h, t}: - show.bind(h, show.binds(t)) - -# each command's bindings, root first, `; ` between commands -def show.levels(mm: Matched) -> String: - match mm: - case Leaf{bs}: - show.binds(bs) - case Node{bs, _n, next}: - show.binds(bs) ++ "; " ++ show.levels(next) - -# a Matched as `path | binds` -def show.matched(+mm: Matched) -> String: - String.join(path_of(mm), "/") ++ " | " ++ show.levels(mm) - -# a parse result as a single line -def show(rr: Result<&2, &2, ParseErr, Matched>) -> String: - match rr: - case Fail{e}: - "err " ++ show.err(e) - case Done{m}: - "ok " ++ show.matched(m) - # the short/long label of an option, plus a metavar for Opt def help.label.kind(kk: ArgKind, +name: String, +label: String) -> String: match kk: diff --git a/src/eq.bend b/src/eq.bend index f34bf29..6336c1b 100644 --- a/src/eq.bend +++ b/src/eq.bend @@ -10,7 +10,7 @@ law bool_cmp_self: {Bool.cmp(bb, bb) == EQ{} : Cmp} # the two bits, each compared with itself -def bool_cmp_self(bb): +def bool_cmp_self(bb): # noqa: L001 a proof of this file's law match bb: case False{}: {==} @@ -24,7 +24,7 @@ law word_cmp_self: {Word.cmp(nn, ww, ww) == EQ{} : Cmp} # by induction on the width: a word of no bits and a bit carried over one -def word_cmp_self(nn, ww): +def word_cmp_self(nn, ww): # noqa: L001 a proof of this file's law match nn: case 0n: match ww: @@ -45,7 +45,7 @@ law u32_cmp_self: {U32.cmp(uu, uu) == EQ{} : Cmp} # a number is a word of thirty-two bits, so the word's law answers for it -def u32_cmp_self(uu): +def u32_cmp_self(uu): # noqa: L001 a proof of this file's law match uu: case U32{+ww}: word_cmp_self(32n, ww) @@ -56,7 +56,7 @@ law char_cmp_self: {Char.cmp(cc, cc) == ((cc, cc), EQ{}) : (Char & Char) & Cmp} # a char is a code point, and the pair it is compared inside rides along -def char_cmp_self(cc): +def char_cmp_self(cc): # noqa: L001 a proof of this file's law match cc: case Chr{+xx}: Equal.cong(Cmp, (Char & Char) & Cmp, rr => ((Chr{xx}, Chr{xx}), rr), @@ -69,7 +69,7 @@ law string_cmp_self: # by induction on the string: the head's law and the tail's, composed the # way String.cmp composes them -def string_cmp_self(ss): +def string_cmp_self(ss): # noqa: L001 a proof of this file's law match ss: case SNil{}: {==} @@ -91,6 +91,6 @@ law string_eq_self: {String.eq(ss, ss) == True{} : Bool} # equality is the comparison read as a bit, so the comparison's law answers -def string_eq_self(ss): +def string_eq_self(ss): # noqa: L001 a proof of this file's law Equal.cong((String & String) & Cmp, Bool, rr => String.eq.fin(rr), String.cmp(ss, ss), ((ss, ss), EQ{}), string_cmp_self(ss)) diff --git a/src/grow.bend b/src/grow.bend index e398679..e7827cd 100644 --- a/src/grow.bend +++ b/src/grow.bend @@ -11,7 +11,7 @@ import ./cli.bend as Shake import ./eq.bend as Eq # the bindings a walker holds for its current command -def binds_of(st: Shake.St) -> List<&2, Shake.Bind>: +def binds_of(st: Shake.St) -> List<&2, Shake.Bind>: # noqa: L001 proof machinery Shake.St{_m, _a, _g, _s, _p, bb, _o, _r, _n} = st bb # `big` is `small` with some bindings put in front @@ -566,7 +566,7 @@ def gw.Stuck(big: Shake.St) -> Type: {gw.live(big) == False{} : Bool} # the three things a word does to a walker -type Moved<-A: Type, -B: Type, -C: Type> is Type: +type Moved<-A: Type, -B: Type, -C: Type> is Type: # noqa: L001 proof machinery: what a step did, for the walker proofs Stays{proof: A} Enters{proof: B} Stops{proof: C} @@ -1159,7 +1159,7 @@ def gw.stuck_walk(more, st, hh): gw.stuck_walk(tt, Shake.parse.step(ww, st), gw.stuck_step(ww, st, hh)) # a walk either grows the walker or leaves it stuck -type Went<-A: Type, -B: Type> is Type: +type Went<-A: Type, -B: Type> is Type: # noqa: L001 proof machinery: what a walk did, for the walker proofs Grew{proof: A} Stopped{proof: B}