Diagnose old()/new() applied to an expression (#1173)

[aallan]

old(@Int.0) in a contract clause reported a generic [E005] parse error with the caret on its own argument. Nothing named old, nothing said what its argument has to be, and the spec pointer went to the formal-grammar chapter. Found by the VeraBench v0.0.18 sweep, VB-T5-009, GPT-5.6 Sol.

What the issue turned out to be

The report frames this as "old() outside ensures()". Probing first changed the diagnosis, and the fix follows the probe rather than the title.

Vera's old/new take an effect reference — old(State<Int>), spec §7.9.2 — not a Dafny-style arbitrary expression. So old(@Int.0) is rejected by old_expr: "old" "(" effect_ref ")" at parse time, wherever it appears. The same [E005] fires inside ensures():

  ensures(old(@Int.0) > 0)
              ^
  Unexpected "@" at this position. Expected one of: UPPER_IDENT

The clause-placement rule the title describes was already implemented and already had a good diagnostic. Current main, unchanged:

Input	Reported today
requires(old(State<Int>) > 0)	[E174], caret on old, names old() and ensures()
decreases(old(State<Int>))	[E174], caret on old
requires(@Int.result > 0)	[E131], caret on @Int.result, names it and ensures()
requires(old(@Int.0) > 0)	[E005], caret on the @
ensures(old(@Int.0) > 0)	[E005], caret on the @

So the real gap is the argument shape, and it is not position-dependent. That also settles what the message must lead with: telling this author "move it into ensures()" would be actively misleading, because old(@Int.0) is still wrong there.

Before / after

Before:

[E005] Error at bump.vera, line 2, column 16:

      requires(old(@Int.0) > 0)
                   ^

  Unexpected "@" at this position. Expected one of: UPPER_IDENT

  The parser reached this position expecting one of the listed tokens; the
  token found does not begin any construct valid here.

  Fix:
    Replace the unexpected token with one of the expected tokens, or check
    for a missing delimiter (such as '}', ')', or ',') earlier in the construct.

  See: Chapter 10, "Formal Grammar"

After:

[E030] Error at bump.vera, line 2, column 12:

      requires(old(@Int.0) > 0)
               ^

  old() takes an effect reference, not an expression. Its only valid argument
  is the name of a stateful effect, as in old(State<Int>), and the call is only
  valid inside an ensures() clause.

  Vera has no mutable variables: a parameter slot or let binding holds one
  value for the whole call, so there is no separate before-value to ask for.
  Effect state is the only thing a call can change, which is why old() names an
  effect rather than wrapping an expression. The clause restriction follows
  from the same reasoning — requires() and decreases() are evaluated before the
  body runs, so every expression in them already observes the pre-state and
  old() would have nothing left to refer to.

  Fix:

    If you meant the value of a parameter, drop the wrapper —
    requires(@Int.0 > 0) says that directly, and the same slot reads
    identically in the postcondition. If you meant an effect's state before the
    call, name the effect inside an ensures() clause:

      ensures(new(State<Int>) == old(State<Int>) + 1)

  See: Chapter 7, Section 7.9.2 "State in Contracts"

Mechanism: (b), a parse-level diagnostic — because (a) is not available

Mechanism (a), parse liberally and reject in the checker, was tried first and measured, not assumed. Three grammar variants were built against real Lark:

Variant	Result
old_expr: "old" "(" expr ")"	Builds — but old(State<Int>) no longer parses. The < reads as a comparison and cmp_expr is non-associative, so the one form that is actually valid Vera breaks.
effect_ref and expr alternatives	GrammarError: Reduce/Reduce collision in Terminal('RPAR') between effect_ref: UPPER_IDENT and fn_call: UPPER_IDENT. Not expressible in LALR(1).
effect_ref | slot_ref | result_ref	Builds and catches the exact repro — but still [E005]s on old(@Int.0 + 1) and old(foo(())), and it would put a non-EffectRef argument into OldExpr, which eleven downstream modules pattern-match assuming an effect reference.

So (a) is a hard grammar constraint, not a matter of effort. The diagnostic is raised at parse, in the existing pattern-matching section of diagnose_lark_error — the same place [E001], [E002], and [E008] already rewrite a Lark failure into a Vera-shaped one. No AST change, no downstream blast radius.

The detector is deliberately narrow: it fires only when nothing but whitespace separates the failing token from an old( / new( immediately to its left — the exact position where the grammar demands an effect reference. A failure later in the argument, such as old(State<Int> > 0) whose real fault is the missing ), leaves a parsed token in between and falls through to [E005] rather than blaming old. keep_old( is excluded by an identifier-boundary check. Both UnexpectedToken and UnexpectedCharacters route through it, so old($x) is covered too.

Sibling verdict: @T.result needs no work

result_ref is in primary_expr, so @Int.result is grammatical everywhere an expression is and always reached the checker. requires(@Int.result > 0) already reports [E131] with the caret on the reference and a message naming both @T.result and ensures(). Left alone, as the brief allows — with caret/column tests added so it cannot regress quietly.

Also in this PR

• [E174] / [E175] gain the pre-state explanation the issue asks for: a requires() or decreases() clause is itself evaluated before the body runs, so every expression in it already observes the pre-state and the after-state new() names does not yet exist. The fix text adds the fact that closes off the obvious retry — a precondition cannot constrain effect state at all, because contract predicates must be pure and old()/new() are the only contract forms that name state.
• spec §7.9.2 now states both rules explicitly (effect-reference argument, ensures-only); §6.2.2 cross-references it, since Chapter 6 is where a reader looks for contract constructs.
• SKILL.md carries both rules beside the State-effects example, and E030/E031 in the error-code list.

Codes

E030 / E031, in the parse range that raises them, in a new E03x — Contract constructs (parse) sub-block. Two codes rather than one, matching the adjacent E174/E175 split for the same two constructs. Registered in ERROR_CODES and in vera/_since.py as 0.1.9. No version bump — this rides [Unreleased].

Testing

Written RED first: 15 of the new parse tests failed with the documented [E005]/[E006] before the fix.

• tests/test_parser.py::TestOldNewArgumentDiagnostic — 21 tests: error code, caret line and column, message content, all five diagnostic fields; requires, ensures, decreases, and nested inside a larger expression (requires(old(@Int.0) > 0 && true)); argument variants (slot ref, result ref, arbitrary expression, call, empty, invalid character, whitespace either side of the paren, argument on a later line); new(); and four over-fire guards.
• tests/test_checker_functions.py::TestContractStateFormPlacement — 6 tests pinning [E174]/[E175]/[E131] caret positions in requires and decreases, plus old()/new() inside ensures still accepted.
• tests/conformance/ch07_old_outside_ensures_rejected.vera, expected_error: E174. The parse-level case gets no conformance fixture on purpose: scripts/check_corpus_canonical.py runs format_source() over every conformance program, and a program that fails to parse cannot be formatted. The fixture header records that, and points at the parser tests.

Mutation-validated. Each piece of the new machinery was broken in turn and the named tests confirmed RED: feature off; identifier-boundary guard dropped; back-scan widened to the nearest ( instead of the first token; caret moved back onto the failing token; [E174] rationale reverted. Two mutations survived the first round — one because the mutation text was ineffective, one because test_identifier_ending_in_old_is_not_matched was passing for the wrong reason (keep_old(@Int.0 > ) fails at the ), nowhere near keep_old(, so it never exercised the guard). Both were fixed; the test now uses keep_old(> 0), which does fail on the first argument token. A third, dropping the open-paren check, is unfalsifiable by construction — after the old keyword the grammar accepts nothing but (, so the parser always fails on the very next token — and that is recorded in a code comment rather than papered over.

Gates

pytest tests/ -q -m "not stress" (8,505 passed, 92 skipped), mypy vera/ clean, ruff check clean (including --select S), conformance 170/170, examples 42/42, corpus canonical 218/218, diagnostic fields, doc counts, site assets, spec/SKILL/FAQ/README/HTML example checks, explicit encoding, limitations sync, version sync. Full pre-commit hook chain passed on commit.

Closes #1173

Summary by CodeRabbit

• New Features

  • Added dedicated error codes and clearer diagnostics for invalid old() and new() usage.
  • Clarified that both forms accept stateful effect references and are valid only in ensures clauses.

• Documentation

  • Updated the specification, FAQ, README, roadmap, changelog and testing guidance.
  • Documented revised test and conformance-suite totals.

• Tests

  • Added parser and contract-validation coverage for valid and invalid old(), new() and result-reference usage, including rejected contract placement.

[coderabbitai]

Note

Reviews paused

It 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 reviews.auto_review.auto_pause_after_reviewed_commits setting.

Use the following commands to manage reviews:

• @coderabbitai resume to resume automatic reviews.
• @coderabbitai review to trigger a single review.

Use the checkboxes below for quick actions:

• ▶️ Resume reviews
• 🔍 Trigger review

📝 Walkthrough

Walkthrough

The change adds dedicated old() and new() diagnostics, restricts their contract usage, adds parser and checker coverage, registers a conformance fixture, and updates related documentation and project metrics.

Changes

Contract-state diagnostics

Layer / File(s)	Summary
Contract rules and diagnostics spec/06-contracts.md, spec/07-effects.md, vera/errors.py, vera/checker/expressions.py, vera/_since.py	old() and new() now require typed effect references in ensures() clauses. E030 and E031 cover invalid arguments. E174 and E175 cover clause placement.
Parser and checker validation tests/test_parser.py, tests/test_checker_functions.py	Tests cover invalid arguments, clause placement, diagnostic details, valid ensures() usage, result references, and preserved generic parse failures.
Conformance validation tests/conformance/manifest.json, TESTING.md	The conformance manifest and validation documentation include ch07_old_outside_ensures_rejected with expected error E174.
Documentation and project metadata CHANGELOG.md, SKILL.md, vera/README.md, AGENTS.md, CLAUDE.md, README.md, FAQ.md, ROADMAP.md	Updated diagnostic references, conformance counts, test counts, validation commands, and fixture lists.

Estimated code review effort: 3 (Moderate) | ~20 minutes

Sequence Diagram(s)

sequenceDiagram
  participant Source
  participant Parser
  participant Checker
  participant DiagnosticSystem
  Source->>Parser: parse old() or new() usage
  Parser->>DiagnosticSystem: report E030 or E031 for expression arguments
  Parser->>Checker: pass valid contract syntax
  Checker->>DiagnosticSystem: validate ensures-only placement
  DiagnosticSystem-->>Checker: report E174 or E175

Loading

Possibly related issues

• old() outside ensures() reports a generic parse error that never mentions old() #1173: The PR directly addresses the generic diagnostic reported for old() outside ensures().

Possibly related PRs

• aallan/vera#826: Both changes modify old() and new() diagnostics in vera/checker/expressions.py and vera/errors.py.

Suggested labels: compiler, tests, spec, docs

🚥 Pre-merge checks | ✅ 7 | ❌ 1

❌ Failed checks (1 warning)

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

✅ Passed checks (7 passed)

Check name	Status	Explanation
Description Check	✅ Passed	Check skipped - CodeRabbit’s high-level summary is enabled.
Title check	✅ Passed	The title clearly identifies the main change: diagnosing invalid use of old() and new() with expression arguments.
Linked Issues check	✅ Passed	The changes address issue #1173 with dedicated diagnostics, correct caret locations, retained result handling, documentation, and regression tests.
Out of Scope Changes check	✅ Passed	The documentation, specification, registry, conformance, parser, and checker updates directly support the linked issue and stated diagnostic objectives.
Changelog Covers Public-Surface Changes	✅ Passed	CHANGELOG.md explicitly describes E030/E031 diagnostics, E174/E175 behaviour, and the spec §7.9.2 rules changed in vera/errors.py, checker expressions, and spec/06–07.
Spec And Implementation Move Together	✅ Passed	The spec now states effect-reference and ensures-only rules in §§6.2.2/7.9.2; the existing grammar, AST, checker, verifier, and codegen already implement those rules.
Diagnostics Carry An Error Code	✅ Passed	New parse diagnostics use E030/E031, pass those codes into Diagnostic, and register them in ERROR_CODES; changed placement diagnostics retain explicit E174/E175 codes.

✨ Finishing Touches 💡 1

📝 Generate docstrings 💡

• Create stacked PR
• Commit on current branch

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Commit unit tests in branch fix/1173-old-outside-ensures

---

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

[codecov]

Codecov Report

❌ Patch coverage is 91.89189% with 3 lines in your changes missing coverage. Please review.
✅ Project coverage is 93.78%. Comparing base (85c4b10) to head (120bb22).

Files with missing lines	Patch %	Lines
vera/errors.py	91.66%	3 Missing ⚠️

Additional details and impacted files

@@            Coverage Diff             @@
##             main    #1180      +/-   ##
==========================================
- Coverage   93.78%   93.78%   -0.01%     
==========================================
  Files          99       99              
  Lines       33600    33637      +37     
  Branches      458      458              
==========================================
+ Hits        31512    31546      +34     
- Misses       2075     2078       +3     
  Partials       13       13              

Flag	Coverage Δ
javascript	78.61% <ø> (ø)
python	95.49% <91.89%> (-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.

[aallan]

Adversarial review — verified against the diff and probed live

Verdict: correct as built. The reframing (argument shape, not clause placement) matches the grammar's reality, and the scan's conservatism points the right way at every edge I attacked:

• old(State<Int> > 0) (real fault: missing )) falls through to the generic diagnostic — verified the guard only fires on the first argument token.
• The keep_old( identifier boundary is real and its test now touches the guard (the mutation round's fix).
• The comment-blanking offset argument holds: blanking preserves length, and a comment wedged inside old( ... ) conservatively falls back to E005.
• The one candidate false positive I hypothesized — a user-defined fn old called in a body with a malformed argument — turns out to be unreachable as a misfire: probing shows old(5) in a body already fails at parse on main (the grammar reserves old(/new( in expression position everywhere), so E030's claim is the grammar's truth in every reachable context. What the probe did surface is a pre-existing quirk — fn old / fn new are declarable but uncallable — tracked separately, not a finding against this PR.
• E174/E175 fix-text strengthening is accurate (contract predicates are pure per §7.9.1, so a precondition genuinely cannot constrain effect state).

Checked and agreed with both brief deviations: §7.9.2 is the right spec_ref (old() appears nowhere in ch5), and a parse-failing conformance fixture is structurally impossible under the canonical-format gate, so the checker-level E174 fixture is the right shape.

[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 `@TESTING.md`:
- Around line 9-11: Reconcile the testing metrics in the TESTING.md overview by
recomputing the canonical total, passed, stress, skipped, and per-file counts so
all reported figures agree. Update every affected numeric occurrence in the
testing summary, including the total test count and 131-file aggregate, while
preserving the coverage and conformance metrics unless they are also
inconsistent.

🪄 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: d21694a2-33a0-4cac-8850-06eb479cef91

📥 Commits

Reviewing files that changed from the base of the PR and between 0640e04 and 099befa.

⛔ Files ignored due to path filters (6)

• docs/SKILL.md is excluded by !docs/**
• docs/index.html is excluded by !docs/**
• docs/index.md is excluded by !docs/**
• docs/llms-full.txt is excluded by !docs/**
• docs/llms.txt is excluded by !docs/**
• tests/conformance/ch07_old_outside_ensures_rejected.vera is excluded by !**/*.vera

📒 Files selected for processing (17)

• AGENTS.md
• CHANGELOG.md
• CLAUDE.md
• FAQ.md
• README.md
• ROADMAP.md
• SKILL.md
• TESTING.md
• spec/06-contracts.md
• spec/07-effects.md
• tests/conformance/manifest.json
• tests/test_checker_functions.py
• tests/test_parser.py
• vera/README.md
• vera/_since.py
• vera/checker/expressions.py
• vera/errors.py

🔗 Linked repositories identified

CodeRabbit considers these linked repositories for cross-repo context during reviews:

• aallan/vera-bench (manual)

[coderabbitai]

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 `@AGENTS.md`:
- Line 11: Correct the companion-module references in the conformance-suite
description in AGENTS.md: identify ch07_cross_module_contracts.vera with
ch07_cross_module_contracts_lib.vera, and ch08_cross_module_generic.vera with
ch08_cross_module_generic_lib.vera. Keep the surrounding suite and verification
guidance unchanged.

In `@FAQ.md`:
- Line 252: Update the test count in the FAQ entry from 8,558 to 8,635,
preserving the existing “including a 170-program conformance suite” wording.

In `@TESTING.md`:
- Around line 217-221: The documentation counts are stale across both referenced
files. In TESTING.md, add the skip-table rows for
ch07_old_outside_ensures_rejected and update the aggregate skip count to 63; in
CLAUDE.md, update the corpus count from 217 to 218. Ensure both values match the
current codebase.

🪄 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: 60a08468-fa16-4895-91ce-5d30f5dc3ce0

📥 Commits

Reviewing files that changed from the base of the PR and between 099befa and 855a514.

⛔ Files ignored due to path filters (6)

• docs/SKILL.md is excluded by !docs/**
• docs/index.html is excluded by !docs/**
• docs/index.md is excluded by !docs/**
• docs/llms-full.txt is excluded by !docs/**
• docs/llms.txt is excluded by !docs/**
• tests/conformance/ch07_old_outside_ensures_rejected.vera is excluded by !**/*.vera

📒 Files selected for processing (17)

• AGENTS.md
• CHANGELOG.md
• CLAUDE.md
• FAQ.md
• README.md
• ROADMAP.md
• SKILL.md
• TESTING.md
• spec/06-contracts.md
• spec/07-effects.md
• tests/conformance/manifest.json
• tests/test_checker_functions.py
• tests/test_parser.py
• vera/README.md
• vera/_since.py
• vera/checker/expressions.py
• vera/errors.py

🔗 Linked repositories identified

CodeRabbit considers these linked repositories for cross-repo context during reviews:

• aallan/vera-bench (manual)

[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 `@CLAUDE.md`:
- Around line 61-63: Update the corpus-program count in AGENTS.md from 217 to
218, matching the existing count used by check_corpus_canonical.py documentation
in CLAUDE.md.

🪄 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: 0bf4979c-c26f-4b4b-bade-0a58e3938d29

📥 Commits

Reviewing files that changed from the base of the PR and between 855a514 and 7dc4664.

⛔ Files ignored due to path filters (6)

• docs/SKILL.md is excluded by !docs/**
• docs/index.html is excluded by !docs/**
• docs/index.md is excluded by !docs/**
• docs/llms-full.txt is excluded by !docs/**
• docs/llms.txt is excluded by !docs/**
• tests/conformance/ch07_old_outside_ensures_rejected.vera is excluded by !**/*.vera

📒 Files selected for processing (17)

• AGENTS.md
• CHANGELOG.md
• CLAUDE.md
• FAQ.md
• README.md
• ROADMAP.md
• SKILL.md
• TESTING.md
• spec/06-contracts.md
• spec/07-effects.md
• tests/conformance/manifest.json
• tests/test_checker_functions.py
• tests/test_parser.py
• vera/README.md
• vera/_since.py
• vera/checker/expressions.py
• vera/errors.py

🔗 Linked repositories identified

CodeRabbit considers these linked repositories for cross-repo context during reviews:

• aallan/vera-bench (manual)

[coderabbitai]

Actionable comments posted: 2

🤖 Prompt for all review comments with AI agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

Inline comments:
In `@AGENTS.md`:
- Line 11: Correct the conformance-suite description in AGENTS.md so it no
longer claims only two programs contain imports. State that most programs are
self-contained while accurately acknowledging all imported-fixture exceptions,
including the additional Chapter 7, Chapter 8, and Chapter 9 cases; preserve the
existing verification-level and negative-fixture guidance.

In `@tests/test_checker_functions.py`:
- Around line 707-718: Add a companion test near
test_new_in_requires_carets_the_construct that places new(State<Int>) in a
decreases() clause, then filter for E175 and assert the diagnostic’s construct
caret location, including its expected line and column.

🪄 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: 84ec0945-4feb-412c-8ef8-ddebf580a568

📥 Commits

Reviewing files that changed from the base of the PR and between 7dc4664 and 1b54347.

⛔ Files ignored due to path filters (6)

• docs/SKILL.md is excluded by !docs/**
• docs/index.html is excluded by !docs/**
• docs/index.md is excluded by !docs/**
• docs/llms-full.txt is excluded by !docs/**
• docs/llms.txt is excluded by !docs/**
• tests/conformance/ch07_old_outside_ensures_rejected.vera is excluded by !**/*.vera

📒 Files selected for processing (17)

• AGENTS.md
• CHANGELOG.md
• CLAUDE.md
• FAQ.md
• README.md
• ROADMAP.md
• SKILL.md
• TESTING.md
• spec/06-contracts.md
• spec/07-effects.md
• tests/conformance/manifest.json
• tests/test_checker_functions.py
• tests/test_parser.py
• vera/README.md
• vera/_since.py
• vera/checker/expressions.py
• vera/errors.py

🔗 Linked repositories identified

CodeRabbit considers these linked repositories for cross-repo context during reviews:

• aallan/vera-bench (manual)

[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/checker/expressions.py`:
- Around line 1306-1316: Extract the duplicated diagnostic fix text used by
_check_old_expr and _check_new_expr into one shared constant, then pass that
constant to both diagnostic call sites. Preserve the existing wording exactly
and remove the separate inline fix strings.

🪄 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: ce7eb37d-c25f-4b2c-ac70-731e1b40d76b

📥 Commits

Reviewing files that changed from the base of the PR and between 1b54347 and 7deffbb.

⛔ Files ignored due to path filters (6)

• docs/SKILL.md is excluded by !docs/**
• docs/index.html is excluded by !docs/**
• docs/index.md is excluded by !docs/**
• docs/llms-full.txt is excluded by !docs/**
• docs/llms.txt is excluded by !docs/**
• tests/conformance/ch07_old_outside_ensures_rejected.vera is excluded by !**/*.vera

📒 Files selected for processing (17)

• AGENTS.md
• CHANGELOG.md
• CLAUDE.md
• FAQ.md
• README.md
• ROADMAP.md
• SKILL.md
• TESTING.md
• spec/06-contracts.md
• spec/07-effects.md
• tests/conformance/manifest.json
• tests/test_checker_functions.py
• tests/test_parser.py
• vera/README.md
• vera/_since.py
• vera/checker/expressions.py
• vera/errors.py

🔗 Linked repositories identified

CodeRabbit considers these linked repositories for cross-repo context during reviews:

• aallan/vera-bench (manual)