Reduced-round SHA-256 experiments (WP34 Axis C)
All scripts are re-runnable from the repository root with PYTHONPATH=src .venv/bin/python experiments/reduced_round_sha256/<script>.py --seed S --out results/reduced_round_sha256/<name>.json. Every result JSON
is written with wp34.provenance.record (host, CPU, RAM, OS, library versions, seed, command, timestamp). The reference
src/wp34/sha256.py is never modified; all helpers live here.
| file | role |
|---|---|
common.py |
path setup, peak-RSS (resource.getrusage), random-oracle control (hashlib over a secret salt), bootstrap CI |
diffusion.py |
avalanche of the compression function, steps 1..64, single-bit difference in W_0 / W_5 / W_15 / IV |
bias_test.py |
bit bias, input/output linear correlations, byte chi-square for r in {1,...,64} + random-oracle control |
cnf_sha256.py |
Tseitin CNF encoder (words = 32 literals, free rotations, Ch/Maj/XOR gates, ripple-carry adders); --selftest |
solvers.py |
CaDiCaL (binary, -t), Kissat (binary, --time), z3 bit-vector model; uniform statistics dict |
preimage_sat.py |
3a: preimage cells (r, k, seed, solver, placement); --list-cells, --cell, --aggregate |
collision_sat.py |
3b: collision cells (r, seed, solver, iv fixed/free, feed-forward); same modes |
local_collision.py |
3c: 9-step local collision — GF(2) verification, empirical conformance, SAT conforming pairs |
cluster_driver.py |
cell queue runner: one fresh subprocess per cell, N workers, seed-0 phase first, deadline, kill guard |
run_cluster.sh |
setup / launch / status / fetch on cluster node M3U96b |
make_summary.py |
aggregates everything into results/reduced_round_sha256/summary.json |
../../figures/make_sha256_figures.py |
regenerates figures/sha256_{diffusion,bias,sat_scaling,collision_scaling,local_collision}.pdf |
../../tests/test_sha256_cnf.py, test_sha256_local_collision.py |
gates: encoder == reference for r in {1,4,16,64}; pattern cancels; vectorised step == reference |
What ran, where, how long
| experiment | host | command | runs | wall |
|---|---|---|---|---|
| diffusion | laptop (MacBook Pro M5 Max, 18 c) | diffusion.py --seed {1,2,3} --n 2000 |
3 seeds x 4 configs x 2000 msgs | 11.5 s per seed |
| bias | laptop | bias_test.py --seed {1,2,3} --n 20000 |
3 seeds x 14 step counts | 7.6 s per seed |
| local collision | laptop | local_collision.py --seed 1 --n 100000 --sat-bits all --sat-timeout 120 and --seed 2 --sat-bits 31,0 --sat-timeout 900 |
32 x 100 000 samples; 32 + 2 SAT runs | 943 s + 70 s |
| preimage SAT grid | M3U96b (Mac Studio M3 Ultra, 28 c / 96 GB, macOS 26.4, python 3.12 venv via uv) | run_cluster.sh launch -> cluster_driver.py --script preimage_sat.py --workers 14 --deadline 4800 |
see below | see below |
| collision SAT grid | M3U96b | cluster_driver.py --script collision_sat.py --workers 10 --deadline 4800 |
see below | see below |
Solver binaries copied to M3U96b:~/wp34/bin/ (kissat 4.0.4 and cadical 3.0.1 from Homebrew, self-contained arm64;
checked with --version and a 2-clause instance). Results come back with run_cluster.sh fetch into
results/reduced_round_sha256/m3u96b/ (per-cell JSONs + driver logs) and the two aggregated files are copied to
results/reduced_round_sha256/{preimage_sat_scaling,collision_sat}.json.
SAT grids: what ran on M3U96b
- Launch 1 (01:06 node time): preimage driver 14 workers + collision driver 10 workers,
--deadline 4800. The first launch (00:45) had been killed after 13 min because CaDiCaL-in-pysat ignored the timeout; its CaDiCaL cells were discarded, Kissat cells kept (identical code path). - Collision grid: 264/264 cells, 3 seeds everywhere, finished in 4363 s (
driver_collision.log). - Preimage grid: 450 cells by the deadline (seed 0 complete = 243 cells; seed 1 complete for
firstand z3, partial forspread), then a completion run (02:33, 24 workers, filterk == 16 or r <= 16, 347 s) added seed 2 for every cell that was solvable. Final: 572 cells — 351 cells with 3 seeds, 190 with 2, 31 with 1 (m3u96b/cells_preimage/skipped_cells.jsonlists the 279 cells never started at the deadline; the 157 cells still missing a seed are all in rows where every started seed timed out at 300 s: k >= 24 with r >= 20, andspreadr >= 24). - Remote aggregation of the preimage grid crashed once because the driver's
skipped_cells.jsonwas globbed as a cell; fixed (aggregators now skip non-cell files) and re-run on the node — both aggregated JSONs carryhost.hostname = m3u96b; per-cell JSONs carry their own hostname. - Preimage cells: 572/572 SAT answers
verified: true; collisions: 119/119verified: true. - Largest solved cells: preimage
firstCaDiCaL r = 64, k = 16 (2/3 seeds, median 262 s), Kissat r = 48, k = 16 (2/3) and r = 64 k = 16 (1/3);spreadCaDiCaL r = 48 k = 16 (3/3, 134 s) and r = 20 k = 32 (2/2, 55 s); z3 r = 12 k = 16 (128 s). Collisions: r = 18 for all four variants (semi-free-start 7–10 s, standard IV 53–145 s); r >= 20 timeouts; r <= 8 UNSAT. Full tables:results/reduced_round_sha256/summary.json,research_log/2026-11-01-sha256.md.
What was reduced relative to the plan
- Preimage grid: seed 2 (and part of seed 1 for
spread) only for cells with k = 16 or r <= 16; the rows k >= 24, r >= 20 have 2 seeds (first, both solvers), thespreadrows r >= 28 have 1–3 seeds (1 for k >= 24). No row was skipped. - Local collision SAT: 120 s budget per bit for the 32-bit sweep (all 32 solved, max 118 s); bits 31 and 0 re-run with a second seed and a 900 s budget (solved in 9.0 s and 52.2 s).
- Nothing else was reduced: diffusion N = 2000 x 3 seeds, bias N = 20 000 x 3 seeds, local-collision 100 000 samples per bit.
Design notes and gotchas
- Preimage free bits. Placement
first(as specified: the first k message bits, W_0 LSB-first, then W_1) makes every r <= 16 cell solvable by unit propagation alone (0 conflicts): the step function is a bijection and with all other words fixed the solver simply inverts the steps from the known target. This is a property of the compression function without unknown IV, not a solver feat. A second placementspread(bit i -> word i mod 16, CaDiCaL only) was added so that the difficulty does not collapse; both are reported. - Collisions. M != M' is restricted to the words an r-step compression reads (W_0..W_{min(r,16)-1}); otherwise a difference in an unused word is a trivial "collision" (this happened in the first smoke test). With a shared IV, feed-forward does not change the collision event; the two CNFs differ only by the extra adders.
- Timeouts. pysat's
interrupt()does not stop CaDiCaL 1.9.5 in-process; the first launch had to be killed and CaDiCaL is now the standalone binary with a real-time limit. CaDiCaL omits statistics lines whose value is 0, which the parser maps to 0 (only when the status is SAT/UNSAT). - Seeds. CaDiCaL/Kissat receive
--seed; the instance (message, target) also depends on the seed for preimage cells. Collision cells have no instance randomness (the seed only changes the solver seed). - Peak RSS is measured per cell (fresh process;
ru_maxrssof self and children).