audit: extract addressMask constant, fix silent fallback, correct docstring#672
Conversation
…string Extract `addressMask` ((2^160)-1) as a public constant in ContractSpec.lean, replacing 15 scattered inline literals across ContractSpec, ASTDriver, and proof terms in Expr.lean. Interpreter.lean keeps a private `addressModulus` (2^160) to avoid importing ContractSpec; a new CI check validates both stay in sync. Also: - check_selectors.py: emit stderr warning when yul-ast/ falls back to ContractSpec specs (was silent — audit transparency gap) - ABI.lean: fix misleading docstring on renderSpecialEntry (claimed "always returns some" but code has a defensive guard) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
![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.
| # Address mask constant sync | ||
| # --------------------------------------------------------------------------- | ||
|
|
||
| _ADDRESS_MASK: int = (2**160) - 1 |
There was a problem hiding this comment.
Unused _ADDRESS_MASK constant never referenced in check
Low Severity
_ADDRESS_MASK is defined at module scope but never referenced by check_address_mask_sync() or anything else. The analogous _ERROR_STRING_SELECTOR_SHIFTED constant is used for value validation in check_error_selector_sync(). This looks like the value-validation step was intended but omitted, leaving dead code and a weaker check than its error-selector counterpart.
Additional Locations (1)
2 participants
Summary
addressMask((2^160)-1) as a public constant inContractSpec.lean, replacing 15 inline literals across compiler codegen, AST driver, and proof termscheck_selectors.py:check_address_mask_sync()validates consistency betweenContractSpec.addressMaskandInterpreter.addressModuluscheck_selectors.pynow emits a stderr warning when yul-ast/ is validated against ContractSpec specs instead of ASTSpecs (was completely silent — audit transparency gap)ABI.lean:renderSpecialEntry(claimed "always returnssome" but code has a defensivenonebranch)What changed
Compiler/ContractSpec.leanaddressMask; 4 inline literals replacedCompiler/ASTDriver.leanaddressMaskadded to open listCompiler/Proofs/IRGeneration/Expr.leanCompiler/Interpreter.leanaddressModulusto canonical constantCompiler/ABI.leanscripts/check_selectors.pycheck_address_mask_sync(); silent fallback → stderr warningAUDIT.mdaddressMaskdesign decision and CI checkTest 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
Primarily refactors repeated address-masking literals into a shared constant and adds CI/doc updates; behavior should be unchanged aside from clearer CI warnings.
Overview
Introduces a canonical
addressMaskconstant inContractSpec.leanand replaces multiple inline(2^160)-1literals across the ContractSpec codegen paths, the AST driver’s constructor arg loading, and IR proof fixtures to keep address normalization consistent.Strengthens CI/audit transparency by extending
scripts/check_selectors.pywith an address mask/modulus sync check (ContractSpec vs Interpreter) and emitting a stderr warning whenyul-ast/validation falls back to ContractSpec specs due to missing/emptyASTSpecs.lean. Also fixes a misleading docstring inABI.leanaboutrenderSpecialEntryand updatesAUDIT.mdto document the new shared constant and CI coverage.Written by Cursor Bugbot for commit dec37ba. This will update automatically on new commits. Configure here.