audit: add CI sync checks for internalFunctionPrefix and special entrypoints

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

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