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.
GRID-PLACEHOLDER
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).