Tests: planted bugs as a script with a record, and clearer input labels

README.md

@@ -71,12 +71,15 @@ Needs Linux, [elan](https://github.com/leanprover/elan), bubblewrap (`apt instal
 lake build
 lake comparator --paranoid
 python3 tests/run_tests.py
+python3 tests/plant_bugs.py
 ```
 
 `lake comparator --paranoid` builds the statements and the proofs in a sandbox. It checks that each theorem in `Proofs/` proves exactly the statement in `Spec.lean`, using only the axioms `propext`, `Classical.choice`, and `Quot.sound`, and replays it through every kernel shipped with Lean.
 
 The test script compares the tool with python-semver. It runs every string of up to eight characters over `0`, `1`, `.`, `-`, `+` and `a`, the examples of the specification, and random and mutated versions from a recorded seed, then compares pairs of versions. It then rewrites `tests/TEST-RESULTS.md`. When Python lacks python-semver 3.1.0, it installs it into `.lake/oracle-venv`, checked against the hashes in `tests/oracle-requirements.txt`.
 
+`tests/plant_bugs.py` plants ten bugs in a copy of the code, one at a time, and records in `tests/PLANTED-BUGS.md` how many failures the tests report for each. Every bug must be caught, and each of them also breaks a proof.
+
 ## Layout
 
 - `SemVer/Types.lean`: the `Version` and `Ident` types.
@@ -91,3 +94,4 @@ The test script compares the tool with python-semver. It runs every string of up
 - `SPEC.md`: the specification in plain words.
 - `tests/run_tests.py`: the differential tests.
 - `tests/oracle-requirements.txt`: the oracle's version, pinned by hash.
+- `tests/plant_bugs.py` and `tests/PLANTED-BUGS.md`: the planted bugs, and the record that the tests catch each one.

bar.toml

@@ -7,8 +7,9 @@ name = "semver"
 status = "in-progress"
 page = "README.md"
 # GitHub handles of everyone who wrote the specification. It was drafted
-# by Claude, an AI agent, for the org, from the fdn-0 account.
-spec_authors = ["claude", "fdn-0"]
+# by Claude, an AI agent, for the org: agent fdn-claude, for the fdn-0
+# account, posting as zero-aska on GitHub.
+spec_authors = ["claude", "fdn-0", "zero-aska"]
 # The program people run. A change to it voids the approval.
 entry_points = ["Main.lean"]
 
@@ -29,4 +30,4 @@ code = ["SemVer.parse", "SemVer.Version.print", "SemVer.Version.compare"]
 [tests]
 results = "tests/TEST-RESULTS.md"
 command = "python3 tests/run_tests.py"
-files = ["tests/run_tests.py", "tests/oracle-requirements.txt"]
+files = ["tests/run_tests.py", "tests/oracle-requirements.txt", "tests/plant_bugs.py"]

tests/PLANTED-BUGS.md

@@ -0,0 +1,19 @@
+# Planted bugs
+
+Written by `tests/plant_bugs.py`. Each bug is a one-line change to `SemVer/Basic.lean`, tested with `tests/run_tests.py --count 2000`. Every bug must give failures, and the unchanged code none.
+
+| Planted bug | Failures |
+|---|---|
+| none | 0 |
+| leading zeros are accepted in numbers | 874 |
+| identifiers are compared by length only, not in ASCII order | 338 |
+| a hyphen is not an identifier character | 945 |
+| an empty build identifier is accepted | 257 |
+| a numeric identifier comes after an alphanumeric one | 309 |
+| a version with a pre-release part comes after the release | 163 |
+| pre-release identifiers are compared the wrong way round | 1471 |
+| build metadata takes part in precedence | 47 |
+| numeric identifiers are compared as text | 17 |
+| a hyphen in the build part starts the pre-release part | 1418 |
+
+Bugs caught: 10 of 10

tests/TEST-RESULTS.md

@@ -7,7 +7,7 @@ Written by `tests/run_tests.py`. Rerun it to check these numbers.
 - Seed: 20261025
 - Inputs: 3021721
 - Mutated: 449861 of the inputs are mutated versions
-- By kind: compare 150022, compare pool 6084, error 13, examples 85, grid 2015539, mutated 449861, random 100539, valid 299578
+- By kind: compare 150022, compare pool 6084, error 13, examples 85, grid 2015539, mutated 449861, random string 100539, random version 299578
 - Strings parsed: 2865602, of which 442325 accepted and 2423277 rejected
 - Accepted versions with a number of 2**64 or more: 72009
 - Pairs compared: 156106: < 66963, = 27956, > 61187, REJECT 0

tests/plant_bugs.py

@@ -0,0 +1,123 @@
+#!/usr/bin/env python3
+"""Check that the differential tests catch planted bugs.
+
+Each bug is a one-line change to SemVer/Basic.lean. The script
+copies the project to a temporary folder, plants one bug at a time,
+runs tests/run_tests.py there with a small count, and records how many
+failures the tests report. Every planted bug must give at least one.
+The unchanged copy must give none. Each bug also breaks a proof, so
+`lake build` of the whole project fails with it in place; the tests
+build only the executable, so they run.
+
+    python3 tests/plant_bugs.py [--count N]
+
+The script writes tests/PLANTED-BUGS.md and exits non-zero if any bug
+goes uncaught.
+"""
+
+import argparse
+import re
+import shutil
+import subprocess
+import sys
+import tempfile
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parent.parent
+RECORD = ROOT / "tests" / "PLANTED-BUGS.md"
+CODE = "SemVer/Basic.lean"
+
+# (what the bug does, the line as written, the line with the bug)
+BUGS = [
+    ('leading zeros are accepted in numbers',
+     "if (c :: cs).all isDigit && (c != '0' || cs.isEmpty) then",
+     'if (c :: cs).all isDigit then'),
+    ('identifiers are compared by length only, not in ASCII order',
+     '| a :: as, b :: bs => (compare a.toNat b.toNat).then (compareAscii as bs)',
+     '| _ :: as, _ :: bs => compareAscii as bs'),
+    ('a hyphen is not an identifier character',
+     "|| c == '-'",
+     ''),
+    ('an empty build identifier is accepted',
+     'if !cs.isEmpty && cs.all isIdentChar then some (String.ofList cs) else none',
+     'if cs.all isIdentChar then some (String.ofList cs) else none'),
+    ('a numeric identifier comes after an alphanumeric one',
+     '| .num _, .alnum _ => .lt',
+     '| .num _, .alnum _ => .gt'),
+    ('a version with a pre-release part comes after the release',
+     '| [], _ :: _ => .gt',
+     '| [], _ :: _ => .lt'),
+    ('pre-release identifiers are compared the wrong way round',
+     '| a :: as, b :: bs => (a.compare b).then (compareIdents as bs)',
+     '| a :: as, b :: bs => (b.compare a).then (compareIdents as bs)'),
+    ('build metadata takes part in precedence',
+     '(Ord.compare a.patch b.patch).then (comparePre a.pre b.pre)',
+     '(Ord.compare a.patch b.patch).then ((comparePre a.pre b.pre).then (Ord.compare a.build.length b.build.length))'),
+    ('numeric identifiers are compared as text',
+     '| .num a, .num b => Ord.compare a b',
+     '| .num a, .num b => compareAscii (toString a).toList (toString b).toList'),
+    ('a hyphen in the build part starts the pre-release part',
+     "let (core, prePart) := breakAt '-' main",
+     "let (core, prePart) := breakAt '-' cs"),
+]
+
+
+def failures(copy, count):
+    """The failures a run of the tests reports, or None, with the run's
+    output, when it reports none: the code did not build, or the run did
+    not finish. A run that dies writes no record, so the old one is
+    removed first rather than read again."""
+    record = copy / "tests" / "TEST-RESULTS.md"
+    record.unlink(missing_ok=True)
+    run = subprocess.run([sys.executable, "tests/run_tests.py", "--count", str(count)],
+                         cwd=copy, capture_output=True, text=True)
+    out = run.stdout + run.stderr
+    if not record.exists():
+        return None, f"no record written, exit status {run.returncode}\n{out}"
+    m = re.search(r"^- Failures: (\d+)(.*)$", record.read_text(encoding="utf-8"), re.M)
+    if m is None or m.group(2).strip():
+        return None, out  # the bug did not build: not a catch
+    n = int(m.group(1))
+    if run.returncode != (1 if n else 0):
+        return None, f"{n} failures but exit status {run.returncode}\n{out}"
+    return n, None
+
+
+def main():
+    ap = argparse.ArgumentParser()
+    ap.add_argument("--count", type=int, default=2000)
+    args = ap.parse_args()
+    rows, missed = [], 0
+    with tempfile.TemporaryDirectory() as tmp:
+        copy = Path(tmp) / "semver"
+        shutil.copytree(ROOT, copy, symlinks=True,
+                        ignore=shutil.ignore_patterns("PLANTED-BUGS.md"))
+        code = copy / CODE
+        original = code.read_text(encoding="utf-8")
+        n, err = failures(copy, args.count)
+        rows.append(("none", n))
+        if n != 0:
+            missed += 1
+        for what, line, bug in BUGS:
+            if original.count(line) != 1:
+                sys.exit(f"{CODE} no longer holds, once, the line for {what!r}: {line}")
+            code.write_text(original.replace(line, bug), encoding="utf-8")
+            n, err = failures(copy, args.count)
+            code.write_text(original, encoding="utf-8")
+            rows.append((what, n))
+            if not n:
+                missed += 1
+            print(f"{what}: {n} failures" + (" (did not build or did not finish)" if err else ""))
+    lines = ["# Planted bugs", "",
+             "Written by `tests/plant_bugs.py`. Each bug is a one-line change to "
+             f"`{CODE}`, tested with `tests/run_tests.py --count {args.count}`. "
+             "Every bug must give failures, and the unchanged code none.", "",
+             "| Planted bug | Failures |", "|---|---|"]
+    lines += [f"| {what} | {'did not build or did not finish' if n is None else n} |" for what, n in rows]
+    lines += ["", f"Bugs caught: {sum(1 for what, n in rows[1:] if n)} of {len(BUGS)}", ""]
+    RECORD.write_text("\n".join(lines), encoding="utf-8")
+    return 1 if missed else 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())

tests/run_tests.py

@@ -346,7 +346,7 @@ def cases(seed, count):
     for _ in range(count):
         r = rng.random()
         if r < 0.3:
-            yield parse_case("valid", random_version(rng))
+            yield parse_case("random version", random_version(rng))
         elif r < 0.75:
             base = random_version(rng)
             s = mutate(rng, base)
@@ -355,7 +355,7 @@ def cases(seed, count):
             yield parse_case("mutated", s, True)
         elif r < 0.85:
             n = rng.randint(0, 12)
-            yield parse_case("random", "".join(rng.choice("0123456789.-+aZ" + "".join(OTHER_CHARS[:3]))
+            yield parse_case("random string", "".join(rng.choice("0123456789.-+aZ" + "".join(OTHER_CHARS[:3]))
                                                for _ in range(n)))
         else:
             a = random_version(rng)