diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-14 15:54:15 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-14 15:54:15 -0500 |
| commit | 4d98d4bcd43c026ee7a74208dfc68e582bdfa122 (patch) | |
| tree | 405e541018308cb7c1fd8594987f20696aaad301 /src/Specific/solinas32_2e512m569_24limbs | |
| parent | c21d39f35ed774dc7f2405d79acbc21086ee2ef1 (diff) | |
Update display logs and c files
Diffstat (limited to 'src/Specific/solinas32_2e512m569_24limbs')
8 files changed, 628 insertions, 0 deletions
diff --git a/src/Specific/solinas32_2e512m569_24limbs/feadd.c b/src/Specific/solinas32_2e512m569_24limbs/feadd.c new file mode 100644 index 000000000..115132981 --- /dev/null +++ b/src/Specific/solinas32_2e512m569_24limbs/feadd.c @@ -0,0 +1,75 @@ +static void feadd(uint32_t out[24], const uint32_t in1[24], const uint32_t in2[24]) { + { const uint32_t x48 = in1[23]; + { const uint32_t x49 = in1[22]; + { const uint32_t x47 = in1[21]; + { const uint32_t x45 = in1[20]; + { const uint32_t x43 = in1[19]; + { const uint32_t x41 = in1[18]; + { const uint32_t x39 = in1[17]; + { const uint32_t x37 = in1[16]; + { const uint32_t x35 = in1[15]; + { const uint32_t x33 = in1[14]; + { const uint32_t x31 = in1[13]; + { const uint32_t x29 = in1[12]; + { const uint32_t x27 = in1[11]; + { const uint32_t x25 = in1[10]; + { const uint32_t x23 = in1[9]; + { const uint32_t x21 = in1[8]; + { const uint32_t x19 = in1[7]; + { const uint32_t x17 = in1[6]; + { const uint32_t x15 = in1[5]; + { const uint32_t x13 = in1[4]; + { const uint32_t x11 = in1[3]; + { const uint32_t x9 = in1[2]; + { const uint32_t x7 = in1[1]; + { const uint32_t x5 = in1[0]; + { const uint32_t x94 = in2[23]; + { const uint32_t x95 = in2[22]; + { const uint32_t x93 = in2[21]; + { const uint32_t x91 = in2[20]; + { const uint32_t x89 = in2[19]; + { const uint32_t x87 = in2[18]; + { const uint32_t x85 = in2[17]; + { const uint32_t x83 = in2[16]; + { const uint32_t x81 = in2[15]; + { const uint32_t x79 = in2[14]; + { const uint32_t x77 = in2[13]; + { const uint32_t x75 = in2[12]; + { const uint32_t x73 = in2[11]; + { const uint32_t x71 = in2[10]; + { const uint32_t x69 = in2[9]; + { const uint32_t x67 = in2[8]; + { const uint32_t x65 = in2[7]; + { const uint32_t x63 = in2[6]; + { const uint32_t x61 = in2[5]; + { const uint32_t x59 = in2[4]; + { const uint32_t x57 = in2[3]; + { const uint32_t x55 = in2[2]; + { const uint32_t x53 = in2[1]; + { const uint32_t x51 = in2[0]; + out[0] = (x5 + x51); + out[1] = (x7 + x53); + out[2] = (x9 + x55); + out[3] = (x11 + x57); + out[4] = (x13 + x59); + out[5] = (x15 + x61); + out[6] = (x17 + x63); + out[7] = (x19 + x65); + out[8] = (x21 + x67); + out[9] = (x23 + x69); + out[10] = (x25 + x71); + out[11] = (x27 + x73); + out[12] = (x29 + x75); + out[13] = (x31 + x77); + out[14] = (x33 + x79); + out[15] = (x35 + x81); + out[16] = (x37 + x83); + out[17] = (x39 + x85); + out[18] = (x41 + x87); + out[19] = (x43 + x89); + out[20] = (x45 + x91); + out[21] = (x47 + x93); + out[22] = (x49 + x95); + out[23] = (x48 + x94); + }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} +} diff --git a/src/Specific/solinas32_2e512m569_24limbs/feaddDisplay.log b/src/Specific/solinas32_2e512m569_24limbs/feaddDisplay.log new file mode 100644 index 000000000..8ec776f44 --- /dev/null +++ b/src/Specific/solinas32_2e512m569_24limbs/feaddDisplay.log @@ -0,0 +1,7 @@ +λ x x0 : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32, +Interp-η +(λ var : Syntax.base_type → Type, + λ '(x48, x49, x47, x45, x43, x41, x39, x37, x35, x33, x31, x29, x27, x25, x23, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x94, x95, x93, x91, x89, x87, x85, x83, x81, x79, x77, x75, x73, x71, x69, x67, x65, x63, x61, x59, x57, x55, x53, x51))%core, + ((x48 + x94), (x49 + x95), (x47 + x93), (x45 + x91), (x43 + x89), (x41 + x87), (x39 + x85), (x37 + x83), (x35 + x81), (x33 + x79), (x31 + x77), (x29 + x75), (x27 + x73), (x25 + x71), (x23 + x69), (x21 + x67), (x19 + x65), (x17 + x63), (x15 + x61), (x13 + x59), (x11 + x57), (x9 + x55), (x7 + x53), (x5 + x51))) +(x, x0)%core + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t) diff --git a/src/Specific/solinas32_2e512m569_24limbs/fesquare.c b/src/Specific/solinas32_2e512m569_24limbs/fesquare.c new file mode 100644 index 000000000..e1d0ea01d --- /dev/null +++ b/src/Specific/solinas32_2e512m569_24limbs/fesquare.c @@ -0,0 +1,152 @@ +static void fesquare(uint32_t out[24], const uint32_t in1[24]) { + { const uint32_t x45 = in1[23]; + { const uint32_t x46 = in1[22]; + { const uint32_t x44 = in1[21]; + { const uint32_t x42 = in1[20]; + { const uint32_t x40 = in1[19]; + { const uint32_t x38 = in1[18]; + { const uint32_t x36 = in1[17]; + { const uint32_t x34 = in1[16]; + { const uint32_t x32 = in1[15]; + { const uint32_t x30 = in1[14]; + { const uint32_t x28 = in1[13]; + { const uint32_t x26 = in1[12]; + { const uint32_t x24 = in1[11]; + { const uint32_t x22 = in1[10]; + { const uint32_t x20 = in1[9]; + { const uint32_t x18 = in1[8]; + { const uint32_t x16 = in1[7]; + { const uint32_t x14 = in1[6]; + { const uint32_t x12 = in1[5]; + { const uint32_t x10 = in1[4]; + { const uint32_t x8 = in1[3]; + { const uint32_t x6 = in1[2]; + { const uint32_t x4 = in1[1]; + { const uint32_t x2 = in1[0]; + { uint64_t x47 = (((uint64_t)x2 * x45) + ((0x2 * ((uint64_t)x4 * x46)) + (((uint64_t)x6 * x44) + (((uint64_t)x8 * x42) + ((0x2 * ((uint64_t)x10 * x40)) + (((uint64_t)x12 * x38) + (((uint64_t)x14 * x36) + ((0x2 * ((uint64_t)x16 * x34)) + (((uint64_t)x18 * x32) + (((uint64_t)x20 * x30) + ((0x2 * ((uint64_t)x22 * x28)) + (((uint64_t)x24 * x26) + (((uint64_t)x26 * x24) + ((0x2 * ((uint64_t)x28 * x22)) + (((uint64_t)x30 * x20) + (((uint64_t)x32 * x18) + ((0x2 * ((uint64_t)x34 * x16)) + (((uint64_t)x36 * x14) + (((uint64_t)x38 * x12) + ((0x2 * ((uint64_t)x40 * x10)) + (((uint64_t)x42 * x8) + (((uint64_t)x44 * x6) + ((0x2 * ((uint64_t)x46 * x4)) + ((uint64_t)x45 * x2)))))))))))))))))))))))); + { uint64_t x48 = ((((uint64_t)x2 * x46) + (((uint64_t)x4 * x44) + (((uint64_t)x6 * x42) + (((uint64_t)x8 * x40) + (((uint64_t)x10 * x38) + (((uint64_t)x12 * x36) + (((uint64_t)x14 * x34) + (((uint64_t)x16 * x32) + (((uint64_t)x18 * x30) + (((uint64_t)x20 * x28) + (((uint64_t)x22 * x26) + (((uint64_t)x24 * x24) + (((uint64_t)x26 * x22) + (((uint64_t)x28 * x20) + (((uint64_t)x30 * x18) + (((uint64_t)x32 * x16) + (((uint64_t)x34 * x14) + (((uint64_t)x36 * x12) + (((uint64_t)x38 * x10) + (((uint64_t)x40 * x8) + (((uint64_t)x42 * x6) + (((uint64_t)x44 * x4) + ((uint64_t)x46 * x2))))))))))))))))))))))) + (0x239 * ((uint64_t)x45 * x45))); + { uint64_t x49 = ((((uint64_t)x2 * x44) + ((0x2 * ((uint64_t)x4 * x42)) + ((0x2 * ((uint64_t)x6 * x40)) + (((uint64_t)x8 * x38) + ((0x2 * ((uint64_t)x10 * x36)) + ((0x2 * ((uint64_t)x12 * x34)) + (((uint64_t)x14 * x32) + ((0x2 * ((uint64_t)x16 * x30)) + ((0x2 * ((uint64_t)x18 * x28)) + (((uint64_t)x20 * x26) + ((0x2 * ((uint64_t)x22 * x24)) + ((0x2 * ((uint64_t)x24 * x22)) + (((uint64_t)x26 * x20) + ((0x2 * ((uint64_t)x28 * x18)) + ((0x2 * ((uint64_t)x30 * x16)) + (((uint64_t)x32 * x14) + ((0x2 * ((uint64_t)x34 * x12)) + ((0x2 * ((uint64_t)x36 * x10)) + (((uint64_t)x38 * x8) + ((0x2 * ((uint64_t)x40 * x6)) + ((0x2 * ((uint64_t)x42 * x4)) + ((uint64_t)x44 * x2)))))))))))))))))))))) + (0x239 * ((0x2 * ((uint64_t)x46 * x45)) + (0x2 * ((uint64_t)x45 * x46))))); + { uint64_t x50 = ((((uint64_t)x2 * x42) + ((0x2 * ((uint64_t)x4 * x40)) + (((uint64_t)x6 * x38) + (((uint64_t)x8 * x36) + ((0x2 * ((uint64_t)x10 * x34)) + (((uint64_t)x12 * x32) + (((uint64_t)x14 * x30) + ((0x2 * ((uint64_t)x16 * x28)) + (((uint64_t)x18 * x26) + (((uint64_t)x20 * x24) + ((0x2 * ((uint64_t)x22 * x22)) + (((uint64_t)x24 * x20) + (((uint64_t)x26 * x18) + ((0x2 * ((uint64_t)x28 * x16)) + (((uint64_t)x30 * x14) + (((uint64_t)x32 * x12) + ((0x2 * ((uint64_t)x34 * x10)) + (((uint64_t)x36 * x8) + (((uint64_t)x38 * x6) + ((0x2 * ((uint64_t)x40 * x4)) + ((uint64_t)x42 * x2))))))))))))))))))))) + (0x239 * (((uint64_t)x44 * x45) + ((0x2 * ((uint64_t)x46 * x46)) + ((uint64_t)x45 * x44))))); + { uint64_t x51 = ((((uint64_t)x2 * x40) + (((uint64_t)x4 * x38) + (((uint64_t)x6 * x36) + (((uint64_t)x8 * x34) + (((uint64_t)x10 * x32) + (((uint64_t)x12 * x30) + (((uint64_t)x14 * x28) + (((uint64_t)x16 * x26) + (((uint64_t)x18 * x24) + (((uint64_t)x20 * x22) + (((uint64_t)x22 * x20) + (((uint64_t)x24 * x18) + (((uint64_t)x26 * x16) + (((uint64_t)x28 * x14) + (((uint64_t)x30 * x12) + (((uint64_t)x32 * x10) + (((uint64_t)x34 * x8) + (((uint64_t)x36 * x6) + (((uint64_t)x38 * x4) + ((uint64_t)x40 * x2)))))))))))))))))))) + (0x239 * (((uint64_t)x42 * x45) + (((uint64_t)x44 * x46) + (((uint64_t)x46 * x44) + ((uint64_t)x45 * x42)))))); + { uint64_t x52 = ((((uint64_t)x2 * x38) + ((0x2 * ((uint64_t)x4 * x36)) + ((0x2 * ((uint64_t)x6 * x34)) + (((uint64_t)x8 * x32) + ((0x2 * ((uint64_t)x10 * x30)) + ((0x2 * ((uint64_t)x12 * x28)) + (((uint64_t)x14 * x26) + ((0x2 * ((uint64_t)x16 * x24)) + ((0x2 * ((uint64_t)x18 * x22)) + (((uint64_t)x20 * x20) + ((0x2 * ((uint64_t)x22 * x18)) + ((0x2 * ((uint64_t)x24 * x16)) + (((uint64_t)x26 * x14) + ((0x2 * ((uint64_t)x28 * x12)) + ((0x2 * ((uint64_t)x30 * x10)) + (((uint64_t)x32 * x8) + ((0x2 * ((uint64_t)x34 * x6)) + ((0x2 * ((uint64_t)x36 * x4)) + ((uint64_t)x38 * x2))))))))))))))))))) + (0x239 * ((0x2 * ((uint64_t)x40 * x45)) + ((0x2 * ((uint64_t)x42 * x46)) + (((uint64_t)x44 * x44) + ((0x2 * ((uint64_t)x46 * x42)) + (0x2 * ((uint64_t)x45 * x40)))))))); + { uint64_t x53 = ((((uint64_t)x2 * x36) + ((0x2 * ((uint64_t)x4 * x34)) + (((uint64_t)x6 * x32) + (((uint64_t)x8 * x30) + ((0x2 * ((uint64_t)x10 * x28)) + (((uint64_t)x12 * x26) + (((uint64_t)x14 * x24) + ((0x2 * ((uint64_t)x16 * x22)) + (((uint64_t)x18 * x20) + (((uint64_t)x20 * x18) + ((0x2 * ((uint64_t)x22 * x16)) + (((uint64_t)x24 * x14) + (((uint64_t)x26 * x12) + ((0x2 * ((uint64_t)x28 * x10)) + (((uint64_t)x30 * x8) + (((uint64_t)x32 * x6) + ((0x2 * ((uint64_t)x34 * x4)) + ((uint64_t)x36 * x2)))))))))))))))))) + (0x239 * (((uint64_t)x38 * x45) + ((0x2 * ((uint64_t)x40 * x46)) + (((uint64_t)x42 * x44) + (((uint64_t)x44 * x42) + ((0x2 * ((uint64_t)x46 * x40)) + ((uint64_t)x45 * x38)))))))); + { uint64_t x54 = ((((uint64_t)x2 * x34) + (((uint64_t)x4 * x32) + (((uint64_t)x6 * x30) + (((uint64_t)x8 * x28) + (((uint64_t)x10 * x26) + (((uint64_t)x12 * x24) + (((uint64_t)x14 * x22) + (((uint64_t)x16 * x20) + (((uint64_t)x18 * x18) + (((uint64_t)x20 * x16) + (((uint64_t)x22 * x14) + (((uint64_t)x24 * x12) + (((uint64_t)x26 * x10) + (((uint64_t)x28 * x8) + (((uint64_t)x30 * x6) + (((uint64_t)x32 * x4) + ((uint64_t)x34 * x2))))))))))))))))) + (0x239 * (((uint64_t)x36 * x45) + (((uint64_t)x38 * x46) + (((uint64_t)x40 * x44) + (((uint64_t)x42 * x42) + (((uint64_t)x44 * x40) + (((uint64_t)x46 * x38) + ((uint64_t)x45 * x36))))))))); + { uint64_t x55 = ((((uint64_t)x2 * x32) + ((0x2 * ((uint64_t)x4 * x30)) + ((0x2 * ((uint64_t)x6 * x28)) + (((uint64_t)x8 * x26) + ((0x2 * ((uint64_t)x10 * x24)) + ((0x2 * ((uint64_t)x12 * x22)) + (((uint64_t)x14 * x20) + ((0x2 * ((uint64_t)x16 * x18)) + ((0x2 * ((uint64_t)x18 * x16)) + (((uint64_t)x20 * x14) + ((0x2 * ((uint64_t)x22 * x12)) + ((0x2 * ((uint64_t)x24 * x10)) + (((uint64_t)x26 * x8) + ((0x2 * ((uint64_t)x28 * x6)) + ((0x2 * ((uint64_t)x30 * x4)) + ((uint64_t)x32 * x2)))))))))))))))) + (0x239 * ((0x2 * ((uint64_t)x34 * x45)) + ((0x2 * ((uint64_t)x36 * x46)) + (((uint64_t)x38 * x44) + ((0x2 * ((uint64_t)x40 * x42)) + ((0x2 * ((uint64_t)x42 * x40)) + (((uint64_t)x44 * x38) + ((0x2 * ((uint64_t)x46 * x36)) + (0x2 * ((uint64_t)x45 * x34))))))))))); + { uint64_t x56 = ((((uint64_t)x2 * x30) + ((0x2 * ((uint64_t)x4 * x28)) + (((uint64_t)x6 * x26) + (((uint64_t)x8 * x24) + ((0x2 * ((uint64_t)x10 * x22)) + (((uint64_t)x12 * x20) + (((uint64_t)x14 * x18) + ((0x2 * ((uint64_t)x16 * x16)) + (((uint64_t)x18 * x14) + (((uint64_t)x20 * x12) + ((0x2 * ((uint64_t)x22 * x10)) + (((uint64_t)x24 * x8) + (((uint64_t)x26 * x6) + ((0x2 * ((uint64_t)x28 * x4)) + ((uint64_t)x30 * x2))))))))))))))) + (0x239 * (((uint64_t)x32 * x45) + ((0x2 * ((uint64_t)x34 * x46)) + (((uint64_t)x36 * x44) + (((uint64_t)x38 * x42) + ((0x2 * ((uint64_t)x40 * x40)) + (((uint64_t)x42 * x38) + (((uint64_t)x44 * x36) + ((0x2 * ((uint64_t)x46 * x34)) + ((uint64_t)x45 * x32))))))))))); + { uint64_t x57 = ((((uint64_t)x2 * x28) + (((uint64_t)x4 * x26) + (((uint64_t)x6 * x24) + (((uint64_t)x8 * x22) + (((uint64_t)x10 * x20) + (((uint64_t)x12 * x18) + (((uint64_t)x14 * x16) + (((uint64_t)x16 * x14) + (((uint64_t)x18 * x12) + (((uint64_t)x20 * x10) + (((uint64_t)x22 * x8) + (((uint64_t)x24 * x6) + (((uint64_t)x26 * x4) + ((uint64_t)x28 * x2)))))))))))))) + (0x239 * (((uint64_t)x30 * x45) + (((uint64_t)x32 * x46) + (((uint64_t)x34 * x44) + (((uint64_t)x36 * x42) + (((uint64_t)x38 * x40) + (((uint64_t)x40 * x38) + (((uint64_t)x42 * x36) + (((uint64_t)x44 * x34) + (((uint64_t)x46 * x32) + ((uint64_t)x45 * x30)))))))))))); + { uint64_t x58 = ((((uint64_t)x2 * x26) + ((0x2 * ((uint64_t)x4 * x24)) + ((0x2 * ((uint64_t)x6 * x22)) + (((uint64_t)x8 * x20) + ((0x2 * ((uint64_t)x10 * x18)) + ((0x2 * ((uint64_t)x12 * x16)) + (((uint64_t)x14 * x14) + ((0x2 * ((uint64_t)x16 * x12)) + ((0x2 * ((uint64_t)x18 * x10)) + (((uint64_t)x20 * x8) + ((0x2 * ((uint64_t)x22 * x6)) + ((0x2 * ((uint64_t)x24 * x4)) + ((uint64_t)x26 * x2))))))))))))) + (0x239 * ((0x2 * ((uint64_t)x28 * x45)) + ((0x2 * ((uint64_t)x30 * x46)) + (((uint64_t)x32 * x44) + ((0x2 * ((uint64_t)x34 * x42)) + ((0x2 * ((uint64_t)x36 * x40)) + (((uint64_t)x38 * x38) + ((0x2 * ((uint64_t)x40 * x36)) + ((0x2 * ((uint64_t)x42 * x34)) + (((uint64_t)x44 * x32) + ((0x2 * ((uint64_t)x46 * x30)) + (0x2 * ((uint64_t)x45 * x28)))))))))))))); + { uint64_t x59 = ((((uint64_t)x2 * x24) + ((0x2 * ((uint64_t)x4 * x22)) + (((uint64_t)x6 * x20) + (((uint64_t)x8 * x18) + ((0x2 * ((uint64_t)x10 * x16)) + (((uint64_t)x12 * x14) + (((uint64_t)x14 * x12) + ((0x2 * ((uint64_t)x16 * x10)) + (((uint64_t)x18 * x8) + (((uint64_t)x20 * x6) + ((0x2 * ((uint64_t)x22 * x4)) + ((uint64_t)x24 * x2)))))))))))) + (0x239 * (((uint64_t)x26 * x45) + ((0x2 * ((uint64_t)x28 * x46)) + (((uint64_t)x30 * x44) + (((uint64_t)x32 * x42) + ((0x2 * ((uint64_t)x34 * x40)) + (((uint64_t)x36 * x38) + (((uint64_t)x38 * x36) + ((0x2 * ((uint64_t)x40 * x34)) + (((uint64_t)x42 * x32) + (((uint64_t)x44 * x30) + ((0x2 * ((uint64_t)x46 * x28)) + ((uint64_t)x45 * x26)))))))))))))); + { uint64_t x60 = ((((uint64_t)x2 * x22) + (((uint64_t)x4 * x20) + (((uint64_t)x6 * x18) + (((uint64_t)x8 * x16) + (((uint64_t)x10 * x14) + (((uint64_t)x12 * x12) + (((uint64_t)x14 * x10) + (((uint64_t)x16 * x8) + (((uint64_t)x18 * x6) + (((uint64_t)x20 * x4) + ((uint64_t)x22 * x2))))))))))) + (0x239 * (((uint64_t)x24 * x45) + (((uint64_t)x26 * x46) + (((uint64_t)x28 * x44) + (((uint64_t)x30 * x42) + (((uint64_t)x32 * x40) + (((uint64_t)x34 * x38) + (((uint64_t)x36 * x36) + (((uint64_t)x38 * x34) + (((uint64_t)x40 * x32) + (((uint64_t)x42 * x30) + (((uint64_t)x44 * x28) + (((uint64_t)x46 * x26) + ((uint64_t)x45 * x24))))))))))))))); + { uint64_t x61 = ((((uint64_t)x2 * x20) + ((0x2 * ((uint64_t)x4 * x18)) + ((0x2 * ((uint64_t)x6 * x16)) + (((uint64_t)x8 * x14) + ((0x2 * ((uint64_t)x10 * x12)) + ((0x2 * ((uint64_t)x12 * x10)) + (((uint64_t)x14 * x8) + ((0x2 * ((uint64_t)x16 * x6)) + ((0x2 * ((uint64_t)x18 * x4)) + ((uint64_t)x20 * x2)))))))))) + (0x239 * ((0x2 * ((uint64_t)x22 * x45)) + ((0x2 * ((uint64_t)x24 * x46)) + (((uint64_t)x26 * x44) + ((0x2 * ((uint64_t)x28 * x42)) + ((0x2 * ((uint64_t)x30 * x40)) + (((uint64_t)x32 * x38) + ((0x2 * ((uint64_t)x34 * x36)) + ((0x2 * ((uint64_t)x36 * x34)) + (((uint64_t)x38 * x32) + ((0x2 * ((uint64_t)x40 * x30)) + ((0x2 * ((uint64_t)x42 * x28)) + (((uint64_t)x44 * x26) + ((0x2 * ((uint64_t)x46 * x24)) + (0x2 * ((uint64_t)x45 * x22))))))))))))))))); + { uint64_t x62 = ((((uint64_t)x2 * x18) + ((0x2 * ((uint64_t)x4 * x16)) + (((uint64_t)x6 * x14) + (((uint64_t)x8 * x12) + ((0x2 * ((uint64_t)x10 * x10)) + (((uint64_t)x12 * x8) + (((uint64_t)x14 * x6) + ((0x2 * ((uint64_t)x16 * x4)) + ((uint64_t)x18 * x2))))))))) + (0x239 * (((uint64_t)x20 * x45) + ((0x2 * ((uint64_t)x22 * x46)) + (((uint64_t)x24 * x44) + (((uint64_t)x26 * x42) + ((0x2 * ((uint64_t)x28 * x40)) + (((uint64_t)x30 * x38) + (((uint64_t)x32 * x36) + ((0x2 * ((uint64_t)x34 * x34)) + (((uint64_t)x36 * x32) + (((uint64_t)x38 * x30) + ((0x2 * ((uint64_t)x40 * x28)) + (((uint64_t)x42 * x26) + (((uint64_t)x44 * x24) + ((0x2 * ((uint64_t)x46 * x22)) + ((uint64_t)x45 * x20))))))))))))))))); + { uint64_t x63 = ((((uint64_t)x2 * x16) + (((uint64_t)x4 * x14) + (((uint64_t)x6 * x12) + (((uint64_t)x8 * x10) + (((uint64_t)x10 * x8) + (((uint64_t)x12 * x6) + (((uint64_t)x14 * x4) + ((uint64_t)x16 * x2)))))))) + (0x239 * (((uint64_t)x18 * x45) + (((uint64_t)x20 * x46) + (((uint64_t)x22 * x44) + (((uint64_t)x24 * x42) + (((uint64_t)x26 * x40) + (((uint64_t)x28 * x38) + (((uint64_t)x30 * x36) + (((uint64_t)x32 * x34) + (((uint64_t)x34 * x32) + (((uint64_t)x36 * x30) + (((uint64_t)x38 * x28) + (((uint64_t)x40 * x26) + (((uint64_t)x42 * x24) + (((uint64_t)x44 * x22) + (((uint64_t)x46 * x20) + ((uint64_t)x45 * x18)))))))))))))))))); + { uint64_t x64 = ((((uint64_t)x2 * x14) + ((0x2 * ((uint64_t)x4 * x12)) + ((0x2 * ((uint64_t)x6 * x10)) + (((uint64_t)x8 * x8) + ((0x2 * ((uint64_t)x10 * x6)) + ((0x2 * ((uint64_t)x12 * x4)) + ((uint64_t)x14 * x2))))))) + (0x239 * ((0x2 * ((uint64_t)x16 * x45)) + ((0x2 * ((uint64_t)x18 * x46)) + (((uint64_t)x20 * x44) + ((0x2 * ((uint64_t)x22 * x42)) + ((0x2 * ((uint64_t)x24 * x40)) + (((uint64_t)x26 * x38) + ((0x2 * ((uint64_t)x28 * x36)) + ((0x2 * ((uint64_t)x30 * x34)) + (((uint64_t)x32 * x32) + ((0x2 * ((uint64_t)x34 * x30)) + ((0x2 * ((uint64_t)x36 * x28)) + (((uint64_t)x38 * x26) + ((0x2 * ((uint64_t)x40 * x24)) + ((0x2 * ((uint64_t)x42 * x22)) + (((uint64_t)x44 * x20) + ((0x2 * ((uint64_t)x46 * x18)) + (0x2 * ((uint64_t)x45 * x16)))))))))))))))))))); + { uint64_t x65 = ((((uint64_t)x2 * x12) + ((0x2 * ((uint64_t)x4 * x10)) + (((uint64_t)x6 * x8) + (((uint64_t)x8 * x6) + ((0x2 * ((uint64_t)x10 * x4)) + ((uint64_t)x12 * x2)))))) + (0x239 * (((uint64_t)x14 * x45) + ((0x2 * ((uint64_t)x16 * x46)) + (((uint64_t)x18 * x44) + (((uint64_t)x20 * x42) + ((0x2 * ((uint64_t)x22 * x40)) + (((uint64_t)x24 * x38) + (((uint64_t)x26 * x36) + ((0x2 * ((uint64_t)x28 * x34)) + (((uint64_t)x30 * x32) + (((uint64_t)x32 * x30) + ((0x2 * ((uint64_t)x34 * x28)) + (((uint64_t)x36 * x26) + (((uint64_t)x38 * x24) + ((0x2 * ((uint64_t)x40 * x22)) + (((uint64_t)x42 * x20) + (((uint64_t)x44 * x18) + ((0x2 * ((uint64_t)x46 * x16)) + ((uint64_t)x45 * x14)))))))))))))))))))); + { uint64_t x66 = ((((uint64_t)x2 * x10) + (((uint64_t)x4 * x8) + (((uint64_t)x6 * x6) + (((uint64_t)x8 * x4) + ((uint64_t)x10 * x2))))) + (0x239 * (((uint64_t)x12 * x45) + (((uint64_t)x14 * x46) + (((uint64_t)x16 * x44) + (((uint64_t)x18 * x42) + (((uint64_t)x20 * x40) + (((uint64_t)x22 * x38) + (((uint64_t)x24 * x36) + (((uint64_t)x26 * x34) + (((uint64_t)x28 * x32) + (((uint64_t)x30 * x30) + (((uint64_t)x32 * x28) + (((uint64_t)x34 * x26) + (((uint64_t)x36 * x24) + (((uint64_t)x38 * x22) + (((uint64_t)x40 * x20) + (((uint64_t)x42 * x18) + (((uint64_t)x44 * x16) + (((uint64_t)x46 * x14) + ((uint64_t)x45 * x12))))))))))))))))))))); + { uint64_t x67 = ((((uint64_t)x2 * x8) + ((0x2 * ((uint64_t)x4 * x6)) + ((0x2 * ((uint64_t)x6 * x4)) + ((uint64_t)x8 * x2)))) + (0x239 * ((0x2 * ((uint64_t)x10 * x45)) + ((0x2 * ((uint64_t)x12 * x46)) + (((uint64_t)x14 * x44) + ((0x2 * ((uint64_t)x16 * x42)) + ((0x2 * ((uint64_t)x18 * x40)) + (((uint64_t)x20 * x38) + ((0x2 * ((uint64_t)x22 * x36)) + ((0x2 * ((uint64_t)x24 * x34)) + (((uint64_t)x26 * x32) + ((0x2 * ((uint64_t)x28 * x30)) + ((0x2 * ((uint64_t)x30 * x28)) + (((uint64_t)x32 * x26) + ((0x2 * ((uint64_t)x34 * x24)) + ((0x2 * ((uint64_t)x36 * x22)) + (((uint64_t)x38 * x20) + ((0x2 * ((uint64_t)x40 * x18)) + ((0x2 * ((uint64_t)x42 * x16)) + (((uint64_t)x44 * x14) + ((0x2 * ((uint64_t)x46 * x12)) + (0x2 * ((uint64_t)x45 * x10))))))))))))))))))))))); + { uint64_t x68 = ((((uint64_t)x2 * x6) + ((0x2 * ((uint64_t)x4 * x4)) + ((uint64_t)x6 * x2))) + (0x239 * (((uint64_t)x8 * x45) + ((0x2 * ((uint64_t)x10 * x46)) + (((uint64_t)x12 * x44) + (((uint64_t)x14 * x42) + ((0x2 * ((uint64_t)x16 * x40)) + (((uint64_t)x18 * x38) + (((uint64_t)x20 * x36) + ((0x2 * ((uint64_t)x22 * x34)) + (((uint64_t)x24 * x32) + (((uint64_t)x26 * x30) + ((0x2 * ((uint64_t)x28 * x28)) + (((uint64_t)x30 * x26) + (((uint64_t)x32 * x24) + ((0x2 * ((uint64_t)x34 * x22)) + (((uint64_t)x36 * x20) + (((uint64_t)x38 * x18) + ((0x2 * ((uint64_t)x40 * x16)) + (((uint64_t)x42 * x14) + (((uint64_t)x44 * x12) + ((0x2 * ((uint64_t)x46 * x10)) + ((uint64_t)x45 * x8))))))))))))))))))))))); + { uint64_t x69 = ((((uint64_t)x2 * x4) + ((uint64_t)x4 * x2)) + (0x239 * (((uint64_t)x6 * x45) + (((uint64_t)x8 * x46) + (((uint64_t)x10 * x44) + (((uint64_t)x12 * x42) + (((uint64_t)x14 * x40) + (((uint64_t)x16 * x38) + (((uint64_t)x18 * x36) + (((uint64_t)x20 * x34) + (((uint64_t)x22 * x32) + (((uint64_t)x24 * x30) + (((uint64_t)x26 * x28) + (((uint64_t)x28 * x26) + (((uint64_t)x30 * x24) + (((uint64_t)x32 * x22) + (((uint64_t)x34 * x20) + (((uint64_t)x36 * x18) + (((uint64_t)x38 * x16) + (((uint64_t)x40 * x14) + (((uint64_t)x42 * x12) + (((uint64_t)x44 * x10) + (((uint64_t)x46 * x8) + ((uint64_t)x45 * x6)))))))))))))))))))))))); + { uint64_t x70 = (((uint64_t)x2 * x2) + (0x239 * ((0x2 * ((uint64_t)x4 * x45)) + ((0x2 * ((uint64_t)x6 * x46)) + (((uint64_t)x8 * x44) + ((0x2 * ((uint64_t)x10 * x42)) + ((0x2 * ((uint64_t)x12 * x40)) + (((uint64_t)x14 * x38) + ((0x2 * ((uint64_t)x16 * x36)) + ((0x2 * ((uint64_t)x18 * x34)) + (((uint64_t)x20 * x32) + ((0x2 * ((uint64_t)x22 * x30)) + ((0x2 * ((uint64_t)x24 * x28)) + (((uint64_t)x26 * x26) + ((0x2 * ((uint64_t)x28 * x24)) + ((0x2 * ((uint64_t)x30 * x22)) + (((uint64_t)x32 * x20) + ((0x2 * ((uint64_t)x34 * x18)) + ((0x2 * ((uint64_t)x36 * x16)) + (((uint64_t)x38 * x14) + ((0x2 * ((uint64_t)x40 * x12)) + ((0x2 * ((uint64_t)x42 * x10)) + (((uint64_t)x44 * x8) + ((0x2 * ((uint64_t)x46 * x6)) + (0x2 * ((uint64_t)x45 * x4)))))))))))))))))))))))))); + { uint64_t x71 = (x70 >> 0x16); + { uint32_t x72 = ((uint32_t)x70 & 0x3fffff); + { uint64_t x73 = (x71 + x69); + { uint64_t x74 = (x73 >> 0x15); + { uint32_t x75 = ((uint32_t)x73 & 0x1fffff); + { uint64_t x76 = (x74 + x68); + { uint64_t x77 = (x76 >> 0x15); + { uint32_t x78 = ((uint32_t)x76 & 0x1fffff); + { uint64_t x79 = (x77 + x67); + { uint64_t x80 = (x79 >> 0x16); + { uint32_t x81 = ((uint32_t)x79 & 0x3fffff); + { uint64_t x82 = (x80 + x66); + { uint64_t x83 = (x82 >> 0x15); + { uint32_t x84 = ((uint32_t)x82 & 0x1fffff); + { uint64_t x85 = (x83 + x65); + { uint64_t x86 = (x85 >> 0x15); + { uint32_t x87 = ((uint32_t)x85 & 0x1fffff); + { uint64_t x88 = (x86 + x64); + { uint64_t x89 = (x88 >> 0x16); + { uint32_t x90 = ((uint32_t)x88 & 0x3fffff); + { uint64_t x91 = (x89 + x63); + { uint64_t x92 = (x91 >> 0x15); + { uint32_t x93 = ((uint32_t)x91 & 0x1fffff); + { uint64_t x94 = (x92 + x62); + { uint64_t x95 = (x94 >> 0x15); + { uint32_t x96 = ((uint32_t)x94 & 0x1fffff); + { uint64_t x97 = (x95 + x61); + { uint64_t x98 = (x97 >> 0x16); + { uint32_t x99 = ((uint32_t)x97 & 0x3fffff); + { uint64_t x100 = (x98 + x60); + { uint64_t x101 = (x100 >> 0x15); + { uint32_t x102 = ((uint32_t)x100 & 0x1fffff); + { uint64_t x103 = (x101 + x59); + { uint64_t x104 = (x103 >> 0x15); + { uint32_t x105 = ((uint32_t)x103 & 0x1fffff); + { uint64_t x106 = (x104 + x58); + { uint64_t x107 = (x106 >> 0x16); + { uint32_t x108 = ((uint32_t)x106 & 0x3fffff); + { uint64_t x109 = (x107 + x57); + { uint64_t x110 = (x109 >> 0x15); + { uint32_t x111 = ((uint32_t)x109 & 0x1fffff); + { uint64_t x112 = (x110 + x56); + { uint64_t x113 = (x112 >> 0x15); + { uint32_t x114 = ((uint32_t)x112 & 0x1fffff); + { uint64_t x115 = (x113 + x55); + { uint64_t x116 = (x115 >> 0x16); + { uint32_t x117 = ((uint32_t)x115 & 0x3fffff); + { uint64_t x118 = (x116 + x54); + { uint64_t x119 = (x118 >> 0x15); + { uint32_t x120 = ((uint32_t)x118 & 0x1fffff); + { uint64_t x121 = (x119 + x53); + { uint64_t x122 = (x121 >> 0x15); + { uint32_t x123 = ((uint32_t)x121 & 0x1fffff); + { uint64_t x124 = (x122 + x52); + { uint64_t x125 = (x124 >> 0x16); + { uint32_t x126 = ((uint32_t)x124 & 0x3fffff); + { uint64_t x127 = (x125 + x51); + { uint64_t x128 = (x127 >> 0x15); + { uint32_t x129 = ((uint32_t)x127 & 0x1fffff); + { uint64_t x130 = (x128 + x50); + { uint64_t x131 = (x130 >> 0x15); + { uint32_t x132 = ((uint32_t)x130 & 0x1fffff); + { uint64_t x133 = (x131 + x49); + { uint64_t x134 = (x133 >> 0x16); + { uint32_t x135 = ((uint32_t)x133 & 0x3fffff); + { uint64_t x136 = (x134 + x48); + { uint64_t x137 = (x136 >> 0x15); + { uint32_t x138 = ((uint32_t)x136 & 0x1fffff); + { uint64_t x139 = (x137 + x47); + { uint32_t x140 = (uint32_t) (x139 >> 0x15); + { uint32_t x141 = ((uint32_t)x139 & 0x1fffff); + { uint64_t x142 = (x72 + ((uint64_t)0x239 * x140)); + { uint32_t x143 = (uint32_t) (x142 >> 0x16); + { uint32_t x144 = ((uint32_t)x142 & 0x3fffff); + { uint32_t x145 = (x143 + x75); + { uint32_t x146 = (x145 >> 0x15); + { uint32_t x147 = (x145 & 0x1fffff); + out[0] = x144; + out[1] = x147; + out[2] = (x146 + x78); + out[3] = x81; + out[4] = x84; + out[5] = x87; + out[6] = x90; + out[7] = x93; + out[8] = x96; + out[9] = x99; + out[10] = x102; + out[11] = x105; + out[12] = x108; + out[13] = x111; + out[14] = x114; + out[15] = x117; + out[16] = x120; + out[17] = x123; + out[18] = x126; + out[19] = x129; + out[20] = x132; + out[21] = x135; + out[22] = x138; + out[23] = x141; + }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} +} diff --git a/src/Specific/solinas32_2e512m569_24limbs/fesquareDisplay.log b/src/Specific/solinas32_2e512m569_24limbs/fesquareDisplay.log new file mode 100644 index 000000000..a942ed88f --- /dev/null +++ b/src/Specific/solinas32_2e512m569_24limbs/fesquareDisplay.log @@ -0,0 +1,108 @@ +λ x : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32, +Interp-η +(λ var : Syntax.base_type → Type, + λ '(x45, x46, x44, x42, x40, x38, x36, x34, x32, x30, x28, x26, x24, x22, x20, x18, x16, x14, x12, x10, x8, x6, x4, x2)%core, + uint64_t x47 = (((uint64_t)x2 * x45) + ((0x2 * ((uint64_t)x4 * x46)) + (((uint64_t)x6 * x44) + (((uint64_t)x8 * x42) + ((0x2 * ((uint64_t)x10 * x40)) + (((uint64_t)x12 * x38) + (((uint64_t)x14 * x36) + ((0x2 * ((uint64_t)x16 * x34)) + (((uint64_t)x18 * x32) + (((uint64_t)x20 * x30) + ((0x2 * ((uint64_t)x22 * x28)) + (((uint64_t)x24 * x26) + (((uint64_t)x26 * x24) + ((0x2 * ((uint64_t)x28 * x22)) + (((uint64_t)x30 * x20) + (((uint64_t)x32 * x18) + ((0x2 * ((uint64_t)x34 * x16)) + (((uint64_t)x36 * x14) + (((uint64_t)x38 * x12) + ((0x2 * ((uint64_t)x40 * x10)) + (((uint64_t)x42 * x8) + (((uint64_t)x44 * x6) + ((0x2 * ((uint64_t)x46 * x4)) + ((uint64_t)x45 * x2)))))))))))))))))))))))); + uint64_t x48 = ((((uint64_t)x2 * x46) + (((uint64_t)x4 * x44) + (((uint64_t)x6 * x42) + (((uint64_t)x8 * x40) + (((uint64_t)x10 * x38) + (((uint64_t)x12 * x36) + (((uint64_t)x14 * x34) + (((uint64_t)x16 * x32) + (((uint64_t)x18 * x30) + (((uint64_t)x20 * x28) + (((uint64_t)x22 * x26) + (((uint64_t)x24 * x24) + (((uint64_t)x26 * x22) + (((uint64_t)x28 * x20) + (((uint64_t)x30 * x18) + (((uint64_t)x32 * x16) + (((uint64_t)x34 * x14) + (((uint64_t)x36 * x12) + (((uint64_t)x38 * x10) + (((uint64_t)x40 * x8) + (((uint64_t)x42 * x6) + (((uint64_t)x44 * x4) + ((uint64_t)x46 * x2))))))))))))))))))))))) + (0x239 * ((uint64_t)x45 * x45))); + uint64_t x49 = ((((uint64_t)x2 * x44) + ((0x2 * ((uint64_t)x4 * x42)) + ((0x2 * ((uint64_t)x6 * x40)) + (((uint64_t)x8 * x38) + ((0x2 * ((uint64_t)x10 * x36)) + ((0x2 * ((uint64_t)x12 * x34)) + (((uint64_t)x14 * x32) + ((0x2 * ((uint64_t)x16 * x30)) + ((0x2 * ((uint64_t)x18 * x28)) + (((uint64_t)x20 * x26) + ((0x2 * ((uint64_t)x22 * x24)) + ((0x2 * ((uint64_t)x24 * x22)) + (((uint64_t)x26 * x20) + ((0x2 * ((uint64_t)x28 * x18)) + ((0x2 * ((uint64_t)x30 * x16)) + (((uint64_t)x32 * x14) + ((0x2 * ((uint64_t)x34 * x12)) + ((0x2 * ((uint64_t)x36 * x10)) + (((uint64_t)x38 * x8) + ((0x2 * ((uint64_t)x40 * x6)) + ((0x2 * ((uint64_t)x42 * x4)) + ((uint64_t)x44 * x2)))))))))))))))))))))) + (0x239 * ((0x2 * ((uint64_t)x46 * x45)) + (0x2 * ((uint64_t)x45 * x46))))); + uint64_t x50 = ((((uint64_t)x2 * x42) + ((0x2 * ((uint64_t)x4 * x40)) + (((uint64_t)x6 * x38) + (((uint64_t)x8 * x36) + ((0x2 * ((uint64_t)x10 * x34)) + (((uint64_t)x12 * x32) + (((uint64_t)x14 * x30) + ((0x2 * ((uint64_t)x16 * x28)) + (((uint64_t)x18 * x26) + (((uint64_t)x20 * x24) + ((0x2 * ((uint64_t)x22 * x22)) + (((uint64_t)x24 * x20) + (((uint64_t)x26 * x18) + ((0x2 * ((uint64_t)x28 * x16)) + (((uint64_t)x30 * x14) + (((uint64_t)x32 * x12) + ((0x2 * ((uint64_t)x34 * x10)) + (((uint64_t)x36 * x8) + (((uint64_t)x38 * x6) + ((0x2 * ((uint64_t)x40 * x4)) + ((uint64_t)x42 * x2))))))))))))))))))))) + (0x239 * (((uint64_t)x44 * x45) + ((0x2 * ((uint64_t)x46 * x46)) + ((uint64_t)x45 * x44))))); + uint64_t x51 = ((((uint64_t)x2 * x40) + (((uint64_t)x4 * x38) + (((uint64_t)x6 * x36) + (((uint64_t)x8 * x34) + (((uint64_t)x10 * x32) + (((uint64_t)x12 * x30) + (((uint64_t)x14 * x28) + (((uint64_t)x16 * x26) + (((uint64_t)x18 * x24) + (((uint64_t)x20 * x22) + (((uint64_t)x22 * x20) + (((uint64_t)x24 * x18) + (((uint64_t)x26 * x16) + (((uint64_t)x28 * x14) + (((uint64_t)x30 * x12) + (((uint64_t)x32 * x10) + (((uint64_t)x34 * x8) + (((uint64_t)x36 * x6) + (((uint64_t)x38 * x4) + ((uint64_t)x40 * x2)))))))))))))))))))) + (0x239 * (((uint64_t)x42 * x45) + (((uint64_t)x44 * x46) + (((uint64_t)x46 * x44) + ((uint64_t)x45 * x42)))))); + uint64_t x52 = ((((uint64_t)x2 * x38) + ((0x2 * ((uint64_t)x4 * x36)) + ((0x2 * ((uint64_t)x6 * x34)) + (((uint64_t)x8 * x32) + ((0x2 * ((uint64_t)x10 * x30)) + ((0x2 * ((uint64_t)x12 * x28)) + (((uint64_t)x14 * x26) + ((0x2 * ((uint64_t)x16 * x24)) + ((0x2 * ((uint64_t)x18 * x22)) + (((uint64_t)x20 * x20) + ((0x2 * ((uint64_t)x22 * x18)) + ((0x2 * ((uint64_t)x24 * x16)) + (((uint64_t)x26 * x14) + ((0x2 * ((uint64_t)x28 * x12)) + ((0x2 * ((uint64_t)x30 * x10)) + (((uint64_t)x32 * x8) + ((0x2 * ((uint64_t)x34 * x6)) + ((0x2 * ((uint64_t)x36 * x4)) + ((uint64_t)x38 * x2))))))))))))))))))) + (0x239 * ((0x2 * ((uint64_t)x40 * x45)) + ((0x2 * ((uint64_t)x42 * x46)) + (((uint64_t)x44 * x44) + ((0x2 * ((uint64_t)x46 * x42)) + (0x2 * ((uint64_t)x45 * x40)))))))); + uint64_t x53 = ((((uint64_t)x2 * x36) + ((0x2 * ((uint64_t)x4 * x34)) + (((uint64_t)x6 * x32) + (((uint64_t)x8 * x30) + ((0x2 * ((uint64_t)x10 * x28)) + (((uint64_t)x12 * x26) + (((uint64_t)x14 * x24) + ((0x2 * ((uint64_t)x16 * x22)) + (((uint64_t)x18 * x20) + (((uint64_t)x20 * x18) + ((0x2 * ((uint64_t)x22 * x16)) + (((uint64_t)x24 * x14) + (((uint64_t)x26 * x12) + ((0x2 * ((uint64_t)x28 * x10)) + (((uint64_t)x30 * x8) + (((uint64_t)x32 * x6) + ((0x2 * ((uint64_t)x34 * x4)) + ((uint64_t)x36 * x2)))))))))))))))))) + (0x239 * (((uint64_t)x38 * x45) + ((0x2 * ((uint64_t)x40 * x46)) + (((uint64_t)x42 * x44) + (((uint64_t)x44 * x42) + ((0x2 * ((uint64_t)x46 * x40)) + ((uint64_t)x45 * x38)))))))); + uint64_t x54 = ((((uint64_t)x2 * x34) + (((uint64_t)x4 * x32) + (((uint64_t)x6 * x30) + (((uint64_t)x8 * x28) + (((uint64_t)x10 * x26) + (((uint64_t)x12 * x24) + (((uint64_t)x14 * x22) + (((uint64_t)x16 * x20) + (((uint64_t)x18 * x18) + (((uint64_t)x20 * x16) + (((uint64_t)x22 * x14) + (((uint64_t)x24 * x12) + (((uint64_t)x26 * x10) + (((uint64_t)x28 * x8) + (((uint64_t)x30 * x6) + (((uint64_t)x32 * x4) + ((uint64_t)x34 * x2))))))))))))))))) + (0x239 * (((uint64_t)x36 * x45) + (((uint64_t)x38 * x46) + (((uint64_t)x40 * x44) + (((uint64_t)x42 * x42) + (((uint64_t)x44 * x40) + (((uint64_t)x46 * x38) + ((uint64_t)x45 * x36))))))))); + uint64_t x55 = ((((uint64_t)x2 * x32) + ((0x2 * ((uint64_t)x4 * x30)) + ((0x2 * ((uint64_t)x6 * x28)) + (((uint64_t)x8 * x26) + ((0x2 * ((uint64_t)x10 * x24)) + ((0x2 * ((uint64_t)x12 * x22)) + (((uint64_t)x14 * x20) + ((0x2 * ((uint64_t)x16 * x18)) + ((0x2 * ((uint64_t)x18 * x16)) + (((uint64_t)x20 * x14) + ((0x2 * ((uint64_t)x22 * x12)) + ((0x2 * ((uint64_t)x24 * x10)) + (((uint64_t)x26 * x8) + ((0x2 * ((uint64_t)x28 * x6)) + ((0x2 * ((uint64_t)x30 * x4)) + ((uint64_t)x32 * x2)))))))))))))))) + (0x239 * ((0x2 * ((uint64_t)x34 * x45)) + ((0x2 * ((uint64_t)x36 * x46)) + (((uint64_t)x38 * x44) + ((0x2 * ((uint64_t)x40 * x42)) + ((0x2 * ((uint64_t)x42 * x40)) + (((uint64_t)x44 * x38) + ((0x2 * ((uint64_t)x46 * x36)) + (0x2 * ((uint64_t)x45 * x34))))))))))); + uint64_t x56 = ((((uint64_t)x2 * x30) + ((0x2 * ((uint64_t)x4 * x28)) + (((uint64_t)x6 * x26) + (((uint64_t)x8 * x24) + ((0x2 * ((uint64_t)x10 * x22)) + (((uint64_t)x12 * x20) + (((uint64_t)x14 * x18) + ((0x2 * ((uint64_t)x16 * x16)) + (((uint64_t)x18 * x14) + (((uint64_t)x20 * x12) + ((0x2 * ((uint64_t)x22 * x10)) + (((uint64_t)x24 * x8) + (((uint64_t)x26 * x6) + ((0x2 * ((uint64_t)x28 * x4)) + ((uint64_t)x30 * x2))))))))))))))) + (0x239 * (((uint64_t)x32 * x45) + ((0x2 * ((uint64_t)x34 * x46)) + (((uint64_t)x36 * x44) + (((uint64_t)x38 * x42) + ((0x2 * ((uint64_t)x40 * x40)) + (((uint64_t)x42 * x38) + (((uint64_t)x44 * x36) + ((0x2 * ((uint64_t)x46 * x34)) + ((uint64_t)x45 * x32))))))))))); + uint64_t x57 = ((((uint64_t)x2 * x28) + (((uint64_t)x4 * x26) + (((uint64_t)x6 * x24) + (((uint64_t)x8 * x22) + (((uint64_t)x10 * x20) + (((uint64_t)x12 * x18) + (((uint64_t)x14 * x16) + (((uint64_t)x16 * x14) + (((uint64_t)x18 * x12) + (((uint64_t)x20 * x10) + (((uint64_t)x22 * x8) + (((uint64_t)x24 * x6) + (((uint64_t)x26 * x4) + ((uint64_t)x28 * x2)))))))))))))) + (0x239 * (((uint64_t)x30 * x45) + (((uint64_t)x32 * x46) + (((uint64_t)x34 * x44) + (((uint64_t)x36 * x42) + (((uint64_t)x38 * x40) + (((uint64_t)x40 * x38) + (((uint64_t)x42 * x36) + (((uint64_t)x44 * x34) + (((uint64_t)x46 * x32) + ((uint64_t)x45 * x30)))))))))))); + uint64_t x58 = ((((uint64_t)x2 * x26) + ((0x2 * ((uint64_t)x4 * x24)) + ((0x2 * ((uint64_t)x6 * x22)) + (((uint64_t)x8 * x20) + ((0x2 * ((uint64_t)x10 * x18)) + ((0x2 * ((uint64_t)x12 * x16)) + (((uint64_t)x14 * x14) + ((0x2 * ((uint64_t)x16 * x12)) + ((0x2 * ((uint64_t)x18 * x10)) + (((uint64_t)x20 * x8) + ((0x2 * ((uint64_t)x22 * x6)) + ((0x2 * ((uint64_t)x24 * x4)) + ((uint64_t)x26 * x2))))))))))))) + (0x239 * ((0x2 * ((uint64_t)x28 * x45)) + ((0x2 * ((uint64_t)x30 * x46)) + (((uint64_t)x32 * x44) + ((0x2 * ((uint64_t)x34 * x42)) + ((0x2 * ((uint64_t)x36 * x40)) + (((uint64_t)x38 * x38) + ((0x2 * ((uint64_t)x40 * x36)) + ((0x2 * ((uint64_t)x42 * x34)) + (((uint64_t)x44 * x32) + ((0x2 * ((uint64_t)x46 * x30)) + (0x2 * ((uint64_t)x45 * x28)))))))))))))); + uint64_t x59 = ((((uint64_t)x2 * x24) + ((0x2 * ((uint64_t)x4 * x22)) + (((uint64_t)x6 * x20) + (((uint64_t)x8 * x18) + ((0x2 * ((uint64_t)x10 * x16)) + (((uint64_t)x12 * x14) + (((uint64_t)x14 * x12) + ((0x2 * ((uint64_t)x16 * x10)) + (((uint64_t)x18 * x8) + (((uint64_t)x20 * x6) + ((0x2 * ((uint64_t)x22 * x4)) + ((uint64_t)x24 * x2)))))))))))) + (0x239 * (((uint64_t)x26 * x45) + ((0x2 * ((uint64_t)x28 * x46)) + (((uint64_t)x30 * x44) + (((uint64_t)x32 * x42) + ((0x2 * ((uint64_t)x34 * x40)) + (((uint64_t)x36 * x38) + (((uint64_t)x38 * x36) + ((0x2 * ((uint64_t)x40 * x34)) + (((uint64_t)x42 * x32) + (((uint64_t)x44 * x30) + ((0x2 * ((uint64_t)x46 * x28)) + ((uint64_t)x45 * x26)))))))))))))); + uint64_t x60 = ((((uint64_t)x2 * x22) + (((uint64_t)x4 * x20) + (((uint64_t)x6 * x18) + (((uint64_t)x8 * x16) + (((uint64_t)x10 * x14) + (((uint64_t)x12 * x12) + (((uint64_t)x14 * x10) + (((uint64_t)x16 * x8) + (((uint64_t)x18 * x6) + (((uint64_t)x20 * x4) + ((uint64_t)x22 * x2))))))))))) + (0x239 * (((uint64_t)x24 * x45) + (((uint64_t)x26 * x46) + (((uint64_t)x28 * x44) + (((uint64_t)x30 * x42) + (((uint64_t)x32 * x40) + (((uint64_t)x34 * x38) + (((uint64_t)x36 * x36) + (((uint64_t)x38 * x34) + (((uint64_t)x40 * x32) + (((uint64_t)x42 * x30) + (((uint64_t)x44 * x28) + (((uint64_t)x46 * x26) + ((uint64_t)x45 * x24))))))))))))))); + uint64_t x61 = ((((uint64_t)x2 * x20) + ((0x2 * ((uint64_t)x4 * x18)) + ((0x2 * ((uint64_t)x6 * x16)) + (((uint64_t)x8 * x14) + ((0x2 * ((uint64_t)x10 * x12)) + ((0x2 * ((uint64_t)x12 * x10)) + (((uint64_t)x14 * x8) + ((0x2 * ((uint64_t)x16 * x6)) + ((0x2 * ((uint64_t)x18 * x4)) + ((uint64_t)x20 * x2)))))))))) + (0x239 * ((0x2 * ((uint64_t)x22 * x45)) + ((0x2 * ((uint64_t)x24 * x46)) + (((uint64_t)x26 * x44) + ((0x2 * ((uint64_t)x28 * x42)) + ((0x2 * ((uint64_t)x30 * x40)) + (((uint64_t)x32 * x38) + ((0x2 * ((uint64_t)x34 * x36)) + ((0x2 * ((uint64_t)x36 * x34)) + (((uint64_t)x38 * x32) + ((0x2 * ((uint64_t)x40 * x30)) + ((0x2 * ((uint64_t)x42 * x28)) + (((uint64_t)x44 * x26) + ((0x2 * ((uint64_t)x46 * x24)) + (0x2 * ((uint64_t)x45 * x22))))))))))))))))); + uint64_t x62 = ((((uint64_t)x2 * x18) + ((0x2 * ((uint64_t)x4 * x16)) + (((uint64_t)x6 * x14) + (((uint64_t)x8 * x12) + ((0x2 * ((uint64_t)x10 * x10)) + (((uint64_t)x12 * x8) + (((uint64_t)x14 * x6) + ((0x2 * ((uint64_t)x16 * x4)) + ((uint64_t)x18 * x2))))))))) + (0x239 * (((uint64_t)x20 * x45) + ((0x2 * ((uint64_t)x22 * x46)) + (((uint64_t)x24 * x44) + (((uint64_t)x26 * x42) + ((0x2 * ((uint64_t)x28 * x40)) + (((uint64_t)x30 * x38) + (((uint64_t)x32 * x36) + ((0x2 * ((uint64_t)x34 * x34)) + (((uint64_t)x36 * x32) + (((uint64_t)x38 * x30) + ((0x2 * ((uint64_t)x40 * x28)) + (((uint64_t)x42 * x26) + (((uint64_t)x44 * x24) + ((0x2 * ((uint64_t)x46 * x22)) + ((uint64_t)x45 * x20))))))))))))))))); + uint64_t x63 = ((((uint64_t)x2 * x16) + (((uint64_t)x4 * x14) + (((uint64_t)x6 * x12) + (((uint64_t)x8 * x10) + (((uint64_t)x10 * x8) + (((uint64_t)x12 * x6) + (((uint64_t)x14 * x4) + ((uint64_t)x16 * x2)))))))) + (0x239 * (((uint64_t)x18 * x45) + (((uint64_t)x20 * x46) + (((uint64_t)x22 * x44) + (((uint64_t)x24 * x42) + (((uint64_t)x26 * x40) + (((uint64_t)x28 * x38) + (((uint64_t)x30 * x36) + (((uint64_t)x32 * x34) + (((uint64_t)x34 * x32) + (((uint64_t)x36 * x30) + (((uint64_t)x38 * x28) + (((uint64_t)x40 * x26) + (((uint64_t)x42 * x24) + (((uint64_t)x44 * x22) + (((uint64_t)x46 * x20) + ((uint64_t)x45 * x18)))))))))))))))))); + uint64_t x64 = ((((uint64_t)x2 * x14) + ((0x2 * ((uint64_t)x4 * x12)) + ((0x2 * ((uint64_t)x6 * x10)) + (((uint64_t)x8 * x8) + ((0x2 * ((uint64_t)x10 * x6)) + ((0x2 * ((uint64_t)x12 * x4)) + ((uint64_t)x14 * x2))))))) + (0x239 * ((0x2 * ((uint64_t)x16 * x45)) + ((0x2 * ((uint64_t)x18 * x46)) + (((uint64_t)x20 * x44) + ((0x2 * ((uint64_t)x22 * x42)) + ((0x2 * ((uint64_t)x24 * x40)) + (((uint64_t)x26 * x38) + ((0x2 * ((uint64_t)x28 * x36)) + ((0x2 * ((uint64_t)x30 * x34)) + (((uint64_t)x32 * x32) + ((0x2 * ((uint64_t)x34 * x30)) + ((0x2 * ((uint64_t)x36 * x28)) + (((uint64_t)x38 * x26) + ((0x2 * ((uint64_t)x40 * x24)) + ((0x2 * ((uint64_t)x42 * x22)) + (((uint64_t)x44 * x20) + ((0x2 * ((uint64_t)x46 * x18)) + (0x2 * ((uint64_t)x45 * x16)))))))))))))))))))); + uint64_t x65 = ((((uint64_t)x2 * x12) + ((0x2 * ((uint64_t)x4 * x10)) + (((uint64_t)x6 * x8) + (((uint64_t)x8 * x6) + ((0x2 * ((uint64_t)x10 * x4)) + ((uint64_t)x12 * x2)))))) + (0x239 * (((uint64_t)x14 * x45) + ((0x2 * ((uint64_t)x16 * x46)) + (((uint64_t)x18 * x44) + (((uint64_t)x20 * x42) + ((0x2 * ((uint64_t)x22 * x40)) + (((uint64_t)x24 * x38) + (((uint64_t)x26 * x36) + ((0x2 * ((uint64_t)x28 * x34)) + (((uint64_t)x30 * x32) + (((uint64_t)x32 * x30) + ((0x2 * ((uint64_t)x34 * x28)) + (((uint64_t)x36 * x26) + (((uint64_t)x38 * x24) + ((0x2 * ((uint64_t)x40 * x22)) + (((uint64_t)x42 * x20) + (((uint64_t)x44 * x18) + ((0x2 * ((uint64_t)x46 * x16)) + ((uint64_t)x45 * x14)))))))))))))))))))); + uint64_t x66 = ((((uint64_t)x2 * x10) + (((uint64_t)x4 * x8) + (((uint64_t)x6 * x6) + (((uint64_t)x8 * x4) + ((uint64_t)x10 * x2))))) + (0x239 * (((uint64_t)x12 * x45) + (((uint64_t)x14 * x46) + (((uint64_t)x16 * x44) + (((uint64_t)x18 * x42) + (((uint64_t)x20 * x40) + (((uint64_t)x22 * x38) + (((uint64_t)x24 * x36) + (((uint64_t)x26 * x34) + (((uint64_t)x28 * x32) + (((uint64_t)x30 * x30) + (((uint64_t)x32 * x28) + (((uint64_t)x34 * x26) + (((uint64_t)x36 * x24) + (((uint64_t)x38 * x22) + (((uint64_t)x40 * x20) + (((uint64_t)x42 * x18) + (((uint64_t)x44 * x16) + (((uint64_t)x46 * x14) + ((uint64_t)x45 * x12))))))))))))))))))))); + uint64_t x67 = ((((uint64_t)x2 * x8) + ((0x2 * ((uint64_t)x4 * x6)) + ((0x2 * ((uint64_t)x6 * x4)) + ((uint64_t)x8 * x2)))) + (0x239 * ((0x2 * ((uint64_t)x10 * x45)) + ((0x2 * ((uint64_t)x12 * x46)) + (((uint64_t)x14 * x44) + ((0x2 * ((uint64_t)x16 * x42)) + ((0x2 * ((uint64_t)x18 * x40)) + (((uint64_t)x20 * x38) + ((0x2 * ((uint64_t)x22 * x36)) + ((0x2 * ((uint64_t)x24 * x34)) + (((uint64_t)x26 * x32) + ((0x2 * ((uint64_t)x28 * x30)) + ((0x2 * ((uint64_t)x30 * x28)) + (((uint64_t)x32 * x26) + ((0x2 * ((uint64_t)x34 * x24)) + ((0x2 * ((uint64_t)x36 * x22)) + (((uint64_t)x38 * x20) + ((0x2 * ((uint64_t)x40 * x18)) + ((0x2 * ((uint64_t)x42 * x16)) + (((uint64_t)x44 * x14) + ((0x2 * ((uint64_t)x46 * x12)) + (0x2 * ((uint64_t)x45 * x10))))))))))))))))))))))); + uint64_t x68 = ((((uint64_t)x2 * x6) + ((0x2 * ((uint64_t)x4 * x4)) + ((uint64_t)x6 * x2))) + (0x239 * (((uint64_t)x8 * x45) + ((0x2 * ((uint64_t)x10 * x46)) + (((uint64_t)x12 * x44) + (((uint64_t)x14 * x42) + ((0x2 * ((uint64_t)x16 * x40)) + (((uint64_t)x18 * x38) + (((uint64_t)x20 * x36) + ((0x2 * ((uint64_t)x22 * x34)) + (((uint64_t)x24 * x32) + (((uint64_t)x26 * x30) + ((0x2 * ((uint64_t)x28 * x28)) + (((uint64_t)x30 * x26) + (((uint64_t)x32 * x24) + ((0x2 * ((uint64_t)x34 * x22)) + (((uint64_t)x36 * x20) + (((uint64_t)x38 * x18) + ((0x2 * ((uint64_t)x40 * x16)) + (((uint64_t)x42 * x14) + (((uint64_t)x44 * x12) + ((0x2 * ((uint64_t)x46 * x10)) + ((uint64_t)x45 * x8))))))))))))))))))))))); + uint64_t x69 = ((((uint64_t)x2 * x4) + ((uint64_t)x4 * x2)) + (0x239 * (((uint64_t)x6 * x45) + (((uint64_t)x8 * x46) + (((uint64_t)x10 * x44) + (((uint64_t)x12 * x42) + (((uint64_t)x14 * x40) + (((uint64_t)x16 * x38) + (((uint64_t)x18 * x36) + (((uint64_t)x20 * x34) + (((uint64_t)x22 * x32) + (((uint64_t)x24 * x30) + (((uint64_t)x26 * x28) + (((uint64_t)x28 * x26) + (((uint64_t)x30 * x24) + (((uint64_t)x32 * x22) + (((uint64_t)x34 * x20) + (((uint64_t)x36 * x18) + (((uint64_t)x38 * x16) + (((uint64_t)x40 * x14) + (((uint64_t)x42 * x12) + (((uint64_t)x44 * x10) + (((uint64_t)x46 * x8) + ((uint64_t)x45 * x6)))))))))))))))))))))))); + uint64_t x70 = (((uint64_t)x2 * x2) + (0x239 * ((0x2 * ((uint64_t)x4 * x45)) + ((0x2 * ((uint64_t)x6 * x46)) + (((uint64_t)x8 * x44) + ((0x2 * ((uint64_t)x10 * x42)) + ((0x2 * ((uint64_t)x12 * x40)) + (((uint64_t)x14 * x38) + ((0x2 * ((uint64_t)x16 * x36)) + ((0x2 * ((uint64_t)x18 * x34)) + (((uint64_t)x20 * x32) + ((0x2 * ((uint64_t)x22 * x30)) + ((0x2 * ((uint64_t)x24 * x28)) + (((uint64_t)x26 * x26) + ((0x2 * ((uint64_t)x28 * x24)) + ((0x2 * ((uint64_t)x30 * x22)) + (((uint64_t)x32 * x20) + ((0x2 * ((uint64_t)x34 * x18)) + ((0x2 * ((uint64_t)x36 * x16)) + (((uint64_t)x38 * x14) + ((0x2 * ((uint64_t)x40 * x12)) + ((0x2 * ((uint64_t)x42 * x10)) + (((uint64_t)x44 * x8) + ((0x2 * ((uint64_t)x46 * x6)) + (0x2 * ((uint64_t)x45 * x4)))))))))))))))))))))))))); + uint64_t x71 = (x70 >> 0x16); + uint32_t x72 = ((uint32_t)x70 & 0x3fffff); + uint64_t x73 = (x71 + x69); + uint64_t x74 = (x73 >> 0x15); + uint32_t x75 = ((uint32_t)x73 & 0x1fffff); + uint64_t x76 = (x74 + x68); + uint64_t x77 = (x76 >> 0x15); + uint32_t x78 = ((uint32_t)x76 & 0x1fffff); + uint64_t x79 = (x77 + x67); + uint64_t x80 = (x79 >> 0x16); + uint32_t x81 = ((uint32_t)x79 & 0x3fffff); + uint64_t x82 = (x80 + x66); + uint64_t x83 = (x82 >> 0x15); + uint32_t x84 = ((uint32_t)x82 & 0x1fffff); + uint64_t x85 = (x83 + x65); + uint64_t x86 = (x85 >> 0x15); + uint32_t x87 = ((uint32_t)x85 & 0x1fffff); + uint64_t x88 = (x86 + x64); + uint64_t x89 = (x88 >> 0x16); + uint32_t x90 = ((uint32_t)x88 & 0x3fffff); + uint64_t x91 = (x89 + x63); + uint64_t x92 = (x91 >> 0x15); + uint32_t x93 = ((uint32_t)x91 & 0x1fffff); + uint64_t x94 = (x92 + x62); + uint64_t x95 = (x94 >> 0x15); + uint32_t x96 = ((uint32_t)x94 & 0x1fffff); + uint64_t x97 = (x95 + x61); + uint64_t x98 = (x97 >> 0x16); + uint32_t x99 = ((uint32_t)x97 & 0x3fffff); + uint64_t x100 = (x98 + x60); + uint64_t x101 = (x100 >> 0x15); + uint32_t x102 = ((uint32_t)x100 & 0x1fffff); + uint64_t x103 = (x101 + x59); + uint64_t x104 = (x103 >> 0x15); + uint32_t x105 = ((uint32_t)x103 & 0x1fffff); + uint64_t x106 = (x104 + x58); + uint64_t x107 = (x106 >> 0x16); + uint32_t x108 = ((uint32_t)x106 & 0x3fffff); + uint64_t x109 = (x107 + x57); + uint64_t x110 = (x109 >> 0x15); + uint32_t x111 = ((uint32_t)x109 & 0x1fffff); + uint64_t x112 = (x110 + x56); + uint64_t x113 = (x112 >> 0x15); + uint32_t x114 = ((uint32_t)x112 & 0x1fffff); + uint64_t x115 = (x113 + x55); + uint64_t x116 = (x115 >> 0x16); + uint32_t x117 = ((uint32_t)x115 & 0x3fffff); + uint64_t x118 = (x116 + x54); + uint64_t x119 = (x118 >> 0x15); + uint32_t x120 = ((uint32_t)x118 & 0x1fffff); + uint64_t x121 = (x119 + x53); + uint64_t x122 = (x121 >> 0x15); + uint32_t x123 = ((uint32_t)x121 & 0x1fffff); + uint64_t x124 = (x122 + x52); + uint64_t x125 = (x124 >> 0x16); + uint32_t x126 = ((uint32_t)x124 & 0x3fffff); + uint64_t x127 = (x125 + x51); + uint64_t x128 = (x127 >> 0x15); + uint32_t x129 = ((uint32_t)x127 & 0x1fffff); + uint64_t x130 = (x128 + x50); + uint64_t x131 = (x130 >> 0x15); + uint32_t x132 = ((uint32_t)x130 & 0x1fffff); + uint64_t x133 = (x131 + x49); + uint64_t x134 = (x133 >> 0x16); + uint32_t x135 = ((uint32_t)x133 & 0x3fffff); + uint64_t x136 = (x134 + x48); + uint64_t x137 = (x136 >> 0x15); + uint32_t x138 = ((uint32_t)x136 & 0x1fffff); + uint64_t x139 = (x137 + x47); + uint32_t x140 = (uint32_t) (x139 >> 0x15); + uint32_t x141 = ((uint32_t)x139 & 0x1fffff); + uint64_t x142 = (x72 + ((uint64_t)0x239 * x140)); + uint32_t x143 = (uint32_t) (x142 >> 0x16); + uint32_t x144 = ((uint32_t)x142 & 0x3fffff); + uint32_t x145 = (x143 + x75); + uint32_t x146 = (x145 >> 0x15); + uint32_t x147 = (x145 & 0x1fffff); + return (Return x141, Return x138, Return x135, Return x132, Return x129, Return x126, Return x123, Return x120, Return x117, Return x114, Return x111, Return x108, Return x105, Return x102, Return x99, Return x96, Return x93, Return x90, Return x87, Return x84, Return x81, (x146 + x78), Return x147, Return x144)) +x + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t) diff --git a/src/Specific/solinas32_2e512m569_24limbs/fesub.c b/src/Specific/solinas32_2e512m569_24limbs/fesub.c new file mode 100644 index 000000000..3acb523c0 --- /dev/null +++ b/src/Specific/solinas32_2e512m569_24limbs/fesub.c @@ -0,0 +1,75 @@ +static void fesub(uint32_t out[24], const uint32_t in1[24], const uint32_t in2[24]) { + { const uint32_t x48 = in1[23]; + { const uint32_t x49 = in1[22]; + { const uint32_t x47 = in1[21]; + { const uint32_t x45 = in1[20]; + { const uint32_t x43 = in1[19]; + { const uint32_t x41 = in1[18]; + { const uint32_t x39 = in1[17]; + { const uint32_t x37 = in1[16]; + { const uint32_t x35 = in1[15]; + { const uint32_t x33 = in1[14]; + { const uint32_t x31 = in1[13]; + { const uint32_t x29 = in1[12]; + { const uint32_t x27 = in1[11]; + { const uint32_t x25 = in1[10]; + { const uint32_t x23 = in1[9]; + { const uint32_t x21 = in1[8]; + { const uint32_t x19 = in1[7]; + { const uint32_t x17 = in1[6]; + { const uint32_t x15 = in1[5]; + { const uint32_t x13 = in1[4]; + { const uint32_t x11 = in1[3]; + { const uint32_t x9 = in1[2]; + { const uint32_t x7 = in1[1]; + { const uint32_t x5 = in1[0]; + { const uint32_t x94 = in2[23]; + { const uint32_t x95 = in2[22]; + { const uint32_t x93 = in2[21]; + { const uint32_t x91 = in2[20]; + { const uint32_t x89 = in2[19]; + { const uint32_t x87 = in2[18]; + { const uint32_t x85 = in2[17]; + { const uint32_t x83 = in2[16]; + { const uint32_t x81 = in2[15]; + { const uint32_t x79 = in2[14]; + { const uint32_t x77 = in2[13]; + { const uint32_t x75 = in2[12]; + { const uint32_t x73 = in2[11]; + { const uint32_t x71 = in2[10]; + { const uint32_t x69 = in2[9]; + { const uint32_t x67 = in2[8]; + { const uint32_t x65 = in2[7]; + { const uint32_t x63 = in2[6]; + { const uint32_t x61 = in2[5]; + { const uint32_t x59 = in2[4]; + { const uint32_t x57 = in2[3]; + { const uint32_t x55 = in2[2]; + { const uint32_t x53 = in2[1]; + { const uint32_t x51 = in2[0]; + out[0] = ((0x7ffb8e + x5) - x51); + out[1] = ((0x3ffffe + x7) - x53); + out[2] = ((0x3ffffe + x9) - x55); + out[3] = ((0x7ffffe + x11) - x57); + out[4] = ((0x3ffffe + x13) - x59); + out[5] = ((0x3ffffe + x15) - x61); + out[6] = ((0x7ffffe + x17) - x63); + out[7] = ((0x3ffffe + x19) - x65); + out[8] = ((0x3ffffe + x21) - x67); + out[9] = ((0x7ffffe + x23) - x69); + out[10] = ((0x3ffffe + x25) - x71); + out[11] = ((0x3ffffe + x27) - x73); + out[12] = ((0x7ffffe + x29) - x75); + out[13] = ((0x3ffffe + x31) - x77); + out[14] = ((0x3ffffe + x33) - x79); + out[15] = ((0x7ffffe + x35) - x81); + out[16] = ((0x3ffffe + x37) - x83); + out[17] = ((0x3ffffe + x39) - x85); + out[18] = ((0x7ffffe + x41) - x87); + out[19] = ((0x3ffffe + x43) - x89); + out[20] = ((0x3ffffe + x45) - x91); + out[21] = ((0x7ffffe + x47) - x93); + out[22] = ((0x3ffffe + x49) - x95); + out[23] = ((0x3ffffe + x48) - x94); + }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} +} diff --git a/src/Specific/solinas32_2e512m569_24limbs/fesubDisplay.log b/src/Specific/solinas32_2e512m569_24limbs/fesubDisplay.log new file mode 100644 index 000000000..a92e47200 --- /dev/null +++ b/src/Specific/solinas32_2e512m569_24limbs/fesubDisplay.log @@ -0,0 +1,7 @@ +λ x x0 : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32, +Interp-η +(λ var : Syntax.base_type → Type, + λ '(x48, x49, x47, x45, x43, x41, x39, x37, x35, x33, x31, x29, x27, x25, x23, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x94, x95, x93, x91, x89, x87, x85, x83, x81, x79, x77, x75, x73, x71, x69, x67, x65, x63, x61, x59, x57, x55, x53, x51))%core, + (((0x3ffffe + x48) - x94), ((0x3ffffe + x49) - x95), ((0x7ffffe + x47) - x93), ((0x3ffffe + x45) - x91), ((0x3ffffe + x43) - x89), ((0x7ffffe + x41) - x87), ((0x3ffffe + x39) - x85), ((0x3ffffe + x37) - x83), ((0x7ffffe + x35) - x81), ((0x3ffffe + x33) - x79), ((0x3ffffe + x31) - x77), ((0x7ffffe + x29) - x75), ((0x3ffffe + x27) - x73), ((0x3ffffe + x25) - x71), ((0x7ffffe + x23) - x69), ((0x3ffffe + x21) - x67), ((0x3ffffe + x19) - x65), ((0x7ffffe + x17) - x63), ((0x3ffffe + x15) - x61), ((0x3ffffe + x13) - x59), ((0x7ffffe + x11) - x57), ((0x3ffffe + x9) - x55), ((0x3ffffe + x7) - x53), ((0x7ffb8e + x5) - x51))) +(x, x0)%core + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t) diff --git a/src/Specific/solinas32_2e512m569_24limbs/freeze.c b/src/Specific/solinas32_2e512m569_24limbs/freeze.c new file mode 100644 index 000000000..a06bca255 --- /dev/null +++ b/src/Specific/solinas32_2e512m569_24limbs/freeze.c @@ -0,0 +1,124 @@ +static void freeze(uint32_t out[24], const uint32_t in1[24]) { + { const uint32_t x45 = in1[23]; + { const uint32_t x46 = in1[22]; + { const uint32_t x44 = in1[21]; + { const uint32_t x42 = in1[20]; + { const uint32_t x40 = in1[19]; + { const uint32_t x38 = in1[18]; + { const uint32_t x36 = in1[17]; + { const uint32_t x34 = in1[16]; + { const uint32_t x32 = in1[15]; + { const uint32_t x30 = in1[14]; + { const uint32_t x28 = in1[13]; + { const uint32_t x26 = in1[12]; + { const uint32_t x24 = in1[11]; + { const uint32_t x22 = in1[10]; + { const uint32_t x20 = in1[9]; + { const uint32_t x18 = in1[8]; + { const uint32_t x16 = in1[7]; + { const uint32_t x14 = in1[6]; + { const uint32_t x12 = in1[5]; + { const uint32_t x10 = in1[4]; + { const uint32_t x8 = in1[3]; + { const uint32_t x6 = in1[2]; + { const uint32_t x4 = in1[1]; + { const uint32_t x2 = in1[0]; + { uint32_t x48, uint8_t x49 = Op (Syntax.SubWithGetBorrow 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (0x0, Return x2, 0x3ffdc7); + { uint32_t x51, uint8_t x52 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x49, Return x4, 0x1fffff); + { uint32_t x54, uint8_t x55 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x52, Return x6, 0x1fffff); + { uint32_t x57, uint8_t x58 = Op (Syntax.SubWithGetBorrow 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x55, Return x8, 0x3fffff); + { uint32_t x60, uint8_t x61 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x58, Return x10, 0x1fffff); + { uint32_t x63, uint8_t x64 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x61, Return x12, 0x1fffff); + { uint32_t x66, uint8_t x67 = Op (Syntax.SubWithGetBorrow 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x64, Return x14, 0x3fffff); + { uint32_t x69, uint8_t x70 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x67, Return x16, 0x1fffff); + { uint32_t x72, uint8_t x73 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x70, Return x18, 0x1fffff); + { uint32_t x75, uint8_t x76 = Op (Syntax.SubWithGetBorrow 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x73, Return x20, 0x3fffff); + { uint32_t x78, uint8_t x79 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x76, Return x22, 0x1fffff); + { uint32_t x81, uint8_t x82 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x79, Return x24, 0x1fffff); + { uint32_t x84, uint8_t x85 = Op (Syntax.SubWithGetBorrow 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x82, Return x26, 0x3fffff); + { uint32_t x87, uint8_t x88 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x85, Return x28, 0x1fffff); + { uint32_t x90, uint8_t x91 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x88, Return x30, 0x1fffff); + { uint32_t x93, uint8_t x94 = Op (Syntax.SubWithGetBorrow 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x91, Return x32, 0x3fffff); + { uint32_t x96, uint8_t x97 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x94, Return x34, 0x1fffff); + { uint32_t x99, uint8_t x100 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x97, Return x36, 0x1fffff); + { uint32_t x102, uint8_t x103 = Op (Syntax.SubWithGetBorrow 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x100, Return x38, 0x3fffff); + { uint32_t x105, uint8_t x106 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x103, Return x40, 0x1fffff); + { uint32_t x108, uint8_t x109 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x106, Return x42, 0x1fffff); + { uint32_t x111, uint8_t x112 = Op (Syntax.SubWithGetBorrow 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x109, Return x44, 0x3fffff); + { uint32_t x114, uint8_t x115 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x112, Return x46, 0x1fffff); + { uint32_t x117, uint8_t x118 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x115, Return x45, 0x1fffff); + { uint32_t x119 = cmovznz32(x118, 0x0, 0xffffffff); + { uint32_t x120 = (x119 & 0x3ffdc7); + { uint32_t x122, uint8_t x123 = Op (Syntax.AddWithGetCarry 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (0x0, Return x48, Return x120); + { uint32_t x124 = (x119 & 0x1fffff); + { uint32_t x126, uint8_t x127 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x123, Return x51, Return x124); + { uint32_t x128 = (x119 & 0x1fffff); + { uint32_t x130, uint8_t x131 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x127, Return x54, Return x128); + { uint32_t x132 = (x119 & 0x3fffff); + { uint32_t x134, uint8_t x135 = Op (Syntax.AddWithGetCarry 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x131, Return x57, Return x132); + { uint32_t x136 = (x119 & 0x1fffff); + { uint32_t x138, uint8_t x139 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x135, Return x60, Return x136); + { uint32_t x140 = (x119 & 0x1fffff); + { uint32_t x142, uint8_t x143 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x139, Return x63, Return x140); + { uint32_t x144 = (x119 & 0x3fffff); + { uint32_t x146, uint8_t x147 = Op (Syntax.AddWithGetCarry 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x143, Return x66, Return x144); + { uint32_t x148 = (x119 & 0x1fffff); + { uint32_t x150, uint8_t x151 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x147, Return x69, Return x148); + { uint32_t x152 = (x119 & 0x1fffff); + { uint32_t x154, uint8_t x155 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x151, Return x72, Return x152); + { uint32_t x156 = (x119 & 0x3fffff); + { uint32_t x158, uint8_t x159 = Op (Syntax.AddWithGetCarry 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x155, Return x75, Return x156); + { uint32_t x160 = (x119 & 0x1fffff); + { uint32_t x162, uint8_t x163 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x159, Return x78, Return x160); + { uint32_t x164 = (x119 & 0x1fffff); + { uint32_t x166, uint8_t x167 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x163, Return x81, Return x164); + { uint32_t x168 = (x119 & 0x3fffff); + { uint32_t x170, uint8_t x171 = Op (Syntax.AddWithGetCarry 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x167, Return x84, Return x168); + { uint32_t x172 = (x119 & 0x1fffff); + { uint32_t x174, uint8_t x175 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x171, Return x87, Return x172); + { uint32_t x176 = (x119 & 0x1fffff); + { uint32_t x178, uint8_t x179 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x175, Return x90, Return x176); + { uint32_t x180 = (x119 & 0x3fffff); + { uint32_t x182, uint8_t x183 = Op (Syntax.AddWithGetCarry 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x179, Return x93, Return x180); + { uint32_t x184 = (x119 & 0x1fffff); + { uint32_t x186, uint8_t x187 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x183, Return x96, Return x184); + { uint32_t x188 = (x119 & 0x1fffff); + { uint32_t x190, uint8_t x191 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x187, Return x99, Return x188); + { uint32_t x192 = (x119 & 0x3fffff); + { uint32_t x194, uint8_t x195 = Op (Syntax.AddWithGetCarry 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x191, Return x102, Return x192); + { uint32_t x196 = (x119 & 0x1fffff); + { uint32_t x198, uint8_t x199 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x195, Return x105, Return x196); + { uint32_t x200 = (x119 & 0x1fffff); + { uint32_t x202, uint8_t x203 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x199, Return x108, Return x200); + { uint32_t x204 = (x119 & 0x3fffff); + { uint32_t x206, uint8_t x207 = Op (Syntax.AddWithGetCarry 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x203, Return x111, Return x204); + { uint32_t x208 = (x119 & 0x1fffff); + { uint32_t x210, uint8_t x211 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x207, Return x114, Return x208); + { uint32_t x212 = (x119 & 0x1fffff); + { uint32_t x214, uint8_t _ = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x211, Return x117, Return x212); + out[0] = x122; + out[1] = x126; + out[2] = x130; + out[3] = x134; + out[4] = x138; + out[5] = x142; + out[6] = x146; + out[7] = x150; + out[8] = x154; + out[9] = x158; + out[10] = x162; + out[11] = x166; + out[12] = x170; + out[13] = x174; + out[14] = x178; + out[15] = x182; + out[16] = x186; + out[17] = x190; + out[18] = x194; + out[19] = x198; + out[20] = x202; + out[21] = x206; + out[22] = x210; + out[23] = x214; + }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} +} diff --git a/src/Specific/solinas32_2e512m569_24limbs/freezeDisplay.log b/src/Specific/solinas32_2e512m569_24limbs/freezeDisplay.log new file mode 100644 index 000000000..d3f60da16 --- /dev/null +++ b/src/Specific/solinas32_2e512m569_24limbs/freezeDisplay.log @@ -0,0 +1,80 @@ +λ x : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32, +Interp-η +(λ var : Syntax.base_type → Type, + λ '(x45, x46, x44, x42, x40, x38, x36, x34, x32, x30, x28, x26, x24, x22, x20, x18, x16, x14, x12, x10, x8, x6, x4, x2)%core, + uint32_t x48, uint8_t x49 = Op (Syntax.SubWithGetBorrow 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (0x0, Return x2, 0x3ffdc7); + uint32_t x51, uint8_t x52 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x49, Return x4, 0x1fffff); + uint32_t x54, uint8_t x55 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x52, Return x6, 0x1fffff); + uint32_t x57, uint8_t x58 = Op (Syntax.SubWithGetBorrow 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x55, Return x8, 0x3fffff); + uint32_t x60, uint8_t x61 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x58, Return x10, 0x1fffff); + uint32_t x63, uint8_t x64 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x61, Return x12, 0x1fffff); + uint32_t x66, uint8_t x67 = Op (Syntax.SubWithGetBorrow 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x64, Return x14, 0x3fffff); + uint32_t x69, uint8_t x70 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x67, Return x16, 0x1fffff); + uint32_t x72, uint8_t x73 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x70, Return x18, 0x1fffff); + uint32_t x75, uint8_t x76 = Op (Syntax.SubWithGetBorrow 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x73, Return x20, 0x3fffff); + uint32_t x78, uint8_t x79 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x76, Return x22, 0x1fffff); + uint32_t x81, uint8_t x82 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x79, Return x24, 0x1fffff); + uint32_t x84, uint8_t x85 = Op (Syntax.SubWithGetBorrow 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x82, Return x26, 0x3fffff); + uint32_t x87, uint8_t x88 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x85, Return x28, 0x1fffff); + uint32_t x90, uint8_t x91 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x88, Return x30, 0x1fffff); + uint32_t x93, uint8_t x94 = Op (Syntax.SubWithGetBorrow 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x91, Return x32, 0x3fffff); + uint32_t x96, uint8_t x97 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x94, Return x34, 0x1fffff); + uint32_t x99, uint8_t x100 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x97, Return x36, 0x1fffff); + uint32_t x102, uint8_t x103 = Op (Syntax.SubWithGetBorrow 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x100, Return x38, 0x3fffff); + uint32_t x105, uint8_t x106 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x103, Return x40, 0x1fffff); + uint32_t x108, uint8_t x109 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x106, Return x42, 0x1fffff); + uint32_t x111, uint8_t x112 = Op (Syntax.SubWithGetBorrow 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x109, Return x44, 0x3fffff); + uint32_t x114, uint8_t x115 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x112, Return x46, 0x1fffff); + uint32_t x117, uint8_t x118 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x115, Return x45, 0x1fffff); + uint32_t x119 = cmovznz32(x118, 0x0, 0xffffffff); + uint32_t x120 = (x119 & 0x3ffdc7); + uint32_t x122, uint8_t x123 = Op (Syntax.AddWithGetCarry 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (0x0, Return x48, Return x120); + uint32_t x124 = (x119 & 0x1fffff); + uint32_t x126, uint8_t x127 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x123, Return x51, Return x124); + uint32_t x128 = (x119 & 0x1fffff); + uint32_t x130, uint8_t x131 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x127, Return x54, Return x128); + uint32_t x132 = (x119 & 0x3fffff); + uint32_t x134, uint8_t x135 = Op (Syntax.AddWithGetCarry 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x131, Return x57, Return x132); + uint32_t x136 = (x119 & 0x1fffff); + uint32_t x138, uint8_t x139 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x135, Return x60, Return x136); + uint32_t x140 = (x119 & 0x1fffff); + uint32_t x142, uint8_t x143 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x139, Return x63, Return x140); + uint32_t x144 = (x119 & 0x3fffff); + uint32_t x146, uint8_t x147 = Op (Syntax.AddWithGetCarry 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x143, Return x66, Return x144); + uint32_t x148 = (x119 & 0x1fffff); + uint32_t x150, uint8_t x151 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x147, Return x69, Return x148); + uint32_t x152 = (x119 & 0x1fffff); + uint32_t x154, uint8_t x155 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x151, Return x72, Return x152); + uint32_t x156 = (x119 & 0x3fffff); + uint32_t x158, uint8_t x159 = Op (Syntax.AddWithGetCarry 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x155, Return x75, Return x156); + uint32_t x160 = (x119 & 0x1fffff); + uint32_t x162, uint8_t x163 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x159, Return x78, Return x160); + uint32_t x164 = (x119 & 0x1fffff); + uint32_t x166, uint8_t x167 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x163, Return x81, Return x164); + uint32_t x168 = (x119 & 0x3fffff); + uint32_t x170, uint8_t x171 = Op (Syntax.AddWithGetCarry 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x167, Return x84, Return x168); + uint32_t x172 = (x119 & 0x1fffff); + uint32_t x174, uint8_t x175 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x171, Return x87, Return x172); + uint32_t x176 = (x119 & 0x1fffff); + uint32_t x178, uint8_t x179 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x175, Return x90, Return x176); + uint32_t x180 = (x119 & 0x3fffff); + uint32_t x182, uint8_t x183 = Op (Syntax.AddWithGetCarry 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x179, Return x93, Return x180); + uint32_t x184 = (x119 & 0x1fffff); + uint32_t x186, uint8_t x187 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x183, Return x96, Return x184); + uint32_t x188 = (x119 & 0x1fffff); + uint32_t x190, uint8_t x191 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x187, Return x99, Return x188); + uint32_t x192 = (x119 & 0x3fffff); + uint32_t x194, uint8_t x195 = Op (Syntax.AddWithGetCarry 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x191, Return x102, Return x192); + uint32_t x196 = (x119 & 0x1fffff); + uint32_t x198, uint8_t x199 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x195, Return x105, Return x196); + uint32_t x200 = (x119 & 0x1fffff); + uint32_t x202, uint8_t x203 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x199, Return x108, Return x200); + uint32_t x204 = (x119 & 0x3fffff); + uint32_t x206, uint8_t x207 = Op (Syntax.AddWithGetCarry 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x203, Return x111, Return x204); + uint32_t x208 = (x119 & 0x1fffff); + uint32_t x210, uint8_t x211 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x207, Return x114, Return x208); + uint32_t x212 = (x119 & 0x1fffff); + uint32_t x214, uint8_t _ = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x211, Return x117, Return x212); + (Return x214, Return x210, Return x206, Return x202, Return x198, Return x194, Return x190, Return x186, Return x182, Return x178, Return x174, Return x170, Return x166, Return x162, Return x158, Return x154, Return x150, Return x146, Return x142, Return x138, Return x134, Return x130, Return x126, Return x122)) +x + : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t) |