Skip to content

Instantly share code, notes, and snippets.

@andres-erbsen

andres-erbsen/det32.diff Secret

Created July 31, 2023 20:16
Show Gist options
  • Save andres-erbsen/a8f6c694e80168354b19710fc811c5c4 to your computer and use it in GitHub Desktop.
Save andres-erbsen/a8f6c694e80168354b19710fc811c5c4 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
det32.diff
commit e83aa131c4e1697159745c637b64475d3a1b3fb4
Author: Andres Erbsen <andres-github@andres.systems>
Date: Mon Jul 31 20:10:58 2023 +0000
default to magnitude 8->1 in Dettman multiplication
diff --git a/fiat-c/src/secp256k1_dettman_32.c b/fiat-c/src/secp256k1_dettman_32.c
index 65560d9be..21ac5b465 100644
--- a/fiat-c/src/secp256k1_dettman_32.c
+++ b/fiat-c/src/secp256k1_dettman_32.c
@@ -31,70 +31,70 @@
* eval out1 mod 115792089237316195423570985008687907853269984665640564039457584007908834671663 = (eval arg1 * eval arg2) mod 115792089237316195423570985008687907853269984665640564039457584007908834671663
*
* Input Bounds:
- * arg1: [[0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7ffffe]]
- * arg2: [[0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7ffffe]]
+ * arg1: [[0x0 ~> 0x3ffffff0], [0x0 ~> 0x3ffffff0], [0x0 ~> 0x3ffffff0], [0x0 ~> 0x3ffffff0], [0x0 ~> 0x3ffffff0], [0x0 ~> 0x3ffffff0], [0x0 ~> 0x3ffffff0], [0x0 ~> 0x3ffffff0], [0x0 ~> 0x3ffffff0], [0x0 ~> 0x3fffff0]]
+ * arg2: [[0x0 ~> 0x3ffffff0], [0x0 ~> 0x3ffffff0], [0x0 ~> 0x3ffffff0], [0x0 ~> 0x3ffffff0], [0x0 ~> 0x3ffffff0], [0x0 ~> 0x3ffffff0], [0x0 ~> 0x3ffffff0], [0x0 ~> 0x3ffffff0], [0x0 ~> 0x3ffffff0], [0x0 ~> 0x3fffff0]]
* Output Bounds:
- * out1: [[0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x5fffff]]
+ * out1: [[0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7ffffe]]
*/
static FIAT_SECP256K1_DETTMAN_FIAT_INLINE void fiat_secp256k1_dettman_mul(uint32_t out1[10], const uint32_t arg1[10], const uint32_t arg2[10]) {
uint64_t x1;
uint32_t x2;
uint32_t x3;
uint64_t x4;
- uint32_t x5;
+ uint64_t x5;
uint32_t x6;
uint64_t x7;
uint32_t x8;
uint32_t x9;
uint64_t x10;
- uint32_t x11;
+ uint64_t x11;
uint32_t x12;
uint64_t x13;
- uint32_t x14;
+ uint64_t x14;
uint32_t x15;
uint64_t x16;
- uint32_t x17;
+ uint64_t x17;
uint32_t x18;
uint32_t x19;
uint32_t x20;
uint64_t x21;
- uint32_t x22;
+ uint64_t x22;
uint32_t x23;
uint64_t x24;
- uint32_t x25;
+ uint64_t x25;
uint32_t x26;
uint64_t x27;
- uint32_t x28;
+ uint64_t x28;
uint32_t x29;
uint64_t x30;
- uint32_t x31;
+ uint64_t x31;
uint32_t x32;
uint64_t x33;
- uint32_t x34;
+ uint64_t x34;
uint32_t x35;
uint64_t x36;
- uint32_t x37;
+ uint64_t x37;
uint32_t x38;
uint64_t x39;
- uint32_t x40;
+ uint64_t x40;
uint32_t x41;
uint64_t x42;
- uint32_t x43;
+ uint64_t x43;
uint32_t x44;
uint64_t x45;
- uint32_t x46;
+ uint64_t x46;
uint32_t x47;
uint64_t x48;
- uint32_t x49;
+ uint64_t x49;
uint32_t x50;
uint64_t x51;
- uint32_t x52;
+ uint64_t x52;
uint32_t x53;
uint64_t x54;
uint32_t x55;
uint32_t x56;
uint64_t x57;
- uint32_t x58;
+ uint64_t x58;
uint32_t x59;
uint64_t x60;
uint32_t x61;
@@ -107,60 +107,60 @@ static FIAT_SECP256K1_DETTMAN_FIAT_INLINE void fiat_secp256k1_dettman_mul(uint32
x2 = (uint32_t)(x1 >> 26);
x3 = (uint32_t)(x1 & UINT32_C(0x3ffffff));
x4 = ((((uint64_t)(arg1[0]) * (arg2[7])) + (((uint64_t)(arg1[1]) * (arg2[6])) + (((uint64_t)(arg1[2]) * (arg2[5])) + (((uint64_t)(arg1[3]) * (arg2[4])) + (((uint64_t)(arg1[4]) * (arg2[3])) + (((uint64_t)(arg1[5]) * (arg2[2])) + (((uint64_t)(arg1[6]) * (arg2[1])) + ((uint64_t)(arg1[7]) * (arg2[0]))))))))) + ((uint64_t)x3 * UINT16_C(0x3d10)));
- x5 = (uint32_t)(x4 >> 26);
+ x5 = (x4 >> 26);
x6 = (uint32_t)(x4 & UINT32_C(0x3ffffff));
x7 = (x2 + ((uint64_t)(arg1[9]) * (arg2[9])));
x8 = (uint32_t)(x7 >> 32);
x9 = (uint32_t)(x7 & UINT32_C(0xffffffff));
x10 = ((x5 + ((((uint64_t)(arg1[0]) * (arg2[8])) + (((uint64_t)(arg1[1]) * (arg2[7])) + (((uint64_t)(arg1[2]) * (arg2[6])) + (((uint64_t)(arg1[3]) * (arg2[5])) + (((uint64_t)(arg1[4]) * (arg2[4])) + (((uint64_t)(arg1[5]) * (arg2[3])) + (((uint64_t)(arg1[6]) * (arg2[2])) + (((uint64_t)(arg1[7]) * (arg2[1])) + ((uint64_t)(arg1[8]) * (arg2[0])))))))))) + ((uint64_t)x3 << 10))) + ((uint64_t)x9 * UINT16_C(0x3d10)));
- x11 = (uint32_t)(x10 >> 26);
+ x11 = (x10 >> 26);
x12 = (uint32_t)(x10 & UINT32_C(0x3ffffff));
x13 = ((x11 + ((((uint64_t)(arg1[0]) * (arg2[9])) + (((uint64_t)(arg1[1]) * (arg2[8])) + (((uint64_t)(arg1[2]) * (arg2[7])) + (((uint64_t)(arg1[3]) * (arg2[6])) + (((uint64_t)(arg1[4]) * (arg2[5])) + (((uint64_t)(arg1[5]) * (arg2[4])) + (((uint64_t)(arg1[6]) * (arg2[3])) + (((uint64_t)(arg1[7]) * (arg2[2])) + (((uint64_t)(arg1[8]) * (arg2[1])) + ((uint64_t)(arg1[9]) * (arg2[0]))))))))))) + ((uint64_t)x9 << 10))) + ((uint64_t)x8 * UINT32_C(0xf4400)));
- x14 = (uint32_t)(x13 >> 26);
+ x14 = (x13 >> 26);
x15 = (uint32_t)(x13 & UINT32_C(0x3ffffff));
- x16 = (x14 + ((((uint64_t)(arg1[1]) * (arg2[9])) + (((uint64_t)(arg1[2]) * (arg2[8])) + (((uint64_t)(arg1[3]) * (arg2[7])) + (((uint64_t)(arg1[4]) * (arg2[6])) + (((uint64_t)(arg1[5]) * (arg2[5])) + (((uint64_t)(arg1[6]) * (arg2[4])) + (((uint64_t)(arg1[7]) * (arg2[3])) + (((uint64_t)(arg1[8]) * (arg2[2])) + ((uint64_t)(arg1[9]) * (arg2[1])))))))))) + (x8 << 16)));
- x17 = (uint32_t)(x16 >> 26);
+ x16 = (x14 + ((((uint64_t)(arg1[1]) * (arg2[9])) + (((uint64_t)(arg1[2]) * (arg2[8])) + (((uint64_t)(arg1[3]) * (arg2[7])) + (((uint64_t)(arg1[4]) * (arg2[6])) + (((uint64_t)(arg1[5]) * (arg2[5])) + (((uint64_t)(arg1[6]) * (arg2[4])) + (((uint64_t)(arg1[7]) * (arg2[3])) + (((uint64_t)(arg1[8]) * (arg2[2])) + ((uint64_t)(arg1[9]) * (arg2[1])))))))))) + ((uint64_t)x8 << 16)));
+ x17 = (x16 >> 26);
x18 = (uint32_t)(x16 & UINT32_C(0x3ffffff));
x19 = (x15 >> 22);
x20 = (x15 & UINT32_C(0x3fffff));
x21 = (((uint64_t)(arg1[0]) * (arg2[0])) + ((uint64_t)(x19 + (x18 << 4)) * UINT16_C(0x3d1)));
- x22 = (uint32_t)(x21 >> 26);
+ x22 = (x21 >> 26);
x23 = (uint32_t)(x21 & UINT32_C(0x3ffffff));
x24 = (x17 + (((uint64_t)(arg1[2]) * (arg2[9])) + (((uint64_t)(arg1[3]) * (arg2[8])) + (((uint64_t)(arg1[4]) * (arg2[7])) + (((uint64_t)(arg1[5]) * (arg2[6])) + (((uint64_t)(arg1[6]) * (arg2[5])) + (((uint64_t)(arg1[7]) * (arg2[4])) + (((uint64_t)(arg1[8]) * (arg2[3])) + ((uint64_t)(arg1[9]) * (arg2[2]))))))))));
- x25 = (uint32_t)(x24 >> 26);
+ x25 = (x24 >> 26);
x26 = (uint32_t)(x24 & UINT32_C(0x3ffffff));
x27 = ((x22 + ((((uint64_t)(arg1[0]) * (arg2[1])) + ((uint64_t)(arg1[1]) * (arg2[0]))) + ((uint64_t)(x19 + (x18 << 4)) << 6))) + ((uint64_t)x26 * UINT16_C(0x3d10)));
- x28 = (uint32_t)(x27 >> 26);
+ x28 = (x27 >> 26);
x29 = (uint32_t)(x27 & UINT32_C(0x3ffffff));
x30 = (x25 + (((uint64_t)(arg1[3]) * (arg2[9])) + (((uint64_t)(arg1[4]) * (arg2[8])) + (((uint64_t)(arg1[5]) * (arg2[7])) + (((uint64_t)(arg1[6]) * (arg2[6])) + (((uint64_t)(arg1[7]) * (arg2[5])) + (((uint64_t)(arg1[8]) * (arg2[4])) + ((uint64_t)(arg1[9]) * (arg2[3])))))))));
- x31 = (uint32_t)(x30 >> 26);
+ x31 = (x30 >> 26);
x32 = (uint32_t)(x30 & UINT32_C(0x3ffffff));
x33 = ((x28 + ((((uint64_t)(arg1[0]) * (arg2[2])) + (((uint64_t)(arg1[1]) * (arg2[1])) + ((uint64_t)(arg1[2]) * (arg2[0])))) + ((uint64_t)x26 << 10))) + ((uint64_t)x32 * UINT16_C(0x3d10)));
- x34 = (uint32_t)(x33 >> 26);
+ x34 = (x33 >> 26);
x35 = (uint32_t)(x33 & UINT32_C(0x3ffffff));
x36 = (x31 + (((uint64_t)(arg1[4]) * (arg2[9])) + (((uint64_t)(arg1[5]) * (arg2[8])) + (((uint64_t)(arg1[6]) * (arg2[7])) + (((uint64_t)(arg1[7]) * (arg2[6])) + (((uint64_t)(arg1[8]) * (arg2[5])) + ((uint64_t)(arg1[9]) * (arg2[4]))))))));
- x37 = (uint32_t)(x36 >> 26);
+ x37 = (x36 >> 26);
x38 = (uint32_t)(x36 & UINT32_C(0x3ffffff));
x39 = ((x34 + ((((uint64_t)(arg1[0]) * (arg2[3])) + (((uint64_t)(arg1[1]) * (arg2[2])) + (((uint64_t)(arg1[2]) * (arg2[1])) + ((uint64_t)(arg1[3]) * (arg2[0]))))) + ((uint64_t)x32 << 10))) + ((uint64_t)x38 * UINT16_C(0x3d10)));
- x40 = (uint32_t)(x39 >> 26);
+ x40 = (x39 >> 26);
x41 = (uint32_t)(x39 & UINT32_C(0x3ffffff));
x42 = (x37 + (((uint64_t)(arg1[5]) * (arg2[9])) + (((uint64_t)(arg1[6]) * (arg2[8])) + (((uint64_t)(arg1[7]) * (arg2[7])) + (((uint64_t)(arg1[8]) * (arg2[6])) + ((uint64_t)(arg1[9]) * (arg2[5])))))));
- x43 = (uint32_t)(x42 >> 26);
+ x43 = (x42 >> 26);
x44 = (uint32_t)(x42 & UINT32_C(0x3ffffff));
x45 = ((x40 + ((((uint64_t)(arg1[0]) * (arg2[4])) + (((uint64_t)(arg1[1]) * (arg2[3])) + (((uint64_t)(arg1[2]) * (arg2[2])) + (((uint64_t)(arg1[3]) * (arg2[1])) + ((uint64_t)(arg1[4]) * (arg2[0])))))) + ((uint64_t)x38 << 10))) + ((uint64_t)x44 * UINT16_C(0x3d10)));
- x46 = (uint32_t)(x45 >> 26);
+ x46 = (x45 >> 26);
x47 = (uint32_t)(x45 & UINT32_C(0x3ffffff));
x48 = (x43 + (((uint64_t)(arg1[6]) * (arg2[9])) + (((uint64_t)(arg1[7]) * (arg2[8])) + (((uint64_t)(arg1[8]) * (arg2[7])) + ((uint64_t)(arg1[9]) * (arg2[6]))))));
- x49 = (uint32_t)(x48 >> 26);
+ x49 = (x48 >> 26);
x50 = (uint32_t)(x48 & UINT32_C(0x3ffffff));
x51 = ((x46 + ((((uint64_t)(arg1[0]) * (arg2[5])) + (((uint64_t)(arg1[1]) * (arg2[4])) + (((uint64_t)(arg1[2]) * (arg2[3])) + (((uint64_t)(arg1[3]) * (arg2[2])) + (((uint64_t)(arg1[4]) * (arg2[1])) + ((uint64_t)(arg1[5]) * (arg2[0]))))))) + ((uint64_t)x44 << 10))) + ((uint64_t)x50 * UINT16_C(0x3d10)));
- x52 = (uint32_t)(x51 >> 26);
+ x52 = (x51 >> 26);
x53 = (uint32_t)(x51 & UINT32_C(0x3ffffff));
x54 = (x49 + (((uint64_t)(arg1[7]) * (arg2[9])) + (((uint64_t)(arg1[8]) * (arg2[8])) + ((uint64_t)(arg1[9]) * (arg2[7])))));
x55 = (uint32_t)(x54 >> 32);
x56 = (uint32_t)(x54 & UINT32_C(0xffffffff));
x57 = ((x52 + ((((uint64_t)(arg1[0]) * (arg2[6])) + (((uint64_t)(arg1[1]) * (arg2[5])) + (((uint64_t)(arg1[2]) * (arg2[4])) + (((uint64_t)(arg1[3]) * (arg2[3])) + (((uint64_t)(arg1[4]) * (arg2[2])) + (((uint64_t)(arg1[5]) * (arg2[1])) + ((uint64_t)(arg1[6]) * (arg2[0])))))))) + ((uint64_t)x50 << 10))) + ((uint64_t)x56 * UINT16_C(0x3d10)));
- x58 = (uint32_t)(x57 >> 26);
+ x58 = (x57 >> 26);
x59 = (uint32_t)(x57 & UINT32_C(0x3ffffff));
x60 = ((x58 + (x6 + ((uint64_t)x56 << 10))) + ((uint64_t)x55 * UINT32_C(0xf4400)));
x61 = (uint32_t)(x60 >> 26);
@@ -188,9 +188,9 @@ static FIAT_SECP256K1_DETTMAN_FIAT_INLINE void fiat_secp256k1_dettman_mul(uint32
* eval out1 mod 115792089237316195423570985008687907853269984665640564039457584007908834671663 = (eval arg1 * eval arg1) mod 115792089237316195423570985008687907853269984665640564039457584007908834671663
*
* Input Bounds:
- * arg1: [[0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7ffffe]]
+ * arg1: [[0x0 ~> 0x3ffffff0], [0x0 ~> 0x3ffffff0], [0x0 ~> 0x3ffffff0], [0x0 ~> 0x3ffffff0], [0x0 ~> 0x3ffffff0], [0x0 ~> 0x3ffffff0], [0x0 ~> 0x3ffffff0], [0x0 ~> 0x3ffffff0], [0x0 ~> 0x3ffffff0], [0x0 ~> 0x3fffff0]]
* Output Bounds:
- * out1: [[0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x5fffff]]
+ * out1: [[0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7ffffe]]
*/
static FIAT_SECP256K1_DETTMAN_FIAT_INLINE void fiat_secp256k1_dettman_square(uint32_t out1[10], const uint32_t arg1[10]) {
uint32_t x1;
@@ -206,60 +206,60 @@ static FIAT_SECP256K1_DETTMAN_FIAT_INLINE void fiat_secp256k1_dettman_square(uin
uint32_t x11;
uint32_t x12;
uint64_t x13;
- uint32_t x14;
+ uint64_t x14;
uint32_t x15;
uint64_t x16;
uint32_t x17;
uint32_t x18;
uint64_t x19;
- uint32_t x20;
+ uint64_t x20;
uint32_t x21;
uint64_t x22;
- uint32_t x23;
+ uint64_t x23;
uint32_t x24;
uint64_t x25;
- uint32_t x26;
+ uint64_t x26;
uint32_t x27;
uint32_t x28;
uint32_t x29;
uint64_t x30;
- uint32_t x31;
+ uint64_t x31;
uint32_t x32;
uint64_t x33;
- uint32_t x34;
+ uint64_t x34;
uint32_t x35;
uint64_t x36;
- uint32_t x37;
+ uint64_t x37;
uint32_t x38;
uint64_t x39;
- uint32_t x40;
+ uint64_t x40;
uint32_t x41;
uint64_t x42;
- uint32_t x43;
+ uint64_t x43;
uint32_t x44;
uint64_t x45;
- uint32_t x46;
+ uint64_t x46;
uint32_t x47;
uint64_t x48;
- uint32_t x49;
+ uint64_t x49;
uint32_t x50;
uint64_t x51;
- uint32_t x52;
+ uint64_t x52;
uint32_t x53;
uint64_t x54;
- uint32_t x55;
+ uint64_t x55;
uint32_t x56;
uint64_t x57;
- uint32_t x58;
+ uint64_t x58;
uint32_t x59;
uint64_t x60;
- uint32_t x61;
+ uint64_t x61;
uint32_t x62;
uint64_t x63;
uint32_t x64;
uint32_t x65;
uint64_t x66;
- uint32_t x67;
+ uint64_t x67;
uint32_t x68;
uint64_t x69;
uint32_t x70;
@@ -281,60 +281,60 @@ static FIAT_SECP256K1_DETTMAN_FIAT_INLINE void fiat_secp256k1_dettman_square(uin
x11 = (uint32_t)(x10 >> 26);
x12 = (uint32_t)(x10 & UINT32_C(0x3ffffff));
x13 = ((((uint64_t)x9 * (arg1[7])) + (((uint64_t)x8 * (arg1[6])) + (((uint64_t)x7 * (arg1[5])) + ((uint64_t)x6 * (arg1[4]))))) + ((uint64_t)x12 * UINT16_C(0x3d10)));
- x14 = (uint32_t)(x13 >> 26);
+ x14 = (x13 >> 26);
x15 = (uint32_t)(x13 & UINT32_C(0x3ffffff));
x16 = (x11 + ((uint64_t)(arg1[9]) * (arg1[9])));
x17 = (uint32_t)(x16 >> 32);
x18 = (uint32_t)(x16 & UINT32_C(0xffffffff));
x19 = ((x14 + ((((uint64_t)x9 * (arg1[8])) + (((uint64_t)x8 * (arg1[7])) + (((uint64_t)x7 * (arg1[6])) + (((uint64_t)x6 * (arg1[5])) + ((uint64_t)(arg1[4]) * (arg1[4])))))) + ((uint64_t)x12 << 10))) + ((uint64_t)x18 * UINT16_C(0x3d10)));
- x20 = (uint32_t)(x19 >> 26);
+ x20 = (x19 >> 26);
x21 = (uint32_t)(x19 & UINT32_C(0x3ffffff));
x22 = ((x20 + ((((uint64_t)x9 * (arg1[9])) + (((uint64_t)x8 * (arg1[8])) + (((uint64_t)x7 * (arg1[7])) + (((uint64_t)x6 * (arg1[6])) + ((uint64_t)x5 * (arg1[5])))))) + ((uint64_t)x18 << 10))) + ((uint64_t)x17 * UINT32_C(0xf4400)));
- x23 = (uint32_t)(x22 >> 26);
+ x23 = (x22 >> 26);
x24 = (uint32_t)(x22 & UINT32_C(0x3ffffff));
- x25 = (x23 + ((((uint64_t)x8 * (arg1[9])) + (((uint64_t)x7 * (arg1[8])) + (((uint64_t)x6 * (arg1[7])) + (((uint64_t)x5 * (arg1[6])) + ((uint64_t)(arg1[5]) * (arg1[5])))))) + (x17 << 16)));
- x26 = (uint32_t)(x25 >> 26);
+ x25 = (x23 + ((((uint64_t)x8 * (arg1[9])) + (((uint64_t)x7 * (arg1[8])) + (((uint64_t)x6 * (arg1[7])) + (((uint64_t)x5 * (arg1[6])) + ((uint64_t)(arg1[5]) * (arg1[5])))))) + ((uint64_t)x17 << 16)));
+ x26 = (x25 >> 26);
x27 = (uint32_t)(x25 & UINT32_C(0x3ffffff));
x28 = (x24 >> 22);
x29 = (x24 & UINT32_C(0x3fffff));
x30 = (((uint64_t)(arg1[0]) * (arg1[0])) + ((uint64_t)(x28 + (x27 << 4)) * UINT16_C(0x3d1)));
- x31 = (uint32_t)(x30 >> 26);
+ x31 = (x30 >> 26);
x32 = (uint32_t)(x30 & UINT32_C(0x3ffffff));
x33 = (x26 + (((uint64_t)x7 * (arg1[9])) + (((uint64_t)x6 * (arg1[8])) + (((uint64_t)x5 * (arg1[7])) + ((uint64_t)x4 * (arg1[6]))))));
- x34 = (uint32_t)(x33 >> 26);
+ x34 = (x33 >> 26);
x35 = (uint32_t)(x33 & UINT32_C(0x3ffffff));
x36 = ((x31 + (((uint64_t)x9 * (arg1[1])) + ((uint64_t)(x28 + (x27 << 4)) << 6))) + ((uint64_t)x35 * UINT16_C(0x3d10)));
- x37 = (uint32_t)(x36 >> 26);
+ x37 = (x36 >> 26);
x38 = (uint32_t)(x36 & UINT32_C(0x3ffffff));
x39 = (x34 + (((uint64_t)x6 * (arg1[9])) + (((uint64_t)x5 * (arg1[8])) + (((uint64_t)x4 * (arg1[7])) + ((uint64_t)(arg1[6]) * (arg1[6]))))));
- x40 = (uint32_t)(x39 >> 26);
+ x40 = (x39 >> 26);
x41 = (uint32_t)(x39 & UINT32_C(0x3ffffff));
x42 = ((x37 + ((((uint64_t)x9 * (arg1[2])) + ((uint64_t)(arg1[1]) * (arg1[1]))) + ((uint64_t)x35 << 10))) + ((uint64_t)x41 * UINT16_C(0x3d10)));
- x43 = (uint32_t)(x42 >> 26);
+ x43 = (x42 >> 26);
x44 = (uint32_t)(x42 & UINT32_C(0x3ffffff));
x45 = (x40 + (((uint64_t)x5 * (arg1[9])) + (((uint64_t)x4 * (arg1[8])) + ((uint64_t)x3 * (arg1[7])))));
- x46 = (uint32_t)(x45 >> 26);
+ x46 = (x45 >> 26);
x47 = (uint32_t)(x45 & UINT32_C(0x3ffffff));
x48 = ((x43 + ((((uint64_t)x9 * (arg1[3])) + ((uint64_t)x8 * (arg1[2]))) + ((uint64_t)x41 << 10))) + ((uint64_t)x47 * UINT16_C(0x3d10)));
- x49 = (uint32_t)(x48 >> 26);
+ x49 = (x48 >> 26);
x50 = (uint32_t)(x48 & UINT32_C(0x3ffffff));
x51 = (x46 + (((uint64_t)x4 * (arg1[9])) + (((uint64_t)x3 * (arg1[8])) + ((uint64_t)(arg1[7]) * (arg1[7])))));
- x52 = (uint32_t)(x51 >> 26);
+ x52 = (x51 >> 26);
x53 = (uint32_t)(x51 & UINT32_C(0x3ffffff));
x54 = ((x49 + ((((uint64_t)x9 * (arg1[4])) + (((uint64_t)x8 * (arg1[3])) + ((uint64_t)(arg1[2]) * (arg1[2])))) + ((uint64_t)x47 << 10))) + ((uint64_t)x53 * UINT16_C(0x3d10)));
- x55 = (uint32_t)(x54 >> 26);
+ x55 = (x54 >> 26);
x56 = (uint32_t)(x54 & UINT32_C(0x3ffffff));
x57 = (x52 + (((uint64_t)x3 * (arg1[9])) + ((uint64_t)x2 * (arg1[8]))));
- x58 = (uint32_t)(x57 >> 26);
+ x58 = (x57 >> 26);
x59 = (uint32_t)(x57 & UINT32_C(0x3ffffff));
x60 = ((x55 + ((((uint64_t)x9 * (arg1[5])) + (((uint64_t)x8 * (arg1[4])) + ((uint64_t)x7 * (arg1[3])))) + ((uint64_t)x53 << 10))) + ((uint64_t)x59 * UINT16_C(0x3d10)));
- x61 = (uint32_t)(x60 >> 26);
+ x61 = (x60 >> 26);
x62 = (uint32_t)(x60 & UINT32_C(0x3ffffff));
x63 = (x58 + (((uint64_t)x2 * (arg1[9])) + ((uint64_t)(arg1[8]) * (arg1[8]))));
x64 = (uint32_t)(x63 >> 32);
x65 = (uint32_t)(x63 & UINT32_C(0xffffffff));
x66 = ((x61 + ((((uint64_t)x9 * (arg1[6])) + (((uint64_t)x8 * (arg1[5])) + (((uint64_t)x7 * (arg1[4])) + ((uint64_t)(arg1[3]) * (arg1[3]))))) + ((uint64_t)x59 << 10))) + ((uint64_t)x65 * UINT16_C(0x3d10)));
- x67 = (uint32_t)(x66 >> 26);
+ x67 = (x66 >> 26);
x68 = (uint32_t)(x66 & UINT32_C(0x3ffffff));
x69 = ((x67 + (x15 + ((uint64_t)x65 << 10))) + ((uint64_t)x64 * UINT32_C(0xf4400)));
x70 = (uint32_t)(x69 >> 26);
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment