From efdf8db9dae06d3af2a9ff0fc0e66b158b021f10 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 22 Feb 2026 04:43:12 +0100 Subject: [PATCH] audit: add CI sync checks for internalFunctionPrefix and special entrypoints MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit check_selectors.py hardcodes _INTERNAL_FUNCTION_PREFIX ("internal_") and _SPECIAL_ENTRYPOINTS ({"fallback", "receive"}) used in collision and filtering checks. These were validated only by code comments saying "Must match ContractSpec.lean" — no automated enforcement. Add checks #10 and #11 that regex-extract the canonical Lean definitions and validate both Python constants match, following the same pattern as checks #7–9. Co-Authored-By: Claude Opus 4.6 --- AUDIT.md | 2 +- scripts/check_selectors.py | 72 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 73 insertions(+), 1 deletion(-) diff --git a/AUDIT.md b/AUDIT.md index 7620811ce..0069afca5 100644 --- a/AUDIT.md +++ b/AUDIT.md @@ -137,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; selector shift 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; internal prefix sync; special entrypoint names 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/scripts/check_selectors.py b/scripts/check_selectors.py index ab00591c6..88217dd55 100755 --- a/scripts/check_selectors.py +++ b/scripts/check_selectors.py @@ -11,6 +11,8 @@ 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. +10) Internal function prefix sync between ContractSpec and CI script. +11) Special entrypoint names sync between ContractSpec and CI script. """ from __future__ import annotations @@ -597,6 +599,70 @@ def check_selector_shift_sync() -> List[str]: return errors +# --------------------------------------------------------------------------- +# Internal function prefix sync +# --------------------------------------------------------------------------- + +_INTERNAL_PREFIX_RE = re.compile( + r'def\s+internalFunctionPrefix\s*:\s*String\s*:=\s*"([^"]*)"' +) + + +def check_internal_prefix_sync() -> List[str]: + """Verify _INTERNAL_FUNCTION_PREFIX matches ContractSpec.internalFunctionPrefix.""" + errors: List[str] = [] + if not CONTRACT_SPEC_FILE.exists(): + errors.append(f"Missing {CONTRACT_SPEC_FILE}") + return errors + text = CONTRACT_SPEC_FILE.read_text(encoding="utf-8") + m = _INTERNAL_PREFIX_RE.search(text) + if not m: + errors.append( + "ContractSpec.lean: missing internalFunctionPrefix definition" + ) + elif m.group(1) != _INTERNAL_FUNCTION_PREFIX: + errors.append( + f"ContractSpec.internalFunctionPrefix is {m.group(1)!r} " + f"but check_selectors.py uses {_INTERNAL_FUNCTION_PREFIX!r}" + ) + return errors + + +# --------------------------------------------------------------------------- +# Special entrypoint names sync +# --------------------------------------------------------------------------- + +_INTEROP_ENTRYPOINTS_RE = re.compile( + r'def\s+isInteropEntrypointName\b.*?:=\s*\[([^\]]*)\]', + re.DOTALL, +) + + +def check_special_entrypoints_sync() -> List[str]: + """Verify _SPECIAL_ENTRYPOINTS matches ContractSpec.isInteropEntrypointName.""" + errors: List[str] = [] + if not CONTRACT_SPEC_FILE.exists(): + errors.append(f"Missing {CONTRACT_SPEC_FILE}") + return errors + text = CONTRACT_SPEC_FILE.read_text(encoding="utf-8") + m = _INTEROP_ENTRYPOINTS_RE.search(text) + if not m: + errors.append( + "ContractSpec.lean: missing isInteropEntrypointName definition" + ) + return errors + # Parse the Lean list literal: ["fallback", "receive"] + lean_names = set( + n.strip().strip('"') for n in m.group(1).split(",") if n.strip() + ) + if lean_names != _SPECIAL_ENTRYPOINTS: + errors.append( + f"ContractSpec.isInteropEntrypointName uses {sorted(lean_names)} " + f"but check_selectors.py uses {sorted(_SPECIAL_ENTRYPOINTS)}" + ) + return errors + + def main() -> None: if not SPEC_FILE.exists(): die(f"Missing specs file: {SPEC_FILE}") @@ -658,6 +724,12 @@ def main() -> None: # Validate selector shift constant consistency. errors.extend(check_selector_shift_sync()) + # Validate internal function prefix consistency. + errors.extend(check_internal_prefix_sync()) + + # Validate special entrypoint names consistency. + errors.extend(check_special_entrypoints_sync()) + report_errors(errors, "Selector checks failed") print("Selector checks passed.")