WP34 v1.0: SHA-256 grids, Lean layer, complete manuscript (74 p.), hypothesis registry, README

modified README.md +3 −3

				`@@ -28,7 +28,7 @@`
28		28
29	\| Item \| Value \|	29	\| Item \| Value \|
30	\|---\|---\|	30	\|---\|---\|
31	−\| Version \| 1.0 (November 2026) \|	31	+\| Version \| 1.0 (2026-11-01) — 74 pages, 16 figures, 22 tables, 129 references \|
32	\| SSRN \| not yet submitted \|	32	\| SSRN \| not yet submitted \|
33	\| Journal \| — (candidate venues: Journal of Cryptology, DCC, IACR ToSC/TCHES depending on emphasis) \|	33	\| Journal \| — (candidate venues: Journal of Cryptology, DCC, IACR ToSC/TCHES depending on emphasis) \|
34	\| Code & data \| fully reproducible from this repository (synthetic instances only; see Appendix A of the paper) \|	34	\| Code & data \| fully reproducible from this repository (synthetic instances only; see Appendix A of the paper) \|
				`@@ -65,8 +65,8 @@ sG = R + eP (BIP340); H(x) = y (SHA-256, 64 steps)`
65	\| Preprocessing \| online cost 1.5·√(n/T); per-instance speed-up up to 42× \| known, reproduced \|	65	\| Preprocessing \| online cost 1.5·√(n/T); per-instance speed-up up to 42× \| known, reproduced \|
66	\| BIP340 batch verification \| 7.9 µs/sig at b = 2048, 3.10× [3.05, 3.16] vs single (k256); saturation explained \| known, reproduced \|	66	\| BIP340 batch verification \| 7.9 µs/sig at b = 2048, 3.10× [3.05, 3.16] vs single (k256); saturation explained \| known, reproduced \|
67	\| Implementations \| pure Python 7.4 ms vs libsecp256k1 13.2 µs per Schnorr verify (560×) \| empirical \|	67	\| Implementations \| pure Python 7.4 ms vs libsecp256k1 13.2 µs per Schnorr verify (560×) \| empirical \|
68	−\| SHA-256 reduced steps \| see `results/reduced_round_sha256/summary.json` and paper §10.9 \| empirical / known \|	68	+\| SHA-256 reduced steps \| full diffusion at step 6 (W_0), no first-order regularity from step 5; generic SAT: preimages only with 16 free bits beyond 16 steps, collisions up to 18 steps (UNSAT for ≤ 8), 9-step local collision reproduced (conforming pairs for all 32 bit positions) \| empirical / known \|
69	−\| Lean 4 \| SHA-256 word identities, step bijection, schedule inversion, linearised local collision, ECDSA malleability, Schnorr correctness (see `formal/README.md`) \| machine-checked \|	69	+\| Lean 4 (32 s build, no sorry) \| Ch/Maj identities, linearity and bijectivity of Σ0, Σ1, σ0, σ1 (refuting our conjecture that σ0/σ1 are singular), step bijection, schedule inversion, 9-step linearised local collision, ECDSA malleability, Schnorr correctness \| machine-checked \|
70		70
71	## 🗂 Repository layout	71	## 🗂 Repository layout
72		72

modified experiments/automated_discovery/registry.py +15 −1

+ def tex_escape(s: str) -> str:
++    s = s.replace("π̄", r"$\bar\pi$").replace("\u0304", "").replace("^", r"\^{}").replace("~", r"\textasciitilde{}")
++    for a, b in [("&", r"\&"), ("%", r"\%"), ("_", r"\_"), ("#", r"\#"), ("√", r"$\surd$"), ("≈", r"$\approx$"), ("≤", r"$\le$"), ("≥", r"$\ge$"),
++                 ("→", r"$\to$"), ("⟹", r"$\Rightarrow$"), ("×", r"$\times$"), ("²", r"$^2$"), ("³", r"$^3$"), ("Ω", r"$\Omega$"), ("φ", r"$\varphi$"), ("λ", r"$\lambda$"),
++                 ("β", r"$\beta$"), ("Σ", r"$\Sigma$"), ("σ", r"$\sigma$"), ("δ", r"$\delta$"), ("π", r"$\pi$"), ("ω", r"$\omega$"), ("χ", r"$\chi$"), ("α", r"$\alpha$"),
++                 ("−", "--"), ("–", "--"), ("—", "---"), ("·", r"$\cdot$"), ("∈", r"$\in$"), ("⊕", r"$\oplus$"), ("≡", r"$\equiv$"), ("∞", r"$\infty$"), ("ℓ", r"$\ell$"),
++                 ("ε", r"$\varepsilon$"), ("≠", r"$\ne$"), ("∘", r"$\circ$"), ("‖", r"$\|$"), ("⁻¹", r"$^{-1}$"), ("⁻⁴", r"$^{-4}$"), ("⁻⁵", r"$^{-5}$"), ("⁴", r"$^4$"), ("⁵", r"$^5$"),
++                 ("₀", r"$_0$"), ("₁", r"$_1$"), ("₂", r"$_2$"), ("±", r"$\pm$"), ("…", r"\ldots{}"), ("µ", r"$\mu$"), ("•", r"$\cdot$"), ("≫", r"$\gg$"), ("≪", r"$\ll$"), ("′", "'"), ("ô", "\\^o"), ("Ø", "O")]:
++        s = s.replace(a, b)
++    greek = {"θ": "theta", "γ": "gamma", "μ": "mu", "ν": "nu", "ρ": "rho", "τ": "tau", "κ": "kappa", "η": "eta", "ζ": "zeta", "ξ": "xi", "ψ": "psi", "Δ": "Delta", "Γ": "Gamma", "Θ": "Theta", "Λ": "Lambda", "Π": "Pi", "Φ": "Phi", "Ψ": "Psi"}
++    for a, b in greek.items():
++        s = s.replace(a, "$\\" + b + "$")
++    bad = sorted({c for c in s if ord(c) > 127 and c not in "éèàçêôûîïüöäñÉÈ"})
++    if bad:
++        print("WARNING tex_escape: unmapped characters", bad)
++    return s
+ def main():

modified experiments/reduced_round_sha256/README.md +29 −1

+ `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

modified experiments/reduced_round_sha256/cluster_driver.py +3 −0

				`@@ -31,11 +31,14 @@ def main():`
31	ap.add_argument("--timeout", type=float, default=None)	31	ap.add_argument("--timeout", type=float, default=None)
32	ap.add_argument("--list-args", default="")	32	ap.add_argument("--list-args", default="")
33	ap.add_argument("--python", default=sys.executable)	33	ap.add_argument("--python", default=sys.executable)
		34	+ ap.add_argument("--filter", default="", help="python expression over the cell dict c, e.g. \"c['k']==16 or c['r']<=16\"")
34	a = ap.parse_args()	35	a = ap.parse_args()
35	script = str(HERE / a.script)	36	script = str(HERE / a.script)
36	cells_dir = pathlib.Path(a.cells_dir); cells_dir.mkdir(parents=True, exist_ok=True)	37	cells_dir = pathlib.Path(a.cells_dir); cells_dir.mkdir(parents=True, exist_ok=True)
37	lst = subprocess.run([a.python, script, "--list-cells"] + a.list_args.split(), capture_output=True, text=True, check=True)	38	lst = subprocess.run([a.python, script, "--list-cells"] + a.list_args.split(), capture_output=True, text=True, check=True)
38	cells = [json.loads(l) for l in lst.stdout.splitlines() if l.strip()]	39	cells = [json.loads(l) for l in lst.stdout.splitlines() if l.strip()]
		40	+ if a.filter:
		41	+ cells = [c for c in cells if eval(a.filter, {}, {"c": c})]
39	# phases: seed 0 first (all cells), then seeds 1, 2, ...; inside a phase by cost	42	# phases: seed 0 first (all cells), then seeds 1, 2, ...; inside a phase by cost
40	cells.sort(key=lambda c: (c["seed"], cost(c)))	43	cells.sort(key=lambda c: (c["seed"], cost(c)))
41	todo = [c for c in cells if not (cells_dir / (cell_name(c) + ".json")).exists()]	44	todo = [c for c in cells if not (cells_dir / (cell_name(c) + ".json")).exists()]

modified experiments/reduced_round_sha256/collision_sat.py +1 −1

				`@@ -80,7 +80,7 @@ def run_cell(cell: dict, timeout: float) -> dict:`
80		80
81		81
82	def aggregate(d: str, out: str, started: float):	82	def aggregate(d: str, out: str, started: float):
83	− cells = [json.loads(p.read_text()) for p in sorted(pathlib.Path(d).glob("*.json"))]	83	+ cells = [c for c in (json.loads(p.read_text()) for p in sorted(pathlib.Path(d).glob("*.json"))) if isinstance(c, dict) and "cell" in c]
84	summary = {}	84	summary = {}
85	for iv, ff in VARIANTS:	85	for iv, ff in VARIANTS:
86	for sol in ("cadical", "kissat"):	86	for sol in ("cadical", "kissat"):

modified experiments/reduced_round_sha256/preimage_sat.py +3 −1

				`@@ -112,7 +112,9 @@ def run_cell(cell: dict, timeout: float) -> dict:`
112	def aggregate(d: str, out: str, started: float):	112	def aggregate(d: str, out: str, started: float):
113	cells = []	113	cells = []
114	for p in sorted(pathlib.Path(d).glob("*.json")):	114	for p in sorted(pathlib.Path(d).glob("*.json")):
115	− cells.append(json.loads(p.read_text()))	115	+ doc = json.loads(p.read_text())
		116	+ if isinstance(doc, dict) and "cell" in doc: # skip the driver's skipped_cells.json
		117	+ cells.append(doc)
116	summary = {}	118	summary = {}
117	for placement in ("first", "spread"):	119	for placement in ("first", "spread"):
118	for sol in ("cadical", "kissat", "z3"):	120	for sol in ("cadical", "kissat", "z3"):

modified figures/make_sha256_figures.py +13 −11

				`@@ -116,17 +116,17 @@ def fig_sat_scaling():`
116	_censored_plot(ax, [r for r, _ in cells], [max(c["median_wall_s"], 1e-3) for _, c in cells],	116	_censored_plot(ax, [r for r, _ in cells], [max(c["median_wall_s"], 1e-3) for _, c in cells],
117	[c["solved_fraction"] for _, c in cells], T, cmap(i / (len(ks) - 1)), "o" if sol == "cadical" else "^",	117	[c["solved_fraction"] for _, c in cells], T, cmap(i / (len(ks) - 1)), "o" if sol == "cadical" else "^",
118	"-" if sol == "cadical" else "--", "$k$ = %d" % k)	118	"-" if sol == "cadical" else "--", "$k$ = %d" % k)
119	− if pl == "first" and sol == "cadical":	119	+ if pl == "first" and sol == "cadical": # z3 bit-vector runs on r<=16, k<=32 overlaid on panel (a)
120	for i, k in enumerate([16, 24, 32]):	120	for i, k in enumerate([16, 24, 32]):
121	cells = [(r, S.get(f"z3:r{r}:k{k}")) for r in rs]; cells = [(r, c) for r, c in cells if c]	121	cells = [(r, S.get(f"z3:r{r}:k{k}")) for r in rs]; cells = [(r, c) for r, c in cells if c]
122	if cells:	122	if cells:
123	_censored_plot(ax, [r for r, _ in cells], [max(c["median_wall_s"], 1e-3) for _, c in cells],	123	_censored_plot(ax, [r for r, _ in cells], [max(c["median_wall_s"], 1e-3) for _, c in cells],
124	− [c["solved_fraction"] for _, c in cells], T, cmap(i / (len(ks) - 1)), "x", ":", "z3 $k$ = %d" % k if i == 0 else None)	124	+ [c["solved_fraction"] for _, c in cells], T, cmap(i / (len(ks) - 1)), "x", ":", "z3, $k$ = %d" % k)
125	ax.axhline(T, color="k", ls=":", lw=0.7); ax.text(rs[0], T * 1.6, "timeout (open = median unsolved)", fontsize=6.5)	125	ax.axhline(T, color="k", ls=":", lw=0.7); ax.text(rs[0], T * 1.6, "timeout (open = median unsolved)", fontsize=6.5)
126	ax.set_yscale("log"); ax.set_xlabel("steps $r$"); ax.set_title(title, fontsize=8.5); ax.set_xticks(rs); ax.tick_params(axis="x", labelsize=6.5)	126	ax.set_yscale("log"); ax.set_xlabel("steps $r$"); ax.set_title(title, fontsize=8.5); ax.set_xticks(rs); ax.tick_params(axis="x", labelsize=6.5)
127	axs[0].set_ylabel("median wall time (s)"); axs[0].set_ylim(1e-3, T * 3)	127	axs[0].set_ylabel("median wall time (s)"); axs[0].set_ylim(1e-3, T * 3)
128	− axs[0].legend(frameon=False, ncol=2, loc="lower right", fontsize=6)	128	+ axs[0].legend(frameon=False, ncol=2, loc="lower right", fontsize=5.5)
129	− fig.suptitle("Preimage of $r$-step SHA-256 compression with $k$ free message bits (3 seeds per cell, timeout %d s)" % T, fontsize=9, y=1.0)	129	+ fig.suptitle("Preimage of $r$-step SHA-256 compression with $k$ free message bits (median over 1-3 seeds per cell, timeout %d s)" % T, fontsize=9, y=1.0)
130	fig.tight_layout(); fig.savefig(FIG / "sha256_sat_scaling.pdf", bbox_inches="tight"); plt.close(fig)	130	fig.tight_layout(); fig.savefig(FIG / "sha256_sat_scaling.pdf", bbox_inches="tight"); plt.close(fig)
131		131
132		132
				`@@ -137,21 +137,23 @@ def fig_collision_scaling():`
137	S = d["measurements"]["summary"]; T = d["params"]["timeout_s"]; rs = d["params"]["r_list"]	137	S = d["measurements"]["summary"]; T = d["params"]["timeout_s"]; rs = d["params"]["r_list"]
138	fig, axs = plt.subplots(1, 2, figsize=(7.2, 2.7), sharey=True)	138	fig, axs = plt.subplots(1, 2, figsize=(7.2, 2.7), sharey=True)
139	for ax, sol in zip(axs, ["cadical", "kissat"]):	139	for ax, sol in zip(axs, ["cadical", "kissat"]):
		140	+ unsat_r = set()
140	for (iv, ff), color, mk in [(("fixed", False), C["cadical"], "o"), (("fixed", True), C["cadical"], "s"),	141	for (iv, ff), color, mk in [(("fixed", False), C["cadical"], "o"), (("fixed", True), C["cadical"], "s"),
141	(("free", False), C["kissat"], "o"), (("free", True), C["kissat"], "s")]:	142	(("free", False), C["kissat"], "o"), (("free", True), C["kissat"], "s")]:
142	cells = [(r, S.get(f"{sol}:iv_{iv}:ff{int(ff)}:r{r}")) for r in rs]; cells = [(r, c) for r, c in cells if c]	143	cells = [(r, S.get(f"{sol}:iv_{iv}:ff{int(ff)}:r{r}")) for r in rs]; cells = [(r, c) for r, c in cells if c]
143	if not cells:	144	if not cells:
144	continue	145	continue
145	− _censored_plot(ax, [r for r, _ in cells], [max(c["median_wall_s"], 1e-3) for _, c in cells],	146	+ resolved = [(c["n_sat"] + c.get("n_unsat", 0)) / c["n_runs"] for _, c in cells]
146	− [c["solved_fraction"] for _, c in cells], T, color, mk, "-" if not ff else "--",	147	+ _censored_plot(ax, [r for r, _ in cells], [max(c["median_wall_s"], 1e-3) for _, c in cells], resolved, T, color, mk,
147	− ("standard IV" if iv == "fixed" else "semi-free-start") + (", feed-forward" if ff else ""))	148	+ "-" if not ff else "--", ("standard IV" if iv == "fixed" else "semi-free-start") + (", feed-forward" if ff else ""))
148	− for r, c in cells: # mark proven UNSAT cells	149	+ unsat_r \|= {r for r, c in cells if c.get("n_unsat", 0) == c["n_runs"]}
149	− if c.get("n_unsat", 0) > 0 or c.get("all_unsat"):	150	+ if unsat_r:
150	− ax.annotate("UNSAT", (r, max(c["median_wall_s"], 1e-3)), fontsize=5.5, textcoords="offset points", xytext=(0, 4), ha="center")	151	+ ax.axvspan(min(unsat_r) - 1, max(unsat_r) + 1, color="#f4d03f", alpha=0.18, lw=0)
		152	+ ax.text((min(unsat_r) + max(unsat_r)) / 2, 2e-3, "no collision\n(UNSAT proved,\nall seeds)", ha="center", fontsize=6.5)
151	ax.axhline(T, color="k", ls=":", lw=0.7); ax.set_yscale("log"); ax.set_xlabel("steps $r$"); ax.set_xticks(rs)	153	ax.axhline(T, color="k", ls=":", lw=0.7); ax.set_yscale("log"); ax.set_xlabel("steps $r$"); ax.set_xticks(rs)
152	ax.set_title({"cadical": "(a) CaDiCaL", "kissat": "(b) Kissat"}[sol], fontsize=9)	154	ax.set_title({"cadical": "(a) CaDiCaL", "kissat": "(b) Kissat"}[sol], fontsize=9)
153	axs[0].set_ylabel("median wall time (s)"); axs[0].set_ylim(1e-3, T * 3); axs[0].legend(frameon=False, fontsize=6.5, loc="lower right")	155	axs[0].set_ylabel("median wall time (s)"); axs[0].set_ylim(1e-3, T * 3); axs[0].legend(frameon=False, fontsize=6.5, loc="lower right")
154	− fig.suptitle("Collision search on $r$-step SHA-256 compression (timeout %d s; open markers = majority unsolved)" % T, fontsize=9, y=1.0)	156	+ fig.suptitle("Collision search on $r$-step SHA-256 compression, 3 seeds per cell (timeout %d s; open markers = majority unresolved)" % T, fontsize=9, y=1.0)
155	fig.tight_layout(); fig.savefig(FIG / "sha256_collision_scaling.pdf", bbox_inches="tight"); plt.close(fig)	157	fig.tight_layout(); fig.savefig(FIG / "sha256_collision_scaling.pdf", bbox_inches="tight"); plt.close(fig)
156		158
157		159

modified figures/sha256_bias.pdf +0 −0

Binary file not shown.

added figures/sha256_collision_scaling.pdf +0 −0

Binary file not shown.

modified figures/sha256_diffusion.pdf +0 −0

Binary file not shown.

modified figures/sha256_local_collision.pdf +0 −0

Binary file not shown.

added figures/sha256_sat_scaling.pdf +0 −0

Binary file not shown.

modified hypotheses/H15-a-single-bit-message-difference-reaches-full-ava.md +7 −4

				`@@ -14,10 +14,13 @@ related_work:`
14	possible_counterexamples: Flip ratio plateauing below 0.5 (would indicate a structural weakness).	14	possible_counterexamples: Flip ratio plateauing below 0.5 (would indicate a structural weakness).
15	verification_strategy: experiments/reduced_round_sha256/diffusion.py	15	verification_strategy: experiments/reduced_round_sha256/diffusion.py
16	computational_budget: minutes	16	computational_budget: minutes
17	−status: running	17	+status: evaluated
18	−classification: pending	18	+classification: known_reproduced
19	−evidence: []	19	+evidence:
20	−verdict: pending	20	+- results/reduced_round_sha256/summary.json
		21	+- results/reduced_round_sha256/diffusion_seed1.json
		22	+verdict: Full diffusion (mean flip ratio ≥ 0.49) at step 6 for a W_0 bit, 11 for W_5, 21 for W_15 (6 steps after entry), 8
		23	+ for an IV bit; identical over 3 seeds × 2000 messages; after 64 steps Hamming weight 128.0 ± 8.1 = random-oracle control.
21	---	24	---
22		25
23	# H15 — A single-bit message difference reaches full avalanche within a small number of steps	26	# H15 — A single-bit message difference reaches full avalanche within a small number of steps

modified hypotheses/H16-statistically-detectable-input-output-correlatio.md +8 −4

				`@@ -14,10 +14,14 @@ related_work:`
14	possible_counterexamples: Residual correlations at 64 steps.	14	possible_counterexamples: Residual correlations at 64 steps.
15	verification_strategy: experiments/reduced_round_sha256/bias_test.py	15	verification_strategy: experiments/reduced_round_sha256/bias_test.py
16	computational_budget: minutes	16	computational_budget: minutes
17	−status: running	17	+status: evaluated
18	−classification: pending	18	+classification: empirical_observation
19	−evidence: []	19	+evidence:
20	−verdict: pending	20	+- results/reduced_round_sha256/summary.json
		21	+- results/reduced_round_sha256/bias_seed1.json
		22	+verdict: 'N = 20 000 × 3 seeds: r ≤ 3 trivially biased (untouched IV registers); r = 4 bias/χ² at noise but 6–13 \|corr\| =
		23	+ 1 pairs (LSB of e_1 affine in LSB of W_0); from r = 5 all statistics at the random-oracle floor through r = 64 (two isolated
		24	+ 4.1σ bits in 10 752 tests, as expected by chance).'
21	---	25	---
22		26
23	# H16 — Statistically detectable input–output correlations vanish after a small number of steps	27	# H16 — Statistically detectable input–output correlations vanish after a small number of steps

modified hypotheses/H17-sat-preimage-search-on-step-reduced-sha-256-scal.md +9 −4

				`@@ -17,10 +17,15 @@ related_work:`
17	possible_counterexamples: Sub-exponential growth (would be surprising and would need explanation).	17	possible_counterexamples: Sub-exponential growth (would be surprising and would need explanation).
18	verification_strategy: experiments/reduced_round_sha256/preimage_sat.py on M3U96b	18	verification_strategy: experiments/reduced_round_sha256/preimage_sat.py on M3U96b
19	computational_budget: ≈ 3 node-hours	19	computational_budget: ≈ 3 node-hours
20	−status: running	20	+status: evaluated
21	−classification: pending	21	+classification: empirical_observation
22	−evidence: []	22	+evidence:
23	−verdict: pending	23	+- results/reduced_round_sha256/summary.json
		24	+- results/reduced_round_sha256/preimage_sat_scaling.json
		25	+verdict: '572 cells, all SAT answers re-hashed. r ≤ 16: solved by propagation (0 conflicts, ≤ 0.03 s) for any k. r ≥ 20: only
		26	+ k = 16 solved (CaDiCaL 6.4 s at r = 20, 87 s at r = 32, 262 s at r = 64 for 2/3 seeds); every k ≥ 24 cell times out at 300
		27	+ s; Z3 2–4 orders of magnitude slower and times out at r ≥ 16. Generic SAT is slower than 2^16 brute force once the expansion
		28	+ matters.'
24	---	29	---
25		30
26	# H17 — SAT preimage search on step-reduced SHA-256 scales exponentially in the number of steps and in the number of free bits	31	# H17 — SAT preimage search on step-reduced SHA-256 scales exponentially in the number of steps and in the number of free bits

modified hypotheses/H18-generic-sat-encodings-find-step-reduced-collisio.md +9 −4

				`@@ -22,10 +22,15 @@ related_work:`
22	possible_counterexamples: SAT reaching ≥ 24 steps unaided (would be notable).	22	possible_counterexamples: SAT reaching ≥ 24 steps unaided (would be notable).
23	verification_strategy: experiments/reduced_round_sha256/collision_sat.py	23	verification_strategy: experiments/reduced_round_sha256/collision_sat.py
24	computational_budget: ≈ 3 node-hours	24	computational_budget: ≈ 3 node-hours
25	−status: running	25	+status: evaluated
26	−classification: pending	26	+classification: known_reproduced
27	−evidence: []	27	+evidence:
28	−verdict: pending	28	+- results/reduced_round_sha256/summary.json
		29	+- results/reduced_round_sha256/collision_sat.json
		30	+verdict: '264 cells, 119 collisions verified. r = 4, 6, 8: UNSAT in all variants/solvers/seeds (72 runs) — no collision within
		31	+ the words an 8-step compression reads. r = 10–16: 0-conflict collisions differing in exactly 9 consecutive words (a terminal
		32	+ local collision). r = 18: 53 s standard IV, 7–10 s semi-free-start. r ≥ 20: all timeouts. Largest 18 steps vs 28 (pure SAT,
		33	+ Alamgir et al. 2024), 31 (Li et al. 2024), 39 SFS.'
29	---	34	---
30		35
31	# H18 — Generic SAT encodings find step-reduced collisions only far below the published dedicated-tool records	36	# H18 — Generic SAT encodings find step-reduced collisions only far below the published dedicated-tool records

modified hypotheses/H19-the-9-step-local-collision-holds-with-probabilit.md +10 −4

				`@@ -17,10 +17,16 @@ related_work:`
17	possible_counterexamples: Linearised cancellation failing for some δ (ruled out by bv_decide).	17	possible_counterexamples: Linearised cancellation failing for some δ (ruled out by bv_decide).
18	verification_strategy: experiments/reduced_round_sha256/local_collision.py + formal/ Lean theorem.	18	verification_strategy: experiments/reduced_round_sha256/local_collision.py + formal/ Lean theorem.
19	computational_budget: minutes	19	computational_budget: minutes
20	−status: running	20	+status: evaluated
21	−classification: pending	21	+classification: known_reproduced
22	−evidence: []	22	+evidence:
23	−verdict: pending	23	+- results/reduced_round_sha256/summary.json
		24	+- results/reduced_round_sha256/local_collision.json
		25	+- formal/README.md
		26	+verdict: 'Pattern (δ, Σ0δ⊕Σ1δ, Σ1(Σ0δ), 0, δ, Σ0δ⊕Σ1δ, 0, 0, δ) cancels in the linearised model for all δ (GF(2) check + Lean
		27	+ theorem localCollision_absorb). Real step: 0 collisions in 32 × 100 000 samples (bound 3·10⁻⁵); survival after step i 0.25
		28	+ (bits 0–30) / 1.0 (bit 31), after i+1 ≈ 10⁻⁴, after i+2 zero. SAT finds conforming pairs for all 32 positions in 4.4–118
		29	+ s, all verified.'
24	---	30	---
25		31
26	# H19 — The 9-step local collision holds with probability 1 in the XOR-linearised model and with low, position-dependent probability in the real step function	32	# H19 — The 9-step local collision holds with probability 1 in the XOR-linearised model and with low, position-dependent probability in the real step function

modified hypotheses/H24-the-six-stage-pipeline-rediscovers-known-structu.md +9 −4

				`@@ -16,10 +16,15 @@ related_work:`
16	possible_counterexamples: A validated novel result (none).	16	possible_counterexamples: A validated novel result (none).
17	verification_strategy: experiments/automated_discovery/registry.py	17	verification_strategy: experiments/automated_discovery/registry.py
18	computational_budget: none	18	computational_budget: none
19	−status: running	19	+status: evaluated
20	−classification: pending	20	+classification: empirical_observation
21	−evidence: []	21	+evidence:
22	−verdict: pending	22	+- research_log/discovery_log.jsonl
		23	+- results/automated_discovery/hypothesis_summary.json
		24	+verdict: '25 hypotheses evaluated: 16 known results reproduced with measured constants, 6 empirical observations, 3 rejected
		25	+ conjectures (orbit quotient group; iteration-function shortcut; non-injectivity of σ0/σ1), 0 new verified results, 0 claims
		26	+ of weakness. Automation found one unrecorded closed form (GLV constants) and one wrong belief (σ0/σ1); the baseline (literature
		27	+ reading) would have left every constant unmeasured.'
23	---	28	---
24		29
25	# H24 — The six-stage pipeline rediscovers known structure at a high rate and reports zero validated novel shortcuts	30	# H24 — The six-stage pipeline rediscovers known structure at a high rate and reports zero validated novel shortcuts

modified paper/appendix/appendix.tex +17 −14

				`@@ -11,8 +11,8 @@`
11	\section{Reproducibility statement}	11	\section{Reproducibility statement}
12	\label{app:repro}	12	\label{app:repro}
13		13
14	−The repository \code{wp34\_uqo} (UQO working-paper series, \code{mathematiques/beyond-square-root-barrier}) contains	14	+The repository \code{wp34\_uqo} (series directory \code{beyond-square-root-barrier} under \code{mathematiques/})
15	−every script, result file and figure source. All experiments are re-runnable from the repository root:	15	+contains every script, result file and figure source. All experiments are re-runnable from the repository root:
16	\begin{lstlisting}	16	\begin{lstlisting}
17	uv venv --python 3.12 .venv && uv pip install -r requirements.txt # Python environment	17	uv venv --python 3.12 .venv && uv pip install -r requirements.txt # Python environment
18	.venv/bin/python -m pytest -q tests/ # cross-implementation gates	18	.venv/bin/python -m pytest -q tests/ # cross-implementation gates
				`@@ -24,12 +24,16 @@ uv venv --python 3.12 .venv && uv pip install -r requirements.txt # Python`
