Quote
Next, perform the double SHA256, and produce a set of equations that represents each bit in the final hash.
Wouldn't the stateful 32-bit operations (ROTR, + mod 32) radically complicate creating a reduceable linear polynomial? ROTR I can see since its just assignment in your model, but where do all the carry flags go in + mod 32?
BTW, this topic is a great match for your nickname.
