audit: extract errorStringSelectorWord constant, add CI sync check

AUDIT.md

@@ -100,6 +100,7 @@ EDSL uses **wrapping** `mod 2^256` arithmetic. Solidity uses **checked** arithme
 | Non-short-circuit `logicalAnd`/`logicalOr` | Compiled to EVM bitwise `and`/`or` — both operands always evaluated. Simpler codegen; no side-effecting expressions in current DSL |
 | Shared `Selector.runKeccak` | Single keccak subprocess helper shared between ContractSpec and AST compilation paths; eliminates duplicated subprocess handling |
 | 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 |
 
 ## Known risks
 
@@ -134,7 +135,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)
+- `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)
 - `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/ContractSpec.lean

@@ -436,13 +436,17 @@ def wordFromBytes (bs : List UInt8) : Nat :=
   let padded := bs ++ List.replicate (32 - bs.length) (0 : UInt8)
   padded.foldl (fun acc b => acc * 256 + b.toNat) 0
 
+/-- The 4-byte selector for `Error(string)` (keccak256("Error(string)")[0:4]),
+    left-shifted to fill a 32-byte EVM word.  This is 0x08c379a0 << 224.
+    Used in `revertWithMessage` (compiler) and concrete IR proofs. -/
+def errorStringSelectorWord : Nat := 0x08c379a0 * (2 ^ 224)
+
 def revertWithMessage (message : String) : List YulStmt :=
   let bytes := bytesFromString message
   let len := bytes.length
   let paddedLen := ((len + 31) / 32) * 32
-  let selectorShifted : Nat := 0x08c379a0 * (2 ^ 224)
   let header := [
-    YulStmt.expr (YulExpr.call "mstore" [YulExpr.lit 0, YulExpr.hex selectorShifted]),
+    YulStmt.expr (YulExpr.call "mstore" [YulExpr.lit 0, YulExpr.hex errorStringSelectorWord]),
     YulStmt.expr (YulExpr.call "mstore" [YulExpr.lit 4, YulExpr.lit 32]),
     YulStmt.expr (YulExpr.call "mstore" [YulExpr.lit 36, YulExpr.lit len])
   ]

Compiler/Interpreter.lean