24	.venv/bin/python experiments/synthetic_ecdlp/preprocessing_python.py # H12	24	.venv/bin/python experiments/synthetic_ecdlp/preprocessing_python.py # H12
25	.venv/bin/python experiments/automated_discovery/identity_search.py # H02, H07	25	.venv/bin/python experiments/automated_discovery/identity_search.py # H02, H07
26	cargo build --release --manifest-path experiments/synthetic_ecdlp/rho_engine/Cargo.toml	26	cargo build --release --manifest-path experiments/synthetic_ecdlp/rho_engine/Cargo.toml
27	−.venv/bin/python experiments/synthetic_ecdlp/run_scaling.py --sizes 20,24,28,32,36,40 # H08-H11 (see README for the cluster split)	27	+.venv/bin/python experiments/synthetic_ecdlp/ecdlp_study.py all # job files (PARI/GP)
28	−cargo run --release --manifest-path experiments/signature_benchmarks/sigbench/Cargo.toml -- ... # H13-H14 (run_bench.py)	28	+.venv/bin/python experiments/synthetic_ecdlp/run_batch_remote.py ... # H04, H08-H11 (see README)
29	−.venv/bin/python experiments/reduced_round_sha256/diffusion.py / bias_test.py / preimage_sat.py / collision_sat.py / local_collision.py	29	+.venv/bin/python experiments/synthetic_ecdlp/analyze_ecdlp.py
		30	+.venv/bin/python experiments/signature_benchmarks/run_bench.py # H13-H14 (builds sigbench)
		31	+.venv/bin/python experiments/reduced_round_sha256/diffusion.py # H15 (also bias_test.py,
		32	+ preimage_sat.py, collision_sat.py, local_collision.py; run_cluster.sh) # H16-H19
30	cd formal && lake build # H21, H22, H25 (Lean 4.35)	33	cd formal && lake build # H21, H22, H25 (Lean 4.35)
31	−.venv/bin/python experiments/automated_discovery/registry.py # discovery log + Table of hypotheses	34	+.venv/bin/python experiments/automated_discovery/registry.py # discovery log + hypothesis table
32	−.venv/bin/python scripts/make_tables.py && cd paper && make # tables/numbers.tex, main.pdf	35	+.venv/bin/python scripts/make_tables.py scripts/make_sha_tables.py # tables/numbers*.tex
		36	+cd paper && make # main.pdf
33	\end{lstlisting}	37	\end{lstlisting}
34	Every result JSON carries a provenance block (host name, CPU, cores, RAM, OS, Python and library versions, seed,	38	Every result JSON carries a provenance block (host name, CPU, cores, RAM, OS, Python and library versions, seed,
35	command line, UTC timestamp, elapsed time). Random seeds are fixed in the scripts (default 34) and recorded.	39	command line, UTC timestamp, elapsed time). Random seeds are fixed in the scripts (default 34) and recorded.
				`@@ -40,10 +44,10 @@ Raw solver outputs and the Rust batch outputs are kept next to the aggregated fi`
40		44
41	\begin{table}[htbp]	45	\begin{table}[htbp]
42	\centering\footnotesize	46	\centering\footnotesize
43	− \begin{threeparttable}	47	+ \caption{Hardware and software used (measured, from the provenance blocks).}
44	− \caption{Hardware and software used (measured, from the provenance blocks).}
45	\label{tab:env}	48	\label{tab:env}
46	− \begin{tabular}{@{}llllll@{}}	49	+ {\footnotesize
		50	+ \begin{tabular}{@{}p{2.6cm}p{2.4cm}p{2.1cm}rrp{5.2cm}@{}}
47	\toprule	51	\toprule
48	Role & Machine & CPU & Cores & RAM & Used for \\	52	Role & Machine & CPU & Cores & RAM & Used for \\
49	\midrule	53	\midrule
				`@@ -52,10 +56,9 @@ Raw solver outputs and the Rust batch outputs are kept next to the aggregated fi`
52	benchmarking & M3U96b (Mac Studio) & Apple M3 Ultra & 28 & 96 GB & SAT/SMT grids, ECDLP scaling \\	56	benchmarking & M3U96b (Mac Studio) & Apple M3 Ultra & 28 & 96 GB & SAT/SMT grids, ECDLP scaling \\
53	\bottomrule	57	\bottomrule
54	\end{tabular}	58	\end{tabular}
55	− \begin{tablenotes}\footnotesize	59	+ }
56	− \item Software: macOS 27.0; Python 3.12 (uv), SymPy 1.14, NumPy 2.5, python-sat 1.9 (CaDiCaL 1.9.5 bindings), Z3 4.15 (\code{z3-solver}), CaDiCaL 2.x and Kissat 4.x binaries, PARI/GP 2.19; Rust 1.95--1.96 (\code{k256} 0.14, \code{secp256k1} 0.33 / \libsecp{}); Lean 4.35.0 (\code{bv\_decide} with bundled CaDiCaL); TeX Live 2026. Exact versions are in each result file. No GPU was used.	60	+ \par\smallskip{\footnotesize Software: macOS 27.0; Python 3.12 (uv), SymPy 1.14, NumPy 2.5, python-sat 1.9 (CaDiCaL 1.9.5 bindings), Z3 4.15 (\code{z3-solver}), CaDiCaL 2.x and Kissat 4.x binaries, PARI/GP 2.19; Rust 1.95--1.96 (\code{k256} 0.14, \code{secp256k1} 0.33 / \libsecp{}); Lean 4.35.0 (\code{bv\_decide} with bundled CaDiCaL); TeX Live 2026. Exact versions are in each result file. No GPU was used.}
57	− \end{tablenotes}	61	+
58	− \end{threeparttable}
59	\end{table}	62	\end{table}
60		63
61	\section{Full secp256k1 constants}	64	\section{Full secp256k1 constants}

added paper/figures/sha256_bias.pdf +0 −0

Binary file not shown.

added paper/figures/sha256_collision_scaling.pdf +0 −0

Binary file not shown.

added paper/figures/sha256_diffusion.pdf +0 −0

Binary file not shown.

added paper/figures/sha256_local_collision.pdf +0 −0

Binary file not shown.

added paper/figures/sha256_sat_scaling.pdf +0 −0

Binary file not shown.

modified paper/main.pdf +0 −0

Binary file not shown.

modified paper/main.tex +2 −1

				`@@ -44,7 +44,7 @@`
44	\usepackage{algorithm}	44	\usepackage{algorithm}
45	\usepackage{algpseudocode}	45	\usepackage{algpseudocode}
46	\usepackage{listings}	46	\usepackage{listings}
47	−\lstset{basicstyle=\ttfamily\footnotesize,breaklines=true,columns=fullflexible,frame=single,framerule=0.2pt}	47	+\lstset{basicstyle=\ttfamily\scriptsize,breaklines=true,columns=fullflexible,frame=single,framerule=0.2pt}
48		48
49	\theoremstyle{plain}	49	\theoremstyle{plain}
50	\newtheorem{theorem}{Theorem}[section]	50	\newtheorem{theorem}{Theorem}[section]
				`@@ -94,6 +94,7 @@`
94	% Numbers generated by scripts (never typed by hand): paper/tables/numbers.tex	94	% Numbers generated by scripts (never typed by hand): paper/tables/numbers.tex
95	\input{tables/numbers}	95	\input{tables/numbers}
96	\input{tables/numbers_ecdlp}	96	\input{tables/numbers_ecdlp}
		97	+\input{tables/numbers_sha}
97		98
98	% ============================================================================	99	% ============================================================================
99	\newcommand{\WPnumber}{34}	100	\newcommand{\WPnumber}{34}

modified paper/sections/01_introduction.tex +1 −1

				@@ -36,7 +36,7 @@ the most natural ``beyond $\sqrt6$'' idea, and we quantify why summation-polynom
36	$\sqrt n$ over prime fields.	36	$\sqrt n$ over prime fields.
37		37
38	\emph{Algorithmic complexity (known results reproduced with precise constants; one rejected shortcut).} A native	38	\emph{Algorithmic complexity (known results reproduced with precise constants; one rejected shortcut).} A native
39	−engine solved $6\,000$ synthetic ECDLP instances of 20--56 bits, all verified. The fitted exponents are	39	+engine solved $6\,240$ synthetic ECDLP instances of 20--56 bits, all verified. The fitted exponents are
40	$0.48$--$0.50$; the rho constant is $1.254\sqrt n$ against the random-mapping prediction $1.2533$; the order-6	40	$0.48$--$0.50$; the rho constant is $1.254\sqrt n$ against the random-mapping prediction $1.2533$; the order-6
41	automorphism classes reduce iterations by $2.42\times$ ($\sqrt6=2.449$) but, in our implementation, save no wall-clock	41	automorphism classes reduce iterations by $2.42\times$ ($\sqrt6=2.449$) but, in our implementation, save no wall-clock
42	time because canonicalisation costs as much as a group addition---a point the literature's record computations	42	time because canonicalisation costs as much as a group addition---a point the literature's record computations

modified paper/sections/02_foundations.tex +25 −0

+   \label{fig:depmap}
+ \end{figure}
++Table~\ref{tab:primitives} lists the primitives, the assumption each rests on and the generic security level that
++the assumption provides.
++
++\begin{table}[htbp]
++  \centering\footnotesize
++      \caption{Cryptographic primitives of Bitcoin, their hardness assumptions and generic security levels.}
++    \label{tab:primitives}
++  \resizebox{\textwidth}{!}{%
++    \begin{tabular}{@{}llllp{4.2cm}@{}}
++      \toprule
++      Primitive & Mathematical object & Assumption & Generic cost & Used for \\
++      \midrule
++      \secp{} group & $E(\F_p)$, $y^2=x^3+7$, $\#E=n$ prime & ECDLP & $\sqrt{\pi n/12}\approx 2^{127.0}$ (rho + automorphisms) & key pairs, all signatures \\
++      ECDSA & $(r,s)$ with $s=k^{-1}(z+rd)$ & ECDLP + conversion-function idealisation & as above & legacy and SegWit v0 spends \\
++      BIP340 Schnorr & $(x(R),s)$ with $s=k+ed$ & ECDLP in ROM (forking lemma) & as above & Taproot (SegWit v1) spends, MuSig2 \\
++      SHA-256 & 64-step Davies--Meyer compression, Merkle--Damg\aa rd & preimage / collision resistance & $2^{256}$ / $2^{128}$ & transaction and block hashes (doubled), Merkle trees, tagged hashes, HMAC, PoW \\
++      RIPEMD-160$\circ$SHA-256 & 160-bit hash of a 256-bit hash & preimage / collision resistance & $2^{160}$ / $2^{80}$ & legacy addresses (P2PKH, P2WPKH) \\
++      Tagged hash & $\mathrm{SHA256}(\mathrm{SHA256}(t)\|\mathrm{SHA256}(t)\|m)$ & domain separation, ROM & as SHA-256 & BIP340 challenges and nonces, Taproot commitments \\
++      \bottomrule
++    \end{tabular}
++  }
++  \par\smallskip{\footnotesize Generic costs are the best known attacks on an ideal instance of each size; Sections~\ref{sec:secp}--\ref{sec:sha} verify that \secp{} and SHA-256 are not known to deviate from them.}
++
++\end{table}
++
+ This section fixes notation and states the mathematical facts the rest of the paper builds on. We give proofs or
+ exact verification scripts for the facts that are specific to \secp{} (Section~\ref{sec:secp}); classical theorems are
+ cited to the standard references \citep{silverman2009arithmetic,washington2008elliptic,hankerson2004guide,galbraith2012mathematics}.

modified paper/sections/03_literature.tex +11 −13

				`@@ -29,13 +29,13 @@ prime fields, and \citet{bernstein2014safecurves} tabulate the exclusion criteri`
29	Table~\ref{tab:ecdlp-records} lists the completed ECDLP computations we could verify. The largest prime-field	29	Table~\ref{tab:ecdlp-records} lists the completed ECDLP computations we could verify. The largest prime-field
30	instance remains the 112-bit computation of \citet{bos2012solving} (July 2009); the binary-field records are 113-bit	30	instance remains the 112-bit computation of \citet{bos2012solving} (July 2009); the binary-field records are 113-bit
31	curves \citep{wenger2014solving,wenger2016harder,bernstein2016faster}; the 131-bit Certicom challenges are open	31	curves \citep{wenger2014solving,wenger2016harder,bernstein2016faster}; the 131-bit Certicom challenges are open
32	−\citep{certicom2009challenge}. The gap to \secp{} is a factor of about $2^{71}$ in expected group operations.	32	+\citep{certicom2009challenge}. The gap to \secp{} is a factor of about $2^{72}$ in expected group operations.
33		33
34	\begin{table}[htbp]	34	\begin{table}[htbp]
35	\centering\footnotesize	35	\centering\footnotesize
36	− \begin{threeparttable}	36	+ \caption{Completed elliptic-curve discrete-logarithm computations (verified records only).}
37	− \caption{Completed elliptic-curve discrete-logarithm computations (verified records only).}
38	\label{tab:ecdlp-records}	37	\label{tab:ecdlp-records}
		38	+ \resizebox{\textwidth}{!}{%
39	\begin{tabular}{@{}llllll@{}}	39	\begin{tabular}{@{}llllll@{}}
40	\toprule	40	\toprule
41	Instance & Bits & Field & Hardware & Completed & Source \\	41	Instance & Bits & Field & Hardware & Completed & Source \\
				`@@ -51,10 +51,9 @@ curves \citep{wenger2014solving,wenger2016harder,bernstein2016faster}; the 131-b`
51	ECCp-131, ECC2-131, ECC2K-130 & 130--131 & prime/binary & --- & open & \citet{certicom2009challenge,bailey2009breaking} \\	51	ECCp-131, ECC2-131, ECC2K-130 & 130--131 & prime/binary & --- & open & \citet{certicom2009challenge,bailey2009breaking} \\
52	\bottomrule	52	\bottomrule
53	\end{tabular}	53	\end{tabular}
54	− \begin{tablenotes}\footnotesize	54	+ }
55	− \item Figures as stated in the sources (\code{literature/records.md}). \secp{} has $n\approx 2^{256}$: rho with the negation map needs $\approx\sqrt{\pi n/4}\approx 2^{127.5}$ operations, about $2^{71}$ times the 112-bit computation.	55	+ \par\smallskip{\footnotesize Figures as stated in the sources (\code{literature/records.md}). \secp{} has $n\approx 2^{256}$: rho with the negation map needs $\approx\sqrt{\pi n/4}\approx 2^{127.8}$ operations, about $2^{72}$ times the 112-bit computation.}
56	− \end{tablenotes}	56	+
57	− \end{threeparttable}
58	\end{table}	57	\end{table}
59		58
60	\subsection{Signatures}	59	\subsection{Signatures}
				`@@ -87,9 +86,9 @@ costs ($2^{63}$).`
