From 438760cc6f99d4a56509b90a6e59dcea33f468db Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 29 Sep 2026 23:53:33 +0000 Subject: [PATCH] chore: bump Bend to 2.0.34 Lock inputs.bend to 777ee0b, the rev whose flake names 2.0.34, and inputs.ez to current master, still following bend. argv drops the program name IO.args gives first. The runtime's help flag is --bend-help. The proof gate reads ALL PROOFS CHECK. Co-authored-by: noah-emp --- README.md | 9 ++++++--- SPEC.md | 14 +++++++------- flake.lock | 13 +++++++------ flake.nix | 19 +++++++++++++++---- main.bend | 7 ++++--- src/LAWS.bend | 2 +- src/args.bend | 16 +++++++++++++--- src/eq.bend | 6 +++++- 8 files changed, 58 insertions(+), 28 deletions(-) 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))