Reserve keyword function names; carve out host-invoked entry points (E153) - #1194
Conversation
…E153) Lark's contextual lexer re-lexes `assert`, `assume`, `forall`, `exists`, `match`, `if`, `let`, `fn`, `true` and `false` as ordinary identifiers after `fn`, so each declares cleanly — and none can be written in expression position, where the spelling is always the keyword: a bare `match(3)` does not parse at all ([E005]), and `assert(3)` / `assume(3)` are read as the statement forms and collide ([E121] plus [E172]/[E173]). Every one is a declarable trap, so E153 now refuses it at the declaration, extending the #1181 gate for the contract state forms under the same one-canonical-form rule as E151 and E152. `handle` is carved out: `public fn handle(@request -> @response)` is the host-invoked `vera serve` / `wasi:http` entry point (spec §9.5.6), so being uncallable from Vera source does not make it dead code. The reserved set is derived as (state forms) | (keywords) - (host-invoked), each piece named and commented, so a future host-invoked entry point joins the carve-out deliberately. Breaking: a module-qualified `mod::match(...)` parses through the module-call rule rather than any keyword rule, so a module export under one of these names was callable cross-module (and only cross-module) — probed on the pre-fix tree, the shape checked and ran. Such an export must now be renamed; the breakage is loud and located at the module's declaration. The E153 rationale branches with the reason (a keyword is not described as a contract state form) while the fix stays "rename" on both. New conformance program ch05_reserved_keyword_fn_rejected (176, was 175). Co-Authored-By: Claude <noreply@anthropic.invalid>
📝 WalkthroughWalkthroughThe checker now rejects reserved grammar-keyword function names with E153, while allowing ChangesReserved function name validation
Estimated code review effort: 3 (Moderate) | ~25 minutes Sequence Diagram(s)sequenceDiagram
participant FunctionDeclaration
participant _register_all
participant _check_reserved_fn_name
participant E153Diagnostic
FunctionDeclaration->>_register_all: register function declaration
_register_all->>_check_reserved_fn_name: validate function name
_check_reserved_fn_name->>E153Diagnostic: emit category-specific E153
Possibly related PRs
Suggested labels: 🚥 Pre-merge checks | ✅ 8✅ Passed checks (8 passed)
✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Comment |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #1194 +/- ##
=======================================
Coverage 93.79% 93.79%
=======================================
Files 99 99
Lines 34126 34134 +8
Branches 458 458
=======================================
+ Hits 32008 32017 +9
+ Misses 2105 2104 -1
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:
|
Adversarial review recordVerdict: implementation matches the #1187 decision exactly; no defects found. Checks performed on this head (2f1dc4a): Set membership traced to the recorded probe. The issue's 33-candidate probe found eleven declarable-but-uncallable names; the decision was reject-ten-plus-carve-out-handle. Three doors probed live on this branch:
Decision-trail cross-check. The issue's second maintainer comment (module-qualified route) is honoured: the whole identifier is reserved and the CHANGELOG carries the Breaking note for the Spec §5.2 states both groups, the whole-identifier rule ( Rebase reconciliation (fixed in this head, worth flagging for the record): the branch as originally prepared carried stale documentation numbers — conformance totals left at 175 across ~13 sites, and a |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 3
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
vera/checker/registration.py (1)
330-374: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winCorrect the E153 reachability rationale.
Both branches state that the declaration cannot be reached “from anywhere in the program”. Module-qualified calls could reach exported
oldand keyword-named functions before this reservation. State that unqualified calls cannot reach the declaration, and that E153 deliberately closes the previously half-usable module-qualified route.Proposed correction
- f"resolves to a function, so this declaration could not " - f"be reached from anywhere in the program — it is dead " - f"code the compiler would otherwise accept in silence." + f"resolves to a function. An unqualified call therefore " + f"cannot reach this declaration. Module-qualified calls " + f"could reach an exported declaration, so Vera reserves " + f"the name rather than leaving it half-usable." ... - f"never resolves to a function. This declaration could " - f"not be reached from anywhere in the program — it is " - f"dead code the compiler would otherwise accept in " - f"silence. Vera provides exactly one way to express each " + f"never resolves to a function. An unqualified call " + f"therefore cannot reach this declaration. " + f"Module-qualified calls could reach an exported " + f"declaration, so Vera reserves the name rather than " + f"leaving it half-usable. Vera provides exactly one way " + f"to express each "🤖 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/checker/registration.py` around lines 330 - 374, Update the E153 rationale and fix text in both branches of the registration logic to state that unqualified calls cannot reach the declaration, rather than claiming it is unreachable from anywhere in the program. Explicitly note that module-qualified calls could previously reach exported reserved-name functions and that E153 closes this formerly half-usable route, while preserving the existing rename guidance.
🤖 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 `@CHANGELOG.md`:
- Around line 36-38: Correct the conformance-program count in the changelog
entry for ch05_reserved_keyword_fn_rejected from “(175, was 174)” to “(176, was
175)”, without changing the separate ch08_reserved_vera_prefix_rejected count.
In `@tests/test_checker_modules.py`:
- Around line 1249-1253: Update the test around KEYWORDS to compare
set(KEYWORDS) against _KEYWORD_FN_NAMES - _HOST_INVOKED_FN_NAMES, so
checker-reserved keywords require corresponding E153 coverage while preserving
the intentional omission of handle.
In `@vera/README.md`:
- Line 83: Update the README table entry for registration.py to remove the
leading spaces from inside the inline code span, keeping any intended
indentation outside the span so markdownlint MD038 passes.
---
Outside diff comments:
In `@vera/checker/registration.py`:
- Around line 330-374: Update the E153 rationale and fix text in both branches
of the registration logic to state that unqualified calls cannot reach the
declaration, rather than claiming it is unreachable from anywhere in the
program. Explicitly note that module-qualified calls could previously reach
exported reserved-name functions and that E153 closes this formerly half-usable
route, while preserving the existing rename guidance.
🪄 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: effc42b1-9fd9-401d-ad9e-a31fdd036b8b
⛔ Files ignored due to path filters (6)
docs/SKILL.mdis excluded by!docs/**docs/index.htmlis excluded by!docs/**docs/index.mdis excluded by!docs/**docs/llms-full.txtis excluded by!docs/**docs/llms.txtis excluded by!docs/**tests/conformance/ch05_reserved_keyword_fn_rejected.verais excluded by!**/*.vera
📒 Files selected for processing (14)
AGENTS.mdCHANGELOG.mdCLAUDE.mdFAQ.mdREADME.mdROADMAP.mdSKILL.mdTESTING.mdspec/05-functions.mdtests/conformance/manifest.jsontests/test_checker_modules.pyvera/README.mdvera/checker/modules.pyvera/checker/registration.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
|
@coderabbitai On the outside-diff finding at |
|
Tip For best results, initiate chat on the files or code changes.
It now distinguishes unreachable unqualified calls from the former reachable ✏️ Learnings added
You are interacting with an AI system. |
1 participant
Summary
A function named after a grammar keyword is now rejected at its declaration site with
E153, extending the #1181 gate (contract state formsold/new) to the keyword class Lark's contextual lexer admits as a function name:assert,assume,forall,exists,match,if,let,fn,true,false.Each of these declares cleanly today — the contextual lexer re-lexes the keyword as an ordinary identifier after
fn— and none can ever be called: in expression position the spelling is always the keyword, so a barematch(3)fails to parse ([E005]) andassert(3)/assume(3)are read as the statement forms and collide ([E121]+[E172]/[E173]). Every one is a declarable trap. The reservation refuses the mistake at its source, under the same one-canonical-form rule asE151(built-in functions),E152(built-in effects), and #1181.handleis carved out.public fn handle(@Request -> @Response)is the host-invokedvera serve/wasi:httpentry point (spec §9.5.6,examples/http_server.vera) — being uncallable from Vera source does not make it dead code. The reserved set is derived as(state forms | keywords) − host-invoked, three named frozensets with the justification recorded on each, so a future host-invoked entry point joins the carve-out deliberately rather than by silently shrinking the keyword list.Breaking: a module-qualified
mod::match(...)parses through the module-call rule rather than any keyword rule, so a module export under one of these names was callable cross-module (and only cross-module) — probed on the pre-fix tree, the shape checked and ran. Such an export must now be renamed; the breakage is loud and located at the module's declaration. Modules surface the rejection into their importers (the establishedE151–E154surfacing list).Mechanism
vera/checker/registration.py:_RESERVED_FN_NAMESrebuilt from_STATE_FORM_FN_NAMES | _KEYWORD_FN_NAMES − _HOST_INVOKED_FN_NAMES;_check_reserved_fn_namebranches theE153rationale by which piece matched (a keyword is not described as a "contract state form") while the fix stays "rename" on both. Recurses intowhere-helpers as before.vera/checker/modules.py: comment updated — theE153importer-surfacing rationale now covers both halves.ch05_reserved_keyword_fn_rejected(expected_error: E153; conformance 176, was 175) and the hand-list updates in CLAUDE/AGENTS/TESTING.tests/test_checker_modules.py(104 total): each of the ten keywords at top level,where-helper, and module-surfaced positions; thehandlecarve-out at all three positions; probe records in docstrings for why the set is exactly this.Verification
mypyclean.fn match→E153at the declaration;fn handlestandalone → clean; a module exportingfn let→E153surfaced into the importer, located at the module's own file/line.Closes #1187
🤖 Generated with Claude Code
Summary by CodeRabbit
Bug Fixes
olderandmatched.handleentry point remains permitted.Documentation