finding: synth#869 — whole 64-bit int<->float family unlowered (ARMv7E-M VFP root cause); relay's source dodge verified exhausted

[avrabe]

relay chased the GI-FPU-001 dodge jess proposed and reported a clean negative result — exactly the right call. Call site confirmed as Timestamp::as_secs_f32() (seconds: u64 + fraction: u32), and the crate correlation closes the diagnosis from both ends: relay-rate/relay-ekf/relay-pos call it = precisely the three GI-FPU-001 stages; relay-att only defines Timestamp and is GI-FPU-002-blocked instead.

Four narrowings tried (integer-domain differencing, u64::min cap, mask-truncate, small-cap early-narrow), disassembled after each: LLVM clamps in the integer domain correctly but won't narrow to i32 before the convert — on wasm both widths cost the same. The op persisted even after deleting the helper outright. No producer-side form exists.

jess probed synth directly — one coherent gap

Minimal WAT over the whole conversion family on synth 0.51.0:

lowers	skipped
f32.convert_i32_u/_s, i32.trunc_f32_s, i32.wrap_i64 + f32.convert_i32_u	f32.convert_i64_u/_s, f64.convert_i64_u/_s, i64.trunc_f32_u/_s

All six 64-bit integer↔float ops are unlowered; every 32-bit form works. So the canonical lowering shape exists in wasm but is unreachable from Rust.

Root cause — an implementation task, not a wiring bug

ARMv7E-M VFP has no 64-bit-integer↔float instruction at all. VCVT on FPv4-SP/FPv5-D16 encodes only S32/U32 ↔ F32/F64; the 64-bit integer forms arrive only with AArch64 SCVTF/UCVTF. Every Cortex-M toolchain routes these through AEABI builtins (__aeabi_ul2f, __aeabi_l2f, __aeabi_ul2d, __aeabi_l2d, __aeabi_f2ulz, __aeabi_f2lz) — and synth already has a --builtins linking path, so the fix needs no new machinery.

Filed synth#869 with the minimal repro, AEABI mapping, per-stage impact (entry symbols named) and relay's exhausted-workaround credited so nobody re-treads it. Both prior anchors (#369, #782) are closed — this family had no open upstream issue.

The gate is now exactly two synth items, neither needing anything from relay

1. synth#869 — i64↔float family → unblocks rate / position / ekf
2. GI-FPU-002 — VFP-regfile exhaustion (no VFP spilling) → unblocks attitude / iekf
3. mixer is already through (0 skips) → next jess rung: lower mixer + run it in the RT1176 Renode model against a SIL differential — the first real relay flight component executing on the M7, exercising the whole consumption path with the gate still open.

rivet validate → PASS.

🤖 Generated with Claude Code