diff --git a/AUDIT.md b/AUDIT.md index d05b96eb2..999b33c76 100644 --- a/AUDIT.md +++ b/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 diff --git a/Compiler/ContractSpec.lean b/Compiler/ContractSpec.lean index aace7d0d5..4a8a32963 100644 --- a/Compiler/ContractSpec.lean +++ b/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]) ] diff --git a/Compiler/Interpreter.lean b/Compiler/Interpreter.lean index 357559cf6..1c83d6c89 100644 --- a/Compiler/Interpreter.lean +++ b/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 diff --git a/Compiler/Proofs/IRGeneration/Expr.lean b/Compiler/Proofs/IRGeneration/Expr.lean index 7c0b755f1..52cb8f73f 100644 --- a/Compiler/Proofs/IRGeneration/Expr.lean +++ b/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]), diff --git a/scripts/check_selectors.py b/scripts/check_selectors.py index e87936364..9a2a28816 100755 --- a/scripts/check_selectors.py +++ b/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.")