v0.0.183

Added

• Tier-1 verification modeling for the modelable @Float64 builtins float_clamp, int_to_float, and float_to_int (follow-up to #797, the #392 smt.py soundness audit's @Float64 → FloatingPoint-sort fix; the three were left as Tier-3 deferrals there). float_clamp(v, lo, hi) is modeled unconditionally as the faithful WASM f64.min(f64.max(v, lo), hi): Z3's own fp.min / fp.max diverge from WASM on NaN (SMT-LIB returns the non-NaN operand; WASM propagates NaN) and on signed zero, so the model builds those semantics explicitly — a naive fpMin / fpMax would unsoundly prove !float_is_nan(float_clamp(NaN, …)). int_to_float and float_to_int cross the Int↔Float boundary, where Z3's symbolic Int↔Real↔FP reasoning is unreliable (it returns spurious counterexamples that do not satisfy their own constraints), so they are modeled at Tier 1 only for a concrete (constant-foldable) argument and a symbolic one defers to a sound Tier 3 — matching the audit principle of deferring what Z3 cannot soundly model. float_to_int compiles to i64.trunc_f64_s, which traps on NaN / ±Inf / out-of-i64-range, so a concrete out-of-domain argument is now a loud compile error (E529) and a symbolic one a runtime-guarded Tier-3 trap. Each model is confirmed by a verify-vs-run differential. The four format/parse @Float64 builtins (float_to_string, parse_float64, decimal_from_float, decimal_to_float) remain Tier-3 by necessity. (#807)

Fixed

• Out-of-range integer literals are now a clean compile error (E149) instead of an opaque codegen failure or a silent unsoundness (found during the #807 review). An integer literal must fit its target machine type — @Int is i64, @Nat is u64. Previously a literal >= 2^64 was accepted by vera check then failed at codegen with a raw i64.const ... out of range error; worse, a literal in (i64.MAX, u64.MAX] used as @Int (e.g. 18446744073709551615) made vera verify prove ensures(@Int.result == 18446744073709551615) while the runtime returned -1 (the i64 reinterpretation of the all-ones bit pattern) — a Tier-1 proof the runtime violates. The checker now range-checks every integer literal against its target type's bound and emits E149 with a clear message; the asymmetric edge -9223372036854775808 (i64.MIN) stays valid. (#812)