Hi, I'm working on a project that reads an assembler file and converts that to sage to help verify that the math the assembler is doing is correct. It's to verify cryptographic implementations. Sage is only part of the verification, other properties are checked using SMT.
What I did so far translate an assembler file like this: movabs $0x7fffffffffffffe0,%rax xor %edx,%edx movabs $0x7fffffffffffffc0,%rcx sub (%rsi),%rcx add %rcx,(%rdi) mov %rax,%rcx adc %rdx,0x8(%rdi) [...] And turn that into: R.<out_0, out_1, out_2, out_3, out_4, out_5, out_6, out_7, out_8, out_9, out_10, out_11, out_12, out_13, out_14, out_15, out_16, out_17, in_0, in_1, in_2, in_3, in_4, in_5, in_6, in_7, in_8> = PolynomialRing(ZZ, 27) v2 = 9223372036854775776 v3 = 0 v4 = 9223372036854775744 v5 = v4 - in_0 v6 = (v5 + out_0) % 2^64 out_0_out = v6 v7 = (v5 + out_0) // 2^64 v8 = (v3 + out_1 + v7) % 2^64 out_1_out = v8 v9 = (v3 + out_1 + v7) // 2^64 [...] v2 and v4 are the first 2 movabs, v3 is the xor. v5 is the sub, which SMT will check doesn't underflow v6 and v7 are the first add. In the processor all integers are 64 bit, so v5 and out_0 can be up to 64 bit. v6 then contains the lower 64 bit, and v7 contains the carry. The adc is than an add with carry, so the v7 is used to calculate v8 and v9. At the end I have this: in_ = in_0 + in_1 * 2^58 + in_2 * 2^116 + in_3 * 2^174 + in_4 * 2^232 + in_5 * 2^290 + in_6 * 2^348 + in_7 * 2^406 + in_8 * 2^464 out = out_0 + out_1 * 2^64 + (out_2 + out_3 * 2^64) * 2^58 + (out_4 + out_5 * 2^64) * 2^116 + (out_6 + out_7 * 2^64) * 2^174 + (out_8 + out_9 * 2^64) * 2^232 + (out_10 + out_11 * 2^64) * 2^290 + (out_12 + out_13 * 2^64) * 2^348 + (out_14 + out_15 * 2^64) * 2^406 + (out_16 + out_17 * 2^64) * 2^464 out_out = out_0_out + out_1_out * 2^64 + (out_2_out + out_3_out * 2^64) * 2^58 + (out_4_out + out_5_out * 2^64) * 2^116 + (out_6_out + out_7_out * 2^64) * 2^174 + (out_8_out + out_9_out * 2^64) * 2^232 + (out_10_out + out_11_out * 2^64) * 2^290 + (out_12_out + out_13_out * 2^64) * 2^348 + (out_14_out + out_15_out * 2^64) * 2^406 + (out_16_out + out_17_out * 2^64) * 2^464 assert out_out % (2^521-1) == (out - in_) % (2^521-1) The function works in mod 2^251-1, and calculates out=out - in. in and out are the variables as they're passed in, out_out the out variable at the function exit. out_out is supposed to be what the assembler generated. And I want to verify that that out_out really contains out-in mod 2^251-1. If you want to know more details about this function, it's this C function: https://github.com/openssl/openssl/blob/0577959ceab4ca2a72a662ed12067da83cdbb3c7/crypto/ec/ecp_nistp521.c#L340-L369 But there are various problems with this. If you put that into sage you get: sage: v4 9223372036854775744 sage: v5 -in_0 + 9223372036854775744 sage: v6 out_0 + 18446744073709551615*in_0 + 9223372036854775744 sage: v7 -in_0 sage: v8 out_1 + 18446744073709551615*in_0 sage: v9 -in_0 So sage turns -in_0 into (2^64-1)*in_0, which is not what I want. The result % 2^64 is correct, but sage seems to have lost the knowledge that it's % 2^64. To avoid that, a "negone" variable was added, "- in0" was replaced by "+ negone * in_0", and the assert turned negone into -1, which makes sage say everything is ok. But if you do that, sage says v7, which is the carry, is 0. I don't understand why sage makes v7 -in_0 in the original case or 0 with the negone. Does someone have a suggestion on how I can do this instead? -- You received this message because you are subscribed to the Google Groups "sage-support" group. To unsubscribe from this group and stop receiving emails from it, send an email to sage-support+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/sage-support/d881ecdc-4c3f-4d85-8bba-0ae46be13551o%40googlegroups.com.
