Tier-1 modeling for the modelable Float64 builtins deferred from #797 (float_clamp, int_to_float, float_to_int)

[aallan]

Follow-up to #797 (the #392 smt.py soundness audit's @Float64 → FloatingPoint-sort fix).

#797 modelled @Float64 with Z3's IEEE-754 FloatingPoint sort, making the arithmetic / comparison / % operators and the float_is_nan / float_is_infinite / nan() / infinity() builtins sound at Tier 1. The remaining Float64-related builtins stay Tier-3. The #806 review correctly flagged that "deferred completeness" hand-waved three genuinely different situations into one bucket — here they are, honestly:

A. Cannot be modelled — Tier-3 by necessity (NOT deferred; out of scope here)

float_to_string, parse_float64, decimal_from_float, decimal_to_float. Z3's string theory can't format/parse a float, and Decimal is an uninterpreted host handle (like Map / Set / regex). There is no sound Z3 model to write — these are Tier-3 permanently, the same way Map operations are. Listed only to make scope explicit; nothing to do.

B. Blocked by #798 — the actual deferred work

int_to_float, float_to_int cross the Int↔Float boundary:

• The verifier's Int is unbounded; the runtime's is i64. That idealisation is the open verifier/smt.py: integer arithmetic overflow unmodeled — Tier 1 proves contracts false under i64/u64 wraparound #798 bug. Modelling int_to_float(n) as fpToFP(toReal(n)) is sound only where the Int model is sound — for out-of-i64 n it would entangle verifier/smt.py: integer arithmetic overflow unmodeled — Tier 1 proves contracts false under i64/u64 wraparound #798's overflow.
• float_to_int is worse: i64.trunc_f64_s traps on NaN / Inf / out-of-range, which the model would also have to capture.

Wiring these to FP before the Int side is sound risks shipping a new Tier-1/Tier-3 divergence — the same class #797 / #799 fixed. Blocked by #798.

C. Modellable now, needs a codegen differential (NOT blocked)

float_clamp is pure Float64 (no Int boundary, no #798). It is modellable — If(fpLT(x, lo), lo, If(fpGT(x, hi), hi, x)) — but its NaN / tie / ±0 semantics must be confirmed against vera/wasm with a verify-vs-run differential before landing (doing it blind is exactly the fp.rem-vs-fmod trap #797's audit caught). This sub-task is not blocked by #798 and can be done independently.

Acceptance

• int_to_float / float_to_int verify at Tier 1 once verifier/smt.py: integer arithmetic overflow unmodeled — Tier 1 proves contracts false under i64/u64 wraparound #798 lands, with a verify-vs-run differential confirming agreement at the i64 boundary (and float_to_int's trap on NaN / Inf / out-of-range).
• float_clamp modelled with a confirmed codegen differential.
• The four bucket-A builtins remain Tier-3 (no change — correct as-is).

Parent audit: #392. Origin: #797 (PR #806).