Reject unsupported Lean releases before formal build preparation

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",

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)

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,