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/02-types.md`:
- Around line 253-255: The example using array_length in the refinement type
contradicts the specification because array_length is already listed as allowed
in the decidable fragment §2.6.1. Replace the array_length example with a
genuinely undecidable refinement predicate that actually falls outside the
decidable fragment, or alternatively rephrase the limitation description to
clarify that this is an unsupported lowering case rather than claiming the
refinement falls outside the decidable fragment. Ensure the example and
explanation are consistent with what is defined as permitted in §2.6.1.

In `@tests/test_verifier.py`:
- Around line 3661-3678: The test currently only asserts that at least one E506
warning exists but does not pin the expected count or verify there are no
errors. Tighten the assertion by replacing the generic check `assert warns,
"expected an E506 Tier-3 warning"` with a more specific check that verifies
exactly one E506 warning exists (using `len(warns) == 1`). Additionally, add an
assertion to verify that there are zero error diagnostics in the result object
to catch unexpected verifier errors that might otherwise be masked by the loose
assertion.

---

Outside diff comments:
In `@vera/verifier.py`:
- Around line 1560-1568: The `_nat_binding_target(arg, None)` calls in the
pipe/call/constructor/effect-op argument checking blocks miss refined targets
from desugaring and generic instantiation (e.g., TypeVar formals instantiated as
PosInt). Create a new refined analogue method (such as
`_nat_binding_target_refined`) that recovers refined targets from the checker
side-table, then replace or supplement the `_nat_binding_target` checks at all
four locations (in the pipe call block around line 1560, and the similar blocks
at lines 1599-1605, 1635-1641, and 1672-1678) with calls to this new method to
ensure E505/E506 errors are properly raised for refined instantiations.
- Around line 657-684: The early return statement in the decl.forall_vars branch
prevents refined return type verification from being performed on generic
functions. Add refined return type checking within the generic function handling
block before the return statement, ensuring that refine_bind results are emitted
for any refined return types in the function signature. When a refined return
type is present, record it as verified if it is translatable to Z3, otherwise
record it with error code E506 to prevent generic functions with concrete
refined returns from silently bypassing verification.
- Around line 1797-1802: The method _obligate_destructure_narrowings and related
code around lines 1905-1912 currently only call Nat-only helpers for handling
projection paths in non-literal destructures, missing refined type projections
for tuple and ADT pattern binds. Create a new term-based refined checker method
analogous to _check_nat_binding_obligation_term that handles refined projections
generally (not just Nat), then update _obligate_destructure_narrowings and the
constructor sub-pattern walkers to call this new method from the non-literal
destructure and constructor sub-pattern walkers to ensure refined type
obligations are generated for cases like let Tuple<`@PosInt`> = make_tuple(...)
and match opt { Some(`@PosInt`) -> ... }.

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 `@ROADMAP.md`:
- Around line 23-24: Remove the completed item `#746` (Refinement-type predicate
verification) from the ROADMAP.md file since it belongs in the completed items
history, not the forward-looking roadmap. Delete the entire row containing the
`#746` issue and its description about user refinement predicates from ROADMAP.md,
then add this completed item with its details to HISTORY.md to maintain an
accurate record of finished work.

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 3391-3441: The `_translate_refined_predicate` method currently
only injects an intrinsic invariant for `@Nat` (>= 0), but `@Byte` is also a
range-constrained primitive that needs similar treatment since it has bounds
0-255. After the existing check for `base == NAT` that returns
`z3.And(value_term >= 0, translated)`, add a similar check for `Byte` that
returns `z3.And(z3.And(value_term >= 0, value_term <= 255), translated)` to
ensure byte refinement predicates are checked against the correct SMT semantics
with the proper bounds constraint.
- Around line 998-1039: The verified refined return predicate from lines
998-1039 is only recorded locally and not propagated to callers, so when
`_translate_call_with_info` in smt.py translates a call to this function, it
strips the RefinedType constraint and leaves the fresh return value
unconstrained. After the refined return predicate is verified and recorded by
`_record_obligation` around line 1022, you need to ensure this constraint is
also added to the caller-side SMT assumptions when a function returning a
RefinedType is called. Either synthesize a call-site assumption that encodes the
verified refined predicate on the fresh call result, or add it as a modular
postcondition that the SMT translation layer can use when processing calls to
functions with verified refined return 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 `@CHANGELOG.md`:
- Line 13: The CHANGELOG.md entry contains two inaccuracies in the Tier-3
explanation section. First, correct the explanation that states Tier-3 warnings
are triggered by undecidable predicates like array_length - the actual reason
for Tier-3 is the non-primitive base type, not predicate decidability (the
array_length example is fine, but the reasoning is wrong). Second, clarify that
the runtime guard applies at every function boundary (refined parameters at
entry, refined returns at exit), not only at public/FFI boundaries - remove or
revise the parenthetical comment that suggests the guard only covers public/FFI
entry points.

