build: bend 2.0.34, proofs re-checked on it, bench reads argv past the program

PROOF.bend

@@ -9023,12 +9023,16 @@ def Laws.str_back(txt, h_sc, h_s):
 
 # WP-P1: the parser on a value's tokens
 
+# the equality answer a string comparison carries, as String.eq reads it
+def eq_of(rr: (String & String) & Cmp) -> Bool:
+  Cmp.is_eq(Pair.snd(String & String, Cmp, rr))
+
 # comparing two strings, one character in front of each, answers as the rest
 law cmp_rec_eq:
   for h1: Char
   for h2: Char
   for rr: (String & String) & Cmp
-  {String.eq.fin(String.cmp.rec(h1, h2, rr)) == String.eq.fin(rr) : Bool}
+  {eq_of(String.cmp.rec(h1, h2, rr)) == eq_of(rr) : Bool}
 
 def cmp_rec_eq(_h1, _h2, rr):
   ((_a, _b), _c) = rr
@@ -9042,7 +9046,7 @@ law str_eq_at:
   for +t1: String
   for +t2: String
   for ec: {U32.cmp(xx, yy) == cc : Cmp}
-  for h: {String.eq.fin(String.cmp.fin(t1, t2, ((Chr{xx}, Chr{yy}), cc))) == True{} : Bool}
+  for h: {eq_of(String.cmp.fin(t1, t2, ((Chr{xx}, Chr{yy}), cc))) == True{} : Bool}
   for ih: {String.eq(t1, t2) == True{} : Bool} -> {t1 == t2 : String}
   {SCon{Chr{xx}, t1} == SCon{Chr{yy}, t2} : String}
 
@@ -9053,8 +9057,8 @@ def str_eq_at(cc, xx, yy, t1, t2, ec, h, ih):
     case GT{}:
       Empty.absurd({SCon{Chr{xx}, t1} == SCon{Chr{yy}, t2} : String}, false_true(h))
     case EQ{}:
