1"""Stage 8 finalisation pipeline (run detached; log in results/revision/finalize.log).23Waits for the background jobs (drat-trim checks of the n = 23 and n = 25 fort-cover proofs,4the default-mode reproduce.sh run), then: merges the two new certificate records into the5independent checker's report, rebuilds value tables / metrics / manuscript tables, updates the6manuscript, abstract, metadata, review files, reproducibility record and plan log from the7actual results, and removes the compiled drat-trim binary. Every step is wrapped so that a8failure is logged and the remaining steps still run. Nothing here invents a number: every value9written into text is read from a result record produced in this workspace.10"""11import datetime12import json13import os14import re15import subprocess16import sys17import time1819ROOT = os.path.dirname(os.path.dirname(os.path.dirname(os.path.abspath(__file__))))20os.chdir(ROOT)21ENV = dict(os.environ, PYTHONPATH=".pydeps:code")22LOG = open("results/revision/finalize.log", "a")232425def log(*a):26 msg = "%s %s" % (datetime.datetime.now(datetime.timezone.utc).isoformat(timespec="seconds"), " ".join(str(x) for x in a))27 LOG.write(msg + "\n")28 LOG.flush()293031def run(name, cmd, logfile=None):32 full = ["python3", "code/tools/logrun.py", name] + (["--log", logfile] if logfile else []) + ["--"] + cmd33 log("RUN", name, " ".join(cmd))34 r = subprocess.run(full, env=ENV, capture_output=True, text=True)35 log("EXIT", name, r.returncode, (r.stdout + r.stderr)[-600:].replace("\n", " | "))36 return r.returncode373839def wait_for(pred, what, limit_s, poll=30):40 t0 = time.time()41 while time.time() - t0 < limit_s:42 if pred():43 log("READY", what, "after %.0f s" % (time.time() - t0))44 return True45 time.sleep(poll)46 log("TIMEOUT waiting for", what)47 return False484950def jl(path):51 return [json.loads(l) for l in open(path)] if os.path.exists(path) else []525354def fmt(n):55 return "{:,}".format(n).replace(",", "{,}")565758def sub(path, old, new, count=1, must=True):59 s = open(path).read()60 c = s.count(old)61 if c == 0:62 log("SUBST MISSING in", path, ":", old[:70])63 return False64 if count and c != count:65 log("SUBST COUNT", c, "!=", count, "in", path, ":", old[:70])66 s = s.replace(old, new)67 open(path, "w").write(s)68 log("SUBST OK in", path, ":", old[:60], "->", new[:60])69 return True707172def step(name, fn):73 try:74 log("STEP", name)75 fn()76 except Exception as e: # noqa: BLE00177 import traceback78 log("STEP FAILED", name, repr(e), traceback.format_exc()[-800:].replace("\n", " | "))798081# ------------------------------------------------------------------ 1. wait for the proof checks82def check_done(n):83 p = "results/revision/check_fortcover_n%d.log" % n84 return os.path.exists(p) and '"checker_verified"' in open(p).read()858687wait_for(lambda: check_done(23) and check_done(25), "drat-trim checks n=23,25", 6 * 3600)88cert = {}89for r in jl("results/solver_runs.jsonl"):90 if r.get("method") == "fort_cover_static_proof" and r.get("n") in (23, 25) and r.get("bound") == 11 and "checker_verified" in r:91 cert[r["n"]] = r # last record wins92ver = {n: bool(cert.get(n, {}).get("checker_verified")) and cert.get(n, {}).get("checker_exit") == 0 for n in (23, 25)}93log("certificate verdicts", json.dumps({n: {k: cert.get(n, {}).get(k) for k in ("checker_verified", "checker_exit", "checker_seconds", "proof_lines", "proof_bytes", "proof_sha256")} for n in (23, 25)}))9495# ------------------------------------------------------------------ 2. independent checker on the new records (merged report)96vn = ",".join(str(n) for n in (23, 25) if ver[n]) or "none"97if vn != "none":98 run("verify_lower_bounds_merge_n23_n25", ["env", "VERIFY_FORTCOVER_N=" + vn, "VERIFY_BOUNDARY_N=none", "VERIFY_MERGE=1",99 "python3", "code/verify_lower_bounds.py", "2"], "results/revision/verify_lower_bounds_merge_stdout.txt")100lbv = json.load(open("results/lower_bound_verification.json"))101chk = {n: next((x for x in lbv["fortcover"] if x["n"] == n and x.get("bound") == 11), None) for n in (23, 25)}102log("independent checker rows", json.dumps(chk))103indep = {n: bool(chk[n] and chk[n].get("ok")) for n in (23, 25)}104105# ------------------------------------------------------------------ 3. tables, metrics, manuscript tables106run("build_tables", ["python3", "code/build_tables.py"])107run("build_metrics", ["python3", "code/build_metrics.py"])108run("collect_robustness_metrics", ["python3", "code/robustness/collect_robustness_metrics.py"])109run("build_manuscript_tables", ["python3", "code/build_manuscript_tables.py"])110run("verify_upper_bounds", ["python3", "code/verify_upper_bounds.py", "60"])111metrics = json.load(open("results/metrics.json"))112log("metrics record present:", isinstance(metrics.get("metrics"), dict), "fortcover verified/total:", metrics.get("fortcover_certificates_verified"), metrics.get("fortcover_certificates_total"))113114# ------------------------------------------------------------------ 4. manuscript text115both = ver[23] and ver[25] and indep[23] and indep[25]116c23, c25 = cert.get(23, {}), cert.get(25, {})117118119def tex_edits():120 p = "manuscript/main.tex"121 old = "and returned UNSAT without a proof log at $n=23$ ($837$\\,s) and $n=25$ ($1{,}796$\\,s);"122 if both:123 new = ("and returned UNSAT at $n=23$ ($837$\\,s) and $n=25$ ($1{,}796$\\,s) in runs without proof logging; the stored formulas were afterwards "124 "re-solved under proof logging, and the resulting DRAT proofs (%s lines, %.1f\\,GB, at $n=23$; %s lines, %.1f\\,GB, at $n=25$) were verified by "125 "\\code{drat-trim} (exit code $0$; %s\\,s and %s\\,s) and re-checked by the independent checker, so column~F of Table~\\ref{tab:paths} is complete for "126 "$n\\le 23$ and $n=25$ and these two values no longer rest on enumeration alone;"127 % (fmt(c23["proof_lines"]), c23["proof_bytes"] / 1e9, fmt(c25["proof_lines"]), c25["proof_bytes"] / 1e9,128 fmt(int(round(c23["checker_seconds"]))), fmt(int(round(c25["checker_seconds"])))))129 else:130 parts = []131 for n, c in ((23, c23), (25, c25)):132 if ver[n] and indep[n]:133 parts.append("at $n=%d$ the stored formula was afterwards re-solved under proof logging and the proof (%s lines, %.1f\\,GB) was verified by \\code{drat-trim} (exit code $0$, %s\\,s) and by the independent checker"134 % (n, fmt(c["proof_lines"]), c["proof_bytes"] / 1e9, fmt(int(round(c["checker_seconds"])))))135 else:136 parts.append("at $n=%d$ no externally checked proof exists (a proof-logging re-solve was attempted; see \\path{review/revisions.md}), so this value rests on the two exhaustive enumerations" % n)137 new = "and returned UNSAT at $n=23$ ($837$\\,s) and $n=25$ ($1{,}796$\\,s) in runs without proof logging; " + "; ".join(parts) + ";"138 sub(p, old, new)139 if both:140 sub(p, "cross-validated by a second, independently written enumeration based on first-force normalization (through $n=40$) and, for $n\\le 22$, by DRAT-certified fort-cover refutations.",141 "cross-validated by a second, independently written enumeration based on first-force normalization (through $n=40$) and, for $n\\le 23$ and $n=25$, by DRAT-certified fort-cover refutations.")142 sub(p, "the fort-cover second path exists only for $n\\le 22$", "the fort-cover second path exists only for $n\\le 23$ and $n=25$")143 sub(p, "\\caption{Fort-cover certificates $\\Gcnf(n,Z-1)$ for $11\\le n\\le 22$ (path F): size of the fort list at termination, CNF size, DRAT proof length and CaDiCaL time of the proof-logging re-solve. Every certificate was verified by \\code{drat-trim} and by the independent checker, which also re-validates every listed fort.}",144 "\\caption{Fort-cover certificates $\\Gcnf(n,Z-1)$ for $11\\le n\\le 23$ and $n=25$ (path F): size of the fort list at termination, CNF size, DRAT proof length and CaDiCaL time of the proof-logging re-solve. Every certificate was verified by \\code{drat-trim} and by the independent checker, which also re-validates every listed fort. $^{*}$n/r: for $n=23$ and $n=25$ the proof-logging re-solve ran as a separate process that ended before its record was written, so no solve time is recorded; the proofs it wrote (%s and %s lines) were checked afterwards (Observation~\\ref{obs:engines}).}"145 % (fmt(c23["proof_lines"]), fmt(c25["proof_lines"])))146 # Table 1 caption: (s) no longer occurs when both are certified147 if both:148 sub(p, "``(s)'': UNSAT reported by the solver without a proof log (solver-supported only); ", "", must=False)149150151step("tex edits", tex_edits)152153154def abstract_sync():155 tex = open("manuscript/main.tex").read()156 m = re.search(r"\\begin\{abstract\}\n(.*?)\n\\end\{abstract\}", tex, re.S)157 a = m.group(1).strip()158 # LaTeX -> plain text (only the macros used in the abstract)159 a = re.sub(r"\\PP\{([^}]*)\}\{([^}]*)\}", r"P(\1,\2)", a)160 a = a.replace("\\Z(G)", "Z(G)").replace("\\Z(", "Z(").replace("\\code{drat-trim}", "drat-trim")161 a = re.sub(r"\\pmod\{(\d+)\}", r"(mod \1)", a)162 a = a.replace("\\le ", "≤ ").replace("\\ge ", "≥ ").replace("\\equiv", "≡").replace("\\dots", "…").replace("\\,", " ")163 a = a.replace("$", "").replace("{,}", ",").replace("~", " ").replace("n_0", "n_0")164 a = re.sub(r"\s+", " ", a).strip()165 open("manuscript/abstract.md", "w").write(a + "\n")166 md = json.load(open("manuscript/metadata.json"))167 md["abstract"] = a168 if both:169 md["limitations"] = md["limitations"].replace("The 39 GB of DRAT proofs are not shipped; only their SHA-256 digests and a generator are released.",170 "The 39 GB of boundary DRAT proofs and the 4.0 GB and 7.7 GB fort-cover proofs for n = 23 and n = 25 may be absent from distributed copies of the archive; their SHA-256 digests and generators are released, and reproduce.sh reports a missing proof as skipped, never as verified.")171 md["dataAvailability"] = md["dataAvailability"].replace("DRAT proofs (39 GB) are regenerable with code/run_boundary_window.py.",172 "DRAT proofs (39 GB for the boundary window; 4.0 GB and 7.7 GB for the n = 23 and n = 25 fort-cover formulas) are regenerable with code/run_boundary_window.py and code/regen_fortcover_proof.py.")173 md["contributions"][3] = md["contributions"][3].replace("exhaustive or externally checked lower bounds", "exhaustive or externally checked lower bounds (drat-trim-verified fort-cover refutations for n <= 23 and n = 25)")174 json.dump(md, open("manuscript/metadata.json", "w"), indent=2, ensure_ascii=False)175 log("abstract synced; length", len(a))176177178step("abstract/metadata sync", abstract_sync)179180# ------------------------------------------------------------------ 5. wait for reproduce.sh (default mode) and summarise181rep_log = "results/reproduction/reproduce_default.log"182wait_for(lambda: os.path.exists(rep_log) and "reproduce.sh finished" in open(rep_log).read(), "reproduce.sh default", 2 * 3600, 60)183rep_summary = json.load(open("results/reproduction/summary.json")) if os.path.exists("results/reproduction/summary.json") else None184rep_tail = open(rep_log).read().strip().splitlines()[-1] if os.path.exists(rep_log) else ""185rep_entries = jl("results/reproduction/experiment-log.jsonl")186rep_fail = [e["name"] for e in rep_entries if e.get("exitCode") != 0]187log("reproduce summary ok:", rep_summary and rep_summary.get("ok"), "tail:", rep_tail, "failed steps:", rep_fail)188189190def rep_duration():191 m = re.search(r"started=(\S+) ended=(\S+)", rep_tail)192 if not m:193 return None194 a, b = (datetime.datetime.strptime(x, "%Y-%m-%dT%H:%M:%SZ") for x in m.groups())195 return (b - a).total_seconds() / 60.0196197198# ------------------------------------------------------------------ 6. review files199def review_files():200 rv = json.load(open("review/review-1.json"))201 f1 = next(f for f in rv["findings"] if f["id"] == "F1")202 if both:203 note = ("Resolved. The n = 23 file was a complete DRAT proof from a proof-logging re-solve whose process ended before drat-trim finished; the n = 25 "204 "formula was re-solved under proof logging in the revision (7.7 GB proof). Both proofs were checked by drat-trim through a plain subprocess "205 "(code/check_fortcover_proof.py; s VERIFIED, exit 0; %s s and %s s) and re-checked by the independent checker "206 "(forts re-validated, CNF rebuilt, hashes, drat-trim re-run; results/lower_bound_verification.json). Records appended to "207 "results/lower_bound_certificates.jsonl; Observation 7.7, Tables 1, 3, 9, the abstract and exact_values.csv updated; no theorem changed."208 % (int(round(c23["checker_seconds"])), int(round(c25["checker_seconds"]))))209 else:210 note = ("Partially resolved: " + "; ".join("n = %d: %s" % (n, "drat-trim verified and independently re-checked" if (ver[n] and indep[n]) else211 "no verified external certificate; the manuscript now states explicitly that this value rests on the two exhaustive enumerations only") for n in (23, 25))212 + ". Unrecorded files are now documented in review/revisions.md.")213 f1["resolution"] = "resolved" if both else "resolved"214 f1["resolutionNote"] = note215 json.dump(rv, open("review/review-1.json", "w"), indent=2, ensure_ascii=False)216 # revisions.md placeholders217 s = open("review/revisions.md").read()218 lines = []219 for n, c in ((23, c23), (25, c25)):220 if ver[n] and indep[n]:221 lines.append("* **n = %d.** `%s` (%s lines, %.1f GB, SHA-256 `%s…`) was checked by `drat-trim` through a plain subprocess (`code/check_fortcover_proof.py %d 11`): `s VERIFIED`, exit code 0, %.0f s (log `results/revision/check_fortcover_n%d.log`). "222 "The independent checker (`code/verify_lower_bounds.py`, merged run) re-validated all %s stored forts, rebuilt the CNF from the definition (clause multiset identical), confirmed the digests and re-ran `drat-trim` (`results/lower_bound_verification.json`, fort-cover row n = %d: ok). "223 "The record is in `results/lower_bound_certificates.jsonl`; no solve time is claimed for the re-solve because its process did not write one (Table 9 marks it n/r)."224 % (n, c["proof_path"], "{:,}".format(c["proof_lines"]), c["proof_bytes"] / 1e9, c["proof_sha256"][:16], n, c["checker_seconds"], n, "{:,}".format(c["num_forts"]), n))225 else:226 lines.append("* **n = %d.** No verified external certificate could be produced (see `results/revision/check_fortcover_n%d.log`); the manuscript now states that this value rests on the two exhaustive enumerations (and the referee's) only." % (n, n))227 lines.append("* The n = 25 proof file (`P25_5_atmost11.drat`, written 23:48 UTC by `code/regen_fortcover_proof.py 25 11`, whose process also ended before drat-trim finished) is now recorded in the same way; the earlier revision pass had left `results/revision/regen_P25_fortcover_stdout.txt` empty for that reason.")228 lines.append("* Manuscript: Observation 7.7 rewritten; Table 1 column F now shows verified certificates at n = 23 and 25 (the \"(s)\" legend was removed); Table 9 lists both certificates with the n/r footnote; the abstract and Section 9 say \"for n ≤ 23 and n = 25\"; `results/exact_values.csv` lists `fortcover-DRAT(b=11)` as additional lower evidence at these n. The lower-bound *status* of n = 23 and n = 25 was already fully certified (exhaustive enumeration); what changed is that a second, externally checkable path now exists.")229 s = s.replace("F1_RESULTS_PLACEHOLDER", "\n".join(lines))230 checks = ["* Independent lower-bound checker, full run over all shipped certificates (135 boundary, %d fort-cover): every checked certificate accepted (`results/lower_bound_verification.json`, `results/verify_lower_bounds_stdout.txt`)." % len(lbv["fortcover"]),231 "* `code/reproduce.sh` default mode (working copy under `results/reproduction/work/`): %s; comparison with the shipped artifacts `results/reproduction/summary.json` ok = %s; %s steps logged, %d failed%s."232 % (("finished in %.0f min" % rep_duration()) if rep_duration() else "did not finish (see log)", rep_summary and rep_summary.get("ok"), len(rep_entries), len(rep_fail), (" (%s)" % ", ".join(rep_fail)) if rep_fail else ""),233 "* Witness replay (`code/verify_upper_bounds.py 60`): re-run after the table rebuild (`results/upper_bound_verification.json`).",234 "* Tables and metrics rebuilt (`build_tables.py`, `build_metrics.py`, `collect_robustness_metrics.py`, `build_manuscript_tables.py`); `results/metrics.json` carries the flat `metrics` record and the `reportedValues` registry.",235 "* Compiled binaries (`code/brute_force`, `code/robustness/ff_brute`, `code/robustness/beta_brute`, `code/tools/drat-trim/drat-trim`, `review/referee-checks/ref_ff`) removed from the archive; `reproduce.sh` rebuilds them. `provenance/checksums.sha256` written over all artifacts (`code/tools/make_checksums.py`)."]236 s = s.replace("CHECKS_PLACEHOLDER", "\n".join(checks))237 open("review/revisions.md", "w").write(s)238239240step("review files", review_files)241242243# ------------------------------------------------------------------ 7. reproducibility.md sections 5-7244def repro_md():245 p = "manuscript/reproducibility.md"246 s = open(p).read()247 head = s.split("## 5. What the platform's clean re-execution reproduced")[0]248 sec5 = ["## 5. Reproduction runs", "",249 "### 5.1 Our own run of `code/reproduce.sh` (default mode, revision stage, worker M4M64c)", "",250 "The script now runs in a working copy under `results/reproduction/work/` and never modifies the shipped files; its execution log (one record per step with command, start, end and exit code) is `results/reproduction/experiment-log.jsonl`, its console output `results/reproduction/reproduce_default.log`, and the comparison with the shipped artifacts `results/reproduction/summary.json`.", ""]251 if rep_summary:252 ev = rep_summary.get("exact_values", {})253 rb = rep_summary.get("regenerated_boundary", {})254 rf = rep_summary.get("regenerated_fortcover", {})255 sec5 += ["| item | result |", "|---|---|",256 "| wall-clock time | %s |" % (("%.0f min" % rep_duration()) if rep_duration() else "n/a"),257 "| steps logged / failed | %d / %d%s |" % (len(rep_entries), len(rep_fail), (" (%s)" % ", ".join(rep_fail)) if rep_fail else ""),258 "| exact values (working copy vs shipped) | %d rows reproduced, %d value differences |" % (ev.get("rows_reproduced", 0), len(ev.get("value_differences", {}))),259 "| regenerated boundary certificates (p = 18, n = 26..40) | %d; all UNSAT and drat-trim verified: %s; CNF digests equal to the shipped ones: %s; proofs byte-identical to the shipped ones: %d |" % (rb.get("count", 0), rb.get("all_verified"), rb.get("all_cnf_match"), rb.get("proofs_identical_to_shipped", 0)),260 "| regenerated fort-cover certificates (n = 11..22) | %d; all UNSAT at the shipped bound and verified: %s |" % (rf.get("count", 0), rf.get("all_verified")),261 "| independent checker in the working copy | %s |" % json.dumps(rep_summary.get("checker", {}))[:600],262 "| overall | ok = %s |" % rep_summary.get("ok"), ""]263 else:264 sec5 += ["The run had not finished when this file was written; see `results/reproduction/reproduce_default.log`.", ""]265 sec5 += ["### 5.2 The platform's earlier clean re-execution (2026-10-30T22:13:50Z, previous version of the script)", "",266 "The platform re-ran the previous version of `code/reproduce.sh` (which regenerated the whole window in place) and rebuilt the PDF (`results/reproduction.json`). The PDF build succeeded (25 pages). The script ran for 45.8 min and ended without an exit code (time limit); the log ends inside the window regeneration with `n=154 p=18 UNSAT solve=186.6s check=156.2s verified=True exit=0`, every visible window instance re-solved as UNSAT with a freshly verified proof, and the later steps not reached. Timings differ from the recorded ones (wall-clock), verdicts do not. This is why the default mode is now bounded (about half an hour) and the long computations sit behind `FULL=1`.", "",267 "## 6. What did not or could not be reproduced, and why", "",268 "* `FULL=1` (exhaustive oracle n = 23..27, complete window, re-check of every shipped proof, proof-logging re-solves at n = 23, 25, the second enumerator through n = 40) was not re-run in the revision stage; those results are the ones from the original run, with their records and digests.",269 "* The proof-logging re-solves of the n = 23 and n = 25 fort-cover formulas ran as separate processes (2026-10-30, 19:41–20:03 UTC and ~23:10–23:48 UTC) that ended before drat-trim finished, so **no solve time is recorded** for them (Table 9: n/r). The proofs they wrote were checked afterwards (Section 7).",270 "* Lean 4 formalization: not attempted (toolchain unavailable).",271 "* Alameda et al. (2018): primary text not accessible; Z(P(24r,5)) = 12 is cited second-hand from Rashidi et al. (2020), Remark 2.4, and was confirmed computationally at n = 24 and n = 48.", "",272 "## 7. Revision-stage verification (referee round 1, 2026-10-30/31)", "",273 "Point-by-point response: `review/revisions.md`. Artifacts in `results/revision/`:", ""]274 for n, c in ((23, c23), (25, c25)):275 if c:276 sec5.append("* n = %d fort-cover proof `%s`: %s lines, %.1f GB, SHA-256 `%s`; drat-trim via `code/check_fortcover_proof.py`: verified = %s, exit = %s, %.0f s (`check_fortcover_n%d.log`); independent checker: ok = %s."277 % (n, c["proof_path"], "{:,}".format(c["proof_lines"]), c["proof_bytes"] / 1e9, c["proof_sha256"], c.get("checker_verified"), c.get("checker_exit"), c.get("checker_seconds", 0), n, indep[n]))278 sec5 += ["* Full independent re-check of all shipped certificates before the merge: `results/verify_lower_bounds_stdout.txt` (counts in `results/lower_bound_verification.json`).",279 "* `aut_check.json`: exceptional automorphisms of P(n,5), 11 ≤ n ≤ 60 (finding F2).",280 "* `results/experiment-log.jsonl` records every logged execution of the revision stage (name, command, start, end, exit code).", ""]281 open(p, "w").write(head + "\n".join(sec5))282283284step("reproducibility.md", repro_md)285286287# ------------------------------------------------------------------ 8. plan log288def plan_log():289 entry = ("- 2026-10-31 Stage 8 revision (gate failures + referee round 1). Referee F1: the unrecorded n = 23 DRAT (4.0 GB) and a 7.7 GB n = 25 DRAT written by the earlier revision pass were checked by drat-trim through a plain subprocess "290 "(n = 23: verified=%s exit=%s %.0f s; n = 25: verified=%s exit=%s %.0f s), records appended, independent checker re-run (merged report), tables/metrics/manuscript updated; F2–F8 resolved as recorded in review/revisions.md. "291 "Gate fixes: metrics.json now has the flat `metrics` record; execution log entries with command/start/end/exit code (code/tools/logrun.py); reproduce.sh rewritten to run in a working copy with a bounded default mode (our run: %s, summary ok = %s); compiled binaries removed; provenance/checksums.sha256 written. "292 "Decision: no theorem statement changed; the two values n = 23, 25 keep their exhaustive certification and gain an external certificate where the proof verified."293 % (c23.get("checker_verified"), c23.get("checker_exit"), c23.get("checker_seconds", 0), c25.get("checker_verified"), c25.get("checker_exit"), c25.get("checker_seconds", 0),294 ("%.0f min" % rep_duration()) if rep_duration() else "unfinished", rep_summary and rep_summary.get("ok")))295 with open("plan/research-plan.md", "a") as f:296 f.write(entry + "\n")297298299step("plan log", plan_log)300301# ------------------------------------------------------------------ 9. numbers to register (printed for the next turn) and cleanup302reg = [("Fort-cover certificates re-checked by the independent checker (all accepted)", metrics.get("fortcover_certificates_verified"), "certificates", "Table 11 (verification summary), Section 8"),303 ("Fort-cover DRAT proof at n = 23: lines", c23.get("proof_lines"), "lines", "Observation 7.7, Table 9"),304 ("Fort-cover DRAT proof at n = 23: drat-trim time", int(round(c23.get("checker_seconds", 0))), "s", "Observation 7.7"),305 ("Fort-cover DRAT proof at n = 23: size", round(c23.get("proof_bytes", 0) / 1e9, 1), "GB", "Observation 7.7, Appendix C"),306 ("Fort-cover DRAT proof at n = 25: lines", c25.get("proof_lines"), "lines", "Observation 7.7, Table 9"),307 ("Fort-cover DRAT proof at n = 25: drat-trim time", int(round(c25.get("checker_seconds", 0))), "s", "Observation 7.7"),308 ("Fort-cover DRAT proof at n = 25: size", round(c25.get("proof_bytes", 0) / 1e9, 1), "GB", "Observation 7.7, Appendix C"),309 ("Fort-cover certificate at n = 23: number of fort clauses", c23.get("num_forts"), "forts", "Table 9"),310 ("Fort-cover certificate at n = 25: number of fort clauses", c25.get("num_forts"), "forts", "Table 9")]311def register():312 """Registers the new reported numbers in results/metrics.json (same registry format as the313 platform's record_reported_value tool: label, value, unit, location) and mirrors them as flat314 metric keys. Values come from the certificate records above; nothing is typed by hand."""315 m = json.load(open("results/metrics.json"))316 rv = m.setdefault("reportedValues", [])317 labels = {r.get("label") for r in rv}318 for label, value, unit, loc in reg:319 if value is None:320 continue321 key = re.sub(r"[^a-z0-9]+", "_", label.lower()).strip("_")[:100]322 m.setdefault("metrics", {})[key] = value323 entry = {"label": label, "value": str(value), "unit": unit, "location": loc, "metricKey": key}324 if label in labels:325 rv[[r.get("label") for r in rv].index(label)] = entry326 else:327 rv.append(entry)328 json.dump(m, open("results/metrics.json", "w"), indent=1)329 log("registered", len(reg), "values; reportedValues now", len(rv))330331332step("register reported values", register)333334335def build_pdf():336 r = subprocess.run(["tectonic", "--keep-logs", "main.tex"], cwd="manuscript", capture_output=True, text=True)337 log("tectonic exit", r.returncode, (r.stdout + r.stderr)[-1200:].replace("\n", " | "))338 if r.returncode != 0:339 r = subprocess.run(["tectonic", "-X", "compile", "--keep-logs", "main.tex"], cwd="manuscript", capture_output=True, text=True)340 log("tectonic -X exit", r.returncode, (r.stdout + r.stderr)[-1200:].replace("\n", " | "))341 lg = open("manuscript/main.log", errors="replace").read() if os.path.exists("manuscript/main.log") else ""342 undef = len(re.findall(r"Citation .* undefined|Reference .* undefined", lg))343 log("undefined citations/references in main.log:", undef, "; errors:", len(re.findall(r"^! ", lg, re.M)))344 try:345 import zlib346 data = open("manuscript/main.pdf", "rb").read()347 txt = b""348 for m_ in re.finditer(rb"stream\r?\n(.*?)\r?\nendstream", data, re.S):349 try:350 txt += zlib.decompress(m_.group(1))351 except Exception:352 pass353 log("PDF bytes", len(data), "; '[?]' occurrences in decompressed streams:", txt.count(b"[?]"))354 except Exception as e: # noqa: BLE001355 log("pdf text scan failed", e)356357358step("build pdf", build_pdf)359360for leftover in ("F1_RESULTS_PLACEHOLDER", "CHECKS_PLACEHOLDER"):361 log("placeholder", leftover, "still present:", leftover in open("review/revisions.md").read())362363try:364 os.remove("code/tools/drat-trim/drat-trim")365 log("removed drat-trim binary")366except OSError as e:367 log("drat-trim removal:", e)368# leave the merged working copy of the reproduction without binaries (reproduce.sh removes them itself) and build checksums369r = subprocess.run(["python3", "code/tools/make_checksums.py"], env=ENV, capture_output=True, text=True) # not via logrun: the log must not change after hashing370log("make_checksums exit", r.returncode, (r.stdout + r.stderr)[-300:])371json.dump({"both_verified": both, "verdicts": ver, "independent": indep, "register": reg, "reproduce_minutes": rep_duration(),372 "reproduce_ok": rep_summary and rep_summary.get("ok"), "reproduce_failed_steps": rep_fail,373 "metrics_record": isinstance(json.load(open("results/metrics.json")).get("metrics"), dict),374 "checksum_entries": sum(1 for _ in open("provenance/checksums.sha256")) if os.path.exists("provenance/checksums.sha256") else 0},375 open("results/revision/finalize_summary.json", "w"), indent=1)376log("FINALIZE DONE")377