diff --git a/README.md b/README.md index c508a02..1cd58bc 100644 --- a/README.md +++ b/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. diff --git a/bar.toml b/bar.toml index 77cf39d..6aeb37f 100644 --- a/bar.toml +++ b/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"] diff --git a/tests/PLANTED-BUGS.md b/tests/PLANTED-BUGS.md new file mode 100644 index 0000000..cbf6f38 --- /dev/null +++ b/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 diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md index d102248..2e85303 100644 --- a/tests/TEST-RESULTS.md +++ b/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 diff --git a/tests/plant_bugs.py b/tests/plant_bugs.py new file mode 100644 index 0000000..bc616bf --- /dev/null +++ b/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()) diff --git a/tests/run_tests.py b/tests/run_tests.py index 68c780a..689b438 100644 --- a/tests/run_tests.py +++ b/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)