1"""SHA-256 result tables and macros from results/reduced_round_sha256/summary.json."""2import json, pathlib3ROOT = pathlib.Path(__file__).resolve().parents[1]4S = json.loads((ROOT / "results/reduced_round_sha256/summary.json").read_text())["measurements"]5T = ROOT / "paper/tables"; M = {}678def wrap(rows):9 return "\\resizebox{\\textwidth}{!}{%\n" + "\n".join(rows) + "}\n"101112# diffusion13d = S["diffusion"]["by_config"]14M["shaDiffWzero"] = d["W0"]["full_diffusion_step"]; M["shaDiffWfive"] = d["W5"]["full_diffusion_step"]; M["shaDiffWfifteen"] = d["W15"]["full_diffusion_step"]; M["shaDiffIV"] = d["IV"]["full_diffusion_step"]15M["shaDiffN"] = S["diffusion"]["n_per_seed"]; M["shaDiffHamming"] = f"{d['W0']['hamming_mean_step64']:.1f}"; M["shaDiffHammingSd"] = f"{d['W0']['hamming_sd_step64']:.1f}"16M["shaDiffRO"] = f"{d['W0']['random_oracle_flip_ratio']:.3f}"17rows = [r"\begin{tabular}{@{}lrrrrrrrr@{}}", r"\toprule Difference in & step 1 & 2 & 3 & 4 & 5 & 6 & 8 & first step $\ge 0.49$ \\ \midrule"]18for k, lab in [("W0", "$W_0$ (one bit)"), ("W5", "$W_5$ (one bit)"), ("W15", "$W_{15}$ (one bit)"), ("IV", "IV register (one bit)")]:19 v = d[k]["mean_flip_ratio_by_step"]; off = {"W0": 0, "W5": 5, "W15": 15, "IV": 0}[k]20 cells = [f"{v[off + i - 1]:.3f}" if off + i - 1 < len(v) else "" for i in (1, 2, 3, 4, 5, 6, 8)]21 rows.append(f"{lab} & " + " & ".join(cells) + f" & {d[k]['full_diffusion_step']} \\\\")22rows += [r"\midrule", f"random-oracle control & \\multicolumn{{7}}{{l}}{{{d['W0']['random_oracle_flip_ratio']:.3f} $\\pm$ {d['W0']['random_oracle_flip_sd']:.3f} at every step}} & 1 \\\\", r"\bottomrule", r"\end{tabular}"]23(T / "sha_diffusion.tex").write_text(wrap(rows))24# bias25b = S["bias"]; M["shaBiasN"] = b["n_per_seed"]; M["shaBiasFirstClean"] = b["first_r_with_correlation_count_at_noise_level"]; M["shaBiasFirstNoBias"] = b["first_r_with_no_bit_bias_and_no_chi2_rejection"]26M["shaBiasExpectedPairs"] = f"{b['expected_pairs_under_null']:.1f}"27rows = [r"\begin{tabular}{@{}rrrrr@{}}", r"\toprule Steps $r$ & biased output bits ($>4\sigma$) & max $|$corr$|$ & (input, output) pairs $>4\sigma$ & bytes failing $\chi^2$ \\ \midrule"]28for r in b["r_list"]:29 v = b["by_r"][str(r)]30 rng_ = lambda xs: (f"{min(xs)}" if min(xs) == max(xs) else f"{min(xs)}--{max(xs)}")31 rows.append(f"{r} & {rng_(v['n_bits_bias_over_4sigma_by_seed'])} & {max(v['max_abs_corr_by_seed']):.3f} & {rng_(v['n_pairs_corr_over_4sigma_by_seed'])} & {rng_(v['chi2_bytes_rejected_by_seed'])} \\\\")32if "random_oracle" in b:33 v = b["random_oracle"]; rows.append(f"random oracle & {v.get('n_bits_bias_over_4sigma', '0')} & {v.get('max_abs_corr', 0):.3f} & {v.get('n_pairs_corr_over_4sigma', '')} & {v.get('chi2_bytes_rejected', '')} \\\\")34rows += [r"\bottomrule", r"\end{tabular}"]35(T / "sha_bias.tex").write_text(wrap(rows))36# preimage37p = S["preimage_sat"]; cells = p["cells"]; M["shaPreCells"] = p["n_cells"]; M["shaPreVerified"] = "all" if p["all_sat_answers_verified"] else "NOT ALL"38rs = [4, 8, 12, 16, 20, 24, 28, 32, 40, 48, 64]; ks = [16, 24, 32, 40, 48, 56, 64]39def cell(solver, r, k):40 c = cells.get(f"{solver}:r{r}:k{k}")41 if not c: return "---"42 if c["n_sat"] == 0: return f"T({c['n_runs']})"43 t = c["median_wall_s_solved"]; f = f"{t:.2f}" if t < 10 else f"{t:.0f}"44 return f"{f}" + ("" if c["n_sat"] == c["n_runs"] else f" ({c['n_sat']}/{c['n_runs']})")45for solver, name in [("cadical", "sha_preimage_cadical"), ("kissat", "sha_preimage_kissat"), ("cadical_spread", "sha_preimage_spread"), ("z3", "sha_preimage_z3")]:46 rows = [r"\begin{tabular}{@{}r" + "r" * len(ks) + "@{}}", r"\toprule Steps $r$ & " + " & ".join(f"$k={k}$" for k in ks) + r" \\ \midrule"]47 for r in rs:48 rows.append(f"{r} & " + " & ".join(cell(solver, r, k) for k in ks) + r" \\")49 rows += [r"\bottomrule", r"\end{tabular}"]50 (T / f"{name}.tex").write_text(wrap(rows))51M["shaPreLargestCadical"] = f"r={p['largest_solved_cell_by_solver']['cadical']['r']}, k={p['largest_solved_cell_by_solver']['cadical']['k']}"52M["shaPreZthreeLargest"] = f"r={p['largest_solved_cell_by_solver']['z3']['r']}, k={p['largest_solved_cell_by_solver']['z3']['k']}"53c64 = cells.get("cadical:r64:k16", {}); M["shaPreRsixtyfourTime"] = f"{c64.get('median_wall_s_solved', 0):.0f}"; M["shaPreRsixtyfourSolved"] = f"{c64.get('n_sat', 0)}/{c64.get('n_runs', 0)}"54c20 = cells.get("cadical:r20:k16", {}); M["shaPreRtwentyTime"] = f"{c20.get('median_wall_s_solved', 0):.1f}"55c16 = cells.get("cadical:r16:k64", {}); M["shaPreRsixteenConf"] = str(c16.get("median_conflicts_solved", "")); M["shaPreRsixteenTime"] = f"{c16.get('median_wall_s_solved', 0):.2f}"56M["shaPreVars"] = f"{cells['cadical:r64:k16']['n_vars']:,}".replace(",", "\\,"); M["shaPreClauses"] = f"{cells['cadical:r64:k16']['n_clauses']:,}".replace(",", "\\,")57# collision58c = S["collision_sat"]; M["shaColCells"] = c["n_cells"]; M["shaColVerified"] = "all" if c["all_collisions_verified"] else "NOT ALL"59M["shaColUnsatCells"] = len(c["proven_unsat_cells (r, iv, feedforward, solver)"])60lv = c["largest_solved_r_by_variant"]; M["shaColLargestR"] = max(v["r"] for v in lv.values())61M["shaColFixedTime"] = f"{lv['cadical:iv_fixed:ff0']['median_wall_s_solved']:.0f}"; M["shaColFreeTime"] = f"{lv['cadical:iv_free:ff0']['median_wall_s_solved']:.1f}"62cc = c.get("cells", {})63if cc:64 rrs = sorted({v["r"] for v in cc.values()})65 variants = [("cadical:iv_fixed:ff0", "CaDiCaL, std IV"), ("kissat:iv_fixed:ff0", "Kissat, std IV"), ("cadical:iv_fixed:ff1", "CaDiCaL, std IV + feed-forward"), ("cadical:iv_free:ff0", "CaDiCaL, semi-free-start"), ("kissat:iv_free:ff0", "Kissat, semi-free-start")]66 rows = [r"\begin{tabular}{@{}r" + "r" * len(variants) + "@{}}", r"\toprule Steps $r$ & " + " & ".join(v[1] for v in variants) + r" \\ \midrule"]67 def ccell(key, r):68 for k, v in cc.items():69 if k.startswith(key) and v["r"] == r:70 if v.get("n_unsat", 0) == v["n_runs"]: return f"UNSAT ({v['median_wall_s']:.1f})"71 if v["n_sat"] == 0: return f"T({v['n_runs']})"72 t = v["median_wall_s_solved"]; f = f"{t:.2f}" if t < 10 else f"{t:.0f}"73 return f + ("" if v["n_sat"] == v["n_runs"] else f" ({v['n_sat']}/{v['n_runs']})")74 return "---"75 for r in rrs:76 rows.append(f"{r} & " + " & ".join(ccell(v[0], r) for v in variants) + r" \\")77 rows += [r"\bottomrule", r"\end{tabular}"]78 (T / "sha_collision.tex").write_text(wrap(rows))79else:80 print("collision cells key missing:", list(c.keys()))81# local collision82l = S["local_collision"]; M["shaLcN"] = f"{l['n_per_bit']:,}".replace(",", "\\,"); M["shaLcBound"] = f"{l['rule_of_three_upper_bound']:.0e}".replace("e-05", r"\times 10^{-5}")83M["shaLcSurvivalMsb"] = f"{l['survival_after_step_i_by_bit'][31]:.2f}"; M["shaLcSurvivalOther"] = f"{sum(l['survival_after_step_i_by_bit'][:31])/31:.3f}"84M["shaLcSatMin"] = f"{min(l['sat_wall_s_by_bit'].values()):.1f}"; M["shaLcSatMax"] = f"{max(l['sat_wall_s_by_bit'].values()):.0f}"; M["shaLcSatBits"] = len(l["sat_found_verified_bits"])85M["shaLcPattern"] = l["pattern_formula"].replace("^", r"$\oplus$").replace("S0", r"$\Sigma_0$").replace("S1", r"$\Sigma_1$").replace("d", r"$\delta$")86(T / "numbers_sha.tex").write_text("% generated by scripts/make_sha_tables.py\n" + "\n".join(f"\\newcommand{{\\{k}}}{{{v}}}" for k, v in M.items()) + "\n")87print(len(M), "macros")88