formal: kit v2.1 (stale mutant patch check)

scripts/formal/README.md

@@ -1,6 +1,6 @@
-# Formal kit (version 2)
+# Formal kit (version 2.1)
 
-`KIT_VERSION = "2"` in `formal_kit.py`; both scripts print it and accept `--version`. Changes from v1 are listed at the end.
+`KIT_VERSION = "2.1"` in `formal_kit.py`; both scripts print it and accept `--version`. Changes from v1 are listed at the end.
 
 Shared tooling that keeps a repository's formal-verification claims honest.
 Python 3 standard library only (tests pass on 3.9, 3.12 and 3.14). Each repo vendors a copy into
@@ -153,3 +153,4 @@ Symbol extractor (Go and Rust only; other file types may only use symbol `*`):
 * Schema stays `1`; new optional keys: `formal_docs`, `scratch_cache_dirs`, claim/mutant `detector_kind`. When adding the table markers, also set `formal_docs` so that losing the file or its markers fails instead of warning.
 * A mutant with its own `detector` that is not a cargo or go test needs `"detector_kind": "custom"` in its own `mutants` map entry; the claim's `custom` does not carry over. averin: the Kani-override mutants `m9-b64-one-byte-tail` and `m10-b64-two-byte-tail` (`bash formal/run-kani.sh --harness ...`) must declare it when averin vendors v2.
 * Residual limits (accepted): the vacuity guard reads output text and can be satisfied by a detector that prints a cargo-looking line (use review, not trust), and it proves only that some test ran, not that every named test did; a vacuous-kill check compares cover hashes only and cannot tell a trivial in-symbol edit from a semantic one; compile-break detection is a heuristic warning; cfg twins with identical signatures stay addressable only through `*`.
+* v2.1: `check_claims.py` runs `git apply --check` for every registered mutant patch against the current tree (no build, so `formal-fast` catches a patch made stale by a source change on the PR that changes it). `check_mutants.py` sets `FORMAL_KIT_MUTATED_TREE=1` for mutated detector runs so a detector that runs `check_claims.py` inside the mutated tree is not killed by its own already-applied patch.

scripts/formal/check_claims.py

@@ -216,17 +216,37 @@ def selected(r: CoverResult) -> bool:
             for r in changes]
 
 
+MUTATED_TREE_ENV = "FORMAL_KIT_MUTATED_TREE"
+
+
 def check_mutants_files(root: Path, data: dict, rep: Report) -> None:
+    # Under check_mutants.py the tree is deliberately mutated (the patch is already applied), so a
+    # detector that runs this checker must not be killed by "patch does not apply"; the runner has
+    # already proved the patch applied to the unmutated tree.
+    mutated = os.environ.get(MUTATED_TREE_ENV) == "1"
     specs, errs = fk.resolve_mutants(data)
     for e in errs:
         rep.fail("mutants", e)
     referenced: Set[str] = set()
+    applied: Set[str] = set()
     for c in data.get("claims", []):
         for m in c.get("mutants", []):
             referenced.add(m)
             p = root / "formal" / "mutants" / (m + ".patch")
             if p.is_file():
-                rep.ok("mutant %s" % m, c["id"])
+                if m in applied:
+                    continue
+                applied.add(m)
+                if mutated:
+                    rep.ok("mutant %s" % m, c["id"])
+                    continue
+                chk = subprocess.run(["git", "apply", "--check", str(p)], cwd=str(root), capture_output=True,
+                                     text=True, encoding="utf-8", errors="replace")
+                if chk.returncode == 0:
+                    rep.ok("mutant %s" % m, c["id"])
+                else:
+                    rep.fail("mutant %s" % m, "claim %s: formal/mutants/%s.patch does not apply to the current tree "
+                             "(stale after a source change; regenerate it): %s" % (c["id"], m, chk.stderr.strip()[:300]))
             else:
                 rep.fail("mutant %s" % m, "claim %s: formal/mutants/%s.patch is missing" % (c["id"], m))
     d = root / "formal" / "mutants"

scripts/formal/check_mutants.py

@@ -289,7 +289,7 @@ def cover_hashes(claim_id: str) -> List[str]:
                 touched = before != cover_hashes(s.claim)
                 neutralize_drift_lock(scratch, claims_rel)
                 t0 = time.time()
-                st, rc, tail = run_detector(s.detector, scratch, timeout, env)
+                st, rc, tail = run_detector(s.detector, scratch, timeout, dict(env, FORMAL_KIT_MUTATED_TREE="1"))
                 row["seconds"] = round(time.time() - t0, 1)
                 # full restore after every mutant run: tracked files back to HEAD (undoes the patch and any
                 # edit the detector made), untracked and ignored files removed (a file the patch created, or

scripts/formal/formal_kit.py

@@ -19,7 +19,7 @@
 from pathlib import Path
 from typing import Dict, List, Optional, Set, Tuple
 
