Skip to content

feat(#782): sound ARM32 i64 trunc_sat via branch-free FP decompose — falcon skip 4→0#812

Merged
avrabe merged 3 commits into
mainfrom
feat/49-782-finale
Jul 17, 2026
Merged

feat(#782): sound ARM32 i64 trunc_sat via branch-free FP decompose — falcon skip 4→0#812
avrabe merged 3 commits into
mainfrom
feat/49-782-finale

Conversation

@avrabe

@avrabe avrabe commented Jul 17, 2026

Copy link
Copy Markdown
Contributor

#782 finale — drive falcon fused-core trunc_sat skips toward zero

Closes the ARM32 half of the #782 trunc_sat skip class: the four
i64.trunc_sat_f32/f64_{s,u} forms — LOUD-declined through v0.48 — now lower
soundly and trap-free on 32-bit ARM (double-FPU / cortex-m7dp). Refs #782, #242.

Skip delta (the headline)

Under the falcon repro flags (-t cortex-m7dp --relocatable) on the #782
skip-class proxy module (scripts/repro/trunc_sat_782.wat):

v0.48 (main) v0.49 (this PR)
i32-target trunc_sat (4 forms) lowered lowered
i64-target trunc_sat (4 forms) 4/4 LOUD-declined 0 declined — all 4 lowered
falcon-flags skip count 4 0

The falcon fused-core's own 26→N delta is UNMEASURABLE LOCALLY — the real
falcon-flight-v1.123 module is a relay/jess-owned asset not in the repo (only
the 29-line falcon_axis.wat, which carries no trunc_sat), and relay was not
addressable via SendMessage this session. So this reports the capability
delta on the #782 skip class the fused core flagged
(4→0), not a fabricated
fused-core count. If the asset arrives, the measurement is a compile → grep "skipping" → categorize away. Blocker surfaced, not papered over.

How (sound, self-contained, trap-free)

lower_i64_trunc_sat_from_f64 (shipping select_with_stack path). WASM §4.3.2
trunc_sat is TOTAL (NaN→0, out-of-range saturates, never traps). No __aeabi
link dependency, no i64 VCVT (ARMv7 VFP lacks it) — an exact FP word-decompose:

  • _u: decompose x directly via two saturating VCVT.U32.F64 over an
    exact 2^-32/2^32 word split (negatives→0, NaN→0, ≥2^64→u64 MAX).
  • _s: VABS to |x|, same unsigned decompose, then a branch-free
    conditional two's-complement negate (v XOR signmask) − signmask (signmask ∈
    {0,−1} from bit 63 of the original x, so no zero/neg register pair) and a
    saturation blend to INT64_MIN/MAX under ASR(hi,31). The −2^63 edge is
    where clamp and negate coincide — no fencepost.

f32-source forms promote to f64 first (exact). On a single-precision target the
f64 promote is genuinely unavailable, so those i64 forms still honest-decline
(ISA-validated on VCVT.F64.F32).

Verification (the real gate — not a self-test)

scripts/repro/trunc_sat_782_differential.py vs wasmtime, bit-exact:

  • Boundary table (NaN, ±inf, exact 2^63/2^64 bounds, ±2^63, ±0.5, in-range).
  • Heavy fuzz — 192,000 random bit-pattern checks (≥10k per source type,
    subnormals / huge / NaN-payloads / every sign, seeded) — the real gate for a
    multi-instruction decompose that a boundary table cannot characterise.
  • Executed on ARM32 m7dp (all 8 forms), aarch64 unicorn, AND native arm64.
    Zero traps anywhere.
  • Fixed a latent vacuity: arm32_run now reads the AAPCS i64 return as
    R0 | (R1<<32) (was R0 only — every hi-word bug was invisible).

Decline-honesty (the v0.46 lesson — moved, never deleted)

  • Repro falcon/arm32 assertions flipped from "i64 SKIPPED + register-pair
    decline named" to "all 8 COMPILE + execute bit-exact" — a regression that
    drops any i64 form fails the gate.
  • New repro m4f assertion: all 4 i64 forms must be ABSENT (loud-declined) on
    single-precision — the only gate on the f32-source ISA-validation decline.
  • select_default (register-blind fallback) still declines i64 trunc_sat as an
    honest safety net (both CLI paths route through select_with_stack); commented.

Gates

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

avrabe and others added 3 commits July 17, 2026 13:56
Lower i64.trunc_sat_f32/f64_{s,u} on 32-bit ARM (select_with_stack path)
as a trap-free, self-contained (no __aeabi link dep) register-pair
conversion — the four forms previously LOUD-declined.

Algorithm (lower_i64_trunc_sat_from_f64):
  _u: decompose x directly via two saturating VCVT.U32.F64 over an exact
      2^-32 / 2^32 word split (negatives->0, NaN->0, >=2^64->u64 MAX).
  _s: VABS to |x|, same unsigned decompose, then a BRANCH-FREE
      conditional negate (v XOR signmask) - signmask and a saturation
      blend to INT64_MIN/MAX under ASR(hi,31). signmask from bit63 of the
      original x. -2^63 edge: clamp and negate coincide.

Register-pressure: the negate uses the two's-complement identity with
signmask in {0,-1} so it needs NO zero/neg pair (the exhaustion that hit
the signed forms on the first cut); saturation words are blended one at a
time. All 8 forms now compile under -t cortex-m7dp --relocatable (falcon
flags), 0 skips.

Boundary+fuzz differential vs wasmtime follows.

Refs #782 #242

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
Differential (scripts/repro/trunc_sat_782_differential.py):
- arm32_run now reads the AAPCS i64 return as R0|(R1<<32) — reading only
  R0 would make every hi-word bug (NaN->0 upper word, saturation MIN/MAX,
  sign) invisible.
- ALL EIGHT forms now execute on ARM32 cortex-m7dp (was: i32 quartet only).
- Honesty-gate FLIP (moved, not deleted, per the v0.46 lesson): the falcon-
  flags + arm32 sections asserted i64 SKIPPED + 'register-pair' decline
  named; they now assert all eight COMPILE and execute bit-exactly. A
  regression that drops any i64 form fails the gate.
- Added run_fuzz: >=10k random bit-patterns per source type (f32+f64,
  subnormals/huge/NaN payloads/every sign, seeded) vs wasmtime — the real
  gate for a multi-instruction decompose that a ~40-point boundary table
  cannot characterise. Full run: 192,000 fuzz checks bit-exact, 0 traps,
  across ARM32 m7dp (all 8) + aarch64 unicorn + native arm64.

Unit test (crates/synth-synthesis/tests/trunc_sat_782.rs):
- i64_trunc_sat_forms_loud_decline_on_arm32 -> _lower_trap_free_on_cortex_m7dp:
  pins COMPILE + no-Udf + VCVT.U32.F64 decompose + I64Sub-iff-signed.
- New i64_trunc_sat_f64_source_declines_on_single_precision keeps the
  double-FPU capability decline honest (f32 source promotes to f64).

Refs #782 #242

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…ctor asymmetry note

- Differential m4f section now asserts ALL FOUR i64_trunc_sat forms are
  ABSENT (loud-declined) on single-precision cortex-m4f — the ONLY gate on
  the f32-source i64 decline, which surfaces at ISA validation (VCVT.F64.F32),
  below the selector-level Rust unit test. Decline-honesty residual moved,
  never deleted (the v0.46 lesson).
- FEATURE_MATRIX: trunc_sat row corrected from 'Not decoded — loud-skip' to
  the accurate lowered status (i32 any-FPU, i64 double-FPU via FP decompose,
  aarch64 all eight), keeping the honest residuals visible. NOT '#782 closed'
  — the pressure-dependent f32 class stays open.
- select_default: commented the select_with_stack/select_default capability
  ASYMMETRY at both i64 trunc_sat decline arms — the shipping path lowers
  them; the register-blind fallback declines as an honest safety net that a
  normal compile never routes through.

Refs #782 #242

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
@temper-pulseengine

Copy link
Copy Markdown
Contributor

Automated review for PR #812

pulseengine/synth:feat/49-782-finale → pulseengine/synth:main

Verdict: 💬 Comment

Summary: The PR has been reviewed and approved by the team.

Findings: 0 mechanical (rivet) · 1 from local AI model.

Findings (1):

  1. docs/status/FEATURE_MATRIX.md:46
    | Non-trapping `trunc_sat` (0xFC prefix) | D | Not decoded — functions using it loud-skip; tracked in #782 |
    
    The non-trapping trunc_sat feature is not yet fully implemented.

Generated by a local AI model and post-validated against a strict JSON contract. Each finding includes the verbatim line being criticised — verify by reading the file at the cited location.

Reviewed at d35ca59

@avrabe
avrabe merged commit 6c234f0 into main Jul 17, 2026
4 checks passed
@avrabe
avrabe deleted the feat/49-782-finale branch July 17, 2026 13:40
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant