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

.github/workflows/ci.yml

@@ -472,8 +472,12 @@ jobs:
     # WASM traps must TRAP under emulation, in-range must match bit-exactly)
     # + min/max NaN/±0 matrix + copysign. #851 added div/rem (SDIV/UDIV+MSUB
     # with WASM ÷0 + INT_MIN/-1 trap guards, execution-verified), popcnt (SIMD
-    # CNT/ADDV), and f64<->i64 reinterpret; the decline-matrix probe now
-    # asserts only rounding + i64<->float conversions still LOUD-decline.
+    # CNT/ADDV), and f64<->i64 reinterpret. v0.54 L2 completes the SCALAR float
+    # surface — rounding (FRINT), f32/f64 load/store (bounds-checked), i64->
+    # float converts, and the DOMAIN-GUARDED trapping i64-target truncations —
+    # so the decline-matrix probe now asserts the STRUCTURAL declines
+    # (call_indirect, br_table, param writes, globals, bulk memory,
+    # value-carrying blocks, SIMD) still LOUD-decline.
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v7
@@ -521,6 +525,38 @@ jobs:
         # AAPCS64 x-view hazard), drop/nop, fixed-memory size/grow parity
         # against a min=max module (growth failure is spec-forced there).
         run: SYNTH=./target/debug/synth python scripts/repro/aarch64_surface_851_differential.py
