1"""Tseitin CNF encoder for r-step SHA-256 compression (research question C2).23Representation. A *bit* is either a DIMACS literal (non-zero int) or a Python bool constant; a *word* is a list of 324bits, index 0 = least significant bit. Rotations and shifts are free (list re-indexing; shifted-in bits are the5constant False). Gates with constant inputs are folded. Gates:6 xor(a,b) : 4 clauses and(a,b) : 3 clauses not : literal negation7 ch(e,f,g) : 4 clauses (z = e ? f : g) maj(a,b,c) : 6 clauses8 full adder : sum = xor(xor(x,y),c) (8 clauses), carry = maj(x,y,c) (6 clauses) -> 14 clauses per bit9 add(x, y) : 32-bit ripple-carry (carry out of bit 31 dropped = mod 2^32); multi-operand sums are chained10 2-operand adders.11The step and schedule follow `wp34.sha256` exactly (T1 = h + S1(e) + Ch(e,f,g) + K_t + W_t; T2 = S0(a) + Maj(a,b,c);12a' = T1 + T2, e' = d + T1). Message words are always fresh variables (fixing bits = unit clauses), so the13variable/clause counts of an instance do not depend on how many bits are fixed. The IV is either the constant H014(folded) or 8 free words (semi-free-start).1516`build_compression(r, feedforward, free_iv)` returns (cnf, W, IV, OUT) where W = 16 message words, IV = 8 words17(constants or variables) and OUT = 8 output words (after r steps, with or without the IV feed-forward).18`decode_word(model, word)` reads a word back from a solver model. The self-test (`python cnf_sha256.py --selftest`)19fixes all 512 message bits + IV and checks the solved output against `wp34.sha256.compress`.20"""21from __future__ import annotations22import argparse, random, sys, time23from common import S, MASK2425K = S.K26H0 = S.H0272829class CNF:30 def __init__(self):31 self.nv = 032 self.clauses: list[list[int]] = []33 self._true = None3435 # ---- variables -------------------------------------------------------------------------------------------36 def var(self) -> int:37 self.nv += 138 return self.nv3940 def word(self) -> list[int]:41 return [self.var() for _ in range(32)]4243 @staticmethod44 def const_word(v: int) -> list[bool]:45 return [bool((v >> i) & 1) for i in range(32)]4647 def true_lit(self) -> int:48 if self._true is None:49 self._true = self.var()50 self.clauses.append([self._true])51 return self._true5253 def lit(self, b) -> int:54 """Any bit -> literal (constants mapped onto a pinned TRUE variable)."""55 if b is True:56 return self.true_lit()57 if b is False:58 return -self.true_lit()59 return b6061 def add(self, *lits):62 self.clauses.append(list(lits))6364 # ---- gates -------------------------------------------------------------------------------------------------65 @staticmethod66 def neg(a):67 if isinstance(a, bool):68 return not a69 return -a7071 def xor(self, a, b):72 if isinstance(a, bool):73 return self.neg(b) if a else b74 if isinstance(b, bool):75 return self.neg(a) if b else a76 if a == b:77 return False78 if a == -b:79 return True80 z = self.var()81 self.add(-a, -b, -z); self.add(a, b, -z); self.add(a, -b, z); self.add(-a, b, z)82 return z8384 def and_(self, a, b):85 if isinstance(a, bool):86 return b if a else False87 if isinstance(b, bool):88 return a if b else False89 if a == b:90 return a91 if a == -b:92 return False93 z = self.var()94 self.add(-z, a); self.add(-z, b); self.add(z, -a, -b)95 return z9697 def or_(self, a, b):98 return self.neg(self.and_(self.neg(a), self.neg(b)))99100 def ch(self, e, f, g):101 """z = (e and f) xor (not e and g) = e ? f : g."""102 if isinstance(e, bool):103 return f if e else g104 if isinstance(f, bool) and isinstance(g, bool):105 if f == g:106 return f107 return e if f else self.neg(e)108 if not isinstance(f, bool) and not isinstance(g, bool) and f == g:109 return f # (never compare a literal with a bool: in Python 1 == True)110 f, g = self.lit(f), self.lit(g)111 z = self.var()112 self.add(-e, -f, z); self.add(-e, f, -z); self.add(e, -g, z); self.add(e, g, -z)113 return z114115 def maj(self, a, b, c):116 for x, y, w in ((a, b, c), (b, c, a), (c, a, b)):117 if isinstance(x, bool):118 return self.or_(y, w) if x else self.and_(y, w)119 if a == b or a == c:120 return a121 if b == c:122 return b123 if a == -b:124 return c125 if a == -c:126 return b127 if b == -c:128 return a129 z = self.var()130 self.add(-a, -b, z); self.add(-a, -c, z); self.add(-b, -c, z)131 self.add(a, b, -z); self.add(a, c, -z); self.add(b, c, -z)132 return z133134 # ---- words -------------------------------------------------------------------------------------------------135 def xor_w(self, x, y):136 return [self.xor(p, q) for p, q in zip(x, y)]137138 def and_w(self, x, y):139 return [self.and_(p, q) for p, q in zip(x, y)]140141 def not_w(self, x):142 return [self.neg(p) for p in x]143144 @staticmethod145 def rotr(x, k):146 return [x[(i + k) % 32] for i in range(32)]147148 @staticmethod149 def shr(x, k):150 return [x[i + k] if i + k < 32 else False for i in range(32)]151152 def Sigma0(self, x):153 return self.xor_w(self.xor_w(self.rotr(x, 2), self.rotr(x, 13)), self.rotr(x, 22))154155 def Sigma1(self, x):156 return self.xor_w(self.xor_w(self.rotr(x, 6), self.rotr(x, 11)), self.rotr(x, 25))157158 def sigma0(self, x):159 return self.xor_w(self.xor_w(self.rotr(x, 7), self.rotr(x, 18)), self.shr(x, 3))160161 def sigma1(self, x):162 return self.xor_w(self.xor_w(self.rotr(x, 17), self.rotr(x, 19)), self.shr(x, 10))163164 def ch_w(self, e, f, g):165 return [self.ch(p, q, s) for p, q, s in zip(e, f, g)]166167 def maj_w(self, a, b, c):168 return [self.maj(p, q, s) for p, q, s in zip(a, b, c)]169170 def add_w(self, x, y):171 """Ripple-carry modular adder."""172 out, carry = [], False173 for i in range(32):174 s = self.xor(self.xor(x[i], y[i]), carry)175 if i < 31:176 carry = self.maj(x[i], y[i], carry)177 out.append(s)178 return out179180 def sum_w(self, *words):181 acc = words[0]182 for w in words[1:]:183 acc = self.add_w(acc, w)184 return acc185186 def eq_w(self, x, y):187 """Assert x == y bitwise."""188 for p, q in zip(x, y):189 self.assert_eq(p, q)190191 def assert_eq(self, p, q):192 if isinstance(p, bool) and isinstance(q, bool):193 if p != q:194 self.add(-self.true_lit())195 return196 if isinstance(p, bool):197 p, q = q, p198 if isinstance(q, bool):199 self.add(p if q else -p)200 return201 self.add(-p, q); self.add(p, -q)202203 def fix_word(self, w, value: int):204 for i in range(32):205 self.assert_eq(w[i], bool((value >> i) & 1))206207 def neq_w_any(self, pairs):208 """Assert that at least one bit differs among the given (word, word) pairs: OR of XORs."""209 diffs = []210 for x, y in pairs:211 for p, q in zip(x, y):212 d = self.xor(p, q)213 if d is True:214 return215 if d is not False:216 diffs.append(d)217 if not diffs:218 self.add(-self.true_lit())219 else:220 self.add(*diffs)221222 # ---- SHA-256 -----------------------------------------------------------------------------------------------223 def step(self, state, k: int, w):224 a, b, c, d, e, f, g, h = state225 T1 = self.sum_w(h, self.Sigma1(e), self.ch_w(e, f, g), self.const_word(k), w)226 T2 = self.add_w(self.Sigma0(a), self.maj_w(a, b, c))227 return (self.add_w(T1, T2), a, b, c, self.add_w(d, T1), e, f, g)228229 def schedule(self, W16, rounds: int):230 W = list(W16)231 for t in range(16, rounds):232 W.append(self.sum_w(self.sigma1(W[t - 2]), W[t - 7], self.sigma0(W[t - 15]), W[t - 16]))233 return W234235 def compress(self, IV, W16, rounds: int, feedforward: bool, trace=None):236 W = self.schedule(W16, rounds)237 s = tuple(IV)238 for t in range(rounds):239 s = self.step(s, K[t], W[t])240 if trace is not None:241 trace.append(s)242 if not feedforward:243 return list(s)244 return [self.add_w(x, y) for x, y in zip(IV, s)]245246 def stats(self):247 return {"n_vars": self.nv, "n_clauses": len(self.clauses)}248249 def to_dimacs(self) -> str:250 lines = ["p cnf %d %d" % (self.nv, len(self.clauses))]251 lines += [" ".join(map(str, c)) + " 0" for c in self.clauses]252 return "\n".join(lines) + "\n"253254255def build_compression(rounds: int, feedforward: bool = False, free_iv: bool = False, cnf: CNF | None = None):256 cnf = cnf or CNF()257 W = [cnf.word() for _ in range(16)]258 IV = [cnf.word() for _ in range(8)] if free_iv else [CNF.const_word(h) for h in H0]259 OUT = cnf.compress(IV, W, rounds, feedforward)260 return cnf, W, IV, OUT261262263def decode_word(model_set, word) -> int:264 """model_set: set of true literals (positive ints)."""265 v = 0266 for i, b in enumerate(word):267 if b is True or (not isinstance(b, bool) and ((b > 0 and b in model_set) or (b < 0 and -b not in model_set))):268 v |= 1 << i269 return v270271272def model_to_set(model) -> set:273 return {l for l in model if l > 0}274275276def selftest(rounds_list=(1, 4, 16, 64), n_msgs=3, seed=0, verbose=True):277 from pysat.solvers import Cadical195278 rng = random.Random(seed)279 ok = True280 for r in rounds_list:281 for ff in (False, True):282 for _ in range(n_msgs):283 block = bytes(rng.getrandbits(8) for _ in range(64))284 words = S.bytes_to_words(block)285 cnf, W, IV, OUT = build_compression(r, feedforward=ff)286 for w, v in zip(W, words):287 cnf.fix_word(w, v)288 t0 = time.time()289 with Cadical195(bootstrap_with=cnf.clauses) as s:290 assert s.solve(), "unexpected UNSAT"291 m = model_to_set(s.get_model())292 got = [decode_word(m, w) for w in OUT]293 ref = S.compress(S.H0, block, r, feedforward=ff)294 good = got == ref295 ok &= good296 if verbose:297 print(f"r={r:2d} ff={ff!s:5} vars={cnf.nv:7d} clauses={len(cnf.clauses):8d} "298 f"solve={time.time()-t0:.3f}s match={good}")299 return ok300301302if __name__ == "__main__":303 ap = argparse.ArgumentParser()304 ap.add_argument("--selftest", action="store_true")305 ap.add_argument("--dimacs", help="write the r-step CNF (free message, fixed IV) to this file")306 ap.add_argument("--rounds", type=int, default=64)307 a = ap.parse_args()308 if a.selftest:309 sys.exit(0 if selftest() else 1)310 if a.dimacs:311 cnf, *_ = build_compression(a.rounds)312 open(a.dimacs, "w").write(cnf.to_dimacs())313 print(cnf.stats())314