FEAT-097: four coverage rules report 100% over an empty population - #196
Open
avrabe wants to merge 2 commits into
Open
FEAT-097: four coverage rules report 100% over an empty population#196avrabe wants to merge 2 commits into
avrabe wants to merge 2 commits into
Conversation
`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
📐 rivet artifact deltaPR: #196 Base SHA: Validationhead — `rivet validate` resultbase — `rivet validate` result (for comparison)Artifact stats
full stats — headDiff (base → head)AADL model — headPosted by the |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The finding
rivet coverageprints seventeen rules. Four report 100.0% over0/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
aspicepreset is embedded and a project cannot subset its rules, so scry cannot decline the four rules. The0/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.2exits 1,--fail-under 88.0exits 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.pyalready 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
unit-verificationfrom the declaration fileswe4-verifies-swe3 at 100% over 0/0safety-goal(5 rows) — a stale entryswe5-new-ruleat 0/0 over an undeclared typeThe 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 sincebea3ddf. 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 validationjob, 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