Skip to content

Codegen: extend the #747 @Nat runtime-guard backstop to generic-instantiated constructor fields #757

Description

@aallan

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    codegenCode generation backendenhancementNew feature or request

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions