VCR-DEC-001 increment 4 (VCR-REACH-001): the allocator models the i64 register-pair ops — 316→411 applied, measured (#242) - #917
Merged
Conversation
…er-pair op model (#242) Traceability leads. Increments 2 (joins, v0.53) and 3 (calls, v0.54) both returned DO NOT FLIP for the same reason — the limiting factor is REACH, not soundness. This artifact states increment 4's requirement, its method, and its acceptance criteria BEFORE the code. The evidence that picks the target: a per-function census of WHICH ops force `unmodeled-op` (the complete set per function, not just the first blocker, gathered by instrumenting `joins::build_cfg`'s admission loop) attributes 167 of the 175 declines to ONE coherent family — the i64 register-pair pseudo-ops (`I64Const` 96 functions, `I32WrapI64` 61, `I64Shl` 51, `I64Ldr` 36, `I64ShrU` 28, `I64Str` 28, `I64SetCond` 22, long tail); the residual 8 are `MemorySize` / `MemoryGrow`. `unmodeled-op` is 47 % of all declines on the 633-function corpus. Two method constraints are written into the requirement because getting either wrong is a silent gate failure: * A NEW shared definition (`liveness::pair_effect`), never a widened `reg_effect`. `reg_effect` returns `None` for these ops DELIBERATELY and the SHIPPING pipeline depends on that `None` — `local_dead_defs`, `reallocate_function` (default-on since v0.24.0), the range-realloc pass and `fuse_cmp_select`'s dead-by-redef check all bail on it. Widening it would hand the greedy/segment allocator streams it has always refused and break the frozen anchors. Increment 3's `call_effect` is the pattern. * The model is verified against the ENCODER, not the IR declaration. These are pseudo-ops expanded downstream — the exact class increment 3 declined `Call`/`CallIndirect` for. Three checks per op: FOOTPRINT (an operand used as a scratch temp, e.g. `I64Shl` overwrites `rm_lo` via `AND rm_lo,rm_lo,#63` and clobbers `rm_hi`), IMPLICIT DISTINCTNESS (a `RegEffect` structurally cannot say "these two must differ" — `I64Ldr`'s second `LDR rdhi,[base,#4]` re-reads a base the first load may have been coalesced onto), and RENAME-INVARIANCE (hand-emitted halfwords with fixed internal branch offsets; any 16-bit register form is the #180/#311 mis-encode class). An op failing a check keeps its decline, RENAMED — the decline moves, it is never deleted. rivet validate: 52 errors / 105 warnings, unchanged from the 52/104 baseline except this artifact's own "needs a verifies link" warning, which every peer VCR-* sw-req also carries; the verification artifact lands with the tests. Trace: VCR-REACH-001
…e instruments (#242) Increment 4's target, chosen by census: `unmodeled-op` was 175 of the 633-function corpus's declines (47 % of all of them), and a per-function census of the COMPLETE unmodeled set (not just the first blocker) attributes 167 to one family — the i64 register-pair pseudo-ops. `liveness::pair_effect` is a NEW definition, not a widened `reg_effect`. `reg_effect` returns `None` on these ops deliberately, and the SHIPPING pipeline depends on that `None` (`local_dead_defs`, `reallocate_function`, `straight_line_value_ranges`, `fuse_cmp_select`'s dead-by-redef scan, `validate_final_allocation`'s fail-safe invariant 1). Widening it would hand the greedy/segment allocator streams it has always refused and move the shipped bytes. This mirrors increment 3's `call_effect` exactly, and the flag-off corpus byte totals confirm it: 41438 relocatable / 49930 self-contained, both unchanged to the byte, frozen anchors 10/10. THREE instruments consume the one definition — the pass (`graph_alloc::joins` liveness / interference / webs), `validate_cfg_rewrite`'s backward transfer, and VCR-VER-004's `abi_contract` forward value graph. Wiring the pass alone would be #872 verbatim: a validator that walks an i64 shift as if it were effect-free certifies its own pass's "live value parked in the shift amount's register" miscompile. Note the abi_contract wiring is NOT optional caution — its `NotAttempted` is a DECLINE at the gate, so omitting it would have switched that instrument off for the entire family this increment reaches. THE MODEL IS READ OFF THE ENCODER, both paths (Thumb-2 `encode_thumb` and A32 `encode_arm_expanded`), never off the IR declaration: * FOOTPRINT. `I64Shl`/`I64ShrU`/`I64ShrS` open with `AND rm_lo, rm_lo, #63` and use `rm_hi` as a pure scratch temp (`SUBS rm_hi, rm_lo, #32`, written before ever read) — the IR field is even commented `// used as temp`. Both are DEFS. `I64Ldr`/`I64Str` additionally DEFINE R12 on the index-register form (`ADD ip, base, rm`); R12 is outside the pool and identity-assigned, so it cannot change a colour — modeled anyway, because an effect function accurate only where inaccuracy happens not to bite stops being true. * DISTINCTNESS, which a `defs`/`uses` pair structurally cannot express. `I64Ldr` is `LDR rdlo,[base,#off]; LDR rdhi,[base,#off+4]`: coalescing `rdlo` onto `base` — which a plain interference graph does the moment `base` is dead after — makes the second load read a clobbered base. Carried by `pair_early_clobber` as interference EDGES (def-web vs every web reaching a use at the same instruction), never by widening `defs`, which would also cost spurious `DefClobbersEquation` rejections. ONE rule, and it is PROVABLY SUFFICIENT: every pair in the hand-derived table (enumerated in the doc comment, both encoders, all ten `I64SetCond` arms) is either two defs of one instruction — already separated by the existing co-def clique — or a def against a use of that instruction, which is exactly what early-clobber adds. `I32WrapI64` is the single documented exception (one `MOV`, elided to a `NOP` in place; 61 functions, overwhelmingly emitted in place). * The shift distinctness constraints are PATH-DEPENDENT — the offending re-read sits on one side of a runtime `BPL` on the dynamic shift amount, so a violation is correct for n >= 32 and wrong for n < 32. Any execution oracle for this family must drive both sides of that branch. Also widened: increment 1 requires a `reg_effect` on every instruction, so a SINGLE-BLOCK function containing a pair op was reachable by neither path. Measured, not hypothetical — the model moved 114 relocatable functions out of `unmodeled-op` and 96 landed straight in `single-block` until the increment-3 `has_call` exception was extended to `has_pair`. MEASURED (633-function ARM repro corpus, ELF symtab bytes, --emit-wcet bounds): relocatable applied 316 -> 399 bytes -100 -> -110 wcet -33 (0 regressions) self-contained applied 113 -> 192 bytes -120 -> -132 wcet -17 (0 regressions) unmodeled-op 175 -> 61 single-block 73 -> 73 (unchanged) SIDE FINDING, and it is a real latent miscompile in the SHIPPING encoder. The i64 shift expansions zero-fill with the 16-bit Thumb `MOVS` T1 form, `0x2000 | (rd_bits << 8)`, whose `rd` field is THREE bits: for R8 that is `0x2800` = `CMP r0, #0`, so the half is never zeroed. Same class as #180 / H-CODE-9, and the same one #311 already fixed for `I64SetCond` — but these expansions are hand-emitted halfwords with FIXED internal branch displacements (`B .done` = two halfwords), so widening the MOV to 4 bytes overshoots the target. NOT fixed here; it needs its own lane and its own execution gate. It IS REACHABLE: `rv32_cmp_select_472.wat` on cortex-m4 emits `I64ShrU { rd_lo: R7, rd_hi: R8, … }` today. It happens to be unobservable there (an `I32WrapI64` discards the high half immediately) — luck, not a guarantee. Pinned by `i64_shift_zero_fill_mis_encodes_for_a_high_destination`, which asserts the 0x2800 byte so the defect cannot be fixed unnoticed, and the colourer refuses such a stream outright rather than put its name to it (`pair_low_reg_only` + the `i64-16bit-form-high-reg` decline + an interference edge to R8's identity-pinned entry web, so R8 is not even a candidate colour). Gates: fmt / clippy -D warnings / `cargo test --workspace` all exit 0; frozen anchors 10/10; `vcr_dec_001_graph_alloc_differential.py` green (flag-off ≡ the four frozen goldens, flag-on applies on 9 fixtures, RA-003 Consistent). Trace: VCR-REACH-001
…s join reach (#242) Two things, both about making the increment's claim checkable rather than asserted. 1. THE EXECUTION ORACLE. `pair_effect` is shared by the pass, `validate_cfg_rewrite` and the ABI observable contract, so — exactly as for increment 3's AAPCS contract — NEITHER dataflow instrument can catch an error IN the model. Only execution can. `vcr_reach_001_i64_pair.wat` gives the family its own population in the existing differential, with its own non-vacuity floors (>= 4 divergent pair functions, and >= 2 of them containing a REAL i64 shift expansion, detected in the EMITTED BYTES by its `AND.W Rd,Rn,#63` opening rather than taken from the case table's say-so). Each fixture is built so a specific WRONG model gives a WRONG VALUE: * `shl_amt_live` / `shl_amt_live_hi` / `shru_amt_live` keep the shift AMOUNT live across the shift and deliberately do NOT pre-mask it — at s = 100 the low half goes in as 100 and comes out as 36, so the `AND rm_lo,rm_lo,#63` RMW is OBSERVABLE. A pre-masked amount would make that `AND` a no-op and the fixture would pass under the mutated model: vacuous coverage that reads exactly like a green gate. * Shift inputs straddle the expansion's internal `BPL` (s < 32 and s >= 32). The distinctness constraints differ between those arms, so a one-sided input set would never execute the arm whose register moved. * `ld_dead_base` / `ld_dead_base_lo` make the address DEAD after the load — the only configuration in which the early-clobber edge is load-bearing. With the address still live, ordinary liveness already forbids the coalesce and the fixture would prove nothing. * `ld_dead_base` folds in BOTH loaded halves (the high one via a scratch store + 32-bit reload, since a `shr_u … 32` here lands its destination on R8 and trips the `i64-16bit-form-high-reg` decline). No `(data …)` segment, deliberately: on this compile path `.linear_memory` is SHT_NOBITS, so the emulator would start zeroed while wasmtime starts initialised and every load would differ for a reason unrelated to the allocator. The load fixtures seed the memory they read, in the same call. Result: 90/90 checks, 26 engaged functions (6 call, 7 i64-pair, 4 of those carrying a real shift expansion). 2. VCR-RA-003's JOIN HALF, which was declining on the whole family. `check_join_availability` built its CFG from `reg_effect` alone, so every i64-pair function returned `NotAttempted { cfg-unmodeled-construct }` — the pass's output was "clean under VCR-RA-003" only in the sense that the interesting half of it never ran. It now consumes the same `pair_effect`, in BOTH admission checks AND in the availability fixpoint's `def_b` — those must move in lockstep, because admitting an op whose defs then read as empty UNDER-states what it produces and could report a value as unavailable at a join, i.e. a FALSE POSITIVE from a validator that HARD-ERRORS the compile. This one runs unconditionally on the shipping path, so it was checked as such: 0 hard errors across the whole corpus with the flag OFF, on both the relocatable and self-contained paths. Measured coverage on 640 functions: VCR-RA-003 join availability v0.54: Consistent 440 / NotAttempted 200 now: Consistent 560 / NotAttempted 80 A 60 % cut in the declining half, on the DEFAULT build — this part is not gated behind `SYNTH_GRAPH_ALLOC` and is the increment's one unconditional verification win. Flag-off byte identity re-verified per FUNCTION rather than in aggregate (the corpus grew by this lane's own fixture, so the totals legitimately move): all 633 pre-existing relocatable functions and all 1059 self-contained ones are byte-identical to v0.54, 0 diffs. Frozen anchors 10/10. Trace: VCR-REACH-001
THE MUTATION EVIDENCE, reported in full — including the mutation that does NOT
go red, because a matrix that lists only its successes is not evidence.
A. `pair_effect` drops BOTH `rm_lo` and `rm_hi` from the shift clobber set.
RED. `rewrite_op`'s RMW-agreement check on `rm_lo` can no longer be
satisfied, every shift function declines, and the engagement floor fires
(PAIRSHAPES 9 -> 3, SHIFTSHAPES 6 -> 0). Caught by refusal-to-emit rather
than by a wrong value.
B. `pair_effect` drops ONLY `rm_hi`, COHERENTLY (absent from defs and uses, so
pass and every validator agree the shift leaves it alone).
GREEN — NOT CAUGHT. An honest residual, established by trying: four shift
fixtures, two of them (`shl_pressure`, `shl_pressure8`, four and eight i32
values live across the shift) built specifically to create the pressure
this mutation needs. 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 and the clobber is unobservable on
this corpus. The `rm_hi` half of the model is sound and cheap but currently
BELT-AND-BRACES, not execution-gated. Named follow-up, not a claim made here.
C. The EARLY-CLOBBER interference edges are deleted.
RED, and this is the sharp one. The colourer coalesces `I64Ldr`'s `rdlo`
onto a `base` the second `LDR` still re-reads. `validate_cfg_rewrite`
ACCEPTS all 7 functions, VCR-RA-003 reports Consistent on all 7, the ABI
observable contract passes all 7 — THREE STATIC INSTRUMENTS GREEN — 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 the code generator.
CI wiring, same commit, `set -euo pipefail` + a NON-ZERO count assertion. The
awk gate gains increment 4's two floors — >= 4 engaged i64-PAIR functions and
>= 2 of them containing a REAL i64 shift expansion, the latter detected in the
EMITTED BYTES by its `AND.W Rd,Rn,#63` opening rather than taken from the case
table's say-so, so a fixture that stops emitting a shift fails loudly instead of
quietly leaving the dangerous class ungated. The gate is verified RED-FIRST on
all three floors (PAIRSHAPES=3, SHIFTSHAPES=1, and a non-all-passing CHECKS
count each exit 1; the real line exits 0).
MEASURED, on the 633-function v0.54 corpus so the comparison is apples-to-apples
despite this lane adding 9 fixture functions (642 / 1071 now):
greedy inc 3 inc 4
applied (reloc) — 316 411
applied (self-cont) — 113 204
bytes (reloc) 41438 -100 -110 (-10 vs inc 3)
bytes (self-cont) 49930 -120 -132 (-12 vs inc 3)
wcet (reloc) 14009 -33 -33 0 regressions, 408 bounded
declines (reloc): unmodeled-op 175 -> 61, single-block 73 -> 73,
identity-colouring 31 -> 58, call-indirect-pseudo 17, unreachable-block 11,
numeric-branch 10, i64-16bit-form-high-reg 1 (new).
READ ON THE FLIP CRITERION: reach is up 30 % / 81 %, bytes moved 10 / 12 more.
That GAP is the finding. It confirms increment 3's diagnosis rather than
softening it — reach converts into bytes almost entirely through
`shrink_callee_saved_saves`, which is LEAF-ONLY, so widening the op model raises
how much of the corpus the colourer can reason about without raising how much of
it it can shrink. The flip criterion is NOT closer on bytes. It IS closer on
confidence: VCR-RA-003's join-availability half went from Consistent 440 to 560
of 640 on the DEFAULT build, which is the one unconditional win here.
Traceability closed: SWVER-022 `verifies` VCR-REACH-001 and VCR-DEC-001, so this
lane's requirement no longer carries the "needs a verifies link" warning — rivet
validate 52 errors / 103 warnings against a 52 / 104 baseline (one FEWER
warning, no new errors), and `rivet check verification-evidence` passes.
Gates by REAL exit code: fmt 0, clippy --workspace --all-targets -D warnings 0,
cargo test --workspace 0, claim_check 37/37, oracle_wiring_check 0 unwired /
0 undeclared, vcr_dec_001_graph_alloc_differential 0 (flag-off frozen), the
execution differential 100/100 PASS, frozen anchors 10/10.
Trace: VCR-REACH-001
… 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
Codecov Report❌ Patch coverage is 📢 Thoughts on this report? Let us know! |
Contributor
Author
|
Heads-up from the #916 fix lane (#919): the defect this PR pins is now fixed, so Three of its assertions are false by design after #919:
Whichever of us merges second should, in that merge:
Happy to do all three on my branch if you'd rather merge #917 first — just say so and I'll rebase onto it. Two things from the fix worth feeding back to VCR-DEC-001: The class was wider than filed — five sites, not two. Your decline is no longer load-bearing for correctness. The shipping encoder now handles Detail, red-first evidence, and the displacement analysis are in #919. |
avrabe
added a commit
that referenced
this pull request
Aug 5, 2026
…degrade into a no-op The execution differential's entire value rests on one unstated fact: the allocator actually places a zero-fill destination in R8 inside `pressure_shru`. That was verified by hand (`MOV.W R8,#0` at .text+0x252) but NOTHING asserted it. Any allocator change can quietly reallocate that function to R0-R7 — and VCR-DEC-001 is actively churning the allocator, with #917's interference edge specifically keeping R8 out of the candidate colours. The differential would then still print "48/48 OK" and exit 0 while testing nothing about the high-register path. That is the #890 "gate that cannot fail" shape, arrived at by drift instead of by a bug. So the witness is now an assertion: scan .text for the 32-bit `MOV.W Rd,#0` (F04F 0000 | Rd<<8) with Rd >= 8, and fail if there is none. That encoding exists ONLY because of the #916 fix — before it, the same site emitted 0x2800. Proven non-vacuous by construction, not by inspection: on the shipped module it reports `reachability witness: MOV.W R8,#0 @ 0x252` and exits 0; on a single-function low-pressure module whose shift destination lands in a low register it fires and exits 1. The assertion message says what to do — raise pressure in the .wat, do not delete the check — and names the likely cause, so if #917's decline lands and takes R8 away, this goes RED (correct: the oracle lost its witness) rather than silently green. Also closed while here: no WCET test asserts an exact cycle literal for i64.shl/shr_u/clz/ctz (the only i64 entry in wcet_bound_gate.rs is div, which declines), so the estimator's 38->40 / 24->26 / 32->34 widening touches no pinned bound. 39/39 wcet_bound_gate green. The direction is sound regardless — a longer instruction yields a HIGHER cycle bound. Refs #916, #890 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
This lane's `i64_shift_zero_fill_mis_encodes_for_a_high_destination` pinned the #916 miscompile so it could not be "fixed by accident and un-noticed". Its own docstring said: *"the day the branch offsets are recomputed the test fails loudly and gets inverted."* That day is now — the #916 fix lane (PR #919) landed the real repair, and three of this test's assertions are false BY DESIGN afterwards: * `low.len() == high.len()` ("expansion length is register-independent") — no longer true; a high destination takes the 4-byte `MOV.W`, so I64Shl/I64ShrU are 40 bytes for rd >= R8 vs 38 for R0-R7; * `tail_high == 0x2800` — the tail is now `F04F 0800` (`MOV.W R8, #0`); * the identical I64ShrU assertion. Dropped rather than inverted: #919's `i64_high_reg_zero_fill_916.rs` supersedes it across ALL FIVE affected sites, not the two this pin covered. The #916 sweep found `I64Clz`/`I64Ctz`/`I64ExtendI32U` share the class with NO `>= 32` precondition at all, so an inverted two-site pin would understate what is now guaranteed. `artifacts/sw-verification.yaml` re-pointed at the superseding test rather than left citing a name that no longer exists — a rivet artifact citing a vanished test is exactly the #911 defect (`cargo test -- <no match>` exits 0), and this release filed that one. **A test pinning a defect must not outlive the defect.** Verified: `cargo test -p synth-backend --lib` exit 0 (263 passed), fmt 0. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe
added a commit
that referenced
this pull request
Aug 6, 2026
…ansmuted to CMP at FIVE sites, not two (#919) * test(#916): RED — i64 zero-fill transmutes to CMP for a high destination (5 sites, not 2) Red-first evidence on unmodified main. `MOVS Rd,#imm8` (T1) has a THREE-bit Rd field; `reg_to_bits(R8)` = 8 overflows into bit 11 and `0x2000|0x0800 = 0x2800` is `CMP r0,#0` — not a move. The half that must be zeroed is never written. The issue named two sites. Sweeping every 16-bit imm8 T1 emission in the Thumb-2 encoder found FIVE: I64Shl rd_lo large-shift arm conditional (n >= 32) I64ShrU rd_hi large-shift arm conditional (n >= 32) I64Clz rnhi high-word clear UNCONDITIONAL I64Ctz rnhi high-word clear UNCONDITIONAL I64ExtendI32U rdhi high-word clear UNCONDITIONAL The last three are worse than the two filed: they have no `n >= 32` precondition, so every i64.clz / i64.ctz / i64.extend_i32_u whose high half lands in R8 returns garbage in its upper 32 bits. `I64ExtendI32U{rdhi=R8}` emits literally [4608, 2800] — a two-instruction expansion, half of which is the wrong instruction. Failing today (7 assertions): I64Shl{rd_lo=R8} tail 0x2800 I64ShrU{rd_hi=R8} tail 0x2800 (the shape rv32_cmp_select_472.wat emits) I64Clz{rnhi=R8} tail 0x2800 I64Ctz{rnhi=R8} tail 0x2800 I64ExtendI32U{rdhi=R8} tail 0x2800 I64Shl / I64ShrU branch-displacement checks (pre-staged for the widening) NOT defective, and pinned as such so the sweep is recorded rather than asserted in prose: - A32 (cortex-r5): `MOV Rd,#0` is `0xE3A00000 | Rd<<12`, a FOUR-bit Rd field. R8 encodes correctly. Test passes on main. - I64ShrS: its large-shift arm sign-fills with the 32-bit `ASR.W rd_hi,rn_hi,#31`, no 16-bit form to transmute. - I64SetCond / I64SetCondZ / Mov / f32+f64 compare: already carry the #311 guard. Branch targets were settled by DECODING the imm fields, not by reading comments: - Shl/ShrU: `B .done` (0xE002) targets halfword 19 = END of expansion, PAST the MOV at halfword 18. Widening the MOV MOVES the target -> displacement must be recomputed to 0xE003. - Clz/Ctz: `B .done` targets byte 22 / 30, which IS THE MOV's OWN ADDRESS. An instruction cannot move its own address -> no displacement change. - I64ExtendI32U: no branches. `assert_branches_still_land` re-derives every target from the emitted bytes so a mis-recomputed displacement fails here rather than at run time. Trading a data miscompile for a control-flow one would be strictly worse. Refs #916, #311, #180, #498 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * fix(#916): GREEN — emit MOV.W for high-register i64 zero-fills, deriving the branch displacement Follows #311's shape (32-bit `MOV.W Rd,#imm8`, T2 `F04F 0000 | Rd<<8 | imm8`, whenever `rd >= R8`) at all FIVE affected sites, behind one shared helper (`emit_thumb_zero_fill`) so a sixth site cannot reintroduce the class silently. INSTRUCTION SIZE / DISPLACEMENTS — the reason this was not a one-liner. `MOV.W` is 4 bytes where `MOVS` was 2. Whether that moves a branch target was settled per site by DECODING the emitted imm fields, not by reading comments: I64Shl / I64ShrU `B .done` (0xE002) targets halfword 19 = the END of the expansion, PAST the zero-fill at halfword 18. The target MOVES. The displacement is now DERIVED from the zero-fill's real width (`thumb_zero_fill_halfwords`) rather than hard-coded, so the encoder cannot drift from itself: 0xE002 for a low destination, 0xE003 for a high one. `BPL .large` (0xD50A) targets halfword 16, before the zero-fill -> unaffected. I64Clz / I64Ctz `B .done` targets byte 22 / 30, which IS the zero-fill's OWN address. An instruction cannot move its own address -> no displacement change. `BEQ` targets 14 / 18, before it. I64ExtendI32U no branches at all. Reordering the large-shift arm to dodge the size change was REJECTED, not overlooked: zeroing rd_lo before the `LSL.W` would destroy rn_lo in the in-place case rd_lo == rn_lo. That reasoning is in the code so it is not "simplified" away later. ESTIMATOR MIRROR (#498). `estimate_arm_byte_size` is a hand-maintained mirror of this encoder and feeds optimized-path branch resolution; I64Shl/ShrU/Clz/Ctz are all classified OnPath. Left un-mirrored, a high-reg shift would be under-counted by 2 and every branch spanning it would land short — the #483 class, and exactly the control-flow miscompile that would have been strictly worse than the data bug. Now register-shape-sensitive (38/40, 24/26, 32/34), matching the existing house pattern for Cmn/Sxtb/Uxth/Mov. The direct selector needs no change: it resolves branches from real `code.len()`, not the estimator. I64ExtendI32U is classified NotOnPath (lowered to 32-bit op pairs upstream), so it has no estimator entry to update. GATE COVERAGE ADDED IN THE SAME COMMIT — re-running the old cases would have proved nothing, because they only ever used low registers: - estimator_encoder_agreement: +5 high-destination cases (I64Shl, I64ShrU, I64ShrS, I64Clz, I64Ctz). Without them the #498 oracle stayed green while blind to the entire high-reg half of these expansions. - i64_expansion_certification: +5 high-register variants fed to the symbolic executor. This was a THIRD validator blind spot in the same family as the two recorded in v0.53 — `covered_i64_pseudo_selections` fed these ops only at R0/R1, and the high-register variant list covered only I64SetCond/ SetCondZ/Mul/Popcnt, so no validator on the tree could see the defect. Confined to rd >= R8: low-register expansions are byte-identical (38/38/40/24/ 32/4), so frozen anchors do not move unless a fixture actually had a high-reg destination. Fixes #916. Refs #311, #180, #498, #483 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * test(#916): RED validator shape — prove the certifier is non-vacuous on this class The five high-register variants added to `shipped_expansions_certify_high_register_variants` are only meaningful if the validator can DISTINGUISH the fixed expansion from the broken one. Splice the pre-fix `I64ShrU{rd_hi=R8}` tail back on — the narrow `B .done` (0xE002) and the transmuted 0x2800 — and it must produce a counterexample: ✗ #916 shape rejected as required: I64ShrU: a_lo=0xffffffff, a_hi=0x0, b_lo=0x20, b_hi=0x0 b_lo = 0x20 = 32, i.e. the solver picked exactly the large-shift arm that reaches the zero-fill. Same pattern as the #632 red shape already in this file. The fixed tail is pinned in the test, so an encoder change breaks it loudly rather than silently making the splice meaningless. Refs #916 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * test(#916): execution differential — 48 runs vs wasmtime, RED before the fix The byte-level test pins the emitted halfword and the certifier pins the symbolic semantics, but neither can catch a MIS-RECOMPUTED BRANCH. Widening the zero-fill from 2 to 4 bytes moved `.done` in I64Shl/I64ShrU; if the displacement were wrong the branch would sail past the end of the expansion, and the tail halfword would still assert clean. Only execution sees that. `i64_high_reg_zero_fill_916.wat` removes the luck that hides the bug on main: every export KEEPS the half the broken instruction was supposed to zero (no following I32WrapI64 to discard it). Shift amounts straddle 32 — 0,1,31 take the small-shift arm and the moved branch, 32,33,40,63 take the large arm with the widened zero-fill. `pressure_shru` is the reachability witness: four i32 params pinned in r0-r3 (#193/#204) plus live i64 pairs push a zero-fill destination into R8. Verified in the emitted image — `MOV.W R8, #0` at byte 0x252 of the compiled .text. R8 and unused argument registers are seeded with 0xDEADBEEF, not left at 0. #916 leaves the destination UNWRITTEN, so a run that passed only because the stale register happened to hold 0 would be a false green. RED-FIRST EVIDENCE (encoder reverted to the pre-fix commit, CLI rebuilt): FAIL pressure_shru(0x20,0x1,0x20,0x2) = 0x22d3c110320fedcc expect 0x00000007320fedcc FAIL pressure_shru(0x28,0x7,0x21,0xb) = 0x7786944434320ff1 expect 0x5555555534320ff1 FAIL pressure_shru(0x3f,0xffffffff,..) = 0x22d3c121b3333335 expect 0x00000032b3333335 exit 1 The three failures are exactly the shift amounts >= 32 (0x20, 0x28, 0x3f); the 0x1 and 0x1f cases pass because they take the small-shift arm and never reach the zero-fill. The corrupted HIGH halves are stale register contents. With the fix restored: 48/48 OK, exit 0. CI-wired in this commit (`set -euo pipefail`, `# ci-status: wired`, and a non-zero-count assertion on executions so a silently-empty run cannot pass). `scripts/oracle_wiring_check.py` green: 159 scripts, 152 wired, 0 unwired, 0 UNDECLARED. `scripts/claim_check.py` green: 38/38. Refs #916 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * style(#916): cargo fmt + clippy unnecessary_cast on the zero-fill helper `((rd_bits as u16) << 8) as u16` — the outer cast is a no-op (rust-1.96 clippy::unnecessary_cast, -D warnings in CI). Gate sweep by REAL exit code, not piped output: cargo fmt --check exit 0 cargo clippy --workspace --all-targets -D warnings exit 0 cargo test --workspace exit 0 frozen_codegen_bytes (10 anchors) exit 0, BYTE-IDENTICAL estimator_encoder_agreement (#498) exit 0 scripts/oracle_wiring_check.py exit 0 scripts/claim_check.py exit 0, 38/38 NO frozen fixture moved. The fix is confined to `rd >= R8` and none of the four anchors (control_step, flight_seam, flight_seam_flat, signed_div_const) has a high-register i64 zero-fill destination, so their .text sha256 pins are unchanged — nothing to re-pin, and no re-pin to justify. Refs #916 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * test(#916): pin the differential's reachability witness so it cannot degrade into a no-op The execution differential's entire value rests on one unstated fact: the allocator actually places a zero-fill destination in R8 inside `pressure_shru`. That was verified by hand (`MOV.W R8,#0` at .text+0x252) but NOTHING asserted it. Any allocator change can quietly reallocate that function to R0-R7 — and VCR-DEC-001 is actively churning the allocator, with #917's interference edge specifically keeping R8 out of the candidate colours. The differential would then still print "48/48 OK" and exit 0 while testing nothing about the high-register path. That is the #890 "gate that cannot fail" shape, arrived at by drift instead of by a bug. So the witness is now an assertion: scan .text for the 32-bit `MOV.W Rd,#0` (F04F 0000 | Rd<<8) with Rd >= 8, and fail if there is none. That encoding exists ONLY because of the #916 fix — before it, the same site emitted 0x2800. Proven non-vacuous by construction, not by inspection: on the shipped module it reports `reachability witness: MOV.W R8,#0 @ 0x252` and exits 0; on a single-function low-pressure module whose shift destination lands in a low register it fires and exits 1. The assertion message says what to do — raise pressure in the .wat, do not delete the check — and names the likely cause, so if #917's decline lands and takes R8 away, this goes RED (correct: the oracle lost its witness) rather than silently green. Also closed while here: no WCET test asserts an exact cycle literal for i64.shl/shr_u/clz/ctz (the only i64 entry in wcet_bound_gate.rs is div, which declines), so the estimator's 38->40 / 24->26 / 32->34 widening touches no pinned bound. 39/39 wcet_bound_gate green. The direction is sound regardless — a longer instruction yields a HIGHER cycle bound. Refs #916, #890 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
# Conflicts: # CHANGELOG.md
… sites This bullet claimed 'found and pinned, not fixed' and named the pinning test that fc2340e deleted. A defect pin must not outlive the defect, and neither should the prose describing it. Scope corrected too: I64Clz/I64Ctz/I64ExtendI32U zero a half with the same 3-bit form under NO precondition, which the two-site framing missed.
Fan-in resolution, all three conflicts kept-both: - CHANGELOG.md: union of both sides' [Unreleased] bullets, count-asserted. - artifacts/sw-verification.yaml: main already owns SWVER-022 (L7's VCR-RA-004 artifact), so this lane's renumbers to SWVER-023. The two in-flight lanes take 023 and 024 so the second to merge cannot collide again.
# Conflicts: # CHANGELOG.md
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
v0.55 lane L3. Flag-off. The deliverable is the measurement, and the verdict is still do not flip — but for a sharper reason than last time.
Which target, and why
Increments 2 (joins, v0.53) and 3 (calls, v0.54) both returned do not flip, and both for the same reason: the limiting factor is reach, not soundness. So I picked the reach target with evidence rather than intuition — a per-function census of which ops force the biggest decline bucket, instrumenting
joins::build_cfg's admission loop to report the complete unmodeled set per function rather than just the first blocker:The other candidate (widening the leaf-only
shrink_callee_saved_saves) was not taken: it changes shipping bytes, and the measurement below is exactly what tells you whether it is worth its own flag and gate. It is.Method — the two things that would have been silent failures
A NEW shared definition, never a widened
reg_effect.reg_effectreturnsNoneon these ops deliberately, and the shipping pipeline depends on thatNone(local_dead_defs,reallocate_function— default-on since v0.24.0 —straight_line_value_ranges,fuse_cmp_select's dead-by-redef scan,validate_final_allocation's fail-safe invariant 1). Widening it hands the greedy allocator streams it has always refused and moves the shipped bytes.liveness::pair_effectfollows increment 3'scall_effectpattern: one definition, consumed by four instruments — the pass,validate_cfg_rewrite, the ABI observable contract, and VCR-RA-003's join CFG.The model is read off the ENCODER, both paths, never off the IR declaration. These are pseudo-ops expanded downstream — the exact class increment 3 declined
Call/CallIndirectfor. A naivedefs = {rdlo, rdhi}is wrong:I64Shl/ShrU/ShrSopen withAND rm_lo, rm_lo, #63and userm_hias a pure scratch temp — the IR field is even commented// used as temp. Both are DEFS.I64Ldr/I64Stradditionally define R12 on the index form.I64LdrisLDR rdlo,[base,#off]; LDR rdhi,[base,#off+4]: coalescingrdloontobase— which a plain interference graph does the momentbaseis dead after — makes the second load read a clobbered base. Carried bypair_early_clobberas interference EDGES. One rule, provably sufficient: every pair in the hand-derived table (enumerated in the doc comment, both encoders, all tenI64SetCondarms) is either two defs of one instruction — already separated by the existing co-def clique — or a def against a use of it.Measured
On the 633-function v0.54 corpus, so the comparison is apples-to-apples despite this lane adding 9 fixture functions (the corpus is 642 / 1071 now — it grows as lanes add fixtures):
Decline histogram (relocatable, 642-function corpus):
single-block73 ·unmodeled-op175 → 61 ·identity-colouring31 → 58 ·call-indirect-pseudo17 ·unreachable-block11 ·numeric-branch10 ·i64-16bit-form-high-reg1 (new).Read on the flip criterion: NOT closer on bytes. Reach is up 30 % / 81 % and bytes moved 10 / 12 more. That gap is the finding — it confirms increment 3's diagnosis rather than softening it. Reach converts into bytes almost entirely through
shrink_callee_saved_saves, which is leaf-only, so widening the op model raises how much of the corpus the colourer can reason about without raising how much it can shrink. That makes the callee-saved lever the obvious v0.56 lane.Closer on confidence, though, and this part is unconditional: VCR-RA-003's join-availability half built its CFG from
reg_effectalone, so every i64-containing function returnedNotAttempted— the interesting half never ran. On the default build, flag off, over 640 functions: Consistent 440 → 560, NotAttempted 200 → 80.Mutation evidence
The model is shared by four instruments, so none of them can catch an error in it. Reported in full, including the mutation that does not go red — the model carries three obligations and only one is execution-gated:
validate_cfg_rewriteaccepts all 7 functions, VCR-RA-003 reports Consistent on all 7, the ABI observable contract passes all 7 — three static instruments green — 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.rm_lo+rm_hifrom the shift clobber setrewrite_op's RMW-agreement check — a guard written in this lane alongside the model it constrains, so it is the model catching its own inconsistency, not independent detection.rm_hi, coherentlyshl_pressure,shl_pressure8, 4 and 8 i32 values live across the shift). The churn-minimising bias fills R0–R3 first and the shift-amount pair sits in callee-saved R4–R8, so no live web ever lands on the originalrm_hiregister. Sound and cheap, but belt-and-braces rather than gated.The fixtures are built so a wrong model gives a wrong value: the shift amount is kept live across the shift and deliberately not pre-masked (at
s = 100it goes in as 100 and comes out as 36, so the in-placeANDis observable — a pre-masked amount would pass under the mutated model, vacuous coverage that reads like a green gate); inputs straddle the expansion's internalBPLon both sides, because the shift constraints are path-dependent; and the load fixtures make the address dead after the load, the only configuration where the early-clobber edge is load-bearing.CI-wired in the same commit,
set -euo pipefail, with two new non-vacuity floors — ≥4 engaged i64-pair functions and ≥2 containing a real i64 shift expansion, the latter detected in the emitted bytes rather than declared. Gate verified red-first on all three floors.Side finding: a latent miscompile, filed as #916
The i64 shift zero-fill uses the 16-bit
MOVST1 form,0x2000 | (rd << 8)— a three-bitrdfield. For R8 that is0x2800, i.e.CMP r0, #0, and the half is never zeroed. Reachable today:rv32_cmp_select_472.waton cortex-m4 emitsI64ShrU { rd_hi: R8, … }; it is unobservable there only because anI32WrapI64discards the high half, which is luck. Not fixed here — unlike #311'sI64SetCondfix, these expansions carry fixed internal branch displacements that a 4-byteMOV.Wwould overshoot, so it needs its own lane and its own execution gate. Pinned by a test asserting the defective byte, and the colourer refuses such streams by name rather than certifying them.Second finding: an oracle that was passing vacuously
rivet check verification-evidencereportednamed_test_steps_checked: 0repo-wide while 31 artifacts carry acargo teststep. Root cause: it scansfields.steps[].run(a sequence); every artifact here writessteps:as a mapping. Pre-existing, not caused by this lane — but I had cited it as evidence in an earlier commit, and that citation was wrong. SWVER-022 is now written in the shape the oracle reads (0 → 1 checked, verified red-first). Converting the other 42 is a follow-up, because each conversion has to re-verify its filter still matches a real test — which is the point. Also: a source with a YAML parse error is silently skipped and the oracle still reportsok: true.Gates — by real exit code
cargo fmt --check0 ·clippy --workspace --all-targets -D warnings0 ·cargo test --workspace0 ·claim_check37/37 ·oracle_wiring_check0 unwired / 0 undeclared · frozen anchors 10/10 ·vcr_dec_001_graph_alloc_differential0 · execution differential 100/100 PASS ·rivet check verification-evidence0 · rivet validate 52 err / 103 warn against a 52 / 104 baseline.SYNTH_GRAPH_ALLOCstays off by default. Flag-off byte identity verified per function, not in aggregate (the corpus legitimately grew): all 633 pre-existing relocatable and all 1059 self-contained functions byte-identical to v0.54, 0 diffs. The one shipping-path change (VCR-RA-003's widened join CFG) was swept on both ISAs — thumb2 and thecortex-r5A32 path, whose expansions are entirely different code — 0 hard errors on either.Trace: VCR-REACH-001 · epic #242 · side findings #916
🤖 Generated with Claude Code
https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L