1"""GF(2) rank / kernel of the SHA-256 sigma functions on 32-bit words.23Each of Sigma0, Sigma1, sigma0, sigma1 is GF(2)-linear (XOR of rotations / shifts), hence a432x32 matrix over GF(2). This script computes the rank, the kernel dimension and an explicit5kernel basis (every non-zero kernel vector is a counter-example to injectivity). It is used6to decide which theorem to state in formal/Wp34/Sha256Words.lean before asking bv_decide.78Run: .venv/bin/python formal/scripts/gf2_rank.py9"""10from __future__ import annotations11import sys, os12sys.path.insert(0, os.path.join(os.path.dirname(__file__), "..", "..", "src"))13from wp34.sha256 import Sigma0, Sigma1, sigma0, sigma1, MASK # noqa: E4021415def columns(f):16 return [f(1 << i) & MASK for i in range(32)] # image of basis vector e_i1718def rank_and_kernel(f):19 cols = columns(f)20 # Gaussian elimination on the columns as 32-bit integers, tracking combinations for the kernel21 basis: list[tuple[int, int]] = [] # (pivot-reduced vector, combination mask over e_i)22 kernel: list[int] = []23 for i, v in enumerate(cols):24 comb = 1 << i25 for bv, bc in basis:26 if v & (1 << (bv.bit_length() - 1)):27 v ^= bv28 comb ^= bc29 if v == 0:30 kernel.append(comb)31 else:32 basis.append((v, comb))33 basis.sort(key=lambda t: -t[0])34 return len(basis), kernel3536def main():37 for name, f in [("Sigma0", Sigma0), ("Sigma1", Sigma1), ("sigma0", sigma0), ("sigma1", sigma1)]:38 r, ker = rank_and_kernel(f)39 print(f"{name}: rank = {r}, kernel dimension = {32 - r}")40 for k in ker:41 assert f(k) & MASK == 0, (name, hex(k))42 print(f" kernel vector x = {k:#010x} ({name}(x) = 0, x != 0)")43 if not ker:44 # check that a random pair with equal image does not exist (bijective)45 print(" injective (kernel trivial) -> bijective on 32 bits")4647if __name__ == "__main__" and "--lean" not in sys.argv:48 main()495051# ---- Lean code generation (explicit inverses, pasted into formal/Wp34/Sha256Words.lean) ----52def inverse_columns(f):53 """Columns of the inverse matrix: inv(e_i) for i = 0..31 (Gauss-Jordan over GF(2))."""54 rows = [0] * 3255 for i in range(32):56 y = f(1 << i) & MASK57 for j in range(32):58 if (y >> j) & 1:59 rows[j] |= 1 << i60 I = [1 << j for j in range(32)]61 for bit in range(32):62 piv = next(i for i in range(bit, 32) if rows[i] >> bit & 1)63 rows[bit], rows[piv] = rows[piv], rows[bit]; I[bit], I[piv] = I[piv], I[bit]64 for i in range(32):65 if i != bit and rows[i] >> bit & 1:66 rows[i] ^= rows[bit]; I[i] ^= I[bit]67 assert rows == [1 << j for j in range(32)]68 def apply(x):69 return sum(((bin(I[j] & x).count("1") & 1) << j) for j in range(32))70 return [apply(1 << i) for i in range(32)], apply7172def rotation_set(apply):73 """If inv is a XOR of rotations, return the rotation amounts (checked), else None."""74 from wp34.sha256 import rotr75 inv1 = apply(1)76 S = sorted(((32 - k) % 32) for k in range(32) if inv1 >> k & 1)77 import random78 for _ in range(2000):79 x = random.getrandbits(32); y = 080 for j in S: y ^= rotr(x, j)81 if y != apply(x):82 return None83 return S8485def lean_code():86 from wp34.sha256 import rotr87 out = []88 for name, f in [("Sigma0", Sigma0), ("Sigma1", Sigma1), ("sigma0", sigma0), ("sigma1", sigma1)]:89 cols, apply = inverse_columns(f)90 for _ in range(2000):91 x = __import__("random").getrandbits(32)92 assert apply(f(x) & MASK) == x and f(apply(x)) & MASK == x93 S = rotation_set(apply)94 if S is not None:95 body = " ^^^ ".join(f"rotr x {j}" for j in S)96 out.append(f"def {name}Inv (x : Word) : Word :=\n {body}")97 else:98 body = " ^^^\n ".join(f"bitMask x {i} &&& {c:#010x}#32" for i, c in enumerate(cols))99 out.append(f"def {name}Inv (x : Word) : Word :=\n {body}")100 return "\n\n".join(out)101102if __name__ == "__main__" and "--lean" in sys.argv:103 print(lean_code())104