Two low-value residuals deferred from the #747 / #749 @Nat-narrowing generalization (feature PR for v0.0.173). Neither is a correctness gap — both sites are obligated statically by the verifier, and the runtime guards that exist trap correctly (localized by the #516 source frame).

1. Effect-op-argument runtime guard

#747 extended the runtime value >= 0 guard to five of the six @nat binding sites (tuple destructure, top-level match bind, ADT sub-pattern, concrete constructor field, call argument). The effect-op-argument site (E.op(@Int.0) into a concrete @nat formal) is the one left unguarded: _effect_ops in codegen carries only the dispatch target, not the op's formal types, so a concrete-@Nat-formal check would need a new op-parameter registry threaded across the handler-dispatch path (both the unqualified _translate_call and qualified _translate_qualified_call loops in vera/wasm/calls.py). It is the rarest narrowing site, already obligated statically and flagged E504 when Tier-3.

2. Dedicated @Nat-guard trap kind (was #749 item 4)

_emit_nat_bind_guard emits a bare unreachable, classified generically by _classify_trap. A tripped guard surfaces as an undifferentiated trap with no pointer to the requires(... >= 0) fix. A dedicated kind needs the contract-fail host-import message channel (last_violation / $vera.contract_fail) wired through to a guard emitted mid-expression — including propagating _needs_contract_fail from the WASM context back to the codegen core so the import is emitted for an otherwise-contract-less function. Mirrors the same deferral the #520 subtraction guard took.

Both surfaced while implementing #747's runtime-guard scope and #749 item 4.