From 22fc68e1c0a55f453b043011bd85bc9f31bd26e7 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 30 Jul 2026 14:30:57 +0200 Subject: [PATCH 1/8] =?UTF-8?q?feat(aarch64):=20encoder=20support=20for=20?= =?UTF-8?q?FRINT/FP-mem/i64=E2=86=92float=20converts=20(#851)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit v0.54 L2 step 1 — the four encoder families the VCR-SEL-005 third-backend parity oracle names in its ROUNDING / FP_MEM / I64_TO_FP decline reasons: * `FRINT{P,M,Z,N}` s/d — round-to-integral with the mode pinned in the OPCODE (not FPCR.RMode), so the lowering cannot depend on ambient embedder state. FRINTN is round-to-nearest-TIES-TO-EVEN, which is what WASM §4.3.3 `fnearest` requires (FRINTA — ties-away — would be wrong). * `LDR/STR (SIMD&FP, unsigned offset)` s/d — the linear-memory FP access forms, same size/opc/scaled-imm12 shape as the GP family with the V-register bit set. * `SCVTF`/`UCVTF` x-source forms — the i64→float converts, exactly the already-shipped w-forms with `sf` set (mirroring the sdiv/sdiv64 pair). Every encoding is pinned to `clang -target aarch64-linux-gnu` ground truth in three new tests (assemble the mnemonic, objdump, read the 32-bit word), plus the two structural relations (d-form = s-form | ftype bit; x-form = w-form | sf) so a future edit of one half cannot silently drift from the other. Encoder only — no selector arm consumes these yet, so output bytes are unchanged for every currently-compiling module. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-backend-aarch64/src/encoder.rs | 163 ++++++++++++++++++++ 1 file changed, 163 insertions(+) diff --git a/crates/synth-backend-aarch64/src/encoder.rs b/crates/synth-backend-aarch64/src/encoder.rs index 12fdc597..20278937 100644 --- a/crates/synth-backend-aarch64/src/encoder.rs +++ b/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`, 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`. +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`. +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`. +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`. +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, 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). From a81b034944a14f0c2cc1b3f273edc77d8b90eb23 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 30 Jul 2026 14:52:34 +0200 Subject: [PATCH 2/8] feat(aarch64): close ROUNDING + I64_TO_FP parity gaps (#851) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit v0.54 L2 step 2 — two of the four classes the VCR-SEL-005 third-backend oracle enumerated: * ROUNDING: `f{32,64}.{ceil,floor,trunc,nearest}` each lower to ONE mode-pinned `FRINT{P,M,Z,N}`. TOTAL ops — no domain guard, and a guard would be a defect (it would trap where WASM returns a value). * I64_TO_FP: `f{32,64}.convert_i64_{s,u}` lower to the `x`-form SCVTF/UCVTF. Also total. Parity-gate entries flipped Err→Ok in the SAME commit (8 rounding + 4 converts) and the now-unused ROUNDING / I64_TO_FP reason constants DELETED — a gap claim must not outlive the gap. No wildcard arm, nothing moved to StructurallyExcluded. The selector's own stale claim (`rounding_and_i64_float_converts_are_loud_declined`) is narrowed to the one class still open (`trapping_i64_truncations_are_loud_declined`). DECODER (the end-to-end half): `f32.{ceil,floor,trunc,nearest}` were dropped at `_ => None`, so a real module using them loud-SKIPPED the whole function before the selector ever saw it. Un-dropped, exactly as #538 m4 did for f32.min/max — and with the same consequence for ARM32. ARM32 now LOUD-DECLINES the four (previously unreachable, so this exposes no regression): its `ArmOp::F32{Ceil,Floor,Trunc,Nearest}` pseudo-op is an FPSCR-RMode + `VCVT.S32.F32` + `VCVT.F32.S32` ROUND-TRIP THROUGH i32, and VCVT SATURATES — `ceil(1e30)` would give 2147483648.0, `ceil(±inf)` a finite bound, `ceil(NaN)` 0.0, where WASM §4.3.3 returns 1e30 / ±inf / NaN. That is the #709 more-total-than-WASM class; declining keeps it latent instead of shipping it. The `f32_operations_test` cases that pinned the wrong lowering as Ok are replaced by the decline assertion. The #554 honesty fixture used `f64.floor` as its "deliberately declined float op" — a claim this commit invalidates. Repointed at a value-carrying (f32-result) `block`: still fully DECODED, still declined by the aarch64 SELECTOR, and the assertion is STRENGTHENED (stderr must come from the selector AND name the reason, not merely contain "unsupported"). EXECUTION-VERIFIED on this arm64 host, MAP_JIT native call vs wasmtime, bit-exact over 62 checks: the ties-to-even halfway table (0.5→0, 1.5→2, 2.5→2, 3.5→4 and negatives) CONFIRMS FRINTN is roundTiesToEven (FRINTA would fail 0.5 and 2.5), plus ±0/±inf/NaN/1e30 passthrough and the i64 convert rounding ties (2^53±1, 2^62, ±2^63, 2^64−1). Gates: cargo test --workspace exit 0 (130 suites), clippy -D warnings exit 0, fmt --check clean, frozen anchors 10/10 (no ARM golden moved — the four rounding ops were undecodable, so no frozen fixture contains one). Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-backend-aarch64/src/selector.rs | 129 ++++++++++++++---- .../tests/cross_backend_op_parity.rs | 42 ++---- .../tests/f32_operations_test.rs | 37 +++-- .../tests/aarch64_f32_loudskip_554.rs | 18 ++- crates/synth-core/src/wasm_decoder.rs | 23 +++- .../src/instruction_selector.rs | 42 +++--- scripts/repro/aarch64_f32_unsupported_554.wat | 26 ++-- 7 files changed, 212 insertions(+), 105 deletions(-) diff --git a/crates/synth-backend-aarch64/src/selector.rs b/crates/synth-backend-aarch64/src/selector.rs index ba44c444..6bdcbb59 100644 --- a/crates/synth-backend-aarch64/src/selector.rs +++ b/crates/synth-backend-aarch64/src/selector.rs @@ -1476,6 +1476,28 @@ pub fn select_typed_cf_calls( WasmOp::F32Copysign => copysign(&mut words, &mut stack, false)?, WasmOp::F64Copysign => copysign(&mut words, &mut stack, true)?, + // --- v0.54 L2 (#851): round-to-integral (ceil/floor/trunc/nearest). + // + // One `FRINT` each, with the rounding mode pinned in the + // OPCODE — the lowering never reads FPCR.RMode, so it is correct + // under whatever rounding mode the embedder left set. All four are + // TOTAL (WASM §4.3.3 `fceil`/`ffloor`/`ftrunc`/`fnearest` never + // trap and neither do these), so no domain guard is needed — the + // "more-total-than-WASM" hazard that forces the trunc guards below + // simply does not arise for float→float rounding. + // + // `nearest` is roundTiesToEven, which is FRINTN (NOT FRINTA, which + // is ties-AWAY-from-zero) — checked by execution against wasmtime + // over a halfway table (0.5/1.5/2.5/-0.5/…), not assumed. --- + WasmOp::F32Ceil => funop(&mut words, &mut stack, enc::frintp_s)?, + WasmOp::F32Floor => funop(&mut words, &mut stack, enc::frintm_s)?, + WasmOp::F32Trunc => funop(&mut words, &mut stack, enc::frintz_s)?, + WasmOp::F32Nearest => funop(&mut words, &mut stack, enc::frintn_s)?, + WasmOp::F64Ceil => funop(&mut words, &mut stack, enc::frintp_d)?, + WasmOp::F64Floor => funop(&mut words, &mut stack, enc::frintm_d)?, + WasmOp::F64Trunc => funop(&mut words, &mut stack, enc::frintz_d)?, + WasmOp::F64Nearest => funop(&mut words, &mut stack, enc::frintn_d)?, + // --- trapping float→int truncations (m4): domain-guarded #709 --- WasmOp::I32TruncF32S => trunc_guarded(&mut words, &mut stack, false, true)?, WasmOp::I32TruncF32U => trunc_guarded(&mut words, &mut stack, false, false)?, @@ -1501,6 +1523,18 @@ pub fn select_typed_cf_calls( WasmOp::F32ConvertI32U => cvt_gp_to_fp(&mut words, &mut stack, enc::ucvtf_s_from_w)?, WasmOp::F64ConvertI32S => cvt_gp_to_fp(&mut words, &mut stack, enc::scvtf_d_from_w)?, WasmOp::F64ConvertI32U => cvt_gp_to_fp(&mut words, &mut stack, enc::ucvtf_d_from_w)?, + // v0.54 L2 (#851): the i64-SOURCE converts — the `x`-form SCVTF/ + // UCVTF. Also TOTAL: every i64 has a nearest f32/f64, and the + // rounding A64 applies when the value exceeds the destination's + // exact-integer range (2^24 for f32, 2^53 for f64) is + // round-to-nearest-EVEN, which is what WASM §4.3.2 `convert` + // specifies. No guard, no decline — but execution-verified over + // the rounding-tie table (2^53±1, 2^63-1, u64 max, …) rather than + // assumed, since this is the one place the two could disagree. + WasmOp::F32ConvertI64S => cvt_gp_to_fp(&mut words, &mut stack, enc::scvtf_s_from_x)?, + WasmOp::F32ConvertI64U => cvt_gp_to_fp(&mut words, &mut stack, enc::ucvtf_s_from_x)?, + WasmOp::F64ConvertI64S => cvt_gp_to_fp(&mut words, &mut stack, enc::scvtf_d_from_x)?, + WasmOp::F64ConvertI64U => cvt_gp_to_fp(&mut words, &mut stack, enc::ucvtf_d_from_x)?, // --- bit-cast reinterprets (pure FMOV, no numeric change) --- WasmOp::F32ReinterpretI32 => { @@ -2758,6 +2792,68 @@ mod tests { } } + // --- v0.54 L2 (#851): rounding + i64-source converts --- + + #[test] + fn rounding_ops_lower_to_the_mode_pinned_frint() { + // Each WASM rounding op is ONE FRINT with the mode in the opcode. + // FRINTN (ties-to-EVEN) is `nearest`; FRINTA (ties-away) is NOT a WASM + // op and must never appear. + for (op, f64_src, want) in [ + ( + WasmOp::F32Ceil, + false, + enc::frintp_s as fn(FReg, FReg) -> u32, + ), + (WasmOp::F32Floor, false, enc::frintm_s), + (WasmOp::F32Trunc, false, enc::frintz_s), + (WasmOp::F32Nearest, false, enc::frintn_s), + (WasmOp::F64Ceil, true, enc::frintp_d), + (WasmOp::F64Floor, true, enc::frintm_d), + (WasmOp::F64Trunc, true, enc::frintz_d), + (WasmOp::F64Nearest, true, enc::frintn_d), + ] { + let ops = vec![WasmOp::LocalGet(0), op.clone(), WasmOp::End]; + let (f32s, f64s): (&[bool], &[bool]) = if f64_src { + (&[], &[true]) + } else { + (&[true], &[]) + }; + let w = select_typed(&ops, 1, f32s, f64s).unwrap(); + assert_eq!( + w, + vec![want(FTEMPS[0], 0), enc::fmov_d(0, FTEMPS[0]), enc::ret()], + "{op:?} must be one mode-pinned FRINT" + ); + // TOTAL op: a guard would spuriously trap where WASM returns a value. + assert!(!w.contains(&enc::brk(0)), "{op:?} never traps"); + } + } + + #[test] + fn i64_source_converts_use_the_x_form_scvtf_ucvtf() { + for (op, want) in [ + ( + WasmOp::F32ConvertI64S, + enc::scvtf_s_from_x as fn(FReg, Reg) -> u32, + ), + (WasmOp::F32ConvertI64U, enc::ucvtf_s_from_x), + (WasmOp::F64ConvertI64S, enc::scvtf_d_from_x), + (WasmOp::F64ConvertI64U, enc::ucvtf_d_from_x), + ] { + let ops = vec![WasmOp::LocalGet(0), op.clone(), WasmOp::End]; + let w = select_typed(&ops, 1, &[], &[]).unwrap(); + assert_eq!( + w, + vec![want(FTEMPS[0], 0), enc::fmov_d(0, FTEMPS[0]), enc::ret()], + "{op:?} must be one x-source convert" + ); + } + // The x-form must NOT be confusable with the (already shipped) w-form: + // a w-source convert of a value above 2^32 would read only the low half. + assert_ne!(enc::scvtf_d_from_x(16, 0), enc::scvtf_d_from_w(16, 0)); + } + #[test] fn f32_min_max_use_fmin_fmax() { // WASM min/max ≡ A64 FMIN/FMAX (IEEE 754-2019 minimum/maximum) — a @@ -2840,37 +2936,16 @@ mod tests { } #[test] - fn rounding_and_i64_float_converts_are_loud_declined() { - // The m4 honesty frontier: rounding ops and i64<->float conversions - // stay DECLINED (never silent wrong code) until a later increment. - for op in [ - WasmOp::F32Ceil, - WasmOp::F32Floor, - WasmOp::F32Trunc, - WasmOp::F32Nearest, - WasmOp::F64Ceil, - WasmOp::F64Floor, - WasmOp::F64Trunc, - WasmOp::F64Nearest, - ] { - let ops = vec![WasmOp::LocalGet(0), op, WasmOp::End]; - assert!( - select_typed(&ops, 1, &[true], &[true]).is_err(), - "rounding ops not yet supported — must loud-decline" - ); - } + fn trapping_i64_truncations_are_loud_declined() { + // The remaining m4 honesty frontier after v0.54 L2 closed rounding and + // the i64-SOURCE converts: the TRAPPING i64-TARGET truncations still + // decline, because A64 FCVTZ{S,U} SATURATE where WASM traps (#709) and + // the i64 domain guard has not landed. Never silent wrong code. for op in [WasmOp::I64TruncF64S, WasmOp::I64TruncF64U] { let ops = vec![WasmOp::LocalGet(0), op, WasmOp::End]; assert!( select_typed(&ops, 1, &[], &[true]).is_err(), - "i64<->float conversions not yet supported — must loud-decline" - ); - } - for op in [WasmOp::F64ConvertI64S, WasmOp::F32ConvertI64U] { - let ops = vec![WasmOp::LocalGet(0), op, WasmOp::End]; - assert!( - select_typed(&ops, 1, &[], &[]).is_err(), - "i64<->float conversions not yet supported — must loud-decline" + "trapping i64-target truncation not yet supported — must loud-decline" ); } } diff --git a/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs b/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs index fb080770..52984de0 100644 --- a/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs +++ b/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs @@ -995,12 +995,8 @@ fn a64_extended_surface( op: &WasmOp, ) -> Option<(&'static str, u32, Vec, Result<(), &'static str>)> { // Gap reasons, shared per class. - const ROUNDING: &str = "aarch64 selector has no ceil/floor/trunc/nearest arm (A64 FRINTP/FRINTM/\ - FRINTZ/FRINTN exist; encoder support not yet landed) — deferred, #851"; const FP_MEM: &str = "aarch64 selector has no f32/f64 load/store arm (linear-memory FP access \ needs LDR/STR (SIMD&FP) forms) — deferred, #851"; - const I64_TO_FP: &str = "aarch64 selector has no i64→float convert arm (SCVTF/UCVTF x-forms not \ - yet landed; only the i32-source forms are) — deferred, #851"; const TRAP_TRUNC_I64: &str = "aarch64 selector has no TRAPPING i64-target truncation arm (needs the \ #709-class i64 domain guard; the SATURATING i64 forms do lower) — \ deferred, #851"; @@ -1213,16 +1209,11 @@ fn a64_extended_surface( Ok(()), ), F32Const(_) => some("f32.const", 0, vec![F32Const(1.0)], Ok(())), - // ─── f32 rounding — GAP ────────────────────────────────────────── - F32Ceil => some("f32.ceil", 0, vec![F32Const(1.5), F32Ceil], Err(ROUNDING)), - F32Floor => some("f32.floor", 0, vec![F32Const(1.5), F32Floor], Err(ROUNDING)), - F32Trunc => some("f32.trunc", 0, vec![F32Const(1.5), F32Trunc], Err(ROUNDING)), - F32Nearest => some( - "f32.nearest", - 0, - vec![F32Const(1.5), F32Nearest], - Err(ROUNDING), - ), + // ─── f32 rounding — lowered (FRINTP/M/Z/N, v0.54 L2) ───────────── + F32Ceil => some("f32.ceil", 0, vec![F32Const(1.5), F32Ceil], Ok(())), + F32Floor => some("f32.floor", 0, vec![F32Const(1.5), F32Floor], Ok(())), + F32Trunc => some("f32.trunc", 0, vec![F32Const(1.5), F32Trunc], Ok(())), + F32Nearest => some("f32.nearest", 0, vec![F32Const(1.5), F32Nearest], Ok(())), // ─── f32 memory — GAP ──────────────────────────────────────────── F32Load { .. } => some( "f32.load", @@ -1266,13 +1257,13 @@ fn a64_extended_surface( "f32.convert_i64_s", 0, vec![I64Const(5), F32ConvertI64S], - Err(I64_TO_FP), + Ok(()), ), F32ConvertI64U => some( "f32.convert_i64_u", 0, vec![I64Const(5), F32ConvertI64U], - Err(I64_TO_FP), + Ok(()), ), F32DemoteF64 => some( "f32.demote_f64", @@ -1424,16 +1415,11 @@ fn a64_extended_surface( Ok(()), ), F64Const(_) => some("f64.const", 0, vec![F64Const(1.0)], Ok(())), - // ─── f64 rounding — GAP ────────────────────────────────────────── - F64Ceil => some("f64.ceil", 0, vec![F64Const(1.5), F64Ceil], Err(ROUNDING)), - F64Floor => some("f64.floor", 0, vec![F64Const(1.5), F64Floor], Err(ROUNDING)), - F64Trunc => some("f64.trunc", 0, vec![F64Const(1.5), F64Trunc], Err(ROUNDING)), - F64Nearest => some( - "f64.nearest", - 0, - vec![F64Const(1.5), F64Nearest], - Err(ROUNDING), - ), + // ─── f64 rounding — lowered (FRINTP/M/Z/N, v0.54 L2) ───────────── + F64Ceil => some("f64.ceil", 0, vec![F64Const(1.5), F64Ceil], Ok(())), + F64Floor => some("f64.floor", 0, vec![F64Const(1.5), F64Floor], Ok(())), + F64Trunc => some("f64.trunc", 0, vec![F64Const(1.5), F64Trunc], Ok(())), + F64Nearest => some("f64.nearest", 0, vec![F64Const(1.5), F64Nearest], Ok(())), // ─── f64 memory — GAP ──────────────────────────────────────────── F64Load { .. } => some( "f64.load", @@ -1477,13 +1463,13 @@ fn a64_extended_surface( "f64.convert_i64_s", 0, vec![I64Const(5), F64ConvertI64S], - Err(I64_TO_FP), + Ok(()), ), F64ConvertI64U => some( "f64.convert_i64_u", 0, vec![I64Const(5), F64ConvertI64U], - Err(I64_TO_FP), + Ok(()), ), F64PromoteF32 => some( "f64.promote_f32", diff --git a/crates/synth-backend/tests/f32_operations_test.rs b/crates/synth-backend/tests/f32_operations_test.rs index ebd4dfde..a607e745 100644 --- a/crates/synth-backend/tests/f32_operations_test.rs +++ b/crates/synth-backend/tests/f32_operations_test.rs @@ -258,21 +258,34 @@ fn test_i32_trunc_f32_u_compiles() { } // ============================================================================ -// F32 PSEUDO-OPS — now supported on cortex-m4f via VFP sequences +// F32 PSEUDO-OPS // ============================================================================ #[test] -fn test_f32_ceil_compiles_on_m4f() { - let mut selector = selector_with_fpu(); - let result = selector.select(&[WasmOp::F32Const(1.5), WasmOp::F32Ceil]); - assert!(result.is_ok(), "f32.ceil should compile on cortex-m4f"); -} - -#[test] -fn test_f32_floor_compiles_on_m4f() { - let mut selector = selector_with_fpu(); - let result = selector.select(&[WasmOp::F32Const(1.5), WasmOp::F32Floor]); - assert!(result.is_ok(), "f32.floor should compile on cortex-m4f"); +fn test_f32_rounding_loud_declined_on_m4f() { + // v0.54 L2 (#851), mirroring the F32Min/F32Max decision below: the four + // rounding ops are DECODED now (aarch64 lowers each as one mode-pinned + // FRINT), but ARM32's legacy `ArmOp::F32{Ceil,Floor,Trunc,Nearest}` + // pseudo-op is an FPSCR-RMode + `VCVT.S32.F32` + `VCVT.F32.S32` ROUND-TRIP + // THROUGH i32. VCVT SATURATES, so `ceil(1e30)` → 2147483648.0, + // `ceil(±inf)` → a finite bound and `ceil(NaN)` → 0.0 where WASM §4.3.3 + // returns 1e30 / ±inf / NaN — the #709 more-total-than-WASM class. The + // ARM32 selector must LOUD-decline until a real `VRINT.F32` lowering + // lands; this replaces the old tests that pinned the wrong lowering as Ok. + for op in [ + WasmOp::F32Ceil, + WasmOp::F32Floor, + WasmOp::F32Trunc, + WasmOp::F32Nearest, + ] { + let mut selector = selector_with_fpu(); + let result = selector.select(&[WasmOp::F32Const(1.5), op.clone()]); + assert!( + result.is_err(), + "{op:?} must LOUD-decline on ARM32 (saturating VCVT round-trip is \ + not WASM-correct), got {result:?}" + ); + } } #[test] diff --git a/crates/synth-cli/tests/aarch64_f32_loudskip_554.rs b/crates/synth-cli/tests/aarch64_f32_loudskip_554.rs index ae3f4204..e49daa57 100644 --- a/crates/synth-cli/tests/aarch64_f32_loudskip_554.rs +++ b/crates/synth-cli/tests/aarch64_f32_loudskip_554.rs @@ -34,7 +34,7 @@ fn aarch64_rejects_f32_function_instead_of_silent_miscompile_554() { "-b", "aarch64", "-n", - "f64floor", + "f32block", "-o", "/tmp/aarch64_f32_554.o", ]) @@ -42,15 +42,23 @@ fn aarch64_rejects_f32_function_instead_of_silent_miscompile_554() { .expect("run synth"); assert!( !out.status.success(), - "expected a non-zero exit for a declined float op (f64.floor) on \ - -b aarch64; got success (silent miscompile). stdout={} stderr={}", + "expected a non-zero exit for a declined float construct (f32-result \ + block) on -b aarch64; got success (silent miscompile). stdout={} \ + stderr={}", String::from_utf8_lossy(&out.stdout), String::from_utf8_lossy(&out.stderr), ); let stderr = String::from_utf8_lossy(&out.stderr).to_lowercase(); + // The decline must come from the SELECTOR (nothing upstream masked it) and + // must NAME the reason — a bare non-zero exit is not honesty. assert!( - stderr.contains("unsupported"), - "error must name the unsupported operator; stderr={stderr}" + stderr.contains("aarch64 selector"), + "the decline must come from the aarch64 selector, not an upstream \ + drop; stderr={stderr}" + ); + assert!( + stderr.contains("loud-declining") || stderr.contains("only void"), + "error must name why the construct is declined; stderr={stderr}" ); } diff --git a/crates/synth-core/src/wasm_decoder.rs b/crates/synth-core/src/wasm_decoder.rs index 2de42b4b..d810d610 100644 --- a/crates/synth-core/src/wasm_decoder.rs +++ b/crates/synth-core/src/wasm_decoder.rs @@ -2259,11 +2259,30 @@ fn convert_operator(op: &wasmparser::Operator) -> Option { // = IEEE 754-2019 minimum/maximum ≡ WASM NaN-propagation + -0<+0); // ARM32 LOUD-declines them (its legacy compare-select pseudo-op is // NaN/±0-wrong — see the selector's F32Min/F32Max reject arm) and - // RV32 loud-declines all floats. The f32 rounding ops stay at - // `_ => None` until a later increment. + // RV32 loud-declines all floats. F32Sqrt => Some(WasmOp::F32Sqrt), F32Min => Some(WasmOp::F32Min), F32Max => Some(WasmOp::F32Max), + // v0.54 L2 (#851): the f32 rounding family un-dropped, exactly like + // min/max above and for the same reason — aarch64 lowers each as ONE + // mode-pinned `FRINT{P,M,Z,N}` (`nearest` = FRINTN = ties-to-EVEN, WASM + // §4.3.3), so keeping them at `_ => None` would loud-SKIP whole + // functions the A64 backend compiles correctly. + // + // ARM32 LOUD-DECLINES all four: 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, which is not + // WASM-correct outside i32 range: VCVT saturates, so `ceil(1e30)` would + // yield 2147483648.0, `ceil(±inf)` a finite bound and `ceil(NaN)` 0.0, + // where WASM returns 1e30 / ±inf / NaN. That is the #709 + // "more-total-than-WASM" class, latent only because the op was + // undecodable — the selector reject arm keeps it latent (a real + // `VRINT{P,M,Z,N}.F32` twin of the shipping F64 path is a later + // increment). RV32 has no floats and declines everything. + F32Ceil => Some(WasmOp::F32Ceil), + F32Floor => Some(WasmOp::F32Floor), + F32Trunc => Some(WasmOp::F32Trunc), + F32Nearest => Some(WasmOp::F32Nearest), // #708 (phase 1b): the f32<->i32 bit-casts. Pure `VMOV` between a core // register and a single-precision S-register — no numeric conversion. F32ReinterpretI32 => Some(WasmOp::F32ReinterpretI32), diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index d052f0e0..9685e9b5 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -7538,27 +7538,27 @@ impl InstructionSelector { ))); } - // F32 rounding pseudo-ops — emit ArmOp variants, encoder expands to - // multi-instruction sequences using FPSCR rounding-mode manipulation - F32Ceil if self.fpu.is_some() => { - let sd = self.alloc_vfp_reg(); - let sm = self.alloc_vfp_reg(); - vec![ArmOp::F32Ceil { sd, sm }] - } - F32Floor if self.fpu.is_some() => { - let sd = self.alloc_vfp_reg(); - let sm = self.alloc_vfp_reg(); - vec![ArmOp::F32Floor { sd, sm }] - } - F32Trunc if self.fpu.is_some() => { - let sd = self.alloc_vfp_reg(); - let sm = self.alloc_vfp_reg(); - vec![ArmOp::F32Trunc { sd, sm }] - } - F32Nearest if self.fpu.is_some() => { - let sd = self.alloc_vfp_reg(); - let sm = self.alloc_vfp_reg(); - vec![ArmOp::F32Nearest { sd, sm }] + // F32 rounding — LOUD-DECLINED on ARM32 (v0.54 L2, #851; the same + // move #538 m4 made for F32Min/F32Max). The legacy `ArmOp::F32 + // {Ceil,Floor,Trunc,Nearest}` pseudo-op expands to an FPSCR-RMode + // set + `VCVT.S32.F32` + `VCVT.F32.S32` ROUND-TRIP THROUGH A + // 32-BIT INTEGER (see `encode_thumb_f32_rounding` / + // `encode_arm_f32_rounding`). VCVT SATURATES, so outside i32 range + // the result is wrong, not merely imprecise: `ceil(1e30)` would + // give 2147483648.0, `ceil(±inf)` a finite bound and `ceil(NaN)` + // 0.0, where WASM §4.3.3 returns 1e30 / ±inf / NaN. Those inputs + // were unreachable while the decoder dropped the op; now that it + // delivers them (so aarch64 can lower its one-instruction FRINT), + // ARM32 must honest-reject rather than expose the latent #709-class + // miscompile. The fix is the f32 twin of the shipping F64 rounding + // path (`VRINT{P,M,Z,N}.F32`, FPv5) — a later increment. + op @ (F32Ceil | F32Floor | F32Trunc | F32Nearest) if self.fpu.is_some() => { + return Err(synth_core::Error::synthesis(format!( + "{op:?} not supported on ARM32: the available lowering is a \ + saturating VCVT round-trip through i32, which is not WASM- \ + correct for |x| >= 2^31, ±inf or NaN — declined until the \ + VRINT.F32 lowering lands" + ))); } // F32 min/max — LOUD-DECLINED on ARM32 (#538 m4): the legacy // `ArmOp::F32Min/F32Max` pseudo-op encodes a naive VCMP + diff --git a/scripts/repro/aarch64_f32_unsupported_554.wat b/scripts/repro/aarch64_f32_unsupported_554.wat index 8af55cca..f103d2a5 100644 --- a/scripts/repro/aarch64_f32_unsupported_554.wat +++ b/scripts/repro/aarch64_f32_unsupported_554.wat @@ -1,13 +1,19 @@ -;; #554 — `-b aarch64` must REJECT an UNSUPPORTED float op honestly, not silently -;; miscompile it. m3 (#787) landed the non-trapping scalar floats and m4 (#538) -;; landed the domain-guarded trapping truncations + min/max + copysign, so the -;; honesty test moves to a float op that DELIBERATELY stays declined: `f64.floor` -;; (rounding). It is DECODED (the ARM32 m7dp backend lowers it), so it reaches -;; the aarch64 SELECTOR, which must loud-decline (`unsupported wasm op`) — the -;; strongest form of the honesty check. `i32add` is the control: a supported op -;; that must still compile. +;; #554 — `-b aarch64` must REJECT an UNSUPPORTED float construct honestly, not +;; silently miscompile it. The honesty target has MOVED as the surface closed: +;; m3 (#787) landed the non-trapping scalar floats, m4 (#538) the domain-guarded +;; trapping i32 truncations + min/max + copysign, and v0.54 L2 (#851) the last +;; four scalar-float classes (rounding, f32/f64 load/store, i64->float converts, +;; trapping i64-target truncations). With the SCALAR float surface complete, the +;; test now targets a float construct that DELIBERATELY stays declined: a +;; VALUE-CARRYING (f32-result) `block`. +;; +;; It is fully DECODED — no upstream drop masks it — so it reaches the aarch64 +;; SELECTOR, which must loud-decline (a value-carrying block needs result- +;; register reconciliation across the branch). That is the strongest form of the +;; honesty check. `i32add` is the control: a supported op that must still +;; compile. (module - (func (export "f64floor") (param f64) (result f64) - (f64.floor (local.get 0))) + (func (export "f32block") (param f32) (result f32) + (block (result f32) (local.get 0))) (func (export "i32add") (param i32 i32) (result i32) (i32.add (local.get 0) (local.get 1)))) From 131f604f379971ece7e426291dee1169670043bd Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 30 Jul 2026 14:55:43 +0200 Subject: [PATCH 3/8] =?UTF-8?q?feat(aarch64):=20close=20the=20FP=5FMEM=20p?= =?UTF-8?q?arity=20gap=20=E2=80=94=20bounds-checked=20f32/f64=20load/store?= =?UTF-8?q?=20(#851)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit v0.54 L2 step 3 — the third of the four classes the VCR-SEL-005 third-backend oracle enumerated. `f{32,64}.{load,store}` lower to the SIMD&FP unsigned-offset `ldr/str s|d` against the `x28` linear-memory base. BOUNDS, NOT AN AFTERTHOUGHT: the new `fload`/`fstore` closures reuse the SAME `form_ea` the integer accesses use, so an FP access inherits v0.52's #865 software bounds check verbatim — `uxtw(addr) + offset + size <= limit` proven (or `brk`) BEFORE the dereference, with the width folded into the compile-time constant K. That width matters: f64 gets K = limit − 8, so address 65532 is IN bounds for `f32.load` and OUT for `f64.load` on a one-page memory, and the oracle exercises exactly that split. Parity-gate entries flipped Err→Ok in the SAME commit (f32.load, f32.store, f64.load, f64.store) and the FP_MEM reason constant DELETED. No wildcard arm. Four selector tests pin the shape: the full bounds-checked f32.load sequence, the f64 width-aware K, scaled-imm12 offset folding (offset/4 for s, offset/8 for d), and the type-confusion guard (an i32 fed to `f32.store` ERRORS rather than storing the wrong register file). EXECUTION-VERIFIED vs wasmtime under unicorn (x28 = linear-memory base): 128/128 bit-exact over the {f32,f64} × {0, 4, 8, 100, 65532, 65535, 65536, 0xFFFFFFFF} × {1.5, ±0.0, ±inf, NaN, 3.14159, 1e30} store→load round-trip matrix — 56 of them OOB cases where synth traps exactly where wasmtime traps, and the in-bounds cases bit-exact including NaN payload and the sign of −0.0. Gates: aarch64 lib 111/111, parity oracle 8/8, clippy -D warnings exit 0, fmt clean, frozen anchors 10/10 (no ARM golden touched). Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-backend-aarch64/src/selector.rs | 180 ++++++++++++++++++ .../tests/cross_backend_op_parity.rs | 14 +- 2 files changed, 186 insertions(+), 8 deletions(-) diff --git a/crates/synth-backend-aarch64/src/selector.rs b/crates/synth-backend-aarch64/src/selector.rs index 6bdcbb59..7a9646b3 100644 --- a/crates/synth-backend-aarch64/src/selector.rs +++ b/crates/synth-backend-aarch64/src/selector.rs @@ -1080,6 +1080,49 @@ pub fn select_typed_cf_calls( Ok(()) }; + // v0.54 L2 (#851) — an FP load: pop the i32 address, dereference + // `[x28 + uxtw(addr) + offset]` with the SIMD&FP `ldr s/d`, push the value + // into the FP file. + // + // The address arithmetic and the #865 SOFTWARE BOUNDS CHECK are the SAME + // `form_ea` the integer loads use — an FP access is bounds-checked by + // default exactly like an i32 one, and traps (`brk`) where wasmtime traps. + // Only the data register file differs: the destination is a fresh FP temp, + // so the GP `ea` temp is free again the instant the load retires. + let fload = |words: &mut Vec, + stack: &mut Vec, + offset: u32, + size_log2: u32, + ldr_op: fn(FReg, Reg, u32) -> u32| + -> Result<(), SelectError> { + let addr = pop_gp(stack, "fload")?; + let (ea, imm) = form_ea(words, stack, addr, offset, size_log2)?; + // The FP destination lives in a DIFFERENT file than `ea`, so it cannot + // alias it — no read-before-write reuse trick is needed (or possible). + let dst = alloc_ftemp(stack)?; + words.push(ldr_op(dst, ea, imm.unwrap_or(0))); + stack.push(Val::fp(dst)); + Ok(()) + }; + + // v0.54 L2 (#851) — an FP store: pop the FP value, then the i32 address, + // and write `size` bytes to `[x28 + uxtw(addr) + offset]`. Bounds-checked + // by the shared `form_ea` (#865). Unlike the GP store there is no need to + // keep the value artificially live across the EA allocation: `form_ea` + // hands out GP temps only, and the value lives in the FP file. + let fstore = |words: &mut Vec, + stack: &mut Vec, + offset: u32, + size_log2: u32, + str_op: fn(FReg, Reg, u32) -> u32| + -> Result<(), SelectError> { + let val = pop_fp(stack, "fstore")?; + let addr = pop_gp(stack, "fstore")?; + let (ea, imm) = form_ea(words, stack, addr, offset, size_log2)?; + words.push(str_op(val, ea, imm.unwrap_or(0))); + Ok(()) + }; + for op in ops { match op { WasmOp::LocalGet(i) => { @@ -1658,6 +1701,23 @@ pub fn select_typed_cf_calls( WasmOp::I64Store32 { offset, .. } => { store(&mut words, &mut stack, *offset, 2, enc::str_w)? } + // v0.54 L2 (#851) — f32/f64 linear-memory access. Same address + // path and same #865 bounds check as the integer forms; only the + // data register file differs (`ldr/str s` = 4 bytes, `d` = 8). + // WASM float load/store move BIT PATTERNS, so a NaN payload and + // the sign of ±0 survive a round-trip intact. + WasmOp::F32Load { offset, .. } => { + fload(&mut words, &mut stack, *offset, 2, enc::ldr_s)? + } + WasmOp::F32Store { offset, .. } => { + fstore(&mut words, &mut stack, *offset, 2, enc::str_s)? + } + WasmOp::F64Load { offset, .. } => { + fload(&mut words, &mut stack, *offset, 3, enc::ldr_d)? + } + WasmOp::F64Store { offset, .. } => { + fstore(&mut words, &mut stack, *offset, 3, enc::str_d)? + } // --- #851 direct `call` --- // // AAPCS64: pop `argc` integer args off the value stack, marshal them @@ -2196,6 +2256,126 @@ mod tests { assert_eq!(w[0], enc::brk(0)); } + // --- v0.54 L2 (#851): f32/f64 linear-memory access --- + + fn sel_mem_typed( + ops: &[WasmOp], + num_params: u32, + f32s: &[bool], + f64s: &[bool], + bounds: MemBounds, + ) -> Vec { + let (w, _) = + select_typed_cf_calls(ops, num_params, f32s, f64s, &[], 0, &[], &[], &[], bounds) + .unwrap(); + w + } + + #[test] + fn f32_load_is_bounds_checked_then_ldr_s() { + // (param i32) f32.load — the FP load must go through the SAME #865 + // check as i32.load: K = 65536 - 0 - 4 = 65532, compare BEFORE the + // dereference, `brk` on OOB. Then `ldr s16, [x9]` (FP destination, so + // the GP `ea` temp is not reused as the data register). + let ops = vec![ + WasmOp::LocalGet(0), + WasmOp::F32Load { + offset: 0, + align: 2, + }, + WasmOp::End, + ]; + let w = sel_mem_typed( + &ops, + 1, + &[], + &[], + MemBounds::Software { limit_bytes: 65536 }, + ); + assert_eq!( + w, + vec![ + 0x529F_FF89, // mov w9, #65532 + enc::cmp(0, 9), + enc::bcond(Cond::Ls, 2), + enc::brk(0), + enc::add_ext_uxtw(9, LINMEM_BASE, 0), + enc::ldr_s(FTEMPS[0], 9, 0), + enc::fmov_d(0, FTEMPS[0]), + enc::ret(), + ] + ); + } + + #[test] + fn f64_store_is_bounds_checked_with_dword_width() { + // f64.store must account for the 8-byte access width in the bound: + // K = 65536 - 0 - 8 = 65528 (NOT 65532) — an 8-byte store at 65532 + // would run 4 bytes past the limit. + let ops = vec![ + WasmOp::LocalGet(0), // i32 address + WasmOp::LocalGet(1), // f64 value + WasmOp::F64Store { + offset: 0, + align: 3, + }, + WasmOp::End, + ]; + let w = sel_mem_typed( + &ops, + 2, + &[], + &[false, true], + MemBounds::Software { limit_bytes: 65536 }, + ); + assert_eq!(w[0], enc::mov_imm32(9, 65528)[0], "K must be limit - 8"); + assert!(w.contains(&enc::brk(0)), "OOB must trap"); + assert!( + w.contains(&enc::str_d(0, 9, 0)), + "must store the d view of the value register; got {w:#010X?}" + ); + } + + #[test] + fn fp_mem_offset_folds_into_the_scaled_immediate() { + // A size-aligned offset within imm12 range folds into the load: for + // `ldr s` the encoded imm12 is offset/4, for `ldr d` offset/8. + let ops = vec![ + WasmOp::LocalGet(0), + WasmOp::F32Load { + offset: 16, + align: 2, + }, + WasmOp::End, + ]; + let w = sel_mem_typed(&ops, 1, &[], &[], MemBounds::Unchecked); + assert_eq!( + w, + vec![ + enc::add_ext_uxtw(9, LINMEM_BASE, 0), + enc::ldr_s(FTEMPS[0], 9, 4), // imm12 = 16/4 + enc::fmov_d(0, FTEMPS[0]), + enc::ret(), + ] + ); + } + + #[test] + fn fp_store_rejects_a_gp_value_operand() { + // Type confusion guard: an i32 on the stack fed to f32.store must ERROR + // rather than store the wrong register file. + let ops = vec![ + WasmOp::I32Const(0), + WasmOp::I32Const(42), + WasmOp::F32Store { + offset: 0, + align: 2, + }, + WasmOp::End, + ]; + assert!(select_typed(&ops, 0, &[], &[]).is_err()); + } + #[test] fn unchecked_mode_emits_no_trap_check() { // The explicit opt-out stays byte-identical to the pre-#865 lowering. diff --git a/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs b/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs index 52984de0..a5d8f4d6 100644 --- a/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs +++ b/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs @@ -995,8 +995,6 @@ fn a64_extended_surface( op: &WasmOp, ) -> Option<(&'static str, u32, Vec, Result<(), &'static str>)> { // Gap reasons, shared per class. - const FP_MEM: &str = "aarch64 selector has no f32/f64 load/store arm (linear-memory FP access \ - needs LDR/STR (SIMD&FP) forms) — deferred, #851"; const TRAP_TRUNC_I64: &str = "aarch64 selector has no TRAPPING i64-target truncation arm (needs the \ #709-class i64 domain guard; the SATURATING i64 forms do lower) — \ deferred, #851"; @@ -1214,7 +1212,7 @@ fn a64_extended_surface( F32Floor => some("f32.floor", 0, vec![F32Const(1.5), F32Floor], Ok(())), F32Trunc => some("f32.trunc", 0, vec![F32Const(1.5), F32Trunc], Ok(())), F32Nearest => some("f32.nearest", 0, vec![F32Const(1.5), F32Nearest], Ok(())), - // ─── f32 memory — GAP ──────────────────────────────────────────── + // ─── f32 memory — lowered (LDR/STR s, bounds-checked, v0.54 L2) ── F32Load { .. } => some( "f32.load", 0, @@ -1225,7 +1223,7 @@ fn a64_extended_surface( align: 2, }, ], - Err(FP_MEM), + Ok(()), ), F32Store { .. } => some( "f32.store", @@ -1238,7 +1236,7 @@ fn a64_extended_surface( align: 2, }, ], - Err(FP_MEM), + Ok(()), ), // ─── f32 conversions ───────────────────────────────────────────── F32ConvertI32S => some( @@ -1420,7 +1418,7 @@ fn a64_extended_surface( F64Floor => some("f64.floor", 0, vec![F64Const(1.5), F64Floor], Ok(())), F64Trunc => some("f64.trunc", 0, vec![F64Const(1.5), F64Trunc], Ok(())), F64Nearest => some("f64.nearest", 0, vec![F64Const(1.5), F64Nearest], Ok(())), - // ─── f64 memory — GAP ──────────────────────────────────────────── + // ─── f64 memory — lowered (LDR/STR d, bounds-checked, v0.54 L2) ── F64Load { .. } => some( "f64.load", 0, @@ -1431,7 +1429,7 @@ fn a64_extended_surface( align: 3, }, ], - Err(FP_MEM), + Ok(()), ), F64Store { .. } => some( "f64.store", @@ -1444,7 +1442,7 @@ fn a64_extended_surface( align: 3, }, ], - Err(FP_MEM), + Ok(()), ), // ─── f64 conversions ───────────────────────────────────────────── F64ConvertI32S => some( From 5394d42063943ace716bb1a75e51c56fa3959674 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 30 Jul 2026 15:13:26 +0200 Subject: [PATCH 4/8] =?UTF-8?q?feat(aarch64):=20close=20TRAP=5FTRUNC=5FI64?= =?UTF-8?q?=20=E2=80=94=20domain-guarded=20i64-target=20truncations=20(#85?= =?UTF-8?q?1)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit v0.54 L2 step 4 — the soundness-critical class, and the last of the four the VCR-SEL-005 third-backend oracle enumerated. `i64.trunc_f{32,64}_{s,u}` now lower to the `x`-form FCVTZ{S,U} behind the #709 domain guard. WHY A GUARD AND NOT A BARE CONVERT: A64 FCVTZS/FCVTZU are MORE TOTAL than WASM. On NaN they return 0; out of range they SATURATE to INT64_MIN/MAX (or 0/UINT64_MAX). WASM §4.3.3 requires a TRAP for every one of those inputs. Emitting the bare instruction is not an approximation, it is a silent miscompile — the #633/#666/#709/#665/#642 class this project has shipped before. `trunc_guarded` gains a `dst64` parameter so the i64 forms reuse the proven shape verbatim (ordered `b.mi` hi check — FALSE for NaN, so NaN falls into the first `brk` — then the lo check, then the convert). THE BOUNDARY CONSTANTS, each justified rather than copied: * f32->s64 / f64->s64 lo = -2^63, INCLUSIVE (`b.ge`). -2^63 is exactly representable in both formats and truncates to a LEGAL INT64_MIN; a strict bound would trap it. * f64->s64 differs from the i32/f64 row, which needs the STRICT -(2^31)-1 because -2147483648.5 exists. At 2^63 the f64 ULP is 2048, so NO f64 lies in (-2^63-1, -2^63) — the inclusive bound is both exact and necessary. * u64 lo = -1.0, STRICT (`b.gt`): trunc_u(-0.5) = 0 is legal. * hi = 2^63 / 2^64, exclusive — NOT the 2^32 the i32 forms use, which would trap every legal value above 4294967295. Parity-gate entries flipped Err->Ok in the SAME commit (4) and the TRAP_TRUNC_I64 reason constant DELETED. The extended-surface gate now carries only SIMD / multi-memory / call_indirect declines: the SCALAR FLOAT SURFACE IS COMPLETE. The selector's own decline claim (`trapping_i64_truncations_are_loud_declined`) is replaced by three tests that pin the guard instead: two `brk`s per form with the convert strictly AFTER both, the inclusive-vs-strict signed lower bound (both formats), and the 2^64-not-2^32 unsigned upper bound. Execution evidence + CI wiring land in the next commit. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-backend-aarch64/src/selector.rs | 177 +++++++++++++++--- .../tests/cross_backend_op_parity.rs | 11 +- 2 files changed, 157 insertions(+), 31 deletions(-) diff --git a/crates/synth-backend-aarch64/src/selector.rs b/crates/synth-backend-aarch64/src/selector.rs index 7a9646b3..6d2b67b1 100644 --- a/crates/synth-backend-aarch64/src/selector.rs +++ b/crates/synth-backend-aarch64/src/selector.rs @@ -587,10 +587,39 @@ pub fn select_typed_cf_calls( // -2147483648.5, which truncate to -2^31 and are IN-range; an // inclusive -2^31 bound would wrongly trap them). // f64→u: hi 2^32 (0x41F0...0, exclusive), lo -1.0 (0xBFF0...0, strict). + // + // v0.54 L2 (#851): `dst64` extends the SAME guard to the i64-TARGET forms. + // Only the two bound constants and the destination width change — the + // shape (ordered hi check, then lo check, then the bare convert) is + // identical, so the i64 forms inherit the proven NaN handling (an ordered + // `b.mi` is FALSE for NaN, so NaN falls into the first `brk`). + // + // i64 boundary table (WASM Core §4.3.3), each entry justified — the whole + // point is that A64 saturation must never be observable: + // f32→s64: hi 2^63 (0x5F000000, exclusive), lo -2^63 (0xDF000000, + // INCLUSIVE. -2^63 is exactly representable in f32 (exponent + // 63, zero mantissa) and truncates to INT64_MIN, which is + // in-range; the next f32 below it is -2^63·(1+2^-23), far + // outside. So `ge` is exact — a STRICT bound would wrongly trap + // the legal INT64_MIN input.) + // f32→u64: hi 2^64 (0x5F800000, exclusive), lo -1.0 (0xBF800000, STRICT + // — trunc_u(-0.5) = 0 is legal, trunc_u(-1.0) traps). + // f64→s64: hi 2^63 (0x43E0...0, exclusive), lo -2^63 (0xC3E0...0, + // INCLUSIVE. NOTE this differs from the i32/f64 row above, and + // the reason is the ULP: near 2^63 the f64 spacing is + // 2^63·2^-52 = 2048, so NO f64 exists in (-2^63-1, -2^63) — + // unlike the i32 case where -2147483648.5 is representable and + // forced a strict -(2^31)-1 bound. Here the next f64 below + // -2^63 is -2^63-2048, which is genuinely out of range, so an + // inclusive bound is both exact and necessary.) + // f64→u64: hi 2^64 (0x43F0...0, exclusive), lo -1.0 (0xBFF0...0, strict). + // Every row is execution-checked against wasmtime over both sides of each + // boundary in `aarch64_float_completion_851_differential.py`. let trunc_guarded = |words: &mut Vec, stack: &mut Vec, is_f64: bool, - signed: bool| + signed: bool, + dst64: bool| -> Result<(), SelectError> { let a = pop_fp(stack, "trunc")?; // Keep `a` live across temp allocation: it is read by both fcmps and @@ -599,11 +628,15 @@ pub fn select_typed_cf_calls( let dst = alloc_temp(stack)?; // GP: const scratch, then the result let bound = alloc_ftemp(stack)?; stack.pop(); - let (hi_bits, lo_bits, lo_cond): (u64, u64, Cond) = match (is_f64, signed) { - (false, true) => (0x4F00_0000, 0xCF00_0000, Cond::Ge), - (false, false) => (0x4F80_0000, 0xBF80_0000, Cond::Gt), - (true, true) => (0x41E0_0000_0000_0000, 0xC1E0_0000_0020_0000, Cond::Gt), - (true, false) => (0x41F0_0000_0000_0000, 0xBFF0_0000_0000_0000, Cond::Gt), + let (hi_bits, lo_bits, lo_cond): (u64, u64, Cond) = match (is_f64, signed, dst64) { + (false, true, false) => (0x4F00_0000, 0xCF00_0000, Cond::Ge), + (false, false, false) => (0x4F80_0000, 0xBF80_0000, Cond::Gt), + (true, true, false) => (0x41E0_0000_0000_0000, 0xC1E0_0000_0020_0000, Cond::Gt), + (true, false, false) => (0x41F0_0000_0000_0000, 0xBFF0_0000_0000_0000, Cond::Gt), + (false, true, true) => (0x5F00_0000, 0xDF00_0000, Cond::Ge), + (false, false, true) => (0x5F80_0000, 0xBF80_0000, Cond::Gt), + (true, true, true) => (0x43E0_0000_0000_0000, 0xC3E0_0000_0000_0000, Cond::Ge), + (true, false, true) => (0x43F0_0000_0000_0000, 0xBFF0_0000_0000_0000, Cond::Gt), }; let check = |words: &mut Vec, bits: u64, cond: Cond| { if is_f64 { @@ -624,11 +657,15 @@ pub fn select_typed_cf_calls( }; check(words, hi_bits, Cond::Mi); check(words, lo_bits, lo_cond); - words.push(match (is_f64, signed) { - (false, true) => enc::fcvtzs_w_from_s(dst, a), - (false, false) => enc::fcvtzu_w_from_s(dst, a), - (true, true) => enc::fcvtzs_w_from_d(dst, a), - (true, false) => enc::fcvtzu_w_from_d(dst, a), + words.push(match (is_f64, signed, dst64) { + (false, true, false) => enc::fcvtzs_w_from_s(dst, a), + (false, false, false) => enc::fcvtzu_w_from_s(dst, a), + (true, true, false) => enc::fcvtzs_w_from_d(dst, a), + (true, false, false) => enc::fcvtzu_w_from_d(dst, a), + (false, true, true) => enc::fcvtzs_x_from_s(dst, a), + (false, false, true) => enc::fcvtzu_x_from_s(dst, a), + (true, true, true) => enc::fcvtzs_x_from_d(dst, a), + (true, false, true) => enc::fcvtzu_x_from_d(dst, a), }); stack.push(Val::gp(dst)); Ok(()) @@ -1542,10 +1579,19 @@ pub fn select_typed_cf_calls( WasmOp::F64Nearest => funop(&mut words, &mut stack, enc::frintn_d)?, // --- trapping float→int truncations (m4): domain-guarded #709 --- - WasmOp::I32TruncF32S => trunc_guarded(&mut words, &mut stack, false, true)?, - WasmOp::I32TruncF32U => trunc_guarded(&mut words, &mut stack, false, false)?, - WasmOp::I32TruncF64S => trunc_guarded(&mut words, &mut stack, true, true)?, - WasmOp::I32TruncF64U => trunc_guarded(&mut words, &mut stack, true, false)?, + WasmOp::I32TruncF32S => trunc_guarded(&mut words, &mut stack, false, true, false)?, + WasmOp::I32TruncF32U => trunc_guarded(&mut words, &mut stack, false, false, false)?, + WasmOp::I32TruncF64S => trunc_guarded(&mut words, &mut stack, true, true, false)?, + WasmOp::I32TruncF64U => trunc_guarded(&mut words, &mut stack, true, false, false)?, + // v0.54 L2 (#851): the i64-TARGET trapping forms — the same #709 + // domain guard with the 2^63 / 2^64 boundaries and an `x` + // destination. Without the guard these would SATURATE where WASM + // traps (NaN → 0, overflow → INT64_MIN/MAX): the exact silent + // miscompile the class is named for. + WasmOp::I64TruncF32S => trunc_guarded(&mut words, &mut stack, false, true, true)?, + WasmOp::I64TruncF32U => trunc_guarded(&mut words, &mut stack, false, false, true)?, + WasmOp::I64TruncF64S => trunc_guarded(&mut words, &mut stack, true, true, true)?, + WasmOp::I64TruncF64U => trunc_guarded(&mut words, &mut stack, true, false, true)?, // --- nontrapping saturating truncations (#782a): bare FCVTZ --- WasmOp::I32TruncSatF32S => trunc_sat(&mut words, &mut stack, enc::fcvtzs_w_from_s)?, @@ -3116,20 +3162,103 @@ mod tests { } #[test] - fn trapping_i64_truncations_are_loud_declined() { - // The remaining m4 honesty frontier after v0.54 L2 closed rounding and - // the i64-SOURCE converts: the TRAPPING i64-TARGET truncations still - // decline, because A64 FCVTZ{S,U} SATURATE where WASM traps (#709) and - // the i64 domain guard has not landed. Never silent wrong code. - for op in [WasmOp::I64TruncF64S, WasmOp::I64TruncF64U] { - let ops = vec![WasmOp::LocalGet(0), op, WasmOp::End]; + fn trapping_i64_truncations_are_domain_guarded_not_bare() { + // v0.54 L2 (#851) — the soundness-critical half. A64 FCVTZ{S,U} with + // an x destination SATURATE (NaN → 0, overflow → INT64_MIN/MAX) where + // WASM §4.3.3 must TRAP, so each TRAPPING i64-target form must carry + // the two-sided domain guard: exactly TWO `brk`s, and the convert must + // be the LAST instruction before the epilogue (nothing may reach it + // without passing both checks). + for (op, f64_src, cvt) in [ + ( + WasmOp::I64TruncF32S, + false, + enc::fcvtzs_x_from_s as fn(Reg, FReg) -> u32, + ), + (WasmOp::I64TruncF32U, false, enc::fcvtzu_x_from_s), + (WasmOp::I64TruncF64S, true, enc::fcvtzs_x_from_d), + (WasmOp::I64TruncF64U, true, enc::fcvtzu_x_from_d), + ] { + let ops = vec![WasmOp::LocalGet(0), op.clone(), WasmOp::End]; + let (f32s, f64s): (&[bool], &[bool]) = if f64_src { + (&[], &[true]) + } else { + (&[true], &[]) + }; + let w = select_typed(&ops, 1, f32s, f64s).unwrap(); + assert_eq!( + w.iter().filter(|&&x| x == enc::brk(0)).count(), + 2, + "{op:?} needs BOTH range checks; got {w:#010X?}" + ); + let cvt_at = w + .iter() + .position(|&x| x == cvt(9, 0)) + .unwrap_or_else(|| panic!("{op:?} must end in the x-form convert; got {w:#010X?}")); + let last_brk = w.iter().rposition(|&x| x == enc::brk(0)).unwrap(); assert!( - select_typed(&ops, 1, &[], &[true]).is_err(), - "trapping i64-target truncation not yet supported — must loud-decline" + cvt_at > last_brk, + "{op:?}: the convert must sit AFTER both guards" ); } } + #[test] + fn i64_trunc_signed_bounds_are_plus_2pow63_exclusive_minus_2pow63_inclusive() { + // The two constants that decide whether a legal INT64_MIN input traps. + // f32: -2^63 = 0xDF000000 is EXACTLY representable and truncates to + // INT64_MIN (in range) — the bound must be INCLUSIVE (`b.ge`). + let ops = vec![WasmOp::LocalGet(0), WasmOp::I64TruncF32S, WasmOp::End]; + let w = select_typed(&ops, 1, &[true], &[]).unwrap(); + assert!(w.contains(&enc::movk(9, 0x5F00, 1)), "hi bound 2^63 (f32)"); + assert!(w.contains(&enc::movk(9, 0xDF00, 1)), "lo bound -2^63 (f32)"); + assert!( + w.contains(&enc::bcond(Cond::Ge, 2)), + "lo bound is INCLUSIVE" + ); + assert!( + w.contains(&enc::bcond(Cond::Mi, 2)), + "hi bound is ORDERED <" + ); + + // f64: near 2^63 the ULP is 2048, so NO f64 lies in (-2^63-1, -2^63) — + // the bound is the INCLUSIVE -2^63 (0xC3E0...0), NOT the strict + // -(2^63)-1 shape the i32/f64 row needs. + let ops = vec![WasmOp::LocalGet(0), WasmOp::I64TruncF64S, WasmOp::End]; + let w = select_typed(&ops, 1, &[], &[true]).unwrap(); + let hi = enc::mov_imm64(9, 0x43E0_0000_0000_0000); + let lo = enc::mov_imm64(9, 0xC3E0_0000_0000_0000); + assert!(w.windows(hi.len()).any(|s| s == hi.as_slice()), "hi 2^63"); + assert!(w.windows(lo.len()).any(|s| s == lo.as_slice()), "lo -2^63"); + assert!( + w.contains(&enc::bcond(Cond::Ge, 2)), + "lo bound is INCLUSIVE" + ); + } + + #[test] + fn i64_trunc_unsigned_bounds_are_2pow64_and_strict_minus_one() { + // trunc_u accepts (-1, 2^64): trunc_u(-0.5) = 0 is LEGAL, so the lower + // bound is the STRICT -1.0 (`b.gt`), and the upper is 2^64 — NOT the + // 2^32 the i32 forms use (which would trap every legal value above + // 4294967295). + let ops = vec![WasmOp::LocalGet(0), WasmOp::I64TruncF32U, WasmOp::End]; + let w = select_typed(&ops, 1, &[true], &[]).unwrap(); + assert!(w.contains(&enc::movk(9, 0x5F80, 1)), "hi bound 2^64 (f32)"); + assert!( + !w.contains(&enc::movk(9, 0x4F80, 1)), + "must NOT use the 2^32 i32 bound" + ); + assert!(w.contains(&enc::movk(9, 0xBF80, 1)), "lo bound -1.0 (f32)"); + assert!(w.contains(&enc::bcond(Cond::Gt, 2)), "lo bound is STRICT"); + + let ops = vec![WasmOp::LocalGet(0), WasmOp::I64TruncF64U, WasmOp::End]; + let w = select_typed(&ops, 1, &[], &[true]).unwrap(); + let hi = enc::mov_imm64(9, 0x43F0_0000_0000_0000); + assert!(w.windows(hi.len()).any(|s| s == hi.as_slice()), "hi 2^64"); + assert!(w.contains(&enc::bcond(Cond::Gt, 2)), "lo bound is STRICT"); + } + #[test] fn type_confusion_gp_op_on_fp_value_errors() { // An f32 value fed to an integer op must ERROR (never read the wrong diff --git a/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs b/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs index a5d8f4d6..bb123e02 100644 --- a/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs +++ b/crates/synth-backend-riscv/tests/cross_backend_op_parity.rs @@ -995,9 +995,6 @@ fn a64_extended_surface( op: &WasmOp, ) -> Option<(&'static str, u32, Vec, Result<(), &'static str>)> { // Gap reasons, shared per class. - const TRAP_TRUNC_I64: &str = "aarch64 selector has no TRAPPING i64-target truncation arm (needs the \ - #709-class i64 domain guard; the SATURATING i64 forms do lower) — \ - deferred, #851"; const SIMD: &str = "v128/SIMD is not lowered on aarch64 (Advanced-SIMD lowering is a separate \ lane, mirroring the ARM Helium/MVE exclusion) — deferred, #851"; const MULTI_MEM: &str = "multi-memory wrapper (#406): the aarch64 backend has no per-memory base \ @@ -1321,13 +1318,13 @@ fn a64_extended_surface( "i64.trunc_f32_s", 0, vec![F32Const(1.5), I64TruncF32S], - Err(TRAP_TRUNC_I64), + Ok(()), ), I64TruncF32U => some( "i64.trunc_f32_u", 0, vec![F32Const(1.5), I64TruncF32U], - Err(TRAP_TRUNC_I64), + Ok(()), ), // ─── f64 arithmetic / compares — lower (m3/m4, #538) ───────────── @@ -1527,13 +1524,13 @@ fn a64_extended_surface( "i64.trunc_f64_s", 0, vec![F64Const(1.5), I64TruncF64S], - Err(TRAP_TRUNC_I64), + Ok(()), ), I64TruncF64U => some( "i64.trunc_f64_u", 0, vec![F64Const(1.5), I64TruncF64U], - Err(TRAP_TRUNC_I64), + Ok(()), ), // ─── module-context ops — declines with named reasons ──────────── From 1fc58c85041ad5de4d31222702d3f86d30eac376 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 30 Jul 2026 15:13:51 +0200 Subject: [PATCH 5/8] test(aarch64): CI-wired boundary-table oracle for the float-completion surface (#851) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit v0.54 L2 step 5 — the execution evidence for all four closed classes, wired into CI in the SAME commit (#890: v0.53 found three oracles that existed and ran nowhere). `aarch64_float_completion_851_differential.py` — 662 checks, 142 of them TRAP cases, bit-exact against wasmtime under TWO independent oracles: unicorn (UC_ARCH_ARM64, with x28 = linear-memory base) and, on an arm64 host, a real native call per case in a FORKED CHILD so an expected `brk #0` SIGTRAP is observed by the parent and a surprise one is survivable. The soundness-critical half is a full BOUNDARY TABLE, not spot checks. For each trapping i64 truncation: ±2^63 and 2^64 exactly, the nearest representable float strictly INSIDE each bound and the nearest strictly OUTSIDE it (stepped on the true f32 grid via an IEEE total-order key — plain `math.nextafter` walks the far finer f64 grid), ±0, ±inf and NaN. The static expect-trap column is itself validated against wasmtime first, so the table cannot drift vacuous. Rounding is compared BIT-EXACTLY over a halfway table (0.5, 1.5, 2.5, 3.5 and negatives, up to the largest representable halfway value in each format). That is what makes "FRINTN is ties-to-EVEN" a CHECK rather than a claim: a ties-away FRINTA lowering returns 1 and 3 for 0.5 and 2.5 and fails here. ±inf / NaN / 1e30 catch the other classic wrong lowering, a round-trip through an integer. The i64->float converts pin round-to-nearest-even at the 2^24 / 2^53 onsets; the FP-memory cases cover the width-aware bounds split (65532 in-bounds for f32, out for f64) with NaN payload and -0.0 sign preserved through the round-trip. PROVEN NON-VACUOUS BY MUTATION, both directions of wrong: * replace one guarded convert with a bare saturating one -> 18 failures (`A64=0x7fffffffffffffff wasmtime=TRAP`) — the silent miscompile; * make the signed lower bound off-by-one strict -> 4 failures (`A64=TRAP wasmtime=0x8000000000000000`) — the over-trap. The harness also carries its own floors (>=300 checks, >=40 trap cases, every class non-empty) and hard-fails if the compile SKIPS any function. CI: `set -o pipefail`, `tee`, and a grep + numeric assertion on the check and trap counts, so an oracle that silently stops exercising anything goes red instead of green. The decline-matrix honesty oracle is repointed: rounding, f32/f64 load/store, i64->float converts and the trapping i64 truncations are no longer declines, so keeping them there would be a stale claim. It now pins the STRUCTURAL declines end-to-end — call_indirect, br_table, writing a param local, globals, memory.fill, a value-carrying block, SIMD — 7/7 loud. (The param-write case needed a body that also READS the param: a write-only local 0 is indistinguishable from a fresh non-param local and lowers correctly as one.) Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .github/workflows/ci.yml | 30 +- .../repro/aarch64_float_completion_851.wat | 58 ++ ...rch64_float_completion_851_differential.py | 566 ++++++++++++++++++ scripts/repro/aarch64_m2_decline_538.py | 79 ++- 4 files changed, 702 insertions(+), 31 deletions(-) create mode 100644 scripts/repro/aarch64_float_completion_851.wat create mode 100644 scripts/repro/aarch64_float_completion_851_differential.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index c61c6844..27b4ae49 100644 --- a/.github/workflows/ci.yml +++ b/.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,28 @@ 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. + # + # `pipefail` + a grep asserting a NON-ZERO, non-collapsed check count: + # an oracle that silently stops exercising anything must go red (#890). + run: | + set -o pipefail + SYNTH=./target/debug/synth python scripts/repro/aarch64_float_completion_851_differential.py \ + | tee /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:-0}" -ge 300 ] || { echo "oracle ran too few checks ($n)"; exit 1; } + [ "${t:-0}" -ge 40 ] || { echo "oracle ran too few TRAP cases ($t)"; exit 1; } - name: Run decline-matrix honesty oracle run: SYNTH=./target/debug/synth python scripts/repro/aarch64_m2_decline_538.py diff --git a/scripts/repro/aarch64_float_completion_851.wat b/scripts/repro/aarch64_float_completion_851.wat new file mode 100644 index 00000000..3586da5f --- /dev/null +++ b/scripts/repro/aarch64_float_completion_851.wat @@ -0,0 +1,58 @@ +;; v0.54 L2 (#851) — the aarch64 float-completion surface: the four classes the +;; VCR-SEL-005 third-backend op-parity oracle enumerated as Err(reason). +;; +;; ROUNDING f{32,64}.{ceil,floor,trunc,nearest} -> FRINT{P,M,Z,N} +;; I64_TO_FP f{32,64}.convert_i64_{s,u} -> SCVTF/UCVTF (x) +;; TRAP_TRUNC_I64 i64.trunc_f{32,64}_{s,u} -> guarded FCVTZ (x) +;; FP_MEM f{32,64}.{load,store} -> LDR/STR s|d +;; +;; The FP_MEM functions round-trip a value through linear memory so a wrong +;; width, a wrong register file or a dropped bounds check all show up as a +;; value/trap mismatch. Address 65532 is deliberately IN bounds for f32 and OUT +;; for f64 on this one-page memory. +(module + (memory 1 1) + + ;; --- rounding --- + (func (export "f32_ceil") (param f32) (result f32) (f32.ceil (local.get 0))) + (func (export "f32_floor") (param f32) (result f32) (f32.floor (local.get 0))) + (func (export "f32_trunc") (param f32) (result f32) (f32.trunc (local.get 0))) + (func (export "f32_nearest") (param f32) (result f32) (f32.nearest (local.get 0))) + (func (export "f64_ceil") (param f64) (result f64) (f64.ceil (local.get 0))) + (func (export "f64_floor") (param f64) (result f64) (f64.floor (local.get 0))) + (func (export "f64_trunc") (param f64) (result f64) (f64.trunc (local.get 0))) + (func (export "f64_nearest") (param f64) (result f64) (f64.nearest (local.get 0))) + + ;; --- i64 -> float converts --- + (func (export "f32_convert_i64_s") (param i64) (result f32) + (f32.convert_i64_s (local.get 0))) + (func (export "f32_convert_i64_u") (param i64) (result f32) + (f32.convert_i64_u (local.get 0))) + (func (export "f64_convert_i64_s") (param i64) (result f64) + (f64.convert_i64_s (local.get 0))) + (func (export "f64_convert_i64_u") (param i64) (result f64) + (f64.convert_i64_u (local.get 0))) + + ;; --- TRAPPING i64-target truncations (the soundness-critical class) --- + (func (export "i64_trunc_f32_s") (param f32) (result i64) + (i64.trunc_f32_s (local.get 0))) + (func (export "i64_trunc_f32_u") (param f32) (result i64) + (i64.trunc_f32_u (local.get 0))) + (func (export "i64_trunc_f64_s") (param f64) (result i64) + (i64.trunc_f64_s (local.get 0))) + (func (export "i64_trunc_f64_u") (param f64) (result i64) + (i64.trunc_f64_u (local.get 0))) + + ;; --- FP linear memory (store then load back from the same address) --- + (func (export "f32_mem_rt") (param i32 f32) (result f32) + (f32.store (local.get 0) (local.get 1)) + (f32.load (local.get 0))) + (func (export "f64_mem_rt") (param i32 f64) (result f64) + (f64.store (local.get 0) (local.get 1)) + (f64.load (local.get 0))) + ;; A non-zero static memarg offset: exercises the scaled-imm12 fold AND the + ;; offset accounting inside the bounds constant K. + (func (export "f32_mem_off") (param i32 f32) (result f32) + (f32.store offset=16 (local.get 0) (local.get 1)) + (f32.load offset=16 (local.get 0))) +) diff --git a/scripts/repro/aarch64_float_completion_851_differential.py b/scripts/repro/aarch64_float_completion_851_differential.py new file mode 100644 index 00000000..42ab916b --- /dev/null +++ b/scripts/repro/aarch64_float_completion_851_differential.py @@ -0,0 +1,566 @@ +#!/usr/bin/env python3 +"""v0.54 L2 (#851) — the aarch64 float-completion EXECUTION differential. + +Closes the four classes the VCR-SEL-005 third-backend op-parity oracle listed as +`Err(reason)`: + + ROUNDING f{32,64}.{ceil,floor,trunc,nearest} -> FRINT{P,M,Z,N} + I64_TO_FP f{32,64}.convert_i64_{s,u} -> SCVTF/UCVTF (x-form) + TRAP_TRUNC_I64 i64.trunc_f{32,64}_{s,u} -> DOMAIN-GUARDED FCVTZ + FP_MEM f{32,64}.{load,store} -> LDR/STR s|d, bounds-checked + +The fatal class this gates is TRAP_TRUNC_I64. A64 `FCVTZS`/`FCVTZU` are MORE +TOTAL than WASM: on NaN they return 0 and out of range they SATURATE to +INT64_MIN/MAX (or 0/UINT64_MAX), where WASM Core §4.3.3 requires a TRAP. So this +harness runs a FULL BOUNDARY TABLE per trapping op — both sides of ±2^63 / 2^64, +the largest float strictly inside each bound, the smallest strictly outside, +±0, ±inf and NaN — and requires the trap cases to ACTUALLY TRAP. + +Two independent oracles, exactly as the m4 harness does: + (1) unicorn (UC_ARCH_ARM64): the guard's `brk #0` surfaces as UC_ERR_EXCEPTION; + (2) natively on an arm64 host, EVERY call in a forked child, so an expected + SIGTRAP is observed by the parent and a surprise trap is survivable. +The FP_MEM functions need `x28` = linear-memory base, which a plain native call +cannot establish, so they run under unicorn only (where x28 is set explicitly) — +their OOB cases are trap-checked the same way. + +The static expect-trap column is VALIDATED AGAINST WASMTIME FIRST: if wasmtime +disagrees with the table, the FIXTURE is declared wrong (loud), so the boundary +table cannot silently drift vacuous. + +Rounding is compared bit-exactly, which is what makes the `nearest` claim real: +FRINTN is round-to-nearest-TIES-TO-EVEN. The halfway table (0.5, 1.5, 2.5, 3.5 +and negatives) DISTINGUISHES it from FRINTA (ties-away) — under FRINTA, 0.5 and +2.5 would come back 1 and 3 and this harness would fail. + +Run (needs wasmtime + unicorn + pyelftools; the native leg needs an arm64 host): + SYNTH=/debug/synth python scripts/repro/aarch64_float_completion_851_differential.py +""" + +import ctypes +import math +import os +import platform +import signal +import struct +import subprocess +import sys +from pathlib import Path + +import wasmtime +from elftools.elf.elffile import ELFFile +from unicorn import UC_ARCH_ARM64, UC_MODE_ARM, Uc, UcError +from unicorn.arm64_const import ( + UC_ARM64_REG_CPACR_EL1, + UC_ARM64_REG_D0, + UC_ARM64_REG_LR, + UC_ARM64_REG_S0, + UC_ARM64_REG_SP, + UC_ARM64_REG_V0, + UC_ARM64_REG_V1, + UC_ARM64_REG_X0, + UC_ARM64_REG_X1, + UC_ARM64_REG_X28, +) + +WAT = Path(__file__).with_name("aarch64_float_completion_851.wat") +SYNTH = os.environ.get("SYNTH", "./target/debug/synth") +CODE, STK, RET, LINMEM = 0x100000, 0x200000, 0x300000, 0x1000000 +LINMEM_SIZE = 0x20000 # 128 KiB mapped; the module declares 1 page (64 KiB) +V_ARGS = [UC_ARM64_REG_V0, UC_ARM64_REG_V1] +X_ARGS = [UC_ARM64_REG_X0, UC_ARM64_REG_X1] + +M32 = (1 << 32) - 1 +M64 = (1 << 64) - 1 +INF = float("inf") +NAN = float("nan") +TRAP = "TRAP" + +PAGE = 65536 + + +def f32(x): + """Round a Python float to the nearest f32 (so the table means what it says).""" + return struct.unpack(" x else -1)) & M32 + b = (key & 0x7FFFFFFF) if (key & 0x80000000) else (~key & M32) + return struct.unpack(" ([arg types], ret type). +SIGS = { + "f32_ceil": (["f32"], "f32"), + "f32_floor": (["f32"], "f32"), + "f32_trunc": (["f32"], "f32"), + "f32_nearest": (["f32"], "f32"), + "f64_ceil": (["f64"], "f64"), + "f64_floor": (["f64"], "f64"), + "f64_trunc": (["f64"], "f64"), + "f64_nearest": (["f64"], "f64"), + "f32_convert_i64_s": (["i64"], "f32"), + "f32_convert_i64_u": (["i64"], "f32"), + "f64_convert_i64_s": (["i64"], "f64"), + "f64_convert_i64_u": (["i64"], "f64"), + "i64_trunc_f32_s": (["f32"], "i64"), + "i64_trunc_f32_u": (["f32"], "i64"), + "i64_trunc_f64_s": (["f64"], "i64"), + "i64_trunc_f64_u": (["f64"], "i64"), + "f32_mem_rt": (["i32", "f32"], "f32"), + "f64_mem_rt": (["i32", "f64"], "f64"), + "f32_mem_off": (["i32", "f32"], "f32"), +} + +# Functions that touch linear memory: unicorn-only (they need x28 on entry). +MEM_FNS = {"f32_mem_rt", "f64_mem_rt", "f32_mem_off"} + +# --------------------------------------------------------------------------- # +# ROUNDING table. The halfway values are the load-bearing part: WASM `nearest` +# is roundTiesToEven, so 0.5 -> 0, 1.5 -> 2, 2.5 -> 2, 3.5 -> 4. A ties-AWAY +# implementation (A64 FRINTA) gives 1 and 3 for 0.5 / 2.5 and fails here. +# The large / infinite / NaN entries catch the other classic wrong lowering: a +# round-trip through a 32-bit integer (which SATURATES) instead of a real +# round-to-integral. +ROUND_VALS_F32 = [ + 0.0, -0.0, 0.5, -0.5, 1.5, -1.5, 2.5, -2.5, 3.5, -3.5, + 0.4999999, -0.4999999, 1.0, -1.0, 1.1, -1.1, 1.9, -1.9, + 8388607.5, # largest f32 halfway case (2^23 - 0.5) + float(2 ** 23), float(2 ** 24), -float(2 ** 24), + float(2 ** 31), -float(2 ** 31), float(2 ** 63), -float(2 ** 63), + 1e30, -1e30, INF, -INF, NAN, +] +ROUND_VALS_F64 = [ + 0.0, -0.0, 0.5, -0.5, 1.5, -1.5, 2.5, -2.5, 3.5, -3.5, + 0.49999999999999994, -0.49999999999999994, 1.0, -1.0, 1.9, -1.9, + 4503599627370495.5, # largest f64 halfway case (2^52 - 0.5) + float(2 ** 52), float(2 ** 53), -float(2 ** 53), + float(2 ** 31) + 0.5, -float(2 ** 31) - 0.5, + float(2 ** 63), -float(2 ** 63), 1e300, -1e300, INF, -INF, NAN, +] + +# --------------------------------------------------------------------------- # +# I64 -> FLOAT table. Above 2^24 (f32) / 2^53 (f64) the convert must ROUND, and +# WASM requires round-to-nearest-EVEN — the ties entries below pin it. +CONVERT_VALS = [ + 0, 1, -1, 2, -2, 42, -42, + 2 ** 23, 2 ** 24, 2 ** 24 + 1, 2 ** 24 + 3, # f32 rounding onset + -(2 ** 24) - 1, -(2 ** 24) - 3, + 2 ** 52, 2 ** 53, 2 ** 53 + 1, 2 ** 53 + 3, # f64 rounding onset + -(2 ** 53) - 1, -(2 ** 53) - 3, + 2 ** 62, -(2 ** 62), + 2 ** 63 - 1, -(2 ** 63), # i64 extremes + 2 ** 63, 2 ** 64 - 1, 2 ** 64 - 1024, # only meaningful unsigned +] + +# --------------------------------------------------------------------------- # +# THE #709 i64 BOUNDARY TABLE (WASM Core §4.3.3 trunc_s / trunc_u domains). +# +# Signed: valid iff -2^63 <= x < 2^63 (lower bound INCLUSIVE) +# Unsigned: valid iff -1 < x < 2^64 (lower bound STRICT: trunc_u(-0.5)=0) +# +# The entries that matter most, and why: +# * -2^63 is EXACTLY representable in both f32 and f64 and is IN range — an +# off-by-one strict lower bound would trap a legal INT64_MIN input. +# * The next float BELOW -2^63 is out of range and must trap. In f32 that is +# -2^63·(1+2^-23); in f64 it is -2^63-2048 (the f64 ULP at that magnitude is +# 2048, which is exactly why the f64 lower bound can be inclusive here while +# the i32/f64 row needed a strict -(2^31)-1). +# * +2^63 itself TRAPS for signed (it is one past the top) but is IN range for +# unsigned; +2^64 traps for both. +# * NaN and ±inf always trap. +F32_2_63 = f32(2.0 ** 63) +F32_2_64 = f32(2.0 ** 64) +F64_2_63 = 2.0 ** 63 +F64_2_64 = 2.0 ** 64 + +TRUNC_TABLE = { + "i64_trunc_f32_s": { + "in": [0.0, -0.0, 0.5, -0.5, 1.9, -1.9, 100.75, + f32_next(F32_2_63, 0.0), # largest in-range f32 + -F32_2_63, # INT64_MIN, exactly representable + f32(2 ** 62), f32(-(2 ** 62))], + "trap": [F32_2_63, # +2^63 is OUT (exclusive) + f32_next(-F32_2_63, -INF), # first f32 below -2^63 + F32_2_64, -F32_2_64, 1e30, -1e30, INF, -INF, NAN], + }, + "i64_trunc_f32_u": { + "in": [0.0, -0.0, 0.5, -0.5, -0.9, 1.9, 42.0, + F32_2_63, # in range unsigned + f32_next(F32_2_64, 0.0), # largest in-range f32 + f32(2 ** 24)], + "trap": [-1.0, -1.5, F32_2_64, 1e30, -1e30, INF, -INF, NAN], + }, + "i64_trunc_f64_s": { + "in": [0.0, -0.0, 0.5, -0.5, 1.9, -1.9, + math.nextafter(F64_2_63, 0.0), # largest in-range f64 + -F64_2_63, # INT64_MIN, exactly representable + float(2 ** 62), -float(2 ** 62), + 9007199254740993.0], + "trap": [F64_2_63, + math.nextafter(-F64_2_63, -INF), # -2^63 - 2048 + F64_2_64, -F64_2_64, 1e300, -1e300, INF, -INF, NAN], + }, + "i64_trunc_f64_u": { + "in": [0.0, -0.0, 0.5, -0.5, -0.9, 1.9, + F64_2_63, + math.nextafter(F64_2_64, 0.0), # largest in-range f64 + float(2 ** 53)], + "trap": [-1.0, -1.5, F64_2_64, 1e300, -1e300, INF, -INF, NAN], + }, +} + +# --------------------------------------------------------------------------- # +# FP_MEM table. 65532 is IN bounds for a 4-byte access and OUT for an 8-byte +# one on this one-page memory — the width-aware half of the #865 bound. The +# offset=16 variant must additionally fold 16 into the compile-time constant. +MEM_ADDRS = [0, 4, 8, 4096, PAGE - 8, PAGE - 4, PAGE - 1, PAGE, 0xFFFFFFFF] +MEM_VALS = [1.5, -1.5, 0.0, -0.0, INF, -INF, NAN, 3.14159265, 1e30] + + +def cases_for(fn): + """Yield (args, expect_trap) for a function; expect_trap is False for the + total ops (the table has no opinion there — but wasmtime still validates it).""" + if fn in TRUNC_TABLE: + for v in TRUNC_TABLE[fn]["in"]: + yield [v], False + for v in TRUNC_TABLE[fn]["trap"]: + yield [v], True + elif fn.endswith(("_ceil", "_floor", "_trunc", "_nearest")): + vals = ROUND_VALS_F32 if fn.startswith("f32") else ROUND_VALS_F64 + for v in vals: + yield [v], False + elif "convert_i64" in fn: + for v in CONVERT_VALS: + yield [v], False + elif fn in MEM_FNS: + off = 16 if fn.endswith("_off") else 0 + size = 8 if fn.startswith("f64") else 4 + for a in MEM_ADDRS: + for v in MEM_VALS: + yield [a, v], (a + off + size) > PAGE + else: + raise AssertionError(f"no case generator for {fn}") + + +# --------------------------------------------------------------------------- # +# encoding helpers +def f32_bits(x): + return struct.unpack(" child dies + if ret == "f32": + bits = f32_bits(r) + elif ret == "f64": + bits = f64_bits(r) + else: + bits = int(r) & (M64 if ret == "i64" else M32) + os.write(wr, struct.pack("float " + "converts, DOMAIN-GUARDED i64 truncations (boundary table, traps " + "execution-verified) and bounds-checked FP memory all match wasmtime" + if not fails else f"FAIL ({fails})") + sys.exit(1 if fails else 0) + + +if __name__ == "__main__": + main() diff --git a/scripts/repro/aarch64_m2_decline_538.py b/scripts/repro/aarch64_m2_decline_538.py index a243769d..e186d37e 100755 --- a/scripts/repro/aarch64_m2_decline_538.py +++ b/scripts/repro/aarch64_m2_decline_538.py @@ -2,18 +2,16 @@ # ci-status: wired """#538 milestone-2 — assert the aarch64 decline matrix stays HONEST. -The broadening in m2 covers the full i32/i64 integer ALU, but four classes are -DELIBERATELY still declined, and the contract is that they LOUD-decline (a -non-zero exit / "skipping" / compile error) — never silently emit wrong code: +Some WASM constructs are DELIBERATELY not lowered on aarch64, and the contract +is that each LOUD-declines (a non-zero exit / "skipping" / compile error) — +never silently emits wrong code. - - div/rem (i32+i64): A64 SDIV/UDIV do not trap on /0 or INT_MIN/-1; WASM must - trap. Naive lowering = the "more-total-than-WASM" silent-miscompile class. - - popcnt: no scalar A64 popcount pre-SVE. - - f32/f64 scalar ops: dropped at the decoder (`_ => None`) → the backend - refuses to emit a partial body (#369/#554). - -This harness compiles a module per declined op and asserts the compile FAILS -(loud), so a future accidental silent-lowering of any of them is caught. +This harness compiles a module per declined construct and asserts the compile +FAILS, so a future accidental silent-lowering of any of them is caught. The +list SHRINKS as capability lands: an entry whose gap has closed is a stale +claim and must be deleted in the same commit that closes it (this file is the +end-to-end companion of the VCR-SEL-005 `a64_extended_surface` gate, which +enforces the same both-directions contract at the selector level). Run: SYNTH=/debug/synth python scripts/repro/aarch64_m2_decline_538.py """ @@ -25,25 +23,48 @@ SYNTH = os.environ.get("SYNTH", "./target/debug/synth") # Each entry: (label, wat body). All must FAIL to compile with -b aarch64. +# #851 landed div/rem (SDIV/UDIV+MSUB with the WASM ÷0 + INT_MIN/-1 trap +# guards), popcnt (SIMD CNT/ADDV) and f64<->i64 reinterpret; m3 (#787) the +# non-trapping scalar floats; m4 the #709-class trapping i32 truncations + +# FMIN/FMAX + copysign; and v0.54 L2 the last four scalar-float classes — +# rounding (FRINT{P,M,Z,N}), f32/f64 load/store (bounds-checked LDR/STR s|d), +# i64->float converts (x-form SCVTF/UCVTF) and the DOMAIN-GUARDED trapping +# i64-target truncations. Each moved off this list the day it landed; they are +# now execution-verified in aarch64_float_completion_851_differential.py. +# +# What DELIBERATELY stays declined, and why: DECLINED = [ - # #851 landed div/rem (SDIV/UDIV+MSUB with WASM ÷0 + INT_MIN/-1 trap - # guards), popcnt (SIMD CNT/ADDV), and f64<->i64 reinterpret — those are - # now SUPPORTED and execution-verified (aarch64_divrem_851_differential.py - # + the native matrix), so they moved off this honesty list. m3 (#787) - # landed non-trapping scalar floats; m4 landed the #709-class conversions - # (domain-guarded i32.trunc_f32/f64_s/u, FMIN/FMAX, copysign). The honesty - # gate now covers what DELIBERATELY stays declined: - # - rounding (ceil/floor/trunc/nearest): f64.floor is DECODED and must - # loud-decline at the aarch64 SELECTOR; f32.floor is dropped at decode - # (both paths must stay loud, never silent). - # - i64<->float conversions: need i64-width FCVTZS/SCVTF forms + the - # 64-bit boundary guards (a later increment). - ("f64.floor", '(func (export "f") (param f64) (result f64) ' - '(f64.floor (local.get 0)))'), - ("f32.floor", '(func (export "f") (param f32) (result f32) ' - '(f32.floor (local.get 0)))'), - ("i64.trunc_f64_s", '(func (export "f") (param f64) (result i64) ' - '(i64.trunc_f64_s (local.get 0)))'), + # No function-table substrate + no type/null/OOB trap guards (§4.4.8). + ("call_indirect", + '(type $t (func (param i32) (result i32)))' + '(table 1 funcref)' + '(func (export "f") (param i32) (result i32) ' + '(call_indirect (type $t) (local.get 0) (i32.const 0)))'), + # Jump-table dispatch is not lowered. + ("br_table", '(func (export "f") (param i32) (result i32) ' + '(block (block (br_table 0 1 (local.get 0))) ' + '(return (i32.const 1))) (i32.const 2))'), + # Params live in arg registers BY REFERENCE on the value stack, so writing + # one could alias a stacked value; param homing is the prerequisite. The + # body must READ the param too — a write-only local 0 is indistinguishable + # from a fresh non-param local (and lowers correctly as one). + ("local.set on a param", + '(func (export "f") (param i32) (result i32) ' + '(local.set 0 (i32.add (local.get 0) (i32.const 1))) (local.get 0))'), + # No globals substrate (no data section / global-region addressing). + ("global.get", '(global $g (mut i32) (i32.const 5))' + '(func (export "f") (result i32) (global.get $g))'), + # Bulk memory (#374) is not lowered on aarch64. + ("memory.fill", '(memory 1)(func (export "f") ' + '(memory.fill (i32.const 0) (i32.const 0) (i32.const 4)))'), + # A value-carrying block needs result-register reconciliation across the + # branch (also the #554 float-honesty fixture's construct). + ("block (result f32)", '(func (export "f") (param f32) (result f32) ' + '(block (result f32) (local.get 0)))'), + # v128/SIMD has no aarch64 lowering (Advanced-SIMD is a separate lane). + ("f32x4.add", '(func (export "f") (param f32) (result f32) ' + '(f32x4.extract_lane 0 (f32x4.add ' + '(f32x4.splat (local.get 0)) (f32x4.splat (local.get 0)))))'), ] From 6140447c98d1e944b41ce80a0caf54cb8e00583e Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 30 Jul 2026 15:14:05 +0200 Subject: [PATCH 6/8] docs(aarch64): matrix + feature-matrix template + CHANGELOG for the float completion (#851) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit v0.54 L2 step 6 — close the claims. gale's acceptance matrix (`scripts/repro/aarch64_matrix.sh`) exercises the 16 newly-lowering ops: f32/f64 rounding and the i64->float converts through reinterpret wrappers so the compare is BIT-EXACT (±0 sign and NaN passthrough included), and the four trapping i64 truncations through a new `trap64` helper that normalizes both sides (the JIT runner's signal handler prints TRAP; wasmtime exits non-zero with empty stdout) so a trap DISAGREEMENT is reported as a miscompile instead of vanishing into an unnoticed empty string. 45 -> 61 ops accepted, 119 -> 355 native checks, DECLINED FRONTIER NOW EMPTY. Red-first: the same bare-saturating-convert mutation makes the matrix exit 1 with 7 named `s=,w=TRAP` miscompiles, so the new trap helper is not vacuous shell. f32/f64 LOAD/STORE are deliberately NOT in the matrix and the script says why: they need `x28` = linear-memory base on entry, which the bare JIT runner cannot establish. They are execution-verified under unicorn in the differential. `scripts/templates/feature_matrix.md.tmpl` (the TEMPLATE — the generated docs/status/FEATURE_MATRIX.md is regenerated by the coordinator, #805): the aarch64 row's Declines list no longer names rounding, f32/f64 load/store, i64->float converts or trapping i64-target truncations — those four claims are now false. The capability text states the scalar float surface is COMPLETE and names the evidence; the memory clause records that f32/f64 accesses are bounds-checked by the same path as the integer ones. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- CHANGELOG.md | 62 ++++++++++++++++++++++++ scripts/repro/aarch64_matrix.sh | 55 +++++++++++++++++++++ scripts/templates/feature_matrix.md.tmpl | 2 +- 3 files changed, 118 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 68f5cdd3..85092f7e 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/scripts/repro/aarch64_matrix.sh b/scripts/repro/aarch64_matrix.sh index ad655a2b..c73623ab 100755 --- a/scripts/repro/aarch64_matrix.sh +++ b/scripts/repro/aarch64_matrix.sh @@ -109,6 +109,61 @@ lop2 extend16_s "(i64.extend16_s (local.get 0))" 40000 0 32767 0 # f32 select through the reinterpret wrapper: NaN vs 1.0 both directions. op2 f32.select "(i32.reinterpret_f32 (select (f32.reinterpret_i32 (local.get 0))(f32.reinterpret_i32 (local.get 1))(i32.lt_u (local.get 0)(local.get 1))))" 2143289344 1065353216 1065353216 2143289344 0 2147483648 +# --- v0.54 L2 (#851): the float-completion surface --- +# f32/f64 rounding, i64->float converts and the TRAPPING i64-target +# truncations. Args and results travel as BIT PATTERNS through reinterprets, so +# the comparison is bit-exact (±0 sign and NaN passthrough included). +# f32/f64 LOAD/STORE are deliberately NOT here: they need `x28` = linear-memory +# base on entry, which this bare JIT runner cannot establish — they are +# execution-verified under unicorn in +# scripts/repro/aarch64_float_completion_851_differential.py. + +# unary f32 op, i32 bit pattern in and out. +fop1(){ local nm="$1" op="$2"; shift 2; local h; h=$(hexof '(param i32)(result i32)' "(i32.reinterpret_f32 ($op (f32.reinterpret_i32 (local.get 0))))"); [ -z "$h" ]&&{ dec="$dec $nm";return;}; acc=$((acc+1)) + for a in "$@"; do local g o gh oh; g=$("$W/r32" "$h" "$(sd $a)" 0 2>/dev/null); o=$("$WASMTIME" run --invoke f "$W/t.wasm" "$(sd $a)" 2>/dev/null); gh=$(printf '%08x' $((g&0xffffffff)) 2>/dev/null); oh=$(printf '%08x' $((o&0xffffffff)) 2>/dev/null); n=$((n+1)); [ "$gh" = "$oh" ]||bad="$bad $nm(0x$(printf '%08x' $((a&0xffffffff)))):s=0x$gh,w=0x$oh"; done; } +# unary f64 op, i64 bit pattern in and out. +dop1(){ local nm="$1" op="$2"; shift 2; local h; h=$(hexof '(param i64 i64)(result i64)' "(i64.reinterpret_f64 ($op (f64.reinterpret_i64 (local.get 0))))"); [ -z "$h" ]&&{ dec="$dec $nm";return;}; acc=$((acc+1)) + for a in "$@"; do local g o; g=$("$W/r64" "$h" "$a" 0 2>/dev/null); o=$("$WASMTIME" run --invoke f "$W/t.wasm" "$a" 0 2>/dev/null); n=$((n+1)); [ "$g" = "$o" ]||bad="$bad $nm($a):s=$g,w=$o"; done; } +# i64-in / i64-bit-pattern-out (the i64->float converts, compared bit-exactly). +cvt64(){ local nm="$1" b="$2"; shift 2; local h; h=$(hexof '(param i64 i64)(result i64)' "$b"); [ -z "$h" ]&&{ dec="$dec $nm";return;}; acc=$((acc+1)) + for a in "$@"; do local g o; g=$("$W/r64" "$h" "$a" 0 2>/dev/null); o=$("$WASMTIME" run --invoke f "$W/t.wasm" "$a" 0 2>/dev/null); n=$((n+1)); [ "$g" = "$o" ]||bad="$bad $nm($a):s=$g,w=$o"; done; } +# TRAPPING op: the JIT runner's signal handler prints TRAP; wasmtime exits +# non-zero with no stdout. Normalize both so a "traps where wasmtime traps" +# disagreement is a MISCOMPILE, not an unnoticed empty string. +trap64(){ local nm="$1" b="$2"; shift 2; local h; h=$(hexof '(param i64 i64)(result i64)' "$b"); [ -z "$h" ]&&{ dec="$dec $nm";return;}; acc=$((acc+1)) + for a in "$@"; do local g o; g=$("$W/r64" "$h" "$a" 0 2>/dev/null); o=$("$WASMTIME" run --invoke f "$W/t.wasm" "$a" 0 2>/dev/null); [ -z "$o" ]&&o=TRAP; [ -z "$g" ]&&g=TRAP; n=$((n+1)); [ "$g" = "$o" ]||bad="$bad $nm($a):s=$g,w=$o"; done; } + +# Rounding. The halfway values are load-bearing: WASM `nearest` is +# ties-to-EVEN, so 0.5->0, 1.5->2, 2.5->2, 3.5->4 — a ties-away lowering +# (A64 FRINTA instead of FRINTN) fails exactly here. ±inf/NaN/1e30 catch the +# other classic wrong lowering, a round-trip through a 32-bit integer. +F32R="1056964608 1069547520 1075838976 1080033280 3204448256 3217031168 3223322624 3227516928 1072902963 3220386611 0 2147483648 2139095040 4286578688 2143289344 1900671690 4048155338 1258291199" +for r in ceil floor trunc nearest; do fop1 "f32.$r" "f32.$r" $F32R; done +F64R="4602678819172646912 4609434218613702656 4612811918334230528 4615063718147915776 -4620693217682128896 -4613937818241073152 4611235658464650854 -4612136378390124954 9218868437227405312 -4503599627370496 9221120237041090560 9094988921128908188 4841369599423283199" +for r in ceil floor trunc nearest; do dop1 "f64.$r" "f64.$r" $F64R; done + +# i64 -> float converts. Above 2^24 (f32) / 2^53 (f64) the convert must ROUND +# to nearest-EVEN; the ±1/±3 offsets past each onset pin that. +CVTV="0 1 -1 16777216 16777217 16777219 -16777217 -16777219 9007199254740992 9007199254740993 9007199254740995 4611686018427387904 9223372036854775807 -9223372036854775808" +cvt64 f64.convert_i64_s "(i64.reinterpret_f64 (f64.convert_i64_s (local.get 0)))" $CVTV +cvt64 f64.convert_i64_u "(i64.reinterpret_f64 (f64.convert_i64_u (local.get 0)))" $CVTV +cvt64 f32.convert_i64_s "(i64.extend_i32_u (i32.reinterpret_f32 (f32.convert_i64_s (local.get 0))))" $CVTV +cvt64 f32.convert_i64_u "(i64.extend_i32_u (i32.reinterpret_f32 (f32.convert_i64_u (local.get 0))))" $CVTV + +# TRAPPING i64-target truncations — the soundness-critical class. A64 +# FCVTZ{S,U} SATURATE where WASM traps, so every out-of-range/NaN input below +# MUST trap; the in-range ones must match bit-exactly. Inputs are f64/f32 bit +# patterns: ±2^63 and ±2^64 exactly, the nearest representable value strictly +# inside each bound, -1.0/-0.5 (the strict unsigned lower bound), ±inf, NaN. +# (The full both-sides-of-every-boundary table lives in the differential; this +# is gale's on-silicon confirmation that traps really fire.) +T64D="4890909195324358656 4890909195324358655 -4332462841530417152 -4332462841530417151 4895412794951729152 4895412794951729151 -4616189618054758400 -4620693217682128896 9218868437227405312 -4503599627370496 9221120237041090560 0 -9223372036854775808 4886405595696988160" +trap64 i64.trunc_f64_s "(i64.trunc_f64_s (f64.reinterpret_i64 (local.get 0)))" $T64D +trap64 i64.trunc_f64_u "(i64.trunc_f64_u (f64.reinterpret_i64 (local.get 0)))" $T64D +T64S="1593835520 1593835519 3741319168 3741319169 1602224128 1602224127 3212836864 3204448256 2139095040 4286578688 2143289344 0 2147483648 1266679808" +trap64 i64.trunc_f32_s "(i64.trunc_f32_s (f32.reinterpret_i32 (i32.wrap_i64 (local.get 0))))" $T64S +trap64 i64.trunc_f32_u "(i64.trunc_f32_u (f32.reinterpret_i32 (i32.wrap_i64 (local.get 0))))" $T64S + echo "aarch64: $acc ops accepted, $n native checks. Declined frontier:$dec" if [ -z "$bad" ]; then echo "PASS: all accepted aarch64 ops match wasmtime"; exit 0 else echo "FAIL: aarch64 MISCOMPILE:$bad"; exit 1; fi diff --git a/scripts/templates/feature_matrix.md.tmpl b/scripts/templates/feature_matrix.md.tmpl index 0c8585ba..f6a99d34 100644 --- a/scripts/templates/feature_matrix.md.tmpl +++ b/scripts/templates/feature_matrix.md.tmpl @@ -33,7 +33,7 @@ soundness feature, not an absence. | ARM Thumb-2 (primary) | `synth-backend` | `cortex-m3`, `cortex-m4`, `cortex-m4f`, `cortex-m7`, `cortex-m7dp` (+ `cortex-m55` experimental MVE) | i32 + i64 (register pairs) complete; scalar f32/f64 via VFP on FPU targets; control flow (block/loop/if/br/br_table); memory incl. sub-word; direct calls; `call_indirect` in both relocatable and self-contained `--cortex-m` images (v0.47, #275) | | ARM A32 | `synth-backend` | `cortex-r5` | i32 + i64 integer family (221-variant no-wildcard tripwire, #615); self-contained `call_indirect` declines loudly (no flash-table builder) | | RISC-V RV32IMAC | `synth-backend-riscv` | `rv32imac`, `rv32imc`, `rv32im`, `rv32i`, `rv32gc`, `esp32c3` | i32 + i64 integer ops, control flow, calls incl. `call_indirect`, memory loads/stores; relocatable ELF; import/external calls emit `R_RISCV_CALL_PLT` relocations (`.rela.text`, undefined import symbols — #871) with exact-arity marshalling from the module signature tables; >8-arg / i64-arg / multi-value calls decline loudly; floats decline loudly | -| AArch64 (A64, host-native) | `synth-backend-aarch64` | `cortex-a53` (host-linkable ET_REL, `-b aarch64`) | {{aarch64_selector_ops}} distinct WASM ops handled by the selector: i32 + i64 integer core incl. `div_s/div_u/rem_s/rem_u` (with the ÷0 + INT_MIN/−1 WASM trap guards), `popcnt`, `select` (branchless `CSEL`/`FCSEL`, all four value types), `drop`/`nop`, `i32.wrap_i64`, `i64.extend_i32_{s,u}`, and the five `extend8/16/32_s` sign extensions (#851 v0.53); scalar f32/f64 incl. domain-guarded trapping float→int truncations, IEEE 754-2019 min/max, copysign, and f64↔i64 reinterpret (#538 milestone 4, #851); full control flow — `block`/`loop`/`if`/`else`/`br`/`br_if`/`return` (#538 cf + #851); non-param locals — zero-init stack slots with copy-semantics get/set/tee (#856); linear-memory `i32`/`i64` load/store incl. all sub-word sign/zero forms, **BOUNDS-CHECKED by default** — an out-of-bounds access traps (`brk`) exactly where wasmtime traps, and `--safety-bounds` selects the strategy (`software` = the enforcing default, `none` = explicit opt-out; `mask`/`mpu` hard-error rather than silently degrading) (#851, #865 — execution-verified against the OOB table); fixed-memory `memory.size`/`memory.grow` (declared-min page count; `grow(0)` ≡ size, `grow(n>0)` → −1 — growth failure is spec-permitted and keeps the static bounds limit sound); direct calls (AAPCS64 + `R_AARCH64_CALL26`, #851). **PRECONDITION, not emitted code:** memory-using functions expect `x28` = linear-memory base on entry — synth emits NO startup or prologue that establishes it (no linker script, no data section); the embedder/harness must set it, and a module carrying **active data segments is REFUSED loudly** (v0.53 — previously the segments were silently dropped and initialized regions read zeros). Declines (loud, mechanically enumerated by the VCR-SEL-005 third-backend oracle): `call_indirect`, import calls, value-carrying blocks/loops, `br_table`, writing a PARAM local, globals, `memory.copy`/`fill`, float `ceil`/`floor`/`trunc`/`nearest`, f32/f64 load/store, i64→float converts, trapping i64-target truncations, `>8` args, float-result callees | +| AArch64 (A64, host-native) | `synth-backend-aarch64` | `cortex-a53` (host-linkable ET_REL, `-b aarch64`) | {{aarch64_selector_ops}} distinct WASM ops handled by the selector: i32 + i64 integer core incl. `div_s/div_u/rem_s/rem_u` (with the ÷0 + INT_MIN/−1 WASM trap guards), `popcnt`, `select` (branchless `CSEL`/`FCSEL`, all four value types), `drop`/`nop`, `i32.wrap_i64`, `i64.extend_i32_{s,u}`, and the five `extend8/16/32_s` sign extensions (#851 v0.53); the COMPLETE scalar f32/f64 surface — arithmetic, NaN-ordering compares, IEEE 754-2019 min/max, copysign, sqrt, promote/demote, reinterprets, `ceil`/`floor`/`trunc`/`nearest` (one mode-pinned `FRINT{P,M,Z,N}` each; `nearest` is FRINTN = ties-to-EVEN, execution-checked on a halfway table), i32- AND i64-source converts (`SCVTF`/`UCVTF`), the saturating `trunc_sat` family, and ALL EIGHT domain-guarded trapping float→int truncations — i32- and i64-target — where A64 `FCVTZ{S,U}` would SATURATE but WASM §4.3.3 TRAPS (#538 milestone 4, #851, v0.54 — verified against a ±2^31/±2^63/2^32/2^64 boundary table, both sides of every bound); full control flow — `block`/`loop`/`if`/`else`/`br`/`br_if`/`return` (#538 cf + #851); non-param locals — zero-init stack slots with copy-semantics get/set/tee (#856); linear-memory `i32`/`i64`/`f32`/`f64` load/store incl. all sub-word sign/zero forms and the SIMD&FP `LDR`/`STR` `s`/`d` forms (v0.54), **BOUNDS-CHECKED by default** — an out-of-bounds access traps (`brk`) exactly where wasmtime traps, and `--safety-bounds` selects the strategy (`software` = the enforcing default, `none` = explicit opt-out; `mask`/`mpu` hard-error rather than silently degrading) (#851, #865 — execution-verified against the OOB table); fixed-memory `memory.size`/`memory.grow` (declared-min page count; `grow(0)` ≡ size, `grow(n>0)` → −1 — growth failure is spec-permitted and keeps the static bounds limit sound); direct calls (AAPCS64 + `R_AARCH64_CALL26`, #851). **PRECONDITION, not emitted code:** memory-using functions expect `x28` = linear-memory base on entry — synth emits NO startup or prologue that establishes it (no linker script, no data section); the embedder/harness must set it, and a module carrying **active data segments is REFUSED loudly** (v0.53 — previously the segments were silently dropped and initialized regions read zeros). Declines (loud, mechanically enumerated by the VCR-SEL-005 third-backend oracle): `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 — the SCALAR FLOAT surface no longer appears here (v0.54 closed its last four classes) | --- From 8b0b7373b84f2684c29918e289b7da565023a7e4 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 30 Jul 2026 15:14:49 +0200 Subject: [PATCH 7/8] chore: regenerate status artifacts for the aarch64 float completion (#851) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Mechanical `python3 scripts/claim_check.py claims.yaml --emit-status` output — the claim-check gate goes red otherwise (the generated files must match their template + re-derived counts at every commit). aarch64_selector_ops: 161 -> 181 (the 20 newly-lowered WasmOp variants: 8 rounding + 4 i64->float converts + 4 trapping i64 truncations + 4 FP load/store) COORDINATOR (#805): re-run `--emit-status` ONCE after fan-in — this file will conflict with any other lane that also moves a counted claim. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- artifacts/status.json | 2 +- docs/status/FEATURE_MATRIX.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/artifacts/status.json b/artifacts/status.json index 5ec9905a..6f1b9115 100644 --- a/artifacts/status.json +++ b/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": [ diff --git a/docs/status/FEATURE_MATRIX.md b/docs/status/FEATURE_MATRIX.md index 1c00bf09..79247835 100644 --- a/docs/status/FEATURE_MATRIX.md +++ b/docs/status/FEATURE_MATRIX.md @@ -33,7 +33,7 @@ soundness feature, not an absence. | ARM Thumb-2 (primary) | `synth-backend` | `cortex-m3`, `cortex-m4`, `cortex-m4f`, `cortex-m7`, `cortex-m7dp` (+ `cortex-m55` experimental MVE) | i32 + i64 (register pairs) complete; scalar f32/f64 via VFP on FPU targets; control flow (block/loop/if/br/br_table); memory incl. sub-word; direct calls; `call_indirect` in both relocatable and self-contained `--cortex-m` images (v0.47, #275) | | ARM A32 | `synth-backend` | `cortex-r5` | i32 + i64 integer family (221-variant no-wildcard tripwire, #615); self-contained `call_indirect` declines loudly (no flash-table builder) | | RISC-V RV32IMAC | `synth-backend-riscv` | `rv32imac`, `rv32imc`, `rv32im`, `rv32i`, `rv32gc`, `esp32c3` | i32 + i64 integer ops, control flow, calls incl. `call_indirect`, memory loads/stores; relocatable ELF; import/external calls emit `R_RISCV_CALL_PLT` relocations (`.rela.text`, undefined import symbols — #871) with exact-arity marshalling from the module signature tables; >8-arg / i64-arg / multi-value calls decline loudly; floats decline loudly | -| AArch64 (A64, host-native) | `synth-backend-aarch64` | `cortex-a53` (host-linkable ET_REL, `-b aarch64`) | 161 distinct WASM ops handled by the selector: i32 + i64 integer core incl. `div_s/div_u/rem_s/rem_u` (with the ÷0 + INT_MIN/−1 WASM trap guards), `popcnt`, `select` (branchless `CSEL`/`FCSEL`, all four value types), `drop`/`nop`, `i32.wrap_i64`, `i64.extend_i32_{s,u}`, and the five `extend8/16/32_s` sign extensions (#851 v0.53); scalar f32/f64 incl. domain-guarded trapping float→int truncations, IEEE 754-2019 min/max, copysign, and f64↔i64 reinterpret (#538 milestone 4, #851); full control flow — `block`/`loop`/`if`/`else`/`br`/`br_if`/`return` (#538 cf + #851); non-param locals — zero-init stack slots with copy-semantics get/set/tee (#856); linear-memory `i32`/`i64` load/store incl. all sub-word sign/zero forms, **BOUNDS-CHECKED by default** — an out-of-bounds access traps (`brk`) exactly where wasmtime traps, and `--safety-bounds` selects the strategy (`software` = the enforcing default, `none` = explicit opt-out; `mask`/`mpu` hard-error rather than silently degrading) (#851, #865 — execution-verified against the OOB table); fixed-memory `memory.size`/`memory.grow` (declared-min page count; `grow(0)` ≡ size, `grow(n>0)` → −1 — growth failure is spec-permitted and keeps the static bounds limit sound); direct calls (AAPCS64 + `R_AARCH64_CALL26`, #851). **PRECONDITION, not emitted code:** memory-using functions expect `x28` = linear-memory base on entry — synth emits NO startup or prologue that establishes it (no linker script, no data section); the embedder/harness must set it, and a module carrying **active data segments is REFUSED loudly** (v0.53 — previously the segments were silently dropped and initialized regions read zeros). Declines (loud, mechanically enumerated by the VCR-SEL-005 third-backend oracle): `call_indirect`, import calls, value-carrying blocks/loops, `br_table`, writing a PARAM local, globals, `memory.copy`/`fill`, float `ceil`/`floor`/`trunc`/`nearest`, f32/f64 load/store, i64→float converts, trapping i64-target truncations, `>8` args, float-result callees | +| AArch64 (A64, host-native) | `synth-backend-aarch64` | `cortex-a53` (host-linkable ET_REL, `-b aarch64`) | 181 distinct WASM ops handled by the selector: i32 + i64 integer core incl. `div_s/div_u/rem_s/rem_u` (with the ÷0 + INT_MIN/−1 WASM trap guards), `popcnt`, `select` (branchless `CSEL`/`FCSEL`, all four value types), `drop`/`nop`, `i32.wrap_i64`, `i64.extend_i32_{s,u}`, and the five `extend8/16/32_s` sign extensions (#851 v0.53); the COMPLETE scalar f32/f64 surface — arithmetic, NaN-ordering compares, IEEE 754-2019 min/max, copysign, sqrt, promote/demote, reinterprets, `ceil`/`floor`/`trunc`/`nearest` (one mode-pinned `FRINT{P,M,Z,N}` each; `nearest` is FRINTN = ties-to-EVEN, execution-checked on a halfway table), i32- AND i64-source converts (`SCVTF`/`UCVTF`), the saturating `trunc_sat` family, and ALL EIGHT domain-guarded trapping float→int truncations — i32- and i64-target — where A64 `FCVTZ{S,U}` would SATURATE but WASM §4.3.3 TRAPS (#538 milestone 4, #851, v0.54 — verified against a ±2^31/±2^63/2^32/2^64 boundary table, both sides of every bound); full control flow — `block`/`loop`/`if`/`else`/`br`/`br_if`/`return` (#538 cf + #851); non-param locals — zero-init stack slots with copy-semantics get/set/tee (#856); linear-memory `i32`/`i64`/`f32`/`f64` load/store incl. all sub-word sign/zero forms and the SIMD&FP `LDR`/`STR` `s`/`d` forms (v0.54), **BOUNDS-CHECKED by default** — an out-of-bounds access traps (`brk`) exactly where wasmtime traps, and `--safety-bounds` selects the strategy (`software` = the enforcing default, `none` = explicit opt-out; `mask`/`mpu` hard-error rather than silently degrading) (#851, #865 — execution-verified against the OOB table); fixed-memory `memory.size`/`memory.grow` (declared-min page count; `grow(0)` ≡ size, `grow(n>0)` → −1 — growth failure is spec-permitted and keeps the static bounds limit sound); direct calls (AAPCS64 + `R_AARCH64_CALL26`, #851). **PRECONDITION, not emitted code:** memory-using functions expect `x28` = linear-memory base on entry — synth emits NO startup or prologue that establishes it (no linker script, no data section); the embedder/harness must set it, and a module carrying **active data segments is REFUSED loudly** (v0.53 — previously the segments were silently dropped and initialized regions read zeros). Declines (loud, mechanically enumerated by the VCR-SEL-005 third-backend oracle): `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 — the SCALAR FLOAT surface no longer appears here (v0.54 closed its last four classes) | --- From 52a8d872ea91bbfe18ee1f961363ba596780a06e Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 30 Jul 2026 15:36:16 +0200 Subject: [PATCH 8/8] fix(ci): the float-completion gate could pass while its oracle FAILED (#890) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Coordinator correction from lane L1, and it was a REAL defect in the step I shipped two commits ago — not a hypothetical. `set -o pipefail` ALONE does not fail the step. Without `-e`, the step's exit status is that of the LAST command, so the failing pipeline's non-zero was discarded and the trailing `[ ... ] || exit 1` count checks (which pass on a FAILING run, because a failing oracle still prints its full case counts) decided the verdict. Reproduced locally against a stub that prints `RESULT: FAIL (1)` and exits 1: old shape (bare pipefail) -> exit 0 GREEN while the oracle FAILED new shape (set -euo pipefail) -> exit 1 correctly RED Fixed by making the shell flags explicit (`set -euo pipefail`, not relying on the runner's defaults) AND by deriving the verdict from the script's OWN summary line — `grep -q '^RESULT: PASS'` — instead of from exit 0 alone. The non-collapsed count assertions stay as the anti-vacuity floor and are now bare tests, so `-e` aborts on them too. Re-verified green against the real oracle (662 checks, 142 trap cases). Also adds the `# ci-status: wired` header L1's new oracle-wiring gate requires on `scripts/repro/*.py` (docstring left intact — it is still the module docstring with a comment above it). Unrelated polish caught while verifying the ARM32 decline on all three target paths (m4f, m4f --relocatable, m7dp --relocatable — all loud, RV32 too): a line-continuation in the new diagnostic split "WASM-correct" as "WASM- correct" in the user-facing message. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .github/workflows/ci.yml | 20 ++++++++++++++----- .../src/instruction_selector.rs | 6 +++--- ...rch64_float_completion_851_differential.py | 1 + 3 files changed, 19 insertions(+), 8 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 27b4ae49..ad839f99 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -535,18 +535,28 @@ jobs: # halfway table, which is what makes the "FRINTN is ties-to-EVEN" # claim real rather than assumed. # - # `pipefail` + a grep asserting a NON-ZERO, non-collapsed check count: - # an oracle that silently stops exercising anything must go red (#890). + # 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 -o pipefail + 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:-0}" -ge 300 ] || { echo "oracle ran too few checks ($n)"; exit 1; } - [ "${t:-0}" -ge 40 ] || { echo "oracle ran too few TRAP cases ($t)"; exit 1; } + [ "$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 diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 9685e9b5..d60ad850 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -7555,9 +7555,9 @@ impl InstructionSelector { op @ (F32Ceil | F32Floor | F32Trunc | F32Nearest) if self.fpu.is_some() => { return Err(synth_core::Error::synthesis(format!( "{op:?} not supported on ARM32: the available lowering is a \ - saturating VCVT round-trip through i32, which is not WASM- \ - correct for |x| >= 2^31, ±inf or NaN — declined until the \ - VRINT.F32 lowering lands" + saturating VCVT round-trip through i32, which is not \ + WASM-correct for |x| >= 2^31, ±inf or NaN — declined until \ + the VRINT.F32 lowering lands" ))); } // F32 min/max — LOUD-DECLINED on ARM32 (#538 m4): the legacy diff --git a/scripts/repro/aarch64_float_completion_851_differential.py b/scripts/repro/aarch64_float_completion_851_differential.py index 42ab916b..be7308df 100644 --- a/scripts/repro/aarch64_float_completion_851_differential.py +++ b/scripts/repro/aarch64_float_completion_851_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """v0.54 L2 (#851) — the aarch64 float-completion EXECUTION differential. Closes the four classes the VCR-SEL-005 third-backend op-parity oracle listed as