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

[avrabe]

Closes #869 (and the #756 i64.trunc_f64 selector-lowering gap).

What now lowers (cortex-m7dp, both --relocatable and self-contained)

op	lowering
f64.convert_i64_{s,u}	exact two-word build: VCVT each half, ×2^32 (exact), one VADD.F64 = the single correct RNE rounding
f32.convert_i64_{s,u}	same build + Fast2Sum exact residual + branch-free round-to-odd fixup + one VCVT.F32.F64 demote (double-rounding-exact, Boldo–Melquiond)
i64.trunc_f32_{s,u}	TRAP-GUARDED: promote (exact) → #709-class i64 domain guard → #782 word-decompose (provably never saturates in-domain)
i64.trunc_f64_{s,u}	#709-class i64 domain guard → #782 word-decompose

Loud-declined by name (no silent holes): every family member on single-precision targets (m4f/m7 — the lowerings run on f64 machinery, undefined encodings on FPv4-SP; the pre-existing i64.trunc_sat_f32 promote path is now caught by the same earlier gate) and on no-FPU targets; select_default (register-blind fallback, not a shipping path) keeps typed declines. aarch64/RV32 unchanged (wildcard declines; parity universe updated).

Inline expansion, not __aeabi builtins — why

gale's issue offered both routes. Chosen: self-contained expansion — (1) no runtime link dependency (--relocatable consumers like meld would inherit an __aeabi_* obligation kiln doesn't ship today), (2) no hard/soft-float ABI variance to verify per target, (3) unicorn-executes directly so the trap rows are executed in CI rather than trusted, (4) it is the #782 trunc_sat precedent — the trapping trunc is literally guard + the shipped decompose. The AEABI builtins also do NOT trap, so they'd still need the exact same guards; the call would buy nothing but a dependency.

Soundness (the load-bearing part)

• WASM §4.3.3 requires the non-sat truncs to trap on NaN/out-of-range; the decompose (like __aeabi_f2lz) saturates — the thumb-2: i64.div_s(INT64_MIN, -1) silently returns INT64_MIN instead of trapping (overflow guard missing on i64 path; i32 path has it) #633/rv32: i32.rem_s(INT_MIN,-1) spuriously traps — div_s overflow ebreak guard wrongly copied into rem_s (irem_s must return 0) #666/thumb-2 f32: i32.trunc_f32_s/u silently saturate instead of trapping on NaN/Inf/out-of-range (bare VCVT, no guard) — WASM Core §4.3.3 soundness bug #709/synth compiles WASM unreachable to a no-op on both thumb-2 and rv32 — falls through instead of trapping (WASM 4.4.5) #665/thumb-2: call_indirect emits no bounds-check and no type-check — OOB/wrong-type index does an uncontrolled indirect branch instead of trapping (WASM 4.4.8) #642 class. The guard bounds are exact on f32/f64 (-2^63 ≤ x < 2^63 signed — no representable value sits in (-2^63-1, -2^63); -1 < x < 2^64 unsigned), ordered compares so NaN falls to the first UDF.
• trunc_sat twins verified still guard-free (no trap leak; unit-pinned).
• The naive promote-then-demote for f32.convert_i64 double-rounds (killer row 0x8000_0080_0000_0001 in the differential); the round-to-odd fixup makes 64→53→24 ≡ 64→24 RNE.

Found & contained: a range-realloc soundness hazard (#872)

The first cut of the fixup used the I64Add pseudo-op; the default-on SYNTH_RANGE_REALLOC pass treats reg_effect=None ops as segment barriers whose register READS are invisible, reused the live-in pair for intermediates, and its own segment validator accepted the wrong rewrite. Caught by this PR's differential at land time; contained here by emitting modeled Adds/Adc (uses visible, exit ranges pinned — unit-pinned so it can't regress to I64Add); the pass-level hazard is filed with full evidence as #872.

Gates (all run locally, green)

1. Red-first repro scripts/repro/i64_float_conv_869.wat — RED on v0.51 (six exports absent from nm), GREEN now (all 12 → T), gale's exact flags.
2. Execution differential scripts/repro/i64_float_conv_869_differential.py (CI-wired into the ARM oracle job): 96,296 checks vs wasmtime under unicorn — full boundary tables with trap rows executed on both sides (NaN, ±inf, 2^63, −2^63, 2^64, largest-below-bound values, (-1,0) no-trap window), double-rounding killers, RNE tie rows at 24- and 53-bit granularity, ≥12k fixed-seed fuzz per direction; m4f decline-honesty; falcon-flags symbol presence.
3. Frozen anchors: frozen_codegen_bytes 10/10 byte-identical (byte-changing only for modules using these ops).
4. cargo test --workspace green, fmt clean, clippy -D clean (final run in CI).
5. Unit contracts (i64_float_conv_869.rs): 8/8 lower on m7dp, truncs exactly 2 UDFs, converts 0, sat twins 0, Adds/Adc pinned, m4f/m3 named declines. Existing trunc_sat_782 suite untouched-green.

falcon evidence: the three blocked stages (rate#tick, position#tick, ekf#estimate) are blocked at their entry points by F32ConvertI64U per the issue; gale's standing jess gate covers the real fused components on this branch.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[avrabe]

Final local gate, all green at 471a33f:

• cargo test --workspace: 129 suites, 0 failures (includes the decoder-test update — its 'still-dropped' probe was i64.trunc_f64_s, which this PR legitimately un-drops; the flag-never-drop honesty contract for the remaining undecoded float surface stays pinned by the float-global test)
• cargo clippy --workspace --all-targets -- -D warnings: clean
• cargo fmt --check: clean
• frozen anchors: 10/10 byte-identical
• i64_float_conv_869_differential.py: 96,296 checks PASS (default env, range-realloc ON)
• regression: trunc_sat_782 (32,686 checks), f64_369 (339), f32_mem_trunc_708_709 (48), float_select_return_782 — all PASS with this branch's binary
• claim_check.py: 25/25 hold

Allocator hazard found during this work is filed with executable evidence as #872.

[codecov]

Codecov Report

❌ Patch coverage is 94.06780% with 28 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-synthesis/src/instruction_selector.rs	96.69%	15 Missing ⚠️
crates/synth-core/src/wasm_decoder.rs	36.36%	7 Missing ⚠️
crates/synth-verify/src/wasm_semantics.rs	0.00%	4 Missing ⚠️
crates/synth-verify/src/trap.rs	0.00%	2 Missing ⚠️

📢 Thoughts on this report? Let us know!

[avrabe]

Rebased onto origin/main (merged df1a8ad, the #867/#870 ISA-model-adequacy lane) and re-verified from scratch — PR is MERGEABLE.

What conflicted: only CHANGELOG.md (both lanes wrote [Unreleased]). Resolved keeping both sides: my #869 bullet plus main's two #867 bullets under one ### Added, then my ### Fixed bullet. ci.yml and claims.yaml auto-merged with both lanes' content intact. No generated files touched — artifacts/status.json, docs/status/FEATURE_MATRIX.md, artifacts/model-coverage.json, coq/STATUS.md are main's versions verbatim (zero drift in my diff; coordinator regenerates at assembly). No code conflicts: main's commit was docs/ledger/CI-only, so liveness.rs and the RISC-V backend had zero interaction.

Re-verified post-merge (fresh binary, worktree-local target on the internal SSD):

• cargo build -p synth-cli — clean
• i64_float_conv_869_differential.py — 96,296 checks PASS (full 12k/direction fuzz, trap rows executed both sides)
• frozen_codegen_bytes — 10/10 byte-identical
• cargo test --workspace — 129 suites, 0 failures
• cargo clippy --workspace --all-targets -- -D warnings — clean; cargo fmt --check — clean
• claim_check.py — 26/26 (incl. main's new SYNTH-ISA-MODEL-BASIS)
• model_coverage_audit.py --check — main's new freshness gate passes unchanged
• regression oracles re-run: trunc_sat #782a, f64 arm backend uses soft-float for all f32/f64 — hardware FPU never used (cortex-m4f/m7/m7dp identical); blocks REQ-PIX-001 hard-float #369 (339/339), f32 f32.load + i32.reinterpret_f32 not lowered on the thumb-2 FPU path — the #369 residual that actually blocks falcon (20 of its 24 float skips) #708/thumb-2 f32: i32.trunc_f32_s/u silently saturate instead of trapping on NaN/Inf/out-of-range (bare VCVT, no guard) — WASM Core §4.3.3 soundness bug #709 (48/48), float-select #782b — all GREEN
• spot-check on post-merge disassembly: f32_to_i64s = promote → 2^63 bound → ordered vcmp.f64/vmrs/it mi → cmp/bne skip → 2 UDF trap sites, as designed

Remote CI on the merged head: 27 SUCCESS, 0 FAILURE (remainder queued on runner availability).