1"""Regenerate the SHA-256 (Axis C) figures from results/reduced_round_sha256/*.json.23 .venv/bin/python figures/make_sha256_figures.py # all figures4Figures: sha256_diffusion.pdf, sha256_bias.pdf, sha256_sat_scaling.pdf, sha256_collision_scaling.pdf,5sha256_local_collision.pdf (vector PDF, serif fonts).6"""7from __future__ import annotations8import glob, json, pathlib, sys9import numpy as np10import matplotlib11matplotlib.use("Agg")12import matplotlib.pyplot as plt1314ROOT = pathlib.Path(__file__).resolve().parents[1]15RES = ROOT / "results" / "reduced_round_sha256"16FIG = ROOT / "figures"17plt.rcParams.update({"font.family": "serif", "font.serif": ["Times New Roman", "Times", "DejaVu Serif"],18 "mathtext.fontset": "stix", "font.size": 9, "axes.labelsize": 9, "legend.fontsize": 7.5,19 "xtick.labelsize": 8, "ytick.labelsize": 8, "pdf.fonttype": 42, "axes.spines.top": False,20 "axes.spines.right": False, "figure.dpi": 150})21C = {"W0": "#1b4f72", "W5": "#b03a2e", "W15": "#239b56", "IV": "#7d3c98", "RO": "#7f8c8d",22 "cadical": "#1b4f72", "kissat": "#b03a2e", "z3": "#239b56"}232425def load(name):26 p = RES / name27 return json.loads(p.read_text()) if p.exists() else None282930def fig_diffusion():31 docs = [json.loads(p.read_text()) for p in sorted(RES.glob("diffusion_seed*.json"))]32 if not docs:33 return34 fig, (ax1, ax2) = plt.subplots(1, 2, figsize=(7.2, 2.9), gridspec_kw={"width_ratios": [1.35, 1]})35 M = np.mean([np.array(d["measurements"]["W0"]["mean_flip_matrix"]) for d in docs], axis=0)36 im = ax1.imshow(M[:32].T, aspect="auto", cmap="viridis", vmin=0, vmax=1, origin="lower",37 extent=[0.5, 32.5, -0.5, 255.5], interpolation="nearest")38 ax1.set_xlabel("step $t$"); ax1.set_ylabel("output bit (0 = MSB of $a$, 255 = LSB of $h$)")39 ax1.set_yticks([0, 32, 64, 96, 128, 160, 192, 224, 255])40 for y in range(32, 256, 32):41 ax1.axhline(y - 0.5, color="w", lw=0.3, alpha=0.6)42 ax1.set_title(r"(a) $\Pr[\mathrm{bit\ flips}]$, one-bit difference in $W_0$", fontsize=9)43 cb = fig.colorbar(im, ax=ax1, fraction=0.04, pad=0.02); cb.set_label("flip probability")44 steps = np.arange(1, 65)45 for cfg in ["W0", "W5", "W15", "IV"]:46 R = np.array([d["measurements"][cfg]["mean_flip_ratio_by_step"] for d in docs])47 ax2.plot(steps, R.mean(axis=0), color=C[cfg], lw=1.2,48 label={"W0": "$W_0$ bit", "W5": "$W_5$ bit", "W15": "$W_{15}$ bit", "IV": "IV bit"}[cfg])49 ro = np.mean([d["measurements"]["W0"]["random_oracle_control"]["flip_ratio_mean"] for d in docs])50 rosd = np.mean([d["measurements"]["W0"]["random_oracle_control"]["flip_ratio_sd"] for d in docs])51 ax2.axhline(ro, color=C["RO"], ls="--", lw=1, label="random oracle (%.3f)" % ro)52 ax2.axhspan(ro - 2 * rosd, ro + 2 * rosd, color=C["RO"], alpha=0.12, lw=0)53 ax2.axhline(0.49, color="k", ls=":", lw=0.7)54 ax2.set_xlim(0, 40); ax2.set_ylim(0, 0.56); ax2.set_xlabel("step $t$"); ax2.set_ylabel("mean flip ratio")55 ax2.set_title("(b) avalanche by step (N = %d x %d seeds)" % (docs[0]["params"]["n"], len(docs)), fontsize=9)56 ax2.legend(loc="lower right", frameon=False)57 fig.tight_layout(); fig.savefig(FIG / "sha256_diffusion.pdf"); plt.close(fig)585960def fig_bias():61 docs = [json.loads(p.read_text()) for p in sorted(RES.glob("bias_seed*.json"))]62 if not docs:63 return64 rs = docs[0]["params"]["r_list"]; n = docs[0]["params"]["n"]65 fig, axs = plt.subplots(1, 3, figsize=(7.2, 2.5))66 mk = ["o", "s", "^"]67 for i, d in enumerate(docs):68 by = d["measurements"]["by_r"]; ro = d["measurements"]["random_oracle_control"]69 axs[0].plot(rs, [by[str(r)]["max_bit_bias"] for r in rs], mk[i % 3], ms=3.5, color=C["W0"], alpha=0.8,70 label="seed %d" % d["seed"] if i == 0 or True else None)71 axs[0].axhline(ro["max_bit_bias"], color=C["RO"], ls="--", lw=0.8)72 axs[1].plot(rs, [by[str(r)]["n_pairs_corr_over_4sigma"] for r in rs], mk[i % 3], ms=3.5, color=C["W5"], alpha=0.8)73 axs[1].axhline(ro["n_pairs_corr_over_4sigma"], color=C["RO"], ls="--", lw=0.8)74 axs[2].plot(rs, [max(by[str(r)]["chi2_min_p"], 1e-12) for r in rs], mk[i % 3], ms=3.5, color=C["W15"], alpha=0.8)75 axs[2].axhline(ro["chi2_min_p"], color=C["RO"], ls="--", lw=0.8)76 thr = 4 * 0.5 / n ** 0.577 axs[0].axhline(thr, color="k", ls=":", lw=0.8); axs[0].text(30, thr * 1.15, r"$4\sigma$", fontsize=7)78 axs[0].set_yscale("log"); axs[0].set_ylabel(r"$\max_j |\Pr[y_j=1]-\frac{1}{2}|$"); axs[0].set_title("(a) output-bit bias", fontsize=9)79 exp = docs[0]["measurements"]["by_r"][str(rs[0])]["expected_pairs_under_null"]80 axs[1].axhline(exp, color="k", ls=":", lw=0.8); axs[1].text(30, exp * 1.3, "null exp.", fontsize=7)81 axs[1].set_yscale("symlog", linthresh=1); axs[1].set_ylabel(r"# pairs with $|c_{ij}|>4/\sqrt{N}$")82 axs[1].set_title("(b) input/output linear correlations", fontsize=9)83 axs[2].set_yscale("log"); axs[2].set_ylim(3e-13, 1.5); axs[2].text(1.1, 2e-12, r"$p<10^{-12}$ (clipped)", fontsize=6); axs[2].axhline(0.01 / 32, color="k", ls=":", lw=0.8)84 axs[2].set_ylabel(r"min $p$ over 32 output bytes ($\chi^2$)"); axs[2].set_title("(c) byte uniformity", fontsize=9)85 for ax in axs:86 ax.set_xscale("log", base=2); ax.set_xlabel("steps $r$"); ax.set_xticks([1, 2, 4, 8, 16, 32, 64]); ax.set_xticklabels([1, 2, 4, 8, 16, 32, 64])87 axs[0].plot([], [], "--", color=C["RO"], label="random oracle"); axs[0].legend(frameon=False, loc="upper right")88 fig.suptitle("Statistical regularity of $r$-step SHA-256 (N = %d messages per seed, 3 seeds)" % n, fontsize=9, y=1.0)89 fig.tight_layout(); fig.savefig(FIG / "sha256_bias.pdf", bbox_inches="tight"); plt.close(fig)909192def _censored_plot(ax, xs, meds, solved_frac, timeout, color, marker, ls, label):93 xs = np.array(xs); meds = np.array(meds, dtype=float); sf = np.array(solved_frac)94 full = sf >= 0.595 ax.plot(xs[full], meds[full], marker=marker, ls=ls, color=color, ms=4, lw=1, label=label, mfc=color)96 if (~full).any():97 ax.plot(xs[~full], np.full((~full).sum(), timeout * 1.25), marker=marker, ls="none", color=color, ms=4, mfc="white")9899100def fig_sat_scaling():101 d = load("preimage_sat_scaling.json")102 if not d:103 return104 S = d["measurements"]["summary"]; T = d["params"]["timeout_s"]105 ks = d["params"]["k_list"]; rs = d["params"]["r_list"]106 cmap = plt.get_cmap("viridis")107 fig, axs = plt.subplots(1, 3, figsize=(7.2, 2.7), sharey=True)108 panels = [("first", "cadical", "(a) CaDiCaL, free bits in $W_0,W_1$"), ("first", "kissat", "(b) Kissat, free bits in $W_0,W_1$"),109 ("spread", "cadical", "(c) CaDiCaL, free bits spread over 16 words")]110 for ax, (pl, sol, title) in zip(axs, panels):111 for i, k in enumerate(ks):112 cells = [(r, S.get(f"{sol}:r{r}:k{k}" + ("" if pl == "first" else ":spread"))) for r in rs]113 cells = [(r, c) for r, c in cells if c]114 if not cells:115 continue116 _censored_plot(ax, [r for r, _ in cells], [max(c["median_wall_s"], 1e-3) for _, c in cells],117 [c["solved_fraction"] for _, c in cells], T, cmap(i / (len(ks) - 1)), "o" if sol == "cadical" else "^",118 "-" if sol == "cadical" else "--", "$k$ = %d" % k)119 if pl == "first" and sol == "cadical":120 for i, k in enumerate([16, 24, 32]):121 cells = [(r, S.get(f"z3:r{r}:k{k}")) for r in rs]; cells = [(r, c) for r, c in cells if c]122 if cells:123 _censored_plot(ax, [r for r, _ in cells], [max(c["median_wall_s"], 1e-3) for _, c in cells],124 [c["solved_fraction"] for _, c in cells], T, cmap(i / (len(ks) - 1)), "x", ":", "z3 $k$ = %d" % k if i == 0 else None)125 ax.axhline(T, color="k", ls=":", lw=0.7); ax.text(rs[0], T * 1.6, "timeout (open = median unsolved)", fontsize=6.5)126 ax.set_yscale("log"); ax.set_xlabel("steps $r$"); ax.set_title(title, fontsize=8.5); ax.set_xticks(rs); ax.tick_params(axis="x", labelsize=6.5)127 axs[0].set_ylabel("median wall time (s)"); axs[0].set_ylim(1e-3, T * 3)128 axs[0].legend(frameon=False, ncol=2, loc="lower right", fontsize=6)129 fig.suptitle("Preimage of $r$-step SHA-256 compression with $k$ free message bits (3 seeds per cell, timeout %d s)" % T, fontsize=9, y=1.0)130 fig.tight_layout(); fig.savefig(FIG / "sha256_sat_scaling.pdf", bbox_inches="tight"); plt.close(fig)131132133def fig_collision_scaling():134 d = load("collision_sat.json")135 if not d:136 return137 S = d["measurements"]["summary"]; T = d["params"]["timeout_s"]; rs = d["params"]["r_list"]138 fig, axs = plt.subplots(1, 2, figsize=(7.2, 2.7), sharey=True)139 for ax, sol in zip(axs, ["cadical", "kissat"]):140 for (iv, ff), color, mk in [(("fixed", False), C["cadical"], "o"), (("fixed", True), C["cadical"], "s"),141 (("free", False), C["kissat"], "o"), (("free", True), C["kissat"], "s")]:142 cells = [(r, S.get(f"{sol}:iv_{iv}:ff{int(ff)}:r{r}")) for r in rs]; cells = [(r, c) for r, c in cells if c]143 if not cells:144 continue145 _censored_plot(ax, [r for r, _ in cells], [max(c["median_wall_s"], 1e-3) for _, c in cells],146 [c["solved_fraction"] for _, c in cells], T, color, mk, "-" if not ff else "--",147 ("standard IV" if iv == "fixed" else "semi-free-start") + (", feed-forward" if ff else ""))148 for r, c in cells: # mark proven UNSAT cells149 if c.get("n_unsat", 0) > 0 or c.get("all_unsat"):150 ax.annotate("UNSAT", (r, max(c["median_wall_s"], 1e-3)), fontsize=5.5, textcoords="offset points", xytext=(0, 4), ha="center")151 ax.axhline(T, color="k", ls=":", lw=0.7); ax.set_yscale("log"); ax.set_xlabel("steps $r$"); ax.set_xticks(rs)152 ax.set_title({"cadical": "(a) CaDiCaL", "kissat": "(b) Kissat"}[sol], fontsize=9)153 axs[0].set_ylabel("median wall time (s)"); axs[0].set_ylim(1e-3, T * 3); axs[0].legend(frameon=False, fontsize=6.5, loc="lower right")154 fig.suptitle("Collision search on $r$-step SHA-256 compression (timeout %d s; open markers = majority unsolved)" % T, fontsize=9, y=1.0)155 fig.tight_layout(); fig.savefig(FIG / "sha256_collision_scaling.pdf", bbox_inches="tight"); plt.close(fig)156157158def fig_local_collision():159 d = load("local_collision.json")160 if not d:161 return162 emp = d["measurements"]["empirical"]; sat = d["measurements"]["sat"]; n = d["params"]["n_per_bit"]163 bits = [e["bit"] for e in emp]164 fig, (ax1, ax2) = plt.subplots(1, 2, figsize=(7.2, 2.6))165 s1 = [e["survival_fraction_by_step"][0] for e in emp]; s2 = [max(e["survival_fraction_by_step"][1], 0.5 / n) for e in emp]166 ax1.plot(bits, s1, "o-", ms=3, color=C["W0"], label="after step $i$ (difference $(\\delta,\\delta)$ in $a,e$)")167 ax1.plot(bits, s2, "s-", ms=3, color=C["W5"], label="after step $i+1$")168 pc = [e["p_collision"] for e in emp]169 ax1.plot(bits, [max(p, 0.5 / n) for p in pc], "^", ms=3.5, color=C["W15"], label="9-step collision (0 observed $\\Rightarrow$ shown at $1/(2N)$)")170 ax1.axhline(3 / n, color=C["RO"], ls="--", lw=0.8, label="rule-of-three 95% upper bound $3/N$")171 ax1.set_yscale("log"); ax1.set_xlabel("bit position of $\\delta$ in $W_i$"); ax1.set_ylabel("fraction of %d samples" % n)172 ax1.set_title("(a) conformance of the XOR pattern, real step", fontsize=9); ax1.legend(frameon=False, fontsize=6, loc="center", bbox_to_anchor=(0.5, 0.55))173 ax1.set_ylim(1e-6, 2)174 sb = [s["bit"] for s in sat]; st = [max(s["wall_s"], 1e-3) for s in sat]; ok = [s.get("verified") is True for s in sat]175 ax2.bar([b for b, o in zip(sb, ok) if o], [t for t, o in zip(st, ok) if o], color=C["W0"], width=0.8, label="conforming pair found (verified)")176 bad = [b for b, o in zip(sb, ok) if not o]177 if bad:178 ax2.bar(bad, [d["params"]["sat_timeout_s"]] * len(bad), color="white", edgecolor=C["W5"], width=0.8, label="timeout")179 ax2.set_yscale("log"); ax2.set_xlabel("bit position of $\\delta$"); ax2.set_ylabel("CaDiCaL wall time (s)")180 ax2.set_title("(b) SAT search for a conforming (state, $W_i..W_{i+8}$)", fontsize=9); ax2.legend(frameon=False, fontsize=6.5)181 fig.tight_layout(); fig.savefig(FIG / "sha256_local_collision.pdf", bbox_inches="tight"); plt.close(fig)182183184if __name__ == "__main__":185 for f in (fig_diffusion, fig_bias, fig_sat_scaling, fig_collision_scaling, fig_local_collision):186 try:187 f(); print("ok", f.__name__)188 except Exception as e: # keep going so a missing result does not block the others189 print("FAILED", f.__name__, repr(e))190