Summary

A refinement / @Nat narrowing bound in a nested constructor sub-pattern (Some(Some(@PosInt)) on Option<Option<Int>>) is now statically obligated (PR #763 made _obligate_subpattern_narrowings recurse via _obligate_subpattern_term), so a vera verify-clean program is sound — a bad nested narrowing is an E505. But the matching runtime guard is not emitted: codegen's _extract_constructor_fields (vera/wasm/data.py) binds only direct sub-patterns, so an unverified vera compile/run does not trap on a refinement-violating value bound at a nested depth.

This is the runtime half of the nested-sub-pattern soundness gap CR flagged on PR #763 — the same class as the other statically-obligated-but-runtime-unguarded sites (#754, #757, #758): a verified program is sound; only an unverified compile is unprotected at the nested site.

Scope

• Sound today (PR feat(746): static verification of refinement-type predicates (v0.0.174) #763): vera verify catches a bad nested narrowing — Some(Some(@PosInt)) on Option<Option<Int>> where the inner Int isn't provably > 0 is an E505.
• Not yet guarded: the codegen runtime check for a nested bind. Direct sub-pattern binds ARE runtime-guarded (Generalize @Nat narrowing obligation to projection binding sites (ADT sub-pattern, non-literal destructure) #747); nested binds are not.

Suggested fix

Make _extract_constructor_fields (and the verifier's static recursion's runtime counterpart) recurse into nested ConstructorPattern sub-patterns, projecting each field and emitting the same @Nat / refinement boundary guard the direct-bind path emits. This mirrors the verifier-side recursion added in #763.

Relationship

Runtime-guard deferral in the same family as #754 / #757 / #758 (statically obligated, runtime-unguarded). Surfaced during the #746 review (PR #763).