87		86
88	\begin{table}[htbp]	87	\begin{table}[htbp]
89	\centering\footnotesize	88	\centering\footnotesize
90	− \begin{threeparttable}	89	+ \caption{Reduced-step cryptanalysis of SHA-256 (64 steps): published records.}
91	− \caption{Reduced-step cryptanalysis of SHA-256 (64 steps): published records.}
92	\label{tab:sha-lit}	90	\label{tab:sha-lit}
		91	+ \resizebox{\textwidth}{!}{%
93	\begin{tabular}{@{}lllll@{}}	92	\begin{tabular}{@{}lllll@{}}
94	\toprule	93	\toprule
95	Type & Steps & Complexity & Practical? & Source \\	94	Type & Steps & Complexity & Practical? & Source \\
				`@@ -108,10 +107,9 @@ costs ($2^{63}$).`
108	Preimage (hash / compression) & 45 / 52 & $\approx 2^{256}$ (bicliques) & no & \citet{khovratovich2012bicliques} \\	107	Preimage (hash / compression) & 45 / 52 & $\approx 2^{256}$ (bicliques) & no & \citet{khovratovich2012bicliques} \\
109	\bottomrule	108	\bottomrule
110	\end{tabular}	109	\end{tabular}
111	− \begin{tablenotes}\footnotesize	110	+ }
112	− \item Figures as stated in the abstracts (\code{literature/records.md}). No attack on the full 64-step function is known; the generic bounds $2^{128}$ (collision) and $2^{256}$ (preimage) stand.	111	+ \par\smallskip{\footnotesize Figures as stated in the abstracts (\code{literature/records.md}). No attack on the full 64-step function is known; the generic bounds $2^{128}$ (collision) and $2^{256}$ (preimage) stand.}
113	− \end{tablenotes}	112	+
114	− \end{threeparttable}
115	\end{table}	113	\end{table}
116		114
117	\subsection{Automated discovery}	115	\subsection{Automated discovery}

modified paper/sections/04_secp256k1.tex +14 −11

				`@@ -10,9 +10,9 @@ library and in PARI/GP~2.19---and the two implementations agree on all fourteen`
10		10
11	\begin{table}[htbp]	11	\begin{table}[htbp]
12	\centering\footnotesize	12	\centering\footnotesize
13	− \begin{threeparttable}	13	+ \caption{secp256k1 parameters and derived algebraic invariants (all verified exactly in Python and PARI/GP).}
14	− \caption{secp256k1 parameters and derived algebraic invariants (all verified exactly in Python and PARI/GP).}
15	\label{tab:secp-params}	14	\label{tab:secp-params}
		15	+ \resizebox{\textwidth}{!}{%
16	\begin{tabular}{@{}llp{8.2cm}@{}}	16	\begin{tabular}{@{}llp{8.2cm}@{}}
17	\toprule	17	\toprule
18	Quantity & Symbol & Value / verified property \\	18	Quantity & Symbol & Value / verified property \\
				`@@ -35,10 +35,9 @@ library and in PARI/GP~2.19---and the two implementations agree on all fourteen`
35	$n-1$, $p-1$ & & $n-1 = 2^6\cdot 3\cdot 149\cdot 631\cdot(\ldots)$; $p-1 = 2\cdot 3\cdot 7\cdot 13441\cdot(\ldots)$ (large cofactors) \\	35	$n-1$, $p-1$ & & $n-1 = 2^6\cdot 3\cdot 149\cdot 631\cdot(\ldots)$; $p-1 = 2\cdot 3\cdot 7\cdot 13441\cdot(\ldots)$ (large cofactors) \\
36	\bottomrule	36	\bottomrule
37	\end{tabular}	37	\end{tabular}
38	− \begin{tablenotes}\footnotesize	38	+ }
39	− \item Source: \code{experiments/baselines/secp256k1\_facts.py}. Hexadecimal values abbreviated; full values in the JSON result and in \code{src/wp34/secp256k1.py}.	39	+ \par\smallskip{\footnotesize Source: \code{experiments/baselines/secp256k1\_facts.py}. Hexadecimal values abbreviated; full values in the JSON result and in \code{src/wp34/secp256k1.py}.}
40	− \end{tablenotes}	40	+
41	− \end{threeparttable}
42	\end{table}	41	\end{table}
43		42
44	\subsection{Why the special form is interesting}	43	\subsection{Why the special form is interesting}
				`@@ -76,8 +75,10 @@ $(k_1,k_2)\leftrightarrow k_1+k_2\omega$, $L$ is the principal ideal $(\bar\pi-1`
76	$\bar\pi=(t-f\sqrt{-3})/2$ is the Frobenius conjugate for which $\omega\mapsto\lambda$ sends $\bar\pi-1$ to~$0$.	75	$\bar\pi=(t-f\sqrt{-3})/2$ is the Frobenius conjugate for which $\omega\mapsto\lambda$ sends $\bar\pi-1$ to~$0$.
77	Consequently	76	Consequently
78	\begin{equation}	77	\begin{equation}
79	− (a_1,b_1) = \Big(\tfrac{t-f}{2}-1,\ -f\Big),\qquad (a_2,b_2) = (a_1-b_1,\ a_1) \;\;(=\omega\cdot(a_1+b_1\omega)\text{ up to sign}),	78	+\begin{aligned}
80	− \qquad a_1^2-a_1b_1+b_1^2 = n ,	79	+ (a_1,b_1) &= \Big(\tfrac{t-f}{2}-1,\ -f\Big), & (a_2,b_2) &= (a_1-b_1,\ a_1)\ \ (=\omega\cdot(a_1+b_1\omega)\text{ up to sign}),\\
		80	+ a_1^2-a_1b_1+b_1^2 &= n ,
		81	+\end{aligned}
81	\label{eq:glvclosed}	82	\label{eq:glvclosed}
82	\end{equation}	83	\end{equation}
83	and these are exactly the constants hard-coded in \libsecp{}.	84	and these are exactly the constants hard-coded in \libsecp{}.
				`@@ -89,7 +90,8 @@ $(\alpha)$ with $\Norm(\alpha)=n$. Now $n=\#E(\F_p)=\Norm(\pi-1)=\Norm(\bar\pi-1`
89	identity, so $\pi-1$ kills every point and one of $\pi-1$, $\bar\pi-1$ lies in $\ker\rho$ (which one depends on the	90	identity, so $\pi-1$ kills every point and one of $\pi-1$, $\bar\pi-1$ lies in $\ker\rho$ (which one depends on the
90	labelling of $\omega$ versus $\lambda$); call it $\bar\pi-1$. Since $(\bar\pi-1)$ and $\ker\rho$ are ideals of the same	91	labelling of $\omega$ versus $\lambda$); call it $\bar\pi-1$. Since $(\bar\pi-1)$ and $\ker\rho$ are ideals of the same
91	norm with one containing the other, they are equal. Writing $\sqrt{-3}=2\omega+1$ gives	92	norm with one containing the other, they are equal. Writing $\sqrt{-3}=2\omega+1$ gives
92	−$\bar\pi-1 = \frac{t-f}{2}-1-f\omega$, i.e.\ $(a_1,b_1)$ as stated; multiplying by the unit $\omega$ gives the second	93	+\[\bar\pi-1 = \tfrac{t-f}{2}-1-f\omega,\]
		94	+i.e.\ $(a_1,b_1)$ as stated; multiplying by the unit $\omega$ gives the second
93	basis vector; and $\Norm(\bar\pi-1)=n$ is~\eqref{eq:glvclosed}. The identification with the \libsecp{} constants is an	95	basis vector; and $\Norm(\bar\pi-1)=n$ is~\eqref{eq:glvclosed}. The identification with the \libsecp{} constants is an
94	exact integer check (\code{identity\_search.json}, field \code{closed\_form\_matches\_libsecp256k1}).	96	exact integer check (\code{identity\_search.json}, field \code{closed\_form\_matches\_libsecp256k1}).
95	\end{proof}	97	\end{proof}
				`@@ -124,8 +126,9 @@ There is no group structure on the orbit set $E(\F_p)/\Aut(E)$ for which the pro`
124	\begin{proof}	126	\begin{proof}
125	If the projection were a homomorphism, its kernel would be the orbit of $\Oinf$, which is $\{\Oinf\}$, so the	127	If the projection were a homomorphism, its kernel would be the orbit of $\Oinf$, which is $\{\Oinf\}$, so the
126	projection would be injective---contradicting the fact that the other orbits have six elements. Equivalently,	128	projection would be injective---contradicting the fact that the other orbits have six elements. Equivalently,
127	−$P\sim\phi P$ and $Q\sim Q$ would force $P+Q\sim\phi P+Q$; on synthetic 16-, 20- and 24-bit $j=0$ curves this fails for	129	+$P\sim\phi P$ and $Q\sim Q$ would force $P+Q\sim\phi P+Q$; on synthetic 16-, 20- and 24-bit $j=0$ curves this fails
128	−every one of $1500$ random pairs (\code{results/theory/orbit\_quotient\_counterexample.json}).	130	+for
		131	+every one of $1500$ random pairs (file \code{orbit\_quotient\_counterexample.json} under \code{results/theory/}).
129	\end{proof}	132	\end{proof}
130		133
131	The same argument applies to any finite group of automorphisms fixing the identity: equivalence classes under	134	The same argument applies to any finite group of automorphisms fixing the identity: equivalence classes under

modified paper/sections/09_experimental_design.tex +5 −6

				`@@ -39,9 +39,9 @@ computed on $\ge 44$ bits and empirical exponents are also fitted on $\ge 32$ bi`
39		39
40	\begin{table}[htbp]	40	\begin{table}[htbp]
41	\centering\footnotesize	41	\centering\footnotesize
42	− \begin{threeparttable}	42	+ \caption{ECDLP experimental configuration (seed 34; all instances verified).}
43	− \caption{ECDLP experimental configuration (seed 34; all instances verified).}
44	\label{tab:ecdlp-config}	43	\label{tab:ecdlp-config}
		44	+ \resizebox{\textwidth}{!}{%
45	\begin{tabular}{@{}llllp{5.6cm}@{}}	45	\begin{tabular}{@{}llllp{5.6cm}@{}}
46	\toprule	46	\toprule
47	Study & Curves & Sizes (bits) & Instances/size & Configurations \\	47	Study & Curves & Sizes (bits) & Instances/size & Configurations \\
				`@@ -54,10 +54,9 @@ computed on $\ge 44$ bits and empirical exponents are also fitted on $\ge 32$ bi`
54	preprocessing (Python) & random & 22, 26 & 60 & $T\in\{2^4,\dots,2^{12}\}$ stored distinguished points \\	54	preprocessing (Python) & random & 22, 26 & 60 & $T\in\{2^4,\dots,2^{12}\}$ stored distinguished points \\
55	\bottomrule	55	\bottomrule
56	\end{tabular}	56	\end{tabular}
57	− \begin{tablenotes}\footnotesize	57	+ }
58	− \item Nodes: generic scaling, sweep and parallel study on M3U96a (Apple M3 Ultra); $j=0$ scaling and time--memory on M2U64 (Apple M2 Ultra); preprocessing on the laptop. A 20-instance pilot of the two scaling studies (kept in \code{results/synthetic\_ecdlp/pilot20/}) was used to size the final runs.	58	+ \par\smallskip{\footnotesize Nodes: generic scaling, sweep and parallel study on M3U96a (Apple M3 Ultra); $j=0$ scaling and time--memory on M2U64 (Apple M2 Ultra); preprocessing on the laptop. A 20-instance pilot of the two scaling studies (kept in \code{results/synthetic\_ecdlp/pilot20/}) was used to size the final runs.}
59	− \end{tablenotes}	59	+
60	− \end{threeparttable}
61	\end{table}	60	\end{table}
62		61
63	\subsection{Measurement and statistics}	62	\subsection{Measurement and statistics}

modified paper/sections/10b_results_sha.tex +155 −1

++\subsection{Axis C: reduced-step SHA-256 (H15--H19)}
++\label{sec:results-sha}
++
++\paragraph{Diffusion (H15).} A single-bit difference in $W_0$ flips on average $1.5\%$ of the state bits after one
++step and reaches the $0.49$ threshold at step~\shaDiffWzero{} (Table~\ref{tab:sha-diff}, Figure~\ref{fig:sha-diff}); a
++difference in $W_5$ or $W_{15}$ is invisible until the word enters the state and then follows the same six-step
++profile (full diffusion at steps \shaDiffWfive{} and \shaDiffWfifteen{}); a difference in an IV register needs
++\shaDiffIV{} steps. The profile is identical across three seeds of \shaDiffN{} messages. After 64 steps the Hamming
++weight of the output difference is $\shaDiffHamming\pm\shaDiffHammingSd$, indistinguishable from the random-oracle
++control ($\shaDiffRO$ flip ratio). Classification: known behaviour, reproduced with a precise step count.
++
++\begin{table}[htbp]
++  \centering\footnotesize
++  \caption{Mean fraction of flipped state bits after $s$ steps for a single-bit input difference (three seeds $\times$ \shaDiffN{} random messages; identical across seeds to three decimals).}
++  \label{tab:sha-diff}
++  \input{tables/sha_diffusion}
++\end{table}
++
++\begin{figure}[htbp]
++  \centering
++  \includegraphics[width=\textwidth]{sha256_diffusion.pdf}
++  \caption{Reduced-round diffusion: flip probability of each output bit by step for a one-bit difference in $W_0$ (heat map) and mean flip ratio by step with the random-oracle control. Generated by \code{figures/make\_sha256\_figures.py}.}
++  \label{fig:sha-diff}
++\end{figure}
++
++\paragraph{Statistical regularities (H16).} With $N=\shaBiasN{}$ messages per seed the $4\sigma$ thresholds are
++$0.014$ for a bit bias and $0.028$ for a correlation, with \shaBiasExpectedPairs{} chance pairs expected among the
++$64\times 256$ tested. For $r\le 3$ steps, $64(4-r)$ output bits are untouched IV registers (bias $0.5$,
++$\chi^2$ rejections, correlations equal to~1); at $r=4$ the bit biases and byte distributions are already at the
++noise floor but 6--13 pairs with $\lvert\mathrm{corr}\rvert=1$ remain (the least significant bit of $e_1$ is an affine
++function of the least significant bit of $W_0$ and is still exposed in register~$h$); from $r=\shaBiasFirstClean$
++every statistic is at the random-oracle floor and stays there through $r=64$ (Table~\ref{tab:sha-bias},
++Figure~\ref{fig:sha-bias}): two isolated $4.1\sigma$ bits in $10\,752$ tests, exactly the number expected by chance.
++These are observations, not attacks: the published differential attacks exploit structure far beyond what
++first-order statistics on random inputs can see.
++
++\begin{table}[htbp]
++  \centering\footnotesize
++  \caption{First-order statistics of the $r$-step compression function on random single-block messages (ranges over three seeds of \shaBiasN{}).}
++  \label{tab:sha-bias}
++  \input{tables/sha_bias}
++\end{table}
++
++\begin{figure}[htbp]
++  \centering
++  \includegraphics[width=0.9\textwidth]{sha256_bias.pdf}
++  \caption{Bias test: number of biased bits, maximum correlation and significant pairs by step count, with the random-oracle control.}
++  \label{fig:sha-bias}
++\end{figure}
++
++\paragraph{SAT and SMT preimage search (H17).} The Tseitin encoding of the full 64-step compression has
++\shaPreVars{} variables and \shaPreClauses{} clauses. Over \shaPreCells{} cells ($r\times k\times$ solver $\times$
++placement of the $k$ free bits, 2--3 seeds, 300~s) every satisfying assignment was re-hashed with the reference
++implementation (\shaPreVerified{} verified). Two regimes appear (Table~\ref{tab:sha-pre}, Figure~\ref{fig:sha-sat}).
++For $r\le 16$ the instance is solved in \shaPreRsixteenTime~s with \shaPreRsixteenConf{} conflicts whatever $k$ is:
++this is not search but propagation---with at most 16 message words entering the computation, inverting the steps
++determines the unknown bits directly (Section~\ref{sec:formal} proves the underlying bijections). As soon as the
++message expansion is involved ($r\ge 20$) only the $k=16$ cells are solved: CaDiCaL needs \shaPreRtwentyTime~s at
++$r=20$ and \shaPreRsixtyfourTime~s at $r=64$ (\shaPreRsixtyfourSolved{} seeds), Kissat is comparable, and every
++$k\ge 24$ cell at $r\ge 20$ times out (the ``spread'' placement of the free bits lets CaDiCaL reach $k=32$ at $r=20$
++only). Since $k=16$ free bits is a $2^{16}$ brute-force space, the solvers are \emph{slower} than exhaustive search
++once the expansion matters. Z3's bit-vector theory is two to four orders of magnitude slower than the CNF route on
++the cells it solves (largest: \shaPreZthreeLargest) and times out on all $r\ge 16$ cells. Peak memory stayed below
++302~MB (CNF) and 605~MB (Z3).
++
++\begin{table}[htbp]
++  \centering\footnotesize
++  \caption{Preimage search on the $r$-step compression function with $k$ free message bits in $W_0,W_1$ (CaDiCaL~3.0.1, median wall-clock seconds of solved seeds; T($m$) = all $m$ seeds timed out at 300~s; fractions give solved seeds when not all solved).}
++  \label{tab:sha-pre}
++  \input{tables/sha_preimage_cadical}
++\end{table}
++
++\begin{figure}[htbp]
++  \centering
++  \includegraphics[width=\textwidth]{sha256_sat_scaling.pdf}
++  \caption{SAT/SMT preimage scaling: solver time against step count for each number of free bits, CaDiCaL and Kissat, timeouts censored at 300~s.}
++  \label{fig:sha-sat}
++\end{figure}
++
++\paragraph{SAT collision search (H18).} Table~\ref{tab:sha-col} and Figure~\ref{fig:sha-col} give the \shaColCells{}
++collision cells (two messages, equal $r$-step output; standard IV or free IV; with or without feed-forward; 600~s;
++\shaColVerified{} 119 collisions verified and saved). For $r\in\{4,6,8\}$ both solvers return UNSAT in every variant and
++seed (\shaColUnsatCells{} runs, 0.1--4.7~s): there is no collision whose differences lie in the words an 8-step
++compression reads, a machine-checked lower bound consistent with the 9-step minimum of the local collision. For
++$r=10$--$16$ with the standard IV the solvers find collisions in $0.02$--$0.05$~s with zero conflicts, and every such
++collision differs in exactly nine consecutive words---a local collision placed at the end of the computation,
++rediscovered by propagation. At $r=18$ all 16 words differ and the cost jumps to \shaColFixedTime~s with the standard
++IV (about $10^6$ conflicts) and \shaColFreeTime~s semi-free-start; at $r\ge 20$ every cell times out. The largest
++collision found by our generic encoding is therefore \shaColLargestR{} steps, against 24 steps for the 2008 hand
++analyses, 28 steps for pure SAT in \citet{alamgir2024sha256}, 31 practical steps for the dedicated tools
++\citep{li2024first} and 39 semi-free-start steps \citep{li2024new}. The answer to question~C4 is that unguided
++automated search reproduces only the trivial regime; the published records require differential characteristics
++that the solver is not given.
++
++\begin{table}[htbp]
++  \centering\footnotesize
++  \caption{Collision search on the $r$-step compression function (median seconds of solved seeds; UNSAT with its median time; T($m$) = timeouts at 600~s).}
++  \label{tab:sha-col}
++  \input{tables/sha_collision}
++\end{table}
++
++\begin{figure}[htbp]
++  \centering
++  \includegraphics[width=0.9\textwidth]{sha256_collision_scaling.pdf}
++  \caption{SAT collision scaling by step count and variant (standard versus free IV, with and without feed-forward), timeouts censored at 600~s.}
++  \label{fig:sha-col}
++\end{figure}
++
++\paragraph{The 9-step local collision (H19).} Deriving the correction pattern from the XOR-linearised step gives
++$(\delta,\ \SigZ\delta\oplus\SigO\delta,\ \SigO(\SigZ\delta),\ 0,\ \delta,\ \SigZ\delta\oplus\SigO\delta,\ 0,\ 0,\ \delta)$
++for $\delta W_i,\dots,\delta W_{i+8}$; a GF(2) matrix computation confirms cancellation for all 32 single-bit
++$\delta$ and 20 random multi-bit $\delta$, dropping any one correction leaves a residue, and the statement is
++machine-checked for all states and all $\delta$ (Section~\ref{sec:formal}). Applied blindly to the real step
++function, the pattern produced \emph{no} collision in \shaLcN{} random samples per bit position (upper bound
++$\shaLcBound$ by the rule of three); the difference survives step $i$ with probability \shaLcSurvivalOther{} for
++bits 0--30 (two carry conditions) and \shaLcSurvivalMsb{} for the most significant bit (no carry), survives step
++$i+1$ with probability $10^{-4}$ to $5\cdot10^{-4}$, and never survives step $i+2$ (Figure~\ref{fig:sha-lc}). That is
++the known picture: the linear model is exact, the real step follows it only under conditions on message and state
++bits. Given the freedom to choose those bits, CaDiCaL finds a conforming (state, $W_i..W_{i+8}$) pair for all
++\shaLcSatBits{} bit positions in \shaLcSatMin--\shaLcSatMax~s (fastest for the high bits, slowest for bit~0), each
++re-verified; a second seed reproduces bits 31 and~0. Classification: known result reproduced, with the linear part
++formally verified.
++
++\begin{figure}[htbp]
++  \centering
++  \includegraphics[width=0.85\textwidth]{sha256_local_collision.pdf}
++  \caption{The 9-step local collision in the real step function: survival probability of the difference pattern after steps $i$ and $i+1$ by bit position (\shaLcN{} samples each), and SAT time to find a conforming pair.}
++  \label{fig:sha-lc}
++\end{figure}
++
++\paragraph{Answers to C1--C5.} C1: reduced-step regularities exist and are fully characterised by the diffusion
++profile and the local-collision structure, both of which disappear within a handful of steps on random inputs.
++C2: SAT formulations make the invertibility of the first 16 steps and the 9-step minimum for collisions explicit
++and machine-checked; beyond that they measure the cost of unguided search, which grows faster than brute force in
++the free bits. C3: the only differential structure that remains meaningful as the step count grows is the local
++collision with its message conditions, which is exactly what the dedicated attacks chain together. C4: generic
++solvers reproduce 18-step collisions, far below the 31-step record. C5: the ``blind'' XOR pattern is a proposed
++simplification ruled out by counterexample ($0/3\,200\,000$).
++
++\subsection{Axis D: the hypothesis portfolio (H23, H24)}
++\label{sec:results-portfolio}
++
++Table~\ref{tab:hypotheses} is the discovery log in condensed form: every hypothesis with its final classification
++and a one-sentence verdict (the full records with evidence files are in \code{hypotheses/}). The tally is sixteen
++known results independently reproduced---each now with a measured constant, confidence interval or machine-checked
++proof---six empirical observations, three rejected conjectures (two of which we had formulated ourselves as
++plausible, \Hname{H05} and \Hname{H22}), no conditional result, no unresolved direction left open by lack of
++evidence, and no new verified result in the strict sense of the rubric. The cross-implementation gate
++(\Hname{H23}) caught two development errors in the Python reference, one in the CNF encoder (a Boolean fold rule
++that silently corrupted $\Ch$ gates) and one in the SAT harness (CaDiCaL's interrupt not honoured through the Python
++bindings), and corrected two statements written from memory (the local-collision correction vector and the
++singularity of $\sigma_0,\sigma_1$). We discuss what this record says about the methodology in
++Section~\ref{sec:implications}.
++
++{\footnotesize\input{tables/hypotheses}}

