#!/usr/bin/env python3
"""Solve the checksum seed: solve_ckseed.py image.bin

CRC32 is affine, so one image's 32-bit equality is 32 linear constraints on
the 32 unknown bits at file[8:12]. Solves via GF(2) Gaussian elimination and
prints the constant K such that
    stored == CRC32(file with [8:12] := K).
Run on several stock images: all must print the same K (here: C27C6282).
Stdlib only.
"""
import binascii
import struct
import sys


def crc(b: bytes, init: int = 0) -> int:
    return binascii.crc32(b, init) & 0xFFFFFFFF


def solve_for_K(d: bytes, target: int):
    n = len(d)
    d0 = bytearray(d)
    d0[8:12] = b"\0\0\0\0"
    rhs = target ^ crc(bytes(d0))
    c0 = crc(bytes(n))
    cols = []
    for p in range(32):
        m = bytearray(n)
        m[8 + p // 8] = 1 << (p % 8)
        cols.append(crc(bytes(m)) ^ c0)
    rows = []
    for r in range(32):
        mask = 0
        for p in range(32):
            if (cols[p] >> r) & 1:
                mask |= 1 << p
        rows.append([mask, (rhs >> r) & 1])
    where = [-1] * 32
    row = 0
    for col in range(32):
        sel = next((i for i in range(row, 32)
                    if (rows[i][0] >> col) & 1), -1)
        if sel < 0:
            continue
        rows[row], rows[sel] = rows[sel], rows[row]
        where[col] = row
        for i in range(32):
            if i != row and ((rows[i][0] >> col) & 1):
                rows[i][0] ^= rows[row][0]
                rows[i][1] ^= rows[row][1]
        row += 1
    for i in range(32):
        if rows[i][0] == 0 and rows[i][1] != 0:
            return None  # inconsistent: wrong structural hypothesis
    if any(w < 0 for w in where):
        return None  # underdetermined
    return sum((rows[where[p]][1] << p) for p in range(32))


def main() -> int:
    d = open(sys.argv[1], "rb").read()
    target = struct.unpack("<I", d[8:12])[0]
    K = solve_for_K(d, target)
    print("%08X" % K if K is not None else "NO_SOLUTION")
    return 0 if K is not None else 1


if __name__ == "__main__":
    sys.exit(main())