Lines Matching +full:in2 +full:-
1 // SPDX-License-Identifier: GPL-2.0 OR MIT
3 * Copyright (C) 2015-2016 The fiat-crypto Authors.
4 * Copyright (C) 2018-2019 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.
17 /* fe means field element. Here the field is \Z/(2^255-19). An element t,
41 h[0] = a0&((1<<26)-1); /* 26 used, 32-26 left. 26 */ in fe_frombytes_impl()
42 h[1] = (a0>>26) | ((a1&((1<<19)-1))<< 6); /* (32-26) + 19 = 6+19 = 25 */ in fe_frombytes_impl()
43 h[2] = (a1>>19) | ((a2&((1<<13)-1))<<13); /* (32-19) + 13 = 13+13 = 26 */ in fe_frombytes_impl()
44 h[3] = (a2>>13) | ((a3&((1<< 6)-1))<<19); /* (32-13) + 6 = 19+ 6 = 25 */ in fe_frombytes_impl()
45 h[4] = (a3>> 6); /* (32- 6) = 26 */ in fe_frombytes_impl()
46 h[5] = a4&((1<<25)-1); /* 25 */ in fe_frombytes_impl()
47 h[6] = (a4>>25) | ((a5&((1<<19)-1))<< 7); /* (32-25) + 19 = 7+19 = 26 */ in fe_frombytes_impl()
48 h[7] = (a5>>19) | ((a6&((1<<12)-1))<<13); /* (32-19) + 12 = 13+12 = 25 */ in fe_frombytes_impl()
49 h[8] = (a6>>12) | ((a7&((1<< 6)-1))<<20); /* (32-12) + 6 = 20+ 6 = 26 */ in fe_frombytes_impl()
50 h[9] = (a7>> 6)&((1<<25)-1); /* 25 */ in fe_frombytes_impl()
55 fe_frombytes_impl(h->v, s); in fe_frombytes()
62 * (26 total), so a 32-bit intermediate is sufficient. in addcarryx_u25()
65 *low = x & ((1 << 25) - 1); in addcarryx_u25()
73 * (27 total), so a 32-bit intermediate is sufficient. in addcarryx_u26()
76 *low = x & ((1 << 26) - 1); in addcarryx_u26()
84 * (26 total), so a 32-bit intermediate is sufficient. in subborrow_u25()
86 u32 x = a - b - c; in subborrow_u25()
87 *low = x & ((1 << 25) - 1); in subborrow_u25()
95 *(27 total), so a 32-bit intermediate is sufficient. in subborrow_u26()
97 u32 x = a - b - c; in subborrow_u26()
98 *low = x & ((1 << 26) - 1); in subborrow_u26()
104 t = -!!t; /* all set if nonzero, 0 if 0 */ in cmovznz32()
167 fe_freeze(h, f->v); in fe_tobytes()
223 h->v[0] = 1; in fe_1()
226 static noinline void fe_add_impl(u32 out[10], const u32 in1[10], const u32 in2[10]) in fe_add_impl()
238 { const u32 x38 = in2[9]; in fe_add_impl()
239 { const u32 x39 = in2[8]; in fe_add_impl()
240 { const u32 x37 = in2[7]; in fe_add_impl()
241 { const u32 x35 = in2[6]; in fe_add_impl()
242 { const u32 x33 = in2[5]; in fe_add_impl()
243 { const u32 x31 = in2[4]; in fe_add_impl()
244 { const u32 x29 = in2[3]; in fe_add_impl()
245 { const u32 x27 = in2[2]; in fe_add_impl()
246 { const u32 x25 = in2[1]; in fe_add_impl()
247 { const u32 x23 = in2[0]; in fe_add_impl()
266 fe_add_impl(h->v, f->v, g->v); in fe_add()
269 static noinline void fe_sub_impl(u32 out[10], const u32 in1[10], const u32 in2[10]) in fe_sub_impl()
281 { const u32 x38 = in2[9]; in fe_sub_impl()
282 { const u32 x39 = in2[8]; in fe_sub_impl()
283 { const u32 x37 = in2[7]; in fe_sub_impl()
284 { const u32 x35 = in2[6]; in fe_sub_impl()
285 { const u32 x33 = in2[5]; in fe_sub_impl()
286 { const u32 x31 = in2[4]; in fe_sub_impl()
287 { const u32 x29 = in2[3]; in fe_sub_impl()
288 { const u32 x27 = in2[2]; in fe_sub_impl()
289 { const u32 x25 = in2[1]; in fe_sub_impl()
290 { const u32 x23 = in2[0]; in fe_sub_impl()
291 out[0] = ((0x7ffffda + x5) - x23); in fe_sub_impl()
292 out[1] = ((0x3fffffe + x7) - x25); in fe_sub_impl()
293 out[2] = ((0x7fffffe + x9) - x27); in fe_sub_impl()
294 out[3] = ((0x3fffffe + x11) - x29); in fe_sub_impl()
295 out[4] = ((0x7fffffe + x13) - x31); in fe_sub_impl()
296 out[5] = ((0x3fffffe + x15) - x33); in fe_sub_impl()
297 out[6] = ((0x7fffffe + x17) - x35); in fe_sub_impl()
298 out[7] = ((0x3fffffe + x19) - x37); in fe_sub_impl()
299 out[8] = ((0x7fffffe + x21) - x39); in fe_sub_impl()
300 out[9] = ((0x3fffffe + x20) - x38); in fe_sub_impl()
304 /* h = f - g
309 fe_sub_impl(h->v, f->v, g->v); in fe_sub()
312 static noinline void fe_mul_impl(u32 out[10], const u32 in1[10], const u32 in2[10]) in fe_mul_impl()
324 { const u32 x38 = in2[9]; in fe_mul_impl()
325 { const u32 x39 = in2[8]; in fe_mul_impl()
326 { const u32 x37 = in2[7]; in fe_mul_impl()
327 { const u32 x35 = in2[6]; in fe_mul_impl()
328 { const u32 x33 = in2[5]; in fe_mul_impl()
329 { const u32 x31 = in2[4]; in fe_mul_impl()
330 { const u32 x29 = in2[3]; in fe_mul_impl()
331 { const u32 x27 = in2[2]; in fe_mul_impl()
332 { const u32 x25 = in2[1]; in fe_mul_impl()
333 { const u32 x23 = in2[0]; in fe_mul_impl()
430 fe_mul_impl(h->v, f->v, g->v); in fe_mul_ttt()
435 fe_mul_impl(h->v, f->v, g->v); in fe_mul_tlt()
441 fe_mul_impl(h->v, f->v, g->v); in fe_mul_tll()
552 fe_sqr_impl(h->v, f->v); in fe_sq_tl()
557 fe_sqr_impl(h->v, f->v); in fe_sq_tt()
625 b = 0 - b; in fe_cswap()
627 u32 x = f->v[i] ^ g->v[i]; in fe_cswap()
629 f->v[i] ^= x; in fe_cswap()
630 g->v[i] ^= x; in fe_cswap()
634 /* NOTE: based on fiat-crypto fe_mul, edited for in2=121666, 0, 0.*/
753 fe_mul_121666_impl(h->v, f->v); in fe_mul121666()
776 * Coq that prime-field arithmetic correctly simulates extension-field in curve25519_generic()
777 * arithmetic on prime-field values. The decoding of the byte array in curve25519_generic()
781 …* <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Spec/M… in curve25519_generic()
785 …* <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves… in curve25519_generic()
789 …* <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves… in curve25519_generic()
790 …* <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves… in curve25519_generic()
800 for (pos = 254; pos >= 0; --pos) { in curve25519_generic()
805 * pos >= -1; if z2 = 0 then x2 is nonzero; if z3 = 0 then x3 in curve25519_generic()
812 * point (r*P-(r+1)*P) in curve25519_generic()
821 …* <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves… in curve25519_generic()
822 …* <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves… in curve25519_generic()
823 …* x1 != 0 <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/sr… in curve25519_generic()
824 …* x1 = 0 <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/sr… in curve25519_generic()
845 /* here pos=-1, so r=e, so to_xz (e*P) === if swap then (x3, z3) in curve25519_generic()