From 2f1dc4a97d51fef86d0976433bd582888f8e6a40 Mon Sep 17 00:00:00 2001 From: Alasdair Allan Date: Mon, 3 Aug 2026 20:16:53 +0100 Subject: [PATCH] Reserve keyword function names; carve out host-invoked entry points (E153) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 E153 now refuses it at the declaration, extending the #1181 gate for the contract state forms under the same one-canonical-form rule as E151 and E152. `handle` is carved out: `public fn handle(@Request -> @Response)` is the host-invoked `vera serve` / `wasi:http` entry point (spec §9.5.6), so being uncallable from Vera source does not make it dead code. The reserved set is derived as (state forms) | (keywords) - (host-invoked), each piece named and commented, so a future host-invoked entry point joins the carve-out deliberately. 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 now be renamed; the breakage is loud and located at the module's declaration. The E153 rationale branches with the reason (a keyword is not described as a contract state form) while the fix stays "rename" on both. New conformance program ch05_reserved_keyword_fn_rejected (176, was 175). Co-Authored-By: Claude --- AGENTS.md | 6 +- CHANGELOG.md | 6 +- CLAUDE.md | 6 +- FAQ.md | 4 +- README.md | 2 +- ROADMAP.md | 2 +- SKILL.md | 4 +- TESTING.md | 32 +- docs/SKILL.md | 4 +- docs/index.html | 2 +- docs/index.md | 2 +- docs/llms-full.txt | 14 +- docs/llms.txt | 2 +- spec/05-functions.md | 12 +- .../ch05_reserved_keyword_fn_rejected.vera | 23 ++ tests/conformance/manifest.json | 14 + tests/test_checker_modules.py | 286 +++++++++++++++++- vera/README.md | 2 +- vera/checker/modules.py | 7 +- vera/checker/registration.py | 127 +++++--- 20 files changed, 461 insertions(+), 96 deletions(-) create mode 100644 tests/conformance/ch05_reserved_keyword_fn_rejected.vera diff --git a/AGENTS.md b/AGENTS.md index 2bae21e5..596eaef2 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -8,7 +8,7 @@ Read `SKILL.md` for the full language reference. It covers syntax, slot referenc ### Conformance programs as reference -The conformance suite in `tests/conformance/` contains 175 small, self-contained programs — often one per language feature — that serve as minimal working examples (most are fully self-contained; the cross-module programs of Chapters 7–9 import companion `_lib`/module fixtures). Each positive program must pass its declared verification level (see `manifest.json` for mappings: `parse`, `check`, `verify`, or `run`); the twenty-two negative fixtures (`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_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch07_bare_effect_op_rejected`) instead must *fail* `check` with the E-code in their `expected_error` field. When you need to see how a specific construct works (e.g. effect handlers, match expressions, closures), check the corresponding conformance program before reading the spec. +The conformance suite in `tests/conformance/` contains 176 small, self-contained programs — often one per language feature — that serve as minimal working examples (most are fully self-contained; the cross-module programs of Chapters 7–9 import companion `_lib`/module fixtures). Each positive program must pass its declared verification level (see `manifest.json` for mappings: `parse`, `check`, `verify`, or `run`); the twenty-three negative fixtures (`ch02_generic_over_unit_rejected`, `ch02_map_unit_value_rejected`, `ch04_let_unit_rejected`, `ch05_apply_fn_arity`, `ch05_decreases_float_rejected`, `ch05_reserved_fn_name_rejected`, `ch05_reserved_keyword_fn_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch07_bare_effect_op_rejected`) instead must *fail* `check` with the E-code in their `expected_error` field. When you need to see how a specific construct works (e.g. effect handlers, match expressions, closures), check the corresponding conformance program before reading the spec. ### Workflow @@ -185,7 +185,7 @@ Each stage is a module with a single public API function (`parse_file`, `transfo pytest tests/ -v # Run all tests (see TESTING.md) pytest tests/test_conformance.py -v # Conformance suite only mypy vera/ # Type-check the compiler -python scripts/check_conformance.py # All 175 conformance programs hold (positives pass; negatives fail with their E-code) +python scripts/check_conformance.py # All 176 conformance programs hold (positives pass; negatives fail with their E-code) python scripts/check_examples.py # All 42 examples must pass python scripts/check_corpus_canonical.py # All 217 corpus programs in canonical form ``` @@ -196,7 +196,7 @@ When implementing a new language feature, write the conformance program *first* ### Invariants -- All 175 conformance programs in `tests/conformance/` must hold at their declared level — positive entries pass, and the negative fixtures (`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_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch07_bare_effect_op_rejected`) must *fail* `check` with their `expected_error` E-code +- All 176 conformance programs in `tests/conformance/` must hold at their declared level — positive entries pass, and the negative fixtures (`ch02_generic_over_unit_rejected`, `ch02_map_unit_value_rejected`, `ch04_let_unit_rejected`, `ch05_apply_fn_arity`, `ch05_decreases_float_rejected`, `ch05_reserved_fn_name_rejected`, `ch05_reserved_keyword_fn_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch07_bare_effect_op_rejected`) must *fail* `check` with their `expected_error` E-code - All 42 examples in `examples/` must pass `vera check` and `vera verify` - `mypy vera/` must be clean - `pytest tests/ -v` must pass diff --git a/CHANGELOG.md b/CHANGELOG.md index 328dc6cd..727d4ca2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -31,7 +31,11 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/). - **`fn old` / `fn new` declarations are rejected at the declaration site, `E153`** ([#1181](https://github.com/aallan/vera/issues/1181)). The grammar reserves `old(` and `new(` in expression position for the contract state forms — `old_expr` / `new_expr` in `vera/grammar.lark`, each of which demands an effect reference — so a bare call `old(5)` is always read as a malformed state reference (`[E030]`/`[E031]`, [#1173](https://github.com/aallan/vera/issues/1173)) and never resolves to a function — not in the declaring file, and not inside the declaring module either. One route did reach such a function: a module-qualified `mod::old(...)` parses through the module-call rule, so a module export named `old` was callable cross-module (and only cross-module) — adversarial review of the fix confirmed the shape checked and ran. The declaration is now refused outright, reserving the whole identifier rather than leaving it a trap in every unqualified position, the sibling of `E151` (built-in functions) and `E152` (built-in effects) under the same one-canonical-form rule. **Breaking**: a module export named `old` or `new` that was called via the qualified route must be renamed. The gate covers top-level and `private` functions, generic `forall` functions, `where`-helpers (called in expression position exactly like top-level functions), and modules — a module declaring `fn old` surfaces `E153` into its importer, as `E151` and `E152` already do. The reservation is on the whole identifier, so `older` / `renew` / `news` stay legal. - The reserved set is exactly `{old, new}`, not every keyword the contextual lexer admits as a function name. `assert`, `assume`, `forall`, `exists`, `handle`, `match`, `if`, `let`, `fn`, `true` and `false` were all probed and share the "declares fine, cannot be called from expression position" property, but that property alone is not grounds for rejection: `public fn handle(@Request -> @Response)` is the `vera serve` entry point (spec §9.5.6), invoked by the host rather than from Vera source. The probe record lives in the test docstrings. Spec §5.2 states the rule; new conformance program `ch05_reserved_fn_name_rejected` (172, was 171) pins it as an `E153` negative. Mutation-validated: emptying the reserved set, dropping the `where`-helper recursion, dropping the module surfacing, and matching on prefix rather than whole identifier each flip their targeted tests RED. + This half of the gate covers the two contract state forms; the keyword class the contextual lexer also admits as a function name is reserved separately, by [#1187](https://github.com/aallan/vera/issues/1187) below. The probe record lives in the test docstrings. Spec §5.2 states the rule; new conformance program `ch05_reserved_fn_name_rejected` (172, was 171) pins it as an `E153` negative. Mutation-validated: emptying the reserved set, dropping the `where`-helper recursion, dropping the module surfacing, and matching on prefix rather than whole identifier each flip their targeted tests RED. + +- **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`). - **`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. diff --git a/CLAUDE.md b/CLAUDE.md index 02f27120..62868407 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -58,7 +58,7 @@ VERA_JS_COVERAGE=1 pytest tests/test_browser.py -v # Browser tests with JS cove VERA_EAGER_GC=1 vera run file.vera # Force GC on every alloc (see ENVIRONMENT.md, debug knob for #593-class GC-rooting bugs) mypy vera/ # Type-check the compiler itself -python scripts/check_conformance.py # Verify all 175 conformance programs (positives pass their level; negatives fail with their expected_error E-code) +python scripts/check_conformance.py # Verify all 176 conformance programs (positives pass their level; negatives fail with their expected_error E-code) python scripts/check_examples.py # Verify all 42 examples parse + check + verify python scripts/check_corpus_canonical.py # Verify all 217 corpus programs are in canonical form (vera fmt) python scripts/check_examples_readme.py # Verify vera run commands in examples/README.md @@ -90,7 +90,7 @@ See [`TOOLCHAIN.md`](TOOLCHAIN.md) for the CLI cookbook — driving the toolchai - `vera/` — Reference compiler: grammar, parser, AST, transformer, type checker, verifier, codegen, CLI - `examples/` — 42 example Vera programs (all must pass `vera check` and `vera verify`) - `tests/` — Test suite (unit tests + conformance suite) -- `tests/conformance/` — 175 conformance programs validating every language feature against the spec +- `tests/conformance/` — 176 conformance programs validating every language feature against the spec - `scripts/` — CI and validation scripts ## Writing Vera code @@ -127,7 +127,7 @@ Before changing code — **adding or removing** — write the test that proves y ## What not to break - Pre-commit hooks run mypy + pytest + conformance suite + example validation on every commit -- All 175 conformance programs in `tests/conformance/` must hold at their declared level — positive entries pass, and the negative fixtures (`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_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch07_bare_effect_op_rejected`) must *fail* `check` with their `expected_error` E-code +- All 176 conformance programs in `tests/conformance/` must hold at their declared level — positive entries pass, and the negative fixtures (`ch02_generic_over_unit_rejected`, `ch02_map_unit_value_rejected`, `ch04_let_unit_rejected`, `ch05_apply_fn_arity`, `ch05_decreases_float_rejected`, `ch05_reserved_fn_name_rejected`, `ch05_reserved_keyword_fn_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch07_bare_effect_op_rejected`) must *fail* `check` with their `expected_error` E-code - All 42 examples in `examples/` must pass `vera check` and `vera verify` - Version must stay in sync across `pyproject.toml`, `vera/__init__.py`, `docs/index.html`, `README.md`, and `uv.lock` (gated by `scripts/check_version_sync.py`); CHANGELOG.md must also carry a matching `## [X.Y.Z]` section - All tests must pass: `pytest tests/ -v` diff --git a/FAQ.md b/FAQ.md index f238ee15..7cc4df8a 100644 --- a/FAQ.md +++ b/FAQ.md @@ -206,7 +206,7 @@ None of this is Vera-specific, but it validates the design choices. The thesis i This is a real concern. LLMs are trained on trillions of tokens of Python, TypeScript, and JavaScript. A MojoBench study (NAACL 2025) found that even fine-tuned models achieved only 30–35% improvement over base models on Mojo code generation, illustrating the cold-start problem for new languages. -Vera's approach has three parts. First, the agent-facing documentation (SKILL.md) is designed to be dropped into a model's context window, so the model works from the language specification rather than training data recall. Second, Vera's syntax is deliberately simple and regular — fewer constructs, each with exactly one canonical form — which reduces the surface area a model needs to learn. Third, the conformance test suite (175 programs covering every language feature) gives models concrete examples to learn from and conform to. Simon Willison's December 2025 JustHTML write-up illustrates the same point in practice: an LLM-assisted implementation, guided by the html5lib conformance suite, conformed to the HTML parsing spec by running against its tests — a comprehensive test suite is a strong scaffold for a model implementing to a specification. +Vera's approach has three parts. First, the agent-facing documentation (SKILL.md) is designed to be dropped into a model's context window, so the model works from the language specification rather than training data recall. Second, Vera's syntax is deliberately simple and regular — fewer constructs, each with exactly one canonical form — which reduces the surface area a model needs to learn. Third, the conformance test suite (176 programs covering every language feature) gives models concrete examples to learn from and conform to. Simon Willison's December 2025 JustHTML write-up illustrates the same point in practice: an LLM-assisted implementation, guided by the html5lib conformance suite, conformed to the HTML parsing spec by running against its tests — a comprehensive test suite is a strong scaffold for a model implementing to a specification. ## How does Vera compare to Dafny / Lean / Koka / F*? @@ -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,796 tests, including a 175-program conformance suite +- 8,840 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/README.md b/README.md index 7838480d..8731ee43 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,796 tests, 95% code coverage, 175 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.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. 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 7c7c33e2..7f40f406 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,796 tests, 175 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,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. ## Stage 19 — The verification completeness sprint diff --git a/SKILL.md b/SKILL.md index 91d06c60..7a32625d 100644 --- a/SKILL.md +++ b/SKILL.md @@ -1264,7 +1264,7 @@ infinity() -- returns Float64 (positive infinity) **Redefining a built-in is an error (E151)**: a function whose name matches a built-in (e.g. `abs`, `array_length`, `clamp`, `to_string`) is rejected at `vera check`. Built-ins are always in scope as the single canonical definition, so a second one is both redundant (one canonical form) and — for the verifier-modelled built-ins — silently unsound: the verifier would reason with the built-in's model while codegen runs your body. Call the built-in directly (no import needed), or give your function a distinct name (e.g. `magnitude`) for genuinely different behaviour. The one exception is the prelude's Option/Result/Json/Html *combinators* (`option_map`, `option_and_then`, `option_unwrap_or`, `result_map`, `result_unwrap_or`, `json_*`, `html_attr`): these are ordinary Vera functions the prelude injects, so a same-named user definition soundly replaces them. -**`old` and `new` are not available as function names (E153)**: both are contract state forms, so `old(...)` / `new(...)` in expression position always parses as a reference to an effect's before/after state (Chapter 7, Section 7.9.2) and never as a call. A `fn old` or `fn new` — top-level, `where`-helper, or in an imported module — could therefore never be called, and is rejected at `vera check`. Rename it. Only the exact identifiers are reserved: `older`, `renew`, and the like are ordinary function names. +**Reserved function names (E153)**: an identifier the grammar claims in expression position cannot be a function name. Two groups. `old` and `new` are contract state forms, so `old(...)` / `new(...)` always parses as a reference to an effect's before/after state (Chapter 7, Section 7.9.2) and never as a call. `assert`, `assume`, `forall`, `exists`, `match`, `if`, `let`, `fn`, `true` and `false` are keywords the lexer admits as a name after `fn` but reads as the keyword everywhere else, so `match(3)` in a body does not parse as a call either. A function under any of these — top-level, `where`-helper, or in an imported module — could never be called, and is rejected at `vera check`. Rename it. Only the exact identifiers are reserved: `older`, `renew`, `matched` and the like are ordinary function names. `handle` is the one keyword still available, because `public fn handle(@Request -> @Response)` is the entry point `vera serve` invokes from the host (Chapter 9, Section 9.5.6). Example: @@ -2429,7 +2429,7 @@ public fn main(@Unit -> @Unit) ## Conformance Suite -The `tests/conformance/` directory contains 175 small programs — most self-contained, with the Chapter 8 module-system programs and a few cross-module Chapter 7 and 9 programs importing companion `_lib.vera` / `_mid.vera` modules — that validate every language feature against the spec — often one program per feature, though some features (slot references, match, contracts) span several. These are the best minimal working examples of Vera syntax and semantics. +The `tests/conformance/` directory contains 176 small programs — most self-contained, with the Chapter 8 module-system programs and a few cross-module Chapter 7 and 9 programs importing companion `_lib.vera` / `_mid.vera` modules — that validate every language feature against the spec — often one program per feature, though some features (slot references, match, contracts) span several. These are the best minimal working examples of Vera syntax and semantics. Each program is organized by spec chapter (`ch01_int_literals.vera`, `ch04_match_basic.vera`, `ch07_state_handler.vera`, etc.) and the `manifest.json` file maps features to programs. When you need to see how a specific construct works, check the conformance program before reading the spec. diff --git a/TESTING.md b/TESTING.md index 44f1a9a2..8e094e16 100644 --- a/TESTING.md +++ b/TESTING.md @@ -6,9 +6,9 @@ This is the single source of truth for Vera's testing infrastructure, coverage d | Metric | Value | |--------|-------| -| **Tests** | 8,796 across 136 files (~106,000 lines of test code; 8,670 passed + 26 stress, 100 skipped) | +| **Tests** | 8,840 across 136 files (~106,000 lines of test code; 8,712 passed + 26 stress, 102 skipped) | | **Compiler code coverage** | 95% Python, 61% JavaScript — 91% combined (CI minimum: 80%) | -| **Conformance programs** | 175 programs across 9 spec chapters, validating every language feature | +| **Conformance programs** | 176 programs across 9 spec chapters, validating every language feature | | **Example programs** | 42, all validated through `vera check` + `vera verify` | | **Spec code blocks** | 189 parseable blocks from 14 spec chapters: 92 parse, 86 type-check, 85 verify (the rest carry inline `vera:skip` annotations, #538) | | **README code blocks** | 4 Vera blocks (4 validated, 0 annotated) | @@ -39,7 +39,7 @@ VERA_EAGER_GC=1 pytest tests/test_codegen_closures.py::TestClosureReturnShadowPu mypy vera/ # strict mode # Validation scripts -python scripts/check_conformance.py # conformance suite (175 programs, see manifest.json) +python scripts/check_conformance.py # conformance suite (176 programs, see manifest.json) python scripts/check_examples.py # 42 example programs python scripts/check_spec_examples.py # spec code blocks python scripts/check_readme_examples.py # README code blocks @@ -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` | 66 | 1,397 | 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 (`old` / `new`, E153 — top-level, `where`-helper, and module-surfaced, with the probe record for why the reserved set is exactly those two), parsed module calls (#420 split) | +| `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_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) | @@ -153,7 +153,7 @@ python scripts/check_wheel_availability.py # pre-flight: every runtime | `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` | 470 | 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_formatter.py` | 471 | 3,638 | Comment extraction, interior comment positioning, expression/declaration formatting, match arm block bodies, §1.8 rule 2 in value position (a `let`-bound `match`/`if` expands exactly as one in statement position, and a comment above an arm inside a statement's value stays on that arm), blank-line preservation (§1.8 rule 13 — gaps between statements, before a block result and around a comment, collapsed to one and never invented), idempotency, parenthesization, spec rules, ability declarations | | `test_cli.py` | 266 | 4,287 | CLI commands (check, verify, compile, run, serve, test, fmt, version, quiet), subprocess integration, JSON error paths (including the `verify --json` `obligations` array and its summary-reproducibility pin, #967), runtime traps, arg validation, multi-file resolution, IO exit codes, --explain-slots, `builtins`/`effects`/`errors` introspection dispatch, and a USAGE-completeness guard (every dispatched `cmd_` 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` 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) | @@ -171,7 +171,7 @@ python scripts/check_wheel_availability.py # pre-flight: every runtime | `test_markdown.py` | 59 | 393 | Markdown parser: block/inline parsing, rendering, round-trips, edge cases | | `test_lsp.py` | 94 | 1211 | LSP transport + coordinate layer (#222 Phase C) and language features (#222 Phase D): parametrized code-point↔UTF-16 goldens incl. astral-plane fixtures and surrogate-pair snapping, Span (1-based, exclusive-end) and SourceLocation (0-based col) → LSP Range conversions, point→token-range widening, DocumentStore open/change/close + index invalidation, an in-process handler-drive test, and one stdio end-to-end round-trip against the real `vera lsp` subprocess (initialize → didOpen → shutdown → exit) pinning serverInfo + textDocumentSync capabilities; plus the Phase D feature suite — parse-error single-diagnostic path, type-error verification short-circuit, tier=3 in E520 diagnostic data, per-function tier Hint synthesis (and its suppression for functions with violated obligations), smallest-enclosing-span hover, De Bruijn slot goto (most-recent-parameter jump, out-of-range None, off-slot None), and typed-hole completion (inside/after hole, away-from-hole None); plus the Phase E speculativeEdit suite — identical-text all-unchanged, breaking edit surfaces newly_undischarged (violated nat_sub) with canonical state untouched, strengthening edit surfaces newly_discharged, parse/type errors report ok:false, deleted functions report removed, proof_delta purity; plus the Phase F1 proposeEdit suite — the apply gate (clean and strengthening edits apply, breaking and non-compiling edits refuse), force overriding both gates with the delta still reported, wiring against a structural fake server (apply round-trip with exact full-document replacement range, refuse touches no canonical state, unopened-URI clamp sentinel), and full-document-range goldens (trailing-newline virtual line, UTF-16 end column); plus the Phase F2 strengthenContract suite — splice goldens (first-clause-only replacement with byte-identical remainder, ensures variant, unknown-fn None), the call-site audit pin (tightened precondition refused with newly_undischarged call_pre items, canonical state untouched), provable-ensures strengthening applies, and the three splice-target refusal paths (no analysis, unparseable document, unknown function); plus the Phase F3 addEffect suite — transitive-caller closure goldens (diamond in declaration order, leaf, unknown-fn None, recursion appears once), effect-row rewrite goldens (pure to singleton set, source-preserving append, already-present None, base-name identity blocking State next to State), diamond propagation applying one multi-site candidate with the bystander untouched, mixed append/replace rows with already-satisfied callers skipped, the fully-satisfied no-op shape, and the two refusal paths; plus the #728 instruction-contract suite — the LSP message carries description, rationale, and the Fix: paragraph (also pinning single E501 emission at the LSP surface), and a bare diagnostic maps to the description alone | | `test_browser.py` | 138 | 3,068 | Browser parity: Python/wasmtime vs Node.js/JS-runtime output equivalence across IO, State, contracts, Markdown, Regex, and all compilable examples | -| `test_conformance.py` | 875 | 125 | Parametrized conformance suite: parse, check, verify, run, format idempotency across 175 programs | +| `test_conformance.py` | 880 | 125 | Parametrized conformance suite: parse, check, verify, run, format idempotency across 176 programs | | `test_prelude.py` | 27 | 526 | Prelude injection: Option/Result/array operation detection, combinator shadowing, type aliases, the reserved-name twins the combinators resolve through (#1184), end-to-end compilation | | `test_checker_apply_fn.py` | 18 | 455 | #854 — `apply_fn` as a checker special form: zero-warning pins (API + CLI `--json` + closures.vera), E201 arity / E202 type / non-function-first-arg errors, E122/E125 effect-row enforcement for applied fn values, E151 redefinition rejection, variadic two-param application, prelude combinator regression pins | | `test_prelude_diagnostics.py` | 8 | 271 | #851 — prelude combinator skip-warnings: unreferenced-prelude E602/E604 suppression (zero-warning minimal compile, API + CLI `--json`), `` origin attribution for referenced-but-skipped combinators (text + `to_dict`), transitive reference scan, and user-fn warning locations pinned unchanged | @@ -194,7 +194,7 @@ python scripts/check_wheel_availability.py # pre-flight: every runtime ## Conformance Suite -The conformance suite is a collection of 175 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. +The conformance suite is a collection of 176 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. @@ -219,15 +219,15 @@ 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 | 29 | +| `check` | Parses and type-checks cleanly | 30 | | `verify` | Type-checks and all contracts verified by Z3 | 13 | | `run` | Compiles to WASM and executes correctly | 133 | -Almost all programs are at the `run` level — they compile and execute, producing correct results. Twenty-nine 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_where_helper_outer_slot_rejected`, `ch07_cross_module_contracts_lib`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch07_bare_effect_op_rejected`, `ch08_circular_import`, `ch08_cross_module_generic_lib`, `ch08_reserved_vera_prefix_rejected`, `ch08_transitive_module_import_base`, `ch08_visibility_private`, `ch08_xmod_widen_lib`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_eq_non_derivable_rejected`, `ch09_http`, `ch09_inference`, `ch09_ord_adt_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`) are at the `check` level. Twenty-two 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_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch07_bare_effect_op_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, and `ch09_sql_numbered_placeholder_rejected` — are **negative tests** that assert a specific diagnostic (E206, E135, E183, E201, E127, E153, E130, E130, E174, E182, E217, E011, E154, E150, E152, E151, E242, E243, E207, E208, E208, and E209 respectively) via the manifest's `expected_error` field; `ch09_http` and `ch09_inference` are environment-gated (network / API key). Thirteen programs (`ch03_slot_let_chains`, `ch03_slot_noncommutative`, `ch04_nested_option_ctor`, `ch04_primitive_obligations`, `ch05_apply_fn_typing`, `ch06_adt_sort_disambiguation`, `ch07_cross_module_contracts`, `ch07_io_read_char`, `ch07_io_sleep`, `ch07_random_effect`, `ch08_transitive_module_import_mid`, `ch09_http_server`, `ch09_math_builtins`) are at the `verify` level, using Z3-provable contracts. +Almost all programs are at the `run` level — they compile and execute, producing correct results. Thirty programs (`ch02_generic_over_unit_rejected`, `ch02_map_unit_value_rejected`, `ch03_typed_holes`, `ch04_let_unit_rejected`, `ch05_apply_fn_arity`, `ch05_decreases_float_rejected`, `ch05_reserved_fn_name_rejected`, `ch05_reserved_keyword_fn_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_cross_module_contracts_lib`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch07_bare_effect_op_rejected`, `ch08_circular_import`, `ch08_cross_module_generic_lib`, `ch08_reserved_vera_prefix_rejected`, `ch08_transitive_module_import_base`, `ch08_visibility_private`, `ch08_xmod_widen_lib`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_eq_non_derivable_rejected`, `ch09_http`, `ch09_inference`, `ch09_ord_adt_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`) are at the `check` level. Twenty-three of them — `ch02_generic_over_unit_rejected`, `ch02_map_unit_value_rejected`, `ch04_let_unit_rejected`, `ch05_apply_fn_arity`, `ch05_decreases_float_rejected`, `ch05_reserved_fn_name_rejected`, `ch05_reserved_keyword_fn_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch07_bare_effect_op_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, and `ch09_sql_numbered_placeholder_rejected` — are **negative tests** that assert a specific diagnostic (E206, E135, E183, E201, E127, E153, E153, E130, E130, E174, E182, E217, E011, E154, E150, E152, E151, E242, E243, E207, E208, E208, and E209 respectively) via the manifest's `expected_error` field; `ch09_http` and `ch09_inference` are environment-gated (network / API key). Thirteen programs (`ch03_slot_let_chains`, `ch03_slot_noncommutative`, `ch04_nested_option_ctor`, `ch04_primitive_obligations`, `ch05_apply_fn_typing`, `ch06_adt_sort_disambiguation`, `ch07_cross_module_contracts`, `ch07_io_read_char`, `ch07_io_sleep`, `ch07_random_effect`, `ch08_transitive_module_import_mid`, `ch09_http_server`, `ch09_math_builtins`) are at the `verify` level, using Z3-provable contracts. ### Skipped tests -`pytest tests/ -v` skips 71 conformance-stage tests across the two categories below (the suite's remaining skips are platform- or tool-gated and documented beside the tests that declare them): +`pytest tests/ -v` skips 73 conformance-stage tests across the two categories below (the suite's remaining skips are platform- or tool-gated and documented beside the tests that declare them): **Level-limited skips** — the conformance framework only runs tests up to the declared level; stages beyond that level are automatically skipped. These are expected and correct. @@ -252,6 +252,8 @@ Almost all programs are at the `run` level — they compile and execute, produci | `test_run[ch05_decreases_float_rejected]` | `ch05_decreases_float_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage | | `test_verify[ch05_reserved_fn_name_rejected]` | `ch05_reserved_fn_name_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E153`): verify stage not run | | `test_run[ch05_reserved_fn_name_rejected]` | `ch05_reserved_fn_name_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage | +| `test_verify[ch05_reserved_keyword_fn_rejected]` | `ch05_reserved_keyword_fn_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E153`): verify stage not run | +| `test_run[ch05_reserved_keyword_fn_rejected]` | `ch05_reserved_keyword_fn_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage | | `test_verify[ch05_where_helper_outer_slot_rejected]` | `ch05_where_helper_outer_slot_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E130`): verify stage not run | | `test_run[ch05_where_helper_outer_slot_rejected]` | `ch05_where_helper_outer_slot_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage | | `test_run[ch06_adt_sort_disambiguation]` | `ch06_adt_sort_disambiguation.vera` | `verify` | `run` | `verify`-level programs don't get a `run` test | @@ -320,7 +322,7 @@ tests/conformance/ ├── 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 -├── ... # 175 programs total, organized by spec chapter +├── ... # 176 programs total, organized by spec chapter ├── ch07_state_handler.vera # Chapter 7: State effect handler ├── ch07_exn_handler.vera # Chapter 7: Exn effect handler ├── ch09_numeric_builtins.vera # Chapter 9: Numeric built-in functions @@ -680,9 +682,9 @@ Twenty-two scripts in `scripts/` validate cross-cutting concerns beyond unit tes | Script | What it validates | |--------|-------------------| -| `check_conformance.py` | All 175 conformance entries hold at their declared level (parse/check/verify/run) — positives pass; the negatives fail `check` with their `expected_error` E-code | +| `check_conformance.py` | All 176 conformance entries hold at their declared level (parse/check/verify/run) — positives pass; the negatives fail `check` with their `expected_error` E-code | | `check_examples.py` | All 42 `.vera` examples pass `vera check` + `vera verify` | -| `check_corpus_canonical.py` | All 223 corpus programs (recursive over `examples/` + `tests/conformance/`) are in canonical form under `vera fmt` | +| `check_corpus_canonical.py` | All 224 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 | @@ -783,9 +785,9 @@ Every push is checked by 32 configured hooks across two stages: 30 are configure | `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 175 conformance entries hold at their declared level — positives pass; negatives fail `check` with their `expected_error` E-code | +| `check_conformance.py` | All 176 conformance entries hold at their declared level — positives pass; negatives fail `check` with their `expected_error` E-code | | `check_examples.py` | All 42 examples pass `vera check` + `vera verify` | -| `check_corpus_canonical.py` | All 223 `examples/` + `tests/conformance/` programs (recursive) are in canonical form (`vera fmt`) | +| `check_corpus_canonical.py` | All 224 `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 | diff --git a/docs/SKILL.md b/docs/SKILL.md index 5f1f6cdd..8b034a48 100644 --- a/docs/SKILL.md +++ b/docs/SKILL.md @@ -1231,7 +1231,7 @@ infinity() -- returns Float64 (positive infinity) **Redefining a built-in is an error (E151)**: a function whose name matches a built-in (e.g. `abs`, `array_length`, `clamp`, `to_string`) is rejected at `vera check`. Built-ins are always in scope as the single canonical definition, so a second one is both redundant (one canonical form) and — for the verifier-modelled built-ins — silently unsound: the verifier would reason with the built-in's model while codegen runs your body. Call the built-in directly (no import needed), or give your function a distinct name (e.g. `magnitude`) for genuinely different behaviour. The one exception is the prelude's Option/Result/Json/Html *combinators* (`option_map`, `option_and_then`, `option_unwrap_or`, `result_map`, `result_unwrap_or`, `json_*`, `html_attr`): these are ordinary Vera functions the prelude injects, so a same-named user definition soundly replaces them. -**`old` and `new` are not available as function names (E153)**: both are contract state forms, so `old(...)` / `new(...)` in expression position always parses as a reference to an effect's before/after state (Chapter 7, Section 7.9.2) and never as a call. A `fn old` or `fn new` — top-level, `where`-helper, or in an imported module — could therefore never be called, and is rejected at `vera check`. Rename it. Only the exact identifiers are reserved: `older`, `renew`, and the like are ordinary function names. +**Reserved function names (E153)**: an identifier the grammar claims in expression position cannot be a function name. Two groups. `old` and `new` are contract state forms, so `old(...)` / `new(...)` always parses as a reference to an effect's before/after state (Chapter 7, Section 7.9.2) and never as a call. `assert`, `assume`, `forall`, `exists`, `match`, `if`, `let`, `fn`, `true` and `false` are keywords the lexer admits as a name after `fn` but reads as the keyword everywhere else, so `match(3)` in a body does not parse as a call either. A function under any of these — top-level, `where`-helper, or in an imported module — could never be called, and is rejected at `vera check`. Rename it. Only the exact identifiers are reserved: `older`, `renew`, `matched` and the like are ordinary function names. `handle` is the one keyword still available, because `public fn handle(@Request -> @Response)` is the entry point `vera serve` invokes from the host (Chapter 9, Section 9.5.6). Example: @@ -2370,7 +2370,7 @@ public fn main(@Unit -> @Unit) ## Conformance Suite -The `tests/conformance/` directory contains 175 small programs — most self-contained, with the Chapter 8 module-system programs and a few cross-module Chapter 7 and 9 programs importing companion `_lib.vera` / `_mid.vera` modules — that validate every language feature against the spec — often one program per feature, though some features (slot references, match, contracts) span several. These are the best minimal working examples of Vera syntax and semantics. +The `tests/conformance/` directory contains 176 small programs — most self-contained, with the Chapter 8 module-system programs and a few cross-module Chapter 7 and 9 programs importing companion `_lib.vera` / `_mid.vera` modules — that validate every language feature against the spec — often one program per feature, though some features (slot references, match, contracts) span several. These are the best minimal working examples of Vera syntax and semantics. Each program is organized by spec chapter (`ch01_int_literals.vera`, `ch04_match_basic.vera`, `ch07_state_handler.vera`, etc.) and the `manifest.json` file maps features to programs. When you need to see how a specific construct works, check the conformance program before reading the spec. diff --git a/docs/index.html b/docs/index.html index 81280116..ff3ae354 100644 --- a/docs/index.html +++ b/docs/index.html @@ -699,7 +699,7 @@

