test(vcr-oracle): estimator↔encoder agreement oracle for the optimized path (#498, #242) - #511

avrabe · 2026-06-26T11:01:15Z

What

VCR-ORACLE-001 (epic #242). A CI-gated oracle that pins the optimized ARM path's hand-maintained byte-size estimator against the real Thumb-2 encoder, for every op the path emits.

Why this matters

ir_to_arm resolves branch displacements by summing estimate_arm_byte_size over the instruction stream. That estimator is a hand-maintained mirror of ArmEncoder::encode, kept by hand only because synth-synthesis cannot depend on synth-backend (the encoder lives downstream) — the structural cause behind #498. When the mirror drifts, a forward branch spanning the drifting op lands at the wrong byte: under-estimate → short (the #483-class miscompile), over-estimate → long. synth-backend sits downstream and can see both, so the oracle lives there.

How

Extract the inline instr_byte_size/reg_num closures from ir_to_arm to a module-level pub fn estimate_arm_byte_size(op: &ArmOp) -> usize. Logic-identical — the whitespace-normalized diff of the match body is empty; frozen byte gate + 59 synthesis tests confirm the optimized path is bit-identical.
Oracle (crates/synth-backend/tests/estimator_encoder_agreement.rs): for each op the optimized path emits, at the operand shapes it emits them in, assert estimate == encode().len() OR a documented KNOWN_GAP pinned to its exact measured (est, enc) pair. A no-wildcard coverage() match over all 220 ArmOp variants is a compile-time tripwire — a new variant won't compile until consciously classified OnPath/OffPath. (It forces classification, not an agreement case; that remains a documented manual step.)

Both failure paths verified non-vacuous: a perturbed gap value trips KNOWN_GAP CHANGED; an agree case pointed at a drift op trips NEW DRIFT.

Scope

A gap-documenting regression guard, NOT a #498 fix. Correcting the estimator is byte-changing codegen (shifts every optimized-path branch displacement) and stays a separately-gated step (re-freeze + execution differential + silicon). No release — pure refactor + test.

Findings (correct + extend #498's original report)

Optimized-path byte-size estimator is incomplete (Cmp/Cmn/Adds/Subs/Popcnt) — latent branch-displacement drift #498's claim that Cmp high-reg drifts is FALSE — 16-bit CMP (T2, 0x45xx) encodes high regs → 2 bytes; the estimator default is right. The real high-reg drifts are Cmn/Adds/Subs (no 16-bit high-reg / flag-setting form) → 4, est 2.
Popcnt is absent from the estimator entirely (_ => 2) but the encoder expands it to 86 bytes — an 84-byte hole, the largest single drift.
I64DivU/RemU/DivS/RemS, I64Popcnt, I64Extend32S over-estimate (e.g. DivU est 100 vs 74).
far BOffset/BCondOffset need the 4-byte form but the estimator sizes the pre-resolution 0-offset placeholder as 2 (single-pass chicken-and-egg).
Mov small-negative imm: the encoder's signed imm <= 255 test emits a wrong-value 2-byte MOVS #(imm&0xFF) — a latent encoder bug, surfaced here as a side effect.

Refs #498, #242.

🤖 Generated with Claude Code

…d path (#498, #242) VCR-ORACLE-001. The optimized ARM path (`ir_to_arm`) resolves branch displacements by summing a hand-maintained byte-size *estimator* over the instruction stream — a mirror of the Thumb-2 encoder, kept by hand only because synth-synthesis cannot depend on synth-backend (the encoder lives downstream). When the mirror drifts, a forward branch spanning the drifting op lands at the wrong byte (the #483-class miscompile). This is the structural cause behind #498. - Extract the inline `instr_byte_size`/`reg_num` closures from `ir_to_arm` to a module-level `pub fn estimate_arm_byte_size(op: &ArmOp) -> usize` (logic-identical; whitespace-normalized diff of the match body is empty). Frozen byte gate + 59 synthesis tests confirm the optimized path is bit-identical. - Add `crates/synth-backend/tests/estimator_encoder_agreement.rs` (synth-backend CAN see both the estimator and the real encoder): for every op the optimized path emits, at the operand shapes it emits them in, assert `estimate_arm_byte_size(op) == ArmEncoder::encode(op).len()` OR a documented `KNOWN_GAP` pinned to its exact measured (est, enc) pair. A no-wildcard `coverage()` match over all 220 `ArmOp` variants is a compile-time tripwire: a new variant won't compile until consciously classified OnPath/OffPath. (It forces classification, NOT an agreement case — an OnPath variant with no `cases()` entry still passes vacuously; adding it is a documented manual step.) Scope: a gap-documenting REGRESSION GUARD, NOT a #498 fix — correcting the estimator is byte-changing codegen (separately gated). Findings the oracle records (correct + extend #498's report): - #498's claim that `Cmp` high-reg drifts is FALSE: 16-bit CMP (T2, 0x45xx) encodes high regs → 2 bytes. The real high-reg drifts are `Cmn`/`Adds`/`Subs` (no 16-bit high-reg / flag-setting form) → 4, est 2. - `Popcnt` is absent from the estimator entirely (`_ => 2`) but the encoder expands it to 86 bytes — an 84-byte hole, the largest single drift. - `I64DivU/RemU/DivS/RemS`, `I64Popcnt`, `I64Extend32S` over-estimate. - far `BOffset`/`BCondOffset` need the 4-byte form but the estimator sizes the pre-resolution 0-offset placeholder as 2 (single-pass chicken-and-egg). - `Mov` small-negative imm: encoder's signed `imm <= 255` test emits a wrong-value 2-byte `MOVS #(imm&0xFF)` — a latent encoder bug, surfaced here. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

codecov · 2026-06-26T11:06:43Z

Codecov Report

❌ Patch coverage is 95.18072% with 4 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-synthesis/src/optimizer_bridge.rs	95.18%	4 Missing ⚠️

📢 Thoughts on this report? Let us know!

…n estimator (#511 follow-on, #242) (#512) The `#[cfg(test)]` byte-counting helper `count_arm_byte_size` was a hand-maintained mirror of the optimized-path size table — a drifted copy with its own `_ => 4` default and only a partial op set. PR #511 extracted that table to `estimate_arm_byte_size` AND established the real independent check (the `estimator_encoder_agreement` oracle, which pins the table against the actual Thumb-2 encoder, the ground truth). With the encoder as the independent oracle, the local hand-drifted proxy is redundant. Replace its body with `arm.iter().map(estimate_arm_byte_size).sum()` and delete the now-unused `reg_idx` test helper (−43 lines). The three byte-count tests (`test_issue94_*`) assert `bytes < 30` on POST-optimization sequences (Mov/Movw/Asr, all ≤4 in both tables) plus direct structural checks (`!has_runtime_shift`, `asr_count == 1`); the production estimator's `_ => 2` default yields counts ≤ the old proxy, so every assertion still holds. Test-only: production codegen is untouched — `estimate_arm_byte_size` is unchanged, only the test helper's body is replaced (frozen-by-construction). Whole synth-synthesis suite green (463 lib tests); no unused-symbol warnings (confirms `reg_idx` had no other consumer). Scope: test consolidation, not a codegen change. Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

… (#513) The register allocator reads each op's def/use classification two ways that MUST agree: `reg_effect` (liveness — which registers an op defines vs uses) and `rewrite_op` (renaming — which fields it rewrites through the def-map vs the use-map). If they drift — an op edited in one but not the other, or a new op modeled inconsistently — the allocator renames a def as a use and silently miscompiles. liveness.rs is the actively-churned heart of VCR-RA and nothing pinned this invariant. This is the Track-A (allocator) analogue of the #511 Track-B (encoder) agreement oracle. There is no third ground truth here, so the achievable invariant is mutual CONSISTENCY, checked structurally without a register extractor: build the def/use maps FROM `reg_effect`'s classification (def regs → a def sentinel, use regs → a use sentinel, read-modify-write regs → one shared sentinel so `rewrite_op` doesn't decline), apply `rewrite_op`, then read the result back with `reg_effect`. If the two agree on every field, every register is rerouted to a sentinel; a SURVIVING original register means `rewrite_op` routed a field through the opposite map — the drift. What the oracle pins, for all 55 modeled ops: - the def/use ROLE of every field (survivor check), and - the read-modify-write PROPERTY of dual-role fields (Movt/MovtSym/SelectMove `rd`): a register `reg_effect` reports in both defs and uses must make `rewrite_op` DECLINE when the two maps disagree on it — otherwise the shared sentinel would mask a drift that turned the RMW field def-only or use-only. - `is_modeled`: a no-wildcard match over all 220 `ArmOp` variants — a new variant won't compile until classified (the tripwire; it already caught `B` and `Nop` being mis-bucketed during authoring). The modeled (true) side is exhaustive (careful 55-variant extraction, all constructed + checked); the unmodeled (false) side is spot-sampled. Scope: a regression GUARD, not a bug fix — the classification AGREES for every modeled op today (measured exhaustively). Test-only; no production code changes. Negative tests confirmed non-vacuous on BOTH branches: misrouting one op's `rd` (def→use) trips the survivor check; dropping `Movt`'s RMW decline trips the RMW check. 464 synth-synthesis lib tests green. Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

… size guard (#242) (#519) gale's v0.17.0 burndown found SYNTH_CONST_CSE=1 GREW a tiny --relocatable function (gust_mix 90→92 B). On --relocatable the optimized path's inline const cache never runs (select_direct), so the post-hoc liveness::apply_const_cse acts alone: it retargeted a use, kept a constant resident longer, and defeated a downstream immediate-fold that would otherwise have absorbed the constant. A remove-movw + rename-use post-pass on already-register-assigned instructions cannot itself spill — it grows code only by changing what a later pass does. Two fixes: 1. CSE-LAST: move the apply_const_cse call to run after every immediate-fold (fold_immediate_shifts / fold_uxth), before branch resolution. Foldable consts are already folded-and-gone, so CSE can no longer defeat a fold. This structurally eliminates gale's mechanism. 2. Per-segment SIZE GUARD in apply_const_cse: stage each segment's removals/ retargets, estimate the rewritten segment via estimate_arm_byte_size (the #511 encoder mirror), and commit only if it does not grow — so a retarget that flips a 16-bit ldr to its 32-bit form (low→high base register) is declined. Verification: - Two contrasting liveness unit tests prove the guard non-vacuous: identical segments differing only in the resident register's class (high R8 → encoding flips → declines; low R2 → no flip → commits). - const_cse_differential.py: flag-on values bit-identical to wasmtime across the corpus; new per-function no-regression gates on BOTH the optimized and --relocatable paths (the latter is the path gale's bug lives on — currently inert on the arithmetic corpus, a tripwire for when gust_mix.wat lands). - Flag-off byte-identical (frozen gate 3/3, const_cse golden 2/2). - cargo test --workspace green (85 suites); fmt + clippy clean. const-CSE stays flag-off (SYNTH_CONST_CSE). The pressure/size prerequisite for the eventual default-on flip is now closed; alias-eviction remains the sole open prerequisite. gale's exact gust_mix case is not yet reproduced in-tree — fixture requested on #242 to pin the trigger. Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

…f-99 miscompile The optimized path resolves BOffset/BCondOffset displacements to byte-accurate halfword offsets inside optimizer_bridge::ir_to_arm — BEFORE apply_const_cse runs — and nothing re-resolves them afterwards. Both const-CSE passes (PR1 cross-reg fold + PR2 extending hoist) violated two invariants of that stream on spill_frame_499.wat::nested (the CI spill-frame teardown oracle, nested(1,) wrote 0 where wasmtime writes 99 at offset 32): 1. JOIN INVISIBLE: a resolved branch target carries no Label op, so a "straight-line segment" spanned the if/else join — the hoist retargeted the join tail's `add r12,r12,r4` onto r0, whose base value is only materialized on the fall-through arm (on the taken arm r0 = the sel param), so the taken path stored 55 over the 99. 2. DISPLACEMENT STALE: deleting the arm's two redundant movw+movt pairs (16 bytes) between the `b` and its target made the pre-resolved `b +0x42` overshoot the join by exactly those 16 bytes. Soundness rule (liveness.rs, resolved_branch_geometry): reconstruct every numeric branch's target index by mirroring the bridge's own offset table (estimate_arm_byte_size, the #511-pinned estimator), then in BOTH passes (1) treat each target as a segment BARRIER — held/hoist state never crosses a join — and (2) FREEZE the total byte size of any segment lying between a branch and its target (commit requires new_bytes == orig_bytes there, not merely no-grow). Unmappable targets or mixed Label/numeric streams decline the whole function. Label-based (--relocatable/direct) streams are unaffected: Label was already a barrier and their branches resolve AFTER this pass. Verification (fix, not fixture — the oracle is untouched): - spill_frame_499_differential.py: PASS (was FAIL nested(1,), off=32 99 vs 0) - full scripts/repro sweep: 54 scripts, 52 PASS both default AND SYNTH_CONST_CSE=0; sret_decide = pre-existing, flag-independent (#359-era characterization, bytes identical on/off); wake_path skipped (needs gale's external gist fixture /tmp/merged.wat) - corpus re-measured: 152 fixture×path combos, 0 functions grow, 38 shrink, total -488 B (was -536 B — the returned 48 B are exactly the branched shapes' unsound wins: nested -24 -> 0, init_branch -16 -> -8); spill12 keeps its full -88 B; all four const_cse_reduction_242 goldens (default + escape-hatch) pass UNCHANGED - 4 new regression tests: target-as-barrier, span freeze (fold + hoist), and fold-outside-span still commits - cargo test -p synth-synthesis -p synth-cli (45 suites ok), fmt, clippy -D warnings: clean Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

…on (#242) (#604) * feat(vcr-ra)!: retire inline const aliasing; SYNTH_CONST_CSE default-on (#242) Two coupled steps, oracle-gated in order: 1. RETIRE the bridge-level inline const aliasing (the flip blocker verified in PR #592): the reg_holds_const alias arm in optimizer_bridge::ir_to_arm made two live vregs share one physical register, breaking the spill model's vreg<->reg bijection (alias-eviction stale-read hazard). Deleted outright — const materialization always falls through to normal allocate-and-emit; the flag now gates ONLY the post-hoc, liveness-proven liveness::apply_const_cse passes (PR1 #519 + PR2 #562). The recorded reg_effect DEF-COMPLETENESS prerequisite retires with it (the post-hoc passes treat unmodeled ops as segment boundaries and decline). 2. FLIP SYNTH_CONST_CSE DEFAULT-ON (opt-out =0), full #583/#592 refreeze ritual: differentials re-run green on the new default bytes BEFORE any golden was pinned (const_cse, frame_slot_dce 8/8, flight_seam 0x07FDF307, spill_rung_581 6/6, volatile_segment_543 incl. a new default-on composition check, control_step 13/13). Corpus sweep 152 fixture-x-path combos: 0 functions grow, 40 shrink (const_cse::spill12 236->148 B), total -536 B. Frozen ARM anchors re-pinned (control_step 304->300, flight_seam 730->726; flat + signed_div_const byte-identical); RV32 untouched. SYNTH_CONST_CSE=0 restores every pre-flip byte (CI-gated: const_cse_escape_hatch_restores_old_bytes_242 + frozen_fixtures_const_cse_escape_hatch_restores_old_bytes); the older stack-fwd/spill-realloc escape hatches gain the =0 composition. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * fix(const-cse): decline across branch boundaries — nested(1,) store-of-99 miscompile The optimized path resolves BOffset/BCondOffset displacements to byte-accurate halfword offsets inside optimizer_bridge::ir_to_arm — BEFORE apply_const_cse runs — and nothing re-resolves them afterwards. Both const-CSE passes (PR1 cross-reg fold + PR2 extending hoist) violated two invariants of that stream on spill_frame_499.wat::nested (the CI spill-frame teardown oracle, nested(1,) wrote 0 where wasmtime writes 99 at offset 32): 1. JOIN INVISIBLE: a resolved branch target carries no Label op, so a "straight-line segment" spanned the if/else join — the hoist retargeted the join tail's `add r12,r12,r4` onto r0, whose base value is only materialized on the fall-through arm (on the taken arm r0 = the sel param), so the taken path stored 55 over the 99. 2. DISPLACEMENT STALE: deleting the arm's two redundant movw+movt pairs (16 bytes) between the `b` and its target made the pre-resolved `b +0x42` overshoot the join by exactly those 16 bytes. Soundness rule (liveness.rs, resolved_branch_geometry): reconstruct every numeric branch's target index by mirroring the bridge's own offset table (estimate_arm_byte_size, the #511-pinned estimator), then in BOTH passes (1) treat each target as a segment BARRIER — held/hoist state never crosses a join — and (2) FREEZE the total byte size of any segment lying between a branch and its target (commit requires new_bytes == orig_bytes there, not merely no-grow). Unmappable targets or mixed Label/numeric streams decline the whole function. Label-based (--relocatable/direct) streams are unaffected: Label was already a barrier and their branches resolve AFTER this pass. Verification (fix, not fixture — the oracle is untouched): - spill_frame_499_differential.py: PASS (was FAIL nested(1,), off=32 99 vs 0) - full scripts/repro sweep: 54 scripts, 52 PASS both default AND SYNTH_CONST_CSE=0; sret_decide = pre-existing, flag-independent (#359-era characterization, bytes identical on/off); wake_path skipped (needs gale's external gist fixture /tmp/merged.wat) - corpus re-measured: 152 fixture×path combos, 0 functions grow, 38 shrink, total -488 B (was -536 B — the returned 48 B are exactly the branched shapes' unsound wins: nested -24 -> 0, init_branch -16 -> -8); spill12 keeps its full -88 B; all four const_cse_reduction_242 goldens (default + escape-hatch) pass UNCHANGED - 4 new regression tests: target-as-barrier, span freeze (fold + hoist), and fold-outside-span still commits - cargo test -p synth-synthesis -p synth-cli (45 suites ok), fmt, clippy -D warnings: clean Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

… silent 0 (#610) (#613) All four ops (plus div_s/rem_s, same disease) compiled without error and returned 0 for every input on the ARM Cortex-M path. Root cause was in the Thumb-2 encoder's multi-instruction expansions, one disease in two forms: * I64Rotl/I64Rotr: the expansion used hardcoded R3/R4 scratch that collided with selector-assigned registers, then its own `POP {R4}` restored the saved scratch OVER the computed result (rd_lo == R4 in the repro) — the op returned the caller's stale R4: 0 under qemu/unicorn reset state. * I64DivU/I64RemU/I64DivS/I64RemS: the expansion IGNORED its register fields outright (`rdlo: _, ...` — hardcoded R0:R1 dividend, R2:R3 divisor, result to R0:R1) while the selector allocated rd elsewhere (R4:R5), which the core's own POP then clobbered with stale values. Fix: a fixed-ABI wrapper around each core — save R0-R3, marshal the operand registers into the core's fixed input regs via the stack (permutation-safe: every source is read before any fixed reg is written), run the core (self-preserving for R4+; R12 is encoder scratch, never allocatable #212), MOV the result pair into the selector's rd (loud Err on the impossible swapped pair), restore R0-R3 skipping the result registers. The rot cores are rewritten to fixed regs (R0:R1 value, R2 amount, R3+R12 scratch); the div/rem shift-subtract cores are byte-identical inside the wrapper. Divide-by-zero now traps (`ORRS R12,R2,R3; BNE +0; UDF #0`), matching WASM semantics and the i32 guard — previously div/0 silently returned 0. Estimator kept in exact agreement (#498/#511 oracle): rot 74→102 bytes, div_u/rem_u/div_s/rem_s 74/78/126/124 → 120/124/172/170; all sizes are register-independent by construction. Frozen fixture hashes bit-identical (these ops appear in no frozen anchor). Red→green: scripts/repro/i64_rot_div_610_differential.py (55 vectors — rot identity/32/63/>=64 + hi-half twins, div by 1/self/0-trap, high-bit patterns, signed variants, shl control) vs wasmtime under unicorn: 40/55 MISMATCH on v0.30.0, 55/55 OK after. Wired as an isolated CI oracle job. New encoder unit tests pin the rd-landing tail, the zero-divisor guard, the rd∈R0-R3 skip-restore, and the swapped-pair loud reject. Closes #610 Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

…wired flag-off (#242) (#623) The first wired increment of the Rocq-discharged selector DSL, per docs/design/vcr-sel-001-first-increment.md — a hand-written select_default arm is served from a verified rule without moving a byte of frozen output. - Rule table (crates/synth-synthesis/src/sel_dsl/mod.rs RULES): declarative op -> parameterized ARM sequence, registers as variables, side conditions explicit. Tier-A six (i32 add/sub/mul/and/or/xor) + tier-B i32.rotl with the SideCondition::NotAlias(Rs, Rn) scratch constraint carried in the rule format and enforced Ok-or-Err in the generated code. - Generator emits plain Rust lowerings COMMITTED to the tree (sel_dsl/generated.rs, rustfmt-stable, pinned by generated_lowering_is_up_to_date; SYNTH_SEL_DSL_REGEN=1 to regenerate). - select_default keeps dispatch: the seven migrated arms delegate to the generated rules behind SYNTH_SEL_DSL (default OFF) — OFF keeps the original hand-written bodies, byte-identical by construction. The exhaustive WasmOp match stays. - Rocq: coq/Synth/Synth/VcrSelRules.v — one universally-quantified T1 theorem per rule, 7 Qed / 0 Admitted, naming 1:1 (rule_X <-> rule_X_correct); tier-A via synth_binop_proof_poly verbatim, rotl via the pilot's stepped proof with the rs <> rn hypothesis. - Coverage gate: //coq:verify_proofs is now a test_suite = :rocq_proofs + :vcr_sel_rules_coverage (manifest pinned to RULES by a cargo test; a rule without its Qed cannot merge). Negative-tested both failure modes. - Gate 1 (mirror-pin, #511/#513 pattern): hand-written arm == generated rule ArmOp sequences for all 7 rules. Gate 2: frozen_codegen_bytes 9/9 green with flag OFF and with SYNTH_SEL_DSL=1. - artifacts: VCR-SEL-001 approved -> implemented (flip + re-freeze ritual still owed before verified). Refs #242. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

…472, #601, epic #242) (#626) Salvaged from an interrupted session (299 tool uses): select_inner now MEASURES promotion profitability — lowers the unpromoted baseline plus every candidate subset (<=3 locals -> <=7 attempts) and keeps a promoted lowering only when emitted_byte_size <= baseline. Prices per-return epilogue restores and WAR-snapshot mvs by construction (the #601 flip blocker). emitted_byte_size mirror-pinned to assemble_function pass-1 sizing (#511 lesson). Corpus no-grow gate: rv32_local_promo_no_grow_corpus_472. Flag SYNTH_RV_LOCAL_PROMO stays opt-in. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

…rflow trap (#632, #633) (#634) #632 — the I64Popcnt expansion's own scratch restore (POP {R3,R4,R5}) clobbered the freshly computed count whenever the allocator-assigned rd landed inside the restore set (ADDS rd,R4,R5 one instruction before the pop). Structural fix on both the Thumb-2 and A32 arms: the total is carried ACROSS the restore in R12 (encoder scratch, never allocatable per #212, never in any restore set) and moved into rd only after the pop — no choice of rd can collide. The entry marshal also routes rnlo through R12 so an operand pair living at (R3,R4) can no longer read a clobbered R4, and the new MOV/MOV.W forms are total over rd/rnhi = R8 where the old 3-bit T1 fields silently corrupted the encoding. Expansion-family audit (pop-restore clobber class): I64Popcnt was the only affected op on either ISA. I64Div{S,U}/I64Rem{S,U} and I64Rotl/Rotr stage their result in R0:R1 before their scratch pop and route it through the #610 fixed-ABI exit (which skips restored registers); I64Clz/I64Ctz and i32 Popcnt push no scratch. #633 — the i64 signed-division expansion emitted only the divide-by-zero guard: INT64_MIN/-1 negated the dividend onto itself and silently returned INT64_MIN instead of trapping (WASM Core 4.3.2 idiv_s). Mirror the i32 path's overflow guard on the #610/#613 fixed-ABI wrapper path (dividend R0:R1, divisor R2:R3): dividend==INT64_MIN && divisor==-1 -> UDF #0, on both the Thumb-2 and A32 I64DivS arms. I64RemS deliberately stays guard-free — rem_s(INT64_MIN,-1) is defined as 0 and must not trap (pinned by the fix-guard twin vectors and unit tests). Oracles (red -> green): - scripts/repro/i64_popcnt_632_differential.py — unicorn-vs-wasmtime, symtab-based: 6/11 vectors MISMATCH (0 for every input) on main, 11/11 OK post-fix. - scripts/repro/i64_divs_overflow_633_differential.py — INT64_MIN/-1 returned 0 instead of TRAP on main (2 MISMATCH), 16/16 OK post-fix including rem_s(INT64_MIN,-1)=0 no-trap and div-by-zero still-traps. - estimator_encoder_agreement (the #511 pin): I64Popcnt 172->180, I64DivS 172->194, register-independent. - frozen_codegen_bytes: all anchors untouched (no i64 popcnt / div_s-overflow shapes in the frozen fixtures). Closes #632 Closes #633 Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

…lision, two-guard obligation split (VCR-PERF-002) (#636) Upgrades exactly the op class phase 2 deliberately left untracked: the fact_spec symbolic walk now tracks i32/i64 div/rem — never deleting them (they can trap; a div result carries no erasable producer slice) but discharging up to TWO INDEPENDENT per-site guard obligations through the ordeal-backed certificate-checked BvSolver BEFORE emission: divide-by-zero guard (div_u/div_s/rem_u/rem_s, i32+i64): UNSAT(P ∧ divisor == 0) INT_MIN/-1 overflow guard (div_s ONLY; rem_s(INT_MIN,-1)==0 never traps): UNSAT(P ∧ dividend == INT_MIN ∧ divisor == -1) THE TWO-GUARD DISTINCTION (#633/#634 synergy): a divisor-nonzero fact (kind 3) discharges the first but NOT the second — divisor ≠ 0 does not exclude -1, so the overflow guard is RETAINED (loud decline) unless the premises independently prove it (divisor ∈ [1,N] proves both; either fact kind works). Sat/Unknown/no-premise ⇒ loud decline, general lowering. Mechanics: discharged obligations become per-site marks (FactSpecResult::elide_div_zero/elide_div_ovf, remapped through any clamp-elision rewrite), threaded via CompileConfig::fact_div_zero_elide/ fact_div_ovf_elide to the DIRECT selector only — the optimized path's IR passes renumber instructions, so marked functions route to select_with_stack (#507/#509 honest-degradation pattern; never fires without SYNTH_FACT_SPEC + facts + a discharged obligation). i32 guards are selector-emitted and skipped; i64 guards live in the ArmOp::I64Div*/Rem* encoder expansions, which gain per-guard elision flags (Thumb-2 + A32), with estimator sizes tracking the flags (#511 agreement oracle extended with the 5 elided variants). Oracles: 9 new fact_spec unit gates (two-guard matrix, i64 width discipline via current_func_params_i64, mark remapping); encoder splice pins (elision removes EXACTLY the 8 B/12 B zero guard; overflow retained under zero-only elision); fact_spec_div_494.rs byte evidence (guard UDFs present without facts, absent with facts+flag; qs64 keeps exactly 1 UDF = the retained INT64_MIN/-1 guard; Sat-decline byte-identity; debug-only SYNTH_FACT_SPEC_FORCE_ADMIT red lever screams); fact_spec_div_494_differential.py (1584-case in-bounds sweep specialized ≡ wasmtime ≡ unspecialized; qs64(INT64_MIN,-1) traps in BOTH wasmtime and the specialized build; --expect-decline byte-identity; --force-admit RED leg: wasmtime traps at divisor=0, the forced unsound build returns 0) — all CI-gated by the extended fact-spec-oracle job. Fixture bytes (cortex-m4): qu 16→12, qs 36→12 (both guards proven dead), ru 20→16, qs64 214→206 (zero guard spliced, 22 B overflow guard retained); .text 446→406. Frozen anchors bit-identical (no fixture carries facts); flag default OFF. Closes nothing yet — #494 phase 3 (gale measurement) remains. Refs #494, #242, #633, #634. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

…rem_s drops the spurious INT_MIN/-1 guard (#666) (#668) #665 — wasm `unreachable` compiled to a NO-OP on thumb-2 AND rv32 (falls through instead of trapping, WASM Core §4.4.5). Root cause was ONE decode drop: `convert_operator` returned `None` for `Unreachable` and `is_intentionally_ignored` whitelisted it alongside `Nop`, so no backend ever received the op — the selector trap arms (ARM `UDF #0`, RV32 `ebreak`) already existed but were dead code. Fix per path: - decoder (synth-core): `Unreachable` now decodes to `WasmOp::Unreachable`; only `Nop` stays intentionally ignorable. - ARM direct (`select_with_stack`) + `select_default`: existing `UDF #0` arms now fire (no change needed). - ARM optimized path (optimizer_bridge): previously lumped `Unreachable` in with Nop as an IR placeholder — now a typed loud-DECLINE to the direct selector (the bridge `Opcode` enum has no trap opcode; adding one would ripple through the #513 mirror-pinned reg_effect/rewrite_op machinery). Same decline-don't-drop pattern as #120 floats / #500 non-tail return. No new ArmOp on the optimized path, so the #511 estimator oracle is untouched (Udf was already covered by the div-zero guards). - RV32: existing `ebreak` arm now fires (no change needed). - aarch64: new `brk #0` encoder + selector arm (was a loud-decline). #666 — rv32 `i32.rem_s(INT_MIN,-1)` spuriously trapped: the selector shared div_s's INT_MIN/-1 overflow `ebreak` guard with rem_s via `bin_with_signed_div_traps`. WASM §4.3.2 defines irem_s(INT_MIN,-1) = 0 with NO trap, and RISC-V M-ext `rem` already returns 0 for the overflow case (unprivileged spec §7.2), so rem_s now takes plain `bin_with_zero_trap` — zero-divisor guard KEPT, bare `rem` is exactly wasm-correct. The pre-existing test `rv32_signed_rem_also_gets_overflow_guard` pinned the BUG; it is rewritten as the #633-twin fix-guard pins (`rv32_signed_rem_carries_only_zero_guard_666` + `rv32_signed_div_still_carries_both_guards_666`), mirroring ARM's `test_633_i64_rems_has_no_overflow_guard` and the existing i64 RV32 pin. Oracles (red on origin/main, green here; CI job trap-semantics-oracle): - scripts/repro/unreachable_665_differential.py — thumb2 + rv32 under unicorn vs wasmtime: bare `unreachable` traps, guarded `unreachable` taken traps, NOT taken returns normally (non-vacuity). Red on main: boom(7,9) "returned" 7 (arg fall-through) on both ISAs. Known gap kept visible: rv32 loud-declines the if/else-result-with-unreachable shape (#343 arity check) — contract-compliant (never falls through). - scripts/repro/rem_s_666_differential.py — rv32 trap table: rems(INT_MIN,-1)→0 no-trap (red on main: spurious ebreak), rems(INT_MIN,1)→0, rems(7,3)→1, rems(-7,3)→-1, rems(7,0) traps, divs(INT_MIN,-1) traps, divs(7,0) traps, divs(7,3)→2. Frozen anchors 10/10 bit-identical (no fixture contains `unreachable` — verified control_step/flight_seam/flight_seam_flat/signed_div_const). Workspace tests 108/108 suites green; fmt + clippy -D warnings clean. Fixes #665 Fixes #666 Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

….0xFFF (#681) (#690) encode_thumb32_add_imm packed the RAW immediate into the T3 ADD.W i:imm3:imm8 field, which is a ThumbExpandImm MODIFIED immediate — correct only for imm <= 0xFF. ThumbExpandImm(0x200) = 0 and ThumbExpandImm(0x400) = 0x8000_0000, so every dynamic-address load/store with a static offset in [256, 4095] silently computed a WRONG address. In --safety-bounds software the guard (correct T4 ADDW) checked the intended address while the access used the mis-encoded one — a bounds-check bypass. #253/#255 ThumbExpandImm class, reached via the #382 paths. Fix: imm <= 0xFFF delegates to encode_thumb32_add, which already picks T3 (<= 0xFF, raw == expanded, bit-identical) vs ADDW T4 plain imm12 (0x100..=0xFFF) per #253. The > 0xFFF MOVW/MOVT path is unchanged, so byte sizes are unchanged (estimator agreement #511 stays green). Class audit (no wildcard survives, #634 style): - ArmOp::Rsb (Thumb T2): field is ThumbExpandImm-coded with NO plain imm12 form — now gated on try_thumb_expand_imm, Err on non-representable. All emitters use imm 32 (byte-identical). - ArmOp::Rsb (A32): imm was silently masked & 0xFF (#378 class) — now Err for imm > 0xFF. - encode_thumb32_and_imm_raw: raw-packed ThumbExpandImm field — now gated; only caller (POPCNT, #0x3F) byte-identical. - encode_thumb32_sub/adds/subs/cmp already correct (T4 / expand-gated). Oracles: - test_encode_add_imm_thumb_expand_681: clang -target thumbv7m pinned bit-for-bit (0xFF/0x100/0x104/0x200/0x3FC/0x400/0xFFF + rd/rn perm). - test_encode_add_imm_large_350's 0x123 assertion upgraded from length-only (which let the mis-encoding pass CI) to exact bytes. - scripts/repro/addw_offset_681_differential.py: unicorn-vs-wasmtime, dynamic base + static offsets, i32/i8/i16/i64 load+store, bounds none+software incl. the bypass pin and OOB trap-to-trap. RED on pre-fix main (36 mismatches: clobber returns 4660 not 111; offset 1024 faults 2 GiB past base), GREEN post-fix (49/49). CI-wired in the trap-semantics oracle job. - Frozen anchors 10/10 byte-identical; estimator agreement green; workspace tests, fmt, clippy -D warnings clean. Closes #681 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

…the type-id sidecar (#676) A HETEROGENEOUS funcref table (mixed signatures — falcon's fused 41-slot dispatch table) can never satisfy the closed-world type check, so every call_indirect through it loud-declined (20 falcon funcs). WASM Core §4.4.8 makes the mismatch a RUNTIME trap, so the sound lowering is the runtime check itself: the object now carries a type-id sidecar (.synth.table_type_ids — one LE u32 STRUCTURAL signature class id per slot, region order; structurally-equal types share one dense 1-based id, the meld 31-decls/25-distinct shape; id 0 reserved for null slots) which the extended R11 layout contract places at R11 + sum(all table sizes)*4, mirroring the pointer region slot for slot. The dispatch inserts, between the #642 bounds guard and the pointer load, on both Thumb-2 and A32: mov ip, idx, lsl #2 ; add ip, r11, ip ; ldr ip, [ip, #type_off] cmp ip, #expected_class_id ; beq ok ; udf The compare subsumes the #664 null trap (id 0 never equals an expected id >= 1), so heterogeneous dispatches emit null_check=false. Encoding ranges decline loudly (sidecar offset > LDR imm12, class id > 255). Homogeneous tables emit type_check=None + no sidecar section — bytes identical BY CONSTRUCTION (the #650 offset-0 / #664 null_check=false trick): whole-ELF cmp verified against origin/main on the #642/#650/#664 fixtures x cortex-m3/r5, frozen anchors 10/10, workspace green. The estimator is untouched (CallIndirect is direct-selector-only, excluded from the #511 agreement oracle). New CI-gated differential (call_indirect_676_differential.py, Thumb-2 + A32): mixed 5-slot table (two classes interleaved + structural-dup type + nulls) — matching-class calls equal wasmtime, wrong-class ("indirect call type mismatch"), null and OOB indices all stop at a UDF; wasmtime's trap REASONS are asserted per category. Non-vacuous red: a build without the check CALLS the wrong-typed function and returns a wrong value. Red at compile on origin/main (capability upgrade). Object-level contract locked in cargo CI (heterogeneous_table_676.rs: sidecar ids [1,2,1,0,0] + no-sidecar for the homogeneous fixtures). Lineage: #642 guards (#646), #650 multi-table (#653), #664 null slots (#669) — this closes the terminal layer of falcon's call_indirect story. Closes #676 Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…the type-id sidecar (#676) (#696) A HETEROGENEOUS funcref table (mixed signatures — falcon's fused 41-slot dispatch table) can never satisfy the closed-world type check, so every call_indirect through it loud-declined (20 falcon funcs). WASM Core §4.4.8 makes the mismatch a RUNTIME trap, so the sound lowering is the runtime check itself: the object now carries a type-id sidecar (.synth.table_type_ids — one LE u32 STRUCTURAL signature class id per slot, region order; structurally-equal types share one dense 1-based id, the meld 31-decls/25-distinct shape; id 0 reserved for null slots) which the extended R11 layout contract places at R11 + sum(all table sizes)*4, mirroring the pointer region slot for slot. The dispatch inserts, between the #642 bounds guard and the pointer load, on both Thumb-2 and A32: mov ip, idx, lsl #2 ; add ip, r11, ip ; ldr ip, [ip, #type_off] cmp ip, #expected_class_id ; beq ok ; udf The compare subsumes the #664 null trap (id 0 never equals an expected id >= 1), so heterogeneous dispatches emit null_check=false. Encoding ranges decline loudly (sidecar offset > LDR imm12, class id > 255). Homogeneous tables emit type_check=None + no sidecar section — bytes identical BY CONSTRUCTION (the #650 offset-0 / #664 null_check=false trick): whole-ELF cmp verified against origin/main on the #642/#650/#664 fixtures x cortex-m3/r5, frozen anchors 10/10, workspace green. The estimator is untouched (CallIndirect is direct-selector-only, excluded from the #511 agreement oracle). New CI-gated differential (call_indirect_676_differential.py, Thumb-2 + A32): mixed 5-slot table (two classes interleaved + structural-dup type + nulls) — matching-class calls equal wasmtime, wrong-class ("indirect call type mismatch"), null and OOB indices all stop at a UDF; wasmtime's trap REASONS are asserted per category. Non-vacuous red: a build without the check CALLS the wrong-typed function and returns a wrong value. Red at compile on origin/main (capability upgrade). Object-level contract locked in cargo CI (heterogeneous_table_676.rs: sidecar ids [1,2,1,0,0] + no-sidecar for the homogeneous fixtures). Lineage: #642 guards (#646), #650 multi-table (#653), #664 null slots (#669) — this closes the terminal layer of falcon's call_indirect story. Closes #676 Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

…umb-2 (#619, #369) The VFP encoder + selector arms existed but the decoder dropped every scalar float op, so `synth compile -t cortex-m4f` honest-rejected f32 on every CLI path. Worse, the "existing" VFP lowering was a non-functional prototype: select_with_stack fell through to select_default's blind %16 round-robin `alloc_vfp_reg`, so f32.const;f32.const;f32.add emitted VADD S2,S3,S4 over garbage. This wires the real bridge for the phase-1 honest subset. Delivered: - Decoder un-drops in-scope f32 ops (add/sub/mul/div, 6 compares, i32.trunc_f32_s/u, f32.convert_i32_s/u, f32.const); f64 + rest stay dropped. - Real VFP value stack in select_with_stack: StackVal::Float, S0..S15 allocator (no spilling — loud-bail on exhaustion), f32 op arms. Integer path untouched. - AAPCS-VFP: f32 params homed in S0..S15 (params_f32 threaded decoder → CompileConfig → selector), f32 result in S0. - FPU gate: m4f/m7/m7dp lower f32; m0/m3/r5 honest-reject with a clear message. - .ARM.attributes Tag_FP_arch=VFPv4-D16 + Tag_ABI_VFP_args on FPU targets; reset handler enables CP10/CP11 in SCB->CPACR (M4F FPU is off at reset). - Fix two latent encoder bugs surfaced by making float reachable: the signed/unsigned VCVT constants were swapped (convert_i32_s was unsigned), and the CPACR ORR mask encoded #0x07800000 instead of #0x00F00000. Held (honest-subset, chosen): f64 (phase 2), f32 load/store + local.set/tee (phase 1b), mixed f32/int param lists + f32-with-calls (loud-decline). Oracle: scripts/repro/f32_vfp_619_differential.py — unicorn (ARM/Thumb, FPU enabled) vs wasmtime, bit-exact on boundary values. RED on origin/main (compile rejects, exit 1) → GREEN after (48/48, exit 0); m3 honest-reject asserted. crates/synth-backend/tests/f32_hardfloat_619.rs locks the wiring in CI without unicorn. Frozen anchors 10/10, #511 estimator oracle, claim gate 17/17 all pass. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…369) (#705) * feat(fpu): GI-FPU-002 phase 1 — scalar f32 hard-float reachable on thumb-2 (#619, #369) The VFP encoder + selector arms existed but the decoder dropped every scalar float op, so `synth compile -t cortex-m4f` honest-rejected f32 on every CLI path. Worse, the "existing" VFP lowering was a non-functional prototype: select_with_stack fell through to select_default's blind %16 round-robin `alloc_vfp_reg`, so f32.const;f32.const;f32.add emitted VADD S2,S3,S4 over garbage. This wires the real bridge for the phase-1 honest subset. Delivered: - Decoder un-drops in-scope f32 ops (add/sub/mul/div, 6 compares, i32.trunc_f32_s/u, f32.convert_i32_s/u, f32.const); f64 + rest stay dropped. - Real VFP value stack in select_with_stack: StackVal::Float, S0..S15 allocator (no spilling — loud-bail on exhaustion), f32 op arms. Integer path untouched. - AAPCS-VFP: f32 params homed in S0..S15 (params_f32 threaded decoder → CompileConfig → selector), f32 result in S0. - FPU gate: m4f/m7/m7dp lower f32; m0/m3/r5 honest-reject with a clear message. - .ARM.attributes Tag_FP_arch=VFPv4-D16 + Tag_ABI_VFP_args on FPU targets; reset handler enables CP10/CP11 in SCB->CPACR (M4F FPU is off at reset). - Fix two latent encoder bugs surfaced by making float reachable: the signed/unsigned VCVT constants were swapped (convert_i32_s was unsigned), and the CPACR ORR mask encoded #0x07800000 instead of #0x00F00000. Held (honest-subset, chosen): f64 (phase 2), f32 load/store + local.set/tee (phase 1b), mixed f32/int param lists + f32-with-calls (loud-decline). Oracle: scripts/repro/f32_vfp_619_differential.py — unicorn (ARM/Thumb, FPU enabled) vs wasmtime, bit-exact on boundary values. RED on origin/main (compile rejects, exit 1) → GREEN after (48/48, exit 0); m3 honest-reject asserted. crates/synth-backend/tests/f32_hardfloat_619.rs locks the wiring in CI without unicorn. Frozen anchors 10/10, #511 estimator oracle, claim gate 17/17 all pass. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * test: map the SCS page in reset-path harnesses — GI-FPU-002 CPACR write (#619) FPU-target startup now writes SCB->CPACR (0xE000ED88) to enable CP10/CP11 (GI-FPU-002). The #649 i64-global-init + #687 stack-layout differentials replay the real reset path under unicorn and faulted UC_ERR_READ_UNMAPPED on that access — the System Control Space page was never mapped (real silicon has the register; the codegen is correct). Map 0xE000E000 (4 KB) in both harnesses. #649 + #687 + f32 differentials all green; frozen anchors 10/10. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

…mpare flag-clobber fix) (#716) * fix(f32): shipped thumb-2 f32 comparisons silently returned 0 (flag clobber) The v0.39.0 f32 hard-float compares (`f32.lt/gt/le/ge/eq/ne`) emitted a flag-setting `MOVS Rd,#0` AFTER `VMRS APSR_nzcv, FPSCR`, clobbering the N/Z/C/V flags the VMRS had just transferred from the VFP compare. The following `IT<cond>` then read stale flags, so every f32 comparison returned 0 on hardware (verified on Cortex-M4F: `flt(1.0,2.0)` -> 0). The bug shipped because the GI-FPU-002 (#619) differential deliberately skipped compare EXECUTION on a false premise — "unicorn does not model the VMRS FPSCR->APSR transfer." unicorn DOES transfer the flags; the skip is exactly what hid the defect. Fix: materialize the `#0` BEFORE the VCMP so its flag side-effect is overwritten by the VMRS (pure byte reorder — instruction sizes unchanged, so the estimator<->encoder agreement oracle #511 is untouched). Re-enable compare execution in the 619 differential (now 60/60 bit-exact vs wasmtime, incl. flt/fgt) and correct the false comment. Byte-pin test updated to the reordered layout (grounded in objdump). This is a prerequisite for #709: the trunc domain guard is built on these compares. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * feat(f32): #709 trunc-must-trap guard + #708 f32.load/reinterpret lowering #709 (SOUNDNESS): `i32.trunc_f32_s/u` lowered to a bare saturating VCVT (NaN->0, out-of-range->saturated) where WASM Core §4.3.3 mandates a TRAP. Emit a domain guard before the (now provably exact) VCVT: trunc_f32_s valid iff -2^31 <= x < 2^31 (bounds exact in f32) trunc_f32_u valid iff -1.0 < x < 2^32 The guard reuses the div-by-zero trap idiom (`Cmp; B<c> +0 skip; UDF`) driven by the ORDERED f32 compares (F32Lt=MI upper, F32Ge=GE / F32Gt=GT lower), each of which yields 0 on NaN — so NaN fails the in-range test and falls to the UDF. F32Lt/F32Gt are STRICT, so `x == 2^31` and `x == -1.0` correctly trap; `x == -2^31` is in-range (inclusive GE). Guarded in the shipping path (`try_lower_f32`) and, for soundness parity, the legacy `select_default` fallback (untested by the oracle — that path is not reached by `select_with_stack`). #708: un-drop `f32.load` and the `i32.reinterpret_f32` / `f32.reinterpret_i32` bit-casts at decode (falcon's #369 residual: 13 F32Load + 7 reinterpret skips). `f32.load` is lowered as the PROVEN i32.load address sequence (`generate_load_with_bounds_check`: the `[R11,idx]`->absolute-base rewrite plus optional bounds guard) into a core register, then a bit-exact `VMOV Sd,Rd` — a VLDR would load the identical 4 bytes (the encoder's `encode_vfp_ldst` silently drops the index register, so a direct `VLDR [R11,idx]` would MISS the dynamic index). Reinterprets are pure VMOV. `f32.store` stays dropped (falcon needs only load + reinterpret) — it loud-skips at decode, never a silent miscompile. Oracle: scripts/repro/f32_mem_trunc_708_709_differential.py — the exact #709 trap table (NaN/±Inf/out-of-range -> UDF; in-range bit-exact vs wasmtime) + f32.load/reinterpret/round-trip bit-exact. 48/48 GREEN on Cortex-M4F under unicorn; m3 honest-reject confirmed. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

avrabe merged commit 861d4c0 into main Jun 26, 2026
22 checks passed

avrabe deleted the vcr-oracle-498-estimator-encoder-agreement branch June 26, 2026 11:18

avrabe mentioned this pull request Jun 26, 2026

test(optimizer-bridge): delegate count_arm_byte_size to the production estimator (#511 follow-on, #242) #512

Merged

avrabe mentioned this pull request Jun 26, 2026

test(vcr-ra): reg_effect ↔ rewrite_op def/use consistency oracle (#242) #513

Merged

This was referenced Jun 26, 2026

fix(vcr-ra): const-CSE size-regression guard — CSE-last + per-segment size guard (#242) #519

Merged

Epic: reach and beat native codegen — proof-carrying specialization as the mechanism (VCR-*) #242

Open

This was referenced Jul 1, 2026

fix(#498): estimator↔encoder alignment — close 10 pure-estimator size gaps #555

Merged

feat(vcr-ra): Belady spill-plan re-choice — flat_flight frame traffic recovered (#242, VCR-RA-001) #576

Merged

avrabe mentioned this pull request Jul 3, 2026

feat(vcr-ra)!: retire inline const aliasing; SYNTH_CONST_CSE default-on (#242) #604

Merged

This was referenced Jul 3, 2026

docs(rivet): #494 proof-carrying design + VCR-SEL-001 first-increment scope (#242) #609

Merged

fix(selector): i64 rotl/rotr/div_u/rem_u compute real results — never silent 0 (#610) #613

Merged

This was referenced Jul 8, 2026

feat(rv32-promo): measured no-grow profitability for local promotion (#472, #601, epic #242) #626

Merged

feat(rv32-promo)!: SYNTH_RV_LOCAL_PROMO default-on — measured local promotion ships (#472, #601, epic #242) #627

Merged

avrabe mentioned this pull request Jul 8, 2026

fix(thumb2): i64.popcnt epilogue clobber + i64.div_s INT64_MIN/-1 overflow trap (#632, #633) #634

Merged

avrabe mentioned this pull request Jul 8, 2026

fix(codegen): call_indirect bounds guard + compile-time type check — OOB/wrong-type traps per WASM §4.4.8 (#642) #646

Merged

avrabe mentioned this pull request Jul 10, 2026

fix(encoder): T3 ADD.W raw-imm packing — ADDW (T4) for static offsets 0x100..0xFFF (#681) #690

Merged

avrabe mentioned this pull request Jul 10, 2026

feat(codegen): heterogeneous funcref tables — runtime type check via the type-id sidecar (#676) #696

Merged

avrabe mentioned this pull request Jul 10, 2026

GI-FPU-002 phase 1: scalar f32 hard-float reachable on thumb-2 (#619, #369) #705

Merged

avrabe mentioned this pull request Jul 11, 2026

feat(f32): #709 trunc-must-trap + #708 f32.load/reinterpret (+ f32-compare flag-clobber fix) #716

Merged

avrabe mentioned this pull request Jul 16, 2026

feat(#778): WCET phase 2 — statically-proven loop trip counts + the --wcet-hints sound-checker seam #793

Merged

Navigation Menu

Uh oh!

test(vcr-oracle): estimator↔encoder agreement oracle for the optimized path (#498, #242) - #511