p224_32.c

/* Autogenerated: src/ExtractionOCaml/bedrock2_word_by_word_montgomery --lang bedrock2 --static --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select p224 32 '2^224 - 2^96 + 1' mul square add sub opp from_montgomery to_montgomery nonzero selectznz to_bytes from_bytes one msat divstep divstep_precomp */
/* curve description: p224 */
/* machine_wordsize = 32 (from "32") */
/* requested operations: mul, square, add, sub, opp, from_montgomery, to_montgomery, nonzero, selectznz, to_bytes, from_bytes, one, msat, divstep, divstep_precomp */
/* m = 0xffffffffffffffffffffffffffffffff000000000000000000000001 (from "2^224 - 2^96 + 1") */
/*                                                                    */
/* NOTE: In addition to the bounds specified above each function, all */
/*   functions synthesized for this Montgomery arithmetic require the */
/*   input to be strictly less than the prime modulus (m), and also   */
/*   require the input to be in the unique saturated representation.  */
/*   All functions also ensure that these two properties are true of  */
/*   return values.                                                   */
/*  */
/* Computed values: */
/* eval z = z[0] + (z[1] << 32) + (z[2] << 64) + (z[3] << 96) + (z[4] << 128) + (z[5] << 160) + (z[6] << 192) */
/* 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) */

#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 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
 *   in1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
 * Output Bounds:
 *   out0: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
 */
