feat: Renode example tests + v0.1.0 release prep - #63

avrabe · 2026-03-21T19:23:22Z

Summary

Renode Execution Tests (85 assertions)

calculator.wast (62 tests): add/sub/mul/div_safe, accumulator, bitwise, min/max/abs
anti_pinch.wast (23 tests): jam detection, PWM ramp, position/direction getters
Both wired into Bazel wast_multi_func_test pipeline

Release v0.1.0 Prep

CHANGELOG.md: comprehensive release notes for all features
16 crate Cargo.toml: descriptions, homepage, keywords, categories
README.md: updated feature matrix, quick start guide, current stats
CLI help: usage examples, accurate about text

Meld/Kiln Integration Instructions

docs/design/meld-kiln-integration-instructions.md
Defines the contract between synth, meld, and kiln-builtins
OSxCAR end-to-end test plan (fetch → fuse → compile → link → run)

Test plan

cargo test --workspace — 851 tests, 0 failures
cargo clippy — clean
cargo fmt --check — clean

🤖 Generated with Claude Code

Renode execution tests: - tests/wast/calculator.wast — 62 assert_return (arithmetic, bitwise, min/max/abs, accumulator) - tests/wast/anti_pinch.wast — 23 assert_return (jam detection, PWM ramp, getters, tick) - Wired into Bazel wast_multi_func_test pipeline Release v0.1.0 preparation: - CHANGELOG.md — comprehensive release notes - All 16 crate Cargo.toml — descriptions, metadata, keywords - README.md — updated features, quick start, 851 tests, 197+ opcodes - CLI help — usage examples, accurate descriptions Meld/kiln integration instructions: - docs/design/meld-kiln-integration-instructions.md - Contract: what synth expects from meld (single-memory core module) - Contract: what synth expects from kiln-builtins (3 C ABI functions) - OSxCAR end-to-end test plan Trace: skip Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

