1"""Gate for the Tseitin SHA-256 encoder: fixed message + IV, solved with CaDiCaL, must reproduce the reference."""2import pathlib, random, sys3ROOT = pathlib.Path(__file__).resolve().parents[1]4sys.path.insert(0, str(ROOT / "src"))5sys.path.insert(0, str(ROOT / "experiments" / "reduced_round_sha256"))6from wp34 import sha256 as S7import cnf_sha256 as C8from pysat.solvers import Cadical19591011def _solve(cnf):12 with Cadical195(bootstrap_with=cnf.clauses) as s:13 assert s.solve()14 return C.model_to_set(s.get_model())151617def test_encoder_matches_reference():18 rng = random.Random(2026)19 for r in (1, 4, 16, 64):20 for ff in (False, True):21 for _ in range(3):22 block = bytes(rng.getrandbits(8) for _ in range(64))23 cnf, W, IV, OUT = C.build_compression(r, feedforward=ff)24 for w, v in zip(W, S.bytes_to_words(block)):25 cnf.fix_word(w, v)26 m = _solve(cnf)27 assert [C.decode_word(m, w) for w in OUT] == S.compress(S.H0, block, r, feedforward=ff)282930def test_encoder_free_iv_matches_reference():31 rng = random.Random(7)32 for r in (3, 20):33 block = bytes(rng.getrandbits(8) for _ in range(64))34 iv = [rng.getrandbits(32) for _ in range(8)]35 cnf, W, IV, OUT = C.build_compression(r, feedforward=True, free_iv=True)36 for w, v in zip(W, S.bytes_to_words(block)):37 cnf.fix_word(w, v)38 for w, v in zip(IV, iv):39 cnf.fix_word(w, v)40 m = _solve(cnf)41 assert [C.decode_word(m, w) for w in OUT] == S.compress(iv, block, r, feedforward=True)424344def test_preimage_small_instance_is_sat_and_verifies():45 rng = random.Random(3)46 block = bytes(rng.getrandbits(8) for _ in range(64))47 target = S.compress(S.H0, block, 8, feedforward=False)48 cnf, W, IV, OUT = C.build_compression(8)49 words = S.bytes_to_words(block)50 for j, w in enumerate(W):51 if j == 0:52 for i in range(16, 32): # 16 free bits, rest fixed53 cnf.assert_eq(w[i], bool((words[0] >> i) & 1))54 else:55 cnf.fix_word(w, words[j])56 for o, v in zip(OUT, target):57 cnf.fix_word(o, v)58 m = _solve(cnf)59 found = [C.decode_word(m, w) for w in W]60 assert S.compress(S.H0, S.words_to_bytes(found), 8, feedforward=False) == target61