{"id":3755,"job_id":7595,"problem_id":6,"lane_id":null,"type":"explore","user_id":90,"model":"claude-sonnet-5-5","provider":"anthropic","report_md":"# Smallest full collision, S2 stage B: sparse windows exist on the 109 B template as far as the first read of the length word (job 7595, explore)\n\n**Caveats first.** Measured, window level only. A window is steps 9..T of the single compression call. A sat witness is a message pair whose per-step XOR weights of Q_t xor Q'_t stay within the weights of Stevens' own published pair plus a slack for t = 9..T, with the differences at t = 9..14 fixed to his. It is not a differential path to step 64, not a near-collision and not a collision: after step T the two states diverge. The length-word difference dm14 = +8 is read at steps 14, 25, 35 and 50 (word schedule); every window here ends at T <= 22, so only the first read (step 14) is covered and the reads at 25, 35 and 50 are untested. `unknown` and `no answer` are not unsat: no run in this return proved anything unsatisfiable. The plan I pre-registered in #3712 was changed in places (section 2). Rung: measured. About 9.19 CPU-hours over 49 solver cells, single-threaded each.\n\n## 1. What is already known\n#3710 (plan, stage 0) and #3712 (stage A: without a fixed prefix the template looked harder than the control at T = 15). #3559: for unequal lengths La < Lb <= 55 the differences are forced to dm14 = 8(Lb - La) plus one word bit; the nearest template to Stevens' path is La = 54, 109 B. The smallest-collision state document (version 12, current through #3608, rechecked during this job) says that absorbing dm14 \"m14 read at steps 14/25/35/50\" is untested; it does not mention any window-level evidence on the template. The licence caveat on stage 1 of #3710 (no modified copies of Stevens' sources without the author's consent) is unchanged and is the person's decision, so nothing here uses or modifies his sources; only his two published example files are read, for the weights and the fixed differences.\n\n## 2. What was run\n**Model** (as in #3712, `s2_model_b_public.py`): both messages, the MD5 step function for steps 0..T, per-step caps = weights of Stevens' pair at t = 9..22 (2, 1, 1, 2, 2, 4, 6, 6, 8, 20, 17, 5, 5, 8) plus slack s, and the XOR differences at t = 9..14 fixed to his (he shares the differential to step 14 with the template). Control: his differences (dm8 = +2^25, dm13 = +2^31), no padding. Template: 54-byte M and 55-byte M'; m13 = `0x0080xxxx` / +2^31, m14 = 432 / 440 (dm14 = +8), m15 = 0.\n**Solvers.** z3 5.1.0 (the declared tool) solved the bit-vector model directly in 37 cells. Kissat 4.0.4 (MIT; built unmodified from the upstream release tarball with gcc and make; **not among the tools declared for this job**, added during the session with the person's approval) solved the same model as CNF in 12 cells; z3 only bit-blasts to CNF (`s2_cnf_run_public.py`). Every sat witness was replayed with an independent pure-Python trace (validated against `hashlib` on 200 of 200 padded messages) and again with the uploaded `replay_stage_b.py`: 35 of 35 pass.\n**Changes against the pre-registered plan (#3712 section 4).** Fixed prefix and control gate: as planned. Seeds: 1 to 3 per cell (planned 4). Slack: 0 and 4 only (planned 0, 2, 4, 8). Caps: 600 to 2400 s (planned 30 min), longer where a cell was the frontier. Windows: T = 14..22 (planned 15..18). Solver: Kissat added mid-run when z3 showed heavy tails. Not finished or not run, and not counted as results: z3 template T = 21 slack 4 seeds 2 and 3 were stopped by the supervisor at its 2520 s wall limit (z3's own 2400 s limit did not return in time): no answer; the z3 control at T = 22 slack 4 was stopped by hand after about 10 minutes and its template twin never started, to give the processor to Kissat; one queued Kissat cell (template T = 17 slack 0 seed 1) was dropped unstarted so its slot went to the slack-0 pairs at T = 18..21.\n\n## 3. Results (49 cells; per-cell records, witnesses and caps in the uploaded summary)\n\n| T | slack | control, z3 | template, z3 | control, Kissat | template, Kissat |\n|---|---|---|---|---|---|\n| 14 | 0 | sat 1 s (seed 1) | sat 4 s (seed 1) | - | - |\n| 15 | 0 | sat 15 s (seed 1); sat 14 s (seed 2) | sat 25 s (seed 1); sat 9 s (seed 2) | - | - |\n| 15 | 4 | - | sat 10 s (seed 1); sat 9 s (seed 2) | - | - |\n| 16 | 0 | sat 238 s (seed 1); sat 295 s (seed 2) | sat 370 s (seed 1); sat 810 s (seed 2) | - | - |\n| 16 | 4 | sat 18 s (seed 1) | sat 23 s (seed 1); sat 20 s (seed 2) | - | - |\n| 17 | 0 | sat 391 s (seed 1); unknown at 600 s cap (seed 2) | unknown at 2000 s cap (seed 1); unknown at 2000 s cap (seed 2) | - | sat 278 s (seed 2) |\n| 17 | 4 | sat 80 s (seed 1) | sat 144 s (seed 1); sat 125 s (seed 2) | - | - |\n| 18 | 0 | unknown at 600 s cap (seed 1); unknown at 600 s cap (seed 2) | - | sat 319 s (seed 1) | sat 530 s (seed 1) |\n| 18 | 4 | sat 28 s (seed 1) | sat 161 s (seed 1) | - | - |\n| 19 | 0 | - | - | sat 316 s (seed 1) | sat 464 s (seed 1) |\n| 19 | 4 | sat 145 s (seed 1) | sat 228 s (seed 1) | - | - |\n| 20 | 0 | - | - | sat 436 s (seed 1) | unknown at 1800 s cap (seed 1) |\n| 20 | 4 | sat 597 s (seed 1) | unknown at 900 s cap (seed 1); sat 329 s (seed 2); sat 652 s (seed 3) | - | - |\n| 21 | 0 | - | - | unknown at 1537 s cap (seed 1) | unknown at 1524 s cap (seed 1) |\n| 21 | 4 | unknown at 900 s cap (seed 1); sat 960 s (seed 2) | unknown at 900 s cap (seed 1); no answer, killed at 2520 s (seed 2); no answer, killed at 2520 s (seed 3) | - | sat 903 s (seed 1) |\n| 22 | 4 | - | - | unknown at 2400 s cap (seed 1) | sat 2006 s (seed 1) |\n\nAll times are single-process wall seconds of the solver on a shared machine with other solver cells running; hardware is withheld at the person's request, so times compare only within this table. The seed is shown per entry; `unknown` is a solver time limit.\n\n**Readings.**\n1. **Pre-registered falsifier (#3712 section 4): met.** Template pairs are sat at T >= 17 within the caps plus 4: T = 17..20 with z3, T = 21 and 22 with Kissat, and with zero slack (exactly Stevens' weights at every step of the window) at T = 17, 18 and 19 with Kissat. So \"the 109 B template is not worth a path search\" is falsified at window level. The opposite evidence (unsat for the template at T >= 16 while the control is sat) was not seen: there is no unsat anywhere.\n2. **The stage A gap was search difficulty, not the padding.** With the first six differences fixed, template and control solve in similar times where both solved: template over control (seed-matched) 0.6 to 2.8 at T = 15 and 16 (slack 0), 1.1 to 1.8 at T = 16 and 17 (slack 4), 1.6 at T = 19 (slack 4), 0.55 to 1.1 at T = 20 (slack 4), 1.7 at T = 18 and 1.5 at T = 19 (Kissat, slack 0); the outlier is 5.7 at T = 18 (slack 4, one seed each). The seed-to-seed spread of one cell is as large: template T = 20 slack 4 took 329 s and 652 s on two seeds and had no answer at 900 s on a third.\n3. **Where the template had no answer and the control solved in the same engine** (the only evidence of a real slowdown): Kissat T = 20 slack 0 (control 436 s; template none at 1800 s; one seed each) and z3 T = 21 slack 4 (control 960 s on seed 2; template none on three seeds at 900 to 2520 s, which Kissat then solved in 903 s). With one to three seeds I cannot separate heavy tails from a slowdown of a few times; I make no claim either way.\n4. **Gate.** Control sat at every slack-4 window run (T = 16..21, z3) and at every slack-0 window run (T = 14..17 with z3, T = 18..20 with Kissat). The Kissat control at T = 22 slack 4 had no answer at 2400 s, so the template's sat at T = 22 (2006 s) has no gate: it counts as a replayed witness, not as a comparison. At T = 21 slack 0 both cells had no answer at about 1530 s: that is the frontier.\n5. **Solvers.** Kissat solved cells z3 left open (template T = 17 slack 0 in 278 s after z3's 2 x 2000 s; template T = 21 slack 4 in 903 s after z3's three seeds), and was 3 to 5 times faster in two smoke tests (control T = 16 slack 4: 6 s against 18 s; T = 17: 17 s against 80 s). The Kissat cells are single seeds, so this is not a like-for-like benchmark.\n6. **Cost per step.** Control solve times grow about 1.6 to 5 times per added step beyond T = 18 for z3 (28, 145, 597, 960 s at T = 18..21, slack 4) and by 1.4 times from T = 19 to 20 for Kissat at slack 0, then no answer at T = 21 in 1530 s. A window that includes the second read of m14 (step 25) is therefore several times beyond what one session of this machine reaches by brute force; extending the window is not the way to decide it.\n\n\n## 4. Next step (pre-registered)\n**Stage C (proposed): does the template survive the second read of m14, at step 25?** Incremental extension instead of a bigger brute-force window.\n1. Take the template witnesses found here (T = 19 slack 0, T = 21 and 22 slack 4, and the others in the summary), fix the XOR differences at t = 9..T0 to each witness's values, and ask Kissat for the remaining steps up to T = 25 under the caps plus slack (Stevens' weights at t = 23..25 are 6, 3 and 5). Each such problem is much smaller than a window from scratch. Controls: the same procedure on the control witnesses (and note that Stevens' own pair is trivially sat at T = 25, so it is no control).\n2. Outcomes, pre-registered: sat is replayed with the independent trace and recorded; unsat only counts as evidence for the fixed prefix it was run on (Kissat gives no checked proof, so confirm with a proof-producing solver or a second engine before relying on it); unknown is reported as unknown.\n3. Falsifier of \"the template survives the read at step 25\": unsat at T = 25, slack <= 4, for at least four prefixes taken from distinct witnesses while the same procedure on controls is sat. Evidence for continuing: any sat at T = 25 with a verified replay.\n4. Budget: about one CPU-hour with Kissat, one to three seeds per prefix, cap 20 min per cell; stop when the controls fail the gate at every T >= 24.\n5. Not assumed: stage 1 of #3710 (patched md5sbc), which still needs the author's consent, and a step-conditions path model, which is the real next level of rigour after this popcount filter.\n\n\n## 5. Blockers\nStage 1 of #3710 (patched md5sbc) still needs the author's consent or a clean-room build (the person's decision). The popcount-window model is a necessary-condition filter with no step conditions; heavy-tailed solver times make single-seed cells weak; Kissat unsat answers carry no checked proof (none occurred).\n\n## 6. Recipe and files\nFiles (immutable, `{server origin}/files/<sha256>?raw=1`): `s2_model_b_public.py` `32dc9e2de90db9962c939516a53e37da1603738dd33cd52ec510dec095eedea9`; `s2_cnf_run_public.py` `0c7246161fa6e10a4e1c45a45bb91242d48e16d31e48d0a6ae38967657d09af0`; `replay_stage_b.py` `e13bccfcf4590194d1f7cbfe91f238a77c3555f354b9665c87d00faed1ebfc85`; `s2_stage_b_summary.json` `e46fd02e2bd89ebffbadb6e848dcc49c8603b391083a5f414691c98234930758`. Stage A script from #3712: `2f87fca06125f1f664583ff4e54e5db1d752aee347bf07f419d4931d3ad123d9`. Stevens' pair: marc-stevens.nl/research/md5-1block-collision/ (message1.bin SHA-256 `54bcb9a4fda31e4f254303e3959acd5e420ad18a80949d56a3000c3716fbd1a0`, message2.bin `90774a6455a2bdb7d106e533923ecbefe81392ca55bed0ce81cfab2c1a7f0afe`). Kissat: `https://github.com/arminbiere/kissat/archive/refs/tags/rel-4.0.4.tar.gz`, SHA-256 `bfe93eaa6323b48011e4b1fcf74b3f2e20f9de544767e728009e5b2018296193` (the hash is what I measured on download; the project publishes none), `./configure && make`, binary at `build/kissat`; MIT, not redistributed here.\nCheck the evidence without any solver: `python3 replay_stage_b.py s2_stage_b_summary.json` prints `trace matches hashlib on 200 of 200 padded single-block messages` and `35 of 35 sat witnesses pass the window replay`. Re-run a cell (directory holding both pair files, z3 5.1.0 importable or `Z3_SITE` set, `KISSAT` pointing at the binary): `python3 s2_cnf_run_public.py run control 18 0 1200 out.json 1 1` (control, T = 18, slack 0, cap 1200 s, seed 1, fixed prefix); z3 only: `python3 s2_model_b_public.py run template 17 4 900 out.json 1 1`. Times vary by machine and seed.\n\n## 7. Access gaps and sources\nNo CUDA or other hardware rates; one machine; one to three seeds per cell; no second independent SAT solver beyond Kissat for any cell. Sources: #3710, #3712, #3559, #3617, #3640, #3704, #3708, the smallest-collision state document v12, Stevens' pair and ePrint 2012/040.\n","patch":null,"cpu_hours":9.19,"hashes":{"replay_stage_b.py":"e13bccfcf4590194d1f7cbfe91f238a77c3555f354b9665c87d00faed1ebfc85","s2_cnf_run_public.py":"0c7246161fa6e10a4e1c45a45bb91242d48e16d31e48d0a6ae38967657d09af0","s2_model_b_public.py":"32dc9e2de90db9962c939516a53e37da1603738dd33cd52ec510dec095eedea9","s2_stage_b_summary.json":"e46fd02e2bd89ebffbadb6e848dcc49c8603b391083a5f414691c98234930758"},"author_rung":"measured","status":"recorded","final_rung":"recorded","created_at":"2026-10-14T17:54:03.669Z","repo_url":null,"commit":null,"cites":{"files":["32dc9e2de90db9962c939516a53e37da1603738dd33cd52ec510dec095eedea9","0c7246161fa6e10a4e1c45a45bb91242d48e16d31e48d0a6ae38967657d09af0","e13bccfcf4590194d1f7cbfe91f238a77c3555f354b9665c87d00faed1ebfc85","e46fd02e2bd89ebffbadb6e848dcc49c8603b391083a5f414691c98234930758"],"handles":[],"returns":[3710,3712,3559,3617,3640,3704,3708],"messages":[]},"tokens":{"log":"summary","input":450,"models":{"claude-sonnet-5-5":178131},"output":178131,"source":"reported","entries":0,"cache_read":33363704,"cache_write":346098,"observed_models":[]},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":null,"verification":null,"target":null,"finding":null,"human_md":null,"provisional":false,"effects_applied_at":null,"effort":"xhigh","also_fix":null,"transcript_omitted":{"share":0,"omitted":0,"outputs":0},"patch_hash":null,"superseded_by":null,"duplicate_of":null,"transcript_resubmitted_at":null,"file_notes":null,"research":null,"research_route_id":null,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":null,"department_id":"dept_00746b34d3822a538a56ec93","run_id":"run_8cd41cfbe5e548ca5688a716","triage_lead":null,"revision_base_sha":null,"integration":null,"resolves":null,"paper_exposition":null,"research_evidence":null,"transcript_mode":"summary","known_work":null,"work_disposition":null,"applicability_assessment":null,"negative_result":null,"first_indexed_at":null,"index_held_at":null,"index_ok":null,"index_reason":null,"handle":"sundayweaver","job_brief":"With the XOR differences at t = 9..14 fixed to Stevens' pair, for windows T in 15..18 and slack in 0, 2, 4, 8: is the template (m13 = 0x0080xxxx, m14 = 432 and 440, m15 = 0, dm8 = +2^25, dm13 = +2^31) sat, unsat or unknown for per-step XOR weights within Stevens' weights plus slack, given a control that is sat at the same T?\n\nWhy this step: Stage A (#3712) solved the control to T = 15, but the template was unknown at T = 15 for slack 0, 2 and 8 within 240 s. Fixing the shared prefix and running four seeds with 30 min caps tests whether that is search hardness or structure; each template cell counts only when its control is sat. Needs no third-party code beyond z3.\n\nStop when: Every cell reported as sat (replayed with the independent trace), unsat or unknown with its control; or no control is sat at any T >= 16; or the session budget is spent, with the cells reached reported.","review_deferred":false,"in_triage":false,"triage":[],"lean_statement_binding":null,"lean_execution_binding":null,"lean_scientific_identity":null,"lean_execution_identity":null,"verification_runs":[],"verification_state":null,"verification_summary":null,"canonical_return":null,"review_history":[],"dependencies":[],"cited_by":[],"route_dependents":[],"research_url":null,"transcript_url":"/projects/md5/return/3755/transcript","files":[{"sha256":"32dc9e2de90db9962c939516a53e37da1603738dd33cd52ec510dec095eedea9","name":"s2_model_b_public.py","bytes":7930},{"sha256":"0c7246161fa6e10a4e1c45a45bb91242d48e16d31e48d0a6ae38967657d09af0","name":"s2_cnf_run_public.py","bytes":5958},{"sha256":"e13bccfcf4590194d1f7cbfe91f238a77c3555f354b9665c87d00faed1ebfc85","name":"replay_stage_b.py","bytes":4296},{"sha256":"e46fd02e2bd89ebffbadb6e848dcc49c8603b391083a5f414691c98234930758","name":"s2_stage_b_summary.json","bytes":39370}],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"report_sha256":"2bf895b352c6b2eca86d55f17b558690c99eb3b1e4c38b6ab58aebc363e8fa52","next_step_sha256":null,"research_authority":{"witness_status":null,"research_status":"recorded","scopes":[]},"research_links":[],"duplicates":[],"cited_messages":[]}