…x-M (#93) Pre-fix, `optimizer_bridge::wasm_to_ir` had no handler for `WasmOp::I64ExtendI32U` / `I64ExtendI32S` / `I32WrapI64`. They fell through the catch-all `_ => Opcode::Nop`, advancing `inst_id` by 1 but never registering the produced i64-pair vregs in `vreg_to_arm`. When a downstream `Opcode::I64ShrU` / `I64Shl` looked up its shift-count vreg via `get_arm_reg`, the lookup missed the map and silently fell back to `Reg::R0` (`optimizer_bridge.rs:1333`). The ARM emitter for the variable i64 shift writes to both `rm_lo` and `rm_hi` as scratch (`AND.W rm_lo, rm_lo, #63; SUBS.W rm_hi, rm_lo, #32; ...`) — so any function that did `i64.shr_u` of an `i64.extend_i32_u`-ed shift count clobbered the AAPCS first-param register R0 inside the shift expansion. For `compiler_builtins::memset`, R0 is the destination pointer, so the byte loop's pointer was destroyed every iteration → non-terminating loop on silicon at `memset+0x4c`. This patch: - Adds `Opcode::I64ExtendI32U`, `Opcode::I64ExtendI32S`, and `Opcode::I32WrapI64` to `synth-opt`. - Handles those WasmOps in `wasm_to_ir`, with slot accounting that keeps `inst_id.saturating_sub(K)` arithmetic correct for downstream i64 ops (extend reuses the consumed i32 slot for `dest_lo`; wrap reuses the i64-lo slot and decrements `inst_id` so the natural +1 cancels with the -1 net slot delta). - Lowers them in `ir_to_arm`. Critically, the extend lowerings allocate a callee-saved consecutive pair via `alloc_i64_pair` and Mov the i32 source into `dest_lo` even when the source already lives in a non-param register. This ensures the downstream i64-shift's `rm_lo`/`rm_hi` (which the emitter treats as clobbered scratch) are never AAPCS param registers. - Updates `analyze_i64_local_gets` to skip the i32 LocalGet that feeds an `I64ExtendI32U`/`I64ExtendI32S` so the analyzer doesn't mistakenly mark it as i64. Regression test: `crates/synth-synthesis/tests/issue_93_memset_i64_codegen.rs` exercises the bug pattern in the optimized path (4-param function shifting an `i64.const` by `i64.extend_i32_u(local.get $n)`) and asserts the emitted i64-shift's `rm_lo`/`rm_hi` are not in R0..R3. Pre-fix: 3 of 5 tests fail (one per shift variant: shr_u, shl, shr_s). Post-fix: 5/5 pass. The no-optimize path was always correct and is exercised by a sanity test in the same file. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…ovably < 32 (#686) gale measured #682's unconditional AND R12,#31 mask at ~12% cyc/call (+14 B) on gust_mix, whose Q8 fixed-point shifts are all CONSTANTS — the mask can never fire there, yet every register-controlled i32 shift pays it. New peephole liveness::elide_shift_masks removes the mask ONLY when the amount is statically provable < 32; anything unproven keeps it — elision is an optimization, the mask stays the sound default. Two proven shapes, keyed on the #682 idiom (and r12,rK,#31 ; shift by r12 — emitted adjacently by both direct selectors, the Rocq-proved DSL rules, and the optimized bridge; the DSL rules stay MASKED, no proof changes): - Const amount: nearest preceding def of rK is a pure materialization (movw, or the bridge's mov #imm) over a fully-modeled redefinition- free window -> fold the whole triple to the immediate shift, REDUCED MOD 32 (so >= 32 amounts shrink too — the fold computes exactly the WASM semantics the mask enforces); C mod 32 == 0 lowers to MOV (imm5 == 0 encodes shift-by-32, the LSR/ASR pitfall). The movw drops when rK has no other reader (reg_dead_by_redef). This supersedes fold_immediate_shifts for the masked idiom — its movw->shift window is intercepted by the #682 and, so post-#682 it declined every const-amount register shift (the gust_mix regression's second half). - Range-carried amount: nearest def is and rK,rX,#c with c < 32 -> rK < 32 at the shift, the re-mask is a no-op; shift by rK directly. Covers the wasm-level x&31 / x&15 idioms. A #494 fact-spec value- range premise is the documented follow-up. Soundness scaffolding as the sibling folds: backward scan aborts on any reg_effect-unmodeled op (call/branch/LABEL = merge point); dropping the and r12 write is safe by the #212 R12-scratch convention; rotr is never masked (#682 exemption) so the pattern cannot match it; removal/rewrite-only before branch resolution (offset-neutral). FLAG-OFF (opt-in SYNTH_SHIFT_MASK_ELIDE=1) per the flag-then-flip protocol: the elision MOVES the frozen anchors — measured on this commit, per-function, no function grows, every const-shift function shrinks (bytes ON vs OFF, identical on both paths): control_step_decide 313 -> 293 (-20) flight_seam flight_algo 376 -> 296 (-80), controller_step 325 -> 241 (-84) flight_seam_flat flight_algo 520 -> 436 (-84), controller_step -84 gust_mix (the #686 fixture) 65 -> 55 (-10) — recovers the measured regression (the +14 B was mask + retained movw + wide shift) i32_shift_mask_682 shl32/shl33/shl300/shr300/sar300 -> 8-12 B each signed_div_const untouched Default (flag unset) is byte-identical to v0.37.1 everywhere: the frozen byte-gate passes unchanged, and shift_mask_elide_686.rs pins unset == opt-out. The default-on flip is the maintainer's separate refreeze (all differentials green on the new bytes, goldens re-pinned). Oracles on this commit: - i32_shift_mask_682_differential.py: all green DEFAULT and ELIDE-ON, both paths, including every >= 32 row; now also CI-gated with the flag ON. RED-TESTED: a temporary force-elide of const >= 32 (bare register shift, no mask) turned 10 rows red on both paths — the oracle catches unsound elision; hack removed. - Execution differentials with the flag ON over the moved fixtures: flight_seam flight_algo 0x07FDF307 MATCH, control_step 13/13, frame_slot_dce PASS, const_cse PASS. - shift_mask_elide_686.rs: per-function no-grow table over the corpus (both paths) + strict shrink on gust_mix + default==opt-out pin. - 10 new unit tests: mod-32 fold (< 32, >= 32, == 32 -> MOV), bridge mov-imm form, range-carried and-mask (#15 folds, #63 declines), unproven def declines, label-in-window declines, movw kept when the amount register has other readers, non-R12 pattern untouched. Closes #686. Refs #682 #683. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…ovably < 32 (#686) (#692) gale measured #682's unconditional AND R12,#31 mask at ~12% cyc/call (+14 B) on gust_mix, whose Q8 fixed-point shifts are all CONSTANTS — the mask can never fire there, yet every register-controlled i32 shift pays it. New peephole liveness::elide_shift_masks removes the mask ONLY when the amount is statically provable < 32; anything unproven keeps it — elision is an optimization, the mask stays the sound default. Two proven shapes, keyed on the #682 idiom (and r12,rK,#31 ; shift by r12 — emitted adjacently by both direct selectors, the Rocq-proved DSL rules, and the optimized bridge; the DSL rules stay MASKED, no proof changes): - Const amount: nearest preceding def of rK is a pure materialization (movw, or the bridge's mov #imm) over a fully-modeled redefinition- free window -> fold the whole triple to the immediate shift, REDUCED MOD 32 (so >= 32 amounts shrink too — the fold computes exactly the WASM semantics the mask enforces); C mod 32 == 0 lowers to MOV (imm5 == 0 encodes shift-by-32, the LSR/ASR pitfall). The movw drops when rK has no other reader (reg_dead_by_redef). This supersedes fold_immediate_shifts for the masked idiom — its movw->shift window is intercepted by the #682 and, so post-#682 it declined every const-amount register shift (the gust_mix regression's second half). - Range-carried amount: nearest def is and rK,rX,#c with c < 32 -> rK < 32 at the shift, the re-mask is a no-op; shift by rK directly. Covers the wasm-level x&31 / x&15 idioms. A #494 fact-spec value- range premise is the documented follow-up. Soundness scaffolding as the sibling folds: backward scan aborts on any reg_effect-unmodeled op (call/branch/LABEL = merge point); dropping the and r12 write is safe by the #212 R12-scratch convention; rotr is never masked (#682 exemption) so the pattern cannot match it; removal/rewrite-only before branch resolution (offset-neutral). FLAG-OFF (opt-in SYNTH_SHIFT_MASK_ELIDE=1) per the flag-then-flip protocol: the elision MOVES the frozen anchors — measured on this commit, per-function, no function grows, every const-shift function shrinks (bytes ON vs OFF, identical on both paths): control_step_decide 313 -> 293 (-20) flight_seam flight_algo 376 -> 296 (-80), controller_step 325 -> 241 (-84) flight_seam_flat flight_algo 520 -> 436 (-84), controller_step -84 gust_mix (the #686 fixture) 65 -> 55 (-10) — recovers the measured regression (the +14 B was mask + retained movw + wide shift) i32_shift_mask_682 shl32/shl33/shl300/shr300/sar300 -> 8-12 B each signed_div_const untouched Default (flag unset) is byte-identical to v0.37.1 everywhere: the frozen byte-gate passes unchanged, and shift_mask_elide_686.rs pins unset == opt-out. The default-on flip is the maintainer's separate refreeze (all differentials green on the new bytes, goldens re-pinned). Oracles on this commit: - i32_shift_mask_682_differential.py: all green DEFAULT and ELIDE-ON, both paths, including every >= 32 row; now also CI-gated with the flag ON. RED-TESTED: a temporary force-elide of const >= 32 (bare register shift, no mask) turned 10 rows red on both paths — the oracle catches unsound elision; hack removed. - Execution differentials with the flag ON over the moved fixtures: flight_seam flight_algo 0x07FDF307 MATCH, control_step 13/13, frame_slot_dce PASS, const_cse PASS. - shift_mask_elide_686.rs: per-function no-grow table over the corpus (both paths) + strict shrink on gust_mix + default==opt-out pin. - 10 new unit tests: mod-32 fold (< 32, >= 32, == 32 -> MOV), bridge mov-imm form, range-carried and-mask (#15 folds, #63 declines), unproven def declines, label-in-window declines, movw kept when the amount register has other readers, non-R12 pattern untouched. Closes #686. Refs #682 #683. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

…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

… register-pair ops — 316→411 applied, measured (#242) (#917) * rivet(VCR-REACH-001): increment 4 requirement — REACH, the i64 register-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 * VCR-REACH-001: model the i64 register-pair ops — one definition, three 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 * VCR-REACH-001: EXECUTION-gate the i64-pair shapes + widen VCR-RA-003'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 * VCR-REACH-001: mutation matrix, CI floors, measurement, CHANGELOG (#242) 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 * 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 * test(#916): drop the defect pin — the defect is fixed 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 * docs(#916): the lane's decline was overtaken — #919 fixed it, at five 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. --------- Co-authored-by: Claude <noreply@anthropic.com>

avrabe merged commit 956b45a into main Mar 21, 2026
6 checks passed

avrabe deleted the feat/renode-tests-release-prep branch March 21, 2026 19:57

Navigation Menu

Uh oh!

feat: Renode example tests + v0.1.0 release prep - #63