From 3962dde55ca25f6e427460f7653c48f01feddcbc Mon Sep 17 00:00:00 2001 From: Alasdair Allan Date: Sun, 6 Sep 2026 23:27:52 +0100 Subject: [PATCH] Key constructor layouts per owning ADT MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Code generation held constructor layouts in one table keyed by bare constructor name across every data type (`ctor_layouts.update(layouts)` over `_adt_layouts.items()`, built-ins first), so a later declaration won the slot outright. #1408 closed that for `Tuple` and `Future` by reserving the names; the mechanism was general, and for an unreserved name it was a silent wrong value. With `private data ZzBox { Less(Bool) }` anywhere in the file — never used — `show(compare(1, 2))`, `(2, 1)` and `(2, 2)` all returned `Less(false)` where the control returns `Less` / `Greater` / `Equal`, on a program `vera check` and `vera verify` both call clean. A second shape degraded rather than lying: `private data ZzBox { UrlParts(Bool) }` beside a genuine `show(@UrlParts)` compiled to a module with no exports behind an `[E602]` warning. Both measured identical at release/v0.2.0 and at the #1404 merge tip. Widening the reservation is not the fix and is not done. §8.4.1 makes the prelude's data types shadowable, #1277 says so in terms, and an AST-level corpus scan — validated against a known positive first, since the obvious version of it silently misses everything by not unwrapping `TopLevelDecl` — shows `examples/vera/collections.vera` declares `None` and `Some`, so a reservation over prelude constructor names would refuse a shipped example. `Tuple` and `Future` are reserved because their SEMANTICS are special-cased by name, which is a different property. So the layouts are keyed per owning ADT. The wasm layer carries the unflattened map beside the flat one; the constructor-plan derivation that renders and compares a value reads the ADT it was asked about rather than whatever the by-name table held; and the three `Ordering` references the `compare` desugaring emits carry their owner structurally, because that desugaring's `Less` means `Ordering` whatever the program declares and a name lookup is exactly what a declaration can move. A bare constructor call whose name genuinely collides is still resolved by name — that is the checker's job, and it already refuses the ambiguous cases (E213/E215/E121). The user's own shadowing constructor keeps working: `show(Less(true))` is `Less(true)` beside `Ordering`'s. Also from the #1404 review round: `test_a_constructor_of_an_unreserved_ builtin_name_is_fine` is renamed to say what it measures (E158 does not fire) rather than a safety property this bug shows it does not have; the two SKILL copies say the reservation covers both namespaces; and a constructor the checker has just refused no longer lands in `env.constructors`. Corpus differential against release/v0.2.0: one mover, the new conformance program itself. Review round 3 closes the remaining findings. Constructor names are unique per NAMESPACE (spec §8.4), and two of the three namespaces had a rail — E610 for two modules, E157 for two imports — while a single file had none. Two declarations sharing a constructor name were accepted silently, and a USE then reported whichever declaration registered last: `Rose { Leaf(T), Node(T, Rose) }` beside `ZzBox { Node(Bool) }` gave "Constructor 'Node' expects 1 field(s), got 2", the OTHER type's arity. That is now E159 at the second declaration, scoped to the registration pass rather than to `env.constructors` — which already holds the prelude's and the imports' entries by then — so the two shadowing shapes §8.4.1 and §8.5.2 make legal are untouched, and both are celled. Corpus and examples: zero refusals outside the new negative. `_desugar_compare` now stamps its three `Ordering` references with their owner, making its "mirrors codegen exactly" docstring true again, and the SMT nullary sort resolves by owner before the recorded-type hint and the bare-name scan. A desugared node has no recorded type of its own, so the scan answered — and a user `data ZzBox { Pad(Bool), Less }` captured the `Less` that `compare` emits, demoting a statically REFUTED postcondition to Tier 3 with exit 0. It reports E500 again, celled across four declaration shapes against the no-declaration control. The flat-map fallbacks are gone, on measurement rather than argument: instrumented over the full pytest suite, the conformance suite twice (the second under VERA_EAGER_GC=1), the examples' check/verify and run gates, and a compile of all 302 corpus programs, all three were reached zero times. The door's impossible case now raises instead of re-resolving by bare name, which is what would have hidden this defect class. A structural rail replaces the one-at-a-time discovery that found the last three sites: every `_ctor_layouts` access in `vera/wasm/` and `vera/smt.py` must be the owner-qualified door or carry a `# ctor-owner-exempt:` reason, mutation-validated to red when a marker is withdrawn. `operators.py`'s conversion stays inert under coverage, and its three legs are asserted rather than asserted-about: the flat enumeration really does lose `Ordering`'s `Less`, every `Ordering` constructor is nullary so the emitted equality cannot see the loss, and the field-carrying shadow that would observe it is unbuildable (E159, or E213 for `Some`/`Ok`/`Err`). Review round 4 closes the five findings that round left open. The new ICE is gone. `_owned_ctor_layout` raised when an owner-stamped reference named a constructor its owner does not declare, and §8.4.1 permits exactly that: `private data Ordering { Less, Equal }` beside `show(compare(1, 2))` is check-clean and verify-clean, and the desugared `Greater` has nowhere to resolve. The door degrades to no-layout, so the caller's CodegenSkip reports the construct and drops the function — the behaviour the compiler had before #1414 — and the nested-recovery site takes the same door rather than silently re-resolving by bare name, so one condition has one policy. Resolving an owner-stamped reference against the built-in snapshot first was tried and reverted: it repairs the constructor's layout but not the render side, which enumerates `Ordering` out of the same ADT-name-keyed map and gets the user's constructors, and the module then fails to load — worse than the skip. Both sides have to become owner-aware together, which is the same per-(owner, ADT, constructor) keying #1436 needs. The structural rail is widened from one attribute in seven hand-listed files to three (`_ctor_layouts`, `_ctor_to_adt`, `_ctor_adt_tp_indices`) across all of vera/wasm/ and vera/codegen/ plus vera/smt.py, discovered by globbing so a new module joins by existing. `vera/smt.py` was listed for an attribute it does not use, which made its listing vacuous while `monomorphize.py` — which builds its own flat ownership map — was outside the rail; both are covered now, the allowlist matches on (class, function) rather than a bare `__init__` name, and the non-vacuity cell asserts every attribute the rail claims is actually present. Two claims this PR made are corrected rather than defended. The `operators.py` justification asserted the observing shadow is "unbuildable"; it is buildable across a module boundary, and that shape is is generated there at all — and the cell now says so. E159's fix text and the new spec §8.4 sentence asserted that shadowing an IMPORTED constructor is safe; the prelude half is true and the imported half is not, so the spec now points at the §11.16 compilation caveat and the fix text claims only the prelude case. Fixes #1414 Fixes #1425 Co-Authored-By: Claude --- AGENTS.md | 8 +- CHANGELOG.md | 4 + CLAUDE.md | 8 +- FAQ.md | 4 +- KNOWN_ISSUES.md | 2 +- README.md | 2 +- ROADMAP.md | 2 +- SKILL.md | 6 +- TESTING.md | 36 +- docs/SKILL.md | 6 +- docs/index.html | 2 +- docs/index.md | 2 +- docs/llms-full.txt | 19 +- docs/llms.txt | 2 +- spec/08-modules.md | 14 +- spec/11-compilation.md | 2 + .../ch08_sibling_ctor_collision_rejected.vera | 22 + .../ch09_user_ctor_shadows_prelude_ctor.vera | 19 + tests/conformance/manifest.json | 26 + tests/test_name_resolution_spine_1316.py | 828 +++++++++++++++++- vera/README.md | 6 +- vera/_since.py | 1 + vera/ast.py | 13 + vera/checker/registration.py | 100 ++- vera/codegen/closures.py | 4 + vera/codegen/core.py | 11 +- vera/codegen/functions.py | 4 + vera/codegen/modules.py | 6 + vera/codegen/monomorphize.py | 3 + vera/codegen/registration.py | 13 + vera/errors.py | 1 + vera/smt.py | 45 +- vera/wasm/calls.py | 2 + vera/wasm/calls_handlers.py | 51 +- vera/wasm/context.py | 63 ++ vera/wasm/data.py | 26 +- vera/wasm/inference.py | 17 +- vera/wasm/operators.py | 26 +- 38 files changed, 1313 insertions(+), 93 deletions(-) create mode 100644 tests/conformance/ch08_sibling_ctor_collision_rejected.vera create mode 100644 tests/conformance/ch09_user_ctor_shadows_prelude_ctor.vera diff --git a/AGENTS.md b/AGENTS.md index 6eb2ab4d1..fe2261622 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 251 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 forty-five negative fixtures (`ch02_generic_over_unit_rejected`, `ch02_map_unit_value_rejected`, `ch02_nonregular_data_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`, `ch04_pattern_ctor_over_container_rejected`, `ch04_pattern_literal_type_rejected`, `ch05_where_helper_sibling_call_rejected`, `ch08_builtin_adt_redefinition_rejected`, `ch08_builtin_tuple_redefinition_rejected`, `ch08_builtin_ctor_redefinition_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 253 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 forty-six negative fixtures (`ch02_generic_over_unit_rejected`, `ch02_map_unit_value_rejected`, `ch02_nonregular_data_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`, `ch04_pattern_ctor_over_container_rejected`, `ch04_pattern_literal_type_rejected`, `ch05_where_helper_sibling_call_rejected`, `ch08_builtin_adt_redefinition_rejected`, `ch08_builtin_tuple_redefinition_rejected`, `ch08_builtin_ctor_redefinition_rejected`, `ch08_sibling_ctor_collision_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 @@ -193,9 +193,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 251 conformance programs hold (positives pass; negatives fail with their E-code) +python scripts/check_conformance.py # All 253 conformance programs hold (positives pass; negatives fail with their E-code) python scripts/check_examples.py # All 43 examples must pass -python scripts/check_corpus_canonical.py # All 301 corpus programs in canonical form +python scripts/check_corpus_canonical.py # All 303 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. @@ -204,7 +204,7 @@ When implementing a new language feature, write the conformance program *first* ### Invariants -- All 251 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`, `ch02_nonregular_data_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`, `ch04_pattern_ctor_over_container_rejected`, `ch04_pattern_literal_type_rejected`, `ch05_where_helper_sibling_call_rejected`, `ch08_builtin_adt_redefinition_rejected`, `ch08_builtin_tuple_redefinition_rejected`, `ch08_builtin_ctor_redefinition_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 253 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`, `ch02_nonregular_data_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`, `ch04_pattern_ctor_over_container_rejected`, `ch04_pattern_literal_type_rejected`, `ch05_where_helper_sibling_call_rejected`, `ch08_builtin_adt_redefinition_rejected`, `ch08_builtin_tuple_redefinition_rejected`, `ch08_builtin_ctor_redefinition_rejected`, `ch08_sibling_ctor_collision_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 43 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 a331f1bc1..33ec50729 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -83,6 +83,10 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/). - **A constructor named after a special-cased built-in ADT is refused, closing a silent wrong value** ([#1408](https://github.com/aallan/vera/issues/1408)). #1397 reserved `Tuple` and `Future` in the `data` TYPE namespace; the CONSTRUCTOR namespace stayed open, and `private data Pair { Tuple(Int, Int) }` was accepted with the declared constructor unreachable in both positions — `show(Tuple(1, 2))` rendered the BUILT-IN carrier's `(1, 2)` where the fresh-named control `MkPair` rendered `MkPair(1, 2)`, the pattern was `[E314]` whose fix text then prescribed the constructor it had just refused, and `Pair` was uninhabitable. Worse, `vera/codegen/functions.py` flattens `ctor_layouts` by CONSTRUCTOR name across every ADT, so the user's layout won the carrier's flat slot — measured, `ctor_layouts['Tuple'].field_offsets` became `((8, 'i64'),)` where the carrier's is `()` — and the tuple-construction gate then read it as "user ADT" and skipped the #820 `@Nat`-to-`@Int` widening guard on a GENUINE built-in tuple construction elsewhere in the same program: with an unrelated `private data ZzBox { Tuple(Bool) }` in the file, `tc(u64.MAX)` returned a reinterpreted negative `@Int` with no trap, and the verifier stopped obligating the coercion because `_lookup_constructor_info` found the user's constructor. A `Bool` payload is load-bearing: with `Tuple(Int)` the clobbered layout's `int_fields` re-guards the component by coincidence and hides the hole. All of it measured identical at `release/v0.2.0`. E158 now covers both namespaces a declaration can put the name in, from the same registry-derived set, with `tests/conformance/ch08_builtin_ctor_redefinition_rejected.vera` pinning it and spec §8.4.1 saying which halves the reservation covers. Zero corpus impact: an AST-level scan of all 300 `examples/` + `tests/conformance/` programs finds no declared constructor of either name. +- **Two data declarations in one namespace may no longer share a constructor name** ([#1425](https://github.com/aallan/vera/issues/1425)). Spec §8.4 puts constructor-name clashes under one rule — "rejected at check time, in whichever namespace holds the clash: the entry program's, or any module's" — and two of the three namespaces had a rail (`E610` for two modules, `E157` for two imports) while a single file had none. `private data A1 { Pair(Int, Int) }` beside `private data A2 { Pair(Bool, Bool) }` was accepted with no diagnostic; a USE of the name then produced `[E212]`/`[E213]` describing whichever declaration registered last rather than the collision — measured, `Rose { Leaf(T), Node(T, Rose) }` beside `ZzBox { Node(Bool) }` reported "Constructor 'Node' expects 1 field(s), got 2", the OTHER type's arity, and which declaration won depended on source order. That is now **E159**, located at the second declaration and naming the first. It is scoped to the registration pass rather than to `env.constructors`, which already holds the prelude's and the imports' entries by then, so the two shadowing shapes §8.4.1 and §8.5.2 make legal are untouched and celled as such: restating a prelude type (`examples/vera/collections.vera` declares `None` and `Some`) and shadowing an imported constructor. Measured across the corpus and examples: zero refusals outside the new `ch08_sibling_ctor_collision_rejected` negative. + +- **A user constructor no longer displaces a built-in or prelude constructor of the same name** ([#1414](https://github.com/aallan/vera/issues/1414)). Code generation held constructor layouts in one table keyed by bare constructor name across every data type, so a later declaration won the slot outright. #1408 closed that for `Tuple` and `Future` by reserving the names; the mechanism was general, and for at least one unreserved name it was a **silent wrong value**: with `private data ZzBox { Less(Bool) }` anywhere in the file — never used — `show(compare(1, 2))`, `(2, 1)` and `(2, 2)` all returned `Less(false)` where the control returns `Less` / `Greater` / `Equal`, on a program with zero diagnostics from both `vera check` and `vera verify`. A second shape degraded instead of lying: `private data ZzBox { UrlParts(Bool) }` beside a genuine `show(@UrlParts)` compiled to a module with no exports behind an `[E602]` warning. Both measured identical at `release/v0.2.0` and at the #1404 merge tip. Widening the reservation is not the fix and is not done: §8.4.1 makes the prelude's data types shadowable, #1277 says so in terms, and `examples/vera/collections.vera` declares `None` and `Some`, so a reservation over prelude constructor names would refuse a shipped example. Instead the layouts are keyed per **owning ADT**: the wasm layer carries the unflattened map beside the flat one, the constructor-plan derivation that renders and compares a value reads the ADT it was asked about rather than whatever the by-name table held, and the three `Ordering` references the `compare` desugaring emits now carry their owner structurally instead of being resolved by a name a declaration can move. A bare constructor call whose name genuinely collides is still resolved by name — that is the checker's job, and it already refuses the ambiguous cases (E213/E215/E121). Both halves are converted, which the first form of this fix was not: keying only the READER left the value TAGGED out of the user's ADT and rendered out of `Ordering`'s, and the two agree exactly when the shadowing constructor sits at its namesake's index — so `data ZzBox { Less(Bool) }` looked correct while `{ Pad(Bool), Less }` rendered `compare(1, 2)` as `Equal` and `{ A, B, C, Less }` rendered it `Greater`. The tag now comes from the same owner-qualified table the value is read through, pinned by a battery over three shadow indices and `compare` on `Int` / `String` / `Float64`, plus `eq` and `hash` of the results — `eq(compare(1, 2), compare(2, 2))` was true under the half-fix, with `hash` agreeing, so neither reader would have caught the other. The user's own shadowing constructor keeps working: `show(Less(true))` is `Less(true)` beside `Ordering`'s `Less`. + - **Running the corpus differential no longer turns the test suite red** ([#1374](https://github.com/aallan/vera/issues/1374)). `scripts/check_corpus_differential.py` materialised its base revision as a git worktree under `.corpus-differential/` and left it there by design — a reuse optimisation, since a burndown session compares repeatedly against one base. What it leaves is a full second copy of the repository INSIDE the repository, and `scripts/check_doc_builtin_shadowing.py`'s doc-surface walk descended into it: every definition in that copy's `spec/09-standard-library.md` was reported as a documentation example redefining a built-in, so `pytest tests/` went red with ~90 offenders after any run of the documented instrument — reading as a regression from whatever change was in flight. Both halves are fixed, because either alone leaves the other's failure mode reachable. The walk now prunes any directory carrying its own `.git` alongside the named `.corpus-differential` entry, stated as a rule about nested checkouts rather than a name list, since `--work-dir` is settable and a stray clone under the repo root is the same hazard whatever it is called; the repo's own `.git` cannot prune the walk it starts, because pruning happens on `os.walk`'s `dirnames` and the root is never in one. And the differential now removes its checkout when the run ends — through `git worktree remove`, not a directory delete, so the repository's worktree registry does not keep a stale entry the next run's cleanliness check cannot see — with `--keep-base` to opt back into the reuse. Removal is best-effort and wrapped around every exit path including the canary refusals: the verdict is already computed by then, and losing it to a housekeeping error would be the worse failure. - **A `type` alias named after a prelude ADT no longer leaks into the prelude's own bodies** ([#1316](https://github.com/aallan/vera/issues/1316)). One of three bugs sharing one root: every derivation that turns a type NAME into a representation re-implemented the checker's branch order by hand, against whatever alias and ADT tables happened to be installed. This is the ENVIRONMENT half. `_type_aliases` is one flat map, so a PRELUDE combinator's body rendered against whatever it held — the entry file's — and under `type Json = Int;`, with no json call anywhere in the program, the prelude's own `json_get` took the alias's i64 where its body wanted the ADT's i32 pointer: the module died at load with `type mismatch: expected i32, found i64` inside `json_get`, on a check-green, verify-green program. `type HtmlNode = Int;` was the same failure in `html_attr`. Spec §8.4.1 scopes the alias namespace to the declaring module, and the prelude is a namespace like any other: `vera.prelude.PRELUDE_NAMESPACE` now names it, its declarations register, its bodies compile and its generic clones are registered and emitted inside `_module_alias_scope(PRELUDE_NAMESPACE)`, and `_declaration_namespace` is the one predicate every registration and emission door asks. Its ADT membership is stated rather than looked up — global infrastructure only — which has to be answered even for a single-file program, where the permissive whole-map answer would hand the prelude the ENTRY file's declarations; the entry program's own `data` names now join `_namespace_declared_adts` so that holds. The wasm layer's ADT-name set became the namespace-scoped `AliasEnv.data_types` rather than the flat layout map, without which an entry `data Array` would have been a data type inside the prelude's own `Array` parameters. Pinned positionally as well as behaviourally: every prelude declaration must compile with the prelude namespace installed and every user declaration with the entry's, and `_fn_sigs['json_get']` must record the prelude's own width — masked today by the Pass-2 derivation, so a falsehood waiting for its first consumer. diff --git a/CLAUDE.md b/CLAUDE.md index f52c8daf1..f3dee6a33 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -62,10 +62,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 251 conformance programs (positives pass their level; negatives fail with their expected_error E-code) +python scripts/check_conformance.py # Verify all 253 conformance programs (positives pass their level; negatives fail with their expected_error E-code) python scripts/check_examples.py # Verify all 43 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 301 corpus programs are in canonical form (vera fmt) +python scripts/check_corpus_canonical.py # Verify all 303 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 @@ -99,7 +99,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/` — 43 example Vera programs (all must pass `vera check` and `vera verify`) - `tests/` — Test suite (unit tests + conformance suite) -- `tests/conformance/` — 251 conformance programs validating every language feature against the spec +- `tests/conformance/` — 253 conformance programs validating every language feature against the spec - `scripts/` — CI and validation scripts ## Writing Vera code @@ -136,7 +136,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 251 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`, `ch02_nonregular_data_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`, `ch04_pattern_ctor_over_container_rejected`, `ch04_pattern_literal_type_rejected`, `ch05_where_helper_sibling_call_rejected`, `ch08_builtin_adt_redefinition_rejected`, `ch08_builtin_tuple_redefinition_rejected`, `ch08_builtin_ctor_redefinition_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 253 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`, `ch02_nonregular_data_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`, `ch04_pattern_ctor_over_container_rejected`, `ch04_pattern_literal_type_rejected`, `ch05_where_helper_sibling_call_rejected`, `ch08_builtin_adt_redefinition_rejected`, `ch08_builtin_tuple_redefinition_rejected`, `ch08_builtin_ctor_redefinition_rejected`, `ch08_sibling_ctor_collision_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 43 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 c72821e8b..5ad6b4b63 100644 --- a/FAQ.md +++ b/FAQ.md @@ -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 one preferred surface spelling `vera fmt` produces deterministically), which reduces the surface area a model needs to learn. Third, the conformance test suite (251 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, and 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 one preferred surface spelling `vera fmt` produces deterministically), which reduces the surface area a model needs to learn. Third, the conformance test suite (253 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, and 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 -- 13,517 tests, including a 251-program conformance suite +- 13,575 tests, including a 253-program conformance suite - 43 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 0b8211c13..7a3d1fa5d 100644 --- a/KNOWN_ISSUES.md +++ b/KNOWN_ISSUES.md @@ -29,7 +29,7 @@ Things Vera cannot do yet, as distinct from defects in what it claims to do. | `vera test`'s input generator builds its `SmtContext` without the function lookup, ADT registry, or recorded-type hook the verifier has, so a `requires` that calls a user function — or any built-in without an explicit translation branch — is untranslatable there and the target is skipped, though the verifier translates the same contract fine. Every such skip is disclosed by name; threading the function lookup and callee-scope machinery through recovers the coverage. | [#1249](https://github.com/aallan/vera/issues/1249) | | Effect row variables cannot be unified, so higher-order functions polymorphic over their effect rows are not expressible. Full effect polymorphism is Milestone 4 work. | [#294](https://github.com/aallan/vera/issues/294) | | Every `vera` invocation re-parses and re-checks the whole module graph from scratch. Incremental compilation is Milestone 4 work; the LSP server's warm `VerificationSession` already covers the editor loop. | [#56](https://github.com/aallan/vera/issues/56) | -| A module cannot re-export an imported symbol, so deep module trees force consumers to import from the defining file. Sequenced in Milestone 4, behind the per-owner declaration identity that now gives a re-exported name somewhere unambiguous to land. | [#127](https://github.com/aallan/vera/issues/127) | +| A module cannot re-export an imported symbol, so deep module trees force consumers to import from the defining file. Sequenced behind module-qualified call disambiguation (#187) in Milestone 4. | [#127](https://github.com/aallan/vera/issues/127) | | There is no package system or registry — all code shares one module tree resolved from the filesystem. Milestone 4 work; the issue carries the design discussion. | [#130](https://github.com/aallan/vera/issues/130) | | There is no interactive read-eval-print loop; the shortest feedback path is `vera run` on a file. Milestone 3 developer-experience work. | [#224](https://github.com/aallan/vera/issues/224) | | The language server resolves module imports from disk rather than open editor buffers, so unsaved changes in imported files aren't seen. Buffer-aware resolution is roadmap Tier 3. | [#724](https://github.com/aallan/vera/issues/724) | diff --git a/README.md b/README.md index b9d439be5..978f6ae77 100644 --- a/README.md +++ b/README.md @@ -261,7 +261,7 @@ cp /path/to/vera/SKILL.md ~/.claude/skills/vera-language/SKILL.md ## Project status -Vera is in **active development** at v0.1.13: 2,000+ commits, 211 releases, 13,517 tests, 95% Python code coverage, 251 conformance programs, 43 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.13: 2,000+ commits, 211 releases, 13,575 tests, 95% Python code coverage, 253 conformance programs, 43 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 7a3161e38..8dd0cd541 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 -13,517 tests, 251 conformance programs, 43 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. +13,575 tests, 253 conformance programs, 43 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. ## The v0.2.0 burndown diff --git a/SKILL.md b/SKILL.md index 9ae320621..8b6018a72 100644 --- a/SKILL.md +++ b/SKILL.md @@ -498,7 +498,7 @@ match @Tuple.0 { } ``` -`Tuple` is just an upper-case constructor — there is no special tuple-literal syntax (no `(1, 2, 3)` form). The empty tuple `Tuple<>` is equivalent to `Unit`. The name is reserved in the data namespace: `data Tuple { ... }` is rejected at `vera check` with **E158** (see below), because the compiler recognises `Tuple` by name when it renders and lays out a value. A `type Tuple = ...` alias is unaffected. +`Tuple` is just an upper-case constructor — there is no special tuple-literal syntax (no `(1, 2, 3)` form). The empty tuple `Tuple<>` is equivalent to `Unit`. The name is reserved in both the data and the constructor namespace: `data Tuple { ... }` and `data Box { Tuple(Bool) }` are each rejected at `vera check` with **E158** (see below), because the compiler recognises `Tuple` by name when it renders and lays out a value. A `type Tuple = ...` alias is unaffected. ### Type aliases @@ -1303,6 +1303,8 @@ infinity() -- returns Float64 (positive infinity) **Redefining a special-cased built-in ADT is an error (E158)**: `data Future { ... }` and `data Tuple { ... }` are rejected at `vera check`, at the entry file and inside a module alike. These two names the compiler recognises *by name* throughout code generation — how a value is rendered, compared and laid out — so a declaration of one could not be told apart from the built-in, and accepting it was silent: `show(MkShadow(7))` under a `data Tuple` printed `(7)`, dropping the constructor name, and `data Future` compiled to a module that fails to load. It is the same rule that reserves built-in function names (E151) and built-in effect names (E152), and it covers both namespaces a declaration can put the name in: the `data` type name and a **constructor** name inside any ADT (`data Box { Tuple(Bool) }` is also E158, because code generation flattens constructor layouts by name and the user's would displace the built-in carrier's). Only those two: the prelude's data types (`Option`, `Result`, `Ordering`, `UrlParts`, `Json`, `HtmlNode`, `MdBlock`, `MdInline`, `Request`, `Response`) are ordinary declarations a program may shadow — `examples/vera/collections.vera` ships a `public data Option` — and so are the container names `Array`, `Map`, `Set` and `Decimal`. A `type Future = ...` / `type Tuple = ...` alias is unaffected: an alias names a binding, not a layout. Rename the declaration, or use the built-in directly. +**Two declarations may not share a constructor name (E159)**: within one file, two `data` declarations may not both declare a constructor of the same name — `private data A1 { Pair(Int, Int) }` beside `private data A2 { Pair(Bool, Bool) }` is rejected at `vera check`, located at the second declaration and naming the first. Constructor names are resolved by name alone, so one namespace cannot hold two, and accepting the pair produced diagnostics describing whichever declaration registered last rather than the collision. It is the single-file sibling of E610 (two modules) and E157 (two imports). Shadowing a *prelude* constructor is a different shape and stays legal — a program may restate `Option`, `Result` or `Ordering` — as is shadowing an *imported* constructor (§8.5.2), though see §11.16 for the compilation caveat on that pair. + **Reserved function names (E153)**: three groups of identifier cannot be a function name — two the grammar claims in expression position, and one the checker binds. `old` and `new` are contract state forms, so `old(...)` / `new(...)` always parses as a reference to an effect's before/after state (Chapter 7, Section 7.9.2) and never as a call. `assert`, `assume`, `forall`, `exists`, `match`, `if`, `let`, `fn`, `true` and `false` are keywords the lexer admits as a name after `fn` but reads as the keyword everywhere else, so `match(3)` in a body does not parse as a call either. A function under any of these — top-level, `where`-helper, or in an imported module — could never be called, and is rejected at `vera check`. Rename it. `resume` is reserved as well, for a different reason: it is not a keyword and a declaration does parse, but inside every handler clause body `resume` is the resumption operator, so declaring a function of that name would give one spelling two meanings by position. The rejection is the whole story: a clause body in the same file still resolves `resume` to the operator, so the rejected declaration draws no second error. Writing `resume(...)` inside a handler clause is unaffected. Only the exact identifiers are reserved: `older`, `renew`, `matched`, `resumed` and the like are ordinary function names. `handle` is the one keyword still available, because `public fn handle(@Request -> @Response)` is the entry point `vera serve` invokes from the host (Chapter 9, Section 9.5.6). Example: @@ -2472,7 +2474,7 @@ public fn main(@Unit -> @Unit) ## Conformance Suite -The `tests/conformance/` directory contains 251 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 253 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 f87dac1fa..784b00700 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** | 13,517 across 203 files (~192,000 lines of test code; 13,302 passed + 26 stress-deselected, 189 skipped) | +| **Tests** | 13,575 across 203 files (~192,000 lines of test code; 13,358 passed + 26 stress-deselected, 191 skipped) | | **Compiler code coverage** | 95% Python, 87% JavaScript (CI minimum: 80%) | -| **Conformance programs** | 251 programs across 9 spec chapters, validating every language feature | +| **Conformance programs** | 253 programs across 9 spec chapters, validating every language feature | | **Example programs** | 43, all validated through `vera check` + `vera verify` | | **Spec code blocks** | 189 parseable blocks from 14 spec chapters: 92 parse, 86 type-check, 85 verify (the rest carry inline `vera:skip` annotations, #538) | | **README code blocks** | 4 Vera blocks (4 validated, 0 annotated) | @@ -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 (251 programs, see manifest.json) +python scripts/check_conformance.py # conformance suite (253 programs, see manifest.json) python scripts/check_examples.py # 43 example programs python scripts/check_spec_examples.py # spec code blocks python scripts/check_readme_examples.py # README code blocks @@ -109,7 +109,7 @@ python scripts/check_wheel_availability.py # pre-flight: every runtime | `test_checker_errors.py` | 74 | 1,231 | 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) | -| `test_obligations.py` | 779 | 1,920 | Reified proof obligations + warm `VerificationSession` (#222 Phase A): full-corpus differential oracle (warm session == cold `verify()` on diagnostics, summary, and obligation stream, plus warm-twice determinism, across all 43 examples and every verify/run-level conformance program), summary↔obligation tier-bookkeeping consistency (including the #967 `total == tier1_verified + tier3_runtime` leg, plus a focused self-consistency pin on the three call-demotion examples), the #1242 stream partition — over a corpus widened to every conformance program that type-checks, at any level, `len(obligations) == total + violated + tier3_unguarded` and every status is one of the documented five, with the vocabulary read from the `ObligationStatus` Literal so a sixth member fails rather than vanishing from the counts — per-kind unit tests (requires / ensures / decreases / nat_sub / call_pre statuses, counterexamples, error codes), content-key stability + same-text-two-sites span disambiguation, session solver reuse, type-error short-circuit, ADT-registry resync between programs; plus the Phase B incremental suite — identical-source full replay, callee-body-edit replays callers while callee-contract-edit invalidates them, span-shift and ADT-edit conservative invalidation, cross-program isolation, timeout-status never cached (monkeypatched solver), FIFO eviction bound; plus the #727 dedup pin — a violating call in a let RHS records exactly one E501 diagnostic and one call_pre obligation; plus the #1208 call-site rendering pin — a PARAMETERISED callee slot substitutes into the E501 message and its fix instead of falling back to the generic wording | +| `test_obligations.py` | 782 | 1,920 | Reified proof obligations + warm `VerificationSession` (#222 Phase A): full-corpus differential oracle (warm session == cold `verify()` on diagnostics, summary, and obligation stream, plus warm-twice determinism, across all 43 examples and every verify/run-level conformance program), summary↔obligation tier-bookkeeping consistency (including the #967 `total == tier1_verified + tier3_runtime` leg, plus a focused self-consistency pin on the three call-demotion examples), the #1242 stream partition — over a corpus widened to every conformance program that type-checks, at any level, `len(obligations) == total + violated + tier3_unguarded` and every status is one of the documented five, with the vocabulary read from the `ObligationStatus` Literal so a sixth member fails rather than vanishing from the counts — per-kind unit tests (requires / ensures / decreases / nat_sub / call_pre statuses, counterexamples, error codes), content-key stability + same-text-two-sites span disambiguation, session solver reuse, type-error short-circuit, ADT-registry resync between programs; plus the Phase B incremental suite — identical-source full replay, callee-body-edit replays callers while callee-contract-edit invalidates them, span-shift and ADT-edit conservative invalidation, cross-program isolation, timeout-status never cached (monkeypatched solver), FIFO eviction bound; plus the #727 dedup pin — a violating call in a let RHS records exactly one E501 diagnostic and one call_pre obligation; plus the #1208 call-site rendering pin — a PARAMETERISED callee slot substitutes into the E501 message and its fix instead of falling back to the generic wording | | `test_verifier_contracts.py` | 96 | 903 | Z3 verification over the example corpus, trivial/ensures/if-else/let/multi-clause contracts, counterexamples, tier classification, arithmetic, verification summaries, Diverge effect, edge cases, string-length + string-predicate verification (#839 split) | | `test_verifier_nat_obligations.py` | 82 | 1,743 | **`@Nat` subtraction underflow obligation** (#520 — Path-A discharge via requires/path-conditions/path-aware Z3 refutation, pure-literal exclusion, Int-Int and Nat-Int exemptions) and **`@Nat` binding-site narrowing obligation** (#552/#747/#749 — Tier-1 `value >= 0` at let/call-arg/effect-op-arg/ctor-field/match-bind/destructure narrowing — a concrete site classifies `tier3_runtime` (codegen-guarded), as do the built-in effect-operation argument and the generic-instantiated constructor field since #754 and #757 closed them; only a USER-declared effect's operation argument classifies `E504` (obligated but unguarded), and its enclosing function is dropped with `E603` so no run reaches it — the rationale names its actual cause — an untranslatable value — rather than the untranslatable-or-timeout conflation #1251 removed, walker-recursion pins, `_narrows_into_nat` verifier/codegen soundness parity; PR #972 clone-instantiated side-table substitution — a `Some(@T)` bind in an `Option`-instantiated clone is no narrowing, genuine clone-path narrowings still obligated); #1201 — a builtin `Tuple` parameter's match-bound components carry their declared component facts (a valid ensures over one proves instead of falsely violating) and an `Int` component bound as `@Nat` fires one loud `E503` per component, both mutation-caught (#839 split) | | `test_verifier_primitive_ops.py` | 39 | 662 | **Primitive-operation safety obligations** (#680) — division/modulo by-zero `E526` and array-index-bounds `E527`, the in-bounds/out-of-bounds two-check with float-exemption, honest Tier-3 for opaque lengths, off-by-one and lower-bound pins, De Bruijn-correct fix hints (#839 split) | @@ -133,7 +133,7 @@ python scripts/check_wheel_availability.py # pre-flight: every runtime | `test_soundness_392.py` | 36 | 584 | #392 audit batches 1–2 — verifier soundness/completeness fixes: signed div/mod truncate toward zero (#799), body `assert(P)` carries a Tier-1 obligation (#800), divisions in contract predicates carry a `div_zero` obligation (#801), and the #804 assume-half of #800's `assert` rule — a prior `assert`/`assume` discharges later obligations (including a later call's precondition) + the postcondition at Tier 1, removing false E501/E503/E500/E505 | | `test_int_overflow.py` | 6 | 143 | #798 — `@Int`/`@Nat` arithmetic-overflow obligations (part of the #392 `smt.py` soundness audit): `+`/`-`/`*` on `@Int`/`@Nat` now emit an `int_overflow` obligation (the analog of `nat_sub`/`div_zero`) rather than modelling the operands as Z3's unbounded integers, so a `ensures(@Int.result > @Int.0)` over `@Int.0 + 1` no longer proves a contract the i64/u64 runtime violates under two's-complement wraparound. Unbounded operands leave the obligation undischarged (Tier-3, runtime-guarded); operand bounds that prove the result stays in range discharge it at Tier 1 | | `test_int_overflow_codegen.py` | 62 | 718 | #798 Stage 3 — runtime overflow-trap codegen: the codegen emits a guard at *exactly* the `@Int`/`@Nat` `+`/`-`/`*` sites the verifier obligates, so `vera run`/`vera compile` programs trap on overflow instead of silently wrapping at the i64/u64 boundary. #808 wired the guard to the `vera.overflow_trap` host import, so the trap now classifies `kind="overflow"` (carrying the overflow Fix paragraph) rather than the generic `unreachable`; `TestOverflowTrapKind808` pins that, with controls proving the #520 `nat_sub` underflow and #813 `@Nat`→`@Int` widen guards still classify `unreachable` | -| `test_int_overflow_differential.py` | 259 | 398 | #798 Stage 3 verifier↔codegen classification differential (cross-component soundness rule): the codegen overflow guard must fire at exactly the sites the verifier obligates *and* classify each site's operand type (`@Int` i64 vs `@Nat` u64) identically — else a Tier-1-clean program traps spuriously or a wrapping op slips through unguarded. Over a corpus exercising all five operand combos plus the literal-left ambiguity (a naive codegen mis-classifies it as `@Nat`), asserts the verifier's per-site gated classification equals the codegen's site for site, both sides driven by the same `ast.span_key` | +| `test_int_overflow_differential.py` | 260 | 398 | #798 Stage 3 verifier↔codegen classification differential (cross-component soundness rule): the codegen overflow guard must fire at exactly the sites the verifier obligates *and* classify each site's operand type (`@Int` i64 vs `@Nat` u64) identically — else a Tier-1-clean program traps spuriously or a wrapping op slips through unguarded. Over a corpus exercising all five operand combos plus the literal-left ambiguity (a naive codegen mis-classifies it as `@Nat`), asserts the verifier's per-site gated classification equals the codegen's site for site, both sides driven by the same `ast.span_key` | | `test_nightly_stress_workflow.py` | 5 | 318 | #1328 — the nightly stress workflow's `-m stress` selection must collect every `stress`-marked test repo-wide, not just whichever file its invocation names. Extracts the live `.github/workflows/nightly-stress.yml` "Run stress tests" `run:` command (not a hand-copied belief about it) and replays the argv VERBATIM (`shlex.split`, verbosity flags stripped) in `--collect-only` mode — not a marker+paths reconstruction, which would silently drop any other flag (`--ignore`, `--deselect`, `-k`) and let the same defect back in a differently-shaped command. Asserts the marker is literally `stress`, that the command's argv is not the exact `-m stress tests/test_stress.py` regression shape, that verbatim replay collects the same node IDs as the canonical `-m stress` selection over pyproject's own `testpaths`, and — the issue's own repro — that all 10 `TestHostHandleReclamation573` instances are among them. Module-scoped fixtures share the two collect-only subprocess calls across all four class-level cells. A standalone pure-unit test pins `_workflow_collect_argv` preserving a non-verbosity flag verbatim — mutation-validated: reintroducing the old marker+paths reconstruction leaves all four class-level cells green (none of them exercises a flag the reconstruction would not know about) and only this cell catches it | | `test_nat_int_widening.py` | 36 | 622 | #813 — `@Nat -> @Int` widening coercion obligation (dual of #552 `nat_bind`, part of the #392 soundness audit): a `@Nat` in (i64.MAX, u64.MAX] reinterprets when widened (u64.MAX → -1), so a `nat_to_int_coerce` obligation that the value is `<= i64.MAX` now fires at the return position — provably-in-range → Tier-1, provably-out-of-range (`@Nat.0 >= 2**63`) → loud E530, unbounded → honest Tier-3 (runtime-guarded), with an `@Int -> @Int` control that must not fire; the unguarded generic-`@Int`-field case also has its `E531` rationale read for WHAT IT SAYS — a value bounded on neither side, not the untranslatable-or-timeout conflation #1251 removed. The #813 follow-up adds the explicit `nat_to_int` built-in and heterogeneous `if`/`match` arms with a non-negative-literal alternative; #820 adds the heterogeneous-`@Int`-slot arm, closure argument, and closure return/capture obligations (each per-arm / per-site, with `@Int`-arm and `@Nat`-formal controls that must not fire) | | `test_int_widening_codegen.py` | 52 | 535 | #813 Stage 3 — runtime `@Nat -> @Int` widening-trap codegen: the codegen emits a guard at *exactly* the `@Nat -> @Int` coercion sites the verifier obligates (return, `let`, call argument, and — since #820 — array element, tuple construction/destructure, heterogeneous `if`/`match` arm, closure argument/return), so `vera run`/`vera compile` programs trap when a `@Nat` above i64.MAX would reinterpret to a negative `@Int` instead of silently returning the wrong value. The trap is a bare `unreachable` (shares `_emit_negative_i64_guard` with the #552 nat-bind guard), classified `kind="unreachable"` today (a dedicated widening trap kind is a follow-up) | @@ -167,7 +167,7 @@ python scripts/check_wheel_availability.py # pre-flight: every runtime | `test_imported_trap_source_map_1189.py` | 8 | 342 | An imported function's runtime trap frame names ITS module's file (#1189), the source-map sibling of #1186's diagnostic fix. Fixtures split the basenames (`chinchilla.vera` module, `stargazer.vera` importer) so a frame's attribution is decidable from the string alone, and every trap is a precondition violation so `WasmTrapError.kind` is pinned. Covers the three doors: an imported non-generic fn (pre-fix `` — never registered on the main generator), a monomorphized clone of an imported generic (pre-fix the IMPORTER's path with the module's line range, which in the fixture names a real-but-unrelated importer function), and the `mod$…` emission of a locally-shadowed import (whose rightmost-`$` strip yields nobody's entry). Asserted at the `cmd_run` text backtrace (per-frame line, never the whole stderr blob — `main` legitimately names the importer), the `--json` frames array, `fn_source_map` itself, and `execute()`'s `WasmTrapError.frames`. Over-correction control: a wholly main-file trap keeps the main file, green before and after. Mutations — the module file on the Pass-0.5 registrar, the bare-name harvest, the mangled-name mirror, the Pass-1.5 module source scope — each killed by a distinct named test | | `test_codegen_typeparam_unit_wildcard_1060.py` | 31 | 959 | Wildcard over a type-parameter field instantiated to `Unit` (#1060), the type-parameter sibling of #1043's declared-`Unit` field: a WILDCARD over `Box` field `T` used to advance the match offset walk by the generic `i32` width, so on `Box` (field erased to 0 bytes) every later field read four bytes high — silently check-green. Bug-manifesting shapes go end-to-end (`Box` trailing-`Int`, `Named` `String` read-back, `Entry` nested-ctor tag, `Bool`-following, second-type-parameter, and a nested-generic `Outer` wrapping `Inner` that exercises the deeper-recursion type substitution); controls stay green (before-erased field, trailing wildcards, `Option`/`Result` builtins, `Box`/`Box`/`Tagged` alignment-coincidence, structural `Eq`/`show` recompute path); the direct-call boundary is pinned (#1065) — a `match mk() { … }` scrutinee recovers its concrete instantiation from the callee's declared return type, so a wildcard followed by a read now compiles and reads the real value (`Box` trailing-`Int`, `Entry` nested-ctor, `Named` `String` read-back) instead of the sound #1060 interim LOUD-skip, while a trailing direct-call wildcard still compiles; the generic-call sibling (#1072) resolves the declared return's type variables from the call site (`P2` at T=Int, the var-typed field at `String` i32_pair width, a fully concrete parameterized return on a generic fn, nested-ctor and `String`-read-back variants, plus a trailing-wildcard control), and the module-call door (#1073) routes `boxlib::mk()` — and the imported-generic #1072 x #1073 compound — through the shared resolver into the same recovery; mutation-validated per arm (reverting the #1060 instantiation-awareness flips exactly the #1060 bug-manifesting shapes RED with declared-`Unit` #1043 tests green; reverting the #1065 declared-return threading flips exactly the three direct-call value shapes RED; neutralizing the #1072 generic arm flips exactly the five generic value shapes + the imported-generic compound RED; neutralizing the #1073 module arm flips exactly the two module tests RED) | | `test_codegen_alias_adt_name_width_1309.py` | 112 | 423 | A `type` alias whose name is also a registered ADT's must emit the ALIAS TARGET's width (#1309). Codegen's `_type_expr_to_wasm_type` tested `_adt_layouts` — and `Array`/`Map`/`Set`/`Decimal`, none of them primitives — before the alias table, where the checker's `_resolve_named` resolves primitive, then alias, then declared ADT; so `type Option = Int;` emitted the ADT's i32 pointer for an i64 slot on a check-green, verify-green program. Three dispositions are pinned separately because they fail differently: LOUD scalar targets (`Int`/`Nat` i64, `Float64` f64) died at load; PAIR targets are the SILENT ones the issue's "matching widths" prediction missed — an `i32_pair` is two words and the single i32 dropped the length, so `string_concat("ab", "ab")` returned junk bytes and `array_length` over three elements returned 0, both at exit 0; and matching-width targets (`Bool`/`Byte`/`Map`/`Set`/`Decimal`, all i32) are INERT, kept as green-both-sides guards that the reorder leaves them alone. The battery is the differential that makes width-luck unreintroducible: every name in the LIVE built-in ADT registry (read off a real `CodeGenerator`, so a new built-in joins without anyone widening a list) crossed with every representation class, comparing the emitted `twice` body in full — header widths and the instructions under them — against the identical program under a fresh alias name, plus the two unit duals — under an alias the derivation answers the target's width, without one it still answers the ADT pointer, so "the alias wins" cannot be satisfied by breaking every ordinary ADT parameter. Primitives are asserted to still shadow a same-named alias — the one branch that must NOT move — across all seven spellings by asking the derivation directly, which is the only way to reach every one of them since two are checker-refused (`@Bool.0 + @Bool.0` is E140, `type Int = Int;` is E132); a run-level program carries the behavioural half, because `type Bool = Int;` used AS a Bool is check-green, runs, and distinguishes the hoist mutant. An earlier draft claimed the checker refuses every program that would exercise this, which is measured false. A separate block covers the THIRD consumer of the same disease (CR on PR #1323): `_return_type_is_string` tested the `Future` transparency strip before the alias table, so under `type Future = Array;` a `@Future` return was classified a string and `execute()` decoded the array's backing bytes as UTF-8 — two NULs where the fresh-name control printed the pointer, measured identically at the branch point and so pre-existing. `String` stays ahead of the alias branch there too, being the one primitive involved, and three over-correction controls hold the #841/#1047 transparent-`Future` decode and PR #1041's alias-to-`Future` shape. `Json` and `HtmlNode` are deliberately outside the prelude-ADT row: their prelude combinator bodies render against the flat alias map a main-file shadow pollutes, which is an alias-env SCOPING defect (#1316) the reorder does not reach — though it does MOVE that failure (17 prelude `json_*` signatures flip width, the loader's complaint reverses direction, `html_attr` loses a push), so "fails identically" — an earlier draft's wording — is measured false | -| `test_name_resolution_spine_1316.py` | 212 | 1282 | #1316 / #1321 / #1331 — ONE name-resolution spine, asked in the DECLARING namespace. The branch ORDER now lives once, in `vera.naming.classify_named`, and the prelude is a namespace like any other (`PRELUDE_NAMESPACE`). **Spine precedence** is pinned on an env where ONE name is simultaneously a type parameter, a primitive, an alias and a declared ADT, so no assertion can pass by the name being absent from a losing table, plus the declaration-index bound on BOTH registries and the arity-mismatch sort; and `resolve_type_expr` is asserted to take the branch the spine names for every sort, so the semantic arm cannot drift into a second opinion only codegen reads. **#1321 / #1331** runs every built-in ADT and container name from the LIVE registry (read off a real `CodeGenerator`, so a new built-in joins without anyone widening a list) as a user `data` declaration, asserting the run value, an EMPTY diagnostic list with both exports present, and a byte-identical `wat_fn_body` differential against a fresh-name control — the run assertion alone accepts a body that reaches 7 through a different representation. **#1316** aliases every one of those names, including the `Json` and `HtmlNode` the #1309 battery had to exclude, and adds the two halves a behaviour test cannot reach: the POSITIONAL assertion that every prelude declaration compiles with `PRELUDE_NAMESPACE` installed and every user declaration with the entry's, and the REGISTRY assertion that `_fn_sigs['json_get']` records the prelude's own i32 rather than the entry file's `type Json = Int;` width — masked today by the Pass-2 derivation, so a falsehood waiting for its first consumer. An entry `data Array` beside a `json_parse` call is the membership half end to end: the prelude's own `Array` parameters must stay a (ptr, len) pair, which only a program that declares the name AND demands the prelude family can tell. **The cross-derivation differential** is what keeps the family closed — each of five derivations must answer for a shadowed name exactly what it answers for a fresh one — because #1331 survived a fix to two of the four width sites precisely because nothing compared them. One of the five (`_ref_type_name_wasm_type`'s branch) is inert TODAY by width-luck, measured and stated as such, and pinned STRUCTURALLY rather than by a behaviour test that cannot fail. **#1397** partitions that live name set in two, reading the reserved half off the checker's own `_SPECIAL_CASED_BUILTIN_ADTS` rather than restating it: `Future` and `Tuple` are refused as a `data` name (E158) at the entry file and inside a module alike, while every other name runs the battery above with NO skips — the `Tuple` show/eq cells that were excused with a measured wrong output are refusals now — and a cell asserts the two halves are disjoint and cover the whole set, so a new special-cased built-in nobody reserves fails the battery instead of going unmeasured. The built-in carrier is pinned beside the refusal (`show(Tuple(1, 2))` renders `(1, 2)`, a match sums to 7, `hash` agrees, and `==` is still the documented `[E243]`) | +| `test_name_resolution_spine_1316.py` | 253 | 2098 | #1316 / #1321 / #1331 — ONE name-resolution spine, asked in the DECLARING namespace. The branch ORDER now lives once, in `vera.naming.classify_named`, and the prelude is a namespace like any other (`PRELUDE_NAMESPACE`). **Spine precedence** is pinned on an env where ONE name is simultaneously a type parameter, a primitive, an alias and a declared ADT, so no assertion can pass by the name being absent from a losing table, plus the declaration-index bound on BOTH registries and the arity-mismatch sort; and `resolve_type_expr` is asserted to take the branch the spine names for every sort, so the semantic arm cannot drift into a second opinion only codegen reads. **#1321 / #1331** runs every built-in ADT and container name from the LIVE registry (read off a real `CodeGenerator`, so a new built-in joins without anyone widening a list) as a user `data` declaration, asserting the run value, an EMPTY diagnostic list with both exports present, and a byte-identical `wat_fn_body` differential against a fresh-name control — the run assertion alone accepts a body that reaches 7 through a different representation. **#1316** aliases every one of those names, including the `Json` and `HtmlNode` the #1309 battery had to exclude, and adds the two halves a behaviour test cannot reach: the POSITIONAL assertion that every prelude declaration compiles with `PRELUDE_NAMESPACE` installed and every user declaration with the entry's, and the REGISTRY assertion that `_fn_sigs['json_get']` records the prelude's own i32 rather than the entry file's `type Json = Int;` width — masked today by the Pass-2 derivation, so a falsehood waiting for its first consumer. An entry `data Array` beside a `json_parse` call is the membership half end to end: the prelude's own `Array` parameters must stay a (ptr, len) pair, which only a program that declares the name AND demands the prelude family can tell. **The cross-derivation differential** is what keeps the family closed — each of five derivations must answer for a shadowed name exactly what it answers for a fresh one — because #1331 survived a fix to two of the four width sites precisely because nothing compared them. One of the five (`_ref_type_name_wasm_type`'s branch) is inert TODAY by width-luck, measured and stated as such, and pinned STRUCTURALLY rather than by a behaviour test that cannot fail. **#1397** partitions that live name set in two, reading the reserved half off the checker's own `_SPECIAL_CASED_BUILTIN_ADTS` rather than restating it: `Future` and `Tuple` are refused as a `data` name (E158) at the entry file and inside a module alike, while every other name runs the battery above with NO skips — the `Tuple` show/eq cells that were excused with a measured wrong output are refusals now — and a cell asserts the two halves are disjoint and cover the whole set, so a new special-cased built-in nobody reserves fails the battery instead of going unmeasured. The built-in carrier is pinned beside the refusal (`show(Tuple(1, 2))` renders `(1, 2)`, a match sums to 7, `hash` agrees, and `==` is still the documented `[E243]`) | | `test_data_namespace_contention_1312.py` | 22 | 805 | #1312 / #1317 — the data-collision rails, asked about LAYOUTS and about OWNERS. Three PAIRS can meet in codegen's one layout slot, and all three decide compatibility through the same `data_decl_shape` derivation — asserted structurally, since a second copy of "can one layout serve both" is a second thing to keep in step. **#1312** pins the new **E623**: the shape where the module's own bodies drop (`exports == ['consume']`, `main` silently gone) and the ISSUE'S OWN repro, which is green at the base because the module never touches its `Json` — the rail keys on the DECLARATIONS, not on the E602 wreckage they happen to produce. Location, severity, source line, the module's file and line in the description, and the diagnostic's rationale/fix/spec_ref are pinned, beside the two relaxations that must survive it: an entry file RESTATING a module's public type compiles and runs, and an entry `data` no module shares is untouched. **#1317** pins the restatement diamond compiling and running, E610 relaxed in LOCKSTEP (relaxing E609 alone would refuse exactly the programs it just admitted), and a restatement spelled through the module's OWN alias — which is what makes the alias-map capture's position load-bearing, since captured after the ADT harvest the module's maps are still empty when its declaration is compared. `TestDifferingShapesAdmittedWhenNothingMeetsThem` and `TestMeetingStillRefused` hold the two sides of per-owner identity's boundary: a narrowed import, a private declaration and a local shadow each leave the two declarations unreachable from one another, so each compiles and runs under `mod$$` (the local-shadow cell leaves E623 no pair to report), while a value that can still cross between two owners stays E609 | | `test_per_owner_adt_identity_1317.py` | 55 | 1994 | #1317 / #187 (data half) — ADT identity is `(owner, name)` by construction. A CONTENDED module `data` declaration and its constructors are renamed to `mod$$` at absorb time, inside every namespace that can name them, so the ~187 name-keyed ADT consumers are correct without knowing the rule exists — the #1029 device applied to the data namespace. `TestTheThreeRemedies` drives #1317's own three measurements (a selective import excluding the type, a local declaration in the importer, a merely `private` namesake) through to the runtime value, since "no longer refused" and "right answer" are different claims. `TestOneSymbolPerOwnerEverywhere` is the differential that keeps the by-construction claim honest: it sweeps EVERY dict the generator carries for a bare name a rename left behind, rather than the registries this change happened to think about, and its docstring records what each of five mutations actually reached. `TestMeeting` is the guard the nameability argument alone does not give — two same-named cross-module ADTs unify, so a value crosses between them through an imported signature (directly, through an imported ADT's field, or spelled through the exporting module's own alias) even under filters that exclude the type, and each of those measured `100` where `7` is the answer before the condition existed. `TestThePreludeIsReserved` pins maintainer ruling R7 (a module `data` named after a prelude ADT stays E621's) against a control that renames the same two declarations to a user name and runs them | | `test_codegen_pair_scrutinee_1305.py` | 32 | 719 | A `match` whose SCRUTINEE is pair-represented (`String` / `Array`) took one local at the internal `i32_pair` pseudo-type, so the module carried `(local $l1 i32_pair)` and never assembled (#1305). The issue reached it through `json_keys` and framed it as an `Option>` payload binder; the docstring records why measurement does not support that — `json_keys` returns `Array`, and `array_length(json_keys(j))` compiled and ran at the branch point — so the tests are built on the shapes that actually trigger it: `match @String.0 { @String -> … }` and `match @Array.0 { @Array -> … }`, both legal and check-green, plus the slot, call-result and builtin-result scrutinee forms. One test returns the BOUND STRING rather than its length, because a fix that allocated two locals and copied only the pointer passes every length-free assertion. The issue's own repro matches `Some`/`None` against that array; a pair carries no tag, so the assertion is that the module assembles and the refusal is a located E602 — not that the nonsense compiles (the checker accepting it is #1315). The guard is a WHITELIST (wildcard and binding only) and these cells are why: as a blacklist naming the two constructor kinds it let `true ->` and `1 ->` fall through into the arm-condition emitter, turning a loud WAT failure into a check-green program that exits 0 printing 100 from the scrutinee's heap POINTER read as a truth value, and its integer twin into a shipped `.wasm` that died at instantiation with no diagnostic — so five unlowerable-arm cells (bool/int/string literals over both pair spellings) and a nullary-arm-FIRST program pin each half, the last because both original repros led with `Some` and left the nullary half droppable green. The two shadow pushes are pinned as EMISSION by a WAT differential against the match-free twin (exactly two more push idioms) plus a position assertion that no length half is rooted: deleting both pushes leaves the whole suite, the GC rooting and reclamation suites, and four allocate-in-the-arm probes under `VERA_EAGER_GC=1` green, so a behavioural claim would be one no probe supports. The two controls the issue listed as already-compiling are kept as regression guards, and an Option/Result binder battery over `Array`/`Array`/`Array`/`Map`/`Set`/`String`/`Int` payloads plus a nested `Option>>` pins the boundary: the scrutinee change left pair-typed constructor FIELDS alone | @@ -218,7 +218,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` | 66 | 705 | 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 `docs/index.md` (#829; `AGENTS.md`'s ellipsis-truncated description/rationale are prefix-compared, its `error_code`/`spec_ref`/`fix` exactly). #954 single-sources the first four: `render_e001_doc_example()` / `render_e001_doc_example_html()` (`vera/errors.py`) render the one canonical `e001_doc_example()` `Diagnostic`, `scripts/build_site.py` calls the renderer directly so `docs/index.md`'s copy is generated rather than hand-copied (structurally cannot drift — proven by changing the canonical fix text and confirming it flows through `build_site.py`'s regeneration with no other file touched), and `README.md`/`spec/00-introduction.md`/`docs/index.html` add a byte-equality test against the same renderer alongside the existing field-by-field checks. `AGENTS.md` stays hand-written and truncated by design, guarded only by the field-by-field checks | | `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` | 549 | 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` | 551 | 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) | @@ -236,7 +236,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` | 425 | 5,270 | 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; plus the #1301 `md_parse` ADT differential (`TestMdParseCrossHostAdtDifferential1301`), which runs a generated corpus — the classes #1301 measured, every block-opening line template one, two and three at a time, every inline shape in the four positions that reach the inline parser, a carriage-return leg and a seeded fuzz leg — through BOTH parsers and compares the resulting trees byte for byte, since a comparison routed through `md_render` cannot see how a paragraph's plain-text runs are grouped, beside `TestMdGrammarSharedTable1301`, which asserts the browser runtime carries `vera/markdown_grammar.py`'s generated pattern table verbatim | -| `test_conformance.py` | 1,255 | 154 | Parametrized conformance suite: parse, check, verify, run, format idempotency across 251 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` | 1,265 | 154 | Parametrized conformance suite: parse, check, verify, run, format idempotency across 251 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 | @@ -261,11 +261,11 @@ python scripts/check_wheel_availability.py # pre-flight: every runtime | `test_doc_builtin_shadowing.py` | 11 | 183 | `check_doc_builtin_shadowing.py` gate ([#819](https://github.com/aallan/vera/issues/819)): reject-set membership (opaque built-ins in, overridable combinators out), top-level + `where`-block `fn ` definitions flagged, non-built-in / overridable / prose-mention ignored, and the shipped docs are currently clean | | `test_runtime_traps.py` | 98 | 3,256 | Runtime trap categorisation (#516 Stage 1), out-of-bounds host-read bounds check (#1145), stdout/stderr-on-trap preservation (#522), `IO.print` live tee (#543), and trap source backtrace (#516 Stage 2): `_classify_trap` per-`kind` mapping (`divide_by_zero`/`out_of_bounds`/`stack_exhausted`/`unreachable`/`overflow`/`contract_violation`/`unknown`), plus `host_error` from `_classify_host_error` on `execute()`'s non-`Trap` branch, `WasmTrapError` shape + `RuntimeError` substitutability, end-to-end `cmd_run` text + JSON envelopes including `trap_kind`, captured `stdout`, captured `stderr`, JSON-mode "no stderr leak" invariant, cross-stream code-order regression using merged `redirect_stdout`/`redirect_stderr`, the v0.0.123 tee suite (live streaming, write-count + order preservation, JSON-mode tee suppression, trap preservation invariant under tee, per-write flush count, default-execute silence), and the v0.0.124 source-mapping suite — `_resolve_trap_frames` unit tests covering user-fn / built-in / built-in-prefix / monomorphized base-name fallback / unknown-name / no-frames-attribute / leaf-first ordering preservation; end-to-end `cmd_run` text-mode + JSON-mode backtrace including the **leaf-first** ordering invariant; contract-violation backtrace in both text and JSON modes; direct `execute()` `WasmTrapError.frames` attachment; **suppression marker** for collapsed leading runtime-helper frames (mocked `vera.codegen.execute` with synthetic `is_builtin=True` leaf frames so the collapse logic is testable deterministically); source-map population for top-level fns + lifted closures (with span-value assertion against the closure literal's exact line range); and the no-builtin-leakage regression that pins built-in helpers (`alloc` / `gc_collect` / `contract_fail`) NOT being registered in `fn_source_map`; plus the v0.0.125 Stage 3 suite (`#547`) — text-mode `Fix:` block surfacing with position-ordering invariant (Fix appears after the source backtrace), text-mode block suppression for `contract_violation` (no empty header noise), JSON-mode `fix` field always-present (schema stability) including the empty-string case, `_TRAP_FIX_PARAGRAPHS` table-completeness assertion (every kind in the taxonomy has a Fix paragraph entry), and the column-wrap invariant (~76 chars max per line, two-space indent under the `Fix:` heading); plus the UTF-8 hardening suite **`TestHostPrintInvalidUtf8589`** (`#589` / `#592`) — after `#592` centralised the `errors="replace"` invariant into the single `vera.runtime.text.safe_utf8_decode` helper — reached only through a shared `_slice_and_decode` helper (`vera/runtime/heap.py`) that the three WASM-memory string readers (`_read_wasm_string` and `_read_string_export` there, and `vera/wasm/markdown.py::_read_string`) delegate to, with the `host_print` / `host_stderr` / `host_contract_fail` host imports and the String-return extractor in `execute()` routing through those readers rather than decoding inline: one helper unit test pinning the invariant once (invalid bytes → U+FFFD, valid + empty pass through), three wire-real end-to-end tests that drive the **production** readers (`_read_wasm_string` / markdown `_read_string` behind a synthetic-WAT `probe` host import; `_read_string_export` against a real exported memory, also covering its out-of-bounds → `None` pointer-fallback) over a region seeded with invalid UTF-8 — so a strict-decode regression surfaces as a `UnicodeDecodeError` escaping wasmtime's trampoline, and the host imports / extractor are transitively covered — and one synthetic-WAT end-to-end test that imports `vera.print` and calls it with raw invalid UTF-8 bytes to pin the wasmtime-trampoline fact independently (a Python `UnicodeDecodeError` inside a host import escapes as a "python exception" cause iff the host decode is strict); the six pre-`#592` structural source-grep assertions were retired by the centralisation; plus the Ctrl-C-during-host-import suite **`TestHostSleepKeyboardInterrupt`** ([#595](https://github.com/aallan/vera/issues/595) / [#599](https://github.com/aallan/vera/issues/599)) — after the v0.0.160 relocation to a single `except KeyboardInterrupt` handler in `execute()` (enabled by `wasmtime>=45.0.0`'s `except BaseException` trampoline fix): one structural assertion that the four per-host-import `raise _VeraExit(130)` guards are gone and the centralized handler maps to `exit_code=130`, plus four end-to-end tests that compile real Vera programs calling `IO.sleep(...)`, `IO.read_char(())`, a mocked fused `await` ([#841](https://github.com/aallan/vera/issues/841) — `Future.result()` patched to interrupt), and a live in-flight fused `await` (no mocking — `_thread.interrupt_main()` fired only once the server confirms the request arrived, handler then released so the executor teardown has a real worker to wait out; post-[#848](https://github.com/aallan/vera/issues/848) the progress print precedes the `async(...)`, so program order makes its stdout assertion deterministic), raise `KeyboardInterrupt` from inside the blocking call, and assert the program exits with `ExecuteResult.exit_code == 130` (pre-interrupt stdout preserved) instead of a raw Python traceback escaping wasmtime's trampoline; plus the host-callback surface suite **`TestHostCallbackErrorSurface1302`** / **`TestClassifyHostError1302`** ([#1302](https://github.com/aallan/vera/issues/1302)) — `execute()` classified on the exception's TYPE NAME (`Trap` / `WasmtimeError`), so a host import raising an ordinary Python exception skipped the conversion and escaped as a 63-line interpreter traceback with the captured streams dropped, and in `--json` mode with no envelope emitted at all. The conversion is now keyed on the BOUNDARY (everything escaping the guest invocation), and the suite drives a real `json_stringify(JNumber(nan()))` program through all three surfaces: `execute()` raising a `WasmTrapError` of `kind="host_error"` carrying the host's sentence, the pre-failure stdout and the original exception as `__cause__`; text-mode `cmd_run` asserted on the ABSENCE of `Traceback` / `File "` / `wasmtime` and a sub-ten-line diagnostic, since asserting only that the sentence appears would still pass on the pre-fix output where it was the traceback's last line; and JSON-mode `cmd_run` producing a parseable envelope with `trap_kind`, an always-present empty `fix`, `frames`, and the captured `stdout`. **`TestHostErrorDebugKnob1302`** covers the escape hatch the conversion needs — `VERA_DEBUG_HOST_ERRORS` (ENVIRONMENT.md) re-raises the original exception so a binding bug stays diagnosable — as a deliberate pair, one test proving the knob does something and one proving its absence is what produces the one-liner, since neither alone distinguishes a working knob from unconditional behaviour, plus the truthiness table shared with `VERA_EAGER_GC` and an end-to-end `cmd_run` case | | `test_serve.py` | 8 | 189 | #305 `vera serve` driver end-to-end: GET/POST echo round-trips (method/path/headers/body cross the host↔guest boundary via `build_request_adt` / `decode_response_adt`), handler status propagation, runtime contract violation → 500 with `trap_kind` JSON, `State` isolation across requests (instance-per-request pinned), and clean `make_server` validation errors (missing / wrong-signature `handle`), and an eager-GC round-trip pinning the Request builder's shadow-rooting; all on ephemeral ports | -| `test_wasi_target.py` | 276 | 2,172 | #237 WASI Preview 2 target (spec chapter 13): component emission validated live against the real wasmtime host — parse (`Component(engine, wat)`), instantiate (`Linker.add_wasip2()` + `WasiConfig`), and execute (stdout/stderr capture, env, argv incl. a 500-arg GC-pressure stress and a >64 KiB arena-cap trap, preopen file round-trips + errno mapping, stdin incl. UTF-8 multibyte, clocks, random bounds, exit, contract-violation text on WASI stderr, overflow); the family gate (clean diagnostic naming unsupported families, never a silent fallback); the core-emission pin (default `--target wasm` WAT untouched); `cmd_compile`/`cmd_run --target wasi-p2` CLI integration (binary component artifact, `--wat` component text, JSON envelopes, trap-kind classification through the component boundary, exit-code 0/1 degradation, `--fn` rejection); the `execute_wasi_p2` host runner (env passthrough, argv, stderr capture, String-main `wasi:cli/run` fallback); the **dual-target conformance differential** (all 174 run-level conformance programs driven under both targets, byte-identical stdout/stderr required — 122 are dual-tested and 52 skip *loudly* rather than passing silently: 45 whose compiled WAT imports a host family outside `IO`/`Random` (`state`, `map`, `json`, `set`, `decimal`, `html`, `md`, `regex`, `db`), 6 with no public zero-argument `main`, and 1 calling a nondeterministic op. The excluded set is defined by those three properties rather than by a filename list, so it stays accurate as programs are added); a stock-`wasmtime`-CLI smoke test (skips when the CLI is not installed); and the Stage-D **server world** (`world="server"`): incoming-handler emission pins (adapter lift, 32-slot dispatch table, @0.2.0 version pin, no `wasi:cli/run`), #305 handler validation + server family-gate diagnostics (rejected IO ops, non-String map instantiations, unsupported families), the cli-world pin (default emission carries no server machinery), Request/Response layout tripwires, and a stock-`wasmtime serve` smoke battery (host-vs-served differential over a method/path/header/body matrix incl. duplicate-header later-wins, in-guest map-op order parity, `IO.print` console routing, trap→500 with symbolized backtrace + violation text, graceful 500s for forbidden headers and out-of-range status, a 1 MiB GC-stress echo, and an eager-GC shadow-push mutation validation; skips when the CLI is not installed) | +| `test_wasi_target.py` | 277 | 2,172 | #237 WASI Preview 2 target (spec chapter 13): component emission validated live against the real wasmtime host — parse (`Component(engine, wat)`), instantiate (`Linker.add_wasip2()` + `WasiConfig`), and execute (stdout/stderr capture, env, argv incl. a 500-arg GC-pressure stress and a >64 KiB arena-cap trap, preopen file round-trips + errno mapping, stdin incl. UTF-8 multibyte, clocks, random bounds, exit, contract-violation text on WASI stderr, overflow); the family gate (clean diagnostic naming unsupported families, never a silent fallback); the core-emission pin (default `--target wasm` WAT untouched); `cmd_compile`/`cmd_run --target wasi-p2` CLI integration (binary component artifact, `--wat` component text, JSON envelopes, trap-kind classification through the component boundary, exit-code 0/1 degradation, `--fn` rejection); the `execute_wasi_p2` host runner (env passthrough, argv, stderr capture, String-main `wasi:cli/run` fallback); the **dual-target conformance differential** (all 175 run-level conformance programs driven under both targets, byte-identical stdout/stderr required — 123 are dual-tested and 52 skip *loudly* rather than passing silently: 45 whose compiled WAT imports a host family outside `IO`/`Random` (`state`, `map`, `json`, `set`, `decimal`, `html`, `md`, `regex`, `db`), 6 with no public zero-argument `main`, and 1 calling a nondeterministic op. The excluded set is defined by those three properties rather than by a filename list, so it stays accurate as programs are added); a stock-`wasmtime`-CLI smoke test (skips when the CLI is not installed); and the Stage-D **server world** (`world="server"`): incoming-handler emission pins (adapter lift, 32-slot dispatch table, @0.2.0 version pin, no `wasi:cli/run`), #305 handler validation + server family-gate diagnostics (rejected IO ops, non-String map instantiations, unsupported families), the cli-world pin (default emission carries no server machinery), Request/Response layout tripwires, and a stock-`wasmtime serve` smoke battery (host-vs-served differential over a method/path/header/body matrix incl. duplicate-header later-wins, in-guest map-op order parity, `IO.print` console routing, trap→500 with symbolized backtrace + violation text, graceful 500s for forbidden headers and out-of-range status, a 1 MiB GC-stress echo, and an eager-GC shadow-push mutation validation; skips when the CLI is not installed) | ## Conformance Suite -The conformance suite is a collection of 251 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 253 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. @@ -290,11 +290,11 @@ 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 | 57 | +| `check` | Parses and type-checks cleanly | 58 | | `verify` | Type-checks and all contracts verified by Z3 | 20 | -| `run` | Compiles to WASM and executes correctly | 174 | +| `run` | Compiles to WASM and executes correctly | 175 | -Almost all programs are at the `run` level — they compile and execute, producing correct results. Fifty-seven programs (`ch02_generic_over_unit_rejected`, `ch02_map_unit_value_rejected`, `ch02_nonregular_data_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_builtin_adt_redefinition_rejected`, `ch08_builtin_tuple_redefinition_rejected`, `ch08_builtin_ctor_redefinition_rejected`, `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`, `ch04_pattern_ctor_over_container_rejected`, `ch04_pattern_literal_type_rejected`, `ch05_where_helper_sibling_call_rejected`) are at the `check` level. Forty-four of them — `ch02_generic_over_unit_rejected`, `ch02_map_unit_value_rejected`, `ch02_nonregular_data_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_builtin_adt_redefinition_rejected`, `ch08_builtin_tuple_redefinition_rejected`, `ch08_builtin_ctor_redefinition_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_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`, `ch02_alias_cycle_rejected`, `ch04_pattern_ctor_over_container_rejected`, `ch04_pattern_literal_type_rejected`, and `ch05_where_helper_sibling_call_rejected` — are **negative tests** that assert a specific diagnostic (E206, E135, E129, E183, E201, E127, E153, E153, E153, E153, E130, E130, E174, E182, E217, E156, E156, E155, E155, E011, E158, E158, E158, E154, E154, E154, E154, E154, E154, E150, E152, E151, E242, E243, E207, E208, E208, E209, E128, E336, E132, E314, E314, and E178 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-eight programs (`ch02_generic_over_unit_rejected`, `ch02_map_unit_value_rejected`, `ch02_nonregular_data_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_builtin_adt_redefinition_rejected`, `ch08_builtin_tuple_redefinition_rejected`, `ch08_builtin_ctor_redefinition_rejected`, `ch08_sibling_ctor_collision_rejected`, `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`, `ch04_pattern_ctor_over_container_rejected`, `ch04_pattern_literal_type_rejected`, `ch05_where_helper_sibling_call_rejected`) are at the `check` level. Forty-five of them — `ch02_generic_over_unit_rejected`, `ch02_map_unit_value_rejected`, `ch02_nonregular_data_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_builtin_adt_redefinition_rejected`, `ch08_builtin_tuple_redefinition_rejected`, `ch08_builtin_ctor_redefinition_rejected`, `ch08_sibling_ctor_collision_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_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`, `ch02_alias_cycle_rejected`, `ch04_pattern_ctor_over_container_rejected`, `ch04_pattern_literal_type_rejected`, and `ch05_where_helper_sibling_call_rejected` — are **negative tests** that assert a specific diagnostic (E206, E135, E129, E183, E201, E127, E153, E153, E153, E153, E130, E130, E174, E182, E217, E156, E156, E155, E155, E011, E158, E158, E158, E159, E154, E154, E154, E154, E154, E154, E150, E152, E151, E242, E243, E207, E208, E208, E209, E128, E336, E132, E314, E314, and E178 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 @@ -446,7 +446,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 -├── ... # 251 programs total, organized by spec chapter +├── ... # 253 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 @@ -1064,9 +1064,9 @@ Twenty-nine scripts in `scripts/` validate cross-cutting concerns beyond unit te | Script | What it validates | |--------|-------------------| -| `check_conformance.py` | All 251 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 253 conformance entries hold at their declared level (parse/check/verify/run) — positives pass; the negatives fail at the stage their `expected_error_stage` names (`check` by default, or `compile`, which also asserts the program type-checks cleanly) with their `expected_error` E-code | | `check_examples.py` | All 43 `.vera` examples pass `vera check` + `vera verify` | -| `check_corpus_canonical.py` | All 301 corpus programs (recursive over `examples/` + `tests/conformance/`) are in canonical form under `vera fmt` | +| `check_corpus_canonical.py` | All 303 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 | @@ -1187,9 +1187,9 @@ The repository configures 39 hooks across two stages: 37 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 251 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 253 conformance entries hold at their declared level — positives pass; negatives fail at the stage their `expected_error_stage` names (`check` or `compile`) with their `expected_error` E-code | | `check_examples.py` | All 43 examples pass `vera check` + `vera verify` | -| `check_corpus_canonical.py` | All 301 `examples/` + `tests/conformance/` programs (recursive) are in canonical form (`vera fmt`) | +| `check_corpus_canonical.py` | All 303 `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 378b2119c..8a37abfc6 100644 --- a/docs/SKILL.md +++ b/docs/SKILL.md @@ -493,7 +493,7 @@ match @Tuple.0 { } ``` -`Tuple` is just an upper-case constructor — there is no special tuple-literal syntax (no `(1, 2, 3)` form). The empty tuple `Tuple<>` is equivalent to `Unit`. The name is reserved in the data namespace: `data Tuple { ... }` is rejected at `vera check` with **E158** (see below), because the compiler recognises `Tuple` by name when it renders and lays out a value. A `type Tuple = ...` alias is unaffected. +`Tuple` is just an upper-case constructor — there is no special tuple-literal syntax (no `(1, 2, 3)` form). The empty tuple `Tuple<>` is equivalent to `Unit`. The name is reserved in both the data and the constructor namespace: `data Tuple { ... }` and `data Box { Tuple(Bool) }` are each rejected at `vera check` with **E158** (see below), because the compiler recognises `Tuple` by name when it renders and lays out a value. A `type Tuple = ...` alias is unaffected. ### Type aliases @@ -1270,6 +1270,8 @@ infinity() -- returns Float64 (positive infinity) **Redefining a special-cased built-in ADT is an error (E158)**: `data Future { ... }` and `data Tuple { ... }` are rejected at `vera check`, at the entry file and inside a module alike. These two names the compiler recognises *by name* throughout code generation — how a value is rendered, compared and laid out — so a declaration of one could not be told apart from the built-in, and accepting it was silent: `show(MkShadow(7))` under a `data Tuple` printed `(7)`, dropping the constructor name, and `data Future` compiled to a module that fails to load. It is the same rule that reserves built-in function names (E151) and built-in effect names (E152), and it covers both namespaces a declaration can put the name in: the `data` type name and a **constructor** name inside any ADT (`data Box { Tuple(Bool) }` is also E158, because code generation flattens constructor layouts by name and the user's would displace the built-in carrier's). Only those two: the prelude's data types (`Option`, `Result`, `Ordering`, `UrlParts`, `Json`, `HtmlNode`, `MdBlock`, `MdInline`, `Request`, `Response`) are ordinary declarations a program may shadow — `examples/vera/collections.vera` ships a `public data Option` — and so are the container names `Array`, `Map`, `Set` and `Decimal`. A `type Future = ...` / `type Tuple = ...` alias is unaffected: an alias names a binding, not a layout. Rename the declaration, or use the built-in directly. +**Two declarations may not share a constructor name (E159)**: within one file, two `data` declarations may not both declare a constructor of the same name — `private data A1 { Pair(Int, Int) }` beside `private data A2 { Pair(Bool, Bool) }` is rejected at `vera check`, located at the second declaration and naming the first. Constructor names are resolved by name alone, so one namespace cannot hold two, and accepting the pair produced diagnostics describing whichever declaration registered last rather than the collision. It is the single-file sibling of E610 (two modules) and E157 (two imports). Shadowing a *prelude* constructor is a different shape and stays legal — a program may restate `Option`, `Result` or `Ordering` — as is shadowing an *imported* constructor (§8.5.2), though see §11.16 for the compilation caveat on that pair. + **Reserved function names (E153)**: three groups of identifier cannot be a function name — two the grammar claims in expression position, and one the checker binds. `old` and `new` are contract state forms, so `old(...)` / `new(...)` always parses as a reference to an effect's before/after state (Chapter 7, Section 7.9.2) and never as a call. `assert`, `assume`, `forall`, `exists`, `match`, `if`, `let`, `fn`, `true` and `false` are keywords the lexer admits as a name after `fn` but reads as the keyword everywhere else, so `match(3)` in a body does not parse as a call either. A function under any of these — top-level, `where`-helper, or in an imported module — could never be called, and is rejected at `vera check`. Rename it. `resume` is reserved as well, for a different reason: it is not a keyword and a declaration does parse, but inside every handler clause body `resume` is the resumption operator, so declaring a function of that name would give one spelling two meanings by position. The rejection is the whole story: a clause body in the same file still resolves `resume` to the operator, so the rejected declaration draws no second error. Writing `resume(...)` inside a handler clause is unaffected. Only the exact identifiers are reserved: `older`, `renew`, `matched`, `resumed` and the like are ordinary function names. `handle` is the one keyword still available, because `public fn handle(@Request -> @Response)` is the entry point `vera serve` invokes from the host (Chapter 9, Section 9.5.6). Example: @@ -2413,7 +2415,7 @@ public fn main(@Unit -> @Unit) ## Conformance Suite -The `tests/conformance/` directory contains 251 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 253 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 62d552e44..b55cb75d7 100644 --- a/docs/index.html +++ b/docs/index.html @@ -697,7 +697,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 251-program conformance suite and 43 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 253-program conformance suite and 43 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 cc77eb1b6..ecbf37340 100644 --- a/docs/index.md +++ b/docs/index.md @@ -279,7 +279,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 251-program conformance suite and 43 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 253-program conformance suite and 43 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 c2d283939..645f5e6f7 100644 --- a/docs/llms-full.txt +++ b/docs/llms-full.txt @@ -499,7 +499,7 @@ match @Tuple.0 { } ``` -`Tuple` is just an upper-case constructor — there is no special tuple-literal syntax (no `(1, 2, 3)` form). The empty tuple `Tuple<>` is equivalent to `Unit`. The name is reserved in the data namespace: `data Tuple { ... }` is rejected at `vera check` with **E158** (see below), because the compiler recognises `Tuple` by name when it renders and lays out a value. A `type Tuple = ...` alias is unaffected. +`Tuple` is just an upper-case constructor — there is no special tuple-literal syntax (no `(1, 2, 3)` form). The empty tuple `Tuple<>` is equivalent to `Unit`. The name is reserved in both the data and the constructor namespace: `data Tuple { ... }` and `data Box { Tuple(Bool) }` are each rejected at `vera check` with **E158** (see below), because the compiler recognises `Tuple` by name when it renders and lays out a value. A `type Tuple = ...` alias is unaffected. ### Type aliases @@ -1276,6 +1276,8 @@ infinity() -- returns Float64 (positive infinity) **Redefining a special-cased built-in ADT is an error (E158)**: `data Future { ... }` and `data Tuple { ... }` are rejected at `vera check`, at the entry file and inside a module alike. These two names the compiler recognises *by name* throughout code generation — how a value is rendered, compared and laid out — so a declaration of one could not be told apart from the built-in, and accepting it was silent: `show(MkShadow(7))` under a `data Tuple` printed `(7)`, dropping the constructor name, and `data Future` compiled to a module that fails to load. It is the same rule that reserves built-in function names (E151) and built-in effect names (E152), and it covers both namespaces a declaration can put the name in: the `data` type name and a **constructor** name inside any ADT (`data Box { Tuple(Bool) }` is also E158, because code generation flattens constructor layouts by name and the user's would displace the built-in carrier's). Only those two: the prelude's data types (`Option`, `Result`, `Ordering`, `UrlParts`, `Json`, `HtmlNode`, `MdBlock`, `MdInline`, `Request`, `Response`) are ordinary declarations a program may shadow — `examples/vera/collections.vera` ships a `public data Option` — and so are the container names `Array`, `Map`, `Set` and `Decimal`. A `type Future = ...` / `type Tuple = ...` alias is unaffected: an alias names a binding, not a layout. Rename the declaration, or use the built-in directly. +**Two declarations may not share a constructor name (E159)**: within one file, two `data` declarations may not both declare a constructor of the same name — `private data A1 { Pair(Int, Int) }` beside `private data A2 { Pair(Bool, Bool) }` is rejected at `vera check`, located at the second declaration and naming the first. Constructor names are resolved by name alone, so one namespace cannot hold two, and accepting the pair produced diagnostics describing whichever declaration registered last rather than the collision. It is the single-file sibling of E610 (two modules) and E157 (two imports). Shadowing a *prelude* constructor is a different shape and stays legal — a program may restate `Option`, `Result` or `Ordering` — as is shadowing an *imported* constructor (§8.5.2), though see §11.16 for the compilation caveat on that pair. + **Reserved function names (E153)**: three groups of identifier cannot be a function name — two the grammar claims in expression position, and one the checker binds. `old` and `new` are contract state forms, so `old(...)` / `new(...)` always parses as a reference to an effect's before/after state (Chapter 7, Section 7.9.2) and never as a call. `assert`, `assume`, `forall`, `exists`, `match`, `if`, `let`, `fn`, `true` and `false` are keywords the lexer admits as a name after `fn` but reads as the keyword everywhere else, so `match(3)` in a body does not parse as a call either. A function under any of these — top-level, `where`-helper, or in an imported module — could never be called, and is rejected at `vera check`. Rename it. `resume` is reserved as well, for a different reason: it is not a keyword and a declaration does parse, but inside every handler clause body `resume` is the resumption operator, so declaring a function of that name would give one spelling two meanings by position. The rejection is the whole story: a clause body in the same file still resolves `resume` to the operator, so the rejected declaration draws no second error. Writing `resume(...)` inside a handler clause is unaffected. Only the exact identifiers are reserved: `older`, `renew`, `matched`, `resumed` and the like are ordinary function names. `handle` is the one keyword still available, because `public fn handle(@Request -> @Response)` is the entry point `vera serve` invokes from the host (Chapter 9, Section 9.5.6). Example: @@ -2419,7 +2421,7 @@ public fn main(@Unit -> @Unit) ## Conformance Suite -The `tests/conformance/` directory contains 251 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 253 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. @@ -2494,7 +2496,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 251 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 forty-five negative fixtures (`ch02_generic_over_unit_rejected`, `ch02_map_unit_value_rejected`, `ch02_nonregular_data_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`, `ch04_pattern_ctor_over_container_rejected`, `ch04_pattern_literal_type_rejected`, `ch05_where_helper_sibling_call_rejected`, `ch08_builtin_adt_redefinition_rejected`, `ch08_builtin_tuple_redefinition_rejected`, `ch08_builtin_ctor_redefinition_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 253 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 forty-six negative fixtures (`ch02_generic_over_unit_rejected`, `ch02_map_unit_value_rejected`, `ch02_nonregular_data_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`, `ch04_pattern_ctor_over_container_rejected`, `ch04_pattern_literal_type_rejected`, `ch05_where_helper_sibling_call_rejected`, `ch08_builtin_adt_redefinition_rejected`, `ch08_builtin_tuple_redefinition_rejected`, `ch08_builtin_ctor_redefinition_rejected`, `ch08_sibling_ctor_collision_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 @@ -2679,9 +2681,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 251 conformance programs hold (positives pass; negatives fail with their E-code) +python scripts/check_conformance.py # All 253 conformance programs hold (positives pass; negatives fail with their E-code) python scripts/check_examples.py # All 43 examples must pass -python scripts/check_corpus_canonical.py # All 301 corpus programs in canonical form +python scripts/check_corpus_canonical.py # All 303 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. @@ -2690,7 +2692,7 @@ When implementing a new language feature, write the conformance program *first* ### Invariants -- All 251 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`, `ch02_nonregular_data_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`, `ch04_pattern_ctor_over_container_rejected`, `ch04_pattern_literal_type_rejected`, `ch05_where_helper_sibling_call_rejected`, `ch08_builtin_adt_redefinition_rejected`, `ch08_builtin_tuple_redefinition_rejected`, `ch08_builtin_ctor_redefinition_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 253 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`, `ch02_nonregular_data_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`, `ch04_pattern_ctor_over_container_rejected`, `ch04_pattern_literal_type_rejected`, `ch05_where_helper_sibling_call_rejected`, `ch08_builtin_adt_redefinition_rejected`, `ch08_builtin_tuple_redefinition_rejected`, `ch08_builtin_ctor_redefinition_rejected`, `ch08_sibling_ctor_collision_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 43 examples in `examples/` must pass `vera check` and `vera verify` - `mypy vera/` must be clean - `pytest tests/ -v` must pass @@ -3235,7 +3237,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 one preferred surface spelling `vera fmt` produces deterministically), which reduces the surface area a model needs to learn. Third, the conformance test suite (251 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, and 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 one preferred surface spelling `vera fmt` produces deterministically), which reduces the surface area a model needs to learn. Third, the conformance test suite (253 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, and a comprehensive test suite is a strong scaffold for a model implementing to a specification. ## How does Vera compare to Dafny / Lean / Koka / F*? @@ -3278,7 +3280,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 -- 13,517 tests, including a 251-program conformance suite +- 13,575 tests, including a 253-program conformance suite - 43 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 @@ -3403,6 +3405,7 @@ Every diagnostic has a stable error code. Codes are grouped by compiler phase: - **E156**: Bare data type name supplied by two imports - **E157**: Bare constructor name supplied by two imports - **E158**: Declaration reuses a special-cased built-in ADT name +- **E159**: Two data declarations share a constructor name - **E160**: Array index must be Int or Nat - **E161**: Cannot index non-array type - **E170**: Let binding type mismatch diff --git a/docs/llms.txt b/docs/llms.txt index c67cfa6aa..efbef0141 100644 --- a/docs/llms.txt +++ b/docs/llms.txt @@ -57,4 +57,4 @@ Current version: 0.1.13. 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): 251 programs validating every language feature against the spec. +- [Conformance Suite](https://github.com/aallan/vera/tree/main/tests/conformance): 253 programs validating every language feature against the spec. diff --git a/spec/08-modules.md b/spec/08-modules.md index 9c9fc138b..67de17475 100644 --- a/spec/08-modules.md +++ b/spec/08-modules.md @@ -106,7 +106,7 @@ private fn helper(@Int -> @Int) - `public` declarations are visible to any module that imports them. - `private` declarations are visible only within the module that defines them. -- Type aliases (`type Foo = ...`), effect declarations (`effect E { ... }`), module declarations, and import statements do not take visibility modifiers. These declarations are **module-local** — they are not importable by other modules. If another module needs the same type alias or effect, it must declare its own copy. The prelude's own combinators resolve their closure-parameter types through aliases a program cannot name: those aliases carry reserved names, and a name beginning with `Vera` followed by an uppercase letter or digit is a compile error (**E154**) — whether the program *declares* that name as a type, an alias, an effect, an ability or a constructor, *binds* it as a type parameter, or merely *mentions* it in a type. The reservation is one rule across every namespace, so the prelude's internal namespace can be neither re-typed, shadowed by a binder, nor referenced, and a program that wants a short name for a function type declares its own alias for it. Outside a type position there is no alias escape, so the fix in the effect, ability and constructor namespaces is simply a name that does not start with the reserved prefix. The prelude's data types (`Option`, `Result`, `Ordering`, `UrlParts`, …) are not in that namespace: they are ordinary public declarations a program names, and shadows, like any other. Two built-in type names are the exception, and are reserved in the **data** namespace: `Future` and `Tuple`, whose semantics the compiler recognises by name throughout code generation — how a value is rendered, compared and laid out — so a declaration of either could not be told apart from the built-in. Declaring one is **E158**, at the entry file and in a module alike, on the same rule that reserves built-in function names (**E151**) and built-in effect names (**E152**). The reservation covers both namespaces a declaration can put the name in — as a `data` type name, and as a **constructor** name inside any ADT (`data Box { Tuple(Bool) }` is also **E158**) — because code generation keys the collision on the type name in one case and on the constructor name in the other, so reserving only the type would leave a declaration in one corner of a file changing what the built-in means in another. A `type` alias of those names is unaffected: an alias names a binding, not a layout. A declaration in the **entry file** shadows the prelude's for the whole program: the prelude injects nothing under that name, so the entry's declaration never contends with the prelude's. Where a *module* declares the same name as well, the entry's declaration and the module's are a distinct pair, arbitrated by the same shape test: they share the one layout when their shapes match, and the compiler reports **E623** at the entry declaration when they differ (§11.16). A declaration in a **module** shadows it for that module alone only while the prelude is not also compiling its own declaration of that name — the two would otherwise contend for one layout in the flat compiled namespace (§11.16), and the compiler reports **E621** at the module's declaration. Whether they contend is decided by the two declarations' *shapes*: a module that restates the prelude's type — the same constructors, in the same order, with the same field types, type parameters compared by position — shares the one layout and is not a contention. A differently-shaped one is, and the condition differs between the two halves of the prelude's data types: for `Json`, `HtmlNode`, `Request` and `Response`, which the prelude injects only when the entry program uses them, the module's declaration stands alone until it does; for `Option`, `Result`, `Ordering` and `UrlParts`, which every program compiles, a differently-shaped module declaration always contends. +- Type aliases (`type Foo = ...`), effect declarations (`effect E { ... }`), module declarations, and import statements do not take visibility modifiers. These declarations are **module-local** — they are not importable by other modules. If another module needs the same type alias or effect, it must declare its own copy. The prelude's own combinators resolve their closure-parameter types through aliases a program cannot name: those aliases carry reserved names, and a name beginning with `Vera` followed by an uppercase letter or digit is a compile error (**E154**) — whether the program *declares* that name as a type, an alias, an effect, an ability or a constructor, *binds* it as a type parameter, or merely *mentions* it in a type. The reservation is one rule across every namespace, so the prelude's internal namespace can be neither re-typed, shadowed by a binder, nor referenced, and a program that wants a short name for a function type declares its own alias for it. Outside a type position there is no alias escape, so the fix in the effect, ability and constructor namespaces is simply a name that does not start with the reserved prefix. The prelude's data types (`Option`, `Result`, `Ordering`, `UrlParts`, …) are not in that namespace: they are ordinary public declarations a program names, and shadows, like any other. Two built-in type names are the exception, and are reserved in the **data** namespace: `Future` and `Tuple`, whose semantics the compiler recognises by name throughout code generation — how a value is rendered, compared and laid out — so a declaration of either could not be told apart from the built-in. Declaring one is **E158**, at the entry file and in a module alike, on the same rule that reserves built-in function names (**E151**) and built-in effect names (**E152**). The reservation covers both namespaces a declaration can put the name in — as a `data` type name, and as a **constructor** name inside any ADT (`data Box { Tuple(Bool) }` is also **E158**) — because code generation keys the collision on the type name in one case and on the constructor name in the other, so reserving only the type would leave a declaration in one corner of a file changing what the built-in means in another. A `type` alias of those names is unaffected: an alias names a binding, not a layout. The reservation stops there: every OTHER built-in or prelude constructor name stays available to a declaration, and a declaration that takes one does not change what the prelude's constructor of that name means — constructor layouts are keyed per owning data type, so the two coexist (a `data ZzBox { Less(Bool) }` leaves `Ordering`'s `Less` rendering as `Less`). A declaration in the **entry file** shadows the prelude's for the whole program: the prelude injects nothing under that name, so the entry's declaration never contends with the prelude's. Where a *module* declares the same name as well, the entry's declaration and the module's are a distinct pair, arbitrated by the same shape test: they share the one layout when their shapes match, and the compiler reports **E623** at the entry declaration when they differ (§11.16). A declaration in a **module** shadows it for that module alone only while the prelude is not also compiling its own declaration of that name — the two would otherwise contend for one layout in the flat compiled namespace (§11.16), and the compiler reports **E621** at the module's declaration. Whether they contend is decided by the two declarations' *shapes*: a module that restates the prelude's type — the same constructors, in the same order, with the same field types, type parameters compared by position — shares the one layout and is not a contention. A differently-shaped one is, and the condition differs between the two halves of the prelude's data types: for `Json`, `HtmlNode`, `Request` and `Response`, which the prelude injects only when the entry program uses them, the module's declaration stands alone until it does; for `Option`, `Result`, `Ordering` and `UrlParts`, which every program compiles, a differently-shaped module declaration always contends. - Functions declared inside `where` blocks are always local to the parent function and do not take visibility modifiers. ### 8.4.2 Data Type Visibility @@ -237,6 +237,14 @@ A constructor is admitted by its parent type's name (§8.5.4), so differently-named types that share a constructor name clash on the constructor alone. The three are therefore reported independently. +Two declarations in ONE namespace sharing a constructor name are the same clash +asked of a single file, and are **E159**, located at the second declaration and +naming the first; shadowing a *prelude* constructor is not that shape and stays +legal (§8.4.1). A local declaration taking a constructor name an *imported* +type also declares is likewise outside this rule (§8.5.2), but see the +compilation caveat in §11.16: the compiled namespace is flat, so that pair is +not yet compiled correctly. + Each is rejected at check time, in whichever namespace holds the clash: the entry program's, or any module's, since a module's bodies resolve in their own namespace (§8.5.2.1) and the rule is a property of that namespace rather than of @@ -350,7 +358,9 @@ import vera.collections(List); ``` Constructor names follow the same shadowing rules as function names: a local -declaration shadows an imported constructor (§8.5.2), and a constructor name two +declaration shadows an imported constructor (§8.5.2) — though see §11.16 for the compilation +caveat on that pair, tracked as [#1436](https://github.com/aallan/vera/issues/1436) — and a +constructor name two imports both supply is refused (§8.5.2.2, **E157**) exactly as a function name is. An imported type's constructors are admitted by the type's name, so a selective import naming the type admits all of them. diff --git a/spec/11-compilation.md b/spec/11-compilation.md index 854d40971..d42839d1d 100644 --- a/spec/11-compilation.md +++ b/spec/11-compilation.md @@ -619,6 +619,8 @@ Imported functions are **not** exported from the WASM module — only the import An imported module's data type may collide with one the **prelude** provides in the same way, and the compiler reports **E621** at the module's declaration. The prelude's declarations are compiled into this same flat namespace, which holds one layout per name, so two declarations of a prelude name contend exactly when their *shapes* differ — different constructors, a different constructor order (the tag is the position), or different field types; type parameters are compared by position, so renaming one is not a difference. A module that restates the prelude's type shares the one layout and compiles. The diagnostic names the module and the type and offers both resolutions: rename it in the module, or give it the prelude's shape. +A constructor name a **local declaration** and an **imported** type both declare is not a collision — §8.5.2 makes the local declaration shadow the imported one — but the compiled namespace is flat, so that pair is not yet compiled correctly: the by-name constructor tables the code generator consults are built across every namespace a compilation absorbs, and the entry file's declaration takes the slot. The exporting module's own bodies are then compiled against the wrong tag, with no diagnostic from `vera check` or `vera verify`. This is tracked as [#1436](https://github.com/aallan/vera/issues/1436). + The **entry file**'s own data types meet the modules' in that same namespace, and the compiler reports **E623** at the entry declaration when the two shapes differ, naming the module's file and line. Shape decides here exactly as it does for the prelude pair, so an entry file that restates a module's public type shares the one layout and compiles. This is the third pair the single slot can hold — module against module (E609/E610), module against prelude (E621), entry file against module (E623) — and all three ask the same question of the two declarations. Whether the prelude is compiling its own declaration of that name depends on which half of its data types the name belongs to. `Json`, `HtmlNode`, `Request` and `Response` are injected only when the entry program uses them, so a module's differently-shaped declaration stands alone until it does. `Option`, `Result`, `Ordering` and `UrlParts` are in every program, so a differently-shaped module declaration of one of those always contends. A declaration in the **entry file** suppresses the prelude's injection outright and so never contends with it (§8.4.1). diff --git a/tests/conformance/ch08_sibling_ctor_collision_rejected.vera b/tests/conformance/ch08_sibling_ctor_collision_rejected.vera new file mode 100644 index 000000000..5d1e20d8d --- /dev/null +++ b/tests/conformance/ch08_sibling_ctor_collision_rejected.vera @@ -0,0 +1,22 @@ +-- Conformance: constructor names are unique per NAMESPACE (Chapter 8, Section 8.4) +-- Tests: E159 — two data declarations in one file share a constructor name (#1425). +-- The intra-namespace sibling of E610 (two modules) and E157 (two imports); +-- spec §8.4 puts all three under one rule. Accepting it left resolution to +-- last-declaration-wins, so a use produced diagnostics naming neither +-- declaration. Shadowing a PRELUDE or IMPORTED constructor stays legal — +-- the rule is two declarations in one namespace. +private data A1 { + Pair(Int, Int) +} + +private data A2 { + Pair(Bool, Bool) +} + +public fn main(-> @Int) + requires(true) + ensures(true) + effects(pure) +{ + 0 +} diff --git a/tests/conformance/ch09_user_ctor_shadows_prelude_ctor.vera b/tests/conformance/ch09_user_ctor_shadows_prelude_ctor.vera new file mode 100644 index 000000000..aae9f49ab --- /dev/null +++ b/tests/conformance/ch09_user_ctor_shadows_prelude_ctor.vera @@ -0,0 +1,19 @@ +-- Conformance: a user constructor sharing a prelude constructor's NAME does +-- not change what the prelude's means (Chapter 9, Section 9.8) +-- Tests: #1414 — constructor layouts are keyed per owning ADT. +-- `ZzBox` is never used; before the fix its mere declaration made every +-- `Ordering` in the program render as `Less(false)`, on a check-clean and +-- verify-clean program. A positive rather than a negative fixture: §8.4.1 +-- makes the prelude's data types shadowable, so this program is LEGAL and +-- the bug was that it compiled to the wrong answer. +private data ZzBox { + Less(Bool) +} + +public fn main(-> @Bool) + requires(true) + ensures(true) + effects(pure) +{ + eq(show(compare(1, 2)), "Less") && eq(show(compare(2, 1)), "Greater") && eq(show(compare(2, 2)), "Equal") && eq(show(Less(true)), "Less(true)") +} diff --git a/tests/conformance/manifest.json b/tests/conformance/manifest.json index 482ab8de2..877a2ef63 100644 --- a/tests/conformance/manifest.json +++ b/tests/conformance/manifest.json @@ -3518,6 +3518,32 @@ "check_error" ] }, + { + "id": "ch09_user_ctor_shadows_prelude_ctor", + "file": "ch09_user_ctor_shadows_prelude_ctor.vera", + "chapter": 9, + "title": "A user constructor does not displace a prelude constructor of the same name", + "level": "run", + "spec_ref": "Section 9.8", + "features": [ + "constructor_shadowing", + "show", + "ord" + ] + }, + { + "id": "ch08_sibling_ctor_collision_rejected", + "file": "ch08_sibling_ctor_collision_rejected.vera", + "chapter": 8, + "title": "Two data declarations in one namespace may not share a constructor name", + "level": "check", + "spec_ref": "Section 8.4", + "expected_error": "E159", + "features": [ + "constructor_collision", + "check_error" + ] + }, { "id": "ch08_builtin_ctor_redefinition_rejected", "file": "ch08_builtin_ctor_redefinition_rejected.vera", diff --git a/tests/test_name_resolution_spine_1316.py b/tests/test_name_resolution_spine_1316.py index 7e8273b0d..2514865c1 100644 --- a/tests/test_name_resolution_spine_1316.py +++ b/tests/test_name_resolution_spine_1316.py @@ -71,6 +71,7 @@ from vera.codegen import CodeGenerator, execute from vera.codegen.api import CompileResult from vera.naming import AliasEnv, NameSort, classify_named +from vera.parser import parse_to_ast from vera.prelude import PRELUDE_NAMESPACE, prelude_adt_names from vera.types import PRIMITIVES from vera.wasm import WasmContext @@ -911,13 +912,49 @@ def test_a_constructor_of_the_name_is_refused_too(self, name: str) -> None: )] assert "E158" in codes, codes - def test_a_constructor_of_an_unreserved_builtin_name_is_fine(self) -> None: - """The constructor reservation is exactly the reserved names. + @pytest.mark.parametrize("name", _EXPECTED_RESERVED) + def test_a_constructor_of_the_name_is_refused_in_a_module_too( + self, name: str, tmp_path: Path, + ) -> None: + """Both doors for the CONSTRUCTOR half as well as the type half. + + The type reservation is measured at both declaration sites, and the + constructor one has to be too: the collision it prevents is a FLAT + `ctor_layouts` slot shared across every ADT in the compiled module, + so a module's declaration reaches the entry program's built-in tuple + constructions exactly as an entry-file one does. Measured at + `release/v0.2.0`: accepted in a module, for both names. + """ + from tests.module_fixture_helpers import build_multi_module_past_check + + module = ( + "module tlib;\n\n" + f"private data ZzBox {{ {name}(Bool) }}\n\n" + "public fn probe(@Int -> @Int)\n" + " requires(true)\n ensures(true)\n effects(pure)\n" + "{\n @Int.0\n}\n" + ) + check_errors, _result, _cg = build_multi_module_past_check( + tmp_path, + {"tlib.vera": module, "main.vera": _MODULE_SHADOW_MAIN}, + ) + assert "E158" in [code for code, _ in check_errors], check_errors - `UrlParts` is a built-in ADT whose constructor shares its name, and - SKILL.md tells programs to redeclare it locally to match on it — so - the constructor namespace must stay open for every name the data - namespace leaves open. + def test_a_constructor_of_an_unreserved_builtin_name_is_not_E158( + self, + ) -> None: + """E158 does not fire — which is all this measures. + + Named for the assertion, not for a safety property it does not + establish (PR #1404 review, finding 7). "Unreserved" is not "safe": + the flat-by-constructor-name layout table reaches every built-in + constructor, and for `Less` it was a silent wrong value while + `Some` / `None` / `Ok` / `Err` are loud (E213 / E215 / E121). That + clobber is #1414, fixed in this PR by per-owner keying rather than + by widening the reservation — §8.4.1 makes the prelude's data types + shadowable and `examples/vera/collections.vera` declares `None` and + `Some`, so a reservation over prelude constructor names would refuse + a shipped example. What stays true here is only the E158 boundary. """ codes = [d.error_code for d in _check( "private data ZzBox { UrlParts(Bool) }\n\n" @@ -927,6 +964,38 @@ def test_a_constructor_of_an_unreserved_builtin_name_is_fine(self) -> None: )] assert "E158" not in codes, codes + @pytest.mark.parametrize("name", _EXPECTED_RESERVED) + def test_a_refused_constructor_is_not_registered(self, name: str) -> None: + """A name the checker refused must not stay resolvable (#1404 review). + + Registration continues past `_error` so the rest of the declaration + still reports, which used to leave the refused constructor in + `env.constructors` — harmless today, because a check failure stops + the pipeline before anything reads it, but a table that disagrees + with the diagnostics is a trap for the next consumer. + + Mutation-validated: withdrawing the `continue` in `_register_data` + puts the entry back and turns this red, so the cell is known to bite + rather than assumed to. + """ + from vera.checker.core import TypeChecker + + source = ( + f"private data ZzBox {{ {name}(Bool) }}\n\n" + "public fn main(@Unit -> @Int)\n" + " requires(true)\n ensures(true)\n effects(pure)\n" + "{\n 0\n}\n" + ) + checker = TypeChecker(source) + checker.check_program(parse_to_ast(source)) + registered = checker.env.constructors.get(name) + # `Future` legitimately occupies the name already — the built-in ADT + # registers its own constructor in `environment.py` — so the property + # is OWNERSHIP, not absence: whatever sits under the name must not be + # the refused declaration's. + assert getattr(registered, "parent_type", None) != "ZzBox", ( + f"{name!r} was refused but ZzBox's constructor was registered") + def test_the_builtin_tuple_is_still_not_eq(self) -> None: """And the built-in's own limitation is unchanged either way. @@ -949,6 +1018,753 @@ def test_the_builtin_tuple_is_still_not_eq(self) -> None: assert codes == ["E243"], codes + +class TestUserConstructorCannotDisplaceABuiltinOne: + """#1414 — a user constructor of a built-in/prelude constructor NAME must + not change what the built-in one means. + + Codegen holds constructor layouts in one table keyed by bare constructor + name across every ADT (`ctor_layouts.update(layouts)` over + `_adt_layouts.items()`, built-ins first), so a later user ADT wins the + slot. #1408 closed this for `Tuple` and `Future` by reserving those two + names, but the mechanism is general and reserving the rest is not + available: §8.4.1 makes the prelude's data types shadowable, #1277 says + so in terms, and `examples/vera/collections.vera` ships a `public data + Option { None, Some(T) }` that a prelude-constructor reservation would + refuse. + + So the fix is per-owner keying, and these are its two measured repros. + Both were check-clean AND verify-clean at `release/v0.2.0` and at the + #1404 merge tip. + """ + + def test_an_unrelated_declaration_does_not_change_what_compare_returns( + self, + ) -> None: + """Base: every `Ordering` rendered as the clobbering constructor. + + `show(compare(1, 2))`, `(2, 1)` and `(2, 2)` all returned + `'Less(false)'` where the control returns `Less` / `Greater` / + `Equal`. `ZzBox` is never used — its mere declaration changed the + answer for every input, on a program with zero diagnostics. + """ + source = """\ +private data ZzBox { Less(Bool) } + +public fn lt(@Unit -> @String) + requires(true) + ensures(true) + effects(pure) +{ + show(compare(1, 2)) +} + +public fn gt(@Unit -> @String) + requires(true) + ensures(true) + effects(pure) +{ + show(compare(2, 1)) +} + +public fn eqq(@Unit -> @String) + requires(true) + ensures(true) + effects(pure) +{ + show(compare(2, 2)) +} +""" + result = _compile_ok(source) + got = { + fn: execute(result, fn_name=fn).value + for fn in ("lt", "gt", "eqq") + } + assert got == {"lt": "Less", "gt": "Greater", "eqq": "Equal"}, got + + def test_the_control_without_the_declaration_is_identical(self) -> None: + """The same three functions with no colliding declaration. + + Green at every revision by construction — it is here so the cell + above cannot be satisfied by breaking `compare` for everyone. + """ + source = """\ +public fn lt(@Unit -> @String) + requires(true) + ensures(true) + effects(pure) +{ + show(compare(1, 2)) +} + +public fn gt(@Unit -> @String) + requires(true) + ensures(true) + effects(pure) +{ + show(compare(2, 1)) +} + +public fn eqq(@Unit -> @String) + requires(true) + ensures(true) + effects(pure) +{ + show(compare(2, 2)) +} +""" + result = _compile_ok(source) + got = { + fn: execute(result, fn_name=fn).value + for fn in ("lt", "gt", "eqq") + } + assert got == {"lt": "Less", "gt": "Greater", "eqq": "Equal"}, got + + def test_a_colliding_declaration_does_not_drop_the_function(self) -> None: + """The second repro: a `[E602]` degrade rather than a wrong value. + + Base: `show(@UrlParts.0)` beside `private data ZzBox { + UrlParts(Bool) }` was check-clean and verify-clean, then compiled to + a module with NO exports behind an `[E602]` warning. No + `UrlParts(...)` pattern appears, so nothing collides at check. + """ + source = """\ +private data ZzBox { UrlParts(Bool) } + +public fn render(@UrlParts -> @String) + requires(true) + ensures(true) + effects(pure) +{ + show(@UrlParts.0) +} +""" + result = _compile(source) + assert [d.error_code for d in result.diagnostics] == [], ( + [(d.severity, d.error_code, d.description[:70]) + for d in result.diagnostics] + ) + assert "render" in result.exports, sorted(result.exports) + + def test_the_user_constructor_still_works_on_its_own_type(self) -> None: + """Per-owner keying must not cost the DECLARATION its meaning. + + §8.4.1 grants the shadow; the point is that both readings coexist, + so the user's `Less(Bool)` has to construct and match as its own + type while `Ordering`'s `Less` stays the prelude's. + """ + source = """\ +private data ZzBox { Less(Bool) } + +public fn mine(@Unit -> @String) + requires(true) + ensures(true) + effects(pure) +{ + show(Less(true)) +} + +public fn theirs(@Unit -> @String) + requires(true) + ensures(true) + effects(pure) +{ + show(compare(1, 2)) +} +""" + result = _compile_ok(source) + assert execute(result, fn_name="mine").value == "Less(true)" + assert execute(result, fn_name="theirs").value == "Less" + + + def test_the_nested_recovery_collision_is_refused_at_check(self) -> None: + """Why the nested-recovery site is LATENT, pinned so it stays so. + + `_recover_ptype_via_nested_fields` reads a constructor's + `field_types` to rebuild a generic ADT's type arguments, and read + the flat by-name table to do it — the render site's defect, one pass + over (PR #1419 review). It is owner-qualified now, and no program + reaches the old path, and since #1425 the reason is a rail rather + than a coincidence: two declarations in one namespace sharing a + constructor name are `[E159]` at the declaration, in either order. + Before that rail the shielding was accidental — the CHECKER + resolved the call through the same last-wins by-name rule, so when + the flat map held the wrong ADT the checker had already refused the + call against that same wrong resolution. + + Two layers wrong in the same direction is a coincidence, not a + guarantee. This cell pins the coincidence: if the checker is ever + taught per-owner resolution without code generation following, the + E212 disappears, this cell goes red, and it names the site whose + owner-qualified read then becomes load-bearing. + """ + rose = "private data Rose { Leaf(T), Node(T, Rose) }" + zz = "private data ZzBox { Node(Bool) }" + body = ( + "\n\npublic fn main(@Unit -> @String)\n" + " requires(true)\n ensures(true)\n effects(pure)\n" + "{\n show(Node(1, Leaf(2)))\n}\n" + ) + # Since #1425 the pair is refused at the DECLARATION, in either + # order — stronger shielding than the E212-on-use it used to rely + # on, and it no longer depends on which declaration won the slot. + for src in (rose + "\n\n" + zz + body, zz + "\n\n" + rose + body): + codes = [d.error_code for d in _check(src)] + # E159 always; one order additionally carries the E212 the USE + # used to be shielded by, which is now redundant but harmless. + assert "E159" in codes, ( + f"the shielding refusal is gone ({codes}) — see the docstring") + + +#: A shadowing `Less` at each TAG INDEX. The first entry is the shape the +#: fix was first written against, and it is the one index where a +#: reader-only fix cannot be caught: the user's `Less` sits at tag 0, which +#: is also `Ordering`'s, so a value tagged through the wrong table still +#: renders right. Shifting the index separates the writer from the reader +#: (PR #1419 review). +_LESS_AT_INDEX = { + "tag0": "private data ZzBox { Less(Bool) }", + "tag1": "private data ZzBox { Pad(Bool), Less }", + "tag3": "private data ZzBox { A, B, C, Less }", +} + +_COMPARE_TRIO = """ +public fn lt(@Unit -> @String) + requires(true) + ensures(true) + effects(pure) +{ + show(compare(%(a)s, %(b)s)) +} + +public fn gt(@Unit -> @String) + requires(true) + ensures(true) + effects(pure) +{ + show(compare(%(b)s, %(a)s)) +} + +public fn eqq(@Unit -> @String) + requires(true) + ensures(true) + effects(pure) +{ + show(compare(%(b)s, %(b)s)) +} +""" + +#: `compare` over each ordered primitive, so the fix is not pinned on `Int` +#: alone — the desugaring is shared and a per-type regression would hide. +_COMPARE_OPERANDS = { + "Int": {"a": "1", "b": "2"}, + "String": {"a": '"a"', "b": '"b"'}, + "Float64": {"a": "1.0", "b": "2.0"}, +} + + +class TestShadowingConstructorTagIndex: + """#1414 — the tag a compiler-emitted constructor is WRITTEN with must + come from the same table it is READ through. + + Converting only the reader left the value tagged through the user's ADT + and rendered through `Ordering`'s, which agree exactly when the + shadowing constructor sits at its namesake's index. Measured on the + reader-only fix: `ZzBox { Pad(Bool), Less }` gave `Equal` / `Greater` / + `Equal` for lt / gt / eqq, and `ZzBox { A, B, C, Less }` gave + `Greater` / `Greater` / `Equal`, on programs `vera check` and + `vera verify` both call clean. + """ + + @pytest.mark.parametrize("index", sorted(_LESS_AT_INDEX)) + @pytest.mark.parametrize("ty", sorted(_COMPARE_OPERANDS)) + def test_compare_renders_correctly_at_every_shadow_index( + self, ty: str, index: str, + ) -> None: + source = ( + _LESS_AT_INDEX[index] + "\n" + + _COMPARE_TRIO % _COMPARE_OPERANDS[ty] + ) + result = _compile_ok(source) + got = { + fn: execute(result, fn_name=fn).value + for fn in ("lt", "gt", "eqq") + } + assert got == {"lt": "Less", "gt": "Greater", "eqq": "Equal"}, got + + @pytest.mark.parametrize("index", sorted(_LESS_AT_INDEX)) + def test_eq_and_hash_of_compare_results_agree_at_every_index( + self, index: str, + ) -> None: + """`show` is not the only reader of the tag. + + A wrongly-tagged `Ordering` compares and hashes wrongly too, and + `eq(compare(1, 2), compare(2, 2))` returned 1 on the reader-only + fix — `Less` and `Equal` indistinguishable — with `hash` agreeing, + so neither would have caught it. + """ + source = _LESS_AT_INDEX[index] + """ + +public fn lt_vs_eq(@Unit -> @Bool) + requires(true) + ensures(true) + effects(pure) +{ + eq(compare(1, 2), compare(2, 2)) +} + +public fn hash_agrees(@Unit -> @Bool) + requires(true) + ensures(true) + effects(pure) +{ + eq(hash(compare(1, 2)), hash(compare(2, 2))) +} +""" + result = _compile_ok(source) + # A `@Bool` comes back as WASM's 0 / 1, not a Python bool. + assert execute(result, fn_name="lt_vs_eq").value == 0, ( + "Less and Equal must not compare equal") + assert execute(result, fn_name="hash_agrees").value == 0, ( + "Less and Equal must not hash alike") + + +class TestStructuralEqEnumerationIsUnobservable: + """#1414 — why `operators.py`'s owner-qualified enumeration is INERT, + stated as the three legs that make it so. + + Forcing `_generate_adt_eq_fn_body` back to the flat map leaves the whole + tag-index battery green, so no behavioural cell can red on it. That is + not because the site is unreached — it runs, measured, as + `$eq_Ordering` — but because its output is insensitive for the only + shapes a program can build. Each leg is asserted here, so if any of + them changes the argument fails loudly instead of rotting. + """ + + _SRC = """\ +private data ZzBox { Pad(Bool), Less } + +public fn cmp_eq(@Unit -> @Bool) + requires(true) + ensures(true) + effects(pure) +{ + eq(compare(1, 2), compare(2, 2)) +} +""" + + def test_leg1_the_flat_enumeration_really_does_lose_a_constructor( + self, + ) -> None: + """The collision is real at this site — the conversion is not a + no-op dressed up as one.""" + _result, gen = _compile_with_generator(self._SRC) + flat_owner = { + c: adt for adt, ls in gen._adt_layouts.items() for c in ls + } + assert flat_owner["Less"] == "ZzBox", flat_owner["Less"] + flat_enum = sorted(c for c, p in flat_owner.items() if p == "Ordering") + assert flat_enum == ["Equal", "Greater"], flat_enum + assert sorted(gen._adt_layouts["Ordering"]) == [ + "Equal", "Greater", "Less"] + + def test_leg2_orderings_constructors_are_all_nullary(self) -> None: + """Which is why losing one cannot change the emitted equality: with + no fields anywhere, the generated body reduces to a tag comparison + and the per-constructor field plans contribute nothing.""" + _result, gen = _compile_with_generator(self._SRC) + assert all( + not layout.field_offsets + for layout in gen._adt_layouts["Ordering"].values() + ) + + @pytest.mark.parametrize("decl,expected", [ + # Two USER declarations sharing a name — E159, this PR. + ("private data A1 { Wrap(Int) }\n\nprivate data A2 { Wrap(Bool) }", + "E159"), + # Shadowing a FIELD-CARRYING prelude constructor — refused at the use. + ("private data ZzBox { Pad(Bool), Some(Bool) }", "E213"), + ]) + def test_leg3_the_single_file_routes_to_that_shadow_are_refused( + self, decl: str, expected: str, + ) -> None: + """Both SINGLE-FILE routes to a field-carrying shadow are refused. + + Deliberately narrower than the claim this cell first made. "The + shadow is unbuildable" is FALSE: it is buildable across a module + boundary, where an entry-file declaration takes a constructor name + an imported type also declares — the shape #1419's review calls + finding A, which is miscompiled today and is not fixed by this PR. + What survives is the conclusion, for a different reason: no `$eq_` + helper is generated for that cross-namespace shape at all (the tag + is what goes wrong there), so this enumeration is still not the site + at fault, and no program reaches it with disagreeing tables. + """ + source = decl + """ + +private fn use_it(@Int -> @Option) + requires(true) + ensures(true) + effects(pure) +{ + Some(@Int.0) +} + +public fn main(@Unit -> @Int) + requires(true) + ensures(true) + effects(pure) +{ + 0 +} +""" + codes = [d.error_code for d in _check(source)] + assert expected in codes, codes + + +class TestRedeclaringAPreludeAdtNeverICEs: + """#1419 finding B — a legal redeclaration must not reach an internal + compiler error. + + §8.4.1 lets a program redeclare a prelude data type, including with + FEWER constructors. `_owned_ctor_layout` briefly raised + `CodegenInvariantError` when an owner-stamped reference named a + constructor its owner did not declare, and `private data Ordering { + Less, Equal }` + `show(compare(1, 2))` — check-clean and verify-clean — + became "Internal compiler error … Please file a bug report". The door + degrades to no-layout instead, so the caller's `CodegenSkip` reports the + construct and drops the function, which is what the compiler did before + #1414. + + What is NOT yet true, and is deliberately not asserted: that `compare` + still WORKS beside a user `Ordering`. Making it work needs the render + side to become owner-aware at the same time — resolving only the + constructor against the built-in table was measured producing a module + that fails to load, which is worse than the skip. That is the same + per-(owner, ADT, constructor) keying finding A needs. + """ + + @pytest.mark.parametrize("decl", [ + "private data Ordering { Less, Equal }", + "public data Ordering { Lt, Eq, Gt }", + "private data Ordering { Less, Equal, Greater }", + ]) + def test_no_internal_compiler_error(self, decl: str) -> None: + source = decl + """ + +public fn probe(@Unit -> @String) + requires(true) + ensures(true) + effects(pure) +{ + show(compare(1, 2)) +} +""" + assert not _check(source), [d.error_code for d in _check(source)] + result = _compile(source) + # Either it compiles, or it is refused with a located diagnostic — + # never an invariant violation. + for d in result.diagnostics: + assert "Internal compiler error" not in d.description, d.description + assert d.error_code != "E999", d.description + + +class TestNoUnannotatedBareConstructorLookup: + """#1414 — the STRUCTURAL rail: every constructor lookup that could + carry an owner must go through the one door. + + `WasmContext._owned_ctor_layout` is that door. Everything else in + `vera/wasm/` and `vera/smt.py` that reaches into the flat, by-name + `_ctor_layouts` map has to say why it cannot name an owner, with a + `# ctor-owner-exempt: ` marker — the same shape the repo already + uses for `# encoding-exempt` and `# diag-fields-exempt`. + + This is what the behavioural cells cannot do. Two of the three + wrong-value sites in this issue were found one at a time, by review, + after the first fix looked complete; a new bare lookup added tomorrow + would be invisible to every program-level test until someone wrote the + program that observes it. Here it is red immediately. + """ + + #: Every module that can reach a flat constructor projection — the whole + #: of `vera/wasm/` and `vera/codegen/` plus `vera/smt.py`, discovered by + #: globbing rather than listed, so a new module joins the rail by + #: existing. The previous form named seven files by hand and included + #: `vera/smt.py` for an attribute it does not use, which made its + #: listing vacuous while `vera/codegen/monomorphize.py` — which builds + #: its own flat ownership map — was outside the rail entirely (PR #1419 + #: review, finding C). + _DIRS = ("vera/wasm", "vera/codegen") + _EXTRA_FILES = ("vera/smt.py",) + #: All three flat projections, not just the layouts one: `_ctor_to_adt` + #: answers "which ADT owns this name" and `_ctor_adt_tp_indices` its + #: type-parameter positions, and both are keyed the same way. + _ATTRS = frozenset({ + "_ctor_layouts", "_ctor_to_adt", "_ctor_adt_tp_indices", + }) + #: The door itself, plus the constructors that store the maps. Matched + #: on the (class, function) pair, not the bare name, so an `__init__` + #: elsewhere cannot inherit the exemption. + _ALLOWED = frozenset({ + ("WasmContext", "_owned_ctor_layout"), + ("WasmContext", "__init__"), + }) + + def _files(self) -> list[str]: + from pathlib import Path as _P + + root = _P(__file__).resolve().parents[1] + out: list[str] = [] + for d in self._DIRS: + out += sorted( + str(f.relative_to(root)) for f in (root / d).glob("*.py")) + return out + list(self._EXTRA_FILES) + + @staticmethod + def _exempt_at(lines: list[str], lineno: int) -> bool: + """Is the access at *lineno* carrying an exemption marker? + + The marker may sit at the end of the access line, or — where that + would push the line past PEP 8, which most of the reasons do — in + the comment block immediately above it (PR #1419 review). Only a + CONTIGUOUS run of comment lines counts, so a marker cannot drift + away from the access it excuses and keep working. + """ + if "ctor-owner-exempt" in lines[lineno - 1]: + return True + i = lineno - 2 + while i >= 0 and lines[i].lstrip().startswith("#"): + if "ctor-owner-exempt" in lines[i]: + return True + i -= 1 + return False + + def _bare_lookups(self) -> list[tuple[str, int, str]]: + import ast as pyast + from pathlib import Path as _P + + root = _P(__file__).resolve().parents[1] + found: list[tuple[str, int, str]] = [] + for rel in self._files(): + src = (root / rel).read_text(encoding="utf-8") + lines = src.split("\n") + tree = pyast.parse(src) + spans: list[tuple[int, int, str, str]] = [] + for cls in pyast.walk(tree): + if not isinstance(cls, pyast.ClassDef): + continue + for fn in pyast.walk(cls): + if isinstance(fn, (pyast.FunctionDef, + pyast.AsyncFunctionDef)): + spans.append( + (fn.lineno, fn.end_lineno, cls.name, fn.name)) + for fn in pyast.walk(tree): + if isinstance(fn, (pyast.FunctionDef, pyast.AsyncFunctionDef)): + if not any(s[0] == fn.lineno for s in spans): + spans.append((fn.lineno, fn.end_lineno, "", fn.name)) + for node in pyast.walk(tree): + if not (isinstance(node, pyast.Attribute) + and node.attr in self._ATTRS): + continue + cls, fn_name = next( + ((c, f) for a, b, c, f in sorted(spans) + if a <= node.lineno <= b), + ("", ""), + ) + if (cls, fn_name) in self._ALLOWED: + continue + if self._exempt_at(lines, node.lineno): + continue + found.append((rel, node.lineno, f"{cls}.{fn_name}")) + return found + + def test_every_bare_lookup_is_the_door_or_annotated(self) -> None: + found = self._bare_lookups() + assert not found, ( + "constructor layouts resolved by bare name with no owner and no " + "`# ctor-owner-exempt:` reason — route through " + "`WasmContext._owned_ctor_layout`, or annotate why an owner is " + f"unavailable here: {found}" + ) + + def test_the_rail_is_not_vacuous(self) -> None: + """The walk must actually FIND the sites it is clearing. + + A rail that matched nothing — a renamed attribute, a moved file — + would pass silently forever. This asserts the walk still sees the + annotated population, so the cell above is known to be measuring + something. + """ + import ast as pyast + from pathlib import Path as _P + + root = _P(__file__).resolve().parents[1] + total = 0 + per_attr = {a: 0 for a in self._ATTRS} + for rel in self._files(): + tree = pyast.parse((root / rel).read_text(encoding="utf-8")) + for n in pyast.walk(tree): + if isinstance(n, pyast.Attribute) and n.attr in self._ATTRS: + total += 1 + per_attr[n.attr] += 1 + assert total >= 35, ( + f"only {total} flat-projection accesses found — the walk has " + "probably stopped matching") + # And EVERY attribute the rail claims to cover is actually present, + # so the set cannot quietly include a name nothing uses (which is + # what made `vera/smt.py`'s listing vacuous before). + assert all(per_attr.values()), per_attr + # And the door is one of them, so the rail is anchored on the very + # method it exists to protect. + door = pyast.parse( + (root / "vera/wasm/context.py").read_text(encoding="utf-8")) + assert any( + isinstance(n, pyast.FunctionDef) and n.name == "_owned_ctor_layout" + for n in pyast.walk(door) + ), "the owner-qualified door has been renamed or removed" + + +class TestCompareDesugaringIsOwnerKeyed: + """#1414 — the SMT desugaring of `compare` means `Ordering`'s + constructors, whatever the program declares. + + `_desugar_compare`'s docstring promises it "mirrors codegen's Pass 1.6 + exactly … so the verifier reasons over the SAME term the runtime + produces". That was untrue once codegen started stamping the three + references with their owner and the SMT copy did not: the SMT node had + no recorded type of its own (its span is the `compare(...)` call's), so + sort resolution fell through to a scan keyed on the bare constructor + name, which a user declaration captures. + """ + + _REFUTED = """\ +%s +public fn f(@Unit -> @Ordering) + requires(true) + ensures(@Ordering.result == Greater) + effects(pure) +{ + compare(1, 2) +} +""" + + @pytest.mark.parametrize("decl", [ + "", + "private data ZzBox { Less(Bool) }\n", + "private data ZzBox { Pad(Bool), Less }\n", + "private data ZzBox { A, B, C, Less }\n", + ]) + def test_a_refuted_postcondition_over_compare_is_violated( + self, decl: str, + ) -> None: + """`compare(1, 2)` is `Less`, so `ensures(result == Greater)` is + statically false and must be reported. + + Measured before the owner-keyed sort resolution: with any of the + colliding declarations present the obligation demoted to `tier3` + with NO diagnostic and `vera verify` exited 0 — a refuted + postcondition passing silently. The empty-declaration row is the + control that reported `violated` all along, so the cell cannot pass + by refusing everything. + """ + from tests.verifier_helpers import _verify + + result = _verify(self._REFUTED % decl) + ensures = [o for o in result.obligations if o.kind == "ensures"] + assert len(ensures) == 1, ensures + assert ensures[0].status == "violated", ( + f"a statically false postcondition demoted to " + f"{ensures[0].status!r} under {decl!r}") + assert "E500" in [ + d.error_code for d in result.diagnostics if d.severity == "error"] + + +class TestSiblingConstructorCollision: + """#1425 — constructor names are unique per NAMESPACE (spec §8.4). + + The intra-namespace sibling of E610 (two modules) and E157 (two + imports). Before it, two declarations sharing a constructor name were + accepted with no diagnostic, and a USE of the name produced `[E212]` / + `[E213]` describing whichever declaration registered last rather than + the collision — measured, `Rose { Leaf(T), Node(T, Rose) }` beside + `ZzBox { Node(Bool) }` gave "Constructor 'Node' expects 1 field(s), got + 2", the OTHER type's arity. + """ + + _FN = ( + "\n\npublic fn main(@Unit -> @Int)\n" + " requires(true)\n ensures(true)\n effects(pure)\n" + "{\n 0\n}\n" + ) + + @pytest.mark.parametrize("pair", [ + ("private data A1 { Pair(Int, Int) }", + "private data A2 { Pair(Bool, Bool) }"), + ("private data Rose { Leaf(T), Node(T, Rose) }", + "private data ZzBox { Node(Bool) }"), + ]) + def test_two_declarations_sharing_a_ctor_name_are_refused( + self, pair: tuple[str, str], + ) -> None: + first, second = pair + codes = [d.error_code for d in _check(first + "\n\n" + second + self._FN)] + assert codes == ["E159"], codes + # Order-independent: the rule is about the namespace, not the order. + codes = [d.error_code for d in _check(second + "\n\n" + first + self._FN)] + assert codes == ["E159"], codes + + @pytest.mark.parametrize("decl", [ + "private data Option { None, Some(T) }", + "private data Result { Ok(T), Err(E) }", + "private data Ordering { Less, Equal, Greater }", + ]) + def test_restating_a_prelude_type_is_not_a_collision( + self, decl: str, + ) -> None: + """The first legal shadowing shape, which E159 must not touch. + + §8.4.1 makes the prelude's data types ordinary declarations a + program may shadow, and `examples/vera/collections.vera` ships a + `public data Option { None, Some(T) }` that a rail keyed on + `env.constructors` — which already holds the prelude's entries by + registration time — would refuse. + """ + assert "E159" not in [d.error_code for d in _check(decl + self._FN)] + + def test_one_declaration_listing_many_constructors_is_fine(self) -> None: + assert "E159" not in [d.error_code for d in _check( + "private data A1 { P1(Int), P2(Bool), P3 }" + self._FN)] + + def test_shadowing_an_imported_constructor_is_not_a_collision( + self, tmp_path: Path, + ) -> None: + """The second legal shadowing shape (§8.5.2). + + A local declaration shadows an imported constructor; that is one + declaration in this namespace and one in another, not two here. + """ + from tests.module_fixture_helpers import build_multi_module + + lib = ( + "module shapelib;\n\n" + "public data Shape { Sq(Int), Ci(Int) }\n\n" + "public fn mk(@Int -> @Shape)\n" + " requires(true)\n ensures(true)\n effects(pure)\n" + "{\n Sq(@Int.0)\n}\n" + ) + main = ( + "import shapelib;\n\n" + "private data Local { Sq(Bool) }\n\n" + "public fn main(@Unit -> @Int)\n" + " requires(true)\n ensures(true)\n effects(pure)\n" + "{\n 7\n}\n" + ) + # Raises on a check error, so reaching the assert IS the property. + verify_errors, _result, cg = build_multi_module( + tmp_path, {"shapelib.vera": lib, "main.vera": main}) + assert not verify_errors and not cg, (verify_errors, cg) + + class TestPreludeNamespaceScope: """A main-file shadow reaches the main file's bodies and nothing else.""" diff --git a/vera/README.md b/vera/README.md index 079ea197e..bfab7a08c 100644 --- a/vera/README.md +++ b/vera/README.md @@ -85,7 +85,7 @@ execute(compile_result, ...) # → run WASM via wasmtime | ` core.py` | 1,407 | | TypeChecker class, orchestration, contracts, constraint validation | | | ` resolution.py` | 535 | | AST TypeExpr → semantic Type, inference | | | ` modules.py` | 534 | | 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` | 1,032 | | Pass 1 forward declarations, ability registration | | +| ` registration.py` | 1,188 | | Pass 1 forward declarations, ability registration | | | ` expressions.py` | 1,485 | | Expression synthesis (bidirectional), operators, statements | | | ` eq_ability.py` | 226 | | Eq ability derivation checks | | | ` sql.py` | 309 | | SQL literal-provenance resolution + placeholder counting (#309) | `resolve_literal_string()`, `count_placeholders()` | @@ -767,11 +767,11 @@ Every diagnostic has a unique code grouped by compiler phase: | E5xx | Verification | `verifier.py` | | E6xx | Codegen | `codegen/` | -The `ERROR_CODES` dict in `errors.py` maps every code to a short description (173 entries — 170 `E` codes and 3 `W` warning codes). Codes are stable across versions — they can be used for programmatic filtering, suppression, and documentation lookups. Formatted output shows the code in brackets: `[E130] Error at line 5, column 3:`. +The `ERROR_CODES` dict in `errors.py` maps every code to a short description (174 entries — 171 `E` codes and 3 `W` warning codes). Codes are stable across versions — they can be used for programmatic filtering, suppression, and documentation lookups. Formatted output shows the code in brackets: `[E130] Error at line 5, column 3:`. ## Test Suite -Testing spans a **pytest suite** of 13,517 tests across 203 files: compiler-internals unit tests plus a **conformance suite** (251 programs in `tests/conformance/` validating every language feature against the spec) and **example programs** (43 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 13,575 tests across 203 files: compiler-internals unit tests plus a **conformance suite** (253 programs in `tests/conformance/` validating every language feature against the spec) and **example programs** (43 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/_since.py b/vera/_since.py index 8f9340e6e..1d0ec4042 100644 --- a/vera/_since.py +++ b/vera/_since.py @@ -270,6 +270,7 @@ "E156": "0.1.12", "E157": "0.1.12", "E158": "0.2.0", + "E159": "0.2.0", "E160": "0.0.43", "E161": "0.0.43", "E170": "0.0.43", diff --git a/vera/ast.py b/vera/ast.py index d7d65f6ba..29a08ed86 100644 --- a/vera/ast.py +++ b/vera/ast.py @@ -444,6 +444,19 @@ class ConstructorCall(Expr): class NullaryConstructor(Expr): """Nullary constructor expression: None.""" name: str + #: The ADT this reference resolves to, when the COMPILER generated the + #: node and already knows (#1414). A parsed reference leaves it `None` + #: and is resolved by name, as before. + #: + #: Code generation keys constructor ownership on a flat by-name table + #: built across every ADT, so a user `data ZzBox { Less(Bool) }` takes + #: the `Less` entry away from `Ordering` — and the desugaring of + #: `compare(a, b)`, which emits bare `Less` / `Equal` / `Greater`, then + #: rendered every `Ordering` in the program as the user's constructor. + #: Those three references are the compiler's own and mean `Ordering` + #: whatever the program declares, so they say so structurally rather + #: than relying on a name lookup that a declaration can move. + owner: str | None = None @dataclass(frozen=True) diff --git a/vera/checker/registration.py b/vera/checker/registration.py index 6fd54cdd2..f3cb81dd2 100644 --- a/vera/checker/registration.py +++ b/vera/checker/registration.py @@ -234,6 +234,16 @@ class RegistrationMixin: def _register_all(self, program: ast.Program) -> None: """Register all top-level declarations (forward reference support).""" + # #1425: constructor names are unique per NAMESPACE, not per data + # type (spec §8.4). This pass IS one namespace — the entry program + # here, a module's own declarations on the temporary checker + # `modules.py` builds — so tracking what this pass declares is + # exactly the right scope, and it deliberately does not consult + # `env.constructors`, which already holds the prelude's and the + # imports' entries by the time registration runs. Shadowing one of + # those stays legal (§8.4.1, §8.5.2); declaring the same name twice + # HERE does not. + self._ns_ctor_owners: dict[str, str] = {} for tld in program.declarations: # C7c: require explicit visibility on fn/data declarations if (tld.visibility is None @@ -934,22 +944,33 @@ def _check_special_cased_builtin_adt( """ if name not in self._SPECIAL_CASED_BUILTIN_ADTS: return - subject = ( - "redeclared as a data type" if kind == "data type" - else "used as a constructor name" - ) - self._error( - node, - f"'{name}' is a built-in type whose meaning the compiler " - f"special-cases, so it cannot be {subject}.", - rationale=( + if kind == "data type": + subject = "redeclared as a data type" + rationale = ( f"Unlike the prelude's data types, which a program may " f"shadow, '{name}' is recognised by name throughout " f"code generation — how it is rendered, compared and laid " f"out. A declaration of that name cannot be told apart from " f"the built-in, so the program would compile against a " f"mixture of the two." - ), + ) + else: + subject = "used as a constructor name" + rationale = ( + f"Constructor layouts are held in one table keyed by " + f"constructor name across every data type, so a " + f"constructor called '{name}' displaces the built-in's " + f"entry rather than sitting beside it. The declared " + f"constructor is then unreachable — a '{name}(...)' call " + f"still resolves to the built-in — while the built-in's own " + f"uses elsewhere in the program are compiled against this " + f"declaration's layout." + ) + self._error( + node, + f"'{name}' is a built-in type whose meaning the compiler " + f"special-cases, so it cannot be {subject}.", + rationale=rationale, fix=( f"Rename the {kind}. If you meant the built-in " f"'{name}', use it directly instead of declaring it." @@ -958,6 +979,57 @@ def _check_special_cased_builtin_adt( error_code="E158", ) + def _check_sibling_ctor_collision( + self, ctor: ast.Constructor, owner: str, + ) -> None: + """Refuse two data declarations in one namespace sharing a + constructor name (#1425, spec §8.4). + + The intra-namespace sibling of E610 (two modules) and E157 (two + imports). Spec §8.4 puts all three under one rule — a constructor + name clash is "rejected at check time, in whichever namespace holds + the clash: the entry program's, or any module's" — and this is the + namespace that had no rail. + + Accepting it was not merely untidy: resolution is by bare name with + the last declaration winning, so the pair produced diagnostics that + named neither declaration (`[E212] Constructor 'Node' expects 1 + field(s), got 2` — the OTHER type's arity) and, before #1414's + per-owner layout keying, a silently wrong value. + + Deliberately NOT fired for the two shadowing shapes §8.4.1 and + §8.5.2 make legal, neither of which is a second declaration in this + namespace: restating a PRELUDE type (``examples/vera/ + collections.vera`` declares `None` and `Some`), and shadowing an + IMPORTED constructor. + """ + first = self._ns_ctor_owners.get(ctor.name) + if first is None: + self._ns_ctor_owners[ctor.name] = owner + return + if first == owner: + return # the same declaration listing it twice is E211's job + self._error( + ctor, + f"Constructor '{ctor.name}' is already declared by data type " + f"'{first}' in this file.", + rationale=( + f"Constructor names are resolved by name alone, so one " + f"namespace cannot hold two constructors called " + f"'{ctor.name}' — a call could not say which type it " + f"builds, and the diagnostics it produces would describe " + f"whichever declaration was registered last rather than " + f"the collision itself." + ), + fix=( + f"Rename this constructor, or rename '{first}'s. The rule " + f"is two declarations in ONE file; shadowing a prelude " + f"type's constructor stays legal." + ), + spec_ref='Chapter 8, Section 8.4 "Visibility"', + error_code="E159", + ) + def _register_data( self, decl: ast.DataDecl, visibility: str | None = None, ) -> None: @@ -982,6 +1054,14 @@ def _register_data( self._check_special_cased_builtin_adt( ctor, ctor.name, "constructor", ) + self._check_sibling_ctor_collision(ctor, decl.name) + if ctor.name in self._SPECIAL_CASED_BUILTIN_ADTS: + # Registration continues past `_error` so the rest of the + # declaration still reports, but a REFUSED constructor must + # not land in `env.constructors` — nothing downstream should + # be able to resolve a name the checker has just rejected + # (PR #1404 review). + continue field_types = None if ctor.fields is not None: field_types = tuple( diff --git a/vera/codegen/closures.py b/vera/codegen/closures.py index 2c55336f0..832a17942 100644 --- a/vera/codegen/closures.py +++ b/vera/codegen/closures.py @@ -324,6 +324,10 @@ def _compile_lifted_closure( ctx = WasmContext( self.string_pool, ctor_layouts=ctor_layouts, + # #1414: the LIVE nested map, not a copy of it — the flat + # `ctor_layouts` above is already derived from it, and a + # third copy is one more thing to drift (PR #1419 review). + adt_ctor_layouts=self._adt_layouts, # #1253/#1316: the namespace's data types, as in `functions.py` # — a lifted closure body belongs to the declaration that # contains it, so it resolves names in that declaration's scope. diff --git a/vera/codegen/core.py b/vera/codegen/core.py index 0e6b21195..8bb5941c2 100644 --- a/vera/codegen/core.py +++ b/vera/codegen/core.py @@ -302,6 +302,8 @@ def __init__( # indices (or None for concrete fields). Used by the monomorphizer and WASM # type inference to correctly bind forall vars from sparse constructors like # Err(e) whose single field maps to Result's *second* type param (E), not T. + # ctor-owner-exempt: declares the flat projection; the per-owner map is + # built from it self._ctor_adt_tp_indices: dict[str, tuple[int | None, ...]] = {} # Maps ADT name → number of type parameters (needed to produce full-length # type-arg tuples with None placeholders for unknown positions). @@ -3556,7 +3558,8 @@ def _rewrite_ops_in_expr( then_branch=ast.Block( statements=(), span=expr.span, expr=ast.NullaryConstructor( - name="Less", span=expr.span), + name="Less", span=expr.span, + owner="Ordering"), ), else_branch=ast.Block( statements=(), span=expr.span, @@ -3568,12 +3571,14 @@ def _rewrite_ops_in_expr( then_branch=ast.Block( statements=(), span=expr.span, expr=ast.NullaryConstructor( - name="Equal", span=expr.span), + name="Equal", span=expr.span, + owner="Ordering"), ), else_branch=ast.Block( statements=(), span=expr.span, expr=ast.NullaryConstructor( - name="Greater", span=expr.span), + name="Greater", span=expr.span, + owner="Ordering"), ), span=expr.span, ), diff --git a/vera/codegen/functions.py b/vera/codegen/functions.py index deea3a2b2..2e5bbf325 100644 --- a/vera/codegen/functions.py +++ b/vera/codegen/functions.py @@ -454,6 +454,10 @@ def _compile_fn( effect_op_cells=effect_op_cells, state_getters=state_getters, ctor_layouts=ctor_layouts, + # #1414: the LIVE nested map, not a copy of it — the flat + # `ctor_layouts` above is already derived from it, and a + # third copy is one more thing to drift (PR #1419 review). + adt_ctor_layouts=self._adt_layouts, adt_type_names=adt_type_names, generic_fn_info=getattr(self, "_generic_fn_info", None), generic_constrained_vars=getattr( diff --git a/vera/codegen/modules.py b/vera/codegen/modules.py index ed654ce9d..71ad198d1 100644 --- a/vera/codegen/modules.py +++ b/vera/codegen/modules.py @@ -711,9 +711,15 @@ def _register_modules(self, program: ast.Program) -> None: self._adt_tp_counts.setdefault( adt_name, temp._adt_tp_counts[adt_name]) for _ctor_name in layouts: + # ctor-owner-exempt: builds the flat projection handed + # to the wasm layer if _ctor_name in temp._ctor_adt_tp_indices: + # ctor-owner-exempt: builds the flat projection + # handed to the wasm layer self._ctor_adt_tp_indices.setdefault( _ctor_name, + # ctor-owner-exempt: builds the flat projection + # handed to the wasm layer temp._ctor_adt_tp_indices[_ctor_name]) self._needs_alloc = True self._needs_memory = True diff --git a/vera/codegen/monomorphize.py b/vera/codegen/monomorphize.py index e2e5707fa..b0f05d2d1 100644 --- a/vera/codegen/monomorphize.py +++ b/vera/codegen/monomorphize.py @@ -1663,6 +1663,9 @@ def _adt_satisfies_eq( tp_names = self._adt_tp_param_names.get(base, ()) tp_mapping = dict(zip(tp_names, args)) for ctor_name, layout in layouts.items(): + # ctor-owner-exempt: no owner in hand at this read; unreached by + # all 289 corpus programs and the ambiguous shapes are E213/E121 at + # check — the owner-qualified table is #1436's tp_indices = self._ctor_adt_tp_indices.get(ctor_name) for i, (_offset, wasm_type) in enumerate(layout.field_offsets): tp_i = ( diff --git a/vera/codegen/registration.py b/vera/codegen/registration.py index 2e026eb42..343ab2c00 100644 --- a/vera/codegen/registration.py +++ b/vera/codegen/registration.py @@ -295,9 +295,17 @@ def _register_builtin_adts(self) -> None: # for concrete (non-type-variable) fields. This lets the monomorphizer # and WASM type inference correctly bind Err(e) to E (index 1 in # Result), not to T (index 0) as naïve positional zipping would do. + # ctor-owner-exempt: registers the built-in layouts; no user owner + # exists yet self._ctor_adt_tp_indices["None"] = () # Option: no fields + # ctor-owner-exempt: registers the built-in layouts; no user owner + # exists yet self._ctor_adt_tp_indices["Some"] = (0,) # field 0 → T (index 0) + # ctor-owner-exempt: registers the built-in layouts; no user owner + # exists yet self._ctor_adt_tp_indices["Ok"] = (0,) # field 0 → T (index 0) + # ctor-owner-exempt: registers the built-in layouts; no user owner + # exists yet self._ctor_adt_tp_indices["Err"] = (1,) # field 0 → E (index 1) self._adt_tp_counts["Option"] = 1 self._adt_tp_counts["Result"] = 2 @@ -342,8 +350,13 @@ def _register_data(self, decl: ast.DataDecl) -> None: indices.append(tp_index[field_te.name]) else: indices.append(None) + # ctor-owner-exempt: keyed by bare ctor name, so a user + # declaration overwrites a built-in's entry; owner-keying it is + # #1436 self._ctor_adt_tp_indices[ctor.name] = tuple(indices) else: + # ctor-owner-exempt: same by-name write as above; owner-keying + # it is #1436 self._ctor_adt_tp_indices[ctor.name] = () def _compute_constructor_layout( diff --git a/vera/errors.py b/vera/errors.py index 1dd8bd47a..98d2ba379 100644 --- a/vera/errors.py +++ b/vera/errors.py @@ -946,6 +946,7 @@ def diagnose_lark_error( "E156": "Bare data type name supplied by two imports", "E157": "Bare constructor name supplied by two imports", "E158": "Declaration reuses a special-cased built-in ADT name", + "E159": "Two data declarations share a constructor name", "E160": "Array index must be Int or Nat", "E161": "Cannot index non-array type", "E170": "Let binding type mismatch", diff --git a/vera/smt.py b/vera/smt.py index 2d592d778..2782303f3 100644 --- a/vera/smt.py +++ b/vera/smt.py @@ -553,6 +553,8 @@ def __init__( self._adt_registry: dict[str, AdtInfo] = {} self._adt_registry_version = 0 self._regularity: tuple[int, RegularityIndex] | None = None + # ctor-owner-exempt: declares the SMT ADT registry, which is + # namespace-flat by design self._ctor_to_adt: dict[str, str] = {} # ctor name → ADT name self._z3_sorts: dict[str, z3.SortRef] = {} # "List" → Z3 sort @@ -750,6 +752,9 @@ def register_adt(self, adt_info: AdtInfo) -> None: # could not. self._adt_registry_version += 1 for ctor_name in adt_info.constructors: + # ctor-owner-exempt: the SMT ADT registry is namespace-flat, and a + # `ConstructorCall` carries no owner to qualify by — only the + # NULLARY path is owner-first (#1436) self._ctor_to_adt[ctor_name] = adt_info.name def _regularity_index(self) -> RegularityIndex: @@ -1748,6 +1753,13 @@ def _desugar_compare(call: ast.FnCall) -> ast.Expr: Mirrors codegen's Pass 1.6 exactly (#874): if a < b then Less else if a == b then Equal else Greater so the verifier reasons over the SAME term the runtime produces. + + "Exactly" includes the constructors' OWNER (#1414): codegen stamps + these three references with ``Ordering`` so a user declaration + sharing one of the names cannot capture them by bare name, and a + desugaring that left them ownerless would reason about a different + type than the one that runs — which is precisely the divergence + this docstring promises does not exist. """ left, right = call.args[0], call.args[1] return ast.IfExpr( @@ -1756,7 +1768,8 @@ def _desugar_compare(call: ast.FnCall) -> ast.Expr: ), then_branch=ast.Block( statements=(), span=call.span, - expr=ast.NullaryConstructor(name="Less", span=call.span), + expr=ast.NullaryConstructor( + name="Less", span=call.span, owner="Ordering"), ), else_branch=ast.Block( statements=(), span=call.span, @@ -1768,12 +1781,14 @@ def _desugar_compare(call: ast.FnCall) -> ast.Expr: then_branch=ast.Block( statements=(), span=call.span, expr=ast.NullaryConstructor( - name="Equal", span=call.span), + name="Equal", span=call.span, + owner="Ordering"), ), else_branch=ast.Block( statements=(), span=call.span, expr=ast.NullaryConstructor( - name="Greater", span=call.span), + name="Greater", span=call.span, + owner="Ordering"), ), span=call.span, ), @@ -2952,6 +2967,9 @@ def _find_sort_for_ctor( ``Option`` is cached) is still materialised — that path is the #918 fix and must keep working. """ + # ctor-owner-exempt: the SMT ADT registry is namespace-flat, and a + # `ConstructorCall` carries no owner to qualify by — only the NULLARY + # path is owner-first (#1436) adt_name = self._ctor_to_adt.get(ctor_name) if adt_name is None: return None @@ -3121,6 +3139,9 @@ def _ctor_instantiation_from_args( can't bind every parameter — in which case the caller keeps the base-name scan. """ + # ctor-owner-exempt: the SMT ADT registry is namespace-flat, and a + # `ConstructorCall` carries no owner to qualify by — only the NULLARY + # path is owner-first (#1436) adt_name = self._ctor_to_adt.get(ctor_name) if adt_name is None: return None @@ -3204,7 +3225,20 @@ def _translate_nullary_ctor( no hint is available (nullary tags in a non-verifier / pure-SMT context, or a hint that does not resolve to a datatype sort owning this ctor). """ - sort = self._nullary_ctor_sort_from_hint(expr) + # #1414: an OWNER-stamped reference is the compiler's own, and says + # which ADT it means. It is consulted before the recorded-type hint + # and the base-name scan, because a desugared node has no recorded + # type of its own (its span is the `compare(...)` call's) and the + # scan resolves by bare constructor name — so a user + # `data ZzBox { Pad(Bool), Less }` captured the `Less` that + # `_desugar_compare` emits, the term came back wrongly sorted or + # untranslatable, and a statically REFUTED postcondition over + # `compare` demoted to Tier 3 with exit 0 instead of reporting E500. + sort = None + if expr.owner is not None: + sort = self._get_or_create_adt_sort(expr.owner, ()) + if sort is None: + sort = self._nullary_ctor_sort_from_hint(expr) if sort is None: sort = self._find_sort_for_ctor(expr.name) if sort is None: @@ -3337,6 +3371,9 @@ def _translate_ctor_call( # up rather than crash: an untranslatable ctor is a Tier-3 # demotion the callers already handle, which is what every other # `return None` on this path means. + # ctor-owner-exempt: the SMT ADT registry is namespace-flat, and a + # `ConstructorCall` carries no owner to qualify by — only the + # NULLARY path is owner-first (#1436) adt_name = self._ctor_to_adt.get(expr.name) exact = ( self._get_or_create_adt_sort(adt_name, type_args) diff --git a/vera/wasm/calls.py b/vera/wasm/calls.py index f3d933ac1..8d5f335e4 100644 --- a/vera/wasm/calls.py +++ b/vera/wasm/calls.py @@ -679,6 +679,8 @@ def _translate_call( # in `_known_fns`. if (self._known_fns and call_target not in self._known_fns + # ctor-owner-exempt: membership test on a parsed call target, + # not a layout read and call_target not in self._ctor_layouts): raise CodegenSkip( call, diff --git a/vera/wasm/calls_handlers.py b/vera/wasm/calls_handlers.py index 5c21f775e..9127a0a67 100644 --- a/vera/wasm/calls_handlers.py +++ b/vera/wasm/calls_handlers.py @@ -414,6 +414,7 @@ def _recover_ctor_ptype( tp_count = self._adt_tp_counts.get(adt_name, 0) if tp_count == 0: return None # non-generic ADT — bare name already correct + # ctor-owner-exempt: no owner available at this site field_tp_idx = self._ctor_adt_tp_indices.get(arg.name) if field_tp_idx is None: return None @@ -459,7 +460,26 @@ def _recover_ptype_via_nested_fields( tp_names = self._adt_tp_param_names.get(adt_name, ()) # Parent parameter NAME → its slot index (`T` → 0). name_to_slot = {name: i for i, name in enumerate(tp_names)} - layout = self._ctor_layouts.get(arg.name) + # #1414: prefer the OWNER-qualified layout. `adt_name` is the ADT + # whose parameters this pass is recovering, so its own table answers + # for `arg.name`; the flat by-name map would hand back another ADT's + # layout after a same-named constructor collision and the recovered + # generic type would be built from the wrong `field_types`. LATENT + # today rather than a live miscompile, and for a reason worth + # stating exactly: the CHECKER resolves a constructor call through + # the same last-declaration-wins by-name rule, so whenever the flat + # map here holds the wrong ADT's layout the checker has already + # refused the call against that same wrong resolution — measured, + # `data Rose { Leaf(T), Node(T, Rose) }` followed by + # `data ZzBox { Node(Bool) }` makes `Node(1, Leaf(2))` an `[E212]` + # ("expects 1 field(s), got 2"), while the reverse declaration + # order leaves Rose in the slot and compiles. Two layers being + # wrong the same way is a coincidence, not a rail, which is exactly + # why this read is owner-qualified: the next change to either + # resolution would inherit the wrong layout silently. The flat map + # stays as the fallback for a namespace whose per-owner table was + # not threaded (PR #1419 review). + layout = self._owned_ctor_layout(adt_name, arg.name) field_types = layout.field_types if layout else () for field_i, decl in enumerate(field_types): if field_i >= len(arg.args): @@ -612,20 +632,33 @@ def _composite_ctor_plans( tp_names = self._adt_tp_param_names.get(base, ()) tp_mapping = dict(zip(tp_names, type_args)) - ctors = sorted( - ( - (cname, self._ctor_layouts[cname]) - for cname, parent in self._ctor_to_adt.items() - if parent == base and cname in self._ctor_layouts - ), - key=lambda x: x[1].tag, - ) + # #1414: read the layouts of the ADT we are rendering, not whatever + # the flat by-name table happens to hold. Both tables here are keyed + # by bare constructor name across every ADT, so a user declaration + # sharing one of this type's constructor names displaced BOTH the + # layout and the `_ctor_to_adt` ownership entry — measured, a + # `data ZzBox { Less(Bool) }` anywhere in the program dropped + # `Ordering`'s own `Less` out of this list and rendered every + # `Ordering` as the user's constructor. The per-owner map answers + # for the type actually being rendered; the flat one is the fallback + # for a namespace whose layouts were not threaded. + # The flat-map fallback that used to sit here was instrumented over + # the full pytest suite, the conformance suite twice (the second + # under VERA_EAGER_GC=1), the examples' check/verify and run gates, + # and a compile of all 302 corpus programs: reached zero times. It + # is gone rather than kept as a comfort branch, because re-resolving + # by bare name is the defect this method was fixed for. + own = self._adt_ctor_layouts.get(base) + if own is None: + return None + ctors = sorted(own.items(), key=lambda x: x[1].tag) if not ctors: return None plans: list[tuple[str, int, list[tuple[int, str, str]]]] = [] for cname, layout in ctors: n_fields = len(layout.field_offsets) + # ctor-owner-exempt: owner-qualified above; parsed-name path tp_idx = self._ctor_adt_tp_indices.get(cname) raw_types = ( layout.field_types diff --git a/vera/wasm/context.py b/vera/wasm/context.py index 77c46976c..7b3cac430 100644 --- a/vera/wasm/context.py +++ b/vera/wasm/context.py @@ -98,6 +98,9 @@ def __init__( effect_op_cells: dict[str, CellNames] | None = None, state_getters: dict[str, str] | None = None, ctor_layouts: dict[str, ConstructorLayout] | None = None, + adt_ctor_layouts: ( + dict[str, dict[str, ConstructorLayout]] | None + ) = None, adt_type_names: set[str] | None = None, generic_fn_info: ( dict[str, tuple[tuple[str, ...], tuple[ast.TypeExpr, ...]]] | None @@ -212,6 +215,19 @@ def __init__( self._clause_inline_depth: int = 0 # Constructor layout mapping: ctor_name -> ConstructorLayout self._ctor_layouts: dict[str, ConstructorLayout] = ctor_layouts or {} + # #1414: the same layouts keyed per OWNING ADT, because the flat map + # above cannot represent two data types sharing a constructor name — + # it is built by `update()` across every ADT, so the last declaration + # registered wins the slot outright. §8.4.1 makes the prelude's data + # types shadowable, so that collision is a legal program: a user + # `data ZzBox { Less(Bool) }` was measured making EVERY `Ordering` in + # the program render as `Less(false)`, check-clean and verify-clean. + # A site that knows which ADT it means reads this map; one that has + # only a bare constructor name (an ordinary `Some(x)` call, which the + # checker has already resolved) keeps the flat one. + self._adt_ctor_layouts: dict[str, dict[str, ConstructorLayout]] = ( + adt_ctor_layouts or {} + ) # ADT type names for slot/param type resolution self._adt_type_names: set[str] = adt_type_names or set() # Generic function info for call rewriting: @@ -550,6 +566,53 @@ def __init__( dict[tuple[int, int, int, int], object] | None ) = None + def _owned_ctor_layout( + self, owner: str | None, ctor_name: str, + ) -> "ConstructorLayout | None": + """The layout of *ctor_name* as owned by *owner* (#1414). + + The single door every constructor lookup that KNOWS its owner goes + through, so the reader and the writer cannot disagree about which + ADT a name belongs to. Falls back to the flat by-name table only + when there is no owner to qualify by — a parsed reference the + checker has already resolved — or when the owner's table was not + threaded into this context. + """ + if owner is None: + # A PARSED reference, which the checker has already resolved; + # there is no owner to qualify by and the flat map is the only + # answer. This is the common path. + # ctor-owner-exempt: the documented no-owner path + return self._ctor_layouts.get(ctor_name) + # An owner-stamped reference whose owner does not declare the name + # returns NO layout. It is not a compiler bug and must not raise: + # a program may legally redeclare a prelude type with FEWER + # constructors (`private data Ordering { Less, Equal }` is + # check-clean and verify-clean, §8.4.1), and the `compare` + # desugaring still emits an owner-stamped `Greater` that the + # program's own `Ordering` has no arm for. An earlier form of this + # method raised `CodegenInvariantError` there and turned that + # program into an internal compiler error, where the caller's + # `CodegenSkip` degrades it cleanly — the behaviour it had before + # #1414 (PR #1419 review, finding B). + # + # Nor does it fall back to the flat by-name map: re-resolving an + # owner-stamped reference by bare name is the defect this method + # exists to prevent, and doing it here would reintroduce it at the + # one site that knows better. Returning None keeps that policy the + # same as `_recover_ptype_via_nested_fields`'s (finding D). + # NOTE: resolving an owner-stamped reference against the BUILT-IN + # snapshot first was tried and reverted. It repairs the + # constructor's layout but not the RENDER side, which enumerates + # `Ordering` out of the same ADT-name-keyed map and gets the user's + # constructors — the two then disagree and the module fails to + # load, which is worse than the clean skip below. Both sides have + # to become owner-aware together; see #1419's finding A/B note. + own = self._adt_ctor_layouts.get(owner) + if own is not None and ctor_name in own: + return own[ctor_name] + return None + def set_expr_semantic_types( self, types: dict[tuple[int, int, int, int], object] | None, diff --git a/vera/wasm/data.py b/vera/wasm/data.py index 2c69f09b3..ea00cbdf4 100644 --- a/vera/wasm/data.py +++ b/vera/wasm/data.py @@ -42,6 +42,8 @@ def _ctor_field_tp_index(self, ctor_name: str, index: int) -> int | None: consumer asking "is this field generic, and which parameter is it?" reads it through here rather than indexing the table itself. """ + # ctor-owner-exempt: the shared by-name reader; callers hold the owner, + # the table does not (#1436) tp_idx = self._ctor_adt_tp_indices.get(ctor_name) if tp_idx is None or index >= len(tp_idx): return None @@ -160,7 +162,14 @@ def _translate_nullary_constructor( Emits: alloc → store tag → return pointer. """ - layout = self._ctor_layouts.get(expr.name) + # #1414: the TAG comes from the same table the value will be READ + # through. Converting only the reader left a compiler-emitted + # `Less` tagged out of the USER's ADT and rendered out of + # `Ordering`'s — agreeing only where the shadowing constructor + # happens to sit at its namesake's index. Measured on that + # half-fix: `data ZzBox { Pad(Bool), Less }` made `compare(1, 2)` + # render `Equal`, and `{ A, B, C, Less }` made it `Greater`. + layout = self._owned_ctor_layout(expr.owner, expr.name) if layout is None: raise CodegenSkip( expr, f"unknown nullary constructor {expr.name!r}" @@ -188,6 +197,8 @@ def _translate_constructor_call( generic constructors (e.g. Some(T) instantiated as Some(Int)) use the correct WASM types and alignment. """ + # ctor-owner-exempt: a parsed call; the checker resolved it WITHIN its + # namespace — the flat map is still cross-namespace (#1436) layout = self._ctor_layouts.get(expr.name) if layout is None: raise CodegenSkip( @@ -403,6 +414,7 @@ def _ctor_field_targets_byte( unthreaded, or the target carries no matching argument — the literal then keeps its i64 translation (the pre-#1092 behaviour). """ + # ctor-owner-exempt: no owner available at this site tp_idx = self._ctor_adt_tp_indices.get(expr.name) if not tp_idx or field_i >= len(tp_idx): return False @@ -987,6 +999,8 @@ def _translate_match_condition( """ if isinstance(pattern, (ast.NullaryPattern, ast.ConstructorPattern)): name = pattern.name + # ctor-owner-exempt: a parsed pattern; checker-resolved within its + # namespace only — cross-namespace is #1436 layout = self._ctor_layouts.get(name) if layout is None: raise CodegenSkip( @@ -1245,6 +1259,8 @@ def _setup_match_arm_env( return (instrs, new_env) if isinstance(pattern, ast.ConstructorPattern): + # ctor-owner-exempt: a parsed pattern; checker-resolved within its + # namespace only — cross-namespace is #1436 layout = self._ctor_layouts.get(pattern.name) if layout is None: raise CodegenSkip( @@ -1443,6 +1459,8 @@ def _extract_constructor_fields( # look up its layout, and recurse to extract its fields. align = _aligns.get("i32", 4) offset = (offset + align - 1) & ~(align - 1) + # ctor-owner-exempt: a parsed pattern; checker-resolved within + # its namespace only — cross-namespace is #1436 sub_layout = self._ctor_layouts.get(sub_pat.name) if sub_layout is None: raise CodegenSkip( @@ -1639,6 +1657,8 @@ def _resolve_nested_scrutinee_type( outer instantiation is missing; the nested walk then LOUD-skips any type-parameter wildcard rather than reading a wrong offset. """ + # ctor-owner-exempt: a parsed sub-pattern; checker-resolved within its + # namespace only — cross-namespace is #1436 layout = self._ctor_layouts.get(ctor_name) if layout is None or field_index >= len(layout.field_types): return None @@ -1646,6 +1666,8 @@ def _resolve_nested_scrutinee_type( base, type_args = self._split_param_type(scrutinee_type or "") tp_names = self._adt_tp_param_names.get(base, ()) tp_mapping = dict(zip(tp_names, type_args)) + # ctor-owner-exempt: a parsed sub-pattern; checker-resolved within its + # namespace only — cross-namespace is #1436 tp_idx = self._ctor_adt_tp_indices.get(ctor_name) return self._resolve_field_type_for_eq( raw, field_index, tp_idx, type_args, tp_mapping, @@ -1705,6 +1727,8 @@ def _collect_nested_tag_checks( if isinstance(sub_pat, (ast.ConstructorPattern, ast.NullaryPattern)): name = sub_pat.name + # ctor-owner-exempt: a parsed sub-pattern; checker-resolved + # within its namespace only — cross-namespace is #1436 sub_layout = self._ctor_layouts.get(name) if sub_layout is None: raise CodegenSkip( diff --git a/vera/wasm/inference.py b/vera/wasm/inference.py index 8a1c876d6..2f72f0d52 100644 --- a/vera/wasm/inference.py +++ b/vera/wasm/inference.py @@ -201,8 +201,12 @@ def _infer_expr_wasm_type(self, expr: ast.Expr) -> str | None: if isinstance(expr, ast.FnCall): return self._infer_fncall_wasm_type(expr) if isinstance(expr, ast.ConstructorCall): + # ctor-owner-exempt: membership test on a parsed name, not a layout + # read return "i32" if expr.name in self._ctor_layouts else None if isinstance(expr, ast.NullaryConstructor): + # ctor-owner-exempt: membership test on a parsed name, not a layout + # read return "i32" if expr.name in self._ctor_layouts else None if isinstance(expr, ast.MatchExpr): # #1276 (F4): the FIRST arm that yields a type, not arm 0. An arm @@ -641,8 +645,12 @@ def _infer_block_result_type(self, block: ast.Block) -> str | None: if isinstance(expr, ast.Block): return self._infer_block_result_type(expr) if isinstance(expr, ast.ConstructorCall): + # ctor-owner-exempt: membership test on a parsed name, not a layout + # read return "i32" if expr.name in self._ctor_layouts else None if isinstance(expr, ast.NullaryConstructor): + # ctor-owner-exempt: membership test on a parsed name, not a layout + # read return "i32" if expr.name in self._ctor_layouts else None if isinstance(expr, ast.MatchExpr): # #1276 (F4): the first arm that yields a type — see the twin arm @@ -1064,7 +1072,12 @@ def _walk_vera_type(self, expr: ast.Expr) -> str | None: if isinstance(expr, ast.ConstructorCall): return self._ctor_to_adt_name(expr.name) if isinstance(expr, ast.NullaryConstructor): - return self._ctor_to_adt_name(expr.name) + # #1414: a compiler-generated reference already knows its ADT. + # The by-name lookup below reads a table flattened across every + # ADT, so a user declaration sharing the name would answer for + # it — which is how `compare`'s desugared `Less` came back as + # the user's `ZzBox`. + return expr.owner or self._ctor_to_adt_name(expr.name) if isinstance(expr, ast.BinaryExpr): if expr.op in (ast.BinOp.EQ, ast.BinOp.NEQ, ast.BinOp.LT, ast.BinOp.GT, ast.BinOp.LE, ast.BinOp.GE, @@ -1497,6 +1510,7 @@ def _resolve_i32_pair_ret_te( def _ctor_to_adt_name(self, ctor_name: str) -> str | None: """Find the ADT type name for a constructor name.""" + # ctor-owner-exempt: the flat ownership projection itself return self._ctor_to_adt.get(ctor_name) def _strip_future_scoped(self, name: str) -> str: @@ -2190,6 +2204,7 @@ def _get_arg_type_info_wasm( # so sparse constructors like Err(e) bind to the correct ADT type param. adt_name = self._ctor_to_adt_name(expr.name) if adt_name: + # ctor-owner-exempt: no owner available at this site field_tp_idx = self._ctor_adt_tp_indices.get(expr.name) adt_tp_count = self._adt_tp_counts.get(adt_name, 0) if field_tp_idx is not None and adt_tp_count > 0: diff --git a/vera/wasm/operators.py b/vera/wasm/operators.py index 57db0d0b8..2f74ca56c 100644 --- a/vera/wasm/operators.py +++ b/vera/wasm/operators.py @@ -440,6 +440,7 @@ def _full_ctor_type_name(self, operand: ast.Expr) -> str | None: base = self._ctor_to_adt_name(operand.name) if base is None: return None + # ctor-owner-exempt: no owner available at this site tp_indices = self._ctor_adt_tp_indices.get(operand.name) tp_count = self._adt_tp_counts.get(base, 0) if not tp_indices or tp_count == 0: @@ -820,14 +821,22 @@ def _generate_adt_eq_fn_body( tp_names = self._adt_tp_param_names.get(base, ()) tp_mapping = dict(zip(tp_names, type_args)) - adt_ctors = sorted( - ( - (ctor_name, self._ctor_layouts[ctor_name]) - for ctor_name, parent in self._ctor_to_adt.items() - if parent == base and ctor_name in self._ctor_layouts - ), - key=lambda x: x[1].tag, - ) + # #1414: enumerate the constructors of the ADT being compared out + # of ITS OWN table. Both maps here are keyed by bare constructor + # name across every ADT, so a user declaration sharing one of this + # type's constructor names displaces the layout AND the ownership + # entry. LATENT under current coverage, and measured to be: + # forcing this branch back to the flat map leaves the whole + # tag-index battery green, because the writer fix in + # `data.py` already gives the value the right tag and this + # enumeration is only reached for types the collision does not + # reorder. Converted anyway, on the same rule as the other + # owner-qualified reads — a site holding the owner must not ask a + # table that cannot represent one (PR #1419 review). + own = self._adt_ctor_layouts.get(base) + # Same measured-dead fallback as `_composite_ctor_plans`, removed on + # the same evidence. + adt_ctors = sorted((own or {}).items(), key=lambda x: x[1].tag) if not adt_ctors: raise CodegenInvariantError( # pragma: no cover "ADT equality on a type with no constructors") @@ -866,6 +875,7 @@ def _generate_adt_eq_fn_body( # resolves positionally to the matching concrete type argument; # any other field deep-substitutes param NAMES nested inside a # parameterized declared type (`List` → `List`). + # ctor-owner-exempt: owner-qualified above; parsed-name path tp_idx = self._ctor_adt_tp_indices.get(cname) raw_types = ( layout.field_types