Harden Nat-narrowing guard data structures + pin #757 deferral by aallan · Pull Request #761 · aallan/vera

aallan · 2026-06-18T14:39:36Z

Summary

Two small post-#756-review hardening follow-ups — closing the two low-value trackers that review spun off, rather than letting them age in the backlog.

#759 — `@Nat` guard data-structure hardening

Single-sourced the span key. The checker→verifier Generalize @Nat narrowing obligation to projection binding sites (ADT sub-pattern, non-literal destructure) #747 side-table was keyed by a hand-rolled (line, column, end_line, end_column) tuple built at three sites (checker/expressions.py, checker/calls.py, verifier._span_key). Extracted ast.span_key() so the write (checker) and read (verifier) halves share one constructor and can't drift apart.
Enforced the nat_fields invariant. ConstructorLayout.nat_fields runs parallel to field_offsets; user constructors build both in one loop, but the built-in MdHeading layout hand-authors them as separate literals. Added a __post_init__ assertion (nat_fields == () or len(nat_fields) == len(field_offsets)) so a drifted literal fails loudly at construction instead of as a silently mis-indexed runtime guard.
Dropped the third Harden the @Nat narrowing guard data structures (single-source span keys, enforce parallel-tuple invariants) #759 item as inert. The issue also listed "mirror expected= into _check_ability_op_call". On inspection it's (a) inert — the verifier doesn't obligate ability-op narrowings at all (lookup_effect_op doesn't search abilities) — and (b) not the one-line mirror it looked like: ability type-params are inferred from the argument types, so the expected type isn't known until after synth (a two-pass restructure). Not worth it; descoped, noted on the issue.

#760 — pin the #757 runtime deferral

The generic-instantiated constructor field is the one #747 narrowing site with no runtime guard (it erases to i64; constructor layouts carry no per-field @Nat mono metadata). Added a codegen test asserting Some(0 - 5) building an Option<Nat> compiles and runs without trapping today. When #757 lands and emits the guard, the test flips to a trap — the regression anchor, symmetric with how #754 is pinned. The verifier still obligates the narrowing statically (E503), so verified programs are unaffected.

Validation

No behaviour change. Verifier (200) + checker (521) suites green — the span-key refactor preserves the side-table read/write paths; conformance 90 + examples 35 confirm the __post_init__ assertion holds on every real layout. mypy + ruff clean.

Closes #759
Closes #760

🤖 Generated with Claude Code

Summary by CodeRabbit

Release Notes

Tests
- Added regression test to pin current behaviour in a specific generic constructor scenario.
- Increased total test count from 4,459 to 4,460.
Chores
- Improved internal robustness through stricter validation and consistency checks.
Documentation
- Updated test documentation and roadmap to reflect latest test metrics.
- Resolved documented test coverage gap.

#759, #760) Post-#756-review hardening follow-ups, kept deliberately minimal. #759 — Nat guard data-structure hardening: - Single-sourced the checker->verifier side-table span key via a new ast.span_key(), replacing the hand-rolled (line, column, end_line, end_column) tuple at three sites (checker/expressions, checker/calls, verifier). The read and write halves of the #747 side-table now share one key constructor, so the format cannot drift between them. - Added ConstructorLayout.__post_init__ asserting nat_fields is empty or length-aligned with field_offsets, so a drifted built-in literal (e.g. MdHeading) fails loudly at construction rather than as a mis-indexed guard. - Dropped the third listed item (mirror expected= into _check_ability_op_call): it is inert (the verifier does not obligate ability-op narrowings) AND not a one-line mirror (ability type-params are inferred FROM the arg types, so the expected type is unknown until after synth). Not worth the restructure. #760 — pinned the generic-instantiated-ctor-field runtime deferral with a codegen test: Some(0 - 5) building Option<Nat> compiles and runs without trapping today (the field erases to i64; no per-field mono metadata, #757). When #757 lands and emits the guard, the test flips to a trap and becomes the regression anchor, symmetric with the #754 effect-op pin. No behaviour change. Verifier (200) + checker (521) suites green (the span-key refactor preserves the side-table read/write paths); conformance 90, examples 35 (the __post_init__ assertion holds on every real layout). Closes #759 Closes #760 Co-Authored-By: Claude <[email protected]>

coderabbitai · 2026-06-18T14:39:50Z

Warning

Review limit reached

@aallan, we couldn't start this review because you've reached your PR review rate limit.

More reviews will be available in 16 minutes and 9 seconds. Learn how PR review limits work.

Your organization has used up its prepaid credits, and credit purchases are no longer available. Enable the review add-on in the billing tab to keep reviews running — you're only billed for reviews past your plan's rate limits ($0.25/file).

⌛ How to resolve this issue?

After more reviews become available, a review can be triggered using the @coderabbitai review command as a PR comment. Alternatively, push new commits to this PR.

To avoid repeated limits, reduce automatic review volume by pausing incremental auto-reviews earlier, using label-based review opt-in, excluding WIP or generated PR titles, or requesting reviews manually when the PR is ready. If your team needs uninterrupted high-volume reviews, an organization admin can enable usage-based credits.

