From 7d25a44861240ff27b0ca488b0cc42bacb50a98e Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 28 Aug 2026 06:31:14 +0200 Subject: [PATCH 1/2] FEAT-097: four coverage rules report 100% over an empty population `rivet coverage` prints seventeen rules. Four report 100.0% over 0/0 -- swe2-allocated-from-swe1, swe3-refines-swe2, swe3-has-verification and swe4-verifies-swe3 -- plus the summary line `V-closure: sw-detail-design (all 2 rules) 100.0% [0/0]`. Measured: zero artifacts of those three types exist under artifacts/, and zero textual occurrences of the type names, so this is not the vocabulary artifact that produced the false scry#113 claim. Four of seventeen rows announce success for work never done. FEAT-033 built the V-model and stated its scope BY ENUMERATION only. It never said what it OMITS and its residual was empty. An enumerated scope reads as complete to anyone who does not already know how many rungs an ASPICE V has. The omission is CORRECT and stays. Design intent 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 own principle is "no fabricated DAL" and it applies to process levels as to integrity levels. The right response to an empty level is to say it is empty, not to fill it. DISCRIMINATED BEFORE BUILDING, and it changed the deliverable. 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, not worked around here. What is scry's is the undeclared scope. The weighted overall is unaffected (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. NO SIXTH GATE. FEAT-088's check-undeveloped-goals.py already 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 -- two pure functions and a declaration file -- rather than duplicated into another 250 lines with the same shape. Self-test 6 -> 17 cases. Five mutants, all red, control green. The one that justifies building it at all: a synthetic `swe5-new-rule` at 0/0 over an undeclared type is caught, which is what a future rivet upgrade looks like -- the schema is pinned at aspice@0.2.0, so that is a real event, not a hypothetical. Also repairs a corrupted line in the V-model header ("the sw-reqs restate the dev the dev requirement..013"), which had been checked in since bea3ddf. Required set unchanged at 12: the guard is a step on the already-required Rivet artifact validation job. Refs: FEAT-097 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc --- .github/aspice-unmodelled-levels.txt | 23 ++++ .github/workflows/ci.yml | 9 +- artifacts/aspice-vmodel.yaml | 38 +++++- artifacts/roadmap-2.0.yaml | 40 ++++++ artifacts/roadmap-v3.4-aspice-scope.yaml | 89 ++++++++++++++ tools/check-undeveloped-goals.py | 149 +++++++++++++++++++++++ 6 files changed, 344 insertions(+), 4 deletions(-) create mode 100644 .github/aspice-unmodelled-levels.txt create mode 100644 artifacts/roadmap-v3.4-aspice-scope.yaml 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..b1f4b2d --- /dev/null +++ b/artifacts/roadmap-v3.4-aspice-scope.yaml @@ -0,0 +1,89 @@ +# 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 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: 17 cases, up from 6 — the original 6 over safety goals, 7 over `check_coverage()` in both directions, 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. + + 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..ffb1dbf 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,59 @@ 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 + + bad = [] + 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) - empty): + 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") + return bad + + def self_test(): """Feed the checker inputs it MUST reject, and one it must accept.""" ok = lambda a: check(a)[0] @@ -125,6 +201,48 @@ 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), + ("REJECT: declared type that appears in NO rule at all is still stale", + [R("a", "x", 5)], {"zzz": "reason"}, 1), + # 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)) + st = "ok" if got == want else "SELF-TEST FAILED" + failed += got != want + print(f" [{st}] {name}: {got} violation(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 +275,37 @@ 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_bad = decl_bad + check_coverage(rules, declared) + 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))") From bb460ff8f9c84e1e32d522668435e4e771edf42f Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 28 Aug 2026 06:35:27 +0200 Subject: [PATCH 2/2] FEAT-097 review fix: a dropped preset rule must not demand deleting a true statement `check_coverage` treated "declared type appears in no rule at all" as a stale entry and failed, and the self-test LOCKED THAT IN by asserting a violation for it. But that state is the preset DROPPING a rule -- the same upgrade MUT5 exists for, seen from the other side. If rivet removes the sw-detail-design rules, `sw-detail-design` leaves the report, and the declaration "scry does not model SWE.3" is still TRUE. No vacuous 100% can result, because the rule is gone. Failing there demands deleting a correct statement to get the build green: the Class-5 shape from this repo's own taxonomy, a guard right about the fact and wrong about the remedy. Split into two outcomes. A declared type whose population is POPULATED still FAILS -- the claim is now false. A declared type absent from the rule set WARNS -- the claim is still true, merely no longer enforceable. Both mutants re-run with no regression (dropping a declared level still exits 1; a populated stale entry still exits 1), and the new case mutation-checked by filtering every sw-detail-design rule out of the live report: exit 0 with the warning. The warning channel gets its own three self-test assertions. A split that silently dropped one side would be invisible from violation counts alone, which is how the original defect survived six passing cases. Self-test 17 -> 20. Also records in the residual that `traces-to FEAT-088` was added to silence rivet's prose-mentions-without-a-link warning, not because `traces-to` describes the relation. Verified inert: no tool reads it, and check-release-ordering.py reads only `depends-on`. Refs: FEAT-097 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc --- artifacts/roadmap-v3.4-aspice-scope.yaml | 12 +++++- tools/check-undeveloped-goals.py | 52 ++++++++++++++++++++---- 2 files changed, 56 insertions(+), 8 deletions(-) diff --git a/artifacts/roadmap-v3.4-aspice-scope.yaml b/artifacts/roadmap-v3.4-aspice-scope.yaml index b1f4b2d..8c4997d 100644 --- a/artifacts/roadmap-v3.4-aspice-scope.yaml +++ b/artifacts/roadmap-v3.4-aspice-scope.yaml @@ -55,8 +55,10 @@ artifacts: - "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: 17 cases, up from 6 — the original 6 over safety goals, 7 over `check_coverage()` in both directions, and 4 over the declaration-file parser including that a reason containing a colon survives." + - "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 @@ -65,6 +67,14 @@ artifacts: 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 diff --git a/tools/check-undeveloped-goals.py b/tools/check-undeveloped-goals.py index ffb1dbf..fd6c5ed 100755 --- a/tools/check-undeveloped-goals.py +++ b/tools/check-undeveloped-goals.py @@ -152,19 +152,32 @@ def check_coverage(rules, declared): (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 = [] + 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) - empty): + 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") - return bad + # 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(): @@ -215,8 +228,14 @@ def self_test(): # 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), - ("REJECT: declared type that appears in NO rule at all is still stale", - [R("a", "x", 5)], {"zzz": "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", @@ -225,11 +244,27 @@ def self_test(): [R("a", "x", 0), R("b", "y", 0)], {}, 2), ] for name, rules, decl, want in cov_cases: - got = len(check_coverage(rules, decl)) + 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), @@ -300,7 +335,10 @@ def main(): print(" FAIL: `rivet coverage` returned no rules -- nothing to check, " "which is not the same as nothing wrong") return 1 - cov_bad = decl_bad + check_coverage(rules, declared) + 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")