Harvest private generic module helpers#1026
Conversation
|
Important Review skippedDraft detected. Please check the settings in the CodeRabbit UI or the ⚙️ Run configurationConfiguration used: Path: .coderabbit.yaml Review profile: ASSERTIVE Plan: Pro Plus Run ID: You can disable this status message by setting the Use the checkbox below for a quick retry:
📝 WalkthroughWalkthroughImported private generic functions are now harvested for transitive compilation and included in importer-side verification. Regression tests cover successful execution through a private helper and detection of an invalid helper contract. ChangesCross-module generic compilation
Estimated code review effort: 3 (Moderate) | ~20 minutes Possibly related issues
Suggested labels: 🚥 Pre-merge checks | ✅ 7 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (7 passed)
✨ Finishing Touches🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
Greptile SummaryThis PR fixes a cross-module monomorphization gap (#1000): when an imported public generic calls a private generic helper, the private body must still be cloned into the flat WASM module and verified at the importer's instantiation sites, even though it is not directly visible to the importer. The fix harvests all
Confidence Score: 4/5The fix is correct for the single-module scenario the tests cover, but the bare-name first-seen-wins registry used for private generics means programs importing two modules that each declare an identically-named private generic will silently monomorphize the second module's calls with the first module's body — a concern flagged in a prior review that remains unaddressed. The codegen and verifier changes are structurally symmetric and handle the targeted regression correctly. However, the harvesting loop adds every private generic to a flat dictionary keyed by bare function name with setdefault, so a second module's private inner is silently shadowed by the first. This silent wrong-body substitution is an existing unresolved finding on the PR, and the new tests do not cover the multi-module private-name-collision scenario. vera/codegen/modules.py and vera/verifier.py — specifically the setdefault(tld.decl.name, tld.decl) call in the private-generic harvesting branch of both files.
|
| Filename | Overview |
|---|---|
| vera/codegen/modules.py | Core fix: harvests private generics from imported modules into _imported_generic_decls for transitive monomorphization; the new condition correctly bypasses the import-filter for private declarations, but uses bare-name setdefault so identically-named private generics from multiple imported modules silently collide (first-seen-wins). |
| vera/verifier.py | Mirrors the codegen change: the verifier's _imported_generic_decls now includes private generics so verification of public-generic clones covers their transitive private calls. Same first-seen-wins setdefault semantics as codegen. |
| tests/test_codegen_modules.py | Adds two regression tests: execution test confirms a private-helper-calling public generic returns the right value; contract-violation test confirms a lying private contract is caught at E500 during verification. Both tests are well-structured and match the existing test file patterns. |
| CHANGELOG.md | Adds an [Unreleased] Fixed bullet for issue #1000 describing the private-helper harvesting fix. |
Reviews (3): Last reviewed commit: "Merge remote-tracking branch 'fork/fix/1..." | Re-trigger Greptile
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
| # #774: an imported generic is monomorphized by the importer | ||
| # at its call sites. Private generics also need harvesting: | ||
| # an imported public generic may call one transitively, and | ||
| # that private body must be cloned into the flat WASM module | ||
| # even though it is not visible to the importer (#1000). | ||
| if tld.decl.forall_vars: |
There was a problem hiding this comment.
vera/ change
CHANGELOG.md was not updated with a new [Unreleased] bullet for this fix (issue #1000), and the commit message carries no Skip-changelog: <reason> trailer. Per the project's CI gate (scripts/check_changelog_updated.py), any PR that modifies files under vera/ or spec/ must either add a CHANGELOG bullet or include that trailer — otherwise the check fails and the PR cannot land.
Context Used: CLAUDE.md (source)
Prompt To Fix With AI
This is a comment left during a code review.
Path: vera/codegen/modules.py
Line: 277-282
Comment:
**Missing CHANGELOG entry for `vera/` change**
`CHANGELOG.md` was not updated with a new `[Unreleased]` bullet for this fix (issue #1000), and the commit message carries no `Skip-changelog: <reason>` trailer. Per the project's CI gate (`scripts/check_changelog_updated.py`), any PR that modifies files under `vera/` or `spec/` must either add a CHANGELOG bullet or include that trailer — otherwise the check fails and the PR cannot land.
**Context Used:** CLAUDE.md ([source](https://app.greptile.com/babilim-light-industries/github/aallan/vera/-/custom-context?memory=4e665b4c-6876-44d6-ad77-0d0f6eb822b4))
How can I resolve this? If you propose a fix, please make it concise.
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
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)
277-302: 🗄️ Data Integrity & Integration | 🟠 Major | 🏗️ Heavy liftMirror private imported generics in the verifier
vera/verifier.py:1139-1168still only seeds_imported_generic_declsfromis_public and in_filter._collect_instantiations()only walks the registered program, so a private generic reached transitively from an imported public generic can be cloned by codegen but never enter_instances, leaving that clone unproved and reintroducing a false Tier-1. Mirror thenot is_publicharvesting branch here and add a regression test for the private-helper case.🤖 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 277 - 302, Update the verifier’s generic-declaration harvesting logic around `_imported_generic_decls` to register private imported generics as codegen does, while retaining `name_filter` for public generics. Ensure transitively reached private helpers enter `_instances` and are verified, then add a regression test covering an imported public generic that calls a private helper.
🤖 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_codegen_modules.py`:
- Around line 780-800: Add a verifier-only test alongside
test_private_generic_reached_by_imported_public_generic_executes that gives
private generic inner a deliberately false ensures clause, invokes it through
imported public outer, and asserts the verifier returns E500. Mirror the
structure and assertions of
test_imported_generic_with_lying_contract_is_caught_at_verify while covering the
private-generic transitive harvesting path.
---
Outside diff comments:
In `@vera/codegen/modules.py`:
- Around line 277-302: Update the verifier’s generic-declaration harvesting
logic around `_imported_generic_decls` to register private imported generics as
codegen does, while retaining `name_filter` for public generics. Ensure
transitively reached private helpers enter `_instances` and are verified, then
add a regression test covering an imported public generic that calls a private
helper.
🪄 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 Plus
Run ID: 5b1676d3-554b-4f55-a74f-894114c61c6c
📒 Files selected for processing (2)
tests/test_codegen_modules.pyvera/codegen/modules.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #1026 +/- ##
=======================================
Coverage 93.51% 93.51%
=======================================
Files 96 96
Lines 32024 32024
Branches 456 456
=======================================
Hits 29948 29948
Misses 2063 2063
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:
|
… into fix/1000-harvest-private-generics
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/verifier.py (1)
1139-1169: 🎯 Functional Correctness | 🟠 Major | 🏗️ Heavy liftNamespace imported private generics per module. Bare-name
setdefaultstill collapses privateforallhelpers from different modules, so a later import can reuse the first module’sFnDecland monomorphise transitive calls against the wrong body. Use an origin-aware or module-qualified key here too.🤖 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 1139 - 1169, Update _imported_generic_decls to key private imported generic declarations by their originating module, rather than using only decl.name in out.setdefault. Preserve bare-name behavior for public generics as appropriate, while ensuring same-named private forall helpers from different modules retain distinct FnDecl entries and resolve transitive monomorphization against the correct body.
🤖 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/verifier.py`:
- Around line 1139-1169: Update _imported_generic_decls to key private imported
generic declarations by their originating module, rather than using only
decl.name in out.setdefault. Preserve bare-name behavior for public generics as
appropriate, while ensuring same-named private forall helpers from different
modules retain distinct FnDecl entries and resolve transitive monomorphization
against the correct body.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: b83d9ab6-c02e-46dc-b25f-c51a1ae20e83
📒 Files selected for processing (3)
CHANGELOG.mdtests/test_codegen_modules.pyvera/verifier.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
aallan
left a comment
aallan
left a comment
There was a problem hiding this comment.
Thanks for the fast iterations here @hasnainkhatri87 — solid progress. Re-checked against f4f1a77 locally: the verifier lockstep is correct (a lying private generic reached through an imported public one is now caught at verify with E500), test_private_generic_with_lying_contract_is_caught_at_verify pins it, and the CHANGELOG/lint is green. The core #1000 harvest works.
One problem remains, and it sits deeper than the harvest: private generics are keyed by bare name on both the codegen and verifier sides, so a name collision resolves to the wrong body.
1. Local collision → silent miscompile. An importer with its own local dup, importing a public generic that transitively calls a private dup:
lib.vera
private forall<T> fn dup(@T -> @Int) requires(true) ensures(true) effects(pure) { 0 }
public forall<T> fn caller(@T -> @Int) requires(true) ensures(true) effects(pure) { dup(@T.0) }
main.vera
import lib(caller);
private fn dup(@Int -> @Int) requires(true) ensures(@Int.result == @Int.0 + 100) effects(pure) { @Int.0 + 100 }
public fn main(@Unit -> @Int) requires(true) ensures(true) effects(pure) { dup(5) }
vera run main.vera → 0 (should be 105)
main's local dup(5) compiles to call the imported private dup$Int — check-clean, verify-clean, no trap. E608 only guards cross-module collisions (fn_provenance is imported-only), not local-vs-import.
2. Verifier keying (CodeRabbit's out-of-diff point): the verifier's _imported_generic_decls uses the same bare-name setdefault, so two modules' same-named private generics collapse to one FnDecl and the other's contract goes unverified.
Both share a root: private-generic routing needs to be module-qualified and still reroute the transitive call — dropping the and is_public gate alone fixes the local call but breaks the transitive one. That's squarely in the mono/import name-resolution family we're actively reworking (#1014 / #1015 and neighbours), so we're going to fold #1000 into that internal pass and carry it forward from here rather than have you chase the collision handling on your own.
Really appreciate you surfacing this — and the verifier-lockstep piece was the right fix. I'll link the follow-up when it lands.
2 participants
Summary
Harvest private generic helpers from imported modules for transitive monomorphization.
An imported public generic can call a private generic helper. The helper is not visible to the importing program, but its concrete clone still must be emitted into the flattened WASM module.
Closes #1000
Implementation
foralldeclarations in the code-generation generic registry.innerhelper called by public genericouter.Validation
pytest tests/test_codegen_modules.py tests/test_verifier_calls_modules.py -qruff check vera/codegen/modules.py tests/test_codegen_modules.pyvera run7git diff --checkMypy was also attempted but reported two pre-existing unused-ignore errors in untouched
vera/codegen/api.pyat lines 646 and 652.Checklist
Summary by CodeRabbit