v0.0.145

Fixed

• #604 / #655 Shape A — generic prelude combinator mono clones now produce the correct type-arg suffix when the closure argument is a SlotRef typed as an FnType alias (e.g. @Doubler.0 where type Doubler = fn(Int -> Int)). Pre-fix _unify_param_arg in vera/codegen/monomorphize.py had an AnonFn-specific alias-resolution path; SlotRef args typed as FnType aliases skipped that path and left the closure's return type variable unbound. The unbound type var fell to the "Bool" phantom-var fallback at result-building time, producing mono suffixes like option_map$Int_Bool instead of option_map$Int_Int and trapping at runtime with wasm trap: indirect call type mismatch. Post-fix: both AnonFn literals and SlotRef-typed-as-FnType-alias args flow through a shared _resolve_arg_fn_shape helper, binding the closure's return type uniformly. Same fix applied at the WASM call-site rewriting layer (vera/wasm/calls.py::_infer_fn_alias_type_args_wasm). Three of the five [E602]/[E604] prelude-skip cases (option_map, option_and_then, result_map) close at runtime; the other two (option_unwrap_or, result_unwrap_or) were already working via mono and only emitted misleading template warnings.

• #604 / #655 Shape A — template-warning suppression — audit recommendation 2 from the #604 investigation comment: post-compile suppression pass in vera/codegen/core.py::compile_program drops [E602] / [E604] / [E605] template-only warnings on generic forall<T> decls whose mono clones successfully compile. Pre-fix every program importing the prelude saw 5 spurious warnings about option_unwrap_or / option_map / option_and_then / result_unwrap_or / result_map even when those functions worked end-to-end via mono. Post-fix the warnings only fire for forall decls whose generic body cannot be compiled AND has no working mono clone — preserving the "this generic can never compile and you're never using a mono clone of it" signal for genuinely-broken or unused user generics, while removing the prelude-noise. Allowlist shrinks from 11 to 6 entries (5 user-code generics from #655 Shape A removed; the 6 remaining are the prelude generics still firing in test files that don't call them, plus the head real codegen gap).

• Documentation fix in CLAUDE.md release-workflow section — "Stage 9 table" reference (stale since the project moved through Stages 10, 11, 12) replaced with a stage-agnostic instruction: "the most recent Stage table in HISTORY.md" with a grep "^## Stage" HISTORY.md | tail -1 hint for confirming the current stage before writing. Caught during the 2026-05-11 review cycle.

Added

• Layer 3 of #626 — new vera/skip.py with two control-flow exception classes: CodegenSkip(node, reason) (raised when a translator hits an unsupported AST shape; caught at the _compile_fn / _compile_lifted_closure boundary and converted to a structured [E602] diagnostic with the unsupported-node's source span) and CodegenInvariantError(msg, node=None) (raised on states that type-check should have rejected; surfaced as a new [E699] "Internal compiler error" at severity=error so vera compile exits non-zero — compiler bugs shouldn't be maskable as soft warnings in CI logs). An audit of all 372 return None sites in vera/codegen/** and vera/wasm/** classified each into SILENT_SKIP / PROPAGATE / OPTIONAL_RETURN / INVARIANT_DEFENSIVE buckets; 104 SILENT_SKIP sites converted to raise CodegenSkip in this PR (55 in calls_arrays.py via a shared _array_elem_triad_or_skip helper, 24 in data.py, 11 in calls_containers.py, 9 in calls_handlers.py, 4 in context.py, 1 in calls.py). Pre-conversion these all silently dropped to a generic enclosing-function-level [E602]; post-conversion they each emit a source-located diagnostic pointing at the specific unsupported expression. The remaining 39 INVARIANT_DEFENSIVE sites and the 154 PROPAGATE sites that may now be unreachable are tracked in #657.

• New _error() API on the codegen builder (vera/codegen/core.py) parallel to the existing _warning() method, hardcoding severity="error". Used by the [E699] catch handlers in _compile_fn (vera/codegen/functions.py) and _compile_lifted_closure (vera/codegen/closures.py) — both updated in this PR to route CodegenInvariantError through _error() rather than _warning() so internal-compiler-error diagnostics propagate to a non-zero CLI exit code rather than a swallowable warning. Only those two internal handlers changed; no user-facing API surface or other _warning() call sites were modified.

