Chapter 8 module conformance + fix module-qualified-call soundness bug (#679, #814)#816
Conversation
…arness + module E-codes The last spec chapter without chNN_*.vera coverage now has eight programs, one per section: module_decl (8.2), import_wildcard (8.3.1), import_selective (8.3.2), visibility_public (8.4), visibility_private (8.4, negative), shadowing (8.5.2), module_qualified_call (8.5.3), circular_import (8.6.3, negative). Companions reuse tests/conformance/vera/math.vera (extended with a private helper) plus a cycle pair. The issue assumed two substrates that did not exist; both are added here: - Module-resolution diagnostics now carry stable E-codes (the every-diagnostic- has-a-code invariant from DESIGN.md): E011 circular import, E012 cannot resolve import, E013 error parsing an imported module (resolver.py), and E150 cannot import a private declaration (checker/modules.py). - Negative-test support in the conformance harness: a manifest entry may declare `expected_error: <code>`, and check_conformance.py / test_conformance.py then assert the program FAILS check with that code (E011 / E150) instead of passing. Writing the programs surfaced two pre-existing module name-resolution bugs, filed as #814 (out of this coverage PR's scope): module-qualified calls do not bypass a local shadow at codegen, and the verifier and codegen disagree on bare-call shadowing. The shadowing and qualified-call programs are written to the correctly-implemented spec surface and avoid those paths. Conformance 93 -> 101. Release prep for v0.0.184. Closes #679. Co-Authored-By: Claude <[email protected]>
Per spec §8.5.3 a qualified call `m::f` resolves to the module's function even when a local `f` shadows the bare name. Codegen desugared ModuleCall to a bare FnCall, dropping the module path, so `m::f` invoked the shadowing local — while the verifier resolved it correctly via its per-module registry. An unsound verifier<->runtime desync: `vera verify` proved a postcondition against the module's contract that the runtime then violated. Shadowed module functions are now emitted under a distinct, collision-free `mod$...` WASM name (`$` is illegal in Vera identifiers, like the monomorphizer's `name$T`); a (module path, name) -> target table routes qualified calls to it, while bare calls still resolve to the local (§8.5.2, unchanged). A bare intra-module call inside a qualified-reached `mod$` body is likewise redirected to the module's sibling (the C2 residual the verifier<->codegen review found). Generic (`forall`) module fns are excluded (cross-module generic monomorphisation is separately unimplemented, #774). Investigating corrected the #814 diagnosis: the reported bare-call "Bug B" does not exist (§8.5.2 works for non-builtin names); the `abs` symptom was the verifier modelling the built-in by name, filed separately as #815. Tests: sharpened ch08_module_qualified_call + ch08_shadowing, a codegen run-value test, an intra-module-sibling (C2) test, a wildcard/coexistence test, a §8.5.2 verifier regression test, and a verifier<->codegen differential. Conformance 101, full suite green, mypy + ruff clean. Closes #814. Co-Authored-By: Claude <[email protected]>
|
Note Reviews pausedIt looks like this branch is under active development. To avoid overwhelming you with review comments due to an influx of new commits, CodeRabbit has automatically paused this review. You can configure this behavior by changing the Use the following commands to manage reviews:
Use the checkboxes below for quick actions:
📝 WalkthroughWalkthroughAdds Chapter 8 conformance programs, negative-test harness support, stable module diagnostics, and module-qualified call codegen and verifier coverage for shadowing. Version, release, and project documentation counts are updated accordingly. ChangesChapter 8 conformance and stable diagnostics
Module-qualified call codegen under local shadowing
Estimated code review effort🎯 4 (Complex) | ⏱️ ~60 minutes Suggested labels
🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✨ Finishing Touches🧪 Generate unit tests (beta)
Comment |
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #816 +/- ##
==========================================
+ Coverage 92.04% 92.06% +0.01%
==========================================
Files 89 89
Lines 26934 27020 +86
Branches 321 321
==========================================
+ Hits 24791 24875 +84
- Misses 2135 2137 +2
Partials 8 8
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: 3
🤖 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 `@TESTING.md`:
- Around line 9-11: The conformance counts in TESTING.md are stale and
internally inconsistent with tests/test_conformance.py. Update every remaining
summary in the conformance section, including the “93 small, focused programs”
wording, the old four check-level program list, and the total skip count, so
they match the current 6 check-level and 8 verify-level entries and the implied
20 skips. Make sure all related occurrences in the file are changed together so
the section is factually consistent end to end.
In `@tests/test_resolver.py`:
- Around line 459-486: These resolver tests are still filtering diagnostics by
description text instead of validating the stable error_code contract. Update
the assertions in the test methods around the _errors helper to check the
returned codes directly for the relevant fixtures, and avoid relying on
substrings like “Circular import”, “Cannot resolve import”, or “Error parsing
imported module”. Keep the existing E011, E012, and E013 expectations tied to
the corresponding test cases so the checks remain resilient to wording changes
in vera/resolver.py.
In `@vera/codegen/modules.py`:
- Around line 214-223: The mangled module-target path in modules.py is only
copying _fn_sigs, but _translate_call() also depends on _fn_nat_params for the
rewritten target. Update the shadowed-module handling around
_module_qualified_wasm_name and _module_intra_renames to also propagate the bare
function’s _fn_nat_params entry to the mangled name, so intra-module calls still
get the `@Int` -> `@Nat` runtime guard.
🪄 Autofix (Beta)
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
Run ID: 4999e269-dee3-4cf2-9259-836ee382a3c2
⛔ Files ignored due to path filters (16)
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/ch08_circular_import.verais excluded by!**/*.veratests/conformance/ch08_import_selective.verais excluded by!**/*.veratests/conformance/ch08_import_wildcard.verais excluded by!**/*.veratests/conformance/ch08_module_decl.verais excluded by!**/*.veratests/conformance/ch08_module_qualified_call.verais excluded by!**/*.veratests/conformance/ch08_shadowing.verais excluded by!**/*.veratests/conformance/ch08_visibility_private.verais excluded by!**/*.veratests/conformance/ch08_visibility_public.verais excluded by!**/*.veratests/conformance/vera/cycle_a.verais excluded by!**/*.veratests/conformance/vera/cycle_b.verais excluded by!**/*.veratests/conformance/vera/math.verais excluded by!**/*.verauv.lockis excluded by!**/*.lock,!uv.lock
📒 Files selected for processing (25)
AGENTS.mdCHANGELOG.mdCLAUDE.mdFAQ.mdHISTORY.mdKNOWN_ISSUES.mdREADME.mdROADMAP.mdTESTING.mdpyproject.tomlscripts/check_conformance.pytests/conformance/manifest.jsontests/test_codegen_modules.pytests/test_conformance.pytests/test_resolver.pytests/test_verifier.pyvera/__init__.pyvera/checker/modules.pyvera/codegen/core.pyvera/codegen/functions.pyvera/codegen/modules.pyvera/errors.pyvera/resolver.pyvera/wasm/calls.pyvera/wasm/context.py
- TESTING.md: finish the conformance-count sweep the coverage commit left stale — 93 -> 101 programs, the check-level list (now six, incl. the two ch08 negatives), and the skipped-test count 16 -> 20 with the ch08 rows. - test_resolver.py: assert the resolver E-codes (E011/E012/E013) directly instead of filtering diagnostics by description substring, so a wording tweak in resolver.py can't make the tests brittle. - codegen/modules.py: mirror the @Nat-parameter guard bitmap onto the mangled mod$ name, so a qualified call to a shadowed module fn with a @nat parameter still emits the call-site narrowing guard. Refs #814, #679. Co-Authored-By: Claude <[email protected]>
There was a problem hiding this comment.
Actionable comments posted: 2
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
vera/codegen/modules.py (1)
198-203: 🎯 Functional Correctness | 🟠 Major | ⚡ Quick winSkip
foralldeclarations before queuing imported bodies.Line 198 queues the imported declaration, and Lines 199-201 queue its where-functions, before Line 202 excludes generics. That means cross-module generic declarations still enter
_imported_fn_decls, despite this block documenting them as unimplemented and excluded. Move the guard before the append.Proposed fix
- self._imported_fn_decls.append(tld.decl) - if tld.decl.where_fns: - for wfn in tld.decl.where_fns: - self._imported_fn_decls.append(wfn) if tld.decl.forall_vars: continue + self._imported_fn_decls.append(tld.decl) + if tld.decl.where_fns: + for wfn in tld.decl.where_fns: + self._imported_fn_decls.append(wfn)🤖 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/modules.py` around lines 198 - 203, The imported-declaration queue in the module import path is adding generic `forall` declarations before they are filtered, so cross-module generics still get stored in `_imported_fn_decls`. Update the logic in the import handling block around `tld.decl`, `where_fns`, and `forall_vars` so the `forall` guard runs first, and only append the declaration and any `where_fns` when the declaration is not generic.
🤖 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 `@TESTING.md`:
- Line 107: Update the conformance-suite description in TESTING.md to remove the
stale “imports nothing” statement, since the suite now includes import/module
cases added in Chapter 8. Revise the sentence near the conformance suite
overview so it still accurately describes `tests/conformance/` while keeping the
special case for `ch07_cross_module_contracts.vera` and its library fixture.
- Line 134: Update the TESTING.md program classification so the negative-test
attribution is correct: in the section describing check-level programs, make
clear that ch08_circular_import and ch08_visibility_private are the two
expected_error negative tests, and that ch09_http and ch09_inference are only
environment-gated check-level programs. Keep the rest of the run/check/verify
breakdown consistent with the existing program names in this paragraph.
---
Outside diff comments:
In `@vera/codegen/modules.py`:
- Around line 198-203: The imported-declaration queue in the module import path
is adding generic `forall` declarations before they are filtered, so
cross-module generics still get stored in `_imported_fn_decls`. Update the logic
in the import handling block around `tld.decl`, `where_fns`, and `forall_vars`
so the `forall` guard runs first, and only append the declaration and any
`where_fns` when the declaration is not generic.
🪄 Autofix (Beta)
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
Run ID: 8b8a352e-cad9-4fe2-a8e7-e2258cdf031a
📒 Files selected for processing (3)
TESTING.mdtests/test_resolver.pyvera/codegen/modules.py
- TESTING.md: drop the stale "imports nothing" claim (the Chapter 8 cases use `import`); fix the negative-test attribution — the expected_error negatives are ch08_circular_import / ch08_visibility_private, while the ch09_http / ch09_inference check-level programs are environment-gated. - codegen/modules.py: move the `forall` guard before the imported-decl append so a generic never enters `_imported_fn_decls` (matches the "excluded throughout" comment and avoids queuing an uncompilable generic template for Pass 2.5; cross-module generics remain #774). Refs #814, #679. Co-Authored-By: Claude <[email protected]>
|
@coderabbitai Addressed the outside-diff finding ( |
|
Tip For best results, initiate chat on the files or code changes.
✏️ Learnings added
|
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/modules.py (1)
223-225: 🎯 Functional Correctness | 🟠 Major | 🏗️ Heavy liftApply module renames to Pass 2.5 imports too.
_module_intra_renamesis only passed when Pass 2.6 emitsmod$…bodies, but non-shadowed imported functions are still compiled in Pass 2.5 without that map. Ifm.g()calls sibling/helperm.f()and the importing module defines localf, the emitted baregbody can call the localfinstead of the module one. Carry the module path with_imported_fn_declsand compile Pass 2.5 entries withself._module_intra_renames.get(path, {})as well, including shadowedwhere_fns.As per path instructions,
vera/**/*.pyis compiler source and should be reviewed for correctness, type safety, and consistency with existing patterns.🤖 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/modules.py` around lines 223 - 225, Pass 2.5 imported function compilation is missing the module rename map, so bare bodies can resolve sibling calls to local shadowed names instead of module-scoped ones. Update `_imported_fn_decls` to carry the originating module path and, in `modules.py`, have the Pass 2.5 emit path compile with `self._module_intra_renames.get(path, {})` just like Pass 2.6 does for `mod$…` bodies. Also make sure shadowed `where_fns` use the same module-specific rename lookup so imported functions consistently pick the module’s `f` over any local `f`.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.
Outside diff comments:
In `@vera/codegen/modules.py`:
- Around line 223-225: Pass 2.5 imported function compilation is missing the
module rename map, so bare bodies can resolve sibling calls to local shadowed
names instead of module-scoped ones. Update `_imported_fn_decls` to carry the
originating module path and, in `modules.py`, have the Pass 2.5 emit path
compile with `self._module_intra_renames.get(path, {})` just like Pass 2.6 does
for `mod$…` bodies. Also make sure shadowed `where_fns` use the same
module-specific rename lookup so imported functions consistently pick the
module’s `f` over any local `f`.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: d9d80d32-1e7d-4410-b725-f6450a5618e0
📒 Files selected for processing (2)
TESTING.mdvera/codegen/modules.py
…ror) A NON-shadowed imported function compiled in Pass 2.5 calls its siblings by bare name; when a sibling is shadowed by a local, that call resolved to the local shadow instead of the module's version (verify OK, run traps) — the mirror of the C2 residual already fixed for the mod$ (Pass 2.6) bodies. _imported_fn_decls now carries the originating module path, and Pass 2.5 compiles each imported body (and its where-fns) with that module's _module_intra_renames map, so a bare sibling call reaches the module's version. Regression test added: a non-shadowed imported `outer` whose body calls a locally-shadowed `inner` returns the module's 100, not the local 7. Refs #814, #679. Co-Authored-By: Claude <[email protected]>
|
@coderabbitai Fixed the Pass 2.5 outside-diff finding in 2175e58 — |
|
Tip For best results, initiate chat on the files or code changes.
Carrying the originating module path with The reproduced failure mode and the regression test ✏️ Learnings added
|
There was a problem hiding this comment.
Actionable comments posted: 1
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
vera/codegen/modules.py (1)
222-231: 🎯 Functional Correctness | 🟠 Major | ⚡ Quick winMirror
_fn_ret_type_exprsfor mangled module targets.The mangled target gets
_fn_sigsand_fn_nat_params, but not the full Vera return-type expression. Qualified calls to a shadowed module function that returnsString/Array<T>can then miss the return-shape inference paths used by indexing/interpolation once the call target resolves tomod$....Proposed fix
self._fn_sigs.setdefault(mangled, mangled_sig) +self._fn_ret_type_exprs.setdefault( + mangled, temp._fn_ret_type_exprs[fn_name], +) self._shadowed_module_fns.append((mod.path, mangled, tld.decl))🤖 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/modules.py` around lines 222 - 231, The mangled module target is already mirrored in _fn_sigs and _fn_nat_params, but _fn_ret_type_exprs is missing, so qualified calls resolving through a mangled name lose return-shape inference. Update the mangling path in modules.py where the shadowed module function is recorded to also copy the original entry from temp._fn_ret_type_exprs onto the mangled symbol, alongside the existing _fn_sigs and _fn_nat_params handling.
🤖 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 `@vera/codegen/modules.py`:
- Around line 204-207: The imported where-function declarations are only being
appended, but they are not going through the same shadow/mangle registration as
the parent declaration, so local names can still shadow imported helpers during
Pass 2.5. Refactor the append plus shadow-registration logic in modules.py into
a helper and invoke it for both tld.decl and each non-generic tld.decl.where_fns
entry; ensure helper functions still populate _shadowed_module_fns and
_module_intra_renames, while only top-level public/in-filter declarations update
_module_qualified_targets.
---
Outside diff comments:
In `@vera/codegen/modules.py`:
- Around line 222-231: The mangled module target is already mirrored in _fn_sigs
and _fn_nat_params, but _fn_ret_type_exprs is missing, so qualified calls
resolving through a mangled name lose return-shape inference. Update the
mangling path in modules.py where the shadowed module function is recorded to
also copy the original entry from temp._fn_ret_type_exprs onto the mangled
symbol, alongside the existing _fn_sigs and _fn_nat_params handling.
🪄 Autofix (Beta)
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
Run ID: 4f5be30c-2f38-40ba-8ea1-9af99a2c1d72
📒 Files selected for processing (5)
ROADMAP.mdTESTING.mdtests/test_codegen_modules.pyvera/codegen/core.pyvera/codegen/modules.py
Two further mirrors of the C2 shadow-resolution class, from CR's re-review: - Imported `where`-fns were appended to the Pass 2.5 list but did NOT go through the shadow registration (only the parent decl did), so an imported `outer`'s call to a locally-shadowed `where` helper resolved to the local shadow (verify OK, run traps). Factored the registration into `_register_shadowed_import` and apply it to the parent decl AND each non-generic where-fn (where-fns are private, never qualified-callable, so no `_module_qualified_targets` entry). Reproduced first; regression test added. - The mangled module target mirrored `_fn_sigs` + `_fn_nat_params` but not `_fn_ret_type_exprs`, so a qualified / intra-module call to a shadowed module fn returning `String` / `Array<T>` would lose index / interpolation element-type inference. Mirror it alongside the other side-tables. Refs #814, #679. Co-Authored-By: Claude <[email protected]>
|
@coderabbitai Addressed the |
|
Tip For best results, initiate chat on the files or code changes.
Mirroring Given your note that the side-table entry was genuinely missing and that the failure mode is an inference fallback rather than a soundness/runtime failure, I agree a dedicated regression test is optional here. ✏️ Learnings added
|
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)
vera/codegen/modules.py (1)
53-60: 🎯 Functional Correctness | 🟠 Major | ⚡ Quick winTreat local
wherefunctions as shadows too.
local_fn_namesonly includes top-level local functions, but localwherehelpers are also emitted into the flat WAT namespace. If an importer has a localwhere helperand importedoutercalls the module’swhere helper, this path will not mangle/register the imported helper, so Pass 2.5 can emit or resolve$helperunder the wrong/local name. Recursively collect localwhere_fnsas shadows, and ensure the bare-name Pass 2.5 skip uses the same set.Suggested direction
- local_fn_names: set[str] = { - tld.decl.name for tld in program.declarations - if isinstance(tld.decl, ast.FnDecl) - } + local_fn_names: set[str] = set() + + def collect_local_fn_names(decl: ast.FnDecl) -> None: + local_fn_names.add(decl.name) + for wfn in decl.where_fns or (): + collect_local_fn_names(wfn) + + for tld in program.declarations: + if isinstance(tld.decl, ast.FnDecl): + collect_local_fn_names(tld.decl)Also thread this same set into the Pass 2.5 bare-name skip, otherwise the imported helper can still be emitted as
$helper.Also applies to: 221-228
🤖 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/modules.py` around lines 53 - 60, Treat local where functions as shadows in the same way as top-level local functions: update the local_fn_names collection in vera/codegen/modules.py to recursively include names from where_fns (and any nested where helpers) so they are recognized as locally shadowing the importer’s namespace. Then make sure the Pass 2.5 bare-name skip uses that same shadow set wherever the imported helper is registered/emitted, so a bare $helper is not generated or resolved under the wrong name while m::helper still points to the module body.TESTING.md (1)
530-530: 📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick winUpdate the conformance-count row in Validation Scripts.
check_conformance.pynow validates 101 conformance programs, so this row is stale at 93 and no longer matches the manifest-driven count.Proposed fix
-| `check_conformance.py` | All 93 conformance programs pass their declared level (parse/check/verify/run) | +| `check_conformance.py` | All 101 conformance programs pass their declared level (parse/check/verify/run) |🤖 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 `@TESTING.md` at line 530, The conformance-count row in the Validation Scripts section is stale and should reflect the current manifest-driven total. Update the `check_conformance.py` entry in `TESTING.md` so it reports 101 conformance programs instead of 93, keeping the declared level description unchanged.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.
Outside diff comments:
In `@TESTING.md`:
- Line 530: The conformance-count row in the Validation Scripts section is stale
and should reflect the current manifest-driven total. Update the
`check_conformance.py` entry in `TESTING.md` so it reports 101 conformance
programs instead of 93, keeping the declared level description unchanged.
In `@vera/codegen/modules.py`:
- Around line 53-60: Treat local where functions as shadows in the same way as
top-level local functions: update the local_fn_names collection in
vera/codegen/modules.py to recursively include names from where_fns (and any
nested where helpers) so they are recognized as locally shadowing the importer’s
namespace. Then make sure the Pass 2.5 bare-name skip uses that same shadow set
wherever the imported helper is registered/emitted, so a bare $helper is not
generated or resolved under the wrong name while m::helper still points to the
module body.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: 733d0e05-50ff-4c81-853f-82e6774e97fb
📒 Files selected for processing (4)
ROADMAP.mdTESTING.mdtests/test_codegen_modules.pyvera/codegen/modules.py
…ounts - codegen: a LOCAL `where`-fn shadowing an imported name produced a duplicate bare `$name` WASM function — the imported body was emitted bare because `local_fn_names` collected only top-level names, so wasmtime rejected the module (check OK / verify OK / run fails on invalid WASM). `_collect_local_fn_names` now gathers names recursively (top-level + where-fn helpers, nested), and Pass 2.5 skips emitting an imported fn under a bare name shadowed by ANY local (top-level or where-fn) — it is reached via its `mod$…` emission instead. Reproduced first; regression test added. - TESTING.md: the Validation Scripts and CI-gate tables still said "93 conformance programs"; updated both to 101. Refs #814, #679. Co-Authored-By: Claude <[email protected]>
|
@coderabbitai Both outside-diff findings fixed in 04823cb:
|
|
Tip For best results, initiate chat on the files or code changes.
The reproduced failure mode plus ✏️ Learnings added
|
|
@coderabbitai resume |
✅ Action performedReviews resumed. |
|
@coderabbitai full review |
✅ Action performedFull review finished. |
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)
tests/test_codegen_modules.py (1)
356-365: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winAssert the type-check result before verifying.
typecheck(...)is currently called only for side effects, so a check-stage module-resolution regression could be missed whileverify(...)still runs.Proposed fix
- typecheck(prog, main_src, resolved_modules=[mod]) + check_result = typecheck(prog, main_src, resolved_modules=[mod]) + check_errors = [ + d for d in check_result.diagnostics + if d.severity == "error" + ] + assert check_errors == [], [e.description for e in check_errors] vres = verify(prog, main_src, resolved_modules=[mod])As per path instructions,
tests/**/*.pyshould flag actual bugs in test logic and missing edge cases for new compiler features.🤖 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_codegen_modules.py` around lines 356 - 365, The test in the `typecheck`/`verify` flow is only invoking `typecheck(...)` for side effects, so a module-resolution regression could slip through unnoticed. Update the test to explicitly assert the `typecheck` result before calling `verify(...)`, using the existing `prog`, `main_src`, and `resolved_modules` setup, so failures in the check stage are caught independently of verification.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.
Outside diff comments:
In `@tests/test_codegen_modules.py`:
- Around line 356-365: The test in the `typecheck`/`verify` flow is only
invoking `typecheck(...)` for side effects, so a module-resolution regression
could slip through unnoticed. Update the test to explicitly assert the
`typecheck` result before calling `verify(...)`, using the existing `prog`,
`main_src`, and `resolved_modules` setup, so failures in the check stage are
caught independently of verification.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: ee929be7-c2de-4c9d-9ad5-cc908465f0a5
📒 Files selected for processing (5)
ROADMAP.mdTESTING.mdtests/test_codegen_modules.pyvera/codegen/core.pyvera/codegen/modules.py
CodeRabbit re-review: the differential test called typecheck() only for side effects, so a check-stage module-resolution regression could slip through while verify() still ran. Capture and assert the typecheck diagnostics (typecheck returns the diagnostics list directly, not a result object) before verifying — so the differential now pins all three stages. Refs #814, #679. Co-Authored-By: Claude <[email protected]>
…ce rules Round-8 reworded the conformance *description* lines but missed the gate-rule lines that also say "must pass their declared level", which is inaccurate now that negative fixtures (expected_error) must FAIL check. Updated all three — CLAUDE.md "What not to break", AGENTS.md command comment, and AGENTS.md rule — to distinguish positive entries (pass their level) from the negative fixtures (fail check with their expected_error E-code). Regenerated docs/llms-full.txt (bundles AGENTS.md) via build_site.py. Refs #814, #679. Co-Authored-By: Claude <[email protected]>
|
@coderabbitai Fixed in 8d39116 — reworded the remaining "must pass" conformance rules (CLAUDE.md "What not to break", AGENTS.md command comment + rule) to distinguish positive entries (pass their declared level) from the negative fixtures |
|
Tip For best results, initiate chat on the files or code changes.
Rewording the
is the right fix. Your note about the earlier pass only updating the descriptive prose, not the normative “must pass” rules, also explains why this kept resurfacing. ✏️ Learnings added
|
CodeRabbit re-review: the E150 "cannot import a private declaration" diagnostic (checker/modules.py — both the fn and data import paths) cited 'Chapter 5, Section 5.8 "Function Visibility"', a section that does not exist (Chapter 5 has no §5.8) and the wrong concept. E150 fires in the import-resolution path, so it now points to the module-system rule, 'Chapter 8, Section 8.4 "Visibility"', keeping the message / rationale / fix unchanged. Refs #814, #679. Co-Authored-By: Claude <[email protected]>
|
@coderabbitai Fixed the outside-diff finding in cd6a0d6 — E150 ("cannot import a private declaration") now cites |
|
@coderabbitai full review |
✅ Action performedFull review finished. |
|
Tip For best results, initiate chat on the files or code changes.
Updating E150 to cite ✏️ Learnings added
|
There was a problem hiding this comment.
♻️ Duplicate comments (1)
TESTING.md (1)
530-530: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winAlign the hook wording with
expected_errorsemantics.Line 530 and Line 630 still say
check_conformance.pymakes all 101 conformance programmes “pass” their declared level. That is imprecise for the Chapter 8 negatives: those entries are successful whencheckfails with the declared E-code.♻️ Suggested fix
-| `check_conformance.py` | All 101 conformance programs pass their declared level (parse/check/verify/run) | +| `check_conformance.py` | All 101 conformance entries satisfy their declared outcome (parse/check/verify/run) | -| `check_conformance.py` | All 101 conformance programs pass their declared level | +| `check_conformance.py` | All 101 conformance entries satisfy their declared outcome |Also applies to: 630-630
🤖 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 `@TESTING.md` at line 530, The wording for `check_conformance.py` is too broad for the Chapter 8 negative cases, since success there means `check` fails with the declared `expected_error` rather than “passing” the level. Update the hook description text in `TESTING.md` for the affected `check_conformance.py` entries so it explicitly reflects `expected_error` semantics, keeping the wording accurate for both normal conformance programs and negative error-expected cases.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.
Duplicate comments:
In `@TESTING.md`:
- Line 530: The wording for `check_conformance.py` is too broad for the Chapter
8 negative cases, since success there means `check` fails with the declared
`expected_error` rather than “passing” the level. Update the hook description
text in `TESTING.md` for the affected `check_conformance.py` entries so it
explicitly reflects `expected_error` semantics, keeping the wording accurate for
both normal conformance programs and negative error-expected cases.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro
Run ID: cfbe6a63-a68c-45f6-8c48-611ed0ba483a
⛔ Files ignored due to path filters (1)
docs/llms-full.txtis excluded by!docs/**
📒 Files selected for processing (8)
AGENTS.mdCLAUDE.mdREADME.mdROADMAP.mdTESTING.mdtests/test_codegen_modules.pyvera/checker/modules.pyvera/wasm/context.py
|
@coderabbitai Fixed the TESTING.md duplicate (lines 530 + 630) in cd6a0d6, plus an exhaustive sweep of the same wording class: the Validation-Scripts and CI-gate tables and CONTRIBUTING.md's gate list now read "All 101 conformance entries hold at their declared level — positives pass; negatives fail The two recurring |
|
@coderabbitai full review |
✅ Action performedFull review finished. |
|
Tip For best results, initiate chat on the files or code changes.
The doc sweep sounds complete now: updating the remaining And agreed on the recurring |
…ning tables The exhaustive sweep's last occurrences of the "all conformance programs pass their declared level" wording — TESTING.md's Validation-Scripts (line 530) and CI-gate (line 630) tables, and CONTRIBUTING.md's gate list — predated the negative-test support and didn't distinguish positives (pass) from the `expected_error` negatives (succeed by failing `check` with their E-code). Reworded all three to match the CLAUDE.md / AGENTS.md phrasing. (Round-5 fixed the count 93->101 on the TESTING lines but not the verb.) Refs #814, #679. Co-Authored-By: Claude <[email protected]>
|
Correction to my comment above: the conformance-wording reword (TESTING.md lines 530 + 630 and CONTRIBUTING.md) actually landed in ad5df1f, not |
|
@coderabbitai full review |
✅ Action performedFull review finished. |
…odeRabbit) The resolver's three module-resolution error paths emitted inconsistent field sets: E011 (circular import) lacked fix+spec_ref, E012 (cannot resolve) lacked spec_ref, E013 (parse error) carried only description+error_code. Because Diagnostic.to_dict() omits empty fields, `vera check --json` exposed module-resolution failures with a JSON schema that drifted from every other diagnostic (49 checker sites set spec_ref; the hand-written E001/E007 carry rationale+fix+spec_ref). Added the missing rationale/fix/spec_ref fields, each citing the relevant Chapter 8 section (§8.6.3 circular import detection, §8.6.1 path mapping, §8.6.5 resolution errors), with instructional fix text. Test-first: test_resolver_diagnostics_carry_full_contract asserts all three paths carry rationale+fix+spec_ref and cite Chapter 8; confirmed RED (E011 fix='') before the change, GREEN after. Verified end-to-end via `vera check --json` on the ch08_circular_import fixture. Doc counts: 5333->5334 tests; test_resolver.py 18->19 tests, 486->550 lines. Co-Authored-By: Claude <[email protected]>
|
@coderabbitai Fixed in c3676a5 (resolver.py outside-diff finding — "Complete the resolver diagnostics' JSON contract"). Completed the diagnostic contract for all three module-resolution error paths: E011 (circular import) now carries |
|
Tip For best results, initiate chat on the files or code changes.
Completing the resolver-side diagnostic contract in
Given that ✏️ Learnings added
|
…resolver except (review-toolkit) Our pr-review-toolkit review of #816 surfaced two untested codegen paths and one over-broad except. All three addressed test-first, each mutation-validated (RED before the fix, GREEN after): 1. i32_pair ModuleCall drop (vera/wasm/context.py): a String/Array- returning module-qualified call in statement position must drop BOTH i32 stack values. The branch was untested; mutating it yields invalid WASM ("values remaining on stack"). Added test_pair_returning_qualified_call_in_statement_position, using a local where-shadow so the mod$ mangled-target path is exercised. 2. @Nat-param guard mirror (vera/codegen/modules.py): the call-site value>=0 narrowing guard must be mirrored onto a shadowed module fn's mod$ target. Untested; dropping the mirror passes a negative value unguarded (verified: m::f(0 - 1) returns -1 with no trap). Added test_nat_param_guard_mirrored_on_shadowed_qualified_call (traps with the mirror, runs unsound without). 3. resolver.py except narrowing: a blanket `except Exception` relabeled any internal compiler bug (e.g. an AttributeError in transform) as E013 "Error parsing imported module", blaming the user's file. Narrowed to (ParseError, TransformError, OSError, UnicodeDecodeError) so real bugs propagate as crashes. Added test_internal_error_not_masked_as_E013 (RED before: "DID NOT RAISE"). Doc counts: 5334->5337 tests; test_codegen_modules 31->33 / 1077->1151 lines, test_resolver 19->20 / 550->585 lines. Co-Authored-By: Claude <[email protected]>
…4 (review follow-up)
The E232 diagnostic (calling a private function via a module-qualified
call `m::f`) and the missing-visibility error both cited 'Chapter 5,
Section 5.8 "Function Visibility"', which no longer exists — module
visibility rules live in spec/08-modules.md §8.4. This matches the E150
(private import) correction already in this PR; E232 is its
qualified-call sibling, and §8.4 line 81 ("Every top-level fn/data must
have an explicit visibility modifier; omitting is a compile error")
covers the missing-visibility error too.
Repointed both sites (vera/checker/calls.py, vera/checker/registration.py)
to 'Chapter 8, Section 8.4 "Visibility"'. Strengthened the existing E232
and missing-visibility tests to assert the spec_ref (the E232 test was
confirmed RED on §5.8 first, GREEN after). No new tests; test_checker.py
line count 6455->6467.
Co-Authored-By: Claude <[email protected]>
There was a problem hiding this comment.
Actionable comments posted: 1
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
vera/resolver.py (1)
103-125: 🗄️ Data Integrity & Integration | 🟠 Major | ⚡ Quick winPopulate the full diagnostic payload for resolver errors.
These three paths still build
Diagnostic(...)with only line/column, soDiagnostic.to_dict()will omitlocation.fileandsource_line.vera check --jsontherefore emits a different schema for E011/E012/E013 than the rest of the compiler, which breaks the documented machine-consumer contract this PR is standardising. Please thread the importing file and offending import line into these diagnostics instead of emitting bare records. As per path instructions, everyDiagnosticshould includedescription,location,source_line,rationale,fix,spec_refand a stableerror_code.Also applies to: 133-155, 192-214
🤖 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/resolver.py` around lines 103 - 125, Populate the full Diagnostic payload in resolver errors so E011/E012/E013 match the standard JSON schema. In the resolver paths that build Diagnostic instances for circular import and related checks, thread through the importing file and offending import line so Diagnostic.to_dict() can include location.file and source_line, not just line/column. Update the relevant diagnostic construction sites in resolver.py to always set description, location, source_line, rationale, fix, spec_ref, and error_code consistently.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 `@tests/test_resolver.py`:
- Around line 545-548: The full diagnostic contract test currently verifies
rationale, fix, and spec_ref for E011/E012/E013 but does not assert source_line,
so it can miss regressions where the offending import line is dropped from JSON.
Update the test in the diagnostic assertions block to include source_line
alongside the existing fields, using the same diag objects (e011, e012, e013) so
the public resolver contract stays fully pinned.
---
Outside diff comments:
In `@vera/resolver.py`:
- Around line 103-125: Populate the full Diagnostic payload in resolver errors
so E011/E012/E013 match the standard JSON schema. In the resolver paths that
build Diagnostic instances for circular import and related checks, thread
through the importing file and offending import line so Diagnostic.to_dict() can
include location.file and source_line, not just line/column. Update the relevant
diagnostic construction sites in resolver.py to always set description,
location, source_line, rationale, fix, spec_ref, and error_code consistently.
🪄 Autofix (Beta)
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
Run ID: 61dd7c89-ab5e-4009-ac14-b7838d40cb55
📒 Files selected for processing (11)
CHANGELOG.mdCONTRIBUTING.mdREADME.mdROADMAP.mdTESTING.mdtests/test_checker.pytests/test_codegen_modules.pytests/test_resolver.pyvera/checker/calls.pyvera/checker/registration.pyvera/resolver.py
…eRabbit) CodeRabbit follow-up on the diagnostic-contract work: E011/E012/E013 set rationale/fix/spec_ref but not location.file or source_line, so `vera check --json` exposed module-resolution failures with a schema missing two fields that every checker diagnostic carries (Diagnostic.to_dict() drops empty fields, so a bare diagnostic drifts from the documented schema). - _location_from_node now threads the importing file into location.file. - New _source_line helper reads the offending import line from the importing file (best-effort: an unreadable file yields "" rather than raising, since the source line is contextual, not essential). Mirrors the checker's _source_line. - Both threaded into all three resolver diagnostic sites (E011/E012/E013). Test-first: extended test_resolver_diagnostics_carry_full_contract to assert location.file and source_line (and that source_line names the offending import) for all three paths; confirmed RED (file=None) before the fix, GREEN after. Verified end-to-end via `vera check --json` on the ch08_circular_import fixture (location.file + source_line now present). Doc counts: test_resolver.py 585->594 lines (no new tests). Co-Authored-By: Claude <[email protected]>
|
@coderabbitai The outside-diff finding on |
|
Tip For best results, initiate chat on the files or code changes.
If I'll treat that review comment as withdrawn. ✏️ Learnings added
|
1 participant
Summary
Closes #679. Closes #814.
Chapter 8 (modules) was the only spec chapter with no
chNN_*.veraconformance coverage. It now has eight programs, one per section. Writing them to the distinguishing spec behaviour surfaced — and this PR fixes — a real module-resolution soundness bug (#814).ch08_module_declch08_import_wildcardch08_import_selectivech08_visibility_publicch08_visibility_privateexpected_error: E150ch08_shadowingch08_module_qualified_callm::fbypasses a local shadowch08_circular_importexpected_error: E011Two substrates the issue assumed but that didn't exist (both added here)
#679 said the negative test should "assert the expected E-code … mirroring the pattern used for other negative conformance tests." Neither held, so acceptance needed two enabling pieces:
resolver.py), E150 cannot import a private declaration (checker/modules.py). Unit-tested intest_resolver.py.expected_error: <code>;check_conformance.pyandtest_conformance.pythen assert the program failscheckwith that code (via--json) instead of passing.The soundness bug the coverage surfaced (#814, fixed here)
ch08_module_qualified_callandch08_shadowingwere initially watered down to dodge#814. Written to the distinguishing spec behaviour they fail — so, per the test-first discipline, they (and matching normal-harness tests) were made to fail first, then the bug was fixed:ModuleCallto a bareFnCall, dropping the module path, som::finvoked a same-named local — while the verifier resolved it correctly via its per-module registry. An unsound verifier↔runtime desync:vera verifyproved a postcondition against the module's contract that the runtime then violated (verifyOK,runtraps). Fix: shadowed module functions are emitted under a distinct, collision-freemod$…WASM name ($is illegal in Vera identifiers, like the monomorphizer'sname$T); a(module path, name) → targettable routes qualified calls to it, bare calls still resolve to the local (§8.5.2). A bare intra-module call inside a qualified-reachedmod$body is likewise redirected to the module's sibling (the residual the review found). Generic (forall) module fns are excluded — cross-module generic monomorphisation is separately unimplemented (Imported generics are not monomorphized by the importer (cross-module generic call crashes at run time) #774).Pinned by a verifier↔codegen differential (fails if either side regresses), a codegen run-value test, an intra-module-sibling test, and a wildcard/coexistence test.
Corrected diagnosis (measured, not assumed)
#814 was filed listing two module bugs. Re-investigating against the actual resolution paths corrected this:
ch08_shadowingnow proves this sharply (it passes). The failure originally attributed to Bug B was a fixture artifact:absis special-cased as a built-in by name in the verifier.absartifact surfaced a separate, unrelated soundness bug — the verifier modelsabs/min/maxby name and ignores a shadowing user definition (verifyproves a false postcondition,runtraps). Filed as Redefining any built-in function should be a checker error (one canonical form; silently unsound for abs/min/max) #815 and recorded in KNOWN_ISSUES; out of scope here (different subsystem + a design fork).Exit checklist
pytest tests/— green (full suite 5,329; +6 over the coverage baseline: 3 codegen module tests, 1 verifier §8.5.2 test, the differential, and the E-code resolver tests)mypy vera/— clean (90 files);ruff check vera/— cleancheck_conformance.py— 101 programs pass (incl. the 2 negatives viaexpected_error)check_examples.py— 35 passcheck_version_sync(0.0.184) /check_doc_counts(101 conformance, 5,329 tests) /check_site_assets/check_limitations_sync --check-states/check_spec_examples— green[0.0.184](Added programs + harness; Fixed E-codes + the Module name resolution: qualified calls don't bypass local shadows (codegen), and verifier↔codegen disagree on bare-call shadowing #814 codegen soundness fix) + link refs; ROADMAP Chapter 8 (modules) has no conformance programs #679 removed; HISTORY row; Redefining any built-in function should be a checker error (one canonical form; silently unsound for abs/min/max) #815 in KNOWN_ISSUESTo sanity-check before merge
mod$…mangling collision-safety claim ($illegal in Vera identifiers) and the intra-module-sibling redirection (C2).expected_errorharness addition is minimal and integrated into the existing manifest/runner.Closes #679.
Closes #814.
Summary by CodeRabbit
expected_error.spec_reftext, and bumped the package version to 0.0.184.