diff options
Diffstat (limited to 'lib/freebl/ecl/ecp_secp521r1.c')
| -rw-r--r-- | lib/freebl/ecl/ecp_secp521r1.c | 1186 |
1 files changed, 622 insertions, 564 deletions
diff --git a/lib/freebl/ecl/ecp_secp521r1.c b/lib/freebl/ecl/ecp_secp521r1.c index d673eccca..57e3a81b8 100644 --- a/lib/freebl/ecl/ecp_secp521r1.c +++ b/lib/freebl/ecl/ecp_secp521r1.c @@ -1,19 +1,19 @@ /* Autogenerated: ECCKiila https://gitlab.com/nisec/ecckiila */ /*- * MIT License - * + * * Copyright (c) 2020 Luis Rivera-Zamarripa, Jesús-Javier Chi-Domínguez, Billy Bob Brumley - * + * * Permission is hereby granted, free of charge, to any person obtaining a copy * of this software and associated documentation files (the "Software"), to deal * in the Software without restriction, including without limitation the rights * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell * copies of the Software, and to permit persons to whom the Software is * furnished to do so, subject to the following conditions: - * + * * The above copyright notice and this permission notice shall be included in all * copies or substantial portions of the Software. - * + * * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE @@ -35,13 +35,6 @@ typedef uint64_t limb_t; #define fe_copy(d, s) memcpy(d, s, sizeof(fe_t)) #define fe_set_zero(d) memset(d, 0, sizeof(fe_t)) -#define fiat_secp521r1_carry_add(c, a, b) \ - fiat_secp521r1_add(c, a, b); \ - fiat_secp521r1_carry(c, c) -#define fiat_secp521r1_carry_sub(c, a, b) \ - fiat_secp521r1_sub(c, a, b); \ - fiat_secp521r1_carry(c, c) - /* Projective points */ typedef struct { fe_t X; @@ -90,16 +83,32 @@ typedef struct { /* tight_bounds_multiplier = 1 (from "") */ /* */ /* Computed values: */ -/* carry_chain = [0, 1, 2, 3, 4, 5, 6, 7, 8, 0, 1] */ -/* eval z = z[0] + (z[1] << 58) + (z[2] << 116) + (z[3] << 174) + (z[4] << 232) + (z[5] << 0x122) + (z[6] << 0x15c) + (z[7] << 0x196) + (z[8] << 0x1d0) */ -/* bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) + (z[32] << 256) + (z[33] << 0x108) + (z[34] << 0x110) + (z[35] << 0x118) + (z[36] << 0x120) + (z[37] << 0x128) + (z[38] << 0x130) + (z[39] << 0x138) + (z[40] << 0x140) + (z[41] << 0x148) + (z[42] << 0x150) + (z[43] << 0x158) + (z[44] << 0x160) + (z[45] << 0x168) + (z[46] << 0x170) + (z[47] << 0x178) + (z[48] << 0x180) + (z[49] << 0x188) + (z[50] << 0x190) + (z[51] << 0x198) + (z[52] << 0x1a0) + (z[53] << 0x1a8) + (z[54] << 0x1b0) + (z[55] << 0x1b8) + (z[56] << 0x1c0) + (z[57] << 0x1c8) + (z[58] << 0x1d0) + (z[59] << 0x1d8) + (z[60] << 0x1e0) + (z[61] << 0x1e8) + (z[62] << 0x1f0) + (z[63] << 0x1f8) + (z[64] << 2^9) + (z[65] << 0x208) */ -/* balance = [0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x3fffffffffffffe] */ +/* carry_chain = [0, 1, 2, 3, 4, 5, 6, 7, 8, 0, 1] */ +/* eval z = z[0] + (z[1] << 58) + (z[2] << 116) + (z[3] << 174) + (z[4] << 232) + (z[5] << 0x122) + (z[6] << 0x15c) + (z[7] << 0x196) + (z[8] << 0x1d0) */ +/* bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) + (z[32] << 256) + (z[33] << 0x108) + (z[34] << 0x110) + (z[35] << 0x118) + (z[36] << 0x120) + (z[37] << 0x128) + (z[38] << 0x130) + (z[39] << 0x138) + (z[40] << 0x140) + (z[41] << 0x148) + (z[42] << 0x150) + (z[43] << 0x158) + (z[44] << 0x160) + (z[45] << 0x168) + (z[46] << 0x170) + (z[47] << 0x178) + (z[48] << 0x180) + (z[49] << 0x188) + (z[50] << 0x190) + (z[51] << 0x198) + (z[52] << 0x1a0) + (z[53] << 0x1a8) + (z[54] << 0x1b0) + (z[55] << 0x1b8) + (z[56] << 0x1c0) + (z[57] << 0x1c8) + (z[58] << 0x1d0) + (z[59] << 0x1d8) + (z[60] << 0x1e0) + (z[61] << 0x1e8) + (z[62] << 0x1f0) + (z[63] << 0x1f8) + (z[64] << 2^9) + (z[65] << 0x208) */ +/* balance = [0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x3fffffffffffffe] */ #include <stdint.h> typedef unsigned char fiat_secp521r1_uint1; typedef signed char fiat_secp521r1_int1; -typedef signed __int128 fiat_secp521r1_int128; -typedef unsigned __int128 fiat_secp521r1_uint128; +#ifdef __GNUC__ +#define FIAT_SECP521R1_FIAT_EXTENSION __extension__ +#define FIAT_SECP521R1_FIAT_INLINE __inline__ +#else +#define FIAT_SECP521R1_FIAT_EXTENSION +#define FIAT_SECP521R1_FIAT_INLINE +#endif + +FIAT_SECP521R1_FIAT_EXTENSION typedef signed __int128 fiat_secp521r1_int128; +FIAT_SECP521R1_FIAT_EXTENSION typedef unsigned __int128 fiat_secp521r1_uint128; + +/* The type fiat_secp521r1_loose_field_element is a field element with loose bounds. */ +/* Bounds: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]] */ +typedef uint64_t fiat_secp521r1_loose_field_element[9]; + +/* The type fiat_secp521r1_tight_field_element is a field element with tight bounds. */ +/* Bounds: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]] */ +typedef uint64_t fiat_secp521r1_tight_field_element[9]; #if (-1 & 3) != 3 #error "This code only works on a two's complement system" @@ -120,6 +129,7 @@ fiat_secp521r1_value_barrier_u64(uint64_t a) /* * The function fiat_secp521r1_addcarryx_u58 is an addition with carry. + * * Postconditions: * out1 = (arg1 + arg2 + arg3) mod 2^58 * out2 = ⌊(arg1 + arg2 + arg3) / 2^58⌋ @@ -150,6 +160,7 @@ fiat_secp521r1_addcarryx_u58(uint64_t *out1, /* * The function fiat_secp521r1_subborrowx_u58 is a subtraction with borrow. + * * Postconditions: * out1 = (-arg1 + arg2 + -arg3) mod 2^58 * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^58⌋ @@ -180,6 +191,7 @@ fiat_secp521r1_subborrowx_u58(uint64_t *out1, /* * The function fiat_secp521r1_addcarryx_u57 is an addition with carry. + * * Postconditions: * out1 = (arg1 + arg2 + arg3) mod 2^57 * out2 = ⌊(arg1 + arg2 + arg3) / 2^57⌋ @@ -210,6 +222,7 @@ fiat_secp521r1_addcarryx_u57(uint64_t *out1, /* * The function fiat_secp521r1_subborrowx_u57 is a subtraction with borrow. + * * Postconditions: * out1 = (-arg1 + arg2 + -arg3) mod 2^57 * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^57⌋ @@ -240,6 +253,7 @@ fiat_secp521r1_subborrowx_u57(uint64_t *out1, /* * The function fiat_secp521r1_cmovznz_u64 is a single-word conditional move. + * * Postconditions: * out1 = (if arg1 = 0 then arg2 else arg3) * @@ -267,18 +281,16 @@ fiat_secp521r1_cmovznz_u64(uint64_t *out1, /* * The function fiat_secp521r1_carry_mul multiplies two field elements and reduces the result. + * * Postconditions: * eval out1 mod m = (eval arg1 * eval arg2) mod m * - * Input Bounds: - * arg1: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]] - * arg2: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]] - * Output Bounds: - * out1: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]] */ static void -fiat_secp521r1_carry_mul(uint64_t out1[9], const uint64_t arg1[9], - const uint64_t arg2[9]) +fiat_secp521r1_carry_mul( + fiat_secp521r1_tight_field_element out1, + const fiat_secp521r1_loose_field_element arg1, + const fiat_secp521r1_loose_field_element arg2) { fiat_secp521r1_uint128 x1; fiat_secp521r1_uint128 x2; @@ -539,17 +551,15 @@ fiat_secp521r1_carry_mul(uint64_t out1[9], const uint64_t arg1[9], /* * The function fiat_secp521r1_carry_square squares a field element and reduces the result. + * * Postconditions: * eval out1 mod m = (eval arg1 * eval arg1) mod m * - * Input Bounds: - * arg1: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]] - * Output Bounds: - * out1: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]] */ static void -fiat_secp521r1_carry_square(uint64_t out1[9], - const uint64_t arg1[9]) +fiat_secp521r1_carry_square( + fiat_secp521r1_tight_field_element out1, + const fiat_secp521r1_loose_field_element arg1) { uint64_t x1; uint64_t x2; @@ -769,17 +779,17 @@ fiat_secp521r1_carry_square(uint64_t out1[9], } /* - * The function fiat_secp521r1_carry reduces a field element. + * The function fiat_secp521r1_carry_add adds two field elements. + * * Postconditions: - * eval out1 mod m = eval arg1 mod m + * eval out1 mod m = (eval arg1 + eval arg2) mod m * - * Input Bounds: - * arg1: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]] - * Output Bounds: - * out1: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]] */ static void -fiat_secp521r1_carry(uint64_t out1[9], const uint64_t arg1[9]) +fiat_secp521r1_carry_add( + fiat_secp521r1_tight_field_element out1, + const fiat_secp521r1_tight_field_element arg1, + const fiat_secp521r1_tight_field_element arg2) { uint64_t x1; uint64_t x2; @@ -801,15 +811,15 @@ fiat_secp521r1_carry(uint64_t out1[9], const uint64_t arg1[9]) uint64_t x18; uint64_t x19; uint64_t x20; - x1 = (arg1[0]); - x2 = ((x1 >> 58) + (arg1[1])); - x3 = ((x2 >> 58) + (arg1[2])); - x4 = ((x3 >> 58) + (arg1[3])); - x5 = ((x4 >> 58) + (arg1[4])); - x6 = ((x5 >> 58) + (arg1[5])); - x7 = ((x6 >> 58) + (arg1[6])); - x8 = ((x7 >> 58) + (arg1[7])); - x9 = ((x8 >> 58) + (arg1[8])); + x1 = ((arg1[0]) + (arg2[0])); + x2 = ((x1 >> 58) + ((arg1[1]) + (arg2[1]))); + x3 = ((x2 >> 58) + ((arg1[2]) + (arg2[2]))); + x4 = ((x3 >> 58) + ((arg1[3]) + (arg2[3]))); + x5 = ((x4 >> 58) + ((arg1[4]) + (arg2[4]))); + x6 = ((x5 >> 58) + ((arg1[5]) + (arg2[5]))); + x7 = ((x6 >> 58) + ((arg1[6]) + (arg2[6]))); + x8 = ((x7 >> 58) + ((arg1[7]) + (arg2[7]))); + x9 = ((x8 >> 58) + ((arg1[8]) + (arg2[8]))); x10 = ((x1 & UINT64_C(0x3ffffffffffffff)) + (x9 >> 57)); x11 = ((fiat_secp521r1_uint1)(x10 >> 58) + (x2 & UINT64_C(0x3ffffffffffffff))); @@ -835,63 +845,17 @@ fiat_secp521r1_carry(uint64_t out1[9], const uint64_t arg1[9]) } /* - * The function fiat_secp521r1_add adds two field elements. - * Postconditions: - * eval out1 mod m = (eval arg1 + eval arg2) mod m + * The function fiat_secp521r1_carry_sub subtracts two field elements. * - * Input Bounds: - * arg1: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]] - * arg2: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]] - * Output Bounds: - * out1: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]] - */ -static void -fiat_secp521r1_add(uint64_t out1[9], const uint64_t arg1[9], - const uint64_t arg2[9]) -{ - uint64_t x1; - uint64_t x2; - uint64_t x3; - uint64_t x4; - uint64_t x5; - uint64_t x6; - uint64_t x7; - uint64_t x8; - uint64_t x9; - x1 = ((arg1[0]) + (arg2[0])); - x2 = ((arg1[1]) + (arg2[1])); - x3 = ((arg1[2]) + (arg2[2])); - x4 = ((arg1[3]) + (arg2[3])); - x5 = ((arg1[4]) + (arg2[4])); - x6 = ((arg1[5]) + (arg2[5])); - x7 = ((arg1[6]) + (arg2[6])); - x8 = ((arg1[7]) + (arg2[7])); - x9 = ((arg1[8]) + (arg2[8])); - out1[0] = x1; - out1[1] = x2; - out1[2] = x3; - out1[3] = x4; - out1[4] = x5; - out1[5] = x6; - out1[6] = x7; - out1[7] = x8; - out1[8] = x9; -} - -/* - * The function fiat_secp521r1_sub subtracts two field elements. * Postconditions: * eval out1 mod m = (eval arg1 - eval arg2) mod m * - * Input Bounds: - * arg1: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]] - * arg2: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]] - * Output Bounds: - * out1: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]] */ static void -fiat_secp521r1_sub(uint64_t out1[9], const uint64_t arg1[9], - const uint64_t arg2[9]) +fiat_secp521r1_carry_sub( + fiat_secp521r1_tight_field_element out1, + const fiat_secp521r1_tight_field_element arg1, + const fiat_secp521r1_tight_field_element arg2) { uint64_t x1; uint64_t x2; @@ -902,38 +866,61 @@ fiat_secp521r1_sub(uint64_t out1[9], const uint64_t arg1[9], uint64_t x7; uint64_t x8; uint64_t x9; + uint64_t x10; + uint64_t x11; + uint64_t x12; + uint64_t x13; + uint64_t x14; + uint64_t x15; + uint64_t x16; + uint64_t x17; + uint64_t x18; + uint64_t x19; + uint64_t x20; x1 = ((UINT64_C(0x7fffffffffffffe) + (arg1[0])) - (arg2[0])); - x2 = ((UINT64_C(0x7fffffffffffffe) + (arg1[1])) - (arg2[1])); - x3 = ((UINT64_C(0x7fffffffffffffe) + (arg1[2])) - (arg2[2])); - x4 = ((UINT64_C(0x7fffffffffffffe) + (arg1[3])) - (arg2[3])); - x5 = ((UINT64_C(0x7fffffffffffffe) + (arg1[4])) - (arg2[4])); - x6 = ((UINT64_C(0x7fffffffffffffe) + (arg1[5])) - (arg2[5])); - x7 = ((UINT64_C(0x7fffffffffffffe) + (arg1[6])) - (arg2[6])); - x8 = ((UINT64_C(0x7fffffffffffffe) + (arg1[7])) - (arg2[7])); - x9 = ((UINT64_C(0x3fffffffffffffe) + (arg1[8])) - (arg2[8])); - out1[0] = x1; - out1[1] = x2; - out1[2] = x3; - out1[3] = x4; - out1[4] = x5; - out1[5] = x6; - out1[6] = x7; - out1[7] = x8; - out1[8] = x9; + x2 = ((x1 >> 58) + ((UINT64_C(0x7fffffffffffffe) + (arg1[1])) - (arg2[1]))); + x3 = ((x2 >> 58) + ((UINT64_C(0x7fffffffffffffe) + (arg1[2])) - (arg2[2]))); + x4 = ((x3 >> 58) + ((UINT64_C(0x7fffffffffffffe) + (arg1[3])) - (arg2[3]))); + x5 = ((x4 >> 58) + ((UINT64_C(0x7fffffffffffffe) + (arg1[4])) - (arg2[4]))); + x6 = ((x5 >> 58) + ((UINT64_C(0x7fffffffffffffe) + (arg1[5])) - (arg2[5]))); + x7 = ((x6 >> 58) + ((UINT64_C(0x7fffffffffffffe) + (arg1[6])) - (arg2[6]))); + x8 = ((x7 >> 58) + ((UINT64_C(0x7fffffffffffffe) + (arg1[7])) - (arg2[7]))); + x9 = ((x8 >> 58) + ((UINT64_C(0x3fffffffffffffe) + (arg1[8])) - (arg2[8]))); + x10 = ((x1 & UINT64_C(0x3ffffffffffffff)) + (x9 >> 57)); + x11 = ((fiat_secp521r1_uint1)(x10 >> 58) + + (x2 & UINT64_C(0x3ffffffffffffff))); + x12 = (x10 & UINT64_C(0x3ffffffffffffff)); + x13 = (x11 & UINT64_C(0x3ffffffffffffff)); + x14 = ((fiat_secp521r1_uint1)(x11 >> 58) + + (x3 & UINT64_C(0x3ffffffffffffff))); + x15 = (x4 & UINT64_C(0x3ffffffffffffff)); + x16 = (x5 & UINT64_C(0x3ffffffffffffff)); + x17 = (x6 & UINT64_C(0x3ffffffffffffff)); + x18 = (x7 & UINT64_C(0x3ffffffffffffff)); + x19 = (x8 & UINT64_C(0x3ffffffffffffff)); + x20 = (x9 & UINT64_C(0x1ffffffffffffff)); + out1[0] = x12; + out1[1] = x13; + out1[2] = x14; + out1[3] = x15; + out1[4] = x16; + out1[5] = x17; + out1[6] = x18; + out1[7] = x19; + out1[8] = x20; } /* - * The function fiat_secp521r1_opp negates a field element. + * The function fiat_secp521r1_carry_opp negates a field element. + * * Postconditions: * eval out1 mod m = -eval arg1 mod m * - * Input Bounds: - * arg1: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]] - * Output Bounds: - * out1: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]] */ static void -fiat_secp521r1_opp(uint64_t out1[9], const uint64_t arg1[9]) +fiat_secp521r1_carry_opp( + fiat_secp521r1_tight_field_element out1, + const fiat_secp521r1_tight_field_element arg1) { uint64_t x1; uint64_t x2; @@ -944,28 +931,62 @@ fiat_secp521r1_opp(uint64_t out1[9], const uint64_t arg1[9]) uint64_t x7; uint64_t x8; uint64_t x9; + uint64_t x10; + uint64_t x11; + uint64_t x12; + uint64_t x13; + uint64_t x14; + uint64_t x15; + uint64_t x16; + uint64_t x17; + uint64_t x18; + uint64_t x19; + uint64_t x20; x1 = (UINT64_C(0x7fffffffffffffe) - (arg1[0])); - x2 = (UINT64_C(0x7fffffffffffffe) - (arg1[1])); - x3 = (UINT64_C(0x7fffffffffffffe) - (arg1[2])); - x4 = (UINT64_C(0x7fffffffffffffe) - (arg1[3])); - x5 = (UINT64_C(0x7fffffffffffffe) - (arg1[4])); - x6 = (UINT64_C(0x7fffffffffffffe) - (arg1[5])); - x7 = (UINT64_C(0x7fffffffffffffe) - (arg1[6])); - x8 = (UINT64_C(0x7fffffffffffffe) - (arg1[7])); - x9 = (UINT64_C(0x3fffffffffffffe) - (arg1[8])); - out1[0] = x1; - out1[1] = x2; - out1[2] = x3; - out1[3] = x4; - out1[4] = x5; - out1[5] = x6; - out1[6] = x7; - out1[7] = x8; - out1[8] = x9; + x2 = ((fiat_secp521r1_uint1)(x1 >> 58) + + (UINT64_C(0x7fffffffffffffe) - (arg1[1]))); + x3 = ((fiat_secp521r1_uint1)(x2 >> 58) + + (UINT64_C(0x7fffffffffffffe) - (arg1[2]))); + x4 = ((fiat_secp521r1_uint1)(x3 >> 58) + + (UINT64_C(0x7fffffffffffffe) - (arg1[3]))); + x5 = ((fiat_secp521r1_uint1)(x4 >> 58) + + (UINT64_C(0x7fffffffffffffe) - (arg1[4]))); + x6 = ((fiat_secp521r1_uint1)(x5 >> 58) + + (UINT64_C(0x7fffffffffffffe) - (arg1[5]))); + x7 = ((fiat_secp521r1_uint1)(x6 >> 58) + + (UINT64_C(0x7fffffffffffffe) - (arg1[6]))); + x8 = ((fiat_secp521r1_uint1)(x7 >> 58) + + (UINT64_C(0x7fffffffffffffe) - (arg1[7]))); + x9 = ((fiat_secp521r1_uint1)(x8 >> 58) + + (UINT64_C(0x3fffffffffffffe) - (arg1[8]))); + x10 = ((x1 & UINT64_C(0x3ffffffffffffff)) + + (uint64_t)(fiat_secp521r1_uint1)(x9 >> 57)); + x11 = ((fiat_secp521r1_uint1)(x10 >> 58) + + (x2 & UINT64_C(0x3ffffffffffffff))); + x12 = (x10 & UINT64_C(0x3ffffffffffffff)); + x13 = (x11 & UINT64_C(0x3ffffffffffffff)); + x14 = ((fiat_secp521r1_uint1)(x11 >> 58) + + (x3 & UINT64_C(0x3ffffffffffffff))); + x15 = (x4 & UINT64_C(0x3ffffffffffffff)); + x16 = (x5 & UINT64_C(0x3ffffffffffffff)); + x17 = (x6 & UINT64_C(0x3ffffffffffffff)); + x18 = (x7 & UINT64_C(0x3ffffffffffffff)); + x19 = (x8 & UINT64_C(0x3ffffffffffffff)); + x20 = (x9 & UINT64_C(0x1ffffffffffffff)); + out1[0] = x12; + out1[1] = x13; + out1[2] = x14; + out1[3] = x15; + out1[4] = x16; + out1[5] = x17; + out1[6] = x18; + out1[7] = x19; + out1[8] = x20; } /* * The function fiat_secp521r1_selectznz is a multi-limb conditional select. + * * Postconditions: * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) * @@ -1013,16 +1034,16 @@ fiat_secp521r1_selectznz(uint64_t out1[9], /* * The function fiat_secp521r1_to_bytes serializes a field element to bytes in little-endian order. + * * Postconditions: * out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..65] * - * Input Bounds: - * arg1: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]] * Output Bounds: * out1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x1]] */ static void -fiat_secp521r1_to_bytes(uint8_t out1[66], const uint64_t arg1[9]) +fiat_secp521r1_to_bytes( + uint8_t out1[66], const fiat_secp521r1_tight_field_element arg1) { uint64_t x1; fiat_secp521r1_uint1 x2; @@ -1444,16 +1465,15 @@ fiat_secp521r1_to_bytes(uint8_t out1[66], const uint64_t arg1[9]) /* * The function fiat_secp521r1_from_bytes deserializes a field element from bytes in little-endian order. + * * Postconditions: * eval out1 mod m = bytes_eval arg1 mod m * * Input Bounds: * arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x1]] - * Output Bounds: - * out1: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]] */ static void -fiat_secp521r1_from_bytes(uint64_t out1[9], +fiat_secp521r1_from_bytes(fiat_secp521r1_tight_field_element out1, const uint8_t arg1[66]) { uint64_t x1; @@ -1751,67 +1771,7 @@ fiat_secp521r1_from_bytes(uint64_t out1[9], /* END verbatim fiat code */ -/*- - * Finite field inversion via FLT. - * NB: this is not a real Fiat function, just named that way for consistency. - * Autogenerated: ecp/secp521r1/fe_inv.op3 - * custom repunit addition chain - */ -static void -fiat_secp521r1_inv(fe_t output, const fe_t t1) -{ - int i; - /* temporary variables */ - fe_t acc, t128, t16, t2, t256, t32, t4, t512, t516, t518, t519, t64, t8; - - fiat_secp521r1_carry_square(acc, t1); - fiat_secp521r1_carry_mul(t2, acc, t1); - fiat_secp521r1_carry_square(acc, t2); - fiat_secp521r1_carry_square(acc, acc); - fiat_secp521r1_carry_mul(t4, acc, t2); - fiat_secp521r1_carry_square(acc, t4); - for (i = 0; i < 3; i++) - fiat_secp521r1_carry_square(acc, acc); - fiat_secp521r1_carry_mul(t8, acc, t4); - fiat_secp521r1_carry_square(acc, t8); - for (i = 0; i < 7; i++) - fiat_secp521r1_carry_square(acc, acc); - fiat_secp521r1_carry_mul(t16, acc, t8); - fiat_secp521r1_carry_square(acc, t16); - for (i = 0; i < 15; i++) - fiat_secp521r1_carry_square(acc, acc); - fiat_secp521r1_carry_mul(t32, acc, t16); - fiat_secp521r1_carry_square(acc, t32); - for (i = 0; i < 31; i++) - fiat_secp521r1_carry_square(acc, acc); - fiat_secp521r1_carry_mul(t64, acc, t32); - fiat_secp521r1_carry_square(acc, t64); - for (i = 0; i < 63; i++) - fiat_secp521r1_carry_square(acc, acc); - fiat_secp521r1_carry_mul(t128, acc, t64); - fiat_secp521r1_carry_square(acc, t128); - for (i = 0; i < 127; i++) - fiat_secp521r1_carry_square(acc, acc); - fiat_secp521r1_carry_mul(t256, acc, t128); - fiat_secp521r1_carry_square(acc, t256); - for (i = 0; i < 255; i++) - fiat_secp521r1_carry_square(acc, acc); - fiat_secp521r1_carry_mul(t512, acc, t256); - fiat_secp521r1_carry_square(acc, t512); - for (i = 0; i < 3; i++) - fiat_secp521r1_carry_square(acc, acc); - fiat_secp521r1_carry_mul(t516, acc, t4); - fiat_secp521r1_carry_square(acc, t516); - fiat_secp521r1_carry_square(acc, acc); - fiat_secp521r1_carry_mul(t518, acc, t2); - fiat_secp521r1_carry_square(acc, t518); - fiat_secp521r1_carry_mul(t519, acc, t1); - fiat_secp521r1_carry_square(acc, t519); - fiat_secp521r1_carry_square(acc, acc); - fiat_secp521r1_carry_mul(output, acc, t1); -} - -/* curve coefficient constants */ +/* curve-related constants */ static const limb_t const_one[9] = { UINT64_C(0x0000000000000001), UINT64_C(0x0000000000000000), @@ -3940,6 +3900,67 @@ static const pt_aff_t lut_cmb[13][16] = { }; /*- + * Finite field inversion. + * Computed with exponentiation via FLT. + * Autogenerated: ecp/secp521r1/fe_inv.op3 + * custom repunit addition chain + * NB: this is not a real fiat-crypto function, just named that way for consistency. + */ +static void +fiat_secp521r1_inv(fe_t output, const fe_t t1) +{ + int i; + /* temporary variables */ + fe_t acc, t128, t16, t2, t256, t32, t4, t512, t516, t518, t519, t64, t8; + + fiat_secp521r1_carry_square(acc, t1); + fiat_secp521r1_carry_mul(t2, acc, t1); + fiat_secp521r1_carry_square(acc, t2); + fiat_secp521r1_carry_square(acc, acc); + fiat_secp521r1_carry_mul(t4, acc, t2); + fiat_secp521r1_carry_square(acc, t4); + for (i = 0; i < 3; i++) + fiat_secp521r1_carry_square(acc, acc); + fiat_secp521r1_carry_mul(t8, acc, t4); + fiat_secp521r1_carry_square(acc, t8); + for (i = 0; i < 7; i++) + fiat_secp521r1_carry_square(acc, acc); + fiat_secp521r1_carry_mul(t16, acc, t8); + fiat_secp521r1_carry_square(acc, t16); + for (i = 0; i < 15; i++) + fiat_secp521r1_carry_square(acc, acc); + fiat_secp521r1_carry_mul(t32, acc, t16); + fiat_secp521r1_carry_square(acc, t32); + for (i = 0; i < 31; i++) + fiat_secp521r1_carry_square(acc, acc); + fiat_secp521r1_carry_mul(t64, acc, t32); + fiat_secp521r1_carry_square(acc, t64); + for (i = 0; i < 63; i++) + fiat_secp521r1_carry_square(acc, acc); + fiat_secp521r1_carry_mul(t128, acc, t64); + fiat_secp521r1_carry_square(acc, t128); + for (i = 0; i < 127; i++) + fiat_secp521r1_carry_square(acc, acc); + fiat_secp521r1_carry_mul(t256, acc, t128); + fiat_secp521r1_carry_square(acc, t256); + for (i = 0; i < 255; i++) + fiat_secp521r1_carry_square(acc, acc); + fiat_secp521r1_carry_mul(t512, acc, t256); + fiat_secp521r1_carry_square(acc, t512); + for (i = 0; i < 3; i++) + fiat_secp521r1_carry_square(acc, acc); + fiat_secp521r1_carry_mul(t516, acc, t4); + fiat_secp521r1_carry_square(acc, t516); + fiat_secp521r1_carry_square(acc, acc); + fiat_secp521r1_carry_mul(t518, acc, t2); + fiat_secp521r1_carry_square(acc, t518); + fiat_secp521r1_carry_mul(t519, acc, t1); + fiat_secp521r1_carry_square(acc, t519); + fiat_secp521r1_carry_square(acc, acc); + fiat_secp521r1_carry_mul(output, acc, t1); +} + +/*- * Q := 2P, both projective, Q and P same pointers OK * Autogenerated: op3/dbl_proj.op3 * https://eprint.iacr.org/2015/1060 Alg 6 @@ -4000,7 +4021,7 @@ point_double(pt_prj_t *Q, const pt_prj_t *P) /*- * out1 = (arg1 == 0) ? 0 : nz * NB: this is not a "mod p equiv" 0, but literal 0 - * NB: this is not a real Fiat function, just named that way for consistency. + * NB: this is not a real fiat-crypto function, just named that way for consistency. */ static void fiat_secp521r1_nonzero(limb_t *out1, const fe_t arg1) @@ -4261,7 +4282,7 @@ var_smul_wnaf_two(pt_aff_t *out, const unsigned char a[66], int i, d, is_neg, is_inf = 1, flipped = 0; int8_t anaf[529] = { 0 }; int8_t bnaf[529] = { 0 }; - pt_prj_t Q = { { 0 } }; + pt_prj_t Q = { { 0 }, { 0 }, { 0 } }; pt_prj_t precomp[DRADIX / 2]; precomp_wnaf(precomp, P); @@ -4273,7 +4294,7 @@ var_smul_wnaf_two(pt_aff_t *out, const unsigned char a[66], point_double(&Q, &Q); if ((d = bnaf[i])) { if ((is_neg = d < 0) != flipped) { - fiat_secp521r1_opp(Q.Y, Q.Y); + fiat_secp521r1_carry_opp(Q.Y, Q.Y); flipped ^= 1; } d = (is_neg) ? (-d - 1) >> 1 : (d - 1) >> 1; @@ -4288,7 +4309,7 @@ var_smul_wnaf_two(pt_aff_t *out, const unsigned char a[66], } if ((d = anaf[i])) { if ((is_neg = d < 0) != flipped) { - fiat_secp521r1_opp(Q.Y, Q.Y); + fiat_secp521r1_carry_opp(Q.Y, Q.Y); flipped ^= 1; } d = (is_neg) ? (-d - 1) >> 1 : (d - 1) >> 1; @@ -4312,7 +4333,7 @@ var_smul_wnaf_two(pt_aff_t *out, const unsigned char a[66], if (flipped) { /* correct sign */ - fiat_secp521r1_opp(Q.Y, Q.Y); + fiat_secp521r1_carry_opp(Q.Y, Q.Y); } /* convert to affine -- NB depends on coordinate system */ @@ -4323,6 +4344,8 @@ var_smul_wnaf_two(pt_aff_t *out, const unsigned char a[66], /*- * Variable point scalar multiplication with "regular" wnaf. + * Here "regular" means _no zeroes_, so the sequence of + * EC arithmetic ops is fixed. */ static void var_smul_rwnaf(pt_aff_t *out, const unsigned char scalar[66], @@ -4330,14 +4353,14 @@ var_smul_rwnaf(pt_aff_t *out, const unsigned char scalar[66], { int i, j, d, diff, is_neg; int8_t rnaf[106] = { 0 }; - pt_prj_t Q = { { 0 } }, lut = { { 0 } }; + pt_prj_t Q = { { 0 }, { 0 }, { 0 } }, lut = { { 0 }, { 0 }, { 0 } }; pt_prj_t precomp[DRADIX / 2]; precomp_wnaf(precomp, P); scalar_rwnaf(rnaf, scalar); #if defined(_MSC_VER) -/* result still unsigned: yes we know */ + /* result still unsigned: yes we know */ #pragma warning(push) #pragma warning(disable : 4146) #endif @@ -4367,7 +4390,7 @@ var_smul_rwnaf(pt_aff_t *out, const unsigned char scalar[66], fiat_secp521r1_selectznz(lut.Z, diff, lut.Z, precomp[j].Z); } /* negate lut point if digit is negative */ - fiat_secp521r1_opp(out->Y, lut.Y); + fiat_secp521r1_carry_opp(out->Y, lut.Y); fiat_secp521r1_selectznz(lut.Y, is_neg, lut.Y, out->Y); point_add_proj(&Q, &Q, &lut); } @@ -4378,7 +4401,7 @@ var_smul_rwnaf(pt_aff_t *out, const unsigned char scalar[66], /* conditionally subtract P if the scalar was even */ fe_copy(lut.X, precomp[0].X); - fiat_secp521r1_opp(lut.Y, precomp[0].Y); + fiat_secp521r1_carry_opp(lut.Y, precomp[0].Y); fe_copy(lut.Z, precomp[0].Z); point_add_proj(&lut, &lut, &Q); fiat_secp521r1_selectznz(Q.X, scalar[0] & 1, lut.X, Q.X); @@ -4399,8 +4422,8 @@ fixed_smul_cmb(pt_aff_t *out, const unsigned char scalar[66]) { int i, j, k, d, diff, is_neg = 0; int8_t rnaf[106] = { 0 }; - pt_prj_t Q = { { 0 } }, R = { { 0 } }; - pt_aff_t lut = { { 0 } }; + pt_prj_t Q = { { 0 }, { 0 }, { 0 } }, R = { { 0 }, { 0 }, { 0 } }; + pt_aff_t lut = { { 0 }, { 0 } }; scalar_rwnaf(rnaf, scalar); @@ -4410,7 +4433,7 @@ fixed_smul_cmb(pt_aff_t *out, const unsigned char scalar[66]) fe_set_zero(Q.Z); #if defined(_MSC_VER) -/* result still unsigned: yes we know */ + /* result still unsigned: yes we know */ #pragma warning(push) #pragma warning(disable : 4146) #endif @@ -4433,7 +4456,7 @@ fixed_smul_cmb(pt_aff_t *out, const unsigned char scalar[66]) fiat_secp521r1_selectznz(lut.Y, diff, lut.Y, lut_cmb[j][k].Y); } /* negate lut point if digit is negative */ - fiat_secp521r1_opp(out->Y, lut.Y); + fiat_secp521r1_carry_opp(out->Y, lut.Y); fiat_secp521r1_selectznz(lut.Y, is_neg, lut.Y, out->Y); point_add_mixed(&Q, &Q, &lut); } @@ -4445,7 +4468,7 @@ fixed_smul_cmb(pt_aff_t *out, const unsigned char scalar[66]) /* conditionally subtract P if the scalar was even */ fe_copy(lut.X, lut_cmb[0][0].X); - fiat_secp521r1_opp(lut.Y, lut_cmb[0][0].Y); + fiat_secp521r1_carry_opp(lut.Y, lut_cmb[0][0].Y); point_add_mixed(&R, &Q, &lut); fiat_secp521r1_selectznz(Q.X, scalar[0] & 1, R.X, Q.X); fiat_secp521r1_selectznz(Q.Y, scalar[0] & 1, R.Y, Q.Y); @@ -4464,10 +4487,11 @@ fixed_smul_cmb(pt_aff_t *out, const unsigned char scalar[66]) * Everything is LE byte ordering. */ static void -point_mul_two(unsigned char outx[66], unsigned char outy[66], - const unsigned char a[66], const unsigned char b[66], - const unsigned char inx[66], - const unsigned char iny[66]) +point_mul_two_secp521r1(unsigned char outx[66], unsigned char outy[66], + const unsigned char a[66], + const unsigned char b[66], + const unsigned char inx[66], + const unsigned char iny[66]) { pt_aff_t P; @@ -4486,8 +4510,8 @@ point_mul_two(unsigned char outx[66], unsigned char outy[66], * Everything is LE byte ordering. */ static void -point_mul_g(unsigned char outx[66], unsigned char outy[66], - const unsigned char scalar[66]) +point_mul_g_secp521r1(unsigned char outx[66], unsigned char outy[66], + const unsigned char scalar[66]) { pt_aff_t P; @@ -4504,10 +4528,10 @@ point_mul_g(unsigned char outx[66], unsigned char outy[66], * Everything is LE byte ordering. */ static void -point_mul(unsigned char outx[66], unsigned char outy[66], - const unsigned char scalar[66], - const unsigned char inx[66], - const unsigned char iny[66]) +point_mul_secp521r1(unsigned char outx[66], unsigned char outy[66], + const unsigned char scalar[66], + const unsigned char inx[66], + const unsigned char iny[66]) { pt_aff_t P; @@ -4632,8 +4656,8 @@ point_mul(unsigned char outx[66], unsigned char outy[66], } while (0) static mp_err -point_mul_g_secp521r1(const mp_int *n, mp_int *out_x, - mp_int *out_y, const ECGroup *group) +point_mul_g_secp521r1_wrap(const mp_int *n, mp_int *out_x, + mp_int *out_y, const ECGroup *group) { unsigned char b_x[66]; unsigned char b_y[66]; @@ -4648,7 +4672,7 @@ point_mul_g_secp521r1(const mp_int *n, mp_int *out_x, MP_CHECKOK(mp_to_fixlen_octets(n, b_n, 66)); MP_BE2LE(b_n); - point_mul_g(b_x, b_y, b_n); + point_mul_g_secp521r1(b_x, b_y, b_n); MP_BE2LE(b_x); MP_BE2LE(b_y); MP_CHECKOK(mp_read_unsigned_octets(out_x, b_x, 66)); @@ -4659,9 +4683,9 @@ CLEANUP: } static mp_err -point_mul_secp521r1(const mp_int *n, const mp_int *in_x, - const mp_int *in_y, mp_int *out_x, - mp_int *out_y, const ECGroup *group) +point_mul_secp521r1_wrap(const mp_int *n, const mp_int *in_x, + const mp_int *in_y, mp_int *out_x, + mp_int *out_y, const ECGroup *group) { unsigned char b_x[66]; unsigned char b_y[66]; @@ -4682,7 +4706,7 @@ point_mul_secp521r1(const mp_int *n, const mp_int *in_x, MP_BE2LE(b_x); MP_BE2LE(b_y); MP_BE2LE(b_n); - point_mul(b_x, b_y, b_n, b_x, b_y); + point_mul_secp521r1(b_x, b_y, b_n, b_x, b_y); MP_BE2LE(b_x); MP_BE2LE(b_y); MP_CHECKOK(mp_read_unsigned_octets(out_x, b_x, 66)); @@ -4693,10 +4717,11 @@ CLEANUP: } static mp_err -point_mul_two_secp521r1(const mp_int *n1, const mp_int *n2, - const mp_int *in_x, const mp_int *in_y, - mp_int *out_x, mp_int *out_y, - const ECGroup *group) +point_mul_two_secp521r1_wrap(const mp_int *n1, const mp_int *n2, + const mp_int *in_x, + const mp_int *in_y, mp_int *out_x, + mp_int *out_y, + const ECGroup *group) { unsigned char b_x[66]; unsigned char b_y[66]; @@ -4706,11 +4731,11 @@ point_mul_two_secp521r1(const mp_int *n1, const mp_int *n2, /* If n2 == NULL or 0, this is just a base-point multiplication. */ if (n2 == NULL || mp_cmp_z(n2) == MP_EQ) - return point_mul_g_secp521r1(n1, out_x, out_y, group); + return point_mul_g_secp521r1_wrap(n1, out_x, out_y, group); /* If n1 == NULL or 0, this is just an arbitary-point multiplication. */ if (n1 == NULL || mp_cmp_z(n1) == MP_EQ) - return point_mul_secp521r1(n2, in_x, in_y, out_x, out_y, group); + return point_mul_secp521r1_wrap(n2, in_x, in_y, out_x, out_y, group); ARGCHK(in_x != NULL && in_y != NULL && out_x != NULL && out_y != NULL, MP_BADARG); @@ -4728,7 +4753,7 @@ point_mul_two_secp521r1(const mp_int *n1, const mp_int *n2, MP_BE2LE(b_y); MP_BE2LE(b_n1); MP_BE2LE(b_n2); - point_mul_two(b_x, b_y, b_n1, b_n2, b_x, b_y); + point_mul_two_secp521r1(b_x, b_y, b_n1, b_n2, b_x, b_y); MP_BE2LE(b_x); MP_BE2LE(b_y); MP_CHECKOK(mp_read_unsigned_octets(out_x, b_x, 66)); @@ -4742,9 +4767,9 @@ mp_err ec_group_set_secp521r1(ECGroup *group, ECCurveName name) { if (name == ECCurve_NIST_P521) { - group->base_point_mul = &point_mul_g_secp521r1; - group->point_mul = &point_mul_secp521r1; - group->points_mul = &point_mul_two_secp521r1; + group->base_point_mul = &point_mul_g_secp521r1_wrap; + group->point_mul = &point_mul_secp521r1_wrap; + group->points_mul = &point_mul_two_secp521r1_wrap; } return MP_OKAY; } @@ -4762,13 +4787,6 @@ typedef uint32_t limb_t; #define fe_copy(d, s) memcpy(d, s, sizeof(fe_t)) #define fe_set_zero(d) memset(d, 0, sizeof(fe_t)) -#define fiat_secp521r1_carry_add(c, a, b) \ - fiat_secp521r1_add(c, a, b); \ - fiat_secp521r1_carry(c, c) -#define fiat_secp521r1_carry_sub(c, a, b) \ - fiat_secp521r1_sub(c, a, b); \ - fiat_secp521r1_carry(c, c) - /* Projective points */ typedef struct { fe_t X; @@ -4817,14 +4835,27 @@ typedef struct { /* tight_bounds_multiplier = 1 (from "") */ /* */ /* Computed values: */ -/* carry_chain = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 0, 1] */ -/* eval z = z[0] + (z[1] << 28) + (z[2] << 55) + (z[3] << 83) + (z[4] << 110) + (z[5] << 138) + (z[6] << 165) + (z[7] << 192) + (z[8] << 220) + (z[9] << 247) + (z[10] << 0x113) + (z[11] << 0x12e) + (z[12] << 0x14a) + (z[13] << 0x165) + (z[14] << 0x180) + (z[15] << 0x19c) + (z[16] << 0x1b7) + (z[17] << 0x1d3) + (z[18] << 0x1ee) */ -/* bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) + (z[32] << 256) + (z[33] << 0x108) + (z[34] << 0x110) + (z[35] << 0x118) + (z[36] << 0x120) + (z[37] << 0x128) + (z[38] << 0x130) + (z[39] << 0x138) + (z[40] << 0x140) + (z[41] << 0x148) + (z[42] << 0x150) + (z[43] << 0x158) + (z[44] << 0x160) + (z[45] << 0x168) + (z[46] << 0x170) + (z[47] << 0x178) + (z[48] << 0x180) + (z[49] << 0x188) + (z[50] << 0x190) + (z[51] << 0x198) + (z[52] << 0x1a0) + (z[53] << 0x1a8) + (z[54] << 0x1b0) + (z[55] << 0x1b8) + (z[56] << 0x1c0) + (z[57] << 0x1c8) + (z[58] << 0x1d0) + (z[59] << 0x1d8) + (z[60] << 0x1e0) + (z[61] << 0x1e8) + (z[62] << 0x1f0) + (z[63] << 0x1f8) + (z[64] << 2^9) + (z[65] << 0x208) */ -/* balance = [0x1ffffffe, 0xffffffe, 0x1ffffffe, 0xffffffe, 0x1ffffffe, 0xffffffe, 0xffffffe, 0x1ffffffe, 0xffffffe, 0x1ffffffe, 0xffffffe, 0x1ffffffe, 0xffffffe, 0xffffffe, 0x1ffffffe, 0xffffffe, 0x1ffffffe, 0xffffffe, 0xffffffe] */ +/* carry_chain = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 0, 1] */ +/* eval z = z[0] + (z[1] << 28) + (z[2] << 55) + (z[3] << 83) + (z[4] << 110) + (z[5] << 138) + (z[6] << 165) + (z[7] << 192) + (z[8] << 220) + (z[9] << 247) + (z[10] << 0x113) + (z[11] << 0x12e) + (z[12] << 0x14a) + (z[13] << 0x165) + (z[14] << 0x180) + (z[15] << 0x19c) + (z[16] << 0x1b7) + (z[17] << 0x1d3) + (z[18] << 0x1ee) */ +/* bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) + (z[32] << 256) + (z[33] << 0x108) + (z[34] << 0x110) + (z[35] << 0x118) + (z[36] << 0x120) + (z[37] << 0x128) + (z[38] << 0x130) + (z[39] << 0x138) + (z[40] << 0x140) + (z[41] << 0x148) + (z[42] << 0x150) + (z[43] << 0x158) + (z[44] << 0x160) + (z[45] << 0x168) + (z[46] << 0x170) + (z[47] << 0x178) + (z[48] << 0x180) + (z[49] << 0x188) + (z[50] << 0x190) + (z[51] << 0x198) + (z[52] << 0x1a0) + (z[53] << 0x1a8) + (z[54] << 0x1b0) + (z[55] << 0x1b8) + (z[56] << 0x1c0) + (z[57] << 0x1c8) + (z[58] << 0x1d0) + (z[59] << 0x1d8) + (z[60] << 0x1e0) + (z[61] << 0x1e8) + (z[62] << 0x1f0) + (z[63] << 0x1f8) + (z[64] << 2^9) + (z[65] << 0x208) */ +/* balance = [0x1ffffffe, 0xffffffe, 0x1ffffffe, 0xffffffe, 0x1ffffffe, 0xffffffe, 0xffffffe, 0x1ffffffe, 0xffffffe, 0x1ffffffe, 0xffffffe, 0x1ffffffe, 0xffffffe, 0xffffffe, 0x1ffffffe, 0xffffffe, 0x1ffffffe, 0xffffffe, 0xffffffe] */ #include <stdint.h> typedef unsigned char fiat_secp521r1_uint1; typedef signed char fiat_secp521r1_int1; +#ifdef __GNUC__ +#define FIAT_SECP521R1_FIAT_INLINE __inline__ +#else +#define FIAT_SECP521R1_FIAT_INLINE +#endif + +/* The type fiat_secp521r1_loose_field_element is a field element with loose bounds. */ +/* Bounds: [[0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000]] */ +typedef uint32_t fiat_secp521r1_loose_field_element[19]; + +/* The type fiat_secp521r1_tight_field_element is a field element with tight bounds. */ +/* Bounds: [[0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000]] */ +typedef uint32_t fiat_secp521r1_tight_field_element[19]; #if (-1 & 3) != 3 #error "This code only works on a two's complement system" @@ -4845,6 +4876,7 @@ fiat_secp521r1_value_barrier_u32(uint32_t a) /* * The function fiat_secp521r1_addcarryx_u28 is an addition with carry. + * * Postconditions: * out1 = (arg1 + arg2 + arg3) mod 2^28 * out2 = ⌊(arg1 + arg2 + arg3) / 2^28⌋ @@ -4875,6 +4907,7 @@ fiat_secp521r1_addcarryx_u28(uint32_t *out1, /* * The function fiat_secp521r1_subborrowx_u28 is a subtraction with borrow. + * * Postconditions: * out1 = (-arg1 + arg2 + -arg3) mod 2^28 * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^28⌋ @@ -4905,6 +4938,7 @@ fiat_secp521r1_subborrowx_u28(uint32_t *out1, /* * The function fiat_secp521r1_addcarryx_u27 is an addition with carry. + * * Postconditions: * out1 = (arg1 + arg2 + arg3) mod 2^27 * out2 = ⌊(arg1 + arg2 + arg3) / 2^27⌋ @@ -4935,6 +4969,7 @@ fiat_secp521r1_addcarryx_u27(uint32_t *out1, /* * The function fiat_secp521r1_subborrowx_u27 is a subtraction with borrow. + * * Postconditions: * out1 = (-arg1 + arg2 + -arg3) mod 2^27 * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^27⌋ @@ -4965,6 +5000,7 @@ fiat_secp521r1_subborrowx_u27(uint32_t *out1, /* * The function fiat_secp521r1_cmovznz_u32 is a single-word conditional move. + * * Postconditions: * out1 = (if arg1 = 0 then arg2 else arg3) * @@ -4992,18 +5028,16 @@ fiat_secp521r1_cmovznz_u32(uint32_t *out1, /* * The function fiat_secp521r1_carry_mul multiplies two field elements and reduces the result. + * * Postconditions: * eval out1 mod m = (eval arg1 * eval arg2) mod m * - * Input Bounds: - * arg1: [[0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000]] - * arg2: [[0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000]] - * Output Bounds: - * out1: [[0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000]] */ static void -fiat_secp521r1_carry_mul(uint32_t out1[19], const uint32_t arg1[19], - const uint32_t arg2[19]) +fiat_secp521r1_carry_mul( + fiat_secp521r1_tight_field_element out1, + const fiat_secp521r1_loose_field_element arg1, + const fiat_secp521r1_loose_field_element arg2) { uint64_t x1; uint64_t x2; @@ -6176,17 +6210,15 @@ fiat_secp521r1_carry_mul(uint32_t out1[19], const uint32_t arg1[19], /* * The function fiat_secp521r1_carry_square squares a field element and reduces the result. + * * Postconditions: * eval out1 mod m = (eval arg1 * eval arg1) mod m * - * Input Bounds: - * arg1: [[0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000]] - * Output Bounds: - * out1: [[0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000]] */ static void -fiat_secp521r1_carry_square(uint32_t out1[19], - const uint32_t arg1[19]) +fiat_secp521r1_carry_square( + fiat_secp521r1_tight_field_element out1, + const fiat_secp521r1_loose_field_element arg1) { uint32_t x1; uint32_t x2; @@ -6870,17 +6902,17 @@ fiat_secp521r1_carry_square(uint32_t out1[19], } /* - * The function fiat_secp521r1_carry reduces a field element. + * The function fiat_secp521r1_carry_add adds two field elements. + * * Postconditions: - * eval out1 mod m = eval arg1 mod m + * eval out1 mod m = (eval arg1 + eval arg2) mod m * - * Input Bounds: - * arg1: [[0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000]] - * Output Bounds: - * out1: [[0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000]] */ static void -fiat_secp521r1_carry(uint32_t out1[19], const uint32_t arg1[19]) +fiat_secp521r1_carry_add( + fiat_secp521r1_tight_field_element out1, + const fiat_secp521r1_tight_field_element arg1, + const fiat_secp521r1_tight_field_element arg2) { uint32_t x1; uint32_t x2; @@ -6922,25 +6954,25 @@ fiat_secp521r1_carry(uint32_t out1[19], const uint32_t arg1[19]) uint32_t x38; uint32_t x39; uint32_t x40; - x1 = (arg1[0]); - x2 = ((x1 >> 28) + (arg1[1])); - x3 = ((x2 >> 27) + (arg1[2])); - x4 = ((x3 >> 28) + (arg1[3])); - x5 = ((x4 >> 27) + (arg1[4])); - x6 = ((x5 >> 28) + (arg1[5])); - x7 = ((x6 >> 27) + (arg1[6])); - x8 = ((x7 >> 27) + (arg1[7])); - x9 = ((x8 >> 28) + (arg1[8])); - x10 = ((x9 >> 27) + (arg1[9])); - x11 = ((x10 >> 28) + (arg1[10])); - x12 = ((x11 >> 27) + (arg1[11])); - x13 = ((x12 >> 28) + (arg1[12])); - x14 = ((x13 >> 27) + (arg1[13])); - x15 = ((x14 >> 27) + (arg1[14])); - x16 = ((x15 >> 28) + (arg1[15])); - x17 = ((x16 >> 27) + (arg1[16])); - x18 = ((x17 >> 28) + (arg1[17])); - x19 = ((x18 >> 27) + (arg1[18])); + x1 = ((arg1[0]) + (arg2[0])); + x2 = ((x1 >> 28) + ((arg1[1]) + (arg2[1]))); + x3 = ((x2 >> 27) + ((arg1[2]) + (arg2[2]))); + x4 = ((x3 >> 28) + ((arg1[3]) + (arg2[3]))); + x5 = ((x4 >> 27) + ((arg1[4]) + (arg2[4]))); + x6 = ((x5 >> 28) + ((arg1[5]) + (arg2[5]))); + x7 = ((x6 >> 27) + ((arg1[6]) + (arg2[6]))); + x8 = ((x7 >> 27) + ((arg1[7]) + (arg2[7]))); + x9 = ((x8 >> 28) + ((arg1[8]) + (arg2[8]))); + x10 = ((x9 >> 27) + ((arg1[9]) + (arg2[9]))); + x11 = ((x10 >> 28) + ((arg1[10]) + (arg2[10]))); + x12 = ((x11 >> 27) + ((arg1[11]) + (arg2[11]))); + x13 = ((x12 >> 28) + ((arg1[12]) + (arg2[12]))); + x14 = ((x13 >> 27) + ((arg1[13]) + (arg2[13]))); + x15 = ((x14 >> 27) + ((arg1[14]) + (arg2[14]))); + x16 = ((x15 >> 28) + ((arg1[15]) + (arg2[15]))); + x17 = ((x16 >> 27) + ((arg1[16]) + (arg2[16]))); + x18 = ((x17 >> 28) + ((arg1[17]) + (arg2[17]))); + x19 = ((x18 >> 27) + ((arg1[18]) + (arg2[18]))); x20 = ((x1 & UINT32_C(0xfffffff)) + (x19 >> 27)); x21 = ((fiat_secp521r1_uint1)(x20 >> 28) + (x2 & UINT32_C(0x7ffffff))); x22 = (x20 & UINT32_C(0xfffffff)); @@ -6984,93 +7016,17 @@ fiat_secp521r1_carry(uint32_t out1[19], const uint32_t arg1[19]) } /* - * The function fiat_secp521r1_add adds two field elements. - * Postconditions: - * eval out1 mod m = (eval arg1 + eval arg2) mod m + * The function fiat_secp521r1_carry_sub subtracts two field elements. * - * Input Bounds: - * arg1: [[0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000]] - * arg2: [[0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000]] - * Output Bounds: - * out1: [[0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000]] - */ -static void -fiat_secp521r1_add(uint32_t out1[19], const uint32_t arg1[19], - const uint32_t arg2[19]) -{ - uint32_t x1; - uint32_t x2; - uint32_t x3; - uint32_t x4; - uint32_t x5; - uint32_t x6; - uint32_t x7; - uint32_t x8; - uint32_t x9; - uint32_t x10; - uint32_t x11; - uint32_t x12; - uint32_t x13; - uint32_t x14; - uint32_t x15; - uint32_t x16; - uint32_t x17; - uint32_t x18; - uint32_t x19; - x1 = ((arg1[0]) + (arg2[0])); - x2 = ((arg1[1]) + (arg2[1])); - x3 = ((arg1[2]) + (arg2[2])); - x4 = ((arg1[3]) + (arg2[3])); - x5 = ((arg1[4]) + (arg2[4])); - x6 = ((arg1[5]) + (arg2[5])); - x7 = ((arg1[6]) + (arg2[6])); - x8 = ((arg1[7]) + (arg2[7])); - x9 = ((arg1[8]) + (arg2[8])); - x10 = ((arg1[9]) + (arg2[9])); - x11 = ((arg1[10]) + (arg2[10])); - x12 = ((arg1[11]) + (arg2[11])); - x13 = ((arg1[12]) + (arg2[12])); - x14 = ((arg1[13]) + (arg2[13])); - x15 = ((arg1[14]) + (arg2[14])); - x16 = ((arg1[15]) + (arg2[15])); - x17 = ((arg1[16]) + (arg2[16])); - x18 = ((arg1[17]) + (arg2[17])); - x19 = ((arg1[18]) + (arg2[18])); - out1[0] = x1; - out1[1] = x2; - out1[2] = x3; - out1[3] = x4; - out1[4] = x5; - out1[5] = x6; - out1[6] = x7; - out1[7] = x8; - out1[8] = x9; - out1[9] = x10; - out1[10] = x11; - out1[11] = x12; - out1[12] = x13; - out1[13] = x14; - out1[14] = x15; - out1[15] = x16; - out1[16] = x17; - out1[17] = x18; - out1[18] = x19; -} - -/* - * The function fiat_secp521r1_sub subtracts two field elements. * Postconditions: * eval out1 mod m = (eval arg1 - eval arg2) mod m * - * Input Bounds: - * arg1: [[0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000]] - * arg2: [[0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000]] - * Output Bounds: - * out1: [[0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000]] */ static void -fiat_secp521r1_sub(uint32_t out1[19], const uint32_t arg1[19], - const uint32_t arg2[19]) +fiat_secp521r1_carry_sub( + fiat_secp521r1_tight_field_element out1, + const fiat_secp521r1_tight_field_element arg1, + const fiat_secp521r1_tight_field_element arg2) { uint32_t x1; uint32_t x2; @@ -7091,58 +7047,99 @@ fiat_secp521r1_sub(uint32_t out1[19], const uint32_t arg1[19], uint32_t x17; uint32_t x18; uint32_t x19; + uint32_t x20; + uint32_t x21; + uint32_t x22; + uint32_t x23; + uint32_t x24; + uint32_t x25; + uint32_t x26; + uint32_t x27; + uint32_t x28; + uint32_t x29; + uint32_t x30; + uint32_t x31; + uint32_t x32; + uint32_t x33; + uint32_t x34; + uint32_t x35; + uint32_t x36; + uint32_t x37; + uint32_t x38; + uint32_t x39; + uint32_t x40; x1 = ((UINT32_C(0x1ffffffe) + (arg1[0])) - (arg2[0])); - x2 = ((UINT32_C(0xffffffe) + (arg1[1])) - (arg2[1])); - x3 = ((UINT32_C(0x1ffffffe) + (arg1[2])) - (arg2[2])); - x4 = ((UINT32_C(0xffffffe) + (arg1[3])) - (arg2[3])); - x5 = ((UINT32_C(0x1ffffffe) + (arg1[4])) - (arg2[4])); - x6 = ((UINT32_C(0xffffffe) + (arg1[5])) - (arg2[5])); - x7 = ((UINT32_C(0xffffffe) + (arg1[6])) - (arg2[6])); - x8 = ((UINT32_C(0x1ffffffe) + (arg1[7])) - (arg2[7])); - x9 = ((UINT32_C(0xffffffe) + (arg1[8])) - (arg2[8])); - x10 = ((UINT32_C(0x1ffffffe) + (arg1[9])) - (arg2[9])); - x11 = ((UINT32_C(0xffffffe) + (arg1[10])) - (arg2[10])); - x12 = ((UINT32_C(0x1ffffffe) + (arg1[11])) - (arg2[11])); - x13 = ((UINT32_C(0xffffffe) + (arg1[12])) - (arg2[12])); - x14 = ((UINT32_C(0xffffffe) + (arg1[13])) - (arg2[13])); - x15 = ((UINT32_C(0x1ffffffe) + (arg1[14])) - (arg2[14])); - x16 = ((UINT32_C(0xffffffe) + (arg1[15])) - (arg2[15])); - x17 = ((UINT32_C(0x1ffffffe) + (arg1[16])) - (arg2[16])); - x18 = ((UINT32_C(0xffffffe) + (arg1[17])) - (arg2[17])); - x19 = ((UINT32_C(0xffffffe) + (arg1[18])) - (arg2[18])); - out1[0] = x1; - out1[1] = x2; - out1[2] = x3; - out1[3] = x4; - out1[4] = x5; - out1[5] = x6; - out1[6] = x7; - out1[7] = x8; - out1[8] = x9; - out1[9] = x10; - out1[10] = x11; - out1[11] = x12; - out1[12] = x13; - out1[13] = x14; - out1[14] = x15; - out1[15] = x16; - out1[16] = x17; - out1[17] = x18; - out1[18] = x19; + x2 = ((x1 >> 28) + ((UINT32_C(0xffffffe) + (arg1[1])) - (arg2[1]))); + x3 = ((x2 >> 27) + ((UINT32_C(0x1ffffffe) + (arg1[2])) - (arg2[2]))); + x4 = ((x3 >> 28) + ((UINT32_C(0xffffffe) + (arg1[3])) - (arg2[3]))); + x5 = ((x4 >> 27) + ((UINT32_C(0x1ffffffe) + (arg1[4])) - (arg2[4]))); + x6 = ((x5 >> 28) + ((UINT32_C(0xffffffe) + (arg1[5])) - (arg2[5]))); + x7 = ((x6 >> 27) + ((UINT32_C(0xffffffe) + (arg1[6])) - (arg2[6]))); + x8 = ((x7 >> 27) + ((UINT32_C(0x1ffffffe) + (arg1[7])) - (arg2[7]))); + x9 = ((x8 >> 28) + ((UINT32_C(0xffffffe) + (arg1[8])) - (arg2[8]))); + x10 = ((x9 >> 27) + ((UINT32_C(0x1ffffffe) + (arg1[9])) - (arg2[9]))); + x11 = ((x10 >> 28) + ((UINT32_C(0xffffffe) + (arg1[10])) - (arg2[10]))); + x12 = ((x11 >> 27) + ((UINT32_C(0x1ffffffe) + (arg1[11])) - (arg2[11]))); + x13 = ((x12 >> 28) + ((UINT32_C(0xffffffe) + (arg1[12])) - (arg2[12]))); + x14 = ((x13 >> 27) + ((UINT32_C(0xffffffe) + (arg1[13])) - (arg2[13]))); + x15 = ((x14 >> 27) + ((UINT32_C(0x1ffffffe) + (arg1[14])) - (arg2[14]))); + x16 = ((x15 >> 28) + ((UINT32_C(0xffffffe) + (arg1[15])) - (arg2[15]))); + x17 = ((x16 >> 27) + ((UINT32_C(0x1ffffffe) + (arg1[16])) - (arg2[16]))); + x18 = ((x17 >> 28) + ((UINT32_C(0xffffffe) + (arg1[17])) - (arg2[17]))); + x19 = ((x18 >> 27) + ((UINT32_C(0xffffffe) + (arg1[18])) - (arg2[18]))); + x20 = ((x1 & UINT32_C(0xfffffff)) + (x19 >> 27)); + x21 = ((fiat_secp521r1_uint1)(x20 >> 28) + (x2 & UINT32_C(0x7ffffff))); + x22 = (x20 & UINT32_C(0xfffffff)); + x23 = (x21 & UINT32_C(0x7ffffff)); + x24 = ((fiat_secp521r1_uint1)(x21 >> 27) + (x3 & UINT32_C(0xfffffff))); + x25 = (x4 & UINT32_C(0x7ffffff)); + x26 = (x5 & UINT32_C(0xfffffff)); + x27 = (x6 & UINT32_C(0x7ffffff)); + x28 = (x7 & UINT32_C(0x7ffffff)); + x29 = (x8 & UINT32_C(0xfffffff)); + x30 = (x9 & UINT32_C(0x7ffffff)); + x31 = (x10 & UINT32_C(0xfffffff)); + x32 = (x11 & UINT32_C(0x7ffffff)); + x33 = (x12 & UINT32_C(0xfffffff)); + x34 = (x13 & UINT32_C(0x7ffffff)); + x35 = (x14 & UINT32_C(0x7ffffff)); + x36 = (x15 & UINT32_C(0xfffffff)); + x37 = (x16 & UINT32_C(0x7ffffff)); + x38 = (x17 & UINT32_C(0xfffffff)); + x39 = (x18 & UINT32_C(0x7ffffff)); + x40 = (x19 & UINT32_C(0x7ffffff)); + out1[0] = x22; + out1[1] = x23; + out1[2] = x24; + out1[3] = x25; + out1[4] = x26; + out1[5] = x27; + out1[6] = x28; + out1[7] = x29; + out1[8] = x30; + out1[9] = x31; + out1[10] = x32; + out1[11] = x33; + out1[12] = x34; + out1[13] = x35; + out1[14] = x36; + out1[15] = x37; + out1[16] = x38; + out1[17] = x39; + out1[18] = x40; } /* - * The function fiat_secp521r1_opp negates a field element. + * The function fiat_secp521r1_carry_opp negates a field element. + * * Postconditions: * eval out1 mod m = -eval arg1 mod m * - * Input Bounds: - * arg1: [[0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000]] - * Output Bounds: - * out1: [[0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000]] */ static void -fiat_secp521r1_opp(uint32_t out1[19], const uint32_t arg1[19]) +fiat_secp521r1_carry_opp( + fiat_secp521r1_tight_field_element out1, + const fiat_secp521r1_tight_field_element arg1) { uint32_t x1; uint32_t x2; @@ -7163,48 +7160,105 @@ fiat_secp521r1_opp(uint32_t out1[19], const uint32_t arg1[19]) uint32_t x17; uint32_t x18; uint32_t x19; + uint32_t x20; + uint32_t x21; + uint32_t x22; + uint32_t x23; + uint32_t x24; + uint32_t x25; + uint32_t x26; + uint32_t x27; + uint32_t x28; + uint32_t x29; + uint32_t x30; + uint32_t x31; + uint32_t x32; + uint32_t x33; + uint32_t x34; + uint32_t x35; + uint32_t x36; + uint32_t x37; + uint32_t x38; + uint32_t x39; + uint32_t x40; x1 = (UINT32_C(0x1ffffffe) - (arg1[0])); - x2 = (UINT32_C(0xffffffe) - (arg1[1])); - x3 = (UINT32_C(0x1ffffffe) - (arg1[2])); - x4 = (UINT32_C(0xffffffe) - (arg1[3])); - x5 = (UINT32_C(0x1ffffffe) - (arg1[4])); - x6 = (UINT32_C(0xffffffe) - (arg1[5])); - x7 = (UINT32_C(0xffffffe) - (arg1[6])); - x8 = (UINT32_C(0x1ffffffe) - (arg1[7])); - x9 = (UINT32_C(0xffffffe) - (arg1[8])); - x10 = (UINT32_C(0x1ffffffe) - (arg1[9])); - x11 = (UINT32_C(0xffffffe) - (arg1[10])); - x12 = (UINT32_C(0x1ffffffe) - (arg1[11])); - x13 = (UINT32_C(0xffffffe) - (arg1[12])); - x14 = (UINT32_C(0xffffffe) - (arg1[13])); - x15 = (UINT32_C(0x1ffffffe) - (arg1[14])); - x16 = (UINT32_C(0xffffffe) - (arg1[15])); - x17 = (UINT32_C(0x1ffffffe) - (arg1[16])); - x18 = (UINT32_C(0xffffffe) - (arg1[17])); - x19 = (UINT32_C(0xffffffe) - (arg1[18])); - out1[0] = x1; - out1[1] = x2; - out1[2] = x3; - out1[3] = x4; - out1[4] = x5; - out1[5] = x6; - out1[6] = x7; - out1[7] = x8; - out1[8] = x9; - out1[9] = x10; - out1[10] = x11; - out1[11] = x12; - out1[12] = x13; - out1[13] = x14; - out1[14] = x15; - out1[15] = x16; - out1[16] = x17; - out1[17] = x18; - out1[18] = x19; + x2 = ((fiat_secp521r1_uint1)(x1 >> 28) + (UINT32_C(0xffffffe) - (arg1[1]))); + x3 = + ((fiat_secp521r1_uint1)(x2 >> 27) + (UINT32_C(0x1ffffffe) - (arg1[2]))); + x4 = ((fiat_secp521r1_uint1)(x3 >> 28) + (UINT32_C(0xffffffe) - (arg1[3]))); + x5 = + ((fiat_secp521r1_uint1)(x4 >> 27) + (UINT32_C(0x1ffffffe) - (arg1[4]))); + x6 = ((fiat_secp521r1_uint1)(x5 >> 28) + (UINT32_C(0xffffffe) - (arg1[5]))); + x7 = ((fiat_secp521r1_uint1)(x6 >> 27) + (UINT32_C(0xffffffe) - (arg1[6]))); + x8 = + ((fiat_secp521r1_uint1)(x7 >> 27) + (UINT32_C(0x1ffffffe) - (arg1[7]))); + x9 = ((fiat_secp521r1_uint1)(x8 >> 28) + (UINT32_C(0xffffffe) - (arg1[8]))); + x10 = + ((fiat_secp521r1_uint1)(x9 >> 27) + (UINT32_C(0x1ffffffe) - (arg1[9]))); + x11 = ((fiat_secp521r1_uint1)(x10 >> 28) + + (UINT32_C(0xffffffe) - (arg1[10]))); + x12 = ((fiat_secp521r1_uint1)(x11 >> 27) + + (UINT32_C(0x1ffffffe) - (arg1[11]))); + x13 = ((fiat_secp521r1_uint1)(x12 >> 28) + + (UINT32_C(0xffffffe) - (arg1[12]))); + x14 = ((fiat_secp521r1_uint1)(x13 >> 27) + + (UINT32_C(0xffffffe) - (arg1[13]))); + x15 = ((fiat_secp521r1_uint1)(x14 >> 27) + + (UINT32_C(0x1ffffffe) - (arg1[14]))); + x16 = ((fiat_secp521r1_uint1)(x15 >> 28) + + (UINT32_C(0xffffffe) - (arg1[15]))); + x17 = ((fiat_secp521r1_uint1)(x16 >> 27) + + (UINT32_C(0x1ffffffe) - (arg1[16]))); + x18 = ((fiat_secp521r1_uint1)(x17 >> 28) + + (UINT32_C(0xffffffe) - (arg1[17]))); + x19 = ((fiat_secp521r1_uint1)(x18 >> 27) + + (UINT32_C(0xffffffe) - (arg1[18]))); + x20 = ((x1 & UINT32_C(0xfffffff)) + + (uint32_t)(fiat_secp521r1_uint1)(x19 >> 27)); + x21 = ((fiat_secp521r1_uint1)(x20 >> 28) + (x2 & UINT32_C(0x7ffffff))); + x22 = (x20 & UINT32_C(0xfffffff)); + x23 = (x21 & UINT32_C(0x7ffffff)); + x24 = ((fiat_secp521r1_uint1)(x21 >> 27) + (x3 & UINT32_C(0xfffffff))); + x25 = (x4 & UINT32_C(0x7ffffff)); + x26 = (x5 & UINT32_C(0xfffffff)); + x27 = (x6 & UINT32_C(0x7ffffff)); + x28 = (x7 & UINT32_C(0x7ffffff)); + x29 = (x8 & UINT32_C(0xfffffff)); + x30 = (x9 & UINT32_C(0x7ffffff)); + x31 = (x10 & UINT32_C(0xfffffff)); + x32 = (x11 & UINT32_C(0x7ffffff)); + x33 = (x12 & UINT32_C(0xfffffff)); + x34 = (x13 & UINT32_C(0x7ffffff)); + x35 = (x14 & UINT32_C(0x7ffffff)); + x36 = (x15 & UINT32_C(0xfffffff)); + x37 = (x16 & UINT32_C(0x7ffffff)); + x38 = (x17 & UINT32_C(0xfffffff)); + x39 = (x18 & UINT32_C(0x7ffffff)); + x40 = (x19 & UINT32_C(0x7ffffff)); + out1[0] = x22; + out1[1] = x23; + out1[2] = x24; + out1[3] = x25; + out1[4] = x26; + out1[5] = x27; + out1[6] = x28; + out1[7] = x29; + out1[8] = x30; + out1[9] = x31; + out1[10] = x32; + out1[11] = x33; + out1[12] = x34; + out1[13] = x35; + out1[14] = x36; + out1[15] = x37; + out1[16] = x38; + out1[17] = x39; + out1[18] = x40; } /* * The function fiat_secp521r1_selectznz is a multi-limb conditional select. + * * Postconditions: * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3) * @@ -7282,16 +7336,16 @@ fiat_secp521r1_selectznz(uint32_t out1[19], /* * The function fiat_secp521r1_to_bytes serializes a field element to bytes in little-endian order. + * * Postconditions: * out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..65] * - * Input Bounds: - * arg1: [[0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000]] * Output Bounds: * out1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x1]] */ static void -fiat_secp521r1_to_bytes(uint8_t out1[66], const uint32_t arg1[19]) +fiat_secp521r1_to_bytes( + uint8_t out1[66], const fiat_secp521r1_tight_field_element arg1) { uint32_t x1; fiat_secp521r1_uint1 x2; @@ -7830,16 +7884,15 @@ fiat_secp521r1_to_bytes(uint8_t out1[66], const uint32_t arg1[19]) /* * The function fiat_secp521r1_from_bytes deserializes a field element from bytes in little-endian order. + * * Postconditions: * eval out1 mod m = bytes_eval arg1 mod m * * Input Bounds: * arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x1]] - * Output Bounds: - * out1: [[0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000]] */ static void -fiat_secp521r1_from_bytes(uint32_t out1[19], +fiat_secp521r1_from_bytes(fiat_secp521r1_tight_field_element out1, const uint8_t arg1[66]) { uint32_t x1; @@ -8187,67 +8240,7 @@ fiat_secp521r1_from_bytes(uint32_t out1[19], /* END verbatim fiat code */ -/*- - * Finite field inversion via FLT. - * NB: this is not a real Fiat function, just named that way for consistency. - * Autogenerated: ecp/secp521r1/fe_inv.op3 - * custom repunit addition chain - */ -static void -fiat_secp521r1_inv(fe_t output, const fe_t t1) -{ - int i; - /* temporary variables */ - fe_t acc, t128, t16, t2, t256, t32, t4, t512, t516, t518, t519, t64, t8; - - fiat_secp521r1_carry_square(acc, t1); - fiat_secp521r1_carry_mul(t2, acc, t1); - fiat_secp521r1_carry_square(acc, t2); - fiat_secp521r1_carry_square(acc, acc); - fiat_secp521r1_carry_mul(t4, acc, t2); - fiat_secp521r1_carry_square(acc, t4); - for (i = 0; i < 3; i++) - fiat_secp521r1_carry_square(acc, acc); - fiat_secp521r1_carry_mul(t8, acc, t4); - fiat_secp521r1_carry_square(acc, t8); - for (i = 0; i < 7; i++) - fiat_secp521r1_carry_square(acc, acc); - fiat_secp521r1_carry_mul(t16, acc, t8); - fiat_secp521r1_carry_square(acc, t16); - for (i = 0; i < 15; i++) - fiat_secp521r1_carry_square(acc, acc); - fiat_secp521r1_carry_mul(t32, acc, t16); - fiat_secp521r1_carry_square(acc, t32); - for (i = 0; i < 31; i++) - fiat_secp521r1_carry_square(acc, acc); - fiat_secp521r1_carry_mul(t64, acc, t32); - fiat_secp521r1_carry_square(acc, t64); - for (i = 0; i < 63; i++) - fiat_secp521r1_carry_square(acc, acc); - fiat_secp521r1_carry_mul(t128, acc, t64); - fiat_secp521r1_carry_square(acc, t128); - for (i = 0; i < 127; i++) - fiat_secp521r1_carry_square(acc, acc); - fiat_secp521r1_carry_mul(t256, acc, t128); - fiat_secp521r1_carry_square(acc, t256); - for (i = 0; i < 255; i++) - fiat_secp521r1_carry_square(acc, acc); - fiat_secp521r1_carry_mul(t512, acc, t256); - fiat_secp521r1_carry_square(acc, t512); - for (i = 0; i < 3; i++) - fiat_secp521r1_carry_square(acc, acc); - fiat_secp521r1_carry_mul(t516, acc, t4); - fiat_secp521r1_carry_square(acc, t516); - fiat_secp521r1_carry_square(acc, acc); - fiat_secp521r1_carry_mul(t518, acc, t2); - fiat_secp521r1_carry_square(acc, t518); - fiat_secp521r1_carry_mul(t519, acc, t1); - fiat_secp521r1_carry_square(acc, t519); - fiat_secp521r1_carry_square(acc, acc); - fiat_secp521r1_carry_mul(output, acc, t1); -} - -/* curve coefficient constants */ +/* curve-related constants */ static const limb_t const_one[19] = { UINT32_C(0x00000001), UINT32_C(0x00000000), UINT32_C(0x00000000), @@ -11212,6 +11205,67 @@ static const pt_aff_t lut_cmb[13][16] = { }; /*- + * Finite field inversion. + * Computed with exponentiation via FLT. + * Autogenerated: ecp/secp521r1/fe_inv.op3 + * custom repunit addition chain + * NB: this is not a real fiat-crypto function, just named that way for consistency. + */ +static void +fiat_secp521r1_inv(fe_t output, const fe_t t1) +{ + int i; + /* temporary variables */ + fe_t acc, t128, t16, t2, t256, t32, t4, t512, t516, t518, t519, t64, t8; + + fiat_secp521r1_carry_square(acc, t1); + fiat_secp521r1_carry_mul(t2, acc, t1); + fiat_secp521r1_carry_square(acc, t2); + fiat_secp521r1_carry_square(acc, acc); + fiat_secp521r1_carry_mul(t4, acc, t2); + fiat_secp521r1_carry_square(acc, t4); + for (i = 0; i < 3; i++) + fiat_secp521r1_carry_square(acc, acc); + fiat_secp521r1_carry_mul(t8, acc, t4); + fiat_secp521r1_carry_square(acc, t8); + for (i = 0; i < 7; i++) + fiat_secp521r1_carry_square(acc, acc); + fiat_secp521r1_carry_mul(t16, acc, t8); + fiat_secp521r1_carry_square(acc, t16); + for (i = 0; i < 15; i++) + fiat_secp521r1_carry_square(acc, acc); + fiat_secp521r1_carry_mul(t32, acc, t16); + fiat_secp521r1_carry_square(acc, t32); + for (i = 0; i < 31; i++) + fiat_secp521r1_carry_square(acc, acc); + fiat_secp521r1_carry_mul(t64, acc, t32); + fiat_secp521r1_carry_square(acc, t64); + for (i = 0; i < 63; i++) + fiat_secp521r1_carry_square(acc, acc); + fiat_secp521r1_carry_mul(t128, acc, t64); + fiat_secp521r1_carry_square(acc, t128); + for (i = 0; i < 127; i++) + fiat_secp521r1_carry_square(acc, acc); + fiat_secp521r1_carry_mul(t256, acc, t128); + fiat_secp521r1_carry_square(acc, t256); + for (i = 0; i < 255; i++) + fiat_secp521r1_carry_square(acc, acc); + fiat_secp521r1_carry_mul(t512, acc, t256); + fiat_secp521r1_carry_square(acc, t512); + for (i = 0; i < 3; i++) + fiat_secp521r1_carry_square(acc, acc); + fiat_secp521r1_carry_mul(t516, acc, t4); + fiat_secp521r1_carry_square(acc, t516); + fiat_secp521r1_carry_square(acc, acc); + fiat_secp521r1_carry_mul(t518, acc, t2); + fiat_secp521r1_carry_square(acc, t518); + fiat_secp521r1_carry_mul(t519, acc, t1); + fiat_secp521r1_carry_square(acc, t519); + fiat_secp521r1_carry_square(acc, acc); + fiat_secp521r1_carry_mul(output, acc, t1); +} + +/*- * Q := 2P, both projective, Q and P same pointers OK * Autogenerated: op3/dbl_proj.op3 * https://eprint.iacr.org/2015/1060 Alg 6 @@ -11272,7 +11326,7 @@ point_double(pt_prj_t *Q, const pt_prj_t *P) /*- * out1 = (arg1 == 0) ? 0 : nz * NB: this is not a "mod p equiv" 0, but literal 0 - * NB: this is not a real Fiat function, just named that way for consistency. + * NB: this is not a real fiat-crypto function, just named that way for consistency. */ static void fiat_secp521r1_nonzero(limb_t *out1, const fe_t arg1) @@ -11533,7 +11587,7 @@ var_smul_wnaf_two(pt_aff_t *out, const unsigned char a[66], int i, d, is_neg, is_inf = 1, flipped = 0; int8_t anaf[529] = { 0 }; int8_t bnaf[529] = { 0 }; - pt_prj_t Q = { { 0 } }; + pt_prj_t Q = { { 0 }, { 0 }, { 0 } }; pt_prj_t precomp[DRADIX / 2]; precomp_wnaf(precomp, P); @@ -11545,7 +11599,7 @@ var_smul_wnaf_two(pt_aff_t *out, const unsigned char a[66], point_double(&Q, &Q); if ((d = bnaf[i])) { if ((is_neg = d < 0) != flipped) { - fiat_secp521r1_opp(Q.Y, Q.Y); + fiat_secp521r1_carry_opp(Q.Y, Q.Y); flipped ^= 1; } d = (is_neg) ? (-d - 1) >> 1 : (d - 1) >> 1; @@ -11560,7 +11614,7 @@ var_smul_wnaf_two(pt_aff_t *out, const unsigned char a[66], } if ((d = anaf[i])) { if ((is_neg = d < 0) != flipped) { - fiat_secp521r1_opp(Q.Y, Q.Y); + fiat_secp521r1_carry_opp(Q.Y, Q.Y); flipped ^= 1; } d = (is_neg) ? (-d - 1) >> 1 : (d - 1) >> 1; @@ -11584,7 +11638,7 @@ var_smul_wnaf_two(pt_aff_t *out, const unsigned char a[66], if (flipped) { /* correct sign */ - fiat_secp521r1_opp(Q.Y, Q.Y); + fiat_secp521r1_carry_opp(Q.Y, Q.Y); } /* convert to affine -- NB depends on coordinate system */ @@ -11595,6 +11649,8 @@ var_smul_wnaf_two(pt_aff_t *out, const unsigned char a[66], /*- * Variable point scalar multiplication with "regular" wnaf. + * Here "regular" means _no zeroes_, so the sequence of + * EC arithmetic ops is fixed. */ static void var_smul_rwnaf(pt_aff_t *out, const unsigned char scalar[66], @@ -11602,14 +11658,14 @@ var_smul_rwnaf(pt_aff_t *out, const unsigned char scalar[66], { int i, j, d, diff, is_neg; int8_t rnaf[106] = { 0 }; - pt_prj_t Q = { { 0 } }, lut = { { 0 } }; + pt_prj_t Q = { { 0 }, { 0 }, { 0 } }, lut = { { 0 }, { 0 }, { 0 } }; pt_prj_t precomp[DRADIX / 2]; precomp_wnaf(precomp, P); scalar_rwnaf(rnaf, scalar); #if defined(_MSC_VER) -/* result still unsigned: yes we know */ + /* result still unsigned: yes we know */ #pragma warning(push) #pragma warning(disable : 4146) #endif @@ -11639,7 +11695,7 @@ var_smul_rwnaf(pt_aff_t *out, const unsigned char scalar[66], fiat_secp521r1_selectznz(lut.Z, diff, lut.Z, precomp[j].Z); } /* negate lut point if digit is negative */ - fiat_secp521r1_opp(out->Y, lut.Y); + fiat_secp521r1_carry_opp(out->Y, lut.Y); fiat_secp521r1_selectznz(lut.Y, is_neg, lut.Y, out->Y); point_add_proj(&Q, &Q, &lut); } @@ -11650,7 +11706,7 @@ var_smul_rwnaf(pt_aff_t *out, const unsigned char scalar[66], /* conditionally subtract P if the scalar was even */ fe_copy(lut.X, precomp[0].X); - fiat_secp521r1_opp(lut.Y, precomp[0].Y); + fiat_secp521r1_carry_opp(lut.Y, precomp[0].Y); fe_copy(lut.Z, precomp[0].Z); point_add_proj(&lut, &lut, &Q); fiat_secp521r1_selectznz(Q.X, scalar[0] & 1, lut.X, Q.X); @@ -11671,8 +11727,8 @@ fixed_smul_cmb(pt_aff_t *out, const unsigned char scalar[66]) { int i, j, k, d, diff, is_neg = 0; int8_t rnaf[106] = { 0 }; - pt_prj_t Q = { { 0 } }, R = { { 0 } }; - pt_aff_t lut = { { 0 } }; + pt_prj_t Q = { { 0 }, { 0 }, { 0 } }, R = { { 0 }, { 0 }, { 0 } }; + pt_aff_t lut = { { 0 }, { 0 } }; scalar_rwnaf(rnaf, scalar); @@ -11682,7 +11738,7 @@ fixed_smul_cmb(pt_aff_t *out, const unsigned char scalar[66]) fe_set_zero(Q.Z); #if defined(_MSC_VER) -/* result still unsigned: yes we know */ + /* result still unsigned: yes we know */ #pragma warning(push) #pragma warning(disable : 4146) #endif @@ -11705,7 +11761,7 @@ fixed_smul_cmb(pt_aff_t *out, const unsigned char scalar[66]) fiat_secp521r1_selectznz(lut.Y, diff, lut.Y, lut_cmb[j][k].Y); } /* negate lut point if digit is negative */ - fiat_secp521r1_opp(out->Y, lut.Y); + fiat_secp521r1_carry_opp(out->Y, lut.Y); fiat_secp521r1_selectznz(lut.Y, is_neg, lut.Y, out->Y); point_add_mixed(&Q, &Q, &lut); } @@ -11717,7 +11773,7 @@ fixed_smul_cmb(pt_aff_t *out, const unsigned char scalar[66]) /* conditionally subtract P if the scalar was even */ fe_copy(lut.X, lut_cmb[0][0].X); - fiat_secp521r1_opp(lut.Y, lut_cmb[0][0].Y); + fiat_secp521r1_carry_opp(lut.Y, lut_cmb[0][0].Y); point_add_mixed(&R, &Q, &lut); fiat_secp521r1_selectznz(Q.X, scalar[0] & 1, R.X, Q.X); fiat_secp521r1_selectznz(Q.Y, scalar[0] & 1, R.Y, Q.Y); @@ -11736,10 +11792,11 @@ fixed_smul_cmb(pt_aff_t *out, const unsigned char scalar[66]) * Everything is LE byte ordering. */ static void -point_mul_two(unsigned char outx[66], unsigned char outy[66], - const unsigned char a[66], const unsigned char b[66], - const unsigned char inx[66], - const unsigned char iny[66]) +point_mul_two_secp521r1(unsigned char outx[66], unsigned char outy[66], + const unsigned char a[66], + const unsigned char b[66], + const unsigned char inx[66], + const unsigned char iny[66]) { pt_aff_t P; @@ -11758,8 +11815,8 @@ point_mul_two(unsigned char outx[66], unsigned char outy[66], * Everything is LE byte ordering. */ static void -point_mul_g(unsigned char outx[66], unsigned char outy[66], - const unsigned char scalar[66]) +point_mul_g_secp521r1(unsigned char outx[66], unsigned char outy[66], + const unsigned char scalar[66]) { pt_aff_t P; @@ -11776,10 +11833,10 @@ point_mul_g(unsigned char outx[66], unsigned char outy[66], * Everything is LE byte ordering. */ static void -point_mul(unsigned char outx[66], unsigned char outy[66], - const unsigned char scalar[66], - const unsigned char inx[66], - const unsigned char iny[66]) +point_mul_secp521r1(unsigned char outx[66], unsigned char outy[66], + const unsigned char scalar[66], + const unsigned char inx[66], + const unsigned char iny[66]) { pt_aff_t P; @@ -11904,8 +11961,8 @@ point_mul(unsigned char outx[66], unsigned char outy[66], } while (0) static mp_err -point_mul_g_secp521r1(const mp_int *n, mp_int *out_x, - mp_int *out_y, const ECGroup *group) +point_mul_g_secp521r1_wrap(const mp_int *n, mp_int *out_x, + mp_int *out_y, const ECGroup *group) { unsigned char b_x[66]; unsigned char b_y[66]; @@ -11920,7 +11977,7 @@ point_mul_g_secp521r1(const mp_int *n, mp_int *out_x, MP_CHECKOK(mp_to_fixlen_octets(n, b_n, 66)); MP_BE2LE(b_n); - point_mul_g(b_x, b_y, b_n); + point_mul_g_secp521r1(b_x, b_y, b_n); MP_BE2LE(b_x); MP_BE2LE(b_y); MP_CHECKOK(mp_read_unsigned_octets(out_x, b_x, 66)); @@ -11931,9 +11988,9 @@ CLEANUP: } static mp_err -point_mul_secp521r1(const mp_int *n, const mp_int *in_x, - const mp_int *in_y, mp_int *out_x, - mp_int *out_y, const ECGroup *group) +point_mul_secp521r1_wrap(const mp_int *n, const mp_int *in_x, + const mp_int *in_y, mp_int *out_x, + mp_int *out_y, const ECGroup *group) { unsigned char b_x[66]; unsigned char b_y[66]; @@ -11954,7 +12011,7 @@ point_mul_secp521r1(const mp_int *n, const mp_int *in_x, MP_BE2LE(b_x); MP_BE2LE(b_y); MP_BE2LE(b_n); - point_mul(b_x, b_y, b_n, b_x, b_y); + point_mul_secp521r1(b_x, b_y, b_n, b_x, b_y); MP_BE2LE(b_x); MP_BE2LE(b_y); MP_CHECKOK(mp_read_unsigned_octets(out_x, b_x, 66)); @@ -11965,10 +12022,11 @@ CLEANUP: } static mp_err -point_mul_two_secp521r1(const mp_int *n1, const mp_int *n2, - const mp_int *in_x, const mp_int *in_y, - mp_int *out_x, mp_int *out_y, - const ECGroup *group) +point_mul_two_secp521r1_wrap(const mp_int *n1, const mp_int *n2, + const mp_int *in_x, + const mp_int *in_y, mp_int *out_x, + mp_int *out_y, + const ECGroup *group) { unsigned char b_x[66]; unsigned char b_y[66]; @@ -11978,11 +12036,11 @@ point_mul_two_secp521r1(const mp_int *n1, const mp_int *n2, /* If n2 == NULL or 0, this is just a base-point multiplication. */ if (n2 == NULL || mp_cmp_z(n2) == MP_EQ) - return point_mul_g_secp521r1(n1, out_x, out_y, group); + return point_mul_g_secp521r1_wrap(n1, out_x, out_y, group); /* If n1 == NULL or 0, this is just an arbitary-point multiplication. */ if (n1 == NULL || mp_cmp_z(n1) == MP_EQ) - return point_mul_secp521r1(n2, in_x, in_y, out_x, out_y, group); + return point_mul_secp521r1_wrap(n2, in_x, in_y, out_x, out_y, group); ARGCHK(in_x != NULL && in_y != NULL && out_x != NULL && out_y != NULL, MP_BADARG); @@ -12000,7 +12058,7 @@ point_mul_two_secp521r1(const mp_int *n1, const mp_int *n2, MP_BE2LE(b_y); MP_BE2LE(b_n1); MP_BE2LE(b_n2); - point_mul_two(b_x, b_y, b_n1, b_n2, b_x, b_y); + point_mul_two_secp521r1(b_x, b_y, b_n1, b_n2, b_x, b_y); MP_BE2LE(b_x); MP_BE2LE(b_y); MP_CHECKOK(mp_read_unsigned_octets(out_x, b_x, 66)); @@ -12014,9 +12072,9 @@ mp_err ec_group_set_secp521r1(ECGroup *group, ECCurveName name) { if (name == ECCurve_NIST_P521) { - group->base_point_mul = &point_mul_g_secp521r1; - group->point_mul = &point_mul_secp521r1; - group->points_mul = &point_mul_two_secp521r1; + group->base_point_mul = &point_mul_g_secp521r1_wrap; + group->point_mul = &point_mul_secp521r1_wrap; + group->points_mul = &point_mul_two_secp521r1_wrap; } return MP_OKAY; } |