static
void internal_fiat_p224_mul(uintptr_t out0, uintptr_t in0, uintptr_t in1) {
  uintptr_t x1, x2, x3, x4, x5, x6, x0, x20, x31, x34, x36, x32, x37, x29, x38, x40, x41, x30, x42, x27, x43, x45, x46, x28, x47, x25, x48, x50, x51, x26, x52, x23, x53, x55, x56, x24, x57, x21, x58, x60, x61, x22, x68, x71, x73, x69, x74, x66, x75, x77, x78, x67, x79, x64, x80, x82, x83, x65, x63, x85, x33, x86, x35, x88, x39, x90, x44, x91, x70, x92, x94, x95, x49, x96, x72, x97, x99, x100, x54, x101, x76, x102, x104, x105, x59, x106, x81, x107, x109, x110, x62, x111, x84, x112, x114, x14, x126, x129, x131, x127, x132, x124, x133, x135, x136, x125, x137, x122, x138, x140, x141, x123, x142, x120, x143, x145, x146, x121, x147, x118, x148, x150, x151, x119, x152, x116, x153, x155, x156, x117, x128, x87, x159, x89, x160, x130, x161, x163, x164, x93, x165, x134, x166, x168, x169, x98, x170, x139, x171, x173, x174, x103, x175, x144, x176, x178, x179, x108, x180, x149, x181, x183, x184, x113, x185, x154, x186, x188, x189, x115, x190, x157, x191, x193, x200, x203, x205, x201, x206, x198, x207, x209, x210, x199, x211, x196, x212, x214, x215, x197, x195, x217, x158, x218, x162, x220, x167, x222, x172, x223, x202, x224, x226, x227, x177, x228, x204, x229, x231, x232, x182, x233, x208, x234, x236, x237, x187, x238, x213, x239, x241, x242, x192, x243, x216, x244, x246, x247, x194, x15, x259, x262, x264, x260, x265, x257, x266, x268, x269, x258, x270, x255, x271, x273, x274, x256, x275, x253, x276, x278, x279, x254, x280, x251, x281, x283, x284, x252, x285, x249, x286, x288, x289, x250, x261, x219, x292, x221, x293, x263, x294, x296, x297, x225, x298, x267, x299, x301, x302, x230, x303, x272, x304, x306, x307, x235, x308, x277, x309, x311, x312, x240, x313, x282, x314, x316, x317, x245, x318, x287, x319, x321, x322, x248, x323, x290, x324, x326, x333, x336, x338, x334, x339, x331, x340, x342, x343, x332, x344, x329, x345, x347, x348, x330, x328, x350, x291, x351, x295, x353, x300, x355, x305, x356, x335, x357, x359, x360, x310, x361, x337, x362, x364, x365, x315, x366, x341, x367, x369, x370, x320, x371, x346, x372, x374, x375, x325, x376, x349, x377, x379, x380, x327, x16, x392, x395, x397, x393, x398, x390, x399, x401, x402, x391, x403, x388, x404, x406, x407, x389, x408, x386, x409, x411, x412, x387, x413, x384, x414, x416, x417, x385, x418, x382, x419, x421, x422, x383, x394, x352, x425, x354, x426, x396, x427, x429, x430, x358, x431, x400, x432, x434, x435, x363, x436, x405, x437, x439, x440, x368, x441, x410, x442, x444, x445, x373, x446, x415, x447, x449, x450, x378, x451, x420, x452, x454, x455, x381, x456, x423, x457, x459, x466, x469, x471, x467, x472, x464, x473, x475, x476, x465, x477, x462, x478, x480, x481, x463, x461, x483, x424, x484, x428, x486, x433, x488, x438, x489, x468, x490, x492, x493, x443, x494, x470, x495, x497, x498, x448, x499, x474, x500, x502, x503, x453, x504, x479, x505, x507, x508, x458, x509, x482, x510, x512, x513, x460, x17, x525, x528, x530, x526, x531, x523, x532, x534, x535, x524, x536, x521, x537, x539, x540, x522, x541, x519, x542, x544, x545, x520, x546, x517, x547, x549, x550, x518, x551, x515, x552, x554, x555, x516, x527, x485, x558, x487, x559, x529, x560, x562, x563, x491, x564, x533, x565, x567, x568, x496, x569, x538, x570, x572, x573, x501, x574, x543, x575, x577, x578, x506, x579, x548, x580, x582, x583, x511, x584, x553, x585, x587, x588, x514, x589, x556, x590, x592, x599, x602, x604, x600, x605, x597, x606, x608, x609, x598, x610, x595, x611, x613, x614, x596, x594, x616, x557, x617, x561, x619, x566, x621, x571, x622, x601, x623, x625, x626, x576, x627, x603, x628, x630, x631, x581, x632, x607, x633, x635, x636, x586, x637, x612, x638, x640, x641, x591, x642, x615, x643, x645, x646, x593, x18, x658, x661, x663, x659, x664, x656, x665, x667, x668, x657, x669, x654, x670, x672, x673, x655, x674, x652, x675, x677, x678, x653, x679, x650, x680, x682, x683, x651, x684, x648, x685, x687, x688, x649, x660, x618, x691, x620, x692, x662, x693, x695, x696, x624, x697, x666, x698, x700, x701, x629, x702, x671, x703, x705, x706, x634, x707, x676, x708, x710, x711, x639, x712, x681, x713, x715, x716, x644, x717, x686, x718, x720, x721, x647, x722, x689, x723, x725, x732, x735, x737, x733, x738, x730, x739, x741, x742, x731, x743, x728, x744, x746, x747, x729, x727, x749, x690, x750, x694, x752, x699, x754, x704, x755, x734, x756, x758, x759, x709, x760, x736, x761, x763, x764, x714, x765, x740, x766, x768, x769, x719, x770, x745, x771, x773, x774, x724, x775, x748, x776, x778, x779, x726, x13, x12, x11, x10, x9, x8, x19, x7, x791, x794, x796, x792, x797, x789, x798, x800, x801, x790, x802, x787, x803, x805, x806, x788, x807, x785, x808, x810, x811, x786, x812, x783, x813, x815, x816, x784, x817, x781, x818, x820, x821, x782, x793, x751, x824, x753, x825, x795, x826, x828, x829, x757, x830, x799, x831, x833, x834, x762, x835, x804, x836, x838, x839, x767, x840, x809, x841, x843, x844, x772, x845, x814, x846, x848, x849, x777, x850, x819, x851, x853, x854, x780, x855, x822, x856, x858, x865, x868, x870, x866, x871, x863, x872, x874, x875, x864, x876, x861, x877, x879, x880, x862, x860, x882, x823, x883, x827, x885, x832, x887, x837, x888, x867, x889, x891, x892, x842, x893, x869, x894, x896, x897, x847, x898, x873, x899, x901, x902, x852, x903, x878, x904, x906, x907, x857, x908, x881, x909, x911, x912, x859, x915, x917, x919, x920, x921, x923, x924, x925, x926, x928, x929, x930, x931, x933, x934, x935, x936, x938, x939, x913, x940, x884, x942, x914, x943, x886, x945, x916, x946, x890, x948, x918, x949, x895, x951, x922, x952, x900, x954, x927, x955, x905, x957, x932, x958, x941, x910, x960, x937, x961, x944, x947, x950, x953, x956, x959, x962, x963, x964, x965, x966, x967, x968, x969;
  x0 = _br2_load((in0)+((uintptr_t)0ULL), sizeof(uintptr_t));
  x1 = _br2_load((in0)+((uintptr_t)4ULL), sizeof(uintptr_t));
  x2 = _br2_load((in0)+((uintptr_t)8ULL), sizeof(uintptr_t));
  x3 = _br2_load((in0)+((uintptr_t)12ULL), sizeof(uintptr_t));
  x4 = _br2_load((in0)+((uintptr_t)16ULL), sizeof(uintptr_t));
  x5 = _br2_load((in0)+((uintptr_t)20ULL), sizeof(uintptr_t));
  x6 = _br2_load((in0)+((uintptr_t)24ULL), sizeof(uintptr_t));
  /*skip*/
  x7 = _br2_load((in1)+((uintptr_t)0ULL), sizeof(uintptr_t));
  x8 = _br2_load((in1)+((uintptr_t)4ULL), sizeof(uintptr_t));
  x9 = _br2_load((in1)+((uintptr_t)8ULL), sizeof(uintptr_t));
  x10 = _br2_load((in1)+((uintptr_t)12ULL), sizeof(uintptr_t));
  x11 = _br2_load((in1)+((uintptr_t)16ULL), sizeof(uintptr_t));
  x12 = _br2_load((in1)+((uintptr_t)20ULL), sizeof(uintptr_t));
  x13 = _br2_load((in1)+((uintptr_t)24ULL), sizeof(uintptr_t));
  /*skip*/
  /*skip*/
  x14 = x1;
  x15 = x2;
  x16 = x3;
  x17 = x4;
  x18 = x5;
  x19 = x6;
  x20 = x0;
  x21 = (x20)*(x13);
  x22 = sizeof(intptr_t) == 4 ? ((uint64_t)(x20)*(x13))>>32 : ((__uint128_t)(x20)*(x13))>>64;
  x23 = (x20)*(x12);
  x24 = sizeof(intptr_t) == 4 ? ((uint64_t)(x20)*(x12))>>32 : ((__uint128_t)(x20)*(x12))>>64;
  x25 = (x20)*(x11);
  x26 = sizeof(intptr_t) == 4 ? ((uint64_t)(x20)*(x11))>>32 : ((__uint128_t)(x20)*(x11))>>64;
  x27 = (x20)*(x10);
  x28 = sizeof(intptr_t) == 4 ? ((uint64_t)(x20)*(x10))>>32 : ((__uint128_t)(x20)*(x10))>>64;
  x29 = (x20)*(x9);
  x30 = sizeof(intptr_t) == 4 ? ((uint64_t)(x20)*(x9))>>32 : ((__uint128_t)(x20)*(x9))>>64;
  x31 = (x20)*(x8);
  x32 = sizeof(intptr_t) == 4 ? ((uint64_t)(x20)*(x8))>>32 : ((__uint128_t)(x20)*(x8))>>64;
  x33 = (x20)*(x7);
  x34 = sizeof(intptr_t) == 4 ? ((uint64_t)(x20)*(x7))>>32 : ((__uint128_t)(x20)*(x7))>>64;
  x35 = (x34)+(x31);
  x36 = (x35)<(x34);
  x37 = (x36)+(x32);
  x38 = (x37)<(x32);
  x39 = (x37)+(x29);
  x40 = (x39)<(x29);
  x41 = (x38)+(x40);
  x42 = (x41)+(x30);
  x43 = (x42)<(x30);
  x44 = (x42)+(x27);
  x45 = (x44)<(x27);
  x46 = (x43)+(x45);
  x47 = (x46)+(x28);
  x48 = (x47)<(x28);
  x49 = (x47)+(x25);
  x50 = (x49)<(x25);
  x51 = (x48)+(x50);
  x52 = (x51)+(x26);
  x53 = (x52)<(x26);
  x54 = (x52)+(x23);
  x55 = (x54)<(x23);
  x56 = (x53)+(x55);
  x57 = (x56)+(x24);
  x58 = (x57)<(x24);
  x59 = (x57)+(x21);
  x60 = (x59)<(x21);
  x61 = (x58)+(x60);
  x62 = (x61)+(x22);
  x63 = (x33)*((uintptr_t)4294967295ULL);
  x64 = (x63)*((uintptr_t)4294967295ULL);
  x65 = sizeof(intptr_t) == 4 ? ((uint64_t)(x63)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x63)*((uintptr_t)4294967295ULL))>>64;
  x66 = (x63)*((uintptr_t)4294967295ULL);
  x67 = sizeof(intptr_t) == 4 ? ((uint64_t)(x63)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x63)*((uintptr_t)4294967295ULL))>>64;
  x68 = (x63)*((uintptr_t)4294967295ULL);
  x69 = sizeof(intptr_t) == 4 ? ((uint64_t)(x63)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x63)*((uintptr_t)4294967295ULL))>>64;
  x70 = (x63)*((uintptr_t)4294967295ULL);
  x71 = sizeof(intptr_t) == 4 ? ((uint64_t)(x63)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x63)*((uintptr_t)4294967295ULL))>>64;
  x72 = (x71)+(x68);
  x73 = (x72)<(x71);
  x74 = (x73)+(x69);
  x75 = (x74)<(x69);
  x76 = (x74)+(x66);
  x77 = (x76)<(x66);
  x78 = (x75)+(x77);
  x79 = (x78)+(x67);
  x80 = (x79)<(x67);
  x81 = (x79)+(x64);
  x82 = (x81)<(x64);
  x83 = (x80)+(x82);
  x84 = (x83)+(x65);
  x85 = (x33)+(x63);
  x86 = (x85)<(x33);
  x87 = (x86)+(x35);
  x88 = (x87)<(x35);
  x89 = (x88)+(x39);
  x90 = (x89)<(x39);
  x91 = (x90)+(x44);
  x92 = (x91)<(x44);
  x93 = (x91)+(x70);
  x94 = (x93)<(x70);
  x95 = (x92)+(x94);
  x96 = (x95)+(x49);
  x97 = (x96)<(x49);
  x98 = (x96)+(x72);
  x99 = (x98)<(x72);
  x100 = (x97)+(x99);
  x101 = (x100)+(x54);
  x102 = (x101)<(x54);
  x103 = (x101)+(x76);
  x104 = (x103)<(x76);
  x105 = (x102)+(x104);
  x106 = (x105)+(x59);
  x107 = (x106)<(x59);
  x108 = (x106)+(x81);
  x109 = (x108)<(x81);
  x110 = (x107)+(x109);
  x111 = (x110)+(x62);
  x112 = (x111)<(x62);
  x113 = (x111)+(x84);
  x114 = (x113)<(x84);
  x115 = (x112)+(x114);
  x116 = (x14)*(x13);
  x117 = sizeof(intptr_t) == 4 ? ((uint64_t)(x14)*(x13))>>32 : ((__uint128_t)(x14)*(x13))>>64;
  x118 = (x14)*(x12);
  x119 = sizeof(intptr_t) == 4 ? ((uint64_t)(x14)*(x12))>>32 : ((__uint128_t)(x14)*(x12))>>64;
  x120 = (x14)*(x11);
  x121 = sizeof(intptr_t) == 4 ? ((uint64_t)(x14)*(x11))>>32 : ((__uint128_t)(x14)*(x11))>>64;
  x122 = (x14)*(x10);
  x123 = sizeof(intptr_t) == 4 ? ((uint64_t)(x14)*(x10))>>32 : ((__uint128_t)(x14)*(x10))>>64;
  x124 = (x14)*(x9);
  x125 = sizeof(intptr_t) == 4 ? ((uint64_t)(x14)*(x9))>>32 : ((__uint128_t)(x14)*(x9))>>64;
  x126 = (x14)*(x8);
  x127 = sizeof(intptr_t) == 4 ? ((uint64_t)(x14)*(x8))>>32 : ((__uint128_t)(x14)*(x8))>>64;
  x128 = (x14)*(x7);
  x129 = sizeof(intptr_t) == 4 ? ((uint64_t)(x14)*(x7))>>32 : ((__uint128_t)(x14)*(x7))>>64;
  x130 = (x129)+(x126);
  x131 = (x130)<(x129);
  x132 = (x131)+(x127);
  x133 = (x132)<(x127);
  x134 = (x132)+(x124);
  x135 = (x134)<(x124);
  x136 = (x133)+(x135);
  x137 = (x136)+(x125);
  x138 = (x137)<(x125);
  x139 = (x137)+(x122);
  x140 = (x139)<(x122);
  x141 = (x138)+(x140);
  x142 = (x141)+(x123);
  x143 = (x142)<(x123);
  x144 = (x142)+(x120);
  x145 = (x144)<(x120);
  x146 = (x143)+(x145);
  x147 = (x146)+(x121);
  x148 = (x147)<(x121);
  x149 = (x147)+(x118);
  x150 = (x149)<(x118);
  x151 = (x148)+(x150);
  x152 = (x151)+(x119);
  x153 = (x152)<(x119);
  x154 = (x152)+(x116);
  x155 = (x154)<(x116);
  x156 = (x153)+(x155);
  x157 = (x156)+(x117);
  x158 = (x87)+(x128);
  x159 = (x158)<(x87);
  x160 = (x159)+(x89);
  x161 = (x160)<(x89);
  x162 = (x160)+(x130);
  x163 = (x162)<(x130);
  x164 = (x161)+(x163);
  x165 = (x164)+(x93);
  x166 = (x165)<(x93);
  x167 = (x165)+(x134);
  x168 = (x167)<(x134);
  x169 = (x166)+(x168);
  x170 = (x169)+(x98);
  x171 = (x170)<(x98);
  x172 = (x170)+(x139);
  x173 = (x172)<(x139);
  x174 = (x171)+(x173);
  x175 = (x174)+(x103);
  x176 = (x175)<(x103);
  x177 = (x175)+(x144);
  x178 = (x177)<(x144);
  x179 = (x176)+(x178);
  x180 = (x179)+(x108);
  x181 = (x180)<(x108);
  x182 = (x180)+(x149);
  x183 = (x182)<(x149);
  x184 = (x181)+(x183);
  x185 = (x184)+(x113);
  x186 = (x185)<(x113);
  x187 = (x185)+(x154);
  x188 = (x187)<(x154);
  x189 = (x186)+(x188);
  x190 = (x189)+(x115);
  x191 = (x190)<(x115);
  x192 = (x190)+(x157);
  x193 = (x192)<(x157);
  x194 = (x191)+(x193);
  x195 = (x158)*((uintptr_t)4294967295ULL);
  x196 = (x195)*((uintptr_t)4294967295ULL);
  x197 = sizeof(intptr_t) == 4 ? ((uint64_t)(x195)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x195)*((uintptr_t)4294967295ULL))>>64;
  x198 = (x195)*((uintptr_t)4294967295ULL);
  x199 = sizeof(intptr_t) == 4 ? ((uint64_t)(x195)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x195)*((uintptr_t)4294967295ULL))>>64;
  x200 = (x195)*((uintptr_t)4294967295ULL);
  x201 = sizeof(intptr_t) == 4 ? ((uint64_t)(x195)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x195)*((uintptr_t)4294967295ULL))>>64;
  x202 = (x195)*((uintptr_t)4294967295ULL);
  x203 = sizeof(intptr_t) == 4 ? ((uint64_t)(x195)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x195)*((uintptr_t)4294967295ULL))>>64;
  x204 = (x203)+(x200);
  x205 = (x204)<(x203);
  x206 = (x205)+(x201);
  x207 = (x206)<(x201);
  x208 = (x206)+(x198);
  x209 = (x208)<(x198);
  x210 = (x207)+(x209);
  x211 = (x210)+(x199);
  x212 = (x211)<(x199);
  x213 = (x211)+(x196);
  x214 = (x213)<(x196);
  x215 = (x212)+(x214);
  x216 = (x215)+(x197);
  x217 = (x158)+(x195);
  x218 = (x217)<(x158);
  x219 = (x218)+(x162);
  x220 = (x219)<(x162);
  x221 = (x220)+(x167);
  x222 = (x221)<(x167);
  x223 = (x222)+(x172);
  x224 = (x223)<(x172);
  x225 = (x223)+(x202);
  x226 = (x225)<(x202);
  x227 = (x224)+(x226);
  x228 = (x227)+(x177);
  x229 = (x228)<(x177);
  x230 = (x228)+(x204);
  x231 = (x230)<(x204);
  x232 = (x229)+(x231);
  x233 = (x232)+(x182);
  x234 = (x233)<(x182);
  x235 = (x233)+(x208);
  x236 = (x235)<(x208);
  x237 = (x234)+(x236);
  x238 = (x237)+(x187);
  x239 = (x238)<(x187);
  x240 = (x238)+(x213);
  x241 = (x240)<(x213);
  x242 = (x239)+(x241);
  x243 = (x242)+(x192);
  x244 = (x243)<(x192);
  x245 = (x243)+(x216);
  x246 = (x245)<(x216);
  x247 = (x244)+(x246);
  x248 = (x247)+(x194);
  x249 = (x15)*(x13);
  x250 = sizeof(intptr_t) == 4 ? ((uint64_t)(x15)*(x13))>>32 : ((__uint128_t)(x15)*(x13))>>64;
  x251 = (x15)*(x12);
  x252 = sizeof(intptr_t) == 4 ? ((uint64_t)(x15)*(x12))>>32 : ((__uint128_t)(x15)*(x12))>>64;
  x253 = (x15)*(x11);
  x254 = sizeof(intptr_t) == 4 ? ((uint64_t)(x15)*(x11))>>32 : ((__uint128_t)(x15)*(x11))>>64;
  x255 = (x15)*(x10);
  x256 = sizeof(intptr_t) == 4 ? ((uint64_t)(x15)*(x10))>>32 : ((__uint128_t)(x15)*(x10))>>64;
  x257 = (x15)*(x9);
  x258 = sizeof(intptr_t) == 4 ? ((uint64_t)(x15)*(x9))>>32 : ((__uint128_t)(x15)*(x9))>>64;
  x259 = (x15)*(x8);
  x260 = sizeof(intptr_t) == 4 ? ((uint64_t)(x15)*(x8))>>32 : ((__uint128_t)(x15)*(x8))>>64;
  x261 = (x15)*(x7);
  x262 = sizeof(intptr_t) == 4 ? ((uint64_t)(x15)*(x7))>>32 : ((__uint128_t)(x15)*(x7))>>64;
  x263 = (x262)+(x259);
  x264 = (x263)<(x262);
  x265 = (x264)+(x260);
  x266 = (x265)<(x260);
  x267 = (x265)+(x257);
  x268 = (x267)<(x257);
  x269 = (x266)+(x268);
  x270 = (x269)+(x258);
  x271 = (x270)<(x258);
  x272 = (x270)+(x255);
  x273 = (x272)<(x255);
  x274 = (x271)+(x273);
  x275 = (x274)+(x256);
  x276 = (x275)<(x256);
  x277 = (x275)+(x253);
  x278 = (x277)<(x253);
  x279 = (x276)+(x278);
  x280 = (x279)+(x254);
  x281 = (x280)<(x254);
  x282 = (x280)+(x251);
  x283 = (x282)<(x251);
  x284 = (x281)+(x283);
  x285 = (x284)+(x252);
  x286 = (x285)<(x252);
  x287 = (x285)+(x249);
  x288 = (x287)<(x249);
  x289 = (x286)+(x288);
  x290 = (x289)+(x250);
  x291 = (x219)+(x261);
  x292 = (x291)<(x219);
  x293 = (x292)+(x221);
  x294 = (x293)<(x221);
  x295 = (x293)+(x263);
  x296 = (x295)<(x263);
  x297 = (x294)+(x296);
  x298 = (x297)+(x225);
  x299 = (x298)<(x225);
  x300 = (x298)+(x267);
  x301 = (x300)<(x267);
  x302 = (x299)+(x301);
  x303 = (x302)+(x230);
  x304 = (x303)<(x230);
  x305 = (x303)+(x272);
  x306 = (x305)<(x272);
  x307 = (x304)+(x306);
  x308 = (x307)+(x235);
  x309 = (x308)<(x235);
  x310 = (x308)+(x277);
  x311 = (x310)<(x277);
  x312 = (x309)+(x311);
  x313 = (x312)+(x240);
  x314 = (x313)<(x240);
  x315 = (x313)+(x282);
  x316 = (x315)<(x282);
  x317 = (x314)+(x316);
  x318 = (x317)+(x245);
  x319 = (x318)<(x245);
  x320 = (x318)+(x287);
  x321 = (x320)<(x287);
  x322 = (x319)+(x321);
  x323 = (x322)+(x248);
  x324 = (x323)<(x248);
  x325 = (x323)+(x290);
  x326 = (x325)<(x290);
  x327 = (x324)+(x326);
  x328 = (x291)*((uintptr_t)4294967295ULL);
  x329 = (x328)*((uintptr_t)4294967295ULL);
  x330 = sizeof(intptr_t) == 4 ? ((uint64_t)(x328)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x328)*((uintptr_t)4294967295ULL))>>64;
  x331 = (x328)*((uintptr_t)4294967295ULL);
  x332 = sizeof(intptr_t) == 4 ? ((uint64_t)(x328)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x328)*((uintptr_t)4294967295ULL))>>64;
  x333 = (x328)*((uintptr_t)4294967295ULL);
  x334 = sizeof(intptr_t) == 4 ? ((uint64_t)(x328)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x328)*((uintptr_t)4294967295ULL))>>64;
  x335 = (x328)*((uintptr_t)4294967295ULL);
  x336 = sizeof(intptr_t) == 4 ? ((uint64_t)(x328)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x328)*((uintptr_t)4294967295ULL))>>64;
  x337 = (x336)+(x333);
  x338 = (x337)<(x336);
  x339 = (x338)+(x334);
  x340 = (x339)<(x334);
  x341 = (x339)+(x331);
  x342 = (x341)<(x331);
  x343 = (x340)+(x342);
  x344 = (x343)+(x332);
  x345 = (x344)<(x332);
  x346 = (x344)+(x329);
  x347 = (x346)<(x329);
  x348 = (x345)+(x347);
  x349 = (x348)+(x330);
  x350 = (x291)+(x328);
  x351 = (x350)<(x291);
  x352 = (x351)+(x295);
  x353 = (x352)<(x295);
  x354 = (x353)+(x300);
  x355 = (x354)<(x300);
  x356 = (x355)+(x305);
  x357 = (x356)<(x305);
  x358 = (x356)+(x335);
  x359 = (x358)<(x335);
  x360 = (x357)+(x359);
  x361 = (x360)+(x310);
  x362 = (x361)<(x310);
  x363 = (x361)+(x337);
  x364 = (x363)<(x337);
  x365 = (x362)+(x364);
  x366 = (x365)+(x315);
  x367 = (x366)<(x315);
  x368 = (x366)+(x341);
  x369 = (x368)<(x341);
  x370 = (x367)+(x369);
  x371 = (x370)+(x320);
  x372 = (x371)<(x320);
  x373 = (x371)+(x346);
  x374 = (x373)<(x346);
  x375 = (x372)+(x374);
  x376 = (x375)+(x325);
  x377 = (x376)<(x325);
  x378 = (x376)+(x349);
  x379 = (x378)<(x349);
  x380 = (x377)+(x379);
  x381 = (x380)+(x327);
  x382 = (x16)*(x13);
  x383 = sizeof(intptr_t) == 4 ? ((uint64_t)(x16)*(x13))>>32 : ((__uint128_t)(x16)*(x13))>>64;
  x384 = (x16)*(x12);
  x385 = sizeof(intptr_t) == 4 ? ((uint64_t)(x16)*(x12))>>32 : ((__uint128_t)(x16)*(x12))>>64;
  x386 = (x16)*(x11);
  x387 = sizeof(intptr_t) == 4 ? ((uint64_t)(x16)*(x11))>>32 : ((__uint128_t)(x16)*(x11))>>64;
  x388 = (x16)*(x10);
  x389 = sizeof(intptr_t) == 4 ? ((uint64_t)(x16)*(x10))>>32 : ((__uint128_t)(x16)*(x10))>>64;
  x390 = (x16)*(x9);
  x391 = sizeof(intptr_t) == 4 ? ((uint64_t)(x16)*(x9))>>32 : ((__uint128_t)(x16)*(x9))>>64;
  x392 = (x16)*(x8);
  x393 = sizeof(intptr_t) == 4 ? ((uint64_t)(x16)*(x8))>>32 : ((__uint128_t)(x16)*(x8))>>64;
  x394 = (x16)*(x7);
  x395 = sizeof(intptr_t) == 4 ? ((uint64_t)(x16)*(x7))>>32 : ((__uint128_t)(x16)*(x7))>>64;
  x396 = (x395)+(x392);
  x397 = (x396)<(x395);
  x398 = (x397)+(x393);
  x399 = (x398)<(x393);
  x400 = (x398)+(x390);
  x401 = (x400)<(x390);
  x402 = (x399)+(x401);
  x403 = (x402)+(x391);
  x404 = (x403)<(x391);
  x405 = (x403)+(x388);
  x406 = (x405)<(x388);
  x407 = (x404)+(x406);
  x408 = (x407)+(x389);
  x409 = (x408)<(x389);
  x410 = (x408)+(x386);
  x411 = (x410)<(x386);
  x412 = (x409)+(x411);
  x413 = (x412)+(x387);
  x414 = (x413)<(x387);
  x415 = (x413)+(x384);
  x416 = (x415)<(x384);
  x417 = (x414)+(x416);
  x418 = (x417)+(x385);
  x419 = (x418)<(x385);
  x420 = (x418)+(x382);
  x421 = (x420)<(x382);
  x422 = (x419)+(x421);
  x423 = (x422)+(x383);
  x424 = (x352)+(x394);
  x425 = (x424)<(x352);
  x426 = (x425)+(x354);
  x427 = (x426)<(x354);
  x428 = (x426)+(x396);
  x429 = (x428)<(x396);
  x430 = (x427)+(x429);
  x431 = (x430)+(x358);
  x432 = (x431)<(x358);
  x433 = (x431)+(x400);
  x434 = (x433)<(x400);
  x435 = (x432)+(x434);
  x436 = (x435)+(x363);
  x437 = (x436)<(x363);
  x438 = (x436)+(x405);
  x439 = (x438)<(x405);
  x440 = (x437)+(x439);
  x441 = (x440)+(x368);
  x442 = (x441)<(x368);
  x443 = (x441)+(x410);
  x444 = (x443)<(x410);
  x445 = (x442)+(x444);
  x446 = (x445)+(x373);
  x447 = (x446)<(x373);
  x448 = (x446)+(x415);
  x449 = (x448)<(x415);
  x450 = (x447)+(x449);
  x451 = (x450)+(x378);
  x452 = (x451)<(x378);
  x453 = (x451)+(x420);
  x454 = (x453)<(x420);
  x455 = (x452)+(x454);
  x456 = (x455)+(x381);
  x457 = (x456)<(x381);
  x458 = (x456)+(x423);
  x459 = (x458)<(x423);
  x460 = (x457)+(x459);
  x461 = (x424)*((uintptr_t)4294967295ULL);
  x462 = (x461)*((uintptr_t)4294967295ULL);
  x463 = sizeof(intptr_t) == 4 ? ((uint64_t)(x461)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x461)*((uintptr_t)4294967295ULL))>>64;
  x464 = (x461)*((uintptr_t)4294967295ULL);
  x465 = sizeof(intptr_t) == 4 ? ((uint64_t)(x461)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x461)*((uintptr_t)4294967295ULL))>>64;
  x466 = (x461)*((uintptr_t)4294967295ULL);
  x467 = sizeof(intptr_t) == 4 ? ((uint64_t)(x461)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x461)*((uintptr_t)4294967295ULL))>>64;
  x468 = (x461)*((uintptr_t)4294967295ULL);
  x469 = sizeof(intptr_t) == 4 ? ((uint64_t)(x461)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x461)*((uintptr_t)4294967295ULL))>>64;
  x470 = (x469)+(x466);
  x471 = (x470)<(x469);
  x472 = (x471)+(x467);
  x473 = (x472)<(x467);
  x474 = (x472)+(x464);
  x475 = (x474)<(x464);
  x476 = (x473)+(x475);
  x477 = (x476)+(x465);
  x478 = (x477)<(x465);
  x479 = (x477)+(x462);
  x480 = (x479)<(x462);
  x481 = (x478)+(x480);
  x482 = (x481)+(x463);
  x483 = (x424)+(x461);
  x484 = (x483)<(x424);
  x485 = (x484)+(x428);
  x486 = (x485)<(x428);
  x487 = (x486)+(x433);
  x488 = (x487)<(x433);
  x489 = (x488)+(x438);
  x490 = (x489)<(x438);
  x491 = (x489)+(x468);
  x492 = (x491)<(x468);
  x493 = (x490)+(x492);
  x494 = (x493)+(x443);
  x495 = (x494)<(x443);
  x496 = (x494)+(x470);
  x497 = (x496)<(x470);
  x498 = (x495)+(x497);
  x499 = (x498)+(x448);
  x500 = (x499)<(x448);
  x501 = (x499)+(x474);
  x502 = (x501)<(x474);
  x503 = (x500)+(x502);
  x504 = (x503)+(x453);
  x505 = (x504)<(x453);
  x506 = (x504)+(x479);
  x507 = (x506)<(x479);
  x508 = (x505)+(x507);
  x509 = (x508)+(x458);
  x510 = (x509)<(x458);
  x511 = (x509)+(x482);
  x512 = (x511)<(x482);
  x513 = (x510)+(x512);
  x514 = (x513)+(x460);
  x515 = (x17)*(x13);
  x516 = sizeof(intptr_t) == 4 ? ((uint64_t)(x17)*(x13))>>32 : ((__uint128_t)(x17)*(x13))>>64;
  x517 = (x17)*(x12);
  x518 = sizeof(intptr_t) == 4 ? ((uint64_t)(x17)*(x12))>>32 : ((__uint128_t)(x17)*(x12))>>64;
  x519 = (x17)*(x11);
  x520 = sizeof(intptr_t) == 4 ? ((uint64_t)(x17)*(x11))>>32 : ((__uint128_t)(x17)*(x11))>>64;
  x521 = (x17)*(x10);
  x522 = sizeof(intptr_t) == 4 ? ((uint64_t)(x17)*(x10))>>32 : ((__uint128_t)(x17)*(x10))>>64;
  x523 = (x17)*(x9);
  x524 = sizeof(intptr_t) == 4 ? ((uint64_t)(x17)*(x9))>>32 : ((__uint128_t)(x17)*(x9))>>64;
  x525 = (x17)*(x8);
  x526 = sizeof(intptr_t) == 4 ? ((uint64_t)(x17)*(x8))>>32 : ((__uint128_t)(x17)*(x8))>>64;
  x527 = (x17)*(x7);
  x528 = sizeof(intptr_t) == 4 ? ((uint64_t)(x17)*(x7))>>32 : ((__uint128_t)(x17)*(x7))>>64;
  x529 = (x528)+(x525);
  x530 = (x529)<(x528);
  x531 = (x530)+(x526);
  x532 = (x531)<(x526);
  x533 = (x531)+(x523);
  x534 = (x533)<(x523);
  x535 = (x532)+(x534);
  x536 = (x535)+(x524);
  x537 = (x536)<(x524);
  x538 = (x536)+(x521);
  x539 = (x538)<(x521);
  x540 = (x537)+(x539);
  x541 = (x540)+(x522);
  x542 = (x541)<(x522);
  x543 = (x541)+(x519);
  x544 = (x543)<(x519);
  x545 = (x542)+(x544);
  x546 = (x545)+(x520);
  x547 = (x546)<(x520);
  x548 = (x546)+(x517);
  x549 = (x548)<(x517);
  x550 = (x547)+(x549);
  x551 = (x550)+(x518);
  x552 = (x551)<(x518);
  x553 = (x551)+(x515);
  x554 = (x553)<(x515);
  x555 = (x552)+(x554);
  x556 = (x555)+(x516);
  x557 = (x485)+(x527);
  x558 = (x557)<(x485);
  x559 = (x558)+(x487);
  x560 = (x559)<(x487);
  x561 = (x559)+(x529);
  x562 = (x561)<(x529);
  x563 = (x560)+(x562);
  x564 = (x563)+(x491);
  x565 = (x564)<(x491);
  x566 = (x564)+(x533);
  x567 = (x566)<(x533);
  x568 = (x565)+(x567);
  x569 = (x568)+(x496);
  x570 = (x569)<(x496);
  x571 = (x569)+(x538);
  x572 = (x571)<(x538);
  x573 = (x570)+(x572);
  x574 = (x573)+(x501);
  x575 = (x574)<(x501);
  x576 = (x574)+(x543);
  x577 = (x576)<(x543);
  x578 = (x575)+(x577);
  x579 = (x578)+(x506);
  x580 = (x579)<(x506);
  x581 = (x579)+(x548);
  x582 = (x581)<(x548);
  x583 = (x580)+(x582);
  x584 = (x583)+(x511);
  x585 = (x584)<(x511);
  x586 = (x584)+(x553);
  x587 = (x586)<(x553);
  x588 = (x585)+(x587);
  x589 = (x588)+(x514);
  x590 = (x589)<(x514);
  x591 = (x589)+(x556);
  x592 = (x591)<(x556);
  x593 = (x590)+(x592);
  x594 = (x557)*((uintptr_t)4294967295ULL);
  x595 = (x594)*((uintptr_t)4294967295ULL);
  x596 = sizeof(intptr_t) == 4 ? ((uint64_t)(x594)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x594)*((uintptr_t)4294967295ULL))>>64;
  x597 = (x594)*((uintptr_t)4294967295ULL);
  x598 = sizeof(intptr_t) == 4 ? ((uint64_t)(x594)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x594)*((uintptr_t)4294967295ULL))>>64;
  x599 = (x594)*((uintptr_t)4294967295ULL);
  x600 = sizeof(intptr_t) == 4 ? ((uint64_t)(x594)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x594)*((uintptr_t)4294967295ULL))>>64;
  x601 = (x594)*((uintptr_t)4294967295ULL);
  x602 = sizeof(intptr_t) == 4 ? ((uint64_t)(x594)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x594)*((uintptr_t)4294967295ULL))>>64;
  x603 = (x602)+(x599);
  x604 = (x603)<(x602);
  x605 = (x604)+(x600);
  x606 = (x605)<(x600);
  x607 = (x605)+(x597);
  x608 = (x607)<(x597);
  x609 = (x606)+(x608);
  x610 = (x609)+(x598);
  x611 = (x610)<(x598);
  x612 = (x610)+(x595);
  x613 = (x612)<(x595);
  x614 = (x611)+(x613);
  x615 = (x614)+(x596);
  x616 = (x557)+(x594);
  x617 = (x616)<(x557);
  x618 = (x617)+(x561);
  x619 = (x618)<(x561);
  x620 = (x619)+(x566);
  x621 = (x620)<(x566);
  x622 = (x621)+(x571);
  x623 = (x622)<(x571);
  x624 = (x622)+(x601);
  x625 = (x624)<(x601);
  x626 = (x623)+(x625);
  x627 = (x626)+(x576);
  x628 = (x627)<(x576);
  x629 = (x627)+(x603);
  x630 = (x629)<(x603);
  x631 = (x628)+(x630);
  x632 = (x631)+(x581);
  x633 = (x632)<(x581);
  x634 = (x632)+(x607);
  x635 = (x634)<(x607);
  x636 = (x633)+(x635);
  x637 = (x636)+(x586);
  x638 = (x637)<(x586);
  x639 = (x637)+(x612);
  x640 = (x639)<(x612);
  x641 = (x638)+(x640);
  x642 = (x641)+(x591);
  x643 = (x642)<(x591);
  x644 = (x642)+(x615);
  x645 = (x644)<(x615);
  x646 = (x643)+(x645);
  x647 = (x646)+(x593);
  x648 = (x18)*(x13);
  x649 = sizeof(intptr_t) == 4 ? ((uint64_t)(x18)*(x13))>>32 : ((__uint128_t)(x18)*(x13))>>64;
  x650 = (x18)*(x12);
  x651 = sizeof(intptr_t) == 4 ? ((uint64_t)(x18)*(x12))>>32 : ((__uint128_t)(x18)*(x12))>>64;
  x652 = (x18)*(x11);
  x653 = sizeof(intptr_t) == 4 ? ((uint64_t)(x18)*(x11))>>32 : ((__uint128_t)(x18)*(x11))>>64;
  x654 = (x18)*(x10);
  x655 = sizeof(intptr_t) == 4 ? ((uint64_t)(x18)*(x10))>>32 : ((__uint128_t)(x18)*(x10))>>64;
  x656 = (x18)*(x9);
  x657 = sizeof(intptr_t) == 4 ? ((uint64_t)(x18)*(x9))>>32 : ((__uint128_t)(x18)*(x9))>>64;
  x658 = (x18)*(x8);
  x659 = sizeof(intptr_t) == 4 ? ((uint64_t)(x18)*(x8))>>32 : ((__uint128_t)(x18)*(x8))>>64;
  x660 = (x18)*(x7);
  x661 = sizeof(intptr_t) == 4 ? ((uint64_t)(x18)*(x7))>>32 : ((__uint128_t)(x18)*(x7))>>64;
  x662 = (x661)+(x658);
  x663 = (x662)<(x661);
  x664 = (x663)+(x659);
  x665 = (x664)<(x659);
  x666 = (x664)+(x656);
  x667 = (x666)<(x656);
  x668 = (x665)+(x667);
  x669 = (x668)+(x657);
  x670 = (x669)<(x657);
  x671 = (x669)+(x654);
  x672 = (x671)<(x654);
  x673 = (x670)+(x672);
  x674 = (x673)+(x655);
  x675 = (x674)<(x655);
  x676 = (x674)+(x652);
  x677 = (x676)<(x652);
  x678 = (x675)+(x677);
  x679 = (x678)+(x653);
  x680 = (x679)<(x653);
  x681 = (x679)+(x650);
  x682 = (x681)<(x650);
  x683 = (x680)+(x682);
  x684 = (x683)+(x651);
  x685 = (x684)<(x651);
  x686 = (x684)+(x648);
  x687 = (x686)<(x648);
  x688 = (x685)+(x687);
  x689 = (x688)+(x649);
  x690 = (x618)+(x660);
  x691 = (x690)<(x618);
  x692 = (x691)+(x620);
  x693 = (x692)<(x620);
  x694 = (x692)+(x662);
  x695 = (x694)<(x662);
  x696 = (x693)+(x695);
  x697 = (x696)+(x624);
  x698 = (x697)<(x624);
  x699 = (x697)+(x666);
  x700 = (x699)<(x666);
  x701 = (x698)+(x700);
  x702 = (x701)+(x629);
  x703 = (x702)<(x629);
  x704 = (x702)+(x671);
  x705 = (x704)<(x671);
  x706 = (x703)+(x705);
  x707 = (x706)+(x634);
  x708 = (x707)<(x634);
  x709 = (x707)+(x676);
  x710 = (x709)<(x676);
  x711 = (x708)+(x710);
  x712 = (x711)+(x639);
  x713 = (x712)<(x639);
  x714 = (x712)+(x681);
  x715 = (x714)<(x681);
  x716 = (x713)+(x715);
  x717 = (x716)+(x644);
  x718 = (x717)<(x644);
  x719 = (x717)+(x686);
  x720 = (x719)<(x686);
  x721 = (x718)+(x720);
  x722 = (x721)+(x647);
  x723 = (x722)<(x647);
  x724 = (x722)+(x689);
  x725 = (x724)<(x689);
  x726 = (x723)+(x725);
  x727 = (x690)*((uintptr_t)4294967295ULL);
  x728 = (x727)*((uintptr_t)4294967295ULL);
  x729 = sizeof(intptr_t) == 4 ? ((uint64_t)(x727)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x727)*((uintptr_t)4294967295ULL))>>64;
  x730 = (x727)*((uintptr_t)4294967295ULL);
  x731 = sizeof(intptr_t) == 4 ? ((uint64_t)(x727)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x727)*((uintptr_t)4294967295ULL))>>64;
  x732 = (x727)*((uintptr_t)4294967295ULL);
  x733 = sizeof(intptr_t) == 4 ? ((uint64_t)(x727)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x727)*((uintptr_t)4294967295ULL))>>64;
  x734 = (x727)*((uintptr_t)4294967295ULL);
  x735 = sizeof(intptr_t) == 4 ? ((uint64_t)(x727)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x727)*((uintptr_t)4294967295ULL))>>64;
  x736 = (x735)+(x732);
  x737 = (x736)<(x735);
  x738 = (x737)+(x733);
  x739 = (x738)<(x733);
  x740 = (x738)+(x730);
  x741 = (x740)<(x730);
  x742 = (x739)+(x741);
  x743 = (x742)+(x731);
  x744 = (x743)<(x731);
  x745 = (x743)+(x728);
  x746 = (x745)<(x728);
  x747 = (x744)+(x746);
  x748 = (x747)+(x729);
  x749 = (x690)+(x727);
  x750 = (x749)<(x690);
  x751 = (x750)+(x694);
  x752 = (x751)<(x694);
  x753 = (x752)+(x699);
  x754 = (x753)<(x699);
  x755 = (x754)+(x704);
  x756 = (x755)<(x704);
  x757 = (x755)+(x734);
  x758 = (x757)<(x734);
  x759 = (x756)+(x758);
  x760 = (x759)+(x709);
  x761 = (x760)<(x709);
  x762 = (x760)+(x736);
  x763 = (x762)<(x736);
  x764 = (x761)+(x763);
  x765 = (x764)+(x714);
  x766 = (x765)<(x714);
  x767 = (x765)+(x740);
  x768 = (x767)<(x740);
  x769 = (x766)+(x768);
  x770 = (x769)+(x719);
  x771 = (x770)<(x719);
  x772 = (x770)+(x745);
  x773 = (x772)<(x745);
  x774 = (x771)+(x773);
  x775 = (x774)+(x724);
  x776 = (x775)<(x724);
  x777 = (x775)+(x748);
  x778 = (x777)<(x748);
  x779 = (x776)+(x778);
  x780 = (x779)+(x726);
  x781 = (x19)*(x13);
  x782 = sizeof(intptr_t) == 4 ? ((uint64_t)(x19)*(x13))>>32 : ((__uint128_t)(x19)*(x13))>>64;
  x783 = (x19)*(x12);
  x784 = sizeof(intptr_t) == 4 ? ((uint64_t)(x19)*(x12))>>32 : ((__uint128_t)(x19)*(x12))>>64;
  x785 = (x19)*(x11);
  x786 = sizeof(intptr_t) == 4 ? ((uint64_t)(x19)*(x11))>>32 : ((__uint128_t)(x19)*(x11))>>64;
  x787 = (x19)*(x10);
  x788 = sizeof(intptr_t) == 4 ? ((uint64_t)(x19)*(x10))>>32 : ((__uint128_t)(x19)*(x10))>>64;
  x789 = (x19)*(x9);
  x790 = sizeof(intptr_t) == 4 ? ((uint64_t)(x19)*(x9))>>32 : ((__uint128_t)(x19)*(x9))>>64;
  x791 = (x19)*(x8);
  x792 = sizeof(intptr_t) == 4 ? ((uint64_t)(x19)*(x8))>>32 : ((__uint128_t)(x19)*(x8))>>64;
  x793 = (x19)*(x7);
  x794 = sizeof(intptr_t) == 4 ? ((uint64_t)(x19)*(x7))>>32 : ((__uint128_t)(x19)*(x7))>>64;
  x795 = (x794)+(x791);
  x796 = (x795)<(x794);
  x797 = (x796)+(x792);
  x798 = (x797)<(x792);
  x799 = (x797)+(x789);
  x800 = (x799)<(x789);
  x801 = (x798)+(x800);
  x802 = (x801)+(x790);
  x803 = (x802)<(x790);
  x804 = (x802)+(x787);
  x805 = (x804)<(x787);
  x806 = (x803)+(x805);
  x807 = (x806)+(x788);
  x808 = (x807)<(x788);
  x809 = (x807)+(x785);
  x810 = (x809)<(x785);
  x811 = (x808)+(x810);
  x812 = (x811)+(x786);
  x813 = (x812)<(x786);
  x814 = (x812)+(x783);
  x815 = (x814)<(x783);
  x816 = (x813)+(x815);
  x817 = (x816)+(x784);
  x818 = (x817)<(x784);
  x819 = (x817)+(x781);
  x820 = (x819)<(x781);
  x821 = (x818)+(x820);
  x822 = (x821)+(x782);
  x823 = (x751)+(x793);
  x824 = (x823)<(x751);
  x825 = (x824)+(x753);
  x826 = (x825)<(x753);
  x827 = (x825)+(x795);
  x828 = (x827)<(x795);
  x829 = (x826)+(x828);
  x830 = (x829)+(x757);
  x831 = (x830)<(x757);
  x832 = (x830)+(x799);
  x833 = (x832)<(x799);
  x834 = (x831)+(x833);
  x835 = (x834)+(x762);
  x836 = (x835)<(x762);
  x837 = (x835)+(x804);
  x838 = (x837)<(x804);
  x839 = (x836)+(x838);
  x840 = (x839)+(x767);
  x841 = (x840)<(x767);
  x842 = (x840)+(x809);
  x843 = (x842)<(x809);
  x844 = (x841)+(x843);
  x845 = (x844)+(x772);
  x846 = (x845)<(x772);
  x847 = (x845)+(x814);
  x848 = (x847)<(x814);
  x849 = (x846)+(x848);
  x850 = (x849)+(x777);
  x851 = (x850)<(x777);
  x852 = (x850)+(x819);
  x853 = (x852)<(x819);
  x854 = (x851)+(x853);
  x855 = (x854)+(x780);
  x856 = (x855)<(x780);
  x857 = (x855)+(x822);
  x858 = (x857)<(x822);
  x859 = (x856)+(x858);
  x860 = (x823)*((uintptr_t)4294967295ULL);
  x861 = (x860)*((uintptr_t)4294967295ULL);
  x862 = sizeof(intptr_t) == 4 ? ((uint64_t)(x860)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x860)*((uintptr_t)4294967295ULL))>>64;
  x863 = (x860)*((uintptr_t)4294967295ULL);
  x864 = sizeof(intptr_t) == 4 ? ((uint64_t)(x860)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x860)*((uintptr_t)4294967295ULL))>>64;
  x865 = (x860)*((uintptr_t)4294967295ULL);
  x866 = sizeof(intptr_t) == 4 ? ((uint64_t)(x860)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x860)*((uintptr_t)4294967295ULL))>>64;
  x867 = (x860)*((uintptr_t)4294967295ULL);
  x868 = sizeof(intptr_t) == 4 ? ((uint64_t)(x860)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x860)*((uintptr_t)4294967295ULL))>>64;
  x869 = (x868)+(x865);
  x870 = (x869)<(x868);
  x871 = (x870)+(x866);
  x872 = (x871)<(x866);
  x873 = (x871)+(x863);
  x874 = (x873)<(x863);
  x875 = (x872)+(x874);
  x876 = (x875)+(x864);
  x877 = (x876)<(x864);
  x878 = (x876)+(x861);
  x879 = (x878)<(x861);
  x880 = (x877)+(x879);
  x881 = (x880)+(x862);
  x882 = (x823)+(x860);
  x883 = (x882)<(x823);
  x884 = (x883)+(x827);
  x885 = (x884)<(x827);
  x886 = (x885)+(x832);
  x887 = (x886)<(x832);
  x888 = (x887)+(x837);
  x889 = (x888)<(x837);
  x890 = (x888)+(x867);
  x891 = (x890)<(x867);
  x892 = (x889)+(x891);
  x893 = (x892)+(x842);
  x894 = (x893)<(x842);
  x895 = (x893)+(x869);
  x896 = (x895)<(x869);
  x897 = (x894)+(x896);
  x898 = (x897)+(x847);
  x899 = (x898)<(x847);
  x900 = (x898)+(x873);
  x901 = (x900)<(x873);
  x902 = (x899)+(x901);
  x903 = (x902)+(x852);
  x904 = (x903)<(x852);
  x905 = (x903)+(x878);
  x906 = (x905)<(x878);
  x907 = (x904)+(x906);
  x908 = (x907)+(x857);
  x909 = (x908)<(x857);
  x910 = (x908)+(x881);
  x911 = (x910)<(x881);
  x912 = (x909)+(x911);
  x913 = (x912)+(x859);
  x914 = (x884)-((uintptr_t)1ULL);
  x915 = (x884)<(x914);
  x916 = (x886)-(x915);
  x917 = (x886)<(x916);
  x918 = (x890)-(x917);
  x919 = (x890)<(x918);
  x920 = (x895)-((uintptr_t)4294967295ULL);
  x921 = (x895)<(x920);
  x922 = (x920)-(x919);
  x923 = (x920)<(x922);
  x924 = (x921)+(x923);
  x925 = (x900)-((uintptr_t)4294967295ULL);
  x926 = (x900)<(x925);
  x927 = (x925)-(x924);
  x928 = (x925)<(x927);
  x929 = (x926)+(x928);
  x930 = (x905)-((uintptr_t)4294967295ULL);
  x931 = (x905)<(x930);
  x932 = (x930)-(x929);
  x933 = (x930)<(x932);
  x934 = (x931)+(x933);
  x935 = (x910)-((uintptr_t)4294967295ULL);
  x936 = (x910)<(x935);
  x937 = (x935)-(x934);
  x938 = (x935)<(x937);
  x939 = (x936)+(x938);
  x940 = (x913)-(x939);
  x941 = (x913)<(x940);
  x942 = ((uintptr_t)-1ULL)+((x941)==((uintptr_t)0ULL));
  x943 = (x942)^((uintptr_t)4294967295ULL);
  x944 = ((x884)&(x942))|((x914)&(x943));
  x945 = ((uintptr_t)-1ULL)+((x941)==((uintptr_t)0ULL));
  x946 = (x945)^((uintptr_t)4294967295ULL);
  x947 = ((x886)&(x945))|((x916)&(x946));
  x948 = ((uintptr_t)-1ULL)+((x941)==((uintptr_t)0ULL));
  x949 = (x948)^((uintptr_t)4294967295ULL);
  x950 = ((x890)&(x948))|((x918)&(x949));
  x951 = ((uintptr_t)-1ULL)+((x941)==((uintptr_t)0ULL));
  x952 = (x951)^((uintptr_t)4294967295ULL);
  x953 = ((x895)&(x951))|((x922)&(x952));
  x954 = ((uintptr_t)-1ULL)+((x941)==((uintptr_t)0ULL));
  x955 = (x954)^((uintptr_t)4294967295ULL);
  x956 = ((x900)&(x954))|((x927)&(x955));
  x957 = ((uintptr_t)-1ULL)+((x941)==((uintptr_t)0ULL));
  x958 = (x957)^((uintptr_t)4294967295ULL);
  x959 = ((x905)&(x957))|((x932)&(x958));
  x960 = ((uintptr_t)-1ULL)+((x941)==((uintptr_t)0ULL));
  x961 = (x960)^((uintptr_t)4294967295ULL);
  x962 = ((x910)&(x960))|((x937)&(x961));
  x963 = x944;
  x964 = x947;
  x965 = x950;
  x966 = x953;
  x967 = x956;
  x968 = x959;
  x969 = x962;
  /*skip*/
  _br2_store((out0)+((uintptr_t)0ULL), x963, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)4ULL), x964, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)8ULL), x965, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)12ULL), x966, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)16ULL), x967, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)20ULL), x968, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)24ULL), x969, sizeof(uintptr_t));
  /*skip*/
  return;
}

