fix(#973): ARM select on an i64-comparison returns the then-arm — and an ARM leg for the corpus CI never compiled by avrabe · Pull Request #992 · pulseengine/synth

avrabe · 2026-08-18T19:16:11Z

Closes #973. RQ-58-SELECT973, both halves.

1. The miscompile

select on an i64-comparison condition with computed arms returned the
then-arm on every vector where the else-arm was due.

Mechanism, re-derived here rather than taken from the issue (capstone over
the ELF .text, never synth disasm text):

add.w  r3, r0, #0x64   ; then-arm -> r3
add.w  r5, r1, #0xc8   ; else-arm -> r5, LIVE from here on
str.w  r3, [sp]        ; then-arm SPILLED: the i64 compare needs a PAIR
...                    ; cmp / sbcs — the 64-bit comparison
ldr.w  r5, [sp]        ; RELOADED INTO r5 — the live else-arm
movne  r6, r5
moveq  r6, r5          ; both `it` arms move the SAME register

pop_operand's reload allocates against the remaining vstack plus
reserved. A value the same op popped a moment ago is on neither list, so the
allocator was free to hand back the register the select still needed. The spill
is not the opt-in SYNTH_SPILL_ON_EXHAUST rung — alloc_consecutive_pair
spills the deepest register-resident entry unconditionally when no free pair
remains, which an i64 comparison's two sign-extended operands guarantee. Hence
the shape: i64 condition (creates the pressure) plus computed arms
(constant arms spill nothing).

Three things the issue did not have, all measured:

the self-contained/optimized leg emits a byte-identical body
(sha256 1bef7e18… on both legs) — one defect on two nominal paths, not two;
the wide (i64-arms) select is green pre-fix — it already reserved its
destination pair, which is the shape of the fix the narrow path needed. Its
val2-pair omission is closed here as the identical latent shape;
guard_same_arm shows the issue's suggested structural assertion ("a select's
two conditional moves must never have the same source") is not sound as
stated — select (local.get 0) (local.get 0) c legitimately moves one
register twice. The real invariant is the reservation, so that is what landed.

The fix generalizes the reservation discipline #677 already established for
bulk-memory ("every popped operand of the op") into pop_operand_committed, so
the next multi-pop site cannot forget it.

Red-first

scripts/repro/select_i64cmp_973_arm_differential.py, landed before the fix
(commit 07bceef):

	pre-fix	post-fix
relocatable	132/180	180/180
self-contained	132/180	180/180
total	264/360	360/360

96 wrong vectors, every one returning the then-arm:

BUG sel_i64_lt_s(7,5):     want=205 got=107
BUG sel_i64_lt_s(0,0):     want=200 got=100
BUG sel_i64_lt_s(100,100): want=300 got=200
BUG sel_i64_eq(-1,1):      want=201 got=99
ok  cmp_i64_lt_s(...)  12/12   <- the comparison ALONE was always correct

Plus four allocator unit tests, including a red one that reproduces the
hazard directly (pop_operand_red_973_reload_lands_on_the_live_operand: with
the reservation the old code passed, the reload takes R5 while the op still
needs it).

Bytes

10/10 frozen anchors UNCHANGED — no re-freeze was needed and none was done.
The reservation can only change an allocation the old code would have answered
with a committed register, which is the miscompile. Where bytes do move they
get smaller and correct: sel_i64_lt_s 68 B → 64 B, because with
val1 != val2 restored the #209 in-place select applies and one conditional
move disappears.

2. The CI gap — the larger half

#973 surfaced only because someone compiled the repro corpus for ARM by hand.
CI never did. The repro-sweep-* jobs run hand-listed oracles each pinned to
one fixture; a fixture written for RV32 or aarch64 never reached the ARM backend.
rv32_cmp_select_472.wat has carried this exact shape as sel_cmp_i64 since
v0.11 and no ARM build ever saw it.

New job repro-sweep-arm-corpus-oracle runs
scripts/repro/arm_corpus_sweep_973.py:

Phase A — compile census over all 156 fixtures: 144 compile, 12 decline,
0 hard errors. The 12 are loud #952 declines listed by name and reason,
ratcheted both ways (an undeclared failure is red; a listed fixture that
starts compiling is red too).
Phase B — execution differential vs wasmtime: 43 modules, 2327 compared
vectors, 2335 emulator entries.

The leg is red-first against its own defect. Run against the pre-fix binary
it reports 7 wrong vectors for rv32_cmp_select_472.wat:sel_cmp_i64 — the
fixture already in the tree — and 55 across the #973 shapes overall.

Floors are measured through the real CI path (oracle_run.py --report-only),
not guessed: emulations >= 360 and emulations >= 2335, both exact. The sweep
carries a second floor the driver cannot express (MIN_COMPARED = 2327),
because emulations counts emulator entries and a run that discarded every
result on budget grounds would still clear it.

3. What the leg newly surfaced — 48 vectors, two classes, both filed

Reported, not narrowed away. Identical on binaries built before and after the
#973 fix, and both proven from the emitted bytes.

#989 — a local.set/local.tee clobbers a live local.get of the same
local (44 vectors, 4 exports). war_set returns 200 for every input:

mov   r0, r0      ; x lives in r0
movw  r1, #0x64
mov   r0, r1      ; local.set x = 100 — overwrites the pushed OLD x
adds  r2, r0, r0  ; 100 + 100

get_set_get_param_no_alias never reads its argument at all. RV32 has the
protection (snapshot_aliases) and its own fixture comment predicts this exact
number; ARM has no equivalent.

#990 — a local written on only one arm of a br_if is never zero-initialised
(3 vectors), reading uninitialised stack. Provable rather than inferred: the
returned values are the harness's 0xDEADBEEF poison ±1, the two select
arms at the merge. #970 closed the parameter half of this class; this is the
local-on-a-br_if half — same information-disclosure shape.

Both are in KNOWN_ARM_MISMATCHES against their issue number, suppressed not
skipped (so listing debt cannot buy slack in the comparison floor) and
ratcheted in both directions — an entry that stops mismatching must be deleted,
which is how each fix will record itself.

A third finding, negative: VCR-RA-003's four invariants (callee-saved,
spill-slot aliasing, caller-saved across calls, availability across joins) do not
cover intra-operation operand liveness, which is why the whole-function
allocation validator was silent on #973. Named, not fixed here.