modified paper/sections/11a_formal.tex +11 −11

				`@@ -15,20 +15,20 @@ the exact build output and a record of the attempts that timed out.`
15	\begin{threeparttable}	15	\begin{threeparttable}
16	\caption{Machine-checked statements (Lean 4.35, \code{bv\_decide} with LRAT certificates unless stated). AIG = nodes of the bit-blasted instance.}	16	\caption{Machine-checked statements (Lean 4.35, \code{bv\_decide} with LRAT certificates unless stated). AIG = nodes of the bit-blasted instance.}
17	\label{tab:formal}	17	\label{tab:formal}
18	− \begin{tabular}{@{}p{3.6cm}p{7.2cm}p{3.4cm}@{}}	18	+ \begin{tabular}{@{}>{\raggedright\arraybackslash}p{4.1cm}>{\raggedright\arraybackslash}p{8.0cm}>{\raggedright\arraybackslash}p{3.4cm}@{}}
19	\toprule	19	\toprule
20	Theorem(s) & Statement & Method (AIG) \\	20	Theorem(s) & Statement & Method (AIG) \\
21	\midrule	21	\midrule
22	− \code{Ch\_opt}, \code{Maj\_opt\_or}, \code{Maj\_opt\_xor} & $\Ch(x,y,z)=((y\oplus z)\wedge x)\oplus z$; $\Maj=(x\wedge(y\vee z))\vee(y\wedge z)=((x\oplus y)\wedge(y\oplus z))\oplus y$ & SAT (608--768) \\	22	+ \code{Ch\_\allowbreak{}opt}, \code{Maj\_\allowbreak{}opt\_\allowbreak{}or}, \code{Maj\_\allowbreak{}opt\_\allowbreak{}xor} & $\Ch(x,y,z)=((y\oplus z)\wedge x)\oplus z$; $\Maj=(x\wedge(y\vee z))\vee(y\wedge z)=((x\oplus y)\wedge(y\oplus z))\oplus y$ & SAT (608--768) \\
23	− \code{Sigma0\_xor}, \ldots, \code{sigma1\_xor} & $\F_2$-linearity of $\SigZ,\SigO,\sigz,\sigo$ & SAT (870--960) \\	23	+ \code{Sigma0\_\allowbreak{}xor}, \ldots, \code{sigma1\_\allowbreak{}xor} & $\F_2$-linearity of $\SigZ,\SigO,\sigz,\sigo$ & SAT (870--960) \\
24	− \code{Sigma0\_injective}, \code{Sigma1\_injective}, \code{sigma0\_injective}, \code{sigma1\_injective} & all four maps are injective on 32 bits & SAT, UNSAT certificates (644--704) \\	24	+ \code{Sigma0\_\allowbreak{}injective}, \code{Sigma1\_\allowbreak{}injective}, \code{sigma0\_\allowbreak{}injective}, \code{sigma1\_\allowbreak{}injective} & all four maps are injective on 32 bits & SAT, UNSAT certificates (644--704) \\
25	− \code{*\_bijective} (4) & explicit inverses: $\SigZ^{-1}$ = XOR of 17 rotations, $\sigz^{-1},\sigo^{-1}$ as $32\times32$ $\F_2$ matrices; both compositions are the identity & byte-split SAT (33--4\,817) + rewriting \\	25	+ \code{*\_\allowbreak{}bijective} (4) & explicit inverses: $\SigZ^{-1}$ = XOR of 17 rotations, $\sigz^{-1},\sigo^{-1}$ as $32\times32$ $\F_2$ matrices; both compositions are the identity & byte-split SAT (33--4\,817) + rewriting \\
26	− \code{shr3\_not\_injective}, \code{sigma0\_rotations\_not\_injective} & controls: each summand of $\sigz$ is singular & \code{decide} \\	26	+ \code{shr3\_\allowbreak{}not\_\allowbreak{}injective}, \code{sigma0\_\allowbreak{}rotations\_\allowbreak{}not\_\allowbreak{}injective} & controls: each summand of $\sigz$ is singular & \code{decide} \\
27	− \code{stepInv\_step}, \code{step\_stepInv}, \code{step\_bijective}, \code{steps\_bijective} & the SHA-256 step is a bijection of the 256-bit state for fixed $(K_t,W_t)$, and so is any sequence of steps & two 160-bit SAT lemmas (2\,048, 2\,420) + rewriting; direct 320-bit SAT timed out \\	27	+ \code{stepInv\_\allowbreak{}step}, \code{step\_\allowbreak{}stepInv}, \code{step\_\allowbreak{}bijective}, \code{steps\_\allowbreak{}bijective} & the SHA-256 step is a bijection of the 256-bit state for fixed $(K_t,W_t)$, and so is any sequence of steps & two 160-bit SAT lemmas (2\,048, 2\,420) + rewriting; direct 320-bit SAT timed out \\
28	− \code{scheduleStep\_inv}, \code{schedule\_backward} & $W_{t-16}=W_t\ominus\sigo(W_{t-2})\ominus W_{t-7}\ominus\sigz(W_{t-15})$; any 16 consecutive schedule words determine all 64 & SAT (1\,921) + recursion \\	28	+ \code{scheduleStep\_\allowbreak{}inv}, \code{schedule\_\allowbreak{}backward} & $W_{t-16}=W_t\ominus\sigo(W_{t-2})\ominus W_{t-7}\ominus\sigz(W_{t-15})$; \newline any 16 consecutive schedule words determine all 64 & SAT (1\,921) + recursion \\
29	− \code{localCollision\_absorb}, \code{localCollision\_xor3} & in the XOR-linearised step (with $\Ch=\Maj=0$, resp.\ $\Ch=\Maj=x\oplus y\oplus z$), for all states, constants, messages and $\delta$: the correction pattern $(\delta,\ \SigO\delta\oplus\SigZ\delta,\ \SigO(\SigZ\delta),\ 0,\ \delta,\ \SigZ\delta\oplus\SigO\delta,\ 0,\ 0,\ \delta)$ cancels after 9 steps & difference version by byte-split SAT (5\,049 / 8\,769), lifted by proven linearity of the 9-step map \\	29	+ \code{localCollision\_\allowbreak{}absorb}, \code{localCollision\_\allowbreak{}xor3} & in the XOR-linearised step (with $\Ch=\Maj=0$, resp.\ $\Ch=\Maj=x\oplus y\oplus z$), for all states, constants, messages and $\delta$: \newline the correction pattern $(\delta,\ \SigO\delta\oplus\SigZ\delta,\ \SigO(\SigZ\delta),\ 0,\ \delta,\ \SigZ\delta\oplus\SigO\delta,\ 0,\ 0,\ \delta)$ cancels after 9 steps & difference version by byte-split SAT (5\,049 / 8\,769), lifted by proven linearity of the 9-step map \\
30	− \code{absorb\_corrections\_not\_real\_collision} & control: the same corrections do \emph{not} give a collision of the real (modular) 9-step map on a concrete input & \code{decide} \\	30	+ \code{absorb\_\allowbreak{}corrections\_\allowbreak{}not\_\allowbreak{}real\_\allowbreak{}collision} & control: the same corrections do \emph{not} give a collision of the real (modular) 9-step map on a concrete input & \code{decide} \\
31	− \code{schnorr\_correct}, \code{ecdsa\_correct}, \code{ecdsa\_malleable} & in an axiomatised cyclic group with $x(-P)=x(P)$: $s\equiv k+ed\Rightarrow [s]G=R+[e]P$; ECDSA verification is correct; $(r,s)$ valid $\Rightarrow(r,n-s)$ valid & rewriting from the structure fields (no SAT) \\	31	+ \code{schnorr\_\allowbreak{}correct}, \code{ecdsa\_\allowbreak{}correct}, \code{ecdsa\_\allowbreak{}malleable} & in an axiomatised cyclic group with $x(-P)=x(P)$: $s\equiv k+ed\Rightarrow [s]G=R+[e]P$; ECDSA verification is correct; $(r,s)$ valid $\Rightarrow(r,n-s)$ valid & rewriting from the structure fields (no SAT) \\
32	\bottomrule	32	\bottomrule
33	\end{tabular}	33	\end{tabular}
34	\begin{tablenotes}\footnotesize	34	\begin{tablenotes}\footnotesize

modified paper/sections/12_implications.tex +3 −3

				`@@ -9,10 +9,10 @@ number of rho iterations (Section~\ref{sec:results}). Proposition~\ref{prop:end}`
9	small as it can be given $j=0$, so there is no further endomorphism to exploit; Proposition~\ref{prop:noquotient}	9	small as it can be given $j=0$, so there is no further endomorphism to exploit; Proposition~\ref{prop:noquotient}
10	shows that the automorphism orbits cannot be turned into a smaller group; and the exact exclusion table	10	shows that the automorphism orbits cannot be turned into a smaller group; and the exact exclusion table
11	(Section~\ref{sec:secp}) confirms that every known algebraic transfer is inapplicable. The generic bound therefore	11	(Section~\ref{sec:secp}) confirms that every known algebraic transfer is inapplicable. The generic bound therefore
12	−stands: solving one \secp{} instance costs about $\sqrt{\pi n/12}\approx 2^{126.7}$ group operations with the full	12	+stands: solving one \secp{} instance costs about $\sqrt{\pi n/12}\approx 2^{127.0}$ group operations with the full
13	−automorphism trick, roughly $2^{70}$ times the largest ECDLP computation ever completed. Preprocessing does not	13	+automorphism trick, roughly $2^{72}$ times the largest ECDLP computation ever completed. Preprocessing does not
14	change this conclusion: the per-instance cost $\sqrt{n/T}$ after a table of $T$ points requires $\sqrt{nT}$ work up	14	change this conclusion: the per-instance cost $\sqrt{n/T}$ after a table of $T$ points requires $\sqrt{nT}$ work up
15	−front, and a table reducing each instance to $2^{80}$ operations would itself cost $2^{174}$ operations and $2^{93}$	15	+front, and a table reducing each instance to $2^{80}$ operations would itself cost $2^{176}$ operations and $2^{96}$
16	entries. Our measurements (Hypothesis~\Hname{H12}) put the constant at about $1.5$, which does not alter the	16	entries. Our measurements (Hypothesis~\Hname{H12}) put the constant at about $1.5$, which does not alter the
17	exponent.	17	exponent.
18		18

modified paper/sections/13_limitations.tex +28 −0

+ \section{Limitations}
+ \label{sec:limitations}
++Table~\ref{tab:contrib} pairs each contribution with its classification and the limitation that bounds it.
++
++\begin{table}[htbp]
++  \centering\footnotesize
++  \begin{threeparttable}
++    \caption{Research contributions and their limitations.}
++    \label{tab:contrib}
++    \begin{tabular}{@{}p{4.6cm}p{3.0cm}p{6.6cm}@{}}
++      \toprule
++      Contribution & Classification & Limitation \\
++      \midrule
++      Two-implementation verification of all \secp{} invariants (Table~\ref{tab:secp-params}) & known, reproduced & exact for the standard; says nothing about implementations \\
++      $\End(E)=\Z[\omega]$; GLV lattice $=(\bar\pi-1)$; closed form of the \libsecp{} constants & known structure, explicit form & a consequence of classical CM theory; exposition, not discovery \\
++      No group law on automorphism orbits (Prop.~\ref{prop:noquotient}) & rejected conjecture & elementary; closes one idea only \\
++      ECDLP baselines on $6\,240$ instances with constants and CIs & known, reproduced & $\le 56$ bits; random-mapping model extrapolates, data do not \\
++      $\sqrt6$ in iterations, $\approx 1\times$ in time for order-6 classes & known + implementation observation & specific to our canonicalisation; record implementations do better \\
++      Iteration-function sweep: nothing below the random-mapping floor & rejected shortcut & bounded design space of generic walks \\
++      Parallel, time--memory and preprocessing curves & known, reproduced & one machine family; constants depend on parameters \\
++      Signature benchmarks and batch-verification saturation mechanism & known, reproduced & two Apple-silicon hosts, two libraries \\
++      SHA-256 diffusion, bias, SAT/SMT calibration, UNSAT for $\le 8$ steps, local collision & known / empirical & generic encodings; no characteristic guidance; nothing about 64 steps \\
++      Lean~4 library of SHA-256 and signature facts; refutation of $\sigma$-singularity & machine-checked & bit-level and abstract-group facts only \\
++      Six-stage pipeline executed autonomously with a conservative classifier & methodological & single run, single agent, qualitative assessment \\
++      \bottomrule
++    \end{tabular}
++  \end{threeparttable}
++\end{table}
++
++
+ \begin{itemize}
+ \item \textbf{Scale.} The ECDLP experiments run on groups of at most $2^{48}$--$2^{56}$ elements. The fitted
+ exponents and constants describe this range; extrapolation to $2^{256}$ rests on the random-mapping heuristic and on

modified paper/sections/14_conclusion.tex +1 −1

				`@@ -10,7 +10,7 @@ enthusiasm. The answer is no, with the following specifics.`
10	The algebraic structure of \secp{} is fully accounted for by complex multiplication by $\Z[\omega]$: it yields the	10	The algebraic structure of \secp{} is fully accounted for by complex multiplication by $\Z[\omega]$: it yields the
11	$\sqrt6$ reduction in rho iterations and the halving of doublings in scalar multiplication, it determines the GLV	11	$\sqrt6$ reduction in rho iterations and the halving of doublings in scalar multiplication, it determines the GLV
12	constants of \libsecp{} in closed form, and it leaves no room for a further endomorphism or for a smaller quotient	12	constants of \libsecp{} in closed form, and it leaves no room for a further endomorphism or for a smaller quotient
13	−group. The generic algorithms behave exactly as the random-mapping theory predicts on $6\,000$ synthetic instances:	13	+group. The generic algorithms behave exactly as the random-mapping theory predicts on $6\,240$ synthetic instances:
14	$T(n)\propto n^{0.5}$, $1.254\sqrt n$ iterations for rho, $\sqrt6$ from the automorphisms in iterations---though not,	14	$T(n)\propto n^{0.5}$, $1.254\sqrt n$ iterations for rho, $\sqrt6$ from the automorphisms in iterations---though not,
15	in our engine, in seconds---and the trade-offs of memory, parallelism and preprocessing that the literature describes.	15	in our engine, in seconds---and the trade-offs of memory, parallelism and preprocessing that the literature describes.
16	An automated search over iteration-function designs cannot beat the random-mapping floor. ECDSA and Schnorr differ	16	An automated search over iteration-function designs cannot beat the random-mapping floor. ECDSA and Schnorr differ

modified paper/sections/abstract.tex +25 −1

+−Placeholder abstract.
+ \ No newline at end of file
++Bitcoin's security rests on the elliptic-curve discrete-logarithm problem on \secp{}, on SHA-256, and on the ECDSA
++and BIP340 Schnorr signature schemes. The generic cost of the discrete logarithm, $\Theta(\sqrt n)$, is a theorem in
++the generic-group model; the curve's unusual structure---a special prime, $j$-invariant~0 and complex multiplication by
++the Eisenstein integers---has long invited speculation that an algebraic shortcut might exist. We test this
++speculation with an autonomous, six-stage discovery pipeline (verified literature base, 25 structured hypotheses,
++exact symbolic checks, seeded experiments with full provenance, Lean~4 machine-checked statements, six-way
++classification) executed by an AI research agent under a written mandate that forbids assuming shortcuts exist.
++Results. (i)~Every \secp{} parameter and invariant is verified twice with exact arithmetic; $\End(E)=\Z[\omega]$ leaves
++nothing beyond the six automorphisms; the GLV lattice is the ideal $(\bar\pi-1)$, which gives the hard-coded
++\libsecp{} constants in closed form ($a_1=(t-f)/2-1$, $b_1=-f$); the automorphism orbits admit no compatible group
++law; prime-field index calculus and all transfer attacks are excluded quantitatively. (ii)~A native engine solved
++$6\,240$ synthetic ECDLP instances of 20--56 bits: empirical exponents $0.48$--$0.50$, rho constant $1.254\sqrt n$
++against the random-mapping prediction $1.2533$, order-6 classes $2.42\times$ fewer iterations ($\sqrt6$) but no
++wall-clock gain in our implementation, $22\times$ parallel speed-up on 28 threads, the predicted time--memory and
++preprocessing trade-offs ($1.5\sqrt{n/T}$ online), and no iteration-function design below the random-mapping floor.
++(iii)~BIP340 batch verification reaches $3.1\times$ and saturates for an identified reason; ECDSA and Schnorr verify
++at the same cost and differ in proof structure. (iv)~Reduced-step SHA-256 diffuses fully in six steps, shows no
++first-order regularity beyond five, and yields to generic SAT search only up to 18-step collisions and $2^{16}$-bit
++preimages, far below the 31-step records; the 9-step local collision is reproduced and its linear part proved.
++(v)~Lean~4 proofs of the word-level identities, the bijectivity of the step and of all four $\Sigma/\sigma$
++functions (refuting our own conjecture that $\sigma_0,\sigma_1$ are singular), the schedule inversion, the
++linearised local collision, ECDSA malleability and Schnorr correctness. The pipeline produced sixteen reproductions
++with measured constants, six empirical observations, three rejected conjectures and no claim of a weakness; we argue
++that this is the correct output for automated mathematical research on cryptographic standards, and we release
++everything needed to reproduce it.

modified paper/tables/hypotheses.tex +21 −21

				`@@ -5,28 +5,28 @@`
