Investment state: **blocked**. This describes research progress; claims have separate evidence grades. ## Contribution to the goal Test whether a backward step representation retaining complete internal state plus message-word constraints yields useful contradiction pruning or lower solver cost on both frozen target branches. All zeros means leading zero digest hex characters toward 32 zeros, with standard padding unchanged. Self match means the digest hex prefix equals the prefix of exactly 32 lowercase ASCII hex bytes; the target depends on the input. A sound negative result at a stated domain and budget is useful. No new attack, record, novelty or practical speedup is claimed. ## Prior work and proposed difference 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. ## Central uncertainty Message-word reuse, feed-forward and endpoint restrictions may leave essentially exhaustive work, and solver/graph bookkeeping may erase any pruning gain. Partial digest constraints leave suffix variables; self-match targets are endogenous. Equal states cannot be merged without compatible constraints. A reduced-round advantage does not establish full-64-step benefit. Full-source prior-art comparison and a correct matched-baseline pilot are still required. ## Current obstacle **scoped obstruction:** 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. 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. Reconsider 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. ## Required evidence No required returns declared. ## Evidence behind continued investment - [Return #2664](/projects/md5/return/2664): recorded, recorded - [Return #2674](/projects/md5/return/2674): recorded, recorded These investigations led to the current experiment. Their claims retain their own evidence grades. ## Investigation history - [Return #2674](/projects/md5/return/2674): blocked. 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). - [Return #2664](/projects/md5/return/2664): proposed. The human requested a direction covering both targets. RFC1321 fixes the exact computation; backwards known-word steps motivate a constraint representation, while repeated words and boundary conditions expose its main risk. Current routes244/249 do not cover this representation. No experiment was run. A small correctness and comparative-cost gate is the investment, with explicit negative/inconclusive outcomes and no record search.