# 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.

SAT-SCALING-PLACEHOLDER

# 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").