@@ -77,6 +77,8 @@ def extractMappingChanges (before after : ContractState) (keys : List (Nat × Ad
     if oldVal ≠ newVal then some (slot, key, newVal) else none
 
 -- EVM revert data for Error(string) uses selector 0x08c379a0 in the first 32 bytes.
+-- Canonical definition: Compiler.ContractSpec.errorStringSelectorWord
+-- Duplicated here to avoid importing ContractSpec into the interpreter.
 private def revertSelectorWord : Nat :=
   3963877391197344453575983046348115674221700746820753546331534351508065746944
 

Compiler/Proofs/IRGeneration/Expr.lean

@@ -272,7 +272,7 @@ def safeCounterOverflowRevert : List YulStmt :=
   [
     YulStmt.expr (YulExpr.call "mstore" [
       YulExpr.lit 0,
-      YulExpr.hex 0x08c379a000000000000000000000000000000000000000000000000000000000
+      YulExpr.hex errorStringSelectorWord
     ]),
     YulStmt.expr (YulExpr.call "mstore" [YulExpr.lit 4, YulExpr.lit 32]),
     YulStmt.expr (YulExpr.call "mstore" [YulExpr.lit 36, YulExpr.lit 21]),
@@ -287,7 +287,7 @@ def safeCounterUnderflowRevert : List YulStmt :=
   [
     YulStmt.expr (YulExpr.call "mstore" [
       YulExpr.lit 0,
-      YulExpr.hex 0x08c379a000000000000000000000000000000000000000000000000000000000
+      YulExpr.hex errorStringSelectorWord
     ]),
     YulStmt.expr (YulExpr.call "mstore" [YulExpr.lit 4, YulExpr.lit 32]),
     YulStmt.expr (YulExpr.call "mstore" [YulExpr.lit 36, YulExpr.lit 22]),
@@ -302,7 +302,7 @@ def insufficientBalanceRevert : List YulStmt :=
   [
     YulStmt.expr (YulExpr.call "mstore" [
       YulExpr.lit 0,
-      YulExpr.hex 0x08c379a000000000000000000000000000000000000000000000000000000000
+      YulExpr.hex errorStringSelectorWord
     ]),
     YulStmt.expr (YulExpr.call "mstore" [YulExpr.lit 4, YulExpr.lit 32]),
     YulStmt.expr (YulExpr.call "mstore" [YulExpr.lit 36, YulExpr.lit 20]),
@@ -529,7 +529,7 @@ def ownedNotOwnerRevert : List YulStmt :=
   [
     YulStmt.expr (YulExpr.call "mstore" [
       YulExpr.lit 0,
-      YulExpr.hex 0x08c379a000000000000000000000000000000000000000000000000000000000
+      YulExpr.hex errorStringSelectorWord
     ]),
     YulStmt.expr (YulExpr.call "mstore" [YulExpr.lit 4, YulExpr.lit 32]),
     YulStmt.expr (YulExpr.call "mstore" [YulExpr.lit 36, YulExpr.lit 9]),

scripts/check_selectors.py

@@ -8,6 +8,7 @@
 4) ASTSpecs function signatures -> keccak selectors match for yul-ast output.
 5) Cross-check: shared contracts have identical signatures in both spec sets.
 6) No function name uses the reserved ``internal_`` prefix (Yul namespace collision).
+7) Error(string) selector constant sync between ContractSpec and Interpreter.
 """
 
 from __future__ import annotations
@@ -22,6 +23,8 @@
 SPEC_FILE = ROOT / "Compiler" / "Specs.lean"
 AST_SPEC_FILE = ROOT / "Compiler" / "ASTSpecs.lean"
 IR_EXPR_FILE = ROOT / "Compiler" / "Proofs" / "IRGeneration" / "Expr.lean"
+CONTRACT_SPEC_FILE = ROOT / "Compiler" / "ContractSpec.lean"
+INTERPRETER_FILE = ROOT / "Compiler" / "Interpreter.lean"
 YUL_DIR_LEGACY = ("yul", YUL_DIR)
 YUL_DIR_AST = ("yul-ast", ROOT / "compiler" / "yul-ast")
 
@@ -454,6 +457,63 @@ def format_selectors(selectors: List[int]) -> str:
     return "[" + ", ".join(f"0x{sel:08x}" for sel in selectors) + "]"
 
 
+# ---------------------------------------------------------------------------
+# Error(string) selector constant sync
+# ---------------------------------------------------------------------------
+
+# Canonical value: keccak256("Error(string)")[0:4] left-shifted to 32-byte word.
+_ERROR_STRING_SELECTOR_SHIFTED: int = 0x08c379a0 * (2**224)
+
+_CANONICAL_RE = re.compile(
+    r"def\s+errorStringSelectorWord\s*:\s*Nat\s*:=\s*(0x[0-9a-fA-F]+)\s*\*\s*\(2\s*\^\s*224\)"
+)
+_INTERPRETER_RE = re.compile(
+    r"def\s+revertSelectorWord\s*:\s*Nat\s*:=\s*\n?\s*(\d+)"
+)
+
+
+def check_error_selector_sync() -> List[str]:
+    """Verify the Error(string) selector constant is consistent across files.
+
+    Checks that:
+    - ContractSpec.errorStringSelectorWord matches the expected value
+    - Interpreter.revertSelectorWord (private copy) matches the canonical value
+    """
+    errors: List[str] = []
+
+    if not CONTRACT_SPEC_FILE.exists():
+        errors.append(f"Missing {CONTRACT_SPEC_FILE}")
+        return errors
+
+    spec_text = CONTRACT_SPEC_FILE.read_text(encoding="utf-8")
+    m = _CANONICAL_RE.search(spec_text)
+    if not m:
+        errors.append(
+            "ContractSpec.lean: missing errorStringSelectorWord definition"
+        )
+    else:
+        canonical = int(m.group(1), 16) * (2**224)
+        if canonical != _ERROR_STRING_SELECTOR_SHIFTED:
+            errors.append(
+                f"ContractSpec.errorStringSelectorWord: expected "
+                f"0x{_ERROR_STRING_SELECTOR_SHIFTED:064x}, got 0x{canonical:064x}"
+            )
+
+    if INTERPRETER_FILE.exists():
+        interp_text = INTERPRETER_FILE.read_text(encoding="utf-8")
+        m2 = _INTERPRETER_RE.search(interp_text)
+        if m2:
+            interp_val = int(m2.group(1))
+            if interp_val != _ERROR_STRING_SELECTOR_SHIFTED:
+                errors.append(
+                    f"Interpreter.revertSelectorWord: value {interp_val} does not "
+                    f"match canonical errorStringSelectorWord "
+                    f"({_ERROR_STRING_SELECTOR_SHIFTED})"
+                )
+
+    return errors
+
+
 def main() -> None:
     if not SPEC_FILE.exists():
         die(f"Missing specs file: {SPEC_FILE}")
@@ -498,6 +558,9 @@ def main() -> None:
     if ast_specs:
         errors.extend(check_ast_vs_legacy_signatures(specs, ast_specs))
 
+    # Validate Error(string) selector constant consistency.
+    errors.extend(check_error_selector_sync())
+
     report_errors(errors, "Selector checks failed")
     print("Selector checks passed.")