Route modules like the checker: one result table, clone-body registries, scoped membership (#1207, #1223, #1241, #1243, #1244, #1253) - #1272
Conversation
…#1207) An effect operation in a value position that fixes a generic's type argument was answered by two independent consultors that disagreed: monomorphization DISCOVERY had no effect-operation registry at all, so a `get(())` driving an instantiation fell through to the literal-driven `Int` default and emitted `pick$Int`, while the WASM call-REWRITE read the cell's type from `_effect_op_result_vera` and called `pick$Nat`. The clone dangled, the caller was skipped with E602, `main` was dropped with E620, and `vera compile` ended with "No exported functions" on a check-green, verify-clean program. `vera.slots.effect_op_result_names` is now the one derivation of op name -> Vera result-type name, and all three sites that need that answer take it from there: codegen's per-function registry built from the declared `effects(<State<T>>)` row, the handler-expression registry inside `_translate_handle_state`, and mono discovery's new scoped walk. Scope is MIRRORED rather than approximated, because codegen's two injection sites are scoped differently and a registry that ignored the difference would move the desync rather than close it: * a `handle` installs its table over its BODY only -- the state-init expression and the clause bodies belong to the enclosing context (#1211), so an operation written there still names the outer cell; * an operation the DECLARED row provides is not injected when a user function already owns the name, which discovery now decides from the same function table (`_fn_sigs`, mirrored into `MonoContext.fn_names`) that codegen's `_effect_ops` guard consults. The name is the alias-OPAQUE source spelling on both sides, so `handle[State<Count>]` with `type Count = Nat` instantiates `pick$Count`; resolving the alias on one side only would dangle exactly as before. Test-first, both directions. The proving check is a DIFFERENTIAL over the two consultors, not a unit test on either -- the compiler's own E602 IS the two sides disagreeing -- and each case additionally pins WHICH name they agreed on, so an alignment on the wrong one still fails. RED on the branch base: all four instantiation-driving cases failed with "call target 'pick$Nat' / 'second$Nat' not registered in this module". The shadowed-name control (`private fn get(@Unit -> @Bool)` in a `State<Int>` row, whose clone must be `pick$Bool`) was green before and after -- it guards the alignment against over-reaching rather than re-testing the repro. Conformance program `ch07_state_op_generic_instantiation` carries the array-element, direct-argument and declared-effect-row forms end to end (suite now 207); `tests/test_mono_effect_op_naming_1207.py` holds the differential and both controls. The `tests/probes/` `p15*` trio this promotes is retired, per the #1213 probe-disposition workflow. Co-Authored-By: Claude <noreply@anthropic.invalid>
A `forall<U>` `where`-helper under a `forall<T>` parent is instantiated only during clone HOISTING -- outside the top-level worklist, which is the loop that rescans every clone it emits. So the helper clone's own body was never walked, and a top-level generic called from inside the helper was discovered only in its still-generic spelling, where the argument's type is the enclosing type VARIABLE: `pick$U` got emitted while the call-rewrite asked for `pick$Bool`. On a check-clean, verify-clean program that is an E602 skip, an E620 drop of the parent, another of `main`, and "No exported functions". Hoisting and the worklist are now a FIXPOINT rather than two phases: each hoisting round re-seeds the worklist from the bodies it just produced, and any clones that yields go back through hoisting for their own where-trees. The main worklist body is extracted as `_drain_generic_worklist` so both drives are the same loop over the same `seen` set. The same walk had the SIBLING case, fixed here too: a helper's concrete clone can call a sibling helper at a type only that clone knows (inside the generic `outer<U>`, `inner(@U.1, @U.0)` binds `inner`'s variable to the type variable's NAME), so the helper FAMILY is now discovered as a family over a GROWING body set -- each clone fed back in -- instead of one helper at a time against its still-generic siblings. Both sides drive one leaf for that discovery, `Monomorphizer.collect_generic_helper_instances`, with `collect_clone_nested_generic_instances` re-expressed on top of it. PAIRING. The codegen half alone makes `pick<Bool>` an instantiation codegen emits and the verifier never checks -- a false Tier-1 -- so the verifier's `record_nested` grows the matching family fixpoint and feeds each helper clone's top-level callees back into its own worklist. The shape is in `tests/test_monomorphize_differential.py`'s `_INLINE_CORPUS`, whose #732 check asserts verifier >= codegen; with only the codegen half applied it fails with verifier did not cover instantiation(s) codegen emits: [('gug_parent$where$gug_inner', ('Bool',)), ('gug_pick', ('Bool',)), ('gug_pick', ('U',))] so the two halves cannot land apart. Test-first, both directions. RED on the branch base: six of the eight cases in `tests/test_generic_under_generic_callees_1223.py` failed -- the user-generic, prelude-generic (`option_unwrap_or`) and two-level nesting shapes, on both the compile-clean assertion and the registered-vs-resolved differential. The two that were green before and after are the non-generic-parent control, which is what proves the trigger is the generic ancestor rather than the nested helper. The differential captures the emitted mono-decl NAMES (not `_emitted_instances`, whose nested entries are keyed by the concrete-free lexical chain) and captures the rewrite side on `_resolve_generic_call` (not from the WAT, which loses the dangling `call` along with the skipped caller). One residual is left as-is and reported rather than fixed here: the still-generic spelling's `pick$U` clone is still emitted and still loudly skipped (E604). That is noise on an otherwise clean compile, not a wrong answer, and suppressing it means filtering instantiations whose type vector mentions an enclosing scope's type variables -- a change to the shared walk with its own blast radius. Co-Authored-By: Claude <noreply@anthropic.invalid>
, #1243) A public generic in `glib` whose body calls `glib`'s private `need` is cloned by the importer and compiled into the importer's flat module. Both consumers of that clone body then resolved the bare name in the IMPORTER's namespace: * #1241, verifier -- `_scoped_fn_lookup` fell through to this program's registry, because `_declaring_module_scope` swapped the naming env, the source buffer and the file name but NOT the function registry. The module's own `CalleeScope` (the #1225 contract-READING pin) is now also keyed by module path and carried by that scope, so a body declared in a module walks in the namespace it was written in. * #1243, codegen -- the clone-emission door was the ONE door that did not thread `_module_intra_renames`, which Passes 2.5 and 2.6 already thread, so a bare sibling call landed on the importer's same-named function instead of the module's `mod$...` emission. The checker's answer is the module's own (spec §8.5.1), and the type-discriminating probe proves it: `glib`'s `need(@int -> @int)` beside an importer's `need(@int -> @Bool)` checks clean, which only types if glib's is meant. MEASURED, both before and mid-fix. At base: a module that verifies clean and runs to 111 standalone is REFUSED through an importer (E500 on its honest `ensures(@Int.result == 111)`, refuted against the importer's function returning 999) and, compiled, traps on that same postcondition; the type-discriminating pair emits invalid WASM (`expected i64, found i32`) from check-green source. With ONLY the verifier half applied (measured by stashing the codegen half and re-running this suite), `vera verify` reports clean and the run raises Postcondition violation in gen$Int(@int -> @int) ensures(@Int.result == 111) failed -- the false Tier-1 the issue predicted, reproduced. The commit structure makes one-half-green impossible because the TESTS do, not because the diff is atomic: every case in `tests/test_clone_body_declaring_module_1241_1243.py` asserts the verify verdict AND the runtime value in the same test, so the verifier half alone fails on the value and the codegen half alone fails on the verdict. Every expected value is the oracle taken from the module verified and run STANDALONE, never from what the importer produces. Test-first, both directions. RED at base: three cases (private callee, two-hop private chain, type-discriminating pair). GREEN before and after: the standalone oracle, and the unshadowed-callee control -- which is what pins the defect to the SHADOWED name rather than to cross-module calls in general, so a reroute that fired unconditionally would show up there instead of passing either way. Co-Authored-By: Claude <noreply@anthropic.invalid>
`mid.vera` imports only `cap` from `deep` and its body also calls `other`. Checked directly that was an E200 -- correct, spec §8.5.1: a module's bodies resolve in the namespace ITS file declares and imports. Checked as a dependency of `main`, the same program was accepted in silence, because the importer only REGISTERED each module (harvesting what it declares) and never checked its bodies at all. The lenient verdict is the dangerous one: it lets a module use names it never imported, and codegen then resolves them out of the importer's flat namespace, so the program runs on a binding the module was never entitled to. The verifier has honoured the module-local rule regardless of entry point since #1225; this is the checker catching up. MEASUREMENT FIRST, as instructed. Blast radius across the whole corpus is ZERO: only 7 of the corpus programs import a non-stdlib module at all, none of their imported modules carries a standalone diagnostic, and all 207 conformance programs and 42 examples pass unchanged. One existing expectation moves, and toward the stricter reading. A module redeclaring the built-in `IO` effect and calling `IO.print(a, b)` now reports E152 AND the E203 arity error -- exactly what `vera check` on that module reports standalone (verified directly). E203 names the CANONICAL built-in's arity ("expects 1 argument(s), got 2"), so the property the case was written for -- the rejected block is not registered -- is now asserted directly rather than by its absence. The same change closes the issue's second shape: a module body binding an `@Int`-returning call to a `@Bool` slot checked clean through an importer, verified Tier-1, and failed at compile. It also removes a duplicate derivation rather than adding one. `_collect_module_artifacts` already ran a full per-module check and surfaced imported-body ERRORS -- but only on the codegen paths (compile/run/serve/test), and warnings-only diagnostics like this one never surfaced there either. It now collects artifacts alone, with the new pass's memo threaded into its sub-checkers so the added work stays one body check per module across the whole call rather than N per module. Test-first, both directions. RED at base: the leaked unimported name, the type-error-through-importer shape, and the report-once diamond. GREEN before and after: the honest control that imports what it uses -- which is what keeps the new body check a visibility rule rather than a blanket rejection of cross-module programs -- and both entry points into an import cycle. The cases assert EQUALITY between the two entry points rather than "the importer warns", because the property is agreement: a change making the standalone verdict lenient would satisfy a one-sided assertion and must fail here on the standalone leg. Co-Authored-By: Claude <noreply@anthropic.invalid>
…1253) `_adt_layouts` is one map across every absorbed namespace, and the naming environment's `data_types` set was derived from all of it -- so inside `_module_alias_scope(blib)` a sibling module's ADTs were still members of `blib`'s namespace, while the checker registers each module in isolation and never sees them. For a `blib` signature fn bcount(@array<Float>, @array<Int> -> @int) with `Float` an ADT `alib` declares and `blib` never imports, the two sides render the same declaration differently -- checker `['Array<?>', 'Array<Int>']`, codegen `['Array<Float>', 'Array<Int>']` -- which is the Membership is now the owning namespace's own declarations plus what that namespace IMPORTS: public only, and only the names an explicit import list mentions, which is exactly the checker's view. So an unimported sibling ADT is as opaque to codegen as it is to the checker, and so is a PRIVATE one -- the visibility dimension appended to the issue, where codegen registers a module's private ADTs (#1008) but the checker registers only its public ones. Imports are read per namespace and never inherited, because §8.6.4 visibility is a property of the importer: a module reached transitively from the entry program is a DIRECT import of whichever module names it, and holds what THAT module's import list allows. The active namespace travels with the alias maps and the declaration-index space in `_module_alias_scope`, so the three answers to "whose namespace is this?" cannot come apart. The permissive fallback is deliberate: with no computed membership (a single-file program, or any point before `_register_modules` runs) the reader takes the whole map, which is what codegen did everywhere before. A wrongly-EMPTY membership would re-open the divergence in the other direction, rendering a name the module does own as opaque. Test-first, both directions. The proving check is a DIFFERENTIAL over the two slot tables, not an assertion on either -- both sides agreeing on the wrong name would satisfy a one-sided check -- and each case also pins the value the checker derives. RED at base: the unimported-public-sibling and private-sibling cases. GREEN before and after: the imported positive control (`Array<Float>` on both sides), which separates scoping the membership from erasing cross-module ADTs, and the entry program's own view of an ADT it imports by name. The E609 rail is untouched and still refuses two modules declaring one ADT name outright, so the owner-slot ordering half of the visibility case stays masked behind it. Co-Authored-By: Claude <noreply@anthropic.invalid>
The module-routing cluster is closed, so its tracker rows come out of the curated tables: #1207 (mono discovery vs effect-op result naming), #1223 (generic-under-generic callees), #1241 + #1243 (imported clone bodies routed through the declaring module), #1244 (entry-point-dependent import visibility), #1253 (codegen ADT membership). The Bugs table goes from 10 rows to 4. `ROADMAP.md`'s #1213 row drops #1207 from the remaining list; #1233 (outward cell addressing for same-family nested handlers) is what is left of that cluster. Each issue's CHANGELOG `[Unreleased]` entry landed with its own fix commit, so nothing moves here but the tables. Skip-changelog: bookkeeping only -- every issue's entry landed with its fix. Co-Authored-By: Claude <noreply@anthropic.invalid>
The six commits above were rebased from cd32636 onto ef7c04c. Every conflict was in a count/doc file; `vera/verifier.py` auto-merged. This commit carries the resolution work that only makes sense at the tip. * COUNTS come from `scripts/check_doc_counts.py`, not from arithmetic: 10,075 tests across 156 files, 207 conformance programs. Upstream's 10,034/151/206 and my 10,037/155/207 were both stale against the merged tree, so neither side's numbers were kept. * `docs/llms-full.txt` and the rest of `docs/` are regenerated by `scripts/build_site.py` rather than hand-merged. * `TESTING.md` loses a duplicate `test_nat_int_widening.py` row. #1268 reworded that row while this branch carried the pre-#1268 text, so a digit-insensitive resolution read the difference as an edit of mine and kept BOTH copies. Upstream's is the current description and the live counts; mine goes. Verified rather than assumed: * CONTENT INTEGRITY -- a diff-of-diffs over `vera/ tests/ spec/` (excluding the count file `vera/README.md`) between cd32636..pre-rebase and ef7c04c..HEAD is identical modulo hunk offsets, across all 24 files. * DOC MERGE -- a three-way check against the common base: every row either side added is present, every row either side deleted is absent, and a row only upstream reworded carries upstream's text. That check is what found the duplicate above; the count oracle cannot see a description drift. * KNOWN_ISSUES -- row-id set comparison. Upstream deleted #1251's row and added #1268/#1269; this branch deletes six. All three operations are applied, 45 rows, no duplicates. C5 INTERACTION, probed rather than inferred. #1268 obligates a `throw` payload, and a clone containing a `throw` is now verified under this branch's pinned module registry. Measured on both trees with the same fixture (an imported `forall<T>` whose body throws a provably-negative payload into an `Exn<Nat>`): ef7c04c gives 4 Tier-1 + 1 Tier-3, and so does this branch -- identical, with and without an importer-side shadow of the payload function. No movement. The probe did surface a PRE-EXISTING observation, present unchanged at ef7c04c and therefore not this branch's: the same payload refutes as a loud E503 in a non-generic function but demotes to Tier-3 inside a monomorphized clone. Full manual gate on the rebased tree (hooks do not run on `rebase --continue`): pytest 9917 passed / 132 skipped / 26 deselected, mypy clean, ruff and ruff --select S clean, explicit-encoding, 207 conformance, 42 examples, 255 corpus canonical, doc counts, site assets, diagnostic fields, limitations sync, e602-clean. Skip-changelog: rebase resolution; every entry landed with its own fix commit. Co-Authored-By: Claude <noreply@anthropic.invalid>
📝 WalkthroughWalkthroughThe compiler now checks imported module bodies under their own imports, scopes ADT membership per module, preserves declaring-module resolution for imported clones, and discovers nested generic instances to a fixpoint. Shared effect-operation naming and regression coverage were added. Documentation counts were updated. ChangesCompiler correctness
Estimated code review effort: 4 (Complex) | ~60 minutes Sequence Diagram(s)sequenceDiagram
participant SourceProgram
participant TypeChecker
participant ContractVerifier
participant Monomorphizer
participant CodeGenerator
participant WasmHandlers
SourceProgram->>TypeChecker: register modules and check bodies
TypeChecker->>ContractVerifier: provide module artefacts and scopes
ContractVerifier->>Monomorphizer: collect generic calls and effect-operation results
Monomorphizer->>CodeGenerator: provide concrete helper instances
CodeGenerator->>WasmHandlers: align generated effect-operation result names
Possibly related issues
Possibly related PRs
Suggested labels: 🚥 Pre-merge checks | ✅ 8✅ Passed checks (8 passed)
✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Comment |
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## release/v0.1.10 #1272 +/- ##
===================================================
- Coverage 94.05% 94.05% -0.01%
===================================================
Files 100 100
Lines 35431 35594 +163
Branches 458 458
===================================================
+ Hits 33324 33477 +153
- Misses 2094 2104 +10
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:
|
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 8
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
vera/verifier.py (1)
1640-1650: 🗄️ Data Integrity & Integration | 🟡 Minor | ⚡ Quick winRecurse through imported
wherehelpers when buildingfn_names. Codegen registers these helpers in_fn_sigs, but the verifier currently records only imported top-level functions. A helper namedgetorputcan therefore be treated as an effect operation by verification but as a user function by codegen. Keep return-type inference top-level-only, but add the imported helper names recursively.🤖 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/verifier.py` around lines 1640 - 1650, Update the `_resolved_modules` traversal in the verifier to recursively collect names of imported `where` helper functions into `fn_names`, including nested helpers such as `get` and `put`. Keep `fn_ret_types` and `fn_ret_type_exprs` populated only from top-level `ast.FnDecl` declarations, matching the existing return-type inference behavior.
🤖 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 `@AGENTS.md`:
- Line 11: Update the negative-fixture count in the conformance-suite
description to twenty-eight so it matches the 28 names enumerated in the list,
leaving the fixture names and verification requirements unchanged.
In `@TESTING.md`:
- Line 194: Update the “Running the conformance suite” text and every other
occurrence of the outdated 1,030 test count in TESTING.md to 1,035, while
preserving unrelated counts and Markdown formatting. Search the entire document
to ensure no old literal remains.
In `@tests/test_clone_body_declaring_module_1241_1243.py`:
- Around line 195-231: The _GLIB_CHAIN fixture comment incorrectly describes
nested where-helper coverage while mid and need are top-level private functions.
Either revise the comment to identify this as a two-hop private chain, or modify
the fixture so need is declared inside mid’s where block and add the
corresponding parameter wiring for the glib module.
- Around line 301-309: Complete the truncated explanatory clause in the
docstring of test_type_discriminating_callee_compiles at
tests/test_clone_body_declaring_module_1241_1243.py:301-309, stating that
routing to or calling the importer’s `@Bool` function would emit invalid WASM from
check-green source. Apply the same completed clause to the fixture comment at
tests/test_clone_body_declaring_module_1241_1243.py:144-148.
- Around line 149-173: Remove the duplicate _GLIB_TYPED fixture and reuse
_GLIB_VALUE in test_type_discriminating_callee_compiles, keeping type
discrimination solely in _APP_TYPED’s need(`@Int` -> `@Bool`) declaration. Update
the test setup or references so the glib fixture still uses the shared value
definition.
- Around line 74-89: Update _verify_codes to check proc.returncode and handle
non-JSON stdout by surfacing both stdout and stderr in the failure result,
clearly identifying which CLI output was unavailable or invalid. Also update
_run_value to safely handle successful executions with empty stdout, returning
an explicit failure marker instead of indexing an empty splitlines result.
In `@tests/test_import_visibility_entry_point_1244.py`:
- Around line 110-120: Update the `_cli` helper’s `subprocess.run` invocation to
include a finite timeout, ensuring non-terminating CLI subprocesses fail
promptly while preserving the existing command, output capture, encoding,
return-code handling, and environment setup.
In `@vera/codegen/modules.py`:
- Around line 686-690: The module membership setup around `_builtin_adt_names`
and `_adt_namespace_members` must include the conditionally injected prelude
ADTs (`Json`, `HtmlNode`, `Request`, and `Response`) in every namespace. Update
the post-`_register_modules` membership construction to track the actual
injected types so module-backed programs expose them through
`AliasEnv.data_types`, and add regression coverage for this behavior.
---
Outside diff comments:
In `@vera/verifier.py`:
- Around line 1640-1650: Update the `_resolved_modules` traversal in the
verifier to recursively collect names of imported `where` helper functions into
`fn_names`, including nested helpers such as `get` and `put`. Keep
`fn_ret_types` and `fn_ret_type_exprs` populated only from top-level
`ast.FnDecl` declarations, matching the existing return-type inference 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: cd43fd49-6743-4f21-903c-e1dc14f4f614
⛔ Files ignored due to path filters (9)
docs/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/**tests/conformance/ch07_state_op_generic_instantiation.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!**/*.vera
📒 Files selected for processing (30)
AGENTS.mdCHANGELOG.mdCLAUDE.mdFAQ.mdKNOWN_ISSUES.mdREADME.mdROADMAP.mdSKILL.mdTESTING.mdtests/conformance/manifest.jsontests/probes/README.mdtests/probes/state_handlers/README.mdtests/test_adt_membership_scope_1253.pytests/test_checker_modules.pytests/test_clone_body_declaring_module_1241_1243.pytests/test_generic_under_generic_callees_1223.pytests/test_import_visibility_entry_point_1244.pytests/test_mono_effect_op_naming_1207.pytests/test_monomorphize_differential.pyvera/README.mdvera/checker/core.pyvera/checker/modules.pyvera/codegen/core.pyvera/codegen/functions.pyvera/codegen/modules.pyvera/codegen/monomorphize.pyvera/monomorphize.pyvera/slots.pyvera/verifier.pyvera/wasm/calls_handlers.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
💤 Files with no reviewable changes (1)
- KNOWN_ISSUES.md
Adversarial review record — round 1 (
|
…guards Adversarial round + CodeRabbit, folded into one round. FIXED * ADT membership now includes the PRELUDE-injected ADTs (CR). `Json`, `HtmlNode`, `Request` and `Response` register in Pass 1.2, two passes after `_register_modules` computes the membership sets, so the built-in snapshot taken there necessarily missed them -- while the checker's `TypeEnv` has carried them from the start. Global infrastructure is now DERIVED (every registered layout no namespace declares) instead of snapshotted, so it cannot go stale with registration order; the built-in snapshot is still unioned in, so a module declaring a built-in's name cannot hide it from everyone else. RED at base on the membership assertion. Measured inert at emission: the whole 255-program corpus compiles to BYTE-IDENTICAL WAT with and without the correction, which is expected -- `AliasEnv.data_types` changes an answer in exactly one place (`naming._resolve_named`) and only for `Decimal` and the one `REMOVED_ALIASES` entry, `Float`. The test therefore asserts the SET, and says so. * `tests/test_adt_membership_scope_1253.py` is base-runnable again. It called `_modules_visible_to`, which THIS branch's #1244 commit adds, so its RED/GREEN claim was not reproducible from the artifact. It now spells out the per-module resolved list the way `_collect_module_artifacts` has since #987. Verified at `ef7c04c0`: 2 RED (both membership cases), 2 GREEN (the controls) -- exactly the claim the commit makes. * `fields()`-completeness guard on `Monomorphizer._collect_calls`'s `HandleExpr` arm. That arm hand-enumerates its children because they are walked in DIFFERENT scopes, so it cannot use the generic recursion, which makes it the one place a new field would go silently unwalked -- and an unwalked child hides every generic call inside it (a dangling clone with no diagnostic pointing here). Mutation-validated: with an extra field on a `HandleExpr` subclass the guard fires; unmutated, it does not. * The `_collect_module_artifacts` cost note was stale after #1244 and is corrected against what the code does now: THIS pass is still codegen-only and O(N^2), but a module's BODY is no longer checked only on those paths -- `check`, `verify` and the warm session all pay one sub-check per resolved module, and the session pays it again per re-check. The registration-memo optimisation is cited as #1275. * Test robustness (CR): the two-hop fixture's comment said "where helper" where `mid`/`need` are top-level privates; the truncated docstring and fixture comment now finish the sentence (routing to the importer's `@Bool` function emitted invalid WASM, `expected i64, found i32`, so the failure is a load trap rather than a wrong value); `_GLIB_TYPED` was a byte-identical duplicate of `_GLIB_VALUE` and is gone, with the discrimination kept in `_APP_TYPED`; `_verify_codes` surfaces a non-JSON stdout as itself instead of a bare `JSONDecodeError`, and `_run_value` distinguishes a zero exit that printed nothing from a value. Finite 300s timeouts on both files' CLI subprocesses. * Doc counts by oracle: `TESTING.md`'s prose "1,030 parametrized tests" (the gated table row was already right) -> 1,035, confirmed by collecting `tests/test_conformance.py`. `AGENTS.md`'s "twenty-six negative fixtures" -> twenty-eight, confirmed three ways: the sentence enumerates 28 names, the manifest carries 28 `expected_error` entries, and this branch's new conformance program is a `run`-level positive, so the figure was already stale at base. * `KNOWN_ISSUES.md` gains the two owed rows: #1274 (the public-generic clone-name collision) and #1271 (the `pick$U` discovery noise), each citing the other as the shared clone-namespace follow-up. SKIPPED, with the trace * CR asked for imported WHERE-HELPER names to be collected recursively into `fn_names`. Doing that would CREATE the desync it means to close. `fn_names` mirrors codegen's `_fn_sigs` for one decision -- is a declared row's `get`/`put` an op, or a user function shadowing it -- and #1015 hoists every imported module's helpers to parent-qualified names BEFORE registration. Measured on a module whose helper is named `get`: codegen's `_fn_sigs` = {`outer`, `outer$where$get`}, the verifier's `fn_names` = {`outer`}, bare `get` absent from BOTH. Adding it would suppress the State op for a row codegen still injects it for. The asymmetry with LOCAL helpers (collected bare) is faithful: codegen keys those bare. Recorded at the `fn_names` comment so it is not re-raised. Full gate: pytest 9918 passed / 132 skipped / 26 deselected, mypy, ruff + --select S, explicit-encoding, 207 conformance, 42 examples, 255 corpus canonical, e602-clean, doc counts, site assets, diagnostic fields, limitations sync (with --check-states, 47 rows). Co-Authored-By: Claude <noreply@anthropic.invalid>
|
@coderabbitai On the outside-diff note for vera/verifier.py (~1640-1650, collecting imported where-helper names recursively into fn_names): verified against current code and SKIPPED — the suggested change would CREATE the desync it means to close. Since #1015, imported where-helpers are hoisted to parent-qualified names BEFORE registration: on a module whose helper is named get, codegen's _fn_sigs holds {outer, outer$where$get} and the verifier's fn_names holds {outer} — the bare name is absent from BOTH sides, which is the agreement that matters. Adding bare helper names to fn_names would suppress the State op for a row codegen still injects it for. The asymmetry with LOCAL helpers (collected bare) is faithful because codegen keys those bare. Recorded as a comment at the fn_names construction so the question isn't re-derived. |
|
Tip For best results, initiate chat on the files or code changes.
Imported helpers are registered with parent-qualified names, such as I withdraw the outside-diff finding. The recorded comment at the ✏️ Learnings added
You are interacting with an AI system. |
Round-1 dispositions (
|
Verify pass (independent,
|
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 (1)
vera/monomorphize.py (1)
1428-1461: 🎯 Functional Correctness | 🟠 Major | ⚡ Quick winReplace the handler operation registry instead of merging it.
Lines 1459-1461 retain operation result types from the enclosing scope. A handler body must use only its handled effect operation registry. The current merge can infer a generic clone from an outer operation that is not visible in the handler body.
This branch also does not exclude names in
self.ctx.fn_names. A user function that shadowsgetcan then be inferred as aStateoperation.Build this registry from
node.effectonly, apply the same shadow filter as_row_op_result_types, and restoresaved_opsafterwards. Add regressions for nested handlers with distinct operations and a user-definedget.Proposed fix
- self._op_result_types = { - **saved_ops, **effect_op_result_names([node.effect]), - } + self._op_result_types = { + op: result_type + for op, result_type in effect_op_result_names( + [node.effect], + ).items() + if op not in self.ctx.fn_names + }🤖 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/monomorphize.py` around lines 1428 - 1461, Update the HandleExpr branch in _collect_calls to replace, rather than merge, _op_result_types with the registry derived from node.effect, filtering names present in self.ctx.fn_names consistently with _row_op_result_types. Keep the handler-body walk using only this registry, and restore saved_ops after completing the handler scope; add regressions covering nested handlers with distinct operations and a user-defined get.
🤖 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 `@vera/monomorphize.py`:
- Around line 1428-1461: Update the HandleExpr branch in _collect_calls to
replace, rather than merge, _op_result_types with the registry derived from
node.effect, filtering names present in self.ctx.fn_names consistently with
_row_op_result_types. Keep the handler-body walk using only this registry, and
restore saved_ops after completing the handler scope; add regressions covering
nested handlers with distinct operations and a user-defined get.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: 086dd3af-b3cf-4bd7-bc59-80ea78ed6332
⛔ Files ignored due to path filters (1)
docs/llms-full.txtis excluded by!docs/**
📒 Files selected for processing (16)
AGENTS.mdCHANGELOG.mdFAQ.mdKNOWN_ISSUES.mdREADME.mdROADMAP.mdTESTING.mdtests/test_adt_membership_scope_1253.pytests/test_clone_body_declaring_module_1241_1243.pytests/test_import_visibility_entry_point_1244.pyvera/README.mdvera/checker/core.pyvera/codegen/core.pyvera/codegen/modules.pyvera/monomorphize.pyvera/verifier.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
…e merge Three dispositions from the verify pass and the late CodeRabbit outside-diff. (1) The membership-fix comment overclaimed. "The builtin snapshot is unioned in, so a module declaring an ADT that shares a built-in's name cannot hide the built-in from everyone else" holds only for the Pass-0.5 snapshot -- which does not contain the four demand-injected prelude names this fix is about. Reproduced: a module declaring `public data Json` puts `Json` in the declared set (builtin_snap_has_Json=False), subtracting it from infrastructure, and the ENTRY program's members lose the prelude `Json`; no E609/E610 fires on that declaration either, the rails being keyed on the same Pass-0.5 snapshot. Inert today for the same reason the rest of the rule is inert (`data_types` decides an answer only for `Decimal` and `REMOVED_ALIASES`), and pre-existing at both baselines -- but a real constraint, so the comment now states what the union covers, what it does not, and what closing it would take. (2) `test_prelude_adts_are_members_of_every_namespace` still called the membership helpers this fix adds, so at `ef7c04c0` it died on `AttributeError` before reaching its assertion -- one test back down the pattern round 1 removed. It now reads `_alias_env.data_types` under the pre-existing `_module_alias_scope`, which is the membership set as consumers actually receive it, and states the invariant from the FIXTURE (neither file declares an ADT, so every registered layout must be a member) rather than from the implementation's own bookkeeping. ef7c04c (branch base) prelude case PASSES -- no membership filter exists yet, so every layout is a member and the defect it pins does not exist. The two #1253 slot-table cases are RED there, per their commit. f4c5070 (pre-fix tip) prelude case RED on its assertion -- the meaningful red baseline. #1253 cases green. HEAD all five green. No test in this file errors at any baseline now; each degrades to its assertion. (3) CR asked for the `HandleExpr` discovery branch to REPLACE the enclosing operation registry rather than merge it. SKIPPED -- it would re-create #1207, measured rather than argued. Both sites merge at HEAD and agree: discovery writes `{**saved_ops, **effect_op_result_names(...)}` and `_translate_handle_state` writes `{**saved_result_vera, **effect_op_result_names(...)}`, while `_translate_handle_exn` never touches the registry at all. So a handler contributing NO result type must leave the enclosing one answering. Patched discovery to replace-semantics and compiled an `Exn` handler nested inside a `State<Nat>` one: discovery emitted `pick$Int` where the rewrite asked for `pick$Nat` -> E602, `main` dropped, "Available exports: pick$Int". That is #1207's exact signature. CR's REGRESSION ask was legitimate even though the semantics is right: under that patch the whole existing suite stayed green (33 passed), so nothing pinned it. Three cases added, and honestly only the first discriminates merge from replace -- the other two pin adjacent semantics CR named and pass under both: exn_nested_in_state the decisive one; RED under replace nested_distinct_state inner `State<Int>` owns `get` for its own body, outer answers outside it (6 + 9 = 15) user_get_under_handler a user `get(@Unit -> @int)` loses to the operation INSIDE a handler body, matching codegen's unconditional `_effect_ops` overwrite (and unlike the declared-row site, where the function wins -- both now pinned) All three verified three-way beforehand: checker accepts, discovery and the rewrite name one clone, the compiled program returns the checker's value. The invariant is recorded at the merge itself so the next reader meets it there. Gate: touched suites, mypy, ruff + --select S, doc counts, site assets, limitations sync; full hook battery on the commit. Skip-changelog: comment accuracy, test-harness coupling and regression pins; no behaviour change. Co-Authored-By: Claude <noreply@anthropic.invalid>
|
@coderabbitai On the outside-diff suggestion for vera/monomorphize.py (~1428-1461, replace rather than merge the handler op registry): verified by EXPERIMENT and skipped — replace-semantics on the discovery side re-creates #1207's exact defect. The decisive shape is an Exn handler nested inside a State one: effect_op_result_names returns nothing for Exn, so under a replace patch discovery answers pick$Int against the rewrite's pick$Nat — E602, main dropped, 'Available exports: pick$Int', the disease this PR exists to close. Both sides MERGE at HEAD and agree (codegen's _translate_handle_state merges; _translate_handle_exn never touches the registry, so an Exn handler must leave the enclosing table answering); for a key the inner handler does supply, ordered merge and replace coincide (inner wins), which is why simpler shapes behave identically either way. Your regression ask was legitimate regardless — under that replace patch the ENTIRE existing suite stayed green, so nothing pinned the semantics. Fixed in 4e9b33d with three cases: the decisive exn-nested-in-state shape (RED under replace), nested distinct State ops (inner owns its body, outer answers outside it), and the user-defined get you named — which loses to the operation inside a handler body but wins at the declared-row site, both directions now pinned, matching codegen's unconditional overwrite. Each verified three-way (checker accepts; discovery and rewrite name one clone; the compiled program returns the checker's value). The invariant is recorded at the merge site. |
Merge gate (
|
|
Tip For best results, initiate chat on the files or code changes.
The required invariant is:
The new regressions in ✏️ Learnings added
You 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 (1)
vera/codegen/core.py (1)
1293-1358: 🎯 Functional Correctness | 🟠 Major | 🏗️ Heavy liftReject collisions with demand-injected prelude ADTs.
A module declaration such as
data Jsonremains accepted. Line 1356 then removesJsonfrom global infrastructure. Later,compile_programskips the injected prelude layout becauseJsonis already inexisting_adtsat Lines 1523-1525 and 1572-1574. The entry namespace can therefore lose PreludeJson, while the checker still exposes it throughTypeEnv.Reserve all demand-injected prelude ADT names before module registration, or emit the existing collision diagnostic for such declarations. Add a regression that imports a module declaring
Jsonwhile the entry program uses PreludeJson.🤖 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/codegen/core.py` around lines 1293 - 1358, Reject module declarations that collide with demand-injected prelude ADTs such as Json, HtmlNode, Request, and Response before registration, using the existing collision diagnostic path. Update the module-registration/prelude handling so these names remain reserved and compile_program cannot skip their injected layouts via existing_adts. Add a regression covering an imported module declaring Json while the entry program uses Prelude Json.
🤖 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 `@vera/codegen/core.py`:
- Around line 1293-1358: Reject module declarations that collide with
demand-injected prelude ADTs such as Json, HtmlNode, Request, and Response
before registration, using the existing collision diagnostic path. Update the
module-registration/prelude handling so these names remain reserved and
compile_program cannot skip their injected layouts via existing_adts. Add a
regression covering an imported module declaring Json while the entry program
uses Prelude Json.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: 54c375d3-10e4-4a99-89a9-14d281788144
⛔ Files ignored due to path filters (1)
docs/llms-full.txtis excluded by!docs/**
📒 Files selected for processing (9)
FAQ.mdREADME.mdROADMAP.mdTESTING.mdtests/test_adt_membership_scope_1253.pytests/test_mono_effect_op_naming_1207.pyvera/README.mdvera/codegen/core.pyvera/monomorphize.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
|
@coderabbitai On the outside-diff suggestion to reserve the demand-injected prelude ADT names (vera/codegen/core.py ~1293-1358): verified and SKIPPED — the reservation would directly reverse ratified spec text. Spec §8.4.1's final sentence (restated in merged PR #1254 and left intact by the #1260 ruling): the prelude's data types 'are ordinary public declarations a program names, and shadows, like any other' — and the reserved namespace is the Vera prefix alone (E154). Within-namespace shadowing works today exactly as that sentence describes (a module declaring and using its own data Json checks, compiles, and runs, measured). Your precise collision scenario — an imported module declaring Json while the entry uses prelude Json — was also measured, and it already fails LOUDLY today: check-clean, then E602 inside the prelude's own json_get with an E620 cascade and zero exports, byte-identical at the branch base and both prior heads, so there is no silent-wrongness forcing a rejection rail; what's wrong there is diagnostic quality (the error points into the prelude rather than at the user's declaration). The genuine latent behind your finding — the cross-namespace member-set subtraction, inert at emission — is now tracked as #1277 with the full measurement, the fix direction (per-namespace subtraction or a complete Pass-0.5 snapshot, not reservation), and the diagnostic-quality case recorded on the same issue. No commit; the branch stands at 4e9b33d. |
|
Tip For best results, initiate chat on the files or code changes.
Vera Specification §8.4.1 permits a program to name and shadow prelude data types. Reserving demand-injected names such as The measured cross-namespace collision fails loudly with E602 and E620. It does not justify a rejection rail that changes valid shadowing semantics. The remaining member-set subtraction issue is separate from name reservation. ✏️ Learnings added
You are interacting with an AI system. |
Rebased onto 9d83df1 (PR #1272). Only doc and count files conflicted; vera/codegen/functions.py and vera/wasm/calls_handlers.py — the two sources both PRs touch — auto-merged, and the boundary suite, the cross-module parity test and the nat-guard suite all stay green, so the _boundary_base consumers and the CellNames threading survive C1's monomorphization and routing work intact. Conflict resolutions, all mechanical: CHANGELOG [Unreleased] — union. C1's five bullets and this branch's four, none dropped, none reworded. The last hunk was NOT a union: it carried C1's five plus a STALE copy of this branch's own bullet against the updated copy, so a blind union would have duplicated it; resolved to C1's five plus the updated one, verified single. KNOWN_ISSUES — both sides' row operations applied by ROW ID, never by position. C1 deleted #1207/#1223/#1241/#1243/#1244/#1253 and added #1271/#1274; this branch deleted #1255/#1256/#1269 and adds #1276. Verified by set comparison over the whole file: every deletion absent, every addition present, no duplicates. Count-bearing prose — structure from upstream (it carries C1's 207 conformance programs and 157 test files), every NUMBER re-derived by scripts/check_doc_counts.py against the merged tree rather than merged from either side: 10,138 tests across 157 files, 9,980 passed + 26 stress + 132 skipped. docs/* — regenerated by build_site.py, never hand-merged. Content integrity: the diff over vera/ and tests/ (excluding the count-bearing vera/README.md paragraph) is identical before and after the rebase, modulo hunk offsets. Full manual gate re-run, hooks not having fired on rebase --continue: pytest 9,980 passed / 132 skipped, mypy clean, ruff and ruff --select S clean, 207 conformance, 42 examples, 255 corpus programs canonical, doc counts consistent, site assets coherent, diagnostic fields, limitations sync and explicit encoding all OK. Skip-changelog: rebase conflict resolution over count-bearing prose; no behaviour change Co-Authored-By: Claude <noreply@anthropic.invalid>
1 participant
Part of the #1213 burndown (PR C1) — the module-routing cluster. Six commits plus the rebase resolution.
What this fixes
#1207 — one effect-op result table (
3718b817). Monomorphization discovery and the WASM rewrite previously derived an effect-op's result type independently and disagreed on aget(())array element driving a generic instantiation (pick$Natvspick$Int— a dangling call target, loud E602 drop).vera.slots.effect_op_result_namesis now the single derivation; codegen's declared-effect-row registry,_translate_handle_state, and discovery's new scoped walk all read it. Scope is mirrored, not approximated: ahandleinstalls its table over its body only (init and clause bodies stay in the enclosing context, per #1211's rule), and a declared-row op is never injected where a user function owns the name.#1223 — generic-under-generic helpers instantiate their own callees (
58dc60e0). The #1002 machinery instantiated the nested helper but never walked the helper's own callees, so a top-level generic called from inside the helper body went unregistered — E602 skip, E620 cascade, zero exports from check-clean verify-clean source. Hoisting and the top-level worklist are now a fixpoint over one shared leaf (collect_generic_helper_instances) that the verifier drives too; that same review surfaced and fixed the sibling case in the growing body set.#1241 + #1243 — clone bodies route through the declaring module, both halves atomically (
32f02c12). An imported generic's clone resolved its bare body calls through the IMPORTER's registries — running the importer's same-named private function (999 where the declaring module's returns 111), with type-discriminating shapes emitting invalid WASM from check-green source. The verifier's_declaring_module_scopenow carries the module's function registry beside env/source/file, and codegen's clone-emission path threads_module_intra_renamesthe way Passes 2.5/2.6 already do. The pairing constraint is measured, not asserted: with the codegen half stashed,vera verifyreports clean and the run raises the postcondition violation — so every test asserts the verify verdict AND the runtime value in one test against a standalone-module oracle, making it impossible for either half to pass alone. This closes the private / non-generic dimension only: the same routing question for an imported public generic whose name the importer also declares is a distinct hole in the clone-name space — both modules'gen2mangle togen2$Booland one overwrites the other — tracked as #1274, pre-existing and byte-identical atef7c04c0.#1244 — every module's bodies check under its own import filter (
03adbe6d). Import visibility was entry-point-dependent (E200 warn when checked directly, silence when reached as an import). Measured blast radius before implementing: ZERO — 7 corpus programs import a non-stdlib module, none of whose modules carries a standalone diagnostic. One existing expectation moved, toward strictness: the module-builtin-effect redeclaration fixture now expects exactly its standalone verdict. The change also removed a duplicate error-surfacing path (codegen-only, errors-only) in favor of one collection with the memo threaded.#1253 — codegen's ADT membership is scoped (
b711e2e9). Membership now derives from the owning namespace plus the module's own imports, public and in-filter — closing both the issue's measurement (['Array<?>', 'Array<Int>']vs['Array<Float>', 'Array<Int>']) and the private-sibling visibility dimension appended from PR #1254's review.Rebase provenance
Rebased onto
ef7c04c0(post-C5) with the resolution as the visible final commit. Content integrity: diff-of-diffs oververa/ tests/ spec/identical modulo hunk offsets across all 24 code files. The C5 interaction was probed with a purpose-built fixture (an importedforall<T>throwing a provably-negative payload, so #1268's new obligation lands inside a clone verified under this PR's pinned registries): identical verdicts on both trees, both variants. That probe surfaced a pre-existing C5 residual (the throw obligation does not survive monomorphization), recorded on #1268 — not this PR's.Adjacent defect, filed not fixed
#1271: discovery inside a still-generic scope binds a callee's type variable to the enclosing variable's name, emitting a spurious
pick$Uclone that is loudly E604-skipped on every generic-under-generic program — the reason #1223's shapes live in pytest rather than conformance. Suppressing it changes the shared discovery walk with its own blast radius; queued separately.Gates
pytest 9,917 passed / 132 skipped / 26 deselected (10,075 collected, oracle-matched); mypy clean; ruff +
--select Sclean; conformance 207/207; examples 42/42; corpus canonical 255/255; doc counts, site assets, diagnostic fields, limitations sync (45 rows), e602-clean, explicit encoding all green. Every commit passed the full 33-hook pre-commit gate; the rebased tree re-gated by hand end to end.Closes #1207.
Closes #1223.
Closes #1241.
Closes #1243.
Closes #1244.
Closes #1253.
(Keywords take effect at the release PR.)
Summary by CodeRabbit
Bug Fixes
throwpayloads and literals against refinements.Tests
Documentation