In `@spec/02-types.md`:
- Around line 255-261: The Runtime Guards section currently states that the
compiler emits predicate checks only at public/FFI boundaries, but the actual
implementation emits guards at every function entry/exit. Revise the
documentation to clarify that refined parameters are checked at entry and
refined returns are checked at exit for all functions (not just public/FFI
boundaries), and that this broader scope provides more comprehensive coverage of
refinement violations. Update the relevant sentences in the paragraph to
accurately reflect that the guard applies universally at function boundaries
rather than limiting the statement to only public/FFI contexts.

In `@vera/codegen/contracts.py`:
- Around line 80-83: When translate_expr returns None for the predicate at the
guard creation point (where cond is None after calling
ctx.translate_expr(predicate, guard_env)), the code currently silently returns
None without any safeguard. Replace the silent return with a diagnostic emission
that indicates the refinement guard could not be lowered, then either skip
processing the function or raise an exception to fail closed. Apply this same
pattern to all other locations where refinement guards are created and
translate_expr is called (including the parameter guards handling), ensuring no
refinement boundary is left unguarded at runtime due to a failed predicate
translation.
- Around line 47-54: The current generic type formatting logic in the code that
builds arg_names for base.type_args only extracts the immediate type name
(ta.name) without recursively handling nested generics. This causes
Array<Option<Int>> to be formatted as Array<Option>, breaking predicate
resolution. Modify the logic that appends to arg_names to recursively format
nested type arguments: when processing each type argument ta, check if it has
its own type_args and recursively format them instead of just appending ta.name,
so the full nested structure like Option<Int> is preserved in the final name
string.

In `@vera/verifier.py`:
- Around line 2265-2282: The `_record_refined_bind_tier3()` method currently
increments `tier3_runtime` for all refined narrowing fallbacks, but this
conflates guarded sites (refined parameters at entry, refined returns at exit)
with unguarded sites (let bindings, destructures, match patterns, ADT fields,
effect arguments). To fix this, either add a `guarded` parameter to
`_record_refined_bind_tier3()` (mirroring the pattern used in
`_record_nat_bind_tier3()`) and only increment `tier3_runtime` when `guarded` is
True, or ensure codegen emits runtime guards for all local refinement sites.
Update all call sites to pass the appropriate `guarded` flag value based on
whether the refinement site has a corresponding codegen guard.

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 3936-3959: The "bad" case assertion is too loose, checking only
that at least one E505 exists without verifying the exact count or catching
spurious additional errors. In the
test_generic_concrete_refined_return_discharged method, replace the assertion
`assert errs, "expected E505 on the generic concrete refined return"` with a
tighter assertion that verifies exactly one E505 error exists and no other
error-level diagnostics are present. This should follow the pattern used in
test_non_primitive_base_is_tier3_e506, where the test asserts a specific count
of errors (e.g., `assert len([d for d in bad.diagnostics if d.error_code ==
"E505"]) == 1` and `assert [d for d in bad.diagnostics if d.severity == "error"]
== [<the E505>]`).

