fix(verifier,codegen): obligate + guard @Int->@Nat narrowing at function return position (#758)

AGENTS.md

@@ -8,7 +8,7 @@ Read `SKILL.md` for the full language reference. It covers syntax, slot referenc
 
 ### Conformance programs as reference
 
-The conformance suite in `tests/conformance/` contains 149 small, self-contained programs — often one per language feature — that serve as minimal working examples (the exceptions are `ch07_cross_module_contracts.vera` and `ch08_cross_module_generic.vera`, which import their `ch07_cross_module_contracts_lib.vera` companion to exercise cross-module contracts). Each positive program must pass its declared verification level (see `manifest.json` for mappings: `parse`, `check`, `verify`, or `run`); the nine negative fixtures (`ch02_generic_over_unit_rejected`, `ch05_apply_fn_arity`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch08_circular_import`, `ch08_visibility_private`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`) instead must *fail* `check` with the E-code in their `expected_error` field. When you need to see how a specific construct works (e.g. effect handlers, match expressions, closures), check the corresponding conformance program before reading the spec.
+The conformance suite in `tests/conformance/` contains 150 small, self-contained programs — often one per language feature — that serve as minimal working examples (the exceptions are `ch07_cross_module_contracts.vera` and `ch08_cross_module_generic.vera`, which import their `ch07_cross_module_contracts_lib.vera` companion to exercise cross-module contracts). Each positive program must pass its declared verification level (see `manifest.json` for mappings: `parse`, `check`, `verify`, or `run`); the nine negative fixtures (`ch02_generic_over_unit_rejected`, `ch05_apply_fn_arity`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch08_circular_import`, `ch08_visibility_private`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`) instead must *fail* `check` with the E-code in their `expected_error` field. When you need to see how a specific construct works (e.g. effect handlers, match expressions, closures), check the corresponding conformance program before reading the spec.
 
 ### Workflow
 
@@ -183,7 +183,7 @@ Each stage is a module with a single public API function (`parse_file`, `transfo
 pytest tests/ -v                       # Run all tests (see TESTING.md)
 pytest tests/test_conformance.py -v    # Conformance suite only
 mypy vera/                             # Type-check the compiler
-python scripts/check_conformance.py    # All 149 conformance programs hold (positives pass; negatives fail with their E-code)
+python scripts/check_conformance.py    # All 150 conformance programs hold (positives pass; negatives fail with their E-code)
 python scripts/check_examples.py       # All 37 examples must pass
 ```
 
@@ -193,7 +193,7 @@ When implementing a new language feature, write the conformance program *first*
 
 ### Invariants
 
-- All 149 conformance programs in `tests/conformance/` must hold at their declared level — positive entries pass, and the negative fixtures (`ch02_generic_over_unit_rejected`, `ch05_apply_fn_arity`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch08_circular_import`, `ch08_visibility_private`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`) must *fail* `check` with their `expected_error` E-code
+- All 150 conformance programs in `tests/conformance/` must hold at their declared level — positive entries pass, and the negative fixtures (`ch02_generic_over_unit_rejected`, `ch05_apply_fn_arity`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch08_circular_import`, `ch08_visibility_private`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`) must *fail* `check` with their `expected_error` E-code
 - All 37 examples in `examples/` must pass `vera check` and `vera verify`
 - `mypy vera/` must be clean
 - `pytest tests/ -v` must pass

CHANGELOG.md

@@ -8,6 +8,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
 
 ### Fixed
 
+- **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](https://github.com/aallan/vera/issues/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](https://github.com/aallan/vera/issues/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](https://github.com/aallan/vera/issues/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.
 - **Reading handler state as a slot in the handled body is now a checker error, closing a check/verify-vs-compile scope divergence** ([#973](https://github.com/aallan/vera/issues/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.

CLAUDE.md

@@ -58,7 +58,7 @@ VERA_JS_COVERAGE=1 pytest tests/test_browser.py -v  # Browser tests with JS cove
 VERA_EAGER_GC=1 vera run file.vera  # Force GC on every alloc (see ENVIRONMENT.md, debug knob for #593-class GC-rooting bugs)
 mypy vera/                        # Type-check the compiler itself
 
-python scripts/check_conformance.py    # Verify all 149 conformance programs (positives pass their level; negatives fail with their expected_error E-code)
+python scripts/check_conformance.py    # Verify all 150 conformance programs (positives pass their level; negatives fail with their expected_error E-code)
 python scripts/check_examples.py      # Verify all 37 examples parse + check + verify
 python scripts/check_examples_readme.py # Verify vera run commands in examples/README.md
 python scripts/check_spec_examples.py # Verify spec code blocks parse
@@ -88,7 +88,7 @@ See [`TOOLCHAIN.md`](TOOLCHAIN.md) for the CLI cookbook — driving the toolchai
 - `vera/` — Reference compiler: grammar, parser, AST, transformer, type checker, verifier, codegen, CLI
 - `examples/` — 37 example Vera programs (all must pass `vera check` and `vera verify`)
 - `tests/` — Test suite (unit tests + conformance suite)
-- `tests/conformance/` — 149 conformance programs validating every language feature against the spec
+- `tests/conformance/` — 150 conformance programs validating every language feature against the spec
 - `scripts/` — CI and validation scripts
 
 ## Writing Vera code
@@ -125,7 +125,7 @@ Before changing code — **adding or removing** — write the test that proves y
 ## What not to break
 
 - Pre-commit hooks run mypy + pytest + conformance suite + example validation on every commit
-- All 149 conformance programs in `tests/conformance/` must hold at their declared level — positive entries pass, and the negative fixtures (`ch02_generic_over_unit_rejected`, `ch05_apply_fn_arity`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch08_circular_import`, `ch08_visibility_private`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`) must *fail* `check` with their `expected_error` E-code
+- All 150 conformance programs in `tests/conformance/` must hold at their declared level — positive entries pass, and the negative fixtures (`ch02_generic_over_unit_rejected`, `ch05_apply_fn_arity`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch08_circular_import`, `ch08_visibility_private`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`) must *fail* `check` with their `expected_error` E-code
 - All 37 examples in `examples/` must pass `vera check` and `vera verify`
 - Version must stay in sync across `vera/__init__.py`, `pyproject.toml`, and `CHANGELOG.md`
 - All tests must pass: `pytest tests/ -v`

FAQ.md

@@ -178,7 +178,7 @@ None of this is Vera-specific, but it validates the design choices. The thesis i
 
 This is a real concern. LLMs are trained on trillions of tokens of Python, TypeScript, and JavaScript. A MojoBench study (NAACL 2025) found that even fine-tuned models achieved only 30–35% improvement over base models on Mojo code generation, illustrating the cold-start problem for new languages.
 
-Vera's approach has three parts. First, the agent-facing documentation (SKILL.md) is designed to be dropped into a model's context window, so the model works from the language specification rather than training data recall. Second, Vera's syntax is deliberately simple and regular — fewer constructs, each with exactly one canonical form — which reduces the surface area a model needs to learn. Third, the conformance test suite (149 programs covering every language feature) gives models concrete examples to learn from and conform to. Simon Willison argued in December 2025 that a language-agnostic conformance suite is the single most important tool for LLM adoption of a new language — LLMs can learn new languages remarkably well when given tests to conform to.
+Vera's approach has three parts. First, the agent-facing documentation (SKILL.md) is designed to be dropped into a model's context window, so the model works from the language specification rather than training data recall. Second, Vera's syntax is deliberately simple and regular — fewer constructs, each with exactly one canonical form — which reduces the surface area a model needs to learn. Third, the conformance test suite (150 programs covering every language feature) gives models concrete examples to learn from and conform to. Simon Willison argued in December 2025 that a language-agnostic conformance suite is the single most important tool for LLM adoption of a new language — LLMs can learn new languages remarkably well when given tests to conform to.
 
 
 ## How does Vera compare to Dafny / Lean / Koka / F*?
@@ -221,7 +221,7 @@ The reference compiler is under active development. The current release includes
 
 - A seven-stage pipeline: parse, transform, resolve, typecheck, verify, compile, execute
 - A 14-chapter formal specification
-- 7,017 tests, including a 149-program conformance suite
+- 7,045 tests, including a 150-program conformance suite
 - 37 working example programs
 - 164 built-in functions covering strings, arrays, math, parsing, and data types
 - Four built-in abilities (Eq, Ord, Hash, Show) with constrained generics and ADT auto-derivation