From 72d42037bb6aea5a95ca828a11a523d552adc87b Mon Sep 17 00:00:00 2001 From: zachyking Date: Sat, 10 Oct 2026 19:34:46 +0100 Subject: [PATCH] formal: vendor kit v2.1 --- scripts/formal/README.md | 5 ++-- scripts/formal/check_claims.py | 22 +++++++++++++- scripts/formal/check_mutants.py | 2 +- scripts/formal/formal_kit.py | 2 +- scripts/formal/tests/test_kit.py | 49 +++++++++++++++++++++++++++++--- 5 files changed, 71 insertions(+), 9 deletions(-) diff --git a/scripts/formal/README.md b/scripts/formal/README.md index e31eac9..e383629 100644 --- a/scripts/formal/README.md +++ b/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. diff --git a/scripts/formal/check_claims.py b/scripts/formal/check_claims.py index 74b2d4d..f96842f 100644 --- a/scripts/formal/check_claims.py +++ b/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" diff --git a/scripts/formal/check_mutants.py b/scripts/formal/check_mutants.py index 1b0386b..41233e4 100644 --- a/scripts/formal/check_mutants.py +++ b/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 diff --git a/scripts/formal/formal_kit.py b/scripts/formal/formal_kit.py index a4f23d4..f8d4b4e 100644 --- a/scripts/formal/formal_kit.py +++ b/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", diff --git a/scripts/formal/tests/test_kit.py b/scripts/formal/tests/test_kit.py index 3c4da0a..c090168 100644 --- a/scripts/formal/tests/test_kit.py +++ b/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\nhand written\n\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"})