In `@vera/verifier.py`:
- Around line 2316-2341: The issue is that check_valid is being called with an
empty premise list, which means parameter predicates and requires clauses are
not being considered when validating the return type. To fix this, after setting
up the parameter variables in the loop over decl.params, collect the assumptions
from these parameters (their refined predicates) and any requires clauses from
the function declaration. Before calling smt.check_valid on the goal, pass these
collected assumptions as the second argument instead of the empty list, ensuring
the validity check properly seeds with the function's assumptions.

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_codegen.py`:
- Around line 5407-5424: The current test has a false positive because head([])
traps both due to the NonEmptyArray guard and due to the out-of-bounds indexing
when accessing `@NonEmptyArray.0`[0]. Modify the body of the head function to
perform an operation that would return normally for an empty array (such as
returning a default value without accessing the array, or checking the array
length), so that the test specifically demonstrates the refinement guard is
firing rather than just the indexing failing. This ensures the test proves the
guard is actually working as intended.

In `@vera/codegen/contracts.py`:
- Around line 228-234: The comment block explaining pair and array return guard
behavior is outdated and contradicts the current implementation. Update the
comment in the section starting with "# Pair returns (String/Array) don't
support general ensures checks" to correctly reflect that array refined returns
ARE now guarded by _refinement_guard_parts() when they have refinements, rather
than stating they get no guard. Remove or correct the statement about array
bases being non-primitive and getting no guard, as this no longer matches the
actual behavior demonstrated by test_array_return_guard_traps_on_empty.

In `@vera/codegen/functions.py`:
- Around line 198-217: The current code compiles preconditions first via
_compile_preconditions and then adds refinement parameter guards via the for
loop that processes value_local and param_te pairs. However, refinement guards
must execute before preconditions since a requires expression may depend on the
refined parameter invariant. Reorder the logic to collect refinement parameter
guards first (move the for loop before the _compile_preconditions call), then
compile the preconditions, and combine both sets of instructions with the
refinement guards appearing first in pre_instrs.

In `@vera/errors.py`:
- Line 504: The E506 error message currently states "not runtime-guarded" which
is inaccurate because E506 is raised for both guarded and unguarded Tier-3
refinement cases. Modify the error message string for E506 to remove the "not
runtime-guarded" claim and instead use guard-neutral wording that only describes
the core issue of unverified refinement narrowing, without making assumptions
about the presence or absence of runtime guards.

In `@vera/obligations/core.py`:
- Around line 68-73: The comment for tier3_unguarded contains outdated semantics
regarding E506 warnings for refinement narrowing. The current comment implies
that refine_bind refinement narrowing warnings only occur at sites with no
runtime guard, but the current refinement flow now emits E506 warnings for both
runtime-checked and non-runtime-checked Tier-3 sites. Update the comment to
accurately reflect that E506 can be emitted for refinement narrowing regardless
of whether a runtime guard is present, removing the outdated qualifier about "no
runtime guard yet".

In `@vera/verifier.py`:
- Around line 2351-2354: The Float64 parameter handling in the generic
refined-return path is incorrectly declaring float types as Int-sort variables
instead of Float64/Real-sort variables. In the conditional block starting with
`elif self._is_float64_type(param_ty):` around line 2351-2352, replace the
`smt.declare_int(z3_name)` call with the appropriate SMT float or real sort
declaration that matches the non-generic setup. This ensures that float values
like 0.5 are properly included in the refinement proof quantification.

---

Duplicate comments:
In `@spec/02-types.md`:
- Line 259: The explanation around line 259 incorrectly attributes the Tier 3
classification to Z3 being unable to decide array_length. Reword the rationale
to clarify that array_length(...) > 0 is actually in the decidable fragment and
remains decidable; the Tier 3 classification instead comes from the
non-primitive `@Array` binder not being lowered, which causes error E506, not from
array_length being undecidable. Update the text to accurately reflect that the
limitation is in the lowering of the `@Array` binder, not in the decidability of
the comparison predicate itself.

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 `@TESTING.md`:
- Around line 61-63: The markdown table in TESTING.md has unescaped literal pipe
characters (|) within the table cell content in the coverage descriptions for
test_obligations.py, test_verifier.py, and test_codegen.py rows, which causes
the markdown parser to treat them as cell delimiters and break the table
structure. Fix this by escaping each literal pipe character in the cell content
with a backslash (change | to \|), or alternatively move the long coverage
descriptions outside the table into separate paragraphs or a different structure
to keep the table properly formatted.

In `@tests/test_codegen.py`:
- Around line 5605-5619: The test method
test_nested_refinement_over_tuple_guard_traps currently only validates the
violating case where a negative value fails the refinement guard on the nested
Pair type. To ensure component recursion does not over-trap valid values, add a
happy-path assertion by creating an additional test case or check that passes a
valid nested tuple value (such as Tuple with a positive integer in the inner
Tuple) to the entry function and verifies it executes successfully without
trapping, ensuring the guard logic correctly handles valid nested refinement
paths.

In `@tests/test_verifier.py`:
- Around line 3963-3979: The test test_generic_refined_return_from_match_arm
covers the positive case with Option<PosInt>, but a matching negative case with
Option<Int> is needed to ensure soundness and prevent generic-specific bugs from
laundering unrefined payloads. Add a new test method that mirrors
test_generic_refined_return_from_match_arm but uses Option<Int> instead of
Option<PosInt> in the function signature, parameter matching, and return type to
verify that the generic refined-return fast path properly rejects unrefined
payloads and produces appropriate error diagnostics.

---

Outside diff comments:
In `@vera/codegen/contracts.py`:
- Around line 45-49: The while loop that walks through type aliases is directly
replacing the node with _type_aliases[node.name] without applying use-site
type_args substitution, causing refinement guards to work with unresolved alias
bodies instead of properly substituted types. Replace the current alias
resolution logic in this while loop with a call to the _resolve_type_alias()
method, which already handles proper type argument substitution. Apply the same
fix to the similar alias resolution code at lines 77-83 to ensure consistent
behavior and proper guard extraction across all alias resolution paths.

In `@vera/verifier.py`:
- Around line 865-866: The LetDestruct block processing in _translate_block
(vera/smt.py lines 1246-1267) does not inject destructured pattern source facts
before translating the block's body expression, unlike match arms which use
_subpattern_fact_hook to provide refined sub-pattern facts. To fix this, modify
_translate_block to extract and emit source facts from LetDestruct pattern
bindings (similar to how _subpattern_fact_hook injects facts for match arms at
lines 1273-1287) before calling smt.translate_expr on the block body at line 866
in verifier.py. This ensures invariants from destructured values (like `@PosInt`
from Tuple destructuring) are available in the SMT context during the initial
body translation pass, preventing false E501/E505 errors on dependent function
calls.

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/codegen/functions.py`:
- Around line 245-265: The guard emission order for refined-tuple parameters
needs to be reordered to ensure component refinements are established before
top-level predicates execute. In the code section around the refined-tuple
parameter handling in functions.py, locate where top-level predicate guards are
emitted before _emit_component_refinement_guards is called. Reorder the emission
sequence so that _emit_component_refinement_guards executes first to establish
the component refinements, followed by the top-level refined guards, and ensure
both guard emissions occur before any requires(...) call. This ensures that
predicates like P in patterns such as { `@Tuple`<NonZero, Int> | P } have access
to properly established component refinements when they execute.

