feat(aarch64): complete the scalar float surface — rounding, FP memory, i64 converts, GUARDED i64 truncations (#851)

[avrabe]

v0.54 lane L2. Closes the four classes v0.53's VCR-SEL-005 third-backend
op-parity oracle enumerated as Err(reason) in a64_extended_surface. Every
gate entry was flipped Err → Ok(()) in the same commit as the lowering
and each now-unused reason constant deleted — no wildcard arm, nothing moved to
StructurallyExcluded. After this the aarch64 extended-surface gate carries only
SIMD / multi-memory / call_indirect: the scalar float surface is complete.

class	lowering	gate entries flipped
ROUNDING	FRINT{P,M,Z,N} s/d	8
FP_MEM	SIMD&FP LDR/STR s/d, bounds-checked	4
I64_TO_FP	SCVTF/UCVTF x-forms	4
TRAP_TRUNC_I64	domain-guarded x-form FCVTZ{S,U}	4

The soundness-critical half

A64 FCVTZS/FCVTZU are more total than WASM: NaN → 0, out of range →
saturate to INT64_MIN/MAX, where §4.3.3 requires a trap. So the trapping
i64 truncations go behind the #709 two-sided guard, and the boundary constants
are justified rather than copied from the i32 rows:

• signed lower bound = inclusive −2^63 (b.ge) in both formats: −2^63 is
  exactly representable and truncates to a legal INT64_MIN; a strict bound
  would trap it. This differs from the i32/f64 row's strict −(2^31)−1, and
  for a concrete reason: the f64 ULP at 2^63 is 2048, so no f64 exists in
  (−2^63−1, −2^63), whereas −2147483648.5 does exist near 2^31.
• unsigned lower bound = strict −1.0 (b.gt): trunc_u(-0.5) = 0 is legal.
• upper bounds 2^63 / 2^64 exclusive — not the 2^32 the i32 forms use, which
  would trap every legal value above 4294967295.

FRINTN being round-to-nearest-ties-to-even (what WASM nearest requires,
vs FRINTA's ties-away) is checked, not assumed: the halfway table
0.5→0, 1.5→2, 2.5→2, 3.5→4 and negatives fails under FRINTA.

FP loads/stores go through the same form_ea as the integer accesses, so
they inherit v0.52's #865 software bounds check verbatim, width-aware: address
65532 is in-bounds for f32.load and out for f64.load on a one-page memory.

Evidence

scripts/repro/aarch64_float_completion_851_differential.py — 662 checks,
142 of them trap cases, bit-exact vs wasmtime under two oracles: unicorn
(x28 = linmem base) and native arm64 (each call in a forked child so an expected
SIGTRAP is observed). NaN compared NaN-aware per §4.3.3; values, traps and ±0
signs bit-for-bit. The static expect-trap column is validated against wasmtime
first, so the table cannot drift vacuous.

Proven non-vacuous by mutation, both directions of wrong:

mutation	result
one guarded convert → bare saturating	18 failures (A64=0x7fffffffffffffff wasmtime=TRAP)
signed lower bound → off-by-one strict	4 failures (A64=TRAP wasmtime=0x8000000000000000)

CI-wired in the same commit with set -o pipefail + a numeric assertion on the
check and trap counts (#890 — v0.53 found three oracles that ran nowhere).

gale's matrix: 45 → 61 ops accepted, 119 → 355 native checks, declined
frontier now EMPTY, including on-silicon trap agreement (its new trap64
helper is itself red-first verified: the same mutation makes it exit 1 with 7
named miscompiles).

Two things I had to move, not delete

• f32.{ceil,floor,trunc,nearest} were dropped at the decoder, so the whole
  function loud-SKIPPED before any backend saw it. Un-dropped — which means
  ARM32 must now LOUD-DECLINE them: its legacy pseudo-op is an FPSCR-RMode +
  VCVT.S32.F32 + VCVT.F32.S32 round-trip through i32, and VCVT
  saturates, so ceil(1e30) → 2147483648.0, ceil(±inf) → a finite bound,
  ceil(NaN) → 0.0. That thumb-2 f32: i32.trunc_f32_s/u silently saturate instead of trapping on NaN/Inf/out-of-range (bare VCVT, no guard) — WASM Core §4.3.3 soundness bug #709-class miscompile was latent only because the op
  was undecodable; declining keeps it latent instead of shipping it. Exactly the
  move Feature challenge: add an aarch64 (host-native) backend so output runs and debugs natively on arm64 dev machines #538 m4 made for f32.min/max. Follow-up: a real VRINT.F32 lowering.
• The -b aarch64 silently miscompiles f32 ops (emits 'mov w0,w1' / drops constants) instead of erroring like other unsupported milestone-1 ops #554 honesty fixture used f64.floor as its "deliberately declined
  float op" — a claim this PR invalidates. Repointed at a value-carrying
  (f32-result) block (still decoded, still declined at the selector) and the
  assertion strengthened: stderr must come from the aarch64 selector and
  name the reason, not merely contain "unsupported". The decline-matrix oracle
  likewise now pins the structural declines (7/7 loud).

Gates (real exit codes, no | tail && echo OK)

cargo test --workspace 0 · clippy --workspace --all-targets -D warnings 0 ·
fmt --check 0 · frozen anchors 10/10 (no ARM golden moved — the four
rounding ops were undecodable, so no frozen fixture contains one) ·
claim_check 34/34 · all 12 pre-existing aarch64 oracles still green.

Coordinator (#805): artifacts/status.json +
docs/status/FEATURE_MATRIX.md were regenerated mechanically
(aarch64_selector_ops 161 → 181) so claim-check is green here. Please re-run
--emit-status once after fan-in; those two files will conflict with any
other lane that moves a counted claim. The template
(scripts/templates/feature_matrix.md.tmpl) is edited as a source file — its
aarch64 Declines list no longer names the four now-false claims.

Left declined, honestly

call_indirect, import calls, value-carrying blocks/loops, br_table, writing
a PARAM local, globals, memory.copy/fill, v128/SIMD, multi-memory, >8
args, float-result callees — all still loud, all still enumerated by the same
oracle.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[avrabe]

Coordinator corrections applied (L1 / #890) — and one of them was a real defect here

1. The gate I added could pass while its own oracle failed. Not hypothetical — reproduced against a stub that prints RESULT: FAIL (1) and exits 1:

step shape	exit	verdict
set -o pipefail (what I shipped in 7cb8771)	0	🟢 GREEN while the oracle FAILED
set -euo pipefail + grep -q '^RESULT: PASS'	1	🔴 correctly RED

Without -e the step's status is that of the last command, and my trailing count assertions pass on a failing run (a failing oracle still prints its full case counts). Fixed in 193958c: explicit set -euo pipefail (not relying on the runner's default flags) plus the verdict taken from the script's own summary line rather than exit 0. Re-verified green against the real oracle — 662 checks, 142 trap cases.

2. # ci-status: wired added to scripts/repro/aarch64_float_completion_851_differential.py (line 2; module docstring intact).

Also re-ran the unicorn-only path (what aarch64-oracle executes on ubuntu-latest, where the native leg is skipped): 662/662, 142 trap cases — well clear of the ≥300 / ≥40 floors.

---

Adjacent finding, deliberately NOT fixed here (lane containment)

Auditing every run: block in ci.yml for the same pattern turns up three more bare-pipefail steps, all in trap-semantics-oracle:

• Run gpio-thin size + mmio execution oracle (#846/#879, cortex-m3)
• Run VFP spill execution oracle (#881, cortex-m7dp)
• Run VCR-DEC-001 join-allocator execution differential (#242, thumb2)

They are materially safer than mine was — each one's last command is a grep on a success marker, so a missing marker does redden the step. The residual hole is narrower: an oracle that prints its success marker and then fails a later sub-check and exits non-zero would still go green.

Leaving them to L1/#890 rather than touching another lane's steps in a file we both edit. Flagging so the decision is explicit, not an oversight.

[codecov]

Codecov Report

❌ Patch coverage is 98.77301% with 4 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-core/src/wasm_decoder.rs	0.00%	4 Missing ⚠️

📢 Thoughts on this report? Let us know!