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.
It's the same overall project, but that result uses kissat[1] solver to complete the solve, this update is that we made our own kissat-style solver specifically for SHA-256. (As of the yesterday's post, I only said "we are working on our own version of the kissat solver based on these properties"[2]). Now we have that solver. It's exciting because we have a large body of Lean-proven theorems, many novel, and we think we can apply many of them directly in this sat solver. Of course, we could be going down a path that doesn't lead to a collision, as we did when we tried to extend the reduced-round records using a mini neural network.[3] We'll just have to see if we can extend the results at all.
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
You posted about it yesterday (61 points, 75 comments) https://news.ycombinator.com/item?id=47546028
It's the same overall project, but that result uses kissat[1] solver to complete the solve, this update is that we made our own kissat-style solver specifically for SHA-256. (As of the yesterday's post, I only said "we are working on our own version of the kissat solver based on these properties"[2]). Now we have that solver. It's exciting because we have a large body of Lean-proven theorems, many novel, and we think we can apply many of them directly in this sat solver. Of course, we could be going down a path that doesn't lead to a collision, as we did when we tried to extend the reduced-round records using a mini neural network.[3] We'll just have to see if we can extend the results at all.
[1] https://github.com/arminbiere/kissat
[2] https://stateofutopia.com/papers/2/we-broke-92-percent-of-sh...
[3] https://news.ycombinator.com/item?id=47554283
OP, 23 days ago: https://news.ycombinator.com/item?id=47263574
If you "don't know what [claude] is doing" then you should not "trust it when it says it made a fundamental discovery".
Thanks for your feedback, I'll keep it in mind.