diff --git a/.github/workflows/conformance.yml b/.github/workflows/conformance.yml index 4946c18..3e7547e 100644 --- a/.github/workflows/conformance.yml +++ b/.github/workflows/conformance.yml @@ -11,9 +11,9 @@ on: required: false default: "" legs: - description: "comma list of legs (suite,cross,pkg,programs,fail,diag)" + description: "comma list of legs (suite,cross,pkg,programs,fail,diag,ref)" required: false - default: "suite,cross,pkg,programs,fail,diag" + default: "suite,cross,pkg,programs,fail,diag,ref" schedule: - cron: "17 3 * * 1" jobs: @@ -45,11 +45,23 @@ jobs: curl -fLO "https://github.com/bytecodealliance/wasmtime/releases/download/${WASMTIME_VERSION}/${TARBALL}" tar xJf "$TARBALL" echo "$PWD/wasmtime-${WASMTIME_VERSION}-x86_64-linux" >> "$GITHUB_PATH" + - name: Build the reference evaluator (ADR-0015 — pinned stable toolchain) + uses: dtolnay/rust-toolchain@stable + with: + toolchain: 1.95.0 + - uses: actions/cache@v4 + with: + path: | + ~/.cargo/registry + ref/target + key: ref-${{ runner.os }}-1.95.0-${{ hashFiles('ref/Cargo.lock', 'ref/src/**') }} + - run: cargo build --release --quiet + working-directory: ref - name: Judge run: | wasmtime --version python3 scripts/conformance.py --almide "$ALMIDE" \ - --legs "${{ inputs.legs || 'suite,cross,pkg,programs,fail,diag' }}" \ + --legs "${{ inputs.legs || 'suite,cross,pkg,programs,fail,diag,ref' }}" \ --jobs 4 --report "conformance-${TAG}.toml" - name: Spec doctest self-test — the judge turns red for every verdict class run: python3 scripts/doctest.py --almide "$ALMIDE" --selftest diff --git a/QUALIFICATION.md b/QUALIFICATION.md index 46096da..63d1850 100644 --- a/QUALIFICATION.md +++ b/QUALIFICATION.md @@ -40,9 +40,13 @@ Stated so they cannot be mistaken for claims: (`ref/`, ADR-0015 — fresh from the ALS text, pinned stable Rust, zero dependencies; λ_almd kernel corpus reproduced 49/49; 173/602 programs of the cross corpora evaluated, the rest ledgered by class, shrink-only, - `proofs/ref-abstain.toml`); what is NOT yet in place is the runner's - `ref` leg whose verdict is *legs == ref* — until it runs, this - limitation stands as declared ([#10](https://github.com/almide/als/issues/10)). + `proofs/ref-abstain.toml`); the runner's `ref` leg (verdict + *legs == ref* wherever the reference evaluates — TOR-8's adjudication, + with the co-drift class pinned red in `selftest-conformance.py`) runs + since 2026-08-21. The limitation therefore narrows rather than lifts: + on the ABSTAINED subset (the ledger) the runner still judges agreement, + and the ledger is the shrink-only bound of that remainder + ([#10](https://github.com/almide/als/issues/10)). Its first pass already produced the class this limitation describes: two programs on which both targets agree and the text-reading evaluator does not (`docs/ref/PARSER-NOTES.md` F1, F2). diff --git a/README.md b/README.md index 61fe6db..51235fa 100644 --- a/README.md +++ b/README.md @@ -125,8 +125,12 @@ paths that were renamed into place lives in the implementation repository. evaluates 173 of 602 programs (171 of the 172 comparable ones agree with the native target; the one disagreement and the two findings are in `docs/ref/PARSER-NOTES.md`) and abstains on 429 in 152 ledgered classes — - the long tail is stdlib. The `ref` leg of the runner (verdict *legs == ref*) - is the next step; until it runs, limitation 2 of QUALIFICATION.md stands. + the long tail is stdlib. The runner's `ref` leg exists (verdict + *legs == ref* wherever the reference evaluates; abstains counted, never + verdicts; `// @ref-allow:` tracks adjudicated findings) — so limitation 2 + of QUALIFICATION.md is now bounded by the abstain ledger instead of by the + absence of an instrument: on the evaluated subset the runner judges truth, + on the abstained subset it still judges agreement. - The `greenfield` rebuild pins this repository as a submodule since 2026-08-20 (BOUNDARY.md, "Stage B"); `almide/almide` `develop` still carries copies, and its cutover is a separately decided step. diff --git a/proofs/gate-verification.toml b/proofs/gate-verification.toml index 73c1ed7..40f1099 100644 --- a/proofs/gate-verification.toml +++ b/proofs/gate-verification.toml @@ -61,12 +61,12 @@ evidence = "Bootstrap run (PR #5, 2026-08-20): before first green, a mis-pathed [[gate]] path = "scripts/conformance.py" class = "NEGATIVE_TESTED" -evidence = "scripts/selftest-conformance.py: 21 scenarios drive the real runner over a scripted stub implementation through every verdict class per leg — cross (stdout/stderr/exit divergence, build refusal, @xt-allow tracked, healed-allow STALE), fail (success-is-failure, wrong message, split legs, missing header is red never skipped, @xf-allow, stale), diag (accepted-broken, missing code, missing hint, unfixable fix), suite (failed-count red even at exit 0) — asserting both the process exit AND the statement's per-leg counters. A dropped scenario fails the declared-count guard (which fired on its own landing run: 21 written, 20 declared). Runs in the gates workflow on every push." +evidence = "scripts/selftest-conformance.py: 21 scenarios drive the real runner over a scripted stub implementation through every verdict class per leg — cross (stdout/stderr/exit divergence, build refusal, @xt-allow tracked, healed-allow STALE), fail (success-is-failure, wrong message, split legs, missing header is red never skipped, @xf-allow, stale), diag (accepted-broken, missing code, missing hint, unfixable fix), suite (failed-count red even at exit 0) — asserting both the process exit AND the statement's per-leg counters. A dropped scenario fails the declared-count guard (which fired on its own landing run: 21 written, 20 declared). Runs in the gates workflow on every push. 2026-08-21: the ref leg (verdict legs == REFERENCE, TOR-8) added with nine selftest scenarios — including the co-drift class (targets agree with each other, both differ from the reference → red), abstain-is-not-a-verdict, malformed-protocol-is-red, and @ref-allow in both directions." [[gate]] path = "scripts/selftest-conformance.py" class = "EXERCISED" -evidence = "Its declared-count guard fired on the landing run (21 scenarios vs a declared 20) and went green only after the declaration was corrected — the harness's own red direction observed before first green. Each scenario asserts a red and its reason, so a runner regression flips at least one scenario." +evidence = "Its declared-count guard fired on the landing run (21 scenarios vs a declared 20) and went green only after the declaration was corrected — the harness's own red direction observed before first green. Each scenario asserts a red and its reason, so a runner regression flips at least one scenario. 2026-08-21: grown from 21 to 30 scenarios with the ref leg (stub als-ref scripted per file; the count guard moved 21→30 so a dropped scenario stays loud)." [[gate]] path = "scripts/doctest.py" diff --git a/proofs/runner-coverage.toml b/proofs/runner-coverage.toml index 41388bc..02173e0 100644 --- a/proofs/runner-coverage.toml +++ b/proofs/runner-coverage.toml @@ -6,7 +6,7 @@ # The floor is EXACT: below it is a regression, above it the floor must be # ratcheted up (--write records the measured value). # -# line_floor = "85.1" -# executable_lines = "261" -# module_level_lines_excluded = "33" -# uncovered = "110-113 145-146 166 199 234 248 299-302 304-305 309-313 380-389 407-408 410-411 413-414 440-441" +# line_floor = "86.3" +# executable_lines = "314" +# module_level_lines_excluded = "34" +# uncovered = "122-125 157-158 178 211 246 260 311-314 316-317 321-325 341 446-455 475-476 478-479 481-482 484 486-487 513-514" diff --git a/scripts/conformance.py b/scripts/conformance.py index 55292a7..529c90a 100755 --- a/scripts/conformance.py +++ b/scripts/conformance.py @@ -32,6 +32,17 @@ diagnostic carrying meta.toml's expects_code / expects_error / hint_substring; `almide check fixed.almd` must pass clean. (tests/diagnostic_harness_test.rs) + ref spec/wasm_cross + spec/programs against the REFERENCE EVALUATOR + (ref/, ADR-0015; TOR-8's adjudication): where the reference + evaluates a program, BOTH targets must equal ITS observables — + agreement between the two targets is no longer sufficient. A + reference abstain (a ledgered class, proofs/ref-abstain.toml) is + counted and skipped, never a pass or a fail; a malformed protocol + reply or an evaluator fault is red. `// @ref-allow: ` + tracks a known reference disagreement (a FINDING under + adjudication, e.g. docs/ref/PARSER-NOTES.md F1) without passing + it, and goes STALE the moment the legs match the reference again. + Needs --ref (default: ref/target/release/als-ref). Exit status: 0 = every leg PASS (no failure, no stale allow); 1 = a failure; 2 = usage / environment error. `--limit N` runs the first N items of each @@ -68,6 +79,7 @@ def _flush(): _atexit.register(_flush) import argparse +import json import concurrent.futures as cf import datetime as dt import platform @@ -83,7 +95,7 @@ def _flush(): FAIL_DIR = "spec/wasm_fail" DIAG_DIR = "tests/diagnostics" SUITE_DIRS = ["spec/lang", "spec/stdlib", "spec/integration"] -ALL_LEGS = ["suite", "cross", "pkg", "programs", "fail", "diag"] +ALL_LEGS = ["suite", "cross", "pkg", "programs", "fail", "diag", "ref"] class Leg: @@ -321,6 +333,59 @@ def leg_fail(args, root): return leg +def ref_item(args, root, rel): + """One program against the reference evaluator: legs == ref (TOR-8).""" + path = os.path.join(root, rel) + code, out, err = run([args.ref, "run", path, "--json"], timeout=300) + if code != 0: + return ("failed", rel, f"reference protocol fault: exit {code}\n {err[:300]}") + try: + doc = json.loads(out) + except json.JSONDecodeError: + return ("failed", rel, f"reference protocol fault: malformed reply {out[:200]!r}") + if "error" in doc: + return ("failed", rel, f"reference evaluator fault: {str(doc['error'])[:300]}") + if "abstain" in doc: + a = doc["abstain"] + return ("abstain", rel, f"{a.get('class', '?')}: {str(a.get('reason', ''))[:160]}") + ref3 = (doc.get("exit"), str(doc.get("stdout", "")).strip(), str(doc.get("stderr", "")).strip()) + allow = header_directive(path, "ref-allow") + native = build_and_run(args, path, "rust") + wasm = build_and_run(args, path, "wasm") + mismatches = [tag for tag, leg3 in (("native", native), ("wasm", wasm)) if leg3 != ref3] + if not mismatches and allow is None: + return ("passed", rel, "") + if not mismatches and allow is not None: + return ("stale", rel, f"@ref-allow now MATCHES (was: {allow}) — remove the directive") + if mismatches and allow is not None: + return ("allowed", rel, allow) + return ("failed", rel, + f"reference disagreement ({', '.join(mismatches)})\n " + fmt_leg("ref", ref3) + + "\n " + fmt_leg("native", native) + "\n " + fmt_leg("wasm", wasm)) + + +def leg_ref(args, root): + leg = Leg("ref") + items = [f"{CROSS_DIR}/{f}" for f in sorted(os.listdir(os.path.join(root, CROSS_DIR))) if f.endswith(".almd")] + items += [f"{PROGRAMS_DIR}/{f}" for f in sorted(os.listdir(os.path.join(root, PROGRAMS_DIR))) if f.endswith(".almd")] + items = items[: args.limit] if args.limit else items + results = pmap(lambda rel: ref_item(args, root, rel), items, args.jobs) + classes = {} + plain = [] + for status, item, detail in results: + if status == "abstain": + leg.total += 1 + leg.skipped.append((item, f"reference abstain — {detail}")) + classes[detail.split(":")[0]] = classes.get(detail.split(":")[0], 0) + 1 + else: + plain.append((status, item, detail)) + collect(leg, plain) + judged = leg.passed + len(leg.failed) + len(leg.allowed) + len(leg.stale) + leg.notes.append(f"reference judged {judged}, abstained {len(leg.skipped)} " + f"(top classes: {', '.join(f'{k} {v}' for k, v in sorted(classes.items(), key=lambda kv: -kv[1])[:6])})") + return leg + + def leg_diag(args, root): leg = Leg("diag") cases = sorted(c for c in os.listdir(os.path.join(root, DIAG_DIR)) @@ -331,7 +396,7 @@ def leg_diag(args, root): LEG_FNS = {"suite": leg_suite, "cross": leg_cross, "pkg": leg_pkg, - "programs": leg_programs, "fail": leg_fail, "diag": leg_diag} + "programs": leg_programs, "fail": leg_fail, "diag": leg_diag, "ref": leg_ref} # ── statement ─────────────────────────────────────────────────────────────── @@ -353,6 +418,7 @@ def statement(args, root, legs, verdict): f"almide = {toml_str(almide_ver)}", f"almide_path = {toml_str(os.path.abspath(args.almide))}", f"wasmtime = {toml_str(wt[1] if wt[0] == 0 else 'absent')}", + f"ref = {toml_str(run([args.ref, '--version'])[1] or 'absent')}", f"platform = {toml_str(platform.platform())}", f"date = {toml_str(dt.datetime.now(dt.timezone.utc).strftime('%Y-%m-%dT%H:%M:%SZ'))}", f"legs = [{', '.join(toml_str(l.name) for l in legs)}]", @@ -395,6 +461,8 @@ def main(): ap.add_argument("--jobs", type=int, default=max(1, (os.cpu_count() or 2) // 2)) ap.add_argument("--legs", default=",".join(ALL_LEGS), help=f"comma list of {ALL_LEGS}") ap.add_argument("--limit", type=int, default=0, help="first N items per leg (smoke run; recorded)") + ap.add_argument("--ref", default=None, + help="path to the reference evaluator (als-ref); default ref/target/release/als-ref under --root") ap.add_argument("--report", help="write the conformance statement (TOML) here") ap.add_argument("--root", default=os.path.join(os.path.dirname(os.path.abspath(__file__)), "..")) args = ap.parse_args() @@ -409,9 +477,14 @@ def main(): if run([args.almide, "--version"])[0] != 0: print(f"cannot execute {args.almide} --version", file=sys.stderr) return 2 - if any(l in legs_wanted for l in ("suite", "cross", "pkg", "programs", "fail")) and run(["wasmtime", "--version"])[0] != 0: + if any(l in legs_wanted for l in ("suite", "cross", "pkg", "programs", "fail", "ref")) and run(["wasmtime", "--version"])[0] != 0: print("wasmtime not on PATH — the wasm leg cannot run (install it, or restrict --legs to diag)", file=sys.stderr) return 2 + if args.ref is None: + args.ref = os.path.join(root, "ref", "target", "release", "als-ref") + if "ref" in legs_wanted and run([args.ref, "--version"])[0] != 0: + print(f"cannot execute {args.ref} --version — build the reference evaluator (cd ref && cargo build --release) or pass --ref", file=sys.stderr) + return 2 legs = [] for name in legs_wanted: diff --git a/scripts/selftest-conformance.py b/scripts/selftest-conformance.py index 726fd28..0cdad0e 100755 --- a/scripts/selftest-conformance.py +++ b/scripts/selftest-conformance.py @@ -60,6 +60,21 @@ sys.exit(2) ''' +STUB_REF = r'''#!/usr/bin/env python3 +import json, os, sys +if sys.argv[1:2] == ["--version"]: + print("als-ref 0.0-stub"); sys.exit(0) +S = json.load(open(os.environ["ALS_STUB_SCENARIO"])) +# argv: run --json +name = os.path.basename(sys.argv[2]) +doc = S.get("refs", {}).get(name) +if doc is None: + print(json.dumps({"abstain": {"class": "stub:unscripted", "reason": "no scripted reply"}})); sys.exit(0) +if doc == "MALFORMED": + print("this is not json"); sys.exit(0) +print(json.dumps(doc)); sys.exit(0) +''' + STUB_WASMTIME = r'''#!/usr/bin/env python3 import json, sys if sys.argv[1:2] == ["--version"]: @@ -89,19 +104,20 @@ def write(root, rel, text): def run_case(td, name, legs, build, expect_exit, expect): """build(root, scenario) populates the tree + stub behaviour.""" root = make_root(td) - scenario = {"programs": {}, "checks": {}, "suites": {}} + scenario = {"programs": {}, "checks": {}, "suites": {}, "refs": {}} build(root, scenario) sdir = os.path.join(td, "stub") os.makedirs(sdir, exist_ok=True) spath = os.path.join(sdir, "scenario.json") json.dump(scenario, open(spath, "w")) - for fname, body in [("almide", STUB_ALMIDE), ("wasmtime", STUB_WASMTIME)]: + for fname, body in [("almide", STUB_ALMIDE), ("wasmtime", STUB_WASMTIME), ("als-ref", STUB_REF)]: p = os.path.join(sdir, fname) open(p, "w").write(body) os.chmod(p, 0o755) report = os.path.join(td, "report.toml") env = dict(os.environ, ALS_STUB_SCENARIO=spath, PATH=sdir + os.pathsep + os.environ["PATH"]) r = subprocess.run([sys.executable, RUNNER, "--almide", os.path.join(sdir, "almide"), + "--ref", os.path.join(sdir, "als-ref"), "--legs", legs, "--jobs", "1", "--report", report, "--root", root], env=env, capture_output=True, text=True, timeout=300) problems = [] @@ -223,6 +239,42 @@ def _(root, s): s["suites"]["spec/lang/wasm"] = {"exit": 0, "stdout": "0 passed, 2 failed (of 2 files)"} +# ── the ref leg: the verdict is legs == REFERENCE, not legs agree ───────── + +REF_OK = {"exit": 0, "stdout": "x\n", "stderr": ""} + +def ref_fixture(root, s, name, native, wasm, ref, header=""): + cross_fixture(root, s, name, native, wasm, header=header) + s["refs"][f"{name}.almd"] = ref + +@case("ref: both legs equal the reference is the only green", "ref", 0, {"ref": {"total": 1, "passed": 1, "failed": 0, "skipped": 0}}) +def _(root, s): ref_fixture(root, s, "r_ok", OK, OK, REF_OK) + +@case("ref: native differing from the reference is red", "ref", 1, {"ref": {"failed": 1}}) +def _(root, s): ref_fixture(root, s, "r_nat", dict(OK, stdout="y\n"), OK, REF_OK) + +@case("ref: wasm differing from the reference is red", "ref", 1, {"ref": {"failed": 1}}) +def _(root, s): ref_fixture(root, s, "r_wasm", OK, dict(OK, stdout="y\n"), REF_OK) + +@case("ref: CO-DRIFT — the targets agree with each other and both differ from the reference — is red", "ref", 1, {"ref": {"failed": 1, "passed": 0}}) +def _(root, s): ref_fixture(root, s, "r_codrift", dict(OK, stdout="y\n"), dict(OK, stdout="y\n"), REF_OK) + +@case("ref: a reference abstain is counted and skipped, never a verdict", "ref", 0, {"ref": {"total": 1, "passed": 0, "failed": 0, "skipped": 1}}) +def _(root, s): ref_fixture(root, s, "r_abst", OK, OK, {"abstain": {"class": "stdlib:x.y", "reason": "scripted"}}) + +@case("ref: a malformed protocol reply is red, never a verdict", "ref", 1, {"ref": {"failed": 1}}) +def _(root, s): ref_fixture(root, s, "r_bad", OK, OK, "MALFORMED") + +@case("ref: an evaluator fault is red", "ref", 1, {"ref": {"failed": 1}}) +def _(root, s): ref_fixture(root, s, "r_fault", OK, OK, {"error": "scripted fault"}) + +@case("ref: @ref-allow tracks an adjudicated disagreement without passing it", "ref", 0, {"ref": {"allowed": 1, "passed": 0, "failed": 0}}) +def _(root, s): ref_fixture(root, s, "r_track", dict(OK, stdout="y\n"), dict(OK, stdout="y\n"), REF_OK, header="// @ref-allow: F-numbered finding under adjudication\n") + +@case("ref: a healed @ref-allow is STALE and red", "ref", 1, {"ref": {"stale": 1, "failed": 0}}) +def _(root, s): ref_fixture(root, s, "r_stale", OK, OK, REF_OK, header="// @ref-allow: was disagreeing\n") + + def main(): failures = [] for name, legs, build, expect_exit, expect in CASES: @@ -235,14 +287,14 @@ def main(): if problems: failures.append(name) n = len(CASES) - expected_n = 21 + expected_n = 30 if n != expected_n: failures.append(f"scenario count {n} != declared {expected_n} — a dropped scenario is a silent hole") print(f" FAIL scenario count {n} != {expected_n}") if failures: print(f"selftest-conformance: {len(failures)} FAILURE(S) — the runner's verdicts cannot be trusted until this is green") return 1 - print(f"selftest-conformance OK: {n} scenarios — every verdict class turns red for its reason and green only for agreement") + print(f"selftest-conformance OK: {n} scenarios — every verdict class turns red for its reason and green only for agreement (and, on the ref leg, only for agreement WITH THE REFERENCE)") return 0 diff --git a/spec/wasm_cross/grain_functions.almd b/spec/wasm_cross/grain_functions.almd index 5eb8be2..005d86c 100644 --- a/spec/wasm_cross/grain_functions.almd +++ b/spec/wasm_cross/grain_functions.almd @@ -1,4 +1,10 @@ // @contract: C-292 +// @ref-allow: F1 (docs/ref/PARSER-NOTES.md) — named-argument EVALUATION ORDER +// is under adjudication: this file's own labeled_args6 comment and the plain +// reading of ALS-E26 say the written order; the implementation evaluates in +// parameter order; the reference evaluator follows the text. ALS-E26 must +// name the order; then either this fixture's comment or the implementation +// is wrong, and this directive comes off. // grain functions.re — curried_func (call-of-call), letrec_2 (mutual // recursion referencing a later definition, order-independent), named and // default arguments (labeled_args1..5, default_args1..5: reorder, omit,