1"""Aggregate every reduced-round SHA-256 result into results/reduced_round_sha256/summary.json (numbers the paper quotes).23 PYTHONPATH=src .venv/bin/python experiments/reduced_round_sha256/make_summary.py4"""5from __future__ import annotations6import json, pathlib, statistics, sys, time7from common import provenance, ROOT89RES = ROOT / "results" / "reduced_round_sha256"101112def load(name):13 p = RES / name14 return json.loads(p.read_text()) if p.exists() else None151617def main():18 t0 = time.time()19 out = {}20 # ---- diffusion21 docs = [json.loads(p.read_text()) for p in sorted(RES.glob("diffusion_seed*.json"))]22 if docs:23 diff = {}24 for cfg in docs[0]["params"]["configs"]:25 fds = [d["measurements"][cfg]["full_diffusion_step"] for d in docs]26 ratios = [d["measurements"][cfg]["mean_flip_ratio_by_step"] for d in docs]27 mean_ratio = [statistics.mean(r[t] for r in ratios) for t in range(64)]28 diff[cfg] = {"full_diffusion_step_by_seed": fds, "full_diffusion_step": max(fds),29 "mean_flip_ratio_by_step": [round(x, 4) for x in mean_ratio],30 "flip_ratio_step64": round(mean_ratio[63], 4),31 "hamming_mean_step64": round(statistics.mean(d["measurements"][cfg]["hamming_mean_by_step"][63] for d in docs), 2),32 "hamming_sd_step64": round(statistics.mean(d["measurements"][cfg]["hamming_sd_by_step"][63] for d in docs), 2),33 "random_oracle_flip_ratio": round(statistics.mean(d["measurements"][cfg]["random_oracle_control"]["flip_ratio_mean"] for d in docs), 4),34 "random_oracle_flip_sd": round(statistics.mean(d["measurements"][cfg]["random_oracle_control"]["flip_ratio_sd"] for d in docs), 4)}35 out["diffusion"] = {"n_per_seed": docs[0]["params"]["n"], "seeds": [d["seed"] for d in docs], "threshold": docs[0]["params"]["threshold"],36 "by_config": diff, "hosts": sorted({d["host"]["hostname"] for d in docs})}37 # ---- bias38 docs = [json.loads(p.read_text()) for p in sorted(RES.glob("bias_seed*.json"))]39 if docs:40 rs = docs[0]["params"]["r_list"]; by = {}41 for r in rs:42 cs = [d["measurements"]["by_r"][str(r)] for d in docs]43 by[str(r)] = {"max_bit_bias_by_seed": [round(c["max_bit_bias"], 4) for c in cs],44 "n_bits_bias_over_4sigma_by_seed": [c["n_bits_bias_over_4sigma"] for c in cs],45 "max_abs_corr_by_seed": [round(c["max_abs_corr"], 4) for c in cs],46 "n_pairs_corr_over_4sigma_by_seed": [c["n_pairs_corr_over_4sigma"] for c in cs],47 "chi2_bytes_rejected_by_seed": [c["chi2_n_bytes_rejected_bonferroni"] for c in cs],48 "chi2_min_p_by_seed": [c["chi2_min_p"] for c in cs]}49 ro = [d["measurements"]["random_oracle_control"] for d in docs]50 by["random_oracle"] = {"max_bit_bias_by_seed": [round(c["max_bit_bias"], 4) for c in ro],51 "n_pairs_corr_over_4sigma_by_seed": [c["n_pairs_corr_over_4sigma"] for c in ro],52 "chi2_bytes_rejected_by_seed": [c["chi2_n_bytes_rejected_bonferroni"] for c in ro]}53 first_clean = next((r for r in rs if all(by[str(r)]["n_bits_bias_over_4sigma_by_seed"][i] == 0 and by[str(r)]["chi2_bytes_rejected_by_seed"][i] == 0 for i in range(len(docs)))), None)54 first_corr_clean = next((r for r in rs if all(x <= 3 for x in by[str(r)]["n_pairs_corr_over_4sigma_by_seed"])), None)55 out["bias"] = {"n_per_seed": docs[0]["params"]["n"], "seeds": [d["seed"] for d in docs], "r_list": rs,56 "bias_threshold_4sigma": docs[0]["measurements"]["by_r"]["1"]["bias_threshold_4sigma"],57 "corr_threshold_4sigma": docs[0]["measurements"]["by_r"]["1"]["corr_threshold_4sigma"],58 "expected_pairs_under_null": docs[0]["measurements"]["by_r"]["1"]["expected_pairs_under_null"],59 "first_r_with_no_bit_bias_and_no_chi2_rejection": first_clean,60 "first_r_with_correlation_count_at_noise_level": first_corr_clean, "by_r": by}61 # ---- preimage62 d = load("preimage_sat_scaling.json")63 if d:64 S = d["measurements"]["summary"]65 largest = {}66 for key, c in S.items():67 if c["solved_fraction"] > 0:68 g = c["solver"] + ("" if c["placement"] == "first" else "_spread")69 best = largest.get(g)70 if best is None or (c["r"], c["k"]) > (best["r"], best["k"]):71 largest[g] = {"r": c["r"], "k": c["k"], "solved_fraction": c["solved_fraction"], "median_wall_s": c["median_wall_s"]}72 frontier = {}73 for sol in ("cadical", "kissat", "z3"):74 for pl in ("first", "spread"):75 rows = {}76 for r in d["params"]["r_list"]:77 ks = [c["k"] for c in S.values() if c["solver"] == sol and c["placement"] == pl and c["r"] == r and c["solved_fraction"] >= 0.5]78 rows[str(r)] = max(ks) if ks else None79 if any(v is not None for v in rows.values()):80 frontier[sol + ("" if pl == "first" else "_spread")] = rows81 out["preimage_sat"] = {"n_cells": d["n_cells"], "timeout_s": d["params"]["timeout_s"], "hosts": sorted({h for c in S.values() for h in c["hosts"]}),82 "largest_solved_cell_by_solver": largest, "max_k_solved_majority_by_r": frontier,83 "all_sat_answers_verified": all(c["all_verified"] in (True, None) for c in S.values()),84 "cells": S}85 # ---- collision86 d = load("collision_sat.json")87 if d:88 S = d["measurements"]["summary"]89 cells = d["measurements"]["cells"]90 largest = {}91 for c in S.values():92 g = f'{c["solver"]}:iv_{c["iv"]}:ff{int(c["feedforward"])}'93 if c["solved_fraction"] > 0 and (g not in largest or c["r"] > largest[g]["r"]):94 largest[g] = {"r": c["r"], "solved_fraction": c["solved_fraction"], "median_wall_s_solved": c["median_wall_s_solved"]}95 unsat = sorted({(c["cell"]["r"], c["cell"]["iv"], c["cell"]["feedforward"], c["cell"]["solver"]) for c in cells if c["status"] == "unsat"})96 examples = {}97 for c in cells:98 if c["status"] == "sat" and c.get("verified"):99 g = f'iv_{c["cell"]["iv"]}:ff{int(c["cell"]["feedforward"])}'100 if g not in examples or c["cell"]["r"] > examples[g]["r"]:101 examples[g] = {"r": c["cell"]["r"], "solver": c["cell"]["solver"], "message1_hex": c["message1_hex"],102 "message2_hex": c["message2_hex"], "iv_hex": c["iv_hex"], "output_hex": c["output_hex"],103 "differing_words": c["differing_words"]}104 out["collision_sat"] = {"n_cells": d["n_cells"], "timeout_s": d["params"]["timeout_s"], "hosts": sorted({h for c in S.values() for h in c["hosts"]}),105 "largest_solved_r_by_variant": largest,106 "proven_unsat_cells (r, iv, feedforward, solver)": unsat,107 "all_collisions_verified": all(c["all_verified"] in (True, None) for c in S.values()),108 "largest_verified_collision_examples": examples, "cells": S}109 # ---- local collision110 d = load("local_collision.json")111 if d:112 m = d["measurements"]113 emp = m["empirical"]; sat = m["sat"]114 out["local_collision"] = {115 "n_per_bit": d["params"]["n_per_bit"], "seed": d["seed"], "host": d["host"]["hostname"],116 "linear_model_all_32_single_bit_cancel": all(v["cancels_after_9_steps"] for v in m["linear_model"].values()),117 "pattern_formula": m["pattern_formula"],118 "pattern_bit31_hex": m["linear_model"]["31"]["pattern_hex"], "pattern_bit0_hex": m["linear_model"]["0"]["pattern_hex"],119 "empirical_collisions_total": sum(e["n_collisions"] for e in emp),120 "empirical_p_collision_by_bit": [e["p_collision"] for e in emp],121 "rule_of_three_upper_bound": 3 / d["params"]["n_per_bit"],122 "survival_after_step_i_by_bit": [e["survival_fraction_by_step"][0] for e in emp],123 "survival_after_step_i+1_by_bit": [e["survival_fraction_by_step"][1] for e in emp],124 "survival_after_step_i+2_by_bit": [e["survival_fraction_by_step"][2] for e in emp],125 "sat_timeout_s": d["params"]["sat_timeout_s"],126 "sat_found_verified_bits": [s["bit"] for s in sat if s.get("verified") is True],127 "sat_timeout_bits": [s["bit"] for s in sat if s["status"] != "sat"],128 "sat_wall_s_by_bit": {str(s["bit"]): s["wall_s"] for s in sat},129 "sat_conflicts_by_bit": {str(s["bit"]): s.get("conflicts") for s in sat},130 }131 d2 = load("local_collision_bits31_0_seed2.json")132 if d2:133 out["local_collision"]["second_run_bits31_0"] = {"seed": d2["seed"], "sat": [{k: s.get(k) for k in ("bit", "status", "wall_s", "conflicts", "verified")} for s in d2["measurements"]["sat"]],134 "empirical_collisions_total": sum(e["n_collisions"] for e in d2["measurements"]["empirical"])}135 provenance.record("sha256_summary", {"sources": sorted(p.name for p in RES.glob("*.json") if p.name != "summary.json")}, out,136 out=RES / "summary.json", started=t0)137 print(json.dumps({k: {kk: vv for kk, vv in v.items() if kk not in ("cells", "by_r", "by_config")} for k, v in out.items()}, indent=1, default=str)[:6000])138139140if __name__ == "__main__":141 main()142