feat(808): precise overflow trap kind + fix postcondition host-import ordering (#823)

[aallan]

Summary

Closes #808 and #823 (both follow-ups to #798).

The #798 @Int / @Nat arithmetic-overflow runtime guard trapped via a bare unreachable, so a dynamic overflow was classified kind="unreachable" and surfaced the generic non-exhaustive-match Fix paragraph — indistinguishable from an unrelated unreachable. This wires the guard to a new vera.overflow_trap host import (mirroring vera.contract_fail), so an integer overflow now classifies kind="overflow" and carries the overflow Fix paragraph.

Design

The guard emits call $vera.overflow_trap immediately before its unreachable. The host signals an out-of-band channel (last_overflow, mirroring contract_fail's last_violation) that _classify_trap checks before the str(exc) substring scan — which would otherwise match the trailing unreachable first. More robust than message-matching: classification never depends on wasmtime's exact trap text. Both runtimes provide the binding: wasmtime in execute() and the browser/Node runtime.mjs import builder (without it, a --target browser bundle LinkErrors on any arithmetic).

#823 — the postcondition import-ordering bug this exposed (also fixed here)

vera.overflow_trap was the first new host import since codegen's per-function flag-propagation was written, and it exposed a latent bug: codegen propagated a function's accumulated host-import + resource flags from the per-function context to the module before lowering postconditions. So a builtin or allocation reachable only through an ensures(...) predicate set its flag too late — the import / memory / GC declaration was omitted and the orphaned call/global.get failed WAT compilation. This hit the overflow guard (unknown func: $vera.overflow_trap), every other host-import family (unknown func: $vera.sin, …), and allocation (unknown global: $gc_sp).

I originally filed this as a separate follow-up (#823) and deferred it; that was wrong — it's the same one-relocation fix and I was already in the code. The propagation now runs after _compile_postconditions, fixing the whole class at once. Verified safe: nothing between the old and new position reads these flags (they're consumed only at module assembly), so the move is purely additive in correctness.

Adversarial review pass

A multi-lens review (propagation / instantiation-hosts / signal-correctness / coverage / release-docs, each finding verified against current code) caught the #823 regression, an unpinned int_mul b==INT_MIN trap branch (now tested), and that the overflow Fix paragraph named only the i64 range though #808 newly routes @Nat/u64 overflows through it (paragraph now names both).

Exit checklist

• Host import vera.overflow_trap called before unreachable (mirrors vera.contract_fail); kind="overflow" with the overflow Fix paragraph (now accurate for both i64/@Int and u64/@Nat)
• Import declared wherever a guard can appear — body, precondition, postcondition, lifted closure — via a single post-postcondition propagation
• test_int_overflow_codegen.py asserts kind == "overflow": all five +/-/* sites, both int_mul trap branches, lifted-closure path, ensures(...)-postcondition path; controls (mutation-validated) keep Nat subtraction silently underflows to negative i64 — refinement-type soundness hole #520/verifier: @Nat → @Int widening of a value > i64.MAX is unsound (Tier-1 proves a false postcondition) #813 at unreachable
• test_codegen.py::TestPostconditionHostImportPropagation823: math host-import + allocation in a postcondition over a scalar body (mutation-validated)
• test_browser.py: wasmtime↔Node parity (mutation-validated: missing binding → LinkError)

Gate floor

• pytest tests/ — green · mypy vera/ — clean · conformance (103) · examples (35)
• check_version_sync (0.0.187 × 6) · check_doc_counts (5457) · check_site_assets · CHANGELOG gate · doc-example validators

Release prep (0.0.186 → 0.0.187)

Version bumped across all 6 sync points; CHANGELOG [0.0.187] (two entries: #808 overflow kind, #823 postcondition propagation; folds in the merged-but-unreleased doc-consistency pass); HISTORY Stage 15 row; ROADMAP #808 row deleted; spec/11 + TESTING updated; #823 removed from KNOWN_ISSUES (closed by this PR).

Notes for review

• No conformance test: trap-kind classification and codegen import-ordering are runtime/codegen concerns, not check/verify-level features — covered by test_int_overflow_codegen.py + test_runtime_traps.py + test_codegen.py + test_browser.py.
• The verifier: @Nat → @Int widening of a value > i64.MAX is unsound (Tier-1 proves a false postcondition) #813 widen and Nat subtraction silently underflows to negative i64 — refinement-type soundness hole #520 nat_sub guards deliberately keep bare unreachable (dedicated kinds deferred, @Nat narrowing: effect-op-argument runtime guard + dedicated guard trap kind #754 / @Nat → @Int widening: remaining deferred coercion sites (follow-up to #813) #820); comments updated to cite Precise overflow trap kind for #798 integer-overflow traps (currently unreachable) #808 as the landed precedent.

🤖 Generated with Claude Code

Summary by CodeRabbit

• Bug Fixes

  • Integer-overflow traps are now classified with an overflow kind and clearer “Integer overflow” diagnostics, with consistent behaviour across browser and runtime.
  • Host-import and allocation/GC requirements referenced only within requires(...)/ensures(...) postconditions are now correctly propagated during lowering.

• Tests

  • Added browser/Python overflow-trap parity coverage, plus regression tests for postcondition-only host/import propagation and overflow classification.

• Documentation

  • Updated changelog, versioning, history, README, roadmap, testing guidance, and the overflow-handling spec for the new release snapshot.

[coderabbitai]

No actionable comments were generated in the recent review. 🎉

ℹ️ Recent review info

⚙️ Run configuration

Configuration used: Path: .coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: 84abd574-5983-4943-b5fe-18e7ed228e59

📥 Commits

Reviewing files that changed from the base of the PR and between 151a264 and 5cee7d1.

📒 Files selected for processing (1)

• HISTORY.md

---

📝 Walkthrough

Walkthrough

Adds a dedicated overflow trap path for integer arithmetic, propagates the new trap signal through runtime classification and the browser harness, defers postcondition flag propagation, and updates tests plus release and documentation files.

Changes

Overflow trap kind and postcondition propagation

Layer / File(s)	Summary
Overflow guard emission vera/wasm/context.py, vera/codegen/core.py, vera/wasm/operators.py, vera/codegen/assembly.py	WasmContext and CodeGenerator gain _needs_overflow_trap; overflow guards now call vera.overflow_trap, set the flag, and trigger a conditional module import.
Trap classification and browser runtime vera/runtime/traps.py, vera/codegen/api.py, vera/browser/runtime.mjs	_classify_trap accepts last_overflow and classifies it as overflow; execute() passes the new signal through; the browser runtime tracks lastOverflow and maps the trap to Integer overflow.
Postcondition propagation vera/codegen/functions.py, vera/codegen/closures.py	Contract predicate scanning and deferred flag copying keep host-import and allocation requirements, including overflow trapping, visible after postcondition lowering and across lifted closures.
Tests and validation tests/test_int_overflow_codegen.py, tests/test_codegen.py, tests/test_browser.py, tests/test_runtime_traps.py	Adds coverage for overflow trap kind, closure overflow, ensures(...) overflow, postcondition import propagation, browser parity, and trap-classification precedence.
Release metadata and docs pyproject.toml, vera/__init__.py, README.md, CHANGELOG.md, HISTORY.md, ROADMAP.md, TESTING.md, spec/11-compilation.md	Bumps version to 0.0.187 and updates release notes, metrics, roadmap/testing tables, and the compilation spec to reflect the new overflow trap path.

Estimated code review effort

🎯 3 (Moderate) | ⏱️ ~25 minutes

Possibly related PRs

• aallan/vera#533: Both PRs modify the same trap classification and diagnostics flow in vera/codegen/api.py and vera/runtime/traps.py.
• aallan/vera#548: Both PRs extend the per-kind trap diagnostics path and use the same fix-paragraph machinery.
• aallan/vera#598: Both PRs touch closure lifting in vera/codegen/closures.py, though for different runtime-side concerns.

Suggested labels

compiler, tests, spec, docs

🚥 Pre-merge checks | ✅ 4 | ❌ 1

❌ Failed checks (1 warning)

Check name	Status	Explanation	Resolution
Docstring Coverage	⚠️ Warning	Docstring coverage is 45.65% which is insufficient. The required threshold is 80.00%.	Write docstrings for the functions missing them to satisfy the coverage threshold.

✅ Passed checks (4 passed)

Check name	Status	Explanation
Description Check	✅ Passed	Check skipped - CodeRabbit’s high-level summary is enabled.
Title check	✅ Passed	The title clearly names the main overflow-trap fix and the postcondition import-ordering follow-up.
Linked Issues check	✅ Passed	The PR implements the #808 overflow-trap host import and updates tests to expect overflow classifications.
Out of Scope Changes check	✅ Passed	The extra docs, version bumps, and runtime/test updates support the overflow-trap and propagation fixes rather than adding unrelated features.

✨ Finishing Touches

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Commit unit tests in branch feat/808-overflow-trap-kind

---

_{Comment @coderabbitai help to get the list of available commands.}

[codecov]

Codecov Report

❌ Patch coverage is 98.27586% with 1 line in your changes missing coverage. Please review.
✅ Project coverage is 92.05%. Comparing base (3e1feb9) to head (5cee7d1).

Files with missing lines	Patch %	Lines
vera/browser/runtime.mjs	95.65%	1 Missing ⚠️

Additional details and impacted files

@@           Coverage Diff           @@
##             main     #824   +/-   ##
=======================================
  Coverage   92.05%   92.05%           
=======================================
  Files          89       89           
  Lines       27258    27299   +41     
  Branches      321      324    +3     
=======================================
+ Hits        25091    25131   +40     
- Misses       2159     2160    +1     
  Partials        8        8           

Flag	Coverage Δ
javascript	65.58% <95.65%> (+0.25%)	⬆️
python	95.06% <100.00%> (+<0.01%)	⬆️

Flags with carried forward coverage won't be shown. Click here to find out more.

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

[aallan]

pr-review-toolkit summary

Ran three specialized reviewers over the diff (code-reviewer, comment-analyzer, silent-failure-hunter), plus an earlier multi-lens adversarial pass. Net: the change is sound; the items surfaced were hardening, all addressed.

code-reviewer — no actionable findings. Independently confirmed the flag-propagation relocation is load-bearing (the AST pre-scan walks only the function body, never contract expressions, so a postcondition-only import reaches the module solely via the ctx-merge) and verified nothing between the old and new merge position reads the flags.

comment-analyzer — no inaccuracies; all 8 issue references verified against code. Two precision nits applied:

• vera/wasm/context.py — name the closures.py merge path alongside functions.py.
• tests/test_int_overflow_codegen.py — cite #820 as the exact widen-kind tracker (not #754, which is the narrowing sibling).

silent-failure-hunter — sound on all three axes (staleness, ordering, browser leak); no silent-misclassification path. One observation applied:

• The last_overflow precedence ordering (beats the unreachable substring; loses to last_violation) had no end-to-end coverage — a single trap signals only one channel — so I added two helper-level unit tests in tests/test_runtime_traps.py pinning it directly.
• Its second observation (a browser cross-call leak regression test) was left out deliberately: the unconditional lastOverflow = false reset at the top of call() makes the leak impossible by construction, and exercising it would need two calls on one instance the Node harness doesn't expose.

Both reviewers also noted a non-actionable, pre-existing observation unrelated to this PR: a closure literal placed inside an ensures(...) predicate would not be lifted (it registers after _lift_pending_closures runs). Vera doesn't currently accept closure literals in contract predicates in a way that reaches codegen, so it's noted for awareness only.

[aallan]

@coderabbitai full review

[coderabbitai]

✅ Action performed

Full review finished.

[coderabbitai]

Actionable comments posted: 2

Caution

Some comments are outside the diff and can’t be posted inline due to platform limitations.

⚠️ Outside diff range comments (1)

vera/codegen/closures.py (1)

447-462: 🎯 Functional Correctness | 🟠 Major | ⚡ Quick win

Keep lifted-closure host flag propagation in sync.

The overflow flag is now forwarded, but this closure-context merge still omits other host-backed builtin flags such as Markdown, regex, HTTP, inference, random, and math. If a lifted closure is the only caller, its WAT can reference a host import that the module never declares.

Proposed fix

         self._decimal_imports.update(ctx._decimal_imports)
         self._json_ops_used.update(ctx._json_ops_used)
         self._html_ops_used.update(ctx._html_ops_used)
+        self._md_ops_used.update(ctx._md_ops_used)
+        self._regex_ops_used.update(ctx._regex_ops_used)
+        self._http_ops_used.update(ctx._http_ops_used)
+        self._inference_ops_used.update(ctx._inference_ops_used)
+        self._random_ops_used.update(ctx._random_ops_used)
+        self._math_ops_used.update(ctx._math_ops_used)
         # `#808`: a `#798` integer-overflow guard inside a lifted closure body sets

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@vera/codegen/closures.py` around lines 447 - 462, The lifted-closure merge in
the closure context propagation path is only forwarding overflow-trap state, but
it still misses other host-backed builtin usage flags. Update the merge logic in
the closure context handling to propagate the same host-import tracking fields
used elsewhere for Markdown, regex, HTTP, inference, random, math, and any
similar builtin import/usage sets from ctx into self, so module assembly can
emit all required imports when a lifted closure is the only caller.

🤖 Prompt for all review comments with AI agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

Inline comments:
In `@CHANGELOG.md`:
- Around line 9-16: The changelog entry for the host-import propagation fix is
missing the `html_*` import family even though the actual fix in
`vera/codegen/functions.py` also merges `_html_ops_used` after
`_compile_postconditions`. Update the `CHANGELOG.md` bullet describing
`tests/test_codegen.py::TestPostconditionHostImportPropagation823` so it
explicitly includes `html_*` alongside the other host-import families, keeping
the summary aligned with the shipped behavior.

In `@vera/codegen/functions.py`:
- Around line 431-462: The deferred flag merge in the module assembly path is
still missing the Markdown and regex host import sets, so `ensures(...)`
lowering can set those flags without `_assemble_module` seeing them. Update the
postconditions merge in this section to also propagate `ctx._md_ops_used` and
`ctx._regex_ops_used` into the corresponding `self` fields, alongside the
existing `_map_*`, `_set_*`, and other host-flag updates, so `md_*` and
`regex_*` imports are preserved.

---

Outside diff comments:
In `@vera/codegen/closures.py`:
- Around line 447-462: The lifted-closure merge in the closure context
propagation path is only forwarding overflow-trap state, but it still misses
other host-backed builtin usage flags. Update the merge logic in the closure
context handling to propagate the same host-import tracking fields used
elsewhere for Markdown, regex, HTTP, inference, random, math, and any similar
builtin import/usage sets from ctx into self, so module assembly can emit all
required imports when a lifted closure is the only caller.

🪄 Autofix (Beta)

Fix all unresolved CodeRabbit comments on this PR:

• Push a commit to this branch (recommended)
• Create a new PR with the fixes

---

ℹ️ Review info

⚙️ Run configuration

Configuration used: Path: .coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro

Run ID: 3d3b4286-7a1c-472d-a437-8abb60779126

📥 Commits

Reviewing files that changed from the base of the PR and between 3e1feb9 and 0762d2a.

⛔ Files ignored due to path filters (5)

• docs/index.html is excluded by !docs/**
• docs/index.md is excluded by !docs/**
• docs/llms-full.txt is excluded by !docs/**
• docs/llms.txt is excluded by !docs/**
• uv.lock is excluded by !**/*.lock, !uv.lock

📒 Files selected for processing (21)

• CHANGELOG.md
• HISTORY.md
• README.md
• ROADMAP.md
• TESTING.md
• pyproject.toml
• spec/11-compilation.md
• tests/test_browser.py
• tests/test_codegen.py
• tests/test_int_overflow_codegen.py
• tests/test_runtime_traps.py
• vera/__init__.py
• vera/browser/runtime.mjs
• vera/codegen/api.py
• vera/codegen/assembly.py
• vera/codegen/closures.py
• vera/codegen/core.py
• vera/codegen/functions.py
• vera/runtime/traps.py
• vera/wasm/context.py
• vera/wasm/operators.py

[aallan]

@coderabbitai Re: the outside-diff note that vera/codegen/closures.py misses md / regex / http / inference / random / math host-import propagation — verified against current code, those are already covered, so closures.py is intentionally unchanged.

The body host-import pre-scan (compilability.py::_scan_io_ops) recurses into AnonFn bodies, so a lifted closure's ops-used flags are registered on the module independently of the closure merge. Confirmed empirically by compiling a closure-only sin(...) call: the emitted WAT carries both the sin import and the call.

The closure merge only needs the ctx-only families the pre-scan can't see — _map_imports / _set_imports / _decimal_imports (the import strings generated during translation) plus vera.overflow_trap — all of which it already forwards. Adding the ops-used families would be dead code.

The one genuine gap, md / regex in a contract predicate, is fixed in 151a264 (see the vera/codegen/functions.py review thread).

[coderabbitai]

Tip

For best results, initiate chat on the files or code changes.

@aallan Thanks — that clarification checks out, and I’m withdrawing that vera/codegen/closures.py concern.

The key distinction is clear:

• compilability.py::_scan_io_ops already recurses into AnonFn bodies, so the ops-used families (md / regex / http / inference / random / math) are registered at module scope independently of the lifted-closure merge.
• vera/codegen/closures.py only needs to forward the ctx-only translation-time families plus vera.overflow_trap, which it already does.

Good catch on the real remaining gap as well: md / regex referenced only from a contract predicate belongs in the vera/codegen/functions.py path, not the closure merge.

---

✏️ Learnings added

Learnt from: aallan
URL: https://github.com/aallan/vera/pull/824

Timestamp: 2026-06-30T11:36:39.037Z
Learning: In Vera, `compilability.py::_scan_io_ops` recurses into `AnonFn` bodies, so lifted-closure ops-used host-import families such as `md`, `regex`, `http`, `inference`, `random`, and `math` are registered on the module during the body pre-scan rather than via `vera/codegen/closures.py`.

---

Learnt from: aallan
URL: https://github.com/aallan/vera/pull/824

Timestamp: 2026-06-30T11:36:39.037Z
Learning: In Vera, `vera/codegen/closures.py` intentionally forwards only ctx-only closure state that the body pre-scan cannot see: `_map_imports`, `_set_imports`, `_decimal_imports`, and `vera.overflow_trap`. Adding ops-used family propagation there would be dead code.

---

Learnt from: aallan
URL: https://github.com/aallan/vera/pull/824

Timestamp: 2026-06-30T11:36:39.037Z
Learning: The genuine host-import propagation gap for this area was `md` / `regex` used only in a contract predicate; that fix belongs in `vera/codegen/functions.py` rather than `vera/codegen/closures.py`, and the user reports it was fixed in commit `151a264`.

Note: Learnings are effective only in the context of similar code segments. To apply general coding guidelines, please configure review instructions. You can manage existing learnings in the app.

[aallan]

@coderabbitai full review

[coderabbitai]

✅ Action performed

Full review finished.

[coderabbitai]

Actionable comments posted: 1

🤖 Prompt for all review comments with AI agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

Inline comments:
In `@HISTORY.md`:
- Line 426: The release snapshot test count in HISTORY.md is out of sync with
the rest of the v0.0.187 docs. Update the Tests value in the HISTORY table to
match the current count used in README.md, ROADMAP.md, and TESTING.md, and keep
the same number consistent across the snapshot.

🪄 Autofix (Beta)

Fix all unresolved CodeRabbit comments on this PR:

• Push a commit to this branch (recommended)
• Create a new PR with the fixes

---

ℹ️ Review info

⚙️ Run configuration

Configuration used: Path: .coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: 1520f92b-c3a2-47e5-8563-58ea26383d7f

📥 Commits

Reviewing files that changed from the base of the PR and between 3e1feb9 and 151a264.

⛔ Files ignored due to path filters (5)

• docs/index.html is excluded by !docs/**
• docs/index.md is excluded by !docs/**
• docs/llms-full.txt is excluded by !docs/**
• docs/llms.txt is excluded by !docs/**
• uv.lock is excluded by !**/*.lock, !uv.lock

📒 Files selected for processing (21)

• CHANGELOG.md
• HISTORY.md
• README.md
• ROADMAP.md
• TESTING.md
• pyproject.toml
• spec/11-compilation.md
• tests/test_browser.py
• tests/test_codegen.py
• tests/test_int_overflow_codegen.py
• tests/test_runtime_traps.py
• vera/__init__.py
• vera/browser/runtime.mjs
• vera/codegen/api.py
• vera/codegen/assembly.py
• vera/codegen/closures.py
• vera/codegen/core.py
• vera/codegen/functions.py
• vera/runtime/traps.py
• vera/wasm/context.py
• vera/wasm/operators.py