finding: synth#869 accepted for v0.52 — family is 8 not 6; trunc_sat already lowers so float->i64 needs no builtin - #173
Merged
Conversation
…already lowers, so the float->i64 half needs no builtin
synth accepted #869 for v0.52 with two corrections, both confirmed by jess re-probe:
(a) COMPLETENESS: the family is EIGHT — i64.trunc_f64_s/_u also skip (synth#756 had it as a
separate selector gap). Verified skipped set is now exact.
(b) SOUNDNESS (synth's catch): the trunc ops are MORE-TOTAL on ARM than in wasm — __aeabi_f2lz/
f2ulz do NOT trap (saturate/garbage on NaN + out-of-range) while wasm REQUIRES a trap, so a
bare builtin call would be a SILENT MISCOMPILE, strictly worse than today's honest skip.
synth will emit domain guards + execute trap cases vs wasmtime (the #709 guard shape).
JESS FINDING that shrinks the job: the four SATURATING variants (i64.trunc_sat_f32_s/u,
i64.trunc_sat_f64_s/u) ALREADY LOWER today (nm: T). So the float->i64 half needs NO builtin —
the trapping variants = existing working trunc_sat lowering + trap guard, and synth never imports
the more-total AEABI totality it would then have to fence. Job splits cleanly:
i64->float (4 convert): genuinely needs AEABI __aeabi_ul2f/l2f/ul2d/l2d
float->i64 (4 trunc): reuse trunc_sat + guard
Supplied the exact trap vectors (NaN, ±inf, >=2^63 / <-2^63 with -2^63 itself non-trapping;
<=-1.0 and >=2^64 for _u with -0.0 and (-1,0) -> 0). Committed jess to running any branch against
the real fused falcon + per-stage components, reporting skip delta BY SYMBOL NAME.
Verified: probe on synth 0.51.0, nm-confirmed lowered/skipped sets; rivet validate PASS.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
synth accepted #869 for v0.52, with two corrections — both confirmed by a jess re-probe.
synth's corrections (both right)
i64.trunc_f64_s/_ualso skip (synth#756 had recordedi64.trunc_f64as a separate selector gap). My original list missed them.truncops are more-total on ARM than in WASM:__aeabi_f2lz/f2ulzdo not trap (they saturate or return garbage on NaN/out-of-range) while WASM requires a trap. A barebl __aeabi_f2lzwould be a silent miscompile — strictly worse than today's honest skip. synth will emit domain guards and execute the trap cases against wasmtime as part of the gate (the #709 guard shape; the class that bit #633/#666/#709/#665/#642).jess finding that shrinks the job
Re-probing the full family turned up something useful: the four saturating variants already lower today (
i64.trunc_sat_f32_s/u,i64.trunc_sat_f64_s/u→nm: T).So the float→i64 half needs no builtin at all — the trapping variants are the existing, working
trunc_satlowering plus a trap guard. That also means synth never imports the more-total AEABI semantics it would then have to fence away. The job splits cleanly:convert__aeabi_ul2f/l2f/ul2d/l2d)trunctrunc_sat+ trap guardAlso supplied the exact trap vectors for the gate (NaN, ±inf,
≥2^63/< -2^63with-2^63itself non-trapping;≤ -1.0and≥ 2^64for_u, with-0.0and(-1,0)→0), and committed jess to running any branch against the real fused falcon + per-stage components, reporting the skip delta by symbol name — a standing gate, not a one-off.rivet validate→ PASS.🤖 Generated with Claude Code