Tell HN: We built our own SAT solver for SHA-256

I wanted to leave this post (these couple of paragraphs) as an artifact of our process in working toward a full SHA-256 collision. After publishing our results yesterday, we continued the work we started. The next step was to go from a generic SAT engine, kissat, to one that is built just for SHA-256. This is now completed and competitive in search speed with kissat (faster for some seeds) specifically for our problem. It completes finding the solution at sr=59 at similar speeds or 20% faster, and we are now getting ready to tackle sr=64 (full schedule), 64 round collision. We have 1,950 lean-verified theorems we can augment this with, iterating on it in this space while using our sr=59 benchmark. Our approach is to iterate on it by benchmarking solving speed, and iteratively add theorems to see if it improves the solving speed, once we've improved the solving speed very substantially (orders of magnitude) we'll try the full run. We also have some exciting statistical tricks to add, such as from [1], [2], and possibly an adaptation of [3], and, because our solver is specifically for SHA-256, we can apply message modification in a vertically integrated way as part of the solve.

Overall, as mentioned, we are now close to having all the parts necessary for a full collision. If we achieve that breakthrough, we will link to this post, so people can see our progress.

[1] https://eprint.iacr.org/2011/037.pdf

[2] https://link.springer.com/article/10.1007/s00145-016-9237-5

[3] https://eprint.iacr.org/2024/255