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?
Here is what my symbolic carry bit code looks like for + (note, TUInt32 is my class which acts as an UInt32 but symbolically tracks all operations applied to it.)
public static TUInt32 operator +(TUInt32 b1, TUInt32 b2)
{
var r = new TUInt32((uint)0);
TBit carryBit = new TBit("0");
for (int i = 0; i < 32; i++)
{
var tmp = new TBit(b1._bits
, "^", b2._bits);
r._bits = new TBit(tmp, "^", carryBit);
var op1 = new TBit(b2._bits, "|", carryBit);
var op2 = new TBit(b1._bits, "&", op1);
var op3 = new TBit(b2._bits, "&", carryBit);
carryBit = new TBit(op2, "|", op3);
}
r._value = (uint)(b1._value + b2._value);
return r;
}
The equations do get quite complicated, but as I mentioned previously, you can PolynomialReduce after each step of the procedure;
For symbolic unsigned integers "a" and "b", having symbolic bits a0-a31 and b0-b31, here is the result for each bit of "c" in the operation "c = (a + b)" after PolynomialReduce:
bit0: (a0^b0)
bit1: (a1^a0&b0^b1)
bit2: (a2^a0&b0&b1^b2)
bit3: (a3^a0&b0&b1&b2^b3)
bit4: (a4^a0&b0&b1&b2&b3^b4)
bit5: (a5^a0&b0&b1&b2&b3&b4^b5)
bit6: (a6^a0&b0&b1&b2&b3&b4&b5^b6)
bit7: (a7^a0&b0&b1&b2&b3&b4&b5&b6^b7)
bit8: (a8^a0&b0&b1&b2&b3&b4&b5&b6&b7^b8)
bit9: (a9^a0&b0&b1&b2&b3&b4&b5&b6&b7&b8^b9)
bit10: (a10^b10^a0&b0&b1&b2&b3&b4&b5&b6&b7&b8&b9)
bit11: (a11^b11^a0&b0&b1&b10&b2&b3&b4&b5&b6&b7&b8&b9)
bit12: (a12^b12^a0&b0&b1&b10&b11&b2&b3&b4&b5&b6&b7&b8&b9)
bit13: (a13^b13^a0&b0&b1&b10&b11&b12&b2&b3&b4&b5&b6&b7&b8&b9)
bit14: (a14^b14^a0&b0&b1&b10&b11&b12&b13&b2&b3&b4&b5&b6&b7&b8&b9)
bit15: (a15^b15^a0&b0&b1&b10&b11&b12&b13&b14&b2&b3&b4&b5&b6&b7&b8&b9)
bit16: (a16^b16^a0&b0&b1&b10&b11&b12&b13&b14&b15&b2&b3&b4&b5&b6&b7&b8&b9)
bit17: (a17^b17^a0&b0&b1&b10&b11&b12&b13&b14&b15&b16&b2&b3&b4&b5&b6&b7&b8&b9)
bit18: (a18^b18^a0&b0&b1&b10&b11&b12&b13&b14&b15&b16&b17&b2&b3&b4&b5&b6&b7&b8&b9)
bit19: (a19^b19^a0&b0&b1&b10&b11&b12&b13&b14&b15&b16&b17&b18&b2&b3&b4&b5&b6&b7&b8&b9)
bit20: (a20^b20^a0&b0&b1&b10&b11&b12&b13&b14&b15&b16&b17&b18&b19&b2&b3&b4&b5&b6&b7&b8&b9)
bit21: (a21^b21^a0&b0&b1&b10&b11&b12&b13&b14&b15&b16&b17&b18&b19&b2&b20&b3&b4&b5&b6&b7&b8&b9)
bit22: (a22^b22^a0&b0&b1&b10&b11&b12&b13&b14&b15&b16&b17&b18&b19&b2&b20&b21&b3&b4&b5&b6&b7&b8&b9)
bit23: (a23^b23^a0&b0&b1&b10&b11&b12&b13&b14&b15&b16&b17&b18&b19&b2&b20&b21&b22&b3&b4&b5&b6&b7&b8&b9)
bit24: (a24^b24^a0&b0&b1&b10&b11&b12&b13&b14&b15&b16&b17&b18&b19&b2&b20&b21&b22&b23&b3&b4&b5&b6&b7&b8&b9)
bit25: (a25^b25^a0&b0&b1&b10&b11&b12&b13&b14&b15&b16&b17&b18&b19&b2&b20&b21&b22&b23&b24&b3&b4&b5&b6&b7&b8&b9)
bit26: (a26^b26^a0&b0&b1&b10&b11&b12&b13&b14&b15&b16&b17&b18&b19&b2&b20&b21&b22&b23&b24&b25&b3&b4&b5&b6&b7&b8&b9)
bit27: (a27^b27^a0&b0&b1&b10&b11&b12&b13&b14&b15&b16&b17&b18&b19&b2&b20&b21&b22&b23&b24&b25&b26&b3&b4&b5&b6&b7&b8&b9)
bit28: (a28^b28^a0&b0&b1&b10&b11&b12&b13&b14&b15&b16&b17&b18&b19&b2&b20&b21&b22&b23&b24&b25&b26&b27&b3&b4&b5&b6&b7&b8&b9)
bit29: (a29^b29^a0&b0&b1&b10&b11&b12&b13&b14&b15&b16&b17&b18&b19&b2&b20&b21&b22&b23&b24&b25&b26&b27&b28&b3&b4&b5&b6&b7&b8&b9)
bit30: (a30^b30^a0&b0&b1&b10&b11&b12&b13&b14&b15&b16&b17&b18&b19&b2&b20&b21&b22&b23&b24&b25&b26&b27&b28&b29&b3&b4&b5&b6&b7&b8&b9)
bit31: (a31^b31^a0&b0&b1&b10&b11&b12&b13&b14&b15&b16&b17&b18&b19&b2&b20&b21&b22&b23&b24&b25&b26&b27&b28&b29&b3&b30&b4&b5&b6&b7&b8&b9)