diff --git a/AGENTS.md b/AGENTS.md index dc29f275..f0f8b9dd 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 243 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 thirty-seven 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_reserved_resume_fn_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch08_ambiguous_import_adt_rejected`, `ch08_ambiguous_import_adt_swapped_rejected`, `ch08_ambiguous_import_rejected`, `ch08_ambiguous_import_swapped_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_reserved_vera_prefix_reference_rejected`, `ch08_reserved_vera_prefix_binder_rejected`, `ch08_reserved_vera_prefix_effect_rejected`, `ch08_reserved_vera_prefix_ability_rejected`, `ch08_reserved_vera_prefix_constructor_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch07_bare_effect_op_rejected`, `ch06_quantifier_array_domain_rejected`, `ch07_handler_state_type_mismatch_rejected`, `ch02_alias_cycle_rejected`, `ch08_module_prelude_adt_contention_rejected`) instead must *fail* with the E-code in their `expected_error` field, at the stage their `expected_error_stage` names — `check` by default, or `compile` for a diagnostic the checker accepts and codegen refuses. 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 244 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 thirty-eight 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_reserved_contextual_keyword_fn_rejected`, `ch05_reserved_resume_fn_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch08_ambiguous_import_adt_rejected`, `ch08_ambiguous_import_adt_swapped_rejected`, `ch08_ambiguous_import_rejected`, `ch08_ambiguous_import_swapped_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_reserved_vera_prefix_reference_rejected`, `ch08_reserved_vera_prefix_binder_rejected`, `ch08_reserved_vera_prefix_effect_rejected`, `ch08_reserved_vera_prefix_ability_rejected`, `ch08_reserved_vera_prefix_constructor_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch07_bare_effect_op_rejected`, `ch06_quantifier_array_domain_rejected`, `ch07_handler_state_type_mismatch_rejected`, `ch02_alias_cycle_rejected`, `ch08_module_prelude_adt_contention_rejected`) instead must *fail* with the E-code in their `expected_error` field, at the stage their `expected_error_stage` names — `check` by default, or `compile` for a diagnostic the checker accepts and codegen refuses. 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 @@ -187,9 +187,9 @@ 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 243 conformance programs hold (positives pass; negatives fail with their E-code) +python scripts/check_conformance.py # All 244 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 292 corpus programs in canonical form +python scripts/check_corpus_canonical.py # All 293 corpus programs in canonical form ``` Test helpers follow a pattern: `_check_ok(source)` / `_check_err(source, match)` / `_verify_ok(source)` / `_verify_err(source, match)`. See existing tests for examples. @@ -198,7 +198,7 @@ When implementing a new language feature, write the conformance program *first* ### Invariants -- All 243 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_reserved_resume_fn_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch08_ambiguous_import_adt_rejected`, `ch08_ambiguous_import_adt_swapped_rejected`, `ch08_ambiguous_import_rejected`, `ch08_ambiguous_import_swapped_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_reserved_vera_prefix_reference_rejected`, `ch08_reserved_vera_prefix_binder_rejected`, `ch08_reserved_vera_prefix_effect_rejected`, `ch08_reserved_vera_prefix_ability_rejected`, `ch08_reserved_vera_prefix_constructor_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch07_bare_effect_op_rejected`, `ch06_quantifier_array_domain_rejected`, `ch07_handler_state_type_mismatch_rejected`, `ch02_alias_cycle_rejected`, `ch08_module_prelude_adt_contention_rejected`) must *fail* with their `expected_error` E-code, at the stage `expected_error_stage` names — `check` by default, or `compile` for a diagnostic the checker accepts and codegen refuses (`ch08_module_prelude_adt_contention_rejected` → E621), which also asserts the program type-checks cleanly first +- All 244 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_reserved_contextual_keyword_fn_rejected`, `ch05_reserved_resume_fn_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch08_ambiguous_import_adt_rejected`, `ch08_ambiguous_import_adt_swapped_rejected`, `ch08_ambiguous_import_rejected`, `ch08_ambiguous_import_swapped_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_reserved_vera_prefix_reference_rejected`, `ch08_reserved_vera_prefix_binder_rejected`, `ch08_reserved_vera_prefix_effect_rejected`, `ch08_reserved_vera_prefix_ability_rejected`, `ch08_reserved_vera_prefix_constructor_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch07_bare_effect_op_rejected`, `ch06_quantifier_array_domain_rejected`, `ch07_handler_state_type_mismatch_rejected`, `ch02_alias_cycle_rejected`, `ch08_module_prelude_adt_contention_rejected`) must *fail* with their `expected_error` E-code, at the stage `expected_error_stage` names — `check` by default, or `compile` for a diagnostic the checker accepts and codegen refuses (`ch08_module_prelude_adt_contention_rejected` → E621), which also asserts the program type-checks cleanly first - 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 9a3e83ce..e631af3d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -12,6 +12,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/). ### Fixed +- **Spec §1.4's reserved-keyword MUST is now enforced, for twenty-one names that nothing held** ([#1296](https://github.com/aallan/vera/issues/1296)). `§1.4` says its keywords must not be used as function names; `E153` held that for eleven of them, and `private fn with(@Int -> @Int)` — with `then`, `else`, `data`, `type`, `module`, `import`, `public`, `private`, `requires`, `ensures`, `invariant`, `decreases`, `effect`, `in`, `where` and `pure` — declared, type-checked, verified, compiled, ran and round-tripped `vera fmt`. They were not traps: a bare `with(1)` resolved to the declaration and returned its value, and stayed working inside a contract clause, inside an `if`/`then`/`else`, in a function carrying its own `where { }` block, and after a `let`. The comment above `_KEYWORD_FN_NAMES` gave the opposite as the reason they were absent from the set — that the contextual lexer "does not admit them as a function name, so no declaration reaches this checker at all" — so the omission rested on a premise the tree refuted, and the divergence was between the specification and the implementation rather than in any program's behaviour: a model trusting §1.4 and a model trusting the compiler derived different programs from one source of truth, with no tool contradicting either. DESIGN principle 1 (checkability) makes an unenforced MUST a defect whatever the program does at runtime, principle 6 (fewer valid programs) chooses enforcement over narrowing §1.4, and principle 3 supplies the precedent — `E152` rejects even a *faithful* re-declaration of a built-in effect, because a second textual spelling is itself the problem. The reserved set is now **derived from `vera/grammar.lark`** rather than hand-listed, the shape `builtin_effect_names()` already uses for `E152`, so a keyword added to the grammar is reserved the moment it is added; the hand-list this replaces had fallen twenty-one names behind the grammar with no gate able to see the drift. The derivation is what found the other four: `ability`, `effects`, `op` and `result` are grammar keywords §1.4 never listed and were accepted as function names on the same footing, and §1.4's list is reconciled to the grammar (gaining those four plus `old` and `new`, which `E153` already reserved). They join `E153` as a **fourth** branch with its own rationale: the existing keyword wording asserts that no call site can reach the declaration, which is false for every one of these names, so reusing it would have told authors a falsehood about their own program — the new branch argues from the reservation instead, and carries a per-name rename suggestion because the generic `_fn` template produces `in_fn` / `type_fn` / `pure_fn`. `handle` stays legal, carved out as the host-invoked `vera serve` / `wasi:http` entry point; the reservation remains on the whole identifier, so `older`, `with_it` and `then_value` are ordinary names. §1.4's "type names" half is corrected rather than enforced: every type-namespace binder in the grammar is an `UPPER_IDENT` and every keyword is lowercase, so that half was never violable. New conformance negative `ch05_reserved_contextual_keyword_fn_rejected` plus 110 tests in `tests/test_checker_modules.py` — five parametrized batteries over all 21 (declaration, visibility, `where`-helper, rationale-free-of-the-false-claim, and a usable fix suggestion) with `handle` and fifteen keyword-containing names as controls; mutation-validated by dropping one keyword from the derivation, which flips that name's five cells and both set pins red while the other twenty stay green. Corpus differential: zero movers, no program in `examples/` or `tests/conformance/` having used such a name. + - **Two imports supplying one bare name are refused, in every namespace** ([#1304](https://github.com/aallan/vera/issues/1304)). Spec §8.5 ordered a local declaration against an import (§8.5.2) and gave the module-qualified form for reaching what a clash hides (§8.5.3), but defined no order between two *imports* that both supply one name. Neither did the implementation, and the gap was reachable: a module importing two dependencies that each export `forall fn gen` — one returning `@Int`, one `@Bool` — bound its bare call to whichever supplier a set of module paths happened to yield first, so one unchanged file was `vera check`-green on one run and `[E121] body has type Bool` on the next. Measured at the branch point across eight consecutive runs and eight hash seeds: accepted on seeds 0, 2 and 3, rejected on 1, 4, 5, 6 and 7, with the winner tracking module-name hash order rather than which import is written first. Codegen's E608 rail caught the *entry-visible* pair before it could matter there; the flap lived in the shapes the rail only reached at compile, from inside a module the entry program merely imports. Spec §8.5.2.2 now states the rule — a program **MUST NOT** leave a namespace with two imports supplying one bare function name — and the checker enforces it as **E155**, a check-phase code for a scope question that had been enforced by a codegen rail at the wrong layer. Refusing is what removes the flap rather than merely labelling it: with no pick to make, there is no iteration order left to expose, which a deterministic first-wins order would not have achieved (it would make the resolved declaration implicit in import sequence, §0.2.2, and let a library *adding* an export silently rebind a downstream bare call). The refusal is **definition-gated**, matching the rail it generalises: it fires because the import pair exists, not because a body names it, so an entry program importing two suppliers and never calling either is refused exactly as E608 already refused it, and rewriting a bare call in module-qualified form does not lift it. Two shapes clear it, both exercised through to their runtime value: a **local declaration** of the name (§8.5.2 — every bare call is then the local one, and each import stays reachable through `dep::name(...)`), or a **selective import** narrowing the other module's list. The ambiguity predicate is the one `namespace_fn_names` already derived for #1281 and #1299, now exposed per namespace as well as unioned, so the layer that refuses early and the layer that backstops it cannot disagree about which shape is ambiguous; the E608 condition keeps its cell, driven through a door that bypasses the checker. An ambiguous name is not injected into the type environment at all — reporting the clash while binding one supplier would leave the follow-on diagnostics keyed to whichever module the injection loop reached first, which is the nondeterminism the refusal exists to remove — so a bare call to it misses with an ordinary `E200` instead — an E-coded diagnostic emitted at **warning** severity, which the `--json` envelope reports in `warnings` rather than `diagnostics` and which does not fail the check on its own (measured: a program whose only diagnostic is `E200` reports `ok: true` and exits 0). The W-series is the separate `W001`/`W002` code namespace, and this is not one of them. **The data namespaces flapped the same way and are folded in.** Spec §8.5.4 gives constructor names the same shadowing rules as function names, which a function-only refusal would have made false: two modules each exporting a `public data Shape` with different constructor field types type-checked on some hash seeds and reported `[E213]` on others (accepted on seeds 2, 8, 9, 10 and 11; rejected on 0, 1, 3, 4, 5, 6 and 7), and the accepting seeds were the worse half — `check` **and** `verify` both passed, and the program died at `run` with an `E609` located at line 0 of the entry file, naming two modules the entry never imported. Data types are now **E156** and constructors **E157**, one code per declaration namespace exactly as codegen splits E608/E609/E610, and reported independently because they come apart: two modules exporting differently-named types that share a constructor name clash on the constructor alone. Their remedy differs from the function one and says so — E609/E610 refuse two modules' same-named data declarations by DECLARATION, consulting neither visibility nor the importer's filter nor local shadowing (the relaxation E608 received in [#1281](https://github.com/aallan/vera/issues/1281) has no data-side twin), so narrowing an import or shadowing the name locally leaves the program `E609` at compile. Both were measured against the fixture and both fail — as does marking one declaration `private` — so the two diagnostics prescribe renaming, and a cell pins that measurement so the fix text cannot drift into offering remedies that do not work. That rail over-breadth is now tracked as [#1317](https://github.com/aallan/vera/issues/1317). **A name the built-in registry already owns is not a clash** — the injection loops are `setdefault` over a `TypeEnv` the built-ins populate first, so a dependency exporting its own `option_map` never wins the bare name (measured as `E201` against the *prelude's* two-argument signature). The first cut of this refusal did not pass the built-in snapshot and reported two such dependencies as a clash, which was a new rejection rather than an earlier one; `namespace_fn_names`' claim that its ambiguity half is identical with or without the prelude argument was wrong for the same reason and is corrected, with the codegen call ordering it depends on now pinned by a cell. - **A `throw` payload is runtime-guarded, not only obligated** ([#1268](https://github.com/aallan/vera/issues/1268)). `throw(v)` narrows `v` into the `Exn` payload, and since the static half of this issue the narrowing carries the same obligation every other binding site does — but codegen emitted no guard, so the obligation's Tier-3 leg promised a runtime check that did not exist and an unverified `vera compile`/`run` delivered the violating value anyway. `throw(0 - 5)` under `effects(>)` ran to completion and returned **-5** through the `@Nat` payload; the refined spelling (`type Pos = { @Int | @Int.0 > 0 }`) did the same. Worse than a wrong answer: a handler clause binds the payload at its declared type, so the verifier hands every downstream consumer the invariant the payload just broke — a `@Nat`-taking function discharging `ensures(@Bool.result)` at Tier 1 from its parameter's type alone reported a **postcondition violation at run time on a postcondition `vera verify` had proved**. `throw` now takes the write boundary's guards at its op-call site, beside `put`'s ([#1203](https://github.com/aallan/vera/issues/1203)): the `@Int` -> `@Nat` sign guard, the `@Nat` -> `@Int` widening guard, and — refined FIRST, as at every other narrowing site — the §2.6.5 predicate guard for a refined payload, which traps through `$vera.contract_fail` naming the predicate that failed (`Refinement violation in throw(@Pos) / payload: @Int.0 > 0 failed`). The three arms mirror the verifier's own obligation triple one-for-one, so the obligation stream and the emitted guards stay in lock-step: the payload obligation is now `guarded` at all three arms and its Tier-3 leg is counted in `tier3_runtime` rather than disclosed as `tier3_unguarded`, and the refined arm's `guarded` claim is intersected with the same `_refined_boundary_codegen_guardable` test every other refined site uses, so an erased `@Unit` base or a nested refinement — which codegen emits no guard for — stays honestly unguarded. That mirror needed one repair to be true: it answered "guarded" for a refinement OVER a refinement, which `_refinement_guard_parts` refuses outright with a loud `E618` because the outer predicate alone would silently drop the inner membership — so `vera verify` exited 0 recording a Tier-3 runtime check for a program `vera compile` then refuses, a promise about a run that can never happen. It now bails on a refinement base, and the obligation discloses `tier3_unguarded` while `E618` still refuses. The same audit found the **qualified spelling recording something different from the bare one**: the `QualifiedCall` arm hardcoded `guarded=False` behind a comment stale since [#1203](https://github.com/aallan/vera/issues/1203), so `Exn.throw(v)` — which codegen lowers by synthesizing a bare node and delegating to the very dispatcher that emits the guards — disclosed `E504`/`E506` for a boundary that traps, and `State.put(v)` had been doing the same since #1203. Both now take the bare arm's rule on the same key (`op.parent_effect`), so the two spellings of one operation record identical statuses. The review of that fix found the arm had been hand-written as a refined-then-`@Nat` chain with **no widening branch at all**, so `State.put(@Nat.0)` / `Exn.throw(@Nat.0)` into an `@Int` cell recorded no obligation whatever while codegen emitted the `@Nat` -> `@Int` widening guard on both spellings — a guard the obligation stream never mentioned, the mirror image of the claim-without-a-guard this issue started from. It now routes through the shared `_obligate_binding_triple`, so the three arms cannot drift apart again by omission. The triple itself then turned out to be missing the [#820](https://github.com/aallan/vera/issues/820) INTERSECTION at these boundaries: its three arms are an `elif` chain, so a refinement OVER `@Int` claimed the value and the widening check never ran — and codegen mirrored that exactly, so both sides agreed to skip a check the UNREFINED spelling performs. A refinement predicate does not imply fit-in-i64, and `{ @Int | true }` is satisfied by the negative a `@Nat` above i64.MAX reinterprets to, so adding a refinement WEAKENED the boundary: `Exn` fed u64.MAX trapped on the widening guard while `Exn<{ @Int | true }>` fed the same value returned **-1**. The widening obligation and its guard now ride beside the refined pair rather than being replaced by it, and the two spellings trap alike; a user-declared effect's operation and `IO.sleep`'s `@Nat` formal stay the honest [#754](https://github.com/aallan/vera/issues/754) unguarded class. Two diagnostic rationales (`E504`, `E531`) that listed the `throw` payload among the unguarded sites — false once the guard landed, and contradicting the spec sentences this change amends — no longer do. Reaching the predicate needed the payload's TYPE, which neither of a cell's two names carries: `family` renders the predicate and `base` strips it, so `CellNames` now carries the type expression its producer already held rather than parsing one back out of a mangled family name. The predicate lowering itself is injected into the translation context (`set_refinement_guard_emitter`), because the two halves of a §2.6.5 guard sit on opposite sides of that seam — which local at what width is the context's question, while the trap message, the contract-fail import and the E617/E618 diagnostics are the generator's. An unrefined payload's WAT is byte-identical to before: a differential over all 278 pre-existing corpus programs — every `examples/` and `tests/conformance/` program, compiled and verified on both trees — moves nothing, in emitted WAT or in the obligation and diagnostic streams. diff --git a/CLAUDE.md b/CLAUDE.md index 9deeda26..442b878d 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -59,10 +59,10 @@ VERA_EAGER_GC=1 vera run file.vera # Force GC on every alloc (see ENVIRONMENT.m VERA_DEBUG_HOST_ERRORS=1 vera run file.vera # Re-raise a host callback's own exception (see ENVIRONMENT.md, debug knob for host-binding bugs) mypy vera/ # Type-check the compiler itself -python scripts/check_conformance.py # Verify all 243 conformance programs (positives pass their level; negatives fail with their expected_error E-code) +python scripts/check_conformance.py # Verify all 244 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_examples_run.py # Run every runnable example trap-free under the native runtime; the rest carry a documented skip property, and an example that is neither is an error -python scripts/check_corpus_canonical.py # Verify all 292 corpus programs are in canonical form (vera fmt) +python scripts/check_corpus_canonical.py # Verify all 293 corpus programs are in canonical form (vera fmt) python scripts/check_examples_readme.py # Verify vera run commands in examples/README.md python scripts/check_spec_examples.py # Verify spec code blocks parse python scripts/check_readme_examples.py # Verify README code blocks parse @@ -94,7 +94,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/` — 243 conformance programs validating every language feature against the spec +- `tests/conformance/` — 244 conformance programs validating every language feature against the spec - `scripts/` — CI and validation scripts ## Writing Vera code @@ -131,7 +131,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 243 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_reserved_resume_fn_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch08_ambiguous_import_adt_rejected`, `ch08_ambiguous_import_adt_swapped_rejected`, `ch08_ambiguous_import_rejected`, `ch08_ambiguous_import_swapped_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_reserved_vera_prefix_reference_rejected`, `ch08_reserved_vera_prefix_binder_rejected`, `ch08_reserved_vera_prefix_effect_rejected`, `ch08_reserved_vera_prefix_ability_rejected`, `ch08_reserved_vera_prefix_constructor_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch07_bare_effect_op_rejected`, `ch06_quantifier_array_domain_rejected`, `ch07_handler_state_type_mismatch_rejected`, `ch02_alias_cycle_rejected`, `ch08_module_prelude_adt_contention_rejected`) must *fail* with their `expected_error` E-code, at the stage `expected_error_stage` names — `check` by default, or `compile` for a diagnostic the checker accepts and codegen refuses (`ch08_module_prelude_adt_contention_rejected` → E621), which also asserts the program type-checks cleanly first +- All 244 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_reserved_contextual_keyword_fn_rejected`, `ch05_reserved_resume_fn_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch08_ambiguous_import_adt_rejected`, `ch08_ambiguous_import_adt_swapped_rejected`, `ch08_ambiguous_import_rejected`, `ch08_ambiguous_import_swapped_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_reserved_vera_prefix_reference_rejected`, `ch08_reserved_vera_prefix_binder_rejected`, `ch08_reserved_vera_prefix_effect_rejected`, `ch08_reserved_vera_prefix_ability_rejected`, `ch08_reserved_vera_prefix_constructor_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch07_bare_effect_op_rejected`, `ch06_quantifier_array_domain_rejected`, `ch07_handler_state_type_mismatch_rejected`, `ch02_alias_cycle_rejected`, `ch08_module_prelude_adt_contention_rejected`) must *fail* with their `expected_error` E-code, at the stage `expected_error_stage` names — `check` by default, or `compile` for a diagnostic the checker accepts and codegen refuses (`ch08_module_prelude_adt_contention_rejected` → E621), which also asserts the program type-checks cleanly first - 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 4a7e13a0..716dcd6d 100644 --- a/FAQ.md +++ b/FAQ.md @@ -170,7 +170,7 @@ vera compile --target browser examples/hello_world.vera # index.html ``` -Serve it with any HTTP server and open `index.html` — no build step, no bundler, no dependencies. The JavaScript runtime provides browser-appropriate implementations of the host bindings the browser target supports — the ones a page can host, which leaves a filesystem, an accept loop, a database and a model provider outside it by construction (spec §12.9.3 lists each and why): `IO.print` writes to the page, `IO.read_line` uses `prompt()`, and State, contracts, JSON serialization and Markdown rendering work identically to the wasmtime runtime. `json_stringify` and `md_render` reach that identity by emitting a canonical form the specification states — §9.7.1 and §9.7.3 — rather than by the two hosts happening to agree, which is what the parity suite checks them against. `json_parse` reaches it from the other side, by accepted domain rather than by output form: §9.7.1 states what it takes — RFC 8259-valid text that decodes to finite numbers and strings of Unicode scalar values — so the JavaScript constants (`NaN`, `Infinity`, `-Infinity`) and a lone-surrogate escape are `Err` at the parse on both hosts, with one message, and every text inside the domain parses identically. `md_parse` is the one operation on the shared surface still to reach parity: the two hand-written parsers disagree across nine measured classes of input the §9.7.3 subset leaves open, the largest by a wide margin being how a paragraph's plain-text runs are grouped — invisible to `md_render`, since the runs concatenate to the same text — and the rest render-visible, from how emphasis markers are scanned to block markers such as a `+` bullet or a list nested more than two deep. That one is tracked as [#1301](https://github.com/aallan/vera/issues/1301). +Serve it with any HTTP server and open `index.html` — no build step, no bundler, no dependencies. The JavaScript runtime provides browser-appropriate implementations of the host bindings the browser target supports — the ones a page can host, which leaves a filesystem, an accept loop, a database and a model provider outside it by construction (spec §12.9.3 lists each and why): `IO.print` writes to the page, `IO.read_line` uses `prompt()`, and State, contracts, JSON serialization and Markdown rendering work identically to the wasmtime runtime. `json_stringify` and `md_render` reach that identity by emitting a canonical form the specification states — §9.7.1 and §9.7.3 — rather than by the two hosts happening to agree, which is what the parity suite checks them against. `json_parse` reaches it from the other side, by accepted domain rather than by output form: §9.7.1 states what it takes — RFC 8259-valid text that decodes to finite numbers and strings of Unicode scalar values — so the JavaScript constants (`NaN`, `Infinity`, `-Infinity`) and a lone-surrogate escape are `Err` at the parse on both hosts, with one message, and every text inside the domain parses identically. `md_parse` is the one operation on the shared surface still to reach parity: the two hand-written parsers disagree across nine measured classes of input the §9.7.3 subset leaves open, the largest by a wide margin being how a paragraph's plain-text runs are grouped — invisible to `md_render`, since the runs concatenate to the same text — and the rest render-visible, from how emphasis markers are scanned to block markers such as a `+` bullet or a list nested more than two deep. That one is tracked as [#1301](https://github.com/aallan/vera/issues/1301). `IO.read_char` is separately not yet supported in the browser target at all, and is a not-yet rather than one of the boundaries above — a page could host it, and until the JSPI suspend/resume primitive it needs lands the stub returns an explanatory `Err` reading `IO.read_char not yet supported in browser target`. Two effects are refused outright rather than merely differing. `Inference` and `DB` return an explanatory `Err` from every operation in the browser, because the API key or database credential they would need is readable from page source and network traffic in client-side JavaScript. Reach them through a server-side endpoint and call it with `Http`, which does run in the browser — it is backed by `XMLHttpRequest`, not a stub. That refusal is a deliberate platform boundary; spec §9.5.5 states it for `Inference`. @@ -236,7 +236,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 (243 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 (244 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*? @@ -279,7 +279,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 -- 11,670 tests, including a 243-program conformance suite +- 11,786 tests, including a 244-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/KNOWN_ISSUES.md b/KNOWN_ISSUES.md index 8f956cd3..7d66d41f 100644 --- a/KNOWN_ISSUES.md +++ b/KNOWN_ISSUES.md @@ -8,6 +8,7 @@ Defects in shipped compiler, runtime, or tooling behaviour — this table matche | Bug | Issue | |-----|-------| +| The nightly stress workflow never exercises `TestHostHandleReclamation573` — its 10 stress-marked instances are deselected from the per-PR suite (`-m 'not stress'` addopts) and `.github/workflows/nightly-stress.yml` runs `pytest -v -m stress tests/test_stress.py`, file-scoped, so no automated lane runs the #573/#575/#576/#706 GC-reclamation battery; the class comment's "Run via `pytest -m stress` or nightly CI" states the unmet intent. Run `pytest -m stress` manually until the workflow adds the file or the comment is re-scoped. | [#1328](https://github.com/aallan/vera/issues/1328) | | Monomorphization's Vera-level type namer has no `IndexExpr` arm, so a generic argument that is an array index drops its caller. `idg(@Array.0[1])` — a `forall` identity called on an element of a local `Array` — is `vera check`-green and then dies at `vera run` with `[E602] Function 'main' body contains unsupported FnCall: call target 'idg$Int' not registered in this module`, leaving `Available exports: (none)`: instantiation discovery (`Monomorphizer._infer_vera_type_name`) answers nothing for the index expression and falls to the phantom-var `Bool` default, while the WASM call-rewrite consultor (`InferenceMixin._infer_vera_type`), which DOES have an `IndexExpr` arm, names `idg$Int` at the call — the two consultors disagreeing, which is the clone-name agreement contract's (#772) failure mode. Loud, never a wrong answer. Measured during #1286's review sweep and unchanged by its fix, which closed the same consultor-parallelism gap for `Block`, `MatchExpr`, `IfExpr` and `HandleExpr` — each an exact one-line mirror of its twin — and deliberately left this one: the rewrite's arm delegates to `_infer_index_element_type`, which resolves chained indexing, type aliases and representation-transparent `Future` payloads against codegen tables the monomorphizer does not carry, so a partial mirror would answer differently from the rewrite for those cases, replacing a shape where both consultors say "unknown" with one where they disagree. Fix direction: lift the element-type derivation into one helper both consultors call, rather than a second partial copy that can drift from the first — the shape #1286 argues for throughout. | [#1327](https://github.com/aallan/vera/issues/1327) | | A match binding's GC shadow-stack push is never popped, so the shadow stack grows with recursion depth until it traps. Both `_translate_match`'s scrutinee rooting and `_setup_match_arm_env`'s binding rooting push onto `$gc_sp` and leave it advanced for the rest of the body; a function restores `$gc_sp` only on the way out, so a recursive function whose body matches pushes once per live frame and eventually crosses `$gc_stack_limit`, whose overflow check is a bare `unreachable`. Bisected on a `decreases`-guarded recursion carrying one match: an ADT (i32) scrutinee survives depth 2046 and traps at **2047**, **identically before and after [#1305](https://github.com/aallan/vera/issues/1305)**, which is what makes this pre-existing rather than new — the i32 rooting has behaved this way since #705/#707. What #1305 changed is reach: a `String` / `Array` scrutinee now takes this path too, and because the pair form roots twice per frame (scrutinee pointer and binder pointer) it survives only 1364 and traps at **1365** — two thirds of the ADT depth, which is what the slot arithmetic predicts: an ADT frame roots the parameter and the binder, a pair frame roots the parameter, the scrutinee pointer and the binder pointer, so three slots per frame against two and 2047 x 2/3 = 1364.7. Loud in every case — `unreachable`, never a wrong value — but the trap names no source construct and the depth at which it arrives is an artefact of how many pushes a body happens to make. Fix direction: pop what a match arm pushes at the arm's end (or scope the rooting to the arm body), so the depth a program can recurse to stops depending on how many matches its body contains. | [#1322](https://github.com/aallan/vera/issues/1322) | | Codegen's built-in-container branches are tested before `_adt_layouts`, so a user `data` declaration named after a container is classified by the container's representation instead of its own. `_type_expr_to_wasm_type` answers `Array` with `i32_pair` before it ever consults the registered ADT layouts, so `private data Array { MkArr(Int) }` — a perfectly ordinary declaration spec §8.4.1 permits — has its parameter classified as a two-word pair rather than the one-word heap pointer its constructor actually builds. `Map`, `Set`, `Decimal`, `Tuple` and `Future` are inert instances of the same ordering (their branch answers `i32`, which is what the ADT branch would have answered anyway) and compile and run correctly; `Array` is the one name whose two answers differ, and it fails on both sides of [#1309](https://github.com/aallan/vera/issues/1309) — as an unassemblable `i32_pair` local before it, and as an `[E602]` skip after. That E602 currently misattributes the cause, since the message it inherits from the [#1305](https://github.com/aallan/vera/issues/1305) pair guard describes the scrutinee's representation rather than the declaration that produced it; the wording no longer names `String` / `Array` as the source types, but a reader still has to know that a user `data Array` is why a pair representation was claimed at all. Sibling of #1309 (which reordered the alias branch ahead of these same container branches) and of [#1316](https://github.com/aallan/vera/issues/1316) (which is the environment those branches are consulted in) — one function, three orthogonal questions. Fix direction: consult `_adt_layouts` before the built-in container branches, matching `_resolve_named`, where a DECLARED ADT precedes the built-in absorption. | [#1321](https://github.com/aallan/vera/issues/1321) | @@ -20,7 +21,6 @@ Defects in shipped compiler, runtime, or tooling behaviour — this table matche | The checker resolves a bare call to a SIBLING function's `where` helper. Spec §5 makes a helper local to its parent, and the checker's own `_lookup_function_scoped` implements that — it walks the enclosing frame stack and reads each frame's direct helpers — but it then falls back to `env.lookup_function`, and `vera/registration.py` has recursed every helper into that flat `TypeEnv`. So a top-level `other()` calling `helperx(7)`, where `helperx` is a helper of an unrelated `holder`, is **check-green and verify-green** and then refused by codegen (`Function 'helperx' is not defined in this module and was not found in any imported module`) — the helper is emitted as `holder$where$helperx`, so the bare call has no target. Loud, never a wrong answer. The op-name variant is the one that matters for the #1284 ownership predicate: with the helper named `get` and the sibling reading a `State` cell by bare `get(())`, the checker binds the HELPER and reports `[E202] Argument 0 of 'get' has type Unit, expected Int` where spec §7.4 resolves the operation — so the checker rejects a program codegen compiles correctly, the two tables disagreeing in the CHECKER's direction for the first time. Codegen's `_scoped_fns` (#1299) implements the spec rule; the fix here is a checker change, whose new rejections need their own blast-radius pass. | [#1307](https://github.com/aallan/vera/issues/1307) | | `md_parse` diverges between the native and browser runtimes on **211 of 1,471** adversarial inputs (14.3%) and **329 of 4,858** blank-line-separated sections of the project's own documentation (6.8%), measured at [PR #1303](https://github.com/aallan/vera/pull/1303) by comparing the two ADTs directly rather than their renders. The second denominator is the repository's own Markdown, so it moves whenever a document gains or loses a section; 11 of those 4,858 also differ in the rendered output. Nine classes, each with a one-line repro. The largest by a wide margin — 173 of the 211 — is *plain-text run grouping*: the browser emits one `MdText` per scan segment where the reference coalesces adjacent runs, so `**unclosed` is `[MdEmph([]), MdText("unclosed")]` natively and `[MdText("*"), MdText("*unclosed")]` in the browser. That class is invisible to `md_render` (the runs concatenate to the same text) but not to a Vera program that matches on the ADT, which is what makes it a §12.9.3 violation rather than a cosmetic one. The rest are render-visible: emphasis/strong scanning (`***both***` renders `**both****` natively, `***both***` in the browser); list-continuation indent width, where the reference strips exactly two (or three) characters and the browser strips all leading whitespace (`- a\n b` → `- a b` vs `- a b`); a `+` bullet, unrecognised in the browser; an `n)` ordered marker, likewise; a loose list, one list natively and two in the browser (`- a\n\n- b`); nesting past two levels, flattened in the browser (`- a\n - b\n - c`); a thematic break with internal spaces (`* * *`); and a table without a separator row (`\| a \| b \|\n- li`). Neither implementation is the specification — §9.7.3 pins the ADT, not the grammar that produces it — so closing this means choosing a parse for each class and stating it, then mirroring. Successor to [#1294](https://github.com/aallan/vera/issues/1294), which closed the `md_render` half; the parity suite pins the shapes they do agree on, so a regression on one of those goes red. | [#1301](https://github.com/aallan/vera/issues/1301) | | A postcondition may name a `State` the function's effect row never declares, and `vera check` accepts it: `ensures(new(State) == false)` under `effects(>)` reports OK, then `vera compile` fails with **E699** — the internal-compiler-error diagnostic whose own text says the type checker should have rejected the input, which is exactly the situation. Both forms land there for the same reason (no cell of that family exists, so `old()` finds no snapshot local and, since [#1285](https://github.com/aallan/vera/issues/1285), `new()` finds no getter). Loud and never a wrong answer, so this is diagnostic quality rather than soundness — but it is a check-green program that cannot compile, reported against the compiler instead of against the program, with a bug-report request the user should not act on. Before #1285 the `new()` side was worse than loud: the name-keyed lookup found the row's other getter and silently read the wrong cell. Fix direction: validate an `OldExpr`/`NewExpr`'s effect reference against the declared row where the checker already validates the rest of the clause, one rule for both forms; `test_a_family_the_row_does_not_declare_is_loud_on_both_sides` pins today's E699 and is the test to flip. | [#1298](https://github.com/aallan/vera/issues/1298) | -| Spec §1.4 says its reserved keywords MUST NOT be used as function names, and for **seventeen of them nothing enforces it**: `then`, `else`, `data`, `type`, `module`, `import`, `public`, `private`, `requires`, `ensures`, `invariant`, `decreases`, `effect`, `with`, `in`, `where` and `pure` all declare and pass `vera check` as `public fn (@Int -> @Int)`. (`handle` is an eighteenth acceptance and is the sanctioned host-entry-point carve-out, §5.2; the other eleven names — `resume`, `exists`, `forall`, `match`, `assert`, `assume`, `fn`, `let`, `if`, `true`, `false` — are refused **E153**.) They are not even traps: `private fn with(@Int -> @Int)` and its `where` / `type` / `pure` / `requires` / `import` siblings are **callable** from the same file, so the declaration resolves and runs like any other function. The comment above `_KEYWORD_FN_NAMES` in `vera/checker/registration.py` gives the opposite as the reason those names are absent from the set — that the contextual lexer "does not admit them as a function name, so no declaration reaches this checker at all" — so the omission rests on a premise the tree refutes, and neither the parser nor the checker holds the MUST. Two resolutions, and the choice is a ruling rather than a mechanical fix: extend `_KEYWORD_FN_NAMES` so the seventeen join `resume` under E153, or narrow §1.4's MUST to the names actually reserved. The `resume` precedent leans to enforcing — `resume` is likewise not a keyword token anywhere and likewise parses, and was reserved *at the checker* precisely because the parser had no keyword to refuse it with — and E153's own rationale, that a keyword names one construct and nothing else (DESIGN principle 3), does not depend on the name being a trap. Until the ruling lands, §1.4's `handle` carve-out sentence deliberately makes no enforcement claim, so the spec does not assert a MUST it cannot back. | [#1296](https://github.com/aallan/vera/issues/1296) | | Spec Chapter 10 is a second, hand-maintained copy of `vera/grammar.lark`, and the rule-name alignment gate `scripts/check_grammar_alignment.py` compares only rule-name headers — three classes of drift pass it unseen. **Terminals, both directions**: the header pattern requires a lowercase lead, so a fabricated terminal added to §10.2 leaves the gate green, and no declared-versus-referenced audit exists in either direction. **Rule references**: restoring a removed ambiguity to a production's right-hand side is invisible, because only headers are compared. **Production bodies**: the class most grammar edits actually fall into. Two instances are live in the chapter on `main` today, both body-level and both this issue's to close: typed holes (`"?" -> hole_expr`, in `grammar.lark` since 2026-03-30) appear nowhere in `primary_expr`, and §10.2's `BLOCK_COMMENT: /\{-[\s\S]*?-\}/` is non-nesting, contradicting both §1.3 ("They nest") and the implementation, which parses `{- a {- b -} c -}` clean. Never a wrong answer from a program — the defect is that the published grammar misdescribes the one the parser has. Fix direction: extend the gate side-aware (terminal audit both ways, reference-set comparison), or fold Chapter 10 toward the DESIGN Grammar row's actual promise of a single-sourced shared grammar rather than a hand-maintained copy held honest by ever-wider cross-checks; the two live instances are fixable independently of which direction wins. | [#1290](https://github.com/aallan/vera/issues/1290) | | `.github/workflows/release.yml`'s `Tag and create GitHub Release` step fails with `HTTP 422: Validation Failed — body is too long (maximum is 125000 characters)` when the CHANGELOG section `scripts/release.py notes` extracts into `RELEASE_NOTES.md` exceeds GitHub's release-body limit. It fired on v0.1.10, whose notes extract to roughly 148,700 bytes — the #1213 burndown's 44-issue section, some 23,000 characters past the limit — and it fired at the worst point in the pipeline: **after** PyPI had accepted the immutable archives and **after** the tag was created, leaving the release half-cut with no repeatable path back. The v0.1.10 GitHub Release was completed by hand, mirroring the step exactly: the run's artifacts downloaded and hash-verified three ways, then `gh release create --verify-tag --latest` with the wheel, sdist and SHA256SUMS, and a generated body — the section's bold bullet lead-ins as a headline index plus a link to the canonical section at the tag. Rare, since it needs a release this large, but rarity is not the mitigating factor here; the landing point is. Fix direction: make the step total — before `gh release create`, regenerate oversized notes into that index form so the release always carries a body that fits, with the full notes staying in `CHANGELOG.md`, which is already the release notes of record. | [#1288](https://github.com/aallan/vera/issues/1288) | | `ch05_closure_nat_return` (a run-level conformance program in the pre-commit + CI gate) trapped **once** in a full `check_conformance.py` run (`unreachable` in `main` — the sentinel `assert` or a GC shadow-stack guard) and has not reproduced in ~960 attempts across isolated, parallel, eager-GC, and hash-seed-swept executions; the emitted WAT is deterministic and correct. Suspected rare runtime/GC/wasmtime interaction, tracked so a future intermittent CI red resolves here instead of starting fresh. | [#996](https://github.com/aallan/vera/issues/996) | diff --git a/README.md b/README.md index 0387a8e3..b5f7593e 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.11: 2,000+ commits, 209 releases, 11,670 tests, 95% Python code coverage, 243 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.11: 2,000+ commits, 209 releases, 11,786 tests, 95% Python code coverage, 244 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 990ed872..1f54b11c 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 -11,670 tests, 243 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. +11,786 tests, 244 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 765fb998..cb82d81e 100644 --- a/SKILL.md +++ b/SKILL.md @@ -2461,7 +2461,7 @@ public fn main(@Unit -> @Unit) ## Conformance Suite -The `tests/conformance/` directory contains 243 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 244 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 159445de..ea569f8d 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** | 11,670 across 174 files (~155,000 lines of test code; 11,473 passed + 26 stress, 171 skipped) | +| **Tests** | 11,786 across 174 files (~155,000 lines of test code; 11,587 passed + 26 stress, 173 skipped) | | **Compiler code coverage** | 95% Python, 87% JavaScript (CI minimum: 80%) | -| **Conformance programs** | 243 programs across 9 spec chapters, validating every language feature | +| **Conformance programs** | 244 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) | @@ -43,7 +43,7 @@ pytest tests/test_runtime_traps.py::TestHostErrorDebugKnob1302 -v mypy vera/ # strict mode # Validation scripts -python scripts/check_conformance.py # conformance suite (243 programs, see manifest.json) +python scripts/check_conformance.py # conformance suite (244 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 @@ -101,7 +101,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 | 780 | #309 — the SQL literal-provenance gate (SQL injection as a compile-time error): non-literal SQL rejected `E207` (bare param slot, function result, `\(expr)` interpolation, `string_concat` with a runtime operand, let-bound runtime value, `if`-expression), literal / concat-of-literals / let-chain-with-shadowing / empty-string accepted, placeholder/param arity `E208` with quote- and comment-aware counting (named/numbered placeholders are rejected outright, `E209`), the `count_placeholders`↔sqlite3 differential (exact count accepted, one too many rejected), and gate scoping — a user `effect DB` shadow is rejected at its declaration (`E152`, #1149) *and* its runtime SQL still draws `E207` alongside it (defence in depth), an unrelated effect's `query` is not gated, and no `E207` cascade onto a mistyped SQL arg | -| `test_checker_modules.py` | 132 | 2,298 | 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; and `resume`, reserved on separate grounds — not a keyword, so the declaration parses and outside a handler a bare call reaches it, but it collides with the resumption binding every clause body carries, and the pins cover the rejection, the where-helper depth, that the rationale carries none of the other two branches' false claims, that handler-clause `resume(...)` still checks AND that a wrongly-typed one is still E202 — the pair, since a binding that accepted anything would satisfy the first alone — and that the rejected declaration draws no second error out of the correct clause bodies it used to shadow, at both top level and where-helper depth), parsed module calls (#420 split) | +| `test_checker_modules.py` | 242 | 2,606 | Module-call diagnostics, cross-module typing, visibility enforcement, builtin redefinition (function E151 and effect E152 surfaced from a module into its importer), reserved function names (E153 — the contract state forms `old` / `new` and the keyword class `assert`/`assume`/`forall`/`exists`/`match`/`if`/`let`/`fn`/`true`/`false`, each top-level, `where`-helper, and module-surfaced, plus the `handle` host-invoked carve-out and the probe record behind both halves; the twenty-one *contextual* keywords `then`/`else`/`data`/`type`/`module`/`import`/`public`/`private`/`requires`/`ensures`/`invariant`/`decreases`/`effect`/`with`/`in`/`where`/`pure`/`ability`/`effects`/`op`/`result`, derived from `grammar.lark` rather than hand-listed and reachable rather than traps — each declared, was called and answered its value before the fix — over five parametrized batteries (declaration, visibility, `where`-helper, a rationale free of the keyword branch's false unreachability claim, and a usable per-name fix suggestion) with `handle` and fifteen keyword-containing names as controls; and `resume`, reserved on separate grounds — not a keyword, so the declaration parses and outside a handler a bare call reaches it, but it collides with the resumption binding every clause body carries, and the pins cover the rejection, the where-helper depth, that the rationale carries none of the other two branches' false claims, that handler-clause `resume(...)` still checks AND that a wrongly-typed one is still E202 — the pair, since a binding that accepted anything would satisfy the first alone — and that the rejected declaration draws no second error out of the correct clause bodies it used to shadow, at both top level and where-helper depth), parsed module calls (#420 split) | | `test_checker_errors.py` | 73 | 1,196 | Error codes, resolution-coverage diagnostics, contracts, error accumulation (#420 split); cyclic type aliases incl. #1059 self-reference through a type argument (`Future`, 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) | @@ -192,7 +192,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` | 538 | 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` | 539 | 3,638 | Comment extraction, interior comment positioning, expression/declaration formatting, match arm block bodies, §1.8 rule 2 in value position (a `let`-bound `match`/`if` expands exactly as one in statement position, and a comment above an arm inside a statement's value stays on that arm), blank-line preservation (§1.8 rule 13 — gaps between statements, before a block result and around a comment, collapsed to one and never invented), idempotency, parenthesization, spec rules, ability declarations | | `test_cli.py` | 273 | 4,612 | CLI commands (check, verify, compile, run, serve, test, fmt, version, quiet), subprocess integration, JSON error paths (including the `verify --json` `obligations` array and its summary-reproducibility pin, #967, and the #1242 partition pin — the array is emitted unfiltered, a refuted obligation is counted by no summary field, and it still joins its E500 on the location key), runtime traps, arg validation, multi-file resolution, IO exit codes, --explain-slots (including the #1208 naming pins — an alias in type-argument position is tabled resolved, and a `forall` variable shadowing a module alias keeps the two parameter stacks apart — and the #1217 `where`-helper tables: the helper prints indented under its parent, appears in the JSON qualified as `parent.helper`, and inherits the enclosing `forall` variables so the shadowing holds inside it too), `builtins`/`effects`/`errors` introspection dispatch, and a USAGE-completeness guard (every dispatched `cmd_` 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) | @@ -210,7 +210,7 @@ python scripts/check_wheel_availability.py # pre-flight: every runtime | `test_markdown.py` | 94 | 610 | Markdown parser: block/inline parsing, rendering, round-trips, edge cases | | `test_lsp.py` | 146 | 2470 | LSP transport + coordinate layer (#222 Phase C) and language features (#222 Phase D): parametrized code-point↔UTF-16 goldens incl. astral-plane fixtures and surrogate-pair snapping, Span (1-based, exclusive-end) and SourceLocation (0-based col) → LSP Range conversions, point→token-range widening, DocumentStore open/change/close + index invalidation, an in-process handler-drive test, and one stdio end-to-end round-trip against the real `vera lsp` subprocess (initialize → didOpen → shutdown → exit) pinning serverInfo + textDocumentSync capabilities; plus the Phase D feature suite — parse-error single-diagnostic path, type-error verification short-circuit, tier=3 in E520 diagnostic data, per-function tier Hint synthesis (and its suppression for functions with violated obligations), smallest-enclosing-span hover, De Bruijn slot goto (most-recent-parameter jump, out-of-range None, off-slot None, and the #1208 keying pins: a parameterised reference resolves, an alias-spelled parameter is reachable from a canonically-spelled reference, and a `forall` variable shadowing a module alias lands on the right parameter), and typed-hole completion (inside/after hole, away-from-hole None); plus the Phase E speculativeEdit suite — identical-text all-unchanged, breaking edit surfaces newly_undischarged (violated nat_sub) with canonical state untouched, strengthening edit surfaces newly_discharged, parse/type errors report ok:false, deleted functions report removed, proof_delta purity; plus the Phase F1 proposeEdit suite — the apply gate (clean and strengthening edits apply, breaking and non-compiling edits refuse), force overriding both gates with the delta still reported, wiring against a structural fake server (apply round-trip with exact full-document replacement range, refuse touches no canonical state, unopened-URI clamp sentinel), and full-document-range goldens (trailing-newline virtual line, UTF-16 end column); plus the Phase F2 strengthenContract suite — splice goldens (first-clause-only replacement with byte-identical remainder, ensures variant, unknown-fn None), the call-site audit pin (tightened precondition refused with newly_undischarged call_pre items, canonical state untouched), provable-ensures strengthening applies, and the three splice-target refusal paths (no analysis, unparseable document, unknown function); plus the Phase F3 addEffect suite — transitive-caller closure goldens (diamond in declaration order, leaf, unknown-fn None, recursion appears once), handler bounding (#725: a caller discharging the effect around its only call site drops out of the closure and is not rewritten, while a second unhandled path, a call in a handler clause, a handler for another effect, a handler naming a different instance of the same effect (`handle[State]` against a `State` propagation, which the checker does not discharge — end-to-end that caller must still be rewritten and the candidate must still apply, with the matching `State` propagation against the same fixture as the positive control that this handler key does prune something), and a bare `where`-helper call all keep it in, as does a refinement type argument at either depth (`Exn<{ @Int \| p }>` and `Exn>` render as their bare base type but discharge nothing of `Exn` — also pinned end-to-end), while an unparameterised `handle[IO]` does bound an `IO` propagation, a whitespace-spelled `State< Int >` request still bounds, and nesting bounds in either order (a matching handler inside a foreign one, a foreign one inside a matching one) — plus a key-level pin that `handle[Mod.IO]` keeps its module, and the effect-less query pinned handler-unaware; plus the two boundary pins the review added — a call in the handler's STATE INITIALISER keeps its edge, since the initialiser is evaluated in the enclosing scope before the handler is installed (pinned beside the E125 the checker raises there against a `pure` caller, with the identical call in the handler body clean as the contrast), and an alias-spelled handler does not bound a `State` propagation though the checker discharges it (`handle[State]` with `type MyAlias = Int` — the spelling comparison's under-prune, #1292, with the alias-spelled request as the control that does prune)), effect-row rewrite goldens (pure to singleton set, source-preserving append, already-present None, base-name identity blocking State 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` | 413 | 5,094 | Browser parity: Python/wasmtime vs Node.js/JS-runtime output equivalence across IO, State, contracts, Markdown, Regex, and the examples the browser target can execute (two explicit lists in the file, not the whole `examples/` directory — interactive stdin, file IO, `DB` and the non-standalone `modules` example are excluded with their reasons recorded); plus the #349 `runtime.mjs` coverage battery — per-value-type and per-key-type Map variants, per-element-type Set variants, cold `Decimal` branches (exact-zero sign, negative-shift division, `decRoundPlaces` special cases, non-finite storage), `readJson`/`json_stringify` across every Json ADT tag, the Regex/Json `Result.Err` arms, and nested-Markdown walks. Two operations carry a canonical form the specification states rather than merely agreeing across the hosts, so their batteries assert more than equality: `json_stringify` (spec §9.7.1) pins the expected string on every Json ADT tag and on the number-rendering boundaries, checks three-pass idempotence, checks that a non-finite `JNumber` fails on both hosts *and* prints nothing, pins the object key orders an ordinary JS object cannot carry (array-index keys, which ES enumeration hoists to the front in ascending numeric order, and a `__proto__` key, whose assignment writes a prototype instead of a field) on both a parsed and a program-built object, and checks the reference host's own number rendering differentially against a real `JSON.stringify` over doubles drawn from raw bit patterns; `md_render` (§9.7.3) pins the expected render, re-renders it to prove the fixed point, runs the round-trip property over a corpus carrying the container and multi-line shapes a flat corpus misses, and renders `MdBlock` values the test builds directly, since several renderer rules — a container's child separator, an empty container, a code span wider than one backtick — are unreachable through `md_parse`. plus the #1306/#1308 accept-domain battery (`TestBrowserJsonAcceptDomainParity1306_1308`), which runs one `.wasm` under both runtimes and compares the WHOLE stdout — arm taken and `Err` message together — over the JavaScript constants, over numbers that overflow to an infinity in both their exponent and integer spellings, and over lone surrogates at every position a string can occupy, with the expected sentences imported from `vera/wasm/json_serde.py` so `runtime.mjs`'s hand-copied duplicates are held against the originals, beside acceptance controls (matched pairs, finite boundary values, underflow to `0`, `"NaN"` as a string value), a ten-case host-native-message battery pinning that neither the substitute-and-re-parse probe nor the value-start constraint hijacks an unrelated syntax error (`-NaN` is the case needing both rules — the substitution alone turns it into `-0` and manufactures a refusal the reference host never makes), a precedence case fixing that a non-finite constant outranks a lone surrogate on both hosts though each reaches that answer by a different route, and a document-order case fixing that overflow and lone surrogate are resolved by one walk rather than by two per-host precedence rules that would agree on every single-violation document; `md_parse` itself is not yet at parity and its remaining divergence classes are a tracked bug ([#1301](https://github.com/aallan/vera/issues/1301)); the suite pins the shapes the two implementations agree on | -| `test_conformance.py` | 1215 | 144 | Parametrized conformance suite: parse, check, verify, run, format idempotency across 243 programs; a negative entry fails at the stage `expected_error_stage` names (`check`, the default, or `compile` — which also asserts the program type-checks cleanly first) | +| `test_conformance.py` | 1220 | 144 | Parametrized conformance suite: parse, check, verify, run, format idempotency across 244 programs; a negative entry fails at the stage `expected_error_stage` names (`check`, the default, or `compile` — which also asserts the program type-checks cleanly first) | | `test_prelude.py` | 29 | 585 | Prelude injection: Option/Result/array operation detection, combinator shadowing, type aliases, the reserved namespace every injected alias declaration lives in — checked against the checker's own E154 regex rather than a second spelling of the rule, since an alias the prelude injects outside it is one codegen resolves and the checker leaves opaque (#1184/#1221) — end-to-end compilation | | `test_checker_apply_fn.py` | 18 | 455 | #854 — `apply_fn` as a checker special form: zero-warning pins (API + CLI `--json` + closures.vera), E201 arity / E202 type / non-function-first-arg errors, E122/E125 effect-row enforcement for applied fn values, E151 redefinition rejection, variadic two-param application, prelude combinator regression pins | | `test_prelude_diagnostics.py` | 8 | 271 | #851 — prelude combinator skip-warnings: unreferenced-prelude E602/E604 suppression (zero-warning minimal compile, API + CLI `--json`), `` origin attribution for referenced-but-skipped combinators (text + `to_dict`), transitive reference scan, and user-fn warning locations pinned unchanged | @@ -236,7 +236,7 @@ python scripts/check_wheel_availability.py # pre-flight: every runtime ## Conformance Suite -The conformance suite is a collection of 243 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 244 small, focused programs in `tests/conformance/` that systematically validate every language feature against the spec. Most programs are self-contained; the module-focused Chapter 8 cases use `import` statements where needed, and `ch07_cross_module_contracts.vera` still depends on `ch07_cross_module_contracts_lib.vera`. Each program tests one feature or a small group of related features. Simon Willison [argues](https://simonwillison.net/tags/conformance-suites/) that conformance suites are a "huge unlock" for language projects — they transform development from trust-based to verification-based. The conformance suite serves as the definitive specification artifact that any implementation (or agent) can validate against. @@ -261,15 +261,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 | 49 | +| `check` | Parses and type-checks cleanly | 50 | | `verify` | Type-checks and all contracts verified by Z3 | 20 | | `run` | Compiles to WASM and executes correctly | 174 | -Almost all programs are at the `run` level — they compile and execute, producing correct results. Forty-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_reserved_keyword_fn_rejected`, `ch05_reserved_resume_fn_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_cross_module_contracts_lib`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch07_bare_effect_op_rejected`, `ch08_ambiguous_import_adt_lib_bool`, `ch08_ambiguous_import_adt_lib_int`, `ch08_ambiguous_import_adt_rejected`, `ch08_ambiguous_import_adt_swapped_rejected`, `ch08_ambiguous_import_lib_bool`, `ch08_ambiguous_import_lib_int`, `ch08_ambiguous_import_rejected`, `ch08_ambiguous_import_swapped_rejected`, `ch08_circular_import`, `ch08_cross_module_generic_lib`, `ch08_module_generic_diamond_base`, `ch08_module_prelude_adt_contention_rejected`, `ch08_reserved_vera_prefix_rejected`, `ch08_reserved_vera_prefix_reference_rejected`, `ch08_reserved_vera_prefix_binder_rejected`, `ch08_reserved_vera_prefix_effect_rejected`, `ch08_reserved_vera_prefix_ability_rejected`, `ch08_reserved_vera_prefix_constructor_rejected`, `ch08_transitive_module_import_base`, `ch08_visibility_private`, `ch08_xmod_widen_lib`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_eq_non_derivable_rejected`, `ch09_http`, `ch09_inference`, `ch09_ord_adt_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch06_quantifier_array_domain_rejected`, `ch07_handler_state_type_mismatch_rejected`, `ch02_alias_cycle_rejected`) are at the `check` level. Thirty-six of them — `ch02_generic_over_unit_rejected`, `ch02_map_unit_value_rejected`, `ch04_let_unit_rejected`, `ch05_apply_fn_arity`, `ch05_decreases_float_rejected`, `ch05_reserved_fn_name_rejected`, `ch05_reserved_keyword_fn_rejected`, `ch05_reserved_resume_fn_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch07_bare_effect_op_rejected`, `ch08_ambiguous_import_adt_rejected`, `ch08_ambiguous_import_adt_swapped_rejected`, `ch08_ambiguous_import_rejected`, `ch08_ambiguous_import_swapped_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_reserved_vera_prefix_reference_rejected`, `ch08_reserved_vera_prefix_binder_rejected`, `ch08_reserved_vera_prefix_effect_rejected`, `ch08_reserved_vera_prefix_ability_rejected`, `ch08_reserved_vera_prefix_constructor_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch06_quantifier_array_domain_rejected`, `ch07_handler_state_type_mismatch_rejected`, and `ch02_alias_cycle_rejected` — are **negative tests** that assert a specific diagnostic (E206, E135, E183, E201, E127, E153, E153, E153, E130, E130, E174, E182, E217, E156, E156, E155, E155, E011, E154, E154, E154, E154, E154, E154, E150, E152, E151, E242, E243, E207, E208, E208, E209, E128, E336, and E132 respectively) via the manifest's `expected_error` field. One more — `ch08_module_prelude_adt_contention_rejected` — is a negative at the `compile` stage rather than at `check`: it carries `expected_error_stage: "compile"` beside `expected_error: E621`, so the harness asserts it type-checks CLEANLY and is then refused by `vera compile` with that code, which is the property a codegen-phase diagnostic exists for. `ch09_http` and `ch09_inference` are environment-gated (network / API key). Twenty programs (`ch03_slot_let_chains`, `ch03_slot_noncommutative`, `ch04_nested_option_ctor`, `ch04_primitive_obligations`, `ch05_apply_fn_typing`, `ch06_adt_sort_disambiguation`, `ch07_cross_module_contracts`, `ch07_invisible_import_op_name_lib`, `ch07_io_read_char`, `ch07_io_sleep`, `ch07_random_effect`, `ch08_state_alias_module_table_lib`, `ch08_module_generic_diamond_mid1`, `ch08_module_generic_diamond_mid2`, `ch08_state_alias_per_module_lib`, `ch08_transitive_module_import_mid`, `ch09_http_server`, `ch09_invisible_import_ability_op_lib`, `ch09_math_builtins`, `ch09_nested_helper_family_op_name_lib`) are at the `verify` level, using Z3-provable contracts — a library module is pinned at the deepest level it reaches, so the two per-module alias-table libraries are verified rather than only checked. +Almost all programs are at the `run` level — they compile and execute, producing correct results. Fifty programs (`ch02_generic_over_unit_rejected`, `ch02_map_unit_value_rejected`, `ch03_typed_holes`, `ch04_let_unit_rejected`, `ch05_apply_fn_arity`, `ch05_decreases_float_rejected`, `ch05_reserved_fn_name_rejected`, `ch05_reserved_keyword_fn_rejected`, `ch05_reserved_contextual_keyword_fn_rejected`, `ch05_reserved_resume_fn_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_cross_module_contracts_lib`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch07_bare_effect_op_rejected`, `ch08_ambiguous_import_adt_lib_bool`, `ch08_ambiguous_import_adt_lib_int`, `ch08_ambiguous_import_adt_rejected`, `ch08_ambiguous_import_adt_swapped_rejected`, `ch08_ambiguous_import_lib_bool`, `ch08_ambiguous_import_lib_int`, `ch08_ambiguous_import_rejected`, `ch08_ambiguous_import_swapped_rejected`, `ch08_circular_import`, `ch08_cross_module_generic_lib`, `ch08_module_generic_diamond_base`, `ch08_module_prelude_adt_contention_rejected`, `ch08_reserved_vera_prefix_rejected`, `ch08_reserved_vera_prefix_reference_rejected`, `ch08_reserved_vera_prefix_binder_rejected`, `ch08_reserved_vera_prefix_effect_rejected`, `ch08_reserved_vera_prefix_ability_rejected`, `ch08_reserved_vera_prefix_constructor_rejected`, `ch08_transitive_module_import_base`, `ch08_visibility_private`, `ch08_xmod_widen_lib`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_eq_non_derivable_rejected`, `ch09_http`, `ch09_inference`, `ch09_ord_adt_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch06_quantifier_array_domain_rejected`, `ch07_handler_state_type_mismatch_rejected`, `ch02_alias_cycle_rejected`) are at the `check` level. Thirty-seven of them — `ch02_generic_over_unit_rejected`, `ch02_map_unit_value_rejected`, `ch04_let_unit_rejected`, `ch05_apply_fn_arity`, `ch05_decreases_float_rejected`, `ch05_reserved_fn_name_rejected`, `ch05_reserved_keyword_fn_rejected`, `ch05_reserved_contextual_keyword_fn_rejected`, `ch05_reserved_resume_fn_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch07_bare_effect_op_rejected`, `ch08_ambiguous_import_adt_rejected`, `ch08_ambiguous_import_adt_swapped_rejected`, `ch08_ambiguous_import_rejected`, `ch08_ambiguous_import_swapped_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_reserved_vera_prefix_reference_rejected`, `ch08_reserved_vera_prefix_binder_rejected`, `ch08_reserved_vera_prefix_effect_rejected`, `ch08_reserved_vera_prefix_ability_rejected`, `ch08_reserved_vera_prefix_constructor_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch06_quantifier_array_domain_rejected`, `ch07_handler_state_type_mismatch_rejected`, and `ch02_alias_cycle_rejected` — are **negative tests** that assert a specific diagnostic (E206, E135, E183, E201, E127, E153, E153, E153, E153, E130, E130, E174, E182, E217, E156, E156, E155, E155, E011, E154, E154, E154, E154, E154, E154, E150, E152, E151, E242, E243, E207, E208, E208, E209, E128, E336, and E132 respectively) via the manifest's `expected_error` field. One more — `ch08_module_prelude_adt_contention_rejected` — is a negative at the `compile` stage rather than at `check`: it carries `expected_error_stage: "compile"` beside `expected_error: E621`, so the harness asserts it type-checks CLEANLY and is then refused by `vera compile` with that code, which is the property a codegen-phase diagnostic exists for. `ch09_http` and `ch09_inference` are environment-gated (network / API key). Twenty programs (`ch03_slot_let_chains`, `ch03_slot_noncommutative`, `ch04_nested_option_ctor`, `ch04_primitive_obligations`, `ch05_apply_fn_typing`, `ch06_adt_sort_disambiguation`, `ch07_cross_module_contracts`, `ch07_invisible_import_op_name_lib`, `ch07_io_read_char`, `ch07_io_sleep`, `ch07_random_effect`, `ch08_state_alias_module_table_lib`, `ch08_module_generic_diamond_mid1`, `ch08_module_generic_diamond_mid2`, `ch08_state_alias_per_module_lib`, `ch08_transitive_module_import_mid`, `ch09_http_server`, `ch09_invisible_import_ability_op_lib`, `ch09_math_builtins`, `ch09_nested_helper_family_op_name_lib`) are at the `verify` level, using Z3-provable contracts — a library module is pinned at the deepest level it reaches, so the two per-module alias-table libraries are verified rather than only checked. ### Skipped tests -`pytest tests/ -v` skips 118 conformance-stage tests, and every one of them is the level rule: a program declared at `check` skips its `verify` and `run` stages, one declared at `verify` skips its `run` — 49 × 2 + 20, which is what the suite reports. The two tables below split those 118 by why the program sits at its level, not by how it skipped: 114 are pinned there by the feature under test, and 4 by an environment CI does not have. Each skip is listed once; the tables do not overlap. (The suite's remaining skips are platform- or tool-gated and documented beside the tests that declare them.) +`pytest tests/ -v` skips 120 conformance-stage tests, and every one of them is the level rule: a program declared at `check` skips its `verify` and `run` stages, one declared at `verify` skips its `run` — 50 × 2 + 20, which is what the suite reports. The two tables below split those 120 by why the program sits at its level, not by how it skipped: 116 are pinned there by the feature under test, and 4 by an environment CI does not have. Each skip is listed once; the tables do not overlap. (The suite's remaining skips are platform- or tool-gated and documented beside the tests that declare them.) **Level-limited skips** — the conformance framework only runs tests up to the declared level; stages beyond that level are automatically skipped. These are expected and correct. @@ -303,6 +303,8 @@ Almost all programs are at the `run` level — they compile and execute, produci | `test_run[ch05_reserved_fn_name_rejected]` | `ch05_reserved_fn_name_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage | | `test_verify[ch05_reserved_keyword_fn_rejected]` | `ch05_reserved_keyword_fn_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E153`): verify stage not run | | `test_run[ch05_reserved_keyword_fn_rejected]` | `ch05_reserved_keyword_fn_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage | +| `test_verify[ch05_reserved_contextual_keyword_fn_rejected]` | `ch05_reserved_contextual_keyword_fn_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E153`): verify stage not run | +| `test_run[ch05_reserved_contextual_keyword_fn_rejected]` | `ch05_reserved_contextual_keyword_fn_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage | | `test_verify[ch05_reserved_resume_fn_rejected]` | `ch05_reserved_resume_fn_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E153`): verify stage not run | | `test_run[ch05_reserved_resume_fn_rejected]` | `ch05_reserved_resume_fn_rejected.vera` | `check` | `run` | `check`-level negative test: no `run` stage | | `test_verify[ch05_where_helper_outer_slot_rejected]` | `ch05_where_helper_outer_slot_rejected.vera` | `check` | `verify` | `check`-level negative test (`expected_error: E130`): verify stage not run | @@ -409,7 +411,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 -├── ... # 243 programs total, organized by spec chapter +├── ... # 244 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 @@ -443,7 +445,7 @@ The manifest is the machine-readable feature inventory — agents can query it t ### Running the conformance suite ```bash -# Via pytest (parametrized — 1,215 tests: five stages × 243 entries) +# Via pytest (parametrized — 1,220 tests: five stages × 244 entries) pytest tests/test_conformance.py -v # Via standalone script (used in CI and pre-commit) @@ -761,7 +763,7 @@ The eager-GC lane is implemented via a `pytest.mark.parametrize("eager_gc", [Fal **Default behaviour**: stress tests are skipped from the per-PR pytest run via `addopts = "-m 'not stress'"` in `pyproject.toml`. Local invocation: ```bash -pytest -m stress # all 16 parametrised test instances (9 logical tests × eager-GC lane) +pytest -m stress # all 26 marker-carrying instances: test_stress.py's 16 (9 logical tests, 7 with an eager-GC twin) + TestHostHandleReclamation573's 10 pytest tests/test_stress.py -m stress -v # full stress suite, verbose pytest tests/test_stress.py::test_array_map_over_10k_int_array -m stress -v # both modes of one test pytest "tests/test_stress.py::test_array_map_over_10k_int_array[eager_gc]" -m stress -v # one mode only @@ -775,7 +777,7 @@ pytest "tests/test_stress.py::test_array_map_over_10k_int_array[eager_gc]" -m st **Failure reporting (cron only)**: when the nightly cron fails, the workflow opens an issue titled "Nightly stress regression on main (tracking)" with the `stress-regression` label, including the commit SHA and the run URL. If an open issue with that label already exists, the new failure posts a comment on it instead of filing a duplicate — so the issue persists across days of failures until a maintainer manually closes it. The `stress-regression` label is auto-created on first failure. This converts cron failures from "visible only to whoever opens the Actions tab" to "visible in the issue feed where Vera work is already triaged." Implementation uses `actions/github-script@v9` with `issues: write` job-scoped permission. -**Budget**: the full suite completes in well under the 5-minute target — measured at **0.66s in-process** on a developer laptop on 2026-05-13 for all 16 test instances (9 logical × eager-GC lane on 7 of them). CI cold-start adds workflow setup time on top. Iteration counts are tuned to the smallest scale where each bug class has historically manifested with ~2-3x safety margin, NOT maximised — the goal is reliable detection of the bug class, not benchmarking. If this measured figure drifts more than ~2x in either direction, treat it as a signal: either iteration counts have grown without rationale (revisit per the "Adding a stress test" rule 2) or a runtime perf regression has landed. +**Budget**: the workflow's suite — `tests/test_stress.py` per the invocation above; the marker's other 10 instances in `test_codegen_gc_reclamation.py` currently run only under an explicit `pytest -m stress` invocation, since the per-PR suite deselects the marker and this workflow is file-scoped ([#1328](https://github.com/aallan/vera/issues/1328)) — completes in well under the 5-minute target: measured at **0.66s in-process** on a developer laptop on 2026-05-13 for its 16 test instances (9 logical × eager-GC lane on 7 of them). CI cold-start adds workflow setup time on top. Iteration counts are tuned to the smallest scale where each bug class has historically manifested with ~2-3x safety margin, NOT maximised — the goal is reliable detection of the bug class, not benchmarking. If this measured figure drifts more than ~2x in either direction, treat it as a signal: either iteration counts have grown without rationale (revisit per the "Adding a stress test" rule 2) or a runtime perf regression has landed. **Assertion shape**: each test asserts on a SPECIFIC observable (e.g. `array_fold` returning the closed-form sum `4999950000`, `IO.print` producing exactly 10000 `x` characters), not just "completed without crashing". This catches a future regression where the loop silently short-circuits or skips iterations. @@ -972,9 +974,9 @@ Twenty-nine scripts in `scripts/` validate cross-cutting concerns beyond unit te | Script | What it validates | |--------|-------------------| -| `check_conformance.py` | All 243 conformance entries hold at their declared level (parse/check/verify/run) — positives pass; the negatives fail at the stage their `expected_error_stage` names (`check` by default, or `compile`, which also asserts the program type-checks cleanly) with their `expected_error` E-code | +| `check_conformance.py` | All 244 conformance entries hold at their declared level (parse/check/verify/run) — positives pass; the negatives fail at the stage their `expected_error_stage` names (`check` by default, or `compile`, which also asserts the program type-checks cleanly) with their `expected_error` E-code | | `check_examples.py` | All 42 `.vera` examples pass `vera check` + `vera verify` | -| `check_corpus_canonical.py` | All 292 corpus programs (recursive over `examples/` + `tests/conformance/`) are in canonical form under `vera fmt` | +| `check_corpus_canonical.py` | All 293 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 | @@ -1081,9 +1083,9 @@ The repository configures 36 hooks across two stages: 34 run at the commit stage | `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 243 conformance entries hold at their declared level — positives pass; negatives fail at the stage their `expected_error_stage` names (`check` or `compile`) with their `expected_error` E-code | +| `check_conformance.py` | All 244 conformance entries hold at their declared level — positives pass; negatives fail at the stage their `expected_error_stage` names (`check` or `compile`) with their `expected_error` E-code | | `check_examples.py` | All 42 examples pass `vera check` + `vera verify` | -| `check_corpus_canonical.py` | All 292 `examples/` + `tests/conformance/` programs (recursive) are in canonical form (`vera fmt`) | +| `check_corpus_canonical.py` | All 293 `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 3d801e1f..71aca508 100644 --- a/docs/SKILL.md +++ b/docs/SKILL.md @@ -2402,7 +2402,7 @@ public fn main(@Unit -> @Unit) ## Conformance Suite -The `tests/conformance/` directory contains 243 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 244 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 08726d78..433fb0a2 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 243-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 244-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 f779ffdf..e7b2b281 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 243-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 244-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 7c7d4184..bb31edc9 100644 --- a/docs/llms-full.txt +++ b/docs/llms-full.txt @@ -2408,7 +2408,7 @@ public fn main(@Unit -> @Unit) ## Conformance Suite -The `tests/conformance/` directory contains 243 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 244 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. @@ -2487,7 +2487,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 243 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 thirty-seven 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_reserved_resume_fn_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch08_ambiguous_import_adt_rejected`, `ch08_ambiguous_import_adt_swapped_rejected`, `ch08_ambiguous_import_rejected`, `ch08_ambiguous_import_swapped_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_reserved_vera_prefix_reference_rejected`, `ch08_reserved_vera_prefix_binder_rejected`, `ch08_reserved_vera_prefix_effect_rejected`, `ch08_reserved_vera_prefix_ability_rejected`, `ch08_reserved_vera_prefix_constructor_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch07_bare_effect_op_rejected`, `ch06_quantifier_array_domain_rejected`, `ch07_handler_state_type_mismatch_rejected`, `ch02_alias_cycle_rejected`, `ch08_module_prelude_adt_contention_rejected`) instead must *fail* with the E-code in their `expected_error` field, at the stage their `expected_error_stage` names — `check` by default, or `compile` for a diagnostic the checker accepts and codegen refuses. 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 244 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 thirty-eight 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_reserved_contextual_keyword_fn_rejected`, `ch05_reserved_resume_fn_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch08_ambiguous_import_adt_rejected`, `ch08_ambiguous_import_adt_swapped_rejected`, `ch08_ambiguous_import_rejected`, `ch08_ambiguous_import_swapped_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_reserved_vera_prefix_reference_rejected`, `ch08_reserved_vera_prefix_binder_rejected`, `ch08_reserved_vera_prefix_effect_rejected`, `ch08_reserved_vera_prefix_ability_rejected`, `ch08_reserved_vera_prefix_constructor_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch07_bare_effect_op_rejected`, `ch06_quantifier_array_domain_rejected`, `ch07_handler_state_type_mismatch_rejected`, `ch02_alias_cycle_rejected`, `ch08_module_prelude_adt_contention_rejected`) instead must *fail* with the E-code in their `expected_error` field, at the stage their `expected_error_stage` names — `check` by default, or `compile` for a diagnostic the checker accepts and codegen refuses. 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 @@ -2666,9 +2666,9 @@ 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 243 conformance programs hold (positives pass; negatives fail with their E-code) +python scripts/check_conformance.py # All 244 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 292 corpus programs in canonical form +python scripts/check_corpus_canonical.py # All 293 corpus programs in canonical form ``` Test helpers follow a pattern: `_check_ok(source)` / `_check_err(source, match)` / `_verify_ok(source)` / `_verify_err(source, match)`. See existing tests for examples. @@ -2677,7 +2677,7 @@ When implementing a new language feature, write the conformance program *first* ### Invariants -- All 243 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_reserved_resume_fn_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch08_ambiguous_import_adt_rejected`, `ch08_ambiguous_import_adt_swapped_rejected`, `ch08_ambiguous_import_rejected`, `ch08_ambiguous_import_swapped_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_reserved_vera_prefix_reference_rejected`, `ch08_reserved_vera_prefix_binder_rejected`, `ch08_reserved_vera_prefix_effect_rejected`, `ch08_reserved_vera_prefix_ability_rejected`, `ch08_reserved_vera_prefix_constructor_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch07_bare_effect_op_rejected`, `ch06_quantifier_array_domain_rejected`, `ch07_handler_state_type_mismatch_rejected`, `ch02_alias_cycle_rejected`, `ch08_module_prelude_adt_contention_rejected`) must *fail* with their `expected_error` E-code, at the stage `expected_error_stage` names — `check` by default, or `compile` for a diagnostic the checker accepts and codegen refuses (`ch08_module_prelude_adt_contention_rejected` → E621), which also asserts the program type-checks cleanly first +- All 244 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_reserved_contextual_keyword_fn_rejected`, `ch05_reserved_resume_fn_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch08_ambiguous_import_adt_rejected`, `ch08_ambiguous_import_adt_swapped_rejected`, `ch08_ambiguous_import_rejected`, `ch08_ambiguous_import_swapped_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_reserved_vera_prefix_reference_rejected`, `ch08_reserved_vera_prefix_binder_rejected`, `ch08_reserved_vera_prefix_effect_rejected`, `ch08_reserved_vera_prefix_ability_rejected`, `ch08_reserved_vera_prefix_constructor_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch07_bare_effect_op_rejected`, `ch06_quantifier_array_domain_rejected`, `ch07_handler_state_type_mismatch_rejected`, `ch02_alias_cycle_rejected`, `ch08_module_prelude_adt_contention_rejected`) must *fail* with their `expected_error` E-code, at the stage `expected_error_stage` names — `check` by default, or `compile` for a diagnostic the checker accepts and codegen refuses (`ch08_module_prelude_adt_contention_rejected` → E621), which also asserts the program type-checks cleanly first - All 42 examples in `examples/` must pass `vera check` and `vera verify` - `mypy vera/` must be clean - `pytest tests/ -v` must pass @@ -3156,7 +3156,7 @@ vera compile --target browser examples/hello_world.vera # index.html ``` -Serve it with any HTTP server and open `index.html` — no build step, no bundler, no dependencies. The JavaScript runtime provides browser-appropriate implementations of the host bindings the browser target supports — the ones a page can host, which leaves a filesystem, an accept loop, a database and a model provider outside it by construction (spec §12.9.3 lists each and why): `IO.print` writes to the page, `IO.read_line` uses `prompt()`, and State, contracts, JSON serialization and Markdown rendering work identically to the wasmtime runtime. `json_stringify` and `md_render` reach that identity by emitting a canonical form the specification states — §9.7.1 and §9.7.3 — rather than by the two hosts happening to agree, which is what the parity suite checks them against. `json_parse` reaches it from the other side, by accepted domain rather than by output form: §9.7.1 states what it takes — RFC 8259-valid text that decodes to finite numbers and strings of Unicode scalar values — so the JavaScript constants (`NaN`, `Infinity`, `-Infinity`) and a lone-surrogate escape are `Err` at the parse on both hosts, with one message, and every text inside the domain parses identically. `md_parse` is the one operation on the shared surface still to reach parity: the two hand-written parsers disagree across nine measured classes of input the §9.7.3 subset leaves open, the largest by a wide margin being how a paragraph's plain-text runs are grouped — invisible to `md_render`, since the runs concatenate to the same text — and the rest render-visible, from how emphasis markers are scanned to block markers such as a `+` bullet or a list nested more than two deep. That one is tracked as [#1301](https://github.com/aallan/vera/issues/1301). +Serve it with any HTTP server and open `index.html` — no build step, no bundler, no dependencies. The JavaScript runtime provides browser-appropriate implementations of the host bindings the browser target supports — the ones a page can host, which leaves a filesystem, an accept loop, a database and a model provider outside it by construction (spec §12.9.3 lists each and why): `IO.print` writes to the page, `IO.read_line` uses `prompt()`, and State, contracts, JSON serialization and Markdown rendering work identically to the wasmtime runtime. `json_stringify` and `md_render` reach that identity by emitting a canonical form the specification states — §9.7.1 and §9.7.3 — rather than by the two hosts happening to agree, which is what the parity suite checks them against. `json_parse` reaches it from the other side, by accepted domain rather than by output form: §9.7.1 states what it takes — RFC 8259-valid text that decodes to finite numbers and strings of Unicode scalar values — so the JavaScript constants (`NaN`, `Infinity`, `-Infinity`) and a lone-surrogate escape are `Err` at the parse on both hosts, with one message, and every text inside the domain parses identically. `md_parse` is the one operation on the shared surface still to reach parity: the two hand-written parsers disagree across nine measured classes of input the §9.7.3 subset leaves open, the largest by a wide margin being how a paragraph's plain-text runs are grouped — invisible to `md_render`, since the runs concatenate to the same text — and the rest render-visible, from how emphasis markers are scanned to block markers such as a `+` bullet or a list nested more than two deep. That one is tracked as [#1301](https://github.com/aallan/vera/issues/1301). `IO.read_char` is separately not yet supported in the browser target at all, and is a not-yet rather than one of the boundaries above — a page could host it, and until the JSPI suspend/resume primitive it needs lands the stub returns an explanatory `Err` reading `IO.read_char not yet supported in browser target`. Two effects are refused outright rather than merely differing. `Inference` and `DB` return an explanatory `Err` from every operation in the browser, because the API key or database credential they would need is readable from page source and network traffic in client-side JavaScript. Reach them through a server-side endpoint and call it with `Http`, which does run in the browser — it is backed by `XMLHttpRequest`, not a stub. That refusal is a deliberate platform boundary; spec §9.5.5 states it for `Inference`. @@ -3222,7 +3222,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 (243 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 (244 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*? @@ -3265,7 +3265,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 -- 11,670 tests, including a 243-program conformance suite +- 11,786 tests, including a 244-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 afb6e578..2989765e 100644 --- a/docs/llms.txt +++ b/docs/llms.txt @@ -56,4 +56,4 @@ Current version: 0.1.11. The reference compiler is written in Python. Install th - [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): 243 programs validating every language feature against the spec. +- [Conformance Suite](https://github.com/aallan/vera/tree/main/tests/conformance): 244 programs validating every language feature against the spec. diff --git a/spec/01-lexical-structure.md b/spec/01-lexical-structure.md index cdc8a6c9..4a57b425 100644 --- a/spec/01-lexical-structure.md +++ b/spec/01-lexical-structure.md @@ -51,7 +51,7 @@ A label written on a **function parameter** or on the **return slot** is preserv ## 1.4 Keywords -The following identifiers are reserved keywords and MUST NOT be used as type names or function names: +The following identifiers are reserved keywords and MUST NOT be used as function names: ``` @@ -60,10 +60,17 @@ match data type module import public private requires ensures invariant decreases assert assume effect handle resume with in forall exists -where true false pure +where true false pure ability +effects op old new result ``` -`handle` is the one exception, and only for function names: `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 a function of that name is not dead code and stays legal. A future host-invoked entry point is exempted on the same grounds; nothing else is. Chapter 5, Section 5.2 gives the full reasoning and the **E153** rule. +The reservation is enforced by **E153** at the declaration, and the compiler derives the list above from the grammar itself rather than from a second hand-maintained copy, so a keyword cannot be reserved in this chapter and admitted by the checker. `resume` is the one entry that is not a grammar keyword; it is reserved on separate grounds, given in Chapter 5, Section 5.2. + +The restriction is on function names alone. Type names cannot collide with a keyword in the first place: every type-namespace binder in the grammar — data types, type aliases, constructors, effects, abilities, and `forall` type parameters — is an `UPPER_IDENT`, and every keyword is lowercase, so `data with` is refused as a malformed type name rather than as a reserved one. + +The restriction is also on the whole identifier, not on a prefix: `older`, `renew`, `matched`, `with_it` and `then_value` are ordinary function names. + +`handle` is the one exception. `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 a function of that name is not dead code and stays legal. A future host-invoked entry point is exempted on the same grounds; nothing else is. Chapter 5, Section 5.2 gives the full reasoning and the **E153** rule. ## 1.5 Operators and Punctuation diff --git a/spec/05-functions.md b/spec/05-functions.md index ac45f89e..08237006 100644 --- a/spec/05-functions.md +++ b/spec/05-functions.md @@ -27,15 +27,19 @@ private fn function_name(@ParamType1, @ParamType2 -> @ReturnType) } ``` -An identifier the grammar claims in expression position is unavailable as a function name. Two groups are affected, and a third name is reserved for a different reason. +An identifier the grammar claims is unavailable as a function name. Three groups are affected, and a fourth name is reserved for a different reason. 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. +The third is the remaining keywords, which the *contextual* lexer admits wherever a name is expected: `then`, `else`, `data`, `type`, `module`, `import`, `public`, `private`, `requires`, `ensures`, `invariant`, `decreases`, `effect`, `with`, `in`, `where`, `pure`, `ability`, `effects`, `op`, and `result`. These differ from the first two groups in that nothing stops a call reaching them — `private fn with(@Int -> @Int)` declares, and `with(1)` resolves to it. They are reserved because Chapter 1, Section 1.4 reserves the identifier: a keyword names one construct, and a second meaning for the same spelling — the language's construct in one position, a user function in another — is what the one-canonical-form rule excludes. Because reachability is not the argument here, the compiler derives this group from the grammar rather than from a list, which is why it covers `ability`, `effects`, `op` and `result`, and why a keyword added to the grammar joins it automatically. + `resume` is reserved on separate grounds. It is not a keyword — a declaration parses, and outside a handler clause a bare `resume(...)` reaches it — but inside every handler clause body `resume` names the operator that resumes the suspended operation (Chapter 7, Section 7.5.2), bound there rather than declared. A function of that name would give one spelling two meanings by position, which the one-canonical-form rule does not admit. Chapter 1, Section 1.4 lists the identifier as reserved; **E153** enforces it, at the declaration and alone — a clause body in the same file still resolves `resume` to the operator, so the rejected declaration draws no second error. Resuming inside a handler clause is unaffected. -In both of the first two 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. +In both of the first two 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. In the third group the declaration is reachable and the program works; what the reservation removes there is the second meaning, not a trap. + +Declaring a function under any name in any of the three groups, or under `resume`, is a compile error (**E153**); rename the function. Because the groups are reserved for different reasons, the diagnostic explains the one that applies — a reader told that `with` can never be called, when their own program just called it, would be misled. 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. diff --git a/tests/conformance/ch05_reserved_contextual_keyword_fn_rejected.vera b/tests/conformance/ch05_reserved_contextual_keyword_fn_rejected.vera new file mode 100644 index 00000000..ceef2313 --- /dev/null +++ b/tests/conformance/ch05_reserved_contextual_keyword_fn_rejected.vera @@ -0,0 +1,27 @@ +-- Conformance: a contextual keyword is not available as a function name (Chapter 5, Section 5.2) +-- Tests: E153 — a user fn named after a grammar keyword the contextual lexer +-- admits as a name is rejected at its declaration (#1296). This branch of the +-- gate is the one whose names are NOT traps: before the reservation this exact +-- program type-checked, verified, compiled and ran, and a bare `with(1)` +-- resolved to the declaration and returned its value. Spec Chapter 1, +-- Section 1.4 reserves the identifier all the same, and nothing held the MUST +-- — the spec and the implementation disagreed about which programs are legal. +-- The reserved set is derived from `vera/grammar.lark` rather than hand-listed, +-- so `ability`, `effects`, `op` and `result` are covered on the same rule even +-- though Section 1.4 never listed them. `handle` stays legal: it is the +-- host-invoked `vera serve` entry point (Chapter 9, Section 9.5.6). +public fn with(@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 db8ab090..dad353fa 100644 --- a/tests/conformance/manifest.json +++ b/tests/conformance/manifest.json @@ -962,6 +962,20 @@ "check_error" ] }, + { + "id": "ch05_reserved_contextual_keyword_fn_rejected", + "file": "ch05_reserved_contextual_keyword_fn_rejected.vera", + "chapter": 5, + "title": "A function named after a contextual grammar keyword is a checker error (#1296)", + "level": "check", + "spec_ref": "Section 5.2", + "expected_error": "E153", + "features": [ + "reserved_fn_name", + "function_declaration", + "check_error" + ] + }, { "id": "ch05_reserved_resume_fn_rejected", "file": "ch05_reserved_resume_fn_rejected.vera", diff --git a/tests/test_checker_modules.py b/tests/test_checker_modules.py index 4aaf3f72..d7c64bca 100644 --- a/tests/test_checker_modules.py +++ b/tests/test_checker_modules.py @@ -1353,11 +1353,21 @@ class TestReservedFnName: * ``old``, ``new`` — declaration accepted, call rejected (E030 / E031). Reserved here, as ``_STATE_FORM_FN_NAMES``. - * ``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. + * ``with``, ``in``, ``effect``, ``op``, ``data``, ``type``, ``import``, + ``public``, ``private``, ``requires``, ``ensures``, ``effects``, + ``decreases``, ``where``, ``then``, ``else``, ``pure``, ``invariant``, + ``module``, ``ability``, ``result`` — declaration *and* call both + accepted, and this row long read "Not reserved; nothing is wrong with + them". Something is: spec §1.4 reserves them and nothing held the + MUST, so the specification and the implementation disagreed about + which programs are legal (#1296). Being callable is what removed the + *unreachability* argument, not the reservation. They are reserved as + ``_CONTEXTUAL_KEYWORD_FN_NAMES`` — derived from ``grammar.lark`` rather + than listed, which is how ``ability``/``effects``/``op``/``result`` + joined despite §1.4 never naming them — and + :class:`TestReservedContextualKeywordFnName` owns that piece. + (``throw`` was on this row and is not a keyword in the grammar at all, + so it stays an ordinary function name.) * ``resume`` — declaration and call both accepted here too, which is why this probe row once read "nothing is wrong with it". Something is: the accepted declaration collides with the resumption binding every handler @@ -2104,6 +2114,304 @@ def test_resume_set_is_its_own_named_piece(self) -> None: assert "resume" in _RESERVED_FN_NAMES +# ===================================================================== +# Reserved CONTEXTUAL keyword function names (E153) — #1296 +# ===================================================================== + +class TestReservedContextualKeywordFnName: + """A ``fn`` named after a *contextual* grammar keyword is rejected + (E153, #1296). + + The fourth piece of :data:`_RESERVED_FN_NAMES`, and the one whose + members are **not** declarable traps. Every name here declares, type + checks, verifies, compiles, runs, and round-trips ``vera fmt``; a + bare call reaches it and returns its value. Lark's contextual lexer + admits the spelling as ``LOWER_IDENT`` wherever a name is expected and + reads it as the keyword only where the keyword's own construct is being + parsed, so nothing collides. + + **Probe record** (run against the pre-#1296 tree, ``private fn + (@Int -> @Int)`` declared and called from ``main``; 21 names × + six positions plus four interaction shapes): + + * All 21 — declaration accepted, bare call accepted, ``vera verify`` + proves the contracts, ``vera run`` returns the computed value, and + ``vera fmt --check`` is clean. Still accepted when called from + inside a contract clause, from an ``if``/``then``/``else`` branch, + from a function that itself carries a ``where { }`` block, and after + a ``let``. No positional ambiguity: unlike ``resume`` these do not + shadow an injected binding, and unlike ``match`` they parse at a call + site. + * ``data`` / ``type`` / constructor positions — refused ``[E005]`` for + every name, but by the *case* rail rather than by any reservation: + the grammar binds every type-namespace name as ``UPPER_IDENT`` and + every keyword is lowercase, so spec §1.4's "type names" half is + vacuous by construction and only the function-name half can be + violated. Pinned by ``test_type_namespace_half_is_vacuous``. + + So the reservation cannot rest on unreachability — that claim is false + for all 21 — and this branch must never reuse the #1187 wording. It + rests on spec §1.4 reserving the identifier, DESIGN principle 1 + (an unenforced MUST is a spec/implementation divergence, whatever the + program does at runtime) and principle 6 (fewer valid programs). + ``test_rationale_makes_no_unreachability_claim`` is the pin. + + **Derived, not hand-listed.** The set comes from ``vera/grammar.lark`` + itself, the shape :func:`builtin_effect_names` already uses for E152, so + a keyword added to the grammar is gated the moment it is added. Four of + the 21 — ``ability``, ``effects``, ``op`` and ``result`` — are grammar + keywords spec §1.4 never listed, and were found by the derivation rather + than by the issue. ``test_reserved_set_is_derived_from_the_grammar`` + pins the derivation against the grammar file. + """ + + #: The names this branch newly reserves (all 21; ``handle`` excluded as + #: the host-invoked carve-out, and the #1187/#1181 pieces excluded as + #: they keep their own rationales). + CONTEXTUAL = ( + # The seventeen spec §1.4 lists and nothing enforced (#1296). + "then", "else", "data", "type", "module", "import", "public", + "private", "requires", "ensures", "invariant", "decreases", + "effect", "with", "in", "where", "pure", + # Four the grammar reserves that spec §1.4 never listed. + "ability", "effects", "op", "result", + ) + + #: Wording from the #1187 keyword branch that is FALSE for these names. + FALSE_CLAIMS = ( + "no unqualified call site can reach", + "does not parse as a call", + "could never be called", + "always lexed as the keyword", + "dead code", + ) + + @staticmethod + def _codes(errs: list[Diagnostic]) -> list[str]: + return [e.error_code for e in errs] + + def test_reserved_set_is_derived_from_the_grammar(self) -> None: + """The reservation is computed from ``grammar.lark``, not hand-listed. + + Reads the grammar file independently of the checker and asserts that + every identifier-shaped string literal it claims — minus the + host-invoked carve-out — is reserved. This is the mutation-catching + pin: replacing the derivation with a hand-list and dropping any one + keyword fails here, which is exactly how #1296 arose (a hand-list + that had silently fallen 21 names behind the grammar). + + ``_`` is excluded because the wildcard pattern is not a valid + ``LOWER_IDENT`` and so can never be a function name. + """ + import re + + from vera.checker.registration import ( + _HOST_INVOKED_FN_NAMES, + _RESERVED_FN_NAMES, + ) + from vera.parser import _GRAMMAR_PATH + + src = re.sub(r"//[^\n]*", "", _GRAMMAR_PATH.read_text(encoding="utf-8")) + literals = { + lit for lit in re.findall(r'"([A-Za-z_][A-Za-z0-9_]*)"', src) + if re.fullmatch(r"[a-z][A-Za-z0-9_]*", lit) + } + # The grammar really does claim these, so the pin has teeth. + assert {"with", "where", "op", "result"} <= literals, sorted(literals) + missing = (literals - _HOST_INVOKED_FN_NAMES) - _RESERVED_FN_NAMES + assert missing == set(), sorted(missing) + + def test_contextual_tuple_matches_checker_set(self) -> None: + """``CONTEXTUAL`` mirrors the checker's contextual piece exactly. + + The sibling of ``test_keyword_tuple_matches_checker_set``: a name + entering the derived set without a per-name cell here fails this pin + instead of silently escaping coverage. + """ + from vera.checker.registration import _CONTEXTUAL_KEYWORD_FN_NAMES + + assert set(self.CONTEXTUAL) == _CONTEXTUAL_KEYWORD_FN_NAMES + + @pytest.mark.parametrize("name", CONTEXTUAL) + def test_contextual_keyword_fn_name_is_E153(self, name: str) -> None: + """Each contextual keyword is refused at the declaration site, + fully tagged per spec §0.5.1.""" + 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 + 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", CONTEXTUAL) + def test_private_contextual_keyword_fn_name_is_E153( + self, name: str, + ) -> None: + """Visibility-independent, as every other 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)) + + @pytest.mark.parametrize("name", CONTEXTUAL) + def test_where_helper_contextual_keyword_is_E153(self, name: str) -> None: + """The where-helper recursion covers this branch too. + + The pre-fix sweep found the helper position mirroring the top-level + one for all 21 (declared, called, ran), so the gate must reach it + identically or the reservation is half-applied. + """ + errs = _errors(f""" +public fn caller(@Int -> @Int) + requires(true) ensures(@Int.result >= 0) effects(pure) +{{ @Int.0 }} +where {{ + fn {name}(@Int -> @Int) + requires(true) ensures(true) effects(pure) + {{ @Int.0 }} +}} +""") + assert "E153" in self._codes(errs), (name, self._codes(errs)) + + @pytest.mark.parametrize("name", CONTEXTUAL) + def test_rationale_makes_no_unreachability_claim(self, name: str) -> None: + """CRITICAL: the branch must not ship the #1187 wording. + + Every phrase in ``FALSE_CLAIMS`` is true of ``match`` and false of + these names — each one is callable, and the pre-fix probe ran them. + A diagnostic asserting otherwise would tell the reader a falsehood + about their own program, which the diagnostic-fields contract + (spec §0.5.1, #955) does not waive for any field. + """ + diag = next( + e for e in _errors(f""" +public fn {name}(@Int -> @Int) + requires(true) ensures(true) effects(pure) +{{ 5 }} +""") if e.error_code == "E153" + ) + text = f"{diag.rationale} {diag.fix}".lower() + for claim in self.FALSE_CLAIMS: + assert claim not in text, (name, claim, diag.rationale) + # It must still say WHY: the identifier is reserved by the spec. + assert "reserved" in text, (name, diag.rationale) + # And it must not borrow either sibling branch's explanation. + assert "state form" not in diag.rationale.lower(), diag.rationale + assert "resumes a suspended" not in diag.rationale.lower(), ( + diag.rationale + ) + + @pytest.mark.parametrize("name", CONTEXTUAL) + def test_fix_suggests_a_usable_replacement(self, name: str) -> None: + """The fix names a concrete replacement that is not itself reserved. + + DESIGN principle 1 asks for "an instruction, not a status report". + A bare ``{name}_fn`` template produces ``in_fn`` / ``type_fn`` / + ``pure_fn``, which is advice no author would take, so the branch + carries a per-name suggestion where the generic suffix misleads. + Pinned by property — the suggested identifier must be a legal Vera + function name and must not be reserved — rather than by exact + wording, so the table can be improved without churning the test. + """ + import re + + from vera.checker.registration import ( + _builtin_reject_names, + _RESERVED_FN_NAMES, + ) + + diag = next( + e for e in _errors(f""" +public fn {name}(@Int -> @Int) + requires(true) ensures(true) effects(pure) +{{ 5 }} +""") if e.error_code == "E153" + ) + quoted = re.findall(r"'([a-z][A-Za-z0-9_]*)'", diag.fix) + suggestions = [q for q in quoted if q != name] + assert suggestions, diag.fix + for s in suggestions: + # Not reserved (E153 again) and not a built-in (E151 instead) — + # advice that trades one error for another is not a fix. + assert s not in _RESERVED_FN_NAMES, (name, s, diag.fix) + assert s not in _builtin_reject_names(), (name, s, diag.fix) + + def test_handle_stays_legal(self) -> None: + """NEGATIVE CONTROL: the carve-out survives a derived set. + + Deriving from the grammar pulls ``handle`` in with every other + keyword, so the subtraction is what keeps ``vera serve`` its entry + point. If the derivation ever forgets it, ``examples/http_server + .vera`` and ``ch09_http_server`` break together. + """ + 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_names_merely_containing_a_contextual_keyword_are_allowed( + self, + ) -> None: + """NEGATIVE CONTROL: the reservation is the whole identifier. + + A substring test would reject a large share of ordinary Vera — + ``with_it``, ``then_value`` and ``older`` are unremarkable function + names, and ``in`` is a substring of a great many words. + """ + for name in ( + "then_value", "older", "with_it", "invariants", "typed", + "public_key", "purity", "wherever", "import_path", "results", + "operation", "effective", "ability_of", "indexed", "dataset", + ): + 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_type_namespace_half_is_vacuous(self) -> None: + """Spec §1.4's "type names" half cannot be violated by construction. + + Every type-namespace binder in the grammar is ``UPPER_IDENT`` and + every keyword is lowercase, so ``data with`` / ``type with = Int;`` + fail at *parse* — and would fail identically for any lowercase name. + Pinned so the spec's corrected wording ("function names") stays + backed by the grammar, and so a future grammar change admitting a + lowercase type name shows up here rather than reopening the hole. + """ + for src in ("private data with {\n MkX(Int)\n}\n", + "type with = Int;\n", + "private data Holder {\n with(Int)\n}\n"): + with pytest.raises(ParseError): + parse_to_ast(src) + # Control: an ordinary LOWERCASE name fails the same way, proving the + # rejection is the case rail and not the reservation. + for src in ("private data helper {\n MkX(Int)\n}\n", + "type helper = Int;\n"): + with pytest.raises(ParseError): + parse_to_ast(src) + + # ===================================================================== # Module-qualified call parse tests (#95) # ===================================================================== diff --git a/vera/README.md b/vera/README.md index 2be365f7..98bdd1c2 100644 --- a/vera/README.md +++ b/vera/README.md @@ -85,7 +85,7 @@ execute(compile_result, ...) # → run WASM via wasmtime | ` core.py` | 1,165 | | TypeChecker class, orchestration, contracts, constraint validation | | | ` resolution.py` | 535 | | AST TypeExpr → semantic Type, inference | | | ` modules.py` | 476 | | Cross-module registration (C7b/C7c), plus the per-module body check that makes a module's diagnostics independent of which file `vera check` was given (#1244) and the #1304 refusal of a bare function, data-type or constructor name two imports both supply (E155/E156/E157) | | -| ` registration.py` | 915 | | Pass 1 forward declarations, ability registration | | +| ` registration.py` | 1,032 | | Pass 1 forward declarations, ability registration | | | ` expressions.py` | 1,485 | | Expression synthesis (bidirectional), operators, statements | | | ` eq_ability.py` | 199 | | Eq ability derivation checks | | | ` sql.py` | 309 | | SQL literal-provenance resolution + placeholder counting (#309) | `resolve_literal_string()`, `count_placeholders()` | @@ -590,7 +590,7 @@ The WASM import interface is the portability contract: the compiled `.wasm` bina ### Browser runtime -`browser/runtime.mjs` is a self-contained JavaScript runtime (~3,877 lines) that provides JavaScript implementations of all Vera host bindings. It works with **any** compiled Vera `.wasm` module — no code generation needed. +`browser/runtime.mjs` is a self-contained JavaScript runtime (~3,877 lines) that provides JavaScript implementations of all Vera host bindings. It works with any core Vera `.wasm` module — the default and browser targets share one import ABI, so no code generation is needed; the `--target wasi-p2` component is a different artifact format with its own host. **Dynamic import introspection:** Instead of generating per-program glue code, the runtime uses `WebAssembly.Module.imports(module)` at initialization to discover which host functions the module actually needs, then builds the import object dynamically. State\ types are pattern-matched from `state_get_*`/`state_put_*` import names. @@ -753,7 +753,7 @@ The `ERROR_CODES` dict in `errors.py` maps every code to a short description (16 ## Test Suite -Testing spans a **pytest suite** of 11,670 tests across 174 files — compiler-internals unit tests plus a **conformance suite** (243 programs in `tests/conformance/` validating every language feature against the spec) and **example programs** (42 end-to-end demos). The conformance suite is the definitive specification artifact — most programs target a single feature, though some (slot references, match, contracts) span several, and each serves as a minimal working example. +Testing spans a **pytest suite** of 11,786 tests across 174 files — compiler-internals unit tests plus a **conformance suite** (244 programs in `tests/conformance/` validating every language feature against the spec) and **example programs** (42 end-to-end demos). The conformance suite is the definitive specification artifact — most programs target a single feature, though some (slot references, match, contracts) span several, and each serves as a minimal working example. See **[TESTING.md](../TESTING.md)** for the comprehensive testing reference -- test file table, conformance suite details, compiler code coverage, language feature coverage, helper conventions, validation scripts, CI pipeline, and guidelines for adding tests. diff --git a/vera/checker/registration.py b/vera/checker/registration.py index b7c107c1..6c883641 100644 --- a/vera/checker/registration.py +++ b/vera/checker/registration.py @@ -69,17 +69,21 @@ def builtin_effect_names() -> frozenset[str]: return _registry_names() -# Identifiers the grammar reserves in *expression* position, so a call to a -# 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). +# Identifiers unavailable as function names (E153). For pieces 1 and 2 the +# grammar claims the spelling in *expression* position, so a function under one +# of those names 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 assembled from four named pieces so a future addition joins the -# right one deliberately. Piece 3 is the exception to the paragraph above: its -# name *is* reachable from expression position, and is reserved because that -# reachability collides with a binding the checker injects. +# The set is assembled from five named pieces so a future addition joins the +# right one deliberately, and each piece carries its own rationale because they +# are reserved for genuinely different reasons. Pieces 3 and 5 are the +# exceptions to the paragraph above — both ARE reachable from expression +# position. Piece 3 is reserved because that reachability collides with a +# binding the checker injects; piece 5 because spec §1.4 reserves the +# identifier and a keyword must not acquire a second meaning by position. +# Only pieces 1 and 2 may claim unreachability in a diagnostic. # 1. The two contract state forms (#1181). ``old_expr`` and ``new_expr`` in # ``vera/grammar.lark`` claim ``"old" "("`` and ``"new" "("``, and each demands @@ -92,12 +96,17 @@ def builtin_effect_names() -> frozenset[str]: # 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]``). Membership is decided by what the -# *lexer* does with the name, and it splits the rest of spec §1.4's keyword -# list two ways. ``with``, ``effect``, ``data``, ``type`` and their kind are -# refused at parse: the contextual lexer does not admit them as a function -# name, so no declaration reaches this checker at all. ``resume`` is refused -# by neither — it is not a keyword token anywhere — and is reserved below on -# its own grounds, by the checker rather than the parser. +# *lexer* does with the name — these are the keywords a call site genuinely +# cannot reach, which is what their rationale below claims. ``resume`` is a +# keyword token nowhere and is reserved by piece 3; every OTHER spec §1.4 +# keyword is reachable and is reserved by piece 5. +# +# This set was once described as covering the whole keyword list, on the +# premise that ``with`` / ``effect`` / ``data`` / ``type`` and their kind were +# "refused at parse: the contextual lexer does not admit them as a function +# name". The tree refuted that premise (#1296): all 21 such names declared, +# type checked, verified, compiled and RAN. They are now reserved by piece 5, +# which argues from the specification rather than from reachability. _KEYWORD_FN_NAMES = frozenset({ "assert", "assume", "forall", "exists", "match", "if", "let", "fn", "true", "false", "handle", @@ -131,6 +140,83 @@ def builtin_effect_names() -> frozenset[str]: # justification — rather than being dropped from the keyword list above. _HOST_INVOKED_FN_NAMES = frozenset({"handle"}) + +@functools.lru_cache(maxsize=1) +def grammar_keyword_names() -> frozenset[str]: + """Every keyword ``vera/grammar.lark`` claims as a bare string literal. + + Read from the grammar file itself (:data:`vera.parser._GRAMMAR_PATH`, the + same one the parser is built from), never a hand-list, so a keyword added + to the grammar is reserved the moment it is added. This is the shape + :func:`builtin_effect_names` already uses for E152, adopted here for the + same reason: the hand-list this replaces had silently fallen 21 names + behind the grammar (#1296), and no gate could see the drift. + + Filtered to identifiers the lexer could actually produce — ``LOWER_IDENT`` + is ``/[a-z][A-Za-z0-9_]*/``, so the wildcard pattern ``"_"`` is excluded + as it can never be a function name. Line comments are stripped first so a + keyword mentioned only in prose is not picked up. + """ + from vera.parser import _GRAMMAR_PATH + + src = re.sub(r"//[^\n]*", "", _GRAMMAR_PATH.read_text(encoding="utf-8")) + return frozenset( + lit for lit in re.findall(r'"([A-Za-z_][A-Za-z0-9_]*)"', src) + if re.fullmatch(r"[a-z][A-Za-z0-9_]*", lit) + ) + + +# 5. The *contextual* keywords: every remaining name the grammar claims (#1296). +# Unlike pieces 1-3 these are not traps. Lark's contextual lexer admits each +# as a name wherever a name is expected and reads it as the keyword only while +# the keyword's own construct is being parsed, so `private fn with(@Int -> +# @Int)` declares, type checks, verifies, compiles, runs, and answers a bare +# `with(1)` — and stays working inside a contract clause, inside an +# `if`/`then`/`else`, in a function carrying a `where { }` block, and after a +# `let`. Nothing about the program breaks. +# +# What breaks is the specification. Spec §1.4 says these identifiers MUST NOT +# be used as function names and nothing held the MUST, so the spec and the +# implementation disagreed about which programs are legal — a model trusting +# §1.4 and a model trusting the compiler derive different programs from the +# same source of truth, and no tool contradicted either. DESIGN principle 1 +# ("checkability over correctness") makes that a defect whatever the program +# does at runtime; principle 6 ("fewer valid programs") chooses enforcement +# over narrowing §1.4; principle 3 supplies the precedent, E152 rejecting even +# a FAITHFUL re-declaration of a built-in effect because a second textual +# spelling is itself the problem. +# +# Derived rather than listed, so the drift cannot recur. Four of the names +# this reserves — `ability`, `effects`, `op`, `result` — are grammar keywords +# spec §1.4 never listed, found by the derivation rather than by the issue. +# A future grammar keyword lands here by default, which is the safe branch: its +# rationale argues from the reservation, which is true of every reserved +# keyword, rather than from unreachability, which is what proved false. +_CONTEXTUAL_KEYWORD_FN_NAMES = ( + grammar_keyword_names() + - _STATE_FORM_FN_NAMES + - _KEYWORD_FN_NAMES + - _HANDLER_OPERATOR_FN_NAMES + - _HOST_INVOKED_FN_NAMES +) + +# A concrete rename for each, because the generic `_fn` template produces +# `in_fn` / `type_fn` / `pure_fn` — advice no author would take, where DESIGN +# principle 1 asks for "an instruction, not a status report". A name absent +# here falls back to the template, so a future grammar keyword still gets a +# usable fix; none of these collides with a built-in (E151) or another +# reserved name, which `test_fix_suggests_a_usable_replacement` pins. +_CONTEXTUAL_RENAME_HINTS = { + "then": "then_branch", "else": "else_branch", "data": "payload", + "type": "type_of", "module": "module_name", "import": "import_path", + "public": "is_public", "private": "is_private", + "requires": "precondition", "ensures": "postcondition", + "invariant": "invariant_of", "decreases": "measure", + "effect": "effect_of", "with": "combined_with", "in": "contains", + "where": "matching", "pure": "is_pure", "ability": "ability_of", + "effects": "effect_row", "op": "operation", "result": "result_of", +} + # 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 @@ -138,7 +224,8 @@ def builtin_effect_names() -> frozenset[str]: # 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 | _HANDLER_OPERATOR_FN_NAMES) + (_STATE_FORM_FN_NAMES | _KEYWORD_FN_NAMES | _HANDLER_OPERATOR_FN_NAMES + | _CONTEXTUAL_KEYWORD_FN_NAMES) - _HOST_INVOKED_FN_NAMES ) @@ -459,19 +546,22 @@ def _check_reserved_type_params( 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), a grammar keyword (#1187), or the - handler-clause resumption operator. + contract state form (#1181), an unreachable grammar keyword (#1187), + the handler-clause resumption operator, or a contextual grammar + keyword (#1296). Recurses into ``where_fns``: a helper is called in expression position exactly like a top-level function, so a helper named ``old`` or - ``match`` is unreachable for the same reason, one scope deeper, and a - helper named ``resume`` collides with the same injected binding. + ``match`` is unreachable for the same reason, one scope deeper, a + helper named ``resume`` collides with the same injected binding, and a + helper named ``with`` is the same second spelling one scope in. The rationale branches on which piece of :data:`_RESERVED_FN_NAMES` - the name came from — the three are reserved for different reasons, and - telling a reader that ``match`` is a "contract state form", or that - ``resume`` is a keyword no call site can reach, would be false. The - fix is the same on every branch: rename. + the name came from — the four are reserved for different reasons, and + telling a reader that ``match`` is a "contract state form", that + ``resume`` is a keyword no call site can reach, or that ``with`` is + unreachable when their own program just called it, would each be + false. The fix is the same on every branch: 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 @@ -524,6 +614,33 @@ def _check_reserved_fn_name(self, decl: ast.FnDecl) -> None: f"Resuming inside a handler clause is unaffected: that " f"'{n}' is bound by the handler, not declared." ) + elif n in _CONTEXTUAL_KEYWORD_FN_NAMES: + hint = _CONTEXTUAL_RENAME_HINTS.get(n, f"{n}_fn") + rationale = ( + f"'{n}' is a keyword of the language: the grammar claims " + f"the spelling for its own construct, and Chapter 1, " + f"Section 1.4 reserves the identifier. Unlike the other " + f"reserved names this one is reachable — the contextual " + f"lexer admits '{n}' as a name where a name is expected, " + f"so the declaration parses and a call resolves to it. " + f"That is what makes it worth refusing rather than " + f"tolerating: the same spelling would name a language " + f"construct in one place and this function in another, " + f"and a reader would have to decide which by position. " + f"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 — '{hint}', 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 contains '{n}' (such as " + f"'{n}_value') is an ordinary function name. 'handle' is " + f"the one keyword still available, because 'vera serve' " + f"invokes it from the host rather than from Vera source." + ) else: rationale = ( f"'{n}' is a keyword the grammar reserves in expression "