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

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

| r \ k | 16 | 24 | 32 | 40 | 48 | 56 | 64 |
|---|---|---|---|---|---|---|---|
| 4–16 | 0.01–0.03 / 0.01–0.02, **0 conflicts** (pure propagation = step inversion) | same | same | same | same | same | same |
| 20 | 6.4 / 1.3 | T / T | T | T | T | T | T |
| 24 | 19.3 / 20.1 | T | T | T | T | T | T |
| 28 | 50.4 / 70.3 | T | T | T | T | T | T |
| 32 | 86.7 / 107.6 | T | T | T | T | T | T |
| 40 | 96.0 / 86.6 | T | T | T | T | T | T |
| 48 | T (0/3) / 279.8 (2/3) | T | T | T | T | T | T |
| 64 | 261.8 (2/3) / 300 (1/3 solved, 249.7 s) | T | T | T | T | T | T |

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)

| r | standard IV | standard IV + ff | semi-free-start | semi-free-start + ff |
|---|---|---|---|---|
| 4, 6, 8 | **UNSAT** (3/3 seeds, both solvers; 0.1–4.7 s) | UNSAT | UNSAT | UNSAT |
| 10–16 | SAT, 0.02–0.05 s, **0 conflicts** | SAT, 0 conflicts | SAT 0.7–2.4 s, 10–38 k conflicts | SAT 0.7–2.4 s |
| 18 | SAT 52.8 / 53.2 s (CaDiCaL / Kissat), 0.9–1.0 M conflicts | SAT 120.8 (2/3) / 144.9 s, 2.0–2.7 M conflicts | SAT 8.5 / 7.1 s, 0.14 M conflicts | SAT 10.1 / 8.2 s |
| 20, 22, 24 | T (all seeds, both solvers) | T | T | T |

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