1"""Python side of formal/Wp34/LocalCollision.lean.231. Simulates two GF(2)-linearised SHA-256 step functions and checks, on random inputs, the4 9-step local-collision correction vectors that are then proven for ALL inputs by bv_decide:5 * model "absorb" : Ch and Maj replaced by the zero function (Gilbert-Handschuh 20036 conditions "the Boolean functions absorb the difference"), '+' replaced by XOR;7 * model "xor3" : Ch and Maj replaced by x ^ y ^ z (Chabaud-Joux 1998 style linearisation),8 '+' replaced by XOR.92. Finds an explicit counter-example showing that the "absorb" correction vector is NOT a10 collision for the real (modular, non-linear) step function -- the linearised local collision11 is a differential characteristic that holds only with some probability on the real function.1213Run: .venv/bin/python formal/scripts/local_collision.py14"""15from __future__ import annotations16import os, random, sys17sys.path.insert(0, os.path.join(os.path.dirname(__file__), "..", "..", "src"))18from wp34.sha256 import Sigma0, Sigma1, Ch, Maj, step, MASK # noqa: E4021920def lin_step(s, k, w, boolf):21 a, b, c, d, e, f, g, h = s22 T1 = h ^ Sigma1(e) ^ boolf(e, f, g) ^ k ^ w23 T2 = Sigma0(a) ^ boolf(a, b, c)24 return (T1 ^ T2, a, b, c, d ^ T1, e, f, g)2526ZERO = lambda x, y, z: 027XOR3 = lambda x, y, z: x ^ y ^ z2829def corrections_absorb(d):30 return [d, Sigma1(d) ^ Sigma0(d), Sigma1(Sigma0(d)), 0, d, Sigma0(d) ^ Sigma1(d), 0, 0, d]3132def corrections_xor3(d):33 S0, S1 = Sigma0(d), Sigma1(d)34 return [d, S1 ^ S0, Sigma1(S0 ^ d) ^ S0 ^ d, S1 ^ S0, S1 ^ S0, S0 ^ S1, d, 0, d]3536def run9(s, K, W, stepf):37 for t in range(9):38 s = stepf(s, K[t], W[t])39 return s4041def main():42 rng = random.Random(34)43 for name, boolf, corr in [("absorb", ZERO, corrections_absorb), ("xor3", XOR3, corrections_xor3)]:44 for _ in range(5000):45 s = tuple(rng.getrandbits(32) for _ in range(8))46 K = [rng.getrandbits(32) for _ in range(9)]47 W = [rng.getrandbits(32) for _ in range(9)]48 d = rng.getrandbits(32)49 W2 = [w ^ c for w, c in zip(W, corr(d))]50 f = lambda st, k, w: lin_step(st, k, w, boolf)51 assert run9(s, K, W, f) == run9(s, K, W2, f), (name, s, K, W, d)52 print(f"model {name}: 9-step local collision holds on 5000 random (state, K, W, delta) -- "53 "the universal statement is proven by bv_decide in Lean")5455 # Counter-example for the real step function (same XOR corrections, "absorb" vector).56 s0 = (0,) * 8; K0 = [0] * 9; W0 = [0] * 9; d = 157 W1 = [w ^ c for w, c in zip(W0, corrections_absorb(d))]58 out0, out1 = run9(s0, K0, W0, step), run9(s0, K0, W1, step)59 print("real step, s = 0, K = 0, W = 0, delta = 1 :")60 print(" corrected W' =", [f"{w:#010x}" for w in W1])61 print(" out(W) =", [f"{w:#010x}" for w in out0])62 print(" out(W') =", [f"{w:#010x}" for w in out1])63 print(" collision on the real step?", out0 == out1)64 # how often does the characteristic hold on the real step for random inputs with 1-bit delta?65 hits = 0; N = 2000066 for _ in range(N):67 s = tuple(rng.getrandbits(32) for _ in range(8))68 K = [rng.getrandbits(32) for _ in range(9)]69 W = [rng.getrandbits(32) for _ in range(9)]70 d = 1 << rng.randrange(32)71 W2 = [w ^ c for w, c in zip(W, corrections_absorb(d))]72 hits += run9(s, K, W, step) == run9(s, K, W2, step)73 print(f" real step, random inputs, 1-bit delta, XOR corrections: {hits}/{N} collisions "74 f"(the XOR characteristic is a low-probability event on the modular function)")7576if __name__ == "__main__":77 main()78