Release v0.1.10 — the handler-machinery consolidation (#1213) - #1283
Merged
Conversation
…ruction (#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>
…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 #1208 / #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 (#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 #1208 / #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 #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>
`_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>
…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 #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 (#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 #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 #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 #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 #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>
) 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 #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 #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>
…1216, #1217) `vera test` resolves a parameter's type through the threaded naming environment before asking whether Z3 can encode it (#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 #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 (#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>
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 #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 #1209 family radius and the #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 (#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>
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 (#1218, #1219, #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>
…n-keyed origins (#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 #1222 row describing both failure directions. Also files #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 (#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 #1223 and #1222 now say what the code does. Review findings: §7.5.1's cell-identity rule is hedged by the mangle-safe-family gate (#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>
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 #1227 (codegen's global `_adt_layouts` versus module-scoped alias envs). Co-Authored-By: Claude <noreply@anthropic.invalid>
…view) Seventeen test files import it via vera.codegen.api's re-export; four via the defining vera.runtime.traps. Join the majority convention. Co-Authored-By: Claude <noreply@anthropic.invalid>
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 (#1216). - DE_BRUIJN.md quoted --explain-slots output with hand-aligned columns the tool does not emit, and no where-helper block (#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>
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 (#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` (#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>
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #1283 +/- ##
==========================================
+ Coverage 93.78% 94.05% +0.26%
==========================================
Files 99 100 +1
Lines 34669 35791 +1122
Branches 458 458
==========================================
+ Hits 32516 33663 +1147
+ Misses 2140 2115 -25
Partials 13 13
Flags with carried forward coverage won't be shown. Click here to find out more. ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
|
Important Review skippedReview was skipped as selected files did not have any reviewable changes. 💤 Files selected but had no reviewable changes (3)
⚙️ Run configurationConfiguration used: Path: .coderabbit.yaml Review profile: ASSERTIVE Plan: Pro Plus Run ID: 📒 Files selected for processing (3)
You can disable this status message by setting the Use the checkbox below for a quick retry:
📝 Walkthrough<hidden_new_layer> Additional compiler, WebAssembly, verifier, LSP, test, documentation, and configuration changes complete the review coverage.range_b69084e204f2 range_1102e2179d78 range_fd9a07f3fec9 range_f2b286f28f80 range_8b283aa504cb range_4f4edabae8f4 range_830a262823dd range_d9d15c7fe8b8 range_213e6d1c258c range_331b4db48669 range_f98faceb4e02 range_10e5ad578d24 range_254265b5215a range_dc6acc0ef7f5 range_741335666ce6 range_36402dab7523 range_5852129bc114 range_95c8b5745930 range_cc4d08417627 range_39d544afa814 range_e7c6669321a0 range_e77caebbd84b range_0e59def7441a range_b4608ebb31ac range_1a43aa6cb404 range_bcd558409f73 range_938a127766d1 range_25e8b4cf2082 range_580dac3e06a7 range_2ccf6ed00ae4 range_daa82d6b6ded range_a8d657ffe94a range_03f99abe215f range_52ee1447d989 range_9eba7b4143d5 range_21ec2e5b2939 range_c82c711d5d91 range_15955f146cb3 range_d18f81796beb range_0b19d06595d5 range_4fd32068bc1d range_81a600923f31 range_77fd25bc0789 range_604829cd0fe1 range_cae8e4248711 range_ba3715b3c597 range_1e21cadde3ee range_d31794511351 range_98829ee5286b range_1e21cadde3ee range_7a7693f9ea13 range_f59111e7ede5 range_967501c6796a range_6f43c786ff41 range_aa64164cd149 range_cdfec8567006 range_2a31d8972c85 range_ac505d3e9a03 range_bd24421d6e16 range_f06f6d6ee6f3 range_da8593031f12 range_f47013305c7a range_e3081ac7ca87 range_ecb51490a1cb range_d9d42d9aad75 range_c33768f393bb range_891d976ec733 range_10b6c0ac2ebd range_6c9b8747f241 range_f1998a673bce range_1330a1696209 range_8e4d65d2d52e range_4ea3bb3cd210 range_9651c4b4c741 range_c4352aaf63a5 range_f300975d44d2 range_085044aa8bc0 range_6453fb65c147 range_82d5df20624f range_d7bea54fad93 range_78c70bbcc1e4 range_dbbb3b8b7e78 range_284a2d9d91b3 range_034c291ad028 range_3e373de1dded range_7aa3aa6d0397 range_66ecb3223942 range_dd9fbc966df0 range_6d6695aad551 range_c2ae8d20502d range_a7ef4c766449 range_ad48df81d799 range_97898ff90da8 range_702200af2fff range_d93ba3e8c760 range_cfd611caeba7 range_ebb9e02ae415 range_1c00555bc0f3 range_09f048593a87 range_adf2664176d5 range_94ed6b0d8c2a range_8cce72023b3d range_a931aa1133ee range_e6a338702990 range_582b51ab41a2 range_ba01abdae990 range_10bce352252a range_2954993c22ad range_280684806072 range_c590374fdbbb range_edbad74026af range_2f11a19fc2a5 range_a7f6362c7239 range_9a97b04c318a range_23bf010dce95 range_8b2b12fbbffb range_4cb300e31030 range_3116c7d5bf3e range_f2c8d24b0f76 range_691fa4865c29 range_243af5e5eb76 range_67695829e9b0 range_241209db40a7 range_15622fd62af6 range_eb53933a55ac range_e966d8ae2521 range_a1ad62920ab2 range_84f1dd2e2c72 range_78d1dbf45c20 range_71d9e2dc3325 range_19b7db49f11c range_a449a9093502 range_e5a90b6fee01 range_a3e75be8be21 range_e2c945ab5d0d range_4ee81007f661 range_215724bdaa30 range_a0476563b07d range_77d3a6d1139b range_30ae87ee104b range_a2f7d891eab2 range_c6512d414910 range_4d864bbbcce0 range_338ddc03e617 range_0c47478cc56c range_e5ca622d7d01 range_a0d81044f7ec range_dee22a6b3bfb range_00e65fd5482a range_8cee88d21d85 range_704b34466805 range_ffae38f2b773 range_057b8b0566fd range_9eb170f7c613 range_71064e618fbe range_b9aaab74a40d range_96e5effc4012 range_43ae0094d448 range_1de4d44763f7 range_a6f35ba310ff range_865e09a7beef range_62add1e648e7 range_6452acceb8f3 range_a3680575de7a range_103fd7645f96 range_7a907b3c402e range_3a428cc5d264 range_7ee591be92e5 range_65759981616a range_66c715a58cdb range_c022d1df72fc range_3ac78137db4c range_7b1eba89eaab range_1b2d9b2c909a range_c139ff1e65eb range_61d88343a448 range_36fd7569ab27 range_80576e206903 range_bf53e955b374 range_66886b55dd25 range_75c119660614 range_bd54e2c9b590 range_c23b233abf18 range_86d9cecb31fc range_d33ac62d78f1 range_47437f0b9c64 range_50c9ac947617 range_190a7c9dcfd0 range_c22e9589a911 range_34a2b3502659 range_805762918cbb range_835adaab729b range_46f7a6bf9fcc range_0f914a98f448 range_ea36628d7a7c range_ebe9f5c9b207 range_039b98ab5cba range_55bd319ef0d8 range_7f0c3870925c range_14a355bec1ee range_99c21758dbd4 range_3e504999ce78 range_ad932ec9eb6f range_ff648f60a65a range_bcf5bf49518b range_8cbaad4731ef range_9adc5911e0e2 range_fc0f42fc50ef range_1d6e03d87393 range_ddf63e721540 range_e8f2c745456d range_503631bab1b3 range_7f8bfe96c967 range_4846cd6d3ac0 range_3115671cf1e1 range_7623be308ecf range_ed1808f48249 range_6a6d69beb5b0 range_d257dbffc79f range_18eee8961772 range_c3301aa33860 range_e55721daada8 range_738859d76abb range_db81aa44c7bb range_f1a834019dd0 range_d8ad439686a5 range_a36eeddc9a59 range_d37f4821a85f range_1e4231357742 range_0edf2cc0528a range_718b5325b339 range_24ca8d3fd52f range_9efcdc7e707c range_391ff1af945f range_b55ecfeb8ae6 range_c40906cc96f9 range_257cf1186bdf range_0aa4b79d7127 range_783531440463 range_dea80300f742 range_c2363953e967 range_48a3a93dbfb3 range_71a74f4eccb0 range_620bd60e297b range_0e9ee8919fcb range_ec330b2e5d10 range_c51fe851138f range_79ed524c3c53 range_c4f0d8fca3ad range_ef951046bc1e range_7bbd47d80443 range_a3772822fa89 range_3fd1ec31b13f range_86fb8a4b16ab range_ca2520174f24 range_ee1771b428b4 range_c369625a5db8 range_e87b2733a296 range_4e8227f7e961 range_af3c95c47bfe range_4bcec78d3a84 range_6381d109330e range_6f2db07625a2 range_a10a02597fa5 range_fd6d8d8c633d range_9b4bb4142579 range_f293633d7035 range_98811e2c230c range_bcee196d7b5b range_7a9d8011eec7 range_ee18843cc0d1 range_74e1881be069 range_fb8ce67c95d8 range_ed01d27a66c6 range_ffe314ba7706 range_10e5692a9d16 range_57b51bc8c47c range_c4f9ba1655d2 range_bb2d7f409993 range_f91c4ae0fdae range_690f4434f1a7 range_32aaa6fef8fc range_150f9a3d8b92 range_20ca45cfa500 range_7f8f609484b6 range_6306f0b7e7aa range_8a393dc73aaf range_c93441a66328 range_b07a45247e35 range_f7d47a937513 range_7d389bdf69d0 range_6a1c57067ef3 range_61aced647403 range_14f7aea50546 range_b5847d8b0fd7 range_f30b93b64de7 range_40eca3f4c0fb range_b699ae2fbd01 range_3e1a582332fb range_c43958d7dcba range_2b49418c1463 range_26e1b9c5a578 range_0136eba3e9ae range_11a458bb561d range_34bf2bd03141 range_62014403138b range_e9f57be46ef5 range_c3f0e70ef6cd range_a31144ef780d range_b3d1db03f9a2 range_b6e932af4cfc range_203a3442c9ec range_cf0907e5a7d8 range_3d719ea0b128 range_c2b5f216c7ee range_fbf773561404 range_fe35946744ac range_1a328738d3c6 range_c7fa23946314 range_128b8dd5c7db range_4796763c435f range_ec1d694c3641 range_7572850bb1dd range_2da56ca53b95 range_a914388884db range_4a475c3b7a86 range_84a9811a9dd3 range_0150368f0f84 range_b2183d69b8f6 range_4e0fc81a3c92 range_81282e8a1f6f range_2a4931ea4e4b range_765e57db5fba range_fb31c28bc7da range_97d4ea9239f1 range_4f719d9cc42b range_fd44581b67f5 range_c08938a3454b range_e31d474b5a61 range_6373dbd5c38f range_ec1e7f6b1070 range_863f5da818b1 range_3b221e653d0c range_a40913cb7f6f range_6efe01f9c624 range_9bdaa57db4f3 range_686edca0ea51 range_66d9cf7deb02 range_a475d0da869d range_70dab5e96d01 range_a2eae362c413 range_221f690fb6b8 range_2e82bf714786 range_396437dd4c88 range_6a37ce2542dc range_bfd5425cb93d range_7a9b305c3485 range_72706e3fc035 range_dd5c37fd8312 range_65181d44fa6f range_9f1255d4832d range_ebb1b947d378 range_aaedc2655203 range_927559d01bd5 range_5a7eec962dee range_8a53bec871a4 range_da2525d88902 range_744ace57d842 range_e3dffe234686 range_b53a778421e0 range_a2c15ac2c083 range_fc269e5bee7c range_1fa05810ece5 range_20e57e8b28ba range_146dde8bfe9f range_d704b8e49b20 range_03757f485773 range_3b0a02b83aa7 range_12c572d28510 range_0fda39052e5b range_81d4564b245d range_fafc991b646e range_7afa382486b4 range_9edb2fabba94 range_7094f2796940 range_6f853c2f3753 range_8f80e8a3290d🚥 Pre-merge checks | ✅ 5 | ❌ 3❌ Failed checks (3 warnings)
✅ Passed checks (5 passed)
✨ Finishing Touches 💡 1📝 Generate docstrings 💡
🧪 Generate unit tests (beta)
Comment |
Owner
Author
Release-surface audit record (
|
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 38
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (2)
vera/checker/expressions.py (1)
199-224: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick win
contextualshould mean "the target is a known integer type", not "an expected type exists".
contextual=expected is not Noneis true even whenexpectedis not an integer type at all — aStringannotation, an ADT field, aFloat64formal. In that casetargets_intis false, so the diagnostic still reports@Nat (u64), yet it now claims contextual knowledge. Because_literal_range_errorreturns early oncewas_contextualis true, that misleading verdict permanently blocks a later, genuine@Intor@Byteverdict for the same literal node.Gate the flag on the target actually being an integer type.
🐛 Proposed fix
base = base_type(expected) if expected is not None else None targets_int = (isinstance(base, PrimitiveType) and base.name == "Int") + # A verdict is CONTEXTUAL only when the target is a known integer + # machine type. A `String`/ADT/Float64 expected type tells this + # pass nothing about the bound, so its verdict stays provisional + # and a later `@Int/`@Byte verdict can still supersede it. + targets_nat = (isinstance(base, PrimitiveType) + and base.name == "Nat") bound = _I64_MAX if targets_int else _U64_MAX if expr.value > bound: type_name = "`@Int` (i64)" if targets_int else "`@Nat` (u64)" self._literal_range_error( @@ - # `expected is None` is a GUESS at `@Nat`, not knowledge - # of the target — a later contextual verdict wins. - contextual=expected is not None, + # An absent — or non-integer — expected type is a GUESS at + # `@Nat`, not knowledge of the target, so a later + # contextual verdict wins. + contextual=targets_int or targets_nat, )🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@vera/checker/expressions.py` around lines 199 - 224, Set the contextual flag in the integer literal range check to indicate that the resolved target is actually an integer type, rather than merely that expected is present. Update the contextual argument near targets_int to use the same integer-type determination, preserving non-contextual handling for String, ADT, Float64, or other non-integer targets so later integer verdicts are not blocked.vera/checker/resolution.py (1)
393-418: 📐 Maintainability & Code Quality | 🟠 Major | ⚡ Quick winRoute
_slot_ref_keythroughnaming.slot_ref_key, and refresh its now-stale docstring.Two points.
vera/naming.pyalready exportsslot_ref_key(ref, env), defined asslot_name(ast.NamedType(name=ref.type_name, type_args=ref.type_args), env).vera/wasm/operators.pyline 38 calls it directly. The checker instead reconstructs thatNamedTypeby hand inside_slot_type_name. Two hand-rolled spellings of one rule is the exact drift this consolidation removes elsewhere — ifnaming.slot_ref_keyever normalises the reference differently, the checker keys bindings one way and every other subsystem looks them up another, and a miss reads as "not statically known" rather than raising.The
_slot_ref_keydocstring still describes the removed mechanism: "_type_expr_to_slot_name→canonical_type_nameover resolved args". That import is gone.♻️ Proposed change: one construction, one renderer
def _slot_ref_key(self, ref: ast.SlotRef) -> str: """Binding-table key for a ``SlotRef``, keyed as ``bind()`` keys it. The `#309` / `#1160` provenance resolvers in :mod:`vera.checker.sql` need to look bindings up, and must do it with the CHECKER's renderer, not - the syntactic one in :mod:`vera.slots`. Binding keys resolve their - type arguments (``_type_expr_to_slot_name`` → ``canonical_type_name`` - over resolved args), so a syntactic render of ``@Array<Option<Txt>>`` + the syntactic one in :mod:`vera.slots`. Both sides route through + :func:`vera.naming.slot_ref_key` (`#1208`), which resolves type + arguments, so a syntactic render of ``@Array<Option<Txt>>`` where ``type Txt = String`` yields ``Array<Option<Txt>>`` and matches the ``Array<Option<String>>`` key not at all. A miss reads as "not statically known", so the check would silently do nothing — the exact failure `#1160` fixed one level up. """ - return self._slot_type_name(ref.type_name, ref.type_args) + # The argument diagnostics the old in-place composition emitted are + # kept by the reporting pass; the NAME comes from the one renderer. + self._check_slot_name_args( + ast.NamedType(name=ref.type_name, type_args=ref.type_args)) + return naming.slot_ref_key(ref, self._naming_env())I have not recommended caching
_naming_env, per the learning that measurements found no meaningful benefit and the alias registry changes through registration.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@vera/checker/resolution.py` around lines 393 - 418, Update _slot_ref_key to return naming.slot_ref_key(ref, self._naming_env()) instead of reconstructing a NamedType through _slot_type_name, using the shared renderer already exposed by vera.naming. Refresh the _slot_ref_key docstring to describe delegation to naming.slot_ref_key and remove references to the obsolete _type_expr_to_slot_name/canonical_type_name mechanism.Source: Learnings
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@assets/diagrams/README.md`:
- Line 70: Update the accessible title metadata in architecture.svg to include
the one-renderer note for naming.py, matching the SVG footer and vera/README.md
description.
In `@DE_BRUIJN.md`:
- Line 486: Clarify the paragraph’s cell-identity flow by distinguishing
resolutions rejected by the compilability gate from resolutions that reach cell
naming and use the alias-opaque fallback. Align the description of bare function
types, failed alias resolution, and fallback naming with the rule in
spec/07-effects.md §7.5.1, ensuring the text no longer implies the same cases
are both rejected and named.
- Around line 637-643: Update the recommended workflow’s step 2 to pass an input
path to vera check --explain-slots, using your_file.vera or - for stdin, so the
command is executable rather than relying on a pathless invocation.
In `@HISTORY.md`:
- Line 478: Update the v0.1.10 release row in HISTORY.md to contain one bold,
user-facing outcome clause and at most the existing issue link; remove the
em-dash implementation-detail list, preserving those technical details for
CHANGELOG.md.
In `@tests/probes/state_handlers/README.md`:
- Around line 45-48: Correct the documented diagnostic for the out-of-range Byte
literal in the affected test case to E149, matching the updated literal rule; if
retaining E170, explicitly identify it as historical behavior from before Byte
range validation.
In `@tests/test_callee_contract_scope_1220_1225_1226.py`:
- Around line 711-723: Strengthen the bounded-fact mutation in the test around
_PARAM_BINDER.replace by retaining the private fn mk contract with
requires(`@Nat.0` >= 18) and asserting the replacement changed exactly one
occurrence. Keep the replacement anchored to the private fn need18 header, then
preserve the existing >=100 assertion and verification checks.
- Around line 1255-1300: Update TestObligationsCarryTheirDeclaringFile to use
_ENTRY_FILE instead of every "main.vera" literal, including the file argument in
_verified’s typecheck and the assertion in
test_an_entry_located_obligation_keeps_the_entry_file. Keep the existing
provenance assertions unchanged so all verification and expected-length keys use
the same entry-file constant.
In `@tests/test_check_doc_counts.py`:
- Around line 199-237: Update _overview to format stress and skipped with
thousands separators, matching total and passed. Add
TestTestsBreakdown.test_thousands_separators_are_read_in_every_component using
component values above 1,000 and assert check_tests_breakdown returns no errors.
In `@tests/test_checker_modules.py`:
- Around line 110-125: Update the affected test to accept the pytest monkeypatch
fixture and use it to replace tempfile.NamedTemporaryFile and
pathlib.Path.unlink instead of assigning globals directly. Remove the manual
real_ntf/real_unlink保存 and finally restoration, while preserving the existing
patch behavior and assertions.
In `@tests/test_closure_boundary_widths_1255_1256_1269.py`:
- Around line 920-949: Parameterize _compile_xmod with a library-source argument
while preserving its existing parse/transform/resolve/compile pipeline and
resolver error assertion. Replace the duplicated setup in
test_the_width_assertion_can_go_red with _compile_xmod, passing the modified
library source, and keep the existing tag and i64.const assertions unchanged.
In `@tests/test_exn_throw_payload_1268.py`:
- Around line 107-109: Reuse a single result from _verify(src) in the test:
store the verification result before filtering its obligations, then use that
stored result for both coerce extraction and the assertion message instead of
invoking _verify twice.
In `@tests/test_generic_under_generic_callees_1223.py`:
- Around line 242-260: Update _registered_and_resolved to accept the pytest
monkeypatch fixture, replace the manual _monomorphize and _resolve_generic_call
save/restore logic with monkeypatch.setattr, and remove the corresponding
original-attribute variables and nested finally block. Keep the existing
compilation and temporary-file cleanup behavior unchanged.
In `@tests/test_handle_exn_divergent_result_1276.py`:
- Around line 338-344: Update test_unit_handler_wat_has_no_unreachable to
extract only the $main function body from the compiled WAT before checking for
“unreachable”; add the required re import and keep the assertion focused on
ensuring no divergence terminator is emitted in that handler body.
In `@tests/test_module_generic_namespace_1274.py`:
- Around line 403-410: Update the hand-built ResolvedModule chain fixture to
pass direct=(stem == "mid") for each module in the ("deep", "mid")
comprehension. Preserve the existing path, program, and source setup so mid is
direct and deep is transitive, matching production resolution.
In `@tests/test_nested_handler_clause_ops.py`:
- Around line 185-188: Add a derivation guard immediately after
_QUALIFIED_IN_CLAUSE is created, matching the existing guard for
_SAME_FAMILY_QUALIFIED: assert that the qualified fixture differs from
_PUT_IN_PUT_CLAUSE so a failed str.replace raises instead of silently producing
a duplicate fixture. Keep the existing replacement and expected behavior
unchanged.
In `@tests/test_phantom_generic_instances_1271.py`:
- Around line 88-100: Pin _CONCRETE_REQUIRED to the labels imported into
_ALL_CASES by adding an explicit set-equality assertion near these definitions.
Ensure the assertion fails when either _CASES gains a label missing from
_CONCRETE_REQUIRED or an existing label is removed upstream, while preserving
the current per-label concrete clone checks.
In `@tests/test_prelude.py`:
- Around line 390-400: Replace the hardcoded block-name tuple in the combinator
test with a derived set of module attributes, selecting every prelude symbol
whose name identifies a combinator block (the existing _OPTION_COMBINATORS,
_RESULT_COMBINATORS, _ARRAY_COMBINATORS, _JSON_COMBINATORS, and
_HTML_COMBINATORS pattern). Keep the existing getattr and bare-name assertions
unchanged so newly added combinator blocks are automatically covered.
In `@tests/test_verifier_shadow_audits.py`:
- Around line 75-89: Strengthen the obligation assertion in the result check to
include each obligation’s error_code alongside kind and status, and assert the
remaining call_pre tier-3 obligation has the claimed E532 code. Update the
diagnostic tuple in the failure message consistently, preserving the existing
filtering and expected single-obligation behavior.
In `@tests/test_walker_defensive_branches_597.py`:
- Around line 837-848: Construct the _FutureContract instance before entering
the pytest.raises block, then pass that prebuilt instance to
compilability.contract_exprs. Keep the TypeError expectation scoped only around
the dispatch call so constructor failures cannot satisfy the test.
In `@vera/checker/core.py`:
- Around line 529-548: Update the literal verdict handling around
_literal_range_verdict and _error so that when a contextual verdict withdraws a
provisional diagnostic but _error emits no new diagnostic because of
deduplication, the withdrawn diagnostic is restored and remains recorded as the
literal’s sole E149 verdict. Preserve the existing replacement behavior when a
new diagnostic is emitted, and add a regression test synthesizing the same
out-of-range literal first with expected=None and then with an `@Nat` expected
type, asserting exactly one E149 remains.
In `@vera/checker/modules.py`:
- Around line 259-275: Exclude mod.path when constructing or extending the
dependency frontier in the visible-module traversal, so the module being scoped
is never appended to its own result even through import cycles. Update the
traversal around by_path, direct, and frontier while preserving normal
dependency discovery and cycle deduplication.
- Around line 233-244: Replace the locally rebuilt seen set in the checker
diagnostic merge logic with the existing self._seen_diag_keys set. Build each
key using the current error_code, file, line, column, severity, and description
shape, check membership there, and add newly appended diagnostics to it before
updating self.errors. Preserve the existing deduplication behavior without
changing the key representation used by TypeChecker._error.
In `@vera/checker/registration.py`:
- Around line 287-290: Update the kind parameter of _check_reserved_decl_name to
use a typing.Literal containing the five noun values passed by its call sites,
so mypy rejects misspelled diagnostic nouns while preserving the existing
capitalization and lower-case formatting behavior.
In `@vera/checker/resolution.py`:
- Around line 10-11: Move the shared reserved-name regex from the private
_RESERVED_TYPE_PREFIX_RE in registration.py into the established public naming
or lexical module as RESERVED_TYPE_PREFIX_RE, preserving its pattern and
documenting its use across declaration, binder, and reference gates. Update
RegistrationMixin._check_reserved_decl_name and
ResolutionMixin._resolve_named_type, plus _check_reserved_type_params if
applicable, to import and use the shared public symbol without cross-module
private imports.
In `@vera/cli.py`:
- Around line 337-357: The location metadata construction should always emit the
file key because path is guaranteed to be a valid required input. In the
obligation serialization block, remove the conditional path guard and
unconditionally include file using o.file with str(p) as the fallback,
preserving the existing own-file preference.
In `@vera/codegen/api.py`:
- Around line 84-85: Add an [Unreleased] entry to CHANGELOG.md documenting that
CompileResult.state_types now uses tuple[CellNames, str] instead of tuple[str,
str], including the related register_state, WASI gate, execute(), and vera serve
behavior.
In `@vera/codegen/assembly.py`:
- Around line 438-459: Update compile_program() to catch CodegenInvariantError
raised by _assemble_module() at the assembly boundary and convert it into the
standard failed CompileResult with the existing [E699] diagnostic formatting,
rather than allowing a traceback to escape. Preserve normal successful assembly
and existing error handling behavior.
In `@vera/codegen/compilability.py`:
- Around line 270-302: Update _register_state_cell and _register_exn_tag to fail
closed when the derived family name (cell.family or type_name) is falsy: return
the existing unsupported/refusal reason instead of returning None or registering
nothing. Correct both docstrings to state that the functions return a reason
string on refusal and None on success, matching callers’ None checks.
In `@vera/codegen/contracts.py`:
- Around line 849-856: Reject non-State or missing-type-argument old()
references during checker validation instead of converting them to UnknownType.
Update the checker’s old-reference handling so invalid expressions cannot
satisfy postconditions and reach _collect_old_types; alternatively, catch the
state_type_arg failure and raise CodegenSkip before calling it. Preserve
existing behavior for valid State references.
In `@vera/codegen/core.py`:
- Around line 1400-1408: Update the declaration-order registration logic around
the early return so a prelude declaration always records its position in
_prelude_decl_order, even when name already exists in _decl_order. Preserve the
existing main declaration ordering and counters, and avoid overwriting an
already-recorded prelude position.
In `@vera/codegen/monomorphize.py`:
- Around line 254-260: Update the seed declaration construction in the
monomorphization flow to access CodeGenerator._imported_fn_decls directly
instead of using getattr, matching the direct access already used elsewhere such
as line 787.
In `@vera/environment.py`:
- Line 11: Update the deferred import handling in vera.environment to use
ast.AbilityConstraint for both deferred imports, reusing the existing
module-level ast import instead of importing AbilityConstraint from
vera.environment. Preserve the current deferred-import behavior while removing
both redundant local imports.
In `@vera/monomorphize.py`:
- Around line 1400-1408: Update the __init__ comment describing _op_result_types
to say that handler scopes use ordered merge semantics: inner effect-operation
mappings overwrite same-name outer mappings, while absent inner mappings
preserve outer mappings. Keep the implementation and the existing HandleExpr
behavior unchanged.
In `@vera/README.md`:
- Line 159: Update the Browser runtime line-count reference in the README from
~3,272 lines to ~3,303 lines, keeping it consistent with the runtime module
table and 3,409 JavaScript total.
In `@vera/wasm/calls.py`:
- Around line 435-441: Resolve the call route before invoking
_reject_unaddressable_clause_op, then use that resolved route for both
State-operation gating and dispatch. Ensure ordinary user-defined get or put
calls are not classified by _STATE_OP_NAMES when they resolve to a user
function, while actual State operations retain the existing rejection behavior;
add a regression test covering the inner clause and same-family enclosing cell
case.
In `@vera/wasm/helpers.py`:
- Around line 478-511: Update the local-binding rooting decisions in WasmContext
and the relevant data-generation paths to pass each binding’s resolved
representation base, using the established family/base-name resolution helpers
before calling is_gc_pointer_base. Preserve the separate zero-size Unit
handling, and add WAT coverage for let, let-destructure, and match-field
bindings to verify refined or aliased Byte values are not rooted.
In `@vera/wasm/inference.py`:
- Around line 203-215: Update _infer_vera_type to inspect each match arm in
order, skipping arms whose inferred type is absent, then fall back to the else
branch when no arm yields a type, matching the divergent-branch rule used by
_infer_expr_wasm_type. Preserve the checker’s behavior for NEVER-only branches
and add regression tests covering ADT-valued match/if expressions, structural
equality, show, and array-element inference.
In `@vera/wasm/operators.py`:
- Around line 1781-1789: Update _translate_new_expr to derive the State family
using _state_effect_family(expr.effect_ref), then select the getter associated
with that family instead of the shared _effect_ops["get"] entry. Preserve the
existing state_type_arg validation, missing-getter invariant error, and
call-target emission while ensuring each State type uses its matching getter.
---
Outside diff comments:
In `@vera/checker/expressions.py`:
- Around line 199-224: Set the contextual flag in the integer literal range
check to indicate that the resolved target is actually an integer type, rather
than merely that expected is present. Update the contextual argument near
targets_int to use the same integer-type determination, preserving
non-contextual handling for String, ADT, Float64, or other non-integer targets
so later integer verdicts are not blocked.
In `@vera/checker/resolution.py`:
- Around line 393-418: Update _slot_ref_key to return naming.slot_ref_key(ref,
self._naming_env()) instead of reconstructing a NamedType through
_slot_type_name, using the shared renderer already exposed by vera.naming.
Refresh the _slot_ref_key docstring to describe delegation to
naming.slot_ref_key and remove references to the obsolete
_type_expr_to_slot_name/canonical_type_name mechanism.
🪄 Autofix
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: 6ecf0dd6-23e6-47bd-83b1-f986f2fbf7d0
⛔ Files ignored due to path filters (159)
assets/diagrams/architecture.svgis excluded by!**/*.svgdocs/SKILL.mdis excluded by!docs/**docs/index.htmlis excluded by!docs/**docs/index.mdis excluded by!docs/**docs/llms-full.txtis excluded by!docs/**docs/llms.txtis excluded by!docs/**examples/array_utilities.verais excluded by!**/*.veraexamples/closures.verais excluded by!**/*.veratests/conformance/ch01_byte_literal_join_width.verais excluded by!**/*.veratests/conformance/ch02_alias_cycle_rejected.verais excluded by!**/*.veratests/conformance/ch02_refinement_base_param_alias.verais excluded by!**/*.veratests/conformance/ch03_slot_alias_type_argument.verais excluded by!**/*.veratests/conformance/ch07_clause_body_op_enclosing.verais excluded by!**/*.veratests/conformance/ch07_effect_op_source_order.verais excluded by!**/*.veratests/conformance/ch07_exn_composite.verais excluded by!**/*.veratests/conformance/ch07_exn_param_alias.verais excluded by!**/*.veratests/conformance/ch07_exn_scalar_alias.verais excluded by!**/*.veratests/conformance/ch07_exn_string_alias.verais excluded by!**/*.veratests/conformance/ch07_handler_registration_positions.verais excluded by!**/*.veratests/conformance/ch07_nested_handlers.verais excluded by!**/*.veratests/conformance/ch07_state_alias_chain.verais excluded by!**/*.veratests/conformance/ch07_state_alias_op_result_positions.verais excluded by!**/*.veratests/conformance/ch07_state_byte_join_writes.verais excluded by!**/*.veratests/conformance/ch07_state_clause_alias_slots.verais excluded by!**/*.veratests/conformance/ch07_state_clause_transform.verais excluded by!**/*.veratests/conformance/ch07_state_composite.verais excluded by!**/*.veratests/conformance/ch07_state_composite_alias.verais excluded by!**/*.veratests/conformance/ch07_state_composite_alias_cross_spelling.verais excluded by!**/*.veratests/conformance/ch07_state_fn_type_alias_cross_spelling.verais excluded by!**/*.veratests/conformance/ch07_state_handler.verais excluded by!**/*.veratests/conformance/ch07_state_nested_param_alias.verais excluded by!**/*.veratests/conformance/ch07_state_op_array_element.verais excluded by!**/*.veratests/conformance/ch07_state_op_generic_instantiation.verais excluded by!**/*.veratests/conformance/ch07_state_refined_cell_family.verais excluded by!**/*.veratests/conformance/ch07_state_scalar_alias_cross_spelling.verais excluded by!**/*.veratests/conformance/ch07_state_scalar_alias_widths.verais excluded by!**/*.veratests/conformance/ch08_reserved_vera_prefix_ability_rejected.verais excluded by!**/*.veratests/conformance/ch08_reserved_vera_prefix_binder_rejected.verais excluded by!**/*.veratests/conformance/ch08_reserved_vera_prefix_constructor_rejected.verais excluded by!**/*.veratests/conformance/ch08_reserved_vera_prefix_effect_rejected.verais excluded by!**/*.veratests/conformance/ch08_reserved_vera_prefix_reference_rejected.verais excluded by!**/*.veratests/conformance/ch08_state_alias_module_table.verais excluded by!**/*.veratests/conformance/ch08_state_alias_module_table_lib.verais excluded by!**/*.veratests/conformance/ch08_state_alias_per_module.verais excluded by!**/*.veratests/conformance/ch08_state_alias_per_module_lib.verais excluded by!**/*.veratests/conformance/ch09_generic_infer_user_fn_return.verais excluded by!**/*.veratests/conformance/ch09_generic_under_generic_callee.verais excluded by!**/*.veratests/conformance/ch09_generic_under_generic_depth_two.verais excluded by!**/*.veratests/conformance/ch09_generic_under_generic_prelude_callee.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/f1_cross_spelling.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/g1_array.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p11_xmod_alias_collision.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p12_cross_spelling.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p13_exn_cross.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p15_generic_elem.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p15b_append.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p15c_direct.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p17b_state_string_minimal.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p22_param_alias.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p23_alias_of_generic.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p24_exn_generic.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p25_refined_cell.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p2_chain.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p2_family_nested_alias.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p3_scalars.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p3a_self_param_cycle.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p3b_mutual_param_cycle.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p3c_byte_alias.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p3d_bool_float.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p6_main.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p7_exn_scalar.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p7_fn_alias_state_arg.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p7a_array.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p7b_match.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p7c_composite_alias.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p7d_eq.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p8_exn_string.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p8_xmod_alias_family.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p9_composite.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p9_exn_nested_alias.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p9_refined_state_minimal.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p_exnalias.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p_nested_app.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/statelib.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/x1_exn_string_alias.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/xmod_lib.verais excluded by!**/*.veratests/probes/state_handlers/checker_gates/e128_array.verais excluded by!**/*.veratests/probes/state_handlers/checker_gates/e337_user_effect_exn.verais excluded by!**/*.veratests/probes/state_handlers/clause_scoping/a11_refined_pattern.verais excluded by!**/*.veratests/probes/state_handlers/clause_scoping/p1b_nested_alias_clause_value.verais excluded by!**/*.veratests/probes/state_handlers/clause_scoping/p1d_single_alias_ref.verais excluded by!**/*.veratests/probes/state_handlers/clause_scoping/p4b_alias_arg_pattern.verais excluded by!**/*.veratests/probes/state_handlers/clause_scoping/p4e_fn_param_baseline.verais excluded by!**/*.veratests/probes/state_handlers/dispatch_paths/p9_cross_family.verais excluded by!**/*.veratests/probes/state_handlers/nested_handlers/p11_init_nested.verais excluded by!**/*.veratests/probes/state_handlers/nested_handlers/p13_exn_in_clause.verais excluded by!**/*.veratests/probes/state_handlers/nested_handlers/p17_string_outer.verais excluded by!**/*.veratests/probes/state_handlers/nested_handlers/p17c_option_outer.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/bare_obs.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_arg_if.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_bare33.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_bare_put.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_delegated_put.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_init999.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_init_if.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_let999.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_let_if.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_neg_composite.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_put42.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_put999.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_put_arith.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_put_if.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_refined_alias.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_refined_violating.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_resume300.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_resume9.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_resume_arith.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_resume_if.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_resume_lit.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_roundtrip.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_with77.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_with_lit.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/d1_literals.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/d2_block_tail_resume.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/mut_put.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p1.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p10_alias_nat_state.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p1205_neg.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p19_guard_bareput.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p1_put_no_clause.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p1_put_noclause.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p2.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p20_guard_init.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p21_guard_resume.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p2_put_with_clause.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p3.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p4.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p4_custom_effect_resume.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p4_refined.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p4c_byte_with.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p5_exn.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p5_get_resume_guard.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p6.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p6_init_guard_control.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p7_with_update_control.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p8_refined_state.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p8_resume_guard.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p8b_positive.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p_bytelet.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p_bytewith.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p_qualput_neg.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/pr_alias.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/pr_alias_min.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/pr_init.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/pr_init_req.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/pr_upd_req.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/pr_update.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/widen_ok.verais excluded by!**/*.verauv.lockis excluded by!**/*.lock,!uv.lock
📒 Files selected for processing (133)
.github/workflows/ci.yml.gitignore.pre-commit-config.yamlAGENTS.mdCHANGELOG.mdCLAUDE.mdCONTRIBUTING.mdDESIGN.mdDE_BRUIJN.mdFAQ.mdHISTORY.mdKNOWN_ISSUES.mdLSP_SERVER.mdREADME.mdROADMAP.mdSKILL.mdTESTING.mdTOOLCHAIN.mdassets/diagrams/README.mdexamples/README.mdpyproject.tomlscripts/check_debruijn_examples.pyscripts/check_doc_counts.pyspec/02-types.mdspec/03-slot-references.mdspec/04-expressions.mdspec/07-effects.mdspec/08-modules.mdtests/codegen_helpers.pytests/conformance/manifest.jsontests/module_fixture_helpers.pytests/naming_helpers.pytests/probes/README.mdtests/probes/state_handlers/README.mdtests/test_adt_membership_scope_1253.pytests/test_alias_application_refinement_base_1237.pytests/test_ast.pytests/test_byte_literal_joins_1212.pytests/test_callee_contract_scope_1220_1225_1226.pytests/test_check_doc_counts.pytests/test_checker_modules.pytests/test_checker_types.pytests/test_cli.pytests/test_clone_body_declaring_module_1241_1243.pytests/test_closure_boundary_widths_1255_1256_1269.pytests/test_closure_lift_boundaries_1234_1235_1245.pytests/test_codegen_collections.pytests/test_codegen_effects.pytests/test_codegen_modules.pytests/test_codegen_monomorphize.pytests/test_codegen_nat_guards.pytests/test_effect_op_determinism.pytests/test_exn_throw_payload_1268.pytests/test_family_naming.pytests/test_generic_under_generic_callees_1223.pytests/test_handle_exn_divergent_result_1276.pytests/test_import_visibility_entry_point_1244.pytests/test_lsp.pytests/test_module_generic_namespace_1274.pytests/test_mono_effect_op_naming_1207.pytests/test_monomorphize_differential.pytests/test_naming_env_provenance_1208.pytests/test_nat_int_widening.pytests/test_nat_narrowing_return_differential.pytests/test_nested_handler_clause_ops.pytests/test_obligations.pytests/test_phantom_generic_instances_1271.pytests/test_prelude.pytests/test_refinement_binder_convergence_1208.pytests/test_slot_naming.pytests/test_slot_naming_blast_radius.pytests/test_slot_naming_differential.pytests/test_state_exn_registration.pytests/test_tester_coverage.pytests/test_verifier_adt_decreases.pytests/test_verifier_calls_modules.pytests/test_verifier_mutation_obligations.pytests/test_verifier_nat_obligations.pytests/test_verifier_refinements.pytests/test_verifier_shadow_audits.pytests/test_walker_defensive_branches_597.pytests/test_wasm_coverage.pyvera/README.mdvera/__init__.pyvera/ast.pyvera/checker/calls.pyvera/checker/control.pyvera/checker/core.pyvera/checker/expressions.pyvera/checker/modules.pyvera/checker/registration.pyvera/checker/resolution.pyvera/cli.pyvera/codegen/api.pyvera/codegen/assembly.pyvera/codegen/closures.pyvera/codegen/compilability.pyvera/codegen/contracts.pyvera/codegen/core.pyvera/codegen/functions.pyvera/codegen/modules.pyvera/codegen/monomorphize.pyvera/codegen/registration.pyvera/codegen/wasi.pyvera/environment.pyvera/errors.pyvera/formatter.pyvera/lexical.pyvera/lsp/convert.pyvera/lsp/extensions.pyvera/lsp/features.pyvera/monomorphize.pyvera/naming.pyvera/obligations/core.pyvera/obligations/session.pyvera/prelude.pyvera/runtime/state.pyvera/skip.pyvera/slots.pyvera/smt.pyvera/tester.pyvera/types.pyvera/verifier.pyvera/wasm/async_fusion.pyvera/wasm/calls.pyvera/wasm/calls_handlers.pyvera/wasm/calls_markup.pyvera/wasm/closures.pyvera/wasm/context.pyvera/wasm/data.pyvera/wasm/helpers.pyvera/wasm/inference.pyvera/wasm/operators.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
Comment on lines
+435
to
+441
| # #1233: inside an inlined clause body, an outward-routed op of the | ||
| # SAME cell family cannot address the enclosing cell — the intrinsics | ||
| # only reach the innermost cell of a family. Refuse it here, before | ||
| # either dispatch below picks a route, so both the clause-inline and | ||
| # the bare-import path are covered by one gate (and so is the | ||
| # qualified `State.get`/`State.put` spelling, which delegates here). | ||
| self._reject_unaddressable_clause_op(call) |
There was a problem hiding this comment.
🩺 Stability & Availability | 🟠 Major | ⚡ Quick win
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# Description: Inspect the unaddressable-clause gate and its shadowing guards.
set -euo pipefail
rg -nP --type=py -C30 'def _reject_unaddressable_clause_op' vera
echo '--- shadowing guards used nearby ---'
rg -nP --type=py -C3 '_state_clause_ops|_known_fns' vera/wasm/calls_handlers.py | head -60Repository: aallan/vera
Length of output: 8353
🏁 Script executed:
#!/bin/bash
set -euo pipefail
printf '%s\n' '--- gate implementation and call dispatch ---'
sed -n '1738,1818p' vera/wasm/calls_handlers.py
sed -n '400,475p' vera/wasm/calls.py
sed -n '630,715p' vera/wasm/calls.py
printf '%s\n' '--- known-function and effect-operation initialisation ---'
rg -n -C5 --type=py 'known_fns|_effect_ops\s*=|_state_clause_ops\s*=' vera/wasmRepository: aallan/vera
Length of output: 29650
🏁 Script executed:
#!/bin/bash
set -euo pipefail
python3 - <<'PY'
import ast
from pathlib import Path
path = Path("vera/wasm/calls_handlers.py")
tree = ast.parse(path.read_text(encoding="utf-8"))
gate = next(
node for node in ast.walk(tree)
if isinstance(node, ast.FunctionDef)
and node.name == "_reject_unaddressable_clause_op"
)
print(f"gate_lines={gate.lineno}-{gate.end_lineno}")
print(ast.unparse(gate))
# Print the direct call sites and the enclosing function names.
for node in ast.walk(tree):
if isinstance(node, ast.Call):
func = node.func
if isinstance(func, ast.Attribute) and func.attr == "_reject_unaddressable_clause_op":
parent = next(
(
candidate for candidate in ast.walk(tree)
if isinstance(candidate, (ast.FunctionDef, ast.AsyncFunctionDef))
and candidate.lineno <= node.lineno <= candidate.end_lineno
),
None,
)
print(f"call_site_line={node.lineno} enclosing={getattr(parent, 'name', None)}")
PYRepository: aallan/vera
Length of output: 3300
🏁 Script executed:
#!/bin/bash
set -euo pipefail
python3 - <<'PY'
import ast
from pathlib import Path
path = Path("vera/wasm/calls_handlers.py")
tree = ast.parse(path.read_text(encoding="utf-8"))
gate = next(
node for node in ast.walk(tree)
if isinstance(node, ast.FunctionDef)
and node.name == "_reject_unaddressable_clause_op"
)
print(f"gate_lines={gate.lineno}-{gate.end_lineno}")
print(ast.unparse(gate))
for node in ast.walk(tree):
if isinstance(node, ast.Call):
if isinstance(node.func, ast.Attribute) and node.func.attr == "_reject_unaddressable_clause_op":
parents = [
candidate for candidate in ast.walk(tree)
if isinstance(candidate, (ast.FunctionDef, ast.AsyncFunctionDef))
and candidate.lineno <= node.lineno <= candidate.end_lineno
]
parent = min(parents, key=lambda candidate: candidate.end_lineno - candidate.lineno)
print(f"call_site_line={node.lineno} enclosing={parent.name}")
PYRepository: aallan/vera
Length of output: 3300
🏁 Script executed:
#!/bin/bash
set -euo pipefail
printf '%s\n' '--- call dispatcher from entry to user-function fallback ---'
sed -n '1,115p' vera/wasm/calls.py
sed -n '475,625p' vera/wasm/calls.py
printf '%s\n' '--- state operation names and declarations/resolution rules ---'
rg -n -C8 --type=py '_STATE_OP_NAMES|reserved.*(get|put)|\b(get|put)\b.*(known|function|effect)|E15[0-9]|E152|duplicate.*(function|effect)' vera tests spec
printf '%s\n' '--- direct user-function shadowing tests and fixtures ---'
rg -n -C8 --type=py 'fn (get|put)|def test_.*(get|put)|shadow.*(get|put)|known_fns' tests veraRepository: aallan/vera
Length of output: 50368
🏁 Script executed:
#!/bin/bash
set -euo pipefail
python3 - <<'PY'
import ast
from pathlib import Path
for filename in ("vera/wasm/calls.py", "vera/wasm/calls_handlers.py"):
tree = ast.parse(Path(filename).read_text(encoding="utf-8"))
print(f"--- {filename} ---")
for node in ast.walk(tree):
if isinstance(node, ast.Assign):
for target in node.targets:
if isinstance(target, ast.Name) and target.id == "_STATE_OP_NAMES":
print("STATE_OP_NAMES:", ast.unparse(node.value))
if isinstance(node, ast.FunctionDef) and node.name in {
"_translate_call", "_reject_unaddressable_clause_op"
}:
print(f"{node.name}: lines {node.lineno}-{node.end_lineno}")
for child in ast.walk(node):
if isinstance(child, ast.If):
test = ast.unparse(child.test)
if any(token in test for token in (
"_known_fns", "_STATE_OP_NAMES", "_state_clause_ops",
"_effect_ops", "_effect_op_cells",
)):
print(" guard:", test)
PYRepository: aallan/vera
Length of output: 609
🏁 Script executed:
#!/bin/bash
set -euo pipefail
printf '%s\n' '--- exact _translate_call dispatch ---'
sed -n '31,75p' vera/wasm/calls.py
sed -n '500,610p' vera/wasm/calls.py
printf '%s\n' '--- exact shadowing fixture ---'
sed -n '2718,2785p' tests/test_nat_narrowing_return_differential.py
printf '%s\n' '--- checker resolution and effect-op registration references ---'
rg -n -C4 --type=py 'known_fns|effect_ops|user.*function|function.*effect|shadow' vera/checker vera/wasm | head -240Repository: aallan/vera
Length of output: 30558
🏁 Script executed:
#!/bin/bash
set -euo pipefail
python3 - <<'PY'
import ast
from pathlib import Path
path = Path("vera/wasm/calls.py")
tree = ast.parse(path.read_text(encoding="utf-8"))
fn = next(
node for node in ast.walk(tree)
if isinstance(node, ast.FunctionDef) and node.name == "_translate_call"
)
for node in ast.walk(fn):
if isinstance(node, ast.If):
test = ast.unparse(node.test)
if any(x in test for x in (
"_known_fns", "_state_clause_ops", "_effect_ops",
"_reject_unaddressable_clause_op",
)):
print(f"lines={node.lineno}-{node.end_lineno}")
print(f"condition={test}")
print(f"body_first={ast.unparse(node.body[0])[:300]}")
PYRepository: aallan/vera
Length of output: 791
🏁 Script executed:
#!/bin/bash
set -euo pipefail
printf '%s\n' '--- checker call-resolution functions ---'
rg -n --type=py 'def .*call|FnCall|effect.*op|known.*fn|function.*name' vera/checker vera | head -180
printf '%s\n' '--- handler clauses containing calls to user-defined get/put ---'
rg -n -U --type=py -P 'fn (get|put)\b[\s\S]{0,500}handle\[[\s\S]{0,1200}\b(get|put)\s*\(' tests
rg -n -U --type=py -P 'handle\[[\s\S]{0,1800}(get|put)\([^)]*\)[\s\S]{0,1800}fn (get|put)\b' tests
printf '%s\n' '--- handler registration of get/put cell metadata ---'
sed -n '1548,1665p' vera/wasm/calls_handlers.pyRepository: aallan/vera
Length of output: 39260
🏁 Script executed:
#!/bin/bash
set -euo pipefail
python3 - <<'PY'
import ast
from pathlib import Path
for filename in ("vera/checker", "vera/wasm"):
root = Path(filename)
print(f"--- {filename} ---")
for path in root.rglob("*.py"):
tree = ast.parse(path.read_text(encoding="utf-8"))
for node in ast.walk(tree):
if isinstance(node, ast.FunctionDef):
source = ast.get_source_segment(
path.read_text(encoding="utf-8"), node
) or ""
if (
"FnCall" in source
and any(term in source.lower() for term in (
"effect", "operation", "known_fn", "function call"
))
):
print(f"{path}:{node.name}:{node.lineno}-{node.end_lineno}")
PYRepository: aallan/vera
Length of output: 1255
🏁 Script executed:
#!/bin/bash
set -euo pipefail
printf '%s\n' '--- bare-call checker precedence ---'
sed -n '108,210p' vera/checker/calls.py
sed -n '670,730p' vera/checker/calls.py
printf '%s\n' '--- handler and clause-body checking ---'
sed -n '640,735p' vera/checker/control.py
rg -n -C12 --type=py 'clause\.body|clause.*state_update|_check.*clause|check.*clauses|Handle' vera/checker
printf '%s\n' '--- user-name registration restrictions ---'
sed -n '1,115p' vera/checker/registration.py
sed -n '285,330p' tests/test_mono_effect_op_naming_1207.pyRepository: aallan/vera
Length of output: 50367
🏁 Script executed:
#!/bin/bash
set -euo pipefail
python3 - <<'PY'
import ast
from pathlib import Path
paths = [
Path("vera/checker/calls.py"),
Path("vera/checker/control.py"),
Path("vera/checker/registration.py"),
]
for path in paths:
source = path.read_text(encoding="utf-8")
tree = ast.parse(source)
print(f"--- {path} ---")
for node in ast.walk(tree):
if isinstance(node, ast.FunctionDef) and node.name in {
"_check_call_with_args",
"_check_handle_state",
"_check_handle",
"_check_fn_call",
"register_function",
}:
print(f"{node.name}: {node.lineno}-{node.end_lineno}")
print(ast.unparse(node)[:5000])
PYRepository: aallan/vera
Length of output: 7693
Resolve the call route before applying the State-operation gate. The checker resolves a same-named user function before an effect operation, but the gate checks only _STATE_OP_NAMES. An inner State<T> clause can therefore raise CodegenSkip for an ordinary user get or put call when an enclosing handler exposes the same-family cell. Use the resolved route for both the gate and dispatch, and add a regression test.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@vera/wasm/calls.py` around lines 435 - 441, Resolve the call route before
invoking _reject_unaddressable_clause_op, then use that resolved route for both
State-operation gating and dispatch. Ensure ordinary user-defined get or put
calls are not classified by _STATE_OP_NAMES when they resolve to a user
function, while actual State operations retain the existing rejection behavior;
add a regression test covering the inner clause and same-family enclosing cell
case.
Owner
Author
There was a problem hiding this comment.
@coderabbitai Filed as #1284, and it is worse than the gate misclassification: an ordinary private fn get(@Nat -> @Nat) called in a clause body is check-green, gets a spurious [E602] skip under same-family nesting, and under different-family nesting lowers to call $vera.state_get_Int, producing a module that fails WASM validation. Route-before-classify alone would convert the loud skip into the broken module, so the fix has to reconcile three sites that currently disagree: the checker resolves user-function-first, codegen/functions.py:359 guards on _fn_sigs, and calls_handlers.py:1578 overwrites unconditionally with a comment stating that as deliberate.
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
set -euo pipefail
printf '%s\n' '--- calls.py relevant dispatch ---'
sed -n '420,475p' vera/wasm/calls.py
printf '%s\n' '--- codegen/functions.py around reported guard ---'
sed -n '330,385p' vera/codegen/functions.py
printf '%s\n' '--- calls_handlers.py around reported overwrite and gate ---'
sed -n '1545,1605p' vera/wasm/calls_handlers.py
rg -n -A70 -B10 --type py 'def _reject_unaddressable_clause_op' vera/wasm/calls_handlers.py
printf '%s\n' '--- checker bare-call precedence ---'
rg -n -A85 -B12 --type py 'def _check_call_with_args|def _check_fn_call' vera/checker/calls.py
printf '%s\n' '--- relevant existing regression tests ---'
rg -n -C5 --type py 'shadow.*(get|put)|fn (get|put)\b|same-family|unaddressable|E602' \
tests/test_nested_handler_clause_ops.py \
tests/test_nat_narrowing_return_differential.py \
tests/test_mono_effect_op_naming_1207.py || trueLength of output: 47157
@aallan, confirmed. The original fix proposal was incomplete.
The checker resolves a user function before an effect operation. codegen/functions.py preserves this rule for declared State rows. _translate_handle_state() breaks this rule by overwriting get and put in _effect_ops. _reject_unaddressable_clause_op() then independently classifies every get or put as a State operation.
The fix for #1284 must use one function-first route decision in all three locations:
- Handler registration must not replace a user-function route.
- The E602 gate must run only for a call resolved to a State intrinsic.
- Call emission must use that same resolved route.
A regression must cover both same-family nesting and different-family nesting. It must assert that private fn get(@nat->@nat) emits a normal function call, has no E602 diagnostic, and produces valid WASM.
Thanks for the additional diagnosis. I used the existing route-precedence behavior and the handler overwrite site to validate it.
🧬 Code Graph Analysis Results
vera/wasm/calls.py
- Lines 31–190:
_translate_call— Dispatches calls, prioritizing user-defined functions by checkingcall.name not in self._known_fnsbefore built-in intrinsic handling. It then rejects unaddressable clause operations, routes state clause operations, resolves effect operations, rewrites generic targets, validates registered call targets, and emits regular WASM calls.
vera/ast.py
- Lines 430–433:
ast.FnCall— Defines an unqualified function call withnameand positionalargs. - Lines 450–454:
ast.QualifiedCall— Defines a qualified call withqualifier,name, and positionalargs.
vera/skip.py
- Lines 149–175:
CodegenSkip— Exception raised when translation cannot support an AST node; carries the node and reason and is converted at compilation boundaries into an[E602]diagnostic.
✏️ Learnings added
Learnt from: aallan
Repo: aallan/vera PR: 1283
File: vera/wasm/calls.py:435-441
Timestamp: 2026-08-12T19:15:05.094Z
Learning: In `aallan/vera`, bare calls resolve user-defined functions before effect operations in `vera/checker/calls.py`. `vera/codegen/functions.py` preserves this precedence for declared State effect rows by not registering `get` or `put` when `self._fn_sigs` already contains the name. `vera/wasm/calls_handlers.py` must preserve the same function-first precedence when installing handler-local State operation routes; otherwise a private user `get` or `put` in a nested State clause is misrouted to a State import. The E602 unaddressable-cell gate must apply only after a call has resolved to a State intrinsic.
Note: Learnings are effective only in the context of similar code segments. To apply general coding guidelines, please configure review instructions. You can manage existing learnings in the app.
🧠 Learnings used
Learnt from: aallan
Repo: aallan/vera PR: 1232
File: vera/wasm/calls_handlers.py:1717-1735
Timestamp: 2026-08-07T16:30:44.012Z
Learning: In `vera/wasm/calls_handlers.py`, `mangle_type_name()` is not idempotent. `_state_import_family()` returns an already-mangled State family suffix, while `StateClauseEntry.family` and `_pushed_cell_families` store canonical unmangled family names. In `_reject_unaddressable_clause_op()`, compare both branches in one representation: mangle canonical family names once, but do not re-mangle an import suffix.
Learnt from: aallan
Repo: aallan/vera PR: 1232
File: KNOWN_ISSUES.md:30-30
Timestamp: 2026-08-07T16:23:47.144Z
Learning: In `tests/test_nested_handler_clause_ops.py`, the four-level `Int`/`Nat`/`Int`/`Nat` same-family nested State handler regression case must include a bare `put` in the level-4 clause. Without that operation, the compiler does not inline the level-3 clause and the at-a-distance unaddressable-cell `E602` path is not exercised.
You are interacting with an AI system.
Comment on lines
+203
to
+215
| # #1276 (F4): the FIRST arm that yields a type, not arm 0. An arm | ||
| # whose every path throws contributes no WAT type, and reading only | ||
| # arm 0 answered `None` for the whole match — so an enclosing | ||
| # `handle` block was emitted result-less while the completing arms | ||
| # left a value in it (`values remaining on stack at end of block`, | ||
| # from check-green source). Arms that DO complete must agree on | ||
| # their type (the checker enforces that), so the first answer is the | ||
| # answer. | ||
| for arm in expr.arms: | ||
| arm_wt = self._infer_expr_wasm_type(arm.body) | ||
| if arm_wt is not None: | ||
| return arm_wt | ||
| return None |
There was a problem hiding this comment.
🎯 Functional Correctness | 🟠 Major | ⚡ Quick win
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# Description: Check whether the Vera-type deciders received the `#1276` divergent-branch treatment.
set -euo pipefail
# The MatchExpr / IfExpr arms of _infer_vera_type in the WASM inference mixin.
ast-grep run --pattern $'def _infer_vera_type($$$) {
$$$
}' --lang python vera/wasm/inference.py || true
rg -n -C 6 '_infer_vera_type' vera/wasm/inference.py
# Any test pinning a Vera-type answer for an all-throwing arm / then-branch.
rg -n -C 5 '1276' tests/ | rg -n -i 'vera_type|infer_vera|structural|interpolat' || \
echo "no `#1276` test touches the Vera-type deciders"Repository: aallan/vera
Length of output: 10499
🏁 Script executed:
#!/bin/bash
set -euo pipefail
printf '%s\n' '--- inference implementation ---'
sed -n '180,250p;930,1075p' vera/wasm/inference.py
printf '%s\n' '--- consumers of the two inference methods ---'
rg -n -C 4 '_infer_(expr_wasm_type|block_result_type|vera_type)\(' vera/wasm --glob '*.py'
printf '%s\n' '--- relevant AST definitions ---'
rg -n -C 5 'class (IfExpr|MatchExpr|Block|HandleExpr)|then_branch|arms:' vera/ast.py
printf '%s\n' '--- tests and specification references ---'
rg -n -i -C 4 '`#1276`|throw.*match|match.*throw|structural|interpolat|container element' tests spec vera | head -400Repository: aallan/vera
Length of output: 50367
🏁 Script executed:
#!/bin/bash
set -euo pipefail
printf '%s\n' '--- equality dispatch ---'
sed -n '130,220p;1360,1460p' vera/wasm/operators.py
rg -n -C 8 'structural|_struct|_infer_vera_type.*left|_infer_vera_type.*right|_translate.*equal|EQ|NEQ' vera/wasm/operators.py
printf '%s\n' '--- match and handler result lowering ---'
sed -n '590,635p;2250,2325p' vera/wasm/data.py vera/wasm/calls_handlers.py
rg -n -C 8 '_infer_match_result_type|_translate_match|MatchExpr' vera/wasm/data.py vera/wasm/operators.py
printf '%s\n' '--- checker rules for match, if, and throw ---'
rg -n -C 8 'MatchExpr|IfExpr|throw|effect.*result|Never|unreachable' vera/checker.py vera --glob '*.py' | head -500Repository: aallan/vera
Length of output: 50367
🏁 Script executed:
#!/bin/bash
set -euo pipefail
printf '%s\n' '--- equality dispatch ---'
sed -n '130,220p;1360,1460p' vera/wasm/operators.py
rg -n -C 8 'structural|_struct|_infer_vera_type.*left|_infer_vera_type.*right|_translate.*equal|EQ|NEQ' vera/wasm/operators.py
printf '%s\n' '--- match and handler result lowering ---'
sed -n '590,635p' vera/wasm/data.py
sed -n '2250,2325p' vera/wasm/calls_handlers.py
rg -n -C 8 '_infer_match_result_type|_translate_match|MatchExpr' vera/wasm/data.py vera/wasm/operators.py
printf '%s\n' '--- checker rules for match, if, and throw ---'
rg -n -C 8 'MatchExpr|IfExpr|throw|effect.*result|Never|unreachable' vera/checker.py vera --glob '*.py' | head -500Repository: aallan/vera
Length of output: 50367
🏁 Script executed:
#!/bin/bash
set -euo pipefail
python3 - <<'PY'
import ast
from pathlib import Path
path = Path("vera/wasm/inference.py")
tree = ast.parse(path.read_text(encoding="utf-8"))
def find_method(name: str) -> ast.FunctionDef:
for node in ast.walk(tree):
if isinstance(node, (ast.FunctionDef, ast.AsyncFunctionDef)) and node.name == name:
return node
raise SystemExit(f"missing method: {name}")
for name in ("_infer_expr_wasm_type", "_infer_vera_type"):
method = find_method(name)
print(f"{name}: lines {method.lineno}-{method.end_lineno}")
for node in ast.walk(method):
if isinstance(node, ast.If) and node.test.__class__ is ast.Call:
continue
if isinstance(node, ast.If):
test = ast.unparse(node.test)
if "MatchExpr" in test or "IfExpr" in test:
print(f" branch line {node.lineno}: {test}")
print(" ", [ast.unparse(stmt) for stmt in node.body])
print(" else:", [ast.unparse(stmt) for stmt in node.orelse])
PY
printf '%s\n' '--- direct structural-equality fallback ---'
sed -n '186,250p' vera/wasm/operators.py
printf '%s\n' '--- checker MatchExpr locations ---'
rg -n -C 6 'isinstance\(.*MatchExpr|MatchExpr' vera/checker.py vera/checker --glob '*.py' | head -250
printf '%s\n' '--- `#1276` tests ---'
rg -n -i -C 3 '`#1276`|1276|always.throw|always.*throw|throw.*match|match.*throw' tests --glob '*.py' --glob '*.vera' | head -250 || trueRepository: aallan/vera
Length of output: 11129
🏁 Script executed:
#!/bin/bash
set -euo pipefail
python3 - <<'PY'
import ast
from pathlib import Path
path = Path("vera/wasm/inference.py")
tree = ast.parse(path.read_text(encoding="utf-8"))
def find_method(name: str) -> ast.FunctionDef:
for node in ast.walk(tree):
if isinstance(node, (ast.FunctionDef, ast.AsyncFunctionDef)) and node.name == name:
return node
raise SystemExit(f"missing method: {name}")
for name in ("_infer_expr_wasm_type", "_infer_vera_type"):
method = find_method(name)
print(f"{name}: lines {method.lineno}-{method.end_lineno}")
for node in ast.walk(method):
if isinstance(node, ast.If):
test = ast.unparse(node.test)
if "MatchExpr" in test or "IfExpr" in test:
print(f" branch line {node.lineno}: {test}")
print(" ", [ast.unparse(stmt) for stmt in node.body])
print(" else:", [ast.unparse(stmt) for stmt in node.orelse])
PY
printf '%s\n' '--- direct structural-equality fallback ---'
sed -n '186,250p' vera/wasm/operators.py
printf '%s\n' '--- checker MatchExpr locations ---'
rg -n -C 6 'isinstance\(.*MatchExpr|MatchExpr' vera/checker.py vera/checker --glob '*.py' | head -250
printf '%s\n' '--- `#1276` tests ---'
rg -n -i -C 3 '`#1276`|1276|always.throw|always.*throw|throw.*match|match.*throw' tests --glob '*.py' --glob '*.vera' | head -250 || trueRepository: aallan/vera
Length of output: 11907
🏁 Script executed:
#!/bin/bash
set -euo pipefail
printf '%s\n' '--- checker branch-type joins ---'
sed -n '1,165p' vera/checker/control.py
printf '%s\n' '--- effect-operation typing ---'
rg -n -C 8 'throw|_effect_ops|effect.*op|EffectOp' vera/checker --glob '*.py' | head -350
printf '%s\n' '--- focused regression-test search ---'
rg -n -i -C 3 '`#1276`|1276|always[ -_]throw|throw.*match|match.*throw|structural.*equal|ADT.*equal' tests --glob '*.py' --glob '*.vera' | head -300 || trueRepository: aallan/vera
Length of output: 50367
Keep Vera-type inference aligned with the divergent-branch rule.
_infer_vera_type still inspects only the first match arm and does not fall back to the else branch. The checker permits these shapes because NEVER branches are skipped during type joins. A check-green ADT-valued match or if can therefore have WASM type i32 but no Vera type. Structural == then falls through to i32.eq pointer comparison, while show and array-element inference can be rejected.
Iterate over match arms and apply the same fallback to else. Add regression tests.
Also applies to: 233-240
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@vera/wasm/inference.py` around lines 203 - 215, Update _infer_vera_type to
inspect each match arm in order, skipping arms whose inferred type is absent,
then fall back to the else branch when no arm yields a type, matching the
divergent-branch rule used by _infer_expr_wasm_type. Preserve the checker’s
behavior for NEVER-only branches and add regression tests covering ADT-valued
match/if expressions, structural equality, show, and array-element inference.
Source: Learnings
Owner
Author
There was a problem hiding this comment.
@coderabbitai Filed as #1286. Confirmed by inspection: _infer_vera_type reads then_branch only at line 1051 and arms[0] only at line 1063, while its sibling _infer_expr_wasm_type took the #1276 divergent-branch treatment at lines 202-215 and 232-240. I could not produce a clean check-green reproduction within this round, so applying the change blind would leave it unproven either way.
There was a problem hiding this comment.
@aallan, agreed. The inspection confirms that _infer_vera_type does not match the divergent-branch handling in _infer_expr_wasm_type.
#1286 is the correct follow-up. A clean check-green reproduction should define the required regression before changing the inference rule. I will keep this finding open until that change and its test coverage are available.
You are interacting with an AI system.
Comment on lines
1781
to
1789
| def _translate_new_expr(self, expr: ast.NewExpr) -> list[str] | None: | ||
| """Translate new(State<T>) → call state_get to read current value.""" | ||
| type_name = self._extract_state_type_name(expr.effect_ref) | ||
| if type_name is None: | ||
| raise CodegenInvariantError( # pragma: no cover | ||
| "new(State<T>) effect ref has no extractable type name", expr) | ||
| state_type_arg(expr.effect_ref) # shape validation; raises otherwise | ||
| # Look up the state getter import | ||
| if "get" not in self._effect_ops: | ||
| raise CodegenInvariantError( # pragma: no cover | ||
| "new(State<T>) has no 'get' effect op registered", expr) | ||
| call_target, _is_void = self._effect_ops["get"] | ||
| return [f"call {call_target}"] |
There was a problem hiding this comment.
🎯 Functional Correctness | 🟠 Major | 🏗️ Heavy lift
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# Is the getter registry family-keyed anywhere, and how is `_effect_ops` populated?
rg -nP --type=py -C10 '_effect_ops\b' vera/wasm/ vera/codegen/
rg -nP --type=py -C10 '_state_types\b' vera/wasm/ vera/codegen/
# Confirm the family derivation used by the old/new pair and the snapshot map.
rg -nP --type=py -C10 'def _state_effect_family|def _collect_old_types|def get_old_state_local'Repository: aallan/vera
Length of output: 50367
🏁 Script executed:
#!/bin/bash
set -e
printf '%s\n' '--- operators.py: old/new translation and family helper ---'
sed -n '1735,1792p' vera/wasm/operators.py
rg -n -C8 'def _state_effect_family|_state_effect_family\(' vera/wasm vera
printf '%s\n' '--- state handler injection and cell registries ---'
sed -n '1510,1605p' vera/wasm/calls_handlers.py
printf '%s\n' '--- state-cell registry injection sites ---'
rg -n -C6 'effect_ops=.*state|get_import|state_get_|_effect_op_cells' vera/codegen vera/wasm/functions.py vera/wasm/calls_handlers.py
printf '%s\n' '--- NewExpr tests and nested State tests ---'
rg -n -C5 'new\(State|NewExpr|nested.*State|State<Int>.*State<Bool>|State<Bool>.*State<Int>' tests veraRepository: aallan/vera
Length of output: 41361
🏁 Script executed:
#!/bin/bash
set -e
printf '%s\n' '--- declared-effect registry construction ---'
sed -n '300,390p' vera/codegen/functions.py
printf '%s\n' '--- old-state collection and postcondition translation ---'
sed -n '760,840p' vera/codegen/contracts.py
rg -n -C8 'NewExpr|new\(State|new\\(' tests vera spec
printf '%s\n' '--- handler-expression and contract call graph ---'
rg -n -C8 '_translate_new_expr|translate.*contract|postcondition|postcondition' vera/wasm vera/codegenRepository: aallan/vera
Length of output: 9344
🏁 Script executed:
#!/bin/bash
set -e
printf '%s\n' '--- NewExpr references ---'
rg -n -F -C5 'NewExpr' tests vera spec || true
rg -n -F -C5 'new(State' tests vera spec || true
printf '%s\n' '--- contract translation call sites ---'
rg -n -F -C10 '_snapshot_old_state' vera
rg -n -F -C10 'translate_contract' vera
rg -n -F -C10 'decl.contracts' vera/wasm vera/codegen
printf '%s\n' '--- effect-row and handler State combinations in tests/spec ---'
rg -n -F -C5 'State<Int>, State<Bool>' tests vera spec || true
rg -n -F -C5 'State<Bool>, State<Int>' tests vera spec || true
rg -n -F -C5 'old(State' tests vera spec || trueRepository: aallan/vera
Length of output: 50369
🏁 Script executed:
#!/bin/bash
set -e
python3 - <<'PY'
from pathlib import Path
import ast
operators = Path("vera/wasm/operators.py").read_text(encoding="utf-8")
functions = Path("vera/codegen/functions.py").read_text(encoding="utf-8")
tree = ast.parse(operators)
new_method = next(
node for node in ast.walk(tree)
if isinstance(node, ast.FunctionDef)
and node.name == "_translate_new_expr"
)
new_source = ast.get_source_segment(operators, new_method)
assert new_source is not None
assert 'self._effect_ops["get"]' in new_source
assert "_state_effect_family" not in new_source
tree = ast.parse(functions)
effect_builder = next(
node for node in ast.walk(tree)
if isinstance(node, ast.FunctionDef)
and node.name == "_compile_fn"
)
builder_source = ast.get_source_segment(functions, effect_builder)
assert builder_source is not None
assert 'effect_ops["get"]' in builder_source
assert '"get" not in effect_ops' in builder_source
print("new(State<T>) uses the name-keyed effect_ops['get'] entry.")
print("Declared State effects populate one get entry; later State entries do not replace it.")
PYRepository: aallan/vera
Length of output: 294
Resolve new(State<T>) by its State family.
When an effect row contains multiple State types, _translate_new_expr uses the single name-keyed _effect_ops["get"] entry. Thus new(State<Bool>) can emit the getter for the first declared State type, producing the wrong value or WASM type. Derive the family with _state_effect_family and select the matching getter.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@vera/wasm/operators.py` around lines 1781 - 1789, Update _translate_new_expr
to derive the State family using _state_effect_family(expr.effect_ref), then
select the getter associated with that family instead of the shared
_effect_ops["get"] entry. Preserve the existing state_type_arg validation,
missing-getter invariant error, and call-target emission while ensuring each
State type uses its matching getter.
Source: Learnings
Owner
Author
There was a problem hiding this comment.
@coderabbitai Filed as #1285, reproduced end to end: with effects(<State<Int>, State<Bool>>) and ensures(new(State<Bool>) == true), the program checks green and $bump emits call $vera.state_get_Int returning i64 into an i32.eq, so vera run fails with type mismatch: expected i32, found i64. _translate_old_expr is already family-keyed through _state_effect_family; new needs a family-to-getter registry, which is a wider codegen change than a release round should carry.
There was a problem hiding this comment.
@aallan, thanks for the end-to-end reproduction and for filing #1285.
The failure confirms the finding. _translate_new_expr selects the name-keyed _effect_ops["get"] entry. With multiple State families, that entry can select State<Int> for new(State<Bool>). The generated i64 result then reaches an i32.eq.
A family-to-getter registry is required to correct this path. Deferring that wider code generation change to #1285 is appropriate for this release PR.
✏️ Learnings added
Learnt from: aallan
Repo: aallan/vera PR: 1283
File: vera/wasm/operators.py:1781-1789
Timestamp: 2026-08-12T19:14:39.146Z
Learning: In `vera/wasm/operators.py`, `_translate_new_expr` currently uses the name-keyed `_effect_ops["get"]` registry entry. When an effect row contains multiple `State<T>` families, such as `State<Int>` and `State<Bool>`, `new(State<Bool>)` can call the `State<Int>` getter and generate an i64/i32 WebAssembly type mismatch. `old(State<T>)` already derives the family through `_state_effect_family`; a correct `new(State<T>)` implementation requires a State-family-to-getter registry. This defect is tracked in GitHub issue `#1285`.
Note: Learnings are effective only in the context of similar code segments. To apply general coding guidelines, please configure review instructions. You can manage existing learnings in the app.
You are interacting with an AI system.
|
Caution CodeRabbit couldn't update its existing comment. The review summary may be out of date. Error details |
test_a_failed_write_leaves_no_temp_file snapshotted gettempdir() for *.vera either side of the call it measures. CI runs pytest -n auto, so that directory is shared by every xdist worker, each writing its own tmp*.vera: a sibling worker's fixture, alive for the microseconds between the snapshot and the assertion, counted as litter this test had left. It did -- AssertionError over a C:\...\tmp*.vera on worker gw1 in the v0.1.10 release push, an hour after the identical tree passed, and reproduced here at 210/300 with a second PROCESS writing into that directory. A thread cannot stand in for the worker: it reaches this process's patched globals, which no worker can, and produced failures of its own that the fixed test is right to ignore. The evidence is now the ONE path the call created, captured from NamedTemporaryFile the way the sibling ordering test captures handles. No shared directory is read at all, so the race is removed rather than relocated to a private TMPDIR -- which would still assert over a directory, and would additionally have to reset tempfile's cached tempdir for the env override to take effect. Same instrument: 0/300. A len(created) == 1 guard keeps the check from passing over an empty list should the builder stop creating its file that way. Both halves are mutation-validated: the pre-#1282 leaking cleanup turns it red naming the stranded path, and switching the builder to mkstemp turns it red on the guard. The siblings from that PR were audited and need no isolation. test_the_handle_is_closed_before_every_unlink asserts over in-process traces (its own handle list and unlink log) that a separate worker cannot reach -- 0/60 under the same adversary -- and test_neither_builder_leaves_a_file_behind names its own unique path rather than reading the directory it sits in. TESTING.md records the rule under Test Fixture Conventions, where CI's parallelism makes it general: evidence about temp files names them. Also, from the release-surface audit: README's status line and HISTORY's "By the numbers" total both said 206 releases against 207 tags -- accurate at v0.1.5, two behind since v0.1.8, and agreeing with each other the whole way down, which is why the cross-check between them never saw it. Both now say 208 (207 tags plus the v0.1.10 tag release.yml creates after the merge), and check_doc_counts.py reads git tag as the oracle: exact equality once the version is tagged, the single pending tag of a release being cut as the only slack, and a printed skip where a checkout has no tags, since that is absence of evidence rather than zero releases. Co-Authored-By: Claude <noreply@anthropic.invalid>
There was a problem hiding this comment.
Actionable comments posted: 24
♻️ Duplicate comments (2)
tests/test_phantom_generic_instances_1271.py (1)
88-100: 📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick winPin
_CONCRETE_REQUIREDagainst the imported label set.
_ALL_CASEStakes its labels from_CASES, which is imported fromtests/test_generic_under_generic_callees_1223.py. Line 346 then indexes_CONCRETE_REQUIRED[label].A label added upstream raises
KeyError, which is loud. A label removed upstream is silent: the corresponding entry in_CONCRETE_REQUIREDbecomes dead, and the "the filter removed the REAL instantiation too" assertion for that shape disappears with no test turning red. That is the exact vacuity class this file exists to prevent, as the module docstring states at lines 15-17. State the correspondence once.♻️ Proposed sync guard
_CONCRETE_REQUIRED = { "user_generic": "pick$Bool", "prelude_generic": "option_unwrap_or$Bool", "depth_two": "pick$Bool", "nongeneric_parent_control": "pick$Bool", "mutual_recursion": "leaf$Bool", } +assert set(_CONCRETE_REQUIRED) == {label for label, _ in _ALL_CASES}, ( + "the required-concrete-clone map drifted from the case set: " + f"{sorted(set(_CONCRETE_REQUIRED) ^ {label for label, _ in _ALL_CASES})}" +)🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@tests/test_phantom_generic_instances_1271.py` around lines 88 - 100, Keep _CONCRETE_REQUIRED synchronized with the labels in _ALL_CASES by adding an assertion that both label sets are exactly equal. Place the guard near the _ALL_CASES and _CONCRETE_REQUIRED definitions so upstream additions or removals fail immediately, while preserving the existing per-label lookup behavior.tests/test_nested_handler_clause_ops.py (1)
182-188: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winGuard the qualified fixture derivation, as the same-family twin does.
_QUALIFIED_IN_CLAUSEderives from_PUT_IN_PUT_CLAUSEbystr.replace. If the bare clause body spelling changes,replacematches nothing and_QUALIFIED_IN_CLAUSEbecomes byte-identical to_PUT_IN_PUT_CLAUSE. Thequalified_in_clauserow at line 311 then duplicatesput_in_put_clause, keeps the same expected value 301000 and the samepre_fix100000111, and stays green whileState.putis no longer exercised at all.
test_every_case_distinguishes_the_two_semanticscannot catch this, because it comparesexpectedagainstpre_fixwithin a row, and both values are unchanged.Lines 635-638 already add exactly this guard for
_SAME_FAMILY_QUALIFIED. Apply the same guard here.🛡️ Proposed guard, mirroring lines 635-638
_QUALIFIED_IN_CLAUSE = _PUT_IN_PUT_CLAUSE.replace( "put(`@Nat`) -> { put(1000); resume(()) }", "put(`@Nat`) -> { State.put(1000); resume(()) }", ) +assert _QUALIFIED_IN_CLAUSE != _PUT_IN_PUT_CLAUSE, ( + "the qualified-spelling fixture no longer derives from the bare one — " + "the bare clause body's spelling changed" +)As per path instructions, tests that do not assert anything meaningful must be flagged; a fixture that collapses onto its own control asserts nothing about the qualified spelling.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@tests/test_nested_handler_clause_ops.py` around lines 182 - 188, Guard the derived _QUALIFIED_IN_CLAUSE fixture immediately after its str.replace call, mirroring the existing guard for _SAME_FAMILY_QUALIFIED: assert that the replacement changed the source and that the qualified fixture differs from _PUT_IN_PUT_CLAUSE. This must fail loudly if the bare clause spelling changes, ensuring the qualified_in_clause case continues exercising State.put rather than silently duplicating the bare case.Source: Path instructions
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In @.pre-commit-config.yaml:
- Around line 111-117: Update the doc-block gates count in the comment above the
pre-commit hooks from six to seven, leaving the correctly configured
debruijn-examples hook and its triggers unchanged.
In `@SKILL.md`:
- Line 152: Update the W002 description to state that effects fall outside the
commutative whitelist `{Http, Async}`, rather than naming only `Http`; preserve
the explanation that such effects cause sequential evaluation at the async()
site.
In `@spec/03-slot-references.md`:
- Line 383: Correct the argument-resolution rule in the slot-name documentation
by adding the missing verb so it explicitly states that two spellings of the
same argument name share one namespace. Preserve the surrounding explanation of
head opacity and alias resolution.
In `@spec/07-effects.md`:
- Line 208: In spec/07-effects.md at lines 208-208, separate the
compilability-gate rule from cell naming: state which resolutions are refused
before cell creation, and separately state which unresolved resolutions reach
cell naming and use alias-opaque spelling. In DE_BRUIJN.md at lines 486-486,
update the paragraph to match the corrected §7.5.1 wording while preserving its
existing cross-reference; both locations must no longer claim that the same
expressions are simultaneously refused and assigned cells.
In `@tests/conformance/manifest.json`:
- Around line 1708-1730: Normalize the feature key in the manifest entries
ch08_reserved_vera_prefix_reference and the preceding reserved-name entry from
"type_aliases" to the established singular "type_alias", leaving all other
feature metadata unchanged.
In `@tests/module_fixture_helpers.py`:
- Around line 52-107: Update both resolved_module and fake_resolved_module to
populate ResolvedModule.direct, setting it to whether the module’s final path
component (stem) equals "mid". Preserve the existing parsing, paths, and source
behavior while ensuring main → mid → deep fixtures identify only mid as direct.
In `@tests/test_byte_literal_joins_1212.py`:
- Around line 508-516: Guard every fixture mutation in the affected tests,
including test_the_other_branch_is_reachable_and_also_a_byte and the additional
replacement sites, by asserting that each expected target string is present
before or as part of applying .replace. Follow the existing assertion pattern
from the sibling suite so a missing target cannot silently leave the fixture
unchanged, while preserving the current replacement-based test behavior.
In `@tests/test_checker_modules.py`:
- Around line 22-28: Rename the misleading _resolved_module alias in
tests/test_checker_modules.py to identify the fake builder, or remove it
entirely; update the call sites around the affected module-diagnostic tests to
invoke fake_resolved_module(...) directly while preserving their existing
behavior.
In `@tests/test_checker_types.py`:
- Around line 2128-2147: In test_two_distinct_literals_keep_two_errors, replace
the set-comprehension comparison with direct assertions that each E149 error
description contains its corresponding literal, preserving the existing
len(e149) == 2 check and producing failure output tied to the actual
descriptions.
In `@tests/test_closure_lift_boundaries_1234_1235_1245.py`:
- Around line 461-473: Remove the redundant elapsed-time assertion after the
t.is_alive() termination check in the worker wait logic, preserving the existing
timeout failure and error propagation behavior. Also remove the time import if
it is unused elsewhere in the test module.
In `@tests/test_codegen_effects.py`:
- Around line 2645-2646: Update the WAT `$probe` function regex in the test
assertion to use an explicit negative lookahead after `probe`, ensuring the
symbol is not immediately followed by a valid identifier character such as `$`.
Preserve the existing function-body matching and missing-function assertion
while preventing matches against monomorphised names like `$probe$Int`.
In `@tests/test_codegen_monomorphize.py`:
- Around line 2529-2532: Update the subprocess.run call in the test around the
prog execution to include the established 120-second timeout, matching the
bounded subprocess invocations in tests/test_effect_op_determinism.py while
preserving check=True and the existing environment settings.
In `@tests/test_codegen_nat_guards.py`:
- Line 1392: Update the negative-control assertions in the parameterized test
near the shown `i64.lt_s` check and its unparameterized twin to reject both
signed and unsigned 64-bit less-than comparisons, using the repository’s
`i64.lt_[su]` boundary pattern. Keep the existing `body` validation and do not
add a blanket `unreachable` assertion, since the refinement guard legitimately
emits a trap edge.
In `@tests/test_exn_throw_payload_1268.py`:
- Around line 103-109: Guard the fixture mutation in the test around _thrower
and the src.replace call by requiring exactly one occurrence of “boom((0 - 5))”
before replacing it, following the single-occurrence replacement pattern used in
test_alias_application_refinement_base_1237.py. Ensure the test fails if the
generated spelling changes or the target is absent, rather than verifying the
unintended original program.
In `@tests/test_prelude.py`:
- Around line 321-327: Add a focused non-vacuity assertion in
tests/test_prelude.py for _RESERVED_TYPE_PREFIX_RE, verifying it matches a
representative reserved alias and does not match a representative ordinary
identifier. Keep this guard near the existing reserved-namespace assertions so
future broadening of the regex cannot make the negative checks pass vacuously.
In `@tests/test_slot_naming_differential.py`:
- Around line 617-647: Move the first comment paragraph describing former
PRELUDE alias spellings and `#1221` from above effect_row_corners_in_arg to
immediately before prelude_alias_in_arg. Keep the effect-row explanation
directly above effect_row_corners_in_arg, preserving both entries and their
existing content.
- Around line 213-263: Add a separate had_te guard recording whether
_type_expr_to_slot_name exists directly in TypeChecker.__dict__, while
preserving the inherited original for patching. In the context manager cleanup,
restore _type_expr_to_slot_name only when had_te is true; otherwise delete the
temporary class attribute, mirroring the existing _slot_type_name handling.
In `@tests/test_slot_naming.py`:
- Around line 649-657: Update the test setup around parse_to_ast, TypeChecker,
and checker.check_program so the checker receives the exact same prefixed
program text used for parsing, including the Box alias declaration. Assert that
the check completes cleanly, matching the neighboring deep-nesting tests, before
comparing the rendered slot name with the checker result.
In `@tests/test_verifier_calls_modules.py`:
- Around line 1436-1454: Update the body-line anchor in the regression test
around _e532_demotions so it is derived from the independently asserted E522
ensures obligation, not from result.obligations filtered by caller. Capture the
clause obligation’s line and assert the demotion line differs from it, while
retaining the existing single-demotion and tier3 clause assertions.
In `@tests/test_verifier_refinements.py`:
- Around line 2315-2361: Update test_no_demotion_site_hardcodes_a_solver_reason
so positional reason arguments are classified instead of skipped: inspect the
recorder call’s positional arguments according to each recorder’s signature, or
enforce that every _RECORDERS method declares reason keyword-only and add the
corresponding structural assertion. Preserve the existing fixed-text checks and
ensure any unclassifiable or solver-related positional reason is reported as an
offender.
In `@vera/obligations/core.py`:
- Around line 156-166: The content_key() rationale in
vera/obligations/core.py#L156-L166 must document vera.lsp.extensions.proof_delta
as a consumer and state that both obligation streams must derive file
identically. In vera/lsp/extensions.py#L125-L131, verify that
vera.lsp.features.analyze and speculative_edit both use the same uri_to_path
conversion, aligning the conversion if they differ.
In `@vera/obligations/session.py`:
- Around line 179-185: Add a table-driven test covering the resolver guard in
the didChange handling around ModuleResolver: absolute and relative on-disk
files must resolve imports, while absent relative, untitled, virtual-filesystem,
and degenerate file-scheme paths must skip resolution. For skipped cases, assert
resolved_modules is empty and resolver_errors remains empty so diagnostics come
only from E230; use the existing test fixtures and diagnostic symbols.
In `@vera/prelude.py`:
- Around line 796-803: Update the docstring around the closure-parameter type
aliases to remove the claim that aliases are “never skipped.” State instead that
each alias is injected exactly when its corresponding combinator body is
injected, while preserving the explanation that the reserved Vera namespace
prevents user alias shadowing.
In `@vera/wasm/calls_handlers.py`:
- Around line 2407-2431: Update _handle_exn_always_throws to return False unless
expr.effect identifies the Exn effect before evaluating the body or clauses.
This guard must reject non-Exn HandleExpr instances such as State handlers,
preserving the docstring’s conservative behavior and preventing them from
authorizing unreachable.
---
Duplicate comments:
In `@tests/test_nested_handler_clause_ops.py`:
- Around line 182-188: Guard the derived _QUALIFIED_IN_CLAUSE fixture
immediately after its str.replace call, mirroring the existing guard for
_SAME_FAMILY_QUALIFIED: assert that the replacement changed the source and that
the qualified fixture differs from _PUT_IN_PUT_CLAUSE. This must fail loudly if
the bare clause spelling changes, ensuring the qualified_in_clause case
continues exercising State.put rather than silently duplicating the bare case.
In `@tests/test_phantom_generic_instances_1271.py`:
- Around line 88-100: Keep _CONCRETE_REQUIRED synchronized with the labels in
_ALL_CASES by adding an assertion that both label sets are exactly equal. Place
the guard near the _ALL_CASES and _CONCRETE_REQUIRED definitions so upstream
additions or removals fail immediately, while preserving the existing per-label
lookup behavior.
🪄 Autofix
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: c986bf56-e5b5-4eb8-b8e7-22e85a883b53
⛔ Files ignored due to path filters (159)
assets/diagrams/architecture.svgis excluded by!**/*.svgdocs/SKILL.mdis excluded by!docs/**docs/index.htmlis excluded by!docs/**docs/index.mdis excluded by!docs/**docs/llms-full.txtis excluded by!docs/**docs/llms.txtis excluded by!docs/**examples/array_utilities.verais excluded by!**/*.veraexamples/closures.verais excluded by!**/*.veratests/conformance/ch01_byte_literal_join_width.verais excluded by!**/*.veratests/conformance/ch02_alias_cycle_rejected.verais excluded by!**/*.veratests/conformance/ch02_refinement_base_param_alias.verais excluded by!**/*.veratests/conformance/ch03_slot_alias_type_argument.verais excluded by!**/*.veratests/conformance/ch07_clause_body_op_enclosing.verais excluded by!**/*.veratests/conformance/ch07_effect_op_source_order.verais excluded by!**/*.veratests/conformance/ch07_exn_composite.verais excluded by!**/*.veratests/conformance/ch07_exn_param_alias.verais excluded by!**/*.veratests/conformance/ch07_exn_scalar_alias.verais excluded by!**/*.veratests/conformance/ch07_exn_string_alias.verais excluded by!**/*.veratests/conformance/ch07_handler_registration_positions.verais excluded by!**/*.veratests/conformance/ch07_nested_handlers.verais excluded by!**/*.veratests/conformance/ch07_state_alias_chain.verais excluded by!**/*.veratests/conformance/ch07_state_alias_op_result_positions.verais excluded by!**/*.veratests/conformance/ch07_state_byte_join_writes.verais excluded by!**/*.veratests/conformance/ch07_state_clause_alias_slots.verais excluded by!**/*.veratests/conformance/ch07_state_clause_transform.verais excluded by!**/*.veratests/conformance/ch07_state_composite.verais excluded by!**/*.veratests/conformance/ch07_state_composite_alias.verais excluded by!**/*.veratests/conformance/ch07_state_composite_alias_cross_spelling.verais excluded by!**/*.veratests/conformance/ch07_state_fn_type_alias_cross_spelling.verais excluded by!**/*.veratests/conformance/ch07_state_handler.verais excluded by!**/*.veratests/conformance/ch07_state_nested_param_alias.verais excluded by!**/*.veratests/conformance/ch07_state_op_array_element.verais excluded by!**/*.veratests/conformance/ch07_state_op_generic_instantiation.verais excluded by!**/*.veratests/conformance/ch07_state_refined_cell_family.verais excluded by!**/*.veratests/conformance/ch07_state_scalar_alias_cross_spelling.verais excluded by!**/*.veratests/conformance/ch07_state_scalar_alias_widths.verais excluded by!**/*.veratests/conformance/ch08_reserved_vera_prefix_ability_rejected.verais excluded by!**/*.veratests/conformance/ch08_reserved_vera_prefix_binder_rejected.verais excluded by!**/*.veratests/conformance/ch08_reserved_vera_prefix_constructor_rejected.verais excluded by!**/*.veratests/conformance/ch08_reserved_vera_prefix_effect_rejected.verais excluded by!**/*.veratests/conformance/ch08_reserved_vera_prefix_reference_rejected.verais excluded by!**/*.veratests/conformance/ch08_state_alias_module_table.verais excluded by!**/*.veratests/conformance/ch08_state_alias_module_table_lib.verais excluded by!**/*.veratests/conformance/ch08_state_alias_per_module.verais excluded by!**/*.veratests/conformance/ch08_state_alias_per_module_lib.verais excluded by!**/*.veratests/conformance/ch09_generic_infer_user_fn_return.verais excluded by!**/*.veratests/conformance/ch09_generic_under_generic_callee.verais excluded by!**/*.veratests/conformance/ch09_generic_under_generic_depth_two.verais excluded by!**/*.veratests/conformance/ch09_generic_under_generic_prelude_callee.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/f1_cross_spelling.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/g1_array.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p11_xmod_alias_collision.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p12_cross_spelling.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p13_exn_cross.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p15_generic_elem.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p15b_append.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p15c_direct.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p17b_state_string_minimal.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p22_param_alias.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p23_alias_of_generic.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p24_exn_generic.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p25_refined_cell.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p2_chain.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p2_family_nested_alias.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p3_scalars.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p3a_self_param_cycle.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p3b_mutual_param_cycle.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p3c_byte_alias.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p3d_bool_float.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p6_main.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p7_exn_scalar.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p7_fn_alias_state_arg.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p7a_array.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p7b_match.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p7c_composite_alias.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p7d_eq.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p8_exn_string.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p8_xmod_alias_family.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p9_composite.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p9_exn_nested_alias.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p9_refined_state_minimal.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p_exnalias.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/p_nested_app.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/statelib.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/x1_exn_string_alias.verais excluded by!**/*.veratests/probes/state_handlers/alias_families/xmod_lib.verais excluded by!**/*.veratests/probes/state_handlers/checker_gates/e128_array.verais excluded by!**/*.veratests/probes/state_handlers/checker_gates/e337_user_effect_exn.verais excluded by!**/*.veratests/probes/state_handlers/clause_scoping/a11_refined_pattern.verais excluded by!**/*.veratests/probes/state_handlers/clause_scoping/p1b_nested_alias_clause_value.verais excluded by!**/*.veratests/probes/state_handlers/clause_scoping/p1d_single_alias_ref.verais excluded by!**/*.veratests/probes/state_handlers/clause_scoping/p4b_alias_arg_pattern.verais excluded by!**/*.veratests/probes/state_handlers/clause_scoping/p4e_fn_param_baseline.verais excluded by!**/*.veratests/probes/state_handlers/dispatch_paths/p9_cross_family.verais excluded by!**/*.veratests/probes/state_handlers/nested_handlers/p11_init_nested.verais excluded by!**/*.veratests/probes/state_handlers/nested_handlers/p13_exn_in_clause.verais excluded by!**/*.veratests/probes/state_handlers/nested_handlers/p17_string_outer.verais excluded by!**/*.veratests/probes/state_handlers/nested_handlers/p17c_option_outer.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/bare_obs.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_arg_if.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_bare33.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_bare_put.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_delegated_put.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_init999.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_init_if.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_let999.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_let_if.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_neg_composite.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_put42.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_put999.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_put_arith.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_put_if.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_refined_alias.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_refined_violating.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_resume300.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_resume9.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_resume_arith.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_resume_if.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_resume_lit.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_roundtrip.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_with77.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/byte_with_lit.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/d1_literals.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/d2_block_tail_resume.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/mut_put.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p1.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p10_alias_nat_state.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p1205_neg.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p19_guard_bareput.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p1_put_no_clause.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p1_put_noclause.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p2.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p20_guard_init.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p21_guard_resume.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p2_put_with_clause.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p3.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p4.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p4_custom_effect_resume.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p4_refined.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p4c_byte_with.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p5_exn.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p5_get_resume_guard.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p6.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p6_init_guard_control.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p7_with_update_control.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p8_refined_state.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p8_resume_guard.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p8b_positive.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p_bytelet.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p_bytewith.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/p_qualput_neg.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/pr_alias.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/pr_alias_min.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/pr_init.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/pr_init_req.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/pr_upd_req.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/pr_update.verais excluded by!**/*.veratests/probes/state_handlers/write_guards/widen_ok.verais excluded by!**/*.verauv.lockis excluded by!**/*.lock,!uv.lock
📒 Files selected for processing (133)
.github/workflows/ci.yml.gitignore.pre-commit-config.yamlAGENTS.mdCHANGELOG.mdCLAUDE.mdCONTRIBUTING.mdDESIGN.mdDE_BRUIJN.mdFAQ.mdHISTORY.mdKNOWN_ISSUES.mdLSP_SERVER.mdREADME.mdROADMAP.mdSKILL.mdTESTING.mdTOOLCHAIN.mdassets/diagrams/README.mdexamples/README.mdpyproject.tomlscripts/check_debruijn_examples.pyscripts/check_doc_counts.pyspec/02-types.mdspec/03-slot-references.mdspec/04-expressions.mdspec/07-effects.mdspec/08-modules.mdtests/codegen_helpers.pytests/conformance/manifest.jsontests/module_fixture_helpers.pytests/naming_helpers.pytests/probes/README.mdtests/probes/state_handlers/README.mdtests/test_adt_membership_scope_1253.pytests/test_alias_application_refinement_base_1237.pytests/test_ast.pytests/test_byte_literal_joins_1212.pytests/test_callee_contract_scope_1220_1225_1226.pytests/test_check_doc_counts.pytests/test_checker_modules.pytests/test_checker_types.pytests/test_cli.pytests/test_clone_body_declaring_module_1241_1243.pytests/test_closure_boundary_widths_1255_1256_1269.pytests/test_closure_lift_boundaries_1234_1235_1245.pytests/test_codegen_collections.pytests/test_codegen_effects.pytests/test_codegen_modules.pytests/test_codegen_monomorphize.pytests/test_codegen_nat_guards.pytests/test_effect_op_determinism.pytests/test_exn_throw_payload_1268.pytests/test_family_naming.pytests/test_generic_under_generic_callees_1223.pytests/test_handle_exn_divergent_result_1276.pytests/test_import_visibility_entry_point_1244.pytests/test_lsp.pytests/test_module_generic_namespace_1274.pytests/test_mono_effect_op_naming_1207.pytests/test_monomorphize_differential.pytests/test_naming_env_provenance_1208.pytests/test_nat_int_widening.pytests/test_nat_narrowing_return_differential.pytests/test_nested_handler_clause_ops.pytests/test_obligations.pytests/test_phantom_generic_instances_1271.pytests/test_prelude.pytests/test_refinement_binder_convergence_1208.pytests/test_slot_naming.pytests/test_slot_naming_blast_radius.pytests/test_slot_naming_differential.pytests/test_state_exn_registration.pytests/test_tester_coverage.pytests/test_verifier_adt_decreases.pytests/test_verifier_calls_modules.pytests/test_verifier_mutation_obligations.pytests/test_verifier_nat_obligations.pytests/test_verifier_refinements.pytests/test_verifier_shadow_audits.pytests/test_walker_defensive_branches_597.pytests/test_wasm_coverage.pyvera/README.mdvera/__init__.pyvera/ast.pyvera/checker/calls.pyvera/checker/control.pyvera/checker/core.pyvera/checker/expressions.pyvera/checker/modules.pyvera/checker/registration.pyvera/checker/resolution.pyvera/cli.pyvera/codegen/api.pyvera/codegen/assembly.pyvera/codegen/closures.pyvera/codegen/compilability.pyvera/codegen/contracts.pyvera/codegen/core.pyvera/codegen/functions.pyvera/codegen/modules.pyvera/codegen/monomorphize.pyvera/codegen/registration.pyvera/codegen/wasi.pyvera/environment.pyvera/errors.pyvera/formatter.pyvera/lexical.pyvera/lsp/convert.pyvera/lsp/extensions.pyvera/lsp/features.pyvera/monomorphize.pyvera/naming.pyvera/obligations/core.pyvera/obligations/session.pyvera/prelude.pyvera/runtime/state.pyvera/skip.pyvera/slots.pyvera/smt.pyvera/tester.pyvera/types.pyvera/verifier.pyvera/wasm/async_fusion.pyvera/wasm/calls.pyvera/wasm/calls_handlers.pyvera/wasm/calls_markup.pyvera/wasm/closures.pyvera/wasm/context.pyvera/wasm/data.pyvera/wasm/helpers.pyvera/wasm/inference.pyvera/wasm/operators.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
Four behaviour fixes, each RED-proofed and differentialed; the rest of the 64 review findings are either doc/test corrections or verified invalid. `_compile_fn`'s old-state snapshot boundary caught `CodegenSkip` alone while the precondition and `decreases` boundaries either side of it catch `CodegenInvariantError` too, so `ensures(old(IO))` — check-green, because the checker types `old(E)` as an unknown type that satisfies a `Bool` postcondition — left `vera compile` as a raw traceback. It is the #939 gap one boundary over and closes the same way, with a source-level reproduction rather than the monkeypatch its three siblings need. `_literal_range_error` could end a literal with ZERO verdicts: a contextual verdict superseding the unconstrained guess withdraws the earlier diagnostic but keeps its dedup key, so a contextual message that repeats it is collapsed as a duplicate and appends nothing. No .vera input reaches it — every transition the checker can take today re-renders the message — but the invariant is what the next contextual verdict rests on. `_handle_exn_always_throws` never asked whether the handler was an `Exn` one, and the structural walk routes every nested handler to it, so a `handle[State<T>]` was analysed with `throw_installed=True`. The answer authorises an `unreachable`; nothing reached a wrong yes, but only because a lowerable State clause body carries a tail `resume(...)`, which made the safety a property of the clause-lowering rule rather than of the predicate. Spec §7.5.1 claimed a bare function type and a non-resolving type expression were both refused by the compilability gate *before* reaching a cell and, in the same sentence, named a cell each. Naming is total and runs first; the refusals are downstream and at different gates — the unresolvable one at the compilability gate, the bare function type only when the function reading it is dropped, its cell declared in the meantime. DE_BRUIJN.md and the `vera/naming.py` docstring repeated the overclaim and are corrected with it. Test-logic: `test_verifier_calls_modules` anchored a demotion's line on `max(caller lines)` — a set the demoted obligation is itself in — so the equality held by construction and stayed green under the very mutant the docstring names. Also a keyword-only `file=` on both legs of the obligation- provenance fixture, a `direct=` matching production resolution, two fixture derivation guards, a pinned E532, a non-vacuity guard on the reserved-name regex, a subprocess timeout, and the LSP resolver-rooting table (six rows, mutation-validated red by dropping the `is_file()` disjunct). All 255 corpus programs emit byte-identical WAT and diagnostics either side of the four compiler changes (digest 5498bc77), and the two instrumented arms — the verdict restore and the snapshot invariant — fire zero times. Co-Authored-By: Claude <noreply@anthropic.invalid>
This was referenced Aug 12, 2026
The final CodeRabbit round on the release PR measured four defects that are real but not minimal fixes on a frozen release tree; each is filed and now tabled, keeping the KNOWN_ISSUES Bugs table one-to-one with the tracker's open bug-labelled issues: - #1284 user-defined `fn get`/`fn put` hijacked in handler clause bodies (three-way checker/codegen desync; gate-only fix measured to break WASM validation) - #1285 `new(State<T>)` reads the name-keyed getter under a multi-`State` row where `old()` is family-keyed (runtime type mismatch from check-green source) - #1286 `_infer_vera_type` never received the #1276 branch-join fix its WAT-side siblings did (latent; no check-green reproduction yet) - #1287 `_stamp_decl_order` skips the prelude stamp when a main-file `type` reuses a prelude name (latent; wrong index inherited by the next decl-order consumer) Skip-changelog: docs-only KNOWN_ISSUES tabling; the CHANGELOG records changes, and these are filings — each issue body carries the evidence. Co-Authored-By: Claude <noreply@anthropic.invalid>
Owner
Author
|
@coderabbitai On the outside-diff finding for |
Owner
Author
|
@coderabbitai On the outside-diff finding for |
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: #!/bin/bash
set -euo pipefail
printf '%s\n' '== resolution.py outline =='
ast-grep outline vera/checker/resolution.py --items all --type function --match 'slot|type' || true
printf '%s\n' '== renderer references =='
rg -n -C 4 'canonical_type_name|_type_expr_to_slot_name|_slot_type_name|slot_ref_key|naming\.slot_name' \
vera/checker/resolution.py tests/test_sql_provenance_309.py || trueLength of output: 5364
✏️ Learnings added
You are interacting with an AI system. |
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: #!/bin/bash
set -euo pipefail
ast-grep outline vera/checker/expressions.py --items all --type function --match 'literal|synth|check' || true
printf '\n--- range diagnostic implementation and call sites ---\n'
rg -n -C 12 '_literal_range_error|expected=BYTE|expected\s*=\s*BYTE' vera/checker/expressions.py
printf '\n--- cited source range ---\n'
sed -n '490,530p' vera/checker/expressions.pyLength of output: 9473 🏁 Script executed: #!/bin/bash
set -euo pipefail
printf '%s\n' '--- definition and all diagnostic-state references ---'
rg -n -C 16 'def _literal_range_error|_literal_range_error|literal.*verdict|range.*verdict|range.*diagnostic' vera/checker
printf '%s\n' '--- integer literal synthesis range paths ---'
sed -n '130,240p' vera/checker/expressions.pyLength of output: 22454
The original finding does not apply. 🧠 Learnings usedYou are interacting with an AI system. |
There was a problem hiding this comment.
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (2)
tests/test_slot_naming.py (1)
649-661: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winAdd the still-missing clean-check assertion.
The source/checker text-alignment half of the earlier review comment is fixed:
parse_to_ast(source)andTypeChecker(source=source, ...)now use the samesourcevalue. The second half of that comment — asserting the check completes with no errors, as the sibling tests at line 598 and line 715 do — is still missing. Without it, a future regression that breaks the check pass for this 250-hop alias chain would not be caught here.✅ Proposed fix
source = "type Box<T> = Option<T>;\n" + source program = parse_to_ast(source) checker = TypeChecker(source=source, file="<deep2>") checker.check_program(program) + assert not [d for d in checker.errors if d.severity == "error"], ( + checker.errors + ) fn = next(d.decl for d in program.declarations🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@tests/test_slot_naming.py` around lines 649 - 661, In the deep alias-chain test around `checker.check_program(program)`, assert that checking completes without errors, matching the clean-check assertions used by the sibling tests. Keep the existing source alignment and slot-name assertions unchanged.vera/README.md (1)
129-142: 📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick winUpdate the
codegen/line-count table.The current
vera/codegen/files contain 18,981 lines, excluding__init__.py. The table lists 18,093 lines and has stale counts for several modules. Update the affected module entries and the package total.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@vera/README.md` around lines 129 - 142, Update the codegen/ line-count table in README.md to reflect the current counts, excluding __init__.py: set the package total to 18,981 and refresh each affected module entry, including the stale counts shown for api.py, core.py, modules.py, registration.py, monomorphize.py, functions.py, tail_position.py, closures.py, contracts.py, assembly.py, compilability.py, and wasi.py.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Outside diff comments:
In `@tests/test_slot_naming.py`:
- Around line 649-661: In the deep alias-chain test around
`checker.check_program(program)`, assert that checking completes without errors,
matching the clean-check assertions used by the sibling tests. Keep the existing
source alignment and slot-name assertions unchanged.
In `@vera/README.md`:
- Around line 129-142: Update the codegen/ line-count table in README.md to
reflect the current counts, excluding __init__.py: set the package total to
18,981 and refresh each affected module entry, including the stale counts shown
for api.py, core.py, modules.py, registration.py, monomorphize.py, functions.py,
tail_position.py, closures.py, contracts.py, assembly.py, compilability.py, and
wasi.py.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: 56528167-ff2c-4064-a854-e04a6e3c0584
⛔ Files ignored due to path filters (2)
assets/diagrams/architecture.svgis excluded by!**/*.svgdocs/llms-full.txtis excluded by!docs/**
📒 Files selected for processing (37)
.pre-commit-config.yamlCHANGELOG.mdDE_BRUIJN.mdFAQ.mdKNOWN_ISSUES.mdREADME.mdROADMAP.mdTESTING.mdspec/07-effects.mdtests/conformance/manifest.jsontests/probes/state_handlers/README.mdtests/test_callee_contract_scope_1220_1225_1226.pytests/test_checker_types.pytests/test_closure_lift_boundaries_1234_1235_1245.pytests/test_codegen_invariant_e699.pytests/test_codegen_monomorphize.pytests/test_exn_throw_payload_1268.pytests/test_handle_exn_divergent_result_1276.pytests/test_lsp.pytests/test_module_generic_namespace_1274.pytests/test_nested_handler_clause_ops.pytests/test_phantom_generic_instances_1271.pytests/test_prelude.pytests/test_slot_naming.pytests/test_slot_naming_differential.pytests/test_sql_provenance_309.pytests/test_verifier_calls_modules.pytests/test_verifier_shadow_audits.pyvera/README.mdvera/checker/core.pyvera/checker/resolution.pyvera/codegen/functions.pyvera/monomorphize.pyvera/naming.pyvera/obligations/core.pyvera/prelude.pyvera/wasm/calls_handlers.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
Two findings from CodeRabbit's incremental review at 619e4aa: - The `<deep2>` alias-chain test aligned its parse/checker text last round but never asserted the check completes cleanly, unlike both its siblings (`<deep>`, `<sib>`); a future regression breaking the check pass for the 250-hop chain would have gone uncaught here. The sibling assertion is copied verbatim. - The codegen/ line-count table in vera/README.md drifted during the burndown inside the doc-counts gate's 10% band: nine module rows and the package total re-measured and corrected (18,093 -> 18,981 excluding __init__.py). The finding's list also named functions.py, tail_position.py and registration.py, which measure exactly as tabled and are unchanged. TESTING.md's per-file row follows the one-line test edit. Skip-changelog: a test assertion plus measured doc-count refreshes; no compiler or user-visible behaviour change. Co-Authored-By: Claude <noreply@anthropic.invalid>
Owner
Author
|
@coderabbitai On the outside-diff finding for |
Owner
Author
|
@coderabbitai On the outside-diff finding for |
|
Tip For best results, initiate chat on the files or code changes.
🧠 Learnings usedYou are interacting with an AI system. |
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: #!/bin/bash
set -euo pipefail
printf '%s\n' '== commit summary =='
git show --no-ext-diff --format=fuller --stat 58555ed6 -- \
vera/README.md TESTING.md tests/test_slot_naming.py
printf '%s\n' '== targeted documentation diff =='
git show --no-ext-diff --format= --unified=4 58555ed6 -- \
vera/README.md TESTING.md tests/test_slot_naming.py
printf '%s\n' '== architecture table context =='
rg -n -C 3 '18,981|18,093|functions\.py|tail_position\.py|registration\.py' vera/README.md
printf '%s\n' '== Python line counts for architecture-table module paths =='
python3 - <<'PY'
from pathlib import Path
import re
text = Path("vera/README.md").read_text(encoding="utf-8")
paths = sorted(set(re.findall(r'`(vera/[A-Za-z0-9_./-]+\.py)`', text)))
for name in paths:
p = Path(name)
if p.is_file():
print(f"{name}: {sum(1 for _ in p.open(encoding='utf-8'))}")
PY
printf '%s\n' '== TESTING row context =='
rg -n -C 3 'test_slot_naming\.py|slot.naming' TESTING.md || trueLength of output: 199009 The current rows match the reported unchanged values. I will now verify the full 🧠 Learnings usedYou are interacting with an AI system. |
This was referenced Aug 13, 2026
chethanuk
pushed a commit
to chethanuk/vera
that referenced
this pull request
Aug 17, 2026
Two defects, one shape: a registry keyed by op NAME was answering a question it does not know the answer to. aallan#1284 — a user-defined `fn get`/`fn put` called under a handler was lowered to the host cell intrinsic. Three sites decided independently whether a bare `get` meant the user's declaration or the operation: the checker resolves user-fn-first (E201/E202 report the user's signature), the declared-effect row withheld the intrinsic when `_fn_sigs` owned the name, and the handler expression installed `get`/`put` unconditionally. From check-green source that gave a silently wrong value, a module WASM validation rejects, or a spurious [E602] naming a State operation the program never contained. `vera.slots.bare_call_denotes_user_fn` now states the checker's rule once; the bare-call dispatch, the three bare-FnCall inference sites, and mono discovery consume it, each over its own name table. The gate is on the DISPATCH, not the registries: the registries record which cell a name reaches, which is true whatever the program's declarations are called. Withholding an entry answered both questions with one table — which is why the gate-only fix measured during PR aallan#1283's review produced a differently-broken module, and why it also cost `State.put(5)` its cell in a program declaring `fn put` (`unknown func: $vera.put`), now lowered as the checker always meant. aallan#1285 — `new(State<T>)` read the name-keyed `_effect_ops["get"]`, so under a multi-`State` row it took whichever family registered first while `old(State<T>)` was already family-keyed. The two sides of one `ensures` clause read different cells: `ensures(new(State<Bool>) == …)` under `effects(<State<Int>, State<Bool>>)` was check- and verify-green and died at load, and where both cells share a width it loaded and refuted a discharged postcondition at runtime. Codegen now carries a family→getter registry built from the per-family CellNames the registration site already computes, and `_translate_new_expr` keys on `_state_effect_family` exactly as `_translate_old_expr` does. Both fixes are proved RED first and by cross-component differential: every expected value is read off the CHECKER's resolution, never off what codegen emits, and each case records what it did before so none can go vacuous. All 256 pre-existing conformance and example programs emit byte-identical WAT (instrument mutation-validated: 39 files move when the predicate is stubbed). Two existing tests encoded the pre-fix codegen answer as their oracle and are corrected: `user_get_under_handler` expected the cell's clone where the checker names the function's, and the qualified-shadow test asserted the loud link failure its own docstring called the wrong semantics. Spec §7.4 now states the declarations-first rule and §7.3.3 that a form naming its type argument names its cell. Pinning both raises in `_translate_new_expr`/`_translate_old_expr` surfaced a checker gap they share — a contract may name a `State<T>` the row never declares — filed as aallan#1298 with a KNOWN_ISSUES row and a test holding today's E699. Closes aallan#1284 Closes aallan#1285 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
1 participant
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.
Release v0.1.10 — the handler-machinery consolidation
This release ends the #1213 burndown: fourteen work PRs, every one through adversarial review to fixed-point, CodeRabbit ledger convergence, and a green 18-context CI wall at its merged head. The thesis, executed: every bug in the cluster traced to two sides re-deriving one fact independently — so each fact now has one derivation.
vera/naming.pyis the one renderer for slot names, reference keys, and State/Exn cell families; handler semantics follow one scoping rule; refined and fn-type cells have their own families; clone bodies route through their declaring module's registries; boundary widths flow from one base derivation; module generics live in one ownership-classified clone namespace; and theVeraprefix is reserved in every declaration namespace.37 bug-labelled issues and 7 others close with this merge (44 total, one keyword per line below). Corpus discipline held throughout: every PR shipped with a corpus-wide differential, and the release tree's full battery is green — 10,149 tests, 213 conformance programs, 42 examples, 261 canonical corpus programs.
Release mechanics in this PR's final commit
Version 0.1.9 → 0.1.10 across the six-value sync surface (with
uv.lockregenerated); the CHANGELOG[Unreleased]section cut to[0.1.10] - 2026-08-12with a fresh empty[Unreleased]and compare-link references; the HISTORY row in the Stage 19/20 table; the #1213 lead row deleted from ROADMAP (the only closes-list row present — swept programmatically); site assets regenerated; the release-notes extraction verified end-to-end against the workflow's non-empty-section validation.Post-cut convergence commits.
2bf3cc7cremoves the xdist race from the temp-file leak check (captured-name isolation) and extends the doc-counts gate to the tag-derived release count.bb9f25f7+619e4aa5close the final CodeRabbit full-diff round — 64 findings verified: 27 fixed, 4 filed, 33 skipped with measured traces, every disposition replied on this PR. The four RED-proofed behavior fixes:ensures(old(IO))now yields one[E699]instead of a raw traceback; an out-of-range literal keeps exactly one range verdict (the supersede/dedup hole closed); the divergence predicate refuses to answer for a non-Exnhandler; and spec §7.5.1's refusal claim corrected against the compiler (withDE_BRUIJN.mdand thevera/naming.pydocstring). All 255 corpus programs emit byte-identical WAT across the four compiler changes, and two independent read-only verification agents concurred with every disposition before it was posted.Deliberately not closed (each tracked with its residual stated)
throw's payload obligation: the static half shipped (loud E503/E505, honesttier3_unguardeddisclosure); the runtime guard and the monomorphization-coverage residuals are documented on the issue with the codegen sizing.fn get/fn putcalled in a handler clause body #1284–_stamp_decl_orderskips the prelude stamp when a main-filetypereuses a prelude name #1287 — the final CodeRabbit round's four filed discoveries, each real but refactor-shaped or not yet reproducible on a frozen release tree, tabled in KNOWN_ISSUES with full evidence: Codegen hijacks a user-definedfn get/fn putcalled in a handler clause body #1284 (a user-definedfn get/fn putin a handler clause body is hijacked by the lowering — three-way checker/codegen desync; the gate-only fix was measured to break WASM validation, so it needs the one-predicate consolidation),new(State<T>)reads the wrong cell's getter under a multi-Stateeffect row #1285 (new(State<T>)reads the name-keyed getter under a multi-Staterow whereold()is family-keyed — runtime type mismatch from check-green source; needs a family→getter registry),_infer_vera_typestill reads one branch ofIfExpr/MatchExpr— the #1276 join fix's unfixed sibling #1286 (_infer_vera_typenever received the A handle[Exn] whose clause body and handled body both diverge emits a result-less block into a result-expecting context: check-green invalid WASM #1276 branch-join fix its WAT-side siblings did — latent, no check-green reproduction constructible within the round),_stamp_decl_orderskips the prelude stamp when a main-filetypereuses a prelude name #1287 (_stamp_decl_orderskips the prelude stamp when a main-filetypereuses a prelude name — latent index defect inherited by the next decl-order consumer).For the maintainer
Merge with a merge commit (the v0.1.0 release model). On merge,
.github/workflows/release.ymldetects the version increase, validates the synchronized version and CHANGELOG section, builds and tests the artifact, pauses at thepypienvironment for your approval, publishes via Trusted Publishing, verifies registry hashes, then tags and cuts the GitHub Release at the merge SHA. No manual tag or upload.Closes #1207.
Closes #1208.
Closes #1209.
Closes #1210.
Closes #1211.
Closes #1212.
Closes #1213.
Closes #1214.
Closes #1215.
Closes #1216.
Closes #1217.
Closes #1218.
Closes #1219.
Closes #1220.
Closes #1221.
Closes #1223.
Closes #1225.
Closes #1226.
Closes #1227.
Closes #1228.
Closes #1229.
Closes #1231.
Closes #1234.
Closes #1235.
Closes #1236.
Closes #1237.
Closes #1240.
Closes #1241.
Closes #1242.
Closes #1243.
Closes #1244.
Closes #1245.
Closes #1246.
Closes #1248.
Closes #1251.
Closes #1252.
Closes #1253.
Closes #1255.
Closes #1256.
Closes #1260.
Closes #1269.
Closes #1271.
Closes #1274.
Closes #1276.
Summary by CodeRabbit
New Features
Bug Fixes
Documentation