aarch64: VCR-SEL-005 third-backend parity gate + 13 measured op gaps closed (#851, #883) - #889
Merged
Conversation
Codecov Report❌ Patch coverage is 📢 Thoughts on this report? Let us know! |
…red op gaps (#851) Extend the cross-backend op-parity oracle to aarch64 (universe-complete, no-wildcard): the integer core is 3-way asserted (ARM/RV32/A64) with a measured 7-entry aarch64 divergence ledger, and the float/SIMD surface the ARM/RV32 oracle structurally excludes gets an aarch64-specific no-wildcard expectation table (aarch64's float lowering is not target-parameterized). Red-first + stale-entry + non-vacuity-floor companions included. The enumeration measured 20 integer-core gaps; 13 closed same-change: select (CSEL/FCSEL both files), drop, nop, i32.wrap_i64, i64.extend_i32_{s,u}, i32/i64.extend8/16/32_s (SXTB/SXTH/SXTW), fixed-memory memory.size + memory.grow (grow(0)==size, grow(n>0)->-1). Remaining ledgered: br_table, param-write homing (set/tee), globals substrate, memory.copy/fill. Encoder adds csel/csel64/fcsel_s/fcsel_d + sxtb/sxth/sxtb64/sxth64/sxtw, all pinned to clang -arch arm64 ground truth. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…45 ops + surface differential (#851) Matrix (gale's native MAP_JIT gate): +10 accepted ops (select i32 computed- cond + const-cond, i64 select, f32 select through the reinterpret wrapper incl. NaN both directions, extend8/16_s i32, i64 extend8/16/32_s, nop+drop) — 35→45 ops accepted, 91→119 native checks, PASS. New host-independent differential aarch64_surface_851_differential.py (unicorn vs wasmtime, 58 checks): select all four value types incl. NaN and -0.0 bit-carry, wrap/extends with POISONED upper argument bits (the AAPCS64 x-view hazard class), drop/nop, and fixed-memory memory.size/memory.grow against a (memory 2 2) min=max module so grow(n>0) failure is spec-FORCED parity, not an always-allowed divergence. growsize pins failed-grow-does- not-change-size. RED-first demonstrated against the v0.52.0 binary (every probe loud-declines, exit 1). Wired into the aarch64-oracle CI job. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…d/memory.size (#851) Closes the fourth instance of the #757/#758/#798 silent-miscompile class. The aarch64 object ships NO data section and NO startup, so a module carrying active data segments had its initialized region read ZEROS where WASM guarantees the segment bytes. Now a loud refusal on both the module and single-function paths, including the memory-0 non-const-offset segments that are legacy-dropped at decode (where the recorded reason is the only remaining trace). Op-surface additions, chosen from the VCR-SEL-005 third-backend complement rather than by hand: select (branchless CSEL/FCSEL, all four value types), drop/nop, i32.wrap_i64, i64.extend_i32_{s,u}, the five extend8/16/32_s sign extensions, and fixed-memory memory.size/memory.grow (grow(0) == size, grow(n>0) -> -1; growth failure is spec-permitted and keeps the static bounds limit sound). Doc honesty: the feature-matrix template now states plainly that x28 is a PRECONDITION, not emitted code -- synth emits no linker script, no data section and no prologue that establishes the linear-memory base; the embedder must. The decline list is now mechanically enumerated by the parity oracle instead of hand-maintained. Recovered from the lane's worktree after it hit a session limit; builds clean and the full workspace suite passes (129 suites, 0 failures). Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
The lane hit its session limit before the final cleanup pass, so cargo fmt had never run over the aarch64 encoder/selector and CLI changes. clippy doc-lazy-continuation on the parity gate's header: the "definitive mechanically-derived list" sentence follows a bullet list and was being read as a lazy continuation of the last bullet. It IS a new paragraph, so the fix is a blank doc line rather than the indentation clippy suggests. Regenerated docs/status/FEATURE_MATRIX.md + artifacts/status.json from the template (#805 says the coordinator regenerates once, lanes never hand-edit): aarch64_selector_ops 148 -> 161, the +13 ops the VCR-SEL-005 third-backend oracle measured as gaps and this lane closed. claim_check: 26/26 hold. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…53 op-list growth L6's #880 template-prose gate caught this on its first cross-lane interaction, which is exactly the drift it was built for. The pinned span ended " and `popcnt` (#851)"; this lane's op-surface work rewrote that sentence to ", `popcnt`, `select` ..., `drop`/`nop`, ...", so the verbatim pin no longer matched. Local runs on this branch passed 26/26 only because the branch predated L6 -- CI checks the MERGE, where L6's 34 pins meet this lane's edited template. Re-pinned to the capability-bearing span rather than the whole sentence. The ÷0 / INT_MIN÷−1 trap-guard parenthetical stays INSIDE the pin, so this is a narrowing that does not weaken the gate -- verified red-first: deleting the parenthetical from the template still reddens SYNTH-MATRIX-AARCH64-DIVREM-POPCNT (exit 1), restoring it returns green. 34/34 claims hold. Rebased onto main so the lane carries L6's pins. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe
force-pushed
the
feat/aarch64-residual-851
branch
from
July 29, 2026 17:49
898237a to
9622cfc
Compare
avrabe
added a commit
that referenced
this pull request
Jul 30, 2026
…CLOSED Cold review found the v0.53 assembly was about to ship the SAME defect class as v0.51 and v0.52, with a new twist: the ledger was defending it. F1 (BLOCK) — the FEATURE_MATRIX "Honest Summary" cited #881, #882 and #872 as open residuals. All three were CLOSED by lanes in THIS release. Root cause is a lane-ordering race: L6's doc-honesty commit landed 2026-07-29 15:28 and said "honest-summary residual examples now cite the actually-open issues (#881/#882/#872)" -- true when written; L1 closed #881 fourteen hours later. The doc-honesty lane ran FIRST and nobody re-swept after the fixes landed. The document had become self-contradictory: the summary said RV32 br_table still declines while the backend row three sections up said it lowers. Re-pointed at genuinely-open issues (#890, #851, #846), verified against `gh issue view`. F2 (BLOCK) — claims.yaml PINNED the stale "#881" verbatim, so `claim_check` reported 34/34 while green-confirming a false residual, and correcting the prose would have turned the gate RED. CLAUDE.md says never fix a red gate by loosening the ledger; this was the inverse -- a ledger entry that had gone false, so the gate protected the defect instead of catching it. The fix is structural, not a re-point: an ISSUE-NUMBER pin goes stale the moment the issue is fixed, because `verbatim` only asserts the phrase is PRESENT. This pin has now been wrong twice for exactly that reason (#782, then #881). It now pins the CAPABILITY GAP -- "single-precision FPUs", the i64-from-f32 decline that genuinely remains -- which becomes false precisely when the gap closes. Red-first verified: replacing the phrase reddens SYNTH-F32-F64-VFP (exit 1), restoring it returns green. F3 -- three of seven lanes had NO changelog entry, including L4/#872: a default-on soundness fix that MOVED SHIPPED BYTES (gust_poll 692->696, fact-spec 132->140). A user diffing v0.52->v0.53 output would have found no explanation. Added L1 (#885), L4 (#888) and L7 (#889) entries, and collapsed a duplicate `### Added` section that violated the Keep-a-Changelog structure the release process mandates. F4 -- README declared "No multi-memory" while the matrix (corrected this release) says P with a CI-wired differential. Multi-memory phase 1 shipped in v0.43 (#749); the README line was ~10 releases stale, so v0.53 would have shipped two documents disagreeing about a capability. F5 -- the #880 changelog entry claimed every pinned phrase is bound to its oracle AND that oracle's CI wiring. SYNTH-MATRIX-WCET-COMPOSITION has neither -- the sound-WCET-bound row, one of the most safety-load-bearing claims in the matrix, is the single exception. Named it rather than softening it away. F6 -- #872's real remaining hole (a mid-segment `Pop {…,PC}` the segment-local validator misses) and VCR-DEC-001's (a wrong-return-register rewrite accepted by `validate_cfg_rewrite` AND VCR-RA-003 both, caught only by execution) existed only in Rust doc-comments. Both now stated in the matrix and CHANGELOG: the release was simultaneously OVERSTATING what is open and OMITTING what is. claim_check 34/34, docs regenerated, render byte-fresh. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe
added a commit
that referenced
this pull request
Jul 30, 2026
* chore(release): v0.53.0 — "The last mile" (7 lanes) Version sweep: workspace + all 13 intra-workspace path-dep pins + MODULE.bazel + status.json, Cargo.lock refreshed to 0.53.0 (v0.52's cold review caught a stale lock; no CI job builds --locked, so this one is on the release process). Docs regenerated once at assembly per #805 -- lanes do not hand-edit generated artifacts. claim_check 34/34, check_version_pins OK. CHANGELOG headline added by the coordinator over the 8 lane-written entries. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L * fix(release): cold-review blockers — stop citing issues this release CLOSED Cold review found the v0.53 assembly was about to ship the SAME defect class as v0.51 and v0.52, with a new twist: the ledger was defending it. F1 (BLOCK) — the FEATURE_MATRIX "Honest Summary" cited #881, #882 and #872 as open residuals. All three were CLOSED by lanes in THIS release. Root cause is a lane-ordering race: L6's doc-honesty commit landed 2026-07-29 15:28 and said "honest-summary residual examples now cite the actually-open issues (#881/#882/#872)" -- true when written; L1 closed #881 fourteen hours later. The doc-honesty lane ran FIRST and nobody re-swept after the fixes landed. The document had become self-contradictory: the summary said RV32 br_table still declines while the backend row three sections up said it lowers. Re-pointed at genuinely-open issues (#890, #851, #846), verified against `gh issue view`. F2 (BLOCK) — claims.yaml PINNED the stale "#881" verbatim, so `claim_check` reported 34/34 while green-confirming a false residual, and correcting the prose would have turned the gate RED. CLAUDE.md says never fix a red gate by loosening the ledger; this was the inverse -- a ledger entry that had gone false, so the gate protected the defect instead of catching it. The fix is structural, not a re-point: an ISSUE-NUMBER pin goes stale the moment the issue is fixed, because `verbatim` only asserts the phrase is PRESENT. This pin has now been wrong twice for exactly that reason (#782, then #881). It now pins the CAPABILITY GAP -- "single-precision FPUs", the i64-from-f32 decline that genuinely remains -- which becomes false precisely when the gap closes. Red-first verified: replacing the phrase reddens SYNTH-F32-F64-VFP (exit 1), restoring it returns green. F3 -- three of seven lanes had NO changelog entry, including L4/#872: a default-on soundness fix that MOVED SHIPPED BYTES (gust_poll 692->696, fact-spec 132->140). A user diffing v0.52->v0.53 output would have found no explanation. Added L1 (#885), L4 (#888) and L7 (#889) entries, and collapsed a duplicate `### Added` section that violated the Keep-a-Changelog structure the release process mandates. F4 -- README declared "No multi-memory" while the matrix (corrected this release) says P with a CI-wired differential. Multi-memory phase 1 shipped in v0.43 (#749); the README line was ~10 releases stale, so v0.53 would have shipped two documents disagreeing about a capability. F5 -- the #880 changelog entry claimed every pinned phrase is bound to its oracle AND that oracle's CI wiring. SYNTH-MATRIX-WCET-COMPOSITION has neither -- the sound-WCET-bound row, one of the most safety-load-bearing claims in the matrix, is the single exception. Named it rather than softening it away. F6 -- #872's real remaining hole (a mid-segment `Pop {…,PC}` the segment-local validator misses) and VCR-DEC-001's (a wrong-return-register rewrite accepted by `validate_cfg_rewrite` AND VCR-RA-003 both, caught only by execution) existed only in Rust doc-comments. Both now stated in the matrix and CHANGELOG: the release was simultaneously OVERSTATING what is open and OMITTING what is. claim_check 34/34, docs regenerated, render byte-fresh. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --------- Co-authored-by: Claude <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.53 lane L7, re-scoped mid-flight after measuring that aarch64 was absent from the cross-backend op-parity gate (#883) — so nothing could say what armv8 was missing, and picking ops by hand was guesswork.
WasmOpvariants with no wildcard arm, so a new op cannot be added without classifying its aarch64 status.Closes #883, advances #851. Lane hit the session limit before final self-report; coordinator gating on CI.