5	\toprule ID & Axis & Hypothesis & Classification & Verdict \\ \midrule \endhead	5	\toprule ID & Axis & Hypothesis & Classification & Verdict \\ \midrule \endhead
6	\bottomrule \endfoot	6	\bottomrule \endfoot
7	H01 & A & Standardised secp256k1 parameters and GLV constants are exactly consistent & Known result reproduced & All 14 facts agree between Python and PARI/GP; ($\beta$, $\lambda$$^2$) mismatch confirmed as expected. \\	7	H01 & A & Standardised secp256k1 parameters and GLV constants are exactly consistent & Known result reproduced & All 14 facts agree between Python and PARI/GP; ($\beta$, $\lambda$$^2$) mismatch confirmed as expected. \\
8	−H02 & A & End(E) = Z[$\omega$] and the GLV basis is the Eisenstein ideal ($\pi$̄ -- 1): closed form of the libsecp256k1 constants & Known result reproduced & Closed form holds exactly; all 22 identities found by the search are explained by CM theory. Known in principle (ideal structure of the GLV lattice), the explicit identification with the published constants is a useful clarification, not new mathematics. \\	8	+H02 & A & End(E) = Z[$\omega$] and the GLV basis is the Eisenstein ideal ($\bar\pi$ -- 1): closed form of the libsecp256k1 constants & Known result reproduced & Closed form holds exactly; all 22 identities found by the search are explained by CM theory. Known in principle (ideal structure of the GLV lattice), the explicit identification with the published constants is a useful clarification, not new mathematics. \\
9	H03 & A & GLV decomposition halves doublings; sub-scalars never exceed 128 bits & Known result reproduced & Max sub-scalar size 128 bits; 184 vs 304 group ops (GLV+wNAF vs wNAF), 2.07$\times$ vs double-and-add. \\	9	H03 & A & GLV decomposition halves doublings; sub-scalars never exceed 128 bits & Known result reproduced & Max sub-scalar size 128 bits; 184 vs 304 group ops (GLV+wNAF vs wNAF), 2.07$\times$ vs double-and-add. \\
10	−H04 & A & Automorphism orbits give exactly $\sqrt{\ }$6 on Pollard rho, with measurable fruitless-cycle overhead & Known result reproduced & 180 paired instances at 44--52 bits: iteration speed-up 2.21 [2.00, 2.45] (r = 128) and 2.42 [2.19, 2.70] (r = 20) vs $\sqrt{\ }$6 = 2.449; constant 0.499$\cdot$$\sqrt{\ }$n vs $\sqrt{\ }$($\pi$/12) = 0.512; negation alone 1.29 vs $\sqrt{\ }$2, $\varphi$-orbits alone 1.52 vs $\sqrt{\ }$3; fruitless cycles $\le$ 0.11 per 1000 iterations. Wall-clock speed-up only 0.95 (order-6) and 0.73 (negation) because canonicalisation costs 56--83 ns vs 38 ns per plain iteration in this engine. \\	10	+H04 & A & Automorphism orbits give exactly $\surd$6 on Pollard rho, with measurable fruitless-cycle overhead & Known result reproduced & 180 paired instances at 44--52 bits: iteration speed-up 2.21 [2.00, 2.45] (r = 128) and 2.42 [2.19, 2.70] (r = 20) vs $\surd$6 = 2.449; constant 0.499$\cdot$$\surd$n vs $\surd$($\pi$/12) = 0.512; negation alone 1.29 vs $\surd$2, $\varphi$-orbits alone 1.52 vs $\surd$3; fruitless cycles $\le$ 0.11 per 1000 iterations. Wall-clock speed-up only 0.95 (order-6) and 0.73 (negation) because canonicalisation costs 56--83 ns vs 38 ns per plain iteration in this engine. \\
11	−H05 & A & The automorphism orbit set cannot be made a group of order n/6 (rejected conjecture) & Rejected conjecture & Compatibility fails for 1500/1500 random pairs; proof: a congruence would make the orbit of O a subgroup H with cosets the other orbits, but orbits have size 6 ≠ \|H\| = 1. \\	11	+H05 & A & The automorphism orbit set cannot be made a group of order n/6 (rejected conjecture) & Rejected conjecture & Compatibility fails for 1500/1500 random pairs; proof: a congruence would make the orbit of O a subgroup H with cosets the other orbits, but orbits have size 6 $\ne$ \|H\| = 1. \\
12	−H06 & A & No known algebraic attack applies to secp256k1; prime-field index calculus with m = 2 costs ≫ $\sqrt{\ }$n & Known result reproduced & All exclusion criteria verified; measured decomposition rates match the Poisson prediction within sampling error; even with a free decomposition oracle the relation stage costs $\ge$ 2.4$\sqrt{\ }$n and the linear algebra \|F\|$^2$ ≫ $\sqrt{\ }$n. \\	12	+H06 & A & No known algebraic attack applies to secp256k1; prime-field index calculus with m = 2 costs $\gg$ $\surd$n & Known result reproduced & All exclusion criteria verified; measured decomposition rates match the Poisson prediction within sampling error; even with a free decomposition oracle the relation stage costs $\ge$ 2.4$\surd$n and the linear algebra \|F\|$^2$ $\gg$ $\surd$n. \\
13	−H07 & A & An exhaustive small-coefficient identity search finds only CM-explained relations and no cross-modulus or generator-specific relation & Empirical observation & 22 identities found, 22 explained, 0 unexplained, 0 false positives (expected chance hits 10^-73). \\	13	+H07 & A & An exhaustive small-coefficient identity search finds only CM-explained relations and no cross-modulus or generator-specific relation & Empirical observation & 22 identities found, 22 explained, 0 unexplained, 0 false positives (expected chance hits 10\^{}-73). \\
14	−H08 & B & Measured ECDLP cost scales as n^0.5 with constants matching random-mapping theory & Known result reproduced & 3 840 verified instances, 20--56 bits: fitted α $\in$ [0.478, 0.500] ($\ge$ 32 bits) for all seven configurations with CIs touching 0.5; pooled rho constant 1.254$\cdot$$\sqrt{\ }$n [1.21, 1.30] on 480 runs vs $\sqrt{\ }$($\pi$/2) = 1.2533; BSGS 1.50$\cdot$$\sqrt{\ }$n (x-keyed ±j table); kangaroo 1.94$\cdot$$\sqrt{\ }$n; Floyd 2.67$\cdot$$\sqrt{\ }$n, Brent 1.65$\cdot$$\sqrt{\ }$n. \\	14	+H08 & B & Measured ECDLP cost scales as n\^{}0.5 with constants matching random-mapping theory & Known result reproduced & 3 840 verified instances, 20--56 bits: fitted $\alpha$ $\in$ [0.478, 0.500] ($\ge$ 32 bits) for all seven configurations with CIs touching 0.5; pooled rho constant 1.254$\cdot$$\surd$n [1.21, 1.30] on 480 runs vs $\surd$($\pi$/2) = 1.2533; BSGS 1.50$\cdot$$\surd$n (x-keyed $\pm$j table); kangaroo 1.94$\cdot$$\surd$n; Floyd 2.67$\cdot$$\surd$n, Brent 1.65$\cdot$$\surd$n. \\
15	−H09 & B & Automated search over iteration-function designs cannot beat the random-mapping constant for a given class size & Rejected conjecture & 25 configurations $\times$ 80 instances: r = 2 and r = 3 walks cost 3.77$\cdot$$\sqrt{\ }$n and 2.26$\cdot$$\sqrt{\ }$n (negative control), r $\ge$ 8 cluster at 1.1--1.5$\cdot$$\sqrt{\ }$n with CIs overlapping $\sqrt{\ }$($\pi$/2); mixed walks indistinguishable; best cell r32 at 1.10 [0.92, 1.28] not significantly below the random-mapping constant. No generic iteration design beats the random-mapping floor. \\	15	+H09 & B & Automated search over iteration-function designs cannot beat the random-mapping constant for a given class size & Rejected conjecture & 25 configurations $\times$ 80 instances: r = 2 and r = 3 walks cost 3.77$\cdot$$\surd$n and 2.26$\cdot$$\surd$n (negative control), r $\ge$ 8 cluster at 1.1--1.5$\cdot$$\surd$n with CIs overlapping $\surd$($\pi$/2); mixed walks indistinguishable; best cell r32 at 1.10 [0.92, 1.28] not significantly below the random-mapping constant. No generic iteration design beats the random-mapping floor. \\
16	H10 & B & Parallel distinguished-point collision search has near-linear speed-up up to 28 threads & Known result reproduced & 56-bit instances on an Apple M3 Ultra: 14.8$\times$ on 16 threads (efficiency 0.93), 22.1$\times$ on 28 threads (0.79, P+E cores); total group operations within a factor 1.0 of single-thread. \\	16	H10 & B & Parallel distinguished-point collision search has near-linear speed-up up to 28 threads & Known result reproduced & 56-bit instances on an Apple M3 Ultra: 14.8$\times$ on 16 threads (efficiency 0.93), 22.1$\times$ on 28 threads (0.79, P+E cores); total group operations within a factor 1.0 of single-thread. \\
17	−H11 & B & Time--memory trade-off: BSGS with memory m costs m + n/m operations; rho with DP density θ stores $\approx$ θ$\cdot$$\sqrt{\ }$($\pi$n/2) points & Known result reproduced & BSGS cost matches m + n/(2m) within 7.8 \% for m from 2^10 to 2^20 at 36 bits; DP-rho at 40 bits spans 1.17--4.95 M operations as the DP density goes from 2^-12 (optimum, $\approx$ $\sqrt{\ }$($\pi$n/2)) to 2^-2 (restart-dominated) and 2^-14 (overshoot-dominated). \\	17	+H11 & B & Time--memory trade-off: BSGS with memory m costs m + n/m operations; rho with DP density $\theta$ stores $\approx$ $\theta$$\cdot$$\surd$($\pi$n/2) points & Known result reproduced & BSGS cost matches m + n/(2m) within 7.8 \% for m from 2\^{}10 to 2\^{}20 at 36 bits; DP-rho at 40 bits spans 1.17--4.95 M operations as the DP density goes from 2\^{}-12 (optimum, $\approx$ $\surd$($\pi$n/2)) to 2\^{}-2 (restart-dominated) and 2\^{}-14 (overshoot-dominated). \\
18	−H12 & B & Discrete logarithms with preprocessing: online cost $\approx$ 1.5$\cdot$$\sqrt{\ }$(n/T) after storing T distinguished points & Known result reproduced & Online/$\sqrt{\ }$(n/T) ratio 1.48--1.67 across T = 2^4 … 2^12 at 22 and 26 bits; per-instance speed-up 2.6$\times$ $\to$ 42$\times$ as predicted by $\sqrt{\ }$T scaling. \\	18	+H12 & B & Discrete logarithms with preprocessing: online cost $\approx$ 1.5$\cdot$$\surd$(n/T) after storing T distinguished points & Known result reproduced & Online/$\surd$(n/T) ratio 1.48--1.67 across T = 2\^{}4 \ldots{} 2\^{}12 at 22 and 26 bits; per-instance speed-up 2.6$\times$ $\to$ 42$\times$ as predicted by $\surd$T scaling. \\
19	−H13 & B & BIP340 batch verification reduces per-signature cost by a factor that grows with batch size and saturates & Known result reproduced & Per-signature cost falls from 24.5 µs (single, k256) to 7.9 µs at b = 2048 with Pippenger (S = 3.10 [3.05, 3.16]; 1.67$\times$ vs libsecp256k1 single verify); Straus plateaus at $\approx$ 2$\times$; $\approx$ 3 µs/sig of non-MSM work (lift\_x, tagged hash) caps the gain; negative control rejected; same shape on M3 Ultra. \\	19	+H13 & B & BIP340 batch verification reduces per-signature cost by a factor that grows with batch size and saturates & Known result reproduced & Per-signature cost falls from 24.5 $\mu$s (single, k256) to 7.9 $\mu$s at b = 2048 with Pippenger (S = 3.10 [3.05, 3.16]; 1.67$\times$ vs libsecp256k1 single verify); Straus plateaus at $\approx$ 2$\times$; $\approx$ 3 $\mu$s/sig of non-MSM work (lift\_x, tagged hash) caps the gain; negative control rejected; same shape on M3 Ultra. \\
20	−H14 & B & Implementation choice dominates signature performance: three orders of magnitude between pure Python and libsecp256k1 & Empirical observation & Schnorr verify: 7.4 ms (pure Python) vs 24.5 µs (k256) vs 13.2 µs (libsecp256k1): 560$\times$ spread; libsecp256k1 verifies 1.9$\times$ faster than k256 while k256 signs 1.8$\times$ faster (table-based generator multiplication 8.3 µs vs blinded ecmult\_gen 19.8 µs); ECDSA and Schnorr verification within 5 \% in libsecp256k1. \\	20	+H14 & B & Implementation choice dominates signature performance: three orders of magnitude between pure Python and libsecp256k1 & Empirical observation & Schnorr verify: 7.4 ms (pure Python) vs 24.5 $\mu$s (k256) vs 13.2 $\mu$s (libsecp256k1): 560$\times$ spread; libsecp256k1 verifies 1.9$\times$ faster than k256 while k256 signs 1.8$\times$ faster (table-based generator multiplication 8.3 $\mu$s vs blinded ecmult\_gen 19.8 $\mu$s); ECDSA and Schnorr verification within 5 \% in libsecp256k1. \\
21	−H15 & C & A single-bit message difference reaches full avalanche within a small number of steps & Pending & pending \\	21	+H15 & C & A single-bit message difference reaches full avalanche within a small number of steps & Known result reproduced & Full diffusion (mean flip ratio $\ge$ 0.49) at step 6 for a W\_0 bit, 11 for W\_5, 21 for W\_15 (6 steps after entry), 8 for an IV bit; identical over 3 seeds $\times$ 2000 messages; after 64 steps Hamming weight 128.0 $\pm$ 8.1 = random-oracle control. \\
22	−H16 & C & Statistically detectable input--output correlations vanish after a small number of steps & Pending & pending \\	22	+H16 & C & Statistically detectable input--output correlations vanish after a small number of steps & Empirical observation & N = 20 000 $\times$ 3 seeds: r $\le$ 3 trivially biased (untouched IV registers); r = 4 bias/$\chi$$^2$ at noise but 6--13 \|corr\| = 1 pairs (LSB of e\_1 affine in LSB of W\_0); from r = 5 all statistics at the random-oracle floor through r = 64 (two isolated 4.1$\sigma$ bits in 10 752 tests, as expected by chance). \\
23	−H17 & C & SAT preimage search on step-reduced SHA-256 scales exponentially in the number of steps and in the number of free bits & Pending & pending \\	23	+H17 & C & SAT preimage search on step-reduced SHA-256 scales exponentially in the number of steps and in the number of free bits & Empirical observation & 572 cells, all SAT answers re-hashed. r $\le$ 16: solved by propagation (0 conflicts, $\le$ 0.03 s) for any k. r $\ge$ 20: only k = 16 solved (CaDiCaL 6.4 s at r = 20, 87 s at r = 32, 262 s at r = 64 for 2/3 seeds); every k $\ge$ 24 cell times out at 300 s; Z3 2--4 orders of magnitude slower and times out at r $\ge$ 16. Generic SAT is slower than 2\^{}16 brute force once the expansion matters. \\
24	−H18 & C & Generic SAT encodings find step-reduced collisions only far below the published dedicated-tool records & Pending & pending \\	24	+H18 & C & Generic SAT encodings find step-reduced collisions only far below the published dedicated-tool records & Known result reproduced & 264 cells, 119 collisions verified. r = 4, 6, 8: UNSAT in all variants/solvers/seeds (72 runs) --- no collision within the words an 8-step compression reads. r = 10--16: 0-conflict collisions differing in exactly 9 consecutive words (a terminal local collision). r = 18: 53 s standard IV, 7--10 s semi-free-start. r $\ge$ 20: all timeouts. Largest 18 steps vs 28 (pure SAT, Alamgir et al. 2024), 31 (Li et al. 2024), 39 SFS. \\
25	−H19 & C & The 9-step local collision holds with probability 1 in the XOR-linearised model and with low, position-dependent probability in the real step function & Pending & pending \\	25	+H19 & C & The 9-step local collision holds with probability 1 in the XOR-linearised model and with low, position-dependent probability in the real step function & Known result reproduced & Pattern ($\delta$, $\Sigma$0$\delta$$\oplus$$\Sigma$1$\delta$, $\Sigma$1($\Sigma$0$\delta$), 0, $\delta$, $\Sigma$0$\delta$$\oplus$$\Sigma$1$\delta$, 0, 0, $\delta$) cancels in the linearised model for all $\delta$ (GF(2) check + Lean theorem localCollision\_absorb). Real step: 0 collisions in 32 $\times$ 100 000 samples (bound 3$\cdot$10$^{-5}$); survival after step i 0.25 (bits 0--30) / 1.0 (bit 31), after i+1 $\approx$ 10$^{-4}$, after i+2 zero. SAT finds conforming pairs for all 32 positions in 4.4--118 s, all verified. \\
26	−H20 & C & The SHA-256 step is a bijection on the state and the message schedule is invertible, so free-start and pseudo-preimage problems on the compression function are trivial & Known result reproduced & Machine-checked: stepInv ∘ step = id and step ∘ stepInv = id (per-component SAT lemmas, AIG 2048/2420), steps\_bijective for any number of rounds, scheduleStep\_inv and schedule\_backward; executable demonstration in tests/test\_core.py. Consequence (pseudo-preimages of the feed-forward-free compression function are free) stated informally. \\	26	+H20 & C & The SHA-256 step is a bijection on the state and the message schedule is invertible, so free-start and pseudo-preimage problems on the compression function are trivial & Known result reproduced & Machine-checked: stepInv $\circ$ step = id and step $\circ$ stepInv = id (per-component SAT lemmas, AIG 2048/2420), steps\_bijective for any number of rounds, scheduleStep\_inv and schedule\_backward; executable demonstration in tests/test\_core.py. Consequence (pseudo-preimages of the feed-forward-free compression function are free) stated informally. \\
27	−H21 & D & Lean 4 bv\_decide machine-checks the SHA-256 word-level identities used by optimised implementations & Known result reproduced & Lean 4.35 bv\_decide (LRAT certificates re-checked in Lean): Ch\_opt, Maj\_opt\_or, Maj\_opt\_xor, GF(2)-linearity of $\Sigma$0, $\Sigma$1, $\sigma$0, $\sigma$1, injectivity and explicit inverses ($\Sigma$0⁻¹ = XOR of 17 rotations) hence bijectivity; clean build 32 s, no sorry, no user axiom, no Mathlib. \\	27	+H21 & D & Lean 4 bv\_decide machine-checks the SHA-256 word-level identities used by optimised implementations & Known result reproduced & Lean 4.35 bv\_decide (LRAT certificates re-checked in Lean): Ch\_opt, Maj\_opt\_or, Maj\_opt\_xor, GF(2)-linearity of $\Sigma$0, $\Sigma$1, $\sigma$0, $\sigma$1, injectivity and explicit inverses ($\Sigma$0$^{-1}$ = XOR of 17 rotations) hence bijectivity; clean build 32 s, no sorry, no user axiom, no Mathlib. \\
28	−H22 & D & $\sigma$0 and $\sigma$1 are not injective on 32-bit words (kernel of positive dimension), unlike $\Sigma$0 and $\Sigma$1 & Rejected conjecture & Conjecture refuted: $\sigma$0 and $\sigma$1 are bijective (bv\_decide UNSAT certificates for injectivity; GF(2) rank 32 by two independent eliminations; explicit 32$\times$32 inverse matrices verified in Lean). The shift makes each summand singular (x≫3 has rank 29; rotr7$\oplus$rotr18 kills 0xFFFFFFFF) but the sum is a unit. A wrong belief caught by the formal layer. \\	28	+H22 & D & $\sigma$0 and $\sigma$1 are not injective on 32-bit words (kernel of positive dimension), unlike $\Sigma$0 and $\Sigma$1 & Rejected conjecture & Conjecture refuted: $\sigma$0 and $\sigma$1 are bijective (bv\_decide UNSAT certificates for injectivity; GF(2) rank 32 by two independent eliminations; explicit 32$\times$32 inverse matrices verified in Lean). The shift makes each summand singular (x$\gg$3 has rank 29; rotr7$\oplus$rotr18 kills 0xFFFFFFFF) but the sum is a unit. A wrong belief caught by the formal layer. \\
29	H23 & D & Cross-implementation agreement is a necessary gate: every arithmetic component is checked against at least one independent implementation & Empirical observation & 11 reference tests pass; agreement with 5 independent implementations; two development bugs caught by the gate (kangaroo retry loop, PARI output parsing). \\	29	H23 & D & Cross-implementation agreement is a necessary gate: every arithmetic component is checked against at least one independent implementation & Empirical observation & 11 reference tests pass; agreement with 5 independent implementations; two development bugs caught by the gate (kangaroo retry loop, PARI output parsing). \\
30	−H24 & D & The six-stage pipeline rediscovers known structure at a high rate and reports zero validated novel shortcuts & Pending & pending \\	30	+H24 & D & The six-stage pipeline rediscovers known structure at a high rate and reports zero validated novel shortcuts & Empirical observation & 25 hypotheses evaluated: 16 known results reproduced with measured constants, 6 empirical observations, 3 rejected conjectures (orbit quotient group; iteration-function shortcut; non-injectivity of $\sigma$0/$\sigma$1), 0 new verified results, 0 claims of weakness. Automation found one unrecorded closed form (GLV constants) and one wrong belief ($\sigma$0/$\sigma$1); the baseline (literature reading) would have left every constant unmeasured. \\
31	−H25 & D & ECDSA malleability and Schnorr correctness follow from the abstract group axioms alone (formalised) & Known result reproduced & Machine-checked in an axiomatised CyclicGroup structure (fields listed in formal/README.md): schnorr\_correct (s = k + e$\cdot$d mod n ⟹ s•G = R + e•P), ecdsa\_correct, ecdsa\_malleable ((r,s) valid ⟹ (r, n--s) valid, modular inverse as witness). Only propext/Quot.sound used. \\	31	+H25 & D & ECDSA malleability and Schnorr correctness follow from the abstract group axioms alone (formalised) & Known result reproduced & Machine-checked in an axiomatised CyclicGroup structure (fields listed in formal/README.md): schnorr\_correct (s = k + e$\cdot$d mod n $\Rightarrow$ s$\cdot$G = R + e$\cdot$P), ecdsa\_correct, ecdsa\_malleable ((r,s) valid $\Rightarrow$ (r, n--s) valid, modular inverse as witness). Only propext/Quot.sound used. \\
32	\end{longtable}	32	\end{longtable}

added paper/tables/numbers_sha.tex +38 −0

++% generated by scripts/make_sha_tables.py
++\newcommand{\shaDiffWzero}{6}
++\newcommand{\shaDiffWfive}{11}
++\newcommand{\shaDiffWfifteen}{21}
++\newcommand{\shaDiffIV}{8}
++\newcommand{\shaDiffN}{2000}
++\newcommand{\shaDiffHamming}{128.0}
++\newcommand{\shaDiffHammingSd}{8.1}
++\newcommand{\shaDiffRO}{0.500}
++\newcommand{\shaBiasN}{20000}
++\newcommand{\shaBiasFirstClean}{5}
++\newcommand{\shaBiasFirstNoBias}{4}
++\newcommand{\shaBiasExpectedPairs}{1.0}
++\newcommand{\shaPreCells}{572}
++\newcommand{\shaPreVerified}{all}
++\newcommand{\shaPreLargestCadical}{r=64, k=16}
++\newcommand{\shaPreZthreeLargest}{r=12, k=16}
++\newcommand{\shaPreRsixtyfourTime}{262}
++\newcommand{\shaPreRsixtyfourSolved}{2/3}
++\newcommand{\shaPreRtwentyTime}{6.4}
++\newcommand{\shaPreRsixteenConf}{0}
++\newcommand{\shaPreRsixteenTime}{0.02}
++\newcommand{\shaPreVars}{70\,802}
++\newcommand{\shaPreClauses}{314\,036}
++\newcommand{\shaColCells}{264}
++\newcommand{\shaColVerified}{all}
++\newcommand{\shaColUnsatCells}{24}
++\newcommand{\shaColLargestR}{18}
++\newcommand{\shaColFixedTime}{53}
++\newcommand{\shaColFreeTime}{8.5}
++\newcommand{\shaLcN}{100\,000}
++\newcommand{\shaLcBound}{3\times 10^{-5}}
++\newcommand{\shaLcSurvivalMsb}{1.00}
++\newcommand{\shaLcSurvivalOther}{0.250}
++\newcommand{\shaLcSatMin}{4.4}
++\newcommand{\shaLcSatMax}{118}
++\newcommand{\shaLcSatBits}{32}
++\newcommand{\shaLcPattern}{($\delta$, $\Sigma_0$($\delta$)$\oplus$$\Sigma_1$($\delta$), $\Sigma_1$($\Sigma_0$($\delta$)), 0, $\delta$, $\Sigma_0$($\delta$)$\oplus$$\Sigma_1$($\delta$), 0, 0, $\delta$)}

