v0.0.127: Close @Nat subtraction soundness hole (#520) by aallan · Pull Request #554 · aallan/vera

aallan · 2026-04-29T09:17:39Z

Closes #520. Spawns #551 (@Byte sibling — now mechanical follow-up) and #552 (architectural generalisation: @Nat invariant check at every binding site, not just subtraction).

The bug

The type system accepted @Nat - @Nat : @Nat but the runtime emitted a plain i64.sub with no underflow check, so a negative i64 could end up in a @Nat slot. Any Tier-1-verified contract relying on Nat >= 0 was logically undermined, and @Array<T>[@Nat.0] indexing with a bad @Nat became a memory-safety issue. The refinement-type layer's central promise — "this value is non-negative" — didn't hold.

Before / after

private fn unsafe(@Nat, @Nat -> @Nat)
  requires(true) ensures(true) effects(pure)
{
  @Nat.1 - @Nat.0
}

public fn main(@Unit -> @Nat)
  requires(true) ensures(true) effects(pure)
{
  unsafe(0, 1)   -- 0 - 1 underflows
}

Before (v0.0.126):

$ vera verify underflow.vera
OK: underflow.vera
Verification: 4 verified (Tier 1)

$ vera run underflow.vera
18446744073709551615   # silent: -1 reinterpreted as unsigned i64

After (v0.0.127), vera verify:

error: [E502] @Nat subtraction in 'unsafe' may underflow.
  Counterexample:
      @Nat.0 = 1
      @Nat.1 = 0
  Fix: Add a precondition that rules out the bad inputs,
       e.g. `requires(@Nat.0 >= @Nat.1)`.

After (v0.0.127), vera run skipping verification:

Error: WASM trap (kind: unreachable)
   ...

Two-sided implementation

The fix has a static half (verifier) and a runtime half (codegen) that share their detection logic exactly so both layers agree on what counts as a guarded site:

Static — verifier proof obligation

vera/verifier.py walks the function body via _walk_for_subtraction_obligations (mirrors _walk_for_calls structurally; descends through IfExpr / MatchExpr with smt._path_conditions push/pop, Block with let-binding env updates). At every BinaryExpr.SUB whose result is statically @Nat AND at least one operand has @Nat provenance, it emits a Tier-1 obligation lhs >= rhs and discharges via smt.check_valid against current preconditions + path conditions. If Z3 can't discharge, emits E502 with counterexample, rationale, fix suggestion, and spec ref to §4.4 + §11.2.1.

Runtime — codegen guard

vera/wasm/operators.py mirrors the verifier's detection (_is_static_nat_typed AND _has_nat_origin_codegen reproduce the verifier's analysis at AST level) and emits a guarded subtraction WAT sequence:

[lhs] [rhs]
local.set $rhs_tmp     ;; pop rhs into temp
local.tee $lhs_tmp     ;; pop lhs into temp, leave on stack
local.get $rhs_tmp     ;; push rhs back
i64.lt_s               ;; lhs < rhs?
if
  unreachable          ;; trap; classified by api.py as kind="unreachable"
end
local.get $lhs_tmp
local.get $rhs_tmp
i64.sub

Programs that ran vera verify first see the static error; programs that skip verification trap cleanly via the runtime guard rather than silently producing a negative @Nat. A dedicated kind="underflow" trap label requires new host-import scaffolding mirroring vera.contract_fail and is left as a follow-up enhancement; for now the trap is classified as the existing kind="unreachable".

Path-A scope: pure-literal subtractions exempt

The corpus uses 0 - 1 widely as the "I want -1" idiom (Err(_) -> 0 - 1, throw(0 - 1)) where the result is consumed at @Int positions and the upcast is well-defined. Both verifier and codegen require at least one operand to have @Nat provenance (a slot ref or function returning @Nat), so pure-literal subtractions are intentionally not flagged. Catching let @Nat = 0 - 1 requires the binding-site generalisation tracked as #552.

Migration

Zero corpus migration needed. Every existing @Nat - @Nat site in examples/ and tests/conformance/ is guarded by if @Nat.0 == 0 then base else recursive(@Nat.0 - 1) and Z3 discharges the obligation from the path condition automatically. External programs that previously verified at Tier 1 may now require explicit requires(lhs >= rhs) clauses; the diagnostic names the fix and shows the counterexample inputs.

Spec

