Verifier cross-module honesty: right registry, right source, right binder, loud generics (#1220, #1225, #1226, #1236) - #1239
Merged
Conversation
|
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:
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: Path: .coderabbit.yaml Review profile: ASSERTIVE Plan: Pro Plus Run ID: ⛔ Files ignored due to path filters (1)
📒 Files selected for processing (11)
🔗 Linked repositories identifiedCodeRabbit considers these linked repositories for cross-repo context during reviews:
📝 WalkthroughWalkthroughThe verifier now preserves declaring-module scope for imported contracts and generic clones. SMT translation uses callee alias environments and function registries. Refined-return binders support parameterised aliases. Generic call-site preconditions produce explicit Tier-3 demotions. Regression coverage and project metrics were updated. ChangesContract scope and verification
Estimated code review effort: 4 (Complex) | ~45 minutes Sequence Diagram(s)sequenceDiagram
participant Verifier
participant CalleeScope
participant SMT
participant DeclaringModule
Verifier->>CalleeScope: Resolve imported callee scope
CalleeScope->>SMT: Translate preconditions and postconditions
SMT->>DeclaringModule: Read clause source and names
SMT-->>Verifier: Return obligations or Tier-3 demotion
Possibly related PRs
Suggested labels: 🚥 Pre-merge checks | ✅ 6 | ❌ 2❌ Failed checks (2 warnings)
✅ Passed checks (6 passed)
✨ Finishing Touches 💡 1📝 Generate docstrings 💡
🧪 Generate unit tests (beta)
Comment |
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## release/v0.1.10 #1239 +/- ##
===================================================
+ Coverage 94.00% 94.03% +0.02%
===================================================
Files 100 100
Lines 35125 35220 +95
Branches 458 458
===================================================
+ Hits 33019 33118 +99
+ Misses 2093 2089 -4
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: 5
🤖 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 `@KNOWN_ISSUES.md`:
- Line 18: Escape both pipe characters in the `#1237` table row’s inline code
example, replacing the separators in `type Grown = { `@Box`<Cnt> | `@Box`<Cnt>.0 >=
18 }` with the table-safe escaped form. Preserve the surrounding issue
description, fix direction, and issue link unchanged.
In `@tests/test_callee_contract_scope_1220_1225_1226.py`:
- Around line 744-766: Add a negative refined-return binder test alongside the
existing binder tests, using a consumer such as need100 that requires `@Nat.0` >=
100 and passing it the result of mk(20). Assert verification reports E501 and
assert _run_mod triggers the corresponding runtime trap, matching the oracle
used by the other refined-return test classes.
- Around line 198-206: Add an assertion immediately after constructing qualified
in test_a_qualified_call_quotes_the_declaring_file_too to verify the intended
import and qualified-call rewrites occurred, matching the guard pattern used by
the sibling tests. Keep the existing result and message assertions unchanged.
In `@tests/test_verifier_calls_modules.py`:
- Around line 1306-1310: Update the _e532_demotions return annotation from
list[object] to list[ProofObligation], using the existing imported type, and
remove the now-unnecessary type: ignore[attr-defined] suppression at its call
site so ProofObligation attributes remain type-checked.
In `@vera/verifier.py`:
- Around line 8133-8151: Update _get_source_line and the _error/_warning
source_line flow to read from _current_source rather than self.source,
preserving the existing span lookup behavior. Ensure diagnostics emitted for
imported or cloned clauses, including E520–E523 from _verify_fn inside
_declaring_module_scope, use the declaring module’s source buffer.
🪄 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: f5f60143-f027-4efa-9d47-97c7af851bbd
⛔ Files ignored due to path filters (1)
docs/llms-full.txtis excluded by!docs/**
📒 Files selected for processing (16)
CHANGELOG.mdFAQ.mdKNOWN_ISSUES.mdREADME.mdROADMAP.mdTESTING.mdtests/probes/README.mdtests/test_callee_contract_scope_1220_1225_1226.pytests/test_naming_env_provenance_1208.pytests/test_verifier_calls_modules.pytests/test_verifier_shadow_audits.pyvera/README.mdvera/ast.pyvera/naming.pyvera/smt.pyvera/verifier.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
Owner
Author
Adversarial review record — round 1Verdict: one HIGH regression, one MEDIUM half-finish, one MEDIUM pre-existing in the closed family, nine accuracy nits — and the core scope machinery held everything thrown at it.
Fix round dispatched; dispositions will be appended. |
This was referenced Aug 7, 2026
aallan
added a commit
that referenced
this pull request
Aug 7, 2026
Wording and characterization from the PR #1239 review; no behaviour changes, and the corpus differential is unmoved. `predicate_binder_ref` stated a false invariant — "a refinement predicate is closed over its single binder, so the first reference found is that binder". A predicate containing a CLOSURE has a second binder, and the traversal is a stack, so it reaches the closure's before the refinement's: `{ @array<Nat> | array_all(@array<Nat>.0, fn(@nat -> @Bool) … { @Nat.0 >= 18 }) }` derives the key `Nat` where the base is `Array<Nat>`. The docstring now says what is true — first in TRAVERSAL order, which is neither source order nor outermost-first — names the exception, and states the consequence: a value pushed under a key no reference resolves leaves the predicate untranslatable, a Tier-3 demotion, never a fact assumed about the wrong term. A characterization test pins both halves (the ref found, and that the verifier neither rejects the program nor claims a Tier-1 for the refinement), so the day someone makes the derivation outermost-first, the change is recorded rather than discovered. The #1236 "both drains" claim needed a qualifier: a generic call in the body AND the ensures is disclosed ONCE, from the body — a body that did not translate leaves no term to check the postcondition against, so the clause never reaches translation and demotes as E522 instead. Said in the docstring and in the CHANGELOG bullet. The corpus-movement claim was under-counted. Three programs gain an obligation; four more re-render E532's rationale, three of them examples — so seven programs' `verify --json` bytes move, not three. Corrected in the CHANGELOG and in the scratchpad differential report. `CalleeScope`'s docstring names the one lookup that deliberately stays outside the record: `_module_fn_lookup` is keyed by module PATH, so it already carries the dimension the record supplies and can only MISS — loudly, as an E532 demotion — never resolve to the wrong module's function. Two fixtures gain the note that their `type Box<T> = Nat;` is load-bearing: simplifying it to `= T` re-breaks the premise silently through #1237, and the #1226 tests would then pass or fail without touching the binder at all. And the provenance pin's floor comment describes the assertion it actually guards — its previous wording named an `all(...)` the test does not contain, which is what a floor is there to stop. Co-Authored-By: Claude <noreply@anthropic.invalid>
Owner
Author
Review record — fix round (
|
There was a problem hiding this comment.
Actionable comments posted: 3
♻️ Duplicate comments (1)
KNOWN_ISSUES.md (1)
19-19: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winThe
#1237row still breaks the table — the pipe is unescaped.The earlier fix removed the inner backticks around
@Boxbut left the|itself bare inside{@box<Cnt> |@box<Cnt>.0 >= 18 }. Backticks do not protect a pipe in a GitHub Flavoured Markdown table cell. markdownlint confirms the row is still split: MD056 reports "Expected: 2; Actual: 3; Too many cells, extra data will be missing".Everything after the pipe is discarded at render time — the
AdtType(name='T')explanation, the spurious-E501 impact, the "distinct root cause from the fixed#1226" note, the fix direction, and the issue link. The rest of this table already escapes them: lines 14, 22, 38 and 41 all write\|.📝 Proposed fix for the cell split
-| A parameterised type-alias APPLICATION is not substituted when a refinement's base is resolved: `type Box<T> = T; type Grown = { `@Box`<Cnt> | `@Box`<Cnt>.0 >= 18 };` resolves `Grown`'s base to `AdtType(name='T')` — the alias's own parameter leaking as an ADT name — so the base fails the modelled-primitive gate, the refined-return fact is dropped, and a valid program is rejected with a spurious E501 while `vera run` returns 0. Distinct root cause from the fixed `#1226` (the binder KEY); fix direction: the verifier's base resolution substitutes the application's arguments, the discipline the naming module already applies on its side. | [`#1237`](https://github.com/aallan/vera/issues/1237) | +| A parameterised type-alias APPLICATION is not substituted when a refinement's base is resolved: `type Box<T> = T; type Grown = { `@Box`<Cnt> \| `@Box`<Cnt>.0 >= 18 };` resolves `Grown`'s base to `AdtType(name='T')` — the alias's own parameter leaking as an ADT name — so the base fails the modelled-primitive gate, the refined-return fact is dropped, and a valid program is rejected with a spurious E501 while `vera run` returns 0. Distinct root cause from the fixed `#1226` (the binder KEY); fix direction: the verifier's base resolution substitutes the application's arguments, the discipline the naming module already applies on its side. | [`#1237`](https://github.com/aallan/vera/issues/1237) |🤖 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 `@KNOWN_ISSUES.md` at line 19, Escape the pipe in the `#1237` table cell’s inline refinement example, changing the bare separator in `{ `@Box`<Cnt> | `@Box`<Cnt>.0 >= 18 }` to the table-safe form `\|`. Preserve the remaining issue description and link unchanged so the row remains a valid two-column Markdown table.Source: Linters/SAST tools
🤖 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_callee_contract_scope_1220_1225_1226.py`:
- Around line 915-917: Update test_the_bare_and_qualified_spellings_agree to
assert that each str.replace operation actually changes _MID_REQ before
comparing results. Guard both the import rewrite and cap(0) qualification
rewrite, so the test fails if either expected source fragment is absent.
- Around line 1150-1160: Update `_predicate` to return `tuple[ContractVerifier,
ast.RefinementType]` instead of `object`, importing the required AST type if
needed. Before returning `verifier.env.type_aliases["Grown"].body`, assert or
otherwise narrow the optional alias body to a non-optional `ast.RefinementType`.
- Around line 1024-1030: Update the _verify_mod verification call to pass the
explicit entry filename file="main.vera", then retain the diagnostic assertion
against that expected filename so incorrect entry-file attribution cannot pass.
---
Duplicate comments:
In `@KNOWN_ISSUES.md`:
- Line 19: Escape the pipe in the `#1237` table cell’s inline refinement example,
changing the bare separator in `{ `@Box`<Cnt> | `@Box`<Cnt>.0 >= 18 }` to the
table-safe form `\|`. Preserve the remaining issue description and link
unchanged so the row remains a valid two-column Markdown table.
🪄 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: 179b143e-53df-4735-a328-ce1796c9d961
⛔ Files ignored due to path filters (1)
docs/llms-full.txtis excluded by!docs/**
📒 Files selected for processing (13)
CHANGELOG.mdFAQ.mdKNOWN_ISSUES.mdREADME.mdROADMAP.mdTESTING.mdtests/test_callee_contract_scope_1220_1225_1226.pytests/test_naming_env_provenance_1208.pyvera/README.mdvera/ast.pyvera/naming.pyvera/smt.pyvera/verifier.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
Owner
Author
Review record — mini-review of the fix round (
|
Owner
Author
Review record — final fix (
|
There was a problem hiding this comment.
Actionable comments posted: 3
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)
2328-2329: 🗄️ Data Integrity & Integration | 🟠 Major | ⚡ Quick winPreserve the declaring-module file in the aggregate fallback.
After Line 2329,
_declaring_module_scoperestores the entry-module state. If_emit_aggregated_diagnosticcannot matchrep_obto an instance diagnostic, its fallback createsSourceLocation(file=self.file, ...). An imported clone then reports the entry file whilerep_ob.filenames the declaring module.Use
rep_ob.file or self.filefor the fallback location. This keeps the diagnostic and obligation joinable on(file, line, column).Proposed fix
location=SourceLocation( - file=self.file, line=rep_ob.line, column=rep_ob.column, + file=rep_ob.file or self.file, + line=rep_ob.line, + column=rep_ob.column, ),🤖 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 2328 - 2329, Update the fallback location construction in _emit_aggregated_diagnostic to use rep_ob.file when available, falling back to self.file otherwise. Preserve the existing line and column values so imported clones remain joinable with their declaring-module diagnostics.
🤖 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_callee_contract_scope_1220_1225_1226.py`:
- Around line 1231-1241: Update test_no_obligation_cites_a_line_its_file_lacks
to build the imported modules explicitly, then extend lengths with
str(modules[0].file_path) mapped to that module’s source line count. Keep the
existing main-file and unrestricted-entry checks, and use the expanded lengths
mapping to assert imported obligations never cite lines beyond their module
source.
In `@tests/test_cli.py`:
- Around line 674-707: Update the CLI verification test around cmd_verify to
capture its return code and assert rc == 1, then assert the parsed JSON payload
has data["ok"] is False before validating obligations and diagnostics. Preserve
the existing JSON parsing and diagnostic assertions.
In `@vera/lexical.py`:
- Around line 205-206: Update the fast-path guard in _contract_source_text to
also check for "/*" before returning source unchanged, ensuring annotation
comments are passed through blank_comments and removed from rendered clauses.
---
Outside diff comments:
In `@vera/verifier.py`:
- Around line 2328-2329: Update the fallback location construction in
_emit_aggregated_diagnostic to use rep_ob.file when available, falling back to
self.file otherwise. Preserve the existing line and column values so imported
clones remain joinable with their declaring-module diagnostics.
🪄 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: 99cc291f-87af-4d46-85e7-4af5217c13c5
⛔ Files ignored due to path filters (1)
docs/llms-full.txtis excluded by!docs/**
📒 Files selected for processing (14)
CHANGELOG.mdFAQ.mdKNOWN_ISSUES.mdREADME.mdROADMAP.mdTESTING.mdtests/test_callee_contract_scope_1220_1225_1226.pytests/test_cli.pytests/test_obligations.pyvera/README.mdvera/cli.pyvera/lexical.pyvera/obligations/core.pyvera/verifier.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
…1220) A contract clause's span numbers lines in the file that DECLARED it, and the E501 renderer indexed the IMPORTER's buffer with it. The `Precondition:` line of a cross-module call violation therefore showed whatever text sat on that line in the importer: where the importer had a `requires` of its own there, the message read as a perfectly well-formed clause belonging to another function, and where the callee's file was the longer one the line fell off the end and the message dropped `Precondition:` entirely. Both halves of "which file is this?" now ride one scope. `_declaring_module_ scope` takes the origin module rather than a bare env and swaps the naming env and the source buffer together, so a clone named in one module cannot quote another's text; `_origin_module_for_generic` is the single chain walk both reads resolve through. Every clause a module declares is additionally pinned to that module's source at registration, walked off the module AST rather than off the flat, last-wins function registry, so a file spelling one helper name twice pins both. A clause reached through the harvested registry, through a `mod::fn` qualified call, or through a monomorphized clone now quotes the same file. The new suite asserts the misattribution direction, not just the absence of the right text: both files carry a plausible `requires` on the same line number, so the pre-fix rendering produced a clause a reader could not tell was the wrong one. Four of its six tests go red against the unfixed verifier; the two that do not are its controls (a local callee, and the runtime oracle proving the imported-helper E501 is a caught violation rather than a spurious one). The `#1208` provenance suite's `TestImportedCalleeContractEnv` closes the loop it deliberately left open citing this issue. The corpus is byte-identical: no `examples/` or `tests/conformance/` program moves a diagnostic, a tier count or an obligation. Co-Authored-By: Claude <noreply@anthropic.invalid>
…1225) A `requires` / `ensures` calls other functions by bare name, and the SMT layer resolved those names through the IMPORTER's registry while it rendered the same contract's slots in the callee's namespace. A module whose exported function is guarded by `requires(@Int.0 < cap(0))` therefore had its precondition interpreted using whatever `cap` the importing file declared — a private helper the callee cannot see. `vera verify` reported all-Tier-1 clean and `vera run` trapped on the precondition the callee actually has. Moving the same literal the other way gives the mirror, a valid call rejected with a spurious E501, and the `ensures` path fails one step later: a postcondition read too strongly proves the CALLER's contract, so the caller is what traps. The naming env and the function registry are now one `CalleeScope`, applied and restored as a pair by one context manager. A scope that swapped one and not the other is precisely the defect — the contract would be read half in its own module and half in the importer's — so making them separable again requires taking the record apart. The pin covers every function a module declares, private helpers included and its builtins behind them, because that is the namespace a bare name in one of its contracts resolves in. The fallback for a callee nothing pins is the scope IN FORCE at the call, passed in by the SMT layer as the same record it saves for the restore: a helper reached from inside another callee's contract is declared in the module being read, not in whatever function the verifier is walking. `_bind_smt_scope` is the one place the verifier hands the SMT layer a scope, so the warm session and the cold path cannot come to bind different halves, and the E501 renderer reads the same pin through the same accessor. `TestBothHalvesOfTheScopeRideTogether` is the seam's own test: one callee contract whose precondition names an alias-typed parameter AND calls a private helper, arranged so that only reading BOTH halves in the callee's module makes it false. Either half read in the importer — or both — proves the precondition and returns a verify-clean verdict on a program that traps. Two isolating controls then show each half separately decides a verdict, so the pair test cannot be passing on one of them alone. Every direction carries a runtime oracle, since a vanished obligation and a spurious one look identical from inside the verifier. All seven new tests go red against the previous commit. Three shapes that used to demote to a loud Tier-3 (E532), because the callee's contract named a function absent from the importer entirely, now get a static verdict the runtime agrees with. The `examples/` and `tests/conformance/` corpus is byte-identical: no diagnostic, tier count or obligation moves. Co-Authored-By: Claude <noreply@anthropic.invalid>
…1226) The binder a refinement predicate was translated under came from the predicate's HEAD identifier, and a head is the binding-table key only when the binder carries no type arguments. `type Grown = { @box<Cnt> | @box<Cnt>.0 >= 18 }` pushed the value under `Box` while `@Box<Cnt>.0` resolves `Box<Nat>`, so the predicate failed to translate and the fact was dropped in silence: at the caller a valid program was rejected with a spurious E501 — `vera run` returns from the same program without trapping — and at the producing function a provable refined return demoted to a Tier-3 runtime guard (E506). `naming.predicate_binder_key` renders the WHOLE reference against the environment the predicate is about to be translated in, so the push side and the lookup side are one derivation over one environment. Both consumers take it: the SMT layer's assumed refined return and the verifier's own membership translation, which reads it off the very `SmtContext` doing the translating rather than off an env passed alongside. `ast.predicate_binder_ref` returns the reference the key is rendered from, and `predicate_binder_name` — the head-only helper, now with no consumer — goes with the bug it caused. Being env-dependent is what makes the callee-namespace wrap around the refined-return translation load-bearing rather than defensive. Moving the derivation outside that scope leaves the single-module case green and turns the cross-module one red, because the same predicate binds `Box<Nat>` in the defining module and `Box<Int>` under an importer's `type Cnt = Int` — exactly the prediction `TestRefinedReturnTranslatesInTheCalleeNamespace` recorded by provenance while the bare-headed binder still masked it. That pin is retargeted at the new derivation (its own floor assertion caught the instrument going blind) and now cites the behavioural assertion beside it. Four new tests, all red against the previous commit, over both sides of the key: the caller's accepted program with its runtime oracle, the producer's Tier-1 discharge, an unparameterised control, and the cross-module twin with its own no-conflict control. The `examples/` and `tests/conformance/` corpus is byte-identical. Co-Authored-By: Claude <noreply@anthropic.invalid>
…it (#1236) A contract written over type parameters has no Z3 sort to build a call summary from, so the SMT layer bails on any callee with `forall_vars` — and it bailed SILENTLY, recording nothing. Unlike every other arm of the same taxonomy (an untranslatable argument, an untranslatable precondition), the call-site obligation did not exist rather than demoting: an importer calling `forall<T> fn pick(@array<T>, @int -> @int) requires(@Int.0 > 10)` as `pick([1, 2], 3)` was reported all-Tier-1 clean while the run trapped on `pick$Int`'s own entry guard. A false Tier 1. It now records the same E532 Tier-3 disclosure the untranslatable-argument path records, naming the generic callee, under the same gate — a callee with only `requires(true)` has no obligation to lose — and through both drains, so a generic call written in the caller's `ensures` is disclosed as well as one in its body. The demotion is unconditional on whether the precondition would in fact HOLD: this is a "cannot check", not a "does not hold", so the satisfied call demotes beside the violating one. Discharging either statically means translating the contract at each monomorphized INSTANCE, which is #732's per-instantiation machinery rather than this call-summary path, and the docstring says so. The postcondition half gets no record of its own, deliberately. An unassumed fact is conservative, and it already surfaces wherever it mattered — the caller's own clause fails to translate and demotes (E520/E522), or a later call's argument does and demotes here. Reifying it as a Tier-3 obligation would claim a runtime check the CALLER never performs (the callee's `ensures` is guarded in the callee, and counted there), which would make the tier bookkeeping less honest, not more. Six new tests, three of them red against the previous commit: the violating direction with the runtime oracle that makes the old verdict a false one rather than a true one, the satisfied direction, the ensures-clause position, and two controls — a non-generic twin still discharged statically (E501 when violated, Tier-1 clean when not) and a `requires(true)` generic that stays silent. Corpus: three `tests/conformance/` programs move, each gaining exactly one E532 warning and one `call_pre` Tier-3 obligation over a `forall` callee with a real precondition (`first_of_first_array`, `opt_count`, `first`). No `examples/` program moves, no Tier-1 count changes, no verdict flips. One existing assertion moves with them: `test_body_nat_underflow_discharged_when_ guarded` asserted `tier3_runtime == 0` as a proxy for "the body proves", and the program's remaining Tier-3 is now the call site, not the body — it asserts the body's `nat_sub` is verified and that the ONE Tier-3 left is the call-pre demotion (that call is in fact safe; the swapped arguments compensate for the De Bruijn order, so it is the conservative direction). E532's rationale names the generic cause beside the host-handle one. KNOWN_ISSUES gains the row for #1237, the parameterised-alias-application leak through refinement-base resolution that PR B.3's probing turned up; it is a type-resolution defect distinct from the binder-key one fixed here as #1226, and lands in PR C. Co-Authored-By: Claude <noreply@anthropic.invalid>
… file Two review findings on the cross-module contract scope, both about a module being read as though it were a lone file. A module's contract calls bare names, and a bare name it can call is one its own file declares OR imports. The registry pinned as its `CalleeScope` came from `_register_all`, which walks declarations only, so an imported name resolved to nothing — silently, and only for the bare spelling. The requires direction demoted an honest Tier-1 to E532 while the same call written `deep::cap(0)` stayed Tier-1; the ensures direction REJECTED a valid program whose run returns exactly what its `ensures` demands. A regression of the #1225 commit: before it, the miss fell through to the importer's registry and usually found something. Each module now takes its imports' public surface exactly as the entry program does — same import-name filter, same `setdefault`, so its own declarations win a clash — through a two-pass registration, because the module it imports may be registered after it. What a module OWNS is snapshotted before any injection and is what it exports and what its scope is pinned to: filling the registry must not re-export a name the module merely imports (§8.6.4), nor pin another module's contract to this one's namespace. A name outside the module's own import filter still misses, and misses loudly (E532) — `vera check` on that module alone rejects it as unresolved (§8.5.1), so binding it to whatever the importer happens to have would interpret a contract with a function the callee cannot name. The rendering half of #1220 was likewise finished only for the quoted clause. The excerpt under the caret was sliced from the entry buffer and the location named the entry file, so a diagnostic raised while an imported clone verifies pointed at the importer's line N for another file's line N — and where the importer is the shorter file, at an empty excerpt with nothing to say it was missing. Both now come from the module under verification: `_declaring_module_ scope` carries the file name beside the env and the source, so a line number and the file it numbers cannot disagree. A clause broken across lines is quoted whole, too, rather than truncated at the first newline into an unbalanced-parenthesis fragment naming a condition the program does not have. Fifteen new tests, ten of them red against the previous commit (the rest are controls). The reviewer's two proving programs are adopted verbatim in behaviour, and the battery they exposed is added: a DEPTH-2 module chain, the shape neither the corpus nor this suite contained — which is exactly why a byte-identical corpus differential said nothing about the regression. The corpus differential is byte-identical again here, and this time that is a claim about programs the fix cannot reach rather than evidence it changes nothing. KNOWN_ISSUES gains the row for #1241 (an imported generic's clone resolving its BODY's bare calls in the importer's registries), which is NOT fixed here: the checker's answer is the module's own, and the verifier and codegen mis-resolve TOGETHER, so today's verdict still matches the runtime. Fixing the verifier alone was prototyped and measured — it turns the honest rejection of `reviewB3pr/xg4` into a verify-clean verdict on a program that still traps, a false Tier-1 — so the two halves have to land together. Co-Authored-By: Claude <noreply@anthropic.invalid>
Wording and characterization from the PR #1239 review; no behaviour changes, and the corpus differential is unmoved. `predicate_binder_ref` stated a false invariant — "a refinement predicate is closed over its single binder, so the first reference found is that binder". A predicate containing a CLOSURE has a second binder, and the traversal is a stack, so it reaches the closure's before the refinement's: `{ @array<Nat> | array_all(@array<Nat>.0, fn(@nat -> @Bool) … { @Nat.0 >= 18 }) }` derives the key `Nat` where the base is `Array<Nat>`. The docstring now says what is true — first in TRAVERSAL order, which is neither source order nor outermost-first — names the exception, and states the consequence: a value pushed under a key no reference resolves leaves the predicate untranslatable, a Tier-3 demotion, never a fact assumed about the wrong term. A characterization test pins both halves (the ref found, and that the verifier neither rejects the program nor claims a Tier-1 for the refinement), so the day someone makes the derivation outermost-first, the change is recorded rather than discovered. The #1236 "both drains" claim needed a qualifier: a generic call in the body AND the ensures is disclosed ONCE, from the body — a body that did not translate leaves no term to check the postcondition against, so the clause never reaches translation and demotes as E522 instead. Said in the docstring and in the CHANGELOG bullet. The corpus-movement claim was under-counted. Three programs gain an obligation; four more re-render E532's rationale, three of them examples — so seven programs' `verify --json` bytes move, not three. Corrected in the CHANGELOG and in the scratchpad differential report. `CalleeScope`'s docstring names the one lookup that deliberately stays outside the record: `_module_fn_lookup` is keyed by module PATH, so it already carries the dimension the record supplies and can only MISS — loudly, as an E532 demotion — never resolve to the wrong module's function. Two fixtures gain the note that their `type Box<T> = Nat;` is load-bearing: simplifying it to `= T` re-breaks the premise silently through #1237, and the the provenance pin's floor comment describes the assertion it actually guards — its previous wording named an `all(...)` the test does not contain, which is what a floor is there to stop. Co-Authored-By: Claude <noreply@anthropic.invalid>
Skip-changelog: three-row bug-table bookkeeping, no compiler change Co-Authored-By: Claude <noreply@anthropic.invalid>
The rendering fix moved DIAGNOSTICS onto the declaring module and left the other half of `verify --json` behind. `ProofObligation` had no file at all, so the CLI stamped the entry path on every entry — under a comment explaining that a consumer must be able to join an obligation to its diagnostic on `(file, line, column)`, a premise the same fix had just falsified. The join produced non-matches for anything raised while an imported body verified (the E501 said `hlib.vera:10`, its own obligation said `main.vera:10`), and the obligation stream cited lines past the entry file's end — the exact class the diagnostic side had just stopped doing. An obligation now carries its file, taken from the same `_current_file` a diagnostic raised at that moment would carry, and the CLI emits it. The fallback to the entry path covers only an obligation reified with no file, which a run given a path does not produce — the verifier is handed `file=str(p)` and hands it straight back, so a main-file obligation still carries byte-identically what its diagnostic carries. The field joins `content_key` as well: a span is unique only within one file, so two identical obligations in an importer and an imported module would otherwise share a cache entry, and adding it can only split entries, never merge them. It is additive — the warm session and the language server copy whole records and read positions — and the incremental suite's cold twin now runs with the same file its warm run is given, which is what that comparison always meant. `_contract_source_text` blanks comments before joining lines, through the lexer's own scanner: joining put a trailing `--` comment in front of the rest of the clause, so the message showed a condition that stops where the comment starts and quoted the comment's prose as code. Using the scanner rather than splitting on `--` is what keeps a `--` inside a string literal intact. Wording, with the facts re-measured rather than recalled: `vera check` on a module that references a name outside its own import filter WARNS (E200, exit 0) — it does not reject — so the entry-point asymmetry is warn-vs-silent, and the #1244 row and the depth-2 test's docstring say that now (the duplicate row this branch had picked up is merged into one). #1241's parenthetical claimed a rejection too, where the accurate evidence is that the type-discriminating program CHECKS CLEAN, which only types if the body's call means the declaring module's. E532's rationale names its third cause, the module-scope miss. And KNOWN_ISSUES gains #1242, the `verification.total` disagreement with the obligations array. Co-Authored-By: Claude <noreply@anthropic.invalid>
Seven fixes from CodeRabbit's passes over PR #1239; the eighth was already fixed by an earlier commit in the branch. The `#1237` row's inline example carried two unescaped `|` characters, which a code span does not protect inside a table cell: the row rendered as three cells in a two-column table and everything past the pipe — impact, fix direction and the issue link — was dropped at render time. Escaped, as the rest of the table already does. A sweep of every issue row's unescaped-pipe count found no other broken cell (the five-column workarounds table is correctly five). Three test rewrites built a fixture with `str.replace` and never checked that either replacement landed. A reworded source makes them no-ops, and each test then silently re-runs the case it is supposed to contrast with: the qualified call re-runs the bare import, and the bare-vs-qualified tier comparison compares the bare spelling against itself and passes. All three now assert the rewrite before using it. `_verify_mod` verified with no file, so the location assertion beside it could only rule out `None` and the literal it named — any THIRD file would have satisfied it. It verifies under a named entry file now, and the assertion compares against the imported module's exact path. The refined-return classes asserted only that the fact SURVIVES. A regression that keyed the binder correctly and then assumed more than the refinement grants would have passed every one of them, which is the over-correction its sibling class guards against with a mirror test. A consumer demanding `>= 100` from a refinement granting `>= 18` is now pinned as a rejection, with the runtime oracle that separates a correct rejection from the spurious one this work removed. Two annotations were widened to `object`, which erased the element type and forced an `attr-defined` suppression to read a field back: `_e532_demotions` returns `list[ProofObligation]` and the closure-binder helper returns its concrete pair, narrowing the alias body it unpacks. Already fixed, not skipped: `_get_source_line` reading the entry buffer was the half of #1220 that `eddd6f86` finished — it reads `_current_source` now, which is what the finding asks for. Co-Authored-By: Claude <noreply@anthropic.invalid>
aallan
force-pushed
the
fix/1220-1225-1226-verifier-xmod
branch
from
August 8, 2026 00:01
fb2b86b to
d59a430
Compare
Owner
Author
Review record — CR round + rebase (
|
There was a problem hiding this comment.
Actionable comments posted: 1
♻️ Duplicate comments (1)
tests/test_callee_contract_scope_1220_1225_1226.py (1)
1279-1289: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winThe imported module's file still has no line bound.
lengthsholds two keys:"main.vera"andNone. The imported module's obligations carrystr(module.file_path), which is in neither.lengths.get(o.file)returnsNonefor every one of them, theif limit is not Noneguard skips, and no bound is checked.The test is named for the symptom the whole class exists to catch — a line number past its file's end — and the module-located obligations are exactly the entries that regressed. Those are the entries this loop passes over.
_verifiedbuildsmodulesitself when the argument isNone, so the fix needs the list built at the call site to read itsfile_pathandsource.As per path instructions, test files must be reviewed for "Missing edge cases for new compiler features".
🧪 Proposed bound for the imported module
def test_no_obligation_cites_a_line_its_file_lacks(self) -> None: """The symptom that made the break visible without a join.""" - lengths = { + modules = [_resolved(("hlib",), _HELPER_LIB)] + lengths = { "main.vera": len(_HELPER_MAIN.splitlines()), + str(modules[0].file_path): len(modules[0].source.splitlines()), None: 10**9, } - result = self._verified() + result = self._verified(modules) for o in result.obligations: limit = lengths.get(o.file) if limit is not None: assert o.line <= limit, (o.kind, o.file, o.line)🤖 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_callee_contract_scope_1220_1225_1226.py` around lines 1279 - 1289, Update test_no_obligation_cites_a_line_its_file_lacks to retain the modules list passed into _verified, derive each imported module’s file path and source line count, and include that path-to-length mapping in lengths. Preserve the existing main.vera and unrestricted None entries, then ensure the loop validates module-located obligations against their actual source bounds.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_verifier_calls_modules.py`:
- Around line 1391-1410: Add a sibling verifier test covering a generic pick
call in both caller’s body and ensures clause, using the existing _verify, pick,
and _e532_demotions helpers. Assert exactly one E532 call_pre demotion sourced
from the body, and additionally verify the ensures clause records the expected
E522 obligation rather than a second E532 demotion.
---
Duplicate comments:
In `@tests/test_callee_contract_scope_1220_1225_1226.py`:
- Around line 1279-1289: Update test_no_obligation_cites_a_line_its_file_lacks
to retain the modules list passed into _verified, derive each imported module’s
file path and source line count, and include that path-to-length mapping in
lengths. Preserve the existing main.vera and unrestricted None entries, then
ensure the loop validates module-located obligations against their actual source
bounds.
🪄 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: 0d39a5f3-ee9d-4389-8141-50c52e3e20ec
⛔ Files ignored due to path filters (1)
docs/llms-full.txtis excluded by!docs/**
📒 Files selected for processing (11)
CHANGELOG.mdFAQ.mdKNOWN_ISSUES.mdREADME.mdROADMAP.mdTESTING.mdtests/probes/README.mdtests/test_callee_contract_scope_1220_1225_1226.pytests/test_verifier_calls_modules.pyvera/README.mdvera/naming.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
The closing review round: one real defect in each of the two things the last
round added, and three tests for rules nothing pinned.
`blank_comments`'s early return checked for `--` and `{-` and returned the
source untouched otherwise — but the scanner it delegates to knows a third
form, the annotation comment `/* */` (spec §1.3). A clause whose only comment
was an annotation therefore skipped blanking entirely and was quoted with the
comment inside it, which is the defect the blanking exists to prevent. The
guard now names all three openers, because an optimisation that recognises less
than the thing it is short-circuiting is a behaviour change wearing a fast
path's clothes.
The aggregate diagnostic a generic instantiation synthesises when no
per-instance diagnostic matches built its location from `self.file` and the
obligation's line. That path runs AFTER `_declaring_module_scope` has been
left, so for an imported clone it paired the entry program's name with the
declaring module's line number — the join the previous commit restored, broken
in the one place that synthesises a diagnostic rather than re-emitting one. It
takes the obligation's own file.
Three rules that held but nothing checked. A generic call written in BOTH the
body and the `ensures` is disclosed once, from the body, with the clause taking
E522 — every existing fixture has the call in one position only, so a
double-recording regression would have passed all of them. The no-line-past-EOF
test bounded only the entry file, leaving an obligation that names the MODULE
free to cite any line at all; both files are bounded now, and the set of files
seen is asserted so the bound cannot go unexercised. And the CLI join test
discarded the return code: it asserts `rc == 1` and `ok is false`, since an
E501 reported with a success exit is exactly the regression a test about that
message should catch.
Co-Authored-By: Claude <noreply@anthropic.invalid>
Owner
Author
|
@coderabbitai Re the outside-diff finding on vera/verifier.py from the fb2b86b-era review (now 68eb106 post-rebase): verified against current code and fixed in 327162b, exactly as proposed — _emit_aggregated_diagnostic's synthesised fallback now builds its SourceLocation from rep_ob.file (falling back to the entry file). Your reasoning holds and is worth restating: aggregation runs after _declaring_module_scope has been left, so self.file is the entry program again while the representative obligation's line numbers the module that declared the clone — the one place that SYNTHESISES a diagnostic rather than re-emitting a matched one, and therefore the one residual break of the (file, line, column) join after the obligation gained its file. The matched path is unaffected (it re-emits the per-instance diagnostic, which already carries the right location). Review record — closing round (
|
|
Tip For best results, initiate chat on the files or code changes.
✏️ Learnings added
You are interacting with an AI system. |
This was referenced Aug 8, 2026
Closed
aallan
added a commit
that referenced
this pull request
Aug 12, 2026
Two diagnostics that described a consequence rather than the cause. The LSP's per-function tier hints were synthesised from the whole obligation stream, which carries the imported modules an entry program pulls in. Those obligations' line numbers index the module that declared them, so an imported generic's hint was published at that line number in the CURRENT document — on whatever text happened to share it, or past the end. publishDiagnostics is per-URI, so a foreign obligation is not this document's to publish under any line; #1239's ProofObligation.file is what finally makes them distinguishable. A record with no file at all came from outside a verifier run, not from another module, so it keeps its hint. The literal range check knew the i64 and u64 bounds but not the Byte one, so a @byte context took 0..255 and let everything else fall through to @nat — and the literal's mistake was then described by whichever mismatch that produced downstream: E301 in a join, E202 at an argument, E170 under a let, E331 at a handler initialiser, a return-type mismatch in a body. All five are one E149 at the literal now, naming 0..255, and the literal keeps the type its context asked for so nothing cascades behind it. Three tests that pinned the old downstream wording assert the range message instead. Closes #1246 Closes #1252 Co-Authored-By: Claude <noreply@anthropic.invalid>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Verifier cross-module honesty: right registry, right source, right binder, loud generics (#1220, #1225, #1226, #1236)
Part of the #1213 burndown (PR B.3). Four commits, one theme: an imported callee's contract is interpreted, quoted, and keyed entirely in its OWN module's terms — and what cannot be interpreted statically discloses loudly instead of vanishing.
#1225 (
2b7330ec) — the false Tier-1: a bare-name call inside an imported module's contract resolved against the IMPORTER's function registry.smt.CalleeScopeis now a frozen (alias_env, fn_lookup) pair — one record, one swap, one restore in onefinally— so the two halves structurally cannot diverge; the verifier pins one scope per module at registration, and both consumers (translation and the E501 renderer) read the same pin. Behaviorally proven with a contract where the naming env decides WHICH argument and the registry decides WHAT the guard function is: only one of the four combinations is honest, and the suite pins all four. Both repro directions flip (false-clean → E501-agreeing-with-the-trap; spurious-flag → clean-run-50), the ensures path flips (false Tier-1 → honest E500), and the no-collision control upgrades from loud Tier-3 to honest Tier-1 both ways.#1220 (
fc57fd1c) — the quoted text: E501 for an imported callee now quotes the callee's actual clause out of the file that declared it (before: the importer's own line at the callee's span — a well-formed clause belonging to another function — or no quote at all when the span ran past a short importer). The deferred text assertion in PR A'sTestImportedCalleeContractEnvis closed.#1226 (
82040aaf) — the binder key: a refined return over a parameterised base pushed the bare head (Box) where the reference resolvesBox<Nat>, dropping the return fact and spuriously rejecting valid programs. The binder now derives throughnaming.predicate_binder_keyinside the callee scope; the single-module repro goes spurious-E501 → 7-verified-Tier-1-clean, the cross-module twin likewise, and the provenance pin that predicted this dependency was retargeted — its own floor assertion caught the instrument going blind when the hook moved.ast.predicate_binder_namelost its last consumer and is deleted.#1236 (
ad2a3415) — the vanishing generic obligations: aforallcallee's call-site precondition produced NO obligation and NO demotion (verify said Tier-1 clean; the run trapped). It now discloses as an E532call_preTier-3 record from both translation drains (body and caller-ensures positions). Corpus movement: exactly 3 conformance programs, each +1 honest disclosure, zero verdict flips, zero examples. Deliberate design choice, stated for review: the requires direction is reified; acall_postobligation is deliberately NOT — an unassumed calleeensuresis conservative (the caller proves less, never more), and acall_postTier-3 record would add a "falls to a runtime check" claim for a check the caller never performs (the callee guards and counts its own ensures). Full static discharge of mono-instantiated contracts is #732's scope, cited in the code.Corpus:
verify --jsonbyte-identical across 241 programs after each of the first three commits; the fourth moves exactly the three programs above. KNOWN_ISSUES rows for the four issues deleted; the #1237 row added (the parameterised-alias-application leak this PR's probing found — distinct root cause, lands in PR C). Suite 9,530 tests / 147 files.Closes #1220. Closes #1225. Closes #1226. Closes #1236. (Keywords take effect at the release PR.)
Review provenance
Adversarial review to fixed-point with per-round records, CodeRabbit ledger convergence, and the CI wall gate the merge, per the #1213 protocol.
Summary by CodeRabbit
Bug Fixes
Documentation