1 /* MIT License
2  *
3  * Copyright (c) 2016-2020 INRIA, CMU and Microsoft Corporation
4  *
5  * Permission is hereby granted, free of charge, to any person obtaining a copy
6  * of this software and associated documentation files (the "Software"), to deal
7  * in the Software without restriction, including without limitation the rights
8  * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
9  * copies of the Software, and to permit persons to whom the Software is
10  * furnished to do so, subject to the following conditions:
11  *
12  * The above copyright notice and this permission notice shall be included in all
13  * copies or substantial portions of the Software.
14  *
15  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
16  * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
17  * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
18  * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
19  * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
20  * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
21  * SOFTWARE.
22  */
23 
24 #ifndef __Hacl_Bignum25519_51_H
25 #define __Hacl_Bignum25519_51_H
26 
27 #if defined(__cplusplus)
28 extern "C" {
29 #endif
30 
31 #include "kremlin/internal/types.h"
32 #include "kremlin/lowstar_endianness.h"
33 #include <string.h>
34 #include <stdbool.h>
35 
36 #include "Hacl_Kremlib.h"
37 
38 static inline void
Hacl_Impl_Curve25519_Field51_fadd(uint64_t * out,uint64_t * f1,uint64_t * f2)39 Hacl_Impl_Curve25519_Field51_fadd(uint64_t *out, uint64_t *f1, uint64_t *f2)
40 {
41     uint64_t f10 = f1[0U];
42     uint64_t f20 = f2[0U];
43     uint64_t f11 = f1[1U];
44     uint64_t f21 = f2[1U];
45     uint64_t f12 = f1[2U];
46     uint64_t f22 = f2[2U];
47     uint64_t f13 = f1[3U];
48     uint64_t f23 = f2[3U];
49     uint64_t f14 = f1[4U];
50     uint64_t f24 = f2[4U];
51     out[0U] = f10 + f20;
52     out[1U] = f11 + f21;
53     out[2U] = f12 + f22;
54     out[3U] = f13 + f23;
55     out[4U] = f14 + f24;
56 }
57 
58 static inline void
Hacl_Impl_Curve25519_Field51_fsub(uint64_t * out,uint64_t * f1,uint64_t * f2)59 Hacl_Impl_Curve25519_Field51_fsub(uint64_t *out, uint64_t *f1, uint64_t *f2)
60 {
61     uint64_t f10 = f1[0U];
62     uint64_t f20 = f2[0U];
63     uint64_t f11 = f1[1U];
64     uint64_t f21 = f2[1U];
65     uint64_t f12 = f1[2U];
66     uint64_t f22 = f2[2U];
67     uint64_t f13 = f1[3U];
68     uint64_t f23 = f2[3U];
69     uint64_t f14 = f1[4U];
70     uint64_t f24 = f2[4U];
71     out[0U] = f10 + (uint64_t)0x3fffffffffff68U - f20;
72     out[1U] = f11 + (uint64_t)0x3ffffffffffff8U - f21;
73     out[2U] = f12 + (uint64_t)0x3ffffffffffff8U - f22;
74     out[3U] = f13 + (uint64_t)0x3ffffffffffff8U - f23;
75     out[4U] = f14 + (uint64_t)0x3ffffffffffff8U - f24;
76 }
77 
78 static inline void
Hacl_Impl_Curve25519_Field51_fmul(uint64_t * out,uint64_t * f1,uint64_t * f2,FStar_UInt128_uint128 * uu___)79 Hacl_Impl_Curve25519_Field51_fmul(
80     uint64_t *out,
81     uint64_t *f1,
82     uint64_t *f2,
83     FStar_UInt128_uint128 *uu___)
84 {
85     uint64_t f10 = f1[0U];
86     uint64_t f11 = f1[1U];
87     uint64_t f12 = f1[2U];
88     uint64_t f13 = f1[3U];
89     uint64_t f14 = f1[4U];
90     uint64_t f20 = f2[0U];
91     uint64_t f21 = f2[1U];
92     uint64_t f22 = f2[2U];
93     uint64_t f23 = f2[3U];
94     uint64_t f24 = f2[4U];
95     uint64_t tmp1 = f21 * (uint64_t)19U;
96     uint64_t tmp2 = f22 * (uint64_t)19U;
97     uint64_t tmp3 = f23 * (uint64_t)19U;
98     uint64_t tmp4 = f24 * (uint64_t)19U;
99     FStar_UInt128_uint128 o00 = FStar_UInt128_mul_wide(f10, f20);
100     FStar_UInt128_uint128 o10 = FStar_UInt128_mul_wide(f10, f21);
101     FStar_UInt128_uint128 o20 = FStar_UInt128_mul_wide(f10, f22);
102     FStar_UInt128_uint128 o30 = FStar_UInt128_mul_wide(f10, f23);
103     FStar_UInt128_uint128 o40 = FStar_UInt128_mul_wide(f10, f24);
104     FStar_UInt128_uint128 o01 = FStar_UInt128_add(o00, FStar_UInt128_mul_wide(f11, tmp4));
105     FStar_UInt128_uint128 o11 = FStar_UInt128_add(o10, FStar_UInt128_mul_wide(f11, f20));
106     FStar_UInt128_uint128 o21 = FStar_UInt128_add(o20, FStar_UInt128_mul_wide(f11, f21));
107     FStar_UInt128_uint128 o31 = FStar_UInt128_add(o30, FStar_UInt128_mul_wide(f11, f22));
108     FStar_UInt128_uint128 o41 = FStar_UInt128_add(o40, FStar_UInt128_mul_wide(f11, f23));
109     FStar_UInt128_uint128 o02 = FStar_UInt128_add(o01, FStar_UInt128_mul_wide(f12, tmp3));
110     FStar_UInt128_uint128 o12 = FStar_UInt128_add(o11, FStar_UInt128_mul_wide(f12, tmp4));
111     FStar_UInt128_uint128 o22 = FStar_UInt128_add(o21, FStar_UInt128_mul_wide(f12, f20));
112     FStar_UInt128_uint128 o32 = FStar_UInt128_add(o31, FStar_UInt128_mul_wide(f12, f21));
113     FStar_UInt128_uint128 o42 = FStar_UInt128_add(o41, FStar_UInt128_mul_wide(f12, f22));
114     FStar_UInt128_uint128 o03 = FStar_UInt128_add(o02, FStar_UInt128_mul_wide(f13, tmp2));
115     FStar_UInt128_uint128 o13 = FStar_UInt128_add(o12, FStar_UInt128_mul_wide(f13, tmp3));
116     FStar_UInt128_uint128 o23 = FStar_UInt128_add(o22, FStar_UInt128_mul_wide(f13, tmp4));
117     FStar_UInt128_uint128 o33 = FStar_UInt128_add(o32, FStar_UInt128_mul_wide(f13, f20));
118     FStar_UInt128_uint128 o43 = FStar_UInt128_add(o42, FStar_UInt128_mul_wide(f13, f21));
119     FStar_UInt128_uint128 o04 = FStar_UInt128_add(o03, FStar_UInt128_mul_wide(f14, tmp1));
120     FStar_UInt128_uint128 o14 = FStar_UInt128_add(o13, FStar_UInt128_mul_wide(f14, tmp2));
121     FStar_UInt128_uint128 o24 = FStar_UInt128_add(o23, FStar_UInt128_mul_wide(f14, tmp3));
122     FStar_UInt128_uint128 o34 = FStar_UInt128_add(o33, FStar_UInt128_mul_wide(f14, tmp4));
123     FStar_UInt128_uint128 o44 = FStar_UInt128_add(o43, FStar_UInt128_mul_wide(f14, f20));
124     FStar_UInt128_uint128 tmp_w0 = o04;
125     FStar_UInt128_uint128 tmp_w1 = o14;
126     FStar_UInt128_uint128 tmp_w2 = o24;
127     FStar_UInt128_uint128 tmp_w3 = o34;
128     FStar_UInt128_uint128 tmp_w4 = o44;
129     FStar_UInt128_uint128
130         l_ = FStar_UInt128_add(tmp_w0, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
131     uint64_t tmp01 = FStar_UInt128_uint128_to_uint64(l_) & (uint64_t)0x7ffffffffffffU;
132     uint64_t c0 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_, (uint32_t)51U));
133     FStar_UInt128_uint128 l_0 = FStar_UInt128_add(tmp_w1, FStar_UInt128_uint64_to_uint128(c0));
134     uint64_t tmp11 = FStar_UInt128_uint128_to_uint64(l_0) & (uint64_t)0x7ffffffffffffU;
135     uint64_t c1 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_0, (uint32_t)51U));
136     FStar_UInt128_uint128 l_1 = FStar_UInt128_add(tmp_w2, FStar_UInt128_uint64_to_uint128(c1));
137     uint64_t tmp21 = FStar_UInt128_uint128_to_uint64(l_1) & (uint64_t)0x7ffffffffffffU;
138     uint64_t c2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_1, (uint32_t)51U));
139     FStar_UInt128_uint128 l_2 = FStar_UInt128_add(tmp_w3, FStar_UInt128_uint64_to_uint128(c2));
140     uint64_t tmp31 = FStar_UInt128_uint128_to_uint64(l_2) & (uint64_t)0x7ffffffffffffU;
141     uint64_t c3 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_2, (uint32_t)51U));
142     FStar_UInt128_uint128 l_3 = FStar_UInt128_add(tmp_w4, FStar_UInt128_uint64_to_uint128(c3));
143     uint64_t tmp41 = FStar_UInt128_uint128_to_uint64(l_3) & (uint64_t)0x7ffffffffffffU;
144     uint64_t c4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_3, (uint32_t)51U));
145     uint64_t l_4 = tmp01 + c4 * (uint64_t)19U;
146     uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
147     uint64_t c5 = l_4 >> (uint32_t)51U;
148     uint64_t o0 = tmp0_;
149     uint64_t o1 = tmp11 + c5;
150     uint64_t o2 = tmp21;
151     uint64_t o3 = tmp31;
152     uint64_t o4 = tmp41;
153     out[0U] = o0;
154     out[1U] = o1;
155     out[2U] = o2;
156     out[3U] = o3;
157     out[4U] = o4;
158 }
159 
160 static inline void
Hacl_Impl_Curve25519_Field51_fmul2(uint64_t * out,uint64_t * f1,uint64_t * f2,FStar_UInt128_uint128 * uu___)161 Hacl_Impl_Curve25519_Field51_fmul2(
162     uint64_t *out,
163     uint64_t *f1,
164     uint64_t *f2,
165     FStar_UInt128_uint128 *uu___)
166 {
167     uint64_t f10 = f1[0U];
168     uint64_t f11 = f1[1U];
169     uint64_t f12 = f1[2U];
170     uint64_t f13 = f1[3U];
171     uint64_t f14 = f1[4U];
172     uint64_t f20 = f2[0U];
173     uint64_t f21 = f2[1U];
174     uint64_t f22 = f2[2U];
175     uint64_t f23 = f2[3U];
176     uint64_t f24 = f2[4U];
177     uint64_t f30 = f1[5U];
178     uint64_t f31 = f1[6U];
179     uint64_t f32 = f1[7U];
180     uint64_t f33 = f1[8U];
181     uint64_t f34 = f1[9U];
182     uint64_t f40 = f2[5U];
183     uint64_t f41 = f2[6U];
184     uint64_t f42 = f2[7U];
185     uint64_t f43 = f2[8U];
186     uint64_t f44 = f2[9U];
187     uint64_t tmp11 = f21 * (uint64_t)19U;
188     uint64_t tmp12 = f22 * (uint64_t)19U;
189     uint64_t tmp13 = f23 * (uint64_t)19U;
190     uint64_t tmp14 = f24 * (uint64_t)19U;
191     uint64_t tmp21 = f41 * (uint64_t)19U;
192     uint64_t tmp22 = f42 * (uint64_t)19U;
193     uint64_t tmp23 = f43 * (uint64_t)19U;
194     uint64_t tmp24 = f44 * (uint64_t)19U;
195     FStar_UInt128_uint128 o00 = FStar_UInt128_mul_wide(f10, f20);
196     FStar_UInt128_uint128 o15 = FStar_UInt128_mul_wide(f10, f21);
197     FStar_UInt128_uint128 o25 = FStar_UInt128_mul_wide(f10, f22);
198     FStar_UInt128_uint128 o30 = FStar_UInt128_mul_wide(f10, f23);
199     FStar_UInt128_uint128 o40 = FStar_UInt128_mul_wide(f10, f24);
200     FStar_UInt128_uint128 o010 = FStar_UInt128_add(o00, FStar_UInt128_mul_wide(f11, tmp14));
201     FStar_UInt128_uint128 o110 = FStar_UInt128_add(o15, FStar_UInt128_mul_wide(f11, f20));
202     FStar_UInt128_uint128 o210 = FStar_UInt128_add(o25, FStar_UInt128_mul_wide(f11, f21));
203     FStar_UInt128_uint128 o310 = FStar_UInt128_add(o30, FStar_UInt128_mul_wide(f11, f22));
204     FStar_UInt128_uint128 o410 = FStar_UInt128_add(o40, FStar_UInt128_mul_wide(f11, f23));
205     FStar_UInt128_uint128 o020 = FStar_UInt128_add(o010, FStar_UInt128_mul_wide(f12, tmp13));
206     FStar_UInt128_uint128 o120 = FStar_UInt128_add(o110, FStar_UInt128_mul_wide(f12, tmp14));
207     FStar_UInt128_uint128 o220 = FStar_UInt128_add(o210, FStar_UInt128_mul_wide(f12, f20));
208     FStar_UInt128_uint128 o320 = FStar_UInt128_add(o310, FStar_UInt128_mul_wide(f12, f21));
209     FStar_UInt128_uint128 o420 = FStar_UInt128_add(o410, FStar_UInt128_mul_wide(f12, f22));
210     FStar_UInt128_uint128 o030 = FStar_UInt128_add(o020, FStar_UInt128_mul_wide(f13, tmp12));
211     FStar_UInt128_uint128 o130 = FStar_UInt128_add(o120, FStar_UInt128_mul_wide(f13, tmp13));
212     FStar_UInt128_uint128 o230 = FStar_UInt128_add(o220, FStar_UInt128_mul_wide(f13, tmp14));
213     FStar_UInt128_uint128 o330 = FStar_UInt128_add(o320, FStar_UInt128_mul_wide(f13, f20));
214     FStar_UInt128_uint128 o430 = FStar_UInt128_add(o420, FStar_UInt128_mul_wide(f13, f21));
215     FStar_UInt128_uint128 o040 = FStar_UInt128_add(o030, FStar_UInt128_mul_wide(f14, tmp11));
216     FStar_UInt128_uint128 o140 = FStar_UInt128_add(o130, FStar_UInt128_mul_wide(f14, tmp12));
217     FStar_UInt128_uint128 o240 = FStar_UInt128_add(o230, FStar_UInt128_mul_wide(f14, tmp13));
218     FStar_UInt128_uint128 o340 = FStar_UInt128_add(o330, FStar_UInt128_mul_wide(f14, tmp14));
219     FStar_UInt128_uint128 o440 = FStar_UInt128_add(o430, FStar_UInt128_mul_wide(f14, f20));
220     FStar_UInt128_uint128 tmp_w10 = o040;
221     FStar_UInt128_uint128 tmp_w11 = o140;
222     FStar_UInt128_uint128 tmp_w12 = o240;
223     FStar_UInt128_uint128 tmp_w13 = o340;
224     FStar_UInt128_uint128 tmp_w14 = o440;
225     FStar_UInt128_uint128 o0 = FStar_UInt128_mul_wide(f30, f40);
226     FStar_UInt128_uint128 o1 = FStar_UInt128_mul_wide(f30, f41);
227     FStar_UInt128_uint128 o2 = FStar_UInt128_mul_wide(f30, f42);
228     FStar_UInt128_uint128 o3 = FStar_UInt128_mul_wide(f30, f43);
229     FStar_UInt128_uint128 o4 = FStar_UInt128_mul_wide(f30, f44);
230     FStar_UInt128_uint128 o01 = FStar_UInt128_add(o0, FStar_UInt128_mul_wide(f31, tmp24));
231     FStar_UInt128_uint128 o111 = FStar_UInt128_add(o1, FStar_UInt128_mul_wide(f31, f40));
232     FStar_UInt128_uint128 o211 = FStar_UInt128_add(o2, FStar_UInt128_mul_wide(f31, f41));
233     FStar_UInt128_uint128 o31 = FStar_UInt128_add(o3, FStar_UInt128_mul_wide(f31, f42));
234     FStar_UInt128_uint128 o41 = FStar_UInt128_add(o4, FStar_UInt128_mul_wide(f31, f43));
235     FStar_UInt128_uint128 o02 = FStar_UInt128_add(o01, FStar_UInt128_mul_wide(f32, tmp23));
236     FStar_UInt128_uint128 o121 = FStar_UInt128_add(o111, FStar_UInt128_mul_wide(f32, tmp24));
237     FStar_UInt128_uint128 o221 = FStar_UInt128_add(o211, FStar_UInt128_mul_wide(f32, f40));
238     FStar_UInt128_uint128 o32 = FStar_UInt128_add(o31, FStar_UInt128_mul_wide(f32, f41));
239     FStar_UInt128_uint128 o42 = FStar_UInt128_add(o41, FStar_UInt128_mul_wide(f32, f42));
240     FStar_UInt128_uint128 o03 = FStar_UInt128_add(o02, FStar_UInt128_mul_wide(f33, tmp22));
241     FStar_UInt128_uint128 o131 = FStar_UInt128_add(o121, FStar_UInt128_mul_wide(f33, tmp23));
242     FStar_UInt128_uint128 o231 = FStar_UInt128_add(o221, FStar_UInt128_mul_wide(f33, tmp24));
243     FStar_UInt128_uint128 o33 = FStar_UInt128_add(o32, FStar_UInt128_mul_wide(f33, f40));
244     FStar_UInt128_uint128 o43 = FStar_UInt128_add(o42, FStar_UInt128_mul_wide(f33, f41));
245     FStar_UInt128_uint128 o04 = FStar_UInt128_add(o03, FStar_UInt128_mul_wide(f34, tmp21));
246     FStar_UInt128_uint128 o141 = FStar_UInt128_add(o131, FStar_UInt128_mul_wide(f34, tmp22));
247     FStar_UInt128_uint128 o241 = FStar_UInt128_add(o231, FStar_UInt128_mul_wide(f34, tmp23));
248     FStar_UInt128_uint128 o34 = FStar_UInt128_add(o33, FStar_UInt128_mul_wide(f34, tmp24));
249     FStar_UInt128_uint128 o44 = FStar_UInt128_add(o43, FStar_UInt128_mul_wide(f34, f40));
250     FStar_UInt128_uint128 tmp_w20 = o04;
251     FStar_UInt128_uint128 tmp_w21 = o141;
252     FStar_UInt128_uint128 tmp_w22 = o241;
253     FStar_UInt128_uint128 tmp_w23 = o34;
254     FStar_UInt128_uint128 tmp_w24 = o44;
255     FStar_UInt128_uint128
256         l_ = FStar_UInt128_add(tmp_w10, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
257     uint64_t tmp00 = FStar_UInt128_uint128_to_uint64(l_) & (uint64_t)0x7ffffffffffffU;
258     uint64_t c00 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_, (uint32_t)51U));
259     FStar_UInt128_uint128 l_0 = FStar_UInt128_add(tmp_w11, FStar_UInt128_uint64_to_uint128(c00));
260     uint64_t tmp10 = FStar_UInt128_uint128_to_uint64(l_0) & (uint64_t)0x7ffffffffffffU;
261     uint64_t c10 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_0, (uint32_t)51U));
262     FStar_UInt128_uint128 l_1 = FStar_UInt128_add(tmp_w12, FStar_UInt128_uint64_to_uint128(c10));
263     uint64_t tmp20 = FStar_UInt128_uint128_to_uint64(l_1) & (uint64_t)0x7ffffffffffffU;
264     uint64_t c20 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_1, (uint32_t)51U));
265     FStar_UInt128_uint128 l_2 = FStar_UInt128_add(tmp_w13, FStar_UInt128_uint64_to_uint128(c20));
266     uint64_t tmp30 = FStar_UInt128_uint128_to_uint64(l_2) & (uint64_t)0x7ffffffffffffU;
267     uint64_t c30 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_2, (uint32_t)51U));
268     FStar_UInt128_uint128 l_3 = FStar_UInt128_add(tmp_w14, FStar_UInt128_uint64_to_uint128(c30));
269     uint64_t tmp40 = FStar_UInt128_uint128_to_uint64(l_3) & (uint64_t)0x7ffffffffffffU;
270     uint64_t c40 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_3, (uint32_t)51U));
271     uint64_t l_4 = tmp00 + c40 * (uint64_t)19U;
272     uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
273     uint64_t c50 = l_4 >> (uint32_t)51U;
274     uint64_t o100 = tmp0_;
275     uint64_t o112 = tmp10 + c50;
276     uint64_t o122 = tmp20;
277     uint64_t o132 = tmp30;
278     uint64_t o142 = tmp40;
279     FStar_UInt128_uint128
280         l_5 = FStar_UInt128_add(tmp_w20, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
281     uint64_t tmp0 = FStar_UInt128_uint128_to_uint64(l_5) & (uint64_t)0x7ffffffffffffU;
282     uint64_t c0 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_5, (uint32_t)51U));
283     FStar_UInt128_uint128 l_6 = FStar_UInt128_add(tmp_w21, FStar_UInt128_uint64_to_uint128(c0));
284     uint64_t tmp1 = FStar_UInt128_uint128_to_uint64(l_6) & (uint64_t)0x7ffffffffffffU;
285     uint64_t c1 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_6, (uint32_t)51U));
286     FStar_UInt128_uint128 l_7 = FStar_UInt128_add(tmp_w22, FStar_UInt128_uint64_to_uint128(c1));
287     uint64_t tmp2 = FStar_UInt128_uint128_to_uint64(l_7) & (uint64_t)0x7ffffffffffffU;
288     uint64_t c2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_7, (uint32_t)51U));
289     FStar_UInt128_uint128 l_8 = FStar_UInt128_add(tmp_w23, FStar_UInt128_uint64_to_uint128(c2));
290     uint64_t tmp3 = FStar_UInt128_uint128_to_uint64(l_8) & (uint64_t)0x7ffffffffffffU;
291     uint64_t c3 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_8, (uint32_t)51U));
292     FStar_UInt128_uint128 l_9 = FStar_UInt128_add(tmp_w24, FStar_UInt128_uint64_to_uint128(c3));
293     uint64_t tmp4 = FStar_UInt128_uint128_to_uint64(l_9) & (uint64_t)0x7ffffffffffffU;
294     uint64_t c4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_9, (uint32_t)51U));
295     uint64_t l_10 = tmp0 + c4 * (uint64_t)19U;
296     uint64_t tmp0_0 = l_10 & (uint64_t)0x7ffffffffffffU;
297     uint64_t c5 = l_10 >> (uint32_t)51U;
298     uint64_t o200 = tmp0_0;
299     uint64_t o212 = tmp1 + c5;
300     uint64_t o222 = tmp2;
301     uint64_t o232 = tmp3;
302     uint64_t o242 = tmp4;
303     uint64_t o10 = o100;
304     uint64_t o11 = o112;
305     uint64_t o12 = o122;
306     uint64_t o13 = o132;
307     uint64_t o14 = o142;
308     uint64_t o20 = o200;
309     uint64_t o21 = o212;
310     uint64_t o22 = o222;
311     uint64_t o23 = o232;
312     uint64_t o24 = o242;
313     out[0U] = o10;
314     out[1U] = o11;
315     out[2U] = o12;
316     out[3U] = o13;
317     out[4U] = o14;
318     out[5U] = o20;
319     out[6U] = o21;
320     out[7U] = o22;
321     out[8U] = o23;
322     out[9U] = o24;
323 }
324 
325 static inline void
Hacl_Impl_Curve25519_Field51_fmul1(uint64_t * out,uint64_t * f1,uint64_t f2)326 Hacl_Impl_Curve25519_Field51_fmul1(uint64_t *out, uint64_t *f1, uint64_t f2)
327 {
328     uint64_t f10 = f1[0U];
329     uint64_t f11 = f1[1U];
330     uint64_t f12 = f1[2U];
331     uint64_t f13 = f1[3U];
332     uint64_t f14 = f1[4U];
333     FStar_UInt128_uint128 tmp_w0 = FStar_UInt128_mul_wide(f2, f10);
334     FStar_UInt128_uint128 tmp_w1 = FStar_UInt128_mul_wide(f2, f11);
335     FStar_UInt128_uint128 tmp_w2 = FStar_UInt128_mul_wide(f2, f12);
336     FStar_UInt128_uint128 tmp_w3 = FStar_UInt128_mul_wide(f2, f13);
337     FStar_UInt128_uint128 tmp_w4 = FStar_UInt128_mul_wide(f2, f14);
338     FStar_UInt128_uint128
339         l_ = FStar_UInt128_add(tmp_w0, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
340     uint64_t tmp0 = FStar_UInt128_uint128_to_uint64(l_) & (uint64_t)0x7ffffffffffffU;
341     uint64_t c0 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_, (uint32_t)51U));
342     FStar_UInt128_uint128 l_0 = FStar_UInt128_add(tmp_w1, FStar_UInt128_uint64_to_uint128(c0));
343     uint64_t tmp1 = FStar_UInt128_uint128_to_uint64(l_0) & (uint64_t)0x7ffffffffffffU;
344     uint64_t c1 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_0, (uint32_t)51U));
345     FStar_UInt128_uint128 l_1 = FStar_UInt128_add(tmp_w2, FStar_UInt128_uint64_to_uint128(c1));
346     uint64_t tmp2 = FStar_UInt128_uint128_to_uint64(l_1) & (uint64_t)0x7ffffffffffffU;
347     uint64_t c2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_1, (uint32_t)51U));
348     FStar_UInt128_uint128 l_2 = FStar_UInt128_add(tmp_w3, FStar_UInt128_uint64_to_uint128(c2));
349     uint64_t tmp3 = FStar_UInt128_uint128_to_uint64(l_2) & (uint64_t)0x7ffffffffffffU;
350     uint64_t c3 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_2, (uint32_t)51U));
351     FStar_UInt128_uint128 l_3 = FStar_UInt128_add(tmp_w4, FStar_UInt128_uint64_to_uint128(c3));
352     uint64_t tmp4 = FStar_UInt128_uint128_to_uint64(l_3) & (uint64_t)0x7ffffffffffffU;
353     uint64_t c4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_3, (uint32_t)51U));
354     uint64_t l_4 = tmp0 + c4 * (uint64_t)19U;
355     uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
356     uint64_t c5 = l_4 >> (uint32_t)51U;
357     uint64_t o0 = tmp0_;
358     uint64_t o1 = tmp1 + c5;
359     uint64_t o2 = tmp2;
360     uint64_t o3 = tmp3;
361     uint64_t o4 = tmp4;
362     out[0U] = o0;
363     out[1U] = o1;
364     out[2U] = o2;
365     out[3U] = o3;
366     out[4U] = o4;
367 }
368 
369 static inline void
Hacl_Impl_Curve25519_Field51_fsqr(uint64_t * out,uint64_t * f,FStar_UInt128_uint128 * uu___)370 Hacl_Impl_Curve25519_Field51_fsqr(uint64_t *out, uint64_t *f, FStar_UInt128_uint128 *uu___)
371 {
372     uint64_t f0 = f[0U];
373     uint64_t f1 = f[1U];
374     uint64_t f2 = f[2U];
375     uint64_t f3 = f[3U];
376     uint64_t f4 = f[4U];
377     uint64_t d0 = (uint64_t)2U * f0;
378     uint64_t d1 = (uint64_t)2U * f1;
379     uint64_t d2 = (uint64_t)38U * f2;
380     uint64_t d3 = (uint64_t)19U * f3;
381     uint64_t d419 = (uint64_t)19U * f4;
382     uint64_t d4 = (uint64_t)2U * d419;
383     FStar_UInt128_uint128
384         s0 =
385             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(f0, f0),
386                                                 FStar_UInt128_mul_wide(d4, f1)),
387                               FStar_UInt128_mul_wide(d2, f3));
388     FStar_UInt128_uint128
389         s1 =
390             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f1),
391                                                 FStar_UInt128_mul_wide(d4, f2)),
392                               FStar_UInt128_mul_wide(d3, f3));
393     FStar_UInt128_uint128
394         s2 =
395             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f2),
396                                                 FStar_UInt128_mul_wide(f1, f1)),
397                               FStar_UInt128_mul_wide(d4, f3));
398     FStar_UInt128_uint128
399         s3 =
400             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f3),
401                                                 FStar_UInt128_mul_wide(d1, f2)),
402                               FStar_UInt128_mul_wide(f4, d419));
403     FStar_UInt128_uint128
404         s4 =
405             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f4),
406                                                 FStar_UInt128_mul_wide(d1, f3)),
407                               FStar_UInt128_mul_wide(f2, f2));
408     FStar_UInt128_uint128 o00 = s0;
409     FStar_UInt128_uint128 o10 = s1;
410     FStar_UInt128_uint128 o20 = s2;
411     FStar_UInt128_uint128 o30 = s3;
412     FStar_UInt128_uint128 o40 = s4;
413     FStar_UInt128_uint128
414         l_ = FStar_UInt128_add(o00, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
415     uint64_t tmp0 = FStar_UInt128_uint128_to_uint64(l_) & (uint64_t)0x7ffffffffffffU;
416     uint64_t c0 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_, (uint32_t)51U));
417     FStar_UInt128_uint128 l_0 = FStar_UInt128_add(o10, FStar_UInt128_uint64_to_uint128(c0));
418     uint64_t tmp1 = FStar_UInt128_uint128_to_uint64(l_0) & (uint64_t)0x7ffffffffffffU;
419     uint64_t c1 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_0, (uint32_t)51U));
420     FStar_UInt128_uint128 l_1 = FStar_UInt128_add(o20, FStar_UInt128_uint64_to_uint128(c1));
421     uint64_t tmp2 = FStar_UInt128_uint128_to_uint64(l_1) & (uint64_t)0x7ffffffffffffU;
422     uint64_t c2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_1, (uint32_t)51U));
423     FStar_UInt128_uint128 l_2 = FStar_UInt128_add(o30, FStar_UInt128_uint64_to_uint128(c2));
424     uint64_t tmp3 = FStar_UInt128_uint128_to_uint64(l_2) & (uint64_t)0x7ffffffffffffU;
425     uint64_t c3 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_2, (uint32_t)51U));
426     FStar_UInt128_uint128 l_3 = FStar_UInt128_add(o40, FStar_UInt128_uint64_to_uint128(c3));
427     uint64_t tmp4 = FStar_UInt128_uint128_to_uint64(l_3) & (uint64_t)0x7ffffffffffffU;
428     uint64_t c4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_3, (uint32_t)51U));
429     uint64_t l_4 = tmp0 + c4 * (uint64_t)19U;
430     uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
431     uint64_t c5 = l_4 >> (uint32_t)51U;
432     uint64_t o0 = tmp0_;
433     uint64_t o1 = tmp1 + c5;
434     uint64_t o2 = tmp2;
435     uint64_t o3 = tmp3;
436     uint64_t o4 = tmp4;
437     out[0U] = o0;
438     out[1U] = o1;
439     out[2U] = o2;
440     out[3U] = o3;
441     out[4U] = o4;
442 }
443 
444 static inline void
Hacl_Impl_Curve25519_Field51_fsqr2(uint64_t * out,uint64_t * f,FStar_UInt128_uint128 * uu___)445 Hacl_Impl_Curve25519_Field51_fsqr2(uint64_t *out, uint64_t *f, FStar_UInt128_uint128 *uu___)
446 {
447     uint64_t f10 = f[0U];
448     uint64_t f11 = f[1U];
449     uint64_t f12 = f[2U];
450     uint64_t f13 = f[3U];
451     uint64_t f14 = f[4U];
452     uint64_t f20 = f[5U];
453     uint64_t f21 = f[6U];
454     uint64_t f22 = f[7U];
455     uint64_t f23 = f[8U];
456     uint64_t f24 = f[9U];
457     uint64_t d00 = (uint64_t)2U * f10;
458     uint64_t d10 = (uint64_t)2U * f11;
459     uint64_t d20 = (uint64_t)38U * f12;
460     uint64_t d30 = (uint64_t)19U * f13;
461     uint64_t d4190 = (uint64_t)19U * f14;
462     uint64_t d40 = (uint64_t)2U * d4190;
463     FStar_UInt128_uint128
464         s00 =
465             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(f10, f10),
466                                                 FStar_UInt128_mul_wide(d40, f11)),
467                               FStar_UInt128_mul_wide(d20, f13));
468     FStar_UInt128_uint128
469         s10 =
470             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d00, f11),
471                                                 FStar_UInt128_mul_wide(d40, f12)),
472                               FStar_UInt128_mul_wide(d30, f13));
473     FStar_UInt128_uint128
474         s20 =
475             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d00, f12),
476                                                 FStar_UInt128_mul_wide(f11, f11)),
477                               FStar_UInt128_mul_wide(d40, f13));
478     FStar_UInt128_uint128
479         s30 =
480             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d00, f13),
481                                                 FStar_UInt128_mul_wide(d10, f12)),
482                               FStar_UInt128_mul_wide(f14, d4190));
483     FStar_UInt128_uint128
484         s40 =
485             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d00, f14),
486                                                 FStar_UInt128_mul_wide(d10, f13)),
487                               FStar_UInt128_mul_wide(f12, f12));
488     FStar_UInt128_uint128 o100 = s00;
489     FStar_UInt128_uint128 o110 = s10;
490     FStar_UInt128_uint128 o120 = s20;
491     FStar_UInt128_uint128 o130 = s30;
492     FStar_UInt128_uint128 o140 = s40;
493     uint64_t d0 = (uint64_t)2U * f20;
494     uint64_t d1 = (uint64_t)2U * f21;
495     uint64_t d2 = (uint64_t)38U * f22;
496     uint64_t d3 = (uint64_t)19U * f23;
497     uint64_t d419 = (uint64_t)19U * f24;
498     uint64_t d4 = (uint64_t)2U * d419;
499     FStar_UInt128_uint128
500         s0 =
501             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(f20, f20),
502                                                 FStar_UInt128_mul_wide(d4, f21)),
503                               FStar_UInt128_mul_wide(d2, f23));
504     FStar_UInt128_uint128
505         s1 =
506             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f21),
507                                                 FStar_UInt128_mul_wide(d4, f22)),
508                               FStar_UInt128_mul_wide(d3, f23));
509     FStar_UInt128_uint128
510         s2 =
511             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f22),
512                                                 FStar_UInt128_mul_wide(f21, f21)),
513                               FStar_UInt128_mul_wide(d4, f23));
514     FStar_UInt128_uint128
515         s3 =
516             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f23),
517                                                 FStar_UInt128_mul_wide(d1, f22)),
518                               FStar_UInt128_mul_wide(f24, d419));
519     FStar_UInt128_uint128
520         s4 =
521             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f24),
522                                                 FStar_UInt128_mul_wide(d1, f23)),
523                               FStar_UInt128_mul_wide(f22, f22));
524     FStar_UInt128_uint128 o200 = s0;
525     FStar_UInt128_uint128 o210 = s1;
526     FStar_UInt128_uint128 o220 = s2;
527     FStar_UInt128_uint128 o230 = s3;
528     FStar_UInt128_uint128 o240 = s4;
529     FStar_UInt128_uint128
530         l_ = FStar_UInt128_add(o100, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
531     uint64_t tmp00 = FStar_UInt128_uint128_to_uint64(l_) & (uint64_t)0x7ffffffffffffU;
532     uint64_t c00 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_, (uint32_t)51U));
533     FStar_UInt128_uint128 l_0 = FStar_UInt128_add(o110, FStar_UInt128_uint64_to_uint128(c00));
534     uint64_t tmp10 = FStar_UInt128_uint128_to_uint64(l_0) & (uint64_t)0x7ffffffffffffU;
535     uint64_t c10 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_0, (uint32_t)51U));
536     FStar_UInt128_uint128 l_1 = FStar_UInt128_add(o120, FStar_UInt128_uint64_to_uint128(c10));
537     uint64_t tmp20 = FStar_UInt128_uint128_to_uint64(l_1) & (uint64_t)0x7ffffffffffffU;
538     uint64_t c20 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_1, (uint32_t)51U));
539     FStar_UInt128_uint128 l_2 = FStar_UInt128_add(o130, FStar_UInt128_uint64_to_uint128(c20));
540     uint64_t tmp30 = FStar_UInt128_uint128_to_uint64(l_2) & (uint64_t)0x7ffffffffffffU;
541     uint64_t c30 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_2, (uint32_t)51U));
542     FStar_UInt128_uint128 l_3 = FStar_UInt128_add(o140, FStar_UInt128_uint64_to_uint128(c30));
543     uint64_t tmp40 = FStar_UInt128_uint128_to_uint64(l_3) & (uint64_t)0x7ffffffffffffU;
544     uint64_t c40 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_3, (uint32_t)51U));
545     uint64_t l_4 = tmp00 + c40 * (uint64_t)19U;
546     uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
547     uint64_t c50 = l_4 >> (uint32_t)51U;
548     uint64_t o101 = tmp0_;
549     uint64_t o111 = tmp10 + c50;
550     uint64_t o121 = tmp20;
551     uint64_t o131 = tmp30;
552     uint64_t o141 = tmp40;
553     FStar_UInt128_uint128
554         l_5 = FStar_UInt128_add(o200, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
555     uint64_t tmp0 = FStar_UInt128_uint128_to_uint64(l_5) & (uint64_t)0x7ffffffffffffU;
556     uint64_t c0 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_5, (uint32_t)51U));
557     FStar_UInt128_uint128 l_6 = FStar_UInt128_add(o210, FStar_UInt128_uint64_to_uint128(c0));
558     uint64_t tmp1 = FStar_UInt128_uint128_to_uint64(l_6) & (uint64_t)0x7ffffffffffffU;
559     uint64_t c1 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_6, (uint32_t)51U));
560     FStar_UInt128_uint128 l_7 = FStar_UInt128_add(o220, FStar_UInt128_uint64_to_uint128(c1));
561     uint64_t tmp2 = FStar_UInt128_uint128_to_uint64(l_7) & (uint64_t)0x7ffffffffffffU;
562     uint64_t c2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_7, (uint32_t)51U));
563     FStar_UInt128_uint128 l_8 = FStar_UInt128_add(o230, FStar_UInt128_uint64_to_uint128(c2));
564     uint64_t tmp3 = FStar_UInt128_uint128_to_uint64(l_8) & (uint64_t)0x7ffffffffffffU;
565     uint64_t c3 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_8, (uint32_t)51U));
566     FStar_UInt128_uint128 l_9 = FStar_UInt128_add(o240, FStar_UInt128_uint64_to_uint128(c3));
567     uint64_t tmp4 = FStar_UInt128_uint128_to_uint64(l_9) & (uint64_t)0x7ffffffffffffU;
568     uint64_t c4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_9, (uint32_t)51U));
569     uint64_t l_10 = tmp0 + c4 * (uint64_t)19U;
570     uint64_t tmp0_0 = l_10 & (uint64_t)0x7ffffffffffffU;
571     uint64_t c5 = l_10 >> (uint32_t)51U;
572     uint64_t o201 = tmp0_0;
573     uint64_t o211 = tmp1 + c5;
574     uint64_t o221 = tmp2;
575     uint64_t o231 = tmp3;
576     uint64_t o241 = tmp4;
577     uint64_t o10 = o101;
578     uint64_t o11 = o111;
579     uint64_t o12 = o121;
580     uint64_t o13 = o131;
581     uint64_t o14 = o141;
582     uint64_t o20 = o201;
583     uint64_t o21 = o211;
584     uint64_t o22 = o221;
585     uint64_t o23 = o231;
586     uint64_t o24 = o241;
587     out[0U] = o10;
588     out[1U] = o11;
589     out[2U] = o12;
590     out[3U] = o13;
591     out[4U] = o14;
592     out[5U] = o20;
593     out[6U] = o21;
594     out[7U] = o22;
595     out[8U] = o23;
596     out[9U] = o24;
597 }
598 
599 static inline void
Hacl_Impl_Curve25519_Field51_store_felem(uint64_t * u64s,uint64_t * f)600 Hacl_Impl_Curve25519_Field51_store_felem(uint64_t *u64s, uint64_t *f)
601 {
602     uint64_t f0 = f[0U];
603     uint64_t f1 = f[1U];
604     uint64_t f2 = f[2U];
605     uint64_t f3 = f[3U];
606     uint64_t f4 = f[4U];
607     uint64_t l_ = f0 + (uint64_t)0U;
608     uint64_t tmp0 = l_ & (uint64_t)0x7ffffffffffffU;
609     uint64_t c0 = l_ >> (uint32_t)51U;
610     uint64_t l_0 = f1 + c0;
611     uint64_t tmp1 = l_0 & (uint64_t)0x7ffffffffffffU;
612     uint64_t c1 = l_0 >> (uint32_t)51U;
613     uint64_t l_1 = f2 + c1;
614     uint64_t tmp2 = l_1 & (uint64_t)0x7ffffffffffffU;
615     uint64_t c2 = l_1 >> (uint32_t)51U;
616     uint64_t l_2 = f3 + c2;
617     uint64_t tmp3 = l_2 & (uint64_t)0x7ffffffffffffU;
618     uint64_t c3 = l_2 >> (uint32_t)51U;
619     uint64_t l_3 = f4 + c3;
620     uint64_t tmp4 = l_3 & (uint64_t)0x7ffffffffffffU;
621     uint64_t c4 = l_3 >> (uint32_t)51U;
622     uint64_t l_4 = tmp0 + c4 * (uint64_t)19U;
623     uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
624     uint64_t c5 = l_4 >> (uint32_t)51U;
625     uint64_t f01 = tmp0_;
626     uint64_t f11 = tmp1 + c5;
627     uint64_t f21 = tmp2;
628     uint64_t f31 = tmp3;
629     uint64_t f41 = tmp4;
630     uint64_t m0 = FStar_UInt64_gte_mask(f01, (uint64_t)0x7ffffffffffedU);
631     uint64_t m1 = FStar_UInt64_eq_mask(f11, (uint64_t)0x7ffffffffffffU);
632     uint64_t m2 = FStar_UInt64_eq_mask(f21, (uint64_t)0x7ffffffffffffU);
633     uint64_t m3 = FStar_UInt64_eq_mask(f31, (uint64_t)0x7ffffffffffffU);
634     uint64_t m4 = FStar_UInt64_eq_mask(f41, (uint64_t)0x7ffffffffffffU);
635     uint64_t mask = (((m0 & m1) & m2) & m3) & m4;
636     uint64_t f0_ = f01 - (mask & (uint64_t)0x7ffffffffffedU);
637     uint64_t f1_ = f11 - (mask & (uint64_t)0x7ffffffffffffU);
638     uint64_t f2_ = f21 - (mask & (uint64_t)0x7ffffffffffffU);
639     uint64_t f3_ = f31 - (mask & (uint64_t)0x7ffffffffffffU);
640     uint64_t f4_ = f41 - (mask & (uint64_t)0x7ffffffffffffU);
641     uint64_t f02 = f0_;
642     uint64_t f12 = f1_;
643     uint64_t f22 = f2_;
644     uint64_t f32 = f3_;
645     uint64_t f42 = f4_;
646     uint64_t o00 = f02 | f12 << (uint32_t)51U;
647     uint64_t o10 = f12 >> (uint32_t)13U | f22 << (uint32_t)38U;
648     uint64_t o20 = f22 >> (uint32_t)26U | f32 << (uint32_t)25U;
649     uint64_t o30 = f32 >> (uint32_t)39U | f42 << (uint32_t)12U;
650     uint64_t o0 = o00;
651     uint64_t o1 = o10;
652     uint64_t o2 = o20;
653     uint64_t o3 = o30;
654     u64s[0U] = o0;
655     u64s[1U] = o1;
656     u64s[2U] = o2;
657     u64s[3U] = o3;
658 }
659 
660 static inline void
Hacl_Impl_Curve25519_Field51_cswap2(uint64_t bit,uint64_t * p1,uint64_t * p2)661 Hacl_Impl_Curve25519_Field51_cswap2(uint64_t bit, uint64_t *p1, uint64_t *p2)
662 {
663     uint64_t mask = (uint64_t)0U - bit;
664     for (uint32_t i = (uint32_t)0U; i < (uint32_t)10U; i++) {
665         uint64_t dummy = mask & (p1[i] ^ p2[i]);
666         p1[i] = p1[i] ^ dummy;
667         p2[i] = p2[i] ^ dummy;
668     }
669 }
670 
671 #if defined(__cplusplus)
672 }
673 #endif
674 
675 #define __Hacl_Bignum25519_51_H_DEFINED
676 #endif
677