Follow-up from the #747 review (PR #756). One @Nat narrowing site is statically obligated by the verifier (so verified programs are sound — a negative narrowing is an E503 compile error) but lacks the codegen i64.lt_s/unreachable runtime backstop that #747 added for user-function call args, constructor fields, let/match/destructure sites, and — folded into #756 — the builtin @Nat translators. It stores a negative @Nat silently only on an unverified compile (vera compile / vera run without vera verify). Same residual class as #754 (effect-op argument).
Builtin half landed in PR #756 (commit fbd68dc). The builtin translators (string_repeat, string_pad_start / _end, string_from_char_code, md_has_heading) now apply _emit_nat_bind_guard; string_slice is exempt because it clamps its indices to [0, len]. This issue is re-scoped to the remaining generic-constructor-field half below.
Generic-instantiated constructor fields
Wrap(@Int.0) building a Box<Nat> (a generic field instantiated to @Nat): constructor layouts carry no per-field @Nat mono metadata, so the guard is skipped. Fix: monomorphise nat_fields per ctor instantiation.
Verifier behaviour is already correct (E503 on a negative; discharged from a precondition). This issue is purely the codegen runtime backstop. Surfaced by CodeRabbit on PR #756.
Follow-up from the #747 review (PR #756). One
@Natnarrowing site is statically obligated by the verifier (so verified programs are sound — a negative narrowing is an E503 compile error) but lacks the codegeni64.lt_s/unreachableruntime backstop that #747 added for user-function call args, constructor fields, let/match/destructure sites, and — folded into #756 — the builtin@Nattranslators. It stores a negative@Natsilently only on an unverified compile (vera compile/vera runwithoutvera verify). Same residual class as #754 (effect-op argument).Generic-instantiated constructor fields
Wrap(@Int.0)building aBox<Nat>(a generic field instantiated to@Nat): constructor layouts carry no per-field@Natmono metadata, so the guard is skipped. Fix: monomorphisenat_fieldsper ctor instantiation.Verifier behaviour is already correct (E503 on a negative; discharged from a precondition). This issue is purely the codegen runtime backstop. Surfaced by CodeRabbit on PR #756.