From ef1108e5336ce78ccbc958c42c291c19d0ae936c Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 20:37:45 +0000 Subject: [PATCH 1/2] Tests: planted bugs as a script with a record; clearer input labels Follow-up to PR 3, as promised in its review thread. The two planted bugs whose counts the PR body gave by hand now run from tests/plant_bugs.py, with eight more, and tests/PLANTED-BUGS.md records the result: 10 of 10 caught, including the two original counts, 874 and 338. A bug that does not build, or a run that does not finish, is not counted as caught. The record's input kinds 'valid' and 'random' become 'random version' and 'random string', so the two read apart. The counts are unchanged: 3,021,721 inputs, 0 failures. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd --- README.md | 4 ++ bar.toml | 2 +- tests/PLANTED-BUGS.md | 19 +++++++ tests/TEST-RESULTS.md | 2 +- tests/plant_bugs.py | 123 ++++++++++++++++++++++++++++++++++++++++++ tests/run_tests.py | 4 +- 6 files changed, 150 insertions(+), 4 deletions(-) create mode 100644 tests/PLANTED-BUGS.md create mode 100644 tests/plant_bugs.py 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..801b45d 100644 --- a/bar.toml +++ b/bar.toml @@ -29,4 +29,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..6fe66b8 --- /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 "build" in m.group(2): + 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) From 90b2c768d18729e74169cbb95129819079fee61f Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 01:25:09 +0000 Subject: [PATCH 2/2] spec_authors names zero-aska bar.toml listed the spec authors as claude and fdn-0. The commits and pull requests come from the GitHub account zero-aska, so bar item 1's independence check would not have refused an approval from it. The same fix went into hostname#2, punycode#2 and bech32#2. plant_bugs.py also counts any run that gives up as missed, as in those repos. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd --- bar.toml | 5 +++-- tests/plant_bugs.py | 2 +- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/bar.toml b/bar.toml index 801b45d..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"] diff --git a/tests/plant_bugs.py b/tests/plant_bugs.py index 6fe66b8..bc616bf 100644 --- a/tests/plant_bugs.py +++ b/tests/plant_bugs.py @@ -75,7 +75,7 @@ def failures(copy, count): 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 "build" in m.group(2): + 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):