/* NOTE: The following wrapper function is not covered by Coq proofs */
static void fiat_p224_mul(uint32_t out1[7], const uint32_t arg1[7], const uint32_t arg2[7]) {
  internal_fiat_p224_mul((uintptr_t)out1, (uintptr_t)arg1, (uintptr_t)arg2);
}


/*
 * Input Bounds:
 *   in0: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
 * Output Bounds:
 *   out0: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
 */
static
void internal_fiat_p224_square(uintptr_t out0, uintptr_t in0) {
  uintptr_t x13, x24, x27, x29, x25, x30, x22, x31, x33, x34, x23, x35, x20, x36, x38, x39, x21, x40, x18, x41, x43, x44, x19, x45, x16, x46, x48, x49, x17, x50, x14, x51, x53, x54, x15, x61, x64, x66, x62, x67, x59, x68, x70, x71, x60, x72, x57, x73, x75, x76, x58, x56, x78, x26, x79, x28, x81, x32, x83, x37, x84, x63, x85, x87, x88, x42, x89, x65, x90, x92, x93, x47, x94, x69, x95, x97, x98, x52, x99, x74, x100, x102, x103, x55, x104, x77, x105, x107, x7, x119, x122, x124, x120, x125, x117, x126, x128, x129, x118, x130, x115, x131, x133, x134, x116, x135, x113, x136, x138, x139, x114, x140, x111, x141, x143, x144, x112, x145, x109, x146, x148, x149, x110, x121, x80, x152, x82, x153, x123, x154, x156, x157, x86, x158, x127, x159, x161, x162, x91, x163, x132, x164, x166, x167, x96, x168, x137, x169, x171, x172, x101, x173, x142, x174, x176, x177, x106, x178, x147, x179, x181, x182, x108, x183, x150, x184, x186, x193, x196, x198, x194, x199, x191, x200, x202, x203, x192, x204, x189, x205, x207, x208, x190, x188, x210, x151, x211, x155, x213, x160, x215, x165, x216, x195, x217, x219, x220, x170, x221, x197, x222, x224, x225, x175, x226, x201, x227, x229, x230, x180, x231, x206, x232, x234, x235, x185, x236, x209, x237, x239, x240, x187, x8, x252, x255, x257, x253, x258, x250, x259, x261, x262, x251, x263, x248, x264, x266, x267, x249, x268, x246, x269, x271, x272, x247, x273, x244, x274, x276, x277, x245, x278, x242, x279, x281, x282, x243, x254, x212, x285, x214, x286, x256, x287, x289, x290, x218, x291, x260, x292, x294, x295, x223, x296, x265, x297, x299, x300, x228, x301, x270, x302, x304, x305, x233, x306, x275, x307, x309, x310, x238, x311, x280, x312, x314, x315, x241, x316, x283, x317, x319, x326, x329, x331, x327, x332, x324, x333, x335, x336, x325, x337, x322, x338, x340, x341, x323, x321, x343, x284, x344, x288, x346, x293, x348, x298, x349, x328, x350, x352, x353, x303, x354, x330, x355, x357, x358, x308, x359, x334, x360, x362, x363, x313, x364, x339, x365, x367, x368, x318, x369, x342, x370, x372, x373, x320, x9, x385, x388, x390, x386, x391, x383, x392, x394, x395, x384, x396, x381, x397, x399, x400, x382, x401, x379, x402, x404, x405, x380, x406, x377, x407, x409, x410, x378, x411, x375, x412, x414, x415, x376, x387, x345, x418, x347, x419, x389, x420, x422, x423, x351, x424, x393, x425, x427, x428, x356, x429, x398, x430, x432, x433, x361, x434, x403, x435, x437, x438, x366, x439, x408, x440, x442, x443, x371, x444, x413, x445, x447, x448, x374, x449, x416, x450, x452, x459, x462, x464, x460, x465, x457, x466, x468, x469, x458, x470, x455, x471, x473, x474, x456, x454, x476, x417, x477, x421, x479, x426, x481, x431, x482, x461, x483, x485, x486, x436, x487, x463, x488, x490, x491, x441, x492, x467, x493, x495, x496, x446, x497, x472, x498, x500, x501, x451, x502, x475, x503, x505, x506, x453, x10, x518, x521, x523, x519, x524, x516, x525, x527, x528, x517, x529, x514, x530, x532, x533, x515, x534, x512, x535, x537, x538, x513, x539, x510, x540, x542, x543, x511, x544, x508, x545, x547, x548, x509, x520, x478, x551, x480, x552, x522, x553, x555, x556, x484, x557, x526, x558, x560, x561, x489, x562, x531, x563, x565, x566, x494, x567, x536, x568, x570, x571, x499, x572, x541, x573, x575, x576, x504, x577, x546, x578, x580, x581, x507, x582, x549, x583, x585, x592, x595, x597, x593, x598, x590, x599, x601, x602, x591, x603, x588, x604, x606, x607, x589, x587, x609, x550, x610, x554, x612, x559, x614, x564, x615, x594, x616, x618, x619, x569, x620, x596, x621, x623, x624, x574, x625, x600, x626, x628, x629, x579, x630, x605, x631, x633, x634, x584, x635, x608, x636, x638, x639, x586, x11, x651, x654, x656, x652, x657, x649, x658, x660, x661, x650, x662, x647, x663, x665, x666, x648, x667, x645, x668, x670, x671, x646, x672, x643, x673, x675, x676, x644, x677, x641, x678, x680, x681, x642, x653, x611, x684, x613, x685, x655, x686, x688, x689, x617, x690, x659, x691, x693, x694, x622, x695, x664, x696, x698, x699, x627, x700, x669, x701, x703, x704, x632, x705, x674, x706, x708, x709, x637, x710, x679, x711, x713, x714, x640, x715, x682, x716, x718, x725, x728, x730, x726, x731, x723, x732, x734, x735, x724, x736, x721, x737, x739, x740, x722, x720, x742, x683, x743, x687, x745, x692, x747, x697, x748, x727, x749, x751, x752, x702, x753, x729, x754, x756, x757, x707, x758, x733, x759, x761, x762, x712, x763, x738, x764, x766, x767, x717, x768, x741, x769, x771, x772, x719, x6, x5, x4, x3, x2, x1, x12, x0, x784, x787, x789, x785, x790, x782, x791, x793, x794, x783, x795, x780, x796, x798, x799, x781, x800, x778, x801, x803, x804, x779, x805, x776, x806, x808, x809, x777, x810, x774, x811, x813, x814, x775, x786, x744, x817, x746, x818, x788, x819, x821, x822, x750, x823, x792, x824, x826, x827, x755, x828, x797, x829, x831, x832, x760, x833, x802, x834, x836, x837, x765, x838, x807, x839, x841, x842, x770, x843, x812, x844, x846, x847, x773, x848, x815, x849, x851, x858, x861, x863, x859, x864, x856, x865, x867, x868, x857, x869, x854, x870, x872, x873, x855, x853, x875, x816, x876, x820, x878, x825, x880, x830, x881, x860, x882, x884, x885, x835, x886, x862, x887, x889, x890, x840, x891, x866, x892, x894, x895, x845, x896, x871, x897, x899, x900, x850, x901, x874, x902, x904, x905, x852, x908, x910, x912, x913, x914, x916, x917, x918, x919, x921, x922, x923, x924, x926, x927, x928, x929, x931, x932, x906, x933, x877, x935, x907, x936, x879, x938, x909, x939, x883, x941, x911, x942, x888, x944, x915, x945, x893, x947, x920, x948, x898, x950, x925, x951, x934, x903, x953, x930, x954, x937, x940, x943, x946, x949, x952, x955, x956, x957, x958, x959, x960, x961, x962;
  x0 = _br2_load((in0)+((uintptr_t)0ULL), sizeof(uintptr_t));
  x1 = _br2_load((in0)+((uintptr_t)4ULL), sizeof(uintptr_t));
  x2 = _br2_load((in0)+((uintptr_t)8ULL), sizeof(uintptr_t));
  x3 = _br2_load((in0)+((uintptr_t)12ULL), sizeof(uintptr_t));
  x4 = _br2_load((in0)+((uintptr_t)16ULL), sizeof(uintptr_t));
  x5 = _br2_load((in0)+((uintptr_t)20ULL), sizeof(uintptr_t));
  x6 = _br2_load((in0)+((uintptr_t)24ULL), sizeof(uintptr_t));
  /*skip*/
  /*skip*/
  x7 = x1;
  x8 = x2;
  x9 = x3;
  x10 = x4;
  x11 = x5;
  x12 = x6;
  x13 = x0;
  x14 = (x13)*(x6);
  x15 = sizeof(intptr_t) == 4 ? ((uint64_t)(x13)*(x6))>>32 : ((__uint128_t)(x13)*(x6))>>64;
  x16 = (x13)*(x5);
  x17 = sizeof(intptr_t) == 4 ? ((uint64_t)(x13)*(x5))>>32 : ((__uint128_t)(x13)*(x5))>>64;
  x18 = (x13)*(x4);
  x19 = sizeof(intptr_t) == 4 ? ((uint64_t)(x13)*(x4))>>32 : ((__uint128_t)(x13)*(x4))>>64;
  x20 = (x13)*(x3);
  x21 = sizeof(intptr_t) == 4 ? ((uint64_t)(x13)*(x3))>>32 : ((__uint128_t)(x13)*(x3))>>64;
  x22 = (x13)*(x2);
  x23 = sizeof(intptr_t) == 4 ? ((uint64_t)(x13)*(x2))>>32 : ((__uint128_t)(x13)*(x2))>>64;
  x24 = (x13)*(x1);
  x25 = sizeof(intptr_t) == 4 ? ((uint64_t)(x13)*(x1))>>32 : ((__uint128_t)(x13)*(x1))>>64;
  x26 = (x13)*(x0);
  x27 = sizeof(intptr_t) == 4 ? ((uint64_t)(x13)*(x0))>>32 : ((__uint128_t)(x13)*(x0))>>64;
  x28 = (x27)+(x24);
  x29 = (x28)<(x27);
  x30 = (x29)+(x25);
  x31 = (x30)<(x25);
  x32 = (x30)+(x22);
  x33 = (x32)<(x22);
  x34 = (x31)+(x33);
  x35 = (x34)+(x23);
  x36 = (x35)<(x23);
  x37 = (x35)+(x20);
  x38 = (x37)<(x20);
  x39 = (x36)+(x38);
  x40 = (x39)+(x21);
  x41 = (x40)<(x21);
  x42 = (x40)+(x18);
  x43 = (x42)<(x18);
  x44 = (x41)+(x43);
  x45 = (x44)+(x19);
  x46 = (x45)<(x19);
  x47 = (x45)+(x16);
  x48 = (x47)<(x16);
  x49 = (x46)+(x48);
  x50 = (x49)+(x17);
  x51 = (x50)<(x17);
  x52 = (x50)+(x14);
  x53 = (x52)<(x14);
  x54 = (x51)+(x53);
  x55 = (x54)+(x15);
  x56 = (x26)*((uintptr_t)4294967295ULL);
  x57 = (x56)*((uintptr_t)4294967295ULL);
  x58 = sizeof(intptr_t) == 4 ? ((uint64_t)(x56)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x56)*((uintptr_t)4294967295ULL))>>64;
  x59 = (x56)*((uintptr_t)4294967295ULL);
  x60 = sizeof(intptr_t) == 4 ? ((uint64_t)(x56)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x56)*((uintptr_t)4294967295ULL))>>64;
  x61 = (x56)*((uintptr_t)4294967295ULL);
  x62 = sizeof(intptr_t) == 4 ? ((uint64_t)(x56)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x56)*((uintptr_t)4294967295ULL))>>64;
  x63 = (x56)*((uintptr_t)4294967295ULL);
  x64 = sizeof(intptr_t) == 4 ? ((uint64_t)(x56)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x56)*((uintptr_t)4294967295ULL))>>64;
  x65 = (x64)+(x61);
  x66 = (x65)<(x64);
  x67 = (x66)+(x62);
  x68 = (x67)<(x62);
  x69 = (x67)+(x59);
  x70 = (x69)<(x59);
  x71 = (x68)+(x70);
  x72 = (x71)+(x60);
  x73 = (x72)<(x60);
  x74 = (x72)+(x57);
  x75 = (x74)<(x57);
  x76 = (x73)+(x75);
  x77 = (x76)+(x58);
  x78 = (x26)+(x56);
  x79 = (x78)<(x26);
  x80 = (x79)+(x28);
  x81 = (x80)<(x28);
  x82 = (x81)+(x32);
  x83 = (x82)<(x32);
  x84 = (x83)+(x37);
  x85 = (x84)<(x37);
  x86 = (x84)+(x63);
  x87 = (x86)<(x63);
  x88 = (x85)+(x87);
  x89 = (x88)+(x42);
  x90 = (x89)<(x42);
  x91 = (x89)+(x65);
  x92 = (x91)<(x65);
  x93 = (x90)+(x92);
  x94 = (x93)+(x47);
  x95 = (x94)<(x47);
  x96 = (x94)+(x69);
  x97 = (x96)<(x69);
  x98 = (x95)+(x97);
  x99 = (x98)+(x52);
  x100 = (x99)<(x52);
  x101 = (x99)+(x74);
  x102 = (x101)<(x74);
  x103 = (x100)+(x102);
  x104 = (x103)+(x55);
  x105 = (x104)<(x55);
  x106 = (x104)+(x77);
  x107 = (x106)<(x77);
  x108 = (x105)+(x107);
  x109 = (x7)*(x6);
  x110 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*(x6))>>32 : ((__uint128_t)(x7)*(x6))>>64;
  x111 = (x7)*(x5);
  x112 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*(x5))>>32 : ((__uint128_t)(x7)*(x5))>>64;
  x113 = (x7)*(x4);
  x114 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*(x4))>>32 : ((__uint128_t)(x7)*(x4))>>64;
  x115 = (x7)*(x3);
  x116 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*(x3))>>32 : ((__uint128_t)(x7)*(x3))>>64;
  x117 = (x7)*(x2);
  x118 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*(x2))>>32 : ((__uint128_t)(x7)*(x2))>>64;
  x119 = (x7)*(x1);
  x120 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*(x1))>>32 : ((__uint128_t)(x7)*(x1))>>64;
  x121 = (x7)*(x0);
  x122 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*(x0))>>32 : ((__uint128_t)(x7)*(x0))>>64;
  x123 = (x122)+(x119);
  x124 = (x123)<(x122);
  x125 = (x124)+(x120);
  x126 = (x125)<(x120);
  x127 = (x125)+(x117);
  x128 = (x127)<(x117);
  x129 = (x126)+(x128);
  x130 = (x129)+(x118);
  x131 = (x130)<(x118);
  x132 = (x130)+(x115);
  x133 = (x132)<(x115);
  x134 = (x131)+(x133);
  x135 = (x134)+(x116);
  x136 = (x135)<(x116);
  x137 = (x135)+(x113);
  x138 = (x137)<(x113);
  x139 = (x136)+(x138);
  x140 = (x139)+(x114);
  x141 = (x140)<(x114);
  x142 = (x140)+(x111);
  x143 = (x142)<(x111);
  x144 = (x141)+(x143);
  x145 = (x144)+(x112);
  x146 = (x145)<(x112);
  x147 = (x145)+(x109);
  x148 = (x147)<(x109);
  x149 = (x146)+(x148);
  x150 = (x149)+(x110);
  x151 = (x80)+(x121);
  x152 = (x151)<(x80);
  x153 = (x152)+(x82);
  x154 = (x153)<(x82);
  x155 = (x153)+(x123);
  x156 = (x155)<(x123);
  x157 = (x154)+(x156);
  x158 = (x157)+(x86);
  x159 = (x158)<(x86);
  x160 = (x158)+(x127);
  x161 = (x160)<(x127);
  x162 = (x159)+(x161);
  x163 = (x162)+(x91);
  x164 = (x163)<(x91);
  x165 = (x163)+(x132);
  x166 = (x165)<(x132);
  x167 = (x164)+(x166);
  x168 = (x167)+(x96);
  x169 = (x168)<(x96);
  x170 = (x168)+(x137);
  x171 = (x170)<(x137);
  x172 = (x169)+(x171);
  x173 = (x172)+(x101);
  x174 = (x173)<(x101);
  x175 = (x173)+(x142);
  x176 = (x175)<(x142);
  x177 = (x174)+(x176);
  x178 = (x177)+(x106);
  x179 = (x178)<(x106);
  x180 = (x178)+(x147);
  x181 = (x180)<(x147);
  x182 = (x179)+(x181);
  x183 = (x182)+(x108);
  x184 = (x183)<(x108);
  x185 = (x183)+(x150);
  x186 = (x185)<(x150);
  x187 = (x184)+(x186);
  x188 = (x151)*((uintptr_t)4294967295ULL);
  x189 = (x188)*((uintptr_t)4294967295ULL);
  x190 = sizeof(intptr_t) == 4 ? ((uint64_t)(x188)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x188)*((uintptr_t)4294967295ULL))>>64;
  x191 = (x188)*((uintptr_t)4294967295ULL);
  x192 = sizeof(intptr_t) == 4 ? ((uint64_t)(x188)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x188)*((uintptr_t)4294967295ULL))>>64;
  x193 = (x188)*((uintptr_t)4294967295ULL);
  x194 = sizeof(intptr_t) == 4 ? ((uint64_t)(x188)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x188)*((uintptr_t)4294967295ULL))>>64;
  x195 = (x188)*((uintptr_t)4294967295ULL);
  x196 = sizeof(intptr_t) == 4 ? ((uint64_t)(x188)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x188)*((uintptr_t)4294967295ULL))>>64;
  x197 = (x196)+(x193);
  x198 = (x197)<(x196);
  x199 = (x198)+(x194);
  x200 = (x199)<(x194);
  x201 = (x199)+(x191);
  x202 = (x201)<(x191);
  x203 = (x200)+(x202);
  x204 = (x203)+(x192);
  x205 = (x204)<(x192);
  x206 = (x204)+(x189);
  x207 = (x206)<(x189);
  x208 = (x205)+(x207);
  x209 = (x208)+(x190);
  x210 = (x151)+(x188);
  x211 = (x210)<(x151);
  x212 = (x211)+(x155);
  x213 = (x212)<(x155);
  x214 = (x213)+(x160);
  x215 = (x214)<(x160);
  x216 = (x215)+(x165);
  x217 = (x216)<(x165);
  x218 = (x216)+(x195);
  x219 = (x218)<(x195);
  x220 = (x217)+(x219);
  x221 = (x220)+(x170);
  x222 = (x221)<(x170);
  x223 = (x221)+(x197);
  x224 = (x223)<(x197);
  x225 = (x222)+(x224);
  x226 = (x225)+(x175);
  x227 = (x226)<(x175);
  x228 = (x226)+(x201);
  x229 = (x228)<(x201);
  x230 = (x227)+(x229);
  x231 = (x230)+(x180);
  x232 = (x231)<(x180);
  x233 = (x231)+(x206);
  x234 = (x233)<(x206);
  x235 = (x232)+(x234);
  x236 = (x235)+(x185);
  x237 = (x236)<(x185);
  x238 = (x236)+(x209);
  x239 = (x238)<(x209);
  x240 = (x237)+(x239);
  x241 = (x240)+(x187);
  x242 = (x8)*(x6);
  x243 = sizeof(intptr_t) == 4 ? ((uint64_t)(x8)*(x6))>>32 : ((__uint128_t)(x8)*(x6))>>64;
  x244 = (x8)*(x5);
  x245 = sizeof(intptr_t) == 4 ? ((uint64_t)(x8)*(x5))>>32 : ((__uint128_t)(x8)*(x5))>>64;
  x246 = (x8)*(x4);
  x247 = sizeof(intptr_t) == 4 ? ((uint64_t)(x8)*(x4))>>32 : ((__uint128_t)(x8)*(x4))>>64;
  x248 = (x8)*(x3);
  x249 = sizeof(intptr_t) == 4 ? ((uint64_t)(x8)*(x3))>>32 : ((__uint128_t)(x8)*(x3))>>64;
  x250 = (x8)*(x2);
  x251 = sizeof(intptr_t) == 4 ? ((uint64_t)(x8)*(x2))>>32 : ((__uint128_t)(x8)*(x2))>>64;
  x252 = (x8)*(x1);
  x253 = sizeof(intptr_t) == 4 ? ((uint64_t)(x8)*(x1))>>32 : ((__uint128_t)(x8)*(x1))>>64;
  x254 = (x8)*(x0);
  x255 = sizeof(intptr_t) == 4 ? ((uint64_t)(x8)*(x0))>>32 : ((__uint128_t)(x8)*(x0))>>64;
  x256 = (x255)+(x252);
  x257 = (x256)<(x255);
  x258 = (x257)+(x253);
  x259 = (x258)<(x253);
  x260 = (x258)+(x250);
  x261 = (x260)<(x250);
  x262 = (x259)+(x261);
  x263 = (x262)+(x251);
  x264 = (x263)<(x251);
  x265 = (x263)+(x248);
  x266 = (x265)<(x248);
  x267 = (x264)+(x266);
  x268 = (x267)+(x249);
  x269 = (x268)<(x249);
  x270 = (x268)+(x246);
  x271 = (x270)<(x246);
  x272 = (x269)+(x271);
  x273 = (x272)+(x247);
  x274 = (x273)<(x247);
  x275 = (x273)+(x244);
  x276 = (x275)<(x244);
  x277 = (x274)+(x276);
  x278 = (x277)+(x245);
  x279 = (x278)<(x245);
  x280 = (x278)+(x242);
  x281 = (x280)<(x242);
  x282 = (x279)+(x281);
  x283 = (x282)+(x243);
  x284 = (x212)+(x254);
  x285 = (x284)<(x212);
  x286 = (x285)+(x214);
  x287 = (x286)<(x214);
  x288 = (x286)+(x256);
  x289 = (x288)<(x256);
  x290 = (x287)+(x289);
  x291 = (x290)+(x218);
  x292 = (x291)<(x218);
  x293 = (x291)+(x260);
  x294 = (x293)<(x260);
  x295 = (x292)+(x294);
  x296 = (x295)+(x223);
  x297 = (x296)<(x223);
  x298 = (x296)+(x265);
  x299 = (x298)<(x265);
  x300 = (x297)+(x299);
  x301 = (x300)+(x228);
  x302 = (x301)<(x228);
  x303 = (x301)+(x270);
  x304 = (x303)<(x270);
  x305 = (x302)+(x304);
  x306 = (x305)+(x233);
  x307 = (x306)<(x233);
  x308 = (x306)+(x275);
  x309 = (x308)<(x275);
  x310 = (x307)+(x309);
  x311 = (x310)+(x238);
  x312 = (x311)<(x238);
  x313 = (x311)+(x280);
  x314 = (x313)<(x280);
  x315 = (x312)+(x314);
  x316 = (x315)+(x241);
  x317 = (x316)<(x241);
  x318 = (x316)+(x283);
  x319 = (x318)<(x283);
  x320 = (x317)+(x319);
  x321 = (x284)*((uintptr_t)4294967295ULL);
  x322 = (x321)*((uintptr_t)4294967295ULL);
  x323 = sizeof(intptr_t) == 4 ? ((uint64_t)(x321)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x321)*((uintptr_t)4294967295ULL))>>64;
  x324 = (x321)*((uintptr_t)4294967295ULL);
  x325 = sizeof(intptr_t) == 4 ? ((uint64_t)(x321)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x321)*((uintptr_t)4294967295ULL))>>64;
  x326 = (x321)*((uintptr_t)4294967295ULL);
  x327 = sizeof(intptr_t) == 4 ? ((uint64_t)(x321)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x321)*((uintptr_t)4294967295ULL))>>64;
  x328 = (x321)*((uintptr_t)4294967295ULL);
  x329 = sizeof(intptr_t) == 4 ? ((uint64_t)(x321)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x321)*((uintptr_t)4294967295ULL))>>64;
  x330 = (x329)+(x326);
  x331 = (x330)<(x329);
  x332 = (x331)+(x327);
  x333 = (x332)<(x327);
  x334 = (x332)+(x324);
  x335 = (x334)<(x324);
  x336 = (x333)+(x335);
  x337 = (x336)+(x325);
  x338 = (x337)<(x325);
  x339 = (x337)+(x322);
  x340 = (x339)<(x322);
  x341 = (x338)+(x340);
  x342 = (x341)+(x323);
  x343 = (x284)+(x321);
  x344 = (x343)<(x284);
  x345 = (x344)+(x288);
  x346 = (x345)<(x288);
  x347 = (x346)+(x293);
  x348 = (x347)<(x293);
  x349 = (x348)+(x298);
  x350 = (x349)<(x298);
  x351 = (x349)+(x328);
  x352 = (x351)<(x328);
  x353 = (x350)+(x352);
  x354 = (x353)+(x303);
  x355 = (x354)<(x303);
  x356 = (x354)+(x330);
  x357 = (x356)<(x330);
  x358 = (x355)+(x357);
  x359 = (x358)+(x308);
  x360 = (x359)<(x308);
  x361 = (x359)+(x334);
  x362 = (x361)<(x334);
  x363 = (x360)+(x362);
  x364 = (x363)+(x313);
  x365 = (x364)<(x313);
  x366 = (x364)+(x339);
  x367 = (x366)<(x339);
  x368 = (x365)+(x367);
  x369 = (x368)+(x318);
  x370 = (x369)<(x318);
  x371 = (x369)+(x342);
  x372 = (x371)<(x342);
  x373 = (x370)+(x372);
  x374 = (x373)+(x320);
  x375 = (x9)*(x6);
  x376 = sizeof(intptr_t) == 4 ? ((uint64_t)(x9)*(x6))>>32 : ((__uint128_t)(x9)*(x6))>>64;
  x377 = (x9)*(x5);
  x378 = sizeof(intptr_t) == 4 ? ((uint64_t)(x9)*(x5))>>32 : ((__uint128_t)(x9)*(x5))>>64;
  x379 = (x9)*(x4);
  x380 = sizeof(intptr_t) == 4 ? ((uint64_t)(x9)*(x4))>>32 : ((__uint128_t)(x9)*(x4))>>64;
  x381 = (x9)*(x3);
  x382 = sizeof(intptr_t) == 4 ? ((uint64_t)(x9)*(x3))>>32 : ((__uint128_t)(x9)*(x3))>>64;
  x383 = (x9)*(x2);
  x384 = sizeof(intptr_t) == 4 ? ((uint64_t)(x9)*(x2))>>32 : ((__uint128_t)(x9)*(x2))>>64;
  x385 = (x9)*(x1);
  x386 = sizeof(intptr_t) == 4 ? ((uint64_t)(x9)*(x1))>>32 : ((__uint128_t)(x9)*(x1))>>64;
  x387 = (x9)*(x0);
  x388 = sizeof(intptr_t) == 4 ? ((uint64_t)(x9)*(x0))>>32 : ((__uint128_t)(x9)*(x0))>>64;
  x389 = (x388)+(x385);
  x390 = (x389)<(x388);
  x391 = (x390)+(x386);
  x392 = (x391)<(x386);
  x393 = (x391)+(x383);
  x394 = (x393)<(x383);
  x395 = (x392)+(x394);
  x396 = (x395)+(x384);
  x397 = (x396)<(x384);
  x398 = (x396)+(x381);
  x399 = (x398)<(x381);
  x400 = (x397)+(x399);
  x401 = (x400)+(x382);
  x402 = (x401)<(x382);
  x403 = (x401)+(x379);
  x404 = (x403)<(x379);
  x405 = (x402)+(x404);
  x406 = (x405)+(x380);
  x407 = (x406)<(x380);
  x408 = (x406)+(x377);
  x409 = (x408)<(x377);
  x410 = (x407)+(x409);
  x411 = (x410)+(x378);
  x412 = (x411)<(x378);
  x413 = (x411)+(x375);
  x414 = (x413)<(x375);
  x415 = (x412)+(x414);
  x416 = (x415)+(x376);
  x417 = (x345)+(x387);
  x418 = (x417)<(x345);
  x419 = (x418)+(x347);
  x420 = (x419)<(x347);
  x421 = (x419)+(x389);
  x422 = (x421)<(x389);
  x423 = (x420)+(x422);
  x424 = (x423)+(x351);
  x425 = (x424)<(x351);
  x426 = (x424)+(x393);
  x427 = (x426)<(x393);
  x428 = (x425)+(x427);
  x429 = (x428)+(x356);
  x430 = (x429)<(x356);
  x431 = (x429)+(x398);
  x432 = (x431)<(x398);
  x433 = (x430)+(x432);
  x434 = (x433)+(x361);
  x435 = (x434)<(x361);
  x436 = (x434)+(x403);
  x437 = (x436)<(x403);
  x438 = (x435)+(x437);
  x439 = (x438)+(x366);
  x440 = (x439)<(x366);
  x441 = (x439)+(x408);
  x442 = (x441)<(x408);
  x443 = (x440)+(x442);
  x444 = (x443)+(x371);
  x445 = (x444)<(x371);
  x446 = (x444)+(x413);
  x447 = (x446)<(x413);
  x448 = (x445)+(x447);
  x449 = (x448)+(x374);
  x450 = (x449)<(x374);
  x451 = (x449)+(x416);
  x452 = (x451)<(x416);
  x453 = (x450)+(x452);
  x454 = (x417)*((uintptr_t)4294967295ULL);
  x455 = (x454)*((uintptr_t)4294967295ULL);
  x456 = sizeof(intptr_t) == 4 ? ((uint64_t)(x454)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x454)*((uintptr_t)4294967295ULL))>>64;
  x457 = (x454)*((uintptr_t)4294967295ULL);
  x458 = sizeof(intptr_t) == 4 ? ((uint64_t)(x454)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x454)*((uintptr_t)4294967295ULL))>>64;
  x459 = (x454)*((uintptr_t)4294967295ULL);
  x460 = sizeof(intptr_t) == 4 ? ((uint64_t)(x454)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x454)*((uintptr_t)4294967295ULL))>>64;
  x461 = (x454)*((uintptr_t)4294967295ULL);
  x462 = sizeof(intptr_t) == 4 ? ((uint64_t)(x454)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x454)*((uintptr_t)4294967295ULL))>>64;
  x463 = (x462)+(x459);
  x464 = (x463)<(x462);
  x465 = (x464)+(x460);
  x466 = (x465)<(x460);
  x467 = (x465)+(x457);
  x468 = (x467)<(x457);
  x469 = (x466)+(x468);
  x470 = (x469)+(x458);
  x471 = (x470)<(x458);
  x472 = (x470)+(x455);
  x473 = (x472)<(x455);
  x474 = (x471)+(x473);
  x475 = (x474)+(x456);
  x476 = (x417)+(x454);
  x477 = (x476)<(x417);
  x478 = (x477)+(x421);
  x479 = (x478)<(x421);
  x480 = (x479)+(x426);
  x481 = (x480)<(x426);
  x482 = (x481)+(x431);
  x483 = (x482)<(x431);
  x484 = (x482)+(x461);
  x485 = (x484)<(x461);
  x486 = (x483)+(x485);
  x487 = (x486)+(x436);
  x488 = (x487)<(x436);
  x489 = (x487)+(x463);
  x490 = (x489)<(x463);
  x491 = (x488)+(x490);
  x492 = (x491)+(x441);
  x493 = (x492)<(x441);
  x494 = (x492)+(x467);
  x495 = (x494)<(x467);
  x496 = (x493)+(x495);
  x497 = (x496)+(x446);
  x498 = (x497)<(x446);
  x499 = (x497)+(x472);
  x500 = (x499)<(x472);
  x501 = (x498)+(x500);
  x502 = (x501)+(x451);
  x503 = (x502)<(x451);
  x504 = (x502)+(x475);
  x505 = (x504)<(x475);
  x506 = (x503)+(x505);
  x507 = (x506)+(x453);
  x508 = (x10)*(x6);
  x509 = sizeof(intptr_t) == 4 ? ((uint64_t)(x10)*(x6))>>32 : ((__uint128_t)(x10)*(x6))>>64;
  x510 = (x10)*(x5);
  x511 = sizeof(intptr_t) == 4 ? ((uint64_t)(x10)*(x5))>>32 : ((__uint128_t)(x10)*(x5))>>64;
  x512 = (x10)*(x4);
  x513 = sizeof(intptr_t) == 4 ? ((uint64_t)(x10)*(x4))>>32 : ((__uint128_t)(x10)*(x4))>>64;
  x514 = (x10)*(x3);
  x515 = sizeof(intptr_t) == 4 ? ((uint64_t)(x10)*(x3))>>32 : ((__uint128_t)(x10)*(x3))>>64;
  x516 = (x10)*(x2);
  x517 = sizeof(intptr_t) == 4 ? ((uint64_t)(x10)*(x2))>>32 : ((__uint128_t)(x10)*(x2))>>64;
  x518 = (x10)*(x1);
  x519 = sizeof(intptr_t) == 4 ? ((uint64_t)(x10)*(x1))>>32 : ((__uint128_t)(x10)*(x1))>>64;
  x520 = (x10)*(x0);
  x521 = sizeof(intptr_t) == 4 ? ((uint64_t)(x10)*(x0))>>32 : ((__uint128_t)(x10)*(x0))>>64;
  x522 = (x521)+(x518);
  x523 = (x522)<(x521);
  x524 = (x523)+(x519);
  x525 = (x524)<(x519);
  x526 = (x524)+(x516);
  x527 = (x526)<(x516);
  x528 = (x525)+(x527);
  x529 = (x528)+(x517);
  x530 = (x529)<(x517);
  x531 = (x529)+(x514);
  x532 = (x531)<(x514);
  x533 = (x530)+(x532);
  x534 = (x533)+(x515);
  x535 = (x534)<(x515);
  x536 = (x534)+(x512);
  x537 = (x536)<(x512);
  x538 = (x535)+(x537);
  x539 = (x538)+(x513);
  x540 = (x539)<(x513);
  x541 = (x539)+(x510);
  x542 = (x541)<(x510);
  x543 = (x540)+(x542);
  x544 = (x543)+(x511);
  x545 = (x544)<(x511);
  x546 = (x544)+(x508);
  x547 = (x546)<(x508);
  x548 = (x545)+(x547);
  x549 = (x548)+(x509);
  x550 = (x478)+(x520);
  x551 = (x550)<(x478);
  x552 = (x551)+(x480);
  x553 = (x552)<(x480);
  x554 = (x552)+(x522);
  x555 = (x554)<(x522);
  x556 = (x553)+(x555);
  x557 = (x556)+(x484);
  x558 = (x557)<(x484);
  x559 = (x557)+(x526);
  x560 = (x559)<(x526);
  x561 = (x558)+(x560);
  x562 = (x561)+(x489);
  x563 = (x562)<(x489);
  x564 = (x562)+(x531);
  x565 = (x564)<(x531);
  x566 = (x563)+(x565);
  x567 = (x566)+(x494);
  x568 = (x567)<(x494);
  x569 = (x567)+(x536);
  x570 = (x569)<(x536);
  x571 = (x568)+(x570);
  x572 = (x571)+(x499);
  x573 = (x572)<(x499);
  x574 = (x572)+(x541);
  x575 = (x574)<(x541);
  x576 = (x573)+(x575);
  x577 = (x576)+(x504);
  x578 = (x577)<(x504);
  x579 = (x577)+(x546);
  x580 = (x579)<(x546);
  x581 = (x578)+(x580);
  x582 = (x581)+(x507);
  x583 = (x582)<(x507);
  x584 = (x582)+(x549);
  x585 = (x584)<(x549);
  x586 = (x583)+(x585);
  x587 = (x550)*((uintptr_t)4294967295ULL);
  x588 = (x587)*((uintptr_t)4294967295ULL);
  x589 = sizeof(intptr_t) == 4 ? ((uint64_t)(x587)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x587)*((uintptr_t)4294967295ULL))>>64;
  x590 = (x587)*((uintptr_t)4294967295ULL);
  x591 = sizeof(intptr_t) == 4 ? ((uint64_t)(x587)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x587)*((uintptr_t)4294967295ULL))>>64;
  x592 = (x587)*((uintptr_t)4294967295ULL);
  x593 = sizeof(intptr_t) == 4 ? ((uint64_t)(x587)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x587)*((uintptr_t)4294967295ULL))>>64;
  x594 = (x587)*((uintptr_t)4294967295ULL);
  x595 = sizeof(intptr_t) == 4 ? ((uint64_t)(x587)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x587)*((uintptr_t)4294967295ULL))>>64;
  x596 = (x595)+(x592);
  x597 = (x596)<(x595);
  x598 = (x597)+(x593);
  x599 = (x598)<(x593);
  x600 = (x598)+(x590);
  x601 = (x600)<(x590);
  x602 = (x599)+(x601);
  x603 = (x602)+(x591);
  x604 = (x603)<(x591);
  x605 = (x603)+(x588);
  x606 = (x605)<(x588);
  x607 = (x604)+(x606);
  x608 = (x607)+(x589);
  x609 = (x550)+(x587);
  x610 = (x609)<(x550);
  x611 = (x610)+(x554);
  x612 = (x611)<(x554);
  x613 = (x612)+(x559);
  x614 = (x613)<(x559);
  x615 = (x614)+(x564);
  x616 = (x615)<(x564);
  x617 = (x615)+(x594);
  x618 = (x617)<(x594);
  x619 = (x616)+(x618);
  x620 = (x619)+(x569);
  x621 = (x620)<(x569);
  x622 = (x620)+(x596);
  x623 = (x622)<(x596);
  x624 = (x621)+(x623);
  x625 = (x624)+(x574);
  x626 = (x625)<(x574);
  x627 = (x625)+(x600);
  x628 = (x627)<(x600);
  x629 = (x626)+(x628);
  x630 = (x629)+(x579);
  x631 = (x630)<(x579);
  x632 = (x630)+(x605);
  x633 = (x632)<(x605);
  x634 = (x631)+(x633);
  x635 = (x634)+(x584);
  x636 = (x635)<(x584);
  x637 = (x635)+(x608);
  x638 = (x637)<(x608);
  x639 = (x636)+(x638);
  x640 = (x639)+(x586);
  x641 = (x11)*(x6);
  x642 = sizeof(intptr_t) == 4 ? ((uint64_t)(x11)*(x6))>>32 : ((__uint128_t)(x11)*(x6))>>64;
  x643 = (x11)*(x5);
  x644 = sizeof(intptr_t) == 4 ? ((uint64_t)(x11)*(x5))>>32 : ((__uint128_t)(x11)*(x5))>>64;
  x645 = (x11)*(x4);
  x646 = sizeof(intptr_t) == 4 ? ((uint64_t)(x11)*(x4))>>32 : ((__uint128_t)(x11)*(x4))>>64;
  x647 = (x11)*(x3);
  x648 = sizeof(intptr_t) == 4 ? ((uint64_t)(x11)*(x3))>>32 : ((__uint128_t)(x11)*(x3))>>64;
  x649 = (x11)*(x2);
  x650 = sizeof(intptr_t) == 4 ? ((uint64_t)(x11)*(x2))>>32 : ((__uint128_t)(x11)*(x2))>>64;
  x651 = (x11)*(x1);
  x652 = sizeof(intptr_t) == 4 ? ((uint64_t)(x11)*(x1))>>32 : ((__uint128_t)(x11)*(x1))>>64;
  x653 = (x11)*(x0);
  x654 = sizeof(intptr_t) == 4 ? ((uint64_t)(x11)*(x0))>>32 : ((__uint128_t)(x11)*(x0))>>64;
  x655 = (x654)+(x651);
  x656 = (x655)<(x654);
  x657 = (x656)+(x652);
  x658 = (x657)<(x652);
  x659 = (x657)+(x649);
  x660 = (x659)<(x649);
  x661 = (x658)+(x660);
  x662 = (x661)+(x650);
  x663 = (x662)<(x650);
  x664 = (x662)+(x647);
  x665 = (x664)<(x647);
  x666 = (x663)+(x665);
  x667 = (x666)+(x648);
  x668 = (x667)<(x648);
  x669 = (x667)+(x645);
  x670 = (x669)<(x645);
  x671 = (x668)+(x670);
  x672 = (x671)+(x646);
  x673 = (x672)<(x646);
  x674 = (x672)+(x643);
  x675 = (x674)<(x643);
  x676 = (x673)+(x675);
  x677 = (x676)+(x644);
  x678 = (x677)<(x644);
  x679 = (x677)+(x641);
  x680 = (x679)<(x641);
  x681 = (x678)+(x680);
  x682 = (x681)+(x642);
  x683 = (x611)+(x653);
  x684 = (x683)<(x611);
  x685 = (x684)+(x613);
  x686 = (x685)<(x613);
  x687 = (x685)+(x655);
  x688 = (x687)<(x655);
  x689 = (x686)+(x688);
  x690 = (x689)+(x617);
  x691 = (x690)<(x617);
  x692 = (x690)+(x659);
  x693 = (x692)<(x659);
  x694 = (x691)+(x693);
  x695 = (x694)+(x622);
  x696 = (x695)<(x622);
  x697 = (x695)+(x664);
  x698 = (x697)<(x664);
  x699 = (x696)+(x698);
  x700 = (x699)+(x627);
  x701 = (x700)<(x627);
  x702 = (x700)+(x669);
  x703 = (x702)<(x669);
  x704 = (x701)+(x703);
  x705 = (x704)+(x632);
  x706 = (x705)<(x632);
  x707 = (x705)+(x674);
  x708 = (x707)<(x674);
  x709 = (x706)+(x708);
  x710 = (x709)+(x637);
  x711 = (x710)<(x637);
  x712 = (x710)+(x679);
  x713 = (x712)<(x679);
  x714 = (x711)+(x713);
  x715 = (x714)+(x640);
  x716 = (x715)<(x640);
  x717 = (x715)+(x682);
  x718 = (x717)<(x682);
  x719 = (x716)+(x718);
  x720 = (x683)*((uintptr_t)4294967295ULL);
  x721 = (x720)*((uintptr_t)4294967295ULL);
  x722 = sizeof(intptr_t) == 4 ? ((uint64_t)(x720)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x720)*((uintptr_t)4294967295ULL))>>64;
  x723 = (x720)*((uintptr_t)4294967295ULL);
  x724 = sizeof(intptr_t) == 4 ? ((uint64_t)(x720)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x720)*((uintptr_t)4294967295ULL))>>64;
  x725 = (x720)*((uintptr_t)4294967295ULL);
  x726 = sizeof(intptr_t) == 4 ? ((uint64_t)(x720)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x720)*((uintptr_t)4294967295ULL))>>64;
  x727 = (x720)*((uintptr_t)4294967295ULL);
  x728 = sizeof(intptr_t) == 4 ? ((uint64_t)(x720)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x720)*((uintptr_t)4294967295ULL))>>64;
  x729 = (x728)+(x725);
  x730 = (x729)<(x728);
  x731 = (x730)+(x726);
  x732 = (x731)<(x726);
  x733 = (x731)+(x723);
  x734 = (x733)<(x723);
  x735 = (x732)+(x734);
  x736 = (x735)+(x724);
  x737 = (x736)<(x724);
  x738 = (x736)+(x721);
  x739 = (x738)<(x721);
  x740 = (x737)+(x739);
  x741 = (x740)+(x722);
  x742 = (x683)+(x720);
  x743 = (x742)<(x683);
  x744 = (x743)+(x687);
  x745 = (x744)<(x687);
  x746 = (x745)+(x692);
  x747 = (x746)<(x692);
  x748 = (x747)+(x697);
  x749 = (x748)<(x697);
  x750 = (x748)+(x727);
  x751 = (x750)<(x727);
  x752 = (x749)+(x751);
  x753 = (x752)+(x702);
  x754 = (x753)<(x702);
  x755 = (x753)+(x729);
  x756 = (x755)<(x729);
  x757 = (x754)+(x756);
  x758 = (x757)+(x707);
  x759 = (x758)<(x707);
  x760 = (x758)+(x733);
  x761 = (x760)<(x733);
  x762 = (x759)+(x761);
  x763 = (x762)+(x712);
  x764 = (x763)<(x712);
  x765 = (x763)+(x738);
  x766 = (x765)<(x738);
  x767 = (x764)+(x766);
  x768 = (x767)+(x717);
  x769 = (x768)<(x717);
  x770 = (x768)+(x741);
  x771 = (x770)<(x741);
  x772 = (x769)+(x771);
  x773 = (x772)+(x719);
  x774 = (x12)*(x6);
  x775 = sizeof(intptr_t) == 4 ? ((uint64_t)(x12)*(x6))>>32 : ((__uint128_t)(x12)*(x6))>>64;
  x776 = (x12)*(x5);
  x777 = sizeof(intptr_t) == 4 ? ((uint64_t)(x12)*(x5))>>32 : ((__uint128_t)(x12)*(x5))>>64;
  x778 = (x12)*(x4);
  x779 = sizeof(intptr_t) == 4 ? ((uint64_t)(x12)*(x4))>>32 : ((__uint128_t)(x12)*(x4))>>64;
  x780 = (x12)*(x3);
  x781 = sizeof(intptr_t) == 4 ? ((uint64_t)(x12)*(x3))>>32 : ((__uint128_t)(x12)*(x3))>>64;
  x782 = (x12)*(x2);
  x783 = sizeof(intptr_t) == 4 ? ((uint64_t)(x12)*(x2))>>32 : ((__uint128_t)(x12)*(x2))>>64;
  x784 = (x12)*(x1);
  x785 = sizeof(intptr_t) == 4 ? ((uint64_t)(x12)*(x1))>>32 : ((__uint128_t)(x12)*(x1))>>64;
  x786 = (x12)*(x0);
  x787 = sizeof(intptr_t) == 4 ? ((uint64_t)(x12)*(x0))>>32 : ((__uint128_t)(x12)*(x0))>>64;
  x788 = (x787)+(x784);
  x789 = (x788)<(x787);
  x790 = (x789)+(x785);
  x791 = (x790)<(x785);
  x792 = (x790)+(x782);
  x793 = (x792)<(x782);
  x794 = (x791)+(x793);
  x795 = (x794)+(x783);
  x796 = (x795)<(x783);
  x797 = (x795)+(x780);
  x798 = (x797)<(x780);
  x799 = (x796)+(x798);
  x800 = (x799)+(x781);
  x801 = (x800)<(x781);
  x802 = (x800)+(x778);
  x803 = (x802)<(x778);
  x804 = (x801)+(x803);
  x805 = (x804)+(x779);
  x806 = (x805)<(x779);
  x807 = (x805)+(x776);
  x808 = (x807)<(x776);
  x809 = (x806)+(x808);
  x810 = (x809)+(x777);
  x811 = (x810)<(x777);
  x812 = (x810)+(x774);
  x813 = (x812)<(x774);
  x814 = (x811)+(x813);
  x815 = (x814)+(x775);
  x816 = (x744)+(x786);
  x817 = (x816)<(x744);
  x818 = (x817)+(x746);
  x819 = (x818)<(x746);
  x820 = (x818)+(x788);
  x821 = (x820)<(x788);
  x822 = (x819)+(x821);
  x823 = (x822)+(x750);
  x824 = (x823)<(x750);
  x825 = (x823)+(x792);
  x826 = (x825)<(x792);
  x827 = (x824)+(x826);
  x828 = (x827)+(x755);
  x829 = (x828)<(x755);
  x830 = (x828)+(x797);
  x831 = (x830)<(x797);
  x832 = (x829)+(x831);
  x833 = (x832)+(x760);
  x834 = (x833)<(x760);
  x835 = (x833)+(x802);
  x836 = (x835)<(x802);
  x837 = (x834)+(x836);
  x838 = (x837)+(x765);
  x839 = (x838)<(x765);
  x840 = (x838)+(x807);
  x841 = (x840)<(x807);
  x842 = (x839)+(x841);
  x843 = (x842)+(x770);
  x844 = (x843)<(x770);
  x845 = (x843)+(x812);
  x846 = (x845)<(x812);
  x847 = (x844)+(x846);
  x848 = (x847)+(x773);
  x849 = (x848)<(x773);
  x850 = (x848)+(x815);
  x851 = (x850)<(x815);
  x852 = (x849)+(x851);
  x853 = (x816)*((uintptr_t)4294967295ULL);
  x854 = (x853)*((uintptr_t)4294967295ULL);
  x855 = sizeof(intptr_t) == 4 ? ((uint64_t)(x853)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x853)*((uintptr_t)4294967295ULL))>>64;
  x856 = (x853)*((uintptr_t)4294967295ULL);
  x857 = sizeof(intptr_t) == 4 ? ((uint64_t)(x853)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x853)*((uintptr_t)4294967295ULL))>>64;
  x858 = (x853)*((uintptr_t)4294967295ULL);
  x859 = sizeof(intptr_t) == 4 ? ((uint64_t)(x853)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x853)*((uintptr_t)4294967295ULL))>>64;
  x860 = (x853)*((uintptr_t)4294967295ULL);
  x861 = sizeof(intptr_t) == 4 ? ((uint64_t)(x853)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x853)*((uintptr_t)4294967295ULL))>>64;
  x862 = (x861)+(x858);
  x863 = (x862)<(x861);
  x864 = (x863)+(x859);
  x865 = (x864)<(x859);
  x866 = (x864)+(x856);
  x867 = (x866)<(x856);
  x868 = (x865)+(x867);
  x869 = (x868)+(x857);
  x870 = (x869)<(x857);
  x871 = (x869)+(x854);
  x872 = (x871)<(x854);
  x873 = (x870)+(x872);
  x874 = (x873)+(x855);
  x875 = (x816)+(x853);
  x876 = (x875)<(x816);
  x877 = (x876)+(x820);
  x878 = (x877)<(x820);
  x879 = (x878)+(x825);
  x880 = (x879)<(x825);
  x881 = (x880)+(x830);
  x882 = (x881)<(x830);
  x883 = (x881)+(x860);
  x884 = (x883)<(x860);
  x885 = (x882)+(x884);
  x886 = (x885)+(x835);
  x887 = (x886)<(x835);
  x888 = (x886)+(x862);
  x889 = (x888)<(x862);
  x890 = (x887)+(x889);
  x891 = (x890)+(x840);
  x892 = (x891)<(x840);
  x893 = (x891)+(x866);
  x894 = (x893)<(x866);
  x895 = (x892)+(x894);
  x896 = (x895)+(x845);
  x897 = (x896)<(x845);
  x898 = (x896)+(x871);
  x899 = (x898)<(x871);
  x900 = (x897)+(x899);
  x901 = (x900)+(x850);
  x902 = (x901)<(x850);
  x903 = (x901)+(x874);
  x904 = (x903)<(x874);
  x905 = (x902)+(x904);
  x906 = (x905)+(x852);
  x907 = (x877)-((uintptr_t)1ULL);
  x908 = (x877)<(x907);
  x909 = (x879)-(x908);
  x910 = (x879)<(x909);
  x911 = (x883)-(x910);
  x912 = (x883)<(x911);
  x913 = (x888)-((uintptr_t)4294967295ULL);
  x914 = (x888)<(x913);
  x915 = (x913)-(x912);
  x916 = (x913)<(x915);
  x917 = (x914)+(x916);
  x918 = (x893)-((uintptr_t)4294967295ULL);
  x919 = (x893)<(x918);
  x920 = (x918)-(x917);
  x921 = (x918)<(x920);
  x922 = (x919)+(x921);
  x923 = (x898)-((uintptr_t)4294967295ULL);
  x924 = (x898)<(x923);
  x925 = (x923)-(x922);
  x926 = (x923)<(x925);
  x927 = (x924)+(x926);
  x928 = (x903)-((uintptr_t)4294967295ULL);
  x929 = (x903)<(x928);
  x930 = (x928)-(x927);
  x931 = (x928)<(x930);
  x932 = (x929)+(x931);
  x933 = (x906)-(x932);
  x934 = (x906)<(x933);
  x935 = ((uintptr_t)-1ULL)+((x934)==((uintptr_t)0ULL));
  x936 = (x935)^((uintptr_t)4294967295ULL);
  x937 = ((x877)&(x935))|((x907)&(x936));
  x938 = ((uintptr_t)-1ULL)+((x934)==((uintptr_t)0ULL));
  x939 = (x938)^((uintptr_t)4294967295ULL);
  x940 = ((x879)&(x938))|((x909)&(x939));
  x941 = ((uintptr_t)-1ULL)+((x934)==((uintptr_t)0ULL));
  x942 = (x941)^((uintptr_t)4294967295ULL);
  x943 = ((x883)&(x941))|((x911)&(x942));
  x944 = ((uintptr_t)-1ULL)+((x934)==((uintptr_t)0ULL));
  x945 = (x944)^((uintptr_t)4294967295ULL);
  x946 = ((x888)&(x944))|((x915)&(x945));
  x947 = ((uintptr_t)-1ULL)+((x934)==((uintptr_t)0ULL));
  x948 = (x947)^((uintptr_t)4294967295ULL);
  x949 = ((x893)&(x947))|((x920)&(x948));
  x950 = ((uintptr_t)-1ULL)+((x934)==((uintptr_t)0ULL));
  x951 = (x950)^((uintptr_t)4294967295ULL);
  x952 = ((x898)&(x950))|((x925)&(x951));
  x953 = ((uintptr_t)-1ULL)+((x934)==((uintptr_t)0ULL));
  x954 = (x953)^((uintptr_t)4294967295ULL);
  x955 = ((x903)&(x953))|((x930)&(x954));
  x956 = x937;
  x957 = x940;
  x958 = x943;
  x959 = x946;
  x960 = x949;
  x961 = x952;
  x962 = x955;
  /*skip*/
  _br2_store((out0)+((uintptr_t)0ULL), x956, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)4ULL), x957, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)8ULL), x958, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)12ULL), x959, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)16ULL), x960, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)20ULL), x961, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)24ULL), x962, sizeof(uintptr_t));
  /*skip*/
  return;
}

