fix(798): trap Int/Nat arithmetic overflow + Tier-1 obligation (v0.0.181)

AGENTS.md

@@ -8,7 +8,7 @@ Read `SKILL.md` for the full language reference. It covers syntax, slot referenc
 
 ### Conformance programs as reference
 
-The conformance suite in `tests/conformance/` contains 92 small programs — often one per language feature — that serve as minimal working examples. Most are self-contained; the exception is `ch07_cross_module_contracts.vera`, which imports its `ch07_cross_module_contracts_lib.vera` companion to exercise cross-module contracts. Each program must pass its declared verification level (see `manifest.json` for mappings: `parse`, `check`, `verify`, or `run`). When you need to see how a specific construct works (e.g. effect handlers, match expressions, closures), check the corresponding conformance program before reading the spec.
+The conformance suite in `tests/conformance/` contains 93 small programs — often one per language feature — that serve as minimal working examples. Most are self-contained; the exception is `ch07_cross_module_contracts.vera`, which imports its `ch07_cross_module_contracts_lib.vera` companion to exercise cross-module contracts. Each program must pass its declared verification level (see `manifest.json` for mappings: `parse`, `check`, `verify`, or `run`). When you need to see how a specific construct works (e.g. effect handlers, match expressions, closures), check the corresponding conformance program before reading the spec.
 
 ### Workflow
 
