# 2026-11-01 — Axis C (SHA-256): diffusion, statistical regularity, SAT/SMT preimage & collision scaling, 9-step local collision

Scripts: experiments/reduced_round_sha256/ (README there lists commands, hosts and durations). Results: results/reduced_round_sha256/ (summary.json aggregates the numbers quoted below). Figures: figures/sha256_*.pdf (regenerate with figures/make_sha256_figures.py). Reference implementation: src/wp34/sha256.py (untouched; every SAT/SMT answer and the vectorised step are checked against it).

# 1. Diffusion / avalanche (C1) — diffusion.py, laptop (M5 Max), 3 seeds x N = 2000, ~12 s per seed

Single-bit difference, state tracked after every step without feed-forward. Mean flip ratio reaches 0.49 ("full diffusion") at step 6 for a bit of W_0 (0.015, 0.097, 0.217, 0.341, 0.451, 0.494, 0.499 ...), step 11 for W_5 (= 6 steps after the word enters), step 21 for W_15 (6 steps after it enters at step 16), and step 8 for an IV bit (0.018, 0.072, 0.162, 0.271, 0.378, 0.448, 0.483, 0.497). Identical across the three seeds. After 64 steps the Hamming weight of the difference is 128.0 +/- 8.0 (sd), indistinguishable from the random-oracle control (flip ratio 0.500, sd 0.031 = 0.5/sqrt(256)). The heatmap (fig. sha256_diffusion.pdf) shows the familiar structure: the word a/e registers flip first, b,c,d/f,g,h lag by one step each (register shift), hence the staircase on the bit axis. Classification: known_reproduced (textbook avalanche behaviour; no anomaly). A per-step avalanche of ~6 steps per injected word is the quantitative figure the paper can quote.

# 2. Statistical regularity (C1) — bias_test.py, laptop, 3 seeds x N = 20 000, ~8 s per seed

Output = r-step compression with feed-forward, standard IV. Thresholds: bit bias 4 sigma = 0.0141, correlation 4/sqrt(N) = 0.0283, chi-square on 32 output bytes with Bonferroni alpha = 0.01/32; expected number of (input bit, output bit) pairs above 4 sigma under uniformity = 1.04 (64 x 256 pairs).

Reading: for r <= 3 whole output words are IV words (untouched registers), hence 64 x (4 - r) biased bits. At r = 4 every register has been written once, bit biases and byte chi-square are already at noise level, but 6–13 pairs still have |corr| = 1: with a fixed IV the LSB of e_1 = d + T1 is an affine function of the LSB of W_0 (no carry into bit 0), and e_1 is still exposed in register h after 4 steps. From r = 5 on, every statistic is at the level of the random-oracle control (0–3 pairs above 4 sigma, max |corr| about 0.03, no chi-square rejection). The isolated 4-sigma bits at r = 24 and r = 64 are what one expects from 14 x 256 x 3 = 10 752 tests (expected 0.7). Classification: known_reproduced / empirical_observation — no regularity of the full compression beyond 4 steps is detectable with N = 20 000 single-bit statistics; this is a sanity floor for anything claimed later, not evidence of structure.

# 3. SAT/SMT (C2, C4) — cnf_sha256.py, preimage_sat.py, collision_sat.py, run on M3U96b (M3 Ultra, 28 c)

Encoder: Tseitin, constants folded, modular addition = ripple-carry (14 clauses/bit, chained for multi-operand sums); 64-step compression = 70 801 variables / 313 792 clauses (ff adds 480 vars). Unit test tests/test_sha256_cnf.py (r in {1,4,16,64}, 3 messages, with and without feed-forward, plus a free-IV case) passes. One bug found and fixed during development: a gate-folding rule compared a DIMACS literal to a Python bool (1 == True), which silently replaced Ch(e, x_1, True) by x_1 — caught by the self-test (3 of 24 mismatches), not by inspection. A second issue: pysat's interrupt() does not stop CaDiCaL 1.9.5 (a 5 s limit ran for 10+ minutes), so CaDiCaL is run as the standalone 3.0.1 binary with -t, Kissat 4.0.4 with --time, both as subprocesses (one thread each); the driver has a kill guard at timeout + 120 s.