+      - name: Run v0.54 L2 float-completion oracle (#851 rounding / i64 converts / GUARDED i64 trunc / FP mem)
+        # The four classes the VCR-SEL-005 third-backend parity gate listed as
+        # Err(reason). The soundness-critical one is TRAP_TRUNC_I64: A64
+        # FCVTZ{S,U} SATURATE where WASM §4.3.3 TRAPS, so the harness runs a
+        # FULL boundary table (both sides of ±2^63 / 2^64, the nearest float
+        # inside/outside each bound, ±0, ±inf, NaN) and requires every trap
+        # case to ACTUALLY TRAP. Rounding is compared bit-exactly over a
+        # halfway table, which is what makes the "FRINTN is ties-to-EVEN"
+        # claim real rather than assumed.
+        #
+        # ANTI-VACUITY (#890). `set -euo pipefail`, NOT bare `pipefail`: with
+        # pipefail ALONE the step's exit status is that of the LAST command, so
+        # an oracle that printed FAIL and exited 1 still went GREEN. `-e` is
+        # what makes the failing pipeline abort the step — and it is stated
+        # explicitly here rather than left to the runner's default shell flags.
+        #
+        # The verdict is then taken from the script's OWN summary line, not
+        # from exit 0 alone, and the counts are asserted non-collapsed: an
+        # oracle that quietly stops exercising anything — or that loses the
+        # out-of-range half of the #709 boundary table, which is this gate's
+        # entire purpose — must go RED.
+        run: |
+          set -euo pipefail
+          SYNTH=./target/debug/synth python scripts/repro/aarch64_float_completion_851_differential.py \
+            | tee /tmp/a64_floatdiff.log
+          grep -q '^RESULT: PASS' /tmp/a64_floatdiff.log
+          grep -Eq '^[0-9]+ wasmtime cases \([0-9]+ trap cases\)' /tmp/a64_floatdiff.log
+          n=$(sed -n 's/^\([0-9]*\) wasmtime cases.*/\1/p' /tmp/a64_floatdiff.log)
+          t=$(sed -n 's/^[0-9]* wasmtime cases (\([0-9]*\) trap cases).*/\1/p' /tmp/a64_floatdiff.log)
+          echo "float-completion oracle ran $n checks, $t of them trap cases"
+          [ "$n" -ge 300 ]
+          [ "$t" -ge 40 ]
       - name: Run decline-matrix honesty oracle
         run: SYNTH=./target/debug/synth python scripts/repro/aarch64_m2_decline_538.py
 

CHANGELOG.md

@@ -141,6 +141,68 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   divergent call-containing functions) which the CI wiring re-asserts from the
   `CALLSHAPES=` summary field (#890). 56/56 checks, 19 engaged functions of which
   6 are call shapes.
+- **aarch64: the scalar float surface is complete (#851).** v0.53's VCR-SEL-005
+  cross-backend op-parity oracle was extended to aarch64 as a third backend and
+  made universe-complete over the `WasmOp` universe with no wildcard arm; its 31
+  `Err(reason)` entries were a mechanically-derived work list. This closes four
+  of those classes, each with the gate entry flipped `Err`→`Ok(())` **in the same
+  commit** and the now-unused reason constant deleted — a gap claim must not
+  outlive the gap:
+  - **Rounding** — `f{32,64}.{ceil,floor,trunc,nearest}` lower to one
+    `FRINT{P,M,Z,N}` each, with the rounding mode pinned in the OPCODE rather
+    than read from `FPCR.RMode`, so the result cannot depend on ambient
+    embedder state. `nearest` is `FRINTN` = round-to-nearest-**ties-to-even**
+    (WASM §4.3.3), **checked** against a halfway table (0.5→0, 1.5→2, 2.5→2,
+    3.5→4 and negatives) that a ties-away `FRINTA` lowering fails.
+  - **f32/f64 linear memory** — the SIMD&FP `LDR`/`STR` `s`/`d` forms, routed
+    through the SAME address path as the integer accesses, so an FP access is
+    **bounds-checked by default** (#865) and traps exactly where wasmtime
+    traps. The access width is folded into the compile-time bound, so address
+    65532 is in-bounds for `f32.load` and out-of-bounds for `f64.load` on a
+    one-page memory.
+  - **i64→float converts** — `f{32,64}.convert_i64_{s,u}` via the `x`-form
+    `SCVTF`/`UCVTF`, with the round-to-nearest-even behaviour past 2^24 / 2^53
+    pinned by execution.
+  - **Trapping i64-target truncations** — `i64.trunc_f{32,64}_{s,u}` behind the
+    #709 domain guard. This is the soundness-critical one: A64 `FCVTZ{S,U}` are
+    **more total than WASM** — NaN yields 0 and out-of-range SATURATES to
+    `INT64_MIN`/`MAX` where §4.3.3 requires a TRAP. Verified against a full
+    boundary table rather than spot checks: both sides of ±2^63 and 2^64, the
+    nearest representable float strictly inside and strictly outside each
+    bound, ±0, ±inf and NaN. The signed lower bound is the INCLUSIVE −2^63
+    (exactly representable, and truncating to a legal `INT64_MIN`); note this
+    differs from the i32/f64 row's strict −(2^31)−1 for a concrete reason — the
+    f64 ULP at 2^63 is 2048, so no f64 exists between −2^63−1 and −2^63.
+  - Evidence: `scripts/repro/aarch64_float_completion_851_differential.py`,
+    662 checks (142 of them trap cases) bit-exact vs wasmtime under unicorn
+    **and** natively on arm64 (every native call in a forked child so an
+    expected `SIGTRAP` is observed). CI-wired in the same commit with
+    `set -o pipefail` and an assertion that the check and trap counts are
+    non-zero, so an oracle that stops exercising anything goes red (#890).
+    Proven non-vacuous by mutation: dropping the guard (18 failures) and
+    making the signed lower bound off-by-one strict (4 failures) both go red.
+  - gale's acceptance matrix (`scripts/repro/aarch64_matrix.sh`) grew 16 ops
+    (45→61 accepted, 355 native checks) including on-silicon trap agreement for
+    the guarded truncations; its **declined frontier is now empty**.
+
+### Changed
+
+- **`f32.{ceil,floor,trunc,nearest}` are decoded** instead of dropped at
+  `_ => None`, so a module using them no longer loud-SKIPS the whole function
+  before any backend sees it.
+- **ARM32 now LOUD-DECLINES the four f32 rounding ops.** Its legacy
+  `ArmOp::F32{Ceil,Floor,Trunc,Nearest}` pseudo-op is an FPSCR-RMode +
+  `VCVT.S32.F32` + `VCVT.F32.S32` round-trip **through a 32-bit integer**, and
+  VCVT saturates: `ceil(1e30)` would return 2147483648.0, `ceil(±inf)` a finite
+  bound and `ceil(NaN)` 0.0, where WASM returns 1e30 / ±inf / NaN. That
+  #709-class miscompile was unreachable only because the decoder dropped the
+  op; declining keeps it latent rather than shipping it. A real `VRINT.F32`
+  lowering (the f32 twin of the shipping f64 path) is the follow-up.
+- The aarch64 decline-matrix oracle and the #554 float-honesty fixture were
+  repointed at constructs that are still genuinely declined (structural ones:
+  `call_indirect`, `br_table`, param writes, globals, bulk memory,
+  value-carrying blocks, SIMD), and the #554 assertion was strengthened to
+  require the diagnostic to come from the aarch64 SELECTOR and name its reason.
 
 ## [0.53.0] - 2026-07-30
 

artifacts/status.json

@@ -1,5 +1,5 @@
 {
-  "aarch64_selector_ops": 161,
+  "aarch64_selector_ops": 181,
   "arm_refinement_assumed_connection": 5,
   "arm_semantics_axioms": 72,
   "backends": [

crates/synth-backend-aarch64/src/encoder.rs

@@ -878,6 +878,118 @@ pub fn ucvtf_d_from_w(rd: FReg, rn: Reg) -> u32 {
     fp2(0x1E63_0000, rd, rn)
 }
 
+// ---------------------------------------------------------------------------
+// v0.54 L2 (#851) — the 64-bit-SOURCE integer→float converts (`sf` = 1). Same
+// opcodes as the `w`-source forms above with bit 31 set, exactly as the
+// `sdiv`/`sdiv64` pair. All four are TOTAL (every i64 has a nearest f32/f64;
+// f32 rounds, f64 rounds above 2^53 — both round-to-nearest-even, which is
+// WASM §4.3.2 `convert` semantics). Ground truth from
+// `clang -target aarch64-linux-gnu` (see `fp_convert_i64_encodings_match_clang`).
+// ---------------------------------------------------------------------------
+
+/// `scvtf sd, xn` — signed i64 → f32 (`f32.convert_i64_s`). Total.
+pub fn scvtf_s_from_x(rd: FReg, rn: Reg) -> u32 {
+    scvtf_s_from_w(rd, rn) | SF64
+}
+/// `ucvtf sd, xn` — unsigned i64 → f32 (`f32.convert_i64_u`). Total.
+pub fn ucvtf_s_from_x(rd: FReg, rn: Reg) -> u32 {
+    ucvtf_s_from_w(rd, rn) | SF64
+}
+/// `scvtf dd, xn` — signed i64 → f64 (`f64.convert_i64_s`). Total.
+pub fn scvtf_d_from_x(rd: FReg, rn: Reg) -> u32 {
+    scvtf_d_from_w(rd, rn) | SF64
+}
+/// `ucvtf dd, xn` — unsigned i64 → f64 (`f64.convert_i64_u`). Total.
+pub fn ucvtf_d_from_x(rd: FReg, rn: Reg) -> u32 {
+    ucvtf_d_from_w(rd, rn) | SF64
+}
+
+// ---------------------------------------------------------------------------
+// v0.54 L2 (#851) — `FRINT<mode>`, the float→float round-to-integral family
+// that implements WASM `ceil`/`floor`/`trunc`/`nearest`.
+//
+// SEMANTICS (why these four and not the FPCR-rounding `FRINTI`/`FRINTX`): each
+// FRINT variant pins its rounding mode in the OPCODE, so the lowering does not
+// depend on the ambient FPCR.RMode the embedder happens to have set.
+//   * `FRINTP` = round toward +inf   = WASM `ceil`
+//   * `FRINTM` = round toward -inf   = WASM `floor`
+//   * `FRINTZ` = round toward zero   = WASM `trunc`
+//   * `FRINTN` = round to nearest, TIES TO EVEN = WASM `nearest` (§4.3.3
+//     `fnearest` is roundTiesToEven — NOT ties-away, which would be `FRINTA`).
+// All four are TOTAL (no WASM trap, no A64 exception): ±inf and NaN pass
+// through (NaN quieted), and -0.5 <= x < 0 yields -0.0 for `nearest`/`ceil`
+// exactly as WASM requires. Execution-verified against wasmtime over a
+// halfway/tie + ±0 + ±inf + NaN table in
+// `scripts/repro/aarch64_float_completion_851_differential.py` — the
+// ties-to-even claim is CHECKED, not assumed.
+// ---------------------------------------------------------------------------
+
+/// `frintp sd, sn` — round toward +inf (WASM `f32.ceil`).
+pub fn frintp_s(rd: FReg, rn: FReg) -> u32 {
+    fp2(0x1E24_C000, rd, rn)
+}
+/// `frintm sd, sn` — round toward -inf (WASM `f32.floor`).
+pub fn frintm_s(rd: FReg, rn: FReg) -> u32 {
+    fp2(0x1E25_4000, rd, rn)
+}
+/// `frintz sd, sn` — round toward zero (WASM `f32.trunc`).
+pub fn frintz_s(rd: FReg, rn: FReg) -> u32 {
+    fp2(0x1E25_C000, rd, rn)
+}
+/// `frintn sd, sn` — round to nearest, ties to EVEN (WASM `f32.nearest`).
+pub fn frintn_s(rd: FReg, rn: FReg) -> u32 {
+    fp2(0x1E24_4000, rd, rn)
+}
+/// `frintp dd, dn` — WASM `f64.ceil`.
+pub fn frintp_d(rd: FReg, rn: FReg) -> u32 {
+    fp2(0x1E64_C000, rd, rn)
+}
+/// `frintm dd, dn` — WASM `f64.floor`.
+pub fn frintm_d(rd: FReg, rn: FReg) -> u32 {
+    fp2(0x1E65_4000, rd, rn)
+}
+/// `frintz dd, dn` — WASM `f64.trunc`.
+pub fn frintz_d(rd: FReg, rn: FReg) -> u32 {
+    fp2(0x1E65_C000, rd, rn)
+}
+/// `frintn dd, dn` — WASM `f64.nearest` (ties to even).
+pub fn frintn_d(rd: FReg, rn: FReg) -> u32 {
+    fp2(0x1E64_4000, rd, rn)
+}
+
+// ---------------------------------------------------------------------------
+// v0.54 L2 (#851) — `LDR/STR (SIMD&FP, immediate, unsigned offset)`: the
+// linear-memory access forms for f32/f64. Same shape as the GP
+// [`ldst_uimm`] family (size[31:30] + opc[23:22] + scaled imm12), with the
+// V-register bit 26 set, so an `s`/`d` register is the data operand.
+//
+// WIDTH: `ldr s` / `str s` move exactly 4 bytes (imm12 scaled by 4); `ldr d` /
+// `str d` exactly 8 (scaled by 8). `ldr s` ZEROES the rest of the V register,
+// so a subsequently-read `d` view is clean — but the selector never relies on
+// that: widths are carried by the op, as everywhere else in this backend.
+//
+// SOUNDNESS: like the GP forms these are emitted only AFTER the #865 bounds
+// check has proven `uxtw(addr) + offset + size <= limit` (or trapped) — an FP
+// access is bounds-checked by exactly the same `form_ea` path.
+// ---------------------------------------------------------------------------
+
+/// `ldr st, [xn, #imm12*4]` — load 32 bits into the `s` view of `V<t>`.
+pub fn ldr_s(rt: FReg, rn: Reg, imm12: u32) -> u32 {
+    ldst_uimm(0xBD40_0000, imm12, rn, rt)
+}
+/// `str st, [xn, #imm12*4]` — store the low 32 bits of `V<t>`.
+pub fn str_s(rt: FReg, rn: Reg, imm12: u32) -> u32 {
+    ldst_uimm(0xBD00_0000, imm12, rn, rt)
+}
+/// `ldr dt, [xn, #imm12*8]` — load 64 bits into the `d` view of `V<t>`.
+pub fn ldr_d(rt: FReg, rn: Reg, imm12: u32) -> u32 {
+    ldst_uimm(0xFD40_0000, imm12, rn, rt)
+}
+/// `str dt, [xn, #imm12*8]` — store the low 64 bits of `V<t>`.
+pub fn str_d(rt: FReg, rn: Reg, imm12: u32) -> u32 {
+    ldst_uimm(0xFD00_0000, imm12, rn, rt)
+}
+
 /// Append a 32-bit instruction word to a little-endian byte buffer.
 pub fn emit(buf: &mut Vec<u8>, word: u32) {
     buf.extend_from_slice(&word.to_le_bytes());
@@ -1100,6 +1212,57 @@ mod tests {
         assert_eq!(ucvtf_d_from_w(0, 1), 0x1E63_0020);
     }
 
+    // v0.54 L2 (#851) — the i64-SOURCE converts. Ground truth from
+    // `clang -target aarch64-linux-gnu` (assemble, objdump, read the word):
+    //   scvtf s0, x1 = 9e220020   ucvtf s2, x3 = 9e230062
+    //   scvtf d4, x5 = 9e6200a4   ucvtf d6, x7 = 9e6300e6
+    #[test]
+    fn fp_convert_i64_encodings_match_clang() {
+        assert_eq!(scvtf_s_from_x(0, 1), 0x9E22_0020);
+        assert_eq!(ucvtf_s_from_x(2, 3), 0x9E23_0062);
+        assert_eq!(scvtf_d_from_x(4, 5), 0x9E62_00A4);
+        assert_eq!(ucvtf_d_from_x(6, 7), 0x9E63_00E6);
+        // The x-forms are EXACTLY the w-forms with sf (bit 31) set.
+        assert_eq!(scvtf_s_from_x(0, 1), scvtf_s_from_w(0, 1) | SF64);
+        assert_eq!(ucvtf_d_from_x(6, 7), ucvtf_d_from_w(6, 7) | SF64);
+    }
+
+    // v0.54 L2 (#851) — FRINT round-to-integral. Ground truth from
+    // `clang -target aarch64-linux-gnu`:
+    //   frintn s0,s1 = 1e244020   frintp s2,s3 = 1e24c062
+    //   frintm s4,s5 = 1e2540a4   frintz s6,s7 = 1e25c0e6
+    //   frintn d0,d1 = 1e644020   frintp d2,d3 = 1e64c062
+    //   frintm d4,d5 = 1e6540a4   frintz d6,d7 = 1e65c0e6
+    #[test]
+    fn frint_encodings_match_clang() {
+        assert_eq!(frintn_s(0, 1), 0x1E24_4020);
+        assert_eq!(frintp_s(2, 3), 0x1E24_C062);
+        assert_eq!(frintm_s(4, 5), 0x1E25_40A4);
+        assert_eq!(frintz_s(6, 7), 0x1E25_C0E6);
+        assert_eq!(frintn_d(0, 1), 0x1E64_4020);
+        assert_eq!(frintp_d(2, 3), 0x1E64_C062);
+        assert_eq!(frintm_d(4, 5), 0x1E65_40A4);
+        assert_eq!(frintz_d(6, 7), 0x1E65_C0E6);
+        // The double forms are the single forms with ftype bit 22 set.
+        assert_eq!(frintn_d(0, 1), frintn_s(0, 1) | 0x0040_0000);
+        assert_eq!(frintz_d(6, 7), frintz_s(6, 7) | 0x0040_0000);
+    }
+
+    // v0.54 L2 (#851) — FP linear-memory load/store. Ground truth from
+    // `clang -target aarch64-linux-gnu`:
+    //   ldr s9,[x10,#16] = bd401149   str s9,[x10,#16] = bd001149
+    //   ldr d9,[x10,#32] = fd401149   str d9,[x10,#32] = fd001149
+    //   ldr s0,[x1]      = bd400020   str d0,[x1]      = fd000020
+    #[test]
+    fn fp_mem_encodings_match_clang() {
+        assert_eq!(ldr_s(9, 10, 16 / 4), 0xBD40_1149);
+        assert_eq!(str_s(9, 10, 16 / 4), 0xBD00_1149);
+        assert_eq!(ldr_d(9, 10, 32 / 8), 0xFD40_1149);
+        assert_eq!(str_d(9, 10, 32 / 8), 0xFD00_1149);
+        assert_eq!(ldr_s(0, 1, 0), 0xBD40_0020);
+        assert_eq!(str_d(0, 1, 0), 0xFD00_0020);
+    }
+
     #[test]
     fn mov_imm64_emits_movz_then_movks() {
         // 0x2345 → single movz (sf set).