1 // SPDX-License-Identifier: GPL-2.0 OR MIT
3  * Copyright (C) 2015-2016 The fiat-crypto Authors.
4  * Copyright (C) 2018-2020 Jason A. Donenfeld <Jason@zx2c4.com>. All Rights Reserved.
6  * This is a machine-generated formally verified implementation of Curve25519
7  * ECDH from: <https://github.com/mit-plv/fiat-crypto>. Though originally
9  * It is optimized for 32-bit machines and machines that cannot work efficiently
10  * with 128-bit integer types.
13 /* fe means field element. Here the field is \Z/(2^255-19). An element t,
14  * entries t[0]...t[9], represents the integer t[0]+2^26 t[1]+2^51 t[2]+2^77
15  * t[3]+2^102 t[4]+...+2^230 t[9].
16  * fe limbs are bounded by 1.125*2^26,1.125*2^25,1.125*2^26,1.125*2^25,etc.
21 /* fe_loose limbs are bounded by 3.375*2^26,3.375*2^25,3.375*2^26,3.375*2^25,etc
28 	/* Ignores top bit of s. */  in fe_frombytes_impl()
37 	h[0] = a0&((1<<26)-1);                    /* 26 used, 32-26 left.   26 */  in fe_frombytes_impl()
38 	h[1] = (a0>>26) | ((a1&((1<<19)-1))<< 6); /* (32-26) + 19 =  6+19 = 25 */  in fe_frombytes_impl()
39 	h[2] = (a1>>19) | ((a2&((1<<13)-1))<<13); /* (32-19) + 13 = 13+13 = 26 */  in fe_frombytes_impl()
40 	h[3] = (a2>>13) | ((a3&((1<< 6)-1))<<19); /* (32-13) +  6 = 19+ 6 = 25 */  in fe_frombytes_impl()
41 	h[4] = (a3>> 6);                          /* (32- 6)              = 26 */  in fe_frombytes_impl()
42 	h[5] = a4&((1<<25)-1);                    /*                        25 */  in fe_frombytes_impl()
43 	h[6] = (a4>>25) | ((a5&((1<<19)-1))<< 7); /* (32-25) + 19 =  7+19 = 26 */  in fe_frombytes_impl()
44 	h[7] = (a5>>19) | ((a6&((1<<12)-1))<<13); /* (32-19) + 12 = 13+12 = 25 */  in fe_frombytes_impl()
45 	h[8] = (a6>>12) | ((a7&((1<< 6)-1))<<20); /* (32-12) +  6 = 20+ 6 = 26 */  in fe_frombytes_impl()
46 	h[9] = (a7>> 6)&((1<<25)-1); /*                                     25 */  in fe_frombytes_impl()
51 	fe_frombytes_impl(h->v, s);  in fe_frombytes()
57 	/* This function extracts 25 bits of result and 1 bit of carry  in addcarryx_u25()
58 	 * (26 total), so a 32-bit intermediate is sufficient.  in addcarryx_u25()
61 	*low = x & ((1 << 25) - 1);  in addcarryx_u25()
68 	/* This function extracts 26 bits of result and 1 bit of carry  in addcarryx_u26()
69 	 * (27 total), so a 32-bit intermediate is sufficient.  in addcarryx_u26()
72 	*low = x & ((1 << 26) - 1);  in addcarryx_u26()
79 	/* This function extracts 25 bits of result and 1 bit of borrow  in subborrow_u25()
80 	 * (26 total), so a 32-bit intermediate is sufficient.  in subborrow_u25()
82 	u32 x = a - b - c;  in subborrow_u25()
83 	*low = x & ((1 << 25) - 1);  in subborrow_u25()
90 	/* This function extracts 26 bits of result and 1 bit of borrow  in subborrow_u26()
91 	 *(27 total), so a 32-bit intermediate is sufficient.  in subborrow_u26()
93 	u32 x = a - b - c;  in subborrow_u26()
94 	*low = x & ((1 << 26) - 1);  in subborrow_u26()
100 	t = -!!t; /* all set if nonzero, 0 if 0 */  in cmovznz32()
113 	{ const u32 x6 = in1[2];  in fe_freeze()
120 	{ u32 x32; u8/*bool*/ x33 = subborrow_u26(x30, x10, 0x3ffffff, &x32);  in fe_freeze()  local
136 	{ u32 x68; u8/*bool*/ x69 = addcarryx_u26(x65, x32, x66, &x68);  in fe_freeze()
149 	out[2] = x60;  in fe_freeze()
163 	fe_freeze(h, f->v);  in fe_tobytes()
166 	s[2] = h[0] >> 16;  in fe_tobytes()
167 	s[3] = (h[0] >> 24) | (h[1] << 2);  in fe_tobytes()
170 	s[6] = (h[1] >> 22) | (h[2] << 3);  in fe_tobytes()
171 	s[7] = h[2] >> 5;  in fe_tobytes()
172 	s[8] = h[2] >> 13;  in fe_tobytes()
173 	s[9] = (h[2] >> 21) | (h[3] << 5);  in fe_tobytes()
177 	s[13] = h[4] >> 2;  in fe_tobytes()
193 	s[29] = h[9] >> 2;  in fe_tobytes()
219 	h->v[0] = 1;  in fe_1()
231 	{ const u32 x9 = in1[2];  in fe_add_impl()
241 	{ const u32 x27 = in2[2];  in fe_add_impl()
246 	out[2] = (x9 + x27);  in fe_add_impl()
262 	fe_add_impl(h->v, f->v, g->v);  in fe_add()
274 	{ const u32 x9 = in1[2];  in fe_sub_impl()
284 	{ const u32 x27 = in2[2];  in fe_sub_impl()
287 	out[0] = ((0x7ffffda + x5) - x23);  in fe_sub_impl()
288 	out[1] = ((0x3fffffe + x7) - x25);  in fe_sub_impl()
289 	out[2] = ((0x7fffffe + x9) - x27);  in fe_sub_impl()
290 	out[3] = ((0x3fffffe + x11) - x29);  in fe_sub_impl()
291 	out[4] = ((0x7fffffe + x13) - x31);  in fe_sub_impl()
292 	out[5] = ((0x3fffffe + x15) - x33);  in fe_sub_impl()
293 	out[6] = ((0x7fffffe + x17) - x35);  in fe_sub_impl()
294 	out[7] = ((0x3fffffe + x19) - x37);  in fe_sub_impl()
295 	out[8] = ((0x7fffffe + x21) - x39);  in fe_sub_impl()
296 	out[9] = ((0x3fffffe + x20) - x38);  in fe_sub_impl()
300 /* h = f - g
305 	fe_sub_impl(h->v, f->v, g->v);  in fe_sub()
317 	{ const u32 x9 = in1[2];  in fe_mul_impl()
327 	{ const u32 x27 = in2[2];  in fe_mul_impl()
413 	out[2] = (x119 + x93);  in fe_mul_impl()
426 	fe_mul_impl(h->v, f->v, g->v);  in fe_mul_ttt()
431 	fe_mul_impl(h->v, f->v, g->v);  in fe_mul_tlt()
437 	fe_mul_impl(h->v, f->v, g->v);  in fe_mul_tll()
449 	{ const u32 x6 = in1[2];  in fe_sqr_impl()
465 	{ u64 x32 = (0x2 * ((((u64)x14 * x16) + ((u64)x12 * x18)) + ((u64)x10 * x17)));  in fe_sqr_impl()  local
486 	{ u64 x53 = (x22 + (x32 << 0x4));  in fe_sqr_impl()
487 	{ u64 x54 = (x53 + (x32 << 0x1));  in fe_sqr_impl()
488 	{ u64 x55 = (x54 + x32);  in fe_sqr_impl()
535 	out[2] = (x98 + x72);  in fe_sqr_impl()
548 	fe_sqr_impl(h->v, f->v);  in fe_sq_tl()
553 	fe_sqr_impl(h->v, f->v);  in fe_sq_tt()
566 	for (i = 1; i < 2; ++i)  in fe_loose_invert()
621 	b = 0 - b;  in fe_cswap()
623 		u32 x = f->v[i] ^ g->v[i];  in fe_cswap()
625 		f->v[i] ^= x;  in fe_cswap()
626 		g->v[i] ^= x;  in fe_cswap()
630 /* NOTE: based on fiat-crypto fe_mul, edited for in2=121666, 0, 0.*/
640 	{ const u32 x9 = in1[2];  in fe_mul_121666_impl()
736 	out[2] = (x119 + x93);  in fe_mul_121666_impl()
749 	fe_mul_121666_impl(h->v, f->v);  in fe_mul121666()
772 	 * Coq that prime-field arithmetic correctly simulates extension-field  in curve25519_generic()
773 	 * arithmetic on prime-field values. The decoding of the byte array  in curve25519_generic()
777 …* <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Spec/M…  in curve25519_generic()
781 …* <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves…  in curve25519_generic()
785 …* <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves…  in curve25519_generic()
786 …* <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves…  in curve25519_generic()
787 	 * preconditions: 0 <= e < 2^255 (not necessarily e < order),  in curve25519_generic()
796 	for (pos = 254; pos >= 0; --pos) {  in curve25519_generic()
801 		 *   pos >= -1; if z2 = 0 then x2 is nonzero; if z3 = 0 then x3  in curve25519_generic()
808 		 *   point (r*P-(r+1)*P)  in curve25519_generic()
817 …* <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves…  in curve25519_generic()
818 …* <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves…  in curve25519_generic()
819 …* x1 != 0 <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/sr…  in curve25519_generic()
820 …* x1  = 0 <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/sr…  in curve25519_generic()
841 	/* here pos=-1, so r=e, so to_xz (e*P) === if swap then (x3, z3)  in curve25519_generic()