🚦 How do rate limits work?

CodeRabbit enforces per-developer PR review limits for each organization. Most developers receive the normal plan refill rate.

For paid Pro and Pro+ PR reviews, CodeRabbit uses adaptive limits for sustained high-volume activity. When a developer's recent PR review activity reaches the 95th percentile or higher among CodeRabbit users, the refill rate gradually slows as usage increases. The highest same-day bursts are limited more strictly.

Please see our Fair Usage Limits Policy for further information.

ℹ️ Review info

⚙️ Run configuration

Configuration used: Path: .coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro

Run ID: 94a906f2-1801-48df-8d81-365cf138be28

📥 Commits

Reviewing files that changed from the base of the PR and between d53c1a6 and 6e6ceb0.

📒 Files selected for processing (1)

vera/codegen/api.py

📝 Walkthrough

Walkthrough

Introduces ast.span_key(node) as a canonical 4-tuple side-table key, adopted by _synth_expr, _check_fn_call_with_info, and ContractVerifier._span_key to eliminate independent key-construction drift. Adds a ConstructorLayout.__post_init__ assertion enforcing nat_fields/field_offsets length alignment, and pins the generic constructor-field runtime-deferral with a new regression test.

Changes

@Nat narrowing guard hardening

Layer / File(s)	Summary
Canonical `span_key` helper `vera/ast.py`	Adds `span_key(node)` returning a `(line, column, end_line, end_column)` 4-tuple or `None`, to be used as the single-sourced side-table key by checker and verifier.
Checker adoption of `ast.span_key` `vera/checker/expressions.py`, `vera/checker/calls.py`	`_synth_expr` and `_check_fn_call_with_info` replace manual `expr.span` destructuring with `ast.span_key(expr)` / `ast.span_key(c_arg)` for all side-table write sites.
Verifier adoption of `ast.span_key` `vera/verifier.py`	`ContractVerifier._span_key` delegates to `ast.span_key(expr)`, aligning lookup keys with the checker's write format and closing the drift risk.
`ConstructorLayout` invariant assertion `vera/codegen/api.py`	`__post_init__` asserts `len(nat_fields) == len(field_offsets)` (when `nat_fields` is non-empty), converting an inspection-only correctness constraint into a loud construction-time failure.
Regression test and docs/tracking `tests/test_codegen.py`, `TESTING.md`, `CHANGELOG.md`, `KNOWN_ISSUES.md`, `ROADMAP.md`	Pins the deferred generic ctor-field guard behaviour (`Some(0 - 5)` does not trap today); resolves KNOWN_ISSUES entry for `#757/`#760; removes `#759` from Tier 2 ROADMAP; increments test tallies throughout.

Estimated code review effort

🎯 2 (Simple) | ⏱️ ~10 minutes

Possibly related issues

#759 — This PR directly implements all three hardening items described in #759: the ConstructorLayout.__post_init__ assertion (nat_fields/field_offsets length invariant), the ast.span_key single-sourcing (checker and verifier), and the corresponding ROADMAP removal confirms closure.
#760 — The new test_generic_ctor_field_negative_does_not_trap_today test is the exact assertion-bearing pin described in #760, symmetric with the #754 pin, and the KNOWN_ISSUES removal confirms this is resolved.
#757 — The ConstructorLayout invariant and regression test together address the monomorphisation/metadata gap for generic-instantiated constructor fields that #757 tracks.
#747 — The ast.span_key canonicalisation directly implements the span-key single-sourcing called for as a follow-up to the #747 type-threading plumbing.

Suggested labels

compiler, tests, docs

🚥 Pre-merge checks | ✅ 4 | ❌ 1

❌ Failed checks (1 warning)

Check name	Status	Explanation	Resolution
Docstring Coverage	⚠️ Warning	Docstring coverage is 66.67% which is insufficient. The required threshold is 80.00%.	Write docstrings for the functions missing them to satisfy the coverage threshold.

✅ Passed checks (4 passed)

Check name	Status	Explanation
Description Check	✅ Passed	Check skipped - CodeRabbit’s high-level summary is enabled.
Title check	✅ Passed	Title accurately captures the main hardening objectives: single-sourced span keys and enforced data structure invariants for `@Nat` guard machinery, directly aligning with issues `#759` and `#760`.
Linked Issues check	✅ Passed	All coding requirements from `#759` and `#760` are met: span_key() helper added and deployed across checker/verifier [`#759`], ConstructorLayout invariant assertion added [`#759`], and codegen test pinning generic-ctor deferred deferral added [`#760`].
Out of Scope Changes check	✅ Passed	All changes are tightly scoped to hardening objectives: documentation/roadmap updates reflect completed work, test additions pin deferred invariants, and refactored span-key logic preserves existing side-table semantics without behaviour drift.

_{✏️ Tip: You can configure your own custom pre-merge checks in the settings.}

✨ Finishing Touches

🧪 Generate unit tests (beta)

Create PR with unit tests
Commit unit tests in branch chore/759-760-nat-guard-hardening

Warning

Review ran into problems

🔥 Problems

