1"""Compares a reproduction working copy with the shipped artifacts and writes a summary.23usage: python3 code/tools/compare_reproduction.py WORK ROOT MODE OUT.json45Checks (none of them modifies the shipped artifacts):6 1. exact values: every (n, Z) in WORK/results/exact_values.csv equals the shipped one;7 2. regenerated boundary certificates (records in WORK whose paths are outside8 code/proofs/certificates): the regenerated CNF has the same SHA-256 as the shipped9 CNF for the same (n, p) (the formula is deterministic), the solver reported UNSAT10 and drat-trim verified the regenerated proof;11 3. regenerated fort-cover certificates: the solver reported UNSAT at the same bound as12 the shipped record and the regenerated proof was verified; the fort list produced13 by the lazy loop may legitimately differ from the shipped one, so CNF digests are14 reported but not required to agree;15 4. every certificate the independent checker actually checked in WORK was accepted.16Exit code 0 iff checks 1, 2 (UNSAT + verified), 3 (UNSAT + verified) and 4 pass.17"""18import csv19import datetime20import json21import os22import sys232425def jl(path):26 return [json.loads(l) for l in open(path)] if os.path.exists(path) else []272829def main(work, root, mode, out_path):30 rep = {"utc": datetime.datetime.now(datetime.timezone.utc).isoformat(timespec="seconds"), "mode": mode, "work": work}31 ok = True32 # 1 exact values33 def vals(p):34 return {int(r["n"]): (r["Z"], r["status"]) for r in csv.DictReader(open(p))} if os.path.exists(p) else {}35 shipped, regen = vals(os.path.join(root, "results", "exact_values.csv")), vals(os.path.join(work, "results", "exact_values.csv"))36 diff = {n: {"shipped": shipped.get(n), "reproduced": regen.get(n)} for n in sorted(set(shipped) | set(regen)) if shipped.get(n, (None,))[0] != regen.get(n, (None,))[0]}37 rep["exact_values"] = {"rows_shipped": len(shipped), "rows_reproduced": len(regen), "value_differences": diff}38 ok &= not diff and bool(regen)39 # 2 regenerated boundary certificates40 shipped_b = {(r["n"], r["p"]): r for r in jl(os.path.join(root, "results", "boundary_certificates.jsonl")) if r.get("sat") is False}41 rows = []42 for r in jl(os.path.join(work, "results", "boundary_certificates.jsonl")):43 if r.get("sat") is not False or r.get("cnf_path", "").startswith("code/proofs/certificates"):44 continue # shipped record copied into WORK, or SAT/timeout45 s = shipped_b.get((r["n"], r["p"]))46 row = {"n": r["n"], "p": r["p"], "unsat": True, "verified": bool(r.get("checker_verified")) and r.get("checker_exit") == 0,47 "cnf_sha_matches_shipped": (s is not None and s["cnf_sha256"] == r["cnf_sha256"]),48 "proof_sha_matches_shipped": (s is not None and s.get("proof_sha256") == r.get("proof_sha256"))}49 rows.append(row)50 ok &= row["verified"] and row["cnf_sha_matches_shipped"]51 rep["regenerated_boundary"] = {"count": len(rows), "all_verified": all(x["verified"] for x in rows), "all_cnf_match": all(x["cnf_sha_matches_shipped"] for x in rows),52 "proofs_identical_to_shipped": sum(1 for x in rows if x["proof_sha_matches_shipped"]), "rows": rows}53 # 3 regenerated fort-cover certificates54 shipped_f = {(r["n"], r["bound"]): r for r in jl(os.path.join(root, "results", "lower_bound_certificates.jsonl"))}55 rows = []56 for r in jl(os.path.join(work, "results", "lower_bound_certificates.jsonl")):57 if r.get("cnf_path", "").startswith("code/proofs/certificates"):58 continue59 s = shipped_f.get((r["n"], r["bound"]))60 row = {"n": r["n"], "bound": r["bound"], "shipped_record_exists_at_same_bound": s is not None,61 "verified": bool(r.get("checker_verified")) and r.get("checker_exit") == 0,62 "cnf_sha_matches_shipped": (s is not None and s["cnf_sha256"] == r["cnf_sha256"]), "num_forts": r.get("num_forts")}63 rows.append(row)64 ok &= row["verified"] and row["shipped_record_exists_at_same_bound"]65 rep["regenerated_fortcover"] = {"count": len(rows), "all_verified": all(x["verified"] for x in rows), "rows": rows}66 # 4 independent checker verdicts in WORK67 checker = {}68 for name in ("lower_bound_verification.json", "lower_bound_verification_regenerated.json"):69 p = os.path.join(work, "results", name)70 if os.path.exists(p):71 v = json.load(open(p))72 checker[name] = {"counts": v.get("counts"), "all_checked_ok": v.get("all_checked_ok", v.get("all_ok"))}73 ok &= bool(checker[name]["all_checked_ok"])74 p = os.path.join(work, "results", "upper_bound_verification.json")75 if os.path.exists(p):76 v = json.load(open(p))77 checker["upper_bound_verification.json"] = {"witnesses_ok": sum(1 for x in v["witnesses"] if x["replay_ok"]), "witnesses": len(v["witnesses"]),78 "P7_all_ok": all(x["replay_ok"] for x in v["P7"])}79 ok &= checker["upper_bound_verification.json"]["witnesses_ok"] == checker["upper_bound_verification.json"]["witnesses"]80 rep["checker"] = checker81 rep["ok"] = bool(ok)82 os.makedirs(os.path.dirname(out_path), exist_ok=True)83 json.dump(rep, open(out_path, "w"), indent=1)84 print(json.dumps({k: v for k, v in rep.items() if k not in ("regenerated_boundary", "regenerated_fortcover")}, indent=1))85 print("regenerated boundary:", {k: v for k, v in rep["regenerated_boundary"].items() if k != "rows"})86 print("regenerated fort-cover:", {k: v for k, v in rep["regenerated_fortcover"].items() if k != "rows"})87 sys.exit(0 if ok else 1)888990if __name__ == "__main__":91 main(*sys.argv[1:5])92