aarch64: call_indirect (§4.4.8 traps) + globals + param homing (#851) - #899
Merged
Conversation
Adds the five A64 primitives lane L3 needs, each pinned to `clang -c -target aarch64-linux-gnu` ground truth in a unit test: blr xn — the indirect-call branch (call_indirect dispatch) adrp xd, <sym> — PC-relative page address (the data-region reach) cmp wn/xn, #imm12 — flags-only immediate compare (no scratch register) add xd,xn,wm,uxtw#s — scaled zero-extended index add (table slot address) `adrp`'s 21-bit page delta splits across TWO disjoint fields (immlo[30:29] + immhi[23:5]); a contiguous placement is silently wrong for every delta >= 1, so the split is pinned by a second test against capstone decodes of the literal words (0xF0000000 = adrp x0,#0x3000; 0x90000020 = #0x4000; 0xF0FFFFE0 = #-0x1000). Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
The substrate both lane-L3 features need, with NO new precondition. `DataBlob` — a synth-EMITTED `.data` (PROGBITS, ALLOC|WRITE, align 8) plus `STT_OBJECT` symbols into it. This is the honest answer to "where do WASM globals live on a backend that emits no startup and no linker script": the bytes ARE the initial values, shipped in the object; the linker places the section; code reaches it with `adrp`+`add :lo12:`. Contrast `x28` (the linear-memory base), which IS an embedder precondition — globals add no second one. RelocKind gains the three AArch64 kinds beyond CALL26: JUMP26 (282, the funcref-table `b func_N` trampolines), ADR_PREL_PG_HI21 (275) and ADD_ABS_LO12_NC (277) (the symbol-address pair). The builder's kind→type mapping has NO wildcard, and an unplaceable symbol now PANICS instead of silently dropping the relocation — an unrelocated `adrp #0` would address the wrong page (silent miscompile), where the old `continue` merely assumed it could not happen. `ElfFunction::is_object` types the `.text`-resident funcref table as OBJECT, not FUNC: it is branched INTO at slot+4, never called at slot+0. Byte-identity: an empty `DataBlob` reproduces the previous 5-section layout exactly (asserted by `empty_data_blob_is_byte_identical_to_the_data_free_builder`), so every globals-free module is unchanged. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…dispatch (#851) Three additions the aarch64 `call_indirect` + globals lowerings consume: * `DecodedModule::structural_type_class_ids()` — factored out of `call_indirect_guards`, which exposed the ids ONLY when its heterogeneous- table sidecar existed. The aarch64 dispatch type-checks UNCONDITIONALLY, so it needs them always. These are STRUCTURAL classes, not raw type indices: WASM type equality is structural, so `call_indirect (type 1)` must reach a function declared with a duplicate `type 0` (SS4.4.8) — comparing indices would trap where wasmtime calls. * `DecodedModule::funcref_region_class_ids()` — per-slot class id in the same contiguous order as `funcref_region_slots()`, 0 for null/unclassifiable. Storing this beside each slot makes ONE compare serve as both the SS4.4.8 type check and the null check (0 never equals a real class, which is >= 1). * `type_result_counts` on `DecodedModule` + `CompileConfig` — an indirect callee is known only by its static type, and `type_ret_i64/f32/f64` conflate void with i32, so the 0-vs-1 "is a value pushed back" distinction needs its own table. Plus `CompileConfig::a64_substrate_emitted`, FAIL-SAFE at `false`: the aarch64 selector will loud-decline globals and `call_indirect` unless the driver has actually emitted the `.data` globals image and the `.text` funcref table, so a driver that compiles bodies without emitting the regions cannot ship code addressing a symbol that is not there. Behavior unchanged: `call_indirect_guards` output is identical (pure refactor), and no consumer reads the new fields yet. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…851) `substrate::plan` materializes the globals `.data` image and the `.text` funcref table from decoded module state, and is called by BOTH aarch64 ELF drivers, so the regions the code addresses and the regions the object ships cannot disagree. PRECONDITION STATUS, stated plainly: neither region is one. Both are EMITTED BY SYNTH and reached with `adrp` + `add :lo12:` against a symbol the same object defines. That is deliberately unlike `x28` (the linear-memory base), which IS an embedder precondition — v0.53 made that explicit so the next feature would not quietly add a second, and this one does not. Using PC-relative addressing instead of a dedicated base register also sidesteps the #275/#717 collision class outright: there is no base register to collide with. Layouts. Globals: ONE 8-BYTE SLOT PER GLOBAL at `k*8` (NOT the ARM/#643 dense width-summed layout) — uniform slots stay naturally aligned for `ldr x`, where a dense layout puts an i64 at offset 4, and the offset stays a foldable constant. Funcref table: 8 bytes per slot, `[u32 structural class id][b func_N]`, null slots `[0][brk #0]`. Every unrepresentable shape LOUD-DECLINES with a machine reason rather than guessing (9 unit tests, decline text asserted): imported globals (value arrives at instantiation), a global with no decoded const initializer (float/v128/non-const expr), >2048 globals or a v128 slot, an unsized (growable imported) table, >4095 slots or class ids past the 12-bit guard immediates, and a table slot holding an imported function. The load-bearing one: an UNVERIFIABLE element segment declines instead of shipping a table. `funcref_region_slots` degrades such a table to all-null, which traps on every dispatch — that LOOKS conservative but is wrong in the other direction, trapping where wasmtime calls successfully. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
Three parity-gate entries flip Err(reason) -> lowering in this commit, so no gap claim outlives its gap: `global.get`, `global.set` (ledger entries deleted) and `call_indirect` (`a64_extended_surface` -> `Ok(())`). GLOBALS. `global k` lives at `__synth_globals + k*8` in the `.data` image synth EMITS; the address is formed `adrp`+`add :lo12:`. i32/f32 use the low word of the slot, i64/f64 the whole slot, and the size-scaled load/store immediate folds the offset. PRECONDITION STATUS: none. Unlike `x28` (the linear-memory base, which IS an embedder precondition), synth ships the region and its initial values; the linker places it. No base register, so nothing can collide with the linear-memory base the way #275/#717 did on ARM. CALL_INDIRECT. All three §4.4.8 traps are emitted, none inherited from `blr`: cmp w_idx,#size / b.lo +2 / brk out-of-range index adrp+add / add x16,x16,w_idx,uxtw#3 slot address (no base register) ldr w17,[x16] / cmp w17,#expected signature mismatch — and, because a b.eq +2 / brk null slot's class id is 0 and every real class is >=1, the null check too add x16,x16,#4 / blr x16 the slot's tail-branch trampoline The compared id is STRUCTURAL, so duplicate-but-identical types stay interchangeable; comparing raw type indices would trap where wasmtime calls. x16/x17 are the AAPCS64 IP0/IP1 scratch registers — outside both the value- stack temp pool (x9..x15) and the argument registers, so no guard can alias a live value. PARAM HOMING was the blocker: a non-leaf function referencing a parameter loud-declined, and a table index almost always IS a parameter, so `call_indirect` would only have dispatched on constants. Non-leaf functions now give EVERY local (params included) an 8-byte stack slot and store the incoming argument registers there at the prologue, reusing the non-param-local machinery verbatim. That restores both properties the decline protected: a post-call read hits the slot (which the call cannot clobber), and every value-stack entry is a temp again, so argument marshalling stays hazard-free. LEAF functions are untouched and byte-identical, so writing a param still declines there and that ledger entry stays valid; a non-leaf FLOAT param also still declines (homing a v-register needs an FP store this encoder lacks). Verified end-to-end, not just in unit tests: both features compile, LINK with a real `ld.lld`, and disassemble correctly — the linker relaxes `adrp`+`add` to `adr`, resolves `__synth_globals` to the emitted `.data` (0x29 = 41, 0x11f71fb04cb = 1234567890123), and the table lays out as `[1][b func_0] [1][b func_1] [2][b func_2] [0][brk #0]`. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
Two unicorn-vs-wasmtime differentials, both wired into the `aarch64-oracle` job in this commit with `set -o pipefail` and a non-zero-count grep (the #890 "oracle exists and runs nowhere" class). `aarch64_globals_851_differential.py` — 17 checks, 6 exports. Reads the INITIAL values before anything is written (a region shipping zeros fails), then runs the cases IN SEQUENCE against ONE region so a dropped or misdirected `global.set` shows up in the next `global.get`. i32 and i64 globals are interleaved, so a wrong slot stride shifts every later global. `aarch64_call_indirect_851_differential.py` — 35 checks (23 trap, 12 value), 6 exports. All three §4.4.8 traps, plus the direction an "always trap" lowering would hide: a structurally-DUPLICATE type must NOT trap. Both harnesses act as the LINKER — they place `.text` and `.data` on different pages and resolve ADRP page / ADD lo12 / JUMP26 themselves — so a wrong page delta, lo12, or trampoline displacement diverges rather than passing. RED-FIRST, and it earned its keep: the first version of the call_indirect oracle PASSED a compiler with the bounds guard removed. Past-the-end bytes read as class id 0, so the TYPE check trapped anyway and masked it. The fixture now declares TWO tables, making index 4 of table 0 land on table 1's fully valid, type-matching `$mul` slot — so only the bounds guard can trap there, and the same fixture makes a dropped per-table base offset return 30-vs-13 instead of agreeing by coincidence. Five injected miscompiles are now caught: weakened bounds guard -> differential red (4 BUG lines) dropped base offset -> differential red (2 BUG lines) removed type check -> differential red (6 BUG lines) null slot made callable -> differential red (2 BUG lines) dense globals layout -> differential red (4 BUG lines) One injection is NOT decidable by execution: a SIGNED bounds compare (`b.lt` for `b.lo`). Under emulation a negative index passes the signed guard and then faults on the unmapped scaled address, so it traps either way — but on real silicon that address can be mapped and the dispatch would branch into it. It is pinned instead by `call_indirect_guard_sequence_uses_an_unsigned_bounds_compare`, which asserts the whole guard sequence word-for-word (verified red: exit 101 when only the shipped code, not the expectation, is mutated). Plus fail-safe and scaling unit tests: both features decline under a default `ModuleCtx`, the slot offset is size-scaled per access width, and a global index past the region declines. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
) The FEATURE_MATRIX template row now says plainly what v0.52's cold review caught the last version of this doc getting wrong: the globals region and the funcref table are EMITTED BY SYNTH, not preconditions. `x28` (the linear-memory base) remains the ONE aarch64 precondition, and the row says so in those words, so a reader cannot come away thinking lane L3 added a second ambient input. The row also enumerates the new LOUD DECLINES by name rather than implying full coverage: imported globals, a global with no decoded const initializer, a non-leaf float param, a growable imported table, an unverifiable element segment, and a table slot holding an imported function. Two new `claims.yaml` pins hold those claims to evidence, both verified RED-FIRST: SYNTH-MATRIX-AARCH64-EMITTED-NOT-PRECONDITION — flipping the sentence to "are ALSO preconditions" reddens the gate; pinned to substrate.rs, the `.data` DataBlob, and the ADRP relocation kind actually being emitted. SYNTH-MATRIX-AARCH64-CALL-INDIRECT-TRAPS — unwiring either oracle from ci.yml reddens the gate, so the §4.4.8 trap claim cannot outlive its execution evidence. `aarch64_selector_ops` 161 -> 164 (global.get, global.set, call_indirect). Generated status files regenerated with the script (NOT hand-edited); the coordinator should re-run `--emit-status` once after the lane fan-in, since every aarch64 lane moves this counter. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
… failing (#851) Extends the CI-wired decline-matrix honesty oracle with the seven shapes lane L3 deliberately refuses, and upgrades the oracle itself: an entry may now pin the machine REASON its diagnostic must contain, because "it failed somehow" is not evidence that it failed for the right cause — a decline with the wrong reason is a different bug than a decline. imported global -> "imports 1 global" float global (no decoded const init) -> "no decoded constant initializer" v128 global -> (declines upstream at decode) growable imported table -> "no compile-time size" passive element segment -> "not statically verifiable" table slot holding an import -> "imported function" non-leaf FLOAT param -> "FLOAT parameter" 10/10 loud-decline, 6 with their reason asserted; the oracle also fails if NO entry carries a reason, so the new check cannot rot into a no-op. Also verified across the whole aarch64 gate set: all 14 unicorn oracles exit 0, `aarch64_calls_851.py` is 5/5 bit-identical, the `--relocatable` path emits the funcref table too, and gale's native acceptance matrix now reports 45 ops accepted / 119 native checks with an EMPTY declined frontier (baseline 32). Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…, #851) Two corrections from lane L1's oracle-wiring gate, applied to this lane's harnesses. 1. Both new oracles carry `# ci-status: wired`. VERIFIED non-inert: pointing the workflow step at a different filename makes the gate report "declares `wired` but NO workflow STEP runs it — the gate is INERT", so the declaration is checked against the parsed executable surface rather than taken on trust. 2. The CI steps now use `set -euo pipefail`, not bare `set -o pipefail`. `pipefail` alone leaves the step's exit status as its LAST command's, so a harness that printed FAIL and exited 1 could still green the step — the precise #890 class. The verdict is now taken three ways: the script's own exit status (via `-e`), a non-zero check-count grep, and the summary `RESULT: PASS` line. MUTATION-PROVEN, not assumed: perturbing the comparison inside the call_indirect harness (`exp` -> `exp + 1`, so a CORRECT compiler mismatches) makes the exact CI step body exit 1, and restoring it returns exit 0. That is the check L1 found `sret_decide_differential.py` failing — a gate that printed `MISMATCH <-- BUG` and exited 0. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
Contributor
Automated review for PR #899pulseengine/synth: Verdict: 💬 Comment Summary: The code has been modified to include new features and changes that need to be reviewed. Findings: 0 mechanical (rivet) · 1 from local AI model. Findings (1):
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 |
Codecov Report❌ Patch coverage is 📢 Thoughts on this report? Let us know! |
… globals) Both lanes extended the same aarch64 selector, matrix row and honesty ledger. Three of the six conflicts were semantic; git's textual resolution would have been wrong for two of them. 1. DECLINE ORACLE — both sides were STALE, in OPPOSITE directions. L3's copy still asserted `f64.floor`, `f32.floor` and `i64.trunc_f64_s` must FAIL to compile (L2 landed all three); main's copy still asserted `global.get` and `call_indirect` must FAIL (L3 landed both). Taking EITHER side verbatim would have shipped a gate asserting a decline for a shipping capability — the doc-honesty defect that has hit three consecutive releases, except here the error exists in NEITHER parent and is created by the merge itself. Resolved to the intersection re-derived from what actually ships (12 entries) and then CHECKED by running it: 12/12 loud-declined, 6 with their machine reason asserted, RESULT: PASS. 2. FEATURE_MATRIX aarch64 row — same shape. Kept L3's precondition prose and its call_indirect/globals lowering, removed the four float declines L2 closed (rounding, f32/f64 load/store, i64->float converts, trapping i64-target truncations), kept v128/SIMD + multi-memory from main's side. 3. A CLEAN textual merge that did not compile: L3 gave `select_typed_cf_calls` an 11th parameter (`&ModuleCtx`) and a third return (relocs); L2's `sel_mem_typed` test helper still used the 10-arg / 2-tuple form. NOTE `cargo build --workspace` PASSED — it does not compile `#[cfg(test)]` code — so only `cargo test` surfaced it. The helper needs no module context, so it passes `&ModuleCtx::default()`. Docs regenerated once at the merge (#805): aarch64_selector_ops reconciles both lanes at 184, claims 37/37, oracle-wiring gate clean. Verified: cargo test --workspace 130 suites / TEST-EXIT=0, fmt clean, frozen anchors 10/10, decline oracle PASS. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe
added a commit
that referenced
this pull request
Aug 5, 2026
…ad 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
avrabe
added a commit
that referenced
this pull request
Aug 5, 2026
`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
avrabe
added a commit
that referenced
this pull request
Aug 6, 2026
… 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>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
v0.54 lane L3. Closes the two largest remaining STRUCTURAL declines on aarch64. Lane was interrupted by an API error mid-flight and resumed; all 9 commits pushed.
What lowers now
call_indirect— a synth-emitted.text-resident funcref table (__synth_func_table), one 8-byte[u32 structural-class-id][b func_N]record per slot across all tables, null slots[0][brk #0]. All three WASM §4.4.8 traps are emitted inline, because A64'sblris total and gives none for free (the #709 more-total-than-WASM class): out-of-range index (unsigned compare), null slot, signature mismatch.The compared id is structural, not the raw type index — duplicate-but-identical types must stay interchangeable, and comparing type indices would trap where wasmtime calls.
x16/x17(AAPCS64 IP0/IP1) carry the slot address and class id, outside both the temp pool and the arg registers.Globals —
global.get/global.setfor i32/i64; each global is an 8-byte slot in a synth-emitted.dataregion (__synth_globals) carrying its decoded constant initializer.Param homing was the unlock. A non-leaf function referencing a parameter used to loud-decline — and a table index almost always is a parameter, so without this
call_indirectcould only dispatch on constants. Non-leaf functions now slot every local and store incoming arg registers at the prologue. Leaf functions are byte-identical, so writing a param still declines there and that ledger entry stays valid.Globals base register — stated plainly
There is no globals base register, and no new precondition. synth emits both regions into the object and reaches them with
adrp+add :lo12:that the linker resolves.x28(linear-memory base) remains the one aarch64 precondition; the FEATURE_MATRIX row now says so in those words and lists the globals region and funcref table as explicitly NOT preconditions. Pinned asSYNTH-MATRIX-AARCH64-EMITTED-NOT-PRECONDITION, red-first verified.PC-relative addressing also removes the #275/#717 base-register collision class by construction — there is no base register to collide with.
Trap evidence, including an oracle that was wrong
aarch64_call_indirect_851_differential.py: 35 checks, 23 traps, vs wasmtime under unicorn.The first version of this oracle passed a compiler with the bounds guard removed. Past-the-end bytes read as class id 0, so the type check trapped anyway and masked the missing guard. The fixture now declares two tables, so index 4 of table 0 lands on table 1's fully valid, type-matching
$mulslot — only the bounds guard can trap there, and a dropped per-table base offset returns 30-vs-13 instead of agreeing by coincidence. Five injected miscompiles now go red (weakened bounds guard, dropped base offset, removed type check, callable null slot, dense globals layout).One is not decidable by execution: a signed bounds compare traps under emulation via an unmapped fault but is unsound on silicon. Pinned instead by a word-for-word guard-sequence unit test (verified red, exit 101).
Still declining, with machine reasons
Imported global · global with no decoded const initializer (float/v128/non-const) · v128 global · growable imported table · unverifiable element segment · table slot holding an imported function · non-leaf float param · anything past the 12-bit guard immediates.
All seven are in the CI-wired decline oracle, which asserts the reason substring, not merely that compilation failed. The load-bearing one: an unverifiable element segment declines rather than shipping the all-null table the existing reconstruction produces — that would trap on every dispatch, i.e. conservative-looking but wrong in the other direction.
Numbers
gale's acceptance matrix 45 ops / 119 native checks, empty declined frontier (was 32).
aarch64_selector_ops161 → 164. Parity-gate ledger entries for globals deleted andcall_indirectflipped toOk(())in the same commit as the lowering.Both oracles carry
# ci-status: wired; CI steps useset -euo pipefail+ count grep +RESULT: PASS, mutation-proven.Coordinator: re-run
--emit-statusonce after fan-in (L2 moves the same counter). Expect conflicts incross_backend_op_parity.rs(aarch64_lowerssignature + newa64_module_ctx()) andCHANGELOG.md.Advances #851.