{"id":2674,"job_id":5554,"problem_id":6,"lane_id":null,"type":"explore","user_id":1,"model":"claude-opus-5-5","provider":"anthropic","report_md":"# Job 5554: route 252 first look. Backward-labelled Z3 encoding vs plain encoding vs random search (all-zeros and ASCII self-match prefixes)\n\n**Outcome: blocked (a scoped negative measurement).** The route's own gate was run: Z3 through its Python bindings, a correctness gate, then a predeclared equal-cap paired pilot. Keeping the full state plus message-word labels (the backward-labelled encoding B) gave no benefit over the plain encoding P at any prefix length tested. Every Z3 encoding costs 10^7 to 10^8 hash equivalents even at k=1, where random search needs 16 hashes. At k=4, all three encodings together solved 1 of 18 runs within 90 s, while random search solved 6 of 6.\n\n## Setup (frozen before the pilot; `plan.json`)\n- One-block MD5 with a 32-byte message. Standard padding (m8=0x80, m14=256), IV and feed-forward are all kept, and the digest suffix is unconstrained. Bytes 0..15 are free and bytes 16..31 are fixed by the seed. **zeros**: free bytes take any value and the first k digest hex chars must be 0. **self**: all 32 bytes are lowercase ASCII hex, and digest hex char c must equal message char c for c<k. The target is tied to the input variables.\n- **P**: the 64 steps as a forward term DAG over the message variables. **B**: state words Q1..Q64 are variables, each step is written in inverse form `m[g(i)] == rotr(Q[i+1]-Q[i], s_i) - Q[i-3] - f_i - K_i`, and each word carries 4 labels. **F** (control): the same state variables as B with forward step equalities. **R**: random search over the same free domain (Python hashlib).\n- Solver: Z3 5.1.0.0 (pip wheel z3-solver 5.1.0.0, installed into a scratch venv for this job), Python 3.14.6, the same pipeline `Then(bit-blast, sat)` for P, F and B. Z3 `memory_max_size` was 1500 MB and the cap was 90 s per solve. Every run executed under an enforced wall and CPU limit with process-group cleanup. Seeds 1-3 were held out; seed 0 was used only for calibration. hashlib rate: 2.46e6 MD5/s on 32-byte messages, one core.\n\n## Claims\n**C1 (verified, exhaustive on the stated domains). The encodings are exact.**\n- RFC 1321 vectors pass.\n- On 4 fixed-message fixtures, the P/F/B digests equal hashlib.\n- Blocking-clause enumeration ends in UNSAT and returns exactly the brute-force solution set for P, F and B on 3 domains: zeros k=3 with bytes 0 and 30 free (2^16 inputs, 17 solutions); self k=2 with chars 0-2 free (16^3 inputs, 19 solutions); self k=1 with chars 0 and 20 free (16^2 inputs, 16 solutions). No feasible input was pruned.\n- Incompatible equal states: B is UNSAT for the full Q path of message A with one byte changed (positions 0, 13, 31), and SAT with the true byte. Fixing Q57..Q60 of A and changing a byte of m4 is UNSAT for that instance.\n- All 76 pilot witnesses re-hash correctly with hashlib.\n\n**C2 (measured). B gives no benefit, and every Z3 encoding loses to random search.** Medians over seeds 1-3, wall seconds; a timeout counts at the 90 s cap:\n\n| branch,k | R hashes | P s | F s | B s | B/P |\n|---|---|---|---|---|---|\n| zeros,1 | 30 | 50.3 | 25.1 | 40.2 | 0.80 |\n| zeros,2 | 267 | 20.3 | 24.8 | 55.5 (1 TO) | 2.73 |\n| zeros,3 | 1760 | 43.0 (1 TO) | 41.4 (1 TO) | 52.2 | 1.21 |\n| zeros,4 | 22295 | TO 3/3 | TO 3/3 | 90.2 (1/3 sat) | ~1 |\n| self,1 | 13 | 55.1 | 35.3 | 37.7 | 0.69 |\n| self,2 | 289 | 2.3 | 14.9 | 33.3 | 14.2 |\n| self,3 | 3962 | 57.7 | 35.6 | 58.6 | 1.02 |\n| self,4 | 31821 | TO 3/3 | TO 3/3 | TO 3/3 | ~1 |\n\n- The predeclared benefit rule was B median < 0.5 x P median at every k. It fails on both branches.\n- The Z3 medians are 0.6e7 to 1.4e8 hash equivalents at k<=3. At k=4 the cap alone is 2.2e8, against 16^4 = 65536 expected for random search.\n- Z3 max memory was at most 320 MB, and B used about 1.3-3x the memory of P.\n- In the enumeration gate B was also slower than P: 1120 vs 599 s, 112 vs 43 s, and 18 vs 10 s.\n- Side observation (seed 0, calibration only, not part of the held-out data): under Z3's default QF_BV pipeline, or with the word-level `simplify` tactic, P hit the 1500 MB cap in 9.2 s, while B stayed within 250 MB but timed out at k=1. With the identical bit-blast pipeline that gap disappears.\n\n**C3 (proven, elementary). Why no backward pruning is available for k<=8.**\n- The first 8 hex chars come from digest word h0 = IV0 + Q61 only.\n- Q61 is set at step 60, which uses m4: Q61 = Q60 + rotl(Q57 + I(Q60,Q59,Q58) + K60 + m4, 6). For any Q57..Q60 and any target there is exactly one label value of m4. Q62..Q64 are unconstrained.\n- So the target fixes no state bit before step 60 (consistent with #2641). The whole condition is consistency of that label with m4's other uses at steps 4, 23 and 37, which is exactly the forward computation that P already encodes.\n- B therefore differs from P only by auxiliary variables, which the bit-blaster creates for P anyway, and by adders written as subtraction.\n- For self-match the prefix chars sit in m0 and m1. m0's last use is step 48, and m1's is step 55. A target that depends on the input adds no earlier constraint.\n\n## Prior art and how it maps\n- Legendre, Dequen and Krajecki (SECRYPT 2012): CDCL inversion of 28-step MD5.\n- Zaikin (arXiv 2212.02405, JAIR 2024): cube-and-conquer, 28-step MD5. Zaikin (CP 2024): 29-step MD5. These are full 128-bit targets on step-reduced MD5; they do not test partial prefixes at 64 steps.\n- mmmaly/md5-sat README: 64-step CNF with CaDiCaL. Partial-output setup B is feasible at small k, times out from 20 bits, and brute force wins. Its code and timings are unverified, but it agrees with our cliff at k=4 (16 bits).\n- Heusser's satcoin (2013): SAT nonce search for leading zeros (SHA-256). It is a claim, not a benchmark.\n- Sasaki-Aoki 2009: access was resolved by #2660 (archived full text). It is a generic-cost MITM preimage on full MD5, and its final-block length family is infeasible for messages of 1024 bytes or less (#2660).\n- Not covered by this work: other solvers (CaDiCaL, Kissat), cube-and-conquer, Dobbertin-style extra constraints, and multi-block messages.\n\n## Limits\n- One machine (macOS arm64). Three held-out seeds per cell. Z3 only.\n- 32-byte messages with 16 free bytes. k<=4 with a 90 s cap.\n- RAM is unenforced by the OS, so the cap is Z3's internal limit only.\n- Compute exceeded the route's 0.2 CPU-h estimate: the exhaustive gate needs UNSAT proofs, and a first gate run hit its 2400 s limit and was split per case.\n- The wall times include process start-up.\n\n## Sources\n- RFC 1321: https://www.rfc-editor.org/rfc/rfc1321.html#section-3\n- Legendre, Dequen, Krajecki 2012: https://www.scitepress.org/Papers/2012/40776/\n- Zaikin: https://arxiv.org/abs/2212.02405v3\n- Zaikin CP 2024: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.31\n- mmmaly/md5-sat: https://github.com/mmmaly/md5-sat\n- Heusser satcoin: https://github.com/jheusser/satcoin\n- Returns #2664, #2641, #2660\n\n## Entry for research/OUTCOMES.md\nRoute 252 (job 5554): blocked. Z3 bit-blast encodings of 64-step one-block MD5, plain vs backward-labelled, are exact (exhaustive tiny-domain gate) but cost ~1e8 hash equivalents for 1-3 hex-char prefixes and mostly time out at 4 chars, on both all-zeros and self-match. Backward labelling gives no benefit, and for k<=8 the target pins only the step-60 label of m4.\n\n17 returns wait for a verdict.\n\nTranscript scrub: the exporter (sah transcript, extra list of local run labels and session/agent ids) replaced about 1077 private values (attempt, run, session and agent ids) with <redacted>. An independent check found no token, account, device or attempt values, no emails and no home paths.\n","patch":null,"cpu_hours":2.56,"hashes":{"selftest_out.json":"8d88bd32af973e4609c2b50ec985be96978f03dfe247c4095b91fb3279793456"},"author_rung":"measured","status":"recorded","final_rung":"recorded","created_at":"2026-10-10T02:39:37.943Z","repo_url":null,"commit":null,"cites":{"files":[],"handles":[],"returns":[2664,2641,2660],"messages":[]},"tokens":{"log":"claude-code","input":156,"models":{"claude-opus-5-5":3271},"output":3271,"source":"claude-jsonl","entries":78,"cache_read":6770282,"cache_write":843647,"observed_models":["claude-opus-5-5"]},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":"Fetch each file with <server origin>/files/<sha256>?raw=1 (Accept: text/plain). Store them in one directory with the job5554_ prefix removed. Python 3.14 with `pip install z3-solver==5.1.0.0`.\n1. `python -I selftest.py --skip-enum` takes about 4 s and must print selftest_out.json byte for byte (sha256 8d88bd32af973e4609c2b50ec985be96978f03dfe247c4095b91fb3279793456; no timings in it).\n2. `python -I enum_one.py <case 0|1|2> <P|F|B>`: each prints pass=true, with z3_count equal to brute_count (17, 19, 16). It takes 10-1120 s. Timings vary, so these outputs are not hashed.\n3. Pilot, run from a directory laid out as research/artifacts/job5554 and calling sah.py exec (or adapt `drive.py` to call pilot.py directly): `python3 drive.py <venv python>` for k=1..3, then `python3 drive.py <venv python> 4`. Each line is `pilot.py <branch> <enc> <k> <seed> 90 bb0`. Expect the Z3 encodings to need tens of seconds at k<=3 and mostly time out at k=4, and random search to finish in under 5 s. Witnesses are re-hashed by `summarize.py calib_out.json pilot_results_k123.jsonl pilot_results_k4.jsonl`.\nTotal CPU used here: about 2.56 h of single-thread wall time (exec-reported), most of it in the exhaustive gate and timeouts.","verification":null,"target":null,"finding":null,"human_md":null,"provisional":false,"effects_applied_at":null,"effort":"high","also_fix":null,"transcript_omitted":{"share":0,"omitted":0,"outputs":80},"patch_hash":null,"superseded_by":null,"duplicate_of":null,"transcript_resubmitted_at":null,"file_notes":[{"sha":"0030a549c498a0b4dc21c5d0a749c0f7404b423e20593d95ba23740fce3b714f","name":"job5554_enum_one.py","notes":["prints what looks like progress or timing to stdout on line 38 (\"'sets_equal': sols == brute, 'pass': ok, 'sec': round(time.time() - t, 2)}), flu\"), inside the statement that starts on line 37: stdout is the artifact and must reproduce byte for byte elsewhere; send progress, timing and rates to stderr. This one is a guess from the text, not a measurement: if the output is already identical from run to run, say so in your return and leave the file alone."]}],"research":{"outcome":"blocked","obstacle":{"kind":"scoped_obstruction","evidence":"Job 5554 files pilot_results_k123.jsonl, pilot_results_k4.jsonl, enum_results.jsonl, selftest_out.json; the step-60 derivation in the report.","statement":"On full 64-step one-block MD5, Z3 bit-blast/CDCL encodings (plain, forward-named, backward-labelled) cost ~1e7-1e8 hash equivalents at 1-3 hex-char prefixes and mostly exceed 2.2e8 at 4, while random search needs 16^k; backward labelling gives no measured or structural pruning for k<=8.","assumptions":"Z3 5.1.0.0, Then(bit-blast, sat); 32-byte messages with 16 free bytes; held-out seeds 1-3; 90 s cap; one macOS arm64 core; all-zeros and lowercase-ASCII-hex self-match targets with standard padding.","revisit_when":"A measured SAT/SMT method (any solver, encoding or extra constraints) solves 64-step one-block MD5 prefix instances for k>=5 hex chars in either branch at fewer than 16^k hash equivalents, or a constraint is found that propagates digest-prefix bits into state words before step 60."},"route_id":252,"depends_on":[],"evidence_md":"First-look gate run as specified (Z3 5.1.0.0 via Python, identical bit-blast pipeline). Correctness: RFC vectors, fixtures, exhaustive enumeration on three tiny domains (2^16, 16^3, 16^2) equals brute force for plain P, forward-named F and backward-labelled B; incompatible equal-state merges are UNSAT. Paired pilot (32-byte one-block message, 16 free bytes, held-out seeds 1-3, 90 s cap): at k=1..3 hex chars all Z3 encodings need 2-59 s median (0.6e7-1.4e8 hashlib-hash equivalents) vs random search 13-3962 hashes; at k=4 1/18 Z3 runs solved, random search 6/6 (<=31821 hashes). B/P median ratio 0.69-14.2, never meeting the predeclared <0.5 rule; B also slower in enumeration (1120 vs 599 s). Derivation: for k<=8 the target only constrains h0=IV0+Q61, and step 60 is a bijection in m4 for any Q57..Q60, so the target fixes no state bit before step 60 (cf. #2641); B can prune only via m4's reuse at steps 4/23/37, which P already encodes. This changes the route from proposed to blocked at Z3/one-block scope; it agrees with mmmaly/md5-sat (CaDiCaL partial output times out from 20 bits).","prior_art_md":"Searched 2026-10-10: SAT MD5 preimage step-reduced; Legendre Dequen Krajecki; Zaikin cube-and-conquer; SAT bitcoin leading zeros. Read: Legendre/Dequen/Krajecki SECRYPT 2012 abstract (28-step MD5 inversion, https://www.scitepress.org/Papers/2012/40776/); Zaikin arXiv 2212.02405v3 abstract (28-step MD5, 4 hashes, cube-and-conquer); Zaikin CP 2024 abstract (29-step MD5, https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.31); mmmaly/md5-sat README (64-step CNF, CaDiCaL; partial-output prefix feasible at small k, >=20 bits timed out, brute force wins; code and timings unverified); Heusser satcoin README (SAT nonce search for leading zeros, SHA-256, claims only). Sasaki/Aoki 2009 access gap resolved by #2660 via the archived full text (final-block length family infeasible for L<=1024). Local: #2641 (MitM closed for self-match; target fixes 0 state bits before step 60), #2618 word/step map. Remaining gap: no stronger solver (CaDiCaL/Kissat, cube-and-conquer, Dobbertin-style constraints) measured on 64-step partial-prefix instances in either branch; no evidence that any of them beats 16^k at k>=5."},"research_route_id":252,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":null,"department_id":"dept_2bfed67ebb6125ca84c61817","run_id":"run_d1501b779dabdbaafcc05df0","triage_lead":null,"revision_base_sha":null,"integration":null,"resolves":null,"paper_exposition":null,"handle":"Benjaminsen","job_brief":"Search online for existing attempts, results, tables and datasets before testing feasibility. Reuse the recorded search and inspect the closest sources and weakest assumption. Use published numbers with citations; do not reproduce them in a first look. Seek the smallest experiment on the uncovered step. Recommend promising only with specific evidence and a bounded next step; do not claim the route is proved. Map the assumptions of any borrowed method onto this problem.\n\nRead GET <project base>/research-routes/252 and return #2664. Return the ordinary report and transcript plus research: {route_id: 252, outcome: \"promising|progress|blocked|inconclusive|known|result\", evidence_md: \"what the evidence changes, <=4000 chars\", prior_art_md: \"updated online search record, sources and exact remaining gap, <=4000\", next_step: {question, method, success, failure, budget_hours} <only for continued pursuit; what to do, never when or how fast; it must not ask for what a return on this route or a linked route already did, and the route returns it builds on go in depends_on or cites.returns>, obstacle: {kind, statement, assumptions, evidence, revisit_when} <for blocked/inconclusive>, depends_on: [<return ids actually required>]}. A result with a distinct next_step requests review and continues pursuit concurrently; omit next_step when no further experiment is warranted. Use known with prior_art_md and no next_step or obstacle when cited prior work already covers the proposed contribution; it stops automatic investigation without requesting review. The evidence grade is separate. Do not close a broad route because one proof attempt failed.","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":[252],"research_url":"/projects/md5/research-routes/252","transcript_url":"/projects/md5/return/2674/transcript","files":[{"sha256":"79ccb80aa28f4592e0d297f865ddc4302f7cd41105126191a0b9181472748545","name":"job5554_md5z3.py","bytes":5924},{"sha256":"4b28a7d787df0aec3a32ed4cc74ee2f5f61de97dd4b0196918634f19e2c7d345","name":"job5554_selftest.py","bytes":5875},{"sha256":"0030a549c498a0b4dc21c5d0a749c0f7404b423e20593d95ba23740fce3b714f","name":"job5554_enum_one.py","bytes":2006},{"sha256":"fccb5f377d77819dc46326afb1cb3434e4b9e6ecb935fce0f0d8b1d40f0272a3","name":"job5554_pilot.py","bytes":2616},{"sha256":"fb7f576394f6a04d6fa385f8a2dcf463fdebb8076d5124fe50456fc3aa927684","name":"job5554_drive.py","bytes":1844},{"sha256":"7daae7b8f4d82dab90543137013bb1aff22e26a91bcf55accb791cf1bdea08b8","name":"job5554_summarize.py","bytes":1984},{"sha256":"a4ebc8765c38786d6879ceaedbb895e51b13e91977f833f7a26f605f6a3cf5d6","name":"job5554_calib.py","bytes":370},{"sha256":"39b90e76acdd6d375aac14c6105abdca07574d922c36e49536c647bf4a9d167b","name":"job5554_plan.json","bytes":1452},{"sha256":"8d88bd32af973e4609c2b50ec985be96978f03dfe247c4095b91fb3279793456","name":"job5554_selftest_out.json","bytes":619},{"sha256":"180510b291afa332acbcb00a0ffebe4a699fedad57fbc6b017d4a3268cfcf33f","name":"job5554_selftest_run1_enum_log.txt","bytes":225},{"sha256":"f6a0529d7c03793284c079ef74a4d9c735da83c983547f1b9a78b37dadbdbaaf","name":"job5554_enum_results.jsonl","bytes":1102},{"sha256":"6ded04117c46e5132a5af83a49d2c045e352974b7ab3c5218b8de6e24104271b","name":"job5554_pilot_results_k123.jsonl","bytes":34044},{"sha256":"173e3253b63325561c4877d5587cfdf4a7ed0468ffc54d6b8b387d426c709d14","name":"job5554_pilot_results_k4.jsonl","bytes":9284},{"sha256":"65bdf8c846e0f2cad94cd78465309d6dc5accbe2bbacdbcf5616ccb639a91de2","name":"job5554_pilot_summary.json","bytes":7429},{"sha256":"11968044b3ccfa5fb6130014d9506305345c2a851ee1f7ab17e2f216f81a3b4e","name":"job5554_calib_out.json","bytes":39}],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"duplicates":[],"cited_messages":[]}