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

Inline comments:
In `@SKILL.md`:
- Line 2276: Remove the claim that there is "one program per feature" in the
sentence about the conformance test directory, as this is factually incorrect.
Since several features (such as slot references, match expressions, and
contracts) map to multiple conformance programs, reword the sentence to
accurately describe that the 90 programs validate language features without
implying a strict 1:1 mapping between features and programs.

In `@spec/11-compilation.md`:
- Line 56: The ADT pattern matching syntax documentation uses an incorrect form
`Some(`@Nat.0`)` when the correct pattern syntax is `Some(`@Nat`)` without the
index; the dotted form `.0` should only appear when referencing the bound value
in the match arm body. Fix this in two locations: in spec/11-compilation.md
(line 56), replace `Some(`@Nat.0`)` with `Some(`@Nat`)` in the pattern example; and
in KNOWN_ISSUES.md (line 22), apply the same correction to the limitation row.
Both changes use the same substitution to align the documentation with actual
Vera pattern syntax.

In `@TESTING.md`:
- Around line 9-11: The overview section in TESTING.md shows 4,390 total tests,
but this conflicts with the actual count of 3,630 from the per-file breakdown
listed below it, a difference of 760 tests. Run the scripts/check_doc_counts.py
script to determine the authoritative test count and then update the test count
figure in the overview (the "4,390 across 36 files" entry) to match the correct
total from the per-file breakdown, ensuring the documentation stays synchronized
with the actual test suite.

In `@tests/test_verifier.py`:
- Around line 764-775: The test function test_let_narrow_unguarded_fails and
similar narrowing-failure test functions currently only assert the error message
text ("may be negative") but do not explicitly verify the error code. Modify
each test function to include an explicit assertion that error_code == "E503" in
addition to the message text check, ensuring the diagnostic error code is
validated and the test will fail if the error code changes while keeping similar
wording. This applies to all similar test functions that check narrowing-related
failures.

In `@vera/README.md`:
- Line 690: In the verification gaps table on line 690 of vera/README.md, revise
the description of `@Nat` narrowing through ADT sub-pattern binds and non-literal
tuple destructures. Change the language from describing it as "unchecked" to
describing it as a "static-verification gap" instead. This is more accurate
because these bindings still receive Tier-3 runtime guards during codegen in
vera/wasm/context.py and vera/wasm/operators.py; the issue is that the verifier
cannot discharge them statically, not that they lack runtime protection
entirely.

In `@vera/verifier.py`:
- Around line 1479-1491: The binding pattern arm check in the match statement at
line 1489 (_check_nat_binding_obligation call) does not account for earlier arms
that may have already excluded certain cases from reaching this binding arm. To
fix this, collect the patterns from all previous arms processed before the
current binding pattern arm, create a condition representing the negation of the
disjunction of those patterns (Not(Or(previous_patterns))), and include this
condition in the assumptions when calling _check_nat_binding_obligation.
Additionally, apply the same negation condition to the arm body walk for
binding-pattern arms to ensure the arm is checked under the actual reachability
conditions determined by the ordered match semantics.
- Around line 1341-1355: The constructor field type checking in the
`_is_nat_type` method call only recognizes concretely resolved Nat types and
misses generic constructor fields (type variables) that are instantiated as Nat
at the call site, allowing Int arguments to bypass E503 obligations. To fix
this, either resolve the constructor field type (field_ty) through the call-site
type instantiation/context before checking if it is Nat in the _is_nat_type
condition, or alternatively emit a conservative Tier-3 nat_bind obligation by
calling _check_nat_binding_obligation even for generic fields to ensure a
runtime guard backs the obligation for common patterns like Option<Nat> and
Result<Nat, E>. Apply whichever approach your design prefers around the existing
_lookup_constructor_info and field_types access in the constructor call handling
block.
- Around line 1821-1823: The current check in the return statement only detects
top-level BinaryExpr with SUB operation, missing nested subtractions like (0 -
1) + 0 or if-else branches containing unproven subtraction. Create a new
recursive helper method (e.g., _contains_unproven_subtraction) that recursively
checks if a value or any of its sub-expressions contains a subtraction without
Nat origin by examining child nodes of BinaryExpr, conditional expressions, and
other composite nodes. Replace the current three-line check with a condition
that uses _is_nat_typed(value) and calls this new recursive predicate to
properly detect unproven subtraction at any nesting level.
- Around line 1506-1507: The fallback return statement at the end of the Nat
binding walker function skips recursion into expression containers like
ast.ArrayLit, causing nested narrowings to be missed. Before the default return
statement, add explicit branches to handle expression container types that can
hold child expressions. For each container type (such as ast.ArrayLit and
similar expression containers), recursively walk their child expressions using
the appropriate binding walker methods before falling through to the default
case.
- Around line 1421-1438: After the literal tuple destructure check completes in
the ast.LetDestruct branch, the destructured bindings are never added to
cur_env, causing subsequent narrowing obligations to refer to stale outer
bindings instead of the newly destructured values. Following the
_check_nat_binding_obligation call for each matching nat type binding, push the
destructured bindings into cur_env so that later code referencing those slots
uses the correct values from the destructure rather than the original outer
scope bindings.

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

