FEAT-097: four coverage rules report 100% over an empty population

.github/aspice-unmodelled-levels.txt

@@ -0,0 +1,23 @@
+# ASPICE process levels scry deliberately does NOT model, one per line as
+# `<source-type>: <reason>`. 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".

.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

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:
 

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

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