added paper/tables/sha_bias.tex +19 −0

++\resizebox{\textwidth}{!}{%
++\begin{tabular}{@{}rrrrr@{}}
++\toprule Steps $r$ & biased output bits ($>4\sigma$) & max $|$corr$|$ & (input, output) pairs $>4\sigma$ & bytes failing $\chi^2$ \\ \midrule
++1 & 192 & 1.000 & 5--13 & 24 \\
++2 & 128 & 1.000 & 7--12 & 16 \\
++3 & 64 & 1.000 & 5--13 & 8 \\
++4 & 0 & 1.000 & 6--13 & 0 \\
++5 & 0 & 0.028 & 0 & 0 \\
++6 & 0 & 0.033 & 0--1 & 0 \\
++8 & 0 & 0.029 & 0--1 & 0 \\
++10 & 0 & 0.029 & 0--1 & 0 \\
++12 & 0 & 0.029 & 0--1 & 0 \\
++16 & 0 & 0.029 & 0--2 & 0 \\
++20 & 0 & 0.030 & 1--3 & 0 \\
++24 & 0--1 & 0.032 & 0--2 & 0 \\
++32 & 0 & 0.032 & 0--1 & 0 \\
++64 & 0--1 & 0.031 & 0--3 & 0 \\
++\bottomrule
++\end{tabular}}

added paper/tables/sha_collision.tex +16 −0

++\resizebox{\textwidth}{!}{%
++\begin{tabular}{@{}rrrrrr@{}}
++\toprule Steps $r$ & CaDiCaL, std IV & Kissat, std IV & CaDiCaL, std IV + feed-forward & CaDiCaL, semi-free-start & Kissat, semi-free-start \\ \midrule
++4 & UNSAT (0.3) & UNSAT (0.1) & UNSAT (0.3) & UNSAT (0.7) & UNSAT (0.5) \\
++6 & UNSAT (3.0) & UNSAT (3.1) & UNSAT (2.1) & UNSAT (2.5) & UNSAT (2.1) \\
++8 & UNSAT (3.5) & UNSAT (4.7) & UNSAT (4.3) & UNSAT (3.8) & UNSAT (4.1) \\
++10 & 0.03 & 0.02 & 0.03 & 1.25 & 1.21 \\
++12 & 0.03 & 0.02 & 0.04 & 1.03 & 0.99 \\
++14 & 0.04 & 0.03 & 0.04 & 1.73 & 1.17 \\
++16 & 0.04 & 0.03 & 0.05 & 1.83 & 1.04 \\
++18 & 53 & 53 & 121 (2/3) & 8.49 & 7.09 \\
++20 & T(3) & T(3) & T(3) & T(3) & T(3) \\
++22 & T(3) & T(3) & T(3) & T(3) & T(3) \\
++24 & T(3) & T(3) & T(3) & T(3) & T(3) \\
++\bottomrule
++\end{tabular}}

added paper/tables/sha_diffusion.tex +11 −0

++\resizebox{\textwidth}{!}{%
++\begin{tabular}{@{}lrrrrrrrr@{}}
++\toprule Difference in & step 1 & 2 & 3 & 4 & 5 & 6 & 8 & first step $\ge 0.49$ \\ \midrule
++$W_0$ (one bit) & 0.015 & 0.097 & 0.217 & 0.341 & 0.451 & 0.494 & 0.499 & 6 \\
++$W_5$ (one bit) & 0.015 & 0.097 & 0.217 & 0.342 & 0.452 & 0.494 & 0.500 & 11 \\
++$W_{15}$ (one bit) & 0.015 & 0.097 & 0.217 & 0.342 & 0.452 & 0.495 & 0.500 & 21 \\
++IV register (one bit) & 0.018 & 0.072 & 0.162 & 0.271 & 0.378 & 0.448 & 0.497 & 8 \\
++\midrule
++random-oracle control & \multicolumn{7}{l}{0.500 $\pm$ 0.031 at every step} & 1 \\
++\bottomrule
++\end{tabular}}

added paper/tables/sha_preimage_cadical.tex +16 −0

++\resizebox{\textwidth}{!}{%
++\begin{tabular}{@{}rrrrrrrr@{}}
++\toprule Steps $r$ & $k=16$ & $k=24$ & $k=32$ & $k=40$ & $k=48$ & $k=56$ & $k=64$ \\ \midrule
++4 & 0.01 & 0.01 & 0.01 & 0.01 & 0.01 & 0.01 & 0.01 \\
++8 & 0.01 & 0.01 & 0.02 & 0.01 & 0.01 & 0.02 & 0.01 \\
++12 & 0.02 & 0.02 & 0.02 & 0.02 & 0.02 & 0.02 & 0.02 \\
++16 & 0.02 & 0.03 & 0.02 & 0.02 & 0.02 & 0.03 & 0.02 \\
++20 & 6.36 & T(2) & T(2) & T(2) & T(2) & T(2) & T(2) \\
++24 & 19 & T(2) & T(2) & T(2) & T(2) & T(2) & T(2) \\
++28 & 50 & T(2) & T(2) & T(2) & T(2) & T(2) & T(2) \\
++32 & 87 & T(2) & T(2) & T(2) & T(2) & T(2) & T(2) \\
++40 & 96 & T(2) & T(2) & T(2) & T(2) & T(2) & T(2) \\
++48 & T(3) & T(2) & T(2) & T(2) & T(2) & T(2) & T(2) \\
++64 & 262 (2/3) & T(2) & T(2) & T(2) & T(2) & T(2) & T(2) \\
++\bottomrule
++\end{tabular}}

added paper/tables/sha_preimage_kissat.tex +16 −0

++\resizebox{\textwidth}{!}{%
++\begin{tabular}{@{}rrrrrrrr@{}}
++\toprule Steps $r$ & $k=16$ & $k=24$ & $k=32$ & $k=40$ & $k=48$ & $k=56$ & $k=64$ \\ \midrule
++4 & 0.01 & 0.01 & 0.01 & 0.01 & 0.01 & 0.01 & 0.01 \\
++8 & 0.01 & 0.01 & 0.01 & 0.01 & 0.01 & 0.01 & 0.01 \\
++12 & 0.01 & 0.02 & 0.02 & 0.01 & 0.01 & 0.01 & 0.01 \\
++16 & 0.02 & 0.02 & 0.02 & 0.02 & 0.02 & 0.02 & 0.02 \\
++20 & 1.34 & T(2) & T(2) & T(2) & T(2) & T(2) & T(2) \\
++24 & 20 & T(2) & T(2) & T(2) & T(2) & T(2) & T(2) \\
++28 & 70 & T(2) & T(2) & T(2) & T(2) & T(2) & T(2) \\
++32 & 108 & T(2) & T(2) & T(2) & T(2) & T(2) & T(2) \\
++40 & 87 & T(2) & T(2) & T(2) & T(2) & T(2) & T(2) \\
++48 & 280 (2/3) & T(2) & T(2) & T(2) & T(2) & T(2) & T(2) \\
++64 & 250 (1/3) & T(2) & T(2) & T(2) & T(2) & T(2) & T(2) \\
++\bottomrule
++\end{tabular}}

added paper/tables/sha_preimage_spread.tex +16 −0

++\resizebox{\textwidth}{!}{%
++\begin{tabular}{@{}rrrrrrrr@{}}
++\toprule Steps $r$ & $k=16$ & $k=24$ & $k=32$ & $k=40$ & $k=48$ & $k=56$ & $k=64$ \\ \midrule
++4 & --- & --- & --- & --- & --- & --- & --- \\
++8 & --- & --- & --- & --- & --- & --- & --- \\
++12 & --- & --- & --- & --- & --- & --- & --- \\
++16 & --- & --- & --- & --- & --- & --- & --- \\
++20 & --- & --- & --- & --- & --- & --- & --- \\
++24 & --- & --- & --- & --- & --- & --- & --- \\
++28 & --- & --- & --- & --- & --- & --- & --- \\
++32 & --- & --- & --- & --- & --- & --- & --- \\
++40 & --- & --- & --- & --- & --- & --- & --- \\
++48 & --- & --- & --- & --- & --- & --- & --- \\
++64 & --- & --- & --- & --- & --- & --- & --- \\
++\bottomrule
++\end{tabular}}

added paper/tables/sha_preimage_z3.tex +16 −0

++\resizebox{\textwidth}{!}{%
++\begin{tabular}{@{}rrrrrrrr@{}}
++\toprule Steps $r$ & $k=16$ & $k=24$ & $k=32$ & $k=40$ & $k=48$ & $k=56$ & $k=64$ \\ \midrule
++4 & 0.01 & 0.01 & 0.01 & --- & --- & --- & --- \\
++8 & 2.00 & 233 (2/3) & T(3) & --- & --- & --- & --- \\
++12 & 128 & T(3) & T(3) & --- & --- & --- & --- \\
++16 & T(3) & T(3) & T(3) & --- & --- & --- & --- \\
++20 & --- & --- & --- & --- & --- & --- & --- \\
++24 & --- & --- & --- & --- & --- & --- & --- \\
++28 & --- & --- & --- & --- & --- & --- & --- \\
++32 & --- & --- & --- & --- & --- & --- & --- \\
++40 & --- & --- & --- & --- & --- & --- & --- \\
++48 & --- & --- & --- & --- & --- & --- & --- \\
++64 & --- & --- & --- & --- & --- & --- & --- \\
++\bottomrule
++\end{tabular}}

modified research_log/2026-11-01-sha256.md +58 −1

+ standalone 3.0.1 binary with `-t`, Kissat 4.0.4 with `--time`, both as subprocesses (one thread each); the driver has a
+ kill guard at timeout + 120 s.
++### 3a. Preimage scaling (572 cells on M3U96b; 351 cells with 3 seeds, 190 with 2, 31 with 1 — see README)
++
++Median wall time (s) per cell, placement `first` (free bits = low bits of W_0 then W_1), CaDiCaL / Kissat; "T" = all
++seeds timed out at 300 s; "x/3" = seeds solved:
++
++| r \ k | 16 | 24 | 32 | 40 | 48 | 56 | 64 |
++|---|---|---|---|---|---|---|---|
++| 4–16 | 0.01–0.03 / 0.01–0.02, **0 conflicts** (pure propagation = step inversion) | same | same | same | same | same | same |
++| 20 | 6.4 / 1.3 | T / T | T | T | T | T | T |
++| 24 | 19.3 / 20.1 | T | T | T | T | T | T |
++| 28 | 50.4 / 70.3 | T | T | T | T | T | T |
++| 32 | 86.7 / 107.6 | T | T | T | T | T | T |
++| 40 | 96.0 / 86.6 | T | T | T | T | T | T |
++| 48 | T (0/3) / 279.8 (2/3) | T | T | T | T | T | T |
++| 64 | 261.8 (2/3) / 300 (1/3 solved, 249.7 s) | T | T | T | T | T | T |
++
++Placement `spread` (CaDiCaL, bit i in word i mod 16): r <= 16 still trivial (<= 1 s, <= 22 k conflicts, since for
++r <= 16 the unused words carry most of the free bits), r = 20: k = 24 in 34 s and k = 32 in 55 s (2 seeds, 0.3–0.6 M
++conflicts), k >= 40 T; r = 24..48: only k = 16 (14 s .. 134 s); r = 64: T even for k = 16 (3 seeds).
++z3 (bit-vector theory, `r <= 16, k <= 32`): r = 4 instant; r = 8: k = 16 in 2.0 s, k = 24 in 233 s (2/3), k = 32 T;
++r = 12: k = 16 in 128 s, else T; r = 16: T for all k — two to four orders of magnitude slower than the CNF route on the same
++cells (CaDiCaL/Kissat solve every r <= 16 cell by propagation); z3's bit-blasting of the ripple-carry sums loses the
++structure that unit propagation exploits in the hand-made CNF. Peak RSS: <= 302 MB for CNF cells (64-step instance:
++70 802 vars / 314 036 clauses), <= 605 MB for z3. Every SAT answer re-hashed with the reference: `verified: true`
++(572/572 solved cells).
++
++Reading: (1) for r <= 16 the "preimage" of the compression function without unknown IV is not a search problem at all —
++the step function is invertible and both solvers find the answer with zero conflicts (this is the known
++invertibility of the Davies–Meyer core, not a solver result); (2) beyond 16 steps the only cells solved within 300 s have
++k = 16 free bits, i.e. a 2^16 brute-force space (~65 k compressions, milliseconds in C): on this grid SAT is **slower**
++than exhaustive search as soon as the message expansion is involved, and k = 24 (2^24, seconds by brute force) already
++times out at r = 20 for `first` placement; (3) seed-to-seed variance is large near the frontier (r = 48/64, k = 16:
++0–2 of 3 seeds solved). Classification: **known_reproduced / empirical_observation** (consistent with the literature on
++SAT-based preimages of SHA-256: solvers do not beat generic search beyond ~20 steps; cf. the 2^16 remark). No statement
++about full SHA-256 follows.
++
++### 3b. Collisions (264 cells = 11 step counts x 4 variants x 2 solvers x 3 seeds; 600 s)
++
++| r | standard IV | standard IV + ff | semi-free-start | semi-free-start + ff |
++|---|---|---|---|---|
++| 4, 6, 8 | **UNSAT** (3/3 seeds, both solvers; 0.1–4.7 s) | UNSAT | UNSAT | UNSAT |
++| 10–16 | SAT, 0.02–0.05 s, **0 conflicts** | SAT, 0 conflicts | SAT 0.7–2.4 s, 10–38 k conflicts | SAT 0.7–2.4 s |
++| 18 | SAT 52.8 / 53.2 s (CaDiCaL / Kissat), 0.9–1.0 M conflicts | SAT 120.8 (2/3) / 144.9 s, 2.0–2.7 M conflicts | SAT 8.5 / 7.1 s, 0.14 M conflicts | SAT 10.1 / 8.2 s |
++| 20, 22, 24 | T (all seeds, both solvers) | T | T | T |
++
++UNSAT for r <= 8 is a machine-checked statement: *no pair of distinct message blocks differing only in the words an
++r-step compression reads (W_0..W_{r-1}) collides after r <= 8 steps, for the standard IV and for any common IV* — this
++is the "a local collision needs 9 steps" fact (the difference injected into a and e must traverse the four-register
++shift twice) established here by exhaustive refutation (24 cell groups = 3 step counts x 4 variants x 2 solvers, 3 seeds each = 72 UNSAT runs). For r = 10..16 with the standard IV every collision found differs in exactly 9 consecutive words (W_1..W_9 for
++r = 10, W_3..W_11 for r = 12, W_5..W_13 for r = 14 (7 words non-zero), W_7..W_15 for r = 16; weight 77–90 bits) and
++is found by preprocessing + propagation alone: a 9-step local collision placed at the end of the computation, with the
++free prefix absorbing the conditions. At r = 18 the expanded words W_16, W_17 depend on the message and the solver needs
++~10^6 conflicts; all 16 words differ (weight ~250). At r >= 20 nothing is found in 600 s (the literature's practical
++collisions for 24–31 steps use dedicated differential tools and far more time; our generic encoding is not competitive,
++which is the expected answer to C4). All 119 collisions are saved (hex) and verified with the reference. Example at
++r = 18, standard IV, from the JSON (`largest_verified_collision_examples`). Classification: **known_reproduced** (9-step
++minimum, local-collision structure, 18-step practical collisions by generic SAT — cf. 18/20-step SAT collisions in the
++literature; UNSAT proofs for r <= 8 are a small **new_verified** by-product, though expected).
+ ## 4. 9-step local collision (C3, C4) — `local_collision.py`, laptop, N = 100 000 per bit, 943 s + 2nd run

added research_log/2026-11-01-synthesis.md +7 −0

++# 2026-11-01 — Synthesis, manuscript and critical review
++
++- All six sub-projects delivered (literature 129 refs; Rust ECDLP engine; signature benchmarks; SHA-256 grids on M3U96b; Lean 4 formal layer; ECDLP studies on M3U96a/M2U64). Every hypothesis file updated; registry: 16 known_reproduced, 6 empirical_observation, 3 rejected, 0 new_verified, 0 pending.
++- Two beliefs written from memory were corrected by the verification layers: σ0/σ1 are bijective (H22 rejected by bv_decide + GF(2) rank), and the local-collision correction vector needs Σ0δ ⊕ Σ1δ at step i+1 (Lean + Python agree).
++- Manuscript: 74 pages, 14 sections + 3 appendices, 16 figures (4 TikZ illustrative, 12 from data), 22 tables (all numeric tables generated by scripts), 0 undefined references, 0 undefined citations, 1 residual overfull box inside a TikZ figure.
++- Critical pass: generic-cost arithmetic corrected (√(π/12)·2^128 = 2^127.0; negation-map cost 2^127.8; gap to the 112-bit record 2^72; preprocessing example 2^176 offline / 2^96 entries); instance count unified at 6 240; TMTO optimum statement corrected (density 2^-8–2^-10).
++- Classification discipline: the GLV closed form is labelled "known structure, explicit form"; no result labelled new_verified.

modified research_log/discovery_log.jsonl +25 −25

				`@@ -1,25 +1,25 @@`
