release(v0.62.0): "Reach is part of correctness" — 9 artifacts, 8 implemented

[avrabe]

v0.62.0 — "Reach is part of correctness"

Release assembly: version bump, pin sweep, and the [0.62.0] CHANGELOG entry.

9 artifacts, 8 implemented. RQ-62-REACH stays proposed deliberately —
its done-when names an 805-module census, this release delivered a 243-module
reachable subset, and the artifact records the gap rather than claiming the
status.

What this PR contains

• 0.61.0 → 0.62.0 across Cargo.toml (workspace + 10 path-dep pins),
  MODULE.bazel, npm/package.json, artifacts/status.json, Cargo.lock
• CHANGELOG.md [0.62.0]
• docs/status/FEATURE_MATRIX.md + artifacts/status.json regenerated via
  claim_check.py claims.yaml --emit-status

Notes derivation

Written against merged code and claims.yaml on the tree, not PR bodies —
the v0.57 cold review found four errors in same-author release prose derived the
other way. Every load-bearing number was re-derived in this session, including
four that came from commit prose and were checked against the shipped scripts:
MIN_DERIVED_SLOTS = 4, MIN_ONLINE = 2, 30 loop-conformance unit tests, and
runs-on: [self-hosted, linux, x64, light].

Two things the notes say that the release would rather not

1. It subtracted nothing. 6,871 insertions against 22 deletions.
2. The subtraction ratchet moved the wrong way. selector_lines_code
   19,213 → 19,227 (+14), waived, bound to the exact value, reason printed in
   claims.yaml. The +14 is the Multi-memory phase 2: per-memory MPU isolation is unreachable — --safety-bounds mpu and multi-memory have disjoint paths #1145 decline stating its root cause at the
   decline site; nothing could be deleted in exchange, because the decline is
   the only handling that class has. Every other pin is flat.

A reach-and-gates release should look like one in the metric that exists to
detect it. Recorded rather than smoothed over.

Gate state

• claim gate 58/58
• pin sweep OK — path-dep pins + MODULE.bazel + Cargo.lock + npm all at 0.62.0
• loop-conformance step 0 (release identity) cleared by this bump
• loop-conformance step 7 (clean-room review) is being run now; its record lands
  in docs/reviews/v0.62-cold-review.md before the tag

Refs #242, #1017, #1062, #1102, #1131, #1132, #1133, #1136, #1143, #1145

[avrabe]

Release-review finding, fixed in b9450a66: the emulation floor had 1,892 of slack

Found while cutting this release, on this release's own new oracle.

The #910 ratchet's stated purpose is to catch "an oracle lost execution". It
enforced --min-emulation-floor 322754 against a declared total of 324640
at v0.61.0 and 324646 here. That slack is larger than most single oracles
declare — so an oracle could stay wired, stay referenced, and drop to zero
executions while the gate built to notice that stayed green.

Demonstrated in an isolated worktree rather than reasoned about:

mutation	before the bump	why
delete mem_isolation_red_1145.py whole	exit 1	caught by the dangling-CI-reference check, not the floor — total only fell to 324,640, still above 322,754
oracle stays wired, declares emulations >= 0	exit 0 — green	the ratchet's own failure mode, invisible
same mutation, after the bump	exit 1	RATCHET BROKEN: 324640 < 324646

Control (unmutated tree, tightened floor) stays exit 0, so the new floor is not
merely stricter — it's correct.

Two mechanisms guard this oracle set and they catch different things:
referential integrity catches deletion; the floor is supposed to catch
execution loss. Only the second is the ratchet's job, and it was the one
that couldn't fire.

The slack was inherited, not introduced here — it had simply never been
tightened when oracles landed. The fix pins the floor equal to the declared
total, so there is no slack to hide in, with the invariant written at the step:
a landing oracle bumps both in the same PR.

claims.yaml's SYNTH-ORACLE-CHECK-FLOORS-910-CI verbatim pin caught the edit
(57/58) before it could ship silently — the pin working exactly as designed.
58/58 after.

Note for the cold review record