4. Honest gaps

91 of 144 compiled modules are excluded from Phase B for declaring a
memory/table/global/data/elem/import section. Their images are
repro-sweep-memory-oracle's job; a differential that reported its own setup
gaps as miscompiles would train people to ignore it.
37 vectors trap under wasmtime, 36 exceed a budget — all counted and printed.
The reservation class beyond select was probed, not proven absent: six
adversarial binop shapes (one of which genuinely spills and reloads) matched
wasmtime 72/72. pop_operand_committed exists so the next site can adopt it
cheaply.

Gates

cargo test --workspace, cargo clippy --workspace --all-targets -D warnings,
cargo fmt --check, python3 scripts/claim_check.py claims.yaml (43/43),
oracle_wiring_check.py --min-emulation-floor 298754 — each run without a pipe.

Ledger moved with the docs per the #910 ritual: ORACLE_WIRING.md 144→146 oracles
and 296,059→298,754 entries, feature_matrix.md.tmpl, claims.yaml (verbatim
texts and the emulations count-min), ci.yml's --min-emulation-floor.
Two pre-existing drifts in that same table were corrected: the stdout floor read
458 against a measured 460, and the doc's --min-emulation-floor 295621
disagreed with ci.yml's 295726.

No [Unreleased] edit, no version bump, no status.json regeneration.
docs/status/FEATURE_MATRIX.md is regenerated because the claim-check gate
requires it when the template changes (one line).

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

… the WEEKLY API limit Committed by the hub coordinator so the work survives. NOT reviewed and NOT complete: the lane stopped mid-task. This is a restore point, not a claim that anything is verified. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

…-973

…4/360) The fixture + unicorn-vs-wasmtime differential for RQ-58-SELECT973, landed BEFORE the fix so the red is on the record. Measured on 60ab227 (pre-fix), `--target cortex-m4`, BOTH ARM lowering legs: [relocatable] 132/180 vectors match wasmtime [self-contained] 132/180 vectors match wasmtime #973 CHECKS=264/360 96 wrong vectors, and every one returns the THEN-arm where the else-arm was due: BUG sel_i64_lt_s(7,5): want=205 got=107 BUG sel_i64_lt_s(0,0): want=200 got=100 BUG sel_i64_lt_s(100,100): want=300 got=200 BUG sel_i64_eq(-1,1): want=201 got=99 MECHANISM RE-DERIVED HERE, not taken from the issue (capstone over the ELF .text, never `synth disasm` text): add.w r5, r1, #0xc8 ; else-arm -> r5, LIVE str.w r3, [sp] ; then-arm SPILLED to free an i64 pair ... ; the 64-bit compare ldr.w r5, [sp] ; RELOADED INTO r5 == the live else-arm movne r6, r5 moveq r6, r5 ; both `it` arms move the SAME register The spill is NOT the opt-in SYNTH_SPILL_ON_EXHAUST rung — `alloc_consecutive_pair` spills the deepest register-resident vstack entry unconditionally when no free consecutive pair remains, which the i64 comparison's two sign-extended pairs guarantee. `pop_operand`'s reload then allocates against the REMAINING vstack plus `live_params`; a value already popped for this same op is on neither list, so the allocator is free to hand out exactly the register the select still needs. Two facts the issue did not have: * the SELF-CONTAINED (optimized) leg emits a BYTE-IDENTICAL body (sha256 1bef7e189ae8e090 both legs) — the i64 ops delegate this shape to `select_with_stack`, so this is one defect on two nominal paths, not two. * `sel_wide_i64cmp` (i64 ARMS under an i64 comparison) is GREEN pre-fix: the wide path already reserves its destination pair across the pops, which is the shape of the fix the narrow path needs. Guards are in the fixture for the two NON-signatures: `guard_const_arms` (constant arms spill nothing, so the bug is invisible) and `guard_same_arm` (two conditional moves reading one register is CORRECT when both arms are the same value — so "same source" is not by itself the defect).

