1"""Builds results/metrics.json, results/tables/*.csv and consolidates2results/counterexamples.jsonl from the raw result files. Run after3build_tables.py, verify_upper_bounds.py and verify_lower_bounds.py."""4import collections5import csv6import json7import math8import os910import common11from build_tables import HOLDOUT, load_jsonl1213R = common.RESULTS14T = os.path.join(R, "tables")15os.makedirs(T, exist_ok=True)161718def main():19 rows = list(csv.DictReader(open(os.path.join(R, "exact_values.csv"))))20 bf = json.load(open(os.path.join(R, "brute_force_values.json")))21 bfr = load_jsonl("brute_force_runs.jsonl")22 bnd = [r for r in load_jsonl("boundary_certificates.jsonl") if "error" not in r]23 lbv = json.load(open(os.path.join(R, "lower_bound_verification.json")))24 ubv = json.load(open(os.path.join(R, "upper_bound_verification.json")))25 btab = [r for r in load_jsonl("boundary_table.jsonl") if "beta" in r]26 runs = load_jsonl("solver_runs.jsonl")27 hold = load_jsonl("holdout_results.jsonl")28 lemma = json.load(open(os.path.join(R, "lemma_checks.json")))29 t1 = json.load(open(os.path.join(R, "t1_graph_invariants.json")))30 t2 = json.load(open(os.path.join(R, "t2_order_independence.json")))3132 status_counts = collections.Counter(r["status"] for r in rows)33 certified = [int(r["n"]) for r in rows if r["status"] == "fully certified"]34 p18 = sorted({r["n"] for r in bnd if r["p"] == 18 and r["sat"] is False and r.get("checker_verified")})35 p18_ok = sorted({x["n"] for x in lbv["boundary"] if x["p"] == 18 and x["ok"]})36 window_complete = all(n in p18_ok for n in range(26, 155))37 solve = [r["solve_seconds"] for r in bnd if r["p"] == 18 and r["sat"] is False]38 check = [r["checker_seconds"] for r in bnd if r["p"] == 18 and r["sat"] is False]39 plines = [r["proof_lines"] for r in bnd if r["p"] == 18 and r["sat"] is False]40 # window-only statistics (26 <= n <= 154; excludes the n = 24 cross-check certificate)41 win = [r for r in bnd if r["p"] == 18 and r["sat"] is False and 26 <= r["n"] <= 154]42 wsolve = [r["solve_seconds"] for r in win]43 wcheck = [r["checker_seconds"] for r in win]44 wlines = [r["proof_lines"] for r in win]45 wbytes = sum(os.path.getsize(os.path.join(common.ROOT, r["proof_path"])) for r in win if os.path.exists(os.path.join(common.ROOT, r["proof_path"])))46 fort_ok_n = sorted({x["n"] for x in lbv["fortcover"] if x["ok"]})47 bf_total_subsets = sum(r["enumerated_subsets"] for r in bfr)48 bf_total_wall = sum(r["wall_seconds"] for r in bfr)49 bf_max_n = max(int(n) for n, v in bf.items() if v["Z"] is not None)50 values = {int(r["n"]): (int(r["Z"]) if r["Z"] else None) for r in rows}51 holdout_pred_ok = all(values.get(n) == 12 for n in HOLDOUT)52 exceptions = {n: values[n] for n in range(11, 23)}53 metrics = {54 "utc": common.utcnow(),55 "k": 5,56 "n_range_tabulated": [11, 48],57 "status_counts": dict(status_counts),58 "fully_certified_n": certified,59 "largest_fully_certified_n": max(certified) if certified else None,60 "values_11_to_22": exceptions,61 "threshold_n0": 23,62 "value_at_and_above_threshold": 12,63 "Z_P22_5": values.get(22),64 "Z_P23_5": values.get(23),65 "Z_P25_5": values.get(25),66 "boundary_parameter_p": 18,67 "boundary_n1": 26,68 "boundary_c_max": 14,69 "boundary_N_max": 154,70 "boundary_window_instances": len(p18_ok),71 "boundary_window_complete_26_to_154": window_complete,72 "boundary_window_all_drat_verified": all(x["ok"] for x in lbv["boundary"] if x["p"] == 18),73 "boundary_p18_solve_seconds": {"min": min(solve), "max": max(solve), "median": sorted(solve)[len(solve) // 2], "total": round(sum(solve), 1)} if solve else None,74 "boundary_p18_check_seconds": {"min": min(check), "max": max(check), "median": sorted(check)[len(check) // 2], "total": round(sum(check), 1)} if check else None,75 "boundary_p18_proof_lines": {"min": min(plines), "max": max(plines), "total": sum(plines)} if plines else None,76 "boundary_window_solve_seconds": {"min": min(wsolve), "max": max(wsolve), "mean": round(sum(wsolve) / len(wsolve), 1), "total": round(sum(wsolve), 1)} if wsolve else None,77 "boundary_window_check_seconds": {"min": min(wcheck), "max": max(wcheck), "mean": round(sum(wcheck) / len(wcheck), 1), "total": round(sum(wcheck), 1)} if wcheck else None,78 "boundary_window_proof_lines": {"min": min(wlines), "max": max(wlines), "total": sum(wlines)} if wlines else None,79 "boundary_window_proof_bytes": wbytes,80 "boundary_window_proof_gigabytes": round(wbytes / 1e9, 1),81 "fortcover_certified_n": fort_ok_n,82 "fortcover_largest_n": max(fort_ok_n) if fort_ok_n else None,83 "boundary_p18_cnf_vars_at_154": next((r["num_vars"] for r in bnd if r["p"] == 18 and r["n"] == 154), None),84 "boundary_p18_cnf_clauses_at_154": next((r["num_clauses"] for r in bnd if r["p"] == 18 and r["n"] == 154), None),85 "boundary_obstruction_n25_p18_beta": next((r["beta"] for r in btab if r["n"] == 25 and r["p"] == 18), None),86 "boundary_table_cells": len(btab),87 "boundary_table_p_range": [min(r["p"] for r in btab), max(r["p"] for r in btab)],88 "boundary_table_n_range": [min(r["n"] for r in btab), max(r["n"] for r in btab)],89 "boundary_fails_at_25_for_all_p_tested": all(any(r["n"] == 25 and r["p"] == p and r["beta"] <= 11 for r in btab) for p in range(12, 25)),90 "brute_force_max_n": bf_max_n,91 "brute_force_total_subsets_enumerated": bf_total_subsets,92 "brute_force_total_wall_seconds": round(bf_total_wall, 1),93 "brute_force_n23_subsets_size11": next((r["enumerated_subsets"] for r in bfr if r["n"] == 23 and r["s"] == 11), None),94 "brute_force_n25_subsets_size11": next((r["enumerated_subsets"] for r in bfr if r["n"] == 25 and r["s"] == 11), None),95 "fortcover_certificates_verified": sum(1 for x in lbv["fortcover"] if x["ok"]),96 "fortcover_certificates_total": len(lbv["fortcover"]),97 "upper_witness_replays_ok": sum(1 for x in ubv["witnesses"] if x["replay_ok"]),98 "upper_witness_replays_total": len(ubv["witnesses"]),99 "P7_replays_ok_12_to_60": all(x["replay_ok"] for x in ubv["P7"]),100 "T1_all_ok": all(r["all_ok"] for r in t1),101 "T1_n_count": len(t1),102 "T2_passed": sum(r["passed"] for r in t2),103 "T2_total": sum(r["total"] for r in t2),104 "CS6_mismatches": lemma["CS6_boundary_identity"]["mismatches"],105 "CS6_total": lemma["CS6_boundary_identity"]["total"],106 "T8_mismatches": lemma["T8_deletion_map"]["mismatches"],107 "T8_total": lemma["T8_deletion_map"]["total"],108 "holdout": sorted(HOLDOUT),109 "holdout_values": {str(n): values.get(n) for n in sorted(HOLDOUT)},110 "holdout_prediction_12_all_correct": holdout_pred_ok,111 "holdout_fortcover_search_timeouts": sum(1 for h in hold if h["sat"] is None),112 "holdout_fortcover_search_witness_found": sum(1 for h in hold if h["sat"]),113 "round_sat_unsat_agreements": sorted({r["n"] for r in runs if r.get("method") == "round_sat" and r.get("sat") is False}),114 "round_sat_timeouts": sorted({r["n"] for r in runs if r.get("method") == "round_sat" and r.get("sat") is None}),115 "versions": common.versions(),116 "drat_trim_source_sha256": lbv.get("drat_trim_sha256"),117 "worker": "M4M64c (16 cores, Apple Silicon, macOS 26.4)",118 }119 # flat copy of the scalar headline metrics under "metrics" (the platform's120 # metrics comparison expects a record at this key; reportedValues may point121 # to these keys through metricKey)122 metrics["metrics"] = {k: v for k, v in metrics.items() if isinstance(v, (int, float, str, bool))}123 # keep the platform-written registry of reported values, if present124 mpath = os.path.join(R, "metrics.json")125 if os.path.exists(mpath):126 try:127 old = json.load(open(mpath))128 if "reportedValues" in old:129 metrics["reportedValues"] = old["reportedValues"]130 except Exception:131 pass132 with open(mpath, "w") as f:133 json.dump(metrics, f, indent=1)134 # tables135 with open(os.path.join(T, "exact_values.csv"), "w", newline="") as f:136 w = csv.writer(f)137 w.writerow(["n", "Z", "status", "lower_evidence", "upper_evidence", "known"])138 for r in rows:139 w.writerow([r["n"], r["Z"], r["status"], r["lower_evidence"], r["upper_evidence"], ""])140 with open(os.path.join(T, "boundary_table.csv"), "w", newline="") as f:141 w = csv.writer(f)142 ns = sorted({r["n"] for r in btab})143 w.writerow(["p"] + ns)144 for p in sorted({r["p"] for r in btab}):145 d = {r["n"]: r["beta"] for r in btab if r["p"] == p}146 w.writerow([p] + [(d[n] if d.get(n, 99) <= 11 else ">=12") for n in ns])147 with open(os.path.join(T, "boundary_window_p18.csv"), "w", newline="") as f:148 w = csv.writer(f)149 w.writerow(["n", "num_vars", "num_clauses", "solve_seconds", "proof_lines", "check_seconds", "verified", "cnf_sha256", "proof_sha256"])150 for r in sorted((r for r in bnd if r["p"] == 18 and r["sat"] is False), key=lambda r: r["n"]):151 w.writerow([r["n"], r["num_vars"], r["num_clauses"], r["solve_seconds"], r["proof_lines"], r["checker_seconds"], r["checker_verified"], r["cnf_sha256"][:16], r["proof_sha256"][:16]])152 with open(os.path.join(T, "brute_force.csv"), "w", newline="") as f:153 w = csv.writer(f)154 w.writerow(["n", "s", "subsets", "orbit_representatives", "forcing_representatives", "wall_seconds"])155 for r in sorted(bfr, key=lambda r: (r["n"], r["s"])):156 if r["enumerated_subsets"]:157 w.writerow([r["n"], r["s"], r["enumerated_subsets"], r["orbit_representatives_tested"], r["forcing_representatives"], r["wall_seconds"]])158 print(json.dumps({k: v for k, v in metrics.items() if k not in ("versions",)}, indent=1))159160161if __name__ == "__main__":162 main()163