# 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 `first` and z3, partial for
  `spread`), then a completion run (02:33, 24 workers, filter `k == 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.json` lists 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, and `spread` r >= 24).
* Remote aggregation of the preimage grid crashed once because the driver's `skipped_cells.json` was globbed as a cell;
  fixed (aggregators now skip non-cell files) and re-run on the node — both aggregated JSONs carry `host.hostname =
  m3u96b`; per-cell JSONs carry their own hostname.
* Preimage cells: 572/572 SAT answers `verified: true`; collisions: 119/119 `verified: true`.
* Largest solved cells: preimage `first` CaDiCaL r = 64, k = 16 (2/3 seeds, median 262 s), Kissat r = 48, k = 16 (2/3) and
  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 = 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), the `spread` rows 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 placement `spread` (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_maxrss` of self and children).