Skip to content

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

Merged
avrabe merged 2 commits into
mainfrom
aspice-scope-declared
Sep 1, 2026
Merged

FEAT-097: four coverage rules report 100% over an empty population#196
avrabe merged 2 commits into
mainfrom
aspice-scope-declared

Conversation

@avrabe

@avrabe avrabe commented Aug 28, 2026

Copy link
Copy Markdown
Contributor

The finding

rivet coverage prints seventeen rules. Four report 100.0% over 0/0:

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]

Measured: zero artifacts of those three types under artifacts/, and zero textual occurrences of the type names — so this is not the vocabulary artifact that produced the false #113 claim. Four of seventeen rows announce success for work never done.

FEAT-033 built this V-model and stated its scope by enumeration — "STK → SYS → SWE.1, with SYS.5 and SWE.6 verification". It never said what it omits, and its residual was empty. An enumerated scope reads as complete to anyone who doesn't already know how many 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, not to fill it.

Discriminating whose defect it is — this 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 rather than worked around here. What is scry's is the undeclared scope, and that is what this fixes.

The weighted overall is not affected — 119/135 = 88.1%, an empty rule adding 0 to both sides. Verified: --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.

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 plus .github/aspice-unmodelled-levels.txt — rather than duplicated into another 250 lines with the same shape. Self-test 6 → 17 cases.

Mutation-checked against real data

mutant measured
drop unit-verification from the declaration file exit 1, names swe4-verifies-swe3 at 100% over 0/0
declare safety-goal (5 rows) — a stale entry exit 1, "makes the file a suppression list instead of a claim"
an entry with no reason exit 1, with file and line
declaration file deleted exit 1, fail-closed
synthetic swe5-new-rule at 0/0 over an undeclared type exit 1
control exit 0

The last one is what justifies building it at all: that is what a future rivet upgrade looks like, and the schema is pinned at aspice@0.2.0, so it is a real event rather than a hypothetical.

Also

Repairs a corrupted line in the V-model header — "the sw-reqs restate the dev the dev requirement..013" — checked in since bea3ddf. Replaced with the verified mapping (SR-1..SR-13 restate REQ-001..REQ-013 one for one, checked by title).

