From f7b98c3f65a97b82e3efc5238256dbd962d7d528 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 29 Sep 2026 23:52:06 +0000 Subject: [PATCH] build: bend 2.0.34, ez follows it Pin bendlang/bend at 777ee0b. The proof gate reads ALL PROOFS CHECK. The bench reads arguments after the program name. Co-authored-by: noah-emp --- PROOF.bend | 22 +++++++++++----------- README.md | 2 +- SPEC.md | 4 ++-- bench/main.bend | 12 ++++++++++-- flake.lock | 7 ++++--- flake.nix | 16 ++++++++++++++-- 6 files changed, 42 insertions(+), 21 deletions(-) diff --git a/PROOF.bend b/PROOF.bend index 38414e2..43efad7 100644 --- a/PROOF.bend +++ b/PROOF.bend @@ -9028,7 +9028,7 @@ 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} + {Cmp.is_eq(Pair.snd(String & String, Cmp, String.cmp.rec(h1, h2, rr))) == Cmp.is_eq(Pair.snd(String & String, Cmp, rr)) : Bool} def cmp_rec_eq(_h1, _h2, rr): ((_a, _b), _c) = rr @@ -9042,7 +9042,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: {Cmp.is_eq(Pair.snd(String & String, Cmp, 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 +9053,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), Cmp.is_eq(Pair.snd(String & String, Cmp, String.cmp.rec(Chr{xx}, Chr{yy}, String.cmp(t1, t2)))), + True{}, Equal.sym(Bool, Cmp.is_eq(Pair.snd(String & String, Cmp, 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,8 +11755,8 @@ 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, - ((Chr{xx}, Chr{yy}), cc))) : Bool} + Cmp.is_eq(Pair.snd(String & String, Cmp, 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): match cc: @@ -11767,8 +11767,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), + Cmp.is_eq(Pair.snd(String & String, Cmp, String.cmp.rec(Chr{xx}, Chr{yy}, String.cmp(sp, bs)))), ih, + Equal.sym(Bool, Cmp.is_eq(Pair.snd(String & String, Cmp, 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 +12894,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)) == Cmp.is_eq(Pair.snd(String & String, Cmp, 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 +12904,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), + Cmp.is_eq(Pair.snd(String & String, Cmp, String.cmp.rec(Chr{xx}, Chr{yy}, String.cmp(as, bs)))), ih, + Equal.sym(Bool, Cmp.is_eq(Pair.snd(String & String, Cmp, 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..a4a8c04 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. @@ -101,4 +101,4 @@ These assumptions sit outside the proofs. They are the complete list of 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-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 proofs check in the flake, run by `nix flake check` in CI; this is EZ-TRUST-4. | diff --git a/bench/main.bend b/bench/main.bend index 8da5222..b5513ce 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 +# the arguments after the program name, which IO.args gives first +def args.after(xs: List) -> List: + match xs: + case _p <> t: + t + case Nil{}: + Nil{} + +# CLI entry: dispatch by the first argument 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.after(args))) diff --git a/flake.lock b/flake.lock index aa8e418..7487737 100644 --- a/flake.lock +++ b/flake.lock @@ -7,16 +7,17 @@ ] }, "locked": { - "lastModified": 1790482124, - "narHash": "sha256-Gv309ikt48M8cISbwSo6V0md2572iieIRiyl3noF1cA=", + "lastModified": 1790643370, + "narHash": "sha256-VYGPIHkNeccEaBHGer1B7+GNiWKQBiN/iiS7PozBXx0=", "owner": "bendlang", "repo": "bend", - "rev": "af569d4826913b2ce3557e9829ccad31fcf86f94", + "rev": "777ee0b55c485afdd7e68bd917b3d23a88d77371", "type": "github" }, "original": { "owner": "bendlang", "repo": "bend", + "rev": "777ee0b55c485afdd7e68bd917b3d23a88d77371", "type": "github" } }, diff --git a/flake.nix b/flake.nix index b3e7857..15317ba 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 = { @@ -41,7 +41,19 @@ apps.${system} = bench.apps; checks.${system} = { - proofs = ez.mkProofs { ez = ezBin; src = self; }; + proofs = pkgs.runCommand "proofs" { + nativeBuildInputs = [ bend ]; + } '' + export HOME=$TMPDIR + export BEND_NO_TELEMETRY=1 + 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;