audit: extract errorStringSelectorWord constant, add CI sync check#671
Conversation
The Error(string) selector (0x08c379a0 << 224) was duplicated as magic hex literals in 6 locations across 3 files. Extract a public constant `errorStringSelectorWord` in ContractSpec.lean and reference it from `revertWithMessage` and the 4 concrete IR proof terms in Expr.lean. Interpreter.lean keeps a private decimal copy to avoid importing ContractSpec; a new CI check in check_selectors.py validates both values 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.
| f"Interpreter.revertSelectorWord: value {interp_val} does not " | ||
| f"match canonical errorStringSelectorWord " | ||
| f"({_ERROR_STRING_SELECTOR_SHIFTED})" | ||
| ) |
There was a problem hiding this comment.
CI sync check silently passes on missing Interpreter definition
Medium Severity
check_error_selector_sync silently passes when _INTERPRETER_RE fails to match in Interpreter.lean (e.g., if the definition is renamed, reformatted, or removed). Unlike the ContractSpec branch which reports an error when its regex doesn't match, the Interpreter branch simply does nothing when m2 is None. This contradicts the stated guarantee in AUDIT.md that "CI validates both values match" and is inconsistent with how other sync checks (e.g., check_builtin_list_sync.py) handle missing definitions.
Additional Locations (1)
2 participants
Summary
errorStringSelectorWord(0x08c379a0 << 224) as a public constant inContractSpec.lean, replacing 5 inline magic hex literals across compiler and proof filesInterpreter.leankeeps a private decimal copy (avoiding ContractSpec import); CI now validates both values stay in synccheck_selectors.py:check_error_selector_sync()validates the constant in both ContractSpec and InterpreterWhat changed
Compiler/ContractSpec.leanerrorStringSelectorWord;revertWithMessageuses itCompiler/Proofs/IRGeneration/Expr.leanCompiler/Interpreter.leanscripts/check_selectors.pycheck_error_selector_sync()validates constant consistencyAUDIT.mdTest plan
check_selectors.pypasses locally (includes new sync check)check_doc_counts.pypasses locally🤖 Generated with Claude Code
Note
Low Risk
Mostly constant deduplication plus an additional CI consistency check; behavior should remain identical aside from preventing accidental selector drift.
Overview
Extracts a shared
errorStringSelectorWordconstant for theError(string)ABI selector (shifted into a 32-byte word) and replaces multiple inline magic literals inContractSpec.revertWithMessageand concrete IR proof revert snippets.Keeps the interpreter’s private copy but documents it as a duplicate of the canonical value, and extends
scripts/check_selectors.pyto CI-validate that theContractSpecandInterpreterconstants remain in sync;AUDIT.mdis updated to record this design decision and the new check.Written by Cursor Bugbot for commit b0fef29. This will update automatically on new commits. Configure here.