From e7678032a70d3d5f1cbf3c0024129661ca606532 Mon Sep 17 00:00:00 2001 From: Alasdair Allan Date: Tue, 4 Aug 2026 01:53:28 +0100 Subject: [PATCH] Release v0.1.9 Cut the [Unreleased] section as 0.1.9: the declarable-trap purge. The reserved-name family completes (E153 grammar keywords with the handle carve-out, E152 built-in effects, E154 Vera-prefixed type names), `vera run` refuses dropped entries, imported functions' diagnostics and trap source maps name their own module, `decreases` is enforced at run time, and codegen skips propagate to transitive callers. Also hardens scripts/check_doc_counts.py: FAQ.md's headline test count is now pinned (it drifted silently through two releases because only the conformance half of the sentence was checked). Version 0.1.8 -> 0.1.9 across the check_version_sync.py surface; HISTORY row added to the Stage 19/20 table; site assets regenerated. Co-Authored-By: Claude --- CHANGELOG.md | 11 +++++++++-- FAQ.md | 2 +- HISTORY.md | 3 ++- README.md | 2 +- ROADMAP.md | 2 +- TESTING.md | 4 ++-- docs/index.html | 2 +- docs/index.md | 2 +- docs/llms-full.txt | 4 ++-- docs/llms.txt | 2 +- pyproject.toml | 2 +- scripts/check_doc_counts.py | 37 +++++++++++++++++++++++++++++++++++ tests/test_checker_modules.py | 19 ++++++++++++++++++ uv.lock | 2 +- vera/__init__.py | 2 +- vera/checker/registration.py | 23 ++++++++++++---------- 16 files changed, 93 insertions(+), 26 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 727d4ca2..fef153ed 100644 --- a/CHANGELOG.md +++ b/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` 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 (...)` 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` 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 (...)` 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 diff --git a/FAQ.md b/FAQ.md index 7cc4df8a..dbd4866a 100644 --- a/FAQ.md +++ b/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 diff --git a/HISTORY.md b/HISTORY.md index 6068e06e..603551dd 100644 --- a/HISTORY.md +++ b/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 `` 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.** diff --git a/README.md b/README.md index 8731ee43..2f5912af 100644 --- a/README.md +++ b/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/). diff --git a/ROADMAP.md b/ROADMAP.md index 7f40f406..9a3fd2c8 100644 --- a/ROADMAP.md +++ b/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 diff --git a/TESTING.md b/TESTING.md index 8e094e16..6c85be37 100644 --- a/TESTING.md +++ b/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 `` marshalling helpers: `Array>` params (inbound reader), `Array>>` query grids (`_alloc_result_ok_rows`) and `Result` 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 `` 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`, mutual `Future`/`Future`, `Array`) 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) | diff --git a/docs/index.html b/docs/index.html index ff3ae354..9d8ea51b 100644 --- a/docs/index.html +++ b/docs/index.html @@ -262,7 +262,7 @@

A programming language designed for LLMs to write, not For Agents → SKILL.md

- v0.1.8 + v0.1.9 CI

diff --git a/docs/index.md b/docs/index.md index 56c17d2f..f0b7b9f0 100644 --- a/docs/index.md +++ b/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? diff --git a/docs/llms-full.txt b/docs/llms-full.txt index 61201e9d..10ba4b5e 100644 --- a/docs/llms-full.txt +++ b/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 diff --git a/docs/llms.txt b/docs/llms.txt index 579a3b51..9650fce6 100644 --- a/docs/llms.txt +++ b/docs/llms.txt @@ -4,7 +4,7 @@ Vera uses De Bruijn indexing for bindings: `@Int.0` is the most recent `Int` binding, `@Int.1` the one before. There are no variable names. Contracts are mandatory — every function must declare `requires(...)`, `ensures(...)`, and `effects(...)`. The Z3 SMT solver verifies contracts statically where possible; remaining contracts become runtime assertions. All side effects (IO, Http, HttpServer, State, Exceptions, Async, Inference, DB, Random, Diverge) are tracked in the type system via algebraic effects. -Current version: 0.1.8. The reference compiler is written in Python. Install the `veralang` distribution from PyPI or use `pip install -e ".[dev]"` from the repository. +Current version: 0.1.9. The reference compiler is written in Python. Install the `veralang` distribution from PyPI or use `pip install -e ".[dev]"` from the repository. ## Homepage diff --git a/pyproject.toml b/pyproject.toml index c8ab5182..70200823 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -1,6 +1,6 @@ [project] name = "veralang" -version = "0.1.8" +version = "0.1.9" description = "Vera: a programming language designed for LLMs, with full contracts, algebraic effects, and typed slot references" readme = "PYPI_README.md" license = "MIT" diff --git a/scripts/check_doc_counts.py b/scripts/check_doc_counts.py index 0abe479e..20f091ee 100644 --- a/scripts/check_doc_counts.py +++ b/scripts/check_doc_counts.py @@ -838,6 +838,25 @@ def check_readme(pattern: str, expected: int, label: str) -> None: f" live is {live_conformance}" ) + # The by-the-numbers test count ("8,840 tests, including a ..."). + # This line drifted silently through two releases because only the + # conformance half of the sentence was pinned. A missing pattern is + # an error, not a skip — otherwise rewording the line disables the + # check and reopens the same blind spot one level up. + m = re.search(r"([\d,]+) tests, including", faq_md) + if not m: + errors.append( + "FAQ.md: headline test-count line" + " ('N tests, including ...') not found" + ) + else: + doc_tests = int(m.group(1).replace(",", "")) + if doc_tests != live_total_tests: + errors.append( + f"FAQ.md: tests count: doc says {doc_tests}," + f" live is {live_total_tests}" + ) + # ------------------------------------------------------------------ # 13. Check docs/index.html status block # ------------------------------------------------------------------ @@ -937,6 +956,24 @@ def check_readme(pattern: str, expected: int, label: str) -> None: history_md = (root / "HISTORY.md").read_text(encoding="utf-8") errors.extend(check_history_row_format(history_md)) + # README's status row and HISTORY's "By the numbers" total are the + # same hand-maintained release count in two places; a release bumps + # both. They disagreed for two releases (204/203, then 205/203) + # before this cross-check existed. + m_readme = re.search(r"(\d+) releases,", readme_md) + m_history = re.search(r"(\d+) tagged releases", history_md) + if not m_readme: + errors.append("README.md: release count ('N releases,') not found") + if not m_history: + errors.append( + "HISTORY.md: release count ('N tagged releases') not found" + ) + if m_readme and m_history and m_readme.group(1) != m_history.group(1): + errors.append( + f"release count mismatch: README.md says {m_readme.group(1)}," + f" HISTORY.md says {m_history.group(1)} tagged releases" + ) + # ------------------------------------------------------------------ # 17. Check the vera/README.md module map against the source tree # ------------------------------------------------------------------ diff --git a/tests/test_checker_modules.py b/tests/test_checker_modules.py index ea865c5a..c38c3cf4 100644 --- a/tests/test_checker_modules.py +++ b/tests/test_checker_modules.py @@ -1256,6 +1256,25 @@ class TestReservedKeywordFnName: def _codes(errs: list[Diagnostic]) -> list[str]: return [e.error_code for e in errs] + def test_keyword_tuple_matches_checker_set(self) -> None: + """``KEYWORDS`` mirrors the checker's reserved keyword set exactly. + + Pins ``set(KEYWORDS) == _KEYWORD_FN_NAMES - _HOST_INVOKED_FN_NAMES`` + so a keyword added to the checker's set without a matching + per-keyword ``E153`` test here fails this pin instead of silently + escaping coverage. The subtraction preserves the deliberate + omission of ``handle`` (the host-invoked carve-out). + """ + from vera.checker.registration import ( + _HOST_INVOKED_FN_NAMES, + _KEYWORD_FN_NAMES, + ) + + assert ( + set(self.KEYWORDS) + == _KEYWORD_FN_NAMES - _HOST_INVOKED_FN_NAMES + ) + @pytest.mark.parametrize("name", KEYWORDS) def test_keyword_fn_name_is_E153(self, name: str) -> None: """Each reserved keyword is refused at the declaration site.""" diff --git a/uv.lock b/uv.lock index 74a1e60b..0da3f741 100644 --- a/uv.lock +++ b/uv.lock @@ -1544,7 +1544,7 @@ wheels = [ [[package]] name = "veralang" -version = "0.1.8" +version = "0.1.9" source = { editable = "." } dependencies = [ { name = "lark" }, diff --git a/vera/__init__.py b/vera/__init__.py index 99c3f916..301e8d4b 100644 --- a/vera/__init__.py +++ b/vera/__init__.py @@ -1,4 +1,4 @@ """Vera: a programming language designed for LLMs.""" -__version__ = "0.1.8" +__version__ = "0.1.9" version = __version__ diff --git a/vera/checker/registration.py b/vera/checker/registration.py index 652d6562..3b5942a7 100644 --- a/vera/checker/registration.py +++ b/vera/checker/registration.py @@ -334,10 +334,12 @@ def _check_reserved_fn_name(self, decl: ast.FnDecl) -> None: f"position as a reference to an effect's " f"{'pre' if n == 'old' else 'post'}-state, whose only " f"valid argument is an effect reference such as " - f"'{n}(State)'. A call '{n}(...)' therefore never " - f"resolves to a function, so this declaration could not " - f"be reached from anywhere in the program — it is dead " - f"code the compiler would otherwise accept in silence." + f"'{n}(State)'. A bare call '{n}(...)' therefore never " + f"resolves to a function, so no unqualified call site " + f"can reach this declaration. The one route that " + f"previously could — a module-qualified 'mod::{n}(...)' " + f"on an exported function — is deliberately closed by " + f"this reservation rather than left half-usable." ) fix = ( f"Rename the function to an identifier that is not a " @@ -354,12 +356,13 @@ def _check_reserved_fn_name(self, decl: ast.FnDecl) -> None: f"parses only because the lexer reads '{n}' as a name " f"after 'fn'; in a body '{n}' is always lexed as the " f"keyword, so '{n}(...)' does not parse as a call and " - f"never resolves to a function. This declaration could " - f"not be reached from anywhere in the program — it is " - f"dead code the compiler would otherwise accept in " - f"silence. Vera provides exactly one way to express each " - f"construct, so a keyword names that construct and " - f"nothing else." + f"no unqualified call site can reach this declaration. " + f"The one route that previously could — a " + f"module-qualified 'mod::{n}(...)' on an exported " + f"function — is deliberately closed by this reservation " + f"rather than left half-usable. Vera provides exactly " + f"one way to express each construct, so a keyword names " + f"that construct and nothing else." ) fix = ( f"Rename the function to an identifier that is not a "