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 `@spec/11-compilation.md`:
- Line 56: The paragraph at the specified location mentions that the
effect-operation argument guard gap and the use of generic trap reporting
instead of a dedicated trap kind are deferred to issue `#754`, but section 11.17
(the limitations summary section) currently concludes with "No open
limitations." You need to update section 11.17 to either add a list of these
residual limitations (specifically the effect-operation binding site guard gap
and the generic trap reporting limitation) or modify the closing statement to
acknowledge that there are still open limitations tracked in `#754` rather than
claiming no limitations remain.

In `@TESTING.md`:
- Line 62: In the TESTING.md file on line 62, within the test_verifier.py row,
locate the `#749` section that mentions "IndexExpr/InterpolatedString
container-recursion pins" and replace the term "container-recursion" with
"walker-recursion" to accurately reflect how PR `#749` describes these pins. This
correction ensures the coverage note accurately represents the recursion type
being tested rather than using misleading terminology.

In `@tests/test_verifier.py`:
- Around line 2418-2436: The test test_imported_ctor_generic_field_nat_obligated
currently only verifies the violated case where a generic constructor field
instantiation fails the obligation. Add a companion test method that checks the
discharged/satisfied case by using a requires clause that actually satisfies the
obligation (such as requires(`@Int.0` >= 0) instead of requires(true)), and verify
that the obligations list contains zero violated entries in this case. This
ensures regression coverage for imported generic-field instantiation so it is
not always treated as violated.

In `@vera/codegen/registration.py`:
- Around line 39-46: The code in the `_fn_nat_params` assignment only recognizes
direct `NamedType("Nat")` instances but does not resolve type aliases or
refinements that ultimately resolve to `Nat`. For each parameter in
`decl.params`, resolve the parameter type through any aliases or refinements
first before checking if it equals `Nat`, then use that resolved type in the
tuple comprehension instead of just checking the raw parameter directly. Apply
the same fix to the similar code handling `nat_fields` around line 269.

In `@vera/verifier.py`:
- Around line 1951-1953: When scrutinee_z3 is None in the conditional block
where lit_args is also None, the current code silently returns and loses the
narrowing obligation for `@Nat` field bindings. Instead of returning early, record
a Tier-3 nat-bind outcome at the match or sub-pattern site to ensure the
runtime-guarded narrowing is captured in diagnostics and the verification
summary. This ensures that unprojectable sub-pattern narrowings are properly
tracked rather than being dropped.
- Around line 533-535: The constructor harvesting loop (iterating through
adt.constructors.items() and adding to _module_constructors with setdefault) is
collecting all constructors from all modules without filtering for visibility or
import status, causing the wrong constructor variant to be used when multiple
modules define constructors with the same name. Apply the same
public/import-name filtering logic that is used for functions when adding
constructors in this loop, or alternatively change the dictionary key structure
from a bare ctor_name to include the resolved module and declaration context so
that lookups can correctly disambiguate between constructors with identical
names from different modules. Look for how function filtering is implemented
elsewhere in the verifier to apply the same pattern to constructor filtering.
- Around line 2032-2035: The `_record_nat_bind_tier3()` method expects the
caller to have already incremented `summary.total` by one before the call, as it
subtracts one for unguarded sites. The direct call to `_record_nat_bind_tier3()`
in the tuple destructure case (when sort is None or idx is None) is missing this
prerequisite increment. Add an increment to `summary.total` by one immediately
before calling `_record_nat_bind_tier3()` to ensure the method's internal logic
correctly nets out the obligation count instead of corrupting the summary.
- Around line 1687-1694: The call to `_obligate_subpattern_narrowings()` in the
constructor pattern arm is being executed before the pattern condition
(pat_cond) is added to the SMT solver's path conditions, which allows Z3 to
consider invalid cases and produce false E503 failures. Ensure that the
`_obligate_subpattern_narrowings()` call is wrapped within the same
constructor-pattern guard condition that is used to protect the arm body proof,
so that pat_cond is already present in smt._path_conditions when the sub-pattern
field obligations are proven.

---

