diff --git a/README.md b/README.md index 861a026..ca48ff3 100644 --- a/README.md +++ b/README.md @@ -76,14 +76,17 @@ list, and `get` still reads one value. `argv` is the process's arguments, each word reusable. A compiled Bend program's runtime reads the command line before shake does -(bend 2.0.27): +(bend 2.0.34): -- `--help` prints the runtime's own usage and exits, and `--gpu-build` - builds the GPU image and exits; neither runs `main`. +- `--bend-help` prints the runtime's own usage and exits, and `--gpu-build` + builds the GPU image and exits; neither runs `main`. `--help` is an + ordinary argument. - `--threads N` and `--gpu X` are taken, with their value, and a bad value stops the program. - The first `--` is taken too, and every word after it is passed on unexamined. +- The first word `IO.args` answers is the program name. `argv` drops it + and returns the words after it. So a `--` ends shake's option parsing (every later word is a positional) only when it is the second one: `tool add -- -- -5 3` binds `-5` and `3`. diff --git a/SPEC.md b/SPEC.md index 289c612..f5a8aa5 100644 --- a/SPEC.md +++ b/SPEC.md @@ -2,11 +2,11 @@ This is the list of every behavior shake guarantees, each under a stable requirement ID. Every requirement is about the interface in `main.bend`: its types, builders, `parse`, `check`, the readers, `help`, `err_text`, `help_path`, `err_path` and `argv`. Every module under `src/` is internal and carries no promise. -Every requirement has one of two levels. A **Proved** requirement holds for every input, and is backed by a quantified law (a `for` or `exs` binder) in `src/LAWS.bend` that passes the proof gate. A **Trusted** requirement is an assumption shake cannot check from inside its own gate, and it is listed in the trust boundary below. A Proved requirement whose laws have not all landed has status **pending**: we intend to prove it, and until then it is not guaranteed. The proof gate is this check: the first line `bend src/PROOF.bend` prints is exactly `All terms check.` (`ez prove`). Tests and fixtures are never evidence for a requirement. +Every requirement has one of two levels. A **Proved** requirement holds for every input, and is backed by a quantified law (a `for` or `exs` binder) in `src/LAWS.bend` that passes the proof gate. A **Trusted** requirement is an assumption shake cannot check from inside its own gate, and it is listed in the trust boundary below. A Proved requirement whose laws have not all landed has status **pending**: we intend to prove it, and until then it is not guaranteed. The proof gate is this check: the first line `bend src/PROOF.bend` prints is exactly `ALL PROOFS CHECK`. Tests and fixtures are never evidence for a requirement. A spec is **well-formed** when `check` reports nothing for it (SHAKE-SPEC-1). The parse requirements hold for well-formed specs; a spec that contradicts itself, such as two options spelled `-n`, is its author's bug and not an input a user can give. Every error a row names but `NeedHelp` also carries `at`, the command path selected where the parse failed (SHAKE-ERR-2); rows write it only where it matters. A **plain word** is `-`, or a word that does not start with `-`. The **current command** is the command whose arguments `parse` matches words against: the root, then each subcommand it selects. The **selected path** is the names of the subcommands selected, in order. A successful parse answers the root command's **Matched**, as clap answers `ArgMatches`: the bindings that command made while it was current and, when a subcommand was selected under it, that subcommand's name and its own Matched, and so on down the selected path. -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 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) and after `argv` has dropped the program name (SHAKE-TRUST-4). 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. @@ -84,7 +84,7 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n | ID | Requirement | Level | Status | Law | | :---- | :---- | :---- | :---- | :---- | -| SHAKE-ARGS-1 | The copy `argv` makes of the words `IO.args` gives keeps all of them, in order and unchanged: for every list, reading the copy back gives the list. | Proved | proved | src/LAWS.bend copy_keeps | +| SHAKE-ARGS-1 | The copy `argv` makes keeps every word it is given, in order and unchanged: for every list, reading the copy back gives the list. | Proved | proved | src/LAWS.bend copy_keeps | ## Left to prove @@ -96,7 +96,7 @@ These assumptions sit outside the proofs. They are the complete list of Trusted | ID | Assumption | Why it is trusted | | :---- | :---- | :---- | -| SHAKE-TRUST-1 | The Bend checker is sound: a proof it accepts proves its law. | It cannot be checked from inside Bend; this is EZ-TRUST-1. shake pins bend 2.0.27 through the flake. | -| SHAKE-TRUST-2 | A program compiled by bend 2.0.27 hands `IO.args` the process's words after the program name, except that it stops examining words at the first `--`, drops that `--` and passes every later word through unchanged; before that `--` it removes `--threads` and `--gpu` with the word after each, and ends the process before `main` on `--help` and on `--gpu-build`. | It is the C `main` bend emits, read from bend 2.0.26's own source (in its binary) and confirmed against the demo; rechecked for 2.0.27, whose `main` is identical. It changes when bend does, so every bend bump rechecks it. | -| SHAKE-TRUST-3 | The proof-gate runner fails the build unless the first line of `bend src/PROOF.bend` is `All terms check.` | It is ez's `mkProofs` running `ez prove`, run by `nix flake check` in CI; this is EZ-TRUST-4. | -| SHAKE-TRUST-4 | `argv` hands on exactly the list `IO.args` answers, through the copy SHAKE-ARGS-1 is about. | It is IO, which no law can reach: `argv` in `src/args.bend` is one `IO.bind` of `IO.args` into `copy`, short enough to check by reading, and marked `# noqa: L001` for that reason. | +| SHAKE-TRUST-1 | The Bend checker is sound: a proof it accepts proves its law. | It cannot be checked from inside Bend; this is EZ-TRUST-1. shake pins bend 2.0.34 through the flake. | +| SHAKE-TRUST-2 | A program compiled by bend 2.0.34 hands `IO.args` the program name and then the process's words, except that it stops examining words at the first `--`, drops that `--` and passes every later word through unchanged; before that `--` it removes `--threads` and `--gpu` with the word after each, and ends the process before `main` on `--bend-help` and on `--gpu-build`. | It is the C `main` bend emits, read from bend 2.0.34's own source and confirmed against the demo. It changes when bend does, so every bend bump rechecks it. | +| SHAKE-TRUST-3 | The proof-gate runner fails the build unless the first line of `bend src/PROOF.bend` is `ALL PROOFS CHECK`. | It is the flake's proofs check, run by `nix flake check` in CI. | +| SHAKE-TRUST-4 | `argv` drops the first word `IO.args` answers (the program name) and hands on the rest through the copy SHAKE-ARGS-1 is about. When `IO.args` answers nothing, so does `argv`. | It is IO, which no law can reach: `argv` in `src/args.bend` binds `IO.args` into `copy` after `after` drops that first word, short enough to check by reading, and both are marked `# noqa: L001` for that reason. | diff --git a/flake.lock b/flake.lock index 55e5bef..7487737 100644 --- a/flake.lock +++ b/flake.lock @@ -7,16 +7,17 @@ ] }, "locked": { - "lastModified": 1790348040, - "narHash": "sha256-6oh+6jj7kyl4xJsmq4p3BtU/BUl2f2LlC/5kH081D1M=", + "lastModified": 1790643370, + "narHash": "sha256-VYGPIHkNeccEaBHGer1B7+GNiWKQBiN/iiS7PozBXx0=", "owner": "bendlang", "repo": "bend", - "rev": "774ef644dccf9c3f8053f7276d8901ad23da006c", + "rev": "777ee0b55c485afdd7e68bd917b3d23a88d77371", "type": "github" }, "original": { "owner": "bendlang", "repo": "bend", + "rev": "777ee0b55c485afdd7e68bd917b3d23a88d77371", "type": "github" } }, @@ -30,11 +31,11 @@ ] }, "locked": { - "lastModified": 1790364897, - "narHash": "sha256-WBj/Hg/Gys7sIz/IYt204QEGQPjQ/qw0TpcXAYpuGQI=", + "lastModified": 1790514265, + "narHash": "sha256-NrMlq4aruqBVCNsy9TZtcMayDn3HEhb1I8AyiE233Kw=", "owner": "Emerging-Patterns", "repo": "ez", - "rev": "94d441e9b58e8b6a8a2f6cb8a74ae35d13b47ceb", + "rev": "f37f6d20dc144cd74bb0cd51f9ec4e6925826548", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index 3223dbe..759c417 100644 --- a/flake.nix +++ b/flake.nix @@ -3,7 +3,7 @@ inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable"; inputs.bend = { - url = "github:bendlang/bend"; + url = "github:bendlang/bend/777ee0b55c485afdd7e68bd917b3d23a88d77371"; inputs.nixpkgs.follows = "nixpkgs"; }; inputs.ez = { @@ -15,6 +15,7 @@ outputs = { self, nixpkgs, ... }@inputs: let system = "x86_64-linux"; + pkgs = nixpkgs.legacyPackages.${system}; ez = inputs.ez.lib.${system}; ezBin = inputs.ez.packages.${system}.default; bend = inputs.bend.packages.${system}.default; @@ -29,12 +30,22 @@ in { packages.${system} = { inherit bend demo bend-cc; ez = ezBin; default = demo; }; apps.${system}.default = { type = "app"; program = "${demo}/bin/demo"; }; - # `proofs` is `ez prove`: every PROOF.bend must print exactly - # `All terms check.` first. `lint` is bolt at the lock's `[tools.bolt]` + # `proofs` is `bend src/PROOF.bend`: its first line must be + # `ALL PROOFS CHECK`. `lint` is bolt at the lock's `[tools.bolt]` # pin, graded by ./bolt.bend. checks.${system} = { inherit demo; - proofs = ez.mkProofs { ez = ezBin; src = self; name = "shake-proofs"; }; + proofs = pkgs.runCommand "shake-proofs" { + nativeBuildInputs = [ bend ]; + BEND_LIB = ez.bendLib ./ez.lock.toml; + } '' + export HOME=$TMPDIR + cp -r ${self} src && chmod -R u+w src && cd src + first=$(cd src && bend PROOF.bend | head -n 1) + echo "src/PROOF.bend: $first" + [ "$first" = "ALL PROOFS CHECK" ] || exit 1 + touch $out + ''; lint = ez.mkLint { src = self; }; }; # bolt, from the lock, is on PATH through `src` diff --git a/main.bend b/main.bend index 40fe17a..d5da2c4 100644 --- a/main.bend +++ b/main.bend @@ -206,8 +206,9 @@ def help_path(err: S.ParseErr) -> Maybe<&2, List<&2, String>>: None{} # the process's arguments, each word reusable. A compiled program's runtime -# has already acted on `--help`, `--gpu-build`, `--threads N` and `--gpu X` -# and taken the first `--`, passing every word after it here unexamined; so -# the `--` that `parse` sees is the user's second one +# has already acted on `--bend-help`, `--gpu-build`, `--threads N` and +# `--gpu X` and taken the first `--`, passing every word after it here +# unexamined; so the `--` that `parse` sees is the user's second one. +# `IO.args` starts with the program name, and `argv` drops it def argv() -> IO(List<&2, String>): # noqa: L001 IO: reads argv Args.argv() diff --git a/src/LAWS.bend b/src/LAWS.bend index a7a70df..c656ef8 100644 --- a/src/LAWS.bend +++ b/src/LAWS.bend @@ -244,7 +244,7 @@ law at_cons: for +rest: List<&2, String> {Shake.at(found, name <> rest) == at.via(Shake.sub_of(found, name), rest) : Maybe<&2, Shake.Matched>} -# LAW: `copy` keeps every word IO.args gives, all of them, in order and +# LAW: `copy` keeps every word it is given, all of them, in order and # unchanged: read back, the copy is the list it was made from # SHAKE-ARGS-1 law copy_keeps: diff --git a/src/args.bend b/src/args.bend index 879684f..7a4e80d 100644 --- a/src/args.bend +++ b/src/args.bend @@ -1,6 +1,7 @@ # shake/args: the process argv, each word reusable, internal (main.bend -# exports it). `IO.args` answers a `&1` list; the rest of a program reads the -# line more than once, so the walk copies it. +# exports it). `IO.args` answers a `&1` list whose first word is the program, +# as C's argv; the rest of a program reads the line more than once, so the +# walk copies the words after that name. import Base # a &1 list copied to &2 @@ -11,7 +12,16 @@ def copy(xs: List<&1, String>) -> List<&2, String>: case Con{+h, t}: h <> copy(t) +# the words after the program, which `IO.args` gives first; none when it +# gave none +def after(xs: List<&1, String>) -> List<&1, String>: # noqa: L001 the program name (SHAKE-TRUST-4) + match xs: + case Nil{}: + Nil{} + case Con{_h, t}: + t + # the process argv def argv() -> IO(List<&2, String>): # noqa: L001 IO: reads argv (SHAKE-TRUST-4) IO.bind(List<&1, String>, List<&2, String>, IO.args(), - xs => IO.pure(List<&2, String>, copy(xs))) + xs => IO.pure(List<&2, String>, copy(after(xs)))) diff --git a/src/eq.bend b/src/eq.bend index 6336c1b..02b64c1 100644 --- a/src/eq.bend +++ b/src/eq.bend @@ -90,7 +90,11 @@ law string_eq_self: for +ss: String {String.eq(ss, ss) == True{} : Bool} +# a string comparison read as a bit: what `String.eq` reads off `String.cmp` +def eq.of(rr: (String & String) & Cmp) -> Bool: # noqa: L001 a proof of this file's law + Cmp.is_eq(Pair.snd(String & String, Cmp, rr)) + # equality is the comparison read as a bit, so the comparison's law answers 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), + Equal.cong((String & String) & Cmp, Bool, rr => eq.of(rr), String.cmp(ss, ss), ((ss, ss), EQ{}), string_cmp_self(ss))