chore(deps): use noah-emp/bend-sha256 and bump bend

.github/workflows/ci.yml

@@ -18,8 +18,8 @@ jobs:
   readme:
     runs-on: ubuntu-latest
     env:
-      BEND_VERSION: 2.0.27
-      BEND_SHA256: 58adc86af6605ed0c48f7d84e4c23028f78893ce4a867a20a4f004b11582687b
+      BEND_VERSION: 2.0.31
+      BEND_SHA256: f7dbecc8ef5991fe15d9953b8b33911bc62a120c735e2e5902aa031e22055bad
     steps:
       - uses: actions/checkout@fbc6f3992d24b796d5a048ff273f7fcc4a7b6c09 # v5.1.0
       - name: Install bend
@@ -32,5 +32,5 @@ jobs:
           echo "$RUNNER_TEMP/bend/bin" >> "$GITHUB_PATH"
       - run: sh bootstrap.sh
       - run: mkdir -p bin
-      - run: BEND_LIB=$PWD/.ez/lib bend ez/main.bend -o bin/ez.bin
+      - run: BEND_LIB=$PWD/.ez/lib bend ez.bend -o bin/ez.bin
       - run: bin/ez.bin prove

AGENTS.md

@@ -11,7 +11,7 @@ ez is a project manager for Bend 2, written in Bend. Each command is a pure plan
 ```bash
 sh bootstrap.sh
 mkdir -p bin
-BEND_LIB=$PWD/.ez/lib bend ez/main.bend -o bin/ez.bin
+BEND_LIB=$PWD/.ez/lib bend ez.bend -o bin/ez.bin
 bin/ez.bin prove                     # the proof gate: every PROOF.bend must pass
 bin/ez.bin tool run bolt -- --gpu off   # lint: 0 errors
 bin/ez.bin lock                      # must leave ez.lock.toml unchanged unless you meant to change it

README.md

@@ -18,10 +18,10 @@ git clone https://github.com/Emerging-Patterns/ez
 cd ez
 sh bootstrap.sh
 mkdir -p bin
-BEND_LIB=$PWD/.ez/lib bend ez/main.bend -o bin/ez.bin
+BEND_LIB=$PWD/.ez/lib bend ez.bend -o bin/ez.bin
 ```
 
-ez runs on Bend 2.0.27, the version CI builds with. Its dependencies are
+ez runs on Bend 2.0.31, the version CI builds with. Its dependencies are
 pinned to git revs, and `ez fetch` is what fetches them, which ez cannot run
 before it is built. `bootstrap.sh` is that one step, and the one helper script
 in the repo: it reads `ez.lock.toml`, fetches each package at its pinned rev

SPEC.md

@@ -1,6 +1,6 @@
 # ez specification
 
-This is the list of every behavior ez guarantees, each under a stable requirement ID. Every requirement has one of two levels. A **Proved** requirement holds for every input, and is backed by a quantified law in a LAWS.bend that passes the proof gate. A **Trusted** requirement is an assumption about something ez cannot check from inside its own gate, and it is listed in the trust boundary below. A Proved requirement whose law has not landed yet has status **pending**: we intend to prove it, and until then it is not guaranteed. The proof gate is this check: for every PROOF.bend in the tree, the first line `bend PROOF.bend` prints is exactly `All terms check.` `ez prove` runs it, and it is the check CI runs.
+This is the list of every behavior ez guarantees, each under a stable requirement ID. Every requirement has one of two levels. A **Proved** requirement holds for every input, and is backed by a quantified law in a LAWS.bend that passes the proof gate. A **Trusted** requirement is an assumption about something ez cannot check from inside its own gate, and it is listed in the trust boundary below. A Proved requirement whose law has not landed yet has status **pending**: we intend to prove it, and until then it is not guaranteed. The proof gate is this check: for every PROOF.bend in the tree, bend is started from a file above the tree that imports it, and the first line bend prints is exactly `All terms check.` Bend 2.0.28 names each file from the program that starts it, so that start is what gives each file one name. `ez prove` runs it, and it is the check CI runs.
 
 The reasoning behind each requirement, and the decisions that shaped them, are in [docs/rfc/ez-spec.md](docs/rfc/ez-spec.md).
 
