diff --git a/artifacts/verification.yaml b/artifacts/verification.yaml index 0ff23dc..97e4c00 100644 --- a/artifacts/verification.yaml +++ b/artifacts/verification.yaml @@ -128,7 +128,7 @@ artifacts: fields: method: automated-test steps: - - run: cargo test -p spar-cli + - run: cargo test -p spar links: - type: satisfies target: ARCH-CLI @@ -318,6 +318,22 @@ artifacts: Eight tests verifying SVG graph output contains correct number of nodes and edges matching the instance model, with proper labels and connection endpoints. + + DEMOTED to `proposed` 2026-08-07 (#404). The step below selects NO test + in spar-wasm: nothing in that package has `topology` in its name. It + looked non-vacuous only because the guardrail matched filters against a + flat workspace-wide inventory while discarding the `-p` it had parsed — + and `topology` does match three tests, all of them in spar-solver and + spar-network. This is #388's own executed proof case, which survived + #388's fix. + + NOT repointed, deliberately. spar-wasm's nearest candidates are the FOUR + tests in `graph::tests`, and this artifact describes EIGHT covering + labels and connection endpoints — so the described evidence cannot be + located, and choosing a filter that merely selects something would assert + a relevance nobody has checked. A human should decide whether the eight + tests are to be written or the claim withdrawn. + status: proposed fields: method: automated-test steps: @@ -680,7 +696,7 @@ artifacts: fields: method: automated-test steps: - - run: cargo test -p spar-cli -- verify + - run: cargo test -p spar -- verify links: - type: verifies target: REQ-VERIFY-001 @@ -699,7 +715,7 @@ artifacts: fields: method: automated-test steps: - - run: cargo test -p spar-cli -- diff + - run: cargo test -p spar -- diff links: - type: verifies target: REQ-DIFF-001 @@ -722,7 +738,7 @@ artifacts: fields: method: automated-test steps: - - run: cargo test -p spar-cli -- mcp + - run: cargo test -p spar -- mcp links: - type: verifies target: REQ-MCP-001 diff --git a/tools/check_lean_sorries.py b/tools/check_lean_sorries.py index 5e53321..aaf4e25 100755 --- a/tools/check_lean_sorries.py +++ b/tools/check_lean_sorries.py @@ -42,8 +42,22 @@ A ratchet, the same shape as the mutants gate: -* Count every bare `sorry`, with NO comment-based exemption. A `-- TODO` is a - note to humans, not a permit. +* Count every unproven obligation, with NO comment-based exemption. A `-- TODO` + is a note to humans, not a permit. + + "Obligation" is broader than the first revision of this gate allowed, and the + widening is #385's defect (b), fixed separately from its defect (a). That + revision matched only a bare `sorry` alone on its line, so `:= by sorry`, + `:= sorry`, `admit` and `axiom cheat : 7 = 8` all reported zero — the four + forms the issue had named explicitly. Worse, its self-test contained a case + ASSERTING that a non-bare occurrence does not count, which made the hole look + deliberate. All five forms (including `sorryAx`) now count, matched over + comment-stripped text so prose still does not. + + MEASURED before widening, so this is not a latent red: the count is 12 either + way — the tree contains no inline `sorry`, no `admit`, no `axiom` and no + `sorryAx` today. The declared floor is unchanged; only the escape hatches are + closed. * Compare against `--max-sorries`, a floor declared in the workflow. * count > floor -> FAIL. New sorries cannot be admitted by writing a comment. * count < floor -> PASS, and say loudly that the floor should be lowered. That @@ -70,19 +84,76 @@ import tempfile from pathlib import Path -# A bare `sorry` on its own line, with or without a trailing comment. The -# trailing comment is CAPTURED, not excluded — that was the bug. -_SORRY = re.compile(r"^[ \t]*sorry[ \t]*(--.*)?$") - - -def scan(root: Path) -> dict[str, list[tuple[int, str]]]: - """{relative path: [(line_no, line_text)]} for every bare sorry.""" - found: dict[str, list[tuple[int, str]]] = {} +# Every way this tree can carry an unproven obligation. +# +# The first revision of this gate matched ONLY `^[ \t]*sorry[ \t]*(--.*)?$` — a +# bare `sorry` alone on its line. That fixed #385's defect (a), the self-service +# `-- TODO` exemption, and left its defect (b) untouched: the issue named +# `:= by sorry`, `:= sorry`, `admit` and `axiom` explicitly, and all four exited +# 0. The self-exemption had been replaced with a narrower one that was just as +# self-service — an author could assert a falsehood via `axiom` and the declared +# floor never moved. +# +# Detection runs over COMMENT-STRIPPED text, which is what lets the patterns be +# word-bounded rather than line-anchored: `-- mentions sorry in prose` must not +# count, and it no longer can, because the comment is gone before matching. +# +# `sorryAx` is counted separately and deliberately. It is Lean's underlying +# escape term; `\bsorry\b` does not match inside it (word boundary), so without +# its own entry it would be invisible. There are zero occurrences today, so +# counting it costs nothing now and closes the hatch later. +_OBLIGATIONS: list[tuple[str, re.Pattern[str]]] = [ + ("sorry", re.compile(r"\bsorry\b")), + ("sorryAx", re.compile(r"\bsorryAx\b")), + ("admit", re.compile(r"\badmit\b")), + # An axiom asserts its statement without proof — `axiom cheat : 7 = 8` is + # strictly worse than a `sorry`, because nothing marks the proof as + # incomplete. Anchored at line start so `Classical.axiom_of_choice`-style + # references in expressions are not swept up. + ("axiom", re.compile(r"^[ \t]*axiom[ \t]+")), +] + + +def strip_comments(text: str) -> str: + """Blank out Lean comments, preserving line structure. + + Handles nested `/- -/` blocks (Lean permits nesting) and `--` to + end-of-line. Newlines are preserved so reported line numbers stay true to + the original file. + """ + out, i, depth = [], 0, 0 + while i < len(text): + if text.startswith("/-", i): + depth += 1 + out.append(" ") + i += 2 + continue + if text.startswith("-/", i) and depth: + depth -= 1 + out.append(" ") + i += 2 + continue + if depth: + out.append("\n" if text[i] == "\n" else " ") + i += 1 + continue + out.append(text[i]) + i += 1 + return "\n".join(re.sub(r"--.*$", "", ln) for ln in "".join(out).splitlines()) + + +def scan(root: Path) -> dict[str, list[tuple[int, str, str]]]: + """{path: [(line_no, kind, original_line_text)]} for every obligation.""" + found: dict[str, list[tuple[int, str, str]]] = {} for path in sorted(root.rglob("*.lean")): - hits = [] - for n, line in enumerate(path.read_text(encoding="utf-8", errors="replace").splitlines(), 1): - if _SORRY.match(line): - hits.append((n, line.strip())) + raw = path.read_text(encoding="utf-8", errors="replace") + raw_lines = raw.splitlines() + hits: list[tuple[int, str, str]] = [] + for n, line in enumerate(strip_comments(raw).splitlines(), 1): + for kind, rx in _OBLIGATIONS: + for _ in rx.finditer(line): + original = raw_lines[n - 1].strip() if n <= len(raw_lines) else line.strip() + hits.append((n, kind, original)) if hits: found[str(path)] = hits return found @@ -103,14 +174,23 @@ def check(root: Path, max_sorries: int, out=sys.stdout) -> int: found = scan(root) total = sum(len(v) for v in found.values()) + by_kind: dict[str, int] = {} + for hits in found.values(): + for _, kind, _text in hits: + by_kind[kind] = by_kind.get(kind, 0) + 1 print("== lean-sorry guardrail ==", file=out) print(f".lean files scanned: {len(lean_files)}", file=out) - print(f"sorries found: {total} (declared floor: {max_sorries})", file=out) + print(f"obligations found: {total} (declared floor: {max_sorries})", file=out) + # Printed on every path, success included, and broken out by kind: the + # forms are not interchangeable, and a shift from `sorry` to `axiom` at a + # constant total would otherwise be invisible. + kinds = ", ".join(f"{k}={by_kind[k]}" for k, _ in _OBLIGATIONS if k in by_kind) + print(f"by kind: {kinds or '(none)'}", file=out) for path, hits in found.items(): print(f" {len(hits):3} {path}", file=out) - for n, text in hits: - print(f" :{n} {text}", file=out) + for n, kind, text in hits: + print(f" :{n} [{kind}] {text}", file=out) if total > max_sorries: print("", file=out) @@ -133,7 +213,16 @@ def check(root: Path, max_sorries: int, out=sys.stdout) -> int: def self_test() -> int: passed = failed = 0 - def case(desc: str, want: int, files: dict[str, str], floor: int) -> None: + def case(desc: str, want: int, files: dict[str, str], floor: int, + want_msg: str | None = None) -> None: + """`want_msg` pins the DIAGNOSIS, not just the exit code. + + The ratchet notice and the per-kind breakdown are output-only: deleting + either changes no verdict, so an exit-code assertion cannot tell whether + they still work. An adversarial review found exactly that — removing the + below-floor branch left 8/8 green. Anything whose whole purpose is to + say something needs a case that reads what it said. + """ nonlocal passed, failed with tempfile.TemporaryDirectory() as td: root = Path(td) @@ -143,14 +232,21 @@ def case(desc: str, want: int, files: dict[str, str], floor: int) -> None: p.write_text(body, encoding="utf-8") buf = io.StringIO() got = check(root, floor, out=buf) - if got == want: - passed += 1 - print(f" ok {desc}") - else: + text = buf.getvalue() + if got != want: failed += 1 print(f" FAIL {desc}: got {got}, want {want}") - for line in buf.getvalue().splitlines()[:6]: + for line in text.splitlines()[:6]: print(f" {line}") + elif want_msg is not None and want_msg not in text: + failed += 1 + print(f" FAIL {desc}: exit {got} correct, but the diagnosis is " + f"wrong — expected {want_msg!r}") + for line in text.splitlines()[:6]: + print(f" {line}") + else: + passed += 1 + print(f" ok {desc}") PLAIN = "theorem t : True := by\n sorry\n" TODO = "theorem t : True := by\n sorry -- TODO(v1.0.0)\n" @@ -168,15 +264,49 @@ def case(desc: str, want: int, files: dict[str, str], floor: int) -> None: case("bare sorry at floor passes", 0, {"A.lean": PLAIN}, 1) # The ratchet direction: improving must never fail. case("below floor PASSES (ratchet may be tightened, not a failure)", 0, - {"A.lean": DONE}, 3) + {"A.lean": DONE}, 3, + want_msg="lower --max-sorries to 0") # Counting across files. case("counts across multiple files", 1, {"A.lean": PLAIN, "sub/B.lean": TODO}, 1) # Broken scans must not read as clean. case("no .lean files is a broken scan, not a clean tree", 2, {"README.md": "x"}, 0) - # A `sorry` inside a word or mid-expression is not a bare sorry. - case("`sorryAx` / inline text is not a bare sorry", 0, - {"A.lean": "def sorryAx := 1\n-- mentions sorry in prose\n"}, 0) + # ── #385 defect (b): the forms the first revision could not see ── + # + # The case that used to sit here read: + # + # case("`sorryAx` / inline text is not a bare sorry", 0, + # {"A.lean": "def sorryAx := 1\n-- mentions sorry in prose\n"}, 0) + # + # It PINNED THE HOLE SHUT rather than finding it — asserting as intended + # behaviour that a non-bare occurrence does not count, at a floor of 0. The + # issue had already enumerated four forms by name; none had a case, and all + # four exited 0. A test that affirms the gap is worse than no test, because + # it makes the gap look deliberate. + case("REGRESSION #385(b): inline `:= by sorry` COUNTS", 1, + {"A.lean": "theorem cheat : 1 = 2 := by sorry\n"}, 0) + case("REGRESSION #385(b): inline `:= sorry` COUNTS", 1, + {"A.lean": "theorem cheat : 1 = 2 := sorry\n"}, 0) + case("REGRESSION #385(b): `admit` COUNTS", 1, + {"A.lean": "theorem cheat : 1 = 2 := by\n admit\n"}, 0) + case("REGRESSION #385(b): `axiom` COUNTS (asserts without proof)", 1, + {"A.lean": "axiom cheat : 7 = 8\n"}, 0, + want_msg="axiom=1") + case("REGRESSION #385(b): `sorryAx` COUNTS (the underlying escape term)", 1, + {"A.lean": "theorem cheat : 1 = 2 := sorryAx _ true\n"}, 0) + + # ...and the legitimate half of the old case still holds: prose must not + # count. This is what makes the widening safe rather than merely stricter — + # detection runs over comment-stripped text, so the word in a comment is + # gone before any pattern is applied. + case("a `sorry` mentioned in a line comment does NOT count", 0, + {"A.lean": "theorem t : True := by\n trivial -- unlike sorry, this closes\n"}, 0) + case("a `sorry` inside a /- block comment -/ does NOT count", 0, + {"A.lean": "/- we could sorry this, or:\n admit it -/\ntheorem t : True := by\n trivial\n"}, 0) + case("a nested /- /- -/ -/ block is fully stripped", 0, + {"A.lean": "/- outer /- inner sorry -/ still comment -/\ntheorem t : True := by\n trivial\n"}, 0) + case("an identifier merely CONTAINING sorry is not a bare sorry", 0, + {"A.lean": "def sorryless := 1\n"}, 0) print(f"\n{passed} passed, {failed} failed") return 1 if failed else 0 diff --git a/tools/check_verification_filters.py b/tools/check_verification_filters.py index e45fd0e..11c33dd 100755 --- a/tools/check_verification_filters.py +++ b/tools/check_verification_filters.py @@ -43,10 +43,17 @@ module::tests::name: test -The inventory is collected once per invocation and every filter is checked -against it in memory. That keeps the check O(one build) rather than O(149 -cargo invocations), and makes the decision procedure identical to libtest's -rather than an approximation of it. +The inventory is collected PER PACKAGE — `cargo test -p X --all-targets -- +--list` for each package a step names — and each filter is checked against its +own package's names in memory. The listings share one build, so this is still +O(one build) rather than O(one invocation per step). + +Per package is not a refinement, it is the correctness condition. The first +revision collected one flat workspace-wide list while parsing (and discarding) +the `-p`, so it asked "does this substring occur ANYWHERE?" where +`run_verification.py` runs "does it occur in package P?". #388's own executed +proof case survived that: `cargo test -p spar-wasm -- topology` matches three +tests, all of them in other crates (#404). A filter that selects nothing fails, naming the artifact, the step and the filter. A count is printed on every path, success included — for the same @@ -175,26 +182,71 @@ def extract_filter(cmd: str) -> tuple[str | None, str | None]: return (pkg, None) -def collect_inventory(manifest_dir: Path) -> set[str]: - """Every test name cargo knows about, via `cargo test -- --list`.""" - proc = subprocess.run( - ["cargo", "test", "--workspace", "--all-targets", "--", "--list"], - cwd=manifest_dir, - capture_output=True, - text=True, - ) - if proc.returncode != 0: - raise RuntimeError( - "cargo test --list failed; cannot build a test inventory, so no " - "filter can be judged. Refusing to report success.\n" - + proc.stderr[-2000:] - ) - return {m.group("name") for m in _LIST_LINE.finditer(proc.stdout)} +def collect_inventory(manifest_dir: Path, packages: set[str]) -> dict[str, set[str]]: + """{package: {test names}} — one listing PER PACKAGE. + The first revision collected a single flat, workspace-wide list. It also + parsed the `-p` out of each command and then never used it, so the gate + asked "does this substring occur anywhere in the workspace?" while + `run_verification.py` runs "does it occur in package P?" — strictly weaker, + and #388's own executed proof case survived it: `cargo test -p spar-wasm -- + topology` matches three tests, all of them in spar-solver and spar-network + (#404). -def check(yaml_path: Path, inventory: set[str], out=sys.stdout) -> int: + Listing per package costs 10 invocations here, but they share one build, and + it is the same question the consumer asks. A gate that answers an easier + question than the thing it guards is the defect this whole requirement is + about. + """ + inv: dict[str, set[str]] = {} + for pkg in sorted(packages): + proc = subprocess.run( + ["cargo", "test", "-p", pkg, "--all-targets", "--", "--list"], + cwd=manifest_dir, + capture_output=True, + text=True, + ) + if proc.returncode != 0: + # Two different failures, and they deserve different reports. + # + # "did not match any packages" means the artifact names a package + # that does not exist — a finding ABOUT that artifact. Omit it from + # the inventory so `check()` can name the affected artifacts and + # exit 2, rather than dying here with a traceback that names only + # the first one. (The live instance: four steps said + # `-p spar-cli`, but `crates/spar-cli/Cargo.toml` declares + # `name = "spar"` and no package `spar-cli` exists. The old flat + # inventory never ran `-p`, so it never noticed.) + # + # Anything else is a broken build, which invalidates every verdict, + # not one artifact's — that stays fatal. + if "did not match any packages" in proc.stderr: + continue + raise RuntimeError( + f"cargo test -p {pkg} --list failed; cannot build a test " + f"inventory for it, so its filters cannot be judged. Refusing " + f"to report success.\n" + proc.stderr[-2000:] + ) + names = {m.group("name") for m in _LIST_LINE.finditer(proc.stdout)} + # An empty list from a SUCCESSFUL cargo run is a truthful answer, not a + # broken scan: some packages genuinely have no tests (a proc-macro crate + # typically does not). Keeping the empty set is also the useful + # behaviour — any filter on such a package selects nothing, which is a + # real finding, and reporting it as one beats dying. + # + # A broken scan is still caught, twice over: a non-zero cargo exit is + # fatal above, and `check()` exits 2 if the union across all packages is + # empty. + if not names: + print(f"note: package {pkg} lists zero tests", file=sys.stderr) + inv[pkg] = names + return inv + + +def check(yaml_path: Path, inventory: dict[str, set[str]], out=sys.stdout) -> int: steps = parse_steps(yaml_path.read_text(encoding="utf-8")) - filtered: list[tuple[str, str, str, str]] = [] + # (artifact id, status, command, filter, package) + filtered: list[tuple[str, str, str, str, str | None]] = [] whole_pkg = 0 other = 0 for aid, status, cmd in steps: @@ -204,13 +256,31 @@ def check(yaml_path: Path, inventory: set[str], out=sys.stdout) -> int: elif filt is None: whole_pkg += 1 else: - filtered.append((aid, status, cmd, filt)) + filtered.append((aid, status, cmd, filt, pkg)) + + # Each filter is judged against ITS OWN package's inventory, not the + # workspace's. `libtest` filters are substring matches over the test paths + # *of the binary being run*, and `cargo test -p X` runs only X's binaries — + # so a filter matching a test in another crate selects nothing here (#404). + # A step with no `-p` really does run everything, so it uses the union. + union: set[str] = set() + for names in inventory.values(): + union |= names + + def pool_for(pkg: str | None) -> set[str] | None: + return union if pkg is None else inventory.get(pkg) + unlistable = [e for e in filtered if pool_for(e[4]) is None] empty = [ - (aid, status, cmd, filt) - for aid, status, cmd, filt in filtered - if not any(filt in name for name in inventory) + e for e in filtered + if (pool := pool_for(e[4])) is not None + and not any(e[3] in name for name in pool) ] + for aid, _status, _cmd, filt, pkg in unlistable: + # No inventory for the named package means the question could not be + # asked. "Could not judge" must not read as "fine". + print(f"::error::{aid}: no test inventory for package {pkg!r}, so its " + f"filter {filt!r} cannot be judged", file=out) # `` is NOT lenient. An artifact whose status this reader cannot find # is unclassifiable, and an unclassifiable artifact with a filter that # selects nothing is exactly the case that must not pass quietly. Same @@ -225,12 +295,14 @@ def check(yaml_path: Path, inventory: set[str], out=sys.stdout) -> int: print(f" cargo test + filter: {len(filtered)}", file=out) print(f" cargo test, whole pkg: {whole_pkg}", file=out) print(f" not a cargo test: {other}", file=out) - print(f"test names in inventory: {len(inventory)}", file=out) + print(f"packages inventoried: {len(inventory)}" + f" ({', '.join(f'{p}={len(n)}' for p, n in sorted(inventory.items()))})", file=out) + print(f"test names, all packages: {len(union)}", file=out) print(f"filters selecting nothing: {len(empty)}", file=out) print(f" claiming evidence (FAIL): {len(vacuous)}", file=out) print(f" proposed/draft (ok): {len(planned)}", file=out) - if not inventory: + if not union: print( "::error::the test inventory is empty, so every filter would look " "vacuous. That is a broken scan, not a finding.", @@ -238,17 +310,29 @@ def check(yaml_path: Path, inventory: set[str], out=sys.stdout) -> int: ) return 2 - for aid, status, cmd, filt in planned: + # A step whose package could not be inventoried is unjudgeable, and + # unjudgeable must not read as fine. Errors were already printed above. + if unlistable: + print(f"\n{len(unlistable)} filtered step(s) name a package with no " + f"inventory — refusing to report success over an unasked question.", + file=out) + return 2 + + for aid, status, cmd, filt, pkg in planned: print(f" note: {aid} ({status}) plans a test that does not exist yet: {filt!r}", file=out) if vacuous: print("", file=out) - for aid, status, cmd, filt in vacuous: - print(f"::error::{aid} (status={status}): filter {filt!r} selects no test", file=out) + for aid, status, cmd, filt, pkg in vacuous: + scope = f"package {pkg}" if pkg else "the workspace" + print(f"::error::{aid} (status={status}): filter {filt!r} selects no " + f"test in {scope}", file=out) print(f" step: {cmd}", file=out) print( "\nA filter that matches nothing exits 0. These steps have been " - "scored as passing without running anything.", + "scored as passing without running anything. Note the scope: a " + "filter matching a test in a DIFFERENT package still selects " + "nothing here, because `cargo test -p X` runs only X's binaries.", file=out, ) return 1 @@ -267,23 +351,48 @@ def self_test() -> int: passed = failed = 0 - def case(desc: str, want: int, yaml_text: str, inv: set[str]) -> None: + def case(desc: str, want: int, yaml_text: str, inv: dict[str, set[str]], + want_msg: str | None = None) -> None: + """`want_msg` pins the DIAGNOSIS as well as the exit code. + + Several distinct broken inputs reach the same exit code by different + routes — an empty inventory and an un-inventoried package both exit 2 — + so asserting the code alone cannot say which check fired, and removing + either leaves the suite green. Pinning the message is what makes each + branch load-bearing. + """ nonlocal passed, failed with tempfile.TemporaryDirectory() as td: p = Path(td) / "v.yaml" p.write_text(yaml_text, encoding="utf-8") buf = io.StringIO() got = check(p, inv, out=buf) - if got == want: - passed += 1 - print(f" ok {desc}") - else: + text = buf.getvalue() + if got != want: failed += 1 print(f" FAIL {desc}: got {got}, want {want}") - for line in buf.getvalue().splitlines()[:6]: + for line in text.splitlines()[:6]: + print(f" {line}") + elif want_msg is not None and want_msg not in text: + failed += 1 + print(f" FAIL {desc}: exit {got} correct, but the diagnosis is " + f"wrong — expected {want_msg!r}") + for line in text.splitlines()[:6]: print(f" {line}") + else: + passed += 1 + print(f" ok {desc}") - INV = {"render::tests::render_basic_aadl", "graph::tests::test_graph_with_connections"} + # Inventories are PER PACKAGE, because that is the scope `cargo test -p X` + # actually searches. `spar-solver` deliberately owns a test whose name would + # match a spar-wasm filter — that is the #404 counterexample, and under the + # old flat inventory it made a vacuous filter look fine. + INV = { + "spar-wasm": {"render::tests::render_basic_aadl", + "graph::tests::test_graph_with_connections"}, + "spar-solver": {"tests::topology_is_deterministic"}, + "spar-parser": {"parse::tests::basic"}, + } Y_GOOD = """artifacts: - id: TEST-OK @@ -325,13 +434,54 @@ def case(desc: str, want: int, yaml_text: str, inv: set[str]) -> None: print("check_verification_filters self-test") # The bug itself. case("REGRESSION #388: filter selecting nothing must FAIL", 1, Y_BAD, INV) + # THE #404 COUNTEREXAMPLE. `topology` matches a real test — in spar-solver, + # not in the spar-wasm this step runs. Under the old flat workspace + # inventory this passed, which is how #388's own executed proof case stayed + # green after #388 was closed. + Y_CROSS = """artifacts: + - id: TEST-STPA-SVG-TOPOLOGY + status: implemented + fields: + steps: + - run: cargo test -p spar-wasm -- topology +""" + case("REGRESSION #404: a filter matching another PACKAGE's test is vacuous", + 1, Y_CROSS, INV) + # ...and the same filter is fine when the step names the package that owns + # the test. Distinct inputs, distinct outputs: a checker that ignored `-p` + # gives both the same verdict and cannot fail the first. + case("...and it PASSES when -p names the package that owns the test", + 0, Y_CROSS.replace("spar-wasm", "spar-solver"), INV) + # A package nobody could list is unjudgeable, which must not read as fine. + case("a step naming an un-inventoried package is CANNOT-JUDGE, not a pass", + 2, Y_GOOD.replace("spar-wasm", "spar-ghost"), INV) + # ...and it names the artifact rather than dying, which is what turns a + # traceback into a finding. LIVE INSTANCE: four steps said `-p spar-cli` + # while `crates/spar-cli/Cargo.toml` declares `name = "spar"`. + case("...and it NAMES the artifact and package", 2, + Y_GOOD.replace("spar-wasm", "spar-ghost"), INV, + want_msg="no test inventory for package 'spar-ghost'") # Normal operation. case("filter selecting a real test passes", 0, Y_GOOD, INV) case("whole-package step is never vacuous", 0, Y_WHOLE, INV) + # ...and it needs no inventory at all. `spar-parser` is deliberately absent + # from INV here: a whole-package step selects everything, so demanding an + # inventory for it is work nothing consumes. The live instance was + # `cargo test -p spar-verify-macros` — a proc-macro crate with zero tests + # that no filter asks about, which made the gate fatal on a package it did + # not need. + case("...and needs no inventory for its package", 0, Y_WHOLE, + {k: v for k, v in INV.items() if k != "spar-parser"}) + # A package that genuinely has no tests is a truthful empty answer, and a + # filter on it selects nothing — a finding, not a crash. + case("a filter on a package with zero tests is vacuous, not fatal", 1, + Y_GOOD, {**INV, "spar-wasm": set()}, + want_msg="selects no test in package spar-wasm") case("non-cargo step is counted, not judged", 0, Y_OTHER, INV) case("one good + one vacuous still fails", 1, Y_MIXED, INV) # Broken scan must not read as clean. - case("empty inventory is a broken scan, not a pass", 2, Y_GOOD, set()) + case("empty inventory is a broken scan, not a pass", 2, Y_GOOD, {}, + want_msg="the test inventory is empty") # Status semantics: a plan is not a false claim. case("proposed artifact planning a future test PASSES", 0, Y_PLANNED, INV) case("NO status is unclassifiable, so it fails closed", 1, @@ -341,6 +491,15 @@ def case(desc: str, want: int, yaml_text: str, inv: set[str]) -> None: # Substring semantics, which is what libtest does. case("filter matching as a SUBSTRING passes", 0, Y_GOOD.replace("render_basic", "basic_aadl"), INV) + # A `::`-bearing filter, because 16 of the 60 real filters carry one and no + # case did. The discriminator: the FULL filter must be matched, not its last + # segment. Here `nonexistent::render_basic` selects nothing even though + # `render_basic` alone would — a checker that split on `::` and matched only + # the tail would pass this and could not fail it. + case("a `::` filter is matched WHOLE, not by its last segment", 1, + Y_GOOD.replace("render_basic", "nonexistent::render_basic"), INV) + case("...and a real module-path filter still passes", 0, + Y_GOOD.replace("render_basic", "render::tests::render_basic"), INV) case("near-miss substring still fails", 1, Y_GOOD.replace("render_basic", "render_basicX"), INV) # A QUOTED step is YAML syntax, not part of the filter. The first run of @@ -375,11 +534,31 @@ def main() -> int: a = ap.parse_args() if a.self_test: return self_test() + verification = Path(a.verification) if a.inventory_json: - inv = set(json.loads(Path(a.inventory_json).read_text(encoding="utf-8"))) + # {"pkg": ["name", ...]} — a flat array is no longer accepted, because a + # flat inventory is exactly the defect (#404): it cannot express which + # package owns a test, so every filter is judged against the wrong pool. + raw = json.loads(Path(a.inventory_json).read_text(encoding="utf-8")) + if not isinstance(raw, dict): + print("::error::--inventory-json must be an object mapping package " + "-> [test names]. A flat list cannot say which package owns a " + "test, which is the #404 defect.", file=sys.stderr) + return 2 + inv = {pkg: set(names) for pkg, names in raw.items()} else: - inv = collect_inventory(Path(a.manifest_dir)) - return check(Path(a.verification), inv) + # Only packages named by a step that HAS a filter. A whole-package step + # (`cargo test -p X` with no `--`) selects everything and can never be + # vacuous, so building an inventory for it is work nothing consumes — + # and it made the gate fatal on `spar-verify-macros`, a proc-macro crate + # with no tests that no filter ever asks about. + packages = set() + for _aid, _status, cmd in parse_steps(verification.read_text(encoding="utf-8")): + pkg, filt = extract_filter(cmd) + if pkg is not None and filt is not None: + packages.add(pkg) + inv = collect_inventory(Path(a.manifest_dir), packages) + return check(verification, inv) if __name__ == "__main__":