/* Autogenerated: /src/ExtractionOCaml/unsaturated_solinas --static p448 32 18 '2^448 - 2^224 - 1' add sub opp carry carry_mul carry_square carry_scmul3 carry_scmul4 carry_scmul8 carry_scmul39082 carry_scmul39081 selectznz to_bytes from_bytes */ /* curve description: p448 */ /* machine_wordsize = 32 (from "32") */ /* requested operations: add, sub, opp, carry, carry_mul, carry_square, carry_scmul3, carry_scmul4, carry_scmul8, carry_scmul39082, carry_scmul39081, selectznz, to_bytes, from_bytes */ /* n = 18 (from "18") */ /* s-c = 2^448 - [(2^224, 1), (1, 1)] (from "2^448 - 2^224 - 1") */ /* tight_bounds_multiplier = 1 (from "") */ /* */ /* Computed values: */ /* carry_chain = [8, 17, 9, 0, 10, 1, 11, 2, 12, 3, 13, 4, 14, 5, 15, 6, 16, 7, 17, 8, 9, 0] */ /* eval z = z[0] + (z[1] << 25) + (z[2] << 50) + (z[3] << 75) + (z[4] << 100) + (z[5] << 125) + (z[6] << 150) + (z[7] << 175) + (z[8] << 200) + (z[9] << 224) + (z[10] << 249) + (z[11] << 0x112) + (z[12] << 0x12b) + (z[13] << 0x144) + (z[14] << 0x15d) + (z[15] << 0x176) + (z[16] << 0x18f) + (z[17] << 0x1a8) */ /* bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) + (z[32] << 256) + (z[33] << 0x108) + (z[34] << 0x110) + (z[35] << 0x118) + (z[36] << 0x120) + (z[37] << 0x128) + (z[38] << 0x130) + (z[39] << 0x138) + (z[40] << 0x140) + (z[41] << 0x148) + (z[42] << 0x150) + (z[43] << 0x158) + (z[44] << 0x160) + (z[45] << 0x168) + (z[46] << 0x170) + (z[47] << 0x178) + (z[48] << 0x180) + (z[49] << 0x188) + (z[50] << 0x190) + (z[51] << 0x198) + (z[52] << 0x1a0) + (z[53] << 0x1a8) + (z[54] << 0x1b0) + (z[55] << 0x1b8) */ /* balance = [0x3fffffe, 0x3fffffe, 0x3fffffe, 0x3fffffe, 0x3fffffe, 0x3fffffe, 0x3fffffe, 0x3fffffe, 0x1fffffe, 0x3fffffc, 0x3fffffe, 0x3fffffe, 0x3fffffe, 0x3fffffe, 0x3fffffe, 0x3fffffe, 0x3fffffe, 0x1fffffe] */ #include typedef unsigned char fiat_p448_uint1; typedef signed char fiat_p448_int1; #if (-1 & 3) != 3 #error "This code only works on a two's complement system" #endif /* * The function fiat_p448_addcarryx_u24 is an addition with carry. * Postconditions: * out1 = (arg1 + arg2 + arg3) mod 2^24 * out2 = ⌊(arg1 + arg2 + arg3) / 2^24⌋ * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffff] * arg3: [0x0 ~> 0xffffff] * Output Bounds: * out1: [0x0 ~> 0xffffff] * out2: [0x0 ~> 0x1] */ static void fiat_p448_addcarryx_u24(uint32_t* out1, fiat_p448_uint1* out2, fiat_p448_uint1 arg1, uint32_t arg2, uint32_t arg3) { uint32_t x1; uint32_t x2; fiat_p448_uint1 x3; x1 = ((arg1 + arg2) + arg3); x2 = (x1 & UINT32_C(0xffffff)); x3 = (fiat_p448_uint1)(x1 >> 24); *out1 = x2; *out2 = x3; } /* * The function fiat_p448_subborrowx_u24 is a subtraction with borrow. * Postconditions: * out1 = (-arg1 + arg2 + -arg3) mod 2^24 * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^24⌋ * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffff] * arg3: [0x0 ~> 0xffffff] * Output Bounds: * out1: [0x0 ~> 0xffffff] * out2: [0x0 ~> 0x1] */ static void fiat_p448_subborrowx_u24(uint32_t* out1, fiat_p448_uint1* out2, fiat_p448_uint1 arg1, uint32_t arg2, uint32_t arg3) { int32_t x1; fiat_p448_int1 x2; uint32_t x3; x1 = ((int32_t)(arg2 - arg1) - (int32_t)arg3); x2 = (fiat_p448_int1)(x1 >> 24); x3 = (x1 & UINT32_C(0xffffff)); *out1 = x3; *out2 = (fiat_p448_uint1)(0x0 - x2); } /* * The function fiat_p448_addcarryx_u25 is an addition with carry. * Postconditions: * out1 = (arg1 + arg2 + arg3) mod 2^25 * out2 = ⌊(arg1 + arg2 + arg3) / 2^25⌋ * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0x1ffffff] * arg3: [0x0 ~> 0x1ffffff] * Output Bounds: * out1: [0x0 ~> 0x1ffffff] * out2: [0x0 ~> 0x1] */ static void fiat_p448_addcarryx_u25(uint32_t* out1, fiat_p448_uint1* out2, fiat_p448_uint1 arg1, uint32_t arg2, uint32_t arg3) { uint32_t x1; uint32_t x2; fiat_p448_uint1 x3; x1 = ((arg1 + arg2) + arg3); x2 = (x1 & UINT32_C(0x1ffffff)); x3 = (fiat_p448_uint1)(x1 >> 25); *out1 = x2; *out2 = x3; } /* * The function fiat_p448_subborrowx_u25 is a subtraction with borrow. * Postconditions: * out1 = (-arg1 + arg2 + -arg3) mod 2^25 * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^25⌋ * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0x1ffffff] * arg3: [0x0 ~> 0x1ffffff] * Output Bounds: * out1: [0x0 ~> 0x1ffffff] * out2: [0x0 ~> 0x1] */ static void fiat_p448_subborrowx_u25(uint32_t* out1, fiat_p448_uint1* out2, fiat_p448_uint1 arg1, uint32_t arg2, uint32_t arg3) { int32_t x1; fiat_p448_int1 x2; uint32_t x3; x1 = ((int32_t)(arg2 - arg1) - (int32_t)arg3); x2 = (fiat_p448_int1)(x1 >> 25); x3 = (x1 & UINT32_C(0x1ffffff)); *out1 = x3; *out2 = (fiat_p448_uint1)(0x0 - x2); } /* * The function fiat_p448_cmovznz_u32 is a single-word conditional move. * Postconditions: * out1 = (if arg1 = 0 then arg2 else arg3) * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [0x0 ~> 0xffffffff] * arg3: [0x0 ~> 0xffffffff] * Output Bounds: * out1: [0x0 ~> 0xffffffff] */ static void fiat_p448_cmovznz_u32(uint32_t* out1, fiat_p448_uint1 arg1, uint32_t arg2, uint32_t arg3) { fiat_p448_uint1 x1; uint32_t x2; uint32_t x3; x1 = (!(!arg1)); x2 = ((fiat_p448_int1)(0x0 - x1) & UINT32_C(0xffffffff)); x3 = ((fe_word_barrier(x2) & arg3) | (fe_word_barrier(~x2) & arg2)); *out1 = x3; } /* * The function fiat_p448_add adds two field elements. * Postconditions: * eval out1 mod m = (eval arg1 + eval arg2) mod m * * Input Bounds: * arg1: [[0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x1000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x1000000]] * arg2: [[0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x1000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x1000000]] * Output Bounds: * out1: [[0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x3000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x3000000]] */ static void fiat_p448_add(uint32_t out1[18], const uint32_t arg1[18], const uint32_t arg2[18]) { uint32_t x1; uint32_t x2; uint32_t x3; uint32_t x4; uint32_t x5; uint32_t x6; uint32_t x7; uint32_t x8; uint32_t x9; uint32_t x10; uint32_t x11; uint32_t x12; uint32_t x13; uint32_t x14; uint32_t x15; uint32_t x16; uint32_t x17; uint32_t x18; x1 = ((arg1[0]) + (arg2[0])); x2 = ((arg1[1]) + (arg2[1])); x3 = ((arg1[2]) + (arg2[2])); x4 = ((arg1[3]) + (arg2[3])); x5 = ((arg1[4]) + (arg2[4])); x6 = ((arg1[5]) + (arg2[5])); x7 = ((arg1[6]) + (arg2[6])); x8 = ((arg1[7]) + (arg2[7])); x9 = ((arg1[8]) + (arg2[8])); x10 = ((arg1[9]) + (arg2[9])); x11 = ((arg1[10]) + (arg2[10])); x12 = ((arg1[11]) + (arg2[11])); x13 = ((arg1[12]) + (arg2[12])); x14 = ((arg1[13]) + (arg2[13])); x15 = ((arg1[14]) + (arg2[14])); x16 = ((arg1[15]) + (arg2[15])); x17 = ((arg1[16]) + (arg2[16])); x18 = ((arg1[17]) + (arg2[17])); out1[0] = x1; out1[1] = x2; out1[2] = x3; out1[3] = x4; out1[4] = x5; out1[5] = x6; out1[6] = x7; out1[7] = x8; out1[8] = x9; out1[9] = x10; out1[10] = x11; out1[11] = x12; out1[12] = x13; out1[13] = x14; out1[14] = x15; out1[15] = x16; out1[16] = x17; out1[17] = x18; } /* * The function fiat_p448_sub subtracts two field elements. * Postconditions: * eval out1 mod m = (eval arg1 - eval arg2) mod m * * Input Bounds: * arg1: [[0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x1000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x1000000]] * arg2: [[0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x1000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x1000000]] * Output Bounds: * out1: [[0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x3000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x3000000]] */ static void fiat_p448_sub(uint32_t out1[18], const uint32_t arg1[18], const uint32_t arg2[18]) { uint32_t x1; uint32_t x2; uint32_t x3; uint32_t x4; uint32_t x5; uint32_t x6; uint32_t x7; uint32_t x8; uint32_t x9; uint32_t x10; uint32_t x11; uint32_t x12; uint32_t x13; uint32_t x14; uint32_t x15; uint32_t x16; uint32_t x17; uint32_t x18; x1 = ((UINT32_C(0x3fffffe) + (arg1[0])) - (arg2[0])); x2 = ((UINT32_C(0x3fffffe) + (arg1[1])) - (arg2[1])); x3 = ((UINT32_C(0x3fffffe) + (arg1[2])) - (arg2[2])); x4 = ((UINT32_C(0x3fffffe) + (arg1[3])) - (arg2[3])); x5 = ((UINT32_C(0x3fffffe) + (arg1[4])) - (arg2[4])); x6 = ((UINT32_C(0x3fffffe) + (arg1[5])) - (arg2[5])); x7 = ((UINT32_C(0x3fffffe) + (arg1[6])) - (arg2[6])); x8 = ((UINT32_C(0x3fffffe) + (arg1[7])) - (arg2[7])); x9 = ((UINT32_C(0x1fffffe) + (arg1[8])) - (arg2[8])); x10 = ((UINT32_C(0x3fffffc) + (arg1[9])) - (arg2[9])); x11 = ((UINT32_C(0x3fffffe) + (arg1[10])) - (arg2[10])); x12 = ((UINT32_C(0x3fffffe) + (arg1[11])) - (arg2[11])); x13 = ((UINT32_C(0x3fffffe) + (arg1[12])) - (arg2[12])); x14 = ((UINT32_C(0x3fffffe) + (arg1[13])) - (arg2[13])); x15 = ((UINT32_C(0x3fffffe) + (arg1[14])) - (arg2[14])); x16 = ((UINT32_C(0x3fffffe) + (arg1[15])) - (arg2[15])); x17 = ((UINT32_C(0x3fffffe) + (arg1[16])) - (arg2[16])); x18 = ((UINT32_C(0x1fffffe) + (arg1[17])) - (arg2[17])); out1[0] = x1; out1[1] = x2; out1[2] = x3; out1[3] = x4; out1[4] = x5; out1[5] = x6; out1[6] = x7; out1[7] = x8; out1[8] = x9; out1[9] = x10; out1[10] = x11; out1[11] = x12; out1[12] = x13; out1[13] = x14; out1[14] = x15; out1[15] = x16; out1[16] = x17; out1[17] = x18; } /* * The function fiat_p448_opp negates a field element. * Postconditions: * eval out1 mod m = -eval arg1 mod m * * Input Bounds: * arg1: [[0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x1000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x1000000]] * Output Bounds: * out1: [[0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x3000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x3000000]] */ static void fiat_p448_opp(uint32_t out1[18], const uint32_t arg1[18]) { uint32_t x1; uint32_t x2; uint32_t x3; uint32_t x4; uint32_t x5; uint32_t x6; uint32_t x7; uint32_t x8; uint32_t x9; uint32_t x10; uint32_t x11; uint32_t x12; uint32_t x13; uint32_t x14; uint32_t x15; uint32_t x16; uint32_t x17; uint32_t x18; x1 = (UINT32_C(0x3fffffe) - (arg1[0])); x2 = (UINT32_C(0x3fffffe) - (arg1[1])); x3 = (UINT32_C(0x3fffffe) - (arg1[2])); x4 = (UINT32_C(0x3fffffe) - (arg1[3])); x5 = (UINT32_C(0x3fffffe) - (arg1[4])); x6 = (UINT32_C(0x3fffffe) - (arg1[5])); x7 = (UINT32_C(0x3fffffe) - (arg1[6])); x8 = (UINT32_C(0x3fffffe) - (arg1[7])); x9 = (UINT32_C(0x1fffffe) - (arg1[8])); x10 = (UINT32_C(0x3fffffc) - (arg1[9])); x11 = (UINT32_C(0x3fffffe) - (arg1[10])); x12 = (UINT32_C(0x3fffffe) - (arg1[11])); x13 = (UINT32_C(0x3fffffe) - (arg1[12])); x14 = (UINT32_C(0x3fffffe) - (arg1[13])); x15 = (UINT32_C(0x3fffffe) - (arg1[14])); x16 = (UINT32_C(0x3fffffe) - (arg1[15])); x17 = (UINT32_C(0x3fffffe) - (arg1[16])); x18 = (UINT32_C(0x1fffffe) - (arg1[17])); out1[0] = x1; out1[1] = x2; out1[2] = x3; out1[3] = x4; out1[4] = x5; out1[5] = x6; out1[6] = x7; out1[7] = x8; out1[8] = x9; out1[9] = x10; out1[10] = x11; out1[11] = x12; out1[12] = x13; out1[13] = x14; out1[14] = x15; out1[15] = x16; out1[16] = x17; out1[17] = x18; } /* * The function fiat_p448_carry reduces a field element. * Postconditions: * eval out1 mod m = eval arg1 mod m * * Input Bounds: * arg1: [[0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x3000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x3000000]] * Output Bounds: * out1: [[0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x1000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x1000000]] */ static void fiat_p448_carry(uint32_t out1[18], const uint32_t arg1[18]) { uint32_t x1; uint32_t x2; uint32_t x3; uint32_t x4; uint32_t x5; uint32_t x6; uint32_t x7; uint32_t x8; uint32_t x9; uint32_t x10; uint32_t x11; uint32_t x12; uint32_t x13; uint32_t x14; uint32_t x15; uint32_t x16; uint32_t x17; uint32_t x18; uint32_t x19; uint32_t x20; uint32_t x21; fiat_p448_uint1 x22; uint32_t x23; uint32_t x24; uint32_t x25; uint32_t x26; uint32_t x27; uint32_t x28; uint32_t x29; uint32_t x30; uint32_t x31; uint32_t x32; uint32_t x33; uint32_t x34; uint32_t x35; uint32_t x36; uint32_t x37; uint32_t x38; uint32_t x39; uint32_t x40; uint32_t x41; uint32_t x42; x1 = (arg1[8]); x2 = (arg1[17]); x3 = (x2 >> 24); x4 = (((x1 >> 24) + (arg1[9])) + x3); x5 = ((arg1[0]) + x3); x6 = ((x4 >> 25) + (arg1[10])); x7 = ((x5 >> 25) + (arg1[1])); x8 = ((x6 >> 25) + (arg1[11])); x9 = ((x7 >> 25) + (arg1[2])); x10 = ((x8 >> 25) + (arg1[12])); x11 = ((x9 >> 25) + (arg1[3])); x12 = ((x10 >> 25) + (arg1[13])); x13 = ((x11 >> 25) + (arg1[4])); x14 = ((x12 >> 25) + (arg1[14])); x15 = ((x13 >> 25) + (arg1[5])); x16 = ((x14 >> 25) + (arg1[15])); x17 = ((x15 >> 25) + (arg1[6])); x18 = ((x16 >> 25) + (arg1[16])); x19 = ((x17 >> 25) + (arg1[7])); x20 = ((x18 >> 25) + (x2 & UINT32_C(0xffffff))); x21 = ((x19 >> 25) + (x1 & UINT32_C(0xffffff))); x22 = (fiat_p448_uint1)(x20 >> 24); x23 = ((x5 & UINT32_C(0x1ffffff)) + (uint32_t)x22); x24 = ((fiat_p448_uint1)(x21 >> 24) + ((x4 & UINT32_C(0x1ffffff)) + (uint32_t)x22)); x25 = (x23 & UINT32_C(0x1ffffff)); x26 = ((fiat_p448_uint1)(x23 >> 25) + (x7 & UINT32_C(0x1ffffff))); x27 = (x9 & UINT32_C(0x1ffffff)); x28 = (x11 & UINT32_C(0x1ffffff)); x29 = (x13 & UINT32_C(0x1ffffff)); x30 = (x15 & UINT32_C(0x1ffffff)); x31 = (x17 & UINT32_C(0x1ffffff)); x32 = (x19 & UINT32_C(0x1ffffff)); x33 = (x21 & UINT32_C(0xffffff)); x34 = (x24 & UINT32_C(0x1ffffff)); x35 = ((fiat_p448_uint1)(x24 >> 25) + (x6 & UINT32_C(0x1ffffff))); x36 = (x8 & UINT32_C(0x1ffffff)); x37 = (x10 & UINT32_C(0x1ffffff)); x38 = (x12 & UINT32_C(0x1ffffff)); x39 = (x14 & UINT32_C(0x1ffffff)); x40 = (x16 & UINT32_C(0x1ffffff)); x41 = (x18 & UINT32_C(0x1ffffff)); x42 = (x20 & UINT32_C(0xffffff)); out1[0] = x25; out1[1] = x26; out1[2] = x27; out1[3] = x28; out1[4] = x29; out1[5] = x30; out1[6] = x31; out1[7] = x32; out1[8] = x33; out1[9] = x34; out1[10] = x35; out1[11] = x36; out1[12] = x37; out1[13] = x38; out1[14] = x39; out1[15] = x40; out1[16] = x41; out1[17] = x42; } /* * The function fiat_p448_carry_mul multiplies two field elements and reduces the result. * Postconditions: * eval out1 mod m = (eval arg1 * eval arg2) mod m * * Input Bounds: * arg1: [[0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x3000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x3000000]] * arg2: [[0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x3000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x3000000]] * Output Bounds: * out1: [[0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x1000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x1000000]] */ static void fiat_p448_carry_mul(uint32_t out1[18], const uint32_t arg1[18], const uint32_t arg2[18]) { uint64_t x1; uint64_t x2; uint64_t x3; uint64_t x4; uint64_t x5; uint64_t x6; uint64_t x7; uint64_t x8; uint64_t x9; uint64_t x10; uint64_t x11; uint64_t x12; uint64_t x13; uint64_t x14; uint64_t x15; uint64_t x16; uint64_t x17; uint64_t x18; uint64_t x19; uint64_t x20; uint64_t x21; uint64_t x22; uint64_t x23; uint64_t x24; uint64_t x25; uint64_t x26; uint64_t x27; uint64_t x28; uint64_t x29; uint64_t x30; uint64_t x31; uint64_t x32; uint64_t x33; uint64_t x34; uint64_t x35; uint64_t x36; uint64_t x37; uint64_t x38; uint64_t x39; uint64_t x40; uint64_t x41; uint64_t x42; uint64_t x43; uint64_t x44; uint64_t x45; uint64_t x46; uint64_t x47; uint64_t x48; uint64_t x49; uint64_t x50; uint64_t x51; uint64_t x52; uint64_t x53; uint64_t x54; uint64_t x55; uint64_t x56; uint64_t x57; uint64_t x58; uint64_t x59; uint64_t x60; uint64_t x61; uint64_t x62; uint64_t x63; uint64_t x64; uint64_t x65; uint64_t x66; uint64_t x67; uint64_t x68; uint64_t x69; uint64_t x70; uint64_t x71; uint64_t x72; uint64_t x73; uint64_t x74; uint64_t x75; uint64_t x76; uint64_t x77; uint64_t x78; uint64_t x79; uint64_t x80; uint64_t x81; uint64_t x82; uint64_t x83; uint64_t x84; uint64_t x85; uint64_t x86; uint64_t x87; uint64_t x88; uint64_t x89; uint64_t x90; uint64_t x91; uint64_t x92; uint64_t x93; uint64_t x94; uint64_t x95; uint64_t x96; uint64_t x97; uint64_t x98; uint64_t x99; uint64_t x100; uint64_t x101; uint64_t x102; uint64_t x103; uint64_t x104; uint64_t x105; uint64_t x106; uint64_t x107; uint64_t x108; uint64_t x109; uint64_t x110; uint64_t x111; uint64_t x112; uint64_t x113; uint64_t x114; uint64_t x115; uint64_t x116; uint64_t x117; uint64_t x118; uint64_t x119; uint64_t x120; uint64_t x121; uint64_t x122; uint64_t x123; uint64_t x124; uint64_t x125; uint64_t x126; uint64_t x127; uint64_t x128; uint64_t x129; uint64_t x130; uint64_t x131; uint64_t x132; uint64_t x133; uint64_t x134; uint64_t x135; uint64_t x136; uint64_t x137; uint64_t x138; uint64_t x139; uint64_t x140; uint64_t x141; uint64_t x142; uint64_t x143; uint64_t x144; uint64_t x145; uint64_t x146; uint64_t x147; uint64_t x148; uint64_t x149; uint64_t x150; uint64_t x151; uint64_t x152; uint64_t x153; uint64_t x154; uint64_t x155; uint64_t x156; uint64_t x157; uint64_t x158; uint64_t x159; uint64_t x160; uint64_t x161; uint64_t x162; uint64_t x163; uint64_t x164; uint64_t x165; uint64_t x166; uint64_t x167; uint64_t x168; uint64_t x169; uint64_t x170; uint64_t x171; uint64_t x172; uint64_t x173; uint64_t x174; uint64_t x175; uint64_t x176; uint64_t x177; uint64_t x178; uint64_t x179; uint64_t x180; uint64_t x181; uint64_t x182; uint64_t x183; uint64_t x184; uint64_t x185; uint64_t x186; uint64_t x187; uint64_t x188; uint64_t x189; uint64_t x190; uint64_t x191; uint64_t x192; uint64_t x193; uint64_t x194; uint64_t x195; uint64_t x196; uint64_t x197; uint64_t x198; uint64_t x199; uint64_t x200; uint64_t x201; uint64_t x202; uint64_t x203; uint64_t x204; uint64_t x205; uint64_t x206; uint64_t x207; uint64_t x208; uint64_t x209; uint64_t x210; uint64_t x211; uint64_t x212; uint64_t x213; uint64_t x214; uint64_t x215; uint64_t x216; uint64_t x217; uint64_t x218; uint64_t x219; uint64_t x220; uint64_t x221; uint64_t x222; uint64_t x223; uint64_t x224; uint64_t x225; uint64_t x226; uint64_t x227; uint64_t x228; uint64_t x229; uint64_t x230; uint64_t x231; uint64_t x232; uint64_t x233; uint64_t x234; uint64_t x235; uint64_t x236; uint64_t x237; uint64_t x238; uint64_t x239; uint64_t x240; uint64_t x241; uint64_t x242; uint64_t x243; uint64_t x244; uint64_t x245; uint64_t x246; uint64_t x247; uint64_t x248; uint64_t x249; uint64_t x250; uint64_t x251; uint64_t x252; uint64_t x253; uint64_t x254; uint64_t x255; uint64_t x256; uint64_t x257; uint64_t x258; uint64_t x259; uint64_t x260; uint64_t x261; uint64_t x262; uint64_t x263; uint64_t x264; uint64_t x265; uint64_t x266; uint64_t x267; uint64_t x268; uint64_t x269; uint64_t x270; uint64_t x271; uint64_t x272; uint64_t x273; uint64_t x274; uint64_t x275; uint64_t x276; uint64_t x277; uint64_t x278; uint64_t x279; uint64_t x280; uint64_t x281; uint64_t x282; uint64_t x283; uint64_t x284; uint64_t x285; uint64_t x286; uint64_t x287; uint64_t x288; uint64_t x289; uint64_t x290; uint64_t x291; uint64_t x292; uint64_t x293; uint64_t x294; uint64_t x295; uint64_t x296; uint64_t x297; uint64_t x298; uint64_t x299; uint64_t x300; uint64_t x301; uint64_t x302; uint64_t x303; uint64_t x304; uint64_t x305; uint64_t x306; uint64_t x307; uint64_t x308; uint64_t x309; uint64_t x310; uint64_t x311; uint64_t x312; uint64_t x313; uint64_t x314; uint64_t x315; uint64_t x316; uint64_t x317; uint64_t x318; uint64_t x319; uint64_t x320; uint64_t x321; uint64_t x322; uint64_t x323; uint64_t x324; uint64_t x325; uint64_t x326; uint64_t x327; uint64_t x328; uint64_t x329; uint64_t x330; uint64_t x331; uint64_t x332; uint64_t x333; uint64_t x334; uint64_t x335; uint64_t x336; uint64_t x337; uint64_t x338; uint64_t x339; uint64_t x340; uint64_t x341; uint64_t x342; uint64_t x343; uint64_t x344; uint64_t x345; uint64_t x346; uint64_t x347; uint64_t x348; uint64_t x349; uint64_t x350; uint64_t x351; uint64_t x352; uint64_t x353; uint64_t x354; uint64_t x355; uint64_t x356; uint64_t x357; uint64_t x358; uint64_t x359; uint64_t x360; uint64_t x361; uint64_t x362; uint64_t x363; uint64_t x364; uint64_t x365; uint64_t x366; uint64_t x367; uint64_t x368; uint64_t x369; uint64_t x370; uint64_t x371; uint64_t x372; uint64_t x373; uint64_t x374; uint64_t x375; uint64_t x376; uint64_t x377; uint64_t x378; uint64_t x379; uint64_t x380; uint64_t x381; uint64_t x382; uint64_t x383; uint64_t x384; uint64_t x385; uint64_t x386; uint64_t x387; uint64_t x388; uint64_t x389; uint64_t x390; uint64_t x391; uint64_t x392; uint64_t x393; uint64_t x394; uint64_t x395; uint64_t x396; uint64_t x397; uint64_t x398; uint64_t x399; uint64_t x400; uint64_t x401; uint64_t x402; uint64_t x403; uint64_t x404; uint64_t x405; uint64_t x406; uint64_t x407; uint64_t x408; uint64_t x409; uint64_t x410; uint64_t x411; uint64_t x412; uint64_t x413; uint64_t x414; uint64_t x415; uint64_t x416; uint64_t x417; uint64_t x418; uint64_t x419; uint64_t x420; uint64_t x421; uint64_t x422; uint64_t x423; uint64_t x424; uint64_t x425; uint64_t x426; uint64_t x427; uint64_t x428; uint64_t x429; uint64_t x430; uint64_t x431; uint64_t x432; uint64_t x433; uint64_t x434; uint64_t x435; uint64_t x436; uint64_t x437; uint64_t x438; uint64_t x439; uint64_t x440; uint64_t x441; uint64_t x442; uint64_t x443; uint64_t x444; uint64_t x445; uint64_t x446; uint64_t x447; uint64_t x448; uint64_t x449; uint64_t x450; uint64_t x451; uint64_t x452; uint64_t x453; uint64_t x454; uint64_t x455; uint64_t x456; uint64_t x457; uint64_t x458; uint64_t x459; uint64_t x460; uint64_t x461; uint64_t x462; uint64_t x463; uint64_t x464; uint64_t x465; uint64_t x466; uint64_t x467; uint64_t x468; uint64_t x469; uint64_t x470; uint64_t x471; uint64_t x472; uint64_t x473; uint64_t x474; uint64_t x475; uint64_t x476; uint64_t x477; uint64_t x478; uint64_t x479; uint64_t x480; uint64_t x481; uint64_t x482; uint64_t x483; uint64_t x484; uint64_t x485; uint64_t x486; uint64_t x487; uint64_t x488; uint64_t x489; uint64_t x490; uint64_t x491; uint64_t x492; uint64_t x493; uint64_t x494; uint64_t x495; uint64_t x496; uint64_t x497; uint64_t x498; uint64_t x499; uint64_t x500; uint64_t x501; uint64_t x502; uint64_t x503; uint64_t x504; uint64_t x505; uint64_t x506; uint64_t x507; uint64_t x508; uint64_t x509; uint64_t x510; uint64_t x511; uint64_t x512; uint64_t x513; uint64_t x514; uint64_t x515; uint32_t x516; uint64_t x517; uint64_t x518; uint64_t x519; uint64_t x520; uint64_t x521; uint64_t x522; uint64_t x523; uint64_t x524; uint64_t x525; uint64_t x526; uint64_t x527; uint64_t x528; uint64_t x529; uint64_t x530; uint64_t x531; uint64_t x532; uint64_t x533; uint64_t x534; uint64_t x535; uint32_t x536; uint64_t x537; uint64_t x538; uint32_t x539; uint64_t x540; uint64_t x541; uint64_t x542; uint32_t x543; uint64_t x544; uint64_t x545; uint32_t x546; uint64_t x547; uint64_t x548; uint32_t x549; uint64_t x550; uint64_t x551; uint32_t x552; uint64_t x553; uint64_t x554; uint32_t x555; uint64_t x556; uint64_t x557; uint32_t x558; uint64_t x559; uint64_t x560; uint32_t x561; uint64_t x562; uint64_t x563; uint32_t x564; uint64_t x565; uint64_t x566; uint32_t x567; uint64_t x568; uint64_t x569; uint32_t x570; uint64_t x571; uint64_t x572; uint32_t x573; uint64_t x574; uint64_t x575; uint32_t x576; uint64_t x577; uint64_t x578; uint32_t x579; uint64_t x580; uint64_t x581; uint32_t x582; uint64_t x583; uint64_t x584; uint32_t x585; uint64_t x586; uint32_t x587; uint32_t x588; uint32_t x589; uint32_t x590; uint32_t x591; uint32_t x592; uint32_t x593; fiat_p448_uint1 x594; uint32_t x595; uint32_t x596; fiat_p448_uint1 x597; uint32_t x598; uint32_t x599; x1 = ((uint64_t)(arg1[17]) * ((arg2[17]) * 0x2)); x2 = ((uint64_t)(arg1[17]) * ((arg2[16]) * 0x2)); x3 = ((uint64_t)(arg1[17]) * ((arg2[15]) * 0x2)); x4 = ((uint64_t)(arg1[17]) * ((arg2[14]) * 0x2)); x5 = ((uint64_t)(arg1[17]) * ((arg2[13]) * 0x2)); x6 = ((uint64_t)(arg1[17]) * ((arg2[12]) * 0x2)); x7 = ((uint64_t)(arg1[17]) * ((arg2[11]) * 0x2)); x8 = ((uint64_t)(arg1[17]) * ((arg2[10]) * 0x2)); x9 = ((uint64_t)(arg1[16]) * ((arg2[17]) * 0x2)); x10 = ((uint64_t)(arg1[16]) * ((arg2[16]) * 0x2)); x11 = ((uint64_t)(arg1[16]) * ((arg2[15]) * 0x2)); x12 = ((uint64_t)(arg1[16]) * ((arg2[14]) * 0x2)); x13 = ((uint64_t)(arg1[16]) * ((arg2[13]) * 0x2)); x14 = ((uint64_t)(arg1[16]) * ((arg2[12]) * 0x2)); x15 = ((uint64_t)(arg1[16]) * ((arg2[11]) * 0x2)); x16 = ((uint64_t)(arg1[15]) * ((arg2[17]) * 0x2)); x17 = ((uint64_t)(arg1[15]) * ((arg2[16]) * 0x2)); x18 = ((uint64_t)(arg1[15]) * ((arg2[15]) * 0x2)); x19 = ((uint64_t)(arg1[15]) * ((arg2[14]) * 0x2)); x20 = ((uint64_t)(arg1[15]) * ((arg2[13]) * 0x2)); x21 = ((uint64_t)(arg1[15]) * ((arg2[12]) * 0x2)); x22 = ((uint64_t)(arg1[14]) * ((arg2[17]) * 0x2)); x23 = ((uint64_t)(arg1[14]) * ((arg2[16]) * 0x2)); x24 = ((uint64_t)(arg1[14]) * ((arg2[15]) * 0x2)); x25 = ((uint64_t)(arg1[14]) * ((arg2[14]) * 0x2)); x26 = ((uint64_t)(arg1[14]) * ((arg2[13]) * 0x2)); x27 = ((uint64_t)(arg1[13]) * ((arg2[17]) * 0x2)); x28 = ((uint64_t)(arg1[13]) * ((arg2[16]) * 0x2)); x29 = ((uint64_t)(arg1[13]) * ((arg2[15]) * 0x2)); x30 = ((uint64_t)(arg1[13]) * ((arg2[14]) * 0x2)); x31 = ((uint64_t)(arg1[12]) * ((arg2[17]) * 0x2)); x32 = ((uint64_t)(arg1[12]) * ((arg2[16]) * 0x2)); x33 = ((uint64_t)(arg1[12]) * ((arg2[15]) * 0x2)); x34 = ((uint64_t)(arg1[11]) * ((arg2[17]) * 0x2)); x35 = ((uint64_t)(arg1[11]) * ((arg2[16]) * 0x2)); x36 = ((uint64_t)(arg1[10]) * ((arg2[17]) * 0x2)); x37 = ((uint64_t)(arg1[17]) * ((arg2[17]) * 0x2)); x38 = ((uint64_t)(arg1[17]) * ((arg2[16]) * 0x2)); x39 = ((uint64_t)(arg1[17]) * ((arg2[15]) * 0x2)); x40 = ((uint64_t)(arg1[17]) * ((arg2[14]) * 0x2)); x41 = ((uint64_t)(arg1[17]) * ((arg2[13]) * 0x2)); x42 = ((uint64_t)(arg1[17]) * ((arg2[12]) * 0x2)); x43 = ((uint64_t)(arg1[17]) * ((arg2[11]) * 0x2)); x44 = ((uint64_t)(arg1[17]) * ((arg2[10]) * 0x2)); x45 = ((uint64_t)(arg1[16]) * ((arg2[17]) * 0x2)); x46 = ((uint64_t)(arg1[16]) * ((arg2[16]) * 0x2)); x47 = ((uint64_t)(arg1[16]) * ((arg2[15]) * 0x2)); x48 = ((uint64_t)(arg1[16]) * ((arg2[14]) * 0x2)); x49 = ((uint64_t)(arg1[16]) * ((arg2[13]) * 0x2)); x50 = ((uint64_t)(arg1[16]) * ((arg2[12]) * 0x2)); x51 = ((uint64_t)(arg1[16]) * ((arg2[11]) * 0x2)); x52 = ((uint64_t)(arg1[15]) * ((arg2[17]) * 0x2)); x53 = ((uint64_t)(arg1[15]) * ((arg2[16]) * 0x2)); x54 = ((uint64_t)(arg1[15]) * ((arg2[15]) * 0x2)); x55 = ((uint64_t)(arg1[15]) * ((arg2[14]) * 0x2)); x56 = ((uint64_t)(arg1[15]) * ((arg2[13]) * 0x2)); x57 = ((uint64_t)(arg1[15]) * ((arg2[12]) * 0x2)); x58 = ((uint64_t)(arg1[14]) * ((arg2[17]) * 0x2)); x59 = ((uint64_t)(arg1[14]) * ((arg2[16]) * 0x2)); x60 = ((uint64_t)(arg1[14]) * ((arg2[15]) * 0x2)); x61 = ((uint64_t)(arg1[14]) * ((arg2[14]) * 0x2)); x62 = ((uint64_t)(arg1[14]) * ((arg2[13]) * 0x2)); x63 = ((uint64_t)(arg1[13]) * ((arg2[17]) * 0x2)); x64 = ((uint64_t)(arg1[13]) * ((arg2[16]) * 0x2)); x65 = ((uint64_t)(arg1[13]) * ((arg2[15]) * 0x2)); x66 = ((uint64_t)(arg1[13]) * ((arg2[14]) * 0x2)); x67 = ((uint64_t)(arg1[12]) * ((arg2[17]) * 0x2)); x68 = ((uint64_t)(arg1[12]) * ((arg2[16]) * 0x2)); x69 = ((uint64_t)(arg1[12]) * ((arg2[15]) * 0x2)); x70 = ((uint64_t)(arg1[11]) * ((arg2[17]) * 0x2)); x71 = ((uint64_t)(arg1[11]) * ((arg2[16]) * 0x2)); x72 = ((uint64_t)(arg1[10]) * ((arg2[17]) * 0x2)); x73 = ((uint64_t)(arg1[17]) * ((arg2[17]) * 0x2)); x74 = ((uint64_t)(arg1[17]) * ((arg2[16]) * 0x2)); x75 = ((uint64_t)(arg1[17]) * ((arg2[15]) * 0x2)); x76 = ((uint64_t)(arg1[17]) * ((arg2[14]) * 0x2)); x77 = ((uint64_t)(arg1[17]) * ((arg2[13]) * 0x2)); x78 = ((uint64_t)(arg1[17]) * ((arg2[12]) * 0x2)); x79 = ((uint64_t)(arg1[17]) * ((arg2[11]) * 0x2)); x80 = ((uint64_t)(arg1[17]) * ((arg2[10]) * 0x2)); x81 = ((uint64_t)(arg1[17]) * (arg2[9])); x82 = ((uint64_t)(arg1[17]) * ((arg2[8]) * 0x2)); x83 = ((uint64_t)(arg1[17]) * ((arg2[7]) * 0x2)); x84 = ((uint64_t)(arg1[17]) * ((arg2[6]) * 0x2)); x85 = ((uint64_t)(arg1[17]) * ((arg2[5]) * 0x2)); x86 = ((uint64_t)(arg1[17]) * ((arg2[4]) * 0x2)); x87 = ((uint64_t)(arg1[17]) * ((arg2[3]) * 0x2)); x88 = ((uint64_t)(arg1[17]) * ((arg2[2]) * 0x2)); x89 = ((uint64_t)(arg1[17]) * ((arg2[1]) * 0x2)); x90 = ((uint64_t)(arg1[16]) * ((arg2[17]) * 0x2)); x91 = ((uint64_t)(arg1[16]) * ((arg2[16]) * 0x2)); x92 = ((uint64_t)(arg1[16]) * ((arg2[15]) * 0x2)); x93 = ((uint64_t)(arg1[16]) * ((arg2[14]) * 0x2)); x94 = ((uint64_t)(arg1[16]) * ((arg2[13]) * 0x2)); x95 = ((uint64_t)(arg1[16]) * ((arg2[12]) * 0x2)); x96 = ((uint64_t)(arg1[16]) * ((arg2[11]) * 0x2)); x97 = ((uint64_t)(arg1[16]) * (arg2[10])); x98 = ((uint64_t)(arg1[16]) * (arg2[9])); x99 = ((uint64_t)(arg1[16]) * ((arg2[8]) * 0x2)); x100 = ((uint64_t)(arg1[16]) * ((arg2[7]) * 0x2)); x101 = ((uint64_t)(arg1[16]) * ((arg2[6]) * 0x2)); x102 = ((uint64_t)(arg1[16]) * ((arg2[5]) * 0x2)); x103 = ((uint64_t)(arg1[16]) * ((arg2[4]) * 0x2)); x104 = ((uint64_t)(arg1[16]) * ((arg2[3]) * 0x2)); x105 = ((uint64_t)(arg1[16]) * ((arg2[2]) * 0x2)); x106 = ((uint64_t)(arg1[15]) * ((arg2[17]) * 0x2)); x107 = ((uint64_t)(arg1[15]) * ((arg2[16]) * 0x2)); x108 = ((uint64_t)(arg1[15]) * ((arg2[15]) * 0x2)); x109 = ((uint64_t)(arg1[15]) * ((arg2[14]) * 0x2)); x110 = ((uint64_t)(arg1[15]) * ((arg2[13]) * 0x2)); x111 = ((uint64_t)(arg1[15]) * ((arg2[12]) * 0x2)); x112 = ((uint64_t)(arg1[15]) * (arg2[11])); x113 = ((uint64_t)(arg1[15]) * (arg2[10])); x114 = ((uint64_t)(arg1[15]) * (arg2[9])); x115 = ((uint64_t)(arg1[15]) * ((arg2[8]) * 0x2)); x116 = ((uint64_t)(arg1[15]) * ((arg2[7]) * 0x2)); x117 = ((uint64_t)(arg1[15]) * ((arg2[6]) * 0x2)); x118 = ((uint64_t)(arg1[15]) * ((arg2[5]) * 0x2)); x119 = ((uint64_t)(arg1[15]) * ((arg2[4]) * 0x2)); x120 = ((uint64_t)(arg1[15]) * ((arg2[3]) * 0x2)); x121 = ((uint64_t)(arg1[14]) * ((arg2[17]) * 0x2)); x122 = ((uint64_t)(arg1[14]) * ((arg2[16]) * 0x2)); x123 = ((uint64_t)(arg1[14]) * ((arg2[15]) * 0x2)); x124 = ((uint64_t)(arg1[14]) * ((arg2[14]) * 0x2)); x125 = ((uint64_t)(arg1[14]) * ((arg2[13]) * 0x2)); x126 = ((uint64_t)(arg1[14]) * (arg2[12])); x127 = ((uint64_t)(arg1[14]) * (arg2[11])); x128 = ((uint64_t)(arg1[14]) * (arg2[10])); x129 = ((uint64_t)(arg1[14]) * (arg2[9])); x130 = ((uint64_t)(arg1[14]) * ((arg2[8]) * 0x2)); x131 = ((uint64_t)(arg1[14]) * ((arg2[7]) * 0x2)); x132 = ((uint64_t)(arg1[14]) * ((arg2[6]) * 0x2)); x133 = ((uint64_t)(arg1[14]) * ((arg2[5]) * 0x2)); x134 = ((uint64_t)(arg1[14]) * ((arg2[4]) * 0x2)); x135 = ((uint64_t)(arg1[13]) * ((arg2[17]) * 0x2)); x136 = ((uint64_t)(arg1[13]) * ((arg2[16]) * 0x2)); x137 = ((uint64_t)(arg1[13]) * ((arg2[15]) * 0x2)); x138 = ((uint64_t)(arg1[13]) * ((arg2[14]) * 0x2)); x139 = ((uint64_t)(arg1[13]) * (arg2[13])); x140 = ((uint64_t)(arg1[13]) * (arg2[12])); x141 = ((uint64_t)(arg1[13]) * (arg2[11])); x142 = ((uint64_t)(arg1[13]) * (arg2[10])); x143 = ((uint64_t)(arg1[13]) * (arg2[9])); x144 = ((uint64_t)(arg1[13]) * ((arg2[8]) * 0x2)); x145 = ((uint64_t)(arg1[13]) * ((arg2[7]) * 0x2)); x146 = ((uint64_t)(arg1[13]) * ((arg2[6]) * 0x2)); x147 = ((uint64_t)(arg1[13]) * ((arg2[5]) * 0x2)); x148 = ((uint64_t)(arg1[12]) * ((arg2[17]) * 0x2)); x149 = ((uint64_t)(arg1[12]) * ((arg2[16]) * 0x2)); x150 = ((uint64_t)(arg1[12]) * ((arg2[15]) * 0x2)); x151 = ((uint64_t)(arg1[12]) * (arg2[14])); x152 = ((uint64_t)(arg1[12]) * (arg2[13])); x153 = ((uint64_t)(arg1[12]) * (arg2[12])); x154 = ((uint64_t)(arg1[12]) * (arg2[11])); x155 = ((uint64_t)(arg1[12]) * (arg2[10])); x156 = ((uint64_t)(arg1[12]) * (arg2[9])); x157 = ((uint64_t)(arg1[12]) * ((arg2[8]) * 0x2)); x158 = ((uint64_t)(arg1[12]) * ((arg2[7]) * 0x2)); x159 = ((uint64_t)(arg1[12]) * ((arg2[6]) * 0x2)); x160 = ((uint64_t)(arg1[11]) * ((arg2[17]) * 0x2)); x161 = ((uint64_t)(arg1[11]) * ((arg2[16]) * 0x2)); x162 = ((uint64_t)(arg1[11]) * (arg2[15])); x163 = ((uint64_t)(arg1[11]) * (arg2[14])); x164 = ((uint64_t)(arg1[11]) * (arg2[13])); x165 = ((uint64_t)(arg1[11]) * (arg2[12])); x166 = ((uint64_t)(arg1[11]) * (arg2[11])); x167 = ((uint64_t)(arg1[11]) * (arg2[10])); x168 = ((uint64_t)(arg1[11]) * (arg2[9])); x169 = ((uint64_t)(arg1[11]) * ((arg2[8]) * 0x2)); x170 = ((uint64_t)(arg1[11]) * ((arg2[7]) * 0x2)); x171 = ((uint64_t)(arg1[10]) * ((arg2[17]) * 0x2)); x172 = ((uint64_t)(arg1[10]) * (arg2[16])); x173 = ((uint64_t)(arg1[10]) * (arg2[15])); x174 = ((uint64_t)(arg1[10]) * (arg2[14])); x175 = ((uint64_t)(arg1[10]) * (arg2[13])); x176 = ((uint64_t)(arg1[10]) * (arg2[12])); x177 = ((uint64_t)(arg1[10]) * (arg2[11])); x178 = ((uint64_t)(arg1[10]) * (arg2[10])); x179 = ((uint64_t)(arg1[10]) * (arg2[9])); x180 = ((uint64_t)(arg1[10]) * ((arg2[8]) * 0x2)); x181 = ((uint64_t)(arg1[9]) * (arg2[17])); x182 = ((uint64_t)(arg1[9]) * (arg2[16])); x183 = ((uint64_t)(arg1[9]) * (arg2[15])); x184 = ((uint64_t)(arg1[9]) * (arg2[14])); x185 = ((uint64_t)(arg1[9]) * (arg2[13])); x186 = ((uint64_t)(arg1[9]) * (arg2[12])); x187 = ((uint64_t)(arg1[9]) * (arg2[11])); x188 = ((uint64_t)(arg1[9]) * (arg2[10])); x189 = ((uint64_t)(arg1[9]) * (arg2[9])); x190 = ((uint64_t)(arg1[8]) * ((arg2[17]) * 0x2)); x191 = ((uint64_t)(arg1[8]) * ((arg2[16]) * 0x2)); x192 = ((uint64_t)(arg1[8]) * ((arg2[15]) * 0x2)); x193 = ((uint64_t)(arg1[8]) * ((arg2[14]) * 0x2)); x194 = ((uint64_t)(arg1[8]) * ((arg2[13]) * 0x2)); x195 = ((uint64_t)(arg1[8]) * ((arg2[12]) * 0x2)); x196 = ((uint64_t)(arg1[8]) * ((arg2[11]) * 0x2)); x197 = ((uint64_t)(arg1[8]) * ((arg2[10]) * 0x2)); x198 = ((uint64_t)(arg1[7]) * ((arg2[17]) * 0x2)); x199 = ((uint64_t)(arg1[7]) * ((arg2[16]) * 0x2)); x200 = ((uint64_t)(arg1[7]) * ((arg2[15]) * 0x2)); x201 = ((uint64_t)(arg1[7]) * ((arg2[14]) * 0x2)); x202 = ((uint64_t)(arg1[7]) * ((arg2[13]) * 0x2)); x203 = ((uint64_t)(arg1[7]) * ((arg2[12]) * 0x2)); x204 = ((uint64_t)(arg1[7]) * ((arg2[11]) * 0x2)); x205 = ((uint64_t)(arg1[6]) * ((arg2[17]) * 0x2)); x206 = ((uint64_t)(arg1[6]) * ((arg2[16]) * 0x2)); x207 = ((uint64_t)(arg1[6]) * ((arg2[15]) * 0x2)); x208 = ((uint64_t)(arg1[6]) * ((arg2[14]) * 0x2)); x209 = ((uint64_t)(arg1[6]) * ((arg2[13]) * 0x2)); x210 = ((uint64_t)(arg1[6]) * ((arg2[12]) * 0x2)); x211 = ((uint64_t)(arg1[5]) * ((arg2[17]) * 0x2)); x212 = ((uint64_t)(arg1[5]) * ((arg2[16]) * 0x2)); x213 = ((uint64_t)(arg1[5]) * ((arg2[15]) * 0x2)); x214 = ((uint64_t)(arg1[5]) * ((arg2[14]) * 0x2)); x215 = ((uint64_t)(arg1[5]) * ((arg2[13]) * 0x2)); x216 = ((uint64_t)(arg1[4]) * ((arg2[17]) * 0x2)); x217 = ((uint64_t)(arg1[4]) * ((arg2[16]) * 0x2)); x218 = ((uint64_t)(arg1[4]) * ((arg2[15]) * 0x2)); x219 = ((uint64_t)(arg1[4]) * ((arg2[14]) * 0x2)); x220 = ((uint64_t)(arg1[3]) * ((arg2[17]) * 0x2)); x221 = ((uint64_t)(arg1[3]) * ((arg2[16]) * 0x2)); x222 = ((uint64_t)(arg1[3]) * ((arg2[15]) * 0x2)); x223 = ((uint64_t)(arg1[2]) * ((arg2[17]) * 0x2)); x224 = ((uint64_t)(arg1[2]) * ((arg2[16]) * 0x2)); x225 = ((uint64_t)(arg1[1]) * ((arg2[17]) * 0x2)); x226 = ((uint64_t)(arg1[17]) * (arg2[9])); x227 = ((uint64_t)(arg1[17]) * ((arg2[8]) * 0x2)); x228 = ((uint64_t)(arg1[17]) * ((arg2[7]) * 0x2)); x229 = ((uint64_t)(arg1[17]) * ((arg2[6]) * 0x2)); x230 = ((uint64_t)(arg1[17]) * ((arg2[5]) * 0x2)); x231 = ((uint64_t)(arg1[17]) * ((arg2[4]) * 0x2)); x232 = ((uint64_t)(arg1[17]) * ((arg2[3]) * 0x2)); x233 = ((uint64_t)(arg1[17]) * ((arg2[2]) * 0x2)); x234 = ((uint64_t)(arg1[17]) * ((arg2[1]) * 0x2)); x235 = ((uint64_t)(arg1[16]) * (arg2[10])); x236 = ((uint64_t)(arg1[16]) * (arg2[9])); x237 = ((uint64_t)(arg1[16]) * ((arg2[8]) * 0x2)); x238 = ((uint64_t)(arg1[16]) * ((arg2[7]) * 0x2)); x239 = ((uint64_t)(arg1[16]) * ((arg2[6]) * 0x2)); x240 = ((uint64_t)(arg1[16]) * ((arg2[5]) * 0x2)); x241 = ((uint64_t)(arg1[16]) * ((arg2[4]) * 0x2)); x242 = ((uint64_t)(arg1[16]) * ((arg2[3]) * 0x2)); x243 = ((uint64_t)(arg1[16]) * ((arg2[2]) * 0x2)); x244 = ((uint64_t)(arg1[15]) * (arg2[11])); x245 = ((uint64_t)(arg1[15]) * (arg2[10])); x246 = ((uint64_t)(arg1[15]) * (arg2[9])); x247 = ((uint64_t)(arg1[15]) * ((arg2[8]) * 0x2)); x248 = ((uint64_t)(arg1[15]) * ((arg2[7]) * 0x2)); x249 = ((uint64_t)(arg1[15]) * ((arg2[6]) * 0x2)); x250 = ((uint64_t)(arg1[15]) * ((arg2[5]) * 0x2)); x251 = ((uint64_t)(arg1[15]) * ((arg2[4]) * 0x2)); x252 = ((uint64_t)(arg1[15]) * ((arg2[3]) * 0x2)); x253 = ((uint64_t)(arg1[14]) * (arg2[12])); x254 = ((uint64_t)(arg1[14]) * (arg2[11])); x255 = ((uint64_t)(arg1[14]) * (arg2[10])); x256 = ((uint64_t)(arg1[14]) * (arg2[9])); x257 = ((uint64_t)(arg1[14]) * ((arg2[8]) * 0x2)); x258 = ((uint64_t)(arg1[14]) * ((arg2[7]) * 0x2)); x259 = ((uint64_t)(arg1[14]) * ((arg2[6]) * 0x2)); x260 = ((uint64_t)(arg1[14]) * ((arg2[5]) * 0x2)); x261 = ((uint64_t)(arg1[14]) * ((arg2[4]) * 0x2)); x262 = ((uint64_t)(arg1[13]) * (arg2[13])); x263 = ((uint64_t)(arg1[13]) * (arg2[12])); x264 = ((uint64_t)(arg1[13]) * (arg2[11])); x265 = ((uint64_t)(arg1[13]) * (arg2[10])); x266 = ((uint64_t)(arg1[13]) * (arg2[9])); x267 = ((uint64_t)(arg1[13]) * ((arg2[8]) * 0x2)); x268 = ((uint64_t)(arg1[13]) * ((arg2[7]) * 0x2)); x269 = ((uint64_t)(arg1[13]) * ((arg2[6]) * 0x2)); x270 = ((uint64_t)(arg1[13]) * ((arg2[5]) * 0x2)); x271 = ((uint64_t)(arg1[12]) * (arg2[14])); x272 = ((uint64_t)(arg1[12]) * (arg2[13])); x273 = ((uint64_t)(arg1[12]) * (arg2[12])); x274 = ((uint64_t)(arg1[12]) * (arg2[11])); x275 = ((uint64_t)(arg1[12]) * (arg2[10])); x276 = ((uint64_t)(arg1[12]) * (arg2[9])); x277 = ((uint64_t)(arg1[12]) * ((arg2[8]) * 0x2)); x278 = ((uint64_t)(arg1[12]) * ((arg2[7]) * 0x2)); x279 = ((uint64_t)(arg1[12]) * ((arg2[6]) * 0x2)); x280 = ((uint64_t)(arg1[11]) * (arg2[15])); x281 = ((uint64_t)(arg1[11]) * (arg2[14])); x282 = ((uint64_t)(arg1[11]) * (arg2[13])); x283 = ((uint64_t)(arg1[11]) * (arg2[12])); x284 = ((uint64_t)(arg1[11]) * (arg2[11])); x285 = ((uint64_t)(arg1[11]) * (arg2[10])); x286 = ((uint64_t)(arg1[11]) * (arg2[9])); x287 = ((uint64_t)(arg1[11]) * ((arg2[8]) * 0x2)); x288 = ((uint64_t)(arg1[11]) * ((arg2[7]) * 0x2)); x289 = ((uint64_t)(arg1[10]) * (arg2[16])); x290 = ((uint64_t)(arg1[10]) * (arg2[15])); x291 = ((uint64_t)(arg1[10]) * (arg2[14])); x292 = ((uint64_t)(arg1[10]) * (arg2[13])); x293 = ((uint64_t)(arg1[10]) * (arg2[12])); x294 = ((uint64_t)(arg1[10]) * (arg2[11])); x295 = ((uint64_t)(arg1[10]) * (arg2[10])); x296 = ((uint64_t)(arg1[10]) * (arg2[9])); x297 = ((uint64_t)(arg1[10]) * ((arg2[8]) * 0x2)); x298 = ((uint64_t)(arg1[9]) * (arg2[17])); x299 = ((uint64_t)(arg1[9]) * (arg2[16])); x300 = ((uint64_t)(arg1[9]) * (arg2[15])); x301 = ((uint64_t)(arg1[9]) * (arg2[14])); x302 = ((uint64_t)(arg1[9]) * (arg2[13])); x303 = ((uint64_t)(arg1[9]) * (arg2[12])); x304 = ((uint64_t)(arg1[9]) * (arg2[11])); x305 = ((uint64_t)(arg1[9]) * (arg2[10])); x306 = ((uint64_t)(arg1[9]) * (arg2[9])); x307 = ((uint64_t)(arg1[8]) * ((arg2[17]) * 0x2)); x308 = ((uint64_t)(arg1[8]) * ((arg2[16]) * 0x2)); x309 = ((uint64_t)(arg1[8]) * ((arg2[15]) * 0x2)); x310 = ((uint64_t)(arg1[8]) * ((arg2[14]) * 0x2)); x311 = ((uint64_t)(arg1[8]) * ((arg2[13]) * 0x2)); x312 = ((uint64_t)(arg1[8]) * ((arg2[12]) * 0x2)); x313 = ((uint64_t)(arg1[8]) * ((arg2[11]) * 0x2)); x314 = ((uint64_t)(arg1[8]) * ((arg2[10]) * 0x2)); x315 = ((uint64_t)(arg1[7]) * ((arg2[17]) * 0x2)); x316 = ((uint64_t)(arg1[7]) * ((arg2[16]) * 0x2)); x317 = ((uint64_t)(arg1[7]) * ((arg2[15]) * 0x2)); x318 = ((uint64_t)(arg1[7]) * ((arg2[14]) * 0x2)); x319 = ((uint64_t)(arg1[7]) * ((arg2[13]) * 0x2)); x320 = ((uint64_t)(arg1[7]) * ((arg2[12]) * 0x2)); x321 = ((uint64_t)(arg1[7]) * ((arg2[11]) * 0x2)); x322 = ((uint64_t)(arg1[6]) * ((arg2[17]) * 0x2)); x323 = ((uint64_t)(arg1[6]) * ((arg2[16]) * 0x2)); x324 = ((uint64_t)(arg1[6]) * ((arg2[15]) * 0x2)); x325 = ((uint64_t)(arg1[6]) * ((arg2[14]) * 0x2)); x326 = ((uint64_t)(arg1[6]) * ((arg2[13]) * 0x2)); x327 = ((uint64_t)(arg1[6]) * ((arg2[12]) * 0x2)); x328 = ((uint64_t)(arg1[5]) * ((arg2[17]) * 0x2)); x329 = ((uint64_t)(arg1[5]) * ((arg2[16]) * 0x2)); x330 = ((uint64_t)(arg1[5]) * ((arg2[15]) * 0x2)); x331 = ((uint64_t)(arg1[5]) * ((arg2[14]) * 0x2)); x332 = ((uint64_t)(arg1[5]) * ((arg2[13]) * 0x2)); x333 = ((uint64_t)(arg1[4]) * ((arg2[17]) * 0x2)); x334 = ((uint64_t)(arg1[4]) * ((arg2[16]) * 0x2)); x335 = ((uint64_t)(arg1[4]) * ((arg2[15]) * 0x2)); x336 = ((uint64_t)(arg1[4]) * ((arg2[14]) * 0x2)); x337 = ((uint64_t)(arg1[3]) * ((arg2[17]) * 0x2)); x338 = ((uint64_t)(arg1[3]) * ((arg2[16]) * 0x2)); x339 = ((uint64_t)(arg1[3]) * ((arg2[15]) * 0x2)); x340 = ((uint64_t)(arg1[2]) * ((arg2[17]) * 0x2)); x341 = ((uint64_t)(arg1[2]) * ((arg2[16]) * 0x2)); x342 = ((uint64_t)(arg1[1]) * ((arg2[17]) * 0x2)); x343 = ((uint64_t)(arg1[17]) * (arg2[0])); x344 = ((uint64_t)(arg1[16]) * (arg2[1])); x345 = ((uint64_t)(arg1[16]) * (arg2[0])); x346 = ((uint64_t)(arg1[15]) * (arg2[2])); x347 = ((uint64_t)(arg1[15]) * (arg2[1])); x348 = ((uint64_t)(arg1[15]) * (arg2[0])); x349 = ((uint64_t)(arg1[14]) * (arg2[3])); x350 = ((uint64_t)(arg1[14]) * (arg2[2])); x351 = ((uint64_t)(arg1[14]) * (arg2[1])); x352 = ((uint64_t)(arg1[14]) * (arg2[0])); x353 = ((uint64_t)(arg1[13]) * (arg2[4])); x354 = ((uint64_t)(arg1[13]) * (arg2[3])); x355 = ((uint64_t)(arg1[13]) * (arg2[2])); x356 = ((uint64_t)(arg1[13]) * (arg2[1])); x357 = ((uint64_t)(arg1[13]) * (arg2[0])); x358 = ((uint64_t)(arg1[12]) * (arg2[5])); x359 = ((uint64_t)(arg1[12]) * (arg2[4])); x360 = ((uint64_t)(arg1[12]) * (arg2[3])); x361 = ((uint64_t)(arg1[12]) * (arg2[2])); x362 = ((uint64_t)(arg1[12]) * (arg2[1])); x363 = ((uint64_t)(arg1[12]) * (arg2[0])); x364 = ((uint64_t)(arg1[11]) * (arg2[6])); x365 = ((uint64_t)(arg1[11]) * (arg2[5])); x366 = ((uint64_t)(arg1[11]) * (arg2[4])); x367 = ((uint64_t)(arg1[11]) * (arg2[3])); x368 = ((uint64_t)(arg1[11]) * (arg2[2])); x369 = ((uint64_t)(arg1[11]) * (arg2[1])); x370 = ((uint64_t)(arg1[11]) * (arg2[0])); x371 = ((uint64_t)(arg1[10]) * (arg2[7])); x372 = ((uint64_t)(arg1[10]) * (arg2[6])); x373 = ((uint64_t)(arg1[10]) * (arg2[5])); x374 = ((uint64_t)(arg1[10]) * (arg2[4])); x375 = ((uint64_t)(arg1[10]) * (arg2[3])); x376 = ((uint64_t)(arg1[10]) * (arg2[2])); x377 = ((uint64_t)(arg1[10]) * (arg2[1])); x378 = ((uint64_t)(arg1[10]) * (arg2[0])); x379 = ((uint64_t)(arg1[9]) * (arg2[8])); x380 = ((uint64_t)(arg1[9]) * (arg2[7])); x381 = ((uint64_t)(arg1[9]) * (arg2[6])); x382 = ((uint64_t)(arg1[9]) * (arg2[5])); x383 = ((uint64_t)(arg1[9]) * (arg2[4])); x384 = ((uint64_t)(arg1[9]) * (arg2[3])); x385 = ((uint64_t)(arg1[9]) * (arg2[2])); x386 = ((uint64_t)(arg1[9]) * (arg2[1])); x387 = ((uint64_t)(arg1[9]) * (arg2[0])); x388 = ((uint64_t)(arg1[8]) * (arg2[9])); x389 = ((uint64_t)(arg1[8]) * ((arg2[8]) * 0x2)); x390 = ((uint64_t)(arg1[8]) * ((arg2[7]) * 0x2)); x391 = ((uint64_t)(arg1[8]) * ((arg2[6]) * 0x2)); x392 = ((uint64_t)(arg1[8]) * ((arg2[5]) * 0x2)); x393 = ((uint64_t)(arg1[8]) * ((arg2[4]) * 0x2)); x394 = ((uint64_t)(arg1[8]) * ((arg2[3]) * 0x2)); x395 = ((uint64_t)(arg1[8]) * ((arg2[2]) * 0x2)); x396 = ((uint64_t)(arg1[8]) * ((arg2[1]) * 0x2)); x397 = ((uint64_t)(arg1[8]) * (arg2[0])); x398 = ((uint64_t)(arg1[7]) * (arg2[10])); x399 = ((uint64_t)(arg1[7]) * (arg2[9])); x400 = ((uint64_t)(arg1[7]) * ((arg2[8]) * 0x2)); x401 = ((uint64_t)(arg1[7]) * ((arg2[7]) * 0x2)); x402 = ((uint64_t)(arg1[7]) * ((arg2[6]) * 0x2)); x403 = ((uint64_t)(arg1[7]) * ((arg2[5]) * 0x2)); x404 = ((uint64_t)(arg1[7]) * ((arg2[4]) * 0x2)); x405 = ((uint64_t)(arg1[7]) * ((arg2[3]) * 0x2)); x406 = ((uint64_t)(arg1[7]) * ((arg2[2]) * 0x2)); x407 = ((uint64_t)(arg1[7]) * (arg2[1])); x408 = ((uint64_t)(arg1[7]) * (arg2[0])); x409 = ((uint64_t)(arg1[6]) * (arg2[11])); x410 = ((uint64_t)(arg1[6]) * (arg2[10])); x411 = ((uint64_t)(arg1[6]) * (arg2[9])); x412 = ((uint64_t)(arg1[6]) * ((arg2[8]) * 0x2)); x413 = ((uint64_t)(arg1[6]) * ((arg2[7]) * 0x2)); x414 = ((uint64_t)(arg1[6]) * ((arg2[6]) * 0x2)); x415 = ((uint64_t)(arg1[6]) * ((arg2[5]) * 0x2)); x416 = ((uint64_t)(arg1[6]) * ((arg2[4]) * 0x2)); x417 = ((uint64_t)(arg1[6]) * ((arg2[3]) * 0x2)); x418 = ((uint64_t)(arg1[6]) * (arg2[2])); x419 = ((uint64_t)(arg1[6]) * (arg2[1])); x420 = ((uint64_t)(arg1[6]) * (arg2[0])); x421 = ((uint64_t)(arg1[5]) * (arg2[12])); x422 = ((uint64_t)(arg1[5]) * (arg2[11])); x423 = ((uint64_t)(arg1[5]) * (arg2[10])); x424 = ((uint64_t)(arg1[5]) * (arg2[9])); x425 = ((uint64_t)(arg1[5]) * ((arg2[8]) * 0x2)); x426 = ((uint64_t)(arg1[5]) * ((arg2[7]) * 0x2)); x427 = ((uint64_t)(arg1[5]) * ((arg2[6]) * 0x2)); x428 = ((uint64_t)(arg1[5]) * ((arg2[5]) * 0x2)); x429 = ((uint64_t)(arg1[5]) * ((arg2[4]) * 0x2)); x430 = ((uint64_t)(arg1[5]) * (arg2[3])); x431 = ((uint64_t)(arg1[5]) * (arg2[2])); x432 = ((uint64_t)(arg1[5]) * (arg2[1])); x433 = ((uint64_t)(arg1[5]) * (arg2[0])); x434 = ((uint64_t)(arg1[4]) * (arg2[13])); x435 = ((uint64_t)(arg1[4]) * (arg2[12])); x436 = ((uint64_t)(arg1[4]) * (arg2[11])); x437 = ((uint64_t)(arg1[4]) * (arg2[10])); x438 = ((uint64_t)(arg1[4]) * (arg2[9])); x439 = ((uint64_t)(arg1[4]) * ((arg2[8]) * 0x2)); x440 = ((uint64_t)(arg1[4]) * ((arg2[7]) * 0x2)); x441 = ((uint64_t)(arg1[4]) * ((arg2[6]) * 0x2)); x442 = ((uint64_t)(arg1[4]) * ((arg2[5]) * 0x2)); x443 = ((uint64_t)(arg1[4]) * (arg2[4])); x444 = ((uint64_t)(arg1[4]) * (arg2[3])); x445 = ((uint64_t)(arg1[4]) * (arg2[2])); x446 = ((uint64_t)(arg1[4]) * (arg2[1])); x447 = ((uint64_t)(arg1[4]) * (arg2[0])); x448 = ((uint64_t)(arg1[3]) * (arg2[14])); x449 = ((uint64_t)(arg1[3]) * (arg2[13])); x450 = ((uint64_t)(arg1[3]) * (arg2[12])); x451 = ((uint64_t)(arg1[3]) * (arg2[11])); x452 = ((uint64_t)(arg1[3]) * (arg2[10])); x453 = ((uint64_t)(arg1[3]) * (arg2[9])); x454 = ((uint64_t)(arg1[3]) * ((arg2[8]) * 0x2)); x455 = ((uint64_t)(arg1[3]) * ((arg2[7]) * 0x2)); x456 = ((uint64_t)(arg1[3]) * ((arg2[6]) * 0x2)); x457 = ((uint64_t)(arg1[3]) * (arg2[5])); x458 = ((uint64_t)(arg1[3]) * (arg2[4])); x459 = ((uint64_t)(arg1[3]) * (arg2[3])); x460 = ((uint64_t)(arg1[3]) * (arg2[2])); x461 = ((uint64_t)(arg1[3]) * (arg2[1])); x462 = ((uint64_t)(arg1[3]) * (arg2[0])); x463 = ((uint64_t)(arg1[2]) * (arg2[15])); x464 = ((uint64_t)(arg1[2]) * (arg2[14])); x465 = ((uint64_t)(arg1[2]) * (arg2[13])); x466 = ((uint64_t)(arg1[2]) * (arg2[12])); x467 = ((uint64_t)(arg1[2]) * (arg2[11])); x468 = ((uint64_t)(arg1[2]) * (arg2[10])); x469 = ((uint64_t)(arg1[2]) * (arg2[9])); x470 = ((uint64_t)(arg1[2]) * ((arg2[8]) * 0x2)); x471 = ((uint64_t)(arg1[2]) * ((arg2[7]) * 0x2)); x472 = ((uint64_t)(arg1[2]) * (arg2[6])); x473 = ((uint64_t)(arg1[2]) * (arg2[5])); x474 = ((uint64_t)(arg1[2]) * (arg2[4])); x475 = ((uint64_t)(arg1[2]) * (arg2[3])); x476 = ((uint64_t)(arg1[2]) * (arg2[2])); x477 = ((uint64_t)(arg1[2]) * (arg2[1])); x478 = ((uint64_t)(arg1[2]) * (arg2[0])); x479 = ((uint64_t)(arg1[1]) * (arg2[16])); x480 = ((uint64_t)(arg1[1]) * (arg2[15])); x481 = ((uint64_t)(arg1[1]) * (arg2[14])); x482 = ((uint64_t)(arg1[1]) * (arg2[13])); x483 = ((uint64_t)(arg1[1]) * (arg2[12])); x484 = ((uint64_t)(arg1[1]) * (arg2[11])); x485 = ((uint64_t)(arg1[1]) * (arg2[10])); x486 = ((uint64_t)(arg1[1]) * (arg2[9])); x487 = ((uint64_t)(arg1[1]) * ((arg2[8]) * 0x2)); x488 = ((uint64_t)(arg1[1]) * (arg2[7])); x489 = ((uint64_t)(arg1[1]) * (arg2[6])); x490 = ((uint64_t)(arg1[1]) * (arg2[5])); x491 = ((uint64_t)(arg1[1]) * (arg2[4])); x492 = ((uint64_t)(arg1[1]) * (arg2[3])); x493 = ((uint64_t)(arg1[1]) * (arg2[2])); x494 = ((uint64_t)(arg1[1]) * (arg2[1])); x495 = ((uint64_t)(arg1[1]) * (arg2[0])); x496 = ((uint64_t)(arg1[0]) * (arg2[17])); x497 = ((uint64_t)(arg1[0]) * (arg2[16])); x498 = ((uint64_t)(arg1[0]) * (arg2[15])); x499 = ((uint64_t)(arg1[0]) * (arg2[14])); x500 = ((uint64_t)(arg1[0]) * (arg2[13])); x501 = ((uint64_t)(arg1[0]) * (arg2[12])); x502 = ((uint64_t)(arg1[0]) * (arg2[11])); x503 = ((uint64_t)(arg1[0]) * (arg2[10])); x504 = ((uint64_t)(arg1[0]) * (arg2[9])); x505 = ((uint64_t)(arg1[0]) * (arg2[8])); x506 = ((uint64_t)(arg1[0]) * (arg2[7])); x507 = ((uint64_t)(arg1[0]) * (arg2[6])); x508 = ((uint64_t)(arg1[0]) * (arg2[5])); x509 = ((uint64_t)(arg1[0]) * (arg2[4])); x510 = ((uint64_t)(arg1[0]) * (arg2[3])); x511 = ((uint64_t)(arg1[0]) * (arg2[2])); x512 = ((uint64_t)(arg1[0]) * (arg2[1])); x513 = ((uint64_t)(arg1[0]) * (arg2[0])); x514 = (x505 + (x488 + (x472 + (x457 + (x443 + (x430 + (x418 + (x407 + (x397 + (x181 + (x172 + (x162 + (x151 + (x139 + (x126 + (x112 + (x97 + x81))))))))))))))))); x515 = (x514 >> 24); x516 = (uint32_t)(x514 & UINT32_C(0xffffff)); x517 = (x496 + (x479 + (x463 + (x448 + (x434 + (x421 + (x409 + (x398 + (x388 + (x379 + (x371 + (x364 + (x358 + (x353 + (x349 + (x346 + (x344 + (x343 + (x298 + (x289 + (x280 + (x271 + (x262 + (x253 + (x244 + (x235 + x226)))))))))))))))))))))))))); x518 = (x497 + (x480 + (x464 + (x449 + (x435 + (x422 + (x410 + (x399 + (x389 + (x380 + (x372 + (x365 + (x359 + (x354 + (x350 + (x347 + (x345 + (x307 + (x299 + (x290 + (x281 + (x272 + (x263 + (x254 + (x245 + (x236 + (x227 + (x73 + x37)))))))))))))))))))))))))))); x519 = (x498 + (x481 + (x465 + (x450 + (x436 + (x423 + (x411 + (x400 + (x390 + (x381 + (x373 + (x366 + (x360 + (x355 + (x351 + (x348 + (x315 + (x308 + (x300 + (x291 + (x282 + (x273 + (x264 + (x255 + (x246 + (x237 + (x228 + (x90 + (x74 + (x45 + x38)))))))))))))))))))))))))))))); x520 = (x499 + (x482 + (x466 + (x451 + (x437 + (x424 + (x412 + (x401 + (x391 + (x382 + (x374 + (x367 + (x361 + (x356 + (x352 + (x322 + (x316 + (x309 + (x301 + (x292 + (x283 + (x274 + (x265 + (x256 + (x247 + (x238 + (x229 + (x106 + (x91 + (x75 + (x52 + (x46 + x39)))))))))))))))))))))))))))))))); x521 = (x500 + (x483 + (x467 + (x452 + (x438 + (x425 + (x413 + (x402 + (x392 + (x383 + (x375 + (x368 + (x362 + (x357 + (x328 + (x323 + (x317 + (x310 + (x302 + (x293 + (x284 + (x275 + (x266 + (x257 + (x248 + (x239 + (x230 + (x121 + (x107 + (x92 + (x76 + (x58 + (x53 + (x47 + x40)))))))))))))))))))))))))))))))))); x522 = (x501 + (x484 + (x468 + (x453 + (x439 + (x426 + (x414 + (x403 + (x393 + (x384 + (x376 + (x369 + (x363 + (x333 + (x329 + (x324 + (x318 + (x311 + (x303 + (x294 + (x285 + (x276 + (x267 + (x258 + (x249 + (x240 + (x231 + (x135 + (x122 + (x108 + (x93 + (x77 + (x63 + (x59 + (x54 + (x48 + x41)))))))))))))))))))))))))))))))))))); x523 = (x502 + (x485 + (x469 + (x454 + (x440 + (x427 + (x415 + (x404 + (x394 + (x385 + (x377 + (x370 + (x337 + (x334 + (x330 + (x325 + (x319 + (x312 + (x304 + (x295 + (x286 + (x277 + (x268 + (x259 + (x250 + (x241 + (x232 + (x148 + (x136 + (x123 + (x109 + (x94 + (x78 + (x67 + (x64 + (x60 + (x55 + (x49 + x42)))))))))))))))))))))))))))))))))))))); x524 = (x503 + (x486 + (x470 + (x455 + (x441 + (x428 + (x416 + (x405 + (x395 + (x386 + (x378 + (x340 + (x338 + (x335 + (x331 + (x326 + (x320 + (x313 + (x305 + (x296 + (x287 + (x278 + (x269 + (x260 + (x251 + (x242 + (x233 + (x160 + (x149 + (x137 + (x124 + (x110 + (x95 + (x79 + (x70 + (x68 + (x65 + (x61 + (x56 + (x50 + x43)))))))))))))))))))))))))))))))))))))))); x525 = (x504 + (x487 + (x471 + (x456 + (x442 + (x429 + (x417 + (x406 + (x396 + (x387 + (x342 + (x341 + (x339 + (x336 + (x332 + (x327 + (x321 + (x314 + (x306 + (x297 + (x288 + (x279 + (x270 + (x261 + (x252 + (x243 + (x234 + (x171 + (x161 + (x150 + (x138 + (x125 + (x111 + (x96 + (x80 + (x72 + (x71 + (x69 + (x66 + (x62 + (x57 + (x51 + x44)))))))))))))))))))))))))))))))))))))))))); x526 = (x506 + (x489 + (x473 + (x458 + (x444 + (x431 + (x419 + (x408 + (x190 + (x182 + (x173 + (x163 + (x152 + (x140 + (x127 + (x113 + (x98 + (x82 + x1)))))))))))))))))); x527 = (x507 + (x490 + (x474 + (x459 + (x445 + (x432 + (x420 + (x198 + (x191 + (x183 + (x174 + (x164 + (x153 + (x141 + (x128 + (x114 + (x99 + (x83 + (x9 + x2))))))))))))))))))); x528 = (x508 + (x491 + (x475 + (x460 + (x446 + (x433 + (x205 + (x199 + (x192 + (x184 + (x175 + (x165 + (x154 + (x142 + (x129 + (x115 + (x100 + (x84 + (x16 + (x10 + x3)))))))))))))))))))); x529 = (x509 + (x492 + (x476 + (x461 + (x447 + (x211 + (x206 + (x200 + (x193 + (x185 + (x176 + (x166 + (x155 + (x143 + (x130 + (x116 + (x101 + (x85 + (x22 + (x17 + (x11 + x4))))))))))))))))))))); x530 = (x510 + (x493 + (x477 + (x462 + (x216 + (x212 + (x207 + (x201 + (x194 + (x186 + (x177 + (x167 + (x156 + (x144 + (x131 + (x117 + (x102 + (x86 + (x27 + (x23 + (x18 + (x12 + x5)))))))))))))))))))))); x531 = (x511 + (x494 + (x478 + (x220 + (x217 + (x213 + (x208 + (x202 + (x195 + (x187 + (x178 + (x168 + (x157 + (x145 + (x132 + (x118 + (x103 + (x87 + (x31 + (x28 + (x24 + (x19 + (x13 + x6))))))))))))))))))))))); x532 = (x512 + (x495 + (x223 + (x221 + (x218 + (x214 + (x209 + (x203 + (x196 + (x188 + (x179 + (x169 + (x158 + (x146 + (x133 + (x119 + (x104 + (x88 + (x34 + (x32 + (x29 + (x25 + (x20 + (x14 + x7)))))))))))))))))))))))); x533 = (x513 + (x225 + (x224 + (x222 + (x219 + (x215 + (x210 + (x204 + (x197 + (x189 + (x180 + (x170 + (x159 + (x147 + (x134 + (x120 + (x105 + (x89 + (x36 + (x35 + (x33 + (x30 + (x26 + (x21 + (x15 + x8))))))))))))))))))))))))); x534 = (x515 + x525); x535 = (x517 >> 24); x536 = (uint32_t)(x517 & UINT32_C(0xffffff)); x537 = (x534 + x535); x538 = (x537 >> 25); x539 = (uint32_t)(x537 & UINT32_C(0x1ffffff)); x540 = (x533 + x535); x541 = (x538 + x524); x542 = (x540 >> 25); x543 = (uint32_t)(x540 & UINT32_C(0x1ffffff)); x544 = (x542 + x532); x545 = (x541 >> 25); x546 = (uint32_t)(x541 & UINT32_C(0x1ffffff)); x547 = (x545 + x523); x548 = (x544 >> 25); x549 = (uint32_t)(x544 & UINT32_C(0x1ffffff)); x550 = (x548 + x531); x551 = (x547 >> 25); x552 = (uint32_t)(x547 & UINT32_C(0x1ffffff)); x553 = (x551 + x522); x554 = (x550 >> 25); x555 = (uint32_t)(x550 & UINT32_C(0x1ffffff)); x556 = (x554 + x530); x557 = (x553 >> 25); x558 = (uint32_t)(x553 & UINT32_C(0x1ffffff)); x559 = (x557 + x521); x560 = (x556 >> 25); x561 = (uint32_t)(x556 & UINT32_C(0x1ffffff)); x562 = (x560 + x529); x563 = (x559 >> 25); x564 = (uint32_t)(x559 & UINT32_C(0x1ffffff)); x565 = (x563 + x520); x566 = (x562 >> 25); x567 = (uint32_t)(x562 & UINT32_C(0x1ffffff)); x568 = (x566 + x528); x569 = (x565 >> 25); x570 = (uint32_t)(x565 & UINT32_C(0x1ffffff)); x571 = (x569 + x519); x572 = (x568 >> 25); x573 = (uint32_t)(x568 & UINT32_C(0x1ffffff)); x574 = (x572 + x527); x575 = (x571 >> 25); x576 = (uint32_t)(x571 & UINT32_C(0x1ffffff)); x577 = (x575 + x518); x578 = (x574 >> 25); x579 = (uint32_t)(x574 & UINT32_C(0x1ffffff)); x580 = (x578 + x526); x581 = (x577 >> 25); x582 = (uint32_t)(x577 & UINT32_C(0x1ffffff)); x583 = (x581 + x536); x584 = (x580 >> 25); x585 = (uint32_t)(x580 & UINT32_C(0x1ffffff)); x586 = (x584 + x516); x587 = (uint32_t)(x583 >> 24); x588 = (uint32_t)(x583 & UINT32_C(0xffffff)); x589 = (uint32_t)(x586 >> 24); x590 = (uint32_t)(x586 & UINT32_C(0xffffff)); x591 = (x539 + x587); x592 = (x543 + x587); x593 = (x589 + x591); x594 = (fiat_p448_uint1)(x593 >> 25); x595 = (x593 & UINT32_C(0x1ffffff)); x596 = (x594 + x546); x597 = (fiat_p448_uint1)(x592 >> 25); x598 = (x592 & UINT32_C(0x1ffffff)); x599 = (x597 + x549); out1[0] = x598; out1[1] = x599; out1[2] = x555; out1[3] = x561; out1[4] = x567; out1[5] = x573; out1[6] = x579; out1[7] = x585; out1[8] = x590; out1[9] = x595; out1[10] = x596; out1[11] = x552; out1[12] = x558; out1[13] = x564; out1[14] = x570; out1[15] = x576; out1[16] = x582; out1[17] = x588; } /* * The function fiat_p448_carry_square squares a field element and reduces the result. * Postconditions: * eval out1 mod m = (eval arg1 * eval arg1) mod m * * Input Bounds: * arg1: [[0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x3000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x3000000]] * Output Bounds: * out1: [[0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x1000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x1000000]] */ static void fiat_p448_carry_square(uint32_t out1[18], const uint32_t arg1[18]) { uint32_t x1; uint32_t x2; uint32_t x3; uint32_t x4; uint32_t x5; uint32_t x6; uint32_t x7; uint32_t x8; uint32_t x9; uint32_t x10; uint32_t x11; uint32_t x12; uint32_t x13; uint32_t x14; uint32_t x15; uint32_t x16; uint32_t x17; uint32_t x18; uint32_t x19; uint32_t x20; uint32_t x21; uint32_t x22; uint32_t x23; uint32_t x24; uint32_t x25; uint32_t x26; uint32_t x27; uint32_t x28; uint32_t x29; uint32_t x30; uint32_t x31; uint32_t x32; uint32_t x33; uint32_t x34; uint32_t x35; uint32_t x36; uint32_t x37; uint32_t x38; uint32_t x39; uint32_t x40; uint32_t x41; uint32_t x42; uint32_t x43; uint32_t x44; uint32_t x45; uint32_t x46; uint32_t x47; uint32_t x48; uint32_t x49; uint32_t x50; uint32_t x51; uint64_t x52; uint64_t x53; uint64_t x54; uint64_t x55; uint64_t x56; uint64_t x57; uint64_t x58; uint64_t x59; uint64_t x60; uint64_t x61; uint64_t x62; uint64_t x63; uint64_t x64; uint64_t x65; uint64_t x66; uint64_t x67; uint64_t x68; uint64_t x69; uint64_t x70; uint64_t x71; uint64_t x72; uint64_t x73; uint64_t x74; uint64_t x75; uint64_t x76; uint64_t x77; uint64_t x78; uint64_t x79; uint64_t x80; uint64_t x81; uint64_t x82; uint64_t x83; uint64_t x84; uint64_t x85; uint64_t x86; uint64_t x87; uint64_t x88; uint64_t x89; uint64_t x90; uint64_t x91; uint64_t x92; uint64_t x93; uint64_t x94; uint64_t x95; uint64_t x96; uint64_t x97; uint64_t x98; uint64_t x99; uint64_t x100; uint64_t x101; uint64_t x102; uint64_t x103; uint64_t x104; uint64_t x105; uint64_t x106; uint64_t x107; uint64_t x108; uint64_t x109; uint64_t x110; uint64_t x111; uint64_t x112; uint64_t x113; uint64_t x114; uint64_t x115; uint64_t x116; uint64_t x117; uint64_t x118; uint64_t x119; uint64_t x120; uint64_t x121; uint64_t x122; uint64_t x123; uint64_t x124; uint64_t x125; uint64_t x126; uint64_t x127; uint64_t x128; uint64_t x129; uint64_t x130; uint64_t x131; uint64_t x132; uint64_t x133; uint64_t x134; uint64_t x135; uint64_t x136; uint64_t x137; uint64_t x138; uint64_t x139; uint64_t x140; uint64_t x141; uint64_t x142; uint64_t x143; uint64_t x144; uint64_t x145; uint64_t x146; uint64_t x147; uint64_t x148; uint64_t x149; uint64_t x150; uint64_t x151; uint64_t x152; uint64_t x153; uint64_t x154; uint64_t x155; uint64_t x156; uint64_t x157; uint64_t x158; uint64_t x159; uint64_t x160; uint64_t x161; uint64_t x162; uint64_t x163; uint64_t x164; uint64_t x165; uint64_t x166; uint64_t x167; uint64_t x168; uint64_t x169; uint64_t x170; uint64_t x171; uint64_t x172; uint64_t x173; uint64_t x174; uint64_t x175; uint64_t x176; uint64_t x177; uint64_t x178; uint64_t x179; uint64_t x180; uint64_t x181; uint64_t x182; uint64_t x183; uint64_t x184; uint64_t x185; uint64_t x186; uint64_t x187; uint64_t x188; uint64_t x189; uint64_t x190; uint64_t x191; uint64_t x192; uint64_t x193; uint64_t x194; uint64_t x195; uint64_t x196; uint64_t x197; uint64_t x198; uint64_t x199; uint64_t x200; uint64_t x201; uint64_t x202; uint64_t x203; uint64_t x204; uint64_t x205; uint64_t x206; uint64_t x207; uint64_t x208; uint64_t x209; uint64_t x210; uint64_t x211; uint64_t x212; uint64_t x213; uint64_t x214; uint64_t x215; uint64_t x216; uint64_t x217; uint64_t x218; uint64_t x219; uint64_t x220; uint64_t x221; uint64_t x222; uint64_t x223; uint64_t x224; uint64_t x225; uint64_t x226; uint64_t x227; uint64_t x228; uint64_t x229; uint64_t x230; uint64_t x231; uint64_t x232; uint64_t x233; uint64_t x234; uint64_t x235; uint64_t x236; uint64_t x237; uint64_t x238; uint64_t x239; uint64_t x240; uint64_t x241; uint64_t x242; uint64_t x243; uint64_t x244; uint64_t x245; uint64_t x246; uint64_t x247; uint64_t x248; uint64_t x249; uint64_t x250; uint64_t x251; uint64_t x252; uint64_t x253; uint64_t x254; uint64_t x255; uint64_t x256; uint64_t x257; uint64_t x258; uint64_t x259; uint64_t x260; uint64_t x261; uint64_t x262; uint64_t x263; uint64_t x264; uint64_t x265; uint64_t x266; uint64_t x267; uint64_t x268; uint64_t x269; uint64_t x270; uint64_t x271; uint64_t x272; uint64_t x273; uint64_t x274; uint64_t x275; uint64_t x276; uint64_t x277; uint64_t x278; uint64_t x279; uint64_t x280; uint64_t x281; uint64_t x282; uint64_t x283; uint64_t x284; uint64_t x285; uint64_t x286; uint64_t x287; uint64_t x288; uint64_t x289; uint64_t x290; uint64_t x291; uint64_t x292; uint64_t x293; uint64_t x294; uint64_t x295; uint64_t x296; uint64_t x297; uint64_t x298; uint64_t x299; uint64_t x300; uint64_t x301; uint64_t x302; uint64_t x303; uint64_t x304; uint64_t x305; uint64_t x306; uint64_t x307; uint64_t x308; uint64_t x309; uint64_t x310; uint64_t x311; uint64_t x312; uint64_t x313; uint64_t x314; uint64_t x315; uint64_t x316; uint64_t x317; uint64_t x318; uint64_t x319; uint64_t x320; uint64_t x321; uint64_t x322; uint64_t x323; uint64_t x324; uint64_t x325; uint32_t x326; uint64_t x327; uint64_t x328; uint64_t x329; uint64_t x330; uint64_t x331; uint64_t x332; uint64_t x333; uint64_t x334; uint64_t x335; uint64_t x336; uint64_t x337; uint64_t x338; uint64_t x339; uint64_t x340; uint64_t x341; uint64_t x342; uint64_t x343; uint64_t x344; uint64_t x345; uint32_t x346; uint64_t x347; uint64_t x348; uint32_t x349; uint64_t x350; uint64_t x351; uint64_t x352; uint32_t x353; uint64_t x354; uint64_t x355; uint32_t x356; uint64_t x357; uint64_t x358; uint32_t x359; uint64_t x360; uint64_t x361; uint32_t x362; uint64_t x363; uint64_t x364; uint32_t x365; uint64_t x366; uint64_t x367; uint32_t x368; uint64_t x369; uint64_t x370; uint32_t x371; uint64_t x372; uint64_t x373; uint32_t x374; uint64_t x375; uint64_t x376; uint32_t x377; uint64_t x378; uint64_t x379; uint32_t x380; uint64_t x381; uint64_t x382; uint32_t x383; uint64_t x384; uint64_t x385; uint32_t x386; uint64_t x387; uint64_t x388; uint32_t x389; uint64_t x390; uint64_t x391; uint32_t x392; uint64_t x393; uint64_t x394; uint32_t x395; uint64_t x396; uint32_t x397; uint32_t x398; uint32_t x399; uint32_t x400; uint32_t x401; uint32_t x402; uint32_t x403; fiat_p448_uint1 x404; uint32_t x405; uint32_t x406; fiat_p448_uint1 x407; uint32_t x408; uint32_t x409; x1 = (arg1[17]); x2 = (arg1[17]); x3 = (x1 * 0x2); x4 = (x2 * 0x2); x5 = ((arg1[17]) * 0x2); x6 = (arg1[16]); x7 = (arg1[16]); x8 = (x6 * 0x2); x9 = (x7 * 0x2); x10 = ((arg1[16]) * 0x2); x11 = (arg1[15]); x12 = (arg1[15]); x13 = (x11 * 0x2); x14 = (x12 * 0x2); x15 = ((arg1[15]) * 0x2); x16 = (arg1[14]); x17 = (arg1[14]); x18 = (x16 * 0x2); x19 = (x17 * 0x2); x20 = ((arg1[14]) * 0x2); x21 = (arg1[13]); x22 = (arg1[13]); x23 = (x21 * 0x2); x24 = (x22 * 0x2); x25 = ((arg1[13]) * 0x2); x26 = (arg1[12]); x27 = (arg1[12]); x28 = (x26 * 0x2); x29 = (x27 * 0x2); x30 = ((arg1[12]) * 0x2); x31 = (arg1[11]); x32 = (arg1[11]); x33 = (x31 * 0x2); x34 = (x32 * 0x2); x35 = ((arg1[11]) * 0x2); x36 = (arg1[10]); x37 = (arg1[10]); x38 = (x36 * 0x2); x39 = (x37 * 0x2); x40 = ((arg1[10]) * 0x2); x41 = (arg1[9]); x42 = (arg1[9]); x43 = ((arg1[9]) * 0x2); x44 = ((arg1[8]) * 0x2); x45 = ((arg1[7]) * 0x2); x46 = ((arg1[6]) * 0x2); x47 = ((arg1[5]) * 0x2); x48 = ((arg1[4]) * 0x2); x49 = ((arg1[3]) * 0x2); x50 = ((arg1[2]) * 0x2); x51 = ((arg1[1]) * 0x2); x52 = ((uint64_t)(arg1[17]) * (x1 * 0x2)); x53 = ((uint64_t)(arg1[16]) * (x3 * 0x2)); x54 = ((uint64_t)(arg1[16]) * (x6 * 0x2)); x55 = ((uint64_t)(arg1[15]) * (x3 * 0x2)); x56 = ((uint64_t)(arg1[15]) * (x8 * 0x2)); x57 = ((uint64_t)(arg1[15]) * (x11 * 0x2)); x58 = ((uint64_t)(arg1[14]) * (x3 * 0x2)); x59 = ((uint64_t)(arg1[14]) * (x8 * 0x2)); x60 = ((uint64_t)(arg1[14]) * (x13 * 0x2)); x61 = ((uint64_t)(arg1[14]) * (x16 * 0x2)); x62 = ((uint64_t)(arg1[13]) * (x3 * 0x2)); x63 = ((uint64_t)(arg1[13]) * (x8 * 0x2)); x64 = ((uint64_t)(arg1[13]) * (x13 * 0x2)); x65 = ((uint64_t)(arg1[13]) * (x18 * 0x2)); x66 = ((uint64_t)(arg1[12]) * (x3 * 0x2)); x67 = ((uint64_t)(arg1[12]) * (x8 * 0x2)); x68 = ((uint64_t)(arg1[12]) * (x13 * 0x2)); x69 = ((uint64_t)(arg1[11]) * (x3 * 0x2)); x70 = ((uint64_t)(arg1[11]) * (x8 * 0x2)); x71 = ((uint64_t)(arg1[10]) * (x3 * 0x2)); x72 = ((uint64_t)(arg1[17]) * (x1 * 0x2)); x73 = ((uint64_t)(arg1[16]) * (x3 * 0x2)); x74 = ((uint64_t)(arg1[16]) * (x6 * 0x2)); x75 = ((uint64_t)(arg1[15]) * (x3 * 0x2)); x76 = ((uint64_t)(arg1[15]) * (x8 * 0x2)); x77 = ((uint64_t)(arg1[15]) * (x11 * 0x2)); x78 = ((uint64_t)(arg1[14]) * (x3 * 0x2)); x79 = ((uint64_t)(arg1[14]) * (x8 * 0x2)); x80 = ((uint64_t)(arg1[14]) * (x13 * 0x2)); x81 = ((uint64_t)(arg1[14]) * (x16 * 0x2)); x82 = ((uint64_t)(arg1[13]) * (x3 * 0x2)); x83 = ((uint64_t)(arg1[13]) * (x8 * 0x2)); x84 = ((uint64_t)(arg1[13]) * (x13 * 0x2)); x85 = ((uint64_t)(arg1[13]) * (x18 * 0x2)); x86 = ((uint64_t)(arg1[12]) * (x3 * 0x2)); x87 = ((uint64_t)(arg1[12]) * (x8 * 0x2)); x88 = ((uint64_t)(arg1[12]) * (x13 * 0x2)); x89 = ((uint64_t)(arg1[11]) * (x3 * 0x2)); x90 = ((uint64_t)(arg1[11]) * (x8 * 0x2)); x91 = ((uint64_t)(arg1[10]) * (x3 * 0x2)); x92 = ((uint64_t)(arg1[17]) * (x2 * 0x2)); x93 = ((uint64_t)(arg1[16]) * (x4 * 0x2)); x94 = ((uint64_t)(arg1[16]) * (x7 * 0x2)); x95 = ((uint64_t)(arg1[15]) * (x4 * 0x2)); x96 = ((uint64_t)(arg1[15]) * (x9 * 0x2)); x97 = ((uint64_t)(arg1[15]) * (x12 * 0x2)); x98 = ((uint64_t)(arg1[14]) * (x4 * 0x2)); x99 = ((uint64_t)(arg1[14]) * (x9 * 0x2)); x100 = ((uint64_t)(arg1[14]) * (x14 * 0x2)); x101 = ((uint64_t)(arg1[14]) * (x17 * 0x2)); x102 = ((uint64_t)(arg1[13]) * (x4 * 0x2)); x103 = ((uint64_t)(arg1[13]) * (x9 * 0x2)); x104 = ((uint64_t)(arg1[13]) * (x14 * 0x2)); x105 = ((uint64_t)(arg1[13]) * (x19 * 0x2)); x106 = ((uint64_t)(arg1[13]) * x22); x107 = ((uint64_t)(arg1[13]) * x21); x108 = ((uint64_t)(arg1[12]) * (x4 * 0x2)); x109 = ((uint64_t)(arg1[12]) * (x9 * 0x2)); x110 = ((uint64_t)(arg1[12]) * (x14 * 0x2)); x111 = ((uint64_t)(arg1[12]) * x19); x112 = ((uint64_t)(arg1[12]) * x18); x113 = ((uint64_t)(arg1[12]) * x24); x114 = ((uint64_t)(arg1[12]) * x23); x115 = ((uint64_t)(arg1[12]) * x27); x116 = ((uint64_t)(arg1[12]) * x26); x117 = ((uint64_t)(arg1[11]) * (x4 * 0x2)); x118 = ((uint64_t)(arg1[11]) * (x9 * 0x2)); x119 = ((uint64_t)(arg1[11]) * x14); x120 = ((uint64_t)(arg1[11]) * x13); x121 = ((uint64_t)(arg1[11]) * x19); x122 = ((uint64_t)(arg1[11]) * x18); x123 = ((uint64_t)(arg1[11]) * x24); x124 = ((uint64_t)(arg1[11]) * x23); x125 = ((uint64_t)(arg1[11]) * x29); x126 = ((uint64_t)(arg1[11]) * x28); x127 = ((uint64_t)(arg1[11]) * x32); x128 = ((uint64_t)(arg1[11]) * x31); x129 = ((uint64_t)(arg1[10]) * (x4 * 0x2)); x130 = ((uint64_t)(arg1[10]) * x9); x131 = ((uint64_t)(arg1[10]) * x8); x132 = ((uint64_t)(arg1[10]) * x14); x133 = ((uint64_t)(arg1[10]) * x13); x134 = ((uint64_t)(arg1[10]) * x19); x135 = ((uint64_t)(arg1[10]) * x18); x136 = ((uint64_t)(arg1[10]) * x24); x137 = ((uint64_t)(arg1[10]) * x23); x138 = ((uint64_t)(arg1[10]) * x29); x139 = ((uint64_t)(arg1[10]) * x28); x140 = ((uint64_t)(arg1[10]) * x34); x141 = ((uint64_t)(arg1[10]) * x33); x142 = ((uint64_t)(arg1[10]) * x37); x143 = ((uint64_t)(arg1[10]) * x36); x144 = ((uint64_t)(arg1[9]) * x4); x145 = ((uint64_t)(arg1[9]) * x3); x146 = ((uint64_t)(arg1[9]) * x9); x147 = ((uint64_t)(arg1[9]) * x8); x148 = ((uint64_t)(arg1[9]) * x14); x149 = ((uint64_t)(arg1[9]) * x13); x150 = ((uint64_t)(arg1[9]) * x19); x151 = ((uint64_t)(arg1[9]) * x18); x152 = ((uint64_t)(arg1[9]) * x24); x153 = ((uint64_t)(arg1[9]) * x23); x154 = ((uint64_t)(arg1[9]) * x29); x155 = ((uint64_t)(arg1[9]) * x28); x156 = ((uint64_t)(arg1[9]) * x34); x157 = ((uint64_t)(arg1[9]) * x33); x158 = ((uint64_t)(arg1[9]) * x39); x159 = ((uint64_t)(arg1[9]) * x38); x160 = ((uint64_t)(arg1[9]) * x42); x161 = ((uint64_t)(arg1[9]) * x41); x162 = ((uint64_t)(arg1[8]) * (x4 * 0x2)); x163 = ((uint64_t)(arg1[8]) * (x3 * 0x2)); x164 = ((uint64_t)(arg1[8]) * (x9 * 0x2)); x165 = ((uint64_t)(arg1[8]) * (x8 * 0x2)); x166 = ((uint64_t)(arg1[8]) * (x14 * 0x2)); x167 = ((uint64_t)(arg1[8]) * (x13 * 0x2)); x168 = ((uint64_t)(arg1[8]) * (x19 * 0x2)); x169 = ((uint64_t)(arg1[8]) * (x18 * 0x2)); x170 = ((uint64_t)(arg1[8]) * (x24 * 0x2)); x171 = ((uint64_t)(arg1[8]) * (x23 * 0x2)); x172 = ((uint64_t)(arg1[8]) * (x29 * 0x2)); x173 = ((uint64_t)(arg1[8]) * (x28 * 0x2)); x174 = ((uint64_t)(arg1[8]) * (x34 * 0x2)); x175 = ((uint64_t)(arg1[8]) * (x33 * 0x2)); x176 = ((uint64_t)(arg1[8]) * (x39 * 0x2)); x177 = ((uint64_t)(arg1[8]) * (x38 * 0x2)); x178 = ((uint64_t)(arg1[8]) * x43); x179 = ((uint64_t)(arg1[8]) * ((arg1[8]) * 0x2)); x180 = ((uint64_t)(arg1[7]) * (x4 * 0x2)); x181 = ((uint64_t)(arg1[7]) * (x3 * 0x2)); x182 = ((uint64_t)(arg1[7]) * (x9 * 0x2)); x183 = ((uint64_t)(arg1[7]) * (x8 * 0x2)); x184 = ((uint64_t)(arg1[7]) * (x14 * 0x2)); x185 = ((uint64_t)(arg1[7]) * (x13 * 0x2)); x186 = ((uint64_t)(arg1[7]) * (x19 * 0x2)); x187 = ((uint64_t)(arg1[7]) * (x18 * 0x2)); x188 = ((uint64_t)(arg1[7]) * (x24 * 0x2)); x189 = ((uint64_t)(arg1[7]) * (x23 * 0x2)); x190 = ((uint64_t)(arg1[7]) * (x29 * 0x2)); x191 = ((uint64_t)(arg1[7]) * (x28 * 0x2)); x192 = ((uint64_t)(arg1[7]) * (x34 * 0x2)); x193 = ((uint64_t)(arg1[7]) * (x33 * 0x2)); x194 = ((uint64_t)(arg1[7]) * x40); x195 = ((uint64_t)(arg1[7]) * x43); x196 = ((uint64_t)(arg1[7]) * (x44 * 0x2)); x197 = ((uint64_t)(arg1[7]) * ((arg1[7]) * 0x2)); x198 = ((uint64_t)(arg1[6]) * (x4 * 0x2)); x199 = ((uint64_t)(arg1[6]) * (x3 * 0x2)); x200 = ((uint64_t)(arg1[6]) * (x9 * 0x2)); x201 = ((uint64_t)(arg1[6]) * (x8 * 0x2)); x202 = ((uint64_t)(arg1[6]) * (x14 * 0x2)); x203 = ((uint64_t)(arg1[6]) * (x13 * 0x2)); x204 = ((uint64_t)(arg1[6]) * (x19 * 0x2)); x205 = ((uint64_t)(arg1[6]) * (x18 * 0x2)); x206 = ((uint64_t)(arg1[6]) * (x24 * 0x2)); x207 = ((uint64_t)(arg1[6]) * (x23 * 0x2)); x208 = ((uint64_t)(arg1[6]) * (x29 * 0x2)); x209 = ((uint64_t)(arg1[6]) * (x28 * 0x2)); x210 = ((uint64_t)(arg1[6]) * x35); x211 = ((uint64_t)(arg1[6]) * x40); x212 = ((uint64_t)(arg1[6]) * x43); x213 = ((uint64_t)(arg1[6]) * (x44 * 0x2)); x214 = ((uint64_t)(arg1[6]) * (x45 * 0x2)); x215 = ((uint64_t)(arg1[6]) * ((arg1[6]) * 0x2)); x216 = ((uint64_t)(arg1[5]) * (x4 * 0x2)); x217 = ((uint64_t)(arg1[5]) * (x3 * 0x2)); x218 = ((uint64_t)(arg1[5]) * (x9 * 0x2)); x219 = ((uint64_t)(arg1[5]) * (x8 * 0x2)); x220 = ((uint64_t)(arg1[5]) * (x14 * 0x2)); x221 = ((uint64_t)(arg1[5]) * (x13 * 0x2)); x222 = ((uint64_t)(arg1[5]) * (x19 * 0x2)); x223 = ((uint64_t)(arg1[5]) * (x18 * 0x2)); x224 = ((uint64_t)(arg1[5]) * (x24 * 0x2)); x225 = ((uint64_t)(arg1[5]) * (x23 * 0x2)); x226 = ((uint64_t)(arg1[5]) * x30); x227 = ((uint64_t)(arg1[5]) * x35); x228 = ((uint64_t)(arg1[5]) * x40); x229 = ((uint64_t)(arg1[5]) * x43); x230 = ((uint64_t)(arg1[5]) * (x44 * 0x2)); x231 = ((uint64_t)(arg1[5]) * (x45 * 0x2)); x232 = ((uint64_t)(arg1[5]) * (x46 * 0x2)); x233 = ((uint64_t)(arg1[5]) * ((arg1[5]) * 0x2)); x234 = ((uint64_t)(arg1[4]) * (x4 * 0x2)); x235 = ((uint64_t)(arg1[4]) * (x3 * 0x2)); x236 = ((uint64_t)(arg1[4]) * (x9 * 0x2)); x237 = ((uint64_t)(arg1[4]) * (x8 * 0x2)); x238 = ((uint64_t)(arg1[4]) * (x14 * 0x2)); x239 = ((uint64_t)(arg1[4]) * (x13 * 0x2)); x240 = ((uint64_t)(arg1[4]) * (x19 * 0x2)); x241 = ((uint64_t)(arg1[4]) * (x18 * 0x2)); x242 = ((uint64_t)(arg1[4]) * x25); x243 = ((uint64_t)(arg1[4]) * x30); x244 = ((uint64_t)(arg1[4]) * x35); x245 = ((uint64_t)(arg1[4]) * x40); x246 = ((uint64_t)(arg1[4]) * x43); x247 = ((uint64_t)(arg1[4]) * (x44 * 0x2)); x248 = ((uint64_t)(arg1[4]) * (x45 * 0x2)); x249 = ((uint64_t)(arg1[4]) * (x46 * 0x2)); x250 = ((uint64_t)(arg1[4]) * (x47 * 0x2)); x251 = ((uint64_t)(arg1[4]) * (arg1[4])); x252 = ((uint64_t)(arg1[3]) * (x4 * 0x2)); x253 = ((uint64_t)(arg1[3]) * (x3 * 0x2)); x254 = ((uint64_t)(arg1[3]) * (x9 * 0x2)); x255 = ((uint64_t)(arg1[3]) * (x8 * 0x2)); x256 = ((uint64_t)(arg1[3]) * (x14 * 0x2)); x257 = ((uint64_t)(arg1[3]) * (x13 * 0x2)); x258 = ((uint64_t)(arg1[3]) * x20); x259 = ((uint64_t)(arg1[3]) * x25); x260 = ((uint64_t)(arg1[3]) * x30); x261 = ((uint64_t)(arg1[3]) * x35); x262 = ((uint64_t)(arg1[3]) * x40); x263 = ((uint64_t)(arg1[3]) * x43); x264 = ((uint64_t)(arg1[3]) * (x44 * 0x2)); x265 = ((uint64_t)(arg1[3]) * (x45 * 0x2)); x266 = ((uint64_t)(arg1[3]) * (x46 * 0x2)); x267 = ((uint64_t)(arg1[3]) * x47); x268 = ((uint64_t)(arg1[3]) * x48); x269 = ((uint64_t)(arg1[3]) * (arg1[3])); x270 = ((uint64_t)(arg1[2]) * (x4 * 0x2)); x271 = ((uint64_t)(arg1[2]) * (x3 * 0x2)); x272 = ((uint64_t)(arg1[2]) * (x9 * 0x2)); x273 = ((uint64_t)(arg1[2]) * (x8 * 0x2)); x274 = ((uint64_t)(arg1[2]) * x15); x275 = ((uint64_t)(arg1[2]) * x20); x276 = ((uint64_t)(arg1[2]) * x25); x277 = ((uint64_t)(arg1[2]) * x30); x278 = ((uint64_t)(arg1[2]) * x35); x279 = ((uint64_t)(arg1[2]) * x40); x280 = ((uint64_t)(arg1[2]) * x43); x281 = ((uint64_t)(arg1[2]) * (x44 * 0x2)); x282 = ((uint64_t)(arg1[2]) * (x45 * 0x2)); x283 = ((uint64_t)(arg1[2]) * x46); x284 = ((uint64_t)(arg1[2]) * x47); x285 = ((uint64_t)(arg1[2]) * x48); x286 = ((uint64_t)(arg1[2]) * x49); x287 = ((uint64_t)(arg1[2]) * (arg1[2])); x288 = ((uint64_t)(arg1[1]) * (x4 * 0x2)); x289 = ((uint64_t)(arg1[1]) * (x3 * 0x2)); x290 = ((uint64_t)(arg1[1]) * x10); x291 = ((uint64_t)(arg1[1]) * x15); x292 = ((uint64_t)(arg1[1]) * x20); x293 = ((uint64_t)(arg1[1]) * x25); x294 = ((uint64_t)(arg1[1]) * x30); x295 = ((uint64_t)(arg1[1]) * x35); x296 = ((uint64_t)(arg1[1]) * x40); x297 = ((uint64_t)(arg1[1]) * x43); x298 = ((uint64_t)(arg1[1]) * (x44 * 0x2)); x299 = ((uint64_t)(arg1[1]) * x45); x300 = ((uint64_t)(arg1[1]) * x46); x301 = ((uint64_t)(arg1[1]) * x47); x302 = ((uint64_t)(arg1[1]) * x48); x303 = ((uint64_t)(arg1[1]) * x49); x304 = ((uint64_t)(arg1[1]) * x50); x305 = ((uint64_t)(arg1[1]) * (arg1[1])); x306 = ((uint64_t)(arg1[0]) * x5); x307 = ((uint64_t)(arg1[0]) * x10); x308 = ((uint64_t)(arg1[0]) * x15); x309 = ((uint64_t)(arg1[0]) * x20); x310 = ((uint64_t)(arg1[0]) * x25); x311 = ((uint64_t)(arg1[0]) * x30); x312 = ((uint64_t)(arg1[0]) * x35); x313 = ((uint64_t)(arg1[0]) * x40); x314 = ((uint64_t)(arg1[0]) * x43); x315 = ((uint64_t)(arg1[0]) * x44); x316 = ((uint64_t)(arg1[0]) * x45); x317 = ((uint64_t)(arg1[0]) * x46); x318 = ((uint64_t)(arg1[0]) * x47); x319 = ((uint64_t)(arg1[0]) * x48); x320 = ((uint64_t)(arg1[0]) * x49); x321 = ((uint64_t)(arg1[0]) * x50); x322 = ((uint64_t)(arg1[0]) * x51); x323 = ((uint64_t)(arg1[0]) * (arg1[0])); x324 = (x315 + (x299 + (x283 + (x267 + (x251 + (x144 + (x130 + (x119 + (x111 + x106))))))))); x325 = (x324 >> 24); x326 = (uint32_t)(x324 & UINT32_C(0xffffff)); x327 = (x306 + (x290 + (x274 + (x258 + (x242 + (x226 + (x210 + (x194 + (x178 + (x145 + (x131 + (x120 + (x112 + x107))))))))))))); x328 = (x307 + (x291 + (x275 + (x259 + (x243 + (x227 + (x211 + (x195 + (x179 + (x163 + (x147 + (x133 + (x122 + (x114 + (x92 + x72))))))))))))))); x329 = (x308 + (x292 + (x276 + (x260 + (x244 + (x228 + (x212 + (x196 + (x181 + (x165 + (x149 + (x135 + (x124 + (x116 + (x93 + x73))))))))))))))); x330 = (x309 + (x293 + (x277 + (x261 + (x245 + (x229 + (x213 + (x199 + (x197 + (x183 + (x167 + (x151 + (x137 + (x126 + (x95 + (x94 + (x75 + x74))))))))))))))))); x331 = (x310 + (x294 + (x278 + (x262 + (x246 + (x230 + (x217 + (x214 + (x201 + (x185 + (x169 + (x153 + (x139 + (x128 + (x98 + (x96 + (x78 + x76))))))))))))))))); x332 = (x311 + (x295 + (x279 + (x263 + (x247 + (x235 + (x231 + (x219 + (x215 + (x203 + (x187 + (x171 + (x155 + (x141 + (x102 + (x99 + (x97 + (x82 + (x79 + x77))))))))))))))))))); x333 = (x312 + (x296 + (x280 + (x264 + (x253 + (x248 + (x237 + (x232 + (x221 + (x205 + (x189 + (x173 + (x157 + (x143 + (x108 + (x103 + (x100 + (x86 + (x83 + x80))))))))))))))))))); x334 = (x313 + (x297 + (x281 + (x271 + (x265 + (x255 + (x249 + (x239 + (x233 + (x223 + (x207 + (x191 + (x175 + (x159 + (x117 + (x109 + (x104 + (x101 + (x89 + (x87 + (x84 + x81))))))))))))))))))))); x335 = (x314 + (x298 + (x289 + (x282 + (x273 + (x266 + (x257 + (x250 + (x241 + (x225 + (x209 + (x193 + (x177 + (x161 + (x129 + (x118 + (x110 + (x105 + (x91 + (x90 + (x88 + x85))))))))))))))))))))); x336 = (x316 + (x300 + (x284 + (x268 + (x162 + (x146 + (x132 + (x121 + (x113 + x52))))))))); x337 = (x317 + (x301 + (x285 + (x269 + (x180 + (x164 + (x148 + (x134 + (x123 + (x115 + x53)))))))))); x338 = (x318 + (x302 + (x286 + (x198 + (x182 + (x166 + (x150 + (x136 + (x125 + (x55 + x54)))))))))); x339 = (x319 + (x303 + (x287 + (x216 + (x200 + (x184 + (x168 + (x152 + (x138 + (x127 + (x58 + x56))))))))))); x340 = (x320 + (x304 + (x234 + (x218 + (x202 + (x186 + (x170 + (x154 + (x140 + (x62 + (x59 + x57))))))))))); x341 = (x321 + (x305 + (x252 + (x236 + (x220 + (x204 + (x188 + (x172 + (x156 + (x142 + (x66 + (x63 + x60)))))))))))); x342 = (x322 + (x270 + (x254 + (x238 + (x222 + (x206 + (x190 + (x174 + (x158 + (x69 + (x67 + (x64 + x61)))))))))))); x343 = (x323 + (x288 + (x272 + (x256 + (x240 + (x224 + (x208 + (x192 + (x176 + (x160 + (x71 + (x70 + (x68 + x65))))))))))))); x344 = (x325 + x335); x345 = (x327 >> 24); x346 = (uint32_t)(x327 & UINT32_C(0xffffff)); x347 = (x344 + x345); x348 = (x347 >> 25); x349 = (uint32_t)(x347 & UINT32_C(0x1ffffff)); x350 = (x343 + x345); x351 = (x348 + x334); x352 = (x350 >> 25); x353 = (uint32_t)(x350 & UINT32_C(0x1ffffff)); x354 = (x352 + x342); x355 = (x351 >> 25); x356 = (uint32_t)(x351 & UINT32_C(0x1ffffff)); x357 = (x355 + x333); x358 = (x354 >> 25); x359 = (uint32_t)(x354 & UINT32_C(0x1ffffff)); x360 = (x358 + x341); x361 = (x357 >> 25); x362 = (uint32_t)(x357 & UINT32_C(0x1ffffff)); x363 = (x361 + x332); x364 = (x360 >> 25); x365 = (uint32_t)(x360 & UINT32_C(0x1ffffff)); x366 = (x364 + x340); x367 = (x363 >> 25); x368 = (uint32_t)(x363 & UINT32_C(0x1ffffff)); x369 = (x367 + x331); x370 = (x366 >> 25); x371 = (uint32_t)(x366 & UINT32_C(0x1ffffff)); x372 = (x370 + x339); x373 = (x369 >> 25); x374 = (uint32_t)(x369 & UINT32_C(0x1ffffff)); x375 = (x373 + x330); x376 = (x372 >> 25); x377 = (uint32_t)(x372 & UINT32_C(0x1ffffff)); x378 = (x376 + x338); x379 = (x375 >> 25); x380 = (uint32_t)(x375 & UINT32_C(0x1ffffff)); x381 = (x379 + x329); x382 = (x378 >> 25); x383 = (uint32_t)(x378 & UINT32_C(0x1ffffff)); x384 = (x382 + x337); x385 = (x381 >> 25); x386 = (uint32_t)(x381 & UINT32_C(0x1ffffff)); x387 = (x385 + x328); x388 = (x384 >> 25); x389 = (uint32_t)(x384 & UINT32_C(0x1ffffff)); x390 = (x388 + x336); x391 = (x387 >> 25); x392 = (uint32_t)(x387 & UINT32_C(0x1ffffff)); x393 = (x391 + x346); x394 = (x390 >> 25); x395 = (uint32_t)(x390 & UINT32_C(0x1ffffff)); x396 = (x394 + x326); x397 = (uint32_t)(x393 >> 24); x398 = (uint32_t)(x393 & UINT32_C(0xffffff)); x399 = (uint32_t)(x396 >> 24); x400 = (uint32_t)(x396 & UINT32_C(0xffffff)); x401 = (x349 + x397); x402 = (x353 + x397); x403 = (x399 + x401); x404 = (fiat_p448_uint1)(x403 >> 25); x405 = (x403 & UINT32_C(0x1ffffff)); x406 = (x404 + x356); x407 = (fiat_p448_uint1)(x402 >> 25); x408 = (x402 & UINT32_C(0x1ffffff)); x409 = (x407 + x359); out1[0] = x408; out1[1] = x409; out1[2] = x365; out1[3] = x371; out1[4] = x377; out1[5] = x383; out1[6] = x389; out1[7] = x395; out1[8] = x400; out1[9] = x405; out1[10] = x406; out1[11] = x362; out1[12] = x368; out1[13] = x374; out1[14] = x380; out1[15] = x386; out1[16] = x392; out1[17] = x398; } /* * The function fiat_p448_carry_scmul_3 multiplies a field element by 3 and reduces the result. * Postconditions: * eval out1 mod m = (3 * eval arg1) mod m * * Input Bounds: * arg1: [[0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x3000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x3000000]] * Output Bounds: * out1: [[0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x1000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x1000000]] */ static void fiat_p448_carry_scmul_3(uint32_t out1[18], const uint32_t arg1[18]) { uint32_t x1; uint32_t x2; uint32_t x3; uint32_t x4; uint32_t x5; uint32_t x6; uint32_t x7; uint32_t x8; uint32_t x9; uint32_t x10; uint32_t x11; uint32_t x12; uint32_t x13; uint32_t x14; uint32_t x15; uint32_t x16; uint32_t x17; uint32_t x18; uint32_t x19; uint32_t x20; uint32_t x21; uint32_t x22; uint32_t x23; uint32_t x24; uint32_t x25; uint32_t x26; uint32_t x27; uint32_t x28; uint32_t x29; uint32_t x30; uint32_t x31; uint32_t x32; uint32_t x33; uint32_t x34; uint32_t x35; uint32_t x36; uint32_t x37; uint32_t x38; uint32_t x39; uint32_t x40; uint32_t x41; uint32_t x42; uint32_t x43; uint32_t x44; uint32_t x45; uint32_t x46; uint32_t x47; uint32_t x48; uint32_t x49; uint32_t x50; uint32_t x51; uint32_t x52; uint32_t x53; uint32_t x54; uint32_t x55; uint32_t x56; uint32_t x57; uint32_t x58; uint32_t x59; uint32_t x60; uint32_t x61; uint32_t x62; uint32_t x63; uint32_t x64; uint32_t x65; uint32_t x66; uint32_t x67; uint32_t x68; uint32_t x69; uint32_t x70; uint32_t x71; uint32_t x72; uint32_t x73; fiat_p448_uint1 x74; uint32_t x75; fiat_p448_uint1 x76; uint32_t x77; uint32_t x78; uint32_t x79; uint32_t x80; fiat_p448_uint1 x81; uint32_t x82; uint32_t x83; fiat_p448_uint1 x84; uint32_t x85; uint32_t x86; x1 = ((arg1[17]) * 0x3); x2 = ((arg1[16]) * 0x3); x3 = ((arg1[15]) * 0x3); x4 = ((arg1[14]) * 0x3); x5 = ((arg1[13]) * 0x3); x6 = ((arg1[12]) * 0x3); x7 = ((arg1[11]) * 0x3); x8 = ((arg1[10]) * 0x3); x9 = ((arg1[9]) * 0x3); x10 = ((arg1[8]) * 0x3); x11 = ((arg1[7]) * 0x3); x12 = ((arg1[6]) * 0x3); x13 = ((arg1[5]) * 0x3); x14 = ((arg1[4]) * 0x3); x15 = ((arg1[3]) * 0x3); x16 = ((arg1[2]) * 0x3); x17 = ((arg1[1]) * 0x3); x18 = ((arg1[0]) * 0x3); x19 = (x10 >> 24); x20 = (x10 & UINT32_C(0xffffff)); x21 = (x19 + x9); x22 = (x1 >> 24); x23 = (x1 & UINT32_C(0xffffff)); x24 = (x21 + x22); x25 = (x24 >> 25); x26 = (x24 & UINT32_C(0x1ffffff)); x27 = (x18 + x22); x28 = (x25 + x8); x29 = (x27 >> 25); x30 = (x27 & UINT32_C(0x1ffffff)); x31 = (x29 + x17); x32 = (x28 >> 25); x33 = (x28 & UINT32_C(0x1ffffff)); x34 = (x32 + x7); x35 = (x31 >> 25); x36 = (x31 & UINT32_C(0x1ffffff)); x37 = (x35 + x16); x38 = (x34 >> 25); x39 = (x34 & UINT32_C(0x1ffffff)); x40 = (x38 + x6); x41 = (x37 >> 25); x42 = (x37 & UINT32_C(0x1ffffff)); x43 = (x41 + x15); x44 = (x40 >> 25); x45 = (x40 & UINT32_C(0x1ffffff)); x46 = (x44 + x5); x47 = (x43 >> 25); x48 = (x43 & UINT32_C(0x1ffffff)); x49 = (x47 + x14); x50 = (x46 >> 25); x51 = (x46 & UINT32_C(0x1ffffff)); x52 = (x50 + x4); x53 = (x49 >> 25); x54 = (x49 & UINT32_C(0x1ffffff)); x55 = (x53 + x13); x56 = (x52 >> 25); x57 = (x52 & UINT32_C(0x1ffffff)); x58 = (x56 + x3); x59 = (x55 >> 25); x60 = (x55 & UINT32_C(0x1ffffff)); x61 = (x59 + x12); x62 = (x58 >> 25); x63 = (x58 & UINT32_C(0x1ffffff)); x64 = (x62 + x2); x65 = (x61 >> 25); x66 = (x61 & UINT32_C(0x1ffffff)); x67 = (x65 + x11); x68 = (x64 >> 25); x69 = (x64 & UINT32_C(0x1ffffff)); x70 = (x68 + x23); x71 = (x67 >> 25); x72 = (x67 & UINT32_C(0x1ffffff)); x73 = (x71 + x20); x74 = (fiat_p448_uint1)(x70 >> 24); x75 = (x70 & UINT32_C(0xffffff)); x76 = (fiat_p448_uint1)(x73 >> 24); x77 = (x73 & UINT32_C(0xffffff)); x78 = (x26 + (uint32_t)x74); x79 = (x30 + (uint32_t)x74); x80 = (x76 + x78); x81 = (fiat_p448_uint1)(x80 >> 25); x82 = (x80 & UINT32_C(0x1ffffff)); x83 = (x81 + x33); x84 = (fiat_p448_uint1)(x79 >> 25); x85 = (x79 & UINT32_C(0x1ffffff)); x86 = (x84 + x36); out1[0] = x85; out1[1] = x86; out1[2] = x42; out1[3] = x48; out1[4] = x54; out1[5] = x60; out1[6] = x66; out1[7] = x72; out1[8] = x77; out1[9] = x82; out1[10] = x83; out1[11] = x39; out1[12] = x45; out1[13] = x51; out1[14] = x57; out1[15] = x63; out1[16] = x69; out1[17] = x75; } /* * The function fiat_p448_carry_scmul_4 multiplies a field element by 4 and reduces the result. * Postconditions: * eval out1 mod m = (4 * eval arg1) mod m * * Input Bounds: * arg1: [[0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x3000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x3000000]] * Output Bounds: * out1: [[0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x1000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x1000000]] */ static void fiat_p448_carry_scmul_4(uint32_t out1[18], const uint32_t arg1[18]) { uint32_t x1; uint32_t x2; uint32_t x3; uint32_t x4; uint32_t x5; uint32_t x6; uint32_t x7; uint32_t x8; uint32_t x9; uint32_t x10; uint32_t x11; uint32_t x12; uint32_t x13; uint32_t x14; uint32_t x15; uint32_t x16; uint32_t x17; uint32_t x18; uint32_t x19; uint32_t x20; uint32_t x21; uint32_t x22; uint32_t x23; uint32_t x24; uint32_t x25; uint32_t x26; uint32_t x27; uint32_t x28; uint32_t x29; uint32_t x30; uint32_t x31; uint32_t x32; uint32_t x33; uint32_t x34; uint32_t x35; uint32_t x36; uint32_t x37; uint32_t x38; uint32_t x39; uint32_t x40; uint32_t x41; uint32_t x42; uint32_t x43; uint32_t x44; uint32_t x45; uint32_t x46; uint32_t x47; uint32_t x48; uint32_t x49; uint32_t x50; uint32_t x51; uint32_t x52; uint32_t x53; uint32_t x54; uint32_t x55; uint32_t x56; uint32_t x57; uint32_t x58; uint32_t x59; uint32_t x60; uint32_t x61; uint32_t x62; uint32_t x63; uint32_t x64; uint32_t x65; uint32_t x66; uint32_t x67; uint32_t x68; uint32_t x69; uint32_t x70; uint32_t x71; uint32_t x72; uint32_t x73; fiat_p448_uint1 x74; uint32_t x75; fiat_p448_uint1 x76; uint32_t x77; uint32_t x78; uint32_t x79; uint32_t x80; fiat_p448_uint1 x81; uint32_t x82; uint32_t x83; fiat_p448_uint1 x84; uint32_t x85; uint32_t x86; x1 = ((arg1[17]) << 2); x2 = ((arg1[16]) << 2); x3 = ((arg1[15]) << 2); x4 = ((arg1[14]) << 2); x5 = ((arg1[13]) << 2); x6 = ((arg1[12]) << 2); x7 = ((arg1[11]) << 2); x8 = ((arg1[10]) << 2); x9 = ((arg1[9]) << 2); x10 = ((arg1[8]) << 2); x11 = ((arg1[7]) << 2); x12 = ((arg1[6]) << 2); x13 = ((arg1[5]) << 2); x14 = ((arg1[4]) << 2); x15 = ((arg1[3]) << 2); x16 = ((arg1[2]) << 2); x17 = ((arg1[1]) << 2); x18 = ((arg1[0]) << 2); x19 = (x10 >> 24); x20 = (x10 & UINT32_C(0xffffff)); x21 = (x19 + x9); x22 = (x1 >> 24); x23 = (x1 & UINT32_C(0xffffff)); x24 = (x21 + x22); x25 = (x24 >> 25); x26 = (x24 & UINT32_C(0x1ffffff)); x27 = (x18 + x22); x28 = (x25 + x8); x29 = (x27 >> 25); x30 = (x27 & UINT32_C(0x1ffffff)); x31 = (x29 + x17); x32 = (x28 >> 25); x33 = (x28 & UINT32_C(0x1ffffff)); x34 = (x32 + x7); x35 = (x31 >> 25); x36 = (x31 & UINT32_C(0x1ffffff)); x37 = (x35 + x16); x38 = (x34 >> 25); x39 = (x34 & UINT32_C(0x1ffffff)); x40 = (x38 + x6); x41 = (x37 >> 25); x42 = (x37 & UINT32_C(0x1ffffff)); x43 = (x41 + x15); x44 = (x40 >> 25); x45 = (x40 & UINT32_C(0x1ffffff)); x46 = (x44 + x5); x47 = (x43 >> 25); x48 = (x43 & UINT32_C(0x1ffffff)); x49 = (x47 + x14); x50 = (x46 >> 25); x51 = (x46 & UINT32_C(0x1ffffff)); x52 = (x50 + x4); x53 = (x49 >> 25); x54 = (x49 & UINT32_C(0x1ffffff)); x55 = (x53 + x13); x56 = (x52 >> 25); x57 = (x52 & UINT32_C(0x1ffffff)); x58 = (x56 + x3); x59 = (x55 >> 25); x60 = (x55 & UINT32_C(0x1ffffff)); x61 = (x59 + x12); x62 = (x58 >> 25); x63 = (x58 & UINT32_C(0x1ffffff)); x64 = (x62 + x2); x65 = (x61 >> 25); x66 = (x61 & UINT32_C(0x1ffffff)); x67 = (x65 + x11); x68 = (x64 >> 25); x69 = (x64 & UINT32_C(0x1ffffff)); x70 = (x68 + x23); x71 = (x67 >> 25); x72 = (x67 & UINT32_C(0x1ffffff)); x73 = (x71 + x20); x74 = (fiat_p448_uint1)(x70 >> 24); x75 = (x70 & UINT32_C(0xffffff)); x76 = (fiat_p448_uint1)(x73 >> 24); x77 = (x73 & UINT32_C(0xffffff)); x78 = (x26 + (uint32_t)x74); x79 = (x30 + (uint32_t)x74); x80 = (x76 + x78); x81 = (fiat_p448_uint1)(x80 >> 25); x82 = (x80 & UINT32_C(0x1ffffff)); x83 = (x81 + x33); x84 = (fiat_p448_uint1)(x79 >> 25); x85 = (x79 & UINT32_C(0x1ffffff)); x86 = (x84 + x36); out1[0] = x85; out1[1] = x86; out1[2] = x42; out1[3] = x48; out1[4] = x54; out1[5] = x60; out1[6] = x66; out1[7] = x72; out1[8] = x77; out1[9] = x82; out1[10] = x83; out1[11] = x39; out1[12] = x45; out1[13] = x51; out1[14] = x57; out1[15] = x63; out1[16] = x69; out1[17] = x75; } /* * The function fiat_p448_carry_scmul_8 multiplies a field element by 8 and reduces the result. * Postconditions: * eval out1 mod m = (8 * eval arg1) mod m * * Input Bounds: * arg1: [[0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x3000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x3000000]] * Output Bounds: * out1: [[0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x1000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x1000000]] */ static void fiat_p448_carry_scmul_8(uint32_t out1[18], const uint32_t arg1[18]) { uint32_t x1; uint32_t x2; uint32_t x3; uint32_t x4; uint32_t x5; uint32_t x6; uint32_t x7; uint32_t x8; uint32_t x9; uint32_t x10; uint32_t x11; uint32_t x12; uint32_t x13; uint32_t x14; uint32_t x15; uint32_t x16; uint32_t x17; uint32_t x18; uint32_t x19; uint32_t x20; uint32_t x21; uint32_t x22; uint32_t x23; uint32_t x24; uint32_t x25; uint32_t x26; uint32_t x27; uint32_t x28; uint32_t x29; uint32_t x30; uint32_t x31; uint32_t x32; uint32_t x33; uint32_t x34; uint32_t x35; uint32_t x36; uint32_t x37; uint32_t x38; uint32_t x39; uint32_t x40; uint32_t x41; uint32_t x42; uint32_t x43; uint32_t x44; uint32_t x45; uint32_t x46; uint32_t x47; uint32_t x48; uint32_t x49; uint32_t x50; uint32_t x51; uint32_t x52; uint32_t x53; uint32_t x54; uint32_t x55; uint32_t x56; uint32_t x57; uint32_t x58; uint32_t x59; uint32_t x60; uint32_t x61; uint32_t x62; uint32_t x63; uint32_t x64; uint32_t x65; uint32_t x66; uint32_t x67; uint32_t x68; uint32_t x69; uint32_t x70; uint32_t x71; uint32_t x72; uint32_t x73; fiat_p448_uint1 x74; uint32_t x75; fiat_p448_uint1 x76; uint32_t x77; uint32_t x78; uint32_t x79; uint32_t x80; fiat_p448_uint1 x81; uint32_t x82; uint32_t x83; fiat_p448_uint1 x84; uint32_t x85; uint32_t x86; x1 = ((arg1[17]) << 3); x2 = ((arg1[16]) << 3); x3 = ((arg1[15]) << 3); x4 = ((arg1[14]) << 3); x5 = ((arg1[13]) << 3); x6 = ((arg1[12]) << 3); x7 = ((arg1[11]) << 3); x8 = ((arg1[10]) << 3); x9 = ((arg1[9]) << 3); x10 = ((arg1[8]) << 3); x11 = ((arg1[7]) << 3); x12 = ((arg1[6]) << 3); x13 = ((arg1[5]) << 3); x14 = ((arg1[4]) << 3); x15 = ((arg1[3]) << 3); x16 = ((arg1[2]) << 3); x17 = ((arg1[1]) << 3); x18 = ((arg1[0]) << 3); x19 = (x10 >> 24); x20 = (x10 & UINT32_C(0xffffff)); x21 = (x19 + x9); x22 = (x1 >> 24); x23 = (x1 & UINT32_C(0xffffff)); x24 = (x21 + x22); x25 = (x24 >> 25); x26 = (x24 & UINT32_C(0x1ffffff)); x27 = (x18 + x22); x28 = (x25 + x8); x29 = (x27 >> 25); x30 = (x27 & UINT32_C(0x1ffffff)); x31 = (x29 + x17); x32 = (x28 >> 25); x33 = (x28 & UINT32_C(0x1ffffff)); x34 = (x32 + x7); x35 = (x31 >> 25); x36 = (x31 & UINT32_C(0x1ffffff)); x37 = (x35 + x16); x38 = (x34 >> 25); x39 = (x34 & UINT32_C(0x1ffffff)); x40 = (x38 + x6); x41 = (x37 >> 25); x42 = (x37 & UINT32_C(0x1ffffff)); x43 = (x41 + x15); x44 = (x40 >> 25); x45 = (x40 & UINT32_C(0x1ffffff)); x46 = (x44 + x5); x47 = (x43 >> 25); x48 = (x43 & UINT32_C(0x1ffffff)); x49 = (x47 + x14); x50 = (x46 >> 25); x51 = (x46 & UINT32_C(0x1ffffff)); x52 = (x50 + x4); x53 = (x49 >> 25); x54 = (x49 & UINT32_C(0x1ffffff)); x55 = (x53 + x13); x56 = (x52 >> 25); x57 = (x52 & UINT32_C(0x1ffffff)); x58 = (x56 + x3); x59 = (x55 >> 25); x60 = (x55 & UINT32_C(0x1ffffff)); x61 = (x59 + x12); x62 = (x58 >> 25); x63 = (x58 & UINT32_C(0x1ffffff)); x64 = (x62 + x2); x65 = (x61 >> 25); x66 = (x61 & UINT32_C(0x1ffffff)); x67 = (x65 + x11); x68 = (x64 >> 25); x69 = (x64 & UINT32_C(0x1ffffff)); x70 = (x68 + x23); x71 = (x67 >> 25); x72 = (x67 & UINT32_C(0x1ffffff)); x73 = (x71 + x20); x74 = (fiat_p448_uint1)(x70 >> 24); x75 = (x70 & UINT32_C(0xffffff)); x76 = (fiat_p448_uint1)(x73 >> 24); x77 = (x73 & UINT32_C(0xffffff)); x78 = (x26 + (uint32_t)x74); x79 = (x30 + (uint32_t)x74); x80 = (x76 + x78); x81 = (fiat_p448_uint1)(x80 >> 25); x82 = (x80 & UINT32_C(0x1ffffff)); x83 = (x81 + x33); x84 = (fiat_p448_uint1)(x79 >> 25); x85 = (x79 & UINT32_C(0x1ffffff)); x86 = (x84 + x36); out1[0] = x85; out1[1] = x86; out1[2] = x42; out1[3] = x48; out1[4] = x54; out1[5] = x60; out1[6] = x66; out1[7] = x72; out1[8] = x77; out1[9] = x82; out1[10] = x83; out1[11] = x39; out1[12] = x45; out1[13] = x51; out1[14] = x57; out1[15] = x63; out1[16] = x69; out1[17] = x75; } /* * The function fiat_p448_carry_scmul_39082 multiplies a field element by 39082 and reduces the result. * Postconditions: * eval out1 mod m = (39082 * eval arg1) mod m * * Input Bounds: * arg1: [[0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x3000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x3000000]] * Output Bounds: * out1: [[0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x1000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x1000000]] */ static void fiat_p448_carry_scmul_39082(uint32_t out1[18], const uint32_t arg1[18]) { uint64_t x1; uint64_t x2; uint64_t x3; uint64_t x4; uint64_t x5; uint64_t x6; uint64_t x7; uint64_t x8; uint64_t x9; uint64_t x10; uint64_t x11; uint64_t x12; uint64_t x13; uint64_t x14; uint64_t x15; uint64_t x16; uint64_t x17; uint64_t x18; uint32_t x19; uint32_t x20; uint64_t x21; uint32_t x22; uint32_t x23; uint64_t x24; uint32_t x25; uint32_t x26; uint64_t x27; uint64_t x28; uint32_t x29; uint32_t x30; uint64_t x31; uint32_t x32; uint32_t x33; uint64_t x34; uint32_t x35; uint32_t x36; uint64_t x37; uint32_t x38; uint32_t x39; uint64_t x40; uint32_t x41; uint32_t x42; uint64_t x43; uint32_t x44; uint32_t x45; uint64_t x46; uint32_t x47; uint32_t x48; uint64_t x49; uint32_t x50; uint32_t x51; uint64_t x52; uint32_t x53; uint32_t x54; uint64_t x55; uint32_t x56; uint32_t x57; uint64_t x58; uint32_t x59; uint32_t x60; uint64_t x61; uint32_t x62; uint32_t x63; uint64_t x64; uint32_t x65; uint32_t x66; uint64_t x67; uint32_t x68; uint32_t x69; uint32_t x70; uint32_t x71; uint32_t x72; uint32_t x73; fiat_p448_uint1 x74; uint32_t x75; fiat_p448_uint1 x76; uint32_t x77; uint32_t x78; uint32_t x79; uint32_t x80; fiat_p448_uint1 x81; uint32_t x82; uint32_t x83; fiat_p448_uint1 x84; uint32_t x85; uint32_t x86; x1 = ((uint64_t)UINT16_C(0x98aa) * (arg1[17])); x2 = ((uint64_t)UINT16_C(0x98aa) * (arg1[16])); x3 = ((uint64_t)UINT16_C(0x98aa) * (arg1[15])); x4 = ((uint64_t)UINT16_C(0x98aa) * (arg1[14])); x5 = ((uint64_t)UINT16_C(0x98aa) * (arg1[13])); x6 = ((uint64_t)UINT16_C(0x98aa) * (arg1[12])); x7 = ((uint64_t)UINT16_C(0x98aa) * (arg1[11])); x8 = ((uint64_t)UINT16_C(0x98aa) * (arg1[10])); x9 = ((uint64_t)UINT16_C(0x98aa) * (arg1[9])); x10 = ((uint64_t)UINT16_C(0x98aa) * (arg1[8])); x11 = ((uint64_t)UINT16_C(0x98aa) * (arg1[7])); x12 = ((uint64_t)UINT16_C(0x98aa) * (arg1[6])); x13 = ((uint64_t)UINT16_C(0x98aa) * (arg1[5])); x14 = ((uint64_t)UINT16_C(0x98aa) * (arg1[4])); x15 = ((uint64_t)UINT16_C(0x98aa) * (arg1[3])); x16 = ((uint64_t)UINT16_C(0x98aa) * (arg1[2])); x17 = ((uint64_t)UINT16_C(0x98aa) * (arg1[1])); x18 = ((uint64_t)UINT16_C(0x98aa) * (arg1[0])); x19 = (uint32_t)(x10 >> 24); x20 = (uint32_t)(x10 & UINT32_C(0xffffff)); x21 = (x19 + x9); x22 = (uint32_t)(x1 >> 24); x23 = (uint32_t)(x1 & UINT32_C(0xffffff)); x24 = (x21 + x22); x25 = (uint32_t)(x24 >> 25); x26 = (uint32_t)(x24 & UINT32_C(0x1ffffff)); x27 = (x18 + x22); x28 = (x25 + x8); x29 = (uint32_t)(x27 >> 25); x30 = (uint32_t)(x27 & UINT32_C(0x1ffffff)); x31 = (x29 + x17); x32 = (uint32_t)(x28 >> 25); x33 = (uint32_t)(x28 & UINT32_C(0x1ffffff)); x34 = (x32 + x7); x35 = (uint32_t)(x31 >> 25); x36 = (uint32_t)(x31 & UINT32_C(0x1ffffff)); x37 = (x35 + x16); x38 = (uint32_t)(x34 >> 25); x39 = (uint32_t)(x34 & UINT32_C(0x1ffffff)); x40 = (x38 + x6); x41 = (uint32_t)(x37 >> 25); x42 = (uint32_t)(x37 & UINT32_C(0x1ffffff)); x43 = (x41 + x15); x44 = (uint32_t)(x40 >> 25); x45 = (uint32_t)(x40 & UINT32_C(0x1ffffff)); x46 = (x44 + x5); x47 = (uint32_t)(x43 >> 25); x48 = (uint32_t)(x43 & UINT32_C(0x1ffffff)); x49 = (x47 + x14); x50 = (uint32_t)(x46 >> 25); x51 = (uint32_t)(x46 & UINT32_C(0x1ffffff)); x52 = (x50 + x4); x53 = (uint32_t)(x49 >> 25); x54 = (uint32_t)(x49 & UINT32_C(0x1ffffff)); x55 = (x53 + x13); x56 = (uint32_t)(x52 >> 25); x57 = (uint32_t)(x52 & UINT32_C(0x1ffffff)); x58 = (x56 + x3); x59 = (uint32_t)(x55 >> 25); x60 = (uint32_t)(x55 & UINT32_C(0x1ffffff)); x61 = (x59 + x12); x62 = (uint32_t)(x58 >> 25); x63 = (uint32_t)(x58 & UINT32_C(0x1ffffff)); x64 = (x62 + x2); x65 = (uint32_t)(x61 >> 25); x66 = (uint32_t)(x61 & UINT32_C(0x1ffffff)); x67 = (x65 + x11); x68 = (uint32_t)(x64 >> 25); x69 = (uint32_t)(x64 & UINT32_C(0x1ffffff)); x70 = (x68 + x23); x71 = (uint32_t)(x67 >> 25); x72 = (uint32_t)(x67 & UINT32_C(0x1ffffff)); x73 = (x71 + x20); x74 = (fiat_p448_uint1)(x70 >> 24); x75 = (x70 & UINT32_C(0xffffff)); x76 = (fiat_p448_uint1)(x73 >> 24); x77 = (x73 & UINT32_C(0xffffff)); x78 = (x26 + (uint32_t)x74); x79 = (x30 + (uint32_t)x74); x80 = (x76 + x78); x81 = (fiat_p448_uint1)(x80 >> 25); x82 = (x80 & UINT32_C(0x1ffffff)); x83 = (x81 + x33); x84 = (fiat_p448_uint1)(x79 >> 25); x85 = (x79 & UINT32_C(0x1ffffff)); x86 = (x84 + x36); out1[0] = x85; out1[1] = x86; out1[2] = x42; out1[3] = x48; out1[4] = x54; out1[5] = x60; out1[6] = x66; out1[7] = x72; out1[8] = x77; out1[9] = x82; out1[10] = x83; out1[11] = x39; out1[12] = x45; out1[13] = x51; out1[14] = x57; out1[15] = x63; out1[16] = x69; out1[17] = x75; } /* * The function fiat_p448_carry_scmul_39081 multiplies a field element by 39081 and reduces the result. * Postconditions: * eval out1 mod m = (39081 * eval arg1) mod m * * Input Bounds: * arg1: [[0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x3000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x6000000], [0x0 ~> 0x3000000]] * Output Bounds: * out1: [[0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x1000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x1000000]] */ static void fiat_p448_carry_scmul_39081(uint32_t out1[18], const uint32_t arg1[18]) { uint64_t x1; uint64_t x2; uint64_t x3; uint64_t x4; uint64_t x5; uint64_t x6; uint64_t x7; uint64_t x8; uint64_t x9; uint64_t x10; uint64_t x11; uint64_t x12; uint64_t x13; uint64_t x14; uint64_t x15; uint64_t x16; uint64_t x17; uint64_t x18; uint32_t x19; uint32_t x20; uint64_t x21; uint32_t x22; uint32_t x23; uint64_t x24; uint32_t x25; uint32_t x26; uint64_t x27; uint64_t x28; uint32_t x29; uint32_t x30; uint64_t x31; uint32_t x32; uint32_t x33; uint64_t x34; uint32_t x35; uint32_t x36; uint64_t x37; uint32_t x38; uint32_t x39; uint64_t x40; uint32_t x41; uint32_t x42; uint64_t x43; uint32_t x44; uint32_t x45; uint64_t x46; uint32_t x47; uint32_t x48; uint64_t x49; uint32_t x50; uint32_t x51; uint64_t x52; uint32_t x53; uint32_t x54; uint64_t x55; uint32_t x56; uint32_t x57; uint64_t x58; uint32_t x59; uint32_t x60; uint64_t x61; uint32_t x62; uint32_t x63; uint64_t x64; uint32_t x65; uint32_t x66; uint64_t x67; uint32_t x68; uint32_t x69; uint32_t x70; uint32_t x71; uint32_t x72; uint32_t x73; fiat_p448_uint1 x74; uint32_t x75; fiat_p448_uint1 x76; uint32_t x77; uint32_t x78; uint32_t x79; uint32_t x80; fiat_p448_uint1 x81; uint32_t x82; uint32_t x83; fiat_p448_uint1 x84; uint32_t x85; uint32_t x86; x1 = ((uint64_t)UINT16_C(0x98a9) * (arg1[17])); x2 = ((uint64_t)UINT16_C(0x98a9) * (arg1[16])); x3 = ((uint64_t)UINT16_C(0x98a9) * (arg1[15])); x4 = ((uint64_t)UINT16_C(0x98a9) * (arg1[14])); x5 = ((uint64_t)UINT16_C(0x98a9) * (arg1[13])); x6 = ((uint64_t)UINT16_C(0x98a9) * (arg1[12])); x7 = ((uint64_t)UINT16_C(0x98a9) * (arg1[11])); x8 = ((uint64_t)UINT16_C(0x98a9) * (arg1[10])); x9 = ((uint64_t)UINT16_C(0x98a9) * (arg1[9])); x10 = ((uint64_t)UINT16_C(0x98a9) * (arg1[8])); x11 = ((uint64_t)UINT16_C(0x98a9) * (arg1[7])); x12 = ((uint64_t)UINT16_C(0x98a9) * (arg1[6])); x13 = ((uint64_t)UINT16_C(0x98a9) * (arg1[5])); x14 = ((uint64_t)UINT16_C(0x98a9) * (arg1[4])); x15 = ((uint64_t)UINT16_C(0x98a9) * (arg1[3])); x16 = ((uint64_t)UINT16_C(0x98a9) * (arg1[2])); x17 = ((uint64_t)UINT16_C(0x98a9) * (arg1[1])); x18 = ((uint64_t)UINT16_C(0x98a9) * (arg1[0])); x19 = (uint32_t)(x10 >> 24); x20 = (uint32_t)(x10 & UINT32_C(0xffffff)); x21 = (x19 + x9); x22 = (uint32_t)(x1 >> 24); x23 = (uint32_t)(x1 & UINT32_C(0xffffff)); x24 = (x21 + x22); x25 = (uint32_t)(x24 >> 25); x26 = (uint32_t)(x24 & UINT32_C(0x1ffffff)); x27 = (x18 + x22); x28 = (x25 + x8); x29 = (uint32_t)(x27 >> 25); x30 = (uint32_t)(x27 & UINT32_C(0x1ffffff)); x31 = (x29 + x17); x32 = (uint32_t)(x28 >> 25); x33 = (uint32_t)(x28 & UINT32_C(0x1ffffff)); x34 = (x32 + x7); x35 = (uint32_t)(x31 >> 25); x36 = (uint32_t)(x31 & UINT32_C(0x1ffffff)); x37 = (x35 + x16); x38 = (uint32_t)(x34 >> 25); x39 = (uint32_t)(x34 & UINT32_C(0x1ffffff)); x40 = (x38 + x6); x41 = (uint32_t)(x37 >> 25); x42 = (uint32_t)(x37 & UINT32_C(0x1ffffff)); x43 = (x41 + x15); x44 = (uint32_t)(x40 >> 25); x45 = (uint32_t)(x40 & UINT32_C(0x1ffffff)); x46 = (x44 + x5); x47 = (uint32_t)(x43 >> 25); x48 = (uint32_t)(x43 & UINT32_C(0x1ffffff)); x49 = (x47 + x14); x50 = (uint32_t)(x46 >> 25); x51 = (uint32_t)(x46 & UINT32_C(0x1ffffff)); x52 = (x50 + x4); x53 = (uint32_t)(x49 >> 25); x54 = (uint32_t)(x49 & UINT32_C(0x1ffffff)); x55 = (x53 + x13); x56 = (uint32_t)(x52 >> 25); x57 = (uint32_t)(x52 & UINT32_C(0x1ffffff)); x58 = (x56 + x3); x59 = (uint32_t)(x55 >> 25); x60 = (uint32_t)(x55 & UINT32_C(0x1ffffff)); x61 = (x59 + x12); x62 = (uint32_t)(x58 >> 25); x63 = (uint32_t)(x58 & UINT32_C(0x1ffffff)); x64 = (x62 + x2); x65 = (uint32_t)(x61 >> 25); x66 = (uint32_t)(x61 & UINT32_C(0x1ffffff)); x67 = (x65 + x11); x68 = (uint32_t)(x64 >> 25); x69 = (uint32_t)(x64 & UINT32_C(0x1ffffff)); x70 = (x68 + x23); x71 = (uint32_t)(x67 >> 25); x72 = (uint32_t)(x67 & UINT32_C(0x1ffffff)); x73 = (x71 + x20); x74 = (fiat_p448_uint1)(x70 >> 24); x75 = (x70 & UINT32_C(0xffffff)); x76 = (fiat_p448_uint1)(x73 >> 24); x77 = (x73 & UINT32_C(0xffffff)); x78 = (x26 + (uint32_t)x74); x79 = (x30 + (uint32_t)x74); x80 = (x76 + x78); x81 = (fiat_p448_uint1)(x80 >> 25); x82 = (x80 & UINT32_C(0x1ffffff)); x83 = (x81 + x33); x84 = (fiat_p448_uint1)(x79 >> 25); x85 = (x79 & UINT32_C(0x1ffffff)); x86 = (x84 + x36); out1[0] = x85; out1[1] = x86; out1[2] = x42; out1[3] = x48; out1[4] = x54; out1[5] = x60; out1[6] = x66; out1[7] = x72; out1[8] = x77; out1[9] = x82; out1[10] = x83; out1[11] = x39; out1[12] = x45; out1[13] = x51; out1[14] = x57; out1[15] = x63; out1[16] = x69; out1[17] = x75; } /* * The function fiat_p448_selectznz is a multi-limb conditional select. * Postconditions: * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) * * Input Bounds: * arg1: [0x0 ~> 0x1] * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * arg3: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] * Output Bounds: * out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */ static void fiat_p448_selectznz(uint32_t out1[18], fiat_p448_uint1 arg1, const uint32_t arg2[18], const uint32_t arg3[18]) { uint32_t x1; uint32_t x2; uint32_t x3; uint32_t x4; uint32_t x5; uint32_t x6; uint32_t x7; uint32_t x8; uint32_t x9; uint32_t x10; uint32_t x11; uint32_t x12; uint32_t x13; uint32_t x14; uint32_t x15; uint32_t x16; uint32_t x17; uint32_t x18; fiat_p448_cmovznz_u32(&x1, arg1, (arg2[0]), (arg3[0])); fiat_p448_cmovznz_u32(&x2, arg1, (arg2[1]), (arg3[1])); fiat_p448_cmovznz_u32(&x3, arg1, (arg2[2]), (arg3[2])); fiat_p448_cmovznz_u32(&x4, arg1, (arg2[3]), (arg3[3])); fiat_p448_cmovznz_u32(&x5, arg1, (arg2[4]), (arg3[4])); fiat_p448_cmovznz_u32(&x6, arg1, (arg2[5]), (arg3[5])); fiat_p448_cmovznz_u32(&x7, arg1, (arg2[6]), (arg3[6])); fiat_p448_cmovznz_u32(&x8, arg1, (arg2[7]), (arg3[7])); fiat_p448_cmovznz_u32(&x9, arg1, (arg2[8]), (arg3[8])); fiat_p448_cmovznz_u32(&x10, arg1, (arg2[9]), (arg3[9])); fiat_p448_cmovznz_u32(&x11, arg1, (arg2[10]), (arg3[10])); fiat_p448_cmovznz_u32(&x12, arg1, (arg2[11]), (arg3[11])); fiat_p448_cmovznz_u32(&x13, arg1, (arg2[12]), (arg3[12])); fiat_p448_cmovznz_u32(&x14, arg1, (arg2[13]), (arg3[13])); fiat_p448_cmovznz_u32(&x15, arg1, (arg2[14]), (arg3[14])); fiat_p448_cmovznz_u32(&x16, arg1, (arg2[15]), (arg3[15])); fiat_p448_cmovznz_u32(&x17, arg1, (arg2[16]), (arg3[16])); fiat_p448_cmovznz_u32(&x18, arg1, (arg2[17]), (arg3[17])); out1[0] = x1; out1[1] = x2; out1[2] = x3; out1[3] = x4; out1[4] = x5; out1[5] = x6; out1[6] = x7; out1[7] = x8; out1[8] = x9; out1[9] = x10; out1[10] = x11; out1[11] = x12; out1[12] = x13; out1[13] = x14; out1[14] = x15; out1[15] = x16; out1[16] = x17; out1[17] = x18; } /* * The function fiat_p448_to_bytes serializes a field element to bytes in little-endian order. * Postconditions: * out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..55] * * Input Bounds: * arg1: [[0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x1000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x1000000]] * Output Bounds: * out1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff]] */ static void fiat_p448_to_bytes(uint8_t out1[56], const uint32_t arg1[18]) { uint32_t x1; fiat_p448_uint1 x2; uint32_t x3; fiat_p448_uint1 x4; uint32_t x5; fiat_p448_uint1 x6; uint32_t x7; fiat_p448_uint1 x8; uint32_t x9; fiat_p448_uint1 x10; uint32_t x11; fiat_p448_uint1 x12; uint32_t x13; fiat_p448_uint1 x14; uint32_t x15; fiat_p448_uint1 x16; uint32_t x17; fiat_p448_uint1 x18; uint32_t x19; fiat_p448_uint1 x20; uint32_t x21; fiat_p448_uint1 x22; uint32_t x23; fiat_p448_uint1 x24; uint32_t x25; fiat_p448_uint1 x26; uint32_t x27; fiat_p448_uint1 x28; uint32_t x29; fiat_p448_uint1 x30; uint32_t x31; fiat_p448_uint1 x32; uint32_t x33; fiat_p448_uint1 x34; uint32_t x35; fiat_p448_uint1 x36; uint32_t x37; uint32_t x38; fiat_p448_uint1 x39; uint32_t x40; fiat_p448_uint1 x41; uint32_t x42; fiat_p448_uint1 x43; uint32_t x44; fiat_p448_uint1 x45; uint32_t x46; fiat_p448_uint1 x47; uint32_t x48; fiat_p448_uint1 x49; uint32_t x50; fiat_p448_uint1 x51; uint32_t x52; fiat_p448_uint1 x53; uint32_t x54; fiat_p448_uint1 x55; uint32_t x56; fiat_p448_uint1 x57; uint32_t x58; fiat_p448_uint1 x59; uint32_t x60; fiat_p448_uint1 x61; uint32_t x62; fiat_p448_uint1 x63; uint32_t x64; fiat_p448_uint1 x65; uint32_t x66; fiat_p448_uint1 x67; uint32_t x68; fiat_p448_uint1 x69; uint32_t x70; fiat_p448_uint1 x71; uint32_t x72; fiat_p448_uint1 x73; uint32_t x74; uint32_t x75; uint32_t x76; uint32_t x77; uint32_t x78; uint32_t x79; uint32_t x80; uint32_t x81; uint32_t x82; uint32_t x83; uint32_t x84; uint32_t x85; uint32_t x86; uint32_t x87; uint8_t x88; uint32_t x89; uint8_t x90; uint32_t x91; uint8_t x92; fiat_p448_uint1 x93; uint32_t x94; uint8_t x95; uint32_t x96; uint8_t x97; uint32_t x98; uint8_t x99; uint8_t x100; uint32_t x101; uint8_t x102; uint32_t x103; uint8_t x104; uint32_t x105; uint8_t x106; uint8_t x107; uint32_t x108; uint8_t x109; uint32_t x110; uint8_t x111; uint32_t x112; uint8_t x113; uint8_t x114; uint32_t x115; uint8_t x116; uint32_t x117; uint8_t x118; uint32_t x119; uint8_t x120; uint8_t x121; uint32_t x122; uint8_t x123; uint32_t x124; uint8_t x125; uint32_t x126; uint8_t x127; uint8_t x128; uint32_t x129; uint8_t x130; uint32_t x131; uint8_t x132; uint32_t x133; uint8_t x134; uint8_t x135; uint32_t x136; uint8_t x137; uint32_t x138; uint8_t x139; uint32_t x140; uint8_t x141; uint8_t x142; uint8_t x143; uint32_t x144; uint8_t x145; uint8_t x146; uint8_t x147; uint32_t x148; uint8_t x149; uint32_t x150; uint8_t x151; fiat_p448_uint1 x152; uint32_t x153; uint8_t x154; uint32_t x155; uint8_t x156; uint32_t x157; uint8_t x158; uint8_t x159; uint32_t x160; uint8_t x161; uint32_t x162; uint8_t x163; uint32_t x164; uint8_t x165; uint8_t x166; uint32_t x167; uint8_t x168; uint32_t x169; uint8_t x170; uint32_t x171; uint8_t x172; uint8_t x173; uint32_t x174; uint8_t x175; uint32_t x176; uint8_t x177; uint32_t x178; uint8_t x179; uint8_t x180; uint32_t x181; uint8_t x182; uint32_t x183; uint8_t x184; uint32_t x185; uint8_t x186; uint8_t x187; uint32_t x188; uint8_t x189; uint32_t x190; uint8_t x191; uint32_t x192; uint8_t x193; uint8_t x194; uint32_t x195; uint8_t x196; uint32_t x197; uint8_t x198; uint32_t x199; uint8_t x200; uint8_t x201; uint8_t x202; uint32_t x203; uint8_t x204; uint8_t x205; fiat_p448_subborrowx_u25(&x1, &x2, 0x0, (arg1[0]), UINT32_C(0x1ffffff)); fiat_p448_subborrowx_u25(&x3, &x4, x2, (arg1[1]), UINT32_C(0x1ffffff)); fiat_p448_subborrowx_u25(&x5, &x6, x4, (arg1[2]), UINT32_C(0x1ffffff)); fiat_p448_subborrowx_u25(&x7, &x8, x6, (arg1[3]), UINT32_C(0x1ffffff)); fiat_p448_subborrowx_u25(&x9, &x10, x8, (arg1[4]), UINT32_C(0x1ffffff)); fiat_p448_subborrowx_u25(&x11, &x12, x10, (arg1[5]), UINT32_C(0x1ffffff)); fiat_p448_subborrowx_u25(&x13, &x14, x12, (arg1[6]), UINT32_C(0x1ffffff)); fiat_p448_subborrowx_u25(&x15, &x16, x14, (arg1[7]), UINT32_C(0x1ffffff)); fiat_p448_subborrowx_u24(&x17, &x18, x16, (arg1[8]), UINT32_C(0xffffff)); fiat_p448_subborrowx_u25(&x19, &x20, x18, (arg1[9]), UINT32_C(0x1fffffe)); fiat_p448_subborrowx_u25(&x21, &x22, x20, (arg1[10]), UINT32_C(0x1ffffff)); fiat_p448_subborrowx_u25(&x23, &x24, x22, (arg1[11]), UINT32_C(0x1ffffff)); fiat_p448_subborrowx_u25(&x25, &x26, x24, (arg1[12]), UINT32_C(0x1ffffff)); fiat_p448_subborrowx_u25(&x27, &x28, x26, (arg1[13]), UINT32_C(0x1ffffff)); fiat_p448_subborrowx_u25(&x29, &x30, x28, (arg1[14]), UINT32_C(0x1ffffff)); fiat_p448_subborrowx_u25(&x31, &x32, x30, (arg1[15]), UINT32_C(0x1ffffff)); fiat_p448_subborrowx_u25(&x33, &x34, x32, (arg1[16]), UINT32_C(0x1ffffff)); fiat_p448_subborrowx_u24(&x35, &x36, x34, (arg1[17]), UINT32_C(0xffffff)); fiat_p448_cmovznz_u32(&x37, x36, 0x0, UINT32_C(0xffffffff)); fiat_p448_addcarryx_u25(&x38, &x39, 0x0, x1, (x37 & UINT32_C(0x1ffffff))); fiat_p448_addcarryx_u25(&x40, &x41, x39, x3, (x37 & UINT32_C(0x1ffffff))); fiat_p448_addcarryx_u25(&x42, &x43, x41, x5, (x37 & UINT32_C(0x1ffffff))); fiat_p448_addcarryx_u25(&x44, &x45, x43, x7, (x37 & UINT32_C(0x1ffffff))); fiat_p448_addcarryx_u25(&x46, &x47, x45, x9, (x37 & UINT32_C(0x1ffffff))); fiat_p448_addcarryx_u25(&x48, &x49, x47, x11, (x37 & UINT32_C(0x1ffffff))); fiat_p448_addcarryx_u25(&x50, &x51, x49, x13, (x37 & UINT32_C(0x1ffffff))); fiat_p448_addcarryx_u25(&x52, &x53, x51, x15, (x37 & UINT32_C(0x1ffffff))); fiat_p448_addcarryx_u24(&x54, &x55, x53, x17, (x37 & UINT32_C(0xffffff))); fiat_p448_addcarryx_u25(&x56, &x57, x55, x19, (x37 & UINT32_C(0x1fffffe))); fiat_p448_addcarryx_u25(&x58, &x59, x57, x21, (x37 & UINT32_C(0x1ffffff))); fiat_p448_addcarryx_u25(&x60, &x61, x59, x23, (x37 & UINT32_C(0x1ffffff))); fiat_p448_addcarryx_u25(&x62, &x63, x61, x25, (x37 & UINT32_C(0x1ffffff))); fiat_p448_addcarryx_u25(&x64, &x65, x63, x27, (x37 & UINT32_C(0x1ffffff))); fiat_p448_addcarryx_u25(&x66, &x67, x65, x29, (x37 & UINT32_C(0x1ffffff))); fiat_p448_addcarryx_u25(&x68, &x69, x67, x31, (x37 & UINT32_C(0x1ffffff))); fiat_p448_addcarryx_u25(&x70, &x71, x69, x33, (x37 & UINT32_C(0x1ffffff))); fiat_p448_addcarryx_u24(&x72, &x73, x71, x35, (x37 & UINT32_C(0xffffff))); x74 = (x70 << 7); x75 = (x68 << 6); x76 = (x66 << 5); x77 = (x64 << 4); x78 = (x62 << 3); x79 = (x60 << 2); x80 = (x58 * (uint32_t)0x2); x81 = (x52 << 7); x82 = (x50 << 6); x83 = (x48 << 5); x84 = (x46 << 4); x85 = (x44 << 3); x86 = (x42 << 2); x87 = (x40 * (uint32_t)0x2); x88 = (uint8_t)(x38 & UINT8_C(0xff)); x89 = (x38 >> 8); x90 = (uint8_t)(x89 & UINT8_C(0xff)); x91 = (x89 >> 8); x92 = (uint8_t)(x91 & UINT8_C(0xff)); x93 = (fiat_p448_uint1)(x91 >> 8); x94 = (x87 + (uint32_t)x93); x95 = (uint8_t)(x94 & UINT8_C(0xff)); x96 = (x94 >> 8); x97 = (uint8_t)(x96 & UINT8_C(0xff)); x98 = (x96 >> 8); x99 = (uint8_t)(x98 & UINT8_C(0xff)); x100 = (uint8_t)(x98 >> 8); x101 = (x86 + (uint32_t)x100); x102 = (uint8_t)(x101 & UINT8_C(0xff)); x103 = (x101 >> 8); x104 = (uint8_t)(x103 & UINT8_C(0xff)); x105 = (x103 >> 8); x106 = (uint8_t)(x105 & UINT8_C(0xff)); x107 = (uint8_t)(x105 >> 8); x108 = (x85 + (uint32_t)x107); x109 = (uint8_t)(x108 & UINT8_C(0xff)); x110 = (x108 >> 8); x111 = (uint8_t)(x110 & UINT8_C(0xff)); x112 = (x110 >> 8); x113 = (uint8_t)(x112 & UINT8_C(0xff)); x114 = (uint8_t)(x112 >> 8); x115 = (x84 + (uint32_t)x114); x116 = (uint8_t)(x115 & UINT8_C(0xff)); x117 = (x115 >> 8); x118 = (uint8_t)(x117 & UINT8_C(0xff)); x119 = (x117 >> 8); x120 = (uint8_t)(x119 & UINT8_C(0xff)); x121 = (uint8_t)(x119 >> 8); x122 = (x83 + (uint32_t)x121); x123 = (uint8_t)(x122 & UINT8_C(0xff)); x124 = (x122 >> 8); x125 = (uint8_t)(x124 & UINT8_C(0xff)); x126 = (x124 >> 8); x127 = (uint8_t)(x126 & UINT8_C(0xff)); x128 = (uint8_t)(x126 >> 8); x129 = (x82 + (uint32_t)x128); x130 = (uint8_t)(x129 & UINT8_C(0xff)); x131 = (x129 >> 8); x132 = (uint8_t)(x131 & UINT8_C(0xff)); x133 = (x131 >> 8); x134 = (uint8_t)(x133 & UINT8_C(0xff)); x135 = (uint8_t)(x133 >> 8); x136 = (x81 + (uint32_t)x135); x137 = (uint8_t)(x136 & UINT8_C(0xff)); x138 = (x136 >> 8); x139 = (uint8_t)(x138 & UINT8_C(0xff)); x140 = (x138 >> 8); x141 = (uint8_t)(x140 & UINT8_C(0xff)); x142 = (uint8_t)(x140 >> 8); x143 = (uint8_t)(x54 & UINT8_C(0xff)); x144 = (x54 >> 8); x145 = (uint8_t)(x144 & UINT8_C(0xff)); x146 = (uint8_t)(x144 >> 8); x147 = (uint8_t)(x56 & UINT8_C(0xff)); x148 = (x56 >> 8); x149 = (uint8_t)(x148 & UINT8_C(0xff)); x150 = (x148 >> 8); x151 = (uint8_t)(x150 & UINT8_C(0xff)); x152 = (fiat_p448_uint1)(x150 >> 8); x153 = (x80 + (uint32_t)x152); x154 = (uint8_t)(x153 & UINT8_C(0xff)); x155 = (x153 >> 8); x156 = (uint8_t)(x155 & UINT8_C(0xff)); x157 = (x155 >> 8); x158 = (uint8_t)(x157 & UINT8_C(0xff)); x159 = (uint8_t)(x157 >> 8); x160 = (x79 + (uint32_t)x159); x161 = (uint8_t)(x160 & UINT8_C(0xff)); x162 = (x160 >> 8); x163 = (uint8_t)(x162 & UINT8_C(0xff)); x164 = (x162 >> 8); x165 = (uint8_t)(x164 & UINT8_C(0xff)); x166 = (uint8_t)(x164 >> 8); x167 = (x78 + (uint32_t)x166); x168 = (uint8_t)(x167 & UINT8_C(0xff)); x169 = (x167 >> 8); x170 = (uint8_t)(x169 & UINT8_C(0xff)); x171 = (x169 >> 8); x172 = (uint8_t)(x171 & UINT8_C(0xff)); x173 = (uint8_t)(x171 >> 8); x174 = (x77 + (uint32_t)x173); x175 = (uint8_t)(x174 & UINT8_C(0xff)); x176 = (x174 >> 8); x177 = (uint8_t)(x176 & UINT8_C(0xff)); x178 = (x176 >> 8); x179 = (uint8_t)(x178 & UINT8_C(0xff)); x180 = (uint8_t)(x178 >> 8); x181 = (x76 + (uint32_t)x180); x182 = (uint8_t)(x181 & UINT8_C(0xff)); x183 = (x181 >> 8); x184 = (uint8_t)(x183 & UINT8_C(0xff)); x185 = (x183 >> 8); x186 = (uint8_t)(x185 & UINT8_C(0xff)); x187 = (uint8_t)(x185 >> 8); x188 = (x75 + (uint32_t)x187); x189 = (uint8_t)(x188 & UINT8_C(0xff)); x190 = (x188 >> 8); x191 = (uint8_t)(x190 & UINT8_C(0xff)); x192 = (x190 >> 8); x193 = (uint8_t)(x192 & UINT8_C(0xff)); x194 = (uint8_t)(x192 >> 8); x195 = (x74 + (uint32_t)x194); x196 = (uint8_t)(x195 & UINT8_C(0xff)); x197 = (x195 >> 8); x198 = (uint8_t)(x197 & UINT8_C(0xff)); x199 = (x197 >> 8); x200 = (uint8_t)(x199 & UINT8_C(0xff)); x201 = (uint8_t)(x199 >> 8); x202 = (uint8_t)(x72 & UINT8_C(0xff)); x203 = (x72 >> 8); x204 = (uint8_t)(x203 & UINT8_C(0xff)); x205 = (uint8_t)(x203 >> 8); out1[0] = x88; out1[1] = x90; out1[2] = x92; out1[3] = x95; out1[4] = x97; out1[5] = x99; out1[6] = x102; out1[7] = x104; out1[8] = x106; out1[9] = x109; out1[10] = x111; out1[11] = x113; out1[12] = x116; out1[13] = x118; out1[14] = x120; out1[15] = x123; out1[16] = x125; out1[17] = x127; out1[18] = x130; out1[19] = x132; out1[20] = x134; out1[21] = x137; out1[22] = x139; out1[23] = x141; out1[24] = x142; out1[25] = x143; out1[26] = x145; out1[27] = x146; out1[28] = x147; out1[29] = x149; out1[30] = x151; out1[31] = x154; out1[32] = x156; out1[33] = x158; out1[34] = x161; out1[35] = x163; out1[36] = x165; out1[37] = x168; out1[38] = x170; out1[39] = x172; out1[40] = x175; out1[41] = x177; out1[42] = x179; out1[43] = x182; out1[44] = x184; out1[45] = x186; out1[46] = x189; out1[47] = x191; out1[48] = x193; out1[49] = x196; out1[50] = x198; out1[51] = x200; out1[52] = x201; out1[53] = x202; out1[54] = x204; out1[55] = x205; } /* * The function fiat_p448_from_bytes deserializes a field element from bytes in little-endian order. * Postconditions: * eval out1 mod m = bytes_eval arg1 mod m * * Input Bounds: * arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff]] * Output Bounds: * out1: [[0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x1000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x2000000], [0x0 ~> 0x1000000]] */ static void fiat_p448_from_bytes(uint32_t out1[18], const uint8_t arg1[56]) { uint32_t x1; uint32_t x2; uint8_t x3; uint32_t x4; uint32_t x5; uint32_t x6; uint32_t x7; uint32_t x8; uint32_t x9; uint32_t x10; uint32_t x11; uint32_t x12; uint32_t x13; uint32_t x14; uint32_t x15; uint32_t x16; uint32_t x17; uint32_t x18; uint32_t x19; uint32_t x20; uint32_t x21; uint32_t x22; uint32_t x23; uint32_t x24; uint32_t x25; uint32_t x26; uint32_t x27; uint8_t x28; uint32_t x29; uint32_t x30; uint8_t x31; uint32_t x32; uint32_t x33; uint32_t x34; uint32_t x35; uint32_t x36; uint32_t x37; uint32_t x38; uint32_t x39; uint32_t x40; uint32_t x41; uint32_t x42; uint32_t x43; uint32_t x44; uint32_t x45; uint32_t x46; uint32_t x47; uint32_t x48; uint32_t x49; uint32_t x50; uint32_t x51; uint32_t x52; uint32_t x53; uint32_t x54; uint32_t x55; uint8_t x56; uint32_t x57; uint32_t x58; uint32_t x59; uint32_t x60; uint8_t x61; uint32_t x62; uint32_t x63; uint32_t x64; uint32_t x65; uint8_t x66; uint32_t x67; uint32_t x68; uint32_t x69; uint32_t x70; uint8_t x71; uint32_t x72; uint32_t x73; uint32_t x74; uint32_t x75; uint8_t x76; uint32_t x77; uint32_t x78; uint32_t x79; uint32_t x80; uint8_t x81; uint32_t x82; uint32_t x83; uint32_t x84; uint32_t x85; uint8_t x86; uint32_t x87; uint32_t x88; uint32_t x89; uint32_t x90; fiat_p448_uint1 x91; uint32_t x92; uint32_t x93; uint32_t x94; uint32_t x95; uint32_t x96; uint32_t x97; uint32_t x98; uint32_t x99; uint32_t x100; uint8_t x101; uint32_t x102; uint32_t x103; uint32_t x104; uint32_t x105; uint8_t x106; uint32_t x107; uint32_t x108; uint32_t x109; uint32_t x110; uint8_t x111; uint32_t x112; uint32_t x113; uint32_t x114; uint32_t x115; uint8_t x116; uint32_t x117; uint32_t x118; uint32_t x119; uint32_t x120; uint8_t x121; uint32_t x122; uint32_t x123; uint32_t x124; uint32_t x125; uint8_t x126; uint32_t x127; uint32_t x128; uint32_t x129; uint32_t x130; fiat_p448_uint1 x131; uint32_t x132; uint32_t x133; uint32_t x134; uint32_t x135; uint32_t x136; x1 = ((uint32_t)(arg1[55]) << 16); x2 = ((uint32_t)(arg1[54]) << 8); x3 = (arg1[53]); x4 = ((uint32_t)(arg1[52]) << 17); x5 = ((uint32_t)(arg1[51]) << 9); x6 = ((uint32_t)(arg1[50]) * 0x2); x7 = ((uint32_t)(arg1[49]) << 18); x8 = ((uint32_t)(arg1[48]) << 10); x9 = ((uint32_t)(arg1[47]) << 2); x10 = ((uint32_t)(arg1[46]) << 19); x11 = ((uint32_t)(arg1[45]) << 11); x12 = ((uint32_t)(arg1[44]) << 3); x13 = ((uint32_t)(arg1[43]) << 20); x14 = ((uint32_t)(arg1[42]) << 12); x15 = ((uint32_t)(arg1[41]) << 4); x16 = ((uint32_t)(arg1[40]) << 21); x17 = ((uint32_t)(arg1[39]) << 13); x18 = ((uint32_t)(arg1[38]) << 5); x19 = ((uint32_t)(arg1[37]) << 22); x20 = ((uint32_t)(arg1[36]) << 14); x21 = ((uint32_t)(arg1[35]) << 6); x22 = ((uint32_t)(arg1[34]) << 23); x23 = ((uint32_t)(arg1[33]) << 15); x24 = ((uint32_t)(arg1[32]) << 7); x25 = ((uint32_t)(arg1[31]) << 24); x26 = ((uint32_t)(arg1[30]) << 16); x27 = ((uint32_t)(arg1[29]) << 8); x28 = (arg1[28]); x29 = ((uint32_t)(arg1[27]) << 16); x30 = ((uint32_t)(arg1[26]) << 8); x31 = (arg1[25]); x32 = ((uint32_t)(arg1[24]) << 17); x33 = ((uint32_t)(arg1[23]) << 9); x34 = ((uint32_t)(arg1[22]) * 0x2); x35 = ((uint32_t)(arg1[21]) << 18); x36 = ((uint32_t)(arg1[20]) << 10); x37 = ((uint32_t)(arg1[19]) << 2); x38 = ((uint32_t)(arg1[18]) << 19); x39 = ((uint32_t)(arg1[17]) << 11); x40 = ((uint32_t)(arg1[16]) << 3); x41 = ((uint32_t)(arg1[15]) << 20); x42 = ((uint32_t)(arg1[14]) << 12); x43 = ((uint32_t)(arg1[13]) << 4); x44 = ((uint32_t)(arg1[12]) << 21); x45 = ((uint32_t)(arg1[11]) << 13); x46 = ((uint32_t)(arg1[10]) << 5); x47 = ((uint32_t)(arg1[9]) << 22); x48 = ((uint32_t)(arg1[8]) << 14); x49 = ((uint32_t)(arg1[7]) << 6); x50 = ((uint32_t)(arg1[6]) << 23); x51 = ((uint32_t)(arg1[5]) << 15); x52 = ((uint32_t)(arg1[4]) << 7); x53 = ((uint32_t)(arg1[3]) << 24); x54 = ((uint32_t)(arg1[2]) << 16); x55 = ((uint32_t)(arg1[1]) << 8); x56 = (arg1[0]); x57 = (x55 + (uint32_t)x56); x58 = (x54 + x57); x59 = (x53 + x58); x60 = (x59 & UINT32_C(0x1ffffff)); x61 = (uint8_t)(x59 >> 25); x62 = (x52 + (uint32_t)x61); x63 = (x51 + x62); x64 = (x50 + x63); x65 = (x64 & UINT32_C(0x1ffffff)); x66 = (uint8_t)(x64 >> 25); x67 = (x49 + (uint32_t)x66); x68 = (x48 + x67); x69 = (x47 + x68); x70 = (x69 & UINT32_C(0x1ffffff)); x71 = (uint8_t)(x69 >> 25); x72 = (x46 + (uint32_t)x71); x73 = (x45 + x72); x74 = (x44 + x73); x75 = (x74 & UINT32_C(0x1ffffff)); x76 = (uint8_t)(x74 >> 25); x77 = (x43 + (uint32_t)x76); x78 = (x42 + x77); x79 = (x41 + x78); x80 = (x79 & UINT32_C(0x1ffffff)); x81 = (uint8_t)(x79 >> 25); x82 = (x40 + (uint32_t)x81); x83 = (x39 + x82); x84 = (x38 + x83); x85 = (x84 & UINT32_C(0x1ffffff)); x86 = (uint8_t)(x84 >> 25); x87 = (x37 + (uint32_t)x86); x88 = (x36 + x87); x89 = (x35 + x88); x90 = (x89 & UINT32_C(0x1ffffff)); x91 = (fiat_p448_uint1)(x89 >> 25); x92 = (x34 + (uint32_t)x91); x93 = (x33 + x92); x94 = (x32 + x93); x95 = (x30 + (uint32_t)x31); x96 = (x29 + x95); x97 = (x27 + (uint32_t)x28); x98 = (x26 + x97); x99 = (x25 + x98); x100 = (x99 & UINT32_C(0x1ffffff)); x101 = (uint8_t)(x99 >> 25); x102 = (x24 + (uint32_t)x101); x103 = (x23 + x102); x104 = (x22 + x103); x105 = (x104 & UINT32_C(0x1ffffff)); x106 = (uint8_t)(x104 >> 25); x107 = (x21 + (uint32_t)x106); x108 = (x20 + x107); x109 = (x19 + x108); x110 = (x109 & UINT32_C(0x1ffffff)); x111 = (uint8_t)(x109 >> 25); x112 = (x18 + (uint32_t)x111); x113 = (x17 + x112); x114 = (x16 + x113); x115 = (x114 & UINT32_C(0x1ffffff)); x116 = (uint8_t)(x114 >> 25); x117 = (x15 + (uint32_t)x116); x118 = (x14 + x117); x119 = (x13 + x118); x120 = (x119 & UINT32_C(0x1ffffff)); x121 = (uint8_t)(x119 >> 25); x122 = (x12 + (uint32_t)x121); x123 = (x11 + x122); x124 = (x10 + x123); x125 = (x124 & UINT32_C(0x1ffffff)); x126 = (uint8_t)(x124 >> 25); x127 = (x9 + (uint32_t)x126); x128 = (x8 + x127); x129 = (x7 + x128); x130 = (x129 & UINT32_C(0x1ffffff)); x131 = (fiat_p448_uint1)(x129 >> 25); x132 = (x6 + (uint32_t)x131); x133 = (x5 + x132); x134 = (x4 + x133); x135 = (x2 + (uint32_t)x3); x136 = (x1 + x135); out1[0] = x60; out1[1] = x65; out1[2] = x70; out1[3] = x75; out1[4] = x80; out1[5] = x85; out1[6] = x90; out1[7] = x94; out1[8] = x96; out1[9] = x100; out1[10] = x105; out1[11] = x110; out1[12] = x115; out1[13] = x120; out1[14] = x125; out1[15] = x130; out1[16] = x134; out1[17] = x136; }