@@ -151,9 +151,9 @@ EZ-DOC-3 reads the committed tree as bend reads it. A hub import line is a root
 
 EZ-VEN-1 is proved for `ez add`, `ez remove` and `ez lock --upgrade`. Over the line-level function `I.lines` (ledger/ignore.bend), its allowlist lines are exactly the vendored hashes, each once, in the order the ledger first names them, and every other line is kept in order; the file `I.sync` writes reads back (`I.file.lines`) as those lines, whatever the file it read ended with, and applying it twice is applying it once; each for a ledger whose vendored hashes hold no newline. `ez remove` and `ez add` leave `.gitignore` holding exactly `I.sync`'s text over the ledger they leave (`remove_syncs_allowlist`, `add_syncs_allowlist`). `ez lock --upgrade`: every `.gitignore` its plan writes has the allowlist of the hashes the upgrade commits and keeps every other line of the file it read, when no source it read is at `.gitignore`; an upgrade that does not refuse and leaves `.gitignore` unwritten read one whose allowlist is already those hashes (`upgrade_allowlist_kept_in_sync`); and the hashes it commits are the vendored hashes of the model it renders when it writes ez.toml (`upgrade_vends_the_ledger`) and of ez.toml as it is when it does not (`upgrade_unmoved_vends_the_ledger`). `ez add`'s half and the upgrade's hold of ez.toml's bytes, since the ledger they leave reads back as the model they render (EZ-LED-4).
 
-EZ-DOC-1 is trusted, not proved: the lock is written as eztoml's `render` of the document ez assembles (`T.normal`, `toml/toml.bend`) and read through eztoml's `parse`, so it reads back when eztoml's round trip holds, which is EZ-TRUST-8, pending in eztoml v0.4.0. ez still writes no lock that `lockable.named` refuses: `lockable` refuses a hash, key or value holding `"`, `\` or a newline, a hash written twice, and a file path holding `=`. eztoml v0.4.0 escapes strings and reads a quoted key whole, so these refusals are no longer needed for eztoml; they are kept for `bootstrap.sh`, whose awk cuts a pair at its first `=` and reads no escape. What the lock records is the packages in hash order with each one's files in path order and each once, each tool pin without `vendor`, and the names in name order and each once. Until ez moved to eztoml 0.4 this row was proved against the v0.1.0 reader (`lock_reads_back` and its tools, names and hub laws); the maintainer chose to move ahead of eztoml's proofs, and those laws went with the reader they unfolded.
+EZ-DOC-1 is trusted, not proved: the lock is written as eztoml's `render` of the document ez assembles (`T.normal`, `toml/toml.bend`) and read through eztoml's `parse`, so it reads back when eztoml's round trip holds, which is EZ-TRUST-8, proved in eztoml v0.5.0 and not re-checked here. ez still writes no lock that `lockable.named` refuses: `lockable` refuses a hash, key or value holding `"`, `\` or a newline, a hash written twice, and a file path holding `=`. eztoml v0.4.0 escapes strings and reads a quoted key whole, so these refusals are no longer needed for eztoml; they are kept for `bootstrap.sh`, whose awk cuts a pair at its first `=` and reads no escape. What the lock records is the packages in hash order with each one's files in path order and each once, each tool pin without `vendor`, and the names in name order and each once. Until ez moved to eztoml 0.4 this row was proved against the v0.1.0 reader (`lock_reads_back` and its tools, names and hub laws); the maintainer chose to move ahead of eztoml's proofs, and those laws went with the reader they unfolded.
 
