"""SHA-256 result tables and macros from results/reduced_round_sha256/summary.json."""
import json, pathlib
ROOT = pathlib.Path(__file__).resolve().parents[1]
S = json.loads((ROOT / "results/reduced_round_sha256/summary.json").read_text())["measurements"]
T = ROOT / "paper/tables"; M = {}


def wrap(rows):
    return "\\resizebox{\\textwidth}{!}{%\n" + "\n".join(rows) + "}\n"


# diffusion
d = S["diffusion"]["by_config"]
M["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"]
M["shaDiffN"] = S["diffusion"]["n_per_seed"]; M["shaDiffHamming"] = f"{d['W0']['hamming_mean_step64']:.1f}"; M["shaDiffHammingSd"] = f"{d['W0']['hamming_sd_step64']:.1f}"
M["shaDiffRO"] = f"{d['W0']['random_oracle_flip_ratio']:.3f}"
rows = [r"\begin{tabular}{@{}lrrrrrrrr@{}}", r"\toprule Difference in & step 1 & 2 & 3 & 4 & 5 & 6 & 8 & first step $\ge 0.49$ \\ \midrule"]
for k, lab in [("W0", "$W_0$ (one bit)"), ("W5", "$W_5$ (one bit)"), ("W15", "$W_{15}$ (one bit)"), ("IV", "IV register (one bit)")]:
    v = d[k]["mean_flip_ratio_by_step"]; off = {"W0": 0, "W5": 5, "W15": 15, "IV": 0}[k]
    cells = [f"{v[off + i - 1]:.3f}" if off + i - 1 < len(v) else "" for i in (1, 2, 3, 4, 5, 6, 8)]
    rows.append(f"{lab} & " + " & ".join(cells) + f" & {d[k]['full_diffusion_step']} \\\\")
rows += [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}"]
(T / "sha_diffusion.tex").write_text(wrap(rows))
# bias
b = 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"]
M["shaBiasExpectedPairs"] = f"{b['expected_pairs_under_null']:.1f}"
rows = [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"]
for r in b["r_list"]:
    v = b["by_r"][str(r)]
    rng_ = lambda xs: (f"{min(xs)}" if min(xs) == max(xs) else f"{min(xs)}--{max(xs)}")
    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'])} \\\\")
if "random_oracle" in b:
    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', '')} \\\\")
rows += [r"\bottomrule", r"\end{tabular}"]
(T / "sha_bias.tex").write_text(wrap(rows))
# preimage
p = S["preimage_sat"]; cells = p["cells"]; M["shaPreCells"] = p["n_cells"]; M["shaPreVerified"] = "all" if p["all_sat_answers_verified"] else "NOT ALL"
rs = [4, 8, 12, 16, 20, 24, 28, 32, 40, 48, 64]; ks = [16, 24, 32, 40, 48, 56, 64]
def cell(solver, r, k):
    c = cells.get(f"{solver}:r{r}:k{k}")
    if not c: return "---"
    if c["n_sat"] == 0: return f"T({c['n_runs']})"
    t = c["median_wall_s_solved"]; f = f"{t:.2f}" if t < 10 else f"{t:.0f}"
    return f"{f}" + ("" if c["n_sat"] == c["n_runs"] else f" ({c['n_sat']}/{c['n_runs']})")
for solver, name in [("cadical", "sha_preimage_cadical"), ("kissat", "sha_preimage_kissat"), ("cadical_spread", "sha_preimage_spread"), ("z3", "sha_preimage_z3")]:
    rows = [r"\begin{tabular}{@{}r" + "r" * len(ks) + "@{}}", r"\toprule Steps $r$ & " + " & ".join(f"$k={k}$" for k in ks) + r" \\ \midrule"]
    for r in rs:
        rows.append(f"{r} & " + " & ".join(cell(solver, r, k) for k in ks) + r" \\")
    rows += [r"\bottomrule", r"\end{tabular}"]
    (T / f"{name}.tex").write_text(wrap(rows))
M["shaPreLargestCadical"] = f"r={p['largest_solved_cell_by_solver']['cadical']['r']}, k={p['largest_solved_cell_by_solver']['cadical']['k']}"
M["shaPreZthreeLargest"] = f"r={p['largest_solved_cell_by_solver']['z3']['r']}, k={p['largest_solved_cell_by_solver']['z3']['k']}"
c64 = 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)}"
c20 = cells.get("cadical:r20:k16", {}); M["shaPreRtwentyTime"] = f"{c20.get('median_wall_s_solved', 0):.1f}"
c16 = cells.get("cadical:r16:k64", {}); M["shaPreRsixteenConf"] = str(c16.get("median_conflicts_solved", "")); M["shaPreRsixteenTime"] = f"{c16.get('median_wall_s_solved', 0):.2f}"
M["shaPreVars"] = f"{cells['cadical:r64:k16']['n_vars']:,}".replace(",", "\\,"); M["shaPreClauses"] = f"{cells['cadical:r64:k16']['n_clauses']:,}".replace(",", "\\,")
# collision
c = S["collision_sat"]; M["shaColCells"] = c["n_cells"]; M["shaColVerified"] = "all" if c["all_collisions_verified"] else "NOT ALL"
M["shaColUnsatCells"] = len(c["proven_unsat_cells (r, iv, feedforward, solver)"])
lv = c["largest_solved_r_by_variant"]; M["shaColLargestR"] = max(v["r"] for v in lv.values())
M["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}"
cc = c.get("cells", {})
if cc:
    rrs = sorted({v["r"] for v in cc.values()})
    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")]
    rows = [r"\begin{tabular}{@{}r" + "r" * len(variants) + "@{}}", r"\toprule Steps $r$ & " + " & ".join(v[1] for v in variants) + r" \\ \midrule"]
    def ccell(key, r):
        for k, v in cc.items():
            if k.startswith(key) and v["r"] == r:
                if v.get("n_unsat", 0) == v["n_runs"]: return f"UNSAT ({v['median_wall_s']:.1f})"
                if v["n_sat"] == 0: return f"T({v['n_runs']})"
                t = v["median_wall_s_solved"]; f = f"{t:.2f}" if t < 10 else f"{t:.0f}"
                return f + ("" if v["n_sat"] == v["n_runs"] else f" ({v['n_sat']}/{v['n_runs']})")
        return "---"
    for r in rrs:
        rows.append(f"{r} & " + " & ".join(ccell(v[0], r) for v in variants) + r" \\")
    rows += [r"\bottomrule", r"\end{tabular}"]
    (T / "sha_collision.tex").write_text(wrap(rows))
else:
    print("collision cells key missing:", list(c.keys()))
# local collision
l = 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}")
M["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}"
M["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"])
M["shaLcPattern"] = l["pattern_formula"].replace("^", r"$\oplus$").replace("S0", r"$\Sigma_0$").replace("S1", r"$\Sigma_1$").replace("d", r"$\delta$")
(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")
print(len(M), "macros")