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

README.md

@@ -21,7 +21,7 @@ mkdir -p bin
 BEND_LIB=$PWD/.ez/lib bend ez/main.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

add/PROOF.bend

@@ -25,7 +25,7 @@ import ../pkg/path.bend as Path
 import ../git/git.bend as Git
 import ../ez/target.bend as Tgt
 import ../ez/named.bend as Named
-import ../sha/sha.bend as Sha
+import ../share/sha.bend as Sha
 import ../check/eq.bend as Eq
 import ../check/str.bend as Str
 import ../pkg/PROOF.bend as Pk
@@ -309,7 +309,7 @@ def wf(k: K.Walked) -> List<&2, K.Source>:
     case K.Refused{_why}:
       []
 
-def ws(k: K.Walked) -> List<&2, K.File>:
+def ws(k: K.Walked) -> List<&2, K.Item>:
   match k:
     case K.Walked{_h, _r, _fs, ss}:
       ss
@@ -438,7 +438,7 @@ law edits_of:
   for +h: String
   for +a: String
   for fs: List<&2, K.Source>
-  for ss: List<&2, K.File>
+  for ss: List<&2, K.Item>
   for +m: M.Manifest
   for +w: A.World
   {P.put.in(AP.effects.of(d, h, a, fs, ss, m, w), "ez.toml")
@@ -522,7 +522,7 @@ law syncs_of:
   for +h: String
   for +a: String
   for fs: List<&2, K.Source>
-  for ss: List<&2, K.File>
+  for ss: List<&2, K.Item>
   for +m: M.Manifest
   for +w: A.World
   {AP.after(P.put.in(AP.effects.of(d, h, a, fs, ss, m, w), ".gitignore"), A.ignore(w))
@@ -602,7 +602,7 @@ law says_of:
   for +h: String
   for +a: String
   for fs: List<&2, K.Source>
-  for ss: List<&2, K.File>
+  for ss: List<&2, K.Item>
   for +m: M.Manifest
   for +w: A.World
   {AP.last.go(P.said.in(AP.effects.of(d, h, a, fs, ss, m, w)), "") == Git.import.line(h, a)
@@ -894,7 +894,7 @@ law fixed_judge:
 def fixed_judge(ok, _bad, root, pre, out):
   match ok:
     case True{}:
-      %Equal.sym(List<&2, K.File>, K.placed(pre, K.hit.sums(out)),
+      %Equal.sym(List<&2, K.Item>, K.placed(pre, K.hit.sums(out)),
         K.laid.sums(K.laid(pre, out)), Pk.placed_is_laid(pre, out))
         : {K.Walked{K.hash_of(K.files_of(K.laid.sums(K.laid(pre, out)))), root, K.laid(pre, out),
           K.files_of(K.laid.sums(K.laid(pre, out)))}
@@ -1048,19 +1048,19 @@ def last_snoc(xs, at, text):
 # LAW: the found files as laid, weighed, are the walk's laid files weighed
 law weigh_srcs:
   for fs: List<&2, K.Source>
-  {W.weighs(AP.srcs(fs)) == K.laid.sums(fs) : List<&2, K.File>}
+  {W.weighs(AP.srcs(fs)) == K.laid.sums(fs) : List<&2, K.Item>}
 
 def weigh_srcs(fs):
   match fs:
     case []:
       {==}
     case K.Source{at, text} <> t:
-      Equal.cong(List<&2, K.File>, List<&2, K.File>, ys => K.File{at, Sha.hex(text)} <> ys,
+      Equal.cong(List<&2, K.Item>, List<&2, K.Item>, ys => K.Item{at, Sha.hex(text)} <> ys,
         W.weighs(AP.srcs(t)), K.laid.sums(t), weigh_srcs(t))
 
 # a package's file list, weighed from its texts, and the files a `Lay`
 # writes for it
-def lsum(fs: List<&2, K.Source>) -> List<&2, K.File>:
+def lsum(fs: List<&2, K.Source>) -> List<&2, K.Item>:
   K.files_of(K.laid.sums(fs))
 
 def lh(fs: List<&2, K.Source>) -> String:
@@ -1081,7 +1081,7 @@ def lay_canon(fs):
     : {Bool.and(String.eq(lh(fs), K.hash_of(K.files_of(W.weighs(_)))),
       String.eq(P.last(lay.files(fs)), K.manifest_of(K.files_of(W.weighs(_))))) == True{}
       : Bool}
-  %Equal.sym(List<&2, K.File>, W.weighs(AP.srcs(fs)), K.laid.sums(fs), weigh_srcs(fs))
+  %Equal.sym(List<&2, K.Item>, W.weighs(AP.srcs(fs)), K.laid.sums(fs), weigh_srcs(fs))
     : {Bool.and(String.eq(lh(fs), K.hash_of(K.files_of(_))),
       String.eq(P.last(lay.files(fs)), K.manifest_of(K.files_of(_)))) == True{} : Bool}
   %Equal.sym(String, P.last(lay.files(fs)), K.manifest_of(lsum(fs)),
@@ -1451,7 +1451,7 @@ law entry_fit:
   for +h: String
   for +r: String
   for fs: List<&2, K.Source>
-  for ss: List<&2, K.File>
+  for ss: List<&2, K.Item>
   for +w: A.World
   for s: {win(AP.outcome.entry(g, K.Walked{h, r, fs, ss}, w)) == True{} : Bool}
   {Rend.renderable(Rend.add.keep(A.manifest.of(A.read(w)), AP.dep.of(h, r, w))) == True{} : Bool}
@@ -2282,7 +2282,7 @@ def lnv(+hash: String, v: W.Verdict) -> Bool:
 law lnv.laid:
   for ok: Bool
   for +hash: String
-  for +fs: List<&2, K.File>
+  for +fs: List<&2, K.Item>
   for +ss: List<&2, String>
   for e: {String.eq(hash, W.named(W.laid(fs, ss))) == ok : Bool}
   {lnv(hash, W.body.laid(ok, hash, fs, ss)) == True{} : Bool}
@@ -2297,7 +2297,7 @@ def lnv.laid(ok, _hash, _fs, _ss, e):
 law lnv.sums:
   for ok: Bool
   for +hash: String
-  for +fs: List<&2, K.File>
+  for +fs: List<&2, K.Item>
   for +ss: List<&2, String>
   {lnv(hash, W.body.sums(ok, hash, fs, ss)) == True{} : Bool}
 
@@ -2312,7 +2312,7 @@ law lnv.escape:
   for clean: Bool
   for +bad: String
   for +hash: String
-  for +fs: List<&2, K.File>
+  for +fs: List<&2, K.Item>
   for +ss: List<&2, String>
   {lnv(hash, W.body.escape.go(clean, bad, hash, fs, ss)) == True{} : Bool}
 

add/hub.bend

@@ -83,7 +83,7 @@ def heard(rs: List<&2, W.Reply>, +key: String) -> Maybe<&2, W.Answer>:
 # every answer is in, with the hash the hub named and the package it serves
 # checked against it; a question is still open; or the add refuses
 type Verdict is Data:
-  Go{hash: String, files: List<&2, K.File>, srcs: List<&2, String>}
+  Go{hash: String, files: List<&2, K.Item>, srcs: List<&2, String>}
   Wait{asks: List<&2, W.Ask>}
   Stop{why: String}
 
@@ -187,7 +187,7 @@ def decide(+world: A.World) -> Verdict:
 # the entry
 
 # whether a package holds a file at this path
-def holds(fs: List<&2, K.File>, +at: String) -> Bool:
+def holds(fs: List<&2, K.Item>, +at: String) -> Bool:
   match fs:
     case []:
       False{}
@@ -209,15 +209,15 @@ def top.at(hit: Bool, +at: String, rest: Unit -> String) -> String:
       rest(Unit{})
 
 # the first top-level `.bend` file, in manifest order, "" for none
-def top(fs: List<&2, K.File>) -> String:
+def top(fs: List<&2, K.Item>) -> String:
   match fs:
     case []:
       ""
     case +h <> t:
       top.at(top.one(K.file.at(h)), K.file.at(h), _u => top(t))
 
 # `main.bend` when the package holds one, else its first top-level file
-def entry.main(held: Bool, fs: List<&2, K.File>) -> String:
+def entry.main(held: Bool, fs: List<&2, K.Item>) -> String:
   match held:
     case True{}:
       "main.bend"
@@ -226,26 +226,26 @@ def entry.main(held: Bool, fs: List<&2, K.File>) -> String:
 
 # the entry a package is recorded with when none was asked for: its
 # `main.bend`, else its first top-level `.bend` file, else none
-def entry.of(+fs: List<&2, K.File>) -> String:
+def entry.of(+fs: List<&2, K.Item>) -> String:
   entry.main(holds(fs, "main.bend"), fs)
 
 # the entry asked for, or, when none was, the package's own
-def entry.pick(none: Bool, +fs: List<&2, K.File>, +asked: String) -> String:
+def entry.pick(none: Bool, +fs: List<&2, K.Item>, +asked: String) -> String:
   match none:
     case True{}:
       entry.of(fs)
     case False{}:
       asked
 
 # the entry recorded: the one asked for, else the package's own
-def entry(+fs: List<&2, K.File>, +world: A.World) -> String:
+def entry(+fs: List<&2, K.Item>, +world: A.World) -> String:
   entry.pick(String.is_empty(asked(world)), fs, asked(world))
 
 # ---------------------------------------------------------------------------
 # the plan
 
 # the dependency recorded for a package the hub named by this hash
-def dep.of(+hash: String, +fs: List<&2, K.File>, +world: A.World) -> M.Dep:
+def dep.of(+hash: String, +fs: List<&2, K.Item>, +world: A.World) -> M.Dep:
   M.Dep{key(world), hash, entry(fs, world), M.Hub{nv(world)}}
 
 # the ledger with the package added, once it is known to read back. A
@@ -267,7 +267,7 @@ def outcome.entry(held: Bool, fit: Bool, +at: String, +world: A.World) -> P.Outc
       P.Refused{"ez: " ++ at ++ " is not in " ++ nv(world)}
 
 # how an add ends once the package is in hand
-def outcome.of(+hash: String, +fs: List<&2, K.File>, +world: A.World) -> P.Outcome:
+def outcome.of(+hash: String, +fs: List<&2, K.Item>, +world: A.World) -> P.Outcome:
   outcome.entry(Bool.or(String.is_empty(asked(world)), holds(fs, Path.norm(asked(world)))),
     Rend.renderable(Rend.add.keep(A.manifest.of(A.read(world)), dep.of(hash, fs, world))),
     asked(world), world)
@@ -325,7 +325,7 @@ def seal(es: List<&2, P.Effect>, outcome: P.Outcome) -> P.Plan:
       P.Plan{[], P.Refused{why}}
 
 # the plan once the package is in hand
-def made(+hash: String, +fs: List<&2, K.File>, +ss: List<&2, String>, +world: A.World) -> P.Plan:
+def made(+hash: String, +fs: List<&2, K.Item>, +ss: List<&2, String>, +world: A.World) -> P.Plan:
   seal(effects.of(dep.of(hash, fs, world), hash, W.laid(fs, ss),
       A.manifest.of(A.read(world)), world),
     outcome.of(hash, fs, world))
@@ -385,7 +385,7 @@ def verdict.hash(verdict: Verdict) -> String:
     case Stop{_why}:
       ""
 
-def verdict.files(verdict: Verdict) -> List<&2, K.File>:
+def verdict.files(verdict: Verdict) -> List<&2, K.Item>:
   match verdict:
     case Go{_hash, fs, _ss}:
       fs
@@ -399,7 +399,7 @@ def hash(+world: A.World) -> String:
   verdict.hash(decide(world))
 
 # the package's files, as the hub served them
-def files(+world: A.World) -> List<&2, K.File>:
+def files(+world: A.World) -> List<&2, K.Item>:
   verdict.files(decide(world))
 
 # the dependency `ez add <name>@<version>` records on a World

add/plan.bend

@@ -564,7 +564,7 @@ def effects.of(
   +hash: String,
   +at: String,
   fs: List<&2, K.Source>,
-  ss: List<&2, K.File>,
+  ss: List<&2, K.Item>,
   +manifest: M.Manifest,
   +world: A.World
 ) -> List<&2, P.Effect>:
@@ -790,21 +790,21 @@ def refuses.command(+world: A.World) -> Bool:
 type Next is Data:
   AskGit{asks: List<&2, Up.Ask>}
   AskHub{asks: List<&2, W.Ask>}
-  Done{plan: P.Plan}
+  Ready{plan: P.Plan}
 
 # the git planner's step
 def next.git(st: Step) -> Next:
   match st:
     case Asking{asks}:
       AskGit{asks}
     case Run{pl}:
-      Done{pl}
+      Ready{pl}
 
 # the hub planner's step: its questions, or its plan once there are none
 def next.hub(asks: List<&2, W.Ask>, +world: A.World) -> Next:
   match asks:
     case []:
-      Done{H.plan(world)}
+      Ready{H.plan(world)}
     case h <> t:
       AskHub{h <> t}
 
@@ -826,5 +826,5 @@ def next.asks(nx: Next) -> Bool:
       True{}
     case AskHub{_asks}:
       True{}
-    case Done{_pl}:
+    case Ready{_pl}:
       False{}

add/run.bend

@@ -10,7 +10,7 @@
 # exits 1 with the reason when the plan refuses. It decides nothing; that it
 # reads and executes faithfully is EZ-TRUST-2.
 import Base
-import 0x103d0af04de36ab98b311e537366ec67/main.bend as R
+import 0xabe575924687afad4cee1a2c1194d639/main.bend as R
 import ../io/file.bend as F
 import ../lock/run.bend as Run
 import ../lock/up.bend as Up
@@ -40,7 +40,7 @@ def loop.step(st: AP.Next, +lib: String, world: A.World, go: A.World -> IO(Unit)
       do IO<Unit>:
         rs : List<&2, W.Reply> <- Run.answer.all(lib, asks)
         go(more.hub(world, rs))
-    case AP.Done{pl}:
+    case AP.Ready{pl}:
       Run.exec.plan(lib, pl)
 
 # the loop, under fuel. Every round adds an answer, since the planner never

check/oracle.bend

@@ -17,9 +17,9 @@
 # One connection is served at a time, each answer states its length and closes
 # the socket, and the oracle stops of its own accord after a million of them.
 import Base
-import ../sha/sha.bend as Sha
+import ../share/sha.bend as Sha
 import ../io/file.bend as F
-import 0x103d0af04de36ab98b311e537366ec67/main.bend as R
+import 0xabe575924687afad4cee1a2c1194d639/main.bend as R
 import ./serve.bend as S
 
 # a list with its last element gone, the head held back one step so the walk can

check/world.bend

@@ -6,7 +6,7 @@
 # directory, and `setsid --fork` returns as soon as the child is a session of
 # its own. Nothing here goes through a shell.
 import Base
-import 0x103d0af04de36ab98b311e537366ec67/main.bend as R
+import 0xabe575924687afad4cee1a2c1194d639/main.bend as R
 
 # the non-empty strings, which is what a program's output amounts to once its
 # trailing newline has been counted as a line

docs/rfc/ez-add-planner.md

@@ -438,7 +438,7 @@ The rewritten `K.pkg_of`, and `K.of` over every tracked file, give the hash, roo
 - A remote's checkout lives at `<root>/<slug>/<rev>/src` with its record at `<root>/<slug>/<rev>/rev`, and every binary at `<dir>/bin/<first 16 hex of Sha.hex(K.show(record))>/<name>.out`, with its record beside it, where `<dir>` is `<root>/<slug>` or `<root>/local<abs>`. A cached checkout is read when its record names the commit and it has an ez.toml; otherwise the interpreter clones it into a scratch directory, the plan lays its texts, and the record goes last, so a checkout cut short is cloned again. The NAR hash `Clone` answers with is not used.
 - The laws, all in `tool/LAWS.bend`: `tool_refusal_writes_nothing`, `sync_refusal_installs_nothing` (EZ-OUT-2); `bin_dir_ez`, `bin_dir_xdg`, `bin_dir_home`, `bin_dir_none`, `tool_links_in_bin_dir`, `tool_needs_bin_dir` (EZ-TOOL-1); `tool_reuses_record`, `tool_builds_on_miss` (EZ-TOOL-2, beside the key laws in `ez/LAWS.bend`); `local_rev_dirty`, `local_rev_unchecked`, `local_rev_elsewhere`, `tool_unrevved_builds` (EZ-TOOL-3); `tool_pin_src`, `tool_pin_rev`, `tool_pin_url`, `tool_pin_over`, `tool_free_src`, `tool_free_rev`, `tool_path_rev`, `local_rev_clean` (EZ-TOOL-4); `tool_run_exits_with_program`, `tool_refusal_exits_one` (EZ-TOOL-5); `tool_link_never_runs` (EZ-TOOL-6); `file_pin_bin`, `file_pin_entry`, `file_bin`, `file_entry`, `file_main`, `tool_builds_file`, `out_name_own`, `out_name_app`, `tool_links_named`, `tool_refuses_unsafe_name` (EZ-TOOL-7); `remote_refuses_slug`, `tool_refuses_bad_slug`, `tool_refuses_nowhere` (EZ-TOOL-8); `tool_rest_dash`, `tool_rest_word`, `tool_rest_none`, `tool_run_passes_words`, `run_line_rest` (EZ-TOOL-9). EZ-TOOL-1 and EZ-TOOL-3 to EZ-TOOL-9 are proved. A law that a condition refuses walks `decide` stage by stage (`pre_*`, `co_*` in `tool/PROOF.bend`), since each stage before the one that checks it stops, waits or goes on.
 - `ez run` hands the entry `Args.run.line(entry, as)`, `bend <entry>` and every word after `run`, so EZ-TOOL-9's second half is a law about that line.
-- `ez/cap.bend`, `ez/env.bend` and `ez/args.bend` are imported as `../ez/…` from every file, as `ez/target.bend` is, since `tool/run.bend` reaches them by that path and bend gives a file one namespace per import closure.
+- `share/cap.bend`, `share/env.bend` and `share/args.bend` live outside every entry directory. Bend 2.0.28 names a file from the importer's real path, so a file in an entry's own directory is one name from there and another from outside it.
 - `ez doctor` has no tool check, so there is nothing of it to convert here.
 
 **Update (WP11, `ez publish`).** `ez publish` is in planner form in the same shape: `pub/world.bend` (the World and the questions), `pub/plan.bend` (pure, with the decision functions of the old `pub/pub.bend`), and `pub/run.bend` (the interpreter), which `ez/cmd.bend` dispatches to. `pub/pub.bend` is deleted. Where it differs from the commands above:

docs/rfc/ez-spec.md

@@ -129,7 +129,7 @@ Every requirement carries exactly one level.
 
 We considered intermediate levels for "checked on examples" and "agrees with an external oracle", and rejected both (see Abandoned Ideas). The short version is that Bend's gate is a proof checker, and anything it checks on a single example is a test wearing a law's syntax. Two levels keep the spec honest: if a claim is not proved for all inputs, we say we are trusting it, and a reader knows exactly how much weight to put on it.
 
-A guarantee proved in a dependency is Trusted from ez's side. The SHA-256 digest comes from Giulio2002/bend-sha256, whose own laws hold it to an executable FIPS 180-4 specification, and HTTP framing is proved in ezhttp, which replaced `net/` in #50. Those proofs are real, but ez's gate does not re-check them, so ez records them as trust with the dependency and pinned hash as the reason.
+A guarantee proved in a dependency is Trusted from ez's side. The SHA-256 digest comes from noah-emp/bend-sha256, whose own laws hold it to an executable FIPS 180-4 specification, and HTTP framing is proved in ezhttp, which replaced `net/` in #50. Those proofs are real, but ez's gate does not re-check them, so ez records them as trust with the dependency and pinned hash as the reason.
 
 A Proved requirement whose law has not landed yet is marked **pending** in `SPEC.md`. Pending is a status, not a third level: it means "intended to be Proved, not yet guaranteed", and the spec says so plainly. Because the gate fails on any undischarged law, a pending requirement's law stays out of LAWS.bend until its proof is written, and the statement lives in `SPEC.md` until then.
 
@@ -507,7 +507,7 @@ These assumptions sit outside the proofs. They are the complete list of Trusted
 | 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. Collision resistance is also assumed. |
 
 EZ-TRUST-3 is narrowed from the first draft: ez verifies hub content itself (EZ-FETCH-1), so what remains is that the hub serves the hash at all, which is what lets EZ-DOC-3 leave hub content out of `inputs`.
 

doctor/plan.bend

@@ -56,7 +56,7 @@ import ../lock/plan.bend as P
 import ../lock/world.bend as W
 import ../lock/lock.bend as L
 import ../ledger/manifest.bend as M
-import ../ez/args.bend as Args
+import ../share/args.bend as Args
 
 # one thing doctor looked at: what to print, and whether it is a problem
 type Note is Data:

doctor/run.bend

@@ -14,10 +14,10 @@
 # is. None of these writes anything, and the plan writes nothing either. It
 # decides nothing; that it reads and executes faithfully is EZ-TRUST-2.
 import Base
-import 0x103d0af04de36ab98b311e537366ec67/main.bend as R
+import 0xabe575924687afad4cee1a2c1194d639/main.bend as R
 import ../run/bend.bend as Bend
 import ../io/file.bend as F
-import ../ez/args.bend as Args
+import ../share/args.bend as Args
 import ../lock/run.bend as Run
 import ../lock/world.bend as W
 import ../lock/lock.bend as L