Thanks, you're right. My "it is possible" is doing some heavy lifting there :). We've found theorems (stated in the paper) that carry through 64 rounds, so it

Thanks, you're right. My "it is possible" is doing some heavy lifting there :). We've found theorems (stated in the paper) that carry through 64 rounds, so it is possible that theorems might carry through the full 128 rounds of double-SHA256. Bitcoin's proof-of-work is indeed a "partial second preimage", and constraints a certain number of leading zeros, i.e. a certain number of set bits. It's possible (there we go again) that this could leave enough wiggle room for large algabraic solvers like kissat to satisfy a large number of clauses about them. So far nobody is doing that, and ASICs are very simplistic. However, we are not making any claims about preimage attacks in this paper!