1	−{"id": "H01", "title": "Standardised secp256k1 parameters and GLV constants are exactly consistent", "axis": "A", "kind": "algebraic", "status": "evaluated", "classification": "known_reproduced", "verdict": "All 14 facts agree between Python and PARI/GP; (\u03b2, \u03bb\u00b2) mismatch confirmed as expected.", "evidence": ["results/baselines/secp256k1_facts.json"], "logged_utc": "2026-11-01T07:04:09+00:00"}	1	+{"id": "H01", "title": "Standardised secp256k1 parameters and GLV constants are exactly consistent", "axis": "A", "kind": "algebraic", "status": "evaluated", "classification": "known_reproduced", "verdict": "All 14 facts agree between Python and PARI/GP; (\u03b2, \u03bb\u00b2) mismatch confirmed as expected.", "evidence": ["results/baselines/secp256k1_facts.json"], "logged_utc": "2026-11-01T07:48:25+00:00"}
2	−{"id": "H02", "title": "End(E) = Z[\u03c9] and the GLV basis is the Eisenstein ideal (\u03c0\u0304 \u2212 1): closed form of the libsecp256k1 constants", "axis": "A", "kind": "algebraic", "status": "evaluated", "classification": "known_reproduced", "verdict": "Closed form holds exactly; all 22 identities found by the search are explained by CM theory. Known in principle (ideal structure of the GLV lattice), the explicit identification with the published constants is a useful clarification, not new mathematics.", "evidence": ["results/automated_discovery/identity_search.json", "results/baselines/secp256k1_facts.json"], "logged_utc": "2026-11-01T07:04:09+00:00"}	2	+{"id": "H02", "title": "End(E) = Z[\u03c9] and the GLV basis is the Eisenstein ideal (\u03c0\u0304 \u2212 1): closed form of the libsecp256k1 constants", "axis": "A", "kind": "algebraic", "status": "evaluated", "classification": "known_reproduced", "verdict": "Closed form holds exactly; all 22 identities found by the search are explained by CM theory. Known in principle (ideal structure of the GLV lattice), the explicit identification with the published constants is a useful clarification, not new mathematics.", "evidence": ["results/automated_discovery/identity_search.json", "results/baselines/secp256k1_facts.json"], "logged_utc": "2026-11-01T07:48:25+00:00"}
3	−{"id": "H03", "title": "GLV decomposition halves doublings; sub-scalars never exceed 128 bits", "axis": "A", "kind": "algebraic", "status": "evaluated", "classification": "known_reproduced", "verdict": "Max sub-scalar size 128 bits; 184 vs 304 group ops (GLV+wNAF vs wNAF), 2.07\u00d7 vs double-and-add.", "evidence": ["results/baselines/scalar_mult_opcount.json"], "logged_utc": "2026-11-01T07:04:09+00:00"}	3	+{"id": "H03", "title": "GLV decomposition halves doublings; sub-scalars never exceed 128 bits", "axis": "A", "kind": "algebraic", "status": "evaluated", "classification": "known_reproduced", "verdict": "Max sub-scalar size 128 bits; 184 vs 304 group ops (GLV+wNAF vs wNAF), 2.07\u00d7 vs double-and-add.", "evidence": ["results/baselines/scalar_mult_opcount.json"], "logged_utc": "2026-11-01T07:48:25+00:00"}
4	−{"id": "H04", "title": "Automorphism orbits give exactly \u221a6 on Pollard rho, with measurable fruitless-cycle overhead", "axis": "A", "kind": "algebraic", "status": "evaluated", "classification": "known_reproduced", "verdict": "180 paired instances at 44\u201352 bits: iteration speed-up 2.21 [2.00, 2.45] (r = 128) and 2.42 [2.19, 2.70] (r = 20) vs \u221a6 = 2.449; constant 0.499\u00b7\u221an vs \u221a(\u03c0/12) = 0.512; negation alone 1.29 vs \u221a2, \u03c6-orbits alone 1.52 vs \u221a3; fruitless cycles \u2264 0.11 per 1000 iterations. Wall-clock speed-up only 0.95 (order-6) and 0.73 (negation) because canonicalisation costs 56\u201383 ns vs 38 ns per plain iteration in this engine.", "evidence": ["results/synthetic_ecdlp/scaling_j0_M2U64.json", "results/synthetic_ecdlp/analysis.json"], "logged_utc": "2026-11-01T07:04:09+00:00"}	4	+{"id": "H04", "title": "Automorphism orbits give exactly \u221a6 on Pollard rho, with measurable fruitless-cycle overhead", "axis": "A", "kind": "algebraic", "status": "evaluated", "classification": "known_reproduced", "verdict": "180 paired instances at 44\u201352 bits: iteration speed-up 2.21 [2.00, 2.45] (r = 128) and 2.42 [2.19, 2.70] (r = 20) vs \u221a6 = 2.449; constant 0.499\u00b7\u221an vs \u221a(\u03c0/12) = 0.512; negation alone 1.29 vs \u221a2, \u03c6-orbits alone 1.52 vs \u221a3; fruitless cycles \u2264 0.11 per 1000 iterations. Wall-clock speed-up only 0.95 (order-6) and 0.73 (negation) because canonicalisation costs 56\u201383 ns vs 38 ns per plain iteration in this engine.", "evidence": ["results/synthetic_ecdlp/scaling_j0_M2U64.json", "results/synthetic_ecdlp/analysis.json"], "logged_utc": "2026-11-01T07:48:25+00:00"}
5	−{"id": "H05", "title": "The automorphism orbit set cannot be made a group of order n/6 (rejected conjecture)", "axis": "A", "kind": "algebraic", "status": "evaluated", "classification": "rejected", "verdict": "Compatibility fails for 1500/1500 random pairs; proof: a congruence would make the orbit of O a subgroup H with cosets the other orbits, but orbits have size 6 \u2260 \|H\| = 1.", "evidence": ["results/theory/orbit_quotient_counterexample.json"], "logged_utc": "2026-11-01T07:04:09+00:00"}	5	+{"id": "H05", "title": "The automorphism orbit set cannot be made a group of order n/6 (rejected conjecture)", "axis": "A", "kind": "algebraic", "status": "evaluated", "classification": "rejected", "verdict": "Compatibility fails for 1500/1500 random pairs; proof: a congruence would make the orbit of O a subgroup H with cosets the other orbits, but orbits have size 6 \u2260 \|H\| = 1.", "evidence": ["results/theory/orbit_quotient_counterexample.json"], "logged_utc": "2026-11-01T07:48:25+00:00"}
6	−{"id": "H06", "title": "No known algebraic attack applies to secp256k1; prime-field index calculus with m = 2 costs \u226b \u221an", "axis": "A", "kind": "algebraic", "status": "evaluated", "classification": "known_reproduced", "verdict": "All exclusion criteria verified; measured decomposition rates match the Poisson prediction within sampling error; even with a free decomposition oracle the relation stage costs \u2265 2.4\u221an and the linear algebra \|F\|\u00b2 \u226b \u221an.", "evidence": ["results/baselines/secp256k1_facts.json", "results/synthetic_ecdlp/index_calculus_probe.json"], "logged_utc": "2026-11-01T07:04:09+00:00"}	6	+{"id": "H06", "title": "No known algebraic attack applies to secp256k1; prime-field index calculus with m = 2 costs \u226b \u221an", "axis": "A", "kind": "algebraic", "status": "evaluated", "classification": "known_reproduced", "verdict": "All exclusion criteria verified; measured decomposition rates match the Poisson prediction within sampling error; even with a free decomposition oracle the relation stage costs \u2265 2.4\u221an and the linear algebra \|F\|\u00b2 \u226b \u221an.", "evidence": ["results/baselines/secp256k1_facts.json", "results/synthetic_ecdlp/index_calculus_probe.json"], "logged_utc": "2026-11-01T07:48:25+00:00"}
7	−{"id": "H07", "title": "An exhaustive small-coefficient identity search finds only CM-explained relations and no cross-modulus or generator-specific relation", "axis": "A", "kind": "algebraic", "status": "evaluated", "classification": "empirical_observation", "verdict": "22 identities found, 22 explained, 0 unexplained, 0 false positives (expected chance hits 10^-73).", "evidence": ["results/automated_discovery/identity_search.json"], "logged_utc": "2026-11-01T07:04:09+00:00"}	7	+{"id": "H07", "title": "An exhaustive small-coefficient identity search finds only CM-explained relations and no cross-modulus or generator-specific relation", "axis": "A", "kind": "algebraic", "status": "evaluated", "classification": "empirical_observation", "verdict": "22 identities found, 22 explained, 0 unexplained, 0 false positives (expected chance hits 10^-73).", "evidence": ["results/automated_discovery/identity_search.json"], "logged_utc": "2026-11-01T07:48:25+00:00"}
8	−{"id": "H08", "title": "Measured ECDLP cost scales as n^0.5 with constants matching random-mapping theory", "axis": "B", "kind": "algorithmic", "status": "evaluated", "classification": "known_reproduced", "verdict": "3 840 verified instances, 20\u201356 bits: fitted \u03b1 \u2208 [0.478, 0.500] (\u2265 32 bits) for all seven configurations with CIs touching 0.5; pooled rho constant 1.254\u00b7\u221an [1.21, 1.30] on 480 runs vs \u221a(\u03c0/2) = 1.2533; BSGS 1.50\u00b7\u221an (x-keyed \u00b1j table); kangaroo 1.94\u00b7\u221an; Floyd 2.67\u00b7\u221an, Brent 1.65\u00b7\u221an.", "evidence": ["results/synthetic_ecdlp/scaling_generic_M3U96a.json", "results/synthetic_ecdlp/scaling_j0_M2U64.json", "results/synthetic_ecdlp/analysis.json"], "logged_utc": "2026-11-01T07:04:09+00:00"}	8	+{"id": "H08", "title": "Measured ECDLP cost scales as n^0.5 with constants matching random-mapping theory", "axis": "B", "kind": "algorithmic", "status": "evaluated", "classification": "known_reproduced", "verdict": "3 840 verified instances, 20\u201356 bits: fitted \u03b1 \u2208 [0.478, 0.500] (\u2265 32 bits) for all seven configurations with CIs touching 0.5; pooled rho constant 1.254\u00b7\u221an [1.21, 1.30] on 480 runs vs \u221a(\u03c0/2) = 1.2533; BSGS 1.50\u00b7\u221an (x-keyed \u00b1j table); kangaroo 1.94\u00b7\u221an; Floyd 2.67\u00b7\u221an, Brent 1.65\u00b7\u221an.", "evidence": ["results/synthetic_ecdlp/scaling_generic_M3U96a.json", "results/synthetic_ecdlp/scaling_j0_M2U64.json", "results/synthetic_ecdlp/analysis.json"], "logged_utc": "2026-11-01T07:48:25+00:00"}
9	−{"id": "H09", "title": "Automated search over iteration-function designs cannot beat the random-mapping constant for a given class size", "axis": "B", "kind": "algorithmic", "status": "evaluated", "classification": "rejected", "verdict": "25 configurations \u00d7 80 instances: r = 2 and r = 3 walks cost 3.77\u00b7\u221an and 2.26\u00b7\u221an (negative control), r \u2265 8 cluster at 1.1\u20131.5\u00b7\u221an with CIs overlapping \u221a(\u03c0/2); mixed walks indistinguishable; best cell r32 at 1.10 [0.92, 1.28] not significantly below the random-mapping constant. No generic iteration design beats the random-mapping floor.", "evidence": ["results/synthetic_ecdlp/sweep_r_M3U96a.json", "results/synthetic_ecdlp/analysis.json"], "logged_utc": "2026-11-01T07:04:09+00:00"}	9	+{"id": "H09", "title": "Automated search over iteration-function designs cannot beat the random-mapping constant for a given class size", "axis": "B", "kind": "algorithmic", "status": "evaluated", "classification": "rejected", "verdict": "25 configurations \u00d7 80 instances: r = 2 and r = 3 walks cost 3.77\u00b7\u221an and 2.26\u00b7\u221an (negative control), r \u2265 8 cluster at 1.1\u20131.5\u00b7\u221an with CIs overlapping \u221a(\u03c0/2); mixed walks indistinguishable; best cell r32 at 1.10 [0.92, 1.28] not significantly below the random-mapping constant. No generic iteration design beats the random-mapping floor.", "evidence": ["results/synthetic_ecdlp/sweep_r_M3U96a.json", "results/synthetic_ecdlp/analysis.json"], "logged_utc": "2026-11-01T07:48:25+00:00"}
10	−{"id": "H10", "title": "Parallel distinguished-point collision search has near-linear speed-up up to 28 threads", "axis": "B", "kind": "algorithmic", "status": "evaluated", "classification": "known_reproduced", "verdict": "56-bit instances on an Apple M3 Ultra: 14.8\u00d7 on 16 threads (efficiency 0.93), 22.1\u00d7 on 28 threads (0.79, P+E cores); total group operations within a factor 1.0 of single-thread.", "evidence": ["results/synthetic_ecdlp/parallel_M3U96a.json", "results/synthetic_ecdlp/analysis.json"], "logged_utc": "2026-11-01T07:04:09+00:00"}	10	+{"id": "H10", "title": "Parallel distinguished-point collision search has near-linear speed-up up to 28 threads", "axis": "B", "kind": "algorithmic", "status": "evaluated", "classification": "known_reproduced", "verdict": "56-bit instances on an Apple M3 Ultra: 14.8\u00d7 on 16 threads (efficiency 0.93), 22.1\u00d7 on 28 threads (0.79, P+E cores); total group operations within a factor 1.0 of single-thread.", "evidence": ["results/synthetic_ecdlp/parallel_M3U96a.json", "results/synthetic_ecdlp/analysis.json"], "logged_utc": "2026-11-01T07:48:25+00:00"}
11	−{"id": "H11", "title": "Time\u2013memory trade-off: BSGS with memory m costs m + n/m operations; rho with DP density \u03b8 stores \u2248 \u03b8\u00b7\u221a(\u03c0n/2) points", "axis": "B", "kind": "algorithmic", "status": "evaluated", "classification": "known_reproduced", "verdict": "BSGS cost matches m + n/(2m) within 7.8 % for m from 2^10 to 2^20 at 36 bits; DP-rho at 40 bits spans 1.17\u20134.95 M operations as the DP density goes from 2^-12 (optimum, \u2248 \u221a(\u03c0n/2)) to 2^-2 (restart-dominated) and 2^-14 (overshoot-dominated).", "evidence": ["results/synthetic_ecdlp/tmto_M2U64.json", "results/synthetic_ecdlp/analysis.json"], "logged_utc": "2026-11-01T07:04:09+00:00"}	11	+{"id": "H11", "title": "Time\u2013memory trade-off: BSGS with memory m costs m + n/m operations; rho with DP density \u03b8 stores \u2248 \u03b8\u00b7\u221a(\u03c0n/2) points", "axis": "B", "kind": "algorithmic", "status": "evaluated", "classification": "known_reproduced", "verdict": "BSGS cost matches m + n/(2m) within 7.8 % for m from 2^10 to 2^20 at 36 bits; DP-rho at 40 bits spans 1.17\u20134.95 M operations as the DP density goes from 2^-12 (optimum, \u2248 \u221a(\u03c0n/2)) to 2^-2 (restart-dominated) and 2^-14 (overshoot-dominated).", "evidence": ["results/synthetic_ecdlp/tmto_M2U64.json", "results/synthetic_ecdlp/analysis.json"], "logged_utc": "2026-11-01T07:48:25+00:00"}
12	−{"id": "H12", "title": "Discrete logarithms with preprocessing: online cost \u2248 1.5\u00b7\u221a(n/T) after storing T distinguished points", "axis": "B", "kind": "algorithmic", "status": "evaluated", "classification": "known_reproduced", "verdict": "Online/\u221a(n/T) ratio 1.48\u20131.67 across T = 2^4 \u2026 2^12 at 22 and 26 bits; per-instance speed-up 2.6\u00d7 \u2192 42\u00d7 as predicted by \u221aT scaling.", "evidence": ["results/synthetic_ecdlp/preprocessing_python.json"], "logged_utc": "2026-11-01T07:04:09+00:00"}	12	+{"id": "H12", "title": "Discrete logarithms with preprocessing: online cost \u2248 1.5\u00b7\u221a(n/T) after storing T distinguished points", "axis": "B", "kind": "algorithmic", "status": "evaluated", "classification": "known_reproduced", "verdict": "Online/\u221a(n/T) ratio 1.48\u20131.67 across T = 2^4 \u2026 2^12 at 22 and 26 bits; per-instance speed-up 2.6\u00d7 \u2192 42\u00d7 as predicted by \u221aT scaling.", "evidence": ["results/synthetic_ecdlp/preprocessing_python.json"], "logged_utc": "2026-11-01T07:48:25+00:00"}
13	−{"id": "H13", "title": "BIP340 batch verification reduces per-signature cost by a factor that grows with batch size and saturates", "axis": "B", "kind": "algorithmic", "status": "evaluated", "classification": "known_reproduced", "verdict": "Per-signature cost falls from 24.5 \u00b5s (single, k256) to 7.9 \u00b5s at b = 2048 with Pippenger (S = 3.10 [3.05, 3.16]; 1.67\u00d7 vs libsecp256k1 single verify); Straus plateaus at \u2248 2\u00d7; \u2248 3 \u00b5s/sig of non-MSM work (lift_x, tagged hash) caps the gain; negative control rejected; same shape on M3 Ultra.", "evidence": ["results/signature_benchmarks/summary.json", "results/signature_benchmarks/bench_MacBookPro-de-simon-pierre-2.json", "results/signature_benchmarks/bench_MacStudnpierre2.json"], "logged_utc": "2026-11-01T07:04:09+00:00"}	13	+{"id": "H13", "title": "BIP340 batch verification reduces per-signature cost by a factor that grows with batch size and saturates", "axis": "B", "kind": "algorithmic", "status": "evaluated", "classification": "known_reproduced", "verdict": "Per-signature cost falls from 24.5 \u00b5s (single, k256) to 7.9 \u00b5s at b = 2048 with Pippenger (S = 3.10 [3.05, 3.16]; 1.67\u00d7 vs libsecp256k1 single verify); Straus plateaus at \u2248 2\u00d7; \u2248 3 \u00b5s/sig of non-MSM work (lift_x, tagged hash) caps the gain; negative control rejected; same shape on M3 Ultra.", "evidence": ["results/signature_benchmarks/summary.json", "results/signature_benchmarks/bench_MacBookPro-de-simon-pierre-2.json", "results/signature_benchmarks/bench_MacStudnpierre2.json"], "logged_utc": "2026-11-01T07:48:25+00:00"}
14	−{"id": "H14", "title": "Implementation choice dominates signature performance: three orders of magnitude between pure Python and libsecp256k1", "axis": "B", "kind": "algorithmic", "status": "evaluated", "classification": "empirical_observation", "verdict": "Schnorr verify: 7.4 ms (pure Python) vs 24.5 \u00b5s (k256) vs 13.2 \u00b5s (libsecp256k1): 560\u00d7 spread; libsecp256k1 verifies 1.9\u00d7 faster than k256 while k256 signs 1.8\u00d7 faster (table-based generator multiplication 8.3 \u00b5s vs blinded ecmult_gen 19.8 \u00b5s); ECDSA and Schnorr verification within 5 % in libsecp256k1.", "evidence": ["results/signature_benchmarks/summary.json"], "logged_utc": "2026-11-01T07:04:09+00:00"}	14	+{"id": "H14", "title": "Implementation choice dominates signature performance: three orders of magnitude between pure Python and libsecp256k1", "axis": "B", "kind": "algorithmic", "status": "evaluated", "classification": "empirical_observation", "verdict": "Schnorr verify: 7.4 ms (pure Python) vs 24.5 \u00b5s (k256) vs 13.2 \u00b5s (libsecp256k1): 560\u00d7 spread; libsecp256k1 verifies 1.9\u00d7 faster than k256 while k256 signs 1.8\u00d7 faster (table-based generator multiplication 8.3 \u00b5s vs blinded ecmult_gen 19.8 \u00b5s); ECDSA and Schnorr verification within 5 % in libsecp256k1.", "evidence": ["results/signature_benchmarks/summary.json"], "logged_utc": "2026-11-01T07:48:25+00:00"}
15	−{"id": "H15", "title": "A single-bit message difference reaches full avalanche within a small number of steps", "axis": "C", "kind": "sha256", "status": "running", "classification": "pending", "verdict": "pending", "evidence": [], "logged_utc": "2026-11-01T07:04:09+00:00"}	15	+{"id": "H15", "title": "A single-bit message difference reaches full avalanche within a small number of steps", "axis": "C", "kind": "sha256", "status": "evaluated", "classification": "known_reproduced", "verdict": "Full diffusion (mean flip ratio \u2265 0.49) at step 6 for a W_0 bit, 11 for W_5, 21 for W_15 (6 steps after entry), 8 for an IV bit; identical over 3 seeds \u00d7 2000 messages; after 64 steps Hamming weight 128.0 \u00b1 8.1 = random-oracle control.", "evidence": ["results/reduced_round_sha256/summary.json", "results/reduced_round_sha256/diffusion_seed1.json"], "logged_utc": "2026-11-01T07:48:25+00:00"}
16	−{"id": "H16", "title": "Statistically detectable input\u2013output correlations vanish after a small number of steps", "axis": "C", "kind": "sha256", "status": "running", "classification": "pending", "verdict": "pending", "evidence": [], "logged_utc": "2026-11-01T07:04:09+00:00"}	16	+{"id": "H16", "title": "Statistically detectable input\u2013output correlations vanish after a small number of steps", "axis": "C", "kind": "sha256", "status": "evaluated", "classification": "empirical_observation", "verdict": "N = 20 000 \u00d7 3 seeds: r \u2264 3 trivially biased (untouched IV registers); r = 4 bias/\u03c7\u00b2 at noise but 6\u201313 \|corr\| = 1 pairs (LSB of e_1 affine in LSB of W_0); from r = 5 all statistics at the random-oracle floor through r = 64 (two isolated 4.1\u03c3 bits in 10 752 tests, as expected by chance).", "evidence": ["results/reduced_round_sha256/summary.json", "results/reduced_round_sha256/bias_seed1.json"], "logged_utc": "2026-11-01T07:48:25+00:00"}
17	−{"id": "H17", "title": "SAT preimage search on step-reduced SHA-256 scales exponentially in the number of steps and in the number of free bits", "axis": "C", "kind": "sha256", "status": "running", "classification": "pending", "verdict": "pending", "evidence": [], "logged_utc": "2026-11-01T07:04:09+00:00"}	17	+{"id": "H17", "title": "SAT preimage search on step-reduced SHA-256 scales exponentially in the number of steps and in the number of free bits", "axis": "C", "kind": "sha256", "status": "evaluated", "classification": "empirical_observation", "verdict": "572 cells, all SAT answers re-hashed. r \u2264 16: solved by propagation (0 conflicts, \u2264 0.03 s) for any k. r \u2265 20: only k = 16 solved (CaDiCaL 6.4 s at r = 20, 87 s at r = 32, 262 s at r = 64 for 2/3 seeds); every k \u2265 24 cell times out at 300 s; Z3 2\u20134 orders of magnitude slower and times out at r \u2265 16. Generic SAT is slower than 2^16 brute force once the expansion matters.", "evidence": ["results/reduced_round_sha256/summary.json", "results/reduced_round_sha256/preimage_sat_scaling.json"], "logged_utc": "2026-11-01T07:48:25+00:00"}
18	−{"id": "H18", "title": "Generic SAT encodings find step-reduced collisions only far below the published dedicated-tool records", "axis": "C", "kind": "sha256", "status": "running", "classification": "pending", "verdict": "pending", "evidence": [], "logged_utc": "2026-11-01T07:04:09+00:00"}	18	+{"id": "H18", "title": "Generic SAT encodings find step-reduced collisions only far below the published dedicated-tool records", "axis": "C", "kind": "sha256", "status": "evaluated", "classification": "known_reproduced", "verdict": "264 cells, 119 collisions verified. r = 4, 6, 8: UNSAT in all variants/solvers/seeds (72 runs) \u2014 no collision within the words an 8-step compression reads. r = 10\u201316: 0-conflict collisions differing in exactly 9 consecutive words (a terminal local collision). r = 18: 53 s standard IV, 7\u201310 s semi-free-start. r \u2265 20: all timeouts. Largest 18 steps vs 28 (pure SAT, Alamgir et al. 2024), 31 (Li et al. 2024), 39 SFS.", "evidence": ["results/reduced_round_sha256/summary.json", "results/reduced_round_sha256/collision_sat.json"], "logged_utc": "2026-11-01T07:48:25+00:00"}
19	−{"id": "H19", "title": "The 9-step local collision holds with probability 1 in the XOR-linearised model and with low, position-dependent probability in the real step function", "axis": "C", "kind": "sha256", "status": "running", "classification": "pending", "verdict": "pending", "evidence": [], "logged_utc": "2026-11-01T07:04:09+00:00"}	19	+{"id": "H19", "title": "The 9-step local collision holds with probability 1 in the XOR-linearised model and with low, position-dependent probability in the real step function", "axis": "C", "kind": "sha256", "status": "evaluated", "classification": "known_reproduced", "verdict": "Pattern (\u03b4, \u03a30\u03b4\u2295\u03a31\u03b4, \u03a31(\u03a30\u03b4), 0, \u03b4, \u03a30\u03b4\u2295\u03a31\u03b4, 0, 0, \u03b4) cancels in the linearised model for all \u03b4 (GF(2) check + Lean theorem localCollision_absorb). Real step: 0 collisions in 32 \u00d7 100 000 samples (bound 3\u00b710\u207b\u2075); survival after step i 0.25 (bits 0\u201330) / 1.0 (bit 31), after i+1 \u2248 10\u207b\u2074, after i+2 zero. SAT finds conforming pairs for all 32 positions in 4.4\u2013118 s, all verified.", "evidence": ["results/reduced_round_sha256/summary.json", "results/reduced_round_sha256/local_collision.json", "formal/README.md"], "logged_utc": "2026-11-01T07:48:25+00:00"}
20	−{"id": "H20", "title": "The SHA-256 step is a bijection on the state and the message schedule is invertible, so free-start and pseudo-preimage problems on the compression function are trivial", "axis": "C", "kind": "sha256", "status": "evaluated", "classification": "known_reproduced", "verdict": "Machine-checked: stepInv \u2218 step = id and step \u2218 stepInv = id (per-component SAT lemmas, AIG 2048/2420), steps_bijective for any number of rounds, scheduleStep_inv and schedule_backward; executable demonstration in tests/test_core.py. Consequence (pseudo-preimages of the feed-forward-free compression function are free) stated informally.", "evidence": ["formal/README.md", "formal/build.log", "tests/test_formal_lean.py", "tests/test_core.py"], "logged_utc": "2026-11-01T07:04:09+00:00"}	20	+{"id": "H20", "title": "The SHA-256 step is a bijection on the state and the message schedule is invertible, so free-start and pseudo-preimage problems on the compression function are trivial", "axis": "C", "kind": "sha256", "status": "evaluated", "classification": "known_reproduced", "verdict": "Machine-checked: stepInv \u2218 step = id and step \u2218 stepInv = id (per-component SAT lemmas, AIG 2048/2420), steps_bijective for any number of rounds, scheduleStep_inv and schedule_backward; executable demonstration in tests/test_core.py. Consequence (pseudo-preimages of the feed-forward-free compression function are free) stated informally.", "evidence": ["formal/README.md", "formal/build.log", "tests/test_formal_lean.py", "tests/test_core.py"], "logged_utc": "2026-11-01T07:48:25+00:00"}
21	−{"id": "H21", "title": "Lean 4 bv_decide machine-checks the SHA-256 word-level identities used by optimised implementations", "axis": "D", "kind": "formal", "status": "evaluated", "classification": "known_reproduced", "verdict": "Lean 4.35 bv_decide (LRAT certificates re-checked in Lean): Ch_opt, Maj_opt_or, Maj_opt_xor, GF(2)-linearity of \u03a30, \u03a31, \u03c30, \u03c31, injectivity and explicit inverses (\u03a30\u207b\u00b9 = XOR of 17 rotations) hence bijectivity; clean build 32 s, no sorry, no user axiom, no Mathlib.", "evidence": ["formal/README.md", "formal/build.log", "tests/test_formal_lean.py"], "logged_utc": "2026-11-01T07:04:09+00:00"}	21	+{"id": "H21", "title": "Lean 4 bv_decide machine-checks the SHA-256 word-level identities used by optimised implementations", "axis": "D", "kind": "formal", "status": "evaluated", "classification": "known_reproduced", "verdict": "Lean 4.35 bv_decide (LRAT certificates re-checked in Lean): Ch_opt, Maj_opt_or, Maj_opt_xor, GF(2)-linearity of \u03a30, \u03a31, \u03c30, \u03c31, injectivity and explicit inverses (\u03a30\u207b\u00b9 = XOR of 17 rotations) hence bijectivity; clean build 32 s, no sorry, no user axiom, no Mathlib.", "evidence": ["formal/README.md", "formal/build.log", "tests/test_formal_lean.py"], "logged_utc": "2026-11-01T07:48:25+00:00"}
22	−{"id": "H22", "title": "\u03c30 and \u03c31 are not injective on 32-bit words (kernel of positive dimension), unlike \u03a30 and \u03a31", "axis": "D", "kind": "formal", "status": "evaluated", "classification": "rejected", "verdict": "Conjecture refuted: \u03c30 and \u03c31 are bijective (bv_decide UNSAT certificates for injectivity; GF(2) rank 32 by two independent eliminations; explicit 32\u00d732 inverse matrices verified in Lean). The shift makes each summand singular (x\u226b3 has rank 29; rotr7\u2295rotr18 kills 0xFFFFFFFF) but the sum is a unit. A wrong belief caught by the formal layer.", "evidence": ["formal/README.md", "formal/build.log", "tests/test_formal_lean.py", "formal/scripts/gf2_rank.py"], "logged_utc": "2026-11-01T07:04:09+00:00"}	22	+{"id": "H22", "title": "\u03c30 and \u03c31 are not injective on 32-bit words (kernel of positive dimension), unlike \u03a30 and \u03a31", "axis": "D", "kind": "formal", "status": "evaluated", "classification": "rejected", "verdict": "Conjecture refuted: \u03c30 and \u03c31 are bijective (bv_decide UNSAT certificates for injectivity; GF(2) rank 32 by two independent eliminations; explicit 32\u00d732 inverse matrices verified in Lean). The shift makes each summand singular (x\u226b3 has rank 29; rotr7\u2295rotr18 kills 0xFFFFFFFF) but the sum is a unit. A wrong belief caught by the formal layer.", "evidence": ["formal/README.md", "formal/build.log", "tests/test_formal_lean.py", "formal/scripts/gf2_rank.py"], "logged_utc": "2026-11-01T07:48:25+00:00"}
23	−{"id": "H23", "title": "Cross-implementation agreement is a necessary gate: every arithmetic component is checked against at least one independent implementation", "axis": "D", "kind": "methodology", "status": "evaluated", "classification": "empirical_observation", "verdict": "11 reference tests pass; agreement with 5 independent implementations; two development bugs caught by the gate (kangaroo retry loop, PARI output parsing).", "evidence": ["tests/test_core.py", "tests/test_dlp_reference.py"], "logged_utc": "2026-11-01T07:04:09+00:00"}	23	+{"id": "H23", "title": "Cross-implementation agreement is a necessary gate: every arithmetic component is checked against at least one independent implementation", "axis": "D", "kind": "methodology", "status": "evaluated", "classification": "empirical_observation", "verdict": "11 reference tests pass; agreement with 5 independent implementations; two development bugs caught by the gate (kangaroo retry loop, PARI output parsing).", "evidence": ["tests/test_core.py", "tests/test_dlp_reference.py"], "logged_utc": "2026-11-01T07:48:25+00:00"}
24	−{"id": "H24", "title": "The six-stage pipeline rediscovers known structure at a high rate and reports zero validated novel shortcuts", "axis": "D", "kind": "methodology", "status": "running", "classification": "pending", "verdict": "pending", "evidence": [], "logged_utc": "2026-11-01T07:04:09+00:00"}	24	+{"id": "H24", "title": "The six-stage pipeline rediscovers known structure at a high rate and reports zero validated novel shortcuts", "axis": "D", "kind": "methodology", "status": "evaluated", "classification": "empirical_observation", "verdict": "25 hypotheses evaluated: 16 known results reproduced with measured constants, 6 empirical observations, 3 rejected conjectures (orbit quotient group; iteration-function shortcut; non-injectivity of \u03c30/\u03c31), 0 new verified results, 0 claims of weakness. Automation found one unrecorded closed form (GLV constants) and one wrong belief (\u03c30/\u03c31); the baseline (literature reading) would have left every constant unmeasured.", "evidence": ["research_log/discovery_log.jsonl", "results/automated_discovery/hypothesis_summary.json"], "logged_utc": "2026-11-01T07:48:25+00:00"}
25	−{"id": "H25", "title": "ECDSA malleability and Schnorr correctness follow from the abstract group axioms alone (formalised)", "axis": "D", "kind": "formal", "status": "evaluated", "classification": "known_reproduced", "verdict": "Machine-checked in an axiomatised CyclicGroup structure (fields listed in formal/README.md): schnorr_correct (s = k + e\u00b7d mod n \u27f9 s\u2022G = R + e\u2022P), ecdsa_correct, ecdsa_malleable ((r,s) valid \u27f9 (r, n\u2212s) valid, modular inverse as witness). Only propext/Quot.sound used.", "evidence": ["formal/README.md", "formal/build.log", "tests/test_formal_lean.py"], "logged_utc": "2026-11-01T07:04:09+00:00"}	25	+{"id": "H25", "title": "ECDSA malleability and Schnorr correctness follow from the abstract group axioms alone (formalised)", "axis": "D", "kind": "formal", "status": "evaluated", "classification": "known_reproduced", "verdict": "Machine-checked in an axiomatised CyclicGroup structure (fields listed in formal/README.md): schnorr_correct (s = k + e\u00b7d mod n \u27f9 s\u2022G = R + e\u2022P), ecdsa_correct, ecdsa_malleable ((r,s) valid \u27f9 (r, n\u2212s) valid, modular inverse as witness). Only propext/Quot.sound used.", "evidence": ["formal/README.md", "formal/build.log", "tests/test_formal_lean.py"], "logged_utc": "2026-11-01T07:48:25+00:00"}