Outside diff comments:
In `@vera/codegen/registration.py`:
- Around line 168-172: The MdHeading built-in type defined in the
_register_builtin_adts function is missing the nat_fields metadata parameter in
its ConstructorLayout definition. The MdHeading type has a Nat field (i32_pair
at offset 16) that requires runtime narrowing guard logic, but without
nat_fields metadata this guard won't be applied. Add the nat_fields parameter to
the MdHeading ConstructorLayout to specify which fields contain Nat values,
similar to how nat_fields generation is handled for user ADTs starting at line
255. This ensures that Nat fields are properly guarded at runtime for built-in
types just as they are for user-defined types.

In `@vera/verifier.py`:
- Around line 2063-2072: The current code treats all non-let-binding sites as
tier3_unguarded E504, but the guard plumbing now covers additional
runtime-guarded sites: call arguments, constructor fields, tuple destructures,
match bindings, and ADT sub-pattern extraction. Update the conditional logic in
the else block to explicitly check for these runtime-guarded sites and increment
tier3_runtime with a tier3_runtime status (similar to the let binding case),
rather than treating them as unguarded E504. Only effect-operation arguments
should remain as the unguarded E504 case. You will need to modify the condition
structure to check for specific site values corresponding to call arguments,
constructor fields, tuple destructures, match bindings, and ADT sub-pattern
extraction before falling back to the unguarded behavior.

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

Outside diff comments:
In `@vera/verifier.py`:
- Around line 97-108: The condition at line 97 only collects artifacts when both
expr_types and expr_target_types are None, but this causes issues when a caller
supplies only one of these tables and leaves the other as None, resulting in the
missing table being silently set to an empty dictionary in ContractVerifier.
Change the condition to check if either expr_types is None OR expr_target_types
is None, then after calling typecheck_with_artifacts, conditionally populate
only the missing tables: if expr_types is None, set it to
_arts.expr_semantic_types, and if expr_target_types is None, set it to
_arts.expr_target_types.
- Around line 2076-2084: The docstring and warning message for the Tier-3
nat_bind outcome handling contains contradictory information. While comments at
lines 1458-1460 and 2029-2030 indicate that codegen guards
projection/destructure sites at runtime, the current message in this section
states the narrowing "is not runtime-guarded" and "neither statically proven nor
runtime-checked", which contradicts the runtime guard coverage. Revise the
warning message to either split the explanation by site type (distinguishing
guarded let sites from unguarded non-let sites with appropriate messaging for
each) or reword it to accurately describe the static E504 gap without falsely
claiming these sites lack runtime guards when they actually do have them for
certain site types.

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 2465-2467: The test is currently only asserting that no `nat_bind`
obligations are violated, but it does not verify that a `nat_bind` obligation
with verified status actually exists. Add an additional assertion that
explicitly checks for the presence of at least one obligation where the kind is
"nat_bind" and the status is "verified". This should be done alongside the
existing assertion that checks for no violated nat_bind obligations to ensure
the regression test properly validates that the discharged path both emits and
verifies the nat_bind obligation as intended.

In `@vera/verifier.py`:
- Around line 2014-2016: The calls to _record_nat_bind_tier3() for ADT
sub-pattern bind and tuple-destructure sites (found in the methods handling
these patterns around the referenced lines) incorrectly treat these
codegen-guarded projection sites as unguarded, causing false E504 errors. Modify
these _record_nat_bind_tier3() calls to skip recording effect-operation
arguments through this path, or add a parameter to indicate these sites are
codegen-guarded rather than unguarded. Ensure that effect-operation arguments
are not downgraded to tier3_unguarded at these guarded projection sites, keeping
them on the unguarded path until the deferred runtime guard implementation is
complete.
- Around line 537-549: The condition at line 547 that checks if ctor_name is in
name_filter does not account for selective imports of data type names
themselves. When a data type name like List is imported via selective import,
its constructors should automatically be available. Modify the condition from
checking only if ctor_name is in name_filter to also check if adt_name (the
parent data type) is in name_filter, so that importing a data type declaration
via its name makes all of its constructors available in _module_constructors
through the setdefault call.

---