Git: Failed to clone repository. Please run the @coderabbitai full review command to re-trigger a full review. If the issue persists, set path_filters to include or exclude specific files.

_{Comment @coderabbitai help to get the list of available commands and usage tips.}

codecov · 2026-06-18T14:40:48Z

Codecov Report

❌ Patch coverage is 84.61538% with 2 lines in your changes missing coverage. Please review.
✅ Project coverage is 91.63%. Comparing base (25e4492) to head (6e6ceb0).

Files with missing lines	Patch %	Lines
vera/ast.py	80.00%	1 Missing ⚠️
vera/codegen/api.py	66.66%	1 Missing ⚠️

Additional details and impacted files

@@            Coverage Diff             @@
##             main     #761      +/-   ##
==========================================
- Coverage   91.63%   91.63%   -0.01%     
==========================================
  Files          70       70              
  Lines       25459    25463       +4     
  Branches      321      321              
==========================================
+ Hits        23329    23332       +3     
- Misses       2122     2123       +1     
  Partials        8        8

Flag	Coverage Δ
javascript	`65.33% <ø> (ø)`
python	`94.82% <84.61%> (-0.01%)`	⬇️

Flags with carried forward coverage won't be shown. Click here to find out more.

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

coderabbitai

Actionable comments posted: 1

🤖 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/api.py`:
- Around line 48-59: The __post_init__ method uses an assert statement to
validate that nat_fields length matches field_offsets length. Replace the assert
with an explicit if condition that raises ValueError instead. Check if
nat_fields exists and its length does not equal field_offsets length, then raise
a ValueError with the same error message that is currently in the assert
statement. This ensures the validation always executes even when Python is run
with optimization flags like -O or -OO.

🪄 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: ea88ec57-bfef-4ca8-baa9-1e27be553296

📥 Commits

Reviewing files that changed from the base of the PR and between 25e4492 and d53c1a6.

📒 Files selected for processing (10)

CHANGELOG.md
KNOWN_ISSUES.md
ROADMAP.md
TESTING.md
tests/test_codegen.py
vera/ast.py
vera/checker/calls.py
vera/checker/expressions.py
vera/codegen/api.py
vera/verifier.py

💤 Files with no reviewable changes (1)

KNOWN_ISSUES.md

…(CR #761) The __post_init__ guard used assert, which python -O/-OO strips — defeating the #759 'fail loudly at construction' intent — and was the sole failure of the CI 'ruff check --select S vera/' gate (S101). Converted to an explicit if ... raise ValueError, matching this file's existing validation style. The 35 existing vera/ asserts are '# noqa: S101' type-narrowing hints (fine to strip); this one is load-bearing validation, so it must always run. Co-Authored-By: Claude <[email protected]>

aallan added refactor Code refactoring and structural improvements testing Test suite structure and coverage labels Jun 18, 2026

coderabbitai Bot reviewed Jun 18, 2026

View reviewed changes

Comment thread vera/codegen/api.py Outdated

aallan merged commit 993963b into main Jun 18, 2026
27 checks passed

aallan deleted the chore/759-760-nat-guard-hardening branch June 18, 2026 15:03

This was referenced Jun 19, 2026

feat(746): static verification of refinement-type predicates (v0.0.174) #763

Merged

test(387): harden the verifier soundness core against mutation testing #793

Merged

This was referenced Jun 27, 2026

fix(798): trap Int/Nat arithmetic overflow + Tier-1 obligation (v0.0.181) #809

Merged

fix(813): @Nat→@Int widening soundness (+ #819 doc-gate, v0.0.186) #821

Merged

test(codegen): split test_codegen.py into 21 feature-focused files (#419) #837

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Harden Nat-narrowing guard data structures + pin #757 deferral#761

Harden Nat-narrowing guard data structures + pin #757 deferral#761
aallan merged 2 commits into
mainfrom
chore/759-760-nat-guard-hardening

aallan commented Jun 18, 2026 •

edited by coderabbitai Bot

Loading

Uh oh!

coderabbitai Bot commented Jun 18, 2026 •

edited

Loading

Review limit reached

Walkthrough

Changes

Estimated code review effort

Possibly related issues

Suggested labels

❌ Failed checks (1 warning)

Review ran into problems

Uh oh!

codecov Bot commented Jun 18, 2026 •

edited

Loading

Uh oh!

coderabbitai Bot left a comment

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

aallan commented Jun 18, 2026 • edited by coderabbitai Bot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

#759 — @Nat guard data-structure hardening

#760 — pin the #757 runtime deferral

Validation

Summary by CodeRabbit

Release Notes

Uh oh!

coderabbitai Bot commented Jun 18, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Review limit reached

Walkthrough

Changes

Estimated code review effort

Possibly related issues

Suggested labels

❌ Failed checks (1 warning)

Review ran into problems

Uh oh!

codecov Bot commented Jun 18, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

coderabbitai Bot left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

aallan commented Jun 18, 2026 •

edited by coderabbitai Bot

Loading

#759 — `@Nat` guard data-structure hardening

coderabbitai Bot commented Jun 18, 2026 •

edited

Loading

codecov Bot commented Jun 18, 2026 •

edited

Loading