Lines Matching +full:1 +full:x64 +full:- +full:bit
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
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()
62 return (x >> 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()
73 return (x >> 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()
114 { const u32 x4 = in1[1]; in fe_freeze()
134 { u32 x64; u8/*bool*/ x65 = addcarryx_u25(x61, x29, x62, &x64); in fe_freeze() local
148 out[1] = x56; in fe_freeze()
150 out[3] = x64; in fe_freeze()
163 fe_freeze(h, f->v); in fe_tobytes()
165 s[1] = h[0] >> 8; in fe_tobytes()
167 s[3] = (h[0] >> 24) | (h[1] << 2); in fe_tobytes()
168 s[4] = h[1] >> 6; in fe_tobytes()
169 s[5] = h[1] >> 14; in fe_tobytes()
170 s[6] = (h[1] >> 22) | (h[2] << 3); in fe_tobytes()
183 s[19] = (h[5] >> 24) | (h[6] << 1); in fe_tobytes()
215 /* h = 1 */
219 h->v[0] = 1; in fe_1()
232 { const u32 x7 = in1[1]; in fe_add_impl()
242 { const u32 x25 = in2[1]; in fe_add_impl()
245 out[1] = (x7 + x25); in fe_add_impl()
262 fe_add_impl(h->v, f->v, g->v); in fe_add()
275 { const u32 x7 = in1[1]; in fe_sub_impl()
285 { const u32 x25 = in2[1]; 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()
318 { const u32 x7 = in1[1]; in fe_mul_impl()
328 { const u32 x25 = in2[1]; in fe_mul_impl()
354 { u64 x64 = (x63 + x57); in fe_mul_impl() local
396 { u64 x106 = (x104 + x64); in fe_mul_impl()
412 out[1] = x120; 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()
450 { const u32 x4 = in1[1]; in fe_sqr_impl()
497 { u64 x64 = (x63 + x29); in fe_sqr_impl() local
498 { u64 x65 = (x64 >> 0x1a); in fe_sqr_impl()
499 { u32 x66 = ((u32)x64 & 0x3ffffff); in fe_sqr_impl()
534 out[1] = x99; 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()
573 for (i = 1; i < 5; ++i) in fe_loose_invert()
577 for (i = 1; i < 10; ++i) in fe_loose_invert()
581 for (i = 1; i < 20; ++i) in fe_loose_invert()
585 for (i = 1; i < 10; ++i) in fe_loose_invert()
589 for (i = 1; i < 50; ++i) in fe_loose_invert()
593 for (i = 1; i < 100; ++i) in fe_loose_invert()
597 for (i = 1; i < 50; ++i) in fe_loose_invert()
601 for (i = 1; i < 5; ++i) in fe_loose_invert()
613 /* Replace (f,g) with (g,f) if b == 1;
616 * Preconditions: b in {0,1}
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.*/
641 { const u32 x7 = in1[1]; in fe_mul_121666_impl()
677 { u64 x64 = (x63 + x57); in fe_mul_121666_impl() local
719 { u64 x106 = (x104 + x64); in fe_mul_121666_impl()
735 out[1] = x120; 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()
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()
803 * let r := e >> (pos+1) in the following equalities of in curve25519_generic()
806 * to_xz ((r+1)*P) === if swap then (x2, z2) else (x3, z3) in curve25519_generic()
808 * point (r*P-(r+1)*P) in curve25519_generic()
810 unsigned b = 1 & (e[pos / 8] >> (pos & 7)); 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()