Outside diff comments:
In `@ROADMAP.md`:
- Line 23: Update the row for issue `#747` in ROADMAP.md to remove stale
information. The current text incorrectly states that the Tier-3 runtime guard
backs only the `let` site and that imported-constructor lookup is still needed.
Replace this outdated content to accurately reflect that these have been
addressed, and specify that the only remaining runtime gap is now the
effect-operation argument, which is tracked in issue `#754`. Ensure the updated
text aligns with the current PR summary and the latest spec documentation.

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 `@vera/verifier.py`:
- Around line 126-136: The _record_nat_bind_tier3() function currently
classifies all Tier-3 narrowings for "call argument" and "constructor field"
sites the same way, treating both concrete and generic-instantiated forms as
unguarded and reporting them as E504. However, concrete `@Nat` function formals
and constructor fields are actually runtime-guarded by codegen and should be
distinguished from the generic-instantiated value-flow cases that remain
unguarded. Modify _record_nat_bind_tier3() to accept and pass a runtime_guarded
parameter that should be True for concrete forms and False for
generic-instantiated forms and effect-operation arguments, ensuring the correct
distinction is preserved when reporting narrowing issues.
- Around line 2090-2099: The current code records only one Tier-3 obligation for
unprojectable tuple component narrowing, but when a tuple contains multiple `@Nat`
components, each should be counted separately to match the behavior of the
literal and projectable paths. Modify the code to iterate through the components
in the narrowing constraints and record or count a Tier-3 obligation for each
`@Int` -> `@Nat` narrowing found, rather than recording just once. This ensures that
let Tuple<`@Nat`, `@Nat`> = opaque_tuple() correctly counts both Nat components as
guarded runtime obligations instead of undercounting.

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

Inline comments:
In `@CHANGELOG.md`:
- Line 13: The arithmetic in the ruff findings summary is incorrect. Locate the
text "~176 findings had accumulated silently" in the CHANGELOG entry and change
the approximate total from "~176" to "~175" to accurately reflect the sum of the
134 auto-fixed findings and 41 hand-triaged findings that are explicitly
mentioned in the same entry.

In `@HISTORY.md`:
- Line 3: The roll-up footer line in HISTORY.md is out of sync with the header
statement. The header indicates 77 active development days, but the footer still
reports 76 active days and 173 tagged releases. Update the footer line to change
the active development days count from 76 to 77 to match the header.
Additionally, verify that the tagged releases count of 173 in this footer
matches the releases figure in README.md to ensure the two files remain
synchronized per coding guidelines.

In `@TESTING.md`:
- Line 62: In the test_verifier.py row within the `@Nat` binding-site narrowing
obligation section, the phrase describing which narrowings surface the E504
unguarded warning currently mentions both effect-op-arg and generic-instantiated
narrowings. Since `#747` now covers generic-instantiated `@Nat` formals, remove the
reference to generic-instantiated narrowings from the residual warning note,
leaving only the effect-op-arg scope that is tracked in the `#754` PR objective.

In `@tests/test_codegen.py`:
- Around line 16533-16547: The `_body` method uses plain substring matching with
`wat.find(f"(func ${fn}")` which can incorrectly match similarly-prefixed WAT
symbols (e.g., matching `$gcall_helper` when searching for `$gcall`). Replace
the substring find calls with a boundary-safe regex pattern that matches the
function name with word boundaries to ensure you only extract the correct
function body. Use regex to search for the opening function definition pattern
and closing boundary in a way that prevents false matches on similarly-named
symbols.

In `@tests/test_verifier.py`:
- Around line 2431-2445: The test method
test_imported_ctor_concrete_nat_field_discharged is not pinning down that the
nat_bind obligation is actually emitted and verified. Currently it only asserts
the absence of violated nat_bind obligations and error diagnostics, which means
the test would pass even if no nat_bind obligations were emitted at all. Add an
assertion to verify that at least one nat_bind obligation with status equal to
"verified" exists in result.obligations, similar to how the generic discharged
companion test handles this, to ensure the test catches real compiler behavior
rather than just the absence of failures.

In `@vera/codegen/registration.py`:
- Around line 277-303: The _type_resolves_to_nat method resolves alias bodies by
name only without applying type argument substitution, so generic aliases like
type Id<T> = T used as Id<Nat> resolve to T instead of Nat. When retrieving the
alias from self._type_aliases.get(te.name) and before assigning it to te for the
next loop iteration, check if te (the NamedType) has type arguments, and if so,
apply those type argument substitutions to the alias body before using it. This
ensures that generic type aliases with concrete type arguments are properly
resolved to their instantiated types rather than their unsubstituted template
forms.