/* NOTE: The following wrapper function is not covered by Coq proofs */
static void fiat_p224_square(uint32_t out1[7], const uint32_t arg1[7]) {
  internal_fiat_p224_square((uintptr_t)out1, (uintptr_t)arg1);
}


/*
 * Input Bounds:
 *   in0: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
 *   in1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
 * Output Bounds:
 *   out0: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
 */
static
void internal_fiat_p224_add(uintptr_t out0, uintptr_t in0, uintptr_t in1) {
  uintptr_t x7, x0, x15, x1, x8, x17, x2, x9, x19, x3, x10, x21, x4, x11, x23, x5, x12, x25, x6, x13, x31, x33, x35, x27, x37, x14, x40, x28, x41, x16, x43, x29, x44, x18, x46, x30, x47, x20, x49, x32, x50, x22, x52, x34, x53, x24, x55, x36, x56, x39, x26, x58, x38, x59, x42, x45, x48, x51, x54, x57, x60, x61, x62, x63, x64, x65, x66, x67;
  x0 = _br2_load((in0)+((uintptr_t)0ULL), sizeof(uintptr_t));
  x1 = _br2_load((in0)+((uintptr_t)4ULL), sizeof(uintptr_t));
  x2 = _br2_load((in0)+((uintptr_t)8ULL), sizeof(uintptr_t));
  x3 = _br2_load((in0)+((uintptr_t)12ULL), sizeof(uintptr_t));
  x4 = _br2_load((in0)+((uintptr_t)16ULL), sizeof(uintptr_t));
  x5 = _br2_load((in0)+((uintptr_t)20ULL), sizeof(uintptr_t));
  x6 = _br2_load((in0)+((uintptr_t)24ULL), sizeof(uintptr_t));
  /*skip*/
  x7 = _br2_load((in1)+((uintptr_t)0ULL), sizeof(uintptr_t));
  x8 = _br2_load((in1)+((uintptr_t)4ULL), sizeof(uintptr_t));
  x9 = _br2_load((in1)+((uintptr_t)8ULL), sizeof(uintptr_t));
  x10 = _br2_load((in1)+((uintptr_t)12ULL), sizeof(uintptr_t));
  x11 = _br2_load((in1)+((uintptr_t)16ULL), sizeof(uintptr_t));
  x12 = _br2_load((in1)+((uintptr_t)20ULL), sizeof(uintptr_t));
  x13 = _br2_load((in1)+((uintptr_t)24ULL), sizeof(uintptr_t));
  /*skip*/
  /*skip*/
  x14 = (x0)+(x7);
  x15 = ((x14)<(x0))+(x1);
  x16 = (x15)+(x8);
  x17 = (((x15)<(x1))+((x16)<(x8)))+(x2);
  x18 = (x17)+(x9);
  x19 = (((x17)<(x2))+((x18)<(x9)))+(x3);
  x20 = (x19)+(x10);
  x21 = (((x19)<(x3))+((x20)<(x10)))+(x4);
  x22 = (x21)+(x11);
  x23 = (((x21)<(x4))+((x22)<(x11)))+(x5);
  x24 = (x23)+(x12);
  x25 = (((x23)<(x5))+((x24)<(x12)))+(x6);
  x26 = (x25)+(x13);
  x27 = ((x25)<(x6))+((x26)<(x13));
  x28 = (x14)-((uintptr_t)1ULL);
  x29 = (x16)-((x14)<(x28));
  x30 = (x18)-((x16)<(x29));
  x31 = (x20)-((uintptr_t)4294967295ULL);
  x32 = (x31)-((x18)<(x30));
  x33 = (x22)-((uintptr_t)4294967295ULL);
  x34 = (x33)-(((x20)<(x31))+((x31)<(x32)));
  x35 = (x24)-((uintptr_t)4294967295ULL);
  x36 = (x35)-(((x22)<(x33))+((x33)<(x34)));
  x37 = (x26)-((uintptr_t)4294967295ULL);
  x38 = (x37)-(((x24)<(x35))+((x35)<(x36)));
  x39 = (x27)<((x27)-(((x26)<(x37))+((x37)<(x38))));
  x40 = ((uintptr_t)-1ULL)+((x39)==((uintptr_t)0ULL));
  x41 = (x40)^((uintptr_t)4294967295ULL);
  x42 = ((x14)&(x40))|((x28)&(x41));
  x43 = ((uintptr_t)-1ULL)+((x39)==((uintptr_t)0ULL));
  x44 = (x43)^((uintptr_t)4294967295ULL);
  x45 = ((x16)&(x43))|((x29)&(x44));
  x46 = ((uintptr_t)-1ULL)+((x39)==((uintptr_t)0ULL));
  x47 = (x46)^((uintptr_t)4294967295ULL);
  x48 = ((x18)&(x46))|((x30)&(x47));
  x49 = ((uintptr_t)-1ULL)+((x39)==((uintptr_t)0ULL));
  x50 = (x49)^((uintptr_t)4294967295ULL);
  x51 = ((x20)&(x49))|((x32)&(x50));
  x52 = ((uintptr_t)-1ULL)+((x39)==((uintptr_t)0ULL));
  x53 = (x52)^((uintptr_t)4294967295ULL);
  x54 = ((x22)&(x52))|((x34)&(x53));
  x55 = ((uintptr_t)-1ULL)+((x39)==((uintptr_t)0ULL));
  x56 = (x55)^((uintptr_t)4294967295ULL);
  x57 = ((x24)&(x55))|((x36)&(x56));
  x58 = ((uintptr_t)-1ULL)+((x39)==((uintptr_t)0ULL));
  x59 = (x58)^((uintptr_t)4294967295ULL);
  x60 = ((x26)&(x58))|((x38)&(x59));
  x61 = x42;
  x62 = x45;
  x63 = x48;
  x64 = x51;
  x65 = x54;
  x66 = x57;
  x67 = x60;
  /*skip*/
  _br2_store((out0)+((uintptr_t)0ULL), x61, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)4ULL), x62, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)8ULL), x63, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)12ULL), x64, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)16ULL), x65, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)20ULL), x66, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)24ULL), x67, sizeof(uintptr_t));
  /*skip*/
  return;
}

/* NOTE: The following wrapper function is not covered by Coq proofs */
static void fiat_p224_add(uint32_t out1[7], const uint32_t arg1[7], const uint32_t arg2[7]) {
  internal_fiat_p224_add((uintptr_t)out1, (uintptr_t)arg1, (uintptr_t)arg2);
}


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

/* NOTE: The following wrapper function is not covered by Coq proofs */
static void fiat_p224_sub(uint32_t out1[7], const uint32_t arg1[7], const uint32_t arg2[7]) {
  internal_fiat_p224_sub((uintptr_t)out1, (uintptr_t)arg1, (uintptr_t)arg2);
}


/*
 * Input Bounds:
 *   in0: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
 * Output Bounds:
 *   out0: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
 */
static
void internal_fiat_p224_opp(uintptr_t out0, uintptr_t in0) {
  uintptr_t x0, x1, x2, x8, x3, x10, x4, x12, x5, x14, x6, x16, x18, x7, x9, x11, x24, x13, x26, x15, x28, x17, x19, x20, x21, x22, x23, x25, x27, 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)4ULL), sizeof(uintptr_t));
  x2 = _br2_load((in0)+((uintptr_t)8ULL), sizeof(uintptr_t));
  x3 = _br2_load((in0)+((uintptr_t)12ULL), sizeof(uintptr_t));
  x4 = _br2_load((in0)+((uintptr_t)16ULL), sizeof(uintptr_t));
  x5 = _br2_load((in0)+((uintptr_t)20ULL), sizeof(uintptr_t));
  x6 = _br2_load((in0)+((uintptr_t)24ULL), sizeof(uintptr_t));
  /*skip*/
  /*skip*/
  x7 = ((uintptr_t)0ULL)-(x0);
  x8 = ((uintptr_t)0ULL)-(x1);
  x9 = (x8)-(((uintptr_t)0ULL)<(x7));
  x10 = ((uintptr_t)0ULL)-(x2);
  x11 = (x10)-((((uintptr_t)0ULL)<(x8))+((x8)<(x9)));
  x12 = ((uintptr_t)0ULL)-(x3);
  x13 = (x12)-((((uintptr_t)0ULL)<(x10))+((x10)<(x11)));
  x14 = ((uintptr_t)0ULL)-(x4);
  x15 = (x14)-((((uintptr_t)0ULL)<(x12))+((x12)<(x13)));
  x16 = ((uintptr_t)0ULL)-(x5);
  x17 = (x16)-((((uintptr_t)0ULL)<(x14))+((x14)<(x15)));
  x18 = ((uintptr_t)0ULL)-(x6);
  x19 = (x18)-((((uintptr_t)0ULL)<(x16))+((x16)<(x17)));
  x20 = ((uintptr_t)-1ULL)+(((((uintptr_t)0ULL)<(x18))+((x18)<(x19)))==((uintptr_t)0ULL));
  x21 = (x7)+((x20)&((uintptr_t)1ULL));
  x22 = ((x21)<(x7))+(x9);
  x23 = ((x22)<(x9))+(x11);
  x24 = ((x23)<(x11))+(x13);
  x25 = (x24)+(x20);
  x26 = (((x24)<(x13))+((x25)<(x20)))+(x15);
  x27 = (x26)+(x20);
  x28 = (((x26)<(x15))+((x27)<(x20)))+(x17);
  x29 = (x28)+(x20);
  x30 = ((((x28)<(x17))+((x29)<(x20)))+(x19))+(x20);
  x31 = x21;
  x32 = x22;
  x33 = x23;
  x34 = x25;
  x35 = x27;
  x36 = x29;
  x37 = x30;
  /*skip*/
  _br2_store((out0)+((uintptr_t)0ULL), x31, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)4ULL), x32, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)8ULL), x33, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)12ULL), x34, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)16ULL), x35, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)20ULL), x36, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)24ULL), x37, sizeof(uintptr_t));
  /*skip*/
  return;
}

/* NOTE: The following wrapper function is not covered by Coq proofs */
static void fiat_p224_opp(uint32_t out1[7], const uint32_t arg1[7]) {
  internal_fiat_p224_opp((uintptr_t)out1, (uintptr_t)arg1);
}


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

/* NOTE: The following wrapper function is not covered by Coq proofs */
static void fiat_p224_from_montgomery(uint32_t out1[7], const uint32_t arg1[7]) {
  internal_fiat_p224_from_montgomery((uintptr_t)out1, (uintptr_t)arg1);
}


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

/* NOTE: The following wrapper function is not covered by Coq proofs */
static void fiat_p224_to_montgomery(uint32_t out1[7], const uint32_t arg1[7]) {
  internal_fiat_p224_to_montgomery((uintptr_t)out1, (uintptr_t)arg1);
}


/*
 * Input Bounds:
 *   in0: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
 * Output Bounds:
 *   out0: [0x0 ~> 0xffffffff]
 */
static
uintptr_t internal_fiat_p224_nonzero(uintptr_t in0) {
  uintptr_t x0, x1, x2, x3, x4, x5, x6, x7, out0, x8;
  x0 = _br2_load((in0)+((uintptr_t)0ULL), sizeof(uintptr_t));
  x1 = _br2_load((in0)+((uintptr_t)4ULL), sizeof(uintptr_t));
  x2 = _br2_load((in0)+((uintptr_t)8ULL), sizeof(uintptr_t));
  x3 = _br2_load((in0)+((uintptr_t)12ULL), sizeof(uintptr_t));
  x4 = _br2_load((in0)+((uintptr_t)16ULL), sizeof(uintptr_t));
  x5 = _br2_load((in0)+((uintptr_t)20ULL), sizeof(uintptr_t));
  x6 = _br2_load((in0)+((uintptr_t)24ULL), sizeof(uintptr_t));
  /*skip*/
  /*skip*/
  x7 = (x0)|((x1)|((x2)|((x3)|((x4)|((x5)|(x6))))));
  x8 = x7;
  out0 = x8;
  return out0;
}

/* NOTE: The following wrapper function is not covered by Coq proofs */
static void fiat_p224_nonzero(uint32_t* out1, const uint32_t arg1[7]) {
  *out1 = (uint32_t)internal_fiat_p224_nonzero((uintptr_t)arg1);
}


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

/* NOTE: The following wrapper function is not covered by Coq proofs */
static void fiat_p224_selectznz(uint32_t out1[7], uint8_t arg1, const uint32_t arg2[7], const uint32_t arg3[7]) {
  internal_fiat_p224_selectznz((uintptr_t)out1, (uintptr_t)arg1, (uintptr_t)arg2, (uintptr_t)arg3);
}


/*
 * Input Bounds:
 *   in0: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
 * 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]]
 */
static
void internal_fiat_p224_to_bytes(uintptr_t out0, uintptr_t in0) {
  uintptr_t x6, x5, x4, x3, x2, x1, x0, x13, x15, x17, x12, x21, x23, x11, x27, x29, x10, x33, x35, x9, x39, x41, x8, x45, x47, x7, x51, x53, x14, x16, x18, x19, x20, x22, x24, x25, x26, x28, x30, x31, x32, x34, x36, x37, x38, x40, x42, x43, x44, x46, x48, x49, x50, x52, x54, x55, x56, x57, x58, x59, x60, x61, x62, x63, x64, x65, x66, x67, x68, x69, x70, x71, x72, x73, x74, x75, x76, x77, x78, x79, x80, x81, x82, x83;
  x0 = _br2_load((in0)+((uintptr_t)0ULL), sizeof(uintptr_t));
  x1 = _br2_load((in0)+((uintptr_t)4ULL), sizeof(uintptr_t));
  x2 = _br2_load((in0)+((uintptr_t)8ULL), sizeof(uintptr_t));
  x3 = _br2_load((in0)+((uintptr_t)12ULL), sizeof(uintptr_t));
  x4 = _br2_load((in0)+((uintptr_t)16ULL), sizeof(uintptr_t));
  x5 = _br2_load((in0)+((uintptr_t)20ULL), sizeof(uintptr_t));
  x6 = _br2_load((in0)+((uintptr_t)24ULL), sizeof(uintptr_t));
  /*skip*/
  /*skip*/
  x7 = x6;
  x8 = x5;
  x9 = x4;
  x10 = x3;
  x11 = x2;
  x12 = x1;
  x13 = x0;
  x14 = (x13)&((uintptr_t)255ULL);
  x15 = (x13)>>((uintptr_t)8ULL);
  x16 = (x15)&((uintptr_t)255ULL);
  x17 = (x15)>>((uintptr_t)8ULL);
  x18 = (x17)&((uintptr_t)255ULL);
  x19 = (x17)>>((uintptr_t)8ULL);
  x20 = (x12)&((uintptr_t)255ULL);
  x21 = (x12)>>((uintptr_t)8ULL);
  x22 = (x21)&((uintptr_t)255ULL);
  x23 = (x21)>>((uintptr_t)8ULL);
  x24 = (x23)&((uintptr_t)255ULL);
  x25 = (x23)>>((uintptr_t)8ULL);
  x26 = (x11)&((uintptr_t)255ULL);
  x27 = (x11)>>((uintptr_t)8ULL);
  x28 = (x27)&((uintptr_t)255ULL);
  x29 = (x27)>>((uintptr_t)8ULL);
  x30 = (x29)&((uintptr_t)255ULL);
  x31 = (x29)>>((uintptr_t)8ULL);
  x32 = (x10)&((uintptr_t)255ULL);
  x33 = (x10)>>((uintptr_t)8ULL);
  x34 = (x33)&((uintptr_t)255ULL);
  x35 = (x33)>>((uintptr_t)8ULL);
  x36 = (x35)&((uintptr_t)255ULL);
  x37 = (x35)>>((uintptr_t)8ULL);
  x38 = (x9)&((uintptr_t)255ULL);
  x39 = (x9)>>((uintptr_t)8ULL);
  x40 = (x39)&((uintptr_t)255ULL);
  x41 = (x39)>>((uintptr_t)8ULL);
  x42 = (x41)&((uintptr_t)255ULL);
  x43 = (x41)>>((uintptr_t)8ULL);
  x44 = (x8)&((uintptr_t)255ULL);
  x45 = (x8)>>((uintptr_t)8ULL);
  x46 = (x45)&((uintptr_t)255ULL);
  x47 = (x45)>>((uintptr_t)8ULL);
  x48 = (x47)&((uintptr_t)255ULL);
  x49 = (x47)>>((uintptr_t)8ULL);
  x50 = (x7)&((uintptr_t)255ULL);
  x51 = (x7)>>((uintptr_t)8ULL);
  x52 = (x51)&((uintptr_t)255ULL);
  x53 = (x51)>>((uintptr_t)8ULL);
  x54 = (x53)&((uintptr_t)255ULL);
  x55 = (x53)>>((uintptr_t)8ULL);
  x56 = x14;
  x57 = x16;
  x58 = x18;
  x59 = x19;
  x60 = x20;
  x61 = x22;
  x62 = x24;
  x63 = x25;
  x64 = x26;
  x65 = x28;
  x66 = x30;
  x67 = x31;
  x68 = x32;
  x69 = x34;
  x70 = x36;
  x71 = x37;
  x72 = x38;
  x73 = x40;
  x74 = x42;
  x75 = x43;
  x76 = x44;
  x77 = x46;
  x78 = x48;
  x79 = x49;
  x80 = x50;
  x81 = x52;
  x82 = x54;
  x83 = x55;
  /*skip*/
  _br2_store((out0)+((uintptr_t)0ULL), x56, 1);
  _br2_store((out0)+((uintptr_t)1ULL), x57, 1);
  _br2_store((out0)+((uintptr_t)2ULL), x58, 1);
  _br2_store((out0)+((uintptr_t)3ULL), x59, 1);
  _br2_store((out0)+((uintptr_t)4ULL), x60, 1);
  _br2_store((out0)+((uintptr_t)5ULL), x61, 1);
  _br2_store((out0)+((uintptr_t)6ULL), x62, 1);
  _br2_store((out0)+((uintptr_t)7ULL), x63, 1);
  _br2_store((out0)+((uintptr_t)8ULL), x64, 1);
  _br2_store((out0)+((uintptr_t)9ULL), x65, 1);
  _br2_store((out0)+((uintptr_t)10ULL), x66, 1);
  _br2_store((out0)+((uintptr_t)11ULL), x67, 1);
  _br2_store((out0)+((uintptr_t)12ULL), x68, 1);
  _br2_store((out0)+((uintptr_t)13ULL), x69, 1);
  _br2_store((out0)+((uintptr_t)14ULL), x70, 1);
  _br2_store((out0)+((uintptr_t)15ULL), x71, 1);
  _br2_store((out0)+((uintptr_t)16ULL), x72, 1);
  _br2_store((out0)+((uintptr_t)17ULL), x73, 1);
  _br2_store((out0)+((uintptr_t)18ULL), x74, 1);
  _br2_store((out0)+((uintptr_t)19ULL), x75, 1);
  _br2_store((out0)+((uintptr_t)20ULL), x76, 1);
  _br2_store((out0)+((uintptr_t)21ULL), x77, 1);
  _br2_store((out0)+((uintptr_t)22ULL), x78, 1);
  _br2_store((out0)+((uintptr_t)23ULL), x79, 1);
  _br2_store((out0)+((uintptr_t)24ULL), x80, 1);
  _br2_store((out0)+((uintptr_t)25ULL), x81, 1);
  _br2_store((out0)+((uintptr_t)26ULL), x82, 1);
  _br2_store((out0)+((uintptr_t)27ULL), x83, 1);
  /*skip*/
  return;
}

/* NOTE: The following wrapper function is not covered by Coq proofs */
static void fiat_p224_to_bytes(uint8_t out1[28], const uint32_t arg1[7]) {
  internal_fiat_p224_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]]
 * Output Bounds:
 *   out0: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
 */
static
void internal_fiat_p224_from_bytes(uintptr_t out0, uintptr_t in0) {
  uintptr_t 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, x54, x55, x53, x56, x52, x57, x50, x51, x49, x59, x48, x60, x46, x47, x45, x62, x44, x63, x42, x43, x41, x65, x40, x66, x38, x39, x37, x68, x36, x69, x34, x35, x33, x71, x32, x72, x30, x31, x29, x74, x28, x75, x58, x61, x64, x67, x70, x73, x76, x77, x78, x79, x80, x81, x82, x83;
  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);
  /*skip*/
  /*skip*/
  x28 = (x27)<<((uintptr_t)24ULL);
  x29 = (x26)<<((uintptr_t)16ULL);
  x30 = (x25)<<((uintptr_t)8ULL);
  x31 = x24;
  x32 = (x23)<<((uintptr_t)24ULL);
  x33 = (x22)<<((uintptr_t)16ULL);
  x34 = (x21)<<((uintptr_t)8ULL);
  x35 = x20;
  x36 = (x19)<<((uintptr_t)24ULL);
  x37 = (x18)<<((uintptr_t)16ULL);
  x38 = (x17)<<((uintptr_t)8ULL);
  x39 = x16;
  x40 = (x15)<<((uintptr_t)24ULL);
  x41 = (x14)<<((uintptr_t)16ULL);
  x42 = (x13)<<((uintptr_t)8ULL);
  x43 = x12;
  x44 = (x11)<<((uintptr_t)24ULL);
  x45 = (x10)<<((uintptr_t)16ULL);
  x46 = (x9)<<((uintptr_t)8ULL);
  x47 = x8;
  x48 = (x7)<<((uintptr_t)24ULL);
  x49 = (x6)<<((uintptr_t)16ULL);
  x50 = (x5)<<((uintptr_t)8ULL);
  x51 = x4;
  x52 = (x3)<<((uintptr_t)24ULL);
  x53 = (x2)<<((uintptr_t)16ULL);
  x54 = (x1)<<((uintptr_t)8ULL);
  x55 = x0;
  x56 = (x54)+(x55);
  x57 = (x53)+(x56);
  x58 = (x52)+(x57);
  x59 = (x50)+(x51);
  x60 = (x49)+(x59);
  x61 = (x48)+(x60);
  x62 = (x46)+(x47);
  x63 = (x45)+(x62);
  x64 = (x44)+(x63);
  x65 = (x42)+(x43);
  x66 = (x41)+(x65);
  x67 = (x40)+(x66);
  x68 = (x38)+(x39);
  x69 = (x37)+(x68);
  x70 = (x36)+(x69);
  x71 = (x34)+(x35);
  x72 = (x33)+(x71);
  x73 = (x32)+(x72);
  x74 = (x30)+(x31);
  x75 = (x29)+(x74);
  x76 = (x28)+(x75);
  x77 = x58;
  x78 = x61;
  x79 = x64;
  x80 = x67;
  x81 = x70;
  x82 = x73;
  x83 = x76;
  /*skip*/
  _br2_store((out0)+((uintptr_t)0ULL), x77, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)4ULL), x78, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)8ULL), x79, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)12ULL), x80, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)16ULL), x81, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)20ULL), x82, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)24ULL), x83, sizeof(uintptr_t));
  /*skip*/
  return;
}

/* NOTE: The following wrapper function is not covered by Coq proofs */
static void fiat_p224_from_bytes(uint32_t out1[7], const uint8_t arg1[28]) {
  internal_fiat_p224_from_bytes((uintptr_t)out1, (uintptr_t)arg1);
}


/*
 * Input Bounds:
 * Output Bounds:
 *   out0: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
 */
static
void internal_fiat_p224_set_one(uintptr_t out0) {
  uintptr_t x0, x1, x2, x3, x4, x5, x6;
  /*skip*/
  x0 = (uintptr_t)4294967295ULL;
  x1 = (uintptr_t)4294967295ULL;
  x2 = (uintptr_t)4294967295ULL;
  x3 = (uintptr_t)0ULL;
  x4 = (uintptr_t)0ULL;
  x5 = (uintptr_t)0ULL;
  x6 = (uintptr_t)0ULL;
  /*skip*/
  _br2_store((out0)+((uintptr_t)0ULL), x0, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)4ULL), x1, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)8ULL), x2, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)12ULL), x3, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)16ULL), x4, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)20ULL), x5, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)24ULL), x6, sizeof(uintptr_t));
  /*skip*/
  return;
}

/* NOTE: The following wrapper function is not covered by Coq proofs */
static void fiat_p224_set_one(uint32_t out1[7]) {
  internal_fiat_p224_set_one((uintptr_t)out1);
}


/*
 * Input Bounds:
 * Output Bounds:
 *   out0: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
 */
static
void internal_fiat_p224_msat(uintptr_t out0) {
  uintptr_t x0, x1, x2, x3, x4, x5, x6, x7;
  /*skip*/
  x0 = (uintptr_t)1ULL;
  x1 = (uintptr_t)0ULL;
  x2 = (uintptr_t)0ULL;
  x3 = (uintptr_t)4294967295ULL;
  x4 = (uintptr_t)4294967295ULL;
  x5 = (uintptr_t)4294967295ULL;
  x6 = (uintptr_t)4294967295ULL;
  x7 = (uintptr_t)0ULL;
  /*skip*/
  _br2_store((out0)+((uintptr_t)0ULL), x0, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)4ULL), x1, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)8ULL), x2, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)12ULL), x3, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)16ULL), x4, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)20ULL), x5, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)24ULL), x6, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)28ULL), x7, sizeof(uintptr_t));
  /*skip*/
  return;
}

/* NOTE: The following wrapper function is not covered by Coq proofs */
static void fiat_p224_msat(uint32_t out1[8]) {
  internal_fiat_p224_msat((uintptr_t)out1);
}


/*
 * Input Bounds:
 *   in0: [0x0 ~> 0xffffffff]
 *   in1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
 *   in2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
 *   in3: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
 *   in4: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
 * Output Bounds:
 *   out0: [0x0 ~> 0xffffffff]
 *   out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
 *   out2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
 *   out3: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
 *   out4: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
 */
static
uintptr_t internal_fiat_p224_divstep(uintptr_t out1, uintptr_t out2, uintptr_t out3, uintptr_t out4, uintptr_t in0, uintptr_t in1, uintptr_t in2, uintptr_t in3, uintptr_t in4) {
  uintptr_t x30, x32, x33, x34, x36, x37, x39, x40, x42, x43, x45, x46, x48, x49, x51, x52, x54, x55, x57, x58, x0, x61, x1, x63, x2, x65, x3, x67, x4, x69, x5, x71, x6, x73, x7, x60, x75, x8, x76, x62, x78, x9, x79, x64, x81, x10, x82, x66, x84, x11, x85, x68, x87, x12, x88, x70, x90, x13, x91, x72, x93, x14, x94, x74, x96, x15, x97, x99, x100, x102, x103, x105, x106, x108, x109, x111, x112, x114, x115, x117, x118, x121, x122, x123, x125, x126, x127, x128, x130, x131, x132, x133, x135, x136, x137, x138, x140, x141, x142, x143, x145, x146, x147, x148, x150, x153, x155, x157, x158, x159, x161, x162, x163, x164, x166, x167, x168, x169, x171, x172, x173, x174, x176, x177, x151, x178, x22, x21, x20, x19, x18, x17, x16, x187, x185, x188, x190, x191, x184, x192, x194, x195, x183, x196, x198, x199, x182, x200, x202, x203, x181, x204, x206, x207, x180, x208, x210, x211, x186, x214, x189, x216, x193, x218, x197, x219, x220, x222, x223, x201, x224, x225, x227, x228, x205, x229, x230, x232, x233, x209, x234, x212, x213, x236, x23, x237, x215, x239, x24, x240, x217, x242, x25, x243, x221, x245, x26, x246, x226, x248, x27, x249, x231, x251, x28, x252, x31, x235, x254, x29, x255, x258, x259, x261, x262, x264, x265, x267, x268, x270, x271, x273, x274, x276, x277, x279, x280, x260, x77, x283, x80, x284, x263, x285, x287, x288, x83, x289, x266, x290, x292, x293, x86, x294, x269, x295, x297, x298, x89, x299, x272, x300, x302, x303, x92, x304, x275, x305, x307, x308, x95, x309, x278, x310, x312, x313, x98, x314, x281, x101, x316, x317, x104, x319, x320, x107, x322, x323, x110, x325, x326, x113, x328, x329, x116, x331, x332, x257, x119, x334, x335, x318, x238, x338, x241, x339, x321, x340, x342, x343, x244, x344, x324, x345, x347, x348, x247, x349, x327, x350, x352, x353, x250, x354, x330, x355, x357, x358, x253, x359, x333, x360, x362, x363, x256, x364, x336, x365, x367, x370, x372, x374, x375, x376, x378, x379, x380, x381, x383, x384, x385, x386, x388, x389, x390, x391, x393, x394, x368, x395, x35, x282, x286, x291, x296, x301, x306, x311, x315, x120, x406, x152, x407, x124, x409, x154, x410, x129, x412, x156, x413, x134, x415, x160, x416, x139, x418, x165, x419, x144, x421, x170, x422, x179, x149, x424, x175, x425, x337, x427, x369, x428, x341, x430, x371, x431, x346, x433, x373, x434, x351, x436, x377, x437, x356, x439, x382, x440, x361, x442, x387, x443, x396, x366, x445, x392, x446, x397, x38, x41, x44, x47, x50, x53, x56, x59, x398, x399, x400, x401, x402, x403, x404, x405, x408, x411, x414, x417, x420, x423, x426, x429, x432, x435, x438, x441, x444, x447, out0, x448, x449, x450, x451, x452, x453, x454, x455, x456, x457, x458, x459, x460, x461, x462, x463, x464, x465, x466, x467, x468, x469, x470, x471, x472, x473, x474, x475, x476, x477, x478;
  /*skip*/
  x0 = _br2_load((in1)+((uintptr_t)0ULL), sizeof(uintptr_t));
  x1 = _br2_load((in1)+((uintptr_t)4ULL), sizeof(uintptr_t));
  x2 = _br2_load((in1)+((uintptr_t)8ULL), sizeof(uintptr_t));
  x3 = _br2_load((in1)+((uintptr_t)12ULL), sizeof(uintptr_t));
  x4 = _br2_load((in1)+((uintptr_t)16ULL), sizeof(uintptr_t));
  x5 = _br2_load((in1)+((uintptr_t)20ULL), sizeof(uintptr_t));
  x6 = _br2_load((in1)+((uintptr_t)24ULL), sizeof(uintptr_t));
  x7 = _br2_load((in1)+((uintptr_t)28ULL), sizeof(uintptr_t));
  /*skip*/
  x8 = _br2_load((in2)+((uintptr_t)0ULL), sizeof(uintptr_t));
  x9 = _br2_load((in2)+((uintptr_t)4ULL), sizeof(uintptr_t));
  x10 = _br2_load((in2)+((uintptr_t)8ULL), sizeof(uintptr_t));
  x11 = _br2_load((in2)+((uintptr_t)12ULL), sizeof(uintptr_t));
  x12 = _br2_load((in2)+((uintptr_t)16ULL), sizeof(uintptr_t));
  x13 = _br2_load((in2)+((uintptr_t)20ULL), sizeof(uintptr_t));
  x14 = _br2_load((in2)+((uintptr_t)24ULL), sizeof(uintptr_t));
  x15 = _br2_load((in2)+((uintptr_t)28ULL), sizeof(uintptr_t));
  /*skip*/
  x16 = _br2_load((in3)+((uintptr_t)0ULL), sizeof(uintptr_t));
  x17 = _br2_load((in3)+((uintptr_t)4ULL), sizeof(uintptr_t));
  x18 = _br2_load((in3)+((uintptr_t)8ULL), sizeof(uintptr_t));
  x19 = _br2_load((in3)+((uintptr_t)12ULL), sizeof(uintptr_t));
  x20 = _br2_load((in3)+((uintptr_t)16ULL), sizeof(uintptr_t));
  x21 = _br2_load((in3)+((uintptr_t)20ULL), sizeof(uintptr_t));
  x22 = _br2_load((in3)+((uintptr_t)24ULL), sizeof(uintptr_t));
  /*skip*/
  x23 = _br2_load((in4)+((uintptr_t)0ULL), sizeof(uintptr_t));
  x24 = _br2_load((in4)+((uintptr_t)4ULL), sizeof(uintptr_t));
  x25 = _br2_load((in4)+((uintptr_t)8ULL), sizeof(uintptr_t));
  x26 = _br2_load((in4)+((uintptr_t)12ULL), sizeof(uintptr_t));
  x27 = _br2_load((in4)+((uintptr_t)16ULL), sizeof(uintptr_t));
  x28 = _br2_load((in4)+((uintptr_t)20ULL), sizeof(uintptr_t));
  x29 = _br2_load((in4)+((uintptr_t)24ULL), sizeof(uintptr_t));
  /*skip*/
  /*skip*/
  x30 = ((in0)^((uintptr_t)4294967295ULL))+((uintptr_t)1ULL);
  x31 = ((x30)>>((uintptr_t)31ULL))&((x8)&((uintptr_t)1ULL));
  x32 = ((in0)^((uintptr_t)4294967295ULL))+((uintptr_t)1ULL);
  x33 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x34 = (x33)^((uintptr_t)4294967295ULL);
  x35 = ((x32)&(x33))|((in0)&(x34));
  x36 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x37 = (x36)^((uintptr_t)4294967295ULL);
  x38 = ((x8)&(x36))|((x0)&(x37));
  x39 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x40 = (x39)^((uintptr_t)4294967295ULL);
  x41 = ((x9)&(x39))|((x1)&(x40));
  x42 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x43 = (x42)^((uintptr_t)4294967295ULL);
  x44 = ((x10)&(x42))|((x2)&(x43));
  x45 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x46 = (x45)^((uintptr_t)4294967295ULL);
  x47 = ((x11)&(x45))|((x3)&(x46));
  x48 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x49 = (x48)^((uintptr_t)4294967295ULL);
  x50 = ((x12)&(x48))|((x4)&(x49));
  x51 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x52 = (x51)^((uintptr_t)4294967295ULL);
  x53 = ((x13)&(x51))|((x5)&(x52));
  x54 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x55 = (x54)^((uintptr_t)4294967295ULL);
  x56 = ((x14)&(x54))|((x6)&(x55));
  x57 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x58 = (x57)^((uintptr_t)4294967295ULL);
  x59 = ((x15)&(x57))|((x7)&(x58));
  x60 = ((uintptr_t)1ULL)+((x0)^((uintptr_t)4294967295ULL));
  x61 = (x60)<((uintptr_t)1ULL);
  x62 = (x61)+((x1)^((uintptr_t)4294967295ULL));
  x63 = (x62)<((x1)^((uintptr_t)4294967295ULL));
  x64 = (x63)+((x2)^((uintptr_t)4294967295ULL));
  x65 = (x64)<((x2)^((uintptr_t)4294967295ULL));
  x66 = (x65)+((x3)^((uintptr_t)4294967295ULL));
  x67 = (x66)<((x3)^((uintptr_t)4294967295ULL));
  x68 = (x67)+((x4)^((uintptr_t)4294967295ULL));
  x69 = (x68)<((x4)^((uintptr_t)4294967295ULL));
  x70 = (x69)+((x5)^((uintptr_t)4294967295ULL));
  x71 = (x70)<((x5)^((uintptr_t)4294967295ULL));
  x72 = (x71)+((x6)^((uintptr_t)4294967295ULL));
  x73 = (x72)<((x6)^((uintptr_t)4294967295ULL));
  x74 = (x73)+((x7)^((uintptr_t)4294967295ULL));
  x75 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x76 = (x75)^((uintptr_t)4294967295ULL);
  x77 = ((x60)&(x75))|((x8)&(x76));
  x78 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x79 = (x78)^((uintptr_t)4294967295ULL);
  x80 = ((x62)&(x78))|((x9)&(x79));
  x81 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x82 = (x81)^((uintptr_t)4294967295ULL);
  x83 = ((x64)&(x81))|((x10)&(x82));
  x84 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x85 = (x84)^((uintptr_t)4294967295ULL);
  x86 = ((x66)&(x84))|((x11)&(x85));
  x87 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x88 = (x87)^((uintptr_t)4294967295ULL);
  x89 = ((x68)&(x87))|((x12)&(x88));
  x90 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x91 = (x90)^((uintptr_t)4294967295ULL);
  x92 = ((x70)&(x90))|((x13)&(x91));
  x93 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x94 = (x93)^((uintptr_t)4294967295ULL);
  x95 = ((x72)&(x93))|((x14)&(x94));
  x96 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x97 = (x96)^((uintptr_t)4294967295ULL);
  x98 = ((x74)&(x96))|((x15)&(x97));
  x99 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x100 = (x99)^((uintptr_t)4294967295ULL);
  x101 = ((x23)&(x99))|((x16)&(x100));
  x102 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x103 = (x102)^((uintptr_t)4294967295ULL);
  x104 = ((x24)&(x102))|((x17)&(x103));
  x105 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x106 = (x105)^((uintptr_t)4294967295ULL);
  x107 = ((x25)&(x105))|((x18)&(x106));
  x108 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x109 = (x108)^((uintptr_t)4294967295ULL);
  x110 = ((x26)&(x108))|((x19)&(x109));
  x111 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x112 = (x111)^((uintptr_t)4294967295ULL);
  x113 = ((x27)&(x111))|((x20)&(x112));
  x114 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x115 = (x114)^((uintptr_t)4294967295ULL);
  x116 = ((x28)&(x114))|((x21)&(x115));
  x117 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x118 = (x117)^((uintptr_t)4294967295ULL);
  x119 = ((x29)&(x117))|((x22)&(x118));
  x120 = (x101)+(x101);
  x121 = (x120)<(x101);
  x122 = (x121)+(x104);
  x123 = (x122)<(x104);
  x124 = (x122)+(x104);
  x125 = (x124)<(x104);
  x126 = (x123)+(x125);
  x127 = (x126)+(x107);
  x128 = (x127)<(x107);
  x129 = (x127)+(x107);
  x130 = (x129)<(x107);
  x131 = (x128)+(x130);
  x132 = (x131)+(x110);
  x133 = (x132)<(x110);
  x134 = (x132)+(x110);
  x135 = (x134)<(x110);
  x136 = (x133)+(x135);
  x137 = (x136)+(x113);
  x138 = (x137)<(x113);
  x139 = (x137)+(x113);
  x140 = (x139)<(x113);
  x141 = (x138)+(x140);
  x142 = (x141)+(x116);
  x143 = (x142)<(x116);
  x144 = (x142)+(x116);
  x145 = (x144)<(x116);
  x146 = (x143)+(x145);
  x147 = (x146)+(x119);
  x148 = (x147)<(x119);
  x149 = (x147)+(x119);
  x150 = (x149)<(x119);
  x151 = (x148)+(x150);
  x152 = (x120)-((uintptr_t)1ULL);
  x153 = (x120)<(x152);
  x154 = (x124)-(x153);
  x155 = (x124)<(x154);
  x156 = (x129)-(x155);
  x157 = (x129)<(x156);
  x158 = (x134)-((uintptr_t)4294967295ULL);
  x159 = (x134)<(x158);
  x160 = (x158)-(x157);
  x161 = (x158)<(x160);
  x162 = (x159)+(x161);
  x163 = (x139)-((uintptr_t)4294967295ULL);
  x164 = (x139)<(x163);
  x165 = (x163)-(x162);
  x166 = (x163)<(x165);
  x167 = (x164)+(x166);
  x168 = (x144)-((uintptr_t)4294967295ULL);
  x169 = (x144)<(x168);
  x170 = (x168)-(x167);
  x171 = (x168)<(x170);
  x172 = (x169)+(x171);
  x173 = (x149)-((uintptr_t)4294967295ULL);
  x174 = (x149)<(x173);
  x175 = (x173)-(x172);
  x176 = (x173)<(x175);
  x177 = (x174)+(x176);
  x178 = (x151)-(x177);
  x179 = (x151)<(x178);
  x180 = x22;
  x181 = x21;
  x182 = x20;
  x183 = x19;
  x184 = x18;
  x185 = x17;
  x186 = x16;
  x187 = ((uintptr_t)0ULL)<(((uintptr_t)0ULL)-(x186));
  x188 = ((uintptr_t)0ULL)<(((uintptr_t)0ULL)-(x185));
  x189 = (((uintptr_t)0ULL)-(x185))-(x187);
  x190 = (((uintptr_t)0ULL)-(x185))<(x189);
  x191 = (x188)+(x190);
  x192 = ((uintptr_t)0ULL)<(((uintptr_t)0ULL)-(x184));
  x193 = (((uintptr_t)0ULL)-(x184))-(x191);
  x194 = (((uintptr_t)0ULL)-(x184))<(x193);
  x195 = (x192)+(x194);
  x196 = ((uintptr_t)0ULL)<(((uintptr_t)0ULL)-(x183));
  x197 = (((uintptr_t)0ULL)-(x183))-(x195);
  x198 = (((uintptr_t)0ULL)-(x183))<(x197);
  x199 = (x196)+(x198);
  x200 = ((uintptr_t)0ULL)<(((uintptr_t)0ULL)-(x182));
  x201 = (((uintptr_t)0ULL)-(x182))-(x199);
  x202 = (((uintptr_t)0ULL)-(x182))<(x201);
  x203 = (x200)+(x202);
  x204 = ((uintptr_t)0ULL)<(((uintptr_t)0ULL)-(x181));
  x205 = (((uintptr_t)0ULL)-(x181))-(x203);
  x206 = (((uintptr_t)0ULL)-(x181))<(x205);
  x207 = (x204)+(x206);
  x208 = ((uintptr_t)0ULL)<(((uintptr_t)0ULL)-(x180));
  x209 = (((uintptr_t)0ULL)-(x180))-(x207);
  x210 = (((uintptr_t)0ULL)-(x180))<(x209);
  x211 = (x208)+(x210);
  x212 = ((uintptr_t)-1ULL)+((x211)==((uintptr_t)0ULL));
  x213 = (((uintptr_t)0ULL)-(x186))+((x212)&((uintptr_t)1ULL));
  x214 = (x213)<(((uintptr_t)0ULL)-(x186));
  x215 = (x214)+(x189);
  x216 = (x215)<(x189);
  x217 = (x216)+(x193);
  x218 = (x217)<(x193);
  x219 = (x218)+(x197);
  x220 = (x219)<(x197);
  x221 = (x219)+(x212);
  x222 = (x221)<(x212);
  x223 = (x220)+(x222);
  x224 = (x223)+(x201);
  x225 = (x224)<(x201);
  x226 = (x224)+(x212);
  x227 = (x226)<(x212);
  x228 = (x225)+(x227);
  x229 = (x228)+(x205);
  x230 = (x229)<(x205);
  x231 = (x229)+(x212);
  x232 = (x231)<(x212);
  x233 = (x230)+(x232);
  x234 = (x233)+(x209);
  x235 = (x234)+(x212);
  x236 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x237 = (x236)^((uintptr_t)4294967295ULL);
  x238 = ((x213)&(x236))|((x23)&(x237));
  x239 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x240 = (x239)^((uintptr_t)4294967295ULL);
  x241 = ((x215)&(x239))|((x24)&(x240));
  x242 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x243 = (x242)^((uintptr_t)4294967295ULL);
  x244 = ((x217)&(x242))|((x25)&(x243));
  x245 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x246 = (x245)^((uintptr_t)4294967295ULL);
  x247 = ((x221)&(x245))|((x26)&(x246));
  x248 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x249 = (x248)^((uintptr_t)4294967295ULL);
  x250 = ((x226)&(x248))|((x27)&(x249));
  x251 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x252 = (x251)^((uintptr_t)4294967295ULL);
  x253 = ((x231)&(x251))|((x28)&(x252));
  x254 = ((uintptr_t)-1ULL)+((x31)==((uintptr_t)0ULL));
  x255 = (x254)^((uintptr_t)4294967295ULL);
  x256 = ((x235)&(x254))|((x29)&(x255));
  x257 = (x77)&((uintptr_t)1ULL);
  x258 = ((uintptr_t)-1ULL)+((x257)==((uintptr_t)0ULL));
  x259 = (x258)^((uintptr_t)4294967295ULL);
  x260 = ((x38)&(x258))|(((uintptr_t)0ULL)&(x259));
  x261 = ((uintptr_t)-1ULL)+((x257)==((uintptr_t)0ULL));
  x262 = (x261)^((uintptr_t)4294967295ULL);
  x263 = ((x41)&(x261))|(((uintptr_t)0ULL)&(x262));
  x264 = ((uintptr_t)-1ULL)+((x257)==((uintptr_t)0ULL));
  x265 = (x264)^((uintptr_t)4294967295ULL);
  x266 = ((x44)&(x264))|(((uintptr_t)0ULL)&(x265));
  x267 = ((uintptr_t)-1ULL)+((x257)==((uintptr_t)0ULL));
  x268 = (x267)^((uintptr_t)4294967295ULL);
  x269 = ((x47)&(x267))|(((uintptr_t)0ULL)&(x268));
  x270 = ((uintptr_t)-1ULL)+((x257)==((uintptr_t)0ULL));
  x271 = (x270)^((uintptr_t)4294967295ULL);
  x272 = ((x50)&(x270))|(((uintptr_t)0ULL)&(x271));
  x273 = ((uintptr_t)-1ULL)+((x257)==((uintptr_t)0ULL));
  x274 = (x273)^((uintptr_t)4294967295ULL);
  x275 = ((x53)&(x273))|(((uintptr_t)0ULL)&(x274));
  x276 = ((uintptr_t)-1ULL)+((x257)==((uintptr_t)0ULL));
  x277 = (x276)^((uintptr_t)4294967295ULL);
  x278 = ((x56)&(x276))|(((uintptr_t)0ULL)&(x277));
  x279 = ((uintptr_t)-1ULL)+((x257)==((uintptr_t)0ULL));
  x280 = (x279)^((uintptr_t)4294967295ULL);
  x281 = ((x59)&(x279))|(((uintptr_t)0ULL)&(x280));
  x282 = (x77)+(x260);
  x283 = (x282)<(x77);
  x284 = (x283)+(x80);
  x285 = (x284)<(x80);
  x286 = (x284)+(x263);
  x287 = (x286)<(x263);
  x288 = (x285)+(x287);
  x289 = (x288)+(x83);
  x290 = (x289)<(x83);
  x291 = (x289)+(x266);
  x292 = (x291)<(x266);
  x293 = (x290)+(x292);
  x294 = (x293)+(x86);
  x295 = (x294)<(x86);
  x296 = (x294)+(x269);
  x297 = (x296)<(x269);
  x298 = (x295)+(x297);
  x299 = (x298)+(x89);
  x300 = (x299)<(x89);
  x301 = (x299)+(x272);
  x302 = (x301)<(x272);
  x303 = (x300)+(x302);
  x304 = (x303)+(x92);
  x305 = (x304)<(x92);
  x306 = (x304)+(x275);
  x307 = (x306)<(x275);
  x308 = (x305)+(x307);
  x309 = (x308)+(x95);
  x310 = (x309)<(x95);
  x311 = (x309)+(x278);
  x312 = (x311)<(x278);
  x313 = (x310)+(x312);
  x314 = (x313)+(x98);
  x315 = (x314)+(x281);
  x316 = ((uintptr_t)-1ULL)+((x257)==((uintptr_t)0ULL));
  x317 = (x316)^((uintptr_t)4294967295ULL);
  x318 = ((x101)&(x316))|(((uintptr_t)0ULL)&(x317));
  x319 = ((uintptr_t)-1ULL)+((x257)==((uintptr_t)0ULL));
  x320 = (x319)^((uintptr_t)4294967295ULL);
  x321 = ((x104)&(x319))|(((uintptr_t)0ULL)&(x320));
  x322 = ((uintptr_t)-1ULL)+((x257)==((uintptr_t)0ULL));
  x323 = (x322)^((uintptr_t)4294967295ULL);
  x324 = ((x107)&(x322))|(((uintptr_t)0ULL)&(x323));
  x325 = ((uintptr_t)-1ULL)+((x257)==((uintptr_t)0ULL));
  x326 = (x325)^((uintptr_t)4294967295ULL);
  x327 = ((x110)&(x325))|(((uintptr_t)0ULL)&(x326));
  x328 = ((uintptr_t)-1ULL)+((x257)==((uintptr_t)0ULL));
  x329 = (x328)^((uintptr_t)4294967295ULL);
  x330 = ((x113)&(x328))|(((uintptr_t)0ULL)&(x329));
  x331 = ((uintptr_t)-1ULL)+((x257)==((uintptr_t)0ULL));
  x332 = (x331)^((uintptr_t)4294967295ULL);
  x333 = ((x116)&(x331))|(((uintptr_t)0ULL)&(x332));
  x334 = ((uintptr_t)-1ULL)+((x257)==((uintptr_t)0ULL));
  x335 = (x334)^((uintptr_t)4294967295ULL);
  x336 = ((x119)&(x334))|(((uintptr_t)0ULL)&(x335));
  x337 = (x238)+(x318);
  x338 = (x337)<(x238);
  x339 = (x338)+(x241);
  x340 = (x339)<(x241);
  x341 = (x339)+(x321);
  x342 = (x341)<(x321);
  x343 = (x340)+(x342);
  x344 = (x343)+(x244);
  x345 = (x344)<(x244);
  x346 = (x344)+(x324);
  x347 = (x346)<(x324);
  x348 = (x345)+(x347);
  x349 = (x348)+(x247);
  x350 = (x349)<(x247);
  x351 = (x349)+(x327);
  x352 = (x351)<(x327);
  x353 = (x350)+(x352);
  x354 = (x353)+(x250);
  x355 = (x354)<(x250);
  x356 = (x354)+(x330);
  x357 = (x356)<(x330);
  x358 = (x355)+(x357);
  x359 = (x358)+(x253);
  x360 = (x359)<(x253);
  x361 = (x359)+(x333);
  x362 = (x361)<(x333);
  x363 = (x360)+(x362);
  x364 = (x363)+(x256);
  x365 = (x364)<(x256);
  x366 = (x364)+(x336);
  x367 = (x366)<(x336);
  x368 = (x365)+(x367);
  x369 = (x337)-((uintptr_t)1ULL);
  x370 = (x337)<(x369);
  x371 = (x341)-(x370);
  x372 = (x341)<(x371);
  x373 = (x346)-(x372);
  x374 = (x346)<(x373);
  x375 = (x351)-((uintptr_t)4294967295ULL);
  x376 = (x351)<(x375);
  x377 = (x375)-(x374);
  x378 = (x375)<(x377);
  x379 = (x376)+(x378);
  x380 = (x356)-((uintptr_t)4294967295ULL);
  x381 = (x356)<(x380);
  x382 = (x380)-(x379);
  x383 = (x380)<(x382);
  x384 = (x381)+(x383);
  x385 = (x361)-((uintptr_t)4294967295ULL);
  x386 = (x361)<(x385);
  x387 = (x385)-(x384);
  x388 = (x385)<(x387);
  x389 = (x386)+(x388);
  x390 = (x366)-((uintptr_t)4294967295ULL);
  x391 = (x366)<(x390);
  x392 = (x390)-(x389);
  x393 = (x390)<(x392);
  x394 = (x391)+(x393);
  x395 = (x368)-(x394);
  x396 = (x368)<(x395);
  x397 = (x35)+((uintptr_t)1ULL);
  x398 = ((x282)>>((uintptr_t)1ULL))|((x286)<<((uintptr_t)31ULL));
  x399 = ((x286)>>((uintptr_t)1ULL))|((x291)<<((uintptr_t)31ULL));
  x400 = ((x291)>>((uintptr_t)1ULL))|((x296)<<((uintptr_t)31ULL));
  x401 = ((x296)>>((uintptr_t)1ULL))|((x301)<<((uintptr_t)31ULL));
  x402 = ((x301)>>((uintptr_t)1ULL))|((x306)<<((uintptr_t)31ULL));
  x403 = ((x306)>>((uintptr_t)1ULL))|((x311)<<((uintptr_t)31ULL));
  x404 = ((x311)>>((uintptr_t)1ULL))|((x315)<<((uintptr_t)31ULL));
  x405 = ((x315)&((uintptr_t)2147483648ULL))|((x315)>>((uintptr_t)1ULL));
  x406 = ((uintptr_t)-1ULL)+((x179)==((uintptr_t)0ULL));
  x407 = (x406)^((uintptr_t)4294967295ULL);
  x408 = ((x120)&(x406))|((x152)&(x407));
  x409 = ((uintptr_t)-1ULL)+((x179)==((uintptr_t)0ULL));
  x410 = (x409)^((uintptr_t)4294967295ULL);
  x411 = ((x124)&(x409))|((x154)&(x410));
  x412 = ((uintptr_t)-1ULL)+((x179)==((uintptr_t)0ULL));
  x413 = (x412)^((uintptr_t)4294967295ULL);
  x414 = ((x129)&(x412))|((x156)&(x413));
  x415 = ((uintptr_t)-1ULL)+((x179)==((uintptr_t)0ULL));
  x416 = (x415)^((uintptr_t)4294967295ULL);
  x417 = ((x134)&(x415))|((x160)&(x416));
  x418 = ((uintptr_t)-1ULL)+((x179)==((uintptr_t)0ULL));
  x419 = (x418)^((uintptr_t)4294967295ULL);
  x420 = ((x139)&(x418))|((x165)&(x419));
  x421 = ((uintptr_t)-1ULL)+((x179)==((uintptr_t)0ULL));
  x422 = (x421)^((uintptr_t)4294967295ULL);
  x423 = ((x144)&(x421))|((x170)&(x422));
  x424 = ((uintptr_t)-1ULL)+((x179)==((uintptr_t)0ULL));
  x425 = (x424)^((uintptr_t)4294967295ULL);
  x426 = ((x149)&(x424))|((x175)&(x425));
  x427 = ((uintptr_t)-1ULL)+((x396)==((uintptr_t)0ULL));
  x428 = (x427)^((uintptr_t)4294967295ULL);
  x429 = ((x337)&(x427))|((x369)&(x428));
  x430 = ((uintptr_t)-1ULL)+((x396)==((uintptr_t)0ULL));
  x431 = (x430)^((uintptr_t)4294967295ULL);
  x432 = ((x341)&(x430))|((x371)&(x431));
  x433 = ((uintptr_t)-1ULL)+((x396)==((uintptr_t)0ULL));
  x434 = (x433)^((uintptr_t)4294967295ULL);
  x435 = ((x346)&(x433))|((x373)&(x434));
  x436 = ((uintptr_t)-1ULL)+((x396)==((uintptr_t)0ULL));
  x437 = (x436)^((uintptr_t)4294967295ULL);
  x438 = ((x351)&(x436))|((x377)&(x437));
  x439 = ((uintptr_t)-1ULL)+((x396)==((uintptr_t)0ULL));
  x440 = (x439)^((uintptr_t)4294967295ULL);
  x441 = ((x356)&(x439))|((x382)&(x440));
  x442 = ((uintptr_t)-1ULL)+((x396)==((uintptr_t)0ULL));
  x443 = (x442)^((uintptr_t)4294967295ULL);
  x444 = ((x361)&(x442))|((x387)&(x443));
  x445 = ((uintptr_t)-1ULL)+((x396)==((uintptr_t)0ULL));
  x446 = (x445)^((uintptr_t)4294967295ULL);
  x447 = ((x366)&(x445))|((x392)&(x446));
  x448 = x397;
  x449 = x38;
  x450 = x41;
  x451 = x44;
  x452 = x47;
  x453 = x50;
  x454 = x53;
  x455 = x56;
  x456 = x59;
  /*skip*/
  x457 = x398;
  x458 = x399;
  x459 = x400;
  x460 = x401;
  x461 = x402;
  x462 = x403;
  x463 = x404;
  x464 = x405;
  /*skip*/
  x465 = x408;
  x466 = x411;
  x467 = x414;
  x468 = x417;
  x469 = x420;
  x470 = x423;
  x471 = x426;
  /*skip*/
  x472 = x429;
  x473 = x432;
  x474 = x435;
  x475 = x438;
  x476 = x441;
  x477 = x444;
  x478 = x447;
  /*skip*/
  out0 = x448;
  _br2_store((out1)+((uintptr_t)0ULL), x449, sizeof(uintptr_t));
  _br2_store((out1)+((uintptr_t)4ULL), x450, sizeof(uintptr_t));
  _br2_store((out1)+((uintptr_t)8ULL), x451, sizeof(uintptr_t));
  _br2_store((out1)+((uintptr_t)12ULL), x452, sizeof(uintptr_t));
  _br2_store((out1)+((uintptr_t)16ULL), x453, sizeof(uintptr_t));
  _br2_store((out1)+((uintptr_t)20ULL), x454, sizeof(uintptr_t));
  _br2_store((out1)+((uintptr_t)24ULL), x455, sizeof(uintptr_t));
  _br2_store((out1)+((uintptr_t)28ULL), x456, sizeof(uintptr_t));
  /*skip*/
  _br2_store((out2)+((uintptr_t)0ULL), x457, sizeof(uintptr_t));
  _br2_store((out2)+((uintptr_t)4ULL), x458, sizeof(uintptr_t));
  _br2_store((out2)+((uintptr_t)8ULL), x459, sizeof(uintptr_t));
  _br2_store((out2)+((uintptr_t)12ULL), x460, sizeof(uintptr_t));
  _br2_store((out2)+((uintptr_t)16ULL), x461, sizeof(uintptr_t));
  _br2_store((out2)+((uintptr_t)20ULL), x462, sizeof(uintptr_t));
  _br2_store((out2)+((uintptr_t)24ULL), x463, sizeof(uintptr_t));
  _br2_store((out2)+((uintptr_t)28ULL), x464, sizeof(uintptr_t));
  /*skip*/
  _br2_store((out3)+((uintptr_t)0ULL), x465, sizeof(uintptr_t));
  _br2_store((out3)+((uintptr_t)4ULL), x466, sizeof(uintptr_t));
  _br2_store((out3)+((uintptr_t)8ULL), x467, sizeof(uintptr_t));
  _br2_store((out3)+((uintptr_t)12ULL), x468, sizeof(uintptr_t));
  _br2_store((out3)+((uintptr_t)16ULL), x469, sizeof(uintptr_t));
  _br2_store((out3)+((uintptr_t)20ULL), x470, sizeof(uintptr_t));
  _br2_store((out3)+((uintptr_t)24ULL), x471, sizeof(uintptr_t));
  /*skip*/
  _br2_store((out4)+((uintptr_t)0ULL), x472, sizeof(uintptr_t));
  _br2_store((out4)+((uintptr_t)4ULL), x473, sizeof(uintptr_t));
  _br2_store((out4)+((uintptr_t)8ULL), x474, sizeof(uintptr_t));
  _br2_store((out4)+((uintptr_t)12ULL), x475, sizeof(uintptr_t));
  _br2_store((out4)+((uintptr_t)16ULL), x476, sizeof(uintptr_t));
  _br2_store((out4)+((uintptr_t)20ULL), x477, sizeof(uintptr_t));
  _br2_store((out4)+((uintptr_t)24ULL), x478, sizeof(uintptr_t));
  /*skip*/
  return out0;
}

/* NOTE: The following wrapper function is not covered by Coq proofs */
static void fiat_p224_divstep(uint32_t* out1, uint32_t out2[8], uint32_t out3[8], uint32_t out4[7], uint32_t out5[7], uint32_t arg1, const uint32_t arg2[8], const uint32_t arg3[8], const uint32_t arg4[7], const uint32_t arg5[7]) {
  *out1 = (uint32_t)internal_fiat_p224_divstep((uintptr_t)out2, (uintptr_t)out3, (uintptr_t)out4, (uintptr_t)out5, (uintptr_t)arg1, (uintptr_t)arg2, (uintptr_t)arg3, (uintptr_t)arg4, (uintptr_t)arg5);
}


/*
 * Input Bounds:
 * Output Bounds:
 *   out0: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
 */
static
void internal_fiat_p224_divstep_precomp(uintptr_t out0) {
  uintptr_t x0, x1, x2, x3, x4, x5, x6;
  /*skip*/
  x0 = (uintptr_t)8388608ULL;
  x1 = (uintptr_t)8388608ULL;
  x2 = (uintptr_t)4261412864ULL;
  x3 = (uintptr_t)16777215ULL;
  x4 = (uintptr_t)0ULL;
  x5 = (uintptr_t)4286578688ULL;
  x6 = (uintptr_t)25165823ULL;
  /*skip*/
  _br2_store((out0)+((uintptr_t)0ULL), x0, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)4ULL), x1, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)8ULL), x2, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)12ULL), x3, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)16ULL), x4, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)20ULL), x5, sizeof(uintptr_t));
  _br2_store((out0)+((uintptr_t)24ULL), x6, sizeof(uintptr_t));
  /*skip*/
  return;
}

/* NOTE: The following wrapper function is not covered by Coq proofs */
static void fiat_p224_divstep_precomp(uint32_t out1[7]) {
  internal_fiat_p224_divstep_precomp((uintptr_t)out1);
}