From 6baf29185781a435cfe307b5bdc27880e0cdddba Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 24 Oct 2026 02:02:14 -0400 Subject: [PATCH] ci: ratchet public tidy statements per module (#456 S3) Add `scripts/check_tidy_surface.py`, which counts, per module of the `Complexity` library, the public declarations whose statement mentions tidy computability: a tidy constant in the type (theorems, definitions, structure fields) or in the exposed body of a definition outside proofs. Proofs, bodies that are not exposed and private declarations do not count, and the 23 raw machine modules of `scripts/tidy_allowlist.txt` (#608) are exempt. Every module's count must equal its entry in `scripts/tidy_surface_baseline.json` (2041 statements in 426 modules on main c1762c51): growth fails, and so does a stale entry until `--update` lowers it, so a removed statement cannot come back on the leftover allowance. `--update` refuses to raise an entry without `--allow-increase`. `scripts/QualityReport.lean` computes `tb` without proofs: subterms whose type is a proposition, and the statement and value of a `let` or `have` whose type is a proposition. Telling them apart needs types, so the modules of the exposed definitions whose body mentions a tidy constant are imported (at the exported level) and their rows printed last. #666's `ph`/`sg` fields and `--names` mode are kept; its raw body scan is replaced. `scripts/tidy_sweep.py`'s docstring says so. The check reads the build outputs through `scripts/quality_report.py`, unchanged, and runs in CI after `lake test`, first running its tests, whose compiled-module cases need Lean. CONTRIBUTING.md states the rule, including that a PR must rebase and rerun `--update` when another merge removes tidy statements first. Review 5636914097 (proof-local tidy in exposed bodies, stale baseline allowance) is addressed by the proof-aware `tb`, the stale-entry failure, and their regression tests. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- .github/workflows/lean_action_ci.yml | 11 + CONTRIBUTING.md | 11 + scripts/QualityReport.lean | 68 ++++- scripts/check_tidy_surface.py | 151 ++++++++++ scripts/test_check_tidy_surface.py | 321 ++++++++++++++++++++ scripts/tidy_surface_baseline.json | 428 +++++++++++++++++++++++++++ scripts/tidy_sweep.py | 4 +- 7 files changed, 986 insertions(+), 8 deletions(-) create mode 100644 scripts/check_tidy_surface.py create mode 100644 scripts/test_check_tidy_surface.py create mode 100644 scripts/tidy_surface_baseline.json diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 32d2ac161..18e23241b 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -84,6 +84,17 @@ jobs: with: path: ./.lake key: ${{ steps.lake-cache.outputs.cache-primary-key }} + # Source hygiene that needs the build outputs: each module's count of public statements that + # mention tidy computability (#456) must equal its baseline; proofs may use it. See + # scripts/check_tidy_surface.py. Its tests on a compiled module need Lean, so the Python + # tests at the start skip them; they run here. + - name: "Tidy statement ratchet" + run: | + set -e + command -v lake + test -d .lake/packages + python3 -B -m unittest scripts/test_check_tidy_surface.py + python3 -B scripts/check_tidy_surface.py - name: "lake exe mk_all --check" run: | set -e diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 8c76fdc5d..9fd59cde2 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -71,6 +71,17 @@ also loads private information, so such edits do reach its clients. unfold a definition by name. Reduction by `rfl` or `decide` is not recorded, and its counts are review signals, not rules. +Tidy computability (`ComputableTidily…`, `ComputesTidily…`, `IsTidy…`) may appear anywhere inside +proofs, through `.tidy`, `.of_tidy`, a proof-local `attribute [local fun_prop] … in` or a tidy +`have`. It never appears in a public statement: a theorem's type, or a definition's type, exposed +body or fields. Only the raw machine constructions in `scripts/tidy_allowlist.txt` are exempt. +CI enforces this with `scripts/check_tidy_surface.py`. The existing tidy statements, which #456 is +restating, are counted per module in `scripts/tidy_surface_baseline.json`, and CI fails when a +module's count differs from its entry. When you remove some, lower the baseline in the same PR +with `python3 scripts/check_tidy_surface.py --update`, so that they cannot come back. Until your +PR lands, any other merge that removes tidy statements makes your baseline stale: rebase and +rerun `--update`. + ## AI assistance and review AI-assisted and human-written contributions follow the same standards. Disclose which AI tools diff --git a/scripts/QualityReport.lean b/scripts/QualityReport.lean index 9a53f95ee..af4348413 100644 --- a/scripts/QualityReport.lean +++ b/scripts/QualityReport.lean @@ -21,7 +21,11 @@ constant: exposed as an `axiom`, and an exposed definition as a `def`; * `doc`: whether it has a docstring (Markdown, Verso or `@[inherit_doc]`); * `tidy`: the constants named `ComputableTidily…`, `ComputesTidily…` or `IsTidy…` in its type; - `tb`: those in its exposed body, for an exported definition; + `tb`: for an exported definition, those in its exposed body outside proofs. Proofs are the + subterms whose type is a proposition, together with the statements of proof-local `have`s (a + `let` whose type is a proposition): tidy computability is allowed there (#456). Telling them + apart needs types, so the modules of the definitions whose body mentions a tidy constant are + imported (at the exported level) for this, and their rows are printed last; * `u`: for an exported constant, the other constants of the same module that its exported statement or exposed body mentions (these cannot become private while it stays public); * `r`: its declaration range `[line, column, endLine, endColumn, selLine, selColumn, selEndLine, @@ -66,6 +70,47 @@ def isTidy (n : Name) : Bool := s.startsWith "IsTidy" | _ => false +def mentionsTidy (e : Expr) : Bool := + e.getUsedConstants.any isTidy + +/-- Add to `found` the tidy constants of `e` outside proofs: subterms whose type is a proposition, +and the type and value of a `let` or `have` whose type is a proposition. A subterm whose type +cannot be inferred counts as a non-proof. -/ +partial def tidyOutsideProofs (found : IO.Ref NameSet) (e : Expr) : MetaM Unit := do + unless mentionsTidy e do return + if ← (try Meta.isProof e catch _ => pure false) then return + match e with + | .const n _ => if isTidy n then found.modify (·.insert n) + | .app f a => tidyOutsideProofs found f; tidyOutsideProofs found a + | .mdata _ b | .proj _ _ b => tidyOutsideProofs found b + | .lam n t b bi | .forallE n t b bi => + tidyOutsideProofs found t + Meta.withLocalDecl n bi t fun x => tidyOutsideProofs found (b.instantiate1 x) + | .letE n t v b _ => + unless ← (try Meta.isProp t catch _ => pure false) do + tidyOutsideProofs found t + tidyOutsideProofs found v + Meta.withLetDecl n t v fun x => tidyOutsideProofs found (b.instantiate1 x) + | _ => pure () + +/-- `tidyOutsideProofs` for the exposed bodies of the definitions `names` of `modules`, which are +imported (at the exported level, as by a client) from the search path of `lake env` and +`libDir`. -/ +unsafe def tidyBodies (libDir : System.FilePath) (modules : Array Name) (names : Array Name) : + IO (NameMap (Array String)) := do + if names.isEmpty then return {} + initSearchPath (← findSysroot) [libDir] + let env ← importModules (modules.map ({ module := · })) {} (level := .exported) + let ctx : Core.Context := { fileName := "", fileMap := default } + let mut result : NameMap (Array String) := {} + for n in names do + let some (.defnInfo v) := env.find? n + | throw <| IO.userError s!"cannot find the exposed body of {n}" + let found ← IO.mkRef {} + discard <| (tidyOutsideProofs found v.value).toIO ctx { env } + result := result.insert n ((← found.get).toArray.map toString) + return result + /-- The declarations named by entries of the extensions whose names end in one of `suffixes`. Every such extension is a `MapDeclarationExtension`, whose entries are pairs headed by a name. -/ unsafe def entryNames (entries : Array (Name × Array EnvExtensionEntry)) (suffixes : List String) : @@ -143,6 +188,9 @@ unsafe def run (libDir : System.FilePath) (pairs : Option String := none) : IO U let mut defs : Std.HashMap (Expr × Expr) (Array (String × Name)) := {} -- The mapped regions must stay alive while `theorems` and `defs` refer to their expressions. let mut regions : Array CompactedRegion := #[] + -- Rows of exposed definitions whose body mentions a tidy constant wait for `tidyBodies`. + let mut deferred : Array (Name × List (String × Json)) := #[] + let mut bodyModules : NameSet := {} repeat let line ← stdin.getLine if line.isEmpty then break @@ -168,12 +216,9 @@ unsafe def run (libDir : System.FilePath) (pairs : Option String := none) : IO U | some ec => ec.type.getUsedConstants | none => #[] let uses := uses.filter (fun n => n != c.name && sameModule.contains n) |>.toList.eraseDups - let tidyBody := match e with - | some (.defnInfo v) => v.value.getUsedConstants.filter isTidy |>.map Name.toString - | _ => #[] let mut row : List (String × Json) := [ ("n", c.name.toString), ("m", mod), ("k", kindOf c), ("e", (e.map kindOf).getD ""), - ("doc", docs.contains c.name), ("tidy", toJson tidy), ("tb", toJson tidyBody), + ("doc", docs.contains c.name), ("tidy", toJson tidy), ("u", toJson (uses.map (·.toString))), ("r", (ranges.find? c.name).map rangeJson |>.getD .null)] if pairs.isSome then @@ -182,7 +227,14 @@ unsafe def run (libDir : System.FilePath) (pairs : Option String := none) : IO U row := row ++ [("ph", toJson (toString hash))] if c.type.getUsedConstants.any preds.contains then row := row ++ [("sg", signature preds c.type)] - stdout.putStrLn <| Json.compress <| Json.mkObj row + let tidyBody := match e with + | some (.defnInfo v) => mentionsTidy v.value + | _ => false + if tidyBody then + deferred := deferred.push (c.name, row) + bodyModules := bodyModules.insert mod.toName + else + stdout.putStrLn <| Json.compress <| Json.mkObj (row ++ [("tb", Json.arr #[])]) if let some ec := e then unless c.name.isInternalDetail do match c, ec with @@ -193,6 +245,10 @@ unsafe def run (libDir : System.FilePath) (pairs : Option String := none) : IO U let key := (normalize ec ec.type, normalize ec v.value) defs := defs.insert key ((defs.getD key #[]).push (mod, c.name)) | _, _ => pure () + let bodies ← tidyBodies libDir bodyModules.toArray (deferred.map (·.1)) + for (n, row) in deferred do + let tb := (bodies.find? n).getD #[] + stdout.putStrLn <| Json.compress <| Json.mkObj (row ++ [("tb", toJson tb)]) let emit (kind : String) (group : Array (String × Name)) : IO Unit := do if (group.map (·.1)).toList.eraseDups.length > 1 then stdout.putStrLn <| Json.compress <| Json.mkObj [ diff --git a/scripts/check_tidy_surface.py b/scripts/check_tidy_surface.py new file mode 100644 index 000000000..8e3f09582 --- /dev/null +++ b/scripts/check_tidy_surface.py @@ -0,0 +1,151 @@ +#!/usr/bin/env python3 +"""Stop tidy computability from spreading into public statements (S3 of #456). + +Usage: python3 scripts/check_tidy_surface.py [--update [--allow-increase]] [--no-build-check] + +Tidy computability (`ComputableTidily…`, `ComputesTidily…`, `IsTidy…`) is a proof device: it may +appear anywhere inside proofs, never in a public statement. A public declaration of the +`Complexity` library has a *tidy statement* when a tidy constant occurs in its type (a theorem's +statement, a definition's type, a structure field) or in the exposed body of a definition. +Proofs, bodies that are not exposed and private declarations do not count, and neither do the raw +machine constructions listed in `scripts/tidy_allowlist.txt` (#608). + +The check counts tidy statements per module and compares the counts with +`scripts/tidy_surface_baseline.json`, which records those that #456's sweep has yet to restate. +Every count must equal its baseline entry (a module without an entry, such as a new one, has +none). A count above its entry is a new tidy statement. A count below it fails too, until the +baseline is lowered in the same change: otherwise the unused allowance would let a removed +statement come back later. `--update` rewrites the baseline with the current counts; it refuses +to raise an entry unless `--allow-increase` is given, for instance when a module that has tidy +statements is moved. + +Declarations written in source come from the `.ilean` files and statements from the `.olean` +files, read by `scripts/quality_report.py` and `scripts/QualityReport.lean`. The check needs the +build outputs of `lake build Complexity ComplexityTests ComplexityAbstracts` (`lake build` and +`lake test`), and refuses stale ones unless `--no-build-check` is given. +""" + +from __future__ import annotations + +import argparse +import json +import sys +from collections import defaultdict +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[1] +sys.path.insert(0, str(ROOT / "scripts")) +import quality_report as qr # noqa: E402 + +ALLOWLIST = ROOT / "scripts/tidy_allowlist.txt" +BASELINE = ROOT / "scripts/tidy_surface_baseline.json" +UPDATE = "python3 scripts/check_tidy_surface.py --update" + +# A tidy statement: the declaration, its line, and the tidy constants it mentions. +Statement = tuple[str, int, list[str]] + + +def load_allowlist(path: Path) -> set[str]: + """Source paths relative to the repository root, one per line; `#` starts a comment.""" + return {line.split("#", 1)[0].strip() for line in path.read_text().splitlines()} - {""} + + +def tidy_statements(lib: qr.Library, allowlist: set[str]) -> dict[str, list[Statement]]: + """The tidy statements of each module outside the allowlist, by source path. Declarations + written in source count, structure fields included; constants generated from them (`simps` + lemmas, equation lemmas, recursors) do not.""" + decls, _, _ = qr.collect_declarations(lib) + found: dict[str, list[Statement]] = defaultdict(list) + for name, decl in decls.items(): + if decl["role"] == "generated": + continue + const = lib.constants[name] + mentions = sorted(set(const["tidy"]) | set(const.get("tb", ()))) + path = "Complexity/" + decl["path"] + if mentions and path not in allowlist: + found[path].append((name, decl["range"][0] if decl["range"] else 0, mentions)) + return {path: sorted(rows, key=lambda row: (row[1], row[0])) for path, rows in found.items()} + + +def load_baseline(path: Path) -> dict[str, int]: + data = json.loads(path.read_text()) + if not isinstance(data, dict) or not all( + isinstance(k, str) and type(v) is int and v > 0 for k, v in data.items()): + sys.exit(f"{path}: expected a JSON object from source paths to positive counts") + return data + + +def baseline_text(counts: dict[str, int]) -> str: + return json.dumps({k: v for k, v in sorted(counts.items()) if v}, indent=1) + "\n" + + +def compare(counts: dict[str, int], baseline: dict[str, int] + ) -> tuple[dict[str, tuple[int, int]], dict[str, tuple[int, int]]]: + """`(over, under)`: the modules whose count exceeds or falls short of their baseline entry, + as `path -> (count, entry)`. A module without an entry has entry 0.""" + over, under = {}, {} + for path in sorted(set(counts) | set(baseline)): + count, entry = counts.get(path, 0), baseline.get(path, 0) + if count > entry: + over[path] = (count, entry) + elif count < entry: + under[path] = (count, entry) + return over, under + + +def over_report(over: dict[str, tuple[int, int]], found: dict[str, list[Statement]]) -> str: + out = ["Public statements may not mention tidy computability, only proofs may (#456). Restate " + "these with plain computability (`ComputableInPolyTime`, `ComputableInTimeAndSpace`, " + "…) and switch inside the proofs (`.tidy`, `.of_tidy`).", ""] + for path, (count, entry) in over.items(): + out.append(f"{path}: {count} tidy statement(s), baseline {entry}:") + out += [f" {path}:{line}: {name} mentions {', '.join(mentions)}" + for name, line, mentions in found.get(path, [])] + return "\n".join(out) + + +def main(argv: list[str] | None = None) -> int: + parser = argparse.ArgumentParser(description=__doc__, + formatter_class=argparse.RawDescriptionHelpFormatter) + parser.add_argument("--update", action="store_true", + help="rewrite the baseline with the current counts") + parser.add_argument("--allow-increase", action="store_true", + help="with --update, allow raising entries and adding modules") + parser.add_argument("--no-build-check", action="store_true", + help="do not check that the build outputs are current") + parser.add_argument("--allowlist", type=Path, default=ALLOWLIST) + parser.add_argument("--baseline", type=Path, default=BASELINE) + args = parser.parse_args(argv) + if args.allow_increase and not args.update: + parser.error("--allow-increase needs --update") + qr.check_outputs(qr.DEFAULT_BUILD_DIR, args.no_build_check) + found = tidy_statements(qr.Library(qr.DEFAULT_BUILD_DIR), load_allowlist(args.allowlist)) + counts = {path: len(rows) for path, rows in found.items()} + baseline = load_baseline(args.baseline) if args.baseline.exists() else {} + over, under = compare(counts, baseline) + summary = f"{sum(counts.values())} public tidy statement(s) in {len(counts)} module(s)" + if args.update: + if over and not args.allow_increase: + print(over_report(over, found), file=sys.stderr) + print("\nThe baseline only goes down; pass --allow-increase to raise it on purpose, " + "for instance for a moved module.", file=sys.stderr) + return 1 + args.baseline.write_text(baseline_text(counts)) + print(f"Wrote {args.baseline}: {summary}.") + return 0 + if over: + print(over_report(over, found), file=sys.stderr) + if under: + print(("\n" if over else "") + "Tidy statements were removed, so the baseline is stale. " + f"Lower it with `{UPDATE}` and commit the result, so that they cannot come back:", + file=sys.stderr) + print("\n".join(f" {path}: {count} (baseline {entry})" + for path, (count, entry) in under.items()), file=sys.stderr) + if over or under: + return 1 + print(f"{summary}, matching the baseline.") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/scripts/test_check_tidy_surface.py b/scripts/test_check_tidy_surface.py new file mode 100644 index 000000000..0ceb2683a --- /dev/null +++ b/scripts/test_check_tidy_surface.py @@ -0,0 +1,321 @@ +"""Unit tests for scripts/check_tidy_surface.py, on synthetic build outputs and, when Lean is +available, on a compiled module (`CompiledFixtureTests`). + +The fixtures have the shape of what `scripts/QualityReport.lean` and the `.ilean` files record for +a module like this one, where only `stated`, `exposed` and `Cert.cert` have tidy statements: + + theorem proved (h : ComputableInPolyTime f e e') : ComputableInPolyTime f e e' := by + have h' : ComputableTidilyInPolyTime f e e' := h.tidy + exact .of_tidy h' + theorem stated (h : ComputableInPolyTime f e e') : ComputableTidilyInPolyTime f e e' := h.tidy + private theorem hidden (h : …) : ComputableTidilyInPolyTime f e e' := h.tidy + @[expose] def exposed … : Prop := ComputableTidilyInPolyTime f e e' + def opaqueBody … : Prop := ComputableTidilyInPolyTime f e e' + structure Cert … : Prop where + cert : ComputableTidilyInPolyTime f e e' +""" + +from __future__ import annotations + +import contextlib +import io +import json +import pathlib +import shutil +import subprocess +import sys +import tempfile +import unittest +from unittest import mock + +sys.path.insert(0, str(pathlib.Path(__file__).resolve().parent)) +import check_tidy_surface as c # noqa: E402 +import quality_report as q # noqa: E402 + +TIDY = "Turing.MultiTapeTM.ComputableTidilyInPolyTime" +PLAIN = "Turing.MultiTapeTM.ComputableInPolyTime" +TIDY_MODULE = "Complexity.Machines.Tidy" + + +def declaration(module: str, name: str, line: int, kind: str = "thm", exported: str = "axiom", + tidy: tuple[str, ...] = (), body: tuple[str, ...] = (), + parent: str | None = None) -> tuple[str, dict, dict]: + """The `.ilean` reference key and entry of a declaration, and its constant row.""" + key = json.dumps({"c": {"m": module, "n": name}}) + span = [line - 1, 8, line - 1, 8 + len(name)] + info = {"definition": span + ([parent] if parent else []), "usages": []} + row = {"n": name, "m": module, "k": kind, "e": exported, "doc": True, "tidy": list(tidy), + "tb": list(body), "u": [], "r": [line, 0, line + 2, 0, line, 8, line, 8 + len(name)]} + return key, info, row + + +def reference(name: str, line: int, user: str) -> tuple[str, dict, None]: + """The `.ilean` entry of a reference to `name`, from another module, in `user`'s proof.""" + key = json.dumps({"c": {"m": TIDY_MODULE, "n": name}}) + return key, {"definition": None, "usages": [[line - 1, 4, line - 1, 30, user]]}, None + + +def module_fixture(module: str, short: str) -> list[tuple[str, dict, dict | None]]: + """The declarations of the module in the docstring, named `short.…`, and the references to + the predicates from their proofs.""" + return [ + reference(TIDY, 11, f"{short}.proved"), + reference(PLAIN, 15, f"{short}.stated"), + declaration(module, f"{short}.proved", 10), + declaration(module, f"{short}.stated", 15, tidy=(TIDY,)), + declaration(module, f"_private.{module}.0.{short}.hidden", 18, exported="", + tidy=(TIDY,)), + declaration(module, f"{short}.exposed", 21, kind="def", exported="def", body=(TIDY,)), + declaration(module, f"{short}.opaqueBody", 24, kind="def"), + declaration(module, f"{short}.Cert", 27, kind="induct", exported="induct", + parent=f"{short}.Cert"), + declaration(module, f"{short}.Cert.cert", 28, tidy=(TIDY,), parent=f"{short}.Cert"), + ] + + +class FakeLibrary(q.Library): + """`quality_report.Library` over in-memory `.ilean` data and constant rows.""" + + def __init__(self, modules: dict[str, list[tuple[str, dict, dict | None]]]): + self.ileans, self.constants, self.sources = {}, {}, {} + for module, entries in modules.items(): + self.ileans[module] = {"module": module, "directImports": [], + "references": {key: info for key, info, _ in entries}} + self.constants.update({row["n"]: row for _, _, row in entries if row}) + self.modules = sorted(self.ileans) + self.duplicate_rows = [] + + +class CountingTests(unittest.TestCase): + def setUp(self) -> None: + module = "Complexity.Classes.A" + self.lib = FakeLibrary({module: module_fixture(module, "A")}) + + def names(self, allowlist: set[str] = frozenset()) -> list[str]: + found = c.tidy_statements(self.lib, set(allowlist)) + return [name for rows in found.values() for name, _, _ in rows] + + def test_statements_count_and_proofs_do_not(self) -> None: + found = c.tidy_statements(self.lib, set()) + self.assertEqual(list(found), ["Complexity/Classes/A.lean"]) + self.assertEqual(found["Complexity/Classes/A.lean"][0], ("A.stated", 15, [TIDY])) + # `proved` mentions the tidy predicate in its proof only. + self.assertNotIn("A.proved", self.names()) + + def test_private_declarations_do_not_count(self) -> None: + self.assertFalse([n for n in self.names() if "hidden" in n]) + + def test_exposed_bodies_and_fields_count(self) -> None: + self.assertEqual(self.names(), ["A.stated", "A.exposed", "A.Cert.cert"]) + self.assertNotIn("A.opaqueBody", self.names()) + + def test_allowlisted_modules_are_exempt(self) -> None: + self.assertEqual(self.names({"Complexity/Classes/A.lean"}), []) + self.assertEqual(len(self.names({"Complexity/Classes/B.lean"})), 3) + + def test_generated_constants_do_not_count(self) -> None: + key, info, row = declaration("Complexity.Classes.A", "A.exposed_apply", 30, + tidy=(TIDY,), parent="A.exposed") + self.lib.ileans["Complexity.Classes.A"]["references"][key] = info + self.lib.constants[row["n"]] = row + self.assertNotIn("A.exposed_apply", self.names()) + + +class RatchetTests(unittest.TestCase): + def test_compare(self) -> None: + over, under = c.compare({"A.lean": 3, "B.lean": 1, "New.lean": 1}, + {"A.lean": 2, "B.lean": 4, "Gone.lean": 5}) + self.assertEqual(over, {"A.lean": (3, 2), "New.lean": (1, 0)}) + self.assertEqual(under, {"B.lean": (1, 4), "Gone.lean": (0, 5)}) + + def test_baseline_text_drops_empty_modules(self) -> None: + self.assertEqual(json.loads(c.baseline_text({"B.lean": 2, "A.lean": 0})), {"B.lean": 2}) + + def test_malformed_baseline_is_refused(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + path = pathlib.Path(tmp) / "baseline.json" + for text in ('["A.lean"]', '{"A.lean": 0}', '{"A.lean": "2"}', '{"A.lean": true}'): + path.write_text(text) + with self.assertRaises(SystemExit, msg=text): + c.load_baseline(path) + + +class MainTests(unittest.TestCase): + """The command on the fixture library, with a temporary allowlist and baseline.""" + + def setUp(self) -> None: + tmp = tempfile.TemporaryDirectory() + self.addCleanup(tmp.cleanup) + self.dir = pathlib.Path(tmp.name) + self.allowlist = self.dir / "allowlist.txt" + self.allowlist.write_text("# raw machines\nComplexity/Machines/Raw.lean\n") + self.baseline = self.dir / "baseline.json" + self.modules = {m: module_fixture(m, m.rsplit(".", 1)[-1]) + for m in ("Complexity.Classes.A", "Complexity.Machines.Raw")} + + def run_main(self, baseline: dict[str, int] | None, *flags: str) -> tuple[int, str, str]: + if baseline is not None: + self.baseline.write_text(json.dumps(baseline)) + out, err = io.StringIO(), io.StringIO() + with mock.patch.object(q, "Library", lambda _: FakeLibrary(self.modules)), \ + contextlib.redirect_stdout(out), contextlib.redirect_stderr(err): + code = c.main(["--no-build-check", "--allowlist", str(self.allowlist), + "--baseline", str(self.baseline), *flags]) + return code, out.getvalue(), err.getvalue() + + def test_at_the_baseline_passes(self) -> None: + code, out, _ = self.run_main({"Complexity/Classes/A.lean": 3}) + self.assertEqual(code, 0) + self.assertIn("3 public tidy statement(s) in 1 module(s)", out) + + def test_growth_fails(self) -> None: + code, _, err = self.run_main({"Complexity/Classes/A.lean": 2}) + self.assertEqual(code, 1) + self.assertIn("Complexity/Classes/A.lean: 3 tidy statement(s), baseline 2", err) + self.assertIn("Complexity/Classes/A.lean:15: A.stated mentions " + TIDY, err) + + def test_new_module_with_a_tidy_statement_fails(self) -> None: + self.modules["Complexity.Classes.New"] = [ + declaration("Complexity.Classes.New", "New.ok", 10), + declaration("Complexity.Classes.New", "New.bad", 12, tidy=(TIDY,))] + code, _, err = self.run_main({"Complexity/Classes/A.lean": 3}) + self.assertEqual(code, 1) + self.assertIn("Complexity/Classes/New.lean: 1 tidy statement(s), baseline 0", err) + self.assertNotIn("Complexity/Classes/A.lean", err) + + def test_missing_baseline_allows_nothing(self) -> None: + code, _, err = self.run_main(None) + self.assertEqual(code, 1) + self.assertIn("Complexity/Classes/A.lean: 3 tidy statement(s), baseline 0", err) + + def test_stale_baseline_fails(self) -> None: + code, _, err = self.run_main({"Complexity/Classes/A.lean": 5, "Complexity/Gone.lean": 1}) + self.assertEqual(code, 1) + self.assertIn(c.UPDATE, err) + self.assertIn("Complexity/Classes/A.lean: 3 (baseline 5)", err) + self.assertIn("Complexity/Gone.lean: 0 (baseline 1)", err) + + def test_removed_statement_cannot_come_back(self) -> None: + # Review 5636914097: removing a tidy statement must not leave reusable allowance. + module = "Complexity.Classes.A" + full = self.modules[module] + self.modules[module] = [e for e in full if not (e[2] and e[2]["n"] == "A.stated")] + code, _, err = self.run_main({"Complexity/Classes/A.lean": 3}) + self.assertEqual(code, 1) + self.assertIn("Complexity/Classes/A.lean: 2 (baseline 3)", err) + self.assertEqual(self.run_main(None, "--update")[0], 0) + self.assertEqual(json.loads(self.baseline.read_text()), {"Complexity/Classes/A.lean": 2}) + self.assertEqual(self.run_main(None)[0], 0) + self.modules[module] = full + code, _, err = self.run_main(None) + self.assertEqual(code, 1) + self.assertIn("Complexity/Classes/A.lean: 3 tidy statement(s), baseline 2", err) + + def test_update_lowers_the_baseline(self) -> None: + code, _, _ = self.run_main({"Complexity/Classes/A.lean": 5, "Complexity/Gone.lean": 1}, + "--update") + self.assertEqual(code, 0) + self.assertEqual(json.loads(self.baseline.read_text()), {"Complexity/Classes/A.lean": 3}) + + def test_update_does_not_raise_the_baseline_by_default(self) -> None: + code, _, err = self.run_main({"Complexity/Classes/A.lean": 2}, "--update") + self.assertEqual(code, 1) + self.assertIn("--allow-increase", err) + self.assertEqual(json.loads(self.baseline.read_text()), {"Complexity/Classes/A.lean": 2}) + code, _, _ = self.run_main(None, "--update", "--allow-increase") + self.assertEqual(code, 0) + self.assertEqual(json.loads(self.baseline.read_text()), {"Complexity/Classes/A.lean": 3}) + + def test_allow_increase_needs_update(self) -> None: + with contextlib.redirect_stderr(io.StringIO()), self.assertRaises(SystemExit): + c.main(["--no-build-check", "--allow-increase"]) + + +# A compiled module for `CompiledFixtureTests`; `ComputableTidilyFake` counts as a tidy constant. +FIXTURE = """module +public import Init +public section + +@[expose] def ComputableTidilyFake (n : Nat) : Prop := n = n + +/-- Review 5636911963: tidy only in a proof-local `have` of an exposed body. -/ +@[expose] def proofLocal (n : Nat) : {m : Nat // m = n} := by + have ht : ComputableTidilyFake n := rfl + exact ⟨n, ht⟩ + +@[expose] def proofTerm (n : Nat) : {m : Nat // m = n} := + ⟨n, (show ComputableTidilyFake n from rfl)⟩ + +theorem proved (n : Nat) : n = n := by + have ht : ComputableTidilyFake n := rfl + exact ht + +def opaqueBody (n : Nat) : Prop := ComputableTidilyFake n + +private theorem privateStated (n : Nat) : ComputableTidilyFake n := rfl + +theorem stated (n : Nat) : ComputableTidilyFake n := rfl + +@[expose] def Alias (n : Nat) : Prop := ComputableTidilyFake n + +@[expose] def Pred : Nat → Prop := fun n => ∃ _ : ComputableTidilyFake n, n = 0 + +def inType (n : Nat) : {m : Nat // ComputableTidilyFake m} := ⟨n, rfl⟩ + +structure Cert (n : Nat) : Prop where + cert : ComputableTidilyFake n + +end +""" + + +@unittest.skipUnless(shutil.which("lake") and (c.ROOT / ".lake/packages").is_dir(), + "needs Lean and the repository's packages (CI runs this after the build)") +class CompiledFixtureTests(unittest.TestCase): + """The whole count on a compiled module: what `scripts/QualityReport.lean` records as a + statement, and what it leaves to proofs.""" + + @classmethod + def setUpClass(cls) -> None: + tmp = tempfile.TemporaryDirectory() + cls.addClassCleanup(tmp.cleanup) + root = pathlib.Path(tmp.name) + build = root / "build" + build.mkdir() + (root / "TidyFixture.lean").write_text(FIXTURE) + subprocess.run(["lake", "env", "lean", f"--root={root}", "-o", + str(build / "TidyFixture.olean"), "-i", str(build / "TidyFixture.ilean"), + str(root / "TidyFixture.lean")], cwd=c.ROOT, check=True, + capture_output=True) + ilean = json.loads((build / "TidyFixture.ilean").read_text()) + constants, _ = q.load_constants(build, ["TidyFixture"]) + cls.constants = constants + lib = FakeLibrary({}) + lib.ileans, lib.modules, lib.constants = {"TidyFixture": ilean}, ["TidyFixture"], constants + cls.counted = {name for rows in c.tidy_statements(lib, set()).values() + for name, _, _ in rows} + + def test_proofs_inside_exposed_bodies_do_not_count(self) -> None: + for name in ("proofLocal", "proofTerm"): + self.assertEqual(self.constants[name]["tidy"], [], name) + self.assertEqual(self.constants[name]["tb"], [], name) + self.assertNotIn(name, self.counted) + + def test_statements_count(self) -> None: + self.assertEqual(self.constants["Alias"]["tb"], ["ComputableTidilyFake"]) + self.assertEqual(self.counted, {"stated", "Alias", "Pred", "inType", "Cert.cert"}) + + +class CommittedFilesTests(unittest.TestCase): + def test_allowlist_paths_exist(self) -> None: + for path in c.load_allowlist(c.ALLOWLIST): + self.assertTrue((c.ROOT / path).is_file(), path) + + def test_baseline_is_well_formed_and_outside_the_allowlist(self) -> None: + baseline = c.load_baseline(c.BASELINE) + self.assertEqual(c.BASELINE.read_text(), c.baseline_text(baseline)) + self.assertFalse(set(baseline) & c.load_allowlist(c.ALLOWLIST)) + + +if __name__ == "__main__": + unittest.main() diff --git a/scripts/tidy_surface_baseline.json b/scripts/tidy_surface_baseline.json new file mode 100644 index 000000000..92b904a0a --- /dev/null +++ b/scripts/tidy_surface_baseline.json @@ -0,0 +1,428 @@ +{ + "Complexity/Computability/Circuit/Boolean/BalancedCode.lean": 1, + "Complexity/Computability/Circuit/Boolean/CarryLookahead/PolyTime.lean": 8, + "Complexity/Computability/Circuit/Boolean/CarrySave/PolyTime.lean": 2, + "Complexity/Computability/Circuit/Boolean/CodeComposition.lean": 7, + "Complexity/Computability/Circuit/Boolean/CodeSubstitution.lean": 2, + "Complexity/Computability/Circuit/Boolean/CodeTemplate.lean": 1, + "Complexity/Computability/Circuit/Boolean/DepthTime/PolyTime.lean": 2, + "Complexity/Computability/Circuit/Boolean/Encoding/Certificate.lean": 3, + "Complexity/Computability/Circuit/Boolean/EvaluationTime.lean": 3, + "Complexity/Computability/Circuit/Boolean/Layered/Compile/PolyTime.lean": 8, + "Complexity/Computability/Circuit/Boolean/Layered/Padding/PolyTime.lean": 2, + "Complexity/Computability/Circuit/Boolean/Layered/PolyTime.lean": 8, + "Complexity/Computability/Circuit/Boolean/PolynomialTime.lean": 1, + "Complexity/Computability/Circuit/Boolean/Tableau/Space.lean": 3, + "Complexity/Computability/Circuit/Rational/Runtime.lean": 10, + "Complexity/Computability/Circuit/Rational/Runtime/Determinant.lean": 9, + "Complexity/Computability/Circuit/Rational/Runtime/Encode.lean": 4, + "Complexity/Computability/Circuit/Rational/Runtime/Lift.lean": 16, + "Complexity/Computability/Circuit/Rational/Runtime/Parameters.lean": 13, + "Complexity/Computability/Circuit/Rational/Runtime/Point.lean": 11, + "Complexity/Computability/Complexity/AffineDisperser/PolyTime.lean": 28, + "Complexity/Computability/Complexity/Classes/AWPP.lean": 1, + "Complexity/Computability/Complexity/Classes/AWPP/Amplification.lean": 1, + "Complexity/Computability/Complexity/Classes/AWPP/OracleWeights.lean": 1, + "Complexity/Computability/Complexity/Classes/Alternation/Game.lean": 2, + "Complexity/Computability/Complexity/Classes/Alternation/GuessVerify.lean": 1, + "Complexity/Computability/Complexity/Classes/Alternation/Savitch.lean": 4, + "Complexity/Computability/Complexity/Classes/Alternation/TQBF.lean": 4, + "Complexity/Computability/Complexity/Classes/ArthurMerlin.lean": 2, + "Complexity/Computability/Complexity/Classes/ArthurMerlin/Amplification.lean": 4, + "Complexity/Computability/Complexity/Classes/ArthurMerlin/GraphNonIsomorphism.lean": 1, + "Complexity/Computability/Complexity/Classes/ArthurMerlin/PH.lean": 2, + "Complexity/Computability/Complexity/Classes/ArthurMerlin/SetLowerBound.lean": 2, + "Complexity/Computability/Complexity/Classes/BPP.lean": 1, + "Complexity/Computability/Complexity/Classes/BPP/Amplification.lean": 1, + "Complexity/Computability/Complexity/Classes/BPP/Derandomization/Generator.lean": 6, + "Complexity/Computability/Complexity/Classes/Constructible.lean": 5, + "Complexity/Computability/Complexity/Classes/EXP.lean": 1, + "Complexity/Computability/Complexity/Classes/FewP.lean": 1, + "Complexity/Computability/Complexity/Classes/Hierarchy.lean": 2, + "Complexity/Computability/Complexity/Classes/Hierarchy/ShortDesc.lean": 1, + "Complexity/Computability/Complexity/Classes/Hierarchy/Space.lean": 1, + "Complexity/Computability/Complexity/Classes/Hierarchy/Time.lean": 1, + "Complexity/Computability/Complexity/Classes/IP/GraphNonIsomorphism.lean": 3, + "Complexity/Computability/Complexity/Classes/IP/PSPACE.lean": 1, + "Complexity/Computability/Complexity/Classes/IP/Simulation.lean": 2, + "Complexity/Computability/Complexity/Classes/IP/TQBF/Words.lean": 12, + "Complexity/Computability/Complexity/Classes/Ladner/PolyTime.lean": 9, + "Complexity/Computability/Complexity/Classes/MIP/NEXP.lean": 9, + "Complexity/Computability/Complexity/Classes/NP.lean": 1, + "Complexity/Computability/Complexity/Classes/NP/GuessVerify.lean": 1, + "Complexity/Computability/Complexity/Classes/NP/Nondeterministic.lean": 1, + "Complexity/Computability/Complexity/Classes/NP/SelfReduction.lean": 2, + "Complexity/Computability/Complexity/Classes/NP/Witness.lean": 6, + "Complexity/Computability/Complexity/Classes/Oracle.lean": 1, + "Complexity/Computability/Complexity/Classes/Oracle/Closure.lean": 3, + "Complexity/Computability/Complexity/Classes/Oracle/PP.lean": 1, + "Complexity/Computability/Complexity/Classes/Oracle/PolyTime.lean": 3, + "Complexity/Computability/Complexity/Classes/Oracle/Replay.lean": 6, + "Complexity/Computability/Complexity/Classes/Oracle/Simulation.lean": 6, + "Complexity/Computability/Complexity/Classes/Oracle/Space.lean": 4, + "Complexity/Computability/Complexity/Classes/Oracle/TQBF.lean": 2, + "Complexity/Computability/Complexity/Classes/P.lean": 1, + "Complexity/Computability/Complexity/Classes/P/Slices.lean": 2, + "Complexity/Computability/Complexity/Classes/PCP.lean": 1, + "Complexity/Computability/Complexity/Classes/PCP/NP.lean": 2, + "Complexity/Computability/Complexity/Classes/PH.lean": 2, + "Complexity/Computability/Complexity/Classes/PH/KarpLipton.lean": 1, + "Complexity/Computability/Complexity/Classes/PH/Projection.lean": 1, + "Complexity/Computability/Complexity/Classes/PH/SipserLautemann.lean": 1, + "Complexity/Computability/Complexity/Classes/PP.lean": 1, + "Complexity/Computability/Complexity/Classes/PP/Characterization.lean": 1, + "Complexity/Computability/Complexity/Classes/PP/TruthTable.lean": 3, + "Complexity/Computability/Complexity/Classes/Padding.lean": 5, + "Complexity/Computability/Complexity/Classes/ParityP.lean": 3, + "Complexity/Computability/Complexity/Classes/Promise/Basic.lean": 2, + "Complexity/Computability/Complexity/Classes/RP.lean": 2, + "Complexity/Computability/Complexity/Classes/RepeatedTrials.lean": 3, + "Complexity/Computability/Complexity/Classes/SBP.lean": 3, + "Complexity/Computability/Complexity/Classes/SBP/Amplification.lean": 2, + "Complexity/Computability/Complexity/Classes/SPP/FewP.lean": 1, + "Complexity/Computability/Complexity/Classes/SharpP.lean": 1, + "Complexity/Computability/Complexity/Classes/SharpP/Aggregation.lean": 3, + "Complexity/Computability/Complexity/Classes/SharpP/Characterization.lean": 1, + "Complexity/Computability/Complexity/Classes/SharpP/Closure.lean": 3, + "Complexity/Computability/Complexity/Classes/SharpP/Combinators.lean": 4, + "Complexity/Computability/Complexity/Classes/SharpP/Completeness.lean": 1, + "Complexity/Computability/Complexity/Classes/SharpP/GapMachine.lean": 2, + "Complexity/Computability/Complexity/Classes/SharpP/Oracle.lean": 1, + "Complexity/Computability/Complexity/Classes/SharpP/PolyTime.lean": 4, + "Complexity/Computability/Complexity/Classes/SharpP/Power.lean": 2, + "Complexity/Computability/Complexity/Classes/SharpP/Products.lean": 3, + "Complexity/Computability/Complexity/Classes/SharpP/Space.lean": 3, + "Complexity/Computability/Complexity/Classes/SharpP/WeightedReplay.lean": 1, + "Complexity/Computability/Complexity/Classes/Space/Closure.lean": 4, + "Complexity/Computability/Complexity/Classes/Space/GeneralizedGeography/Membership.lean": 2, + "Complexity/Computability/Complexity/Classes/Space/GeneralizedGeography/Reduction.lean": 9, + "Complexity/Computability/Complexity/Classes/Space/TQBF/Membership.lean": 2, + "Complexity/Computability/Complexity/Classes/Space/TQBF/PolyTime.lean": 27, + "Complexity/Computability/Complexity/Classes/Space/TQBF/Prenex.lean": 2, + "Complexity/Computability/Complexity/Classes/TFNP.lean": 8, + "Complexity/Computability/Complexity/Classes/TFNP/Subclasses.lean": 28, + "Complexity/Computability/Complexity/Classes/TFNP/Subclasses/Completeness.lean": 5, + "Complexity/Computability/Complexity/Classes/Time.lean": 3, + "Complexity/Computability/Complexity/Classes/Toda/Counting.lean": 5, + "Complexity/Computability/Complexity/Classes/Toda/Hierarchy.lean": 3, + "Complexity/Computability/Complexity/Classes/Toda/Isolation.lean": 1, + "Complexity/Computability/Complexity/Classes/UP.lean": 1, + "Complexity/Computability/Complexity/Classes/ValiantVazirani/Reduction.lean": 4, + "Complexity/Computability/Complexity/Classes/WPP.lean": 5, + "Complexity/Computability/Complexity/Classes/WPP/Bounded.lean": 4, + "Complexity/Computability/Complexity/Classes/WPP/TruthTable.lean": 2, + "Complexity/Computability/Complexity/Classes/ZPP.lean": 1, + "Complexity/Computability/Complexity/CookLevin/Clauses.lean": 9, + "Complexity/Computability/Complexity/CookLevin/Encoding.lean": 9, + "Complexity/Computability/Complexity/CookLevin/Parameters.lean": 1, + "Complexity/Computability/Complexity/CookLevin/PolyTime.lean": 2, + "Complexity/Computability/Complexity/Fagin/StrictVerifier.lean": 1, + "Complexity/Computability/Complexity/Fagin/Verifier.lean": 7, + "Complexity/Computability/Complexity/FineGrained.lean": 5, + "Complexity/Computability/Complexity/FineGrained/Assignment.lean": 1, + "Complexity/Computability/Complexity/FineGrained/BruteForce.lean": 2, + "Complexity/Computability/Complexity/FineGrained/OrthogonalVectors.lean": 5, + "Complexity/Computability/Complexity/FineGrained/Reduction.lean": 3, + "Complexity/Computability/Complexity/FineGrained/Sparsification.lean": 1, + "Complexity/Computability/Complexity/HardnessEncoding/PolyTime.lean": 7, + "Complexity/Computability/Complexity/Parameterized.lean": 13, + "Complexity/Computability/Complexity/Parameterized/Kernelization.lean": 1, + "Complexity/Computability/Complexity/Parameterized/VertexCover.lean": 6, + "Complexity/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean": 14, + "Complexity/Computability/Complexity/Problems/CircuitSAT.lean": 1, + "Complexity/Computability/Complexity/Problems/CircuitValue.lean": 1, + "Complexity/Computability/Complexity/Problems/CircuitValue/Compilation.lean": 1, + "Complexity/Computability/Complexity/Problems/CircuitValue/Completeness.lean": 4, + "Complexity/Computability/Complexity/Problems/CircuitValue/Writer.lean": 1, + "Complexity/Computability/Complexity/Problems/Clique.lean": 2, + "Complexity/Computability/Complexity/Problems/Coloring.lean": 4, + "Complexity/Computability/Complexity/Problems/CountingSAT.lean": 1, + "Complexity/Computability/Complexity/Problems/ExactThreeSAT.lean": 3, + "Complexity/Computability/Complexity/Problems/Graph.lean": 4, + "Complexity/Computability/Complexity/Problems/GraphIsomorphism.lean": 4, + "Complexity/Computability/Complexity/Problems/Hamiltonian.lean": 10, + "Complexity/Computability/Complexity/Problems/Hamiltonian/Diamond.lean": 5, + "Complexity/Computability/Complexity/Problems/Hamiltonian/Directed.lean": 3, + "Complexity/Computability/Complexity/Problems/Hamiltonian/Sparse.lean": 7, + "Complexity/Computability/Complexity/Problems/Hamiltonian/Undirected.lean": 2, + "Complexity/Computability/Complexity/Problems/IndependentSet.lean": 5, + "Complexity/Computability/Complexity/Problems/IndependentSet/Sparse.lean": 1, + "Complexity/Computability/Complexity/Problems/IntegerProgramming.lean": 2, + "Complexity/Computability/Complexity/Problems/Knapsack.lean": 2, + "Complexity/Computability/Complexity/Problems/Partition.lean": 2, + "Complexity/Computability/Complexity/Problems/SAT/PolyTime.lean": 8, + "Complexity/Computability/Complexity/Problems/SharpSAT.lean": 4, + "Complexity/Computability/Complexity/Problems/SubsetSum.lean": 9, + "Complexity/Computability/Complexity/Problems/SubsetSum/Mask.lean": 1, + "Complexity/Computability/Complexity/Problems/TQBF/Closed.lean": 1, + "Complexity/Computability/Complexity/Problems/TSP.lean": 3, + "Complexity/Computability/Complexity/Problems/ThreeSAT.lean": 3, + "Complexity/Computability/Complexity/Problems/VertexCover.lean": 2, + "Complexity/Computability/Complexity/Reduction.lean": 1, + "Complexity/Computability/Complexity/Reduction/TruthTable.lean": 2, + "Complexity/Computability/GenericRAM/Native.lean": 6, + "Complexity/Computability/GenericRAM/Native/Combinators.lean": 8, + "Complexity/Computability/GenericRAM/Native/Nat.lean": 6, + "Complexity/Computability/GenericRAM/Simulation/Run.lean": 8, + "Complexity/Computability/GenericRAM/Simulation/Turing.lean": 1, + "Complexity/Computability/GenericRAM/SparseMemory/Turing.lean": 8, + "Complexity/Computability/MCSP/NP.lean": 2, + "Complexity/Computability/Machines/ReadMachine/Tidy.lean": 10, + "Complexity/Computability/Machines/Turing/MultiTape/Combinators/Encoding.lean": 19, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Arith.lean": 2, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO.lean": 38, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Constructible.lean": 3, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Option.lean": 1, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Pi.lean": 5, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Plain.lean": 5, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Sum.lean": 8, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Binary.lean": 4, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/BinaryCompare.lean": 2, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Degree.lean": 24, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Fold.lean": 2, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace.lean": 19, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace/Bit.lean": 1, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace/Plain.lean": 4, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpaceLib.lean": 45, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LinearSpaceArith.lean": 1, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Lists.lean": 14, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace.lean": 2, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Radix.lean": 3, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Routines.lean": 8, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/CounterProgram.lean": 11, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/InductiveCounting/Callbacks.lean": 14, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/InductiveCounting/Routines.lean": 34, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine.lean": 5, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine/Compiler.lean": 1, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine/Routines.lean": 1, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/QueryMachine.lean": 9, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean": 4, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolySpace.lean": 12, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolySpace/Fold.lean": 2, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolySpace/Plain.lean": 4, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime.lean": 19, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Basic.lean": 27, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/BitString.lean": 34, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Configuration.lean": 18, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/DPi.lean": 3, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Finite.lean": 1, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Fold.lean": 7, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Int.lean": 13, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Int/Binary.lean": 24, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Int/BinaryDiv.lean": 2, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Iteration.lean": 7, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/List.lean": 67, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Matrix/Binary.lean": 1, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Membership.lean": 2, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat.lean": 17, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/Binary.lean": 17, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/BinaryDiv.lean": 5, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/Div.lean": 4, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/Factorial.lean": 1, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/Fin.lean": 1, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/Gcd.lean": 2, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/Log.lean": 5, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/Prime.lean": 1, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/Search.lean": 1, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Option.lean": 5, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Pi.lean": 7, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Plain.lean": 7, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap.lean": 5, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/Family.lean": 3, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/Tower.lean": 4, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/Walk.lean": 3, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Sum.lean": 2, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Tape.lean": 14, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Window.lean": 2, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Primitives.lean": 9, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Quantitative.lean": 18, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space.lean": 7, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space/Decode.lean": 8, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space/Reachability.lean": 3, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space/Savitch.lean": 2, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Streaming.lean": 14, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Translate.lean": 2, + "Complexity/Computability/Machines/Turing/MultiTape/Counting/Checker.lean": 6, + "Complexity/Computability/Machines/Turing/MultiTape/Counting/Verifier.lean": 1, + "Complexity/Computability/Machines/Turing/MultiTape/Encodings/Basic.lean": 8, + "Complexity/Computability/Machines/Turing/MultiTape/Encodings/Decoder.lean": 3, + "Complexity/Computability/Machines/Turing/MultiTape/Encodings/MultiPass.lean": 1, + "Complexity/Computability/Machines/Turing/MultiTape/Encodings/Nat.lean": 3, + "Complexity/Computability/Machines/Turing/MultiTape/Encodings/NatPower.lean": 1, + "Complexity/Computability/Machines/Turing/MultiTape/Encodings/NatStream.lean": 1, + "Complexity/Computability/Machines/Turing/MultiTape/Encodings/StepMachine.lean": 10, + "Complexity/Computability/Machines/Turing/MultiTape/Encodings/StreamFold.lean": 4, + "Complexity/Computability/Machines/Turing/MultiTape/Halting/Computable.lean": 5, + "Complexity/Computability/Machines/Turing/MultiTape/Halting/Rice.lean": 3, + "Complexity/Computability/Machines/Turing/MultiTape/Halting/SMN.lean": 20, + "Complexity/Computability/Machines/Turing/MultiTape/Plumbing/PrepareClock.lean": 1, + "Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/QueryTake.lean": 2, + "Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/ReplayInput.lean": 2, + "Complexity/Computability/Machines/Turing/MultiTape/SingleTape.lean": 2, + "Complexity/Computability/Machines/Turing/MultiTape/Universal/Complexity.lean": 7, + "Complexity/Computability/Machines/Turing/MultiTape/Universal/Compose.lean": 7, + "Complexity/Computability/Machines/Turing/MultiTape/Universal/Decode.lean": 1, + "Complexity/Computability/Machines/Turing/MultiTape/Universal/InPlace.lean": 9, + "Complexity/Computability/Machines/Turing/MultiTape/Universal/Machine.lean": 2, + "Complexity/Computability/Machines/Turing/MultiTape/Universal/PolyTime.lean": 5, + "Complexity/Computability/Machines/Turing/MultiTape/Universal/SpaceBudget.lean": 2, + "Complexity/Computability/Machines/Turing/TM2/PolySpace.lean": 2, + "Complexity/Computability/Machines/Turing/TM2/PolyTime.lean": 3, + "Complexity/Computability/Machines/Turing/TM2/Simulation.lean": 6, + "Complexity/Computability/PCP/Approximation/MaxExactThreeSAT.lean": 1, + "Complexity/Computability/PCP/Approximation/MaxThreeSAT.lean": 1, + "Complexity/Computability/PCP/Encoded/AddTrivial.lean": 2, + "Complexity/Computability/PCP/Encoded/Amplification.lean": 1, + "Complexity/Computability/PCP/Encoded/Amplification/Arithmetic.lean": 1, + "Complexity/Computability/PCP/Encoded/Amplification/Enumeration.lean": 1, + "Complexity/Computability/PCP/Encoded/Amplification/Iteration.lean": 1, + "Complexity/Computability/PCP/Encoded/AssignmentTester.lean": 2, + "Complexity/Computability/PCP/Encoded/Basic.lean": 10, + "Complexity/Computability/PCP/Encoded/Cloud.lean": 3, + "Complexity/Computability/PCP/Encoded/CloudRotation.lean": 1, + "Complexity/Computability/PCP/Encoded/Composition.lean": 5, + "Complexity/Computability/PCP/Encoded/Composition/Enumeration.lean": 1, + "Complexity/Computability/PCP/Encoded/Constraints.lean": 4, + "Complexity/Computability/PCP/Encoded/DegreeReduction.lean": 5, + "Complexity/Computability/PCP/Encoded/GapTheorem.lean": 1, + "Complexity/Computability/PCP/Encoded/GenericComposition.lean": 5, + "Complexity/Computability/PCP/Encoded/GenericComposition/Enumeration.lean": 1, + "Complexity/Computability/PCP/Encoded/Iteration.lean": 1, + "Complexity/Computability/PCP/Encoded/Power.lean": 1, + "Complexity/Computability/PCP/Encoded/Preprocess.lean": 2, + "Complexity/Computability/PCP/Encoded/Preprocess/Programs.lean": 3, + "Complexity/Computability/PCP/Encoded/SelectedAssignmentTester.lean": 2, + "Complexity/Computability/PCP/Encoded/SelectedComposition.lean": 1, + "Complexity/Computability/PCP/Encoded/SelectedComposition/Enumeration.lean": 1, + "Complexity/Computability/PCP/Encoded/ThreeSAT.lean": 4, + "Complexity/Computability/PCP/Encoded/Verifier.lean": 4, + "Complexity/Computability/PCP/Encoded/Verifier/Reduction.lean": 2, + "Complexity/Computability/PCP/Encoded/Verifier/Repetition.lean": 1, + "Complexity/Computability/PCP/Power/Complexity.lean": 1, + "Complexity/Computability/Probabilistic/Adaptive.lean": 5, + "Complexity/Computability/Probabilistic/CenteredBinomial.lean": 1, + "Complexity/Computability/Probabilistic/CoinTape.lean": 5, + "Complexity/Computability/Probabilistic/Finite.lean": 1, + "Complexity/Computability/Probabilistic/LinearHash.lean": 2, + "Complexity/Computability/Probabilistic/Memoize.lean": 1, + "Complexity/Computability/Probabilistic/Oracle.lean": 1, + "Complexity/Computability/Probabilistic/Oracle/Composition.lean": 12, + "Complexity/Computability/Probabilistic/Oracle/Iteration.lean": 3, + "Complexity/Computability/Probabilistic/Oracle/Memoize.lean": 1, + "Complexity/Computability/Probabilistic/Oracle/Normalization.lean": 4, + "Complexity/Computability/Probabilistic/Oracle/Parameter.lean": 2, + "Complexity/Computability/Probabilistic/Oracle/Substitution.lean": 2, + "Complexity/Computability/Probabilistic/Oracle/Tidy.lean": 18, + "Complexity/Computability/Probabilistic/OracleSimulation.lean": 1, + "Complexity/Computability/Probabilistic/PPT.lean": 1, + "Complexity/Computability/Probabilistic/PPT/Capture.lean": 5, + "Complexity/Computability/Probabilistic/PPT/Composition.lean": 2, + "Complexity/Computability/Probabilistic/Parameter.lean": 2, + "Complexity/Computability/Probabilistic/Presample.lean": 2, + "Complexity/Computability/Probabilistic/Realization/OpenOracleSimulation.lean": 1, + "Complexity/Computability/Probabilistic/Realization/OracleSimulation.lean": 1, + "Complexity/Computability/Probabilistic/Repeat.lean": 4, + "Complexity/Computability/Probabilistic/Sampling.lean": 1, + "Complexity/Computability/Probabilistic/Selection.lean": 3, + "Complexity/Computability/Probabilistic/Traverse.lean": 1, + "Complexity/Computability/Probabilistic/UniformNat.lean": 5, + "Complexity/Computability/TreeEval/Reader/Cert/Machine.lean": 1, + "Complexity/Computability/TreeEval/Reader/Cert/Offset.lean": 5, + "Complexity/Computability/TreeEval/Reader/Cert/Regs.lean": 6, + "Complexity/Computability/TreeEval/Reader/Cert/Residue.lean": 5, + "Complexity/Computability/TreeEval/Reader/Cert/Step.lean": 8, + "Complexity/Computability/TreeEval/Reader/Cert/Weight.lean": 1, + "Complexity/Computability/TreeEval/Space.lean": 2, + "Complexity/Computability/USTCON/Reader/Cert.lean": 3, + "Complexity/Computability/USTCON/Space.lean": 1, + "Complexity/Computability/WordRAM/Native.lean": 1, + "Complexity/Crypto/Computational/Basic.lean": 1, + "Complexity/Crypto/Computational/Commitment.lean": 13, + "Complexity/Crypto/Computational/Encryption/PolyTime.lean": 2, + "Complexity/Crypto/Computational/GGM/Evaluation.lean": 3, + "Complexity/Crypto/Computational/GGM/Expansion.lean": 2, + "Complexity/Crypto/Computational/GGM/Hybrid.lean": 2, + "Complexity/Crypto/Computational/GGM/Reduction.lean": 3, + "Complexity/Crypto/Computational/GGM/Security.lean": 1, + "Complexity/Crypto/Computational/GMW/PolyTime.lean": 36, + "Complexity/Crypto/Computational/GMW/Simulator.lean": 3, + "Complexity/Crypto/Computational/GeneratorPadding.lean": 2, + "Complexity/Crypto/Computational/GeneratorReindex.lean": 4, + "Complexity/Crypto/Computational/GeneratorXor.lean": 3, + "Complexity/Crypto/Computational/GoldreichLevin/HardCore.lean": 2, + "Complexity/Crypto/Computational/GoldreichLevin/WordDecoder.lean": 7, + "Complexity/Crypto/Computational/GoldreichLevin/WordReduction.lean": 3, + "Complexity/Crypto/Computational/HardCore.lean": 4, + "Complexity/Crypto/Computational/Homomorphic/BitEncryption/PolyTime.lean": 2, + "Complexity/Crypto/Computational/Homomorphic/Circuit/PolyTime.lean": 1, + "Complexity/Crypto/Computational/Homomorphic/Efficiency.lean": 3, + "Complexity/Crypto/Computational/Homomorphic/Evaluation/PolyTime.lean": 1, + "Complexity/Crypto/Computational/Homomorphic/FixedKey/Bootstrapping.lean": 1, + "Complexity/Crypto/Computational/Homomorphic/FixedKey/PolyTime.lean": 9, + "Complexity/Crypto/Computational/Homomorphic/GSW/DepthParameters.lean": 6, + "Complexity/Crypto/Computational/Homomorphic/GSW/Parameters.lean": 6, + "Complexity/Crypto/Computational/Homomorphic/GSW/Sampling/Serialized.lean": 2, + "Complexity/Crypto/Computational/Homomorphic/GSW/Security.lean": 2, + "Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Evaluation/PolyTime.lean": 4, + "Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/PolyTime.lean": 7, + "Complexity/Crypto/Computational/Homomorphic/KeyChain/Hybrid/PolyTime.lean": 5, + "Complexity/Crypto/Computational/Homomorphic/KeyChain/PolyTime.lean": 3, + "Complexity/Crypto/Computational/Homomorphic/KeyChain/Reduction/PolyTime.lean": 4, + "Complexity/Crypto/Computational/Homomorphic/KeyChain/Security.lean": 1, + "Complexity/Crypto/Computational/Homomorphic/Layered/PolyTime.lean": 4, + "Complexity/Crypto/Computational/Homomorphic/Leveled/Bootstrapping.lean": 2, + "Complexity/Crypto/Computational/Homomorphic/Leveled/Compactness.lean": 2, + "Complexity/Crypto/Computational/Homomorphic/Leveled/PolyTime.lean": 10, + "Complexity/Crypto/Computational/Homomorphic/Leveled/Reduction/PolyTime.lean": 1, + "Complexity/Crypto/Computational/Homomorphic/Leveled/Security.lean": 3, + "Complexity/Crypto/Computational/Hybrid/SavedPrediction.lean": 6, + "Complexity/Crypto/Computational/Hybrid/Sequence.lean": 4, + "Complexity/Crypto/Computational/OneWay.lean": 4, + "Complexity/Crypto/Computational/OneWay/BPP.lean": 1, + "Complexity/Crypto/Computational/OneWay/MCSP.lean": 6, + "Complexity/Crypto/Computational/OneWay/NP.lean": 6, + "Complexity/Crypto/Computational/OneWay/Normalize.lean": 3, + "Complexity/Crypto/Computational/OneWayToSignature.lean": 6, + "Complexity/Crypto/Computational/PRGToOneWay.lean": 1, + "Complexity/Crypto/Computational/Prediction.lean": 1, + "Complexity/Crypto/Computational/Pseudoentropy/Boosting/Clipped.lean": 1, + "Complexity/Crypto/Computational/Pseudoentropy/Boosting/Decision.lean": 2, + "Complexity/Crypto/Computational/Pseudoentropy/Boosting/Learner.lean": 3, + "Complexity/Crypto/Computational/Pseudoentropy/Boosting/Program.lean": 16, + "Complexity/Crypto/Computational/Pseudoentropy/Boosting/Sampling.lean": 2, + "Complexity/Crypto/Computational/Pseudoentropy/Boosting/Selection.lean": 4, + "Complexity/Crypto/Computational/Pseudoentropy/Boosting/Training.lean": 3, + "Complexity/Crypto/Computational/Pseudoentropy/DenseMask.lean": 2, + "Complexity/Crypto/Computational/Pseudoentropy/EntropyGrid.lean": 6, + "Complexity/Crypto/Computational/Pseudoentropy/ExtractionSchedule.lean": 2, + "Complexity/Crypto/Computational/Pseudoentropy/Generator.lean": 1, + "Complexity/Crypto/Computational/Pseudoentropy/HashPair.lean": 4, + "Complexity/Crypto/Computational/Pseudoentropy/LabelExtraction.lean": 2, + "Complexity/Crypto/Computational/Pseudoentropy/Masking.lean": 3, + "Complexity/Crypto/Computational/Pseudoentropy/MatrixExtraction.lean": 1, + "Complexity/Crypto/Computational/Pseudoentropy/RepeatedExtraction.lean": 2, + "Complexity/Crypto/Computational/Pseudoentropy/Seed.lean": 3, + "Complexity/Crypto/Computational/Pseudoentropy/Selection.lean": 2, + "Complexity/Crypto/Computational/Pseudoentropy/SequenceLearner.lean": 6, + "Complexity/Crypto/Computational/Pseudoentropy/ThreeSource.lean": 5, + "Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Amplification.lean": 1, + "Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Candidates.lean": 5, + "Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Combined.lean": 1, + "Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Padding.lean": 5, + "Complexity/Crypto/Computational/Pseudoentropy/ThreeSource/Seeded.lean": 2, + "Complexity/Crypto/Computational/Pseudoentropy/WordExtraction.lean": 4, + "Complexity/Crypto/Computational/Pseudoentropy/WordReduction.lean": 3, + "Complexity/Crypto/Computational/Pseudoentropy/WordSeedExtraction.lean": 2, + "Complexity/Crypto/Computational/PseudorandomFunction.lean": 1, + "Complexity/Crypto/Computational/PseudorandomFunction/RandomOracle.lean": 1, + "Complexity/Crypto/Computational/PseudorandomFunction/TruthTable.lean": 1, + "Complexity/Crypto/Computational/PseudorandomGenerator.lean": 6, + "Complexity/Crypto/Computational/Signature.lean": 5, + "Complexity/Crypto/Computational/Stretch.lean": 8, + "Complexity/Crypto/Computational/Stretch/Quantitative.lean": 9, + "Complexity/Crypto/Computational/UniformChoice.lean": 2, + "Complexity/Logics/Propositional/CNF/PolyTime.lean": 13, + "Complexity/Logics/Propositional/CNF/ThreeCNF/PolyTime.lean": 3, + "Complexity/Logics/Propositional/ClauseSet/Sparsification/PolyTime.lean": 4, + "Complexity/Tactic/PolyTime.lean": 3 +} diff --git a/scripts/tidy_sweep.py b/scripts/tidy_sweep.py index ca9284f45..9e464c0ac 100644 --- a/scripts/tidy_sweep.py +++ b/scripts/tidy_sweep.py @@ -9,8 +9,8 @@ Plain computability is the API and tidy computability is how the machine layer proves it: outside the raw machine constructions of the allowlist (`scripts/tidy_allowlist.txt`, from #608), no public statement should mention a tidy notion. Every public declaration outside the allowlist -whose statement (its type, or the exposed body of a definition) mentions a tidy predicate falls -in one case of the S2 design +whose statement (its type, or the exposed body of a definition outside proofs) mentions a tidy +predicate falls in one case of the S2 design (https://github.com/cslib-community/complexitylib/issues/456#issuecomment-6376748411): 1. a theorem with a committed plain twin: proofs that become plain use the twin, and the