fix: address CodeRabbit full-review findings (alias-aware guards, side-table, test pins, doc counts)

aallan · Claude · aallan · commit f5a328f3bcea · 2026-06-18T07:57:22.000+01:00
CodeRabbit's full review of PR #756 surfaced 8 findings; this commit addresses all (7 fixes + 1 evidence-based reword). Soundness (Major): - registration.py `_type_resolves_to_nat`: apply alias type-argument substitution so a generic alias instantiated to Nat (`type Id<T> = T` used as `Id<Nat>`) resolves to Nat rather than the bare type-param `T`, closing a missed runtime guard for generic-alias Nat ctor fields / formals. - wasm/data.py + wasm/context.py: the four bind-site runtime guards (let, top-level match, ADT sub-pattern, tuple-destructure component) gated on `type_name == "Nat"` now resolve through `_resolve_base_type_name`, so a `type Age = Nat` alias / refined-Nat target is guarded too (was silently skipped on a verification-less compile). Provable no-op for non-aliases. - verifier.py `verify()`: recompute the checker side-tables when EITHER is missing (was `and`), so a caller supplying only one table no longer leaves the other empty and silently under-fires the #747 generic-instantiation checks. Tests: - test_codegen.py `_body`: boundary-safe regex so `$gcall` does not slice `$gcall_helper`'s body. Add two alias-guard regression pins (Nat-alias let-bind, generic-alias ctor field). - test_verifier.py: pin the concrete imported-ctor discharged test to `status == ["verified"]` (was satisfiable by no obligation emitted at all). Docs: - CHANGELOG: ruff total ~176 -> ~175 (134 auto-fixed + 41 hand-triaged). - HISTORY footer: 173 -> 174 tagged releases, 76 -> 77 active days (sync with the intro header and the README status line). - TESTING: reworded the Nat E504-residual note. Kept generic-instantiated — empirically it DOES reach E504 (a generic formal erases to i64, so codegen cannot guard it), so removing it as suggested would make the doc inaccurate; fixed only the muddled shared parenthetical. Synced test/line counts. - ROADMAP: test count 4441 -> 4443. Co-Authored-By: Claude <noreply@anthropic.invalid>
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -10,7 +10,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
 
 ### Added
 
