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