Follow-up to #520 (scope expansion). Surfaced by CodeRabbit review on PR #554.

vera/verifier.py _verify_fn skips ALL static verification for generic (forall<T>) functions, returning early after recording E520 warnings for non-trivial contracts (line 421-438). This early return means _walk_for_subtraction_obligations (the #520 underflow walker) never runs on generic-function bodies, so an @Nat - @Nat site inside a forall<T> function will not produce E502 at verify time. The codegen runtime guard fires per-monomorphization, so the safety net is in place — but the static check is bypassed.

Why this is a real gap

A function like:

fn safe_decrement<T>(@Nat -> @Nat)
  requires(true)
  ensures(true)
  decreases(@Nat.0)
  effects(pure)
{
  if @Nat.0 == 0 then 0
  else @Nat.0 - 1
}

would emit E502 at verify-time today if it were non-generic, but with the unused <T> type parameter the verifier silently bails. An author who specialises this function via a concrete instantiation gets the runtime guard at compile time, but never sees the static obligation discharge / failure during vera verify.

Why this is non-trivial

The SMT context setup at lines 451-490 declares Z3 vars for concrete-typed params (declare_nat, declare_int, declare_bool, etc.). Type-variable parameters can't be declared as Z3 sorts (Z3 has no notion of type variables), so the existing convention bails before the setup. Two paths:

1. Skip-typevar approach: declare only concrete-typed params, run the walker; obligations involving TypeVar operands would fail to translate and silently drop to Tier 3 — inflates Tier-3 counts without catching anything new.
2. Special-case approach: extend the walker's _is_nat_typed / _has_nat_origin to recognise "concrete @nat slot ref even inside a generic function context"; deeper change to the helpers but avoids the Tier-3 inflation.

Approach (2) is the right shape but requires careful unit testing for false-positive regressions on functions where the TypeVar implicates the type system reasoning.

Convention note

The early return is consistent with how E520 / E521 / E523 / E524 / E525 all treat generic functions today. Extending E502 alone would deviate from that convention; doing it for all the other verifier checks at the same time would be a larger refactor (and arguably the right scope for a Tier 2 verification PR — see #427).

Acceptance

• A fn foo<T>(@Nat -> @Nat) body with @Nat.0 - 1 (no path-condition guard) emits E502 at vera verify time.
• Existing generic-function tests continue to pass (no false-positive E502s for type-variable-involving operands).
• Implementation chooses path (1) or (2) explicitly, with documentation of the trade-off.

Related

• Nat subtraction silently underflows to negative i64 — refinement-type soundness hole #520 — @Nat subtraction underflow (parent — verifier obligation is now in place but skips generics).
• @Byte subtraction silent underflow (follow-up to #520) #551 — @Byte subtraction underflow (sibling, also currently skips generics).
• Generalize @Nat invariant check to all binding sites (broader generalisation of #520) #552 — @Nat invariant check at every binding site (broader generalisation).
• Implement Tier 2 verification (Z3-guided with hints from assert/lemma) #427 — Tier 2 verification (broader fix would generalise the convention).