forked from mit-plv/fiat-crypto
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathp521_64.c
1995 lines (1962 loc) · 90.9 KB
/
p521_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_unsaturated_solinas --lang bedrock2 --static --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select p521 64 9 '2^521 - 1' carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes */
/* curve description: p521 */
/* machine_wordsize = 64 (from "64") */
/* requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes */
/* n = 9 (from "9") */
/* s-c = 2^521 - [(1, 1)] (from "2^521 - 1") */
/* tight_bounds_multiplier = 1 (from "") */
/* */
/* Computed values: */
/* carry_chain = [0, 1, 2, 3, 4, 5, 6, 7, 8, 0, 1] */
/* eval z = z[0] + (z[1] << 58) + (z[2] << 116) + (z[3] << 174) + (z[4] << 232) + (z[5] << 0x122) + (z[6] << 0x15c) + (z[7] << 0x196) + (z[8] << 0x1d0) */
/* 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) + (z[48] << 0x180) + (z[49] << 0x188) + (z[50] << 0x190) + (z[51] << 0x198) + (z[52] << 0x1a0) + (z[53] << 0x1a8) + (z[54] << 0x1b0) + (z[55] << 0x1b8) + (z[56] << 0x1c0) + (z[57] << 0x1c8) + (z[58] << 0x1d0) + (z[59] << 0x1d8) + (z[60] << 0x1e0) + (z[61] << 0x1e8) + (z[62] << 0x1f0) + (z[63] << 0x1f8) + (z[64] << 2^9) + (z[65] << 0x208) */
/* balance = [0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x3fffffffffffffe] */
#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 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]]
* in1: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]]
* Output Bounds:
* out0: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]]
*/
static
void internal_fiat_p521_carry_mul(uintptr_t out0, uintptr_t in0, uintptr_t in1) {
uintptr_t x8, x7, x6, x5, x4, x3, x2, x1, x17, x16, x15, x14, x13, x12, x11, x10, x0, x9, x32, x46, x181, x47, x182, x33, x180, x58, x185, x59, x186, x183, x184, x68, x189, x69, x190, x187, x188, x76, x193, x77, x194, x191, x192, x82, x197, x83, x198, x195, x196, x86, x201, x87, x202, x199, x200, x88, x205, x89, x206, x203, x204, x178, x209, x179, x210, x207, x211, x208, x90, x92, x216, x93, x217, x91, x215, x96, x220, x97, x221, x218, x219, x102, x224, x103, x225, x222, x223, x110, x228, x111, x229, x226, x227, x120, x232, x121, x233, x230, x231, x132, x236, x133, x237, x234, x235, x146, x240, x147, x241, x238, x239, x162, x244, x163, x245, x242, x18, x94, x248, x95, x249, x19, x247, x98, x252, x99, x253, x250, x251, x104, x256, x105, x257, x254, x255, x112, x260, x113, x261, x258, x259, x122, x264, x123, x265, x262, x263, x134, x268, x135, x269, x266, x267, x148, x272, x149, x273, x270, x271, x164, x276, x165, x277, x274, x20, x34, x280, x35, x281, x21, x279, x100, x284, x101, x285, x282, x283, x106, x288, x107, x289, x286, x287, x114, x292, x115, x293, x290, x291, x124, x296, x125, x297, x294, x295, x136, x300, x137, x301, x298, x299, x150, x304, x151, x305, x302, x303, x166, x308, x167, x309, x306, x22, x36, x312, x37, x313, x23, x311, x48, x316, x49, x317, x314, x315, x108, x320, x109, x321, x318, x319, x116, x324, x117, x325, x322, x323, x126, x328, x127, x329, x326, x327, x138, x332, x139, x333, x330, x331, x152, x336, x153, x337, x334, x335, x168, x340, x169, x341, x338, x24, x38, x344, x39, x345, x25, x343, x50, x348, x51, x349, x346, x347, x60, x352, x61, x353, x350, x351, x118, x356, x119, x357, x354, x355, x128, x360, x129, x361, x358, x359, x140, x364, x141, x365, x362, x363, x154, x368, x155, x369, x366, x367, x170, x372, x171, x373, x370, x26, x40, x376, x41, x377, x27, x375, x52, x380, x53, x381, x378, x379, x62, x384, x63, x385, x382, x383, x70, x388, x71, x389, x386, x387, x130, x392, x131, x393, x390, x391, x142, x396, x143, x397, x394, x395, x156, x400, x157, x401, x398, x399, x172, x404, x173, x405, x402, x28, x42, x408, x43, x409, x29, x407, x54, x412, x55, x413, x410, x411, x64, x416, x65, x417, x414, x415, x72, x420, x73, x421, x418, x419, x78, x424, x79, x425, x422, x423, x144, x428, x145, x429, x426, x427, x158, x432, x159, x433, x430, x431, x174, x436, x175, x437, x434, x30, x44, x440, x45, x441, x31, x439, x56, x444, x57, x445, x442, x443, x66, x448, x67, x449, x446, x447, x74, x452, x75, x453, x450, x451, x80, x456, x81, x457, x454, x455, x84, x460, x85, x461, x458, x459, x160, x464, x161, x465, x462, x463, x176, x468, x177, x469, x466, x467, x212, x472, x213, x473, x470, x474, x471, x435, x475, x479, x476, x480, x438, x481, x478, x403, x482, x486, x483, x487, x406, x488, x485, x371, x489, x493, x490, x494, x374, x495, x492, x339, x496, x500, x497, x501, x342, x502, x499, x307, x503, x507, x504, x508, x310, x509, x506, x275, x510, x514, x511, x515, x278, x516, x513, x243, x517, x521, x518, x522, x246, x523, x520, x524, x214, x528, x525, x529, x527, x530, x477, x532, x533, x484, x531, x534, x535, x491, x498, x505, x512, x519, x526, x536, x537, x538, x539, x540, x541, x542, x543, x544;
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));
x6 = _br2_load((in0)+((uintptr_t)48ULL), sizeof(uintptr_t));
x7 = _br2_load((in0)+((uintptr_t)56ULL), sizeof(uintptr_t));
x8 = _br2_load((in0)+((uintptr_t)64ULL), sizeof(uintptr_t));
/*skip*/
x9 = _br2_load((in1)+((uintptr_t)0ULL), sizeof(uintptr_t));
x10 = _br2_load((in1)+((uintptr_t)8ULL), sizeof(uintptr_t));
x11 = _br2_load((in1)+((uintptr_t)16ULL), sizeof(uintptr_t));
x12 = _br2_load((in1)+((uintptr_t)24ULL), sizeof(uintptr_t));
x13 = _br2_load((in1)+((uintptr_t)32ULL), sizeof(uintptr_t));
x14 = _br2_load((in1)+((uintptr_t)40ULL), sizeof(uintptr_t));
x15 = _br2_load((in1)+((uintptr_t)48ULL), sizeof(uintptr_t));
x16 = _br2_load((in1)+((uintptr_t)56ULL), sizeof(uintptr_t));
x17 = _br2_load((in1)+((uintptr_t)64ULL), sizeof(uintptr_t));
/*skip*/
/*skip*/
x18 = (x8)*((x17)*((uintptr_t)2ULL));
x19 = sizeof(intptr_t) == 4 ? ((uint64_t)(x8)*((x17)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x8)*((x17)*((uintptr_t)2ULL)))>>64;
x20 = (x8)*((x16)*((uintptr_t)2ULL));
x21 = sizeof(intptr_t) == 4 ? ((uint64_t)(x8)*((x16)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x8)*((x16)*((uintptr_t)2ULL)))>>64;
x22 = (x8)*((x15)*((uintptr_t)2ULL));
x23 = sizeof(intptr_t) == 4 ? ((uint64_t)(x8)*((x15)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x8)*((x15)*((uintptr_t)2ULL)))>>64;
x24 = (x8)*((x14)*((uintptr_t)2ULL));
x25 = sizeof(intptr_t) == 4 ? ((uint64_t)(x8)*((x14)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x8)*((x14)*((uintptr_t)2ULL)))>>64;
x26 = (x8)*((x13)*((uintptr_t)2ULL));
x27 = sizeof(intptr_t) == 4 ? ((uint64_t)(x8)*((x13)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x8)*((x13)*((uintptr_t)2ULL)))>>64;
x28 = (x8)*((x12)*((uintptr_t)2ULL));
x29 = sizeof(intptr_t) == 4 ? ((uint64_t)(x8)*((x12)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x8)*((x12)*((uintptr_t)2ULL)))>>64;
x30 = (x8)*((x11)*((uintptr_t)2ULL));
x31 = sizeof(intptr_t) == 4 ? ((uint64_t)(x8)*((x11)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x8)*((x11)*((uintptr_t)2ULL)))>>64;
x32 = (x8)*((x10)*((uintptr_t)2ULL));
x33 = sizeof(intptr_t) == 4 ? ((uint64_t)(x8)*((x10)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x8)*((x10)*((uintptr_t)2ULL)))>>64;
x34 = (x7)*((x17)*((uintptr_t)2ULL));
x35 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*((x17)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x7)*((x17)*((uintptr_t)2ULL)))>>64;
x36 = (x7)*((x16)*((uintptr_t)2ULL));
x37 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*((x16)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x7)*((x16)*((uintptr_t)2ULL)))>>64;
x38 = (x7)*((x15)*((uintptr_t)2ULL));
x39 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*((x15)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x7)*((x15)*((uintptr_t)2ULL)))>>64;
x40 = (x7)*((x14)*((uintptr_t)2ULL));
x41 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*((x14)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x7)*((x14)*((uintptr_t)2ULL)))>>64;
x42 = (x7)*((x13)*((uintptr_t)2ULL));
x43 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*((x13)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x7)*((x13)*((uintptr_t)2ULL)))>>64;
x44 = (x7)*((x12)*((uintptr_t)2ULL));
x45 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*((x12)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x7)*((x12)*((uintptr_t)2ULL)))>>64;
x46 = (x7)*((x11)*((uintptr_t)2ULL));
x47 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*((x11)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x7)*((x11)*((uintptr_t)2ULL)))>>64;
x48 = (x6)*((x17)*((uintptr_t)2ULL));
x49 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*((x17)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x6)*((x17)*((uintptr_t)2ULL)))>>64;
x50 = (x6)*((x16)*((uintptr_t)2ULL));
x51 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*((x16)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x6)*((x16)*((uintptr_t)2ULL)))>>64;
x52 = (x6)*((x15)*((uintptr_t)2ULL));
x53 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*((x15)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x6)*((x15)*((uintptr_t)2ULL)))>>64;
x54 = (x6)*((x14)*((uintptr_t)2ULL));
x55 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*((x14)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x6)*((x14)*((uintptr_t)2ULL)))>>64;
x56 = (x6)*((x13)*((uintptr_t)2ULL));
x57 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*((x13)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x6)*((x13)*((uintptr_t)2ULL)))>>64;
x58 = (x6)*((x12)*((uintptr_t)2ULL));
x59 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*((x12)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x6)*((x12)*((uintptr_t)2ULL)))>>64;
x60 = (x5)*((x17)*((uintptr_t)2ULL));
x61 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*((x17)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x5)*((x17)*((uintptr_t)2ULL)))>>64;
x62 = (x5)*((x16)*((uintptr_t)2ULL));
x63 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*((x16)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x5)*((x16)*((uintptr_t)2ULL)))>>64;
x64 = (x5)*((x15)*((uintptr_t)2ULL));
x65 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*((x15)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x5)*((x15)*((uintptr_t)2ULL)))>>64;
x66 = (x5)*((x14)*((uintptr_t)2ULL));
x67 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*((x14)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x5)*((x14)*((uintptr_t)2ULL)))>>64;
x68 = (x5)*((x13)*((uintptr_t)2ULL));
x69 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*((x13)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x5)*((x13)*((uintptr_t)2ULL)))>>64;
x70 = (x4)*((x17)*((uintptr_t)2ULL));
x71 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*((x17)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x4)*((x17)*((uintptr_t)2ULL)))>>64;
x72 = (x4)*((x16)*((uintptr_t)2ULL));
x73 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*((x16)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x4)*((x16)*((uintptr_t)2ULL)))>>64;
x74 = (x4)*((x15)*((uintptr_t)2ULL));
x75 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*((x15)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x4)*((x15)*((uintptr_t)2ULL)))>>64;
x76 = (x4)*((x14)*((uintptr_t)2ULL));
x77 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*((x14)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x4)*((x14)*((uintptr_t)2ULL)))>>64;
x78 = (x3)*((x17)*((uintptr_t)2ULL));
x79 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*((x17)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x3)*((x17)*((uintptr_t)2ULL)))>>64;
x80 = (x3)*((x16)*((uintptr_t)2ULL));
x81 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*((x16)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x3)*((x16)*((uintptr_t)2ULL)))>>64;
x82 = (x3)*((x15)*((uintptr_t)2ULL));
x83 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*((x15)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x3)*((x15)*((uintptr_t)2ULL)))>>64;
x84 = (x2)*((x17)*((uintptr_t)2ULL));
x85 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*((x17)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x2)*((x17)*((uintptr_t)2ULL)))>>64;
x86 = (x2)*((x16)*((uintptr_t)2ULL));
x87 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*((x16)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x2)*((x16)*((uintptr_t)2ULL)))>>64;
x88 = (x1)*((x17)*((uintptr_t)2ULL));
x89 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*((x17)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x1)*((x17)*((uintptr_t)2ULL)))>>64;
x90 = (x8)*(x9);
x91 = sizeof(intptr_t) == 4 ? ((uint64_t)(x8)*(x9))>>32 : ((__uint128_t)(x8)*(x9))>>64;
x92 = (x7)*(x10);
x93 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*(x10))>>32 : ((__uint128_t)(x7)*(x10))>>64;
x94 = (x7)*(x9);
x95 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*(x9))>>32 : ((__uint128_t)(x7)*(x9))>>64;
x96 = (x6)*(x11);
x97 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*(x11))>>32 : ((__uint128_t)(x6)*(x11))>>64;
x98 = (x6)*(x10);
x99 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*(x10))>>32 : ((__uint128_t)(x6)*(x10))>>64;
x100 = (x6)*(x9);
x101 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*(x9))>>32 : ((__uint128_t)(x6)*(x9))>>64;
x102 = (x5)*(x12);
x103 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*(x12))>>32 : ((__uint128_t)(x5)*(x12))>>64;
x104 = (x5)*(x11);
x105 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*(x11))>>32 : ((__uint128_t)(x5)*(x11))>>64;
x106 = (x5)*(x10);
x107 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*(x10))>>32 : ((__uint128_t)(x5)*(x10))>>64;
x108 = (x5)*(x9);
x109 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*(x9))>>32 : ((__uint128_t)(x5)*(x9))>>64;
x110 = (x4)*(x13);
x111 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*(x13))>>32 : ((__uint128_t)(x4)*(x13))>>64;
x112 = (x4)*(x12);
x113 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*(x12))>>32 : ((__uint128_t)(x4)*(x12))>>64;
x114 = (x4)*(x11);
x115 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*(x11))>>32 : ((__uint128_t)(x4)*(x11))>>64;
x116 = (x4)*(x10);
x117 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*(x10))>>32 : ((__uint128_t)(x4)*(x10))>>64;
x118 = (x4)*(x9);
x119 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*(x9))>>32 : ((__uint128_t)(x4)*(x9))>>64;
x120 = (x3)*(x14);
x121 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*(x14))>>32 : ((__uint128_t)(x3)*(x14))>>64;
x122 = (x3)*(x13);
x123 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*(x13))>>32 : ((__uint128_t)(x3)*(x13))>>64;
x124 = (x3)*(x12);
x125 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*(x12))>>32 : ((__uint128_t)(x3)*(x12))>>64;
x126 = (x3)*(x11);
x127 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*(x11))>>32 : ((__uint128_t)(x3)*(x11))>>64;
x128 = (x3)*(x10);
x129 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*(x10))>>32 : ((__uint128_t)(x3)*(x10))>>64;
x130 = (x3)*(x9);
x131 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*(x9))>>32 : ((__uint128_t)(x3)*(x9))>>64;
x132 = (x2)*(x15);
x133 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*(x15))>>32 : ((__uint128_t)(x2)*(x15))>>64;
x134 = (x2)*(x14);
x135 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*(x14))>>32 : ((__uint128_t)(x2)*(x14))>>64;
x136 = (x2)*(x13);
x137 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*(x13))>>32 : ((__uint128_t)(x2)*(x13))>>64;
x138 = (x2)*(x12);
x139 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*(x12))>>32 : ((__uint128_t)(x2)*(x12))>>64;
x140 = (x2)*(x11);
x141 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*(x11))>>32 : ((__uint128_t)(x2)*(x11))>>64;
x142 = (x2)*(x10);
x143 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*(x10))>>32 : ((__uint128_t)(x2)*(x10))>>64;
x144 = (x2)*(x9);
x145 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*(x9))>>32 : ((__uint128_t)(x2)*(x9))>>64;
x146 = (x1)*(x16);
x147 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x16))>>32 : ((__uint128_t)(x1)*(x16))>>64;
x148 = (x1)*(x15);
x149 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x15))>>32 : ((__uint128_t)(x1)*(x15))>>64;
x150 = (x1)*(x14);
x151 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x14))>>32 : ((__uint128_t)(x1)*(x14))>>64;
x152 = (x1)*(x13);
x153 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x13))>>32 : ((__uint128_t)(x1)*(x13))>>64;
x154 = (x1)*(x12);
x155 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x12))>>32 : ((__uint128_t)(x1)*(x12))>>64;
x156 = (x1)*(x11);
x157 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x11))>>32 : ((__uint128_t)(x1)*(x11))>>64;
x158 = (x1)*(x10);
x159 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x10))>>32 : ((__uint128_t)(x1)*(x10))>>64;
x160 = (x1)*(x9);
x161 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x9))>>32 : ((__uint128_t)(x1)*(x9))>>64;
x162 = (x0)*(x17);
x163 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x17))>>32 : ((__uint128_t)(x0)*(x17))>>64;
x164 = (x0)*(x16);
x165 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x16))>>32 : ((__uint128_t)(x0)*(x16))>>64;
x166 = (x0)*(x15);
x167 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x15))>>32 : ((__uint128_t)(x0)*(x15))>>64;
x168 = (x0)*(x14);
x169 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x14))>>32 : ((__uint128_t)(x0)*(x14))>>64;
x170 = (x0)*(x13);
x171 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x13))>>32 : ((__uint128_t)(x0)*(x13))>>64;
x172 = (x0)*(x12);
x173 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x12))>>32 : ((__uint128_t)(x0)*(x12))>>64;
x174 = (x0)*(x11);
x175 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x11))>>32 : ((__uint128_t)(x0)*(x11))>>64;
x176 = (x0)*(x10);
x177 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x10))>>32 : ((__uint128_t)(x0)*(x10))>>64;
x178 = (x0)*(x9);
x179 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x9))>>32 : ((__uint128_t)(x0)*(x9))>>64;
x180 = (x46)+(x32);
x181 = (x180)<(x46);
x182 = (x181)+(x47);
x183 = (x182)+(x33);
x184 = (x58)+(x180);
x185 = (x184)<(x58);
x186 = (x185)+(x59);
x187 = (x186)+(x183);
x188 = (x68)+(x184);
x189 = (x188)<(x68);
x190 = (x189)+(x69);
x191 = (x190)+(x187);
x192 = (x76)+(x188);
x193 = (x192)<(x76);
x194 = (x193)+(x77);
x195 = (x194)+(x191);
x196 = (x82)+(x192);
x197 = (x196)<(x82);
x198 = (x197)+(x83);
x199 = (x198)+(x195);
x200 = (x86)+(x196);
x201 = (x200)<(x86);
x202 = (x201)+(x87);
x203 = (x202)+(x199);
x204 = (x88)+(x200);
x205 = (x204)<(x88);
x206 = (x205)+(x89);
x207 = (x206)+(x203);
x208 = (x178)+(x204);
x209 = (x208)<(x178);
x210 = (x209)+(x179);
x211 = (x210)+(x207);
x212 = ((x208)>>((uintptr_t)58ULL))|((x211)<<((uintptr_t)6ULL));
x213 = (x211)>>((uintptr_t)58ULL);
x214 = (x208)&((uintptr_t)288230376151711743ULL);
x215 = (x92)+(x90);
x216 = (x215)<(x92);
x217 = (x216)+(x93);
x218 = (x217)+(x91);
x219 = (x96)+(x215);
x220 = (x219)<(x96);
x221 = (x220)+(x97);
x222 = (x221)+(x218);
x223 = (x102)+(x219);
x224 = (x223)<(x102);
x225 = (x224)+(x103);
x226 = (x225)+(x222);
x227 = (x110)+(x223);
x228 = (x227)<(x110);
x229 = (x228)+(x111);
x230 = (x229)+(x226);
x231 = (x120)+(x227);
x232 = (x231)<(x120);
x233 = (x232)+(x121);
x234 = (x233)+(x230);
x235 = (x132)+(x231);
x236 = (x235)<(x132);
x237 = (x236)+(x133);
x238 = (x237)+(x234);
x239 = (x146)+(x235);
x240 = (x239)<(x146);
x241 = (x240)+(x147);
x242 = (x241)+(x238);
x243 = (x162)+(x239);
x244 = (x243)<(x162);
x245 = (x244)+(x163);
x246 = (x245)+(x242);
x247 = (x94)+(x18);
x248 = (x247)<(x94);
x249 = (x248)+(x95);
x250 = (x249)+(x19);
x251 = (x98)+(x247);
x252 = (x251)<(x98);
x253 = (x252)+(x99);
x254 = (x253)+(x250);
x255 = (x104)+(x251);
x256 = (x255)<(x104);
x257 = (x256)+(x105);
x258 = (x257)+(x254);
x259 = (x112)+(x255);
x260 = (x259)<(x112);
x261 = (x260)+(x113);
x262 = (x261)+(x258);
x263 = (x122)+(x259);
x264 = (x263)<(x122);
x265 = (x264)+(x123);
x266 = (x265)+(x262);
x267 = (x134)+(x263);
x268 = (x267)<(x134);
x269 = (x268)+(x135);
x270 = (x269)+(x266);
x271 = (x148)+(x267);
x272 = (x271)<(x148);
x273 = (x272)+(x149);
x274 = (x273)+(x270);
x275 = (x164)+(x271);
x276 = (x275)<(x164);
x277 = (x276)+(x165);
x278 = (x277)+(x274);
x279 = (x34)+(x20);
x280 = (x279)<(x34);
x281 = (x280)+(x35);
x282 = (x281)+(x21);
x283 = (x100)+(x279);
x284 = (x283)<(x100);
x285 = (x284)+(x101);
x286 = (x285)+(x282);
x287 = (x106)+(x283);
x288 = (x287)<(x106);
x289 = (x288)+(x107);
x290 = (x289)+(x286);
x291 = (x114)+(x287);
x292 = (x291)<(x114);
x293 = (x292)+(x115);
x294 = (x293)+(x290);
x295 = (x124)+(x291);
x296 = (x295)<(x124);
x297 = (x296)+(x125);
x298 = (x297)+(x294);
x299 = (x136)+(x295);
x300 = (x299)<(x136);
x301 = (x300)+(x137);
x302 = (x301)+(x298);
x303 = (x150)+(x299);
x304 = (x303)<(x150);
x305 = (x304)+(x151);
x306 = (x305)+(x302);
x307 = (x166)+(x303);
x308 = (x307)<(x166);
x309 = (x308)+(x167);
x310 = (x309)+(x306);
x311 = (x36)+(x22);
x312 = (x311)<(x36);
x313 = (x312)+(x37);
x314 = (x313)+(x23);
x315 = (x48)+(x311);
x316 = (x315)<(x48);
x317 = (x316)+(x49);
x318 = (x317)+(x314);
x319 = (x108)+(x315);
x320 = (x319)<(x108);
x321 = (x320)+(x109);
x322 = (x321)+(x318);
x323 = (x116)+(x319);
x324 = (x323)<(x116);
x325 = (x324)+(x117);
x326 = (x325)+(x322);
x327 = (x126)+(x323);
x328 = (x327)<(x126);
x329 = (x328)+(x127);
x330 = (x329)+(x326);
x331 = (x138)+(x327);
x332 = (x331)<(x138);
x333 = (x332)+(x139);
x334 = (x333)+(x330);
x335 = (x152)+(x331);
x336 = (x335)<(x152);
x337 = (x336)+(x153);
x338 = (x337)+(x334);
x339 = (x168)+(x335);
x340 = (x339)<(x168);
x341 = (x340)+(x169);
x342 = (x341)+(x338);
x343 = (x38)+(x24);
x344 = (x343)<(x38);
x345 = (x344)+(x39);
x346 = (x345)+(x25);
x347 = (x50)+(x343);
x348 = (x347)<(x50);
x349 = (x348)+(x51);
x350 = (x349)+(x346);
x351 = (x60)+(x347);
x352 = (x351)<(x60);
x353 = (x352)+(x61);
x354 = (x353)+(x350);
x355 = (x118)+(x351);
x356 = (x355)<(x118);
x357 = (x356)+(x119);
x358 = (x357)+(x354);
x359 = (x128)+(x355);
x360 = (x359)<(x128);
x361 = (x360)+(x129);
x362 = (x361)+(x358);
x363 = (x140)+(x359);
x364 = (x363)<(x140);
x365 = (x364)+(x141);
x366 = (x365)+(x362);
x367 = (x154)+(x363);
x368 = (x367)<(x154);
x369 = (x368)+(x155);
x370 = (x369)+(x366);
x371 = (x170)+(x367);
x372 = (x371)<(x170);
x373 = (x372)+(x171);
x374 = (x373)+(x370);
x375 = (x40)+(x26);
x376 = (x375)<(x40);
x377 = (x376)+(x41);
x378 = (x377)+(x27);
x379 = (x52)+(x375);
x380 = (x379)<(x52);
x381 = (x380)+(x53);
x382 = (x381)+(x378);
x383 = (x62)+(x379);
x384 = (x383)<(x62);
x385 = (x384)+(x63);
x386 = (x385)+(x382);
x387 = (x70)+(x383);
x388 = (x387)<(x70);
x389 = (x388)+(x71);
x390 = (x389)+(x386);
x391 = (x130)+(x387);
x392 = (x391)<(x130);
x393 = (x392)+(x131);
x394 = (x393)+(x390);
x395 = (x142)+(x391);
x396 = (x395)<(x142);
x397 = (x396)+(x143);
x398 = (x397)+(x394);
x399 = (x156)+(x395);
x400 = (x399)<(x156);
x401 = (x400)+(x157);
x402 = (x401)+(x398);
x403 = (x172)+(x399);
x404 = (x403)<(x172);
x405 = (x404)+(x173);
x406 = (x405)+(x402);
x407 = (x42)+(x28);
x408 = (x407)<(x42);
x409 = (x408)+(x43);
x410 = (x409)+(x29);
x411 = (x54)+(x407);
x412 = (x411)<(x54);
x413 = (x412)+(x55);
x414 = (x413)+(x410);
x415 = (x64)+(x411);
x416 = (x415)<(x64);
x417 = (x416)+(x65);
x418 = (x417)+(x414);
x419 = (x72)+(x415);
x420 = (x419)<(x72);
x421 = (x420)+(x73);
x422 = (x421)+(x418);
x423 = (x78)+(x419);
x424 = (x423)<(x78);
x425 = (x424)+(x79);
x426 = (x425)+(x422);
x427 = (x144)+(x423);
x428 = (x427)<(x144);
x429 = (x428)+(x145);
x430 = (x429)+(x426);
x431 = (x158)+(x427);
x432 = (x431)<(x158);
x433 = (x432)+(x159);
x434 = (x433)+(x430);
x435 = (x174)+(x431);
x436 = (x435)<(x174);
x437 = (x436)+(x175);
x438 = (x437)+(x434);
x439 = (x44)+(x30);
x440 = (x439)<(x44);
x441 = (x440)+(x45);
x442 = (x441)+(x31);
x443 = (x56)+(x439);
x444 = (x443)<(x56);
x445 = (x444)+(x57);
x446 = (x445)+(x442);
x447 = (x66)+(x443);
x448 = (x447)<(x66);
x449 = (x448)+(x67);
x450 = (x449)+(x446);
x451 = (x74)+(x447);
x452 = (x451)<(x74);
x453 = (x452)+(x75);
x454 = (x453)+(x450);
x455 = (x80)+(x451);
x456 = (x455)<(x80);
x457 = (x456)+(x81);
x458 = (x457)+(x454);
x459 = (x84)+(x455);
x460 = (x459)<(x84);
x461 = (x460)+(x85);
x462 = (x461)+(x458);
x463 = (x160)+(x459);
x464 = (x463)<(x160);
x465 = (x464)+(x161);
x466 = (x465)+(x462);
x467 = (x176)+(x463);
x468 = (x467)<(x176);
x469 = (x468)+(x177);
x470 = (x469)+(x466);
x471 = (x212)+(x467);
x472 = (x471)<(x212);
x473 = (x472)+(x213);
x474 = (x473)+(x470);
x475 = ((x471)>>((uintptr_t)58ULL))|((x474)<<((uintptr_t)6ULL));
x476 = (x474)>>((uintptr_t)58ULL);
x477 = (x471)&((uintptr_t)288230376151711743ULL);
x478 = (x475)+(x435);
x479 = (x478)<(x475);
x480 = (x479)+(x476);
x481 = (x480)+(x438);
x482 = ((x478)>>((uintptr_t)58ULL))|((x481)<<((uintptr_t)6ULL));
x483 = (x481)>>((uintptr_t)58ULL);
x484 = (x478)&((uintptr_t)288230376151711743ULL);
x485 = (x482)+(x403);
x486 = (x485)<(x482);
x487 = (x486)+(x483);
x488 = (x487)+(x406);
x489 = ((x485)>>((uintptr_t)58ULL))|((x488)<<((uintptr_t)6ULL));
x490 = (x488)>>((uintptr_t)58ULL);
x491 = (x485)&((uintptr_t)288230376151711743ULL);
x492 = (x489)+(x371);
x493 = (x492)<(x489);
x494 = (x493)+(x490);
x495 = (x494)+(x374);
x496 = ((x492)>>((uintptr_t)58ULL))|((x495)<<((uintptr_t)6ULL));
x497 = (x495)>>((uintptr_t)58ULL);
x498 = (x492)&((uintptr_t)288230376151711743ULL);
x499 = (x496)+(x339);
x500 = (x499)<(x496);
x501 = (x500)+(x497);
x502 = (x501)+(x342);
x503 = ((x499)>>((uintptr_t)58ULL))|((x502)<<((uintptr_t)6ULL));
x504 = (x502)>>((uintptr_t)58ULL);
x505 = (x499)&((uintptr_t)288230376151711743ULL);
x506 = (x503)+(x307);
x507 = (x506)<(x503);
x508 = (x507)+(x504);
x509 = (x508)+(x310);
x510 = ((x506)>>((uintptr_t)58ULL))|((x509)<<((uintptr_t)6ULL));
x511 = (x509)>>((uintptr_t)58ULL);
x512 = (x506)&((uintptr_t)288230376151711743ULL);
x513 = (x510)+(x275);
x514 = (x513)<(x510);
x515 = (x514)+(x511);
x516 = (x515)+(x278);
x517 = ((x513)>>((uintptr_t)58ULL))|((x516)<<((uintptr_t)6ULL));
x518 = (x516)>>((uintptr_t)58ULL);
x519 = (x513)&((uintptr_t)288230376151711743ULL);
x520 = (x517)+(x243);
x521 = (x520)<(x517);
x522 = (x521)+(x518);
x523 = (x522)+(x246);
x524 = ((x520)>>((uintptr_t)57ULL))|((x523)<<((uintptr_t)7ULL));
x525 = (x523)>>((uintptr_t)57ULL);
x526 = (x520)&((uintptr_t)144115188075855871ULL);
x527 = (x214)+(x524);
x528 = (x527)<(x214);
x529 = (x528)+(x525);
x530 = ((x527)>>((uintptr_t)58ULL))|((x529)<<((uintptr_t)6ULL));
x531 = (x527)&((uintptr_t)288230376151711743ULL);
x532 = (x530)+(x477);
x533 = (x532)>>((uintptr_t)58ULL);
x534 = (x532)&((uintptr_t)288230376151711743ULL);
x535 = (x533)+(x484);
x536 = x531;
x537 = x534;
x538 = x535;
x539 = x491;
x540 = x498;
x541 = x505;
x542 = x512;
x543 = x519;
x544 = x526;
/*skip*/
_br2_store((out0)+((uintptr_t)0ULL), x536, sizeof(uintptr_t));
_br2_store((out0)+((uintptr_t)8ULL), x537, sizeof(uintptr_t));
_br2_store((out0)+((uintptr_t)16ULL), x538, sizeof(uintptr_t));
_br2_store((out0)+((uintptr_t)24ULL), x539, sizeof(uintptr_t));
_br2_store((out0)+((uintptr_t)32ULL), x540, sizeof(uintptr_t));
_br2_store((out0)+((uintptr_t)40ULL), x541, sizeof(uintptr_t));
_br2_store((out0)+((uintptr_t)48ULL), x542, sizeof(uintptr_t));
_br2_store((out0)+((uintptr_t)56ULL), x543, sizeof(uintptr_t));
_br2_store((out0)+((uintptr_t)64ULL), x544, sizeof(uintptr_t));
/*skip*/
return;
}
/* NOTE: The following wrapper function is not covered by Coq proofs */
static void fiat_p521_carry_mul(uint64_t out1[9], const uint64_t arg1[9], const uint64_t arg2[9]) {
internal_fiat_p521_carry_mul((uintptr_t)out1, (uintptr_t)arg1, (uintptr_t)arg2);
}
/*
* Input Bounds:
* in0: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]]
* Output Bounds:
* out0: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]]
*/
static
void internal_fiat_p521_carry_square(uintptr_t out0, uintptr_t in0) {
uintptr_t x8, x9, x7, x12, x6, x15, x5, x18, x19, x4, x16, x3, x13, x2, x10, x1, x11, x14, x17, x20, x21, x22, x23, x24, x0, x51, x59, x116, x60, x117, x52, x115, x69, x120, x70, x121, x118, x119, x81, x124, x82, x125, x122, x123, x113, x128, x114, x129, x126, x130, x127, x53, x61, x135, x62, x136, x54, x134, x71, x139, x72, x140, x137, x138, x83, x143, x84, x144, x141, x142, x97, x147, x98, x148, x145, x25, x63, x151, x64, x152, x26, x150, x73, x155, x74, x156, x153, x154, x85, x159, x86, x160, x157, x158, x99, x163, x100, x164, x161, x27, x65, x167, x66, x168, x28, x166, x75, x171, x76, x172, x169, x170, x87, x175, x88, x176, x173, x174, x101, x179, x102, x180, x177, x29, x31, x183, x32, x184, x30, x182, x77, x187, x78, x188, x185, x186, x89, x191, x90, x192, x189, x190, x103, x195, x104, x196, x193, x33, x37, x199, x38, x200, x34, x198, x79, x203, x80, x204, x201, x202, x91, x207, x92, x208, x205, x206, x105, x211, x106, x212, x209, x35, x39, x215, x40, x216, x36, x214, x45, x219, x46, x220, x217, x218, x93, x223, x94, x224, x221, x222, x107, x227, x108, x228, x225, x41, x47, x231, x48, x232, x42, x230, x55, x235, x56, x236, x233, x234, x95, x239, x96, x240, x237, x238, x109, x243, x110, x244, x241, x43, x49, x247, x50, x248, x44, x246, x57, x251, x58, x252, x249, x250, x67, x255, x68, x256, x253, x254, x111, x259, x112, x260, x257, x258, x131, x263, x132, x264, x261, x265, x262, x242, x266, x270, x267, x271, x245, x272, x269, x226, x273, x277, x274, x278, x229, x279, x276, x210, x280, x284, x281, x285, x213, x286, x283, x194, x287, x291, x288, x292, x197, x293, x290, x178, x294, x298, x295, x299, x181, x300, x297, x162, x301, x305, x302, x306, x165, x307, x304, x146, x308, x312, x309, x313, x149, x314, x311, x315, x133, x319, x316, x320, x318, x321, x268, x323, x324, x275, x322, x325, x326, x282, x289, x296, x303, x310, x317, x327, x328, x329, x330, x331, x332, x333, x334, x335;
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));
x6 = _br2_load((in0)+((uintptr_t)48ULL), sizeof(uintptr_t));
x7 = _br2_load((in0)+((uintptr_t)56ULL), sizeof(uintptr_t));
x8 = _br2_load((in0)+((uintptr_t)64ULL), sizeof(uintptr_t));
/*skip*/
/*skip*/
x9 = x8;
x10 = (x9)*((uintptr_t)2ULL);
x11 = (x8)*((uintptr_t)2ULL);
x12 = x7;
x13 = (x12)*((uintptr_t)2ULL);
x14 = (x7)*((uintptr_t)2ULL);
x15 = x6;
x16 = (x15)*((uintptr_t)2ULL);
x17 = (x6)*((uintptr_t)2ULL);
x18 = x5;
x19 = (x18)*((uintptr_t)2ULL);
x20 = (x5)*((uintptr_t)2ULL);
x21 = (x4)*((uintptr_t)2ULL);
x22 = (x3)*((uintptr_t)2ULL);
x23 = (x2)*((uintptr_t)2ULL);
x24 = (x1)*((uintptr_t)2ULL);
x25 = (x8)*((x9)*((uintptr_t)2ULL));
x26 = sizeof(intptr_t) == 4 ? ((uint64_t)(x8)*((x9)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x8)*((x9)*((uintptr_t)2ULL)))>>64;
x27 = (x7)*((x10)*((uintptr_t)2ULL));
x28 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*((x10)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x7)*((x10)*((uintptr_t)2ULL)))>>64;
x29 = (x7)*((x12)*((uintptr_t)2ULL));
x30 = sizeof(intptr_t) == 4 ? ((uint64_t)(x7)*((x12)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x7)*((x12)*((uintptr_t)2ULL)))>>64;
x31 = (x6)*((x10)*((uintptr_t)2ULL));
x32 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*((x10)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x6)*((x10)*((uintptr_t)2ULL)))>>64;
x33 = (x6)*((x13)*((uintptr_t)2ULL));
x34 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*((x13)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x6)*((x13)*((uintptr_t)2ULL)))>>64;
x35 = (x6)*((x15)*((uintptr_t)2ULL));
x36 = sizeof(intptr_t) == 4 ? ((uint64_t)(x6)*((x15)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x6)*((x15)*((uintptr_t)2ULL)))>>64;
x37 = (x5)*((x10)*((uintptr_t)2ULL));
x38 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*((x10)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x5)*((x10)*((uintptr_t)2ULL)))>>64;
x39 = (x5)*((x13)*((uintptr_t)2ULL));
x40 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*((x13)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x5)*((x13)*((uintptr_t)2ULL)))>>64;
x41 = (x5)*((x16)*((uintptr_t)2ULL));
x42 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*((x16)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x5)*((x16)*((uintptr_t)2ULL)))>>64;
x43 = (x5)*((x18)*((uintptr_t)2ULL));
x44 = sizeof(intptr_t) == 4 ? ((uint64_t)(x5)*((x18)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x5)*((x18)*((uintptr_t)2ULL)))>>64;
x45 = (x4)*((x10)*((uintptr_t)2ULL));
x46 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*((x10)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x4)*((x10)*((uintptr_t)2ULL)))>>64;
x47 = (x4)*((x13)*((uintptr_t)2ULL));
x48 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*((x13)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x4)*((x13)*((uintptr_t)2ULL)))>>64;
x49 = (x4)*((x16)*((uintptr_t)2ULL));
x50 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*((x16)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x4)*((x16)*((uintptr_t)2ULL)))>>64;
x51 = (x4)*((x19)*((uintptr_t)2ULL));
x52 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*((x19)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x4)*((x19)*((uintptr_t)2ULL)))>>64;
x53 = (x4)*(x4);
x54 = sizeof(intptr_t) == 4 ? ((uint64_t)(x4)*(x4))>>32 : ((__uint128_t)(x4)*(x4))>>64;
x55 = (x3)*((x10)*((uintptr_t)2ULL));
x56 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*((x10)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x3)*((x10)*((uintptr_t)2ULL)))>>64;
x57 = (x3)*((x13)*((uintptr_t)2ULL));
x58 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*((x13)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x3)*((x13)*((uintptr_t)2ULL)))>>64;
x59 = (x3)*((x16)*((uintptr_t)2ULL));
x60 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*((x16)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x3)*((x16)*((uintptr_t)2ULL)))>>64;
x61 = (x3)*(x20);
x62 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*(x20))>>32 : ((__uint128_t)(x3)*(x20))>>64;
x63 = (x3)*(x21);
x64 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*(x21))>>32 : ((__uint128_t)(x3)*(x21))>>64;
x65 = (x3)*(x3);
x66 = sizeof(intptr_t) == 4 ? ((uint64_t)(x3)*(x3))>>32 : ((__uint128_t)(x3)*(x3))>>64;
x67 = (x2)*((x10)*((uintptr_t)2ULL));
x68 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*((x10)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x2)*((x10)*((uintptr_t)2ULL)))>>64;
x69 = (x2)*((x13)*((uintptr_t)2ULL));
x70 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*((x13)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x2)*((x13)*((uintptr_t)2ULL)))>>64;
x71 = (x2)*(x17);
x72 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*(x17))>>32 : ((__uint128_t)(x2)*(x17))>>64;
x73 = (x2)*(x20);
x74 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*(x20))>>32 : ((__uint128_t)(x2)*(x20))>>64;
x75 = (x2)*(x21);
x76 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*(x21))>>32 : ((__uint128_t)(x2)*(x21))>>64;
x77 = (x2)*(x22);
x78 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*(x22))>>32 : ((__uint128_t)(x2)*(x22))>>64;
x79 = (x2)*(x2);
x80 = sizeof(intptr_t) == 4 ? ((uint64_t)(x2)*(x2))>>32 : ((__uint128_t)(x2)*(x2))>>64;
x81 = (x1)*((x10)*((uintptr_t)2ULL));
x82 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*((x10)*((uintptr_t)2ULL)))>>32 : ((__uint128_t)(x1)*((x10)*((uintptr_t)2ULL)))>>64;
x83 = (x1)*(x14);
x84 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x14))>>32 : ((__uint128_t)(x1)*(x14))>>64;
x85 = (x1)*(x17);
x86 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x17))>>32 : ((__uint128_t)(x1)*(x17))>>64;
x87 = (x1)*(x20);
x88 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x20))>>32 : ((__uint128_t)(x1)*(x20))>>64;
x89 = (x1)*(x21);
x90 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x21))>>32 : ((__uint128_t)(x1)*(x21))>>64;
x91 = (x1)*(x22);
x92 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x22))>>32 : ((__uint128_t)(x1)*(x22))>>64;
x93 = (x1)*(x23);
x94 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x23))>>32 : ((__uint128_t)(x1)*(x23))>>64;
x95 = (x1)*(x1);
x96 = sizeof(intptr_t) == 4 ? ((uint64_t)(x1)*(x1))>>32 : ((__uint128_t)(x1)*(x1))>>64;
x97 = (x0)*(x11);
x98 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x11))>>32 : ((__uint128_t)(x0)*(x11))>>64;
x99 = (x0)*(x14);
x100 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x14))>>32 : ((__uint128_t)(x0)*(x14))>>64;
x101 = (x0)*(x17);
x102 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x17))>>32 : ((__uint128_t)(x0)*(x17))>>64;
x103 = (x0)*(x20);
x104 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x20))>>32 : ((__uint128_t)(x0)*(x20))>>64;
x105 = (x0)*(x21);
x106 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x21))>>32 : ((__uint128_t)(x0)*(x21))>>64;
x107 = (x0)*(x22);
x108 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x22))>>32 : ((__uint128_t)(x0)*(x22))>>64;
x109 = (x0)*(x23);
x110 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x23))>>32 : ((__uint128_t)(x0)*(x23))>>64;
x111 = (x0)*(x24);
x112 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x24))>>32 : ((__uint128_t)(x0)*(x24))>>64;
x113 = (x0)*(x0);
x114 = sizeof(intptr_t) == 4 ? ((uint64_t)(x0)*(x0))>>32 : ((__uint128_t)(x0)*(x0))>>64;
x115 = (x59)+(x51);
x116 = (x115)<(x59);
x117 = (x116)+(x60);
x118 = (x117)+(x52);
x119 = (x69)+(x115);
x120 = (x119)<(x69);
x121 = (x120)+(x70);
x122 = (x121)+(x118);
x123 = (x81)+(x119);
x124 = (x123)<(x81);
x125 = (x124)+(x82);
x126 = (x125)+(x122);
x127 = (x113)+(x123);
x128 = (x127)<(x113);
x129 = (x128)+(x114);
x130 = (x129)+(x126);
x131 = ((x127)>>((uintptr_t)58ULL))|((x130)<<((uintptr_t)6ULL));
x132 = (x130)>>((uintptr_t)58ULL);
x133 = (x127)&((uintptr_t)288230376151711743ULL);
x134 = (x61)+(x53);
x135 = (x134)<(x61);
x136 = (x135)+(x62);
x137 = (x136)+(x54);
x138 = (x71)+(x134);
x139 = (x138)<(x71);
x140 = (x139)+(x72);
x141 = (x140)+(x137);
x142 = (x83)+(x138);
x143 = (x142)<(x83);
x144 = (x143)+(x84);
x145 = (x144)+(x141);
x146 = (x97)+(x142);
x147 = (x146)<(x97);
x148 = (x147)+(x98);
x149 = (x148)+(x145);
x150 = (x63)+(x25);
x151 = (x150)<(x63);
x152 = (x151)+(x64);
x153 = (x152)+(x26);
x154 = (x73)+(x150);
x155 = (x154)<(x73);
x156 = (x155)+(x74);
x157 = (x156)+(x153);
x158 = (x85)+(x154);
x159 = (x158)<(x85);
x160 = (x159)+(x86);
x161 = (x160)+(x157);
x162 = (x99)+(x158);
x163 = (x162)<(x99);
x164 = (x163)+(x100);
x165 = (x164)+(x161);
x166 = (x65)+(x27);
x167 = (x166)<(x65);
x168 = (x167)+(x66);
x169 = (x168)+(x28);
x170 = (x75)+(x166);
x171 = (x170)<(x75);
x172 = (x171)+(x76);
x173 = (x172)+(x169);
x174 = (x87)+(x170);
x175 = (x174)<(x87);
x176 = (x175)+(x88);
x177 = (x176)+(x173);
x178 = (x101)+(x174);
x179 = (x178)<(x101);
x180 = (x179)+(x102);
x181 = (x180)+(x177);
x182 = (x31)+(x29);
x183 = (x182)<(x31);
x184 = (x183)+(x32);
x185 = (x184)+(x30);
x186 = (x77)+(x182);
x187 = (x186)<(x77);
x188 = (x187)+(x78);
x189 = (x188)+(x185);
x190 = (x89)+(x186);
x191 = (x190)<(x89);
x192 = (x191)+(x90);
x193 = (x192)+(x189);
x194 = (x103)+(x190);
x195 = (x194)<(x103);
x196 = (x195)+(x104);
x197 = (x196)+(x193);
x198 = (x37)+(x33);
x199 = (x198)<(x37);
x200 = (x199)+(x38);
x201 = (x200)+(x34);
x202 = (x79)+(x198);
x203 = (x202)<(x79);
x204 = (x203)+(x80);
x205 = (x204)+(x201);
x206 = (x91)+(x202);
x207 = (x206)<(x91);
x208 = (x207)+(x92);
x209 = (x208)+(x205);
x210 = (x105)+(x206);
x211 = (x210)<(x105);
x212 = (x211)+(x106);
x213 = (x212)+(x209);
x214 = (x39)+(x35);
x215 = (x214)<(x39);
x216 = (x215)+(x40);
x217 = (x216)+(x36);
x218 = (x45)+(x214);
x219 = (x218)<(x45);
x220 = (x219)+(x46);
x221 = (x220)+(x217);
x222 = (x93)+(x218);
x223 = (x222)<(x93);
x224 = (x223)+(x94);
x225 = (x224)+(x221);
x226 = (x107)+(x222);
x227 = (x226)<(x107);
x228 = (x227)+(x108);
x229 = (x228)+(x225);
x230 = (x47)+(x41);
x231 = (x230)<(x47);
x232 = (x231)+(x48);
x233 = (x232)+(x42);
x234 = (x55)+(x230);
x235 = (x234)<(x55);
x236 = (x235)+(x56);
x237 = (x236)+(x233);
x238 = (x95)+(x234);
x239 = (x238)<(x95);
x240 = (x239)+(x96);
x241 = (x240)+(x237);
x242 = (x109)+(x238);
x243 = (x242)<(x109);
x244 = (x243)+(x110);
x245 = (x244)+(x241);
x246 = (x49)+(x43);
x247 = (x246)<(x49);
x248 = (x247)+(x50);
x249 = (x248)+(x44);
x250 = (x57)+(x246);
x251 = (x250)<(x57);
x252 = (x251)+(x58);
x253 = (x252)+(x249);
x254 = (x67)+(x250);
x255 = (x254)<(x67);
x256 = (x255)+(x68);
x257 = (x256)+(x253);
x258 = (x111)+(x254);
x259 = (x258)<(x111);
x260 = (x259)+(x112);
x261 = (x260)+(x257);
x262 = (x131)+(x258);
x263 = (x262)<(x131);
x264 = (x263)+(x132);
x265 = (x264)+(x261);
x266 = ((x262)>>((uintptr_t)58ULL))|((x265)<<((uintptr_t)6ULL));
x267 = (x265)>>((uintptr_t)58ULL);
x268 = (x262)&((uintptr_t)288230376151711743ULL);
x269 = (x266)+(x242);
x270 = (x269)<(x266);
x271 = (x270)+(x267);
x272 = (x271)+(x245);
x273 = ((x269)>>((uintptr_t)58ULL))|((x272)<<((uintptr_t)6ULL));
x274 = (x272)>>((uintptr_t)58ULL);
x275 = (x269)&((uintptr_t)288230376151711743ULL);
x276 = (x273)+(x226);
x277 = (x276)<(x273);
x278 = (x277)+(x274);
x279 = (x278)+(x229);
x280 = ((x276)>>((uintptr_t)58ULL))|((x279)<<((uintptr_t)6ULL));
x281 = (x279)>>((uintptr_t)58ULL);
x282 = (x276)&((uintptr_t)288230376151711743ULL);
x283 = (x280)+(x210);
x284 = (x283)<(x280);
x285 = (x284)+(x281);
x286 = (x285)+(x213);
x287 = ((x283)>>((uintptr_t)58ULL))|((x286)<<((uintptr_t)6ULL));
x288 = (x286)>>((uintptr_t)58ULL);
x289 = (x283)&((uintptr_t)288230376151711743ULL);
x290 = (x287)+(x194);
x291 = (x290)<(x287);
x292 = (x291)+(x288);
x293 = (x292)+(x197);
x294 = ((x290)>>((uintptr_t)58ULL))|((x293)<<((uintptr_t)6ULL));
x295 = (x293)>>((uintptr_t)58ULL);
x296 = (x290)&((uintptr_t)288230376151711743ULL);
x297 = (x294)+(x178);
x298 = (x297)<(x294);
x299 = (x298)+(x295);
x300 = (x299)+(x181);
x301 = ((x297)>>((uintptr_t)58ULL))|((x300)<<((uintptr_t)6ULL));
x302 = (x300)>>((uintptr_t)58ULL);
x303 = (x297)&((uintptr_t)288230376151711743ULL);
x304 = (x301)+(x162);
x305 = (x304)<(x301);
x306 = (x305)+(x302);
x307 = (x306)+(x165);
x308 = ((x304)>>((uintptr_t)58ULL))|((x307)<<((uintptr_t)6ULL));
x309 = (x307)>>((uintptr_t)58ULL);
x310 = (x304)&((uintptr_t)288230376151711743ULL);
x311 = (x308)+(x146);
x312 = (x311)<(x308);
x313 = (x312)+(x309);
x314 = (x313)+(x149);
x315 = ((x311)>>((uintptr_t)57ULL))|((x314)<<((uintptr_t)7ULL));
x316 = (x314)>>((uintptr_t)57ULL);
x317 = (x311)&((uintptr_t)144115188075855871ULL);
x318 = (x133)+(x315);
x319 = (x318)<(x133);
x320 = (x319)+(x316);
x321 = ((x318)>>((uintptr_t)58ULL))|((x320)<<((uintptr_t)6ULL));
x322 = (x318)&((uintptr_t)288230376151711743ULL);
x323 = (x321)+(x268);
x324 = (x323)>>((uintptr_t)58ULL);
x325 = (x323)&((uintptr_t)288230376151711743ULL);
x326 = (x324)+(x275);
x327 = x322;
x328 = x325;
x329 = x326;
x330 = x282;
x331 = x289;
x332 = x296;
x333 = x303;
x334 = x310;
x335 = x317;
/*skip*/
_br2_store((out0)+((uintptr_t)0ULL), x327, sizeof(uintptr_t));
_br2_store((out0)+((uintptr_t)8ULL), x328, sizeof(uintptr_t));
_br2_store((out0)+((uintptr_t)16ULL), x329, sizeof(uintptr_t));
_br2_store((out0)+((uintptr_t)24ULL), x330, sizeof(uintptr_t));
_br2_store((out0)+((uintptr_t)32ULL), x331, sizeof(uintptr_t));
_br2_store((out0)+((uintptr_t)40ULL), x332, sizeof(uintptr_t));
_br2_store((out0)+((uintptr_t)48ULL), x333, sizeof(uintptr_t));
_br2_store((out0)+((uintptr_t)56ULL), x334, sizeof(uintptr_t));
_br2_store((out0)+((uintptr_t)64ULL), x335, sizeof(uintptr_t));
/*skip*/
return;
}
/* NOTE: The following wrapper function is not covered by Coq proofs */
static void fiat_p521_carry_square(uint64_t out1[9], const uint64_t arg1[9]) {
internal_fiat_p521_carry_square((uintptr_t)out1, (uintptr_t)arg1);
}
/*
* Input Bounds:
* in0: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]]
* Output Bounds:
* out0: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]]
*/
static
void internal_fiat_p521_carry(uintptr_t out0, uintptr_t in0) {
uintptr_t x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x18, x19, x11, x12, x13, x14, x15, x16, x17, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31, x32, x33, x34, x35, x36, x37;
x0 = _br2_load((in0)+((uintptr_t)0ULL), sizeof(uintptr_t));
x1 = _br2_load((in0)+((uintptr_t)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));
x6 = _br2_load((in0)+((uintptr_t)48ULL), sizeof(uintptr_t));
x7 = _br2_load((in0)+((uintptr_t)56ULL), sizeof(uintptr_t));
x8 = _br2_load((in0)+((uintptr_t)64ULL), sizeof(uintptr_t));
/*skip*/
/*skip*/
x9 = x0;
x10 = ((x9)>>((uintptr_t)58ULL))+(x1);
x11 = ((x10)>>((uintptr_t)58ULL))+(x2);
x12 = ((x11)>>((uintptr_t)58ULL))+(x3);