1# Reduced-round SHA-256 experiments (WP34 Axis C)23All scripts are re-runnable from the repository root with `PYTHONPATH=src .venv/bin/python4experiments/reduced_round_sha256/<script>.py --seed S --out results/reduced_round_sha256/<name>.json`. Every result JSON5is written with `wp34.provenance.record` (host, CPU, RAM, OS, library versions, seed, command, timestamp). The reference6`src/wp34/sha256.py` is never modified; all helpers live here.78| file | role |9|---|---|10| `common.py` | path setup, peak-RSS (`resource.getrusage`), random-oracle control (hashlib over a secret salt), bootstrap CI |11| `diffusion.py` | avalanche of the compression function, steps 1..64, single-bit difference in W_0 / W_5 / W_15 / IV |12| `bias_test.py` | bit bias, input/output linear correlations, byte chi-square for r in {1,...,64} + random-oracle control |13| `cnf_sha256.py` | Tseitin CNF encoder (words = 32 literals, free rotations, Ch/Maj/XOR gates, ripple-carry adders); `--selftest` |14| `solvers.py` | CaDiCaL (binary, `-t`), Kissat (binary, `--time`), z3 bit-vector model; uniform statistics dict |15| `preimage_sat.py` | 3a: preimage cells (r, k, seed, solver, placement); `--list-cells`, `--cell`, `--aggregate` |16| `collision_sat.py` | 3b: collision cells (r, seed, solver, iv fixed/free, feed-forward); same modes |17| `local_collision.py` | 3c: 9-step local collision — GF(2) verification, empirical conformance, SAT conforming pairs |18| `cluster_driver.py` | cell queue runner: one fresh subprocess per cell, N workers, seed-0 phase first, deadline, kill guard |19| `run_cluster.sh` | `setup` / `launch` / `status` / `fetch` on cluster node M3U96b |20| `make_summary.py` | aggregates everything into `results/reduced_round_sha256/summary.json` |21| `../../figures/make_sha256_figures.py` | regenerates `figures/sha256_{diffusion,bias,sat_scaling,collision_scaling,local_collision}.pdf` |22| `../../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 |2324## What ran, where, how long2526| experiment | host | command | runs | wall |27|---|---|---|---|---|28| 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 |29| bias | laptop | `bias_test.py --seed {1,2,3} --n 20000` | 3 seeds x 14 step counts | 7.6 s per seed |30| 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 |31| 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 |32| collision SAT grid | M3U96b | `cluster_driver.py --script collision_sat.py --workers 10 --deadline 4800` | see below | see below |3334Solver binaries copied to `M3U96b:~/wp34/bin/` (kissat 4.0.4 and cadical 3.0.1 from Homebrew, self-contained arm64;35checked with `--version` and a 2-clause instance). Results come back with `run_cluster.sh fetch` into36`results/reduced_round_sha256/m3u96b/` (per-cell JSONs + driver logs) and the two aggregated files are copied to37`results/reduced_round_sha256/{preimage_sat_scaling,collision_sat}.json`.3839GRID-PLACEHOLDER4041## Design notes and gotchas4243* **Preimage free bits.** Placement `first` (as specified: the first k message bits, W_0 LSB-first, then W_1) makes every44 r <= 16 cell solvable by unit propagation alone (0 conflicts): the step function is a bijection and with all other words45 fixed the solver simply inverts the steps from the known target. This is a property of the compression function46 without unknown IV, not a solver feat. A second placement `spread` (bit i -> word i mod 16, CaDiCaL only) was added so47 that the difficulty does not collapse; both are reported.48* **Collisions.** M != M' is restricted to the words an r-step compression reads (W_0..W_{min(r,16)-1}); otherwise a49 difference in an unused word is a trivial "collision" (this happened in the first smoke test). With a shared IV,50 feed-forward does not change the collision event; the two CNFs differ only by the extra adders.51* **Timeouts.** pysat's `interrupt()` does not stop CaDiCaL 1.9.5 in-process; the first launch had to be killed and52 CaDiCaL is now the standalone binary with a real-time limit. CaDiCaL omits statistics lines whose value is 0, which the53 parser maps to 0 (only when the status is SAT/UNSAT).54* **Seeds.** CaDiCaL/Kissat receive `--seed`; the instance (message, target) also depends on the seed for preimage cells.55 Collision cells have no instance randomness (the seed only changes the solver seed).56* Peak RSS is measured per cell (fresh process; `ru_maxrss` of self and children).57