In `@vera/verifier.py`:
- Around line 97-108: The condition checking whether to recompute artifacts uses
AND operator to verify that both expr_types and expr_target_types are None, but
it should use OR to check if either one is missing. Change the condition from
expr_types is None and expr_target_types is None to expr_types is None or
expr_target_types is None. Additionally, after calling typecheck_with_artifacts,
selectively assign only the missing tables by adding conditional checks: assign
expr_types from _arts.expr_semantic_types only if expr_types is None, and assign
expr_target_types from _arts.expr_target_types only if expr_target_types is
None. This ensures that partially-provided tables are completed consistently and
`#747` narrowing checks fire correctly.

In `@vera/wasm/data.py`:
- Around line 218-225: The runtime guard detection at lines 224, 454, and 569
uses a simple string comparison `type_name == "Nat"` which fails to detect Nat
aliases and refinement-wrapped Nat types, leading to missed guards. Replace the
direct `type_name == "Nat"` checks with an alias-aware Nat detection method that
properly resolves aliases and refinement types, similar to how constructor and
call metadata paths already handle Nat detection. Apply this change consistently
across all three guard emission sites where `_emit_nat_bind_guard` is called.

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 `@ROADMAP.md`:
- Line 11: There is a discrepancy between the test count reported in ROADMAP.md
(line 11 shows 4,443 tests) and the test count in README.md's project-status
section (which shows 4,436 tests). Verify the actual current test count from the
live test suite, then update both ROADMAP.md and README.md to reflect the same
correct count, ensuring consistency across all documentation references to test
totals.

In `@spec/06-contracts.md`:
- Line 248: The final sentence describing which cases surface E504 warnings is
ambiguous about unguarded narrowing sites. The sentence currently mixes
effect-operation arguments and generic formals/fields in a way that suggests the
latter only applies when `@Nat` erases to i64, but both are actually separate
residual classes that surface E504. Revise the sentence to explicitly call out
two distinct unguarded classes: effect-operation arguments as one site-kind
residual, and generic-instantiated formals/fields as a separate residual, making
clear both surface E504 warnings independently rather than treating them as
conditionally related.

In `@spec/11-compilation.md`:
- Line 596: The section summary in §11.17 currently states that only the
effect-operation argument is an uncovered binding site for the `@Nat` >= 0
narrowing invariant, but the detailed coverage in §11.2.1 identifies an
additional residual: generic-instantiated `@Nat` formals and fields on the E504
path are also left uncovered. Update the summary in §11.17 to reflect both
residuals tracked in issue `#754` rather than just the effect-operation argument
site-kind gap, ensuring the summary accurately represents all coverage gaps
documented in the detailed sections.

In `@tests/test_codegen.py`:
- Around line 16552-16571: The guard-shape assertions in
test_param_destructure_nat_components_guarded and
test_subpattern_nat_bind_guarded are incomplete. Currently each test only
asserts the presence of "i64.lt_s" in the compiled WAT output, but this can miss
regressions where the comparison is emitted without the trap edge. Strengthen
each assertion by adding an additional check for "unreachable" in the same WAT
body, ensuring both the comparison instruction and the unreachable trap
instruction are present together, which verifies the complete guard
implementation.
- Around line 16572-16579: The test_toplevel_match_nat_bind_guarded test only
verifies the structural WAT output by checking for the presence of the i64.lt_s
instruction, but does not test runtime trapping behavior. Add a runtime
negative-input test case that calls the gmatch function with an invalid input (a
negative integer that violates the `@Nat` guard constraint) and verifies that the
function traps or raises an exception at runtime. This ensures that the
narrowing and guard semantics are actually enforced during execution, not just
present in the compiled code structure.

In `@vera/codegen/registration.py`:
- Around line 271-275: The nat_fields tuple in manually registered concrete-Nat
built-ins like MdHeading is not being populated and remains as an empty default
tuple, which prevents the proper validation guards from being applied during
constructor emission. Identify where manual built-in layouts are being
registered (look for explicit ConstructorLayout instantiations outside of
_compute_constructor_layout), and for those layouts that have concrete Nat
fields (such as MdHeading with its first Nat field), populate the nat_fields
parameter with a tuple containing the indices of the Nat-type fields instead of
leaving it empty, ensuring the i64.lt_s/unreachable guard is properly generated
to prevent invalid negative values from being stored as Nat.