@@ -182,7 +182,7 @@ Each stage is a module with a single public API function (`parse_file`, `transfo
 pytest tests/ -v                       # Run all tests (see TESTING.md)
 pytest tests/test_conformance.py -v    # Conformance suite only
 mypy vera/                             # Type-check the compiler
-python scripts/check_conformance.py    # All 92 conformance programs must pass
+python scripts/check_conformance.py    # All 93 conformance programs must pass
 python scripts/check_examples.py       # All 35 examples must pass
 ```
 
@@ -192,7 +192,7 @@ When implementing a new language feature, write the conformance program *first*
 
 ### Invariants
 
-- All 92 conformance programs in `tests/conformance/` must pass their declared level
+- All 93 conformance programs in `tests/conformance/` must pass their declared level
 - All 35 examples in `examples/` must pass `vera check` and `vera verify`
 - `mypy vera/` must be clean
 - `pytest tests/ -v` must pass

CHANGELOG.md

@@ -6,6 +6,12 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
 
 ## [Unreleased]
 
+## [0.0.181] - 2026-06-27
+
+### Fixed
+
+- **Verifier + codegen soundness: `@Int` / `@Nat` arithmetic overflow now traps** (batch 4 of the [#392](https://github.com/aallan/vera/issues/392) `smt.py` soundness audit).  The verifier modelled `@Int` / `@Nat` as Z3's *unbounded* integers, so `+` / `-` / `*` were total — it proved postconditions the i64 / u64 runtime then violated under two's-complement wraparound: `ensures(@Int.result > @Int.0)` for `{ @Int.0 + 1 }` verified at Tier 1, yet `inc(i64.MAX)` wraps to `i64.MIN`.  `@Int` / `@Nat` `+` / `-` / `*` are now *partial* operations that **trap** on overflow at runtime (consistent with `@Nat` underflow and signed-division `MIN / -1`), and the verifier auto-synthesises an `int_overflow` obligation that the result stays in range — a two-check mirroring array bounds: provably in range → Tier 1; provably out of range (e.g. a literal `u64.MAX + 1`, or `@Int.0 + 1` under `requires(@Int.0 == i64.MAX)`) → a compile error (**E528**); dynamic operands → a runtime-guarded Tier-3 overflow trap.  Overflow is classified at the operands' **common (coerced) type** (`@Int` if either operand is `@Int`), so a literal-left `5 + @Int.0` and an `@Int + 1` narrowed into a `@Nat` slot are both i64 adds — not the literal's `@Nat` self-type nor the narrowed result.  `@Nat` subtraction stays the existing underflow obligation (E502).  The runtime overflow trap is currently the generic `unreachable` kind; a precise `overflow` kind is tracked as [#808](https://github.com/aallan/vera/issues/808).  ([#798](https://github.com/aallan/vera/issues/798))
+
 ## [0.0.180] - 2026-06-26
 
 ### Fixed
@@ -2598,7 +2604,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.180...HEAD
+[Unreleased]: https://github.com/aallan/vera/compare/v0.0.181...HEAD
+[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
 [0.0.179]: https://github.com/aallan/vera/compare/v0.0.178...v0.0.179
 [0.0.178]: https://github.com/aallan/vera/compare/v0.0.177...v0.0.178

CLAUDE.md

@@ -53,7 +53,7 @@ VERA_JS_COVERAGE=1 pytest tests/test_browser.py -v  # Browser tests with JS cove
 VERA_EAGER_GC=1 vera run file.vera  # Force GC on every alloc (see ENVIRONMENT.md, debug knob for #593-class GC-rooting bugs)
 mypy vera/                        # Type-check the compiler itself
 
-python scripts/check_conformance.py    # Verify all 92 conformance programs pass their declared level
+python scripts/check_conformance.py    # Verify all 93 conformance programs pass their declared level
 python scripts/check_examples.py      # Verify all 35 examples parse + check + verify
 python scripts/check_examples_readme.py # Verify vera run commands in examples/README.md
 python scripts/check_spec_examples.py # Verify spec code blocks parse
@@ -82,7 +82,7 @@ See [`TOOLCHAIN.md`](TOOLCHAIN.md) for the CLI cookbook — driving the toolchai
 - `vera/` — Reference compiler: grammar, parser, AST, transformer, type checker, verifier, codegen, CLI
 - `examples/` — 35 example Vera programs (all must pass `vera check` and `vera verify`)
 - `tests/` — Test suite (unit tests + conformance suite)
-- `tests/conformance/` — 92 conformance programs validating every language feature against the spec
+- `tests/conformance/` — 93 conformance programs validating every language feature against the spec
 - `scripts/` — CI and validation scripts
 
 ## Writing Vera code
@@ -119,7 +119,7 @@ Before changing code — **adding or removing** — write the test that proves y
 ## What not to break
 
 - Pre-commit hooks run mypy + pytest + conformance suite + example validation on every commit
-- All 92 conformance programs in `tests/conformance/` must pass their declared level
+- All 93 conformance programs in `tests/conformance/` must pass their declared level
 - All 35 examples in `examples/` must pass `vera check` and `vera verify`
 - Version must stay in sync across `vera/__init__.py`, `pyproject.toml`, and `CHANGELOG.md`
 - All tests must pass: `pytest tests/ -v`

FAQ.md

@@ -173,7 +173,7 @@ None of this is Vera-specific, but it validates the design choices. The thesis i
 
 This is a real concern. LLMs are trained on trillions of tokens of Python, TypeScript, and JavaScript. A MojoBench study (NAACL 2025) found that even fine-tuned models achieved only 30–35% improvement over base models on Mojo code generation, illustrating the cold-start problem for new languages.
 
-Vera's approach has three parts. First, the agent-facing documentation (SKILL.md) is designed to be dropped into a model's context window, so the model works from the language specification rather than training data recall. Second, Vera's syntax is deliberately simple and regular — fewer constructs, each with exactly one canonical form — which reduces the surface area a model needs to learn. Third, the conformance test suite (92 programs covering every language feature) gives models concrete examples to learn from and conform to. Simon Willison argued in December 2025 that a language-agnostic conformance suite is the single most important tool for LLM adoption of a new language — LLMs can learn new languages remarkably well when given tests to conform to.
+Vera's approach has three parts. First, the agent-facing documentation (SKILL.md) is designed to be dropped into a model's context window, so the model works from the language specification rather than training data recall. Second, Vera's syntax is deliberately simple and regular — fewer constructs, each with exactly one canonical form — which reduces the surface area a model needs to learn. Third, the conformance test suite (93 programs covering every language feature) gives models concrete examples to learn from and conform to. Simon Willison argued in December 2025 that a language-agnostic conformance suite is the single most important tool for LLM adoption of a new language — LLMs can learn new languages remarkably well when given tests to conform to.
 
 
 ## How does Vera compare to Dafny / Lean / Koka / F*?
@@ -214,7 +214,7 @@ The reference compiler is under active development. The current release includes
 
 - A seven-stage pipeline: parse, transform, resolve, typecheck, verify, compile, execute
 - A 13-chapter formal specification
-- Over 3,000 unit tests plus a 92-program conformance suite
+- Over 3,000 unit tests plus a 93-program conformance suite
 - 35 working example programs
 - 164 built-in functions covering strings, arrays, math, parsing, and data types
 - Four built-in abilities (Eq, Ord, Hash, Show) with constrained generics and ADT auto-derivation

HISTORY.md

@@ -391,6 +391,7 @@ Proof obligations became first-class records with a warm Z3 session, and the LSP
 | v0.0.178 | 25 Jun | **`vera builtins/effects/errors --json` compiler introspection subcommands make the compiler the source of truth for its own built-ins, effects, and error codes, each with a best-effort `since` version** ([#539](https://github.com/aallan/vera/issues/539)). |
 | v0.0.179 | 26 Jun | **The `smt.py` soundness-audit batch lands: signed `/` and `%` truncate toward zero, a body `assert(P)` carries a Tier-1 obligation (loud `E507`), contract-position divisions get a `div_zero` obligation, and a prior `assert`/`assume` now discharges later obligations plus the postcondition at Tier 1** ([#392](https://github.com/aallan/vera/issues/392)). |
 | 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)). |
 
 ---
 
@@ -406,4 +407,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, 180 tagged releases, 77 active development days.**
+Total: **1,400+ commits, 181 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.180 — 1,400+ commits, 180 releases, 4,950 tests, 91% code coverage, 92 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.181 — 1,400+ commits, 181 releases, 5,156 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
 
-4,950 tests, 92 conformance programs, 35 examples, 13 spec chapters.
+5,156 tests, 93 conformance programs, 35 examples, 13 spec chapters.
 
 ## The roadmap
 
@@ -22,6 +22,7 @@ The infrastructure that catches the next regression before a user does, plus the
 |---|---|
 | [#392](https://github.com/aallan/vera/issues/392) | Audit the `smt.py` Z3 translation layer for soundness — a bug here silently bypasses verification. |
 | [#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. |
 | [#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). |

SKILL.md

@@ -134,7 +134,7 @@ Every diagnostic has a stable error code grouped by compiler phase:
 - **E120–E176** — Type check: core + expressions (type mismatches, slot resolution, operators)
 - **E200–E233** — Type check: calls (unresolved functions, argument mismatches, module calls)
 - **E300–E335** — Type check: control flow (if/match, patterns, effect handlers)
-- **E500–E525** — Verification (contract violations, undecidable fallbacks)
+- **E500–E528** — Verification (contract violations, undecidable fallbacks, primitive-operation safety incl. arithmetic overflow)
 - **E600–E614** — Codegen (unsupported features, typed holes block compilation)
 - **E700–E702** — Testing (contract violations, input generation, execution errors)