The verifier currently checks the @Nat >= 0 invariant only at function return positions (test_int_to_nat_negative_caught: fn bad(...) -> @Nat { -1 } correctly fails verification) and via implicit Z3 constraints on @Nat parameters (test_nat_constraint_used: @Nat.0 >= 0 is asserted automatically). It does NOT check intermediate binding sites where an expression of broader type narrows into an @Nat-typed slot.

Concretely, after #520 + #551 close the unsigned-subtraction underflow holes, the remaining gap is:

private fn leaky(@Int -> @Int)
  requires(true)
  ensures(@Int.result == @Int.0)
  effects(pure)
{
  let @Nat = @Int.0 - 100;  // could be negative if @Int.0 < 100
  @Int.0                     // returns the parameter, not the bad let
}

The bad let @Nat = ... slips past the verifier because the @Nat-invariant check fires only at the function's return position. The let value's narrowing from @Int to @Nat is not obligation-checked. If the bad slot is later used in arithmetic, postcondition checks on the result might surface the violation — but only if the postcondition happens to depend on that path. Sites where the bad value silently flows into another expression propagate the invariant violation invisibly.

This is the architectural generalisation of #520 (subtraction is one specific site that violates the invariant) and #551 (@Byte subtraction).

Scope

Generalize the existing return-position invariant check to fire at every binding site that introduces an @Nat-typed slot from a broader-typed value:

• Let bindings: let @Nat = <Int expr>
• Function call arguments: f(<Int expr>) where f's formal parameter is declared @Nat
• Match arm pattern bindings narrowing to @Nat
• Other narrowing-to-@Nat sites the audit surfaces

Same Tier-3 fallback story as #520: when Z3 discharges the obligation, the binding compiles cleanly. When it cannot, codegen emits a runtime guard (if (val < 0) trap underflow) at the binding site.

Why follow-up rather than bundled with #520

#520 is scoped specifically to subtraction — the most common and most demonstrably-broken path. Path B is a verifier-architecture generalisation — broader scope, broader test surface, broader audit of every place a fresh @Nat slot enters scope. Splitting keeps each PR reviewable and lets the subtraction fix ship while the architectural piece gets thought through.

Open design questions

1. Symmetric coverage for @Byte? Same invariant problem (0..=255 violations). Probably yes — bundle into this issue rather than a separate sibling.
2. Refinement types more generally? type PosInt = { @Int | @Int.0 > 0 } has the same shape — narrowing into a refined slot should also obligate. Should this issue cover refinement narrowing or stay scoped to built-in unsigned types?
3. Performance: emitting an obligation at every @Nat binding site is a measurable Z3 load increase on large programs. Worth profiling on the conformance suite once a draft exists.

Acceptance

• Programs that introduce @Nat-typed slots from @Int expressions get a verifier obligation val >= 0 at the binding site (let / arg / match-bind).
• Existing tests still pass (return-position machinery is preserved, not duplicated).
• Conformance test demonstrating the canonical "narrow to @Nat with explicit requires" pattern.
• KNOWN_ISSUES.md / vera/README.md limitation entries removed once this lands.

Related

• Nat subtraction silently underflows to negative i64 — refinement-type soundness hole #520 — @Nat subtraction silent underflow (parent — narrow case of this invariant gap)
• @Byte subtraction silent underflow (follow-up to #520) #551 — @Byte subtraction silent underflow (sibling — same shape, byte type)