…loading pop RQ-58-SELECT973. `select` on an i64-comparison condition with COMPUTED arms returned the then-arm on every vector where the else-arm was due. MECHANISM (verified by execution and by the emitted bytes, not taken from the issue). `pop_operand`'s reload allocates against the REMAINING vstack plus `reserved`. A value the SAME op popped a moment ago is on neither list — it left the vstack when it was popped, and the caller has to thread it through by hand. The narrow `Select` arm passed only `live_params`, so the reload was free to hand back the register the select still needed: add.w r5, r1, #0xc8 ; else-arm -> r5, LIVE str.w r3, [sp] ; then-arm spilled: the i64 compare needs a PAIR ldr.w r5, [sp] ; reloaded INTO the live else-arm movne r6, r5 moveq r6, r5 ; both `it` arms move the same register The spill is NOT the opt-in SYNTH_SPILL_ON_EXHAUST rung — `alloc_consecutive_pair` spills the deepest register-resident entry unconditionally when no free pair remains, which an i64 comparison's two sign-extended operands guarantee. That is why the bug needs an i64 CONDITION and COMPUTED arms: constant arms spill nothing. THE FIX is the reservation discipline #677 already established for bulk-memory ("every popped operand of the op"), generalized into `pop_operand_committed` so the next multi-pop site cannot forget it: the condition register is committed across both pops, and `val2` across the second. The wide (i64-arms) path gets the same treatment for `val2`'s PAIR — that path measured GREEN pre-fix because it already reserved its destination pair, so this is the identical latent shape closed rather than a second live bug. BYTES. The reservation can only change an allocation the OLD code would have answered with a committed register — which is the miscompile — so everything else is byte-identical: * 10/10 frozen anchors UNCHANGED (`cargo test -p synth-cli --test frozen_codegen_bytes`), control_step and flight_algo included. No re-freeze was needed and none was done. * full `cargo test --workspace` green (142 test binaries), clippy -D warnings clean. Where bytes DO move, they move to correct AND smaller code — `sel_i64_lt_s` 68 B -> 64 B, because with `val1 != val2` restored the #209 in-place select applies and one conditional move disappears: ldr.w r6, [sp] ; reload lands clear of the live else-arm cmp r4, #0 it ne movne r5, r6 ; single in-place move; r5 already holds the else-arm EXECUTION EVIDENCE. `scripts/repro/select_i64cmp_973_arm_differential.py` 264/360 -> 360/360 against wasmtime, on BOTH ARM lowering legs (relocatable and self-contained, whose bodies are byte-identical here). The defensive `Err` in `pop_operand_committed` is a TRIPWIRE for future edits, not a live path: with the reservation in place it is unreachable by construction. It is unit-tested directly rather than left as untested prose.

…ith floors The second half of RQ-58-SELECT973, and the larger half. #973 was found only because a lane compiled `scripts/repro/*.wat` for ARM BY HAND. Nothing in CI did that: the `repro-sweep-*` jobs run hand-listed oracles, each pinned to the one fixture its issue was about, so a fixture written for RV32 or aarch64 never reached the ARM backend even when its shape is backend-independent. `rv32_cmp_select_472.wat` has carried the #973 shape as `sel_cmp_i64` since v0.11 and no ARM build ever saw it. RED-FIRST FOR THE GATE ITSELF, not only for the fix. Run against the PRE-fix binary, this sweep reports 7 wrong vectors for `rv32_cmp_select_472.wat:sel_cmp_i64` — the already-in-tree fixture — and 55 across the #973 shapes in total. Post-fix those are gone. The leg would have caught the defect it was built for, with no new fixture required. TWO PHASES, because compiling alone would not have caught #973 (it compiled perfectly and returned the wrong number): A. COMPILE CENSUS over all 156 fixtures at `--target cortex-m4f --relocatable --all-exports`. Measured 144 compile / 12 decline / 0 hard error. The 12 are LOUD `#952` declines listed by name and reason, ratcheted BOTH ways: an undeclared failure is red, and a listed fixture that starts compiling is red too ("remove the entry"), so the list cannot rot into a permanent excuse. B. EXECUTION DIFFERENTIAL vs wasmtime over every all-i32 export of every module pure enough to emulate faithfully. Measured 43 modules, 2327 compared vectors, 2335 emulator entries. WHAT IT SURFACED — 48 pre-existing wrong vectors that have nothing to do with #973, identical on binaries built before and after the fix. Reported, not narrowed away, and both classes proven from the emitted bytes: * #989 — a `local.set`/`local.tee` clobbers an earlier `local.get` of the SAME local still on the operand stack. `war_set` returns 200 for EVERY input (`mov r0,r0; movw r1,#0x64; mov r0,r1; adds r2,r0,r0`); `get_set_get_param_no_alias` never reads its argument at all. RV32 has the protection (`snapshot_aliases`) and its own fixture comment predicts this miscompile; ARM has no equivalent. 44 vectors, 4 exports. * #990 — a local written on only ONE arm of a `br_if` is never zero-inited, so the merge reads uninitialised stack (`bne` jumps past the only `str.w`, then `ldr.w` reads the slot). Provable rather than inferred: the returned values are this harness's 0xDEADBEEF poison plus/minus one, the two `select` arms at the merge. #970 closed the parameter half of this class; this is the local-on-a-br_if half. 3 vectors, information-disclosure shape. They are listed in `KNOWN_ARM_MISMATCHES` against their issue number, ratcheted in both directions — an entry that stops mismatching must be deleted, which is how each fix will record itself — and SUPPRESSED rather than skipped, so listing debt cannot buy slack in the comparison floor. FLOORS ARE MEASURED, NOT GUESSED (this hub found existing floors at half their real value). Both scripts were calibrated through the real CI invocation path, `scripts/oracle_run.py --report-only`: select_i64cmp_973_arm_differential.py emulations = 360 (floor 360) arm_corpus_sweep_973.py emulations = 2335 (floor 2335) The sweep carries a SECOND floor the driver cannot express: `emulations` counts emulator ENTRIES, and a run that entered the emulator and then discarded every result on budget grounds would still clear it. `MIN_COMPARED = 2327` is the floor on vectors actually compared against wasmtime. HONEST GAPS, all counted and printed rather than assumed away: 91 modules are excluded from phase B for declaring a memory/table/global/data/elem/import section (their images are `repro-sweep-memory-oracle`'s job — a differential that reported its own setup gaps as miscompiles would train people to ignore it); 37 vectors trap under wasmtime; 36 exceed a budget. Both engines get one — wasmtime runs on FUEL, unicorn on an instruction count — because `aarch64_ctrlflow_851.wat:countdown(-1)` is a 2^32-iteration loop that costs 1.4 s per vector in the interpreter, and a leg that takes an hour gets deleted. Ledger moved with the docs, as the #910 ritual requires: ORACLE_WIRING.md 144 -> 146 oracles and 296,059 -> 298,754 entries, feature_matrix.md.tmpl, claims.yaml (both the verbatim texts and the emulations count-min), and ci.yml's `--min-emulation-floor`. Also corrected two pre-existing drifts found in the same table: the stdout floor total read 458 against a measured 460, and the doc's `--min-emulation-floor 295621` disagreed with ci.yml's 295726. claim_check 43/43.

