1"""3a. SAT/SMT preimage scaling on r-step SHA-256 compression (standard IV, no feed-forward), question C2.23Cell = (r, k, seed, solver). A seeded random 512-bit message M* is drawn; target = compress(H0, M*, r, ff=False),4so a preimage exists. The k *free* bits are the first k message bits in (word, LSB-first) order: W_0 bits 0..31,5then W_1, ... ; all other message bits are fixed to M* by unit clauses. Solvers: CaDiCaL 1.9.5 (pysat Cadical195),6Kissat 4.0.4 (subprocess, --time), and z3 (bit-vector theory) on r <= 16, k <= 32. Every SAT answer is verified7by recomputing the hash with wp34.sha256.compress.89Modes:10 --list-cells print one JSON cell spec per line (used by cluster_driver.py)11 --cell '<json>' --out f run one cell in this process (fresh process => peak RSS is per cell)12 --aggregate DIR --out f gather per-cell JSONs into the experiment result with provenance13"""14from __future__ import annotations15import argparse, json, os, pathlib, random, sys, time16from common import S, provenance, peak_rss_mb, MASK, mean_sd17import cnf_sha256 as C18import solvers as SV1920R_LIST = [4, 8, 12, 16, 20, 24, 28, 32, 40, 48, 64]21K_LIST = [16, 24, 32, 40, 48, 56, 64]22TIMEOUT = 300.0232425def free_positions(k: int, placement: str):26 """'first': the first k message bits (W_0 LSB-first, then W_1, ...).27 'spread': k bits spread evenly over the 16 words (bit i -> word i mod 16, position i // 16), so that no single28 word carries all the freedom (for r <= 16 a single free word makes the instance invertible step by step)."""29 if placement == "first":30 return [(i // 32, i % 32) for i in range(k)]31 if placement == "spread":32 return [(i % 16, i // 16) for i in range(k)]33 raise ValueError(placement)343536def instance(r: int, k: int, seed: int, placement: str = "first"):37 rng = random.Random(1_000_003 * seed + 1_000 * r + k)38 block = bytes(rng.getrandbits(8) for _ in range(64))39 words = S.bytes_to_words(block)40 target = S.compress(S.H0, block, r, feedforward=False)41 return block, words, target, free_positions(k, placement)424344def list_cells(seeds, solvers, placements=("first", "spread")):45 cells = []46 for placement in placements:47 for r in R_LIST:48 for k in K_LIST:49 for seed in seeds:50 for sol in solvers:51 if sol == "z3" and not (r <= 16 and k <= 32):52 continue53 if placement == "spread" and sol != "cadical":54 continue55 cells.append({"r": r, "k": k, "seed": seed, "solver": sol, "placement": placement})56 return cells575859def run_cell(cell: dict, timeout: float) -> dict:60 r, k, seed, sol = cell["r"], cell["k"], cell["seed"], cell["solver"]61 placement = cell.setdefault("placement", "first")62 block, words, target, free = instance(r, k, seed, placement)63 freeset = set(free)64 t0 = time.time()65 res = {"cell": cell, "timeout_s": timeout, "target_hex": "".join("%08x" % v for v in target),66 "fixed_message_hex": block.hex(), "free_bits": "%d bits, placement=%s" % (k, placement)}67 if sol in ("cadical", "kissat"):68 cnf, W, IV, OUT = C.build_compression(r, feedforward=False)69 for j, w in enumerate(W):70 for i in range(32):71 if (j, i) not in freeset:72 cnf.assert_eq(w[i], bool((words[j] >> i) & 1))73 for o, v in zip(OUT, target):74 cnf.fix_word(o, v)75 res.update(cnf.stats())76 res["encode_s"] = round(time.time() - t0, 3)77 if sol == "cadical":78 out = SV.run_cadical(cnf.clauses, timeout, n_vars=cnf.nv, seed=seed)79 else:80 out = SV.run_kissat(cnf.clauses, cnf.nv, timeout, seed=seed)81 model = out.pop("model", None)82 res.update(out)83 if out["status"] == "sat":84 found = [C.decode_word(model, w) for w in W]85 res["preimage_hex"] = "".join("%08x" % v for v in found)86 res["verified"] = S.compress(S.H0, S.words_to_bytes(found), r, feedforward=False) == target87 elif sol == "z3":88 def build(z3, s):89 Wv = [z3.BitVec("W%d" % j, 32) for j in range(16)]90 for j in range(16):91 for i in range(32):92 if (j, i) not in freeset:93 s.add(z3.Extract(i, i, Wv[j]) == z3.BitVecVal((words[j] >> i) & 1, 1))94 OUT = SV.z3_compress(z3, list(S.H0), Wv, r, False)95 for o, v in zip(OUT, target):96 s.add(o == z3.BitVecVal(v, 32))97 return {"W%d" % j: Wv[j] for j in range(16)}98 res["encode_s"] = None99 out = SV.run_z3(build, timeout, seed=seed)100 model = out.pop("model", None)101 res.update(out)102 if out["status"] == "sat":103 found = [model["W%d" % j] for j in range(16)]104 res["preimage_hex"] = "".join("%08x" % v for v in found)105 res["verified"] = S.compress(S.H0, S.words_to_bytes(found), r, feedforward=False) == target106 res["total_wall_s"] = round(time.time() - t0, 3)107 res["peak_rss_mb"] = max(peak_rss_mb(), peak_rss_mb(children=True))108 res["hostname"] = provenance.host_info()["hostname"]109 return res110111112def aggregate(d: str, out: str, started: float):113 cells = []114 for p in sorted(pathlib.Path(d).glob("*.json")):115 doc = json.loads(p.read_text())116 if isinstance(doc, dict) and "cell" in doc: # skip the driver's skipped_cells.json117 cells.append(doc)118 summary = {}119 for placement in ("first", "spread"):120 for sol in ("cadical", "kissat", "z3"):121 for r in R_LIST:122 for k in K_LIST:123 cs = [c for c in cells if c["cell"]["solver"] == sol and c["cell"]["r"] == r and c["cell"]["k"] == k124 and c["cell"].get("placement", "first") == placement]125 if not cs:126 continue127 times = sorted(c["wall_s"] for c in cs)128 solved = [c for c in cs if c["status"] == "sat"]129 conf = sorted(c["conflicts"] for c in solved if c.get("conflicts") is not None)130 key = f"{sol}:r{r}:k{k}" + ("" if placement == "first" else ":spread")131 summary[key] = {132 "solver": sol, "placement": placement, "r": r, "k": k, "n_runs": len(cs), "n_sat": len(solved),133 "n_timeout": sum(c["status"] == "timeout" for c in cs),134 "solved_fraction": len(solved) / len(cs),135 "median_wall_s": times[len(times) // 2],136 "median_wall_s_solved": sorted(c["wall_s"] for c in solved)[len(solved) // 2] if solved else None,137 "median_conflicts_solved": conf[len(conf) // 2] if conf else None,138 "all_verified": all(c.get("verified") for c in solved) if solved else None,139 "n_vars": cs[0].get("n_vars"), "n_clauses": cs[0].get("n_clauses"),140 "max_peak_rss_mb": max(c["peak_rss_mb"] for c in cs),141 "hosts": sorted({c["hostname"] for c in cs}),142 }143 provenance.record("sha256_preimage_sat_scaling",144 {"r_list": R_LIST, "k_list": K_LIST, "timeout_s": TIMEOUT, "feedforward": False,145 "iv": "standard H0", "free_bits": {"first": "first k message bits, W_0 LSB-first", "spread": "bit i -> word i mod 16, position i//16 (cadical only)"},146 "solvers": {"cadical": "pysat Cadical195 (CaDiCaL 1.9.5)", "kissat": "kissat 4.0.4 binary",147 "z3": "z3 bit-vector, r<=16 & k<=32"}},148 {"summary": summary, "cells": cells}, seed="per-cell (see cells)",149 extra={"n_cells": len(cells)}, out=out, started=started)150 print("aggregated", len(cells), "cells ->", out)151152153if __name__ == "__main__":154 ap = argparse.ArgumentParser()155 ap.add_argument("--list-cells", action="store_true")156 ap.add_argument("--seeds", default="0,1,2")157 ap.add_argument("--solvers", default="cadical,kissat,z3")158 ap.add_argument("--placements", default="first,spread")159 ap.add_argument("--cell")160 ap.add_argument("--timeout", type=float, default=TIMEOUT)161 ap.add_argument("--aggregate")162 ap.add_argument("--out")163 ap.add_argument("--seed", type=int, default=0, help="(single-cell convenience) seed when --cell omits it")164 a = ap.parse_args()165 t0 = time.time()166 if a.list_cells:167 for c in list_cells([int(x) for x in a.seeds.split(",")], a.solvers.split(","), a.placements.split(",")):168 print(json.dumps(c))169 elif a.cell:170 cell = json.loads(a.cell)171 cell.setdefault("seed", a.seed)172 res = run_cell(cell, a.timeout)173 if a.out:174 pathlib.Path(a.out).parent.mkdir(parents=True, exist_ok=True)175 pathlib.Path(a.out).write_text(json.dumps(res, indent=1, default=str))176 print(json.dumps({k: v for k, v in res.items() if k not in ("fixed_message_hex",)}, default=str))177 elif a.aggregate:178 aggregate(a.aggregate, a.out, t0)179