Put the in-scope slot table in the E130 error (#558) - #11
Merged
Conversation
…ruction (aallan#1208) `TypeAliasInfo` carried only `resolved_type` — the semantic collapse computed at registration time, which cannot be walked back to the spelling. The one naming renderer landing in `vera/naming.py` needs the SOURCE-level alias body to build its `AliasEnv` from a live `Environment`, the same map codegen already keeps in its own `_type_aliases` side-table. Adds `body: ast.TypeExpr | None = None` and populates it at both construction sites (the checker's and the verifier's `_register_alias`). Defaulted, so any other constructor stays valid; nothing reads the field yet. Co-Authored-By: Claude <noreply@anthropic.invalid>
…#1208, aallan#1209) Six subsystems independently rendered "the name of this type expression" and disagreed about aliases; a name minted one way and looked up another misses silently, which is the aallan#1208 / aallan#1209 bug class. This lands the single renderer, with the CHECKER's current rendering as the rule. No consumer flips yet — the module is additive, and the differential that proves it byte-identical to the checker follows. THE RULE, as implemented: syntactic (alias-opaque) HEAD, fully resolved type ARGUMENTS; a refinement renders its base at top level and the predicate-elided form in argument position; a function type renders `Fn` at top level and its full spelling (effect row SORTED) in argument position; every renderer is total and unresolvable types render `?`. Argument resolution rebuilds the checker's own semantic `Type` and hands it to the checker's own `pretty_type` / `canonical_type_name`, so byte-identity is structural rather than a coincidence to maintain. Alias visibility follows REGISTRATION ORDER: an alias body sees only the aliases declared before it, exactly as `_register_alias` resolves each body against the table as it stood. A forward reference stays opaque and a cycle terminates on the same placeholder the checker produces — the ordering restriction is well-founded, so no depth bound is needed. `substitute_named`, `resolve_alias_type_expr` and `AliasResolutionDepthError` MOVE here from `vera/slots.py` (unchanged, re-exported there for the existing importers). `resolve_scalar_alias_te` stays behind until its callers flip. `tests/test_slot_naming.py` is the rule table: 61 tests pinning each clause to an exact rendered string, including the two orderings the rounds cost — arguments resolve before heads, and alias parameters substitute before the refinement branch (both mutation-validated: each inversion turns its own tests red). Co-Authored-By: Claude <noreply@anthropic.invalid>
…al gate (aallan#1208) The consolidation takes the CHECKER's rendering as the rule, so the load-bearing claim is byte-identity with the checker — not "the module looks right". A unit suite cannot establish that: the divergences that caused the aallan#1208 / aallan#1209 bug class live in alias corners nobody thought to enumerate. This instruments the checker's two naming entry points (`_type_expr_to_slot_name` and `_slot_type_name`, the latter also carrying every `_slot_ref_key` reference, so the binding side and the reference side are both covered) to record a (checker, module) pair on EVERY call, then sweeps the whole `.vera` corpus — 42 examples, 183 conformance programs and their module fixtures, the 283-file PR aallan#1202 probe corpus — plus a 24-program inline battery aimed at the alias / refinement / function-type / shadowing corners, and asserts ZERO divergence over every recorded pair. The module-side `AliasEnv` is built AT RECORD TIME from the live environment, so each comparison sees the alias table and `forall` scope the checker had at that instant — and exercising the C0 `body` field on the live path is part of what is being proved. The checker's own result is what is returned to it, so the instrumentation cannot change what the checker does (pinned). A program that fails to CHECK still contributes every observation recorded before it, since naming runs while diagnostics accumulate and rejected programs reach the malformed shapes disproportionately often; only parse failures contribute nothing, and they are counted. Measured on this corpus: 6,109 observations, 1,438 under a non-empty alias environment, 81 where an argument names an alias pre-resolution, 533 files swept, 5 parse-skipped (pre-existing probe fixtures), 0 divergences. The floors asserted in `test_corpus_sweep_is_not_vacuous` sit below those so corpus drift shows up as a failure rather than as a quietly emptier gate. `test_differential_gate_detects_divergence` is the live proof the gate can go red: perturb the module renderer and the harness reports every pair, with the checker's own results unchanged. Mutation-validated beyond that — dropping alias resolution, and dropping `Decimal`'s argument-eliding branch, each turn the sweep red. Parse + check only, one checker per program: the full sweep runs in ~1.4s, so it stays a default-CI test rather than a slow-marked one. Co-Authored-By: Claude <noreply@anthropic.invalid>
…lan#1208) `_type_expr_to_slot_name` and `_slot_type_name` (the latter carrying every `_slot_ref_key` slot reference) now call `naming.slot_name` with an `AliasEnv` built from the live checker environment. The in-checker rendering composition is gone; `canonical_type_name`, `pretty_type`, and `_resolve_type` stay, because they serve type checking broadly — only the NAMING composition moved. Closes the data-type corner `_resolve_named` recorded. A user may declare `data Float` or `data Decimal` (both check clean), and the checker's `_resolve_named_type` reaches its data-type branch BEFORE the `Decimal` and removed-alias branches, so `@Option<Float>` renders `Option<Float>` and a user `Decimal` keeps its type arguments. `AliasEnv` gains `data_types`, populated from `env.data_types` or from the walked `DataDecl`s, and the branch sits at the checker's precedence position. A narrower ordering sub-corner remains and is now stated in both the module and the unit table: ADT visibility is not declaration-index-bounded the way alias visibility is, so an alias body naming a special-cased ADT declared BELOW it diverges; closing that needs the two registries merged into one index space, a data change rather than a rendering change. Naming is total and silent by design, so delegating would have dropped the E133 / E134 / E135 / removed-alias diagnostics the old composition emitted as a side effect of resolving each argument — at a slot reference (`@Option<Box>.0` for a parameterised `Box`) that incidental report is the only one there is. `_check_slot_name_args` keeps them, walking exactly the traversal the old composition took. Proved by a corpus-wide and a targeted diagnostic differential: byte-identical diagnostics before and after. The naming differential is inverted so it stays non-vacuous. With the checker delegating, comparing it to the module compares the module to itself; the legacy side is now a test-local rebuild of the historical composition from still-live checker machinery, and the module side is what the checker returns. Same corpus, same floors, same red-proof — and the perturbation now moves only the module side. 6,111 observations over 534 files, 1,449 under a non-empty alias env, 83 with an alias in an argument, zero divergences. Co-Authored-By: Claude <noreply@anthropic.invalid>
…allan#1208) Plumbing for the renderer swaps that follow: each subsystem now HOLDS the `AliasEnv` it will name against. Nothing reads it to render yet, and no rendered output changes — proved by a WAT + codegen-diagnostic differential over all 510 corpus programs, byte-identical before and after, and by `vera check --explain-slots` output identical over examples + conformance. * `CheckArtifacts` gains `alias_env` (the entry module's, always present) and `module_alias_envs` (per resolved module, keyed by module path and gated on `collect_module_artifacts`) — mirroring the aallan#987 `module_artifacts` wiring end to end, and for the same reason: aliases are module-scoped (spec §8.4.1), so an imported body must be named against ITS namespace. * `WasmContext.set_type_aliases` / `set_type_alias_params` are REPLACED by one `set_alias_env`. The pair had to be overlaid together (aallan#1184) and now cannot be half-updated. Every consumer in `vera/wasm/` reads `_alias_env.aliases` / `.alias_params`. One semantic seam needed care: `alias_params` keys every alias and maps a non-parameterised one to `None`, where the flat map simply omitted it, so the one MEMBERSHIP test on it becomes the equivalent `is None` test. * `CodeGenerator` holds `_alias_env`, DERIVED from its flat maps rather than taken from `CheckArtifacts`: codegen's alias view is the prelude overlaid by the main file (and, inside `_module_alias_scope`, by the compiling module) over the transformed, monomorphized AST — not the checker's view. Sourcing it from the check would name against a table codegen does not otherwise use, which is the very split aallan#1208 closes. `_sync_alias_env` re-derives it at each point the flat maps change, `_module_alias_scope` swaps and restores it with them. * `ContractVerifier._alias_env` is built at the end of `register_program`; `SmtContext` takes an `alias_env` (threaded from both cold sites, rebound per function on the warm session exactly as `_fn_lookup` is); `MonoContext` gains the field, populated by both drivers; the tester carries it from artifacts down to the Z3 input generator; the LSP `Analysis` lifts both envs out of its artifacts; and `vera check --explain-slots` now takes the artifact-returning check so the table can be named against the checker's own aliases (only that flag pays for it). The alias-map parameters of `resolve_alias_type_expr`, `resolve_type_alias`, `resolve_fn_type_alias`, `resolve_scalar_alias_te`, and the async-fusion predicates widen to `Mapping`, since what reaches them is now an `AliasEnv` field. Read-only either way. Two test FIXTURES construct a `WasmContext` by poking the private alias map; they set the env instead. No expectation changed, and the aallan#633 cycle-guard test still goes red when the guard is mutated — checked, because an empty env would have made it pass vacuously. Co-Authored-By: Claude <noreply@anthropic.invalid>
`_resolve_named` recorded a split: alias visibility followed registration
order, ADT membership was a flat set, so `type M = Decimal<Int>;` declared
ABOVE `private data Decimal { ... }` resolved against an ADT the checker's
table did not yet hold when it resolved that body. The checker gives the
built-in `Decimal` (arguments dropped) and, for the `Float` spelling, `?`;
the module gave the ADT. Closing it needed the two registries in ONE index
space, which is a data change rather than a rendering change.
`AdtInfo` and `TypeAliasInfo` gain `decl_index`, stamped from one shared
per-module counter (`TypeEnv.next_decl_index`) at the moment of registration
by both the checker's and the verifier's passes. `AliasEnv.data_types`
becomes a name -> declaration-index `Mapping` in the same space as `_order`,
and `_resolve_named` applies the SAME bound to ADT membership that aliases
already got. `-1` reads as "precedes everything", which is what the built-in
ADTs are and what any unstamped construction site conservatively gets; the
top-level bound becomes an explicit `_UNBOUNDED` sentinel, since the shared
space now runs past the alias count.
Codegen's `_sync_alias_env` is the third env builder and needed its own index
space. `_decl_order` stamps aliases and ADTs together in three blocks
ordered as the checker sees them: built-ins, then the prelude (a NEGATIVE
block, because `inject_prelude` PREPENDS its declarations while codegen
registers the main file before injecting them -- without it a main-file alias
over a prelude alias would resolve opaquely here and fully at check), then
user declarations from 0 up, each module's absorbed in its own source order
as it is captured. A sweep of every parameter / let / pattern / slot-ref
type expression in the 505-program corpus renders identically through
codegen's env and the checker's: 9,145 observations, 0 divergences.
The pinning test flips from documents-divergence to asserts-agreement and
gains the mirror spelling (`data Float`, whose bound leaves the removed-alias
`?` reachable) and the top-level control (the bound stops at the alias body,
so a slot naming the ADT directly renders against the whole table whatever
the order). The differential battery gains all four shapes, each carrying
its own prelude -- the corner IS where the `data` sits relative to the `type`
-- and is mutation-validated: removing the bound turns 10 of its 24
observations red. The corpus itself is unmoved (510 programs, `check --json`
diagnostics and probe `run` output byte-identical), as expected for a corner
that requires an ADT named after a built-in or a removed alias.
Co-Authored-By: Claude <noreply@anthropic.invalid>
The checker already delegated its naming. Everything downstream still re-derived it: the monomorphizer's De Bruijn recount, codegen's bind sites and its reference resolution, a five-method clause-scope mirror of the checker's rendering, the verifier, the SMT layer, the tester, and `--explain-slots`. They agreed with each other and disagreed with the checker, which is the aallan#1208 bug class. This flips them all, in ONE commit, on the BIND side and the REFERENCE side together. Four prior attempts retreated because a partial flip produces silent index skew — a binding minted under one rendering and looked up under another either dangles or, worse, lands on the wrong member of the checker's equivalence class. Atomicity is the defence, so the two sides of every lookup move in the same change or not at all. DELETED, not adapted: * the clause-scope mirror in `wasm/inference.py` — `_canonical_clause_slot_ name`, `_checker_arg_name`, `_checker_form_slot_name`, `_checker_form_arg_name`, `_head_resolves_through_refinement` (184 lines). Its refined-argument deviation existed because the reference side could not spell the predicate-elided form; both sides render it now, so they meet there. * BOTH class-collision `CodegenSkip` gates in `wasm/calls_handlers.py`. They guarded exactly the skew this removes: one direction split a checker class across two codegen keys, the other merged two into one. The shapes they refused now lower with the checker's semantics, and their three tests assert the run values instead of the refusal. * the "retreat to opaque-only refs" comment block in `wasm/operators.py`, which described the pre-consolidation compromise. * both `or type_name` fallbacks at the handler-clause bind sites. `type_name` was the EFFECT's type argument, not the pattern's name, so the fallback bound the clause parameter under a key the checker never used. * `slots.slot_ref_name`, which has no consumers left. Two derivations deliberately stay syntactic, and both are about a type's REPRESENTATION rather than about naming a binding: `type_expr_slot_name` still answers the WASM width / erasure walks and the structural-`Eq` oracle, and the State/Exn cell FAMILY keeps its own opaque fallback, now derived INSIDE `_family_name` / `_family_name_te` (`family_fallback_name`) so the eight call sites cannot pass different ones. Resolving the family changes the emitted import surface — that is aallan#1209's — and the checker's argument rendering is not mangle-safe: a refined argument renders `Option<{@int | ...}>`, which `mangle_type_name` does not escape. The refinement guard had to move with the reference side: it binds its predicate over the base's slot name, and a predicate's `@Base.n` now resolves through `naming.slot_ref_key`. Both `_refinement_guard_parts` and `naming.refinement_binder_parts` name the binder with `slot_name`, which is also what `_check_one_refinement_predicate` binds it under. BLAST RADIUS, measured over all 510 corpus programs (`check --json` diagnostics for every file, `run` for every probe), before and after: SIX files differ, all in `tests/probes/`, all one class — a program that died on a dangling-slot [E699] now resolves and runs with the value the CHECKER's binding rule gives. Three of them record that value in their own header comment, and it is what they now print. No `check` diagnostic moved anywhere, in code, severity, line, or message; no example and no conformance program is affected. `tests/test_slot_naming_blast_radius.py` pins the set by path with its expected value, plus five slot-heavy sentinels outside it, and is mutation-validated in both directions: reverting either the bind side or the reference side turns it red. `--explain-slots` is the user-facing oracle and now reports the checker's names. On the corpus's one signature-level rename it says `@Option<Int>.0` for a parameter written `@Option<Cnt>`; on two constructed merges it reports one stack where it used to report two, and the programs — which were HARD codegen crashes on check-green input before this — return exactly the parameter the table names. One regression the corpus could not see was found by hand and fixed here: `monomorphize_fn` rendered a clone's binders against the DRIVER's alias namespace. Aliases are module-scoped (§8.4.1), so an imported generic's module-local alias stayed opaque, the recount missed the merge, and the clone — which codegen emits under the DEFINING module's scope — resolved a reference onto the wrong parameter, silently, with the right arity and type. `monomorphize_fn` now takes the env it must name against, and each of the four codegen clone sites supplies its origin module's through `_clone_alias_env`. Pinned against its single-namespace control. E130 diagnostic wording is untouched (`vera/errors.py` unchanged) and the SQL-provenance suite is byte-identical. Co-Authored-By: Claude <noreply@anthropic.invalid>
…llan#1208) The three PRESENTATION surfaces were the last consumers still resolving a `@T.n` by hand. Two of them did it with the reference's bare HEAD against a table keyed by the full rendered name, so a parameterised reference could never match — and both failed CLOSED, which is why neither had a symptom anyone would report: * `verifier._pre_at_call_site` abandoned the whole substitution on the first parameterised slot, so E501 fell back to its generic wording ("Add a precondition to 'caller'…") on exactly the signatures where naming the concrete arguments helps most. `@Wrap<Int>.0` in a callee's `requires` now renders `At this call site: 0 > 0`, and the fix shows the guard. * `lsp.definition_at` returned nothing, so go-to-definition was silently dead for every container-typed parameter — `@Option<Int>.0`, `@Map<String, Int>.0`, an alias-spelled parameter reached from a canonical reference. Both now key with `naming.slot_ref_key` against the same env the binding side is rendered in. Auditing the third consumer's env for module-correctness turned up a divergence none of them was rendering right: a function's OWN `forall` variables shadow same-named module aliases, and the checker binds its parameters with them in scope (`_check_fn` step 1, before step 4). Rendered against the bare module env, `type T = Int` + `forall<T> fn g(@option<Int>, @option<T>)` collapses two checker stacks into one, and `--explain-slots` reported `@Option<Int>.0` as parameter 2 where the checker resolves it to parameter 1 — a wrong answer, not a vague one, from the tool whose whole job is answering that question. `slot_table` now takes the owning function's `forall_vars` as a REQUIRED argument, for the same reason its `env` is required: the omission has no symptom of its own. `slots.fn_slot_scope` is the one narrowing, so the binding side and the reference side cannot end up scoped differently. The tester's threaded env is verified inert-but-correct rather than assumed: `_get_param_types` matches a parameter's SYNTACTIC head against `PRIMITIVES` and never resolves aliases, so an alias-typed parameter is skipped (E701) before any Z3 variable is named. Both halves are pinned — the renderer canonicalizes a type-argument alias given a real env, and the gate that currently bounds its reach — so a future `_get_param_types` that does resolve aliases inherits correct naming instead of discovering it afterwards. Residual-duplication sweep: every remaining `type_expr_slot_name` caller is one of the two documented representation-only classes — the WASM width / erasure walks (`wasm/inference.py`, `codegen/monomorphize.py`'s Eq-derivability oracle) and the State/Exn cell FAMILY (`wasm/calls_handlers.py`, `wasm/operators.py`, `codegen/functions.py`). Both stay syntactic by design. No presentation-layer file derives a slot name independently any more. Tests, each written to fail first: * `test_obligations.py` — a parameterised callee slot substitutes into E501's message and fix (was: generic wording). * `test_lsp.py` — a parameterised reference resolves; an alias-spelled parameter is reachable from a canonical reference; a `forall` shadow lands on parameter 1 (was: None, None, parameter 2). * `test_cli.py` — `--explain-slots` tables an alias type argument resolved, and keeps a `forall`-shadowed pair as two stacks. * `test_tester_coverage.py` — the tester's env is load-bearing, and the primitive-head gate that bounds it. * `test_slot_naming_blast_radius.py`, `test_obligations.py` — the two existing `slot_table` / `_pre_at_call_site` call sites take the new argument. Co-Authored-By: Claude <noreply@anthropic.invalid>
The checker resolves an effect instance's type arguments in full (`_resolve_effect_ref` -> `_resolve_type`), so `State<MaybeInt>` under `type MaybeInt = Option<Int>` and `State<Option<Int>>` are ONE `EffectInstance`: one handler handles both spellings, and a call across them type-checks. Codegen named the cell FAMILY from the source spelling for anything that did not resolve to a scalar (the aallan#1205 gate), so those two spellings minted two host cells — one cell per checker, two per codegen, a silent state split behind a green check. A cross-spelling program returned the untouched initial value; a cross-MODULE one did the same. `naming.family_name` is now the ONE family renderer at every site: registration (`_check_state_type` / `_check_exn_type` / the body scan), per-function lowering, both handler translations, and the `old(State<T>)` snapshot. Each renders against the DECLARING module's `AliasEnv`, so a name means what it meant where it was written — two modules declaring `Hid<T>` differently keep two cells. `slots.resolve_scalar_alias_te` is deleted: its scalar gate is exactly what aallan#1209 retires. `family_fallback_name` stays, re-justified, for the residue resolution cannot name. Mangle-safety is part of the family's contract now, not an argument for not resolving it. A family feeds `mangle_type_name`, whose escape covers exactly the canonical `Head<arg, arg>` grammar, so `family_name` gates on `is_ref_spellable` and keeps the opaque spelling for a resolution that renders outside it (`Option<fn(Int) -> Int>`, `Option<{@int | ...}>`) — without the gate the flip emitted an import name the WAT parser rejects. Falling back can leave a family split; it can never merge two cells the checker keeps apart. The family's old TypeExpr-level walk carried a 32-level depth bound whose overflow was a loud per-function skip. `vera.naming` resolves each alias body against a strictly shorter prefix of the table, so it is well-founded with no bound — the same shape the checker's own registration has, which is why the checker accepted deep chains all along. A 33-hop chain now compiles and runs instead of dropping its function, and the two E607/E612 arms that reported the bound are gone with it. Measured: the whole 510-program corpus captured before and after (`check --json` codes, emitted `state_*`/`exn_*` symbols, `run` for every probe). Six files differ, all in `tests/probes/state_handlers/alias_families/`: one changes VALUE (`f1_cross_spelling`, -1 -> 7, the two spellings now share the cell), five rename or collapse symbols (`state_*_MaybeInt` -> `state_*_Option_LInt_R`, `exn_Msg` -> `exn_String`) at unchanged values. No example, no conformance program, and no `check` diagnostic moved. The 25 E533/E336 gate probes verify byte-identically — obligation tier counts included — because those gates compare Types, not rendered names. `tests/test_family_naming.py` pins the collapse where it is observable (bare alias, parameterised alias, and an `Exn<Msg>`/`type Msg = String` payload whose `i32_pair` must arrive through the same tag), one import per collapsed family, the cross-module case, the negative (`Option<Int>` and `Option<Bool>` stay two cells), the mangle-safety gate, byte-stable symbols for seven alias-free corpus programs, and the whole measured radius. Mutation-validated: reverting the resolution, dropping the mangle gate, and dropping type arguments each flip a distinct, correct subset red. Skip-changelog: the PR's [Unreleased] bullet already states the composite collapse. Co-Authored-By: Claude <noreply@anthropic.invalid>
…allan#1216, aallan#1217) `vera test` resolves a parameter's type through the threaded naming environment before asking whether Z3 can encode it (aallan#1216). The old derivation matched a parameter's SYNTACTIC head against `PRIMITIVES`, so `type Cnt = Int` never reached `Int` and every alias-typed signature was classified un-encodable and skipped (E701) before a variable was named. Resolution is not encodability: an ADT, a function type, a type variable and an unresolvable expression still skip — now by the resolved answer, and the skip reason names it (`cannot generate Option<Int> inputs`). An alias is also the only way to write a refined parameter, so aallan#1216 is what first brings refinements to the generator. Codegen guards them on entry, so the predicate is seeded into Z3 through `naming.refinement_binder_parts` — without it 96 of 100 trials on a `type Pos = { @int | @Int.0 > 0 }` parameter are reported as refinement violations. Both rendering sites now name in the function's own slot scope (its `forall` variables shadow same-named module aliases). `vera check --explain-slots` prints a table for every `where`-block helper too (aallan#1217), indented under its parent and qualified `parent.helper` in the JSON. The accumulation of enclosing type parameters moves into `slots.fn_scopes`, shared with the language server's `definition_at`, so the two surfaces cannot answer differently about one helper. `naming.resolve_alias_type_expr`, `naming.substitute_named` and `naming.AliasResolutionDepthError` are deleted with their `vera.slots` re-exports and their unit test: the family flip retired the last caller, and the full suite is green with both functions raising on entry. Co-Authored-By: Claude <noreply@anthropic.invalid>
…re their probes Every probe under `tests/probes/` is eventually promoted to CI or deleted. This dispositions the shapes owned by the two issues this PR closes: seventeen new conformance programs carry the alias × handler corner the PR aallan#1202 review probes were written to reach, and the thirty-three probes that measured them are deleted. ch03_slot_alias_type_argument head opaque, arguments resolved ch07_state_composite_alias composite alias cell + match ch07_state_composite_alias_cross_spelling two spellings, one cell ch07_state_scalar_alias_cross_spelling scalar alias across a fn boundary ch07_state_alias_chain multi-hop / parameterised / alias-of ch07_state_nested_param_alias twice-applied `Id<Id<Nat>>` ch07_state_scalar_alias_widths Bool / Byte / Float64 cells ch07_state_alias_op_result_positions get(()) as element / operand / scrutinee ch07_state_clause_alias_slots alias spellings in clause slots ch07_exn_scalar_alias Exn<Code> caught as Exn<Int> ch07_exn_string_alias Exn<Name> i32_pair payload, one tag ch07_exn_param_alias Exn<Id<Int>> / Exn<Id<Id<Int>>> ch08_state_alias_per_module(+_lib) same alias NAME, two modules ch08_state_alias_module_table(+_lib) same name, different body ch02_alias_cycle_rejected E132 negative (new coverage) The two suite fixtures that read those probe paths — the aallan#1209 family radius and the aallan#1208 blast radius — now read the promoted conformance programs. The pinned values are the MEASURED ones, not a re-baseline: each shape's entry point is public so the probe's own expected value is still what is asserted, and perturbing a promoted fixture takes the blast-radius assertion red. Differential sweep after the deletions: 6,084 observations (floor 2,000), 1,423 under a non-empty alias env (floor 200), 102 arguments naming an alias pre-resolution (floor 40), 522 files (floor 500), 5 parse-skipped (cap 10) — the five known parse-broken probes, now flagged as such in the index and left for the PRs that close their issues. Co-Authored-By: Claude <noreply@anthropic.invalid>
The naming consolidation gave the toolchain one renderer; several consumers were still feeding it the wrong ENVIRONMENT, and a name minted in the wrong namespace misses silently. Four provenance seams, each a real regression the adversarial review exhibited: * an IMPORTED callee's contract was rendered with the IMPORTER's alias env, so where two modules spell one alias differently the call-precondition obligation either attached to the wrong argument and VANISHED (a false Tier-1) or split a stack the callee merged (a spurious E501). The verifier now builds a naming env per resolved module from that module's own registration and pins each harvested contract to it; the SMT layer scopes the callee-parameter stack and both contract translations to it, and the call-site message renders its substitution table there too. * an imported GENERIC was monomorphized AND verified under the importer's env while codegen used the defining module's, so the two sides proved and emitted different bodies — the De Bruijn recount permutes the parameters. A lying imported contract could prove clean and violate its own postcondition guard at run time. Origins are recorded per discovery key and threaded into every `monomorphize_fn` call and into the clone's re-declaration. * a `forall` variable SHADOWS a same-named module alias for the whole signature, and nothing outside the checker applied that narrowing: the monomorphizer's recount, the verifier's parameter declaration, and codegen's emission of the exported uninstantiated template all collapsed two parameter stacks the checker keeps apart. The recount now renders its pre-substitution side in the narrowed scope (accumulating `where`-helper parameters as `fn_scopes` does) and its post-substitution side un-narrowed, matching what the consumers rebuild; the verifier and codegen narrow per function. * the tester keyed its slot names in the narrowed scope but handed `SmtContext` the un-narrowed env, so a reference would have resolved against a scope the bind side never used. `CheckArtifacts.module_alias_envs` is deleted rather than wired up: the two consumers that need a per-module env each build it from a namespace they already hold, and `vera verify` runs with module-artifact collection off — an artifact-sourced table would have been empty exactly where these obligations need it. Co-Authored-By: Claude <noreply@anthropic.invalid>
…ion (aallan#1208) Two of the three remaining review findings; the third is characterized rather than fixed, because closing it is a checker-semantics change. `vera/naming.py` resolved an alias by recursive descent, one Python frame per hop, so a legal `type A1 = A0; type A2 = A1; …` chain raised an uncaught `RecursionError` at ~340 hops — from inside a renderer this module's own docstring calls TOTAL, and the checker's cost is O(1) per hop (it stores each alias's `resolved_type` at registration). Resolution is now iterative and dependency-first: every alias a body mentions has a strictly smaller declaration index, so the mention graph is a DAG, and memoizing the deepest first leaves each `_resolve` recursing no further than its own body's syntactic nesting. This is an evaluation ORDER, not a depth bound — a 400- hop chain still renders `Option<Int>`, which both the checker-equivalence rule and the 41-hop `ch07_state_alias_chain` conformance program require. The alias branch also stops indexing `env.aliases` unconditionally, so an environment whose `_order` names a body-less alias falls through instead of raising. Codegen's `_refinement_guard_parts` was a second hand-maintained copy of `naming.refinement_binder_parts` — chase the alias chain, name the base, conjoin the `@Nat` / `@Byte` implicit range — and the two had already drifted at the erased-base and nested-base corners. Codegen now consumes the one derivation and layers its two WASM-specific decisions on top: an erased base emits no guard, a nested refinement base is rejected loudly (E618). A differential pins their agreement, and because that differential is green whether or not they share an implementation, a mutation assertion carries the weight: perturb the shared derivation and codegen's binder has to move with it. The prelude-alias asymmetry is INVESTIGATED and not forced. `inject_prelude` runs at codegen and at the verifier's mono discovery, never at check, so the checker has no `ArrayMapFn` and renders it as an opaque ADT while codegen resolves it to a function type — in argument position the two therefore merge different parameter stacks, and an exported body reads the wrong one. Both naming envs faithfully report their own side, so this is not a renderer bug: closing it means registering the prelude's aliases in the CHECKER, which changes what the checker resolves, and with it `--explain-slots`, LSP hovers, and the binding table. The shape joins the differential battery and the gap is pinned by a characterization test that fails the day someone closes it. Co-Authored-By: Claude <noreply@anthropic.invalid>
…an#1208) Validation, not behaviour — with two exceptions noted below. The differential's inline battery could go inert without failing. A blanket `contextlib.suppress(Exception)` around the check swallowed a compiler-level raise, so an entry that self-destructed contributed no observations at all and read exactly like an entry that agreed; only `VeraError` is absorbed now, and even that is recorded and floored at zero. The cycle and forward-reference corners were one program, so one failure took both down; they are two entries, and the reach test asserts the exact string each must render rather than counting. The corpus alias-in-argument floor is CORPUS-ONLY, which exposed that the corpus contributes 34 of the combined count rather than the 40 the shared floor implied — growing the battery can no longer mask corpus decay. Two zero-covered effect-row branches gain battery entries: a qualified effect reference (`Module.Effect`) and an effect ROW VARIABLE, both inside a function type in argument position. The LSP's `where`-helper narrowing was mutation-surviving: dropping the `fn_scopes` accumulation in `definition_at` failed the CLI suite and passed the LSP one. Its twin now exists — one narrowing, two surfaces, both watching. `vera.naming.type_arg_name` had no caller while `slot_name`'s docstring claimed a composition through it; `slot_name` now renders each argument through it for real and restates only the `Head<a, b>` join, which the corpus differential compares against `canonical_type_name` directly. `alias_env_from_declarations` had no production caller either — every consumer builds its environment from a namespace it already holds — so it leaves the shipped module and becomes a test fixture constructor, where a second implementation of declaration-index assignment cannot become a source of truth. The two per-module alias-table conformance libraries pass `verify` and were pinned at `check`; both are raised to the deepest level they reach, which also enrols them in the warm/cold obligation-parity corpus. `ch02_alias_cycle_rejected`'s header claimed the diagnostic lands on the second declaration; it lands on the first, and the comment now says why. KNOWN_ISSUES.md regains the one-to-one invariant with the open `bug`-labelled set (aallan#1218, aallan#1219, aallan#1220). The naming module's docstring is made true: totality is defended rather than asserted (the iterative resolution and the `env.aliases` membership check are named as what defends it), the argument-rendering claim matches the code, the representation-only sites are two rather than one, and the environment rules — module provenance and `forall` narrowing — are stated as rules alongside THE RULE, because one renderer is only half the contract. TESTING.md's naming rows describe what the suite pins rather than narrating how it got there. Co-Authored-By: Claude <noreply@anthropic.invalid>
…ion at its open tracker aallan#1222 The Bugs table stays one-to-one with open bug-labeled issues; the limitation row cited closed aallan#1172 and now cites aallan#1222, filed for it. Skip-changelog: two-row KNOWN_ISSUES bookkeeping, no compiler change Co-Authored-By: Claude <noreply@anthropic.invalid>
…n-keyed origins (aallan#1208) The fixed-point adversarial review's second round found five places where the naming consolidation was right by coincidence rather than by construction. F1 — `_resolve_alias` still recursed once per level. Pushing a body's whole pending list puts SIBLINGS in progress together, and the `in_progress` guard then filters a sibling that is also a real dependency, so the body is resolved with that sibling unmemoized and `_resolve` reaches it by recursing. A `type Bk = D(k-1); type Ck = Drop<Bk>; type Dk = Drop2<Bk, Ck>` graph raised `RecursionError` at a few hundred levels, from the renderer the module docstring calls TOTAL. One dependency per iteration leaves only ANCESTORS in progress, and an ancestor can never be a pending dependency, so nothing is filtered and the nesting is constant. The docstring now claims exactly that. F2 — the verifier's `_fn_naming_scope` was green both ways: every call site renders a signature and the references into it against the SAME env, so a wrong scope is wrong consistently and invisible from inside. Crossed against a second component instead: the verifier's declared parameter names against `slots.slot_table`'s, and its `where`-helper scope against `slots.fn_scopes`' accumulation. F3 — the De Bruijn recount narrowed only its PRE side, justified by "the clone carries forall_vars=None". True of the function being cloned, false one level down: substitution clears only the top declaration's variables, so a `forall<U>` helper keeps them in the clone and both consumers narrow by them. The POST side now narrows by the variables that SURVIVE substitution. F4 — the differential's file floor counted corpus plus inline battery, so battery growth could mask corpus shrinkage. Corpus-only now, and three docstrings that overclaimed which floors read which population are corrected. F5 — `_alias_env_for_generic` looked an imported nested generic's origin up under its chain's FIRST segment, which is never a recorded key, and the verification-time clone looked it up under the helper's bare name. Both fall back to the importer's namespace, and the two being wrong TOGETHER is why nothing saw it. The whole lexical chain is probed now, one `$where$` segment shorter at a time, on both sides. Plus the review's low batch: a stale `CheckArtifacts.module_alias_envs` reference in codegen, a tester fixture with no shadowed parameter to shadow, the `Future<Unit>` erased-base corner and a `@Nat` runtime analogue in the binder-convergence differential, a predicate as well as a binder-name mutation, obligation-level assertions on the imported-callee E501s, and the KNOWN_ISSUES aallan#1222 row describing both failure directions. Also files aallan#1223: a generic `where`-helper under a GENERIC parent never has its own generic callees instantiated by codegen, so a check-clean, verify-clean program compiles to no exports. Byte-identical on this HEAD and at the branch point, so it predates this work; tracked, not fixed. Co-Authored-By: Claude <noreply@anthropic.invalid>
… refined returns (aallan#1208) Three namespace defects the review probes reached, each with the failure that exhibited it: - Codegen's declaration-index space was shared across every absorbed namespace, and `_stamp_decl_order` is idempotent by name, so a name an imported module had stamped at Pass 0.5 kept that earlier index inside the main file's namespace at Pass 1 — turning a forward alias reference into a backward one. `import lib;` + `type Z = X; type X = Nat;` resolved `Z` to `Nat` in codegen and to the imported ADT at check, merging two parameter stacks the checker kept apart: a check-clean, verify-clean program that read the wrong parameter through valid WASM (both erase to i32, so nothing trapped). The space is now keyed to its owning namespace and swapped by `_module_alias_scope` beside the alias maps it describes. `origin/main` returns 7 on the repro; this branch returned 137438953472 before the fix. - `_callee_alias_env`'s unpinned fallback rendered in the ENTRY program's namespace. Only public functions of directly imported modules are pinned, so an imported generic's own `where`-helper always reached it, and a helper whose parameters are two stacks in its module and one in the importer's discharged a violated precondition as true — a false Tier-1 that traps at run time, with a spurious E501 as its mirror. The fallback is now the module under verification. - A callee's refined-RETURN predicate was translated outside `_callee_naming_scope` while its `requires`/`ensures` were inside it. Latent today (the binder beside it is bare-headed, so push and lookup miss under both namespaces), so it is pinned by provenance. Round-3 findings: the monomorphizer's post-substitution scope narrows by the vars the CLONE declares rather than by those surviving substitution — the two differ under an identity mapping, where the post side minted `Option<Int>` against consumers' `Option<T>`; E618 reports once per declaration rather than once per visit and per clone; the tester translates a refinement's membership predicate against a binder-only `SlotEnv`, matching the checker's isolated single-binder scope; and the KNOWN_ISSUES rows for aallan#1223 and aallan#1222 now say what the code does. Review findings: §7.5.1's cell-identity rule is hedged by the mangle-safe-family gate (aallan#1219); TESTING.md's conformance counts are 33/26 as the manifest has them; boundary-safe WAT symbol and `local.get` matching; recursive type-argument spellings; trap assertions on `kind` alongside their predicate text; an invocation floor under the constant-nesting assertion; and three cross-component docstrings now say which axis they are independent on and which shared renderer the literal assertions cover. Co-Authored-By: Claude <noreply@anthropic.invalid>
Skip-changelog: two-row bug-table bookkeeping, no compiler change Co-Authored-By: Claude <noreply@anthropic.invalid>
…n#1208) Codegen enters an imported module's namespace in four places. Three paired `_module_alias_scope` with `_module_source_scope`; the mono-clone body pass entered the alias scope alone, so any diagnostic raised while compiling a clone of an IMPORTED generic carried the importer's path with module-local line/column — coordinates naming unrelated source, or a line past the importer's end that renders an empty `source_line`. That also swallowed a distinct module's diagnostic: the E618 nested-refinement rejection is deduplicated on the resolved location, on the premise that a location carries the file it belongs to. Two imported library modules of identical shape declare at coinciding line/column, so the pair collapsed to one report. The new cross-module test pins the count and the attribution together, with the coordinate coincidence asserted first so a fixture edit cannot leave it green for the wrong reason. Also: TESTING.md's level-limited skip table was missing four rows — both stages for `ch02_alias_cycle_rejected` and the `run` stage for the two per-module alias-table libraries — and understated the documented total; measured against the manifest, the true count is 81, not 77. KNOWN_ISSUES gains the row for aallan#1227 (codegen's global `_adt_layouts` versus module-scoped alias envs). Co-Authored-By: Claude <noreply@anthropic.invalid>
One renderer: the naming module (aallan#1208, aallan#1209)
…1213) The binding table is keyed by the checker's rendering, and five documents described a rule the compiler does not implement. - vera/README.md and the Binding docstring in vera/environment.py called a canonical type name "the syntactic name". Alias opacity is a property of the HEAD; type ARGUMENTS resolve, so @option<Cnt> under type Cnt = Int binds Option<Int>. - vera/README.md attributed the monomorphizer's De Bruijn recount to full-depth slot names from vera/slots.py; it renders through naming.slot_name against the clone's origin-module AliasEnv. - SKILL.md read as though any non-primitive parameter is skipped by vera test. The decision is made on the resolved type (aallan#1216). - DE_BRUIJN.md quoted --explain-slots output with hand-aligned columns the tool does not emit, and no where-helper block (aallan#1217). The sample is now the verbatim output of a real run. - spec/03 3.8 asserted aliases are "not transparent for reference resolution" unqualified, contradicting 3.8.1 twelve lines below. The module map also gains the environment half of the contract on the five rows that carry it: monomorphize, smt, verifier, lsp/features and codegen/modules. Co-Authored-By: Claude <noreply@anthropic.invalid>
The head-opaque / arguments-resolved / cells-resolve rule was implemented across six subsystems and written down nowhere a reader would look. DE_BRUIJN.md gains a section 6, "Type aliases and slot names": the three-clause rule, aliases as the way to name a parameter without names, merged stacks and which line of --explain-slots is authoritative, forall shadowing, and cell identity. Sections 6 to 10 renumber to 7 to 11. Section 4 gains the where-helper and forall-variable binding rules, the quick reference gains Aliases and where helpers entries, the debugging workflow gains the alias case and the qualified JSON helper names, and further reading points at spec 3.8 / 3.8.1 and 7.5.1. Every example in the new section was run; the tables are verbatim output. The sweep also found two pre-existing section 5.6 closure examples that never parsed - an inline function type in return position - now written through a type alias as the conformance suite does. vera/README.md gains Design Pattern 8, "One renderer for slot names": the rule, the environment that is the other half of the contract, the two representation derivations that stay in slots.py, and the differential that proves the two sides agree. The two alias-opacity paragraphs gain the argument clause, and the per-section "Files:" lines drop their line counts, which contradicted the gated module map. TOOLCHAIN.md, LSP_SERVER.md, FAQ.md, DESIGN.md, spec/02 and spec/08 gain the clauses their surfaces had grown; architecture.svg and its text twin place naming.py in the type-check stage and state the one-renderer fact. Co-Authored-By: Claude <noreply@anthropic.invalid>
) vera/README.md's Test Suite paragraph cited 6,821 tests across 104 files, 143 conformance programs and 37 demos against a live 9,390 / 143 / 196 / 42. Only the module map in that file was gated, so the sentence drifted for many releases with nothing to catch it - the same class as FAQ.md's headline line, and the same fix: read the numbers the way the oracle reads every other citation of them, and treat a reworded sentence as an error rather than a skip. TESTING.md's overview row states a total and its parts. The total was pinned; the parts were not, so refreshing only the number the gate reads would leave an arithmetically impossible parenthetical behind. The parts are now checked to sum to the collected total. Both checks are unit-tested and mutation-validated: dropping any one of the four vera/README citations, comparing the breakdown sum to nothing, or returning silently on a reworded sentence each turns exactly its own test red. DE_BRUIJN.md joins the shared parse-only doc gate (now five documents). Its two section 5.6 closure examples had stopped parsing with nothing watching, which is the gap rather than the examples. Co-Authored-By: Claude <noreply@anthropic.invalid>
…an#1213) Section 6.4 wrote `forall<T> fn split(@option<T>, @option<Int>)` and said that without the shadow the reference would land on the wrong parameter. It would not: in that order the shadowed and unshadowed readings both resolve `@Option<Int>.0` to parameter 2, so the example demonstrated nothing. With the parameters the other way round the two readings disagree - parameter 1 shadowed, parameter 2 merged - which is the shape the LSP and CLI regression tests pin. Table re-run. Section 6.3's note on the report is also tightened: the signature line re-prints the type NAMES as written, not the line as written, and the rows are authoritative because they are the checker's binding keys. Co-Authored-By: Claude <noreply@anthropic.invalid>
Review of the sweep turned up claims the compiler does not implement, and count citations no gate reads. The absolutes about cell identity are false where the resolved type has no mangle-safe family name — `naming.family_name` falls back to the alias-opaque spelling there, so two spellings name two cells (aallan#1219, spec §7.5.1). The caveat now lives once, in `DE_BRUIJN.md` §6.5, and §6.1, §9, `FAQ.md` and `DESIGN.md` point at it instead of each restating "spelling never splits a cell". `DE_BRUIJN.md` §5.6's lead-in stated two rules that are not rules: a function type needs neither a `type` alias (`-> @fn(Int -> Int) effects(pure)` checks) nor a `Unit` parameter to be nullary (`-> @fn(-> Int) effects(pure)` checks). The real constraints are the `@` prefix on a return type expression and plain inner type names inside a type-level `fn(...)` (grammar.lark:49); the alias is the conformance suite's convention, and the examples say so. The same false clause is corrected in this cycle's CHANGELOG bullet. `SKILL.md`'s `vera test` paragraph claimed a type variable skips with its resolved type named, where `tester.py` short-circuits a generic function as `generic function` before parameter types are read at all; and that `type Count = Nat; public fn twice(@count -> @nat)` is "tested", where trials are what a Tier 3 contract gets — that signature reports `VERIFIED (Tier 1)`. Both now describe the classification the tester performs. `DE_BRUIJN.md` §6.2's `[E130]` block was hand-composed to one line; it is now the compiler's verbatim output, as §10's sample already is. Count and inventory fixes: `CONTRIBUTING.md`'s commit-stage hook count (31, matching the intro and `.pre-commit-config.yaml`); `TESTING.md`'s validation-script count (twenty-four, the rows it introduces) plus the `check_debruijn_examples.py` row it lacked; and the CI **lint** row, which now lists every step `ci.yml`'s lint job runs, in order. `vera/README.md` states the W-series alongside the E-series (`W001` typed holes, `W002` eager `async` argument) and credits `slots.py` with the `fn_slot_scope` helper the tester and monomorphizer import. The root `README.md` architecture alt text matches `vera/README.md`'s. `check_doc_counts.py` reads all four `vera/README.md` Test Suite counts comma-tolerantly, so none of them switches its own check off by crossing a thousand — pinned by a test that fails on the digits-only pattern. Co-Authored-By: Claude <noreply@anthropic.invalid>
The review of the previous commit turned up five more citations of the same staleness class, all of them inventories that grew without their description. `TESTING.md`'s validation-script table gains `check_explicit_encoding.py` (aallan#645), which the CI lint job and the `explicit-encoding` hook both run, and `check_distribution.py`, which `ci.yml`'s `package-distribution` job runs — twenty-six rows now, counted from the table. That job had no row in the CI table at all; it does now, listing the build, `twine check`, `check_distribution.py` and the out-of-checkout wheel smoke-test it performs. With it the table lists all nine jobs the "nine parallel jobs" prose promises. `vera/README.md`'s `ERROR_CODES` entry count was nine short, and a bare total tells a reader nothing about what moved, so it states the split: 156 entries, 154 `E` codes and the two `W` warning codes. The `vera errors` one-liners in `README.md`, `AGENTS.md` and `SKILL.md` described an `E`-only registry, where the command prints `W001` and `W002` as well; all three now name the full registry, matching Design Pattern 9's wording. `check_vera_readme_test_counts`'s docstring is present-tense, like its sibling `check_tests_breakdown`. Co-Authored-By: Claude <noreply@anthropic.invalid>
Skip-changelog: one-file orientation-doc sync with the inventory pass Co-Authored-By: Claude <noreply@anthropic.invalid>
`_VERA_README_TESTS` spans four counts across a long sentence, so it matches with `DOTALL` — and it searched the whole of `vera/README.md`. That let the paragraph's head pair with digits from any LATER section: reword the paragraph until it no longer states the counts, leave a matching `(196 programs in \`tests/conformance/\` …)` and `(42 end-to-end demos)` anywhere further down, and the check greens. An adversarial fixture confirms it — reworded section plus decoys returned no errors, and with wrong decoys it reported an unrelated section's digits as "the Test Suite counts". A silent skip is precisely what this gate exists to prevent. The counts are now read from the `## Test Suite` section alone, sliced at the next `## ` heading, and a renamed heading is the same loud "no longer gated" error a reworded sentence already was. Two regression tests pin both, and the live file still catches a wrong count rather than passing vacuously. `check_tests_breakdown`'s docstring illustrated the row it parses with the day's real totals, which go stale by construction; it uses obviously illustrative numbers instead. `SKILL.md`'s error-code reference listed `W001` alone, where the registry also carries `W002` — the `async()` argument whose effects fall outside the commutative set and is therefore evaluated eagerly. Its line states what the diagnostic states. Co-Authored-By: Claude <noreply@anthropic.invalid>
Skip-changelog: one-sentence doc-accuracy fix inside the sweep PR Co-Authored-By: Claude <noreply@anthropic.invalid>
Eight findings, one round. E154's rationale claimed a consequence that cannot happen on three of the four rails. The prelude's reserved namespace holds six type ALIASES and five type PARAMETERS and nothing else, so there is nothing for a reserved effect, ability or constructor name to re-type — with the gate bypassed, a reserved-name constructor compiles and runs, returning 42. The rationale now branches the way the fix-text already did: the type/alias rail keeps the re-typing consequence, the other three state the forward reason aallan#1260 was decided on. A test asserts the branch per rail, and a second asserts the premise it rests on by walking the prelude — so a future prelude effect in that namespace fails there first. No automated gate can catch a false rationale; check_diagnostic_fields checks presence, not truth. The LSP fix from the previous commit was inert on the shipped path. server.py hands analyze() the document URI, and the pipeline uses its file= as a path — the module resolver reads imports from Path(file).parent, which for file:///a/b.vera is the directory `file:`. So a multi-module document resolved no imports, produced zero obligations and zero hints, and reported nothing: verify_source returns resolver errors as check_diagnostics, which analyze does not collect. uri_to_path joins the three coordinate conversions at that boundary, and Analysis carries both spellings because they answer different questions — the URI is what the client is told (a definition Location must carry one), the path is what the compiler was told and therefore what an obligation's file compares against. Non-file schemes pass through, which is what an unsaved buffer needs; LSP_SERVER.md's limitation row says so. E149's spec sentence enumerated Int and Nat only; it now states the Byte range and the refinement rule. A differential against the base measured the aallan#1252 radius: eight shapes reroute, and a join with more than one out-of-range literal now reports one error per literal instead of one about the branches disagreeing. Positions that never push the Byte expectation into the literal are unchanged. The CHANGELOG bullet says what was measured rather than the five sites originally claimed. Also: the corpus-count gate read TESTING.md alone, so CLAUDE.md's and AGENTS.md's citations went stale where the gate's own output could not show them — all three are read now, anchored on the script name rather than a bare numeral. Six temp-file sites in test_codegen_modules.py never unlinked; one shared helper parses and removes, which is this PR's theme and takes that file's stray count to zero. The three new conformance fixtures take a `reserved_name` family tag, since an effect name is not a type name. examples/README.md credited io_operations.vera with three operations it does not call; a sweep of every Demonstrates cell found no others. Co-Authored-By: Claude <noreply@anthropic.invalid>
uri_to_path raised an uncaught URLError on any file:// URI with a
non-localhost authority under Python 3.14, which is the project's own
venv: url2pathname validates the authority itself and raises before the
UNC fold that was meant to handle it ever ran. analyze() calls the
conversion outside its try/except and analyze_and_publish has none, so it
left the didOpen/didChange handler. The old fold was wrong on every
version, not only 3.14 — 3.13 returned a //host/... string, which on
POSIX is a stray local path rather than a UNC mount.
The authority is decided here now, so the answer no longer depends on the
interpreter: this process can only open a local file, so a remote
authority names none and the URI comes back unchanged, as the opaque
label the pipeline already carries for non-file schemes. Same for a
degenerate URI decoding to the empty string — an empty file= is not "no
file" downstream, it is the process CWD, which is how an unrelated module
gets pulled into an unrelated document — and for anything url2pathname
rejects, caught as a backstop so a future validation cannot reopen the
escape. file:/// still means the root directory, which IS a path. Scheme
matching is case-insensitive per RFC 3986. Tests cover the foreign
authority, an IP authority, both degenerate forms, the root URI, the
uppercase scheme, and analyze() itself over every shape.
A refinement predicate's operands are synthesised twice, so
{ @byte | @Byte.0 < 18446744073709551616 } drew two E149s for one literal
naming two different bounds; the existing duplicate collapse could not see
it, since the messages differ. The unconstrained pass is a guess — u64
because nothing told it the target — so a contextual verdict supersedes it
and the guess is withdrawn. The reverse never happens, and an
unconstrained verdict standing alone is the aallan#812 gate itself. Keyed on
the literal's occurrence, so two 999s in one call still report two errors.
Also from review: the module-fixture builders' docstrings claimed
resolved_module produced "a file the pipeline can open", which was never
true after the unlink — they differ by parse provenance, not by file
existence, and neither leaves a file behind; TESTING.md said the same
thing and a new test pins the real contract, including a cross-module
type-check against an already-deleted path. The corpus-count gate's
"reworded row is an error" held per document, so rewording one of
TESTING.md's two rows stayed green; each document now declares how many
citations it carries. The aallan#1252 CHANGELOG note gains the non-join count
increase: g(999) against a two-parameter g reports the range violation
beside the arity mismatch, both true.
Co-Authored-By: Claude <noreply@anthropic.invalid>
The warm session rooted a ModuleResolver at Path(file).parent whenever it
had a file at all, and a document naming no location gives '.' — the
process CWD. So an untitled: buffer, a non-file: URI, a degenerate file:
or file://, or an empty label searched for imports wherever the language
server was started; a probe measured an unrelated glib.vera being pulled
out of that directory into a document that never referred to it.
Pre-existing rather than a regression, and never silent — the imports it
did NOT find still warned E230 — but what it did find, it used.
The resolver is now built only when file names a directory that exists and
is not '.'; anything else gets resolved_modules=[] and is analysed alone,
its relative imports reported through the same E230 because they cannot
meaningfully resolve. The rule sits at the session so both verify_source
callers obey it rather than one call site getting a special case — and the
second caller needed it: speculative_edit still passed the raw URI, so
after analyze moved onto the path earlier in this cycle the proof delta
was comparing two differently-keyed streams. An identical-text edit
reported unchanged: 0 with every obligation removed. The suite missed it
because its baseline was a second verify_source call spelling the document
the same way the speculative side did; it goes through analyze now, as the
server does.
My earlier note claimed returning the URI unchanged from uri_to_path
prevented the CWD rooting. It does not — Path("file:") is exactly as
directory-less as Path("") — and the test pinned the returned string
rather than the property, so it passed for the wrong reason. Both
docstrings say what is actually true, and the reviewer's probe is now the
test: same source, analysed from a directory that holds an importable
module and from one that does not, asserting no obligation belongs to a
foreign file, with the importable-from-a-real-path premise beside it so
the pair cannot both hold vacuously.
Windows CI repairs, same seam: two new TestUriToPath assertions compared
url2pathname output against POSIX-shaped literals, which that converter
only returns off Windows. Both are relational now — case-insensitivity is
"every spelling gives the lowercase spelling's answer, and is not the
input", and file:/// is "converted, and the result has no filename and is
its own parent", which holds of / and \ alike. The other seven assertions
in the class were audited and are already portable: they compare against a
path the test built, or against the input returned unchanged. TESTING.md
gains the rule as the assertion-side twin of the two path rules it already
carries, and CLAUDE.md's "three Windows-portability rules" is now five,
with the two it had never listed.
Co-Authored-By: Claude <noreply@anthropic.invalid>
Rebasing onto 3a7e928 (PR aallan#1280) conflicted only in count-bearing prose and the negative-fixture rosters — no code file conflicted, and the diff-of-diffs confirms every one of the twenty-odd code files contributes byte-identically to what it contributed before the rebase. Both sides' additions are unions rather than choices. The conformance suite is 213: C8's three run-level programs and my three check-level negatives are disjoint. The corpus is 261. KNOWN_ISSUES' Bugs table is C8's row-id set exactly — aallan#1281, aallan#1277, aallan#1268, aallan#996 — with nothing dropped, nothing added and no duplicate aallan#1277, which was the specific hazard since C8's branch carried that row. CHANGELOG keeps all five [Unreleased] bullets from the conflicting section, three of C8's and two of mine, and the sections merged cleanly elsewhere. Every number here is the oracle's at the merged tree, not arithmetic on the two branches: 10,282 tests across 160 files, 213 conformance programs, 261 corpus programs, 38 check-level entries, 31 negatives. docs/ is regenerated rather than hand-merged. One repair the oracle could not have caught. Resolving the first conflicted commit with `git checkout --ours TESTING.md` replaced the whole file, discarding the roster edits the same commit had auto-merged into untouched regions — the counts stayed right while the prose naming the fixtures silently reverted. The remaining commits were resolved hunk by hunk instead, and the roster is restored and checked against the manifest: all 31 negatives named in TESTING.md, CLAUDE.md and AGENTS.md, six E154s in the E-code list, and the six skip-table rows back. A count gate cannot see a missing name, so that check is a set comparison against the manifest rather than a number. Co-Authored-By: Claude <noreply@anthropic.invalid>
The path-less isolation rule keyed on "the parent directory is '.'",
which is true of an untitled: buffer and equally true of entry.vera — a
real file whose directory happens to be the process CWD. So the rule
that stopped a path-less document borrowing the CWD's modules also took
the siblings away from a genuine relative-path one, measured at three
obligations instead of four with the import silently gone. is_file()
separates them: a document that exists on disk resolves against the
directory it actually lives in, whatever spelling names it.
analyze type-checks module-blind and then calls verify_source, which
type-checks module-aware, and only the second sees the resolver's errors
or anything needing an imported signature to detect. Those came back as
check_diagnostics and were dropped on the floor: glib::takes_int("nope")
published one warning, produced no obligations, and said nothing about
the E202 that had stopped verification; a missing import lost its E012
the same way. Appended now, minus what the blind check already reported,
because the module-aware pass re-derives those and a straight append
shows each twice — both halves are mutation-proved.
uri_to_path was still not total: urlsplit raises ValueError on a bad
authority (file://[ is "Invalid IPv6 URL") from inside the split itself,
before the guards that make the rest of it total, on the same
didOpen/didChange path the URLError escaped from.
Spec §4.2 described the integer range check in the wrong place. An
integer literal is always non-negative — a leading minus is negation over
the magnitude — so the upper bounds are checked on the literal and the
lower bound on the negation, whose operand may reach 2^63 and no further.
Both were already enforced; only the prose was wrong. Measured rather
than assumed: every IntLit the parser produces carries a non-negative
value, including for -9223372036854775809.
Also from review: the fixture builder's try/finally started after the
write, so a failed write stranded the file the contract promises to
remove; the strengthening-edit test still built its baseline from a raw
URI, so it passed whatever the delta said, and now goes through analyze
like its siblings, asserting that the surviving nat_sub obligation is
re-proved rather than replaced; TESTING.md's conformance-stage skip total
said 85 against a table of 91 and pytest's own 91, and is now gated
against that table — the third count in this PR that no gate was reading.
Two review findings verified and skipped. The scheme guard already
lowercases through urlsplit and is tested across three spellings. The
FAQ's 10,290 is the collected total, which is the convention the gate
reads and TESTING.md's headline uses; 10,126 is the passed count, and
that line is gated, at check_doc_counts' FAQ headline check.
Co-Authored-By: Claude <noreply@anthropic.invalid>
The leak fix from the previous round was green on POSIX and red on all three Windows cells. Two rules meet in that helper and the obvious arrangement satisfies only one: delete=False means the temp file outlives its with-block, so a failed write must still remove it — but Windows cannot delete a file whose handle is open, so the unlink I put in an except beside the write is PermissionError WinError 32 there, not a cleanup. That is TESTING.md's own first fixture rule, broken by the fix for its own corollary. One cleanup site now covers every path: the name is captured and the try entered before anything that can fail, the with closes the handle however it exits, and the finally unlinks after it. The sibling helper in test_codegen_modules.py had the same latent write-failure window and takes the same shape. The ordering is observable without a Windows machine — record whether the handle is closed at the moment each unlink is issued — so it is a test rather than a note, and it goes red on the exact shape CI rejected. An AST sweep for the general form (an unlink anywhere inside an open NamedTemporaryFile block) found that one site and now finds none; the first, text-based version of that sweep reported a clean zero because a multi-line with-header defeated its indentation scan, which is why it was rewritten before being trusted. TESTING.md records the sequencing corollary under the rule it belongs to, with both shapes. Also from review: the CHANGELOG still described resolved_module as producing "a file the pipeline can open" — the claim the docstring and TESTING.md had already been corrected away from in this PR, and the one place I missed. It now says what the other two say: parse provenance, deleted before return, neither builder leaving a file behind. Co-Authored-By: Claude <noreply@anthropic.invalid>
Hygiene tail: reserve every namespace, name the Byte range, one fixture helper (aallan#1228, aallan#1240, aallan#1246, aallan#1252, aallan#1260)
Cut the [Unreleased] section as 0.1.10: the handler-machinery consolidation that ends the aallan#1213 burndown. Each fact gets one derivation across the checker, verifier and codegen — the shared naming module, handler semantics, State/Exn family mangling, cross-module routing, boundary widths, and the clone namespace — with 37 bug-labelled issues closed against it. Version 0.1.9 -> 0.1.10 across the check_version_sync.py surface; HISTORY row added to the Stage 19/20 table; the aallan#1213 lead row deleted from ROADMAP.md's Stage 20 table, its one live pointer (aallan#1233) already tracked as a KNOWN_ISSUES.md limitation; site assets regenerated. Co-Authored-By: Claude <noreply@anthropic.invalid>
test_a_failed_write_leaves_no_temp_file snapshotted gettempdir() for *.vera either side of the call it measures. CI runs pytest -n auto, so that directory is shared by every xdist worker, each writing its own tmp*.vera: a sibling worker's fixture, alive for the microseconds between the snapshot and the assertion, counted as litter this test had left. It did -- AssertionError over a C:\...\tmp*.vera on worker gw1 in the v0.1.10 release push, an hour after the identical tree passed, and reproduced here at 210/300 with a second PROCESS writing into that directory. A thread cannot stand in for the worker: it reaches this process's patched globals, which no worker can, and produced failures of its own that the fixed test is right to ignore. The evidence is now the ONE path the call created, captured from NamedTemporaryFile the way the sibling ordering test captures handles. No shared directory is read at all, so the race is removed rather than relocated to a private TMPDIR -- which would still assert over a directory, and would additionally have to reset tempfile's cached tempdir for the env override to take effect. Same instrument: 0/300. A len(created) == 1 guard keeps the check from passing over an empty list should the builder stop creating its file that way. Both halves are mutation-validated: the pre-aallan#1282 leaking cleanup turns it red naming the stranded path, and switching the builder to mkstemp turns it red on the guard. The siblings from that PR were audited and need no isolation. test_the_handle_is_closed_before_every_unlink asserts over in-process traces (its own handle list and unlink log) that a separate worker cannot reach -- 0/60 under the same adversary -- and test_neither_builder_leaves_a_file_behind names its own unique path rather than reading the directory it sits in. TESTING.md records the rule under Test Fixture Conventions, where CI's parallelism makes it general: evidence about temp files names them. Also, from the release-surface audit: README's status line and HISTORY's "By the numbers" total both said 206 releases against 207 tags -- accurate at v0.1.5, two behind since v0.1.8, and agreeing with each other the whole way down, which is why the cross-check between them never saw it. Both now say 208 (207 tags plus the v0.1.10 tag release.yml creates after the merge), and check_doc_counts.py reads git tag as the oracle: exact equality once the version is tagged, the single pending tag of a release being cut as the only slack, and a printed skip where a checkout has no tags, since that is absence of evidence rather than zero releases. Co-Authored-By: Claude <noreply@anthropic.invalid>
Four behaviour fixes, each RED-proofed and differentialed; the rest of the 64 review findings are either doc/test corrections or verified invalid. `_compile_fn`'s old-state snapshot boundary caught `CodegenSkip` alone while the precondition and `decreases` boundaries either side of it catch `CodegenInvariantError` too, so `ensures(old(IO))` — check-green, because the checker types `old(E)` as an unknown type that satisfies a `Bool` postcondition — left `vera compile` as a raw traceback. It is the aallan#939 gap one boundary over and closes the same way, with a source-level reproduction rather than the monkeypatch its three siblings need. `_literal_range_error` could end a literal with ZERO verdicts: a contextual verdict superseding the unconstrained guess withdraws the earlier diagnostic but keeps its dedup key, so a contextual message that repeats it is collapsed as a duplicate and appends nothing. No .vera input reaches it — every transition the checker can take today re-renders the message — but the invariant is what the next contextual verdict rests on. `_handle_exn_always_throws` never asked whether the handler was an `Exn` one, and the structural walk routes every nested handler to it, so a `handle[State<T>]` was analysed with `throw_installed=True`. The answer authorises an `unreachable`; nothing reached a wrong yes, but only because a lowerable State clause body carries a tail `resume(...)`, which made the safety a property of the clause-lowering rule rather than of the predicate. Spec §7.5.1 claimed a bare function type and a non-resolving type expression were both refused by the compilability gate *before* reaching a cell and, in the same sentence, named a cell each. Naming is total and runs first; the refusals are downstream and at different gates — the unresolvable one at the compilability gate, the bare function type only when the function reading it is dropped, its cell declared in the meantime. DE_BRUIJN.md and the `vera/naming.py` docstring repeated the overclaim and are corrected with it. Test-logic: `test_verifier_calls_modules` anchored a demotion's line on `max(caller lines)` — a set the demoted obligation is itself in — so the equality held by construction and stayed green under the very mutant the docstring names. Also a keyword-only `file=` on both legs of the obligation- provenance fixture, a `direct=` matching production resolution, two fixture derivation guards, a pinned E532, a non-vacuity guard on the reserved-name regex, a subprocess timeout, and the LSP resolver-rooting table (six rows, mutation-validated red by dropping the `is_file()` disjunct). All 255 corpus programs emit byte-identical WAT and diagnostics either side of the four compiler changes (digest 5498bc77), and the two instrumented arms — the verdict restore and the snapshot invariant — fire zero times. Co-Authored-By: Claude <noreply@anthropic.invalid>
The final CodeRabbit round on the release PR measured four defects that are real but not minimal fixes on a frozen release tree; each is filed and now tabled, keeping the KNOWN_ISSUES Bugs table one-to-one with the tracker's open bug-labelled issues: - aallan#1284 user-defined `fn get`/`fn put` hijacked in handler clause bodies (three-way checker/codegen desync; gate-only fix measured to break WASM validation) - aallan#1285 `new(State<T>)` reads the name-keyed getter under a multi-`State` row where `old()` is family-keyed (runtime type mismatch from check-green source) - aallan#1286 `_infer_vera_type` never received the aallan#1276 branch-join fix its WAT-side siblings did (latent; no check-green reproduction yet) - aallan#1287 `_stamp_decl_order` skips the prelude stamp when a main-file `type` reuses a prelude name (latent; wrong index inherited by the next decl-order consumer) Skip-changelog: docs-only KNOWN_ISSUES tabling; the CHANGELOG records changes, and these are filings — each issue body carries the evidence. Co-Authored-By: Claude <noreply@anthropic.invalid>
Two findings from CodeRabbit's incremental review at 619e4aa: - The `<deep2>` alias-chain test aligned its parse/checker text last round but never asserted the check completes cleanly, unlike both its siblings (`<deep>`, `<sib>`); a future regression breaking the check pass for the 250-hop chain would have gone uncaught here. The sibling assertion is copied verbatim. - The codegen/ line-count table in vera/README.md drifted during the burndown inside the doc-counts gate's 10% band: nine module rows and the package total re-measured and corrected (18,093 -> 18,981 excluding __init__.py). The finding's list also named functions.py, tail_position.py and registration.py, which measure exactly as tabled and are unchanged. TESTING.md's per-file row follows the one-line test edit. Skip-changelog: a test assertion plus measured doc-count refreshes; no compiler or user-visible behaviour change. Co-Authored-By: Claude <noreply@anthropic.invalid>
Release v0.1.10 — the handler-machinery consolidation (aallan#1213)
…rammar The spec still called the assertion forms assert_stmt/assume_stmt after they became expressions (assert_expr/assume_expr in vera/grammar.lark), and three Lark rules appeared in no EBNF block at all: pure_effect and effect_set were inlined into effect_row, and with_clause was missing entirely, so the `with` form of a handler clause was undocumented as a production. scripts/check_grammar_alignment.py now holds the two files together in pre-commit and CI. Every rule header in one must exist in the other, with a six-entry allowlist for the pairs that differ on purpose: start/program, and the four spec headers Lark expresses as `-> alias` names or folds into a more general rule. Rule names only; bodies are not compared. Each entry records the side its name lives on plus the Lark alias its reason rests on, so the reason is checked rather than asserted — a name gone from both files is reported as a broken premise, not as "the sides now agree". Two more Chapter 10 defects go with it. `statement` carried `assert_expr SEMICOLON | assume_expr SEMICOLON` alongside `expr SEMICOLON`, so `assert(p);` derived two ways in the published grammar where the reference parser has one production. And a `RESUME: "resume"` terminal was declared but referenced by no production, contradicting the neighbouring note that `resume(expr)` parses as an ordinary fn_call; grammar.lark has no such terminal and binds resume as a plain LOWER_IDENT. The issue also asked to rename qualified_call to module_call in the Lark grammar. That is not done and should not be: both names are already there and they denote different constructs, Effect.op() and mod::fn(). A test pins that the gate never reports either name. Closes aallan#683
The premise check behind each ALLOWLIST entry could pass on facts that were not true. It searched the raw Lark text for the bare alias name, so a production commented out with `//` kept its own waiver alive through the deletion, and an alias that moved to a different rule kept it alive through the move. The two tuple entries were the worst case: `-> constructor_call` and `-> named_type` are the general constructor and named-type forms and occur file-wide, so their premises would have survived tuples leaving the language entirely. Aliases are now attributed to the production they are an alternative of -- in Lark, a header line plus its continuation lines -- and read from comment-stripped text through the one `strip_comment` helper both extractors already use. A waiver records `lark_rule` alongside `lark_alias`, and all four hold against today's grammar.lark. The tuple entries keep a checked premise (the alternative still sits on `fn_call` / `type_expr`) and now say plainly what it does not establish: that the alternative still spells a tuple is a body-level fact a header-only gate cannot see. Two smaller corrections ride along. A name could land in both the stale and the unsound bucket, telling the maintainer to delete a waiver and to restore what it names in the same run; the buckets are now exclusive. And the docstring called the leading-underscore hazard latent while the same "documented production, no tree node" situation is live sixteen times over via Lark's `?` marker -- verified against the built parser, none of the sixteen can appear as a node under its own name -- which is intended behaviour, not a gap, since Chapter 10 documents productions rather than the parse tree. The allowlist bound drops from 15 to 7, one above the six entries reviewed. At 15 the assertion admitted nine more entries without argument. Co-Authored-By: Claude <noreply@anthropic.invalid>
aallan
force-pushed
the
feat/issue-558-e130-slot-table
branch
from
August 13, 2026 08:14
c3f4682 to
4dfc13c
Compare
|
Skipping CodeAnt AI review — this PR changes more than 100 files, which usually means a migration, codemod, or vendored drop. Line-level review on diffs this large produces duplicate findings on the same rewrite pattern and drowns out anything that actually matters. If you still want a review, comment |
Chapter 1, Section 1.4 lists `resume` among the identifiers that MUST NOT be used as function names. Nothing enforced it, and unlike every other name on the E153 rail this one is not a declarable trap: `vera/grammar.lark` has no RESUME terminal, `resume` lexes as an ordinary LOWER_IDENT everywhere, so `private fn resume(@int -> @int)` parsed, type-checked, compiled, and a bare `resume(7)` outside a handler resolved to it and printed its result. The declaration is not merely permitted; it breaks working code. Inside each handler clause body the checker binds `resume` to the effect-resumption operator, typed from the handled operation's return type. With a top-level declaration in the same file, the clause bodies resolved against the *user's* signature instead: an otherwise valid `handle[State<Int>]` was rejected on `put(@int) -> { resume(()) }` with [E202] "has type Unit, expected Int", and with the declaration deleted the identical handler checked clean. Declaring one name silently invalidated a handler elsewhere in the file. So the declaration is refused at the checker -- the parser has no keyword to refuse it with -- on the existing E153 rail, in a fourth named piece (`_HANDLER_OPERATOR_FN_NAMES`) rather than folded into the keyword set. It needs its own rationale: the keyword branch says no unqualified call site can reach the declaration, which is false here, and the keyword set is pinned against a per-keyword test list `resume` does not belong in. The reservation is on declarations only, so `resume(...)` inside a handler clause -- bound by the handler, not declared -- is untouched, and a where-helper of that name is rejected one scope deeper like every other reserved name. The comment claiming the parser already refuses these declarations was false for `resume` and is corrected for the whole list it names: `with`, `effect`, `data` and their kind are refused at parse; `resume` is refused by neither parser nor the old checker set. Chapter 5 gains the third group, Chapter 10's note that `resume` is a plain LOWER_IDENT stays -- it is true at parse level -- and now says which phase enforces the reservation, so the two statements do not read as contradictory. E153's registry title drops "by the grammar", which is no longer true of every name it covers. The `w_resume.vera` probe asked whether the reserved-name machinery misfired on a where-helper of this name; its index row records the answer. Co-Authored-By: Claude <noreply@anthropic.invalid>
Deleting `RESUME: "resume"` applied a criterion -- a terminal declared in
Chapter 10's lexical grammar and referenced by no production is not inert
prose, because under the spec's own lexer it shadows the identifier terminal
it overlaps -- to one instance out of six. Applied to the rest of section
10.2 it clears five more phantom declarations and one omission.
`SOME` / `NONE` / `OK` / `ERR` were declared as keyword terminals and
referenced nowhere. `Some`, `None`, `Ok` and `Err` are ordinary prelude ADT
constructors (`data Option<T> { None, Some(T) }`, `data Result<T, E> { Ok(T),
Err(E) }`) and lex as UPPER_IDENT; the declarations would shadow UPPER_IDENT
and stop `Some(1)` parsing as a constructor call at all, exactly what RESUME
did to LOWER_IDENT. `COLON` was declared for a `:` that no production in
either file uses -- `vera/grammar.lark` contains no bare `":"` literal. All
five are deleted.
The converse case goes with them: `module_call` referenced `DOUBLE_COLON`,
which section 10.2 never declared. It is added as `DOUBLE_COLON: "::"`, the
spelling grammar.lark carries as an inline string literal.
The whitespace and comment terminals stay. They are labelled "(skipped)" in
the same block and `%ignore`d by grammar.lark, so being referenced by no
production is correct for them, not drift.
This commit fixes the six instances. It adds no machinery: the rule-name gate
compares rule headers only and never looked at terminals, so it is unchanged
and still reports 81 / 85 / 6 differ / 6 allowlisted. Auditing
declared-versus-referenced terminals as a gate remains aallan#1290's scope.
Verified with a by-hand audit of section 10.2's declarations against every
reference in the chapter's ebnf fences: five declared-unreferenced and one
referenced-undeclared before, none of either after.
Co-Authored-By: Claude <noreply@anthropic.invalid>
![codeant-ai[bot]](https://avatars.githubusercontent.com/in/646884?s=60&v=4){kind=small}
Review round on the reservation commit. Four of five findings held. The substantive one: rejecting the declaration was not the end of it. A bare call resolves lexically -- enclosing where-helpers, then the top-level function of that name, then the flat registry -- and the binding a handler clause installs for its body lives in that last tier. So a declared `resume` won the lookup and drew a SECOND error out of clause bodies that were correct: `put(@int) -> { resume(()) }` came back [E202] "has type Unit, expected Int" against the user's parameter, and its stated fix would have broken a working handler. Both shapes did it, top level and where-helper. `_lookup_function_scoped` now resolves a handler-operator name against the flat registry alone, which is the only place its binding can live. On a valid program this changes nothing -- the name is reserved, so no declaration of it exists in either scoped tier -- which is the narrowest form the fix can take. Skipping registration instead, as first tried, fixes the two handler shapes and breaks the third: an ordinary `resume(7)` call site then has nothing to resolve to, trading one spurious error for another. The prose that motivated the reservation described that cascade in the present tense, so it goes with it: the E153 rationale, Chapter 5, SKILL.md and the conformance fixture now say the declaration is refused and refused alone. CHANGELOG keeps the history. Also from the round: - SKILL.md opened the reserved-names paragraph "Two groups" and then listed three; Chapter 5 already said "and a third", this now matches. - TESTING.md's conformance-stage skip table was consistent with its own total and stale against the manifest: a check-level program contributes a test_verify and a test_run skip, which is the +2 the suite already showed. 89 level-limited rows + 4 environment-gated = 93. - vera/README.md claimed each conformance program tests one feature, where AGENTS.md and SKILL.md say some span several; 206 of the 214 manifest entries carry more than one feature tag, so the qualifier was the accurate one. Three tests: the wrong-typed clause `resume` the guidelines ask for as the partner to the correct-typed one (mutation-validated -- with the clause body left unchecked it goes red while its partner stays green, which is the point of having both), and one per cascade shape. Co-Authored-By: Claude <noreply@anthropic.invalid>
…alignment-gate fix(spec,tooling): align Chapter 10 EBNF rule names with the Lark grammar
An unresolved slot reference told you how many same-typed bindings were in scope and nothing else, so recovering the right index meant tracing pattern pushes and `let`s by hand, or writing a typed hole and re-running. `vera check --explain-slots` stops at the signature, which is where it stops being useful: a few levels into a `match` arm the stack has grown past anything the signature shows. The E130 fix text now ends with the table `_collect_scope_bindings()` already produces for the W001 typed-hole hint, rendered the same way and from the same set, so the read-time and write-time diagnostics agree. Nothing is appended when no binding is in scope, and the two narrow hints (aallan#973 handler state, aallan#969 where-helper) keep their tailored first sentence. That set is the whole scope, zero-size bindings included, because the index range in the description counts them: suppress them and one diagnostic describes two scopes, so `@Unit.1` against `(@Unit, @int)` reports "valid indices: 0..0" and offers a lower index above a table with no `Unit` row. Suppression buys little in return. Across the 2,126 slot-reference positions in `tests/**/*.vera` and `examples/`, dropping zero-size rows changes the table at 867 of them and empties an otherwise non-empty one at 2 — both `@Unit`-only handler-state fixtures whose real fix is the aallan#973 hint they already carry, and never at a position with nothing in scope. A zero-size read is E182's to explain, and it says to write `()` instead. SKILL.md's slot workflow now points at the diagnostic's own table rather than telling you to re-read the signature one, and bounds what it claims: `@T.result` is not a slot binding and never appears there, `ensures` included. This is the issue's option (a) only. The positional query (option (b), `--explain-slots-at <line>:<col>`) stays open, and the ROADMAP aallan#558 row now names it instead of the part that shipped here. The doc-count edits are the mechanical consequence of six new tests and fourteen new compiler lines, both of which `scripts/check_doc_counts.py` pins. TESTING.md's passed/stress/skipped breakdown is re-derived from a full run rather than carried forward (10,157 + 26 + 138 = 10,321), which is what v0.1.10's new breakdown check requires of it.
The only rendered E130 block in the repo stopped at "...or use a lower index.", which is where the diagnostic used to end. Nothing checks that a pasted ```text fence still matches the compiler, so the block went stale the moment the fix text grew a table. This one is re-pasted from `vera check` on §6.2's own program. What the fence now shows is worth a sentence, because on its face it reads as a contradiction: two entries whose type is `Int` sitting under "no `Metres` bindings in scope". They are not the same column. The left of each entry is a slot reference you can write, alias spelling intact; the right is what that reference resolves to. Writing `@Int.0` in that body reports no `Int` bindings above the same two entries — §6.1's opaque head, which is the rule §6.2 exists to demonstrate and the one place a reader is most likely to talk themselves out of it. Co-Authored-By: Claude <noreply@anthropic.invalid>
The table appended to `E130` grows one row per binding in scope, and the language server concatenates the fix into its hover message, so a wide function turns one diagnostic into a wall of rows nobody reads: thirty same-typed parameters rendered a 492-character fix. It now prints the first twelve rows and then `; … and K more`, where `K` counts the rows withheld. Twelve is measured, not picked. Across the 2,080 slot-reference positions in `tests/**/*.vera` and `examples/` the table is 7 rows at the 95th percentile and 11 at the 99th, so every position through the 99th still renders complete; 12 of the 2,080 elide, and the p95 segment length is 166 characters before and after. The same 30-parameter case now renders 255. Rows are dropped off the END, so a printed `@T.n` means what it meant uncapped — the boundary tests feed every rendered row back as the body and check it resolves. One rule, applied once. `_render_scope_table` is shared by the `E130` fix and the `W001` hole hint, which is what keeps those two from disagreeing about a scope they both describe. It is a rendering rule and deliberately not part of `_collect_scope_bindings()`, whose third consumer is the LSP typed-hole completion — there a dropped row is a missing completion item, so that path keeps every binding. Separately, SKILL.md tells the reader `@T.result` never appears in the table, `ensures` included. That was true and unpinned. The new test holds both halves: an out-of-range slot inside an `ensures` produces a table with no `.result` row, and the same `ensures` with an index the table offers still resolves `@Int.result` — so the omission is about what a slot binding is, not about `.result` being unavailable there. A future change to the collector now falsifies the sentence loudly. Co-Authored-By: Claude <noreply@anthropic.invalid>
The cap test asserted _SCOPE_TABLE_MAX_ROWS >= 12, which pins only the direction that truncates ordinary diagnostics. Every other test in the class derives its expectation from the constant, so a raised cap slid through the file unremarked: with the constant at 13 — and at 40, far past the corpus p99 — the pin still passed, while a raised cap re-widens the hover message the cap exists to bound. Equality makes moving the cap an edit to that line, with the corpus measurement (7 rows at p95, 11 at p99 across the 2,080 slot-reference positions) kept beside it to re-derive the new value from. TESTING.md carries the file's line count, so it moves with the docstring. Co-Authored-By: Claude <noreply@anthropic.invalid>
Both defects predate this branch and sit outside its diff; the review round surfaced them, so they land as a commit of their own. FAQ: the contract-testing walkthrough read `requires(@Int.1 != 0)` as constraining *the second* parameter. Under De Bruijn indexing `@Int.0` is the most recent binding, so `@Int.1` is the leftmost — the first. The slot spelling stays as written: the FAQ uses the same guard at two other points, and `examples/safe_divide.vera` — the example that same answer tells the reader to run three paragraphs later — guards `@Int.1 != 0` as its divisor and documents that slot as the first argument. Correcting the word puts all four back in agreement with DE_BRUIJN.md; re-spelling the slot to `@Int.0` instead would have split them. vera/README.md: the cross-cutting summary credited `errors.py` with the `E`-codes, where the `ERROR_CODES` description further down the same file counts 154 `E` codes and the two `W` warning codes. Now spelled `E`- and `W`-series diagnostic codes, matching that later wording. `docs/llms-full.txt` regenerates from FAQ.md via scripts/build_site.py. Co-Authored-By: Claude <noreply@anthropic.invalid>
aallan
force-pushed
the
feat/issue-558-e130-slot-table
branch
from
August 13, 2026 10:27
c11c8c8 to
64742de
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixes aallan#558
Scoped to option (a) only. Per your comment that (a) and (b) "are CLI-side and independent of the LSP, so they can land separately" —
--explain-slots-at <line>:<col>is not in this change, and the reporter withdrew (c).Summary
lets by hand, or writing a typed hole and re-running.vera check --explain-slotsstops at the signature, which is exactly where it stops being useful — a few levels into amatcharm the stack has grown past anything the signature shows.Fix:text now ends with the table_collect_scope_bindings()already produces for the W001 typed-hole hint (vera/checker/expressions.py:1174, used by the W001 path at:1198), rendered identically, so the read-time and write-time diagnostics agree. Eight lines at the E130 site.An earlier draft suppressed zero-size bindings — measured, and reverted
The reasoning was that reading a
Unitbinding is itself a hard error (E182), and that since@Unitentry points are the norm it would frequently be the only thing in scope, leaving a table whose one row is unusable. It produced a diagnostic that contradicts itself:The description says index 0 is valid, the fix says "use a lower index", and the table then omits
@Unit.0entirely — so reading the table you conclude noUnitbinding exists, and following the description you write@Unit.0and hit E182.Rather than argue it, I measured it across every slot-reference position in
tests/**/*.veraandexamples/— 503 files, 2,126 positions:So the premise was measurably false — the "frequently the only binding in scope" case is 2 positions out of 2,126, and both are
@Int.0with only@Unit.0in scope in handler-state tests that already carry the aallan#973 hint as their real fix. Meanwhile the divergence it introduced between two identically-labelled tables affects 40.8% of positions. Suppression also loses information in precisely the 2 cases it existed for: an empty table says nothing, where the full one correctly reports that the only binding in scope is aUnit.Dropping the filter is the smaller change too —
vera/checker/expressions.pyis +14 net lines rather than +21, and_collect_scope_bindingsstays a no-argument helper. E130 and W001 now print the same set under the same label, which was the stated goal.One claim went with it. The filter came with a guarantee that it ran after index assignment so no
@T.ncould shift — true, but vacuous:index_by_typeis keyed ontype_name, so only whole per-type runs can drop and a gap can never open. Neutering it left the suite green and 523 diagnostics byte-identical. Not worth keeping a tested-looking assurance nothing can test.Before and after, on the issue's motivating shape —
@Int.9insideAbs(@Term) ->:Only the
Fix:paragraph changes.Test plan
tests/test_checker_errors.py(56 → 62), written first. RED run: the one that passed initially is the no-bindings-in-scope case, which asserts the table is absent, so it is green by construction — called out rather than counted as evidence.-k SlotTableInE130(6 tests):test_e130_table_covers_the_indices_it_calls_valid,test_e130_and_w001_tables_agreeif scope:guardempty_scope_lists_nothingThe two new tests are RED on the pre-amend code and GREEN after, so they pin this change rather than the surrounding behaviour.
grep -rn "Ensure enough"hits onlyvera/checker/expressions.py, so no doc quotes the E130 fix text — the spec and SKILL passages that quote the E130 description are unaffected.scripts/check_diagnostic_fields.pygreen (the diagnostic keeps its rationale, fix, and spec_ref).mypy vera/clean,ruff check .clean.Full
pytest tests/andpre-commit run --all-filesgreen.TESTING.md's breakdown re-derived so it sums: 9,043 total = 8,910 passed + 26 stress + 107 skipped. It had stopped summing (8,908 + 26 + 107 = 9,041 against a stated 9,043) andcheck_doc_counts.pypins only the total, so the gate was green on a wrong addend. Cross-checked againstmain's 8,904 + 6 new tests.SKILL.mdstep 4 corrected — it claimed the table lists "every readable binding in scope at that reference", but@T.resultis readable inensuresand never appears (it isn't a slot binding). Confirmed:ensures(@Int.5 == 0)onfn f(@Int -> @Int)lists only@Int.0. Wording fixed rather than_collect_scope_bindings, which is pre-existing behaviour and out of scope here.Two things I'm leaving to you
fixfield is unbounded. 22 in-scope bindings produce a 423-character single line, in the terminal, in the JSON diagnostic, and appended to LSP hover text. No sibling diagnostic truncates, so there's no precedent to follow — and dropping the filter makes tables marginally longer, so this is slightly more visible than before.@Nat.0; @String.0; @Int.0; @Int.1; @Float64.0; @String.1; @Bool.0; @Int.2. For a diagnostic whose whole purpose is reading the right@Int.noff one line, grouping by type would probably serve better. Both traits are inherited from the W001 hint, so changing either changes that too — happy to do it if you want it.The doc-count edits are the mechanical consequence of adding six tests, which
scripts/check_doc_counts.pypins.