The independent review was dispatched against 0a8c1e1f and will name that
commit. b9450a66 landed after it started and contains only this floor fix
plus its CHANGELOG entry and pin update. The review record will say so rather
than silently claiming to have covered it.

[avrabe]

Independent cold review complete — and both actionable findings were mine

Record committed at docs/reviews/v0.62-cold-review.md (reviewer's text
unedited; a disposition table is additive). Dispatched with no inherited
framing against 0a8c1e1f.

1 MUST-FIX · 1 SHOULD-FIX · 5 NOTEs · 4 unverifiable-as-stated · ~20 claims
verified by execution.

What it did to verify, rather than read

• Rebuilt synth from the branch and re-ran the whole acceptance census on all
  three backends over the artifact's corpus roots — 27/243, 40/243, 46/243, every
  stratum, every ranked blocker (including multi-memory 50/50/0 and the aarch64
  inversion at 31% of core), zero timeouts, partial bucket zero. Reproduced exactly.
• Rebuilt the pre-fix compiler (858ff8d0^) in an isolated worktree to
  reproduce the rv32: a retained function relocating against a declined INTERNAL emits a dangling synth_func_N and exits 0 — the #851 guard #1013 gave aarch64 is not on the RISC-V path #1102-residual hole end-to-end: object ships exit 0,
  arm-none-eabi-ld links it clean, nm -u shows zero UNDEF symbols. Real.
• Proved the new P1 status rule potent by injecting a violation (red, then
  green on restore) in a throwaway worktree.

Both actionable findings, fixed — not waived

MUST-FIX — the tip failed its own required Claim Check. My floor-fix commit
was delivery-shaped with no artifact or issue anchor, so R10 refused it — the
rule added in #1124 for exactly this shape, firing on its author. Fixed by
giving the work the artifact it deserved (RQ-62-FLOORTIGHT, carrying the
finding and its red-first evidence) rather than loosening the rule or bolting a
landed: onto an unrelated artifact. Now exit 0, 2 delivery commits — 2 attributed.

SHOULD-FIX — a false claim I wrote, in three files. Release prose said the
dynamic index was load-bearing because "a constant index devirtualizes and the
table never materializes." I re-verified against emitted bytes before acting
rather than taking the review's word:

movw  r2, #0          ; the constant, materialized
cmp   r4, ip / bcc    ; bounds check still emitted
ldr.w ip, [fp, ip]    ; RUNTIME TABLE LOAD
blx   ip              ; INDIRECT CALL

It does not devirtualize — synth has no such pass at all. Corrected in
CHANGELOG.md, RQ-62-TABLEDANGLE.yaml and tabledangle_1102_elem.rs, each
as a stated correction so the wrong rationale can't be re-derived from
history. The fix, its red-first evidence, and the dynamic-index fixture are
unaffected — only the rationale was wrong. That's the dangerous shape: a
correct artifact resting on a plausible reason nobody checked, and the reason is
what the next contributor reasons from.

NOTEs 1, 3, 4 applied — each narrowing a sentence that claimed too much

• diff-stat scope now stated (feature merges; release commit +213/−51 named)
• the 81%→11% comparison now says the denominator differs (307 vs 243), that
  the subcounts come from the v0.59 artifact rather than this release, that
  per-module records weren't preserved, and that the 125 and 77 may overlap
• "fail-closed on unknown mnemonics" now says what the code does: undecodable
  instructions and zero-instruction scans always refuse; an unknown mnemonic
  refuses only when its operand text names a reserved register

NOTE 5 (census hex-immediate collapse) is deliberately not fixed here,
and the disposition says why: no number in the release is wrong, and changing a
measurement script mid-cut under the oracle it feeds risks the census for no
gain. Carried to v0.63, where re-measurement is increment 1.

Branch anchor re-cut

The two mid-review commits were collapsed into one attributed commit. Tree hash
captured before and after — identical (24d0c109…), so the rewrite lost
nothing.

Gate state

status_evidence_check 0 · claim_check 58/58 · oracle_wiring_check
0 at the tightened floor · loop-conformance step 7 DERIVED-PASS, one slot
left (MC/DC on commit, waiting on CI).

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!