forked from mit-plv/fiat-crypto
-
Notifications
You must be signed in to change notification settings - Fork 0
/
p384_64.c
3830 lines (3782 loc) · 190 KB
/
p384_64.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 p384 64 '2^384 - 2^128 - 2^96 + 2^32 - 1' mul square add sub opp from_montgomery to_montgomery nonzero selectznz to_bytes from_bytes one msat divstep divstep_precomp */
/* curve description: p384 */
/* machine_wordsize = 64 (from "64") */
/* requested operations: mul, square, add, sub, opp, from_montgomery, to_montgomery, nonzero, selectznz, to_bytes, from_bytes, one, msat, divstep, divstep_precomp */
/* m = 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000ffffffff (from "2^384 - 2^128 - 2^96 + 2^32 - 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] << 64) + (z[2] << 128) + (z[3] << 192) + (z[4] << 256) + (z[5] << 0x140) */
/* bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) + (z[32] << 256) + (z[33] << 0x108) + (z[34] << 0x110) + (z[35] << 0x118) + (z[36] << 0x120) + (z[37] << 0x128) + (z[38] << 0x130) + (z[39] << 0x138) + (z[40] << 0x140) + (z[41] << 0x148) + (z[42] << 0x150) + (z[43] << 0x158) + (z[44] << 0x160) + (z[45] << 0x168) + (z[46] << 0x170) + (z[47] << 0x178) */
/* twos_complement_eval z = let x1 := z[0] + (z[1] << 64) + (z[2] << 128) + (z[3] << 192) + (z[4] << 256) + (z[5] << 0x140) in */
/* if x1 & (2^384-1) < 2^383 then x1 & (2^384-1) else (x1 & (2^384-1)) - 2^384 */
#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 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
* in1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
* Output Bounds:
* out0: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
*/
static
void internal_fiat_p384_mul(uintptr_t out0, uintptr_t in0, uintptr_t in1) {
uintptr_t x1, x2, x3, x4, x5, x0, x17, x26, x29, x31, x27, x32, x24, x33, x35, x36, x25, x37, x22, x38, x40, x41, x23, x42, x20, x43, x45, x46, x21, x47, x18, x48, x50, x51, x19, x53, x62, x65, x67, x63, x68, x60, x69, x71, x72, x61, x73, x58, x74, x76, x77, x59, x78, x56, x79, x81, x82, x57, x83, x54, x84, x86, x87, x55, x64, x89, x28, x90, x30, x91, x66, x92, x94, x95, x34, x96, x70, x97, x99, x100, x39, x101, x75, x102, x104, x105, x44, x106, x80, x107, x109, x110, x49, x111, x85, x112, x114, x115, x52, x116, x88, x117, x119, x12, x129, x132, x134, x130, x135, x127, x136, x138, x139, x128, x140, x125, x141, x143, x144, x126, x145, x123, x146, x148, x149, x124, x150, x121, x151, x153, x154, x122, x131, x93, x157, x98, x158, x133, x159, x161, x162, x103, x163, x137, x164, x166, x167, x108, x168, x142, x169, x171, x172, x113, x173, x147, x174, x176, x177, x118, x178, x152, x179, x181, x182, x120, x183, x155, x184, x186, x188, x197, x200, x202, x198, x203, x195, x204, x206, x207, x196, x208, x193, x209, x211, x212, x194, x213, x191, x214, x216, x217, x192, x218, x189, x219, x221, x222, x190, x199, x224, x156, x225, x160, x226, x201, x227, x229, x230, x165, x231, x205, x232, x234, x235, x170, x236, x210, x237, x239, x240, x175, x241, x215, x242, x244, x245, x180, x246, x220, x247, x249, x250, x185, x251, x223, x252, x254, x255, x187, x13, x265, x268, x270, x266, x271, x263, x272, x274, x275, x264, x276, x261, x277, x279, x280, x262, x281, x259, x282, x284, x285, x260, x286, x257, x287, x289, x290, x258, x267, x228, x293, x233, x294, x269, x295, x297, x298, x238, x299, x273, x300, x302, x303, x243, x304, x278, x305, x307, x308, x248, x309, x283, x310, x312, x313, x253, x314, x288, x315, x317, x318, x256, x319, x291, x320, x322, x324, x333, x336, x338, x334, x339, x331, x340, x342, x343, x332, x344, x329, x345, x347, x348, x330, x349, x327, x350, x352, x353, x328, x354, x325, x355, x357, x358, x326, x335, x360, x292, x361, x296, x362, x337, x363, x365, x366, x301, x367, x341, x368, x370, x371, x306, x372, x346, x373, x375, x376, x311, x377, x351, x378, x380, x381, x316, x382, x356, x383, x385, x386, x321, x387, x359, x388, x390, x391, x323, x14, x401, x404, x406, x402, x407, x399, x408, x410, x411, x400, x412, x397, x413, x415, x416, x398, x417, x395, x418, x420, x421, x396, x422, x393, x423, x425, x426, x394, x403, x364, x429, x369, x430, x405, x431, x433, x434, x374, x435, x409, x436, x438, x439, x379, x440, x414, x441, x443, x444, x384, x445, x419, x446, x448, x449, x389, x450, x424, x451, x453, x454, x392, x455, x427, x456, x458, x460, x469, x472, x474, x470, x475, x467, x476, x478, x479, x468, x480, x465, x481, x483, x484, x466, x485, x463, x486, x488, x489, x464, x490, x461, x491, x493, x494, x462, x471, x496, x428, x497, x432, x498, x473, x499, x501, x502, x437, x503, x477, x504, x506, x507, x442, x508, x482, x509, x511, x512, x447, x513, x487, x514, x516, x517, x452, x518, x492, x519, x521, x522, x457, x523, x495, x524, x526, x527, x459, x15, x537, x540, x542, x538, x543, x535, x544, x546, x547, x536, x548, x533, x549, x551, x552, x534, x553, x531, x554, x556, x557, x532, x558, x529, x559, x561, x562, x530, x539, x500, x565, x505, x566, x541, x567, x569, x570, x510, x571, x545, x572, x574, x575, x515, x576, x550, x577, x579, x580, x520, x581, x555, x582, x584, x585, x525, x586, x560, x587, x589, x590, x528, x591, x563, x592, x594, x596, x605, x608, x610, x606, x611, x603, x612, x614, x615, x604, x616, x601, x617, x619, x620, x602, x621, x599, x622, x624, x625, x600, x626, x597, x627, x629, x630, x598, x607, x632, x564, x633, x568, x634, x609, x635, x637, x638, x573, x639, x613, x640, x642, x643, x578, x644, x618, x645, x647, x648, x583, x649, x623, x650, x652, x653, x588, x654, x628, x655, x657, x658, x593, x659, x631, x660, x662, x663, x595, x11, x10, x9, x8, x7, x16, x6, x673, x676, x678, x674, x679, x671, x680, x682, x683, x672, x684, x669, x685, x687, x688, x670, x689, x667, x690, x692, x693, x668, x694, x665, x695, x697, x698, x666, x675, x636, x701, x641, x702, x677, x703, x705, x706, x646, x707, x681, x708, x710, x711, x651, x712, x686, x713, x715, x716, x656, x717, x691, x718, x720, x721, x661, x722, x696, x723, x725, x726, x664, x727, x699, x728, x730, x732, x741, x744, x746, x742, x747, x739, x748, x750, x751, x740, x752, x737, x753, x755, x756, x738, x757, x735, x758, x760, x761, x736, x762, x733, x763, x765, x766, x734, x743, x768, x700, x769, x704, x770, x745, x771, x773, x774, x709, x775, x749, x776, x778, x779, x714, x780, x754, x781, x783, x784, x719, x785, x759, x786, x788, x789, x724, x790, x764, x791, x793, x794, x729, x795, x767, x796, x798, x799, x731, x802, x803, x804, x806, x807, x808, x809, x811, x812, x813, x814, x816, x817, x818, x819, x821, x822, x823, x824, x826, x827, x800, x828, x772, x830, x801, x831, x777, x833, x805, x834, x782, x836, x810, x837, x787, x839, x815, x840, x792, x842, x820, x843, x829, x797, x845, x825, x846, x832, x835, x838, x841, x844, x847, x848, x849, x850, x851, x852, x853;
x0 = _br2_load((in0)+((uintptr_t)0ULL), sizeof(uintptr_t));
x1 = _br2_load((in0)+((uintptr_t)8ULL), sizeof(uintptr_t));
x2 = _br2_load((in0)+((uintptr_t)16ULL), sizeof(uintptr_t));
x3 = _br2_load((in0)+((uintptr_t)24ULL), sizeof(uintptr_t));
x4 = _br2_load((in0)+((uintptr_t)32ULL), sizeof(uintptr_t));
x5 = _br2_load((in0)+((uintptr_t)40ULL), sizeof(uintptr_t));
/*skip*/
x6 = _br2_load((in1)+((uintptr_t)0ULL), sizeof(uintptr_t));
x7 = _br2_load((in1)+((uintptr_t)8ULL), sizeof(uintptr_t));
x8 = _br2_load((in1)+((uintptr_t)16ULL), sizeof(uintptr_t));
x9 = _br2_load((in1)+((uintptr_t)24ULL), sizeof(uintptr_t));
x10 = _br2_load((in1)+((uintptr_t)32ULL), sizeof(uintptr_t));
x11 = _br2_load((in1)+((uintptr_t)40ULL), sizeof(uintptr_t));
/*skip*/
/*skip*/
x12 = x1;
x13 = x2;
x14 = x3;
x15 = x4;
x16 = x5;
x17 = x0;
x18 = (x17)*(x11);
x19 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x17)*(x11))>>32 : ((__uint128_t)(x17)*(x11))>>64);
x20 = (x17)*(x10);
x21 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x17)*(x10))>>32 : ((__uint128_t)(x17)*(x10))>>64);
x22 = (x17)*(x9);
x23 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x17)*(x9))>>32 : ((__uint128_t)(x17)*(x9))>>64);
x24 = (x17)*(x8);
x25 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x17)*(x8))>>32 : ((__uint128_t)(x17)*(x8))>>64);
x26 = (x17)*(x7);
x27 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x17)*(x7))>>32 : ((__uint128_t)(x17)*(x7))>>64);
x28 = (x17)*(x6);
x29 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x17)*(x6))>>32 : ((__uint128_t)(x17)*(x6))>>64);
x30 = (x29)+(x26);
x31 = (uintptr_t)((x30)<(x29));
x32 = (x31)+(x27);
x33 = (uintptr_t)((x32)<(x27));
x34 = (x32)+(x24);
x35 = (uintptr_t)((x34)<(x24));
x36 = (x33)+(x35);
x37 = (x36)+(x25);
x38 = (uintptr_t)((x37)<(x25));
x39 = (x37)+(x22);
x40 = (uintptr_t)((x39)<(x22));
x41 = (x38)+(x40);
x42 = (x41)+(x23);
x43 = (uintptr_t)((x42)<(x23));
x44 = (x42)+(x20);
x45 = (uintptr_t)((x44)<(x20));
x46 = (x43)+(x45);
x47 = (x46)+(x21);
x48 = (uintptr_t)((x47)<(x21));
x49 = (x47)+(x18);
x50 = (uintptr_t)((x49)<(x18));
x51 = (x48)+(x50);
x52 = (x51)+(x19);
x53 = (x28)*((uintptr_t)4294967297ULL);
x54 = (x53)*((uintptr_t)18446744073709551615ULL);
x55 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x53)*((uintptr_t)18446744073709551615ULL))>>32 : ((__uint128_t)(x53)*((uintptr_t)18446744073709551615ULL))>>64);
x56 = (x53)*((uintptr_t)18446744073709551615ULL);
x57 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x53)*((uintptr_t)18446744073709551615ULL))>>32 : ((__uint128_t)(x53)*((uintptr_t)18446744073709551615ULL))>>64);
x58 = (x53)*((uintptr_t)18446744073709551615ULL);
x59 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x53)*((uintptr_t)18446744073709551615ULL))>>32 : ((__uint128_t)(x53)*((uintptr_t)18446744073709551615ULL))>>64);
x60 = (x53)*((uintptr_t)18446744073709551614ULL);
x61 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x53)*((uintptr_t)18446744073709551614ULL))>>32 : ((__uint128_t)(x53)*((uintptr_t)18446744073709551614ULL))>>64);
x62 = (x53)*((uintptr_t)18446744069414584320ULL);
x63 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x53)*((uintptr_t)18446744069414584320ULL))>>32 : ((__uint128_t)(x53)*((uintptr_t)18446744069414584320ULL))>>64);
x64 = (x53)*((uintptr_t)4294967295ULL);
x65 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x53)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x53)*((uintptr_t)4294967295ULL))>>64);
x66 = (x65)+(x62);
x67 = (uintptr_t)((x66)<(x65));
x68 = (x67)+(x63);
x69 = (uintptr_t)((x68)<(x63));
x70 = (x68)+(x60);
x71 = (uintptr_t)((x70)<(x60));
x72 = (x69)+(x71);
x73 = (x72)+(x61);
x74 = (uintptr_t)((x73)<(x61));
x75 = (x73)+(x58);
x76 = (uintptr_t)((x75)<(x58));
x77 = (x74)+(x76);
x78 = (x77)+(x59);
x79 = (uintptr_t)((x78)<(x59));
x80 = (x78)+(x56);
x81 = (uintptr_t)((x80)<(x56));
x82 = (x79)+(x81);
x83 = (x82)+(x57);
x84 = (uintptr_t)((x83)<(x57));
x85 = (x83)+(x54);
x86 = (uintptr_t)((x85)<(x54));
x87 = (x84)+(x86);
x88 = (x87)+(x55);
x89 = (x28)+(x64);
x90 = (uintptr_t)((x89)<(x28));
x91 = (x90)+(x30);
x92 = (uintptr_t)((x91)<(x30));
x93 = (x91)+(x66);
x94 = (uintptr_t)((x93)<(x66));
x95 = (x92)+(x94);
x96 = (x95)+(x34);
x97 = (uintptr_t)((x96)<(x34));
x98 = (x96)+(x70);
x99 = (uintptr_t)((x98)<(x70));
x100 = (x97)+(x99);
x101 = (x100)+(x39);
x102 = (uintptr_t)((x101)<(x39));
x103 = (x101)+(x75);
x104 = (uintptr_t)((x103)<(x75));
x105 = (x102)+(x104);
x106 = (x105)+(x44);
x107 = (uintptr_t)((x106)<(x44));
x108 = (x106)+(x80);
x109 = (uintptr_t)((x108)<(x80));
x110 = (x107)+(x109);
x111 = (x110)+(x49);
x112 = (uintptr_t)((x111)<(x49));
x113 = (x111)+(x85);
x114 = (uintptr_t)((x113)<(x85));
x115 = (x112)+(x114);
x116 = (x115)+(x52);
x117 = (uintptr_t)((x116)<(x52));
x118 = (x116)+(x88);
x119 = (uintptr_t)((x118)<(x88));
x120 = (x117)+(x119);
x121 = (x12)*(x11);
x122 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x12)*(x11))>>32 : ((__uint128_t)(x12)*(x11))>>64);
x123 = (x12)*(x10);
x124 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x12)*(x10))>>32 : ((__uint128_t)(x12)*(x10))>>64);
x125 = (x12)*(x9);
x126 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x12)*(x9))>>32 : ((__uint128_t)(x12)*(x9))>>64);
x127 = (x12)*(x8);
x128 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x12)*(x8))>>32 : ((__uint128_t)(x12)*(x8))>>64);
x129 = (x12)*(x7);
x130 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x12)*(x7))>>32 : ((__uint128_t)(x12)*(x7))>>64);
x131 = (x12)*(x6);
x132 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x12)*(x6))>>32 : ((__uint128_t)(x12)*(x6))>>64);
x133 = (x132)+(x129);
x134 = (uintptr_t)((x133)<(x132));
x135 = (x134)+(x130);
x136 = (uintptr_t)((x135)<(x130));
x137 = (x135)+(x127);
x138 = (uintptr_t)((x137)<(x127));
x139 = (x136)+(x138);
x140 = (x139)+(x128);
x141 = (uintptr_t)((x140)<(x128));
x142 = (x140)+(x125);
x143 = (uintptr_t)((x142)<(x125));
x144 = (x141)+(x143);
x145 = (x144)+(x126);
x146 = (uintptr_t)((x145)<(x126));
x147 = (x145)+(x123);
x148 = (uintptr_t)((x147)<(x123));
x149 = (x146)+(x148);
x150 = (x149)+(x124);
x151 = (uintptr_t)((x150)<(x124));
x152 = (x150)+(x121);
x153 = (uintptr_t)((x152)<(x121));
x154 = (x151)+(x153);
x155 = (x154)+(x122);
x156 = (x93)+(x131);
x157 = (uintptr_t)((x156)<(x93));
x158 = (x157)+(x98);
x159 = (uintptr_t)((x158)<(x98));
x160 = (x158)+(x133);
x161 = (uintptr_t)((x160)<(x133));
x162 = (x159)+(x161);
x163 = (x162)+(x103);
x164 = (uintptr_t)((x163)<(x103));
x165 = (x163)+(x137);
x166 = (uintptr_t)((x165)<(x137));
x167 = (x164)+(x166);
x168 = (x167)+(x108);
x169 = (uintptr_t)((x168)<(x108));
x170 = (x168)+(x142);
x171 = (uintptr_t)((x170)<(x142));
x172 = (x169)+(x171);
x173 = (x172)+(x113);
x174 = (uintptr_t)((x173)<(x113));
x175 = (x173)+(x147);
x176 = (uintptr_t)((x175)<(x147));
x177 = (x174)+(x176);
x178 = (x177)+(x118);
x179 = (uintptr_t)((x178)<(x118));
x180 = (x178)+(x152);
x181 = (uintptr_t)((x180)<(x152));
x182 = (x179)+(x181);
x183 = (x182)+(x120);
x184 = (uintptr_t)((x183)<(x120));
x185 = (x183)+(x155);
x186 = (uintptr_t)((x185)<(x155));
x187 = (x184)+(x186);
x188 = (x156)*((uintptr_t)4294967297ULL);
x189 = (x188)*((uintptr_t)18446744073709551615ULL);
x190 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x188)*((uintptr_t)18446744073709551615ULL))>>32 : ((__uint128_t)(x188)*((uintptr_t)18446744073709551615ULL))>>64);
x191 = (x188)*((uintptr_t)18446744073709551615ULL);
x192 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x188)*((uintptr_t)18446744073709551615ULL))>>32 : ((__uint128_t)(x188)*((uintptr_t)18446744073709551615ULL))>>64);
x193 = (x188)*((uintptr_t)18446744073709551615ULL);
x194 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x188)*((uintptr_t)18446744073709551615ULL))>>32 : ((__uint128_t)(x188)*((uintptr_t)18446744073709551615ULL))>>64);
x195 = (x188)*((uintptr_t)18446744073709551614ULL);
x196 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x188)*((uintptr_t)18446744073709551614ULL))>>32 : ((__uint128_t)(x188)*((uintptr_t)18446744073709551614ULL))>>64);
x197 = (x188)*((uintptr_t)18446744069414584320ULL);
x198 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x188)*((uintptr_t)18446744069414584320ULL))>>32 : ((__uint128_t)(x188)*((uintptr_t)18446744069414584320ULL))>>64);
x199 = (x188)*((uintptr_t)4294967295ULL);
x200 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x188)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x188)*((uintptr_t)4294967295ULL))>>64);
x201 = (x200)+(x197);
x202 = (uintptr_t)((x201)<(x200));
x203 = (x202)+(x198);
x204 = (uintptr_t)((x203)<(x198));
x205 = (x203)+(x195);
x206 = (uintptr_t)((x205)<(x195));
x207 = (x204)+(x206);
x208 = (x207)+(x196);
x209 = (uintptr_t)((x208)<(x196));
x210 = (x208)+(x193);
x211 = (uintptr_t)((x210)<(x193));
x212 = (x209)+(x211);
x213 = (x212)+(x194);
x214 = (uintptr_t)((x213)<(x194));
x215 = (x213)+(x191);
x216 = (uintptr_t)((x215)<(x191));
x217 = (x214)+(x216);
x218 = (x217)+(x192);
x219 = (uintptr_t)((x218)<(x192));
x220 = (x218)+(x189);
x221 = (uintptr_t)((x220)<(x189));
x222 = (x219)+(x221);
x223 = (x222)+(x190);
x224 = (x156)+(x199);
x225 = (uintptr_t)((x224)<(x156));
x226 = (x225)+(x160);
x227 = (uintptr_t)((x226)<(x160));
x228 = (x226)+(x201);
x229 = (uintptr_t)((x228)<(x201));
x230 = (x227)+(x229);
x231 = (x230)+(x165);
x232 = (uintptr_t)((x231)<(x165));
x233 = (x231)+(x205);
x234 = (uintptr_t)((x233)<(x205));
x235 = (x232)+(x234);
x236 = (x235)+(x170);
x237 = (uintptr_t)((x236)<(x170));
x238 = (x236)+(x210);
x239 = (uintptr_t)((x238)<(x210));
x240 = (x237)+(x239);
x241 = (x240)+(x175);
x242 = (uintptr_t)((x241)<(x175));
x243 = (x241)+(x215);
x244 = (uintptr_t)((x243)<(x215));
x245 = (x242)+(x244);
x246 = (x245)+(x180);
x247 = (uintptr_t)((x246)<(x180));
x248 = (x246)+(x220);
x249 = (uintptr_t)((x248)<(x220));
x250 = (x247)+(x249);
x251 = (x250)+(x185);
x252 = (uintptr_t)((x251)<(x185));
x253 = (x251)+(x223);
x254 = (uintptr_t)((x253)<(x223));
x255 = (x252)+(x254);
x256 = (x255)+(x187);
x257 = (x13)*(x11);
x258 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x13)*(x11))>>32 : ((__uint128_t)(x13)*(x11))>>64);
x259 = (x13)*(x10);
x260 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x13)*(x10))>>32 : ((__uint128_t)(x13)*(x10))>>64);
x261 = (x13)*(x9);
x262 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x13)*(x9))>>32 : ((__uint128_t)(x13)*(x9))>>64);
x263 = (x13)*(x8);
x264 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x13)*(x8))>>32 : ((__uint128_t)(x13)*(x8))>>64);
x265 = (x13)*(x7);
x266 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x13)*(x7))>>32 : ((__uint128_t)(x13)*(x7))>>64);
x267 = (x13)*(x6);
x268 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x13)*(x6))>>32 : ((__uint128_t)(x13)*(x6))>>64);
x269 = (x268)+(x265);
x270 = (uintptr_t)((x269)<(x268));
x271 = (x270)+(x266);
x272 = (uintptr_t)((x271)<(x266));
x273 = (x271)+(x263);
x274 = (uintptr_t)((x273)<(x263));
x275 = (x272)+(x274);
x276 = (x275)+(x264);
x277 = (uintptr_t)((x276)<(x264));
x278 = (x276)+(x261);
x279 = (uintptr_t)((x278)<(x261));
x280 = (x277)+(x279);
x281 = (x280)+(x262);
x282 = (uintptr_t)((x281)<(x262));
x283 = (x281)+(x259);
x284 = (uintptr_t)((x283)<(x259));
x285 = (x282)+(x284);
x286 = (x285)+(x260);
x287 = (uintptr_t)((x286)<(x260));
x288 = (x286)+(x257);
x289 = (uintptr_t)((x288)<(x257));
x290 = (x287)+(x289);
x291 = (x290)+(x258);
x292 = (x228)+(x267);
x293 = (uintptr_t)((x292)<(x228));
x294 = (x293)+(x233);
x295 = (uintptr_t)((x294)<(x233));
x296 = (x294)+(x269);
x297 = (uintptr_t)((x296)<(x269));
x298 = (x295)+(x297);
x299 = (x298)+(x238);
x300 = (uintptr_t)((x299)<(x238));
x301 = (x299)+(x273);
x302 = (uintptr_t)((x301)<(x273));
x303 = (x300)+(x302);
x304 = (x303)+(x243);
x305 = (uintptr_t)((x304)<(x243));
x306 = (x304)+(x278);
x307 = (uintptr_t)((x306)<(x278));
x308 = (x305)+(x307);
x309 = (x308)+(x248);
x310 = (uintptr_t)((x309)<(x248));
x311 = (x309)+(x283);
x312 = (uintptr_t)((x311)<(x283));
x313 = (x310)+(x312);
x314 = (x313)+(x253);
x315 = (uintptr_t)((x314)<(x253));
x316 = (x314)+(x288);
x317 = (uintptr_t)((x316)<(x288));
x318 = (x315)+(x317);
x319 = (x318)+(x256);
x320 = (uintptr_t)((x319)<(x256));
x321 = (x319)+(x291);
x322 = (uintptr_t)((x321)<(x291));
x323 = (x320)+(x322);
x324 = (x292)*((uintptr_t)4294967297ULL);
x325 = (x324)*((uintptr_t)18446744073709551615ULL);
x326 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x324)*((uintptr_t)18446744073709551615ULL))>>32 : ((__uint128_t)(x324)*((uintptr_t)18446744073709551615ULL))>>64);
x327 = (x324)*((uintptr_t)18446744073709551615ULL);
x328 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x324)*((uintptr_t)18446744073709551615ULL))>>32 : ((__uint128_t)(x324)*((uintptr_t)18446744073709551615ULL))>>64);
x329 = (x324)*((uintptr_t)18446744073709551615ULL);
x330 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x324)*((uintptr_t)18446744073709551615ULL))>>32 : ((__uint128_t)(x324)*((uintptr_t)18446744073709551615ULL))>>64);
x331 = (x324)*((uintptr_t)18446744073709551614ULL);
x332 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x324)*((uintptr_t)18446744073709551614ULL))>>32 : ((__uint128_t)(x324)*((uintptr_t)18446744073709551614ULL))>>64);
x333 = (x324)*((uintptr_t)18446744069414584320ULL);
x334 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x324)*((uintptr_t)18446744069414584320ULL))>>32 : ((__uint128_t)(x324)*((uintptr_t)18446744069414584320ULL))>>64);
x335 = (x324)*((uintptr_t)4294967295ULL);
x336 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x324)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x324)*((uintptr_t)4294967295ULL))>>64);
x337 = (x336)+(x333);
x338 = (uintptr_t)((x337)<(x336));
x339 = (x338)+(x334);
x340 = (uintptr_t)((x339)<(x334));
x341 = (x339)+(x331);
x342 = (uintptr_t)((x341)<(x331));
x343 = (x340)+(x342);
x344 = (x343)+(x332);
x345 = (uintptr_t)((x344)<(x332));
x346 = (x344)+(x329);
x347 = (uintptr_t)((x346)<(x329));
x348 = (x345)+(x347);
x349 = (x348)+(x330);
x350 = (uintptr_t)((x349)<(x330));
x351 = (x349)+(x327);
x352 = (uintptr_t)((x351)<(x327));
x353 = (x350)+(x352);
x354 = (x353)+(x328);
x355 = (uintptr_t)((x354)<(x328));
x356 = (x354)+(x325);
x357 = (uintptr_t)((x356)<(x325));
x358 = (x355)+(x357);
x359 = (x358)+(x326);
x360 = (x292)+(x335);
x361 = (uintptr_t)((x360)<(x292));
x362 = (x361)+(x296);
x363 = (uintptr_t)((x362)<(x296));
x364 = (x362)+(x337);
x365 = (uintptr_t)((x364)<(x337));
x366 = (x363)+(x365);
x367 = (x366)+(x301);
x368 = (uintptr_t)((x367)<(x301));
x369 = (x367)+(x341);
x370 = (uintptr_t)((x369)<(x341));
x371 = (x368)+(x370);
x372 = (x371)+(x306);
x373 = (uintptr_t)((x372)<(x306));
x374 = (x372)+(x346);
x375 = (uintptr_t)((x374)<(x346));
x376 = (x373)+(x375);
x377 = (x376)+(x311);
x378 = (uintptr_t)((x377)<(x311));
x379 = (x377)+(x351);
x380 = (uintptr_t)((x379)<(x351));
x381 = (x378)+(x380);
x382 = (x381)+(x316);
x383 = (uintptr_t)((x382)<(x316));
x384 = (x382)+(x356);
x385 = (uintptr_t)((x384)<(x356));
x386 = (x383)+(x385);
x387 = (x386)+(x321);
x388 = (uintptr_t)((x387)<(x321));
x389 = (x387)+(x359);
x390 = (uintptr_t)((x389)<(x359));
x391 = (x388)+(x390);
x392 = (x391)+(x323);
x393 = (x14)*(x11);
x394 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x14)*(x11))>>32 : ((__uint128_t)(x14)*(x11))>>64);
x395 = (x14)*(x10);
x396 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x14)*(x10))>>32 : ((__uint128_t)(x14)*(x10))>>64);
x397 = (x14)*(x9);
x398 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x14)*(x9))>>32 : ((__uint128_t)(x14)*(x9))>>64);
x399 = (x14)*(x8);
x400 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x14)*(x8))>>32 : ((__uint128_t)(x14)*(x8))>>64);
x401 = (x14)*(x7);
x402 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x14)*(x7))>>32 : ((__uint128_t)(x14)*(x7))>>64);
x403 = (x14)*(x6);
x404 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x14)*(x6))>>32 : ((__uint128_t)(x14)*(x6))>>64);
x405 = (x404)+(x401);
x406 = (uintptr_t)((x405)<(x404));
x407 = (x406)+(x402);
x408 = (uintptr_t)((x407)<(x402));
x409 = (x407)+(x399);
x410 = (uintptr_t)((x409)<(x399));
x411 = (x408)+(x410);
x412 = (x411)+(x400);
x413 = (uintptr_t)((x412)<(x400));
x414 = (x412)+(x397);
x415 = (uintptr_t)((x414)<(x397));
x416 = (x413)+(x415);
x417 = (x416)+(x398);
x418 = (uintptr_t)((x417)<(x398));
x419 = (x417)+(x395);
x420 = (uintptr_t)((x419)<(x395));
x421 = (x418)+(x420);
x422 = (x421)+(x396);
x423 = (uintptr_t)((x422)<(x396));
x424 = (x422)+(x393);
x425 = (uintptr_t)((x424)<(x393));
x426 = (x423)+(x425);
x427 = (x426)+(x394);
x428 = (x364)+(x403);
x429 = (uintptr_t)((x428)<(x364));
x430 = (x429)+(x369);
x431 = (uintptr_t)((x430)<(x369));
x432 = (x430)+(x405);
x433 = (uintptr_t)((x432)<(x405));
x434 = (x431)+(x433);
x435 = (x434)+(x374);
x436 = (uintptr_t)((x435)<(x374));
x437 = (x435)+(x409);
x438 = (uintptr_t)((x437)<(x409));
x439 = (x436)+(x438);
x440 = (x439)+(x379);
x441 = (uintptr_t)((x440)<(x379));
x442 = (x440)+(x414);
x443 = (uintptr_t)((x442)<(x414));
x444 = (x441)+(x443);
x445 = (x444)+(x384);
x446 = (uintptr_t)((x445)<(x384));
x447 = (x445)+(x419);
x448 = (uintptr_t)((x447)<(x419));
x449 = (x446)+(x448);
x450 = (x449)+(x389);
x451 = (uintptr_t)((x450)<(x389));
x452 = (x450)+(x424);
x453 = (uintptr_t)((x452)<(x424));
x454 = (x451)+(x453);
x455 = (x454)+(x392);
x456 = (uintptr_t)((x455)<(x392));
x457 = (x455)+(x427);
x458 = (uintptr_t)((x457)<(x427));
x459 = (x456)+(x458);
x460 = (x428)*((uintptr_t)4294967297ULL);
x461 = (x460)*((uintptr_t)18446744073709551615ULL);
x462 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x460)*((uintptr_t)18446744073709551615ULL))>>32 : ((__uint128_t)(x460)*((uintptr_t)18446744073709551615ULL))>>64);
x463 = (x460)*((uintptr_t)18446744073709551615ULL);
x464 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x460)*((uintptr_t)18446744073709551615ULL))>>32 : ((__uint128_t)(x460)*((uintptr_t)18446744073709551615ULL))>>64);
x465 = (x460)*((uintptr_t)18446744073709551615ULL);
x466 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x460)*((uintptr_t)18446744073709551615ULL))>>32 : ((__uint128_t)(x460)*((uintptr_t)18446744073709551615ULL))>>64);
x467 = (x460)*((uintptr_t)18446744073709551614ULL);
x468 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x460)*((uintptr_t)18446744073709551614ULL))>>32 : ((__uint128_t)(x460)*((uintptr_t)18446744073709551614ULL))>>64);
x469 = (x460)*((uintptr_t)18446744069414584320ULL);
x470 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x460)*((uintptr_t)18446744069414584320ULL))>>32 : ((__uint128_t)(x460)*((uintptr_t)18446744069414584320ULL))>>64);
x471 = (x460)*((uintptr_t)4294967295ULL);
x472 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x460)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x460)*((uintptr_t)4294967295ULL))>>64);
x473 = (x472)+(x469);
x474 = (uintptr_t)((x473)<(x472));
x475 = (x474)+(x470);
x476 = (uintptr_t)((x475)<(x470));
x477 = (x475)+(x467);
x478 = (uintptr_t)((x477)<(x467));
x479 = (x476)+(x478);
x480 = (x479)+(x468);
x481 = (uintptr_t)((x480)<(x468));
x482 = (x480)+(x465);
x483 = (uintptr_t)((x482)<(x465));
x484 = (x481)+(x483);
x485 = (x484)+(x466);
x486 = (uintptr_t)((x485)<(x466));
x487 = (x485)+(x463);
x488 = (uintptr_t)((x487)<(x463));
x489 = (x486)+(x488);
x490 = (x489)+(x464);
x491 = (uintptr_t)((x490)<(x464));
x492 = (x490)+(x461);
x493 = (uintptr_t)((x492)<(x461));
x494 = (x491)+(x493);
x495 = (x494)+(x462);
x496 = (x428)+(x471);
x497 = (uintptr_t)((x496)<(x428));
x498 = (x497)+(x432);
x499 = (uintptr_t)((x498)<(x432));
x500 = (x498)+(x473);
x501 = (uintptr_t)((x500)<(x473));
x502 = (x499)+(x501);
x503 = (x502)+(x437);
x504 = (uintptr_t)((x503)<(x437));
x505 = (x503)+(x477);
x506 = (uintptr_t)((x505)<(x477));
x507 = (x504)+(x506);
x508 = (x507)+(x442);
x509 = (uintptr_t)((x508)<(x442));
x510 = (x508)+(x482);
x511 = (uintptr_t)((x510)<(x482));
x512 = (x509)+(x511);
x513 = (x512)+(x447);
x514 = (uintptr_t)((x513)<(x447));
x515 = (x513)+(x487);
x516 = (uintptr_t)((x515)<(x487));
x517 = (x514)+(x516);
x518 = (x517)+(x452);
x519 = (uintptr_t)((x518)<(x452));
x520 = (x518)+(x492);
x521 = (uintptr_t)((x520)<(x492));
x522 = (x519)+(x521);
x523 = (x522)+(x457);
x524 = (uintptr_t)((x523)<(x457));
x525 = (x523)+(x495);
x526 = (uintptr_t)((x525)<(x495));
x527 = (x524)+(x526);
x528 = (x527)+(x459);
x529 = (x15)*(x11);
x530 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x15)*(x11))>>32 : ((__uint128_t)(x15)*(x11))>>64);
x531 = (x15)*(x10);
x532 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x15)*(x10))>>32 : ((__uint128_t)(x15)*(x10))>>64);
x533 = (x15)*(x9);
x534 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x15)*(x9))>>32 : ((__uint128_t)(x15)*(x9))>>64);
x535 = (x15)*(x8);
x536 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x15)*(x8))>>32 : ((__uint128_t)(x15)*(x8))>>64);
x537 = (x15)*(x7);
x538 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x15)*(x7))>>32 : ((__uint128_t)(x15)*(x7))>>64);
x539 = (x15)*(x6);
x540 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x15)*(x6))>>32 : ((__uint128_t)(x15)*(x6))>>64);
x541 = (x540)+(x537);
x542 = (uintptr_t)((x541)<(x540));
x543 = (x542)+(x538);
x544 = (uintptr_t)((x543)<(x538));
x545 = (x543)+(x535);
x546 = (uintptr_t)((x545)<(x535));
x547 = (x544)+(x546);
x548 = (x547)+(x536);
x549 = (uintptr_t)((x548)<(x536));
x550 = (x548)+(x533);
x551 = (uintptr_t)((x550)<(x533));
x552 = (x549)+(x551);
x553 = (x552)+(x534);
x554 = (uintptr_t)((x553)<(x534));
x555 = (x553)+(x531);
x556 = (uintptr_t)((x555)<(x531));
x557 = (x554)+(x556);
x558 = (x557)+(x532);
x559 = (uintptr_t)((x558)<(x532));
x560 = (x558)+(x529);
x561 = (uintptr_t)((x560)<(x529));
x562 = (x559)+(x561);
x563 = (x562)+(x530);
x564 = (x500)+(x539);
x565 = (uintptr_t)((x564)<(x500));
x566 = (x565)+(x505);
x567 = (uintptr_t)((x566)<(x505));
x568 = (x566)+(x541);
x569 = (uintptr_t)((x568)<(x541));
x570 = (x567)+(x569);
x571 = (x570)+(x510);
x572 = (uintptr_t)((x571)<(x510));
x573 = (x571)+(x545);
x574 = (uintptr_t)((x573)<(x545));
x575 = (x572)+(x574);
x576 = (x575)+(x515);
x577 = (uintptr_t)((x576)<(x515));
x578 = (x576)+(x550);
x579 = (uintptr_t)((x578)<(x550));
x580 = (x577)+(x579);
x581 = (x580)+(x520);
x582 = (uintptr_t)((x581)<(x520));
x583 = (x581)+(x555);
x584 = (uintptr_t)((x583)<(x555));
x585 = (x582)+(x584);
x586 = (x585)+(x525);
x587 = (uintptr_t)((x586)<(x525));
x588 = (x586)+(x560);
x589 = (uintptr_t)((x588)<(x560));
x590 = (x587)+(x589);
x591 = (x590)+(x528);
x592 = (uintptr_t)((x591)<(x528));
x593 = (x591)+(x563);
x594 = (uintptr_t)((x593)<(x563));
x595 = (x592)+(x594);
x596 = (x564)*((uintptr_t)4294967297ULL);
x597 = (x596)*((uintptr_t)18446744073709551615ULL);
x598 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x596)*((uintptr_t)18446744073709551615ULL))>>32 : ((__uint128_t)(x596)*((uintptr_t)18446744073709551615ULL))>>64);
x599 = (x596)*((uintptr_t)18446744073709551615ULL);
x600 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x596)*((uintptr_t)18446744073709551615ULL))>>32 : ((__uint128_t)(x596)*((uintptr_t)18446744073709551615ULL))>>64);
x601 = (x596)*((uintptr_t)18446744073709551615ULL);
x602 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x596)*((uintptr_t)18446744073709551615ULL))>>32 : ((__uint128_t)(x596)*((uintptr_t)18446744073709551615ULL))>>64);
x603 = (x596)*((uintptr_t)18446744073709551614ULL);
x604 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x596)*((uintptr_t)18446744073709551614ULL))>>32 : ((__uint128_t)(x596)*((uintptr_t)18446744073709551614ULL))>>64);
x605 = (x596)*((uintptr_t)18446744069414584320ULL);
x606 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x596)*((uintptr_t)18446744069414584320ULL))>>32 : ((__uint128_t)(x596)*((uintptr_t)18446744069414584320ULL))>>64);
x607 = (x596)*((uintptr_t)4294967295ULL);
x608 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x596)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x596)*((uintptr_t)4294967295ULL))>>64);
x609 = (x608)+(x605);
x610 = (uintptr_t)((x609)<(x608));
x611 = (x610)+(x606);
x612 = (uintptr_t)((x611)<(x606));
x613 = (x611)+(x603);
x614 = (uintptr_t)((x613)<(x603));
x615 = (x612)+(x614);
x616 = (x615)+(x604);
x617 = (uintptr_t)((x616)<(x604));
x618 = (x616)+(x601);
x619 = (uintptr_t)((x618)<(x601));
x620 = (x617)+(x619);
x621 = (x620)+(x602);
x622 = (uintptr_t)((x621)<(x602));
x623 = (x621)+(x599);
x624 = (uintptr_t)((x623)<(x599));
x625 = (x622)+(x624);
x626 = (x625)+(x600);
x627 = (uintptr_t)((x626)<(x600));
x628 = (x626)+(x597);
x629 = (uintptr_t)((x628)<(x597));
x630 = (x627)+(x629);
x631 = (x630)+(x598);
x632 = (x564)+(x607);
x633 = (uintptr_t)((x632)<(x564));
x634 = (x633)+(x568);
x635 = (uintptr_t)((x634)<(x568));
x636 = (x634)+(x609);
x637 = (uintptr_t)((x636)<(x609));
x638 = (x635)+(x637);
x639 = (x638)+(x573);
x640 = (uintptr_t)((x639)<(x573));
x641 = (x639)+(x613);
x642 = (uintptr_t)((x641)<(x613));
x643 = (x640)+(x642);
x644 = (x643)+(x578);
x645 = (uintptr_t)((x644)<(x578));
x646 = (x644)+(x618);
x647 = (uintptr_t)((x646)<(x618));
x648 = (x645)+(x647);
x649 = (x648)+(x583);
x650 = (uintptr_t)((x649)<(x583));
x651 = (x649)+(x623);
x652 = (uintptr_t)((x651)<(x623));
x653 = (x650)+(x652);
x654 = (x653)+(x588);
x655 = (uintptr_t)((x654)<(x588));
x656 = (x654)+(x628);
x657 = (uintptr_t)((x656)<(x628));
x658 = (x655)+(x657);
x659 = (x658)+(x593);
x660 = (uintptr_t)((x659)<(x593));
x661 = (x659)+(x631);
x662 = (uintptr_t)((x661)<(x631));
x663 = (x660)+(x662);
x664 = (x663)+(x595);
x665 = (x16)*(x11);
x666 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x16)*(x11))>>32 : ((__uint128_t)(x16)*(x11))>>64);
x667 = (x16)*(x10);
x668 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x16)*(x10))>>32 : ((__uint128_t)(x16)*(x10))>>64);
x669 = (x16)*(x9);
x670 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x16)*(x9))>>32 : ((__uint128_t)(x16)*(x9))>>64);
x671 = (x16)*(x8);
x672 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x16)*(x8))>>32 : ((__uint128_t)(x16)*(x8))>>64);
x673 = (x16)*(x7);
x674 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x16)*(x7))>>32 : ((__uint128_t)(x16)*(x7))>>64);
x675 = (x16)*(x6);
x676 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x16)*(x6))>>32 : ((__uint128_t)(x16)*(x6))>>64);
x677 = (x676)+(x673);
x678 = (uintptr_t)((x677)<(x676));
x679 = (x678)+(x674);
x680 = (uintptr_t)((x679)<(x674));
x681 = (x679)+(x671);
x682 = (uintptr_t)((x681)<(x671));
x683 = (x680)+(x682);
x684 = (x683)+(x672);
x685 = (uintptr_t)((x684)<(x672));
x686 = (x684)+(x669);
x687 = (uintptr_t)((x686)<(x669));
x688 = (x685)+(x687);
x689 = (x688)+(x670);
x690 = (uintptr_t)((x689)<(x670));
x691 = (x689)+(x667);
x692 = (uintptr_t)((x691)<(x667));
x693 = (x690)+(x692);
x694 = (x693)+(x668);
x695 = (uintptr_t)((x694)<(x668));
x696 = (x694)+(x665);
x697 = (uintptr_t)((x696)<(x665));
x698 = (x695)+(x697);
x699 = (x698)+(x666);
x700 = (x636)+(x675);
x701 = (uintptr_t)((x700)<(x636));
x702 = (x701)+(x641);
x703 = (uintptr_t)((x702)<(x641));
x704 = (x702)+(x677);
x705 = (uintptr_t)((x704)<(x677));
x706 = (x703)+(x705);
x707 = (x706)+(x646);
x708 = (uintptr_t)((x707)<(x646));
x709 = (x707)+(x681);
x710 = (uintptr_t)((x709)<(x681));
x711 = (x708)+(x710);
x712 = (x711)+(x651);
x713 = (uintptr_t)((x712)<(x651));
x714 = (x712)+(x686);
x715 = (uintptr_t)((x714)<(x686));
x716 = (x713)+(x715);
x717 = (x716)+(x656);
x718 = (uintptr_t)((x717)<(x656));
x719 = (x717)+(x691);
x720 = (uintptr_t)((x719)<(x691));
x721 = (x718)+(x720);
x722 = (x721)+(x661);
x723 = (uintptr_t)((x722)<(x661));
x724 = (x722)+(x696);
x725 = (uintptr_t)((x724)<(x696));
x726 = (x723)+(x725);
x727 = (x726)+(x664);
x728 = (uintptr_t)((x727)<(x664));
x729 = (x727)+(x699);
x730 = (uintptr_t)((x729)<(x699));
x731 = (x728)+(x730);
x732 = (x700)*((uintptr_t)4294967297ULL);
x733 = (x732)*((uintptr_t)18446744073709551615ULL);
x734 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x732)*((uintptr_t)18446744073709551615ULL))>>32 : ((__uint128_t)(x732)*((uintptr_t)18446744073709551615ULL))>>64);
x735 = (x732)*((uintptr_t)18446744073709551615ULL);
x736 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x732)*((uintptr_t)18446744073709551615ULL))>>32 : ((__uint128_t)(x732)*((uintptr_t)18446744073709551615ULL))>>64);
x737 = (x732)*((uintptr_t)18446744073709551615ULL);
x738 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x732)*((uintptr_t)18446744073709551615ULL))>>32 : ((__uint128_t)(x732)*((uintptr_t)18446744073709551615ULL))>>64);
x739 = (x732)*((uintptr_t)18446744073709551614ULL);
x740 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x732)*((uintptr_t)18446744073709551614ULL))>>32 : ((__uint128_t)(x732)*((uintptr_t)18446744073709551614ULL))>>64);
x741 = (x732)*((uintptr_t)18446744069414584320ULL);
x742 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x732)*((uintptr_t)18446744069414584320ULL))>>32 : ((__uint128_t)(x732)*((uintptr_t)18446744069414584320ULL))>>64);
x743 = (x732)*((uintptr_t)4294967295ULL);
x744 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x732)*((uintptr_t)4294967295ULL))>>32 : ((__uint128_t)(x732)*((uintptr_t)4294967295ULL))>>64);
x745 = (x744)+(x741);
x746 = (uintptr_t)((x745)<(x744));
x747 = (x746)+(x742);
x748 = (uintptr_t)((x747)<(x742));
x749 = (x747)+(x739);
x750 = (uintptr_t)((x749)<(x739));
x751 = (x748)+(x750);
x752 = (x751)+(x740);
x753 = (uintptr_t)((x752)<(x740));
x754 = (x752)+(x737);
x755 = (uintptr_t)((x754)<(x737));
x756 = (x753)+(x755);
x757 = (x756)+(x738);
x758 = (uintptr_t)((x757)<(x738));
x759 = (x757)+(x735);
x760 = (uintptr_t)((x759)<(x735));
x761 = (x758)+(x760);
x762 = (x761)+(x736);
x763 = (uintptr_t)((x762)<(x736));
x764 = (x762)+(x733);
x765 = (uintptr_t)((x764)<(x733));
x766 = (x763)+(x765);
x767 = (x766)+(x734);
x768 = (x700)+(x743);
x769 = (uintptr_t)((x768)<(x700));
x770 = (x769)+(x704);
x771 = (uintptr_t)((x770)<(x704));
x772 = (x770)+(x745);
x773 = (uintptr_t)((x772)<(x745));
x774 = (x771)+(x773);
x775 = (x774)+(x709);
x776 = (uintptr_t)((x775)<(x709));
x777 = (x775)+(x749);
x778 = (uintptr_t)((x777)<(x749));
x779 = (x776)+(x778);
x780 = (x779)+(x714);
x781 = (uintptr_t)((x780)<(x714));
x782 = (x780)+(x754);
x783 = (uintptr_t)((x782)<(x754));
x784 = (x781)+(x783);
x785 = (x784)+(x719);
x786 = (uintptr_t)((x785)<(x719));
x787 = (x785)+(x759);
x788 = (uintptr_t)((x787)<(x759));
x789 = (x786)+(x788);
x790 = (x789)+(x724);
x791 = (uintptr_t)((x790)<(x724));
x792 = (x790)+(x764);
x793 = (uintptr_t)((x792)<(x764));
x794 = (x791)+(x793);
x795 = (x794)+(x729);
x796 = (uintptr_t)((x795)<(x729));
x797 = (x795)+(x767);
x798 = (uintptr_t)((x797)<(x767));
x799 = (x796)+(x798);
x800 = (x799)+(x731);
x801 = (x772)-((uintptr_t)4294967295ULL);
x802 = (uintptr_t)((x772)<(x801));
x803 = (x777)-((uintptr_t)18446744069414584320ULL);
x804 = (uintptr_t)((x777)<(x803));
x805 = (x803)-(x802);
x806 = (uintptr_t)((x803)<(x805));
x807 = (x804)+(x806);
x808 = (x782)-((uintptr_t)18446744073709551614ULL);
x809 = (uintptr_t)((x782)<(x808));
x810 = (x808)-(x807);
x811 = (uintptr_t)((x808)<(x810));
x812 = (x809)+(x811);
x813 = (x787)-((uintptr_t)18446744073709551615ULL);
x814 = (uintptr_t)((x787)<(x813));
x815 = (x813)-(x812);
x816 = (uintptr_t)((x813)<(x815));
x817 = (x814)+(x816);
x818 = (x792)-((uintptr_t)18446744073709551615ULL);
x819 = (uintptr_t)((x792)<(x818));
x820 = (x818)-(x817);
x821 = (uintptr_t)((x818)<(x820));
x822 = (x819)+(x821);
x823 = (x797)-((uintptr_t)18446744073709551615ULL);
x824 = (uintptr_t)((x797)<(x823));
x825 = (x823)-(x822);
x826 = (uintptr_t)((x823)<(x825));
x827 = (x824)+(x826);
x828 = (x800)-(x827);
x829 = (uintptr_t)((x800)<(x828));
x830 = ((uintptr_t)-1ULL)+((uintptr_t)((x829)==((uintptr_t)0ULL)));
x831 = (x830)^((uintptr_t)18446744073709551615ULL);
x832 = ((x772)&(x830))|((x801)&(x831));
x833 = ((uintptr_t)-1ULL)+((uintptr_t)((x829)==((uintptr_t)0ULL)));
x834 = (x833)^((uintptr_t)18446744073709551615ULL);
x835 = ((x777)&(x833))|((x805)&(x834));
x836 = ((uintptr_t)-1ULL)+((uintptr_t)((x829)==((uintptr_t)0ULL)));
x837 = (x836)^((uintptr_t)18446744073709551615ULL);
x838 = ((x782)&(x836))|((x810)&(x837));
x839 = ((uintptr_t)-1ULL)+((uintptr_t)((x829)==((uintptr_t)0ULL)));
x840 = (x839)^((uintptr_t)18446744073709551615ULL);
x841 = ((x787)&(x839))|((x815)&(x840));
x842 = ((uintptr_t)-1ULL)+((uintptr_t)((x829)==((uintptr_t)0ULL)));
x843 = (x842)^((uintptr_t)18446744073709551615ULL);
x844 = ((x792)&(x842))|((x820)&(x843));
x845 = ((uintptr_t)-1ULL)+((uintptr_t)((x829)==((uintptr_t)0ULL)));
x846 = (x845)^((uintptr_t)18446744073709551615ULL);
x847 = ((x797)&(x845))|((x825)&(x846));
x848 = x832;
x849 = x835;
x850 = x838;
x851 = x841;
x852 = x844;
x853 = x847;
/*skip*/
_br2_store((out0)+((uintptr_t)0ULL), x848, sizeof(uintptr_t));
_br2_store((out0)+((uintptr_t)8ULL), x849, sizeof(uintptr_t));
_br2_store((out0)+((uintptr_t)16ULL), x850, sizeof(uintptr_t));
_br2_store((out0)+((uintptr_t)24ULL), x851, sizeof(uintptr_t));
_br2_store((out0)+((uintptr_t)32ULL), x852, sizeof(uintptr_t));
_br2_store((out0)+((uintptr_t)40ULL), x853, sizeof(uintptr_t));
/*skip*/
return;
}
/* NOTE: The following wrapper function is not covered by Coq proofs */
static void fiat_p384_mul(uint64_t out1[6], const uint64_t arg1[6], const uint64_t arg2[6]) {
internal_fiat_p384_mul((uintptr_t)out1, (uintptr_t)arg1, (uintptr_t)arg2);
}
/*
* Input Bounds:
* in0: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
* Output Bounds:
* out0: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
*/
static
void internal_fiat_p384_square(uintptr_t out0, uintptr_t in0) {
uintptr_t x11, x20, x23, x25, x21, x26, x18, x27, x29, x30, x19, x31, x16, x32, x34, x35, x17, x36, x14, x37, x39, x40, x15, x41, x12, x42, x44, x45, x13, x47, x56, x59, x61, x57, x62, x54, x63, x65, x66, x55, x67, x52, x68, x70, x71, x53, x72, x50, x73, x75, x76, x51, x77, x48, x78, x80, x81, x49, x58, x83, x22, x84, x24, x85, x60, x86, x88, x89, x28, x90, x64, x91, x93, x94, x33, x95, x69, x96, x98, x99, x38, x100, x74, x101, x103, x104, x43, x105, x79, x106, x108, x109, x46, x110, x82, x111, x113, x6, x123, x126, x128, x124, x129, x121, x130, x132, x133, x122, x134, x119, x135, x137, x138, x120, x139, x117, x140, x142, x143, x118, x144, x115, x145, x147, x148, x116, x125, x87, x151, x92, x152, x127, x153, x155, x156, x97, x157, x131, x158, x160, x161, x102, x162, x136, x163, x165, x166, x107, x167, x141, x168, x170, x171, x112, x172, x146, x173, x175, x176, x114, x177, x149, x178, x180, x182, x191, x194, x196, x192, x197, x189, x198, x200, x201, x190, x202, x187, x203, x205, x206, x188, x207, x185, x208, x210, x211, x186, x212, x183, x213, x215, x216, x184, x193, x218, x150, x219, x154, x220, x195, x221, x223, x224, x159, x225, x199, x226, x228, x229, x164, x230, x204, x231, x233, x234, x169, x235, x209, x236, x238, x239, x174, x240, x214, x241, x243, x244, x179, x245, x217, x246, x248, x249, x181, x7, 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, x261, x222, x287, x227, x288, x263, x289, x291, x292, x232, x293, x267, x294, x296, x297, x237, x298, x272, x299, x301, x302, x242, x303, x277, x304, x306, x307, x247, x308, x282, x309, x311, x312, x250, x313, x285, x314, x316, x318, x327, x330, x332, x328, x333, x325, x334, x336, x337, x326, x338, x323, x339, x341, x342, x324, x343, x321, x344, x346, x347, x322, x348, x319, x349, x351, x352, x320, x329, x354, x286, x355, x290, x356, x331, x357, x359, x360, x295, x361, x335, x362, x364, x365, x300, x366, x340, x367, x369, x370, x305, x371, x345, x372, x374, x375, x310, x376, x350, x377, x379, x380, x315, x381, x353, x382, x384, x385, x317, x8, x395, x398, x400, x396, x401, x393, x402, x404, x405, x394, x406, x391, x407, x409, x410, x392, x411, x389, x412, x414, x415, x390, x416, x387, x417, x419, x420, x388, x397, x358, x423, x363, x424, x399, x425, x427, x428, x368, x429, x403, x430, x432, x433, x373, x434, x408, x435, x437, x438, x378, x439, x413, x440, x442, x443, x383, x444, x418, x445, x447, x448, x386, x449, x421, x450, x452, x454, x463, x466, x468, x464, x469, x461, x470, x472, x473, x462, x474, x459, x475, x477, x478, x460, x479, x457, x480, x482, x483, x458, x484, x455, x485, x487, x488, x456, x465, x490, x422, x491, x426, x492, x467, x493, x495, x496, x431, x497, x471, x498, x500, x501, x436, x502, x476, x503, x505, x506, x441, x507, x481, x508, x510, x511, x446, x512, x486, x513, x515, x516, x451, x517, x489, x518, x520, x521, x453, x9, x531, x534, x536, x532, x537, x529, x538, x540, x541, x530, x542, x527, x543, x545, x546, x528, x547, x525, x548, x550, x551, x526, x552, x523, x553, x555, x556, x524, x533, x494, x559, x499, x560, x535, x561, x563, x564, x504, x565, x539, x566, x568, x569, x509, x570, x544, x571, x573, x574, x514, x575, x549, x576, x578, x579, x519, x580, x554, x581, x583, x584, x522, x585, x557, x586, x588, x590, x599, x602, x604, x600, x605, x597, x606, x608, x609, x598, x610, x595, x611, x613, x614, x596, x615, x593, x616, x618, x619, x594, x620, x591, x621, x623, x624, x592, x601, x626, x558, x627, x562, x628, x603, x629, x631, x632, x567, x633, x607, x634, x636, x637, x572, x638, x612, x639, x641, x642, x577, x643, x617, x644, x646, x647, x582, x648, x622, x649, x651, x652, x587, x653, x625, x654, x656, x657, x589, x5, x4, x3, x2, x1, x10, x0, x667, x670, x672, x668, x673, x665, x674, x676, x677, x666, x678, x663, x679, x681, x682, x664, x683, x661, x684, x686, x687, x662, x688, x659, x689, x691, x692, x660, x669, x630, x695, x635, x696, x671, x697, x699, x700, x640, x701, x675, x702, x704, x705, x645, x706, x680, x707, x709, x710, x650, x711, x685, x712, x714, x715, x655, x716, x690, x717, x719, x720, x658, x721, x693, x722, x724, x726, x735, x738, x740, x736, x741, x733, x742, x744, x745, x734, x746, x731, x747, x749, x750, x732, x751, x729, x752, x754, x755, x730, x756, x727, x757, x759, x760, x728, x737, x762, x694, x763, x698, x764, x739, x765, x767, x768, x703, x769, x743, x770, x772, x773, x708, x774, x748, x775, x777, x778, x713, x779, x753, x780, x782, x783, x718, x784, x758, x785, x787, x788, x723, x789, x761, x790, x792, x793, x725, x796, x797, x798, x800, x801, x802, x803, x805, x806, x807, x808, x810, x811, x812, x813, x815, x816, x817, x818, x820, x821, x794, x822, x766, x824, x795, x825, x771, x827, x799, x828, x776, x830, x804, x831, x781, x833, x809, x834, x786, x836, x814, x837, x823, x791, x839, x819, x840, x826, x829, x832, x835, x838, x841, x842, x843, x844, x845, x846, x847;
x0 = _br2_load((in0)+((uintptr_t)0ULL), sizeof(uintptr_t));
x1 = _br2_load((in0)+((uintptr_t)8ULL), sizeof(uintptr_t));
x2 = _br2_load((in0)+((uintptr_t)16ULL), sizeof(uintptr_t));
x3 = _br2_load((in0)+((uintptr_t)24ULL), sizeof(uintptr_t));
x4 = _br2_load((in0)+((uintptr_t)32ULL), sizeof(uintptr_t));
x5 = _br2_load((in0)+((uintptr_t)40ULL), sizeof(uintptr_t));
/*skip*/
/*skip*/
x6 = x1;
x7 = x2;
x8 = x3;
x9 = x4;
x10 = x5;
x11 = x0;
x12 = (x11)*(x5);
x13 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x11)*(x5))>>32 : ((__uint128_t)(x11)*(x5))>>64);
x14 = (x11)*(x4);
x15 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x11)*(x4))>>32 : ((__uint128_t)(x11)*(x4))>>64);
x16 = (x11)*(x3);
x17 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x11)*(x3))>>32 : ((__uint128_t)(x11)*(x3))>>64);
x18 = (x11)*(x2);
x19 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x11)*(x2))>>32 : ((__uint128_t)(x11)*(x2))>>64);
x20 = (x11)*(x1);
x21 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x11)*(x1))>>32 : ((__uint128_t)(x11)*(x1))>>64);
x22 = (x11)*(x0);
x23 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x11)*(x0))>>32 : ((__uint128_t)(x11)*(x0))>>64);
x24 = (x23)+(x20);
x25 = (uintptr_t)((x24)<(x23));
x26 = (x25)+(x21);
x27 = (uintptr_t)((x26)<(x21));
x28 = (x26)+(x18);
x29 = (uintptr_t)((x28)<(x18));
x30 = (x27)+(x29);
x31 = (x30)+(x19);
x32 = (uintptr_t)((x31)<(x19));
x33 = (x31)+(x16);
x34 = (uintptr_t)((x33)<(x16));
x35 = (x32)+(x34);
x36 = (x35)+(x17);
x37 = (uintptr_t)((x36)<(x17));
x38 = (x36)+(x14);
x39 = (uintptr_t)((x38)<(x14));
x40 = (x37)+(x39);
x41 = (x40)+(x15);
x42 = (uintptr_t)((x41)<(x15));
x43 = (x41)+(x12);
x44 = (uintptr_t)((x43)<(x12));
x45 = (x42)+(x44);
x46 = (x45)+(x13);
x47 = (x22)*((uintptr_t)4294967297ULL);
x48 = (x47)*((uintptr_t)18446744073709551615ULL);
x49 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x47)*((uintptr_t)18446744073709551615ULL))>>32 : ((__uint128_t)(x47)*((uintptr_t)18446744073709551615ULL))>>64);
x50 = (x47)*((uintptr_t)18446744073709551615ULL);
x51 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x47)*((uintptr_t)18446744073709551615ULL))>>32 : ((__uint128_t)(x47)*((uintptr_t)18446744073709551615ULL))>>64);
x52 = (x47)*((uintptr_t)18446744073709551615ULL);
x53 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x47)*((uintptr_t)18446744073709551615ULL))>>32 : ((__uint128_t)(x47)*((uintptr_t)18446744073709551615ULL))>>64);
x54 = (x47)*((uintptr_t)18446744073709551614ULL);
x55 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x47)*((uintptr_t)18446744073709551614ULL))>>32 : ((__uint128_t)(x47)*((uintptr_t)18446744073709551614ULL))>>64);
x56 = (x47)*((uintptr_t)18446744069414584320ULL);
x57 = (uintptr_t)(sizeof(intptr_t) == 4 ? ((uint64_t)(x47)*((uintptr_t)18446744069414584320ULL))>>32 : ((__uint128_t)(x47)*((uintptr_t)18446744069414584320ULL))>>64);