audit: extract selectorShift constant, add CI sync check#673
Conversation
The selector shift amount (224 = 256 - 32 bits) was hardcoded as bare literals in Codegen.buildSwitch and ContractSpec.revertWithCustomError, while the proof module had its own named `selectorShift` in Builtins.lean. Define the canonical constant in ContractSpec.lean and named copies in Codegen.lean and Builtins.lean (avoiding cross-module imports). A new CI check validates all three definitions stay in sync. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
There was a problem hiding this comment.
Cursor Bugbot has reviewed your changes and found 1 potential issue.
Bugbot Autofix is OFF. To automatically fix reported issues with Cloud Agents, enable Autofix in the Cursor dashboard.
|
|
||
| _SELECTOR_SHIFT_RE = re.compile( | ||
| r"def\s+selectorShift\s*:\s*Nat\s*:=\s*224" | ||
| ) |
There was a problem hiding this comment.
Regex lacks trailing word boundary after value
Low Severity
_SELECTOR_SHIFT_RE ends with the bare literal 224 without a trailing word boundary (\b) or end-of-line anchor. Since re.search is used, a value like 2240 or 22400 would still match because 224 appears as a prefix. This undermines the sync check's purpose — it would silently accept an incorrect shift value. Adding \b or $ after 224 would ensure an exact match.
2 participants
Summary
selectorShift(224) as a named constant across ContractSpec, Codegen, and proof Builtins — replaces bare224literals in dispatcher codegen and custom error encodingcheck_selectors.py:check_selector_shift_sync()validates all three definitions matchWhat changed
Compiler/ContractSpec.leanselectorShift; used inrevertWithCustomErrorCompiler/Codegen.leanselectorShift; used inbuildSwitchCompiler/Proofs/YulGeneration/Builtins.leanscripts/check_selectors.pycheck_selector_shift_sync()validates 3-way consistencyAUDIT.mdTest plan
check_selectors.pypasses locally (includes new sync check)check_doc_counts.pypasses locallycheck_builtin_list_sync.pypasses locally🤖 Generated with Claude Code
Note
Low Risk
Constant extraction + CI check only; behavior should be unchanged aside from reducing risk of future constant drift in selector/custom-error encoding.
Overview
Extracts
selectorShift(=224) into a named constant inContractSpec, and mirrors it inCodegenand proofBuiltins, replacing hard-coded224literals in selector extraction and custom error selector packing.Extends
scripts/check_selectors.pywith a new CI validation to ensureselectorShiftstays consistent across those three modules, and updatesAUDIT.mdto document the shared-constant decision and the new check.Written by Cursor Bugbot for commit 416aa90. This will update automatically on new commits. Configure here.