aarch64: br_table + value-carrying block/loop/if (#851, VCR-A64-CF-001) - #914
Merged
Conversation
…ue-carrying CF STEP 1 of v0.55 lane L6: the traceability artifact BEFORE the code, so the requirement states what must hold and the verification artifact states what proves it — rather than being retrofitted onto a landed diff. VCR-A64-CF-001 (sw-req, derives-from VCR-001, traces-to VCR-SEL-005) names the two largest entries in the mechanically-derived aarch64 decline complement: `br_table` (declined outright) and value-carrying `block`/`loop`/`if` (the #509 result-register-reconciliation class). It pins the SOUNDNESS-CRITICAL distinction up front — a `br` to a `loop` carries the loop's PARAMETER count, not its result count, so a `loop (result i32)` must NOT reconcile on its back-edge — and it names the residuals that stay declined (>16 targets, value-carrying br_table targets, block params, multi-value) rather than promising a coverage the lowering will not have. SWVER-022 (sw-verification, verifies VCR-A64-CF-001) states the both-directions evidence: a wasmtime-vs-unicorn/native execution differential over the br_table index lattice (default arm, at-bound, over-bound, 0xFFFFFFFF, mixed loop/block targets) plus the value-carrying loop back-edge, with a trap case so the harness cannot collapse to all-values; and the decline-honesty half pinned by name in `br_table_subshape_asymmetry_882`. `rivet validate` unchanged at the pre-existing baseline (52 errors, 104 warnings — none of them new); `--explain VCR-A64-CF-001` reports no diagnostics and both traceability rules satisfied. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…CF-001) The two largest entries left in the VCR-SEL-005 third-backend complement were STRUCTURAL, not arithmetic — and both made whole functions skip on `-b aarch64`. Selector goes 184 -> 185 ops. BR_TABLE lowers as a compare-and-branch CHAIN — `cbz w_idx, L0` for entry 0, `cmp w_idx, #i` + `b.eq L_i` per further entry, then an unconditional `b L_default`. Deliberately the same construction #882 chose for RV32, so the two backends stay reviewable against each other. The compares are the W view, so the UNSIGNED index rule holds exactly: only 0..len-1 match and every other index — including the "negative" i32s that denote huge unsigned values — reaches the DEFAULT. One table may MIX a backward loop header (resolved eagerly to a negative offset) with forward block ends (patched at `End`), because the chain dispatches on the TARGET FRAME's kind exactly as `br`/`br_if` already do. `patch_branch` grows a fourth placeholder kind (`b.<cond>`, 0x54…), rebuilt directly so the condition field survives the patch. VALUE-CARRYING FRAMES get a reserved reconciliation register pair (one GP, one FP — the arity side-table carries COUNTS only, so the result's register file is unknown at frame entry) withheld from the temp allocator for the frame's whole extent. Every edge into the join deposits there: `br`/`br_if` at the branch, the then-arm at `else`, the fall-through at `end`. i32/i64 ride `mov x`, f32/f64 ride `fmov d` (the same width argument `epilogue` already relies on). Two things were got right BY CONSTRUCTION rather than by test, and both are silent miscompiles if wrong: * A `br` to a LOOP label targets the HEADER and carries the loop's PARAMETERS, not its results. So a `loop (result T)` back-edge reconciles NOTHING. The frame carries `label_arity` SEPARATELY from `result_arity` and branch reconciliation is driven off the former; treating "the frame has a result" as "reconcile on every branch to it" stamps a garbage value into the result register every iteration. * The reservation is a BITMASK, not a value-stack entry. The value stack is consumed wholesale by the `call`/`call_indirect` argument marshalling (`stack.iter().enumerate()` + `stack.clear()`), so a placeholder pushed there would be marshalled as an argument and then erased. A separate mask is out of reach of every whole-stack consumer, and `epilogue(stack.last())` can never return a reservation. The four scratch-allocation sites that bypass `alloc_temp` (copysign, divrem, popcnt, memory.grow) consult it too. `reconcile_into` documents why no clobber window exists: the slot is reserved, so the move never destroys a live operand; and every write is IMMEDIATELY followed by the transfer to the join, so not even a `bl` (which clobbers the caller-saved x9..x15 pool) runs in between. On any other path the written value is dead and is re-written before that path reaches the join. THREE NAMED RESIDUALS replace two blanket declines — partial coverage with named gaps, not a claim that cannot be backed: * `br_table` past BR_TABLE_MAX_TARGETS (16 — the same threshold RV32 uses; the chain is O(n), PC-relative jump-table dispatch is the follow-up); * `br_table` with VALUE-CARRYING targets (the flat chain has no per-path edge to deposit a result on — refused conservatively when any targeted frame, default included, has non-zero label arity or a different entry height); * a block type with PARAMETERS or MULTI-VALUE results (the slot is ONE register). LEDGERS, both directions, same commit as the lowering: * the `br_table` whole-op entry is DELETED from `aarch64_known_divergences()` — the stale-entry check is what forced it — and the ledger's own "leaving the SEVEN below" prose is corrected to FOUR; * `br_table_subshape_asymmetry_882` grows an aarch64 leg pinning all three residuals BY NAME (via a new `aarch64_decline_reason`, so a bare `is_err()` from an unrelated probe artifact cannot satisfy the claim) AND asserting positively that a `(0,1)` value-carrying block now LOWERS, so the claim cannot quietly widen back into "typed blocks decline"; * `aarch64_m2_decline_538.py` swaps its `br_table` and `block (result f32)` entries for the three narrower residuals; * `feature_matrix.md.tmpl` states the capability and the residuals (the generated FEATURE_MATRIX + status.json are regenerated by the script, 185). The #554 float-honesty fixture MOVES again: it targeted a value-carrying f32-result block, which now lowers, so it re-points at a float construct that genuinely still declines — a NON-LEAF function reading an f32 parameter. EVIDENCE. `aarch64_brtable_blockvals_851_differential.py` (new, CI-wired with `set -euo pipefail` + non-zero counts in BOTH outcome classes): 84 checks over 17 exported functions vs wasmtime, under unicorn AND natively on an arm64 host. Per table it walks the index lattice — every arm, the index exactly AT the bound, one OVER it, and 0xFFFFFFFF — plus a table at exactly 16 targets, a table mixing loop and block targets in both orders, a `br_table` arm falling into a trap, and both join edges of every value-carrying frame. NON-VACUITY BY MUTATION, not assertion: * taking the join position BEFORE the fall-through's reconciliation move (so forward branches land ON it) -> 16 checks red; * an off-by-one in the chain constants -> 22 red, incl. switch16(16); * `result_arity` where `label_arity` belongs -> `loop_value` and `nested_value_frames` fail to compile at all. FROZEN-SAFE: 13 of the 14 aarch64 repro fixtures compile BYTE-IDENTICALLY to a v0.54.0 build; the one that differs is `aarch64_f32_unsupported_554`, and it differs exactly because its declined function now lowers. ARM/RV32 goldens 10/10. All 16 aarch64 CI oracles green; `cargo fmt --check`, `clippy --workspace --all-targets -D warnings` and `cargo test --workspace` all exit 0. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…uted claim `reconcile_into` documents that a call cannot clobber a live reconciliation slot, even though `bl` clobbers the caller-saved x9..x15 pool the slot lives in. Nothing in the suite executed that claim: no case had a `call` inside a value-carrying frame. It was the only documented soundness property in this change with no oracle behind it. Two cases close it. `block_over_call` deposits 7 on the `br_if` edge and calls `$three` on the fall-through; `if_value_over_call` does the same across the `else` deposit rather than the `end` one. Cond nonzero -> the branch's 7 must survive (the `bl` never runs); cond zero -> the call's 3 must come back (the clobber must be invisible, because the deposited value is dead on that path). Both shapes also force the HOMED-PARAM path (non-leaf + reads a param), which no other value-carrying case here touches. The first attempt HUNG rather than failed, which is worth recording: `bl func_N` is emitted as a placeholder plus an `R_AARCH64_CALL26` a linker would resolve, so executing the object unlinked makes every call branch to ITSELF. `load()` now APPLIES those relocations — which also turns the emitted relocation into part of what this oracle checks — and the count is asserted non-zero in the summary line and in CI, because if the relocations vanished the calls would silently become self-branches and the clobber claim would go untested while the gate stayed green. The native forked child also gets a `signal.alarm(20)` so a runaway branch FAILS instead of hanging the parent: a gate that never reports is worse than a red one. 84 -> 88 checks, 17 -> 19 exported functions, 2 direct-call relocations applied. Verdict unchanged: PASS. Every CI grep assertion in the new step was re-verified locally against the real log. Also ran gale's `aarch64_matrix.sh` acceptance gate (the separate `aarch64-native-matrix` job, which auto-flips declined->verified the day a lowering lands, so this change is exactly such a day): 61 ops, 355 native checks, empty declined frontier, exit 0 — unchanged, no op flipped unexpectedly. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
The `aarch64` job's header comment still described the decline-matrix probe as asserting `br_table`, globals, `call_indirect` and value-carrying blocks — all four of which now SHIP (v0.54 L3 and this lane). A comment is not a gate, but this is the exact doc-honesty defect the v0.54 fan-in hit from the other direction, and it sits directly above the step whose whole purpose is decline honesty. Rewritten to name the narrower residue the probe actually asserts today, with the rule that an entry leaves the list the day its lowering lands. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
Codecov Report❌ Patch coverage is
📢 Thoughts on this report? Let us know! |
# Conflicts: # CHANGELOG.md
Fan-in resolution, all three conflicts kept-both: - CHANGELOG.md: union of both sides' [Unreleased] bullets, count-asserted. - artifacts/sw-verification.yaml: main already owns SWVER-022 (L7's VCR-RA-004 artifact), so this lane's renumbers to SWVER-024. The two in-flight lanes take 023 and 024 so the second to merge cannot collide again.
# Conflicts: # CHANGELOG.md
Fan-in round 3. Conflicts kept-both: - CHANGELOG.md — 2 blocks, 7 bullets, count-asserted. - artifacts/sw-verification.yaml — NO id collision this time: main carries L3's SWVER-023 and this lane holds SWVER-024, because both were renumbered off 022 before either merged. The pre-emptive split is why this was mechanical. `Claim Check` was red for the same structural reason it was on #918: this lane's own oracle predates the rule that every oracle declare what it attests, so `aarch64_brtable_blockvals_851_differential.py` carried a `# ci-status:` but no `# ci-checks:`. No lane did anything wrong — L5 changed the requirement while this one was in flight. Floor MEASURED through the driver, not guessed: measured=88 emulations=88 wasmtime_calls=88 compiles=1 (88 checks — 2 trap, 86 value — across 19 exported functions) The step now routes through `scripts/oracle_run.py`, so it reports to the per-job ledger like every other wired oracle; its existing tee+grep non-vacuity assertions are unchanged and still bind. Totals 135 -> 136 oracles, 295,333 -> 295,421 entries, updated on ALL THREE pinned surfaces (ORACLE_WIRING.md, ci.yml, and the FEATURE_MATRIX template — the third one only became gate-backed earlier in this release, when the ledger was found reporting 42/42 HOLD over a matrix carrying a stale number). Local: 43/43 claims hold; 160 repro scripts, 0 UNDECLARED, emulations 136 / floor 295421. Refs #851, #910
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.55 lane L6. The two largest entries left in the VCR-SEL-005 third-backend complement were structural, not arithmetic — and both made whole functions skip on
-b aarch64. The aarch64 selector goes 184 → 185 ops.What lowers now
br_table— a compare-and-branch chain:cbz w_idx, L0for entry 0,cmp w_idx, #i+b.eq L_iper further entry, then an unconditionalb L_default. Deliberately the same construction #882 chose for RV32, so the two backends stay reviewable against each other. The compares are the W view, so the UNSIGNED index rule holds exactly: only0..len-1match, and every other index — including the "negative" i32s that denote huge unsigned values — reaches the default. One table may mix a backward loop header (resolved eagerly) with forward block ends (patched atEnd).patch_branchgrows a fourth placeholder kind (b.<cond>,0x54…), rebuilt directly so the condition field survives the patch.Value-carrying
block/loop/if— the frame reserves a reconciliation register pair (one GP, one FP; the arity side-table carries counts only, so the result's register file is unknown at frame entry) and withholds it from the temp allocator for the frame's whole extent. Every edge into the join deposits there —br/br_ifat the branch, the then-arm atelse, the fall-through atend— so the result is in one register on every path. i32/i64 ridemov x, f32/f64 ridefmov d.Two things got right by construction, not by test
Both are silent miscompiles if wrong:
brto alooplabel carries the loop's PARAMETERS, not its results. So aloop (result T)back-edge reconciles nothing. The frame carrieslabel_arityseparately fromresult_arity, and branch reconciliation is driven off the former. Treating "the frame has a result" as "reconcile on every branch to it" stamps a garbage value into the result register every iteration.call/call_indirectargument marshalling (stack.iter().enumerate()+stack.clear()), so a placeholder pushed there would be marshalled as an argument and then erased. The four scratch-allocation sites that bypassalloc_tempconsult the mask too.reconcile_intodocuments why no clobber window exists: every slot write is immediately followed by the transfer to the join, so not even abl(which clobbers the caller-savedx9..x15pool) runs in between. That claim is executed, not just asserted — seeblock_over_call/if_value_over_callbelow.What still declines, and why
Three named residuals replace two blanket declines:
br_tablepastBR_TABLE_MAX_TARGETS(16)br_tablewith VALUE-CARRYING targetsLedgers — same commit as the lowering, both directions
br_tablewhole-op entry is deleted fromaarch64_known_divergences(); the stale-entry check is what forced it. The ledger's own "leaving the SEVEN below" prose is corrected to FOUR.br_table_subshape_asymmetry_882grows an aarch64 leg pinning all three residuals by name (via a newaarch64_decline_reason, so a bareis_err()from an unrelated probe artifact cannot satisfy the claim) and asserting positively that a(0,1)value-carrying block now lowers — the claim cannot quietly widen back into "typed blocks decline".scripts/repro/aarch64_m2_decline_538.pyswaps itsbr_tableandblock (result f32)entries for the three narrower residuals.scripts/templates/feature_matrix.md.tmplstates the capability and the residuals.Evidence
scripts/repro/aarch64_brtable_blockvals_851_differential.py(new, CI-wired withset -euo pipefail+ non-zero counts asserted in BOTH outcome classes and on the applied-relocation count): 88 checks over 19 exported functions vs wasmtime, under unicorn and natively on an arm64 host. Per table it walks the index lattice — every arm, the index exactly AT the bound, one OVER it,0xFFFFFFFF— plus a table at exactly 16 targets, tables mixing loop and block targets in both orders, abr_tablearm falling into a trap, and both join edges of every value-carrying frame including a value-carrying loop's back-edge. Two cases put ablinside a value-carrying frame; the harness applies theR_AARCH64_CALL26relocations itself, so the emitted relocation is part of what is checked rather than a hang, and the native child carries asignal.alarmso a runaway branch fails instead of hanging the gate.Non-vacuity by MUTATION, not assertion:
switch16(16)result_aritywherelabel_aritybelongs (the loop back-edge bug)loop_value+nested_value_framesfail to compile at allFrozen-safe: 13 of the 14 aarch64 repro fixtures compile byte-identically to a v0.54.0 build; the one that differs is
aarch64_f32_unsupported_554, and it differs exactly because its declined function now lowers. A void frame reserves no register and emits no reconciliation move, so the property holds by construction. ARM/RV32 frozen goldens 10/10.Gates by real exit code:
cargo fmt --all --check= 0,cargo clippy --workspace --all-targets -- -D warnings= 0,cargo test --workspace= 0 (130 test binaries), all 16 aarch64 unicorn oracles PASS, gale'saarch64_matrix.shacceptance gate = 0 (61 ops / 355 native checks / empty declined frontier — unchanged, no op flipped unexpectedly),claim_check.py37/37,oracle_wiring_check.pyclean.Traceability:
VCR-A64-CF-001(sw-req) +SWVER-022(sw-verification) landed before the code;rivet validateunchanged at the pre-existing baseline.Note for the coordinator (#805)
This lane commits regenerated
docs/status/FEATURE_MATRIX.md+artifacts/status.json. That was forced, not chosen:claim-checkis a required check and goes red on generated-artifact staleness the moment the template changes. Expect a conflict on those two files at fan-in — the resolution ispython3 scripts/claim_check.py claims.yaml --emit-statusafter merging, never a manual merge of the rendered text.🤖 Generated with Claude Code
https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L