Inline comments:
In `@tests/test_verifier.py`:
- Around line 1032-1051: The test_adt_subpattern_bind_not_obligated_yet method
currently only asserts the absence of nat_bind obligations in the result, but
does not verify that the overall verification succeeds with no errors. Add an
explicit assertion to check that the result object contains no errors (examine
the result object structure to determine the appropriate attribute or method to
check for errors). This strengthens the test to fully pin the current successful
verification behavior, ensuring that if the verifier fails through a different
diagnostic path in the future, the test will catch it rather than passing
silently.

---

Outside diff comments:
In `@ROADMAP.md`:
- Around line 23-24: The `#747` row in ROADMAP.md describes the narrowing
limitations too narrowly compared to what is documented in KNOWN_ISSUES.md.
Expand the `#747` row description to include generic constructor fields
instantiated to `@Nat` as an additional uncovered case alongside the currently
mentioned ADT sub-pattern binds and non-literal tuple destructures, ensuring
both documents align on the actual scope of the limitation.

In `@vera/verifier.py`:
- Around line 1366-1371: The handling of QualifiedCall expressions in
_walk_for_nat_binding_obligations is incomplete. Before recursing into the
arguments, the code must first resolve the operation's signature and check
whether the formal parameter types require narrowing (such as a Nat parameter).
Apply the same narrowing and obligation checking logic to the formal types of
the qualified operation before processing the arguments, so that E503
obligations are properly emitted for operations like IO.sleep that expect
specific parameter types.
- Around line 1269-1283: The `_lookup_constructor_info()` method currently only
searches `self.env` for constructors, but imported ADT constructors are
registered in resolved-module registries that are not being checked. Extend the
method to also search through the constructor registries from resolved/imported
modules after checking `self.env.lookup_constructor()` and
`self.env.data_types`, ensuring that imported constructors with concrete fields
are included in the lookup for proper type-checking and E503 obligation
validation.
- Around line 1622-1643: The code in the nat_bind checking block (both in the
`val is None` case and the solver timeout case) records obligations as
tier3_runtime for all binding sites, but runtime guards only exist for `let`
bindings. Before recording as tier3_runtime in both locations where
self.summary.tier3_runtime is incremented, add a check to determine if this is a
`let` binding. For non-let sites (call arguments, constructor fields, match
binds), either emit a diagnostic/warning instead of recording as tier3_runtime,
or skip the tier3_runtime recording altogether and handle unguarded non-let
failures differently to avoid marking unproved narrowings as runtime-covered
when no guard actually exists at compilation time.

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

Inline comments:
In `@tests/test_verifier.py`:
- Around line 1139-1153: The test_effect_op_argument_narrowing_caught method
only covers the error case where IO.sleep receives a negative `@Int` value. Add a
companion test method (such as test_effect_op_argument_narrowing_discharged)
that verifies the positive case where the same narrowing operation succeeds
cleanly. This companion test should use the same function structure and IO.sleep
call with `@Int.0`, but add a requires guard that ensures the value is
non-negative (e.g., requires(`@Int.0` >= 0)) so that verification passes, ensuring
regressions are caught if the narrowing binding site becomes overly
conservative.

---

Outside diff comments:
In `@TESTING.md`:
- Line 199: The pytest parametrized test count in the heading is stale and does
not match the updated conformance-suite table. Update the test count from 445 to
450 in the line "# Via pytest (parametrized — 445 tests)" to maintain
consistency with the table reported above. Verify that all other literal test
count references in the file are also synchronized with the current
conformance-suite numbers.

