feat(coverage): let a project declare rules it does not model (REQ-320) - #893
Merged
Conversation
Reported from scry (#871 part 2). Adopting an embedded preset for part of its scope drags in the rest of its rules: taking `aspice` for SWE.1/SWE.6 necessarily inherits SWE.2/3/4 rows the project has no intention of satisfying. There was nowhere to say so, and an unmodelled level rendered as an empty row forever — indistinguishable from one nobody got round to. coverage: unmodelled-rules: - rule: swe3-refines-swe2 reason: detail design lives in a parallel dev spine, by intent The reason is REQUIRED. A declaration without one is indistinguishable from suppressing an inconvenient row, which is the thing this must not become. The declared rule STAYS in the report, annotated: hiding it is the failure this replaces, not the fix. Two ways a declaration can fail, and both fail the run: STALE the rule now has source artifacts, so the project said it does not model something and then modelled it UNKNOWN no such rule exists in the active schemas — silently ignoring a typo would let a project believe it had declared something The staleness half is the point, and it is what was promised to the reporter when this was filed: an exemption that outlives its reason is the same defect as the 100% it replaced — a number that stopped meaning what it says. It fails always rather than under a flag, because a stale exemption silently shrinks the denominator every later number is computed against. Implemented additively as `mark_unmodelled` rather than as a parameter on `compute_coverage`, whose signature is public. Grouped deliberately with REQ-309 (`exempt-when-field`: an artifact declares itself out of a rule's population) and REQ-313 (declared-blocked acceptance criteria). Three levels of one idea — artifact, criterion, project scope — and this is the project-scope one. Three unrelated mechanisms would each have grown their own staleness check and given a reader three places to look when a number goes quiet. The oracle was written against the real dev-schema rule names after a first draft guessed one that does not exist — a fixture naming a rule the schema has never heard of would have exercised nothing. `decision-justification` has an empty population in the fixture and is the happy path; `requirement-verification` has one and is the stale path. Unit tests live in rivet-core beside the function because the mutation gate runs `-- --lib`. Negative-controlled at that scope: never detecting stale, ignoring an unknown rule, and not annotating each redden exactly one test. Note `rivet-core/src/proofs.rs` — the new `CoverageEntry` field had to be added there too. That file is `#[cfg(kani)]`, so it is invisible to cargo build, cargo test and clippy; the same omission broke the Kani proofs once before and the signal was written off as flake six times. Verified structurally this time by comparing the literal's field set against the struct's (14 of 14), since `--cfg kani` cannot build locally — a dependency carries its own kani-gated code. Confirmed with cargo fmt --check, clippy --all-targets -D warnings on 1.97.0, cargo test --workspace (exit 0, 66 ok, 0 failed), the full cli_commands suite (189 passed), rivet validate, rivet docs check, yamllint on the CI paths, and `rivet coverage` on this repo (unchanged — no declaration means no behaviour change) — all exit 0. With this, every artifact scoped to v0.36.0 is `verified`. Implements: REQ-320 Verifies: REQ-320 Refs: REQ-309, REQ-313, REQ-294
📐 Rivet artifact delta
Graphgraph LR
REQ_320["REQ-320"]:::modified
classDef added fill:#d4edda,stroke:#28a745,color:#155724
classDef removed fill:#f8d7da,stroke:#dc3545,color:#721c24
classDef modified fill:#fff3cd,stroke:#ffc107,color:#856404
classDef overflow fill:#e2e3e5,stroke:#6c757d,color:#495057,stroke-dasharray: 3 3
Modified
Posted by |
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
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
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.
Closes the remaining half of #871.
Adopting an embedded preset for part of its scope drags in the rest of its
rules: taking
aspicefor SWE.1/SWE.6 necessarily inherits SWE.2/3/4 rows theproject has no intention of satisfying. There was nowhere to say so, and an
unmodelled level rendered as an empty row forever — indistinguishable from
one nobody got round to.
The reason is required. A declaration without one is indistinguishable from
suppressing an inconvenient row, which is the thing this must not become. And
the declared rule stays in the report, annotated — hiding it is the failure
this replaces, not the fix.
Two ways a declaration fails, and both fail the run
The staleness half is the point, and it's what I promised you when this was
filed: an exemption that outlives its reason is the same defect as the 100% it
replaced — a number that stopped meaning what it says. It fails always rather
than under a flag, because a stale exemption silently shrinks the denominator
every later number is computed against.
Grouped, not standalone
Deliberately built alongside REQ-309 (
exempt-when-field— an artifact declaresitself out of a rule's population) and REQ-313 (declared-blocked acceptance
criteria). Three levels of one idea — artifact, criterion, project scope —
and this is the project-scope one. Three unrelated mechanisms would each have
grown their own staleness check and given a reader three places to look when a
number goes quiet.
Notes on the build
mark_unmodelledrather than a parameter oncompute_coverage, whose signature is public.draft guessed one that doesn't exist — a fixture naming a rule the schema has
never heard of exercises nothing.
decision-justification(empty population)is the happy path;
requirement-verification(populated) is the stale path.rivet-corebeside the function because the mutation gateruns
-- --lib. Negative-controlled there: never detecting stale, ignoring anunknown rule, and not annotating each redden exactly one test.
rivet-core/src/proofs.rsneeded the new field too. That file is#[cfg(kani)]— invisible to build, test and clippy. The same omission brokethe Kani proofs once before and the signal was written off as flake six times.
Verified structurally (14/14 fields) since
--cfg kanican't build locally: adependency carries its own kani-gated code.
Heads-up: this adds public fields to
ProjectConfigandCoverageEntry, soSemver Checks may flag them. Precedent says fields have been added before
(
release,externals,baselines) — I'd rather let CI answer than predict.Gates
cargo fmt --check·clippy --all-targets -D warningson 1.97.0 ·cargo test --workspace(exit 0, 66 ok) · fullcli_commands(189 passed) ·rivet validate·rivet docs check·yamllint·rivet coverageon thisrepo (unchanged — no declaration means no behaviour change) — all exit 0.
With this, every artifact scoped to v0.36.0 is
verified(10/10).