-      et = ih(Equal.trans(Bool, String.eq(t1, t2), String.eq.fin(String.cmp.rec(Chr{xx}, Chr{yy}, String.cmp(t1, t2))),
-        True{}, Equal.sym(Bool, String.eq.fin(String.cmp.rec(Chr{xx}, Chr{yy}, String.cmp(t1, t2))), String.eq(t1, t2),
+      et = ih(Equal.trans(Bool, String.eq(t1, t2), eq_of(String.cmp.rec(Chr{xx}, Chr{yy}, String.cmp(t1, t2))),
+        True{}, Equal.sym(Bool, eq_of(String.cmp.rec(Chr{xx}, Chr{yy}, String.cmp(t1, t2))), String.eq(t1, t2),
           cmp_rec_eq(Chr{xx}, Chr{yy}, String.cmp(t1, t2))), h))
       ex = ueq(xx, yy, Equal.cong(Cmp, Bool, zz => Cmp.is_eq(zz), U32.cmp(xx, yy), EQ{}, ec))
       %ex : {SCon{Chr{xx}, t1} == SCon{Chr{_}, t2} : String}
@@ -11755,7 +11759,7 @@ law span_eq_at:
   for ih: {V.span.eq.go(as, True{}, U32.is_zero(U32.sub(nn, 1)), bs, U32.sub(nn, 1)) ==
     String.eq(V.span.str(as, U32.sub(nn, 1), U32.is_zero(U32.sub(nn, 1))), bs) : Bool}
   {V.span.eq.go(as, Cmp.is_eq(cc), U32.is_zero(U32.sub(nn, 1)), bs, U32.sub(nn, 1)) ==
-    String.eq.fin(String.cmp.fin(V.span.str(as, U32.sub(nn, 1), U32.is_zero(U32.sub(nn, 1))), bs,
+    eq_of(String.cmp.fin(V.span.str(as, U32.sub(nn, 1), U32.is_zero(U32.sub(nn, 1))), bs,
       ((Chr{xx}, Chr{yy}), cc))) : Bool}
 
 def span_eq_at(cc, xx, yy, as, bs, nn, ih):
@@ -11767,8 +11771,8 @@ def span_eq_at(cc, xx, yy, as, bs, nn, ih):
     case EQ{}:
       +sp = V.span.str(as, U32.sub(nn, 1), U32.is_zero(U32.sub(nn, 1)))
       Equal.trans(Bool, V.span.eq.go(as, True{}, U32.is_zero(U32.sub(nn, 1)), bs, U32.sub(nn, 1)), String.eq(sp, bs),
-        String.eq.fin(String.cmp.rec(Chr{xx}, Chr{yy}, String.cmp(sp, bs))), ih,
-        Equal.sym(Bool, String.eq.fin(String.cmp.rec(Chr{xx}, Chr{yy}, String.cmp(sp, bs))), String.eq(sp, bs),
+        eq_of(String.cmp.rec(Chr{xx}, Chr{yy}, String.cmp(sp, bs))), ih,
+        Equal.sym(Bool, eq_of(String.cmp.rec(Chr{xx}, Chr{yy}, String.cmp(sp, bs))), String.eq(sp, bs),
           cmp_rec_eq(Chr{xx}, Chr{yy}, String.cmp(sp, bs))))
 
 # comparing a span with a key is comparing what the span covers with it
@@ -12894,7 +12898,7 @@ law find_str_at:
   for +as: String
   for +bs: String
   for ih: {V.find.eq.go(as, bs, True{}) == String.eq(as, bs) : Bool}
-  {V.find.eq.go(as, bs, Cmp.is_eq(cc)) == String.eq.fin(String.cmp.fin(as, bs, ((Chr{xx}, Chr{yy}), cc))) : Bool}
+  {V.find.eq.go(as, bs, Cmp.is_eq(cc)) == eq_of(String.cmp.fin(as, bs, ((Chr{xx}, Chr{yy}), cc))) : Bool}
 
 def find_str_at(cc, xx, yy, as, bs, ih):
   match cc:
@@ -12904,8 +12908,8 @@ def find_str_at(cc, xx, yy, as, bs, ih):
       find_miss(as, bs)
     case EQ{}:
       Equal.trans(Bool, V.find.eq.go(as, bs, True{}), String.eq(as, bs),
-        String.eq.fin(String.cmp.rec(Chr{xx}, Chr{yy}, String.cmp(as, bs))), ih,
-        Equal.sym(Bool, String.eq.fin(String.cmp.rec(Chr{xx}, Chr{yy}, String.cmp(as, bs))), String.eq(as, bs),
+        eq_of(String.cmp.rec(Chr{xx}, Chr{yy}, String.cmp(as, bs))), ih,
+        Equal.sym(Bool, eq_of(String.cmp.rec(Chr{xx}, Chr{yy}, String.cmp(as, bs))), String.eq(as, bs),
           cmp_rec_eq(Chr{xx}, Chr{yy}, String.cmp(as, bs))))
 
 # find.eq is String.eq

README.md

@@ -96,7 +96,7 @@ def owned(cur: Pull.Cur) -> (String & Pull.Cur):
 to [RFC 8259](https://www.rfc-editor.org/rfc/rfc8259) and the behavior of
 each def in `main.bend`. A row is either proved by a quantified law in
 `LAWS.bend`, checked by `bend PROOF.bend` (the first line must be
-`All terms check.`), or listed in its trust boundary. A row marked pending is
+`ALL PROOFS CHECK`), or listed in its trust boundary. A row marked pending is
 not guaranteed yet. [docs/rfc/ezjson-spec.md](docs/rfc/ezjson-spec.md) has the
 reasoning and the rollout.
 

SPEC.md

@@ -2,7 +2,7 @@
 
 This is the list of every behavior ezjson guarantees, each under a stable requirement ID. There are two families: conformance to [RFC 8259](https://www.rfc-editor.org/rfc/rfc8259) (JSON-TEXT, JSON-NUM, JSON-STR, JSON-PRINT) and the public interface in `main.bend` (JSON-TREE, JSON-PULL). Every other module 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 `LAWS.bend` that passes the proof gate. A **Trusted** requirement is an assumption ezjson 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 PROOF.bend` prints is exactly `All terms check.` 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 `LAWS.bend` that passes the proof gate. A **Trusted** requirement is an assumption ezjson 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 PROOF.bend` prints is exactly `ALL PROOFS CHECK`. Tests and fixtures are never evidence for a requirement.
 
 A value is **well-formed** when `V.wf` holds of it: its arrays and objects are chains of cells ending in `JNil`, no cell stands where a value belongs, and every number's text is a JSON number. Every value built through `main.bend` or returned by `parse` is well-formed (JSON-PRINT-3). `same` is the specification relation "the same JSON value", which ignores whether a string or key is owned or a span of the source. `LAWS.bend` decides it with `own`, which reads every span out into its own string: two values are `same` when their `own` forms are equal.
 
@@ -98,7 +98,7 @@ These assumptions sit outside the proofs. They are the complete list of Trusted
 
 | ID | Assumption | Why it is trusted |
 | :---- | :---- | :---- |
-| JSON-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. ezjson pins bend 2.0.25 through the flake. |
+| JSON-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. ezjson pins bend 2.0.34 through the flake. |
 | JSON-TRUST-2 | `F32.read` in Bend's base library reads a decimal spelling as documented, rounding to nearest. | Foreign to this project; `as_f32` forwards to it. `U32.read` is no longer trusted: JSON-TREE-6's `as_u32_num` is proved through it as written. |
 | JSON-TRUST-3 | The cursor does not keep a parse tree or the text it has passed: memory while walking a large text stays proportional to the open containers and the events the caller holds. | A law sees values, not heap shape. The `scale` flake check walks a 563 KiB and a 615 KiB text with the cursor as an integration check. |
-| JSON-TRUST-4 | The proof-gate runner fails the build unless the first line of `bend PROOF.bend` is `All terms check.` | It is ez's `mkProofs`, run by `nix flake check` in CI; this is EZ-TRUST-4. |
+| JSON-TRUST-4 | The proof-gate runner fails the build unless the first line of `bend PROOF.bend` is `ALL PROOFS CHECK`. | It is the flake's `checks.proofs`, run by `nix flake check` in CI on the flake's bend 2.0.34; it stands in for ez's `mkProofs` (EZ-TRUST-4) until ez runs on 2.0.34. |

bench/main.bend

@@ -730,8 +730,16 @@ def main.go(quad: String & String & String & String) -> IO(Unit):
   (a, b, c, d) = quad
   run.named(a, b, c, d)
 
-# CLI entry: dispatch by the first argv word
+# argv past the program name (bend 2.0.32 puts the program first)
+def args.rest(xs: List<String>) -> List<String>:
+  match xs:
+    case _p <> t:
+      t
+    case Nil{}:
+      Nil{}
+
+# CLI entry: dispatch by the first argument after the program
 def main() -> IO(Unit):  # noqa: L001 IO entry point
   do IO<Unit>:
     args : List<String> <- IO.args()
-    main.go(args.of4(args))
+    main.go(args.of4(args.rest(args)))

flake.nix

@@ -2,14 +2,19 @@
   description = "ezjson: JSON for Bend 2";
 
   inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable";
+  # bendlang/bend's flake at the commit that packages 2.0.34 (the v2.0.34 tag
+  # still packages 2.0.33)
   inputs.bend = {
-    url = "github:bendlang/bend";
+    url = "github:bendlang/bend/777ee0b55c485afdd7e68bd917b3d23a88d77371";
     inputs.nixpkgs.follows = "nixpkgs";
   };
+  # ez and its bolt stay on the bend ez's own flake.lock records until ez
+  # releases on 2.0.34, so ez's inputs.bend is pinned, not followed. The
+  # package's own builds and its proofs (checks.proofs) run on 2.0.34.
   inputs.ez = {
     url = "github:Emerging-Patterns/ez";
     inputs.nixpkgs.follows = "nixpkgs";
-    inputs.bend.follows = "bend";
+    inputs.bend.url = "github:bendlang/bend/af569d4826913b2ce3557e9829ccad31fcf86f94";
   };
 
   outputs = { self, nixpkgs, ... }@inputs:
@@ -41,7 +46,21 @@
       apps.${system} = bench.apps;
 
       checks.${system} = {
-        proofs = ez.mkProofs { ez = ezBin; src = self; };
+        # every PROOF.bend on this flake's bend: its first line must be
+        # ALL PROOFS CHECK. ez.mkProofs comes back when ez runs on 2.0.34.
+        proofs = pkgs.runCommand "ezjson-proofs" {
+          nativeBuildInputs = [ bend ];
+          BEND_LIB = ez.bendLib ./ez.lock.toml;
+        } ''
+          export HOME=$TMPDIR
+          cp -r ${self} src && chmod -R u+w src && cd src
+          for p in $(find . -name PROOF.bend -not -path './.ez/*' | sort); do
+            first=$(cd "$(dirname "$p")" && bend "$(basename "$p")" | head -n 1)
+            echo "$p: $first"
+            [ "$first" = "ALL PROOFS CHECK" ] || exit 1
+          done
+          touch $out
+        '';
         lint = ez.mkLint { src = self; };
       } // bench.checks // scale.checks;