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;