L7: traceability repair — rivet ours-errors 2 → 0, VCR-RA-004/SEL-005 de-staled, VCR-VER-004 filed (#893) by avrabe · Pull Request #913 · pulseengine/synth

avrabe · 2026-08-05T16:23:44Z

v0.55 lane L7 — traceability repair + the honest-N/A backlog. No behaviour
changes; what changes is whether the project's evidence artifacts can be trusted
to mean one thing. Closes #893, resolves the last non-external rivet validate
errors, files #912.

rivet: non-external errors 2 → 0

rivet validate still reports ~50 errors locally; all 50 are cross-repo links
into sibling repos that are not checked out here (kiln 21, gale 18, sigil 5,
scry 3, jess 2, witness 1) and are unresolvable from this tree. The measurable
claim is the other bucket:

	before	after
total errors	52	50
errors that are OURS	2	0
warnings	104	104 (net unchanged)
INFO	—	+1
lifecycle coverage gaps	54	56
`rivet coverage` weighted overall	90.3 %	90.7 %
`rivet coverage` sw-req V-closure	31/60 (51.7 %)	33/60 (55.0 %)

The full diagnostic diff vs main is exactly: −2 ERROR (both ours), −2
WARN (GI-FPU-002 and VCR-RA-004 "should be verified by", both closed by new
verifies links), +2 WARN +1 INFO (all three VCR-VER-004's, all of kinds
its sibling sys-verification artifacts already carry).

Lifecycle gaps 54 → 56 is honest, not a regression: a proposed artifact
is not lifecycle-checked, so GI-FPU-002 and VCR-RA-004 were absent from the
baseline list because a wrong status exempted them. They are newly checked,
and the sw-verification half of each gap is closed in this PR by SWVER-022
and GI-FPU-VER-002 — two artifacts recording evidence that already existed
and was already named in the requirements' criteria, but had no typed link.

The brief expected one ours-error. There were two — and the reason the second
one was invisible turned out to be the more interesting finding (see the CI
section). Warning delta is −1 (VCR-RA-004's "should be verified by" closed by a
new verifies link) and +3 attributable to the new VCR-VER-004 artifact; the
diagnostic-class diff against baseline shows no new kind, and all three
kinds are ones its sibling artifacts already carry.

What was wrong, and what I decided

VCR-DEC-003 → traces-to: synth:396. An issue NUMBER where an artifact id
belongs. Decision: retarget to VCR-COV-001, don't delete and don't create a
396 artifact. The evidence is primary-source — synth#396's own body says
"Tracked in rivet as VCR-COV-001, sibling to VCR-DBG-001", and VCR-COV-001's
title carries "(synth #396)". In-repo traces-to targets are already idiomatic
in that file. synth-396 joins the tags so the issue number survives as a
reference rather than a resolvable target.

GI-FPU-002 was declared TWICE — gale-integration.yaml (proposed, the
original #369 ask) and verified-codegen-roadmap.yaml (implemented, PR #705's
phase-1 delivery record). rivet loaded the second over the first, so the graph
reported the requirement NOT STARTED while README/CHANGELOG report #369
closed, f32 v0.41, f64 v0.43, VFP spilling v0.53. Decision: merge, don't
delete, and keep the copy in gale-integration.yaml — that is the id's
namespace home (GI-002 → GI-FPU-001 → GI-FPU-002 → GI-FPU-VER-001 are one chain
there; GI-FPU-002 was the only GI-* artifact in the roadmap), and it already
carried derives-from GI-002, traces-to gale:369 and the jess REQ-PIX-001
linkage that a straight delete of that side would have dropped. The roadmap
copy's phase-1 evidence and verification criteria were folded in; the merge had
to pick a status, so it is now implemented with the post-phase-1 evidence and
the two remaining float declines named.

VCR-RA-004 (#893). The brief offered "new id for the v0.53 work" or "flip
to implemented". Decision: flip to implemented — and the framing that it is
one id meaning two things does not survive the evidence. The resolver
VCR-RA-004 describes shipped in v0.11.38 (synth_synthesis::parallel_move);
the artifact's own tags already said release-v0.11.38, and the CHANGELOG names
it there and again at v0.11.39. v0.53's #881 extended it to the VFP file. Only
the status field was never flipped; minting a second id would have created the
collision the issue wanted removed. Added SWVER-022 so the right side of
the V closes by a typed verifies link. implemented, not verified — the
demanded property test exists and does exactly what the criteria specify (6000
sequentializations vs a reference parallel semantics, scratch sets 0/1/2), but
the second pitfall the artifact names (split points inside hot loops) is still
bounded by assumption, and that residual is now written down.

VCR-SEL-005 "BOTH the ARM and RISC-V selectors" → three backends since
v0.53 (#883); SWVER-017 carried the same claim in its title. Correcting the
count exposed that every ledger size asserted around it had also drifted, all
in the flattering direction: roadmap said 21 for an array of 18,
known_divergences's doc comment said 19, aarch64_known_divergences's said
"the SEVEN below" over an array of 5. The stale-entry check forces a closed gap
to retire its ledger line — nothing forced the prose about the ledger to move
with it.

`VCR-VER-004` now exists in the roadmap

It shipped in v0.54 and appeared in the CHANGELOG, the feature-matrix template
and CI — but not in the file README calls "the single source of truth for
roadmap status". The entry records the four axes on which it fails differently,
and all three limits — including the one that bounds the whole claim: the op
model is still shared. All three instruments extract def/use through
liveness::reg_effect, so a mismodeled op is a common blind spot. VCR-VER-004
closes the shared-contract hole, not the shared-op-model hole, and until
synth-verify's ArmSemantics::encode_op is pinned against it (VCR-ISA-001's
Sail-derived semantics being the eventual anchor — now a typed link, not a prose
aside), "three independent validators" would be an overclaim.

The finding the brief did not anticipate: the gate could not see either error

Both defects sat in a tree with Rivet Validation green. Not a coincidence —
the filter had two holes, one per defect:

grep "^ ERROR:" anchored on two-space-indented lines, so rivet's
filename-prefixed diagnostics were invisible — including "artifact id X
is declared more than once … the second definition silently overwrites the
first". That is exactly how GI-FPU-002 stayed broken.
The cross-repo exemption targets '.*:.*' which does not exist exempted any
target containing a colon. synth:396 contains a colon, so a broken link
in our own graph was classified as an un-rivet'd sibling repo and waved
through.

Fixed structurally, not by allowlist: every ERROR: line counts, and the
exemption is "a foreign prefix", with our own synth: added back to the
ours-count. Failures now print the offending lines. Red-first, end to end, by
extracting the step from the YAML and replaying it against both trees:

pre-fix artifacts (65417c0): exit 1, "Found 2 rivet validation errors that
are OURS", both named;
this branch: exit 0, cross-repo warning still emitted.

⚠️ Verified against local rivet 0.28.0 while the job pins 0.23.0. Hole
(2)'s fix is version-independent; hole (1)'s may be latent protection if 0.23.0
lacks that diagnostic. This PR's own Rivet Validation run is the empirical
test — if 0.23.0 emits some other filename-prefixed error invisible locally,
this is where it surfaces, and surfacing it is the point.

Also

README's synth-backend-aarch64 row said "integer subset"; it has not been one
since v0.54. It now points at the generated feature matrix rather than
restating the op list — a second copy of that list is how v0.54's cold review
found a doc-honesty defect.
CLAUDE.md's three stale aarch64 claims (0f0c232). The lane declined this
on brief scope (agent configuration, not lane surface) and flagged it instead;
the coordinator picked it up and found a third instance neither the README
fix nor the flag had covered: the Track-C note said aarch64 is N/A for
VCR-VER-003 "(no linear-memory ops in the integer subset)". The verdict is
still right and the reason is false — aarch64 has had bounds-checked
linear-memory load/store since v0.52 (aarch64: linear-memory load/store emit NO bounds check and --safety-bounds is a no-op (all modes byte-identical) — OOB reads/writes up to 4GiB past the guest memory instead of trapping #865); it is N/A because it emits no data
section and refuses data-carrying modules loudly (v0.53), so there is no
served-vs-runtime image to compare. A correct conclusion resting on a rotted
premise is the harder version of this defect, and it is the fourth copy of a
list this project keeps duplicating (oracle, matrix row, CHANGELOG, CLAUDE.md).
Both facts re-verified against the generated feature matrix; claim_check
stays 37/37 with CLAUDE.md pinned by three ledger entries.
Recurring N/A: witness MC/DC (feature-loop step 5) skipped four releases running — record a standing exemption or retire it #912 filed: feature-loop step 5 (witness MC/DC) marked N/A four releases
running (v0.51–v0.54), past the skill's own three-feature threshold. Filed,
not decided: synth compiles Wasm rather than emitting components, so witness
may have no artifact to instrument — but VCR-COV-001 is the standing argument
that the DO-178C 6.4.4.2 source-to-object obligation does not vanish just
because the measurement point does. Three candidate resolutions, no
recommendation.

Gates (real exit codes, local)

gate	result
`cargo fmt --check`	0
`cargo clippy --workspace --all-targets -- -D warnings`	0
`cargo test --workspace`	0 — 2675 passed, 0 failed
`python3 scripts/claim_check.py claims.yaml`	0 — 37/37
`cargo test -p synth-synthesis parallel_move`	0 — 13/13
`cargo test -p synth-backend-riscv --test cross_backend_op_parity`	0 — 8/8
`rivet validate` non-external errors	0 (was 2)
`rivet coverage` (the job's 2nd step)	0 — 90.3 % → 90.7 %

No generated doc was hand-edited — docs/status/FEATURE_MATRIX.md and
artifacts/status.json are absent from the diff; only the template is a source
file and it needed no change.

Closes #893.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

`traces-to: synth:396` was the one genuinely-ours rivet broken-link error: `synth:396` reads as "artifact 396 in repo synth", and no such artifact exists — an issue number used where an artifact id belongs. The traceability intent is preserved rather than deleted: synth#396's own body says "Tracked in rivet as VCR-COV-001, sibling to VCR-DBG-001", and VCR-COV-001's title carries "(synth #396)". So the link retargets to VCR-COV-001 (in-repo `traces-to` targets are already idiomatic in this file — VCR-SEL-001, VCR-RA-001, VCR-MEM-001, …), and `synth-396` joins the tags so the issue number stays discoverable as a reference instead of a resolvable target. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

…tly won The second genuinely-ours rivet error, which the lane brief did not know about because the local grep for it (`^ ERROR:`) misses filename-prefixed diagnostics: gale-integration.yaml: ERROR: [GI-FPU-002] artifact id 'GI-FPU-002' is declared more than once: ./artifacts/verified-codegen-roadmap.yaml and ./artifacts/gale-integration.yaml — the second definition silently overwrites the first This is the #893 class one level worse than a stale description: the requirement was declared in gale-integration.yaml (`status: proposed`, the original #369 ask) and AGAIN in verified-codegen-roadmap.yaml (`status: implemented`, the phase-1 delivery record added by PR #705). rivet loaded the `proposed` copy over the `implemented` one, so the traceability graph reported GI-FPU-002 as NOT STARTED while README/CHANGELOG report #369 CLOSED, f32 complete v0.41, f64 complete v0.43, and VFP register-file spilling shipped v0.53. Resolved by MERGING, not deleting — the two copies carried disjoint edges and disjoint evidence: * Survivor: gale-integration.yaml. That is the id's namespace home (GI-002 -> GI-FPU-001 -> GI-FPU-002 -> GI-FPU-VER-001 are one chain in that file; GI-FPU-002 was the ONLY GI-* artifact in the roadmap). It also already carried `derives-from GI-002`, `traces-to gale:369`, and the jess REQ-PIX-001 / AFD-024 Pixhawk linkage — all of which a straight delete of that side would have dropped. README names the roadmap the single source of truth for the VCR-* program's roadmap status, which GI-* is not. * Folded in: the roadmap copy's six-point phase-1 DELIVERED list and its full verification-criteria (the f32_vfp_619_differential RED->GREEN evidence, the m3 honest-reject direction, the f32_hardfloat_619.rs unit lock, and the recorded unicorn VMRS FPSCR->APSR emulator gap). * De-staled, since the merge had to pick one status anyway: `proposed` -> `implemented`, with the post-phase-1 evidence the roadmap copy predated — f64 complete v0.43 (#369 closed), v0.52 #869 inline i64<->float, v0.53 #881 VFP spilling (109 rows bit-identical to wasmtime) — and the two residuals stated as loud declines rather than implied away (`f32.{ceil,floor,trunc,nearest}` pending a real VRINT.F32 after v0.54 removed the unsound saturating-VCVT pseudo-op, and `i64.trunc_sat_f32_*` on single-precision FPUs). * Where the duplicate was, the roadmap now carries a pointer comment explaining why the id is not defined there. rivet: 52 -> 50 errors; NON-EXTERNAL errors 2 -> 0. Warning/info diagnostic sets are byte-identical before/after (no new class introduced). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

…0.11.38 Half of #893: v0.53's VFP-spilling lane tagged its work `VCR-RA-004`, while artifacts/verified-codegen-roadmap.yaml still carried that id as `status: proposed`. The brief offered two resolutions — mint a new id for the v0.53 work, or flip VCR-RA-004 to implemented. The evidence decides it, and it is neither of the two things the ID-collision framing suggested: the resolver VCR-RA-004 describes shipped in **v0.11.38**, three years of releases before the lane that got blamed for overloading the id. `synth_synthesis::parallel_move` is verbatim what the artifact asks for — a pure, testable component that sequentializes a parallel move set with cycle detection, scratch selection from dead registers, and a guaranteed-progress fallback. The artifact's own tags already said `release-v0.11.38`; the CHANGELOG names it twice (v0.11.38 "Cycle-safe parallel-move resolver (`synth_synthesis::parallel_move`, VCR-RA-004)" and v0.11.39 "#327 — VCR-RA-004's resolver (v0.11.38) breaks cycles via a stack-scratch cell"). Only the status field was never flipped. Minting a second id would have created the collision the issue was trying to remove. So: `proposed` -> `implemented`, with the evidence written down instead of left in changelog prose — * the algorithm and its progress discipline (the size bound and the strictly-shrinking pending set are `assert!`s in the resolver, so an unbounded path aborts rather than emitting); * both consumers, each of which removed a real defect rather than only adding a component: v0.11.39 #327 arg-move marshalling (the old cycle-breaker demanded a callee-saved register AND miscompiled genuine 2-swaps by duplicating a value), and v0.53 #881 VFP register-file spilling (the falcon `S0..S15 all live` wall) — which is precisely the work the v0.53 notes tagged VCR-RA-004; * SWVER-022, a new sw-verification artifact linking `verifies` -> VCR-RA-004, so the right side of the V is closed by a typed link rather than by a paragraph. It records the run recipe and what each of the three criteria clauses is actually met by. `implemented`, NOT `verified`, deliberately. The property test the criteria demand does exist and does exactly what they specify — 2000 iterations over R0..R8 alternating full random permutations with partial move sets, each re-checked at scratch-set sizes 0/1/2 (6000 sequentializations) against a reference parallel semantics, plus 12 directed shape tests — verified locally, `cargo test -p synth-synthesis parallel_move` 13/13, real exit 0. But the second pitfall the artifact names, split points landing inside hot loops, is still bounded by ASSUMPTION (synth's straight-line segment scope) rather than by a check that fails when segments widen. That residual is now stated in both the requirement and SWVER-022 rather than implied away. rivet: non-external errors still 0; warnings 104 -> 103 (VCR-RA-004's "should be verified by at least one verification measure" WARN closed, no new warning introduced). claim_check 37/37. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

…ad drifted Second half of #893. VCR-SEL-005's description still said the gate lowers probes on "BOTH the ARM (Thumb-2) and RISC-V (RV32IMAC) selectors" — it has covered a third, aarch64, since v0.53 (#883). SWVER-017, the verification artifact that is supposed to be the right-side evidence for exactly this requirement, carried the same claim in its title ("ARM vs RISC-V") and described a two-selector ledger. While correcting the backend count I checked the numbers the same documents assert, and both were stale in the same direction — they described gaps that have since CLOSED, which is the flattering direction and therefore the one worth checking: * The roadmap said "the KNOWN_DIVERGENCES ledger is now 5 Zbb + 16 new = 21 entries". The array holds 18: `memory.size`/`memory.grow` closed in v0.50 and `br_table` in v0.53 (#882). * `known_divergences`'s own doc comment said 19 (it had accounted for v0.50 but not #882). * `aarch64_known_divergences`'s doc comment said "leaving the SEVEN below" over an array of 5 — v0.54 (#899) closed `global.get`/`global.set` and removed the entries without updating the prose above them. All four now state what the arrays hold, with the counts' derivation written out so the next drift is visible, and a note at each site that the count must move with the array. The stale-entry check already forces a CLOSED gap to retire its ledger line; nothing forced the PROSE ABOUT the ledger to move with it, which is the #893 defect one layer up. Also recorded, because it is the part of the third-backend leg that is not just "one more backend": aarch64 gets a probed FLOAT/SIMD surface (`a64_extended_surface`, floor `probed >= 100`) that ARM and RV32 structurally cannot have — float is `StructurallyExcluded` from their leg because ARM float lowering is TARGET-parameterized (f32.add declines at fpu=None, lowers at Single/Double) and RV32 has no FPU, whereas the aarch64 backend has one fixed host profile, so both directions are assertable and a stale gap-claim is caught the same way a stale divergence is. Changes are prose and doc-comment only — no test logic touched. `cargo test -p synth-backend-riscv --test cross_backend_op_parity` 8/8, real exit 0. rivet non-external errors still 0; claim_check 37/37. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

…NO roadmap entry README calls artifacts/verified-codegen-roadmap.yaml "the single source of truth for roadmap status". VCR-VER-004 shipped in v0.54 and appeared in the CHANGELOG, the FEATURE_MATRIX template and the CI job list — but the roadmap had no entry for it at all, so the one document the README points at for "what is the state of the VCR-* program" was missing the release's headline validator. The entry records what it is and, more importantly, why it exists: v0.53 showed by mutation that emptying `cfg_exit_observable` makes the compiler leave a return value in the WRONG REGISTER and that BOTH per-compilation validators accept it (`validate_cfg_rewrite` -> Ok, VCR-RA-003 -> Consistent). Only execution caught it. `abi_contract::validate_abi_contract` is not a third file on the same axis — it differs on four axes (an obligation that cannot be emptied because it is `RETURN_CONTRACT_REGS = [R0, R1]` hard-named in its own source; forward rather than backward, so there is no seed whose empty set is a vacuous fixpoint; evidence that is a VALUE compared by greatest-fixpoint bisimulation rather than a name-pair; and a `(orig, rewritten)` signature that takes nothing from the pass). Its honest limit is in the entry, not implied away — all three residuals: (a) it GATES only the flag-off colouring allocator; on the default path it is a report-only audit held to a `Violated 0` CI floor, because gating a user's compile on a checker whose false-positive rate is measured rather than proven is a flip we have deliberately not taken; (b) memory is NOT in its obligation (complementary to `validate_cfg_rewrite`, not redundant with it); (c) THE OP MODEL IS STILL SHARED — def/use extraction runs through `liveness::reg_effect`, so a mismodeled op is a blind spot common to all three instruments. VCR-VER-004 closes the shared-CONTRACT hole, not the shared-OP-MODEL hole, and until `synth-verify`'s `ArmSemantics::encode_op` is pinned against it (VCR-ISA-001's Sail-derived semantics being the eventual anchor, now a typed `traces-to` link rather than a prose aside) "three independent validators" WOULD BE AN OVERCLAIM. Shaped to match its two siblings VCR-VER-003 / VCR-VER-761 exactly: `sys-verification`, `verifies -> VCR-001`, `method: translation-validation`, `preconditions`/`steps`/`pass-criteria`. That inherits two diagnostics those siblings already carry (the schema's `method` allowed-values does not list `translation-validation`, and `pass-criteria` is not a declared sys-verification field) — kept deliberately, because the fix for those is a rivet schema decision about the whole family, not a divergent shape for one member. rivet: 50 errors, non-external 0 (unchanged). Warnings 103 -> 105; the delta is exactly the three new-artifact diagnostics above, and the diagnostic-class diff against the lane's baseline shows no new KIND. claim_check 37/37. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

`synth-backend-aarch64` has not been an integer subset since v0.54. The row now names what actually ships and points at the generated feature matrix for the exact surface rather than restating it (a second copy of that list is how v0.54's cold review found a doc-honesty defect): * the complete scalar f32/f64 surface (v0.54 #898 — rounding, FP memory, i64 converts, guarded i64 truncations); * bounds-checked linear memory (default `--safety-bounds software`, #865); * WASM globals and `call_indirect` with all three §4.4.8 trap guards (v0.54 #899); * direct calls and full control flow. The row is the LAST place in README that described the backend by what it could not do; the intro paragraph and the feature matrix were already current. Note for whoever picks this up next: CLAUDE.md carries a byte-identical stale copy of this row. It is deliberately NOT touched here — that file is agent configuration and is not mine to edit on a lane brief. claim_check 37/37 (the aarch64 rows in the generated matrix are template- driven and unaffected — no generated doc was hand-edited). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

…ane fixed Both defects this lane repaired were sitting in a tree with `Rivet Validation` green. That is not a coincidence — the job's filter had two holes, and each one swallowed exactly one of them. (1) `grep "^ ERROR:"` anchored on two-space-indented lines. rivet prefixes SOME diagnostics with the source file instead (`gale-integration.yaml: ERROR: …`), so that entire class was invisible to the gate — including "artifact id X is declared more than once … the second definition silently overwrites the first". That is how GI-FPU-002 could be `implemented` in one file and `proposed` in another, with rivet resolving it to `proposed`, and nothing complained. (2) The cross-repo exemption `targets '.*:.*' which does not exist` exempted any target containing a COLON. `synth:396` contains a colon. So a broken link in our OWN graph — an issue number written where an artifact id belongs — was classified as an unresolvable link into an un-rivet'd sibling repo and waved through. Fixed structurally rather than by allowlist: every line containing `ERROR:` is now considered, and the exemption is "a target carrying a FOREIGN prefix", with our own `synth:` prefix explicitly added back to the ours-count. A new sibling repo therefore needs no edit here, and our own prefix can never slip back into the exempt set. Failures now PRINT the offending lines instead of only a count, so the next one is self-diagnosing. RED-FIRST, end to end, by replaying this exact step (extracted from the YAML, not paraphrased) against both trees: * pre-fix artifacts (65417c0): exit 1, "Found 2 rivet validation errors that are OURS (not cross-repo)", both named; * fixed artifacts (this branch): exit 0, with the expected cross-repo warning still emitted. CAVEAT, stated rather than assumed: this was verified against local rivet 0.28.0, while the job pins 0.23.0. The duplicate-id diagnostic may not exist in 0.23.0 at all, in which case hole (1)'s fix is latent protection rather than an active check today; hole (2)'s fix is version-independent. If 0.23.0 emits some other filename-prefixed error we cannot see locally, this job is where it will surface — and surfacing it is the point. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

…revealed Flipping GI-FPU-002 from `proposed` to `implemented` made rivet START checking its lifecycle coverage, which correctly reported that the requirement had NO verification artifact at all. The gap was not created by the flip — the wrong status was HIDING it, which is the same failure mode as the duplicate id itself, one rule further down. The evidence already existed and was already named in the requirement's own criteria; it simply had no typed `verifies` link. GI-FPU-VER-002 is that link, and it records what the verification actually is rather than asserting that some exists: * the f32 execution differential (48/48 bit-exact vs wasmtime on cortex-m4f, symbols read from the ELF SYMTAB per #489 rather than from host-dependent `synth disasm` text, FPU genuinely enabled via CPACR + FPEXC.EN); * the HONEST-REJECT direction in the same harness (cortex-m3 must still refuse) — a one-directional differential would pass equally well on a compiler that had quietly widened the FPU gate; * the unit-level pins that need no emulator (AAPCS-VFP S0/S1 homing, the swapped-VCVT signedness fix); * the v0.53 #881 spilled-VFP differential (109 rows, NaN-aware per WASM §4.3.3, internal `bl` resolved by a REAL link so an unresolved relocation cannot be silently skipped as a pass); * and the one part of the surface whose evidence is encoding-level ONLY — the f32 comparisons, because unicorn does not model the VMRS FPSCR→APSR flag transfer. Recorded, not omitted. Deliberately shaped `method: automated-test` + `steps.run`/`steps.coverage` rather than mirroring GI-FPU-VER-001's `method: test` + `pass-criteria`, which produce a WARN and an INFO against the schema. This adds ZERO new diagnostics. MEASURED, prompted by review asking whether `rivet coverage` — the SECOND step of the same CI job, which I had not exercised — moved: rivet coverage, real exit 0 both sides swe1-has-verification (sw-req) 31/60 (51.7%) -> 33/60 (55.0%) swe6-verifies-swe1 32/32 -> 34/34 sys5-verifies-sys2 49/49 -> 50/50 Overall (weighted) 90.3% -> 90.7% VCR-RA-004 and GI-FPU-002 both drop off the "lacking verification" list. Full diagnostic diff for the whole branch vs main is now exactly: −2 ERROR (both ours: synth:396, the duplicate id) −2 WARN (GI-FPU-002 and VCR-RA-004 "should be verified by", both closed) +2 WARN, +1 INFO (all three VCR-VER-004's, all of kinds its sibling sys-verification artifacts already carry) So: errors 52 -> 50 with ours 2 -> 0, and warnings net UNCHANGED at 104. Lifecycle coverage gaps 54 -> 56 — honest, not a regression: GI-FPU-002 and VCR-RA-004 are newly CHECKED because they are no longer `proposed`. Both were absent from the baseline list only because a wrong status exempted them. cargo fmt 0 / clippy 0 / test --workspace 0 (2675 passed) / claim_check 37/37. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

…verage delta Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

…4 named) The prose grouped `local.set`+get and `local.tee` on a param local as one phrase over two separate ledger entries, so the sentence read as four items beside the count 5 — a small instance of exactly the prose-vs-array drift this paragraph exists to prevent. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

L7 correctly declined to touch this on a lane brief (agent configuration, not lane scope) and flagged it instead. Coordinator picking it up. CLAUDE.md carried a byte-identical copy of the stale README row the v0.54 cold review found, plus a third instance nobody had spotted: 1. header: "AArch64 (host-native, integer subset)" — the scalar float surface is complete as of v0.54. 2. crate map: "integer subset" — now i32/i64 core, complete scalar f32/f64, globals, call_indirect, bounds-checked linear memory. 3. VCR-VER-003 note: "AArch64 is N/A (no linear-memory ops in the integer subset)". The VERDICT is still right, the REASON is false — aarch64 has had bounds-checked linear-memory load/store since v0.52 (#865). It is N/A because it emits no data section and REFUSES data-carrying modules loudly (v0.53), so there is no served-vs-runtime image to compare. A correct conclusion resting on a false premise is the harder version of this defect: the sentence reads fine and the reasoning has rotted. Fourth copy of a list this project keeps duplicating (oracle, matrix row, CHANGELOG, CLAUDE.md). Generating the prose from the executable decline list is the standing fix; #911 is the nearest tracked version of it. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

…otted premise 0f0c232 landed the CLAUDE.md half of the aarch64 doc fix but no release note. Adding one — and specifically calling out its third finding, which is the only one of the four that is not a plain stale string: VCR-VER-003's aarch64 N/A note gave a FALSE REASON for a TRUE verdict ("no linear-memory ops in the integer subset" — aarch64 has had bounds-checked linear-memory load/store since v0.52 #865). It is N/A because it emits no data section and refuses data-carrying modules loudly, so there is no served-vs-runtime image to compare. That failure mode deserves the note more than the two string copies do: a stale "integer subset" reads wrong and invites a check, whereas a correct conclusion resting on a rotted premise still reads fine, so nothing prompts one. Both underlying facts re-verified against the generated feature matrix before writing this. claim_check 37/37 (CLAUDE.md is pinned by three ledger entries; unaffected). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

codecov · 2026-08-05T17:25:48Z

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!

# Conflicts: # CHANGELOG.md

avrabe and others added 13 commits August 5, 2026 18:02

docs(CHANGELOG): v0.55 L7 — traceability repair + the honest-N/A backlog

f810b1a

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

docs(CHANGELOG): record the two verification artifacts + the rivet co…

3e99332

…verage delta Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

merge: origin/main into lane/v0.55-L7-traceability

4d55a35

# Conflicts: # CHANGELOG.md

avrabe merged commit 1c35b08 into main Aug 6, 2026
56 checks passed

avrabe deleted the lane/v0.55-L7-traceability branch August 6, 2026 12:38

Navigation Menu

Uh oh!

L7: traceability repair — rivet ours-errors 2 → 0, VCR-RA-004/SEL-005 de-staled, VCR-VER-004 filed (#893) - #913

L7: traceability repair — rivet ours-errors 2 → 0, VCR-RA-004/SEL-005 de-staled, VCR-VER-004 filed (#893)#913
avrabe merged 14 commits into
mainfrom
lane/v0.55-L7-traceability

avrabe commented Aug 5, 2026 •

edited

Loading

Uh oh!

codecov Bot commented Aug 5, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

avrabe commented Aug 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

rivet: non-external errors 2 → 0

What was wrong, and what I decided

VCR-VER-004 now exists in the roadmap

The finding the brief did not anticipate: the gate could not see either error

Also

Gates (real exit codes, local)

Uh oh!

codecov Bot commented Aug 5, 2026

Codecov Report

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

avrabe commented Aug 5, 2026 •

edited

Loading

`VCR-VER-004` now exists in the roadmap