-EZ-LED-4 is proved relative to EZ-TRUST-8. `ledger/LAWS.bend` states the read-back as a premise, `ReadsBack`: every ledger `Rend.renderable` accepts reads back, from the text `Rend.show` writes, as itself. `Rend.show` is eztoml's `render` of the document ez assembles (`Rend.text`) and `M.parse` reads through eztoml's `parse`, so the premise is eztoml's round trip, pending in eztoml v0.4.0, and ez does not prove it. What ez proves is the rest: every command that writes ez.toml refuses a ledger that is not renderable, with no effect (EZ-OUT-2), and writes one that reads back, given the premise, as the model its laws are stated over: `ez init` the package and entry it was given (`init_ledger_reads_back`), `ez add` the ledger with the dependency added (`add_ledger_reads_back`, `add_named_reads_back`), and `ez remove` the ledger with it dropped (`remove_ledger_reads_back`). `renderable` refuses a name or value holding `"`, `\` or a newline, a dependency with no hash, and a git source that names no repo or no root. A ledger written before ez used eztoml 0.4 reads to the same model: `toml/toml.bend` passes over the tables a dotted header implies, and `tests/toml.bend` reads an old ledger and lock and their new forms to the same sections.
+EZ-LED-4 is proved relative to EZ-TRUST-8. `ledger/LAWS.bend` states the read-back as a premise, `ReadsBack`: every ledger `Rend.renderable` accepts reads back, from the text `Rend.show` writes, as itself. `Rend.show` is eztoml's `render` of the document ez assembles (`Rend.text`) and `M.parse` reads through eztoml's `parse`, so the premise is eztoml's round trip, proved in eztoml v0.5.0, and ez does not prove it. What ez proves is the rest: every command that writes ez.toml refuses a ledger that is not renderable, with no effect (EZ-OUT-2), and writes one that reads back, given the premise, as the model its laws are stated over: `ez init` the package and entry it was given (`init_ledger_reads_back`), `ez add` the ledger with the dependency added (`add_ledger_reads_back`, `add_named_reads_back`), and `ez remove` the ledger with it dropped (`remove_ledger_reads_back`). `renderable` refuses a name or value holding `"`, `\` or a newline, a dependency with no hash, and a git source that names no repo or no root. A ledger written before ez used eztoml 0.4 reads to the same model: `toml/toml.bend` passes over the tables a dotted header implies, and `tests/toml.bend` reads an old ledger and lock and their new forms to the same sections.
 
 The upgrade laws of phase three, for EZ-RES-4, EZ-RES-5, EZ-RES-6, EZ-RES-8 and the `ez lock --upgrade` half of EZ-VEN-1, are stated over the ledger model the upgrade renders into ez.toml, and hold of the file's bytes because those bytes read back as that model (EZ-LED-4). The design is in [docs/rfc/ez-lock-planner.md](docs/rfc/ez-lock-planner.md). EZ-RES-4 and EZ-RES-6 are proved so: their laws (`lock/LAWS.bend`) are over `P.ledger.next`, the model an upgrade renders, and over `P.wants.up`, the questions it asks, and what they say of ez.toml's bytes, and of the lock made from those bytes read back, holds by EZ-LED-4. EZ-RES-6's `NAME` is a nonempty `--package`; an empty one is no filter, as `ez lock --upgrade` alone.
 
@@ -194,15 +194,15 @@ These assumptions sit outside the proofs. They are the complete list of Trusted
 | EZ-TRUST-1 | The Bend checker is sound. | We cannot check it from inside Bend. The BendTT paper and a Lean formalization exist, and the release notes report mismatches between the formalization and the implementation. |
 | EZ-TRUST-2 | The interpreter reads the World and executes plans faithfully. | It makes no decisions and is kept small enough to review line by line. |
 | EZ-TRUST-3 | The hub serves, for a hash, what was published under it. | ez checks every hub body against the hash it asked for (EZ-FETCH-1), so this reduces to availability and EZ-HASH-6. |
-| EZ-TRUST-4 | `ez prove` runs `bend` on every PROOF.bend in the tree and passes only on an exact `All terms check.` first line. | It is ez code run by `mkProofs`, not a law. CI builds from a clean tree, so nothing is cached. |
-| EZ-TRUST-5 | HTTP framing and URL parsing are correct. | Proved in ezhttp v0.5.0, the rev ez.toml pins; ez's gate does not re-check it. |
+| EZ-TRUST-4 | `ez prove` runs `bend` on a file above the tree that imports every PROOF.bend, and passes only on an exact `All terms check.` first line. | It is ez code run by `mkProofs`, not a law. CI builds from a clean tree, so nothing is cached. Bend 2.0.28 names a file from the program that starts it, so the start is above the tree. |
+| EZ-TRUST-5 | HTTP framing and URL parsing are correct. | Proved in ezhttp v0.6.0, the rev ez.toml pins; ez's gate does not re-check it. |
 | EZ-TRUST-6 | A `<name>@<version>` the hub answered once names the same hash forever. | The hub never moves a name once it is taken, so a name is resolved once and pinned in the lock. The package it names is still checked against its hash (EZ-FETCH-1). |
 | EZ-TRUST-7 | Command-line parsing is correct: `parse` binds a line as shake's spec says, `help_path` names a request for help and only one, `path_of` and `at` follow the selected path, and `get`, `on` and `help` read and render it. | Proved in shake v0.2.0, the rev ez.toml pins (SHAKE-PARSE-1 to SHAKE-PARSE-10, SHAKE-GET-1, SHAKE-GET-2, SHAKE-HELP-1, SHAKE-ERR-1, SHAKE-ERR-2); ez imports only its interface, `main.bend`, and its gate does not re-check it. In particular `ez help <path>` with a word that names no command there fails as `Unexpected`, not as a request for help (SHAKE-PARSE-8). |
