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 #include "Hacl_Curve25519_51.h"
25 
26 static inline void
fadd0(uint64_t * out,uint64_t * f1,uint64_t * f2)27 fadd0(uint64_t *out, uint64_t *f1, uint64_t *f2)
28 {
29     uint64_t f10 = f1[0U];
30     uint64_t f20 = f2[0U];
31     uint64_t f11 = f1[1U];
32     uint64_t f21 = f2[1U];
33     uint64_t f12 = f1[2U];
34     uint64_t f22 = f2[2U];
35     uint64_t f13 = f1[3U];
36     uint64_t f23 = f2[3U];
37     uint64_t f14 = f1[4U];
38     uint64_t f24 = f2[4U];
39     out[0U] = f10 + f20;
40     out[1U] = f11 + f21;
41     out[2U] = f12 + f22;
42     out[3U] = f13 + f23;
43     out[4U] = f14 + f24;
44 }
45 
46 static inline void
fsub0(uint64_t * out,uint64_t * f1,uint64_t * f2)47 fsub0(uint64_t *out, uint64_t *f1, uint64_t *f2)
48 {
49     uint64_t f10 = f1[0U];
50     uint64_t f20 = f2[0U];
51     uint64_t f11 = f1[1U];
52     uint64_t f21 = f2[1U];
53     uint64_t f12 = f1[2U];
54     uint64_t f22 = f2[2U];
55     uint64_t f13 = f1[3U];
56     uint64_t f23 = f2[3U];
57     uint64_t f14 = f1[4U];
58     uint64_t f24 = f2[4U];
59     out[0U] = f10 + (uint64_t)0x3fffffffffff68U - f20;
60     out[1U] = f11 + (uint64_t)0x3ffffffffffff8U - f21;
61     out[2U] = f12 + (uint64_t)0x3ffffffffffff8U - f22;
62     out[3U] = f13 + (uint64_t)0x3ffffffffffff8U - f23;
63     out[4U] = f14 + (uint64_t)0x3ffffffffffff8U - f24;
64 }
65 
66 static inline void
fmul0(uint64_t * out,uint64_t * f1,uint64_t * f2)67 fmul0(uint64_t *out, uint64_t *f1, uint64_t *f2)
68 {
69     uint64_t f10 = f1[0U];
70     uint64_t f11 = f1[1U];
71     uint64_t f12 = f1[2U];
72     uint64_t f13 = f1[3U];
73     uint64_t f14 = f1[4U];
74     uint64_t f20 = f2[0U];
75     uint64_t f21 = f2[1U];
76     uint64_t f22 = f2[2U];
77     uint64_t f23 = f2[3U];
78     uint64_t f24 = f2[4U];
79     uint64_t tmp1 = f21 * (uint64_t)19U;
80     uint64_t tmp2 = f22 * (uint64_t)19U;
81     uint64_t tmp3 = f23 * (uint64_t)19U;
82     uint64_t tmp4 = f24 * (uint64_t)19U;
83     FStar_UInt128_uint128 o00 = FStar_UInt128_mul_wide(f10, f20);
84     FStar_UInt128_uint128 o10 = FStar_UInt128_mul_wide(f10, f21);
85     FStar_UInt128_uint128 o20 = FStar_UInt128_mul_wide(f10, f22);
86     FStar_UInt128_uint128 o30 = FStar_UInt128_mul_wide(f10, f23);
87     FStar_UInt128_uint128 o40 = FStar_UInt128_mul_wide(f10, f24);
88     FStar_UInt128_uint128 o01 = FStar_UInt128_add(o00, FStar_UInt128_mul_wide(f11, tmp4));
89     FStar_UInt128_uint128 o11 = FStar_UInt128_add(o10, FStar_UInt128_mul_wide(f11, f20));
90     FStar_UInt128_uint128 o21 = FStar_UInt128_add(o20, FStar_UInt128_mul_wide(f11, f21));
91     FStar_UInt128_uint128 o31 = FStar_UInt128_add(o30, FStar_UInt128_mul_wide(f11, f22));
92     FStar_UInt128_uint128 o41 = FStar_UInt128_add(o40, FStar_UInt128_mul_wide(f11, f23));
93     FStar_UInt128_uint128 o02 = FStar_UInt128_add(o01, FStar_UInt128_mul_wide(f12, tmp3));
94     FStar_UInt128_uint128 o12 = FStar_UInt128_add(o11, FStar_UInt128_mul_wide(f12, tmp4));
95     FStar_UInt128_uint128 o22 = FStar_UInt128_add(o21, FStar_UInt128_mul_wide(f12, f20));
96     FStar_UInt128_uint128 o32 = FStar_UInt128_add(o31, FStar_UInt128_mul_wide(f12, f21));
97     FStar_UInt128_uint128 o42 = FStar_UInt128_add(o41, FStar_UInt128_mul_wide(f12, f22));
98     FStar_UInt128_uint128 o03 = FStar_UInt128_add(o02, FStar_UInt128_mul_wide(f13, tmp2));
99     FStar_UInt128_uint128 o13 = FStar_UInt128_add(o12, FStar_UInt128_mul_wide(f13, tmp3));
100     FStar_UInt128_uint128 o23 = FStar_UInt128_add(o22, FStar_UInt128_mul_wide(f13, tmp4));
101     FStar_UInt128_uint128 o33 = FStar_UInt128_add(o32, FStar_UInt128_mul_wide(f13, f20));
102     FStar_UInt128_uint128 o43 = FStar_UInt128_add(o42, FStar_UInt128_mul_wide(f13, f21));
103     FStar_UInt128_uint128 o04 = FStar_UInt128_add(o03, FStar_UInt128_mul_wide(f14, tmp1));
104     FStar_UInt128_uint128 o14 = FStar_UInt128_add(o13, FStar_UInt128_mul_wide(f14, tmp2));
105     FStar_UInt128_uint128 o24 = FStar_UInt128_add(o23, FStar_UInt128_mul_wide(f14, tmp3));
106     FStar_UInt128_uint128 o34 = FStar_UInt128_add(o33, FStar_UInt128_mul_wide(f14, tmp4));
107     FStar_UInt128_uint128 o44 = FStar_UInt128_add(o43, FStar_UInt128_mul_wide(f14, f20));
108     FStar_UInt128_uint128 tmp_w0 = o04;
109     FStar_UInt128_uint128 tmp_w1 = o14;
110     FStar_UInt128_uint128 tmp_w2 = o24;
111     FStar_UInt128_uint128 tmp_w3 = o34;
112     FStar_UInt128_uint128 tmp_w4 = o44;
113     FStar_UInt128_uint128
114         l_ = FStar_UInt128_add(tmp_w0, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
115     uint64_t tmp01 = FStar_UInt128_uint128_to_uint64(l_) & (uint64_t)0x7ffffffffffffU;
116     uint64_t c0 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_, (uint32_t)51U));
117     FStar_UInt128_uint128 l_0 = FStar_UInt128_add(tmp_w1, FStar_UInt128_uint64_to_uint128(c0));
118     uint64_t tmp11 = FStar_UInt128_uint128_to_uint64(l_0) & (uint64_t)0x7ffffffffffffU;
119     uint64_t c1 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_0, (uint32_t)51U));
120     FStar_UInt128_uint128 l_1 = FStar_UInt128_add(tmp_w2, FStar_UInt128_uint64_to_uint128(c1));
121     uint64_t tmp21 = FStar_UInt128_uint128_to_uint64(l_1) & (uint64_t)0x7ffffffffffffU;
122     uint64_t c2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_1, (uint32_t)51U));
123     FStar_UInt128_uint128 l_2 = FStar_UInt128_add(tmp_w3, FStar_UInt128_uint64_to_uint128(c2));
124     uint64_t tmp31 = FStar_UInt128_uint128_to_uint64(l_2) & (uint64_t)0x7ffffffffffffU;
125     uint64_t c3 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_2, (uint32_t)51U));
126     FStar_UInt128_uint128 l_3 = FStar_UInt128_add(tmp_w4, FStar_UInt128_uint64_to_uint128(c3));
127     uint64_t tmp41 = FStar_UInt128_uint128_to_uint64(l_3) & (uint64_t)0x7ffffffffffffU;
128     uint64_t c4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_3, (uint32_t)51U));
129     uint64_t l_4 = tmp01 + c4 * (uint64_t)19U;
130     uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
131     uint64_t c5 = l_4 >> (uint32_t)51U;
132     uint64_t o0 = tmp0_;
133     uint64_t o1 = tmp11 + c5;
134     uint64_t o2 = tmp21;
135     uint64_t o3 = tmp31;
136     uint64_t o4 = tmp41;
137     out[0U] = o0;
138     out[1U] = o1;
139     out[2U] = o2;
140     out[3U] = o3;
141     out[4U] = o4;
142 }
143 
144 static inline void
fmul20(uint64_t * out,uint64_t * f1,uint64_t * f2)145 fmul20(uint64_t *out, uint64_t *f1, uint64_t *f2)
146 {
147     uint64_t f10 = f1[0U];
148     uint64_t f11 = f1[1U];
149     uint64_t f12 = f1[2U];
150     uint64_t f13 = f1[3U];
151     uint64_t f14 = f1[4U];
152     uint64_t f20 = f2[0U];
153     uint64_t f21 = f2[1U];
154     uint64_t f22 = f2[2U];
155     uint64_t f23 = f2[3U];
156     uint64_t f24 = f2[4U];
157     uint64_t f30 = f1[5U];
158     uint64_t f31 = f1[6U];
159     uint64_t f32 = f1[7U];
160     uint64_t f33 = f1[8U];
161     uint64_t f34 = f1[9U];
162     uint64_t f40 = f2[5U];
163     uint64_t f41 = f2[6U];
164     uint64_t f42 = f2[7U];
165     uint64_t f43 = f2[8U];
166     uint64_t f44 = f2[9U];
167     uint64_t tmp11 = f21 * (uint64_t)19U;
168     uint64_t tmp12 = f22 * (uint64_t)19U;
169     uint64_t tmp13 = f23 * (uint64_t)19U;
170     uint64_t tmp14 = f24 * (uint64_t)19U;
171     uint64_t tmp21 = f41 * (uint64_t)19U;
172     uint64_t tmp22 = f42 * (uint64_t)19U;
173     uint64_t tmp23 = f43 * (uint64_t)19U;
174     uint64_t tmp24 = f44 * (uint64_t)19U;
175     FStar_UInt128_uint128 o00 = FStar_UInt128_mul_wide(f10, f20);
176     FStar_UInt128_uint128 o15 = FStar_UInt128_mul_wide(f10, f21);
177     FStar_UInt128_uint128 o25 = FStar_UInt128_mul_wide(f10, f22);
178     FStar_UInt128_uint128 o30 = FStar_UInt128_mul_wide(f10, f23);
179     FStar_UInt128_uint128 o40 = FStar_UInt128_mul_wide(f10, f24);
180     FStar_UInt128_uint128 o010 = FStar_UInt128_add(o00, FStar_UInt128_mul_wide(f11, tmp14));
181     FStar_UInt128_uint128 o110 = FStar_UInt128_add(o15, FStar_UInt128_mul_wide(f11, f20));
182     FStar_UInt128_uint128 o210 = FStar_UInt128_add(o25, FStar_UInt128_mul_wide(f11, f21));
183     FStar_UInt128_uint128 o310 = FStar_UInt128_add(o30, FStar_UInt128_mul_wide(f11, f22));
184     FStar_UInt128_uint128 o410 = FStar_UInt128_add(o40, FStar_UInt128_mul_wide(f11, f23));
185     FStar_UInt128_uint128 o020 = FStar_UInt128_add(o010, FStar_UInt128_mul_wide(f12, tmp13));
186     FStar_UInt128_uint128 o120 = FStar_UInt128_add(o110, FStar_UInt128_mul_wide(f12, tmp14));
187     FStar_UInt128_uint128 o220 = FStar_UInt128_add(o210, FStar_UInt128_mul_wide(f12, f20));
188     FStar_UInt128_uint128 o320 = FStar_UInt128_add(o310, FStar_UInt128_mul_wide(f12, f21));
189     FStar_UInt128_uint128 o420 = FStar_UInt128_add(o410, FStar_UInt128_mul_wide(f12, f22));
190     FStar_UInt128_uint128 o030 = FStar_UInt128_add(o020, FStar_UInt128_mul_wide(f13, tmp12));
191     FStar_UInt128_uint128 o130 = FStar_UInt128_add(o120, FStar_UInt128_mul_wide(f13, tmp13));
192     FStar_UInt128_uint128 o230 = FStar_UInt128_add(o220, FStar_UInt128_mul_wide(f13, tmp14));
193     FStar_UInt128_uint128 o330 = FStar_UInt128_add(o320, FStar_UInt128_mul_wide(f13, f20));
194     FStar_UInt128_uint128 o430 = FStar_UInt128_add(o420, FStar_UInt128_mul_wide(f13, f21));
195     FStar_UInt128_uint128 o040 = FStar_UInt128_add(o030, FStar_UInt128_mul_wide(f14, tmp11));
196     FStar_UInt128_uint128 o140 = FStar_UInt128_add(o130, FStar_UInt128_mul_wide(f14, tmp12));
197     FStar_UInt128_uint128 o240 = FStar_UInt128_add(o230, FStar_UInt128_mul_wide(f14, tmp13));
198     FStar_UInt128_uint128 o340 = FStar_UInt128_add(o330, FStar_UInt128_mul_wide(f14, tmp14));
199     FStar_UInt128_uint128 o440 = FStar_UInt128_add(o430, FStar_UInt128_mul_wide(f14, f20));
200     FStar_UInt128_uint128 tmp_w10 = o040;
201     FStar_UInt128_uint128 tmp_w11 = o140;
202     FStar_UInt128_uint128 tmp_w12 = o240;
203     FStar_UInt128_uint128 tmp_w13 = o340;
204     FStar_UInt128_uint128 tmp_w14 = o440;
205     FStar_UInt128_uint128 o0 = FStar_UInt128_mul_wide(f30, f40);
206     FStar_UInt128_uint128 o1 = FStar_UInt128_mul_wide(f30, f41);
207     FStar_UInt128_uint128 o2 = FStar_UInt128_mul_wide(f30, f42);
208     FStar_UInt128_uint128 o3 = FStar_UInt128_mul_wide(f30, f43);
209     FStar_UInt128_uint128 o4 = FStar_UInt128_mul_wide(f30, f44);
210     FStar_UInt128_uint128 o01 = FStar_UInt128_add(o0, FStar_UInt128_mul_wide(f31, tmp24));
211     FStar_UInt128_uint128 o111 = FStar_UInt128_add(o1, FStar_UInt128_mul_wide(f31, f40));
212     FStar_UInt128_uint128 o211 = FStar_UInt128_add(o2, FStar_UInt128_mul_wide(f31, f41));
213     FStar_UInt128_uint128 o31 = FStar_UInt128_add(o3, FStar_UInt128_mul_wide(f31, f42));
214     FStar_UInt128_uint128 o41 = FStar_UInt128_add(o4, FStar_UInt128_mul_wide(f31, f43));
215     FStar_UInt128_uint128 o02 = FStar_UInt128_add(o01, FStar_UInt128_mul_wide(f32, tmp23));
216     FStar_UInt128_uint128 o121 = FStar_UInt128_add(o111, FStar_UInt128_mul_wide(f32, tmp24));
217     FStar_UInt128_uint128 o221 = FStar_UInt128_add(o211, FStar_UInt128_mul_wide(f32, f40));
218     FStar_UInt128_uint128 o32 = FStar_UInt128_add(o31, FStar_UInt128_mul_wide(f32, f41));
219     FStar_UInt128_uint128 o42 = FStar_UInt128_add(o41, FStar_UInt128_mul_wide(f32, f42));
220     FStar_UInt128_uint128 o03 = FStar_UInt128_add(o02, FStar_UInt128_mul_wide(f33, tmp22));
221     FStar_UInt128_uint128 o131 = FStar_UInt128_add(o121, FStar_UInt128_mul_wide(f33, tmp23));
222     FStar_UInt128_uint128 o231 = FStar_UInt128_add(o221, FStar_UInt128_mul_wide(f33, tmp24));
223     FStar_UInt128_uint128 o33 = FStar_UInt128_add(o32, FStar_UInt128_mul_wide(f33, f40));
224     FStar_UInt128_uint128 o43 = FStar_UInt128_add(o42, FStar_UInt128_mul_wide(f33, f41));
225     FStar_UInt128_uint128 o04 = FStar_UInt128_add(o03, FStar_UInt128_mul_wide(f34, tmp21));
226     FStar_UInt128_uint128 o141 = FStar_UInt128_add(o131, FStar_UInt128_mul_wide(f34, tmp22));
227     FStar_UInt128_uint128 o241 = FStar_UInt128_add(o231, FStar_UInt128_mul_wide(f34, tmp23));
228     FStar_UInt128_uint128 o34 = FStar_UInt128_add(o33, FStar_UInt128_mul_wide(f34, tmp24));
229     FStar_UInt128_uint128 o44 = FStar_UInt128_add(o43, FStar_UInt128_mul_wide(f34, f40));
230     FStar_UInt128_uint128 tmp_w20 = o04;
231     FStar_UInt128_uint128 tmp_w21 = o141;
232     FStar_UInt128_uint128 tmp_w22 = o241;
233     FStar_UInt128_uint128 tmp_w23 = o34;
234     FStar_UInt128_uint128 tmp_w24 = o44;
235     FStar_UInt128_uint128
236         l_ = FStar_UInt128_add(tmp_w10, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
237     uint64_t tmp00 = FStar_UInt128_uint128_to_uint64(l_) & (uint64_t)0x7ffffffffffffU;
238     uint64_t c00 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_, (uint32_t)51U));
239     FStar_UInt128_uint128 l_0 = FStar_UInt128_add(tmp_w11, FStar_UInt128_uint64_to_uint128(c00));
240     uint64_t tmp10 = FStar_UInt128_uint128_to_uint64(l_0) & (uint64_t)0x7ffffffffffffU;
241     uint64_t c10 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_0, (uint32_t)51U));
242     FStar_UInt128_uint128 l_1 = FStar_UInt128_add(tmp_w12, FStar_UInt128_uint64_to_uint128(c10));
243     uint64_t tmp20 = FStar_UInt128_uint128_to_uint64(l_1) & (uint64_t)0x7ffffffffffffU;
244     uint64_t c20 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_1, (uint32_t)51U));
245     FStar_UInt128_uint128 l_2 = FStar_UInt128_add(tmp_w13, FStar_UInt128_uint64_to_uint128(c20));
246     uint64_t tmp30 = FStar_UInt128_uint128_to_uint64(l_2) & (uint64_t)0x7ffffffffffffU;
247     uint64_t c30 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_2, (uint32_t)51U));
248     FStar_UInt128_uint128 l_3 = FStar_UInt128_add(tmp_w14, FStar_UInt128_uint64_to_uint128(c30));
249     uint64_t tmp40 = FStar_UInt128_uint128_to_uint64(l_3) & (uint64_t)0x7ffffffffffffU;
250     uint64_t c40 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_3, (uint32_t)51U));
251     uint64_t l_4 = tmp00 + c40 * (uint64_t)19U;
252     uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
253     uint64_t c50 = l_4 >> (uint32_t)51U;
254     uint64_t o100 = tmp0_;
255     uint64_t o112 = tmp10 + c50;
256     uint64_t o122 = tmp20;
257     uint64_t o132 = tmp30;
258     uint64_t o142 = tmp40;
259     FStar_UInt128_uint128
260         l_5 = FStar_UInt128_add(tmp_w20, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
261     uint64_t tmp0 = FStar_UInt128_uint128_to_uint64(l_5) & (uint64_t)0x7ffffffffffffU;
262     uint64_t c0 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_5, (uint32_t)51U));
263     FStar_UInt128_uint128 l_6 = FStar_UInt128_add(tmp_w21, FStar_UInt128_uint64_to_uint128(c0));
264     uint64_t tmp1 = FStar_UInt128_uint128_to_uint64(l_6) & (uint64_t)0x7ffffffffffffU;
265     uint64_t c1 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_6, (uint32_t)51U));
266     FStar_UInt128_uint128 l_7 = FStar_UInt128_add(tmp_w22, FStar_UInt128_uint64_to_uint128(c1));
267     uint64_t tmp2 = FStar_UInt128_uint128_to_uint64(l_7) & (uint64_t)0x7ffffffffffffU;
268     uint64_t c2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_7, (uint32_t)51U));
269     FStar_UInt128_uint128 l_8 = FStar_UInt128_add(tmp_w23, FStar_UInt128_uint64_to_uint128(c2));
270     uint64_t tmp3 = FStar_UInt128_uint128_to_uint64(l_8) & (uint64_t)0x7ffffffffffffU;
271     uint64_t c3 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_8, (uint32_t)51U));
272     FStar_UInt128_uint128 l_9 = FStar_UInt128_add(tmp_w24, FStar_UInt128_uint64_to_uint128(c3));
273     uint64_t tmp4 = FStar_UInt128_uint128_to_uint64(l_9) & (uint64_t)0x7ffffffffffffU;
274     uint64_t c4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_9, (uint32_t)51U));
275     uint64_t l_10 = tmp0 + c4 * (uint64_t)19U;
276     uint64_t tmp0_0 = l_10 & (uint64_t)0x7ffffffffffffU;
277     uint64_t c5 = l_10 >> (uint32_t)51U;
278     uint64_t o200 = tmp0_0;
279     uint64_t o212 = tmp1 + c5;
280     uint64_t o222 = tmp2;
281     uint64_t o232 = tmp3;
282     uint64_t o242 = tmp4;
283     uint64_t o10 = o100;
284     uint64_t o11 = o112;
285     uint64_t o12 = o122;
286     uint64_t o13 = o132;
287     uint64_t o14 = o142;
288     uint64_t o20 = o200;
289     uint64_t o21 = o212;
290     uint64_t o22 = o222;
291     uint64_t o23 = o232;
292     uint64_t o24 = o242;
293     out[0U] = o10;
294     out[1U] = o11;
295     out[2U] = o12;
296     out[3U] = o13;
297     out[4U] = o14;
298     out[5U] = o20;
299     out[6U] = o21;
300     out[7U] = o22;
301     out[8U] = o23;
302     out[9U] = o24;
303 }
304 
305 static inline void
fmul1(uint64_t * out,uint64_t * f1,uint64_t f2)306 fmul1(uint64_t *out, uint64_t *f1, uint64_t f2)
307 {
308     uint64_t f10 = f1[0U];
309     uint64_t f11 = f1[1U];
310     uint64_t f12 = f1[2U];
311     uint64_t f13 = f1[3U];
312     uint64_t f14 = f1[4U];
313     FStar_UInt128_uint128 tmp_w0 = FStar_UInt128_mul_wide(f2, f10);
314     FStar_UInt128_uint128 tmp_w1 = FStar_UInt128_mul_wide(f2, f11);
315     FStar_UInt128_uint128 tmp_w2 = FStar_UInt128_mul_wide(f2, f12);
316     FStar_UInt128_uint128 tmp_w3 = FStar_UInt128_mul_wide(f2, f13);
317     FStar_UInt128_uint128 tmp_w4 = FStar_UInt128_mul_wide(f2, f14);
318     FStar_UInt128_uint128
319         l_ = FStar_UInt128_add(tmp_w0, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
320     uint64_t tmp0 = FStar_UInt128_uint128_to_uint64(l_) & (uint64_t)0x7ffffffffffffU;
321     uint64_t c0 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_, (uint32_t)51U));
322     FStar_UInt128_uint128 l_0 = FStar_UInt128_add(tmp_w1, FStar_UInt128_uint64_to_uint128(c0));
323     uint64_t tmp1 = FStar_UInt128_uint128_to_uint64(l_0) & (uint64_t)0x7ffffffffffffU;
324     uint64_t c1 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_0, (uint32_t)51U));
325     FStar_UInt128_uint128 l_1 = FStar_UInt128_add(tmp_w2, FStar_UInt128_uint64_to_uint128(c1));
326     uint64_t tmp2 = FStar_UInt128_uint128_to_uint64(l_1) & (uint64_t)0x7ffffffffffffU;
327     uint64_t c2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_1, (uint32_t)51U));
328     FStar_UInt128_uint128 l_2 = FStar_UInt128_add(tmp_w3, FStar_UInt128_uint64_to_uint128(c2));
329     uint64_t tmp3 = FStar_UInt128_uint128_to_uint64(l_2) & (uint64_t)0x7ffffffffffffU;
330     uint64_t c3 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_2, (uint32_t)51U));
331     FStar_UInt128_uint128 l_3 = FStar_UInt128_add(tmp_w4, FStar_UInt128_uint64_to_uint128(c3));
332     uint64_t tmp4 = FStar_UInt128_uint128_to_uint64(l_3) & (uint64_t)0x7ffffffffffffU;
333     uint64_t c4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_3, (uint32_t)51U));
334     uint64_t l_4 = tmp0 + c4 * (uint64_t)19U;
335     uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
336     uint64_t c5 = l_4 >> (uint32_t)51U;
337     uint64_t o0 = tmp0_;
338     uint64_t o1 = tmp1 + c5;
339     uint64_t o2 = tmp2;
340     uint64_t o3 = tmp3;
341     uint64_t o4 = tmp4;
342     out[0U] = o0;
343     out[1U] = o1;
344     out[2U] = o2;
345     out[3U] = o3;
346     out[4U] = o4;
347 }
348 
349 static inline void
fsqr0(uint64_t * out,uint64_t * f)350 fsqr0(uint64_t *out, uint64_t *f)
351 {
352     uint64_t f0 = f[0U];
353     uint64_t f1 = f[1U];
354     uint64_t f2 = f[2U];
355     uint64_t f3 = f[3U];
356     uint64_t f4 = f[4U];
357     uint64_t d0 = (uint64_t)2U * f0;
358     uint64_t d1 = (uint64_t)2U * f1;
359     uint64_t d2 = (uint64_t)38U * f2;
360     uint64_t d3 = (uint64_t)19U * f3;
361     uint64_t d419 = (uint64_t)19U * f4;
362     uint64_t d4 = (uint64_t)2U * d419;
363     FStar_UInt128_uint128
364         s0 =
365             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(f0, f0),
366                                                 FStar_UInt128_mul_wide(d4, f1)),
367                               FStar_UInt128_mul_wide(d2, f3));
368     FStar_UInt128_uint128
369         s1 =
370             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f1),
371                                                 FStar_UInt128_mul_wide(d4, f2)),
372                               FStar_UInt128_mul_wide(d3, f3));
373     FStar_UInt128_uint128
374         s2 =
375             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f2),
376                                                 FStar_UInt128_mul_wide(f1, f1)),
377                               FStar_UInt128_mul_wide(d4, f3));
378     FStar_UInt128_uint128
379         s3 =
380             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f3),
381                                                 FStar_UInt128_mul_wide(d1, f2)),
382                               FStar_UInt128_mul_wide(f4, d419));
383     FStar_UInt128_uint128
384         s4 =
385             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f4),
386                                                 FStar_UInt128_mul_wide(d1, f3)),
387                               FStar_UInt128_mul_wide(f2, f2));
388     FStar_UInt128_uint128 o00 = s0;
389     FStar_UInt128_uint128 o10 = s1;
390     FStar_UInt128_uint128 o20 = s2;
391     FStar_UInt128_uint128 o30 = s3;
392     FStar_UInt128_uint128 o40 = s4;
393     FStar_UInt128_uint128
394         l_ = FStar_UInt128_add(o00, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
395     uint64_t tmp0 = FStar_UInt128_uint128_to_uint64(l_) & (uint64_t)0x7ffffffffffffU;
396     uint64_t c0 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_, (uint32_t)51U));
397     FStar_UInt128_uint128 l_0 = FStar_UInt128_add(o10, FStar_UInt128_uint64_to_uint128(c0));
398     uint64_t tmp1 = FStar_UInt128_uint128_to_uint64(l_0) & (uint64_t)0x7ffffffffffffU;
399     uint64_t c1 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_0, (uint32_t)51U));
400     FStar_UInt128_uint128 l_1 = FStar_UInt128_add(o20, FStar_UInt128_uint64_to_uint128(c1));
401     uint64_t tmp2 = FStar_UInt128_uint128_to_uint64(l_1) & (uint64_t)0x7ffffffffffffU;
402     uint64_t c2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_1, (uint32_t)51U));
403     FStar_UInt128_uint128 l_2 = FStar_UInt128_add(o30, FStar_UInt128_uint64_to_uint128(c2));
404     uint64_t tmp3 = FStar_UInt128_uint128_to_uint64(l_2) & (uint64_t)0x7ffffffffffffU;
405     uint64_t c3 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_2, (uint32_t)51U));
406     FStar_UInt128_uint128 l_3 = FStar_UInt128_add(o40, FStar_UInt128_uint64_to_uint128(c3));
407     uint64_t tmp4 = FStar_UInt128_uint128_to_uint64(l_3) & (uint64_t)0x7ffffffffffffU;
408     uint64_t c4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_3, (uint32_t)51U));
409     uint64_t l_4 = tmp0 + c4 * (uint64_t)19U;
410     uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
411     uint64_t c5 = l_4 >> (uint32_t)51U;
412     uint64_t o0 = tmp0_;
413     uint64_t o1 = tmp1 + c5;
414     uint64_t o2 = tmp2;
415     uint64_t o3 = tmp3;
416     uint64_t o4 = tmp4;
417     out[0U] = o0;
418     out[1U] = o1;
419     out[2U] = o2;
420     out[3U] = o3;
421     out[4U] = o4;
422 }
423 
424 static inline void
fsqr20(uint64_t * out,uint64_t * f)425 fsqr20(uint64_t *out, uint64_t *f)
426 {
427     uint64_t f10 = f[0U];
428     uint64_t f11 = f[1U];
429     uint64_t f12 = f[2U];
430     uint64_t f13 = f[3U];
431     uint64_t f14 = f[4U];
432     uint64_t f20 = f[5U];
433     uint64_t f21 = f[6U];
434     uint64_t f22 = f[7U];
435     uint64_t f23 = f[8U];
436     uint64_t f24 = f[9U];
437     uint64_t d00 = (uint64_t)2U * f10;
438     uint64_t d10 = (uint64_t)2U * f11;
439     uint64_t d20 = (uint64_t)38U * f12;
440     uint64_t d30 = (uint64_t)19U * f13;
441     uint64_t d4190 = (uint64_t)19U * f14;
442     uint64_t d40 = (uint64_t)2U * d4190;
443     FStar_UInt128_uint128
444         s00 =
445             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(f10, f10),
446                                                 FStar_UInt128_mul_wide(d40, f11)),
447                               FStar_UInt128_mul_wide(d20, f13));
448     FStar_UInt128_uint128
449         s10 =
450             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d00, f11),
451                                                 FStar_UInt128_mul_wide(d40, f12)),
452                               FStar_UInt128_mul_wide(d30, f13));
453     FStar_UInt128_uint128
454         s20 =
455             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d00, f12),
456                                                 FStar_UInt128_mul_wide(f11, f11)),
457                               FStar_UInt128_mul_wide(d40, f13));
458     FStar_UInt128_uint128
459         s30 =
460             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d00, f13),
461                                                 FStar_UInt128_mul_wide(d10, f12)),
462                               FStar_UInt128_mul_wide(f14, d4190));
463     FStar_UInt128_uint128
464         s40 =
465             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d00, f14),
466                                                 FStar_UInt128_mul_wide(d10, f13)),
467                               FStar_UInt128_mul_wide(f12, f12));
468     FStar_UInt128_uint128 o100 = s00;
469     FStar_UInt128_uint128 o110 = s10;
470     FStar_UInt128_uint128 o120 = s20;
471     FStar_UInt128_uint128 o130 = s30;
472     FStar_UInt128_uint128 o140 = s40;
473     uint64_t d0 = (uint64_t)2U * f20;
474     uint64_t d1 = (uint64_t)2U * f21;
475     uint64_t d2 = (uint64_t)38U * f22;
476     uint64_t d3 = (uint64_t)19U * f23;
477     uint64_t d419 = (uint64_t)19U * f24;
478     uint64_t d4 = (uint64_t)2U * d419;
479     FStar_UInt128_uint128
480         s0 =
481             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(f20, f20),
482                                                 FStar_UInt128_mul_wide(d4, f21)),
483                               FStar_UInt128_mul_wide(d2, f23));
484     FStar_UInt128_uint128
485         s1 =
486             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f21),
487                                                 FStar_UInt128_mul_wide(d4, f22)),
488                               FStar_UInt128_mul_wide(d3, f23));
489     FStar_UInt128_uint128
490         s2 =
491             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f22),
492                                                 FStar_UInt128_mul_wide(f21, f21)),
493                               FStar_UInt128_mul_wide(d4, f23));
494     FStar_UInt128_uint128
495         s3 =
496             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f23),
497                                                 FStar_UInt128_mul_wide(d1, f22)),
498                               FStar_UInt128_mul_wide(f24, d419));
499     FStar_UInt128_uint128
500         s4 =
501             FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f24),
502                                                 FStar_UInt128_mul_wide(d1, f23)),
503                               FStar_UInt128_mul_wide(f22, f22));
504     FStar_UInt128_uint128 o200 = s0;
505     FStar_UInt128_uint128 o210 = s1;
506     FStar_UInt128_uint128 o220 = s2;
507     FStar_UInt128_uint128 o230 = s3;
508     FStar_UInt128_uint128 o240 = s4;
509     FStar_UInt128_uint128
510         l_ = FStar_UInt128_add(o100, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
511     uint64_t tmp00 = FStar_UInt128_uint128_to_uint64(l_) & (uint64_t)0x7ffffffffffffU;
512     uint64_t c00 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_, (uint32_t)51U));
513     FStar_UInt128_uint128 l_0 = FStar_UInt128_add(o110, FStar_UInt128_uint64_to_uint128(c00));
514     uint64_t tmp10 = FStar_UInt128_uint128_to_uint64(l_0) & (uint64_t)0x7ffffffffffffU;
515     uint64_t c10 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_0, (uint32_t)51U));
516     FStar_UInt128_uint128 l_1 = FStar_UInt128_add(o120, FStar_UInt128_uint64_to_uint128(c10));
517     uint64_t tmp20 = FStar_UInt128_uint128_to_uint64(l_1) & (uint64_t)0x7ffffffffffffU;
518     uint64_t c20 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_1, (uint32_t)51U));
519     FStar_UInt128_uint128 l_2 = FStar_UInt128_add(o130, FStar_UInt128_uint64_to_uint128(c20));
520     uint64_t tmp30 = FStar_UInt128_uint128_to_uint64(l_2) & (uint64_t)0x7ffffffffffffU;
521     uint64_t c30 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_2, (uint32_t)51U));
522     FStar_UInt128_uint128 l_3 = FStar_UInt128_add(o140, FStar_UInt128_uint64_to_uint128(c30));
523     uint64_t tmp40 = FStar_UInt128_uint128_to_uint64(l_3) & (uint64_t)0x7ffffffffffffU;
524     uint64_t c40 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_3, (uint32_t)51U));
525     uint64_t l_4 = tmp00 + c40 * (uint64_t)19U;
526     uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
527     uint64_t c50 = l_4 >> (uint32_t)51U;
528     uint64_t o101 = tmp0_;
529     uint64_t o111 = tmp10 + c50;
530     uint64_t o121 = tmp20;
531     uint64_t o131 = tmp30;
532     uint64_t o141 = tmp40;
533     FStar_UInt128_uint128
534         l_5 = FStar_UInt128_add(o200, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
535     uint64_t tmp0 = FStar_UInt128_uint128_to_uint64(l_5) & (uint64_t)0x7ffffffffffffU;
536     uint64_t c0 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_5, (uint32_t)51U));
537     FStar_UInt128_uint128 l_6 = FStar_UInt128_add(o210, FStar_UInt128_uint64_to_uint128(c0));
538     uint64_t tmp1 = FStar_UInt128_uint128_to_uint64(l_6) & (uint64_t)0x7ffffffffffffU;
539     uint64_t c1 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_6, (uint32_t)51U));
540     FStar_UInt128_uint128 l_7 = FStar_UInt128_add(o220, FStar_UInt128_uint64_to_uint128(c1));
541     uint64_t tmp2 = FStar_UInt128_uint128_to_uint64(l_7) & (uint64_t)0x7ffffffffffffU;
542     uint64_t c2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_7, (uint32_t)51U));
543     FStar_UInt128_uint128 l_8 = FStar_UInt128_add(o230, FStar_UInt128_uint64_to_uint128(c2));
544     uint64_t tmp3 = FStar_UInt128_uint128_to_uint64(l_8) & (uint64_t)0x7ffffffffffffU;
545     uint64_t c3 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_8, (uint32_t)51U));
546     FStar_UInt128_uint128 l_9 = FStar_UInt128_add(o240, FStar_UInt128_uint64_to_uint128(c3));
547     uint64_t tmp4 = FStar_UInt128_uint128_to_uint64(l_9) & (uint64_t)0x7ffffffffffffU;
548     uint64_t c4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_9, (uint32_t)51U));
549     uint64_t l_10 = tmp0 + c4 * (uint64_t)19U;
550     uint64_t tmp0_0 = l_10 & (uint64_t)0x7ffffffffffffU;
551     uint64_t c5 = l_10 >> (uint32_t)51U;
552     uint64_t o201 = tmp0_0;
553     uint64_t o211 = tmp1 + c5;
554     uint64_t o221 = tmp2;
555     uint64_t o231 = tmp3;
556     uint64_t o241 = tmp4;
557     uint64_t o10 = o101;
558     uint64_t o11 = o111;
559     uint64_t o12 = o121;
560     uint64_t o13 = o131;
561     uint64_t o14 = o141;
562     uint64_t o20 = o201;
563     uint64_t o21 = o211;
564     uint64_t o22 = o221;
565     uint64_t o23 = o231;
566     uint64_t o24 = o241;
567     out[0U] = o10;
568     out[1U] = o11;
569     out[2U] = o12;
570     out[3U] = o13;
571     out[4U] = o14;
572     out[5U] = o20;
573     out[6U] = o21;
574     out[7U] = o22;
575     out[8U] = o23;
576     out[9U] = o24;
577 }
578 
579 static void
store_felem(uint64_t * u64s,uint64_t * f)580 store_felem(uint64_t *u64s, uint64_t *f)
581 {
582     uint64_t f0 = f[0U];
583     uint64_t f1 = f[1U];
584     uint64_t f2 = f[2U];
585     uint64_t f3 = f[3U];
586     uint64_t f4 = f[4U];
587     uint64_t l_ = f0 + (uint64_t)0U;
588     uint64_t tmp0 = l_ & (uint64_t)0x7ffffffffffffU;
589     uint64_t c0 = l_ >> (uint32_t)51U;
590     uint64_t l_0 = f1 + c0;
591     uint64_t tmp1 = l_0 & (uint64_t)0x7ffffffffffffU;
592     uint64_t c1 = l_0 >> (uint32_t)51U;
593     uint64_t l_1 = f2 + c1;
594     uint64_t tmp2 = l_1 & (uint64_t)0x7ffffffffffffU;
595     uint64_t c2 = l_1 >> (uint32_t)51U;
596     uint64_t l_2 = f3 + c2;
597     uint64_t tmp3 = l_2 & (uint64_t)0x7ffffffffffffU;
598     uint64_t c3 = l_2 >> (uint32_t)51U;
599     uint64_t l_3 = f4 + c3;
600     uint64_t tmp4 = l_3 & (uint64_t)0x7ffffffffffffU;
601     uint64_t c4 = l_3 >> (uint32_t)51U;
602     uint64_t l_4 = tmp0 + c4 * (uint64_t)19U;
603     uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
604     uint64_t c5 = l_4 >> (uint32_t)51U;
605     uint64_t f01 = tmp0_;
606     uint64_t f11 = tmp1 + c5;
607     uint64_t f21 = tmp2;
608     uint64_t f31 = tmp3;
609     uint64_t f41 = tmp4;
610     uint64_t m0 = FStar_UInt64_gte_mask(f01, (uint64_t)0x7ffffffffffedU);
611     uint64_t m1 = FStar_UInt64_eq_mask(f11, (uint64_t)0x7ffffffffffffU);
612     uint64_t m2 = FStar_UInt64_eq_mask(f21, (uint64_t)0x7ffffffffffffU);
613     uint64_t m3 = FStar_UInt64_eq_mask(f31, (uint64_t)0x7ffffffffffffU);
614     uint64_t m4 = FStar_UInt64_eq_mask(f41, (uint64_t)0x7ffffffffffffU);
615     uint64_t mask = (((m0 & m1) & m2) & m3) & m4;
616     uint64_t f0_ = f01 - (mask & (uint64_t)0x7ffffffffffedU);
617     uint64_t f1_ = f11 - (mask & (uint64_t)0x7ffffffffffffU);
618     uint64_t f2_ = f21 - (mask & (uint64_t)0x7ffffffffffffU);
619     uint64_t f3_ = f31 - (mask & (uint64_t)0x7ffffffffffffU);
620     uint64_t f4_ = f41 - (mask & (uint64_t)0x7ffffffffffffU);
621     uint64_t f02 = f0_;
622     uint64_t f12 = f1_;
623     uint64_t f22 = f2_;
624     uint64_t f32 = f3_;
625     uint64_t f42 = f4_;
626     uint64_t o00 = f02 | f12 << (uint32_t)51U;
627     uint64_t o10 = f12 >> (uint32_t)13U | f22 << (uint32_t)38U;
628     uint64_t o20 = f22 >> (uint32_t)26U | f32 << (uint32_t)25U;
629     uint64_t o30 = f32 >> (uint32_t)39U | f42 << (uint32_t)12U;
630     uint64_t o0 = o00;
631     uint64_t o1 = o10;
632     uint64_t o2 = o20;
633     uint64_t o3 = o30;
634     u64s[0U] = o0;
635     u64s[1U] = o1;
636     u64s[2U] = o2;
637     u64s[3U] = o3;
638 }
639 
640 static inline void
cswap20(uint64_t bit,uint64_t * p1,uint64_t * p2)641 cswap20(uint64_t bit, uint64_t *p1, uint64_t *p2)
642 {
643     uint64_t mask = (uint64_t)0U - bit;
644     for (uint32_t i = (uint32_t)0U; i < (uint32_t)10U; i++) {
645         uint64_t dummy = mask & (p1[i] ^ p2[i]);
646         p1[i] = p1[i] ^ dummy;
647         p2[i] = p2[i] ^ dummy;
648     }
649 }
650 
651 static const uint8_t g25519[32U] = { (uint8_t)9U };
652 
653 static void
point_add_and_double(uint64_t * q,uint64_t * p01_tmp1,FStar_UInt128_uint128 * tmp2)654 point_add_and_double(uint64_t *q, uint64_t *p01_tmp1, FStar_UInt128_uint128 *tmp2)
655 {
656     uint64_t *nq = p01_tmp1;
657     uint64_t *nq_p1 = p01_tmp1 + (uint32_t)10U;
658     uint64_t *tmp1 = p01_tmp1 + (uint32_t)20U;
659     uint64_t *x1 = q;
660     uint64_t *x2 = nq;
661     uint64_t *z2 = nq + (uint32_t)5U;
662     uint64_t *z3 = nq_p1 + (uint32_t)5U;
663     uint64_t *a = tmp1;
664     uint64_t *b = tmp1 + (uint32_t)5U;
665     uint64_t *ab = tmp1;
666     uint64_t *dc = tmp1 + (uint32_t)10U;
667     fadd0(a, x2, z2);
668     fsub0(b, x2, z2);
669     uint64_t *x3 = nq_p1;
670     uint64_t *z31 = nq_p1 + (uint32_t)5U;
671     uint64_t *d0 = dc;
672     uint64_t *c0 = dc + (uint32_t)5U;
673     fadd0(c0, x3, z31);
674     fsub0(d0, x3, z31);
675     fmul20(dc, dc, ab);
676     fadd0(x3, d0, c0);
677     fsub0(z31, d0, c0);
678     uint64_t *a1 = tmp1;
679     uint64_t *b1 = tmp1 + (uint32_t)5U;
680     uint64_t *d = tmp1 + (uint32_t)10U;
681     uint64_t *c = tmp1 + (uint32_t)15U;
682     uint64_t *ab1 = tmp1;
683     uint64_t *dc1 = tmp1 + (uint32_t)10U;
684     fsqr20(dc1, ab1);
685     fsqr20(nq_p1, nq_p1);
686     a1[0U] = c[0U];
687     a1[1U] = c[1U];
688     a1[2U] = c[2U];
689     a1[3U] = c[3U];
690     a1[4U] = c[4U];
691     fsub0(c, d, c);
692     fmul1(b1, c, (uint64_t)121665U);
693     fadd0(b1, b1, d);
694     fmul20(nq, dc1, ab1);
695     fmul0(z3, z3, x1);
696 }
697 
698 static void
point_double(uint64_t * nq,uint64_t * tmp1,FStar_UInt128_uint128 * tmp2)699 point_double(uint64_t *nq, uint64_t *tmp1, FStar_UInt128_uint128 *tmp2)
700 {
701     uint64_t *x2 = nq;
702     uint64_t *z2 = nq + (uint32_t)5U;
703     uint64_t *a = tmp1;
704     uint64_t *b = tmp1 + (uint32_t)5U;
705     uint64_t *d = tmp1 + (uint32_t)10U;
706     uint64_t *c = tmp1 + (uint32_t)15U;
707     uint64_t *ab = tmp1;
708     uint64_t *dc = tmp1 + (uint32_t)10U;
709     fadd0(a, x2, z2);
710     fsub0(b, x2, z2);
711     fsqr20(dc, ab);
712     a[0U] = c[0U];
713     a[1U] = c[1U];
714     a[2U] = c[2U];
715     a[3U] = c[3U];
716     a[4U] = c[4U];
717     fsub0(c, d, c);
718     fmul1(b, c, (uint64_t)121665U);
719     fadd0(b, b, d);
720     fmul20(nq, dc, ab);
721 }
722 
723 static void
montgomery_ladder(uint64_t * out,uint8_t * key,uint64_t * init)724 montgomery_ladder(uint64_t *out, uint8_t *key, uint64_t *init)
725 {
726     FStar_UInt128_uint128 tmp2[10U];
727     for (uint32_t _i = 0U; _i < (uint32_t)10U; ++_i)
728         tmp2[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U);
729     uint64_t p01_tmp1_swap[41U] = { 0U };
730     uint64_t *p0 = p01_tmp1_swap;
731     uint64_t *p01 = p01_tmp1_swap;
732     uint64_t *p03 = p01;
733     uint64_t *p11 = p01 + (uint32_t)10U;
734     memcpy(p11, init, (uint32_t)10U * sizeof(init[0U]));
735     uint64_t *x0 = p03;
736     uint64_t *z0 = p03 + (uint32_t)5U;
737     x0[0U] = (uint64_t)1U;
738     x0[1U] = (uint64_t)0U;
739     x0[2U] = (uint64_t)0U;
740     x0[3U] = (uint64_t)0U;
741     x0[4U] = (uint64_t)0U;
742     z0[0U] = (uint64_t)0U;
743     z0[1U] = (uint64_t)0U;
744     z0[2U] = (uint64_t)0U;
745     z0[3U] = (uint64_t)0U;
746     z0[4U] = (uint64_t)0U;
747     uint64_t *p01_tmp1 = p01_tmp1_swap;
748     uint64_t *p01_tmp11 = p01_tmp1_swap;
749     uint64_t *nq1 = p01_tmp1_swap;
750     uint64_t *nq_p11 = p01_tmp1_swap + (uint32_t)10U;
751     uint64_t *swap = p01_tmp1_swap + (uint32_t)40U;
752     cswap20((uint64_t)1U, nq1, nq_p11);
753     point_add_and_double(init, p01_tmp11, tmp2);
754     swap[0U] = (uint64_t)1U;
755     for (uint32_t i = (uint32_t)0U; i < (uint32_t)251U; i++) {
756         uint64_t *p01_tmp12 = p01_tmp1_swap;
757         uint64_t *swap1 = p01_tmp1_swap + (uint32_t)40U;
758         uint64_t *nq2 = p01_tmp12;
759         uint64_t *nq_p12 = p01_tmp12 + (uint32_t)10U;
760         uint64_t
761             bit =
762                 (uint64_t)(key[((uint32_t)253U - i) / (uint32_t)8U] >> ((uint32_t)253U - i) % (uint32_t)8U & (uint8_t)1U);
763         uint64_t sw = swap1[0U] ^ bit;
764         cswap20(sw, nq2, nq_p12);
765         point_add_and_double(init, p01_tmp12, tmp2);
766         swap1[0U] = bit;
767     }
768     uint64_t sw = swap[0U];
769     cswap20(sw, nq1, nq_p11);
770     uint64_t *nq10 = p01_tmp1;
771     uint64_t *tmp1 = p01_tmp1 + (uint32_t)20U;
772     point_double(nq10, tmp1, tmp2);
773     point_double(nq10, tmp1, tmp2);
774     point_double(nq10, tmp1, tmp2);
775     memcpy(out, p0, (uint32_t)10U * sizeof(p0[0U]));
776 }
777 
778 static void
fsquare_times(uint64_t * o,uint64_t * inp,FStar_UInt128_uint128 * tmp,uint32_t n)779 fsquare_times(uint64_t *o, uint64_t *inp, FStar_UInt128_uint128 *tmp, uint32_t n)
780 {
781     fsqr0(o, inp);
782     for (uint32_t i = (uint32_t)0U; i < n - (uint32_t)1U; i++) {
783         fsqr0(o, o);
784     }
785 }
786 
787 static void
finv(uint64_t * o,uint64_t * i,FStar_UInt128_uint128 * tmp)788 finv(uint64_t *o, uint64_t *i, FStar_UInt128_uint128 *tmp)
789 {
790     uint64_t t1[20U] = { 0U };
791     uint64_t *a = t1;
792     uint64_t *b = t1 + (uint32_t)5U;
793     uint64_t *c = t1 + (uint32_t)10U;
794     uint64_t *t00 = t1 + (uint32_t)15U;
795     FStar_UInt128_uint128 *tmp1 = tmp;
796     fsquare_times(a, i, tmp1, (uint32_t)1U);
797     fsquare_times(t00, a, tmp1, (uint32_t)2U);
798     fmul0(b, t00, i);
799     fmul0(a, b, a);
800     fsquare_times(t00, a, tmp1, (uint32_t)1U);
801     fmul0(b, t00, b);
802     fsquare_times(t00, b, tmp1, (uint32_t)5U);
803     fmul0(b, t00, b);
804     fsquare_times(t00, b, tmp1, (uint32_t)10U);
805     fmul0(c, t00, b);
806     fsquare_times(t00, c, tmp1, (uint32_t)20U);
807     fmul0(t00, t00, c);
808     fsquare_times(t00, t00, tmp1, (uint32_t)10U);
809     fmul0(b, t00, b);
810     fsquare_times(t00, b, tmp1, (uint32_t)50U);
811     fmul0(c, t00, b);
812     fsquare_times(t00, c, tmp1, (uint32_t)100U);
813     fmul0(t00, t00, c);
814     fsquare_times(t00, t00, tmp1, (uint32_t)50U);
815     fmul0(t00, t00, b);
816     fsquare_times(t00, t00, tmp1, (uint32_t)5U);
817     uint64_t *a0 = t1;
818     uint64_t *t0 = t1 + (uint32_t)15U;
819     fmul0(o, t0, a0);
820 }
821 
822 static void
encode_point(uint8_t * o,uint64_t * i)823 encode_point(uint8_t *o, uint64_t *i)
824 {
825     uint64_t *x = i;
826     uint64_t *z = i + (uint32_t)5U;
827     uint64_t tmp[5U] = { 0U };
828     uint64_t u64s[4U] = { 0U };
829     FStar_UInt128_uint128 tmp_w[10U];
830     for (uint32_t _i = 0U; _i < (uint32_t)10U; ++_i)
831         tmp_w[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U);
832     finv(tmp, z, tmp_w);
833     fmul0(tmp, tmp, x);
834     store_felem(u64s, tmp);
835     for (uint32_t i0 = (uint32_t)0U; i0 < (uint32_t)4U; i0++) {
836         store64_le(o + i0 * (uint32_t)8U, u64s[i0]);
837     }
838 }
839 
840 void
Hacl_Curve25519_51_scalarmult(uint8_t * out,uint8_t * priv,uint8_t * pub)841 Hacl_Curve25519_51_scalarmult(uint8_t *out, uint8_t *priv, uint8_t *pub)
842 {
843     uint64_t init[10U] = { 0U };
844     uint64_t tmp[4U] = { 0U };
845     for (uint32_t i = (uint32_t)0U; i < (uint32_t)4U; i++) {
846         uint64_t *os = tmp;
847         uint8_t *bj = pub + i * (uint32_t)8U;
848         uint64_t u = load64_le(bj);
849         uint64_t r = u;
850         uint64_t x = r;
851         os[i] = x;
852     }
853     uint64_t tmp3 = tmp[3U];
854     tmp[3U] = tmp3 & (uint64_t)0x7fffffffffffffffU;
855     uint64_t *x = init;
856     uint64_t *z = init + (uint32_t)5U;
857     z[0U] = (uint64_t)1U;
858     z[1U] = (uint64_t)0U;
859     z[2U] = (uint64_t)0U;
860     z[3U] = (uint64_t)0U;
861     z[4U] = (uint64_t)0U;
862     uint64_t f0l = tmp[0U] & (uint64_t)0x7ffffffffffffU;
863     uint64_t f0h = tmp[0U] >> (uint32_t)51U;
864     uint64_t f1l = (tmp[1U] & (uint64_t)0x3fffffffffU) << (uint32_t)13U;
865     uint64_t f1h = tmp[1U] >> (uint32_t)38U;
866     uint64_t f2l = (tmp[2U] & (uint64_t)0x1ffffffU) << (uint32_t)26U;
867     uint64_t f2h = tmp[2U] >> (uint32_t)25U;
868     uint64_t f3l = (tmp[3U] & (uint64_t)0xfffU) << (uint32_t)39U;
869     uint64_t f3h = tmp[3U] >> (uint32_t)12U;
870     x[0U] = f0l;
871     x[1U] = f0h | f1l;
872     x[2U] = f1h | f2l;
873     x[3U] = f2h | f3l;
874     x[4U] = f3h;
875     montgomery_ladder(init, priv, init);
876     encode_point(out, init);
877 }
878 
879 void
Hacl_Curve25519_51_secret_to_public(uint8_t * pub,uint8_t * priv)880 Hacl_Curve25519_51_secret_to_public(uint8_t *pub, uint8_t *priv)
881 {
882     uint8_t basepoint[32U] = { 0U };
883     for (uint32_t i = (uint32_t)0U; i < (uint32_t)32U; i++) {
884         uint8_t *os = basepoint;
885         uint8_t x = g25519[i];
886         os[i] = x;
887     }
888     Hacl_Curve25519_51_scalarmult(pub, priv, basepoint);
889 }
890 
891 bool
Hacl_Curve25519_51_ecdh(uint8_t * out,uint8_t * priv,uint8_t * pub)892 Hacl_Curve25519_51_ecdh(uint8_t *out, uint8_t *priv, uint8_t *pub)
893 {
894     uint8_t zeros[32U] = { 0U };
895     Hacl_Curve25519_51_scalarmult(out, priv, pub);
896     uint8_t res = (uint8_t)255U;
897     for (uint32_t i = (uint32_t)0U; i < (uint32_t)32U; i++) {
898         uint8_t uu____0 = FStar_UInt8_eq_mask(out[i], zeros[i]);
899         res = uu____0 & res;
900     }
901     uint8_t z = res;
902     bool r = z == (uint8_t)255U;
903     return !r;
904 }
905