tools: preserve reproducible Zeta5 certificate generation

README.md

@@ -40,6 +40,9 @@ make setup    # pull Mathlib oleans, build the whole pool (~1.5h), install Pytho
 To work on a single project you don't need the whole pool built — see the
 [fast per-project build](CONTRIBUTING.md#dev-setup) in `CONTRIBUTING.md`.
 
+To regenerate the preserved Zeta5 numerical certificates, see the
+[certificate reproduction guide](scripts/zeta5-certificates/README.md).
+
 ### Challenge mode
 
 [`Challenge/`](Challenge/) is the other half of the pool: open *statements* rather than finished proofs. A challenge is a theorem written in Mathlib vocabulary and left as `sorry`, registered in [`Challenge/challenges.yml`](Challenge/challenges.yml) alongside the English statement it is supposed to say. It is the only place `sorry` is allowed, and only for the declarations the registry lists — everything else in the file must be closed, and every other gate still applies.

python/tests/test_zeta5_certificates.py

@@ -0,0 +1,140 @@
+"""Check exact and constrained rendering of the Zeta5 certificate archive."""
+
+import hashlib
+import importlib.util
+import json
+import shutil
+from pathlib import Path, PureWindowsPath
+
+import pytest
+
+SCRIPT = Path(__file__).parents[2] / "scripts/zeta5-certificates/regenerate.py"
+SPECIFICATION = importlib.util.spec_from_file_location("zeta5_regenerate", SCRIPT)
+assert SPECIFICATION is not None and SPECIFICATION.loader is not None
+GENERATOR = importlib.util.module_from_spec(SPECIFICATION)
+SPECIFICATION.loader.exec_module(GENERATOR)
+
+
+def test_exact_large_rational_and_name() -> None:
+    """Preserve huge rational numerators, signs, names, and Unicode byte for byte."""
+    template = (
+        "lemma U_{{integer}} : (-( {{integer}} / {{integer}} : ℝ)) ≤ x := by\n"
+        "  exact h\n"
+    )
+    numerator = "123456789012345678901234567890123456789"
+    result = GENERATOR.render(template, ["12", numerator, "200000000000000000000"])
+    assert (
+        result
+        == f"lemma U_12 : (-( {numerator} / 200000000000000000000 : ℝ)) ≤ x := by\n"
+        "  exact h\n"
+    )
+
+
+@pytest.mark.parametrize("parameters", [[], ["1", "2"], ["1e100"], ["0; run"]])
+def test_reject_invalid_parameters(parameters: list[str]) -> None:
+    """Reject malformed or incomplete certificate data before rendering."""
+    with pytest.raises(ValueError):
+        GENERATOR.render("{{integer}}", parameters)
+
+
+@pytest.mark.parametrize("path", ["../bad.lean", "/bad.lean", "LeanPool/Other/A.lean"])
+def test_reject_output_outside_project(path: str) -> None:
+    """Keep accidental manifest edits from writing unrelated files."""
+    with pytest.raises(ValueError):
+        GENERATOR.certificate_path(path)
+
+
+def test_complete_archive(tmp_path: Path) -> None:
+    """Regenerate every output and independently check its pinned hash."""
+    archive = SCRIPT.parent / "archive"
+    GENERATOR.verify_archive(archive)
+    assert GENERATOR.regenerate(archive, tmp_path / "generated", False) == 118
+    assert GENERATOR.regenerate(archive, tmp_path / "generated", True) == 118
+    manifest = json.loads((archive / "manifest.json").read_text(encoding="utf-8"))
+    first = tmp_path / "generated" / next(iter(manifest["files"]))
+    first.write_text(
+        first.read_text(encoding="utf-8") + "-- damaged\n", encoding="utf-8"
+    )
+    with pytest.raises(ValueError, match="Certificates differ"):
+        GENERATOR.regenerate(archive, tmp_path / "generated", True)
+
+
+def test_reject_reused_or_symlinked_destination(tmp_path: Path) -> None:
+    """Protect pre-existing output trees and symlink targets from writes."""
+    outside = tmp_path / "outside"
+    outside.mkdir()
+    sentinel = outside / "sentinel"
+    sentinel.write_text("preserve me")
+    symlink = tmp_path / "link"
+    symlink.symlink_to(outside, target_is_directory=True)
+    for destination in (outside, symlink):
+        with pytest.raises(FileExistsError):
+            GENERATOR.regenerate(SCRIPT.parent / "archive", destination, False)
+    assert sentinel.read_text(encoding="utf-8") == "preserve me"
+    assert list(outside.iterdir()) == [sentinel]
+
+
+def test_failed_later_record_creates_nothing(tmp_path: Path) -> None:
+    """Create no output when a later template is absent."""
+    archive = tmp_path / "archive"
+    shutil.copytree(SCRIPT.parent / "archive", archive)
+    manifest = json.loads((archive / "manifest.json").read_text(encoding="utf-8"))
+    last = list(manifest["files"].values())[-1]
+    records = archive / "records" / last["records"]
+    records.write_text('[["999", []]]')
+    output = tmp_path / "generated"
+    with pytest.raises(FileNotFoundError):
+        GENERATOR.regenerate(archive, output, False)
+    assert not output.exists()
+    assert list(tmp_path.glob(".zeta5-certificates-*")) == []
+
+
+def test_destination_created_during_render_is_preserved(
+    tmp_path: Path, monkeypatch: pytest.MonkeyPatch
+) -> None:
+    """Do not replace a destination created after the operation starts."""
+    output = tmp_path / "generated"
+
+    def competing_creation(archive: Path) -> dict[Path, bytes]:
+        output.mkdir()
+        return {Path("LeanPool/Zeta5Irrational/A.lean"): b"test"}
+
+    monkeypatch.setattr(GENERATOR, "_render_modules", competing_creation)
+    with pytest.raises(FileExistsError):
+        GENERATOR.regenerate(SCRIPT.parent / "archive", output, False)
+    assert output.is_dir()
+    assert list(output.iterdir()) == []
+
+
+def test_nested_output_and_write_failure_cleanup(
+    tmp_path: Path, monkeypatch: pytest.MonkeyPatch
+) -> None:
+    """Support new parents and clean up output if writing fails."""
+    relative = Path("LeanPool/Zeta5Irrational/A.lean")
+    monkeypatch.setattr(GENERATOR, "_render_modules", lambda _: {relative: b"test"})
+    output = tmp_path / "new" / "parents" / "generated"
+    assert GENERATOR.regenerate(SCRIPT.parent / "archive", output, False) == 1
+    assert (output / relative).read_bytes() == b"test"
+
+    def fail_write(path: Path, content: bytes) -> None:
+        raise OSError("disk full")
+
+    monkeypatch.setattr(Path, "write_bytes", fail_write)
+    failed_output = tmp_path / "failed"
+    with pytest.raises(OSError, match="disk full"):
+        GENERATOR.regenerate(SCRIPT.parent / "archive", failed_output, False)
+    assert not failed_output.exists()
+
+
+def test_archive_manifest_uses_portable_paths(
+    tmp_path: Path, monkeypatch: pytest.MonkeyPatch
+) -> None:
+    """Look up POSIX manifest keys even when rendering uses Windows paths."""
+    content = b"certificate"
+    path = PureWindowsPath("LeanPool/Zeta5Irrational/Table/U00.lean")
+    manifest = {
+        "files": {path.as_posix(): {"sha256": hashlib.sha256(content).hexdigest()}}
+    }
+    (tmp_path / "manifest.json").write_text(json.dumps(manifest), encoding="utf-8")
+    monkeypatch.setattr(GENERATOR, "_render_modules", lambda _: {path: content})
+    GENERATOR.verify_archive(tmp_path)

scripts/zeta5-certificates/README.md

@@ -0,0 +1,64 @@
+# Reproducing the Zeta5 numerical certificates
+
+This archive reproduces all 118 generated modules in Lean Pool PR #540, including
+114 U/V endpoint tables, the 684-interval assembly, and the inner/outer growth
+tables and inner sum. The manifest pins source commit
+`b00b44fc50beb974417bfdff2898aeedd83cfdde`, upstream
+[`mo271/Zeta5`](https://github.com/mo271/Zeta5/tree/f19a1960609f7d38e7b63fd2acb05e6f60a7b741),
+and each output's SHA-256. The archive includes the import cleanup from the
+final review; every mathematical certificate body is preserved.
+
+Use Python 3.13 or later. No third-party packages, network, Lean installation,
+floating-point arithmetic, or execution of archived code is needed for rendering:
+
+```sh
+python3 scripts/zeta5-certificates/regenerate.py --verify-archive
+python3 scripts/zeta5-certificates/regenerate.py --output "$CODEX_SCRATCH_ROOT/zeta5-regenerated"
+python3 scripts/zeta5-certificates/regenerate.py --check /path/to/import-checkout
+```
+
+`--output` writes only the recorded project modules underneath its argument;
+the destination must not already exist, even as an empty directory or symlink.
+All records are validated and rendered in memory before the destination is
+created exclusively. Missing parent directories are created automatically. A
+malformed record creates no output; a write failure removes the new output tree.
+Wait for successful completion before reading or copying generated files. `--check` compares
+bytes without writing. The archive hash verification is separate so a deliberate
+template edit can be rendered before its baseline hashes are updated.
+
+## Data and shared proof templates
+
+The archive contains 14,147 blocks represented by 461 text templates. A record
+is `[template_identifier, decimal_integer_strings]`. Replace the consecutive
+`{{integer}}` markers in the named template with those strings, preserving all
+other bytes, and concatenate a file's records in order. Signs, rational division,
+Lean syntax, tactic calls, and layout live in the templates. Parameters include
+numeric suffixes in declaration names as well as mathematical integers. Integer
+strings avoid any JSON floating-point precision loss.
+
+The templates were extracted from the canonical, compiled Lean port, splitting
+before top-level `lemma`, `theorem`, and `def` declarations (including private
+ones), and replacing each ASCII decimal digit run with a marker. Templates with
+identical resulting bytes are shared. Layout variants remain separate to preserve
+byte-for-byte output. The complete round trip and all output hashes were checked.
+
+This is a generator for the **preserved certificate set**, not a search algorithm
+for stronger bounds or a claim to reconstruct the original numerical search.
+The upstream scripts document that search, but do not reproduce this port. Here
+the exact certified rational parameters are explicit inputs. Changes to a common
+proof idiom can be made once in its template rather than across its users; the
+most-used template occurs 4,500 times. Grepping `records/` for its identifier finds
+all affected modules. A change to the number of markers requires corresponding
+parameter changes and is rejected if their counts disagree.
+
+After editing, render to scratch, inspect the diff, copy the intended outputs to
+a content branch, and run the project build, style checks, linters, and trust
+audit. Every emitted theorem must still pass the Lean kernel. New interval
+partitions or new rational bounds additionally need mathematical validation;
+this tool does not certify them on its own. Keep tooling edits in a separate PR
+from Lean content, as required by the repository's separation policy.
+
+The certificate text and numeric data derive from Moritz Firsching's Apache-2.0
+formalization, with AI-assisted proof refactoring by the Lean Pool acquisition
+agent. Original copyright/author headers are reproduced in the outputs. This
+tool and archive are distributed under the repository's Apache-2.0 license.