Hacl_P384.c (54615B)
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 "Hacl_P384.h" 26 27 #include "internal/Hacl_Krmllib.h" 28 #include "internal/Hacl_Bignum_Base.h" 29 30 static inline uint64_t 31 bn_is_eq_mask(uint64_t *x, uint64_t *y) 32 { 33 uint64_t mask = 0xFFFFFFFFFFFFFFFFULL; 34 KRML_MAYBE_FOR6(i, 35 0U, 36 6U, 37 1U, 38 uint64_t uu____0 = FStar_UInt64_eq_mask(x[i], y[i]); 39 mask = uu____0 & mask;); 40 uint64_t mask1 = mask; 41 return mask1; 42 } 43 44 static inline void 45 bn_cmovznz(uint64_t *a, uint64_t b, uint64_t *c, uint64_t *d) 46 { 47 uint64_t mask = ~FStar_UInt64_eq_mask(b, 0ULL); 48 KRML_MAYBE_FOR6(i, 49 0U, 50 6U, 51 1U, 52 uint64_t *os = a; 53 uint64_t uu____0 = c[i]; 54 uint64_t x = uu____0 ^ (mask & (d[i] ^ uu____0)); 55 os[i] = x;); 56 } 57 58 static inline void 59 bn_add_mod(uint64_t *a, uint64_t *b, uint64_t *c, uint64_t *d) 60 { 61 uint64_t c10 = 0ULL; 62 { 63 uint64_t t1 = c[4U * 0U]; 64 uint64_t t20 = d[4U * 0U]; 65 uint64_t *res_i0 = a + 4U * 0U; 66 c10 = Lib_IntTypes_Intrinsics_add_carry_u64(c10, t1, t20, res_i0); 67 uint64_t t10 = c[4U * 0U + 1U]; 68 uint64_t t21 = d[4U * 0U + 1U]; 69 uint64_t *res_i1 = a + 4U * 0U + 1U; 70 c10 = Lib_IntTypes_Intrinsics_add_carry_u64(c10, t10, t21, res_i1); 71 uint64_t t11 = c[4U * 0U + 2U]; 72 uint64_t t22 = d[4U * 0U + 2U]; 73 uint64_t *res_i2 = a + 4U * 0U + 2U; 74 c10 = Lib_IntTypes_Intrinsics_add_carry_u64(c10, t11, t22, res_i2); 75 uint64_t t12 = c[4U * 0U + 3U]; 76 uint64_t t2 = d[4U * 0U + 3U]; 77 uint64_t *res_i = a + 4U * 0U + 3U; 78 c10 = Lib_IntTypes_Intrinsics_add_carry_u64(c10, t12, t2, res_i); 79 } 80 KRML_MAYBE_FOR2(i, 81 4U, 82 6U, 83 1U, 84 uint64_t t1 = c[i]; 85 uint64_t t2 = d[i]; 86 uint64_t *res_i = a + i; 87 c10 = Lib_IntTypes_Intrinsics_add_carry_u64(c10, t1, t2, res_i);); 88 uint64_t c0 = c10; 89 uint64_t tmp[6U] = { 0U }; 90 uint64_t c1 = 0ULL; 91 { 92 uint64_t t1 = a[4U * 0U]; 93 uint64_t t20 = b[4U * 0U]; 94 uint64_t *res_i0 = tmp + 4U * 0U; 95 c1 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c1, t1, t20, res_i0); 96 uint64_t t10 = a[4U * 0U + 1U]; 97 uint64_t t21 = b[4U * 0U + 1U]; 98 uint64_t *res_i1 = tmp + 4U * 0U + 1U; 99 c1 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c1, t10, t21, res_i1); 100 uint64_t t11 = a[4U * 0U + 2U]; 101 uint64_t t22 = b[4U * 0U + 2U]; 102 uint64_t *res_i2 = tmp + 4U * 0U + 2U; 103 c1 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c1, t11, t22, res_i2); 104 uint64_t t12 = a[4U * 0U + 3U]; 105 uint64_t t2 = b[4U * 0U + 3U]; 106 uint64_t *res_i = tmp + 4U * 0U + 3U; 107 c1 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c1, t12, t2, res_i); 108 } 109 KRML_MAYBE_FOR2(i, 110 4U, 111 6U, 112 1U, 113 uint64_t t1 = a[i]; 114 uint64_t t2 = b[i]; 115 uint64_t *res_i = tmp + i; 116 c1 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c1, t1, t2, res_i);); 117 uint64_t c11 = c1; 118 uint64_t c2 = c0 - c11; 119 KRML_MAYBE_FOR6(i, 120 0U, 121 6U, 122 1U, 123 uint64_t *os = a; 124 uint64_t x = (c2 & a[i]) | (~c2 & tmp[i]); 125 os[i] = x;); 126 } 127 128 static inline uint64_t 129 bn_sub(uint64_t *a, uint64_t *b, uint64_t *c) 130 { 131 uint64_t c1 = 0ULL; 132 { 133 uint64_t t1 = b[4U * 0U]; 134 uint64_t t20 = c[4U * 0U]; 135 uint64_t *res_i0 = a + 4U * 0U; 136 c1 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c1, t1, t20, res_i0); 137 uint64_t t10 = b[4U * 0U + 1U]; 138 uint64_t t21 = c[4U * 0U + 1U]; 139 uint64_t *res_i1 = a + 4U * 0U + 1U; 140 c1 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c1, t10, t21, res_i1); 141 uint64_t t11 = b[4U * 0U + 2U]; 142 uint64_t t22 = c[4U * 0U + 2U]; 143 uint64_t *res_i2 = a + 4U * 0U + 2U; 144 c1 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c1, t11, t22, res_i2); 145 uint64_t t12 = b[4U * 0U + 3U]; 146 uint64_t t2 = c[4U * 0U + 3U]; 147 uint64_t *res_i = a + 4U * 0U + 3U; 148 c1 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c1, t12, t2, res_i); 149 } 150 KRML_MAYBE_FOR2(i, 151 4U, 152 6U, 153 1U, 154 uint64_t t1 = b[i]; 155 uint64_t t2 = c[i]; 156 uint64_t *res_i = a + i; 157 c1 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c1, t1, t2, res_i);); 158 uint64_t c10 = c1; 159 return c10; 160 } 161 162 static inline void 163 bn_sub_mod(uint64_t *a, uint64_t *b, uint64_t *c, uint64_t *d) 164 { 165 uint64_t c10 = 0ULL; 166 { 167 uint64_t t1 = c[4U * 0U]; 168 uint64_t t20 = d[4U * 0U]; 169 uint64_t *res_i0 = a + 4U * 0U; 170 c10 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c10, t1, t20, res_i0); 171 uint64_t t10 = c[4U * 0U + 1U]; 172 uint64_t t21 = d[4U * 0U + 1U]; 173 uint64_t *res_i1 = a + 4U * 0U + 1U; 174 c10 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c10, t10, t21, res_i1); 175 uint64_t t11 = c[4U * 0U + 2U]; 176 uint64_t t22 = d[4U * 0U + 2U]; 177 uint64_t *res_i2 = a + 4U * 0U + 2U; 178 c10 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c10, t11, t22, res_i2); 179 uint64_t t12 = c[4U * 0U + 3U]; 180 uint64_t t2 = d[4U * 0U + 3U]; 181 uint64_t *res_i = a + 4U * 0U + 3U; 182 c10 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c10, t12, t2, res_i); 183 } 184 KRML_MAYBE_FOR2(i, 185 4U, 186 6U, 187 1U, 188 uint64_t t1 = c[i]; 189 uint64_t t2 = d[i]; 190 uint64_t *res_i = a + i; 191 c10 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c10, t1, t2, res_i);); 192 uint64_t c0 = c10; 193 uint64_t tmp[6U] = { 0U }; 194 uint64_t c1 = 0ULL; 195 { 196 uint64_t t1 = a[4U * 0U]; 197 uint64_t t20 = b[4U * 0U]; 198 uint64_t *res_i0 = tmp + 4U * 0U; 199 c1 = Lib_IntTypes_Intrinsics_add_carry_u64(c1, t1, t20, res_i0); 200 uint64_t t10 = a[4U * 0U + 1U]; 201 uint64_t t21 = b[4U * 0U + 1U]; 202 uint64_t *res_i1 = tmp + 4U * 0U + 1U; 203 c1 = Lib_IntTypes_Intrinsics_add_carry_u64(c1, t10, t21, res_i1); 204 uint64_t t11 = a[4U * 0U + 2U]; 205 uint64_t t22 = b[4U * 0U + 2U]; 206 uint64_t *res_i2 = tmp + 4U * 0U + 2U; 207 c1 = Lib_IntTypes_Intrinsics_add_carry_u64(c1, t11, t22, res_i2); 208 uint64_t t12 = a[4U * 0U + 3U]; 209 uint64_t t2 = b[4U * 0U + 3U]; 210 uint64_t *res_i = tmp + 4U * 0U + 3U; 211 c1 = Lib_IntTypes_Intrinsics_add_carry_u64(c1, t12, t2, res_i); 212 } 213 KRML_MAYBE_FOR2(i, 214 4U, 215 6U, 216 1U, 217 uint64_t t1 = a[i]; 218 uint64_t t2 = b[i]; 219 uint64_t *res_i = tmp + i; 220 c1 = Lib_IntTypes_Intrinsics_add_carry_u64(c1, t1, t2, res_i);); 221 uint64_t c11 = c1; 222 KRML_MAYBE_UNUSED_VAR(c11); 223 uint64_t c2 = 0ULL - c0; 224 KRML_MAYBE_FOR6(i, 225 0U, 226 6U, 227 1U, 228 uint64_t *os = a; 229 uint64_t x = (c2 & tmp[i]) | (~c2 & a[i]); 230 os[i] = x;); 231 } 232 233 static inline void 234 bn_mul(uint64_t *a, uint64_t *b, uint64_t *c) 235 { 236 memset(a, 0U, 12U * sizeof(uint64_t)); 237 KRML_MAYBE_FOR6( 238 i0, 239 0U, 240 6U, 241 1U, 242 uint64_t bj = c[i0]; 243 uint64_t *res_j = a + i0; 244 uint64_t c1 = 0ULL; 245 { 246 uint64_t a_i = b[4U * 0U]; 247 uint64_t *res_i0 = res_j + 4U * 0U; 248 c1 = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, bj, c1, res_i0); 249 uint64_t a_i0 = b[4U * 0U + 1U]; 250 uint64_t *res_i1 = res_j + 4U * 0U + 1U; 251 c1 = Hacl_Bignum_Base_mul_wide_add2_u64(a_i0, bj, c1, res_i1); 252 uint64_t a_i1 = b[4U * 0U + 2U]; 253 uint64_t *res_i2 = res_j + 4U * 0U + 2U; 254 c1 = Hacl_Bignum_Base_mul_wide_add2_u64(a_i1, bj, c1, res_i2); 255 uint64_t a_i2 = b[4U * 0U + 3U]; 256 uint64_t *res_i = res_j + 4U * 0U + 3U; 257 c1 = Hacl_Bignum_Base_mul_wide_add2_u64(a_i2, bj, c1, res_i); 258 } KRML_MAYBE_FOR2(i, 259 4U, 260 6U, 261 1U, 262 uint64_t a_i = b[i]; 263 uint64_t *res_i = res_j + i; 264 c1 = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, bj, c1, res_i);); 265 uint64_t r = c1; 266 a[6U + i0] = r;); 267 } 268 269 static inline void 270 bn_sqr(uint64_t *a, uint64_t *b) 271 { 272 memset(a, 0U, 12U * sizeof(uint64_t)); 273 KRML_MAYBE_FOR6( 274 i0, 275 0U, 276 6U, 277 1U, 278 uint64_t *ab = b; 279 uint64_t a_j = b[i0]; 280 uint64_t *res_j = a + i0; 281 uint64_t c = 0ULL; 282 for (uint32_t i = 0U; i < i0 / 4U; i++) { 283 uint64_t a_i = ab[4U * i]; 284 uint64_t *res_i0 = res_j + 4U * i; 285 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, a_j, c, res_i0); 286 uint64_t a_i0 = ab[4U * i + 1U]; 287 uint64_t *res_i1 = res_j + 4U * i + 1U; 288 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i0, a_j, c, res_i1); 289 uint64_t a_i1 = ab[4U * i + 2U]; 290 uint64_t *res_i2 = res_j + 4U * i + 2U; 291 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i1, a_j, c, res_i2); 292 uint64_t a_i2 = ab[4U * i + 3U]; 293 uint64_t *res_i = res_j + 4U * i + 3U; 294 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i2, a_j, c, res_i); 295 } for (uint32_t i = i0 / 4U * 4U; i < i0; i++) { 296 uint64_t a_i = ab[i]; 297 uint64_t *res_i = res_j + i; 298 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, a_j, c, res_i); 299 } uint64_t r = c; 300 a[i0 + i0] = r;); 301 uint64_t c0 = Hacl_Bignum_Addition_bn_add_eq_len_u64(12U, a, a, a); 302 KRML_MAYBE_UNUSED_VAR(c0); 303 uint64_t tmp[12U] = { 0U }; 304 KRML_MAYBE_FOR6(i, 305 0U, 306 6U, 307 1U, 308 FStar_UInt128_uint128 res = FStar_UInt128_mul_wide(b[i], b[i]); 309 uint64_t hi = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(res, 64U)); 310 uint64_t lo = FStar_UInt128_uint128_to_uint64(res); 311 tmp[2U * i] = lo; 312 tmp[2U * i + 1U] = hi;); 313 uint64_t c1 = Hacl_Bignum_Addition_bn_add_eq_len_u64(12U, a, tmp, a); 314 KRML_MAYBE_UNUSED_VAR(c1); 315 } 316 317 static inline void 318 bn_to_bytes_be(uint8_t *a, uint64_t *b) 319 { 320 uint8_t tmp[48U] = { 0U }; 321 KRML_MAYBE_UNUSED_VAR(tmp); 322 KRML_MAYBE_FOR6(i, 0U, 6U, 1U, store64_be(a + i * 8U, b[6U - i - 1U]);); 323 } 324 325 static inline void 326 bn_from_bytes_be(uint64_t *a, uint8_t *b) 327 { 328 KRML_MAYBE_FOR6(i, 329 0U, 330 6U, 331 1U, 332 uint64_t *os = a; 333 uint64_t u = load64_be(b + (6U - i - 1U) * 8U); 334 uint64_t x = u; 335 os[i] = x;); 336 } 337 338 static inline void 339 p384_make_prime(uint64_t *n) 340 { 341 n[0U] = 0x00000000ffffffffULL; 342 n[1U] = 0xffffffff00000000ULL; 343 n[2U] = 0xfffffffffffffffeULL; 344 n[3U] = 0xffffffffffffffffULL; 345 n[4U] = 0xffffffffffffffffULL; 346 n[5U] = 0xffffffffffffffffULL; 347 } 348 349 static inline void 350 p384_make_order(uint64_t *n) 351 { 352 n[0U] = 0xecec196accc52973ULL; 353 n[1U] = 0x581a0db248b0a77aULL; 354 n[2U] = 0xc7634d81f4372ddfULL; 355 n[3U] = 0xffffffffffffffffULL; 356 n[4U] = 0xffffffffffffffffULL; 357 n[5U] = 0xffffffffffffffffULL; 358 } 359 360 static inline void 361 p384_make_a_coeff(uint64_t *a) 362 { 363 a[0U] = 0x00000003fffffffcULL; 364 a[1U] = 0xfffffffc00000000ULL; 365 a[2U] = 0xfffffffffffffffbULL; 366 a[3U] = 0xffffffffffffffffULL; 367 a[4U] = 0xffffffffffffffffULL; 368 a[5U] = 0xffffffffffffffffULL; 369 } 370 371 static inline void 372 p384_make_b_coeff(uint64_t *b) 373 { 374 b[0U] = 0x081188719d412dccULL; 375 b[1U] = 0xf729add87a4c32ecULL; 376 b[2U] = 0x77f2209b1920022eULL; 377 b[3U] = 0xe3374bee94938ae2ULL; 378 b[4U] = 0xb62b21f41f022094ULL; 379 b[5U] = 0xcd08114b604fbff9ULL; 380 } 381 382 static inline void 383 p384_make_g_x(uint64_t *n) 384 { 385 n[0U] = 0x3dd0756649c0b528ULL; 386 n[1U] = 0x20e378e2a0d6ce38ULL; 387 n[2U] = 0x879c3afc541b4d6eULL; 388 n[3U] = 0x6454868459a30effULL; 389 n[4U] = 0x812ff723614ede2bULL; 390 n[5U] = 0x4d3aadc2299e1513ULL; 391 } 392 393 static inline void 394 p384_make_g_y(uint64_t *n) 395 { 396 n[0U] = 0x23043dad4b03a4feULL; 397 n[1U] = 0xa1bfa8bf7bb4a9acULL; 398 n[2U] = 0x8bade7562e83b050ULL; 399 n[3U] = 0xc6c3521968f4ffd9ULL; 400 n[4U] = 0xdd8002263969a840ULL; 401 n[5U] = 0x2b78abc25a15c5e9ULL; 402 } 403 404 static inline void 405 p384_make_fmont_R2(uint64_t *n) 406 { 407 n[0U] = 0xfffffffe00000001ULL; 408 n[1U] = 0x0000000200000000ULL; 409 n[2U] = 0xfffffffe00000000ULL; 410 n[3U] = 0x0000000200000000ULL; 411 n[4U] = 0x0000000000000001ULL; 412 n[5U] = 0x0ULL; 413 } 414 415 static inline void 416 p384_make_fzero(uint64_t *n) 417 { 418 memset(n, 0U, 6U * sizeof(uint64_t)); 419 n[0U] = 0ULL; 420 } 421 422 static inline void 423 p384_make_fone(uint64_t *n) 424 { 425 n[0U] = 0xffffffff00000001ULL; 426 n[1U] = 0x00000000ffffffffULL; 427 n[2U] = 0x1ULL; 428 n[3U] = 0x0ULL; 429 n[4U] = 0x0ULL; 430 n[5U] = 0x0ULL; 431 } 432 433 static inline void 434 p384_make_qone(uint64_t *f) 435 { 436 f[0U] = 0x1313e695333ad68dULL; 437 f[1U] = 0xa7e5f24db74f5885ULL; 438 f[2U] = 0x389cb27e0bc8d220ULL; 439 f[3U] = 0x0ULL; 440 f[4U] = 0x0ULL; 441 f[5U] = 0x0ULL; 442 } 443 444 static inline void 445 fmont_reduction(uint64_t *res, uint64_t *x) 446 { 447 uint64_t n[6U] = { 0U }; 448 p384_make_prime(n); 449 uint64_t c0 = 0ULL; 450 KRML_MAYBE_FOR6( 451 i0, 452 0U, 453 6U, 454 1U, 455 uint64_t qj = 4294967297ULL * x[i0]; 456 uint64_t *res_j0 = x + i0; 457 uint64_t c = 0ULL; 458 { 459 uint64_t a_i = n[4U * 0U]; 460 uint64_t *res_i0 = res_j0 + 4U * 0U; 461 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, qj, c, res_i0); 462 uint64_t a_i0 = n[4U * 0U + 1U]; 463 uint64_t *res_i1 = res_j0 + 4U * 0U + 1U; 464 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i0, qj, c, res_i1); 465 uint64_t a_i1 = n[4U * 0U + 2U]; 466 uint64_t *res_i2 = res_j0 + 4U * 0U + 2U; 467 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i1, qj, c, res_i2); 468 uint64_t a_i2 = n[4U * 0U + 3U]; 469 uint64_t *res_i = res_j0 + 4U * 0U + 3U; 470 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i2, qj, c, res_i); 471 } KRML_MAYBE_FOR2(i, 472 4U, 473 6U, 474 1U, 475 uint64_t a_i = n[i]; 476 uint64_t *res_i = res_j0 + i; 477 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, qj, c, res_i);); 478 uint64_t r = c; 479 uint64_t c1 = r; 480 uint64_t *resb = x + 6U + i0; 481 uint64_t res_j = x[6U + i0]; 482 c0 = Lib_IntTypes_Intrinsics_add_carry_u64(c0, c1, res_j, resb);); 483 memcpy(res, x + 6U, 6U * sizeof(uint64_t)); 484 uint64_t c00 = c0; 485 uint64_t tmp[6U] = { 0U }; 486 uint64_t c = 0ULL; 487 { 488 uint64_t t1 = res[4U * 0U]; 489 uint64_t t20 = n[4U * 0U]; 490 uint64_t *res_i0 = tmp + 4U * 0U; 491 c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t1, t20, res_i0); 492 uint64_t t10 = res[4U * 0U + 1U]; 493 uint64_t t21 = n[4U * 0U + 1U]; 494 uint64_t *res_i1 = tmp + 4U * 0U + 1U; 495 c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t10, t21, res_i1); 496 uint64_t t11 = res[4U * 0U + 2U]; 497 uint64_t t22 = n[4U * 0U + 2U]; 498 uint64_t *res_i2 = tmp + 4U * 0U + 2U; 499 c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t11, t22, res_i2); 500 uint64_t t12 = res[4U * 0U + 3U]; 501 uint64_t t2 = n[4U * 0U + 3U]; 502 uint64_t *res_i = tmp + 4U * 0U + 3U; 503 c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t12, t2, res_i); 504 } 505 KRML_MAYBE_FOR2(i, 506 4U, 507 6U, 508 1U, 509 uint64_t t1 = res[i]; 510 uint64_t t2 = n[i]; 511 uint64_t *res_i = tmp + i; 512 c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t1, t2, res_i);); 513 uint64_t c1 = c; 514 uint64_t c2 = c00 - c1; 515 KRML_MAYBE_FOR6(i, 516 0U, 517 6U, 518 1U, 519 uint64_t *os = res; 520 uint64_t x1 = (c2 & res[i]) | (~c2 & tmp[i]); 521 os[i] = x1;); 522 } 523 524 static inline void 525 qmont_reduction(uint64_t *res, uint64_t *x) 526 { 527 uint64_t n[6U] = { 0U }; 528 p384_make_order(n); 529 uint64_t c0 = 0ULL; 530 KRML_MAYBE_FOR6( 531 i0, 532 0U, 533 6U, 534 1U, 535 uint64_t qj = 7986114184663260229ULL * x[i0]; 536 uint64_t *res_j0 = x + i0; 537 uint64_t c = 0ULL; 538 { 539 uint64_t a_i = n[4U * 0U]; 540 uint64_t *res_i0 = res_j0 + 4U * 0U; 541 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, qj, c, res_i0); 542 uint64_t a_i0 = n[4U * 0U + 1U]; 543 uint64_t *res_i1 = res_j0 + 4U * 0U + 1U; 544 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i0, qj, c, res_i1); 545 uint64_t a_i1 = n[4U * 0U + 2U]; 546 uint64_t *res_i2 = res_j0 + 4U * 0U + 2U; 547 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i1, qj, c, res_i2); 548 uint64_t a_i2 = n[4U * 0U + 3U]; 549 uint64_t *res_i = res_j0 + 4U * 0U + 3U; 550 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i2, qj, c, res_i); 551 } KRML_MAYBE_FOR2(i, 552 4U, 553 6U, 554 1U, 555 uint64_t a_i = n[i]; 556 uint64_t *res_i = res_j0 + i; 557 c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, qj, c, res_i);); 558 uint64_t r = c; 559 uint64_t c1 = r; 560 uint64_t *resb = x + 6U + i0; 561 uint64_t res_j = x[6U + i0]; 562 c0 = Lib_IntTypes_Intrinsics_add_carry_u64(c0, c1, res_j, resb);); 563 memcpy(res, x + 6U, 6U * sizeof(uint64_t)); 564 uint64_t c00 = c0; 565 uint64_t tmp[6U] = { 0U }; 566 uint64_t c = 0ULL; 567 { 568 uint64_t t1 = res[4U * 0U]; 569 uint64_t t20 = n[4U * 0U]; 570 uint64_t *res_i0 = tmp + 4U * 0U; 571 c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t1, t20, res_i0); 572 uint64_t t10 = res[4U * 0U + 1U]; 573 uint64_t t21 = n[4U * 0U + 1U]; 574 uint64_t *res_i1 = tmp + 4U * 0U + 1U; 575 c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t10, t21, res_i1); 576 uint64_t t11 = res[4U * 0U + 2U]; 577 uint64_t t22 = n[4U * 0U + 2U]; 578 uint64_t *res_i2 = tmp + 4U * 0U + 2U; 579 c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t11, t22, res_i2); 580 uint64_t t12 = res[4U * 0U + 3U]; 581 uint64_t t2 = n[4U * 0U + 3U]; 582 uint64_t *res_i = tmp + 4U * 0U + 3U; 583 c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t12, t2, res_i); 584 } 585 KRML_MAYBE_FOR2(i, 586 4U, 587 6U, 588 1U, 589 uint64_t t1 = res[i]; 590 uint64_t t2 = n[i]; 591 uint64_t *res_i = tmp + i; 592 c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t1, t2, res_i);); 593 uint64_t c1 = c; 594 uint64_t c2 = c00 - c1; 595 KRML_MAYBE_FOR6(i, 596 0U, 597 6U, 598 1U, 599 uint64_t *os = res; 600 uint64_t x1 = (c2 & res[i]) | (~c2 & tmp[i]); 601 os[i] = x1;); 602 } 603 604 static inline uint64_t 605 bn_is_lt_prime_mask(uint64_t *f) 606 { 607 uint64_t tmp[6U] = { 0U }; 608 p384_make_prime(tmp); 609 uint64_t c = bn_sub(tmp, f, tmp); 610 uint64_t m = FStar_UInt64_gte_mask(c, 0ULL) & ~FStar_UInt64_eq_mask(c, 0ULL); 611 return m; 612 } 613 614 static inline void 615 fadd0(uint64_t *a, uint64_t *b, uint64_t *c) 616 { 617 uint64_t n[6U] = { 0U }; 618 p384_make_prime(n); 619 bn_add_mod(a, n, b, c); 620 } 621 622 static inline void 623 fsub0(uint64_t *a, uint64_t *b, uint64_t *c) 624 { 625 uint64_t n[6U] = { 0U }; 626 p384_make_prime(n); 627 bn_sub_mod(a, n, b, c); 628 } 629 630 static inline void 631 fmul0(uint64_t *a, uint64_t *b, uint64_t *c) 632 { 633 uint64_t tmp[12U] = { 0U }; 634 bn_mul(tmp, b, c); 635 fmont_reduction(a, tmp); 636 } 637 638 static inline void 639 fsqr0(uint64_t *a, uint64_t *b) 640 { 641 uint64_t tmp[12U] = { 0U }; 642 bn_sqr(tmp, b); 643 fmont_reduction(a, tmp); 644 } 645 646 static inline void 647 from_mont(uint64_t *a, uint64_t *b) 648 { 649 uint64_t tmp[12U] = { 0U }; 650 memcpy(tmp, b, 6U * sizeof(uint64_t)); 651 fmont_reduction(a, tmp); 652 } 653 654 static inline void 655 to_mont(uint64_t *a, uint64_t *b) 656 { 657 uint64_t r2modn[6U] = { 0U }; 658 p384_make_fmont_R2(r2modn); 659 uint64_t tmp[12U] = { 0U }; 660 bn_mul(tmp, b, r2modn); 661 fmont_reduction(a, tmp); 662 } 663 664 static inline void 665 fexp_consttime(uint64_t *out, uint64_t *a, uint64_t *b) 666 { 667 uint64_t table[192U] = { 0U }; 668 uint64_t tmp[6U] = { 0U }; 669 uint64_t *t0 = table; 670 uint64_t *t1 = table + 6U; 671 p384_make_fone(t0); 672 memcpy(t1, a, 6U * sizeof(uint64_t)); 673 KRML_MAYBE_FOR15(i, 674 0U, 675 15U, 676 1U, 677 uint64_t *t11 = table + (i + 1U) * 6U; 678 fsqr0(tmp, t11); 679 memcpy(table + (2U * i + 2U) * 6U, tmp, 6U * sizeof(uint64_t)); 680 uint64_t *t2 = table + (2U * i + 2U) * 6U; 681 fmul0(tmp, a, t2); 682 memcpy(table + (2U * i + 3U) * 6U, tmp, 6U * sizeof(uint64_t));); 683 uint32_t i0 = 380U; 684 uint64_t bits_c = Hacl_Bignum_Lib_bn_get_bits_u64(6U, b, i0, 5U); 685 memcpy(out, (uint64_t *)table, 6U * sizeof(uint64_t)); 686 for (uint32_t i1 = 0U; i1 < 31U; i1++) { 687 uint64_t c = FStar_UInt64_eq_mask(bits_c, (uint64_t)(i1 + 1U)); 688 const uint64_t *res_j = table + (i1 + 1U) * 6U; 689 KRML_MAYBE_FOR6(i, 690 0U, 691 6U, 692 1U, 693 uint64_t *os = out; 694 uint64_t x = (c & res_j[i]) | (~c & out[i]); 695 os[i] = x;); 696 } 697 uint64_t tmp0[6U] = { 0U }; 698 for (uint32_t i1 = 0U; i1 < 76U; i1++) { 699 KRML_MAYBE_FOR5(i, 0U, 5U, 1U, fsqr0(out, out);); 700 uint32_t k = 380U - 5U * i1 - 5U; 701 uint64_t bits_l = Hacl_Bignum_Lib_bn_get_bits_u64(6U, b, k, 5U); 702 memcpy(tmp0, (uint64_t *)table, 6U * sizeof(uint64_t)); 703 for (uint32_t i2 = 0U; i2 < 31U; i2++) { 704 uint64_t c = FStar_UInt64_eq_mask(bits_l, (uint64_t)(i2 + 1U)); 705 const uint64_t *res_j = table + (i2 + 1U) * 6U; 706 KRML_MAYBE_FOR6(i, 707 0U, 708 6U, 709 1U, 710 uint64_t *os = tmp0; 711 uint64_t x = (c & res_j[i]) | (~c & tmp0[i]); 712 os[i] = x;); 713 } 714 fmul0(out, out, tmp0); 715 } 716 } 717 718 static inline void 719 p384_finv(uint64_t *res, uint64_t *a) 720 { 721 uint64_t b[6U] = { 0U }; 722 b[0U] = 0x00000000fffffffdULL; 723 b[1U] = 0xffffffff00000000ULL; 724 b[2U] = 0xfffffffffffffffeULL; 725 b[3U] = 0xffffffffffffffffULL; 726 b[4U] = 0xffffffffffffffffULL; 727 b[5U] = 0xffffffffffffffffULL; 728 fexp_consttime(res, a, b); 729 } 730 731 static inline void 732 p384_fsqrt(uint64_t *res, uint64_t *a) 733 { 734 uint64_t b[6U] = { 0U }; 735 b[0U] = 0x0000000040000000ULL; 736 b[1U] = 0xbfffffffc0000000ULL; 737 b[2U] = 0xffffffffffffffffULL; 738 b[3U] = 0xffffffffffffffffULL; 739 b[4U] = 0xffffffffffffffffULL; 740 b[5U] = 0x3fffffffffffffffULL; 741 fexp_consttime(res, a, b); 742 } 743 744 static inline uint64_t 745 load_qelem_conditional(uint64_t *a, uint8_t *b) 746 { 747 bn_from_bytes_be(a, b); 748 uint64_t tmp[6U] = { 0U }; 749 p384_make_order(tmp); 750 uint64_t c = bn_sub(tmp, a, tmp); 751 uint64_t is_lt_order = FStar_UInt64_gte_mask(c, 0ULL) & ~FStar_UInt64_eq_mask(c, 0ULL); 752 uint64_t bn_zero[6U] = { 0U }; 753 uint64_t res = bn_is_eq_mask(a, bn_zero); 754 uint64_t is_eq_zero = res; 755 uint64_t is_b_valid = is_lt_order & ~is_eq_zero; 756 uint64_t oneq[6U] = { 0U }; 757 memset(oneq, 0U, 6U * sizeof(uint64_t)); 758 oneq[0U] = 1ULL; 759 KRML_MAYBE_FOR6(i, 760 0U, 761 6U, 762 1U, 763 uint64_t *os = a; 764 uint64_t uu____0 = oneq[i]; 765 uint64_t x = uu____0 ^ (is_b_valid & (a[i] ^ uu____0)); 766 os[i] = x;); 767 return is_b_valid; 768 } 769 770 static inline void 771 qmod_short(uint64_t *a, uint64_t *b) 772 { 773 uint64_t tmp[6U] = { 0U }; 774 p384_make_order(tmp); 775 uint64_t c = bn_sub(tmp, b, tmp); 776 bn_cmovznz(a, c, tmp, b); 777 } 778 779 static inline void 780 qadd(uint64_t *a, uint64_t *b, uint64_t *c) 781 { 782 uint64_t n[6U] = { 0U }; 783 p384_make_order(n); 784 bn_add_mod(a, n, b, c); 785 } 786 787 static inline void 788 qmul(uint64_t *a, uint64_t *b, uint64_t *c) 789 { 790 uint64_t tmp[12U] = { 0U }; 791 bn_mul(tmp, b, c); 792 qmont_reduction(a, tmp); 793 } 794 795 static inline void 796 qsqr(uint64_t *a, uint64_t *b) 797 { 798 uint64_t tmp[12U] = { 0U }; 799 bn_sqr(tmp, b); 800 qmont_reduction(a, tmp); 801 } 802 803 static inline void 804 from_qmont(uint64_t *a, uint64_t *b) 805 { 806 uint64_t tmp[12U] = { 0U }; 807 memcpy(tmp, b, 6U * sizeof(uint64_t)); 808 qmont_reduction(a, tmp); 809 } 810 811 static inline void 812 qexp_consttime(uint64_t *out, uint64_t *a, uint64_t *b) 813 { 814 uint64_t table[192U] = { 0U }; 815 uint64_t tmp[6U] = { 0U }; 816 uint64_t *t0 = table; 817 uint64_t *t1 = table + 6U; 818 p384_make_qone(t0); 819 memcpy(t1, a, 6U * sizeof(uint64_t)); 820 KRML_MAYBE_FOR15(i, 821 0U, 822 15U, 823 1U, 824 uint64_t *t11 = table + (i + 1U) * 6U; 825 qsqr(tmp, t11); 826 memcpy(table + (2U * i + 2U) * 6U, tmp, 6U * sizeof(uint64_t)); 827 uint64_t *t2 = table + (2U * i + 2U) * 6U; 828 qmul(tmp, a, t2); 829 memcpy(table + (2U * i + 3U) * 6U, tmp, 6U * sizeof(uint64_t));); 830 uint32_t i0 = 380U; 831 uint64_t bits_c = Hacl_Bignum_Lib_bn_get_bits_u64(6U, b, i0, 5U); 832 memcpy(out, (uint64_t *)table, 6U * sizeof(uint64_t)); 833 for (uint32_t i1 = 0U; i1 < 31U; i1++) { 834 uint64_t c = FStar_UInt64_eq_mask(bits_c, (uint64_t)(i1 + 1U)); 835 const uint64_t *res_j = table + (i1 + 1U) * 6U; 836 KRML_MAYBE_FOR6(i, 837 0U, 838 6U, 839 1U, 840 uint64_t *os = out; 841 uint64_t x = (c & res_j[i]) | (~c & out[i]); 842 os[i] = x;); 843 } 844 uint64_t tmp0[6U] = { 0U }; 845 for (uint32_t i1 = 0U; i1 < 76U; i1++) { 846 KRML_MAYBE_FOR5(i, 0U, 5U, 1U, qsqr(out, out);); 847 uint32_t k = 380U - 5U * i1 - 5U; 848 uint64_t bits_l = Hacl_Bignum_Lib_bn_get_bits_u64(6U, b, k, 5U); 849 memcpy(tmp0, (uint64_t *)table, 6U * sizeof(uint64_t)); 850 for (uint32_t i2 = 0U; i2 < 31U; i2++) { 851 uint64_t c = FStar_UInt64_eq_mask(bits_l, (uint64_t)(i2 + 1U)); 852 const uint64_t *res_j = table + (i2 + 1U) * 6U; 853 KRML_MAYBE_FOR6(i, 854 0U, 855 6U, 856 1U, 857 uint64_t *os = tmp0; 858 uint64_t x = (c & res_j[i]) | (~c & tmp0[i]); 859 os[i] = x;); 860 } 861 qmul(out, out, tmp0); 862 } 863 } 864 865 static inline void 866 p384_qinv(uint64_t *res, uint64_t *a) 867 { 868 uint64_t b[6U] = { 0U }; 869 b[0U] = 0xecec196accc52971ULL; 870 b[1U] = 0x581a0db248b0a77aULL; 871 b[2U] = 0xc7634d81f4372ddfULL; 872 b[3U] = 0xffffffffffffffffULL; 873 b[4U] = 0xffffffffffffffffULL; 874 b[5U] = 0xffffffffffffffffULL; 875 qexp_consttime(res, a, b); 876 } 877 878 static inline void 879 point_add(uint64_t *x, uint64_t *y, uint64_t *xy) 880 { 881 uint64_t tmp[54U] = { 0U }; 882 uint64_t *t0 = tmp; 883 uint64_t *t1 = tmp + 36U; 884 uint64_t *x3 = t1; 885 uint64_t *y3 = t1 + 6U; 886 uint64_t *z3 = t1 + 12U; 887 uint64_t *t01 = t0; 888 uint64_t *t11 = t0 + 6U; 889 uint64_t *t2 = t0 + 12U; 890 uint64_t *t3 = t0 + 18U; 891 uint64_t *t4 = t0 + 24U; 892 uint64_t *t5 = t0 + 30U; 893 uint64_t *x1 = x; 894 uint64_t *y1 = x + 6U; 895 uint64_t *z10 = x + 12U; 896 uint64_t *x20 = y; 897 uint64_t *y20 = y + 6U; 898 uint64_t *z20 = y + 12U; 899 fmul0(t01, x1, x20); 900 fmul0(t11, y1, y20); 901 fmul0(t2, z10, z20); 902 fadd0(t3, x1, y1); 903 fadd0(t4, x20, y20); 904 fmul0(t3, t3, t4); 905 fadd0(t4, t01, t11); 906 uint64_t *y10 = x + 6U; 907 uint64_t *z11 = x + 12U; 908 uint64_t *y2 = y + 6U; 909 uint64_t *z21 = y + 12U; 910 fsub0(t3, t3, t4); 911 fadd0(t4, y10, z11); 912 fadd0(t5, y2, z21); 913 fmul0(t4, t4, t5); 914 fadd0(t5, t11, t2); 915 fsub0(t4, t4, t5); 916 uint64_t *x10 = x; 917 uint64_t *z1 = x + 12U; 918 uint64_t *x2 = y; 919 uint64_t *z2 = y + 12U; 920 fadd0(x3, x10, z1); 921 fadd0(y3, x2, z2); 922 fmul0(x3, x3, y3); 923 fadd0(y3, t01, t2); 924 fsub0(y3, x3, y3); 925 uint64_t b_coeff[6U] = { 0U }; 926 p384_make_b_coeff(b_coeff); 927 fmul0(z3, b_coeff, t2); 928 fsub0(x3, y3, z3); 929 fadd0(z3, x3, x3); 930 fadd0(x3, x3, z3); 931 fsub0(z3, t11, x3); 932 fadd0(x3, t11, x3); 933 uint64_t b_coeff0[6U] = { 0U }; 934 p384_make_b_coeff(b_coeff0); 935 fmul0(y3, b_coeff0, y3); 936 fadd0(t11, t2, t2); 937 fadd0(t2, t11, t2); 938 fsub0(y3, y3, t2); 939 fsub0(y3, y3, t01); 940 fadd0(t11, y3, y3); 941 fadd0(y3, t11, y3); 942 fadd0(t11, t01, t01); 943 fadd0(t01, t11, t01); 944 fsub0(t01, t01, t2); 945 fmul0(t11, t4, y3); 946 fmul0(t2, t01, y3); 947 fmul0(y3, x3, z3); 948 fadd0(y3, y3, t2); 949 fmul0(x3, t3, x3); 950 fsub0(x3, x3, t11); 951 fmul0(z3, t4, z3); 952 fmul0(t11, t3, t01); 953 fadd0(z3, z3, t11); 954 memcpy(xy, t1, 18U * sizeof(uint64_t)); 955 } 956 957 static inline void 958 point_double(uint64_t *x, uint64_t *xx) 959 { 960 uint64_t tmp[30U] = { 0U }; 961 uint64_t *x1 = x; 962 uint64_t *z = x + 12U; 963 uint64_t *x3 = xx; 964 uint64_t *y3 = xx + 6U; 965 uint64_t *z3 = xx + 12U; 966 uint64_t *t0 = tmp; 967 uint64_t *t1 = tmp + 6U; 968 uint64_t *t2 = tmp + 12U; 969 uint64_t *t3 = tmp + 18U; 970 uint64_t *t4 = tmp + 24U; 971 uint64_t *x2 = x; 972 uint64_t *y = x + 6U; 973 uint64_t *z1 = x + 12U; 974 fsqr0(t0, x2); 975 fsqr0(t1, y); 976 fsqr0(t2, z1); 977 fmul0(t3, x2, y); 978 fadd0(t3, t3, t3); 979 fmul0(t4, y, z1); 980 fmul0(z3, x1, z); 981 fadd0(z3, z3, z3); 982 uint64_t b_coeff[6U] = { 0U }; 983 p384_make_b_coeff(b_coeff); 984 fmul0(y3, b_coeff, t2); 985 fsub0(y3, y3, z3); 986 fadd0(x3, y3, y3); 987 fadd0(y3, x3, y3); 988 fsub0(x3, t1, y3); 989 fadd0(y3, t1, y3); 990 fmul0(y3, x3, y3); 991 fmul0(x3, x3, t3); 992 fadd0(t3, t2, t2); 993 fadd0(t2, t2, t3); 994 uint64_t b_coeff0[6U] = { 0U }; 995 p384_make_b_coeff(b_coeff0); 996 fmul0(z3, b_coeff0, z3); 997 fsub0(z3, z3, t2); 998 fsub0(z3, z3, t0); 999 fadd0(t3, z3, z3); 1000 fadd0(z3, z3, t3); 1001 fadd0(t3, t0, t0); 1002 fadd0(t0, t3, t0); 1003 fsub0(t0, t0, t2); 1004 fmul0(t0, t0, z3); 1005 fadd0(y3, y3, t0); 1006 fadd0(t0, t4, t4); 1007 fmul0(z3, t0, z3); 1008 fsub0(x3, x3, z3); 1009 fmul0(z3, t0, t1); 1010 fadd0(z3, z3, z3); 1011 fadd0(z3, z3, z3); 1012 } 1013 1014 static inline void 1015 point_zero(uint64_t *one) 1016 { 1017 uint64_t *x = one; 1018 uint64_t *y = one + 6U; 1019 uint64_t *z = one + 12U; 1020 p384_make_fzero(x); 1021 p384_make_fone(y); 1022 p384_make_fzero(z); 1023 } 1024 1025 static inline void 1026 point_mul(uint64_t *res, uint64_t *scalar, uint64_t *p) 1027 { 1028 uint64_t table[288U] = { 0U }; 1029 uint64_t tmp[18U] = { 0U }; 1030 uint64_t *t0 = table; 1031 uint64_t *t1 = table + 18U; 1032 point_zero(t0); 1033 memcpy(t1, p, 18U * sizeof(uint64_t)); 1034 KRML_MAYBE_FOR7(i, 1035 0U, 1036 7U, 1037 1U, 1038 uint64_t *t11 = table + (i + 1U) * 18U; 1039 point_double(t11, tmp); 1040 memcpy(table + (2U * i + 2U) * 18U, tmp, 18U * sizeof(uint64_t)); 1041 uint64_t *t2 = table + (2U * i + 2U) * 18U; 1042 point_add(p, t2, tmp); 1043 memcpy(table + (2U * i + 3U) * 18U, tmp, 18U * sizeof(uint64_t));); 1044 point_zero(res); 1045 uint64_t tmp0[18U] = { 0U }; 1046 for (uint32_t i0 = 0U; i0 < 96U; i0++) { 1047 KRML_MAYBE_FOR4(i, 0U, 4U, 1U, point_double(res, res);); 1048 uint32_t k = 384U - 4U * i0 - 4U; 1049 uint64_t bits_l = Hacl_Bignum_Lib_bn_get_bits_u64(6U, scalar, k, 4U); 1050 memcpy(tmp0, (uint64_t *)table, 18U * sizeof(uint64_t)); 1051 KRML_MAYBE_FOR15( 1052 i1, 1053 0U, 1054 15U, 1055 1U, 1056 uint64_t c = FStar_UInt64_eq_mask(bits_l, (uint64_t)(i1 + 1U)); 1057 const uint64_t *res_j = table + (i1 + 1U) * 18U; 1058 for (uint32_t i = 0U; i < 18U; i++) { 1059 uint64_t *os = tmp0; 1060 uint64_t x = (c & res_j[i]) | (~c & tmp0[i]); 1061 os[i] = x; 1062 }); 1063 point_add(res, tmp0, res); 1064 } 1065 } 1066 1067 static inline void 1068 point_mul_g(uint64_t *res, uint64_t *scalar) 1069 { 1070 uint64_t g[18U] = { 0U }; 1071 uint64_t *x = g; 1072 uint64_t *y = g + 6U; 1073 uint64_t *z = g + 12U; 1074 p384_make_g_x(x); 1075 p384_make_g_y(y); 1076 p384_make_fone(z); 1077 point_mul(res, scalar, g); 1078 } 1079 1080 static inline void 1081 point_mul_double_g(uint64_t *res, uint64_t *scalar1, uint64_t *scalar2, uint64_t *p) 1082 { 1083 uint64_t tmp[18U] = { 0U }; 1084 point_mul_g(tmp, scalar1); 1085 point_mul(res, scalar2, p); 1086 point_add(res, tmp, res); 1087 } 1088 1089 static inline bool 1090 ecdsa_sign_msg_as_qelem( 1091 uint8_t *signature, 1092 uint64_t *m_q, 1093 uint8_t *private_key, 1094 uint8_t *nonce) 1095 { 1096 uint64_t rsdk_q[24U] = { 0U }; 1097 uint64_t *r_q = rsdk_q; 1098 uint64_t *s_q = rsdk_q + 6U; 1099 uint64_t *d_a = rsdk_q + 12U; 1100 uint64_t *k_q = rsdk_q + 18U; 1101 uint64_t is_sk_valid = load_qelem_conditional(d_a, private_key); 1102 uint64_t is_nonce_valid = load_qelem_conditional(k_q, nonce); 1103 uint64_t are_sk_nonce_valid = is_sk_valid & is_nonce_valid; 1104 uint64_t p[18U] = { 0U }; 1105 point_mul_g(p, k_q); 1106 uint64_t zinv[6U] = { 0U }; 1107 uint64_t *px = p; 1108 uint64_t *pz = p + 12U; 1109 p384_finv(zinv, pz); 1110 fmul0(r_q, px, zinv); 1111 from_mont(r_q, r_q); 1112 qmod_short(r_q, r_q); 1113 uint64_t kinv[6U] = { 0U }; 1114 p384_qinv(kinv, k_q); 1115 qmul(s_q, r_q, d_a); 1116 from_qmont(m_q, m_q); 1117 qadd(s_q, m_q, s_q); 1118 qmul(s_q, kinv, s_q); 1119 bn_to_bytes_be(signature, r_q); 1120 bn_to_bytes_be(signature + 48U, s_q); 1121 uint64_t bn_zero0[6U] = { 0U }; 1122 uint64_t res = bn_is_eq_mask(r_q, bn_zero0); 1123 uint64_t is_r_zero = res; 1124 uint64_t bn_zero[6U] = { 0U }; 1125 uint64_t res0 = bn_is_eq_mask(s_q, bn_zero); 1126 uint64_t is_s_zero = res0; 1127 uint64_t m = are_sk_nonce_valid & (~is_r_zero & ~is_s_zero); 1128 bool res1 = m == 0xFFFFFFFFFFFFFFFFULL; 1129 return res1; 1130 } 1131 1132 static inline bool 1133 ecdsa_verify_msg_as_qelem( 1134 uint64_t *m_q, 1135 uint8_t *public_key, 1136 uint8_t *signature_r, 1137 uint8_t *signature_s) 1138 { 1139 uint64_t tmp[42U] = { 0U }; 1140 uint64_t *pk = tmp; 1141 uint64_t *r_q = tmp + 18U; 1142 uint64_t *s_q = tmp + 24U; 1143 uint64_t *u1 = tmp + 30U; 1144 uint64_t *u2 = tmp + 36U; 1145 uint64_t p_aff[12U] = { 0U }; 1146 uint8_t *p_x = public_key; 1147 uint8_t *p_y = public_key + 48U; 1148 uint64_t *bn_p_x = p_aff; 1149 uint64_t *bn_p_y = p_aff + 6U; 1150 bn_from_bytes_be(bn_p_x, p_x); 1151 bn_from_bytes_be(bn_p_y, p_y); 1152 uint64_t *px0 = p_aff; 1153 uint64_t *py0 = p_aff + 6U; 1154 uint64_t lessX = bn_is_lt_prime_mask(px0); 1155 uint64_t lessY = bn_is_lt_prime_mask(py0); 1156 uint64_t res0 = lessX & lessY; 1157 bool is_xy_valid = res0 == 0xFFFFFFFFFFFFFFFFULL; 1158 bool res; 1159 if (!is_xy_valid) { 1160 res = false; 1161 } else { 1162 uint64_t rp[6U] = { 0U }; 1163 uint64_t tx[6U] = { 0U }; 1164 uint64_t ty[6U] = { 0U }; 1165 uint64_t *px = p_aff; 1166 uint64_t *py = p_aff + 6U; 1167 to_mont(tx, px); 1168 to_mont(ty, py); 1169 uint64_t tmp1[6U] = { 0U }; 1170 fsqr0(rp, tx); 1171 fmul0(rp, rp, tx); 1172 p384_make_a_coeff(tmp1); 1173 fmul0(tmp1, tmp1, tx); 1174 fadd0(rp, tmp1, rp); 1175 p384_make_b_coeff(tmp1); 1176 fadd0(rp, tmp1, rp); 1177 fsqr0(ty, ty); 1178 uint64_t r = bn_is_eq_mask(ty, rp); 1179 uint64_t r0 = r; 1180 bool r1 = r0 == 0xFFFFFFFFFFFFFFFFULL; 1181 res = r1; 1182 } 1183 if (res) { 1184 uint64_t *px = p_aff; 1185 uint64_t *py = p_aff + 6U; 1186 uint64_t *rx = pk; 1187 uint64_t *ry = pk + 6U; 1188 uint64_t *rz = pk + 12U; 1189 to_mont(rx, px); 1190 to_mont(ry, py); 1191 p384_make_fone(rz); 1192 } 1193 bool is_pk_valid = res; 1194 bn_from_bytes_be(r_q, signature_r); 1195 bn_from_bytes_be(s_q, signature_s); 1196 uint64_t tmp10[6U] = { 0U }; 1197 p384_make_order(tmp10); 1198 uint64_t c = bn_sub(tmp10, r_q, tmp10); 1199 uint64_t is_lt_order = FStar_UInt64_gte_mask(c, 0ULL) & ~FStar_UInt64_eq_mask(c, 0ULL); 1200 uint64_t bn_zero0[6U] = { 0U }; 1201 uint64_t res1 = bn_is_eq_mask(r_q, bn_zero0); 1202 uint64_t is_eq_zero = res1; 1203 uint64_t is_r_valid = is_lt_order & ~is_eq_zero; 1204 uint64_t tmp11[6U] = { 0U }; 1205 p384_make_order(tmp11); 1206 uint64_t c0 = bn_sub(tmp11, s_q, tmp11); 1207 uint64_t is_lt_order0 = FStar_UInt64_gte_mask(c0, 0ULL) & ~FStar_UInt64_eq_mask(c0, 0ULL); 1208 uint64_t bn_zero1[6U] = { 0U }; 1209 uint64_t res2 = bn_is_eq_mask(s_q, bn_zero1); 1210 uint64_t is_eq_zero0 = res2; 1211 uint64_t is_s_valid = is_lt_order0 & ~is_eq_zero0; 1212 bool is_rs_valid = is_r_valid == 0xFFFFFFFFFFFFFFFFULL && is_s_valid == 0xFFFFFFFFFFFFFFFFULL; 1213 if (!(is_pk_valid && is_rs_valid)) { 1214 return false; 1215 } 1216 uint64_t sinv[6U] = { 0U }; 1217 p384_qinv(sinv, s_q); 1218 uint64_t tmp1[6U] = { 0U }; 1219 from_qmont(tmp1, m_q); 1220 qmul(u1, sinv, tmp1); 1221 uint64_t tmp12[6U] = { 0U }; 1222 from_qmont(tmp12, r_q); 1223 qmul(u2, sinv, tmp12); 1224 uint64_t res3[18U] = { 0U }; 1225 point_mul_double_g(res3, u1, u2, pk); 1226 uint64_t *pz0 = res3 + 12U; 1227 uint64_t bn_zero[6U] = { 0U }; 1228 uint64_t res10 = bn_is_eq_mask(pz0, bn_zero); 1229 uint64_t m = res10; 1230 if (m == 0xFFFFFFFFFFFFFFFFULL) { 1231 return false; 1232 } 1233 uint64_t x[6U] = { 0U }; 1234 uint64_t zinv[6U] = { 0U }; 1235 uint64_t *px = res3; 1236 uint64_t *pz = res3 + 12U; 1237 p384_finv(zinv, pz); 1238 fmul0(x, px, zinv); 1239 from_mont(x, x); 1240 qmod_short(x, x); 1241 uint64_t m0 = bn_is_eq_mask(x, r_q); 1242 bool res11 = m0 == 0xFFFFFFFFFFFFFFFFULL; 1243 return res11; 1244 } 1245 1246 /******************************************************************************* 1247 1248 Verified C library for ECDSA and ECDH functions over the P-384 NIST curve. 1249 1250 This module implements signing and verification, key validation, conversions 1251 between various point representations, and ECDH key agreement. 1252 1253 *******************************************************************************/ 1254 1255 /*****************/ 1256 /* ECDSA signing */ 1257 /*****************/ 1258 1259 /** 1260 Create an ECDSA signature WITHOUT hashing first. 1261 1262 This function is intended to receive a hash of the input. 1263 For convenience, we recommend using one of the hash-and-sign combined functions above. 1264 1265 The argument `msg` MUST be at least 48 bytes (i.e. `msg_len >= 48`). 1266 1267 NOTE: The equivalent functions in OpenSSL and Fiat-Crypto both accept inputs 1268 smaller than 48 bytes. These libraries left-pad the input with enough zeroes to 1269 reach the minimum 48 byte size. Clients who need behavior identical to OpenSSL 1270 need to perform the left-padding themselves. 1271 1272 The function returns `true` for successful creation of an ECDSA signature and `false` otherwise. 1273 1274 The outparam `signature` (R || S) points to 96 bytes of valid memory, i.e., uint8_t[96]. 1275 The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len]. 1276 The arguments `private_key` and `nonce` point to 48 bytes of valid memory, i.e., uint8_t[48]. 1277 1278 The function also checks whether `private_key` and `nonce` are valid values: 1279 • 0 < `private_key` < the order of the curve 1280 • 0 < `nonce` < the order of the curve 1281 */ 1282 bool 1283 Hacl_P384_ecdsa_sign_p384_without_hash( 1284 uint8_t *signature, 1285 uint32_t msg_len, 1286 uint8_t *msg, 1287 uint8_t *private_key, 1288 uint8_t *nonce) 1289 { 1290 uint64_t m_q[6U] = { 0U }; 1291 uint8_t mHash[48U] = { 0U }; 1292 memcpy(mHash, msg, 48U * sizeof(uint8_t)); 1293 KRML_MAYBE_UNUSED_VAR(msg_len); 1294 uint8_t *mHash48 = mHash; 1295 bn_from_bytes_be(m_q, mHash48); 1296 qmod_short(m_q, m_q); 1297 bool res = ecdsa_sign_msg_as_qelem(signature, m_q, private_key, nonce); 1298 return res; 1299 } 1300 1301 /**********************/ 1302 /* ECDSA verification */ 1303 /**********************/ 1304 1305 /** 1306 Verify an ECDSA signature WITHOUT hashing first. 1307 1308 This function is intended to receive a hash of the input. 1309 For convenience, we recommend using one of the hash-and-verify combined functions above. 1310 1311 The argument `msg` MUST be at least 48 bytes (i.e. `msg_len >= 48`). 1312 1313 The function returns `true` if the signature is valid and `false` otherwise. 1314 1315 The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len]. 1316 The argument `public_key` (x || y) points to 96 bytes of valid memory, i.e., uint8_t[96]. 1317 The arguments `signature_r` and `signature_s` point to 48 bytes of valid memory, i.e., uint8_t[48]. 1318 1319 The function also checks whether `public_key` is valid 1320 */ 1321 bool 1322 Hacl_P384_ecdsa_verif_without_hash( 1323 uint32_t msg_len, 1324 uint8_t *msg, 1325 uint8_t *public_key, 1326 uint8_t *signature_r, 1327 uint8_t *signature_s) 1328 { 1329 uint64_t m_q[6U] = { 0U }; 1330 uint8_t mHash[48U] = { 0U }; 1331 memcpy(mHash, msg, 48U * sizeof(uint8_t)); 1332 KRML_MAYBE_UNUSED_VAR(msg_len); 1333 uint8_t *mHash48 = mHash; 1334 bn_from_bytes_be(m_q, mHash48); 1335 qmod_short(m_q, m_q); 1336 bool res = ecdsa_verify_msg_as_qelem(m_q, public_key, signature_r, signature_s); 1337 return res; 1338 } 1339 1340 /******************/ 1341 /* Key validation */ 1342 /******************/ 1343 1344 /** 1345 Public key validation. 1346 1347 The function returns `true` if a public key is valid and `false` otherwise. 1348 1349 The argument `public_key` points to 96 bytes of valid memory, i.e., uint8_t[96]. 1350 1351 The public key (x || y) is valid (with respect to SP 800-56A): 1352 • the public key is not the “point at infinity”, represented as O. 1353 • the affine x and y coordinates of the point represented by the public key are 1354 in the range [0, p – 1] where p is the prime defining the finite field. 1355 • y^2 = x^3 + ax + b where a and b are the coefficients of the curve equation. 1356 The last extract is taken from: https://neilmadden.blog/2017/05/17/so-how-do-you-validate-nist-ecdh-public-keys/ 1357 */ 1358 bool 1359 Hacl_P384_validate_public_key(uint8_t *public_key) 1360 { 1361 uint64_t point_jac[18U] = { 0U }; 1362 uint64_t p_aff[12U] = { 0U }; 1363 uint8_t *p_x = public_key; 1364 uint8_t *p_y = public_key + 48U; 1365 uint64_t *bn_p_x = p_aff; 1366 uint64_t *bn_p_y = p_aff + 6U; 1367 bn_from_bytes_be(bn_p_x, p_x); 1368 bn_from_bytes_be(bn_p_y, p_y); 1369 uint64_t *px0 = p_aff; 1370 uint64_t *py0 = p_aff + 6U; 1371 uint64_t lessX = bn_is_lt_prime_mask(px0); 1372 uint64_t lessY = bn_is_lt_prime_mask(py0); 1373 uint64_t res0 = lessX & lessY; 1374 bool is_xy_valid = res0 == 0xFFFFFFFFFFFFFFFFULL; 1375 bool res; 1376 if (!is_xy_valid) { 1377 res = false; 1378 } else { 1379 uint64_t rp[6U] = { 0U }; 1380 uint64_t tx[6U] = { 0U }; 1381 uint64_t ty[6U] = { 0U }; 1382 uint64_t *px = p_aff; 1383 uint64_t *py = p_aff + 6U; 1384 to_mont(tx, px); 1385 to_mont(ty, py); 1386 uint64_t tmp[6U] = { 0U }; 1387 fsqr0(rp, tx); 1388 fmul0(rp, rp, tx); 1389 p384_make_a_coeff(tmp); 1390 fmul0(tmp, tmp, tx); 1391 fadd0(rp, tmp, rp); 1392 p384_make_b_coeff(tmp); 1393 fadd0(rp, tmp, rp); 1394 fsqr0(ty, ty); 1395 uint64_t r = bn_is_eq_mask(ty, rp); 1396 uint64_t r0 = r; 1397 bool r1 = r0 == 0xFFFFFFFFFFFFFFFFULL; 1398 res = r1; 1399 } 1400 if (res) { 1401 uint64_t *px = p_aff; 1402 uint64_t *py = p_aff + 6U; 1403 uint64_t *rx = point_jac; 1404 uint64_t *ry = point_jac + 6U; 1405 uint64_t *rz = point_jac + 12U; 1406 to_mont(rx, px); 1407 to_mont(ry, py); 1408 p384_make_fone(rz); 1409 } 1410 bool res1 = res; 1411 return res1; 1412 } 1413 1414 /** 1415 Private key validation. 1416 1417 The function returns `true` if a private key is valid and `false` otherwise. 1418 1419 The argument `private_key` points to 48 bytes of valid memory, i.e., uint8_t[48]. 1420 1421 The private key is valid: 1422 • 0 < `private_key` < the order of the curve 1423 */ 1424 bool 1425 Hacl_P384_validate_private_key(uint8_t *private_key) 1426 { 1427 uint64_t bn_sk[6U] = { 0U }; 1428 bn_from_bytes_be(bn_sk, private_key); 1429 uint64_t tmp[6U] = { 0U }; 1430 p384_make_order(tmp); 1431 uint64_t c = bn_sub(tmp, bn_sk, tmp); 1432 uint64_t is_lt_order = FStar_UInt64_gte_mask(c, 0ULL) & ~FStar_UInt64_eq_mask(c, 0ULL); 1433 uint64_t bn_zero[6U] = { 0U }; 1434 uint64_t res = bn_is_eq_mask(bn_sk, bn_zero); 1435 uint64_t is_eq_zero = res; 1436 uint64_t res0 = is_lt_order & ~is_eq_zero; 1437 return res0 == 0xFFFFFFFFFFFFFFFFULL; 1438 } 1439 1440 /******************************************************************************* 1441 Parsing and Serializing public keys. 1442 1443 A public key is a point (x, y) on the P-384 NIST curve. 1444 1445 The point can be represented in the following three ways. 1446 • raw = [ x || y ], 96 bytes 1447 • uncompressed = [ 0x04 || x || y ], 97 bytes 1448 • compressed = [ (0x02 for even `y` and 0x03 for odd `y`) || x ], 33 bytes 1449 1450 *******************************************************************************/ 1451 1452 /** 1453 Convert a public key from uncompressed to its raw form. 1454 1455 The function returns `true` for successful conversion of a public key and `false` otherwise. 1456 1457 The outparam `pk_raw` points to 96 bytes of valid memory, i.e., uint8_t[96]. 1458 The argument `pk` points to 97 bytes of valid memory, i.e., uint8_t[97]. 1459 1460 The function DOESN'T check whether (x, y) is a valid point. 1461 */ 1462 bool 1463 Hacl_P384_uncompressed_to_raw(uint8_t *pk, uint8_t *pk_raw) 1464 { 1465 uint8_t pk0 = pk[0U]; 1466 if (pk0 != 0x04U) { 1467 return false; 1468 } 1469 memcpy(pk_raw, pk + 1U, 96U * sizeof(uint8_t)); 1470 return true; 1471 } 1472 1473 /** 1474 Convert a public key from compressed to its raw form. 1475 1476 The function returns `true` for successful conversion of a public key and `false` otherwise. 1477 1478 The outparam `pk_raw` points to 96 bytes of valid memory, i.e., uint8_t[96]. 1479 The argument `pk` points to 33 bytes of valid memory, i.e., uint8_t[33]. 1480 1481 The function also checks whether (x, y) is a valid point. 1482 */ 1483 bool 1484 Hacl_P384_compressed_to_raw(uint8_t *pk, uint8_t *pk_raw) 1485 { 1486 uint64_t xa[6U] = { 0U }; 1487 uint64_t ya[6U] = { 0U }; 1488 uint8_t *pk_xb = pk + 1U; 1489 uint8_t s0 = pk[0U]; 1490 uint8_t s01 = s0; 1491 bool b; 1492 if (!(s01 == 0x02U || s01 == 0x03U)) { 1493 b = false; 1494 } else { 1495 uint8_t *xb = pk + 1U; 1496 bn_from_bytes_be(xa, xb); 1497 uint64_t is_x_valid = bn_is_lt_prime_mask(xa); 1498 bool is_x_valid1 = is_x_valid == 0xFFFFFFFFFFFFFFFFULL; 1499 bool is_y_odd = s01 == 0x03U; 1500 if (!is_x_valid1) { 1501 b = false; 1502 } else { 1503 uint64_t y2M[6U] = { 0U }; 1504 uint64_t xM[6U] = { 0U }; 1505 uint64_t yM[6U] = { 0U }; 1506 to_mont(xM, xa); 1507 uint64_t tmp[6U] = { 0U }; 1508 fsqr0(y2M, xM); 1509 fmul0(y2M, y2M, xM); 1510 p384_make_a_coeff(tmp); 1511 fmul0(tmp, tmp, xM); 1512 fadd0(y2M, tmp, y2M); 1513 p384_make_b_coeff(tmp); 1514 fadd0(y2M, tmp, y2M); 1515 p384_fsqrt(yM, y2M); 1516 from_mont(ya, yM); 1517 fsqr0(yM, yM); 1518 uint64_t r = bn_is_eq_mask(yM, y2M); 1519 uint64_t r0 = r; 1520 bool is_y_valid = r0 == 0xFFFFFFFFFFFFFFFFULL; 1521 bool is_y_valid0 = is_y_valid; 1522 if (!is_y_valid0) { 1523 b = false; 1524 } else { 1525 uint64_t is_y_odd1 = ya[0U] & 1ULL; 1526 bool is_y_odd2 = is_y_odd1 == 1ULL; 1527 uint64_t zero[6U] = { 0U }; 1528 if (is_y_odd2 != is_y_odd) { 1529 fsub0(ya, zero, ya); 1530 } 1531 b = true; 1532 } 1533 } 1534 } 1535 if (b) { 1536 memcpy(pk_raw, pk_xb, 48U * sizeof(uint8_t)); 1537 bn_to_bytes_be(pk_raw + 48U, ya); 1538 } 1539 return b; 1540 } 1541 1542 /** 1543 Convert a public key from raw to its uncompressed form. 1544 1545 The outparam `pk` points to 97 bytes of valid memory, i.e., uint8_t[97]. 1546 The argument `pk_raw` points to 96 bytes of valid memory, i.e., uint8_t[96]. 1547 1548 The function DOESN'T check whether (x, y) is a valid point. 1549 */ 1550 void 1551 Hacl_P384_raw_to_uncompressed(uint8_t *pk_raw, uint8_t *pk) 1552 { 1553 pk[0U] = 0x04U; 1554 memcpy(pk + 1U, pk_raw, 96U * sizeof(uint8_t)); 1555 } 1556 1557 /** 1558 Convert a public key from raw to its compressed form. 1559 1560 The outparam `pk` points to 33 bytes of valid memory, i.e., uint8_t[33]. 1561 The argument `pk_raw` points to 96 bytes of valid memory, i.e., uint8_t[96]. 1562 1563 The function DOESN'T check whether (x, y) is a valid point. 1564 */ 1565 void 1566 Hacl_P384_raw_to_compressed(uint8_t *pk_raw, uint8_t *pk) 1567 { 1568 uint8_t *pk_x = pk_raw; 1569 uint8_t *pk_y = pk_raw + 48U; 1570 uint64_t bn_f[6U] = { 0U }; 1571 bn_from_bytes_be(bn_f, pk_y); 1572 uint64_t is_odd_f = bn_f[0U] & 1ULL; 1573 pk[0U] = (uint32_t)(uint8_t)is_odd_f + 0x02U; 1574 memcpy(pk + 1U, pk_x, 48U * sizeof(uint8_t)); 1575 } 1576 1577 /******************/ 1578 /* ECDH agreement */ 1579 /******************/ 1580 1581 /** 1582 Compute the public key from the private key. 1583 1584 The function returns `true` if a private key is valid and `false` otherwise. 1585 1586 The outparam `public_key` points to 96 bytes of valid memory, i.e., uint8_t[96]. 1587 The argument `private_key` points to 48 bytes of valid memory, i.e., uint8_t[48]. 1588 1589 The private key is valid: 1590 • 0 < `private_key` < the order of the curve. 1591 */ 1592 bool 1593 Hacl_P384_dh_initiator(uint8_t *public_key, uint8_t *private_key) 1594 { 1595 uint64_t tmp[24U] = { 0U }; 1596 uint64_t *sk = tmp; 1597 uint64_t *pk = tmp + 6U; 1598 uint64_t is_sk_valid = load_qelem_conditional(sk, private_key); 1599 point_mul_g(pk, sk); 1600 uint64_t aff_p[12U] = { 0U }; 1601 uint64_t zinv[6U] = { 0U }; 1602 uint64_t *px = pk; 1603 uint64_t *py0 = pk + 6U; 1604 uint64_t *pz = pk + 12U; 1605 uint64_t *x = aff_p; 1606 uint64_t *y = aff_p + 6U; 1607 p384_finv(zinv, pz); 1608 fmul0(x, px, zinv); 1609 fmul0(y, py0, zinv); 1610 from_mont(x, x); 1611 from_mont(y, y); 1612 uint64_t *px0 = aff_p; 1613 uint64_t *py = aff_p + 6U; 1614 bn_to_bytes_be(public_key, px0); 1615 bn_to_bytes_be(public_key + 48U, py); 1616 return is_sk_valid == 0xFFFFFFFFFFFFFFFFULL; 1617 } 1618 1619 /** 1620 Execute the diffie-hellmann key exchange. 1621 1622 The function returns `true` for successful creation of an ECDH shared secret and 1623 `false` otherwise. 1624 1625 The outparam `shared_secret` points to 96 bytes of valid memory, i.e., uint8_t[96]. 1626 The argument `their_pubkey` points to 96 bytes of valid memory, i.e., uint8_t[96]. 1627 The argument `private_key` points to 48 bytes of valid memory, i.e., uint8_t[48]. 1628 1629 The function also checks whether `private_key` and `their_pubkey` are valid. 1630 */ 1631 bool 1632 Hacl_P384_dh_responder(uint8_t *shared_secret, uint8_t *their_pubkey, uint8_t *private_key) 1633 { 1634 uint64_t tmp[192U] = { 0U }; 1635 uint64_t *sk = tmp; 1636 uint64_t *pk = tmp + 6U; 1637 uint64_t p_aff[12U] = { 0U }; 1638 uint8_t *p_x = their_pubkey; 1639 uint8_t *p_y = their_pubkey + 48U; 1640 uint64_t *bn_p_x = p_aff; 1641 uint64_t *bn_p_y = p_aff + 6U; 1642 bn_from_bytes_be(bn_p_x, p_x); 1643 bn_from_bytes_be(bn_p_y, p_y); 1644 uint64_t *px0 = p_aff; 1645 uint64_t *py0 = p_aff + 6U; 1646 uint64_t lessX = bn_is_lt_prime_mask(px0); 1647 uint64_t lessY = bn_is_lt_prime_mask(py0); 1648 uint64_t res0 = lessX & lessY; 1649 bool is_xy_valid = res0 == 0xFFFFFFFFFFFFFFFFULL; 1650 bool res; 1651 if (!is_xy_valid) { 1652 res = false; 1653 } else { 1654 uint64_t rp[6U] = { 0U }; 1655 uint64_t tx[6U] = { 0U }; 1656 uint64_t ty[6U] = { 0U }; 1657 uint64_t *px = p_aff; 1658 uint64_t *py = p_aff + 6U; 1659 to_mont(tx, px); 1660 to_mont(ty, py); 1661 uint64_t tmp1[6U] = { 0U }; 1662 fsqr0(rp, tx); 1663 fmul0(rp, rp, tx); 1664 p384_make_a_coeff(tmp1); 1665 fmul0(tmp1, tmp1, tx); 1666 fadd0(rp, tmp1, rp); 1667 p384_make_b_coeff(tmp1); 1668 fadd0(rp, tmp1, rp); 1669 fsqr0(ty, ty); 1670 uint64_t r = bn_is_eq_mask(ty, rp); 1671 uint64_t r0 = r; 1672 bool r1 = r0 == 0xFFFFFFFFFFFFFFFFULL; 1673 res = r1; 1674 } 1675 if (res) { 1676 uint64_t *px = p_aff; 1677 uint64_t *py = p_aff + 6U; 1678 uint64_t *rx = pk; 1679 uint64_t *ry = pk + 6U; 1680 uint64_t *rz = pk + 12U; 1681 to_mont(rx, px); 1682 to_mont(ry, py); 1683 p384_make_fone(rz); 1684 } 1685 bool is_pk_valid = res; 1686 uint64_t is_sk_valid = load_qelem_conditional(sk, private_key); 1687 uint64_t ss_proj[18U] = { 0U }; 1688 if (is_pk_valid) { 1689 point_mul(ss_proj, sk, pk); 1690 uint64_t aff_p[12U] = { 0U }; 1691 uint64_t zinv[6U] = { 0U }; 1692 uint64_t *px = ss_proj; 1693 uint64_t *py1 = ss_proj + 6U; 1694 uint64_t *pz = ss_proj + 12U; 1695 uint64_t *x = aff_p; 1696 uint64_t *y = aff_p + 6U; 1697 p384_finv(zinv, pz); 1698 fmul0(x, px, zinv); 1699 fmul0(y, py1, zinv); 1700 from_mont(x, x); 1701 from_mont(y, y); 1702 uint64_t *px1 = aff_p; 1703 uint64_t *py = aff_p + 6U; 1704 bn_to_bytes_be(shared_secret, px1); 1705 bn_to_bytes_be(shared_secret + 48U, py); 1706 } 1707 return is_sk_valid == 0xFFFFFFFFFFFFFFFFULL && is_pk_valid; 1708 }