# Testing

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

## Overview

| Metric | Value |
|--------|-------|
| **Tests** | 12,290 across 181 files (~157,000 lines of test code; 12,091 passed + 26 stress-deselected, 173 skipped) |
| **Compiler code coverage** | 95% Python, 87% JavaScript (CI minimum: 80%) |
| **Conformance programs** | 244 programs across 9 spec chapters, validating every language feature |
| **Example programs** | 43, 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** | 3 Vera blocks in FAQ.md (2 validated, 1 annotated snippet) |
| **HTML code blocks** | 5 Vera blocks in docs/index.html (5 validated: parse + check + verify) |
| **Contract verification** | 411 of 533 obligations (77.1%) across the 43 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

# Host-binding diagnostic (re-raises a host callback's own exception, see ENVIRONMENT.md).
# The suite sets and unsets VERA_DEBUG_HOST_ERRORS itself, so run it without a prefix:
pytest tests/test_runtime_traps.py::TestHostErrorDebugKnob1302 -v

# Type checking
mypy vera/                                           # strict mode

# Validation scripts
python scripts/check_conformance.py                  # conformance suite (244 programs, see manifest.json)
python scripts/check_examples.py                     # 43 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` | 171 | 1370 | Grammar rules, operator precedence, parse errors |
| `test_ast.py` | 138 | 1,145 | AST transformation, node structure, serialisation, string escape sequences, ability declarations |
| `test_checker_types.py` | 249 | 3,830 | 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_slot_naming.py` | 56 | 810 | The rule table for `vera/naming.py`, the ONE slot/family naming renderer (#1208/#1209): each clause of THE RULE pinned to an exact rendered string — syntactic (alias-opaque) head vs fully-resolved type arguments, refinement at top level (base) vs argument position (the elided `{@Int \| ...}` form) with alias parameters substituted BEFORE the refinement branch, `Fn` at top level vs the full `fn(...) effects(...)` spelling with a SORTED effect row in argument position, the total `?` paths (arity mismatch, `Decimal` with arguments, a removed alias, an unresolvable type expression), type parameters shadowing same-named aliases, declaration-order alias visibility (a cycle and a forward reference terminate on the checker's opaque placeholder; a 40-deep in-order chain resolves, and a 400-hop chain — bare names and composites alike — resolves without a per-hop frame; a 300-level alias graph whose bodies mention SIBLINGS as well as ancestors resolves too, and at 1000 levels the resolver is instrumented to prove its nesting is CONSTANT rather than merely under this machine's recursion limit), slot-reference keys matching the binding side, `family_name` collapsing scalar / composite / parameterised-composite aliases and its fallbacks, `family_base_name` (identity vs representation, #1218), the refinement-binder derivation (including its deliberately syntactic argument naming), a declared ADT outranking the `Decimal` and removed-alias branches (a user `data Float` / `data Decimal` renders as itself and keeps its type arguments) while an alias still outranks a same-named ADT, ADT visibility bounded by declaration index in BOTH directions (an ADT declared below the alias body that names it is invisible to it, above it is not — and the bound stops at the alias body, so a top-level slot names the ADT whatever the order), and the env builder |
| `test_slot_naming_differential.py` | 6 | 912 | The load-bearing proof behind `vera/naming.py` (#1208/#1209): the checker's two naming entry points (`_type_expr_to_slot_name` and `_slot_type_name`, the latter also carrying every `_slot_ref_key` reference) are instrumented to record a (reference, module) rendering pair on EVERY call, and the whole `.vera` corpus (examples, conformance programs and their module fixtures, the PR #1202 probe corpus) plus a 31-program inline battery aimed at the alias / refinement / function-type / shadowing / declared-ADT corners (four of them carrying their own preludes, because the declaration-ORDER corner is about where the `data` sits relative to the `type`) is swept for ZERO divergence.  The checker DELEGATES its naming, so the module side is what the checker returns and the reference side is a test-local statement of the rule (syntactic head, arguments through the checker's own `_resolve_type`, joined by `canonical_type_name`, plus the refined-top recursion) — independent by design, so a future edit to the module has to disagree with a written-down rule rather than re-baseline both sides at once.  It is also what pins the join: `vera/naming.py` renders each argument through `type_arg_name` and restates only the `Head<a, b>` bracketing, and this side calls `canonical_type_name` itself.  Check failures still contribute observations (naming runs while diagnostics accumulate); only parse failures are skipped, and counted.  Self-protecting: floors on total observations, observations under a non-empty alias env, and — counted over the CORPUS alone, so battery growth cannot mask corpus decay — both the number of `.vera` files swept and the arguments naming an alias pre-resolution; a battery reach test that names the exact string each corner must render, so an entry contributing nothing fails instead of reading as agreement; a `VeraError`-only absorption around the check, so a compiler-level raise propagates rather than silently emptying an entry; and a live proof the gate can go red (perturb the module renderer, assert the harness reports it and that the reference side stands still) |
| `test_slot_naming_blast_radius.py` | 15 | 337 | The MEASURED radius of the #1208 core flip: every subsystem downstream of the checker (the monomorphizer, codegen, the verifier, the SMT layer) derives slot names AND slot-reference keys from `vera/naming.py`, and the radius is measured over the whole `.vera` corpus (`check --json` diagnostics for every file, `run` for every probe).  Six shapes differ, all one class: a program that died on a dangling-slot `[E699]` now resolves and runs with the value the CHECKER's binding rule gives — each pinned by path and entry point with its expected value, so a regression that re-splits the naming names the program rather than failing diffusely.  The six live in `tests/conformance/`, which is where the assertions read them.  No `check` diagnostic moved anywhere (the checker was already delegating), and five slot-heavy sentinels outside the radius are asserted still clean.  Also pins the two things the corpus cannot show: `--explain-slots` reporting the merged parameter stack under the checker's own name, and the module-scope rule — an imported generic's clone has its De Bruijn recount rendered in the DEFINING module's alias namespace (§8.4.1), not the importer's, or the merge goes unseen and the clone silently resolves onto the wrong parameter |
| `test_family_naming.py` | 66 | 1,583 | The State/Exn cell FAMILY is the cell the CHECKER typed (#1209): the checker resolves an effect instance's type arguments in full, so `State<MaybeInt>` under `type MaybeInt = Option<Int>` and `State<Option<Int>>` are ONE instance, and the family is named from the resolution rather than from the source spelling — a spelling-keyed family mints two host cells behind a green check for anything that does not resolve to a scalar.  Pins the collapse where it is OBSERVABLE (a mixed-spelling program returns the shared cell's 7, not the split cell's -1 — bare alias, parameterised alias, and an `Exn<Msg>`/`type Msg = String` payload whose `i32_pair` (ptr, len) has to arrive through the SAME tag), the import surface collapsing with it (one `state_get_` import, not two), the same collapse across a MODULE boundary (each side resolving in its own alias namespace), the negative (`Option<Int>` and `Option<Bool>` stay two cells, and the outer cell keeps its value — a renderer that dropped type arguments passes every positive and fails here), the resolved function-carrying family (#1219 — `State<Handler>` under `type Handler = Option<fn(Int -> Int) effects(pure)>` takes its resolution's name, and the alias and the resolution share one cell, proved by the value), the surviving bare-function-type fallback (the residue, refused downstream so the split is free), the refined cell's own family (#1218 — nested `Pos`/`Neg` route to their own cells, and a refined cell keeps its base's write guards and pair-ness), the linear-in-the-predicate symbol length with its `MAX_CELL_FAMILY_SYMBOL` backstop refused loudly on both targets, and the two formatter-coverage gates behind the predicate renderer, byte-stable family symbols for seven alias-free corpus programs (the emitted names are ABI), and the whole measured radius: the six shapes the flip moved (now in `tests/conformance/`), each at the symbols AND the value it renders to |
| `test_naming_env_provenance_1208.py` | 45 | 2,097 | The other half of the #1208 contract: every consumer is handed the ENVIRONMENT the checker rendered under, not just the same renderer.  Four provenance seams, each pinned by the adversarial probe that exhibited it — an IMPORTED callee's contract rendered in its DEFINING module's alias namespace (a violated precondition that vanished, and its mirror, a correct call spuriously rejected, both under a `Cnt` that names different bodies on the two sides), an imported GENERIC monomorphized and verified in that same namespace (a lying postcondition that proved clean, plus a verifier↔codegen clone differential over the recounted slot references — the desync is invisible to a unit test on either side), a `forall` variable shadowing a same-named module alias wherever a generic signature renders (the mono clone, a body `let`, the verifier's collapsed premises, and the exported uninstantiated template), and the tester's `SmtContext` holding the narrowed scope its own names were keyed in — the last one behavioural, since a generator handed the wrong scope collapses two parameters onto one variable and returns NO inputs at all.  Three of the seams are also crossed against a SECOND component rather than checked for internal consistency, because a wrong-but-consistent scope is invisible from inside one: the verifier's declared parameter names against `slots.slot_table`'s, its `where`-helper scope against `slots.fn_scopes`' accumulation, and the monomorphizer's post-substitution names against what the consumers rebuild on the clone — each independent on the axis under test (which variables the two sides narrow by) but sharing `fn_slot_scope`/`slot_name` below it, so the hand-derived literal rendering beside every comparison is what a shared-renderer defect cannot satisfy.  An imported generic nested under a non-generic function is pinned too — both its discovery-time recount and its verification-time clone must run in the DEFINING module's namespace.  Three more seams arrived from the PR #1224 review, each with the false Tier-1 or miscompile that exhibited it: an UNPINNED callee (an imported generic's own `where`-helper, which the origin registry never pins) rendering in the module under verification rather than the entry program, whose absence let a violated precondition discharge as true and trap at run time; a callee's refined-RETURN predicate translated in the callee's namespace alongside its `requires`/`ensures`, pinned by provenance because today's bare-headed binder masks it behaviourally; and codegen's declaration-index space keyed PER NAMESPACE, without which a module's stamp turned the main file's forward alias reference into a backward one and a check-clean, verify-clean program read the wrong parameter through valid WASM.  Two seams from the #1213 burndown close the same shape from the other side: the prelude's own aliases are injected only into the reserved `Vera` namespace, so no name a program can spell resolves on the codegen side alone (#1221 — the differential compares the checker's and codegen's partition of one signature, with the emitted WAT beside it), and an imported ADT is ordered at the index its OWN module gave it rather than the built-in floor (#1227), each with the control that differs by exactly the namespace under test.  Controls carried alongside: the same programs with the alias renamed or the shadowing declaration removed, and the runtime oracle that shows the new E500/E501 agrees with the emitted code rather than merely reporting more |
| `test_callee_contract_scope_1220_1225_1226.py` | 40 | 1,433 | A callee's contract is READ in the callee's own module.  Three burndown defects, each asserted against the runtime oracle wherever the two directions of a wrong namespace (an obligation that vanishes, one that fires for no reason) look identical from inside the verifier: an E501's `Precondition:` line quoted from the file that DECLARED the clause (#1220 — in the misattribution direction too, both files carrying a plausible `requires` on the same line number, plus the imported-generic `where`-helper whose clause sits past the end of a short importer and used to quote nothing at all); a bare-name call inside an IMPORTED callee's contract resolved through the CALLEE's module registry (#1225 — the false Tier-1 whose run traps and its mirror spurious E501, through the `requires` and the `ensures` path, against a no-collision control); and the refined-RETURN binder derived through the naming layer, so a refinement over a PARAMETERISED base pushes the key its own predicate looks itself up under (#1226 — single-module and cross-module, the second proving the derivation happens INSIDE the callee scope); plus the PR #1239 review round — a module's pinned registry holds what its OWN file imports (a DEPTH-2 chain, the shape the single-level corpus could not exhibit: requires and ensures directions, bare-vs-qualified tier agreement, a name outside the middle module's import filter still missing per §8.5.1, and the mirror gate that filling the registry does not re-export), and every part of a diagnostic follows the declaring module (location, file name and excerpt, including a clause past a shorter importer's end, with a multi-line clause quoted whole), and the characterization of the binder-reference walk's one documented exception — a CLOSURE inside a predicate owns the first `@T.n` in traversal order, whose consequence is a Tier-3 demotion rather than a fact assumed about the wrong term; and the mini-review round — an obligation carries the FILE its line number belongs to, so the documented `(file, line, column)` join between the two `--json` arrays holds for a module-located obligation, with the entry-file control and warm==cold parity, and a multi-line clause is quoted with its `--` comments blanked (a `--` inside a string literal surviving, which a naive split would corrupt) |
| `test_alias_application_refinement_base_1237.py` | 11 | 398 | A parameterised alias APPLICATION substitutes its arguments in the verifier's own resolver (#1237).  `type Box<T> = T;` applied as `@Box<Cnt>` resolved to `AdtType('T')` — the alias's binder leaking as an ADT name — so a refinement over it failed the modelled-primitive gate, the refined-return fact was dropped, and a valid program was rejected with a spurious E501 while `vera run` returned the right answer.  Both halves of the fix are asserted separately: the alias body registers its own parameters as type variables (`substitute` maps type variables, so an ADT-named binder is unsubstitutable however the application side is written) and the application substitutes.  Plus depth (an argument that is itself an application, and an alias whose body applies another alias), the bounded direction (a consumer wanting `>= 100` where the refinement grants `>= 18` is still rejected, and the runtime agrees), and the gate that must NOT move — an unmodelled `@Byte` base resolves correctly and still degrades to a Tier-3 runtime check, with a consumer of its predicate still refused |
| `test_exn_throw_payload_1268.py` | 42 | 1056 | `throw`'s payload is obligated AND runtime-guarded like every other narrowing site (#1268).  `throw(0 - 5)` under `effects(<Exn<Nat>>)` verified at 4/4 Tier 1 with ZERO obligations while `vera run` returned -5 out of the `@Nat` payload — check-green, verify-green, silently wrong — because `throw` is a bare call with no function-registry entry, so the argument loop never saw it and the table-driven fallback added for the same hole at the State `put` was keyed on that one name.  All three arms are asserted (the `@Nat` refutation, the refined refutation over a modelled base, and the `@Nat`->`@Int` widening obligation appearing where none existed), plus the #1251(b) concrete gate reaching the payload for free (`throw(200)` into an `Exn<{ @Byte \| @Byte.0 < 10 }>` names the value; the satisfying twin proves at Tier 1), the user-effect contrast that localized the bug (a declared op's argument was loud for the same value — both are loud now, at the same site name), and the refined-alias payload spelling.  The GUARD is checked against codegen rather than asserted: an undischargeable payload must land on the runtime-guarded `tier3` leg, counted in the totals, and a run must confirm the payload really is stopped — the two together go red whichever side moves without the other (delete the emission and the runs go red; flip the flag back and the statuses do).  Both arms are run at the boundary: a `@Nat` payload traps on -5 and delivers 5, a refined `{ @Int \| @Int.0 > 0 }` payload traps through the `$vera.contract_fail` channel on BOTH -5 and 0 — the value that clears the base's `>= 0` and violates the predicate, so a sign guard standing in for the predicate guard fails here — and delivers 7.  The type gate carries its own over-refusal control: an `Exn<Int>` payload has no invariant to violate, so a negative one is a correct program and must still return -5.  Both REPRESENTATIONS are covered — a scalar payload in one local, and a `@String`-based one whose (ptr, len) pair has to be saved in two, checked over the ptr and put back in the right order (the satisfying twin is what shows the order).  The **soundness differential** is the point of the guard rather than a property of it: the clause parameter's type is what the verifier hands every downstream consumer, so a consumer discharging `ensures(@Bool.result)` at Tier 1 from its `@Nat` parameter alone is asserted PROVED and then run — pre-fix the run reported a postcondition violation on that proved postcondition, with nothing else in the path (the argument is already `@Nat`-typed, so no call-site narrowing guard fires).  A dischargeable twin proves the site is not merely always-loud, and the six `Exn` conformance programs are verified whole as canaries so obligating a position that had none names itself instead of arriving as one line of a corpus sweep.  The adversarial round adds the three places the `guarded` PROMISE and the emitted guard could disagree in a direction no value oracle can see, because the program either never runs or runs identically either way: a refinement OVER a refinement is asserted `tier3_unguarded` AND `E618`-refused at compile in one cell (the mirror claimed a runtime check for a program that cannot be compiled at all — either half alone reads as consistent); the bare and qualified spellings of one operation are asserted to record IDENTICAL statuses as a differential rather than two literals, on both arms, with the run confirming which value is the true one (`Exn.throw` was disclosed unguarded while codegen delegated it to the guard-emitting dispatcher, and `State.put` had been since #1203); the #820 INTERSECTION at this boundary — a refinement over `@Int` keeps the widening obligation AND its guard beside the predicate's, pinned as a differential against the unrefined spelling (both must trap at u64.MAX, where the refined one used to return -1) with an in-range control so the guard is not simply always-on; and `E504`'s rationale is read from a real diagnostic — reached through the site that IS still unguarded, a user-declared effect's operation argument — to pin that it no longer lists the `throw` payload among the sites with no runtime guard |
| `test_refinement_binder_convergence_1208.py` | 16 | 459 | Codegen's refinement boundary guard and `vera/naming.py` derive the predicate binder ONCE (#1208).  A per-shape differential over a direct refinement, an alias hop, `@Nat`- and `@Byte`-based refinements (both range-conjoining), a composite base whose binder is a RESOLVED argument list, and two non-refinements that must be `None` on both sides — plus the property the convergence exists to hold, that the guard's binder equals the key a predicate's own `@Base.n` resolves to.  A per-shape differential is green either way while two copies agree — which is exactly how a duplicated derivation drifts unnoticed — so the load-bearing assertion is a MUTATION: perturb `naming.refinement_binder_parts` and codegen's guard must report the perturbed binder.  Codegen's two layered WASM decisions are pinned alongside — the loud E618 for a nested refinement base, reported ONCE per declaration however many call sites consult the derivation and however many clones a generic is instantiated into (two genuinely distinct sites still report twice), and no guard at all for an erased one (parametrized over `@Unit` and `Future<Unit>`, the corner that erases identically but is not spelled `Unit`) — plus runtime traps proving BOTH the `@Byte` and the `@Nat` range conjunctions reach the emitted check, each pinned by trap `kind` as well as by the conjunct its message names.  The mutation perturbs the predicate as well as the binder name: the two travel by different routes, and the range conjunction lives on the predicate.  The once-per-site dedup is keyed on a resolved location, so a cross-module pin holds up the premise that a location carries its owning file: two imported library modules of identical shape, declaring their nested refinement at the same line and column, must produce two diagnostics attributed to two files — each quoting its own module's declaration, which is also what catches an attribution pointing past the importer's last line |
| `test_checker_effects.py` | 90 | 1,465 | 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_state_exn_registration.py` | 30 | 1,298 | #1210 — State/Exn host-import registration covers the whole handler, not just its body.  Four shapes, one per sub-expression position the walk used to miss (a nested handler in a clause body, in the state-init expression, in a clause's `with` update, and an `Exn` handler in a clause body), each check-green and verify-clean and therefore required to COMPILE — pre-fix every one died at whole-module WAT compilation with `unknown func` / `unknown tag`; plus the `i32_pair` cell (`handle[State<String>]` in a `pure` function) that the walk skipped in silence, now the same loud E607 the declared-effect gate emits.  The **registration-completeness differential** is the cross-component invariant itself: over every `examples/` + `tests/conformance/` program that compiles, every `state_*` / `exn_*` symbol the emitted WAT REFERENCES must have a matching import or tag DECLARATION — a desync between the registration pass and the lowering pass is invisible to a unit test on either.  Round two adds the Exn twin of the silent skip (`handle[Exn<Unit>]` in a `pure` function — the walk called the shared tag registration and discarded the verdict, so it compiled where the declared-row spelling was a clean E612) and the four CONTRACT positions, which are lowered code: a handler in a `requires`, an `ensures`, an `assert`, or a `decreases` measure.  The differential gained a **validation leg** — every HANDLER-BEARING module is handed to `wasmtime.Module` through the exceptions-enabled engine `execute()` uses, because a symbol declared at the WRONG TYPE passes the name comparison while being invalid WASM, and 10 of the 30 handler-bearing modules fail to load with `wasm_exceptions` off — a supported wasmtime configuration, though the current runner defaults it on.  The conformance suite's deliberate negatives are filtered out of the sweep: they never reach codegen through `vera check`.  Carries floors on programs swept, modules validated, summed symbol references and globally distinct symbols, plus three can-go-red tests: the State and Exn extractions each stripped of their declaration lines, and a planted retyped import that only the validation leg catches.  Round five adds the three positions no corpus program contained — a destructuring `let`'s value (which also disarmed the E612 gate), a module call's ARGUMENTS, and a signature refinement predicate reached through the alias table — and a cross-module shape test for the module-call leg.  Round seven adds the boundary-guard routes that enumeration missed (a tuple parameter's components, a tuple return's, and a closure's refined formal and return) and the co-extensiveness half those shapes cannot show: a refined tuple behind a CLOSURE formal must declare nothing, since the closure path emits no component guards, and the nested-refinement (E618) and erased-base bails must stay silent registrars too.  Plus the cycle guard on the closure signature leg, asserted in both directions — the walk terminates, and with the guard neutered the same walk blows the recursion limit |
| `test_closure_lift_boundaries_1234_1235_1245.py` | 18 | 757 | Closure lifting at refinement boundaries — three burndown defects of one seam.  **#1245**: `_lift_pending_closures` ran BEFORE `_compile_postconditions`, so a closure created while lowering a refined-RETURN guard, a tuple return's component guards, or an `ensures(...)` predicate was registered and never lifted — the table stayed empty, its `call_indirect` was orphaned, and the #1185 propagation dropped the function and every caller: a check-green, verify-clean program compiling to ZERO exports.  The param-position twin (lowered before the lift, so it always worked) is carried as the control that makes it an ORDERING defect, the `ensures`-clause twin shows the same bug with no refinement in sight, and a violating return asserts the lifted guard ENFORCES rather than merely existing.  **#1234**: the lift worklist fed itself — a refinement whose predicate holds a closure refined by a type whose chain leads back to it (`type SelfRef = { @Int \| ... fn(@SelfRef -> @Int) ... }`, and equally a mutual `A -> B -> A` or a three-type cycle) had each lift's own boundary guard queue an `AnonFn` for ever, and `vera compile` never returned.  All three cycle lengths are asserted on a daemon thread with a wall-clock budget, so a regression fails fast instead of hanging the suite, and each on the [E602] naming the closure it refused (a guard that never fired cannot produce it).  Two controls carry the other half — the guard is keyed on the lift CHAIN, not on everything already lifted, so `fn f(@R, @R -> @Int)` and a diamond, which each legitimately lift one predicate's closure twice, must still run; mutation-measured, they are the only two tests a seen-set spelling reddens.  **#1235**: a `Tuple<PosInt, Int>` formal crossing into a closure was unguarded where the named path traps — both spellings of the same boundary are run against each other, violating and passing |
| `test_byte_literal_joins_1212.py` | 25 | 759 | #1212 — a `@Byte` literal inside a value-position join lowers at the i32 Byte width.  `@Byte` is i32 (spec §11) while an int literal defaults to `i64.const`, and the #865 / #1092 coercions each tested for a TOP-LEVEL `IntLit` — which the checker's bidirectional coercion is equally happy to type inside an `if` or `match` branch.  Ten write boundaries are parametrized with the literal in a branch (`let`, handler state-init, clause-dispatched `put`, bare `put`, get-clause `resume` — verbatim the form the E602 clause-lowerability skip message recommends — a clause `with` update, a `@Byte` call argument, a generic constructor field at `Box<Byte>`, a lifted closure's own RETURN whose named twin had been coerced since #865 while the closure path had no such step, and a HETEROGENEOUS join at a `@Byte` return, where the arm the result-type decider reads is already i32 and a sibling is a bare literal — arm ORDER decided which way that one failed, so both orders and both paths are pinned).  The module docstring states what that list is and is not: measured coverage, since the checker's single Byte coercion makes the true enumeration "every position propagating a Byte expectation", which nothing enumerates in one place, each a check-green program that failed WASM validation with `type mismatch: expected i32, found i64` before the fix.  Every case carries a VALUE oracle (200, distinguishable from every other constant in its fixture) rather than merely asserting the module runs, and a separate test drives the OTHER branch so a fix that marked only the arm the result type is read off would still fail.  The controls are the load-bearing half: a plain `@Int` join must stay i64 — pinned on 5,000,000,000, which an i32 store cannot represent, so a spreading mark is a wrong VALUE and not just a validation failure — a Byte join with no literal arm must be untouched, and a Byte-RETURNING literal join must keep its own #865 return coercion.  The constructor-field case runs through the real pipeline (checker artifacts threaded), because the #1092 width keys on the checker-recorded target type |
| `test_closure_boundary_widths_1255_1256_1269.py` | 52 | 973 | Widths and pointer-ness at a closure or effect boundary — three burndown defects of one seam, each a boundary answering "what is this declared type" from something other than that type.  **#1255**: GC pointer-ness was read off the SYNTACTIC head, so `type SmallByte = { @Byte \| ... }` was rooted on the shadow stack at the closure parameter, return and capture and at the two named-function twins.  The oracle is a DIFFERENTIAL against the `@Byte` spelling of the same program rather than an absolute push count — these bodies must allocate or no prologue is emitted at all, so they legitimately root their own intermediates — with the base spelling's own count PINNED beside it, because equality alone also holds when both spellings root the scalar, which is the pre-fix state and what a mutation deleting the exclusion outright would produce.  A genuine pointer at each of the four boundaries is the control (rooting nothing anywhere satisfies the differential too), and every shape runs under `VERA_EAGER_GC=1` — a collection at each `$alloc`, where removing a load-bearing push reads back as a wrong value rather than as a passing test.  The heap-layout invariant the defect was inert behind is executable here: a module with no string pool at all — the exposure the issue named — still starts its heap above the inline scalar range, and shrinking the two constants that create that margin fires the build guard.  **#1256**: the `apply_fn` `call_indirect` signature took each parameter's width from the ARGUMENT, so a `@Byte` formal fed a literal registered two incompatible `$closure_sig` types and trapped; asserted by run AND by the emitted signature list, since a value oracle alone would also pass if both sides converged on the wrong shared width.  The join spelling, the refined formal, the function-type-alias arm of the formal recovery, a directly-called named twin and an i64 control (pinned above 2^32, which an i32 parameter cannot carry) surround it.  **#1269**: `throw`'s payload was not a `@Byte` write boundary, so `throw(5)` into `Exn<{ @Byte \| @Byte.0 < 10 }>` put an `i64.const` under an i32 tag and failed WASM validation at load.  Both halves of the width agreement are pinned — a fix that widened the TAG would also run, and would put a Byte cell at eight bytes everywhere else — across the bare, aliased, refined, branch-literal, qualified-`Exn.throw` and thrown-inside-the-handled-body spellings, the last two reaching registration paths the others do not |
| `test_nested_handler_clause_ops.py` | 27 | 971 | #1211 — a handler clause body's bare `get`/`put` belongs to the handler's DECLARATION scope, not to the body it refines.  Eight nested shapes, each asserted on all three components (checker accepts, verifier discharges clean, compiled program returns the checker-derived value): `put` in a put clause and in a get clause, a bare `get` in a `with` state-update expression, depth-3 nesting proving the IMMEDIATELY enclosing handler wins, the qualified `State.put` spelling, a nested handle expression inside a clause body (its registries must be restored to the declaration's, not the intervening handler's), and the two op-result-type mirrors — a bare `get(())` in match-scrutinee (`_effect_op_result_wt`) and array-element (`_effect_op_result_vera`) position, both of which emitted invalid WASM for a check-green program before the alignment.  Every oracle is derived from the checker's story, never from what codegen emits, and a meta-test asserts each shape still SEPARATES enclosing-cell from inner-cell routing (the pre-fix value is recorded per case) so none can go vacuous.  Round two adds the two dispositions of an EMPTY enclosing handler stack — the declared effect row (the only route that reads the restored `_effect_ops`, which every handler-enclosed case bypasses) and the outermost handler in a `pure` function (E122 at check) — the enclosing handler's own clause running on the outward-routed op (a transforming `with` one level out: 300100, where the intrinsic reading gives 300050), `IO.print` inside a clause body, the #1233 same-family refusals (nested handler, `with` expression, declared row) with their different-family control, and the outward-re-entry depth cap (below it, at it with a WAT-size bound, and past it as a loud E602) |
| `test_handler_op_ownership_1284.py` | 15 | 419 | #1284 — whose declaration a bare `get`/`put` call site denotes.  The checker resolves user-fn-first (pinned directly: an over-applied `get` under a `handle[State<Int>]` reports the USER signature's arity), and codegen used to answer that question twice more and differently — the declared-effect row withheld the op when a function owned the name, the handler expression overwrote unconditionally.  Four shapes from check-green source, each asserted on the CHECKER's value and on the dispatch target in the emitted WAT: a handled body returning the cell instead of the function's answer (silently 5 for 4), a `@Bool`-returning user `get` whose module WASM validation rejected, same-family nesting refused outright with a spurious `[E602]` naming a State operation the source never contained, and different-family nesting emitting the enclosing cell's getter at the wrong width.  A parametrized differential runs all five shapes (the four plus a user `put`) as one table with each case's pre-fix behaviour recorded, so a case that stops distinguishing the two answers is visible rather than vacuous; the controls — an unshadowed handler and an unshadowed declared row, both of which must still reach the intrinsics — are what a fix that simply stopped installing the ops would fail, and `new(State<Int>)` under a shadowed op name pins that the #1285 family registry composes with this |
| `test_new_state_family_1285.py` | 9 | 323 | #1285 — which cell `new(State<T>)` reads under a multi-`State` effect row.  `old()` has been family-keyed since #1205/#1209 while `new()` read the name-keyed op registry, so the two sides of one `ensures` clause read different cells: `effects(<State<Int>, State<Bool>>)` with `ensures(new(State<Bool>) == …)` was check-green and verify-green, put `state_get_Int`'s i64 into the Bool comparison's `i32.eq`, and died at load.  Three multi-row cases — the width-mismatched shape that could not load, an `Int`/`Nat` pair that loaded and answered about the wrong cell, and `old()` beside `new()` of one family, whose unchanged-cell claim the runtime refuted on a contract the verifier had discharged — plus the single-`State` and alias-spelled controls the whole existing corpus exercises.  Each cell is seeded from a caller's handler at a value the other cell is not holding, so a wrong-cell read cannot coincide with the right answer, and a deliberately false postcondition asserts the Tier 3 runtime check really traps, without which every "the program runs" assertion here would prove nothing |
| `test_adt_membership_scope_1253.py` | 5 | 334 | #1253 — a checker↔codegen DIFFERENTIAL over one module's slot table.  `_adt_layouts` is one map across every absorbed namespace, so a sibling module's ADTs were members of a module that never imported them while the checker kept the name opaque: `['Array<?>', 'Array<Int>']` against `['Array<Float>', 'Array<Int>']` for the same signature.  Each case renders the module's parameters through `vera.naming` twice — once against the environment the checker binds that module's declarations in (built by the production `_modules_visible_to` + `check_program` path, not a rebuild of it) and once against codegen's `_alias_env` inside `_module_alias_scope` — and asserts both the agreement and the checker's own value, so an alignment on the WRONG name still fails.  Three membership cases (an unimported public sibling, a private sibling, and the imported positive control that is green before and after — what separates scoping the membership from erasing cross-module ADTs) plus the entry program's own view, which must keep seeing the ADT it imports by name |
| `test_prelude_decl_stamp_1287.py` | 4 | 240 | #1287 — the prelude's declaration-index block is a fact about the prelude.  `_stamp_decl_order` guarded the PRELUDE write on `_decl_order`, the active (main-file) namespace, so a main-file `type Option = Int` — accepted under §8.4.1, and not a `data`, so it does not suppress the prelude's own `Option` — made the guard fire and left `Option` out of `_prelude_decl_order` entirely, with every later prelude declaration shifted one place earlier because the counter never advanced.  That map is the base layer under every module's index space (`{**prelude, **module_own}`), so the wrong index reached `AliasEnv.data_types` as `_BUILTIN_DECL_INDEX`.  Stated as an INVARIANCE — the same program with and without the shadowing alias must stamp an identical prelude block — plus the module-namespace index it feeds, and a control that the main file's own stamp still wins its own namespace (which a fix stamping `_decl_order` unconditionally would break) |
| `test_prelude_adt_namespace_1277.py` | 61 | 1034 | #1277 — one file's `data Json` must not evict the prelude's from another namespace, and a module declaration contending with a prelude one must be loud.  Three halves, pinned by disjoint cases so a regression in any is attributable.  **Acceptance battery**: all eight prelude ADT names × {module declares it alone, entry also uses the prelude's}, asserting that no cell reports `[E602]`/`[E620]` and that a cell which does not report `[E621]` emits every public function the entry declares — the silent-drop check, and the guard against the rail's original four-of-eight coverage returning (the layout harvest skips a built-in name, so a layout-keyed rail saw `data Json` and never `data Option`).  That battery accepts either answer per cell by design, so the §8.4.1 injection split is pinned separately: an entry that never names the type must still report `[E621]` for the four every program compiles (`Option`, `Result`, `Ordering`, `UrlParts`) and must stay clean for the four injected on demand, with a partition cell holding the two halves to the battery's own name list.  Plus two-declaring-module cells in both import orders — the entry's import order is derived from the parametrization, and the both-differ cell asserts the two reports arrive in that order, so the pair cannot quietly become one program compiled twice — covering restate+differ, both-differ, both-restate, and a non-prelude control that must stay E609's, because the rail asks every declarer and a first-wins lookup made it order-dependent.  Plus the restatement control for all eight: a module that restates the prelude's shape shares the one layout, compiles and runs, and must not be refused — measured legal at the branch point, and refused by the rail's first form for four of them.  **Rail detail**: severity, the module's own file and line, the description naming the type and the module, the empty exports, and `cmd_compile` returning 1 over a `cmd_check`-green program.  **Floor**: the checker registers the prelude ADTs in every `TypeEnv` unconditionally, so codegen's membership must too; asserted as a differential against the checker's own `data_types` in a module namespace, and on the entry namespace's member set for the issue's measured shape.  `prelude_adt_names()` is compared against `inject_prelude` itself, and `data_decl_shape` is pinned on the directions that matter — a renamed type parameter is the same layout, a reordered constructor is not, an alias-spelled restatement keys EQUAL to the prelude's, and a type parameter shadows an alias of its own name.  Each declaration is resolved through the aliases of the namespace it was written in, one side only: the two whole-program cells pin both directions of that — a module restating the prelude through `type Payload = String;` must compile, and a module hiding a mismatch behind `type Array<T> = Int;` must not |
| `test_import_visibility_entry_point_1244.py` | 6 | 269 | #1244 — `vera check` reports the same diagnostics whether it was given a module or a file that imports it.  Registration alone says what a module DECLARES; the importer never checked its bodies, so a name a module never imported was rejected standalone (E200, §8.5.1) and accepted in silence through an importer.  Written as EQUALITY between the two entry points rather than as "the importer warns", because the property is agreement — a future change making the standalone verdict lenient would satisfy a one-sided assertion and must fail here on the standalone leg.  Six cases: the leaked unimported name, the honest control that imports what it uses (green before and after, so the new body check is the visibility rule rather than a blanket rejection of cross-module programs), the issue's type-error-through-importer shape (an `@Int` call bound to a `@Bool` slot: check-clean, Tier-1, failing at compile), a diamond proving each module is reported ONCE (the body check is memoised by path across nested checkers), and both entry points into an import cycle proving the memo terminates it |
| `test_clone_body_declaring_module_1241_1243.py` | 5 | 344 | #1241 + #1243 — an imported generic's clone body resolves its bare calls in the DECLARING module, on both sides.  The verifier's lexical lookup fell through to the importer's registry (`_declaring_module_scope` swapped the naming env, source and file but not the function registry) and codegen's clone-emission door was the one door that did not thread the module's intra-rename map, so `glib`'s `gen` called the importer's `need`.  The two halves are one routing rule, and the tests are written so neither passes alone: each case asserts the `vera verify` verdict AND the `vera run` value together, so the verifier half alone (which makes verify clean while the compiled program still traps on the postcondition it just proved — the measured false Tier-1) fails the same test the codegen half alone (right value, verify still refusing) fails.  Every expected value comes from the module verified and run STANDALONE, never from what the importer produces.  Shapes: a private direct callee, a two-hop private chain, the type-discriminating pair (`@Int` vs `@Bool` — check-green source that emitted invalid WASM), and the unshadowed-callee control that was correct before and after, which is what pins the defect to the SHADOWED name rather than to cross-module calls in general |
| `test_module_generic_namespace_1274.py` | 24 | 1,015 | #1274 — a module generic that does not own the importer's bare name is reached under `mod$<path>$name`.  Pre-fix only PRIVATE module generics were routed that way (#1000), so a PUBLIC one collided with the importer's same-named generic in the clone-name space: both files' `gen2` mangled to one `gen2$Bool`, one overwrote the other, and the module's own body ran the importer's — a **false Tier-1** (`check`/`verify` clean, the module's proved `ensures` violated at run: 999 where the declaring module answers 111).  The full visibility matrix (module generic × importer generic), the import-filter dimension (out-of-filter, in-filter, wildcard), the unshadowed-out-of-filter cell that assembled to `unknown func $gen2`, and a type-discriminating shape whose two clones have different WAT result types.  Each cell asserts the verify VERDICT and the runtime VALUE together in one test — a clean verify beside a violated postcondition IS the bug, so splitting them across sibling tests would let it hide — against the standalone library as oracle, and re-checks that the importer's own generic still answers its own value.  The per-module both-sides differential lives in `test_monomorphize_differential.py`.  Two further families joined after the adversarial round: the module→module **hop** — a module's bare call to a DIFFERENT module's qualified-only generic, which the per-module classification never rerouted, in both a LOUD spelling (a contract pins the answer, so a captured call traps) and a SILENT one (every contract admits both answers, so only the value distinguishes them) plus the two-hop shape where the entry never imports the declaring module at all; and the **shared-input** pair, which pins that the two sides compute the importer's occupied bare names identically — codegen reads them after Pass 0's helper renames, the verifier from the pre-transform AST, and a non-generic `where`-helper named `gen2` made the same imported generic bare-name-owning on one side and qualified-only on the other.  The idempotence of that derivation is asserted directly across BOTH Pass-0 transforms and their composition — over a fixture carrying every helper shape it distinguishes (non-generic under non-generic, under a generic parent, under a generic helper, and a generic helper), since a fixture missing one would let a partial assertion look total — with each shape's membership pinned individually beside it, because idempotence alone would hold for a derivation that answered the same WRONG set every time.  Two more families close the visibility dimension: the **transitive** one, driven through the production `ModuleResolver` (a hand-built `ResolvedModule` defaults `direct=True` and would never reach the path), asserting that a module reached only transitively has ALL its generics qualified-only — the entry's namespace does not hold them at all; and the **user-written qualified call** (`deep::gen(true)` where the importer declares its own `gen`), which must key its instantiation to the module's declaration rather than to whoever owns the bare name |
| `test_module_shadowed_generic_effect_op_1310.py` | 4 | 410 | #1310: a qualified-only (shadowed) module generic's instantiation discovery had no effect-operation registry at all, unlike #1207's unshadowed discovery walk.  `idg(get(()))` inside `handle[State<Int>]`, where `idg` is a `forall<T>` generic declared in an imported module, checked and verified clean and then compiled with `[E602]`/`[E620]` notes and no `main` in the emitted module: the WASM call-rewrite correctly named `mod$mlib5$idg$Int`, but `_collect_shadowed_qualified_calls` (codegen) and its mirror `walk_seed` (the verifier's `_collect_shadowed_qualified_instances`, #732) fell through to the phantom-var `Bool` default for the effect-op argument, so `mod$mlib5$idg$Bool` was the clone actually emitted and verified.  The issue's own repro is pinned end to end (no E602/E620, the checker's own clone name in the WAT, and the runtime value), plus a nested-distinct-state cell (mirroring #1207's own) that would still pass a fix stopping the `Bool` default without preserving `HandleExpr`'s merge-over-the-enclosing-scope semantics, now also asserting the outer cell's clone is absent, matching the first cell's shape.  Two more cells run the #732 differential directly on both fixtures: codegen's `_emitted_instances` and the verifier's `_instances` must name the identical instantiation, red if either side's `HandleExpr` merge is reverted alone |
| `test_ambiguous_import_refusal_1304.py` | 40 | 1,202 | #1304 — two imports supplying one bare name are refused, in every namespace.  Spec §8.5 ordered a local declaration against an import and gave the qualified form for a clash it hides, but defined no order between two IMPORTS of one name, and neither did the implementation: a module importing two dependencies that each export `forall<T> fn gen` — one `@Int`-returning, one `@Bool` — bound its bare call to whichever supplier a set of module paths yielded first, so one unchanged file was check-green on one run and `[E121] body has type Bool` on the next (at the branch point: accepted on hash seeds 0, 2 and 3, rejected on 1, 4, 5, 6 and 7).  The load-bearing cells are the DETERMINISM ones — each import order checked in four fresh subprocesses under four `PYTHONHASHSEED` values, asserting one byte-identical verdict including message and location, which the base tree cannot satisfy and which a merely deterministic PICK would also fail (the refusal is what removes the choice).  Around them: the refusal is definition-gated like the E608 rail it generalises, so an unused clash is still refused and swapping a bare call for the qualified form does not lift it; the two escape hatches — a local declaration (§8.5.2) and a selective import — are asserted to their RUNTIME VALUE, since a disambiguation resolving to the wrong supplier is silent at check and wrong at run; four non-ambiguous controls (one supplier, disjoint names, a private namesake, an out-of-filter namesake) hold the refusal to bare-name ambiguity; and the emitted code is held to a typecheck-phase range, because reusing a codegen code would carry #1304's own complaint — a scope question enforced at the wrong layer — into the fix.  A subprocess canary pins that every fresh interpreter measures this checkout |
| `test_module_generic_collision_1281.py` | 20 | 809 | #1281 — E608 must not refuse two modules' PROVABLY DISTINCT generics.  A generic emits nothing under its bare name, and since #1274 its clones live in a namespace chosen per OWNER, so the diamond (`base` public, `mid1` private, both named `gen`) cannot overwrite anything — and was refused outright, with `vera verify` returning rc=0 beside the refusal.  Each door now answers its own module's generic (555 + 111) against the standalone oracles, and the emitted module carries `mod$…$mid1$gen$Bool` and `mod$…$base$gen$Bool` with nothing in the entry's bare clone namespace.  The relaxation is gated on three conditions, each with its own cell: both declarations are top-level generics (a generic beside a non-generic keeps the refusal), at most one owns the bare name (asked of the predicate directly, since end to end the ambiguity gate catches that shape first), and no namespace can name both — a module importing two dependencies that each export `gen` would resolve its own bare call to one of them, and spec §8.5 refuses the name outright rather than ordering the two imports (issue 1304).  The CHECKER reports that (E155) and this rail is its backstop, so both cells drive the shape through `build_multi_module_past_check` and assert both layers: a rail no test can reach is one that can rot into a relaxation nobody measures.  A namespace that declares its own `gen` is not ambiguous however many dependencies export one (§8.5.2).  The registration half — a qualified-only generic contributing no bare `_fn_sigs` or `_fn_ret_type_exprs` entry — is pinned by two STRUCTURAL cells, one per table, and its docstring says why: with #1299's scope narrowing in place both withholdings are defence in depth, reverting them leaves every suite and the whole conformance corpus green, and they are kept only because four consumers read those tables per NAME and nothing but their current internals stops each from picking one |
| `test_lexical_fn_scope_1299.py` | 56 | 1,554 | #1299 — codegen's bare-call ownership table must be the CALL SITE's lexical scope.  The #1284 predicate is one rule over two tables, and codegen's was `set(_fn_sigs)`: every symbol the whole compilation absorbed, including names the compiling body cannot see, so a bare `get(())` the checker resolved to a `State` operation was lowered as a call to some other declaration.  Four routes, all check-green — an imported module's **private** `get`, a **public** one a selective import excludes, a `where` helper of a **`forall<T>` parent** (which keeps a bare key beside its clone-qualified one where a non-generic parent's does not), and the ability operation `show`, which E151 does not reserve and which reaches the same table through the INTRINSIC gate rather than the op one.  Where the widths agreed the module loaded and answered the invisible declaration's value (7007 for the cell's 42007); where they differed it failed to load; the generic-`where` route is always loud (`unknown func $get`).  Every expected value is the checker's, PROVEN by a type oracle rather than assumed — the invisible `get` returns `@Bool` while the caller returns `@Int` from it and checks green — and each route carries a rename control.  The visibility matrix (public/private × in-filter/excluded/wildcard × shadowed/unshadowed × direct/transitive) asserts the verify verdict and the runtime value together per cell.  The two directions are pinned at once: the sibling loses the name, the generic TEMPLATE keeps it (asserted on the emitted instruction stream, since monomorphization supersedes the template and a value assertion would be green either way), and a lifted closure — compiled through its own `WasmContext` — inherits its parent's scope.  Four table invariants sit beside them: the scoped set is a subset of the registry, every `$`-bearing key stays in it, prelude names stay in it, and every emission door supplies a declaration its own helpers |
| `test_phantom_generic_instances_1271.py` | 14 | 358 | #1271 — discovery inside a still-generic scope must not instantiate a callee at an ENCLOSING scope's type VARIABLE.  `pick(@U.1, @U.0)` inside `forall<U> fn helper` bound `pick`'s variable to the NAME `U`, so a `pick$U` clone was emitted whose parameter has no WASM type and which the compilability pass then skipped with a loud `[E604]` — the noise that kept #1223's shapes out of the conformance suite.  Drives the four #1223 fixtures plus a mutual-recursion shape (two sibling generic helpers under a generic parent, whose phantoms include one arriving through a callee's declared RETURN type, `leaf$W`), asserting on ONE compile that no clone is keyed by a type variable, that no E602/E604/E605 skip is emitted, AND that the genuinely concrete clone is still there — the third assertion being what separates the filter from an over-filter that would take the real instantiation with it.  Plus the **primitive-spelled binder** matrix (`forall<Int>`, `<Bool>`, `<String>`, `<Float64>`), each row instantiating a sibling at exactly the type its binder is spelled like — a shared `idw(5)` would have let every row but `Int` pass for free — asserted on the clone set AND on the program still running; with the `Q`-binder control that keeps a genuine type variable filtered, so the fix cannot degenerate into "never filter".  That control CREATES a live phantom candidate — a generic helper under a generic parent, handing its callee an argument typed by its own binder — because a control that merely fails to create one holds under any filter including none; mutation-checked by disabling the filter, which turns it red |
| `test_handle_exn_divergent_result_1276.py` | 10 | 391 | #1276 — a `handle[Exn]` whose clause body AND handled body both diverge emitted a result-LESS `block` into a result-expecting context: check-green, verify-green, rejected at load with `type mismatch: expected i64 but nothing on stack`.  Four divergent shapes (the issue's Int rethrow, the `Byte` payload spelling #1269 unmasked, a three-deep rethrow chain, and a clause diverging through both arms of an `if`), each asserted on valid WASM AND on the observable — the OUTER handler's clause value, 1000.  Paired with the Unit TWIN, which infers `None` for the same reason but DOES complete: it must keep running and its WAT must contain no `unreachable` at all.  The pairing is the point — `result_wt is None` means two things wanting opposite lowerings, and a fix that terminated both would trap a program that runs.  The MIRROR family covers a clause that throws on one path and COMPLETES on the other (`if` and `match` spellings), where the inference read only the `then` branch / arm 0, answered `None`, and left the completing path's value stranded in a result-less block; the `if` case appears twice with different thrown values so both the throwing and the completing path are exercised from one inference |
| `test_infer_vera_type_join_1286.py` | 26 | 577 | #1286 — the VERA-level siblings of #1276's WAT join.  `InferenceMixin._infer_vera_type` (the WASM call-rewrite consultor) read `then_branch` only and `arms[0]` only, and `Monomorphizer._infer_vera_type_name` (the instantiation-discovery consultor) read `then_branch` only and had no `MatchExpr` arm at all — so a branch that throws, naming no type, decided the answer for the whole expression.  Two symptoms from check-green (and, with contracts, verify-green) source: as an array-literal ELEMENT the `None` raised `CodegenSkip` and the declared `main` simply left the exports with a loud [E602] note, and as a GENERIC ARGUMENT it left the type variable unbound, so `idg$Bool` — the phantom-var default, an i32 clone — was emitted for an i64 `Int` argument and the module failed to load.  Seven witnesses (array literal in the `if`, `match` and pair-representation `String` spellings; generic argument in the `if` and `match` spellings; the constructor FIELD behind the same conditional), each asserted on the value, on `main` surviving into the exports, and on the absence of the skip note — the drop is quiet at the value level once the function is gone.  The seventh witness is the consultor-AGREEMENT case, where every arm completes and nothing diverges: the rewrite named `idg$Int` from arm 0 while discovery named the phantom default, and the caller was dropped on a dangling target — which is why the repair lands on both consultors together, the clone-name agreement contract (#772) making the pair the unit.  Each witness carries its ARM-SWAPPED twin and the pair must agree, so the join property under test is order-invariance rather than a remembered value; a WAT assertion pins WHICH clone the module carries, since a value can be right for the wrong reason.  The PR review round found the same divergence one shape over and the sweep it prompted found a third, both closed here: discovery had no `Block` arm, and the transformer leaves a braced match-arm body AS a `Block`, so `Some(@Int) -> { let … }` named nothing there while the rewrite named the concrete clone — `idg$Int` emitted and never registered, `main` dropped from a check-green program.  It only reaches a wrong answer when no later arm yields either, so the witness pairs the block-bodied arm with a throwing one; the braced-`if` variant needs the branch TAIL to be a block in its own right, a `let` inside the branch being a statement.  The third is a `handle` in argument position, a presence cell since it has no branches to exchange.  An `IndexExpr` argument dangles the same way and is deliberately NOT closed here, tracked as #1327 — the rewrite's arm resolves chained indexing, aliases and `Future` payloads against codegen tables the monomorphizer lacks, so a partial mirror would trade "both say unknown" for "the two disagree".  WAT membership is tested through `wat_fn_names` / `wat_calls`, not `in wat`: the substring form is a prefix test that a longer mangled symbol satisfies, which is exactly how one clone impersonates another.  Mutation-checked one edit at a time: reverting the rewrite-side `if` fails 13, its `match` 8, the discovery-side `if` 8, `match` 9, `Block` 6 and `HandleExpr` 2, and all six at once fails all 26 |
| `test_generic_under_generic_callees_1223.py` | 8 | 298 | #1223 — a generic `where`-helper under a GENERIC parent instantiates its own generic callees.  The helper is monomorphized only during clone hoisting, outside the worklist that rescans every clone it emits, so a top-level generic called from the helper body was discovered only in its still-generic spelling (`pick$U`, binding the enclosing type variable's NAME) while the rewrite called `pick$Bool` — E602 skip, E620 drop of the parent and of `main`, "No exported functions" from a check-clean, verify-clean program.  Four shapes — a user generic, the prelude twin (`option_unwrap_or`), two levels of generic nesting where the INNER helper is the caller, and the non-generic-parent control that compiled before the fix and must keep compiling (it is what proves the trigger is the generic ancestor rather than the nested helper) — each asserted on no E602/E620, the checker's run value (the helper's argument order is non-commutative, so a miswiring gives 7 instead of 3), and a REGISTERED-vs-RESOLVED differential.  That differential captures the emitted mono-decl names rather than `_emitted_instances` (whose generic-under-generic entries are keyed by the concrete-free lexical chain, not by the per-clone emission name the rewrite calls) and captures the rewrite side on `_resolve_generic_call` rather than from the WAT, because a desync skips the calling function and removes the dangling `call` along with it.  The verifier's half of the pair is pinned in `test_monomorphize_differential.py`'s inline corpus, not here |
| `test_mono_effect_op_naming_1207.py` | 9 | 339 | #1207 — monomorphization discovery and the WASM call-rewrite name ONE clone when an effect operation fixes a generic's type argument.  A differential over the two consultors, not a unit test on either: the compiler's own E602 ("call target not registered in this module") IS the two sides disagreeing, so each case asserts no E602/E620, and additionally pins WHICH name they agreed on — an alignment on the wrong one still fails.  Four instantiation-driving shapes (`get(())` as an array-literal element under a plain `State<Nat>` cell, under a `type Count = Nat` alias cell whose clone must be `pick$Count`, in a function whose operation comes from the DECLARED effect row rather than an enclosing `handle`, and in direct argument position), plus the `array_append` builtin-argument control and a shadowed-name control — a user `get(@Unit -> @Bool)` is NOT an effect op in a declared row, so the clone must be `pick$Bool` and not the cell's; that case is green before the fix as well as after, which is what makes it a guard against the alignment over-reaching rather than a second copy of the repro |
| `test_effect_op_determinism.py` | 9 | 504 | #1215 — bare effect-op resolution order: the built-in `State` and `Http` both declare `get`, so `effects(<State<Int>, Http>)` is a two-candidate row with no user `effect` declaration needed.  The two candidate bindings are made to produce DIFFERENT observables (the source-order program runs to `70`; the reversed row is a loud `E217` naming `Http.get`), swept across six `PYTHONHASHSEED` values in child interpreters so a frozenset-order flip cannot pass — plus the innermost-handler-beats-declared-row precedence case, a signature-level assertion that the resolved `OpInfo` follows the recorded order both ways (including the deterministic name tiebreak for a row member no order tuple mentions), and the qualified-lookup control.  The type-ARGUMENT sibling rides here too: `effects(<State<Int>, State<Bool>>)` (two independent cells, spec §7.3.3) had the identical frozenset dependence in `_effect_type_mapping`, and codegen took the LAST instantiation in the row where the checker takes the first — both now source-order-first, swept the same way.  A sixth sweep covers the public `ordered_effect_row()` fallback for a row member no order tuple mentions: its two members share the effect NAME and differ only in type ARGUMENT, so a name-only sort key ties them and hands back frozenset order — the order AND the `_effect_type_mapping` selection it drives are both asserted stable across the same seeds.  Two further sweeps take that structural key down a level: a type argument may itself be a FUNCTION type, whose own effect row was rendered by `pretty_effect` — so two outer instances differing only INSIDE a nested row (by a refinement's predicate, or by a type variable's built-in marker) tied again, and both legs are asserted single-outcome across the same seeds, separately, so a regression names the elision that came back |
| `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 | 780 | #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` | 242 | 2,632 | 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; the twenty-one *contextual* keywords `then`/`else`/`data`/`type`/`module`/`import`/`public`/`private`/`requires`/`ensures`/`invariant`/`decreases`/`effect`/`with`/`in`/`where`/`pure`/`ability`/`effects`/`op`/`result`, derived from `grammar.lark` rather than hand-listed and reachable rather than traps — each declared, was called and answered its value before the fix — over five parametrized batteries (declaration, visibility, `where`-helper, a rationale free of the keyword branch's false unreachability claim, and a usable per-name fix suggestion) with `handle` and fifteen keyword-containing names as controls; and `resume`, reserved on separate grounds — not a keyword, so the declaration parses and outside a handler a bare call reaches it, but it collides with the resumption binding every clause body carries, and the pins cover the rejection, the where-helper depth, that the rationale carries none of the other two branches' false claims, that handler-clause `resume(...)` still checks AND that a wrongly-typed one is still E202 — the pair, since a binding that accepted anything would satisfy the first alone — and that the rejected declaration draws no second error out of the correct clause bodies it used to shadow, at both top level and where-helper depth), parsed module calls (#420 split) |
| `test_checker_errors.py` | 73 | 1,196 | 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` | 775 | 1,741 | 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 43 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), the #1242 stream partition — over a corpus widened to every conformance program that type-checks, at any level, `len(obligations) == total + violated + tier3_unguarded` and every status is one of the documented five, with the vocabulary read from the `ObligationStatus` Literal so a sixth member fails rather than vanishing from the counts — 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; plus the #1208 call-site rendering pin — a PARAMETERISED callee slot substitutes into the E501 message and its fix instead of falling back to the generic wording |
| `test_verifier_contracts.py` | 96 | 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` | 82 | 1,743 | **`@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) whose rationale names its actual cause — an untranslatable value — rather than the untranslatable-or-timeout conflation #1251 removed, 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` | 81 | 2,199 | 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); #1236 — a GENERIC callee's call-site precondition demotes loudly (E532 Tier-3) instead of vanishing, in the violating direction with the runtime oracle that makes the old all-Tier-1 verdict a FALSE one, in the satisfied direction (conservative until #732 translates the contract per instantiation), and from the ensures-clause drain as well as the body's, against a non-generic twin that is still discharged statically and a `requires(true)` generic that stays silent |
| `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_budget.py` | 36 | 285 | #1350 — the configurable Z3 budget. Resolution order (explicit argument > `VERA_Z3_TIMEOUT_MS` > 10 s default), malformed values raising rather than silently reverting, the seams that construct a solver honouring it, and the CLI surface (`--timeout-ms`, the effective budget echoed in `verify --json`, refusal by name on every command that cannot honour it — including the no-file ones that dispatch early, `lsp` worst of all — and `compile` unaffected by a stray env value). The budget's arrival is checked by SPYING on `z3.Solver.set` rather than by timing anything: explicit argument, environment and default each reach the solver, cold and warm, and a warm session and a cold `verify()` given the same budget hand the solver the same number — the differential oracle's property at the plumbing level. Deliberately no wall-clock assertions live here; the categorical control that separates "needed more time" from "cannot see through it" is `test_examples_ephemeris.py::test_transcendentals_stay_tier_3_at_any_budget`, which re-verifies at three budgets instead of measuring elapsed time. |
| `test_verifier_adt_decreases.py` | 22 | 822 | 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` | 92 | 2,480 | 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); plus the #1214 zero-size-argument differential — `mk(())` and `mk(1)` must record the same `refine_bind`/`violated`/E505 obligation and the same summary, a satisfying call-site precondition must discharge under both spellings, and a zero-size formal sitting BEFORE an informative one must not shift which argument the callee's precondition is checked against, an ERASED argument that is itself a call keeps its own nested precondition obligation (the walk happens, only the result is discarded), and `Future<Unit>` — direct and behind an alias — is masked as the second zero-size type; plus the #1251 disclosure-honesty set — an E506 over an UNMODELLED base names the base rather than blaming Z3's decidable fragment, a modelled base with a deferred predicate still names the predicate (the over-correction guard), and a SYMBOLIC narrowing keeps its obligation, status and code once the concrete gate lands; plus the #1251(b) concrete-decision set — a LITERAL narrowing over an unmodelled base is decided rather than disclosed (`@Small = 200` is a rejection naming the value, `@Small = 5` a Tier-1 proof, the alias spelling of the cell the same), a predicate the fold cannot settle stays disclosed so the gate is shown to DECIDE rather than widen the base, and `ch02_byte_refinement` is pinned whole — verdict, counts and per-obligation status in order, since counts alone would net out a rejection here against a new proof there; plus the non-verdict split — `check_valid`'s `opaque` (#1199) and `unknown` outcomes get different reasons, driven directly by injecting the outcome since no whole program is known to reach those branches, with two structural pins over `vera/verifier.py`'s AST, both ranging over all three Tier-3 recorders (refinement, `nat_bind`, `nat_to_int_coerce`) and checking that roster against the source so a rename cannot make them vacuous: no demotion site fixes a solver reason at the call site instead of deriving it from `result.status`, and no call that is not literally `guarded=True` omits the reason its disclosure has to state — closed against the two measured escapes (an f-string parses as `JoinedStr`, a shared module constant as `Name`), failing on any `reason=` shape it cannot classify, and reading the module through `inspect.getsourcefile` so it is neither cwd-dependent nor able to inspect a different file than the tests import |
| `test_verifier_shadow_audits.py` | 71 | 1,395 | **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 | 888 | #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` | 259 | 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` | 36 | 602 | #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 unguarded generic-`@Int`-field case also has its `E531` rationale read for WHAT IT SAYS — a value bounded on neither side, not the untranslatable-or-timeout conflation #1251 removed. 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` | 136 | 2,897 | #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_nat_bind_construction_soundness_1332.py` | 42 | 713 | #1332 — a `@Nat` tuple component narrowed at CONSTRUCTION is obligated, never assumed (part of the #392 false-Tier-1 audit; the construction-position counterpart to `test_nat_narrowing_return_differential.py`'s return-position half).  `let @Tuple<Nat, Int> = Tuple(@Int.0, N)` destructured by an irrefutable single-arm `match` verified as **proved** while `vera run` trapped on a negative: `_translate_match` asserted the arm's `@Nat` sub-pattern source fact UNCONDITIONALLY at the solver's base level, where the datatype accessor axiom reduced it to the construction obligation's own goal — the obligation discharged itself.  The anti-circularity test existed but was SYNTACTIC (is the scrutinee AST a `ConstructorCall`?) where a `let`-bound tuple arrives as a slot reference whose TERM is one.  Every cell pins the verdict against a control that must not move, because a verdict alone cannot separate the repair from over-rejection: the precondition-discharged form still proves and still runs, the return-position form is unchanged in both directions, and the two construction spellings — with and without the destructure — must agree with each other, which is the internal inconsistency the bug consisted of.  The soundness differential asserts the verdict and the run in ONE test (verify-clean beside a trapping run IS the bug, so siblings would each pass alone), with its `requires(@Int.0 >= 0)` parametrisation verify-clean so the implication is exercised with a true antecedent.  The REFINED sibling is here too, repaired by the same change and worse in kind — a refined tuple component carries no runtime guard, so pre-fix it returned `-7` for a `PosInt` from a verify-clean build rather than trapping.  Two over-rejection controls straddle the guard: one where it FIRES (a tuple built from an already-`@Nat` parameter, whose postcondition still proves from the parameter's own declaration) and one where it does NOT (an opaque `@Tuple<Nat, Int>` parameter, whose declared source facts must survive).  The suite is then parametrised over how the scrutinee is PRODUCED, because a guard asking "is this term literally `C(args)`" is defeated by anything that wraps the construction — an `if` producing the tuple laundered past the first version, verifying both narrowings while the program trapped, and a `match`-produced spelling did the same.  Bare constructor, `if` with both arms constructed, `if` with one constructed and one call-produced, `match`-produced and let-of-let are each required to keep the narrowing obligated, in the `@Nat` and refined families alike, beside call-produced and opaque-parameter controls that must keep their facts — the boundary being PROVENANCE: a call- or parameter-produced value's component facts were established in the callee's context, a locally constructed one's are still outstanding |
| `test_nested_ctor_sort_1360.py` | 30 | 680 | #1360 — a `Tuple` nested inside a constructor translates, and `verify --json` always envelopes.  `let @Option<Tuple<Nat, Int>> = Some(Tuple(@Nat.0, 1234));` was check-green and killed `vera verify` with a raw `z3.z3types.Z3Exception: Sort mismatch`, emitting NO `--json` envelope at all.  Two sorts derived by different routes disagreed: a nested `Tuple` argument is built by the variadic-tuple branch keyed on the arguments' Z3 sorts (`Nat` reads back as `Int`, so always the `Int` spelling), while the enclosing ctor's sort comes from `_resolve_pinned_sort`, which prefers a cached instantiation equal to the pin MODULO `Nat`/`Int` — sound at a scalar position where both spell one `IntSort`, unsound at a datatype position where #884 made the two injective sorts.  The `Nat` appears even in an all-`Int` program because a positive literal types as `Nat` on the declared side, which is why the trigger is the NESTING and not `Nat`; same-ADT nesting (`Some(Some(...))`) is carried as a control, measured passing before the fix, so the repair is pinned to the disagreeing sorts rather than to nesting in general.  The envelope half is asserted INDEPENDENTLY of that crash — a translation function is monkeypatched to raise and the cell asserts stdout is a parseable `E699` envelope rather than empty, so the machine-readable contract holds for the next translator bug too — and the pair mutation-validates apart: reverting the sort fix reddens the four translation cells while the controls stay green, breaking the backstop reddens exactly the two envelope cells.  A fourth group covers the guard PREDICATE itself: `_ctor_accepts` exists to intercept Z3's raise-instead-of-error behaviour, so a predicate that can itself raise defeats its own purpose — hostile stand-ins whose `arity()`, `domain()` and `sort()` raise must be ANSWERED `False` (the conservative "does not accept", which routes to the decline path) rather than propagate, beside a discrimination cell over real Z3 terms so the group cannot be satisfied by a predicate that swallowed its body and declined everything |
| `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` | 62 | 2,191 | #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.  The #1274 per-module half lives here too: every QUALIFIED-ONLY module generic (private, out-of-filter, or locally shadowed) must be emitted AND discovered under the same `mod$<path>$name` base, with the complement pinned beside it — a public in-filter unshadowed generic must keep the bare name, or #774's bare-call routing would break in silence |
| `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` | 117 | 2,665 | 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_alias_adt_name_width_1309.py` | 112 | 423 | A `type` alias whose name is also a registered ADT's must emit the ALIAS TARGET's width (#1309).  Codegen's `_type_expr_to_wasm_type` tested `_adt_layouts` — and `Array`/`Map`/`Set`/`Decimal`, none of them primitives — before the alias table, where the checker's `_resolve_named` resolves primitive, then alias, then declared ADT; so `type Option = Int;` emitted the ADT's i32 pointer for an i64 slot on a check-green, verify-green program.  Three dispositions are pinned separately because they fail differently: LOUD scalar targets (`Int`/`Nat` i64, `Float64` f64) died at load; PAIR targets are the SILENT ones the issue's "matching widths" prediction missed — an `i32_pair` is two words and the single i32 dropped the length, so `string_concat("ab", "ab")` returned junk bytes and `array_length` over three elements returned 0, both at exit 0; and matching-width targets (`Bool`/`Byte`/`Map`/`Set`/`Decimal`, all i32) are INERT, kept as green-both-sides guards that the reorder leaves them alone.  The battery is the differential that makes width-luck unreintroducible: every name in the LIVE built-in ADT registry (read off a real `CodeGenerator`, so a new built-in joins without anyone widening a list) crossed with every representation class, comparing the emitted `twice` body in full — header widths and the instructions under them — against the identical program under a fresh alias name, plus the two unit duals — under an alias the derivation answers the target's width, without one it still answers the ADT pointer, so "the alias wins" cannot be satisfied by breaking every ordinary ADT parameter.  Primitives are asserted to still shadow a same-named alias — the one branch that must NOT move — across all seven spellings by asking the derivation directly, which is the only way to reach every one of them since two are checker-refused (`@Bool.0 + @Bool.0` is E140, `type Int = Int;` is E132); a run-level program carries the behavioural half, because `type Bool = Int;` used AS a Bool is check-green, runs, and distinguishes the hoist mutant.  An earlier draft claimed the checker refuses every program that would exercise this, which is measured false.  A separate block covers the THIRD consumer of the same disease (CR on PR #1323): `_return_type_is_string` tested the `Future<T>` transparency strip before the alias table, so under `type Future<T> = Array<T>;` a `@Future<String>` return was classified a string and `execute()` decoded the array's backing bytes as UTF-8 — two NULs where the fresh-name control printed the pointer, measured identically at the branch point and so pre-existing.  `String` stays ahead of the alias branch there too, being the one primitive involved, and three over-correction controls hold the #841/#1047 transparent-`Future` decode and PR #1041's alias-to-`Future` shape.  `Json` and `HtmlNode` are deliberately outside the prelude-ADT row: their prelude combinator bodies render against the flat alias map a main-file shadow pollutes, which is an alias-env SCOPING defect (#1316) the reorder does not reach — though it does MOVE that failure (17 prelude `json_*` signatures flip width, the loader's complaint reverses direction, `html_attr` loses a push), so "fails identically" — an earlier draft's wording — is measured false |
| `test_codegen_pair_scrutinee_1305.py` | 32 | 685 | A `match` whose SCRUTINEE is pair-represented (`String` / `Array<T>`) took one local at the internal `i32_pair` pseudo-type, so the module carried `(local $l1 i32_pair)` and never assembled (#1305).  The issue reached it through `json_keys` and framed it as an `Option<Array<String>>` payload binder; the docstring records why measurement does not support that — `json_keys` returns `Array<String>`, and `array_length(json_keys(j))` compiled and ran at the branch point — so the tests are built on the shapes that actually trigger it: `match @String.0 { @String -> … }` and `match @Array<Int>.0 { @Array<Int> -> … }`, both legal and check-green, plus the slot, call-result and builtin-result scrutinee forms.  One test returns the BOUND STRING rather than its length, because a fix that allocated two locals and copied only the pointer passes every length-free assertion.  The issue's own repro matches `Some`/`None` against that array; a pair carries no tag, so the assertion is that the module assembles and the refusal is a located E602 — not that the nonsense compiles (the checker accepting it is #1315).  The guard is a WHITELIST (wildcard and binding only) and these cells are why: as a blacklist naming the two constructor kinds it let `true ->` and `1 ->` fall through into the arm-condition emitter, turning a loud WAT failure into a check-green program that exits 0 printing 100 from the scrutinee's heap POINTER read as a truth value, and its integer twin into a shipped `.wasm` that died at instantiation with no diagnostic — so five unlowerable-arm cells (bool/int/string literals over both pair spellings) and a nullary-arm-FIRST program pin each half, the last because both original repros led with `Some` and left the nullary half droppable green.  The two shadow pushes are pinned as EMISSION by a WAT differential against the match-free twin (exactly two more push idioms) plus a position assertion that no length half is rooted: deleting both pushes leaves the whole suite, the GC rooting and reclamation suites, and four allocate-in-the-arm probes under `VERA_EAGER_GC=1` green, so a behavioural claim would be one no probe supports.  The two controls the issue listed as already-compiling are kept as regression guards, and an Option/Result binder battery over `Array<String>`/`Array<Int>`/`Array<Json>`/`Map`/`Set`/`String`/`Int` payloads plus a nested `Option<Option<Array<String>>>` pins the boundary: the scrutinee change left pair-typed constructor FIELDS alone |
| `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,141 | Map + Set collections (#62), wrapper-handle bit-31 tagging (#578) (#419 split) |
| `test_codegen_json.py` | 116 | 1,112 | Json collection, typed accessors (#419 split), canonical serialization (#1293 — `format_json_number`'s ECMAScript boundaries and `dumps_canonical`'s shape, insertion-ordered keys, non-finite refusal, and rejection of values outside `read_json`'s domain) |
| `test_json_accept_domain_1306_1308.py` | 97 | 720 | `json_parse`'s accepted domain on the reference host (#1306, #1308): spec §9.7.1 states it as RFC 8259-valid text that decodes to finite numbers and strings of Unicode scalar values, and all three exclusions are pinned end-to-end through a compiled program that reports which arm it took plus the whole `Err` message — the JavaScript constants at the top level and nested in containers, with the first of two naming the refusal; a number that OVERFLOWS to an infinity (`1e999`, `-1e999`, `[1e999]`, `{"a":1e309}`, `1E999`, `[[1e999]]`), the second entry route to a non-finite `JNumber` and the one both host parsers accepted, so it diverged from the stated domain on both hosts at once rather than between them; the same overflow in its INTEGER spelling (`1` followed by 309, 310 and 400 zeros, signed and nested), which was reference-host-only because `json.loads` returns an `int` there and a float-only range check never saw it, with the bound pinned as the double ROUNDING boundary against `float()` as oracle and `int(sys.float_info.max) + 1` as the control that separates it from the obvious-but-wrong bound; and a lone surrogate parameterised over position (value, key, array element, nested, top-level string) and escape casing.  The controls carry the weight the refusals cannot: matched surrogate pairs (single, adjacent, at end of string, literal astral) still parse, `1e308` / `-1e308` / the largest representable double still parse so the overflow refusal is a boundary and not a wall, **underflow is decided rather than assumed** (`1e-999` decodes to `0`, finite and in the domain, so it is accepted — the plausible wrong answer is symmetry with overflow), `"NaN"` as a string value and as a key is ordinary JSON, and text malformed for any other reason keeps its host-native syntax message — the constant-lookalike shapes (`[Infinity_x]`, `{Infinity:1}`) that a raise-on-sight `parse_constant` hook would have misreported, which is why the hook records and the refusal is decided after the parse, and the sign/case shapes (`-NaN`, `[-NaN]`, `+Infinity`, `infinity`, `nan`, `-Infinityx`) that a token scan without a value-start constraint would have claimed.  Unit tests on `first_domain_violation` — the ONE document-order walk both value-level exclusions share, so "whichever comes first names the refusal" needs no precedence table — pin the traversal directly (key before its own value, earlier entry before later, D800/DFFF inclusive at both ends, an `int` and a `bool` never read as a non-finite number, and the NaN arm that no JSON text can reach) where the end-to-end probe can only observe the first refusal.  The cross-host half is `TestBrowserJsonAcceptDomainParity1306_1308` in `test_browser.py` |
| `test_codegen_decimal.py` | 57 | 779 | Decimal collection, Decimal monomorphization (#419 split) |
| `test_codegen_host_effects.py` | 71 | 1,135 | Html/Http/Inference host effects, provider dispatch, postcondition host-import propagation (#823) (#419 split) |
| `test_inference_response_shapes_1333.py` | 164 | 2,131 | #1333 — `Inference.complete` parses a provider response by SHAPE, not by position.  The Anthropic Messages API returns `content` as a list of TYPED blocks and a reasoning-capable flagship leads with a `thinking` block, so `content[0]["text"]` raised `KeyError('text')` and the host boundary published the bare key `'text'` as the whole `Result::Err` payload.  Three properties, one per defect: selection by `type` across both response families — the OpenAI-style `message.content` is a string, a list of typed parts, or `null` on a reasoning turn, where the old `str(...)` returned the literal completion `"None"` — with a selected entry's `text` itself required to BE a string, the review having found the same coercion one level deeper, where `text: null` became that completion and an object became a Python repr; every shape failure and HTTP rejection naming the provider AND the model that answered, with the error body read under a 64 KiB cap so the message bound is a memory bound too, every interpolated field routed through the same 200-character limit, and the configured key plus any credential-shaped token redacted before it can reach a Vera value — on every route, a table of twelve parametrized rows standing in for the invariant after a review pass found the non-JSON-body path unredacted, a sweep found six more, and a second pass found four render sites whose `api_key` could be dropped with nothing red; two structural tripwires now hold it — the count of `api_key`-carrying render sites, read by an AST walk rather than a regex (which undercounted the same source by one and could not see a positional key in a multi-line call), and the row count itself, since deleting a row was invisible to the first and left the suite green one cell lighter. An empty or whitespace-only completion is an error only when the provider explained it — `stop_reason` `refusal` or `max_tokens`, `message.refusal`, `finish_reason` `length` — with the reason matched case-insensitively and the token carried verbatim into the diagnostic, and a response with no block or part of the selected type at all reported as an error naming the types that were present, and the blank test is `.strip()` on both the string and list paths, which is what round 9 claimed and delivered only for the exactly-empty fragment, which is what makes the sweep's own misattribution impossible to repeat — with `VERA_INFERENCE_PROVIDER` unset, auto-detect takes the first key set to a non-empty value in registry order, so a still-exported Anthropic key won the "xAI run"; and a boundary that labels any exception this module did not itself write.  The verbatim channel belongs to a dedicated `InferenceError` and nothing else: the original rule named plain `RuntimeError` / `ValueError` by exact type, which the PR review refuted — those are the types an unforeseen transport failure raises too, so `RuntimeError("boom")` from below claimed the channel and surfaced as the bare `boom`.  The headline cells run END TO END through `execute()` over a mocked `urlopen` — the product path the report came from — with the six-provider sweep parametrized in registry order, its rows pinned against `_PROVIDERS` so a new provider cannot silently leave the sweep.  Mutation-checked, every count re-measured on the tree as it stands: the by-position read 45, the boundary's plain-type rule 18, the shared redaction helper 28, the boundary label 8, the `str()` coercion 8, the missing-`text`-key skip 7, the reason clause 21 (the same whether its function body is emptied or all four call sites are neutralised — an earlier note claimed the two forms differed), the `output_text` preference 6, the empty-completion rule 10, the blank test's truthiness revert 4, the reason's case fold 3, the `xai` credential prefix 3, the strict `.decode("utf-8")` 3, and the narrower one-to-three-cell guards (redact-before-truncate, the exact-key rule, the `output_text` preference, the truncation window's start, the "(no keys)" honesty rule, the credential pattern's eight-character floor, and the three bounded-read guards). Every `pytest.raises` in the file names `InferenceError` rather than `RuntimeError`: the class is a `RuntimeError` subclass, so the looser assertion accepted a site regressing to a plain one — making that regression fails 15 cells now against 2 before. The plain-type figure had read 5 with the drop blamed on cells bypassing the boundary; that was wrong. Threading the model into the boundary label made it a prefix of itself, so eleven `startswith` cells matched the wrapped message they existed to reject and lost discrimination silently — they now assert the label's absence too, via one shared helper, and the figure went back to 16, rising with each `_assert_deliberate` cell added since |
| `test_codegen_nat_guards.py` | 61 | 1,435 | **`@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.  #1256 extends both alias-aware gates to a parameterised alias APPLICATION (`type Ident<T> = T; type Count = Ident<Nat>;`), which the name-only chase resolved to the bare head `Ident` — so neither gate fired and `f(0 - 5)` returned -5 through the `@Nat` slot, #983's silent negative one spelling over.  Each parameterised case carries its unparameterised twin as the oracle (the claim is that the two spellings compile to the SAME guard, which a bare presence assertion would not catch losing), plus the run-trap on the violating value, the pass on a satisfying one, and the refinement-over-application control that pins the `_refinement_guard_parts` conjunct still keeps a refined return single-guarded |
| `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` | 258 | 5,102 | 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` | 5 | 266 | `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,835 | 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` | 34 | 855 | 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).  Also hosts the two compilability pre-scans' **field-coverage gate** (#1210 rounds 5, 7 and 9): it derives the obligations from the dataclass fields of `vera/ast.py` — one per `(class, field)` PAIR — and a pair is discharged only by the conjunction (the class `isinstance`-branched AND the field name read inside that branch) or by a justified-ignore entry naming the route its expressions ARE reached by.  Stronger than `scripts/check_walker_coverage.py`, whose set is the `Expr` subclasses and whose verdict is "the class is NAMED"; and stronger than the class-keyed obligation it replaced, which discharged the moment a class had ANY branch, leaving a new field on an already-dispatched class to a second, weaker screen (the mutation is pinned: fabricating one must fail the OBLIGATION).  The ignore table takes either key shape, and a class-level entry is permitted only while its class has a single field — otherwise it would exempt whatever field the class grows next, the same hole one table down.  The name-based limit of the dispatch route is stated on the gate.  Round seven adds the **boundary-guard derivation gate**: the emitter, the return-epilogue predicate and the import pre-scan must all read one tuple decomposition and none may reclassify behind it, which is the structure that makes their agreement a property of one function rather than of three.  Plus `contract_exprs`'s explicit dispatch, including the raise on an unknown `ast.Contract` subclass |
| `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` | 542 | 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` | 273 | 4,612 | 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, and the #1242 partition pin — the array is emitted unfiltered, a refuted obligation is counted by no summary field, and it still joins its E500 on the location key), runtime traps, arg validation, multi-file resolution, IO exit codes, --explain-slots (including the #1208 naming pins — an alias in type-argument position is tabled resolved, and a `forall` variable shadowing a module alias keeps the two parameter stacks apart — and the #1217 `where`-helper tables: the helper prints indented under its parent, appears in the JSON qualified as `parent.helper`, and inherits the enclosing `forall` variables so the shadowing holds inside it too), `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,976 | 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` | 49 | 1,395 | 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), the #1208 naming pin (the threaded alias environment canonicalizes a type-argument alias), and the #1216 resolution set — an alias-typed parameter is trialed rather than skipped, its alias-spelled `requires` constrains the generated inputs, a refined alias reaches Z3 with its predicate so no trial violates codegen's entry guard, a `forall` variable shadowing a same-named module alias still resolves to an unsupported type variable, and a parameter that resolves to a non-encodable type still skips with that type named; plus the #1229 set — an UNTRANSLATABLE input constraint skips the function naming the blocking conjunct instead of scoring the resulting entry-guard trap as a contract failure, on the reported `string_length` repro, on a mixed clause (only the untranslatable conjunct is named), on a quantified precondition and on a refined parameter's predicate, with a Tier-3 control that must still be tested so a skip taxonomy firing on everything cannot pass |
| `test_markdown.py` | 94 | 610 | Markdown parser: block/inline parsing, rendering, round-trips, edge cases |
| `test_lsp.py` | 146 | 2470 | 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 the #1208 keying pins: a parameterised reference resolves, an alias-spelled parameter is reachable from a canonically-spelled reference, and a `forall` variable shadowing a module alias lands on the right parameter), 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), handler bounding (#725: a caller discharging the effect around its only call site drops out of the closure and is not rewritten, while a second unhandled path, a call in a handler clause, a handler for another effect, a handler naming a different instance of the same effect (`handle[State<Nat>]` against a `State<Int>` propagation, which the checker does not discharge — end-to-end that caller must still be rewritten and the candidate must still apply, with the matching `State<Nat>` propagation against the same fixture as the positive control that this handler key does prune something), and a bare `where`-helper call all keep it in, as does a refinement type argument at either depth (`Exn<{ @Int \| p }>` and `Exn<Array<{ @Int \| p }>>` render as their bare base type but discharge nothing of `Exn<Int>` — also pinned end-to-end), while an unparameterised `handle[IO]` does bound an `IO` propagation, a whitespace-spelled `State< Int >` request still bounds, and nesting bounds in either order (a matching handler inside a foreign one, a foreign one inside a matching one) — plus a key-level pin that `handle[Mod.IO]` keeps its module, and the effect-less query pinned handler-unaware; plus the two boundary pins the review added — a call in the handler's STATE INITIALISER keeps its edge, since the initialiser is evaluated in the enclosing scope before the handler is installed (pinned beside the E125 the checker raises there against a `pure` caller, with the identical call in the handler body clean as the contrast), and an alias-spelled handler does not bound a `State<Int>` propagation though the checker discharges it (`handle[State<MyAlias>]` with `type MyAlias = Int` — the spelling comparison's under-prune, #1292, with the alias-spelled request as the control that does prune)), 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` | 413 | 5,094 | Browser parity: Python/wasmtime vs Node.js/JS-runtime output equivalence across IO, State, contracts, Markdown, Regex, and the examples the browser target can execute (two explicit lists in the file, not the whole `examples/` directory — interactive stdin, file IO, `DB` and the non-standalone `modules` example are excluded with their reasons recorded); plus the #349 `runtime.mjs` coverage battery — per-value-type and per-key-type Map variants, per-element-type Set variants, cold `Decimal` branches (exact-zero sign, negative-shift division, `decRoundPlaces` special cases, non-finite storage), `readJson`/`json_stringify` across every Json ADT tag, the Regex/Json `Result.Err` arms, and nested-Markdown walks.  Two operations carry a canonical form the specification states rather than merely agreeing across the hosts, so their batteries assert more than equality: `json_stringify` (spec §9.7.1) pins the expected string on every Json ADT tag and on the number-rendering boundaries, checks three-pass idempotence, checks that a non-finite `JNumber` fails on both hosts *and* prints nothing, pins the object key orders an ordinary JS object cannot carry (array-index keys, which ES enumeration hoists to the front in ascending numeric order, and a `__proto__` key, whose assignment writes a prototype instead of a field) on both a parsed and a program-built object, and checks the reference host's own number rendering differentially against a real `JSON.stringify` over doubles drawn from raw bit patterns; `md_render` (§9.7.3) pins the expected render, re-renders it to prove the fixed point, runs the round-trip property over a corpus carrying the container and multi-line shapes a flat corpus misses, and renders `MdBlock` values the test builds directly, since several renderer rules — a container's child separator, an empty container, a code span wider than one backtick — are unreachable through `md_parse`.  plus the #1306/#1308 accept-domain battery (`TestBrowserJsonAcceptDomainParity1306_1308`), which runs one `.wasm` under both runtimes and compares the WHOLE stdout — arm taken and `Err` message together — over the JavaScript constants, over numbers that overflow to an infinity in both their exponent and integer spellings, and over lone surrogates at every position a string can occupy, with the expected sentences imported from `vera/wasm/json_serde.py` so `runtime.mjs`'s hand-copied duplicates are held against the originals, beside acceptance controls (matched pairs, finite boundary values, underflow to `0`, `"NaN"` as a string value), a ten-case host-native-message battery pinning that neither the substitute-and-re-parse probe nor the value-start constraint hijacks an unrelated syntax error (`-NaN` is the case needing both rules — the substitution alone turns it into `-0` and manufactures a refusal the reference host never makes), a precedence case fixing that a non-finite constant outranks a lone surrogate on both hosts though each reaches that answer by a different route, and a document-order case fixing that overflow and lone surrogate are resolved by one walk rather than by two per-host precedence rules that would agree on every single-violation document; `md_parse` itself is not yet at parity and its remaining divergence classes are a tracked bug ([#1301](https://github.com/aallan/vera/issues/1301)); the suite pins the shapes the two implementations agree on |
| `test_conformance.py` | 1220 | 154 | Parametrized conformance suite: parse, check, verify, run, format idempotency across 244 programs; a negative entry fails at the stage `expected_error_stage` names (`check`, the default, or `compile` — which also asserts the program type-checks cleanly first) |
| `test_prelude.py` | 29 | 585 | Prelude injection: Option/Result/array operation detection, combinator shadowing, type aliases, the reserved namespace every injected alias declaration lives in — checked against the checker's own E154 regex rather than a second spelling of the rule, since an alias the prelude injects outside it is one codegen resolves and the checker leaves opaque (#1184/#1221) — 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_examples_ephemeris.py` | 11 | 351 | #143 — the tree's only floating-point example. Pins the rendered stdout byte-exact and both geocentric distances, then re-derives the angles from that output and checks them against an INDEPENDENT reference (ERFA's analytic model via astropy) to 30″ — the tolerance is the JPL element set's arcminute accuracy, not the code's. Per-function tier pins (`wrap_deg` at Tier 1, `kepler_solve`'s termination proved, and the two eccentricity refinement binds verified in `earth_elements` and `mars_elements` — the bound-at-construction story) deliberately stand in for a corpus-wide tier count, which moves legitimately whenever obligations are added elsewhere. The transcendental contracts are pinned at EXACTLY `tier3` across three solver budgets, which is the categorical claim the example's header makes: `verified` at 60 s would falsify it and `timeout` would mean the demotion had become merely slow. The fixture fails on any type error before verifying, so no tier is ever asserted about a program that does not compile. |
| `test_build_site.py` | 54 | 847 | 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; plus the #1341 implementation-status appendix — `Status:` callout extraction in both spellings (blockquote and bare paragraph), nearest-heading attribution, generated-file header, idempotence, POSIX-form chapter paths, and count parity against an independent live scan of `spec/` |
| `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` | 62 | 798 | 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` | 103 | 1,151 | `check_doc_counts.py`'s pure per-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), HISTORY version-row format (issue-link limit, ` — ` separator rejection, dateless-row and prose exemption, line-number reporting), the TESTING.md tests breakdown (parts summing to the collected total, a self-consistent-but-stale row, and the reworded-row error), and vera/README.md's Test Suite counts (all four checked independently — mutation-validated by dropping each citation in turn — plus the reworded-paragraph error, a thousands-separator case pinning that every one of the four counts is read comma-tolerantly, and the two section-anchoring cases — a reworded paragraph with decoy counts in a later section, and a renamed heading, both of which must fail loud rather than match across the section boundary).  The reworded case is a test in its own right for both new checks: a pattern that matches nothing must be an error, or rewording the sentence silently switches the gate off.  Also the release count (README's status line and HISTORY's total against each other and against `git tag`: the matching case, the one-ahead release cut that `release.yml` has not tagged yet, that +1 being the ONLY slack once the version is tagged, the two-behind drift that actually shipped, per-document reporting, and a tagless checkout standing the oracle down without standing down the cross-check), plus the tag reader itself against real repositories built in `tmp_path` — release tags read, `nightly`/`-rc1` not counted as releases, and both no-evidence answers (`None` rather than `[]`, since an empty list would read as zero releases and make every documented count wrong) for a tagless checkout and a directory that is not a repository at all.  CONTRIBUTING.md's pre-commit hook count is checked the same way, reworded-sentence case included; and the CI-pipeline lint row against `ci.yml`'s lint job — a matching row, a step present in CI but absent from the row (the drift that shipped), a row entry CI no longer runs, the same set in a different order, a reworded row and a renamed job (both errors, not skips), that only the lint job is read rather than the whole workflow, and the shipped pair both clean and red with one entry dropped).  Also `check_faq_example_count` (#1346), which reads FAQ.md's by-the-numbers example bullet: the page's conformance bullet was pinned first and its test bullet only after that one had drifted through two releases, so the example bullet is pinned rather than left as the third instance of one lesson.  Its cells are all about ANCHORING, because an unanchored search reads whichever occurrence comes first and reports the page consistent while the bullet itself is stale — a decoy phrase carrying the right count in prose above the list, a duplicate bullet (two answers, and the check cannot say which one a reader believes), an inline mention, and an indented sub-bullet; each reddens if the anchor is dropped, and a reworded bullet is an error rather than a skip for the same reason as the checks above |
| `test_grammar_alignment.py` | 91 | 753 | `check_grammar_alignment.py` gate ([#683](https://github.com/aallan/vera/issues/683)): both extractors (Lark headers with the `?`/`!`/`_` markers stripped, template parameters and rule priorities tolerated, and `-> alias` names deliberately not collected; spec headers from ```ebnf fences only), the allowlist arithmetic in all three directions — unwaived drift, a spent entry both files now have, and an entry whose premise broke — one case per waiver proving the fact it rests on is actually checked, the name-deleted-from-both-files case that must not read as agreement, a mutation restoring the spec's old `assert_stmt` name, non-vacuous extraction, and the false positive the issue itself rested on: `qualified_call` and `module_call` are spec headers Lark expresses as aliases, and must never be reported as drift. Three pin the premise checks against ways they used to pass vacuously: an alias surviving only inside a `//` comment must not hold its waiver up, an alias that moved to another rule must fail the waiver naming `fn_call`, and a spent waiver whose premise also broke must yield one instruction rather than two opposite ones |
| `test_check_examples_run.py` | 79 | 1,315 | `check_examples_run.py`, the harness gate that RUNS the examples.  Five separable parts, each in both directions.  **The coverage rule** — the shipped tables cover the shipped corpus exactly, and an unclassified example, a stale `RUN_SPECS` or `SKIPS` key whose file is gone, a name in both tables, and a skip citing an undocumented property are each an error; the empty corpus is an error too, since a glob that stops matching would otherwise report success over zero programs.  Plus the specs' own well-formedness: every named entry point is `public` in its example, every no-main example pins one (or `vera run` would fall back to an arbitrary first export), and no skip property is unused.  **The runner** — a seeded `tmp_path` corpus proves it goes red on a program that type-checks and compiles but traps at run time, green on one that does not, and reports only the broken member of a mixed pair; a fixture whose first export is clean and whose named one traps proves `spec.fn` is actually honoured rather than ignored; a writer program proves each run gets a scratch working directory, so a gate run leaves nothing beside the examples.  **The TESTING.md cross-check** — missing row, extra row, rename (reported naming both sides), wrong disposition and wrong skip property are errors, the parse stops at the next heading so a row-shaped line in a later section is not swept in, and both a reworded heading and a heading whose table has vanished fail loud rather than finding nothing to compare.  **The output signal** -- the second half of the two-signal discipline `check_examples.py` established: the fallback note that `vera run` prints when it cannot use the named entry point is a failure even at exit 0, an absent `expect` sentinel is a failure even at exit 0, and a spec without one asserts nothing about output; end to end, a privatised `main` and a program that completed down a graceful arm each go red, and the same program passes once its own output is the sentinel, so the check reads the output rather than always failing.  Which specs must carry a sentinel is **derived** from what each example declares — a resource effect in a function's effect row, or a call to a resource operation, both validated against the live effect registry so a renamed effect or op fails loudly — and asserted equal to the specs that have one, in both directions; the previous hard-coded triple could not see a fourth such example arriving without one.  The runner's use of BOTH streams is pinned structurally -- `vera run` writes the note to stderr and nothing there on a clean exit, so no fixture can distinguish reading both streams from reading stdout alone, and a tripwire wired to the wrong stream is no tripwire.  Also the hermetic-environment property: an ambient `VERA_DB_URL` or provider key is stripped so a gate run cannot be pointed at a real database or turned into a billed API call, a fixture spec puts its own URL back, and every neutralised name is checked to be one `vera/runtime/` actually reads |
| `test_check_corpus_differential.py` | 52 | 895 | `check_corpus_differential.py`, the burndown instrument that compiles the corpus at two revisions.  The pure pieces only — the real two-revision run costs minutes and is not a test.  **Classification**, all four verdicts: identical, WAT differs, and each one-sided compile failure as its own kind, since a compilability reversal reported as a text difference is the mis-description the instrument exists to avoid; failing at both revisions is not a mover and is counted separately, so a green run states how much of it was vacuous.  **Enumeration** — recursive, keyed by repo-relative POSIX path, and an empty corpus is an error rather than a clean run over nothing.  **The canary** — each side must import the compiler it was pointed at, so a side silently resolving to the venv's editable install cannot compare a revision against itself; an import failure and a foreign compiler are different messages.  **Reporting** — every mover named with its reason, the exit code, the `--json` shape, and a program missing from one side reported rather than dropped.  One test asserts the instrument is absent from `.pre-commit-config.yaml`, so the docstring's claim cannot rot |
| `test_check_editor_grammars.py` | 20 | 249 | `check_editor_grammars.py` gate ([#1156](https://github.com/aallan/vera/issues/1156)): the registry read (every effect in, every ability out, and the four names the grammars actually drifted on present so the set checked is non-vacuous), the word-boundary presence test across all three grammar formats (JSON, plist XML, Vim keyword list) including the prefix pair `Http`/`HttpServer` in both directions, the deliberate comment-mention false pass, a metacharacter pair that only passes when the name is matched literally (`A.B` present, `A0B` not), and the empty registry; the gate's primary path end to end — a listed grammar with an effect stripped out, and a listed README with one stripped out of its prose bullet, each red against an otherwise-clean mirrored tree; the completeness guard — a grammar discovered under `editors/` but absent from `GRAMMARS` fails that same tree, over three discovery routes (`.el` outside a syntax directory, a tree-sitter `.scm` query set, a `.tmLanguage.json` filed anywhere but `syntaxes/`); and the registry's provenance, run as a subprocess against a throwaway checkout whose `vera` package names an effect the grammars do not, which is the only way to see that the list comes from the tree being checked rather than from site-packages.  The shipped grammars and READMEs are currently clean |
| `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` | 13 | 233 | `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` | 98 | 3,255 | 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`), plus `host_error` from `_classify_host_error` on `execute()`'s non-`Trap` branch, `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; plus the host-callback surface suite **`TestHostCallbackErrorSurface1302`** / **`TestClassifyHostError1302`** ([#1302](https://github.com/aallan/vera/issues/1302)) — `execute()` classified on the exception's TYPE NAME (`Trap` / `WasmtimeError`), so a host import raising an ordinary Python exception skipped the conversion and escaped as a 63-line interpreter traceback with the captured streams dropped, and in `--json` mode with no envelope emitted at all.  The conversion is now keyed on the BOUNDARY (everything escaping the guest invocation), and the suite drives a real `json_stringify(JNumber(nan()))` program through all three surfaces: `execute()` raising a `WasmTrapError` of `kind="host_error"` carrying the host's sentence, the pre-failure stdout and the original exception as `__cause__`; text-mode `cmd_run` asserted on the ABSENCE of `Traceback` / `File "` / `wasmtime` and a sub-ten-line diagnostic, since asserting only that the sentence appears would still pass on the pre-fix output where it was the traceback's last line; and JSON-mode `cmd_run` producing a parseable envelope with `trap_kind`, an always-present empty `fix`, `frames`, and the captured `stdout`.  **`TestHostErrorDebugKnob1302`** covers the escape hatch the conversion needs — `VERA_DEBUG_HOST_ERRORS` (ENVIRONMENT.md) re-raises the original exception so a binding bug stays diagnosable — as a deliberate pair, one test proving the knob does something and one proving its absence is what produces the one-liner, since neither alone distinguishes a working knob from unconditional behaviour, plus the truthiness table shared with `VERA_EAGER_GC` and an end-to-end `cmd_run` case |
| `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` | 275 | 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 174 run-level conformance programs driven under both targets, byte-identical stdout/stderr required — 122 are dual-tested and 52 skip *loudly* rather than passing silently: 45 whose compiled WAT imports a host family outside `IO`/`Random` (`state`, `map`, `json`, `set`, `decimal`, `html`, `md`, `regex`, `db`), 6 with no public zero-argument `main`, and 1 calling a nondeterministic op.  The excluded set is defined by those three properties rather than by a filename list, so it stays accurate as programs are added); 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 244 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 | 50 |
| `verify` | Type-checks and all contracts verified by Z3 | 20 |
| `run` | Compiles to WASM and executes correctly | 174 |

Almost all programs are at the `run` level — they compile and execute, producing correct results. Fifty 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_reserved_contextual_keyword_fn_rejected`, `ch05_reserved_resume_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_ambiguous_import_adt_lib_bool`, `ch08_ambiguous_import_adt_lib_int`, `ch08_ambiguous_import_adt_rejected`, `ch08_ambiguous_import_adt_swapped_rejected`, `ch08_ambiguous_import_lib_bool`, `ch08_ambiguous_import_lib_int`, `ch08_ambiguous_import_rejected`, `ch08_ambiguous_import_swapped_rejected`, `ch08_circular_import`, `ch08_cross_module_generic_lib`, `ch08_module_generic_diamond_base`, `ch08_module_prelude_adt_contention_rejected`, `ch08_reserved_vera_prefix_rejected`, `ch08_reserved_vera_prefix_reference_rejected`, `ch08_reserved_vera_prefix_binder_rejected`, `ch08_reserved_vera_prefix_effect_rejected`, `ch08_reserved_vera_prefix_ability_rejected`, `ch08_reserved_vera_prefix_constructor_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`, `ch02_alias_cycle_rejected`) are at the `check` level. Thirty-seven 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_reserved_contextual_keyword_fn_rejected`, `ch05_reserved_resume_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_ambiguous_import_adt_rejected`, `ch08_ambiguous_import_adt_swapped_rejected`, `ch08_ambiguous_import_rejected`, `ch08_ambiguous_import_swapped_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_reserved_vera_prefix_reference_rejected`, `ch08_reserved_vera_prefix_binder_rejected`, `ch08_reserved_vera_prefix_effect_rejected`, `ch08_reserved_vera_prefix_ability_rejected`, `ch08_reserved_vera_prefix_constructor_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`, `ch07_handler_state_type_mismatch_rejected`, and `ch02_alias_cycle_rejected` — are **negative tests** that assert a specific diagnostic (E206, E135, E183, E201, E127, E153, E153, E153, E153, E130, E130, E174, E182, E217, E156, E156, E155, E155, E011, E154, E154, E154, E154, E154, E154, E150, E152, E151, E242, E243, E207, E208, E208, E209, E128, E336, and E132 respectively) via the manifest's `expected_error` field.  One more — `ch08_module_prelude_adt_contention_rejected` — is a negative at the `compile` stage rather than at `check`: it carries `expected_error_stage: "compile"` beside `expected_error: E621`, so the harness asserts it type-checks CLEANLY and is then refused by `vera compile` with that code, which is the property a codegen-phase diagnostic exists for.  `ch09_http` and `ch09_inference` are environment-gated (network / API key). Twenty 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_invisible_import_op_name_lib`, `ch07_io_read_char`, `ch07_io_sleep`, `ch07_random_effect`, `ch08_state_alias_module_table_lib`, `ch08_module_generic_diamond_mid1`, `ch08_module_generic_diamond_mid2`, `ch08_state_alias_per_module_lib`, `ch08_transitive_module_import_mid`, `ch09_http_server`, `ch09_invisible_import_ability_op_lib`, `ch09_math_builtins`, `ch09_nested_helper_family_op_name_lib`) are at the `verify` level, using Z3-provable contracts — a library module is pinned at the deepest level it reaches, so the two per-module alias-table libraries are verified rather than only checked.

### Skipped tests

`pytest tests/ -v` skips 120 conformance-stage tests, and every one of them is the level rule: a program declared at `check` skips its `verify` and `run` stages, one declared at `verify` skips its `run` — 50 × 2 + 20, which is what the suite reports.  The two tables below split those 120 by why the program sits at its level, not by how it skipped: 116 are pinned there by the feature under test, and 4 by an environment CI does not have.  Each skip is listed once; the tables do not overlap.  (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_alias_cycle_rejected]` | `ch02_alias_cycle_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E132`): verify stage not run |
| `test_run[ch02_alias_cycle_rejected]` | `ch02_alias_cycle_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `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_run[ch07_invisible_import_op_name_lib]` | `ch07_invisible_import_op_name_lib.vera` | `verify` | `run` | `verify`-level programs don't get a `run` test |
| `test_run[ch08_module_generic_diamond_mid1]` | `ch08_module_generic_diamond_mid1.vera` | `verify` | `run` | `verify`-level programs don't get a `run` test |
| `test_run[ch08_module_generic_diamond_mid2]` | `ch08_module_generic_diamond_mid2.vera` | `verify` | `run` | `verify`-level programs don't get a `run` test |
| `test_run[ch09_invisible_import_ability_op_lib]` | `ch09_invisible_import_ability_op_lib.vera` | `verify` | `run` | `verify`-level programs don't get a `run` test |
| `test_run[ch09_nested_helper_family_op_name_lib]` | `ch09_nested_helper_family_op_name_lib.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_reserved_contextual_keyword_fn_rejected]` | `ch05_reserved_contextual_keyword_fn_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E153`): verify stage not run |
| `test_run[ch05_reserved_contextual_keyword_fn_rejected]` | `ch05_reserved_contextual_keyword_fn_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_verify[ch05_reserved_resume_fn_rejected]` | `ch05_reserved_resume_fn_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E153`): verify stage not run |
| `test_run[ch05_reserved_resume_fn_rejected]` | `ch05_reserved_resume_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_module_prelude_adt_contention_rejected]` | `ch08_module_prelude_adt_contention_rejected.vera` | `check` | `verify` | `compile`-stage negative test (`expected_error: E621`, `expected_error_stage: compile`): verify stage not run |
| `test_run[ch08_module_prelude_adt_contention_rejected]` | `ch08_module_prelude_adt_contention_rejected.vera` | `check` | `run` | `compile`-stage 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_reserved_vera_prefix_reference_rejected]` | `ch08_reserved_vera_prefix_reference_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E154`): verify stage not run |
| `test_run[ch08_reserved_vera_prefix_reference_rejected]` | `ch08_reserved_vera_prefix_reference_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_verify[ch08_reserved_vera_prefix_binder_rejected]` | `ch08_reserved_vera_prefix_binder_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E154`): verify stage not run |
| `test_run[ch08_reserved_vera_prefix_binder_rejected]` | `ch08_reserved_vera_prefix_binder_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_verify[ch08_reserved_vera_prefix_effect_rejected]` | `ch08_reserved_vera_prefix_effect_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E154`): verify stage not run |
| `test_run[ch08_reserved_vera_prefix_effect_rejected]` | `ch08_reserved_vera_prefix_effect_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_verify[ch08_reserved_vera_prefix_ability_rejected]` | `ch08_reserved_vera_prefix_ability_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E154`): verify stage not run |
| `test_run[ch08_reserved_vera_prefix_ability_rejected]` | `ch08_reserved_vera_prefix_ability_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_verify[ch08_reserved_vera_prefix_constructor_rejected]` | `ch08_reserved_vera_prefix_constructor_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E154`): verify stage not run |
| `test_run[ch08_reserved_vera_prefix_constructor_rejected]` | `ch08_reserved_vera_prefix_constructor_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_verify[ch08_ambiguous_import_rejected]` | `ch08_ambiguous_import_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E155`): verify stage not run |
| `test_run[ch08_ambiguous_import_rejected]` | `ch08_ambiguous_import_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_verify[ch08_ambiguous_import_swapped_rejected]` | `ch08_ambiguous_import_swapped_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E155`): verify stage not run |
| `test_run[ch08_ambiguous_import_swapped_rejected]` | `ch08_ambiguous_import_swapped_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_verify[ch08_ambiguous_import_adt_lib_int]` | `ch08_ambiguous_import_adt_lib_int.vera` | `check` | `verify` | `check`-level library module: verify stage not run |
| `test_run[ch08_ambiguous_import_adt_lib_int]` | `ch08_ambiguous_import_adt_lib_int.vera` | `check` | `run` | `check`-level library module: no standalone `main` |
| `test_verify[ch08_ambiguous_import_adt_lib_bool]` | `ch08_ambiguous_import_adt_lib_bool.vera` | `check` | `verify` | `check`-level library module: verify stage not run |
| `test_run[ch08_ambiguous_import_adt_lib_bool]` | `ch08_ambiguous_import_adt_lib_bool.vera` | `check` | `run` | `check`-level library module: no standalone `main` |
| `test_verify[ch08_ambiguous_import_adt_rejected]` | `ch08_ambiguous_import_adt_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E156`): verify stage not run |
| `test_run[ch08_ambiguous_import_adt_rejected]` | `ch08_ambiguous_import_adt_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_verify[ch08_ambiguous_import_adt_swapped_rejected]` | `ch08_ambiguous_import_adt_swapped_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E156`): verify stage not run |
| `test_run[ch08_ambiguous_import_adt_swapped_rejected]` | `ch08_ambiguous_import_adt_swapped_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage |
| `test_verify[ch08_ambiguous_import_lib_int]` | `ch08_ambiguous_import_lib_int.vera` | `check` | `verify` | `check`-level library module: verify stage not run |
| `test_run[ch08_ambiguous_import_lib_int]` | `ch08_ambiguous_import_lib_int.vera` | `check` | `run` | `check`-level library module: no standalone `main` |
| `test_verify[ch08_ambiguous_import_lib_bool]` | `ch08_ambiguous_import_lib_bool.vera` | `check` | `verify` | `check`-level library module: verify stage not run |
| `test_run[ch08_ambiguous_import_lib_bool]` | `ch08_ambiguous_import_lib_bool.vera` | `check` | `run` | `check`-level library module: no standalone `main` |
| `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_module_generic_diamond_base]` | `ch08_module_generic_diamond_base.vera` | `check` | `verify` | `check`-level library module: verify stage not run |
| `test_run[ch08_module_generic_diamond_base]` | `ch08_module_generic_diamond_base.vera` | `check` | `run` | `check`-level library module: no standalone `main` |
| `test_run[ch08_state_alias_module_table_lib]` | `ch08_state_alias_module_table_lib.vera` | `verify` | `run` | `verify`-level programs don't get a `run` test |
| `test_run[ch08_state_alias_per_module_lib]` | `ch08_state_alias_per_module_lib.vera` | `verify` | `run` | `verify`-level programs don't get a `run` test |
| `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
├── ...                        # 244 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 — 1,220 tests: five stages × 244 entries)
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 43 example programs (live sums of `vera verify --json`; regenerate by summing the `verification` block over `examples/*.vera`):

These totals are measured at the DEFAULT per-query Z3 budget of 10,000 ms, with
`VERA_Z3_TIMEOUT_MS` unset and no `--timeout-ms` flag. The budget is part of the
measurement, not a detail of it: an obligation whose proof lands near it is Tier 1
on a fast host and Tier 3 on a slow one, so a re-derived total that disagrees with
the figures below should be checked against the budget before it is treated as
drift ([#1350](https://github.com/aallan/vera/issues/1350)).

| Metric | Value |
|--------|-------|
| **Tier 1 (static)** | 411 obligations — proved automatically by Z3 |
| **Tier 3 (runtime)** | 122 obligations — checked at runtime |
| **Total** | 533 obligations (77.1% 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` 29, `maximum_syntax.vera` 11, `collections.vera` 10, `array_utilities.vera` 9, `nested_closures.vera` 7, `string_utilities.vera` 6), with a long tail of one to five per example across twenty 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 43 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 its own module-level helper functions rather than sharing them through `conftest.py`, which carries only session-scoped fixtures — opt-in JS coverage, and the `VERA_Z3_TIMEOUT_MS` scrub that stops tier assertions inheriting an ambient solver budget, so the ones that do not name a budget of their own measure the default (#1350) — an explicit `timeout_ms=` outranks the environment and was never exposed.  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`; the two `json_parse` accept-domain batteries (#1306 / #1308) share their Vera probe program, its JSON-into-a-Vera-literal escaper, the `OK:` / `ERR:` output protocol and the two integer-overflow boundary constants through `tests/json_domain_helpers.py`, because a reference-host battery and a cross-host one only mean the same thing if they send `json_parse` the same bytes — one mutation of that escaper reddens both, which is the property a second copy would quietly lose;
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`.

`tests/naming_helpers.py` holds one fixture constructor rather than a suite's
shared helpers: `alias_env_from_declarations(decls, base=None)` builds a
`vera.naming.AliasEnv` by walking a parsed program's declarations.  Every
production consumer builds its environment from a namespace it already holds
(the checker and the verifier from a live `TypeEnv`, codegen from its own flat
alias maps), so this walk lives test-side, where it cannot become a second
source of truth for declaration-index assignment.

`tests/module_fixture_helpers.py` cuts across all three suites: it builds the
`ResolvedModule` fixtures the multi-module tests need, and its two functions
are two different things rather than one with an option.  What separates them
is **parse provenance**, not whether a file survives the call — **neither
leaves one on disk, and neither `file_path` can be opened after it returns**.
`resolved_module(path, source)` writes the source to a real temporary file,
parses THAT via `parse_file`, and deletes it before returning: the module keeps
a program that came through the on-disk parse path, under a realistic absolute
path.  `fake_resolved_module(path, source)` parses in memory via `parse_to_ast`
and labels the module `/fake/<path>.vera` — cheaper, and correct wherever the
parse path does not matter; the label is conspicuously synthetic, so a path in
a failure message is recognisable as a fixture's.

Deleting is safe because nothing downstream reopens `file_path`: `compile()`
and the checker work off the parsed program and the in-memory `source` string
and keep the path only as a diagnostic label (PR #664 review).  A test that
needs a module file to EXIST while it runs must write one itself.
`TestModuleFixtureBuilders` in `test_checker_modules.py` pins all of that,
including a cross-module type-check against an already-deleted path.

Both are the canonical implementation of the tempfile, encoding and path rules
in [Test Fixture Conventions](#test-fixture-conventions) below — six files
carried their own copies before #1228, one of which leaked a temp file per
fixture, and a new multi-module test should import from here rather than write
a seventh.

```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 43 example programs in `examples/` is carried through the front of the pipeline by parametrised tests that glob the directory, so a new `.vera` example joins them the moment it lands: parsing (`test_parser.py`), AST transformation (`test_ast.py`), type checking (`test_checker_functions.py`), contract verification (`test_verifier_contracts.py`), and canonical form (`test_formatter.py`).

The back of the pipeline — compilation and execution — is not covered by a directory glob, and is described in full below.

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

### Example execution coverage

An example that parses, type-checks, verifies and compiles can still trap the instant it runs. Six layers cover `examples/`, and only the last three execute anything:

| Layer | Mechanism | Reach |
|-------|-----------|-------|
| Check + verify | `scripts/check_examples.py` | all 43 |
| Canonical form, parse, transform, check, verify | the directory-globbing parametrised tests above | all 43 |
| Compilation to WASM | `scripts/check_e602_clean.py` — it exists to police `[E602]`/`[E604]` silent skips, but it compiles every example with `--json` and treats an `ok: false` envelope as a hard failure, so full compile coverage is real though incidental to the script's name | all 43 |
| Execution under both runtimes | `tests/test_browser.py`, from two explicit lists — `EXAMPLES_WITH_MAIN` (10, compared on stdout) and `FUNCTION_CALL_EXAMPLES` (11 distinct examples, compared on return value) | 21 |
| Execution with pinned output | dedicated tests, each asserting a specific value or rendering (see the table) | 12 |
| Execution asserted trap-free | `scripts/check_examples_run.py` — the harness gate | 35 |

The gate is what makes the set closed. It enumerates `examples/*.vera` from disk and requires every name to be either run or matched to a documented skip property, so **an unclassified example fails the gate** and adding an example forces the author to classify it. The table below is cross-checked against the script's own tables on every run: a row that disagrees, a missing row, or a renamed example is an error, on the same principle as `check_doc_counts.py` — the codebase is the oracle and the documentation must match it.

What the gate asserts is *runs green*, deliberately not *prints what it used to*: output pinning stays in the dedicated tests, which is why `sqlitedb.vera`'s rendered city table and `inference_json.vera`'s score line are pinned there and only trap-freedom here.

Trap-freedom is two signals, not one — the discipline `check_examples.py` already applies, for the same reason. An exit code alone accepts two measured failures. Every spec names its entry point rather than relying on `vera run`'s first-export fallback, because a `main` that is privatised or renamed otherwise runs *some other function* at exit 0. And the three examples that reach outside the process — `sqlitedb.vera` for its committed fixture, `database.vera` for an in-memory database, `file_io.vera` for the filesystem — answer a failure by printing a message and completing normally, so each pins a substring only its success path prints. Deleting `examples/sqlitedb.sqlite` fails the gate on that sentinel rather than passing on the graceful in-memory arm.

| Example | Executed by | Harness gate |
|---------|-------------|--------------|
| `absolute_value.vera` | browser parity (return value); `test_codegen_infrastructure.py` pins three results | runs |
| `array_utilities.vera` | nothing, before the gate | runs |
| `async_futures.vera` | browser parity (stdout) | runs |
| `async_http_fanout.vera` | nothing | skip: network |
| `base64.vera` | browser parity (stdout) | runs |
| `closures.vera` | browser parity (return value); `test_codegen_closures.py` pins 15 and 105 | runs |
| `collections.vera` | nothing, before the gate | runs |
| `database.vera` | nothing, before the gate | runs |
| `effect_handler.vera` | browser parity (stdout + State round-trips); `test_codegen_effects.py` pins six results | runs |
| `ephemeris.vera` | `test_examples_ephemeris.py` pins the full stdout, both geocentric distances, agreement with ERFA to 30″, and the per-function tier statuses — the eccentricity binds verified, `wrap_deg` at Tier 1, the transcendentals exactly `tier3` at a low, the default and a generous budget, `kepler_solve`'s termination proved | runs |
| `factorial.vera` | browser parity (return value); `test_codegen_infrastructure.py` pins 120 | runs |
| `file_io.vera` | browser runtime only, where file IO is a documented `Err` stub; never run natively before the gate | runs |
| `fizzbuzz.vera` | nothing, before the gate | runs |
| `gc_pressure.vera` | browser parity (stdout) | runs |
| `generics.vera` | browser parity (return value); `test_codegen_monomorphize.py` compiles it without running it | runs |
| `hello_world.vera` | browser parity (stdout); `test_codegen_strings.py` pins the greeting | runs |
| `html.vera` | nothing, before the gate | runs |
| `http.vera` | nothing | skip: network |
| `http_server.vera` | `test_wasi_target.py` serves the emitted component under stock `wasmtime serve` and pins three request round-trips | skip: non-scalar-entry |
| `increment.vera` | browser parity (return value + State); `test_codegen_effects.py` | runs |
| `inference.vera` | nothing | skip: api-key |
| `inference_json.vera` | `test_codegen_host_effects.py` pins five score renderings and the bad-response arm against a mocked provider | skip: api-key |
| `io_operations.vera` | nothing | skip: stdin |
| `json.vera` | nothing, before the gate | runs |
| `life.vera` | nothing | skip: long-running |
| `list_ops.vera` | browser parity (return value); `test_codegen_monomorphize.py` pins 60 | runs |
| `markdown.vera` | browser parity (stdout) | runs |
| `maximum_syntax.vera` | nothing, before the gate | runs |
| `modules.vera` | nothing, before the gate | runs |
| `mutual_recursion.vera` | browser parity (return value); `test_codegen_infrastructure.py` pins three results | runs |
| `nested_closures.vera` | nothing, before the gate | runs |
| `pattern_matching.vera` | browser parity (return value) | runs |
| `quantifiers.vera` | browser parity (return value) | runs |
| `read_char.vera` | nothing | skip: stdin |
| `refinement_types.vera` | browser parity (return value) | runs |
| `regex.vera` | browser parity (stdout) | runs |
| `safe_divide.vera` | browser parity (return value + precondition failure); `test_codegen_infrastructure.py` pins the result and the trap | runs |
| `scoreboard.vera` | nothing, before the gate | runs |
| `sqlitedb.vera` | `test_db_runtime.py` pins the rendered city table against the committed fixture | runs |
| `string_ops.vera` | browser parity (stdout) | runs |
| `string_utilities.vera` | nothing, before the gate | runs |
| `url_encoding.vera` | browser parity (stdout) | runs |
| `url_parsing.vera` | browser parity (stdout) | runs |

Seventeen of those examples were executed by nothing at all before the gate. It runs eleven of them; the remaining six are the ones a property excludes. A twelfth example joins them natively — `file_io.vera`, which ran only under the browser runtime, where the file IO it demonstrates is a deliberate `Err` stub.

Each skip cites a property, and the gate prints the property and its reason on every run:

| Property | Examples | Why the harness cannot run it |
|----------|----------|-------------------------------|
| `network` | `async_http_fanout.vera`, `http.vera` | live outbound HTTP, so a run would depend on network reachability and a third party's uptime |
| `api-key` | `inference.vera`, `inference_json.vera` | with a provider key configured the gate would issue a real, billed request; without one it would only exercise the not-configured arm |
| `stdin` | `io_operations.vera`, `read_char.vera` | reads interactive input, so what runs is a property of the invoking terminal |
| `non-scalar-entry` | `http_server.vera` | no `main`, and `handle` takes a `Request` ADT that `vera run` cannot build from CLI arguments |
| `long-running` | `life.vera` | its only public entry point animates 300 generations at 100 ms a frame |

Skipping is for programs the harness structurally cannot drive. An example that *can* be driven and fails is a bug in the compiler or in the example, not a candidate for the skip table.

## 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 26 marker-carrying instances: test_stress.py's 16 (9 logical tests, 7 with an eager-GC twin) + TestHostHandleReclamation573's 10
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@v9` with `issues: write` job-scoped permission.

**Budget**: the workflow's suite — `tests/test_stress.py` per the invocation above; the marker's other 10 instances in `test_codegen_gc_reclamation.py` currently run only under an explicit `pytest -m stress` invocation, since the per-PR suite deselects the marker and this workflow is file-scoped ([#1328](https://github.com/aallan/vera/issues/1328)) — completes in well under the 5-minute target: measured at **0.66s in-process** on a developer laptop on 2026-05-13 for its 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

Footguns in how a fixture is written or run — most cross-platform, from the post-#637 Windows CI rollout (PRs #639/#643/#644/#646) and #1246's, and one about which checkout a suite actually measures.  Each has a workaround that makes the fixture portable across Linux / macOS / Windows.  This section is the one place they are stated; for the specific job of building a `ResolvedModule` fixture, `tests/module_fixture_helpers.py` applies all of them and is what a multi-module test should import (#1228).

### Running against ANOTHER checkout: the argument decides, not `PYTHONPATH`

To measure a test file against a different revision — a baseline worktree, to
prove a new cell is red before a fix — it is not enough to set `PYTHONPATH` to
that checkout and pass the test file by path:

```bash
# WRONG — silently measures the CURRENT checkout
cd /path/to/baseline
PYTHONPATH=/path/to/baseline pytest /path/to/current/tests/test_x.py
```

pytest resolves its rootdir from the ARGUMENTS, finds the current checkout's
`pyproject.toml`, and inserts that directory at `sys.path[0]` — ahead of
`PYTHONPATH`.  `import vera` then loads the tree the file came from, so the
"baseline" run exercises the code under test and passes.  Nothing warns; the
run simply proves the opposite of what it appears to.

```bash
# RIGHT — copy the file in, so rootdir and sys.path[0] are the baseline.
# The SOURCE path is absolute: a relative one resolves against whatever
# directory you are in, and the block above has already left you in the
# baseline — where it would copy the file over itself and measure nothing.
cp /path/to/current/tests/test_x.py /path/to/baseline/tests/
cd /path/to/baseline && pytest tests/test_x.py
```

The same trap has a second form, and it is the one most people meet first:
for `python -c` and `python -m`, `sys.path[0]` is the process's CWD, so those
invocations follow the directory you are standing in and ignore a `PYTHONPATH`
that points elsewhere — including the canary below, which is why the canary
must be run from the tree you mean to measure.

Assert the canary rather than trusting it: `python -c "import vera;
print(vera.__file__)"`, run from the baseline directory, must name the
baseline.  A red-proof is worth exactly as much as the certainty about which
compiler produced it.

### 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.

**Corollary — the cleanup must be sequenced, not just present.** `delete=False` means the file outlives its `with`, so a failure *inside* the block leaves it behind and the fixture needs its own cleanup. It is tempting to put that in an `except` next to the write — but Windows cannot delete a file whose handle is still open, so an unlink there is `PermissionError` (WinError 32) rather than a cleanup. Both rules are satisfied by capturing the name first, letting the `with` close the handle on its way out however it leaves, and unlinking once afterwards:

```python
# Wrong — cleans up on failure, but while the handle is still open:
with tempfile.NamedTemporaryFile(mode="w", delete=False, encoding="utf-8") as f:
    fp = f.name
    try:
        f.write(source)
    except BaseException:
        os.unlink(fp)          # WinError 32 on Windows
        raise

# Right — one cleanup site, after the handle is closed, on every path:
tmp = tempfile.NamedTemporaryFile(mode="w", delete=False, encoding="utf-8")
fp = tmp.name
try:
    with tmp as f:             # closes the handle however this block exits
        f.write(source)
    ...
finally:
    Path(fp).unlink(missing_ok=True)
```

The ordering is observable without a Windows machine — record whether the handle is closed at the moment each unlink is issued — which is how `TestModuleFixtureBuilders::test_the_handle_is_closed_before_every_unlink` pins it on every platform.  Surfaced by #1228's leak fix, which was green on POSIX and red on all three Windows cells.

### 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.

### Repo-relative paths COMPARED as strings must be POSIX form

The rule above is about a path *embedded in Vera source*; this one is about a path used as a **key**.  `str(path.relative_to(ROOT))` renders `tests\conformance\x.vera` on Windows, so any later `startswith("tests/conformance/")`, `"examples/" in origin`, or dict lookup against a POSIX-spelled literal matches **nothing** — and matching nothing is silent.  A filter that classifies zero files does not raise; it reports an empty population, which reads as "the thing you were counting shrank", not "your comparison is broken".  It is also invisible to a local hook run, because macOS and Linux satisfy the POSIX spelling.

```python
# Wrong — the string is native-separator, so every POSIX prefix misses on Windows:
origin = str(path.relative_to(ROOT))
maintained = [o for o in origins if o.startswith("examples/")]   # [] on Windows

# Right — POSIX by construction, at the point the path becomes a string:
origin = path.relative_to(ROOT).as_posix()
```

Do the conversion where the string is *created*, not at each comparison: one `as_posix()` makes the property hold for every consumer, where a per-comparison fix has to be remembered by each new one.  `Path.parts` tuples are an equally portable alternative when you are matching whole segments rather than a prefix.

Surfaced via `tests/test_slot_naming_differential.py::test_corpus_is_almost_entirely_parseable`, which re-anchored its floor on the maintained corpus (`examples/` + `tests/conformance/`) and went red on all three Windows cells with `AssertionError: (0, 428)` — the walk had collected all 428 files, and the *classification* matched none of them.  That test now also asserts no origin contains a backslash, so the regression names its own cause.

### A path a converter RETURNED must not be asserted by its POSIX shape

The two rules above are about paths the test *constructs* — embedded into Vera source, or compared as a repo-relative key.  This is their assertion-side twin: a path handed back by a standard-library converter is in the **platform's** spelling, so pinning it against a literal `/`-shaped string passes on Linux and macOS and fails on all three Windows cells.  `urllib.request.url2pathname("/tmp/x.vera")` is `/tmp/x.vera` on POSIX and `\tmp\x.vera` on Windows; `url2pathname("/")` is `/` and `\`.  The POSIX cells greening proves nothing about the Windows ones, which is what makes this class of assertion easy to write and impossible to notice locally.

Assert the **property**, relationally, so no shape is named:

```python
# Wrong — a POSIX shape, so red on every Windows cell:
assert uri_to_path("FILE:///tmp/x.vera") == "/tmp/x.vera"
assert uri_to_path("file:///") == "/"

# Right — case-insensitivity is "every spelling gives the same answer as
# the lowercase one", and the inequality keeps three non-conversions from
# satisfying it by all agreeing:
lowercase = uri_to_path("file:///tmp/x.vera")
assert uri_to_path("FILE:///tmp/x.vera") == lowercase
assert uri_to_path("FILE:///tmp/x.vera") != "FILE:///tmp/x.vera"

# Right — "is a root" holds of `/` and `\` alike:
root = Path(uri_to_path("file:///"))
assert root.name == "" and root.parent == root
```

Assertions that compare against a path the test itself built (`str(tmp_path / "x.vera")`, or a round-trip through `Path.as_uri()`) are already portable — the expected value is in the same spelling as the actual.  So are assertions that the INPUT comes back unchanged, which is how the opaque/pass-through cases are pinned.  Surfaced by `tests/test_lsp.py::TestUriToPath` (#1246), where two of nine assertions named a shape and seven did not.

### 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.

### Evidence about temp files must name them, not sweep a shared directory

CI runs `pytest -v -n auto`, so several xdist workers build fixtures at the same time, each creating its own `tmp*.vera` in the **one** system temp directory.  A test that asserts over the *contents* of that directory is therefore reading other workers' files, and a sibling's fixture that lives for the microseconds between the snapshot and the assertion reads as litter this test left:

```python
# Wrong — the evidence set includes every worker's files:
pattern = str(Path(tempfile.gettempdir()) / "*.vera")
before = set(glob.glob(pattern))
...
assert set(glob.glob(pattern)) - before == set()

# Right — the evidence is the path THIS call created:
created: list[str] = []
monkeypatch.setattr(helpers.tempfile, "NamedTemporaryFile", recording_ntf)
...
assert len(created) == 1, created          # else the check is vacuous
assert [n for n in created if Path(n).exists()] == []
```

The sweep form was flaky rather than wrong: it passed for a whole PR and then failed on the v0.1.10 release push over a `C:\...\tmp*.vera` on worker gw1, an hour after the identical tree passed (~33% reproducible on macOS under a second writer).  Capturing the name removes the race instead of relocating it — no shared directory is read at all — and a `len(...) == 1` guard keeps it from passing vacuously if the builder stops creating its file that way.  Redirecting `TMPDIR`/`TEMP`/`TMP` at a private directory is the other cure, but it costs an env triple plus a reset of `tempfile.tempdir` (which caches the resolved directory, so the env alone changes nothing) and still asserts over a directory rather than a file.

## 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`)
5a. **New multi-module test (any suite):** Build the imported modules with `resolved_module()` / `fake_resolved_module()` from `tests/module_fixture_helpers.py` — never a local tempfile copy
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-nine 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 244 conformance entries hold at their declared level (parse/check/verify/run) — positives pass; the negatives fail at the stage their `expected_error_stage` names (`check` by default, or `compile`, which also asserts the program type-checks cleanly) with their `expected_error` E-code |
| `check_examples.py` | All 43 `.vera` examples pass `vera check` + `vera verify` |
| `check_corpus_canonical.py` | All 294 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_debruijn_examples.py` | All Vera code blocks in DE_BRUIJN.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` | The same version in five files: `pyproject.toml`, `vera/__init__.py`, `docs/index.html` (the badge, whose URL and link text are checked separately), `README.md`'s "active development at vX.Y.Z", and `uv.lock`'s editable `veralang` entry.  It does NOT read `CHANGELOG.md` — the matching `## [X.Y.Z]` section is a separate requirement, enforced by the changelog gate and the release workflow |
| `check_doc_counts.py` | A fixed set of *named* citations match the live codebase — not every number in the docs. Filesystem-derived counts (conformance programs, examples, test files, pre-commit hooks, CI jobs, corpus programs, releases against `git tag`) and pytest-collection counts (suite total, per-file test and line counts) where TESTING.md, CONTRIBUTING.md, CLAUDE.md, README.md, SKILL.md, AGENTS.md, FAQ.md and ROADMAP.md cite them; TESTING.md's passed/stress/skipped breakdown against the collected total and its conformance skip total against its own table; `vera/README.md`'s module map and its Test Suite paragraph's four counts; the landing-page facts (#528); KNOWN_ISSUES refactoring counts within ±10%; HISTORY version-row format; and the CI-pipeline lint row enumerating exactly the scripts `ci.yml`'s lint job runs, in its order. Each is keyed to the sentence that carries it, so a reworded citation is an error rather than a silent skip — but a count in prose the script does not name is not read at all, and hand-written program lists (such as the conformance-level lists in this document) are outside its scope entirely. CHANGELOG.md is excluded deliberately: its counts are frozen historical snapshots |
| `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_explicit_encoding.py` | Every text-mode `open()` / `read_text()` / `write_text()`, `subprocess.run/Popen/check_output` text capture, and text-mode `tempfile.NamedTemporaryFile` under `vera/`, `scripts/` and `tests/` passes an explicit `encoding="utf-8"`; `# encoding-exempt: <reason>` opts a deliberate non-UTF-8 site out (#645) |
| `check_e602_clean.py` | No unexpected E602/E604 silent-skip sites outside the explicit allowlist |
| `check_examples_run.py` | Every `examples/*.vera` either runs trap-free under the native runtime or carries a documented skip property.  Two signals, as in `check_examples.py`: the exit code, and an output signal — every spec names its entry point (so a privatised or renamed `main` exits 1 instead of silently running another export) and every example that declares a resource effect or calls a resource operation pins a success sentinel (so a vanished fixture fails rather than passing on a graceful arm), the set being derived from those declarations rather than named.  An unclassified example is an error, and TESTING.md's execution-coverage table must match the script's own classification |
| `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_grammar_alignment.py` | Every rule header in `spec/10-grammar.md`'s EBNF has a same-named rule in `vera/grammar.lark`, and the reverse ([#683](https://github.com/aallan/vera/issues/683)); every terminal is declared and referenced within its own file, every regex-bodied terminal carries the same pattern in both, and each shared production's right-hand side refers to the same rules and terminals ([#1290](https://github.com/aallan/vera/issues/1290)).  The *shape* of a right-hand side — alternation, grouping, repetition — is still not compared |
| `check_editor_grammars.py` | Every editor grammar under `editors/` (vscode, TextMate, Vim), and the two extension READMEs that repeat the list in prose, carries every built-in effect name from the live registry — read from the checked-out tree, not from whatever `vera` is importable.  Word-boundary presence: absence is conclusive, presence is optimistic — the observed failure is omission.  A completeness guard fails any grammar discovered under `editors/` that the checked list doesn't name ([#1156](https://github.com/aallan/vera/issues/1156)) |
| `check_distribution.py` | The built wheel and sdist carry the project's own name and version, ship the files the installed package needs plus a packaged LICENSE, and exclude `tests/` and generated Python files |
| `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 |

Each runs in its configured pre-commit hook or CI job, so issues are caught locally before they reach the remote; `build_site.py` is the generator whose output `check_site_assets.py` verifies.

One script is deliberately outside that set. `check_corpus_differential.py` compiles every corpus program at two revisions and reports the ones whose WAT moved, including the ones that compile on only one side — the measurement behind a "codegen is unchanged" claim, and the scope list when output is meant to change. It costs minutes rather than milliseconds, so it is a burndown instrument run by hand (`--base-ref origin/main`), not a hook and not a CI gate; a test asserts its absence from `.pre-commit-config.yaml` so that claim cannot rot. `check_doc_counts.py --check-bug-issues` is opt-in for the same kind of reason — it needs the GitHub API, which a commit hook must not — and belongs to the release PR (see `RELEASING.md`).

### 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

The repository configures 36 hooks across two stages: 34 run at the commit stage (after `pre-commit install`), and 2 (`check-changelog-updated`, `uv-lock-check`) run 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 244 conformance entries hold at their declared level — positives pass; negatives fail at the stage their `expected_error_stage` names (`check` or `compile`) with their `expected_error` E-code |
| `check_examples.py` | All 43 examples pass `vera check` + `vera verify` |
| `check_corpus_canonical.py` | All 294 `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_debruijn_examples.py` | DE_BRUIJN.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_grammar_alignment.py` | Spec EBNF and Lark grammar agree on every rule name ([#683](https://github.com/aallan/vera/issues/683)), every terminal, and the symbols each shared production refers to ([#1290](https://github.com/aallan/vera/issues/1290)) |
| `check_editor_grammars.py` | Every editor grammar under `editors/`, and the two extension READMEs, carry every built-in effect name from the live registry ([#1156](https://github.com/aallan/vera/issues/1156)) |
| `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_examples_run.py` | Every example runs trap-free (exit code plus an output signal) or carries a documented skip property, and TESTING.md's execution-coverage table matches |
| `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 matches the Python runtime across the surface the two share |
| `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 -- each fires only when files matching its own `files:` pattern in `.pre-commit-config.yaml` change, so that file is the authority on any given hook's trigger set. The common patterns are `.vera` sources, `vera/**/*.py`, `grammar.lark`, and the Markdown file a doc gate reads; narrower ones exist too, such as `editors/*` for the editor-grammar gate and `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_grammar_alignment.py`, `check_readme_examples.py`, `check_skill_examples.py`, `check_faq_examples.py`, `check_debruijn_examples.py`, `check_pypi_readme_examples.py`, `check_html_examples.py`, `check_doc_builtin_shadowing.py`, `check_e602_clean.py`, `check_examples_run.py`, `check_editor_grammars.py`, `check_diagnostic_fields.py`, `check_explicit_encoding.py`, `check_site_assets.py`, `check_licenses.py`, `check_doc_counts.py`, `check_limitations_sync.py`, `ruff check .`, `ruff check --select S vera/` (security rules), `uv lock --check` |
| **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` — checks all installed packages against the OSV vulnerability database (skips the local editable `vera` package) |
| **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 |
| **package-distribution** | Python 3.12 x Ubuntu | `python -m build`, `twine check dist/*`, and `python scripts/check_distribution.py dist` on the artifacts that will ship under the `veralang` name, then a wheel smoke-test: install `dist/*.whl` into a fresh venv outside the checkout and run `vera version` / `vera check` / `vera run` over `hello_world.vera`. PR CI validates the archives and publishes nothing (#737) |
| **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, 87% JavaScript** — matching the overview table above. The two are reported as two figures and never blended into one: they come from different collectors over different line populations (`pytest --cov` over the Python compiler, V8 over `vera/browser/`), so a combined percentage would need a line-weighted total that neither report produces. 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`. Action refs are pinned to major-version tags (`actions/checkout@v7`), with two exceptions pinned to full commit SHAs: `pypa/gh-action-pypi-publish` (the Trusted Publishing step, which holds the `pypi` environment's credentials) and `codecov/codecov-action` (a third-party uploader that runs with the repository checkout). Each SHA carries the tag it corresponds to in a trailing comment.

## Open CI/Tooling Issues

Tracked improvements to the testing and CI infrastructure:

| Issue | Description |
|-------|-------------|
| [#1295](https://github.com/aallan/vera/issues/1295) | Decide whether the four abilities (`Eq`/`Hash`/`Ord`/`Show`) highlight distinctly from ordinary types in the editor grammars |
| [#1103](https://github.com/aallan/vera/issues/1103) | Migrate GitHub Pages off legacy branch-deploy to a self-owned Actions workflow |
| [#712](https://github.com/aallan/vera/issues/712) | Watch: Codecov → Harness migration (action / token / endpoint / badge). The JavaScript side is also unasserted today — `codecov.yml` marks both JavaScript statuses `informational: true` with `target: auto` (a comparison against the base commit, not an absolute floor), and the `browser-parity` job uploads `lcov.info` without printing or asserting a percentage, so nothing holds `runtime.mjs` above a threshold the way `pytest --cov` holds the Python side |
| [#540](https://github.com/aallan/vera/issues/540) | Add lychee + markdownlint MD051 for cross-doc anchor validation |
| [#402](https://github.com/aallan/vera/issues/402) | Investigate parser fuzzing with Atheris for crash detection |
| [#386](https://github.com/aallan/vera/issues/386) | Add property-based testing for parser/formatter round-trip |

## 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.