In `@vera/verifier.py`:
- Around line 1726-1732: At tuple construction and destructure sites (around
lines 1726-1732, 1948-1952, and 2885-2888), before extracting type_args from
tuple types, unwrap any RefinedType wrappers by accessing the base property
first. When processing tuples that may be wrapped in RefinedType (like {
`@Tuple`<PosInt, Int> | P }), use RefinedType.base to get the underlying AdtType
before reading component types, ensuring component obligations are properly
tracked instead of being skipped due to the refined type hiding the actual tuple
base.
- Around line 2721-2724: The current sub-pattern handling in the loops at lines
2721-2724 and 2794-2824 only processes direct BindingPattern children and does
not recursively handle ConstructorPattern children, causing nested patterns like
Some(Some(`@PosInt`)) to miss inner refine_bind obligations and source facts.
Refactor the sub-pattern obligation and fact generation logic into a recursive
helper function that accepts the projected field term and declared field type as
parameters, then have this helper recursively process both BindingPattern and
ConstructorPattern children so that nested constructor patterns generate the
appropriate refine_bind obligations and source facts at each nesting level.

---

Duplicate comments:
In `@vera/codegen/contracts.py`:
- Around line 45-49: Apply generic alias substitution in the two guard-decision
walk functions at the specified locations, similar to how _resolve_type_alias()
handles type aliases. When processing generic type aliases like Id<T>, ensure
that type parameters are properly substituted so that base_node correctly
resolves to the concrete type (e.g., Nat instead of T). This will ensure that
implicit membership guards like the >= 0 check are properly included and prevent
invalid values like -1 from satisfying boundary checks.

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 3879-3880: Replace the loose `assert any(d.error_code == "E505"
for d in result.diagnostics if d.severity == "error")` assertions at both
locations with more precise checks that verify the exact count of E505 error
diagnostics and ensure no other unexpected error diagnostics are present.
Instead of just checking that at least one E505 exists, count the filtered
results (e.g., using `assert len([d for d in result.diagnostics if d.severity ==
"error" and d.error_code == "E505"]) == <expected_count>`) and separately assert
that the total error count matches expectations or that only E505 errors are
present in the error diagnostics to prevent false-positive passes from unrelated
error diagnostics.