Required set 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 (#130).

What this does not do

It does not make the four 100%s disappear — a reader who doesn't open the declaration file still sees four green rows. And it checks types, not levels: a rule with one token artifact would pass at 100% with no real decomposition behind it. That is #117's class again, and only reading the artifacts reaches it.

Refs: FEAT-097 · FEAT-033 · FEAT-088

🤖 Generated with Claude Code

https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc

`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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc
… 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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc
@github-actions

Copy link
Copy Markdown

📐 rivet artifact delta

PR: #196 Base SHA: 35cf3167

Validation

head — `rivet validate` result
  SR-11 (sw-req, status: accepted) — missing: sw-integration-verification, unit-verification
  SR-12 (sw-req, status: accepted) — missing: sw-integration-verification, unit-verification
  SR-13 (sw-req, status: accepted) — missing: sw-integration-verification, unit-verification
  SR-2 (sw-req, status: accepted) — missing: sw-integration-verification, unit-verification
  SR-3 (sw-req, status: accepted) — missing: sw-integration-verification, unit-verification
  SR-4 (sw-req, status: accepted) — missing: sw-integration-verification, unit-verification
  SR-5 (sw-req, status: accepted) — missing: sw-integration-verification, unit-verification
  SR-6 (sw-req, status: accepted) — missing: sw-integration-verification, unit-verification
  SR-7 (sw-req, status: accepted) — missing: sw-integration-verification, unit-verification
  SR-8 (sw-req, status: accepted) — missing: sw-integration-verification, unit-verification
  SR-9 (sw-req, status: accepted) — missing: sw-integration-verification, unit-verification
  SYS-1 (system-req, status: accepted) — missing: sys-integration-verification
  SYS-2 (system-req, status: accepted) — missing: sys-integration-verification
  SYS-3 (system-req, status: accepted) — missing: sys-integration-verification
  SYS-4 (system-req, status: accepted) — missing: sys-integration-verification
  SYS-5 (system-req, status: accepted) — missing: sys-integration-verification
  → run `rivet validate --explain SR-1` to see which link type and source types satisfy a gap

Result: PASS (186 warnings)
Schemas: common@0.3.0 (embedded), dev@0.3.0 (embedded), research@0.1.0 (embedded), research-ext@0.1.0 (on-disk), safety-case@0.1.0 (embedded), aspice@0.2.0 (embedded)
base — `rivet validate` result (for comparison)
  SR-11 (sw-req, status: accepted) — missing: sw-integration-verification, unit-verification
  SR-12 (sw-req, status: accepted) — missing: sw-integration-verification, unit-verification
  SR-13 (sw-req, status: accepted) — missing: sw-integration-verification, unit-verification
  SR-2 (sw-req, status: accepted) — missing: sw-integration-verification, unit-verification
  SR-3 (sw-req, status: accepted) — missing: sw-integration-verification, unit-verification
  SR-4 (sw-req, status: accepted) — missing: sw-integration-verification, unit-verification
  SR-5 (sw-req, status: accepted) — missing: sw-integration-verification, unit-verification
  SR-6 (sw-req, status: accepted) — missing: sw-integration-verification, unit-verification
  SR-7 (sw-req, status: accepted) — missing: sw-integration-verification, unit-verification
  SR-8 (sw-req, status: accepted) — missing: sw-integration-verification, unit-verification
  SR-9 (sw-req, status: accepted) — missing: sw-integration-verification, unit-verification
  SYS-1 (system-req, status: accepted) — missing: sys-integration-verification
  SYS-2 (system-req, status: accepted) — missing: sys-integration-verification
  SYS-3 (system-req, status: accepted) — missing: sys-integration-verification
  SYS-4 (system-req, status: accepted) — missing: sys-integration-verification
  SYS-5 (system-req, status: accepted) — missing: sys-integration-verification
  → run `rivet validate --explain SR-1` to see which link type and source types satisfy a gap

Result: PASS (185 warnings)
Schemas: common@0.3.0 (embedded), dev@0.3.0 (embedded), research@0.1.0 (embedded), research-ext@0.1.0 (on-disk), safety-case@0.1.0 (embedded), aspice@0.2.0 (embedded)

Artifact stats

base head
Total artifacts 266 267
full stats — head
Artifact summary:
  academic-reference               24
  competitive-analysis             11
  design-decision                  22
  feature                          97
  market-finding                    7
  requirement                      21
  safety-context                    3
  safety-goal                       5
  safety-justification              4
  safety-solution                   6
  safety-strategy                   1
  stakeholder-req                   3
  sw-req                           13
  sw-verification                  13
  sys-verification                  5
  system-req                        5
  technology-evaluation            12
  verification                     15
  TOTAL                           267

Orphan artifacts (no links): 12
  CA-001
  CA-002
  CA-003
  CA-004
  CA-005
  CA-006
  CA-007
  CA-008
  CA-009
  CA-010
  CA-011
  FEAT-078

Diagnostics: 0 error(s), 186 warning(s), 31 info(s)

Diff (base → head)

+ FEAT-097  v3.4 — The ASPICE V-model says which levels it does NOT model, and four vacuous 100%s stop reading as success
~ FEAT-033
  field changed: residual

1 added, 0 removed, 1 modified, 265 unchanged

~ NEW    WARN: [FEAT-097] prose mentions 'FEAT-096' but no typed link to it; add a link in `links:` or remove the mention
0 new errors, 0 resolved errors, 1 new warnings, 0 resolved warnings

AADL model — head

spar/scry.aadl: OK

Posted by the rivet-delta workflow. Informational only — does not gate the PR.

@avrabe
avrabe merged commit d0a9b83 into main Sep 1, 2026
13 checks passed
@avrabe
avrabe deleted the aspice-scope-declared branch September 1, 2026 18:22
avrabe added a commit that referenced this pull request Sep 1, 2026
…198)

artifacts/aspice-vmodel.yaml said "the dev REQ-* carry no verifies link
by construction". Measured today: 15 of 21 dev requirements carry an
incoming `verifies`, every one of them from a `verification` artifact.
The statement is simply false.

It was TRUE when FEAT-033 landed (bea3ddf) — no artifact type could
source a `verifies` link onto a dev REQ-*, which is the gap FEAT-033
existed to close. Commit 6be7359 then added artifacts/verifications.yaml
("wire the dev V's right side — 15/21 REQs verified, 6 honestly open"),
whose `verification` artifacts link straight at the dev REQ-*. Nothing
revisited this comment. It stayed checked in, false, for months.

THE REPLACEMENT CARRIES NO COUNT. Writing "15 of 21" would drift exactly
the same way, just more slowly. The comment now states the STRUCTURE —
dev REQ-* are verified by `verification` artifacts in
verifications.yaml, whose DELIBERATELY UNCOVERED block names each gap
with what evidence would close it — and points at `rivet coverage` for
the current split rather than restating it.

HOW IT SURVIVED ME YESTERDAY, which is the reusable part. FEAT-097 (#196)
repaired a corrupted sentence one line above this one. I was editing for
a different defect and treated the surrounding prose as given, so I
rewrote its neighbour and propagated it verbatim. Proximity to a thing
you are fixing is not evidence that a claim is true; a false statement
adjacent to a repair is likelier to be re-blessed than one nobody is
looking at.

Checked for other copies before fixing the one I happened to be reading:
`carry no verifies link` appears exactly once in the repo, and FEAT-033's
own description states it in the PAST tense ("requirements had no
verifies backlinks"), which is still historically accurate. The residuals
added yesterday to FEAT-033 and FEAT-097 do not repeat it.

NO GATE ADDED, and that is a decision. The six uncovered requirements are
already declared individually in verifications.yaml with a "Would verify"
for each — the best artifact in this repo for its purpose — and it sits
directly above the data it describes. Binding it mechanically would mean
scraping `^#\s+(REQ-\d+)` out of a YAML comment, which is this repo's
dominant documented failure class (four instances of text-matching when
the question is discrimination) deployed to guard a block its own editor
is already looking at. `rivet coverage --fail-under` was also considered
and rejected: below the current value it is scry#117's loose floor, at it
any legitimate artifact addition that shifts the denominator fails.

Refs: FEAT-097


Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant