p448_solinas_64.c

/* Autogenerated: src/ExtractionOCaml/bedrock2_unsaturated_solinas --lang bedrock2 --static --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select p448 64 8 '2^448 - 2^224 - 1' carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes */
/* curve description: p448 */
/* machine_wordsize = 64 (from "64") */
/* requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes */
/* n = 8 (from "8") */
/* s-c = 2^448 - [(2^224, 1), (1, 1)] (from "2^448 - 2^224 - 1") */
/* tight_bounds_multiplier = 1 (from "") */
/*  */
/* Computed values: */
/* carry_chain = [3, 7, 4, 0, 5, 1, 6, 2, 7, 3, 4, 0] */
/* eval z = z[0] + (z[1] << 56) + (z[2] << 112) + (z[3] << 168) + (z[4] << 224) + (z[5] << 0x118) + (z[6] << 0x150) + (z[7] << 0x188) */
/* 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 = [0x1fffffffffffffe, 0x1fffffffffffffe, 0x1fffffffffffffe, 0x1fffffffffffffe, 0x1fffffffffffffc, 0x1fffffffffffffe, 0x1fffffffffffffe, 0x1fffffffffffffe] */

#include <stdint.h>
#include <memory.h>

// LITTLE-ENDIAN memory access is REQUIRED
// the following two functions are required to work around -fstrict-aliasing
static inline uintptr_t _br2_load(uintptr_t a, size_t sz) {
  uintptr_t r = 0;
  memcpy(&r, (void*)a, sz);
  return r;
}

static inline void _br2_store(uintptr_t a, uintptr_t v, size_t sz) {
  memcpy((void*)a, &v, sz);
}



/*
 * Input Bounds:
 *   in0: [[0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000]]
 *   in1: [[0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000]]
 * Output Bounds:
 *   out0: [[0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000]]
 */
static
void internal_fiat_p448_carry_mul(uintptr_t out0, uintptr_t in0, uintptr_t in1) {
  uintptr_t x7, x6, x5, x4, x3, x2, x1, x15, x14, x13, x12, x11, x10, x9, x0, x8, x46, x58, x213, x59, x214, x47, x212, x68, x217, x69, x218, x215, x216, x76, x221, x77, x222, x219, x220, x168, x225, x169, x226, x223, x224, x178, x229, x179, x230, x227, x228, x190, x233, x191, x234, x231, x232, x204, x237, x205, x238, x235, x239, x236, x96, x104, x243, x105, x244, x97, x242, x112, x247, x113, x248, x245, x246, x120, x251, x121, x252, x249, x250, x140, x255, x141, x256, x253, x254, x142, x259, x143, x260, x257, x258, x146, x263, x147, x264, x261, x262, x152, x267, x153, x268, x265, x266, x160, x271, x161, x272, x269, x270, x170, x275, x171, x276, x273, x274, x182, x279, x183, x280, x277, x278, x196, x283, x197, x284, x281, x28, x40, x287, x41, x288, x29, x286, x98, x291, x99, x292, x289, x290, x106, x295, x107, x296, x293, x294, x114, x299, x115, x300, x297, x298, x122, x303, x123, x304, x301, x302, x128, x307, x129, x308, x305, x306, x144, x311, x145, x312, x309, x310, x148, x315, x149, x316, x313, x314, x154, x319, x155, x320, x317, x318, x162, x323, x163, x324, x321, x322, x172, x327, x173, x328, x325, x326, x184, x331, x185, x332, x329, x330, x198, x335, x199, x336, x333, x30, x34, x339, x35, x340, x31, x338, x42, x343, x43, x344, x341, x342, x54, x347, x55, x348, x345, x346, x100, x351, x101, x352, x349, x350, x108, x355, x109, x356, x353, x354, x116, x359, x117, x360, x357, x358, x124, x363, x125, x364, x361, x362, x130, x367, x131, x368, x365, x366, x134, x371, x135, x372, x369, x370, x150, x375, x151, x376, x373, x374, x156, x379, x157, x380, x377, x378, x164, x383, x165, x384, x381, x382, x174, x387, x175, x388, x385, x386, x186, x391, x187, x392, x389, x390, x200, x395, x201, x396, x393, x32, x36, x399, x37, x400, x33, x398, x38, x403, x39, x404, x401, x402, x44, x407, x45, x408, x405, x406, x56, x411, x57, x412, x409, x410, x66, x415, x67, x416, x413, x414, x102, x419, x103, x420, x417, x418, x110, x423, x111, x424, x421, x422, x118, x427, x119, x428, x425, x426, x126, x431, x127, x432, x429, x430, x132, x435, x133, x436, x433, x434, x136, x439, x137, x440, x437, x438, x138, x443, x139, x444, x441, x442, x158, x447, x159, x448, x445, x446, x166, x451, x167, x452, x449, x450, x176, x455, x177, x456, x453, x454, x188, x459, x189, x460, x457, x458, x202, x463, x203, x464, x461, x16, x48, x467, x49, x468, x17, x466, x60, x471, x61, x472, x469, x470, x70, x475, x71, x476, x473, x474, x78, x479, x79, x480, x477, x478, x84, x483, x85, x484, x481, x482, x180, x487, x181, x488, x485, x486, x192, x491, x193, x492, x489, x490, x206, x495, x207, x496, x493, x18, x22, x499, x23, x500, x19, x498, x50, x503, x51, x504, x501, x502, x62, x507, x63, x508, x505, x506, x72, x511, x73, x512, x509, x510, x80, x515, x81, x516, x513, x514, x86, x519, x87, x520, x517, x518, x90, x523, x91, x524, x521, x522, x194, x527, x195, x528, x525, x526, x208, x531, x209, x532, x529, x20, x24, x535, x25, x536, x21, x534, x26, x539, x27, x540, x537, x538, x52, x543, x53, x544, x541, x542, x64, x547, x65, x548, x545, x546, x74, x551, x75, x552, x549, x550, x82, x555, x83, x556, x553, x554, x88, x559, x89, x560, x557, x558, x92, x563, x93, x564, x561, x562, x94, x567, x95, x568, x565, x566, x210, x571, x211, x572, x569, x462, x240, x575, x465, x285, x282, x574, x580, x576, x581, x579, x577, x570, x585, x573, x394, x582, x588, x397, x586, x584, x530, x590, x593, x533, x589, x587, x334, x595, x598, x337, x594, x592, x494, x600, x603, x497, x599, x597, x605, x578, x604, x602, x608, x241, x607, x610, x583, x591, x611, x613, x615, x617, x618, x596, x616, x621, x601, x622, x623, x609, x614, x619, x620, x606, x612, x624, x625, x626, x627, x628, x629, x630, x631;
  x0 = _br2_load((in0)+((uintptr_t)0ULL), sizeof(uintptr_t));
  x1 = _br2_load((in0)+((uintptr_t)8ULL), sizeof(uintptr_t));
  x2 = _br2_load((in0)+((uintptr_t)16ULL), sizeof(uintptr_t));
  x3 = _br2_load((in0)+((uintptr_t)24ULL), sizeof(uintptr_t));
  x4 = _br2_load((in0)+((uintptr_t)32ULL), sizeof(uintptr_t));
  x5 = _br2_load((in0)+((uintptr_t)40ULL), sizeof(uintptr_t));
  x6 = _br2_load((in0)+((uintptr_t)48ULL), sizeof(uintptr_t));
  x7 = _br2_load((in0)+((uintptr_t)56ULL), sizeof(uintptr_t));
  /*skip*/
  x8 = _br2_load((in1)+((uintptr_t)0ULL), sizeof(uintptr_t));
  x9 = _br2_load((in1)+((uintptr_t)8ULL), sizeof(uintptr_t));
  x10 = _br2_load((in1)+((uintptr_t)16ULL), sizeof(uintptr_t));
  x11 = _br2_load((in1)+((uintptr_t)24ULL), sizeof(uintptr_t));
  x12 = _br2_load((in1)+((uintptr_t)32ULL), sizeof(uintptr_t));
  x13 = _br2_load((in1)+((uintptr_t)40ULL), sizeof(uintptr_t));
  x14 = _br2_load((in1)+((uintptr_t)48ULL), sizeof(uintptr_t));
  x15 = _br2_load((in1)+((uintptr_t)56ULL), sizeof(uintptr_t));
  /*skip*/
  /*skip*/
  x16 = (x7)*(x15);
  x17 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*(x15))>>32 : ((__uint128_t)(x7)*(x15))>>64;
  x18 = (x7)*(x14);
  x19 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*(x14))>>32 : ((__uint128_t)(x7)*(x14))>>64;
  x20 = (x7)*(x13);
  x21 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*(x13))>>32 : ((__uint128_t)(x7)*(x13))>>64;
  x22 = (x6)*(x15);
  x23 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*(x15))>>32 : ((__uint128_t)(x6)*(x15))>>64;
  x24 = (x6)*(x14);
  x25 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*(x14))>>32 : ((__uint128_t)(x6)*(x14))>>64;
  x26 = (x5)*(x15);
  x27 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*(x15))>>32 : ((__uint128_t)(x5)*(x15))>>64;
  x28 = (x7)*(x15);
  x29 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*(x15))>>32 : ((__uint128_t)(x7)*(x15))>>64;
  x30 = (x7)*(x14);
  x31 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*(x14))>>32 : ((__uint128_t)(x7)*(x14))>>64;
  x32 = (x7)*(x13);
  x33 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*(x13))>>32 : ((__uint128_t)(x7)*(x13))>>64;
  x34 = (x6)*(x15);
  x35 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*(x15))>>32 : ((__uint128_t)(x6)*(x15))>>64;
  x36 = (x6)*(x14);
  x37 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*(x14))>>32 : ((__uint128_t)(x6)*(x14))>>64;
  x38 = (x5)*(x15);
  x39 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*(x15))>>32 : ((__uint128_t)(x5)*(x15))>>64;
  x40 = (x7)*(x15);
  x41 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*(x15))>>32 : ((__uint128_t)(x7)*(x15))>>64;
  x42 = (x7)*(x14);
  x43 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*(x14))>>32 : ((__uint128_t)(x7)*(x14))>>64;
  x44 = (x7)*(x13);
  x45 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*(x13))>>32 : ((__uint128_t)(x7)*(x13))>>64;
  x46 = (x7)*(x12);
  x47 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*(x12))>>32 : ((__uint128_t)(x7)*(x12))>>64;
  x48 = (x7)*(x11);
  x49 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*(x11))>>32 : ((__uint128_t)(x7)*(x11))>>64;
  x50 = (x7)*(x10);
  x51 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*(x10))>>32 : ((__uint128_t)(x7)*(x10))>>64;
  x52 = (x7)*(x9);
  x53 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*(x9))>>32 : ((__uint128_t)(x7)*(x9))>>64;
  x54 = (x6)*(x15);
  x55 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*(x15))>>32 : ((__uint128_t)(x6)*(x15))>>64;
  x56 = (x6)*(x14);
  x57 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*(x14))>>32 : ((__uint128_t)(x6)*(x14))>>64;
  x58 = (x6)*(x13);
  x59 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*(x13))>>32 : ((__uint128_t)(x6)*(x13))>>64;
  x60 = (x6)*(x12);
  x61 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*(x12))>>32 : ((__uint128_t)(x6)*(x12))>>64;
  x62 = (x6)*(x11);
  x63 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*(x11))>>32 : ((__uint128_t)(x6)*(x11))>>64;
  x64 = (x6)*(x10);
  x65 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*(x10))>>32 : ((__uint128_t)(x6)*(x10))>>64;
  x66 = (x5)*(x15);
  x67 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*(x15))>>32 : ((__uint128_t)(x5)*(x15))>>64;
  x68 = (x5)*(x14);
  x69 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*(x14))>>32 : ((__uint128_t)(x5)*(x14))>>64;
  x70 = (x5)*(x13);
  x71 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*(x13))>>32 : ((__uint128_t)(x5)*(x13))>>64;
  x72 = (x5)*(x12);
  x73 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*(x12))>>32 : ((__uint128_t)(x5)*(x12))>>64;
  x74 = (x5)*(x11);
  x75 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*(x11))>>32 : ((__uint128_t)(x5)*(x11))>>64;
  x76 = (x4)*(x15);
  x77 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*(x15))>>32 : ((__uint128_t)(x4)*(x15))>>64;
  x78 = (x4)*(x14);
  x79 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*(x14))>>32 : ((__uint128_t)(x4)*(x14))>>64;
  x80 = (x4)*(x13);
  x81 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*(x13))>>32 : ((__uint128_t)(x4)*(x13))>>64;
  x82 = (x4)*(x12);
  x83 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*(x12))>>32 : ((__uint128_t)(x4)*(x12))>>64;
  x84 = (x3)*(x15);
  x85 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*(x15))>>32 : ((__uint128_t)(x3)*(x15))>>64;
  x86 = (x3)*(x14);
  x87 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*(x14))>>32 : ((__uint128_t)(x3)*(x14))>>64;
  x88 = (x3)*(x13);
  x89 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*(x13))>>32 : ((__uint128_t)(x3)*(x13))>>64;
  x90 = (x2)*(x15);
  x91 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*(x15))>>32 : ((__uint128_t)(x2)*(x15))>>64;
  x92 = (x2)*(x14);
  x93 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*(x14))>>32 : ((__uint128_t)(x2)*(x14))>>64;
  x94 = (x1)*(x15);
  x95 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x15))>>32 : ((__uint128_t)(x1)*(x15))>>64;
  x96 = (x7)*(x12);
  x97 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*(x12))>>32 : ((__uint128_t)(x7)*(x12))>>64;
  x98 = (x7)*(x11);
  x99 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*(x11))>>32 : ((__uint128_t)(x7)*(x11))>>64;
  x100 = (x7)*(x10);
  x101 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*(x10))>>32 : ((__uint128_t)(x7)*(x10))>>64;
  x102 = (x7)*(x9);
  x103 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*(x9))>>32 : ((__uint128_t)(x7)*(x9))>>64;
  x104 = (x6)*(x13);
  x105 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*(x13))>>32 : ((__uint128_t)(x6)*(x13))>>64;
  x106 = (x6)*(x12);
  x107 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*(x12))>>32 : ((__uint128_t)(x6)*(x12))>>64;
  x108 = (x6)*(x11);
  x109 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*(x11))>>32 : ((__uint128_t)(x6)*(x11))>>64;
  x110 = (x6)*(x10);
  x111 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*(x10))>>32 : ((__uint128_t)(x6)*(x10))>>64;
  x112 = (x5)*(x14);
  x113 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*(x14))>>32 : ((__uint128_t)(x5)*(x14))>>64;
  x114 = (x5)*(x13);
  x115 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*(x13))>>32 : ((__uint128_t)(x5)*(x13))>>64;
  x116 = (x5)*(x12);
  x117 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*(x12))>>32 : ((__uint128_t)(x5)*(x12))>>64;
  x118 = (x5)*(x11);
  x119 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*(x11))>>32 : ((__uint128_t)(x5)*(x11))>>64;
  x120 = (x4)*(x15);
  x121 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*(x15))>>32 : ((__uint128_t)(x4)*(x15))>>64;
  x122 = (x4)*(x14);
  x123 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*(x14))>>32 : ((__uint128_t)(x4)*(x14))>>64;
  x124 = (x4)*(x13);
  x125 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*(x13))>>32 : ((__uint128_t)(x4)*(x13))>>64;
  x126 = (x4)*(x12);
  x127 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*(x12))>>32 : ((__uint128_t)(x4)*(x12))>>64;
  x128 = (x3)*(x15);
  x129 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*(x15))>>32 : ((__uint128_t)(x3)*(x15))>>64;
  x130 = (x3)*(x14);
  x131 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*(x14))>>32 : ((__uint128_t)(x3)*(x14))>>64;
  x132 = (x3)*(x13);
  x133 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*(x13))>>32 : ((__uint128_t)(x3)*(x13))>>64;
  x134 = (x2)*(x15);
  x135 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*(x15))>>32 : ((__uint128_t)(x2)*(x15))>>64;
  x136 = (x2)*(x14);
  x137 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*(x14))>>32 : ((__uint128_t)(x2)*(x14))>>64;
  x138 = (x1)*(x15);
  x139 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x15))>>32 : ((__uint128_t)(x1)*(x15))>>64;
  x140 = (x7)*(x8);
  x141 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*(x8))>>32 : ((__uint128_t)(x7)*(x8))>>64;
  x142 = (x6)*(x9);
  x143 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*(x9))>>32 : ((__uint128_t)(x6)*(x9))>>64;
  x144 = (x6)*(x8);
  x145 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*(x8))>>32 : ((__uint128_t)(x6)*(x8))>>64;
  x146 = (x5)*(x10);
  x147 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*(x10))>>32 : ((__uint128_t)(x5)*(x10))>>64;
  x148 = (x5)*(x9);
  x149 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*(x9))>>32 : ((__uint128_t)(x5)*(x9))>>64;
  x150 = (x5)*(x8);
  x151 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*(x8))>>32 : ((__uint128_t)(x5)*(x8))>>64;
  x152 = (x4)*(x11);
  x153 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*(x11))>>32 : ((__uint128_t)(x4)*(x11))>>64;
  x154 = (x4)*(x10);
  x155 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*(x10))>>32 : ((__uint128_t)(x4)*(x10))>>64;
  x156 = (x4)*(x9);
  x157 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*(x9))>>32 : ((__uint128_t)(x4)*(x9))>>64;
  x158 = (x4)*(x8);
  x159 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*(x8))>>32 : ((__uint128_t)(x4)*(x8))>>64;
  x160 = (x3)*(x12);
  x161 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*(x12))>>32 : ((__uint128_t)(x3)*(x12))>>64;
  x162 = (x3)*(x11);
  x163 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*(x11))>>32 : ((__uint128_t)(x3)*(x11))>>64;
  x164 = (x3)*(x10);
  x165 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*(x10))>>32 : ((__uint128_t)(x3)*(x10))>>64;
  x166 = (x3)*(x9);
  x167 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*(x9))>>32 : ((__uint128_t)(x3)*(x9))>>64;
  x168 = (x3)*(x8);
  x169 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*(x8))>>32 : ((__uint128_t)(x3)*(x8))>>64;
  x170 = (x2)*(x13);
  x171 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*(x13))>>32 : ((__uint128_t)(x2)*(x13))>>64;
  x172 = (x2)*(x12);
  x173 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*(x12))>>32 : ((__uint128_t)(x2)*(x12))>>64;
  x174 = (x2)*(x11);
  x175 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*(x11))>>32 : ((__uint128_t)(x2)*(x11))>>64;
  x176 = (x2)*(x10);
  x177 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*(x10))>>32 : ((__uint128_t)(x2)*(x10))>>64;
  x178 = (x2)*(x9);
  x179 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*(x9))>>32 : ((__uint128_t)(x2)*(x9))>>64;
  x180 = (x2)*(x8);
  x181 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*(x8))>>32 : ((__uint128_t)(x2)*(x8))>>64;
  x182 = (x1)*(x14);
  x183 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x14))>>32 : ((__uint128_t)(x1)*(x14))>>64;
  x184 = (x1)*(x13);
  x185 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x13))>>32 : ((__uint128_t)(x1)*(x13))>>64;
  x186 = (x1)*(x12);
  x187 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x12))>>32 : ((__uint128_t)(x1)*(x12))>>64;
  x188 = (x1)*(x11);
  x189 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x11))>>32 : ((__uint128_t)(x1)*(x11))>>64;
  x190 = (x1)*(x10);
  x191 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x10))>>32 : ((__uint128_t)(x1)*(x10))>>64;
  x192 = (x1)*(x9);
  x193 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x9))>>32 : ((__uint128_t)(x1)*(x9))>>64;
  x194 = (x1)*(x8);
  x195 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x8))>>32 : ((__uint128_t)(x1)*(x8))>>64;
  x196 = (x0)*(x15);
  x197 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x15))>>32 : ((__uint128_t)(x0)*(x15))>>64;
  x198 = (x0)*(x14);
  x199 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x14))>>32 : ((__uint128_t)(x0)*(x14))>>64;
  x200 = (x0)*(x13);
  x201 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x13))>>32 : ((__uint128_t)(x0)*(x13))>>64;
  x202 = (x0)*(x12);
  x203 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x12))>>32 : ((__uint128_t)(x0)*(x12))>>64;
  x204 = (x0)*(x11);
  x205 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x11))>>32 : ((__uint128_t)(x0)*(x11))>>64;
  x206 = (x0)*(x10);
  x207 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x10))>>32 : ((__uint128_t)(x0)*(x10))>>64;
  x208 = (x0)*(x9);
  x209 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x9))>>32 : ((__uint128_t)(x0)*(x9))>>64;
  x210 = (x0)*(x8);
  x211 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x8))>>32 : ((__uint128_t)(x0)*(x8))>>64;
  x212 = (x58)+(x46);
  x213 = (x212)<(x58);
  x214 = (x213)+(x59);
  x215 = (x214)+(x47);
  x216 = (x68)+(x212);
  x217 = (x216)<(x68);
  x218 = (x217)+(x69);
  x219 = (x218)+(x215);
  x220 = (x76)+(x216);
  x221 = (x220)<(x76);
  x222 = (x221)+(x77);
  x223 = (x222)+(x219);
  x224 = (x168)+(x220);
  x225 = (x224)<(x168);
  x226 = (x225)+(x169);
  x227 = (x226)+(x223);
  x228 = (x178)+(x224);
  x229 = (x228)<(x178);
  x230 = (x229)+(x179);
  x231 = (x230)+(x227);
  x232 = (x190)+(x228);
  x233 = (x232)<(x190);
  x234 = (x233)+(x191);
  x235 = (x234)+(x231);
  x236 = (x204)+(x232);
  x237 = (x236)<(x204);
  x238 = (x237)+(x205);
  x239 = (x238)+(x235);
  x240 = ((x236)>>((uintptr_t)56ULL))|((x239)<<((uintptr_t)8ULL));
  x241 = (x236)&((uintptr_t)72057594037927935ULL);
  x242 = (x104)+(x96);
  x243 = (x242)<(x104);
  x244 = (x243)+(x105);
  x245 = (x244)+(x97);
  x246 = (x112)+(x242);
  x247 = (x246)<(x112);
  x248 = (x247)+(x113);
  x249 = (x248)+(x245);
  x250 = (x120)+(x246);
  x251 = (x250)<(x120);
  x252 = (x251)+(x121);
  x253 = (x252)+(x249);
  x254 = (x140)+(x250);
  x255 = (x254)<(x140);
  x256 = (x255)+(x141);
  x257 = (x256)+(x253);
  x258 = (x142)+(x254);
  x259 = (x258)<(x142);
  x260 = (x259)+(x143);
  x261 = (x260)+(x257);
  x262 = (x146)+(x258);
  x263 = (x262)<(x146);
  x264 = (x263)+(x147);
  x265 = (x264)+(x261);
  x266 = (x152)+(x262);
  x267 = (x266)<(x152);
  x268 = (x267)+(x153);
  x269 = (x268)+(x265);
  x270 = (x160)+(x266);
  x271 = (x270)<(x160);
  x272 = (x271)+(x161);
  x273 = (x272)+(x269);
  x274 = (x170)+(x270);
  x275 = (x274)<(x170);
  x276 = (x275)+(x171);
  x277 = (x276)+(x273);
  x278 = (x182)+(x274);
  x279 = (x278)<(x182);
  x280 = (x279)+(x183);
  x281 = (x280)+(x277);
  x282 = (x196)+(x278);
  x283 = (x282)<(x196);
  x284 = (x283)+(x197);
  x285 = (x284)+(x281);
  x286 = (x40)+(x28);
  x287 = (x286)<(x40);
  x288 = (x287)+(x41);
  x289 = (x288)+(x29);
  x290 = (x98)+(x286);
  x291 = (x290)<(x98);
  x292 = (x291)+(x99);
  x293 = (x292)+(x289);
  x294 = (x106)+(x290);
  x295 = (x294)<(x106);
  x296 = (x295)+(x107);
  x297 = (x296)+(x293);
  x298 = (x114)+(x294);
  x299 = (x298)<(x114);
  x300 = (x299)+(x115);
  x301 = (x300)+(x297);
  x302 = (x122)+(x298);
  x303 = (x302)<(x122);
  x304 = (x303)+(x123);
  x305 = (x304)+(x301);
  x306 = (x128)+(x302);
  x307 = (x306)<(x128);
  x308 = (x307)+(x129);
  x309 = (x308)+(x305);
  x310 = (x144)+(x306);
  x311 = (x310)<(x144);
  x312 = (x311)+(x145);
  x313 = (x312)+(x309);
  x314 = (x148)+(x310);
  x315 = (x314)<(x148);
  x316 = (x315)+(x149);
  x317 = (x316)+(x313);
  x318 = (x154)+(x314);
  x319 = (x318)<(x154);
  x320 = (x319)+(x155);
  x321 = (x320)+(x317);
  x322 = (x162)+(x318);
  x323 = (x322)<(x162);
  x324 = (x323)+(x163);
  x325 = (x324)+(x321);
  x326 = (x172)+(x322);
  x327 = (x326)<(x172);
  x328 = (x327)+(x173);
  x329 = (x328)+(x325);
  x330 = (x184)+(x326);
  x331 = (x330)<(x184);
  x332 = (x331)+(x185);
  x333 = (x332)+(x329);
  x334 = (x198)+(x330);
  x335 = (x334)<(x198);
  x336 = (x335)+(x199);
  x337 = (x336)+(x333);
  x338 = (x34)+(x30);
  x339 = (x338)<(x34);
  x340 = (x339)+(x35);
  x341 = (x340)+(x31);
  x342 = (x42)+(x338);
  x343 = (x342)<(x42);
  x344 = (x343)+(x43);
  x345 = (x344)+(x341);
  x346 = (x54)+(x342);
  x347 = (x346)<(x54);
  x348 = (x347)+(x55);
  x349 = (x348)+(x345);
  x350 = (x100)+(x346);
  x351 = (x350)<(x100);
  x352 = (x351)+(x101);
  x353 = (x352)+(x349);
  x354 = (x108)+(x350);
  x355 = (x354)<(x108);
  x356 = (x355)+(x109);
  x357 = (x356)+(x353);
  x358 = (x116)+(x354);
  x359 = (x358)<(x116);
  x360 = (x359)+(x117);
  x361 = (x360)+(x357);
  x362 = (x124)+(x358);
  x363 = (x362)<(x124);
  x364 = (x363)+(x125);
  x365 = (x364)+(x361);
  x366 = (x130)+(x362);
  x367 = (x366)<(x130);
  x368 = (x367)+(x131);
  x369 = (x368)+(x365);
  x370 = (x134)+(x366);
  x371 = (x370)<(x134);
  x372 = (x371)+(x135);
  x373 = (x372)+(x369);
  x374 = (x150)+(x370);
  x375 = (x374)<(x150);
  x376 = (x375)+(x151);
  x377 = (x376)+(x373);
  x378 = (x156)+(x374);
  x379 = (x378)<(x156);
  x380 = (x379)+(x157);
  x381 = (x380)+(x377);
  x382 = (x164)+(x378);
  x383 = (x382)<(x164);
  x384 = (x383)+(x165);
  x385 = (x384)+(x381);
  x386 = (x174)+(x382);
  x387 = (x386)<(x174);
  x388 = (x387)+(x175);
  x389 = (x388)+(x385);
  x390 = (x186)+(x386);
  x391 = (x390)<(x186);
  x392 = (x391)+(x187);
  x393 = (x392)+(x389);
  x394 = (x200)+(x390);
  x395 = (x394)<(x200);
  x396 = (x395)+(x201);
  x397 = (x396)+(x393);
  x398 = (x36)+(x32);
  x399 = (x398)<(x36);
  x400 = (x399)+(x37);
  x401 = (x400)+(x33);
  x402 = (x38)+(x398);
  x403 = (x402)<(x38);
  x404 = (x403)+(x39);
  x405 = (x404)+(x401);
  x406 = (x44)+(x402);
  x407 = (x406)<(x44);
  x408 = (x407)+(x45);
  x409 = (x408)+(x405);
  x410 = (x56)+(x406);
  x411 = (x410)<(x56);
  x412 = (x411)+(x57);
  x413 = (x412)+(x409);
  x414 = (x66)+(x410);
  x415 = (x414)<(x66);
  x416 = (x415)+(x67);
  x417 = (x416)+(x413);
  x418 = (x102)+(x414);
  x419 = (x418)<(x102);
  x420 = (x419)+(x103);
  x421 = (x420)+(x417);
  x422 = (x110)+(x418);
  x423 = (x422)<(x110);
  x424 = (x423)+(x111);
  x425 = (x424)+(x421);
  x426 = (x118)+(x422);
  x427 = (x426)<(x118);
  x428 = (x427)+(x119);
  x429 = (x428)+(x425);
  x430 = (x126)+(x426);
  x431 = (x430)<(x126);
  x432 = (x431)+(x127);
  x433 = (x432)+(x429);
  x434 = (x132)+(x430);
  x435 = (x434)<(x132);
  x436 = (x435)+(x133);
  x437 = (x436)+(x433);
  x438 = (x136)+(x434);
  x439 = (x438)<(x136);
  x440 = (x439)+(x137);
  x441 = (x440)+(x437);
  x442 = (x138)+(x438);
  x443 = (x442)<(x138);
  x444 = (x443)+(x139);
  x445 = (x444)+(x441);
  x446 = (x158)+(x442);
  x447 = (x446)<(x158);
  x448 = (x447)+(x159);
  x449 = (x448)+(x445);
  x450 = (x166)+(x446);
  x451 = (x450)<(x166);
  x452 = (x451)+(x167);
  x453 = (x452)+(x449);
  x454 = (x176)+(x450);
  x455 = (x454)<(x176);
  x456 = (x455)+(x177);
  x457 = (x456)+(x453);
  x458 = (x188)+(x454);
  x459 = (x458)<(x188);
  x460 = (x459)+(x189);
  x461 = (x460)+(x457);
  x462 = (x202)+(x458);
  x463 = (x462)<(x202);
  x464 = (x463)+(x203);
  x465 = (x464)+(x461);
  x466 = (x48)+(x16);
  x467 = (x466)<(x48);
  x468 = (x467)+(x49);
  x469 = (x468)+(x17);
  x470 = (x60)+(x466);
  x471 = (x470)<(x60);
  x472 = (x471)+(x61);
  x473 = (x472)+(x469);
  x474 = (x70)+(x470);
  x475 = (x474)<(x70);
  x476 = (x475)+(x71);
  x477 = (x476)+(x473);
  x478 = (x78)+(x474);
  x479 = (x478)<(x78);
  x480 = (x479)+(x79);
  x481 = (x480)+(x477);
  x482 = (x84)+(x478);
  x483 = (x482)<(x84);
  x484 = (x483)+(x85);
  x485 = (x484)+(x481);
  x486 = (x180)+(x482);
  x487 = (x486)<(x180);
  x488 = (x487)+(x181);
  x489 = (x488)+(x485);
  x490 = (x192)+(x486);
  x491 = (x490)<(x192);
  x492 = (x491)+(x193);
  x493 = (x492)+(x489);
  x494 = (x206)+(x490);
  x495 = (x494)<(x206);
  x496 = (x495)+(x207);
  x497 = (x496)+(x493);
  x498 = (x22)+(x18);
  x499 = (x498)<(x22);
  x500 = (x499)+(x23);
  x501 = (x500)+(x19);
  x502 = (x50)+(x498);
  x503 = (x502)<(x50);
  x504 = (x503)+(x51);
  x505 = (x504)+(x501);
  x506 = (x62)+(x502);
  x507 = (x506)<(x62);
  x508 = (x507)+(x63);
  x509 = (x508)+(x505);
  x510 = (x72)+(x506);
  x511 = (x510)<(x72);
  x512 = (x511)+(x73);
  x513 = (x512)+(x509);
  x514 = (x80)+(x510);
  x515 = (x514)<(x80);
  x516 = (x515)+(x81);
  x517 = (x516)+(x513);
  x518 = (x86)+(x514);
  x519 = (x518)<(x86);
  x520 = (x519)+(x87);
  x521 = (x520)+(x517);
  x522 = (x90)+(x518);
  x523 = (x522)<(x90);
  x524 = (x523)+(x91);
  x525 = (x524)+(x521);
  x526 = (x194)+(x522);
  x527 = (x526)<(x194);
  x528 = (x527)+(x195);
  x529 = (x528)+(x525);
  x530 = (x208)+(x526);
  x531 = (x530)<(x208);
  x532 = (x531)+(x209);
  x533 = (x532)+(x529);
  x534 = (x24)+(x20);
  x535 = (x534)<(x24);
  x536 = (x535)+(x25);
  x537 = (x536)+(x21);
  x538 = (x26)+(x534);
  x539 = (x538)<(x26);
  x540 = (x539)+(x27);
  x541 = (x540)+(x537);
  x542 = (x52)+(x538);
  x543 = (x542)<(x52);
  x544 = (x543)+(x53);
  x545 = (x544)+(x541);
  x546 = (x64)+(x542);
  x547 = (x546)<(x64);
  x548 = (x547)+(x65);
  x549 = (x548)+(x545);
  x550 = (x74)+(x546);
  x551 = (x550)<(x74);
  x552 = (x551)+(x75);
  x553 = (x552)+(x549);
  x554 = (x82)+(x550);
  x555 = (x554)<(x82);
  x556 = (x555)+(x83);
  x557 = (x556)+(x553);
  x558 = (x88)+(x554);
  x559 = (x558)<(x88);
  x560 = (x559)+(x89);
  x561 = (x560)+(x557);
  x562 = (x92)+(x558);
  x563 = (x562)<(x92);
  x564 = (x563)+(x93);
  x565 = (x564)+(x561);
  x566 = (x94)+(x562);
  x567 = (x566)<(x94);
  x568 = (x567)+(x95);
  x569 = (x568)+(x565);
  x570 = (x210)+(x566);
  x571 = (x570)<(x210);
  x572 = (x571)+(x211);
  x573 = (x572)+(x569);
  x574 = (x240)+(x462);
  x575 = (x574)<(x240);
  x576 = (x575)+(x465);
  x577 = ((x282)>>((uintptr_t)56ULL))|((x285)<<((uintptr_t)8ULL));
  x578 = (x282)&((uintptr_t)72057594037927935ULL);
  x579 = (x574)+(x577);
  x580 = (x579)<(x574);
  x581 = (x580)+(x576);
  x582 = ((x579)>>((uintptr_t)56ULL))|((x581)<<((uintptr_t)8ULL));
  x583 = (x579)&((uintptr_t)72057594037927935ULL);
  x584 = (x570)+(x577);
  x585 = (x584)<(x570);
  x586 = (x585)+(x573);
  x587 = (x582)+(x394);
  x588 = (x587)<(x582);
  x589 = (x588)+(x397);
  x590 = ((x584)>>((uintptr_t)56ULL))|((x586)<<((uintptr_t)8ULL));
  x591 = (x584)&((uintptr_t)72057594037927935ULL);
  x592 = (x590)+(x530);
  x593 = (x592)<(x590);
  x594 = (x593)+(x533);
  x595 = ((x587)>>((uintptr_t)56ULL))|((x589)<<((uintptr_t)8ULL));
  x596 = (x587)&((uintptr_t)72057594037927935ULL);
  x597 = (x595)+(x334);
  x598 = (x597)<(x595);
  x599 = (x598)+(x337);
  x600 = ((x592)>>((uintptr_t)56ULL))|((x594)<<((uintptr_t)8ULL));
  x601 = (x592)&((uintptr_t)72057594037927935ULL);
  x602 = (x600)+(x494);
  x603 = (x602)<(x600);
  x604 = (x603)+(x497);
  x605 = ((x597)>>((uintptr_t)56ULL))|((x599)<<((uintptr_t)8ULL));
  x606 = (x597)&((uintptr_t)72057594037927935ULL);
  x607 = (x605)+(x578);
  x608 = ((x602)>>((uintptr_t)56ULL))|((x604)<<((uintptr_t)8ULL));
  x609 = (x602)&((uintptr_t)72057594037927935ULL);
  x610 = (x608)+(x241);
  x611 = (x607)>>((uintptr_t)56ULL);
  x612 = (x607)&((uintptr_t)72057594037927935ULL);
  x613 = (x610)>>((uintptr_t)56ULL);
  x614 = (x610)&((uintptr_t)72057594037927935ULL);
  x615 = (x583)+(x611);
  x616 = (x591)+(x611);
  x617 = (x613)+(x615);
  x618 = (x617)>>((uintptr_t)56ULL);
  x619 = (x617)&((uintptr_t)72057594037927935ULL);
  x620 = (x618)+(x596);
  x621 = (x616)>>((uintptr_t)56ULL);
  x622 = (x616)&((uintptr_t)72057594037927935ULL);
  x623 = (x621)+(x601);
  x624 = x622;
  x625 = x623;
  x626 = x609;
  x627 = x614;
  x628 = x619;
  x629 = x620;
  x630 = x606;
  x631 = x612;
  /*skip*/
  _br2_store((out0)+((uintptr_t)0ULL), x624, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)8ULL), x625, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)16ULL), x626, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)24ULL), x627, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)32ULL), x628, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)40ULL), x629, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)48ULL), x630, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)56ULL), x631, sizeof(uintptr_t));
  /*skip*/
  return;
}

/* NOTE: The following wrapper function is not covered by Coq proofs */
static void fiat_p448_carry_mul(uint64_t out1[8], const uint64_t arg1[8], const uint64_t arg2[8]) {
  internal_fiat_p448_carry_mul((uintptr_t)out1, (uintptr_t)arg1, (uintptr_t)arg2);
}


/*
 * Input Bounds:
 *   in0: [[0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000]]
 * Output Bounds:
 *   out0: [[0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000]]
 */
static
void internal_fiat_p448_carry_square(uintptr_t out0, uintptr_t in0) {
  uintptr_t x8, x13, x7, x9, x6, x14, x19, x5, x18, x24, x4, x23, x21, x20, x3, x16, x15, x2, x11, x10, x1, x12, x17, x22, x25, x26, x27, x28, x0, x53, x61, x142, x62, x143, x54, x141, x121, x146, x122, x147, x144, x145, x133, x150, x134, x151, x148, x152, x149, x55, x63, x156, x64, x157, x56, x155, x89, x160, x90, x161, x158, x159, x101, x164, x102, x165, x162, x163, x113, x168, x114, x169, x166, x167, x125, x172, x126, x173, x170, x37, x45, x176, x46, x177, x38, x175, x59, x180, x60, x181, x178, x179, x67, x184, x68, x185, x182, x183, x79, x188, x80, x189, x186, x187, x91, x192, x92, x193, x190, x191, x103, x196, x104, x197, x194, x195, x115, x200, x116, x201, x198, x199, x127, x204, x128, x205, x202, x39, x47, x208, x48, x209, x40, x207, x71, x212, x72, x213, x210, x211, x83, x216, x84, x217, x214, x215, x95, x220, x96, x221, x218, x219, x105, x224, x106, x225, x222, x223, x117, x228, x118, x229, x226, x227, x129, x232, x130, x233, x230, x41, x43, x236, x44, x237, x42, x235, x49, x240, x50, x241, x238, x239, x51, x244, x52, x245, x242, x243, x75, x248, x76, x249, x246, x247, x87, x252, x88, x253, x250, x251, x99, x256, x100, x257, x254, x255, x107, x260, x108, x261, x258, x259, x111, x264, x112, x265, x262, x263, x119, x268, x120, x269, x266, x267, x131, x272, x132, x273, x270, x29, x57, x276, x58, x277, x30, x275, x65, x280, x66, x281, x278, x279, x77, x284, x78, x285, x282, x283, x123, x288, x124, x289, x286, x287, x135, x292, x136, x293, x290, x31, x69, x296, x70, x297, x32, x295, x81, x300, x82, x301, x298, x299, x93, x304, x94, x305, x302, x303, x137, x308, x138, x309, x306, x33, x35, x312, x36, x313, x34, x311, x73, x316, x74, x317, x314, x315, x85, x320, x86, x321, x318, x319, x97, x324, x98, x325, x322, x323, x109, x328, x110, x329, x326, x327, x139, x332, x140, x333, x330, x271, x153, x336, x274, x174, x171, x335, x341, x337, x342, x340, x338, x331, x346, x334, x231, x343, x349, x234, x347, x345, x307, x351, x354, x310, x350, x348, x203, x356, x359, x206, x355, x353, x291, x361, x364, x294, x360, x358, x366, x339, x365, x363, x369, x154, x368, x371, x344, x352, x372, x374, x376, x378, x379, x357, x377, x382, x362, x383, x384, x370, x375, x380, x381, x367, x373, x385, x386, x387, x388, x389, x390, x391, x392;
  x0 = _br2_load((in0)+((uintptr_t)0ULL), sizeof(uintptr_t));
  x1 = _br2_load((in0)+((uintptr_t)8ULL), sizeof(uintptr_t));
  x2 = _br2_load((in0)+((uintptr_t)16ULL), sizeof(uintptr_t));
  x3 = _br2_load((in0)+((uintptr_t)24ULL), sizeof(uintptr_t));
  x4 = _br2_load((in0)+((uintptr_t)32ULL), sizeof(uintptr_t));
  x5 = _br2_load((in0)+((uintptr_t)40ULL), sizeof(uintptr_t));
  x6 = _br2_load((in0)+((uintptr_t)48ULL), sizeof(uintptr_t));
  x7 = _br2_load((in0)+((uintptr_t)56ULL), sizeof(uintptr_t));
  /*skip*/
  /*skip*/
  x8 = x7;
  x9 = x7;
  x10 = (x8)*((uintptr_t)2ULL);
  x11 = (x9)*((uintptr_t)2ULL);
  x12 = (x7)*((uintptr_t)2ULL);
  x13 = x6;
  x14 = x6;
  x15 = (x13)*((uintptr_t)2ULL);
  x16 = (x14)*((uintptr_t)2ULL);
  x17 = (x6)*((uintptr_t)2ULL);
  x18 = x5;
  x19 = x5;
  x20 = (x18)*((uintptr_t)2ULL);
  x21 = (x19)*((uintptr_t)2ULL);
  x22 = (x5)*((uintptr_t)2ULL);
  x23 = x4;
  x24 = x4;
  x25 = (x4)*((uintptr_t)2ULL);
  x26 = (x3)*((uintptr_t)2ULL);
  x27 = (x2)*((uintptr_t)2ULL);
  x28 = (x1)*((uintptr_t)2ULL);
  x29 = (x7)*(x8);
  x30 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*(x8))>>32 : ((__uint128_t)(x7)*(x8))>>64;
  x31 = (x6)*(x10);
  x32 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*(x10))>>32 : ((__uint128_t)(x6)*(x10))>>64;
  x33 = (x6)*(x13);
  x34 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*(x13))>>32 : ((__uint128_t)(x6)*(x13))>>64;
  x35 = (x5)*(x10);
  x36 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*(x10))>>32 : ((__uint128_t)(x5)*(x10))>>64;
  x37 = (x7)*(x8);
  x38 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*(x8))>>32 : ((__uint128_t)(x7)*(x8))>>64;
  x39 = (x6)*(x10);
  x40 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*(x10))>>32 : ((__uint128_t)(x6)*(x10))>>64;
  x41 = (x6)*(x13);
  x42 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*(x13))>>32 : ((__uint128_t)(x6)*(x13))>>64;
  x43 = (x5)*(x10);
  x44 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*(x10))>>32 : ((__uint128_t)(x5)*(x10))>>64;
  x45 = (x7)*(x9);
  x46 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*(x9))>>32 : ((__uint128_t)(x7)*(x9))>>64;
  x47 = (x6)*(x11);
  x48 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*(x11))>>32 : ((__uint128_t)(x6)*(x11))>>64;
  x49 = (x6)*(x14);
  x50 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*(x14))>>32 : ((__uint128_t)(x6)*(x14))>>64;
  x51 = (x5)*(x11);
  x52 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*(x11))>>32 : ((__uint128_t)(x5)*(x11))>>64;
  x53 = (x5)*(x16);
  x54 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*(x16))>>32 : ((__uint128_t)(x5)*(x16))>>64;
  x55 = (x5)*(x15);
  x56 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*(x15))>>32 : ((__uint128_t)(x5)*(x15))>>64;
  x57 = (x5)*(x19);
  x58 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*(x19))>>32 : ((__uint128_t)(x5)*(x19))>>64;
  x59 = (x5)*(x18);
  x60 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*(x18))>>32 : ((__uint128_t)(x5)*(x18))>>64;
  x61 = (x4)*(x11);
  x62 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*(x11))>>32 : ((__uint128_t)(x4)*(x11))>>64;
  x63 = (x4)*(x10);
  x64 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*(x10))>>32 : ((__uint128_t)(x4)*(x10))>>64;
  x65 = (x4)*(x16);
  x66 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*(x16))>>32 : ((__uint128_t)(x4)*(x16))>>64;
  x67 = (x4)*(x15);
  x68 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*(x15))>>32 : ((__uint128_t)(x4)*(x15))>>64;
  x69 = (x4)*(x21);
  x70 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*(x21))>>32 : ((__uint128_t)(x4)*(x21))>>64;
  x71 = (x4)*(x20);
  x72 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*(x20))>>32 : ((__uint128_t)(x4)*(x20))>>64;
  x73 = (x4)*(x24);
  x74 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*(x24))>>32 : ((__uint128_t)(x4)*(x24))>>64;
  x75 = (x4)*(x23);
  x76 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*(x23))>>32 : ((__uint128_t)(x4)*(x23))>>64;
  x77 = (x3)*(x11);
  x78 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*(x11))>>32 : ((__uint128_t)(x3)*(x11))>>64;
  x79 = (x3)*(x10);
  x80 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*(x10))>>32 : ((__uint128_t)(x3)*(x10))>>64;
  x81 = (x3)*(x16);
  x82 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*(x16))>>32 : ((__uint128_t)(x3)*(x16))>>64;
  x83 = (x3)*(x15);
  x84 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*(x15))>>32 : ((__uint128_t)(x3)*(x15))>>64;
  x85 = (x3)*(x21);
  x86 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*(x21))>>32 : ((__uint128_t)(x3)*(x21))>>64;
  x87 = (x3)*(x20);
  x88 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*(x20))>>32 : ((__uint128_t)(x3)*(x20))>>64;
  x89 = (x3)*(x25);
  x90 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*(x25))>>32 : ((__uint128_t)(x3)*(x25))>>64;
  x91 = (x3)*(x3);
  x92 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*(x3))>>32 : ((__uint128_t)(x3)*(x3))>>64;
  x93 = (x2)*(x11);
  x94 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*(x11))>>32 : ((__uint128_t)(x2)*(x11))>>64;
  x95 = (x2)*(x10);
  x96 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*(x10))>>32 : ((__uint128_t)(x2)*(x10))>>64;
  x97 = (x2)*(x16);
  x98 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*(x16))>>32 : ((__uint128_t)(x2)*(x16))>>64;
  x99 = (x2)*(x15);
  x100 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*(x15))>>32 : ((__uint128_t)(x2)*(x15))>>64;
  x101 = (x2)*(x22);
  x102 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*(x22))>>32 : ((__uint128_t)(x2)*(x22))>>64;
  x103 = (x2)*(x25);
  x104 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*(x25))>>32 : ((__uint128_t)(x2)*(x25))>>64;
  x105 = (x2)*(x26);
  x106 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*(x26))>>32 : ((__uint128_t)(x2)*(x26))>>64;
  x107 = (x2)*(x2);
  x108 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*(x2))>>32 : ((__uint128_t)(x2)*(x2))>>64;
  x109 = (x1)*(x11);
  x110 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x11))>>32 : ((__uint128_t)(x1)*(x11))>>64;
  x111 = (x1)*(x10);
  x112 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x10))>>32 : ((__uint128_t)(x1)*(x10))>>64;
  x113 = (x1)*(x17);
  x114 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x17))>>32 : ((__uint128_t)(x1)*(x17))>>64;
  x115 = (x1)*(x22);
  x116 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x22))>>32 : ((__uint128_t)(x1)*(x22))>>64;
  x117 = (x1)*(x25);
  x118 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x25))>>32 : ((__uint128_t)(x1)*(x25))>>64;
  x119 = (x1)*(x26);
  x120 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x26))>>32 : ((__uint128_t)(x1)*(x26))>>64;
  x121 = (x1)*(x27);
  x122 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x27))>>32 : ((__uint128_t)(x1)*(x27))>>64;
  x123 = (x1)*(x1);
  x124 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x1))>>32 : ((__uint128_t)(x1)*(x1))>>64;
  x125 = (x0)*(x12);
  x126 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x12))>>32 : ((__uint128_t)(x0)*(x12))>>64;
  x127 = (x0)*(x17);
  x128 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x17))>>32 : ((__uint128_t)(x0)*(x17))>>64;
  x129 = (x0)*(x22);
  x130 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x22))>>32 : ((__uint128_t)(x0)*(x22))>>64;
  x131 = (x0)*(x25);
  x132 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x25))>>32 : ((__uint128_t)(x0)*(x25))>>64;
  x133 = (x0)*(x26);
  x134 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x26))>>32 : ((__uint128_t)(x0)*(x26))>>64;
  x135 = (x0)*(x27);
  x136 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x27))>>32 : ((__uint128_t)(x0)*(x27))>>64;
  x137 = (x0)*(x28);
  x138 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x28))>>32 : ((__uint128_t)(x0)*(x28))>>64;
  x139 = (x0)*(x0);
  x140 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x0))>>32 : ((__uint128_t)(x0)*(x0))>>64;
  x141 = (x61)+(x53);
  x142 = (x141)<(x61);
  x143 = (x142)+(x62);
  x144 = (x143)+(x54);
  x145 = (x121)+(x141);
  x146 = (x145)<(x121);
  x147 = (x146)+(x122);
  x148 = (x147)+(x144);
  x149 = (x133)+(x145);
  x150 = (x149)<(x133);
  x151 = (x150)+(x134);
  x152 = (x151)+(x148);
  x153 = ((x149)>>((uintptr_t)56ULL))|((x152)<<((uintptr_t)8ULL));
  x154 = (x149)&((uintptr_t)72057594037927935ULL);
  x155 = (x63)+(x55);
  x156 = (x155)<(x63);
  x157 = (x156)+(x64);
  x158 = (x157)+(x56);
  x159 = (x89)+(x155);
  x160 = (x159)<(x89);
  x161 = (x160)+(x90);
  x162 = (x161)+(x158);
  x163 = (x101)+(x159);
  x164 = (x163)<(x101);
  x165 = (x164)+(x102);
  x166 = (x165)+(x162);
  x167 = (x113)+(x163);
  x168 = (x167)<(x113);
  x169 = (x168)+(x114);
  x170 = (x169)+(x166);
  x171 = (x125)+(x167);
  x172 = (x171)<(x125);
  x173 = (x172)+(x126);
  x174 = (x173)+(x170);
  x175 = (x45)+(x37);
  x176 = (x175)<(x45);
  x177 = (x176)+(x46);
  x178 = (x177)+(x38);
  x179 = (x59)+(x175);
  x180 = (x179)<(x59);
  x181 = (x180)+(x60);
  x182 = (x181)+(x178);
  x183 = (x67)+(x179);
  x184 = (x183)<(x67);
  x185 = (x184)+(x68);
  x186 = (x185)+(x182);
  x187 = (x79)+(x183);
  x188 = (x187)<(x79);
  x189 = (x188)+(x80);
  x190 = (x189)+(x186);
  x191 = (x91)+(x187);
  x192 = (x191)<(x91);
  x193 = (x192)+(x92);
  x194 = (x193)+(x190);
  x195 = (x103)+(x191);
  x196 = (x195)<(x103);
  x197 = (x196)+(x104);
  x198 = (x197)+(x194);
  x199 = (x115)+(x195);
  x200 = (x199)<(x115);
  x201 = (x200)+(x116);
  x202 = (x201)+(x198);
  x203 = (x127)+(x199);
  x204 = (x203)<(x127);
  x205 = (x204)+(x128);
  x206 = (x205)+(x202);
  x207 = (x47)+(x39);
  x208 = (x207)<(x47);
  x209 = (x208)+(x48);
  x210 = (x209)+(x40);
  x211 = (x71)+(x207);
  x212 = (x211)<(x71);
  x213 = (x212)+(x72);
  x214 = (x213)+(x210);
  x215 = (x83)+(x211);
  x216 = (x215)<(x83);
  x217 = (x216)+(x84);
  x218 = (x217)+(x214);
  x219 = (x95)+(x215);
  x220 = (x219)<(x95);
  x221 = (x220)+(x96);
  x222 = (x221)+(x218);
  x223 = (x105)+(x219);
  x224 = (x223)<(x105);
  x225 = (x224)+(x106);
  x226 = (x225)+(x222);
  x227 = (x117)+(x223);
  x228 = (x227)<(x117);
  x229 = (x228)+(x118);
  x230 = (x229)+(x226);
  x231 = (x129)+(x227);
  x232 = (x231)<(x129);
  x233 = (x232)+(x130);
  x234 = (x233)+(x230);
  x235 = (x43)+(x41);
  x236 = (x235)<(x43);
  x237 = (x236)+(x44);
  x238 = (x237)+(x42);
  x239 = (x49)+(x235);
  x240 = (x239)<(x49);
  x241 = (x240)+(x50);
  x242 = (x241)+(x238);
  x243 = (x51)+(x239);
  x244 = (x243)<(x51);
  x245 = (x244)+(x52);
  x246 = (x245)+(x242);
  x247 = (x75)+(x243);
  x248 = (x247)<(x75);
  x249 = (x248)+(x76);
  x250 = (x249)+(x246);
  x251 = (x87)+(x247);
  x252 = (x251)<(x87);
  x253 = (x252)+(x88);
  x254 = (x253)+(x250);
  x255 = (x99)+(x251);
  x256 = (x255)<(x99);
  x257 = (x256)+(x100);
  x258 = (x257)+(x254);
  x259 = (x107)+(x255);
  x260 = (x259)<(x107);
  x261 = (x260)+(x108);
  x262 = (x261)+(x258);
  x263 = (x111)+(x259);
  x264 = (x263)<(x111);
  x265 = (x264)+(x112);
  x266 = (x265)+(x262);
  x267 = (x119)+(x263);
  x268 = (x267)<(x119);
  x269 = (x268)+(x120);
  x270 = (x269)+(x266);
  x271 = (x131)+(x267);
  x272 = (x271)<(x131);
  x273 = (x272)+(x132);
  x274 = (x273)+(x270);
  x275 = (x57)+(x29);
  x276 = (x275)<(x57);
  x277 = (x276)+(x58);
  x278 = (x277)+(x30);
  x279 = (x65)+(x275);
  x280 = (x279)<(x65);
  x281 = (x280)+(x66);
  x282 = (x281)+(x278);
  x283 = (x77)+(x279);
  x284 = (x283)<(x77);
  x285 = (x284)+(x78);
  x286 = (x285)+(x282);
  x287 = (x123)+(x283);
  x288 = (x287)<(x123);
  x289 = (x288)+(x124);
  x290 = (x289)+(x286);
  x291 = (x135)+(x287);
  x292 = (x291)<(x135);
  x293 = (x292)+(x136);
  x294 = (x293)+(x290);
  x295 = (x69)+(x31);
  x296 = (x295)<(x69);
  x297 = (x296)+(x70);
  x298 = (x297)+(x32);
  x299 = (x81)+(x295);
  x300 = (x299)<(x81);
  x301 = (x300)+(x82);
  x302 = (x301)+(x298);
  x303 = (x93)+(x299);
  x304 = (x303)<(x93);
  x305 = (x304)+(x94);
  x306 = (x305)+(x302);
  x307 = (x137)+(x303);
  x308 = (x307)<(x137);
  x309 = (x308)+(x138);
  x310 = (x309)+(x306);
  x311 = (x35)+(x33);
  x312 = (x311)<(x35);
  x313 = (x312)+(x36);
  x314 = (x313)+(x34);
  x315 = (x73)+(x311);
  x316 = (x315)<(x73);
  x317 = (x316)+(x74);
  x318 = (x317)+(x314);
  x319 = (x85)+(x315);
  x320 = (x319)<(x85);
  x321 = (x320)+(x86);
  x322 = (x321)+(x318);
  x323 = (x97)+(x319);
  x324 = (x323)<(x97);
  x325 = (x324)+(x98);
  x326 = (x325)+(x322);
  x327 = (x109)+(x323);
  x328 = (x327)<(x109);
  x329 = (x328)+(x110);
  x330 = (x329)+(x326);
  x331 = (x139)+(x327);
  x332 = (x331)<(x139);
  x333 = (x332)+(x140);
  x334 = (x333)+(x330);
  x335 = (x153)+(x271);
  x336 = (x335)<(x153);
  x337 = (x336)+(x274);
  x338 = ((x171)>>((uintptr_t)56ULL))|((x174)<<((uintptr_t)8ULL));
  x339 = (x171)&((uintptr_t)72057594037927935ULL);
  x340 = (x335)+(x338);
  x341 = (x340)<(x335);
  x342 = (x341)+(x337);
  x343 = ((x340)>>((uintptr_t)56ULL))|((x342)<<((uintptr_t)8ULL));
  x344 = (x340)&((uintptr_t)72057594037927935ULL);
  x345 = (x331)+(x338);
  x346 = (x345)<(x331);
  x347 = (x346)+(x334);
  x348 = (x343)+(x231);
  x349 = (x348)<(x343);
  x350 = (x349)+(x234);
  x351 = ((x345)>>((uintptr_t)56ULL))|((x347)<<((uintptr_t)8ULL));
  x352 = (x345)&((uintptr_t)72057594037927935ULL);
  x353 = (x351)+(x307);
  x354 = (x353)<(x351);
  x355 = (x354)+(x310);
  x356 = ((x348)>>((uintptr_t)56ULL))|((x350)<<((uintptr_t)8ULL));
  x357 = (x348)&((uintptr_t)72057594037927935ULL);
  x358 = (x356)+(x203);
  x359 = (x358)<(x356);
  x360 = (x359)+(x206);
  x361 = ((x353)>>((uintptr_t)56ULL))|((x355)<<((uintptr_t)8ULL));
  x362 = (x353)&((uintptr_t)72057594037927935ULL);
  x363 = (x361)+(x291);
  x364 = (x363)<(x361);
  x365 = (x364)+(x294);
  x366 = ((x358)>>((uintptr_t)56ULL))|((x360)<<((uintptr_t)8ULL));
  x367 = (x358)&((uintptr_t)72057594037927935ULL);
  x368 = (x366)+(x339);
  x369 = ((x363)>>((uintptr_t)56ULL))|((x365)<<((uintptr_t)8ULL));
  x370 = (x363)&((uintptr_t)72057594037927935ULL);
  x371 = (x369)+(x154);
  x372 = (x368)>>((uintptr_t)56ULL);
  x373 = (x368)&((uintptr_t)72057594037927935ULL);
  x374 = (x371)>>((uintptr_t)56ULL);
  x375 = (x371)&((uintptr_t)72057594037927935ULL);
  x376 = (x344)+(x372);
  x377 = (x352)+(x372);
  x378 = (x374)+(x376);
  x379 = (x378)>>((uintptr_t)56ULL);
  x380 = (x378)&((uintptr_t)72057594037927935ULL);
  x381 = (x379)+(x357);
  x382 = (x377)>>((uintptr_t)56ULL);
  x383 = (x377)&((uintptr_t)72057594037927935ULL);
  x384 = (x382)+(x362);
  x385 = x383;
  x386 = x384;
  x387 = x370;
  x388 = x375;
  x389 = x380;
  x390 = x381;
  x391 = x367;
  x392 = x373;
  /*skip*/
  _br2_store((out0)+((uintptr_t)0ULL), x385, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)8ULL), x386, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)16ULL), x387, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)24ULL), x388, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)32ULL), x389, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)40ULL), x390, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)48ULL), x391, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)56ULL), x392, sizeof(uintptr_t));
  /*skip*/
  return;
}

/* NOTE: The following wrapper function is not covered by Coq proofs */
static void fiat_p448_carry_square(uint64_t out1[8], const uint64_t arg1[8]) {
  internal_fiat_p448_carry_square((uintptr_t)out1, (uintptr_t)arg1);
}


/*
 * Input Bounds:
 *   in0: [[0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000]]
 * Output Bounds:
 *   out0: [[0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000]]
 */
static
void internal_fiat_p448_carry(uintptr_t out0, uintptr_t in0) {
  uintptr_t x3, x7, x4, x0, x10, x5, x1, x6, x2, x9, x8, x12, x11, x19, x20, x14, x16, x18, x21, x13, x15, x17, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31, x32, x33, x34, x35, x36, x37;
  x0 = _br2_load((in0)+((uintptr_t)0ULL), sizeof(uintptr_t));
  x1 = _br2_load((in0)+((uintptr_t)8ULL), sizeof(uintptr_t));
  x2 = _br2_load((in0)+((uintptr_t)16ULL), sizeof(uintptr_t));
  x3 = _br2_load((in0)+((uintptr_t)24ULL), sizeof(uintptr_t));
  x4 = _br2_load((in0)+((uintptr_t)32ULL), sizeof(uintptr_t));
  x5 = _br2_load((in0)+((uintptr_t)40ULL), sizeof(uintptr_t));
  x6 = _br2_load((in0)+((uintptr_t)48ULL), sizeof(uintptr_t));
  x7 = _br2_load((in0)+((uintptr_t)56ULL), sizeof(uintptr_t));
  /*skip*/
  /*skip*/
  x8 = x3;
  x9 = x7;
  x10 = (x9)>>((uintptr_t)56ULL);
  x11 = (((x8)>>((uintptr_t)56ULL))+(x4))+(x10);
  x12 = (x0)+(x10);
  x13 = ((x11)>>((uintptr_t)56ULL))+(x5);
  x14 = ((x12)>>((uintptr_t)56ULL))+(x1);
  x15 = ((x13)>>((uintptr_t)56ULL))+(x6);
  x16 = ((x14)>>((uintptr_t)56ULL))+(x2);
  x17 = ((x15)>>((uintptr_t)56ULL))+((x9)&((uintptr_t)72057594037927935ULL));
  x18 = ((x16)>>((uintptr_t)56ULL))+((x8)&((uintptr_t)72057594037927935ULL));
  x19 = (x17)>>((uintptr_t)56ULL);
  x20 = ((x12)&((uintptr_t)72057594037927935ULL))+(x19);
  x21 = ((x18)>>((uintptr_t)56ULL))+(((x11)&((uintptr_t)72057594037927935ULL))+(x19));
  x22 = (x20)&((uintptr_t)72057594037927935ULL);
  x23 = ((x20)>>((uintptr_t)56ULL))+((x14)&((uintptr_t)72057594037927935ULL));
  x24 = (x16)&((uintptr_t)72057594037927935ULL);
  x25 = (x18)&((uintptr_t)72057594037927935ULL);
  x26 = (x21)&((uintptr_t)72057594037927935ULL);
  x27 = ((x21)>>((uintptr_t)56ULL))+((x13)&((uintptr_t)72057594037927935ULL));
  x28 = (x15)&((uintptr_t)72057594037927935ULL);
  x29 = (x17)&((uintptr_t)72057594037927935ULL);
  x30 = x22;
  x31 = x23;
  x32 = x24;
  x33 = x25;
  x34 = x26;
  x35 = x27;
  x36 = x28;
  x37 = x29;
  /*skip*/
  _br2_store((out0)+((uintptr_t)0ULL), x30, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)8ULL), x31, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)16ULL), x32, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)24ULL), x33, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)32ULL), x34, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)40ULL), x35, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)48ULL), x36, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)56ULL), x37, sizeof(uintptr_t));
  /*skip*/
  return;
}

/* NOTE: The following wrapper function is not covered by Coq proofs */
static void fiat_p448_carry(uint64_t out1[8], const uint64_t arg1[8]) {
  internal_fiat_p448_carry((uintptr_t)out1, (uintptr_t)arg1);
}


/*
 * Input Bounds:
 *   in0: [[0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000]]
 *   in1: [[0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000]]
 * Output Bounds:
 *   out0: [[0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000]]
 */
static
void internal_fiat_p448_add(uintptr_t out0, uintptr_t in0, uintptr_t in1) {
  uintptr_t x0, x8, x1, x9, x2, x10, x3, x11, x4, x12, x5, x13, x6, x14, x7, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31;
  x0 = _br2_load((in0)+((uintptr_t)0ULL), sizeof(uintptr_t));
  x1 = _br2_load((in0)+((uintptr_t)8ULL), sizeof(uintptr_t));
  x2 = _br2_load((in0)+((uintptr_t)16ULL), sizeof(uintptr_t));
  x3 = _br2_load((in0)+((uintptr_t)24ULL), sizeof(uintptr_t));
  x4 = _br2_load((in0)+((uintptr_t)32ULL), sizeof(uintptr_t));
  x5 = _br2_load((in0)+((uintptr_t)40ULL), sizeof(uintptr_t));
  x6 = _br2_load((in0)+((uintptr_t)48ULL), sizeof(uintptr_t));
  x7 = _br2_load((in0)+((uintptr_t)56ULL), sizeof(uintptr_t));
  /*skip*/
  x8 = _br2_load((in1)+((uintptr_t)0ULL), sizeof(uintptr_t));
  x9 = _br2_load((in1)+((uintptr_t)8ULL), sizeof(uintptr_t));
  x10 = _br2_load((in1)+((uintptr_t)16ULL), sizeof(uintptr_t));
  x11 = _br2_load((in1)+((uintptr_t)24ULL), sizeof(uintptr_t));
  x12 = _br2_load((in1)+((uintptr_t)32ULL), sizeof(uintptr_t));
  x13 = _br2_load((in1)+((uintptr_t)40ULL), sizeof(uintptr_t));
  x14 = _br2_load((in1)+((uintptr_t)48ULL), sizeof(uintptr_t));
  x15 = _br2_load((in1)+((uintptr_t)56ULL), sizeof(uintptr_t));
  /*skip*/
  /*skip*/
  x16 = (x0)+(x8);
  x17 = (x1)+(x9);
  x18 = (x2)+(x10);
  x19 = (x3)+(x11);
  x20 = (x4)+(x12);
  x21 = (x5)+(x13);
  x22 = (x6)+(x14);
  x23 = (x7)+(x15);
  x24 = x16;
  x25 = x17;
  x26 = x18;
  x27 = x19;
  x28 = x20;
  x29 = x21;
  x30 = x22;
  x31 = x23;
  /*skip*/
  _br2_store((out0)+((uintptr_t)0ULL), x24, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)8ULL), x25, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)16ULL), x26, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)24ULL), x27, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)32ULL), x28, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)40ULL), x29, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)48ULL), x30, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)56ULL), x31, sizeof(uintptr_t));
  /*skip*/
  return;
}

/* NOTE: The following wrapper function is not covered by Coq proofs */
static void fiat_p448_add(uint64_t out1[8], const uint64_t arg1[8], const uint64_t arg2[8]) {
  internal_fiat_p448_add((uintptr_t)out1, (uintptr_t)arg1, (uintptr_t)arg2);
}


/*
 * Input Bounds:
 *   in0: [[0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000]]
 *   in1: [[0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000]]
 * Output Bounds:
 *   out0: [[0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000]]
 */
static
void internal_fiat_p448_sub(uintptr_t out0, uintptr_t in0, uintptr_t in1) {
  uintptr_t x0, x8, x1, x9, x2, x10, x3, x11, x4, x12, x5, x13, x6, x14, x7, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31;
  x0 = _br2_load((in0)+((uintptr_t)0ULL), sizeof(uintptr_t));
  x1 = _br2_load((in0)+((uintptr_t)8ULL), sizeof(uintptr_t));
  x2 = _br2_load((in0)+((uintptr_t)16ULL), sizeof(uintptr_t));
  x3 = _br2_load((in0)+((uintptr_t)24ULL), sizeof(uintptr_t));
  x4 = _br2_load((in0)+((uintptr_t)32ULL), sizeof(uintptr_t));
  x5 = _br2_load((in0)+((uintptr_t)40ULL), sizeof(uintptr_t));
  x6 = _br2_load((in0)+((uintptr_t)48ULL), sizeof(uintptr_t));
  x7 = _br2_load((in0)+((uintptr_t)56ULL), sizeof(uintptr_t));
  /*skip*/
  x8 = _br2_load((in1)+((uintptr_t)0ULL), sizeof(uintptr_t));
  x9 = _br2_load((in1)+((uintptr_t)8ULL), sizeof(uintptr_t));
  x10 = _br2_load((in1)+((uintptr_t)16ULL), sizeof(uintptr_t));
  x11 = _br2_load((in1)+((uintptr_t)24ULL), sizeof(uintptr_t));
  x12 = _br2_load((in1)+((uintptr_t)32ULL), sizeof(uintptr_t));
  x13 = _br2_load((in1)+((uintptr_t)40ULL), sizeof(uintptr_t));
  x14 = _br2_load((in1)+((uintptr_t)48ULL), sizeof(uintptr_t));
  x15 = _br2_load((in1)+((uintptr_t)56ULL), sizeof(uintptr_t));
  /*skip*/
  /*skip*/
  x16 = (((uintptr_t)144115188075855870ULL)+(x0))-(x8);
  x17 = (((uintptr_t)144115188075855870ULL)+(x1))-(x9);
  x18 = (((uintptr_t)144115188075855870ULL)+(x2))-(x10);
  x19 = (((uintptr_t)144115188075855870ULL)+(x3))-(x11);
  x20 = (((uintptr_t)144115188075855868ULL)+(x4))-(x12);
  x21 = (((uintptr_t)144115188075855870ULL)+(x5))-(x13);
  x22 = (((uintptr_t)144115188075855870ULL)+(x6))-(x14);
  x23 = (((uintptr_t)144115188075855870ULL)+(x7))-(x15);
  x24 = x16;
  x25 = x17;
  x26 = x18;
  x27 = x19;
  x28 = x20;
  x29 = x21;
  x30 = x22;
  x31 = x23;
  /*skip*/
  _br2_store((out0)+((uintptr_t)0ULL), x24, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)8ULL), x25, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)16ULL), x26, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)24ULL), x27, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)32ULL), x28, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)40ULL), x29, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)48ULL), x30, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)56ULL), x31, sizeof(uintptr_t));
  /*skip*/
  return;
}

/* NOTE: The following wrapper function is not covered by Coq proofs */
static void fiat_p448_sub(uint64_t out1[8], const uint64_t arg1[8], const uint64_t arg2[8]) {
  internal_fiat_p448_sub((uintptr_t)out1, (uintptr_t)arg1, (uintptr_t)arg2);
}


/*
 * Input Bounds:
 *   in0: [[0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000]]
 * Output Bounds:
 *   out0: [[0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000]]
 */
static
void internal_fiat_p448_opp(uintptr_t out0, uintptr_t in0) {
  uintptr_t x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23;
  x0 = _br2_load((in0)+((uintptr_t)0ULL), sizeof(uintptr_t));
  x1 = _br2_load((in0)+((uintptr_t)8ULL), sizeof(uintptr_t));
  x2 = _br2_load((in0)+((uintptr_t)16ULL), sizeof(uintptr_t));
  x3 = _br2_load((in0)+((uintptr_t)24ULL), sizeof(uintptr_t));
  x4 = _br2_load((in0)+((uintptr_t)32ULL), sizeof(uintptr_t));
  x5 = _br2_load((in0)+((uintptr_t)40ULL), sizeof(uintptr_t));
  x6 = _br2_load((in0)+((uintptr_t)48ULL), sizeof(uintptr_t));
  x7 = _br2_load((in0)+((uintptr_t)56ULL), sizeof(uintptr_t));
  /*skip*/
  /*skip*/
  x8 = ((uintptr_t)144115188075855870ULL)-(x0);
  x9 = ((uintptr_t)144115188075855870ULL)-(x1);
  x10 = ((uintptr_t)144115188075855870ULL)-(x2);
  x11 = ((uintptr_t)144115188075855870ULL)-(x3);
  x12 = ((uintptr_t)144115188075855868ULL)-(x4);
  x13 = ((uintptr_t)144115188075855870ULL)-(x5);
  x14 = ((uintptr_t)144115188075855870ULL)-(x6);
  x15 = ((uintptr_t)144115188075855870ULL)-(x7);
  x16 = x8;
  x17 = x9;
  x18 = x10;
  x19 = x11;
  x20 = x12;
  x21 = x13;
  x22 = x14;
  x23 = x15;
  /*skip*/
  _br2_store((out0)+((uintptr_t)0ULL), x16, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)8ULL), x17, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)16ULL), x18, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)24ULL), x19, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)32ULL), x20, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)40ULL), x21, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)48ULL), x22, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)56ULL), x23, sizeof(uintptr_t));
  /*skip*/
  return;
}

/* NOTE: The following wrapper function is not covered by Coq proofs */
static void fiat_p448_opp(uint64_t out1[8], const uint64_t arg1[8]) {
  internal_fiat_p448_opp((uintptr_t)out1, (uintptr_t)arg1);
}


/*
 * Input Bounds:
 *   in0: [0x0 ~> 0x1]
 *   in1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 *   in2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 * Output Bounds:
 *   out0: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 */
static
void internal_fiat_p448_selectznz(uintptr_t out0, uintptr_t in0, uintptr_t in1, uintptr_t in2) {
  uintptr_t x8, x16, x0, x17, x9, x19, x1, x20, x10, x22, x2, x23, x11, x25, x3, x26, x12, x28, x4, x29, x13, x31, x5, x32, x14, x34, x6, x35, x15, x37, x7, x38, x18, x21, x24, x27, x30, x33, x36, x39, x40, x41, x42, x43, x44, x45, x46, x47;
  /*skip*/
  x0 = _br2_load((in1)+((uintptr_t)0ULL), sizeof(uintptr_t));
  x1 = _br2_load((in1)+((uintptr_t)8ULL), sizeof(uintptr_t));
  x2 = _br2_load((in1)+((uintptr_t)16ULL), sizeof(uintptr_t));
  x3 = _br2_load((in1)+((uintptr_t)24ULL), sizeof(uintptr_t));
  x4 = _br2_load((in1)+((uintptr_t)32ULL), sizeof(uintptr_t));
  x5 = _br2_load((in1)+((uintptr_t)40ULL), sizeof(uintptr_t));
  x6 = _br2_load((in1)+((uintptr_t)48ULL), sizeof(uintptr_t));
  x7 = _br2_load((in1)+((uintptr_t)56ULL), sizeof(uintptr_t));
  /*skip*/
  x8 = _br2_load((in2)+((uintptr_t)0ULL), sizeof(uintptr_t));
  x9 = _br2_load((in2)+((uintptr_t)8ULL), sizeof(uintptr_t));
  x10 = _br2_load((in2)+((uintptr_t)16ULL), sizeof(uintptr_t));
  x11 = _br2_load((in2)+((uintptr_t)24ULL), sizeof(uintptr_t));
  x12 = _br2_load((in2)+((uintptr_t)32ULL), sizeof(uintptr_t));
  x13 = _br2_load((in2)+((uintptr_t)40ULL), sizeof(uintptr_t));
  x14 = _br2_load((in2)+((uintptr_t)48ULL), sizeof(uintptr_t));
  x15 = _br2_load((in2)+((uintptr_t)56ULL), sizeof(uintptr_t));
  /*skip*/
  /*skip*/
  x16 = ((uintptr_t)-1ULL)+((in0)==((uintptr_t)0ULL));
  x17 = (x16)^((uintptr_t)18446744073709551615ULL);
  x18 = ((x8)&(x16))|((x0)&(x17));
  x19 = ((uintptr_t)-1ULL)+((in0)==((uintptr_t)0ULL));
  x20 = (x19)^((uintptr_t)18446744073709551615ULL);
  x21 = ((x9)&(x19))|((x1)&(x20));
  x22 = ((uintptr_t)-1ULL)+((in0)==((uintptr_t)0ULL));
  x23 = (x22)^((uintptr_t)18446744073709551615ULL);
  x24 = ((x10)&(x22))|((x2)&(x23));
  x25 = ((uintptr_t)-1ULL)+((in0)==((uintptr_t)0ULL));
  x26 = (x25)^((uintptr_t)18446744073709551615ULL);
  x27 = ((x11)&(x25))|((x3)&(x26));
  x28 = ((uintptr_t)-1ULL)+((in0)==((uintptr_t)0ULL));
  x29 = (x28)^((uintptr_t)18446744073709551615ULL);
  x30 = ((x12)&(x28))|((x4)&(x29));
  x31 = ((uintptr_t)-1ULL)+((in0)==((uintptr_t)0ULL));
  x32 = (x31)^((uintptr_t)18446744073709551615ULL);
  x33 = ((x13)&(x31))|((x5)&(x32));
  x34 = ((uintptr_t)-1ULL)+((in0)==((uintptr_t)0ULL));
  x35 = (x34)^((uintptr_t)18446744073709551615ULL);
  x36 = ((x14)&(x34))|((x6)&(x35));
  x37 = ((uintptr_t)-1ULL)+((in0)==((uintptr_t)0ULL));
  x38 = (x37)^((uintptr_t)18446744073709551615ULL);
  x39 = ((x15)&(x37))|((x7)&(x38));
  x40 = x18;
  x41 = x21;
  x42 = x24;
  x43 = x27;
  x44 = x30;
  x45 = x33;
  x46 = x36;
  x47 = x39;
  /*skip*/
  _br2_store((out0)+((uintptr_t)0ULL), x40, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)8ULL), x41, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)16ULL), x42, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)24ULL), x43, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)32ULL), x44, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)40ULL), x45, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)48ULL), x46, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)56ULL), x47, sizeof(uintptr_t));
  /*skip*/
  return;
}

/* NOTE: The following wrapper function is not covered by Coq proofs */
static void fiat_p448_selectznz(uint64_t out1[8], uint8_t arg1, const uint64_t arg2[8], const uint64_t arg3[8]) {
  internal_fiat_p448_selectznz((uintptr_t)out1, (uintptr_t)arg1, (uintptr_t)arg2, (uintptr_t)arg3);
}


/*
 * Input Bounds:
 *   in0: [[0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000]]
 * Output Bounds:
 *   out0: [[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 internal_fiat_p448_to_bytes(uintptr_t out0, uintptr_t in0) {
  uintptr_t x0, x9, x8, x1, x11, x12, x13, x15, x16, x14, x2, x18, x19, x20, x22, x23, x21, x3, x25, x26, x27, x29, x30, x28, x4, x32, x33, x34, x36, x37, x35, x5, x39, x40, x41, x43, x44, x42, x6, x46, x47, x48, x50, x51, x49, x7, x53, x54, x55, x57, x58, x56, x60, x10, x62, x63, x65, x17, x66, x67, x69, x68, x70, x72, x24, x73, x74, x76, x75, x77, x79, x31, x80, x81, x83, x82, x84, x86, x38, x87, x88, x90, x89, x91, x93, x45, x94, x95, x97, x96, x98, x100, x52, x101, x102, x104, x103, x105, x107, x59, x108, x61, x109, x64, x112, x114, x116, x118, x120, x71, x124, x126, x128, x130, x132, x78, x136, x138, x140, x142, x144, x85, x148, x150, x152, x154, x156, x92, x160, x162, x164, x166, x168, x99, x172, x174, x176, x178, x180, x106, x184, x186, x188, x190, x192, x110, x196, x198, x200, x202, x204, x111, x113, x115, x117, x119, x121, x122, x123, x125, x127, x129, x131, x133, x134, x135, x137, x139, x141, x143, x145, x146, x147, x149, x151, x153, x155, x157, x158, x159, x161, x163, x165, x167, x169, x170, x171, x173, x175, x177, x179, x181, x182, x183, x185, x187, x189, x191, x193, x194, x195, x197, x199, x201, x203, x205, x206, x207, x208, x209, x210, x211, x212, x213, x214, x215, x216, x217, x218, x219, x220, x221, x222, x223, x224, x225, x226, x227, x228, x229, x230, x231, x232, x233, x234, x235, x236, x237, x238, x239, x240, x241, x242, x243, x244, x245, x246, x247, x248, x249, x250, x251, x252, x253, x254, x255, x256, x257, x258, x259, x260, x261, x262;
  x0 = _br2_load((in0)+((uintptr_t)0ULL), sizeof(uintptr_t));
  x1 = _br2_load((in0)+((uintptr_t)8ULL), sizeof(uintptr_t));
  x2 = _br2_load((in0)+((uintptr_t)16ULL), sizeof(uintptr_t));
  x3 = _br2_load((in0)+((uintptr_t)24ULL), sizeof(uintptr_t));
  x4 = _br2_load((in0)+((uintptr_t)32ULL), sizeof(uintptr_t));
  x5 = _br2_load((in0)+((uintptr_t)40ULL), sizeof(uintptr_t));
  x6 = _br2_load((in0)+((uintptr_t)48ULL), sizeof(uintptr_t));
  x7 = _br2_load((in0)+((uintptr_t)56ULL), sizeof(uintptr_t));
  /*skip*/
  /*skip*/
  x8 = (x0)-((uintptr_t)72057594037927935ULL);
  x9 = (x0)<(x8);
  x10 = (x8)&((uintptr_t)72057594037927935ULL);
  x11 = ((x9)<<((uintptr_t)8ULL))-((x8)>>((uintptr_t)56ULL));
  x12 = (x1)-((uintptr_t)72057594037927935ULL);
  x13 = (x1)<(x12);
  x14 = (x12)-(x11);
  x15 = (x12)<(x14);
  x16 = (x13)+(x15);
  x17 = (x14)&((uintptr_t)72057594037927935ULL);
  x18 = ((x16)<<((uintptr_t)8ULL))-((x14)>>((uintptr_t)56ULL));
  x19 = (x2)-((uintptr_t)72057594037927935ULL);
  x20 = (x2)<(x19);
  x21 = (x19)-(x18);
  x22 = (x19)<(x21);
  x23 = (x20)+(x22);
  x24 = (x21)&((uintptr_t)72057594037927935ULL);
  x25 = ((x23)<<((uintptr_t)8ULL))-((x21)>>((uintptr_t)56ULL));
  x26 = (x3)-((uintptr_t)72057594037927935ULL);
  x27 = (x3)<(x26);
  x28 = (x26)-(x25);
  x29 = (x26)<(x28);
  x30 = (x27)+(x29);
  x31 = (x28)&((uintptr_t)72057594037927935ULL);
  x32 = ((x30)<<((uintptr_t)8ULL))-((x28)>>((uintptr_t)56ULL));
  x33 = (x4)-((uintptr_t)72057594037927934ULL);
  x34 = (x4)<(x33);
  x35 = (x33)-(x32);
  x36 = (x33)<(x35);
  x37 = (x34)+(x36);
  x38 = (x35)&((uintptr_t)72057594037927935ULL);
  x39 = ((x37)<<((uintptr_t)8ULL))-((x35)>>((uintptr_t)56ULL));
  x40 = (x5)-((uintptr_t)72057594037927935ULL);
  x41 = (x5)<(x40);
  x42 = (x40)-(x39);
  x43 = (x40)<(x42);
  x44 = (x41)+(x43);
  x45 = (x42)&((uintptr_t)72057594037927935ULL);
  x46 = ((x44)<<((uintptr_t)8ULL))-((x42)>>((uintptr_t)56ULL));
  x47 = (x6)-((uintptr_t)72057594037927935ULL);
  x48 = (x6)<(x47);
  x49 = (x47)-(x46);
  x50 = (x47)<(x49);
  x51 = (x48)+(x50);
  x52 = (x49)&((uintptr_t)72057594037927935ULL);
  x53 = ((x51)<<((uintptr_t)8ULL))-((x49)>>((uintptr_t)56ULL));
  x54 = (x7)-((uintptr_t)72057594037927935ULL);
  x55 = (x7)<(x54);
  x56 = (x54)-(x53);
  x57 = (x54)<(x56);
  x58 = (x55)+(x57);
  x59 = (x56)&((uintptr_t)72057594037927935ULL);
  x60 = ((x58)<<((uintptr_t)8ULL))-((x56)>>((uintptr_t)56ULL));
  x61 = ((uintptr_t)-1ULL)+((x60)==((uintptr_t)0ULL));
  x62 = (x10)+((x61)&((uintptr_t)72057594037927935ULL));
  x63 = (x62)<(x10);
  x64 = (x62)&((uintptr_t)72057594037927935ULL);
  x65 = ((x62)>>((uintptr_t)56ULL))+((x63)<<((uintptr_t)8ULL));
  x66 = (x65)+(x17);
  x67 = (x66)<(x17);
  x68 = (x66)+((x61)&((uintptr_t)72057594037927935ULL));
  x69 = (x68)<((x61)&((uintptr_t)72057594037927935ULL));
  x70 = (x67)+(x69);
  x71 = (x68)&((uintptr_t)72057594037927935ULL);
  x72 = ((x68)>>((uintptr_t)56ULL))+((x70)<<((uintptr_t)8ULL));
  x73 = (x72)+(x24);
  x74 = (x73)<(x24);
  x75 = (x73)+((x61)&((uintptr_t)72057594037927935ULL));
  x76 = (x75)<((x61)&((uintptr_t)72057594037927935ULL));
  x77 = (x74)+(x76);
  x78 = (x75)&((uintptr_t)72057594037927935ULL);
  x79 = ((x75)>>((uintptr_t)56ULL))+((x77)<<((uintptr_t)8ULL));
  x80 = (x79)+(x31);
  x81 = (x80)<(x31);
  x82 = (x80)+((x61)&((uintptr_t)72057594037927935ULL));
  x83 = (x82)<((x61)&((uintptr_t)72057594037927935ULL));
  x84 = (x81)+(x83);
  x85 = (x82)&((uintptr_t)72057594037927935ULL);
  x86 = ((x82)>>((uintptr_t)56ULL))+((x84)<<((uintptr_t)8ULL));
  x87 = (x86)+(x38);
  x88 = (x87)<(x38);
  x89 = (x87)+((x61)&((uintptr_t)72057594037927934ULL));
  x90 = (x89)<((x61)&((uintptr_t)72057594037927934ULL));
  x91 = (x88)+(x90);
  x92 = (x89)&((uintptr_t)72057594037927935ULL);
  x93 = ((x89)>>((uintptr_t)56ULL))+((x91)<<((uintptr_t)8ULL));
  x94 = (x93)+(x45);
  x95 = (x94)<(x45);
  x96 = (x94)+((x61)&((uintptr_t)72057594037927935ULL));
  x97 = (x96)<((x61)&((uintptr_t)72057594037927935ULL));
  x98 = (x95)+(x97);
  x99 = (x96)&((uintptr_t)72057594037927935ULL);
  x100 = ((x96)>>((uintptr_t)56ULL))+((x98)<<((uintptr_t)8ULL));
  x101 = (x100)+(x52);
  x102 = (x101)<(x52);
  x103 = (x101)+((x61)&((uintptr_t)72057594037927935ULL));
  x104 = (x103)<((x61)&((uintptr_t)72057594037927935ULL));
  x105 = (x102)+(x104);
  x106 = (x103)&((uintptr_t)72057594037927935ULL);
  x107 = ((x103)>>((uintptr_t)56ULL))+((x105)<<((uintptr_t)8ULL));
  x108 = (x107)+(x59);
  x109 = (x108)+((x61)&((uintptr_t)72057594037927935ULL));
  x110 = (x109)&((uintptr_t)72057594037927935ULL);
  x111 = (x64)&((uintptr_t)255ULL);
  x112 = (x64)>>((uintptr_t)8ULL);
  x113 = (x112)&((uintptr_t)255ULL);
  x114 = (x112)>>((uintptr_t)8ULL);
  x115 = (x114)&((uintptr_t)255ULL);
  x116 = (x114)>>((uintptr_t)8ULL);
  x117 = (x116)&((uintptr_t)255ULL);
  x118 = (x116)>>((uintptr_t)8ULL);
  x119 = (x118)&((uintptr_t)255ULL);
  x120 = (x118)>>((uintptr_t)8ULL);
  x121 = (x120)&((uintptr_t)255ULL);
  x122 = (x120)>>((uintptr_t)8ULL);
  x123 = (x71)&((uintptr_t)255ULL);
  x124 = (x71)>>((uintptr_t)8ULL);
  x125 = (x124)&((uintptr_t)255ULL);
  x126 = (x124)>>((uintptr_t)8ULL);
  x127 = (x126)&((uintptr_t)255ULL);
  x128 = (x126)>>((uintptr_t)8ULL);
  x129 = (x128)&((uintptr_t)255ULL);
  x130 = (x128)>>((uintptr_t)8ULL);
  x131 = (x130)&((uintptr_t)255ULL);
  x132 = (x130)>>((uintptr_t)8ULL);
  x133 = (x132)&((uintptr_t)255ULL);
  x134 = (x132)>>((uintptr_t)8ULL);
  x135 = (x78)&((uintptr_t)255ULL);
  x136 = (x78)>>((uintptr_t)8ULL);
  x137 = (x136)&((uintptr_t)255ULL);
  x138 = (x136)>>((uintptr_t)8ULL);
  x139 = (x138)&((uintptr_t)255ULL);
  x140 = (x138)>>((uintptr_t)8ULL);
  x141 = (x140)&((uintptr_t)255ULL);
  x142 = (x140)>>((uintptr_t)8ULL);
  x143 = (x142)&((uintptr_t)255ULL);
  x144 = (x142)>>((uintptr_t)8ULL);
  x145 = (x144)&((uintptr_t)255ULL);
  x146 = (x144)>>((uintptr_t)8ULL);
  x147 = (x85)&((uintptr_t)255ULL);
  x148 = (x85)>>((uintptr_t)8ULL);
  x149 = (x148)&((uintptr_t)255ULL);
  x150 = (x148)>>((uintptr_t)8ULL);
  x151 = (x150)&((uintptr_t)255ULL);
  x152 = (x150)>>((uintptr_t)8ULL);
  x153 = (x152)&((uintptr_t)255ULL);
  x154 = (x152)>>((uintptr_t)8ULL);
  x155 = (x154)&((uintptr_t)255ULL);
  x156 = (x154)>>((uintptr_t)8ULL);
  x157 = (x156)&((uintptr_t)255ULL);
  x158 = (x156)>>((uintptr_t)8ULL);
  x159 = (x92)&((uintptr_t)255ULL);
  x160 = (x92)>>((uintptr_t)8ULL);
  x161 = (x160)&((uintptr_t)255ULL);
  x162 = (x160)>>((uintptr_t)8ULL);
  x163 = (x162)&((uintptr_t)255ULL);
  x164 = (x162)>>((uintptr_t)8ULL);
  x165 = (x164)&((uintptr_t)255ULL);
  x166 = (x164)>>((uintptr_t)8ULL);
  x167 = (x166)&((uintptr_t)255ULL);
  x168 = (x166)>>((uintptr_t)8ULL);
  x169 = (x168)&((uintptr_t)255ULL);
  x170 = (x168)>>((uintptr_t)8ULL);
  x171 = (x99)&((uintptr_t)255ULL);
  x172 = (x99)>>((uintptr_t)8ULL);
  x173 = (x172)&((uintptr_t)255ULL);
  x174 = (x172)>>((uintptr_t)8ULL);
  x175 = (x174)&((uintptr_t)255ULL);
  x176 = (x174)>>((uintptr_t)8ULL);
  x177 = (x176)&((uintptr_t)255ULL);
  x178 = (x176)>>((uintptr_t)8ULL);
  x179 = (x178)&((uintptr_t)255ULL);
  x180 = (x178)>>((uintptr_t)8ULL);
  x181 = (x180)&((uintptr_t)255ULL);
  x182 = (x180)>>((uintptr_t)8ULL);
  x183 = (x106)&((uintptr_t)255ULL);
  x184 = (x106)>>((uintptr_t)8ULL);
  x185 = (x184)&((uintptr_t)255ULL);
  x186 = (x184)>>((uintptr_t)8ULL);
  x187 = (x186)&((uintptr_t)255ULL);
  x188 = (x186)>>((uintptr_t)8ULL);
  x189 = (x188)&((uintptr_t)255ULL);
  x190 = (x188)>>((uintptr_t)8ULL);
  x191 = (x190)&((uintptr_t)255ULL);
  x192 = (x190)>>((uintptr_t)8ULL);
  x193 = (x192)&((uintptr_t)255ULL);
  x194 = (x192)>>((uintptr_t)8ULL);
  x195 = (x110)&((uintptr_t)255ULL);
  x196 = (x110)>>((uintptr_t)8ULL);
  x197 = (x196)&((uintptr_t)255ULL);
  x198 = (x196)>>((uintptr_t)8ULL);
  x199 = (x198)&((uintptr_t)255ULL);
  x200 = (x198)>>((uintptr_t)8ULL);
  x201 = (x200)&((uintptr_t)255ULL);
  x202 = (x200)>>((uintptr_t)8ULL);
  x203 = (x202)&((uintptr_t)255ULL);
  x204 = (x202)>>((uintptr_t)8ULL);
  x205 = (x204)&((uintptr_t)255ULL);
  x206 = (x204)>>((uintptr_t)8ULL);
  x207 = x111;
  x208 = x113;
  x209 = x115;
  x210 = x117;
  x211 = x119;
  x212 = x121;
  x213 = x122;
  x214 = x123;
  x215 = x125;
  x216 = x127;
  x217 = x129;
  x218 = x131;
  x219 = x133;
  x220 = x134;
  x221 = x135;
  x222 = x137;
  x223 = x139;
  x224 = x141;
  x225 = x143;
  x226 = x145;
  x227 = x146;
  x228 = x147;
  x229 = x149;
  x230 = x151;
  x231 = x153;
  x232 = x155;
  x233 = x157;
  x234 = x158;
  x235 = x159;
  x236 = x161;
  x237 = x163;
  x238 = x165;
  x239 = x167;
  x240 = x169;
  x241 = x170;
  x242 = x171;
  x243 = x173;
  x244 = x175;
  x245 = x177;
  x246 = x179;
  x247 = x181;
  x248 = x182;
  x249 = x183;
  x250 = x185;
  x251 = x187;
  x252 = x189;
  x253 = x191;
  x254 = x193;
  x255 = x194;
  x256 = x195;
  x257 = x197;
  x258 = x199;
  x259 = x201;
  x260 = x203;
  x261 = x205;
  x262 = x206;
  /*skip*/
  _br2_store((out0)+((uintptr_t)0ULL), x207, 1);
  _br2_store((out0)+((uintptr_t)1ULL), x208, 1);
  _br2_store((out0)+((uintptr_t)2ULL), x209, 1);
  _br2_store((out0)+((uintptr_t)3ULL), x210, 1);
  _br2_store((out0)+((uintptr_t)4ULL), x211, 1);
  _br2_store((out0)+((uintptr_t)5ULL), x212, 1);
  _br2_store((out0)+((uintptr_t)6ULL), x213, 1);
  _br2_store((out0)+((uintptr_t)7ULL), x214, 1);
  _br2_store((out0)+((uintptr_t)8ULL), x215, 1);
  _br2_store((out0)+((uintptr_t)9ULL), x216, 1);
  _br2_store((out0)+((uintptr_t)10ULL), x217, 1);
  _br2_store((out0)+((uintptr_t)11ULL), x218, 1);
  _br2_store((out0)+((uintptr_t)12ULL), x219, 1);
  _br2_store((out0)+((uintptr_t)13ULL), x220, 1);
  _br2_store((out0)+((uintptr_t)14ULL), x221, 1);
  _br2_store((out0)+((uintptr_t)15ULL), x222, 1);
  _br2_store((out0)+((uintptr_t)16ULL), x223, 1);
  _br2_store((out0)+((uintptr_t)17ULL), x224, 1);
  _br2_store((out0)+((uintptr_t)18ULL), x225, 1);
  _br2_store((out0)+((uintptr_t)19ULL), x226, 1);
  _br2_store((out0)+((uintptr_t)20ULL), x227, 1);
  _br2_store((out0)+((uintptr_t)21ULL), x228, 1);
  _br2_store((out0)+((uintptr_t)22ULL), x229, 1);
  _br2_store((out0)+((uintptr_t)23ULL), x230, 1);
  _br2_store((out0)+((uintptr_t)24ULL), x231, 1);
  _br2_store((out0)+((uintptr_t)25ULL), x232, 1);
  _br2_store((out0)+((uintptr_t)26ULL), x233, 1);
  _br2_store((out0)+((uintptr_t)27ULL), x234, 1);
  _br2_store((out0)+((uintptr_t)28ULL), x235, 1);
  _br2_store((out0)+((uintptr_t)29ULL), x236, 1);
  _br2_store((out0)+((uintptr_t)30ULL), x237, 1);
  _br2_store((out0)+((uintptr_t)31ULL), x238, 1);
  _br2_store((out0)+((uintptr_t)32ULL), x239, 1);
  _br2_store((out0)+((uintptr_t)33ULL), x240, 1);
  _br2_store((out0)+((uintptr_t)34ULL), x241, 1);
  _br2_store((out0)+((uintptr_t)35ULL), x242, 1);
  _br2_store((out0)+((uintptr_t)36ULL), x243, 1);
  _br2_store((out0)+((uintptr_t)37ULL), x244, 1);
  _br2_store((out0)+((uintptr_t)38ULL), x245, 1);
  _br2_store((out0)+((uintptr_t)39ULL), x246, 1);
  _br2_store((out0)+((uintptr_t)40ULL), x247, 1);
  _br2_store((out0)+((uintptr_t)41ULL), x248, 1);
  _br2_store((out0)+((uintptr_t)42ULL), x249, 1);
  _br2_store((out0)+((uintptr_t)43ULL), x250, 1);
  _br2_store((out0)+((uintptr_t)44ULL), x251, 1);
  _br2_store((out0)+((uintptr_t)45ULL), x252, 1);
  _br2_store((out0)+((uintptr_t)46ULL), x253, 1);
  _br2_store((out0)+((uintptr_t)47ULL), x254, 1);
  _br2_store((out0)+((uintptr_t)48ULL), x255, 1);
  _br2_store((out0)+((uintptr_t)49ULL), x256, 1);
  _br2_store((out0)+((uintptr_t)50ULL), x257, 1);
  _br2_store((out0)+((uintptr_t)51ULL), x258, 1);
  _br2_store((out0)+((uintptr_t)52ULL), x259, 1);
  _br2_store((out0)+((uintptr_t)53ULL), x260, 1);
  _br2_store((out0)+((uintptr_t)54ULL), x261, 1);
  _br2_store((out0)+((uintptr_t)55ULL), x262, 1);
  /*skip*/
  return;
}

/* NOTE: The following wrapper function is not covered by Coq proofs */
static void fiat_p448_to_bytes(uint8_t out1[56], const uint64_t arg1[8]) {
  internal_fiat_p448_to_bytes((uintptr_t)out1, (uintptr_t)arg1);
}


/*
 * Input Bounds:
 *   in0: [[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:
 *   out0: [[0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000]]
 */
static
void internal_fiat_p448_from_bytes(uintptr_t out0, uintptr_t in0) {
  uintptr_t x55, x54, x53, x52, x51, x50, x49, x48, x47, x46, x45, x44, x43, x42, x41, x40, x39, x38, x37, x36, x35, x34, x33, x32, x31, x30, x29, x28, x27, x26, x25, x24, x23, x22, x21, x20, x19, x18, x17, x16, x15, x14, x13, x12, x11, x10, x9, x8, x7, x6, x5, x4, x3, x2, x1, x0, x110, x111, x109, x112, x108, x113, x107, x114, x106, x115, x105, x116, x103, x104, x102, x118, x101, x119, x100, x120, x99, x121, x98, x122, x96, x97, x95, x124, x94, x125, x93, x126, x92, x127, x91, x128, x89, x90, x88, x130, x87, x131, x86, x132, x85, x133, x84, x134, x82, x83, x81, x136, x80, x137, x79, x138, x78, x139, x77, x140, x75, x76, x74, x142, x73, x143, x72, x144, x71, x145, x70, x146, x68, x69, x67, x148, x66, x149, x65, x150, x64, x151, x63, x152, x61, x62, x60, x154, x59, x155, x58, x156, x57, x157, x56, x158, x117, x123, x129, x135, x141, x147, x153, x159, x160, x161, x162, x163, x164, x165, x166, x167;
  x0 = _br2_load((in0)+((uintptr_t)0ULL), 1);
  x1 = _br2_load((in0)+((uintptr_t)1ULL), 1);
  x2 = _br2_load((in0)+((uintptr_t)2ULL), 1);
  x3 = _br2_load((in0)+((uintptr_t)3ULL), 1);
  x4 = _br2_load((in0)+((uintptr_t)4ULL), 1);
  x5 = _br2_load((in0)+((uintptr_t)5ULL), 1);
  x6 = _br2_load((in0)+((uintptr_t)6ULL), 1);
  x7 = _br2_load((in0)+((uintptr_t)7ULL), 1);
  x8 = _br2_load((in0)+((uintptr_t)8ULL), 1);
  x9 = _br2_load((in0)+((uintptr_t)9ULL), 1);
  x10 = _br2_load((in0)+((uintptr_t)10ULL), 1);
  x11 = _br2_load((in0)+((uintptr_t)11ULL), 1);
  x12 = _br2_load((in0)+((uintptr_t)12ULL), 1);
  x13 = _br2_load((in0)+((uintptr_t)13ULL), 1);
  x14 = _br2_load((in0)+((uintptr_t)14ULL), 1);
  x15 = _br2_load((in0)+((uintptr_t)15ULL), 1);
  x16 = _br2_load((in0)+((uintptr_t)16ULL), 1);
  x17 = _br2_load((in0)+((uintptr_t)17ULL), 1);
  x18 = _br2_load((in0)+((uintptr_t)18ULL), 1);
  x19 = _br2_load((in0)+((uintptr_t)19ULL), 1);
  x20 = _br2_load((in0)+((uintptr_t)20ULL), 1);
  x21 = _br2_load((in0)+((uintptr_t)21ULL), 1);
  x22 = _br2_load((in0)+((uintptr_t)22ULL), 1);
  x23 = _br2_load((in0)+((uintptr_t)23ULL), 1);
  x24 = _br2_load((in0)+((uintptr_t)24ULL), 1);
  x25 = _br2_load((in0)+((uintptr_t)25ULL), 1);
  x26 = _br2_load((in0)+((uintptr_t)26ULL), 1);
  x27 = _br2_load((in0)+((uintptr_t)27ULL), 1);
  x28 = _br2_load((in0)+((uintptr_t)28ULL), 1);
  x29 = _br2_load((in0)+((uintptr_t)29ULL), 1);
  x30 = _br2_load((in0)+((uintptr_t)30ULL), 1);
  x31 = _br2_load((in0)+((uintptr_t)31ULL), 1);
  x32 = _br2_load((in0)+((uintptr_t)32ULL), 1);
  x33 = _br2_load((in0)+((uintptr_t)33ULL), 1);
  x34 = _br2_load((in0)+((uintptr_t)34ULL), 1);
  x35 = _br2_load((in0)+((uintptr_t)35ULL), 1);
  x36 = _br2_load((in0)+((uintptr_t)36ULL), 1);
  x37 = _br2_load((in0)+((uintptr_t)37ULL), 1);
  x38 = _br2_load((in0)+((uintptr_t)38ULL), 1);
  x39 = _br2_load((in0)+((uintptr_t)39ULL), 1);
  x40 = _br2_load((in0)+((uintptr_t)40ULL), 1);
  x41 = _br2_load((in0)+((uintptr_t)41ULL), 1);
  x42 = _br2_load((in0)+((uintptr_t)42ULL), 1);
  x43 = _br2_load((in0)+((uintptr_t)43ULL), 1);
  x44 = _br2_load((in0)+((uintptr_t)44ULL), 1);
  x45 = _br2_load((in0)+((uintptr_t)45ULL), 1);
  x46 = _br2_load((in0)+((uintptr_t)46ULL), 1);
  x47 = _br2_load((in0)+((uintptr_t)47ULL), 1);
  x48 = _br2_load((in0)+((uintptr_t)48ULL), 1);
  x49 = _br2_load((in0)+((uintptr_t)49ULL), 1);
  x50 = _br2_load((in0)+((uintptr_t)50ULL), 1);
  x51 = _br2_load((in0)+((uintptr_t)51ULL), 1);
  x52 = _br2_load((in0)+((uintptr_t)52ULL), 1);
  x53 = _br2_load((in0)+((uintptr_t)53ULL), 1);
  x54 = _br2_load((in0)+((uintptr_t)54ULL), 1);
  x55 = _br2_load((in0)+((uintptr_t)55ULL), 1);
  /*skip*/
  /*skip*/
  x56 = (x55)<<((uintptr_t)48ULL);
  x57 = (x54)<<((uintptr_t)40ULL);
  x58 = (x53)<<((uintptr_t)32ULL);
  x59 = (x52)<<((uintptr_t)24ULL);
  x60 = (x51)<<((uintptr_t)16ULL);
  x61 = (x50)<<((uintptr_t)8ULL);
  x62 = x49;
  x63 = (x48)<<((uintptr_t)48ULL);
  x64 = (x47)<<((uintptr_t)40ULL);
  x65 = (x46)<<((uintptr_t)32ULL);
  x66 = (x45)<<((uintptr_t)24ULL);
  x67 = (x44)<<((uintptr_t)16ULL);
  x68 = (x43)<<((uintptr_t)8ULL);
  x69 = x42;
  x70 = (x41)<<((uintptr_t)48ULL);
  x71 = (x40)<<((uintptr_t)40ULL);
  x72 = (x39)<<((uintptr_t)32ULL);
  x73 = (x38)<<((uintptr_t)24ULL);
  x74 = (x37)<<((uintptr_t)16ULL);
  x75 = (x36)<<((uintptr_t)8ULL);
  x76 = x35;
  x77 = (x34)<<((uintptr_t)48ULL);
  x78 = (x33)<<((uintptr_t)40ULL);
  x79 = (x32)<<((uintptr_t)32ULL);
  x80 = (x31)<<((uintptr_t)24ULL);
  x81 = (x30)<<((uintptr_t)16ULL);
  x82 = (x29)<<((uintptr_t)8ULL);
  x83 = x28;
  x84 = (x27)<<((uintptr_t)48ULL);
  x85 = (x26)<<((uintptr_t)40ULL);
  x86 = (x25)<<((uintptr_t)32ULL);
  x87 = (x24)<<((uintptr_t)24ULL);
  x88 = (x23)<<((uintptr_t)16ULL);
  x89 = (x22)<<((uintptr_t)8ULL);
  x90 = x21;
  x91 = (x20)<<((uintptr_t)48ULL);
  x92 = (x19)<<((uintptr_t)40ULL);
  x93 = (x18)<<((uintptr_t)32ULL);
  x94 = (x17)<<((uintptr_t)24ULL);
  x95 = (x16)<<((uintptr_t)16ULL);
  x96 = (x15)<<((uintptr_t)8ULL);
  x97 = x14;
  x98 = (x13)<<((uintptr_t)48ULL);
  x99 = (x12)<<((uintptr_t)40ULL);
  x100 = (x11)<<((uintptr_t)32ULL);
  x101 = (x10)<<((uintptr_t)24ULL);
  x102 = (x9)<<((uintptr_t)16ULL);
  x103 = (x8)<<((uintptr_t)8ULL);
  x104 = x7;
  x105 = (x6)<<((uintptr_t)48ULL);
  x106 = (x5)<<((uintptr_t)40ULL);
  x107 = (x4)<<((uintptr_t)32ULL);
  x108 = (x3)<<((uintptr_t)24ULL);
  x109 = (x2)<<((uintptr_t)16ULL);
  x110 = (x1)<<((uintptr_t)8ULL);
  x111 = x0;
  x112 = (x110)+(x111);
  x113 = (x109)+(x112);
  x114 = (x108)+(x113);
  x115 = (x107)+(x114);
  x116 = (x106)+(x115);
  x117 = (x105)+(x116);
  x118 = (x103)+(x104);
  x119 = (x102)+(x118);
  x120 = (x101)+(x119);
  x121 = (x100)+(x120);
  x122 = (x99)+(x121);
  x123 = (x98)+(x122);
  x124 = (x96)+(x97);
  x125 = (x95)+(x124);
  x126 = (x94)+(x125);
  x127 = (x93)+(x126);
  x128 = (x92)+(x127);
  x129 = (x91)+(x128);
  x130 = (x89)+(x90);
  x131 = (x88)+(x130);
  x132 = (x87)+(x131);
  x133 = (x86)+(x132);
  x134 = (x85)+(x133);
  x135 = (x84)+(x134);
  x136 = (x82)+(x83);
  x137 = (x81)+(x136);
  x138 = (x80)+(x137);
  x139 = (x79)+(x138);
  x140 = (x78)+(x139);
  x141 = (x77)+(x140);
  x142 = (x75)+(x76);
  x143 = (x74)+(x142);
  x144 = (x73)+(x143);
  x145 = (x72)+(x144);
  x146 = (x71)+(x145);
  x147 = (x70)+(x146);
  x148 = (x68)+(x69);
  x149 = (x67)+(x148);
  x150 = (x66)+(x149);
  x151 = (x65)+(x150);
  x152 = (x64)+(x151);
  x153 = (x63)+(x152);
  x154 = (x61)+(x62);
  x155 = (x60)+(x154);
  x156 = (x59)+(x155);
  x157 = (x58)+(x156);
  x158 = (x57)+(x157);
  x159 = (x56)+(x158);
  x160 = x117;
  x161 = x123;
  x162 = x129;
  x163 = x135;
  x164 = x141;
  x165 = x147;
  x166 = x153;
  x167 = x159;
  /*skip*/
  _br2_store((out0)+((uintptr_t)0ULL), x160, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)8ULL), x161, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)16ULL), x162, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)24ULL), x163, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)32ULL), x164, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)40ULL), x165, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)48ULL), x166, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)56ULL), x167, sizeof(uintptr_t));
  /*skip*/
  return;
}

/* NOTE: The following wrapper function is not covered by Coq proofs */
static void fiat_p448_from_bytes(uint64_t out1[8], const uint8_t arg1[56]) {
  internal_fiat_p448_from_bytes((uintptr_t)out1, (uintptr_t)arg1);
}