release(v0.58.0): "Delete the thing you replaced"

[avrabe]

All 11 of 11 RQ-58-* artifacts are implemented and merged, so the release-readiness query over artifacts/release-v0.58.yaml is satisfied.

The release in one number

	v0.57.0	v0.58.0
Rocq-verified selection rules	50	74
…each with a 1:1 correctness theorem	50	74
Rocq Qed (whole suite)	592	617
selector, non-test region	18,480	17,961
selector wildcard arms, non-test	62	55
selector, total lines	29,616	28,582

The first release in the epic's history where the selector shrank while the verified rule count grew. From v0.42.0 → v0.57.0 it had gone the other way: 24,909 → 29,616 lines (5,515 added / 808 deleted, 6.8:1) while verified rules went 40 → 50 and sat flat for twelve releases.

Every number re-derived from merged code

Not from PR bodies — v0.57's cold review found 4 factual errors in release prose written the same way, by the same author. Sources: coq/vcr_sel_rules.manifest and VcrSelRules.v at tag vs HEAD; the coq/Synth tree; the selector files measured with the ratchet's own region marker.

Two corrections the cold review caught in my own draft:

1. The v0.57.0 baseline is 18,480 / 62 wildcards, not 18,582 / 63. The latter pair is the METRIC pin's creation value — measured mid-v0.58 after fix(#973): ARM select on an i64-comparison returns the then-arm — and an ARM leg for the corpus CI never compiled #992 grew the file — not the v0.57.0 release value. I had carried the wrong pair through several working notes. Re-measured at the tag with the ratchet's own marker (#[cfg(test)]\nmod tests, asserted unique) so the delta is like-for-like.

2. The SPLIT bullet originally read "the root file went 29,616 → 18,284." True release-over-release, but it credits SPLIT with a drop that RETIRE (−1,312) and SELDSL (−79) partly produced. Corrected to SPLIT's own effect: 10,298 lines moved out, 28,533 → 18,284. A locally-true sentence with wrong attribution — the same shape as all four v0.57 errors.

Contents

• Version pin sweep across all four surfaces + Cargo.lock — check_version_pins.py exits 0 at 0.58.0 (30 replacements, 13 files).
• Regenerated artifacts/status.json + docs/status/FEATURE_MATRIX.md via --emit-status.
• Rivet: RQ-58-OBJECT and RQ-58-SPLIT → implemented, completing 11/11.
• CHANGELOG: the v0.58.0 entry.

Gates

claim_check.py 49/49 · check_version_pins.py 0 · model_coverage_audit.py --check 0 · cargo fmt --check 0.

Refs #242.

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!