RQ-60-VFPPRESSURE increment 1: AEABI-routed i64-f32 conversions on single-precision FPU targets - Refs #1069, Refs #869

[avrabe]

RQ-60-VFPPRESSURE increment 1 — the conversion routing only (the S-register pool extension is increment 2, a separate lane). Refs #1069, refs #869.

What this does

A function whose WASM signature contains no f64 anywhere was refused on cortex-m4f/m7 for "needing f64", because the #869 inline lowering of the i64↔float conversions runs on double-precision machinery. That pinned every conversion-carrying function to cortex-m7dp — the reach failure #1069 measured on the falcon cascade.

This routes exactly the six i64/f32-typed family members through the AEABI runtime helpers — the route #869's acceptance comment specified: base-AAPCS core-register calls, zero VFP pressure:

op	route	fence
f32.convert_i64_s / _u	bl __aeabi_l2f / __aeabi_ul2f	none needed (total)
i64.trunc_f32_s / _u	f32 domain guard (2 UDF) + bl __aeabi_f2lz / __aeabi_f2ulz	exact-f32 bounds trap NaN/out-of-range before the call; unsigned (-1,0)→+0 clamp so the C-style helper never sees undefined input
i64.trunc_sat_f32_s / _u	inline NaN/saturation select + bl	only in-range values reach the helper; no UDF (§4.3.2 never traps)

