VCR-REACH-001: close the cold-review blockers — A32 sweep, un-vacuate the evidence oracle, scope the mutation claim (#242)

Three corrections from review, two of them blocking.

1. THE WIDENED SHIPPING VALIDATOR, CHECKED ON THE PATH I HAD NOT COMPILED.
   `check_join_availability` now admits i64-pair ops and takes their defs from
   `pair_effect` — and its `use_b` comes from the same line. That matters,
   because `pair_effect` lists `rm_hi` in `uses` DELIBERATELY (conservative for
   the pass: it keeps the incoming value live INTO the op, which is strictly
   more interference). Over-stating `uses` is safe for interference; inside a
   MUST availability fixpoint that HARD-ERRORS the compile, it is the
   false-positive direction. The thumb2 corpus sweep found 0 hard errors, but
   the A32 expansions are entirely different code (`encode_arm_expanded`) and I
   had never compiled it. Now swept: `--target cortex-r5`, both the relocatable
   and self-contained paths, 293 successful compiles, **0 RA-003 hard errors**,
   and the same coverage improvement (Consistent 563 / NotAttempted 79).

2. `rivet check verification-evidence` WAS PASSING VACUOUSLY — repo-wide, and
   before this lane. It reported `named_test_steps_checked: 0` while 31
   artifacts carry a `cargo test` step. Root cause found by bisecting the shape:
   the oracle scans `fields.steps[].run`, a SEQUENCE, and every artifact in this
   repo writes `steps:` as a MAPPING, so it matches nothing and exits 0. A green
   gate that checked nothing is precisely the class this project pins, and I had
   cited it as evidence in the previous commit — that citation was wrong.
   SWVER-022 is now written in the shape the oracle actually reads, taking it
   from 0 checked to 1, and the check is verified RED-FIRST: substituting a
   nonexistent test name makes it exit 1 and name the artifact, filter and
   command. Converting the other 42 is a FOLLOW-UP, not a drive-by: each
   conversion has to re-verify that its filter still matches a real test, which
   is the entire point of the oracle. Second, smaller finding recorded with it:
   a source with a YAML parse error is silently skipped and the oracle still
   reports `ok: true`.

3. THE MUTATION CLAIM IS NOW SCOPED TO WHAT IT COVERS. "Proven non-vacuous by
   mutation" followed by one example invites the reader to generalise it to the
   whole model. The model carries THREE obligations and only ONE is
   execution-gated:
     * EARLY-CLOBBER edges — yes, strongly (3 static instruments green, only
       execution red, 3 wrong values).
     * The `rm_lo` RMW clobber — defended by `rewrite_op`'s RMW-agreement check,
       NOT by execution. And that guard was written in this same lane alongside
       the model it constrains, so it is the model catching its own
       inconsistency, not independent detection. Said plainly now.
     * The `rm_hi` scratch clobber — NOT caught. Belt-and-braces.

Also, per this repo's convention that a gap claim should not outlive the gap:
the latent Thumb encoder defect this lane found is now issue **#916** with a
full reproduction, the reason #311's fix does not transplant (fixed internal
branch displacements), and a suggested acceptance gate — referenced from the
CHANGELOG, from `pair_low_reg_only`'s doc and from the pinning test, so the
follow-up lane has a home.

And one characterisation the review asked for: `identity-colouring` nearly
doubled, 31 -> 58. About 27 newly-admitted functions are fully modeled and fully
validated and then colour to identity, so they go straight back to the shipping
pass. Honest behaviour, and the cheapest reach left — a candidate for the next
increment alongside the leaf-only `shrink_callee_saved_saves` lever.

Gates: fmt 0, claim_check 37/37, the pinning test 0, `rivet check
verification-evidence` 0 with 1 step genuinely checked, rivet validate 52
errors / 103 warnings against the 52 / 104 baseline.

Trace: VCR-REACH-001

Author: avrabe

CHANGELOG.md

@@ -37,8 +37,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   converts into bytes almost entirely through `shrink_callee_saved_saves`, which
   is LEAF-ONLY. **Still flag-off, and the flip criterion is no closer on bytes.**
 
