diff --git a/.github/aspice-unmodelled-levels.txt b/.github/aspice-unmodelled-levels.txt new file mode 100644 index 0000000..d214525 --- /dev/null +++ b/.github/aspice-unmodelled-levels.txt @@ -0,0 +1,23 @@ +# ASPICE process levels scry deliberately does NOT model, one per line as +# `: `. A reason is REQUIRED — see FEAT-088's rule 2: a +# flag with no justification is what a forgotten gap looks like once somebody +# notices the number. +# +# WHY A FILE AT ALL. The `aspice` preset is EMBEDDED and a project cannot +# subset its rules, so `rivet coverage` emits rules for levels this project +# does not model and renders an EMPTY population as 100.0%. Four of seventeen +# rules currently report success for work that was never done. The weighted +# overall is honest (an empty rule adds 0 to both sides, 119/135 = 88.1%), so +# the aggregate is safe to gate on and the per-row display is not. +# +# tools/check-undeveloped-goals.py reads this and fails BOTH directions: +# - an empty coverage population NOT listed here -> undeclared gap +# - a type listed here whose population is NOT empty -> stale entry +# The second is what keeps this file honest rather than append-only, and it is +# what would catch a rivet upgrade adding a level we never populate. +# +# The 0/0 -> 100% rendering is rivet's, not scry's. Reported upstream. + +sw-arch-component: SWE.2 software architectural design. scry's architecture is the 13-crate decomposition, already tracked in the dev FEAT/DD spine; restating it as ASPICE architecture elements would add structure without adding evidence. +sw-detail-design: SWE.3 software detailed design. No detailed-design step exists in this project's process — code is written against typed requirements and gated by oracles, so a detail-design layer would be written after the fact to fill a row. +unit-verification: SWE.4 unit verification. scry's unit tests are real (332 in CI) but they verify sw-reqs via SWE.6, not detail-design elements; authoring one unit-verification artifact per absent detail-design element would be fabricated traceability. FEAT-033's governing principle is "no fabricated DAL". diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index c14b7d0..799a1e6 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -261,7 +261,14 @@ jobs: # declaration must be justified. Ships a --self-test, run FIRST, which # includes the subtle case (flag present, no justification naming it) -- # the shape a forgotten goal takes once someone quiets the report. - - name: Guard — an unsupported safety goal is DECLARED and justified + # Two populations, ONE rule: an absent thing must be DECLARED and + # JUSTIFIED. Safety goals were the first. The second is coverage rules + # whose population is EMPTY -- rivet renders those as 100.0%, and four + # of scry's seventeen currently do, because the `aspice` preset is + # embedded and a project cannot subset its rules. Checked in BOTH + # directions against .github/aspice-unmodelled-levels.txt so the file + # cannot become an append-only suppression list. + - name: Guard — an absent goal or coverage level is DECLARED and justified run: | python3 tools/check-undeveloped-goals.py --self-test python3 tools/check-undeveloped-goals.py diff --git a/artifacts/aspice-vmodel.yaml b/artifacts/aspice-vmodel.yaml index 7b8c1f7..64c1622 100644 --- a/artifacts/aspice-vmodel.yaml +++ b/artifacts/aspice-vmodel.yaml @@ -7,9 +7,41 @@ # (SYS.2) → sw-req (SWE.1), with sys-verification (SYS.5) and sw-verification # (SWE.6) measures naming the REAL tests / Rocq proofs / MC-DC gate / host # tests / clean-room that discharge each requirement. Mirrors the meld/spar -# house pattern (dev + aspice schemas side by side). The sw-reqs restate the -# dev the dev requirement..013 as software requirements; the verification mapping is the -# authoritative one (the dev REQ-* carry no verifies link by construction). +# house pattern (dev + aspice schemas side by side). SR-1..SR-13 restate dev +# REQ-001..REQ-013 as software requirements (one for one, checked by title) and +# derive structurally from the SYS-* system requirements; the verification +# mapping is the authoritative one (the dev REQ-* carry no verifies link by +# construction). +# +# SCOPE, STATED BY EXCLUSION AND NOT ONLY BY ENUMERATION. Three ASPICE levels +# are DELIBERATELY NOT MODELLED here: SWE.2 (software architectural design), +# SWE.3 (software detailed design) and SWE.4 (unit verification). MEASURED: +# zero artifacts of type sw-arch-component, sw-detail-design or +# unit-verification exist anywhere under artifacts/, and zero textual +# occurrences of those type names. +# +# That is a choice, not an oversight. scry's design intent already lives in the +# dev REQ/FEAT/DD spine; a parallel ASPICE architecture and detailed-design +# decomposition would restate the crate structure without adding evidence, and +# authoring a unit-verification artifact per detail-design element would be +# fabricated traceability. FEAT-033's governing principle is "no fabricated +# DAL", and it applies to process levels exactly as to integrity levels. +# +# THE COST IS FOUR VACUOUS GREENS, so read `rivet coverage` knowing it. The +# aspice preset is EMBEDDED and a project cannot subset its rules, so the +# report carries rules for levels this project does not model and renders an +# empty population as success: +# +# swe2-allocated-from-swe1 sw-arch-component 0/0 100.0% +# swe3-refines-swe2 sw-detail-design 0/0 100.0% +# swe4-verifies-swe3 unit-verification 0/0 100.0% +# swe3-has-verification sw-detail-design 0/0 100.0% +# V-closure: sw-detail-design (all 2 rules) 100.0% [0/0] +# +# Those 100%s mean "nothing to check", NOT "checked". The weighted overall does +# NOT inherit it -- 119/135 = 88.1%, and an empty rule adds 0 to both sides -- +# so `rivet coverage --fail-under` keys off an honest number (VERIFIED in both +# directions: --fail-under 88.2 exits 1, --fail-under 88.0 exits 0). # ───────────────────────────────────────────────────────────────────────── artifacts: diff --git a/artifacts/roadmap-2.0.yaml b/artifacts/roadmap-2.0.yaml index 6a06de8..ae458b2 100644 --- a/artifacts/roadmap-2.0.yaml +++ b/artifacts/roadmap-2.0.yaml @@ -1743,6 +1743,46 @@ artifacts: acceptance-criteria: - "Given the ASPICE V-model, When `rivet validate` runs, Then every sw-req derives from a system-req (← stakeholder-req) and is verified by at least one sw-verification, and every system-req by a sys-verification — the right side of the V is closed." - "Given each sw-verification, When read, Then its description names a verification measure that actually exists in the repo (a test function, a proofs/rocq/*.v file, the MC/DC gate, or a host test) and genuinely discharges the linked sw-req — no fabricated evidence." + residual: > + SCOPE IS STATED BY ENUMERATION AND NOT BY EXCLUSION, which is why this + residual exists at all -- it was written on 2026-08-28, long after the + feature was accepted with no residual at all. + + The V-model this feature built covers SYS.1 -> SYS.2 -> SWE.1 with SYS.5 + and SWE.6 verification. It does NOT model SWE.2 (software architectural + design), SWE.3 (software detailed design) or SWE.4 (unit verification). + MEASURED 2026-08-28: zero artifacts of type sw-arch-component, + sw-detail-design or unit-verification exist anywhere under artifacts/, + and zero textual occurrences of those type names. + + That is deliberate. Design intent already lives in the dev REQ/FEAT/DD + spine; a parallel ASPICE architecture and detailed-design decomposition + would restate the crate structure without adding evidence, and a + unit-verification artifact per detail-design element would be fabricated + traceability. This feature's own governing principle is "no fabricated + DAL", and it applies to process levels exactly as to integrity levels. + The right response to an empty level is to say it is empty, not to fill + it. + + THE COST, AND WHY IT COULD MISLEAD AN ASSESSOR. The aspice preset is + EMBEDDED and a project cannot subset its rules, so `rivet coverage` + emits rules for levels scry does not model and renders an EMPTY + population as SUCCESS -- four rules at 100.0% over 0/0 + (swe2-allocated-from-swe1, swe3-refines-swe2, swe4-verifies-swe3, + swe3-has-verification), plus the summary line + `V-closure: sw-detail-design (all 2 rules) 100.0% [0/0]`. Read row by + row, four of seventeen rules report success for work that was never + done. This is scry#117's class -- an accurate metric over the wrong + population -- appearing in the traceability report rather than in a gate. + + The weighted overall does NOT inherit the defect: it is 119/135 = 88.1% + and an empty rule contributes 0 to both numerator and denominator, so + `rivet coverage --fail-under` keys off an honest number. VERIFIED in + both directions: --fail-under 88.2 exits 1, --fail-under 88.0 exits 0. + So the aggregate is safe to gate on and the per-row display is not. + + The 0/0 -> 100% rendering is rivet's, not scry's, and scry cannot opt + out of the rules; reported upstream rather than worked around here. links: - type: satisfies target: REQ-005 diff --git a/artifacts/roadmap-v3.4-aspice-scope.yaml b/artifacts/roadmap-v3.4-aspice-scope.yaml new file mode 100644 index 0000000..8c4997d --- /dev/null +++ b/artifacts/roadmap-v3.4-aspice-scope.yaml @@ -0,0 +1,99 @@ +# v3.4.0 addendum — own file per scry#143 fix (1). +artifacts: + - id: FEAT-097 + type: feature + title: "v3.4 — The ASPICE V-model says which levels it does NOT model, and four vacuous 100%s stop reading as success" + status: accepted + release: v3.4.0 + description: > + `rivet coverage` reports seventeen rules. FOUR of them report 100.0% over + an EMPTY population: swe2-allocated-from-swe1 (sw-arch-component), + swe3-refines-swe2 and swe3-has-verification (sw-detail-design), and + swe4-verifies-swe3 (unit-verification). The summary carries it too, as + `V-closure: sw-detail-design (all 2 rules) 100.0% [0/0]`. + + MEASURED: zero artifacts of those three types exist anywhere under + artifacts/, and zero textual occurrences of the type names — so this is + not a vocabulary artifact of the kind that produced the false scry#113 + claim. Four of seventeen rows announce success for work never done. + + FEAT-033 built this V-model and stated its scope BY ENUMERATION — + "stakeholder-req (SYS.1) -> system-req (SYS.2) -> sw-req (SWE.1), with + SYS.5 and SWE.6 verification". It never stated what it OMITS, and its + residual was empty. An enumerated scope reads as complete to anyone who + does not already know which rungs an ASPICE V has. + + THE OMISSION IS CORRECT AND STAYS. Design intent already lives in the dev + REQ/FEAT/DD spine; an ASPICE architecture and detailed-design + decomposition would restate the crate structure without adding evidence, + and a unit-verification artifact per absent detail-design element would be + fabricated traceability. FEAT-033's governing principle is "no fabricated + DAL" and it applies to process levels exactly as to integrity levels. The + right response to an empty level is to say it is empty. + + WHOSE DEFECT IS WHICH, discriminated before building. The `aspice` preset + is EMBEDDED and a project cannot subset its rules, so scry cannot decline + the four rules; the 0/0 -> 100% RENDERING is rivet's and is reported + upstream. What is scry's is the undeclared scope, and that is what this + feature fixes. The weighted overall is NOT affected — 119/135 = 88.1%, + an empty rule adding 0 to both sides — so `rivet coverage --fail-under` + keys off an honest number and needs no parser. + + NO SIXTH GATE. The rule already exists: FEAT-088's + `check-undeveloped-goals.py` enforces "an absent thing must be DECLARED + and JUSTIFIED" over safety goals. Empty coverage rules are a second + population under the same rule, so the tool was extended rather than + duplicated — two pure functions and eleven self-test cases against a + declaration file, versus a new 250-line tool with the same shape. + tags: [traceability, aspice, v-model, gate, honesty, v3.4] + fields: + phase: phase-3 + acceptance-criteria: + - "Given a coverage rule whose population is EMPTY and whose source type is not declared, When the gate runs, Then it FAILS naming the rule and the type. MUTATION-CHECKED against real data: removing `unit-verification` from the declaration file exits 1 naming `swe4-verifies-swe3 at 100% over 0/0`." + - "Given a declared type whose population is NOT empty, When the gate runs, Then it FAILS as a STALE entry. This is the direction that stops the file becoming an append-only suppression list. MUTATION-CHECKED: declaring `safety-goal` (5 rows) exits 1." + - "Given a declaration with no reason, When the gate runs, Then it FAILS — an unjustified declaration is what a forgotten gap looks like once somebody notices the number. This is FEAT-088's rule 2, which is the rule that matters. MUTATION-CHECKED: a reasonless entry exits 1 with the file and line." + - "Given the declaration file is missing, or `rivet coverage` fails, or it returns no rules, When the gate runs, Then it FAILS CLOSED. Inability to check is not evidence of correctness (scry#141). MUTATION-CHECKED: deleting the file exits 1." + - "THE CASE THAT JUSTIFIES BUILDING IT AT ALL. Given a future rivet upgrade introduces a rule over a level scry never populates, When the gate runs, Then it FAILS rather than adding a fifth silent 100%. The schema is pinned at aspice@0.2.0, so this is a real future event and not a hypothetical. MUTATION-CHECKED by injecting a synthetic `swe5-new-rule` at 0/0 over an undeclared type: exit 1 naming it." + - "Given a type that has one EMPTY rule and one POPULATED rule, When the gate runs, Then it is NOT treated as empty and no declaration is demanded. The naive `any(total == 0)` reading would wrongly demand one. Self-tested." + - "Given a declared type that NO coverage rule mentions at all, When the gate runs, Then it WARNS and does NOT fail. CORRECTED IN REVIEW, and the original self-test had LOCKED THE DEFECT IN by asserting a violation. That state means the preset DROPPED the rule — the same upgrade this gate exists for, seen from the other side — so the declaration (`scry does not model SWE.3`) is still TRUE, merely no longer observable, and no vacuous 100% can result because the rule is gone. Failing would demand deleting a correct statement to get the build green: the Class-5 shape, a guard right about the fact and wrong about the remedy. MUTATION-CHECKED by filtering every sw-detail-design rule out of the live report: exit 0 with the warning." + - "Given the split between failing and warning, When the self-test runs, Then BOTH channels are asserted separately — a split that silently dropped one side would be invisible from the violation counts alone. Three warn-channel cases: absent-from-rule-set warns exactly once, a POPULATED stale entry fails and does not warn, and a correctly declared empty population does neither." + - "Given FEAT-033, When read, Then its residual states which ASPICE levels are unmodelled, why, and what it costs in the coverage report — where before it had NO residual at all. The V-model file states scope by exclusion as well as by enumeration." + - "SELF-TESTED, run BEFORE the real check in CI: 20 cases, up from 6 — the original 6 over safety goals, 7 over `check_coverage()`'s violation channel, 3 over its warning channel, and 4 over the declaration-file parser including that a reason containing a colon survives." + - "Given the required-check set, When this lands, Then it is UNCHANGED at 12 — the guard is a step on the already-required `Rivet artifact validation` job, so it binds on merge with no post-merge ruleset edit to forget (scry#130). VERIFIED with `--against-file`." + residual: > + THIS DOES NOT MAKE THE FOUR 100%s DISAPPEAR. `rivet coverage` still + prints them, and a reader who does not open the declaration file still + sees four green rows. The gate guarantees the emptiness is DECLARED and + JUSTIFIED, not that the report is legible. Making 0/0 render as "n/a" + rather than 100% is rivet's to fix and is reported upstream. + + THE `traces-to FEAT-088` LINK WAS ADDED TO SILENCE A LINTER, and that is + worth stating rather than hiding. rivet warns when prose names an + artifact with no typed link — a good warning, and the same defect + FEAT-096 gated one level up — but the real relation is "extends its + tool with a second population", which no predicate expresses. Verified + inert: no tool reads `traces-to`, and `check-release-ordering.py` reads + only `depends-on`, so it creates no ordering edge. + + IT CHECKS TYPES, NOT LEVELS. A rule whose population is non-empty but + WRONG — one token artifact of a type, satisfying the rule at 100% with + no real decomposition behind it — passes silently. That is the scry#117 + class again and this gate does not reach it; only reading the artifacts + does. + + The three declared levels are declared for THIS project's process. If + scry ever adopts a real detailed-design step, the entries become stale + and the gate goes red until they are removed — which is the intended + pressure, but it does mean adopting SWE.3 has a gate to satisfy. + + FEAT-033 stays `accepted`. Its acceptance criteria were met; what was + missing was disclosure, which is now written. Re-opening a shipped + feature to add a residual it should have had is the honest repair, not + a status change. + links: + - type: traces-to + target: REQ-005 + - type: traces-to + target: FEAT-033 + - type: traces-to + target: FEAT-088 diff --git a/tools/check-undeveloped-goals.py b/tools/check-undeveloped-goals.py index c261f1a..fd6c5ed 100755 --- a/tools/check-undeveloped-goals.py +++ b/tools/check-undeveloped-goals.py @@ -22,6 +22,29 @@ NOT WHAT THIS DOES: it does not make `rivet coverage`'s 40% meaningful. That figure still counts declared-undeveloped goals as uncovered and still prints 40%. This gate closes one direction only -- forgotten hiding among declared. + +SECOND POPULATION, SAME RULE (2026-08-28). The rule above generalises: AN +ABSENT THING MUST BE DECLARED AND JUSTIFIED. Safety goals are one population; +EMPTY COVERAGE RULES are another, and they fail in the more dangerous +direction because rivet renders an empty population as SUCCESS. + +MEASURED: four of seventeen rules report 100.0% over 0/0 -- +swe2-allocated-from-swe1, swe3-refines-swe2, swe4-verifies-swe3 and +swe3-has-verification -- plus the summary line +`V-closure: sw-detail-design (all 2 rules) 100.0% [0/0]`. Read row by row, +four rules announce success for work that was never done. scry cannot opt out: +the `aspice` preset is EMBEDDED and a project cannot subset its rule set. + +The weighted overall does NOT inherit it (119/135 = 88.1%; an empty rule adds +0 to both sides), verified by `--fail-under 88.2` exiting 1 and `88.0` exiting +0. So the aggregate is safe to gate on and the per-row display is not. + +Checked in BOTH directions against `.github/aspice-unmodelled-levels.txt`: +an empty population not listed there is an undeclared gap; a listed type whose +population is NOT empty is a stale entry and also fails. The second direction +is what stops the file becoming append-only, and it is what would catch a +rivet upgrade introducing a level we never populate -- which is the real +future event here, since the schema is pinned at aspice@0.2.0. """ import sys, json, glob, subprocess, tempfile, os @@ -91,6 +114,72 @@ def check(arts): return bad, goals +DECL_PATH = ".github/aspice-unmodelled-levels.txt" + + +def load_declared(text): + """-> {source_type: reason}. Pure. A reason is REQUIRED (FEAT-088 rule 2).""" + out, bad = {}, [] + for i, line in enumerate(text.split("\n"), 1): + line = line.strip() + if not line or line.startswith("#"): + continue + if ":" not in line: + bad.append(f"{DECL_PATH}:{i}: no `: ` separator") + continue + k, v = line.split(":", 1) + if not v.strip(): + bad.append(f"{DECL_PATH}:{i}: `{k.strip()}` declared with NO reason -- " + f"an unjustified declaration is what a forgotten gap looks like") + continue + out[k.strip()] = v.strip() + return out, bad + + +def check_coverage(rules, declared): + """-> list of violations. Pure: the self-test drives this too. + + BOTH directions. An empty population that is not declared is an undeclared + gap wearing a 100%. A declared type whose population is NOT empty is a + stale entry -- that direction is what keeps the file from becoming an + append-only suppression list, and is the one that fires on a rivet upgrade. + """ + empty, nonempty = set(), set() + for r in rules: + st = r.get("source_type") + if st is None: + continue + (empty if r.get("total") == 0 else nonempty).add(st) + # A type is only genuinely empty if NO rule over it has rows. + empty -= nonempty + known = empty | nonempty + + bad, warn = [], [] + for st in sorted(empty - set(declared)): + names = sorted(r.get("name") for r in rules + if r.get("source_type") == st and r.get("total") == 0) + bad.append(f"coverage population `{st}` is EMPTY, so rivet reports " + f"{', '.join(names)} at 100% over 0/0 -- populate it, or declare " + f"it in {DECL_PATH} with a reason") + for st in sorted(set(declared) & nonempty): + bad.append(f"`{st}` is declared unmodelled in {DECL_PATH} but its population " + f"is NOT empty -- remove the entry; a stale declaration makes the " + f"file a suppression list instead of a claim") + # A declared type that no rule mentions AT ALL is a different situation and + # must NOT fail. It happens when the preset drops a rule -- exactly the + # upgrade this gate exists for, seen from the other side. The declaration + # ("scry does not model SWE.3") is STILL TRUE, merely no longer observable, + # and no vacuous 100% can result because the rule is gone. Failing here + # would demand deleting a correct statement to get the build green, which + # is the Class-5 shape: a guard that is right about the fact and wrong + # about the remedy. + for st in sorted(set(declared) - known): + warn.append(f"`{st}` is declared unmodelled but NO coverage rule mentions it " + f"-- the rule set changed (a preset upgrade?). The declaration may " + f"still be true; it is simply no longer enforceable here.") + return bad, warn + + def self_test(): """Feed the checker inputs it MUST reject, and one it must accept.""" ok = lambda a: check(a)[0] @@ -125,6 +214,70 @@ def self_test(): got = len(ok(prose)) print(f" [{'ok' if got==0 else 'SELF-TEST FAILED'}] prose-only justification counts: {got} violation(s), expected 0") failed += got != 0 + + # ---- second population: empty coverage rules ---- + R = lambda n, st, tot: {"name": n, "source_type": st, "total": tot} + cov_cases = [ + ("healthy: every rule has rows", + [R("a", "x", 5), R("b", "y", 3)], {}, 0), + ("REJECT: an empty population that is NOT declared", + [R("a", "x", 5), R("b", "y", 0)], {}, 1), + ("healthy: the same empty population, DECLARED", + [R("a", "x", 5), R("b", "y", 0)], {"y": "reason"}, 0), + # The direction that keeps the file from becoming append-only, and the + # one that fires when a rivet upgrade populates a level we declared. + ("REJECT: a STALE declaration whose population is not empty", + [R("a", "x", 5)], {"x": "reason"}, 1), + # CORRECTED 2026-08-28: this case originally asserted 1 violation, which + # LOCKED IN a defect. A declared type that no rule mentions means the + # PRESET DROPPED THE RULE -- the very upgrade MUT5 exists for, seen from + # the other side. The declaration is still true and no vacuous 100% can + # result, so failing would demand deleting a correct statement to go + # green. It warns instead. + ("a declared type absent from the rule set does NOT fail", + [R("a", "x", 5)], {"zzz": "reason"}, 0), + # A type with one empty rule and one populated rule is NOT empty; the + # naive `any total==0` reading would wrongly demand a declaration. + ("a type with one empty and one populated rule is not empty", + [R("a", "x", 0), R("b", "x", 4)], {}, 0), + ("two undeclared empty populations are both reported", + [R("a", "x", 0), R("b", "y", 0)], {}, 2), + ] + for name, rules, decl, want in cov_cases: + got = len(check_coverage(rules, decl)[0]) + st = "ok" if got == want else "SELF-TEST FAILED" + failed += got != want + print(f" [{st}] {name}: {got} violation(s), expected {want}") + + # The warn channel is a real output and needs its own assertions -- a split + # that silently dropped one side would look identical from the fail counts. + warn_cases = [ + ("absent-from-rule-set WARNS (exactly once)", + [R("a", "x", 5)], {"zzz": "r"}, 1), + ("a POPULATED stale entry fails and does NOT warn", + [R("a", "x", 5)], {"x": "r"}, 0), + ("a correctly declared empty population neither fails nor warns", + [R("a", "x", 0)], {"x": "r"}, 0), + ] + for name, rules, decl, want in warn_cases: + got = len(check_coverage(rules, decl)[1]) + st = "ok" if got == want else "SELF-TEST FAILED" + failed += got != want + print(f" [{st}] {name}: {got} warning(s), expected {want}") + + # ---- the declaration file parser ---- + decl_cases = [ + ("a reason is required", "a: because\nb:\n", 1), + ("comments and blanks are skipped", "# note\n\na: because\n", 0), + ("a line with no separator is rejected", "just-a-type\n", 1), + ("a reason containing a colon survives", "a: see rivet: upstream\n", 0), + ] + for name, text, want in decl_cases: + _, bad = load_declared(text) + got = len(bad) + st = "ok" if got == want else "SELF-TEST FAILED" + failed += got != want + print(f" [{st}] decl-file: {name}: {got} problem(s), expected {want}") return failed @@ -157,6 +310,40 @@ def main(): except Exception as e: print(f" WARN: rivet cross-check skipped ({e})", file=sys.stderr) + # ---- second population: coverage rules whose population is EMPTY ---- + # FAIL CLOSED throughout: this check exists because an empty rule renders + # as 100%, so a checker that skips on an error would itself report green + # while checking nothing (scry#141). + try: + text = open(DECL_PATH, encoding="utf-8").read() + except OSError as e: + print(f" FAIL: cannot read {DECL_PATH} ({e}) -- the declaration file is " + f"the whole basis of this check") + return 1 + declared, decl_bad = load_declared(text) + try: + out = subprocess.run(["rivet", "coverage", "--format", "json"], + capture_output=True, text=True, timeout=180) + if out.returncode != 0: + print(f" FAIL: `rivet coverage` exited {out.returncode}") + return 1 + rules = json.loads(out.stdout).get("rules") or [] + except Exception as e: + print(f" FAIL: cannot read coverage rules ({e})") + return 1 + if not rules: + print(" FAIL: `rivet coverage` returned no rules -- nothing to check, " + "which is not the same as nothing wrong") + return 1 + cov_viol, cov_warn = check_coverage(rules, declared) + for w in cov_warn: + print(f" WARN: {w}") + cov_bad = decl_bad + cov_viol + n_empty = sum(1 for r in rules if r.get("total") == 0) + print(f" coverage: {len(rules)} rule(s), {n_empty} over an EMPTY population; " + f"{len(declared)} level(s) declared unmodelled") + + bad = bad + cov_bad for b in bad: print(f" FAIL: {b}") print("PASS" if not bad else f"FAIL ({len(bad)} violation(s))")