audit: extract selectorShift constant, add CI sync check

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

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)

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)

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 :=

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.")