diff --git a/formal/manifest.json b/formal/manifest.json index 8d4318869..f8ebaf031 100644 --- a/formal/manifest.json +++ b/formal/manifest.json @@ -43,8 +43,8 @@ "formal/REVIEW_LANE.md": "6a0dcdd93f1aec16ede829820b913116a5c60c2bbbd78630690599dbc5d8be41", "formal/reviews/TEMPLATE_alignment_review.json": "e722e928ca43c16981e063d8eb1c91e9bf8c683241d9dcf156400a419e72feb3", "formal/reviews/README.md": "333ca71e7c676cee89e5d01cd61999c21bb0584e41d6bdacb18afa410109f95d", - "tools/formal_gate_check.py": "21c355e02ac6e01337d10465a3105b34b93f832586ee60aa2430f662a90cd8b7", - "tests/test_formal_gate.py": "4286136d8b24eca9b26d1e7b12933bed5b0961809b362a60c3af7bf46e6ed4b6" + "tools/formal_gate_check.py": "1125e435429f0a7391d6b076c99f1198bf862376276f6c00c91b5ea4f6a88ec5", + "tests/test_formal_gate.py": "2b13ad83b03d2b45f4be70ce03af597c195563a1ed0bd3983a2b7040068a3a84" }, "unbound_files": [ "formal/manifest.json", diff --git a/tests/test_formal_gate.py b/tests/test_formal_gate.py index 0b36e5139..348bb503b 100644 --- a/tests/test_formal_gate.py +++ b/tests/test_formal_gate.py @@ -11,8 +11,11 @@ import io import json from pathlib import Path +import shutil +import subprocess import tempfile import unittest +from unittest import mock ROOT = Path(__file__).resolve().parents[1] spec = importlib.util.spec_from_file_location("gate", ROOT / "tools/formal_gate_check.py") @@ -322,6 +325,153 @@ def test_alignment_table_drift_fails_cli(self): self.assertEqual(code, 1) + # Ordering cases derive from the published, source-bound diagnostic: + # https://github.com/d6g8k5htny-coder/main/issues/307#issuecomment-6066278094 + # Only subprocess outputs and Git identity are synthetic. The real execute, + # run/log writer, axiom parser and temporary-package source checker run here. + LEAN_COMMIT = "5045d0056413266e57c625dcd7c365b10e377c52" + RUNTIME_RELEASE = ( + "Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit " + + LEAN_COMMIT + ", Release)\n" + ) + WRONG_RUNTIMES = ( + "Lean (version 4.34.10, x86_64, Release)", + "Lean (version 4.34.100, x86_64, Release)", + "Lean (version 4.34.1-rc1, x86_64, Release)", + "Lean (version 4.34.1-nightly, x86_64, Release)", + "unrelated diagnostic: version 4.34.1", + "Lean (version 4.34.2, x86_64, Release)", + "Lean (version 4.35.1, x86_64, Release)", + "Lean (version 4.34.0, x86_64, Release)", + "Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit 5, Release)", + "Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit " + "a" * 40 + ", Release)", + "Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit " + + LEAN_COMMIT + ", Debug)", + "Lean (version 4.34.1,", + "Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit " + + LEAN_COMMIT + ", Release)\ntrailing diagnostic", + "", + ) + + def runtime_probe(self, versions, *, version_returncode=0, version_timeout=False, + mutate_source=False): + m, digest, pkg = self.check() + shutil.rmtree(pkg / ".lake", ignore_errors=True) + sentinel = pkg / ".lake/build/existing-build-sentinel" + sentinel.parent.mkdir(parents=True) + sentinel.write_text("temporary build must survive preflight refusal\n") + out = pkg / ".lake/formal-evidence" + events = [] + self.runtime_state = {"events": events, "sentinel": sentinel, "out": out} + version_outputs = iter(versions) + source_check = gate.source_check + + def check_source(root): + events.append("source-check") + return source_check(root, "pkg/manifest.json") + + def run_process(command, **kwargs): + if command == ["git", "rev-parse", "HEAD"]: + events.append("git-head") + return subprocess.CompletedProcess(command, 0, "a" * 40 + "\n") + self.assertEqual(command[0], "/synthetic/lake") + self.assertEqual(kwargs["cwd"], pkg) + if command[1:] == ["env", "lean", "--version"]: + events.append("version") + if version_timeout: + raise subprocess.TimeoutExpired(command, kwargs["timeout"]) + return subprocess.CompletedProcess(command, version_returncode, next(version_outputs)) + if command[1:] == ["build"]: + events.append("build") + if mutate_source: + with (pkg / "sources/SOURCE.md").open("a") as f: + f.write("synthetic build changed a bound source\n") + return subprocess.CompletedProcess(command, 0, "synthetic build\n") + if command[1:] == ["env", "leanchecker", "Demo"]: + events.append("leanchecker") + return subprocess.CompletedProcess(command, 0, "synthetic replay\n") + self.assertEqual(command[1:3], ["env", "lean"]) + name = Path(command[3]).name + events.append(name) + if name == "Audit.lean": + return subprocess.CompletedProcess(command, 0, AUDIT) + if name == "Types.lean": + return subprocess.CompletedProcess(command, 0, "synthetic elaborated types\n") + if name == "tight.lean": + return subprocess.CompletedProcess(command, 1, "is false\n") + if name in {"sorry.lean", "custom_imported.lean", "native.lean"}: + return subprocess.CompletedProcess(command, 0, "'injected' depends on axioms: [sorryAx]\n") + self.fail("unexpected synthetic process: " + repr(command)) + + with mock.patch.object(gate, "lake_binary", return_value="/synthetic/lake"), \ + mock.patch.object(gate.subprocess, "run", side_effect=run_process), \ + mock.patch.object(gate, "source_check", side_effect=check_source), \ + contextlib.redirect_stdout(io.StringIO()): + return gate.execute(m, digest, pkg, self.root) + + def test_wrong_runtime_preserves_build_and_refuses_before_work(self): + for version in self.WRONG_RUNTIMES: + with self.subTest(version=version): + with self.assertRaisesRegex(ValueError, "unexpected running Lean version"): + self.runtime_probe([version]) + self.assertTrue(self.runtime_state["sentinel"].is_file()) + self.assertEqual(self.runtime_state["events"], ["version"]) + self.assertFalse((self.runtime_state["out"] / "receipt.json").exists()) + self.assertEqual((self.runtime_state["out"] / "preflight-version.log").read_text(), version) + + def test_valid_runtime_preserves_both_version_observations_and_logs(self): + final_version = ( + "Lean (version 4.34.1, aarch64-unknown-linux-gnu, commit " + + self.LEAN_COMMIT + ", Release)\n" + ) + receipt = self.runtime_probe([self.RUNTIME_RELEASE, final_version]) + self.assertEqual(self.runtime_state["events"], [ + "version", "build", "leanchecker", "Audit.lean", "Types.lean", "tight.lean", + "sorry.lean", "custom_imported.lean", "native.lean", "source-check", "version", "git-head"]) + self.assertFalse(self.runtime_state["sentinel"].exists()) + self.assertEqual(receipt["lean_version"], final_version.strip()) + out = self.runtime_state["out"] + self.assertEqual((out / "preflight-version.log").read_text(), self.RUNTIME_RELEASE) + self.assertEqual((out / "version.log").read_text(), final_version) + self.assertEqual(set(receipt["logs"]), { + "preflight-version.log", "version.log", "build.log", "leanchecker.log", + "axioms.log", "elaborated-types.log", "tight.log", "sorry.log", + "custom_imported.log", "native.log"}) + for name, digest in receipt["logs"].items(): + self.assertEqual(digest, sha((out / name).read_bytes()), name) + + def test_wrong_postflight_runtime_refuses_receipt_after_source_recheck(self): + for version in self.WRONG_RUNTIMES: + with self.subTest(version=version): + with self.assertRaisesRegex(ValueError, "unexpected running Lean version"): + self.runtime_probe([self.RUNTIME_RELEASE, version]) + self.assertEqual(self.runtime_state["events"][0], "version") + self.assertEqual(self.runtime_state["events"][-2:], ["source-check", "version"]) + self.assertFalse((self.runtime_state["out"] / "receipt.json").exists()) + + def test_postflight_source_change_still_refuses_receipt(self): + with self.assertRaisesRegex(ValueError, "source hash mismatch"): + self.runtime_probe([self.RUNTIME_RELEASE], mutate_source=True) + self.assertEqual(self.runtime_state["events"][0], "version") + self.assertEqual(self.runtime_state["events"][-1], "source-check") + self.assertEqual(self.runtime_state["events"].count("version"), 1) + self.assertFalse((self.runtime_state["out"] / "receipt.json").exists()) + + def test_preflight_process_failure_preserves_build(self): + with self.assertRaisesRegex(ValueError, "unexpected process outcome"): + self.runtime_probe([self.RUNTIME_RELEASE], version_returncode=17) + self.assertTrue(self.runtime_state["sentinel"].is_file()) + self.assertEqual(self.runtime_state["events"], ["version"]) + self.assertFalse((self.runtime_state["out"] / "receipt.json").exists()) + + def test_preflight_timeout_preserves_build(self): + with self.assertRaises(subprocess.TimeoutExpired): + self.runtime_probe([], version_timeout=True) + self.assertTrue(self.runtime_state["sentinel"].is_file()) + self.assertEqual(self.runtime_state["events"], ["version"]) + self.assertFalse((self.runtime_state["out"] / "receipt.json").exists()) + + class RepositoryControls(unittest.TestCase): def test_real_manifest_source_check(self): m, digest, pkg = gate.source_check(ROOT) diff --git a/tools/formal_gate_check.py b/tools/formal_gate_check.py index b057225d3..263d8674c 100644 --- a/tools/formal_gate_check.py +++ b/tools/formal_gate_check.py @@ -55,6 +55,7 @@ THEOREM = re.compile(r"^(?:theorem|lemma)\s+(" + NAME + r")", re.M) NAMESPACE = re.compile(r"^namespace\s+(\S+)", re.M) TOOLCHAIN = "leanprover/lean4:v4.34.1" +LEAN_COMMIT = "5045d0056413266e57c625dcd7c365b10e377c52" BUILD_DIR = ".lake" @@ -221,6 +222,17 @@ def lake_binary() -> str | None: return str(candidate) if candidate.is_file() else None +def check_lean_version(text: str) -> str: + pin = re.fullmatch(r"leanprover/lean4:v(\d+\.\d+\.\d+)", TOOLCHAIN) + require(pin is not None, "unsupported pinned Lean toolchain") + version = text.strip() + record = (r"Lean \(version " + re.escape(pin.group(1)) + + r", [A-Za-z0-9_.+-]+, commit " + LEAN_COMMIT + r", Release\)") + require(re.fullmatch(record, version) is not None, + "unexpected running Lean version") + return version + + def run(command, label, out: Path, cwd: Path, env, expect_success=True): result = subprocess.run(command, cwd=cwd, text=True, stdout=subprocess.PIPE, stderr=subprocess.STDOUT, timeout=900, env=env) (out / (label + ".log")).write_text(result.stdout, encoding="utf-8") @@ -251,6 +263,7 @@ def execute(m: dict, digest: str, pkg: Path, root: Path) -> dict: out = pkg / BUILD_DIR / "formal-evidence" out.mkdir(parents=True, exist_ok=True) require(not (pkg / BUILD_DIR).is_symlink() and not (pkg / BUILD_DIR / "build").is_symlink(), "symlink build directory") + check_lean_version(run([lake, "env", "lean", "--version"], "preflight-version", out, pkg, env)) if (pkg / BUILD_DIR / "build").exists(): shutil.rmtree(pkg / BUILD_DIR / "build") targets = [t["name"] for t in m["targets"]] @@ -281,8 +294,7 @@ def execute(m: dict, digest: str, pkg: Path, root: Path) -> dict: outcomes[label] = "REJECTED_BY_LEAN" _, after, _ = source_check(root) require(after == digest, "manifest changed during execution") - version = run([lake, "env", "lean", "--version"], "version", out, pkg, env).strip() - require("version 4.34.1" in version, "unexpected running Lean version") + version = check_lean_version(run([lake, "env", "lean", "--version"], "version", out, pkg, env)) head = subprocess.run(["git", "rev-parse", "HEAD"], cwd=root, text=True, capture_output=True).stdout.strip() require(HEX40.fullmatch(head or ""), "missing exact checked commit") receipt = dict(schema_version=1, scientific_effect="NONE", scientific_status_authority=False,