In `@vera/verifier.py`:
- Around line 2732-2733: The depth guard using `_depth > 16` silently drops
obligations for deeper nested patterns by returning an empty list, which allows
legitimate pattern checking to be bypassed. Since the pattern AST is finite,
remove the depth cap check from the condition that includes `_depth > 16`,
allowing the obligation walk to continue at any depth. Alternatively, instead of
returning an empty list, emit an unguarded Tier-3 diagnostic to report the deep
nesting issue rather than silently ignoring it. Apply the same fix to the
similar condition also mentioned around lines 2779-2780.
- Around line 2881-2896: The nested constructor pattern recursion in the branch
checking `if sort is not None and idx is not None` only handles opaque path
cases but excludes literal constructor scrutinees where `lit_args` is set and
`sort` remains `None`. Add an additional condition to also recurse when handling
literal nested constructor arguments by checking if `lit_args` exists, and call
`_obligate_subpattern_term` with the appropriate literal argument accessor
instead of the sort-based accessor, ensuring the inner narrowing obligation is
verified for both opaque and literal nested constructors.

---

Outside diff comments:
In `@vera/codegen/contracts.py`:
- Around line 43-49: The manual type alias resolution in the while loop that
iterates through self._type_aliases drops generic type arguments, whereas the
_resolve_type_alias() method below preserves them. This causes issues with
generic refinement aliases like NonEmpty<T> losing their type parameters during
resolution. Replace the manual while loop that walks through self._type_aliases
with a call to _resolve_type_alias() instead. This same issue also appears in
another location (lines 77-83), so apply the same fix to both occurrences to
ensure generic type arguments are preserved for refinement guard decisions.
- Around line 110-129: The code currently handles Unit and Nat base types with
special guards in the boundary predicate check, but Byte type is not explicitly
handled and falls through with only the user predicate, allowing invalid values
outside the 0-255 range to pass. Add a new conditional block after the Nat
handling to detect when base_node is an ast.NamedType with name equal to "Byte",
and construct a BinaryExpr similar to the Nat case that conjuncts two range
checks (0 <= the slot reference AND the slot reference <= 255) with the existing
predicate, then return the combined predicate with the name tuple.

In `@vera/verifier.py`:
- Around line 2677-2680: In the _instantiated_field_types() function, the
isinstance check for AdtType fails for refined ADT scrutinees (like {
`@Option`<Int> | P }) because they are not direct AdtType instances. Before
checking if scrut_ty is an AdtType with type_args, unwrap the refined ADT base
from the scrutinee using the same logic that _is_adt_type() uses, then perform
the isinstance check on the unwrapped type to ensure refined ADT scrutinees are
properly handled for constructor field type instantiation.

---

Duplicate comments:
In `@vera/verifier.py`:
- Around line 1955-1960: The code extracting type_args from src_tuple_ty only
handles bare AdtType instances but misses refined tuple types like {
`@Tuple`<PosInt, Int> | P }. Before the isinstance check for AdtType in the block
starting at line 1955, unwrap any type refinements or constraints from
src_tuple_ty to expose the underlying tuple type, then extract type_args from
the unwrapped tuple type. This ensures component invariants are preserved when
seeding component facts and prevents false E505 errors during later re-narrowing
of the source value.