Repository navigation
fix(rivet): validate 22 errors → PASS; resolve externals in CI (v0.12.0 evidence prerequisite) - #314
Conversation
|
Correcting how the PASS in this PR's description was measured. It was right, but it was measured against the wrong store, and that mattered enough to redo. My local Re-measured with a fresh Same verdict, now from the right store. Externals load, cross-refs are checked. Two things that turned up in the re-run
What still has to be true before the tagNo PR CI run exercises any of this: 🤖 Generated with Claude Code |
…d way Each of these cost real time this cycle and none of them was written anywhere. **`rivet verify`, never `--set-status verified`** (checklist item 6). `--set-status verified` writes the field and checks nothing; `rivet verify` is the gate. This release's three requirements were all `verified` with zero evidence, and the tool refused all three the moment it was actually asked. Readiness is `rivet verify --dry-run` over the release's scope, not a read of the status field. **A masked gate's exit code is in the LOG, not the API** (item 7). A step under `continue-on-error` reports `conclusion: success` for the step AND the job over REST. Four of five Kani modules masked, seven harnesses failing, every job green — and a workflow comment asserting three ran unmasked, which had already propagated into the rivet store and the CHANGELOG before anyone read the matrix below it. **Confirm the merge actually waited** (item 8). `required_status_checks.contexts` was empty with no rulesets, so every check here was advisory. Records the one required context and why a paths-filtered context must never be required directly — it will not report on an unrelated PR, and a *skipped* required context satisfies the merge button. **Never `--squash` a stacked PR** (merge step). It collapses the lower PR's commits under the upper one's message, misattributes the work, and leaves the lower PR looking unmerged forever. Twice here: REQ-27 under #273, and #301 inside #305. Also notes the merge-commit alternative's second benefit — the base commit stays a real ancestor, so the sibling branch needs no replay and no conflict resolution that might quietly drop a guard. Plus: the `rivet validate` line this PR added already needed replacing. It said "22 errors ... not a release gate". #314 takes it to PASS, and it IS a gate — the compliance action propagates validate's exit code (rivet #953) and the bundle is this project's V-model evidence. Also distinguishes the ~182 warnings (real coverage gaps, `requirement-verification` 0/38) from errors, with the rule that a warning is never closed by demoting an artifact to `draft`. Two additions to "what NOT to do": never re-pin a baseline to get green, and never add a `cargo audit --ignore` line to clear a release. Refs #284, #300, #301, #302, #305, #314, #316, #317 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012aR3Md1h46K9wAUWMQiESH
…solve in CI With #307 unfreezing the rivet binary the compliance job stops panicking in Export and fails one step later, in Validate: `rivet validate` exited 1 on 22 errors, and the action's run_validate.sh (rivet #953) propagates that as the step's exit. So the compliance evidence for v0.12.0 stayed unobtainable even after the pin fix. This closes it: **Result: PASS, exit 0.** Every one of the 22 was mechanical, and all were fixed with `rivet modify` / `rivet link` rather than hand-edited YAML: **11 x off-vocabulary `status: in-progress`.** `in-progress` was never in rivet's canonical lifecycle (draft -> proposed -> approved -> implemented -> verified -> released, plus accepted/deprecated/rejected). rivet gained enforcement of that enum in REQ-162 / #352 — the value had been passing silently before. Mapped by checking each artifact against the code, not by picking whichever value validated: FEAT-2,6,7,8,9,10,11 -> implemented the implementing code exists — format/mcuboot.rs, transcoding.rs + intoto.rs, container/digest.rs + bundle.rs, keyless/proof_cache.rs, container/referrer.rs, formal-verification.yml, src/component CV-20, CV-21, CV-22 -> approved deliberately NOT `implemented`. These are the Verus and Rocq verification activities, and all three steps exit 1 behind continue-on-error today (CV-22 is a stub; audit C-1 records `assume(false)` in the Verus side). A verification that does not discharge is scoped, not implemented. REQ-14 -> approved its proofs are the three above. `draft` would have validated too, and for the coverage rules it is the cheaper answer — a draft artifact is exempt from them. That is exactly why it was not used: it would have bought a PASS by making the gate look away. `approved` keeps all three CVs and REQ-14 inside the coverage rules, which is where the 182 warnings come from. **6 x `satisfies` declared with zero targets** (DD-8..DD-13). Linked to the requirement each decision actually serves rather than deleting the empty key, which would only have moved DD-10's failure to the design-decision coverage rule: DD-8 -> REQ-17 HW-preferred verify with SW fallback <- the wsc:crypto hardware-verify interface with curve negotiation DD-9 -> REQ-15 "a wasm component via meld/loom/synth, NOT a hand-carved no_std staticlib" is the design choice FOR REQ-15 DD-10 -> REQ-19 MAX_SLICE_LEN = 256MB exists to hold the large embedded core-module section REQ-19 names DD-11 -> REQ-23 offline keyless verify: SET mandatory, Merkle not checked DD-12 -> REQ-23 offline verify cannot check SCTs (no CT key in the bundle) DD-13 -> REQ-24 DSSE extracted to wsc-dsse, not into wsc-verify-core **3 x undeclared `related-to` link type** (H-36/37/38). No STPA link type expresses hazard-to-hazard adjacency — `prevents` is constraint->hazard, `leads-to-hazard` is uca->hazard — so the relation had been written with a type the schema never declared, which made it unenforceable and invisible to coverage rules. Declared in schemas/stpa-sec.yaml (sigil's own on-disk schema) rather than deleted: that three hazards are variants of H-25, H-33/34 and H-14 is real analysis, and it is explicitly NOT `sub-hazard` — they are peers, so neither inherits the other's constraints. **1 x duplicate artifact id, which is the one real defect in the set.** CV-25 was declared twice in the same file: "Transcoding attestation roundtrip test" (#58) and "Mechanised sister logic for compositional attestation-chain trust" (#94). rivet's own words: "the second definition silently overwrites the first" — so since #94 the transcoding roundtrip verification has not been in the trace at all, along with its `verifies` link. The newcomer is renumbered to CV-35 (`rivet next-id`); the original keeps CV-25. Nothing else referenced the id, so no links needed rewiring. This is the one edit made by hand: rivet can *detect* a duplicate id but offers no `--set-id` and no rename/renumber subcommand, so there is no command to do it with. Filed as friction in rivet. Both callers of the compliance action now clone synth before invoking it. rivet.yaml declares `synth` as an external at ../synth, and ONE unresolvable external makes rivet abandon cross-ref checking for all of them — reporting "cross-refs NOT CHECKED — externals failed to load" and counting sigil's 9 valid synth links as broken. A single-repo checkout has no sibling, so CI saw 31 errors where a developer with ../synth checked out saw 22. #307's kiln removal does nothing about that; this does. actions/checkout refuses to write outside GITHUB_WORKSPACE, hence a direct `git clone`. Pinned to v0.87.0 rather than main, deliberately: a compliance bundle is audit evidence and re-running a release must re-derive the same report, which a moving HEAD cannot promise. The cost is stated in the workflow comment — a cross-ref sigil still claims could rot in synth's later commits without this job noticing. That drift shows up in a developer's local run and when the pin is next raised. claims.yaml gains SYNTH-PIN-AGREES so the two callers cannot pin different refs and validate the release-time report against a different store than the on-demand one. Negative controls, each run: callers pin v0.86.0 vs v0.87.0 -> RED, names both files, exit 1 one clone step deleted -> RED, 1 < min-captures 2, exit 1 claim's pattern has no group -> RED, named, exit 1 Writing that claim found a real fault in `captures-agree` itself: a pattern whose group 1 does not participate (easy with an alternation) yielded None and raised TypeError inside the sort — which aborted main() and left **every later claim unevaluated**. The run still exited non-zero, so no false green, but the silently-skipped tail is the dangerous half: fixing the broken claim later re-enables claims nobody has looked at since. Both shapes are now named as claim defects and reported, deduped, with the suite running to the end. Prerequisite for tagging v0.12.0: the release's compliance report is the V-model evidence, and it has not been produced since 2026-09-08. Refs #284, #300 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012aR3Md1h46K9wAUWMQiESH
d8237f9 to
5144fa3
Compare
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
Stacked on #307. With the pin unfrozen the compliance job stops panicking in Export and fails one step later, in Validate —
rivet validateexited 1 on 22 errors andrun_validate.sh(rivet #953) propagates it. This closes that:Result: PASS, exit 0.The 22, all mechanical, all via
rivet modify/rivet link11 × off-vocabulary
status: in-progress— never in rivet's canonical lifecycle; rivet gained enforcement of the enum in REQ-162/#352, so the value had been passing silently. Mapped by checking each artifact against the code:implementedformat/mcuboot.rs,transcoding.rs+intoto.rs,container/digest.rs+bundle.rs,keyless/proof_cache.rs,container/referrer.rs,formal-verification.yml,src/componentapprovedimplemented: these are the Verus/Rocq verification activities, and all three steps exit 1 behindcontinue-on-errortoday (CV-22 is a stub; audit C-1 recordsassume(false)). A verification that does not discharge is scoped, not implemented.approveddraftwould also have validated, and is cheaper — a draft artifact is exempt from the coverage rules. That is precisely why it was not used: it buys a PASS by making the gate look away.approvedkeeps all four inside the coverage rules, which is where the 182 warnings come from.6 ×
satisfiesdeclared with zero targets (DD-8…13) — linked to the requirement each decision actually serves, rather than deleting the empty key, which would only move DD-10's failure to the design-decision coverage rule:wsc:cryptohardware-verify interfaceMAX_SLICE_LEN = 256MBexists to hold the large embedded core-module section REQ-19 nameswsc-dsse, not intowsc-verify-core3 × undeclared
related-to(H-36/37/38) — no STPA link type expresses hazard↔hazard adjacency (preventsis constraint→hazard,leads-to-hazardis uca→hazard), so the relation used a type the schema never declared, making it unenforceable and invisible to coverage rules. Declared inschemas/stpa-sec.yamlrather than deleted: that these three are variants of H-25, H-33/34 and H-14 is real analysis. Explicitly notsub-hazard— they are peers, so neither inherits the other's constraints.1 × duplicate artifact id — the one real defect in the set
CV-25was declared twice in the same file: "Transcoding attestation roundtrip test" (#58) and "Mechanised sister logic for compositional attestation-chain trust" (#94). In rivet's words, "the second definition silently overwrites the first" — so since #94 the transcoding roundtrip verification has not been in the trace at all, along with itsverifieslink. The newcomer is renumbered toCV-35(rivet next-id); the original keepsCV-25. Nothing else referenced the id.This is the one edit made by hand: rivet can detect a duplicate id but has no
--set-idand no rename subcommand, so there is no command to do it with. Filed as friction in rivet.Externals in CI
Both callers now
git clonesynth before invoking the action.rivet.yamldeclaressynthat../synth, and one unresolvable external makes rivet abandon cross-ref checking for all of them — so CI saw 31 errors where a developer with../synthchecked out saw 22. #307's kiln removal does nothing about that; this does.actions/checkoutrefuses to write outsideGITHUB_WORKSPACE, hence the direct clone.Pinned to v0.87.0, not
main— a compliance bundle is audit evidence and re-running a release must re-derive the same report. The cost is stated in the workflow comment: a cross-ref sigil still claims could rot in synth's later commits without this job noticing. That drift surfaces in a developer's local run and when the pin is next raised.claims.yamlgains SYNTH-PIN-AGREES so the two callers cannot pin different refs and validate the release-time report against a different store than the on-demand one:A crash in the instrument
Writing that claim found a real fault in
captures-agreeitself: a pattern whose group 1 does not participate — easy with an alternation — yieldedNoneand raisedTypeErrorinside the sort, which abortedmain()and left every later claim unevaluated. The run still exited non-zero, so no false green; the silently-skipped tail is the dangerous half, because fixing the broken claim later re-enables claims nobody has looked at since. Both shapes are now reported as named claim defects, deduped, with the suite running to the end.Prerequisite for tagging v0.12.0: the compliance report is the release's V-model evidence, and none has been produced since 2026-09-08.
Refs #284, #300
🤖 Generated with Claude Code
https://claude.ai/code/session_012aR3Md1h46K9wAUWMQiESH