# Testing

This is the single source of truth for Vera's testing infrastructure, coverage data, and test conventions.

## Overview

| Metric | Value |
|--------|-------|
| **Tests** | 9,037 across 137 files (~108,000 lines of test code; 8,904 passed + 26 stress, 107 skipped) |
| **Compiler code coverage** | 95% Python, 61% JavaScript — 91% combined (CI minimum: 80%) |
| **Conformance programs** | 179 programs across 9 spec chapters, validating every language feature |
| **Example programs** | 42, all validated through `vera check` + `vera verify` |
| **Spec code blocks** | 189 parseable blocks from 14 spec chapters: 92 parse, 86 type-check, 85 verify (the rest carry inline `vera:skip` annotations, #538) |
| **README code blocks** | 4 Vera blocks (4 validated, 0 annotated) |
| **FAQ code blocks** | 2 Vera blocks in FAQ.md (1 validated, 1 annotated snippet) |
| **HTML code blocks** | 5 Vera blocks in docs/index.html (5 validated: parse + check + verify) |
| **Contract verification** | 357 of 462 obligations (77.3%) across the 42 examples verified statically (Tier 1) — the denominator grew with the auto-synthesised primitive-op obligations of the soundness campaign |
| **CI matrix** | 13 combinations (Python 3.11/3.12/3.13 × ubuntu-latest/macos-15/macos-26/windows-latest, plus an advisory ubuntu-24.04-arm × 3.12 cell) + browser parity (Node.js 22) + wheel-availability preflight |

## Running Tests

All commands assume the virtual environment is active (`source .venv/bin/activate`).

```bash
# Test suite
pytest tests/ -v                                     # full suite, verbose
pytest tests/test_codegen_expressions.py             # single file
pytest tests/test_codegen_expressions.py::TestArithmetic  # single class
pytest tests/test_conformance.py -v                  # conformance suite only
pytest tests/ --cov=vera --cov-report=term-missing   # with coverage

# JavaScript coverage (browser runtime)
VERA_JS_COVERAGE=1 pytest tests/test_browser.py -v  # V8 coverage via c8

# GC-rooting diagnostic (forces $gc_collect on every alloc, see ENVIRONMENT.md)
VERA_EAGER_GC=1 pytest tests/test_codegen_closures.py::TestClosureReturnShadowPushBalance -v

# Type checking
mypy vera/                                           # strict mode

# Validation scripts
python scripts/check_conformance.py                  # conformance suite (179 programs, see manifest.json)
python scripts/check_examples.py                     # 42 example programs
python scripts/check_spec_examples.py                # spec code blocks
python scripts/check_readme_examples.py              # README code blocks
python scripts/check_skill_examples.py               # SKILL.md code blocks
python scripts/check_faq_examples.py                 # FAQ.md code blocks
python scripts/check_pypi_readme_examples.py         # PYPI_README.md code blocks (parse + check + verify)
python scripts/check_html_examples.py               # docs/index.html code blocks
python scripts/check_version_sync.py                 # version consistency
python scripts/check_wheel_availability.py           # pre-flight: every runtime dep has wheels for all supported platforms (#691 backstop)
```

## Test Files

| File | Tests | Lines | What it covers |
|------|------:|------:|----------------|
| `test_parser.py` | 170 | 1370 | Grammar rules, operator precedence, parse errors |
| `test_ast.py` | 135 | 1,125 | AST transformation, node structure, serialisation, string escape sequences, ability declarations |
| `test_checker_types.py` | 236 | 3,562 | Primitive types, literals, binary/unary ops, generics, constructors, refinement types, arrays, tuples, zero-size container rejection (E135 for Map/Set — #1075), return/match-arm types, the fresh-ctor-var family (a bare `None` adopting the expected type at return/`let`/match #971, nested ctor fields #979, comparison operands #981, and call/op/init arguments #993 — with cross-ADT and `None == None` guardrail rejections), byte-arithmetic + integer-literal-range rejection (#420 split), the #898 cross-argument type-argument merge (`eq2(MkErr(5), MkOk("x"))` fully determines `Res<String, Int>` and type-checks; a per-parameter conflict `eq2(MkOk("x"), MkOk(5))` is a clear E205; a determined-non-Eq type still type-checks), the #900/#939 generic-over-zero-size rejection (E206 fires only when the `forall<T>` READS `@T` and `T` erases to no WASM local — bare `Unit` OR a transparent `Future<Unit>` (#939) — in the body (direct return, match scrutinee, nested `let`/`if`) OR in a `requires`/`ensures` clause (#939); a `@T`-unread generic like `firstInt`/`ignore`, a boxed `Option<Unit>`, a `Future<Int>`, and the built-in `async(IO.print(...))` over Unit all stay accepted), the #945 array-of-zero-size rejection (`Array<Unit>` / a bare `[()]` is E135 at both the type-resolution and array-literal gates — emitted exactly once, the literal gate defers to the annotation when both apply (including a refined `{ @Array<Unit> \| p }` annotation, whose `RefinedType` the guard strips via `base_type`), and a zero-size `Array` param reports E135 once via the general exact-duplicate diagnostic dedup (PR #938); `Array<Int>` stays accepted), the #1204 quantifier-bound gate (E128 for array/String/Float64 domains; count form, `@Nat`, refined-integer, and TypeVar bounds accepted), the #1206 handler-state cell gate (E336 when the declared state type diverges from the builtin State effect's resolved `T` — `state_cell_decl_equal` on resolved types, since `is_subtype` conflates `Int`/`Nat` and erases refinements, with refined predicates compared structurally so a refined-vs-refined divergence is caught; aliases of `T`, a refined alias on both sides, and two textually identical refinement aliases stay accepted, a TypeVar cell defers to instantiation, and a user effect's handler state stays free), and the E337 builtin-effect handle arity gate (bare `handle[State]`, `State<A, B>`, and the Exn twin) |
| `test_checker_int_nat.py` | 8 | 153 | #755 — mixed `Int <op> Nat` arithmetic joins to the formal LUB `Int` (not `Nat`); direct `expr_types` observation that `@Int.0 - 2`, `@Int.0 + @Nat.0`, `@Int.0 * @Nat.0`, `@Int.0 / @Nat.0`, and `@Int.0 % @Nat.0` synthesise `Int` (the DIV/MOD pins kill a per-operator `numeric_join` bypass nothing else in the suite catches), with `Nat`/`Nat` → `Nat` and `Int`/`Int` → `Int` guards against over-correction |
| `test_checker_patterns.py` | 59 | 932 | Pattern matching, match-arm typing, exhaustiveness, pattern/match coverage, bidirectional inference, typed holes (#420 split) |
| `test_checker_functions.py` | 86 | 1103 | Function signatures, slot references, result refs, calls, control flow, higher-order, where-blocks (incl. #969 closed-scope isolation over bodies + contract clauses, nested-where hint targeting, handler-vs-where hint ordering), expression diagnostics, IO operations, string interpolation (#420 split) |
| `test_checker_effects.py` | 85 | 1,333 | Effect declarations, abilities, effect subtyping, async effect, handler typing (#420 split), and the #1149 built-in-effect redeclaration gate (E152: divergent and faithful `effect IO`, codegen-only `Exn<E>`, a registry-parametrised sweep, and a differential pinning the gate's name set to what `vera effects --json` publishes) |
| `test_db_effect.py` | 9 | 136 | #229 — the built-in `<DB>` effect: `DB.query` / `DB.execute` type-check under `effects(<DB>)` (E122 without it; E204 on a non-`String` SQL argument), plus `is_db_sql_op` — the predicate the #309 gate keys on — gating any `DB.query`/`DB.execute` by `parent_effect == "DB"` + op name (the same axis codegen routes to the host on), so a user `effect DB` shadow's op IS gated (it would still reach the host) while an unrelated effect's `query` is not — the shadow is itself rejected at its declaration since #1149 (E152), so this predicate is defence in depth; a checker↔codegen differential pins the gated set to the built-in DB ops |
| `test_db_marshalling.py` | 35 | 234 | #229 — the `<DB>` marshalling helpers: `Array<Option<String>>` params (inbound reader), `Array<Array<Option<String>>>` query grids (`_alloc_result_ok_rows`) and `Result<Int>` row-counts, round-tripped through an `InstanceCaller` over a real compiled module — each case run normally AND under `VERA_EAGER_GC=1` (every `$alloc` fires `$gc_collect`), the large-grid case forcing free-block reuse; mutation-validated (dropping a shadow-stack root corrupts the read-back / SIGBUSes the swept-pointer read) |
| `test_db_runtime.py` | 21 | 301 | #229 — the `<DB>` host binding (`vera/runtime/db.py`) on stdlib `sqlite3`: create/insert/select round-trips against `:memory:`, NULL cells → `None`, the affected-row count (incl. the `-1` DDL sentinel), a BLOB cell UTF-8-decoded with replacement, the `Err`-not-crash error path, an unopenable `VERA_DB_URL` deferred to an `Err` (not a host crash), and injection-safety (a malicious param binds as a literal, table intact); plus `_open_connection`'s `VERA_DB_URL` surface (memory + file URLs, in-memory default) and `register_db`'s bind/no-op paths |
| `test_sql_provenance_309.py` | 79 | 778 | #309 — the SQL literal-provenance gate (SQL injection as a compile-time error): non-literal SQL rejected `E207` (bare param slot, function result, `\(expr)` interpolation, `string_concat` with a runtime operand, let-bound runtime value, `if`-expression), literal / concat-of-literals / let-chain-with-shadowing / empty-string accepted, placeholder/param arity `E208` with quote- and comment-aware counting (named/numbered placeholders are rejected outright, `E209`), the `count_placeholders`↔sqlite3 differential (exact count accepted, one too many rejected), and gate scoping — a user `effect DB` shadow is rejected at its declaration (`E152`, #1149) *and* its runtime SQL still draws `E207` alongside it (defence in depth), an unrelated effect's `query` is not gated, and no `E207` cascade onto a mistyped SQL arg |
| `test_checker_modules.py` | 105 | 1,672 | Module-call diagnostics, cross-module typing, visibility enforcement, builtin redefinition (function E151 and effect E152 surfaced from a module into its importer), reserved function names (E153 — the contract state forms `old` / `new` and the keyword class `assert`/`assume`/`forall`/`exists`/`match`/`if`/`let`/`fn`/`true`/`false`, each top-level, `where`-helper, and module-surfaced, plus the `handle` host-invoked carve-out and the probe record behind both halves), parsed module calls (#420 split) |
| `test_checker_errors.py` | 56 | 866 | Error codes, resolution-coverage diagnostics, contracts, error accumulation (#420 split); cyclic type aliases incl. #1059 self-reference through a type argument (`Future<F>`, mutual `Future<B>`/`Future<A>`, `Array<L>`) rejected E132 |
| `test_checker_builtins_collections.py` | 97 | 848 | Map / Set / Decimal / Json / Html / Http / Inference built-in type-checking (#420 split) |
| `test_checker_builtins_strings.py` | 122 | 945 | String / numeric / type-conversion / float-predicate / string-search / markdown / regex built-in type-checking, removed-legacy-name regression (#420 split) |
| `test_obligations.py` | 427 | 1,521 | Reified proof obligations + warm `VerificationSession` (#222 Phase A): full-corpus differential oracle (warm session == cold `verify()` on diagnostics, summary, and obligation stream, plus warm-twice determinism, across all 42 examples and every verify/run-level conformance program), summary↔obligation tier-bookkeeping consistency (including the #967 `total == tier1_verified + tier3_runtime` leg, plus a focused self-consistency pin on the three call-demotion examples), per-kind unit tests (requires / ensures / decreases / nat_sub / call_pre statuses, counterexamples, error codes), content-key stability + same-text-two-sites span disambiguation, session solver reuse, type-error short-circuit, ADT-registry resync between programs; plus the Phase B incremental suite — identical-source full replay, callee-body-edit replays callers while callee-contract-edit invalidates them, span-shift and ADT-edit conservative invalidation, cross-program isolation, timeout-status never cached (monkeypatched solver), FIFO eviction bound; plus the #727 dedup pin — a violating call in a let RHS records exactly one E501 diagnostic and one call_pre obligation |
| `test_verifier_contracts.py` | 95 | 898 | Z3 verification over the example corpus, trivial/ensures/if-else/let/multi-clause contracts, counterexamples, tier classification, arithmetic, verification summaries, Diverge effect, edge cases, string-length + string-predicate verification (#839 split) |
| `test_verifier_nat_obligations.py` | 81 | 1,708 | **`@Nat` subtraction underflow obligation** (#520 — Path-A discharge via requires/path-conditions/path-aware Z3 refutation, pure-literal exclusion, Int-Int and Nat-Int exemptions) and **`@Nat` binding-site narrowing obligation** (#552/#747/#749 — Tier-1 `value >= 0` at let/call-arg/effect-op-arg/ctor-field/match-bind/destructure narrowing — a concrete site classifies `tier3_runtime` (codegen-guarded) while the effect-op argument and generic-instantiated constructor field classify `E504` (obligated but unguarded, #754/#757), walker-recursion pins, `_narrows_into_nat` verifier/codegen soundness parity; PR #972 clone-instantiated side-table substitution — a `Some(@T)` bind in an `Option<Nat>`-instantiated clone is no narrowing, genuine clone-path narrowings still obligated); #1201 — a builtin `Tuple<Nat, Nat>` parameter's match-bound components carry their declared component facts (a valid ensures over one proves instead of falsely violating) and an `Int` component bound as `@Nat` fires one loud `E503` per component, both mutation-caught (#839 split) |
| `test_verifier_primitive_ops.py` | 39 | 662 | **Primitive-operation safety obligations** (#680) — division/modulo by-zero `E526` and array-index-bounds `E527`, the in-bounds/out-of-bounds two-check with float-exemption, honest Tier-3 for opaque lengths, off-by-one and lower-bound pins, De Bruijn-correct fix hints (#839 split) |
| `test_verifier_calls_modules.py` | 74 | 1,985 | Call-site preconditions (incl. branch-aware), pipe-operator verification, cross-module contracts (#839 split); #764 — block translation continues through a `let`-destructure (E501 fires at/after it, De Bruijn component order pinned with a mutation-caught reversed-order check, ensures over the block result proves Tier 1, the #730 statement-position product case, and the pre-fix before-destructure guard); #1199 — an untranslatable `let` value binds a span-keyed opaque constant (violating call after it fires E501, `assert` repairs the proof via #804, two effect-op lets are never provably equal, an ensures depending on the opaque value demotes E522 rather than falsely violating — the taint gate, mutation-caught; a registered user `data Tuple` routes through the registry constructor path, pinned by an isomorphic-rename differential and an uncached-instantiation demotion check, both mutation-caught) |
| `test_verifier_fresh_scope.py` | 46 | 1,106 | Fresh-scope obligation walking (#779/#985): primitive ops and binding sites inside closure bodies, quantifier predicates, and handler clauses are obligated Tier-3 under the empty fresh-scope slot environment — with scope-honesty soundness pins for BOTH walkers (a closure param or clause payload never proves against the outer requires; mutation-derived, each killing a full-suite-surviving mutant) — quantifier domains, handler state-inits, and handler bodies walk at enclosing-scope full precision (Tier-1 from requires), manifest violations in closures stay loud (E526/E527/E507/E503), a refined closure narrowing discloses `tier3_unguarded` + E506, assert/assume conditions are descended by the nat-binding walker, ensures-position quantifier predicates record Tier-3, a nested closure's return widening/narrowing is reported matching codegen's lifted-closure guards, the #1203 boundary obligations fire through a scalar `State<T>` alias exactly as their codegen guards do (loud E503 init/put through `type Count = Nat`, Tier-1 from requires — #1205 obligation↔guard parity), and the E533 per-instantiation state-declaration recheck is pinned both ways (a concrete `(@Nat = ...)` on `handle[State<T>]` at T=Int is loud with the failing instantiation named; the honest `@T` control is clean with zero `state_decl` obligations) |
| `test_verifier_adt_decreases.py` | 22 | 791 | Match/ADT verification, decreases measures (incl. ADT decreases), mutual recursion (#839 split) |
| `test_mutual_recursive_sorts_881.py` | 15 | 317 | #881 mutually-recursive `data` declarations — Z3 sort construction for a mutual group (issue repro, 3-cycle, one-base-case pair, Float64-field pair) declared together via `z3.CreateDatatypes` rather than recursing unboundedly into fresh sort creation (which otherwise raises a raw `RecursionError` on a check-green program); plus the `Tuple`-mediated cases (self-recursion `MkC(Tuple<C, Int>)` and a well-founded mutual pair through a `Tuple` field), where a fresh `Tuple` sort build re-entered the same `RecursionError`; pins non-FP mutual equality (direct and `Tuple`-mediated) as Tier-1 and recursive-FP mutual equality as a loud Tier-3 (#871 interaction), with a mutation-kill that re-raises `RecursionError` when the direct or `Tuple`-mediated group construction is reverted |
| `test_adt_float64_eq_871.py` | 9 | 306 | ADT equality over Float64 fields: per-field fpEQ soundness differentials (NaN, signed zero), multi-constructor recognizer guards, recursive-ADT Tier-3 demotion (#871) |
| `test_adt_ord_reject_921.py` | 40 | 676 | #921 `compare`/ordering on a user ADT is rejected (`E242`) rather than returning a silent wrong result — the `Ord` ability op's bare type variable is now constrained to the §4.5/§9.8.1 orderable primitives (`Int`/`Nat`/`Float64`/`Byte`/`String`); covers simple/recursive/enum ADT rejection, constrained-generic accept vs ADT-instantiation reject, the diagnostic naming the offending type, the `ensures`-position no-traceback pin, primitive `compare` still checks + runs, structural ADT `==` untouched, and a Tier-1 verify + false-`ensures` rejection differential |
| `test_adt_eq_reject_928.py` | 23 | 447 | #928 `==`/`!=`/`eq` on a non-Eq-derivable type is rejected (`E243`) rather than a silent pointer-identity comparison — the equality sibling of #921; covers function-typed `==`/`!=`/`eq()`, `State<Rec>`/composite-with-`Map`-field, direct `Map`/`Array`-field ADT reject (upgraded from a late `E613`); positive controls (Int/String/Bool, `Box`, `List<Int>`, `Option`, `Result`, nested-generic `List<List<Int>>`) still check + compile + run to the correct structural-equality result; plus the **checker↔codegen Eq-derivability differential** (both real predicates over a shared corpus) and codegen ground-truth pins, mutation-validated |
| `test_verifier_refinements.py` | 62 | 1,462 | Refined Bool/String/Float64 param sorts, **refinement-predicate translation + verification** (#746 — Tier-1 discharge at narrowing/return positions, E505 with counterexample, E506 Tier-3 for untranslatable predicates, the R3 already-refined exemption, refined-ADT-sub-pattern arm-fact carry into `@Nat` narrowings and call preconditions, alias-base refined returns, refined returns from match arms) (#839 split) |
| `test_verifier_shadow_audits.py` | 71 | 1,377 | **Per-monomorphization generic verification** (#732 — per-instantiation body verification, collapsed-type-var De Bruijn reindex soundness, one-diagnostic dedup, decreases-only discovery, Tier-3 `E520` residual) and the **#680 shadow/projection audit battery** — 57 differential tests pinning the safe→verified / opaque→Tier-3 / unsafe→loud trichotomy across compound shadows, destructure De Bruijn alignment, opaque match scrutinees, and intra-block scoping; **mutation-validated** (every test flips RED when its target machinery is broken) (#839 split) |
| `test_verifier_mutation_obligations.py` | 38 | 883 | #387 mutation-hardening: obligation-record completeness and projection-helper pins (#839 split) |
| `test_verifier_mutation_gates_smt.py` | 52 | 1,317 | #387 mutation-hardening: the verifier's soundness-gate predicates, generic-instantiation aggregation/meet logic, and SMT translation pins (#839 split) |
| `test_soundness_392.py` | 36 | 584 | #392 audit batches 1–2 — verifier soundness/completeness fixes: signed div/mod truncate toward zero (#799), body `assert(P)` carries a Tier-1 obligation (#800), divisions in contract predicates carry a `div_zero` obligation (#801), and the #804 assume-half of #800's `assert` rule — a prior `assert`/`assume` discharges later obligations (including a later call's precondition) + the postcondition at Tier 1, removing false E501/E503/E500/E505 |
| `test_int_overflow.py` | 6 | 143 | #798 — `@Int`/`@Nat` arithmetic-overflow obligations (part of the #392 `smt.py` soundness audit): `+`/`-`/`*` on `@Int`/`@Nat` now emit an `int_overflow` obligation (the analog of `nat_sub`/`div_zero`) rather than modelling the operands as Z3's unbounded integers, so a `ensures(@Int.result > @Int.0)` over `@Int.0 + 1` no longer proves a contract the i64/u64 runtime violates under two's-complement wraparound. Unbounded operands leave the obligation undischarged (Tier-3, runtime-guarded); operand bounds that prove the result stays in range discharge it at Tier 1 |
| `test_int_overflow_codegen.py` | 62 | 718 | #798 Stage 3 — runtime overflow-trap codegen: the codegen emits a guard at *exactly* the `@Int`/`@Nat` `+`/`-`/`*` sites the verifier obligates, so `vera run`/`vera compile` programs trap on overflow instead of silently wrapping at the i64/u64 boundary. #808 wired the guard to the `vera.overflow_trap` host import, so the trap now classifies `kind="overflow"` (carrying the overflow Fix paragraph) rather than the generic `unreachable`; `TestOverflowTrapKind808` pins that, with controls proving the #520 `nat_sub` underflow and #813 `@Nat`→`@Int` widen guards still classify `unreachable` |
| `test_int_overflow_differential.py` | 211 | 398 | #798 Stage 3 verifier↔codegen classification differential (cross-component soundness rule): the codegen overflow guard must fire at exactly the sites the verifier obligates *and* classify each site's operand type (`@Int` i64 vs `@Nat` u64) identically — else a Tier-1-clean program traps spuriously or a wrapping op slips through unguarded. Over a corpus exercising all five operand combos plus the literal-left ambiguity (a naive codegen mis-classifies it as `@Nat`), asserts the verifier's per-site gated classification equals the codegen's site for site, both sides driven by the same `ast.span_key` |
| `test_nat_int_widening.py` | 35 | 576 | #813 — `@Nat -> @Int` widening coercion obligation (dual of #552 `nat_bind`, part of the #392 soundness audit): a `@Nat` in (i64.MAX, u64.MAX] reinterprets when widened (u64.MAX → -1), so a `nat_to_int_coerce` obligation that the value is `<= i64.MAX` now fires at the return position — provably-in-range → Tier-1, provably-out-of-range (`@Nat.0 >= 2**63`) → loud E530, unbounded → honest Tier-3 (runtime-guarded), with an `@Int -> @Int` control that must not fire. The #813 follow-up adds the explicit `nat_to_int` built-in and heterogeneous `if`/`match` arms with a non-negative-literal alternative; #820 adds the heterogeneous-`@Int`-slot arm, closure argument, and closure return/capture obligations (each per-arm / per-site, with `@Int`-arm and `@Nat`-formal controls that must not fire) |
| `test_int_widening_codegen.py` | 52 | 535 | #813 Stage 3 — runtime `@Nat -> @Int` widening-trap codegen: the codegen emits a guard at *exactly* the `@Nat -> @Int` coercion sites the verifier obligates (return, `let`, call argument, and — since #820 — array element, tuple construction/destructure, heterogeneous `if`/`match` arm, closure argument/return), so `vera run`/`vera compile` programs trap when a `@Nat` above i64.MAX would reinterpret to a negative `@Int` instead of silently returning the wrong value. The trap is a bare `unreachable` (shares `_emit_negative_i64_guard` with the #552 nat-bind guard), classified `kind="unreachable"` today (a dedicated widening trap kind is a follow-up) |
| `test_int_widening_differential.py` | 26 | 320 | #813 verifier↔codegen behavioural differential (cross-component soundness rule): at every `@Nat -> @Int` coercion site the verifier's `nat_to_int_coerce` classification must AGREE with the runtime — a `tier3` (codegen-guarded) site MUST trap on a `@Nat` above i64.MAX (return / `let` / call-arg / constructor field / ADT sub-pattern / match-bind, and the #820 array-element / tuple-component / heterogeneous-arm / closure argument-return sites), while a `tier3_unguarded` (E531) site must NOT trap (the generic-instantiated `@Int`-field coercion codegen cannot guard).  Runs BOTH sides on one corpus so the "runtime-guarded" claim is checked against the actual trap — catching a verifier deferral codegen never guards (unsound silent -1) or a spurious trap |
| `test_nat_narrowing_return_differential.py` | 134 | 2,757 | #758 verifier↔codegen behavioural differential (cross-component soundness rule): at the function-return `@Int -> @Nat` coercion slot the verifier's `nat_bind` verdict must AGREE with the runtime — an unproven narrowing leaves the return obligation undischarged (loud E503, or an honest `tier3` for an opaque value) and codegen's return guard TRAPS on a negative input, while a proven narrowing (`requires` / path condition) discharges at Tier 1 and the guard is dead (`vera run` returns the value, no trap).  Runs BOTH sides on one corpus so "the verifier obligates this return" is checked against the actual guard — the return-position dual of `test_int_widening_differential`.  #983 review adds the `tier3` quadrant (opaque `float_to_int`, verify + compile in one run), `let_before_tail` / `nested_if_join` join shapes, a `type Count = Nat` alias case, and threads `file=` + `resolved_modules=` through the verify side for CLI-pipeline fidelity.  #1017 adds the `apply_fn` ARGUMENT-narrowing quadrant (the `@Int -> @Nat` dual of the #820 argument widening): a provably-negative arg is E503, a runtime arg is obligated + `call_indirect`-guarded (run traps), a `requires`-bounded arg proves Tier 1, a `@Nat -> @Nat` arg is unobligated, and an opaque `float_to_int` arg records `tier3` with the codegen `i64.lt_s`/`unreachable` guard emitted (verify + compile cross-checked in one pipeline run).  #1024 adds the REFINED apply_fn-argument quadrant (`refine_bind`, the refinement dual of #1017): an argument narrowing into a `{ @Nat \| @Nat.0 > 0 }` closure formal discharges the FULL predicate refined-first — a constant `0` is E505 (clears the `@Nat` base's `>= 0` but violates `> 0`), a runtime arg is obligated + guarded at the lifted closure's prologue (run(0) traps with a `contract_violation` Refinement-violation message), a constant `5` / `requires`-bounded arg proves Tier 1, and a `@Pos -> @Pos` arg is unobligated.  #1032 adds the REFINED closure-RETURN quadrant (the return-side dual of #1024): `fn(@Int -> @Pos) { @Int.0 }` records exactly one tier3 `refine_bind` (opaque body — never a false Tier 1), run(-5) AND run(0) trap at the lifted body's return guard with the "return value" refinement message, a satisfying value passes, and the always-satisfying body stays an honest tier3 with no spurious trap — plus the re-derived single-guard pin (exactly one `contract_fail` refinement check in the lifted body, zero `i64.lt_s` narrowing checks).  PR #1202 adds the #1203 handler-boundary quadrants (init/put/with/resume × trap/pass/zero, bare-put and clause-body-put dispatch shapes, widen duals at U64_MAX with i64.MAX boundary controls) and the #1205 scalar-alias family quadrants: alias and refined-alias `State<T>` cells compile and run, every #1203 guard keys through the alias (init/put trap on negatives, widen dual at U64_MAX), the alias-equal annotation binds clause slots under its SOURCE name, a stateless handler's clause `@T.0` reaches the op ARGUMENT (the pre-fix capture skew read the cell — pinned in both directions), `Exn<Code>` compiles with the payload bound under the clause pattern's name, `old(State<Count>)` snapshots through the collapsed family, and the retired lying-annotation fixture is pinned as check-rejected E336.  The second adversarial round adds the clause-scope checker-parity battery (mixed-spelling State and Exn shapes bind under the checker's canonicalized argument names, both patternless twins bind nothing, the declaration-scope shadow probe), the parameterised-alias family differentials (`State<Id<Nat>>`, alias-of-generic-alias, `Exn<Id<Int>>`), and the `State<Byte>` write-boundary battery (init/clause-put/bare-put/`with`/resume literals at i32) |
| `test_hetero_widen_tailcall.py` | 21 | 312 | The heterogeneous per-arm widen guard vs tail calls (#986) and targets: an arm whose `@Nat` value is a tail call must lower to a plain `call` so the appended guard stays live (`return_call` would skip it — the widening dual of the #983 per-leaf narrowing), the genuine `@Int` arm's recursive `return_call` keeps TCO (100k-depth run), the gate is target-aware (`_is_hetero_int_widen_join`: a hetero join in a `@Nat`-returning context must NOT widen-guard its legal `@Nat` arm — the target-blind gate false-trapped 2^63), and a user `data Tuple` must not take the builtin variadic carrier's target-table path (verifier emits no obligation there; guarding it was an opposite-direction desync) |
| `test_xmod_span_collision.py` | 4 | 156 | #987 — the span-keyed target-type table is single-module (keyed by bare span, no file identity): an imported body's expression span can coincide with a main-file entry. #987 threads each module's OWN table into codegen (`CheckArtifacts.module_artifacts` → `_compile_fn(module_tables=...)`), so the engineered line-for-line collision pair now proves the legal all-`@Nat` imported function is not falsely widen-guarded by CORRECTNESS (its own table targets `Tuple<Nat, Nat>`), not merely suppression — with a `thread_modules=False` control pinning the #986 suppression fallback still holds when no module tables are threaded, and a same-file control proving top-level guards unaffected |
| `test_xmod_widening_differential.py` | 18 | 293 | #987 verifier↔codegen widening differential run THROUGH THE IMPORT DOOR (the same-file `test_int_widening_differential` was green while this door was open): for each cross-module shape (array-element, tuple-construction, tuple-destructure control, transitive 3-level, and shadowed-import) the library's standalone verify must classify the `@Nat -> @Int` coercion Tier-3, AND the importing program compiled the way `vera run`/`vera compile` compile it (per-module tables threaded) must TRAP at `u64.MAX` — never the silent -1 — while passing `2^63-1` and `42` unchanged.  Pins that the #820 array/tuple-construction guards, recovered from the span-keyed target table, now fire for imported bodies.  Also pins the import-door trap is the guard's bare `unreachable` net (not some other trap), and a two-independent-libraries-both-widen scenario asserting BOTH imported bodies trap at `u64.MAX` (kills a first-module-only partial-collection mutant) |
| `test_xmod_artifact_collection.py` | 5 | 205 | The per-module `CheckArtifacts.module_artifacts` pass is OPT-IN (`collect_module_artifacts=`, default off) because only the codegen-bound callers consume it and it is O(N²) sub-checks in the module count.  Pins that `typecheck_with_artifacts` WITHOUT the flag leaves `module_artifacts` empty (the `vera verify` / warm-session path pays nothing) and WITH it collects each resolved module's own table; plus the GAP-1 artifact-level pin — in a transitive fixture (`main -> alib -> blib`) the middle module `alib`'s target table has 2 entries only because its `direct` flags are re-derived from its OWN imports (a first-module-only / top-level-flags mutant drops it to 1) |
| `test_xmod_generic_widen_gap.py` | 15 | 413 | #998 guarded differential: an imported **generic** function's mono clones carry their origin module and compile against ITS span tables, so the #820 widen guards fire at every instantiation through the import door.  For the array-element and tuple-construction sites × `T=Bool`/`T=Int` instantiations, the standalone library verify must promise Tier-3 AND the importer must trap with the guard's bare `unreachable` at `u64.MAX` (never the silent `-1`) while in-range values round-trip — through both the bare-call and shadowed (`lib::wrap` → `mod$…`) doors, plus a hoisted-where-helper-widen scenario (the per-clone hoisted copy inherits the clone's origin) and a local-generic control (local clones keep the main-file tables) |
| `test_xmod_ability_ops_992.py` | 5 | 156 | #992 imported-body ability-op rewrite: `eq` in an imported top-level fn, its where-helper, and a nested grandchild; `compare` (the other AST-rewritten ability op); and the shadowed (`mod$…`, Pass 2.6) door — each runs end-to-end through the import door (a raw call would drop the body and dangle the importer's call) |
| `test_xmod_where_helper_import_991.py` | 3 | 190 | A non-generic where-helper's name (#991) no longer suppresses a same-named IMPORT's bare emission — the shadow set is collected from the POST-hoist program, so the import wins outside the parent (spec §5 helper locality) while the parent's body call reaches its own hoisted helper (`go(0) == 701`, both doors observed; a stale bare-name shadow would dangle `unknown func` or silently capture the import-bound call).  Controls: a TOP-LEVEL local sharing an import's name still shadows it (§8.5.2), and an UNINSTANTIATED T-unused generic helper's name still shadows (its template still emits bare; dropping it would duplicate the import's bare emission) |
| `test_generic_where_helper_990.py` | 10 | 339 | #990 nested-generic monomorphization: a `forall<T>` where-helper under a NON-generic parent is a mono base — the issue repro (direct instantiation), the grandchild variant (all-non-generic ancestor chain), two instantiations (`T=Int` + `T=Bool`) both emitted, and WAT-level single-emission pins (exactly one `gid$Int` clone, no bare `@T` template); plus the #904 control (helper under a GENERIC parent stays hoisted per-clone, no standalone duplicate) and the own-where-child shape (the generic's T-dependent and T-independent children are hoisted per-clone only — the Pass-2 where-fn sweep stops at the generic template) |
| `test_codegen_where_helper_mangling_991.py` | 13 | 553 | #991 non-generic where-helper name collisions: parent-qualified mangling (`compute$where$branchA$where$leaf`) so two siblings' same-named nested helpers, and a helper named like a top-level function, compile and run each their OWN body (RUN-value assertions — sibling `leaf`s summing to a value only distinct bodies yield, nested-helper vs top-level both reachable) instead of crashing WAT assembly with `duplicate func identifier`; plus WAT name-scheme pins (top-level names stay bare, nested helpers mangled), full lexical resolution (a grandchild calling an ancestor-scope "aunt", and an inner helper shadowing an outer same-named one), a collision coexisting with a nested generic (`gid$Int` still emitted), the generic-subtree capture battery — a generic helper's call to its OWN nested `shared` must not be captured onto an ancestor's hoisted name (silent-wrong-value shape, the false-Tier-1 verify+run differential, the unshadowed-ancestor-call no-regression guard, and a generic child's name shadowing an ancestor's) — and the CHECKER leg: a differing-signature diamond (`@Int -> @Int` vs `@Int -> @String` leaves) that the flat last-wins lookup falsely E121'd must check clean AND run to the three-subsystem-agreement value |
| `test_monomorphize_differential.py` | 45 | 1,720 | #732 differential soundness: the verifier's per-monomorphization instantiation discovery covers every instantiation codegen emits (name coverage + per-generic count), over real generic programs (conformance ch02/ch09, `examples/generics.vera`) plus inline cases for the soundness-critical scenarios — collapsed type vars, **prelude combinator emission** (`option_map`), transitive generics, a generic whose type arg is fixed only by a **where-helper's return** (a `Float64`-returning helper, so the unresolved-var `"Bool"` phantom default cannot mask a miss), a generic whose type arg is fixed only by an **imported constructor** (`id2(MkBox(7))` — the verifier's mono-context must include `_module_constructors`, else it phantom-defaults and misses codegen's `id2<Box>`), a generic whose type arg is fixed only by an **imported function's return** (`id_g(make_int(...))` — the verifier's mono-context must seed `fn_ret_types` from imported functions, else it phantom-defaults and misses codegen's `id_g<Int>`, plus a **private-shadow** case pinning the imported-fn seeding stays unfiltered like codegen since filtering would diverge into a false Tier-1), and a generic reached only through a **contract clause or `where` helper** (codegen must seed Pass 1.5 from the shared node-level walk, not just `decl.body`, or it skips the clone → `CodegenSkip` at run time) — so a missed instantiation (a false Tier-1) is caught. Guards against a vacuous pass when codegen emits nothing, plus a **determinism guard** (`vera compile --wat` is byte-stable across `PYTHONHASHSEED` — the mono worklist sorts its instantiation sets); plus the #899 **call-rewrite↔emitted-clone differential** (`test_call_rewrite_matches_emitted_clones`) — the THIRD consultor the verifier⊇codegen check never exercised: captures every mangled target the WASM call-rewriter (`_resolve_generic_call`) resolves and asserts each is an actually-emitted clone, over user-fn-return-into-generic-arg shapes (a non-generic user fn returning `Option<Decimal>`/`Result<Decimal, String>` in `Option<T>`/`Result<T, _>` position; a scalar-resolving alias `type Age = Int` and a named refinement in bare `@T` position; and a non-generic user fn returning a LITERAL parameterized type `Option<…>`/`Result<…>`/`Box<…>` bound to a bare `@T`, where discovery keys the clone by base name `pick_last$Option` — the base-name key is sound because a bare-`@T` body is representation-polymorphic) — a dangling target is the check-green-then-`run`-drops-`main` desync.  All three consultors (discovery, verifier, call-rewrite) route the user-fn-return clone key through ONE shared `declared_return_clone_key`, so they cannot desync by construction.  The #898 cross-argument merge (`eq2(MkErr(5), MkOk("x"))` — one argument fixes each of a sparse `Res<A, B>`'s two parameters) is in BOTH corpora: a symmetric collapse of the merge trips the inline differential's vacuous-emission guard (codegen emits nothing once the type under-determines), and an asymmetric one-sided merge surfaces in the call-rewrite differential as a dangling bare `eq2$Res` clone |
| `test_codegen_expressions.py` | 89 | 787 | Int/Bool/Float64 literals, slot refs, arithmetic, comparison, boolean logic, unary ops, if/let, function calls, recursion, pipe operator, `CompileResult` surface (#419 split) |
| `test_codegen_calls.py` | 32 | 1,402 | Statement-position unit calls (#556), **WASM tail-call optimization** (#517 — `return_call` emission, 50K- and 1M-iteration stress, structural `return_call`/plain-`call` boundary assertions, **GC-aware TCO for allocating fns** (#549 — `$gc_sp` restore before each `return_call`), postcondition-fallback regression, analyzer unit tests over tail-transparent constructs), pair-typed closure params + captures (#535) (#419 split) |
| `test_codegen_infrastructure.py` | 24 | 455 | Module assembly import/memory conditionals, execute error paths, unsupported-construct skips + node-level E602 reasons (#626), built-in shadowing (#154), typed holes, example round-trips (#419 split) |
| `test_codegen_interpolation.py` | 35 | 1,321 | String interpolation, the E615 loud inference-fallthrough channel (#630) (#419 split) |
| `test_codegen_effects.py` | 115 | 2,562 | State\<T\> host imports, effect handlers, Exn\<E\> handlers (incl. expression-bodied, #475), Async/Future\<T\>, Random effect (#419 split); plus the #841 concurrent-Async battery (`TestConcurrentAsync841`) — fused `async_http_get`/`async_http_post`/`async_await` import pins, sync-import suppression, pure-shape eager pin (no task imports), kind-4 `register_wrapper` structural pin, a generic-fn-with-concrete-Future-return await classification pin, the behavioural two-gets-overlap test (local `ThreadingHTTPServer`, server-side request-log ordering, no wall-clock), and the #843 indirect-closure Ok-path pin (payload byte-exact through `await(apply_fn(...))`); plus the #1109 alias-Future battery (`TestConcurrentAsyncAlias1109`) — alias-typed let, alias-declared fn return, two-hop alias chain, and payload-alias (`Future<R>`) shapes classify for the fused-handle check (import pins + byte-exact Ok payloads), plus the aliased two-gets-overlap behavioural pin |
| `test_state_clause_semantics.py` | 27 | 696 | #976 intrinsic-hybrid State clause semantics: clause bodies execute (get-transform 105/30), `with` overrides the intrinsic store (10), the pre-store capture makes `with @T = @T.0` keep-old (7 — the corpus-migration canary); composite (heap) state transform + a captured-pointer-read-after-alloc shape; non-tail `resume` skips loudly; canonical clauses pinned as exact identity (99, and the spec §7.5.3 counter anchor 10); #1006 effect ops as array-literal elements (identity + transforming get clause, and the declared-`effects(<State<Int>>)` helper covering the second op-injection site) |
| `test_codegen_data_types.py` | 93 | 1,864 | ADT metadata + constructors, match expressions (incl. nested patterns), tuples (incl. the #902 zero-size `Unit` component in a by-value Tuple / user-ADT layout — construct, match-extract, multi-Unit, Unit in any position, and a side-effecting `Unit`-returning call field `Tuple(IO.print(...), n)` all compile + run; the #1031 transparent `Future<Unit>` component erasing like bare `Unit` through both let-destructure and match, incl. an alias to the compound and an alias-of-alias chain; and the #1037 alias to a representable compound `type FI = Future<Int>` binding a real local through destructure, match, an alias chain, and a standalone let), ADT string fields, generic-monomorphization regressions (#604, #767) (#419 split) |
| `test_codegen_structural_eq.py` | 58 | 1371 | Structural `Eq` auto-derivation (#773): String-field ADTs compared by content (distinct `string_concat` allocations), nested-ADT fields compared by value not pointer, 2-level recursion, a recursive generic ADT (`List<Int>` — the self-calling `$eq_` function + deep `List<T>` param substitution), a mutually-recursive ADT pair, `P<String>` wrapping `Box<T>`, `Box<String>` under an `Eq`-constrained generic, type-alias fields (alias-to-Int/String/ADT/refinement + 2-hop chains resolve before Eq dispatch), NaN-field runtime consistency with primitive `==`, Byte fields, loud E613 for `Map`/`Array`/`Set`-field ADTs on the generic path AND for direct `==` (Map-field, Md-builtin, ctor-inferred bare generic, and the always-true `Tuple` placeholder), the checker↔codegen derivability differential, the #772 constructor-path lockstep probe, and the #898 sparse-multi-type-parameter probe (a fully-determined `Res<Int, Int>` derives + compares by value on the ctor path; the under-determined `id1(MkErr(5))` — `A` free — reports the clearer E619 not the misleading E613; the determined-but-non-Eq `Res<Array, Int>` soundness gate stays E613; the cross-argument merge `eq2(MkErr(5), MkOk("x"))` compiles + runs the `Res<String, Int>` clone; a determined-non-Eq cross-arg type is E613; the E619-accuracy split — a recovered non-Eq component `Res<A, Array<Int>>` or a structural non-Eq field `W<A,B>{K(Array<A>,B)}` is E613, an all-known-Eq free-param case stays E619); and the #923 nested-generic direct-`==` probe (a `List<List<Int>>` / 3-level `List<List<List<Int>>>` / `Chain<Pair<Int>>` operand inferred from constructor calls derives + compares by value where a one-level type-arg recovery would spuriously E613; the `eq(...)` builtin form matches; a non-Eq nested component `List<List<Array<Int>>>` stays E613); and the #932 generic-call sibling (the same `List<List<Int>>` / 3-level / `Chain<Pair<Int>>` nesting reached THROUGH an `Eq`-constrained generic call `eq2(@T, @T -> @Bool)` derives + runs where a one-level clone-path recovery would spuriously E613; a non-Eq nested leaf stays E613 — the fix recurses the derivability-name recovery without changing the mangled clone name) |
| `test_codegen_zero_size_fields_1043.py` | 22 | 463 | Registered constructor layouts erase zero-size fields (#1043): the layout differential — registered `field_offsets`/`field_types` for a bare `Unit`, `Future<Unit>`, or alias/alias-chain field (erased first, last, and multi-erased) match construction's `"unit"` (size 0 / align 1) convention — plus every consumer end-to-end: a wildcard-over-erased nested match extracts the real value (not zeroed fresh-alloc memory), structural `Eq` over an erased field first / multi (equal compares equal, distinct stays false), `show` renders the field as `unit`, `hash` is payload-sensitive (not garbage), no-erased-field controls stay green, and the builtin variadic `Tuple` wildcard-over-erased still LOUD-skips (E602, not silent); a dedicated `Future<Unit>` end-to-end block (construct via `async(())` + wildcard-match + `Eq` + `show`, exact values) pins that `async(())` construction is not blocked by any skip; mutation-validated (each edit site reverted independently flips its consumer's tests RED) |
| `test_codegen_orphan_call_indirect_1185.py` | 9 | 433 | No `call_indirect` reaches the output without a table to dispatch on (#1185), the unclosed half of the #1100 class: an [E602] skip swallowing a module's ONLY closure rolled the lift back, suppressing the `(table)`/`(elem)` sections while every surviving carrier kept its indirect call — an uninstantiable module emitted with zero error diagnostics, raw `unknown table 0` on the first call to ANY export. Both carrier shapes are pinned (the `apply_fn` special form on a closure-typed parameter, and a monomorphized clone of prelude `option_map` — the clone's drop attributed to `<prelude>`, not to whatever the user's file holds at that line), plus the no-closure-anywhere shape that previously produced NO diagnostic at all; each asserts the [E620] chain names the [E602] root with its location and that the unrelated victim export RUNS (41). Over-correction controls, green before and after: a surviving closure keeps the table so the `apply_fn` carrier is NOT dropped and still computes (107), the `array_map`/`array_fold` emission site likewise (63), and a closure-free program has neither. Mutation-validated — neutering the carrier seeding flips exactly the three orphan tests RED with the controls green, and un-hardening #1100's acceptance helper on the same broken module makes it pass again. The exception-path lift skip (a raise ESCAPING `_lift_pending_closures`, unreachable from a check-green program today) is pinned by a stubbed-lift regression asserting the carrier's [E620] names the root rather than claiming the program creates no closure |
| `test_codegen_skip_propagation_1100.py` | 8 | 325 | A codegen skip propagates to (transitive) callers before module assembly (#1100): the repro (helper skipped, `main` calls it — clean [E620] warning naming caller + root, no raw wasmtime `unknown func` text, module still assembles), depth-2 transitive drops in BOTH declaration-order permutations (caller-first needs a second fixed-point round, so a single-sweep propagation goes RED), root-cause naming with the skip's line embedded and the E620 located at the caller's declaration, an untouched public sibling that keeps its export and RUNS (41 — no fallback coincides), mutual-recursion termination (ping/pong cycle + skipped callee drops all three callers, sibling still runs), the closure shape (the dangling call lives in the lifted closure's WAT; the parent drops via the construction edge and the stub keeps table indices valid), and a no-callers control (root E602 only, no E620, everything else untouched); mutations — single sweep, dropped closure edge, dropped stubbing, hop-instead-of-root threading — each killed by a named test |
| `test_dropped_entry_1183_1186.py` | 21 | 561 | A dropped entry function is refused, never silently replaced (#1183), and an imported body's skip locates in its own module (#1186). #1183: the repro — declared `main` dropped, one public sibling surviving — exits nonzero with `main` and the root [E602]/[E620] named, and the sibling's 4243 sentinel (a value no fallback, default, or error path produces) never appears on stdout; the same for an explicit `--fn`, for the `--json` envelope (`ok: false`), and at the `execute()` library boundary; `CompileResult.dropped_fns` is pinned as the reified source of the refusal; the `Compilation notes:` block appears when a sibling survives (the ungating); auto-selection survives for the never-declared case and prints a one-line stderr note naming its choice; zero-export `compile` exits nonzero in both text and JSON; and the browser bundle refuses a dropped `main` using the SURVIVING-sibling fixture, so a non-empty export list rules out the zero-export check as the cause. #1186: the root E602 carries the MODULE's path with module-local line/column and quotes the module's source line, the [E620] cross-file prefix fires with its exact wording derived from the root's own location, a same-file control keeps the bare `at line N, column M` form, and `vera test` names the [E602] root instead of calling a public-but-dropped function private. Mutations — api.py refusal, CLI refusal, the E620 drop record, the module source scope, the tester reason, the notes ungating, the auto-select note, the zero-export gate, the browser refusal — each killed by a named test |
| `test_imported_trap_source_map_1189.py` | 8 | 342 | An imported function's runtime trap frame names ITS module's file (#1189), the source-map sibling of #1186's diagnostic fix. Fixtures split the basenames (`chinchilla.vera` module, `stargazer.vera` importer) so a frame's attribution is decidable from the string alone, and every trap is a precondition violation so `WasmTrapError.kind` is pinned. Covers the three doors: an imported non-generic fn (pre-fix `<unknown>` — never registered on the main generator), a monomorphized clone of an imported generic (pre-fix the IMPORTER's path with the module's line range, which in the fixture names a real-but-unrelated importer function), and the `mod$…` emission of a locally-shadowed import (whose rightmost-`$` strip yields nobody's entry). Asserted at the `cmd_run` text backtrace (per-frame line, never the whole stderr blob — `main` legitimately names the importer), the `--json` frames array, `fn_source_map` itself, and `execute()`'s `WasmTrapError.frames`. Over-correction control: a wholly main-file trap keeps the main file, green before and after. Mutations — the module file on the Pass-0.5 registrar, the bare-name harvest, the mangled-name mirror, the Pass-1.5 module source scope — each killed by a distinct named test |
| `test_codegen_typeparam_unit_wildcard_1060.py` | 31 | 959 | Wildcard over a type-parameter field instantiated to `Unit` (#1060), the type-parameter sibling of #1043's declared-`Unit` field: a WILDCARD over `Box<T>` field `T` used to advance the match offset walk by the generic `i32` width, so on `Box<Unit>` (field erased to 0 bytes) every later field read four bytes high — silently check-green. Bug-manifesting shapes go end-to-end (`Box<Unit>` trailing-`Int`, `Named<Unit>` `String` read-back, `Entry<Unit>` nested-ctor tag, `Bool`-following, second-type-parameter, and a nested-generic `Outer<Unit>` wrapping `Inner<Unit>` that exercises the deeper-recursion type substitution); controls stay green (before-erased field, trailing wildcards, `Option`/`Result<Unit>` builtins, `Box<String>`/`Box<Int>`/`Tagged<Unit>` alignment-coincidence, structural `Eq`/`show` recompute path); the direct-call boundary is pinned (#1065) — a `match mk() { … }` scrutinee recovers its concrete instantiation from the callee's declared return type, so a wildcard followed by a read now compiles and reads the real value (`Box<Unit>` trailing-`Int`, `Entry<Unit>` nested-ctor, `Named<Unit>` `String` read-back) instead of the sound #1060 interim LOUD-skip, while a trailing direct-call wildcard still compiles; the generic-call sibling (#1072) resolves the declared return's type variables from the call site (`P2<T, Unit>` at T=Int, the var-typed field at `String` i32_pair width, a fully concrete parameterized return on a generic fn, nested-ctor and `String`-read-back variants, plus a trailing-wildcard control), and the module-call door (#1073) routes `boxlib::mk()` — and the imported-generic #1072 x #1073 compound — through the shared resolver into the same recovery; mutation-validated per arm (reverting the #1060 instantiation-awareness flips exactly the #1060 bug-manifesting shapes RED with declared-`Unit` #1043 tests green; reverting the #1065 declared-return threading flips exactly the three direct-call value shapes RED; neutralizing the #1072 generic arm flips exactly the five generic value shapes + the imported-generic compound RED; neutralizing the #1073 module arm flips exactly the two module tests RED) |
| `test_codegen_erased_alias_typeargs_1070.py` | 15 | 398 | Non-literal erases-to-Unit type ARGUMENTS (#1070): `Box<U>` (`type U = Unit;`), `Box<Future<Unit>>`, `Box<FU>`, and alias chains — the #1060 width recomputation's zero-size test was the literal name `Unit`, so these spellings got 4 bytes and every later field read a shifted offset (silent 22→0, nested 314→0); the same literal-test disease made structural `Eq` over the same spellings fall back to the scalar POINTER compare (pre-existing — equal structs compared unequal, silently) and `show`/`hash` loud-skip. Pins every spelling end-to-end: wildcard reads (trailing `Int`, nested ctor), `Eq` equal/distinct + `Future<Unit>` arg, `show` renders `unit` + the real fields, `hash` payload-sensitive + deterministic, literal-`Unit` controls; the rider — a zero-size `@Unit` BINDING after an unrecoverable wildcard is not a read (compiles), while a genuine read beyond it still LOUD-skips (E602); mutation-validated per site (width fn, field-name canonicalisation, both dispatch gates, derivability gate, rider — each flips exactly its own test subset) |
| `test_codegen_alias_typeargs_eq_1076.py` | 34 | 499 | The Eq-dispatch ground-spelling cluster (#1076/#1077/#1078). #1076: structural `==` over NON-Unit alias type args (`Box<MyInt>`/`MyStr`/`MyBool`/`Future<Int>`/chains) silently pointer-compared (equal structs → 0, check-green) — equal AND distinct pairs per spelling, i64-width pins with >2^32 payloads whose low 32 bits collide, `MyStr` content-vs-pointer compare, plus the #1060-walk width shapes (`Bool` follows the type-param field, so an i32-sized `MyInt`/`MyStr`/`Future<Int>` manifests); a genuine free `T` (dead base-generic clone, #912) still compiles via its scalar fallback. #1077: `show`/`hash` of `Tuple<U, Int>` (raw-args Tuple plan branch) and of bare aliased-Unit values (literal-name top-level arms) loud-skipped — all four now compute (exact renders, payload-sensitive hash), literal controls pinned. #1078: element-wise `==` on arrays of parameterized ADTs (`Array<Box<Int>>`, literal included) pointer-compared (the `IndexExpr` operand's element head drops its type args) — equal/distinct/`>2^32`/aliased-element shapes, non-generic-array + direct-compare controls; mutation-validated per site (canonicalization helper, width fn, both dispatch gates, derivability gate, Tuple plan branch, top-level Unit arms, IndexExpr recovery arm — each flips exactly its own subset) |
| `test_codegen_alias_of_adt_eq_show_1085.py` | 49 | 1,140 | The alias-of-ADT / forall-Eq / bare-Future dispatch cluster (#1085/#1086/#1087 + the PR #1090 review round: #1091/#1092), siblings of #1076/#1077 at entry points the ground-spelling pass never reached. #1085: structural `==` over an alias of a WHOLE ADT (`type MyBox = Box<Int>;`, `@MyBox.0 == @MyBox.1`) silently pointer-compared (equal structs → 0, check-green) — the operand reaches the dispatch as the bare alias name, absent from `_adt_type_names`; equal AND distinct pairs, i64-width `>2^32` low-bits-collide pins, `String`-content, non-generic-ADT and alias-chain shapes, direct-compare control, plus the refinement-over-whole-ADT `==` (`type NB = { @Box<Int> \| true };` — the same silent pointer compare, equal + distinct pins). #1086: a `forall<T where Eq<T>>` instantiated at an Eq alias (`@Box<MyInt>`) wrong-loud E613'd (the top-level constraint gate misses alias / `Future` spellings) — equal / distinct / i64 pins for `MyInt` and `Future<Int>`, an alias-of-whole-ADT positive, plus a non-Eq alias (`Array<Int>`) differential (still E613, never the codegen E699 — gate↔codegen lockstep, #732). #1087: `show` / `hash` of a bare or aliased `Future` value loud-skipped (E602) — the inferred type reaches the top-level dispatch un-peeled; aliased + bare `Future<Int>` / `Future<Bool>` renders, payload-sensitive i64 hash, plain-Int + aliased-primitive + refinement controls. #1091 + composite-Future (PR #1090 review): the composite path's `_parameterized_arg_type` recovery UNDID the grounding — bare/aliased `Future<Option<Int>>` show+hash, alias-of-whole-ADT show/hash (`type MyBox = Box;`, `type MB = Box<Int>;`), `@Array<FI>` slot + array-literal element grounding, with Tuple-component and ctor-argument GREEN pins (grounded at plan consumption, #1076/#1077). #1092: an in-range int literal coerced into a `@Byte`-instantiated generic ctor field was stored i64 while every reader sizes i32 — `MkB(0) == MkB(255)` silently equal, extraction read 0 for a stored 255; distinct + equal + extraction + aliased-forall-Eq shapes through the full checked pipeline (`_run_checked` threads the checker's target-type table exactly as the CLI does), passthrough + `Int`-instantiation controls; mutation-validated per site (operand grounding, gate fallback, show + hash grounding, recovery grounding, Array-arm element grounding, Byte width coercion — each flips exactly its own subset) |
| `test_composite_postcondition_eq_912.py` | 16 | 492 | Composite (`Box`/`Option`/nested-ADT) `==` in an `ensures` postcondition lowers its runtime check to STRUCTURAL equality, not a pointer compare (#912): true `@T.result == ctor` postconditions run without a spurious `Postcondition violation` trap in both operand orders, the `E500`+runtime-trap negative controls prove a false composite postcondition is still rejected by `vera verify` AND traps, and a Tier-1 verify pin; a function generic over the parameterized ADT itself (`fn id2(@Box<T> -> @Box<T>)`) with a slot-vs-slot postcondition compiles + runs — the free-type-var scalar fallback affects only the DEAD base generic clone, while the reachable monomorphized clone lowers the `==` structurally (pinned by a `rebox` test where a FRESHLY-constructed, structurally-equal, DIFFERENT-pointer result is Tier-1-verified AND runs without trapping, plus a WAT assertion that the reachable mono clone's postcondition uses `call $eq_` not `i32.eq`); a genuinely non-`Eq` contract composite (`Box<Array<Int>>`, `Tuple`) is a clean `E613` not an uncaught crash — mutation-validated (neuter the `ResultRef` arm → left-`@T.result` run tests AND the `rebox`/structural-WAT pins flip RED; neuter the free-type-var routing → the `Box<T>` run tests flip RED via the dead-base-clone `E613`; remove the postcondition backstop → the clean-`E613` tests raise an uncaught exception) |
| `test_contract_predicate_degradation_922.py` | 9 | 250 | A non-`Eq` composite `==` / unsupported `hash`/`show` in a CONTRACT-PREDICATE position degrades to a clean diagnostic, never an uncaught Python traceback (#922): a `Tuple == Tuple` in a `requires` or a `{ @T \| P }` refinement guard is a clean `E613`, a `hash(recursiveADT)` in a `requires`/`ensures` is a clean `E602` (the #912 postcondition backstop caught only `AdtEqNotDerivableError`, not `CodegenSkip`); regression pins that valid contracts (primitive `==`, derivable-ADT `==`, refinements over primitives, primitive postconditions) still compile + run, plus a cross-check that the #912 concrete-`Tuple` postcondition still degrades to `E613` — mutation-validated (neuter each new catch → its repro re-crashes with an uncaught traceback) |
| `test_codegen_arrays.py` | 242 | 4,467 | Byte type, array literals / bounds checking / length / range / concat, direct indexing of builtin call results (#1048, #1051, alias-canonicalized #1055), `array_flatten` of inline nested literals + type-variable builtins nested as call arguments + alias-spelled / user-fn call-emission arguments incl. the Map/Set host-import tag inference (#1052, #1053, #1063), nested-alias element classification (#1067), generic-alias container returns (#1068), bare-alias returns + Block args (#1071), `Future<alias>` element sizing (#1074), map/mapi/fold closure-return `Future<T>` sizing incl. the fold SlotRef-init fallback (#1079), the post-#1041 `Future<Bool>` map stride-desync regression (#1081), collection-alias `Array<Future<Alias>>` payload canonicalization (#1082), construction builtins (#209), compound element types (#132), array utilities (#419 split) |
| `test_array_map_slot_closure_1056.py` | 10 | 227 | #1056 — a fn-typed slot (`@Mapper.0` where `type Mapper = fn(A -> B)`) as the closure argument to `array_map` / `array_mapi` / the `array_fold` accumulator: let-bound and parameter slots, type-changing `Int -> String` mappers (map and mapi), chained two-slot maps, order-pinned mapi and fold (non-commutative, non-literal initializer), an `apply_fn`-parity pin, and the inline-`AnonFn` control |
| `test_codegen_refinements.py` | 72 | 1,208 | Assert/assume, forall/exists quantifiers (incl. WAT inspection), refinement type aliases, **refinement-predicate runtime guards** (#746 — primitive- and `@Array`-base boundary guards, `@Byte`-base i32-width guards incl. `@Byte`-returning fn-call operands + `0..255` range conjoin (#766), tuple-component decomposition at the FFI boundary, generic tuple aliases, infinite-alias E617 fail-closed, refinement-over-tuple unwrapping, zero-size base guard-skip for `@Unit` **and** `@Future<Unit>` (#943)), head-over-refinement shape (#655) (#419 split) |
| `test_codegen_strings.py` | 113 | 1,266 | String literals + IO host bindings, WAT string escaping (unit + end-to-end), String/Array signatures, format expressions, core string ops (length/concat/slice/char codes/repeat), char classification, string utilities (#419 split) |
| `test_codegen_string_builtins.py` | 153 | 1,341 | parse\_nat/float/int/bool (Result-returning), base64, URL encode/decode/parse/join, search/transform builtins (#198), universal to-string (#106) (#419 split) |
| `test_codegen_numeric.py` | 86 | 1,104 | Math builtins (#199), numeric type conversions (#208), Float64 predicates + constants (#212), int64-min / float-carry to-string regressions (#475) (#419 split) |
| `test_codegen_io.py` | 42 | 821 | IO operations (#135: read\_line, read\_file, write\_file, args, exit, get\_env, sleep, time, stderr), Markdown + Regex host bindings (#419 split) |
| `test_codegen_collections.py` | 69 | 1,131 | Map + Set collections (#62), wrapper-handle bit-31 tagging (#578) (#419 split) |
| `test_codegen_json.py` | 59 | 984 | Json collection, typed accessors (#419 split) |
| `test_codegen_decimal.py` | 57 | 779 | Decimal collection, Decimal monomorphization (#419 split) |
| `test_codegen_host_effects.py` | 58 | 964 | Html/Http/Inference host effects, provider dispatch, postcondition host-import propagation (#823) (#419 split) |
| `test_codegen_nat_guards.py` | 54 | 1,325 | **`@Nat` runtime guards**: subtraction underflow (#520) and binding-site narrowing (#552 let site; #747 tuple-destructure / match-bind / ADT sub-pattern / ctor-field / call-arg sites; #758 per-leaf function-return guards incl. type-alias returns and TCO preservation on mixed-arm tails — `i64.lt_s; unreachable` net, `@Int` targets exempt) (#419 split); #758 `@Int -> @Nat` return-position guard; #983 review adds alias-aware return gates (`type Count = Nat` narrow, `type MyInt = Int` widen), the alias-to-refinement single-guard exclusion, and the per-narrowing-leaf emission that keeps a non-narrowing `@Nat -> @Nat` recursive tail call's `return_call` (TCO) intact |
| `test_codegen_translator_fixes.py` | 27 | 528 | WASM call-translator regression fixes (#475): string/array slice clamps, char-code bounds, URL/base64/parse edge cases, map-array-value rejection (#419 split) |
| `test_codegen_gc_alloc.py` | 39 | 892 | Layout helpers, bump allocator, GC core (#515), shadow-stack overflow, multi-page grow (#487), worklist overflow (#348) (#419 split) |
| `test_codegen_gc_rooting.py` | 38 | 1,560 | Opaque-handle param rooting (#347, #490), host-walker GC rooting (#692), Map host-store reachability (#695), ADT-builder rooting (#743) (#419 split); plus the #841 Future-handle battery (`TestFutureHandleGCRooting841`) — eager-GC survival across an intervening alloc, the operand-stack window (`both(async(A), async(B))` with get/post-distinguished Err text), Phase-2c reclamation of fire-and-forget futures via `host_store_sizes["future"]`, and repeated-await memoization; host-import pair-let rooting (`TestHostImportPairLetRooting846`) — `IO.args` / `IO.read_line` pairs surviving an intervening alloc under eager GC, with `IO.read_file` / `IO.get_env` ADT-path confirmation; and the `_ShadowGuard.push` slot-complete bound (`TestShadowGuardPushBound791`) — partial-headroom / full-window / negative-`sp` rejection and the exact-final-slot accept boundary, constructed directly on a hand-rolled module |
| `test_codegen_gc_reclamation.py` | 21 | 706 | Transient Map/Set/Decimal reclamation (#573; scale trio marked `stress`, #738), bucket occupancy (#706), SameValueZero keys (#743) (#419 split) |
| `test_codegen_contracts.py` | 33 | 601 | Runtime pre/postconditions, contract fail messages, old/new state postconditions, the #958 tier-agnostic always-emit pin |
| `test_codegen_decreases_guard.py` | 24 | 859 | The #1172 runtime termination guard: non-terminating measures trap through the contract channel instead of hanging (the issue's ADT repro, constant/growing/negative-floor scalars, a lexicographic violation, mutual `where` recursion), terminating programs run clean with the guard emitted (Tier-1 countdown, the corrected spec Ackermann, sequential siblings pinning the exit restore, a concrete ADT measure), the tier3-obligation ⇒ emitted-guard differential, E127 rejection of non-well-founded measures (Float64/String/Bool and a lex component) plus acceptance of the well-founded family, and the parameterized-ADT-measure no-guard pin (#1177) |
| `test_codegen_monomorphize.py` | 224 | 4,893 | Generic instantiation, type inference, monomorphization edge cases, ability constraint satisfaction (Eq/Ord/Hash/Show), operation rewriting (eq/compare), show/hash dispatch (incl. structural show/hash for composites, same-base finite nesting, and `_split_param_type` — #911; recursive-ADT show/hash via a generated self-calling helper, deep-list termination + GC-frame `$gc_sp` restore, non-generic mutual recursion — #924), ADT auto-derivation, array operations (slice/map/filter/fold), nested `where`-helper emission on the non-generic path (#978/#989 — a grandchild helper using `eq`/`compare` in its body or contracts must have its ability op rewritten so its body is emitted, and a node with two nested helpers emits both) |
| `test_codegen_nested_nullary_ctor_994.py` | 7 | 229 | **#994 F2 nested payload-less constructor in a `forall<T>` `==`/`!=`** — the #979/#981 checker adoption newly accepts `ensures(Some(None) == @Option<Option<T>>.result)` under `forall<T>`; `check`+`verify` passed but `compile` raised a spurious E613 because the structural-Eq derivation erased the type argument (the inner `None` renders bare `Option`, so `Some(None)` recovers as `Option<Option>`; the dead base clone's slot renders `Option<Option<T>>` with a nested free `T` the top-level-only free-var check missed). The fix recovers the fully-concrete name from whichever operand carries it (both share a type by E142) and routes to the scalar dead-code lowering only when NEITHER resolves. Pins: both operand orders + `!=` + a body-position `==` compile + RUN to their sentinels (55/77), with concrete and payload-carrying controls that must keep compiling — mutation-validated (remove the sibling recovery → the reachable clone TRAPS on a scalar pointer compare; remove the concreteness gate → the base clone flips back to E613) |
| `test_codegen_closures.py` | 63 | 2,024 | Closure lifting, captured variables, higher-order functions, iterative-builder shadow-stack regressions (#570), closure return-value shadow-push balance for both i32-pair and i32-ADT branches across array_map and array_mapi, plus VERA_EAGER_GC injection self-test (#593), IndexExpr-of-FnCall element-type inference (#614), non-contiguous capture and walker-order miscompiles (#615), `Future<T>` free-variable capture width (#1044) |
| `test_codegen_invariant_e699.py` | 4 | 216 | `CodegenInvariantError` raised in a translator surfaces as a structured `[E699]` "internal compiler error" at the `_compile_fn` boundary, not a raw traceback (#657 Track 2), across all four contract-lowering paths — body, closure, precondition, and postcondition (#939 completes the precondition + postcondition nets) |
| `test_codegen_modules.py` | 186 | 3,902 | Cross-module guard rail, cross-module codegen, module-qualified call resolution bypassing a local shadow incl. intra-module siblings, where-fn helpers both directions, unit- and pair-returning calls in statement position, and the @Nat-parameter guard mirrored onto shadowed targets (#814 §8.5.3), name collision detection (E608/E609/E610), fused-async `await` of a cross-module future (#841/#842) and of an indirectly-called closure (#843 — `await(apply_fn(closure, …))` classified by declared return type incl. generic-alias type-arg substitution; unresolvable shapes fail loud via E616 or the #867 WASM-validation trap), transitive module imports (#890 — a `main -> mid -> base` chain and a `main -> {left, right} -> base` diamond compile and run via the real on-disk resolver, while a transitive symbol stays invisible to the top-level importer per §8.6.4), a non-void `ModuleCall` used *directly* as a constructor argument or array-literal element (#905 — its return type is resolved at the field/element site via the shared `_resolve_module_call_wasm_name`, closing a check-green→codegen-crash gap; the non-void sibling of #902's Unit-field fix), a user-defined function named `show`/`hash` used in a constructor field or array element (#908 — the ability-op width special-case must defer to the user fn's declared return width when the name resolves to a user fn, matching codegen's `not in known_fns` dispatch gate; a genuine unshadowed ability op still uses the special-case width), and an imported function's nested `where`-helper at any depth (#989 — the registration walk must reach grandchildren via `_flatten_where_fns`, so an imported `libfn -> child -> grandchild` chain that checks + verifies green also emits every helper and no call dangles) |
| `test_codegen_coverage.py` | 5 | 244 | Defensive error paths: E600, E601, E605, E606, unknown module calls  |
| `test_execute_characterization.py` | 24 | 510 | Characterization harness pinning `execute()`'s observable contract ahead of the #421 runtime decomposition (#734): every `ExecuteResult` field (`value` int/float/str — including a transparent `Future<String>` return decoded for display (#1047) — heap-pointer/None, `stdout`, `state`, `exit_code`, `stderr`) crossed with the three completion modes — normal return, WASM trap (raises `WasmTrapError` with a classified `kind`, output-before-trap preserved), and interrupt/exit (`IO.exit(n)` → `exit_code` n with `value` None, Ctrl-C → 130) — plus the positional-constructor compatibility shape and `capture_stderr` True-vs-default. **Mutation-validated**: every cell confirmed to flip RED when its target return path in `api.py` is deliberately broken (9 mutations, 0 green-for-the-wrong-reason tests) |
| `test_walker_defensive_branches_597.py` | 21 | 296 | Synthetic-AST tests for the 11 defensive `isinstance` branches added by #597 (`_scan_io_ops` / `_scan_expr_for_handlers` / `_infer_expr_wasm_type` / `_infer_vera_type`) plus the 5 pr-review fixes (#2/#3/#8 — ModuleCall/AnonFn/QualifiedCall return None; dead `is not None` guards on Block/HandleExpr removed) |
| `test_check_walker_coverage_597.py` | 15 | 311 | Unit tests for `scripts/check_walker_coverage.py` parsing logic — Expr subclass extraction, isinstance flattening (incl. tuple form), checklist-block anchoring (incl. CR-3 regression test: `# Foo → bar` outside WALKER_COVERAGE block not counted), section-header tolerance, auto-discovery invariants, end-to-end main exit code |
| `test_diagnostic_fields.py` | 90 | 1438 | Unit tests for `scripts/check_diagnostic_fields.py` (#682) — required-field detection, the warning severity rule (no `fix`), spec_ref validity, the codegen structural-exemption registry, the `# diag-fields-exempt` per-call opt-out, the error_code-registration check (#828), a live-tree integration check that all of `vera/` is fully tagged, and the narrowed plumbing-skip (#827: the skip now requires a genuine `self`-receiver helper *method* — a direct class member, not a `@staticmethod`, module-level or nested look-alike — whose **sole own-scope** `Diagnostic` it is, where own-scope means the body and excludes decorators / parameter defaults / annotations; a stray second ctor, or one in a nested `def`, is inspected by all three passes: field presence, `spec_ref` validity, `error_code` registration; each guard and each pass's use of the skip is mutation-pinned separately; #956: the skip also requires that sole ctor be reachable as the helper's result — return-ed, appended, or bound to a local later return-ed/appended — not merely constructed and handed to something else, a name rebound by any binding form — counted generically: every Store-context name (assignment/unpack of any shape, `for`/`with` targets, walrus), `import ... as`, `except ... as`, `match` captures, parameters, and `nonlocal` declarations in nested functions; a bare annotation is not a rebind, and the return/append name-match is order-sensitive — after that binding is treated as unreliable rather than reachable, and only a `self.<attr>.append(...)` call counts as a diagnostic sink, not an append to an unrelated throwaway local; #955: the `# diag-fields-exempt` opt-out is honoured for an *unresolvable* non-literal severity/spec_ref — marker found anywhere across the call's span — but never for a spec_ref/error_code that resolves yet is factually wrong, and the error_code pass skips non-literal codes entirely) |
| `test_stress.py` | 16 | 553 | Scale-dependent regression tests (#596) — `@pytest.mark.stress`, skipped by default.  9 logical tests × eager-GC lane parametrisation = 16 test instances.  10K `array_map`, 5K nested-array `array_map`, 1K-deep tail recursion with allocating arg, 1M-deep tail recursion with allocating arg (#549 GC-aware TCO), 20×20 nested array-fold-of-array-fold, 100K `array_fold`, 10K String allocations, 1K `State<Int>` get/put cycles, 10K `IO.print` calls.  Pins #570 / #515 / #593 / #549 / #487 / #348 / #573 regression coverage |
| `test_string_length_soundness.py` | 15 | 278 | #802 — string_length code-point vs UTF-8 byte soundness: a non-literal `string_length` defers to Tier 3 (the issue's `"é"` probe no longer proves `== 1` at Tier 1), a string-literal length is modeled at its exact UTF-8 byte count (`== 2` for `"é"`), and the boolean predicates `string_contains` / `string_starts_with` / `string_ends_with` stay Tier 1 (sound under UTF-8 self-synchronization), while a predicate over an astral (> U+2FFFF) or lone-surrogate literal defers to Tier 3 (z3.StringVal cannot model those code points) |
| `test_errors.py` | 62 | 657 | Error code registry, diagnostic formatting, serialisation, SourceLocation, and error display sync — the canonical `E001` diagnostic must match each of its mirrors: `README.md`, `docs/index.html`, `spec/00-introduction.md`, `AGENTS.md`'s example `--json` block, and the hardcoded example in `scripts/build_site.py` that generates `docs/index.md` (#829; `AGENTS.md`'s ellipsis-truncated description/rationale are prefix-compared, its `error_code`/`spec_ref`/`fix` exactly) |
| `test_eq_contract_874.py` | 13 | 430 | `eq`/`compare` ability ops in contract position: codegen canonicalization + verifier Tier-1 discharge/counterexample, where-fn contracts, compare Ordering-sort materialization, shadowing guard (#874) |
| `test_formatter.py` | 474 | 3,638 | Comment extraction, interior comment positioning, expression/declaration formatting, match arm block bodies, §1.8 rule 2 in value position (a `let`-bound `match`/`if` expands exactly as one in statement position, and a comment above an arm inside a statement's value stays on that arm), blank-line preservation (§1.8 rule 13 — gaps between statements, before a block result and around a comment, collapsed to one and never invented), idempotency, parenthesization, spec rules, ability declarations |
| `test_cli.py` | 266 | 4,287 | CLI commands (check, verify, compile, run, serve, test, fmt, version, quiet), subprocess integration, JSON error paths (including the `verify --json` `obligations` array and its summary-reproducibility pin, #967), runtime traps, arg validation, multi-file resolution, IO exit codes, --explain-slots, `builtins`/`effects`/`errors` introspection dispatch, and a USAGE-completeness guard (every dispatched `cmd_<name>` handler has a help row) |
| `test_introspect.py` | 39 | 221 | `vera builtins/effects/errors --json` registry introspection (#539): the `{schema, items}` envelope, count-equals-registry differential per registry, error-phase derivation, effect/ability `kind` tagging, the parameterised `Exn<E>` effect, and best-effort `since` attribution with full-coverage guards |
| `test_resolver.py` | 20 | 602 | Module resolution, path lookup, parse caching, circular import detection, the E011/E012/E013 diagnostic contract, internal-error isolation (a compiler bug is not masked as E013), and the transitive-closure return of `resolve_imports` (#890 — a diamond yields each reachable module once, direct imports tagged `direct`, the transitive one not) |
| `test_types.py` | 82 | 443 | Type operations: subtyping, effect subtyping, equality, substitution, pretty-printing (including leaked-placeholder rendering to `?`, #1069), canonical names |
| `test_wasm.py` | 29 | 502 | WASM internals: StringPool, WasmSlotEnv, translation edge cases via full pipeline; plus the fused-await payload-alias canonicalizer cycle-guard pins (`TestCanonicalizeTypeExprAliases`) |
| `test_verifier_coverage.py` | 92 | 1,651 | Verifier/SMT coverage gaps: SMT encoding paths, verifier edge cases, defensive branches, **#667 SMT translator coverage for `FloatLit` / `IndexExpr` / `ArrayLit`** (Tier 1 verification of float/array literal/index contract predicates) |
| `test_verifier_sort_name_collision_884.py` | 5 | 203 | **#884 Z3 sort-name collision** — regression pins that lossy type-name mangling can no longer collide two distinct ADT/tuple sorts onto one Z3 datatype (`_get_or_create_adt_sort` / `_get_or_create_tuple_sort` routed through the injective `mangle_type_name`), plus the Array-element reverse-lookup fix (`_get_element_sort_for_array`) |
| `test_verifier_nested_ctor_sort_918.py` | 14 | 441 | **#918 same-ADT self-nested constructor sort selection** — a `Some(Some(x))` body (or nested same-ADT ctor literal in a contract) once resolved the outer ctor to whichever `Option<...>` instantiation was cached (base-name-wins), feeding `sort.constructor(idx)` a wrongly-sorted `DatatypeRef` and crashing Z3 with an uncaught traceback on a `vera check`-green program; the fix translates the ctor call's arguments, recovers each argument's Vera type from its Z3 sort, and unifies against the ctor's declared field types to pin the owning ADT's FULL instantiation. Pins: nested-body + nested-contract verify without crash, a TRUE nested postcondition PROVED at Tier 1 (not blanket-demoted), a FALSE one still disproved (E500 soundness), the #887-trap single-level call-arg staying opaque/clean (on-demand materialisation gate), a different-ADT nesting staying clean, and no Z3-internal exception text leaking as a diagnostic |
| `test_verifier_nullary_ctor_sort_994.py` | 11 | 228 | **#994 F1 bare nullary-constructor sort selection in `==`/`!=`** — the #979/#981 checker adoption newly accepts `Some(None) : Option<Option<Int>>` compared against `None`/`Some(None)` in a contract; a bare `None` carries no payload, so the base-name scan picked the wrong live `Option<...>` sort and `_datatype_value_eq`'s `left == right` raised an uncaught Z3 `sort mismatch` on a `vera check`-green program. The fix hints the nullary-ctor sort from the checker's recorded (instance-substituted) semantic type via the gated #918 pinning, and degrades a residual sort mismatch to Tier-3 rather than crash. Pins: true `!= None` / `== Some(None)` PROVE at Tier 1 (both operand orders, concrete + forall), false `== None` disproved (E500) against a match-based oracle, `verify --json` always emits JSON, and a direct `_datatype_value_eq` degradation backstop — mutation-validated (disable the hint → the false-disproof tests flip RED; disable the guard → the direct mismatch backstop raises) |
| `test_verifier_where_helper_scope_991.py` | 5 | 235 | **#991 lexically-scoped where-helper resolution** — the flat, last-wins `env.functions` lookup assumed the WRONG same-named helper's `ensures` at a call site, a false E500 in a diamond of two siblings each carrying a nested `leaf` with a different postcondition. The scoped lookup resolves a bare helper call to the nearest same-named helper in the enclosing `where`-tree (own children, then ancestors), then the top-level function, then the flat registry. Pins: the diamond verifies (each parent proves against its OWN leaf), the wrong-helper counterexample does not arise, and a genuine postcondition violation against a helper's own body is still caught — mutation-validated (revert the scoped lookup → the diamond flips RED). Plus the clone-scope shape: `_verify_generic_instances` threads the `enclosing` ancestor chain into each clone's verification, so a nested generic helper's unshadowed ancestor-helper call cannot be captured by a same-named decoy helper under another function (false E500) — verified AND run (verifier↔codegen agreement) with a non-trivial decoy postcondition, per-function Tier-1 ensures-obligation checks (present and `verified`, never skipped), and both doors executed (host and decoy run values) |
| `test_wasm_coverage.py` | 226 | 3,971 | WASM coverage gaps: helpers unit tests, inference branches, closure free-var walking, operator/data/context edge cases |
| `test_tester.py` | 17 | 445 | Contract-driven testing: tier classification, input generation, test execution, skip message content |
| `test_tester_artifacts.py` | 1 | 89 | `vera test` compiles through the same artifact tables as the other CLI doors: the tester-compiled WAT for a tuple-component widening carries the widen guard (without the shared artifact tables, `cmd_test` emits no guard while the verifier claims Tier-3 runtime-guarded — a verifier↔codegen divergence) |
| `test_tester_coverage.py` | 35 | 942 | Tester coverage gaps: String/Float64/ADT parameter input generation, Bool/Byte parameters, unsatisfiable preconditions, type expression edge cases, FP model-value extraction (NaN/Inf/signed-zero, #797) |
| `test_markdown.py` | 59 | 393 | Markdown parser: block/inline parsing, rendering, round-trips, edge cases |
| `test_lsp.py` | 94 | 1211 | LSP transport + coordinate layer (#222 Phase C) and language features (#222 Phase D): parametrized code-point↔UTF-16 goldens incl. astral-plane fixtures and surrogate-pair snapping, Span (1-based, exclusive-end) and SourceLocation (0-based col) → LSP Range conversions, point→token-range widening, DocumentStore open/change/close + index invalidation, an in-process handler-drive test, and one stdio end-to-end round-trip against the real `vera lsp` subprocess (initialize → didOpen → shutdown → exit) pinning serverInfo + textDocumentSync capabilities; plus the Phase D feature suite — parse-error single-diagnostic path, type-error verification short-circuit, tier=3 in E520 diagnostic data, per-function tier Hint synthesis (and its suppression for functions with violated obligations), smallest-enclosing-span hover, De Bruijn slot goto (most-recent-parameter jump, out-of-range None, off-slot None), and typed-hole completion (inside/after hole, away-from-hole None); plus the Phase E speculativeEdit suite — identical-text all-unchanged, breaking edit surfaces newly_undischarged (violated nat_sub) with canonical state untouched, strengthening edit surfaces newly_discharged, parse/type errors report ok:false, deleted functions report removed, proof_delta purity; plus the Phase F1 proposeEdit suite — the apply gate (clean and strengthening edits apply, breaking and non-compiling edits refuse), force overriding both gates with the delta still reported, wiring against a structural fake server (apply round-trip with exact full-document replacement range, refuse touches no canonical state, unopened-URI clamp sentinel), and full-document-range goldens (trailing-newline virtual line, UTF-16 end column); plus the Phase F2 strengthenContract suite — splice goldens (first-clause-only replacement with byte-identical remainder, ensures variant, unknown-fn None), the call-site audit pin (tightened precondition refused with newly_undischarged call_pre items, canonical state untouched), provable-ensures strengthening applies, and the three splice-target refusal paths (no analysis, unparseable document, unknown function); plus the Phase F3 addEffect suite — transitive-caller closure goldens (diamond in declaration order, leaf, unknown-fn None, recursion appears once), effect-row rewrite goldens (pure to singleton set, source-preserving append, already-present None, base-name identity blocking State<Int> next to State<Bool>), diamond propagation applying one multi-site candidate with the bystander untouched, mixed append/replace rows with already-satisfied callers skipped, the fully-satisfied no-op shape, and the two refusal paths; plus the #728 instruction-contract suite — the LSP message carries description, rationale, and the Fix: paragraph (also pinning single E501 emission at the LSP surface), and a bare diagnostic maps to the description alone |
| `test_browser.py` | 138 | 3,068 | Browser parity: Python/wasmtime vs Node.js/JS-runtime output equivalence across IO, State, contracts, Markdown, Regex, and all compilable examples |
| `test_conformance.py` | 895 | 125 | Parametrized conformance suite: parse, check, verify, run, format idempotency across 179 programs |
| `test_prelude.py` | 27 | 526 | Prelude injection: Option/Result/array operation detection, combinator shadowing, type aliases, the reserved-name twins the combinators resolve through (#1184), end-to-end compilation |
| `test_checker_apply_fn.py` | 18 | 455 | #854 — `apply_fn` as a checker special form: zero-warning pins (API + CLI `--json` + closures.vera), E201 arity / E202 type / non-function-first-arg errors, E122/E125 effect-row enforcement for applied fn values, E151 redefinition rejection, variadic two-param application, prelude combinator regression pins |
| `test_prelude_diagnostics.py` | 8 | 271 | #851 — prelude combinator skip-warnings: unreferenced-prelude E602/E604 suppression (zero-warning minimal compile, API + CLI `--json`), `<prelude>` origin attribution for referenced-but-skipped combinators (text + `to_dict`), transitive reference scan, and user-fn warning locations pinned unchanged |
| `test_readme.py` | 2 | 79 | README code sample parsing |
| `test_html.py` | 4 | 167 | HTML landing page code samples: parse, check, verify (vera:skip-annotation aware, #538) |
| `test_float64_fp.py` | 10 | 260 | #797 — `@Float64` contracts via Z3's IEEE-754 FloatingPoint sort: unsound relational / reflexive contracts (rounding at 2^53, `NaN`, `Inf`) flip from proved to violated/Tier-3, NaN-guarded contracts still verify at Tier 1, `==`/`!=` use IEEE `fpEQ`/`fpNEQ` (incl. `+0.0 == -0.0`), `%` matches codegen truncated remainder (not `fp.rem`; NaN-by-zero + large-magnitude edges), and `float_is_nan` / `float_is_infinite` / `nan()` / `infinity()` translate to FP predicates / constants. Also guards mixed `@Float64`/`@Int` ordering as a clean E142 (not a Z3 crash) |
| `test_float64_builtins_807.py` | 81 | 491 | #807 — Tier-1 modeling of the modelable `@Float64` builtins. `float_clamp` modeled unconditionally as faithful WASM `f64.min(f64.max(v,lo),hi)` (the NaN-propagation soundness guard distinguishes it from a naive `z3.fpMin`/`fpMax`); `int_to_float` / `float_to_int` concrete-gated (symbolic args defer to Tier 3 — Z3's symbolic FP↔Real reasoning returns spurious counterexamples); `float_to_int` domain obligation (E529) for concrete NaN/Inf/out-of-range args. Verify-vs-run differentials confirm each model agrees with wasmtime bit-for-bit (±0, ±inf, NaN, ties, lo>hi, the 2^53 rounding boundary, i64 max, and the trap cases) |
| `test_build_site.py` | 46 | 698 | Site-asset tooling — `_abs_links` rewriting (relative links, fenced-block immunity incl. inline backticks and tilde fences, http/https/fragment pass-through, Vera effect syntax not mis-parsed), `build_site` `<lastmod>` stability (preserve/refresh keyed on URL-structure change), `check_site_assets` sitemap staleness (missing / date-only-clean / structural-stale), and the #538 leak guard (vera:skip fence annotations stripped from generated `docs/SKILL.md` / `docs/llms-full.txt`, with a non-vacuous precondition that the source carries annotations); plus the #1154 `check_fact_coherence()` suite — index.html↔index.md fact extraction and divergence detection |
| `test_builtin_typevar_collision_970.py` | 61 | 811 | #970 a user `forall` type-var name colliding with a built-in generic's internal name (`T`/`E`/`A`/`B`/`K`/`U`/`V`): focused check/verify pins for the compound-argument shapes (`@Array<Option<T>>`, `@Result<Int, Option<E>>`, `@Map<K, Option<V>>`) plus a collide-vs-control differential battery over every generic-builtin family and contract/where-helper position.  Also pins marker-strip (the `#b` namespacing marker must never reach an E205/E202 diagnostic), a registry-consistency pin (every built-in ability-constraint `type_var` stays a member of its `forall_vars`), the dual completeness-gap pinned in both argument orders, a tier-split equality pin, and the #1069 leaked-placeholder message-rendering sweep (a stripped built-in var renders as `?`, not a bare letter, at every reachable actual-type slot: the mismatch sites plus the operator/index/interpolation family, `assert`/`assume`, `if` condition and branches, and the contract/refinement predicates — one parametrized row per converted render slot, with the provably-unreachable sites documented in the class docstring) |
| `test_check_changelog_updated.py` | 68 | 712 | `check_changelog_updated.py` unit + end-to-end tests: file classification (incl. file-style exact-match vs directory-style prefix-match), CHANGELOG diff parsing with `[Unreleased]` section tracking, bare-heading rejection, and full-file context (regression test for bullets far below the heading), `Skip-changelog:` trailer detection, temp-repo integration covering substantive/exempt/label/trailer paths, and `GIT_*`-env hermeticity of the temp-repo fixtures (regression for the pre-commit-hook env leak) |
| `test_release.py` | 47 | 566 | Release policy and registry verification (#481): strict project-name and version parsing/comparison, version-bump/TestPyPI/recovery planning, exact confirmation and immutable-tag guards, first-parent version-introduction discovery, package-change recovery refusal, non-empty CHANGELOG extraction, one-wheel/one-sdist SHA-256 manifests, malformed registry-response handling, missing/filename/hash propagation retries, exact filename/hash verification, and CLI dispatch/GitHub-output wiring.  An autouse fixture scrubs hook-exported `GIT_*` variables so the tmp-repo git calls (fixture helpers and `release.py`'s own) never resolve to the developer's repository when the suite runs inside a pre-commit hook. |
| `test_check_doc_counts.py` | 19 | 187 | `check_doc_counts.py` planning-document checks: KNOWN_ISSUES refactoring line counts (±10% tolerance band incl. the exact-boundary case, drift detection, empty-file citation, hyphenated paths, missing file/section/rows, the #419 empty-section sentinel + its cannot-mask-a-malformed-table dual) and HISTORY version-row format (issue-link limit, ` — ` separator rejection, dateless-row and prose exemption, line-number reporting) |
| `test_check_explicit_encoding.py` | 54 | 254 | `check_explicit_encoding.py` gate (#645): flags text-mode `open()` / `read_text()` / `write_text()` **and** `subprocess.run/Popen/check_output(..., text=True)` captures missing an `encoding="utf-8"` literal (rejects non-literal / non-UTF-8 values), skips binary/bytes-mode calls, honours the `# encoding-exempt` opt-out, and asserts the shipped repo is clean |
| `test_check_limitations_sync.py` | 6 | 108 | `check_limitations_sync.py` section extraction: table-rows-only issue harvesting, prose-link exemption, bounding at the next second-level heading, `None` for absent or sub-level headings so renamed sections fail loudly; plus the #852 fail-loud rule: an UNKNOWN issue state under `--check-states` (gh missing / auth failure / timeout) is an error, never a silent pass |
| `test_doc_annotations.py` | 23 | 340 | `scripts/doc_annotations.py` — the inline `vera:skip-<stage>` fence-annotation reader and shared `run_parse_only_gate` used by the doc-block gates ([#538](https://github.com/aallan/vera/issues/538)): markdown/HTML scanning (annotation attached to the following fence / `<pre>`, stacked directives), hard problems (malformed, dangling incl. EOF, duplicate-stage, unknown-stage, unterminated fence / unclosed `<pre>`; prose mentions without comment syntax are fine), the gate round-trip semantics via `evaluate_block` (unannotated failure fails, annotated failure skips, annotated PASS is a stale annotation, skip-check still runs parse first and stops the pipeline), unsupported-stage detection for parse-only gates, and `strip_annotations` (annotation lines removed, other HTML comments survive) |
| `test_doc_builtin_shadowing.py` | 8 | 107 | `check_doc_builtin_shadowing.py` gate ([#819](https://github.com/aallan/vera/issues/819)): reject-set membership (opaque built-ins in, overridable combinators out), top-level + `where`-block `fn <builtin>` definitions flagged, non-built-in / overridable / prose-mention ignored, and the shipped docs are currently clean |
| `test_runtime_traps.py` | 75 | 2,877 | Runtime trap categorisation (#516 Stage 1), out-of-bounds host-read bounds check (#1145), stdout/stderr-on-trap preservation (#522), `IO.print` live tee (#543), and trap source backtrace (#516 Stage 2): `_classify_trap` per-`kind` mapping (`divide_by_zero`/`out_of_bounds`/`stack_exhausted`/`unreachable`/`overflow`/`contract_violation`/`unknown`), `WasmTrapError` shape + `RuntimeError` substitutability, end-to-end `cmd_run` text + JSON envelopes including `trap_kind`, captured `stdout`, captured `stderr`, JSON-mode "no stderr leak" invariant, cross-stream code-order regression using merged `redirect_stdout`/`redirect_stderr`, the v0.0.123 tee suite (live streaming, write-count + order preservation, JSON-mode tee suppression, trap preservation invariant under tee, per-write flush count, default-execute silence), and the v0.0.124 source-mapping suite — `_resolve_trap_frames` unit tests covering user-fn / built-in / built-in-prefix / monomorphized base-name fallback / unknown-name / no-frames-attribute / leaf-first ordering preservation; end-to-end `cmd_run` text-mode + JSON-mode backtrace including the **leaf-first** ordering invariant; contract-violation backtrace in both text and JSON modes; direct `execute()` `WasmTrapError.frames` attachment; **suppression marker** for collapsed leading runtime-helper frames (mocked `vera.codegen.execute` with synthetic `is_builtin=True` leaf frames so the collapse logic is testable deterministically); source-map population for top-level fns + lifted closures (with span-value assertion against the closure literal's exact line range); and the no-builtin-leakage regression that pins built-in helpers (`alloc` / `gc_collect` / `contract_fail`) NOT being registered in `fn_source_map`; plus the v0.0.125 Stage 3 suite (`#547`) — text-mode `Fix:` block surfacing with position-ordering invariant (Fix appears after the source backtrace), text-mode block suppression for `contract_violation` (no empty header noise), JSON-mode `fix` field always-present (schema stability) including the empty-string case, `_TRAP_FIX_PARAGRAPHS` table-completeness assertion (every kind in the taxonomy has a Fix paragraph entry), and the column-wrap invariant (~76 chars max per line, two-space indent under the `Fix:` heading); plus the UTF-8 hardening suite **`TestHostPrintInvalidUtf8589`** (`#589` / `#592`) — after `#592` centralised the `errors="replace"` invariant into the single `vera.runtime.text.safe_utf8_decode` helper — reached only through a shared `_slice_and_decode` helper (`vera/runtime/heap.py`) that the three WASM-memory string readers (`_read_wasm_string` and `_read_string_export` there, and `vera/wasm/markdown.py::_read_string`) delegate to, with the `host_print` / `host_stderr` / `host_contract_fail` host imports and the String-return extractor in `execute()` routing through those readers rather than decoding inline: one helper unit test pinning the invariant once (invalid bytes → U+FFFD, valid + empty pass through), three wire-real end-to-end tests that drive the **production** readers (`_read_wasm_string` / markdown `_read_string` behind a synthetic-WAT `probe` host import; `_read_string_export` against a real exported memory, also covering its out-of-bounds → `None` pointer-fallback) over a region seeded with invalid UTF-8 — so a strict-decode regression surfaces as a `UnicodeDecodeError` escaping wasmtime's trampoline, and the host imports / extractor are transitively covered — and one synthetic-WAT end-to-end test that imports `vera.print` and calls it with raw invalid UTF-8 bytes to pin the wasmtime-trampoline fact independently (a Python `UnicodeDecodeError` inside a host import escapes as a "python exception" cause iff the host decode is strict); the six pre-`#592` structural source-grep assertions were retired by the centralisation; plus the Ctrl-C-during-host-import suite **`TestHostSleepKeyboardInterrupt`** ([#595](https://github.com/aallan/vera/issues/595) / [#599](https://github.com/aallan/vera/issues/599)) — after the v0.0.160 relocation to a single `except KeyboardInterrupt` handler in `execute()` (enabled by `wasmtime>=45.0.0`'s `except BaseException` trampoline fix): one structural assertion that the four per-host-import `raise _VeraExit(130)` guards are gone and the centralized handler maps to `exit_code=130`, plus four end-to-end tests that compile real Vera programs calling `IO.sleep(...)`, `IO.read_char(())`, a mocked fused `await` ([#841](https://github.com/aallan/vera/issues/841) — `Future.result()` patched to interrupt), and a live in-flight fused `await` (no mocking — `_thread.interrupt_main()` fired only once the server confirms the request arrived, handler then released so the executor teardown has a real worker to wait out; post-[#848](https://github.com/aallan/vera/issues/848) the progress print precedes the `async(...)`, so program order makes its stdout assertion deterministic), raise `KeyboardInterrupt` from inside the blocking call, and assert the program exits with `ExecuteResult.exit_code == 130` (pre-interrupt stdout preserved) instead of a raw Python traceback escaping wasmtime's trampoline |
| `test_serve.py` | 8 | 189 | #305 `vera serve` driver end-to-end: GET/POST echo round-trips (method/path/headers/body cross the host↔guest boundary via `build_request_adt` / `decode_response_adt`), handler status propagation, runtime contract violation → 500 with `trap_kind` JSON, `State<Int>` isolation across requests (instance-per-request pinned), and clean `make_server` validation errors (missing / wrong-signature `handle`), and an eager-GC round-trip pinning the Request builder's shadow-rooting; all on ephemeral ports |
| `test_wasi_target.py` | 235 | 2,142 | #237 WASI Preview 2 target (spec chapter 13): component emission validated live against the real wasmtime host — parse (`Component(engine, wat)`), instantiate (`Linker.add_wasip2()` + `WasiConfig`), and execute (stdout/stderr capture, env, argv incl. a 500-arg GC-pressure stress and a >64 KiB arena-cap trap, preopen file round-trips + errno mapping, stdin incl. UTF-8 multibyte, clocks, random bounds, exit, contract-violation text on WASI stderr, overflow); the family gate (clean diagnostic naming unsupported families, never a silent fallback); the core-emission pin (default `--target wasm` WAT untouched); `cmd_compile`/`cmd_run --target wasi-p2` CLI integration (binary component artifact, `--wat` component text, JSON envelopes, trap-kind classification through the component boundary, exit-code 0/1 degradation, `--fn` rejection); the `execute_wasi_p2` host runner (env passthrough, argv, stderr capture, String-main `wasi:cli/run` fallback); the **dual-target conformance differential** (all 134 run-level conformance programs under both targets, byte-identical stdout/stderr required; nondeterministic-op and family-gated programs skip loudly); a stock-`wasmtime`-CLI smoke test (skips when the CLI is not installed); and the Stage-D **server world** (`world="server"`): incoming-handler emission pins (adapter lift, 32-slot dispatch table, @0.2.0 version pin, no `wasi:cli/run`), #305 handler validation + server family-gate diagnostics (rejected IO ops, non-String map instantiations, unsupported families), the cli-world pin (default emission carries no server machinery), Request/Response layout tripwires, and a stock-`wasmtime serve` smoke battery (host-vs-served differential over a method/path/header/body matrix incl. duplicate-header later-wins, in-guest map-op order parity, `IO.print` console routing, trap→500 with symbolized backtrace + violation text, graceful 500s for forbidden headers and out-of-range status, a 1 MiB GC-stress echo, and an eager-GC shadow-push mutation validation; skips when the CLI is not installed) |

## Conformance Suite

The conformance suite is a collection of 179 small, focused programs in `tests/conformance/` that systematically validate every language feature against the spec. Most programs are self-contained; the module-focused Chapter 8 cases use `import` statements where needed, and `ch07_cross_module_contracts.vera` still depends on `ch07_cross_module_contracts_lib.vera`. Each program tests one feature or a small group of related features.

Simon Willison [argues](https://simonwillison.net/tags/conformance-suites/) that conformance suites are a "huge unlock" for language projects — they transform development from trust-based to verification-based. The conformance suite serves as the definitive specification artifact that any implementation (or agent) can validate against.

### Three-layer testing model

Vera has three distinct test layers, each serving a different purpose:

![The three test layers — unit tests for compiler internals, spec-anchored conformance programs, end-to-end examples — and the four nested conformance levels: parse, check, verify, run.](assets/diagrams/testing-layers.svg)

| Layer | Location | Purpose | What it tests |
|-------|----------|---------|---------------|
| **Unit tests** | `tests/test_*.py` | Test compiler internals | Error paths, edge cases, internal APIs |
| **Conformance suite** | `tests/conformance/` | Spec-anchored feature validation | Every language feature, one program per feature |
| **Example programs** | `examples/` | Showcase programs and demos | End-to-end usage, documentation |

Unit tests verify that the compiler works correctly. Conformance programs verify that the *language* works correctly. Examples demonstrate how to use the language. All three run in CI and pre-commit hooks.

### Test levels

Each conformance program declares the deepest pipeline stage it must pass:

| Level | What it validates | Count |
|-------|-------------------|------:|
| `parse` | Source text is syntactically valid | 0 |
| `check` | Parses and type-checks cleanly | 32 |
| `verify` | Type-checks and all contracts verified by Z3 | 13 |
| `run` | Compiles to WASM and executes correctly | 134 |

Almost all programs are at the `run` level — they compile and execute, producing correct results. Thirty-two programs (`ch02_generic_over_unit_rejected`, `ch02_map_unit_value_rejected`, `ch03_typed_holes`, `ch04_let_unit_rejected`, `ch05_apply_fn_arity`, `ch05_decreases_float_rejected`, `ch05_reserved_fn_name_rejected`, `ch05_reserved_keyword_fn_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_cross_module_contracts_lib`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch07_bare_effect_op_rejected`, `ch08_circular_import`, `ch08_cross_module_generic_lib`, `ch08_reserved_vera_prefix_rejected`, `ch08_transitive_module_import_base`, `ch08_visibility_private`, `ch08_xmod_widen_lib`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_eq_non_derivable_rejected`, `ch09_http`, `ch09_inference`, `ch09_ord_adt_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch06_quantifier_array_domain_rejected`, `ch07_handler_state_type_mismatch_rejected`) are at the `check` level. Twenty-five of them — `ch02_generic_over_unit_rejected`, `ch02_map_unit_value_rejected`, `ch04_let_unit_rejected`, `ch05_apply_fn_arity`, `ch05_decreases_float_rejected`, `ch05_reserved_fn_name_rejected`, `ch05_reserved_keyword_fn_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch07_bare_effect_op_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch06_quantifier_array_domain_rejected`, and `ch07_handler_state_type_mismatch_rejected` — are **negative tests** that assert a specific diagnostic (E206, E135, E183, E201, E127, E153, E153, E130, E130, E174, E182, E217, E011, E154, E150, E152, E151, E242, E243, E207, E208, E208, E209, E128, and E336 respectively) via the manifest's `expected_error` field; `ch09_http` and `ch09_inference` are environment-gated (network / API key). Thirteen programs (`ch03_slot_let_chains`, `ch03_slot_noncommutative`, `ch04_nested_option_ctor`, `ch04_primitive_obligations`, `ch05_apply_fn_typing`, `ch06_adt_sort_disambiguation`, `ch07_cross_module_contracts`, `ch07_io_read_char`, `ch07_io_sleep`, `ch07_random_effect`, `ch08_transitive_module_import_mid`, `ch09_http_server`, `ch09_math_builtins`) are at the `verify` level, using Z3-provable contracts.

### Skipped tests

`pytest tests/ -v` skips 77 conformance-stage tests across the two categories below (the suite's remaining skips are platform- or tool-gated and documented beside the tests that declare them):

**Level-limited skips** — the conformance framework only runs tests up to the declared level; stages beyond that level are automatically skipped. These are expected and correct.

| Test | Program | Declared level | Skipped stage | Reason |
|------|---------|---------------|--------------|--------|
| `test_verify[ch02_generic_over_unit_rejected]` | `ch02_generic_over_unit_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E206`): verify stage not run |
| `test_run[ch02_generic_over_unit_rejected]` | `ch02_generic_over_unit_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_verify[ch02_map_unit_value_rejected]` | `ch02_map_unit_value_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E135`): verify stage not run |
| `test_run[ch02_map_unit_value_rejected]` | `ch02_map_unit_value_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_run[ch03_slot_let_chains]` | `ch03_slot_let_chains.vera` | `verify` | `run` | `verify`-level programs don't get a `run` test |
| `test_run[ch03_slot_noncommutative]` | `ch03_slot_noncommutative.vera` | `verify` | `run` | `verify`-level programs don't get a `run` test |
| `test_verify[ch03_typed_holes]` | `ch03_typed_holes.vera` | `check` | `verify` | `check`-level program: verify stage not run |
| `test_run[ch03_typed_holes]` | `ch03_typed_holes.vera` | `check` | `run` | `check`-level program: no standalone `main` |
| `test_verify[ch04_let_unit_rejected]` | `ch04_let_unit_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E183`): verify stage not run |
| `test_run[ch04_let_unit_rejected]` | `ch04_let_unit_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_run[ch04_nested_option_ctor]` | `ch04_nested_option_ctor.vera` | `verify` | `run` | `verify`-level programs don't get a `run` test |
| `test_run[ch04_primitive_obligations]` | `ch04_primitive_obligations.vera` | `verify` | `run` | `verify`-level programs don't get a `run` test |
| `test_verify[ch05_apply_fn_arity]` | `ch05_apply_fn_arity.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E201`): verify stage not run |
| `test_run[ch05_apply_fn_arity]` | `ch05_apply_fn_arity.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_run[ch05_apply_fn_typing]` | `ch05_apply_fn_typing.vera` | `verify` | `run` | `verify`-level programs don't get a `run` test |
| `test_verify[ch05_decreases_float_rejected]` | `ch05_decreases_float_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E127`): verify stage not run |
| `test_run[ch05_decreases_float_rejected]` | `ch05_decreases_float_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_verify[ch05_reserved_fn_name_rejected]` | `ch05_reserved_fn_name_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E153`): verify stage not run |
| `test_run[ch05_reserved_fn_name_rejected]` | `ch05_reserved_fn_name_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_verify[ch05_reserved_keyword_fn_rejected]` | `ch05_reserved_keyword_fn_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E153`): verify stage not run |
| `test_run[ch05_reserved_keyword_fn_rejected]` | `ch05_reserved_keyword_fn_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_verify[ch05_where_helper_outer_slot_rejected]` | `ch05_where_helper_outer_slot_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E130`): verify stage not run |
| `test_run[ch05_where_helper_outer_slot_rejected]` | `ch05_where_helper_outer_slot_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_run[ch06_adt_sort_disambiguation]` | `ch06_adt_sort_disambiguation.vera` | `verify` | `run` | `verify`-level programs don't get a `run` test |
| `test_run[ch07_cross_module_contracts]` | `ch07_cross_module_contracts.vera` | `verify` | `run` | `verify`-level programs don't get a `run` test |
| `test_verify[ch07_cross_module_contracts_lib]` | `ch07_cross_module_contracts_lib.vera` | `check` | `verify` | `check`-level library module: verify stage not run |
| `test_run[ch07_cross_module_contracts_lib]` | `ch07_cross_module_contracts_lib.vera` | `check` | `run` | `check`-level library module: no standalone `main` |
| `test_verify[ch07_handler_state_body_scope_rejected]` | `ch07_handler_state_body_scope_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E130`): verify stage not run |
| `test_run[ch07_handler_state_body_scope_rejected]` | `ch07_handler_state_body_scope_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_run[ch07_io_read_char]` | `ch07_io_read_char.vera` | `verify` | `run` | `verify`-level programs don't get a `run` test |
| `test_run[ch07_io_sleep]` | `ch07_io_sleep.vera` | `verify` | `run` | `verify`-level programs don't get a `run` test |
| `test_verify[ch07_old_outside_ensures_rejected]` | `ch07_old_outside_ensures_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E174`): verify stage not run |
| `test_run[ch07_old_outside_ensures_rejected]` | `ch07_old_outside_ensures_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_run[ch07_random_effect]` | `ch07_random_effect.vera` | `verify` | `run` | `verify`-level programs don't get a `run` test |
| `test_verify[ch07_state_unit_op_param_read_rejected]` | `ch07_state_unit_op_param_read_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E182`): verify stage not run |
| `test_run[ch07_state_unit_op_param_read_rejected]` | `ch07_state_unit_op_param_read_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_verify[ch07_bare_effect_op_rejected]` | `ch07_bare_effect_op_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E217`): verify stage not run |
| `test_run[ch07_bare_effect_op_rejected]` | `ch07_bare_effect_op_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_verify[ch06_quantifier_array_domain_rejected]` | `ch06_quantifier_array_domain_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E128`): verify stage not run |
| `test_run[ch06_quantifier_array_domain_rejected]` | `ch06_quantifier_array_domain_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_verify[ch07_handler_state_type_mismatch_rejected]` | `ch07_handler_state_type_mismatch_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E336`): verify stage not run |
| `test_run[ch07_handler_state_type_mismatch_rejected]` | `ch07_handler_state_type_mismatch_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_verify[ch08_circular_import]` | `ch08_circular_import.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E011`): verify stage not run |
| `test_run[ch08_circular_import]` | `ch08_circular_import.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_verify[ch08_reserved_vera_prefix_rejected]` | `ch08_reserved_vera_prefix_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E154`): verify stage not run |
| `test_run[ch08_reserved_vera_prefix_rejected]` | `ch08_reserved_vera_prefix_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_verify[ch08_cross_module_generic_lib]` | `ch08_cross_module_generic_lib.vera` | `check` | `verify` | `check`-level library module: verify stage not run |
| `test_run[ch08_cross_module_generic_lib]` | `ch08_cross_module_generic_lib.vera` | `check` | `run` | `check`-level library module: no standalone `main` |
| `test_verify[ch08_transitive_module_import_base]` | `ch08_transitive_module_import_base.vera` | `check` | `verify` | `check`-level library module: verify stage not run |
| `test_run[ch08_transitive_module_import_base]` | `ch08_transitive_module_import_base.vera` | `check` | `run` | `check`-level library module: no standalone `main` |
| `test_run[ch08_transitive_module_import_mid]` | `ch08_transitive_module_import_mid.vera` | `verify` | `run` | `verify`-level programs don't get a `run` test |
| `test_verify[ch08_visibility_private]` | `ch08_visibility_private.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E150`): verify stage not run |
| `test_run[ch08_visibility_private]` | `ch08_visibility_private.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_verify[ch08_xmod_widen_lib]` | `ch08_xmod_widen_lib.vera` | `check` | `verify` | `check`-level library module: verify stage not run |
| `test_run[ch08_xmod_widen_lib]` | `ch08_xmod_widen_lib.vera` | `check` | `run` | `check`-level library module: no standalone `main` |
| `test_verify[ch09_builtin_effect_redefinition_rejected]` | `ch09_builtin_effect_redefinition_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E152`): verify stage not run |
| `test_run[ch09_builtin_effect_redefinition_rejected]` | `ch09_builtin_effect_redefinition_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_verify[ch09_builtin_redefinition]` | `ch09_builtin_redefinition.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E151`): verify stage not run |
| `test_run[ch09_builtin_redefinition]` | `ch09_builtin_redefinition.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_verify[ch09_eq_non_derivable_rejected]` | `ch09_eq_non_derivable_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E243`): verify stage not run |
| `test_run[ch09_eq_non_derivable_rejected]` | `ch09_eq_non_derivable_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_run[ch09_http_server]` | `ch09_http_server.vera` | `verify` | `run` | `verify`-level programs don't get a `run` test |
| `test_run[ch09_math_builtins]` | `ch09_math_builtins.vera` | `verify` | `run` | `verify`-level programs don't get a `run` test |
| `test_verify[ch09_ord_adt_rejected]` | `ch09_ord_adt_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E242`): verify stage not run |
| `test_run[ch09_ord_adt_rejected]` | `ch09_ord_adt_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_verify[ch09_sql_injection_rejected]` | `ch09_sql_injection_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E207`): verify stage not run |
| `test_run[ch09_sql_injection_rejected]` | `ch09_sql_injection_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_verify[ch09_sql_placeholder_mismatch_rejected]` | `ch09_sql_placeholder_mismatch_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E208`): verify stage not run |
| `test_run[ch09_sql_placeholder_mismatch_rejected]` | `ch09_sql_placeholder_mismatch_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_verify[ch09_sql_placeholder_let_mismatch_rejected]` | `ch09_sql_placeholder_let_mismatch_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E208`): verify stage not run |
| `test_run[ch09_sql_placeholder_let_mismatch_rejected]` | `ch09_sql_placeholder_let_mismatch_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_verify[ch09_sql_numbered_placeholder_rejected]` | `ch09_sql_numbered_placeholder_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E209`): verify stage not run |
| `test_run[ch09_sql_numbered_placeholder_rejected]` | `ch09_sql_numbered_placeholder_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |

**Environment-gated skips** — these programs require network access or a live API key that is not available in CI. They pass `vera check` (type-checking) but cannot be executed.

| Test | Program | Declared level | Skipped stage | Reason |
|------|---------|---------------|--------------|--------|
| `test_verify[ch09_http]` | `ch09_http.vera` | `check` | `verify` | Requires outbound HTTP; unavailable in CI sandbox |
| `test_run[ch09_http]` | `ch09_http.vera` | `check` | `run` | Requires outbound HTTP; unavailable in CI sandbox |
| `test_verify[ch09_inference]` | `ch09_inference.vera` | `check` | `verify` | Requires `VERA_*_API_KEY`; not set in CI |
| `test_run[ch09_inference]` | `ch09_inference.vera` | `check` | `run` | Requires `VERA_*_API_KEY`; not set in CI |

To run the environment-gated tests locally: set `VERA_ANTHROPIC_API_KEY` (or another provider key) and ensure outbound HTTP is available, then `vera run tests/conformance/ch09_http.vera` / `vera run tests/conformance/ch09_inference.vera`.

### Directory structure

```
tests/conformance/
├── manifest.json              # Machine-readable test metadata
├── ch01_int_literals.vera     # Chapter 1: Integer literals
├── ch01_float_literals.vera   # Chapter 1: Float64 literals
├── ch01_string_escapes.vera   # Chapter 1: String escape sequences
├── ...                        # 179 programs total, organized by spec chapter
├── ch07_state_handler.vera    # Chapter 7: State<T> effect handler
├── ch07_exn_handler.vera      # Chapter 7: Exn<E> effect handler
├── ch09_numeric_builtins.vera # Chapter 9: Numeric built-in functions
├── ch09_type_conversions.vera # Chapter 9: Numeric type conversions
├── ch09_markdown.vera         # Chapter 9: Markdown standard library
├── ch09_regex.vera            # Chapter 9: Regular expression matching
├── ch09_decimal.vera          # Chapter 9: Decimal type operations
├── ch09_json.vera             # Chapter 9: JSON standard library
├── ch09_http.vera             # Chapter 9: Http effect (check level)
└── ch09_float_predicates.vera # Chapter 9: Float64 predicates and constants
```

### Manifest

`manifest.json` maps each program to its spec chapter, test level, and feature tags:

```json
{
  "id": "ch04_arithmetic",
  "file": "ch04_arithmetic.vera",
  "chapter": 4,
  "title": "Arithmetic operators",
  "level": "run",
  "spec_ref": "Section 4.1",
  "features": ["add", "sub", "mul", "div", "mod", "unary_neg"]
}
```

The manifest is the machine-readable feature inventory — agents can query it to find which features exist and where they are tested.

### Running the conformance suite

```bash
# Via pytest (parametrized — 895 tests)
pytest tests/test_conformance.py -v

# Via standalone script (used in CI and pre-commit)
python scripts/check_conformance.py
```

The pytest runner (`test_conformance.py`) parametrizes over every manifest entry and runs five checks per program: parse, check, verify, run, and format idempotency.

### Adding a conformance test

1. Write a `.vera` program in `tests/conformance/` following the naming convention `chNN_feature_name.vera`
2. Include a header comment indicating the spec chapter and what the program tests
3. Ensure the program has a `main` function (for `run`-level tests)
4. Format it: `vera fmt --write tests/conformance/your_file.vera`
5. Add an entry to `manifest.json` with the appropriate level and feature tags
6. Run `python scripts/check_conformance.py` to validate

When implementing a new language feature, the conformance program should be written *first* — this is test-driven development against the spec.

## Compiler Code Coverage

Coverage by module, measured by `pytest --cov=vera`:

| Module | Stmts | Miss | Coverage |
|--------|------:|-----:|---------:|
| `wasm/` | 11,130 | 566 | 95% |
| `codegen/` | 3,605 | 239 | 93% |
| `checker/` | 1,223 | 68 | 94% |
| `lsp/` | 492 | 52 | 89% |
| `obligations/` | 188 | 1 | 99% |
| `browser/` | 21 | 0 | 100% |
| `verifier.py` | 702 | 31 | 96% |
| `transform.py` | 617 | 24 | 96% |
| `formatter.py` | 675 | 49 | 93% |
| `ast.py` | 462 | 17 | 96% |
| `smt.py` | 651 | 32 | 95% |
| `markdown.py` | 413 | 54 | 87% |
| `types.py` | 182 | 7 | 96% |
| `errors.py` | 129 | 1 | 99% |
| `environment.py` | 339 | 8 | 98% |
| `cli.py` | 583 | 29 | 95% |
| `parser.py` | 45 | 0 | 100% |
| `resolver.py` | 68 | 2 | 97% |
| `slots.py` | 41 | 5 | 88% |
| `skip.py` | 12 | 3 | 75% |
| `tester.py` | 389 | 3 | 99% |
| `prelude.py` | 187 | 9 | 95% |
| `registration.py` | 18 | 0 | 100% |
| `__init__.py` | 2 | 0 | 100% |
| **Total** | **22,174** | **1,200** | **95%** |

The lowest-coverage files of any size are `vera/lsp/server.py` at 64% (pygls feature-registration glue, exercised end-to-end by editors rather than by unit tests) and `wasm/inference.py` at 80% (deep type-dispatch branches for specific builtin return types).

## Contract Verification Coverage

Vera's verifier classifies each contract into one of three tiers. **Tier 1** contracts are proved correct statically by Z3; the non-trivial runtime check is still emitted as a defensive backstop (code generation is tier-agnostic — see spec §11.8), so a Tier-1 proof means the guard provably never fires, not that it is absent. **Tier 3** contracts cannot be fully decided by the SMT solver, so their runtime check is the only line of defence. The verifier never rejects a valid program; it simply warns when a contract drops to Tier 3.

Across all 42 example programs (live sums of `vera verify --json`; regenerate by summing the `verification` block over `examples/*.vera`):

| Metric | Value |
|--------|-------|
| **Tier 1 (static)** | 357 obligations — proved automatically by Z3 |
| **Tier 3 (runtime)** | 105 obligations — checked at runtime |
| **Total** | 462 obligations (77.3% static; the summary's `total` field equals `tier1_verified + tier3_runtime`, derived from the reified obligation stream) |

The Tier 3 population is dominated by a few built-in-heavy examples (`life.vera` 24, `array_utilities.vera` 12, `collections.vera` 11, `string_utilities.vera` 6, `gc_pressure.vera` 5, `html.vera` 5), with a long tail of one to four per example across eighteen more.  The recurring reasons: postconditions over collection/string/HTML built-in pipelines outside the decidable fragment, `decreases` metrics the fragment cannot express, `old`/`new` state modelling (not yet implemented), and generic type parameters without a Z3 sort.

The Tier 1 fragment covers: integer/boolean arithmetic, comparisons, if/else, let bindings, match expressions, ADT constructors, function calls (modular postcondition), `length`, and `decreases` clauses (self-recursive, mutual recursion via where-blocks, Nat and structural ADT measures).

## Language Feature Coverage

How Vera language features (by spec chapter) map to test files and example programs:

| Spec chapter | Feature | Test files | Conformance | Examples |
|-------------|---------|-----------|-------------|----------|
| Ch 1: Lexical | Literals (Int, Float64, Bool, Byte, String) | test_ast, test_codegen_* | ch01_int_literals, ch01_float_literals, ch01_bool_literals, ch01_byte_literals | most examples |
| Ch 1: Lexical | String escape sequences (`\n`, `\t`, `\\`, `\"`, `\r`, `\0`, `\u{XXXX}`) | test_ast, test_codegen_* | ch01_string_escapes | io_operations, file_io |
| Ch 1: Lexical | Comments | test_parser | ch01_comments | — |
| Ch 2: Types | Int, Nat, Bool, String, Float64, Byte, Unit | test_codegen_*, test_checker_* | ch02_builtin_types | most examples |
| Ch 2: Types | ADTs (algebraic data types), Option, Result | test_codegen_*, test_checker_* | ch02_adt_basic, ch02_adt_recursive, ch02_option_result | pattern_matching, list_ops |
| Ch 2: Types | Refinement types | test_codegen_*, test_verifier_* | ch02_refinement_types | refinement_types, safe_divide |
| Ch 2: Types | Generics (`forall<T>`) | test_codegen_monomorphize, test_checker_* | ch02_generics | generics |
| Ch 3: Slots | `@T.n` references, De Bruijn indexing | test_checker_*, test_codegen_* | ch03_slot_basic, ch03_slot_indexing, ch03_slot_result | all 42 examples |
| Ch 4: Expressions | Arithmetic, comparison, boolean, unary ops | test_codegen_*, test_checker_* | ch04_arithmetic, ch04_comparison, ch04_boolean_ops, ch04_int_overflow | factorial, absolute_value |
| Ch 4: Expressions | If/else, let, match, pipe operator | test_codegen_*, test_checker_* | ch04_if_else, ch04_let_binding, ch04_match_basic, ch04_match_nested, ch04_pipe_operator | pattern_matching |
| Ch 4: Expressions | String and array builtins | test_codegen_* | ch04_string_builtins, ch04_array_ops | string_ops |
| Ch 5: Functions | Declarations, recursion, mutual recursion | test_codegen_*, test_checker_* | ch05_basic_function, ch05_recursion, ch05_mutual_recursion | factorial, mutual_recursion |
| Ch 5: Functions | Closures, higher-order functions | test_codegen_closures | ch05_closures | closures |
| Ch 5: Functions | Visibility (`public`/`private`) | test_checker_* | ch05_visibility | modules |
| Ch 6: Contracts | Preconditions (`requires`) | test_codegen_contracts, test_verifier_* | ch06_requires | safe_divide |
| Ch 6: Contracts | Postconditions (`ensures`) | test_codegen_contracts, test_verifier_* | ch06_ensures | absolute_value |
| Ch 6: Contracts | Decreases clauses, assert/assume | test_verifier_*, test_codegen_* | ch06_decreases, ch06_assert_assume | factorial |
| Ch 6: Contracts | Quantifiers (forall, exists) | test_codegen_*, test_verifier_* | ch06_quantifiers | quantifiers |
| Ch 7: Effects | Pure, IO, State\<T\> | test_codegen_*, test_checker_* | ch07_pure, ch07_io, ch07_state_handler | hello_world, increment, io_operations, file_io |
| Ch 7: Effects | Effect handlers (State\<T\>, Exn\<E\>) | test_codegen_*, test_checker_* | ch07_state_handler, ch07_exn_handler | effect_handler |
| Ch 9: Stdlib | Numeric builtins (abs, min, max, floor, ceil, round, sqrt, pow) | test_codegen_*, test_checker_* | ch09_numeric_builtins | — |
| Ch 9: Stdlib | Type conversions (int_to_float, float_to_int, nat_to_int, int_to_nat, byte_to_int, int_to_byte) | test_codegen_*, test_checker_* | ch09_type_conversions | — |
| Ch 9: Stdlib | Float64 predicates (float_is_nan, float_is_infinite, nan, infinity) | test_codegen_*, test_checker_* | ch09_float_predicates | — |
| Ch 7: Effects | Effect subtyping (§7.8), call-site checking | test_types, test_checker_* | — | — |
| Ch 2: Types | Bidirectional type checking (local inference) | test_checker_* | — | — |
| Ch 4: Expressions | Nested constructor patterns in match | test_codegen_* | ch04_match_nested | pattern_matching |
| Ch 8: Modules | Imports, cross-module typing and codegen | test_codegen_modules, test_resolver | — | modules |
| Ch 11: Compilation | Cross-module name collision detection (E608/E609/E610) | test_codegen_modules | — | — |
| Ch 9: Stdlib | Markdown (md_parse, md_render, md_has_heading, md_has_code_block, md_extract_code_blocks) | test_codegen_*, test_markdown | ch09_markdown | markdown |
| Ch 9: Stdlib | Regex (regex_match, regex_find, regex_find_all, regex_replace) | test_codegen_*, test_checker_* | ch09_regex | regex |
| Ch 9: Stdlib | Map, Set, Decimal collections | test_codegen_*, test_checker_* | ch09_map, ch09_set, ch09_decimal, ch09_decimal_generics | collections |
| Ch 9: Stdlib | Json (json_parse, json_stringify, json_get, json_array_get, json_array_length, json_keys, json_has_field, json_type) | test_codegen_*, test_checker_* | ch09_json | json |
| Ch 9: Stdlib | Html (html_parse, html_to_string, html_query, html_text, html_attr) | test_codegen_*, test_checker_* | ch09_html | html |
| Ch 9: Stdlib | Http effect (Http.get, Http.post) | test_codegen_*, test_checker_* | ch09_http | http |
| Ch 9: Stdlib | Async/Future\<T\> effect (async, await, #841 concurrency) | test_checker_effects, test_codegen_effects | ch09_async | — |
| Ch 7: Effects | HttpServer marker effect, `vera serve` (§7.7.5, #305) | test_serve, test_checker_effects | ch09_http_server | http_server |
| Ch 11: Compilation | Contract-driven testing (Z3 input gen + WASM execution) | test_tester, test_cli | — | safe_divide, factorial |
| Ch 12: Runtime | Browser runtime parity (JS host bindings match Python) | test_browser | — | — |
| Ch 13: WASI | WASI Preview 2 target (component emission, wasip2 host runner, dual-target differential); `--world server` wasi:http components (§13.7) | test_wasi_target | run-level suite via the dual-target differential | — |

## Test Helpers

Each test module defines module-level helper functions (no `conftest.py`).  The
three split suites are the exception: the `test_checker_*.py` files (split from
`test_checker.py`, #420) import their shared helpers from
`tests/checker_helpers.py`; the `test_codegen_*.py` feature files (split from
`test_codegen.py`, #419) import theirs — plus the `_IO_PRELUDE` /
`_INLINE_BUILTIN_NAMES` fixture constants — from `tests/codegen_helpers.py`;
and the `test_verifier_*.py` theme files (split from `test_verifier.py`, #839)
import theirs — plus the `EXAMPLES_DIR` / `ALL_EXAMPLES` corpus constants and
the `_MK` source template — from `tests/verifier_helpers.py`.

```python
# test_checker_*.py pattern (helpers from tests/checker_helpers.py):
_check_ok(source)              # assert no type errors
_check_err(source, "match")    # assert at least one error matching substring

# test_verifier_*.py pattern (helpers from tests/verifier_helpers.py):
_verify_ok(source)             # assert no verification errors
_verify_err(source, "match")   # assert at least one verification error
_verify_warn(source, "match")  # assert at least one warning

# test_codegen_*.py pattern (helpers from tests/codegen_helpers.py):
_compile_ok(source)            # assert compilation succeeds
_run(source, fn, args)         # compile + execute, return result
_run_io(source, fn, args)      # compile + execute, return captured stdout
_run_trap(source, fn, args)    # compile + execute, assert WASM trap
```

`_compile()` — and therefore every helper built on it — asserts the #1185
invariant on the emitted WAT: a module that contains a `call_indirect` must
declare a function table.  This is a differential over the two sides that have
to agree (the instruction stream and the table section), so a future desync
fails wherever it is introduced rather than at the next `vera run`.
`test_codegen_closures.py` owns a local `_compile` and carries the same gate
explicitly, being the densest closure / `call_indirect` coverage in the suite.
Only that direction is universal: a table with no indirect call is inert and
happens legitimately when a lift succeeds but the sole carrier is dropped for
an unrelated reason.  Fixtures where the table's presence is itself under test
use `_assert_call_indirect_iff_table` for the biconditional.

## Round-Trip Testing

Every one of the 42 example programs in `examples/` is tested through **every pipeline stage** via parametrised tests: parsing, AST transformation, type checking, contract verification, WASM compilation, and execution. If you add a new `.vera` example, it is automatically included in the round-trip suite.

The formatter has **idempotency tests**: `format(format(x)) == format(x)` for all tested programs.

## Stress Tests

Scale-dependent regression tests live in `tests/test_stress.py` (#596).  These exercise Vera programs at sizes where historical bugs (#570 iterative-builder shadow-stack overflow at ~4000 elements, #515 GC self-fault under sustained allocation, #593 Conway's Life corruption at 12×30+) first manifested, plus 2-3x safety margin.

### The 9 initial test programs

Each test compiles a self-contained Vera program, executes it via the in-process API, and asserts on a SPECIFIC observable.  Iteration counts are tuned to the smallest scale where each bug class historically manifested.

Tests marked **[eager-GC]** also run under the `VERA_EAGER_GC=1` lane (see below).

**1. `test_array_map_over_10k_int_array`** **[eager-GC]** — `array_map` over a 10,000-element `Array<Int>`, each element incremented by 1.  Asserts `array_length` of the result == 10000.  Pre-#570 this class of program shadow-stack-overflowed at ~4,000 elements; 10K is a 2.5x safety margin.  Pins the iterative-builder fix and acts as an early-warning for any future regression in shadow-stack hygiene under `array_map`.

**2. `test_array_map_over_5k_nested_bool_array`** **[eager-GC]** — `array_map` over a 5,000-element `Array<Int>` producing a fresh `Array<Bool>` (`[true, false, true]`) per iteration.  Asserts the outer length == 5000.  Tests per-iteration allocation pressure where each closure call allocates and the result must remain rooted across the loop.  Pre-#570 + pre-#515 this class corrupted intermediate roots; the test pins the per-iteration alloc/root hygiene fix.

**3. `test_deep_tail_recursion_with_allocating_arg`** **[eager-GC]** — 1,000-deep tail recursion over `loop(@Int, @Int -> @Int)` where each iteration allocates a fresh `let @Array<Int> = [@Int.0, @Int.1]` before recursing.  Asserts the final accumulator == 2,000 (1,000 × `array_length([_, _])` = 1,000 × 2).  Tests the TCO / GC interaction (#549) — tail-call optimisation must not discard the shadow-stack roots that keep the allocating arg live.  The body allocates a genuine heap array each iteration (a string-pool literal would not trigger `needs_alloc`), so the eager-GC lane fires on every iteration.

**4. `test_conways_life_grid_alloc_and_count_alive_20x20`** **[eager-GC]** — synthetic regression covering #593 (Life corruption from gen 1+ at 12×30).  Bug is closed; this test pins the fix.  The program builds a 20×20 all-false `Array<Array<Bool>>` via nested `array_map`-of-`array_range`, then runs a single `count_alive` pass — an array-fold over array-fold that walks every cell.  Asserts the count == 0.  This is a **structural-shape** test, not a Life simulation: it does NOT run 100 generations (the original test name implied that; the rename in #669 corrects it).  The structural shape — 400-cell allocation, nested `array_fold` of `array_fold`, captured outer-binding references inside the inner closure — is what matters; the trivially-deterministic outcome (all-false → 0) makes the test fast and unambiguous while still exercising the code paths #593 hit.  (An earlier version of this entry also cited #595 — that was misattributed; #595 is a cleanup-path bug exercised by `TestHostSleepKeyboardInterrupt` in `test_runtime_traps.py`, not by this stress test.)

**5. `test_array_fold_100k_iterations`** — `array_fold` over an `array_range(0, 100000)` summing all values.  Asserts the result == 4,999,950,000 (the closed-form sum of 0..99999).  Tests the fold accumulator across many GC cycles.  Pre-#487 / #348 (worklist + multi-page grow) this class of program ran the heap into multi-page territory and tripped allocation-pressure bugs; the test pins the fixes.  The closed-form assertion catches any regression that silently short-circuits or skips iterations.  *Not in the eager-GC lane* — allocation-pressure target, not GC-rooting; 100K × forced-GC would inflate suite time without strengthening detection.

**6. `test_10k_string_allocations`** **[eager-GC]** — `array_fold` over `array_range(0, 10000)` where each iteration produces a fresh String via `let @String = "\(@Int.0)"` and accumulates `string_length`.  Asserts the total == 38,890 (10 × 1-digit + 90 × 2-digit + 900 × 3-digit + 9000 × 4-digit).  Pre-#573 (wrap-table compaction) and #575 / #576 (host-store reclamation) this class of program would leak handles or self-fault under sustained String allocation; the test pins the fixes.  The digit-count assertion is uniquely sensitive to any short-circuit because it varies non-linearly with iteration count.

**7. `test_state_handler_1k_ops`** **[eager-GC]** — 1,000 `State<Int>` get/put cycles within a single `handle[State<Int>](@Int = 0) { ... } in { ... }` scope, driven by a `count_up(@Int -> @Int)` helper that does `get(()); put(state + 1); count_up(n - 1)`.  Asserts the final state == 1000.  Pins the handler installation + resume continuation plumbing under sustained host-import call rate.  Pre-stage-11 / pre-#535 work, large State-handler programs accumulated captured-frame roots without bound.

**8. `test_10k_io_print_calls`** — 10,000 `IO.print("x\n")` calls in sequence via a `loop(@Int -> @Unit)` helper, with `tee_stdout=True` so the captured output buffer grows in lock-step.  Asserts the captured stdout contains exactly 10,000 `x` characters.  Exercises the `host_print` bridge at sustained rate; tests the in-process stdout-capture buffer's growth and the host-import call path under load.  The character-count assertion (rather than line-count) is robust to subtle buffering variations.  *Not in the eager-GC lane* — host-import target, not GC-rooting; the `host_print` bridge doesn't allocate Vera-heap data.

**9. `test_tco_with_allocation_1m_iterations`** **[eager-GC]** — 1,000,000-deep tail recursion over `loop(@Int, @Int -> @Int)` with a fresh `let @Array<Int> = [_, _]` per iteration.  Asserts the final accumulator == 2,000,000 (1M × 2).  The high-volume companion to #3.  1M plain `call`s would blow the WASM call stack at ~30K frames; the `return_call` + `$gc_sp` restore keeps shadow-stack usage flat, so 1M iterations complete in constant memory in ~190ms in both default and eager-GC modes.  A shadow-stack leak per iteration would trap the overflow guard around 1,300 iterations (16K shadow stack / ~12 bytes per leaked frame); completing all 1M proves the invariant.

### Eager-GC lane

Seven of the nine tests target GC-rooting bug classes (#570 / #515 / #549 / #573 / #593 / captured-frame State handlers).  Each of those runs under **two parameter modes**: default GC and `VERA_EAGER_GC=1`.  The `VERA_EAGER_GC` env var (read at compile time by `vera/codegen/assembly.py`) emits a `call $gc_collect` as the first instruction of the runtime's `$alloc` function, forcing a full GC pass on every allocation.

This converts latent missing-shadow-root bugs from "fires occasionally at scale" to "fires on the very next allocation," so a regression that would normally require thousands of iterations to surface will fail on the first or second iteration under eager GC.  The eager lane embeds this diagnostic capability as ongoing regression coverage.

The eager-GC lane is implemented via a `pytest.mark.parametrize("eager_gc", [False, True], ids=["default_gc", "eager_gc"])` decorator + a `monkeypatch` fixture that scopes the env var to the parametrised test instance.  The two non-parametrised tests — `test_array_fold_100k_iterations` (allocation-pressure target, not GC-rooting) and `test_10k_io_print_calls` (host-import target) — would inflate the suite under eager GC without strengthening detection of the relevant bug class.

### Configuration and behaviour

**Default behaviour**: stress tests are skipped from the per-PR pytest run via `addopts = "-m 'not stress'"` in `pyproject.toml`.  Local invocation:

```bash
pytest -m stress                    # all 16 parametrised test instances (9 logical tests × eager-GC lane)
pytest tests/test_stress.py -m stress -v   # full stress suite, verbose
pytest tests/test_stress.py::test_array_map_over_10k_int_array -m stress -v   # both modes of one test
pytest "tests/test_stress.py::test_array_map_over_10k_int_array[eager_gc]" -m stress -v   # one mode only
```

**CI integration**: `.github/workflows/nightly-stress.yml` runs them in three triggers:

1. **Nightly cron** (`0 6 * * *` UTC) — primary safety net, catches drift in a daily window so bisection cost stays small.  **Failures auto-file (or comment on) a tracking issue** with the `stress-regression` label so the regression is visible to anyone watching the issue feed.  See the failure-reporting subsection below.
2. **Path-filtered PRs** touching `vera/codegen/**`, `vera/wasm/**`, `vera/checker/**`, `tests/test_stress.py`, or the workflow file itself — fail-fast for PRs that change code most likely to break stress invariants.  `vera/checker/**` is included because the AST shape it produces flows into codegen — a checker change that subtly alters the AST can break runtime invariants without touching `vera/codegen/` or `vera/wasm/`.  PR failures show on the PR's checks tab; no tracking issue is filed (the PR author already sees the failure).
3. **`workflow_dispatch`** — manual trigger from the Actions tab for local-suspicious commits.  Failures are visible to whoever triggered the run; no tracking issue is filed.

**Failure reporting (cron only)**: when the nightly cron fails, the workflow opens an issue titled "Nightly stress regression on main (tracking)" with the `stress-regression` label, including the commit SHA and the run URL.  If an open issue with that label already exists, the new failure posts a comment on it instead of filing a duplicate — so the issue persists across days of failures until a maintainer manually closes it.  The `stress-regression` label is auto-created on first failure.  This converts cron failures from "visible only to whoever opens the Actions tab" to "visible in the issue feed where Vera work is already triaged."  Implementation uses `actions/github-script@v7` with `issues: write` job-scoped permission.

**Budget**: the full suite completes in well under the 5-minute target — measured at **0.66s in-process** on a developer laptop on 2026-05-13 for all 16 test instances (9 logical × eager-GC lane on 7 of them).  CI cold-start adds workflow setup time on top.  Iteration counts are tuned to the smallest scale where each bug class has historically manifested with ~2-3x safety margin, NOT maximised — the goal is reliable detection of the bug class, not benchmarking.  If this measured figure drifts more than ~2x in either direction, treat it as a signal: either iteration counts have grown without rationale (revisit per the "Adding a stress test" rule 2) or a runtime perf regression has landed.

**Assertion shape**: each test asserts on a SPECIFIC observable (e.g. `array_fold` returning the closed-form sum `4999950000`, `IO.print` producing exactly 10000 `x` characters), not just "completed without crashing".  This catches a future regression where the loop silently short-circuits or skips iterations.

### Adding a stress test

A new stress test should:

1. **Target a specific scale axis** (iteration count, allocation pressure, recursion depth, handler-op rate, etc.) and **name the bug class it guards against** in its docstring.  Reference the issue number(s).
2. **Pick the smallest scale that reliably manifested the bug class historically**, plus ~2-3x safety margin.  Don't maximise — bigger isn't better and inflates the suite.
3. **Assert on a SPECIFIC observable** with a closed-form or otherwise unambiguous expected value.  Avoid "no exception raised" — that passes silently when the loop short-circuits.
4. **Use the `_run` helper** (or a parallel helper for non-pure tests) — it handles tempfile lifecycle, parsing, compilation, error checking, and execution.
5. **Carry `pytestmark = pytest.mark.stress` at module level** (the file already does) so the test is collected only under `pytest -m stress`.
6. **Opt into the eager-GC lane** if the target bug class is GC-rooting-related (shadow-stack, captured-frame, alloc-pressure-root-loss).  Add `@EAGER_GC_PARAMS` above the function, change the signature to `(eager_gc: bool, monkeypatch: pytest.MonkeyPatch)`, and pass both through to `_run(src, eager_gc=eager_gc, monkeypatch=monkeypatch)`.  Skip the lane if the bug class is unrelated to GC rooting (host-import call rate, parser perf) — doubling the test cost without strengthening detection is the wrong trade.

## Mutation Testing

A passing suite is necessary, not sufficient — a green test can pass *for the wrong reason* (the #680 audit found 8 such tests in one 57-test battery; #734 had to mutation-validate its own harness).  Mutation testing checks the checker: it deliberately breaks each line of `vera/` and confirms a test flips RED.  A surviving mutant is a test gap — a **weak test** to strengthen or an **equivalent mutant** to annotate (`# pragma: no mutate`).

The full mechanics — the tool decision (`mutmut`, the `[mutation]` extra, the `[tool.mutmut]` config), the **in-process-oracle caveat** (subprocess suites import the un-mutated package, so they can't kill mutants), resume-after-hard-kill, the Z3-flakiness guardrail, and the survivor-triage workflow — live in the runbook: **[`MUTATION.md`](MUTATION.md)**.

**Baseline — soundness core.**  The first sweep covers `verifier.py`, `smt.py`, `checker/`, and `obligations/`: 10,620 mutants, **80.8% caught**, 2,038 survivors.  The committed score is `mutation-summary.csv` (per-module, diff-able) plus a README badge (`mutation.json`, regenerated by `scripts/mutation_report.py`); the full survivor inventory and per-module chart are attached to [#387](https://github.com/aallan/vera/issues/387).  Soundness-core triage and the whole-`vera/` sweep — deferred behind the [#421](https://github.com/aallan/vera/issues/421) `execute()` decomposition, which otherwise inflates a mutant file mutmut can't index — are tracked there.

Mutation testing runs **locally** for now (the measure-all sweep is multi-day; CI's 6 h job cap can't hold it).  A non-gating on-demand workflow and a diff-scoped PR gate are deferred to a focused follow-up PR — see `MUTATION.md` § CI.

## Test Fixture Conventions

Cross-platform footguns hit by the post-#637 Windows CI rollout (PRs #639/#643/#644/#646).  Each has a workaround that makes the fixture portable across Linux / macOS / Windows.

### Tempfiles handed off to subprocesses must use `delete=False`

Windows can't reopen a file while another handle is still held; if a test fixture writes to a tempfile via `with tempfile.NamedTemporaryFile(delete=True) as f:` and then runs `subprocess.run([..., f.name])` inside the `with` block, the subprocess fails with a `PermissionError` because the parent still holds the handle.  Unix allows concurrent handles so the same fixture works there.

```python
# Wrong — fails on Windows:
with tempfile.NamedTemporaryFile(mode="w", suffix=".vera", delete=True) as f:
    f.write(content)
    f.flush()
    subprocess.run([sys.executable, "-m", "vera.cli", "check", f.name])

# Right — portable:
f = tempfile.NamedTemporaryFile(mode="w", suffix=".vera", delete=False)
try:
    f.write(content)
    f.close()
    subprocess.run([sys.executable, "-m", "vera.cli", "check", f.name])
finally:
    Path(f.name).unlink(missing_ok=True)
```

Surfaced via `tests/test_html.py::TestHtmlCodeSamples` — see PR #646 for the fix.

### Paths embedded into Vera string literals must use POSIX form

Windows tempfile paths look like `C:\Users\runner\AppData\Local\Temp\...`.  Vera's grammar (correctly) rejects `\U` as an invalid string-literal escape, so embedding such a path via f-string interpolation trips `[E009] Invalid escape sequence: \U` at parse time.  Convert to POSIX form before embedding:

```python
# Wrong — fails on Windows:
source = f'IO.read_file("{tmp_path}")'

# Right — portable (Windows file APIs accept forward slashes).
# `Path(tmp_path).as_posix()` works whether `tmp_path` is a str
# (from `tempfile.NamedTemporaryFile().name`) or a `pathlib.Path`
# (from pytest's `tmp_path` fixture).  Don't use `tmp_path.replace`
# — that's `str.replace` on a string but `Path.replace` (the
# rename method!) on a Path, which would silently move the file.
vera_path = Path(tmp_path).as_posix()
source = f'IO.read_file("{vera_path}")'
```

Surfaced via `tests/test_codegen_io.py::TestIOOperations::test_io_read_file_*` — see PR #643 for the fix.

### File I/O without explicit encoding falls back to the locale default

Python's text-mode `open()` / `read_text()` / `write_text()` without an explicit `encoding=` kwarg defaults to `locale.getpreferredencoding()`, which is **cp1252 on en-US Windows**.  Tests that read or write files containing `→` (right arrow), `—` (em-dash), or other non-ASCII characters fail on Windows with `UnicodeEncodeError: 'charmap' codec can't encode '→'` or `UnicodeDecodeError: ... 0x97`.

Every text-mode `open()` / `read_text()` / `write_text()` under `vera/`, `scripts/`, `tests/` — **and** every `subprocess.run/Popen/check_output(..., text=True)` capture and text-mode `tempfile.NamedTemporaryFile` — therefore MUST pass an explicit `encoding="utf-8"`, enforced by `scripts/check_explicit_encoding.py` (pre-commit + CI lint, #645).  The `vera` CLI additionally reconfigures its stdin/stdout/stderr to UTF-8 at startup, so a Vera program reading or printing `→` / `—` is UTF-8 on any locale.  Together these made text I/O locale-independent and let the `PYTHONUTF8=1` CI backstop (#641) be removed.  Use the explicit form (a deliberate non-UTF-8 site can opt out with `# encoding-exempt: <reason>`):

```python
# Implicit — locale-dependent (cp1252 on Windows); rejected by the gate:
text = path.read_text()

# Explicit — works everywhere:
text = path.read_text(encoding="utf-8")
```

Surfaced via ~9 tests across `test_codegen_monomorphize.py`, `test_codegen_closures.py`, `test_html.py`, and the other `test_codegen_*.py` split files — see PR #646 for the CI-side fix.

## Adding Tests

When extending the compiler, add tests following the existing patterns:

1. **New grammar construct:** Add parser tests to `test_parser.py` (positive and negative)
2. **New AST node:** Add transformation tests to `test_ast.py` (check node fields, spans, serialisation)
3. **New type rule:** Add checker tests to the matching `test_checker_*.py` phase file using `_check_ok()`/`_check_err()` (imported from `tests/checker_helpers.py`)
4. **New SMT support:** Add verifier tests to the matching `test_verifier_*.py` theme file using `_verify_ok()`/`_verify_err()` (imported from `tests/verifier_helpers.py`)
5. **New codegen support:** Add compilation tests to the matching `test_codegen_*.py` feature file using `_compile_ok()`/`_run()`/`_run_trap()` (imported from `tests/codegen_helpers.py`)
6. **New example program:** Add to `examples/` -- it is automatically included in round-trip tests
7. **New error pattern:** Add formatting tests to `test_errors.py`
8. **New tester feature:** Add tests to `test_tester.py` using `_test(source)` helper
9. **New host binding:** Add parity tests to `test_browser.py` to ensure the JavaScript runtime stays in sync with the Python runtime

## Validation Scripts

Twenty-two scripts in `scripts/` validate cross-cutting concerns beyond unit tests (one of them — `build_site.py` — generates rather than checks; the doc-block gates share the fence-annotation reader `scripts/doc_annotations.py`, a helper module rather than a gate):

| Script | What it validates |
|--------|-------------------|
| `check_conformance.py` | All 179 conformance entries hold at their declared level (parse/check/verify/run) — positives pass; the negatives fail `check` with their `expected_error` E-code |
| `check_examples.py` | All 42 `.vera` examples pass `vera check` + `vera verify` |
| `check_corpus_canonical.py` | All 227 corpus programs (recursive over `examples/` + `tests/conformance/`) are in canonical form under `vera fmt` |
| `check_examples_readme.py` | Every `vera run` command in examples/README.md references an existing file and exported function |
| `check_spec_examples.py` | 189 parseable code blocks from spec chapters: parse, type-check, and verify |
| `check_readme_examples.py` | All Vera code blocks in README.md parse correctly |
| `check_skill_examples.py` | All Vera code blocks in SKILL.md parse correctly |
| `check_faq_examples.py` | All Vera code blocks in FAQ.md parse correctly |
| `check_pypi_readme_examples.py` | All Vera code blocks in PYPI_README.md parse, check, and verify |
| `check_examples_doc.py` | All Vera code blocks in EXAMPLES.md parse correctly |
| `check_html_examples.py` | All Vera code blocks in docs/index.html pass parse + check + verify |
| `check_site_assets.py` | Generated site assets under `docs/` are up-to-date, and `check_fact_coherence()` verifies the load-bearing facts of `docs/index.html` and `docs/index.md` agree (#1154) |
| `check_version_sync.py` | `pyproject.toml`, `vera/__init__.py`, and the docs badge carry the same version |
| `check_doc_counts.py` | Counts cited in the docs match the live codebase, KNOWN_ISSUES refactoring counts within ±10%, HISTORY version-row format |
| `check_limitations_sync.py` | Limitation tables consistent across KNOWN_ISSUES.md, vera/README.md, spec chapters, SKILL.md, and LSP_SERVER.md |
| `check_changelog_updated.py` | CHANGELOG.md gains an entry when substantive files change (`Skip-changelog:` trailer to bypass) |
| `check_walker_coverage.py` | Every walker function in `vera/` covers every `Expr` subclass via `isinstance` dispatch or `# WALKER_COVERAGE:` checklist comment (#597) |
| `check_diagnostic_fields.py` | Every diagnostic in `vera/` carries rationale + spec_ref, and errors also a `fix` (warnings exempt); every present spec_ref resolves to a real spec section; every literal `error_code` is registered in `ERROR_CODES` (#828); `# diag-fields-exempt: <reason>` waives missing/unresolvable fields only — never a wrong-but-resolving spec_ref or an unregistered error_code (#682, #955) |
| `check_e602_clean.py` | No unexpected E602/E604 silent-skip sites outside the explicit allowlist |
| `check_doc_builtin_shadowing.py` | No documentation example defines a function named after an opaque verifier-modelled built-in (would fail `vera check` with E151); the `spec/09` signature reference is exempt ([#819](https://github.com/aallan/vera/issues/819)) |
| `check_wheel_availability.py` | Every runtime dependency ships wheels for all supported platforms |
| `check_licenses.py` | All installed packages have MIT-compatible licenses |
| `build_site.py` | Regenerates the AI-readable site assets that `check_site_assets.py` verifies |

These run in both pre-commit hooks and CI, so issues are caught locally before they reach the remote.

### Spec validation pipeline

`check_spec_examples.py` pushes spec code blocks through three compiler stages. A block that intentionally fails a stage carries an inline annotation on the line before its fence — `<!-- vera:skip-parse category="..." reason="..." -->` (or `vera:skip-check` / `vera:skip-verify`; see `scripts/doc_annotations.py` and [#538](https://github.com/aallan/vera/issues/538)):

| Stage | Pass | Annotated | Categories |
|-------|-----:|----------:|------------|
| **Parse** | 92 | 96 | FRAGMENT (83), FUTURE (13) |
| **Type-check** | 86 | 6 | INCOMPLETE (5), ILLUSTRATIVE (1) |
| **Verify** | 85 | 1 | ILLUSTRATIVE (1) |

Annotations travel with their fence through spec edits, so there are no line numbers to maintain (no line-number-keyed allowlist to maintain — [#538](https://github.com/aallan/vera/issues/538)/[#606](https://github.com/aallan/vera/issues/606)). Stale-detection is built in: the gate still runs the exempted stage, and an annotated block that passes it fails the gate until the annotation is removed — when a feature lands, the skip surface shrinks. The INCOMPLETE check entries reference functions or types not defined in the block (e.g. `is_sorted` in a data invariant); the ILLUSTRATIVE entries demonstrate syntax with contracts that are intentionally imprecise. The same annotation mechanism (parse stage only) covers SKILL.md, FAQ.md, README.md, and EXAMPLES.md; `check_html_examples.py` reads it from HTML comments before `<pre>` blocks in docs/index.html. `build_site.py` strips the annotations from generated site assets.

## JSON Output Stability

`vera check --json`, `vera verify --json`, and `vera test --json` emit structured JSON for downstream tooling (CI pipelines, IDE plugins, agent feedback loops).  The field set is a public API — see [`spec/00-introduction.md` §0.5.8](../spec/00-introduction.md#058-machine-readable-output---json) for the stability rules.  Tests in `tests/test_cli.py` assert on the documented field set, so a regression that drops a documented field will fail at least one test.

### `vera check --json` / `vera verify --json`

Top-level:

| Field | Type | Description |
|---|---|---|
| `ok` | bool | `true` iff the file passed all checks at the requested stage; the canonical exit-code signal |
| `file` | string | The source file checked (echoes the path argument) |
| `diagnostics` | array | List of error-severity `Diagnostic` objects (see below) |
| `warnings` | array | List of warning-severity `Diagnostic` objects |
| `verification` | object | Only on `vera verify --json` — counts of `tier1_verified`, `tier3_runtime`, `total` |
| `slot_environments` | array | Only when `--explain-slots` is passed — per-function slot tables |

`Diagnostic` shape: `severity`, `description`, `location`, `source_line`, `rationale`, `fix`, `spec_ref`, `error_code` (the `error_code` set is documented in `vera/errors.py::ERROR_CODES`).

### `vera test --json`

Top-level:

| Field | Type | Description |
|---|---|---|
| `ok` | bool | `true` iff `summary.failed == 0` and no verifier errors; the canonical exit-code signal |
| `file` | string | The source file tested |
| `functions` | array | Per-function `FunctionTestResult`: `name`, `category` (one of `"verified"`, `"tested"`, `"failed"`, `"skipped"`), `reason`, `trials_run`, `trials_passed`, `trials_failed`, `failures` |
| `summary` | object | Aggregate counts (see below) |
| `diagnostics` | array | Verifier-error diagnostics that fed into `"failed"` classifications |

`summary` field set:

| Field | Description |
|---|---|
| `verified` | Functions classified Tier 1 (proved by Z3) |
| `tested` | Functions exercised with Z3-generated inputs |
| `passed` | Subset of `tested` where all trials passed |
| `failed` | Verifier-refuted OR Tier-3-tested-with-trial-failures |
| `skipped` | Functions whose inputs can't be Z3-generated (e.g. ADT params) |
| `total_trials` | Sum of trials run across all tested functions |
| `total_passes` | Sum of passing trials |
| `total_failures` | Sum of failing trials |
| `unlisted_errors` | Verifier-error diagnostics whose attributable function isn't in the displayed `functions` list (`--fn` filtering, private helpers).  Added in v0.0.156. |

### Stability contract

Per `spec/00-introduction.md` §0.5.8: fields MAY be added (consumers MUST tolerate unknowns), fields MUST NOT be removed or renamed without a major version bump, and field semantics MUST NOT change.  `ok` is the canonical gate; downstream CI SHOULD read it rather than parse field-by-field.

## Pre-commit Hooks

Every push is checked by 32 configured hooks across two stages: 30 are configured at the commit stage (after `pre-commit install`), and 2 (`check-changelog-updated`, `uv-lock-check`) are configured at the push stage (after `pre-commit install --hook-type pre-push`). Many commit-stage hooks use per-hook `files:` / `types:` filters and only fire when matching files are staged — a docs-only commit triggers a small subset, a compiler-level commit triggers most. Full list:

| Hook | What it does |
|------|-------------|
| `trailing-whitespace` | Strip trailing whitespace |
| `end-of-file-fixer` | Ensure files end with a newline |
| `check-yaml` | Validate YAML syntax |
| `check-toml` | Validate TOML syntax |
| `check-merge-conflict` | Detect conflict markers |
| `check-added-large-files` | Reject files >500 KB |
| `debug-statements` | Detect `pdb`/`ipdb` imports |
| `ruff check .` | Lint Python with ruff (default `F` + `E` rules) |
| `mypy vera/` | Type-check compiler in strict mode |
| `pytest tests/ -q` | Run full test suite |
| `check_conformance.py` | All 179 conformance entries hold at their declared level — positives pass; negatives fail `check` with their `expected_error` E-code |
| `check_examples.py` | All 42 examples pass `vera check` + `vera verify` |
| `check_corpus_canonical.py` | All 227 `examples/` + `tests/conformance/` programs (recursive) are in canonical form (`vera fmt`) |
| `check_examples_readme.py` | `vera run` commands in `examples/README.md` reference existing files and exported functions |
| `check_readme_examples.py` | README code blocks parse correctly |
| `check_examples_doc.py` | EXAMPLES.md code blocks parse correctly |
| `check_skill_examples.py` | SKILL.md code blocks parse correctly |
| `check_faq_examples.py` | FAQ.md code blocks parse correctly |
| `check_pypi_readme_examples.py` | PYPI_README.md code blocks parse, check, and verify |
| `check_html_examples.py` | HTML landing page code blocks pass parse + check + verify |
| `check_doc_builtin_shadowing.py` | No doc example defines a function named after an opaque built-in (would fail `vera check` with E151); `spec/09` signature reference exempt ([#819](https://github.com/aallan/vera/issues/819)) |
| `check_e602_clean.py` | No unexpected `[E602]` (body unsupported) / `[E604]` (param unsupported) silent skips outside the explicit allowlist (Layer 1 of [#626](https://github.com/aallan/vera/issues/626)) |
| `check_doc_counts.py` | Counts in docs match live codebase |
| `check_walker_coverage.py` | Every walker function covers every `Expr` subclass via dispatch or checklist comment (#597) |
| `check_diagnostic_fields.py` | Every diagnostic in `vera/` carries rationale + spec_ref, and errors also a `fix` (warnings exempt); every present spec_ref resolves to a real spec section; every literal `error_code` is registered in `ERROR_CODES` (#828); `# diag-fields-exempt: <reason>` waives missing/unresolvable fields only — never a wrong-but-resolving spec_ref or an unregistered error_code (#682, #955) |
| `explicit-encoding` | Every text-mode `open()` / `read_text()` / `write_text()`, `subprocess.run/Popen/check_output` text capture, and text-mode `tempfile.NamedTemporaryFile` passes `encoding="utf-8"` (#645) |
| `check_limitations_sync.py` | Limitation tables consistent across KNOWN_ISSUES.md, vera/README.md, spec chapters, SKILL.md, and LSP_SERVER.md |
| `check_licenses.py` | All package licenses are MIT-compatible |
| `build_site.py` | Regenerate AI-readable site assets (llms.txt, llms-full.txt, robots.txt, sitemap.xml, index.md) |
| `browser parity` | Browser runtime produces identical output to Python runtime |
| `check-changelog-updated` (pre-push) | CHANGELOG has a new entry when substantive files changed |
| `uv-lock-check` (pre-push) | `uv.lock` is in sync with `pyproject.toml` |

The validation hooks are smart about triggers -- they only run when relevant files change (`.vera`, `vera/**/*.py`, `grammar.lark`, the corresponding Markdown file, or `vera/browser/*` for browser parity). The two pre-push hooks only fire at push time.

## Scheduled limitations sync

`.github/workflows/limitations-sync.yml` runs `check_limitations_sync.py --check-states` every Monday 07:00 UTC (and on demand via `workflow_dispatch`): every issue a KNOWN_ISSUES.md / vera/README.md / spec / SKILL.md / LSP_SERVER.md limitation row cites is queried against the tracker, and a closed issue still listed as a limitation fails the run — as does an issue whose state cannot be determined (gh auth failure / rate limit / timeout), which errors rather than passing vacuously (#852, #960).  Deliberately **not** a required merge check: issue state drifts independently of any PR, so it is a visibility signal — a cron failure files or updates a `limitations-drift`-labelled tracking issue, mirroring `nightly-stress.yml`'s failure routing.

## CI Pipeline

GitHub Actions ([`.github/workflows/ci.yml`](.github/workflows/ci.yml)) runs the following nine parallel jobs on every push and pull request to `main` (the test row is split into a baseline variant and a coverage-instrumented variant on the gating cell, sharing the same underlying job definition):

| Job | Matrix / Runner | What it checks |
|-----|----------------|---------------|
| **test** | Python 3.11, 3.12, 3.13 × ubuntu-latest, macos-15, macos-26, windows-latest, plus advisory ubuntu-24.04-arm × 3.12 (13 combos) | `pytest -v` passes on all combinations |
| **test** (coverage) | Python 3.12 x Ubuntu only | `pytest --cov=vera --cov-fail-under=80` |
| **typecheck** | Python 3.12 x Ubuntu | `mypy vera/` clean in strict mode |
| **lint** | Python 3.12 x Ubuntu | `check_changelog_updated.py`, `check_conformance.py`, `check_examples.py`, `check_corpus_canonical.py`, `check_examples_readme.py`, `check_version_sync.py`, `check_spec_examples.py`, `check_readme_examples.py`, `check_skill_examples.py`, `check_faq_examples.py`, `check_pypi_readme_examples.py`, `check_html_examples.py`, `check_e602_clean.py`, `check_doc_builtin_shadowing.py`, `check_diagnostic_fields.py`, `check_site_assets.py`, `check_licenses.py`, `check_doc_counts.py`, `check_limitations_sync.py`, `ruff check --select S vera/` (security rules) |
| **security** | Ubuntu | [Gitleaks](https://github.com/gitleaks/gitleaks-action) secret scanning on full history |
| **dependency-audit** | Python 3.12 x Ubuntu | `pip-audit --skip-editable --ignore-vuln CVE-2026-4539` — checks all installed packages against the OSV vulnerability database (skips the local editable `vera` package; `CVE-2026-4539` suppressed pending a pygments fix release) |
| **wheel-preflight** | Python 3.12 x Ubuntu | `python scripts/check_wheel_availability.py` — verifies every runtime dep has prebuilt wheels for every (platform, python-version) tuple documented in README §Supported platforms; structural backstop for #691-class install regressions |
| **sbom** | Python 3.12 x Ubuntu | `cyclonedx-py environment` — generates a [CycloneDX](https://cyclonedx.org) JSON SBOM of the full installed dependency tree and uploads it as a 90-day CI artifact |
| **browser-parity** | Python 3.12 + Node.js 22 x Ubuntu | `pytest tests/test_browser.py -v` — verifies JS runtime matches Python runtime; collects V8 coverage via `NODE_V8_COVERAGE` and uploads to Codecov |

The coverage threshold of **80%** is enforced in CI. Current coverage is **95% Python, 61% JavaScript (91% combined)** — matching the overview table above. JavaScript coverage for `vera/browser/runtime.mjs` is collected separately using V8's built-in coverage and uploaded to Codecov with the `javascript` flag, independently of the Python `pytest --cov` report.

Each job uses scoped permissions (`contents: read`; the security job additionally has `security-events: write`) and all checkout steps set `persist-credentials: false` to prevent the `GITHUB_TOKEN` from being baked into `.git/config`. Actions without SHA-pinned version refs are tracked in [#390](https://github.com/aallan/vera/issues/390).

## Open CI/Tooling Issues

Tracked improvements to the testing and CI infrastructure:

| Issue | Description |
|-------|-------------|
| [#349](https://github.com/aallan/vera/issues/349) | Improve browser runtime (`runtime.mjs`) test coverage to >80% — JS code is invisible to pytest-cov, blocking codecov/patch on PRs that touch the runtime |

## Opportunities

Testing infrastructure that could be added in the future:

- **Property-based testing** -- `hypothesis` is installed as a dev dependency but not yet used. Could generate random programs to test parser robustness and formatter idempotency at scale.
- **Formatter round-trip invariant** -- verify `parse(format(parse(src))) == parse(src)` for all valid programs, not just the examples.
- **WASM inference.py coverage** -- `wasm/inference.py` at 80% has the most remaining gaps, mostly in deep type-dispatch branches for specific builtin function return types. These branches require very specific expression nesting patterns to reach.
- **Performance benchmarks** -- no benchmark infrastructure exists. Could track compilation time and Z3 verification time across releases.
