Hacl_P256.c (65315B)
1 /* MIT License 2 * 3 * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation 4 * Copyright (c) 2022-2023 HACL* Contributors 5 * 6 * Permission is hereby granted, free of charge, to any person obtaining a copy 7 * of this software and associated documentation files (the "Software"), to deal 8 * in the Software without restriction, including without limitation the rights 9 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell 10 * copies of the Software, and to permit persons to whom the Software is 11 * furnished to do so, subject to the following conditions: 12 * 13 * The above copyright notice and this permission notice shall be included in all 14 * copies or substantial portions of the Software. 15 * 16 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR 17 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, 18 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE 19 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER 20 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, 21 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE 22 * SOFTWARE. 23 */ 24 25 #include "internal/Hacl_P256.h" 26 27 #include "internal/Hacl_P256_PrecompTable.h" 28 #include "internal/Hacl_Krmllib.h" 29 #include "internal/Hacl_Bignum_Base.h" 30 #include "lib_intrinsics.h" 31 32 static inline uint64_t 33 bn_is_zero_mask4(uint64_t *f) 34 { 35 uint64_t bn_zero[4U] = { 0U }; 36 uint64_t mask = (uint64_t)0xFFFFFFFFFFFFFFFFU; 37 KRML_MAYBE_FOR4(i, 38 (uint32_t)0U, 39 (uint32_t)4U, 40 (uint32_t)1U, 41 uint64_t uu____0 = FStar_UInt64_eq_mask(f[i], bn_zero[i]); 42 mask = uu____0 & mask;); 43 uint64_t mask1 = mask; 44 uint64_t res = mask1; 45 return res; 46 } 47 48 static inline bool 49 bn_is_zero_vartime4(uint64_t *f) 50 { 51 uint64_t m = bn_is_zero_mask4(f); 52 return m == (uint64_t)0xFFFFFFFFFFFFFFFFU; 53 } 54 55 static inline uint64_t 56 bn_is_eq_mask4(uint64_t *a, uint64_t *b) 57 { 58 uint64_t mask = (uint64_t)0xFFFFFFFFFFFFFFFFU; 59 KRML_MAYBE_FOR4(i, 60 (uint32_t)0U, 61 (uint32_t)4U, 62 (uint32_t)1U, 63 uint64_t uu____0 = FStar_UInt64_eq_mask(a[i], b[i]); 64 mask = uu____0 & mask;); 65 uint64_t mask1 = mask; 66 return mask1; 67 } 68 69 static inline bool 70 bn_is_eq_vartime4(uint64_t *a, uint64_t *b) 71 { 72 uint64_t m = bn_is_eq_mask4(a, b); 73 return m == (uint64_t)0xFFFFFFFFFFFFFFFFU; 74 } 75 76 static inline void 77 bn_cmovznz4(uint64_t *res, uint64_t cin, uint64_t *x, uint64_t *y) 78 { 79 uint64_t mask = ~FStar_UInt64_eq_mask(cin, (uint64_t)0U); 80 KRML_MAYBE_FOR4(i, 81 (uint32_t)0U, 82 (uint32_t)4U, 83 (uint32_t)1U, 84 uint64_t *os = res; 85 uint64_t uu____0 = x[i]; 86 uint64_t x1 = uu____0 ^ (mask & (y[i] ^ uu____0)); 87 os[i] = x1;); 88 } 89 90 static inline void 91 bn_add_mod4(uint64_t *res, uint64_t *n, uint64_t *x, uint64_t *y) 92 { 93 uint64_t c0 = (uint64_t)0U; 94 { 95 uint64_t t1 = x[(uint32_t)4U * (uint32_t)0U]; 96 uint64_t t20 = y[(uint32_t)4U * (uint32_t)0U]; 97 uint64_t *res_i0 = res + (uint32_t)4U * (uint32_t)0U; 98 c0 = Lib_IntTypes_Intrinsics_add_carry_u64(c0, t1, t20, res_i0); 99 uint64_t t10 = x[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U]; 100 uint64_t t21 = y[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U]; 101 uint64_t *res_i1 = res + (uint32_t)4U * (uint32_t)0U + (uint32_t)1U; 102 c0 = Lib_IntTypes_Intrinsics_add_carry_u64(c0, t10, t21, res_i1); 103 uint64_t t11 = x[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U]; 104 uint64_t t22 = y[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U]; 105 uint64_t *res_i2 = res + (uint32_t)4U * (uint32_t)0U + (uint32_t)2U; 106 c0 = Lib_IntTypes_Intrinsics_add_carry_u64(c0, t11, t22, res_i2); 107 uint64_t t12 = x[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U]; 108 uint64_t t2 = y[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U]; 109 uint64_t *res_i = res + (uint32_t)4U * (uint32_t)0U + (uint32_t)3U; 110 c0 = Lib_IntTypes_Intrinsics_add_carry_u64(c0, t12, t2, res_i); 111 } 112 uint64_t c00 = c0; 113 uint64_t tmp[4U] = { 0U }; 114 uint64_t c = (uint64_t)0U; 115 { 116 uint64_t t1 = res[(uint32_t)4U * (uint32_t)0U]; 117 uint64_t t20 = n[(uint32_t)4U * (uint32_t)0U]; 118 uint64_t *res_i0 = tmp + (uint32_t)4U * (uint32_t)0U; 119 c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t1, t20, res_i0); 120 uint64_t t10 = res[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U]; 121 uint64_t t21 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U]; 122 uint64_t *res_i1 = tmp + (uint32_t)4U * (uint32_t)0U + (uint32_t)1U; 123 c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t10, t21, res_i1); 124 uint64_t t11 = res[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U]; 125 uint64_t t22 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U]; 126 uint64_t *res_i2 = tmp + (uint32_t)4U * (uint32_t)0U + (uint32_t)2U; 127 c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t11, t22, res_i2); 128 uint64_t t12 = res[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U]; 129 uint64_t t2 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U]; 130 uint64_t *res_i = tmp + (uint32_t)4U * (uint32_t)0U + (uint32_t)3U; 131 c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t12, t2, res_i); 132 } 133 uint64_t c1 = c; 134 uint64_t c2 = c00 - c1; 135 KRML_MAYBE_FOR4(i, 136 (uint32_t)0U, 137 (uint32_t)4U, 138 (uint32_t)1U, 139 uint64_t *os = res; 140 uint64_t x1 = (c2 & res[i]) | (~c2 & tmp[i]); 141 os[i] = x1;); 142 } 143 144 static inline uint64_t 145 bn_sub4(uint64_t *res, uint64_t *x, uint64_t *y) 146 { 147 uint64_t c = (uint64_t)0U; 148 { 149 uint64_t t1 = x[(uint32_t)4U * (uint32_t)0U]; 150 uint64_t t20 = y[(uint32_t)4U * (uint32_t)0U]; 151 uint64_t *res_i0 = res + (uint32_t)4U * (uint32_t)0U; 152 c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t1, t20, res_i0); 153 uint64_t t10 = x[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U]; 154 uint64_t t21 = y[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U]; 155 uint64_t *res_i1 = res + (uint32_t)4U * (uint32_t)0U + (uint32_t)1U; 156 c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t10, t21, res_i1); 157 uint64_t t11 = x[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U]; 158 uint64_t t22 = y[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U]; 159 uint64_t *res_i2 = res + (uint32_t)4U * (uint32_t)0U + (uint32_t)2U; 160 c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t11, t22, res_i2); 161 uint64_t t12 = x[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U]; 162 uint64_t t2 = y[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U]; 163 uint64_t *res_i = res + (uint32_t)4U * (uint32_t)0U + (uint32_t)3U; 164 c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t12, t2, res_i); 165 } 166 uint64_t c0 = c; 167 return c0; 168 } 169 170 static inline void 171 bn_sub_mod4(uint64_t *res, uint64_t *n, uint64_t *x, uint64_t *y) 172 { 173 uint64_t c0 = (uint64_t)0U; 174 { 175 uint64_t t1 = x[(uint32_t)4U * (uint32_t)0U]; 176 uint64_t t20 = y[(uint32_t)4U * (uint32_t)0U]; 177 uint64_t *res_i0 = res + (uint32_t)4U * (uint32_t)0U; 178 c0 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c0, t1, t20, res_i0); 179 uint64_t t10 = x[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U]; 180 uint64_t t21 = y[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U]; 181 uint64_t *res_i1 = res + (uint32_t)4U * (uint32_t)0U + (uint32_t)1U; 182 c0 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c0, t10, t21, res_i1); 183 uint64_t t11 = x[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U]; 184 uint64_t t22 = y[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U]; 185 uint64_t *res_i2 = res + (uint32_t)4U * (uint32_t)0U + (uint32_t)2U; 186 c0 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c0, t11, t22, res_i2); 187 uint64_t t12 = x[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U]; 188 uint64_t t2 = y[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U]; 189 uint64_t *res_i = res + (uint32_t)4U * (uint32_t)0U + (uint32_t)3U; 190 c0 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c0, t12, t2, res_i); 191 } 192 uint64_t c00 = c0; 193 uint64_t tmp[4U] = { 0U }; 194 uint64_t c = (uint64_t)0U; 195 { 196 uint64_t t1 = res[(uint32_t)4U * (uint32_t)0U]; 197 uint64_t t20 = n[(uint32_t)4U * (uint32_t)0U]; 198 uint64_t *res_i0 = tmp + (uint32_t)4U * (uint32_t)0U; 199 c = Lib_IntTypes_Intrinsics_add_carry_u64(c, t1, t20, res_i0); 200 uint64_t t10 = res[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U]; 201 uint64_t t21 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U]; 202 uint64_t *res_i1 = tmp + (uint32_t)4U * (uint32_t)0U + (uint32_t)1U; 203 c = Lib_IntTypes_Intrinsics_add_carry_u64(c, t10, t21, res_i1); 204 uint64_t t11 = res[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U]; 205 uint64_t t22 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U]; 206 uint64_t *res_i2 = tmp + (uint32_t)4U * (uint32_t)0U + (uint32_t)2U; 207 c = Lib_IntTypes_Intrinsics_add_carry_u64(c, t11, t22, res_i2); 208 uint64_t t12 = res[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U]; 209 uint64_t t2 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U]; 210 uint64_t *res_i = tmp + (uint32_t)4U * (uint32_t)0U + (uint32_t)3U; 211 c = Lib_IntTypes_Intrinsics_add_carry_u64(c, t12, t2, res_i); 212 } 213 uint64_t c1 = c; 214 KRML_HOST_IGNORE(c1); 215 uint64_t c2 = (uint64_t)0U - c00; 216 KRML_MAYBE_FOR4(i, 217 (uint32_t)0U, 218 (uint32_t)4U, 219 (uint32_t)1U, 220 uint64_t *os = res; 221 uint64_t x1 = (c2 & tmp[i]) | (~c2 & res[i]); 222 os[i] = x1;); 223 } 224 225 static inline void 226 bn_mul4(uint64_t *res, uint64_t *x, uint64_t *y) 227 { 228 memset(res, 0U, (uint32_t)8U * sizeof(uint64_t)); 229 KRML_MAYBE_FOR4( 230 i0, 231 (uint32_t)0U, 232 (uint32_t)4U, 233 (uint32_t)1U, 234 uint64_t bj = y[i0]; 235 uint64_t *res_j = res + i0; 236 uint64_t c = (uint64_t)0U; 237 { 238 uint64_t a_i = x[(uint32_t)4U * (uint32_t)0U]; 239 uint64_t *res_i0 = res_j + (uint32_t)4U * (uint32_t)0U; 240 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, bj, c, res_i0); 241 uint64_t a_i0 = x[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U]; 242 uint64_t *res_i1 = res_j + (uint32_t)4U * (uint32_t)0U + (uint32_t)1U; 243 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i0, bj, c, res_i1); 244 uint64_t a_i1 = x[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U]; 245 uint64_t *res_i2 = res_j + (uint32_t)4U * (uint32_t)0U + (uint32_t)2U; 246 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i1, bj, c, res_i2); 247 uint64_t a_i2 = x[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U]; 248 uint64_t *res_i = res_j + (uint32_t)4U * (uint32_t)0U + (uint32_t)3U; 249 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i2, bj, c, res_i); 250 } uint64_t r = c; 251 res[(uint32_t)4U + i0] = r;); 252 } 253 254 static inline void 255 bn_sqr4(uint64_t *res, uint64_t *x) 256 { 257 memset(res, 0U, (uint32_t)8U * sizeof(uint64_t)); 258 KRML_MAYBE_FOR4( 259 i0, 260 (uint32_t)0U, 261 (uint32_t)4U, 262 (uint32_t)1U, 263 uint64_t *ab = x; 264 uint64_t a_j = x[i0]; 265 uint64_t *res_j = res + i0; 266 uint64_t c = (uint64_t)0U; 267 for (uint32_t i = (uint32_t)0U; i < i0 / (uint32_t)4U; i++) { 268 uint64_t a_i = ab[(uint32_t)4U * i]; 269 uint64_t *res_i0 = res_j + (uint32_t)4U * i; 270 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, a_j, c, res_i0); 271 uint64_t a_i0 = ab[(uint32_t)4U * i + (uint32_t)1U]; 272 uint64_t *res_i1 = res_j + (uint32_t)4U * i + (uint32_t)1U; 273 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i0, a_j, c, res_i1); 274 uint64_t a_i1 = ab[(uint32_t)4U * i + (uint32_t)2U]; 275 uint64_t *res_i2 = res_j + (uint32_t)4U * i + (uint32_t)2U; 276 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i1, a_j, c, res_i2); 277 uint64_t a_i2 = ab[(uint32_t)4U * i + (uint32_t)3U]; 278 uint64_t *res_i = res_j + (uint32_t)4U * i + (uint32_t)3U; 279 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i2, a_j, c, res_i); 280 } for (uint32_t i = i0 / (uint32_t)4U * (uint32_t)4U; i < i0; i++) { 281 uint64_t a_i = ab[i]; 282 uint64_t *res_i = res_j + i; 283 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, a_j, c, res_i); 284 } uint64_t r = c; 285 res[i0 + i0] = r;); 286 uint64_t c0 = Hacl_Bignum_Addition_bn_add_eq_len_u64((uint32_t)8U, res, res, res); 287 KRML_HOST_IGNORE(c0); 288 uint64_t tmp[8U] = { 0U }; 289 KRML_MAYBE_FOR4(i, 290 (uint32_t)0U, 291 (uint32_t)4U, 292 (uint32_t)1U, 293 FStar_UInt128_uint128 res1 = FStar_UInt128_mul_wide(x[i], x[i]); 294 uint64_t hi = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(res1, (uint32_t)64U)); 295 uint64_t lo = FStar_UInt128_uint128_to_uint64(res1); 296 tmp[(uint32_t)2U * i] = lo; 297 tmp[(uint32_t)2U * i + (uint32_t)1U] = hi;); 298 uint64_t c1 = Hacl_Bignum_Addition_bn_add_eq_len_u64((uint32_t)8U, res, tmp, res); 299 KRML_HOST_IGNORE(c1); 300 } 301 302 static inline void 303 bn_to_bytes_be4(uint8_t *res, uint64_t *f) 304 { 305 uint8_t tmp[32U] = { 0U }; 306 KRML_HOST_IGNORE(tmp); 307 KRML_MAYBE_FOR4(i, 308 (uint32_t)0U, 309 (uint32_t)4U, 310 (uint32_t)1U, 311 store64_be(res + i * (uint32_t)8U, f[(uint32_t)4U - i - (uint32_t)1U]);); 312 } 313 314 static inline void 315 bn_from_bytes_be4(uint64_t *res, uint8_t *b) 316 { 317 KRML_MAYBE_FOR4(i, 318 (uint32_t)0U, 319 (uint32_t)4U, 320 (uint32_t)1U, 321 uint64_t *os = res; 322 uint64_t u = load64_be(b + ((uint32_t)4U - i - (uint32_t)1U) * (uint32_t)8U); 323 uint64_t x = u; 324 os[i] = x;); 325 } 326 327 static inline void 328 bn2_to_bytes_be4(uint8_t *res, uint64_t *x, uint64_t *y) 329 { 330 bn_to_bytes_be4(res, x); 331 bn_to_bytes_be4(res + (uint32_t)32U, y); 332 } 333 334 static inline void 335 make_prime(uint64_t *n) 336 { 337 n[0U] = (uint64_t)0xffffffffffffffffU; 338 n[1U] = (uint64_t)0xffffffffU; 339 n[2U] = (uint64_t)0x0U; 340 n[3U] = (uint64_t)0xffffffff00000001U; 341 } 342 343 static inline void 344 make_order(uint64_t *n) 345 { 346 n[0U] = (uint64_t)0xf3b9cac2fc632551U; 347 n[1U] = (uint64_t)0xbce6faada7179e84U; 348 n[2U] = (uint64_t)0xffffffffffffffffU; 349 n[3U] = (uint64_t)0xffffffff00000000U; 350 } 351 352 static inline void 353 make_a_coeff(uint64_t *a) 354 { 355 a[0U] = (uint64_t)0xfffffffffffffffcU; 356 a[1U] = (uint64_t)0x3ffffffffU; 357 a[2U] = (uint64_t)0x0U; 358 a[3U] = (uint64_t)0xfffffffc00000004U; 359 } 360 361 static inline void 362 make_b_coeff(uint64_t *b) 363 { 364 b[0U] = (uint64_t)0xd89cdf6229c4bddfU; 365 b[1U] = (uint64_t)0xacf005cd78843090U; 366 b[2U] = (uint64_t)0xe5a220abf7212ed6U; 367 b[3U] = (uint64_t)0xdc30061d04874834U; 368 } 369 370 static inline void 371 make_g_x(uint64_t *n) 372 { 373 n[0U] = (uint64_t)0x79e730d418a9143cU; 374 n[1U] = (uint64_t)0x75ba95fc5fedb601U; 375 n[2U] = (uint64_t)0x79fb732b77622510U; 376 n[3U] = (uint64_t)0x18905f76a53755c6U; 377 } 378 379 static inline void 380 make_g_y(uint64_t *n) 381 { 382 n[0U] = (uint64_t)0xddf25357ce95560aU; 383 n[1U] = (uint64_t)0x8b4ab8e4ba19e45cU; 384 n[2U] = (uint64_t)0xd2e88688dd21f325U; 385 n[3U] = (uint64_t)0x8571ff1825885d85U; 386 } 387 388 static inline void 389 make_fmont_R2(uint64_t *n) 390 { 391 n[0U] = (uint64_t)0x3U; 392 n[1U] = (uint64_t)0xfffffffbffffffffU; 393 n[2U] = (uint64_t)0xfffffffffffffffeU; 394 n[3U] = (uint64_t)0x4fffffffdU; 395 } 396 397 static inline void 398 make_fzero(uint64_t *n) 399 { 400 n[0U] = (uint64_t)0U; 401 n[1U] = (uint64_t)0U; 402 n[2U] = (uint64_t)0U; 403 n[3U] = (uint64_t)0U; 404 } 405 406 static inline void 407 make_fone(uint64_t *n) 408 { 409 n[0U] = (uint64_t)0x1U; 410 n[1U] = (uint64_t)0xffffffff00000000U; 411 n[2U] = (uint64_t)0xffffffffffffffffU; 412 n[3U] = (uint64_t)0xfffffffeU; 413 } 414 415 static inline uint64_t 416 bn_is_lt_prime_mask4(uint64_t *f) 417 { 418 uint64_t tmp[4U] = { 0U }; 419 make_prime(tmp); 420 uint64_t c = bn_sub4(tmp, f, tmp); 421 return (uint64_t)0U - c; 422 } 423 424 static inline uint64_t 425 feq_mask(uint64_t *a, uint64_t *b) 426 { 427 uint64_t r = bn_is_eq_mask4(a, b); 428 return r; 429 } 430 431 static inline void 432 fadd0(uint64_t *res, uint64_t *x, uint64_t *y) 433 { 434 uint64_t n[4U] = { 0U }; 435 make_prime(n); 436 bn_add_mod4(res, n, x, y); 437 } 438 439 static inline void 440 fsub0(uint64_t *res, uint64_t *x, uint64_t *y) 441 { 442 uint64_t n[4U] = { 0U }; 443 make_prime(n); 444 bn_sub_mod4(res, n, x, y); 445 } 446 447 static inline void 448 fnegate_conditional_vartime(uint64_t *f, bool is_negate) 449 { 450 uint64_t zero[4U] = { 0U }; 451 if (is_negate) { 452 fsub0(f, zero, f); 453 } 454 } 455 456 static inline void 457 mont_reduction(uint64_t *res, uint64_t *x) 458 { 459 uint64_t n[4U] = { 0U }; 460 make_prime(n); 461 uint64_t c0 = (uint64_t)0U; 462 KRML_MAYBE_FOR4( 463 i0, 464 (uint32_t)0U, 465 (uint32_t)4U, 466 (uint32_t)1U, 467 uint64_t qj = (uint64_t)1U * x[i0]; 468 uint64_t *res_j0 = x + i0; 469 uint64_t c = (uint64_t)0U; 470 { 471 uint64_t a_i = n[(uint32_t)4U * (uint32_t)0U]; 472 uint64_t *res_i0 = res_j0 + (uint32_t)4U * (uint32_t)0U; 473 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, qj, c, res_i0); 474 uint64_t a_i0 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U]; 475 uint64_t *res_i1 = res_j0 + (uint32_t)4U * (uint32_t)0U + (uint32_t)1U; 476 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i0, qj, c, res_i1); 477 uint64_t a_i1 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U]; 478 uint64_t *res_i2 = res_j0 + (uint32_t)4U * (uint32_t)0U + (uint32_t)2U; 479 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i1, qj, c, res_i2); 480 uint64_t a_i2 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U]; 481 uint64_t *res_i = res_j0 + (uint32_t)4U * (uint32_t)0U + (uint32_t)3U; 482 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i2, qj, c, res_i); 483 } uint64_t r = c; 484 uint64_t c1 = r; 485 uint64_t *resb = x + (uint32_t)4U + i0; 486 uint64_t res_j = x[(uint32_t)4U + i0]; 487 c0 = Lib_IntTypes_Intrinsics_add_carry_u64(c0, c1, res_j, resb);); 488 memcpy(res, x + (uint32_t)4U, (uint32_t)4U * sizeof(uint64_t)); 489 uint64_t c00 = c0; 490 uint64_t tmp[4U] = { 0U }; 491 uint64_t c = (uint64_t)0U; 492 { 493 uint64_t t1 = res[(uint32_t)4U * (uint32_t)0U]; 494 uint64_t t20 = n[(uint32_t)4U * (uint32_t)0U]; 495 uint64_t *res_i0 = tmp + (uint32_t)4U * (uint32_t)0U; 496 c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t1, t20, res_i0); 497 uint64_t t10 = res[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U]; 498 uint64_t t21 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U]; 499 uint64_t *res_i1 = tmp + (uint32_t)4U * (uint32_t)0U + (uint32_t)1U; 500 c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t10, t21, res_i1); 501 uint64_t t11 = res[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U]; 502 uint64_t t22 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U]; 503 uint64_t *res_i2 = tmp + (uint32_t)4U * (uint32_t)0U + (uint32_t)2U; 504 c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t11, t22, res_i2); 505 uint64_t t12 = res[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U]; 506 uint64_t t2 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U]; 507 uint64_t *res_i = tmp + (uint32_t)4U * (uint32_t)0U + (uint32_t)3U; 508 c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t12, t2, res_i); 509 } 510 uint64_t c1 = c; 511 uint64_t c2 = c00 - c1; 512 KRML_MAYBE_FOR4(i, 513 (uint32_t)0U, 514 (uint32_t)4U, 515 (uint32_t)1U, 516 uint64_t *os = res; 517 uint64_t x1 = (c2 & res[i]) | (~c2 & tmp[i]); 518 os[i] = x1;); 519 } 520 521 static inline void 522 fmul0(uint64_t *res, uint64_t *x, uint64_t *y) 523 { 524 uint64_t tmp[8U] = { 0U }; 525 bn_mul4(tmp, x, y); 526 mont_reduction(res, tmp); 527 } 528 529 static inline void 530 fsqr0(uint64_t *res, uint64_t *x) 531 { 532 uint64_t tmp[8U] = { 0U }; 533 bn_sqr4(tmp, x); 534 mont_reduction(res, tmp); 535 } 536 537 static inline void 538 from_mont(uint64_t *res, uint64_t *a) 539 { 540 uint64_t tmp[8U] = { 0U }; 541 memcpy(tmp, a, (uint32_t)4U * sizeof(uint64_t)); 542 mont_reduction(res, tmp); 543 } 544 545 static inline void 546 to_mont(uint64_t *res, uint64_t *a) 547 { 548 uint64_t r2modn[4U] = { 0U }; 549 make_fmont_R2(r2modn); 550 fmul0(res, a, r2modn); 551 } 552 553 static inline void 554 fmul_by_b_coeff(uint64_t *res, uint64_t *x) 555 { 556 uint64_t b_coeff[4U] = { 0U }; 557 make_b_coeff(b_coeff); 558 fmul0(res, b_coeff, x); 559 } 560 561 static inline void 562 fcube(uint64_t *res, uint64_t *x) 563 { 564 fsqr0(res, x); 565 fmul0(res, res, x); 566 } 567 568 static inline void 569 finv(uint64_t *res, uint64_t *a) 570 { 571 uint64_t tmp[16U] = { 0U }; 572 uint64_t *x30 = tmp; 573 uint64_t *x2 = tmp + (uint32_t)4U; 574 uint64_t *tmp1 = tmp + (uint32_t)8U; 575 uint64_t *tmp2 = tmp + (uint32_t)12U; 576 memcpy(x2, a, (uint32_t)4U * sizeof(uint64_t)); 577 { 578 fsqr0(x2, x2); 579 } 580 fmul0(x2, x2, a); 581 memcpy(x30, x2, (uint32_t)4U * sizeof(uint64_t)); 582 { 583 fsqr0(x30, x30); 584 } 585 fmul0(x30, x30, a); 586 memcpy(tmp1, x30, (uint32_t)4U * sizeof(uint64_t)); 587 KRML_MAYBE_FOR3(i, (uint32_t)0U, (uint32_t)3U, (uint32_t)1U, fsqr0(tmp1, tmp1);); 588 fmul0(tmp1, tmp1, x30); 589 memcpy(tmp2, tmp1, (uint32_t)4U * sizeof(uint64_t)); 590 KRML_MAYBE_FOR6(i, (uint32_t)0U, (uint32_t)6U, (uint32_t)1U, fsqr0(tmp2, tmp2);); 591 fmul0(tmp2, tmp2, tmp1); 592 memcpy(tmp1, tmp2, (uint32_t)4U * sizeof(uint64_t)); 593 KRML_MAYBE_FOR3(i, (uint32_t)0U, (uint32_t)3U, (uint32_t)1U, fsqr0(tmp1, tmp1);); 594 fmul0(tmp1, tmp1, x30); 595 memcpy(x30, tmp1, (uint32_t)4U * sizeof(uint64_t)); 596 KRML_MAYBE_FOR15(i, (uint32_t)0U, (uint32_t)15U, (uint32_t)1U, fsqr0(x30, x30);); 597 fmul0(x30, x30, tmp1); 598 memcpy(tmp1, x30, (uint32_t)4U * sizeof(uint64_t)); 599 KRML_MAYBE_FOR2(i, (uint32_t)0U, (uint32_t)2U, (uint32_t)1U, fsqr0(tmp1, tmp1);); 600 fmul0(tmp1, tmp1, x2); 601 memcpy(x2, tmp1, (uint32_t)4U * sizeof(uint64_t)); 602 for (uint32_t i = (uint32_t)0U; i < (uint32_t)32U; i++) { 603 fsqr0(x2, x2); 604 } 605 fmul0(x2, x2, a); 606 for (uint32_t i = (uint32_t)0U; i < (uint32_t)128U; i++) { 607 fsqr0(x2, x2); 608 } 609 fmul0(x2, x2, tmp1); 610 for (uint32_t i = (uint32_t)0U; i < (uint32_t)32U; i++) { 611 fsqr0(x2, x2); 612 } 613 fmul0(x2, x2, tmp1); 614 for (uint32_t i = (uint32_t)0U; i < (uint32_t)30U; i++) { 615 fsqr0(x2, x2); 616 } 617 fmul0(x2, x2, x30); 618 KRML_MAYBE_FOR2(i, (uint32_t)0U, (uint32_t)2U, (uint32_t)1U, fsqr0(x2, x2);); 619 fmul0(tmp1, x2, a); 620 memcpy(res, tmp1, (uint32_t)4U * sizeof(uint64_t)); 621 } 622 623 static inline void 624 fsqrt(uint64_t *res, uint64_t *a) 625 { 626 uint64_t tmp[8U] = { 0U }; 627 uint64_t *tmp1 = tmp; 628 uint64_t *tmp2 = tmp + (uint32_t)4U; 629 memcpy(tmp1, a, (uint32_t)4U * sizeof(uint64_t)); 630 { 631 fsqr0(tmp1, tmp1); 632 } 633 fmul0(tmp1, tmp1, a); 634 memcpy(tmp2, tmp1, (uint32_t)4U * sizeof(uint64_t)); 635 KRML_MAYBE_FOR2(i, (uint32_t)0U, (uint32_t)2U, (uint32_t)1U, fsqr0(tmp2, tmp2);); 636 fmul0(tmp2, tmp2, tmp1); 637 memcpy(tmp1, tmp2, (uint32_t)4U * sizeof(uint64_t)); 638 KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, fsqr0(tmp1, tmp1);); 639 fmul0(tmp1, tmp1, tmp2); 640 memcpy(tmp2, tmp1, (uint32_t)4U * sizeof(uint64_t)); 641 KRML_MAYBE_FOR8(i, (uint32_t)0U, (uint32_t)8U, (uint32_t)1U, fsqr0(tmp2, tmp2);); 642 fmul0(tmp2, tmp2, tmp1); 643 memcpy(tmp1, tmp2, (uint32_t)4U * sizeof(uint64_t)); 644 KRML_MAYBE_FOR16(i, (uint32_t)0U, (uint32_t)16U, (uint32_t)1U, fsqr0(tmp1, tmp1);); 645 fmul0(tmp1, tmp1, tmp2); 646 memcpy(tmp2, tmp1, (uint32_t)4U * sizeof(uint64_t)); 647 for (uint32_t i = (uint32_t)0U; i < (uint32_t)32U; i++) { 648 fsqr0(tmp2, tmp2); 649 } 650 fmul0(tmp2, tmp2, a); 651 for (uint32_t i = (uint32_t)0U; i < (uint32_t)96U; i++) { 652 fsqr0(tmp2, tmp2); 653 } 654 fmul0(tmp2, tmp2, a); 655 for (uint32_t i = (uint32_t)0U; i < (uint32_t)94U; i++) { 656 fsqr0(tmp2, tmp2); 657 } 658 memcpy(res, tmp2, (uint32_t)4U * sizeof(uint64_t)); 659 } 660 661 static inline void 662 make_base_point(uint64_t *p) 663 { 664 uint64_t *x = p; 665 uint64_t *y = p + (uint32_t)4U; 666 uint64_t *z = p + (uint32_t)8U; 667 make_g_x(x); 668 make_g_y(y); 669 make_fone(z); 670 } 671 672 static inline void 673 make_point_at_inf(uint64_t *p) 674 { 675 uint64_t *x = p; 676 uint64_t *y = p + (uint32_t)4U; 677 uint64_t *z = p + (uint32_t)8U; 678 make_fzero(x); 679 make_fone(y); 680 make_fzero(z); 681 } 682 683 static inline bool 684 is_point_at_inf_vartime(uint64_t *p) 685 { 686 uint64_t *pz = p + (uint32_t)8U; 687 return bn_is_zero_vartime4(pz); 688 } 689 690 static inline void 691 to_aff_point(uint64_t *res, uint64_t *p) 692 { 693 uint64_t zinv[4U] = { 0U }; 694 uint64_t *px = p; 695 uint64_t *py = p + (uint32_t)4U; 696 uint64_t *pz = p + (uint32_t)8U; 697 uint64_t *x = res; 698 uint64_t *y = res + (uint32_t)4U; 699 finv(zinv, pz); 700 fmul0(x, px, zinv); 701 fmul0(y, py, zinv); 702 from_mont(x, x); 703 from_mont(y, y); 704 } 705 706 static inline void 707 to_aff_point_x(uint64_t *res, uint64_t *p) 708 { 709 uint64_t zinv[4U] = { 0U }; 710 uint64_t *px = p; 711 uint64_t *pz = p + (uint32_t)8U; 712 finv(zinv, pz); 713 fmul0(res, px, zinv); 714 from_mont(res, res); 715 } 716 717 static inline void 718 to_proj_point(uint64_t *res, uint64_t *p) 719 { 720 uint64_t *px = p; 721 uint64_t *py = p + (uint32_t)4U; 722 uint64_t *rx = res; 723 uint64_t *ry = res + (uint32_t)4U; 724 uint64_t *rz = res + (uint32_t)8U; 725 to_mont(rx, px); 726 to_mont(ry, py); 727 make_fone(rz); 728 } 729 730 static inline bool 731 is_on_curve_vartime(uint64_t *p) 732 { 733 uint64_t rp[4U] = { 0U }; 734 uint64_t tx[4U] = { 0U }; 735 uint64_t ty[4U] = { 0U }; 736 uint64_t *px = p; 737 uint64_t *py = p + (uint32_t)4U; 738 to_mont(tx, px); 739 to_mont(ty, py); 740 uint64_t tmp[4U] = { 0U }; 741 fcube(rp, tx); 742 make_a_coeff(tmp); 743 fmul0(tmp, tmp, tx); 744 fadd0(rp, tmp, rp); 745 make_b_coeff(tmp); 746 fadd0(rp, tmp, rp); 747 fsqr0(ty, ty); 748 uint64_t r = feq_mask(ty, rp); 749 bool r0 = r == (uint64_t)0xFFFFFFFFFFFFFFFFU; 750 return r0; 751 } 752 753 static inline void 754 aff_point_store(uint8_t *res, uint64_t *p) 755 { 756 uint64_t *px = p; 757 uint64_t *py = p + (uint32_t)4U; 758 bn2_to_bytes_be4(res, px, py); 759 } 760 761 static inline void 762 point_store(uint8_t *res, uint64_t *p) 763 { 764 uint64_t aff_p[8U] = { 0U }; 765 to_aff_point(aff_p, p); 766 aff_point_store(res, aff_p); 767 } 768 769 static inline bool 770 aff_point_load_vartime(uint64_t *p, uint8_t *b) 771 { 772 uint8_t *p_x = b; 773 uint8_t *p_y = b + (uint32_t)32U; 774 uint64_t *bn_p_x = p; 775 uint64_t *bn_p_y = p + (uint32_t)4U; 776 bn_from_bytes_be4(bn_p_x, p_x); 777 bn_from_bytes_be4(bn_p_y, p_y); 778 uint64_t *px = p; 779 uint64_t *py = p + (uint32_t)4U; 780 uint64_t lessX = bn_is_lt_prime_mask4(px); 781 uint64_t lessY = bn_is_lt_prime_mask4(py); 782 uint64_t res = lessX & lessY; 783 bool is_xy_valid = res == (uint64_t)0xFFFFFFFFFFFFFFFFU; 784 if (!is_xy_valid) { 785 return false; 786 } 787 return is_on_curve_vartime(p); 788 } 789 790 static inline bool 791 load_point_vartime(uint64_t *p, uint8_t *b) 792 { 793 uint64_t p_aff[8U] = { 0U }; 794 bool res = aff_point_load_vartime(p_aff, b); 795 if (res) { 796 to_proj_point(p, p_aff); 797 } 798 return res; 799 } 800 801 static inline bool 802 aff_point_decompress_vartime(uint64_t *x, uint64_t *y, uint8_t *s) 803 { 804 uint8_t s0 = s[0U]; 805 uint8_t s01 = s0; 806 if (!(s01 == (uint8_t)0x02U || s01 == (uint8_t)0x03U)) { 807 return false; 808 } 809 uint8_t *xb = s + (uint32_t)1U; 810 bn_from_bytes_be4(x, xb); 811 uint64_t is_x_valid = bn_is_lt_prime_mask4(x); 812 bool is_x_valid1 = is_x_valid == (uint64_t)0xFFFFFFFFFFFFFFFFU; 813 bool is_y_odd = s01 == (uint8_t)0x03U; 814 if (!is_x_valid1) { 815 return false; 816 } 817 uint64_t y2M[4U] = { 0U }; 818 uint64_t xM[4U] = { 0U }; 819 uint64_t yM[4U] = { 0U }; 820 to_mont(xM, x); 821 uint64_t tmp[4U] = { 0U }; 822 fcube(y2M, xM); 823 make_a_coeff(tmp); 824 fmul0(tmp, tmp, xM); 825 fadd0(y2M, tmp, y2M); 826 make_b_coeff(tmp); 827 fadd0(y2M, tmp, y2M); 828 fsqrt(yM, y2M); 829 from_mont(y, yM); 830 fsqr0(yM, yM); 831 uint64_t r = feq_mask(yM, y2M); 832 bool is_y_valid = r == (uint64_t)0xFFFFFFFFFFFFFFFFU; 833 bool is_y_valid0 = is_y_valid; 834 if (!is_y_valid0) { 835 return false; 836 } 837 uint64_t is_y_odd1 = y[0U] & (uint64_t)1U; 838 bool is_y_odd2 = is_y_odd1 == (uint64_t)1U; 839 fnegate_conditional_vartime(y, is_y_odd2 != is_y_odd); 840 return true; 841 } 842 843 static inline void 844 point_double(uint64_t *res, uint64_t *p) 845 { 846 uint64_t tmp[20U] = { 0U }; 847 uint64_t *x = p; 848 uint64_t *z = p + (uint32_t)8U; 849 uint64_t *x3 = res; 850 uint64_t *y3 = res + (uint32_t)4U; 851 uint64_t *z3 = res + (uint32_t)8U; 852 uint64_t *t0 = tmp; 853 uint64_t *t1 = tmp + (uint32_t)4U; 854 uint64_t *t2 = tmp + (uint32_t)8U; 855 uint64_t *t3 = tmp + (uint32_t)12U; 856 uint64_t *t4 = tmp + (uint32_t)16U; 857 uint64_t *x1 = p; 858 uint64_t *y = p + (uint32_t)4U; 859 uint64_t *z1 = p + (uint32_t)8U; 860 fsqr0(t0, x1); 861 fsqr0(t1, y); 862 fsqr0(t2, z1); 863 fmul0(t3, x1, y); 864 fadd0(t3, t3, t3); 865 fmul0(t4, y, z1); 866 fmul0(z3, x, z); 867 fadd0(z3, z3, z3); 868 fmul_by_b_coeff(y3, t2); 869 fsub0(y3, y3, z3); 870 fadd0(x3, y3, y3); 871 fadd0(y3, x3, y3); 872 fsub0(x3, t1, y3); 873 fadd0(y3, t1, y3); 874 fmul0(y3, x3, y3); 875 fmul0(x3, x3, t3); 876 fadd0(t3, t2, t2); 877 fadd0(t2, t2, t3); 878 fmul_by_b_coeff(z3, z3); 879 fsub0(z3, z3, t2); 880 fsub0(z3, z3, t0); 881 fadd0(t3, z3, z3); 882 fadd0(z3, z3, t3); 883 fadd0(t3, t0, t0); 884 fadd0(t0, t3, t0); 885 fsub0(t0, t0, t2); 886 fmul0(t0, t0, z3); 887 fadd0(y3, y3, t0); 888 fadd0(t0, t4, t4); 889 fmul0(z3, t0, z3); 890 fsub0(x3, x3, z3); 891 fmul0(z3, t0, t1); 892 fadd0(z3, z3, z3); 893 fadd0(z3, z3, z3); 894 } 895 896 static inline void 897 point_add(uint64_t *res, uint64_t *p, uint64_t *q) 898 { 899 uint64_t tmp[36U] = { 0U }; 900 uint64_t *t0 = tmp; 901 uint64_t *t1 = tmp + (uint32_t)24U; 902 uint64_t *x3 = t1; 903 uint64_t *y3 = t1 + (uint32_t)4U; 904 uint64_t *z3 = t1 + (uint32_t)8U; 905 uint64_t *t01 = t0; 906 uint64_t *t11 = t0 + (uint32_t)4U; 907 uint64_t *t2 = t0 + (uint32_t)8U; 908 uint64_t *t3 = t0 + (uint32_t)12U; 909 uint64_t *t4 = t0 + (uint32_t)16U; 910 uint64_t *t5 = t0 + (uint32_t)20U; 911 uint64_t *x1 = p; 912 uint64_t *y1 = p + (uint32_t)4U; 913 uint64_t *z10 = p + (uint32_t)8U; 914 uint64_t *x20 = q; 915 uint64_t *y20 = q + (uint32_t)4U; 916 uint64_t *z20 = q + (uint32_t)8U; 917 fmul0(t01, x1, x20); 918 fmul0(t11, y1, y20); 919 fmul0(t2, z10, z20); 920 fadd0(t3, x1, y1); 921 fadd0(t4, x20, y20); 922 fmul0(t3, t3, t4); 923 fadd0(t4, t01, t11); 924 uint64_t *y10 = p + (uint32_t)4U; 925 uint64_t *z11 = p + (uint32_t)8U; 926 uint64_t *y2 = q + (uint32_t)4U; 927 uint64_t *z21 = q + (uint32_t)8U; 928 fsub0(t3, t3, t4); 929 fadd0(t4, y10, z11); 930 fadd0(t5, y2, z21); 931 fmul0(t4, t4, t5); 932 fadd0(t5, t11, t2); 933 fsub0(t4, t4, t5); 934 uint64_t *x10 = p; 935 uint64_t *z1 = p + (uint32_t)8U; 936 uint64_t *x2 = q; 937 uint64_t *z2 = q + (uint32_t)8U; 938 fadd0(x3, x10, z1); 939 fadd0(y3, x2, z2); 940 fmul0(x3, x3, y3); 941 fadd0(y3, t01, t2); 942 fsub0(y3, x3, y3); 943 fmul_by_b_coeff(z3, t2); 944 fsub0(x3, y3, z3); 945 fadd0(z3, x3, x3); 946 fadd0(x3, x3, z3); 947 fsub0(z3, t11, x3); 948 fadd0(x3, t11, x3); 949 fmul_by_b_coeff(y3, y3); 950 fadd0(t11, t2, t2); 951 fadd0(t2, t11, t2); 952 fsub0(y3, y3, t2); 953 fsub0(y3, y3, t01); 954 fadd0(t11, y3, y3); 955 fadd0(y3, t11, y3); 956 fadd0(t11, t01, t01); 957 fadd0(t01, t11, t01); 958 fsub0(t01, t01, t2); 959 fmul0(t11, t4, y3); 960 fmul0(t2, t01, y3); 961 fmul0(y3, x3, z3); 962 fadd0(y3, y3, t2); 963 fmul0(x3, t3, x3); 964 fsub0(x3, x3, t11); 965 fmul0(z3, t4, z3); 966 fmul0(t11, t3, t01); 967 fadd0(z3, z3, t11); 968 memcpy(res, t1, (uint32_t)12U * sizeof(uint64_t)); 969 } 970 971 static inline void 972 point_mul(uint64_t *res, uint64_t *scalar, uint64_t *p) 973 { 974 uint64_t table[192U] = { 0U }; 975 uint64_t tmp[12U] = { 0U }; 976 uint64_t *t0 = table; 977 uint64_t *t1 = table + (uint32_t)12U; 978 make_point_at_inf(t0); 979 memcpy(t1, p, (uint32_t)12U * sizeof(uint64_t)); 980 KRML_MAYBE_FOR7(i, 981 (uint32_t)0U, 982 (uint32_t)7U, 983 (uint32_t)1U, 984 uint64_t *t11 = table + (i + (uint32_t)1U) * (uint32_t)12U; 985 point_double(tmp, t11); 986 memcpy(table + ((uint32_t)2U * i + (uint32_t)2U) * (uint32_t)12U, 987 tmp, 988 (uint32_t)12U * sizeof(uint64_t)); 989 uint64_t *t2 = table + ((uint32_t)2U * i + (uint32_t)2U) * (uint32_t)12U; 990 point_add(tmp, p, t2); 991 memcpy(table + ((uint32_t)2U * i + (uint32_t)3U) * (uint32_t)12U, 992 tmp, 993 (uint32_t)12U * sizeof(uint64_t));); 994 make_point_at_inf(res); 995 uint64_t tmp0[12U] = { 0U }; 996 for (uint32_t i0 = (uint32_t)0U; i0 < (uint32_t)64U; i0++) { 997 KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, point_double(res, res);); 998 uint32_t k = (uint32_t)256U - (uint32_t)4U * i0 - (uint32_t)4U; 999 uint64_t bits_l = Hacl_Bignum_Lib_bn_get_bits_u64((uint32_t)4U, scalar, k, (uint32_t)4U); 1000 memcpy(tmp0, (uint64_t *)table, (uint32_t)12U * sizeof(uint64_t)); 1001 KRML_MAYBE_FOR15(i1, 1002 (uint32_t)0U, 1003 (uint32_t)15U, 1004 (uint32_t)1U, 1005 uint64_t c = FStar_UInt64_eq_mask(bits_l, (uint64_t)(i1 + (uint32_t)1U)); 1006 const uint64_t *res_j = table + (i1 + (uint32_t)1U) * (uint32_t)12U; 1007 KRML_MAYBE_FOR12(i, 1008 (uint32_t)0U, 1009 (uint32_t)12U, 1010 (uint32_t)1U, 1011 uint64_t *os = tmp0; 1012 uint64_t x = (c & res_j[i]) | (~c & tmp0[i]); 1013 os[i] = x;);); 1014 point_add(res, res, tmp0); 1015 } 1016 } 1017 1018 static inline void 1019 precomp_get_consttime(const uint64_t *table, uint64_t bits_l, uint64_t *tmp) 1020 { 1021 memcpy(tmp, (uint64_t *)table, (uint32_t)12U * sizeof(uint64_t)); 1022 KRML_MAYBE_FOR15(i0, 1023 (uint32_t)0U, 1024 (uint32_t)15U, 1025 (uint32_t)1U, 1026 uint64_t c = FStar_UInt64_eq_mask(bits_l, (uint64_t)(i0 + (uint32_t)1U)); 1027 const uint64_t *res_j = table + (i0 + (uint32_t)1U) * (uint32_t)12U; 1028 KRML_MAYBE_FOR12(i, 1029 (uint32_t)0U, 1030 (uint32_t)12U, 1031 (uint32_t)1U, 1032 uint64_t *os = tmp; 1033 uint64_t x = (c & res_j[i]) | (~c & tmp[i]); 1034 os[i] = x;);); 1035 } 1036 1037 static inline void 1038 point_mul_g(uint64_t *res, uint64_t *scalar) 1039 { 1040 uint64_t q1[12U] = { 0U }; 1041 make_base_point(q1); 1042 uint64_t 1043 q2[12U] = { 1044 (uint64_t)1499621593102562565U, (uint64_t)16692369783039433128U, 1045 (uint64_t)15337520135922861848U, (uint64_t)5455737214495366228U, 1046 (uint64_t)17827017231032529600U, (uint64_t)12413621606240782649U, 1047 (uint64_t)2290483008028286132U, (uint64_t)15752017553340844820U, 1048 (uint64_t)4846430910634234874U, (uint64_t)10861682798464583253U, 1049 (uint64_t)15404737222404363049U, (uint64_t)363586619281562022U 1050 }; 1051 uint64_t 1052 q3[12U] = { 1053 (uint64_t)14619254753077084366U, (uint64_t)13913835116514008593U, 1054 (uint64_t)15060744674088488145U, (uint64_t)17668414598203068685U, 1055 (uint64_t)10761169236902342334U, (uint64_t)15467027479157446221U, 1056 (uint64_t)14989185522423469618U, (uint64_t)14354539272510107003U, 1057 (uint64_t)14298211796392133693U, (uint64_t)13270323784253711450U, 1058 (uint64_t)13380964971965046957U, (uint64_t)8686204248456909699U 1059 }; 1060 uint64_t 1061 q4[12U] = { 1062 (uint64_t)7870395003430845958U, (uint64_t)18001862936410067720U, 1063 (uint64_t)8006461232116967215U, (uint64_t)5921313779532424762U, 1064 (uint64_t)10702113371959864307U, (uint64_t)8070517410642379879U, 1065 (uint64_t)7139806720777708306U, (uint64_t)8253938546650739833U, 1066 (uint64_t)17490482834545705718U, (uint64_t)1065249776797037500U, 1067 (uint64_t)5018258455937968775U, (uint64_t)14100621120178668337U 1068 }; 1069 uint64_t *r1 = scalar; 1070 uint64_t *r2 = scalar + (uint32_t)1U; 1071 uint64_t *r3 = scalar + (uint32_t)2U; 1072 uint64_t *r4 = scalar + (uint32_t)3U; 1073 make_point_at_inf(res); 1074 uint64_t tmp[12U] = { 0U }; 1075 KRML_MAYBE_FOR16(i, 1076 (uint32_t)0U, 1077 (uint32_t)16U, 1078 (uint32_t)1U, 1079 KRML_MAYBE_FOR4(i0, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, point_double(res, res);); 1080 uint32_t k = (uint32_t)64U - (uint32_t)4U * i - (uint32_t)4U; 1081 uint64_t bits_l = Hacl_Bignum_Lib_bn_get_bits_u64((uint32_t)1U, r4, k, (uint32_t)4U); 1082 precomp_get_consttime(Hacl_P256_PrecompTable_precomp_g_pow2_192_table_w4, bits_l, tmp); 1083 point_add(res, res, tmp); 1084 uint32_t k0 = (uint32_t)64U - (uint32_t)4U * i - (uint32_t)4U; 1085 uint64_t bits_l0 = Hacl_Bignum_Lib_bn_get_bits_u64((uint32_t)1U, r3, k0, (uint32_t)4U); 1086 precomp_get_consttime(Hacl_P256_PrecompTable_precomp_g_pow2_128_table_w4, bits_l0, tmp); 1087 point_add(res, res, tmp); 1088 uint32_t k1 = (uint32_t)64U - (uint32_t)4U * i - (uint32_t)4U; 1089 uint64_t bits_l1 = Hacl_Bignum_Lib_bn_get_bits_u64((uint32_t)1U, r2, k1, (uint32_t)4U); 1090 precomp_get_consttime(Hacl_P256_PrecompTable_precomp_g_pow2_64_table_w4, bits_l1, tmp); 1091 point_add(res, res, tmp); 1092 uint32_t k2 = (uint32_t)64U - (uint32_t)4U * i - (uint32_t)4U; 1093 uint64_t bits_l2 = Hacl_Bignum_Lib_bn_get_bits_u64((uint32_t)1U, r1, k2, (uint32_t)4U); 1094 precomp_get_consttime(Hacl_P256_PrecompTable_precomp_basepoint_table_w4, bits_l2, tmp); 1095 point_add(res, res, tmp);); 1096 KRML_HOST_IGNORE(q1); 1097 KRML_HOST_IGNORE(q2); 1098 KRML_HOST_IGNORE(q3); 1099 KRML_HOST_IGNORE(q4); 1100 } 1101 1102 static inline void 1103 point_mul_double_g(uint64_t *res, uint64_t *scalar1, uint64_t *scalar2, uint64_t *q2) 1104 { 1105 uint64_t q1[12U] = { 0U }; 1106 make_base_point(q1); 1107 uint64_t table2[384U] = { 0U }; 1108 uint64_t tmp[12U] = { 0U }; 1109 uint64_t *t0 = table2; 1110 uint64_t *t1 = table2 + (uint32_t)12U; 1111 make_point_at_inf(t0); 1112 memcpy(t1, q2, (uint32_t)12U * sizeof(uint64_t)); 1113 KRML_MAYBE_FOR15(i, 1114 (uint32_t)0U, 1115 (uint32_t)15U, 1116 (uint32_t)1U, 1117 uint64_t *t11 = table2 + (i + (uint32_t)1U) * (uint32_t)12U; 1118 point_double(tmp, t11); 1119 memcpy(table2 + ((uint32_t)2U * i + (uint32_t)2U) * (uint32_t)12U, 1120 tmp, 1121 (uint32_t)12U * sizeof(uint64_t)); 1122 uint64_t *t2 = table2 + ((uint32_t)2U * i + (uint32_t)2U) * (uint32_t)12U; 1123 point_add(tmp, q2, t2); 1124 memcpy(table2 + ((uint32_t)2U * i + (uint32_t)3U) * (uint32_t)12U, 1125 tmp, 1126 (uint32_t)12U * sizeof(uint64_t));); 1127 uint64_t tmp0[12U] = { 0U }; 1128 uint32_t i0 = (uint32_t)255U; 1129 uint64_t bits_c = Hacl_Bignum_Lib_bn_get_bits_u64((uint32_t)4U, scalar1, i0, (uint32_t)5U); 1130 uint32_t bits_l32 = (uint32_t)bits_c; 1131 const uint64_t 1132 *a_bits_l = Hacl_P256_PrecompTable_precomp_basepoint_table_w5 + bits_l32 * (uint32_t)12U; 1133 memcpy(res, (uint64_t *)a_bits_l, (uint32_t)12U * sizeof(uint64_t)); 1134 uint32_t i1 = (uint32_t)255U; 1135 uint64_t bits_c0 = Hacl_Bignum_Lib_bn_get_bits_u64((uint32_t)4U, scalar2, i1, (uint32_t)5U); 1136 uint32_t bits_l320 = (uint32_t)bits_c0; 1137 const uint64_t *a_bits_l0 = table2 + bits_l320 * (uint32_t)12U; 1138 memcpy(tmp0, (uint64_t *)a_bits_l0, (uint32_t)12U * sizeof(uint64_t)); 1139 point_add(res, res, tmp0); 1140 uint64_t tmp1[12U] = { 0U }; 1141 for (uint32_t i = (uint32_t)0U; i < (uint32_t)51U; i++) { 1142 KRML_MAYBE_FOR5(i2, (uint32_t)0U, (uint32_t)5U, (uint32_t)1U, point_double(res, res);); 1143 uint32_t k = (uint32_t)255U - (uint32_t)5U * i - (uint32_t)5U; 1144 uint64_t bits_l = Hacl_Bignum_Lib_bn_get_bits_u64((uint32_t)4U, scalar2, k, (uint32_t)5U); 1145 uint32_t bits_l321 = (uint32_t)bits_l; 1146 const uint64_t *a_bits_l1 = table2 + bits_l321 * (uint32_t)12U; 1147 memcpy(tmp1, (uint64_t *)a_bits_l1, (uint32_t)12U * sizeof(uint64_t)); 1148 point_add(res, res, tmp1); 1149 uint32_t k0 = (uint32_t)255U - (uint32_t)5U * i - (uint32_t)5U; 1150 uint64_t bits_l0 = Hacl_Bignum_Lib_bn_get_bits_u64((uint32_t)4U, scalar1, k0, (uint32_t)5U); 1151 uint32_t bits_l322 = (uint32_t)bits_l0; 1152 const uint64_t 1153 *a_bits_l2 = Hacl_P256_PrecompTable_precomp_basepoint_table_w5 + bits_l322 * (uint32_t)12U; 1154 memcpy(tmp1, (uint64_t *)a_bits_l2, (uint32_t)12U * sizeof(uint64_t)); 1155 point_add(res, res, tmp1); 1156 } 1157 } 1158 1159 static inline uint64_t 1160 bn_is_lt_order_mask4(uint64_t *f) 1161 { 1162 uint64_t tmp[4U] = { 0U }; 1163 make_order(tmp); 1164 uint64_t c = bn_sub4(tmp, f, tmp); 1165 return (uint64_t)0U - c; 1166 } 1167 1168 static inline uint64_t 1169 bn_is_lt_order_and_gt_zero_mask4(uint64_t *f) 1170 { 1171 uint64_t is_lt_order = bn_is_lt_order_mask4(f); 1172 uint64_t is_eq_zero = bn_is_zero_mask4(f); 1173 return is_lt_order & ~is_eq_zero; 1174 } 1175 1176 static inline void 1177 qmod_short(uint64_t *res, uint64_t *x) 1178 { 1179 uint64_t tmp[4U] = { 0U }; 1180 make_order(tmp); 1181 uint64_t c = bn_sub4(tmp, x, tmp); 1182 bn_cmovznz4(res, c, tmp, x); 1183 } 1184 1185 static inline void 1186 qadd(uint64_t *res, uint64_t *x, uint64_t *y) 1187 { 1188 uint64_t n[4U] = { 0U }; 1189 make_order(n); 1190 bn_add_mod4(res, n, x, y); 1191 } 1192 1193 static inline void 1194 qmont_reduction(uint64_t *res, uint64_t *x) 1195 { 1196 uint64_t n[4U] = { 0U }; 1197 make_order(n); 1198 uint64_t c0 = (uint64_t)0U; 1199 KRML_MAYBE_FOR4( 1200 i0, 1201 (uint32_t)0U, 1202 (uint32_t)4U, 1203 (uint32_t)1U, 1204 uint64_t qj = (uint64_t)0xccd1c8aaee00bc4fU * x[i0]; 1205 uint64_t *res_j0 = x + i0; 1206 uint64_t c = (uint64_t)0U; 1207 { 1208 uint64_t a_i = n[(uint32_t)4U * (uint32_t)0U]; 1209 uint64_t *res_i0 = res_j0 + (uint32_t)4U * (uint32_t)0U; 1210 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, qj, c, res_i0); 1211 uint64_t a_i0 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U]; 1212 uint64_t *res_i1 = res_j0 + (uint32_t)4U * (uint32_t)0U + (uint32_t)1U; 1213 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i0, qj, c, res_i1); 1214 uint64_t a_i1 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U]; 1215 uint64_t *res_i2 = res_j0 + (uint32_t)4U * (uint32_t)0U + (uint32_t)2U; 1216 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i1, qj, c, res_i2); 1217 uint64_t a_i2 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U]; 1218 uint64_t *res_i = res_j0 + (uint32_t)4U * (uint32_t)0U + (uint32_t)3U; 1219 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i2, qj, c, res_i); 1220 } uint64_t r = c; 1221 uint64_t c1 = r; 1222 uint64_t *resb = x + (uint32_t)4U + i0; 1223 uint64_t res_j = x[(uint32_t)4U + i0]; 1224 c0 = Lib_IntTypes_Intrinsics_add_carry_u64(c0, c1, res_j, resb);); 1225 memcpy(res, x + (uint32_t)4U, (uint32_t)4U * sizeof(uint64_t)); 1226 uint64_t c00 = c0; 1227 uint64_t tmp[4U] = { 0U }; 1228 uint64_t c = (uint64_t)0U; 1229 { 1230 uint64_t t1 = res[(uint32_t)4U * (uint32_t)0U]; 1231 uint64_t t20 = n[(uint32_t)4U * (uint32_t)0U]; 1232 uint64_t *res_i0 = tmp + (uint32_t)4U * (uint32_t)0U; 1233 c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t1, t20, res_i0); 1234 uint64_t t10 = res[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U]; 1235 uint64_t t21 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U]; 1236 uint64_t *res_i1 = tmp + (uint32_t)4U * (uint32_t)0U + (uint32_t)1U; 1237 c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t10, t21, res_i1); 1238 uint64_t t11 = res[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U]; 1239 uint64_t t22 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U]; 1240 uint64_t *res_i2 = tmp + (uint32_t)4U * (uint32_t)0U + (uint32_t)2U; 1241 c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t11, t22, res_i2); 1242 uint64_t t12 = res[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U]; 1243 uint64_t t2 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U]; 1244 uint64_t *res_i = tmp + (uint32_t)4U * (uint32_t)0U + (uint32_t)3U; 1245 c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t12, t2, res_i); 1246 } 1247 uint64_t c1 = c; 1248 uint64_t c2 = c00 - c1; 1249 KRML_MAYBE_FOR4(i, 1250 (uint32_t)0U, 1251 (uint32_t)4U, 1252 (uint32_t)1U, 1253 uint64_t *os = res; 1254 uint64_t x1 = (c2 & res[i]) | (~c2 & tmp[i]); 1255 os[i] = x1;); 1256 } 1257 1258 static inline void 1259 from_qmont(uint64_t *res, uint64_t *x) 1260 { 1261 uint64_t tmp[8U] = { 0U }; 1262 memcpy(tmp, x, (uint32_t)4U * sizeof(uint64_t)); 1263 qmont_reduction(res, tmp); 1264 } 1265 1266 static inline void 1267 qmul(uint64_t *res, uint64_t *x, uint64_t *y) 1268 { 1269 uint64_t tmp[8U] = { 0U }; 1270 bn_mul4(tmp, x, y); 1271 qmont_reduction(res, tmp); 1272 } 1273 1274 static inline void 1275 qsqr(uint64_t *res, uint64_t *x) 1276 { 1277 uint64_t tmp[8U] = { 0U }; 1278 bn_sqr4(tmp, x); 1279 qmont_reduction(res, tmp); 1280 } 1281 1282 bool 1283 Hacl_Impl_P256_DH_ecp256dh_i(uint8_t *public_key, uint8_t *private_key) 1284 { 1285 uint64_t tmp[16U] = { 0U }; 1286 uint64_t *sk = tmp; 1287 uint64_t *pk = tmp + (uint32_t)4U; 1288 bn_from_bytes_be4(sk, private_key); 1289 uint64_t is_b_valid = bn_is_lt_order_and_gt_zero_mask4(sk); 1290 uint64_t oneq[4U] = { 0U }; 1291 oneq[0U] = (uint64_t)1U; 1292 oneq[1U] = (uint64_t)0U; 1293 oneq[2U] = (uint64_t)0U; 1294 oneq[3U] = (uint64_t)0U; 1295 KRML_MAYBE_FOR4(i, 1296 (uint32_t)0U, 1297 (uint32_t)4U, 1298 (uint32_t)1U, 1299 uint64_t *os = sk; 1300 uint64_t uu____0 = oneq[i]; 1301 uint64_t x = uu____0 ^ (is_b_valid & (sk[i] ^ uu____0)); 1302 os[i] = x;); 1303 uint64_t is_sk_valid = is_b_valid; 1304 point_mul_g(pk, sk); 1305 point_store(public_key, pk); 1306 return is_sk_valid == (uint64_t)0xFFFFFFFFFFFFFFFFU; 1307 } 1308 1309 bool 1310 Hacl_Impl_P256_DH_ecp256dh_r( 1311 uint8_t *shared_secret, 1312 uint8_t *their_pubkey, 1313 uint8_t *private_key) 1314 { 1315 uint64_t tmp[16U] = { 0U }; 1316 uint64_t *sk = tmp; 1317 uint64_t *pk = tmp + (uint32_t)4U; 1318 bool is_pk_valid = load_point_vartime(pk, their_pubkey); 1319 bn_from_bytes_be4(sk, private_key); 1320 uint64_t is_b_valid = bn_is_lt_order_and_gt_zero_mask4(sk); 1321 uint64_t oneq[4U] = { 0U }; 1322 oneq[0U] = (uint64_t)1U; 1323 oneq[1U] = (uint64_t)0U; 1324 oneq[2U] = (uint64_t)0U; 1325 oneq[3U] = (uint64_t)0U; 1326 KRML_MAYBE_FOR4(i, 1327 (uint32_t)0U, 1328 (uint32_t)4U, 1329 (uint32_t)1U, 1330 uint64_t *os = sk; 1331 uint64_t uu____0 = oneq[i]; 1332 uint64_t x = uu____0 ^ (is_b_valid & (sk[i] ^ uu____0)); 1333 os[i] = x;); 1334 uint64_t is_sk_valid = is_b_valid; 1335 uint64_t ss_proj[12U] = { 0U }; 1336 if (is_pk_valid) { 1337 point_mul(ss_proj, sk, pk); 1338 point_store(shared_secret, ss_proj); 1339 } 1340 return is_sk_valid == (uint64_t)0xFFFFFFFFFFFFFFFFU && is_pk_valid; 1341 } 1342 1343 static inline void 1344 qinv(uint64_t *res, uint64_t *r) 1345 { 1346 uint64_t tmp[28U] = { 0U }; 1347 uint64_t *x6 = tmp; 1348 uint64_t *x_11 = tmp + (uint32_t)4U; 1349 uint64_t *x_101 = tmp + (uint32_t)8U; 1350 uint64_t *x_111 = tmp + (uint32_t)12U; 1351 uint64_t *x_1111 = tmp + (uint32_t)16U; 1352 uint64_t *x_10101 = tmp + (uint32_t)20U; 1353 uint64_t *x_101111 = tmp + (uint32_t)24U; 1354 memcpy(x6, r, (uint32_t)4U * sizeof(uint64_t)); 1355 { 1356 qsqr(x6, x6); 1357 } 1358 qmul(x_11, x6, r); 1359 qmul(x_101, x6, x_11); 1360 qmul(x_111, x6, x_101); 1361 memcpy(x6, x_101, (uint32_t)4U * sizeof(uint64_t)); 1362 { 1363 qsqr(x6, x6); 1364 } 1365 qmul(x_1111, x_101, x6); 1366 { 1367 qsqr(x6, x6); 1368 } 1369 qmul(x_10101, x6, r); 1370 memcpy(x6, x_10101, (uint32_t)4U * sizeof(uint64_t)); 1371 { 1372 qsqr(x6, x6); 1373 } 1374 qmul(x_101111, x_101, x6); 1375 qmul(x6, x_10101, x6); 1376 uint64_t tmp1[4U] = { 0U }; 1377 KRML_MAYBE_FOR2(i, (uint32_t)0U, (uint32_t)2U, (uint32_t)1U, qsqr(x6, x6);); 1378 qmul(x6, x6, x_11); 1379 memcpy(tmp1, x6, (uint32_t)4U * sizeof(uint64_t)); 1380 KRML_MAYBE_FOR8(i, (uint32_t)0U, (uint32_t)8U, (uint32_t)1U, qsqr(tmp1, tmp1);); 1381 qmul(tmp1, tmp1, x6); 1382 memcpy(x6, tmp1, (uint32_t)4U * sizeof(uint64_t)); 1383 KRML_MAYBE_FOR16(i, (uint32_t)0U, (uint32_t)16U, (uint32_t)1U, qsqr(x6, x6);); 1384 qmul(x6, x6, tmp1); 1385 memcpy(tmp1, x6, (uint32_t)4U * sizeof(uint64_t)); 1386 for (uint32_t i = (uint32_t)0U; i < (uint32_t)64U; i++) { 1387 qsqr(tmp1, tmp1); 1388 } 1389 qmul(tmp1, tmp1, x6); 1390 for (uint32_t i = (uint32_t)0U; i < (uint32_t)32U; i++) { 1391 qsqr(tmp1, tmp1); 1392 } 1393 qmul(tmp1, tmp1, x6); 1394 KRML_MAYBE_FOR6(i, (uint32_t)0U, (uint32_t)6U, (uint32_t)1U, qsqr(tmp1, tmp1);); 1395 qmul(tmp1, tmp1, x_101111); 1396 KRML_MAYBE_FOR5(i, (uint32_t)0U, (uint32_t)5U, (uint32_t)1U, qsqr(tmp1, tmp1);); 1397 qmul(tmp1, tmp1, x_111); 1398 KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, qsqr(tmp1, tmp1);); 1399 qmul(tmp1, tmp1, x_11); 1400 KRML_MAYBE_FOR5(i, (uint32_t)0U, (uint32_t)5U, (uint32_t)1U, qsqr(tmp1, tmp1);); 1401 qmul(tmp1, tmp1, x_1111); 1402 KRML_MAYBE_FOR5(i, (uint32_t)0U, (uint32_t)5U, (uint32_t)1U, qsqr(tmp1, tmp1);); 1403 qmul(tmp1, tmp1, x_10101); 1404 KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, qsqr(tmp1, tmp1);); 1405 qmul(tmp1, tmp1, x_101); 1406 KRML_MAYBE_FOR3(i, (uint32_t)0U, (uint32_t)3U, (uint32_t)1U, qsqr(tmp1, tmp1);); 1407 qmul(tmp1, tmp1, x_101); 1408 KRML_MAYBE_FOR3(i, (uint32_t)0U, (uint32_t)3U, (uint32_t)1U, qsqr(tmp1, tmp1);); 1409 qmul(tmp1, tmp1, x_101); 1410 KRML_MAYBE_FOR5(i, (uint32_t)0U, (uint32_t)5U, (uint32_t)1U, qsqr(tmp1, tmp1);); 1411 qmul(tmp1, tmp1, x_111); 1412 KRML_MAYBE_FOR9(i, (uint32_t)0U, (uint32_t)9U, (uint32_t)1U, qsqr(tmp1, tmp1);); 1413 qmul(tmp1, tmp1, x_101111); 1414 KRML_MAYBE_FOR6(i, (uint32_t)0U, (uint32_t)6U, (uint32_t)1U, qsqr(tmp1, tmp1);); 1415 qmul(tmp1, tmp1, x_1111); 1416 KRML_MAYBE_FOR2(i, (uint32_t)0U, (uint32_t)2U, (uint32_t)1U, qsqr(tmp1, tmp1);); 1417 qmul(tmp1, tmp1, r); 1418 KRML_MAYBE_FOR5(i, (uint32_t)0U, (uint32_t)5U, (uint32_t)1U, qsqr(tmp1, tmp1);); 1419 qmul(tmp1, tmp1, r); 1420 KRML_MAYBE_FOR6(i, (uint32_t)0U, (uint32_t)6U, (uint32_t)1U, qsqr(tmp1, tmp1);); 1421 qmul(tmp1, tmp1, x_1111); 1422 KRML_MAYBE_FOR5(i, (uint32_t)0U, (uint32_t)5U, (uint32_t)1U, qsqr(tmp1, tmp1);); 1423 qmul(tmp1, tmp1, x_111); 1424 KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, qsqr(tmp1, tmp1);); 1425 qmul(tmp1, tmp1, x_111); 1426 KRML_MAYBE_FOR5(i, (uint32_t)0U, (uint32_t)5U, (uint32_t)1U, qsqr(tmp1, tmp1);); 1427 qmul(tmp1, tmp1, x_111); 1428 KRML_MAYBE_FOR5(i, (uint32_t)0U, (uint32_t)5U, (uint32_t)1U, qsqr(tmp1, tmp1);); 1429 qmul(tmp1, tmp1, x_101); 1430 KRML_MAYBE_FOR3(i, (uint32_t)0U, (uint32_t)3U, (uint32_t)1U, qsqr(tmp1, tmp1);); 1431 qmul(tmp1, tmp1, x_11); 1432 KRML_MAYBE_FOR10(i, (uint32_t)0U, (uint32_t)10U, (uint32_t)1U, qsqr(tmp1, tmp1);); 1433 qmul(tmp1, tmp1, x_101111); 1434 KRML_MAYBE_FOR2(i, (uint32_t)0U, (uint32_t)2U, (uint32_t)1U, qsqr(tmp1, tmp1);); 1435 qmul(tmp1, tmp1, x_11); 1436 KRML_MAYBE_FOR5(i, (uint32_t)0U, (uint32_t)5U, (uint32_t)1U, qsqr(tmp1, tmp1);); 1437 qmul(tmp1, tmp1, x_11); 1438 KRML_MAYBE_FOR5(i, (uint32_t)0U, (uint32_t)5U, (uint32_t)1U, qsqr(tmp1, tmp1);); 1439 qmul(tmp1, tmp1, x_11); 1440 KRML_MAYBE_FOR3(i, (uint32_t)0U, (uint32_t)3U, (uint32_t)1U, qsqr(tmp1, tmp1);); 1441 qmul(tmp1, tmp1, r); 1442 KRML_MAYBE_FOR7(i, (uint32_t)0U, (uint32_t)7U, (uint32_t)1U, qsqr(tmp1, tmp1);); 1443 qmul(tmp1, tmp1, x_10101); 1444 KRML_MAYBE_FOR6(i, (uint32_t)0U, (uint32_t)6U, (uint32_t)1U, qsqr(tmp1, tmp1);); 1445 qmul(tmp1, tmp1, x_1111); 1446 memcpy(x6, tmp1, (uint32_t)4U * sizeof(uint64_t)); 1447 memcpy(res, x6, (uint32_t)4U * sizeof(uint64_t)); 1448 } 1449 1450 static inline void 1451 qmul_mont(uint64_t *sinv, uint64_t *b, uint64_t *res) 1452 { 1453 uint64_t tmp[4U] = { 0U }; 1454 from_qmont(tmp, b); 1455 qmul(res, sinv, tmp); 1456 } 1457 1458 static inline bool 1459 ecdsa_verify_msg_as_qelem( 1460 uint64_t *m_q, 1461 uint8_t *public_key, 1462 uint8_t *signature_r, 1463 uint8_t *signature_s) 1464 { 1465 uint64_t tmp[28U] = { 0U }; 1466 uint64_t *pk = tmp; 1467 uint64_t *r_q = tmp + (uint32_t)12U; 1468 uint64_t *s_q = tmp + (uint32_t)16U; 1469 uint64_t *u1 = tmp + (uint32_t)20U; 1470 uint64_t *u2 = tmp + (uint32_t)24U; 1471 bool is_pk_valid = load_point_vartime(pk, public_key); 1472 bn_from_bytes_be4(r_q, signature_r); 1473 bn_from_bytes_be4(s_q, signature_s); 1474 uint64_t is_r_valid = bn_is_lt_order_and_gt_zero_mask4(r_q); 1475 uint64_t is_s_valid = bn_is_lt_order_and_gt_zero_mask4(s_q); 1476 bool 1477 is_rs_valid = 1478 is_r_valid == (uint64_t)0xFFFFFFFFFFFFFFFFU && is_s_valid == (uint64_t)0xFFFFFFFFFFFFFFFFU; 1479 if (!(is_pk_valid && is_rs_valid)) { 1480 return false; 1481 } 1482 uint64_t sinv[4U] = { 0U }; 1483 qinv(sinv, s_q); 1484 qmul_mont(sinv, m_q, u1); 1485 qmul_mont(sinv, r_q, u2); 1486 uint64_t res[12U] = { 0U }; 1487 point_mul_double_g(res, u1, u2, pk); 1488 if (is_point_at_inf_vartime(res)) { 1489 return false; 1490 } 1491 uint64_t x[4U] = { 0U }; 1492 to_aff_point_x(x, res); 1493 qmod_short(x, x); 1494 bool res1 = bn_is_eq_vartime4(x, r_q); 1495 return res1; 1496 } 1497 1498 static inline bool 1499 ecdsa_sign_msg_as_qelem( 1500 uint8_t *signature, 1501 uint64_t *m_q, 1502 uint8_t *private_key, 1503 uint8_t *nonce) 1504 { 1505 uint64_t rsdk_q[16U] = { 0U }; 1506 uint64_t *r_q = rsdk_q; 1507 uint64_t *s_q = rsdk_q + (uint32_t)4U; 1508 uint64_t *d_a = rsdk_q + (uint32_t)8U; 1509 uint64_t *k_q = rsdk_q + (uint32_t)12U; 1510 bn_from_bytes_be4(d_a, private_key); 1511 uint64_t is_b_valid0 = bn_is_lt_order_and_gt_zero_mask4(d_a); 1512 uint64_t oneq0[4U] = { 0U }; 1513 oneq0[0U] = (uint64_t)1U; 1514 oneq0[1U] = (uint64_t)0U; 1515 oneq0[2U] = (uint64_t)0U; 1516 oneq0[3U] = (uint64_t)0U; 1517 KRML_MAYBE_FOR4(i, 1518 (uint32_t)0U, 1519 (uint32_t)4U, 1520 (uint32_t)1U, 1521 uint64_t *os = d_a; 1522 uint64_t uu____0 = oneq0[i]; 1523 uint64_t x = uu____0 ^ (is_b_valid0 & (d_a[i] ^ uu____0)); 1524 os[i] = x;); 1525 uint64_t is_sk_valid = is_b_valid0; 1526 bn_from_bytes_be4(k_q, nonce); 1527 uint64_t is_b_valid = bn_is_lt_order_and_gt_zero_mask4(k_q); 1528 uint64_t oneq[4U] = { 0U }; 1529 oneq[0U] = (uint64_t)1U; 1530 oneq[1U] = (uint64_t)0U; 1531 oneq[2U] = (uint64_t)0U; 1532 oneq[3U] = (uint64_t)0U; 1533 KRML_MAYBE_FOR4(i, 1534 (uint32_t)0U, 1535 (uint32_t)4U, 1536 (uint32_t)1U, 1537 uint64_t *os = k_q; 1538 uint64_t uu____1 = oneq[i]; 1539 uint64_t x = uu____1 ^ (is_b_valid & (k_q[i] ^ uu____1)); 1540 os[i] = x;); 1541 uint64_t is_nonce_valid = is_b_valid; 1542 uint64_t are_sk_nonce_valid = is_sk_valid & is_nonce_valid; 1543 uint64_t p[12U] = { 0U }; 1544 point_mul_g(p, k_q); 1545 to_aff_point_x(r_q, p); 1546 qmod_short(r_q, r_q); 1547 uint64_t kinv[4U] = { 0U }; 1548 qinv(kinv, k_q); 1549 qmul(s_q, r_q, d_a); 1550 from_qmont(m_q, m_q); 1551 qadd(s_q, m_q, s_q); 1552 qmul(s_q, kinv, s_q); 1553 bn2_to_bytes_be4(signature, r_q, s_q); 1554 uint64_t is_r_zero = bn_is_zero_mask4(r_q); 1555 uint64_t is_s_zero = bn_is_zero_mask4(s_q); 1556 uint64_t m = are_sk_nonce_valid & (~is_r_zero & ~is_s_zero); 1557 bool res = m == (uint64_t)0xFFFFFFFFFFFFFFFFU; 1558 return res; 1559 } 1560 1561 /******************************************************************************* 1562 1563 Verified C library for ECDSA and ECDH functions over the P-256 NIST curve. 1564 1565 This module implements signing and verification, key validation, conversions 1566 between various point representations, and ECDH key agreement. 1567 1568 *******************************************************************************/ 1569 1570 /*****************/ 1571 /* ECDSA signing */ 1572 /*****************/ 1573 1574 /** 1575 Create an ECDSA signature WITHOUT hashing first. 1576 1577 This function is intended to receive a hash of the input. 1578 For convenience, we recommend using one of the hash-and-sign combined functions above. 1579 1580 The argument `msg` MUST be at least 32 bytes (i.e. `msg_len >= 32`). 1581 1582 NOTE: The equivalent functions in OpenSSL and Fiat-Crypto both accept inputs 1583 smaller than 32 bytes. These libraries left-pad the input with enough zeroes to 1584 reach the minimum 32 byte size. Clients who need behavior identical to OpenSSL 1585 need to perform the left-padding themselves. 1586 1587 The function returns `true` for successful creation of an ECDSA signature and `false` otherwise. 1588 1589 The outparam `signature` (R || S) points to 64 bytes of valid memory, i.e., uint8_t[64]. 1590 The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len]. 1591 The arguments `private_key` and `nonce` point to 32 bytes of valid memory, i.e., uint8_t[32]. 1592 1593 The function also checks whether `private_key` and `nonce` are valid values: 1594 • 0 < `private_key` < the order of the curve 1595 • 0 < `nonce` < the order of the curve 1596 */ 1597 bool 1598 Hacl_P256_ecdsa_sign_p256_without_hash( 1599 uint8_t *signature, 1600 uint32_t msg_len, 1601 uint8_t *msg, 1602 uint8_t *private_key, 1603 uint8_t *nonce) 1604 { 1605 uint64_t m_q[4U] = { 0U }; 1606 uint8_t mHash[32U] = { 0U }; 1607 memcpy(mHash, msg, (uint32_t)32U * sizeof(uint8_t)); 1608 KRML_HOST_IGNORE(msg_len); 1609 uint8_t *mHash32 = mHash; 1610 bn_from_bytes_be4(m_q, mHash32); 1611 qmod_short(m_q, m_q); 1612 bool res = ecdsa_sign_msg_as_qelem(signature, m_q, private_key, nonce); 1613 return res; 1614 } 1615 1616 /**********************/ 1617 /* ECDSA verification */ 1618 /**********************/ 1619 1620 /** 1621 Verify an ECDSA signature WITHOUT hashing first. 1622 1623 This function is intended to receive a hash of the input. 1624 For convenience, we recommend using one of the hash-and-verify combined functions above. 1625 1626 The argument `msg` MUST be at least 32 bytes (i.e. `msg_len >= 32`). 1627 1628 The function returns `true` if the signature is valid and `false` otherwise. 1629 1630 The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len]. 1631 The argument `public_key` (x || y) points to 64 bytes of valid memory, i.e., uint8_t[64]. 1632 The arguments `signature_r` and `signature_s` point to 32 bytes of valid memory, i.e., uint8_t[32]. 1633 1634 The function also checks whether `public_key` is valid 1635 */ 1636 bool 1637 Hacl_P256_ecdsa_verif_without_hash( 1638 uint32_t msg_len, 1639 uint8_t *msg, 1640 uint8_t *public_key, 1641 uint8_t *signature_r, 1642 uint8_t *signature_s) 1643 { 1644 uint64_t m_q[4U] = { 0U }; 1645 uint8_t mHash[32U] = { 0U }; 1646 memcpy(mHash, msg, (uint32_t)32U * sizeof(uint8_t)); 1647 KRML_HOST_IGNORE(msg_len); 1648 uint8_t *mHash32 = mHash; 1649 bn_from_bytes_be4(m_q, mHash32); 1650 qmod_short(m_q, m_q); 1651 bool res = ecdsa_verify_msg_as_qelem(m_q, public_key, signature_r, signature_s); 1652 return res; 1653 } 1654 1655 /******************/ 1656 /* Key validation */ 1657 /******************/ 1658 1659 /** 1660 Public key validation. 1661 1662 The function returns `true` if a public key is valid and `false` otherwise. 1663 1664 The argument `public_key` points to 64 bytes of valid memory, i.e., uint8_t[64]. 1665 1666 The public key (x || y) is valid (with respect to SP 800-56A): 1667 • the public key is not the “point at infinity”, represented as O. 1668 • the affine x and y coordinates of the point represented by the public key are 1669 in the range [0, p – 1] where p is the prime defining the finite field. 1670 • y^2 = x^3 + ax + b where a and b are the coefficients of the curve equation. 1671 The last extract is taken from: https://neilmadden.blog/2017/05/17/so-how-do-you-validate-nist-ecdh-public-keys/ 1672 */ 1673 bool 1674 Hacl_P256_validate_public_key(uint8_t *public_key) 1675 { 1676 uint64_t point_jac[12U] = { 0U }; 1677 bool res = load_point_vartime(point_jac, public_key); 1678 return res; 1679 } 1680 1681 /** 1682 Private key validation. 1683 1684 The function returns `true` if a private key is valid and `false` otherwise. 1685 1686 The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32]. 1687 1688 The private key is valid: 1689 • 0 < `private_key` < the order of the curve 1690 */ 1691 bool 1692 Hacl_P256_validate_private_key(uint8_t *private_key) 1693 { 1694 uint64_t bn_sk[4U] = { 0U }; 1695 bn_from_bytes_be4(bn_sk, private_key); 1696 uint64_t res = bn_is_lt_order_and_gt_zero_mask4(bn_sk); 1697 return res == (uint64_t)0xFFFFFFFFFFFFFFFFU; 1698 } 1699 1700 /******************************************************************************* 1701 Parsing and Serializing public keys. 1702 1703 A public key is a point (x, y) on the P-256 NIST curve. 1704 1705 The point can be represented in the following three ways. 1706 • raw = [ x || y ], 64 bytes 1707 • uncompressed = [ 0x04 || x || y ], 65 bytes 1708 • compressed = [ (0x02 for even `y` and 0x03 for odd `y`) || x ], 33 bytes 1709 1710 *******************************************************************************/ 1711 1712 /** 1713 Convert a public key from uncompressed to its raw form. 1714 1715 The function returns `true` for successful conversion of a public key and `false` otherwise. 1716 1717 The outparam `pk_raw` points to 64 bytes of valid memory, i.e., uint8_t[64]. 1718 The argument `pk` points to 65 bytes of valid memory, i.e., uint8_t[65]. 1719 1720 The function DOESN'T check whether (x, y) is a valid point. 1721 */ 1722 bool 1723 Hacl_P256_uncompressed_to_raw(uint8_t *pk, uint8_t *pk_raw) 1724 { 1725 uint8_t pk0 = pk[0U]; 1726 if (pk0 != (uint8_t)0x04U) { 1727 return false; 1728 } 1729 memcpy(pk_raw, pk + (uint32_t)1U, (uint32_t)64U * sizeof(uint8_t)); 1730 return true; 1731 } 1732 1733 /** 1734 Convert a public key from compressed to its raw form. 1735 1736 The function returns `true` for successful conversion of a public key and `false` otherwise. 1737 1738 The outparam `pk_raw` points to 64 bytes of valid memory, i.e., uint8_t[64]. 1739 The argument `pk` points to 33 bytes of valid memory, i.e., uint8_t[33]. 1740 1741 The function also checks whether (x, y) is a valid point. 1742 */ 1743 bool 1744 Hacl_P256_compressed_to_raw(uint8_t *pk, uint8_t *pk_raw) 1745 { 1746 uint64_t xa[4U] = { 0U }; 1747 uint64_t ya[4U] = { 0U }; 1748 uint8_t *pk_xb = pk + (uint32_t)1U; 1749 bool b = aff_point_decompress_vartime(xa, ya, pk); 1750 if (b) { 1751 memcpy(pk_raw, pk_xb, (uint32_t)32U * sizeof(uint8_t)); 1752 bn_to_bytes_be4(pk_raw + (uint32_t)32U, ya); 1753 } 1754 return b; 1755 } 1756 1757 /** 1758 Convert a public key from raw to its uncompressed form. 1759 1760 The outparam `pk` points to 65 bytes of valid memory, i.e., uint8_t[65]. 1761 The argument `pk_raw` points to 64 bytes of valid memory, i.e., uint8_t[64]. 1762 1763 The function DOESN'T check whether (x, y) is a valid point. 1764 */ 1765 void 1766 Hacl_P256_raw_to_uncompressed(uint8_t *pk_raw, uint8_t *pk) 1767 { 1768 pk[0U] = (uint8_t)0x04U; 1769 memcpy(pk + (uint32_t)1U, pk_raw, (uint32_t)64U * sizeof(uint8_t)); 1770 } 1771 1772 /** 1773 Convert a public key from raw to its compressed form. 1774 1775 The outparam `pk` points to 33 bytes of valid memory, i.e., uint8_t[33]. 1776 The argument `pk_raw` points to 64 bytes of valid memory, i.e., uint8_t[64]. 1777 1778 The function DOESN'T check whether (x, y) is a valid point. 1779 */ 1780 void 1781 Hacl_P256_raw_to_compressed(uint8_t *pk_raw, uint8_t *pk) 1782 { 1783 uint8_t *pk_x = pk_raw; 1784 uint8_t *pk_y = pk_raw + (uint32_t)32U; 1785 uint64_t bn_f[4U] = { 0U }; 1786 bn_from_bytes_be4(bn_f, pk_y); 1787 uint64_t is_odd_f = bn_f[0U] & (uint64_t)1U; 1788 pk[0U] = (uint8_t)is_odd_f + (uint8_t)0x02U; 1789 memcpy(pk + (uint32_t)1U, pk_x, (uint32_t)32U * sizeof(uint8_t)); 1790 } 1791 1792 /******************/ 1793 /* ECDH agreement */ 1794 /******************/ 1795 1796 /** 1797 Compute the public key from the private key. 1798 1799 The function returns `true` if a private key is valid and `false` otherwise. 1800 1801 The outparam `public_key` points to 64 bytes of valid memory, i.e., uint8_t[64]. 1802 The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32]. 1803 1804 The private key is valid: 1805 • 0 < `private_key` < the order of the curve. 1806 */ 1807 bool 1808 Hacl_P256_dh_initiator(uint8_t *public_key, uint8_t *private_key) 1809 { 1810 return Hacl_Impl_P256_DH_ecp256dh_i(public_key, private_key); 1811 } 1812 1813 /** 1814 Execute the diffie-hellmann key exchange. 1815 1816 The function returns `true` for successful creation of an ECDH shared secret and 1817 `false` otherwise. 1818 1819 The outparam `shared_secret` points to 64 bytes of valid memory, i.e., uint8_t[64]. 1820 The argument `their_pubkey` points to 64 bytes of valid memory, i.e., uint8_t[64]. 1821 The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32]. 1822 1823 The function also checks whether `private_key` and `their_pubkey` are valid. 1824 */ 1825 bool 1826 Hacl_P256_dh_responder(uint8_t *shared_secret, uint8_t *their_pubkey, uint8_t *private_key) 1827 { 1828 return Hacl_Impl_P256_DH_ecp256dh_r(shared_secret, their_pubkey, private_key); 1829 }