aboutsummaryrefslogtreecommitdiffstats
path: root/curve25519-fiat64.c
diff options
context:
space:
mode:
Diffstat (limited to 'curve25519-fiat64.c')
-rw-r--r--curve25519-fiat64.c577
1 files changed, 0 insertions, 577 deletions
diff --git a/curve25519-fiat64.c b/curve25519-fiat64.c
deleted file mode 100644
index ed8119f..0000000
--- a/curve25519-fiat64.c
+++ /dev/null
@@ -1,577 +0,0 @@
-/* SPDX-License-Identifier: GPL-2.0
- *
- * Copyright (C) 2015-2016 The fiat-crypto Authors.
- * Copyright (C) 2018 Jason A. Donenfeld <Jason@zx2c4.com>. All Rights Reserved.
- *
- * This is a machine-generated formally verified implementation of curve25519 DH from:
- * https://github.com/mit-plv/fiat-crypto
- */
-
-#include <linux/kernel.h>
-#include <linux/string.h>
-
-typedef __uint128_t u128;
-
-enum { CURVE25519_POINT_SIZE = 32 };
-
-static __always_inline void normalize_secret(u8 secret[CURVE25519_POINT_SIZE])
-{
- secret[0] &= 248;
- secret[31] &= 127;
- secret[31] |= 64;
-}
-
-/* fe means field element. Here the field is \Z/(2^255-19). An element t,
- * entries t[0]...t[4], represents the integer t[0]+2^51 t[1]+2^102 t[2]+2^153
- * t[3]+2^204 t[4].
- * fe limbs are bounded by 1.125*2^51.
- * Multiplication and carrying produce fe from fe_loose.
- */
-typedef struct fe { u64 v[5]; } fe;
-
-/* fe_loose limbs are bounded by 3.375*2^51.
- * Addition and subtraction produce fe_loose from (fe, fe).
- */
-typedef struct fe_loose { u64 v[5]; } fe_loose;
-
-static __always_inline void fe_frombytes_impl(u64 h[5], const u8 *s)
-{
- // Ignores top bit of s.
- u64 a0 = le64_to_cpup((__force __le64 *)(s));
- u64 a1 = le64_to_cpup((__force __le64 *)(s+8));
- u64 a2 = le64_to_cpup((__force __le64 *)(s+16));
- u64 a3 = le64_to_cpup((__force __le64 *)(s+24));
- // Use 51 bits, 64-51 = 13 left.
- h[0] = a0 & ((1ULL << 51) - 1);
- // (64-51) + 38 = 13 + 38 = 51
- h[1] = (a0 >> 51) | ((a1 & ((1ULL << 38) - 1)) << 13);
- // (64-38) + 25 = 26 + 25 = 51
- h[2] = (a1 >> 38) | ((a2 & ((1ULL << 25) - 1)) << 26);
- // (64-25) + 12 = 39 + 12 = 51
- h[3] = (a2 >> 25) | ((a3 & ((1ULL << 12) - 1)) << 39);
- // (64-12) = 52, ignore top bit
- h[4] = (a3 >> 12) & ((1ULL << 51) - 1);
-}
-
-static __always_inline void fe_frombytes(fe *h, const u8 *s)
-{
- fe_frombytes_impl(h->v, s);
-}
-
-static __always_inline u8 /*bool*/ addcarryx_u51(u8 /*bool*/ c, u64 a, u64 b, u64 *low)
-{
- /* This function extracts 51 bits of result and 1 bit of carry (52 total), so
- *a 64-bit intermediate is sufficient.
- */
- u64 x = a + b + c;
- *low = x & ((1ULL << 51) - 1);
- return (x >> 51) & 1;
-}
-
-static __always_inline u8 /*bool*/ subborrow_u51(u8 /*bool*/ c, u64 a, u64 b, u64 *low)
-{
- /* This function extracts 51 bits of result and 1 bit of borrow (52 total), so
- * a 64-bit intermediate is sufficient.
- */
- u64 x = a - b - c;
- *low = x & ((1ULL << 51) - 1);
- return x >> 63;
-}
-
-static __always_inline u64 cmovznz64(u64 t, u64 z, u64 nz)
-{
- /* all set if nonzero, 0 if 0 */
- t = -!!t;
- return (t&nz) | ((~t)&z);
-}
-
-static __always_inline void fe_freeze(u64 out[5], const u64 in1[5])
-{
- { const u64 x7 = in1[4];
- { const u64 x8 = in1[3];
- { const u64 x6 = in1[2];
- { const u64 x4 = in1[1];
- { const u64 x2 = in1[0];
- { u64 x10; u8/*bool*/ x11 = subborrow_u51(0x0, x2, 0x7ffffffffffed, &x10);
- { u64 x13; u8/*bool*/ x14 = subborrow_u51(x11, x4, 0x7ffffffffffff, &x13);
- { u64 x16; u8/*bool*/ x17 = subborrow_u51(x14, x6, 0x7ffffffffffff, &x16);
- { u64 x19; u8/*bool*/ x20 = subborrow_u51(x17, x8, 0x7ffffffffffff, &x19);
- { u64 x22; u8/*bool*/ x23 = subborrow_u51(x20, x7, 0x7ffffffffffff, &x22);
- { u64 x24 = cmovznz64(x23, 0x0, 0xffffffffffffffffL);
- { u64 x25 = (x24 & 0x7ffffffffffed);
- { u64 x27; u8/*bool*/ x28 = addcarryx_u51(0x0, x10, x25, &x27);
- { u64 x29 = (x24 & 0x7ffffffffffff);
- { u64 x31; u8/*bool*/ x32 = addcarryx_u51(x28, x13, x29, &x31);
- { u64 x33 = (x24 & 0x7ffffffffffff);
- { u64 x35; u8/*bool*/ x36 = addcarryx_u51(x32, x16, x33, &x35);
- { u64 x37 = (x24 & 0x7ffffffffffff);
- { u64 x39; u8/*bool*/ x40 = addcarryx_u51(x36, x19, x37, &x39);
- { u64 x41 = (x24 & 0x7ffffffffffff);
- { u64 x43; addcarryx_u51(x40, x22, x41, &x43);
- out[0] = x27;
- out[1] = x31;
- out[2] = x35;
- out[3] = x39;
- out[4] = x43;
- }}}}}}}}}}}}}}}}}}}}}
-}
-
-static __always_inline void fe_tobytes(u8 s[32], const fe *f)
-{
- u64 h[5];
- fe_freeze(h, f->v);
-
- s[0] = h[0] >> 0;
- s[1] = h[0] >> 8;
- s[2] = h[0] >> 16;
- s[3] = h[0] >> 24;
- s[4] = h[0] >> 32;
- s[5] = h[0] >> 40;
- s[6] = (h[0] >> 48) | (h[1] << 3);
- s[7] = h[1] >> 5;
- s[8] = h[1] >> 13;
- s[9] = h[1] >> 21;
- s[10] = h[1] >> 29;
- s[11] = h[1] >> 37;
- s[12] = (h[1] >> 45) | (h[2] << 6);
- s[13] = h[2] >> 2;
- s[14] = h[2] >> 10;
- s[15] = h[2] >> 18;
- s[16] = h[2] >> 26;
- s[17] = h[2] >> 34;
- s[18] = h[2] >> 42;
- s[19] = (h[2] >> 50) | (h[3] << 1);
- s[20] = h[3] >> 7;
- s[21] = h[3] >> 15;
- s[22] = h[3] >> 23;
- s[23] = h[3] >> 31;
- s[24] = h[3] >> 39;
- s[25] = (h[3] >> 47) | (h[4] << 4);
- s[26] = h[4] >> 4;
- s[27] = h[4] >> 12;
- s[28] = h[4] >> 20;
- s[29] = h[4] >> 28;
- s[30] = h[4] >> 36;
- s[31] = h[4] >> 44;
-}
-
-/* h = f */
-static __always_inline void fe_copy(fe *h, const fe *f)
-{
- memmove(h, f, sizeof(fe));
-}
-
-static __always_inline void fe_copy_lt(fe_loose *h, const fe *f)
-{
- memmove(h, f, sizeof(fe));
-}
-
-/* h = 0 */
-static __always_inline void fe_0(fe *h)
-{
- memset(h, 0, sizeof(fe));
-}
-
-/* h = 1 */
-static __always_inline void fe_1(fe *h)
-{
- memset(h, 0, sizeof(fe));
- h->v[0] = 1;
-}
-
-static __always_inline void fe_add_impl(u64 out[5], const u64 in1[5], const u64 in2[5])
-{
- { const u64 x10 = in1[4];
- { const u64 x11 = in1[3];
- { const u64 x9 = in1[2];
- { const u64 x7 = in1[1];
- { const u64 x5 = in1[0];
- { const u64 x18 = in2[4];
- { const u64 x19 = in2[3];
- { const u64 x17 = in2[2];
- { const u64 x15 = in2[1];
- { const u64 x13 = in2[0];
- out[0] = (x5 + x13);
- out[1] = (x7 + x15);
- out[2] = (x9 + x17);
- out[3] = (x11 + x19);
- out[4] = (x10 + x18);
- }}}}}}}}}}
-}
-
-/* h = f + g
- * Can overlap h with f or g.
- */
-static __always_inline void fe_add(fe_loose *h, const fe *f, const fe *g)
-{
- fe_add_impl(h->v, f->v, g->v);
-}
-
-static __always_inline void fe_sub_impl(u64 out[5], const u64 in1[5], const u64 in2[5])
-{
- { const u64 x10 = in1[4];
- { const u64 x11 = in1[3];
- { const u64 x9 = in1[2];
- { const u64 x7 = in1[1];
- { const u64 x5 = in1[0];
- { const u64 x18 = in2[4];
- { const u64 x19 = in2[3];
- { const u64 x17 = in2[2];
- { const u64 x15 = in2[1];
- { const u64 x13 = in2[0];
- out[0] = ((0xfffffffffffda + x5) - x13);
- out[1] = ((0xffffffffffffe + x7) - x15);
- out[2] = ((0xffffffffffffe + x9) - x17);
- out[3] = ((0xffffffffffffe + x11) - x19);
- out[4] = ((0xffffffffffffe + x10) - x18);
- }}}}}}}}}}
-}
-
-/* h = f - g
- * Can overlap h with f or g.
- */
-static __always_inline void fe_sub(fe_loose *h, const fe *f, const fe *g)
-{
- fe_sub_impl(h->v, f->v, g->v);
-}
-
-static __always_inline void fe_mul_impl(u64 out[5], const u64 in1[5], const u64 in2[5])
-{
- { const u64 x10 = in1[4];
- { const u64 x11 = in1[3];
- { const u64 x9 = in1[2];
- { const u64 x7 = in1[1];
- { const u64 x5 = in1[0];
- { const u64 x18 = in2[4];
- { const u64 x19 = in2[3];
- { const u64 x17 = in2[2];
- { const u64 x15 = in2[1];
- { const u64 x13 = in2[0];
- { u128 x20 = ((u128)x5 * x13);
- { u128 x21 = (((u128)x5 * x15) + ((u128)x7 * x13));
- { u128 x22 = ((((u128)x5 * x17) + ((u128)x9 * x13)) + ((u128)x7 * x15));
- { u128 x23 = (((((u128)x5 * x19) + ((u128)x11 * x13)) + ((u128)x7 * x17)) + ((u128)x9 * x15));
- { u128 x24 = ((((((u128)x5 * x18) + ((u128)x10 * x13)) + ((u128)x11 * x15)) + ((u128)x7 * x19)) + ((u128)x9 * x17));
- { u64 x25 = (x10 * 0x13);
- { u64 x26 = (x7 * 0x13);
- { u64 x27 = (x9 * 0x13);
- { u64 x28 = (x11 * 0x13);
- { u128 x29 = ((((x20 + ((u128)x25 * x15)) + ((u128)x26 * x18)) + ((u128)x27 * x19)) + ((u128)x28 * x17));
- { u128 x30 = (((x21 + ((u128)x25 * x17)) + ((u128)x27 * x18)) + ((u128)x28 * x19));
- { u128 x31 = ((x22 + ((u128)x25 * x19)) + ((u128)x28 * x18));
- { u128 x32 = (x23 + ((u128)x25 * x18));
- { u64 x33 = (u64) (x29 >> 0x33);
- { u64 x34 = ((u64)x29 & 0x7ffffffffffff);
- { u128 x35 = (x33 + x30);
- { u64 x36 = (u64) (x35 >> 0x33);
- { u64 x37 = ((u64)x35 & 0x7ffffffffffff);
- { u128 x38 = (x36 + x31);
- { u64 x39 = (u64) (x38 >> 0x33);
- { u64 x40 = ((u64)x38 & 0x7ffffffffffff);
- { u128 x41 = (x39 + x32);
- { u64 x42 = (u64) (x41 >> 0x33);
- { u64 x43 = ((u64)x41 & 0x7ffffffffffff);
- { u128 x44 = (x42 + x24);
- { u64 x45 = (u64) (x44 >> 0x33);
- { u64 x46 = ((u64)x44 & 0x7ffffffffffff);
- { u64 x47 = (x34 + (0x13 * x45));
- { u64 x48 = (x47 >> 0x33);
- { u64 x49 = (x47 & 0x7ffffffffffff);
- { u64 x50 = (x48 + x37);
- { u64 x51 = (x50 >> 0x33);
- { u64 x52 = (x50 & 0x7ffffffffffff);
- out[0] = x49;
- out[1] = x52;
- out[2] = (x51 + x40);
- out[3] = x43;
- out[4] = x46;
- }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}
-}
-
-static __always_inline void fe_mul_ttt(fe *h, const fe *f, const fe *g)
-{
- fe_mul_impl(h->v, f->v, g->v);
-}
-
-static __always_inline void fe_mul_tlt(fe *h, const fe_loose *f, const fe *g)
-{
- fe_mul_impl(h->v, f->v, g->v);
-}
-
-static __always_inline void fe_mul_tll(fe *h, const fe_loose *f, const fe_loose *g)
-{
- fe_mul_impl(h->v, f->v, g->v);
-}
-
-
-static __always_inline void fe_sqr_impl(u64 out[5], const u64 in1[5])
-{
- { const u64 x7 = in1[4];
- { const u64 x8 = in1[3];
- { const u64 x6 = in1[2];
- { const u64 x4 = in1[1];
- { const u64 x2 = in1[0];
- { u64 x9 = (x2 * 0x2);
- { u64 x10 = (x4 * 0x2);
- { u64 x11 = ((x6 * 0x2) * 0x13);
- { u64 x12 = (x7 * 0x13);
- { u64 x13 = (x12 * 0x2);
- { u128 x14 = ((((u128)x2 * x2) + ((u128)x13 * x4)) + ((u128)x11 * x8));
- { u128 x15 = ((((u128)x9 * x4) + ((u128)x13 * x6)) + ((u128)x8 * (x8 * 0x13)));
- { u128 x16 = ((((u128)x9 * x6) + ((u128)x4 * x4)) + ((u128)x13 * x8));
- { u128 x17 = ((((u128)x9 * x8) + ((u128)x10 * x6)) + ((u128)x7 * x12));
- { u128 x18 = ((((u128)x9 * x7) + ((u128)x10 * x8)) + ((u128)x6 * x6));
- { u64 x19 = (u64) (x14 >> 0x33);
- { u64 x20 = ((u64)x14 & 0x7ffffffffffff);
- { u128 x21 = (x19 + x15);
- { u64 x22 = (u64) (x21 >> 0x33);
- { u64 x23 = ((u64)x21 & 0x7ffffffffffff);
- { u128 x24 = (x22 + x16);
- { u64 x25 = (u64) (x24 >> 0x33);
- { u64 x26 = ((u64)x24 & 0x7ffffffffffff);
- { u128 x27 = (x25 + x17);
- { u64 x28 = (u64) (x27 >> 0x33);
- { u64 x29 = ((u64)x27 & 0x7ffffffffffff);
- { u128 x30 = (x28 + x18);
- { u64 x31 = (u64) (x30 >> 0x33);
- { u64 x32 = ((u64)x30 & 0x7ffffffffffff);
- { u64 x33 = (x20 + (0x13 * x31));
- { u64 x34 = (x33 >> 0x33);
- { u64 x35 = (x33 & 0x7ffffffffffff);
- { u64 x36 = (x34 + x23);
- { u64 x37 = (x36 >> 0x33);
- { u64 x38 = (x36 & 0x7ffffffffffff);
- out[0] = x35;
- out[1] = x38;
- out[2] = (x37 + x26);
- out[3] = x29;
- out[4] = x32;
- }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}
-}
-
-static __always_inline void fe_sq_tl(fe *h, const fe_loose *f)
-{
- fe_sqr_impl(h->v, f->v);
-}
-
-static __always_inline void fe_sq_tt(fe *h, const fe *f)
-{
- fe_sqr_impl(h->v, f->v);
-}
-
-static __always_inline void fe_loose_invert(fe *out, const fe_loose *z)
-{
- fe t0;
- fe t1;
- fe t2;
- fe t3;
- int i;
-
- fe_sq_tl(&t0, z);
- fe_sq_tt(&t1, &t0);
- for (i = 1; i < 2; ++i)
- fe_sq_tt(&t1, &t1);
- fe_mul_tlt(&t1, z, &t1);
- fe_mul_ttt(&t0, &t0, &t1);
- fe_sq_tt(&t2, &t0);
- fe_mul_ttt(&t1, &t1, &t2);
- fe_sq_tt(&t2, &t1);
- for (i = 1; i < 5; ++i)
- fe_sq_tt(&t2, &t2);
- fe_mul_ttt(&t1, &t2, &t1);
- fe_sq_tt(&t2, &t1);
- for (i = 1; i < 10; ++i)
- fe_sq_tt(&t2, &t2);
- fe_mul_ttt(&t2, &t2, &t1);
- fe_sq_tt(&t3, &t2);
- for (i = 1; i < 20; ++i)
- fe_sq_tt(&t3, &t3);
- fe_mul_ttt(&t2, &t3, &t2);
- fe_sq_tt(&t2, &t2);
- for (i = 1; i < 10; ++i)
- fe_sq_tt(&t2, &t2);
- fe_mul_ttt(&t1, &t2, &t1);
- fe_sq_tt(&t2, &t1);
- for (i = 1; i < 50; ++i)
- fe_sq_tt(&t2, &t2);
- fe_mul_ttt(&t2, &t2, &t1);
- fe_sq_tt(&t3, &t2);
- for (i = 1; i < 100; ++i)
- fe_sq_tt(&t3, &t3);
- fe_mul_ttt(&t2, &t3, &t2);
- fe_sq_tt(&t2, &t2);
- for (i = 1; i < 50; ++i)
- fe_sq_tt(&t2, &t2);
- fe_mul_ttt(&t1, &t2, &t1);
- fe_sq_tt(&t1, &t1);
- for (i = 1; i < 5; ++i)
- fe_sq_tt(&t1, &t1);
- fe_mul_ttt(out, &t1, &t0);
-}
-
-static __always_inline void fe_invert(fe *out, const fe *z)
-{
- fe_loose l;
- fe_copy_lt(&l, z);
- fe_loose_invert(out, &l);
-}
-
-/* Replace (f,g) with (g,f) if b == 1;
- * replace (f,g) with (f,g) if b == 0.
- *
- * Preconditions: b in {0,1}
- */
-static __always_inline void fe_cswap(fe *f, fe *g, u64 b)
-{
- unsigned i;
- b = 0-b;
- for (i = 0; i < 5; i++) {
- u64 x = f->v[i] ^ g->v[i];
- x &= b;
- f->v[i] ^= x;
- g->v[i] ^= x;
- }
-}
-
-/* NOTE: based on fiat-crypto fe_mul, edited for in2=121666, 0, 0.*/
-static __always_inline void fe_mul_121666_impl(u64 out[5], const u64 in1[5])
-{
- { const u64 x10 = in1[4];
- { const u64 x11 = in1[3];
- { const u64 x9 = in1[2];
- { const u64 x7 = in1[1];
- { const u64 x5 = in1[0];
- { const u64 x18 = 0;
- { const u64 x19 = 0;
- { const u64 x17 = 0;
- { const u64 x15 = 0;
- { const u64 x13 = 121666;
- { u128 x20 = ((u128)x5 * x13);
- { u128 x21 = (((u128)x5 * x15) + ((u128)x7 * x13));
- { u128 x22 = ((((u128)x5 * x17) + ((u128)x9 * x13)) + ((u128)x7 * x15));
- { u128 x23 = (((((u128)x5 * x19) + ((u128)x11 * x13)) + ((u128)x7 * x17)) + ((u128)x9 * x15));
- { u128 x24 = ((((((u128)x5 * x18) + ((u128)x10 * x13)) + ((u128)x11 * x15)) + ((u128)x7 * x19)) + ((u128)x9 * x17));
- { u64 x25 = (x10 * 0x13);
- { u64 x26 = (x7 * 0x13);
- { u64 x27 = (x9 * 0x13);
- { u64 x28 = (x11 * 0x13);
- { u128 x29 = ((((x20 + ((u128)x25 * x15)) + ((u128)x26 * x18)) + ((u128)x27 * x19)) + ((u128)x28 * x17));
- { u128 x30 = (((x21 + ((u128)x25 * x17)) + ((u128)x27 * x18)) + ((u128)x28 * x19));
- { u128 x31 = ((x22 + ((u128)x25 * x19)) + ((u128)x28 * x18));
- { u128 x32 = (x23 + ((u128)x25 * x18));
- { u64 x33 = (u64) (x29 >> 0x33);
- { u64 x34 = ((u64)x29 & 0x7ffffffffffff);
- { u128 x35 = (x33 + x30);
- { u64 x36 = (u64) (x35 >> 0x33);
- { u64 x37 = ((u64)x35 & 0x7ffffffffffff);
- { u128 x38 = (x36 + x31);
- { u64 x39 = (u64) (x38 >> 0x33);
- { u64 x40 = ((u64)x38 & 0x7ffffffffffff);
- { u128 x41 = (x39 + x32);
- { u64 x42 = (u64) (x41 >> 0x33);
- { u64 x43 = ((u64)x41 & 0x7ffffffffffff);
- { u128 x44 = (x42 + x24);
- { u64 x45 = (u64) (x44 >> 0x33);
- { u64 x46 = ((u64)x44 & 0x7ffffffffffff);
- { u64 x47 = (x34 + (0x13 * x45));
- { u64 x48 = (x47 >> 0x33);
- { u64 x49 = (x47 & 0x7ffffffffffff);
- { u64 x50 = (x48 + x37);
- { u64 x51 = (x50 >> 0x33);
- { u64 x52 = (x50 & 0x7ffffffffffff);
- out[0] = x49;
- out[1] = x52;
- out[2] = (x51 + x40);
- out[3] = x43;
- out[4] = x46;
- }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}
-}
-
-static __always_inline void fe_mul121666(fe *h, const fe_loose *f)
-{
- fe_mul_121666_impl(h->v, f->v);
-}
-
-bool curve25519_fiat64(u8 out[CURVE25519_POINT_SIZE], const u8 scalar[CURVE25519_POINT_SIZE], const u8 point[CURVE25519_POINT_SIZE])
-{
- fe x1, x2, z2, x3, z3, tmp0, tmp1;
- fe_loose x2l, z2l, x3l, tmp0l, tmp1l;
- unsigned swap = 0;
- int pos;
- u8 e[32];
-
- memcpy(e, scalar, 32);
- normalize_secret(e);
-
- /* The following implementation was transcribed to Coq and proven to
- * correspond to unary scalar multiplication in affine coordinates given that
- * x1 != 0 is the x coordinate of some point on the curve. It was also checked
- * in Coq that doing a ladderstep with x1 = x3 = 0 gives z2' = z3' = 0, and z2
- * = z3 = 0 gives z2' = z3' = 0. The statement was quantified over the
- * underlying field, so it applies to Curve25519 itself and the quadratic
- * twist of Curve25519. It was not proven in Coq that prime-field arithmetic
- * correctly simulates extension-field arithmetic on prime-field values.
- * The decoding of the byte array representation of e was not considered.
- * Specification of Montgomery curves in affine coordinates:
- * <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Spec/MontgomeryCurve.v#L27>
- * Proof that these form a group that is isomorphic to a Weierstrass curve:
- * <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves/Montgomery/AffineProofs.v#L35>
- * Coq transcription and correctness proof of the loop (where scalarbits=255):
- * <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves/Montgomery/XZ.v#L118>
- * <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves/Montgomery/XZProofs.v#L278>
- * preconditions: 0 <= e < 2^255 (not necessarily e < order), fe_invert(0) = 0
- */
- fe_frombytes(&x1, point);
- fe_1(&x2);
- fe_0(&z2);
- fe_copy(&x3, &x1);
- fe_1(&z3);
-
- for (pos = 254; pos >= 0; --pos) {
- /* loop invariant as of right before the test, for the case where x1 != 0:
- * pos >= -1; if z2 = 0 then x2 is nonzero; if z3 = 0 then x3 is nonzero
- * let r := e >> (pos+1) in the following equalities of projective points:
- * to_xz (r*P) === if swap then (x3, z3) else (x2, z2)
- * to_xz ((r+1)*P) === if swap then (x2, z2) else (x3, z3)
- * x1 is the nonzero x coordinate of the nonzero point (r*P-(r+1)*P)
- */
- unsigned b = 1 & (e[pos / 8] >> (pos & 7));
- swap ^= b;
- fe_cswap(&x2, &x3, swap);
- fe_cswap(&z2, &z3, swap);
- swap = b;
- /* Coq transcription of ladderstep formula (called from transcribed loop):
- * <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves/Montgomery/XZ.v#L89>
- * <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves/Montgomery/XZProofs.v#L131>
- * x1 != 0 <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves/Montgomery/XZProofs.v#L217>
- * x1 = 0 <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves/Montgomery/XZProofs.v#L147>
- */
- fe_sub(&tmp0l, &x3, &z3);
- fe_sub(&tmp1l, &x2, &z2);
- fe_add(&x2l, &x2, &z2);
- fe_add(&z2l, &x3, &z3);
- fe_mul_tll(&z3, &tmp0l, &x2l);
- fe_mul_tll(&z2, &z2l, &tmp1l);
- fe_sq_tl(&tmp0, &tmp1l);
- fe_sq_tl(&tmp1, &x2l);
- fe_add(&x3l, &z3, &z2);
- fe_sub(&z2l, &z3, &z2);
- fe_mul_ttt(&x2, &tmp1, &tmp0);
- fe_sub(&tmp1l, &tmp1, &tmp0);
- fe_sq_tl(&z2, &z2l);
- fe_mul121666(&z3, &tmp1l);
- fe_sq_tl(&x3, &x3l);
- fe_add(&tmp0l, &tmp0, &z3);
- fe_mul_ttt(&z3, &x1, &z2);
- fe_mul_tll(&z2, &tmp1l, &tmp0l);
- }
- /* here pos=-1, so r=e, so to_xz (e*P) === if swap then (x3, z3) else (x2, z2) */
- fe_cswap(&x2, &x3, swap);
- fe_cswap(&z2, &z3, swap);
-
- fe_invert(&z2, &z2);
- fe_mul_ttt(&x2, &x2, &z2);
- fe_tobytes(out, &x2);
-
- return true;
-}
Copyright © 1996 – 2023 Jason A. Donenfeld. All Rights Reverse Engineered.