-KIT_VERSION = "2"
+KIT_VERSION = "2.1"
 SCHEMA_VERSION = 1
 METHODS = (
     "lean", "kani", "tla", "aeneas", "exhaustive", "differential-vectors",

scripts/formal/tests/test_kit.py

@@ -5,6 +5,7 @@
 import sys
 import tempfile
 import unittest
+from unittest import mock
 from pathlib import Path
 
 HERE = Path(__file__).resolve().parent
@@ -431,6 +432,8 @@ def git(*a):
     return d, git
 
 
+M_PATCH = "--- a/m.txt\n+++ b/m.txt\n@@ -1 +1 @@\n-x\n+y\n"
+
 CI_OK = ("name: ci\non: push\njobs:\n  go:\n    runs-on: x\n  nightly:\n    if: github.event_name == 'schedule'\n"
          "    runs-on: x\n  ci-required:\n    if: always()\n    needs: [go]\n    runs-on: x\n")
 
@@ -456,7 +459,7 @@ class ClaimsChecks(unittest.TestCase):
     def setUp(self):
         self.d, self.git = make_repo({
             "p.go": GO_FILE, ".github/workflows/ci.yml": CI_OK, "docs/a.md": "plain text\n",
-            "formal/mutants/add-sub.patch": "",
+            "m.txt": "x\n", "formal/mutants/add-sub.patch": M_PATCH,
         })
         self.claims = self.d / "formal" / "claims.json"
         self.claims.write_text(json.dumps(base_claims(), indent=2) + "\n")
@@ -919,7 +922,7 @@ def test_unterminated_item_is_an_error(self):
 class DocsTable(unittest.TestCase):
     def setUp(self):
         self.d, self.git = make_repo({
-            "p.go": GO_FILE, ".github/workflows/ci.yml": CI_OK, "formal/mutants/add-sub.patch": "",
+            "p.go": GO_FILE, ".github/workflows/ci.yml": CI_OK, "m.txt": "x\n", "formal/mutants/add-sub.patch": M_PATCH,
             "docs/dev/FORMAL.md": "# Formal\n\nintro\n\n<!-- formal-claims:begin -->\nhand written\n<!-- formal-claims:end -->\n\ntail\n",
         })
         self.claims = self.d / "formal" / "claims.json"
@@ -1033,7 +1036,7 @@ def test_cli_render_docs(self):
 class CiRequiredAlways(unittest.TestCase):
     def check(self, ci_required_block):
         wf = "name: ci\non: push\njobs:\n  go:\n    runs-on: x\n  ci-required:\n" + ci_required_block
-        d, _ = make_repo({"p.go": GO_FILE, ".github/workflows/ci.yml": wf, "formal/mutants/add-sub.patch": ""})
+        d, _ = make_repo({"p.go": GO_FILE, ".github/workflows/ci.yml": wf, "m.txt": "x\n", "formal/mutants/add-sub.patch": M_PATCH})
         (d / "formal").mkdir(exist_ok=True)
         (d / "formal" / "claims.json").write_text(json.dumps(base_claims()))
         rep, _ = cc.run_all(d, d / "formal" / "claims.json")
@@ -1324,9 +1327,47 @@ def test_compile_break_kill_is_flagged(self):
     setattr(V2MutantRunner, _name, None)  # inherited tests already run in MutantRunner
 
 
+class StalePatch(unittest.TestCase):
+    """v2.1: every registered mutant patch must apply to the current tree (no build)."""
+
+    def setUp(self):
+        self.d, self.git = make_repo({
+            "p.go": GO_FILE, ".github/workflows/ci.yml": CI_OK, "m.txt": "x\n",
+            "formal/mutants/add-sub.patch": M_PATCH,
+        })
+        self.claims = self.d / "formal" / "claims.json"
+        self.claims.write_text(json.dumps(base_claims(), indent=2) + "\n")
+
+    def mutant_rows(self):
+        rep, _ = cc.run_all(self.d, self.claims, do_relock=True)
+        return [(ok, m) for c, ok, m in rep.rows if c.startswith("mutant add-sub")]
+
+    def test_applying_patch_passes(self):
+        self.assertEqual([ok for ok, _ in self.mutant_rows()], [True])
+
+    def test_stale_patch_fails_with_regenerate_hint(self):
+        (self.d / "m.txt").write_text("changed\n")
+        rows = self.mutant_rows()
+        self.assertEqual([ok for ok, _ in rows], [False])
+        self.assertIn("does not apply", rows[0][1])
+        self.assertIn("regenerate", rows[0][1])
+
+    def test_patch_shared_by_two_claims_is_checked_once(self):
+        d = base_claims()
+        d["claims"].append(dict(d["claims"][0], id="other"))
+        self.claims.write_text(json.dumps(d))
+        self.assertEqual(len(self.mutant_rows()), 1)
+
+    def test_mutated_tree_env_skips_the_check(self):
+        (self.d / "m.txt").write_text("y\n")  # the patch is already applied, as inside check_mutants
+        with mock.patch.dict(os.environ, {"FORMAL_KIT_MUTATED_TREE": "1"}):
+            self.assertEqual([ok for ok, _ in self.mutant_rows()], [True])
+        self.assertEqual([ok for ok, _ in self.mutant_rows()], [False])
+
+
 class KitVersion(unittest.TestCase):
     def test_version(self):
-        self.assertEqual(fk.KIT_VERSION, "2")
+        self.assertEqual(fk.KIT_VERSION, "2.1")
         import io
         from contextlib import redirect_stdout
         d, _ = make_repo({"x": "1"})