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