-- **Latent miscompile found and pinned (not fixed): the i64 shift zero-fill
-  mis-encodes for a high destination.** `I64Shl`/`I64ShrU`'s Thumb expansions
+- **Latent miscompile found and pinned, not fixed (#916): the i64 shift
+  zero-fill mis-encodes for a high destination.** `I64Shl`/`I64ShrU`'s Thumb expansions
   zero a half with the 16-bit `MOVS` T1 form, `0x2000 | (rd << 8)`, whose `rd`
   field is three bits — for R8 that is `0x2800`, i.e. `CMP r0, #0`, and the half
   is never zeroed. Same class as #180 / H-CODE-9, and the same one #311 already
@@ -72,19 +72,42 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - The i64-pair model is stated ONCE (`liveness::pair_effect`) and consumed by the
   pass, `validate_cfg_rewrite`, the ABI observable contract and VCR-RA-003 — so
   no static instrument can catch an error in the model itself. The new shapes are
-  therefore EXECUTED against wasmtime, and the coverage is proven non-vacuous by
-  mutation: deleting the early-clobber interference edges lets the colourer
-  coalesce `I64Ldr`'s `rdlo` onto a base the second `LDR` re-reads —
-  `validate_cfg_rewrite`, VCR-RA-003 and the ABI contract are ALL green on all
-  seven functions, and only execution fails it. A third counterexample to the
-  idea that per-compilation validation is an independent check on codegen.
-- Honest residual, reported because a mutation matrix that lists only its
-  successes is not evidence: the coherent "model omits `rm_hi`" mutation is NOT
-  caught, even against two purpose-built register-pressure fixtures. The
-  churn-minimising colour bias fills R0–R3 first and the shift-amount pair sits
-  in callee-saved R4–R8, so no live web is ever placed on the original `rm_hi`
-  register. That half of the clobber model is sound and cheap but currently
-  belt-and-braces rather than execution-gated.
+  therefore EXECUTED against wasmtime. **Precisely which obligation that gates:**
+  the model carries three, and only ONE of them is execution-gated.
+  - The EARLY-CLOBBER edges — yes, and strongly. Deleting them lets the colourer
+    coalesce `I64Ldr`'s `rdlo` onto a base the second `LDR` re-reads;
+    `validate_cfg_rewrite`, VCR-RA-003 and the ABI contract are ALL green on all
+    seven functions and only execution fails, with 3 wrong values. A third
+    counterexample (after v0.53's and v0.54's) to the idea that per-compilation
+    validation is an independent check on codegen.
+  - The `rm_lo` RMW clobber — defended by `rewrite_op`'s RMW-agreement check,
+    NOT by execution. Dropping it makes the rewrite unrepresentable and every
+    shift function declines. Worth having, but that guard was written in this
+    same lane alongside the model it constrains, so it is the model catching its
+    own inconsistency rather than independent detection.
+  - The `rm_hi` scratch clobber — NOT caught, and this is reported because a
+    mutation matrix that lists only its successes is not evidence. The coherent
+    "model omits `rm_hi`" mutation stays green even against two purpose-built
+    register-pressure fixtures (four and eight i32 values live across the shift):
+    the churn-minimising colour bias fills R0–R3 first and the shift-amount pair
+    sits in callee-saved R4–R8, so no live web is ever placed on the original
+    `rm_hi` register. Sound and cheap, but belt-and-braces rather than gated.
+- `identity-colouring` nearly doubled, 31 → 58: about 27 newly-admitted functions
+  are fully modeled and fully validated and then colour to identity, so they are
+  handed straight back to the shipping pass. That is honest behaviour, and it is
+  also the cheapest reach left on the table — a candidate for the next increment
+  alongside the leaf-only `shrink_callee_saved_saves` lever.
+- Found while adding this lane's own verification artifact, and pre-existing:
+  `rivet check verification-evidence` was VACUOUS repo-wide. It scans
+  `fields.steps[].run` (a sequence) while every artifact here writes `steps:` as
+  a mapping, so it reported `named_test_steps_checked: 0` while 31 artifacts
+  carry a `cargo test` step — and passed green. SWVER-022 is written in the shape
+  the oracle actually reads (verified red-first: a nonexistent test name makes it
+  exit 1), which takes it from 0 checked to 1. Converting the other 42 is a
+  follow-up, because each conversion has to re-verify that its filter still
+  matches a real test — which is the entire point of the oracle. Separately, a
+  source with a YAML parse error is silently skipped and the oracle still reports
+  `ok: true`.
 - Still declined, by name, with the histogram to prove it: `single-block` 73,
   `unmodeled-op` 61 (the i64 div/rem software loops, rotates, `I64Mul`,
   popcnt/clz/ctz, the narrow sign-extends, `MemorySize`/`MemoryGrow`),

artifacts/sw-verification.yaml

@@ -577,17 +577,30 @@ artifacts:
         target: VCR-DEC-001
     fields:
       method: automated-test
+      # `steps:` is a SEQUENCE here, not the mapping every other artifact in
+      # this repo uses. That is deliberate, and it is a FINDING rather than a
+      # style choice: `rivet check verification-evidence` scans
+      # `fields.steps[].run`, so the mapping shape makes it scan NOTHING — it
+      # reports `named_test_steps_checked: 0` repo-wide while 31 artifacts carry
+      # a `cargo test` step, and passes green. A gate that checks nothing is the
+      # exact class this project pins. Written in the shape the oracle actually
+      # reads, so at least THIS entry's test filter is verified to exist; the
+      # other 42 artifacts are a follow-up, because each conversion has to
+      # re-verify that its filter still matches a real test — which is the point.
       steps:
-        run: "cargo test -p synth-backend --lib i64_shift_zero_fill_mis_encodes_for_a_high_destination && cargo test -p synth-cli --test frozen_codegen_bytes"
-        differential: >
-          SYNTH=./target/debug/synth python3
-          scripts/repro/vcr_dec_001_join_alloc_execution_differential.py — CI-wired
-          (`set -euo pipefail`, awk asserts CHECKS non-zero and all-passing,
-          ENGAGED non-zero, CALLSHAPES >= 4, PAIRSHAPES >= 4, SHIFTSHAPES >= 2)
-        coverage: >
-          100/100 execution checks over 28 engaged functions (6 call shapes,
-          9 i64-pair shapes, 6 of those carrying a real i64 shift expansion);
-          frozen anchors 10/10 and all 633 pre-existing relocatable + 1059
-          self-contained corpus functions byte-identical to v0.54 with the flag
-          off; VCR-RA-003 join availability Consistent 440 -> 560 of 640 on the
-          DEFAULT build with 0 hard errors across the corpus
+        - run: "cargo test -p synth-backend --lib i64_shift_zero_fill_mis_encodes_for_a_high_destination"
+        - run: "cargo test -p synth-cli --test frozen_codegen_bytes"
+        - differential: >
+            SYNTH=./target/debug/synth python3
+            scripts/repro/vcr_dec_001_join_alloc_execution_differential.py — CI-wired
+            (`set -euo pipefail`, awk asserts CHECKS non-zero and all-passing,
+            ENGAGED non-zero, CALLSHAPES >= 4, PAIRSHAPES >= 4, SHIFTSHAPES >= 2)
+        - coverage: >
+            100/100 execution checks over 28 engaged functions (6 call shapes,
+            9 i64-pair shapes, 6 of those carrying a real i64 shift expansion);
+            frozen anchors 10/10 and all 633 pre-existing relocatable + 1059
+            self-contained corpus functions byte-identical to v0.54 with the flag
+            off; VCR-RA-003 join availability Consistent 440 -> 560 of 640 on the
+            DEFAULT build with 0 hard errors across the corpus (thumb2 AND the
+            cortex-r5 A32 path, whose expansions differ)
+

crates/synth-backend/src/arm_encoder.rs

@@ -11642,7 +11642,7 @@ mod tests {
         assert!(code.len() >= 4, "I64Xor should emit at least 4 bytes");
     }
 
-    /// VCR-REACH-001 side finding — the i64 shift expansions' zero-fill uses the
+    /// #916 (VCR-REACH-001 side finding) — the i64 shift expansions' zero-fill uses the
     /// 16-bit Thumb `MOVS` T1 form, whose `rd` field is THREE bits, so a
     /// destination in R8-R12 does not encode a `MOV` at all.
     ///

crates/synth-synthesis/src/liveness.rs

@@ -3917,8 +3917,8 @@ pub fn pair_early_clobber(op: &ArmOp) -> bool {
 /// the 32-bit `MOV.W` the way #311 fixed `I64SetCond`, because these expansions
 /// are hand-emitted halfwords with FIXED internal branch displacements
 /// (`B .done` = `0xE002`, two halfwords) that a 4-byte instruction would
-/// overshoot — so this is reported as a latent encoder defect and the allocator
-/// is kept from REACHING it, rather than papered over here.
+/// overshoot — so this is filed as a latent encoder defect (#916) and the
+/// allocator is kept from REACHING it, rather than papered over here.
 ///
 /// The pass uses this to (a) block R8 as a colour for the named operand and
 /// (b) DECLINE outright when the incoming stream already has a high register