feat(inference): add xAI Grok provider (#425) - #10
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>
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-425-xai-grok-provider
branch
from
August 13, 2026 11:03
b8a8009 to
8a8fc2d
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 |
…t-table Put the in-scope slot table in the E130 error (aallan#558)
The transitive-caller closure was handler-unaware: a caller that
wrapped its call in handle[E] had E appended to its own effects(...)
row even though the handler discharges it there, so the workflow wrote
rows the program does not need and dragged that caller's own callers in
behind it.
A call site inside a handle[E] body now contributes no edge.
transitive_callers takes an optional effect argument (None keeps the
old handler-unaware closure, which the existing goldens still pin), and
_unhandled_callee_names subtracts the handled sub-tree from
direct_callee_names.
Two cases deliberately still propagate, because the effect really does
escape them: a caller that reaches the callee on any unhandled path as
well, and a call in a handler clause body, which runs outside its own
handler. Both are pinned by tests, and reverting either half of the
bound turns the matching test red.
Containment is structural rather than span arithmetic - identical
answers where both apply, no special case for a node with no span, and
it reuses the existing walk_nodes walker.
The handler has to name the same effect instance, type arguments and
all. The checker discharges against EffectInstance, whose equality
includes type_args, so handle[State<Nat>] does not discharge
State<Int>: pruning that edge on a base-name match would leave the
caller pure, never write the row it actually needs, and fail the whole
candidate on E125. Only an exact match prunes, and every other outcome
keeps the edge - a surviving edge writes a row the program may not
strictly need, which still type-checks. Row identity is a separate
question and stays the base name, so State<Int> is still not appended
beside an existing State<Bool>. Asking the same fixture for
State<Nat> is the positive control: that handler key does prune, so
the surviving State<Int> edge is attributable to the type argument
and not to a key nothing can match.
A refinement argument is one of those distinct instances, and the
narrowest way to get this wrong: format_type_expr renders
{ @int | p } as its bare base type, so a key built straight from it
spells Exn<Int> for a handler that discharges nothing of Exn<Int>, and
the pruned caller would keep pure while its call site fails E125. Any
argument holding a refinement - nested inside another type argument
included, since the renderer recurses - is spelled unmatchably
instead, so the edge survives. handle[Exn<{ @int | p }>] and
handle[Exn<Array<{ @int | p }>>] both check clean, so both are pinned,
end-to-end as well as at the closure.
The two remaining branches of the key are pinned too: an
unparameterised handle[IO] bounding an IO propagation (IO and Async are
what addEffect propagates most), whitespace-insensitive request
spelling, and handler nesting in both orders - a matching handler
inside a foreign one still bounds, and a foreign one inside a matching
one does not un-bound. handle[Mod.IO] is pinned at the key rather than
through a program: effects are only ever registered under an
unqualified name, so a qualified handler always fails E330 and no
program in which that key could prune ever type-checks.
where-block attribution is unchanged: a helper's bare call still
attributes to its containing top-level function, while a helper that
discharges the effect itself bounds the closure at its parent. Row
rewriting is also unchanged, and still top-level-only - a where helper
that needs the new effect does not get one, and the gate refuses that
candidate rather than applying it half-done.
The KNOWN_ISSUES.md and LSP_SERVER.md limitation rows are retired.
Three review fixes on the handler bound. They share lines in the module docstring and the CHANGELOG bullet, so they land together. The handler's STATE INITIALISER was documented as escaping the bound for the clause rule's reason, and nothing pinned it: patching _unhandled_callee_names to prune h.state as well left the whole suite green. It has its own reason - the initialiser is evaluated in the ENCLOSING scope, before the handler is installed, which is why _check_handle synths state.init_expr before it extends env.current_effect_row and why _translate_handle_state evaluates it before pushing the cell. The docstring now derives the two boundaries separately, and two tests pin them: the closure keeps an edge whose only call site is an initialiser (with a body call under the same handler spelling as the positive control that the key does prune), and the checker raises E125 on that call against a pure caller while the identical call in the handler body is clean. The comparison was documented as instance-for-instance in three places. It is not: format_type_expr does not resolve aliases, so the key compares the handle[...] head's SOURCE SPELLING to the request string, and handle[State<MyAlias>] with type MyAlias = Int does not bound a State<Int> propagation even though the checker discharges it. That under-prunes - the caller keeps a row it does not need, which still type-checks - so it is the safe direction and the key is left alone; aallan#1292 owns the swap onto resolved instances. The module docstring, the transitive_callers docstring and LSP_SERVER.md now say spelling, name the under-prune, and cite aallan#1292, and a test pins both halves on one fixture: the program is error-free (only possible if the alias-spelled handler discharges the State<Int> row its callee declares) and the State<Int> request keeps the edge, with the alias-spelled request as the control that does prune. The retired LSP_SERVER.md limitation row stated two things and only one of them is fixed, so the file boundary comes back as its own row. It carries no issue link, being deliberate behaviour rather than tracked work, with a note above the table saying so. Counts and llms-full.txt are refreshed from their oracles. Co-Authored-By: Claude <noreply@anthropic.invalid>
…er-aware-propagation Bound vera/addEffect propagation at handlers (aallan#725)
…#349) The issue's premise is stale. It cites 57.79% line coverage on `vera/browser/runtime.mjs` and asks for >80%; the actual figure at HEAD is 81.74%, so the target was already met before this branch existed. The parity tests added by aallan#707, aallan#744, aallan#856 and aallan#920 got it there. What this change delivers is not a rescued metric but coverage of the specific untested host imports the issue enumerates — several were registered yet never invoked, so their closure bodies had zero hits — plus two genuine parity bugs that fell out of writing them. 81.74% -> 86.86% lines, 82.99% -> 89.21% branches, 81.09% -> 88.05% functions. Measured with the command TESTING.md documents: `VERA_JS_COVERAGE=1 pytest tests/test_browser.py`, which is the same `npx c8 report --src=vera/browser/` invocation the browser-parity CI job uploads to Codecov. 33 cases in six classes. Each compiles one `.wasm` and runs it under both wasmtime and Node, so a failure isolates `runtime.mjs` rather than codegen. - Map: per-value-type and per-key-type variants over `map_get`, `map_size`, `map_values`, `map_keys`, `map_remove`. The first three and `mapAllocArrayOfStrings` had no browser-side caller. - Set: per-element-type variants over `set_to_array` and `set_remove`. `rebuildWithout`, 37 lines shared with `map_remove`, never ran. - Decimal: the exact-zero sign rule in `decAdd`, `decDiv`'s negative-shift arm, two `decRoundPlaces` special cases, `pyFloatRepr`'s exponential arm, `decimalAlloc`, `decimal_to_float`. - Json: `readJson` across all six ADT tags, plus `json_stringify`. - Error paths: the `Result.Err` arms of `regex_find` / `regex_find_all` / `regex_replace` / `json_parse`, and the `read_file` / `read_char` browser stubs. - Markdown: list lazy-continuation loops and the recursive descents in `hasHeading` / `hasCodeBlock` / `extractCodeBlocks`. Two browser/native divergences surfaced. Neither is fixed — fixing means editing `runtime.mjs`, which this change deliberately leaves alone. Each is recorded by asserting the native and the browser output as separate exact strings, not by an `xfail`. A bare strict `xfail` accepts *any* exception as the expected failure, so a broken compile, a dead Node harness or an unrelated `runtime.mjs` regression would all read as the known divergence. These two cases are the only browser-side coverage of `json_stringify` and `md_render`, so a real regression there would have been invisible. Pinning both strings tolerates the documented difference and nothing else: - `json_stringify` calls bare `JSON.stringify` where the native host calls `json.dumps`, so separators and integral numbers differ — `[1,2]` against `[1.0, 2.0]`. - `md_render` keeps a list item's lazy continuation on its own line where the native renderer joins it onto the item. Neither could have been caught before: neither builtin had a browser-side caller, and `examples/markdown.vera` is flat enough to miss the second. The 434 lines still uncovered are accounted for. 312 need a DOM or `XMLHttpRequest` (the Html and Http families) and cannot run under Node at all; 76 are defensive throws reachable only through memory corruption; 19 are WASM import kinds Vera never emits; 16 are the embedder host API the harness never calls; 5 are dead (`allocResultOkUnit` has no callers anywhere in the file); 6 are genuinely reachable. That puts the ceiling for this style of test at 87.04%. TESTING.md also claimed "61% JavaScript" in two places. That figure dates to v0.0.171 (be10658) and is not reproducible by any documented command — the one TESTING.md itself documents yields 86.86% for `runtime.mjs` and 87.06% across `vera/browser/`. Both now read 87%, which is correct under either reading. The adjacent "91% combined" figure is left untouched: deriving it needs a Python coverage total this change has no measurement for, and a guessed number is worse than a stale one. It needs its own fix. README.md's project-status line carried the same ambiguity in shorter form: "95% code coverage", unqualified, in the most-read file in the repo. That 95% is the Python figure on its own, and unqualified it reads as a whole-project total. It now says "95% Python code coverage". The combined figure stays out for the reason above. The `check_doc_counts.py` pattern that anchors the live test count on that sentence was updated to take the inserted word, so the count assertion keeps its anchor rather than silently matching nothing: perturbing the README count by one digit still fails with "README.md project-status tests: doc says 9071, live is 9070". Tests and docs only — no `vera/` or `spec/` file is touched, so the CHANGELOG gate does not apply. The count rows that `scripts/check_doc_counts.py` gates moved in `TESTING.md`, `README.md`, `ROADMAP.md` and `FAQ.md`, and the README pattern in the script itself moved with them; `docs/llms-full.txt` is the regenerated `scripts/build_site.py` output that embeds FAQ.md.
…eaks
The `md_render` divergence was recorded as "list lazy continuations".
That is the case that was found first, not the rule. Running both
runtimes over four shapes gives the actual scope: any multi-line
paragraph. The browser keeps the paragraph's internal soft line break
and does not re-apply the container prefix, where the native renderer
collapses it to a space — `hello\nworld` diverges with no list in
sight. Worse, the browser render is not a fixed point: re-rendering its
own output moves the continuation out of its container, so `> a b`
becomes `> a\nb` and then `> a\n\nb`, with `b` no longer quoted at all.
That breaks the round-trip property spec §9.7.6 states for `md_render`
itself, on top of §12.9.3's identical-results requirement. Parsing is
unaffected — the three predicates and the extractor are byte-identical
across the runtimes — so the defect is renderer-scoped. Tracked as
The nesting battery already compiles the destructive case — a
blockquote wrapping an h2 and a fenced block — but only substring-
asserts its render, so the strings were unpinned. They are pinned now,
both runtimes, both rounds:
native render 1 == render 2 (a fixed point)
browser render 1 loses the `> ` from the fence's contents
browser render 2 fragments the fence into three and lifts `x = 1`
clean out of the quote
The four assertions were confirmed to bite in the direction a fix would
move them: replacing each browser expectation with the native string —
what a repaired `runtime.mjs` would produce — fails the test, once at
`browser1` and, with that reverted, again at `browser2`. Both failures
print the real Node output, so neither assertion is vacuous.
`json_stringify`'s docstring claimed a fix would fail "the browser
assertion", singular. Measuring every `_JSON_TAG_CASES` entry against
both hosts puts the blast radius at five: this test plus `jarray`,
`jobject`, `nested` and `array_of_objects`, the four whose pinned
strings carry a separator or an integral number. The other seven are
already byte-identical. Tracked as aallan#1293.
`TestBrowserDecimalExact856` carried a private `_parity_stdout` that
had been duplicated to module scope for the aallan#349 classes; its nineteen
call sites now use the module-level helper with the `dec856` filename
passed through, and the surviving docstring no longer describes itself
as a mirror of something that no longer exists.
Three TESTING.md claims were also wrong. Action refs are not uniformly
pinned to major-version tags — `pypa/gh-action-pypi-publish` and
`codecov/codecov-action` are pinned to full commit SHAs, verified
against the workflows. The nightly-stress section cited
`actions/github-script@v7` where both workflows use `@v9`. And the
"91% combined" coverage figure is not derivable: the two collectors
measure different line populations, so blending them needs a
line-weighted total neither report produces. The two real figures, 95%
Python and 87% JavaScript, stay; the invented third is gone from the
overview table and the CI section both. The test-corpus estimate moves
from ~109,000 lines to the measured ~151,000 (151,297 by
`wc -l tests/test_*.py`).
Open CI/Tooling Issues had been emptied to "No open CI/tooling issues"
when aallan#349's entry was removed, though six remain open and verified as
such: aallan#1156, aallan#1103, aallan#712, aallan#540, aallan#402 and aallan#386. The table is back, with
one-line descriptions from the issues' own titles. aallan#712's row also
carries the gap this branch's own coverage work observed: `codecov.yml`
marks both JavaScript statuses `informational: true` with
`target: auto`, and `browser-parity` uploads `lcov.info` without
printing or asserting a percentage, so nothing holds `runtime.mjs`
above a floor the way `--cov-fail-under=80` holds the Python side.
Counts refreshed from `scripts/check_doc_counts.py` rather than by
hand: the new test moves the total to 10,347 across TESTING.md,
README.md, FAQ.md, ROADMAP.md and vera/README.md, and `docs/llms-full.txt`
is the regenerated `scripts/build_site.py` output that embeds FAQ.md.
Co-Authored-By: Claude <noreply@anthropic.invalid>
Both are open `bug`-labelled issues, so the KNOWN_ISSUES.md Bugs table owes them a row each under the one-to-one convention its own preamble states. any multi-line paragraph rather than the list lazy continuation first observed, the browser render unstable under re-render, the nested blockquote destroyed outright, and parsing unaffected — the three predicates and the extractor are byte-identical across the runtimes, so the defect is scoped precisely to the renderer. and integral-number rendering, plus the NaN asymmetry that folds in with them: the native host traps where the browser silently emits `null`. Neither host is individually wrong — §9.7.5 pins no output format — but §12.9.3 requires identical results, so the divergence is the defect, and the fix direction picks one canonical form per DESIGN principle 3. The CHANGELOG entry records the coverage battery and both divergences under [Unreleased], which also restores the `check_changelog_updated` gate: the rebase pulled `vera/README.md` into the diff, and a substantive path with no new entry is exactly what that gate blocks. Co-Authored-By: Claude <noreply@anthropic.invalid>
The table's own preamble claims it matches the open `bug`-labelled issues one-to-one, and two were missing: aallan#1288 from the v0.1.10 release recovery and aallan#1290 from aallan#1279's review round. Neither belongs to this branch's work, but the rows are owed whatever vehicle carries them, and this branch is already bringing the table current. Table now holds exactly the twelve open `bug`-labelled issues. aallan#1288 is release.yml's `Tag and create GitHub Release` step 422ing when the extracted CHANGELOG section exceeds GitHub's 125,000-character release-body limit. Size measured with the workflow's own extractor rather than taken from the issue: `scripts/release.py notes --version 0.1.10` produces 148,701 bytes / 147,919 characters, roughly 23,000 past the limit. What makes it worth a row is not the rarity but the landing point — it fires after PyPI has accepted the immutable archives and after the tag exists. aallan#1290 is the Chapter 10 drift a rule-name alignment gate cannot see. Worded against THIS branch's base rather than the issue's framing, because aallan#1279 is still open: `scripts/check_grammar_alignment.py` does not exist on `main` yet, so the row says the gate aallan#1279 *adds* will not see three classes of drift, not that a gate is failing to. All eight live instances were re-verified against the tree here rather than copied across: spec/10-grammar.md:63-66,99 SOME/NONE/OK/ERR/COLON declared, each appearing exactly once in the chapter — no production references them spec/10-grammar.md:323 module_call references DOUBLE_COLON, declared nowhere in the chapter spec/10-grammar.md:279-301 primary_expr has no "?" alternative; grammar.lark:199 has had one since 2026-03-30 spec/10-grammar.md:24 BLOCK_COMMENT's regex is non-nesting against spec/01-lexical.md:33 ("They nest") and against the parser, which takes `{- a {- b -} c -}` clean The six terminal instances are fixed on aallan#1279's branch (confirmed in its diff) and the row says so, so the row shrinks to its two body-level items when that merges rather than reading stale. Tracked-limitation count 50 -> 52, taken from `scripts/check_limitations_sync.py` rather than incremented by hand. No document cites that figure, so nothing else moved with it. No CHANGELOG entry: both issues stay open, so there are no release notes to write, and this PR's [Unreleased] bullet already covers its own work. Co-Authored-By: Claude <noreply@anthropic.invalid>
Four of the review round's seven findings were still valid at head. `test_read_file_is_err_stub_in_browser` did not pin what its docstring claimed. Against `nonexistent.txt` the native host returns `Err` too, so `value == 0` held on either runtime and the browser stub was indistinguishable from a genuine not-found — the assertion would have stayed green if `hostReadFile` were fully implemented. Confirmed before touching it: native `'err'`, browser `'err'`. It now writes a real file under `tmp_path`, embeds it with `.as_posix()` per the Windows rule, and pins both sides through `_both_stdouts` — native `ok`, browser `err`. Mutating the browser pin to `ok` fails, which the old shape could not do. `test_nested_walks_and_list_continuations` ran Node only while its class docstring asserted, in prose, that the three parse-side predicates match the native runtime. That claim is not decoration: it is what scopes aallan#1294 to the renderer rather than to the Markdown family, and this branch put it in KNOWN_ISSUES.md. It is now a differential — one module, both runtimes, trailing fields compared — so a native regression in the recursive descents reds instead of passing. Mutating the expected native field to `false` fails against the real `['true', 'true', '1']`. `FAQ.md` claimed the browser runtime "produces identical results to the wasmtime runtime" and that Markdown in particular "works identically". Both are contradicted by the two divergences this branch documents, and the contradiction is this branch's own doing — it filed them. Both sentences now name aallan#1293 and aallan#1294. `vera/README.md`'s parity sentence was example-scoped and stayed true, but carried an ungated hand-count of "56 mandatory parity tests" against a file now holding 172; the number goes in favour of the invariant plus the three pinned exceptions. `vera/README.md` disagreed with itself on the runtime family count in three places — `×14` with a fourteen-name list at line 148, "thirteen" without `db` at 573, "twelve adapters" twice at 575. Resolved against the codebase rather than by picking one: `vera/runtime/` defines exactly fourteen `register_<effect>` entry points, so line 148 was right and the other two are now fourteen, with `db` named in the list and given the one-clause description its siblings have. The three skipped findings, for the record: README.md:266 already reads "95% Python code coverage" (and the "91% combined" alternative is the figure this branch removed as underivable); the `aallan#390` reference in TESTING.md no longer exists and the pinning claim around it has been corrected against the workflows; and aallan#349's completion is recorded in CHANGELOG's `[Unreleased]`, with the HISTORY.md one-liner deferred to tag time per the release convention. No test count movement — both test changes are rewrites, not additions. `test_browser.py`'s line count moved and was re-derived from `scripts/check_doc_counts.py`. Co-Authored-By: Claude <noreply@anthropic.invalid>
…runtime-coverage test: cover browser runtime Map/Set/Decimal/Json host imports (aallan#349)
The grammars under editors/ enumerate the built-in effect names by hand and nothing checked them. They drifted: HttpServer, Inference and Random never reached the vscode and TextMate grammars, and DB (v0.1.7) reached none of the three until aallan#1155 fixed the Vim one. The drift is silent, so four accumulated unnoticed -- an unknown capitalised identifier falls through to the generic type-reference rule, so DB.query(...) still highlights as something, just not as an effect. scripts/check_editor_grammars.py reads vera.introspect.effects_payload() in-process and requires a word-boundary occurrence of every registered effect name in each grammar. Absence is conclusive, presence is optimistic, which is the right way round when the failure is omission and keeps the check immune to the three files' formats (JSON, plist XML, Vim regex). Written and run before the fix: 6/10 on vscode and TextMate naming DB, HttpServer, Inference and Random, 10/10 on Vim -- so the check discriminates rather than failing everywhere. Both alternations now carry all ten, with HttpServer before Http so the match does not depend on backtracking. The two extension READMEs listed the same stale six in prose. The checked list is explicit, since not every file under editors/ is a grammar, so it is paired with a completeness guard: a file in a syntax directory or carrying a grammar extension that the list does not name fails the gate with an instruction to add it. Otherwise the gate would have the same omission hole as the grammars it polices -- a fourth editor would get a green tick while knowing none of the effects. Registered as a pre-commit hook triggered by editors/ and by the registry files themselves, since adding an effect is what puts the grammars out of date. Hook count 32 -> 33 in CONTRIBUTING.md and TESTING.md. Two nearby prose defects go with it, both about this section's accuracy. The opener said every push is checked by all 33 hooks; the 31 commit-stage ones run at commit time, so it now states what the repository configures rather than what a push runs. And the trigger summary listed a closed set of paths -- .vera, vera/**/*.py, grammar.lark, the matching Markdown file, vera/browser/* -- that this hook's editors/ pattern is not among; it now names each hook's own files: pattern in .pre-commit-config.yaml as the authority and gives the common ones as examples. check_doc_counts.py reads the hook total out of the reworded sentence, so its pattern moves with it, and still fails both files when the number drifts. Abilities (Eq/Hash/Ord/Show) stay out of scope: whether they should highlight distinctly from ordinary types is an open design question. Closes aallan#1156
Review fixes for the editor-grammar gate. Four of them are about the gate itself; the fifth is a neighbouring check with the same defect. The registry read came from whatever `vera` the interpreter could import. `scripts/` is not a package, so `import vera` fell through to site-packages, and an editable install points at the main checkout -- from a git worktree the gate held one tree's grammars against another tree's effect list. A differential shows it: a checkout whose registry carries an eleventh effect `Telemetry` that no grammar names reported "OK: all 3 editor grammars carry all 10 built-in effects" and exited 0. With the in-repo bootstrap from check_corpus_canonical.py it exits 1 naming Telemetry in all three. A test pins it by running the gate as a subprocess against a throwaway checkout built the same way, which is the only way to see this -- in-process, `vera` is already imported. The primary failure path had no test. Deleting the `if missing` branch from `main` -- drift no longer fails the gate -- left the whole file green. It now strips `DB` from a mirrored grammar and requires exit 1 with the name in the report, and the deletion is caught. The completeness guard had two evasions. Suffix matching is on the whole filename, so `.tmlanguage` did not cover `vera.tmLanguage.json` -- the real vscode grammar's name -- filed anywhere but a syntax directory, and the tree-sitter editors keep their highlight queries in `queries/*.scm`, matching neither half of the guard. Both are listed now, each with a case in the parametrized guard test. Neither flags anything in the current tree. The two extension READMEs repeat the effect list in prose. They carried the same stale six, were hand-corrected with the grammars, and were left ungated, so the documented list could fall behind again with nothing to say so. They go through the same loop against the same registry; a mirrored README with `Random` removed is red. `check_doc_counts.py` read CONTRIBUTING.md's hook count behind a bare `if m:` -- a reworded sentence would switch the check off in silence, the failure its TESTING.md twin already reports loudly. Extracted as `check_contributing_hook_count` in the shape the file's other checks use, a missing sentence is now an error, and the reworded case is a test. The abilities note in the Vim syntax file pointed at aallan#1156, which this work closes; the open design question -- whether Eq/Hash/Ord/Show should highlight distinctly from ordinary types -- is now tracked in aallan#1295, and the roadmap's CI line carries it. Counts, site assets and the extension's own CHANGELOG follow: 10,336 tests, and a bullet for the grammar fix under an unreleased heading, since 0.2.1 is published. Co-Authored-By: Claude <noreply@anthropic.invalid>
The gate was added to `.github/workflows/ci.yml`'s lint job but not to TESTING.md's description of what that job runs, so the table enumerated 21 of the 22 scripts the job actually invokes and the one it omitted was the one this PR introduced. A differential over the two files is the check: before, `check_editor_grammars.py` was in CI and undocumented and the two lists were not even in the same order; after, both are 22 entries in identical order. The list is prose, so nothing gates it against the workflow — the same second-copy drift this PR's own gate exists to prevent, one layer out. Co-Authored-By: Claude <noreply@anthropic.invalid>
The row hand-enumerates every script the lint job runs, and nothing held the two in step. This PR walked straight into it: 3099640 had to correct the row by hand after d6d1eb0 added a lint step without it, leaving the table describing 21 of the 22 scripts the job invokes with every gate green. That is the same hand-enumerated-list drift aallan#1156's own gate exists to prevent, one layer out, so it is closed the same way. `check_ci_lint_scripts(testing_text, ci_text)` extracts the lint job's `run: python scripts/<name>.py` steps and compares them against the row's `.py` names. Three properties earn their own tests. The comparison is job-scoped, because every other job runs scripts too and a whole-file scan would report all of them as undocumented -- the fixture carries decoys in the test and security jobs, and `on:`'s two-space-indented `push:`/`pull_request:` keys, which a naive job scan would count. Order is compared, not just membership, since the row reads as the job's sequence and a set comparison would let a reordered row lie. And a row or job that cannot be found is an error, not a pass: rewording either side must not switch the check off in silence, which is the failure this whole script is written against. Mutation-validated on the artefact rather than the checker, since a doc gate's subject is the document. With the check wired in, dropping `check_editor_grammars.py` from the row exits 1 naming it; with the `main()` wiring removed, the same mutated row exits 0. That pair is the evidence, not the unit tests -- with the wiring removed and the tree pristine all nine still pass, because they call the function directly and cannot see whether `main()` calls it at all. Counts follow: 10,345 tests. Co-Authored-By: Claude <noreply@anthropic.invalid>
…ammar-gate ci: gate editor grammars against the effect registry (aallan#1156)
xAI's chat-completions endpoint is OpenAI-compatible: bearer auth and a
`choices[0].message.content` response. `_call_inference_provider` branches
only on `auth_style` and `response_style`, so supporting Grok needs no new
dispatch code — one row in `_PROVIDERS` is the whole change, which is what
the registry comment promises.
The default model is `grok-4.3`, not the `grok-3-mini-fast-beta` the issue
asks for. xAI no longer documents that name anywhere: the model list carries
grok-4.5, grok-4.3, the three grok-4.20 variants, and grok-build-0.1 with no
grok-3 family at all, and the retirement table that names a redirect target
for every withdrawn slug covers plain `grok-3` but not the `-mini-fast-beta`
variant. What the endpoint does when sent an undocumented name was never
tested against a live key, so nothing here claims a call-time outcome in
either direction — the default is simply a model xAI currently lists.
grok-4.3 is the cheapest of the current general-chat models ($1.25/$2.50 per
million in/out), which keeps the row on the cheap/fast tier its neighbours
use (`claude-haiku-4-5-20251001`, `gpt-4o-mini`, `mistral-small-latest`).
grok-build-0.1 is listed lower at $1.00/$2.00 but is a special-purpose build
model, not a general default.
The row is appended last. Insertion order is the auto-detect precedence
(the loop picks the first provider whose key is present), so appending
leaves the behaviour of every existing key untouched; a comment now says
so at the append point.
Six tests. Two were written before the row and confirmed failing on
"Unknown inference provider 'xai'", then re-failed when the row was
removed again, so they pin the registry entry rather than the dispatch
code they share with Mistral. The other four are one parametrized case per
provider ahead of xai — anthropic, openai, moonshot, mistral — asserting
that with that provider's key and `VERA_XAI_API_KEY` both set, the earlier
provider still wins. The names are literal rather than sliced out of
`_PROVIDERS`, because a derived list would shrink to match a relocated row
and pass vacuously; a single hardcoded 'anthropic' case would likewise stay
green while openai, moonshot, or mistral silently lost precedence. Relocating
the xai row fails exactly the providers it jumped: 4 red at the head of the
registry, then 3 before openai, 2 before moonshot, 1 before mistral. The
older `test_multi_key_auto_detect_respects_provider_order` stays green
through the same reorders because it reads its expectation out of
`_PROVIDERS`, which is why the append-last invariant needs its own coverage.
The dispatch test pins the exact request payload — `[{"role": "user",
"content": "prompt"}]` — instead of checking that a `messages` key exists.
A presence check does not discriminate: the payload builder was mutated
three ways, role flipped to `assistant`, content dropped, list emptied, and
the presence check stayed green on all three while the exact-value assertion
goes red on all three. The third argument is the model, not a system prompt,
so an empty string there selects the row's default and adds no system turn;
one user message is the whole body, which is the OpenAI-compatible shape the
endpoint expects.
Doc mirrors updated wherever the providers are enumerated: the spec §9.5.5
table, ENVIRONMENT.md, SKILL.md, AGENTS.md, FAQ.md, the landing-page copy
in scripts/build_site.py and docs/index.html, and the runnable-key header
comments in the two inference examples. ENVIRONMENT.md's local-run example
now points at the other keys instead of reading as Anthropic-only. The
landing-page feature blurb called `Inference.complete` "mockable", which
it is not — `handle[Inference]` is still open work (aallan#372) — so that word
is now "host-backed" on both the generator and the hand-written page. The
generated docs/ assets were rebuilt, and the test-count rows
check_doc_counts.py pins were bumped.
Closes aallan#425.
The `_PROVIDERS` registry defaulted each provider to its cheap/fast tier, and aallan#425 followed that convention for the new xAI row. The trade is wrong for a default: a program's contracts are written against what the default model can do, so capability is what the default owes the caller, and the cheap tier stays one `VERA_INFERENCE_MODEL` away. Every ID verified against the vendor's own live documentation: anthropic claude-opus-5 https://platform.claude.com/docs/en/docs/about-claude/models/overview Claude Opus 5 -- "Claude API ID: claude-opus-5" openai gpt-5.6-sol https://developers.openai.com/api/docs/models "gpt-5.6-sol" (alias "gpt-5.6"), "Frontier model for complex professional work" moonshot kimi-k3 https://platform.kimi.ai/docs/pricing/chat-k3 "kimi-k3" -- "Flagship model with a 1M-token context window" mistral mistral-large-latest https://docs.mistral.ai/api "mistral-large-latest" -- the alias Mistral's own chat-completion examples use, and the floating form the Mistral row already used xai grok-4.6 https://docs.x.ai/docs/models "For everything else, including code, use Grok 4.6. It is the most intelligent and fastest model we've built." The xAI row is grok-4.6, not the grok-4.5 a version-number guess reaches for: 4.5 and 4.3 are both still listed, so the ordering had to come from xAI rather than from the numbering. This also retires two IDs whose vendors no longer document them, `gpt-4o-mini` and `kimi-k2-0905-preview`, both reported in aallan#1263. Test-first: the five model assertions were flipped to the new IDs and confirmed failing against the old ones before the registry moved. Two of them could not have proved anything as written -- `test_openai_provider` asserted against `_PROVIDERS["openai"].default_model`, which pins the value to itself and would have stayed green through the flip, and `test_anthropic_provider` asserted no model at all. Both are literals now. Detecting an ID that rots at the vendor rather than in this repo still needs network access, and remains aallan#1263. Co-Authored-By: Claude <noreply@anthropic.invalid>
The provider registry's `default_model` IDs rot at the vendor, and aallan#1263 was open, unlabelled, and tracked nowhere. It is enhancement-class rather than a bug -- nothing in the repo is wrong, the world moves underneath it -- so it belongs on the ongoing CI/process/tooling thread rather than in KNOWN_ISSUES. The row states what the tests can and cannot see, since that distinction is the whole issue: pinning each ID to a literal catches an edit to the registry, but no offline assertion can catch a vendor delisting an ID. Co-Authored-By: Claude <noreply@anthropic.invalid>
Rebasing onto main moved every test-count surface, and the review raised two points that hold against the rebased tree. Counts, all oracle-derived rather than arithmetic on the old values: 10,478 collected (10,312 passed + 26 stress, 140 skipped) across the five documents check_doc_counts.py gates, and the per-file table row for test_codegen_host_effects.py at 1,036 lines. docs/llms-full.txt is a build_site.py regeneration, not a hand edit. TESTING.md's conformance section states each non-run level twice, as a number and as a hand-written list of program names, and neither is gated. ch05_reserved_resume_fn_rejected reached neither list, so the check level read thirty-eight against a manifest holding thirty-nine and the negative subset read thirty-one against thirty-two; the E-code sequence aligned to that subset "respectively" was short by the same one entry. The thirty-one codes that were present did pair correctly with the thirty-one names that were present, which is why the omission left nothing visibly wrong. The parametrized-suite count in the same section read 1,035 where the runner collects 1,070 -- five checks over each of the 214 programs -- drift of seven programs, predating that fixture. All four are now checked against the manifest as the single oracle. test_xai_provider asserts the request's Content-Type, which its OpenAI sibling already checked and the new row did not. Confirmed discriminating before it was kept: flipping the header in inference.py to text/plain fails the new assertion at its own line, and passes again on restore. Co-Authored-By: Claude <noreply@anthropic.invalid>
aallan
force-pushed
the
feat/issue-425-xai-grok-provider
branch
from
August 13, 2026 14:49
8a8fc2d to
55cdab8
Compare
![codeant-ai[bot]](https://avatars.githubusercontent.com/in/646884?s=60&v=4){kind=small}
All five verified against the branch tree before anything was written. SKILL.md said only "auto-detected from whichever key is set", which answers nothing when several are. The detection loop walks _PROVIDERS in insertion order and breaks on the first key present, so the rule is now stated with its order, and VERA_INFERENCE_PROVIDER is described as skipping detection rather than merely overriding it. The auto-detect tests asserted the provider NAME only. Dispatch passes (provider, prompt, model, api_key) positionally, so the key is index 3; both auto-detect tests now assert it. Confirmed discriminating: pinning the key lookup to VERA_XAI_API_KEY leaves every provider name correct and fails all four precedence cases on the key alone. FAQ.md claimed everything but json_stringify and md_render behaves identically in the browser. Two effects are refused outright there -- runtime.mjs returns an explanatory Err for Inference and for both DB ops -- so the answer now separates a deliberate platform boundary from the two unintended divergences, and notes Http really does work (XMLHttpRequest, not a stub) so the proxy advice is actionable. DB is named beside Inference; the finding mentioned only Inference, but the code refuses both identically. TESTING.md described check_doc_counts.py as verifying that counts cited in the docs match the codebase. The conformance-list drift fixed in the previous commit disproves that blanket claim, so the row now enumerates what the script reads and states that an unnamed count is not read. vera/README.md and host-families.svg both counted two stateful family adapters. There are three: register_async takes a future_store that execute() creates up-front, publishes it as host_store_refs["future"] for host_store_sizes, and has entries evicted by host_decref_handle kind 4, which also cancels an unstarted future (aallan#841). Prose, diagram label, legend and accessible title move together; the widened pill was checked for collisions in a renderer rather than assumed. Line count for test_codegen_host_effects.py re-derived to 1,046. Co-Authored-By: Claude <noreply@anthropic.invalid>
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#425
Summary
choices[0].message.content._call_inference_providerbranches only onauth_styleandresponse_style, so Grok needs no new dispatch code. One row in_PROVIDERSis the whole change, which is what the registry comment promises.https://api.x.ai/v1/chat/completions,VERA_XAI_API_KEY. The default model is not — see below.The model the issue specifies is no longer documented
The issue asks for
grok-3-mini-fast-beta. xAI's model list documents onlygrok-4.5,grok-4.3, the threegrok-4.20variants, andgrok-build-0.1— no grok-3 family at all.Default is
grok-4.3, the cheapest current general-chat tier ($1.25/$2.50 per M tokens), keeping the cheap-tier convention the registry already follows.grok-build-0.1is nominally cheaper at $1.00/$2.00 but is a special-purpose build model, so not a sensible general default.What I am deliberately not claiming. An earlier draft of this PR said shipping the issue's name "would make every
Inference.completecall fail." I never tested that — I verified the name is undocumented, which isn't the same thing, and a vendor may 404, error, or alias a withdrawn slug.xAI does publish a retirement page with a table mapping each withdrawn slug to a redirect target, stating "The slugs themselves continue to resolve, so you do not need to change your code to avoid breakage." That table covers plain
grok-3→grok-4.3but notgrok-3-mini-fast-beta,grok-3-mini-fast, orgrok-3-mini, and says nothing about slugs outside it. So "it still resolves" is plausible by analogy with the sibling slug and undocumented for the name actually requested. With noapi.x.aicredential I can't settle it, so nothing here asserts a call-time outcome in either direction — the default is simply a model xAI currently lists. (That page does independently support the tier choice: plaingrok-3's own redirect target isgrok-4.3.)Worth noting CI could not have caught the stale name either way. Every provider test asserts
sent_body["model"] == "<the literal from the registry>", so the test pins the value to itself and stays green regardless of whether the ID resolves. Same blind spot applies to the two names flagged at the bottom.test_multi_key_auto_detect_respects_provider_orderreadsnext(iter(_PROVIDERS))and would break on a prepend. There's now a comment at the append point saying so.On considering all three siblings
You noted that registry changes should consider aallan#450 (DeepSeek) and aallan#451 (Gemini) too.
response_style, so it needs a new dispatch branch rather than a registry row. That's a design question about how far the registry should stretch before it stops being a registry, and it shouldn't ride on a one-row PR.Files touched beyond the row
The provider list is enumerated in more places than the issue lists. Mirrored into the spec §9.5.5 table,
ENVIRONMENT.md,SKILL.md,AGENTS.md,FAQ.md, the landing-page copy inscripts/build_site.pyanddocs/index.html, and the runnable-key header comments in the two inference examples, thendocs/regenerated. The issue namesvera/codegen/api.pyandtests/test_codegen.py; both moved in aallan#421 and are nowvera/runtime/inference.pyandtests/test_codegen_host_effects.py. There is no README env-var table to update.Test plan
ValueError: Unknown inference provider 'xai'— so they pin the registry entry, not the dispatch code they share with Mistral.TestInferenceProviderDispatch's file.test_xai_providerasserts the endpoint URL,Authorization: Bearer …, absence ofX-api-key, the default model, and absence of Anthropic'smax_tokens— so an OpenAI/Anthropic mix-up in either direction fails.[{"role": "user", "content": "prompt"}], not just thatmessagesis present. The presence check it replaced passed with the role flipped, the content dropped, or the list emptied:"assistant"messages: []The same presence-only check remains on
anthropic,openaiandmistral, andtest_moonshot_providerhas nomessagesassertion at all — four tests, all pre-existing onmainand deliberately untouched here. The anthropic one looks the highest-value: its payload is the only one that differs (max_tokens: 1024) and nothing pins its turn list.test_xai_auto_detectasserts the key is picked up when it is the only one set; the existing multi-key precedence test still passes unchanged.xai, not just the first. The single-provider version it replaced stayed green if the row jumpedopenai,moonshotormistral— only a jump pastanthropicfailed it. Relocation matrix:xairow moved toopenaimoonshotmistralThe failure count equals the number of providers jumped. The parametrize list is a literal tuple, deliberately: a list sliced from
_PROVIDERSwould shrink along with a relocated row and pass vacuously.urllib.request.urlopenis patched, followingtest_mistral_provider.mypy vera/clean,ruff check .clean, conformance (179), examples (42), corpus canonical (227),check_site_assets.py,check_doc_counts.pyall green.pytest tests/andpre-commit run --all-filesgreen.Exercised against a live server, not only a mock
Every provider test in the suite patches
urllib.request.urlopen, so thebearer+openaiarms this row depends on had never met a real socket. Since the whole premise is "no new dispatch code is needed", I checked that end to end rather than trusting it:_call_inference_providercalled with no patching at all, against two live OpenAI-compatible endpoints, using a runtime-injected row of exactly this shape. Both returned real completions.vera run examples/inference.veradriven through the shippedxairow — auto-detect fromVERA_XAI_API_KEY, bearer header,choices[0].message.contentparsing, and the full compile → wasm → wasmtime → host-import → HTTP chain — returning a real classification.One honest limit: I have no
api.x.aicredential, so for the toolchain run the row'surlwas temporarily repointed at another OpenAI-compatible host and reverted immediately. That validates every part of the row and the path except that x.ai's own hostname accepts the request. Nothing in the tests or the diff touches the network — all committed tests remain mocked.Two model IDs already on
mainlook retired too — not touched hereFound while verifying this one; flagging rather than fixing, since neither is in this issue's scope and each deserves the same check:
gpt-4o-miniis absent from OpenAI's active model list; the cost-tier recommendation there is nowgpt-5.6-luna.kimi-k2-0905-previewis absent from Kimi's pricing page, which lists Kimi K3, K2.7 Code, K2.6, and Moonshot V1. Incidentally the spec's Moonshot docs host is stale as well —platform.moonshot.ainow 301s toplatform.kimi.ai.claude-haiku-4-5-20251001andmistral-small-latestI didn't check. Delisting isn't always removal from the API, so I'd rather not batch-edit them on a hunch — happy to file one issue covering the whole registry, or fold the fixes in here if you'd prefer.