From d2e4c1365f097d43576e7e0b88dfdd0970079cbd Mon Sep 17 00:00:00 2001 From: Noah Gardner Date: Tue, 29 Sep 2026 19:54:56 -0400 Subject: [PATCH] build: bend 2.0.34, proofs re-checked on it, bench reads argv past the program Bend 2.0.33 removed String.eq.fin; String.eq is now Cmp.is_eq(String.order(a, b)). PROOF.bend's four string-comparison helper laws (cmp_rec_eq, str_eq_at, span_eq_at, find_str_at) state the same fact through a local eq_of, which reads the Cmp a comparison carries as String.eq does. No law in LAWS.bend changed. The flake pins bendlang/bend at 777ee0b, the commit whose flake packages 2.0.34. ez stays on its own bend (2.0.31) until ez releases on 2.0.34, so checks.proofs runs every PROOF.bend on this flake's bend and requires ALL PROOFS CHECK, in place of ez.mkProofs for now. SPEC's proof gate and JSON-TRUST-1/4 describe that. Bend 2.0.32 hands IO.args the program first, so the bench driver drops it before reading its command. Co-Authored-By: Claude Opus 5.5 --- PROOF.bend | 24 ++++++++++++++---------- README.md | 2 +- SPEC.md | 6 +++--- bench/main.bend | 12 ++++++++++-- flake.lock | 42 ++++++++++++++++++++++++++++++++++++++---- flake.nix | 25 ++++++++++++++++++++++--- 6 files changed, 88 insertions(+), 23 deletions(-) diff --git a/PROOF.bend b/PROOF.bend index 38414e2..2dbf7f0 100644 --- a/PROOF.bend +++ b/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 diff --git a/README.md b/README.md index 9e08ebb..e964112 100644 --- a/README.md +++ b/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. diff --git a/SPEC.md b/SPEC.md index 40f8393..15caeea 100644 --- a/SPEC.md +++ b/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. | diff --git a/bench/main.bend b/bench/main.bend index 8da5222..35d8d9c 100644 --- a/bench/main.bend +++ b/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) -> List: + 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: args : List <- IO.args() - main.go(args.of4(args)) + main.go(args.of4(args.rest(args))) diff --git a/flake.lock b/flake.lock index aa8e418..c1c07c1 100644 --- a/flake.lock +++ b/flake.lock @@ -6,6 +6,25 @@ "nixpkgs" ] }, + "locked": { + "lastModified": 1790643370, + "narHash": "sha256-VYGPIHkNeccEaBHGer1B7+GNiWKQBiN/iiS7PozBXx0=", + "owner": "bendlang", + "repo": "bend", + "rev": "777ee0b55c485afdd7e68bd917b3d23a88d77371", + "type": "github" + }, + "original": { + "owner": "bendlang", + "repo": "bend", + "rev": "777ee0b55c485afdd7e68bd917b3d23a88d77371", + "type": "github" + } + }, + "bend_2": { + "inputs": { + "nixpkgs": "nixpkgs" + }, "locked": { "lastModified": 1790482124, "narHash": "sha256-Gv309ikt48M8cISbwSo6V0md2572iieIRiyl3noF1cA=", @@ -17,14 +36,13 @@ "original": { "owner": "bendlang", "repo": "bend", + "rev": "af569d4826913b2ce3557e9829ccad31fcf86f94", "type": "github" } }, "ez": { "inputs": { - "bend": [ - "bend" - ], + "bend": "bend_2", "nixpkgs": [ "nixpkgs" ] @@ -44,6 +62,22 @@ } }, "nixpkgs": { + "locked": { + "lastModified": 1790578696, + "narHash": "sha256-ZoxIApko70jCdbH3l20HWXOBaT2HZd87orzd2yJ9dVE=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "7a0f122f5090cf4c2ade2a13a0e229d4e19ba71f", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixos-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, + "nixpkgs_2": { "locked": { "lastModified": 1789546076, "narHash": "sha256-zVxLZiSnmaaPLwnhj7pwmqe3axBg/C6nG5JZsJMh2g4=", @@ -63,7 +97,7 @@ "inputs": { "bend": "bend", "ez": "ez", - "nixpkgs": "nixpkgs" + "nixpkgs": "nixpkgs_2" } } }, diff --git a/flake.nix b/flake.nix index b3e7857..6c275ea 100644 --- a/flake.nix +++ b/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;