avrabe · 2026-08-18T19:18:25Z

Follow-up: the `guard_same_arm` claim, measured

The PR body argues the issue's suggested structural assertion — "a select's two
conditional moves must never have the same source" — is not sound as stated.
That was code reading; here it is from the bytes (capstone over the ELF .text),
guard_same_arm(a, b) = select(a, a, (i64)a < (i64)b) at --target cortex-m4 --relocatable:

03c0: cmp     r6, #0
03c2: it      ne
03c4: movne   r7, r0
03c6: it      eq
03c8: moveq   r7, r0     <- SAME source register, and CORRECT
03ca: mov     r0, r7

Both it arms read r0 because both wasm arms are local.get 0. The function
returns a for every input and matches wasmtime 12/12 in the differential. The
proposed assertion would have false-fired on correct code, so the invariant that
landed is the reservation (pop_operand_committed) rather than a same-source
check on the emitted moves.

temper-pulseengine · 2026-08-18T19:21:12Z

Automated review for PR #992

pulseengine/synth:fix/arm-select-i64cmp-973 → pulseengine/synth:main

Verdict: 💬 Comment

Summary: The commit message does not clearly explain why the number of assertions has increased from 144 to 146. It is also unclear what changes were made to the code that caused this increase.

Findings: 0 mechanical (rivet) · 1 from local AI model.

Findings (1):

docs/status/FEATURE_MATRIX.md:150

see [coq/STATUS.md](../../coq/STATUS.md) for the per-file matrix.
the newly wired ones; exactly 8 asserted a printed verdict or count. Every
`wired` oracle now declares a `# ci-checks:` floor that
`scripts/oracle_run.py` enforces per run by counting real emulator entries,

wasmtime executions and compilations: **144 oracles assert 296,059 emulator
```
The number of assertions has increased from 144 to 146.
```

Generated by a local AI model and post-validated against a strict JSON contract. Each finding includes the verbatim line being criticised — verify by reading the file at the cited location.

Reviewed at 0119ba3

…me itself Pre-emptive fix for the class this job would otherwise have discovered the hard way. The ARM corpus sweep shelled out to `wat2wasm --enable-all`, which makes the EXECUTED POPULATION depend on the runner's wabt build: several fixtures use post-MVP proposals (multi-memory, bulk-memory), and a wabt that rejects the flag or a proposal would have refused every fixture, collapsed the comparison count, and reported it as a coverage failure rather than as the toolchain problem it is. That is the #850/#881 host-dependency class, and a never-before-run job is exactly where it hides — this repo's own #890 job comments say so verbatim. `wasmtime.wat2wasm` is the SAME library that then instantiates the module, so what parses and what runs cannot disagree, and there is no apt package in the path at all (the step is gone; the #973 differential never used wat2wasm either, it loads the `.wat` through `Module.from_file`). MEASURED EQUIVALENT, not assumed: across all 156 fixtures wabt and wasmtime accept exactly the same set (0 refusals each), and the section-id purity classification is identical for every one of them. The sweep's numbers are unchanged — compiled 144/156, 2327 compared vectors, emulations 2335, so no floor moved. Also: a mass reference-refusal now names ITSELF. Without it, a host whose assembler cannot read the corpus reds on the comparison floor, which reads as "the sweep lost coverage" and sends the next reader to the compiler. Fail-closed either way; the difference is the diagnostic. Gates re-run after the change, each without a pipe: sweep PASS (floor 2335, measured 2335), #973 differential 360/360 (floor 360, measured 360), oracle_wiring_check --min-emulation-floor 298754 rc=0, claim_check 43/43.

