[avrabe]

#923 — measured first, and the measurement changed the plan

cargo llvm-cov --workspace with CI's exclusion set, classified per file by
whether an out-of-process execution oracle asserts it:

class	lines	instrumented-covered
differential	50238	86.2 %
unit-only	47754	83.4 %
TOTAL	97992	84.8 %

The issue's hypothesis was that differential-covered files get dragged down
because llvm-cov instruments in-process while the differentials spawn
synth separately. At the aggregate that is not what the data shows —
differential-asserted files read slightly higher. The effect is real per-file
(synth-backend-aarch64/src/backend.rs: 267 lines, 44.2 %, exercised
end-to-end constantly) but it does not dominate; 6945 uncovered lines sit in
differential-asserted files.

The measurement also named the real target, and it is not the one expected:
synth-verify/src/arm_semantics.rs — 2481 lines at 47.4 %, unit-only, the
largest genuine gap in the workspace. Tests there add evidence; tests written
to lift the aarch64 backend's number would not. That makes step 2 of the issue
a targeted job instead of a vague one.

codecov.yml (validated against codecov's own endpoint — Valid!)

• project target 80 %, threshold 1 % — a floor met today with headroom, so
  a red project means coverage genuinely fell, not "a PR touched an awkward
  file". Ratchet up as the arm_semantics.rs gap closes.
• patch informational: true, explicitly. Not a surrender: a patch
  status cannot distinguish "untested" from "asserted by a differential the
  instrument cannot see", so until VG-009 lands it reports a number it has no
  way to make true. It still posts — it just stops pretending to be a gate.

An ignored red is worse than no check; it's the reflex that let a red Clippy
through as "just codecov" (#683).

Three deferrals to v0.57 — logged, not silent

artifact	why
RQ-56-GPIO (#846)	changes shipping bytes for a 4-byte win; wants frozen anchors + the gpio differential re-pinned in its own gated lane
RQ-56-A64PARAM (#851)	capability work needing its own execution differential across the 4 named divergences
RQ-57-I32CONST (#933)	new artifact — the issue had none, and an untriaged issue is invisible to the plan. A Rocq contract change across 9 .v files under the repo's own #166 gate ("never weaken a theorem to force a Qed"), with a long hermetic verify loop

rivet validate, replaying the CI job's OURS-not-theirs filter: 0 errors,
same as main. My first draft of RQ-57-I32CONST added one — a derives-from
link with no target — caught by running it rather than assuming.

Refs #923, #846, #851, #933

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!