# 3a. Preimage scaling (572 cells on M3U96b; 351 cells with 3 seeds, 190 with 2, 31 with 1 — see README)

Median wall time (s) per cell, placement first (free bits = low bits of W_0 then W_1), CaDiCaL / Kissat; "T" = all seeds timed out at 300 s; "x/3" = seeds solved:

Placement spread (CaDiCaL, bit i in word i mod 16): r <= 16 still trivial (<= 1 s, <= 22 k conflicts, since for r <= 16 the unused words carry most of the free bits), r = 20: k = 24 in 34 s and k = 32 in 55 s (2 seeds, 0.3–0.6 M conflicts), k >= 40 T; r = 24..48: only k = 16 (14 s .. 134 s); r = 64: T even for k = 16 (3 seeds). z3 (bit-vector theory, r <= 16, k <= 32): r = 4 instant; r = 8: k = 16 in 2.0 s, k = 24 in 233 s (2/3), k = 32 T; r = 12: k = 16 in 128 s, else T; r = 16: T for all k — two to four orders of magnitude slower than the CNF route on the same cells (CaDiCaL/Kissat solve every r <= 16 cell by propagation); z3's bit-blasting of the ripple-carry sums loses the structure that unit propagation exploits in the hand-made CNF. Peak RSS: <= 302 MB for CNF cells (64-step instance: 70 802 vars / 314 036 clauses), <= 605 MB for z3. Every SAT answer re-hashed with the reference: verified: true (572/572 solved cells).

Reading: (1) for r <= 16 the "preimage" of the compression function without unknown IV is not a search problem at all — the step function is invertible and both solvers find the answer with zero conflicts (this is the known invertibility of the Davies–Meyer core, not a solver result); (2) beyond 16 steps the only cells solved within 300 s have k = 16 free bits, i.e. a 2^16 brute-force space (~65 k compressions, milliseconds in C): on this grid SAT is slower than exhaustive search as soon as the message expansion is involved, and k = 24 (2^24, seconds by brute force) already times out at r = 20 for first placement; (3) seed-to-seed variance is large near the frontier (r = 48/64, k = 16: 0–2 of 3 seeds solved). Classification: known_reproduced / empirical_observation (consistent with the literature on SAT-based preimages of SHA-256: solvers do not beat generic search beyond ~20 steps; cf. the 2^16 remark). No statement about full SHA-256 follows.

# 3b. Collisions (264 cells = 11 step counts x 4 variants x 2 solvers x 3 seeds; 600 s)

