diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml index fd0e1106d..0dffaaeca 100644 --- a/.github/workflows/verify.yml +++ b/.github/workflows/verify.yml @@ -419,36 +419,8 @@ jobs: - name: Build split Lake packages independently run: python3 scripts/check_split_package_builds.py - - name: Check for axioms in proof files - run: | - echo "Checking for axioms in Compiler/ and Verity/..." - grep -rnE "^(private |protected )?axiom " Compiler/ Verity/ --include="*.lean" | tee axioms.txt || true - AXIOM_COUNT=$(wc -l < axioms.txt 2>/dev/null | tr -d ' ') - echo "Found $AXIOM_COUNT axiom declaration(s)" - if [ "$AXIOM_COUNT" -gt 0 ]; then - echo "::warning::Found $AXIOM_COUNT axiom(s) in proof files" - if [ ! -f "AXIOMS.md" ]; then - echo "::error::AXIOMS.md not found. All axioms must be documented." - exit 1 - fi - AXIOM_NAMES=$(sed -E 's/.*:(private |protected )?axiom ([a-zA-Z0-9_]*).*/\2/' axioms.txt | sort -u) - UNDOCUMENTED="" - for axiom_name in $AXIOM_NAMES; do - if ! grep -q "$axiom_name" AXIOMS.md; then - echo "::error::Axiom '$axiom_name' not documented in AXIOMS.md" - UNDOCUMENTED="$UNDOCUMENTED $axiom_name" - else - echo "✓ Axiom '$axiom_name' is documented" - fi - done - if [ -n "$UNDOCUMENTED" ]; then - echo "::error::Undocumented axioms:$UNDOCUMENTED" - exit 1 - fi - echo "✓ All $AXIOM_COUNT axioms are documented in AXIOMS.md" - else - echo "✓ No axioms found in proof files" - fi + - name: Check documented Lean axioms + run: python3 scripts/check_axioms.py - name: Build proof modules for axiom audit run: lake build PrintAxioms diff --git a/AXIOMS.md b/AXIOMS.md index 8bf0ea168..f4b2e2222 100644 --- a/AXIOMS.md +++ b/AXIOMS.md @@ -45,6 +45,28 @@ axiom solidityMappingSlot_lt_evmModulus (baseSlot key : Nat) : **Runtime performance**: An `@[implemented_by]` annotation optionally redirects to the FFI version at runtime for speed, without affecting proof soundness. +## Trusted Reduction and Codegen Surface (Non-Axiom) + +Verity currently has zero project-level Lean axioms, but some proofs and tests +intentionally rely on Lean mechanisms that sit outside ordinary kernel +elaboration: + +- `native_decide` proofs depend on Lean's native code generation and the builtin + `Lean.ofReduceBool` axiom. They are acceptable for executable smoke tests, + concrete bridge checks, and explicitly documented reduction witnesses, but + they are tracked as trusted reduction surface rather than counted as + project-level axioms. +- `@[implemented_by ...]` may redirect runtime execution to a faster + implementation. The proof term still sees the kernel-computable definition, + so this is a runtime/codegen trust boundary rather than a Lean axiom. +- `partial def` marks recursive executable helpers whose termination is not + kernel-proved. These helpers are allowed in macro, codegen, reporting, and + native-test infrastructure, and their presence is registry-gated. + +CI runs `scripts/check_trust_surface_registry.py` to ensure these mechanisms and +all explicit ECM assumptions (`axioms := [...]`) remain documented when their +source footprint changes. + ### 2. Selector computation (eliminated earlier) Function selector derivation (`bytes4(keccak256(signature))`) was previously @@ -178,6 +200,13 @@ compilation fail if any assumption hasn't been reviewed. | `Hashing.sha256PackedWords` / `Hashing.sha256Packed` | `evm_sha256_precompile`, `abi_packed_static_word_layout` | Static packed words are laid out before SHA-256 precompile call | | `Hashing.sha256PackedStaticSegments` | `evm_sha256_precompile`, `abi_packed_static_segment_layout` | Static packed byte-width segments are laid out before SHA-256 precompile call | +### Test-Only ECM Assumptions + +| Fixture | Assumption | Meaning | +|---------|------------|---------| +| `Compiler.CompileDriverTest` | `test_call_interface` | Synthetic compile-driver fixture for ECM trust reporting | +| `Compiler.CompileDriverTest` | `ctor_hook_interface` | Synthetic constructor fixture for ECM trust reporting | + ### Third-Party Module Assumptions Third-party ECMs (external Lean packages) document their assumptions in their own diff --git a/Compiler/CompilationModelFeatureTest.lean b/Compiler/CompilationModelFeatureTest.lean index 3bb3be1fa..a5b4c3be2 100644 --- a/Compiler/CompilationModelFeatureTest.lean +++ b/Compiler/CompilationModelFeatureTest.lean @@ -232,6 +232,27 @@ example : hashSliceExecutableUsesRuntimeStub = true := by native_decide end MacroKeccakSmoke +namespace MappingWordSmoke + +open Contracts.Smoke + +example : + MappingWordSmoke.setWord1_modelBody = + [ Stmt.setMappingWord "words" (Expr.param "key") 1 (Expr.param "value"), + Stmt.stop ] := rfl + +example : + MappingWordSmoke.getWord1_modelBody = + [ Stmt.letVar "word" (Expr.mappingWord "words" (Expr.param "key") 1), + Stmt.return (Expr.localVar "word") ] := rfl + +example : + MappingWordSmoke.isWord1NonZero_modelBody = + [ Stmt.letVar "word" (Expr.mappingWord "words" (Expr.param "key") 1), + Stmt.return (Expr.logicalNot (Expr.eq (Expr.localVar "word") (Expr.literal 0))) ] := rfl + +end MappingWordSmoke + namespace MacroExternalSmoke open Contracts @@ -5451,10 +5472,11 @@ set_option maxRecDepth 4096 in expectCompileToYul "abiEncodeStaticArray smoke spec" abiEncodeStaticArraySmokeSpec expectTrue "abiEncodeStaticArray writes the single dynamic argument head and length" (contains abiEncodeStaticArrayYul "mstore(__digest_abi_array_ptr, 32)" && - contains abiEncodeStaticArrayYul "mstore(add(__digest_abi_array_ptr, 32), items_length)") + contains abiEncodeStaticArrayYul "let __digest_abi_array_length := items_length" && + contains abiEncodeStaticArrayYul "mstore(add(__digest_abi_array_ptr, 32), __digest_abi_array_length)") expectTrue "abiEncodeStaticArray copies the fixed-width element payload" (contains abiEncodeStaticArrayYul - "let __digest_abi_array_data_bytes := mul(items_length, 128)" && + "let __digest_abi_array_data_bytes := mul(__digest_abi_array_length, 128)" && contains abiEncodeStaticArrayYul "calldatacopy(add(__digest_abi_array_ptr, 64), items_data_offset, __digest_abi_array_data_bytes)") expectTrue "abiEncodeStaticArray hashes the ABI-encoded dynamic array byte length" diff --git a/Compiler/Keccak/Sponge.lean b/Compiler/Keccak/Sponge.lean index 2f376e0a9..a34858d50 100644 --- a/Compiler/Keccak/Sponge.lean +++ b/Compiler/Keccak/Sponge.lean @@ -71,13 +71,16 @@ def domainSuffix (v : HashVariant) : UInt8 := /-- Pads the message tail (0 to 135 bytes) to a full 136-byte block. -/ def padBlock (leftover : ByteArray) (variant : HashVariant) : ByteArray := let rate := 136 - let arr1 := leftover.data.push (domainSuffix variant) - let padLen := rate - arr1.size - let arr2 := arr1 ++ Array.replicate padLen 0 - let lastIdx := rate - 1 - let lastVal := arr2[lastIdx]? |>.getD 0 - let arr3 := arr2.set! lastIdx (lastVal ||| 0x80) - ⟨arr3⟩ + if leftover.size >= rate then + panic! "Keccak.padBlock: leftover block must be shorter than rate" + else + let arr1 := leftover.data.push (domainSuffix variant) + let padLen := rate - arr1.size + let arr2 := arr1 ++ Array.replicate padLen 0 + let lastIdx := rate - 1 + let lastVal := arr2[lastIdx]? |>.getD 0 + let arr3 := arr2.set! lastIdx (lastVal ||| 0x80) + ⟨arr3⟩ /-- Kernel-friendly evaluation of a single bitwise instruction. -/ @[always_inline, inline] diff --git a/Compiler/Modules/Hashing.lean b/Compiler/Modules/Hashing.lean index 71466d6b4..c93305d23 100644 --- a/Compiler/Modules/Hashing.lean +++ b/Compiler/Modules/Hashing.lean @@ -181,22 +181,25 @@ def abiEncodeStaticArrayModule if elementWords == 0 then throw "abiEncodeStaticArray requires elementWords > 0" let ptrName := s!"__{resultVar}_abi_array_ptr" + let lengthName := s!"__{resultVar}_abi_array_length" let dataBytesName := s!"__{resultVar}_abi_array_data_bytes" let totalBytesName := s!"__{resultVar}_abi_array_total_bytes" let paddedTotalName := s!"__{resultVar}_abi_array_padded_total" let ptr := YulExpr.ident ptrName + let length := YulExpr.ident lengthName let dataBytes := YulExpr.ident dataBytesName let totalBytes := YulExpr.ident totalBytesName pure [ YulStmt.block ([ YulStmt.let_ ptrName (YulExpr.call "mload" [YulExpr.lit freeMemoryPointer]), + YulStmt.let_ lengthName arrayLengthExpr, YulStmt.expr (YulExpr.call "mstore" [ptr, YulExpr.lit 32]), YulStmt.expr (YulExpr.call "mstore" [ YulExpr.call "add" [ptr, YulExpr.lit 32], - arrayLengthExpr + length ]), YulStmt.let_ dataBytesName (YulExpr.call "mul" [ - arrayLengthExpr, + length, YulExpr.lit (elementWords * 32) ]) ] ++ ECM.dynamicCopyData ctx diff --git a/Makefile b/Makefile index 834533b6e..b6a7f5cff 100644 --- a/Makefile +++ b/Makefile @@ -126,6 +126,8 @@ check: ## Run local CI-equivalent checks job (no Lean build, no solc) python3 scripts/check_paths.py python3 scripts/check_compilationmodel_split.py python3 scripts/check_axioms.py + python3 scripts/check_trust_surface_registry.py + python3 scripts/check_benchmark_cases.py python3 scripts/generate_verification_status.py --check python3 scripts/generate_layer2_boundary_catalog.py --check python3 scripts/check_verification_status_doc.py diff --git a/docs/EXTERNAL_CALL_MODULES.md b/docs/EXTERNAL_CALL_MODULES.md index 489b3b905..847030548 100644 --- a/docs/EXTERNAL_CALL_MODULES.md +++ b/docs/EXTERNAL_CALL_MODULES.md @@ -100,6 +100,7 @@ Standard modules ship in `Compiler/Modules/`: | `ERC20.solmateSafeTransferFrom` | `transferFrom(from, to, amount)` | Solmate SafeTransferLib semantics: accepts no returndata or first returned word equal to `true` when `returndatasize() > 31` | `erc20_solmate_safe_transferFrom_interface` | | `Hashing.abiEncodeStaticWords` | Static-word `abi.encode` Keccak | Writes full 32-byte ABI words contiguously at the Solidity free-memory pointer and binds `keccak256(ptr, wordCount * 32)` | `keccak256_memory_slice_matches_evm`, `abi_standard_static_word_layout` | | `Hashing.abiEncodePackedWords` / `Hashing.abiEncodePacked` | Static-word packed Keccak | Writes 32-byte words contiguously at the Solidity free-memory pointer and binds `keccak256(ptr, wordCount * 32)` | `keccak256_memory_slice_matches_evm`, `abi_packed_static_word_layout` | +| `Hashing.abiEncodeStaticArray` | Standard dynamic-array Keccak | Writes ABI head offset, binds array length once, writes contiguous fixed-width static elements, and hashes the ABI frame | `keccak256_memory_slice_matches_evm`, `abi_standard_dynamic_array_static_element_layout` | | `Hashing.sha256PackedWords` / `Hashing.sha256Packed` | Static-word packed SHA-256 | Writes 32-byte words contiguously, calls precompile 0x02, and binds digest word | `evm_sha256_precompile`, `abi_packed_static_word_layout` | | `Hashing.abiEncodePackedStaticSegments` | Static byte-width packed Keccak | Writes 1- to 32-byte static segments at byte-precise offsets from the Solidity free-memory pointer and binds `keccak256(ptr, totalBytes)` | `keccak256_memory_slice_matches_evm`, `abi_packed_static_segment_layout` | | `Hashing.sha256PackedStaticSegments` | Static byte-width packed SHA-256 | Writes 1- to 32-byte static segments, calls precompile 0x02 over the exact byte length, and binds digest word | `evm_sha256_precompile`, `abi_packed_static_segment_layout` | diff --git a/scripts/check_axioms.py b/scripts/check_axioms.py index 9913974c9..822acc9c8 100644 --- a/scripts/check_axioms.py +++ b/scripts/check_axioms.py @@ -18,6 +18,7 @@ from property_utils import ROOT, die, report_errors, scrub_lean_code AXIOM_DECL_RE = re.compile(r"^(?:private |protected )?axiom\s+([A-Za-z_][A-Za-z0-9_']*)\b") +DEFAULT_AXIOM_ROOTS = ("Compiler", "Verity", "Contracts", "Benchmark") LEAN_BUILTIN_AXIOMS = frozenset([ "propext", @@ -56,7 +57,7 @@ def parse_active_axiom_count(axioms_md_text: str) -> int | None: def discover_repo_axioms() -> dict[str, tuple[str, int]]: """Return all Lean axiom declarations as ``{name: (relative_path, line)}``.""" discovered: dict[str, tuple[str, int]] = {} - for subdir in ("Compiler", "Verity"): + for subdir in DEFAULT_AXIOM_ROOTS: base_dir = ROOT / subdir if not base_dir.exists(): continue diff --git a/scripts/check_benchmark_cases.py b/scripts/check_benchmark_cases.py new file mode 100644 index 000000000..823a82578 --- /dev/null +++ b/scripts/check_benchmark_cases.py @@ -0,0 +1,79 @@ +#!/usr/bin/env python3 +"""Validate optional benchmark-case metadata. + +Core Verity checkouts do not normally contain `Benchmark/`; downstream +benchmark repos may vendor or overlay `Benchmark/`, while the standalone +benchmark repository keeps metadata under `cases/`. When present, each +`case.yaml` is a publication boundary and must identify the upstream target +commit. If a case has `FormalAudit.lean`, it must not still be marked +`proof_status: not_started`. +""" + +from __future__ import annotations + +import re +from pathlib import Path + +from property_utils import ROOT, report_errors + +KEY_VALUE_RE = re.compile(r"^\s*([A-Za-z_][A-Za-z0-9_-]*)\s*:\s*(.*?)\s*$") + + +def parse_case_yaml(path: Path) -> dict[str, str]: + values: dict[str, str] = {} + for line in path.read_text(encoding="utf-8").splitlines(): + line = line.split("#", 1)[0].strip() + if not line: + continue + match = KEY_VALUE_RE.match(line) + if match: + values[match.group(1)] = match.group(2).strip().strip("\"'") + return values + + +def discover_case_files(root: Path = ROOT) -> list[Path]: + case_files = sorted((root / "Benchmark").glob("Cases/**/case.yaml")) + case_files += sorted((root / "cases").glob("**/case.yaml")) + return case_files + + +def check_benchmark_cases(root: Path = ROOT) -> list[str]: + case_files = discover_case_files(root) + if not case_files: + return [] + + errors: list[str] = [] + for case_yaml in case_files: + metadata = parse_case_yaml(case_yaml) + case_dir = case_yaml.parent + rel = case_yaml.relative_to(root) + + if not metadata.get("upstream_commit"): + errors.append(f"{rel}: missing upstream_commit") + + if (case_dir / "FormalAudit.lean").exists(): + proof_status = metadata.get("proof_status") + if proof_status == "not_started": + errors.append(f"{rel}: FormalAudit.lean exists but proof_status is not_started") + + audit_target_commit = metadata.get("audit_target_commit") + if audit_target_commit is not None and not re.fullmatch(r"[0-9a-fA-F]{7,40}", audit_target_commit): + errors.append(f"{rel}: audit_target_commit must be a 7-40 character git hex prefix") + + return errors + + +def main() -> int: + case_files = discover_case_files() + if not case_files: + print("OK: no benchmark case metadata found; benchmark metadata check skipped") + return 0 + + errors = check_benchmark_cases() + report_errors(errors, "Benchmark case metadata check failed") + print(f"OK: benchmark metadata check passed for {len(case_files)} case.yaml file(s)") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/scripts/check_trust_surface_registry.py b/scripts/check_trust_surface_registry.py new file mode 100644 index 000000000..8bacfc69a --- /dev/null +++ b/scripts/check_trust_surface_registry.py @@ -0,0 +1,103 @@ +#!/usr/bin/env python3 +"""Validate that non-axiom trusted surfaces are documented. + +The Lean kernel axiom registry is intentionally separate from Verity's broader +trusted surface. This checker covers mechanisms that do not create project +Lean axioms, but still matter for audit soundness: + +* `native_decide` +* `@[implemented_by ...]` +* `partial def` +* explicit ECM assumption strings in `axioms := [...]` +""" + +from __future__ import annotations + +import re +from pathlib import Path + +from property_utils import ROOT, report_errors, scrub_lean_code, strip_lean_comments + +SCAN_ROOTS = ("Compiler", "Verity", "Contracts", "Benchmark") +DOC_PATHS = ("AXIOMS.md", "TRUST_ASSUMPTIONS.md") +DOC_DIRS = ("docs",) + +ECM_AXIOM_STRING_RE = re.compile(r'"([^"]+)"') + +MECHANISM_PATTERNS = ( + ("native_decide", re.compile(r"\bnative_decide\b")), + ("@[implemented_by", re.compile(r"@\[\s*implemented_by\b")), + ("partial def", re.compile(r"\bpartial\s+def\b")), +) + + +def _iter_lean_files(root: Path = ROOT) -> list[Path]: + files: list[Path] = [] + for subdir in SCAN_ROOTS: + base = root / subdir + if base.exists(): + files.extend(sorted(base.rglob("*.lean"))) + return files + + +def _read_doc_corpus(root: Path = ROOT) -> str: + chunks: list[str] = [] + for rel in DOC_PATHS: + path = root / rel + if path.exists(): + chunks.append(path.read_text(encoding="utf-8")) + for rel in DOC_DIRS: + base = root / rel + if base.exists(): + for path in sorted(base.rglob("*.md")): + chunks.append(path.read_text(encoding="utf-8")) + return "\n".join(chunks) + + +def collect_trust_surface(root: Path = ROOT) -> tuple[dict[str, int], dict[str, tuple[str, int]]]: + mechanisms = {name: 0 for name, _ in MECHANISM_PATTERNS} + ecm_axioms: dict[str, tuple[str, int]] = {} + + for path in _iter_lean_files(root): + raw_text = path.read_text(encoding="utf-8") + text = scrub_lean_code(raw_text) + text_without_comments = strip_lean_comments(raw_text) + rel = str(path.relative_to(root)) + for name, pattern in MECHANISM_PATTERNS: + mechanisms[name] += len(pattern.findall(text)) + for match in re.finditer(r"axioms\s*:=\s*\[(.*?)\]", text_without_comments, flags=re.DOTALL): + line_no = text_without_comments.count("\n", 0, match.start()) + 1 + for axiom_name in ECM_AXIOM_STRING_RE.findall(match.group(1)): + ecm_axioms.setdefault(axiom_name, (rel, line_no)) + + return mechanisms, ecm_axioms + + +def main() -> int: + docs = _read_doc_corpus() + mechanisms, ecm_axioms = collect_trust_surface() + + errors: list[str] = [] + for name, count in mechanisms.items(): + if count > 0 and name not in docs: + errors.append( + f"{name}: {count} occurrence(s) found in Lean sources but missing from trust docs" + ) + + for axiom_name, (rel, line) in sorted(ecm_axioms.items()): + if axiom_name not in docs: + errors.append( + f"{axiom_name}: ECM assumption from {rel}:{line} is missing from trust docs" + ) + + report_errors(errors, "Trust-surface registry check failed") + print( + "OK: trust-surface registry documents " + f"{len(ecm_axioms)} ECM assumption(s), " + + ", ".join(f"{name}={count}" for name, count in mechanisms.items()) + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/scripts/test_check_axioms.py b/scripts/test_check_axioms.py index aa9c124aa..7abdb1f7f 100644 --- a/scripts/test_check_axioms.py +++ b/scripts/test_check_axioms.py @@ -38,6 +38,7 @@ def test_discover_repo_axioms_ignores_comments_and_strings(self) -> None: root = Path(tmpdir) (root / "Compiler").mkdir(parents=True, exist_ok=True) (root / "Verity").mkdir(parents=True, exist_ok=True) + (root / "Benchmark").mkdir(parents=True, exist_ok=True) (root / "Compiler" / "A.lean").write_text( "\n".join( [ @@ -50,6 +51,10 @@ def test_discover_repo_axioms_ignores_comments_and_strings(self) -> None: + "\n", encoding="utf-8", ) + (root / "Benchmark" / "Case.lean").write_text( + "axiom benchmark_axiom : True\n", + encoding="utf-8", + ) old_root = check_axioms.ROOT try: @@ -58,7 +63,13 @@ def test_discover_repo_axioms_ignores_comments_and_strings(self) -> None: finally: check_axioms.ROOT = old_root - self.assertEqual(discovered, {"real_axiom": ("Compiler/A.lean", 4)}) + self.assertEqual( + discovered, + { + "real_axiom": ("Compiler/A.lean", 4), + "benchmark_axiom": ("Benchmark/Case.lean", 1), + }, + ) def test_main_reports_missing_registry_entries_and_count_drift(self) -> None: with tempfile.TemporaryDirectory() as tmpdir: diff --git a/scripts/test_check_benchmark_cases.py b/scripts/test_check_benchmark_cases.py new file mode 100644 index 000000000..dc90371d0 --- /dev/null +++ b/scripts/test_check_benchmark_cases.py @@ -0,0 +1,71 @@ +#!/usr/bin/env python3 +from __future__ import annotations + +import sys +import tempfile +import unittest +from pathlib import Path + +SCRIPT_DIR = Path(__file__).resolve().parent +if str(SCRIPT_DIR) not in sys.path: + sys.path.insert(0, str(SCRIPT_DIR)) + +import check_benchmark_cases + + +class CheckBenchmarkCasesTests(unittest.TestCase): + def test_no_benchmark_metadata_is_ok(self) -> None: + with tempfile.TemporaryDirectory() as tmpdir: + self.assertEqual(check_benchmark_cases.check_benchmark_cases(Path(tmpdir)), []) + + def test_overlaid_formal_audit_case_requires_started_status_and_upstream_commit(self) -> None: + with tempfile.TemporaryDirectory() as tmpdir: + root = Path(tmpdir) + case = root / "Benchmark" / "Cases" / "UnlinkXyz" / "Pool" + case.mkdir(parents=True) + (case / "FormalAudit.lean").write_text("example : True := trivial\n", encoding="utf-8") + (case / "case.yaml").write_text( + "proof_status: not_started\naudit_target_commit: not-a-sha\n", + encoding="utf-8", + ) + + errors = check_benchmark_cases.check_benchmark_cases(root) + + self.assertIn("Benchmark/Cases/UnlinkXyz/Pool/case.yaml: missing upstream_commit", errors) + self.assertIn( + "Benchmark/Cases/UnlinkXyz/Pool/case.yaml: FormalAudit.lean exists but proof_status is not_started", + errors, + ) + self.assertIn( + "Benchmark/Cases/UnlinkXyz/Pool/case.yaml: audit_target_commit must be a 7-40 character git hex prefix", + errors, + ) + + def test_valid_case_passes(self) -> None: + with tempfile.TemporaryDirectory() as tmpdir: + root = Path(tmpdir) + case = root / "Benchmark" / "Cases" / "UnlinkXyz" / "Pool" + case.mkdir(parents=True) + (case / "FormalAudit.lean").write_text("example : True := trivial\n", encoding="utf-8") + (case / "case.yaml").write_text( + "proof_status: proved\nupstream_commit: 7617b3e\naudit_target_commit: 7617b3e\n", + encoding="utf-8", + ) + + self.assertEqual(check_benchmark_cases.check_benchmark_cases(root), []) + + def test_standalone_benchmark_cases_layout_is_checked(self) -> None: + with tempfile.TemporaryDirectory() as tmpdir: + root = Path(tmpdir) + case = root / "cases" / "unlink_xyz" / "pool" + case.mkdir(parents=True) + (case / "case.yaml").write_text( + "proof_status: proved\nupstream_commit: 7617b3e\n", + encoding="utf-8", + ) + + self.assertEqual(check_benchmark_cases.check_benchmark_cases(root), []) + + +if __name__ == "__main__": + unittest.main() diff --git a/scripts/test_check_trust_surface_registry.py b/scripts/test_check_trust_surface_registry.py new file mode 100644 index 000000000..58e7ceb25 --- /dev/null +++ b/scripts/test_check_trust_surface_registry.py @@ -0,0 +1,87 @@ +#!/usr/bin/env python3 +from __future__ import annotations + +import sys +import tempfile +import unittest +from pathlib import Path + +SCRIPT_DIR = Path(__file__).resolve().parent +if str(SCRIPT_DIR) not in sys.path: + sys.path.insert(0, str(SCRIPT_DIR)) + +import check_trust_surface_registry + + +class CheckTrustSurfaceRegistryTests(unittest.TestCase): + def test_collects_mechanisms_and_ecm_axioms(self) -> None: + with tempfile.TemporaryDirectory() as tmpdir: + root = Path(tmpdir) + (root / "Compiler").mkdir(parents=True) + (root / "Compiler" / "A.lean").write_text( + "\n".join( + [ + "@[implemented_by fastFoo]", + "def foo : True := by native_decide", + "partial def walk : Nat -> Nat | n => n", + 'def mod where axioms := ["external_surface"]', + ] + ) + + "\n", + encoding="utf-8", + ) + + mechanisms, ecm_axioms = check_trust_surface_registry.collect_trust_surface(root) + + self.assertEqual(mechanisms["native_decide"], 1) + self.assertEqual(mechanisms["@[implemented_by"], 1) + self.assertEqual(mechanisms["partial def"], 1) + self.assertEqual(ecm_axioms, {"external_surface": ("Compiler/A.lean", 4)}) + + def test_collects_benchmark_tree_when_present(self) -> None: + with tempfile.TemporaryDirectory() as tmpdir: + root = Path(tmpdir) + (root / "Benchmark").mkdir(parents=True) + (root / "Benchmark" / "Case.lean").write_text( + 'def mod where axioms := ["benchmark_external_surface"]\n', + encoding="utf-8", + ) + + _, ecm_axioms = check_trust_surface_registry.collect_trust_surface(root) + + self.assertEqual( + ecm_axioms, + {"benchmark_external_surface": ("Benchmark/Case.lean", 1)}, + ) + + def test_collects_multiline_ecm_axioms(self) -> None: + with tempfile.TemporaryDirectory() as tmpdir: + root = Path(tmpdir) + (root / "Compiler").mkdir(parents=True) + (root / "Compiler" / "A.lean").write_text( + "\n".join( + [ + "def mod where", + " axioms := [", + ' "first_surface",', + ' "second_surface"', + " ]", + ] + ) + + "\n", + encoding="utf-8", + ) + + _, ecm_axioms = check_trust_surface_registry.collect_trust_surface(root) + + self.assertEqual( + ecm_axioms, + { + "first_surface": ("Compiler/A.lean", 2), + "second_surface": ("Compiler/A.lean", 2), + }, + ) + + +if __name__ == "__main__": + unittest.main() diff --git a/scripts/verify_sync_spec.json b/scripts/verify_sync_spec.json index c50bad5d6..145aeb663 100644 --- a/scripts/verify_sync_spec.json +++ b/scripts/verify_sync_spec.json @@ -723,6 +723,8 @@ "python3 scripts/check_paths.py", "python3 scripts/check_compilationmodel_split.py", "python3 scripts/check_axioms.py", + "python3 scripts/check_trust_surface_registry.py", + "python3 scripts/check_benchmark_cases.py", "python3 scripts/generate_verification_status.py --check", "python3 scripts/check_verification_status_doc.py", "python3 scripts/generate_verify_sync_spec.py --check", @@ -763,6 +765,7 @@ ], "expected_build_audit_commands": [ "check_split_package_builds.py", + "check_axioms.py", "check_proof_length.py --format=markdown >> $GITHUB_STEP_SUMMARY", "report_property_coverage.py --format=markdown >> $GITHUB_STEP_SUMMARY", "check_storage_layout.py --format=markdown >> $GITHUB_STEP_SUMMARY" diff --git a/scripts/verify_sync_spec_source.py b/scripts/verify_sync_spec_source.py index ac2dfb48e..37bda321e 100644 --- a/scripts/verify_sync_spec_source.py +++ b/scripts/verify_sync_spec_source.py @@ -618,6 +618,8 @@ 'python3 scripts/check_paths.py', 'python3 scripts/check_compilationmodel_split.py', 'python3 scripts/check_axioms.py', + 'python3 scripts/check_trust_surface_registry.py', + 'python3 scripts/check_benchmark_cases.py', 'python3 scripts/generate_verification_status.py --check', 'python3 scripts/check_verification_status_doc.py', 'python3 scripts/generate_verify_sync_spec.py --check', @@ -656,6 +658,7 @@ 'expected_build_commands': ['check_lean_warning_regression.py --log lake-build.log'], 'required_build_run_commands': ['lake build PrintAxioms'], 'expected_build_audit_commands': ['check_split_package_builds.py', + 'check_axioms.py', 'check_proof_length.py --format=markdown >> ' '$GITHUB_STEP_SUMMARY', 'report_property_coverage.py --format=markdown >> '