aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/montgomery64_2e321m9_6limbs/femul.c
blob: b56aef734c4320a776781deae3d521411c5230e0 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
static void femul(uint64_t out[6], const uint64_t in1[6], const uint64_t in2[6]) {
  { const uint64_t x12 = in1[5];
  { const uint64_t x13 = in1[4];
  { const uint64_t x11 = in1[3];
  { const uint64_t x9 = in1[2];
  { const uint64_t x7 = in1[1];
  { const uint64_t x5 = in1[0];
  { const uint64_t x22 = in2[5];
  { const uint64_t x23 = in2[4];
  { const uint64_t x21 = in2[3];
  { const uint64_t x19 = in2[2];
  { const uint64_t x17 = in2[1];
  { const uint64_t x15 = in2[0];
  { uint64_t x26;  uint64_t x25 = _mulx_u64(x5, x15, &x26);
  { uint64_t x29;  uint64_t x28 = _mulx_u64(x5, x17, &x29);
  { uint64_t x32;  uint64_t x31 = _mulx_u64(x5, x19, &x32);
  { uint64_t x35;  uint64_t x34 = _mulx_u64(x5, x21, &x35);
  { uint64_t x38;  uint64_t x37 = _mulx_u64(x5, x23, &x38);
  { uint64_t x41;  uint64_t x40 = _mulx_u64(x5, x22, &x41);
  { uint64_t x43; uint8_t x44 = _addcarryx_u64(0x0, x26, x28, &x43);
  { uint64_t x46; uint8_t x47 = _addcarryx_u64(x44, x29, x31, &x46);
  { uint64_t x49; uint8_t x50 = _addcarryx_u64(x47, x32, x34, &x49);
  { uint64_t x52; uint8_t x53 = _addcarryx_u64(x50, x35, x37, &x52);
  { uint64_t x55; uint8_t x56 = _addcarryx_u64(x53, x38, x40, &x55);
  { uint64_t x58; uint8_t _ = _addcarryx_u64(0x0, x56, x41, &x58);
  { uint64_t _;  uint64_t x61 = _mulx_u64(x25, 0x8e38e38e38e38e39L, &_);
  { uint64_t x65;  uint64_t x64 = _mulx_u64(x61, 0xfffffffffffffff7L, &x65);
  { uint64_t x68;  uint64_t x67 = _mulx_u64(x61, 0xffffffffffffffffL, &x68);
  { uint64_t x71;  uint64_t x70 = _mulx_u64(x61, 0xffffffffffffffffL, &x71);
  { uint64_t x74;  uint64_t x73 = _mulx_u64(x61, 0xffffffffffffffffL, &x74);
  { uint64_t x77;  uint64_t x76 = _mulx_u64(x61, 0xffffffffffffffffL, &x77);
  { uint64_t x79; uint8_t x80 = _addcarryx_u64(0x0, x65, x67, &x79);
  { uint64_t x82; uint8_t x83 = _addcarryx_u64(x80, x68, x70, &x82);
  { uint64_t x85; uint8_t x86 = _addcarryx_u64(x83, x71, x73, &x85);
  { uint64_t x88; uint8_t x89 = _addcarryx_u64(x86, x74, x76, &x88);
  { uint64_t x91; uint8_t x92 = _addcarryx_u64(x89, x77, x61, &x91);
  { uint64_t _; uint8_t x95 = _addcarryx_u64(0x0, x25, x64, &_);
  { uint64_t x97; uint8_t x98 = _addcarryx_u64(x95, x43, x79, &x97);
  { uint64_t x100; uint8_t x101 = _addcarryx_u64(x98, x46, x82, &x100);
  { uint64_t x103; uint8_t x104 = _addcarryx_u64(x101, x49, x85, &x103);
  { uint64_t x106; uint8_t x107 = _addcarryx_u64(x104, x52, x88, &x106);
  { uint64_t x109; uint8_t x110 = _addcarryx_u64(x107, x55, x91, &x109);
  { uint64_t x112; uint8_t x113 = _addcarryx_u64(x110, x58, x92, &x112);
  { uint64_t x116;  uint64_t x115 = _mulx_u64(x7, x15, &x116);
  { uint64_t x119;  uint64_t x118 = _mulx_u64(x7, x17, &x119);
  { uint64_t x122;  uint64_t x121 = _mulx_u64(x7, x19, &x122);
  { uint64_t x125;  uint64_t x124 = _mulx_u64(x7, x21, &x125);
  { uint64_t x128;  uint64_t x127 = _mulx_u64(x7, x23, &x128);
  { uint64_t x131;  uint64_t x130 = _mulx_u64(x7, x22, &x131);
  { uint64_t x133; uint8_t x134 = _addcarryx_u64(0x0, x116, x118, &x133);
  { uint64_t x136; uint8_t x137 = _addcarryx_u64(x134, x119, x121, &x136);
  { uint64_t x139; uint8_t x140 = _addcarryx_u64(x137, x122, x124, &x139);
  { uint64_t x142; uint8_t x143 = _addcarryx_u64(x140, x125, x127, &x142);
  { uint64_t x145; uint8_t x146 = _addcarryx_u64(x143, x128, x130, &x145);
  { uint64_t x148; uint8_t _ = _addcarryx_u64(0x0, x146, x131, &x148);
  { uint64_t x151; uint8_t x152 = _addcarryx_u64(0x0, x97, x115, &x151);
  { uint64_t x154; uint8_t x155 = _addcarryx_u64(x152, x100, x133, &x154);
  { uint64_t x157; uint8_t x158 = _addcarryx_u64(x155, x103, x136, &x157);
  { uint64_t x160; uint8_t x161 = _addcarryx_u64(x158, x106, x139, &x160);
  { uint64_t x163; uint8_t x164 = _addcarryx_u64(x161, x109, x142, &x163);
  { uint64_t x166; uint8_t x167 = _addcarryx_u64(x164, x112, x145, &x166);
  { uint64_t x169; uint8_t x170 = _addcarryx_u64(x167, x113, x148, &x169);
  { uint64_t _;  uint64_t x172 = _mulx_u64(x151, 0x8e38e38e38e38e39L, &_);
  { uint64_t x176;  uint64_t x175 = _mulx_u64(x172, 0xfffffffffffffff7L, &x176);
  { uint64_t x179;  uint64_t x178 = _mulx_u64(x172, 0xffffffffffffffffL, &x179);
  { uint64_t x182;  uint64_t x181 = _mulx_u64(x172, 0xffffffffffffffffL, &x182);
  { uint64_t x185;  uint64_t x184 = _mulx_u64(x172, 0xffffffffffffffffL, &x185);
  { uint64_t x188;  uint64_t x187 = _mulx_u64(x172, 0xffffffffffffffffL, &x188);
  { uint64_t x190; uint8_t x191 = _addcarryx_u64(0x0, x176, x178, &x190);
  { uint64_t x193; uint8_t x194 = _addcarryx_u64(x191, x179, x181, &x193);
  { uint64_t x196; uint8_t x197 = _addcarryx_u64(x194, x182, x184, &x196);
  { uint64_t x199; uint8_t x200 = _addcarryx_u64(x197, x185, x187, &x199);
  { uint64_t x202; uint8_t x203 = _addcarryx_u64(x200, x188, x172, &x202);
  { uint64_t _; uint8_t x206 = _addcarryx_u64(0x0, x151, x175, &_);
  { uint64_t x208; uint8_t x209 = _addcarryx_u64(x206, x154, x190, &x208);
  { uint64_t x211; uint8_t x212 = _addcarryx_u64(x209, x157, x193, &x211);
  { uint64_t x214; uint8_t x215 = _addcarryx_u64(x212, x160, x196, &x214);
  { uint64_t x217; uint8_t x218 = _addcarryx_u64(x215, x163, x199, &x217);
  { uint64_t x220; uint8_t x221 = _addcarryx_u64(x218, x166, x202, &x220);
  { uint64_t x223; uint8_t x224 = _addcarryx_u64(x221, x169, x203, &x223);
  { uint8_t x225 = (x224 + x170);
  { uint64_t x228;  uint64_t x227 = _mulx_u64(x9, x15, &x228);
  { uint64_t x231;  uint64_t x230 = _mulx_u64(x9, x17, &x231);
  { uint64_t x234;  uint64_t x233 = _mulx_u64(x9, x19, &x234);
  { uint64_t x237;  uint64_t x236 = _mulx_u64(x9, x21, &x237);
  { uint64_t x240;  uint64_t x239 = _mulx_u64(x9, x23, &x240);
  { uint64_t x243;  uint64_t x242 = _mulx_u64(x9, x22, &x243);
  { uint64_t x245; uint8_t x246 = _addcarryx_u64(0x0, x228, x230, &x245);
  { uint64_t x248; uint8_t x249 = _addcarryx_u64(x246, x231, x233, &x248);
  { uint64_t x251; uint8_t x252 = _addcarryx_u64(x249, x234, x236, &x251);
  { uint64_t x254; uint8_t x255 = _addcarryx_u64(x252, x237, x239, &x254);
  { uint64_t x257; uint8_t x258 = _addcarryx_u64(x255, x240, x242, &x257);
  { uint64_t x260; uint8_t _ = _addcarryx_u64(0x0, x258, x243, &x260);
  { uint64_t x263; uint8_t x264 = _addcarryx_u64(0x0, x208, x227, &x263);
  { uint64_t x266; uint8_t x267 = _addcarryx_u64(x264, x211, x245, &x266);
  { uint64_t x269; uint8_t x270 = _addcarryx_u64(x267, x214, x248, &x269);
  { uint64_t x272; uint8_t x273 = _addcarryx_u64(x270, x217, x251, &x272);
  { uint64_t x275; uint8_t x276 = _addcarryx_u64(x273, x220, x254, &x275);
  { uint64_t x278; uint8_t x279 = _addcarryx_u64(x276, x223, x257, &x278);
  { uint64_t x281; uint8_t x282 = _addcarryx_u64(x279, x225, x260, &x281);
  { uint64_t _;  uint64_t x284 = _mulx_u64(x263, 0x8e38e38e38e38e39L, &_);
  { uint64_t x288;  uint64_t x287 = _mulx_u64(x284, 0xfffffffffffffff7L, &x288);
  { uint64_t x291;  uint64_t x290 = _mulx_u64(x284, 0xffffffffffffffffL, &x291);
  { uint64_t x294;  uint64_t x293 = _mulx_u64(x284, 0xffffffffffffffffL, &x294);
  { uint64_t x297;  uint64_t x296 = _mulx_u64(x284, 0xffffffffffffffffL, &x297);
  { uint64_t x300;  uint64_t x299 = _mulx_u64(x284, 0xffffffffffffffffL, &x300);
  { uint64_t x302; uint8_t x303 = _addcarryx_u64(0x0, x288, x290, &x302);
  { uint64_t x305; uint8_t x306 = _addcarryx_u64(x303, x291, x293, &x305);
  { uint64_t x308; uint8_t x309 = _addcarryx_u64(x306, x294, x296, &x308);
  { uint64_t x311; uint8_t x312 = _addcarryx_u64(x309, x297, x299, &x311);
  { uint64_t x314; uint8_t x315 = _addcarryx_u64(x312, x300, x284, &x314);
  { uint64_t _; uint8_t x318 = _addcarryx_u64(0x0, x263, x287, &_);
  { uint64_t x320; uint8_t x321 = _addcarryx_u64(x318, x266, x302, &x320);
  { uint64_t x323; uint8_t x324 = _addcarryx_u64(x321, x269, x305, &x323);
  { uint64_t x326; uint8_t x327 = _addcarryx_u64(x324, x272, x308, &x326);
  { uint64_t x329; uint8_t x330 = _addcarryx_u64(x327, x275, x311, &x329);
  { uint64_t x332; uint8_t x333 = _addcarryx_u64(x330, x278, x314, &x332);
  { uint64_t x335; uint8_t x336 = _addcarryx_u64(x333, x281, x315, &x335);
  { uint8_t x337 = (x336 + x282);
  { uint64_t x340;  uint64_t x339 = _mulx_u64(x11, x15, &x340);
  { uint64_t x343;  uint64_t x342 = _mulx_u64(x11, x17, &x343);
  { uint64_t x346;  uint64_t x345 = _mulx_u64(x11, x19, &x346);
  { uint64_t x349;  uint64_t x348 = _mulx_u64(x11, x21, &x349);
  { uint64_t x352;  uint64_t x351 = _mulx_u64(x11, x23, &x352);
  { uint64_t x355;  uint64_t x354 = _mulx_u64(x11, x22, &x355);
  { uint64_t x357; uint8_t x358 = _addcarryx_u64(0x0, x340, x342, &x357);
  { uint64_t x360; uint8_t x361 = _addcarryx_u64(x358, x343, x345, &x360);
  { uint64_t x363; uint8_t x364 = _addcarryx_u64(x361, x346, x348, &x363);
  { uint64_t x366; uint8_t x367 = _addcarryx_u64(x364, x349, x351, &x366);
  { uint64_t x369; uint8_t x370 = _addcarryx_u64(x367, x352, x354, &x369);
  { uint64_t x372; uint8_t _ = _addcarryx_u64(0x0, x370, x355, &x372);
  { uint64_t x375; uint8_t x376 = _addcarryx_u64(0x0, x320, x339, &x375);
  { uint64_t x378; uint8_t x379 = _addcarryx_u64(x376, x323, x357, &x378);
  { uint64_t x381; uint8_t x382 = _addcarryx_u64(x379, x326, x360, &x381);
  { uint64_t x384; uint8_t x385 = _addcarryx_u64(x382, x329, x363, &x384);
  { uint64_t x387; uint8_t x388 = _addcarryx_u64(x385, x332, x366, &x387);
  { uint64_t x390; uint8_t x391 = _addcarryx_u64(x388, x335, x369, &x390);
  { uint64_t x393; uint8_t x394 = _addcarryx_u64(x391, x337, x372, &x393);
  { uint64_t _;  uint64_t x396 = _mulx_u64(x375, 0x8e38e38e38e38e39L, &_);
  { uint64_t x400;  uint64_t x399 = _mulx_u64(x396, 0xfffffffffffffff7L, &x400);
  { uint64_t x403;  uint64_t x402 = _mulx_u64(x396, 0xffffffffffffffffL, &x403);
  { uint64_t x406;  uint64_t x405 = _mulx_u64(x396, 0xffffffffffffffffL, &x406);
  { uint64_t x409;  uint64_t x408 = _mulx_u64(x396, 0xffffffffffffffffL, &x409);
  { uint64_t x412;  uint64_t x411 = _mulx_u64(x396, 0xffffffffffffffffL, &x412);
  { uint64_t x414; uint8_t x415 = _addcarryx_u64(0x0, x400, x402, &x414);
  { uint64_t x417; uint8_t x418 = _addcarryx_u64(x415, x403, x405, &x417);
  { uint64_t x420; uint8_t x421 = _addcarryx_u64(x418, x406, x408, &x420);
  { uint64_t x423; uint8_t x424 = _addcarryx_u64(x421, x409, x411, &x423);
  { uint64_t x426; uint8_t x427 = _addcarryx_u64(x424, x412, x396, &x426);
  { uint64_t _; uint8_t x430 = _addcarryx_u64(0x0, x375, x399, &_);
  { uint64_t x432; uint8_t x433 = _addcarryx_u64(x430, x378, x414, &x432);
  { uint64_t x435; uint8_t x436 = _addcarryx_u64(x433, x381, x417, &x435);
  { uint64_t x438; uint8_t x439 = _addcarryx_u64(x436, x384, x420, &x438);
  { uint64_t x441; uint8_t x442 = _addcarryx_u64(x439, x387, x423, &x441);
  { uint64_t x444; uint8_t x445 = _addcarryx_u64(x442, x390, x426, &x444);
  { uint64_t x447; uint8_t x448 = _addcarryx_u64(x445, x393, x427, &x447);
  { uint8_t x449 = (x448 + x394);
  { uint64_t x452;  uint64_t x451 = _mulx_u64(x13, x15, &x452);
  { uint64_t x455;  uint64_t x454 = _mulx_u64(x13, x17, &x455);
  { uint64_t x458;  uint64_t x457 = _mulx_u64(x13, x19, &x458);
  { uint64_t x461;  uint64_t x460 = _mulx_u64(x13, x21, &x461);
  { uint64_t x464;  uint64_t x463 = _mulx_u64(x13, x23, &x464);
  { uint64_t x467;  uint64_t x466 = _mulx_u64(x13, x22, &x467);
  { uint64_t x469; uint8_t x470 = _addcarryx_u64(0x0, x452, x454, &x469);
  { uint64_t x472; uint8_t x473 = _addcarryx_u64(x470, x455, x457, &x472);
  { uint64_t x475; uint8_t x476 = _addcarryx_u64(x473, x458, x460, &x475);
  { uint64_t x478; uint8_t x479 = _addcarryx_u64(x476, x461, x463, &x478);
  { uint64_t x481; uint8_t x482 = _addcarryx_u64(x479, x464, x466, &x481);
  { uint64_t x484; uint8_t _ = _addcarryx_u64(0x0, x482, x467, &x484);
  { uint64_t x487; uint8_t x488 = _addcarryx_u64(0x0, x432, x451, &x487);
  { uint64_t x490; uint8_t x491 = _addcarryx_u64(x488, x435, x469, &x490);
  { uint64_t x493; uint8_t x494 = _addcarryx_u64(x491, x438, x472, &x493);
  { uint64_t x496; uint8_t x497 = _addcarryx_u64(x494, x441, x475, &x496);
  { uint64_t x499; uint8_t x500 = _addcarryx_u64(x497, x444, x478, &x499);
  { uint64_t x502; uint8_t x503 = _addcarryx_u64(x500, x447, x481, &x502);
  { uint64_t x505; uint8_t x506 = _addcarryx_u64(x503, x449, x484, &x505);
  { uint64_t _;  uint64_t x508 = _mulx_u64(x487, 0x8e38e38e38e38e39L, &_);
  { uint64_t x512;  uint64_t x511 = _mulx_u64(x508, 0xfffffffffffffff7L, &x512);
  { uint64_t x515;  uint64_t x514 = _mulx_u64(x508, 0xffffffffffffffffL, &x515);
  { uint64_t x518;  uint64_t x517 = _mulx_u64(x508, 0xffffffffffffffffL, &x518);
  { uint64_t x521;  uint64_t x520 = _mulx_u64(x508, 0xffffffffffffffffL, &x521);
  { uint64_t x524;  uint64_t x523 = _mulx_u64(x508, 0xffffffffffffffffL, &x524);
  { uint64_t x526; uint8_t x527 = _addcarryx_u64(0x0, x512, x514, &x526);
  { uint64_t x529; uint8_t x530 = _addcarryx_u64(x527, x515, x517, &x529);
  { uint64_t x532; uint8_t x533 = _addcarryx_u64(x530, x518, x520, &x532);
  { uint64_t x535; uint8_t x536 = _addcarryx_u64(x533, x521, x523, &x535);
  { uint64_t x538; uint8_t x539 = _addcarryx_u64(x536, x524, x508, &x538);
  { uint64_t _; uint8_t x542 = _addcarryx_u64(0x0, x487, x511, &_);
  { uint64_t x544; uint8_t x545 = _addcarryx_u64(x542, x490, x526, &x544);
  { uint64_t x547; uint8_t x548 = _addcarryx_u64(x545, x493, x529, &x547);
  { uint64_t x550; uint8_t x551 = _addcarryx_u64(x548, x496, x532, &x550);
  { uint64_t x553; uint8_t x554 = _addcarryx_u64(x551, x499, x535, &x553);
  { uint64_t x556; uint8_t x557 = _addcarryx_u64(x554, x502, x538, &x556);
  { uint64_t x559; uint8_t x560 = _addcarryx_u64(x557, x505, x539, &x559);
  { uint8_t x561 = (x560 + x506);
  { uint64_t x564;  uint64_t x563 = _mulx_u64(x12, x15, &x564);
  { uint64_t x567;  uint64_t x566 = _mulx_u64(x12, x17, &x567);
  { uint64_t x570;  uint64_t x569 = _mulx_u64(x12, x19, &x570);
  { uint64_t x573;  uint64_t x572 = _mulx_u64(x12, x21, &x573);
  { uint64_t x576;  uint64_t x575 = _mulx_u64(x12, x23, &x576);
  { uint64_t x579;  uint64_t x578 = _mulx_u64(x12, x22, &x579);
  { uint64_t x581; uint8_t x582 = _addcarryx_u64(0x0, x564, x566, &x581);
  { uint64_t x584; uint8_t x585 = _addcarryx_u64(x582, x567, x569, &x584);
  { uint64_t x587; uint8_t x588 = _addcarryx_u64(x585, x570, x572, &x587);
  { uint64_t x590; uint8_t x591 = _addcarryx_u64(x588, x573, x575, &x590);
  { uint64_t x593; uint8_t x594 = _addcarryx_u64(x591, x576, x578, &x593);
  { uint64_t x596; uint8_t _ = _addcarryx_u64(0x0, x594, x579, &x596);
  { uint64_t x599; uint8_t x600 = _addcarryx_u64(0x0, x544, x563, &x599);
  { uint64_t x602; uint8_t x603 = _addcarryx_u64(x600, x547, x581, &x602);
  { uint64_t x605; uint8_t x606 = _addcarryx_u64(x603, x550, x584, &x605);
  { uint64_t x608; uint8_t x609 = _addcarryx_u64(x606, x553, x587, &x608);
  { uint64_t x611; uint8_t x612 = _addcarryx_u64(x609, x556, x590, &x611);
  { uint64_t x614; uint8_t x615 = _addcarryx_u64(x612, x559, x593, &x614);
  { uint64_t x617; uint8_t x618 = _addcarryx_u64(x615, x561, x596, &x617);
  { uint64_t _;  uint64_t x620 = _mulx_u64(x599, 0x8e38e38e38e38e39L, &_);
  { uint64_t x624;  uint64_t x623 = _mulx_u64(x620, 0xfffffffffffffff7L, &x624);
  { uint64_t x627;  uint64_t x626 = _mulx_u64(x620, 0xffffffffffffffffL, &x627);
  { uint64_t x630;  uint64_t x629 = _mulx_u64(x620, 0xffffffffffffffffL, &x630);
  { uint64_t x633;  uint64_t x632 = _mulx_u64(x620, 0xffffffffffffffffL, &x633);
  { uint64_t x636;  uint64_t x635 = _mulx_u64(x620, 0xffffffffffffffffL, &x636);
  { uint64_t x638; uint8_t x639 = _addcarryx_u64(0x0, x624, x626, &x638);
  { uint64_t x641; uint8_t x642 = _addcarryx_u64(x639, x627, x629, &x641);
  { uint64_t x644; uint8_t x645 = _addcarryx_u64(x642, x630, x632, &x644);
  { uint64_t x647; uint8_t x648 = _addcarryx_u64(x645, x633, x635, &x647);
  { uint64_t x650; uint8_t x651 = _addcarryx_u64(x648, x636, x620, &x650);
  { uint64_t _; uint8_t x654 = _addcarryx_u64(0x0, x599, x623, &_);
  { uint64_t x656; uint8_t x657 = _addcarryx_u64(x654, x602, x638, &x656);
  { uint64_t x659; uint8_t x660 = _addcarryx_u64(x657, x605, x641, &x659);
  { uint64_t x662; uint8_t x663 = _addcarryx_u64(x660, x608, x644, &x662);
  { uint64_t x665; uint8_t x666 = _addcarryx_u64(x663, x611, x647, &x665);
  { uint64_t x668; uint8_t x669 = _addcarryx_u64(x666, x614, x650, &x668);
  { uint64_t x671; uint8_t x672 = _addcarryx_u64(x669, x617, x651, &x671);
  { uint8_t x673 = (x672 + x618);
  { uint64_t x675; uint8_t x676 = _subborrow_u64(0x0, x656, 0xfffffffffffffff7L, &x675);
  { uint64_t x678; uint8_t x679 = _subborrow_u64(x676, x659, 0xffffffffffffffffL, &x678);
  { uint64_t x681; uint8_t x682 = _subborrow_u64(x679, x662, 0xffffffffffffffffL, &x681);
  { uint64_t x684; uint8_t x685 = _subborrow_u64(x682, x665, 0xffffffffffffffffL, &x684);
  { uint64_t x687; uint8_t x688 = _subborrow_u64(x685, x668, 0xffffffffffffffffL, &x687);
  { uint64_t x690; uint8_t x691 = _subborrow_u64(x688, x671, 0x1, &x690);
  { uint64_t _; uint8_t x694 = _subborrow_u64(x691, x673, 0x0, &_);
  { uint64_t x695 = cmovznz64(x694, x690, x671);
  { uint64_t x696 = cmovznz64(x694, x687, x668);
  { uint64_t x697 = cmovznz64(x694, x684, x665);
  { uint64_t x698 = cmovznz64(x694, x681, x662);
  { uint64_t x699 = cmovznz64(x694, x678, x659);
  { uint64_t x700 = cmovznz64(x694, x675, x656);
  out[0] = x700;
  out[1] = x699;
  out[2] = x698;
  out[3] = x697;
  out[4] = x696;
  out[5] = x695;
  }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}
}