Both found by re-reading the checkers rather than the checked code — v0.57's lesson was that 5 of its 10 defects lived in instruments. 1. The #973 differential did not assert that the emulation REACHED the return pad. The instruction budget is ~500x what these straight-line functions need, so it cannot be hit today; the point is that if it ever were, `run()` would return whatever R0 happened to hold and the vector could COMPARE EQUAL by accident. A differential that passes on a value it never finished computing is precisely the shape being guarded against elsewhere in this lane. The corpus sweep already checked PC; now both do. 2. The sweep leaked its temp dir (`mkdtemp` with no cleanup). Re-verified after the change, each without a pipe: differential 360/360 (floor 360, measured 360), sweep PASS with compiled 144/156 and 2327 compared vectors (floor 2335 emulations, measured 2335). No number moved.

avrabe · 2026-08-18T19:31:00Z

Runner reconciliation: ubuntu-latest matches macOS exactly

The floors in this PR sit at the measured value with no headroom, and this
job had never run on a Linux runner — so the numbers were verified there rather
than assumed. Run
32175663442,
job repro sweep — ARM corpus, conclusion success (and the run as a whole
green across all 53 jobs):

#973 CHECKS=360/360
ORACLE-EVIDENCE script=select_i64cmp_973_arm_differential.py
  mode=emulations floor=360 measured=360 emulations=360 wasmtime_calls=360 compiles=2

  modules executed=43  vectors=2327  mismatches=48  faults=0
  skipped: impure-module=91, unrunnable-object=0, reference-refused=0,
           wasm-trap-vectors=37, over-budget-vectors=36
#973 ARM CORPUS compiled=144/156 executed=2279/2327
ORACLE-EVIDENCE script=arm_corpus_sweep_973.py
  mode=emulations floor=2335 measured=2335 emulations=2335 wasmtime_calls=2400 compiles=156

Every counter is identical to the local measurement — compiled 144/156, 43
modules, 2327 compared vectors, 48 (all listed) mismatches, and the three skip
classes 91 / 37 / 36. Nothing to reconcile: the zero-headroom floors are
empirically justified rather than optimistic.

Two later commits tightened the harnesses after that run — the reference
assembler moved from wabt to wasmtime.wat2wasm (removing a host dependency the
executed population would otherwise have ridden on) and the #973 differential
now asserts the emulation reached its return pad. The ARM corpus job is green on
the assembler change too
(job 95838691346);
the run for the final HEAD is in flight.

codecov · 2026-08-18T19:40:26Z

Codecov Report

❌ Patch coverage is 86.66667% with 16 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-synthesis/src/instruction_selector.rs	86.66%	16 Missing ⚠️

📢 Thoughts on this report? Let us know!