UNSAT for r <= 8 is a machine-checked statement: no pair of distinct message blocks differing only in the words an r-step compression reads (W_0..W_{r-1}) collides after r <= 8 steps, for the standard IV and for any common IV — this is the "a local collision needs 9 steps" fact (the difference injected into a and e must traverse the four-register shift twice) established here by exhaustive refutation (24 cell groups = 3 step counts x 4 variants x 2 solvers, 3 seeds each = 72 UNSAT runs). For r = 10..16 with the standard IV every collision found differs in exactly 9 consecutive words (W_1..W_9 for r = 10, W_3..W_11 for r = 12, W_5..W_13 for r = 14 (7 words non-zero), W_7..W_15 for r = 16; weight 77–90 bits) and is found by preprocessing + propagation alone: a 9-step local collision placed at the end of the computation, with the free prefix absorbing the conditions. At r = 18 the expanded words W_16, W_17 depend on the message and the solver needs ~10^6 conflicts; all 16 words differ (weight ~250). At r >= 20 nothing is found in 600 s (the literature's practical collisions for 24–31 steps use dedicated differential tools and far more time; our generic encoding is not competitive, which is the expected answer to C4). All 119 collisions are saved (hex) and verified with the reference. Example at r = 18, standard IV, from the JSON (largest_verified_collision_examples). Classification: known_reproduced (9-step minimum, local-collision structure, 18-step practical collisions by generic SAT — cf. 18/20-step SAT collisions in the literature; UNSAT proofs for r <= 8 are a small new_verified by-product, though expected).

# 4. 9-step local collision (C3, C4) — local_collision.py, laptop, N = 100 000 per bit, 943 s + 2nd run

Linearised model: + -> XOR and Boolean functions absorb all differences; the propagation is then GF(2)-linear, dstate' = A dstate + B dW with A (256 x 256) built from the Sigma matrices and the register shifts. Derived pattern for a perturbation d in W_i (docstring of the script has the step-by-step derivation): (d, S0(d)^S1(d), S1(S0(d)), 0, d, S0(d)^S1(d), 0, 0, d) — the a-register carries a difference only at step i+1, the e-register at i+1 (d), i+2 (S0(d)) and i+5 (d). Verified by matrix arithmetic for all 32 single-bit d and 20 random multi-bit d (the map is linear so the 32 basis checks are exhaustive); dropping any correction leaves a nonzero difference (tests/test_sha256_local_collision.py). For d = 2^31 the pattern is (80000000, 22140240, 42851098, 0, 80000000, 22140240, 0, 0, 80000000).

Real (modular) step, random state and words, XOR pattern applied blindly: 0 collisions in 32 x 100 000 samples (rule-of-three upper bound 3e-5 per position; second seed, bits 31 and 0: also 0). The survival of the intended difference after step i is 0.25 for bits 0..30 and 1.0 for bit 31: at step i only W_i differs, so the modular difference of T1 is +/-2^j and the XOR difference of a' = T1 + T2 and of e' = d + T1 equals 2^j iff no carry propagates in each of the two sums (probability 1/2 each, 1/4 overall); for the MSB no carry is possible, so the first step always conforms. After step i+1 survival drops to 3e-5 – 5.4e-4 (the 6-bit correction S0(d)^S1(d) must be absorbed through three additions and two Boolean functions), and after step i+2 it is 0 in every sample. Classification: known_reproduced (the pattern holds only under message / state conditions; the raw probability of the XOR characteristic is far below 2^-17 per step i+1 alone).

SAT (CaDiCaL binary, free 256-bit state and free W_i..W_{i+8}, W' = W ^ pattern, equal state after 9 steps, 15 218 vars / 66 208 clauses, K_0..K_8): a conforming pair was found and verified with the reference for all 32 bit positions, in 4.4 s (bit 29) to 118 s (bit 0); bit 31 in 5.1 s / 328 k conflicts (second seed 9.0 s), bit 0 in 118 s / 7.5 M conflicts (second seed 52 s / 3.3 M). Example for d = 2^31: state 3ffffe31 7ff49fa2 67ff13c8 ffe19d9b dffae8db ff73ee77 ff7dfdfe b91789e0, W = 88f6da84 dd518e9d 094ddd6f 3e9f5b2d ae8d60e9 ffeff1bf b652c097 b7f66631 80000000. Classification: known_reproduced (existence of conforming pairs for the GH local collision under conditions — Gilbert–Handschuh 2003, Mendel et al. 2006 — reproduced by a generic SAT solver with no hand-made conditions).

# 5. Honest summary

• Nothing here touches the security of full SHA-256: every solved instance is either <= 24 steps or has <= 16 free bits; 64-step preimage cells with >= 16 free bits all time out at 300 s, as expected.
• The useful quantitative outputs for the paper are: 6 steps per injected word to full diffusion; statistics at the random-oracle floor from r = 5; the SAT frontier tables (section 3); UNSAT proofs for r <= 8 collisions; the 9-step local-collision pattern with its measured conformance probabilities and SAT-found conforming pairs.
• Reductions actually applied to the plan: see README ("What was reduced").