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

| r | bits with bias > 4 sigma (3 seeds) | pairs with corr > 4 sigma | bytes rejected (chi2) |
|---|---|---|---|
| 1 | 192 / 192 / 192 | 13 / 5 / 10 (max corr 1.0) | 24 / 24 / 24 |
| 2 | 128 | 12 / 7 / 10 (1.0) | 16 |
| 3 | 64 | 13 / 5 / 10 (1.0) | 8 |
| 4 | 0 | 13 / 6 / 10 (**1.0**) | 0 |
| 5 | 0 | 0 / 0 / 0 (0.028) | 0 |
| 6–64 | 0 (one 4.1-sigma bit at r = 24 seed 2 and one at r = 64 seed 1) | 0–3 per seed | 0 |
| random oracle | 0 | 1 / 0 / 0 | 0 |

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