spec/04-expressions.md §4.4 — short clause mirroring the divide-by-zero language: subtraction on unsigned types is undefined behaviour when it would underflow; the compiler SHOULD verify lhs >= rhs and MUST insert a runtime check otherwise.
spec/11-compilation.md §11.2.1 — full treatment with the Tier-1 proof obligation, Tier-3 fallback codegen, the lift-back path via requires, and references to @Byte subtraction silent underflow (follow-up to #520) #551 (@byte) and Generalize @Nat invariant check to all binding sites (broader generalisation of #520) #552 (binding-site generalisation).
spec/11-compilation.md §11.3.3 — footnote on the operator table pointing back to §11.2.1 so readers of the canonical "what does each operator compile to" reference learn that @Nat - @Nat is conditionally guarded.

Tests

New TestNatSubtractionObligation520 in tests/test_verifier.py (9 tests):

requires-clause discharge
if-guard / path-condition discharge (canonical recursion shape)
trivial discharges (@Nat.0 - 0, @Nat.0 - @Nat.0)
unguarded-subtract counterexample
@Int - @Int and @Nat - @Int → @Int exclusions
partial-requires non-discharge
pure-literal exclusion documenting Path-A scope

New TestNatSubtractionRuntimeGuard520 in tests/test_codegen.py (6 tests):

underflow traps at runtime
safe subtraction returns correct result
structural WAT assertions (guard present for @Nat - @Nat, absent for @Int - @Int and pure-literal 0 - 1)
deep-recursion path-discharged site runs without spurious traps

New tests/conformance/ch04_nat_subtraction.vera demonstrating canonical discharge patterns. Verifies at Tier 1 with 17 contracts; runs to produce 7. Conformance corpus 81 → 82.

Tier-count assertions updated where the new obligations land: test_recursive_call_decreases_verified and test_mixed_tiers (3 → 4 T1), test_overall_tier_counts aggregate (219/26/245 → 222/26/248), test_mutual_recursion_example_all_t1 (8 → 10 T1).

New error code

E502 — @Nat subtraction underflow obligation not discharged. Counterexample-bearing diagnostic with rationale, fix suggestion, and spec ref to §4.4 + §11.2.1.

Documentation

KNOWN_ISSUES.md — Nat subtraction silently underflows to negative i64 — refinement-type soundness hole #520 row removed (this PR closes it); Generalize @Nat invariant check to all binding sites (broader generalisation of #520) #552 limitation entry retains its "generalisation of Nat subtraction silently underflows to negative i64 — refinement-type soundness hole #520" cross-reference.
ROADMAP.md — campaign tracker bumped from "nine remain" to "eight remain"; priority table reordered: Pre-existing bugs in WASM call translators (surfaced by #474 review) #475 takes row 1, @Byte subtraction silent underflow (follow-up to #520) #551 moves to row 2 with a "now mechanical" note explaining the verifier helper + codegen guard from Nat subtraction silently underflows to negative i64 — refinement-type soundness hole #520 generalise directly.
SKILL.md — three stale "Known Bugs" rows swept (GC collect itself faults with out-of-bounds memory access under sustained allocation pressure #515 closed v0.0.122, Runtime traps need Vera-native diagnostics, not raw wasmtime stack traces #516 Stages 2-3 closed v0.0.124-125, Tail-call optimization missing: deep recursion blows the WASM call stack #517 closed v0.0.126 — replaced with GC-aware tail-call optimization for allocating functions #549 documenting the TCO-on-allocating-functions residual). Diagnostic concluding paragraph rewritten to reflect the now-shipped reality of trap-classification + Fix paragraph + source backtrace.
HISTORY.md — terse v0.0.127 row per the hardened single-link single-clause template.
CHANGELOG.md — full release notes under [0.0.127].

Test plan

Co-Authored-By: Claude noreply@anthropic.invalid

Summary by CodeRabbit

Bug Fixes
- Fixed @nat subtraction underflow soundness: failing sites now trap at runtime when verification is absent
New Features
- Tiered verifier obligations for @nat subtraction so verified sites avoid runtime traps; functions can be reclassified via preconditions
Documentation
- Updated spec, roadmap, changelog and project metadata for v0.0.127; introduced diagnostic E502; conformance suite now 82 programs
Tests
- Added verifier and codegen tests covering Nat-subtraction obligations and guarded runtime behaviour

… (refs #520) Two follow-up issues filed during design discussion for #520: - #551 — `@Byte - @Byte` has the same underflow shape as `@Nat - @Nat`. Mechanical follow-up once the verifier helper and codegen guard from #520 are reusable. Joins #520 in row 1 of the bug-killing campaign as a paired cluster (mirroring #487+#348 and #346+#347+#490 elsewhere in the table). - #552 — `@Nat` invariant check fires only at function return position. Narrowing from `@Int` into a `@Nat`-typed let binding or function argument is not obligation-checked. #520 closes the subtraction subset of this hole; #552 is the architectural generalisation. Filed in the Verification depth table (alongside Tier 2 and effect handler lifting) and as a Limitation in KNOWN_ISSUES.md, deliberately scoped *not* to block #520 — ships separately after #520 + #551 so the obligation infrastructure is reusable. Limitation tracker stays consistent (33 in KNOWN_ISSUES.md). Co-Authored-By: Claude <noreply@anthropic.invalid>

@byte

Three spec edits, ahead of the implementation, naming what the verifier will check and what the codegen will emit: - spec/04-expressions.md §4.4 — short clause mirroring the existing divide-by-zero language: "Subtraction on unsigned types is undefined behaviour when it would underflow. The compiler SHOULD verify lhs >= rhs. If it cannot, it MUST insert a runtime check." - spec/11-compilation.md §11.2.1 — full treatment. Names the proof obligation, the Tier-3 fallback codegen (guarded sub trapping with WasmTrapError(kind="underflow")), the lift-back path via `requires`, and references #551 (@byte) and #552 (binding-site generalisation). - spec/11-compilation.md §11.3.3 — footnote on the operator table pointing back to §11.2.1, so readers of the canonical "what does each operator compile to" reference learn that @nat - @nat is conditionally guarded. Allowlist line shift in scripts/check_spec_examples.py (130 -> 132) is a mechanical consequence of the §4.4 insertion; no duplicate keys. The spec is now honest about what §11.2.1 has long claimed ("the non-negativity invariant of Nat is enforced by the contract system") — naming the one operation that breaks the promise and how the compiler will close the gap. Co-Authored-By: Claude <noreply@anthropic.invalid>

@nat

Closes the verifier half of #520; the codegen runtime guard for unverifiable sites lands in the next commit. vera/verifier.py - _walk_for_subtraction_obligations: walks the function body and emits an `lhs >= rhs` proof obligation at every BinaryExpr.SUB whose result is statically @Nat-typed. Mirrors _walk_for_calls structurally — descends through IfExpr (push/pop on smt._path_conditions for then/else), MatchExpr (per-arm pattern conditions), Block (let-bindings update slot_env), BinaryExpr, UnaryExpr, FnCall args. - _check_subtraction_obligation: refutation check via smt.check_valid; counts Tier-1 verified or Tier-3 fallback (timeout/untranslatable), and emits E502 with counterexample on violated. - _report_underflow: E502 diagnostic with rationale, fix suggestion (`requires(@Nat.0 >= @Nat.1)` or guarded if-branch), and spec ref to §4.4 + §11.2.1. - _is_nat_typed: conservative static-type helper. Returns True for SlotRef of type @nat, non-negative IntLits, arithmetic expressions where both operands are @nat (per vera/checker/expressions.py:264-267 Nat <: Int subtyping rule), IfExpr/MatchExpr where every branch is @nat, FnCall returning @nat. False elsewhere. - _has_nat_origin: stricter helper requiring at least one operand to derive from a definitely-@nat source (slot ref or function return) — distinguishes `@Nat.0 - 1` (real subtraction on flowed Nat value) from `0 - 1` (the common "I want -1 as a literal" idiom widely used in `Err(_) -> 0 - 1` and `throw(0 - 1)` positions). Pure-literal underflow into a @nat binding is Path B / #552 territory. - Wired into _verify_fn at step 5.5 (after body translation, before call-violation drainage). vera/errors.py - E502: "@nat subtraction underflow obligation not discharged" in the E5xx verification cluster, adjacent to E500 (postcondition verified false) and E501 (call-site precondition violation). tests/test_verifier.py - TestNatSubtractionObligation520 — 9 test cases covering: * requires-clause discharge * if-guard / path-condition discharge (canonical recursion shape) * trivial discharges (subtract 0, self-subtract) * unguarded subtract failure (counterexample required) * Int-Int and Nat-Int -> Int exclusions (no obligation) * partial-requires non-discharge * pure-literal exclusion documenting Path-A scope - Updated tier counts where the new obligations land: * test_recursive_call_decreases_verified: 3 -> 4 T1 (factorial's @Nat.0 - 1 discharges via path condition) * test_mixed_tiers: 3 -> 4 (sum_to-shape function) * test_overall_tier_counts: 219/26/245 -> 222/26/248 aggregate (factorial.vera +1, mutual_recursion.vera +2) * test_mutual_recursion_example_all_t1: 8 -> 10 T1 Doc and site-asset updates (auto-regenerated): - TESTING.md test count 3618 -> 3627; test_verifier.py row updated from 135/1896 to 144/2061 with #520 narrative entry - ROADMAP.md test count 3618 -> 3627 - docs/llms-full.txt and docs/sitemap.xml regenerated to match Verification: - 144 verifier tests pass; 3514 full pytest suite pass; mypy clean - All 81 conformance programs pass; all 33 examples pass - Zero corpus migration needed: every existing @nat-nat site is guarded by `if @Nat.0 == 0 then base else recursive(@Nat.0 - 1)` and Z3 discharges from the path condition Co-Authored-By: Claude <noreply@anthropic.invalid>

@nat

Closes the codegen half of #520; with the verifier obligation from b446cac, both static and runtime sides of the soundness hole are now closed. Programs that run `vera verify` get a Tier-1 counterexample diagnostic; programs that skip verification trap cleanly via the runtime guard rather than silently producing a negative @nat value. vera/wasm/operators.py - _is_nat_subtraction: detects sites the guard must fire on. Mirrors the verifier's `_is_nat_typed AND _has_nat_origin` exactly so both layers agree on what counts as a guarded site. - _is_static_nat_typed / _has_nat_origin_codegen: AST-level helpers (no SmtContext required) recursing through SlotRef, IntLit, BinaryExpr, IfExpr, Block, MatchExpr, FnCall. Static type follows the checker's Nat <: Int subtyping rule (vera/checker/expressions.py:264-267); provenance distinguishes real @Nat-flowed values from pure-literal idioms. - _emit_nat_sub_guard: emits the WAT guard sequence using two fresh i64 locals (`alloc_local("i64")` for lhs/rhs). Pattern: `local.set $rhs; local.tee $lhs; local.get $rhs; i64.lt_s; if; unreachable; end; local.get $lhs; local.get $rhs; i64.sub`. - Wired into _translate_binary's BinOp.SUB path: when the helper matches, emit the guarded sequence; otherwise the bare `i64.sub` as before. The guard traps via bare `unreachable`, classified by vera/codegen/api.py:_classify_trap as `kind="unreachable"`. A dedicated `kind="underflow"` requires new host-import scaffolding mirroring `vera.contract_fail` and is left as a follow-up enhancement. Users who want a precise diagnostic should run `vera verify` first; the guard's role is preventing silent corruption, not perfect runtime diagnostics. tests/test_codegen.py — TestNatSubtractionRuntimeGuard520 - 6 tests: underflow traps at runtime, safe subtraction returns correct result, structural WAT assertions for @nat-nat (guard present) and @int-int / pure-literal (guard absent), deep recursion (path-discharged site) runs without spurious traps. - Test fixtures use `@Nat.1 - @Nat.0` (first - second) rather than `@Nat.0 - @Nat.1` so call-site `unsafe(0, 1)` reads naturally despite De Bruijn ordering — `@T.0` is the most recent (last) binding. tests/conformance/ch04_nat_subtraction.vera (new — Section 4.4 / 11.2.1) - Demonstrates the canonical discharge patterns: * Explicit `requires(@Nat.0 >= @Nat.1)`. * `if`-guarded recursion (path-condition discharge — the canonical `if @Nat.0 == 0 then base else recursive(@Nat.0 - 1)` shape used throughout examples and conformance). * Trivial discharges (`@Nat.0 - 0`, `@Nat.0 - @Nat.0`). * `@Nat - @int -> @Int` exclusion documenting the type-rule promotion that opts out of the obligation. - 17 contracts verify at Tier 1; runs to produce 7. - Manifest entry at level=run with feature tags nat_subtraction / underflow_obligation / tier1_discharge / path_condition_discharge / trivial_discharge. - Conformance corpus is now 82 programs (was 81). Doc count synchronisation: - TESTING.md: 3,627 -> 3,638 tests; 81 -> 82 conformance (4 occurrences); test_codegen.py 990 -> 996 / 13,705 -> 13,933 lines; test_conformance.py 405 -> 410; run-level 71 -> 72. - ROADMAP.md, CLAUDE.md, SKILL.md, AGENTS.md, FAQ.md: 81 -> 82 conformance. CHANGELOG.md - [Unreleased] entry under ### Fixed naming the soundness hole, the two-sided fix (verifier obligation + codegen guard), the Path-A scope choice (pure-literal exclusion), and the #551 / #552 follow-up trackers. Includes the migration note that zero corpus updates were required because every existing @nat-nat site is path-discharged. Verification: - 3525 tests pass; mypy clean; all 82 conformance + 33 examples pass. The codegen guard agrees with the verifier on which sites count as @nat-nat subtraction; both layers exclude pure-literal idioms (Path B / #552 territory). Co-Authored-By: Claude <noreply@anthropic.invalid>

@nat

Cuts the v0.0.127 release covering #520 (the @nat subtraction soundness hole) and clears six stale references to bugs that shipped in earlier releases — #515 (closed v0.0.122), #516 Stages 2-3 (closed v0.0.124-125), and #517 (closed v0.0.126). The campaign tracker in ROADMAP.md now reflects the post-#520 state: eight bugs remain (was nine), with the priority table reordered so #475 takes row 1 and #551 (the @byte sibling of #520) takes row 2 as a now-mechanical follow-up. Version files (4-file sync via scripts/check_version_sync.py): - vera/__init__.py: 0.0.126 -> 0.0.127 - pyproject.toml: 0.0.126 -> 0.0.127 - README.md: project-status line + release / test counts - docs/index.html: header version badge CHANGELOG.md - Insert [0.0.127] - 2026-04-29 header above the existing Unreleased content (which becomes the v0.0.127 entry). - Add [0.0.127] link reference; bump [Unreleased] base to v0.0.127. HISTORY.md - One-line v0.0.127 row under the Stage 9 release table: "**`@Nat` subtraction soundness hole closed** ([#520]())." Single bolded outcome clause, single link, no em-dashes — per the hardened HISTORY-row discipline (detail belongs in CHANGELOG). KNOWN_ISSUES.md - Remove the #520 row from the Bugs table (closed by this PR). The #552 limitation row keeps its "generalisation of #520 (which fixes the subtraction-specific subset)" cross-reference so triagers can see why #552 exists as a separate ticket without re-reading the soundness story. Limitation count drops 33 -> 32. ROADMAP.md - "Where we are" intro: v0.0.126 -> v0.0.127. - Campaign tracker paragraph: append v0.0.127 closing #520, drop count from "nine remain" to "eight remain", remove #520 from the inline list and from the #520+#551 cluster note. - Priority table: row 1 was #520+#551 cluster (soundness), now becomes #475 (translator bugs); #551 moves to row 2 with a "now mechanical" note explaining that the verifier helper + codegen guard from #520 generalise directly. - "By the numbers" footer: 126 releases (as of v0.0.126) -> 127 releases (as of v0.0.127). SKILL.md (Known Bugs and Workarounds table) - Drop #515 row: $gc_collect bounds-checking shipped v0.0.122, no longer a current bug. - Drop #516 Stages 2-3 row: source backtrace shipped v0.0.124, per-kind Fix paragraphs shipped v0.0.125. Both stages closed. - Drop #517 "no tail-call optimization" row: v0.0.126 shipped TCO for non-allocating functions. Replace with #549 row documenting the residual ("TCO disabled for allocating functions") so agents know the remaining failure mode and the workaround (allocate outside the recursion or iterate via array_fold). - Update the diagnostic concluding paragraph: drop the #515 / #517 / #516-Stages-2-3 trap-shape pointers, add #549 for the allocating-tail-recursion case. Reframe "trap message tells you the what but not the where" as the now-shipped reality: every trap carries kind + Fix paragraph + source backtrace. Site-asset regeneration: - docs/SKILL.md, docs/index.md, docs/llms-full.txt, docs/llms.txt rebuilt automatically by the site-assets pre-commit hook to pick up the SKILL.md content drift. Verification: - All four pre-commit gates green: version sync (0.0.127 across 4 files), doc counts (3638 tests / 29 files / 82 conformance / 33 examples / 25 hooks / 7 CI jobs), limitation sync (32 KNOWN_ISSUES / 15 vera/README / 2 spec chapters), mypy. Co-Authored-By: Claude <noreply@anthropic.invalid>

codecov · 2026-04-29T09:18:43Z

Codecov Report

❌ Patch coverage is 72.64151% with 58 lines in your changes missing coverage. Please review.
✅ Project coverage is 90.92%. Comparing base (8e97a1f) to head (1a2c084).
⚠️ Report is 11 commits behind head on main.

Files with missing lines	Patch %	Lines
vera/verifier.py	77.41%	35 Missing ⚠️
vera/wasm/operators.py	58.18%	23 Missing ⚠️

Additional details and impacted files

@@            Coverage Diff             @@
##             main     #554      +/-   ##
==========================================
- Coverage   91.06%   90.92%   -0.14%     
==========================================
  Files          59       59              
  Lines       22178    22388     +210     
  Branches      259      259              
==========================================
+ Hits        20196    20356     +160     
- Misses       1975     2025      +50     
  Partials        7        7

Flag	Coverage Δ
javascript	`56.83% <ø> (ø)`
python	`94.79% <72.64%> (-0.20%)`	⬇️

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

☔ View full report in Codecov by Sentry.
📢 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.

coderabbitai · 2026-04-29T09:19:01Z

Note

Reviews paused

It looks like this branch is under active development. To avoid overwhelming you with review comments due to an influx of new commits, CodeRabbit has automatically paused this review. You can configure this behavior by changing the reviews.auto_review.auto_pause_after_reviewed_commits setting.

Use the following commands to manage reviews:

@coderabbitai resume to resume automatic reviews.
@coderabbitai review to trigger a single review.

Use the checkboxes below for quick actions:

▶️ Resume reviews
🔍 Trigger review

📝 Walkthrough

Walkthrough

Implements fix for issue #520 by adding Tier‑1 SMT obligations (lhs >= rhs) for @Nat - @Nat`` in the verifier, emitting Tier‑3 guarded runtime traps in codegen on obligation failure, adding tests, spec and docs updates, a new E502 diagnostic and a version bump to v0.0.127. (≈34 words)

Changes

Cohort / File(s)	Summary
Version Metadata `pyproject.toml`, `vera/__init__.py`	Bump package version `0.0.126` → `0.0.127`.
Verifier: Obligation Detection & Discharge `vera/verifier.py`	Add traversal to locate `@Nat -` @Nat`` sites, build `lhs >= rhs` SMT obligations using caller preconditions + active path conditions, update tier accounting, and emit `E502` with counterexample on failure.
Codegen: Runtime Guard Emission `vera/wasm/operators.py`	Emit guarded WAT for `@Nat` subtraction (compare `lhs < rhs` → `unreachable` then `i64.sub`) when provenance/typing criteria match; add helpers for nat-typing and provenance checks and generate guard sequence.
Diagnostics `vera/errors.py`	Add error code `E502` for undischarged `@Nat` subtraction underflow obligations.
Specification `spec/04-expressions.md`, `spec/11-compilation.md`	Document `@Nat` subtraction underflow semantics: verifier obligation `lhs >= rhs` and codegen guard fallback; note `@Byte` tracked separately.
Tests: Verifier & Codegen `tests/test_verifier.py`, `tests/test_codegen.py`	Add verifier and codegen regression tests for `@Nat -` @Nat`` obligations, WAT guard emission and runtime trapping; update tier accounting expectations.
Conformance & Scripts `tests/conformance/manifest.json`, `scripts/check_spec_examples.py`	Add conformance manifest entry for NAT subtraction obligation; adjust spec example allowlist line number.
Docs & Metadata `README.md`, `AGENTS.md`, `CLAUDE.md`, `FAQ.md`, `ROADMAP.md`, `SKILL.md`, `TESTING.md`, `HISTORY.md`, `KNOWN_ISSUES.md`, `CHANGELOG.md`	Update version, test/conformance counts (`81` → `82`), record v0.0.127 release, move `#520` to resolved/limitations and add roadmap/backlog items for `@Byte` and invariant generalisation.
Large edits (tests & verifier/codegen) `vera/verifier.py`, `vera/wasm/operators.py`, `tests/test_codegen.py`, `tests/test_verifier.py`	Concentrated new logic and tests; review focus: SMT obligation formation, path-condition handling, provenance checks, WAT guard correctness and test assertions.

Sequence Diagram(s)

sequenceDiagram
    participant Verifier as Verifier
    participant PathCond as PathConditions
    participant SMT as SMT Solver (Z3)
    participant Codegen as Codegen/WASM

    Note over Verifier: Encounter `@Nat - `@Nat`` expression
    Verifier->>PathCond: Read active path conditions (if/match, requires)
    PathCond-->>Verifier: Return path constraints
    Verifier->>SMT: check_valid(lhs >= rhs, caller_preconds + path_constraints)
    alt Obligation discharged (Tier‑1)
        SMT-->>Verifier: Valid
        Verifier->>Verifier: Increment tier1_verified
        Verifier->>Codegen: Emit direct i64.sub
    else Obligation fails
        SMT-->>Verifier: Counterexample
        Verifier->>Verifier: Emit E502 diagnostic
        Verifier->>Codegen: Emit guarded subtraction
        Codegen->>Codegen: WAT: (if (i64.lt_s lhs rhs) (then unreachable)) i64.sub
    end

Estimated code review effort

🎯 4 (Complex) | ⏱️ ~50 minutes

Possibly related issues

@Byte subtraction silent underflow (follow-up to #520) #551 — Adds analogous verifier obligations and codegen guards for @Byte - @Byte``; closely related by pattern and scope.
Generic functions bypass E502 underflow obligation (follow-up to #520) #555 — Notes verifier early-return for forall<T> generics that can skip the new E502 check; relevant to generic-function verification gaps introduced by this PR.

Possibly related PRs

fix: SMT translator String/Float64 param sorts + string predicates (v0.0.111) #456 — Modifies verifier SMT/type handling (_verify_fn) similar to this PR’s verifier changes.

Suggested labels

compiler, tests, spec, ci, docs

🚥 Pre-merge checks | ✅ 5

✅ Passed checks (5 passed)

Check name	Status	Explanation
Description Check	✅ Passed	Check skipped - CodeRabbit’s high-level summary is enabled.
Title check	✅ Passed	Title accurately summarises the PR's primary objective: closing issue `#520` by preventing `@Nat` subtraction underflow via a soundness fix in release v0.0.127.
Linked Issues check	✅ Passed	All key objectives from `#520` are implemented: verifier emits Tier-1 obligation lhs >= rhs with E502 error on failure; codegen/runtime emits guarded WAT that traps on underflow; pure-literal exemption via provenance; spec, tests, diagnostics, and conformance updated.
Out of Scope Changes check	✅ Passed	All changes are directly scoped to `#520`: verifier pass, codegen guard, error code, spec sections, test suites, documentation updates, and conformance corpus. No unrelated modifications detected.
Docstring Coverage	✅ Passed	Docstring coverage is 91.89% which is sufficient. The required threshold is 80.00%.

_{✏️ Tip: You can configure your own custom pre-merge checks in the settings.}

✨ Finishing Touches

🧪 Generate unit tests (beta)

Create PR with unit tests
Commit unit tests in branch claude/fix-520-nat-underflow

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

coderabbitai

Actionable comments posted: 12

🤖 Prompt for all review comments with AI agents

Verify each finding against the current code and only fix it if needed.

Inline comments:
In `@CLAUDE.md`:
- Line 77: The doc shows inconsistent example counts: update the project-layout
entry that currently reads "32 examples" to the correct count matching the
conformance line "`tests/conformance/` — 82 conformance programs" (i.e., change
"32" → "82") so both entries agree; locate the string "32 examples" (or the
"project-layout" bullet near it) in CLAUDE.md and edit the numeric count, then
re-run any doc checks to confirm the Markdown now matches the repo validation
scripts.

In `@HISTORY.md`:
- Line 264: The HISTORY.md update added the v0.0.127 release row but left the
summary footer roll-up unchanged; update the footer count that currently reads
"126 tagged releases" to "127 tagged releases" so the release total matches the
new v0.0.127 entry (verify the footer text near the file bottom and the new
release line "v0.0.127" are consistent).

In `@KNOWN_ISSUES.md`:
- Line 23: Update the KNOWN_ISSUES.md entry to avoid claiming a general "Tier-3
fallback" exists: change the wording to state that only the subtraction-specific
runtime guard implemented in vera/wasm/operators.py (the `#520` pattern) is
currently present, while broader let/argument `@Int-`>@Nat narrowing remains
unimplemented and tracked as future work in vera/verifier.py (issue `#552`);
ensure the text clearly ties the runtime protection to operators.py and not to a
project-wide Tier-3 fallback.

In `@ROADMAP.md`:
- Line 25: The ROADMAP wording overstates the fix by implying every `@Nat -
`@Nat`` subtraction is guarded; update the sentence to clarify the
verifier/runtime change only applies to subtractions where operands carry Nat
provenance (i.e., non-pure-literal cases), and that the verifier now emits a
Tier-1 `lhs >= rhs` proof obligation and the codegen emits a runtime guard only
for those provenance-bearing `@Nat - `@Nat`` sites (pure literals like `0 - 1`
without Nat provenance are exempt).

In `@SKILL.md`:
- Around line 2294-2298: Remove the misleading "recurse over an `@Int`
accumulator" workaround from the stack-exhaustion guidance and replace it with
the canonical remediation: recommend using array_fold / array_map (which compile
to WASM loops), splitting large recursion into bounded chunks of <5K frames, or
waiting for the GC-aware return_call fix (issue `#517` / `#549`); update the
sentence that currently reads "recurse over an `@Int` accumulator" to list only
those three remedies and ensure references to `array_fold`, `array_map`, and
`return_call` remain for clarity.

In `@spec/04-expressions.md`:
- Line 50: The spec currently requires underflow checks for both Nat and Byte
but the implementation in vera/verifier.py and vera/wasm/operators.py only
enforces Nat subtraction checks; update the spec text in spec/04-expressions.md
(the sentence about subtraction on unsigned types) to scope the MUST/SHOULD
requirement to Nat only (remove Byte) or alternatively note that Byte underflow
is not currently checked by the verifier, aligning the normative language with
the implementation; reference the Nat-specific behavior already present in
vera/verifier.py and vera/wasm/operators.py so readers know which type is
covered.

In `@spec/11-compilation.md`:
- Around line 46-55: Update the spec text for Nat-subtraction checks to match
implementation: change the statement that obligations are emitted at “every
`@Nat - `@Nat`` site” to explicitly note that the compiler omits obligations for
pure literal operands and only emits them when the result has Nat provenance
(i.e., non-literal or derived Nat slots), and replace the runtime trap
annotation `kind="underflow"` with `kind="unreachable"` to reflect the current
classification; keep the rest of the paragraph about guarded subtraction and the
note about `@Byte`/return checks intact.

In `@TESTING.md`:
- Line 9: The Tests summary row in TESTING.md is inconsistent: the table
currently reads "| **Tests** | 3,638 across 29 files (~34,500 lines of test
code; 3,613 passed, 14 skipped) |" but 3,613 + 14 = 3,627; update the table row
so the total and breakdown reconcile (either change the total from 3,638 to
3,627 or adjust the passed/skipped numbers to match 3,638). Edit the "|
**Tests** | ..." line accordingly to ensure the parenthetical breakdown sums to
the reported total.

In `@tests/test_codegen.py`:
- Around line 13902-13933: Add an explicit structural check that the generated
lowering for countdown still includes the runtime guard for the subtraction
rather than just relying on _run passing: after invoking the codegen for
test_recursion_with_path_guard_runs_clean (or by inspecting the lowered WAT for
the function named countdown produced by the same pipeline used by _run), assert
that the countdown body contains the guarded subtraction pattern (e.g., the
emitted lhs>=rhs or the specific guard instruction sequence your backend emits)
so the test fails if the guard is accidentally removed while the runtime
behavior remains 0.

In `@tests/test_verifier.py`:
- Around line 553-566: Update the class docstring for
TestNatSubtractionObligation520 to match the test behavior by adding the
provenance/literal exception: state that `@Nat - `@Nat`` sites generally require
proof of `lhs >= rhs` but exempt pure-literal (provenance) subtraction cases
(for example `0 - 1`) which the verifier treats specially; ensure the updated
text references the class name TestNatSubtractionObligation520 and the `lhs >=
rhs` obligation so readers can find the related tests and logic.

In `@vera/verifier.py`:
- Around line 871-1200: The walker and Nat classifiers currently only handle
ast.FnCall and thus miss module-qualified calls; update
_walk_for_subtraction_obligations to also descend into the module-qualified call
node (treat its args and return like ast.FnCall), and update _is_nat_typed and
_has_nat_origin to recognise module-qualified calls by resolving the callee with
the existing _lookup_module_function (or similar module-function resolver) and
then using _is_nat_type(fn.return_type) / _is_nat_type on the resolved function
return type (and _is_nat_origin logic for its provenance). Ensure you reference
and reuse the same resolution path used elsewhere (the _lookup_module_function
helper) so cross-module calls produce the same Nat typing/origin behaviour as
plain FnCall.

In `@vera/wasm/operators.py`:
- Around line 728-832: The helpers miss imported module function calls because
they only handle ast.FnCall; update _is_static_nat_typed and
_has_nat_origin_codegen (which feed _is_nat_subtraction) to also recognise and
treat imported/callable expressions that represent cross-module function calls
(e.g. qualified/imported calls where the AST node isn't ast.FnCall but has a
callee/qualified name) by invoking _infer_fncall_vera_type for those call-like
nodes (or by extracting the callee and calling the existing
_infer_fncall_vera_type) and returning True when that returns "Nat" so imported
`@Nat` functions are treated the same as ast.FnCall for both static-typing and
provenance checks.

🪄 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: 0dd29930-8ea7-45f9-a958-5b1d1b1cd558

📥 Commits

Reviewing files that changed from the base of the PR and between 8e97a1f and 9def35a.

⛔ Files ignored due to path filters (7)

docs/SKILL.md is excluded by !docs/**
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/**
docs/sitemap.xml is excluded by !docs/**
tests/conformance/ch04_nat_subtraction.vera is excluded by !**/*.vera

📒 Files selected for processing (21)

AGENTS.md
CHANGELOG.md
CLAUDE.md
FAQ.md
HISTORY.md
KNOWN_ISSUES.md
README.md
ROADMAP.md
SKILL.md
TESTING.md
pyproject.toml
scripts/check_spec_examples.py
spec/04-expressions.md
spec/11-compilation.md
tests/conformance/manifest.json
tests/test_codegen.py
tests/test_verifier.py
vera/__init__.py
vera/errors.py
vera/verifier.py
vera/wasm/operators.py

@nat

Eleven Rabbit findings actioned plus one CI failure unblocked. Each finding was verified against the current code; small refinements where the underlying point was real but the suggested wording was imprecise. CI fix - uv.lock regenerated. v0.0.127 bump in pyproject.toml left the lockfile pinned at 0.0.126; lint job ran `uv lock --check` and failed. `uv lock` produces a one-line update (vera 0.0.126 -> 0.0.127); no transitive dependency churn. Documentation accuracy - CLAUDE.md project-layout: "32 example Vera programs" -> "33". (Rabbit suggested 32 -> 82, conflating examples with conformance; the actual stale figure was 32 vs the live 33.) - HISTORY.md "By the numbers" table: rightmost column updated from v0.0.126 (28 Apr) to v0.0.127 (29 Apr) with the new metrics (3,638 tests, 82 conformance, 33 examples). Total releases 126 -> 127; active development days 48 -> 49. - KNOWN_ISSUES.md #552 entry: rephrased to drop the misleading "Tier-3 fallback compiles correctly" claim. There is no general Tier-3 fallback — only #520's subtraction-specific guard in vera/wasm/operators.py. The new wording ties the runtime protection explicitly to the operators.py guard and notes that let / argument narrowing remains unimplemented at both static and runtime layers (issue #552). - ROADMAP.md campaign tracker: clarified that v0.0.127 only guards `@Nat - @Nat` sites with `@Nat` *provenance* (slot ref or function return), not pure-literal idioms like `0 - 1`. Mirrors the Path-A scope choice and points readers at #552 for the binding-site generalisation. - TESTING.md Tests row: pass/skip math reconciled. Total reads 3,638; previous breakdown was 3,613 + 14 = 3,627 (off by 11). Updated to 3,624 + 14 = 3,638. Spec / implementation alignment - spec/04-expressions.md §4.4 underflow clause: scoped the normative MUST/SHOULD to `Nat` only. Previous wording included `Byte`, but the implementation in vera/verifier.py and vera/wasm/operators.py only enforces `Nat`; `Byte` is tracked as #551 (now explicitly named in the spec text). - spec/11-compilation.md §11.2.1: two corrections. (a) Trap kind classification updated `kind="underflow"` -> `kind="unreachable"` to match the actual implementation (the bare `unreachable` instruction is classified as `kind="unreachable"` by vera/codegen/api.py:_classify_trap; a dedicated `underflow` kind requires new host-import scaffolding mirroring `vera.contract_fail` and is left as a future enhancement). (b) "At every such site" softened to "At every such site whose result is statically @nat AND at least one operand has @nat provenance" — pure-literal subtractions like `0 - 1` are intentionally exempt at Path-A scope, so the spec now matches what the verifier and codegen actually do. Verifier and codegen completeness - vera/verifier.py: `_walk_for_subtraction_obligations` now descends into `ast.ModuleCall` args (mirroring its `ast.FnCall` handling) so `@Nat - @Nat` sites inside `Foo.bar(arg)` are not silently skipped. `_is_nat_typed` and `_has_nat_origin` resolve `ast.ModuleCall` callees via the existing `_lookup_module_function` registry and check the resolved `FunctionInfo.return_type` — so a module-qualified call returning `@Nat` is treated identically to an unqualified `ast.FnCall` for both static-typing and provenance purposes. - vera/wasm/operators.py: `_is_static_nat_typed` and `_has_nat_origin_codegen` now handle `ast.ModuleCall` by synthesizing the equivalent `ast.FnCall(name=expr.name, args=expr.args)` and feeding it through the existing `_infer_fncall_vera_type`. Matches the desugar that vera/wasm/context.py:translate_expr already performs at line 315 (ModuleCall -> flat FnCall via flattened import names), so the codegen guard fires on the same set of sites the verifier obligates. Test coverage - tests/test_codegen.py `test_recursion_with_path_guard_runs_clean`: added a structural WAT assertion that the `@Nat.0 - 1` site inside `countdown` actually emits the `i64.lt_s` + `unreachable` guard. Pre-fix the test was coverage-blind: the path condition guarantees `@Nat.0 >= 1` in the recursive arm, so the runtime guard never fires whether or not it's emitted, and the behavioural assertion (`countdown(100) == 0`) would pass even if the codegen detector silently skipped path-discharged sites. - tests/test_verifier.py `TestNatSubtractionObligation520` class docstring: extended to name the provenance-bearing requirement and the pure-literal exemption explicitly, with a cross-reference to `test_pure_literal_subtraction_not_flagged` and the Path-B / #552 binding-site generalisation. SKILL.md "Known Bugs" #549 row workaround text: - Replaced the "@int accumulator" hint with the canonical remediation list: prefer `array_fold` / `array_map` (which compile to WASM loops with no per-iteration frame cost) for most cases; fall back to splitting the recursion into bounded chunks of <5K frames; or wait for the GC-aware `return_call` follow-up tracked by #549. The accumulator hint was misleading because most accumulator shapes carrying heap data are themselves allocating, so they don't actually escape the bug. Verification - 3,525 tests pass; mypy clean; doc-counts / limitations-sync / version-sync / spec-examples all green; all 82 conformance + 33 examples still pass. Co-Authored-By: Claude <noreply@anthropic.invalid>

coderabbitai

Actionable comments posted: 3

Caution

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

⚠️ Outside diff range comments (1)

tests/test_codegen.py (1)
13712-13959: ⚠️ Potential issue | 🟠 Major

Add a ModuleCall-provenance regression for the Nat-underflow guard path.

This suite covers direct @Nat provenance (slot refs/literals) well, but it does not exercise provenance flowing through a module-qualified call. A regression in the ModuleCall path could re-open the soundness hole while these tests remain green. Please add one case that sources a @Nat operand via a qualified call and assert both structural guard emission and runtime behaviour.

As per coding guidelines: tests/test_codegen.py: Add codegen/runtime tests in tests/test_codegen.py for built-in functions — cover normal cases, edge cases (empty inputs, zero values), and composition with other built-ins.
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.

In `@tests/test_codegen.py` around lines 13712 - 13959, Add a new test in the
TestNatSubtractionRuntimeGuard520 class that exercises a ModuleCall provenance:
create a small source that defines a module-scoped helper (e.g. fn m::nat_prov()
-> `@Nat`) or a module-qualified call that returns a `@Nat` and then performs `@Nat
- `@Nat`` where one operand comes from that qualified call; use the same helpers
as the existing tests (_compile_ok, _run, execute) to assert runtime behaviour
(trap on unsafe underflow and correct result on safe case) and a structural WAT
assertion mirroring test_guard_emitted_in_wat_for_nat_sub /
test_recursion_with_path_guard to check the guarded function body contains both
"i64.lt_s" and "unreachable" (and for an Int-like control case assert absence),
naming the new test clearly (e.g.
test_modulecall_provenance_emits_guard_and_traps) and following the established
patterns for slicing the WAT body and asserting presence/absence of the guard.

🤖 Prompt for all review comments with AI agents

Verify each finding against the current code and only fix it if needed.

Inline comments:
In `@TESTING.md`:
- Line 11: Update the prose totals in TESTING.md to match the new conformance
program count: replace the occurrence that still says "81" with "82" (the prose
phrase referencing the collection count, e.g., "a collection of N small, focused
programs") and update the pytest count that currently reads "405 tests" to "410
tests" (the sentence like "Via pytest (parametrized — N tests)") so all ungated
prose reflects 82 programs × 5 tests = 410 tests.

In `@vera/verifier.py`:
- Around line 871-1032: The walker _walk_for_subtraction_obligations misses
ast.ConstructorCall arguments (so subtractions like Just(`@Nat.0` - `@Nat.1`) aren't
recursed); add a branch analogous to the ast.FnCall / ast.ModuleCall cases:
detect isinstance(expr, ast.ConstructorCall) and for each arg call
self._walk_for_subtraction_obligations(decl, arg, smt, slot_env, assumptions) so
those argument expressions are inspected and _check_subtraction_obligation can
catch `@Nat-`@Nat sites.

---

Outside diff comments:
In `@tests/test_codegen.py`:
- Around line 13712-13959: Add a new test in the
TestNatSubtractionRuntimeGuard520 class that exercises a ModuleCall provenance:
create a small source that defines a module-scoped helper (e.g. fn m::nat_prov()
-> `@Nat`) or a module-qualified call that returns a `@Nat` and then performs `@Nat
- `@Nat`` where one operand comes from that qualified call; use the same helpers
as the existing tests (_compile_ok, _run, execute) to assert runtime behaviour
(trap on unsafe underflow and correct result on safe case) and a structural WAT
assertion mirroring test_guard_emitted_in_wat_for_nat_sub /
test_recursion_with_path_guard to check the guarded function body contains both
"i64.lt_s" and "unreachable" (and for an Int-like control case assert absence),
naming the new test clearly (e.g.
test_modulecall_provenance_emits_guard_and_traps) and following the established
patterns for slicing the WAT body and asserting presence/absence of the guard.

🪄 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: e31dbd2c-bde6-476c-8943-f62fb097596c

📥 Commits

Reviewing files that changed from the base of the PR and between 9def35a and 76966cb.

⛔ Files ignored due to path filters (3)

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

📒 Files selected for processing (12)

CLAUDE.md
HISTORY.md
KNOWN_ISSUES.md
ROADMAP.md
SKILL.md
TESTING.md
spec/04-expressions.md
spec/11-compilation.md
tests/test_codegen.py
tests/test_verifier.py
vera/verifier.py
vera/wasm/operators.py

@nat

Two more in-diff findings and one out-of-diff suggestion, all real. vera/verifier.py - _walk_for_subtraction_obligations now recurses into the args of ast.ConstructorCall and ast.QualifiedCall, in addition to the existing ast.FnCall and ast.ModuleCall branches. Previously `Some(@Nat.0 - @Nat.1)` would slip past the obligation walker because the constructor call's children weren't visited; now they are. ConstructorCall results are ADT-typed (not @nat), so _is_nat_typed / _has_nat_origin don't need branches for them. QualifiedCall is similar (e.g. `Map.get(...)`); the SMT layer doesn't translate QualifiedCall itself, so any obligation rooted ON one would already drop to Tier 3, but recursing here catches obligations rooted INSIDE the args. tests/test_codegen.py - New test_modulecall_provenance_emits_guard_and_traps in TestNatSubtractionRuntimeGuard520 (out-of-diff suggestion from Rabbit, real value-add). Exercises the round-1 ModuleCall fix end-to-end: compiles a function using `vera.math::abs(@Int.1) - vera.math::abs(@Int.0)` (a @nat - @nat site where both operands have @nat provenance via ast.ModuleCall, not ast.FnCall), asserts the codegen emits the i64.lt_s + unreachable guard in the WAT, asserts the runtime traps cleanly when called with arguments that underflow (`unsafe_modcall(0, 5)` → `abs(0) - abs(5)`), and asserts the safe case (`safe_modcall(5, 3)` → `abs(5) - abs(3) = 2`) runs cleanly through the guard. Pinning the De Bruijn ordering in comments since the test relies on `@Int.1` being the first parameter. TESTING.md - Updated two stale prose / code-block totals: "a collection of 81 small, focused programs" → "82" (matches the new conformance count from the v0.0.127 ch04_nat_subtraction.vera entry); "Via pytest (parametrized — 405 tests)" → "410 tests" (matches the 82 programs × 5 tests-per-program = 410 product). - Bumped test_codegen.py row counts (996 → 997, 13,958 → 14,039) and the overall Tests metric (3,638 → 3,639, passed 3,624 → 3,625) for the new test_modulecall_provenance test. ROADMAP.md - 3,638 → 3,639 in the "Where we are" intro paragraph and the By the Numbers footer (kept in sync with TESTING.md / live pytest count). Verification: - 16 #520 tests pass; mypy clean; doc-counts / limitations-sync / version-sync all green. Co-Authored-By: Claude <noreply@anthropic.invalid>

aallan · 2026-04-29T10:12:09Z

@coderabbitai resolve

coderabbitai

Actionable comments posted: 1

Caution

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

⚠️ Outside diff range comments (1)

vera/verifier.py (1)
420-438: ⚠️ Potential issue | 🟠 Major

Do not let the generic-function fast path bypass E502.

Line 420 returns before Line 525 ever runs, so forall<T> functions with an otherwise ordinary @Nat - @nat:@Nat`` site never get the new verifier-side underflow check. An unrelated type parameter is enough to suppress the Tier-1 half of #520, which weakens the verifier-first guarantee to runtime trapping only.
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.

In `@vera/verifier.py` around lines 420 - 438, The current fast path returns when
decl.forall_vars is true, skipping the verifier-side underflow check that emits
E502; change the logic so generic functions still run the underflow verification
for each contract before returning (either by moving the E502-checking code to
run prior to the early return or by invoking the same underflow-check routine
that non-generic functions use). Specifically, in the block that handles
decl.forall_vars and iterates decl.contracts (and uses self._is_trivial /
self._warning), ensure you also call the verifier underflow check that can raise
E502 for `@Nat-like` sites (or reuse the existing function that performs the E502
check) so that generic functions do not bypass E502 while still recording
tier3_runtime where appropriate.

♻️ Duplicate comments (1)

tests/test_codegen.py (1)

13847-13854: ⚠️ Potential issue | 🟡 Minor

Harden the negative controls against comparator swaps.

Both tests only ban i64.lt_s. If the guard regresses to i64.lt_u, or leaves only the trap marker behind, these assertions still pass while the body is still guarded. Assert absence of both the compare and unreachable here.

Suggested hardening

-        assert "i64.lt_s" not in body, (
-            f"Unexpected `i64.lt_s` in int_sub body — Int subtraction "
+        assert not re.search(r"i64\.lt_[su]", body), (
+            f"Unexpected underflow-guard compare in int_sub body — Int subtraction "
             f"should not have an underflow guard. Body: {body!r}"
         )
+        assert "unreachable" not in body, (
+            f"Unexpected `unreachable` in int_sub body — Int subtraction "
+            f"should not trap. Body: {body!r}"
+        )
@@
-        assert "i64.lt_s" not in body, (
-            f"Pure-literal `0 - 1` should not get a guard at Path-A "
+        assert not re.search(r"i64\.lt_[su]", body), (
+            f"Pure-literal `0 - 1` should not get an underflow-guard compare at Path-A "
             f"scope. Body: {body!r}"
         )
+        assert "unreachable" not in body, (
+            f"Pure-literal `0 - 1` should not emit a trap guard at Path-A "
+            f"scope. Body: {body!r}"
+        )

As per coding guidelines: `tests/**/*.py`: These are pytest test files. Review for correctness and coverage gaps.

Also applies to: 13893-13900

🤖 Prompt for AI Agents

Verify each finding against the current code and only fix it if needed.

In `@tests/test_codegen.py` around lines 13847 - 13854, The test currently only
asserts that "i64.lt_s" is not present in the generated body, which misses
regressions that replace it with "i64.lt_u" or leave only a trap marker; update
the assertions in the int_sub negative-control blocks (the ones checking for
absence of underflow guard) to assert that none of "i64.lt_s", "i64.lt_u", nor
the string "unreachable" appear in body (i.e., add checks like assert "i64.lt_u"
not in body and assert "unreachable" not in body alongside the existing i64.lt_s
check) and apply the same three-way absence checks to the other similar block
around the later lines referenced.

🤖 Prompt for all review comments with AI agents

Verify each finding against the current code and only fix it if needed.

Inline comments:
In `@tests/test_codegen.py`:
- Around line 14014-14015: Update the stale comment to match the actual call
order used in main: it evaluates unsafe_modcall(0, 5), so change the explanation
to refer to unsafe_modcall(0, 5) and the resulting computation (abs(5) - abs(0)
= 5 - 0 = 5 / no underflow) instead of the reversed unsafe_modcall(5, 0); ensure
the comment near the test referencing unsafe_modcall and main reflects the
correct argument order.

---

Outside diff comments:
In `@vera/verifier.py`:
- Around line 420-438: The current fast path returns when decl.forall_vars is
true, skipping the verifier-side underflow check that emits E502; change the
logic so generic functions still run the underflow verification for each
contract before returning (either by moving the E502-checking code to run prior
to the early return or by invoking the same underflow-check routine that
non-generic functions use). Specifically, in the block that handles
decl.forall_vars and iterates decl.contracts (and uses self._is_trivial /
self._warning), ensure you also call the verifier underflow check that can raise
E502 for `@Nat-like` sites (or reuse the existing function that performs the E502
check) so that generic functions do not bypass E502 while still recording
tier3_runtime where appropriate.

---

Duplicate comments:
In `@tests/test_codegen.py`:
- Around line 13847-13854: The test currently only asserts that "i64.lt_s" is
not present in the generated body, which misses regressions that replace it with
"i64.lt_u" or leave only a trap marker; update the assertions in the int_sub
negative-control blocks (the ones checking for absence of underflow guard) to
assert that none of "i64.lt_s", "i64.lt_u", nor the string "unreachable" appear
in body (i.e., add checks like assert "i64.lt_u" not in body and assert
"unreachable" not in body alongside the existing i64.lt_s check) and apply the
same three-way absence checks to the other similar block around the later lines
referenced.

🪄 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: 80960775-1d8f-474c-8513-4cdf02b3346b

📥 Commits

Reviewing files that changed from the base of the PR and between 76966cb and fecfb28.

📒 Files selected for processing (4)

ROADMAP.md
TESTING.md
tests/test_codegen.py
vera/verifier.py

coderabbitai · 2026-04-29T10:18:17Z

✅ Actions performed

Comments resolved. Approval is disabled; enable reviews.request_changes_workflow to allow explicit top-level @coderabbitai resolve or @coderabbitai approve commands.

…ertions Single-finding round. CodeRabbit pushed back on the round-2 ModuleCall reply with a concrete strengthening for the two negative control tests: ban both `i64.lt_s` AND `i64.lt_u` (signed and unsigned compare variants) AND assert `unreachable` is absent. The previous `"i64.lt_s" not in body` substring check would have silently passed if the codegen ever switched to unsigned comparison or a different compare-then-trap variant. tests/test_codegen.py - test_int_subtract_emits_no_guard: replaced `assert "i64.lt_s" not in body` with `assert not re.search(r"\bi64\.lt_[su]\b", body)` and added `assert "unreachable" not in body`. - test_pure_literal_subtract_emits_no_guard: same hardening. - Inline comments document why both bans matter together: the comparator could change (signed -> unsigned) without breaking the substring check, and the trap mechanism could change (unreachable -> a host-import call) without breaking the comparator check. Banning both keeps the test future-proof. - `re` is already imported at the top of the file (line 14), so this is drop-in. Verification: - All 7 TestNatSubtractionRuntimeGuard520 tests still pass; the positive cases (`test_underflow_traps_at_runtime`, `test_guard_emitted_in_wat_for_nat_sub`, `test_modulecall_provenance_emits_guard_and_traps`) all still see the expected `i64.lt_s` + `unreachable` guard sequence. Co-Authored-By: Claude <noreply@anthropic.invalid>

coderabbitai

Actionable comments posted: 1

♻️ Duplicate comments (1)

tests/test_codegen.py (1)

14031-14032: ⚠️ Potential issue | 🟡 Minor

Fix the stale call-order comment.

The comment says unsafe_modcall(5, 0), but main actually calls unsafe_modcall(0, 5). In a De Bruijn-sensitive test, that mismatch is easy to cargo-cult.

Minimal fix

-        # Behavioural assertion: unsafe_modcall(5, 0) produces
+        # Behavioural assertion: unsafe_modcall(0, 5) produces

🤖 Prompt for AI Agents

Verify each finding against the current code and only fix it if needed.

In `@tests/test_codegen.py` around lines 14031 - 14032, The comment incorrectly
references unsafe_modcall(5, 0) while main actually calls unsafe_modcall(0, 5);
update the behavioural assertion comment to reflect the real call order
(unsafe_modcall(0, 5)) and correct the expected expression/result (abs(5) -
abs(0) = 5 - 0 = 5, not an underflow/trap). Locate the call site in main and the
comment near the test assertion and revise the text accordingly.

🤖 Prompt for all review comments with AI agents

Verify each finding against the current code and only fix it if needed.

Inline comments:
In `@tests/test_codegen.py`:
- Around line 13712-14056: Add a new test that exercises the rhs-only-provenance
subtraction shape (literal left operand minus a `@Nat` slot) so the codegen helper
`_has_nat_origin_codegen` can't accidentally ignore the right operand; in the
TestNatSubtractionRuntimeGuard520 class add a case similar to `_GUARDED_SUB` /
`test_guard_emitted_in_wat_for_nat_sub` that uses a body like `0 - `@Nat.0`` (or a
wrapper fn that calls a private unsafe fn with that body), then assert the WAT
for that function contains both "i64.lt_s" and "unreachable" and that executing
the program with arguments that cause underflow (e.g. passing 1 where rhs is 1)
raises a trap using the same patterns/assertions as existing tests (reuse
function names such as `unsafe`, `unsafe_modcall` idiom and runtime checks with
pytest.raises and execute/_run).

---

Duplicate comments:
In `@tests/test_codegen.py`:
- Around line 14031-14032: The comment incorrectly references unsafe_modcall(5,
0) while main actually calls unsafe_modcall(0, 5); update the behavioural
assertion comment to reflect the real call order (unsafe_modcall(0, 5)) and
correct the expected expression/result (abs(5) - abs(0) = 5 - 0 = 5, not an
underflow/trap). Locate the call site in main and the comment near the test
assertion and revise the text accordingly.

🪄 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: df4b7843-fb4d-41c5-844f-0d8590160a1c

📥 Commits

Reviewing files that changed from the base of the PR and between fecfb28 and 488deff.

📒 Files selected for processing (2)

TESTING.md
tests/test_codegen.py

…low-up #555 Three findings verified. One real fix (stale comment), one already-addressed duplicate (round 3 already handled it), and one real-but-out-of-scope soundness gap filed as #555 follow-up. tests/test_codegen.py - Stale Python-side comment in test_modulecall_provenance_emits_guard _and_traps fixed: round-2 updated the Vera-side comment in `main` to say `unsafe_modcall(0, 5)` (the corrected De Bruijn-aware call order) but missed the explanatory Python comment immediately above the `pytest.raises` block, which still said `unsafe_modcall(5, 0)`. Updated to match the actual call order and added an inline reminder that `@Int.1` is the first parameter (older / De Bruijn = 1) and `@Int.0` is the second (most-recent) so the test's De Bruijn-sensitive arg-vs-slot mapping reads cleanly. KNOWN_ISSUES.md - New Limitation entry tracking #555: generic (forall<T>) functions bypass the E502 underflow obligation at verify time because the verifier's early return for forall_vars skips _walk_for_subtraction_obligations along with all other static contract checks. Consistent with how E520-E525 all skip generics today; the codegen guard catches it post-monomorphization at runtime so the safety net is in place — only the static check is missing. #555 was filed via gh issue create; the PR's inline reply explains why the fix is non-trivial (SMT context setup needs concrete-typed params; type-variable params can't be declared as Z3 sorts) and why I'm scoping it out of #520 — it inherits the convention used by every other verifier check on generic functions, and the runtime guard at codegen time already provides safety. Round 4 ALSO had a "duplicate" finding asking us to harden test_int_subtract_emits_no_guard and test_pure_literal_subtract _emits_no_guard with `re.search(r"\bi64\.lt_[su]\b", body)` and `assert "unreachable" not in body`. Already addressed in round 3 commit 488deff; the inline reply points at that commit. Verification: - All 7 TestNatSubtractionRuntimeGuard520 tests pass. - Limitation tracking consistent (33 in KNOWN_ISSUES.md / 15 in vera/README.md / 2 across spec chapters). - mypy clean. Co-Authored-By: Claude <noreply@anthropic.invalid>

aallan · 2026-04-29T10:32:19Z

@coderabbitai Verified — this is a real gap, but I'm scoping it as out of #520 because the fix is non-trivial and the codegen guard already catches it at runtime. Filed as #555 for the follow-up.

Two reasons for keeping the static skip in this PR:

The SMT context setup at line 451-490 declares Z3 vars for concrete-typed params (declare_nat, declare_int, declare_bool, etc.) and falls through for unknown types. For forall<T> functions, type-variable parameters can't be declared as Z3 sorts (Z3 has no notion of type variables), so the existing convention bails BEFORE setup. To run _walk_for_subtraction_obligations we'd need to either (a) skip type-variable params and declare only concrete ones (then walk; obligations involving TypeVar operands would fail to translate and silently drop to Tier-3 — inflating Tier-3 counts without catching anything new), or (b) special-case "@Nat-typed slot ref where the slot type is concrete" inside the walker (deeper change to _is_nat_typed / _has_nat_origin).
Generic functions are monomorphized at codegen time, and the codegen guard (_is_static_nat_typed + _has_nat_origin_codegen) fires per-instantiation — so a concrete foo$Int instantiation of a generic fn foo<T>(@Nat -> T) with @Nat.0 - 1 in its body gets the runtime guard at compile time and traps on underflow. The static-check skip is a "best-effort" gap, not a soundness hole — the runtime safety net is in place.

Convention-wise this matches how E520 / E521 / E523 / E524 / E525 all bail out for generic functions today; #520's E502 inherits the same convention. #555 tracks extending E502 (and ideally the others) to generic-function bodies.

aallan · 2026-04-29T10:32:21Z

@coderabbitai Already addressed in round-3 commit 488deff (PR #554 round 3 review fix). Both test_int_subtract_emits_no_guard and test_pure_literal_subtract_emits_no_guard now use re.search(r"\bi64\.lt_[su]\b", body) (banning both signed and unsigned compare variants) AND assert "unreachable" not in body (banning the trap marker). Inline comments document why both bans matter together (comparator could flip without breaking the substring check; trap mechanism could change without breaking the comparator check). All 7 tests in the class still pass with the strengthened assertions.

coderabbitai · 2026-04-29T10:32:54Z

Tip

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

@aallan: Confirmed — the dual-ban pattern (re.search(r"\bi64\.lt_[su]\b", body) + assert "unreachable" not in body) is exactly right. The two checks are orthogonal: a future comparator change could swap lt_s for lt_u while silently defeating a single-variant substring match, and a future trap-mechanism change (e.g. swapping unreachable for a host-import call) could defeat the comparator check alone. Requiring both to be absent makes the negative controls genuinely tight. Good hardening.

✏️ Learnings added

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

Timestamp: 2026-04-29T10:32:53.208Z
Learning: Repo aallan/vera — tests/test_codegen.py (PR `#554`, commit 488deff): Negative-guard tests for `Nat - Nat` underflow absence (e.g. `test_int_subtract_emits_no_guard`, `test_pure_literal_subtract_emits_no_guard`) use a dual-ban pattern: `assert not re.search(r"\bi64\.lt_[su]\b", body)` (banning both signed and unsigned compare variants) AND `assert "unreachable" not in body` (banning the trap marker). The two bans are independent: comparator could flip `lt_s`→`lt_u` without breaking a single-variant check; trap mechanism could change without breaking the comparator check. Both must be independently negated for the negative controls to be sound. Positive guard tests still assert the specific `i64.lt_s` + `unreachable` sequence.

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.

🧠 Learnings used

Learnt from: aallan
Repo: aallan/vera PR: 554
File: tests/test_codegen.py:13850-13853
Timestamp: 2026-04-29T10:11:31.416Z
Learning: Repo aallan/vera — tests/test_codegen.py::TestNatSubtractionRuntimeGuard520 now includes ModuleCall coverage: `vera.math::abs(Int.1) - vera.math::abs(Int.0)` is treated as `Nat - Nat` with Nat provenance via `ast.ModuleCall`, and the WAT underflow guard (`i64.lt_s` + `unreachable`) must be emitted and trap on underflow. This ensures codegen recognizes module‑qualified Nat returns for guard insertion.

Learnt from: aallan
Repo: aallan/vera PR: 554
File: vera/verifier.py:871-1058
Timestamp: 2026-04-29T10:10:47.850Z
Learning: In `vera/verifier.py` `_walk_for_subtraction_obligations` (post-PR `#554`): `ast.ConstructorCall` and `ast.QualifiedCall` must have their `.args` walked even though neither returns `Nat`. `ConstructorCall` (returns ADT) and `QualifiedCall` (e.g. `Map.get`, currently untranslatable in SMT) don't need branches in `_is_nat_typed` or `_has_nat_origin`, but omitting arg-recursion causes `Nat - Nat` obligations nested INSIDE those args (e.g. `Some(Nat.0 - Nat.1)`) to be silently skipped. The fix is a branch per call shape that iterates args and recurses — identical in structure to the `FnCall`/`ModuleCall` branches.

Learnt from: aallan
Repo: aallan/vera PR: 554
File: spec/11-compilation.md:0-0
Timestamp: 2026-04-29T09:53:58.860Z
Learning: In `vera/codegen/api.py` `_classify_trap` (post-PR `#554`): the `Nat - Nat` underflow guard emits a bare WASM `unreachable` instruction, which `_classify_trap` classifies as `kind="unreachable"`, NOT `kind="underflow"`. A dedicated `underflow` kind would require new host-import scaffolding mirroring `vera.contract_fail` and is deferred as a future enhancement (tracked with the `kind="underflow"` follow-up alongside `#551/`#552). Do NOT flag the spec or codegen as incorrect for using `kind="unreachable"` here.

Learnt from: aallan
Repo: aallan/vera PR: 511
File: tests/test_browser.py:1272-1379
Timestamp: 2026-04-23T13:38:11.484Z
Learning: Repo aallan/vera: When a test in tests/test_browser.py or tests/test_codegen.py needs to verify that json_as_int returns Some(INT64_MIN) for the input -2^63 (i.e. JNumber(0.0 - 9223372036854775808.0)), do NOT call int_to_string(Int.0) directly — there is a pre-existing bug (`#475`, queued for v0.0.120) where int_to_string(INT64_MIN) triggers a negation overflow inside the WAT code. The correct workaround is to probe the value indirectly, e.g. via `bool_to_string(Int.0 < 0)`, and assert the result is "true". Add an inline test-body comment documenting the `#475` bug to prevent future reviewers from replacing the workaround with a direct print.

Learnt from: aallan
Repo: aallan/vera PR: 511
File: tests/test_codegen.py:12473-12510
Timestamp: 2026-04-23T13:51:17.615Z
Learning: Repo aallan/vera — tests/test_codegen.py and tests/test_browser.py: When verifying json_as_int at -2^63 (JNumber(-9223372036854775808.0)), use two indirect probes to avoid the known int_to_string(INT64_MIN) negation-overflow bug (`#475`): (a) assert bool_to_string(Int.0 < 0) == "true"; and (b) assert int_to_string(Int.0 + 1) == "-9223372036854775807". Include an inline "#475" comment. Implemented in commit 3cf5a13 (PR `#511`).

Learnt from: aallan
Repo: aallan/vera PR: 550
File: tests/test_codegen.py:1930-2111
Timestamp: 2026-04-28T19:28:33.529Z
Learning: Repo aallan/vera — tests/test_codegen.py (PR `#550`): Tail-position analyzer coverage now includes explicit negative unit tests asserting compute_tail_call_sites does NOT mark calls in non-transparent positions:
- test_analyzer_does_not_mark_call_in_block_statement (ExprStmt.expr in a Block),
- test_analyzer_does_not_mark_call_in_if_condition (IfExpr.condition),
- test_analyzer_does_not_mark_call_in_match_scrutinee (MatchExpr.scrutinee).
These complement existing positives (Block trailing expr, If branches, Match arm bodies) and prior negatives (LetStmt.value, FnCall.args), making the analyzer’s transparent vs non-transparent rules pairwise complete.

Learnt from: aallan
Repo: aallan/vera PR: 0
File: :0-0
Timestamp: 2026-03-29T17:17:11.974Z
Learning: In `tests/test_codegen.py`, `test_option_unwrap_or_map` (lines ~9936–9949) and `test_option_unwrap_or_set` (lines ~9950–9963) are regular, unconditionally-passing tests with NO `xfail`, `skip`, or `skipif` marks. `grep -rn "xfail" tests/` returns zero results across the entire test suite. The PR `#428` fix resolved the underlying monomorphiser inference gap for opaque i32 handle types (Map, Set) in `option_unwrap_or` generics. Do NOT flag these tests as xfail or claim there is a monomorphiser limitation for Map/Set in this context.

Learnt from: aallan
Repo: aallan/vera PR: 550
File: vera/codegen/functions.py:0-0
Timestamp: 2026-04-28T18:27:48.322Z
Learning: In `vera/codegen/functions.py` `_compile_fn` (post-PR `#550`, commit 28d0262): the `return_call` → `call` revert in `body_instrs` MUST be gated on `ctx.needs_alloc OR (len(post_instrs) > 0)`, NOT on `ctx.needs_alloc` alone. Two independent sources of post-body work can follow `body_instrs` in the assembled WAT: (1) `post_instrs` from `_compile_postconditions` (`local.set $ret`, condition check, `unreachable`, `local.get $ret`) — WASM `return_call` would silently skip every `ensures(...)` check in tail-recursive functions; (2) the GC epilogue (`global.set $gc_sp`, shadow-stack unwind) for allocating functions — `return_call` leaks shadow-stack slots. The revert must be positioned AFTER `_compile_postconditions` has returned `post_instrs` (so its non-emptiness is known). The test `test_postcondition_function_falls_back_to_plain_call` is the regression guard. Do NOT re-gate this revert on `ctx.needs_alloc` alone.

Learnt from: aallan
Repo: aallan/vera PR: 485
File: vera/wasm/calls_arrays.py:622-626
Timestamp: 2026-04-17T10:13:59.841Z
Learning: In `vera/wasm/calls_arrays.py`, do NOT add per-site `arr_len * sizeof(B) > 65535` trap guards in individual array combinators (`array_map`, `array_range`, `array_concat`, `array_append`, `array_slice`). All of these can allocate >65535 bytes and are equally affected by the 16-bit GC object-header size field truncation bug. The correct, single-point fix is issue `#484`: widen the GC header size field from 16-bit to 31-bit in `vera/codegen/assembly.py` by updating the two `i32.const 65535 / i32.and` masks in `$alloc` and three in `$gc_collect`. Per-site guards would shift the landmine without defusing it.

Learnt from: aallan
Repo: aallan/vera PR: 489
File: vera/wasm/calls_arrays.py:1072-1082
Timestamp: 2026-04-17T17:27:34.889Z
Learning: In `vera/wasm/calls_arrays.py` (PR `#489`), the `u_is_adt` / `u_needs_root` heuristic in `_translate_array_fold` deliberately over-roots any non-Bool/Byte `i32` accumulator, including opaque host handles (Map, Set, Decimal, Regex). This is intentional safe over-caution: the conservative GC's alignment/range check rejects out-of-range small integers (e.g. `5` from `host_map_new`) so no spurious marking occurs, while under-rooting would be a silent-GC bug (class `#464`). The correct fix — a positive `is_gc_managed(type)` predicate applied cross-cutting across all rooting-decision sites in every mixin — is tracked in issue `#490` and is out of scope for PR `#489`. Do NOT flag the `u_is_adt` condition as incorrect or missing a positive-predicate check; it is a deliberate bias-to-root default.

Learnt from: aallan
Repo: aallan/vera PR: 544
File: tests/test_codegen.py:0-0
Timestamp: 2026-04-27T17:35:34.921Z
Learning: tests/test_codegen.py::TestGarbageCollection::test_gc_collect_bounds_check_against_heap_ptr asserts structural GC bounds checks using exact opcode patterns, not comments. It verifies:
- Layer 2: "local.get $obj_ptr … i32.add global.get $heap_ptr i32.gt_u if br $m_loop" (11 tokens) right after the "Layer 2 (issue `#515`)" marker.
- Layer 1: "local.get $obj_ptr … i32.add i32.const 4 i32.add global.get $heap_ptr i32.gt_u br_if $sc_done" (13 tokens) after "Layer 1 (issue `#515`)".
The helper _opcodes_after strips comments and normalizes whitespace, so refactors that drop these guards while keeping comments will fail the test.

Learnt from: aallan
Repo: aallan/vera PR: 344
File: tests/test_codegen.py:8452-8628
Timestamp: 2026-03-25T11:11:27.827Z
Learning: In `tests/test_codegen.py` (`TestDecimalCollection`), the tests `test_decimal_if_expr_result_type`, `test_map_if_expr_result_type`, and `test_set_if_expr_result_type` target `_infer_block_result_type` in `vera/wasm/inference.py` for opaque handle types (Decimal, Map, Set). They always execute the then-branch by design: the WASM `(if (result i32) ...)` type annotation is emitted for both branches at compile time, so a single branch execution is sufficient to verify the inference path. False-branch runtime correctness for these types is already covered separately in `TestDecimalCollection`, `TestMapCollection`, and `TestSetCollection`. Do not flag these tests as lacking else-branch coverage.

Learnt from: aallan
Repo: aallan/vera PR: 533
File: tests/test_runtime_traps.py:195-263
Timestamp: 2026-04-27T09:26:35.192Z
Learning: In `tests/test_runtime_traps.py` (vera/aallan), all JSON-mode cmd_run tests must assert `captured.err == ""` after `capsys.readouterr()`. This pins the contract that JSON-mode output is self-contained in the envelope and no human-readable `Error: ...` text leaks to real stderr. The implementation guard is in `vera/cli.py`'s `WasmTrapError` handler (~lines 645–664): stream writes are conditioned on `if as_json: ... return`, so stray stderr writes are structurally prevented, but the assertion acts as a regression net. Affected tests: test_json_mode_includes_stdout_in_envelope, test_json_mode_includes_stderr_in_envelope, test_json_mode_includes_trap_kind, test_json_contract_violation_kind.

Learnt from: aallan
Repo: aallan/vera PR: 546
File: TESTING.md:0-0
Timestamp: 2026-04-27T21:19:56.665Z
Learning: In `tests/test_runtime_traps.py` (aallan/vera PR `#546`), the CLI text-mode suppression-marker tests (`test_text_mode_collapses_leading_runtime_helper_frames` and `test_text_mode_does_not_collapse_when_all_frames_are_builtins`) use `unittest.mock.patch` on `vera.codegen.execute` to raise `WasmTrapError` with synthetic frame chains (all `is_builtin=True`). This is the canonical pattern for testing the collapse logic deterministically — real GC/allocator traps with builtin-leaf frames are timing-sensitive and not reproducible from a Vera fixture. Do not attempt to test the suppression-marker path through a real WASM trap; use the monkeypatch approach instead.

Learnt from: aallan
Repo: aallan/vera PR: 498
File: tests/test_codegen.py:10494-10511
Timestamp: 2026-04-20T10:50:31.048Z
Learning: Repo aallan/vera — tests/test_codegen.py: In TestMathBuiltins, clamp(Int) and float_clamp(Float64) intentionally define inverted-bounds (lo > hi) semantics via the implementation pattern min(max(v, lo), hi); tests expect the result to equal hi. Future reviews should not suggest changing this behavior without updating the tests and docs accordingly.

Learnt from: aallan
Repo: aallan/vera PR: 442
File: SKILL.md:1249-1249
Timestamp: 2026-03-31T21:25:04.988Z
Learning: In the Vera type system, `Nat` is a subtype of `Int`. Passing a `Nat` value where an `Int` is expected is valid and type-checks correctly without any explicit conversion (e.g., `nat_to_int`). This was confirmed by aallan via `vera check` in PR `#442`.

Learnt from: aallan
Repo: aallan/vera PR: 510
File: vera/wasm/calls_strings.py:2877-2962
Timestamp: 2026-04-23T10:22:01.626Z
Learning: In `vera/wasm/calls_strings.py` (and WASM translation mixins generally): a DRY refactor that consolidates duplicate code into a shared helper (e.g. `_translate_strip` delegating to `_translate_trim`) does NOT automatically propagate GC-root correctness from the old duplicates to the new helper. After any such consolidation, the surviving helper must be independently audited for GC shadow-stack rooting: every heap pointer that is still live across a subsequent `call $alloc` must appear in a `gc_shadow_push` before that alloc. The `_translate_trim` fix (PR `#510`, commit fb4d0b6) is the canonical example: the strip→trim DRY refactor correctly unified the whitespace predicate (rule 1) but missed the missing `gc_shadow_push(ptr)` before the destination alloc (rule 2). These two correctness properties are independent and must be checked separately.

coderabbitai · 2026-04-29T10:33:06Z

Tip

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

@aallan: Understood — the two-level argument is watertight:

Z3 can't represent type-variable sorts, so the SMT context must bail before _walk_for_subtraction_obligations runs for forall<T> bodies; option (a) silently inflates Tier-3 without catching anything, and option (b) is a deeper structural change that belongs in #555.
The codegen guard fires at each concrete monomorphized instantiation, so the runtime safety net is already in place for every compiled specialisation — this is a best-effort static gap, not a soundness hole.

The convention alignment with E520/E521/E523/E524/E525 (all bailing on generic functions today) is the right reference point. #555 as the umbrella follow-up makes sense.

✏️ Learnings added

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

Timestamp: 2026-04-29T10:33:05.026Z
Learning: In `vera/verifier.py` `_walk_for_subtraction_obligations` (PR `#554`): generic (`forall<T>`) functions are statically skipped because the SMT context setup (lines 451–490) declares Z3 vars only for concrete-typed params (`declare_nat`, `declare_int`, `declare_bool`, etc.) and bails BEFORE setup for unknown types — Z3 has no notion of type variables. Running the walker for generic bodies would either (a) silently drop obligations involving TypeVar operands to Tier-3 (inflating counts without catching anything) or (b) require deeper changes to `_is_nat_typed`/`_has_nat_origin`. This matches the existing convention for E520/E521/E523/E524/E525. The codegen guard (`_is_static_nat_typed` + `_has_nat_origin_codegen`) fires per-monomorphized instantiation, providing a runtime safety net. Extending E502 (and the other E5xx codes) to generic-function bodies is tracked in issue `#555`.

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.

🧠 Learnings used

Learnt from: aallan
Repo: aallan/vera PR: 554
File: tests/test_codegen.py:13850-13853
Timestamp: 2026-04-29T10:11:31.416Z
Learning: Repo aallan/vera — tests/test_codegen.py::TestNatSubtractionRuntimeGuard520 now includes ModuleCall coverage: `vera.math::abs(Int.1) - vera.math::abs(Int.0)` is treated as `Nat - Nat` with Nat provenance via `ast.ModuleCall`, and the WAT underflow guard (`i64.lt_s` + `unreachable`) must be emitted and trap on underflow. This ensures codegen recognizes module‑qualified Nat returns for guard insertion.

Learnt from: aallan
Repo: aallan/vera PR: 554
File: vera/verifier.py:871-1058
Timestamp: 2026-04-29T10:10:47.850Z
Learning: In `vera/verifier.py` `_walk_for_subtraction_obligations` (post-PR `#554`): `ast.ConstructorCall` and `ast.QualifiedCall` must have their `.args` walked even though neither returns `Nat`. `ConstructorCall` (returns ADT) and `QualifiedCall` (e.g. `Map.get`, currently untranslatable in SMT) don't need branches in `_is_nat_typed` or `_has_nat_origin`, but omitting arg-recursion causes `Nat - Nat` obligations nested INSIDE those args (e.g. `Some(Nat.0 - Nat.1)`) to be silently skipped. The fix is a branch per call shape that iterates args and recurses — identical in structure to the `FnCall`/`ModuleCall` branches.

Learnt from: aallan
Repo: aallan/vera PR: 554
File: spec/11-compilation.md:0-0
Timestamp: 2026-04-29T09:53:58.860Z
Learning: In `vera/codegen/api.py` `_classify_trap` (post-PR `#554`): the `Nat - Nat` underflow guard emits a bare WASM `unreachable` instruction, which `_classify_trap` classifies as `kind="unreachable"`, NOT `kind="underflow"`. A dedicated `underflow` kind would require new host-import scaffolding mirroring `vera.contract_fail` and is deferred as a future enhancement (tracked with the `kind="underflow"` follow-up alongside `#551/`#552). Do NOT flag the spec or codegen as incorrect for using `kind="unreachable"` here.

Learnt from: aallan
Repo: aallan/vera PR: 511
File: tests/test_browser.py:1272-1379
Timestamp: 2026-04-23T13:38:11.484Z
Learning: Repo aallan/vera: When a test in tests/test_browser.py or tests/test_codegen.py needs to verify that json_as_int returns Some(INT64_MIN) for the input -2^63 (i.e. JNumber(0.0 - 9223372036854775808.0)), do NOT call int_to_string(Int.0) directly — there is a pre-existing bug (`#475`, queued for v0.0.120) where int_to_string(INT64_MIN) triggers a negation overflow inside the WAT code. The correct workaround is to probe the value indirectly, e.g. via `bool_to_string(Int.0 < 0)`, and assert the result is "true". Add an inline test-body comment documenting the `#475` bug to prevent future reviewers from replacing the workaround with a direct print.

Learnt from: aallan
Repo: aallan/vera PR: 511
File: tests/test_codegen.py:12473-12510
Timestamp: 2026-04-23T13:51:17.615Z
Learning: Repo aallan/vera — tests/test_codegen.py and tests/test_browser.py: When verifying json_as_int at -2^63 (JNumber(-9223372036854775808.0)), use two indirect probes to avoid the known int_to_string(INT64_MIN) negation-overflow bug (`#475`): (a) assert bool_to_string(Int.0 < 0) == "true"; and (b) assert int_to_string(Int.0 + 1) == "-9223372036854775807". Include an inline "#475" comment. Implemented in commit 3cf5a13 (PR `#511`).

Learnt from: aallan
Repo: aallan/vera PR: 550
File: tests/test_codegen.py:1930-2111
Timestamp: 2026-04-28T19:28:33.529Z
Learning: Repo aallan/vera — tests/test_codegen.py (PR `#550`): Tail-position analyzer coverage now includes explicit negative unit tests asserting compute_tail_call_sites does NOT mark calls in non-transparent positions:
- test_analyzer_does_not_mark_call_in_block_statement (ExprStmt.expr in a Block),
- test_analyzer_does_not_mark_call_in_if_condition (IfExpr.condition),
- test_analyzer_does_not_mark_call_in_match_scrutinee (MatchExpr.scrutinee).
These complement existing positives (Block trailing expr, If branches, Match arm bodies) and prior negatives (LetStmt.value, FnCall.args), making the analyzer’s transparent vs non-transparent rules pairwise complete.

Learnt from: aallan
Repo: aallan/vera PR: 0
File: :0-0
Timestamp: 2026-03-29T17:17:11.974Z
Learning: In `tests/test_codegen.py`, `test_option_unwrap_or_map` (lines ~9936–9949) and `test_option_unwrap_or_set` (lines ~9950–9963) are regular, unconditionally-passing tests with NO `xfail`, `skip`, or `skipif` marks. `grep -rn "xfail" tests/` returns zero results across the entire test suite. The PR `#428` fix resolved the underlying monomorphiser inference gap for opaque i32 handle types (Map, Set) in `option_unwrap_or` generics. Do NOT flag these tests as xfail or claim there is a monomorphiser limitation for Map/Set in this context.

Learnt from: aallan
Repo: aallan/vera PR: 550
File: vera/codegen/functions.py:0-0
Timestamp: 2026-04-28T18:27:48.322Z
Learning: In `vera/codegen/functions.py` `_compile_fn` (post-PR `#550`, commit 28d0262): the `return_call` → `call` revert in `body_instrs` MUST be gated on `ctx.needs_alloc OR (len(post_instrs) > 0)`, NOT on `ctx.needs_alloc` alone. Two independent sources of post-body work can follow `body_instrs` in the assembled WAT: (1) `post_instrs` from `_compile_postconditions` (`local.set $ret`, condition check, `unreachable`, `local.get $ret`) — WASM `return_call` would silently skip every `ensures(...)` check in tail-recursive functions; (2) the GC epilogue (`global.set $gc_sp`, shadow-stack unwind) for allocating functions — `return_call` leaks shadow-stack slots. The revert must be positioned AFTER `_compile_postconditions` has returned `post_instrs` (so its non-emptiness is known). The test `test_postcondition_function_falls_back_to_plain_call` is the regression guard. Do NOT re-gate this revert on `ctx.needs_alloc` alone.

Learnt from: aallan
Repo: aallan/vera PR: 485
File: vera/wasm/calls_arrays.py:622-626
Timestamp: 2026-04-17T10:13:59.841Z
Learning: In `vera/wasm/calls_arrays.py`, do NOT add per-site `arr_len * sizeof(B) > 65535` trap guards in individual array combinators (`array_map`, `array_range`, `array_concat`, `array_append`, `array_slice`). All of these can allocate >65535 bytes and are equally affected by the 16-bit GC object-header size field truncation bug. The correct, single-point fix is issue `#484`: widen the GC header size field from 16-bit to 31-bit in `vera/codegen/assembly.py` by updating the two `i32.const 65535 / i32.and` masks in `$alloc` and three in `$gc_collect`. Per-site guards would shift the landmine without defusing it.

Learnt from: aallan
Repo: aallan/vera PR: 489
File: vera/wasm/calls_arrays.py:1072-1082
Timestamp: 2026-04-17T17:27:34.889Z
Learning: In `vera/wasm/calls_arrays.py` (PR `#489`), the `u_is_adt` / `u_needs_root` heuristic in `_translate_array_fold` deliberately over-roots any non-Bool/Byte `i32` accumulator, including opaque host handles (Map, Set, Decimal, Regex). This is intentional safe over-caution: the conservative GC's alignment/range check rejects out-of-range small integers (e.g. `5` from `host_map_new`) so no spurious marking occurs, while under-rooting would be a silent-GC bug (class `#464`). The correct fix — a positive `is_gc_managed(type)` predicate applied cross-cutting across all rooting-decision sites in every mixin — is tracked in issue `#490` and is out of scope for PR `#489`. Do NOT flag the `u_is_adt` condition as incorrect or missing a positive-predicate check; it is a deliberate bias-to-root default.

Learnt from: aallan
Repo: aallan/vera PR: 508
File: vera/wasm/calls_arrays.py:0-0
Timestamp: 2026-04-22T21:04:45.783Z
Learning: In `vera/wasm/calls_arrays.py`, `_translate_array_flatten` intentionally restricts inner-element-type (`T`) recovery to `ast.SlotRef` inputs only. `_infer_concat_elem_type` is used as a first gate (returns `"Array"` for the outer element type, bails on anything else), but it drops nested type parameters — it cannot recover `T` from `Array<Array<T>>` when the input is a `FnCall` result or a type alias. Teaching helpers to carry structural type representations (or adding a `_infer_nested_array_inner_type` helper) is the correct fix, tracked in issue `#507` alongside the broader inference-infrastructure work. Do NOT flag the SlotRef-only walk as incomplete — it is the intentional scope for PR `#508` / phase 1.

Learnt from: aallan
Repo: aallan/vera PR: 554
File: SKILL.md:0-0
Timestamp: 2026-04-29T09:52:56.682Z
Learning: In `aallan/vera` `SKILL.md` (and the `stack_exhausted` fix paragraph in `vera/codegen/api.py`): accumulator-style recursion where the accumulator carries heap data (e.g. an `Array<T>` or `String`) does NOT escape the `call stack exhausted` bug for allocating tail-recursive functions — the accumulator itself is allocating, so `return_call` still cannot be used. The canonical three-option workaround remains: (1) iterate via `array_fold`/`array_map` (compile to WASM loops with no per-iteration frame cost), (2) split into bounded chunks of <5K frames each, (3) wait for GC-aware `return_call` (`#549`). Do NOT recommend `Int` accumulator reshaping as a stack-flattening technique unless the recursion is confirmed non-allocating.

Learnt from: aallan
Repo: aallan/vera PR: 548
File: vera/codegen/api.py:0-0
Timestamp: 2026-04-28T15:29:31.096Z
Learning: In `vera/codegen/api.py` `_TRAP_FIX_PARAGRAPHS["stack_exhausted"]` (post-PR `#548` commit 1bb3983): the canonical pre-TCO fix paragraph names three working workarounds — (1) iterate via `array_fold`/`array_map`/etc. which compile to WASM loops rather than recursion, (2) split work into bounded chunks of <5K frames each, (3) wait for `#517`. It explicitly states "Until `#517` ships, accumulator-style recursion will not save you here — without TCO each tail call still pushes a fresh frame." Do NOT recommend accumulator-shaped recursive helpers as a stack-flattening technique until `return_call` (`#517`) ships. The test substring anchor is `"return_call" in fix`.

Learnt from: aallan
Repo: aallan/vera PR: 344
File: tests/test_codegen.py:8630-8834
Timestamp: 2026-03-29T17:13:40.986Z
Learning: In `tests/test_codegen.py` (`TestDecimalMonomorphization`), there is a deliberate asymmetry in opaque-handle monomorphization for Map and Set:
- `match` on `Option<Map<...>>` / `Option<Set<...>>` compiles and runs correctly because `match` is emitted inline by the codegen (no standalone monomorphized function is required).
- `option_unwrap_or<Map<...>>` / `option_unwrap_or<Set<...>>` currently fails (pinned as `xfail` in `test_option_unwrap_or_map`) because it requires the monomorphizer to generate a standalone specialised function body (e.g. `option_unwrap_or$Map`), which is not yet supported for opaque i32 handle types (Map, Set). `option_unwrap_or<Decimal>` works because Decimal support was added in PR `#344`. The remaining Map/Set gap is tracked as a follow-up to issue `#341`.

Learnt from: aallan
Repo: aallan/vera PR: 442
File: SKILL.md:1249-1249
Timestamp: 2026-03-31T21:25:04.988Z
Learning: In the Vera type system, `Nat` is a subtype of `Int`. Passing a `Nat` value where an `Int` is expected is valid and type-checks correctly without any explicit conversion (e.g., `nat_to_int`). This was confirmed by aallan via `vera check` in PR `#442`.

Learnt from: aallan
Repo: aallan/vera PR: 510
File: vera/wasm/calls_strings.py:2877-2962
Timestamp: 2026-04-23T10:22:01.626Z
Learning: In `vera/wasm/calls_strings.py` (and WASM translation mixins generally): a DRY refactor that consolidates duplicate code into a shared helper (e.g. `_translate_strip` delegating to `_translate_trim`) does NOT automatically propagate GC-root correctness from the old duplicates to the new helper. After any such consolidation, the surviving helper must be independently audited for GC shadow-stack rooting: every heap pointer that is still live across a subsequent `call $alloc` must appear in a `gc_shadow_push` before that alloc. The `_translate_trim` fix (PR `#510`, commit fb4d0b6) is the canonical example: the strip→trim DRY refactor correctly unified the whitespace predicate (rule 1) but missed the missing `gc_shadow_push(ptr)` before the destination alloc (rule 2). These two correctness properties are independent and must be checked separately.

coderabbitai

♻️ Duplicate comments (1)

tests/test_codegen.py (1)

13712-14059: ⚠️ Potential issue | 🟠 Major

Add a rhs-only provenance regression test (0 - @Nat.0``).

The suite still misses the asymmetric rhs-only provenance path. If _has_nat_origin_codegen ever regresses to lhs-only checking, this class can still pass while shipping an unguarded underflow site.

Proposed test addition

+    def test_rhs_only_nat_provenance_emits_guard_and_traps(self) -> None:
+        """`0 - `@Nat.0`` must still emit the underflow guard."""
+        src = """
+private fn rhs_only(`@Nat` -> `@Nat`)
+  requires(true) ensures(true) effects(pure)
+{
+  0 - `@Nat.0`
+}
+
+public fn main(`@Unit` -> `@Nat`)
+  requires(true) ensures(true) effects(pure)
+{
+  rhs_only(1)
+}
+"""
+        result = _compile_ok(src)
+        wat = result.wat
+        fn_idx = wat.find("(func $rhs_only")
+        assert fn_idx >= 0
+        body_end = wat.find("\n  (func ", fn_idx + 1)
+        if body_end < 0:
+            body_end = len(wat)
+        body = wat[fn_idx:body_end]
+        assert "i64.lt_s" in body and "unreachable" in body
+        with pytest.raises((wasmtime.WasmtimeError, wasmtime.Trap, RuntimeError)):
+            execute(result, fn_name="main", args=[])

As per coding guidelines: “DO flag: Missing edge cases for new compiler features.”

🤖 Prompt for AI Agents

Verify each finding against the current code and only fix it if needed.

In `@tests/test_codegen.py` around lines 13712 - 14059, Add a new test in
TestNatSubtractionRuntimeGuard520 that covers the asymmetric rhs-only provenance
case (literal lhs, provenanced rhs) so regressions that check only the lhs don't
slip; create a small src where the body computes `0 - `@Nat.0`` (eg. private fn
unsafe_rhs_only(`@Nat` -> `@Nat`) { 0 - `@Nat.0` } and public main calling
unsafe_rhs_only(1) to cause underflow), then assert structurally that the
compiled WAT for the function (find "(func $unsafe_rhs_only") contains both
"i64.lt_s" and "unreachable" and assert behaviourally that executing main traps
(wrap call in pytest.raises like other tests) and add a safe case (e.g. call
with 0) to verify non-underflow returns cleanly; place the test method alongside
the existing tests in the same class so it covers the missing edge-case for
_has_nat_origin_codegen.

🤖 Prompt for all review comments with AI agents

Verify each finding against the current code and only fix it if needed.

Duplicate comments:
In `@tests/test_codegen.py`:
- Around line 13712-14059: Add a new test in TestNatSubtractionRuntimeGuard520
that covers the asymmetric rhs-only provenance case (literal lhs, provenanced
rhs) so regressions that check only the lhs don't slip; create a small src where
the body computes `0 - `@Nat.0`` (eg. private fn unsafe_rhs_only(`@Nat` -> `@Nat`) { 0
- `@Nat.0` } and public main calling unsafe_rhs_only(1) to cause underflow), then
assert structurally that the compiled WAT for the function (find "(func
$unsafe_rhs_only") contains both "i64.lt_s" and "unreachable" and assert
behaviourally that executing main traps (wrap call in pytest.raises like other
tests) and add a safe case (e.g. call with 0) to verify non-underflow returns
cleanly; place the test method alongside the existing tests in the same class so
it covers the missing edge-case for _has_nat_origin_codegen.

ℹ️ Review info

⚙️ Run configuration

Configuration used: Path: .coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro

Run ID: 04ab674c-b64a-49d9-bf9e-770acd2eceee

📥 Commits

Reviewing files that changed from the base of the PR and between 488deff and d0ee770.

📒 Files selected for processing (3)

KNOWN_ISSUES.md
TESTING.md
tests/test_codegen.py

@nat

One real coverage gap; one duplicate finding already addressed in round 4. tests/test_codegen.py - New test_rhs_only_provenance_emits_guard_and_traps in TestNatSubtractionRuntimeGuard520. The previous tests pin three provenance shapes: * left-only: `@Nat.0 - 1` (test_recursion_with_path_guard) * both: `@Nat.1 - @Nat.0` (test_underflow_traps_at_runtime) * both via ModuleCall: `vera.math::abs(...) - vera.math::abs(...)` (test_modulecall_provenance_emits_guard_and_traps) But not RIGHT-only. Without that case, a future refactor that accidentally ignored `expr.right` in `_has_nat_origin_codegen` (or changed the `or` between the two helper calls to `and`) would still pass every existing test while silently re-opening the underflow hole for the right-only shape. New test uses body `0 - @Nat.0` — non-negative IntLit on the left, @nat slot on the right. Both operands are statically @nat (per checker.py:62 — non-negative IntLit is @nat) but only the slot has @nat *provenance*, so the `or` in `_is_nat_subtraction` makes the subtraction-detector fire via the rhs-only branch. Asserts: * Structural: WAT body of `lit_minus_slot` contains both `i64.lt_s` and `unreachable`. * Behavioural (unsafe): `lit_minus_slot(1)` → `0 - 1` → trap. * Behavioural (safe): `lit_minus_slot(0)` → `0 - 0 = 0`. TESTING.md / ROADMAP.md - Doc-counts bump for the new test: * Tests headline: 3,639 → 3,640 across (3,626 passed, 14 skipped). * test_codegen.py row: 997 → 998 / 14,059 → 14,131. * ROADMAP.md by-the-numbers footer: 3,639 → 3,640. The duplicate finding (stale comment about `unsafe_modcall(5, 0)` on line 14031) was already corrected in round 4 commit d0ee770; no further change needed. Inline reply on the PR points at d0ee770. Verification: - All 8 TestNatSubtractionRuntimeGuard520 tests pass; mypy clean; doc-counts / limitations-sync / version-sync / spec-examples all green. Co-Authored-By: Claude <noreply@anthropic.invalid>

aallan and others added 5 commits April 28, 2026 23:07

coderabbitai Bot reviewed Apr 29, 2026

View reviewed changes

Comment thread TESTING.md

Comment thread tests/test_codegen.py Outdated

Comment thread vera/verifier.py

coderabbitai Bot reviewed Apr 29, 2026

View reviewed changes

Comment thread tests/test_codegen.py Outdated

coderabbitai Bot reviewed Apr 29, 2026

View reviewed changes

Comment thread tests/test_codegen.py

aallan mentioned this pull request Apr 29, 2026

Generic functions bypass E502 underflow obligation (follow-up to #520) #555

Open

coderabbitai Bot reviewed Apr 29, 2026

View reviewed changes

aallan merged commit 62b57f7 into main Apr 29, 2026
20 checks passed

aallan deleted the claude/fix-520-nat-underflow branch April 29, 2026 10:51

aallan mentioned this pull request May 1, 2026

ROADMAP: split #170 row into bookmark + active features (#562) #563

Merged

4 tasks

coderabbitai Bot mentioned this pull request Jun 10, 2026

feat: reify proof obligations + warm Z3 session (#222 Phase A) #716

Merged

Conversation

aallan commented Apr 29, 2026 • edited by coderabbitai Bot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

The bug

Before / after

Two-sided implementation

Static — verifier proof obligation

Runtime — codegen guard

Path-A scope: pure-literal subtractions exempt

Migration

Spec

Tests

New error code

Documentation

Test plan

Summary by CodeRabbit

Uh oh!

codecov Bot commented Apr 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

coderabbitai Bot commented Apr 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Reviews paused

Walkthrough

Changes

Sequence Diagram(s)

Estimated code review effort

Possibly related issues

Possibly related PRs

Suggested labels

Uh oh!

coderabbitai Bot left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

coderabbitai Bot left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

aallan commented Apr 29, 2026

Uh oh!

coderabbitai Bot left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

coderabbitai Bot commented Apr 29, 2026

Uh oh!

coderabbitai Bot left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

aallan commented Apr 29, 2026

Uh oh!

aallan commented Apr 29, 2026

Uh oh!

coderabbitai Bot commented Apr 29, 2026

Uh oh!

coderabbitai Bot commented Apr 29, 2026

Uh oh!

coderabbitai Bot left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

aallan commented Apr 29, 2026 •

edited by coderabbitai Bot

Loading

codecov Bot commented Apr 29, 2026 •

edited

Loading

coderabbitai Bot commented Apr 29, 2026 •

edited

Loading