1 #include <openssl/base.h>
2 #include "../../crypto/internal.h"
3
4 #include <stdbool.h>
5 #include <stdint.h>
6 #include <immintrin.h>
7
8 typedef uint64_t fe4[4];
9 typedef uint8_t fiat_uint1;
10 typedef int8_t fiat_int1;
11
fiat_value_barrier_u64(uint64_t a)12 static __inline__ uint64_t fiat_value_barrier_u64(uint64_t a) {
13 __asm__("" : "+r"(a) : /* no inputs */);
14 return a;
15 }
16
17 __attribute__((target("adx,bmi2")))
fe4_mul(fe4 out,const fe4 x,const fe4 y)18 static inline void fe4_mul(fe4 out, const fe4 x, const fe4 y) { fiat_curve25519_adx_mul(out, x, y); }
19
20 __attribute__((target("adx,bmi2")))
fe4_sq(fe4 out,const fe4 x)21 static inline void fe4_sq(fe4 out, const fe4 x) { fiat_curve25519_adx_square(out, x); }
22
23 /*
24 * The function fiat_mulx_u64 is a multiplication, returning the full double-width result.
25 *
26 * Postconditions:
27 * out1 = (arg1 * arg2) mod 2^64
28 * out2 = ⌊arg1 * arg2 / 2^64⌋
29 *
30 * Input Bounds:
31 * arg1: [0x0 ~> 0xffffffffffffffff]
32 * arg2: [0x0 ~> 0xffffffffffffffff]
33 * Output Bounds:
34 * out1: [0x0 ~> 0xffffffffffffffff]
35 * out2: [0x0 ~> 0xffffffffffffffff]
36 */
37 __attribute__((target("adx,bmi2")))
fiat_mulx_u64(uint64_t * out1,uint64_t * out2,uint64_t arg1,uint64_t arg2)38 static inline void fiat_mulx_u64(uint64_t* out1, uint64_t* out2, uint64_t arg1, uint64_t arg2) {
39 // NOTE: edited after generation
40 #if defined(_M_X64)
41 unsigned long long t;
42 *out1 = _umul128(arg1, arg2, &t);
43 *out2 = t;
44 #elif defined(_M_ARM64)
45 *out1 = arg1 * arg2;
46 *out2 = __umulh(arg1, arg2);
47 #else
48 unsigned __int128 t = (unsigned __int128)arg1 * arg2;
49 *out1 = t;
50 *out2 = (t >> 64);
51 #endif
52 }
53
54 /*
55 * The function fiat_addcarryx_u64 is an addition with carry.
56 *
57 * Postconditions:
58 * out1 = (arg1 + arg2 + arg3) mod 2^64
59 * out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋
60 *
61 * Input Bounds:
62 * arg1: [0x0 ~> 0x1]
63 * arg2: [0x0 ~> 0xffffffffffffffff]
64 * arg3: [0x0 ~> 0xffffffffffffffff]
65 * Output Bounds:
66 * out1: [0x0 ~> 0xffffffffffffffff]
67 * out2: [0x0 ~> 0x1]
68 */
69 __attribute__((target("adx,bmi2")))
fiat_addcarryx_u64(uint64_t * out1,fiat_uint1 * out2,fiat_uint1 arg1,uint64_t arg2,uint64_t arg3)70 static inline void fiat_addcarryx_u64(uint64_t* out1, fiat_uint1* out2, fiat_uint1 arg1, uint64_t arg2, uint64_t arg3) {
71 // NOTE: edited after generation
72 #if defined(__has_builtin)
73 # if __has_builtin(__builtin_ia32_addcarryx_u64)
74 # define addcarry64 __builtin_ia32_addcarryx_u64
75 # endif
76 #endif
77 #if defined(addcarry64)
78 long long unsigned int t;
79 *out2 = addcarry64(arg1, arg2, arg3, &t);
80 *out1 = t;
81 #elif defined(_M_X64)
82 long long unsigned int t;
83 *out2 = _addcarry_u64(arg1, arg2, arg3, out1);
84 *out1 = t;
85 #else
86 arg2 += arg1;
87 arg1 = arg2 < arg1;
88 uint64_t ret = arg2 + arg3;
89 arg1 += ret < arg2;
90 *out1 = ret;
91 *out2 = arg1;
92 #endif
93 #undef addcarry64
94 }
95
96 /*
97 * The function fiat_subborrowx_u64 is a subtraction with borrow.
98 *
99 * Postconditions:
100 * out1 = (-arg1 + arg2 + -arg3) mod 2^64
101 * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋
102 *
103 * Input Bounds:
104 * arg1: [0x0 ~> 0x1]
105 * arg2: [0x0 ~> 0xffffffffffffffff]
106 * arg3: [0x0 ~> 0xffffffffffffffff]
107 * Output Bounds:
108 * out1: [0x0 ~> 0xffffffffffffffff]
109 * out2: [0x0 ~> 0x1]
110 */
111 __attribute__((target("adx,bmi2")))
fiat_subborrowx_u64(uint64_t * out1,fiat_uint1 * out2,fiat_uint1 arg1,uint64_t arg2,uint64_t arg3)112 static inline void fiat_subborrowx_u64(uint64_t* out1, fiat_uint1* out2, fiat_uint1 arg1, uint64_t arg2, uint64_t arg3) {
113 #if defined(__has_builtin)
114 # if __has_builtin(__builtin_ia32_subborrow_u64)
115 # define subborrow64 __builtin_ia32_subborrow_u64
116 # endif
117 #endif
118 #if defined(subborrow64)
119 long long unsigned int t;
120 *out2 = subborrow64(arg1, arg2, arg3, &t);
121 *out1 = t;
122 #elif defined(_M_X64)
123 long long unsigned int t;
124 *out2 = _subborrow_u64(arg1, arg2, arg3, &t); // NOTE: edited after generation
125 *out1 = t;
126 #else
127 *out1 = arg2 - arg3 - arg1;
128 *out2 = (arg2 < arg3) | ((arg2 == arg3) & arg1);
129 #endif
130 #undef subborrow64
131 }
132
133 /*
134 * The function fiat_cmovznz_u64 is a single-word conditional move.
135 *
136 * Postconditions:
137 * out1 = (if arg1 = 0 then arg2 else arg3)
138 *
139 * Input Bounds:
140 * arg1: [0x0 ~> 0x1]
141 * arg2: [0x0 ~> 0xffffffffffffffff]
142 * arg3: [0x0 ~> 0xffffffffffffffff]
143 * Output Bounds:
144 * out1: [0x0 ~> 0xffffffffffffffff]
145 */
146 __attribute__((target("adx,bmi2")))
fiat_cmovznz_u64(uint64_t * out1,fiat_uint1 arg1,uint64_t arg2,uint64_t arg3)147 static inline void fiat_cmovznz_u64(uint64_t* out1, fiat_uint1 arg1, uint64_t arg2, uint64_t arg3) {
148 fiat_uint1 x1;
149 uint64_t x2;
150 uint64_t x3;
151 x1 = (!(!arg1));
152 x2 = ((fiat_int1)(0x0 - x1) & UINT64_C(0xffffffffffffffff));
153 x3 = ((fiat_value_barrier_u64(x2) & arg3) | (fiat_value_barrier_u64((~x2)) & arg2));
154 *out1 = x3;
155 }
156
157 /*
158 * Input Bounds:
159 * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
160 * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
161 * Output Bounds:
162 * out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
163 */
164 __attribute__((target("adx,bmi2")))
fe4_add(uint64_t out1[4],const uint64_t arg1[4],const uint64_t arg2[4])165 static void fe4_add(uint64_t out1[4], const uint64_t arg1[4], const uint64_t arg2[4]) {
166 uint64_t x1;
167 fiat_uint1 x2;
168 uint64_t x3;
169 fiat_uint1 x4;
170 uint64_t x5;
171 fiat_uint1 x6;
172 uint64_t x7;
173 fiat_uint1 x8;
174 uint64_t x9;
175 uint64_t x10;
176 fiat_uint1 x11;
177 uint64_t x12;
178 fiat_uint1 x13;
179 uint64_t x14;
180 fiat_uint1 x15;
181 uint64_t x16;
182 fiat_uint1 x17;
183 uint64_t x18;
184 uint64_t x19;
185 fiat_uint1 x20;
186 fiat_addcarryx_u64(&x1, &x2, 0x0, (arg1[0]), (arg2[0]));
187 fiat_addcarryx_u64(&x3, &x4, x2, (arg1[1]), (arg2[1]));
188 fiat_addcarryx_u64(&x5, &x6, x4, (arg1[2]), (arg2[2]));
189 fiat_addcarryx_u64(&x7, &x8, x6, (arg1[3]), (arg2[3]));
190 fiat_cmovznz_u64(&x9, x8, 0x0, UINT8_C(0x26)); // NOTE: clang 14 for Zen 2 uses sbb, and
191 fiat_addcarryx_u64(&x10, &x11, 0x0, x1, x9);
192 fiat_addcarryx_u64(&x12, &x13, x11, x3, 0x0);
193 fiat_addcarryx_u64(&x14, &x15, x13, x5, 0x0);
194 fiat_addcarryx_u64(&x16, &x17, x15, x7, 0x0);
195 fiat_cmovznz_u64(&x18, x17, 0x0, UINT8_C(0x26)); // NOTE: clang 14 for Zen 2 uses sbb, and
196 fiat_addcarryx_u64(&x19, &x20, 0x0, x10, x18);
197 out1[0] = x19;
198 out1[1] = x12;
199 out1[2] = x14;
200 out1[3] = x16;
201 }
202
203 /*
204 * Input Bounds:
205 * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
206 * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
207 * Output Bounds:
208 * out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
209 */
210 __attribute__((target("adx,bmi2")))
fe4_sub(uint64_t out1[4],const uint64_t arg1[4],const uint64_t arg2[4])211 static void fe4_sub(uint64_t out1[4], const uint64_t arg1[4], const uint64_t arg2[4]) {
212 uint64_t x1;
213 uint64_t x2;
214 fiat_uint1 x3;
215 uint64_t x4;
216 uint64_t x5;
217 fiat_uint1 x6;
218 uint64_t x7;
219 uint64_t x8;
220 fiat_uint1 x9;
221 uint64_t x10;
222 uint64_t x11;
223 fiat_uint1 x12;
224 uint64_t x13;
225 uint64_t x14;
226 fiat_uint1 x15;
227 uint64_t x16;
228 fiat_uint1 x17;
229 uint64_t x18;
230 fiat_uint1 x19;
231 uint64_t x20;
232 fiat_uint1 x21;
233 uint64_t x22;
234 uint64_t x23;
235 fiat_uint1 x24;
236 x1 = (arg2[0]);
237 fiat_subborrowx_u64(&x2, &x3, 0x0, (arg1[0]), x1);
238 x4 = (arg2[1]);
239 fiat_subborrowx_u64(&x5, &x6, x3, (arg1[1]), x4);
240 x7 = (arg2[2]);
241 fiat_subborrowx_u64(&x8, &x9, x6, (arg1[2]), x7);
242 x10 = (arg2[3]);
243 fiat_subborrowx_u64(&x11, &x12, x9, (arg1[3]), x10);
244 fiat_cmovznz_u64(&x13, x12, 0x0, UINT8_C(0x26)); // NOTE: clang 14 for Zen 2 uses sbb, and
245 fiat_subborrowx_u64(&x14, &x15, 0x0, x2, x13);
246 fiat_subborrowx_u64(&x16, &x17, x15, x5, 0x0);
247 fiat_subborrowx_u64(&x18, &x19, x17, x8, 0x0);
248 fiat_subborrowx_u64(&x20, &x21, x19, x11, 0x0);
249 fiat_cmovznz_u64(&x22, x21, 0x0, UINT8_C(0x26)); // NOTE: clang 14 for Zen 2 uses sbb, and
250 fiat_subborrowx_u64(&x23, &x24, 0x0, x14, x22);
251 out1[0] = x23;
252 out1[1] = x16;
253 out1[2] = x18;
254 out1[3] = x20;
255 }
256
257 /*
258 * Input Bounds:
259 * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
260 * arg2: [0x0 ~> 0x3ffffffffffffff] // NOTE: this is not any uint64!
261 * Output Bounds:
262 * out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
263 */
264 __attribute__((target("adx,bmi2")))
fe4_scmul(uint64_t out1[4],const uint64_t arg1[4],uint64_t arg2)265 static void fe4_scmul(uint64_t out1[4], const uint64_t arg1[4], uint64_t arg2) {
266 uint64_t x1;
267 uint64_t x2;
268 uint64_t x3;
269 uint64_t x4;
270 uint64_t x5;
271 fiat_uint1 x6;
272 uint64_t x7;
273 uint64_t x8;
274 uint64_t x9;
275 fiat_uint1 x10;
276 uint64_t x11;
277 uint64_t x12;
278 uint64_t x13;
279 fiat_uint1 x14;
280 uint64_t x15;
281 uint64_t x16;
282 uint64_t x17;
283 fiat_uint1 x18;
284 uint64_t x19;
285 fiat_uint1 x20;
286 uint64_t x21;
287 fiat_uint1 x22;
288 uint64_t x23;
289 fiat_uint1 x24;
290 uint64_t x25;
291 uint64_t x26;
292 fiat_uint1 x27;
293 fiat_mulx_u64(&x1, &x2, (arg1[0]), arg2);
294 fiat_mulx_u64(&x3, &x4, (arg1[1]), arg2);
295 fiat_addcarryx_u64(&x5, &x6, 0x0, x2, x3);
296 fiat_mulx_u64(&x7, &x8, (arg1[2]), arg2);
297 fiat_addcarryx_u64(&x9, &x10, x6, x4, x7);
298 fiat_mulx_u64(&x11, &x12, (arg1[3]), arg2);
299 fiat_addcarryx_u64(&x13, &x14, x10, x8, x11);
300 fiat_mulx_u64(&x15, &x16, (x12 + (uint64_t)x14), UINT8_C(0x26));
301 fiat_addcarryx_u64(&x17, &x18, 0x0, x1, x15);
302 fiat_addcarryx_u64(&x19, &x20, x18, x5, 0x0);
303 fiat_addcarryx_u64(&x21, &x22, x20, x9, 0x0);
304 fiat_addcarryx_u64(&x23, &x24, x22, x13, 0x0);
305 fiat_cmovznz_u64(&x25, x24, 0x0, UINT8_C(0x26)); // NOTE: clang 14 for Zen 2 uses sbb, and
306 fiat_addcarryx_u64(&x26, &x27, 0x0, x17, x25);
307 out1[0] = x26;
308 out1[1] = x19;
309 out1[2] = x21;
310 out1[3] = x23;
311 }
312
313 /*
314 * Input Bounds:
315 * arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
316 * Output Bounds:
317 * out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
318 */
319 __attribute__((target("adx,bmi2")))
fe4_canon(uint64_t out1[4],const uint64_t arg1[4])320 static void fe4_canon(uint64_t out1[4], const uint64_t arg1[4]) {
321 uint64_t x1;
322 fiat_uint1 x2;
323 uint64_t x3;
324 fiat_uint1 x4;
325 uint64_t x5;
326 fiat_uint1 x6;
327 uint64_t x7;
328 fiat_uint1 x8;
329 uint64_t x9;
330 uint64_t x10;
331 uint64_t x11;
332 uint64_t x12;
333 uint64_t x13;
334 fiat_uint1 x14;
335 uint64_t x15;
336 fiat_uint1 x16;
337 uint64_t x17;
338 fiat_uint1 x18;
339 uint64_t x19;
340 fiat_uint1 x20;
341 uint64_t x21;
342 uint64_t x22;
343 uint64_t x23;
344 uint64_t x24;
345 fiat_subborrowx_u64(&x1, &x2, 0x0, (arg1[0]), UINT64_C(0xffffffffffffffed));
346 fiat_subborrowx_u64(&x3, &x4, x2, (arg1[1]), UINT64_C(0xffffffffffffffff));
347 fiat_subborrowx_u64(&x5, &x6, x4, (arg1[2]), UINT64_C(0xffffffffffffffff));
348 fiat_subborrowx_u64(&x7, &x8, x6, (arg1[3]), UINT64_C(0x7fffffffffffffff));
349 fiat_cmovznz_u64(&x9, x8, x1, (arg1[0]));
350 fiat_cmovznz_u64(&x10, x8, x3, (arg1[1]));
351 fiat_cmovznz_u64(&x11, x8, x5, (arg1[2]));
352 fiat_cmovznz_u64(&x12, x8, x7, (arg1[3]));
353 fiat_subborrowx_u64(&x13, &x14, 0x0, x9, UINT64_C(0xffffffffffffffed));
354 fiat_subborrowx_u64(&x15, &x16, x14, x10, UINT64_C(0xffffffffffffffff));
355 fiat_subborrowx_u64(&x17, &x18, x16, x11, UINT64_C(0xffffffffffffffff));
356 fiat_subborrowx_u64(&x19, &x20, x18, x12, UINT64_C(0x7fffffffffffffff));
357 fiat_cmovznz_u64(&x21, x20, x13, x9);
358 fiat_cmovznz_u64(&x22, x20, x15, x10);
359 fiat_cmovznz_u64(&x23, x20, x17, x11);
360 fiat_cmovznz_u64(&x24, x20, x19, x12);
361 out1[0] = x21;
362 out1[1] = x22;
363 out1[2] = x23;
364 out1[3] = x24;
365 }
366
367 /*
368 * Input Bounds:
369 * arg1: [0x0 ~> 0x1]
370 * arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
371 * arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
372 * Output Bounds:
373 * out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
374 * out2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
375 */
376 __attribute__((target("adx,bmi2")))
fe4_cswap(uint64_t out1[4],uint64_t out2[4],fiat_uint1 arg1,const uint64_t arg2[4],const uint64_t arg3[4])377 static void fe4_cswap(uint64_t out1[4], uint64_t out2[4], fiat_uint1 arg1, const uint64_t arg2[4], const uint64_t arg3[4]) {
378 uint64_t x1;
379 uint64_t x2;
380 uint64_t x3;
381 uint64_t x4;
382 uint64_t x5;
383 uint64_t x6;
384 uint64_t x7;
385 uint64_t x8;
386 // NOTE: clang 14 for Zen 2 uses YMM registers
387 fiat_cmovznz_u64(&x1, arg1, (arg2[0]), (arg3[0]));
388 fiat_cmovznz_u64(&x2, arg1, (arg2[1]), (arg3[1]));
389 fiat_cmovznz_u64(&x3, arg1, (arg2[2]), (arg3[2]));
390 fiat_cmovznz_u64(&x4, arg1, (arg2[3]), (arg3[3]));
391 fiat_cmovznz_u64(&x5, arg1, (arg3[0]), (arg2[0]));
392 fiat_cmovznz_u64(&x6, arg1, (arg3[1]), (arg2[1]));
393 fiat_cmovznz_u64(&x7, arg1, (arg3[2]), (arg2[2]));
394 fiat_cmovznz_u64(&x8, arg1, (arg3[3]), (arg2[3]));
395 out1[0] = x1;
396 out1[1] = x2;
397 out1[2] = x3;
398 out1[3] = x4;
399 out2[0] = x5;
400 out2[1] = x6;
401 out2[2] = x7;
402 out2[3] = x8;
403 }
404
405 // The following functions are adaped from crypto/curve25519/curve25519.c
406 // It would be desirable to share the code, but with the current field
407 // implementations both 4-limb and 5-limb versions of the curve-level code need
408 // to be included in builds targetting an unknown variant of x86_64.
409
410 __attribute__((target("adx,bmi2")))
fe4_invert(fe4 out,const fe4 z)411 static void fe4_invert(fe4 out, const fe4 z) {
412 fe4 t0;
413 fe4 t1;
414 fe4 t2;
415 fe4 t3;
416 int i;
417
418 fe4_sq(t0, z);
419 fe4_sq(t1, t0);
420 for (i = 1; i < 2; ++i) {
421 fe4_sq(t1, t1);
422 }
423 fe4_mul(t1, z, t1);
424 fe4_mul(t0, t0, t1);
425 fe4_sq(t2, t0);
426 fe4_mul(t1, t1, t2);
427 fe4_sq(t2, t1);
428 for (i = 1; i < 5; ++i) {
429 fe4_sq(t2, t2);
430 }
431 fe4_mul(t1, t2, t1);
432 fe4_sq(t2, t1);
433 for (i = 1; i < 10; ++i) {
434 fe4_sq(t2, t2);
435 }
436 fe4_mul(t2, t2, t1);
437 fe4_sq(t3, t2);
438 for (i = 1; i < 20; ++i) {
439 fe4_sq(t3, t3);
440 }
441 fe4_mul(t2, t3, t2);
442 fe4_sq(t2, t2);
443 for (i = 1; i < 10; ++i) {
444 fe4_sq(t2, t2);
445 }
446 fe4_mul(t1, t2, t1);
447 fe4_sq(t2, t1);
448 for (i = 1; i < 50; ++i) {
449 fe4_sq(t2, t2);
450 }
451 fe4_mul(t2, t2, t1);
452 fe4_sq(t3, t2);
453 for (i = 1; i < 100; ++i) {
454 fe4_sq(t3, t3);
455 }
456 fe4_mul(t2, t3, t2);
457 fe4_sq(t2, t2);
458 for (i = 1; i < 50; ++i) {
459 fe4_sq(t2, t2);
460 }
461 fe4_mul(t1, t2, t1);
462 fe4_sq(t1, t1);
463 for (i = 1; i < 5; ++i) {
464 fe4_sq(t1, t1);
465 }
466 fe4_mul(out, t1, t0);
467 }
468
469 __attribute__((target("adx,bmi2")))
x25519_scalar_mult_adx(uint8_t out[32],const uint8_t scalar[32],const uint8_t point[32])470 void x25519_scalar_mult_adx(uint8_t out[32], const uint8_t scalar[32],
471 const uint8_t point[32]) {
472 uint8_t e[32];
473 OPENSSL_memcpy(e, scalar, 32);
474 e[0] &= 248;
475 e[31] &= 127;
476 e[31] |= 64;
477
478 // The following implementation was transcribed to Coq and proven to
479 // correspond to unary scalar multiplication in affine coordinates given that
480 // x1 != 0 is the x coordinate of some point on the curve. It was also checked
481 // in Coq that doing a ladderstep with x1 = x3 = 0 gives z2' = z3' = 0, and z2
482 // = z3 = 0 gives z2' = z3' = 0. The statement was quantified over the
483 // underlying field, so it applies to Curve25519 itself and the quadratic
484 // twist of Curve25519. It was not proven in Coq that prime-field arithmetic
485 // correctly simulates extension-field arithmetic on prime-field values.
486 // The decoding of the byte array representation of e was not considered.
487 // Specification of Montgomery curves in affine coordinates:
488 // <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Spec/MontgomeryCurve.v#L27>
489 // Proof that these form a group that is isomorphic to a Weierstrass curve:
490 // <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves/Montgomery/AffineProofs.v#L35>
491 // Coq transcription and correctness proof of the loop (where scalarbits=255):
492 // <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves/Montgomery/XZ.v#L118>
493 // <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves/Montgomery/XZProofs.v#L278>
494 // preconditions: 0 <= e < 2^255 (not necessarily e < order), fe_invert(0) = 0
495 fe4 x1, x2 = {1}, z2 = {0}, x3, z3 = {1}, tmp0, tmp1;
496 OPENSSL_memcpy(x1, point, sizeof(fe4));
497 x1[3] &= (uint64_t)(-1)>>1;
498 OPENSSL_memcpy(x3, x1, sizeof(fe4));
499
500 unsigned swap = 0;
501 int pos;
502 for (pos = 254; pos >= 0; --pos) {
503 // loop invariant as of right before the test, for the case where x1 != 0:
504 // pos >= -1; if z2 = 0 then x2 is nonzero; if z3 = 0 then x3 is nonzero
505 // let r := e >> (pos+1) in the following equalities of projective points:
506 // to_xz (r*P) === if swap then (x3, z3) else (x2, z2)
507 // to_xz ((r+1)*P) === if swap then (x2, z2) else (x3, z3)
508 // x1 is the nonzero x coordinate of the nonzero point (r*P-(r+1)*P)
509 unsigned b = 1 & (e[pos / 8] >> (pos & 7));
510 swap ^= b;
511 fe4_cswap(x2, x3, swap, x2, x3);
512 fe4_cswap(z2, z3, swap, z2, z3);
513 swap = b;
514 // Coq transcription of ladderstep formula (called from transcribed loop):
515 // <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves/Montgomery/XZ.v#L89>
516 // <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves/Montgomery/XZProofs.v#L131>
517 // x1 != 0 <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves/Montgomery/XZProofs.v#L217>
518 // x1 = 0 <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves/Montgomery/XZProofs.v#L147>
519 fe4_sub(tmp0, x3, z3);
520 fe4_sub(tmp1, x2, z2);
521 fe4_add(x2, x2, z2);
522 fe4_add(z2, x3, z3);
523 fe4_mul(z3, tmp0, x2);
524 fe4_mul(z2, z2, tmp1);
525 fe4_sq(tmp0, tmp1);
526 fe4_sq(tmp1, x2);
527 fe4_add(x3, z3, z2);
528 fe4_sub(z2, z3, z2);
529 fe4_mul(x2, tmp1, tmp0);
530 fe4_sub(tmp1, tmp1, tmp0);
531 fe4_sq(z2, z2);
532 fe4_scmul(z3, tmp1, 121666);
533 fe4_sq(x3, x3);
534 fe4_add(tmp0, tmp0, z3);
535 fe4_mul(z3, x1, z2);
536 fe4_mul(z2, tmp1, tmp0);
537 }
538 // here pos=-1, so r=e, so to_xz (e*P) === if swap then (x3, z3) else (x2, z2)
539 fe4_cswap(x2, x3, swap, x2, x3);
540 fe4_cswap(z2, z3, swap, z2, z3);
541
542 fe4_invert(z2, z2);
543 fe4_mul(x2, x2, z2);
544 fe4_canon(x2, x2);
545 OPENSSL_memcpy(out, x2, sizeof(fe4));
546 }
547
548 typedef struct {
549 fe4 X;
550 fe4 Y;
551 fe4 Z;
552 fe4 T;
553 } ge_p3_4;
554
555 typedef struct {
556 fe4 yplusx;
557 fe4 yminusx;
558 fe4 xy2d;
559 } ge_precomp_4;
560
561 __attribute__((target("adx,bmi2")))
inline_x25519_ge_dbl_4(ge_p3_4 * r,const ge_p3_4 * p,bool skip_t)562 static void inline_x25519_ge_dbl_4(ge_p3_4 *r, const ge_p3_4 *p, bool skip_t) {
563 // Transcribed from a Coq function proven against affine coordinates.
564 // https://github.com/mit-plv/fiat-crypto/blob/9943ba9e7d8f3e1c0054b2c94a5edca46ea73ef8/src/Curves/Edwards/XYZT/Basic.v#L136-L165
565 fe4 trX, trZ, trT, t0, cX, cY, cZ, cT;
566 fe4_sq(trX, p->X);
567 fe4_sq(trZ, p->Y);
568 fe4_sq(trT, p->Z);
569 fe4_add(trT, trT, trT);
570 fe4_add(cY, p->X, p->Y);
571 fe4_sq(t0, cY);
572 fe4_add(cY, trZ, trX);
573 fe4_sub(cZ, trZ, trX);
574 fe4_sub(cX, t0, cY);
575 fe4_sub(cT, trT, cZ);
576 fe4_mul(r->X, cX, cT);
577 fe4_mul(r->Y, cY, cZ);
578 fe4_mul(r->Z, cZ, cT);
579 if (!skip_t) {
580 fe4_mul(r->T, cX, cY);
581 }
582 }
583
584 __attribute__((target("adx,bmi2")))
585 __attribute__((always_inline)) // 4% speedup with clang14 and zen2
586 static inline void
ge_p3_add_p3_precomp_4(ge_p3_4 * r,const ge_p3_4 * p,const ge_precomp_4 * q)587 ge_p3_add_p3_precomp_4(ge_p3_4 *r, const ge_p3_4 *p, const ge_precomp_4 *q) {
588 fe4 A, B, C, YplusX, YminusX, D, X3, Y3, Z3, T3;
589 // Transcribed from a Coq function proven against affine coordinates.
590 // https://github.com/mit-plv/fiat-crypto/blob/a36568d1d73aff5d7accc79fd28be672882f9c17/src/Curves/Edwards/XYZT/Precomputed.v#L38-L56
591 fe4_add(YplusX, p->Y, p->X);
592 fe4_sub(YminusX, p->Y, p->X);
593 fe4_mul(A, YplusX, q->yplusx);
594 fe4_mul(B, YminusX, q->yminusx);
595 fe4_mul(C, q->xy2d, p->T);
596 fe4_add(D, p->Z, p->Z);
597 fe4_sub(X3, A, B);
598 fe4_add(Y3, A, B);
599 fe4_add(Z3, D, C);
600 fe4_sub(T3, D, C);
601 fe4_mul(r->X, X3, T3);
602 fe4_mul(r->Y, Y3, Z3);
603 fe4_mul(r->Z, Z3, T3);
604 fe4_mul(r->T, X3, Y3);
605 }
606
607 __attribute__((always_inline)) // 25% speedup with clang14 and zen2
table_select_4(ge_precomp_4 * t,const int pos,const signed char b)608 static inline void table_select_4(ge_precomp_4 *t, const int pos,
609 const signed char b) {
610 uint8_t bnegative = constant_time_msb_w(b);
611 uint8_t babs = b - ((bnegative & b) << 1);
612
613 uint8_t t_bytes[3][32] = {
614 {constant_time_is_zero_w(b) & 1}, {constant_time_is_zero_w(b) & 1}, {0}};
615 #if defined(__clang__)
616 __asm__("" : "+m" (t_bytes) : /*no inputs*/);
617 #endif
618 static_assert(sizeof(t_bytes) == sizeof(k25519Precomp[pos][0]), "");
619 for (int i = 0; i < 8; i++) {
620 constant_time_conditional_memxor(t_bytes, k25519Precomp[pos][i],
621 sizeof(t_bytes),
622 constant_time_eq_w(babs, 1 + i));
623 }
624
625 static_assert(sizeof(t_bytes) == sizeof(ge_precomp_4), "");
626
627 // fe4 uses saturated 64-bit limbs, so converting from bytes is just a copy.
628 OPENSSL_memcpy(t, t_bytes, sizeof(ge_precomp_4));
629
630 fe4 xy2d_neg = {0};
631 fe4_sub(xy2d_neg, xy2d_neg, t->xy2d);
632 constant_time_conditional_memcpy(t->yplusx, t_bytes[1], sizeof(fe4),
633 bnegative);
634 constant_time_conditional_memcpy(t->yminusx, t_bytes[0], sizeof(fe4),
635 bnegative);
636 constant_time_conditional_memcpy(t->xy2d, xy2d_neg, sizeof(fe4), bnegative);
637 }
638
639 // h = a * B
640 // where a = a[0]+256*a[1]+...+256^31 a[31]
641 // B is the Ed25519 base point (x,4/5) with x positive.
642 //
643 // Preconditions:
644 // a[31] <= 127
645 __attribute__((target("adx,bmi2")))
x25519_ge_scalarmult_base_adx(uint8_t h[4][32],const uint8_t a[32])646 void x25519_ge_scalarmult_base_adx(uint8_t h[4][32], const uint8_t a[32]) {
647 signed char e[64];
648 signed char carry;
649
650 for (unsigned i = 0; i < 32; ++i) {
651 e[2 * i + 0] = (a[i] >> 0) & 15;
652 e[2 * i + 1] = (a[i] >> 4) & 15;
653 }
654 // each e[i] is between 0 and 15
655 // e[63] is between 0 and 7
656
657 carry = 0;
658 for (unsigned i = 0; i < 63; ++i) {
659 e[i] += carry;
660 carry = e[i] + 8;
661 carry >>= 4;
662 e[i] -= carry << 4;
663 }
664 e[63] += carry;
665 // each e[i] is between -8 and 8
666
667 ge_p3_4 r = {{0}, {1}, {1}, {0}};
668 for (unsigned i = 1; i < 64; i += 2) {
669 ge_precomp_4 t;
670 table_select_4(&t, i / 2, e[i]);
671 ge_p3_add_p3_precomp_4(&r, &r, &t);
672 }
673
674 inline_x25519_ge_dbl_4(&r, &r, /*skip_t=*/true);
675 inline_x25519_ge_dbl_4(&r, &r, /*skip_t=*/true);
676 inline_x25519_ge_dbl_4(&r, &r, /*skip_t=*/true);
677 inline_x25519_ge_dbl_4(&r, &r, /*skip_t=*/false);
678
679 for (unsigned i = 0; i < 64; i += 2) {
680 ge_precomp_4 t;
681 table_select_4(&t, i / 2, e[i]);
682 ge_p3_add_p3_precomp_4(&r, &r, &t);
683 }
684
685 // fe4 uses saturated 64-bit limbs, so converting to bytes is just a copy.
686 // Satisfy stated precondition of fiat_25519_from_bytes; tests pass either way
687 fe4_canon(r.X, r.X);
688 fe4_canon(r.Y, r.Y);
689 fe4_canon(r.Z, r.Z);
690 fe4_canon(r.T, r.T);
691 static_assert(sizeof(ge_p3_4) == sizeof(uint8_t[4][32]), "");
692 OPENSSL_memcpy(h, &r, sizeof(ge_p3_4));
693 }
694