Release v0.1.9

CHANGELOG.md

@@ -6,6 +6,12 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
 
 ## [Unreleased]
 
+## [0.1.9] - 2026-08-04
+
+### Added
+
+- **`scripts/check_doc_counts.py` pins FAQ.md's headline test count.** The "by the numbers" line in FAQ.md carried a total-test figure no gate checked — only the conformance half of the sentence was pinned — and it drifted silently through two releases before being caught by hand both times. The oracle now reads the number the same way it reads README.md's status row, so the next drift fails pre-commit and CI instead of shipping.
+
 ### Fixed
 
 - **`vera run` no longer executes a different function when the entry was dropped** ([#1183](https://github.com/aallan/vera/issues/1183)). When the `[E620]` skip propagation dropped `main` — or an explicit `--fn` target — and any public sibling survived, `execute()` fell through to `result.exports[0]`: the sibling's body ran, its result printed, exit 0, nothing on stderr. A regression of the #1178 review class, and the one outcome the loud-skip design exists to prevent, since the user could not tell the answer came from a different function. A dropped entry is now a refusal: `vera run` exits nonzero and names both the requested function and the root `[E602]`/`[E620]` diagnostic that removed it (`--json` reports `ok: false` with the same text). Auto-selection survives only for the never-declared case — no `main` anywhere in the source — and announces itself with a one-line `Note:` on stderr naming the function it picked, so the choice is never invisible. The `Compilation notes:` block is no longer gated on an empty export list; it prints on every run that has skip/drop diagnostics, which is exactly the case (a surviving sibling) where the user was least likely to notice something went missing. The same review's sibling surfaces are closed alongside: `vera compile` exits nonzero when a program declares a public non-generic function and the module ends up exporting nothing (a file of private helpers, or a cross-module generic library, still compiles clean — neither has an entry point to lose), and `vera compile --target browser` refuses to write a bundle without a `main` export — whether `main` was declared and dropped (the refusal quotes the E620 chain) or never declared at all (it names what is exported instead) — since the generated `index.html` calls `main()` on load either way. `CompileResult` gains `dropped_fns`, mapping each dropped user function to the diagnostic that explains it, so the refusal quotes the root cause rather than re-deriving it.
@@ -35,7 +41,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
 
 - **A function named after a grammar keyword is rejected at the declaration site, `E153`** ([#1187](https://github.com/aallan/vera/issues/1187)). Lark's contextual lexer re-lexes `assert`, `assume`, `forall`, `exists`, `match`, `if`, `let`, `fn`, `true` and `false` as ordinary identifiers after `fn`, so each declares cleanly — and none can be written in expression position, where the spelling is always the keyword: a bare `match(3)` does not parse at all (`[E005]`), and `assert(3)` / `assume(3)` are read as the statement forms and collide (`[E121]` plus `[E172]`/`[E173]`). Every one is a declarable trap, so the reservation refuses the mistake at its source rather than letting it surface as whichever call-site error the spelling happens to produce — the same one-canonical-form rule that already covers the contract state forms ([#1181](https://github.com/aallan/vera/issues/1181)), built-in functions (`E151`) and built-in effects (`E152`). **Breaking**: a module-qualified `mod::match(...)` parses through the module-call rule rather than any keyword rule, so a module export under one of these names was callable cross-module (and only cross-module) — probed on the pre-fix tree, the shape checked and ran. Such an export must be renamed; the breakage is loud and located at the module's declaration.
 
-  `handle` is carved out and stays legal: `public fn handle(@Request -> @Response)` is the entry point the host invokes under `vera serve` and `wasi:http` (spec §9.5.6, `examples/http_server.vera`), so being uncallable from Vera source does not make it dead code. It lives in a named `_HOST_INVOKED_FN_NAMES` set subtracted from the reservation, so a future host-invoked entry point joins it deliberately rather than by editing a flat list. The `E153` rationale branches with the reason — a keyword is not described as a contract state form — while the fix stays "rename" on both. The gate inherits the #1181 shape: top-level, `private` and generic `forall<T>` functions, `where`-helpers, and modules (a module declaring `fn match` surfaces `E153` into its importer, carrying the module's own file path). Matching is on the whole identifier, so `matched` / `letter` / `iffy` stay legal, and `op <keyword>(...)` inside an `effect` block never reaches the gate — the lexer refuses that spelling at parse (`[E005]`), pinned so a grammar change that admits it shows up as a failure to widen. Spec §5.2 states both halves of the rule; new conformance program `ch05_reserved_keyword_fn_rejected` (175, was 174) pins it as an `E153` negative. Mutation-validated: emptying the keyword set flips the ten keyword tests RED with the `old`/`new` tests still green, and emptying the carve-out flips the `handle` control RED (and breaks `examples/http_server.vera` and `ch09_http_server`).
+  `handle` is carved out and stays legal: `public fn handle(@Request -> @Response)` is the entry point the host invokes under `vera serve` and `wasi:http` (spec §9.5.6, `examples/http_server.vera`), so being uncallable from Vera source does not make it dead code. It lives in a named `_HOST_INVOKED_FN_NAMES` set subtracted from the reservation, so a future host-invoked entry point joins it deliberately rather than by editing a flat list. The `E153` rationale branches with the reason — a keyword is not described as a contract state form — while the fix stays "rename" on both. The gate inherits the #1181 shape: top-level, `private` and generic `forall<T>` functions, `where`-helpers, and modules (a module declaring `fn match` surfaces `E153` into its importer, carrying the module's own file path). Matching is on the whole identifier, so `matched` / `letter` / `iffy` stay legal, and `op <keyword>(...)` inside an `effect` block never reaches the gate — the lexer refuses that spelling at parse (`[E005]`), pinned so a grammar change that admits it shows up as a failure to widen. Spec §5.2 states both halves of the rule; new conformance program `ch05_reserved_keyword_fn_rejected` (176, was 175) pins it as an `E153` negative. Mutation-validated: emptying the keyword set flips the ten keyword tests RED with the `old`/`new` tests still green, and emptying the carve-out flips the `handle` control RED (and breaks `examples/http_server.vera` and `ch09_http_server`).
 
 - **`Vera`-prefixed type names are reserved for the prelude, `E154`** ([#1184](https://github.com/aallan/vera/issues/1184) review). The prelude's combinators resolve their parameter types through generated declarations in that namespace (`VeraOptionMapFn`; type parameters `VeraA`/`VeraB`, #869), and `inject_prelude` skips any of its declarations whose name a user program already spells — so `type VeraOptionMapFn = Int;` silently re-typed the prelude's own signatures: check-green, then a WebAssembly validation failure at run. Declaring a type or alias whose name begins with `Vera` plus an uppercase letter or digit is now refused at the declaration, with module declarations surfacing the error into their importer as the E151/E152/E153 family does. Ordinary names merely containing the letters (`Veranda`, `MyVeraThing`) are unaffected, and shadowing the *unprefixed* prelude aliases (`OptionMapFn`) remains legal. New conformance program `ch08_reserved_vera_prefix_rejected` (175, was 174) pins the rule.
 
@@ -3194,7 +3200,8 @@ Small docs sweep — closes six aging documentation issues in one PR.  No code c
 - Grammar: handler body simplified to avoid LALR reduce/reduce conflict
 - `pyproject.toml`: corrected build backend, package discovery, PEP 639 compliance
 
-[Unreleased]: https://github.com/aallan/vera/compare/v0.1.8...HEAD
+[Unreleased]: https://github.com/aallan/vera/compare/v0.1.9...HEAD
+[0.1.9]: https://github.com/aallan/vera/compare/v0.1.8...v0.1.9
 [0.1.8]: https://github.com/aallan/vera/compare/v0.1.7...v0.1.8
 [0.1.7]: https://github.com/aallan/vera/compare/v0.1.6...v0.1.7
 [0.1.6]: https://github.com/aallan/vera/compare/v0.1.5...v0.1.6

FAQ.md

@@ -249,7 +249,7 @@ The reference compiler is under active development. The current release includes
 
 - A seven-stage pipeline: parse, transform, resolve, typecheck, verify, compile, execute
 - A 14-chapter formal specification
-- 8,840 tests, including a 176-program conformance suite
+- 8,841 tests, including a 176-program conformance suite
 - 42 working example programs
 - 164 built-in functions covering strings, arrays, math, parsing, and data types
 - Four built-in abilities (Eq, Ord, Hash, Show) with constrained generics and ADT auto-derivation

HISTORY.md

@@ -474,6 +474,7 @@ Stages 19 and 20 run dual-threaded: community PRs against the single-source spri
 | v0.1.6 | 20 Jul | **The comment system** — block comments nest, malformed ones get their own `E02x` diagnostics, annotation labels reach the AST, and `vera fmt` stops deleting comments it had silently dropped since the formatter was written ([#1112](https://github.com/aallan/vera/issues/1112)). |
 | v0.1.7 | 24 Jul | **SQL injection won't compile** — the built-in `<DB>` effect and a literal-provenance checker that makes SQL injection a compile-time error ([#309](https://github.com/aallan/vera/issues/309): `E207`/`E208`/`E209`), plus the bare-effect-op routing check (`E217`) and a Float64 rounding-assertion CI-flake fix. |
 | v0.1.8 | 27 Jul | **Editors and toolchain hygiene** — the VS Code extension reaches the Marketplace, Vim and Neovim gain a package, the ruff rule set is declared rather than inherited with five defect-class rules adopted, and the SQL checker's `E208` follows a `let` chain as `E207` already did ([#1106](https://github.com/aallan/vera/issues/1106)). |
+| v0.1.9 | 4 Aug | **The declarable-trap purge** — the reserved-name family completes: grammar keywords join `old`/`new` under E153 with a named host-invoked carve-out ([#1187](https://github.com/aallan/vera/issues/1187)), built-in effects cannot be redeclared (E152), and `Vera`-prefixed type names are reserved for the prelude (E154). `vera run` refuses a dropped entry instead of executing a sibling, imported functions' diagnostics and trap backtraces name their own module, `decreases` is enforced at run time, and codegen skips propagate to transitive callers with `call_indirect` emitted only when a table exists. |
 
 ---
 
@@ -494,4 +495,4 @@ Ten releases, chosen for the capability each one unlocked rather than even spaci
 | Spec chapters | 7 | 10 | 12 | 13 | 13 | 13 | 13 | 14 | 14 | 14 |
 | Python coverage | — | — | 90% | 96% | 95% | 95% | 95% | 95% | 95% | 95% |
 
-Total: **2,000+ commits, 203 tagged releases, 103 active development days.**
+Total: **2,000+ commits, 205 tagged releases, 103 active development days.**

README.md

@@ -263,7 +263,7 @@ cp /path/to/vera/SKILL.md ~/.claude/skills/vera-language/SKILL.md
 
 ## Project status
 
-Vera is in **active development** at v0.1.8: 2,000+ commits, 204 releases, 8,840 tests, 95% code coverage, 176 conformance programs, 42 examples, and a 14-chapter specification. Known bugs and limitations are tracked in **[KNOWN_ISSUES.md](KNOWN_ISSUES.md)**. See **[HISTORY.md](HISTORY.md)** for how the compiler was built.
+Vera is in **active development** at v0.1.9: 2,000+ commits, 205 releases, 8,841 tests, 95% code coverage, 176 conformance programs, 42 examples, and a 14-chapter specification. Known bugs and limitations are tracked in **[KNOWN_ISSUES.md](KNOWN_ISSUES.md)**. See **[HISTORY.md](HISTORY.md)** for how the compiler was built.
 
 The reference compiler — parser, AST, type checker, contract verifier (Z3), WASM code generator, module system, browser runtime, and runtime contract insertion — is working. The language specification is in draft across [14 chapters](spec/).
 

ROADMAP.md

@@ -12,7 +12,7 @@ Ordering derives from the design principles ([DESIGN.md](DESIGN.md)): verificati
 
 ## Where we are
 
-8,840 tests, 176 conformance programs, 42 examples, 14 spec chapters.  [KNOWN_ISSUES.md](KNOWN_ISSUES.md) tracks the open bugs — burndown material rather than stage work — plus the *limitations* the stages below retire.
+8,841 tests, 176 conformance programs, 42 examples, 14 spec chapters.  [KNOWN_ISSUES.md](KNOWN_ISSUES.md) tracks the open bugs — burndown material rather than stage work — plus the *limitations* the stages below retire.
 
 ## Stage 19 — The verification completeness sprint
 

TESTING.md

@@ -6,7 +6,7 @@ This is the single source of truth for Vera's testing infrastructure, coverage d
 
 | Metric | Value |
 |--------|-------|
-| **Tests** | 8,840 across 136 files (~106,000 lines of test code; 8,712 passed + 26 stress, 102 skipped) |
+| **Tests** | 8,841 across 136 files (~106,000 lines of test code; 8,713 passed + 26 stress, 102 skipped) |
 | **Compiler code coverage** | 95% Python, 61% JavaScript — 91% combined (CI minimum: 80%) |
 | **Conformance programs** | 176 programs across 9 spec chapters, validating every language feature |
 | **Example programs** | 42, all validated through `vera check` + `vera verify` |
@@ -66,7 +66,7 @@ python scripts/check_wheel_availability.py           # pre-flight: every runtime
 | `test_db_marshalling.py` | 35 | 234 | #229 — the `<DB>` marshalling helpers: `Array<Option<String>>` params (inbound reader), `Array<Array<Option<String>>>` query grids (`_alloc_result_ok_rows`) and `Result<Int>` row-counts, round-tripped through an `InstanceCaller` over a real compiled module — each case run normally AND under `VERA_EAGER_GC=1` (every `$alloc` fires `$gc_collect`), the large-grid case forcing free-block reuse; mutation-validated (dropping a shadow-stack root corrupts the read-back / SIGBUSes the swept-pointer read) |
 | `test_db_runtime.py` | 21 | 301 | #229 — the `<DB>` host binding (`vera/runtime/db.py`) on stdlib `sqlite3`: create/insert/select round-trips against `:memory:`, NULL cells → `None`, the affected-row count (incl. the `-1` DDL sentinel), a BLOB cell UTF-8-decoded with replacement, the `Err`-not-crash error path, an unopenable `VERA_DB_URL` deferred to an `Err` (not a host crash), and injection-safety (a malicious param binds as a literal, table intact); plus `_open_connection`'s `VERA_DB_URL` surface (memory + file URLs, in-memory default) and `register_db`'s bind/no-op paths |
 | `test_sql_provenance_309.py` | 79 | 778 | #309 — the SQL literal-provenance gate (SQL injection as a compile-time error): non-literal SQL rejected `E207` (bare param slot, function result, `\(expr)` interpolation, `string_concat` with a runtime operand, let-bound runtime value, `if`-expression), literal / concat-of-literals / let-chain-with-shadowing / empty-string accepted, placeholder/param arity `E208` with quote- and comment-aware counting (named/numbered placeholders are rejected outright, `E209`), the `count_placeholders`↔sqlite3 differential (exact count accepted, one too many rejected), and gate scoping — a user `effect DB` shadow is rejected at its declaration (`E152`, #1149) *and* its runtime SQL still draws `E207` alongside it (defence in depth), an unrelated effect's `query` is not gated, and no `E207` cascade onto a mistyped SQL arg |
-| `test_checker_modules.py` | 104 | 1,653 | Module-call diagnostics, cross-module typing, visibility enforcement, builtin redefinition (function E151 and effect E152 surfaced from a module into its importer), reserved function names (E153 — the contract state forms `old` / `new` and the keyword class `assert`/`assume`/`forall`/`exists`/`match`/`if`/`let`/`fn`/`true`/`false`, each top-level, `where`-helper, and module-surfaced, plus the `handle` host-invoked carve-out and the probe record behind both halves), parsed module calls (#420 split) |
+| `test_checker_modules.py` | 105 | 1,672 | Module-call diagnostics, cross-module typing, visibility enforcement, builtin redefinition (function E151 and effect E152 surfaced from a module into its importer), reserved function names (E153 — the contract state forms `old` / `new` and the keyword class `assert`/`assume`/`forall`/`exists`/`match`/`if`/`let`/`fn`/`true`/`false`, each top-level, `where`-helper, and module-surfaced, plus the `handle` host-invoked carve-out and the probe record behind both halves), parsed module calls (#420 split) |
 | `test_checker_errors.py` | 56 | 866 | Error codes, resolution-coverage diagnostics, contracts, error accumulation (#420 split); cyclic type aliases incl. #1059 self-reference through a type argument (`Future<F>`, mutual `Future<B>`/`Future<A>`, `Array<L>`) rejected E132 |
 | `test_checker_builtins_collections.py` | 97 | 848 | Map / Set / Decimal / Json / Html / Http / Inference built-in type-checking (#420 split) |
 | `test_checker_builtins_strings.py` | 122 | 945 | String / numeric / type-conversion / float-predicate / string-search / markdown / regex built-in type-checking, removed-legacy-name regression (#420 split) |

docs/index.html

@@ -262,7 +262,7 @@ <h1 class="hero-tagline">A programming language designed for LLMs to write, not
         <a href="/SKILL.md" rel="agent-instructions" type="text/markdown" class="btn btn-ghost">For Agents → SKILL.md</a>
       </div>
       <p class="version">
-        <span>v<a href="https://github.com/aallan/vera/releases/tag/v0.1.8">0.1.8</a></span>
+        <span>v<a href="https://github.com/aallan/vera/releases/tag/v0.1.9">0.1.9</a></span>
         <a href="https://github.com/aallan/vera/actions/workflows/ci.yml" aria-label="CI status"><img src="https://github.com/aallan/vera/actions/workflows/ci.yml/badge.svg" alt="CI" style="height:18px"></a>
       </p>
     </div>

docs/index.md

@@ -4,7 +4,7 @@
 
 From the Latin *veritas* — truth. In Vera, verification is a first-class citizen.
 
-**Current version:** [0.1.8](https://github.com/aallan/vera/releases/tag/v0.1.8)  ·  [GitHub](https://github.com/aallan/vera)  ·  [SKILL.md](https://veralang.dev/SKILL.md) (agent language reference)
+**Current version:** [0.1.9](https://github.com/aallan/vera/releases/tag/v0.1.9)  ·  [GitHub](https://github.com/aallan/vera)  ·  [SKILL.md](https://veralang.dev/SKILL.md) (agent language reference)
 
 ## Why?
 

docs/llms-full.txt

@@ -2,7 +2,7 @@
 
 > Vera is a statically typed, purely functional programming language designed for large language models to write. It uses typed slot references (@T.n) instead of variable names, requires contracts on every function, and compiles to WebAssembly.
 
-This file contains the core Vera language documentation — language reference, agent instructions, FAQ, error codes, and formal grammar — compiled into a single document. Version 0.1.8. For the full documentation index including the 14-chapter specification and supplementary docs, see llms.txt.
+This file contains the core Vera language documentation — language reference, agent instructions, FAQ, error codes, and formal grammar — compiled into a single document. Version 0.1.9. For the full documentation index including the 14-chapter specification and supplementary docs, see llms.txt.
 
 
 ========================================================================
@@ -3158,7 +3158,7 @@ The reference compiler is under active development. The current release includes
 
 - A seven-stage pipeline: parse, transform, resolve, typecheck, verify, compile, execute
 - A 14-chapter formal specification
-- 8,840 tests, including a 176-program conformance suite
+- 8,841 tests, including a 176-program conformance suite
 - 42 working example programs
 - 164 built-in functions covering strings, arrays, math, parsing, and data types
 - Four built-in abilities (Eq, Ord, Hash, Show) with constrained generics and ADT auto-derivation