forked from mit-plv/fiat-crypto
-
Notifications
You must be signed in to change notification settings - Fork 0
/
secp256k1_32.c
5662 lines (5614 loc) · 277 KB
/
secp256k1_32.c
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
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
/* Autogenerated: 'src/ExtractionOCaml/bedrock2_word_by_word_montgomery' --lang bedrock2 --static --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select --no-field-element-typedefs secp256k1 32 '2^256 - 2^32 - 977' mul square add sub opp from_montgomery to_montgomery nonzero selectznz to_bytes from_bytes one msat divstep divstep_precomp */
/* curve description: secp256k1 */
/* 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 = 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2f (from "2^256 - 2^32 - 977") */
/* */
/* 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) + (z[7] << 224) */
/* bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) */
/* twos_complement_eval z = let x1 := z[0] + (z[1] << 32) + (z[2] << 64) + (z[3] << 96) + (z[4] << 128) + (z[5] << 160) + (z[6] << 192) + (z[7] << 224) in */
/* if x1 & (2^256-1) < 2^255 then x1 & (2^256-1) else (x1 & (2^256-1)) - 2^256 */
#include <stdint.h>
#include <string.h>
// We use memcpy to work around -fstrict-aliasing.
// A plain memcpy is enough on clang 10, but not on gcc 10, which fails
// to infer the bounds on an integer loaded by memcpy.
// Adding a range mask after memcpy in turn makes slower code in clang.
// Loading individual bytes, shifting them together, and or-ing is fast
// on clang and sometimes on GCC, but other times GCC inlines individual
// byte operations without reconstructing wider accesses.
// The little-endian idiom below seems fast in gcc 9+ and clang 10.
static __attribute__((always_inline)) inline uintptr_t
_br2_load(uintptr_t a, uintptr_t sz) {
switch (sz) {
case 1: { uint8_t r = 0; memcpy(&r, (void*)a, 1); return r; }
case 2: { uint16_t r = 0; memcpy(&r, (void*)a, 2); return r; }
case 4: { uint32_t r = 0; memcpy(&r, (void*)a, 4); return r; }
case 8: { uint64_t r = 0; memcpy(&r, (void*)a, 8); return r; }
default: __builtin_unreachable();
}
}
static __attribute__((always_inline)) inline void
_br2_store(uintptr_t a, uintptr_t v, uintptr_t sz) {
memcpy((void*)a, &v, sz);
}
/*
* Input Bounds:
* in0: [[0x0 ~> 0xffffffff], [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], [0x0 ~> 0xffffffff]]
* Output Bounds:
* out0: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
*/
static
void internal_fiat_secp256k1_mul(uintptr_t out0, uintptr_t in0, uintptr_t in1) {
uintptr_t x1, x2, x3, x4, x5, x6, x7, x0, x23, x36, x39, x41, x37, x42, x34, x43, x45, x46, x35, x47, x32, x48, x50, x51, x33, x52, x30, x53, x55, x56, x31, x57, x28, x58, x60, x61, x29, x62, x26, x63, x65, x66, x27, x67, x24, x68, x70, x71, x25, x73, x86, x89, x91, x87, x92, x84, x93, x95, x96, x85, x97, x82, x98, x100, x101, x83, x102, x80, x103, x105, x106, x81, x107, x78, x108, x110, x111, x79, x112, x76, x113, x115, x116, x77, x117, x74, x118, x120, x121, x75, x88, x123, x38, x124, x40, x125, x90, x126, x128, x129, x44, x130, x94, x131, x133, x134, x49, x135, x99, x136, x138, x139, x54, x140, x104, x141, x143, x144, x59, x145, x109, x146, x148, x149, x64, x150, x114, x151, x153, x154, x69, x155, x119, x156, x158, x159, x72, x160, x122, x161, x163, x16, x177, x180, x182, x178, x183, x175, x184, x186, x187, x176, x188, x173, x189, x191, x192, x174, x193, x171, x194, x196, x197, x172, x198, x169, x199, x201, x202, x170, x203, x167, x204, x206, x207, x168, x208, x165, x209, x211, x212, x166, x179, x127, x215, x132, x216, x181, x217, x219, x220, x137, x221, x185, x222, x224, x225, x142, x226, x190, x227, x229, x230, x147, x231, x195, x232, x234, x235, x152, x236, x200, x237, x239, x240, x157, x241, x205, x242, x244, x245, x162, x246, x210, x247, x249, x250, x164, x251, x213, x252, x254, x256, x269, x272, x274, x270, x275, x267, x276, x278, x279, x268, x280, x265, x281, x283, x284, x266, x285, x263, x286, x288, x289, x264, x290, x261, x291, x293, x294, x262, x295, x259, x296, x298, x299, x260, x300, x257, x301, x303, x304, x258, x271, x306, x214, x307, x218, x308, x273, x309, x311, x312, x223, x313, x277, x314, x316, x317, x228, x318, x282, x319, x321, x322, x233, x323, x287, x324, x326, x327, x238, x328, x292, x329, x331, x332, x243, x333, x297, x334, x336, x337, x248, x338, x302, x339, x341, x342, x253, x343, x305, x344, x346, x347, x255, x17, x361, x364, x366, x362, x367, x359, x368, x370, x371, x360, x372, x357, x373, x375, x376, x358, x377, x355, x378, x380, x381, x356, x382, x353, x383, x385, x386, x354, x387, x351, x388, x390, x391, x352, x392, x349, x393, x395, x396, x350, x363, x310, x399, x315, x400, x365, x401, x403, x404, x320, x405, x369, x406, x408, x409, x325, x410, x374, x411, x413, x414, x330, x415, x379, x416, x418, x419, x335, x420, x384, x421, x423, x424, x340, x425, x389, x426, x428, x429, x345, x430, x394, x431, x433, x434, x348, x435, x397, x436, x438, x440, x453, x456, x458, x454, x459, x451, x460, x462, x463, x452, x464, x449, x465, x467, x468, x450, x469, x447, x470, x472, x473, x448, x474, x445, x475, x477, x478, x446, x479, x443, x480, x482, x483, x444, x484, x441, x485, x487, x488, x442, x455, x490, x398, x491, x402, x492, x457, x493, x495, x496, x407, x497, x461, x498, x500, x501, x412, x502, x466, x503, x505, x506, x417, x507, x471, x508, x510, x511, x422, x512, x476, x513, x515, x516, x427, x517, x481, x518, x520, x521, x432, x522, x486, x523, x525, x526, x437, x527, x489, x528, x530, x531, x439, x18, x545, x548, x550, x546, x551, x543, x552, x554, x555, x544, x556, x541, x557, x559, x560, x542, x561, x539, x562, x564, x565, x540, x566, x537, x567, x569, x570, x538, x571, x535, x572, x574, x575, x536, x576, x533, x577, x579, x580, x534, x547, x494, x583, x499, x584, x549, x585, x587, x588, x504, x589, x553, x590, x592, x593, x509, x594, x558, x595, x597, x598, x514, x599, x563, x600, x602, x603, x519, x604, x568, x605, x607, x608, x524, x609, x573, x610, x612, x613, x529, x614, x578, x615, x617, x618, x532, x619, x581, x620, x622, x624, x637, x640, x642, x638, x643, x635, x644, x646, x647, x636, x648, x633, x649, x651, x652, x634, x653, x631, x654, x656, x657, x632, x658, x629, x659, x661, x662, x630, x663, x627, x664, x666, x667, x628, x668, x625, x669, x671, x672, x626, x639, x674, x582, x675, x586, x676, x641, x677, x679, x680, x591, x681, x645, x682, x684, x685, x596, x686, x650, x687, x689, x690, x601, x691, x655, x692, x694, x695, x606, x696, x660, x697, x699, x700, x611, x701, x665, x702, x704, x705, x616, x706, x670, x707, x709, x710, x621, x711, x673, x712, x714, x715, x623, x19, x729, x732, x734, x730, x735, x727, x736, x738, x739, x728, x740, x725, x741, x743, x744, x726, x745, x723, x746, x748, x749, x724, x750, x721, x751, x753, x754, x722, x755, x719, x756, x758, x759, x720, x760, x717, x761, x763, x764, x718, x731, x678, x767, x683, x768, x733, x769, x771, x772, x688, x773, x737, x774, x776, x777, x693, x778, x742, x779, x781, x782, x698, x783, x747, x784, x786, x787, x703, x788, x752, x789, x791, x792, x708, x793, x757, x794, x796, x797, x713, x798, x762, x799, x801, x802, x716, x803, x765, x804, x806, x808, x821, x824, x826, x822, x827, x819, x828, x830, x831, x820, x832, x817, x833, x835, x836, x818, x837, x815, x838, x840, x841, x816, x842, x813, x843, x845, x846, x814, x847, x811, x848, x850, x851, x812, x852, x809, x853, x855, x856, x810, x823, x858, x766, x859, x770, x860, x825, x861, x863, x864, x775, x865, x829, x866, x868, x869, x780, x870, x834, x871, x873, x874, x785, x875, x839, x876, x878, x879, x790, x880, x844, x881, x883, x884, x795, x885, x849, x886, x888, x889, x800, x890, x854, x891, x893, x894, x805, x895, x857, x896, x898, x899, x807, x20, x913, x916, x918, x914, x919, x911, x920, x922, x923, x912, x924, x909, x925, x927, x928, x910, x929, x907, x930, x932, x933, x908, x934, x905, x935, x937, x938, x906, x939, x903, x940, x942, x943, x904, x944, x901, x945, x947, x948, x902, x915, x862, x951, x867, x952, x917, x953, x955, x956, x872, x957, x921, x958, x960, x961, x877, x962, x926, x963, x965, x966, x882, x967, x931, x968, x970, x971, x887, x972, x936, x973, x975, x976, x892, x977, x941, x978, x980, x981, x897, x982, x946, x983, x985, x986, x900, x987, x949, x988, x990, x992, x1005, x1008, x1010, x1006, x1011, x1003, x1012, x1014, x1015, x1004, x1016, x1001, x1017, x1019, x1020, x1002, x1021, x999, x1022, x1024, x1025, x1000, x1026, x997, x1027, x1029, x1030, x998, x1031, x995, x1032, x1034, x1035, x996, x1036, x993, x1037, x1039, x1040, x994, x1007, x1042, x950, x1043, x954, x1044, x1009, x1045, x1047, x1048, x959, x1049, x1013, x1050, x1052, x1053, x964, x1054, x1018, x1055, x1057, x1058, x969, x1059, x1023, x1060, x1062, x1063, x974, x1064, x1028, x1065, x1067, x1068, x979, x1069, x1033, x1070, x1072, x1073, x984, x1074, x1038, x1075, x1077, x1078, x989, x1079, x1041, x1080, x1082, x1083, x991, x21, x1097, x1100, x1102, x1098, x1103, x1095, x1104, x1106, x1107, x1096, x1108, x1093, x1109, x1111, x1112, x1094, x1113, x1091, x1114, x1116, x1117, x1092, x1118, x1089, x1119, x1121, x1122, x1090, x1123, x1087, x1124, x1126, x1127, x1088, x1128, x1085, x1129, x1131, x1132, x1086, x1099, x1046, x1135, x1051, x1136, x1101, x1137, x1139, x1140, x1056, x1141, x1105, x1142, x1144, x1145, x1061, x1146, x1110, x1147, x1149, x1150, x1066, x1151, x1115, x1152, x1154, x1155, x1071, x1156, x1120, x1157, x1159, x1160, x1076, x1161, x1125, x1162, x1164, x1165, x1081, x1166, x1130, x1167, x1169, x1170, x1084, x1171, x1133, x1172, x1174, x1176, x1189, x1192, x1194, x1190, x1195, x1187, x1196, x1198, x1199, x1188, x1200, x1185, x1201, x1203, x1204, x1186, x1205, x1183, x1206, x1208, x1209, x1184, x1210, x1181, x1211, x1213, x1214, x1182, x1215, x1179, x1216, x1218, x1219, x1180, x1220, x1177, x1221, x1223, x1224, x1178, x1191, x1226, x1134, x1227, x1138, x1228, x1193, x1229, x1231, x1232, x1143, x1233, x1197, x1234, x1236, x1237, x1148, x1238, x1202, x1239, x1241, x1242, x1153, x1243, x1207, x1244, x1246, x1247, x1158, x1248, x1212, x1249, x1251, x1252, x1163, x1253, x1217, x1254, x1256, x1257, x1168, x1258, x1222, x1259, x1261, x1262, x1173, x1263, x1225, x1264, x1266, x1267, x1175, x15, x14, x13, x12, x11, x10, x9, x22, x8, x1281, x1284, x1286, x1282, x1287, x1279, x1288, x1290, x1291, x1280, x1292, x1277, x1293, x1295, x1296, x1278, x1297, x1275, x1298, x1300, x1301, x1276, x1302, x1273, x1303, x1305, x1306, x1274, x1307, x1271, x1308, x1310, x1311, x1272, x1312, x1269, x1313, x1315, x1316, x1270, x1283, x1230, x1319, x1235, x1320, x1285, x1321, x1323, x1324, x1240, x1325, x1289, x1326, x1328, x1329, x1245, x1330, x1294, x1331, x1333, x1334, x1250, x1335, x1299, x1336, x1338, x1339, x1255, x1340, x1304, x1341, x1343, x1344, x1260, x1345, x1309, x1346, x1348, x1349, x1265, x1350, x1314, x1351, x1353, x1354, x1268, x1355, x1317, x1356, x1358, x1360, x1373, x1376, x1378, x1374, x1379, x1371, x1380, x1382, x1383, x1372, x1384, x1369, x1385, x1387, x1388, x1370, x1389, x1367, x1390, x1392, x1393, x1368, x1394, x1365, x1395, x1397, x1398, x1366, x1399, x1363, x1400, x1402, x1403, x1364, x1404, x1361, x1405, x1407, x1408, x1362, x1375, x1410, x1318, x1411, x1322, x1412, x1377, x1413, x1415, x1416, x1327, x1417, x1381, x1418, x1420, x1421, x1332, x1422, x1386, x1423, x1425, x1426, x1337, x1427, x1391, x1428, x1430, x1431, x1342, x1432, x1396, x1433, x1435, x1436, x1347, x1437, x1401, x1438, x1440, x1441, x1352, x1442, x1406, x1443, x1445, x1446, x1357, x1447, x1409, x1448, x1450, x1451, x1359, x1454, x1455, x1456, x1458, x1459, x1460, x1461, x1463, x1464, x1465, x1466, x1468, x1469, x1470, x1471, x1473, x1474, x1475, x1476, x1478, x1479, x1480, x1481, x1483, x1484, x1485, x1486, x1488, x1489, x1452, x1490, x1414, x1492, x1453, x1493, x1419, x1495, x1457, x1496, x1424, x1498, x1462, x1499, x1429, x1501, x1467, x1502, x1434, x1504, x1472, x1505, x1439, x1507, x1477, x1508, x1444, x1510, x1482, x1511, x1491, x1449, x1513, x1487, x1514, x1494, x1497, x1500, x1503, x1506, x1509, x1512, x1515, x1516, x1517, x1518, x1519, x1520, x1521, x1522, x1523;
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));
x7 = _br2_load((in0)+((uintptr_t)28ULL), sizeof(uintptr_t));
/*skip*/
x8 = _br2_load((in1)+((uintptr_t)0ULL), sizeof(uintptr_t));
x9 = _br2_load((in1)+((uintptr_t)4ULL), sizeof(uintptr_t));
x10 = _br2_load((in1)+((uintptr_t)8ULL), sizeof(uintptr_t));
x11 = _br2_load((in1)+((uintptr_t)12ULL), sizeof(uintptr_t));
x12 = _br2_load((in1)+((uintptr_t)16ULL), sizeof(uintptr_t));
x13 = _br2_load((in1)+((uintptr_t)20ULL), sizeof(uintptr_t));
x14 = _br2_load((in1)+((uintptr_t)24ULL), sizeof(uintptr_t));
x15 = _br2_load((in1)+((uintptr_t)28ULL), sizeof(uintptr_t));
/*skip*/
/*skip*/
x16 = x1;
x17 = x2;
x18 = x3;
x19 = x4;
x20 = x5;
x21 = x6;
x22 = x7;
x23 = x0;
x24 = (x23)*(x15);
x25 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x23)*(x15))>>32 : ((__uint128_t)(x23)*(x15))>>64);
x26 = (x23)*(x14);
x27 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x23)*(x14))>>32 : ((__uint128_t)(x23)*(x14))>>64);
x28 = (x23)*(x13);
x29 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x23)*(x13))>>32 : ((__uint128_t)(x23)*(x13))>>64);
x30 = (x23)*(x12);
x31 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x23)*(x12))>>32 : ((__uint128_t)(x23)*(x12))>>64);
x32 = (x23)*(x11);
x33 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x23)*(x11))>>32 : ((__uint128_t)(x23)*(x11))>>64);
x34 = (x23)*(x10);
x35 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x23)*(x10))>>32 : ((__uint128_t)(x23)*(x10))>>64);
x36 = (x23)*(x9);
x37 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x23)*(x9))>>32 : ((__uint128_t)(x23)*(x9))>>64);
x38 = (x23)*(x8);
x39 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x23)*(x8))>>32 : ((__uint128_t)(x23)*(x8))>>64);
x40 = (x39)+(x36);
x41 = (uintptr_t)((x40)<(x39));
x42 = (x41)+(x37);
x43 = (uintptr_t)((x42)<(x37));
x44 = (x42)+(x34);
x45 = (uintptr_t)((x44)<(x34));
x46 = (x43)+(x45);
x47 = (x46)+(x35);
x48 = (uintptr_t)((x47)<(x35));
x49 = (x47)+(x32);
x50 = (uintptr_t)((x49)<(x32));
x51 = (x48)+(x50);
x52 = (x51)+(x33);
x53 = (uintptr_t)((x52)<(x33));
x54 = (x52)+(x30);
x55 = (uintptr_t)((x54)<(x30));
x56 = (x53)+(x55);
x57 = (x56)+(x31);
x58 = (uintptr_t)((x57)<(x31));
x59 = (x57)+(x28);
x60 = (uintptr_t)((x59)<(x28));
x61 = (x58)+(x60);
x62 = (x61)+(x29);
x63 = (uintptr_t)((x62)<(x29));
x64 = (x62)+(x26);
x65 = (uintptr_t)((x64)<(x26));
x66 = (x63)+(x65);
x67 = (x66)+(x27);
x68 = (uintptr_t)((x67)<(x27));
x69 = (x67)+(x24);
x70 = (uintptr_t)((x69)<(x24));
x71 = (x68)+(x70);
x72 = (x71)+(x25);
x73 = (x38)*((uintptr_t)3525653809ULL);
x74 = (x73)*((uintptr_t)4294967295ULL);
x75 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x73)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x73)*((uintptr_t)4294967295ULL))>>64);
x76 = (x73)*((uintptr_t)4294967295ULL);
x77 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x73)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x73)*((uintptr_t)4294967295ULL))>>64);
x78 = (x73)*((uintptr_t)4294967295ULL);
x79 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x73)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x73)*((uintptr_t)4294967295ULL))>>64);
x80 = (x73)*((uintptr_t)4294967295ULL);
x81 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x73)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x73)*((uintptr_t)4294967295ULL))>>64);
x82 = (x73)*((uintptr_t)4294967295ULL);
x83 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x73)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x73)*((uintptr_t)4294967295ULL))>>64);
x84 = (x73)*((uintptr_t)4294967295ULL);
x85 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x73)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x73)*((uintptr_t)4294967295ULL))>>64);
x86 = (x73)*((uintptr_t)4294967294ULL);
x87 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x73)*((uintptr_t)4294967294ULL))>>32 : ((__uint128_t)(x73)*((uintptr_t)4294967294ULL))>>64);
x88 = (x73)*((uintptr_t)4294966319ULL);
x89 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x73)*((uintptr_t)4294966319ULL))>>32 : ((__uint128_t)(x73)*((uintptr_t)4294966319ULL))>>64);
x90 = (x89)+(x86);
x91 = (uintptr_t)((x90)<(x89));
x92 = (x91)+(x87);
x93 = (uintptr_t)((x92)<(x87));
x94 = (x92)+(x84);
x95 = (uintptr_t)((x94)<(x84));
x96 = (x93)+(x95);
x97 = (x96)+(x85);
x98 = (uintptr_t)((x97)<(x85));
x99 = (x97)+(x82);
x100 = (uintptr_t)((x99)<(x82));
x101 = (x98)+(x100);
x102 = (x101)+(x83);
x103 = (uintptr_t)((x102)<(x83));
x104 = (x102)+(x80);
x105 = (uintptr_t)((x104)<(x80));
x106 = (x103)+(x105);
x107 = (x106)+(x81);
x108 = (uintptr_t)((x107)<(x81));
x109 = (x107)+(x78);
x110 = (uintptr_t)((x109)<(x78));
x111 = (x108)+(x110);
x112 = (x111)+(x79);
x113 = (uintptr_t)((x112)<(x79));
x114 = (x112)+(x76);
x115 = (uintptr_t)((x114)<(x76));
x116 = (x113)+(x115);
x117 = (x116)+(x77);
x118 = (uintptr_t)((x117)<(x77));
x119 = (x117)+(x74);
x120 = (uintptr_t)((x119)<(x74));
x121 = (x118)+(x120);
x122 = (x121)+(x75);
x123 = (x38)+(x88);
x124 = (uintptr_t)((x123)<(x38));
x125 = (x124)+(x40);
x126 = (uintptr_t)((x125)<(x40));
x127 = (x125)+(x90);
x128 = (uintptr_t)((x127)<(x90));
x129 = (x126)+(x128);
x130 = (x129)+(x44);
x131 = (uintptr_t)((x130)<(x44));
x132 = (x130)+(x94);
x133 = (uintptr_t)((x132)<(x94));
x134 = (x131)+(x133);
x135 = (x134)+(x49);
x136 = (uintptr_t)((x135)<(x49));
x137 = (x135)+(x99);
x138 = (uintptr_t)((x137)<(x99));
x139 = (x136)+(x138);
x140 = (x139)+(x54);
x141 = (uintptr_t)((x140)<(x54));
x142 = (x140)+(x104);
x143 = (uintptr_t)((x142)<(x104));
x144 = (x141)+(x143);
x145 = (x144)+(x59);
x146 = (uintptr_t)((x145)<(x59));
x147 = (x145)+(x109);
x148 = (uintptr_t)((x147)<(x109));
x149 = (x146)+(x148);
x150 = (x149)+(x64);
x151 = (uintptr_t)((x150)<(x64));
x152 = (x150)+(x114);
x153 = (uintptr_t)((x152)<(x114));
x154 = (x151)+(x153);
x155 = (x154)+(x69);
x156 = (uintptr_t)((x155)<(x69));
x157 = (x155)+(x119);
x158 = (uintptr_t)((x157)<(x119));
x159 = (x156)+(x158);
x160 = (x159)+(x72);
x161 = (uintptr_t)((x160)<(x72));
x162 = (x160)+(x122);
x163 = (uintptr_t)((x162)<(x122));
x164 = (x161)+(x163);
x165 = (x16)*(x15);
x166 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x16)*(x15))>>32 : ((__uint128_t)(x16)*(x15))>>64);
x167 = (x16)*(x14);
x168 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x16)*(x14))>>32 : ((__uint128_t)(x16)*(x14))>>64);
x169 = (x16)*(x13);
x170 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x16)*(x13))>>32 : ((__uint128_t)(x16)*(x13))>>64);
x171 = (x16)*(x12);
x172 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x16)*(x12))>>32 : ((__uint128_t)(x16)*(x12))>>64);
x173 = (x16)*(x11);
x174 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x16)*(x11))>>32 : ((__uint128_t)(x16)*(x11))>>64);
x175 = (x16)*(x10);
x176 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x16)*(x10))>>32 : ((__uint128_t)(x16)*(x10))>>64);
x177 = (x16)*(x9);
x178 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x16)*(x9))>>32 : ((__uint128_t)(x16)*(x9))>>64);
x179 = (x16)*(x8);
x180 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x16)*(x8))>>32 : ((__uint128_t)(x16)*(x8))>>64);
x181 = (x180)+(x177);
x182 = (uintptr_t)((x181)<(x180));
x183 = (x182)+(x178);
x184 = (uintptr_t)((x183)<(x178));
x185 = (x183)+(x175);
x186 = (uintptr_t)((x185)<(x175));
x187 = (x184)+(x186);
x188 = (x187)+(x176);
x189 = (uintptr_t)((x188)<(x176));
x190 = (x188)+(x173);
x191 = (uintptr_t)((x190)<(x173));
x192 = (x189)+(x191);
x193 = (x192)+(x174);
x194 = (uintptr_t)((x193)<(x174));
x195 = (x193)+(x171);
x196 = (uintptr_t)((x195)<(x171));
x197 = (x194)+(x196);
x198 = (x197)+(x172);
x199 = (uintptr_t)((x198)<(x172));
x200 = (x198)+(x169);
x201 = (uintptr_t)((x200)<(x169));
x202 = (x199)+(x201);
x203 = (x202)+(x170);
x204 = (uintptr_t)((x203)<(x170));
x205 = (x203)+(x167);
x206 = (uintptr_t)((x205)<(x167));
x207 = (x204)+(x206);
x208 = (x207)+(x168);
x209 = (uintptr_t)((x208)<(x168));
x210 = (x208)+(x165);
x211 = (uintptr_t)((x210)<(x165));
x212 = (x209)+(x211);
x213 = (x212)+(x166);
x214 = (x127)+(x179);
x215 = (uintptr_t)((x214)<(x127));
x216 = (x215)+(x132);
x217 = (uintptr_t)((x216)<(x132));
x218 = (x216)+(x181);
x219 = (uintptr_t)((x218)<(x181));
x220 = (x217)+(x219);
x221 = (x220)+(x137);
x222 = (uintptr_t)((x221)<(x137));
x223 = (x221)+(x185);
x224 = (uintptr_t)((x223)<(x185));
x225 = (x222)+(x224);
x226 = (x225)+(x142);
x227 = (uintptr_t)((x226)<(x142));
x228 = (x226)+(x190);
x229 = (uintptr_t)((x228)<(x190));
x230 = (x227)+(x229);
x231 = (x230)+(x147);
x232 = (uintptr_t)((x231)<(x147));
x233 = (x231)+(x195);
x234 = (uintptr_t)((x233)<(x195));
x235 = (x232)+(x234);
x236 = (x235)+(x152);
x237 = (uintptr_t)((x236)<(x152));
x238 = (x236)+(x200);
x239 = (uintptr_t)((x238)<(x200));
x240 = (x237)+(x239);
x241 = (x240)+(x157);
x242 = (uintptr_t)((x241)<(x157));
x243 = (x241)+(x205);
x244 = (uintptr_t)((x243)<(x205));
x245 = (x242)+(x244);
x246 = (x245)+(x162);
x247 = (uintptr_t)((x246)<(x162));
x248 = (x246)+(x210);
x249 = (uintptr_t)((x248)<(x210));
x250 = (x247)+(x249);
x251 = (x250)+(x164);
x252 = (uintptr_t)((x251)<(x164));
x253 = (x251)+(x213);
x254 = (uintptr_t)((x253)<(x213));
x255 = (x252)+(x254);
x256 = (x214)*((uintptr_t)3525653809ULL);
x257 = (x256)*((uintptr_t)4294967295ULL);
x258 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x256)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x256)*((uintptr_t)4294967295ULL))>>64);
x259 = (x256)*((uintptr_t)4294967295ULL);
x260 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x256)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x256)*((uintptr_t)4294967295ULL))>>64);
x261 = (x256)*((uintptr_t)4294967295ULL);
x262 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x256)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x256)*((uintptr_t)4294967295ULL))>>64);
x263 = (x256)*((uintptr_t)4294967295ULL);
x264 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x256)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x256)*((uintptr_t)4294967295ULL))>>64);
x265 = (x256)*((uintptr_t)4294967295ULL);
x266 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x256)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x256)*((uintptr_t)4294967295ULL))>>64);
x267 = (x256)*((uintptr_t)4294967295ULL);
x268 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x256)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x256)*((uintptr_t)4294967295ULL))>>64);
x269 = (x256)*((uintptr_t)4294967294ULL);
x270 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x256)*((uintptr_t)4294967294ULL))>>32 : ((__uint128_t)(x256)*((uintptr_t)4294967294ULL))>>64);
x271 = (x256)*((uintptr_t)4294966319ULL);
x272 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x256)*((uintptr_t)4294966319ULL))>>32 : ((__uint128_t)(x256)*((uintptr_t)4294966319ULL))>>64);
x273 = (x272)+(x269);
x274 = (uintptr_t)((x273)<(x272));
x275 = (x274)+(x270);
x276 = (uintptr_t)((x275)<(x270));
x277 = (x275)+(x267);
x278 = (uintptr_t)((x277)<(x267));
x279 = (x276)+(x278);
x280 = (x279)+(x268);
x281 = (uintptr_t)((x280)<(x268));
x282 = (x280)+(x265);
x283 = (uintptr_t)((x282)<(x265));
x284 = (x281)+(x283);
x285 = (x284)+(x266);
x286 = (uintptr_t)((x285)<(x266));
x287 = (x285)+(x263);
x288 = (uintptr_t)((x287)<(x263));
x289 = (x286)+(x288);
x290 = (x289)+(x264);
x291 = (uintptr_t)((x290)<(x264));
x292 = (x290)+(x261);
x293 = (uintptr_t)((x292)<(x261));
x294 = (x291)+(x293);
x295 = (x294)+(x262);
x296 = (uintptr_t)((x295)<(x262));
x297 = (x295)+(x259);
x298 = (uintptr_t)((x297)<(x259));
x299 = (x296)+(x298);
x300 = (x299)+(x260);
x301 = (uintptr_t)((x300)<(x260));
x302 = (x300)+(x257);
x303 = (uintptr_t)((x302)<(x257));
x304 = (x301)+(x303);
x305 = (x304)+(x258);
x306 = (x214)+(x271);
x307 = (uintptr_t)((x306)<(x214));
x308 = (x307)+(x218);
x309 = (uintptr_t)((x308)<(x218));
x310 = (x308)+(x273);
x311 = (uintptr_t)((x310)<(x273));
x312 = (x309)+(x311);
x313 = (x312)+(x223);
x314 = (uintptr_t)((x313)<(x223));
x315 = (x313)+(x277);
x316 = (uintptr_t)((x315)<(x277));
x317 = (x314)+(x316);
x318 = (x317)+(x228);
x319 = (uintptr_t)((x318)<(x228));
x320 = (x318)+(x282);
x321 = (uintptr_t)((x320)<(x282));
x322 = (x319)+(x321);
x323 = (x322)+(x233);
x324 = (uintptr_t)((x323)<(x233));
x325 = (x323)+(x287);
x326 = (uintptr_t)((x325)<(x287));
x327 = (x324)+(x326);
x328 = (x327)+(x238);
x329 = (uintptr_t)((x328)<(x238));
x330 = (x328)+(x292);
x331 = (uintptr_t)((x330)<(x292));
x332 = (x329)+(x331);
x333 = (x332)+(x243);
x334 = (uintptr_t)((x333)<(x243));
x335 = (x333)+(x297);
x336 = (uintptr_t)((x335)<(x297));
x337 = (x334)+(x336);
x338 = (x337)+(x248);
x339 = (uintptr_t)((x338)<(x248));
x340 = (x338)+(x302);
x341 = (uintptr_t)((x340)<(x302));
x342 = (x339)+(x341);
x343 = (x342)+(x253);
x344 = (uintptr_t)((x343)<(x253));
x345 = (x343)+(x305);
x346 = (uintptr_t)((x345)<(x305));
x347 = (x344)+(x346);
x348 = (x347)+(x255);
x349 = (x17)*(x15);
x350 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x17)*(x15))>>32 : ((__uint128_t)(x17)*(x15))>>64);
x351 = (x17)*(x14);
x352 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x17)*(x14))>>32 : ((__uint128_t)(x17)*(x14))>>64);
x353 = (x17)*(x13);
x354 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x17)*(x13))>>32 : ((__uint128_t)(x17)*(x13))>>64);
x355 = (x17)*(x12);
x356 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x17)*(x12))>>32 : ((__uint128_t)(x17)*(x12))>>64);
x357 = (x17)*(x11);
x358 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x17)*(x11))>>32 : ((__uint128_t)(x17)*(x11))>>64);
x359 = (x17)*(x10);
x360 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x17)*(x10))>>32 : ((__uint128_t)(x17)*(x10))>>64);
x361 = (x17)*(x9);
x362 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x17)*(x9))>>32 : ((__uint128_t)(x17)*(x9))>>64);
x363 = (x17)*(x8);
x364 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x17)*(x8))>>32 : ((__uint128_t)(x17)*(x8))>>64);
x365 = (x364)+(x361);
x366 = (uintptr_t)((x365)<(x364));
x367 = (x366)+(x362);
x368 = (uintptr_t)((x367)<(x362));
x369 = (x367)+(x359);
x370 = (uintptr_t)((x369)<(x359));
x371 = (x368)+(x370);
x372 = (x371)+(x360);
x373 = (uintptr_t)((x372)<(x360));
x374 = (x372)+(x357);
x375 = (uintptr_t)((x374)<(x357));
x376 = (x373)+(x375);
x377 = (x376)+(x358);
x378 = (uintptr_t)((x377)<(x358));
x379 = (x377)+(x355);
x380 = (uintptr_t)((x379)<(x355));
x381 = (x378)+(x380);
x382 = (x381)+(x356);
x383 = (uintptr_t)((x382)<(x356));
x384 = (x382)+(x353);
x385 = (uintptr_t)((x384)<(x353));
x386 = (x383)+(x385);
x387 = (x386)+(x354);
x388 = (uintptr_t)((x387)<(x354));
x389 = (x387)+(x351);
x390 = (uintptr_t)((x389)<(x351));
x391 = (x388)+(x390);
x392 = (x391)+(x352);
x393 = (uintptr_t)((x392)<(x352));
x394 = (x392)+(x349);
x395 = (uintptr_t)((x394)<(x349));
x396 = (x393)+(x395);
x397 = (x396)+(x350);
x398 = (x310)+(x363);
x399 = (uintptr_t)((x398)<(x310));
x400 = (x399)+(x315);
x401 = (uintptr_t)((x400)<(x315));
x402 = (x400)+(x365);
x403 = (uintptr_t)((x402)<(x365));
x404 = (x401)+(x403);
x405 = (x404)+(x320);
x406 = (uintptr_t)((x405)<(x320));
x407 = (x405)+(x369);
x408 = (uintptr_t)((x407)<(x369));
x409 = (x406)+(x408);
x410 = (x409)+(x325);
x411 = (uintptr_t)((x410)<(x325));
x412 = (x410)+(x374);
x413 = (uintptr_t)((x412)<(x374));
x414 = (x411)+(x413);
x415 = (x414)+(x330);
x416 = (uintptr_t)((x415)<(x330));
x417 = (x415)+(x379);
x418 = (uintptr_t)((x417)<(x379));
x419 = (x416)+(x418);
x420 = (x419)+(x335);
x421 = (uintptr_t)((x420)<(x335));
x422 = (x420)+(x384);
x423 = (uintptr_t)((x422)<(x384));
x424 = (x421)+(x423);
x425 = (x424)+(x340);
x426 = (uintptr_t)((x425)<(x340));
x427 = (x425)+(x389);
x428 = (uintptr_t)((x427)<(x389));
x429 = (x426)+(x428);
x430 = (x429)+(x345);
x431 = (uintptr_t)((x430)<(x345));
x432 = (x430)+(x394);
x433 = (uintptr_t)((x432)<(x394));
x434 = (x431)+(x433);
x435 = (x434)+(x348);
x436 = (uintptr_t)((x435)<(x348));
x437 = (x435)+(x397);
x438 = (uintptr_t)((x437)<(x397));
x439 = (x436)+(x438);
x440 = (x398)*((uintptr_t)3525653809ULL);
x441 = (x440)*((uintptr_t)4294967295ULL);
x442 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x440)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x440)*((uintptr_t)4294967295ULL))>>64);
x443 = (x440)*((uintptr_t)4294967295ULL);
x444 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x440)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x440)*((uintptr_t)4294967295ULL))>>64);
x445 = (x440)*((uintptr_t)4294967295ULL);
x446 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x440)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x440)*((uintptr_t)4294967295ULL))>>64);
x447 = (x440)*((uintptr_t)4294967295ULL);
x448 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x440)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x440)*((uintptr_t)4294967295ULL))>>64);
x449 = (x440)*((uintptr_t)4294967295ULL);
x450 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x440)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x440)*((uintptr_t)4294967295ULL))>>64);
x451 = (x440)*((uintptr_t)4294967295ULL);
x452 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x440)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x440)*((uintptr_t)4294967295ULL))>>64);
x453 = (x440)*((uintptr_t)4294967294ULL);
x454 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x440)*((uintptr_t)4294967294ULL))>>32 : ((__uint128_t)(x440)*((uintptr_t)4294967294ULL))>>64);
x455 = (x440)*((uintptr_t)4294966319ULL);
x456 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x440)*((uintptr_t)4294966319ULL))>>32 : ((__uint128_t)(x440)*((uintptr_t)4294966319ULL))>>64);
x457 = (x456)+(x453);
x458 = (uintptr_t)((x457)<(x456));
x459 = (x458)+(x454);
x460 = (uintptr_t)((x459)<(x454));
x461 = (x459)+(x451);
x462 = (uintptr_t)((x461)<(x451));
x463 = (x460)+(x462);
x464 = (x463)+(x452);
x465 = (uintptr_t)((x464)<(x452));
x466 = (x464)+(x449);
x467 = (uintptr_t)((x466)<(x449));
x468 = (x465)+(x467);
x469 = (x468)+(x450);
x470 = (uintptr_t)((x469)<(x450));
x471 = (x469)+(x447);
x472 = (uintptr_t)((x471)<(x447));
x473 = (x470)+(x472);
x474 = (x473)+(x448);
x475 = (uintptr_t)((x474)<(x448));
x476 = (x474)+(x445);
x477 = (uintptr_t)((x476)<(x445));
x478 = (x475)+(x477);
x479 = (x478)+(x446);
x480 = (uintptr_t)((x479)<(x446));
x481 = (x479)+(x443);
x482 = (uintptr_t)((x481)<(x443));
x483 = (x480)+(x482);
x484 = (x483)+(x444);
x485 = (uintptr_t)((x484)<(x444));
x486 = (x484)+(x441);
x487 = (uintptr_t)((x486)<(x441));
x488 = (x485)+(x487);
x489 = (x488)+(x442);
x490 = (x398)+(x455);
x491 = (uintptr_t)((x490)<(x398));
x492 = (x491)+(x402);
x493 = (uintptr_t)((x492)<(x402));
x494 = (x492)+(x457);
x495 = (uintptr_t)((x494)<(x457));
x496 = (x493)+(x495);
x497 = (x496)+(x407);
x498 = (uintptr_t)((x497)<(x407));
x499 = (x497)+(x461);
x500 = (uintptr_t)((x499)<(x461));
x501 = (x498)+(x500);
x502 = (x501)+(x412);
x503 = (uintptr_t)((x502)<(x412));
x504 = (x502)+(x466);
x505 = (uintptr_t)((x504)<(x466));
x506 = (x503)+(x505);
x507 = (x506)+(x417);
x508 = (uintptr_t)((x507)<(x417));
x509 = (x507)+(x471);
x510 = (uintptr_t)((x509)<(x471));
x511 = (x508)+(x510);
x512 = (x511)+(x422);
x513 = (uintptr_t)((x512)<(x422));
x514 = (x512)+(x476);
x515 = (uintptr_t)((x514)<(x476));
x516 = (x513)+(x515);
x517 = (x516)+(x427);
x518 = (uintptr_t)((x517)<(x427));
x519 = (x517)+(x481);
x520 = (uintptr_t)((x519)<(x481));
x521 = (x518)+(x520);
x522 = (x521)+(x432);
x523 = (uintptr_t)((x522)<(x432));
x524 = (x522)+(x486);
x525 = (uintptr_t)((x524)<(x486));
x526 = (x523)+(x525);
x527 = (x526)+(x437);
x528 = (uintptr_t)((x527)<(x437));
x529 = (x527)+(x489);
x530 = (uintptr_t)((x529)<(x489));
x531 = (x528)+(x530);
x532 = (x531)+(x439);
x533 = (x18)*(x15);
x534 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x18)*(x15))>>32 : ((__uint128_t)(x18)*(x15))>>64);
x535 = (x18)*(x14);
x536 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x18)*(x14))>>32 : ((__uint128_t)(x18)*(x14))>>64);
x537 = (x18)*(x13);
x538 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x18)*(x13))>>32 : ((__uint128_t)(x18)*(x13))>>64);
x539 = (x18)*(x12);
x540 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x18)*(x12))>>32 : ((__uint128_t)(x18)*(x12))>>64);
x541 = (x18)*(x11);
x542 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x18)*(x11))>>32 : ((__uint128_t)(x18)*(x11))>>64);
x543 = (x18)*(x10);
x544 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x18)*(x10))>>32 : ((__uint128_t)(x18)*(x10))>>64);
x545 = (x18)*(x9);
x546 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x18)*(x9))>>32 : ((__uint128_t)(x18)*(x9))>>64);
x547 = (x18)*(x8);
x548 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x18)*(x8))>>32 : ((__uint128_t)(x18)*(x8))>>64);
x549 = (x548)+(x545);
x550 = (uintptr_t)((x549)<(x548));
x551 = (x550)+(x546);
x552 = (uintptr_t)((x551)<(x546));
x553 = (x551)+(x543);
x554 = (uintptr_t)((x553)<(x543));
x555 = (x552)+(x554);
x556 = (x555)+(x544);
x557 = (uintptr_t)((x556)<(x544));
x558 = (x556)+(x541);
x559 = (uintptr_t)((x558)<(x541));
x560 = (x557)+(x559);
x561 = (x560)+(x542);
x562 = (uintptr_t)((x561)<(x542));
x563 = (x561)+(x539);
x564 = (uintptr_t)((x563)<(x539));
x565 = (x562)+(x564);
x566 = (x565)+(x540);
x567 = (uintptr_t)((x566)<(x540));
x568 = (x566)+(x537);
x569 = (uintptr_t)((x568)<(x537));
x570 = (x567)+(x569);
x571 = (x570)+(x538);
x572 = (uintptr_t)((x571)<(x538));
x573 = (x571)+(x535);
x574 = (uintptr_t)((x573)<(x535));
x575 = (x572)+(x574);
x576 = (x575)+(x536);
x577 = (uintptr_t)((x576)<(x536));
x578 = (x576)+(x533);
x579 = (uintptr_t)((x578)<(x533));
x580 = (x577)+(x579);
x581 = (x580)+(x534);
x582 = (x494)+(x547);
x583 = (uintptr_t)((x582)<(x494));
x584 = (x583)+(x499);
x585 = (uintptr_t)((x584)<(x499));
x586 = (x584)+(x549);
x587 = (uintptr_t)((x586)<(x549));
x588 = (x585)+(x587);
x589 = (x588)+(x504);
x590 = (uintptr_t)((x589)<(x504));
x591 = (x589)+(x553);
x592 = (uintptr_t)((x591)<(x553));
x593 = (x590)+(x592);
x594 = (x593)+(x509);
x595 = (uintptr_t)((x594)<(x509));
x596 = (x594)+(x558);
x597 = (uintptr_t)((x596)<(x558));
x598 = (x595)+(x597);
x599 = (x598)+(x514);
x600 = (uintptr_t)((x599)<(x514));
x601 = (x599)+(x563);
x602 = (uintptr_t)((x601)<(x563));
x603 = (x600)+(x602);
x604 = (x603)+(x519);
x605 = (uintptr_t)((x604)<(x519));
x606 = (x604)+(x568);
x607 = (uintptr_t)((x606)<(x568));
x608 = (x605)+(x607);
x609 = (x608)+(x524);
x610 = (uintptr_t)((x609)<(x524));
x611 = (x609)+(x573);
x612 = (uintptr_t)((x611)<(x573));
x613 = (x610)+(x612);
x614 = (x613)+(x529);
x615 = (uintptr_t)((x614)<(x529));
x616 = (x614)+(x578);
x617 = (uintptr_t)((x616)<(x578));
x618 = (x615)+(x617);
x619 = (x618)+(x532);
x620 = (uintptr_t)((x619)<(x532));
x621 = (x619)+(x581);
x622 = (uintptr_t)((x621)<(x581));
x623 = (x620)+(x622);
x624 = (x582)*((uintptr_t)3525653809ULL);
x625 = (x624)*((uintptr_t)4294967295ULL);
x626 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x624)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x624)*((uintptr_t)4294967295ULL))>>64);
x627 = (x624)*((uintptr_t)4294967295ULL);
x628 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x624)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x624)*((uintptr_t)4294967295ULL))>>64);
x629 = (x624)*((uintptr_t)4294967295ULL);
x630 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x624)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x624)*((uintptr_t)4294967295ULL))>>64);
x631 = (x624)*((uintptr_t)4294967295ULL);
x632 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x624)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x624)*((uintptr_t)4294967295ULL))>>64);
x633 = (x624)*((uintptr_t)4294967295ULL);
x634 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x624)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x624)*((uintptr_t)4294967295ULL))>>64);
x635 = (x624)*((uintptr_t)4294967295ULL);
x636 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x624)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x624)*((uintptr_t)4294967295ULL))>>64);
x637 = (x624)*((uintptr_t)4294967294ULL);
x638 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x624)*((uintptr_t)4294967294ULL))>>32 : ((__uint128_t)(x624)*((uintptr_t)4294967294ULL))>>64);
x639 = (x624)*((uintptr_t)4294966319ULL);
x640 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x624)*((uintptr_t)4294966319ULL))>>32 : ((__uint128_t)(x624)*((uintptr_t)4294966319ULL))>>64);
x641 = (x640)+(x637);
x642 = (uintptr_t)((x641)<(x640));
x643 = (x642)+(x638);
x644 = (uintptr_t)((x643)<(x638));
x645 = (x643)+(x635);
x646 = (uintptr_t)((x645)<(x635));
x647 = (x644)+(x646);
x648 = (x647)+(x636);
x649 = (uintptr_t)((x648)<(x636));
x650 = (x648)+(x633);
x651 = (uintptr_t)((x650)<(x633));
x652 = (x649)+(x651);
x653 = (x652)+(x634);
x654 = (uintptr_t)((x653)<(x634));
x655 = (x653)+(x631);
x656 = (uintptr_t)((x655)<(x631));
x657 = (x654)+(x656);
x658 = (x657)+(x632);
x659 = (uintptr_t)((x658)<(x632));
x660 = (x658)+(x629);
x661 = (uintptr_t)((x660)<(x629));
x662 = (x659)+(x661);
x663 = (x662)+(x630);
x664 = (uintptr_t)((x663)<(x630));
x665 = (x663)+(x627);
x666 = (uintptr_t)((x665)<(x627));
x667 = (x664)+(x666);
x668 = (x667)+(x628);
x669 = (uintptr_t)((x668)<(x628));
x670 = (x668)+(x625);
x671 = (uintptr_t)((x670)<(x625));
x672 = (x669)+(x671);
x673 = (x672)+(x626);
x674 = (x582)+(x639);
x675 = (uintptr_t)((x674)<(x582));
x676 = (x675)+(x586);
x677 = (uintptr_t)((x676)<(x586));
x678 = (x676)+(x641);
x679 = (uintptr_t)((x678)<(x641));
x680 = (x677)+(x679);
x681 = (x680)+(x591);
x682 = (uintptr_t)((x681)<(x591));
x683 = (x681)+(x645);
x684 = (uintptr_t)((x683)<(x645));
x685 = (x682)+(x684);
x686 = (x685)+(x596);
x687 = (uintptr_t)((x686)<(x596));
x688 = (x686)+(x650);
x689 = (uintptr_t)((x688)<(x650));
x690 = (x687)+(x689);
x691 = (x690)+(x601);
x692 = (uintptr_t)((x691)<(x601));
x693 = (x691)+(x655);
x694 = (uintptr_t)((x693)<(x655));
x695 = (x692)+(x694);
x696 = (x695)+(x606);
x697 = (uintptr_t)((x696)<(x606));
x698 = (x696)+(x660);
x699 = (uintptr_t)((x698)<(x660));
x700 = (x697)+(x699);
x701 = (x700)+(x611);
x702 = (uintptr_t)((x701)<(x611));
x703 = (x701)+(x665);
x704 = (uintptr_t)((x703)<(x665));
x705 = (x702)+(x704);
x706 = (x705)+(x616);
x707 = (uintptr_t)((x706)<(x616));
x708 = (x706)+(x670);
x709 = (uintptr_t)((x708)<(x670));
x710 = (x707)+(x709);
x711 = (x710)+(x621);
x712 = (uintptr_t)((x711)<(x621));
x713 = (x711)+(x673);
x714 = (uintptr_t)((x713)<(x673));
x715 = (x712)+(x714);
x716 = (x715)+(x623);
x717 = (x19)*(x15);
x718 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x19)*(x15))>>32 : ((__uint128_t)(x19)*(x15))>>64);
x719 = (x19)*(x14);
x720 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x19)*(x14))>>32 : ((__uint128_t)(x19)*(x14))>>64);
x721 = (x19)*(x13);
x722 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x19)*(x13))>>32 : ((__uint128_t)(x19)*(x13))>>64);
x723 = (x19)*(x12);
x724 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x19)*(x12))>>32 : ((__uint128_t)(x19)*(x12))>>64);
x725 = (x19)*(x11);
x726 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x19)*(x11))>>32 : ((__uint128_t)(x19)*(x11))>>64);
x727 = (x19)*(x10);
x728 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x19)*(x10))>>32 : ((__uint128_t)(x19)*(x10))>>64);
x729 = (x19)*(x9);
x730 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x19)*(x9))>>32 : ((__uint128_t)(x19)*(x9))>>64);
x731 = (x19)*(x8);
x732 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x19)*(x8))>>32 : ((__uint128_t)(x19)*(x8))>>64);
x733 = (x732)+(x729);
x734 = (uintptr_t)((x733)<(x732));
x735 = (x734)+(x730);
x736 = (uintptr_t)((x735)<(x730));
x737 = (x735)+(x727);
x738 = (uintptr_t)((x737)<(x727));
x739 = (x736)+(x738);
x740 = (x739)+(x728);
x741 = (uintptr_t)((x740)<(x728));
x742 = (x740)+(x725);
x743 = (uintptr_t)((x742)<(x725));
x744 = (x741)+(x743);
x745 = (x744)+(x726);
x746 = (uintptr_t)((x745)<(x726));
x747 = (x745)+(x723);
x748 = (uintptr_t)((x747)<(x723));
x749 = (x746)+(x748);
x750 = (x749)+(x724);
x751 = (uintptr_t)((x750)<(x724));
x752 = (x750)+(x721);
x753 = (uintptr_t)((x752)<(x721));
x754 = (x751)+(x753);
x755 = (x754)+(x722);
x756 = (uintptr_t)((x755)<(x722));
x757 = (x755)+(x719);
x758 = (uintptr_t)((x757)<(x719));
x759 = (x756)+(x758);
x760 = (x759)+(x720);
x761 = (uintptr_t)((x760)<(x720));
x762 = (x760)+(x717);
x763 = (uintptr_t)((x762)<(x717));
x764 = (x761)+(x763);
x765 = (x764)+(x718);
x766 = (x678)+(x731);
x767 = (uintptr_t)((x766)<(x678));
x768 = (x767)+(x683);
x769 = (uintptr_t)((x768)<(x683));
x770 = (x768)+(x733);
x771 = (uintptr_t)((x770)<(x733));
x772 = (x769)+(x771);
x773 = (x772)+(x688);
x774 = (uintptr_t)((x773)<(x688));
x775 = (x773)+(x737);
x776 = (uintptr_t)((x775)<(x737));
x777 = (x774)+(x776);
x778 = (x777)+(x693);
x779 = (uintptr_t)((x778)<(x693));
x780 = (x778)+(x742);
x781 = (uintptr_t)((x780)<(x742));
x782 = (x779)+(x781);
x783 = (x782)+(x698);
x784 = (uintptr_t)((x783)<(x698));
x785 = (x783)+(x747);
x786 = (uintptr_t)((x785)<(x747));
x787 = (x784)+(x786);
x788 = (x787)+(x703);
x789 = (uintptr_t)((x788)<(x703));
x790 = (x788)+(x752);
x791 = (uintptr_t)((x790)<(x752));
x792 = (x789)+(x791);
x793 = (x792)+(x708);
x794 = (uintptr_t)((x793)<(x708));
x795 = (x793)+(x757);
x796 = (uintptr_t)((x795)<(x757));
x797 = (x794)+(x796);
x798 = (x797)+(x713);
x799 = (uintptr_t)((x798)<(x713));
x800 = (x798)+(x762);
x801 = (uintptr_t)((x800)<(x762));
x802 = (x799)+(x801);
x803 = (x802)+(x716);
x804 = (uintptr_t)((x803)<(x716));
x805 = (x803)+(x765);
x806 = (uintptr_t)((x805)<(x765));
x807 = (x804)+(x806);
x808 = (x766)*((uintptr_t)3525653809ULL);
x809 = (x808)*((uintptr_t)4294967295ULL);
x810 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x808)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x808)*((uintptr_t)4294967295ULL))>>64);
x811 = (x808)*((uintptr_t)4294967295ULL);
x812 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x808)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x808)*((uintptr_t)4294967295ULL))>>64);
x813 = (x808)*((uintptr_t)4294967295ULL);
x814 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x808)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x808)*((uintptr_t)4294967295ULL))>>64);
x815 = (x808)*((uintptr_t)4294967295ULL);
x816 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x808)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x808)*((uintptr_t)4294967295ULL))>>64);
x817 = (x808)*((uintptr_t)4294967295ULL);
x818 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x808)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x808)*((uintptr_t)4294967295ULL))>>64);
x819 = (x808)*((uintptr_t)4294967295ULL);
x820 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x808)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x808)*((uintptr_t)4294967295ULL))>>64);
x821 = (x808)*((uintptr_t)4294967294ULL);
x822 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x808)*((uintptr_t)4294967294ULL))>>32 : ((__uint128_t)(x808)*((uintptr_t)4294967294ULL))>>64);
x823 = (x808)*((uintptr_t)4294966319ULL);
x824 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x808)*((uintptr_t)4294966319ULL))>>32 : ((__uint128_t)(x808)*((uintptr_t)4294966319ULL))>>64);
x825 = (x824)+(x821);
x826 = (uintptr_t)((x825)<(x824));
x827 = (x826)+(x822);
x828 = (uintptr_t)((x827)<(x822));
x829 = (x827)+(x819);
x830 = (uintptr_t)((x829)<(x819));
x831 = (x828)+(x830);
x832 = (x831)+(x820);
x833 = (uintptr_t)((x832)<(x820));
x834 = (x832)+(x817);
x835 = (uintptr_t)((x834)<(x817));
x836 = (x833)+(x835);
x837 = (x836)+(x818);
x838 = (uintptr_t)((x837)<(x818));
x839 = (x837)+(x815);
x840 = (uintptr_t)((x839)<(x815));
x841 = (x838)+(x840);
x842 = (x841)+(x816);
x843 = (uintptr_t)((x842)<(x816));
x844 = (x842)+(x813);
x845 = (uintptr_t)((x844)<(x813));
x846 = (x843)+(x845);
x847 = (x846)+(x814);
x848 = (uintptr_t)((x847)<(x814));
x849 = (x847)+(x811);
x850 = (uintptr_t)((x849)<(x811));
x851 = (x848)+(x850);
x852 = (x851)+(x812);
x853 = (uintptr_t)((x852)<(x812));
x854 = (x852)+(x809);
x855 = (uintptr_t)((x854)<(x809));
x856 = (x853)+(x855);
x857 = (x856)+(x810);
x858 = (x766)+(x823);
x859 = (uintptr_t)((x858)<(x766));
x860 = (x859)+(x770);
x861 = (uintptr_t)((x860)<(x770));
x862 = (x860)+(x825);
x863 = (uintptr_t)((x862)<(x825));
x864 = (x861)+(x863);
x865 = (x864)+(x775);
x866 = (uintptr_t)((x865)<(x775));
x867 = (x865)+(x829);
x868 = (uintptr_t)((x867)<(x829));
x869 = (x866)+(x868);
x870 = (x869)+(x780);
x871 = (uintptr_t)((x870)<(x780));
x872 = (x870)+(x834);
x873 = (uintptr_t)((x872)<(x834));
x874 = (x871)+(x873);
x875 = (x874)+(x785);
x876 = (uintptr_t)((x875)<(x785));
x877 = (x875)+(x839);
x878 = (uintptr_t)((x877)<(x839));
x879 = (x876)+(x878);
x880 = (x879)+(x790);
x881 = (uintptr_t)((x880)<(x790));
x882 = (x880)+(x844);
x883 = (uintptr_t)((x882)<(x844));
x884 = (x881)+(x883);
x885 = (x884)+(x795);
x886 = (uintptr_t)((x885)<(x795));
x887 = (x885)+(x849);
x888 = (uintptr_t)((x887)<(x849));
x889 = (x886)+(x888);
x890 = (x889)+(x800);
x891 = (uintptr_t)((x890)<(x800));
x892 = (x890)+(x854);
x893 = (uintptr_t)((x892)<(x854));
x894 = (x891)+(x893);
x895 = (x894)+(x805);
x896 = (uintptr_t)((x895)<(x805));
x897 = (x895)+(x857);
x898 = (uintptr_t)((x897)<(x857));
x899 = (x896)+(x898);
x900 = (x899)+(x807);
x901 = (x20)*(x15);
x902 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x20)*(x15))>>32 : ((__uint128_t)(x20)*(x15))>>64);
x903 = (x20)*(x14);
x904 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x20)*(x14))>>32 : ((__uint128_t)(x20)*(x14))>>64);
x905 = (x20)*(x13);
x906 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x20)*(x13))>>32 : ((__uint128_t)(x20)*(x13))>>64);
x907 = (x20)*(x12);
x908 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x20)*(x12))>>32 : ((__uint128_t)(x20)*(x12))>>64);
x909 = (x20)*(x11);
x910 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x20)*(x11))>>32 : ((__uint128_t)(x20)*(x11))>>64);
x911 = (x20)*(x10);
x912 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x20)*(x10))>>32 : ((__uint128_t)(x20)*(x10))>>64);
x913 = (x20)*(x9);
x914 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x20)*(x9))>>32 : ((__uint128_t)(x20)*(x9))>>64);
x915 = (x20)*(x8);
x916 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x20)*(x8))>>32 : ((__uint128_t)(x20)*(x8))>>64);
x917 = (x916)+(x913);
x918 = (uintptr_t)((x917)<(x916));
x919 = (x918)+(x914);
x920 = (uintptr_t)((x919)<(x914));
x921 = (x919)+(x911);
x922 = (uintptr_t)((x921)<(x911));
x923 = (x920)+(x922);
x924 = (x923)+(x912);
x925 = (uintptr_t)((x924)<(x912));
x926 = (x924)+(x909);
x927 = (uintptr_t)((x926)<(x909));
x928 = (x925)+(x927);
x929 = (x928)+(x910);
x930 = (uintptr_t)((x929)<(x910));
x931 = (x929)+(x907);
x932 = (uintptr_t)((x931)<(x907));
x933 = (x930)+(x932);
x934 = (x933)+(x908);
x935 = (uintptr_t)((x934)<(x908));
x936 = (x934)+(x905);
x937 = (uintptr_t)((x936)<(x905));
x938 = (x935)+(x937);
x939 = (x938)+(x906);