From 416aa90c0ada20c4f9603253f2623643ec86bdfc Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 22 Feb 2026 04:31:04 +0100 Subject: [PATCH] audit: extract selectorShift constant, add CI sync check 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 --- AUDIT.md | 3 +- Compiler/Codegen.lean | 7 +++- Compiler/ContractSpec.lean | 7 +++- Compiler/Proofs/YulGeneration/Builtins.lean | 2 ++ scripts/check_selectors.py | 39 +++++++++++++++++++++ 5 files changed, 55 insertions(+), 3 deletions(-) diff --git a/AUDIT.md b/AUDIT.md index aed1ab900..7620811ce 100644 --- a/AUDIT.md +++ b/AUDIT.md @@ -102,6 +102,7 @@ EDSL uses **wrapping** `mod 2^256` arithmetic. Solidity uses **checked** arithme | Shared `internalFunctionPrefix` | `"internal_"` prefix for generated Yul internal function names defined once; CI validates no user function name collides with this prefix | | Shared `errorStringSelectorWord` | `Error(string)` selector (`0x08c379a0 << 224`) defined once in ContractSpec; reused in revert codegen and proof terms. Interpreter keeps a private copy (decimal) to avoid importing ContractSpec; CI validates both values match | | Shared `addressMask` | 160-bit address mask `(2^160)-1` defined once in ContractSpec; used across codegen (ContractSpec, ASTDriver) and proof terms (Expr.lean). Interpreter keeps private `addressModulus` (`2^160`); CI validates both | +| Shared `selectorShift` | Selector shift amount (`224` bits) defined in ContractSpec; Codegen and proof Builtins keep private copies to avoid cross-module imports. CI validates all three definitions match | ## Known risks @@ -136,7 +137,7 @@ EDSL uses **wrapping** `mod 2^256` arithmetic. Solidity uses **checked** arithme 30+ scripts enforce consistency between proofs, tests, and documentation. Key checks: - `check_yul_compiles.py`: All generated Yul compiles with solc; legacy/AST bytecode diff baseline -- `check_selectors.py` / `check_selector_fixtures.py`: Selector cross-validation (both ContractSpec and ASTSpecs; cross-checks signature equivalence; reserved prefix collision check; Error(string) selector constant sync; address mask constant sync) +- `check_selectors.py` / `check_selector_fixtures.py`: Selector cross-validation (both ContractSpec and ASTSpecs; cross-checks signature equivalence; reserved prefix collision check; Error(string) selector constant sync; address mask constant sync; selector shift constant sync) - `check_doc_counts.py`: Theorem/test counts consistent across all docs - `check_lean_warning_regression.py`: Zero-warning policy - `check_axiom_locations.py`: All axioms documented in AXIOMS.md diff --git a/Compiler/Codegen.lean b/Compiler/Codegen.lean index 6d742a003..01fefb7f4 100644 --- a/Compiler/Codegen.lean +++ b/Compiler/Codegen.lean @@ -76,11 +76,16 @@ private def defaultDispatchCase (dispatchBody fb.payable "fallback()" fb.body) ]] +-- Selector shift amount (224 = 256 - 32). +-- Canonical definition: Compiler.ContractSpec.selectorShift +-- Duplicated here to avoid importing ContractSpec into the lightweight Codegen module. +private def selectorShift : Nat := 224 + def buildSwitch (funcs : List IRFunction) (fallback : Option IREntrypoint := none) (receive : Option IREntrypoint := none) : YulStmt := - let selectorExpr := YulExpr.call "shr" [YulExpr.lit 224, YulExpr.call "calldataload" [YulExpr.lit 0]] + let selectorExpr := YulExpr.call "shr" [YulExpr.lit selectorShift, YulExpr.call "calldataload" [YulExpr.lit 0]] let cases := funcs.map (fun fn => let body := dispatchBody fn.payable s!"{fn.name}()" ([calldatasizeGuard fn.params.length] ++ fn.body) (fn.selector, body) diff --git a/Compiler/ContractSpec.lean b/Compiler/ContractSpec.lean index e3c38a210..d3129b10f 100644 --- a/Compiler/ContractSpec.lean +++ b/Compiler/ContractSpec.lean @@ -446,6 +446,11 @@ def errorStringSelectorWord : Nat := 0x08c379a0 * (2 ^ 224) so the upper 96 bits must be cleared. -/ def addressMask : Nat := (2 ^ 160) - 1 +/-- Selector shift: function selectors occupy the top 4 bytes of a 32-byte + EVM word, so calldata word 0 is right-shifted by 224 bits to extract + the selector, and error hashes are left-shifted by 224 bits to pack them. -/ +def selectorShift : Nat := 224 + def revertWithMessage (message : String) : List YulStmt := let bytes := bytesFromString message let len := bytes.length @@ -1283,7 +1288,7 @@ private def revertWithCustomError (dynamicSource : DynamicDataSource) let hashStmt := YulStmt.let_ "__err_hash" (YulExpr.call "keccak256" [YulExpr.ident "__err_ptr", YulExpr.lit sigBytes.length]) let selectorStmt := YulStmt.let_ "__err_selector" - (YulExpr.call "shl" [YulExpr.lit 224, YulExpr.call "shr" [YulExpr.lit 224, YulExpr.ident "__err_hash"]]) + (YulExpr.call "shl" [YulExpr.lit selectorShift, YulExpr.call "shr" [YulExpr.lit selectorShift, YulExpr.ident "__err_hash"]]) let selectorStore := YulStmt.expr (YulExpr.call "mstore" [YulExpr.lit 0, YulExpr.ident "__err_selector"]) let headSize := errorDef.params.length * 32 let tailInit := YulStmt.let_ "__err_tail" (YulExpr.lit headSize) diff --git a/Compiler/Proofs/YulGeneration/Builtins.lean b/Compiler/Proofs/YulGeneration/Builtins.lean index ce31bd2e8..0438ae279 100644 --- a/Compiler/Proofs/YulGeneration/Builtins.lean +++ b/Compiler/Proofs/YulGeneration/Builtins.lean @@ -9,6 +9,8 @@ abbrev evmModulus : Nat := Compiler.Proofs.evmModulus def selectorModulus : Nat := 2 ^ 32 +-- Canonical definition: Compiler.ContractSpec.selectorShift +-- Duplicated here to avoid importing ContractSpec into the proof module. def selectorShift : Nat := 224 def selectorWord (selector : Nat) : Nat := diff --git a/scripts/check_selectors.py b/scripts/check_selectors.py index 31fa6cbb1..ab00591c6 100755 --- a/scripts/check_selectors.py +++ b/scripts/check_selectors.py @@ -10,6 +10,7 @@ 6) No function name uses the reserved ``internal_`` prefix (Yul namespace collision). 7) Error(string) selector constant sync between ContractSpec and Interpreter. 8) Address mask constant sync between ContractSpec and Interpreter. +9) Selector shift constant sync between ContractSpec, Codegen, and Builtins. """ from __future__ import annotations @@ -27,6 +28,8 @@ IR_EXPR_FILE = ROOT / "Compiler" / "Proofs" / "IRGeneration" / "Expr.lean" CONTRACT_SPEC_FILE = ROOT / "Compiler" / "ContractSpec.lean" INTERPRETER_FILE = ROOT / "Compiler" / "Interpreter.lean" +CODEGEN_FILE = ROOT / "Compiler" / "Codegen.lean" +BUILTINS_FILE = ROOT / "Compiler" / "Proofs" / "YulGeneration" / "Builtins.lean" YUL_DIR_LEGACY = ("yul", YUL_DIR) YUL_DIR_AST = ("yul-ast", ROOT / "compiler" / "yul-ast") @@ -561,6 +564,39 @@ def check_address_mask_sync() -> List[str]: return errors +# --------------------------------------------------------------------------- +# Selector shift constant sync +# --------------------------------------------------------------------------- + +_SELECTOR_SHIFT_RE = re.compile( + r"def\s+selectorShift\s*:\s*Nat\s*:=\s*224" +) + + +def check_selector_shift_sync() -> List[str]: + """Verify the selectorShift constant (224) is consistent across files. + + Checks that ContractSpec, Codegen, and Builtins all define selectorShift = 224. + """ + errors: List[str] = [] + targets = [ + ("ContractSpec.lean", CONTRACT_SPEC_FILE), + ("Codegen.lean", CODEGEN_FILE), + ("Builtins.lean", BUILTINS_FILE), + ] + for label, path in targets: + if not path.exists(): + errors.append(f"Missing {path}") + continue + text = path.read_text(encoding="utf-8") + if not _SELECTOR_SHIFT_RE.search(text): + errors.append( + f"{label}: missing or changed selectorShift definition " + f"(expected: def selectorShift : Nat := 224)" + ) + return errors + + def main() -> None: if not SPEC_FILE.exists(): die(f"Missing specs file: {SPEC_FILE}") @@ -619,6 +655,9 @@ def main() -> None: # Validate address mask constant consistency. errors.extend(check_address_mask_sync()) + # Validate selector shift constant consistency. + errors.extend(check_selector_shift_sync()) + report_errors(errors, "Selector checks failed") print("Selector checks passed.")