-| EZ-TRUST-8 | A document eztoml v0.4.0 renders reads back as itself, and a text it reads without error renders back as the same document: its TOML-RT-1, TOML-RT-2 and TOML-RT-3. | Pending in eztoml v0.4.0, the rev ez.toml pins, which states them and has not proved them yet. ez relies on them for EZ-DOC-1 and EZ-LED-4; the maintainer chose to move to eztoml 0.4 ahead of the proofs. Revisit when eztoml proves them. ez's step between its sections and eztoml's document (`toml/toml.bend`) is ez code with no law: `tests/toml.bend` checks it on an old and a new ledger and lock. |
+| EZ-TRUST-8 | A document eztoml v0.5.0 renders reads back as itself, and a text it reads without error renders back as the same document: its TOML-RT-1, TOML-RT-2 and TOML-RT-3. | Proved in eztoml v0.5.0, the rev ez.toml pins; ez's gate does not re-check it. ez relies on it for EZ-DOC-1 and EZ-LED-4. ez's step between its sections and eztoml's document (`toml/toml.bend`) is ez code with no law: `tests/toml.bend` checks it on an old and a new ledger and lock. |
 | EZ-DOC-1 | Parsing a rendered lock yields the packages, hub, names and tools that were rendered. | It is EZ-TRUST-8 for the document ez assembles for the lock. |
 | EZ-RES-7 | git reports refs, tags, and ancestry accurately. | The World model takes git's answers as given. |
 | EZ-HASH-4 | ez's 0x hash matches `bend --publish`. | The publisher is a separate program. |
 | EZ-HASH-5 | ez's narHash matches nix. | nix is a separate program. What ez trusts of its own walk is GNU `find`'s listing of the tree, each path's type, `%M` mode, name and link target, and the file effect's read of each file's bytes. The walk takes the executable bit from the owner's exec bit of that mode, as nix's dumper does, and reads names and targets as listed (EZ-HASH-7). Submodules are not part of the tree: ez weighs a checkout without them, and its nix side asks `fetchgit` for the same. |
-| EZ-HASH-6 | `Sha.raw` computes the SHA-256 digest of its bytes, and `Sha.hex` of its text's UTF-8. | Proved in Giulio2002/bend-sha256 against an executable FIPS 180-4 specification, at the hash ez vendors; ez's gate does not re-check it. Collision resistance is also assumed. |
+| EZ-HASH-6 | `Sha.raw` computes the SHA-256 digest of its bytes, and `Sha.hex` of its text's UTF-8. | Proved in noah-emp/bend-sha256 against an executable FIPS 180-4 specification, at the hash ez vendors; ez's gate does not re-check it. The git pin is temporary. Collision resistance is also assumed. |
 
 EZ-VEN-2 and EZ-VEN-3 are proved for the moves an upgrade makes (`ledger/LAWS.bend` `moves.ok`): each old hash names something, no hash holds `/` or a newline, as a `0x` name never does, and no move's new hash is the old hash of a move after it. That last is the premise the spec's notes call for: swaps apply one after another, so a new hash that is a later move's old one would be moved again. The text laws are over `U.reimport.many`, and the plan laws carry them to what `ez lock --upgrade` leaves at a `.bend` source it read and the World names once (`found`, with `pre` and `post` around it), when the lock does not refuse; that the sources the upgrade reads are the `.bend` files outside `.ez` and `.git` is the interpreter's (EZ-TRUST-2). A line names a hash when it starts `import <hash>/` at column 0; the new hash a line names is the one the first move of its old hash sends it to.