The fences matter because the AEABI helpers are more-total than WASM (the #633/#666/#709/#665/#642 class) — the exact soundness constraint from #869's acceptance comment, honored here on the builtin route.

Red first (literal output)

The eight-line repro on current main:

$ synth compile conv.wat -t cortex-m4f --relocatable --all-exports
warning: skipping function 'conv': ... GI-FPU-002 phase 2: scalar f64 requires a
double-precision FPU target (cortex-m7dp); 'thumbv7em-none-eabihf' has a
single-precision FPU (f32 only) — refusing to emit f64 (declining the function, #369)
Error: no functions compiled successfully (1 skipped) — nothing to emit   [exit 1]

The new test suite against pre-change sources (git stash of the impl, test kept):

test m4f_relocatable_routes_all_six_through_named_aeabi_builtins ... FAILED
test m4f_non_relocatable_still_declines_and_names_the_route ... FAILED
thread '...' panicked: F32ConvertI64S must lower on single-precision m4f --relocatable, got decline: ...
test result: FAILED. 3 passed; 2 failed

After (this branch):

$ synth compile conv.wat -t cortex-m4f --relocatable --all-exports
Compiled 1 functions ... 44 bytes; RELOCATION: R_ARM_THM_CALL __aeabi_ul2f
test result: ok. 5 passed; 0 failed   (tests/aeabi_i64_float_1069.rs)

Design decisions

1. Unconditional or pressure-heuristic? Neither, exactly: the builtin route applies only where inline is impossible — single-precision FPU targets, where the family previously had no lowering at all. On m7dp the #869 inline path is untouched. Rationale: predictable, and it moves zero shipping bytes (see below). What would make this the wrong call: if position#tick's m7dp D-exhaustion must be fixed on m7dp — that would need a pressure heuristic choosing builtin-over-inline there, and it belongs with the pressure work, stated as a named follow-up, not drifted into here. (Measured mitigation that exists today: on cortex-m7 — single-precision, the actual RT1176 core for an f32-only cascade — the route makes position#tick compile fully; see below.)

2. Which conversions. Measured on main: all 12 family members decline on m4f. Routed: the six whose WASM types are i64/f32 only (their f64 was an artifact of the lowering, not the program). Left declined by name: f64.convert_i64_s/u, i64.trunc_f64_s/u, i64.trunc_sat_f64_s/u — their WASM types carry f64, which a single-precision target genuinely cannot represent (any producer/consumer of that f64 value declines anyway). Routing them would be reach theater.

3. m7dp emitted bytes: none moved. The route is gated on FPUPrecision::Single, so m7dp never enters it. Verified three ways: pre/post cmp on the compiled minimal repro object (byte-identical), all frozen anchors green (cargo test --workspace, 151 suites, 0 failures — includes the frozen-fixture differentials), and the new test pins that no __aeabi_* call ever appears on m7dp. The pre-existing #869 (96,296 checks) and #782 (192,686 checks) oracles re-run green.

Gating on --relocatable: the bl __aeabi_* gets the same R_ARM_THM_CALL-against-undefined-symbol shape as every #197 external call, so the host linker resolves it. A self-contained image has no linker — non-relocatable single-precision keeps the loud decline, whose message now names the closable gap (compile with --relocatable to route ... through the AEABI builtins). This is a distinct mechanism from the existing --builtins <kiln-builtins.o> CLI flag (which links an object into --link mode); reusing that flag name for selection-time routing would conflate "what to link" with "how to lower", so the route keys on target capability + relocatable mode instead, and the flag keeps its one meaning.

The runtime-library dependency, stated

The emitted object now imports up to four symbols the embedder must provide at link time: __aeabi_l2f, __aeabi_ul2f, __aeabi_f2lz, __aeabi_f2ulz. Any of libgcc (-lgcc), compiler-rt builtins, or kiln's builtins archive satisfies them (jess links a kiln bridge already). Verified end-to-end: the m4f object links cleanly against real arm-none-eabi libgcc (link-exit=0), and the linked ELF — real libgcc code, no stubs — executes 88/88 boundary checks bit-exact vs wasmtime under unicorn, including the trap rows and the 0x8000008000000001 double-rounding killer.

Execution differential (CI-wired)

scripts/repro/aeabi_i64_float_1069_differential.py — 24,270 checks, 0 failures (19,139 stubbed builtin calls) vs wasmtime under unicorn on the m4f-compiled object:

• boundaries: 0, ±1, 2^24±, 2^53±, 2^63±, 2^64±, u64::MAX, i64::MIN/MAX, the arm backend: the entire 64-bit integer<->float conversion family is unlowered (6 ops) — blocks 3 of 5 falcon cascade stages at their entry points; source-side workaround verified exhausted #869 double-rounding killer 0x8000008000000001, largest-f32-below-each-bound, next-f32-below -2^63, -1.0, -0.0, (-1,0) residue, NaN payloads, ±inf;
• 4,000 fixed-seed fuzz patterns per direction (tie-prone-mantissa biased);
• every trap row executed on both sides (wasmtime trap ⇔ ARM UDF stop);
• the builtin stubs are spec-exact (integer-arithmetic RNE / truncation) and assert their C-defined input domain, so a guard hole reddens the run even when the numeric answer coincides;
• negative control executed: an off-by-one stub mutation reds the run with 4,088 failures.

Wired per #890/#910: ci-status: wired, emulations >= 24000, new oracle_run step; --min-emulation-floor 298754 → 322754 moved together on all four surfaces (ci.yml, claims.yaml pins, ORACLE_WIRING.md, feature-matrix template).

Real falcon components (the #1069 gate, run locally)

Pulled the published falcon 1.134.1 components from ghcr (the issue's public repro) and compiled with -t cortex-m4f --relocatable --all-exports --embedder-data-init --embedder-global-init:

component	main	this branch
rate	rate@0.7.0#tick skipped (GI-FPU-002 phase 2), exit non-zero	6/6 compile, #tick exported, sole external __aeabi_ul2f
position	position@0.7.0#tick skipped	8/8 compile, #tick exported, externals __aeabi_ul2f, __aeabi_f2lz, __aeabi_l2f
position on cortex-m7	#tick skipped (m7dp-only pinning → D0..D7 exhausted)	8/8 compile — the route removes the f64 pressure entirely on the single-precision M7

So of #1069's three named blockers, position#tick is now compilable on the M7 (as -t cortex-m7; on m7dp the inline path is deliberately unchanged and still D-exhausts). attitude#tick / ekf#estimate are phase-1 S-register exhaustion — increment 2's scope, untouched here.

Gates

• cargo fmt --all clean, cargo clippy --workspace --all-targets -- -D warnings clean, cargo test --workspace 151 suites / 0 failures.
• python3 scripts/claim_check.py claims.yaml exit 0 (51/51), incl. the ratchet: selector_lines_code 18288 → 18910 with a same-commit waiver (to: 18910) — growth, not substitution, by design: the m7dp path is byte-frozen so nothing could be deleted in exchange; this is new reach on targets where the family had no lowering at all. selector_lines_total 28929 → 29556. Wildcard pins unmoved (55/90).
• Oracles re-run locally: arm backend: the entire 64-bit integer<->float conversion family is unlowered (6 ops) — blocks 3 of 5 falcon cascade stages at their entry points; source-side workaround verified exhausted #869 (96,296 checks PASS), #369 marked closed, but the real falcon-flight-v1.123 fused core still skips 26/156 on --relocatable cortex-m7dp (incl. run-stabilization); trunc_sat unsupported + a pressure-dependent 'integer popped f32' class #782 trunc_sat (192,686 PASS), ARM: select on an i64-comparison condition with COMPUTED arms always returns the then-arm — reload clobbers the live else-arm register #973 ARM corpus sweep (152/164 compiled, 2,502 vectors, PASS — all 12 expected declines held).

Known residuals (named, not hidden)

• m7dp D-pressure from inline conversions (position#tick on m7dp): unchanged by design; fixing it there means builtin-vs-inline under pressure — a follow-up decision, not this increment.
• Self-contained (--cortex-m) single-precision still declines the family: no linker to satisfy __aeabi_*. Embedding a builtins blob in the image is a possible follow-up.
• vfp_op_demand for the routed ops still carries the inline path's conservative 4-D-pair figure; on the Single route it only over-spills under the GI-FPU-002 + RA tail is now the ONLY gate between the falcon cascade and the M7 — 5 entry-point symbols; phase-2 D-register pressure is new in v0.52 (inline-f64 #869 lowering) #881 retry rung (sound, never wrong bytes).
• WCET: a routed function's bl __aeabi_* is an external call → the existing call loud-decline, honest and unchanged.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[codecov]

Codecov Report

❌ Patch coverage is 94.22633% with 25 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-synthesis/src/instruction_selector.rs	93.98%	24 Missing ⚠️
...esis/src/instruction_selector/select_with_stack.rs	97.05%	1 Missing ⚠️

📢 Thoughts on this report? Let us know!