This page is also a machine-readable specificati Vera is under active development

- A complete compiler with 164 built-in functions, ten algebraic effects (IO, Http, HttpServer, State, Exceptions, Async, Inference, DB, Random, Diverge), contract-driven testing via Z3, a language server with agent-facing proof deltas, and a 14-chapter specification. A 175-program conformance suite and 42 worked examples are validated against the spec on every pull request. All of it is developed openly on GitHub and released under the MIT licence. + A complete compiler with 164 built-in functions, ten algebraic effects (IO, Http, HttpServer, State, Exceptions, Async, Inference, DB, Random, Diverge), contract-driven testing via Z3, a language server with agent-facing proof deltas, and a 14-chapter specification. A 176-program conformance suite and 42 worked examples are validated against the spec on every pull request. All of it is developed openly on GitHub and released under the MIT licence.

diff --git a/docs/index.md b/docs/index.md index 58c4d57f..56c17d2f 100644 --- a/docs/index.md +++ b/docs/index.md @@ -281,7 +281,7 @@ For other models: point them at [`SKILL.md`](https://veralang.dev/SKILL.md) via ## Status -Vera is under [active development](https://raw.githubusercontent.com/aallan/vera/main/ROADMAP.md). A complete compiler with 164 built-in functions, ten algebraic effects (IO, Http, HttpServer, State, Exceptions, Async, Inference, DB, Random, Diverge), contract-driven testing via [Z3](https://www.microsoft.com/en-us/research/project/z3-3/), and a 14-chapter specification. A 175-program conformance suite and 42 worked examples are validated against the spec on every pull request. All of it is developed openly on [GitHub](https://github.com/aallan/vera) and released under the MIT licence. +Vera is under [active development](https://raw.githubusercontent.com/aallan/vera/main/ROADMAP.md). A complete compiler with 164 built-in functions, ten algebraic effects (IO, Http, HttpServer, State, Exceptions, Async, Inference, DB, Random, Diverge), contract-driven testing via [Z3](https://www.microsoft.com/en-us/research/project/z3-3/), and a 14-chapter specification. A 176-program conformance suite and 42 worked examples are validated against the spec on every pull request. All of it is developed openly on [GitHub](https://github.com/aallan/vera) and released under the MIT licence. ## Links diff --git a/docs/llms-full.txt b/docs/llms-full.txt index ab1a2cf1..61201e9d 100644 --- a/docs/llms-full.txt +++ b/docs/llms-full.txt @@ -1237,7 +1237,7 @@ infinity() -- returns Float64 (positive infinity) **Redefining a built-in is an error (E151)**: a function whose name matches a built-in (e.g. `abs`, `array_length`, `clamp`, `to_string`) is rejected at `vera check`. Built-ins are always in scope as the single canonical definition, so a second one is both redundant (one canonical form) and — for the verifier-modelled built-ins — silently unsound: the verifier would reason with the built-in's model while codegen runs your body. Call the built-in directly (no import needed), or give your function a distinct name (e.g. `magnitude`) for genuinely different behaviour. The one exception is the prelude's Option/Result/Json/Html *combinators* (`option_map`, `option_and_then`, `option_unwrap_or`, `result_map`, `result_unwrap_or`, `json_*`, `html_attr`): these are ordinary Vera functions the prelude injects, so a same-named user definition soundly replaces them. -**`old` and `new` are not available as function names (E153)**: both are contract state forms, so `old(...)` / `new(...)` in expression position always parses as a reference to an effect's before/after state (Chapter 7, Section 7.9.2) and never as a call. A `fn old` or `fn new` — top-level, `where`-helper, or in an imported module — could therefore never be called, and is rejected at `vera check`. Rename it. Only the exact identifiers are reserved: `older`, `renew`, and the like are ordinary function names. +**Reserved function names (E153)**: an identifier the grammar claims in expression position cannot be a function name. Two groups. `old` and `new` are contract state forms, so `old(...)` / `new(...)` always parses as a reference to an effect's before/after state (Chapter 7, Section 7.9.2) and never as a call. `assert`, `assume`, `forall`, `exists`, `match`, `if`, `let`, `fn`, `true` and `false` are keywords the lexer admits as a name after `fn` but reads as the keyword everywhere else, so `match(3)` in a body does not parse as a call either. A function under any of these — top-level, `where`-helper, or in an imported module — could never be called, and is rejected at `vera check`. Rename it. Only the exact identifiers are reserved: `older`, `renew`, `matched` and the like are ordinary function names. `handle` is the one keyword still available, because `public fn handle(@Request -> @Response)` is the entry point `vera serve` invokes from the host (Chapter 9, Section 9.5.6). Example: @@ -2376,7 +2376,7 @@ public fn main(@Unit -> @Unit) ## Conformance Suite -The `tests/conformance/` directory contains 175 small programs — most self-contained, with the Chapter 8 module-system programs and a few cross-module Chapter 7 and 9 programs importing companion `_lib.vera` / `_mid.vera` modules — that validate every language feature against the spec — often one program per feature, though some features (slot references, match, contracts) span several. These are the best minimal working examples of Vera syntax and semantics. +The `tests/conformance/` directory contains 176 small programs — most self-contained, with the Chapter 8 module-system programs and a few cross-module Chapter 7 and 9 programs importing companion `_lib.vera` / `_mid.vera` modules — that validate every language feature against the spec — often one program per feature, though some features (slot references, match, contracts) span several. These are the best minimal working examples of Vera syntax and semantics. Each program is organized by spec chapter (`ch01_int_literals.vera`, `ch04_match_basic.vera`, `ch07_state_handler.vera`, etc.) and the `manifest.json` file maps features to programs. When you need to see how a specific construct works, check the conformance program before reading the spec. @@ -2454,7 +2454,7 @@ Read `SKILL.md` for the full language reference. It covers syntax, slot referenc ### Conformance programs as reference -The conformance suite in `tests/conformance/` contains 175 small, self-contained programs — often one per language feature — that serve as minimal working examples (most are fully self-contained; the cross-module programs of Chapters 7–9 import companion `_lib`/module fixtures). Each positive program must pass its declared verification level (see `manifest.json` for mappings: `parse`, `check`, `verify`, or `run`); the twenty-two negative fixtures (`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_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch07_bare_effect_op_rejected`) instead must *fail* `check` with the E-code in their `expected_error` field. When you need to see how a specific construct works (e.g. effect handlers, match expressions, closures), check the corresponding conformance program before reading the spec. +The conformance suite in `tests/conformance/` contains 176 small, self-contained programs — often one per language feature — that serve as minimal working examples (most are fully self-contained; the cross-module programs of Chapters 7–9 import companion `_lib`/module fixtures). Each positive program must pass its declared verification level (see `manifest.json` for mappings: `parse`, `check`, `verify`, or `run`); the twenty-three negative fixtures (`ch02_generic_over_unit_rejected`, `ch02_map_unit_value_rejected`, `ch04_let_unit_rejected`, `ch05_apply_fn_arity`, `ch05_decreases_float_rejected`, `ch05_reserved_fn_name_rejected`, `ch05_reserved_keyword_fn_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch07_bare_effect_op_rejected`) instead must *fail* `check` with the E-code in their `expected_error` field. When you need to see how a specific construct works (e.g. effect handlers, match expressions, closures), check the corresponding conformance program before reading the spec. ### Workflow @@ -2631,7 +2631,7 @@ Each stage is a module with a single public API function (`parse_file`, `transfo pytest tests/ -v # Run all tests (see TESTING.md) pytest tests/test_conformance.py -v # Conformance suite only mypy vera/ # Type-check the compiler -python scripts/check_conformance.py # All 175 conformance programs hold (positives pass; negatives fail with their E-code) +python scripts/check_conformance.py # All 176 conformance programs hold (positives pass; negatives fail with their E-code) python scripts/check_examples.py # All 42 examples must pass python scripts/check_corpus_canonical.py # All 217 corpus programs in canonical form ``` @@ -2642,7 +2642,7 @@ When implementing a new language feature, write the conformance program *first* ### Invariants -- All 175 conformance programs in `tests/conformance/` must hold at their declared level — positive entries pass, and the negative fixtures (`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_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch07_bare_effect_op_rejected`) must *fail* `check` with their `expected_error` E-code +- All 176 conformance programs in `tests/conformance/` must hold at their declared level — positive entries pass, and the negative fixtures (`ch02_generic_over_unit_rejected`, `ch02_map_unit_value_rejected`, `ch04_let_unit_rejected`, `ch05_apply_fn_arity`, `ch05_decreases_float_rejected`, `ch05_reserved_fn_name_rejected`, `ch05_reserved_keyword_fn_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch07_bare_effect_op_rejected`) must *fail* `check` with their `expected_error` E-code - All 42 examples in `examples/` must pass `vera check` and `vera verify` - `mypy vera/` must be clean - `pytest tests/ -v` must pass @@ -3115,7 +3115,7 @@ None of this is Vera-specific, but it validates the design choices. The thesis i This is a real concern. LLMs are trained on trillions of tokens of Python, TypeScript, and JavaScript. A MojoBench study (NAACL 2025) found that even fine-tuned models achieved only 30–35% improvement over base models on Mojo code generation, illustrating the cold-start problem for new languages. -Vera's approach has three parts. First, the agent-facing documentation (SKILL.md) is designed to be dropped into a model's context window, so the model works from the language specification rather than training data recall. Second, Vera's syntax is deliberately simple and regular — fewer constructs, each with exactly one canonical form — which reduces the surface area a model needs to learn. Third, the conformance test suite (175 programs covering every language feature) gives models concrete examples to learn from and conform to. Simon Willison's December 2025 JustHTML write-up illustrates the same point in practice: an LLM-assisted implementation, guided by the html5lib conformance suite, conformed to the HTML parsing spec by running against its tests — a comprehensive test suite is a strong scaffold for a model implementing to a specification. +Vera's approach has three parts. First, the agent-facing documentation (SKILL.md) is designed to be dropped into a model's context window, so the model works from the language specification rather than training data recall. Second, Vera's syntax is deliberately simple and regular — fewer constructs, each with exactly one canonical form — which reduces the surface area a model needs to learn. Third, the conformance test suite (176 programs covering every language feature) gives models concrete examples to learn from and conform to. Simon Willison's December 2025 JustHTML write-up illustrates the same point in practice: an LLM-assisted implementation, guided by the html5lib conformance suite, conformed to the HTML parsing spec by running against its tests — a comprehensive test suite is a strong scaffold for a model implementing to a specification. ## How does Vera compare to Dafny / Lean / Koka / F*? @@ -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,796 tests, including a 175-program conformance suite +- 8,840 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 24ee6225..579a3b51 100644 --- a/docs/llms.txt +++ b/docs/llms.txt @@ -56,4 +56,4 @@ Current version: 0.1.8. The reference compiler is written in Python. Install the - [TESTING.md](https://raw.githubusercontent.com/aallan/vera/main/TESTING.md): Test suite architecture, coverage data, and test conventions. - [KNOWN_ISSUES.md](https://raw.githubusercontent.com/aallan/vera/main/KNOWN_ISSUES.md): Known bugs and limitations. - [CONTRIBUTING.md](https://raw.githubusercontent.com/aallan/vera/main/CONTRIBUTING.md): Contribution guidelines. -- [Conformance Suite](https://github.com/aallan/vera/tree/main/tests/conformance): 175 programs validating every language feature against the spec. +- [Conformance Suite](https://github.com/aallan/vera/tree/main/tests/conformance): 176 programs validating every language feature against the spec. diff --git a/spec/05-functions.md b/spec/05-functions.md index eae001ac..b54a7c90 100644 --- a/spec/05-functions.md +++ b/spec/05-functions.md @@ -27,7 +27,17 @@ private fn function_name(@ParamType1, @ParamType2 -> @ReturnType) } ``` -Two identifiers are unavailable as function names: `old` and `new`. Both are contract state forms — in expression position `old(...)` and `new(...)` name an effect's state before and after a call, and take an effect reference rather than an arbitrary expression (Chapter 7, Section 7.9.2). A bare call written `old(x)` is therefore always read as a state reference, never as a function call: a function under either name cannot be called from its own file, and a module cannot call its own export. The only route that reaches one is a module-qualified call (`mod::old(...)`, Chapter 8), which parses through the module-call rule — leaving the name a trap in every unqualified position and half-usable cross-module. Vera reserves the whole identifier instead: declaring a function named `old` or `new` is a compile error (**E153**); rename the function. The restriction is on the whole identifier, so names that merely begin with a reserved word — `older`, `renew` — are ordinary function names. The same one-canonical-form reasoning rejects redefining a built-in function (**E151**, Chapter 9, Section 9.6) and redeclaring a built-in effect (**E152**, Chapter 9, Section 9.5.1). +An identifier the grammar claims in expression position is unavailable as a function name. Two groups are affected. + +The first is the contract state forms `old` and `new` — in expression position `old(...)` and `new(...)` name an effect's state before and after a call, and take an effect reference rather than an arbitrary expression (Chapter 7, Section 7.9.2). A bare call written `old(x)` is therefore always read as a state reference, never as a function call. + +The second is the keywords the lexer admits as a name after `fn` but reads as the keyword everywhere else: `assert`, `assume`, `forall`, `exists`, `match`, `if`, `let`, `fn`, `true`, and `false`. A body containing `match(x)` does not parse as a call at all. + +In both groups the declaration parses and no bare call can reach it: a function under such a name cannot be called from its own file, and a module cannot call its own export. The only route that reaches one is a module-qualified call (`mod::old(...)`, Chapter 8), which parses through the module-call rule — leaving the name a trap in every unqualified position and half-usable cross-module. Vera reserves the whole identifier instead: declaring a function under any of these names is a compile error (**E153**); rename the function. The restriction is on the whole identifier, so names that merely begin with a reserved word — `older`, `renew`, `matched` — are ordinary function names. + +`handle` is the one exception. It is a keyword, and equally uncallable from Vera source, but `public fn handle(@Request -> @Response)` is the entry point a *host* invokes under `vera serve` and `wasi:http` (Chapter 9, Section 9.5.6), so it is not dead code and stays legal. A future host-invoked entry point is exempted on the same grounds; nothing else is. + +The same one-canonical-form reasoning rejects redefining a built-in function (**E151**, Chapter 9, Section 9.6) and redeclaring a built-in effect (**E152**, Chapter 9, Section 9.5.1). ### 5.2.1 Complete Example diff --git a/tests/conformance/ch05_reserved_keyword_fn_rejected.vera b/tests/conformance/ch05_reserved_keyword_fn_rejected.vera new file mode 100644 index 00000000..0ae6a84c --- /dev/null +++ b/tests/conformance/ch05_reserved_keyword_fn_rejected.vera @@ -0,0 +1,23 @@ +-- Conformance: a keyword is not available as a function name (Chapter 5, Section 5.2) +-- Tests: E153 — a user fn named after a grammar keyword is rejected at its +-- declaration (#1187). Lark's contextual lexer re-lexes `match` as an +-- identifier after `fn`, so the declaration parses; in a body `match` is +-- always the keyword, so `match(3)` fails to parse (E005) and this function +-- could never be called. Rejecting the declaration refuses the dead code at +-- its source. `handle` is carved out — it is the host-invoked `vera serve` +-- entry point (Chapter 9, Section 9.5.6). +public fn match(@Int -> @Int) + requires(true) + ensures(@Int.result >= 0) + effects(pure) +{ + 5 +} + +public fn main(@Unit -> @Int) + requires(true) + ensures(true) + effects(pure) +{ + 0 +} diff --git a/tests/conformance/manifest.json b/tests/conformance/manifest.json index d945a7bf..b7914a0b 100644 --- a/tests/conformance/manifest.json +++ b/tests/conformance/manifest.json @@ -934,6 +934,20 @@ "check_error" ] }, + { + "id": "ch05_reserved_keyword_fn_rejected", + "file": "ch05_reserved_keyword_fn_rejected.vera", + "chapter": 5, + "title": "A function named after a grammar keyword is a checker error (#1187)", + "level": "check", + "spec_ref": "Section 5.2", + "expected_error": "E153", + "features": [ + "reserved_fn_name", + "function_declaration", + "check_error" + ] + }, { "id": "ch06_requires", "file": "ch06_requires.vera", diff --git a/tests/test_checker_modules.py b/tests/test_checker_modules.py index 5a433b95..ea865c5a 100644 --- a/tests/test_checker_modules.py +++ b/tests/test_checker_modules.py @@ -962,29 +962,22 @@ class TestReservedFnName: functions) and E152 (built-in effects), and the same DESIGN.md "one canonical form" / fail-loud rule. - **Why the set is exactly** ``{old, new}``. Every candidate below was - probed by declaring ``private fn (@Int -> @Int)`` and then calling + **Where the state-form piece sits.** Every candidate below was probed by + declaring ``private fn (@Int -> @Int)`` and then calling ``(3)`` from ``main``: * ``old``, ``new`` — declaration accepted, call rejected (E030 / E031). - Reserved here. + Reserved here, as ``_STATE_FORM_FN_NAMES``. * ``resume``, ``throw``, ``with``, ``in``, ``effect``, ``op``, ``data``, ``type``, ``import``, ``public``, ``private``, ``requires``, ``ensures``, ``effects``, ``decreases``, ``where``, ``then``, ``else``, ``pure``, ``invariant`` — declaration *and* call both accepted. Not reserved; nothing is wrong with them. - * ``assert``, ``assume``, ``forall``, ``exists``, ``handle``, ``match``, - ``if``, ``let``, ``fn``, ``true``, ``false`` — Lark's contextual lexer - re-lexes these keywords as ``LOWER_IDENT`` in declaration position, so - they declare fine, and a bare ``(3)`` does not parse as a call - either. They are deliberately **not** in the set: ``handle`` disproves - "uncallable from expression position" as a sufficient criterion on its - own, because ``public fn handle(@Request -> @Response)`` is the - ``vera serve`` entry point (spec §9.5.6, ``examples/http_server.vera``) - — invoked by the host, never from Vera source, and entirely legitimate. - Banning keywords as function names is a separate, broader rule that - would need its own carve-outs; #1181 is about the two names the - *contract state forms* reserve. + * ``assert``, ``assume``, ``forall``, ``exists``, ``match``, ``if``, + ``let``, ``fn``, ``true``, ``false`` — the keyword class, reserved by + #1187 as ``_KEYWORD_FN_NAMES``; ``handle`` is carved back out as a + host-invoked entry point. :class:`TestReservedKeywordFnName` below + owns that half of the gate. """ @staticmethod @@ -1210,6 +1203,269 @@ def test_effect_op_named_old_never_reaches_the_gate(self) -> None: assert exc.value.diagnostic.error_code == "E030" +# ===================================================================== +# Reserved keyword function names (E153) — #1187 +# ===================================================================== + + +class TestReservedKeywordFnName: + """A ``fn`` named after a grammar keyword is rejected (E153, #1187). + + Lark's contextual lexer re-lexes each of these keywords as + ``LOWER_IDENT`` in *declaration* position, so ``private fn match(...)`` + declares happily. None of them can be written in *expression* position: + a bare ``match(3)`` fails to parse (``[E005]``), and ``assert(3)`` / + ``assume(3)`` are read as the statement forms and collide + (``[E121]`` + ``[E172]``/``[E173]``). Every one is therefore a + declarable trap, and #1187 refuses it at the declaration — the same + one-canonical-form rule as ``old``/``new`` (E153, #1181), E151 (built-in + functions) and E152 (built-in effects). + + **Probe record** (run against the pre-#1187 tree, one row per name, + ``private fn (@Int -> @Int)`` plus ``(3)`` in ``main``): + + * ``assert``, ``assume`` — declaration accepted, bare call reaches the + statement form and fails ``[E121]`` + ``[E172]``/``[E173]``. + * ``forall``, ``exists``, ``match``, ``if``, ``let``, ``fn``, ``true``, + ``false``, ``handle`` — declaration accepted, bare call ``[E005]`` + (does not parse as a call at all). + * A module-qualified ``mod::(5)`` type-checked **and ran** for + every one of the eleven (``vera run`` printed 6 for ``match``) — + exactly the half-usable-cross-module shape #1181 found for ``old``. + Reserving the name closes it deliberately; see + ``test_module_qualified_keyword_call_route_is_closed``. + * ``op (...)`` inside an ``effect`` block does *not* parse + (``[E005]``), so no effect-operation carve-out is needed; pinned by + ``test_effect_op_named_match_never_reaches_the_gate``. + + ``handle`` is the one carve-out: ``public fn handle(@Request -> + @Response)`` is the host-invoked ``vera serve`` / ``wasi:http`` entry + point (spec §9.5.6), called by the host rather than from Vera source, so + "uncallable from expression position" does not make it dead code. It + lives in a named ``_HOST_INVOKED_FN_NAMES`` set subtracted from the + reservation, pinned by ``test_handle_stays_legal``. + """ + + #: Every keyword the reservation covers (``handle`` deliberately absent). + KEYWORDS = ( + "assert", "assume", "forall", "exists", "match", + "if", "let", "fn", "true", "false", + ) + + @staticmethod + def _codes(errs: list[Diagnostic]) -> list[str]: + return [e.error_code for e in errs] + + @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.""" + errs = _errors(f""" +public fn {name}(@Int -> @Int) + requires(true) ensures(@Int.result >= 0) effects(pure) +{{ 5 }} +""") + assert "E153" in self._codes(errs), (name, self._codes(errs)) + diag = next(e for e in errs if e.error_code == "E153") + assert name in diag.description, diag.description + assert "reserved" in diag.description.lower(), diag.description + # Instructional on the keyword branch too (check_diagnostic_fields). + assert diag.rationale and diag.fix and diag.spec_ref + assert "Chapter 5" in diag.spec_ref, diag.spec_ref + assert "rename" in diag.fix.lower(), diag.fix + + @pytest.mark.parametrize("name", KEYWORDS) + def test_private_keyword_fn_name_is_E153(self, name: str) -> None: + """Visibility-independent, as the ``old``/``new`` branch is.""" + errs = _errors(f""" +private fn {name}(@Int -> @Int) + requires(true) ensures(@Int.result >= 0) effects(pure) +{{ 5 }} +""") + assert "E153" in self._codes(errs), (name, self._codes(errs)) + + def test_keyword_rationale_is_not_the_state_form_rationale(self) -> None: + """The two branches explain themselves differently. + + ``old``/``new`` are reserved because they are *contract state forms*; + a keyword is reserved because the grammar claims the spelling in + expression position. Reusing the state-form wording for ``match`` + would tell the reader a falsehood about why their program is wrong, + so pin that the keyword branch says neither. + """ + kw = next( + e for e in _errors(""" +public fn match(@Int -> @Int) + requires(true) ensures(true) effects(pure) +{ 5 } +""") if e.error_code == "E153" + ) + assert "state form" not in kw.rationale.lower(), kw.rationale + assert "keyword" in kw.rationale.lower(), kw.rationale + # And the old/new branch keeps its own explanation. + state = next( + e for e in _errors(""" +public fn old(@Int -> @Int) + requires(true) ensures(true) effects(pure) +{ 5 } +""") if e.error_code == "E153" + ) + assert "state form" in state.rationale.lower(), state.rationale + + def test_handle_stays_legal(self) -> None: + """``handle`` is carved out — CRITICAL positive control. + + ``public fn handle(@Request -> @Response)`` is the ``vera serve`` / + ``wasi:http`` entry point (spec §9.5.6), invoked by the *host*, so it + is legitimate despite being uncallable from Vera source. This is the + shape of ``examples/http_server.vera`` and + ``tests/conformance/ch09_http_server.vera``; if the reservation ever + swallows it, both break and `vera serve` loses its entry point. + """ + errs = _errors(""" +public fn handle(@Request -> @Response) + requires(true) ensures(true) effects() +{ + match @Request.0 { + Request(@String, @String, @Map, @String) -> + Response(200, map_new(), @String.0) + } +} +""") + assert self._codes(errs) == [], self._codes(errs) + + def test_where_helper_named_match_is_E153(self) -> None: + """The where-helper recursion covers keywords too. + + A helper is called in expression position exactly like a top-level + function, so ``match(...)`` in the parent body hits the same grammar + wall one scope deeper. Inherited from the set-driven gate; pinned so + a future refactor that splits the branches cannot drop it. + """ + errs = _errors(""" +public fn caller(@Int -> @Int) + requires(true) ensures(@Int.result >= 0) effects(pure) +{ @Int.0 } +where { + fn match(@Int -> @Int) + requires(true) ensures(true) effects(pure) + { 5 } +} +""") + assert "E153" in self._codes(errs), self._codes(errs) + + def test_keyword_E153_is_the_only_diagnostic(self) -> None: + """The rejection must not cascade into secondary errors.""" + errs = _errors(""" +public fn match(@Int -> @Int) + requires(true) ensures(@Int.result >= 0) effects(pure) +{ 5 } + +public fn main(@Unit -> @Int) + requires(true) ensures(true) effects(pure) +{ 0 } +""") + codes = self._codes(errs) + assert "E153" in codes, codes + assert [c for c in codes if c != "E153"] == [], codes + + def test_names_merely_beginning_with_a_keyword_are_allowed(self) -> None: + """Whole-identifier matching, not prefix matching. + + The grammar reserves the exact tokens only, so ``matched(3)`` and + friends parse as ordinary calls and must stay legal — a naive + ``startswith`` would break every one of them. + """ + for name in ("matched", "iffy", "letter", "asserting", "forall2", + "existsp", "fnord", "truthy", "falsey", "assumed", + "handler"): + errs = _errors(f""" +public fn {name}(@Int -> @Int) + requires(true) ensures(@Int.result >= 0) effects(pure) +{{ 5 }} + +public fn main(@Unit -> @Int) + requires(true) ensures(true) effects(pure) +{{ {name}(3) }} +""") + assert self._codes(errs) == [], (name, self._codes(errs)) + + def test_imported_module_fn_named_match_is_E153(self) -> None: + """A module declaring ``fn match`` surfaces E153 into its importer, + carrying the *module's* file path — same mechanism as E151/E152 and + the ``old``/``new`` branch.""" + mod_src = ( + "module lexy;\n" + "public fn match(@Int -> @Int)\n" + " requires(true) ensures(@Int.result >= 0) effects(pure)\n" + "{ 5 }\n" + ) + mod = _resolved_module(("lexy",), mod_src) + prog = parse_to_ast( + "import lexy;\n" + "public fn main(@Unit -> @Int)\n" + " requires(true) ensures(true) effects(pure)\n" + "{ 0 }\n" + ) + diags = typecheck(prog, source="", resolved_modules=[mod]) + codes = [d.error_code for d in diags] + assert "E153" in codes, codes + e153 = next(d for d in diags if d.error_code == "E153") + assert e153.location.file == str(mod.file_path), e153.location.file + + def test_module_qualified_keyword_call_route_is_closed(self) -> None: + """E153 fires even where a qualified call site proved reachability. + + Probed on the pre-#1187 tree: this exact program — module export + named ``match``, importer calling ``lexy::match(5)`` — type-checked + AND ran, printing 6. The qualified route parses through the + module-call rule rather than any keyword rule, so "no program can + reach it" was false for module exports, exactly as #1181 found for + ``old``. The reservation closes the route deliberately (breaking for + such an export) and the breakage is loud and located at the module's + declaration. + """ + mod_src = ( + "module lexy;\n" + "public fn match(@Int -> @Int)\n" + " requires(true) ensures(true) effects(pure)\n" + "{ @Int.0 + 1 }\n" + ) + mod = _resolved_module(("lexy",), mod_src) + prog = parse_to_ast( + "import lexy;\n" + "public fn main(@Unit -> @Int)\n" + " requires(true) ensures(true) effects(pure)\n" + "{ lexy::match(5) }\n" + ) + diags = typecheck(prog, source="", resolved_modules=[mod]) + codes = [d.error_code for d in diags] + assert "E153" in codes, codes + e153 = next(d for d in diags if d.error_code == "E153") + assert e153.location.file == str(mod.file_path), e153.location.file + + @pytest.mark.parametrize("name", [*KEYWORDS, "handle"]) + def test_effect_op_named_match_never_reaches_the_gate( + self, name: str, + ) -> None: + """Boundary pin: ``op (...)`` is refused by the grammar. + + The contextual lexer admits a keyword as a ``fn`` name but not as an + ``op`` name, so ``op match(@Int -> @Int)`` fails at parse with + ``[E005]`` and the gate — which covers ``fn`` declarations only — + never has to see it. ``handle`` is included: its carve-out is for + ``fn`` declarations, and does not (and need not) extend to ``op``. + Pinned so a grammar change admitting the ``op`` spelling shows up as + a failure to widen the gate rather than a silent reopening. + """ + with pytest.raises(ParseError) as exc: + parse_to_ast(f""" +effect Renamer {{ + op {name}(@Int -> @Int) +}} +""") + assert exc.value.diagnostic.error_code == "E005" + + # ===================================================================== # Module-qualified call parse tests (#95) # ===================================================================== diff --git a/vera/README.md b/vera/README.md index ef55856f..b04ab717 100644 --- a/vera/README.md +++ b/vera/README.md @@ -80,7 +80,7 @@ execute(compile_result, ...) # → run WASM via wasmtime | ` core.py` | 952 | | TypeChecker class, orchestration, contracts, constraint validation | | | ` resolution.py` | 419 | | AST TypeExpr → semantic Type, inference | | | ` modules.py` | 180 | | Cross-module registration (C7b/C7c) | | -| ` registration.py` | 597 | | Pass 1 forward declarations, ability registration | | +| ` registration.py` | 717 | | Pass 1 forward declarations, ability registration | | | ` expressions.py` | 1,335 | | Expression synthesis (bidirectional), operators, statements | | | ` eq_ability.py` | 199 | | Eq ability derivation checks | | | ` sql.py` | 308 | | SQL literal-provenance resolution + placeholder counting (#309) | `resolve_literal_string()`, `count_placeholders()` | diff --git a/vera/checker/modules.py b/vera/checker/modules.py index b5a8d687..cacebf3a 100644 --- a/vera/checker/modules.py +++ b/vera/checker/modules.py @@ -62,9 +62,10 @@ def _register_modules(self, program: ast.Program) -> None: # on the same grounds — the block is invisible to codegen, which # routes the qualified call to the host import regardless, so an # unchecked module would miscompile the importer. - # #1181: E153 (a module fn named after a contract state form) - # likewise — a module imported but never checked standalone would - # otherwise carry a declaration no importer could ever call. + # #1181/#1187: E153 (a module fn named after a contract state form + # or a grammar keyword) likewise — a module imported but never + # checked standalone would otherwise carry a declaration no + # importer could ever bare-call. self.errors.extend( e for e in temp.errors if e.error_code in ("E151", "E152", "E153", "E154") diff --git a/vera/checker/registration.py b/vera/checker/registration.py index bf1d1b73..652d6562 100644 --- a/vera/checker/registration.py +++ b/vera/checker/registration.py @@ -70,29 +70,50 @@ def builtin_effect_names() -> frozenset[str]: # Identifiers the grammar reserves in *expression* position, so a call to a -# same-named function can never parse (E153, #1181). ``old_expr`` and -# ``new_expr`` in ``vera/grammar.lark`` claim ``"old" "("`` and ``"new" "("`` -# for the contract state forms, and each demands an *effect reference* as its -# argument: ``old(5)`` is diagnosed as a malformed state reference -# (``[E030]``/``[E031]``, #1173), never resolved as a call. A *bare* call can -# therefore never reach such a function — not from its own file, not from a -# sibling in its own module, not from an importer. One route did reach it: -# a module-qualified ``mod::old(...)`` parses through the module-call rule, -# not the state-form rule, so a module export named ``old`` was previously -# callable cross-module (and only cross-module). The reservation closes that -# route deliberately: a name that is a trap in every unqualified position is -# reserved outright rather than left half-usable, the same one-canonical-form -# rule as E151/E152. +# same-named function can never parse (E153). A function under one of them is +# a declarable trap: it declares cleanly and no bare call site can reach it. +# The reservation refuses the mistake at its source rather than letting it +# surface later as a call-site error, the same one-canonical-form rule as E151 +# (built-in functions) and E152 (built-in effects). # -# The set is exactly the two contract state forms, and deliberately not every -# keyword the contextual lexer lets through as a function name (``assert``, -# ``assume``, ``forall``, ``exists``, ``handle``, ``match``, ``if``, ``let``, -# ``fn``, ``true``, ``false``). Being uncallable from expression position is -# not on its own grounds for rejection: a function can be an *entry point* the -# host invokes rather than Vera source — ``public fn handle(@Request -> -# @Response)`` is the ``vera serve`` handler (spec §9.5.6). Widening the rule -# to keywords is a separate decision that needs its own carve-outs. -_RESERVED_FN_NAMES = frozenset({"old", "new"}) +# The set is assembled from three named pieces so a future addition joins the +# right one deliberately. + +# 1. The two contract state forms (#1181). ``old_expr`` and ``new_expr`` in +# ``vera/grammar.lark`` claim ``"old" "("`` and ``"new" "("``, and each demands +# an *effect reference* as its argument: ``old(5)`` is diagnosed as a malformed +# state reference (``[E030]``/``[E031]``, #1173), never resolved as a call. +_STATE_FORM_FN_NAMES = frozenset({"old", "new"}) + +# 2. The keywords Lark's *contextual* lexer re-lexes as ``LOWER_IDENT`` in +# declaration position (#1187). Each declares fine and none can be written in +# expression position: a bare ``match(3)`` does not parse at all (``[E005]``), +# and ``assert(3)`` / ``assume(3)`` are read as the statement forms and collide +# (``[E121]`` + ``[E172]``/``[E173]``). Keywords the lexer does *not* admit as +# a function name (``resume``, ``with``, ``effect``, ``data``, …) need no entry +# here — the parser already refuses those declarations. +_KEYWORD_FN_NAMES = frozenset({ + "assert", "assume", "forall", "exists", "match", + "if", "let", "fn", "true", "false", "handle", +}) + +# 3. The carve-out: names a *host* invokes rather than Vera source, so being +# uncallable from expression position does not make them dead code. +# ``public fn handle(@Request -> @Response)`` is the ``vera serve`` / +# ``wasi:http`` entry point (spec §9.5.6, ``examples/http_server.vera``). A +# future host-invoked entry point joins this set — deliberately, with the same +# justification — rather than being dropped from the keyword list above. +_HOST_INVOKED_FN_NAMES = frozenset({"handle"}) + +# One route did reach a reserved name before it was reserved: a module-qualified +# ``mod::old(...)`` / ``mod::match(...)`` parses through the module-call rule +# rather than any reserved rule, so a module export under one of these names was +# callable cross-module (and only cross-module). The reservation closes that +# route deliberately — a name that is a trap in every unqualified position is +# reserved outright rather than left half-usable. +_RESERVED_FN_NAMES = ( + (_STATE_FORM_FN_NAMES | _KEYWORD_FN_NAMES) - _HOST_INVOKED_FN_NAMES +) def _strip_rejected_where_fns(decl: ast.FnDecl) -> ast.FnDecl: @@ -138,10 +159,11 @@ def _register_all(self, program: ast.Program) -> None: fix=f"private {kind} {name}(...) or public {kind} {name}(...)", spec_ref='Chapter 8, Section 8.4 "Visibility"', ) - # #1181: a fn named after a contract state form (`old` / `new`) - # could never be called, because the grammar claims those spellings - # in expression position. Checked before the E151 gate and without - # affecting its control flow, so the two rules stay independent. + # #1181/#1187: a fn named after a contract state form (`old` / + # `new`) or a grammar keyword (`match`, `let`, …) could never be + # called, because the grammar claims those spellings in expression + # position. Checked before the E151 gate and without affecting its + # control flow, so the two rules stay independent. if isinstance(tld.decl, ast.FnDecl): self._check_reserved_fn_name(tld.decl) # #815: redefining a built-in is a one-canonical-form violation @@ -287,11 +309,16 @@ def _check_reserved_type_name( def _check_reserved_fn_name(self, decl: ast.FnDecl) -> None: """Emit E153 if ``decl`` — or a nested where-helper — is named after a - contract state form (#1181). + contract state form (#1181) or a grammar keyword (#1187). Recurses into ``where_fns``: a helper is called in expression position - exactly like a top-level function, so a helper named ``old`` is - unreachable for the same reason, one scope deeper. + exactly like a top-level function, so a helper named ``old`` or + ``match`` is unreachable for the same reason, one scope deeper. + + The rationale branches on which piece of :data:`_RESERVED_FN_NAMES` + the name came from — the two are reserved for different reasons, and + telling a reader that ``match`` is a "contract state form" would be + false. The fix is the same on both branches: rename. The rejected declaration is still registered, unlike E151's. There is no canonical built-in for the name to shadow here — nothing can resolve @@ -300,10 +327,8 @@ def _check_reserved_fn_name(self, decl: ast.FnDecl) -> None: """ if decl.name in _RESERVED_FN_NAMES: n = decl.name - self._error( - decl, - f"Function name '{n}' is reserved.", - rationale=( + if n in _STATE_FORM_FN_NAMES: + rationale = ( f"'{n}' is a contract state form, not an ordinary " f"identifier: the grammar reads '{n}(' in expression " f"position as a reference to an effect's " @@ -313,15 +338,45 @@ def _check_reserved_fn_name(self, decl: ast.FnDecl) -> None: 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." - ), - fix=( + ) + fix = ( f"Rename the function to an identifier that is not a " f"contract state form (e.g. '{n}_value' or " f"'{'previous' if n == 'old' else 'updated'}') and " f"update its call sites. Only the exact spellings 'old' " f"and 'new' are reserved — 'older' and 'renew' are " f"ordinary function names." - ), + ) + else: + rationale = ( + f"'{n}' is a keyword the grammar reserves in expression " + f"position, not an ordinary identifier. The declaration " + 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." + ) + fix = ( + f"Rename the function to an identifier that is not a " + f"keyword — '{n}_fn', or better a name describing what " + f"it computes — and update its call sites. The " + f"reservation is on the whole identifier, so a longer " + f"name that merely begins with '{n}' (such as " + f"'{n}_value') is an ordinary function name. 'handle' is " + f"the one keyword still available, because 'vera serve' " + f"invokes 'handle(@Request -> @Response)' from the host " + f"rather than from Vera source." + ) + self._error( + decl, + f"Function name '{n}' is reserved.", + rationale=rationale, + fix=fix, spec_ref='Chapter 5, Section 5.2 "Function Declaration Syntax"', error_code="E153", )