Verifier does not obligate @Nat->@Int widening in a nested closure's return (codegen over-guards soundly; reporting-completeness gap)

[aallan]

Summary

A closure defined inside another closure's body that widens @Nat into an @Int return is runtime-guarded by codegen (_compile_lifted_closure lifts and guards it) but not obligated by the verifier — the verifier's AnonFn widening handler is deliberately shallow: it does not recurse into a closure body, because translating there against the outer slot environment could mis-resolve a closure parameter and prove a false Tier-1.

Consequence: codegen over-guards (sound — an extra runtime trap on a real widening, never a false proof), but vera verify under-reports: the obligation stream carries no entry for the nested closure's widening, so the summary's Tier-3 count omits a runtime check that codegen actually emits, and the strict verifier↔codegen differential does not hold for the nested shape.

A reporting-completeness limitation, not a soundness hole — same family as #779 (obligation walkers stopping at fresh-scope bodies: closures / quantifiers / handler clauses).

Found during the #820 per-component metadata work (PR pending), which added the single-level closure argument/return/capture obligations and guards; the nested case is the residual.

[aallan]

The @Int → @Nat narrowing direction shares this exact gap, confirmed empirically while closing #984 (the closure-return narrowing obligation + per-leaf runtime guard).

#984 records the closure-return nat_bind obligation shallow-syntactically in the same AnonFn arm of _walk_for_nat_binding_obligations that #820 uses for the widening nat_to_int_coerce — and that arm is deliberately terminal (it does not recurse into the closure body, for the same false-Tier-1 reason described here). So a closure nested inside another closure's body has its narrowing @Int → @Nat return guarded by codegen (every lifted closure passes through _compile_lifted_closure, nested included) but carries no nat_bind entry in vera verify's obligation stream — the narrowing dual of the widening residual this issue already tracks.

Repro: a nested fn(@Int -> @Nat) { @Int.0 } reports 0 Tier-3 obligations from vera verify, yet vera run traps on a negative input (sound over-guarding, not a soundness hole). Both directions close together when the AnonFn walk gains a body recursion that resolves closure parameters against the closure's own slot scope rather than the outer env. Noting here so the narrowing dual is closed alongside the widening one; the KNOWN_ISSUES row for this issue now covers both directions.