Hacl_Ed25519.c (70453B)
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_Ed25519.h" 26 27 #include "internal/Hacl_Krmllib.h" 28 #include "internal/Hacl_Ed25519_PrecompTable.h" 29 #include "internal/Hacl_Curve25519_51.h" 30 #include "internal/Hacl_Bignum_Base.h" 31 #include "internal/Hacl_Bignum25519_51.h" 32 33 #include "../Hacl_Hash_SHA2_shim.h" 34 35 static inline void 36 fsum(uint64_t *out, uint64_t *a, uint64_t *b) 37 { 38 Hacl_Impl_Curve25519_Field51_fadd(out, a, b); 39 } 40 41 static inline void 42 fdifference(uint64_t *out, uint64_t *a, uint64_t *b) 43 { 44 Hacl_Impl_Curve25519_Field51_fsub(out, a, b); 45 } 46 47 void 48 Hacl_Bignum25519_reduce_513(uint64_t *a) 49 { 50 uint64_t f0 = a[0U]; 51 uint64_t f1 = a[1U]; 52 uint64_t f2 = a[2U]; 53 uint64_t f3 = a[3U]; 54 uint64_t f4 = a[4U]; 55 uint64_t l_ = f0 + (uint64_t)0U; 56 uint64_t tmp0 = l_ & (uint64_t)0x7ffffffffffffU; 57 uint64_t c0 = l_ >> (uint32_t)51U; 58 uint64_t l_0 = f1 + c0; 59 uint64_t tmp1 = l_0 & (uint64_t)0x7ffffffffffffU; 60 uint64_t c1 = l_0 >> (uint32_t)51U; 61 uint64_t l_1 = f2 + c1; 62 uint64_t tmp2 = l_1 & (uint64_t)0x7ffffffffffffU; 63 uint64_t c2 = l_1 >> (uint32_t)51U; 64 uint64_t l_2 = f3 + c2; 65 uint64_t tmp3 = l_2 & (uint64_t)0x7ffffffffffffU; 66 uint64_t c3 = l_2 >> (uint32_t)51U; 67 uint64_t l_3 = f4 + c3; 68 uint64_t tmp4 = l_3 & (uint64_t)0x7ffffffffffffU; 69 uint64_t c4 = l_3 >> (uint32_t)51U; 70 uint64_t l_4 = tmp0 + c4 * (uint64_t)19U; 71 uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU; 72 uint64_t c5 = l_4 >> (uint32_t)51U; 73 a[0U] = tmp0_; 74 a[1U] = tmp1 + c5; 75 a[2U] = tmp2; 76 a[3U] = tmp3; 77 a[4U] = tmp4; 78 } 79 80 static inline void 81 fmul0(uint64_t *output, uint64_t *input, uint64_t *input2) 82 { 83 FStar_UInt128_uint128 tmp[10U]; 84 for (uint32_t _i = 0U; _i < (uint32_t)10U; ++_i) 85 tmp[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U); 86 Hacl_Impl_Curve25519_Field51_fmul(output, input, input2, tmp); 87 } 88 89 static inline void 90 times_2(uint64_t *out, uint64_t *a) 91 { 92 uint64_t a0 = a[0U]; 93 uint64_t a1 = a[1U]; 94 uint64_t a2 = a[2U]; 95 uint64_t a3 = a[3U]; 96 uint64_t a4 = a[4U]; 97 uint64_t o0 = (uint64_t)2U * a0; 98 uint64_t o1 = (uint64_t)2U * a1; 99 uint64_t o2 = (uint64_t)2U * a2; 100 uint64_t o3 = (uint64_t)2U * a3; 101 uint64_t o4 = (uint64_t)2U * a4; 102 out[0U] = o0; 103 out[1U] = o1; 104 out[2U] = o2; 105 out[3U] = o3; 106 out[4U] = o4; 107 } 108 109 static inline void 110 times_d(uint64_t *out, uint64_t *a) 111 { 112 uint64_t d[5U] = { 0U }; 113 d[0U] = (uint64_t)0x00034dca135978a3U; 114 d[1U] = (uint64_t)0x0001a8283b156ebdU; 115 d[2U] = (uint64_t)0x0005e7a26001c029U; 116 d[3U] = (uint64_t)0x000739c663a03cbbU; 117 d[4U] = (uint64_t)0x00052036cee2b6ffU; 118 fmul0(out, d, a); 119 } 120 121 static inline void 122 times_2d(uint64_t *out, uint64_t *a) 123 { 124 uint64_t d2[5U] = { 0U }; 125 d2[0U] = (uint64_t)0x00069b9426b2f159U; 126 d2[1U] = (uint64_t)0x00035050762add7aU; 127 d2[2U] = (uint64_t)0x0003cf44c0038052U; 128 d2[3U] = (uint64_t)0x0006738cc7407977U; 129 d2[4U] = (uint64_t)0x0002406d9dc56dffU; 130 fmul0(out, d2, a); 131 } 132 133 static inline void 134 fsquare(uint64_t *out, uint64_t *a) 135 { 136 FStar_UInt128_uint128 tmp[5U]; 137 for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i) 138 tmp[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U); 139 Hacl_Impl_Curve25519_Field51_fsqr(out, a, tmp); 140 } 141 142 static inline void 143 fsquare_times(uint64_t *output, uint64_t *input, uint32_t count) 144 { 145 FStar_UInt128_uint128 tmp[5U]; 146 for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i) 147 tmp[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U); 148 Hacl_Curve25519_51_fsquare_times(output, input, tmp, count); 149 } 150 151 static inline void 152 fsquare_times_inplace(uint64_t *output, uint32_t count) 153 { 154 FStar_UInt128_uint128 tmp[5U]; 155 for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i) 156 tmp[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U); 157 Hacl_Curve25519_51_fsquare_times(output, output, tmp, count); 158 } 159 160 void 161 Hacl_Bignum25519_inverse(uint64_t *out, uint64_t *a) 162 { 163 FStar_UInt128_uint128 tmp[10U]; 164 for (uint32_t _i = 0U; _i < (uint32_t)10U; ++_i) 165 tmp[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U); 166 Hacl_Curve25519_51_finv(out, a, tmp); 167 } 168 169 static inline void 170 reduce(uint64_t *out) 171 { 172 uint64_t o0 = out[0U]; 173 uint64_t o1 = out[1U]; 174 uint64_t o2 = out[2U]; 175 uint64_t o3 = out[3U]; 176 uint64_t o4 = out[4U]; 177 uint64_t l_ = o0 + (uint64_t)0U; 178 uint64_t tmp0 = l_ & (uint64_t)0x7ffffffffffffU; 179 uint64_t c0 = l_ >> (uint32_t)51U; 180 uint64_t l_0 = o1 + c0; 181 uint64_t tmp1 = l_0 & (uint64_t)0x7ffffffffffffU; 182 uint64_t c1 = l_0 >> (uint32_t)51U; 183 uint64_t l_1 = o2 + c1; 184 uint64_t tmp2 = l_1 & (uint64_t)0x7ffffffffffffU; 185 uint64_t c2 = l_1 >> (uint32_t)51U; 186 uint64_t l_2 = o3 + c2; 187 uint64_t tmp3 = l_2 & (uint64_t)0x7ffffffffffffU; 188 uint64_t c3 = l_2 >> (uint32_t)51U; 189 uint64_t l_3 = o4 + c3; 190 uint64_t tmp4 = l_3 & (uint64_t)0x7ffffffffffffU; 191 uint64_t c4 = l_3 >> (uint32_t)51U; 192 uint64_t l_4 = tmp0 + c4 * (uint64_t)19U; 193 uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU; 194 uint64_t c5 = l_4 >> (uint32_t)51U; 195 uint64_t f0 = tmp0_; 196 uint64_t f1 = tmp1 + c5; 197 uint64_t f2 = tmp2; 198 uint64_t f3 = tmp3; 199 uint64_t f4 = tmp4; 200 uint64_t m0 = FStar_UInt64_gte_mask(f0, (uint64_t)0x7ffffffffffedU); 201 uint64_t m1 = FStar_UInt64_eq_mask(f1, (uint64_t)0x7ffffffffffffU); 202 uint64_t m2 = FStar_UInt64_eq_mask(f2, (uint64_t)0x7ffffffffffffU); 203 uint64_t m3 = FStar_UInt64_eq_mask(f3, (uint64_t)0x7ffffffffffffU); 204 uint64_t m4 = FStar_UInt64_eq_mask(f4, (uint64_t)0x7ffffffffffffU); 205 uint64_t mask = (((m0 & m1) & m2) & m3) & m4; 206 uint64_t f0_ = f0 - (mask & (uint64_t)0x7ffffffffffedU); 207 uint64_t f1_ = f1 - (mask & (uint64_t)0x7ffffffffffffU); 208 uint64_t f2_ = f2 - (mask & (uint64_t)0x7ffffffffffffU); 209 uint64_t f3_ = f3 - (mask & (uint64_t)0x7ffffffffffffU); 210 uint64_t f4_ = f4 - (mask & (uint64_t)0x7ffffffffffffU); 211 uint64_t f01 = f0_; 212 uint64_t f11 = f1_; 213 uint64_t f21 = f2_; 214 uint64_t f31 = f3_; 215 uint64_t f41 = f4_; 216 out[0U] = f01; 217 out[1U] = f11; 218 out[2U] = f21; 219 out[3U] = f31; 220 out[4U] = f41; 221 } 222 223 void 224 Hacl_Bignum25519_load_51(uint64_t *output, uint8_t *input) 225 { 226 uint64_t u64s[4U] = { 0U }; 227 KRML_MAYBE_FOR4(i, 228 (uint32_t)0U, 229 (uint32_t)4U, 230 (uint32_t)1U, 231 uint64_t *os = u64s; 232 uint8_t *bj = input + i * (uint32_t)8U; 233 uint64_t u = load64_le(bj); 234 uint64_t r = u; 235 uint64_t x = r; 236 os[i] = x;); 237 uint64_t u64s3 = u64s[3U]; 238 u64s[3U] = u64s3 & (uint64_t)0x7fffffffffffffffU; 239 output[0U] = u64s[0U] & (uint64_t)0x7ffffffffffffU; 240 output[1U] = u64s[0U] >> (uint32_t)51U | (u64s[1U] & (uint64_t)0x3fffffffffU) << (uint32_t)13U; 241 output[2U] = u64s[1U] >> (uint32_t)38U | (u64s[2U] & (uint64_t)0x1ffffffU) << (uint32_t)26U; 242 output[3U] = u64s[2U] >> (uint32_t)25U | (u64s[3U] & (uint64_t)0xfffU) << (uint32_t)39U; 243 output[4U] = u64s[3U] >> (uint32_t)12U; 244 } 245 246 void 247 Hacl_Bignum25519_store_51(uint8_t *output, uint64_t *input) 248 { 249 uint64_t u64s[4U] = { 0U }; 250 Hacl_Impl_Curve25519_Field51_store_felem(u64s, input); 251 KRML_MAYBE_FOR4(i, 252 (uint32_t)0U, 253 (uint32_t)4U, 254 (uint32_t)1U, 255 store64_le(output + i * (uint32_t)8U, u64s[i]);); 256 } 257 258 void 259 Hacl_Impl_Ed25519_PointDouble_point_double(uint64_t *out, uint64_t *p) 260 { 261 uint64_t tmp[20U] = { 0U }; 262 uint64_t *tmp1 = tmp; 263 uint64_t *tmp20 = tmp + (uint32_t)5U; 264 uint64_t *tmp30 = tmp + (uint32_t)10U; 265 uint64_t *tmp40 = tmp + (uint32_t)15U; 266 uint64_t *x10 = p; 267 uint64_t *y10 = p + (uint32_t)5U; 268 uint64_t *z1 = p + (uint32_t)10U; 269 fsquare(tmp1, x10); 270 fsquare(tmp20, y10); 271 fsum(tmp30, tmp1, tmp20); 272 fdifference(tmp40, tmp1, tmp20); 273 fsquare(tmp1, z1); 274 times_2(tmp1, tmp1); 275 uint64_t *tmp10 = tmp; 276 uint64_t *tmp2 = tmp + (uint32_t)5U; 277 uint64_t *tmp3 = tmp + (uint32_t)10U; 278 uint64_t *tmp4 = tmp + (uint32_t)15U; 279 uint64_t *x1 = p; 280 uint64_t *y1 = p + (uint32_t)5U; 281 fsum(tmp2, x1, y1); 282 fsquare(tmp2, tmp2); 283 Hacl_Bignum25519_reduce_513(tmp3); 284 fdifference(tmp2, tmp3, tmp2); 285 Hacl_Bignum25519_reduce_513(tmp10); 286 Hacl_Bignum25519_reduce_513(tmp4); 287 fsum(tmp10, tmp10, tmp4); 288 uint64_t *tmp_f = tmp; 289 uint64_t *tmp_e = tmp + (uint32_t)5U; 290 uint64_t *tmp_h = tmp + (uint32_t)10U; 291 uint64_t *tmp_g = tmp + (uint32_t)15U; 292 uint64_t *x3 = out; 293 uint64_t *y3 = out + (uint32_t)5U; 294 uint64_t *z3 = out + (uint32_t)10U; 295 uint64_t *t3 = out + (uint32_t)15U; 296 fmul0(x3, tmp_e, tmp_f); 297 fmul0(y3, tmp_g, tmp_h); 298 fmul0(t3, tmp_e, tmp_h); 299 fmul0(z3, tmp_f, tmp_g); 300 } 301 302 void 303 Hacl_Impl_Ed25519_PointAdd_point_add(uint64_t *out, uint64_t *p, uint64_t *q) 304 { 305 uint64_t tmp[30U] = { 0U }; 306 uint64_t *tmp1 = tmp; 307 uint64_t *tmp20 = tmp + (uint32_t)5U; 308 uint64_t *tmp30 = tmp + (uint32_t)10U; 309 uint64_t *tmp40 = tmp + (uint32_t)15U; 310 uint64_t *x1 = p; 311 uint64_t *y1 = p + (uint32_t)5U; 312 uint64_t *x2 = q; 313 uint64_t *y2 = q + (uint32_t)5U; 314 fdifference(tmp1, y1, x1); 315 fdifference(tmp20, y2, x2); 316 fmul0(tmp30, tmp1, tmp20); 317 fsum(tmp1, y1, x1); 318 fsum(tmp20, y2, x2); 319 fmul0(tmp40, tmp1, tmp20); 320 uint64_t *tmp10 = tmp; 321 uint64_t *tmp2 = tmp + (uint32_t)5U; 322 uint64_t *tmp3 = tmp + (uint32_t)10U; 323 uint64_t *tmp4 = tmp + (uint32_t)15U; 324 uint64_t *tmp5 = tmp + (uint32_t)20U; 325 uint64_t *tmp6 = tmp + (uint32_t)25U; 326 uint64_t *z1 = p + (uint32_t)10U; 327 uint64_t *t1 = p + (uint32_t)15U; 328 uint64_t *z2 = q + (uint32_t)10U; 329 uint64_t *t2 = q + (uint32_t)15U; 330 times_2d(tmp10, t1); 331 fmul0(tmp10, tmp10, t2); 332 times_2(tmp2, z1); 333 fmul0(tmp2, tmp2, z2); 334 fdifference(tmp5, tmp4, tmp3); 335 fdifference(tmp6, tmp2, tmp10); 336 fsum(tmp10, tmp2, tmp10); 337 fsum(tmp2, tmp4, tmp3); 338 uint64_t *tmp_g = tmp; 339 uint64_t *tmp_h = tmp + (uint32_t)5U; 340 uint64_t *tmp_e = tmp + (uint32_t)20U; 341 uint64_t *tmp_f = tmp + (uint32_t)25U; 342 uint64_t *x3 = out; 343 uint64_t *y3 = out + (uint32_t)5U; 344 uint64_t *z3 = out + (uint32_t)10U; 345 uint64_t *t3 = out + (uint32_t)15U; 346 fmul0(x3, tmp_e, tmp_f); 347 fmul0(y3, tmp_g, tmp_h); 348 fmul0(t3, tmp_e, tmp_h); 349 fmul0(z3, tmp_f, tmp_g); 350 } 351 352 void 353 Hacl_Impl_Ed25519_PointConstants_make_point_inf(uint64_t *b) 354 { 355 uint64_t *x = b; 356 uint64_t *y = b + (uint32_t)5U; 357 uint64_t *z = b + (uint32_t)10U; 358 uint64_t *t = b + (uint32_t)15U; 359 x[0U] = (uint64_t)0U; 360 x[1U] = (uint64_t)0U; 361 x[2U] = (uint64_t)0U; 362 x[3U] = (uint64_t)0U; 363 x[4U] = (uint64_t)0U; 364 y[0U] = (uint64_t)1U; 365 y[1U] = (uint64_t)0U; 366 y[2U] = (uint64_t)0U; 367 y[3U] = (uint64_t)0U; 368 y[4U] = (uint64_t)0U; 369 z[0U] = (uint64_t)1U; 370 z[1U] = (uint64_t)0U; 371 z[2U] = (uint64_t)0U; 372 z[3U] = (uint64_t)0U; 373 z[4U] = (uint64_t)0U; 374 t[0U] = (uint64_t)0U; 375 t[1U] = (uint64_t)0U; 376 t[2U] = (uint64_t)0U; 377 t[3U] = (uint64_t)0U; 378 t[4U] = (uint64_t)0U; 379 } 380 381 static inline void 382 pow2_252m2(uint64_t *out, uint64_t *z) 383 { 384 uint64_t buf[20U] = { 0U }; 385 uint64_t *a = buf; 386 uint64_t *t00 = buf + (uint32_t)5U; 387 uint64_t *b0 = buf + (uint32_t)10U; 388 uint64_t *c0 = buf + (uint32_t)15U; 389 fsquare_times(a, z, (uint32_t)1U); 390 fsquare_times(t00, a, (uint32_t)2U); 391 fmul0(b0, t00, z); 392 fmul0(a, b0, a); 393 fsquare_times(t00, a, (uint32_t)1U); 394 fmul0(b0, t00, b0); 395 fsquare_times(t00, b0, (uint32_t)5U); 396 fmul0(b0, t00, b0); 397 fsquare_times(t00, b0, (uint32_t)10U); 398 fmul0(c0, t00, b0); 399 fsquare_times(t00, c0, (uint32_t)20U); 400 fmul0(t00, t00, c0); 401 fsquare_times_inplace(t00, (uint32_t)10U); 402 fmul0(b0, t00, b0); 403 fsquare_times(t00, b0, (uint32_t)50U); 404 uint64_t *a0 = buf; 405 uint64_t *t0 = buf + (uint32_t)5U; 406 uint64_t *b = buf + (uint32_t)10U; 407 uint64_t *c = buf + (uint32_t)15U; 408 fsquare_times(a0, z, (uint32_t)1U); 409 fmul0(c, t0, b); 410 fsquare_times(t0, c, (uint32_t)100U); 411 fmul0(t0, t0, c); 412 fsquare_times_inplace(t0, (uint32_t)50U); 413 fmul0(t0, t0, b); 414 fsquare_times_inplace(t0, (uint32_t)2U); 415 fmul0(out, t0, a0); 416 } 417 418 static inline bool 419 is_0(uint64_t *x) 420 { 421 uint64_t x0 = x[0U]; 422 uint64_t x1 = x[1U]; 423 uint64_t x2 = x[2U]; 424 uint64_t x3 = x[3U]; 425 uint64_t x4 = x[4U]; 426 return x0 == (uint64_t)0U && x1 == (uint64_t)0U && x2 == (uint64_t)0U && x3 == (uint64_t)0U && x4 == (uint64_t)0U; 427 } 428 429 static inline void 430 mul_modp_sqrt_m1(uint64_t *x) 431 { 432 uint64_t sqrt_m1[5U] = { 0U }; 433 sqrt_m1[0U] = (uint64_t)0x00061b274a0ea0b0U; 434 sqrt_m1[1U] = (uint64_t)0x0000d5a5fc8f189dU; 435 sqrt_m1[2U] = (uint64_t)0x0007ef5e9cbd0c60U; 436 sqrt_m1[3U] = (uint64_t)0x00078595a6804c9eU; 437 sqrt_m1[4U] = (uint64_t)0x0002b8324804fc1dU; 438 fmul0(x, x, sqrt_m1); 439 } 440 441 static inline bool 442 recover_x(uint64_t *x, uint64_t *y, uint64_t sign) 443 { 444 uint64_t tmp[15U] = { 0U }; 445 uint64_t *x2 = tmp; 446 uint64_t x00 = y[0U]; 447 uint64_t x1 = y[1U]; 448 uint64_t x21 = y[2U]; 449 uint64_t x30 = y[3U]; 450 uint64_t x4 = y[4U]; 451 bool 452 b = 453 x00 >= (uint64_t)0x7ffffffffffedU && x1 == (uint64_t)0x7ffffffffffffU && x21 == (uint64_t)0x7ffffffffffffU && x30 == (uint64_t)0x7ffffffffffffU && x4 == (uint64_t)0x7ffffffffffffU; 454 bool res; 455 if (b) { 456 res = false; 457 } else { 458 uint64_t tmp1[20U] = { 0U }; 459 uint64_t *one = tmp1; 460 uint64_t *y2 = tmp1 + (uint32_t)5U; 461 uint64_t *dyyi = tmp1 + (uint32_t)10U; 462 uint64_t *dyy = tmp1 + (uint32_t)15U; 463 one[0U] = (uint64_t)1U; 464 one[1U] = (uint64_t)0U; 465 one[2U] = (uint64_t)0U; 466 one[3U] = (uint64_t)0U; 467 one[4U] = (uint64_t)0U; 468 fsquare(y2, y); 469 times_d(dyy, y2); 470 fsum(dyy, dyy, one); 471 Hacl_Bignum25519_reduce_513(dyy); 472 Hacl_Bignum25519_inverse(dyyi, dyy); 473 fdifference(x2, y2, one); 474 fmul0(x2, x2, dyyi); 475 reduce(x2); 476 bool x2_is_0 = is_0(x2); 477 uint8_t z; 478 if (x2_is_0) { 479 if (sign == (uint64_t)0U) { 480 x[0U] = (uint64_t)0U; 481 x[1U] = (uint64_t)0U; 482 x[2U] = (uint64_t)0U; 483 x[3U] = (uint64_t)0U; 484 x[4U] = (uint64_t)0U; 485 z = (uint8_t)1U; 486 } else { 487 z = (uint8_t)0U; 488 } 489 } else { 490 z = (uint8_t)2U; 491 } 492 if (z == (uint8_t)0U) { 493 res = false; 494 } else if (z == (uint8_t)1U) { 495 res = true; 496 } else { 497 uint64_t *x210 = tmp; 498 uint64_t *x31 = tmp + (uint32_t)5U; 499 uint64_t *t00 = tmp + (uint32_t)10U; 500 pow2_252m2(x31, x210); 501 fsquare(t00, x31); 502 fdifference(t00, t00, x210); 503 Hacl_Bignum25519_reduce_513(t00); 504 reduce(t00); 505 bool t0_is_0 = is_0(t00); 506 if (!t0_is_0) { 507 mul_modp_sqrt_m1(x31); 508 } 509 uint64_t *x211 = tmp; 510 uint64_t *x3 = tmp + (uint32_t)5U; 511 uint64_t *t01 = tmp + (uint32_t)10U; 512 fsquare(t01, x3); 513 fdifference(t01, t01, x211); 514 Hacl_Bignum25519_reduce_513(t01); 515 reduce(t01); 516 bool z1 = is_0(t01); 517 if (z1 == false) { 518 res = false; 519 } else { 520 uint64_t *x32 = tmp + (uint32_t)5U; 521 uint64_t *t0 = tmp + (uint32_t)10U; 522 reduce(x32); 523 uint64_t x0 = x32[0U]; 524 uint64_t x01 = x0 & (uint64_t)1U; 525 if (!(x01 == sign)) { 526 t0[0U] = (uint64_t)0U; 527 t0[1U] = (uint64_t)0U; 528 t0[2U] = (uint64_t)0U; 529 t0[3U] = (uint64_t)0U; 530 t0[4U] = (uint64_t)0U; 531 fdifference(x32, t0, x32); 532 Hacl_Bignum25519_reduce_513(x32); 533 reduce(x32); 534 } 535 memcpy(x, x32, (uint32_t)5U * sizeof(uint64_t)); 536 res = true; 537 } 538 } 539 } 540 bool res0 = res; 541 return res0; 542 } 543 544 bool 545 Hacl_Impl_Ed25519_PointDecompress_point_decompress(uint64_t *out, uint8_t *s) 546 { 547 uint64_t tmp[10U] = { 0U }; 548 uint64_t *y = tmp; 549 uint64_t *x = tmp + (uint32_t)5U; 550 uint8_t s31 = s[31U]; 551 uint8_t z = s31 >> (uint32_t)7U; 552 uint64_t sign = (uint64_t)z; 553 Hacl_Bignum25519_load_51(y, s); 554 bool z0 = recover_x(x, y, sign); 555 bool res; 556 if (z0 == false) { 557 res = false; 558 } else { 559 uint64_t *outx = out; 560 uint64_t *outy = out + (uint32_t)5U; 561 uint64_t *outz = out + (uint32_t)10U; 562 uint64_t *outt = out + (uint32_t)15U; 563 memcpy(outx, x, (uint32_t)5U * sizeof(uint64_t)); 564 memcpy(outy, y, (uint32_t)5U * sizeof(uint64_t)); 565 outz[0U] = (uint64_t)1U; 566 outz[1U] = (uint64_t)0U; 567 outz[2U] = (uint64_t)0U; 568 outz[3U] = (uint64_t)0U; 569 outz[4U] = (uint64_t)0U; 570 fmul0(outt, x, y); 571 res = true; 572 } 573 bool res0 = res; 574 return res0; 575 } 576 577 void 578 Hacl_Impl_Ed25519_PointCompress_point_compress(uint8_t *z, uint64_t *p) 579 { 580 uint64_t tmp[15U] = { 0U }; 581 uint64_t *x = tmp + (uint32_t)5U; 582 uint64_t *out = tmp + (uint32_t)10U; 583 uint64_t *zinv1 = tmp; 584 uint64_t *x1 = tmp + (uint32_t)5U; 585 uint64_t *out1 = tmp + (uint32_t)10U; 586 uint64_t *px = p; 587 uint64_t *py = p + (uint32_t)5U; 588 uint64_t *pz = p + (uint32_t)10U; 589 Hacl_Bignum25519_inverse(zinv1, pz); 590 fmul0(x1, px, zinv1); 591 reduce(x1); 592 fmul0(out1, py, zinv1); 593 Hacl_Bignum25519_reduce_513(out1); 594 uint64_t x0 = x[0U]; 595 uint64_t b = x0 & (uint64_t)1U; 596 Hacl_Bignum25519_store_51(z, out); 597 uint8_t xbyte = (uint8_t)b; 598 uint8_t o31 = z[31U]; 599 z[31U] = o31 + (xbyte << (uint32_t)7U); 600 } 601 602 static inline void 603 barrett_reduction(uint64_t *z, uint64_t *t) 604 { 605 uint64_t t0 = t[0U]; 606 uint64_t t1 = t[1U]; 607 uint64_t t2 = t[2U]; 608 uint64_t t3 = t[3U]; 609 uint64_t t4 = t[4U]; 610 uint64_t t5 = t[5U]; 611 uint64_t t6 = t[6U]; 612 uint64_t t7 = t[7U]; 613 uint64_t t8 = t[8U]; 614 uint64_t t9 = t[9U]; 615 uint64_t m00 = (uint64_t)0x12631a5cf5d3edU; 616 uint64_t m10 = (uint64_t)0xf9dea2f79cd658U; 617 uint64_t m20 = (uint64_t)0x000000000014deU; 618 uint64_t m30 = (uint64_t)0x00000000000000U; 619 uint64_t m40 = (uint64_t)0x00000010000000U; 620 uint64_t m0 = m00; 621 uint64_t m1 = m10; 622 uint64_t m2 = m20; 623 uint64_t m3 = m30; 624 uint64_t m4 = m40; 625 uint64_t m010 = (uint64_t)0x9ce5a30a2c131bU; 626 uint64_t m110 = (uint64_t)0x215d086329a7edU; 627 uint64_t m210 = (uint64_t)0xffffffffeb2106U; 628 uint64_t m310 = (uint64_t)0xffffffffffffffU; 629 uint64_t m410 = (uint64_t)0x00000fffffffffU; 630 uint64_t mu0 = m010; 631 uint64_t mu1 = m110; 632 uint64_t mu2 = m210; 633 uint64_t mu3 = m310; 634 uint64_t mu4 = m410; 635 uint64_t y_ = (t5 & (uint64_t)0xffffffU) << (uint32_t)32U; 636 uint64_t x_ = t4 >> (uint32_t)24U; 637 uint64_t z00 = x_ | y_; 638 uint64_t y_0 = (t6 & (uint64_t)0xffffffU) << (uint32_t)32U; 639 uint64_t x_0 = t5 >> (uint32_t)24U; 640 uint64_t z10 = x_0 | y_0; 641 uint64_t y_1 = (t7 & (uint64_t)0xffffffU) << (uint32_t)32U; 642 uint64_t x_1 = t6 >> (uint32_t)24U; 643 uint64_t z20 = x_1 | y_1; 644 uint64_t y_2 = (t8 & (uint64_t)0xffffffU) << (uint32_t)32U; 645 uint64_t x_2 = t7 >> (uint32_t)24U; 646 uint64_t z30 = x_2 | y_2; 647 uint64_t y_3 = (t9 & (uint64_t)0xffffffU) << (uint32_t)32U; 648 uint64_t x_3 = t8 >> (uint32_t)24U; 649 uint64_t z40 = x_3 | y_3; 650 uint64_t q0 = z00; 651 uint64_t q1 = z10; 652 uint64_t q2 = z20; 653 uint64_t q3 = z30; 654 uint64_t q4 = z40; 655 FStar_UInt128_uint128 xy000 = FStar_UInt128_mul_wide(q0, mu0); 656 FStar_UInt128_uint128 xy010 = FStar_UInt128_mul_wide(q0, mu1); 657 FStar_UInt128_uint128 xy020 = FStar_UInt128_mul_wide(q0, mu2); 658 FStar_UInt128_uint128 xy030 = FStar_UInt128_mul_wide(q0, mu3); 659 FStar_UInt128_uint128 xy040 = FStar_UInt128_mul_wide(q0, mu4); 660 FStar_UInt128_uint128 xy100 = FStar_UInt128_mul_wide(q1, mu0); 661 FStar_UInt128_uint128 xy110 = FStar_UInt128_mul_wide(q1, mu1); 662 FStar_UInt128_uint128 xy120 = FStar_UInt128_mul_wide(q1, mu2); 663 FStar_UInt128_uint128 xy130 = FStar_UInt128_mul_wide(q1, mu3); 664 FStar_UInt128_uint128 xy14 = FStar_UInt128_mul_wide(q1, mu4); 665 FStar_UInt128_uint128 xy200 = FStar_UInt128_mul_wide(q2, mu0); 666 FStar_UInt128_uint128 xy210 = FStar_UInt128_mul_wide(q2, mu1); 667 FStar_UInt128_uint128 xy220 = FStar_UInt128_mul_wide(q2, mu2); 668 FStar_UInt128_uint128 xy23 = FStar_UInt128_mul_wide(q2, mu3); 669 FStar_UInt128_uint128 xy24 = FStar_UInt128_mul_wide(q2, mu4); 670 FStar_UInt128_uint128 xy300 = FStar_UInt128_mul_wide(q3, mu0); 671 FStar_UInt128_uint128 xy310 = FStar_UInt128_mul_wide(q3, mu1); 672 FStar_UInt128_uint128 xy32 = FStar_UInt128_mul_wide(q3, mu2); 673 FStar_UInt128_uint128 xy33 = FStar_UInt128_mul_wide(q3, mu3); 674 FStar_UInt128_uint128 xy34 = FStar_UInt128_mul_wide(q3, mu4); 675 FStar_UInt128_uint128 xy400 = FStar_UInt128_mul_wide(q4, mu0); 676 FStar_UInt128_uint128 xy41 = FStar_UInt128_mul_wide(q4, mu1); 677 FStar_UInt128_uint128 xy42 = FStar_UInt128_mul_wide(q4, mu2); 678 FStar_UInt128_uint128 xy43 = FStar_UInt128_mul_wide(q4, mu3); 679 FStar_UInt128_uint128 xy44 = FStar_UInt128_mul_wide(q4, mu4); 680 FStar_UInt128_uint128 z01 = xy000; 681 FStar_UInt128_uint128 z11 = FStar_UInt128_add_mod(xy010, xy100); 682 FStar_UInt128_uint128 z21 = FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy020, xy110), xy200); 683 FStar_UInt128_uint128 684 z31 = 685 FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy030, xy120), xy210), 686 xy300); 687 FStar_UInt128_uint128 688 z41 = 689 FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy040, 690 xy130), 691 xy220), 692 xy310), 693 xy400); 694 FStar_UInt128_uint128 695 z5 = 696 FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy14, xy23), xy32), 697 xy41); 698 FStar_UInt128_uint128 z6 = FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy24, xy33), xy42); 699 FStar_UInt128_uint128 z7 = FStar_UInt128_add_mod(xy34, xy43); 700 FStar_UInt128_uint128 z8 = xy44; 701 FStar_UInt128_uint128 carry0 = FStar_UInt128_shift_right(z01, (uint32_t)56U); 702 FStar_UInt128_uint128 c00 = carry0; 703 FStar_UInt128_uint128 704 carry1 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z11, c00), (uint32_t)56U); 705 FStar_UInt128_uint128 c10 = carry1; 706 FStar_UInt128_uint128 707 carry2 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z21, c10), (uint32_t)56U); 708 FStar_UInt128_uint128 c20 = carry2; 709 FStar_UInt128_uint128 710 carry3 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z31, c20), (uint32_t)56U); 711 FStar_UInt128_uint128 c30 = carry3; 712 FStar_UInt128_uint128 713 carry4 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z41, c30), (uint32_t)56U); 714 uint64_t 715 t100 = 716 FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z41, c30)) & (uint64_t)0xffffffffffffffU; 717 FStar_UInt128_uint128 c40 = carry4; 718 uint64_t t410 = t100; 719 FStar_UInt128_uint128 720 carry5 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z5, c40), (uint32_t)56U); 721 uint64_t 722 t101 = 723 FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z5, c40)) & (uint64_t)0xffffffffffffffU; 724 FStar_UInt128_uint128 c5 = carry5; 725 uint64_t t51 = t101; 726 FStar_UInt128_uint128 727 carry6 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z6, c5), (uint32_t)56U); 728 uint64_t 729 t102 = 730 FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z6, c5)) & (uint64_t)0xffffffffffffffU; 731 FStar_UInt128_uint128 c6 = carry6; 732 uint64_t t61 = t102; 733 FStar_UInt128_uint128 734 carry7 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z7, c6), (uint32_t)56U); 735 uint64_t 736 t103 = 737 FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z7, c6)) & (uint64_t)0xffffffffffffffU; 738 FStar_UInt128_uint128 c7 = carry7; 739 uint64_t t71 = t103; 740 FStar_UInt128_uint128 741 carry8 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z8, c7), (uint32_t)56U); 742 uint64_t 743 t104 = 744 FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z8, c7)) & (uint64_t)0xffffffffffffffU; 745 FStar_UInt128_uint128 c8 = carry8; 746 uint64_t t81 = t104; 747 uint64_t t91 = FStar_UInt128_uint128_to_uint64(c8); 748 uint64_t qmu4_ = t410; 749 uint64_t qmu5_ = t51; 750 uint64_t qmu6_ = t61; 751 uint64_t qmu7_ = t71; 752 uint64_t qmu8_ = t81; 753 uint64_t qmu9_ = t91; 754 uint64_t y_4 = (qmu5_ & (uint64_t)0xffffffffffU) << (uint32_t)16U; 755 uint64_t x_4 = qmu4_ >> (uint32_t)40U; 756 uint64_t z02 = x_4 | y_4; 757 uint64_t y_5 = (qmu6_ & (uint64_t)0xffffffffffU) << (uint32_t)16U; 758 uint64_t x_5 = qmu5_ >> (uint32_t)40U; 759 uint64_t z12 = x_5 | y_5; 760 uint64_t y_6 = (qmu7_ & (uint64_t)0xffffffffffU) << (uint32_t)16U; 761 uint64_t x_6 = qmu6_ >> (uint32_t)40U; 762 uint64_t z22 = x_6 | y_6; 763 uint64_t y_7 = (qmu8_ & (uint64_t)0xffffffffffU) << (uint32_t)16U; 764 uint64_t x_7 = qmu7_ >> (uint32_t)40U; 765 uint64_t z32 = x_7 | y_7; 766 uint64_t y_8 = (qmu9_ & (uint64_t)0xffffffffffU) << (uint32_t)16U; 767 uint64_t x_8 = qmu8_ >> (uint32_t)40U; 768 uint64_t z42 = x_8 | y_8; 769 uint64_t qdiv0 = z02; 770 uint64_t qdiv1 = z12; 771 uint64_t qdiv2 = z22; 772 uint64_t qdiv3 = z32; 773 uint64_t qdiv4 = z42; 774 uint64_t r0 = t0; 775 uint64_t r1 = t1; 776 uint64_t r2 = t2; 777 uint64_t r3 = t3; 778 uint64_t r4 = t4 & (uint64_t)0xffffffffffU; 779 FStar_UInt128_uint128 xy00 = FStar_UInt128_mul_wide(qdiv0, m0); 780 FStar_UInt128_uint128 xy01 = FStar_UInt128_mul_wide(qdiv0, m1); 781 FStar_UInt128_uint128 xy02 = FStar_UInt128_mul_wide(qdiv0, m2); 782 FStar_UInt128_uint128 xy03 = FStar_UInt128_mul_wide(qdiv0, m3); 783 FStar_UInt128_uint128 xy04 = FStar_UInt128_mul_wide(qdiv0, m4); 784 FStar_UInt128_uint128 xy10 = FStar_UInt128_mul_wide(qdiv1, m0); 785 FStar_UInt128_uint128 xy11 = FStar_UInt128_mul_wide(qdiv1, m1); 786 FStar_UInt128_uint128 xy12 = FStar_UInt128_mul_wide(qdiv1, m2); 787 FStar_UInt128_uint128 xy13 = FStar_UInt128_mul_wide(qdiv1, m3); 788 FStar_UInt128_uint128 xy20 = FStar_UInt128_mul_wide(qdiv2, m0); 789 FStar_UInt128_uint128 xy21 = FStar_UInt128_mul_wide(qdiv2, m1); 790 FStar_UInt128_uint128 xy22 = FStar_UInt128_mul_wide(qdiv2, m2); 791 FStar_UInt128_uint128 xy30 = FStar_UInt128_mul_wide(qdiv3, m0); 792 FStar_UInt128_uint128 xy31 = FStar_UInt128_mul_wide(qdiv3, m1); 793 FStar_UInt128_uint128 xy40 = FStar_UInt128_mul_wide(qdiv4, m0); 794 FStar_UInt128_uint128 carry9 = FStar_UInt128_shift_right(xy00, (uint32_t)56U); 795 uint64_t t105 = FStar_UInt128_uint128_to_uint64(xy00) & (uint64_t)0xffffffffffffffU; 796 FStar_UInt128_uint128 c0 = carry9; 797 uint64_t t010 = t105; 798 FStar_UInt128_uint128 799 carry10 = 800 FStar_UInt128_shift_right(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy01, xy10), c0), 801 (uint32_t)56U); 802 uint64_t 803 t106 = 804 FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy01, xy10), c0)) & (uint64_t)0xffffffffffffffU; 805 FStar_UInt128_uint128 c11 = carry10; 806 uint64_t t110 = t106; 807 FStar_UInt128_uint128 808 carry11 = 809 FStar_UInt128_shift_right(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy02, 810 xy11), 811 xy20), 812 c11), 813 (uint32_t)56U); 814 uint64_t 815 t107 = 816 FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy02, 817 xy11), 818 xy20), 819 c11)) & 820 (uint64_t)0xffffffffffffffU; 821 FStar_UInt128_uint128 c21 = carry11; 822 uint64_t t210 = t107; 823 FStar_UInt128_uint128 824 carry = 825 FStar_UInt128_shift_right(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy03, 826 xy12), 827 xy21), 828 xy30), 829 c21), 830 (uint32_t)56U); 831 uint64_t 832 t108 = 833 FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy03, 834 xy12), 835 xy21), 836 xy30), 837 c21)) & 838 (uint64_t)0xffffffffffffffU; 839 FStar_UInt128_uint128 c31 = carry; 840 uint64_t t310 = t108; 841 uint64_t 842 t411 = 843 FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy04, 844 xy13), 845 xy22), 846 xy31), 847 xy40), 848 c31)) & 849 (uint64_t)0xffffffffffU; 850 uint64_t qmul0 = t010; 851 uint64_t qmul1 = t110; 852 uint64_t qmul2 = t210; 853 uint64_t qmul3 = t310; 854 uint64_t qmul4 = t411; 855 uint64_t b5 = (r0 - qmul0) >> (uint32_t)63U; 856 uint64_t t109 = (b5 << (uint32_t)56U) + r0 - qmul0; 857 uint64_t c1 = b5; 858 uint64_t t011 = t109; 859 uint64_t b6 = (r1 - (qmul1 + c1)) >> (uint32_t)63U; 860 uint64_t t1010 = (b6 << (uint32_t)56U) + r1 - (qmul1 + c1); 861 uint64_t c2 = b6; 862 uint64_t t111 = t1010; 863 uint64_t b7 = (r2 - (qmul2 + c2)) >> (uint32_t)63U; 864 uint64_t t1011 = (b7 << (uint32_t)56U) + r2 - (qmul2 + c2); 865 uint64_t c3 = b7; 866 uint64_t t211 = t1011; 867 uint64_t b8 = (r3 - (qmul3 + c3)) >> (uint32_t)63U; 868 uint64_t t1012 = (b8 << (uint32_t)56U) + r3 - (qmul3 + c3); 869 uint64_t c4 = b8; 870 uint64_t t311 = t1012; 871 uint64_t b9 = (r4 - (qmul4 + c4)) >> (uint32_t)63U; 872 uint64_t t1013 = (b9 << (uint32_t)40U) + r4 - (qmul4 + c4); 873 uint64_t t412 = t1013; 874 uint64_t s0 = t011; 875 uint64_t s1 = t111; 876 uint64_t s2 = t211; 877 uint64_t s3 = t311; 878 uint64_t s4 = t412; 879 uint64_t m01 = (uint64_t)0x12631a5cf5d3edU; 880 uint64_t m11 = (uint64_t)0xf9dea2f79cd658U; 881 uint64_t m21 = (uint64_t)0x000000000014deU; 882 uint64_t m31 = (uint64_t)0x00000000000000U; 883 uint64_t m41 = (uint64_t)0x00000010000000U; 884 uint64_t y0 = m01; 885 uint64_t y1 = m11; 886 uint64_t y2 = m21; 887 uint64_t y3 = m31; 888 uint64_t y4 = m41; 889 uint64_t b10 = (s0 - y0) >> (uint32_t)63U; 890 uint64_t t1014 = (b10 << (uint32_t)56U) + s0 - y0; 891 uint64_t b0 = b10; 892 uint64_t t01 = t1014; 893 uint64_t b11 = (s1 - (y1 + b0)) >> (uint32_t)63U; 894 uint64_t t1015 = (b11 << (uint32_t)56U) + s1 - (y1 + b0); 895 uint64_t b1 = b11; 896 uint64_t t11 = t1015; 897 uint64_t b12 = (s2 - (y2 + b1)) >> (uint32_t)63U; 898 uint64_t t1016 = (b12 << (uint32_t)56U) + s2 - (y2 + b1); 899 uint64_t b2 = b12; 900 uint64_t t21 = t1016; 901 uint64_t b13 = (s3 - (y3 + b2)) >> (uint32_t)63U; 902 uint64_t t1017 = (b13 << (uint32_t)56U) + s3 - (y3 + b2); 903 uint64_t b3 = b13; 904 uint64_t t31 = t1017; 905 uint64_t b = (s4 - (y4 + b3)) >> (uint32_t)63U; 906 uint64_t t10 = (b << (uint32_t)56U) + s4 - (y4 + b3); 907 uint64_t b4 = b; 908 uint64_t t41 = t10; 909 uint64_t mask = b4 - (uint64_t)1U; 910 uint64_t z03 = s0 ^ (mask & (s0 ^ t01)); 911 uint64_t z13 = s1 ^ (mask & (s1 ^ t11)); 912 uint64_t z23 = s2 ^ (mask & (s2 ^ t21)); 913 uint64_t z33 = s3 ^ (mask & (s3 ^ t31)); 914 uint64_t z43 = s4 ^ (mask & (s4 ^ t41)); 915 uint64_t z04 = z03; 916 uint64_t z14 = z13; 917 uint64_t z24 = z23; 918 uint64_t z34 = z33; 919 uint64_t z44 = z43; 920 uint64_t o0 = z04; 921 uint64_t o1 = z14; 922 uint64_t o2 = z24; 923 uint64_t o3 = z34; 924 uint64_t o4 = z44; 925 uint64_t z0 = o0; 926 uint64_t z1 = o1; 927 uint64_t z2 = o2; 928 uint64_t z3 = o3; 929 uint64_t z4 = o4; 930 z[0U] = z0; 931 z[1U] = z1; 932 z[2U] = z2; 933 z[3U] = z3; 934 z[4U] = z4; 935 } 936 937 static inline void 938 mul_modq(uint64_t *out, uint64_t *x, uint64_t *y) 939 { 940 uint64_t tmp[10U] = { 0U }; 941 uint64_t x0 = x[0U]; 942 uint64_t x1 = x[1U]; 943 uint64_t x2 = x[2U]; 944 uint64_t x3 = x[3U]; 945 uint64_t x4 = x[4U]; 946 uint64_t y0 = y[0U]; 947 uint64_t y1 = y[1U]; 948 uint64_t y2 = y[2U]; 949 uint64_t y3 = y[3U]; 950 uint64_t y4 = y[4U]; 951 FStar_UInt128_uint128 xy00 = FStar_UInt128_mul_wide(x0, y0); 952 FStar_UInt128_uint128 xy01 = FStar_UInt128_mul_wide(x0, y1); 953 FStar_UInt128_uint128 xy02 = FStar_UInt128_mul_wide(x0, y2); 954 FStar_UInt128_uint128 xy03 = FStar_UInt128_mul_wide(x0, y3); 955 FStar_UInt128_uint128 xy04 = FStar_UInt128_mul_wide(x0, y4); 956 FStar_UInt128_uint128 xy10 = FStar_UInt128_mul_wide(x1, y0); 957 FStar_UInt128_uint128 xy11 = FStar_UInt128_mul_wide(x1, y1); 958 FStar_UInt128_uint128 xy12 = FStar_UInt128_mul_wide(x1, y2); 959 FStar_UInt128_uint128 xy13 = FStar_UInt128_mul_wide(x1, y3); 960 FStar_UInt128_uint128 xy14 = FStar_UInt128_mul_wide(x1, y4); 961 FStar_UInt128_uint128 xy20 = FStar_UInt128_mul_wide(x2, y0); 962 FStar_UInt128_uint128 xy21 = FStar_UInt128_mul_wide(x2, y1); 963 FStar_UInt128_uint128 xy22 = FStar_UInt128_mul_wide(x2, y2); 964 FStar_UInt128_uint128 xy23 = FStar_UInt128_mul_wide(x2, y3); 965 FStar_UInt128_uint128 xy24 = FStar_UInt128_mul_wide(x2, y4); 966 FStar_UInt128_uint128 xy30 = FStar_UInt128_mul_wide(x3, y0); 967 FStar_UInt128_uint128 xy31 = FStar_UInt128_mul_wide(x3, y1); 968 FStar_UInt128_uint128 xy32 = FStar_UInt128_mul_wide(x3, y2); 969 FStar_UInt128_uint128 xy33 = FStar_UInt128_mul_wide(x3, y3); 970 FStar_UInt128_uint128 xy34 = FStar_UInt128_mul_wide(x3, y4); 971 FStar_UInt128_uint128 xy40 = FStar_UInt128_mul_wide(x4, y0); 972 FStar_UInt128_uint128 xy41 = FStar_UInt128_mul_wide(x4, y1); 973 FStar_UInt128_uint128 xy42 = FStar_UInt128_mul_wide(x4, y2); 974 FStar_UInt128_uint128 xy43 = FStar_UInt128_mul_wide(x4, y3); 975 FStar_UInt128_uint128 xy44 = FStar_UInt128_mul_wide(x4, y4); 976 FStar_UInt128_uint128 z00 = xy00; 977 FStar_UInt128_uint128 z10 = FStar_UInt128_add_mod(xy01, xy10); 978 FStar_UInt128_uint128 z20 = FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy02, xy11), xy20); 979 FStar_UInt128_uint128 980 z30 = 981 FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy03, xy12), xy21), 982 xy30); 983 FStar_UInt128_uint128 984 z40 = 985 FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy04, 986 xy13), 987 xy22), 988 xy31), 989 xy40); 990 FStar_UInt128_uint128 991 z50 = 992 FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy14, xy23), xy32), 993 xy41); 994 FStar_UInt128_uint128 z60 = FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy24, xy33), xy42); 995 FStar_UInt128_uint128 z70 = FStar_UInt128_add_mod(xy34, xy43); 996 FStar_UInt128_uint128 z80 = xy44; 997 FStar_UInt128_uint128 carry0 = FStar_UInt128_shift_right(z00, (uint32_t)56U); 998 uint64_t t10 = FStar_UInt128_uint128_to_uint64(z00) & (uint64_t)0xffffffffffffffU; 999 FStar_UInt128_uint128 c0 = carry0; 1000 uint64_t t0 = t10; 1001 FStar_UInt128_uint128 1002 carry1 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z10, c0), (uint32_t)56U); 1003 uint64_t 1004 t11 = 1005 FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z10, c0)) & (uint64_t)0xffffffffffffffU; 1006 FStar_UInt128_uint128 c1 = carry1; 1007 uint64_t t1 = t11; 1008 FStar_UInt128_uint128 1009 carry2 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z20, c1), (uint32_t)56U); 1010 uint64_t 1011 t12 = 1012 FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z20, c1)) & (uint64_t)0xffffffffffffffU; 1013 FStar_UInt128_uint128 c2 = carry2; 1014 uint64_t t2 = t12; 1015 FStar_UInt128_uint128 1016 carry3 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z30, c2), (uint32_t)56U); 1017 uint64_t 1018 t13 = 1019 FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z30, c2)) & (uint64_t)0xffffffffffffffU; 1020 FStar_UInt128_uint128 c3 = carry3; 1021 uint64_t t3 = t13; 1022 FStar_UInt128_uint128 1023 carry4 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z40, c3), (uint32_t)56U); 1024 uint64_t 1025 t14 = 1026 FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z40, c3)) & (uint64_t)0xffffffffffffffU; 1027 FStar_UInt128_uint128 c4 = carry4; 1028 uint64_t t4 = t14; 1029 FStar_UInt128_uint128 1030 carry5 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z50, c4), (uint32_t)56U); 1031 uint64_t 1032 t15 = 1033 FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z50, c4)) & (uint64_t)0xffffffffffffffU; 1034 FStar_UInt128_uint128 c5 = carry5; 1035 uint64_t t5 = t15; 1036 FStar_UInt128_uint128 1037 carry6 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z60, c5), (uint32_t)56U); 1038 uint64_t 1039 t16 = 1040 FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z60, c5)) & (uint64_t)0xffffffffffffffU; 1041 FStar_UInt128_uint128 c6 = carry6; 1042 uint64_t t6 = t16; 1043 FStar_UInt128_uint128 1044 carry7 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z70, c6), (uint32_t)56U); 1045 uint64_t 1046 t17 = 1047 FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z70, c6)) & (uint64_t)0xffffffffffffffU; 1048 FStar_UInt128_uint128 c7 = carry7; 1049 uint64_t t7 = t17; 1050 FStar_UInt128_uint128 1051 carry = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z80, c7), (uint32_t)56U); 1052 uint64_t 1053 t = 1054 FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z80, c7)) & (uint64_t)0xffffffffffffffU; 1055 FStar_UInt128_uint128 c8 = carry; 1056 uint64_t t8 = t; 1057 uint64_t t9 = FStar_UInt128_uint128_to_uint64(c8); 1058 uint64_t z0 = t0; 1059 uint64_t z1 = t1; 1060 uint64_t z2 = t2; 1061 uint64_t z3 = t3; 1062 uint64_t z4 = t4; 1063 uint64_t z5 = t5; 1064 uint64_t z6 = t6; 1065 uint64_t z7 = t7; 1066 uint64_t z8 = t8; 1067 uint64_t z9 = t9; 1068 tmp[0U] = z0; 1069 tmp[1U] = z1; 1070 tmp[2U] = z2; 1071 tmp[3U] = z3; 1072 tmp[4U] = z4; 1073 tmp[5U] = z5; 1074 tmp[6U] = z6; 1075 tmp[7U] = z7; 1076 tmp[8U] = z8; 1077 tmp[9U] = z9; 1078 barrett_reduction(out, tmp); 1079 } 1080 1081 static inline void 1082 add_modq(uint64_t *out, uint64_t *x, uint64_t *y) 1083 { 1084 uint64_t x0 = x[0U]; 1085 uint64_t x1 = x[1U]; 1086 uint64_t x2 = x[2U]; 1087 uint64_t x3 = x[3U]; 1088 uint64_t x4 = x[4U]; 1089 uint64_t y0 = y[0U]; 1090 uint64_t y1 = y[1U]; 1091 uint64_t y2 = y[2U]; 1092 uint64_t y3 = y[3U]; 1093 uint64_t y4 = y[4U]; 1094 uint64_t carry0 = (x0 + y0) >> (uint32_t)56U; 1095 uint64_t t0 = (x0 + y0) & (uint64_t)0xffffffffffffffU; 1096 uint64_t t00 = t0; 1097 uint64_t c0 = carry0; 1098 uint64_t carry1 = (x1 + y1 + c0) >> (uint32_t)56U; 1099 uint64_t t1 = (x1 + y1 + c0) & (uint64_t)0xffffffffffffffU; 1100 uint64_t t10 = t1; 1101 uint64_t c1 = carry1; 1102 uint64_t carry2 = (x2 + y2 + c1) >> (uint32_t)56U; 1103 uint64_t t2 = (x2 + y2 + c1) & (uint64_t)0xffffffffffffffU; 1104 uint64_t t20 = t2; 1105 uint64_t c2 = carry2; 1106 uint64_t carry = (x3 + y3 + c2) >> (uint32_t)56U; 1107 uint64_t t3 = (x3 + y3 + c2) & (uint64_t)0xffffffffffffffU; 1108 uint64_t t30 = t3; 1109 uint64_t c3 = carry; 1110 uint64_t t4 = x4 + y4 + c3; 1111 uint64_t m0 = (uint64_t)0x12631a5cf5d3edU; 1112 uint64_t m1 = (uint64_t)0xf9dea2f79cd658U; 1113 uint64_t m2 = (uint64_t)0x000000000014deU; 1114 uint64_t m3 = (uint64_t)0x00000000000000U; 1115 uint64_t m4 = (uint64_t)0x00000010000000U; 1116 uint64_t y01 = m0; 1117 uint64_t y11 = m1; 1118 uint64_t y21 = m2; 1119 uint64_t y31 = m3; 1120 uint64_t y41 = m4; 1121 uint64_t b5 = (t00 - y01) >> (uint32_t)63U; 1122 uint64_t t5 = (b5 << (uint32_t)56U) + t00 - y01; 1123 uint64_t b0 = b5; 1124 uint64_t t01 = t5; 1125 uint64_t b6 = (t10 - (y11 + b0)) >> (uint32_t)63U; 1126 uint64_t t6 = (b6 << (uint32_t)56U) + t10 - (y11 + b0); 1127 uint64_t b1 = b6; 1128 uint64_t t11 = t6; 1129 uint64_t b7 = (t20 - (y21 + b1)) >> (uint32_t)63U; 1130 uint64_t t7 = (b7 << (uint32_t)56U) + t20 - (y21 + b1); 1131 uint64_t b2 = b7; 1132 uint64_t t21 = t7; 1133 uint64_t b8 = (t30 - (y31 + b2)) >> (uint32_t)63U; 1134 uint64_t t8 = (b8 << (uint32_t)56U) + t30 - (y31 + b2); 1135 uint64_t b3 = b8; 1136 uint64_t t31 = t8; 1137 uint64_t b = (t4 - (y41 + b3)) >> (uint32_t)63U; 1138 uint64_t t = (b << (uint32_t)56U) + t4 - (y41 + b3); 1139 uint64_t b4 = b; 1140 uint64_t t41 = t; 1141 uint64_t mask = b4 - (uint64_t)1U; 1142 uint64_t z00 = t00 ^ (mask & (t00 ^ t01)); 1143 uint64_t z10 = t10 ^ (mask & (t10 ^ t11)); 1144 uint64_t z20 = t20 ^ (mask & (t20 ^ t21)); 1145 uint64_t z30 = t30 ^ (mask & (t30 ^ t31)); 1146 uint64_t z40 = t4 ^ (mask & (t4 ^ t41)); 1147 uint64_t z01 = z00; 1148 uint64_t z11 = z10; 1149 uint64_t z21 = z20; 1150 uint64_t z31 = z30; 1151 uint64_t z41 = z40; 1152 uint64_t o0 = z01; 1153 uint64_t o1 = z11; 1154 uint64_t o2 = z21; 1155 uint64_t o3 = z31; 1156 uint64_t o4 = z41; 1157 uint64_t z0 = o0; 1158 uint64_t z1 = o1; 1159 uint64_t z2 = o2; 1160 uint64_t z3 = o3; 1161 uint64_t z4 = o4; 1162 out[0U] = z0; 1163 out[1U] = z1; 1164 out[2U] = z2; 1165 out[3U] = z3; 1166 out[4U] = z4; 1167 } 1168 1169 static inline bool 1170 gte_q(uint64_t *s) 1171 { 1172 uint64_t s0 = s[0U]; 1173 uint64_t s1 = s[1U]; 1174 uint64_t s2 = s[2U]; 1175 uint64_t s3 = s[3U]; 1176 uint64_t s4 = s[4U]; 1177 if (s4 > (uint64_t)0x00000010000000U) { 1178 return true; 1179 } 1180 if (s4 < (uint64_t)0x00000010000000U) { 1181 return false; 1182 } 1183 if (s3 > (uint64_t)0x00000000000000U) { 1184 return true; 1185 } 1186 if (s2 > (uint64_t)0x000000000014deU) { 1187 return true; 1188 } 1189 if (s2 < (uint64_t)0x000000000014deU) { 1190 return false; 1191 } 1192 if (s1 > (uint64_t)0xf9dea2f79cd658U) { 1193 return true; 1194 } 1195 if (s1 < (uint64_t)0xf9dea2f79cd658U) { 1196 return false; 1197 } 1198 if (s0 >= (uint64_t)0x12631a5cf5d3edU) { 1199 return true; 1200 } 1201 return false; 1202 } 1203 1204 static inline bool 1205 eq(uint64_t *a, uint64_t *b) 1206 { 1207 uint64_t a0 = a[0U]; 1208 uint64_t a1 = a[1U]; 1209 uint64_t a2 = a[2U]; 1210 uint64_t a3 = a[3U]; 1211 uint64_t a4 = a[4U]; 1212 uint64_t b0 = b[0U]; 1213 uint64_t b1 = b[1U]; 1214 uint64_t b2 = b[2U]; 1215 uint64_t b3 = b[3U]; 1216 uint64_t b4 = b[4U]; 1217 return a0 == b0 && a1 == b1 && a2 == b2 && a3 == b3 && a4 == b4; 1218 } 1219 1220 bool 1221 Hacl_Impl_Ed25519_PointEqual_point_equal(uint64_t *p, uint64_t *q) 1222 { 1223 uint64_t tmp[20U] = { 0U }; 1224 uint64_t *pxqz = tmp; 1225 uint64_t *qxpz = tmp + (uint32_t)5U; 1226 fmul0(pxqz, p, q + (uint32_t)10U); 1227 reduce(pxqz); 1228 fmul0(qxpz, q, p + (uint32_t)10U); 1229 reduce(qxpz); 1230 bool b = eq(pxqz, qxpz); 1231 if (b) { 1232 uint64_t *pyqz = tmp + (uint32_t)10U; 1233 uint64_t *qypz = tmp + (uint32_t)15U; 1234 fmul0(pyqz, p + (uint32_t)5U, q + (uint32_t)10U); 1235 reduce(pyqz); 1236 fmul0(qypz, q + (uint32_t)5U, p + (uint32_t)10U); 1237 reduce(qypz); 1238 return eq(pyqz, qypz); 1239 } 1240 return false; 1241 } 1242 1243 void 1244 Hacl_Impl_Ed25519_PointNegate_point_negate(uint64_t *p, uint64_t *out) 1245 { 1246 uint64_t zero[5U] = { 0U }; 1247 zero[0U] = (uint64_t)0U; 1248 zero[1U] = (uint64_t)0U; 1249 zero[2U] = (uint64_t)0U; 1250 zero[3U] = (uint64_t)0U; 1251 zero[4U] = (uint64_t)0U; 1252 uint64_t *x = p; 1253 uint64_t *y = p + (uint32_t)5U; 1254 uint64_t *z = p + (uint32_t)10U; 1255 uint64_t *t = p + (uint32_t)15U; 1256 uint64_t *x1 = out; 1257 uint64_t *y1 = out + (uint32_t)5U; 1258 uint64_t *z1 = out + (uint32_t)10U; 1259 uint64_t *t1 = out + (uint32_t)15U; 1260 fdifference(x1, zero, x); 1261 Hacl_Bignum25519_reduce_513(x1); 1262 memcpy(y1, y, (uint32_t)5U * sizeof(uint64_t)); 1263 memcpy(z1, z, (uint32_t)5U * sizeof(uint64_t)); 1264 fdifference(t1, zero, t); 1265 Hacl_Bignum25519_reduce_513(t1); 1266 } 1267 1268 void 1269 Hacl_Impl_Ed25519_Ladder_point_mul(uint64_t *out, uint8_t *scalar, uint64_t *q) 1270 { 1271 uint64_t bscalar[4U] = { 0U }; 1272 KRML_MAYBE_FOR4(i, 1273 (uint32_t)0U, 1274 (uint32_t)4U, 1275 (uint32_t)1U, 1276 uint64_t *os = bscalar; 1277 uint8_t *bj = scalar + i * (uint32_t)8U; 1278 uint64_t u = load64_le(bj); 1279 uint64_t r = u; 1280 uint64_t x = r; 1281 os[i] = x;); 1282 uint64_t table[320U] = { 0U }; 1283 uint64_t tmp[20U] = { 0U }; 1284 uint64_t *t0 = table; 1285 uint64_t *t1 = table + (uint32_t)20U; 1286 Hacl_Impl_Ed25519_PointConstants_make_point_inf(t0); 1287 memcpy(t1, q, (uint32_t)20U * sizeof(uint64_t)); 1288 KRML_MAYBE_FOR7(i, 1289 (uint32_t)0U, 1290 (uint32_t)7U, 1291 (uint32_t)1U, 1292 uint64_t *t11 = table + (i + (uint32_t)1U) * (uint32_t)20U; 1293 Hacl_Impl_Ed25519_PointDouble_point_double(tmp, t11); 1294 memcpy(table + ((uint32_t)2U * i + (uint32_t)2U) * (uint32_t)20U, 1295 tmp, 1296 (uint32_t)20U * sizeof(uint64_t)); 1297 uint64_t *t2 = table + ((uint32_t)2U * i + (uint32_t)2U) * (uint32_t)20U; 1298 Hacl_Impl_Ed25519_PointAdd_point_add(tmp, q, t2); 1299 memcpy(table + ((uint32_t)2U * i + (uint32_t)3U) * (uint32_t)20U, 1300 tmp, 1301 (uint32_t)20U * sizeof(uint64_t));); 1302 Hacl_Impl_Ed25519_PointConstants_make_point_inf(out); 1303 uint64_t tmp0[20U] = { 0U }; 1304 for (uint32_t i0 = (uint32_t)0U; i0 < (uint32_t)64U; i0++) { 1305 KRML_MAYBE_FOR4(i, 1306 (uint32_t)0U, 1307 (uint32_t)4U, 1308 (uint32_t)1U, 1309 Hacl_Impl_Ed25519_PointDouble_point_double(out, out);); 1310 uint32_t k = (uint32_t)256U - (uint32_t)4U * i0 - (uint32_t)4U; 1311 uint64_t bits_l = Hacl_Bignum_Lib_bn_get_bits_u64((uint32_t)4U, bscalar, k, (uint32_t)4U); 1312 memcpy(tmp0, (uint64_t *)table, (uint32_t)20U * sizeof(uint64_t)); 1313 KRML_MAYBE_FOR15( 1314 i1, 1315 (uint32_t)0U, 1316 (uint32_t)15U, 1317 (uint32_t)1U, 1318 uint64_t c = FStar_UInt64_eq_mask(bits_l, (uint64_t)(i1 + (uint32_t)1U)); 1319 const uint64_t *res_j = table + (i1 + (uint32_t)1U) * (uint32_t)20U; 1320 for (uint32_t i = (uint32_t)0U; i < (uint32_t)20U; i++) { 1321 uint64_t *os = tmp0; 1322 uint64_t x = (c & res_j[i]) | (~c & tmp0[i]); 1323 os[i] = x; 1324 }); 1325 Hacl_Impl_Ed25519_PointAdd_point_add(out, out, tmp0); 1326 } 1327 } 1328 1329 static inline void 1330 precomp_get_consttime(const uint64_t *table, uint64_t bits_l, uint64_t *tmp) 1331 { 1332 memcpy(tmp, (uint64_t *)table, (uint32_t)20U * sizeof(uint64_t)); 1333 KRML_MAYBE_FOR15( 1334 i0, 1335 (uint32_t)0U, 1336 (uint32_t)15U, 1337 (uint32_t)1U, 1338 uint64_t c = FStar_UInt64_eq_mask(bits_l, (uint64_t)(i0 + (uint32_t)1U)); 1339 const uint64_t *res_j = table + (i0 + (uint32_t)1U) * (uint32_t)20U; 1340 for (uint32_t i = (uint32_t)0U; i < (uint32_t)20U; i++) { 1341 uint64_t *os = tmp; 1342 uint64_t x = (c & res_j[i]) | (~c & tmp[i]); 1343 os[i] = x; 1344 }); 1345 } 1346 1347 static inline void 1348 point_mul_g(uint64_t *out, uint8_t *scalar) 1349 { 1350 uint64_t bscalar[4U] = { 0U }; 1351 KRML_MAYBE_FOR4(i, 1352 (uint32_t)0U, 1353 (uint32_t)4U, 1354 (uint32_t)1U, 1355 uint64_t *os = bscalar; 1356 uint8_t *bj = scalar + i * (uint32_t)8U; 1357 uint64_t u = load64_le(bj); 1358 uint64_t r = u; 1359 uint64_t x = r; 1360 os[i] = x;); 1361 uint64_t q1[20U] = { 0U }; 1362 uint64_t *gx = q1; 1363 uint64_t *gy = q1 + (uint32_t)5U; 1364 uint64_t *gz = q1 + (uint32_t)10U; 1365 uint64_t *gt = q1 + (uint32_t)15U; 1366 gx[0U] = (uint64_t)0x00062d608f25d51aU; 1367 gx[1U] = (uint64_t)0x000412a4b4f6592aU; 1368 gx[2U] = (uint64_t)0x00075b7171a4b31dU; 1369 gx[3U] = (uint64_t)0x0001ff60527118feU; 1370 gx[4U] = (uint64_t)0x000216936d3cd6e5U; 1371 gy[0U] = (uint64_t)0x0006666666666658U; 1372 gy[1U] = (uint64_t)0x0004ccccccccccccU; 1373 gy[2U] = (uint64_t)0x0001999999999999U; 1374 gy[3U] = (uint64_t)0x0003333333333333U; 1375 gy[4U] = (uint64_t)0x0006666666666666U; 1376 gz[0U] = (uint64_t)1U; 1377 gz[1U] = (uint64_t)0U; 1378 gz[2U] = (uint64_t)0U; 1379 gz[3U] = (uint64_t)0U; 1380 gz[4U] = (uint64_t)0U; 1381 gt[0U] = (uint64_t)0x00068ab3a5b7dda3U; 1382 gt[1U] = (uint64_t)0x00000eea2a5eadbbU; 1383 gt[2U] = (uint64_t)0x0002af8df483c27eU; 1384 gt[3U] = (uint64_t)0x000332b375274732U; 1385 gt[4U] = (uint64_t)0x00067875f0fd78b7U; 1386 uint64_t 1387 q2[20U] = { 1388 (uint64_t)13559344787725U, (uint64_t)2051621493703448U, (uint64_t)1947659315640708U, 1389 (uint64_t)626856790370168U, (uint64_t)1592804284034836U, (uint64_t)1781728767459187U, 1390 (uint64_t)278818420518009U, (uint64_t)2038030359908351U, (uint64_t)910625973862690U, 1391 (uint64_t)471887343142239U, (uint64_t)1298543306606048U, (uint64_t)794147365642417U, 1392 (uint64_t)129968992326749U, (uint64_t)523140861678572U, (uint64_t)1166419653909231U, 1393 (uint64_t)2009637196928390U, (uint64_t)1288020222395193U, (uint64_t)1007046974985829U, 1394 (uint64_t)208981102651386U, (uint64_t)2074009315253380U 1395 }; 1396 uint64_t 1397 q3[20U] = { 1398 (uint64_t)557549315715710U, (uint64_t)196756086293855U, (uint64_t)846062225082495U, 1399 (uint64_t)1865068224838092U, (uint64_t)991112090754908U, (uint64_t)522916421512828U, 1400 (uint64_t)2098523346722375U, (uint64_t)1135633221747012U, (uint64_t)858420432114866U, 1401 (uint64_t)186358544306082U, (uint64_t)1044420411868480U, (uint64_t)2080052304349321U, 1402 (uint64_t)557301814716724U, (uint64_t)1305130257814057U, (uint64_t)2126012765451197U, 1403 (uint64_t)1441004402875101U, (uint64_t)353948968859203U, (uint64_t)470765987164835U, 1404 (uint64_t)1507675957683570U, (uint64_t)1086650358745097U 1405 }; 1406 uint64_t 1407 q4[20U] = { 1408 (uint64_t)1129953239743101U, (uint64_t)1240339163956160U, (uint64_t)61002583352401U, 1409 (uint64_t)2017604552196030U, (uint64_t)1576867829229863U, (uint64_t)1508654942849389U, 1410 (uint64_t)270111619664077U, (uint64_t)1253097517254054U, (uint64_t)721798270973250U, 1411 (uint64_t)161923365415298U, (uint64_t)828530877526011U, (uint64_t)1494851059386763U, 1412 (uint64_t)662034171193976U, (uint64_t)1315349646974670U, (uint64_t)2199229517308806U, 1413 (uint64_t)497078277852673U, (uint64_t)1310507715989956U, (uint64_t)1881315714002105U, 1414 (uint64_t)2214039404983803U, (uint64_t)1331036420272667U 1415 }; 1416 uint64_t *r1 = bscalar; 1417 uint64_t *r2 = bscalar + (uint32_t)1U; 1418 uint64_t *r3 = bscalar + (uint32_t)2U; 1419 uint64_t *r4 = bscalar + (uint32_t)3U; 1420 Hacl_Impl_Ed25519_PointConstants_make_point_inf(out); 1421 uint64_t tmp[20U] = { 0U }; 1422 KRML_MAYBE_FOR16(i, 1423 (uint32_t)0U, 1424 (uint32_t)16U, 1425 (uint32_t)1U, 1426 KRML_MAYBE_FOR4(i0, 1427 (uint32_t)0U, 1428 (uint32_t)4U, 1429 (uint32_t)1U, 1430 Hacl_Impl_Ed25519_PointDouble_point_double(out, out);); 1431 uint32_t k = (uint32_t)64U - (uint32_t)4U * i - (uint32_t)4U; 1432 uint64_t bits_l = Hacl_Bignum_Lib_bn_get_bits_u64((uint32_t)1U, r4, k, (uint32_t)4U); 1433 precomp_get_consttime(Hacl_Ed25519_PrecompTable_precomp_g_pow2_192_table_w4, bits_l, tmp); 1434 Hacl_Impl_Ed25519_PointAdd_point_add(out, out, tmp); 1435 uint32_t k0 = (uint32_t)64U - (uint32_t)4U * i - (uint32_t)4U; 1436 uint64_t bits_l0 = Hacl_Bignum_Lib_bn_get_bits_u64((uint32_t)1U, r3, k0, (uint32_t)4U); 1437 precomp_get_consttime(Hacl_Ed25519_PrecompTable_precomp_g_pow2_128_table_w4, bits_l0, tmp); 1438 Hacl_Impl_Ed25519_PointAdd_point_add(out, out, tmp); 1439 uint32_t k1 = (uint32_t)64U - (uint32_t)4U * i - (uint32_t)4U; 1440 uint64_t bits_l1 = Hacl_Bignum_Lib_bn_get_bits_u64((uint32_t)1U, r2, k1, (uint32_t)4U); 1441 precomp_get_consttime(Hacl_Ed25519_PrecompTable_precomp_g_pow2_64_table_w4, bits_l1, tmp); 1442 Hacl_Impl_Ed25519_PointAdd_point_add(out, out, tmp); 1443 uint32_t k2 = (uint32_t)64U - (uint32_t)4U * i - (uint32_t)4U; 1444 uint64_t bits_l2 = Hacl_Bignum_Lib_bn_get_bits_u64((uint32_t)1U, r1, k2, (uint32_t)4U); 1445 precomp_get_consttime(Hacl_Ed25519_PrecompTable_precomp_basepoint_table_w4, bits_l2, tmp); 1446 Hacl_Impl_Ed25519_PointAdd_point_add(out, out, tmp);); 1447 KRML_HOST_IGNORE(q2); 1448 KRML_HOST_IGNORE(q3); 1449 KRML_HOST_IGNORE(q4); 1450 } 1451 1452 static inline void 1453 point_mul_g_double_vartime(uint64_t *out, uint8_t *scalar1, uint8_t *scalar2, uint64_t *q2) 1454 { 1455 uint64_t tmp[28U] = { 0U }; 1456 uint64_t *g = tmp; 1457 uint64_t *bscalar1 = tmp + (uint32_t)20U; 1458 uint64_t *bscalar2 = tmp + (uint32_t)24U; 1459 uint64_t *gx = g; 1460 uint64_t *gy = g + (uint32_t)5U; 1461 uint64_t *gz = g + (uint32_t)10U; 1462 uint64_t *gt = g + (uint32_t)15U; 1463 gx[0U] = (uint64_t)0x00062d608f25d51aU; 1464 gx[1U] = (uint64_t)0x000412a4b4f6592aU; 1465 gx[2U] = (uint64_t)0x00075b7171a4b31dU; 1466 gx[3U] = (uint64_t)0x0001ff60527118feU; 1467 gx[4U] = (uint64_t)0x000216936d3cd6e5U; 1468 gy[0U] = (uint64_t)0x0006666666666658U; 1469 gy[1U] = (uint64_t)0x0004ccccccccccccU; 1470 gy[2U] = (uint64_t)0x0001999999999999U; 1471 gy[3U] = (uint64_t)0x0003333333333333U; 1472 gy[4U] = (uint64_t)0x0006666666666666U; 1473 gz[0U] = (uint64_t)1U; 1474 gz[1U] = (uint64_t)0U; 1475 gz[2U] = (uint64_t)0U; 1476 gz[3U] = (uint64_t)0U; 1477 gz[4U] = (uint64_t)0U; 1478 gt[0U] = (uint64_t)0x00068ab3a5b7dda3U; 1479 gt[1U] = (uint64_t)0x00000eea2a5eadbbU; 1480 gt[2U] = (uint64_t)0x0002af8df483c27eU; 1481 gt[3U] = (uint64_t)0x000332b375274732U; 1482 gt[4U] = (uint64_t)0x00067875f0fd78b7U; 1483 KRML_MAYBE_FOR4(i, 1484 (uint32_t)0U, 1485 (uint32_t)4U, 1486 (uint32_t)1U, 1487 uint64_t *os = bscalar1; 1488 uint8_t *bj = scalar1 + i * (uint32_t)8U; 1489 uint64_t u = load64_le(bj); 1490 uint64_t r = u; 1491 uint64_t x = r; 1492 os[i] = x;); 1493 KRML_MAYBE_FOR4(i, 1494 (uint32_t)0U, 1495 (uint32_t)4U, 1496 (uint32_t)1U, 1497 uint64_t *os = bscalar2; 1498 uint8_t *bj = scalar2 + i * (uint32_t)8U; 1499 uint64_t u = load64_le(bj); 1500 uint64_t r = u; 1501 uint64_t x = r; 1502 os[i] = x;); 1503 uint64_t table2[640U] = { 0U }; 1504 uint64_t tmp1[20U] = { 0U }; 1505 uint64_t *t0 = table2; 1506 uint64_t *t1 = table2 + (uint32_t)20U; 1507 Hacl_Impl_Ed25519_PointConstants_make_point_inf(t0); 1508 memcpy(t1, q2, (uint32_t)20U * sizeof(uint64_t)); 1509 KRML_MAYBE_FOR15(i, 1510 (uint32_t)0U, 1511 (uint32_t)15U, 1512 (uint32_t)1U, 1513 uint64_t *t11 = table2 + (i + (uint32_t)1U) * (uint32_t)20U; 1514 Hacl_Impl_Ed25519_PointDouble_point_double(tmp1, t11); 1515 memcpy(table2 + ((uint32_t)2U * i + (uint32_t)2U) * (uint32_t)20U, 1516 tmp1, 1517 (uint32_t)20U * sizeof(uint64_t)); 1518 uint64_t *t2 = table2 + ((uint32_t)2U * i + (uint32_t)2U) * (uint32_t)20U; 1519 Hacl_Impl_Ed25519_PointAdd_point_add(tmp1, q2, t2); 1520 memcpy(table2 + ((uint32_t)2U * i + (uint32_t)3U) * (uint32_t)20U, 1521 tmp1, 1522 (uint32_t)20U * sizeof(uint64_t));); 1523 uint64_t tmp10[20U] = { 0U }; 1524 uint32_t i0 = (uint32_t)255U; 1525 uint64_t bits_c = Hacl_Bignum_Lib_bn_get_bits_u64((uint32_t)4U, bscalar1, i0, (uint32_t)5U); 1526 uint32_t bits_l32 = (uint32_t)bits_c; 1527 const uint64_t 1528 *a_bits_l = Hacl_Ed25519_PrecompTable_precomp_basepoint_table_w5 + bits_l32 * (uint32_t)20U; 1529 memcpy(out, (uint64_t *)a_bits_l, (uint32_t)20U * sizeof(uint64_t)); 1530 uint32_t i1 = (uint32_t)255U; 1531 uint64_t bits_c0 = Hacl_Bignum_Lib_bn_get_bits_u64((uint32_t)4U, bscalar2, i1, (uint32_t)5U); 1532 uint32_t bits_l320 = (uint32_t)bits_c0; 1533 const uint64_t *a_bits_l0 = table2 + bits_l320 * (uint32_t)20U; 1534 memcpy(tmp10, (uint64_t *)a_bits_l0, (uint32_t)20U * sizeof(uint64_t)); 1535 Hacl_Impl_Ed25519_PointAdd_point_add(out, out, tmp10); 1536 uint64_t tmp11[20U] = { 0U }; 1537 for (uint32_t i = (uint32_t)0U; i < (uint32_t)51U; i++) { 1538 KRML_MAYBE_FOR5(i2, 1539 (uint32_t)0U, 1540 (uint32_t)5U, 1541 (uint32_t)1U, 1542 Hacl_Impl_Ed25519_PointDouble_point_double(out, out);); 1543 uint32_t k = (uint32_t)255U - (uint32_t)5U * i - (uint32_t)5U; 1544 uint64_t bits_l = Hacl_Bignum_Lib_bn_get_bits_u64((uint32_t)4U, bscalar2, k, (uint32_t)5U); 1545 uint32_t bits_l321 = (uint32_t)bits_l; 1546 const uint64_t *a_bits_l1 = table2 + bits_l321 * (uint32_t)20U; 1547 memcpy(tmp11, (uint64_t *)a_bits_l1, (uint32_t)20U * sizeof(uint64_t)); 1548 Hacl_Impl_Ed25519_PointAdd_point_add(out, out, tmp11); 1549 uint32_t k0 = (uint32_t)255U - (uint32_t)5U * i - (uint32_t)5U; 1550 uint64_t bits_l0 = Hacl_Bignum_Lib_bn_get_bits_u64((uint32_t)4U, bscalar1, k0, (uint32_t)5U); 1551 uint32_t bits_l322 = (uint32_t)bits_l0; 1552 const uint64_t 1553 *a_bits_l2 = Hacl_Ed25519_PrecompTable_precomp_basepoint_table_w5 + bits_l322 * (uint32_t)20U; 1554 memcpy(tmp11, (uint64_t *)a_bits_l2, (uint32_t)20U * sizeof(uint64_t)); 1555 Hacl_Impl_Ed25519_PointAdd_point_add(out, out, tmp11); 1556 } 1557 } 1558 1559 static inline void 1560 point_negate_mul_double_g_vartime( 1561 uint64_t *out, 1562 uint8_t *scalar1, 1563 uint8_t *scalar2, 1564 uint64_t *q2) 1565 { 1566 uint64_t q2_neg[20U] = { 0U }; 1567 Hacl_Impl_Ed25519_PointNegate_point_negate(q2, q2_neg); 1568 point_mul_g_double_vartime(out, scalar1, scalar2, q2_neg); 1569 } 1570 1571 static inline void 1572 store_56(uint8_t *out, uint64_t *b) 1573 { 1574 uint64_t b0 = b[0U]; 1575 uint64_t b1 = b[1U]; 1576 uint64_t b2 = b[2U]; 1577 uint64_t b3 = b[3U]; 1578 uint64_t b4 = b[4U]; 1579 uint32_t b4_ = (uint32_t)b4; 1580 uint8_t *b8 = out; 1581 store64_le(b8, b0); 1582 uint8_t *b80 = out + (uint32_t)7U; 1583 store64_le(b80, b1); 1584 uint8_t *b81 = out + (uint32_t)14U; 1585 store64_le(b81, b2); 1586 uint8_t *b82 = out + (uint32_t)21U; 1587 store64_le(b82, b3); 1588 store32_le(out + (uint32_t)28U, b4_); 1589 } 1590 1591 static inline void 1592 load_64_bytes(uint64_t *out, uint8_t *b) 1593 { 1594 uint8_t *b80 = b; 1595 uint64_t u = load64_le(b80); 1596 uint64_t z = u; 1597 uint64_t b0 = z & (uint64_t)0xffffffffffffffU; 1598 uint8_t *b81 = b + (uint32_t)7U; 1599 uint64_t u0 = load64_le(b81); 1600 uint64_t z0 = u0; 1601 uint64_t b1 = z0 & (uint64_t)0xffffffffffffffU; 1602 uint8_t *b82 = b + (uint32_t)14U; 1603 uint64_t u1 = load64_le(b82); 1604 uint64_t z1 = u1; 1605 uint64_t b2 = z1 & (uint64_t)0xffffffffffffffU; 1606 uint8_t *b83 = b + (uint32_t)21U; 1607 uint64_t u2 = load64_le(b83); 1608 uint64_t z2 = u2; 1609 uint64_t b3 = z2 & (uint64_t)0xffffffffffffffU; 1610 uint8_t *b84 = b + (uint32_t)28U; 1611 uint64_t u3 = load64_le(b84); 1612 uint64_t z3 = u3; 1613 uint64_t b4 = z3 & (uint64_t)0xffffffffffffffU; 1614 uint8_t *b85 = b + (uint32_t)35U; 1615 uint64_t u4 = load64_le(b85); 1616 uint64_t z4 = u4; 1617 uint64_t b5 = z4 & (uint64_t)0xffffffffffffffU; 1618 uint8_t *b86 = b + (uint32_t)42U; 1619 uint64_t u5 = load64_le(b86); 1620 uint64_t z5 = u5; 1621 uint64_t b6 = z5 & (uint64_t)0xffffffffffffffU; 1622 uint8_t *b87 = b + (uint32_t)49U; 1623 uint64_t u6 = load64_le(b87); 1624 uint64_t z6 = u6; 1625 uint64_t b7 = z6 & (uint64_t)0xffffffffffffffU; 1626 uint8_t *b8 = b + (uint32_t)56U; 1627 uint64_t u7 = load64_le(b8); 1628 uint64_t z7 = u7; 1629 uint64_t b88 = z7 & (uint64_t)0xffffffffffffffU; 1630 uint8_t b63 = b[63U]; 1631 uint64_t b9 = (uint64_t)b63; 1632 out[0U] = b0; 1633 out[1U] = b1; 1634 out[2U] = b2; 1635 out[3U] = b3; 1636 out[4U] = b4; 1637 out[5U] = b5; 1638 out[6U] = b6; 1639 out[7U] = b7; 1640 out[8U] = b88; 1641 out[9U] = b9; 1642 } 1643 1644 static inline void 1645 load_32_bytes(uint64_t *out, uint8_t *b) 1646 { 1647 uint8_t *b80 = b; 1648 uint64_t u0 = load64_le(b80); 1649 uint64_t z = u0; 1650 uint64_t b0 = z & (uint64_t)0xffffffffffffffU; 1651 uint8_t *b81 = b + (uint32_t)7U; 1652 uint64_t u1 = load64_le(b81); 1653 uint64_t z0 = u1; 1654 uint64_t b1 = z0 & (uint64_t)0xffffffffffffffU; 1655 uint8_t *b82 = b + (uint32_t)14U; 1656 uint64_t u2 = load64_le(b82); 1657 uint64_t z1 = u2; 1658 uint64_t b2 = z1 & (uint64_t)0xffffffffffffffU; 1659 uint8_t *b8 = b + (uint32_t)21U; 1660 uint64_t u3 = load64_le(b8); 1661 uint64_t z2 = u3; 1662 uint64_t b3 = z2 & (uint64_t)0xffffffffffffffU; 1663 uint32_t u = load32_le(b + (uint32_t)28U); 1664 uint32_t b4 = u; 1665 uint64_t b41 = (uint64_t)b4; 1666 out[0U] = b0; 1667 out[1U] = b1; 1668 out[2U] = b2; 1669 out[3U] = b3; 1670 out[4U] = b41; 1671 } 1672 1673 static inline void 1674 sha512_modq_pre(uint64_t *out, uint8_t *prefix, uint32_t len, uint8_t *input) 1675 { 1676 uint64_t tmp[10U] = { 0U }; 1677 uint8_t hash[64U] = { 0U }; 1678 sha512_pre_msg(hash, prefix, len, input); 1679 load_64_bytes(tmp, hash); 1680 barrett_reduction(out, tmp); 1681 } 1682 1683 static inline void 1684 sha512_modq_pre_pre2( 1685 uint64_t *out, 1686 uint8_t *prefix, 1687 uint8_t *prefix2, 1688 uint32_t len, 1689 uint8_t *input) 1690 { 1691 uint64_t tmp[10U] = { 0U }; 1692 uint8_t hash[64U] = { 0U }; 1693 sha512_pre_pre2_msg(hash, prefix, prefix2, len, input); 1694 load_64_bytes(tmp, hash); 1695 barrett_reduction(out, tmp); 1696 } 1697 1698 static inline void 1699 point_mul_g_compress(uint8_t *out, uint8_t *s) 1700 { 1701 uint64_t tmp[20U] = { 0U }; 1702 point_mul_g(tmp, s); 1703 Hacl_Impl_Ed25519_PointCompress_point_compress(out, tmp); 1704 } 1705 1706 static inline void 1707 secret_expand(uint8_t *expanded, uint8_t *secret) 1708 { 1709 Hacl_Streaming_SHA2_hash_512(secret, (uint32_t)32U, expanded); 1710 uint8_t *h_low = expanded; 1711 uint8_t h_low0 = h_low[0U]; 1712 uint8_t h_low31 = h_low[31U]; 1713 h_low[0U] = h_low0 & (uint8_t)0xf8U; 1714 h_low[31U] = (h_low31 & (uint8_t)127U) | (uint8_t)64U; 1715 } 1716 1717 /******************************************************************************** 1718 Verified C library for EdDSA signing and verification on the edwards25519 curve. 1719 ********************************************************************************/ 1720 1721 /** 1722 Compute the public key from the private key. 1723 1724 The outparam `public_key` points to 32 bytes of valid memory, i.e., uint8_t[32]. 1725 The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32]. 1726 */ 1727 void 1728 Hacl_Ed25519_secret_to_public(uint8_t *public_key, uint8_t *private_key) 1729 { 1730 uint8_t expanded_secret[64U] = { 0U }; 1731 secret_expand(expanded_secret, private_key); 1732 uint8_t *a = expanded_secret; 1733 point_mul_g_compress(public_key, a); 1734 } 1735 1736 /** 1737 Compute the expanded keys for an Ed25519 signature. 1738 1739 The outparam `expanded_keys` points to 96 bytes of valid memory, i.e., uint8_t[96]. 1740 The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32]. 1741 1742 If one needs to sign several messages under the same private key, it is more efficient 1743 to call `expand_keys` only once and `sign_expanded` multiple times, for each message. 1744 */ 1745 void 1746 Hacl_Ed25519_expand_keys(uint8_t *expanded_keys, uint8_t *private_key) 1747 { 1748 uint8_t *public_key = expanded_keys; 1749 uint8_t *s_prefix = expanded_keys + (uint32_t)32U; 1750 uint8_t *s = expanded_keys + (uint32_t)32U; 1751 secret_expand(s_prefix, private_key); 1752 point_mul_g_compress(public_key, s); 1753 } 1754 1755 /** 1756 Create an Ed25519 signature with the (precomputed) expanded keys. 1757 1758 The outparam `signature` points to 64 bytes of valid memory, i.e., uint8_t[64]. 1759 The argument `expanded_keys` points to 96 bytes of valid memory, i.e., uint8_t[96]. 1760 The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len]. 1761 1762 The argument `expanded_keys` is obtained through `expand_keys`. 1763 1764 If one needs to sign several messages under the same private key, it is more efficient 1765 to call `expand_keys` only once and `sign_expanded` multiple times, for each message. 1766 */ 1767 void 1768 Hacl_Ed25519_sign_expanded( 1769 uint8_t *signature, 1770 uint8_t *expanded_keys, 1771 uint32_t msg_len, 1772 uint8_t *msg) 1773 { 1774 uint8_t *rs = signature; 1775 uint8_t *ss = signature + (uint32_t)32U; 1776 uint64_t rq[5U] = { 0U }; 1777 uint64_t hq[5U] = { 0U }; 1778 uint8_t rb[32U] = { 0U }; 1779 uint8_t *public_key = expanded_keys; 1780 uint8_t *s = expanded_keys + (uint32_t)32U; 1781 uint8_t *prefix = expanded_keys + (uint32_t)64U; 1782 sha512_modq_pre(rq, prefix, msg_len, msg); 1783 store_56(rb, rq); 1784 point_mul_g_compress(rs, rb); 1785 sha512_modq_pre_pre2(hq, rs, public_key, msg_len, msg); 1786 uint64_t aq[5U] = { 0U }; 1787 load_32_bytes(aq, s); 1788 mul_modq(aq, hq, aq); 1789 add_modq(aq, rq, aq); 1790 store_56(ss, aq); 1791 } 1792 1793 /** 1794 Create an Ed25519 signature. 1795 1796 The outparam `signature` points to 64 bytes of valid memory, i.e., uint8_t[64]. 1797 The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32]. 1798 The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len]. 1799 1800 The function first calls `expand_keys` and then invokes `sign_expanded`. 1801 1802 If one needs to sign several messages under the same private key, it is more efficient 1803 to call `expand_keys` only once and `sign_expanded` multiple times, for each message. 1804 */ 1805 void 1806 Hacl_Ed25519_sign(uint8_t *signature, uint8_t *private_key, uint32_t msg_len, uint8_t *msg) 1807 { 1808 uint8_t expanded_keys[96U] = { 0U }; 1809 Hacl_Ed25519_expand_keys(expanded_keys, private_key); 1810 Hacl_Ed25519_sign_expanded(signature, expanded_keys, msg_len, msg); 1811 } 1812 1813 /** 1814 Verify an Ed25519 signature. 1815 1816 The function returns `true` if the signature is valid and `false` otherwise. 1817 1818 The argument `public_key` points to 32 bytes of valid memory, i.e., uint8_t[32]. 1819 The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len]. 1820 The argument `signature` points to 64 bytes of valid memory, i.e., uint8_t[64]. 1821 */ 1822 bool 1823 Hacl_Ed25519_verify(uint8_t *public_key, uint32_t msg_len, uint8_t *msg, uint8_t *signature) 1824 { 1825 uint64_t a_[20U] = { 0U }; 1826 bool b = Hacl_Impl_Ed25519_PointDecompress_point_decompress(a_, public_key); 1827 if (b) { 1828 uint64_t r_[20U] = { 0U }; 1829 uint8_t *rs = signature; 1830 bool b_ = Hacl_Impl_Ed25519_PointDecompress_point_decompress(r_, rs); 1831 if (b_) { 1832 uint8_t hb[32U] = { 0U }; 1833 uint8_t *rs1 = signature; 1834 uint8_t *sb = signature + (uint32_t)32U; 1835 uint64_t tmp[5U] = { 0U }; 1836 load_32_bytes(tmp, sb); 1837 bool b1 = gte_q(tmp); 1838 bool b10 = b1; 1839 if (b10) { 1840 return false; 1841 } 1842 uint64_t tmp0[5U] = { 0U }; 1843 sha512_modq_pre_pre2(tmp0, rs1, public_key, msg_len, msg); 1844 store_56(hb, tmp0); 1845 uint64_t exp_d[20U] = { 0U }; 1846 point_negate_mul_double_g_vartime(exp_d, sb, hb, a_); 1847 bool b2 = Hacl_Impl_Ed25519_PointEqual_point_equal(exp_d, r_); 1848 return b2; 1849 } 1850 return false; 1851 } 1852 return false; 1853 }