feat(#869): lower the ARM 64-bit integer<->float conversion family — self-contained expansions, trap-guarded truncs, round-to-odd-exact f32 converts

.github/workflows/ci.yml

@@ -626,6 +626,16 @@ jobs:
       # This gate caught the optimized-path silent-NOP drop at land time.
       - name: Run trunc_sat boundary oracle (#782a, m7dp+m4f+aarch64)
         run: SYNTH=./target/debug/synth python scripts/repro/trunc_sat_782_differential.py
+      # #869: the 64-bit integer<->float conversion family (gale's six +
+      # the #756 i64.trunc_f64 pair) on cortex-m7dp — converts bit-exact
+      # (incl. the round-to-odd double-rounding killers), the TRAPPING trunc
+      # forms EXECUTED on every NaN/±inf/2^63/-2^63/2^64 boundary row (a
+      # wasmtime trap must be an ARM UDF stop — the #709-class silent-
+      # miscompile gate), m4f loud-decline honesty, falcon-flags symbol
+      # presence, and >=10k fixed-seed fuzz per direction. This gate caught
+      # the range-realloc cross-barrier live-in miscompile at land time.
+      - name: Run i64<->float conversion family oracle (#869, m7dp+m4f)
+        run: SYNTH=./target/debug/synth python scripts/repro/i64_float_conv_869_differential.py
       # #782(b): float `select` + explicit float `return` — the dominant class
       # on the real falcon fused core (12/26 skips incl. run-stabilization was
       # "an integer operation popped an f32"): select over two f32/f64 values

CHANGELOG.md

@@ -9,6 +9,37 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Added
 
+- **ARM 64-bit integer↔float conversion family lowered (#869, + the #756
+  `i64.trunc_f64` pair)** — all eight ops that previously loud-skipped their
+  function with `GI-FPU-001` now compile on `cortex-m7dp` (the falcon target),
+  unblocking `falcon:cascade/rate#tick`, `position#tick`, and `ekf#estimate`
+  at their public entry points. ARMv7E-M VFP has no 64-bit-integer `VCVT`, so
+  the lowerings are **self-contained multi-step expansions** (no `__aeabi`
+  runtime dependency, unicorn-executable):
+  - `f64.convert_i64_{s,u}`: exact two-word build — `VCVT` each 32-bit half,
+    scale the high word by 2^32 (exact), one `VADD.F64` = the single correct
+    round-to-nearest-even.
+  - `f32.convert_i64_{s,u}`: the same build plus a Fast2Sum exact residual and
+    a branch-free **round-to-odd** integer fixup before the `VCVT.F32.F64`
+    demote — the naive demote double-rounds (e.g. `0x8000_0080_0000_0001`
+    must round UP to 2^63+2^40 in f32; the f64 intermediate erases the sticky
+    bit). Round-to-odd at 53 bits makes the two-step rounding exactly equal
+    the direct 64→24 RNE (Boldo–Melquiond).
+  - `i64.trunc_f32_{s,u}` / `i64.trunc_f64_{s,u}` (**TRAPPING**, WASM §4.3.3):
+    the #709-class i64 domain guard (`-2^63 <= x < 2^63` signed /
+    `-1 < x < 2^64` unsigned, ordered compares + `UDF`; NaN fails the first
+    compare) in front of the #782 word-decompose, which for a guarded operand
+    provably never saturates. A bare decompose — or a bare `__aeabi_f2lz`
+    call — would saturate where WASM requires a trap: the
+    #633/#666/#709/#665/#642 silent-miscompile class.
+
+  CI gate: `scripts/repro/i64_float_conv_869_differential.py` — bit-exact vs
+  wasmtime under unicorn on every boundary row **with the trap rows executed
+  on both sides** (NaN, ±inf, 2^63, −2^63, 2^64, the largest-below-bound
+  f32/f64 values), the double-rounding killer patterns, and ≥10k fixed-seed
+  random patterns per direction (96k checks). Frozen fixtures 10/10
+  byte-identical (byte-changing only for modules using these ops).
+
 - **ISA-model adequacy (#867): "proved against a simplified model" is now an
   explicit, counted, CI-pinned trusted-base entry.** #682's shape — a green
   Qed while shipped code silently miscompiled, because the SIMPLIFIED
@@ -50,6 +81,15 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   model (differential suites exercise compiler OUTPUT); the artifact records
   that explicitly instead of implying test coverage.
 
+### Fixed
+
+- **Single-precision targets (m4f/m7) now loud-decline the whole #869 family
+  by name at the selector preamble** (listed in the f64 capability scope):
+  every member's lowering runs on double-precision machinery, and the
+  pre-existing `i64.trunc_sat_f32_{s,u}` promote-to-f64 path previously slid
+  past the capability gate to be caught only later at ISA validation. Same
+  honest-skip outcome, one gate earlier and named.
+
 ## [0.51.0] - 2026-07-23
 
 **"aarch64 runs real WASM modules."** The `-b aarch64` host-native backend crosses

claims.yaml

@@ -430,8 +430,10 @@ claims:
   # in-progress, not implemented. LIVE (derived-ARM-trap-term) classes now:
   # i32 div/rem, i64 div/rem (#756, field-derived), unreachable, i32
   # load/store (all widths), call_indirect, i32.trunc_f32_s/u, i32.trunc_f64_s/u
-  # (#756, D-register guard). i64.trunc_f64 has no shipped lowering (selector
-  # declines it) — its classifier is unit-gated only.
+  # (#756, D-register guard). i64.trunc_f32/f64 SHIP a guarded lowering since
+  # #869, but their symbolic ARM-side wiring (F64 compare/decompose chain) is
+  # the named residual — classifier unit-gated + EXECUTION-gated (the #869
+  # differential runs every trap row under unicorn), not yet derived-term VC.
   # Phase B (ordeal 0.9.1, ordeal#59/TR-020): float→int trunc trap class
   # covered — trunc_op/trap_trunc wrapper + #709 boundary-table eval gate.
   - id: SYNTH-VCR-VER-002-STATUS

crates/synth-backend-riscv/tests/cross_backend_op_parity.rs

@@ -525,7 +525,12 @@ fn classify(op: &WasmOp) -> ParityClass {
         | I32TruncSatF32S
         | I32TruncSatF32U
         | I64TruncSatF32S
-        | I64TruncSatF32U => StructurallyExcluded(FLOAT),
+        | I64TruncSatF32U
+        // #869: the f32-source i64-target TRAPPING truncations (ARM32 m7dp
+        // lowers them via the i64 domain guard + #782 decompose; RV32 has no
+        // floats — target-parameterized like the rest of the float surface).
+        | I64TruncF32S
+        | I64TruncF32U => StructurallyExcluded(FLOAT),
         // ─── f64 (StructurallyExcluded — target-parameterized) ───────────
         F64Add
         | F64Sub
@@ -648,7 +653,7 @@ fn all_wasm_op_representatives() -> Vec<WasmOp> {
         F32Load { offset: 0, align: 2 }, F32Store { offset: 0, align: 2 },
         F32ConvertI32S, F32ConvertI32U, F32ConvertI64S, F32ConvertI64U, F32DemoteF64,
         F32ReinterpretI32, I32ReinterpretF32, I32TruncF32S, I32TruncF32U, I32TruncSatF32S,
-        I32TruncSatF32U, I64TruncSatF32S, I64TruncSatF32U,
+        I32TruncSatF32U, I64TruncSatF32S, I64TruncSatF32U, I64TruncF32S, I64TruncF32U,
         // f64
         F64Add, F64Sub, F64Mul, F64Div, F64Eq, F64Ne, F64Lt, F64Le, F64Gt, F64Ge, F64Abs,
         F64Neg, F64Ceil, F64Floor, F64Trunc, F64Nearest, F64Sqrt, F64Min, F64Max,

crates/synth-core/src/wasm_decoder.rs

@@ -2258,6 +2258,21 @@ fn convert_operator(op: &wasmparser::Operator) -> Option<WasmOp> {
         F32ConvertI32U => Some(WasmOp::F32ConvertI32U),
         I32TruncF32S => Some(WasmOp::I32TruncF32S),
         I32TruncF32U => Some(WasmOp::I32TruncF32U),
+        // #869: the 64-bit integer<->float conversion family — previously all
+        // dropped here (`_ => None`), which loud-skipped every function using
+        // them (3 of 5 falcon cascade stages at their public entry points).
+        // ARMv7E-M VFP has no 64-bit-integer<->float instruction (VCVT on
+        // FPv4-SP/FPv5-D16 encodes only S32/U32 <-> F32/F64), so the ARM32
+        // lowering is a self-contained multi-step expansion on cortex-m7dp
+        // (see `try_lower_f32`/`try_lower_f64`); the TRAPPING trunc forms
+        // carry the #709-class i64 domain guard (WASM §4.3.3 requires a trap
+        // on NaN/out-of-range — the saturating decompose alone would be a
+        // silent miscompile). Backends without the machinery (RV32, aarch64's
+        // current subset, single-precision ARM) still loud-decline downstream.
+        F32ConvertI64S => Some(WasmOp::F32ConvertI64S),
+        F32ConvertI64U => Some(WasmOp::F32ConvertI64U),
+        I64TruncF32S => Some(WasmOp::I64TruncF32S),
+        I64TruncF32U => Some(WasmOp::I64TruncF32U),
         // #782a: the nontrapping trunc_sat family (0xFC-prefixed,
         // saturating-float-to-int proposal) — TOTAL ops (§4.3.2: NaN → 0,
         // out-of-range saturates to INT_MIN/INT_MAX, no traps). Un-dropped so
@@ -2309,8 +2324,8 @@ fn convert_operator(op: &wasmparser::Operator) -> Option<WasmOp> {
         // splice, f32.demote_f64 / i32<->f64 conversions via VCVT
         // (i32.trunc_f64_* carries the #709 trap-on-out-of-range domain
         // guard). Still m7dp-only (the selector preamble honest-rejects any
-        // f64 op elsewhere). Remaining dropped f64 surface: the i64<->f64
-        // conversions and reinterprets (need lowered i64 pair plumbing).
+        // f64 op elsewhere). The i64<->f64 reinterprets were un-dropped by
+        // #851 and the i64<->f64 conversions by #869 (below).
         F64Ceil => Some(WasmOp::F64Ceil),
         F64Floor => Some(WasmOp::F64Floor),
         F64Trunc => Some(WasmOp::F64Trunc),
@@ -2323,6 +2338,14 @@ fn convert_operator(op: &wasmparser::Operator) -> Option<WasmOp> {
         F64ConvertI32U => Some(WasmOp::F64ConvertI32U),
         I32TruncF64S => Some(WasmOp::I32TruncF64S),
         I32TruncF64U => Some(WasmOp::I32TruncF64U),
+        // #869 (+#756): the f64 half of the 64-bit integer<->float family —
+        // i64->f64 exact two-word VCVT+scale+add, i64.trunc_f64_* via the
+        // #709-class i64 domain guard + the #782 word-decompose. See the f32
+        // group above for the family story.
+        F64ConvertI64S => Some(WasmOp::F64ConvertI64S),
+        F64ConvertI64U => Some(WasmOp::F64ConvertI64U),
+        I64TruncF64S => Some(WasmOp::I64TruncF64S),
+        I64TruncF64U => Some(WasmOp::I64TruncF64U),
         // #782a: f64-source trunc_sat twins (see the f32 group above). falcon
         // v1.123 carries 7× i32.trunc_sat_f64_s — the m7dp double-precision
         // VCVT twins lower the i32-target forms; i64 targets loud-decline.
@@ -3011,11 +3034,12 @@ mod tests {
         // is no longer flagged — and since phase 2 (#369) so is the lowered
         // f64 subset (`f64.add` here; the m7dp-only capability gate lives in
         // the selector). Since phase 3 the f64 op TAIL (`f64.min` here) is
-        // decoded too; an out-of-scope scalar float op (`i64.trunc_f64_s` —
-        // the i64<->f64 conversions need lowered pair plumbing) is STILL
-        // flagged (loud-skip), never silently dropped — the #369 honesty
-        // contract holds for the not-yet-lowered surface. A pure-integer
-        // function stays clean.
+        // decoded too; and since #869 the 64-bit integer<->float conversion
+        // family (`i64.trunc_f64_s` here) decodes as well — the scalar float
+        // decode surface is complete, with capability gating (m7dp-only)
+        // living in the selector. The flag-never-drop honesty contract for
+        // the remaining undecoded float surface is pinned by the
+        // float-global test below. A pure-integer function stays clean.
         let wat = r#"
             (module
                 (func (export "fadd") (param f32 f32) (result f32)
@@ -3084,12 +3108,18 @@ mod tests {
             "f64.min must decode to WasmOp::F64Min: {:?}",
             dmin.ops
         );
-        // Out-of-scope scalar double op: still flagged, never dropped.
+        // #869: the i64<->f64 conversions are now IN scope — decoded, not
+        // flagged (the m7dp capability gate lives in the selector preamble).
         assert!(
-            dtrunc64.unsupported.is_some(),
-            "i64.trunc_f64_s must still flag the function unsupported (out of scope), got {:?}",
+            dtrunc64.unsupported.is_none(),
+            "#869: i64.trunc_f64_s must now decode (not be flagged), got {:?}",
             dtrunc64.unsupported
         );
+        assert!(
+            dtrunc64.ops.contains(&WasmOp::I64TruncF64S),
+            "i64.trunc_f64_s must decode to WasmOp::I64TruncF64S: {:?}",
+            dtrunc64.ops
+        );
         assert!(
             iadd.unsupported.is_none(),
             "a pure-integer function must NOT be flagged: {:?}",

crates/synth-core/src/wasm_op.rs

@@ -365,6 +365,11 @@ pub enum WasmOp {
     I64TruncF64U,      // Truncate f64 to unsigned i64
     I32TruncF64S,      // Truncate f64 to signed i32
     I32TruncF64U,      // Truncate f64 to unsigned i32
+    // #869: the f32-source i64-target TRAPPING truncations — the only two
+    // members of the 64-bit integer<->float conversion family that had no
+    // WasmOp variant at all (the rest existed but were dropped at decode).
+    I64TruncF32S, // Truncate f32 to signed i64 (traps on NaN/out-of-range)
+    I64TruncF32U, // Truncate f32 to unsigned i64 (traps on NaN/out-of-range)
 
     // Nontrapping f64→int (saturating-float-to-int, §4.3.2 trunc_sat — see
     // the f32 group above for the semantics).

crates/synth-core/src/wasm_stack_check.rs

@@ -163,8 +163,9 @@ fn stack_effect_or_bail(op: &WasmOp) -> StackEffect {
         | F32ReinterpretI32 | I32ReinterpretF32 | I32TruncF32S | I32TruncF32U | F64ConvertI32S
         | F64ConvertI32U | F64ConvertI64S | F64ConvertI64U | F64PromoteF32 | F64ReinterpretI64
         | I64ReinterpretF64 | I64TruncF64S | I64TruncF64U | I32TruncF64S | I32TruncF64U
-        | I32TruncSatF32S | I32TruncSatF32U | I32TruncSatF64S | I32TruncSatF64U
-        | I64TruncSatF32S | I64TruncSatF32U | I64TruncSatF64S | I64TruncSatF64U => modeled(1, 1),
+        | I64TruncF32S | I64TruncF32U | I32TruncSatF32S | I32TruncSatF32U | I32TruncSatF64S
+        | I32TruncSatF64U | I64TruncSatF32S | I64TruncSatF32U | I64TruncSatF64S
+        | I64TruncSatF64U => modeled(1, 1),
 
         // ---- pop-only ----------------------------------------------------
         LocalSet(_) | GlobalSet(_) | Drop => modeled(1, 0),