modified results/automated_discovery/hypothesis_summary.json +5 −5

				`@@ -8,12 +8,12 @@`
8	"methodology": 2	8	"methodology": 2
9	},	9	},
10	"by_classification": {	10	"by_classification": {
11	− "new_verified": 0,
12	− "conditional": 0,
13	"unresolved": 0,	11	"unresolved": 0,
14	− "empirical_observation": 3,	12	+ "pending": 0,
15	− "known_reproduced": 13,	13	+ "conditional": 0,
		14	+ "empirical_observation": 6,
16	"rejected": 3,	15	"rejected": 3,
17	− "pending": 6	16	+ "new_verified": 0,
		17	+ "known_reproduced": 16
18	}	18	}
19	}	19	}
	\ No newline at end of file

added results/reduced_round_sha256/collision_sat.json +10639 −0

Large diff (10,640 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-10_seed-1_solver-cadical.json +41 −0

Large diff (42 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-10_seed-1_solver-kissat.json +41 −0

Large diff (42 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-10_seed-2_solver-cadical.json +41 −0

Large diff (42 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-10_seed-2_solver-kissat.json +41 −0

Large diff (42 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-12_seed-1_solver-cadical.json +40 −0

Large diff (41 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-12_seed-1_solver-kissat.json +40 −0

Large diff (41 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-12_seed-2_solver-cadical.json +40 −0

Large diff (41 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-12_seed-2_solver-kissat.json +40 −0

Large diff (41 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-14_seed-1_solver-cadical.json +39 −0

Large diff (40 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-14_seed-1_solver-kissat.json +39 −0

Large diff (40 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-14_seed-2_solver-cadical.json +39 −0

Large diff (40 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-14_seed-2_solver-kissat.json +39 −0

Large diff (40 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-16_seed-1_solver-cadical.json +40 −0

Large diff (41 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-16_seed-1_solver-kissat.json +40 −0

Large diff (41 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-16_seed-2_solver-cadical.json +40 −0

Large diff (41 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-16_seed-2_solver-kissat.json +40 −0

Large diff (41 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-18_seed-1_solver-cadical.json +48 −0

Large diff (49 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-18_seed-1_solver-kissat.json +48 −0

Large diff (49 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-18_seed-2_solver-cadical.json +48 −0

Large diff (49 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-18_seed-2_solver-kissat.json +48 −0

Large diff (49 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-20_seed-0_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-20_seed-1_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-20_seed-1_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-20_seed-2_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-20_seed-2_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-22_seed-0_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-22_seed-1_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-22_seed-1_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-22_seed-2_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-22_seed-2_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-24_seed-0_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-24_seed-0_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-24_seed-1_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-24_seed-1_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-24_seed-2_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-24_seed-2_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-4_seed-1_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-4_seed-1_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-4_seed-2_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-4_seed-2_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-6_seed-1_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-6_seed-1_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-6_seed-2_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-6_seed-2_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-8_seed-1_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-8_seed-1_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-8_seed-2_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-fixed_r-8_seed-2_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-10_seed-1_solver-cadical.json +42 −0

Large diff (43 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-10_seed-1_solver-kissat.json +42 −0

Large diff (43 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-10_seed-2_solver-cadical.json +42 −0

Large diff (43 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-10_seed-2_solver-kissat.json +42 −0

Large diff (43 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-12_seed-1_solver-cadical.json +44 −0

Large diff (45 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-12_seed-1_solver-kissat.json +40 −0

Large diff (41 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-12_seed-2_solver-cadical.json +44 −0

Large diff (45 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-12_seed-2_solver-kissat.json +44 −0

Large diff (45 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-14_seed-1_solver-cadical.json +46 −0

Large diff (47 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-14_seed-1_solver-kissat.json +46 −0

Large diff (47 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-14_seed-2_solver-cadical.json +46 −0

Large diff (47 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-14_seed-2_solver-kissat.json +46 −0

Large diff (47 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-16_seed-1_solver-cadical.json +48 −0

Large diff (49 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-16_seed-1_solver-kissat.json +48 −0

Large diff (49 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-16_seed-2_solver-cadical.json +48 −0

Large diff (49 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-16_seed-2_solver-kissat.json +48 −0

Large diff (49 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-18_seed-1_solver-cadical.json +48 −0

Large diff (49 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-18_seed-1_solver-kissat.json +48 −0

Large diff (49 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-18_seed-2_solver-cadical.json +48 −0

Large diff (49 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-18_seed-2_solver-kissat.json +48 −0

Large diff (49 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-20_seed-0_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-20_seed-1_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-20_seed-1_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-20_seed-2_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-20_seed-2_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-22_seed-0_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-22_seed-0_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-22_seed-1_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-22_seed-1_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-22_seed-2_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-22_seed-2_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-24_seed-0_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-24_seed-0_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-24_seed-1_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-24_seed-1_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-24_seed-2_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-24_seed-2_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-4_seed-1_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-4_seed-1_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-4_seed-2_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-4_seed-2_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-6_seed-1_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-6_seed-1_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-6_seed-2_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-6_seed-2_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-8_seed-1_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-8_seed-1_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-8_seed-2_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-False_iv-free_r-8_seed-2_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-10_seed-1_solver-cadical.json +41 −0

Large diff (42 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-10_seed-1_solver-kissat.json +41 −0

Large diff (42 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-10_seed-2_solver-cadical.json +41 −0

Large diff (42 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-10_seed-2_solver-kissat.json +41 −0

Large diff (42 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-12_seed-1_solver-cadical.json +40 −0

Large diff (41 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-12_seed-1_solver-kissat.json +40 −0

Large diff (41 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-12_seed-2_solver-cadical.json +40 −0

Large diff (41 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-12_seed-2_solver-kissat.json +40 −0

Large diff (41 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-14_seed-1_solver-cadical.json +39 −0

Large diff (40 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-14_seed-1_solver-kissat.json +39 −0

Large diff (40 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-14_seed-2_solver-cadical.json +39 −0

Large diff (40 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-14_seed-2_solver-kissat.json +39 −0

Large diff (40 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-16_seed-1_solver-cadical.json +40 −0

Large diff (41 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-16_seed-1_solver-kissat.json +40 −0

Large diff (41 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-16_seed-2_solver-cadical.json +40 −0

Large diff (41 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-16_seed-2_solver-kissat.json +40 −0

Large diff (41 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-18_seed-1_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-18_seed-1_solver-kissat.json +48 −0

Large diff (49 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-18_seed-2_solver-cadical.json +48 −0

Large diff (49 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-18_seed-2_solver-kissat.json +48 −0

Large diff (49 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-20_seed-0_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-20_seed-1_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-20_seed-1_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-20_seed-2_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-20_seed-2_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-22_seed-0_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-22_seed-0_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-22_seed-1_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-22_seed-1_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-22_seed-2_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-22_seed-2_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-24_seed-0_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-24_seed-0_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-24_seed-1_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-24_seed-1_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-24_seed-2_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-24_seed-2_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-4_seed-1_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-4_seed-1_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-4_seed-2_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-4_seed-2_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-6_seed-1_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-6_seed-1_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-6_seed-2_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-6_seed-2_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-8_seed-1_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-8_seed-1_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-8_seed-2_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-fixed_r-8_seed-2_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-10_seed-1_solver-cadical.json +42 −0

Large diff (43 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-10_seed-1_solver-kissat.json +42 −0

Large diff (43 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-10_seed-2_solver-cadical.json +40 −0

Large diff (41 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-10_seed-2_solver-kissat.json +42 −0

Large diff (43 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-12_seed-1_solver-cadical.json +44 −0

Large diff (45 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-12_seed-1_solver-kissat.json +43 −0

Large diff (44 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-12_seed-2_solver-cadical.json +44 −0

Large diff (45 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-12_seed-2_solver-kissat.json +44 −0

Large diff (45 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-14_seed-1_solver-cadical.json +46 −0

Large diff (47 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-14_seed-1_solver-kissat.json +46 −0

Large diff (47 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-14_seed-2_solver-cadical.json +46 −0

Large diff (47 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-14_seed-2_solver-kissat.json +46 −0

Large diff (47 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-16_seed-1_solver-cadical.json +48 −0

Large diff (49 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-16_seed-1_solver-kissat.json +48 −0

Large diff (49 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-16_seed-2_solver-cadical.json +48 −0

Large diff (49 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-16_seed-2_solver-kissat.json +47 −0

Large diff (48 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-18_seed-1_solver-cadical.json +48 −0

Large diff (49 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-18_seed-1_solver-kissat.json +48 −0

Large diff (49 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-18_seed-2_solver-cadical.json +48 −0

Large diff (49 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-18_seed-2_solver-kissat.json +48 −0

Large diff (49 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-20_seed-0_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-20_seed-1_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-20_seed-1_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-20_seed-2_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-20_seed-2_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-22_seed-0_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-22_seed-0_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-22_seed-1_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-22_seed-1_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-22_seed-2_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-22_seed-2_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-24_seed-0_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-24_seed-0_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-24_seed-1_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-24_seed-1_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-24_seed-2_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-24_seed-2_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-4_seed-1_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-4_seed-1_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-4_seed-2_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-4_seed-2_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-6_seed-1_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-6_seed-1_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-6_seed-2_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-6_seed-2_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-8_seed-1_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-8_seed-1_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-8_seed-2_solver-cadical.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_collision/feedforward-True_iv-free_r-8_seed-2_solver-kissat.json +24 −0

Large diff (25 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-12_seed-1_solver-cadical.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-12_seed-1_solver-kissat.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-12_seed-1_solver-z3.json +56 −0

Large diff (57 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-12_seed-2_solver-cadical.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-12_seed-2_solver-kissat.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-12_seed-2_solver-z3.json +58 −0

Large diff (59 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-16_seed-1_solver-cadical.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-16_seed-1_solver-kissat.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-16_seed-1_solver-z3.json +56 −0

Large diff (57 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-16_seed-2_solver-cadical.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-16_seed-2_solver-kissat.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-16_seed-2_solver-z3.json +54 −0

Large diff (55 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-20_seed-1_solver-cadical.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-20_seed-1_solver-kissat.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-20_seed-2_solver-cadical.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-20_seed-2_solver-kissat.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-24_seed-1_solver-cadical.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-24_seed-1_solver-kissat.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-24_seed-2_solver-cadical.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-24_seed-2_solver-kissat.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-28_seed-0_solver-cadical.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-28_seed-0_solver-kissat.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-28_seed-1_solver-cadical.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-28_seed-1_solver-kissat.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-28_seed-2_solver-cadical.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-28_seed-2_solver-kissat.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-32_seed-0_solver-cadical.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-32_seed-0_solver-kissat.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-32_seed-1_solver-cadical.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-32_seed-1_solver-kissat.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-32_seed-2_solver-cadical.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-32_seed-2_solver-kissat.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-40_seed-0_solver-cadical.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-40_seed-0_solver-kissat.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-40_seed-1_solver-cadical.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-40_seed-1_solver-kissat.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-40_seed-2_solver-cadical.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-40_seed-2_solver-kissat.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-48_seed-0_solver-cadical.json +27 −0

Large diff (28 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-48_seed-0_solver-kissat.json +27 −0

Large diff (28 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-48_seed-1_solver-cadical.json +27 −0

Large diff (28 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-48_seed-1_solver-kissat.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-48_seed-2_solver-cadical.json +27 −0

Large diff (28 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-48_seed-2_solver-kissat.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-4_seed-1_solver-cadical.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-4_seed-1_solver-kissat.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-4_seed-1_solver-z3.json +39 −0

Large diff (40 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-4_seed-2_solver-cadical.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-4_seed-2_solver-kissat.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-4_seed-2_solver-z3.json +39 −0

Large diff (40 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-64_seed-0_solver-cadical.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-64_seed-0_solver-kissat.json +27 −0

Large diff (28 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-64_seed-1_solver-cadical.json +27 −0

Large diff (28 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-64_seed-1_solver-kissat.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-64_seed-2_solver-cadical.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-64_seed-2_solver-kissat.json +27 −0

Large diff (28 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-8_seed-1_solver-cadical.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-8_seed-1_solver-kissat.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-8_seed-1_solver-z3.json +57 −0

Large diff (58 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-8_seed-2_solver-cadical.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-8_seed-2_solver-kissat.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-first_r-8_seed-2_solver-z3.json +56 −0

Large diff (57 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-spread_r-12_seed-0_solver-cadical.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-spread_r-12_seed-1_solver-cadical.json +29 −0

Large diff (30 lines) is not loaded by default to keep the page fast.Load diff

added results/reduced_round_sha256/m3u96b/cells_preimage/k-16_placement-spread_r-12_seed-2_solver-cadical.json +2 −0

Large diff (2 lines) is not loaded by default to keep the page fast.Load diff

Diff truncated — file too large.

spb/wp34_uqo

Theme