• Layer 1 of #626 — new scripts/check_e602_clean.py pre-commit + CI gate that fails when any compile of an example or conformance program emits [E602] (body unsupported) or [E604] (param unsupported) outside an explicit allowlist. The [E602] warning channel was the project's only signal for silent translator-skip failures, and several long-standing instances of it were buried in every WASM compile — making it impossible to spot a new genuine skip without manually sifting through expected noise. The gate makes a new silent skip a hard build failure unless explicitly allowlisted with a tracking-issue reference.

• Allowlist of 11 currently-expected silent skips, each tagged with a tracking issue: 5 prelude combinators (option_unwrap_or / result_unwrap_or / option_map / option_and_then / result_map — #604), 6 user-code cases surfaced by the new gate's first run (5 generic-decl spurious warnings + 1 real codegen gap — #655).

Documentation

Small docs sweep — closes six aging documentation issues in one PR. No code changes; touches spec/02-types.md, spec/03-slot-references.md, spec/06-contracts.md, SKILL.md, README.md, and HISTORY.md.

• #557 — spec/03-slot-references.md Example 9 said the match-arm pattern binding "shadows the function parameter" without defining "shadow". Two readings were equally consistent with the prose (replace vs push-on-top); the compiler implements push-on-top. Replaced the one-liner with an explicit paragraph spelling out push-on-binding semantics, the resulting De Bruijn ordering for multi-field constructors (leftmost = deepest = highest index, rightmost = shallowest), and the non-commutative-operations caveat that exposes the rule.

• #561 — two tier-accuracy bugs in spec/06-contracts.md. (1) §6.3.1 (Tier 1) was missing pure-fn calls in ensures / @T.result / if/then/else, which actually verify at Tier 1 today; §6.3.2 (Tier 2 NYI) incorrectly listed them. Moved all three from §6.3.2 to §6.3.1. (2) §6.3.3 said "Bounded quantification is decidable for finite bounds and is handled by Z3 via finite unrolling" — that reads as Tier 1, but Tier 2 (the tier that would handle quantifier unrolling) is #427 NYI. Clarified that every forall/exists in a contract falls to Tier 3 today, both for forall and the symmetric exists text.

• #560 — the invariant(...) clause on data declarations is documented in spec/02-types.md §2.4.1, spec/06-contracts.md §6.2.3, and SKILL.md, but every documented form fails with [E130] no <DataName> bindings in scope at v0.0.144. Added inline NYI markers at all three sites pointing at #560, with the working alternative (refinement types). Added the limitation to spec/06-contracts.md's §6.9 Limitations table.

• #607 — added a new spec/02-types.md §2.2.1 "Int and Nat compatibility" subsection covering the bidirectional subtyping (Nat <: Int always; Int <: Nat permitted with verifier-discharged obligation). Practical-implication note tells agents not to insert nat_to_int defensively when calling array_length etc. into @Nat positions. Cross-reference added to SKILL.md's "Primitive types" listing.

• #608 — added SKILL.md "IO model: terminal vs browser" subsection (under §Browser compilation) explaining that programs using IO.sleep + ANSI escapes for terminal pacing/rendering compile cleanly to --target browser but render escapes as literal text and busy-wait the main thread. The recommended browser pattern is "Vera pure simulation core + JS driver via requestAnimationFrame". Two runtime gaps that would make the recommended pattern more ergonomic are tracked separately (#609 JSPI sleep, #610 ANSI subset interpreter). README.md's "write once, run anywhere" line qualified to acknowledge the IO seam.

• #512 — trimmed all 31 Stage 11 rows in HISTORY.md (v0.0.112 → v0.0.138) to match the early-stage one-sentence format established in Stage 1–8. Per the canonical template now in long-term memory: **X** ([#N]). per row, no em-dash separator, no secondary clauses, no implementation detail. Detailed mechanism descriptions for each version stay in CHANGELOG under their respective ## [0.0.X] section.

Changed

• mypy 1.20.2 → 2.0.0 (pyproject.toml, uv.lock). Mypy 2.0 enables three flags by default that were opt-in under 1.x: --local-partial-types (changes inference of types based on assignments in other scopes), --strict-bytes (per PEP 688: bytearray and memoryview no longer assignable to bytes), and --allow-redefinition behaves like 1.x's --allow-redefinition-new (more flexible variable redefinition across blocks). Running mypy 2.0 against vera/ produced zero errors with the existing source — no compiler-source changes needed to clear the upgrade. Manual upgrade in favour of dependabot PR #647 (closed in favour of this change).