feat(807): Tier-1 Float64 builtin modeling + integer-literal range check (#807, #812)

CHANGELOG.md

@@ -6,6 +6,16 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
 
 ## [Unreleased]
 
+## [0.0.183] - 2026-06-27
+
+### Added
+
+- **Tier-1 verification modeling for the modelable `@Float64` builtins `float_clamp`, `int_to_float`, and `float_to_int`** (follow-up to [#797](https://github.com/aallan/vera/issues/797), the [#392](https://github.com/aallan/vera/issues/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](https://github.com/aallan/vera/issues/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](https://github.com/aallan/vera/issues/812))
+
 ## [0.0.182] - 2026-06-27
 
 ### Fixed
@@ -2610,7 +2620,8 @@ Small docs sweep — closes six aging documentation issues in one PR.  No code c
 - Grammar: handler body simplified to avoid LALR reduce/reduce conflict
 - `pyproject.toml`: corrected build backend, package discovery, PEP 639 compliance
 
-[Unreleased]: https://github.com/aallan/vera/compare/v0.0.182...HEAD
+[Unreleased]: https://github.com/aallan/vera/compare/v0.0.183...HEAD
+[0.0.183]: https://github.com/aallan/vera/compare/v0.0.182...v0.0.183
 [0.0.182]: https://github.com/aallan/vera/compare/v0.0.181...v0.0.182
 [0.0.181]: https://github.com/aallan/vera/compare/v0.0.180...v0.0.181
 [0.0.180]: https://github.com/aallan/vera/compare/v0.0.179...v0.0.180

HISTORY.md

@@ -393,6 +393,7 @@ Proof obligations became first-class records with a warm Z3 session, and the LSP
 | v0.0.180 | 26 Jun | **`@Float64` contracts are verified against Z3's IEEE-754 FloatingPoint sort instead of mathematical reals, so Tier-1 proofs respect `NaN`/`Inf`/signed-zero/rounding and `%` (C `fmod`) and match the runtime, so unsound relational / reflexive Float64 contracts are now correctly rejected** ([#797](https://github.com/aallan/vera/issues/797)). |
 | v0.0.181 | 27 Jun | **`@Int` / `@Nat` arithmetic overflow now traps: `+` / `-` / `*` are partial operations carrying an auto-synthesised `int_overflow` obligation, so a result that provably leaves i64 / u64 range is a compile error (E528) and a dynamic one is a runtime-guarded trap, instead of the verifier proving postconditions the two's-complement runtime then violated** ([#798](https://github.com/aallan/vera/issues/798)). |
 | v0.0.182 | 27 Jun | **`string_length` UTF-8 byte soundness defers non-literal `string_length` to Tier 3 and models string literals at their exact byte length, completing the `smt.py` soundness audit** ([#802](https://github.com/aallan/vera/issues/802)). |
+| v0.0.183 | 27 Jun | **Tier-1 verification modeling for the modelable `@Float64` builtins: `float_clamp` (faithful WASM `f64.min`/`f64.max`, NaN/±0-correct), and concrete-gated `int_to_float` / `float_to_int` (symbolic args defer to Tier 3 since Z3's FP↔Real reasoning is unreliable), with a `float_to_int` domain obligation (E529) and verify-vs-run differentials** ([#807](https://github.com/aallan/vera/issues/807)).  Also range-checks integer literals against their target machine type (E149, #812), closing a silent unsoundness where a literal in (i64.MAX, u64.MAX] used as `@Int` verified but ran to `-1`. |
 
 ---
 
@@ -408,4 +409,4 @@ Proof obligations became first-class records with a warm Z3 session, and the LSP
 | Spec chapters | 7 | 10 | 11 | 12 | 13 | 13 | 13 | 13 |
 | Code coverage | — | — | — | 90% | 91% | 96% | 96% | 95% |
 
-Total: **1,400+ commits, 182 tagged releases, 77 active development days.**
+Total: **1,400+ commits, 183 tagged releases, 77 active development days.**

README.md

@@ -215,7 +215,7 @@ cp /path/to/vera/SKILL.md ~/.claude/skills/vera-language/SKILL.md
 
 ## Project status
 
-Vera is in **active development** at v0.0.182 — 1,400+ commits, 182 releases, 5,173 tests, 91% code coverage, 93 conformance programs, 35 examples, and a 13-chapter specification. See **[HISTORY.md](HISTORY.md)** for how the compiler was built.
+Vera is in **active development** at v0.0.183 — 1,400+ commits, 183 releases, 5,263 tests, 91% code coverage, 93 conformance programs, 35 examples, and a 13-chapter specification. See **[HISTORY.md](HISTORY.md)** for how the compiler was built.
 
 The reference compiler — parser, AST, type checker, contract verifier (Z3), WASM code generator, module system, browser runtime, and runtime contract insertion — is working. The language specification is in draft across [13 chapters](spec/).
 

ROADMAP.md

@@ -8,7 +8,7 @@ Priority lives in this file and nowhere else — issues carry kind and area labe
 
 ## Where we are
 
-5,173 tests, 93 conformance programs, 35 examples, 13 spec chapters.
+5,263 tests, 93 conformance programs, 35 examples, 13 spec chapters.
 
 ## The roadmap
 
@@ -20,8 +20,8 @@ The infrastructure that catches the next regression before a user does, plus the
 
 | Issue | What |
 |---|---|
-| [#807](https://github.com/aallan/vera/issues/807) | Tier-1 model the deferred-but-modelable `@Float64` builtins from #797.  **Blocked by #798**: `int_to_float`/`float_to_int` cross the Int↔Float boundary that the unbounded-`Int` idealisation (#798) makes unsound, so they wait on that fix; `float_clamp` is unblocked but needs a verify-vs-run codegen differential first.  The four format/parse builtins (`float_to_string`, `parse_float64`, `decimal_from_float`/`_to_float`) are Tier-3 by necessity, not deferred. |
 | [#808](https://github.com/aallan/vera/issues/808) | Give the `@Int` / `@Nat` arithmetic-overflow runtime trap (#798) a precise `overflow` trap kind, so a dynamic overflow surfaces as a dedicated trap message rather than the generic `unreachable` kind it currently shares. |
+| [#813](https://github.com/aallan/vera/issues/813) | **Soundness:** emit a verifier obligation at every `@Nat → @Int` coercion that the value is `<= i64.MAX`.  A `@Nat` value in (i64.MAX, u64.MAX] currently reinterprets to a negative `@Int` at runtime while Tier 1 proves over the unbounded non-negative value — a false postcondition (the `widen(u64.MAX)` repro).  Mirror with a codegen guard + verify-vs-run differential, like #798/#799.  Found during the #807 review. |
 | [#592](https://github.com/aallan/vera/issues/592) | End-to-end behavioural tests for the five UTF-8 decode sites currently pinned only by structural greps. |
 | [#645](https://github.com/aallan/vera/issues/645) | Explicit `encoding='utf-8'` at every text-mode file call, with a pre-commit check to hold the line. |
 | [#657](https://github.com/aallan/vera/issues/657) | Convert `INVARIANT_DEFENSIVE` sites and audit `PROPAGATE` cleanup (follow-up to the #626 error-handling taxonomy). |