In `@vera/verifier.py`:
- Around line 327-334: The _register_effect() method currently initializes
operations as an empty dictionary, which means user-defined effect operations
are not registered with their OpInfo entries. This causes lookup_effect_op() to
be unable to access param_types for user-defined operations, allowing E503
narrowing checks to be bypassed. Refactor _register_effect() to mirror the
pattern used in _register_ability() by iterating through the operations declared
in the effect declaration (decl.operations) and populating the operations
dictionary with OpInfo entries for each operation, including their param_types
information.

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

Inline comments:
In `@tests/test_verifier.py`:
- Around line 1168-1185: Add a companion test method after
test_user_effect_op_argument_narrowing_caught that verifies the passing path for
user-declared effect operation argument narrowing. Create a new test using
_verify_ok (instead of _verify_err) with the same effect E definition and
function f structure, but add requires(`@Int.0` >= 0) to the function to satisfy
the non-negativity constraint for the E.wait(Nat) parameter. This ensures that
when the narrowing requirement is properly discharged, the code verification
succeeds, catching any regressions that might make the compiler
over-conservative at user-declared effect-op sites.

In `@vera/verifier.py`:
- Around line 343-348: Generic effect-op formals are not being instantiated
before the _is_nat_type check, allowing invalid operations on concrete effect
instances. When processing operations in the op registration logic (around
verifier.py lines 343-348 and 1389-1394), resolve the operation signatures
(param_types and return_type) through the enclosing function's effect-row
instantiation to replace any TypeVar formals with their concrete types before
testing _is_nat_type on those formals. This ensures that when a generic effect
like E<T> with operation wait(T -> Unit) is instantiated as E<Nat>, the formal T
is resolved to Nat before the `@Nat` type check occurs.

---

Outside diff comments:
In `@vera/verifier.py`:
- Around line 1457-1488: The code only pushes destructured slot bindings to
cur_env when the destructure source is a literal constructor call (when
isinstance(stmt.value, ast.ConstructorCall) and stmt.value.name ==
stmt.constructor is true), leaving stale outer bindings in cur_env for
non-literal sources like field accesses. This allows verification against an old
constrained value while codegen uses the destructured field. After the
conditional block that handles literal sources, add logic to handle non-literal
destructures by pushing conservative bindings or accessor terms for all
destructured slots in stmt.type_bindings, or alternatively prevent subsequent
statement checking from using the stale cur_env by resetting it or using a
separate environment for the non-literal case.

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

Inline comments:
In `@tests/test_verifier.py`:
- Around line 1314-1330: The test_user_effect_op_argument_narrowing_discharged
test currently uses _verify_ok(...) which only checks for the absence of errors,
but does not verify that the nat_bind obligation was actually discharged. This
can mask regressions in user effect-op formal resolution. Replace the
_verify_ok(...) call with a stronger assertion pattern that verifies the
nat_bind status is ["verified"], following the same pattern demonstrated in the
tests around line 1291-1293. This ensures the test explicitly confirms the
narrowing logic is working as intended, not just that the code happens to
compile.

In `@vera/verifier.py`:
- Around line 1466-1468: The comment at lines 1466-1468 incorrectly states that
a non-literal source "degrades to the runtime guard". Update this comment to
accurately reflect that non-literal destructures are not runtime-guarded at
codegen time—only the canonical `let `@Nat` = ...` site has runtime guard
protection. The implementation below only freshens slots for non-literal
sources. Clarify that this represents gap `#747` and is not protected at codegen
time, so future changes do not make incorrect assumptions about runtime guard
coverage.

---

Outside diff comments:
In `@vera/verifier.py`:
- Around line 1459-1463: When translate_expr returns None for a let statement's
value (untranslatable expression), the current code does not update cur_env,
allowing later slot references to incorrectly resolve to stale outer bindings.
Handle the None case by still extracting the type_name using
_type_expr_to_slot_name on stmt.type_expr and pushing a fresh slot variable to
cur_env instead of the translated val. This ensures that even untranslatable let
bindings create new environment entries, preventing false resolution to outer
scope bindings that could incorrectly discharge E503 errors.
- Around line 1355-1356: The check for Nat type narrowing in the loop iterating
through expr.args and param_types does not instantiate generic TypeVars that may
be fixed to Nat by the call context or surrounding type information. Before the
loop that zips expr.args with param_types, instantiate param_types to resolve
any generic TypeVars based on the actual call context, ensuring
_is_nat_type(formal) can correctly identify Nat types in generic functions
(e.g., where T=Nat in collection-style APIs). Alternatively, if full
instantiation is not feasible, defer the narrowing check for generic function
formals to match the existing deferral/test coverage applied to generic
constructor fields and effect-op formals.