… defeated gates Conflict resolution (claims.yaml, scripts/claim_check.py): union of the two lanes — main's RQ-58-METRIC ratchet engine + this branch's RQ-58-MIRRORS fields (the retired aarch64_selector_ops derivation stays deleted; the branch-only fields-equal evidence kind is ported into main's _check_evidence dispatcher). Two gates were silently defeated on main and are re-armed here: 1. MC/DC rustc pin (#984): dependabot bumped dtolnay/rust-toolchain 1.96.1 -> 1.100.0 — for that action the ref IS the compiler, so the MC/DC job's deliberate measurement pin was changed with no re-measure of the floors. Restored to 1.96.1 and excluded from dependabot with the reason in both files. 2. Subtraction ratchet stale-base cross (#991 x #992): #992 merged 19:50 adding 102 code-region selector lines and one _ => None helper arm; #991 pinned the ratchet values at 20:07 from a base that predated it, so main itself derives 18582/29839/63/106 against a ledger saying 18480/29616/62/105 and is red on its own queued push CI. This PR is the first to carry the union; the pins move here with waivers attributing the growth to #992's #973 miscompile fix, not to this lane. mirror_marker_files 57 -> 58 is waived as the surviving single count_params copy's own RQ-58-MIRRORS retirement-provenance comment — the heuristic's documented prose over-count, not a new mirror. status.json + FEATURE_MATRIX.md regenerated via --emit-status; 49/49 claims hold on the merged tree. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

…DSL rules replaced (-1,312 lines, byte-identical) (#999) * retire(#242): i32.add — delete the hand-written select_default arm The Rocq-proved rule_i32_add is the shipped lowering since the default-on flip; the superseded arm is deleted. Byte-identity: 688-row corpus manifest (156 fixtures x 4 configs incl. declines) identical to origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i32.sub — delete the hand-written select_default arm Same evidence as i32.add: 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i32.mul — delete the hand-written select_default arm 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i32.and — delete the hand-written select_default arm 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i32.or — delete the hand-written select_default arm 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i32.xor — delete the hand-written select_default arm 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i32.shl — delete the hand-written select_default arm The Rocq-proved rule carries the #682 mod-32 R12 mask. 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i32.shr_s — delete the hand-written select_default arm 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i32.shr_u — delete the hand-written select_default arm 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i32.rotl — delete the hand-written select_default arm 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i32.rotr — delete the hand-written select_default arm 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i32.clz — delete the hand-written select_default arm 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i32.ctz — delete the hand-written select_default arm 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i32.popcnt — delete the hand-written select_default arm 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i64.add — delete both hand-written arms (default + direct) One op, both selectors: the select_default fixed-pair arm and the select_with_stack allocated-pair arm each collapse to the Rocq-proved rule_i64_add call that has been the shipped path since the flip. 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i64.sub — delete both hand-written arms (default + direct) 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i64.and — delete the hand-written select_default arm 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i64.or — delete the hand-written select_default arm 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i64.xor — delete the hand-written select_default arm 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i64.{or,and,xor} — delete the hand-written direct-selector arm One grouped select_with_stack arm serves the three i64 bitwise ops via the shared i64_pair_rule dispatch, so the deletion unit is the group (its select_default counterparts were retired per-op in the three previous commits). Also removes the group's '_ => unreachable!()' wildcard arm. 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i64.eqz — delete both hand-written arms (default + direct) 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i64 comparisons x10 — delete the hand-written select_default arm One grouped arm serves the ten binary i64 comparisons via the shared i64_setcond_rule dispatch, so the deletion unit is the group. Also removes the group's '_ => unreachable!()' condition-map wildcard arm. 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i64.{shl,shr_u,shr_s} — delete the hand-written direct-selector arm One grouped select_with_stack arm serves the three i64 variable shifts via the shared i64_pair_bin_rule dispatch; the deletion unit is the group. Also removes the group's '_ => unreachable!()' wildcard arm. 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i32 comparisons x10 — retire the flag conditioning on the direct selector PARTIAL by design, and named as residual: this grouped arm is dual-use. The reg-reg case now takes the Rocq-proved i32_cmp_rule unconditionally; the #258 cmp/cmn imm-fold case has no DSL rule (no CmpImm-shaped rule exists), so its hand-written Cmp+SetCond fallback emission STAYS and is enumerated in the RQ-58-SPLIT residual set rather than deleted. 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i32.eqz — delete the hand-written direct-selector arm 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i32.{shl,shr_s,shr_u,rotr} — delete the hand-written direct-selector arm One grouped select_with_stack arm serves the four register shifts/rotates via the shared i32_shift_rule dispatch; the deletion unit is the group. The generated rules carry the #682 mod-32 R12 mask themselves. Also removes the group's '_ => unreachable!()' wildcard arm. 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i32.clz — delete the hand-written direct-selector arm 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i32.ctz — delete the hand-written direct-selector arm 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i32.popcnt — delete the hand-written direct-selector arm 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i64 comparisons x10 — delete the hand-written direct-selector arm One grouped select_with_stack arm serves the ten binary i64 comparisons via the shared i64_setcond_rule dispatch; the deletion unit is the group. Also removes the group's '_ => unreachable!()' condition-map wildcard arm. 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i64.mul — delete the hand-written direct-selector arm 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i64.{rotl,rotr} — delete the hand-written direct-selector arm One grouped select_with_stack arm serves both rotates via the shared i64_rot_rule dispatch; the deletion unit is the group. Also removes the group's '_ => unreachable!()' wildcard arm. 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): i64.{clz,ctz,popcnt} — delete the hand-written direct-selector arm One grouped select_with_stack arm serves the three i64 bit-counts via the shared i64_unary_count_rule dispatch; the deletion unit is the group. Also removes the group's '_ => unreachable!()' wildcard arm. 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * retire(#242): the SYNTH_SEL_DSL lever itself + the now-vacuous mirror-pin gates With every superseded arm deleted there is no second implementation for the flag to select: the sel_dsl field, sel_dsl_from_env (SYNTH_SEL_DSL / SYNTH_NO_SEL_DSL), and set_sel_dsl are dead code and go. The four mirror-pin tests (sd + sws + i64-pair + defaults-on) compared the two paths byte-for-byte; with one path left they are vacuous — retired on the same grounds as the VcrSelRulesGenCheck reflexivity gate (see coq/STATUS.md). The #258 imm-fold holdout test is REWRITTEN, not deleted: the residual hand-written Cmp/Cmn+SetCond emission it pins survived the retirement (cmp_imm_fold_residual_path_stays_handwritten_258). The RULES table — including its Delegation wiring metadata that the Rocq generation and the manifest gates consume — is untouched. Byte-identity: 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green; synth-synthesis suite 732+ green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * docs+ledger(#242): re-bank the subtraction ratchet for RQ-58-RETIRE claims.yaml: selector_lines_code 18582 -> 17897 (banked), wildcard_arms_code 63 -> 56 (banked), totals tracked 29839 -> 28495 / 106 -> 91; the two former #992 waivers deleted with the re-bank (a waiver above the new baseline is a standing licence to grow back). status.json regenerated via --emit-status. CLAUDE.md / coq/STATUS.md / verified-codegen-roadmap.yaml no longer claim the SYNTH_NO_SEL_DSL opt-out exists; rivet RQ-58-RETIRE -> implemented with evidence + the measured residual set. claim_check 49/49. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

… can run (#1001) #1000, from a toolchain-wide CLI survey: `synth verify` exists in the tree and in `--help`, fails closed with an exemplary message — and is in NO artifact a user can obtain. Reproduced by the reporter on the layer build (0.55.0) AND the current release (0.57.0), whose four platform tarballs all lack the feature. THE ISSUE'S OWN ESCAPE HATCH IS DEAD, AND I MEASURED IT RATHER THAN ASSUMING. #1000 offers: "or, if the Z3 dependency makes that undesirable for the default artifact, publish a variant". There is no Z3 dependency: cargo tree -p synth-cli --features verify -> 0 z3 nodes cargo tree -p synth-cli --features verify,…/z3-solver -> 2 z3 nodes `verify = ["synth-verify"]` and nothing more. `z3-solver = ["z3"]` is a separate opt-in with `optional = true`, and even enabled it links the SYSTEM libz3 rather than bundling it (#553). Ordeal (pure Rust QF_BV) has been the default engine since v0.27.0. Shipping `--features verify` costs no Z3, no libz3, no C++ toolchain — so this is a release-workflow change, not a trade-off. README.md:98 IS THE OTHER HALF OF THE FINDING, and it is corrected here. It said the CLI `verify` feature "currently also enables the feature-gated Z3 differential oracle (statically linked)". False since v0.27.0 — and it is exactly the sentence that would make a maintainer accept #1000's escape hatch and NOT ship the feature. Prose that was true once, quietly stopped being, and stayed load-bearing on a release decision: the class the v0.57 cold review kept turning up, found again by a user asking a good question about a stale premise. Artifact scope, three parts, with the middle one carrying the weight: 1. build the released binaries (four tarballs + npm) with `--features verify` 2. a NON-VACUITY GATE — a released-artifact smoke test that actually RUNS `synth verify` on a freshly compiled module and asserts a VERDICT, not the capability-missing error. Red-first against a binary built without the feature. Without this, "we shipped the feature" regresses silently to "we shipped the help text", which is the class this whole release closes. 3. move the capability check AHEAD of the banner — today the four `Translation validation:` lines including `Strategy: Per-rule SMT verification (ASIL D path)` print BEFORE the tool discovers it cannot verify, so a log-scraper finds the ASIL-D line in a run that verified nothing. Exit code is already correct. Out of scope, named not dropped: #1000's `synthesize`-vs-`compile` description overlap, `--format json`, help-line width. Also re-graded RQ-58-MIRRORS (#993) and RQ-58-SELECT973 (#992) proposed -> implemented; both merged and the ledger had not caught up. rivet: 50 errors before AND after (unchanged); warnings +2, the standard pair every artifact carries. claim_check 49/49. Refs #1000, #242 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

…11/11, version pin sweep All 11 RQ-58-* artifacts are implemented and merged, so the release-readiness query over artifacts/release-v0.58.yaml is satisfied. Every number in the CHANGELOG was re-derived from MERGED CODE at this commit, not from PR bodies (v0.57's cold review found 4 factual errors in release prose written the same way): DSL rules 50 -> 74 (coq/vcr_sel_rules.manifest, tag vs HEAD) 1:1 Qed theorems 50 -> 74 (VcrSelRules.v) Rocq Qed (suite) 592 -> 617 (2 Admitted, 2 admit.) selector code 18,480 -> 17,961 selector wildcards 62 -> 55 selector total 29,616 -> 28,582 TWO CORRECTIONS the cold review caught in my own draft: 1. The v0.57.0 code-region baseline is 18,480 / 62 wildcards, NOT 18,582 / 63. The latter pair is the METRIC pin's CREATION value — measured mid-v0.58 after #992 grew the file — not the v0.57.0 release value. Re-measured at the tag with the ratchet's own marker ('#[cfg(test)]\nmod tests', asserted unique) so the release-over-release delta is like-for-like. 2. The SPLIT bullet originally read 'the root file went 29,616 -> 18,284', which is true release-over-release but credits SPLIT with a drop that RETIRE (-1,312) and SELDSL (-79) partly produced. Corrected to SPLIT's own effect: 10,298 lines moved out, 28,533 -> 18,284. Locally-true sentence, wrong attribution — the same shape as all four v0.57 errors. Version pin sweep across all four surfaces + Cargo.lock: check_version_pins.py exits 0 at 0.58.0. claim_check 49/49, model_coverage_audit --check ok, fmt clean. Refs #242.

…11/11, version pin sweep (#1010) All 11 RQ-58-* artifacts are implemented and merged, so the release-readiness query over artifacts/release-v0.58.yaml is satisfied. Every number in the CHANGELOG was re-derived from MERGED CODE at this commit, not from PR bodies (v0.57's cold review found 4 factual errors in release prose written the same way): DSL rules 50 -> 74 (coq/vcr_sel_rules.manifest, tag vs HEAD) 1:1 Qed theorems 50 -> 74 (VcrSelRules.v) Rocq Qed (suite) 592 -> 617 (2 Admitted, 2 admit.) selector code 18,480 -> 17,961 selector wildcards 62 -> 55 selector total 29,616 -> 28,582 TWO CORRECTIONS the cold review caught in my own draft: 1. The v0.57.0 code-region baseline is 18,480 / 62 wildcards, NOT 18,582 / 63. The latter pair is the METRIC pin's CREATION value — measured mid-v0.58 after #992 grew the file — not the v0.57.0 release value. Re-measured at the tag with the ratchet's own marker ('#[cfg(test)]\nmod tests', asserted unique) so the release-over-release delta is like-for-like. 2. The SPLIT bullet originally read 'the root file went 29,616 -> 18,284', which is true release-over-release but credits SPLIT with a drop that RETIRE (-1,312) and SELDSL (-79) partly produced. Corrected to SPLIT's own effect: 10,298 lines moved out, 28,533 -> 18,284. Locally-true sentence, wrong attribution — the same shape as all four v0.57 errors. Version pin sweep across all four surfaces + Cargo.lock: check_version_pins.py exits 0 at 0.58.0. claim_check 49/49, model_coverage_audit --check ok, fmt clean. Refs #242.

…ery compile path — the decoder had no StartSection arm at all The section fell through the catch-all and was discarded outright: all three backends compiled a (start)-carrying module, exited 0, printed no warning, and the start function was not even in the object. wasmtime runs it at instantiation (WASM Core §4.5.5) and returns 42 on the repro; synth-compiled code read never-initialized memory and returned 0. - wasm_decoder: Payload::StartSection arm + DecodedModule.start_function - main.rs: refuse_dropped_start_function at all three compile decode sites (module path, single-function path, WAST merge path) — non-zero exit + a reason naming the start section, the #851/#1041 refusal shape - deliberately NO escape hatch: the start function's code is not in the artifact, so no embedder contract can honor it (unlike #1041's --embedder-data-init, where the embedder holds the bytes) - start-function INVOCATION is a capability follow-on, not this fix 0 fixtures/harnesses affected (no .wat/.wast/.wasm in the repo carries a start section — swept textually AND by binary section id); emitted bytes for start-free modules are unchanged (guard only fires on Some), frozen anchors untouched; EXPECTED_DECLINES (#992) unchanged (keys on scripts/repro/*.wat, none of which carry (start)). Red-first: the 7 refusal tests in start_section_refusal_1046.rs failed on the parent commit and pass now; the start-free control passes throughout. Gates: fmt, clippy -D warnings, cargo test --workspace (true exit 0), claim_check 50/50, model_coverage_audit ok, rivet validate 50 errors (= main baseline, #1012). Refs #1046 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

… by ALL THREE backends — decode it and refuse loudly; fourth silent drop (globals inits, #1052) found and filed (#1053) * test(#1046): RED-FIRST — every backend must refuse a (start ...) module, asserted as a loud refusal naming the start section All 7 refusal cases FAIL on current main (exit 0, no warning, start function absent from the object); the start-free control passes. The assertions deliberately name the refusal (non-zero exit + reason string containing 'start function' and '#1046'), NOT the absence of invocation — which was already true on the broken behaviour and is exactly why the bug survived every existing test. Refs #1046 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * fix(#1046): decode the (start ...) section and REFUSE it loudly on every compile path — the decoder had no StartSection arm at all The section fell through the catch-all and was discarded outright: all three backends compiled a (start)-carrying module, exited 0, printed no warning, and the start function was not even in the object. wasmtime runs it at instantiation (WASM Core §4.5.5) and returns 42 on the repro; synth-compiled code read never-initialized memory and returned 0. - wasm_decoder: Payload::StartSection arm + DecodedModule.start_function - main.rs: refuse_dropped_start_function at all three compile decode sites (module path, single-function path, WAST merge path) — non-zero exit + a reason naming the start section, the #851/#1041 refusal shape - deliberately NO escape hatch: the start function's code is not in the artifact, so no embedder contract can honor it (unlike #1041's --embedder-data-init, where the embedder holds the bytes) - start-function INVOCATION is a capability follow-on, not this fix 0 fixtures/harnesses affected (no .wat/.wast/.wasm in the repo carries a start section — swept textually AND by binary section id); emitted bytes for start-free modules are unchanged (guard only fires on Some), frozen anchors untouched; EXPECTED_DECLINES (#992) unchanged (keys on scripts/repro/*.wat, none of which carry (start)). Red-first: the 7 refusal tests in start_section_refusal_1046.rs failed on the parent commit and pass now; the start-free control passes throughout. Gates: fmt, clippy -D warnings, cargo test --workspace (true exit 0), claim_check 50/50, model_coverage_audit ok, rivet validate 50 errors (= main baseline, #1012). Refs #1046 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

avrabe and others added 5 commits August 18, 2026 20:09

Merge remote-tracking branch 'origin/main' into fix/arm-select-i64cmp…

dcccbcb

…-973

avrabe added 2 commits August 18, 2026 21:22

avrabe merged commit 7d05ea9 into main Aug 18, 2026
60 checks passed

avrabe deleted the fix/arm-select-i64cmp-973 branch August 18, 2026 19:50

avrabe mentioned this pull request Aug 18, 2026

fix(main): waive #973's selector growth — the subtraction gate caught its first real event #994

Closed

avrabe mentioned this pull request Aug 20, 2026

release(v0.58.0): "Delete the thing you replaced" #1010

Merged

Navigation Menu

fix(#973): ARM select on an i64-comparison returns the then-arm — and an ARM leg for the corpus CI never compiled - #992

fix(#973): ARM select on an i64-comparison returns the then-arm — and an ARM leg for the corpus CI never compiled#992
avrabe merged 7 commits into
mainfrom
fix/arm-select-i64cmp-973

avrabe commented Aug 18, 2026

Uh oh!

avrabe commented Aug 18, 2026

Uh oh!

temper-pulseengine Bot commented Aug 18, 2026

Uh oh!

avrabe commented Aug 18, 2026

Uh oh!

codecov Bot commented Aug 18, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

avrabe commented Aug 18, 2026

1. The miscompile

Red-first

Bytes

2. The CI gap — the larger half

3. What the leg newly surfaced — 48 vectors, two classes, both filed

4. Honest gaps

Gates

Uh oh!

avrabe commented Aug 18, 2026

Follow-up: the guard_same_arm claim, measured

Uh oh!

temper-pulseengine Bot commented Aug 18, 2026

Automated review for PR #992

Uh oh!

avrabe commented Aug 18, 2026

Runner reconciliation: ubuntu-latest matches macOS exactly

Uh oh!

codecov Bot commented Aug 18, 2026

Codecov Report

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Follow-up: the `guard_same_arm` claim, measured