ci(vcr-oracle): CI-gate the RV32 immediate-shift-fold execution oracle (#472, #242) - #489

avrabe · 2026-06-25T11:25:37Z

What

CI-gates the RV32 immediate-shift-fold differential oracle. VCR-ORACLE-001's deliverable is CI-gating the differentials, not shipping them as dev-time scripts you have to remember to run.

The RV32 immediate-shift-fold lever (#487, landed flag-off behind SYNTH_RV_SHIFT_FOLD) came with a unicorn UC_ARCH_RISCV differential (shift_fold_riscv_differential.py) that only ran by hand. Because the lever sits flag-off awaiting the on-silicon flip, nothing else exercises the flag-on path — the exact gap the cmp-select two-move oracle was added to close for that lever.

How

Adds an isolated rv32-shift-fold-oracle CI job that mirrors the existing cmp-select-oracle job:

build synth, pip-install wasmtime/unicorn/pyelftools in that job only (the main cargo test gate is not taxed with the C-library build graph);
run the differential, which executes every fixture function in both flag states under unicorn and asserts bit-identical-to-wasmtime.

It continuously validates the slli/srli/srai folds, the & 31 mask on >=32 and negative shift amounts, and the variable-shift non-fold, plus non-vacuity (.text 168B→148B, 5 folds). The differential now honors a SYNTH env override (default release for local dev; CI points it at the debug build for speed, exactly like cmp-select).

Frozen-safe

No codegen change, no emitted-bytes change — this wires an already-written, already-passing oracle into CI. Verified locally with the exact CI invocation:

$ cargo build -p synth-cli
$ SYNTH=./target/debug/synth python scripts/repro/shift_fold_riscv_differential.py
.text 168B -> 148B (-20B): 5 const shift(s) folded
ORACLE: PASS

ci.yml parses (yaml.safe_load); the new job is well-formed.

Part of epic #242 (VCR-*), closing the CI-gate loop on the #472 lever-1 oracle.

🤖 Generated with Claude Code

#472, #242) VCR-ORACLE-001's deliverable is CI-gating the differential oracles, not just shipping them as dev-time scripts. The RV32 immediate-shift-fold lever (#487, PR landed flag-off behind SYNTH_RV_SHIFT_FOLD) came with a unicorn UC_ARCH_RISCV differential (shift_fold_riscv_differential.py) but it only ran by hand. Since the lever sits flag-off awaiting the on-silicon flip, nothing else exercises the flag-on path — exactly the gap the cmp-select two-move oracle was added to close. Adds an isolated `rv32-shift-fold-oracle` CI job mirroring the existing `cmp-select-oracle` job: build synth, pip-install wasmtime+unicorn+pyelftools in that job ONLY (the main `cargo test` gate is not taxed with the C-library build graph), and run the differential. It executes every fixture function in BOTH flag states under unicorn and asserts bit-identical-to-wasmtime — continuously validating the slli/srli/srai folds, the `& 31` mask on >=32 and negative shift amounts, and the variable-shift non-fold, plus non-vacuity (.text 168B->148B, 5 folds). The differential now honors a SYNTH env override (default release for local dev; CI points it at the debug build for speed, like cmp-select). Frozen-safe: no codegen change, no emitted bytes change — wires an already-written, already-passing oracle into CI. Verified locally with the exact CI invocation (debug binary via SYNTH=./target/debug/synth): ORACLE PASS. ci.yml parses; new job well-formed. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

codecov · 2026-06-25T11:52:38Z

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!

…h disasm` text The CI oracle job failed with `SYMBOL MISSING` on the fresh runner while passing locally: the harness scraped function addresses out of `synth disasm` stdout with a regex, and that text is host-dependent (the disasm backend even decodes RISC-V bytes with an ARM decoder, and on the bare runner the symbol-line format differs so the regex matched nothing). Read the addresses straight from the ELF symbol table via pyelftools instead — the same backend-independent approach base_cse_differential.py uses. synth emits the symtab with an empty section name, so it's found by sh_type (SHT_SYMTAB), and addresses are made .text-relative by subtracting sh_addr. Re-verified with the exact CI invocation (debug binary via SYNTH env): ORACLE PASS, 5 folds, all 6 functions matched. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

…t func_N (#570) (#575) The script parsed `synth disasm` text and hardcoded func_0/func_1 — broken since the #394 name work (functions carry export/name-section names in the paths the script reads) and host-dependent besides (PR #489 lesson). Now: read STT_FUNC symbols from the ELF SHT_SYMTAB (located by section TYPE — synth's ET_REL objects emit it with an empty name), clear the Thumb bit from st_value, match the export name first with a positional func_N fallback for older objects, and derive the bl-scan window from the next symbol address. The `synth disasm` subprocess (and its ./target/debug/synth dependency) is gone entirely. Vectors and semantics unchanged; both variants (inlined #212, flat #215) PASS vs wasmtime with the flight_algo anchor 0x07FDF307. Also CI-gates the oracle (flight-seam-570-oracle job, mirroring the existing execution-oracle jobs) so this load-bearing fixture can't drift silently again. Closes #570 Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

) (#586) The script parsed `synth disasm` text with a regex to find the control_step_decide entry point — the #489 host-dependence class — and drifted into a KeyError on current main (found by the #583 flip lane; identical with SYNTH_SPILL_REALLOC=0, so pre-existing harness drift, not a codegen change). Symbols now come from the ELF symtab via pyelftools, mirroring the merged #575 flight_seam_differential pattern: - locate SHT_SYMTAB by section TYPE (synth's ET_REL objects emit it with an empty section name, so get_section_by_name fails) - mask the Thumb bit on STT_FUNC st_value - export name first (control_step_decide), positional func_0 fallback for older objects, loud SYMBOL MISSING exit otherwise Vectors and semantics are unchanged (13 vectors incl. gale's reference anchor control_step_decide(3000,50,40,0) = 0x00210A55); the script no longer needs a synth binary at runtime at all. Also CI-gates it as control-step-584-oracle (flight-seam-570-oracle pattern) so harness drift reddens instead of rotting — the r12_spill_496 oracle covers control_step on the DEFAULT optimized path, this covers --relocatable. Closes #584 Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

…d mask profile Two defects in the #374 memory.copy/memory.fill lowering (select_with_stack), one lane: (dst/src as walking loop pointers, len as the byte buffer). LocalGet of a register-homed local (AAPCS param r0-r3, promoted local r4-r8) pushes the HOME register itself, so a local reused AFTER the op read a wild mem_base+cursor pointer or the last byte copied. Fix, mirroring the #193 reservation discipline: `bulk_mutable_operand` copies a popped operand into a fresh scratch before mutation when it is still live (live param/promoted home, duplicate vstack entry, if/block result reg, or aliased to another popped operand of the same op); a provably-dead temp is used in place, keeping the const-operand shapes byte-identical (#374 differential still 16/16). The red differential also exposed the #663-class range-realloc hole the fix then tripped over: `try_reallocate_segment` treated a pool register with NO range in a segment as free, but such a register can be LIVE-THROUGH (a param home the segment never touches — the memcpy backward path recolored its walking-pointer intermediate onto R0, the still-live dst local). Absent pool colours are now blocked with synthetic pinned interference nodes; identity colouring within the segment's present registers always exists, so no recoloring the original bytes had is lost (frozen anchors stay 10/10 bit-identical). Relaxed-exit terminal segments keep the #580 exemptions (only absent R0/R1 blocked past the bx lr). was emitted byte-identical to `none` while safety-manifest.json still attested "mask" (attestation-integrity hole). The lowering now applies the scalar #651/#654 mask_effective_address wrap-not-trap discipline: dst and src effective addresses fold with AND (size-1) and len clamps to size-dst / size-src so the FINAL byte stays in bounds — every loop access lands in [0, size), wasm-in-bounds ops are unchanged, and the manifest's mask claim is now backed by the emission (mask ≢ none proven by the pure-bulk byte-diff gate). Oracles (all run locally, red on v0.37.1 → green here): - scripts/repro/bulk_local_clobber_677_differential.py — 2/8 → 8/8 vs wasmtime under unicorn (dst/src/len reuse + const control). - scripts/repro/bulk_mask_679_differential.py — pure-bulk byte-diff (identical → differs), manifest coherence, escape/fold/clamp vectors with R10=4096 and out-of-bound containment (raw escaped writes → contained). - scripts/repro/bulk_memory_374_differential.py — 16/16 (unchanged shapes byte-identical; script gains SYNTH env override). - frozen_codegen_bytes 10/10; safety_bounds_377 13/13+13/13; unreachable_665, i32_shift_mask_682 PASS; cargo test --workspace green; fmt + clippy -D clean. - 8 new selector unit tests (677 preservation/aliasing/no-copy-when-dead, 679 fold+clamp presence, mask≠none structural). Both oracles are CI-wired in the trap-semantics job (#489 discipline). Closes #677. Closes #679. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…pattern) - liveness.rs: iter_mut over map → values_mut (rust-1.97 clippy). - The two #677/#679 differential harnesses read .symtab via get_section_by_name, which returns None because synth emits an unnamed SHT_SYMTAB section; switched to iterate by sh_type (the established #489 pattern all other harnesses use). Both oracles PASS locally. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…d mask profile Two defects in the #374 memory.copy/memory.fill lowering (select_with_stack), one lane: (dst/src as walking loop pointers, len as the byte buffer). LocalGet of a register-homed local (AAPCS param r0-r3, promoted local r4-r8) pushes the HOME register itself, so a local reused AFTER the op read a wild mem_base+cursor pointer or the last byte copied. Fix, mirroring the #193 reservation discipline: `bulk_mutable_operand` copies a popped operand into a fresh scratch before mutation when it is still live (live param/promoted home, duplicate vstack entry, if/block result reg, or aliased to another popped operand of the same op); a provably-dead temp is used in place, keeping the const-operand shapes byte-identical (#374 differential still 16/16). The red differential also exposed the #663-class range-realloc hole the fix then tripped over: `try_reallocate_segment` treated a pool register with NO range in a segment as free, but such a register can be LIVE-THROUGH (a param home the segment never touches — the memcpy backward path recolored its walking-pointer intermediate onto R0, the still-live dst local). Absent pool colours are now blocked with synthetic pinned interference nodes; identity colouring within the segment's present registers always exists, so no recoloring the original bytes had is lost (frozen anchors stay 10/10 bit-identical). Relaxed-exit terminal segments keep the #580 exemptions (only absent R0/R1 blocked past the bx lr). was emitted byte-identical to `none` while safety-manifest.json still attested "mask" (attestation-integrity hole). The lowering now applies the scalar #651/#654 mask_effective_address wrap-not-trap discipline: dst and src effective addresses fold with AND (size-1) and len clamps to size-dst / size-src so the FINAL byte stays in bounds — every loop access lands in [0, size), wasm-in-bounds ops are unchanged, and the manifest's mask claim is now backed by the emission (mask ≢ none proven by the pure-bulk byte-diff gate). Oracles (all run locally, red on v0.37.1 → green here): - scripts/repro/bulk_local_clobber_677_differential.py — 2/8 → 8/8 vs wasmtime under unicorn (dst/src/len reuse + const control). - scripts/repro/bulk_mask_679_differential.py — pure-bulk byte-diff (identical → differs), manifest coherence, escape/fold/clamp vectors with R10=4096 and out-of-bound containment (raw escaped writes → contained). - scripts/repro/bulk_memory_374_differential.py — 16/16 (unchanged shapes byte-identical; script gains SYNTH env override). - frozen_codegen_bytes 10/10; safety_bounds_377 13/13+13/13; unreachable_665, i32_shift_mask_682 PASS; cargo test --workspace green; fmt + clippy -D clean. - 8 new selector unit tests (677 preservation/aliasing/no-copy-when-dead, 679 fold+clamp presence, mask≠none structural). Both oracles are CI-wired in the trap-semantics job (#489 discipline). Closes #677. Closes #679. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…pattern) - liveness.rs: iter_mut over map → values_mut (rust-1.97 clippy). - The two #677/#679 differential harnesses read .symtab via get_section_by_name, which returns None because synth emits an unnamed SHT_SYMTAB section; switched to iterate by sh_type (the established #489 pattern all other harnesses use). Both oracles PASS locally. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…copy/fill (#695) * fix(bulk-memory): #677 operand-register clobber + #679 silent-unmasked mask profile Two defects in the #374 memory.copy/memory.fill lowering (select_with_stack), one lane: (dst/src as walking loop pointers, len as the byte buffer). LocalGet of a register-homed local (AAPCS param r0-r3, promoted local r4-r8) pushes the HOME register itself, so a local reused AFTER the op read a wild mem_base+cursor pointer or the last byte copied. Fix, mirroring the #193 reservation discipline: `bulk_mutable_operand` copies a popped operand into a fresh scratch before mutation when it is still live (live param/promoted home, duplicate vstack entry, if/block result reg, or aliased to another popped operand of the same op); a provably-dead temp is used in place, keeping the const-operand shapes byte-identical (#374 differential still 16/16). The red differential also exposed the #663-class range-realloc hole the fix then tripped over: `try_reallocate_segment` treated a pool register with NO range in a segment as free, but such a register can be LIVE-THROUGH (a param home the segment never touches — the memcpy backward path recolored its walking-pointer intermediate onto R0, the still-live dst local). Absent pool colours are now blocked with synthetic pinned interference nodes; identity colouring within the segment's present registers always exists, so no recoloring the original bytes had is lost (frozen anchors stay 10/10 bit-identical). Relaxed-exit terminal segments keep the #580 exemptions (only absent R0/R1 blocked past the bx lr). was emitted byte-identical to `none` while safety-manifest.json still attested "mask" (attestation-integrity hole). The lowering now applies the scalar #651/#654 mask_effective_address wrap-not-trap discipline: dst and src effective addresses fold with AND (size-1) and len clamps to size-dst / size-src so the FINAL byte stays in bounds — every loop access lands in [0, size), wasm-in-bounds ops are unchanged, and the manifest's mask claim is now backed by the emission (mask ≢ none proven by the pure-bulk byte-diff gate). Oracles (all run locally, red on v0.37.1 → green here): - scripts/repro/bulk_local_clobber_677_differential.py — 2/8 → 8/8 vs wasmtime under unicorn (dst/src/len reuse + const control). - scripts/repro/bulk_mask_679_differential.py — pure-bulk byte-diff (identical → differs), manifest coherence, escape/fold/clamp vectors with R10=4096 and out-of-bound containment (raw escaped writes → contained). - scripts/repro/bulk_memory_374_differential.py — 16/16 (unchanged shapes byte-identical; script gains SYNTH env override). - frozen_codegen_bytes 10/10; safety_bounds_377 13/13+13/13; unreachable_665, i32_shift_mask_682 PASS; cargo test --workspace green; fmt + clippy -D clean. - 8 new selector unit tests (677 preservation/aliasing/no-copy-when-dead, 679 fold+clamp presence, mask≠none structural). Both oracles are CI-wired in the trap-semantics job (#489 discipline). Closes #677. Closes #679. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * fix: clippy values_mut + harness reads symtab by SHT_SYMTAB type (#489 pattern) - liveness.rs: iter_mut over map → values_mut (rust-1.97 clippy). - The two #677/#679 differential harnesses read .symtab via get_section_by_name, which returns None because synth emits an unnamed SHT_SYMTAB section; switched to iterate by sh_type (the established #489 pattern all other harnesses use). Both oracles PASS locally. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

… install ld Wiring the oracle (previous commit) immediately earned its keep: it failed on the CI runner with FileNotFoundError 'arm-none-eabi-nm' while passing locally. A host dependency is exactly what a local run cannot detect -- the #850 class, where an oracle that only works on the author's machine is a local check, not a gate. Two host dependencies, handled differently because they are not the same: 1. `arm-none-eabi-nm` -- REMOVED. Symbols now come from the ELF symbol table via pyelftools (already a dependency of this job). Note this file's own `load()` already did it that way, citing #489 "symtab, not disasm text"; only main() still shelled out. The port must look the table up by TYPE (SHT_SYMTAB), not by name: synth's relocatable objects emit their symtab with an EMPTY sh_name, so get_section_by_name(".symtab") returns None on a file that has one. `nm` searches by type, which is why the shell-out worked and a naive by-name port reported "no .symtab" -- a false failure that would have looked like a miscompile. 2. `arm-none-eabi-ld` -- INSTALLED (binutils only, not the full gcc). The link step is load-bearing: it proves the internal `bl` relocation actually resolves, and skipping it would make that half of the gate vacuous. When a dependency backs a real check, install the dependency; do not delete the check. Verified: 7 exports emitted, 109 execution rows bit-identical to wasmtime. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

…R-RA-004, epic #242) (#885) * test(#881): red-first repro — the two GI-FPU-002 exhaustion classes + the #869 mixed shape deep_s: >16 live f32 (phase-1 S-file), deep_d: >8 live f64 (phase-2 D-file), deep_mix: i64->f32 converts under a live f32 stack (the v0.52 falcon rate/ekf D-pressure in f32-only-by-policy code). All three currently loud-decline on -t cortex-m7dp --relocatable with the exact messages the falcon v1.128 entry points report. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * feat(#881): VFP register-file spilling — the GI-FPU-002 exhaustion rung (VCR-RA-004, epic #242) StackVal::{Float,Double}Spilled + spill_deepest_vfp (deepest segment-local = farthest next use under LIFO discipline, the Belady criterion) + vfp_reload_spilled + vfp_ensure_headroom, driven by a pre-op VFP pressure guard active ONLY under the new vfp_spill_on_exhaustion retry rung (the backend re-runs the full recovery ladder with it after a first pass ends in a GI-FPU-002 exhaustion Err, composing with the #587 pool-grow rung). Soundness rails: - straight-line floor: entries pushed before the last control-flow boundary are never victims (a conditional spill store would not dominate its reload on the untaken path) - S/D aliasing: victims/holes tracked through the ONE shared 16-slot vfp_used map (D-alloc marks both S halves; the D-headroom loop spills until a FULL aligned pair frees) - pinned f32/f64 param+local homes are never victims (freeing relieves nothing) - VSTR/VLDR imm8*4 range (>1020 declines loudly, #180/#185) - spilled entries reaching any integer/float consumer un-reloaded is a loud decline, never a stale register read All three #881 repro shapes (deep_s S-file, deep_d D-file, deep_mix = the v0.52 #869 D-pressure-in-f32-only-code) now emit T symbols on -t cortex-m7dp --relocatable. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * test(#881): execution differential — 7 spilled-VFP shapes bit-identical vs wasmtime Falcon flags (-t cortex-m7dp --relocatable), internal bl resolved by a real arm-none-eabi-ld link (hard-fail on any diagnostic — no reloc ever silently skipped), 109 rows incl. NaN/inf/subnormal operands, both select arms, spilled-across-call, pinned-home, and S/D-aliasing-churn shapes. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * feat(#881): VCR-RA-003 sees the VFP file — slot-aliasing + caller-saved-across-call twins Invariant 5: per-straight-line-segment VFP spill-slot non-aliasing at 4-byte-half granularity (an F32Store clobbering half of a live F64Store's slot is caught; a provably-same-value re-store — same source S-word, no redefinition, the legal preserve-then-arg-stage overlap — is benign). Invariant 6: an S-word (2..16) defined before a bl and read after with no redefinition crossed the AAPCS-VFP caller-saved boundary; words 0/1 (S0/D0 return) excluded, the documented R0/R1-twin false-negative boundary. Both driven by vfp_word_effect: precise word-level defs/uses for the simple VFP ops, loud None for encoder-expanded compounds (decline > guess applied to the checker), Some(empty) for provably-VFP-free integer ops. All 8 float differentials re-run green against the now-stricter unconditional validator (no false positives on shipped patterns): 619 84/84, 708/709 48/48, 719 238/238, 369 339/339, 869 96296, 782 192686, 782b 702, 881 109. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * test(#881): red-first pins for the VFP RA-003 twins — 7 unit cases Live-fixture red evidence (both reverted): dropping S2 preservation in preserve_vfp_caller_saved fired VfpCallerSavedLiveAcrossCall{word:2, call_index:32} on spill_call; forcing every VFP spill onto slot 0 fired VfpSpillSlotAliased on deep_s/deep_d/spill_call — compiles REFUSED, not miscompiled. Unit pins: two-live-values aliasing, F32-over-F64-half (S/D aliasing), same-value refresh benign, refresh-after-redef caught, live-across-bl caught, preserve/restore green, S0/S1 return exclusion. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * ci(#881/#879): wire the VFP spill execution oracle — it existed but nothing ran it vfp_spill_881_differential.py is the oracle behind this lane's headline claim (7 falcon-shaped exports reaching nm -> T, execution rows bit-identical to wasmtime on cortex-m7dp). It was written, committed, and referenced NOWHERE -- `git grep` found no ci.yml entry and no other caller. The PR board was green with its central gate inert, so the claim was hand-checked only. That is the #879 shelfware class recurring inside the very release whose audit found and fixed two other instances of it (gpio-thin, rv32-boot). Writing an oracle and wiring an oracle are separate steps, and the second is the one that gets dropped when a lane runs out of budget -- which is exactly what happened here: the lane died on a session limit. Wired with the anti-vacuity discipline the #879 fix established: set -o pipefail (a bare `| tee` would report tee's exit status), plus greps on BOTH halves of the claim -- the full export count, so a silent decline cannot read as success, and a non-zero execution-row count. Exit 0 alone is not trusted. Verified red-first by mutation: rewriting the summary to 0 execution rows fails the row grep, and to "all 6 exports" fails the export grep. The committed branch state passes on its own (7 exports, 109 rows) with the lane's uncommitted work-in-progress excluded. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * fix(#881): make the VFP oracle host-independent — symtab by TYPE, and install ld Wiring the oracle (previous commit) immediately earned its keep: it failed on the CI runner with FileNotFoundError 'arm-none-eabi-nm' while passing locally. A host dependency is exactly what a local run cannot detect -- the #850 class, where an oracle that only works on the author's machine is a local check, not a gate. Two host dependencies, handled differently because they are not the same: 1. `arm-none-eabi-nm` -- REMOVED. Symbols now come from the ELF symbol table via pyelftools (already a dependency of this job). Note this file's own `load()` already did it that way, citing #489 "symtab, not disasm text"; only main() still shelled out. The port must look the table up by TYPE (SHT_SYMTAB), not by name: synth's relocatable objects emit their symtab with an EMPTY sh_name, so get_section_by_name(".symtab") returns None on a file that has one. `nm` searches by type, which is why the shell-out worked and a naive by-name port reported "no .symtab" -- a false failure that would have looked like a miscompile. 2. `arm-none-eabi-ld` -- INSTALLED (binutils only, not the full gcc). The link step is load-bearing: it proves the internal `bl` relocation actually resolves, and skipping it would make that half of the gate vacuous. When a dependency backs a real check, install the dependency; do not delete the check. Verified: 7 exports emitted, 109 execution rows bit-identical to wasmtime. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --------- Co-authored-by: Claude <noreply@anthropic.com>

…revealed Flipping GI-FPU-002 from `proposed` to `implemented` made rivet START checking its lifecycle coverage, which correctly reported that the requirement had NO verification artifact at all. The gap was not created by the flip — the wrong status was HIDING it, which is the same failure mode as the duplicate id itself, one rule further down. The evidence already existed and was already named in the requirement's own criteria; it simply had no typed `verifies` link. GI-FPU-VER-002 is that link, and it records what the verification actually is rather than asserting that some exists: * the f32 execution differential (48/48 bit-exact vs wasmtime on cortex-m4f, symbols read from the ELF SYMTAB per #489 rather than from host-dependent `synth disasm` text, FPU genuinely enabled via CPACR + FPEXC.EN); * the HONEST-REJECT direction in the same harness (cortex-m3 must still refuse) — a one-directional differential would pass equally well on a compiler that had quietly widened the FPU gate; * the unit-level pins that need no emulator (AAPCS-VFP S0/S1 homing, the swapped-VCVT signedness fix); * the v0.53 #881 spilled-VFP differential (109 rows, NaN-aware per WASM §4.3.3, internal `bl` resolved by a REAL link so an unresolved relocation cannot be silently skipped as a pass); * and the one part of the surface whose evidence is encoding-level ONLY — the f32 comparisons, because unicorn does not model the VMRS FPSCR→APSR flag transfer. Recorded, not omitted. Deliberately shaped `method: automated-test` + `steps.run`/`steps.coverage` rather than mirroring GI-FPU-VER-001's `method: test` + `pass-criteria`, which produce a WARN and an INFO against the schema. This adds ZERO new diagnostics. MEASURED, prompted by review asking whether `rivet coverage` — the SECOND step of the same CI job, which I had not exercised — moved: rivet coverage, real exit 0 both sides swe1-has-verification (sw-req) 31/60 (51.7%) -> 33/60 (55.0%) swe6-verifies-swe1 32/32 -> 34/34 sys5-verifies-sys2 49/49 -> 50/50 Overall (weighted) 90.3% -> 90.7% VCR-RA-004 and GI-FPU-002 both drop off the "lacking verification" list. Full diagnostic diff for the whole branch vs main is now exactly: −2 ERROR (both ours: synth:396, the duplicate id) −2 WARN (GI-FPU-002 and VCR-RA-004 "should be verified by", both closed) +2 WARN, +1 INFO (all three VCR-VER-004's, all of kinds its sibling sys-verification artifacts already carry) So: errors 52 -> 50 with ours 2 -> 0, and warnings net UNCHANGED at 104. Lifecycle coverage gaps 54 -> 56 — honest, not a regression: GI-FPU-002 and VCR-RA-004 are newly CHECKED because they are no longer `proposed`. Both were absent from the baseline list only because a wrong status exempted them. cargo fmt 0 / clippy 0 / test --workspace 0 (2675 passed) / claim_check 37/37. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

… de-staled, VCR-VER-004 filed (#893) (#913) * fix(rivet): VCR-DEC-003 traces-to an ARTIFACT, not a GitHub issue number `traces-to: synth:396` was the one genuinely-ours rivet broken-link error: `synth:396` reads as "artifact 396 in repo synth", and no such artifact exists — an issue number used where an artifact id belongs. The traceability intent is preserved rather than deleted: synth#396's own body says "Tracked in rivet as VCR-COV-001, sibling to VCR-DBG-001", and VCR-COV-001's title carries "(synth #396)". So the link retargets to VCR-COV-001 (in-repo `traces-to` targets are already idiomatic in this file — VCR-SEL-001, VCR-RA-001, VCR-MEM-001, …), and `synth-396` joins the tags so the issue number stays discoverable as a reference instead of a resolvable target. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * fix(rivet): GI-FPU-002 was declared TWICE — the `proposed` copy silently won The second genuinely-ours rivet error, which the lane brief did not know about because the local grep for it (`^ ERROR:`) misses filename-prefixed diagnostics: gale-integration.yaml: ERROR: [GI-FPU-002] artifact id 'GI-FPU-002' is declared more than once: ./artifacts/verified-codegen-roadmap.yaml and ./artifacts/gale-integration.yaml — the second definition silently overwrites the first This is the #893 class one level worse than a stale description: the requirement was declared in gale-integration.yaml (`status: proposed`, the original #369 ask) and AGAIN in verified-codegen-roadmap.yaml (`status: implemented`, the phase-1 delivery record added by PR #705). rivet loaded the `proposed` copy over the `implemented` one, so the traceability graph reported GI-FPU-002 as NOT STARTED while README/CHANGELOG report #369 CLOSED, f32 complete v0.41, f64 complete v0.43, and VFP register-file spilling shipped v0.53. Resolved by MERGING, not deleting — the two copies carried disjoint edges and disjoint evidence: * Survivor: gale-integration.yaml. That is the id's namespace home (GI-002 -> GI-FPU-001 -> GI-FPU-002 -> GI-FPU-VER-001 are one chain in that file; GI-FPU-002 was the ONLY GI-* artifact in the roadmap). It also already carried `derives-from GI-002`, `traces-to gale:369`, and the jess REQ-PIX-001 / AFD-024 Pixhawk linkage — all of which a straight delete of that side would have dropped. README names the roadmap the single source of truth for the VCR-* program's roadmap status, which GI-* is not. * Folded in: the roadmap copy's six-point phase-1 DELIVERED list and its full verification-criteria (the f32_vfp_619_differential RED->GREEN evidence, the m3 honest-reject direction, the f32_hardfloat_619.rs unit lock, and the recorded unicorn VMRS FPSCR->APSR emulator gap). * De-staled, since the merge had to pick one status anyway: `proposed` -> `implemented`, with the post-phase-1 evidence the roadmap copy predated — f64 complete v0.43 (#369 closed), v0.52 #869 inline i64<->float, v0.53 #881 VFP spilling (109 rows bit-identical to wasmtime) — and the two residuals stated as loud declines rather than implied away (`f32.{ceil,floor,trunc,nearest}` pending a real VRINT.F32 after v0.54 removed the unsound saturating-VCVT pseudo-op, and `i64.trunc_sat_f32_*` on single-precision FPUs). * Where the duplicate was, the roadmap now carries a pointer comment explaining why the id is not defined there. rivet: 52 -> 50 errors; NON-EXTERNAL errors 2 -> 0. Warning/info diagnostic sets are byte-identical before/after (no new class introduced). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * fix(#893): VCR-RA-004 was `proposed` for a resolver that shipped in v0.11.38 Half of #893: v0.53's VFP-spilling lane tagged its work `VCR-RA-004`, while artifacts/verified-codegen-roadmap.yaml still carried that id as `status: proposed`. The brief offered two resolutions — mint a new id for the v0.53 work, or flip VCR-RA-004 to implemented. The evidence decides it, and it is neither of the two things the ID-collision framing suggested: the resolver VCR-RA-004 describes shipped in **v0.11.38**, three years of releases before the lane that got blamed for overloading the id. `synth_synthesis::parallel_move` is verbatim what the artifact asks for — a pure, testable component that sequentializes a parallel move set with cycle detection, scratch selection from dead registers, and a guaranteed-progress fallback. The artifact's own tags already said `release-v0.11.38`; the CHANGELOG names it twice (v0.11.38 "Cycle-safe parallel-move resolver (`synth_synthesis::parallel_move`, VCR-RA-004)" and v0.11.39 "#327 — VCR-RA-004's resolver (v0.11.38) breaks cycles via a stack-scratch cell"). Only the status field was never flipped. Minting a second id would have created the collision the issue was trying to remove. So: `proposed` -> `implemented`, with the evidence written down instead of left in changelog prose — * the algorithm and its progress discipline (the size bound and the strictly-shrinking pending set are `assert!`s in the resolver, so an unbounded path aborts rather than emitting); * both consumers, each of which removed a real defect rather than only adding a component: v0.11.39 #327 arg-move marshalling (the old cycle-breaker demanded a callee-saved register AND miscompiled genuine 2-swaps by duplicating a value), and v0.53 #881 VFP register-file spilling (the falcon `S0..S15 all live` wall) — which is precisely the work the v0.53 notes tagged VCR-RA-004; * SWVER-022, a new sw-verification artifact linking `verifies` -> VCR-RA-004, so the right side of the V is closed by a typed link rather than by a paragraph. It records the run recipe and what each of the three criteria clauses is actually met by. `implemented`, NOT `verified`, deliberately. The property test the criteria demand does exist and does exactly what they specify — 2000 iterations over R0..R8 alternating full random permutations with partial move sets, each re-checked at scratch-set sizes 0/1/2 (6000 sequentializations) against a reference parallel semantics, plus 12 directed shape tests — verified locally, `cargo test -p synth-synthesis parallel_move` 13/13, real exit 0. But the second pitfall the artifact names, split points landing inside hot loops, is still bounded by ASSUMPTION (synth's straight-line segment scope) rather than by a check that fails when segments widen. That residual is now stated in both the requirement and SWVER-022 rather than implied away. rivet: non-external errors still 0; warnings 104 -> 103 (VCR-RA-004's "should be verified by at least one verification measure" WARN closed, no new warning introduced). claim_check 37/37. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * fix(#893): VCR-SEL-005 spans THREE backends, and both ledger counts had drifted Second half of #893. VCR-SEL-005's description still said the gate lowers probes on "BOTH the ARM (Thumb-2) and RISC-V (RV32IMAC) selectors" — it has covered a third, aarch64, since v0.53 (#883). SWVER-017, the verification artifact that is supposed to be the right-side evidence for exactly this requirement, carried the same claim in its title ("ARM vs RISC-V") and described a two-selector ledger. While correcting the backend count I checked the numbers the same documents assert, and both were stale in the same direction — they described gaps that have since CLOSED, which is the flattering direction and therefore the one worth checking: * The roadmap said "the KNOWN_DIVERGENCES ledger is now 5 Zbb + 16 new = 21 entries". The array holds 18: `memory.size`/`memory.grow` closed in v0.50 and `br_table` in v0.53 (#882). * `known_divergences`'s own doc comment said 19 (it had accounted for v0.50 but not #882). * `aarch64_known_divergences`'s doc comment said "leaving the SEVEN below" over an array of 5 — v0.54 (#899) closed `global.get`/`global.set` and removed the entries without updating the prose above them. All four now state what the arrays hold, with the counts' derivation written out so the next drift is visible, and a note at each site that the count must move with the array. The stale-entry check already forces a CLOSED gap to retire its ledger line; nothing forced the PROSE ABOUT the ledger to move with it, which is the #893 defect one layer up. Also recorded, because it is the part of the third-backend leg that is not just "one more backend": aarch64 gets a probed FLOAT/SIMD surface (`a64_extended_surface`, floor `probed >= 100`) that ARM and RV32 structurally cannot have — float is `StructurallyExcluded` from their leg because ARM float lowering is TARGET-parameterized (f32.add declines at fpu=None, lowers at Single/Double) and RV32 has no FPU, whereas the aarch64 backend has one fixed host profile, so both directions are assertable and a stale gap-claim is caught the same way a stale divergence is. Changes are prose and doc-comment only — no test logic touched. `cargo test -p synth-backend-riscv --test cross_backend_op_parity` 8/8, real exit 0. rivet non-external errors still 0; claim_check 37/37. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * docs(roadmap): file VCR-VER-004 — a shipped North-Star component had NO roadmap entry README calls artifacts/verified-codegen-roadmap.yaml "the single source of truth for roadmap status". VCR-VER-004 shipped in v0.54 and appeared in the CHANGELOG, the FEATURE_MATRIX template and the CI job list — but the roadmap had no entry for it at all, so the one document the README points at for "what is the state of the VCR-* program" was missing the release's headline validator. The entry records what it is and, more importantly, why it exists: v0.53 showed by mutation that emptying `cfg_exit_observable` makes the compiler leave a return value in the WRONG REGISTER and that BOTH per-compilation validators accept it (`validate_cfg_rewrite` -> Ok, VCR-RA-003 -> Consistent). Only execution caught it. `abi_contract::validate_abi_contract` is not a third file on the same axis — it differs on four axes (an obligation that cannot be emptied because it is `RETURN_CONTRACT_REGS = [R0, R1]` hard-named in its own source; forward rather than backward, so there is no seed whose empty set is a vacuous fixpoint; evidence that is a VALUE compared by greatest-fixpoint bisimulation rather than a name-pair; and a `(orig, rewritten)` signature that takes nothing from the pass). Its honest limit is in the entry, not implied away — all three residuals: (a) it GATES only the flag-off colouring allocator; on the default path it is a report-only audit held to a `Violated 0` CI floor, because gating a user's compile on a checker whose false-positive rate is measured rather than proven is a flip we have deliberately not taken; (b) memory is NOT in its obligation (complementary to `validate_cfg_rewrite`, not redundant with it); (c) THE OP MODEL IS STILL SHARED — def/use extraction runs through `liveness::reg_effect`, so a mismodeled op is a blind spot common to all three instruments. VCR-VER-004 closes the shared-CONTRACT hole, not the shared-OP-MODEL hole, and until `synth-verify`'s `ArmSemantics::encode_op` is pinned against it (VCR-ISA-001's Sail-derived semantics being the eventual anchor, now a typed `traces-to` link rather than a prose aside) "three independent validators" WOULD BE AN OVERCLAIM. Shaped to match its two siblings VCR-VER-003 / VCR-VER-761 exactly: `sys-verification`, `verifies -> VCR-001`, `method: translation-validation`, `preconditions`/`steps`/`pass-criteria`. That inherits two diagnostics those siblings already carry (the schema's `method` allowed-values does not list `translation-validation`, and `pass-criteria` is not a declared sys-verification field) — kept deliberately, because the fix for those is a rivet schema decision about the whole family, not a divergent shape for one member. rivet: 50 errors, non-external 0 (unchanged). Warnings 103 -> 105; the delta is exactly the three new-artifact diagnostics above, and the diagnostic-class diff against the lane's baseline shows no new KIND. claim_check 37/37. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * docs(README): the aarch64 crate row still said "integer subset" `synth-backend-aarch64` has not been an integer subset since v0.54. The row now names what actually ships and points at the generated feature matrix for the exact surface rather than restating it (a second copy of that list is how v0.54's cold review found a doc-honesty defect): * the complete scalar f32/f64 surface (v0.54 #898 — rounding, FP memory, i64 converts, guarded i64 truncations); * bounds-checked linear memory (default `--safety-bounds software`, #865); * WASM globals and `call_indirect` with all three §4.4.8 trap guards (v0.54 #899); * direct calls and full control flow. The row is the LAST place in README that described the backend by what it could not do; the intro paragraph and the feature matrix were already current. Note for whoever picks this up next: CLAUDE.md carries a byte-identical stale copy of this row. It is deliberately NOT touched here — that file is agent configuration and is not mine to edit on a lane brief. claim_check 37/37 (the aarch64 rows in the generated matrix are template- driven and unaffected — no generated doc was hand-edited). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * ci(#893): the Rivet Validation gate could not see either error this lane fixed Both defects this lane repaired were sitting in a tree with `Rivet Validation` green. That is not a coincidence — the job's filter had two holes, and each one swallowed exactly one of them. (1) `grep "^ ERROR:"` anchored on two-space-indented lines. rivet prefixes SOME diagnostics with the source file instead (`gale-integration.yaml: ERROR: …`), so that entire class was invisible to the gate — including "artifact id X is declared more than once … the second definition silently overwrites the first". That is how GI-FPU-002 could be `implemented` in one file and `proposed` in another, with rivet resolving it to `proposed`, and nothing complained. (2) The cross-repo exemption `targets '.*:.*' which does not exist` exempted any target containing a COLON. `synth:396` contains a colon. So a broken link in our OWN graph — an issue number written where an artifact id belongs — was classified as an unresolvable link into an un-rivet'd sibling repo and waved through. Fixed structurally rather than by allowlist: every line containing `ERROR:` is now considered, and the exemption is "a target carrying a FOREIGN prefix", with our own `synth:` prefix explicitly added back to the ours-count. A new sibling repo therefore needs no edit here, and our own prefix can never slip back into the exempt set. Failures now PRINT the offending lines instead of only a count, so the next one is self-diagnosing. RED-FIRST, end to end, by replaying this exact step (extracted from the YAML, not paraphrased) against both trees: * pre-fix artifacts (65417c0): exit 1, "Found 2 rivet validation errors that are OURS (not cross-repo)", both named; * fixed artifacts (this branch): exit 0, with the expected cross-repo warning still emitted. CAVEAT, stated rather than assumed: this was verified against local rivet 0.28.0, while the job pins 0.23.0. The duplicate-id diagnostic may not exist in 0.23.0 at all, in which case hole (1)'s fix is latent protection rather than an active check today; hole (2)'s fix is version-independent. If 0.23.0 emits some other filename-prefixed error we cannot see locally, this job is where it will surface — and surfacing it is the point. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * docs(CHANGELOG): v0.55 L7 — traceability repair + the honest-N/A backlog Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * fix(#893): GI-FPU-VER-002 — close the gap the GI-FPU-002 status flip revealed Flipping GI-FPU-002 from `proposed` to `implemented` made rivet START checking its lifecycle coverage, which correctly reported that the requirement had NO verification artifact at all. The gap was not created by the flip — the wrong status was HIDING it, which is the same failure mode as the duplicate id itself, one rule further down. The evidence already existed and was already named in the requirement's own criteria; it simply had no typed `verifies` link. GI-FPU-VER-002 is that link, and it records what the verification actually is rather than asserting that some exists: * the f32 execution differential (48/48 bit-exact vs wasmtime on cortex-m4f, symbols read from the ELF SYMTAB per #489 rather than from host-dependent `synth disasm` text, FPU genuinely enabled via CPACR + FPEXC.EN); * the HONEST-REJECT direction in the same harness (cortex-m3 must still refuse) — a one-directional differential would pass equally well on a compiler that had quietly widened the FPU gate; * the unit-level pins that need no emulator (AAPCS-VFP S0/S1 homing, the swapped-VCVT signedness fix); * the v0.53 #881 spilled-VFP differential (109 rows, NaN-aware per WASM §4.3.3, internal `bl` resolved by a REAL link so an unresolved relocation cannot be silently skipped as a pass); * and the one part of the surface whose evidence is encoding-level ONLY — the f32 comparisons, because unicorn does not model the VMRS FPSCR→APSR flag transfer. Recorded, not omitted. Deliberately shaped `method: automated-test` + `steps.run`/`steps.coverage` rather than mirroring GI-FPU-VER-001's `method: test` + `pass-criteria`, which produce a WARN and an INFO against the schema. This adds ZERO new diagnostics. MEASURED, prompted by review asking whether `rivet coverage` — the SECOND step of the same CI job, which I had not exercised — moved: rivet coverage, real exit 0 both sides swe1-has-verification (sw-req) 31/60 (51.7%) -> 33/60 (55.0%) swe6-verifies-swe1 32/32 -> 34/34 sys5-verifies-sys2 49/49 -> 50/50 Overall (weighted) 90.3% -> 90.7% VCR-RA-004 and GI-FPU-002 both drop off the "lacking verification" list. Full diagnostic diff for the whole branch vs main is now exactly: −2 ERROR (both ours: synth:396, the duplicate id) −2 WARN (GI-FPU-002 and VCR-RA-004 "should be verified by", both closed) +2 WARN, +1 INFO (all three VCR-VER-004's, all of kinds its sibling sys-verification artifacts already carry) So: errors 52 -> 50 with ours 2 -> 0, and warnings net UNCHANGED at 104. Lifecycle coverage gaps 54 -> 56 — honest, not a regression: GI-FPU-002 and VCR-RA-004 are newly CHECKED because they are no longer `proposed`. Both were absent from the baseline list only because a wrong status exempted them. cargo fmt 0 / clippy 0 / test --workspace 0 (2675 passed) / claim_check 37/37. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * docs(CHANGELOG): record the two verification artifacts + the rivet coverage delta Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * docs(roadmap): disambiguate the aarch64 ledger count (5 entries, not 4 named) The prose grouped `local.set`+get and `local.tee` on a param local as one phrase over two separate ledger entries, so the sentence read as four items beside the count 5 — a small instance of exactly the prose-vs-array drift this paragraph exists to prevent. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * docs(CLAUDE.md): de-stale the three aarch64 claims L7 correctly declined to touch this on a lane brief (agent configuration, not lane scope) and flagged it instead. Coordinator picking it up. CLAUDE.md carried a byte-identical copy of the stale README row the v0.54 cold review found, plus a third instance nobody had spotted: 1. header: "AArch64 (host-native, integer subset)" — the scalar float surface is complete as of v0.54. 2. crate map: "integer subset" — now i32/i64 core, complete scalar f32/f64, globals, call_indirect, bounds-checked linear memory. 3. VCR-VER-003 note: "AArch64 is N/A (no linear-memory ops in the integer subset)". The VERDICT is still right, the REASON is false — aarch64 has had bounds-checked linear-memory load/store since v0.52 (#865). It is N/A because it emits no data section and REFUSES data-carrying modules loudly (v0.53), so there is no served-vs-runtime image to compare. A correct conclusion resting on a false premise is the harder version of this defect: the sentence reads fine and the reasoning has rotted. Fourth copy of a list this project keeps duplicating (oracle, matrix row, CHANGELOG, CLAUDE.md). Generating the prose from the executable decline list is the standing fix; #911 is the nearest tracked version of it. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * docs(CHANGELOG): record the CLAUDE.md aarch64 de-staling, incl. the rotted premise 0f0c232 landed the CLAUDE.md half of the aarch64 doc fix but no release note. Adding one — and specifically calling out its third finding, which is the only one of the four that is not a plain stale string: VCR-VER-003's aarch64 N/A note gave a FALSE REASON for a TRUE verdict ("no linear-memory ops in the integer subset" — aarch64 has had bounds-checked linear-memory load/store since v0.52 #865). It is N/A because it emits no data section and refuses data-carrying modules loudly, so there is no served-vs-runtime image to compare. That failure mode deserves the note more than the two string copies do: a stale "integer subset" reads wrong and invites a check, whereas a correct conclusion resting on a rotted premise still reads fine, so nothing prompts one. Both underlying facts re-verified against the generated feature matrix before writing this. claim_check 37/37 (CLAUDE.md is pinned by three ledger entries; unaffected). 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 merged commit b371731 into main Jun 25, 2026
12 checks passed

avrabe deleted the ci/rv32-shift-fold-oracle-472 branch June 25, 2026 12:18

This was referenced Jul 2, 2026

flight_seam_differential.py broken on main: looks up 'func_0', absent since the #394 name work — dev-script drift not caught by CI #570

Closed

fix(repro): flight_seam_differential resolves symbols from symtab, not func_N (#570) #575

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

Navigation Menu

ci(vcr-oracle): CI-gate the RV32 immediate-shift-fold execution oracle (#472, #242) - #489