3 ms·

You posted about it yesterday (61 points, 75 comments) https://news.ycombinator.com/item?id=47546028 https://news.ycombinator.com/item?id=47546028

• logicallee 7mo ago
  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 https://github.com/arminbiere/kissat [2] https://stateofutopia.com/papers/2/we-broke-92-percent-of-sha-256.html#:~:text=are%20working%20on%20our%20own%20version%20of%20the%20kissat%20solver%20based%20on%20these%20properties. https://stateofutopia.com/papers/2/we-broke-92-percent-of-sh... [3] https://news.ycombinator.com/item?id=47554283 https://news.ycombinator.com/item?id=47554283