v0.1.4

Fixed

• Duplicate where-helper names now compile and verify correctly via parent-qualified mangling instead of crashing WAT assembly or proving against the wrong helper (#991). Non-generic where-helper WAT names were flat and unmangled and _fn_sigs registration was last-wins, so two same-named helpers in different parent subtrees (a leaf under each of two siblings), or a helper named like a top-level function, collided in the single flat WAT namespace: vera compile failed with a raw duplicate func identifier on a check-green program (before the #978 nested-emission fix one variant was worse — a colliding grandchild was silently dropped and its call bound to the same-named top-level function, a silent wrong value). A related verifier facet: the flat, last-wins env.functions lookup assumed the WRONG same-named helper's ensures at a call site, reporting a false E500 in a diamond of same-named helpers with different postconditions. The DESIGN call is parent-qualified mangling, not a checker rejection: spec §5 (spec/05-functions.md) makes where-helpers "always local to the parent function", so two same-named helpers under different parents are a semantically VALID program — the collision was codegen's flat namespace leaking, not a user error — and mangling gives one canonical treatment of helper symbols across the generic and non-generic paths (the generic path already parent-qualifies its per-clone hoists, gid$Int$where$helper; DESIGN principle 3). Codegen now hoists every non-generic where-helper to a parent-qualified top-level decl (compute$where$branchA$where$leaf) before registration, rewriting every lexically-visible helper call in the parent's body and in each nested helper's body to the mangled target — the non-generic mirror of the #904 clone hoist — so registration, monomorphization discovery, and Pass-2 emission all see collision-free names; generic helpers stay structurally nested for the mono path (each is a monomorphization base, #990/#904), with their bodies rewritten shadow-aware (see below). Resolution is lexical throughout: a helper's bare call binds to the NEAREST same-named helper in the enclosing where-tree — its own children, then any ancestor's (a grandchild calling an "aunt" — a sibling of its parent — is redirected across scope levels), with an inner helper shadowing an outer same-named one for its subtree. The verifier and the CHECKER resolve a bare helper call the same way — the nearest same-named helper in the enclosing where-tree (own children first, then each ancestor's), then the top-level function, then the flat registry — so each parent proves and type-checks against its OWN helper: the review's third round found the checker still resolving through the flat last-wins registry, which falsely REJECTED (E121) a valid diamond whose two same-named leafs differ in signature (branchA's @Int -> @Int call synthesized against branchB's @Int -> @String leaf, registered last); the checker now threads a _fn_scope_stack through _check_fn and resolves calls (and the commutativity analysis's effect-row lookups) lexically, completing the issue's checker/verifier/codegen agreement clause — with the #969/#977 slot-isolation and #815 builtin-redefinition (E151) invariants pinned intact by the negative conformance fixtures. Top-level names stay bare (exports and execute(fn_name=…) lookups depend on them) and generic clones are never double-mangled. The hoist also corrects the IMPORT door (review round 4): a non-generic helper's name no longer suppresses a same-named import's bare emission — the _local_shadowed_fn_names collection now walks the POST-hoist program, so outside the parent the import wins, exactly as the lexical resolution rules state. At base this shape was a silent wrong body: the helper's bare emission captured a top-level import-bound call (leaf(0) ran the helper's + 1 instead of the import's + 7 — 101 where the correct result is 701); the first cut upgraded it to a loud unknown func (the stale pre-hoist shadow suppressed the import while the helper no longer occupied the bare name); the fix resolves it correctly — the import through its bare emission, the parent's call through its own parent-qualified helper. A top-level local sharing an import's name still shadows it (§8.5.2), and a RETAINED generic helper's name still shadows: an uninstantiated T-unused generic template still emits under its bare name, which would otherwise collide with the import's bare emission (pinned by tests/test_xmod_where_helper_import_991.py). The PR #1013 review then closed three residuals of the first cut, all in how the rewrite met GENERIC subtrees: (1) the ancestor-scope rewrite descended into retained generic helpers' bodies without re-applying their own inner shadowing, so a generic helper's call to its OWN nested shared was captured onto an ancestor's p$where$shared — mono cloned it with the call pre-rewritten, so the per-clone redirect never fired: a silent wrong value (base returned 35, the capture returned 25) and, contracted, a false Tier-1 (verify proved the contract against the right helper while the compiled program ran the wrong one and trapped) — the descent is now shadow-aware per level, and a generic helper's NAME also erases a same-named ancestor entry for its level's subtree; (2) a fully-concrete (T-unused) generic helper template compiles, and its dead emission dangled once its own helpers moved to per-clone symbols (pre-#991 it WAT-validated only by resolving to a same-named ancestor's bare emission) — the dead template WAT is now dropped when clones are registered, keeping the @T-template warning surface and the uninstantiated-generic fallback; (3) the verifier's per-instantiation dispatch dropped the enclosing ancestor chain, so a nested generic helper's clone resolved an unshadowed ancestor-helper call through the flat last-wins registry, where a same-named decoy helper under any other function captured it (a false E500 against the decoy's contract on a correct program) — _verify_generic_instances now threads the chain into each clone's verification. Pinned by tests/test_codegen_where_helper_mangling_991.py (sibling-leaf collision, helper-shadows-top-level with both bodies independently reachable, ancestor-scope and shadowing shapes, a collision coexisting with a nested generic, the generic-subtree capture shapes including the false-Tier-1 verify+run differential, and the checker-leg differing-signature diamond checked AND run — every run assertion checks a value that only its OWN helper body yields) and tests/test_verifier_where_helper_scope_991.py (the diamond verifies, a genuine-violation guardrail still caught, and the decoy-capture clone-scope shape verifies with per-function Tier-1 obligation checks and runs both doors), with each mechanism — emission mangling, call-name rewriting, verifier scoping, checker scoping, shadow-aware generic descent, generic-name erasure, and the clone-chain threading — reverted to a RED test.
• The static E503 @Nat-narrowing obligation now fires for the concrete components of a partially-generic constructor argument (#1010). Every re-synthesis in the generic-call argument loop was gated on the WHOLE parameter type being typevar-free, so a constructor argument against @Pair<Nat, T> was never re-typed against its instantiated parameter — the concrete Nat component's narrowing target went unrecorded, and wants(MkPair(0 - 5, None)) checked, verified clean, and silently stored the negative (the fully-concrete @Pair<Nat, Int> analogue was E503 at verify). Constructor-expression arguments are now re-synthesized against the instantiated parameter even when type variables remain — the #971 fill adopts component-wise, typevar components stay unconstrained, and each field's target is recorded exactly as on the concrete path, so the provably-negative shape is E503, an unconstrained @Int param into the component is E503 with its counterexample, and the requires(@Int.0 >= 0) variant discharges Tier-1. The runtime-guard half for generic fields is unchanged and stays documented under the #754/#757 limitation rows (the static promise is what #1010 restored). Found by the PR #1009 review; pinned by five tests in tests/test_verifier_nat_obligations.py (three fixed shapes, a no-false-positive guard, and the concrete control) with a revert-the-fix mutant killed.
• A bare None (nullary constructor) as a call argument now adopts the expected type (#993). Final mechanism of the fresh-ctor-var family (return/let/match #971, nested ctor fields #979, comparison operands #981): five argument-position sites still minted an unresolvable T$n and rejected well-typed programs. (1) The #971 bidirectional fill now overrides a tentative type-arg binding whose value is a bare fresh var — the same fresh-is-tentative precedence _unify_for_inference applies between arguments (#293) — fixing MkA(None) under a bare forall var (E121, the nested nullary ctor's own placeholder had leaked into the instantiation). (2) The generic-call argument loop treats a residual type variable on either side as a structural wildcard before rejecting — option_unwrap_or(nothing(()), None) (E202) is satisfiable at some instantiation when every argument is itself polymorphic, while a cross-ADT or concrete-leaf mismatch is still rejected. (3) Ability-op constructor arguments re-synthesize against the resolved parameter type — ensures(eq(@Option<Int>.result, None)) (E241) now checks at concrete and forall expected types, matching the operator form fixed by #981. (4) The handler-state initializer synthesizes with the declared state type expected, so handle[State<Option<Int>>](@Option<Int> = None) (E331) checks. (5) A both-constructor comparison may adopt from a resolved constructor sibling — Some(5) == None (E142) checks, while None == None (no side to adopt from) stays rejected. The PR #1009 review round then hardened all five against the rigid/fresh distinction: the wildcard is scoped to genuinely unresolved vars — fresh T$n, #b-marked builtin vars, and callee forall vars leaked from an uninferrable call — while the enclosing function's own declared forall params stay rigid (passing @Option<T>.0 where Option<Int> is required is E202 again; the first cut wildcarded every TypeVar, a soundness regression caught in review), a function type's effect row is never wildcarded (<IO> cannot satisfy a pure formal), the ability-op mapping no longer locks onto the first argument's fresh var (eq(None, Some(5)) and ensures(eq(None, @Option<Int>.result)) re-anchor on the later resolved argument and check, while eq(None, None) stays rejected — a fresh-holed param is not a resolved type to adopt), and the both-ctor adoption guard distinguishes rigid from fresh (Some(@T.0) == None under forall<T where Eq<T>> checks; None == None still rejected). Pinned by eighteen tests in tests/test_checker_types.py (twelve fixed shapes incl. every reversed operand order + six guardrail rejections) with a twelve-mutant battery: each mechanism reverted flips its test RED, and every over-broadening mutant (cross-ADT wildcard, rigid-var wildcard, effect-row wildcard, unresolved-sibling adoption, fresh-param adoption) is killed by a guardrail pin. The review also surfaced a pre-existing static-obligation gap, filed as #1010: the E503 @Nat-narrowing obligation is lost when a constructor argument's parameter type contains a typevar (MkPair(0 - 5, None) as @Pair<Nat, T> verifies clean and silently stores the negative) — identical at the integration base; fixed by the #1010 entry above.
• eq(...)/compare(...) in imported function bodies now compile (#992). The Pass-1.6 ability-op rewrite canonicalized the two AST-rewritten ability operations for the top-level program's declarations and the mono clones but never for the imported populations, which compile directly in Pass 2.5/2.6 — an eq anywhere in an imported body (top-level, where-helper, or nested grandchild) stayed a raw call codegen cannot lower, the body was dropped, and the importer's call dangled at WAT assembly (unknown func) on a check-green, verify-green pair. The rewrite now runs over every _imported_fn_decls / _shadowed_module_fns entry (the flattened where-tree, so each helper is its own entry; the rewrite is idempotent, so a parent's carried subtree cannot double-transform). Pinned by tests/test_xmod_ability_ops_992.py — eq at all three nesting depths, compare, and the shadowed (mod$…) door — with a drop-the-rewrite mutant killed.
• A nested handle[State<T>]'s initial-state expression now observes the ENCLOSING scope's state (#976 review, pre-existing). _translate_handle_state pushed the fresh inner cell BEFORE evaluating the init expression, so a get(()) in the init — lexically an outer handler's operation — read the new inner cell's default 0 instead of the outer state: handle[State<Int>](@Int = get(()) + 5) under an outer handler holding 100 silently initialized to 5, check- and verify-green. The init expression is now evaluated first (it belongs to the enclosing scope), then the fresh cell is pushed and the value stored. Found by PR #1003's adversarial panel; pinned by ledger tests (105 and 205 shapes) in tests/test_state_clause_semantics.py.
• handle[State<T>] operation clauses now execute, with intrinsic-hybrid semantics (#976, closing the §7.5 spec contradiction #988). Clause bodies and with state-update expressions were type-checked but never lowered — _translate_handle_state compiled the handled body against the builtin host-side state cell and dropped expr.clauses wholesale, so a clause that transformed resume's argument or a with value differing from put's argument was silently discarded (the corpus never noticed: every fixture's clauses mimicked the builtin semantics exactly). Under the maintainer-pinned option-C semantics: put stores / get reads intrinsically (the operations' declared meaning, independent of the clauses); the matching clause body executes with its resume(value) as the op's result at the call site; with @T = expr overrides the intrinsic store; and the clause's @T.0 is captured pre-store, so with @T = @T.0 means keep the old state. The lowering inlines the clause at each get/put call site over the existing host-cell imports (capture → intrinsic store → clause body with resume(v) lowered to the value → optional override) — no host changes, wasmtime and browser in lockstep by construction, wasi-p2 unchanged (State stays unsupported there). resume in a State clause is single-shot and tail-position enforced (a missing, repeated, or non-tail resume skips the function loudly; multi-shot stays FUTURE). Because with @T = @T.0 flips from a silent no-op to a meaningful keep-old override, the corpus's redundant with @T = @T.0 clauses (written as no-ops under the dropped-clause behaviour) are migrated to the canonical no-with form, which is an exact identity under the new semantics. Verifier posture unchanged: obligations inside handle bodies stay Tier-3 (#439), and the runtime checks now observe the clause-transformed values. Spec §7.5.1/§7.5.2 rewritten to state the semantics explicitly (closes #988; the §7.5.3 example's result is unchanged). Pinned by tests/test_state_clause_semantics.py (transform, override, keep-old canary, composite-state transform incl. a captured-pointer-after-alloc shape probed green under VERA_EAGER_GC, non-tail-resume rejection, and canonical-identity controls) and a run-level conformance program (tests/conformance/ch07_state_clause_transform.vera).
• The @Nat → @Int per-component widening guards now fire for imported module bodies, closing the cross-module half of the #820 guard wave where a library's vera verify promise was silently dropped through the import door (#987). #820 threaded the checker's expr_target_types table into code generation, but that table is keyed by bare span (no file identity) and computed for the top-level program only — so an imported function body compiled into the importer's flat WASM module (vera run/compile/test, browser, and wasi-p2 all share the artifact) found no entry and dropped the array-element and tuple-construction widen guards, and a @Nat above 2^63 - 1 reinterpreted to a negative @Int (u64.MAX → -1) with no trap even though the library's own vera verify reported the site Tier-3. (The tuple-destructure guard, recovered structurally from the let Tuple<@Int, …> binding pattern rather than the span table, already crossed the door, as did the closure positions, recovered from the closure's function type.) PR #986's interim mitigation suppressed span-keyed lookups for imported bodies entirely — necessary because an engineered cross-file span collision could otherwise hand an all-@Nat imported body the importer's Tuple<Int, Int> target and emit a spurious guard that false-trapped a legal @Nat. The fix computes each resolved module's OWN span-keyed target/semantic side-tables (CheckArtifacts.module_artifacts, keyed by module path, with each module's direct imports re-derived so its check matches a standalone one) and threads them through compile() → CodeGenerator → _compile_fn(module_tables=…), so an imported body is resolved against its module's table (correct spans, no cross-file collision) rather than the importer's — flipping the collision guarantee from suppression to correctness (the collision fixtures now prove no guard because the module's own target is genuinely Tuple<Nat, Nat>, tests/test_xmod_span_collision.py), and reaching transitively-imported and shadowed (mod$…) module bodies too. A module with no threaded table falls back to the #986 suppression, never a wrong-file guard. The per-module collection is opt-in (collect_module_artifacts= on typecheck_with_artifacts, default off): it is O(N²) sub-checks in the module count (each of N resolved modules gets a full check_program re-registering the other N−1), so only the codegen-bound callers (vera compile/run/serve/test) request it — vera verify and the warm VerificationSession, which read only the top-level target tables, skip the pass entirely (PR #997 review). The verifier needs no change — its per-module classification was already correct; the promise the codegen artifact was breaking. Pinned by a cross-module verifier↔codegen differential run through the import door (tests/test_xmod_widening_differential.py: array-element, tuple-construction, transitive 3-level, and shadowed-import shapes each trap at u64.MAX and round-trip 2^63 - 1/42, with a tuple-destructure control) and a run-level conformance program (tests/conformance/ch08_xmod_widen.vera). A separate pre-existing residual is unchanged and out of scope: a compile-time @Nat literal above 2^63 - 1 folded directly into an Array<Int>/Tuple<Int, …> still constant-folds to a verify-clean value that runs negative at both same-file and cross-module — a const-fold disclosure gap, not this cross-module threading. A second pre-existing residual is disclosed here and tracked as #998: an imported generic function's mono clones compile on the monomorphization path without the threaded module table, so a concrete Array<Int>/Tuple<Int, Int> widening inside a forall<T> import — which the library's own vera verify still classifies Tier-3 once instantiated — is not runtime-guarded at any instantiation reached through the import door (the @Nat above i64.MAX silently reads back as -1, the same broken-promise shape this entry closes for monomorphic imports). Unlike the const-fold gap it was not verifier-disclosed (still reported Tier-3), making it an unsound residual — closed in this release by the #998 entry below.
• A forall<T> where-helper under a non-generic parent is now monomorphized, so its concrete call sites compile instead of dangling at an internal unknown-func error (#990). Generic discovery collected mono bases from top-level declarations only, so a generic helper nested in a non-generic function's where block was invisible: no clone was emitted, the parent's concrete-typed call lowered to the bare unmangled name, and vera compile failed WAT assembly on a check-green, verify-green program. Both sides now build their base set with a SHARED collector (vera/monomorphize.py collect_nested_generic_decls): codegen Pass 1.5 emits clones for nested generics whose whole ancestor chain is non-generic (stopping at generic helpers — their subtrees are carried per-clone and hoisted by the #904 path, so nothing double-emits), and the verifier's instance discovery collects the identical set, so each nested instantiation is verified per-monomorphization exactly like a top-level generic's (_verify_fn's forall dispatch already keys on the decl name). The Pass-2 where-fn sweep stops at a generic template's subtree (the template itself still surfaces the standard uncompilable-template warning, and the clone-compiled suppression set now includes nested templates). Codegen⊇verifier lockstep is pinned by a nested_generic_where_helper corpus entry in the #732 differential (tests/test_monomorphize_differential.py), behaviour by tests/test_generic_where_helper_990.py (direct, grandchild, two-instantiation, own-where-child, and #904-control shapes with WAT-level single-emission assertions) and a run-level conformance program (tests/conformance/ch09_generic_where_nongeneric_parent.vera). Two sibling gaps found by this fix's grounding probes are pre-existing and tracked separately: a nested generic inside an imported function (#999) and a private module generic reached transitively from an exported one (#1000).
• Monomorphized clones of imported generic functions now carry their origin module and compile against that module's span-keyed tables, so the #820 per-component @Nat → @Int widen guards fire at every instantiation through the import door (#998). #987 threaded per-module tables into non-generic imported bodies, but clones of a forall<T> import compiled on the monomorphization path with the IMPORTER's tables (no entries for the library body's spans), so a library generic widening @Nat into a concrete Array<Int>/Tuple<Int, Int> component ran unguarded (u64.MAX → -1, no trap) while the library's standalone vera verify promised the site Tier-3 — the same broken-promise shape #987 closed for monomorphic imports. The module harvest now records each unshadowed imported generic's origin path (_imported_generic_origins), every emitted clone of an imported base is tagged with it (_mono_clone_origins — the main worklist, the shadowed mod$… clones, the shadowed-body transitive chase, and the per-clone hoisted where-helpers, which inherit their clone's origin), and the mono compile loop threads imported=True + that module's module_artifacts table for tagged clones exactly like Pass 2.5/2.6 bodies (monomorphization preserves node spans, so the template module's table keys the clone's body correctly; absent tables fall back to the #986 suppression, never a wrong-file guard). A local generic's clones carry no tag and keep the main-file tables — pinned by an explicit control. tests/test_xmod_generic_widen_gap.py flips from the honest gap pin to the guarded differential: array-element and tuple-construction sites × T=Bool/T=Int instantiations trap unreachable at u64.MAX and round-trip in-range values, through both the bare-call and shadowed (lib::wrap → mod$…) doors, plus a hoisted-where-helper-widen scenario and the local-clone control.
• An @Int → @Nat narrowing at a lifted closure's return is now obligated and runtime-guarded, closing the last residual of the #758 return-narrowing hole (#984). fn(@Int -> @Nat) { @Int.0 } applied to a negative value returned it through the @Nat slot silently on a verify-clean program: top-level functions and where-helpers were covered by #758's return obligation + guard, but the closure body's return leaf — reachable only through _compile_lifted_closure — was neither obligated by the verifier nor guarded by codegen. This is the narrowing dual of the #820 closure-return @Nat → @Int widening and hangs off the same lifted-closure hook. The verifier's AnonFn arm gains the narrowing case (a _is_nat_type resolved return whose body _return_narrows_into_nat): because the closure body is opaque to the SMT layer (translating it against the outer slot env could mis-resolve a closure parameter and prove a false Tier 1), it is obligated shallow-syntactically as a Tier-3 nat_bind, never a false Tier-1 verified. Codegen guards the closure return PER NARROWING LEAF (_nat_return_leaf_ids threaded into the lifted body, exactly as _compile_fn does for the top-level return) rather than as a whole-body wrap — a wrap would false-trap a legitimate @Nat leaf of a heterogeneous body (a captured @Nat above i64.MAX reads as a negative i64); an alias-aware, refinement-excluded gate mirrors the top-level narrow-return gate, so an already-@Nat closure return and an @Int → @Int closure stay untouched. The verifier↔codegen agreement is pinned by an extended tests/test_nat_narrowing_return_differential.py battery (trapping, over-guarded-but-safe abs, and non-narrowing control shapes, plus a pin of the #985 nested-closure residual) and a run-level conformance program (tests/conformance/ch05_closure_nat_return.vera). One residual is tracked honestly: a closure nested inside another closure's body is guarded by codegen but not obligated by the verifier (the AnonFn walk is deliberately shallow) — #985, whose scope now covers this narrowing direction alongside its original widening one.
• A where-helper that carries its OWN where-helpers now has those nested helpers emitted by the non-generic codegen path, closing a check/verify-green-then-compile-fail divergence (#978). A non-generic fn outer { … } where { fn child { … } where { fn grandchild … } } passed vera check and vera verify but crashed vera compile with unknown func: $grandchild at WAT assembly: the checker (_check_fn), verifier (_verify_fn), and registration (_register_fn) all recurse into nested where blocks — so grandchild's name was registered and child's body lowered its call to return_call $grandchild — but the Pass-2 emission loop in vera/codegen/core.py compiled only ONE level of decl.where_fns, so a nested helper's body was never emitted and the reference dangled. Single-level where blocks were unaffected, and the generic-parent path already recursed (monomorphize._hoist_where_fns_under flattens the whole helper tree per clone), so the identical program under a forall<T> parent compiled and ran. The non-generic loop now flattens decl.where_fns recursively to arbitrary depth (pre-order, with an id-keyed visited guard) and emits every helper. The verifier already descended (a false ensures on a grandchild is caught at Tier 1), so this is a codegen-only completeness fix, no verify change. Pinned end-to-end by tests/conformance/ch05_nested_where_helpers.vera (a two-level and a three-level chain, each helper carrying a meaningful ensures so the leaf's contribution is proven up the chain at Tier 1 and the whole runs to a leaf-dependent value) and unit coverage over the two- and three-level shapes plus the generic-parent control (tests/test_codegen_monomorphize.py::TestNestedWhereHelperEmission978). PR review (#989) found and closed two residuals of the same divergence. (1) Ability-op rewrite recursion: Pass 1.6 (_rewrite_where_fns, in vera/codegen/core.py) rewrote each DIRECT child helper's body + contracts (eq/compare → operator form) but never recursed into a helper's OWN where_fns — so a grandchild using eq/compare in its body or contracts kept a raw FnCall, _compile_fn tripped CodegenSkip and dropped its body, and the parent's return_call $grandchild dangled even though the emission loop had reached it; _rewrite_where_fns now recurses (body, contracts, and nested where_fns) mirroring the flatten walk. (2) Imported-module registration recursion: _register_modules (vera/codegen/modules.py) collected an imported function's where-helpers with a one-level loop, so an imported libfn -> child -> grandchild chain registered only child for Pass-2.5 emission — grandchild checked and verified green but never emitted, dangling child's call to it; the registration walk now reuses the same _flatten_where_fns the local Pass-2 loop uses, reaching helpers at any depth. Pinned by three ability-op grandchild shapes plus a branching two-nested-helper shape (TestNestedWhereHelperEmission978) and a check/verify/compile/run differential over imported two- and three-level chains (tests/test_codegen_modules.py::TestImportedNestedWhereEmission989).
• The @Nat → @Int widening is now obligated and runtime-guarded at the array-element, tuple-component, heterogeneous-arm, and closure argument/return sites, closing the last silent @Nat widening residuals (#820). A @Nat above i64.MAX bit-reinterprets to a negative @Int when widened; #813 guarded the sites where code generation can statically see the source @Nat (return, let, call-argument, concrete @Int field, ADT sub-pattern, match-bind), but five sites still widened on a verify-clean program — two silently (a closure argument/return/capture, and a heterogeneous if/match whose alternative is a genuine @Int-slot, both carrying no obligation at all) and three E531-disclosed but runtime-unguarded (the array-literal element and the tuple construction/destructure component). The enabler is a new per-component target-type table: the checker's expr_target_types side-table (the expected type each expression was checked against) is now threaded into code generation — the dual of the verifier's _target_type_of — so the erased WASM layouts recover the @Int target that the source-typed layout cannot. With it, code generation guards the array element (target Array<Int>), the tuple component at construction and at the destructure read (target Tuple<…, Int, …>), the @Nat arm of a heterogeneous @Int-join if/match per-arm (the boundary guard cannot fire without false-trapping the genuine @Int arm), the closure argument (formal type recovered from the closure's function-type, call_indirect-guarded), and the closure return/capture (the closure body's @Int return guarded in _compile_lifted_closure, obligated shallow-syntactically because the body is opaque to the verifier's SMT layer). The verifier obligates exactly these sites (nat_to_int_coerce, Tier-3 runtime-guarded), and the verifier↔codegen agreement is pinned by the extended tests/test_int_widening_differential.py battery. The per-arm machinery is target-aware and TCO-safe, hardened by the PR's adversarial review: the arm guard fires only when the join's target is @Int (mirroring the verifier's _is_hetero_int_widen_join — without the target check, a heterogeneous join in a @Nat-returning function false-trapped a legal @Nat above 2^63 - 1), and an arm whose @Nat value is a tail call lowers to a plain call so the appended guard stays live (a return_call would skip it — the widening dual of the #983 per-leaf narrowing lesson; the genuine @Int arm's recursive return_call is preserved, both pinned by tests/test_hetero_widen_tailcall.py). vera test now compiles and verifies with the same artifact tables as the other CLI doors (tests/test_tester_artifacts.py), and a user-defined data Tuple no longer takes the builtin variadic carrier's target-table path (Tuple gated on the carrier's empty layout, not the name). Two residuals are tracked honestly: #985 — a closure nested inside another closure's body is guarded by codegen but not yet obligated by the verifier (the AnonFn walk is deliberately shallow), so vera verify under-reports that one runtime check (sound over-guarding, not a widening hole) — and #987 — the array-element and tuple-construction component guards were initially not emitted for imported module bodies (the target-type table was single-module and span-keyed), now closed by threading each resolved module's own table into code generation (see the dedicated #987 entry). The one component site still unguarded — a generic-instantiated @Int field (Some(@Nat.0) into Option<Int>, erased to i64 with no per-field mono metadata) — stays honestly E531-disclosed and is tracked with its narrowing dual (#757); the same target-type enabler now unblocks the deferred @Int → @Nat narrowing guards (#754/#757/#765) and the closure-return narrowing (#984).
• A @Int value narrowing into a @Nat return slot is now statically obligated and runtime-guarded, closing a soundness hole where a vera verify-clean function could return a negative @Nat (#758). fn to_nat(@Int -> @Nat) { @Int.0 } verified clean at Tier 1, yet to_nat(0 - 5) returned -5 through the @Nat slot with no trap: the narrowing walker obligated every binding site (let, call-argument, constructor-field, match-bind, destructure — #552/#747) but never the function's own return slot, and codegen emitted no return coercion guard. The verifier now emits the nat_bind result >= 0 obligation at the return position — the dual of #813's @Nat -> @Int widen-return — discharged under the body's path conditions (so an if @Int.0 >= 0 then @Int.0 else -@Int.0 tail and examples/absolute_value.vera prove at Tier 1, an unconstrained narrowing is a loud E503, and an opaque one is an honest Tier-3), and codegen emits the mirroring return guard so an unverified compile traps rather than returning a reinterpreted negative. Detection descends if/match joins to their leaf return expressions (the whole target-typed body reads as @Nat in the checker's side-table, masking a narrowing arm), and a genuine @Nat -> @Nat tail call (count_down(@Nat.0 - 1)) is excluded via the side-table / declared-return-type classifier so its return_call tail-call optimization is preserved. The verifier↔codegen site sets are pinned by a return-position differential (tests/test_nat_narrowing_return_differential.py) and tests/conformance/ch04_nat_return_obligation.vera. PR review closed two follow-on gaps in the same fix: the codegen return gates now resolve type aliases (via the resolver the let-site guard already uses) — a type Count = Nat return is guarded (narrow) and a type MyInt = Int return with a @Nat body is guarded (widen), matching the verifier's alias-resolving gates — while an alias-to-refinement (type Pos = { @Nat | ... }) stays on its single refinement-boundary guard rather than double-guarding; and the narrowing guard is emitted per narrowing leaf during body translation instead of as a whole-body wrap, so a mixed-arm recursion (drain(@Int -> @Nat) { if @Int.0 == 0 then @Int.0 else drain(@Int.0 - 1) }) keeps its non-narrowing @Nat -> @Nat recursive return_call and runs constant-stack — the whole-body wrap had reverted every return_call, so drain lost TCO and stack-exhausted at ~35k depth.
• A user forall type-variable name (T, E, A, B, K, U, V) no longer collides with a built-in generic's internal name, so generic-builtin calls over compound argument types check clean (#970). The inference skip-guard in _unify_for_inference compared a concrete argument's type-args against the callee's forall_vars by name, and the built-in registry named its internal generics T/U/A/B/E/K/V — the same letters a user reaches for. The filed bare-@Array<T> repro was masked by a name coincidence (the unsubstituted parameter @Array<T> happened to equal the argument), but the defect was live whenever the colliding user var was the immediate type-argument of a compound argument type: array_length(@Array<Option<T>>.0) under a user forall<T> was rejected with a spurious E202, and the issue's own suggested workaround (forall<E>) re-triggered it against the result_* built-ins. It fired across every generic-builtin family (array_*/option_*/result_*/set_*/map_*) and in function bodies, requires/ensures clauses, and where-helpers — a false rejection of well-typed programs, never a false accept. Every internal registry generic name is now alpha-renamed at registration to a parser-unwritable form (suffix #b, outside the UPPER_IDENT grammar and distinct from the $ used for fresh inference placeholders), so a user name can never coincide; the skip-guard itself is unchanged, and the marker is stripped from every user-facing surface — pretty_type type rendering and the diagnostics in both text and --json output never show #b. The same rename exposed and closed a dual completeness gap — given a user-defined forall<T> fn nothing(@Unit -> @Option<T>), a concrete argument now correctly overrides the bare type variable that leaks unresolved from a nested generic call (option_unwrap_or(nothing(()), 11), where nothing(()) returns @Option<T>), which the old name coincidence had been hiding; the fix is pinned in both argument orders (the leak-first order routes through the concrete-wins rule, the concrete-first order through the #898 position-wise merge). Pinned end-to-end by tests/conformance/ch09_generic_builtin_typevar.vera (a forall<T> and a forall<E> generic over compound element types, monomorphized and run) and a 19-case collide-vs-control differential battery (29 tests total).
• A bare None under forall<T> now resolves its type argument from the declared context instead of being rejected against a type that unifies trivially (#971). A nullary constructor whose type argument is fully determined by the surrounding declaration — a forall<T> return type @Option<T>, a let @Option<T> = None, or the common type of match arms — minted an unrelated fresh constructor variable T$n and then refused the well-typed program (None in return position failed E121 body has type Option<T$1>, expected Option<T>; the same miss produced E170 in a let and E302 across match arms). The checker lacked any var-to-var unification, so the fresh ctor var was never tied to the declared forall var. The bidirectional fill in _ctor_result_type now adopts an expected TypeVar — guarded, as before, by expected.name == ci.parent_type, so a constructor only ever adopts the variable its own parent's declaration names at that position and two ADTs sharing a parameter name still cannot cross-contaminate (the fresh-var minting for genuinely-unresolved variables is unchanged). Regression pinned end-to-end by tests/conformance/ch09_generic_none_return.vera, which monomorphizes all three shapes at T = Int and runs them.
• A NESTED bare None under forall<T> now threads the declared forall var through the nested-constructor field path, so Some(None) returned as @Option<Option<T>> checks clean (#979). #971 fixed the top-level result / let / match positions, but the same fresh-var pathology survived one level down: the inner None's expected field type (Option<T>) still carries the declared var, and the constructor argument loop's field-propagation guard (not contains_typevar(ft)) suppressed any typevar-bearing expected type, so the inner constructor was typed with no expected, minted an unrelated T$n, and the well-typed program was rejected (return position failed E121 body has type Option<Option<T$1>>, expected Option<Option<T>>, a let E170, match arms E302). The argument loop now forwards a typevar-bearing expected field type when — and only when — the argument is itself a constructor (ConstructorCall / NullaryConstructor), so the nested constructor's own bidirectional fill in _ctor_result_type can adopt the declared var. Feeding a typevar-bearing expected is safe solely into a nested constructor because that fill's per-level expected.name == ci.parent_type guard means an inner constructor adopts a variable only from ITS OWN parent's declared position, so two ADTs sharing a parameter name still cannot cross-contaminate (an inner constructor of a different parent sees a name mismatch, mints fresh, and the field-type check then rejects the genuinely ill-typed nesting). Deeper nesting (Some(Some(None)) at @Option<Option<Option<T>>>) descends every level, and the ill-typed direction is unchanged (Some(Some(5)) stays Option<Option<Nat>>, still E121). Pinned end-to-end by tests/conformance/ch09_generic_none_nested.vera (monomorphized at T = Int and run) and tests/test_checker_types.py::TestForallNullaryCtorNested979 (return / let / match / three-level / alternate-param-name shapes plus cross-ADT-resolution and ill-typed rejection pins).
• A bare None compared with == / != against a known Option type now adopts that type instead of minting a fresh variable, so ensures(@Option<T>.result == None) checks clean (#981). The comparison-synthesis path typed each operand with no expected type, so a nullary None operand minted an unrelated T$n that could not be compared: @Option<T>.result == None was rejected E142 Cannot compare Option<T> with Option<T$1> — in BOTH operand orders, in requires as well as ensures, and (the defect was wider than the forall case) even at a concrete @Option<Int>, which minted Option<T$1> and failed identically. For == / !=, when the initially-synthesized operands do not unify and exactly one is a constructor expression whose type still carries an unresolved variable while the other has a concrete AdtType, that constructor operand is re-synthesized against the sibling's type as expected, so the #971 fill in _ctor_result_type adopts the sibling's type arguments. Restricting the re-synth to == / != (ADTs are neither numeric nor orderable) and to a single still-unresolved constructor operand keeps it from re-typing an already-well-typed operand, and the fill's expected.name == ci.parent_type guard still rejects a genuinely cross-ADT comparison (@Result<T, Int>.result == None stays E142). This is a type-checking fix only — the verifier is untouched: a true == None postcondition proves at Tier 1, and a false != None one is correctly deferred to a Tier-3 runtime check that traps. Pinned by tests/conformance/ch09_generic_none_nested.vera (both operand orders, verified and run at T = Int) and tests/test_checker_types.py::TestForallNullaryCtorComparison981 (both orders across == / !=, the requires and concrete-Option<Int> shapes, plus non-Option and cross-ADT rejection pins).
• A NESTED payload-less constructor result (Some(None) : Option<Option<Int>>) compared against None / Some(None) in a contract no longer crashes vera verify, closing a check-green-then-verify-crash the #979/#981 checker adoption newly reached (#994 review, F1). A bare None carries no payload for the verifier's SMT sort recovery, so _find_sort_for_ctor's base-name scan picked whichever Option<...> instantiation cached first — with both Option<Int> and Option<Option<Int>> live it returned the wrong sort, and _datatype_value_eq's structural left == right raised an uncaught z3.z3types.Z3Exception: sort mismatch — a Python traceback out of vera verify (exit 1, no JSON, so --json too) on a vera check-green program. The nullary-ctor translation now hints its sort from the checker's recorded (instance-substituted) semantic type — routed through the gated #918 pinning, which PREFERS an already-cached instantiation so the hint disambiguates among live sorts without perturbing the warm/cold sort-creation order the obligations differential pins — resolving None's exact Option<Option<Int>>; a residual sort mismatch in _datatype_value_eq now degrades to an honest Tier-3 rather than crash, so vera verify --json always emits JSON. A true != None / == Some(None) postcondition PROVES at Tier 1 (both operand orders, concrete and forall); a false == None one is disproved (E500). Pinned by tests/test_verifier_nullary_ctor_sort_994.py (proof / disproof against a match-based oracle, a --json-always-JSON subprocess test, and a direct _datatype_value_eq sort-mismatch degradation backstop), mutation-validated in both halves.
• A NESTED payload-less constructor in a forall<T> == / != contract (ensures(Some(None) == @Option<Option<T>>.result)) now compiles and runs instead of a spurious E613 (#994 review, F2). The same #979/#981 shape passed check and verify but vera compile raised Type 'Option<Option>' does not satisfy ability 'Eq': the runtime-check lowering of the contract == erased the operand's type argument — the inner None renders as the bare Option (no payload to recover <Int> from), so Some(None) recovers as Option<Option>, and the dead base generic clone's slot renders Option<Option<T>> whose nested free T the top-level-only free-var check missed — so a name the structural-Eq derivation cannot lower reached it. Both operands of an == share a type (checker E142 otherwise) and a monomorphized reachable clone substitutes the sibling slot to a fully concrete name, so codegen now recovers the fully-concrete name from whichever operand carries it and routes to the scalar (dead-base-clone) lowering only when NEITHER resolves. Concrete and payload-carrying nested comparisons are unaffected, and a genuinely non-Eq concrete operand (Box<Array<Int>>, Tuple<Int, Int>) still raises the correct E613. Pinned by tests/test_codegen_nested_nullary_ctor_994.py (both operand orders + != + a body-position == compile and RUN to their sentinels, with concrete / payload-carrying controls), mutation-validated (remove the sibling recovery → the reachable clone traps on a scalar pointer compare; remove the concreteness gate → the base clone reverts to E613).
• Reading handler state as a slot in the handled body is now a checker error, closing a check/verify-vs-compile scope divergence (#973). A handle[State<T>] reaches its state only through the typed get(()) / put(...) operations — spec §7.5 scopes state to the handler clauses, and both backends agree (codegen routes state through host-side cells and gives the handled body no local; the verifier consumes no body-scope state reference). The checker, though, bound handler state into the handled body's slot scope too, so a body that read the state slot (e.g. @Int.0 under handle[State<Int>](@Int = 0)) passed vera check and vera verify, then crashed vera compile with an internal E699 dangling-slot error (or, when an enclosing same-typed binding existed, silently read that instead of the state). The checker no longer binds body-scope state; such a reference is now a natural E130 unresolved-slot error whose fix text steers the user to get(()). Handler clause bodies are unchanged — they keep their state slot, consistent with codegen and the captures walk.
• A where-helper body reading the OUTER function's parameter slot is now a checker error, closing the same check/verify-vs-compile scope divergence for where blocks (#969). spec §5 makes a where-helper always local to its parent, carrying its own mandatory contract over its own parameters; both backends compile each helper as an independent param-rooted scope. The checker, though, checked helper bodies while the parent's value scope was still live, so a helper reading an outer parameter slot (e.g. @Int.0 inside a helper(@Bool -> @Int) whose parent is outer(@Int -> @Int)) resolved to the parent's parameter and passed vera check and vera verify, then crashed vera compile with an internal E699 dangling-slot error. The parent's value-slot scope is now popped before helper bodies are checked, so such a reference is a natural E130 unresolved-slot error whose fix text explains that helpers are closed, param-rooted scopes and steers the user to pass the value as an explicit argument. The parent's forall type parameters stay in scope, so a helper of a generic parent may still be written over @T; only value slots are isolated (an implicit outer-frame capture would move a value across a contract boundary — capture semantics already have their one canonical construct in closures).
• vera verify --json's summary is now derived from the reified obligation stream, closing a total off-by-one (#967). The VerifySummary counters (tier1_verified, tier3_runtime, total) were accumulated by ~50 hand-written increments scattered through the verifier. One of them — the #882 call-site precondition demotion — bumped tier3_runtime and reified a tier3 call_pre obligation but forgot the matching total bump, so tier1_verified + tier3_runtime == total + 1 on the three examples that hit the path (http.vera, inference.vera, async_http_fanout.vera). Diagnostics and the individual tier counts were unaffected — only the summary's own arithmetic was internally inconsistent. The fix replaces every hand-written counter with a single summarize(obligations) derivation (status verified → tier1_verified; tier3/timeout → tier3_runtime; violated/tier3_unguarded excluded; total = tier1_verified + tier3_runtime), computed at report-assembly time on both the cold verify and the warm VerificationSession paths, so the counts can no longer drift from the obligations a consumer reads. vera verify --json also gains an obligations array (per obligation: kind, status, description, location, and error_code when present), so a machine consumer can reproduce or refine the tier counts directly.