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`.3839## SAT grids: what ran on M3U96b4041* Launch 1 (01:06 node time): preimage driver 14 workers + collision driver 10 workers, `--deadline 4800`. The first42 launch (00:45) had been killed after 13 min because CaDiCaL-in-pysat ignored the timeout; its CaDiCaL cells were43 discarded, Kissat cells kept (identical code path).44* Collision grid: **264/264 cells, 3 seeds everywhere**, finished in 4363 s (`driver_collision.log`).45* Preimage grid: 450 cells by the deadline (seed 0 complete = 243 cells; seed 1 complete for `first` and z3, partial for46 `spread`), then a completion run (02:33, 24 workers, filter `k == 16 or r <= 16`, 347 s) added seed 2 for every47 cell that was solvable. Final: **572 cells** — 351 cells with 3 seeds, 190 with 2, 31 with 148 (`m3u96b/cells_preimage/skipped_cells.json` lists the 279 cells never started at the deadline; the 157 cells still49 missing a seed are all in rows where every started seed timed out at 300 s: k >= 24 with r >= 20, and `spread` r >= 24).50* Remote aggregation of the preimage grid crashed once because the driver's `skipped_cells.json` was globbed as a cell;51 fixed (aggregators now skip non-cell files) and re-run on the node — both aggregated JSONs carry `host.hostname =52 m3u96b`; per-cell JSONs carry their own hostname.53* Preimage cells: 572/572 SAT answers `verified: true`; collisions: 119/119 `verified: true`.54* Largest solved cells: preimage `first` CaDiCaL r = 64, k = 16 (2/3 seeds, median 262 s), Kissat r = 48, k = 16 (2/3) and55 r = 64 k = 16 (1/3); `spread` CaDiCaL r = 48 k = 16 (3/3, 134 s) and r = 20 k = 32 (2/2, 55 s); z3 r = 12 k = 1656 (128 s). Collisions: r = 18 for all four variants (semi-free-start 7–10 s, standard IV 53–145 s); r >= 20 timeouts;57 r <= 8 UNSAT. Full tables: `results/reduced_round_sha256/summary.json`, `research_log/2026-11-01-sha256.md`.5859### What was reduced relative to the plan6061* Preimage grid: seed 2 (and part of seed 1 for `spread`) only for cells with k = 16 or r <= 16; the rows k >= 24,62 r >= 20 have 2 seeds (`first`, both solvers), the `spread` rows r >= 28 have 1–3 seeds (1 for k >= 24). No row was63 skipped.64* 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 a65 second seed and a 900 s budget (solved in 9.0 s and 52.2 s).66* Nothing else was reduced: diffusion N = 2000 x 3 seeds, bias N = 20 000 x 3 seeds, local-collision 100 000 samples67 per bit.6869## Design notes and gotchas7071* **Preimage free bits.** Placement `first` (as specified: the first k message bits, W_0 LSB-first, then W_1) makes every72 r <= 16 cell solvable by unit propagation alone (0 conflicts): the step function is a bijection and with all other words73 fixed the solver simply inverts the steps from the known target. This is a property of the compression function74 without unknown IV, not a solver feat. A second placement `spread` (bit i -> word i mod 16, CaDiCaL only) was added so75 that the difficulty does not collapse; both are reported.76* **Collisions.** M != M' is restricted to the words an r-step compression reads (W_0..W_{min(r,16)-1}); otherwise a77 difference in an unused word is a trivial "collision" (this happened in the first smoke test). With a shared IV,78 feed-forward does not change the collision event; the two CNFs differ only by the extra adders.79* **Timeouts.** pysat's `interrupt()` does not stop CaDiCaL 1.9.5 in-process; the first launch had to be killed and80 CaDiCaL is now the standalone binary with a real-time limit. CaDiCaL omits statistics lines whose value is 0, which the81 parser maps to 0 (only when the status is SAT/UNSAT).82* **Seeds.** CaDiCaL/Kissat receive `--seed`; the instance (message, target) also depends on the seed for preimage cells.83 Collision cells have no instance randomness (the seed only changes the solver seed).84* Peak RSS is measured per cell (fresh process; `ru_maxrss` of self and children).85