chore(release): v0.60.0 assembly — "Derive what you check against, and reach is part of correctness"

[avrabe]

Release assembly for v0.60.0 — "Derive what you check against, and reach is part of correctness." Refs #242, #1091.

One assembly commit rather than v0.59's two, because each PR costs a full nine-context CI cycle and six of those nine queue behind a single GitHub-hosted pool (#1062).

1. CHANGELOG [Unreleased] gains the v0.60 entries, written from merged code rather than PR bodies — the practice that caught four attribution errors in the v0.57 notes.
2. Pin sweep 0.59.0 → 0.60.0: 30 occurrences across 13 manifests; Cargo.lock regenerated.
3. status.json + FEATURE_MATRIX.md regenerated with claim_check.py claims.yaml --emit-status, never hand-edited.
4. [Unreleased] cut to [0.60.0] - 2026-08-27.

What the notes say that a flattering version would not

• AArch64 acceptance is UNMEASURED since RQ-60-A64IMPORT (VCR-REACH-002 inc. 1): aarch64 import dispatch — SHN_UNDEF externals, the ARM #197 contract ported. Refs #1017, Refs #242 #1071. The import-dispatch blocker is closed with execution evidence (ld.lld + unicorn: run(37)=42 through the import), but the 805-module census has not been re-run — the corpus is not synth-local. Requested at Real-world corpus (805 modules): arm accepts 66%, aarch64 1.6% — priority ranking + an 8-module sample to work against #1017. No reach improvement is asserted.
• The subtraction ratchet moved the wrong way on three directed pins, with sel_dsl_rules flat at 80:

  selector_lines_code        19199   baseline 17897   +1302   must FALL
  mirror_marker_files           60   baseline    57      +3   must FALL
  mirror_obligation_files       24   baseline    23      +1   must FALL
  sel_dsl_rules                 80   baseline    80      +0   must RISE
  

• selector_lines_code's waiver count moved 9 → 10 with the value unchanged — a destroyed record restored (claims.yaml has a duplicate reason: key: a +622-line waiver is recorded with a +10-line justification, and claim_check passes #1087), not a further growth permitted. Those two look identical in a summary table and are opposite events.
• RQ-60-CANARY's code shipped in v0.59.0 (gate merged 08:50, v0.59.0 tagged 15:19, the v0.60 plan written 18:56 scoping it as future work). v0.60 carries its traceability closure, not the capability.
• "66 shrink / 0 grow" is a measurement, from a script that declares itself ci-status: manual and carries no verdict. What is CI-gated is the allocator's correctness.
• The V is not closed on the right-hand side (The traceability completeness gate has never fired: 60/60 release artifacts across v0.56-v0.60 have no linked sys-verification, and 'rivet coverage' prints instead of asserting #1091): 60 of 60 release artifacts across v0.56–v0.60 carry no verifies link, and rivet coverage prints 40.1% and exits 0 rather than asserting. The verification exists in every case; the typed link does not.

Numbers, re-derived against origin/main

proof inventory ....... 138 constructors, 138 Qed, 63 result-correspondence (75 existence-only)
Rocq suite ............ 630 Qed / 2 Admitted
v0.60 scope ........... 8 artifacts — 7 implemented, 1 verified

Gates on this tree

claim_check 52/52 · check_version_pins OK at 0.60.0 · status-evidence 0 failures
proof_inventory --check ok · test_claim_check OK · test_status_evidence OK

The pin sweep was rehearsed and discarded in a scratch worktree before being applied here, and the first attempt was caught on a stale base (51/51 instead of 52/52) by the generated-file staleness gate.

Not tagged by this PR. Tagging and publishing require explicit maintainer authorization.

🤖 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!