-- **ruff is now an enforced lint gate** ([#733](https://github.com/aallan/vera/issues/733)).  `ruff check` (default `F`/`E` rules) runs in pre-commit (before mypy) and the CI lint job — ruff shipped in the `[dev]` extras but nothing ran it, so ~176 findings had accumulated silently.  All cleared: 134 auto-fixed (unused imports, placeholder-less f-strings, redefinitions) and 41 hand-triaged (the three dead `skip_langs` sets, unused locals, ambiguous names, `ResolvedModule` string-annotation hoists, semicolon splits, a `type()` comparison).  Bundles the ruff `0.15.16` → `0.15.17` bump ([#741](https://github.com/aallan/vera/pull/741)).
+- **ruff is now an enforced lint gate** ([#733](https://github.com/aallan/vera/issues/733)).  `ruff check` (default `F`/`E` rules) runs in pre-commit (before mypy) and the CI lint job — ruff shipped in the `[dev]` extras but nothing ran it, so ~175 findings had accumulated silently.  All cleared: 134 auto-fixed (unused imports, placeholder-less f-strings, redefinitions) and 41 hand-triaged (the three dead `skip_langs` sets, unused locals, ambiguous names, `ResolvedModule` string-annotation hoists, semicolon splits, a `type()` comparison).  Bundles the ruff `0.15.16` → `0.15.17` bump ([#741](https://github.com/aallan/vera/pull/741)).
 - **The `@Nat >= 0` narrowing invariant is now obligated at every binding site** ([#747](https://github.com/aallan/vera/issues/747)).  #552 covered `let` / call-argument / effect-operation-argument / concrete-constructor-field / match-bind / literal-tuple-destructure narrowing; #747 extends the **static** obligation to the projection and instantiation sites — ADT sub-pattern binds (`match opt { Some(@Nat) -> }` on `Option<Int>`), non-literal tuple destructures (via new Z3 tuple-datatype support in the SMT layer), generic constructor / effect-operation / function formals instantiated to `@Nat`, and imported ADT constructors with `@Nat` fields — by threading the checker's instantiated expression types into the verifier, so every narrowing shape now verifies statically.  The Tier-3 **runtime** guard also extends to the tuple-destructure, top-level match-bind, ADT-sub-pattern, concrete-constructor-field, and call-argument sites, so an unverified compile traps on a negative `@Nat` rather than storing it silently (the effect-operation-argument runtime guard and a dedicated guard trap kind are tracked as [#754](https://github.com/aallan/vera/issues/754)).  Folds in the [#749](https://github.com/aallan/vera/issues/749) review-debt test pins (IndexExpr / InterpolatedString walker recursion, the `_fresh_slot_var` nat-alias path, and a `_narrows_into_nat` verifier/codegen parity test).
 
 ### Changed
diff --git a/HISTORY.md b/HISTORY.md
@@ -399,4 +399,4 @@ Proof obligations became first-class records with a warm Z3 session, and the LSP
 | Spec chapters | 7 | 10 | 11 | 12 | 13 | 13 | 13 | 13 |
 | Code coverage | — | — | — | 90% | 91% | 96% | 96% | 95% |
 
-Total: **1,400+ commits, 173 tagged releases, 76 active development days.**
+Total: **1,400+ commits, 174 tagged releases, 77 active development days.**
diff --git a/ROADMAP.md b/ROADMAP.md
@@ -8,7 +8,7 @@ Priority lives in this file and nowhere else — issues carry kind and area labe
 
 ## Where we are
 
-4,441 tests, 90 conformance programs, 35 examples, 13 spec chapters.
+4,443 tests, 90 conformance programs, 35 examples, 13 spec chapters.
 
 ## The roadmap
 
diff --git a/TESTING.md b/TESTING.md
@@ -6,7 +6,7 @@ This is the single source of truth for Vera's testing infrastructure, coverage d
 
 | Metric | Value |
 |--------|-------|
-| **Tests** | 4,441 across 36 files (~57,700 lines of test code; 4,410 passed + 16 stress, 15 skipped) |
+| **Tests** | 4,443 across 36 files (~57,700 lines of test code; 4,412 passed + 16 stress, 15 skipped) |
 | **Compiler code coverage** | 95% Python, 61% JavaScript — 91% combined (CI minimum: 80%) |
 | **Conformance programs** | 90 programs across 9 spec chapters, validating every language feature |
 | **Example programs** | 35, all validated through `vera check` + `vera verify` |
@@ -59,8 +59,8 @@ python scripts/fix_allowlists.py --fix               # auto-fix stale allowlists
 | `test_ast.py` | 128 | 1,122 | AST transformation, node structure, serialisation, string escape sequences, ability declarations |
 | `test_checker.py` | 521 | 5,939 | Type synthesis, slot resolution, effects, effect subtyping, contracts, exhaustiveness, cross-module typing, visibility, error codes, string built-ins, generic rejection, IO operation types, Markdown types, Regex types, abilities, Map collection, Set collection, Decimal type, Json type, Html type, Http effect, Inference effect, removed legacy name regression |
 | `test_obligations.py` | 268 | 851 | Reified proof obligations + warm `VerificationSession` (#222 Phase A): full-corpus differential oracle (warm session == cold `verify()` on diagnostics, summary, and obligation stream, plus warm-twice determinism, across all 35 examples and every verify/run-level conformance program), summary↔obligation tier-bookkeeping consistency, per-kind unit tests (requires / ensures / decreases / nat_sub / call_pre statuses, counterexamples, error codes), content-key stability + same-text-two-sites span disambiguation, session solver reuse, type-error short-circuit, ADT-registry resync between programs; plus the Phase B incremental suite — identical-source full replay, callee-body-edit replays callers while callee-contract-edit invalidates them, span-shift and ADT-edit conservative invalidation, cross-program isolation, timeout-status never cached (monkeypatched solver), FIFO eviction bound; plus the #727 dedup pin — a violating call in a let RHS records exactly one E501 diagnostic and one call_pre obligation |
-| `test_verifier.py` | 195 | 3,169 | Z3 verification, counterexamples, tier classification, call-site preconditions, branch-aware preconditions, pipe operator, cross-module contracts, match/ADT verification, decreases verification, mutual recursion, refined Bool/String/Float64 param sorts, **@Nat subtraction underflow obligation** (#520 — Path-A obligation discharge via requires/path-conditions/path-aware Z3 refutation, pure-literal exclusion, Int-Int and Nat-Int → Int exemptions), **@Nat binding-site narrowing obligation** (#552 — Tier-1 `value >= 0` at let/call-arg/effect-op-arg/ctor-field/match-bind/literal-destructure narrowing, #520 double-emit disjointness, E503 counterexample-witness pin; #747 — generic-instantiation, ADT sub-pattern, non-literal tuple-destructure, and cross-module imported-ctor narrowing, with concrete-site Tier-3 narrowings (incl. the if-expr-source SMT gap, recorded per-component) classified as codegen-guarded `tier3_runtime` and only effect-op-arg / generic-instantiated narrowings (whose `@Nat` codegen erases to i64) surfacing the `E504` unguarded warning; #749 — IndexExpr/InterpolatedString walker-recursion pins, `_fresh_slot_var` nat-alias unit test, `_narrows_into_nat` verifier/codegen soundness parity) |
-| `test_codegen.py` | 1,167 | 20,268 | WASM compilation, arithmetic, Float64, Byte, arrays (incl. compound element types), ADTs, match (incl. nested patterns), generics, State\<T\>, Exn\<E\> handlers, control flow, strings, string escape sequences, IO (read\_line, read\_file, write\_file, args, exit, get\_env, sleep, time, stderr), bounds checking, quantifiers, assert/assume, refinement type aliases, pipe operator, string built-ins, built-in shadowing, parse\_nat Result, GC, Markdown host bindings, Regex host bindings, Map collection, Set collection, Decimal type, Json type, Html type, Http effect, Inference effect, Random effect, example round-trips, GC shadow stack overflow, **WASM tail-call optimization** (#517 — `return_call` emission for tail-position calls, 50K- and 1M-iteration stress, structural assertions on `return_call`/plain `call` boundary, **GC-aware TCO for allocating fns (#549 — `$gc_sp` restore before each `return_call`)**, postcondition-fallback regression (still reverts to plain `call`), analyzer unit tests covering Block-trailing / IfExpr-both-branches / MatchExpr-arm-bodies / let-value-NOT-marked / call-args-NOT-marked / ExprStmt-statement-NOT-marked / IfExpr-condition-NOT-marked / MatchExpr-scrutinee-NOT-marked), **@Nat narrowing runtime guards** (#552 let site; #747 extends to tuple-destructure / top-level match-bind / ADT sub-pattern / concrete ctor-field / call-arg sites — `i64.lt_s; unreachable` net, @Int targets exempt) |
+| `test_verifier.py` | 195 | 3,173 | Z3 verification, counterexamples, tier classification, call-site preconditions, branch-aware preconditions, pipe operator, cross-module contracts, match/ADT verification, decreases verification, mutual recursion, refined Bool/String/Float64 param sorts, **@Nat subtraction underflow obligation** (#520 — Path-A obligation discharge via requires/path-conditions/path-aware Z3 refutation, pure-literal exclusion, Int-Int and Nat-Int → Int exemptions), **@Nat binding-site narrowing obligation** (#552 — Tier-1 `value >= 0` at let/call-arg/effect-op-arg/ctor-field/match-bind/literal-destructure narrowing, #520 double-emit disjointness, E503 counterexample-witness pin; #747 — generic-instantiation, ADT sub-pattern, non-literal tuple-destructure, and cross-module imported-ctor narrowing, with concrete-site Tier-3 narrowings (incl. the if-expr-source SMT gap, recorded per-component) classified as codegen-guarded `tier3_runtime`, and the two genuinely-unguarded residuals — effect-op-arg narrowings (no codegen guard yet, #754) and generic-instantiated field/argument narrowings (whose `@Nat` erases to i64) — surfacing the `E504` unguarded warning; #749 — IndexExpr/InterpolatedString walker-recursion pins, `_fresh_slot_var` nat-alias unit test, `_narrows_into_nat` verifier/codegen soundness parity) |
+| `test_codegen.py` | 1,169 | 20,296 | WASM compilation, arithmetic, Float64, Byte, arrays (incl. compound element types), ADTs, match (incl. nested patterns), generics, State\<T\>, Exn\<E\> handlers, control flow, strings, string escape sequences, IO (read\_line, read\_file, write\_file, args, exit, get\_env, sleep, time, stderr), bounds checking, quantifiers, assert/assume, refinement type aliases, pipe operator, string built-ins, built-in shadowing, parse\_nat Result, GC, Markdown host bindings, Regex host bindings, Map collection, Set collection, Decimal type, Json type, Html type, Http effect, Inference effect, Random effect, example round-trips, GC shadow stack overflow, **WASM tail-call optimization** (#517 — `return_call` emission for tail-position calls, 50K- and 1M-iteration stress, structural assertions on `return_call`/plain `call` boundary, **GC-aware TCO for allocating fns (#549 — `$gc_sp` restore before each `return_call`)**, postcondition-fallback regression (still reverts to plain `call`), analyzer unit tests covering Block-trailing / IfExpr-both-branches / MatchExpr-arm-bodies / let-value-NOT-marked / call-args-NOT-marked / ExprStmt-statement-NOT-marked / IfExpr-condition-NOT-marked / MatchExpr-scrutinee-NOT-marked), **@Nat narrowing runtime guards** (#552 let site; #747 extends to tuple-destructure / top-level match-bind / ADT sub-pattern / concrete ctor-field / call-arg sites — `i64.lt_s; unreachable` net, @Int targets exempt) |
 | `test_codegen_contracts.py` | 32 | 570 | Runtime pre/postconditions, contract fail messages, old/new state postconditions |
 | `test_codegen_monomorphize.py` | 71 | 1,320 | Generic instantiation, type inference, monomorphization edge cases, ability constraint satisfaction (Eq/Ord/Hash/Show), operation rewriting (eq/compare), show/hash dispatch, ADT auto-derivation, array operations (slice/map/filter/fold) |
 | `test_codegen_closures.py` | 50 | 1,618 | Closure lifting, captured variables, higher-order functions, iterative-builder shadow-stack regressions (#570), closure return-value shadow-push balance for both i32-pair and i32-ADT branches across array_map and array_mapi, plus VERA_EAGER_GC injection self-test (#593), IndexExpr-of-FnCall element-type inference (#614), non-contiguous capture and walker-order miscompiles (#615) |
diff --git a/tests/test_codegen.py b/tests/test_codegen.py
@@ -16541,8 +16541,11 @@ def _body(wat: str, fn: str) -> str:
         arithmetic / ctor / match bodies — the negative-traps tests below
         pin the guard's runtime *semantics* independently.
         """
-        idx = wat.find(f"(func ${fn}")
-        assert idx >= 0, f"{fn} not found in WAT"
+        # Boundary-safe so `$gcall` does not match `$gcall_helper` — a plain
+        # substring `find` would slice the wrong body (CR #756).
+        m = re.search(rf"\(func \${re.escape(fn)}(?![A-Za-z0-9_$.])", wat)
+        assert m is not None, f"{fn} not found in WAT"
+        idx = m.start()
         end = wat.find("\n  (func ", idx + 1)
         return wat[idx:end if end >= 0 else len(wat)]
 
@@ -16597,6 +16600,31 @@ def test_concrete_nat_call_arg_guarded(self) -> None:
 """)
         assert "i64.lt_s" in self._body(result.wat, "gcall")
 
+    def test_nat_alias_let_bind_guarded(self) -> None:
+        """A `type Age = Nat` alias target is guarded at the let-bind site —
+        `_resolve_base_type_name` resolves the alias so the runtime guard is
+        not skipped by the bare `type_name == "Nat"` check (CR #756)."""
+        result = _compile_ok("""
+type Age = Nat;
+public fn galias(@Int -> @Age)
+  requires(true) ensures(true) effects(pure)
+{ let @Age = @Int.0; @Age.0 }
+""")
+        assert "i64.lt_s" in self._body(result.wat, "galias")
+
+    def test_generic_nat_alias_ctor_field_guarded(self) -> None:
+        """A generic alias instantiated to @Nat (`type Id<T> = T` used as
+        `Id<Nat>`) resolves to Nat via type-argument substitution, so the
+        constructor-field narrowing is still guarded (CR #756)."""
+        result = _compile_ok("""
+type Id<T> = T;
+public data GBox { GWrap(Id<Nat>) }
+public fn ggen(@Int -> @GBox)
+  requires(true) ensures(true) effects(pure)
+{ GWrap(@Int.0) }
+""")
+        assert "i64.lt_s" in self._body(result.wat, "ggen")
+
     def test_int_ctor_field_emits_no_guard(self) -> None:
         """A concrete @Int constructor field is not a narrowing target —
         no guard, mirroring the @Int-field/@Int-formal exemption."""
diff --git a/tests/test_verifier.py b/tests/test_verifier.py
@@ -2440,8 +2440,12 @@ def test_imported_ctor_concrete_nat_field_discharged(self) -> None:
   effects(pure)
 { WrapN(@Int.0) }
 """, [mod])
-        assert not [o for o in result.obligations
-                    if o.kind == "nat_bind" and o.status == "violated"]
+        # Pin that the obligation actually fired and verified — not merely the
+        # absence of a violation (which a no-obligation regression would also
+        # satisfy), mirroring the generic discharged companion (CR #756).
+        statuses = [o.status for o in result.obligations
+                    if o.kind == "nat_bind"]
+        assert statuses == ["verified"], statuses
         assert [d for d in result.diagnostics if d.severity == "error"] == []
 
     def test_imported_ctor_generic_field_nat_obligated(self) -> None:
diff --git a/vera/codegen/registration.py b/vera/codegen/registration.py
@@ -8,6 +8,7 @@
 
 from vera import ast
 from vera.codegen.api import ConstructorLayout, _align_up, _wasm_type_align, _wasm_type_size
+from vera.wasm.inference import substitute_type_vars
 
 
 class RegistrationMixin:
@@ -276,15 +277,18 @@ def _compute_constructor_layout(
 
     def _type_resolves_to_nat(self, te: ast.TypeExpr) -> bool:
         """True if *te* is ``@Nat`` directly, through a ``type X = Nat``
-        alias, or as the base of a refinement (``{ @Nat | p }``) — used for
-        the #747 runtime-guard metadata so an alias/refinement-typed @Nat
-        formal or field is still guarded (CR #756), mirroring the verifier's
-        alias-aware ``_is_nat_type``.
+        alias, the base of a refinement (``{ @Nat | p }``), or a *generic*
+        alias instantiated to @Nat (``type Id<T> = T`` used as ``Id<Nat>``)
+        — used for the #747 runtime-guard metadata so an alias/refinement-
+        typed @Nat formal or field is still guarded (CR #756), mirroring the
+        verifier's alias-aware ``_is_nat_type``.
 
         Alias resolution uses ``self._type_aliases``, populated in
         declaration order during ``_register_all``; a `@Nat` alias declared
         *after* the function/data that uses it is not yet visible here and
-        falls back to the verifier's static obligation.
+        falls back to the verifier's static obligation.  Generic alias
+        arguments are bound into the body via ``substitute_type_vars`` so
+        ``Id<Nat>`` resolves to ``Nat`` rather than the bare type-param ``T``.
         """
         seen: set[str] = set()
         while True:
@@ -297,6 +301,12 @@ def _type_resolves_to_nat(self, te: ast.TypeExpr) -> bool:
                 alias = self._type_aliases.get(te.name)
                 if alias is not None and te.name not in seen:
                     seen.add(te.name)
+                    params = self._type_alias_params.get(te.name)
+                    if (params and te.type_args
+                            and len(params) == len(te.type_args)):
+                        alias = substitute_type_vars(
+                            alias, dict(zip(params, te.type_args)),
+                        )
                     te = alias
                     continue
             return False
diff --git a/vera/verifier.py b/vera/verifier.py
@@ -94,18 +94,23 @@ def verify(
     contract verification (C7d).  Imported function preconditions are
     checked at call sites; postconditions are assumed.
     """
-    if expr_types is None and expr_target_types is None:
+    if expr_types is None or expr_target_types is None:
         # #747: when the caller didn't supply the checker's semantic-type
         # side-tables, collect them here so a bare verify() matches the CLI
         # (cmd_verify) and LSP (VerificationSession) paths — both of which
         # thread them — keeping the warm/cold differential oracle and any
-        # external caller consistent.  Lazy import avoids a module cycle.
+        # external caller consistent.  A caller that supplies only *one*
+        # table still gets the other filled — an empty target table would
+        # silently under-fire the #747 generic-instantiation checks (CR
+        # #756).  Lazy import avoids a module cycle.
         from vera.checker import typecheck_with_artifacts
         _diags, _arts = typecheck_with_artifacts(
             program, source, file=file, resolved_modules=resolved_modules,
         )
-        expr_types = _arts.expr_semantic_types
-        expr_target_types = _arts.expr_target_types
+        if expr_types is None:
+            expr_types = _arts.expr_semantic_types
+        if expr_target_types is None:
+            expr_target_types = _arts.expr_target_types
     verifier = ContractVerifier(
         source=source, file=file, timeout_ms=timeout_ms,
         resolved_modules=resolved_modules,
diff --git a/vera/wasm/context.py b/vera/wasm/context.py
@@ -519,8 +519,10 @@ def translate_block(
                 # statically (Tier 3), or when codegen runs without
                 # `vera verify`.  The guard never trips on a provably-@Nat
                 # value, mirroring the #520 subtraction guard's
-                # belt-and-suspenders role.
-                if (type_name == "Nat"
+                # belt-and-suspenders role.  Alias-aware (`type Age = Nat`)
+                # via `_resolve_base_type_name` so an alias/refined @Nat let
+                # target is guarded too (CR #756).
+                if (self._resolve_base_type_name(type_name) == "Nat"
                         and self._narrows_into_nat(stmt.value)):
                     instructions.extend(
                         self._emit_nat_bind_guard(val_instrs))
diff --git a/vera/wasm/data.py b/vera/wasm/data.py