In `@vera/README.md`:
- Line 690: In the README.md file within the "Verification gaps that downgrade
silently" table row, the issue references `#754` and `#730` do not exist in the
aallan/vera repository. Remove these non-existent issue references or replace
them with verified tracking issue numbers if they exist. Verify that `#555`
remains correctly referenced as it is documented in KNOWN_ISSUES.md and tracks
the generic forall body verification gaps mentioned in the row description.

In `@vera/verifier.py`:
- Around line 1468-1481: The comments at the projection site handling (around
the ADT sub-pattern bind and non-literal tuple destructure discussion) describe
outdated behavior where non-let Tier-3 paths were not runtime-backed. Update
these comments to reflect that the current implementation records guarded tuple
destructure, match-bind, and ADT sub-pattern fallbacks as tier3_runtime by
passing guarded=True. Clarify that these paths are now treated as
runtime-backed/guarded in the current accounting scheme, rather than as
unguarded paths that become E504 errors. Apply the same updates to the related
comments also mentioned in the affected line ranges to maintain consistency
across all similar documentation.

---

Outside diff comments:
In `@ROADMAP.md`:
- Line 73: In the ROADMAP.md file, locate the `#749` row and remove the completed
items from it: the container IndexExpr/InterpolatedString test pins, the
_fresh_slot_var alias unit-test, and the _narrows_into_nat differential test.
Either trim the row to only include the dedicated trap-kind work if it warrants
separate tracking, or delete the entire `#749` row if the remaining work is
already captured in the related `#754` issue, following the guideline that
completed roadmap items should be removed once they land with residual work
tracked separately.

In `@vera/verifier.py`:
- Around line 1705-1749: When the scrutinee cannot be translated to Z3
(scrutinee_z3 is None), pattern bindings in match arms are not properly
shadowed, causing stale or missing bindings in downstream obligations. Add the
proposed _bind_fresh_pattern_slots method to the Verifier class to recursively
create fresh slot variables for BindingPattern and ConstructorPattern cases. In
the match expression handling where arm_env is initialized to slot_env, check if
scrutinee_z3 is None and call _bind_fresh_pattern_slots to update arm_env with
fresh pattern slots instead of leaving it as the outer slot_env, ensuring
pattern bindings are properly shadowed similar to how LetDestruct handles this
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 `@KNOWN_ISSUES.md`:
- Line 23: The final two sentences of this KNOWN_ISSUES row conflate static
compile-time obligations with runtime-unguarded sites, making it unclear which
failures occur where. Reorganize the text to clearly separate two distinct
issues: first, identify which specific sites have static obligations that
produce E503/E504 compile errors, then separately describe which different sites
remain runtime-unguarded in unverified compiles and would trip a generic
unreachable rather than the proper requires check. This separation will prevent
overstating what fails at compile time versus what still traps at runtime.

In `@spec/06-contracts.md`:
- Line 248: The paragraph currently presents the generic function-formal calls
guard as universally protective, but this needs qualification. Add a caveat to
the sentence discussing "generic function-formal calls, which guard on the
monomorphised callee" to acknowledge that while concrete guarded call-arguments
work reliably, generic-instantiated `@Nat` formals can still erase to i64 and
surface E504 errors when the expression is untranslatable, similar to the caveat
already noted for generic-instantiated constructor fields staying unguarded.

In `@spec/11-compilation.md`:
- Line 56: The paragraph describing the Tier-3 runtime guard coverage is
incomplete. Locate the sentence that currently states "The Tier-3 runtime guard
backs every binding site except the effect-operation argument" and expand it to
also exclude generic-instantiated constructor fields from having runtime guards,
since the verifier/codegen path leaves these unguarded. Update the sentence to
mention both the effect-operation argument and constructor-field residuals as
sites where the runtime guard does not apply, ensuring consistency with section
11.17 which already reflects this split.

In `@TESTING.md`:
- Line 62: The current description in the test_verifier.py row conflates the
guarded cases with all generic function-formal call-arg handling, making it
appear that all such cases are protected by the monomorphised callee guard.
Revise the text to explicitly separate the concrete guarded cases from the
residual path where untranslatable generic-instantiated formals and fields can
still erase to i64 and surface E504 warnings. Keep the unguarded residual path
explicit in the documentation rather than collapsing it into the guarded
description, ensuring readers understand that generic instantiation does not
universally prevent E504 emissions.