/* MIT License * * Copyright (c) 2016-2017 INRIA and Microsoft Corporation * * Permission is hereby granted, free of charge, to any person obtaining a copy * of this software and associated documentation files (the "Software"), to deal * in the Software without restriction, including without limitation the rights * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell * copies of the Software, and to permit persons to whom the Software is * furnished to do so, subject to the following conditions: * * The above copyright notice and this permission notice shall be included in all * copies or substantial portions of the Software. * * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE * SOFTWARE. */ #include "Hacl_Ed25519.h" static void Hacl_Bignum_Modulo_carry_top(uint64_t *b) { uint64_t b4 = b[4U]; uint64_t b0 = b[0U]; uint64_t b4_ = b4 & (uint64_t)0x7ffffffffffffU; uint64_t b0_ = b0 + (uint64_t)19U * (b4 >> (uint32_t)51U); b[4U] = b4_; b[0U] = b0_; } inline static void Hacl_Bignum_Fproduct_copy_from_wide_(uint64_t *output, FStar_UInt128_t *input) { { FStar_UInt128_t xi = input[0U]; output[0U] = FStar_UInt128_uint128_to_uint64(xi); } { FStar_UInt128_t xi = input[1U]; output[1U] = FStar_UInt128_uint128_to_uint64(xi); } { FStar_UInt128_t xi = input[2U]; output[2U] = FStar_UInt128_uint128_to_uint64(xi); } { FStar_UInt128_t xi = input[3U]; output[3U] = FStar_UInt128_uint128_to_uint64(xi); } { FStar_UInt128_t xi = input[4U]; output[4U] = FStar_UInt128_uint128_to_uint64(xi); } } inline static void Hacl_Bignum_Fproduct_sum_scalar_multiplication_( FStar_UInt128_t *output, uint64_t *input, uint64_t s ) { { FStar_UInt128_t xi = output[0U]; uint64_t yi = input[0U]; output[0U] = FStar_UInt128_add_mod(xi, FStar_UInt128_mul_wide(yi, s)); } { FStar_UInt128_t xi = output[1U]; uint64_t yi = input[1U]; output[1U] = FStar_UInt128_add_mod(xi, FStar_UInt128_mul_wide(yi, s)); } { FStar_UInt128_t xi = output[2U]; uint64_t yi = input[2U]; output[2U] = FStar_UInt128_add_mod(xi, FStar_UInt128_mul_wide(yi, s)); } { FStar_UInt128_t xi = output[3U]; uint64_t yi = input[3U]; output[3U] = FStar_UInt128_add_mod(xi, FStar_UInt128_mul_wide(yi, s)); } { FStar_UInt128_t xi = output[4U]; uint64_t yi = input[4U]; output[4U] = FStar_UInt128_add_mod(xi, FStar_UInt128_mul_wide(yi, s)); } } inline static void Hacl_Bignum_Fproduct_carry_wide_(FStar_UInt128_t *tmp) { { uint32_t ctr = (uint32_t)0U; FStar_UInt128_t tctr = tmp[ctr]; FStar_UInt128_t tctrp1 = tmp[ctr + (uint32_t)1U]; uint64_t r0 = FStar_UInt128_uint128_to_uint64(tctr) & (uint64_t)0x7ffffffffffffU; FStar_UInt128_t c = FStar_UInt128_shift_right(tctr, (uint32_t)51U); tmp[ctr] = FStar_UInt128_uint64_to_uint128(r0); tmp[ctr + (uint32_t)1U] = FStar_UInt128_add(tctrp1, c); } { uint32_t ctr = (uint32_t)1U; FStar_UInt128_t tctr = tmp[ctr]; FStar_UInt128_t tctrp1 = tmp[ctr + (uint32_t)1U]; uint64_t r0 = FStar_UInt128_uint128_to_uint64(tctr) & (uint64_t)0x7ffffffffffffU; FStar_UInt128_t c = FStar_UInt128_shift_right(tctr, (uint32_t)51U); tmp[ctr] = FStar_UInt128_uint64_to_uint128(r0); tmp[ctr + (uint32_t)1U] = FStar_UInt128_add(tctrp1, c); } { uint32_t ctr = (uint32_t)2U; FStar_UInt128_t tctr = tmp[ctr]; FStar_UInt128_t tctrp1 = tmp[ctr + (uint32_t)1U]; uint64_t r0 = FStar_UInt128_uint128_to_uint64(tctr) & (uint64_t)0x7ffffffffffffU; FStar_UInt128_t c = FStar_UInt128_shift_right(tctr, (uint32_t)51U); tmp[ctr] = FStar_UInt128_uint64_to_uint128(r0); tmp[ctr + (uint32_t)1U] = FStar_UInt128_add(tctrp1, c); } { uint32_t ctr = (uint32_t)3U; FStar_UInt128_t tctr = tmp[ctr]; FStar_UInt128_t tctrp1 = tmp[ctr + (uint32_t)1U]; uint64_t r0 = FStar_UInt128_uint128_to_uint64(tctr) & (uint64_t)0x7ffffffffffffU; FStar_UInt128_t c = FStar_UInt128_shift_right(tctr, (uint32_t)51U); tmp[ctr] = FStar_UInt128_uint64_to_uint128(r0); tmp[ctr + (uint32_t)1U] = FStar_UInt128_add(tctrp1, c); } } inline static void Hacl_Bignum_Fmul_shift_reduce(uint64_t *output) { uint64_t tmp = output[4U]; { uint32_t ctr = (uint32_t)5U - (uint32_t)0U - (uint32_t)1U; uint64_t z = output[ctr - (uint32_t)1U]; output[ctr] = z; } { uint32_t ctr = (uint32_t)5U - (uint32_t)1U - (uint32_t)1U; uint64_t z = output[ctr - (uint32_t)1U]; output[ctr] = z; } { uint32_t ctr = (uint32_t)5U - (uint32_t)2U - (uint32_t)1U; uint64_t z = output[ctr - (uint32_t)1U]; output[ctr] = z; } { uint32_t ctr = (uint32_t)5U - (uint32_t)3U - (uint32_t)1U; uint64_t z = output[ctr - (uint32_t)1U]; output[ctr] = z; } output[0U] = tmp; uint64_t b0 = output[0U]; output[0U] = (uint64_t)19U * b0; } static void Hacl_Bignum_Fmul_mul_shift_reduce_(FStar_UInt128_t *output, uint64_t *input, uint64_t *input21) { { uint64_t input2i = input21[0U]; Hacl_Bignum_Fproduct_sum_scalar_multiplication_(output, input, input2i); Hacl_Bignum_Fmul_shift_reduce(input); } { uint64_t input2i = input21[1U]; Hacl_Bignum_Fproduct_sum_scalar_multiplication_(output, input, input2i); Hacl_Bignum_Fmul_shift_reduce(input); } { uint64_t input2i = input21[2U]; Hacl_Bignum_Fproduct_sum_scalar_multiplication_(output, input, input2i); Hacl_Bignum_Fmul_shift_reduce(input); } { uint64_t input2i = input21[3U]; Hacl_Bignum_Fproduct_sum_scalar_multiplication_(output, input, input2i); Hacl_Bignum_Fmul_shift_reduce(input); } uint32_t i = (uint32_t)4U; uint64_t input2i = input21[i]; Hacl_Bignum_Fproduct_sum_scalar_multiplication_(output, input, input2i); } inline static void Hacl_Bignum_Fmul_fmul(uint64_t *output, uint64_t *input, uint64_t *input21) { uint64_t tmp[5U] = { 0U }; memcpy(tmp, input, (uint32_t)5U * sizeof input[0U]); KRML_CHECK_SIZE(FStar_UInt128_uint64_to_uint128((uint64_t)0U), (uint32_t)5U); FStar_UInt128_t t[5U]; for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i) t[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U); Hacl_Bignum_Fmul_mul_shift_reduce_(t, tmp, input21); Hacl_Bignum_Fproduct_carry_wide_(t); FStar_UInt128_t b4 = t[4U]; FStar_UInt128_t b0 = t[0U]; FStar_UInt128_t b4_ = FStar_UInt128_logand(b4, FStar_UInt128_uint64_to_uint128((uint64_t)0x7ffffffffffffU)); FStar_UInt128_t b0_ = FStar_UInt128_add(b0, FStar_UInt128_mul_wide((uint64_t)19U, FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(b4, (uint32_t)51U)))); t[4U] = b4_; t[0U] = b0_; Hacl_Bignum_Fproduct_copy_from_wide_(output, t); uint64_t i0 = output[0U]; uint64_t i1 = output[1U]; uint64_t i0_ = i0 & (uint64_t)0x7ffffffffffffU; uint64_t i1_ = i1 + (i0 >> (uint32_t)51U); output[0U] = i0_; output[1U] = i1_; } inline static void Hacl_Bignum_Fsquare_fsquare__(FStar_UInt128_t *tmp, uint64_t *output) { uint64_t r0 = output[0U]; uint64_t r1 = output[1U]; uint64_t r2 = output[2U]; uint64_t r3 = output[3U]; uint64_t r4 = output[4U]; uint64_t d0 = r0 * (uint64_t)2U; uint64_t d1 = r1 * (uint64_t)2U; uint64_t d2 = r2 * (uint64_t)2U * (uint64_t)19U; uint64_t d419 = r4 * (uint64_t)19U; uint64_t d4 = d419 * (uint64_t)2U; FStar_UInt128_t s0 = FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(r0, r0), FStar_UInt128_mul_wide(d4, r1)), FStar_UInt128_mul_wide(d2, r3)); FStar_UInt128_t s1 = FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, r1), FStar_UInt128_mul_wide(d4, r2)), FStar_UInt128_mul_wide(r3 * (uint64_t)19U, r3)); FStar_UInt128_t s2 = FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, r2), FStar_UInt128_mul_wide(r1, r1)), FStar_UInt128_mul_wide(d4, r3)); FStar_UInt128_t s3 = FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, r3), FStar_UInt128_mul_wide(d1, r2)), FStar_UInt128_mul_wide(r4, d419)); FStar_UInt128_t s4 = FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, r4), FStar_UInt128_mul_wide(d1, r3)), FStar_UInt128_mul_wide(r2, r2)); tmp[0U] = s0; tmp[1U] = s1; tmp[2U] = s2; tmp[3U] = s3; tmp[4U] = s4; } inline static void Hacl_Bignum_Fsquare_fsquare_(FStar_UInt128_t *tmp, uint64_t *output) { Hacl_Bignum_Fsquare_fsquare__(tmp, output); Hacl_Bignum_Fproduct_carry_wide_(tmp); FStar_UInt128_t b4 = tmp[4U]; FStar_UInt128_t b0 = tmp[0U]; FStar_UInt128_t b4_ = FStar_UInt128_logand(b4, FStar_UInt128_uint64_to_uint128((uint64_t)0x7ffffffffffffU)); FStar_UInt128_t b0_ = FStar_UInt128_add(b0, FStar_UInt128_mul_wide((uint64_t)19U, FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(b4, (uint32_t)51U)))); tmp[4U] = b4_; tmp[0U] = b0_; Hacl_Bignum_Fproduct_copy_from_wide_(output, tmp); uint64_t i0 = output[0U]; uint64_t i1 = output[1U]; uint64_t i0_ = i0 & (uint64_t)0x7ffffffffffffU; uint64_t i1_ = i1 + (i0 >> (uint32_t)51U); output[0U] = i0_; output[1U] = i1_; } static void Hacl_Bignum_Fsquare_fsquare_times_(uint64_t *input, FStar_UInt128_t *tmp, uint32_t count1) { Hacl_Bignum_Fsquare_fsquare_(tmp, input); for (uint32_t i = (uint32_t)1U; i < count1; i = i + (uint32_t)1U) Hacl_Bignum_Fsquare_fsquare_(tmp, input); } inline static void Hacl_Bignum_Fsquare_fsquare_times(uint64_t *output, uint64_t *input, uint32_t count1) { KRML_CHECK_SIZE(FStar_UInt128_uint64_to_uint128((uint64_t)0U), (uint32_t)5U); FStar_UInt128_t t[5U]; for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i) t[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U); memcpy(output, input, (uint32_t)5U * sizeof input[0U]); Hacl_Bignum_Fsquare_fsquare_times_(output, t, count1); } inline static void Hacl_Bignum_Fsquare_fsquare_times_inplace(uint64_t *output, uint32_t count1) { KRML_CHECK_SIZE(FStar_UInt128_uint64_to_uint128((uint64_t)0U), (uint32_t)5U); FStar_UInt128_t t[5U]; for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i) t[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U); Hacl_Bignum_Fsquare_fsquare_times_(output, t, count1); } inline static void Hacl_Bignum_Crecip_crecip(uint64_t *out, uint64_t *z) { uint64_t buf[20U] = { 0U }; uint64_t *a = buf; uint64_t *t00 = buf + (uint32_t)5U; uint64_t *b0 = buf + (uint32_t)10U; Hacl_Bignum_Fsquare_fsquare_times(a, z, (uint32_t)1U); Hacl_Bignum_Fsquare_fsquare_times(t00, a, (uint32_t)2U); Hacl_Bignum_Fmul_fmul(b0, t00, z); Hacl_Bignum_Fmul_fmul(a, b0, a); Hacl_Bignum_Fsquare_fsquare_times(t00, a, (uint32_t)1U); Hacl_Bignum_Fmul_fmul(b0, t00, b0); Hacl_Bignum_Fsquare_fsquare_times(t00, b0, (uint32_t)5U); uint64_t *t01 = buf + (uint32_t)5U; uint64_t *b1 = buf + (uint32_t)10U; uint64_t *c0 = buf + (uint32_t)15U; Hacl_Bignum_Fmul_fmul(b1, t01, b1); Hacl_Bignum_Fsquare_fsquare_times(t01, b1, (uint32_t)10U); Hacl_Bignum_Fmul_fmul(c0, t01, b1); Hacl_Bignum_Fsquare_fsquare_times(t01, c0, (uint32_t)20U); Hacl_Bignum_Fmul_fmul(t01, t01, c0); Hacl_Bignum_Fsquare_fsquare_times_inplace(t01, (uint32_t)10U); Hacl_Bignum_Fmul_fmul(b1, t01, b1); Hacl_Bignum_Fsquare_fsquare_times(t01, b1, (uint32_t)50U); uint64_t *a0 = buf; uint64_t *t0 = buf + (uint32_t)5U; uint64_t *b = buf + (uint32_t)10U; uint64_t *c = buf + (uint32_t)15U; Hacl_Bignum_Fmul_fmul(c, t0, b); Hacl_Bignum_Fsquare_fsquare_times(t0, c, (uint32_t)100U); Hacl_Bignum_Fmul_fmul(t0, t0, c); Hacl_Bignum_Fsquare_fsquare_times_inplace(t0, (uint32_t)50U); Hacl_Bignum_Fmul_fmul(t0, t0, b); Hacl_Bignum_Fsquare_fsquare_times_inplace(t0, (uint32_t)5U); Hacl_Bignum_Fmul_fmul(out, t0, a0); } inline static void Hacl_Bignum_Crecip_crecip_(uint64_t *out, uint64_t *z) { uint64_t buf[20U] = { 0U }; uint64_t *a = buf; uint64_t *t00 = buf + (uint32_t)5U; uint64_t *b0 = buf + (uint32_t)10U; Hacl_Bignum_Fsquare_fsquare_times(a, z, (uint32_t)1U); Hacl_Bignum_Fsquare_fsquare_times(t00, a, (uint32_t)2U); Hacl_Bignum_Fmul_fmul(b0, t00, z); Hacl_Bignum_Fmul_fmul(a, b0, a); Hacl_Bignum_Fsquare_fsquare_times(t00, a, (uint32_t)1U); Hacl_Bignum_Fmul_fmul(b0, t00, b0); Hacl_Bignum_Fsquare_fsquare_times(t00, b0, (uint32_t)5U); uint64_t *t01 = buf + (uint32_t)5U; uint64_t *b1 = buf + (uint32_t)10U; uint64_t *c0 = buf + (uint32_t)15U; Hacl_Bignum_Fmul_fmul(b1, t01, b1); Hacl_Bignum_Fsquare_fsquare_times(t01, b1, (uint32_t)10U); Hacl_Bignum_Fmul_fmul(c0, t01, b1); Hacl_Bignum_Fsquare_fsquare_times(t01, c0, (uint32_t)20U); Hacl_Bignum_Fmul_fmul(t01, t01, c0); Hacl_Bignum_Fsquare_fsquare_times_inplace(t01, (uint32_t)10U); Hacl_Bignum_Fmul_fmul(b1, t01, b1); Hacl_Bignum_Fsquare_fsquare_times(t01, b1, (uint32_t)50U); uint64_t *a0 = buf; Hacl_Bignum_Fsquare_fsquare_times(a0, z, (uint32_t)1U); uint64_t *a1 = buf; uint64_t *t0 = buf + (uint32_t)5U; uint64_t *b = buf + (uint32_t)10U; uint64_t *c = buf + (uint32_t)15U; Hacl_Bignum_Fmul_fmul(c, t0, b); Hacl_Bignum_Fsquare_fsquare_times(t0, c, (uint32_t)100U); Hacl_Bignum_Fmul_fmul(t0, t0, c); Hacl_Bignum_Fsquare_fsquare_times_inplace(t0, (uint32_t)50U); Hacl_Bignum_Fmul_fmul(t0, t0, b); Hacl_Bignum_Fsquare_fsquare_times_inplace(t0, (uint32_t)2U); Hacl_Bignum_Fmul_fmul(out, t0, a1); } inline static void Hacl_Bignum_fsum(uint64_t *a, uint64_t *b) { { uint64_t xi = a[0U]; uint64_t yi = b[0U]; a[0U] = xi + yi; } { uint64_t xi = a[1U]; uint64_t yi = b[1U]; a[1U] = xi + yi; } { uint64_t xi = a[2U]; uint64_t yi = b[2U]; a[2U] = xi + yi; } { uint64_t xi = a[3U]; uint64_t yi = b[3U]; a[3U] = xi + yi; } { uint64_t xi = a[4U]; uint64_t yi = b[4U]; a[4U] = xi + yi; } } inline static void Hacl_Bignum_fdifference(uint64_t *a, uint64_t *b) { uint64_t tmp[5U] = { 0U }; memcpy(tmp, b, (uint32_t)5U * sizeof b[0U]); uint64_t b0 = tmp[0U]; uint64_t b1 = tmp[1U]; uint64_t b2 = tmp[2U]; uint64_t b3 = tmp[3U]; uint64_t b4 = tmp[4U]; tmp[0U] = b0 + (uint64_t)0x3fffffffffff68U; tmp[1U] = b1 + (uint64_t)0x3ffffffffffff8U; tmp[2U] = b2 + (uint64_t)0x3ffffffffffff8U; tmp[3U] = b3 + (uint64_t)0x3ffffffffffff8U; tmp[4U] = b4 + (uint64_t)0x3ffffffffffff8U; { uint64_t xi = a[0U]; uint64_t yi = tmp[0U]; a[0U] = yi - xi; } { uint64_t xi = a[1U]; uint64_t yi = tmp[1U]; a[1U] = yi - xi; } { uint64_t xi = a[2U]; uint64_t yi = tmp[2U]; a[2U] = yi - xi; } { uint64_t xi = a[3U]; uint64_t yi = tmp[3U]; a[3U] = yi - xi; } { uint64_t xi = a[4U]; uint64_t yi = tmp[4U]; a[4U] = yi - xi; } } inline static void Hacl_Bignum_fmul(uint64_t *output, uint64_t *a, uint64_t *b) { Hacl_Bignum_Fmul_fmul(output, a, b); } static void Hacl_EC_Format_fexpand(uint64_t *output, uint8_t *input) { uint64_t i0 = load64_le(input); uint8_t *x00 = input + (uint32_t)6U; uint64_t i1 = load64_le(x00); uint8_t *x01 = input + (uint32_t)12U; uint64_t i2 = load64_le(x01); uint8_t *x02 = input + (uint32_t)19U; uint64_t i3 = load64_le(x02); uint8_t *x0 = input + (uint32_t)24U; uint64_t i4 = load64_le(x0); uint64_t output0 = i0 & (uint64_t)0x7ffffffffffffU; uint64_t output1 = i1 >> (uint32_t)3U & (uint64_t)0x7ffffffffffffU; uint64_t output2 = i2 >> (uint32_t)6U & (uint64_t)0x7ffffffffffffU; uint64_t output3 = i3 >> (uint32_t)1U & (uint64_t)0x7ffffffffffffU; uint64_t output4 = i4 >> (uint32_t)12U & (uint64_t)0x7ffffffffffffU; output[0U] = output0; output[1U] = output1; output[2U] = output2; output[3U] = output3; output[4U] = output4; } static void Hacl_EC_Format_fcontract_first_carry_pass(uint64_t *input) { uint64_t t0 = input[0U]; uint64_t t1 = input[1U]; uint64_t t2 = input[2U]; uint64_t t3 = input[3U]; uint64_t t4 = input[4U]; uint64_t t1_ = t1 + (t0 >> (uint32_t)51U); uint64_t t0_ = t0 & (uint64_t)0x7ffffffffffffU; uint64_t t2_ = t2 + (t1_ >> (uint32_t)51U); uint64_t t1__ = t1_ & (uint64_t)0x7ffffffffffffU; uint64_t t3_ = t3 + (t2_ >> (uint32_t)51U); uint64_t t2__ = t2_ & (uint64_t)0x7ffffffffffffU; uint64_t t4_ = t4 + (t3_ >> (uint32_t)51U); uint64_t t3__ = t3_ & (uint64_t)0x7ffffffffffffU; input[0U] = t0_; input[1U] = t1__; input[2U] = t2__; input[3U] = t3__; input[4U] = t4_; } static void Hacl_EC_Format_fcontract_first_carry_full(uint64_t *input) { Hacl_EC_Format_fcontract_first_carry_pass(input); Hacl_Bignum_Modulo_carry_top(input); } static void Hacl_EC_Format_fcontract_second_carry_pass(uint64_t *input) { uint64_t t0 = input[0U]; uint64_t t1 = input[1U]; uint64_t t2 = input[2U]; uint64_t t3 = input[3U]; uint64_t t4 = input[4U]; uint64_t t1_ = t1 + (t0 >> (uint32_t)51U); uint64_t t0_ = t0 & (uint64_t)0x7ffffffffffffU; uint64_t t2_ = t2 + (t1_ >> (uint32_t)51U); uint64_t t1__ = t1_ & (uint64_t)0x7ffffffffffffU; uint64_t t3_ = t3 + (t2_ >> (uint32_t)51U); uint64_t t2__ = t2_ & (uint64_t)0x7ffffffffffffU; uint64_t t4_ = t4 + (t3_ >> (uint32_t)51U); uint64_t t3__ = t3_ & (uint64_t)0x7ffffffffffffU; input[0U] = t0_; input[1U] = t1__; input[2U] = t2__; input[3U] = t3__; input[4U] = t4_; } static void Hacl_EC_Format_fcontract_second_carry_full(uint64_t *input) { Hacl_EC_Format_fcontract_second_carry_pass(input); Hacl_Bignum_Modulo_carry_top(input); uint64_t i0 = input[0U]; uint64_t i1 = input[1U]; uint64_t i0_ = i0 & (uint64_t)0x7ffffffffffffU; uint64_t i1_ = i1 + (i0 >> (uint32_t)51U); input[0U] = i0_; input[1U] = i1_; } static void Hacl_EC_Format_fcontract_trim(uint64_t *input) { uint64_t a0 = input[0U]; uint64_t a1 = input[1U]; uint64_t a2 = input[2U]; uint64_t a3 = input[3U]; uint64_t a4 = input[4U]; uint64_t mask0 = FStar_UInt64_gte_mask(a0, (uint64_t)0x7ffffffffffedU); uint64_t mask1 = FStar_UInt64_eq_mask(a1, (uint64_t)0x7ffffffffffffU); uint64_t mask2 = FStar_UInt64_eq_mask(a2, (uint64_t)0x7ffffffffffffU); uint64_t mask3 = FStar_UInt64_eq_mask(a3, (uint64_t)0x7ffffffffffffU); uint64_t mask4 = FStar_UInt64_eq_mask(a4, (uint64_t)0x7ffffffffffffU); uint64_t mask = (((mask0 & mask1) & mask2) & mask3) & mask4; uint64_t a0_ = a0 - ((uint64_t)0x7ffffffffffedU & mask); uint64_t a1_ = a1 - ((uint64_t)0x7ffffffffffffU & mask); uint64_t a2_ = a2 - ((uint64_t)0x7ffffffffffffU & mask); uint64_t a3_ = a3 - ((uint64_t)0x7ffffffffffffU & mask); uint64_t a4_ = a4 - ((uint64_t)0x7ffffffffffffU & mask); input[0U] = a0_; input[1U] = a1_; input[2U] = a2_; input[3U] = a3_; input[4U] = a4_; } static void Hacl_EC_Format_reduce(uint64_t *out) { Hacl_EC_Format_fcontract_first_carry_full(out); Hacl_EC_Format_fcontract_second_carry_full(out); Hacl_EC_Format_fcontract_trim(out); } static void Hacl_Lib_Create64_make_h64_5( uint64_t *b, uint64_t s0, uint64_t s1, uint64_t s2, uint64_t s3, uint64_t s4 ) { b[0U] = s0; b[1U] = s1; b[2U] = s2; b[3U] = s3; b[4U] = s4; } static void Hacl_Lib_Create64_make_h64_10( uint64_t *b, uint64_t s0, uint64_t s1, uint64_t s2, uint64_t s3, uint64_t s4, uint64_t s5, uint64_t s6, uint64_t s7, uint64_t s8, uint64_t s9 ) { b[0U] = s0; b[1U] = s1; b[2U] = s2; b[3U] = s3; b[4U] = s4; b[5U] = s5; b[6U] = s6; b[7U] = s7; b[8U] = s8; b[9U] = s9; } static void Hacl_Bignum25519_fsum(uint64_t *a, uint64_t *b) { Hacl_Bignum_fsum(a, b); } static void Hacl_Bignum25519_fdifference(uint64_t *a, uint64_t *b) { Hacl_Bignum_fdifference(a, b); } static void Hacl_Bignum25519_reduce_513(uint64_t *a) { uint64_t t0 = a[0U]; uint64_t t1 = a[1U]; uint64_t t2 = a[2U]; uint64_t t3 = a[3U]; uint64_t t4 = a[4U]; uint64_t t1_ = t1 + (t0 >> (uint32_t)51U); uint64_t t0_ = t0 & (uint64_t)0x7ffffffffffffU; uint64_t t2_ = t2 + (t1_ >> (uint32_t)51U); uint64_t t1__ = t1_ & (uint64_t)0x7ffffffffffffU; uint64_t t3_ = t3 + (t2_ >> (uint32_t)51U); uint64_t t2__ = t2_ & (uint64_t)0x7ffffffffffffU; uint64_t t4_ = t4 + (t3_ >> (uint32_t)51U); uint64_t t3__ = t3_ & (uint64_t)0x7ffffffffffffU; Hacl_Lib_Create64_make_h64_5(a, t0_, t1__, t2__, t3__, t4_); Hacl_Bignum_Modulo_carry_top(a); uint64_t i0 = a[0U]; uint64_t i1 = a[1U]; uint64_t i0_ = i0 & (uint64_t)0x7ffffffffffffU; uint64_t i1_ = i1 + (i0 >> (uint32_t)51U); a[0U] = i0_; a[1U] = i1_; } static void Hacl_Bignum25519_fdifference_reduced(uint64_t *a, uint64_t *b) { Hacl_Bignum25519_fdifference(a, b); Hacl_Bignum25519_reduce_513(a); } static void Hacl_Bignum25519_fmul(uint64_t *out, uint64_t *a, uint64_t *b) { Hacl_Bignum_fmul(out, a, b); } static void Hacl_Bignum25519_times_2(uint64_t *out, uint64_t *a) { uint64_t a0 = a[0U]; uint64_t a1 = a[1U]; uint64_t a2 = a[2U]; uint64_t a3 = a[3U]; uint64_t a4 = a[4U]; uint64_t o0 = (uint64_t)2U * a0; uint64_t o1 = (uint64_t)2U * a1; uint64_t o2 = (uint64_t)2U * a2; uint64_t o3 = (uint64_t)2U * a3; uint64_t o4 = (uint64_t)2U * a4; Hacl_Lib_Create64_make_h64_5(out, o0, o1, o2, o3, o4); } static void Hacl_Bignum25519_times_d(uint64_t *out, uint64_t *a) { uint64_t d1[5U] = { 0U }; Hacl_Lib_Create64_make_h64_5(d1, (uint64_t)0x00034dca135978a3U, (uint64_t)0x0001a8283b156ebdU, (uint64_t)0x0005e7a26001c029U, (uint64_t)0x000739c663a03cbbU, (uint64_t)0x00052036cee2b6ffU); Hacl_Bignum25519_fmul(out, d1, a); } static void Hacl_Bignum25519_times_2d(uint64_t *out, uint64_t *a) { uint64_t d2[5U] = { 0U }; Hacl_Lib_Create64_make_h64_5(d2, (uint64_t)0x00069b9426b2f159U, (uint64_t)0x00035050762add7aU, (uint64_t)0x0003cf44c0038052U, (uint64_t)0x0006738cc7407977U, (uint64_t)0x0002406d9dc56dffU); Hacl_Bignum25519_fmul(out, a, d2); } static void Hacl_Bignum25519_fsquare(uint64_t *out, uint64_t *a) { KRML_CHECK_SIZE(FStar_UInt128_uint64_to_uint128((uint64_t)0U), (uint32_t)5U); FStar_UInt128_t tmp[5U]; for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i) tmp[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U); memcpy(out, a, (uint32_t)5U * sizeof a[0U]); Hacl_Bignum_Fsquare_fsquare_(tmp, out); } static void Hacl_Bignum25519_inverse(uint64_t *out, uint64_t *a) { Hacl_Bignum_Crecip_crecip(out, a); } static void Hacl_Bignum25519_reduce(uint64_t *out) { Hacl_EC_Format_reduce(out); } static uint64_t *Hacl_Impl_Ed25519_ExtPoint_getx(uint64_t *p) { return p; } static uint64_t *Hacl_Impl_Ed25519_ExtPoint_gety(uint64_t *p) { return p + (uint32_t)5U; } static uint64_t *Hacl_Impl_Ed25519_ExtPoint_getz(uint64_t *p) { return p + (uint32_t)10U; } static uint64_t *Hacl_Impl_Ed25519_ExtPoint_gett(uint64_t *p) { return p + (uint32_t)15U; } static void Hacl_Impl_Ed25519_G_make_g(uint64_t *g1) { uint64_t *gx = Hacl_Impl_Ed25519_ExtPoint_getx(g1); uint64_t *gy = Hacl_Impl_Ed25519_ExtPoint_gety(g1); uint64_t *gz = Hacl_Impl_Ed25519_ExtPoint_getz(g1); uint64_t *gt1 = Hacl_Impl_Ed25519_ExtPoint_gett(g1); Hacl_Lib_Create64_make_h64_5(gx, (uint64_t)0x00062d608f25d51aU, (uint64_t)0x000412a4b4f6592aU, (uint64_t)0x00075b7171a4b31dU, (uint64_t)0x0001ff60527118feU, (uint64_t)0x000216936d3cd6e5U); Hacl_Lib_Create64_make_h64_5(gy, (uint64_t)0x0006666666666658U, (uint64_t)0x0004ccccccccccccU, (uint64_t)0x0001999999999999U, (uint64_t)0x0003333333333333U, (uint64_t)0x0006666666666666U); Hacl_Lib_Create64_make_h64_5(gz, (uint64_t)0x0000000000000001U, (uint64_t)0x0000000000000000U, (uint64_t)0x0000000000000000U, (uint64_t)0x0000000000000000U, (uint64_t)0x0000000000000000U); Hacl_Lib_Create64_make_h64_5(gt1, (uint64_t)0x00068ab3a5b7dda3U, (uint64_t)0x00000eea2a5eadbbU, (uint64_t)0x0002af8df483c27eU, (uint64_t)0x000332b375274732U, (uint64_t)0x00067875f0fd78b7U); } static void Hacl_Impl_Store51_store_51_(uint8_t *output, uint64_t *input) { uint64_t t0 = input[0U]; uint64_t t1 = input[1U]; uint64_t t2 = input[2U]; uint64_t t3 = input[3U]; uint64_t t4 = input[4U]; uint64_t o0 = t1 << (uint32_t)51U | t0; uint64_t o1 = t2 << (uint32_t)38U | t1 >> (uint32_t)13U; uint64_t o2 = t3 << (uint32_t)25U | t2 >> (uint32_t)26U; uint64_t o3 = t4 << (uint32_t)12U | t3 >> (uint32_t)39U; uint8_t *b0 = output; uint8_t *b1 = output + (uint32_t)8U; uint8_t *b2 = output + (uint32_t)16U; uint8_t *b3 = output + (uint32_t)24U; store64_le(b0, o0); store64_le(b1, o1); store64_le(b2, o2); store64_le(b3, o3); } static uint64_t Hacl_Impl_Ed25519_PointCompress_x_mod_2(uint64_t *x) { uint64_t x0 = x[0U]; return x0 & (uint64_t)1U; } static void Hacl_Impl_Ed25519_PointCompress_point_compress(uint8_t *z, uint64_t *p) { uint64_t tmp[15U] = { 0U }; uint64_t *x0 = tmp + (uint32_t)5U; uint64_t *out0 = tmp + (uint32_t)10U; uint64_t *zinv = tmp; uint64_t *x = tmp + (uint32_t)5U; uint64_t *out = tmp + (uint32_t)10U; uint64_t *px = Hacl_Impl_Ed25519_ExtPoint_getx(p); uint64_t *py = Hacl_Impl_Ed25519_ExtPoint_gety(p); uint64_t *pz = Hacl_Impl_Ed25519_ExtPoint_getz(p); Hacl_Bignum25519_inverse(zinv, pz); Hacl_Bignum25519_fmul(x, px, zinv); Hacl_Bignum25519_reduce(x); Hacl_Bignum25519_fmul(out, py, zinv); Hacl_Bignum25519_reduce(out); uint64_t b = Hacl_Impl_Ed25519_PointCompress_x_mod_2(x0); Hacl_Impl_Store51_store_51_(z, out0); uint8_t xbyte = (uint8_t)b; uint8_t o31 = z[31U]; z[31U] = o31 + (xbyte << (uint32_t)7U); } static void Hacl_Impl_Ed25519_SwapConditional_swap_conditional_step( uint64_t *a_, uint64_t *b_, uint64_t *a, uint64_t *b, uint64_t swap1 ) { uint64_t a0 = a[0U]; uint64_t a1 = a[1U]; uint64_t a2 = a[2U]; uint64_t a3 = a[3U]; uint64_t a4 = a[4U]; uint64_t b0 = b[0U]; uint64_t b1 = b[1U]; uint64_t b2 = b[2U]; uint64_t b3 = b[3U]; uint64_t b4 = b[4U]; uint64_t x0 = swap1 & (a0 ^ b0); uint64_t x1 = swap1 & (a1 ^ b1); uint64_t x2 = swap1 & (a2 ^ b2); uint64_t x3 = swap1 & (a3 ^ b3); uint64_t x4 = swap1 & (a4 ^ b4); uint64_t a0_ = a0 ^ x0; uint64_t b0_ = b0 ^ x0; uint64_t a1_ = a1 ^ x1; uint64_t b1_ = b1 ^ x1; uint64_t a2_ = a2 ^ x2; uint64_t b2_ = b2 ^ x2; uint64_t a3_ = a3 ^ x3; uint64_t b3_ = b3 ^ x3; uint64_t a4_ = a4 ^ x4; uint64_t b4_ = b4 ^ x4; Hacl_Lib_Create64_make_h64_5(a_, a0_, a1_, a2_, a3_, a4_); Hacl_Lib_Create64_make_h64_5(b_, b0_, b1_, b2_, b3_, b4_); } static void Hacl_Impl_Ed25519_SwapConditional_swap_conditional( uint64_t *a_, uint64_t *b_, uint64_t *a, uint64_t *b, uint64_t iswap ) { uint64_t swap1 = (uint64_t)0U - iswap; Hacl_Impl_Ed25519_SwapConditional_swap_conditional_step(Hacl_Impl_Ed25519_ExtPoint_getx(a_), Hacl_Impl_Ed25519_ExtPoint_getx(b_), Hacl_Impl_Ed25519_ExtPoint_getx(a), Hacl_Impl_Ed25519_ExtPoint_getx(b), swap1); Hacl_Impl_Ed25519_SwapConditional_swap_conditional_step(Hacl_Impl_Ed25519_ExtPoint_gety(a_), Hacl_Impl_Ed25519_ExtPoint_gety(b_), Hacl_Impl_Ed25519_ExtPoint_gety(a), Hacl_Impl_Ed25519_ExtPoint_gety(b), swap1); Hacl_Impl_Ed25519_SwapConditional_swap_conditional_step(Hacl_Impl_Ed25519_ExtPoint_getz(a_), Hacl_Impl_Ed25519_ExtPoint_getz(b_), Hacl_Impl_Ed25519_ExtPoint_getz(a), Hacl_Impl_Ed25519_ExtPoint_getz(b), swap1); Hacl_Impl_Ed25519_SwapConditional_swap_conditional_step(Hacl_Impl_Ed25519_ExtPoint_gett(a_), Hacl_Impl_Ed25519_ExtPoint_gett(b_), Hacl_Impl_Ed25519_ExtPoint_gett(a), Hacl_Impl_Ed25519_ExtPoint_gett(b), swap1); } static void Hacl_Impl_Ed25519_SwapConditional_swap_conditional_inplace( uint64_t *a, uint64_t *b, uint64_t iswap ) { uint64_t swap1 = (uint64_t)0U - iswap; Hacl_Impl_Ed25519_SwapConditional_swap_conditional_step(Hacl_Impl_Ed25519_ExtPoint_getx(a), Hacl_Impl_Ed25519_ExtPoint_getx(b), Hacl_Impl_Ed25519_ExtPoint_getx(a), Hacl_Impl_Ed25519_ExtPoint_getx(b), swap1); Hacl_Impl_Ed25519_SwapConditional_swap_conditional_step(Hacl_Impl_Ed25519_ExtPoint_gety(a), Hacl_Impl_Ed25519_ExtPoint_gety(b), Hacl_Impl_Ed25519_ExtPoint_gety(a), Hacl_Impl_Ed25519_ExtPoint_gety(b), swap1); Hacl_Impl_Ed25519_SwapConditional_swap_conditional_step(Hacl_Impl_Ed25519_ExtPoint_getz(a), Hacl_Impl_Ed25519_ExtPoint_getz(b), Hacl_Impl_Ed25519_ExtPoint_getz(a), Hacl_Impl_Ed25519_ExtPoint_getz(b), swap1); Hacl_Impl_Ed25519_SwapConditional_swap_conditional_step(Hacl_Impl_Ed25519_ExtPoint_gett(a), Hacl_Impl_Ed25519_ExtPoint_gett(b), Hacl_Impl_Ed25519_ExtPoint_gett(a), Hacl_Impl_Ed25519_ExtPoint_gett(b), swap1); } static void Hacl_Impl_Ed25519_SwapConditional_copy(uint64_t *output, uint64_t *input) { memcpy(output, input, (uint32_t)20U * sizeof input[0U]); } static void Hacl_Impl_Ed25519_PointAdd_point_add(uint64_t *out, uint64_t *p, uint64_t *q1) { uint64_t tmp[30U] = { 0U }; uint64_t *tmp1 = tmp; uint64_t *tmp20 = tmp + (uint32_t)5U; uint64_t *tmp30 = tmp + (uint32_t)10U; uint64_t *tmp40 = tmp + (uint32_t)15U; uint64_t *x1 = Hacl_Impl_Ed25519_ExtPoint_getx(p); uint64_t *y1 = Hacl_Impl_Ed25519_ExtPoint_gety(p); uint64_t *x2 = Hacl_Impl_Ed25519_ExtPoint_getx(q1); uint64_t *y2 = Hacl_Impl_Ed25519_ExtPoint_gety(q1); memcpy(tmp1, x1, (uint32_t)5U * sizeof x1[0U]); memcpy(tmp20, x2, (uint32_t)5U * sizeof x2[0U]); Hacl_Bignum25519_fdifference_reduced(tmp1, y1); Hacl_Bignum25519_fdifference(tmp20, y2); Hacl_Bignum25519_fmul(tmp30, tmp1, tmp20); memcpy(tmp1, y1, (uint32_t)5U * sizeof y1[0U]); memcpy(tmp20, y2, (uint32_t)5U * sizeof y2[0U]); Hacl_Bignum25519_fsum(tmp1, x1); Hacl_Bignum25519_fsum(tmp20, x2); Hacl_Bignum25519_fmul(tmp40, tmp1, tmp20); uint64_t *tmp10 = tmp; uint64_t *tmp21 = tmp + (uint32_t)5U; uint64_t *tmp31 = tmp + (uint32_t)10U; uint64_t *tmp50 = tmp + (uint32_t)20U; uint64_t *tmp60 = tmp + (uint32_t)25U; uint64_t *z1 = Hacl_Impl_Ed25519_ExtPoint_getz(p); uint64_t *t1 = Hacl_Impl_Ed25519_ExtPoint_gett(p); uint64_t *z2 = Hacl_Impl_Ed25519_ExtPoint_getz(q1); uint64_t *t2 = Hacl_Impl_Ed25519_ExtPoint_gett(q1); Hacl_Bignum25519_times_2d(tmp10, t1); Hacl_Bignum25519_fmul(tmp21, tmp10, t2); Hacl_Bignum25519_times_2(tmp10, z1); Hacl_Bignum25519_fmul(tmp50, tmp10, z2); memcpy(tmp10, tmp31, (uint32_t)5U * sizeof tmp31[0U]); memcpy(tmp60, tmp21, (uint32_t)5U * sizeof tmp21[0U]); uint64_t *tmp11 = tmp; uint64_t *tmp2 = tmp + (uint32_t)5U; uint64_t *tmp3 = tmp + (uint32_t)10U; uint64_t *tmp41 = tmp + (uint32_t)15U; uint64_t *tmp51 = tmp + (uint32_t)20U; uint64_t *tmp61 = tmp + (uint32_t)25U; Hacl_Bignum25519_fdifference_reduced(tmp11, tmp41); Hacl_Bignum25519_fdifference(tmp61, tmp51); Hacl_Bignum25519_fsum(tmp51, tmp2); Hacl_Bignum25519_fsum(tmp41, tmp3); uint64_t *tmp12 = tmp; uint64_t *tmp4 = tmp + (uint32_t)15U; uint64_t *tmp5 = tmp + (uint32_t)20U; uint64_t *tmp6 = tmp + (uint32_t)25U; uint64_t *x3 = Hacl_Impl_Ed25519_ExtPoint_getx(out); uint64_t *y3 = Hacl_Impl_Ed25519_ExtPoint_gety(out); uint64_t *z3 = Hacl_Impl_Ed25519_ExtPoint_getz(out); uint64_t *t3 = Hacl_Impl_Ed25519_ExtPoint_gett(out); Hacl_Bignum25519_fmul(x3, tmp12, tmp6); Hacl_Bignum25519_fmul(y3, tmp5, tmp4); Hacl_Bignum25519_fmul(t3, tmp12, tmp4); Hacl_Bignum25519_fmul(z3, tmp5, tmp6); } static void Hacl_Impl_Ed25519_PointDouble_point_double_step_1(uint64_t *p, uint64_t *tmp) { uint64_t *tmp1 = tmp; uint64_t *tmp2 = tmp + (uint32_t)5U; uint64_t *tmp3 = tmp + (uint32_t)10U; uint64_t *tmp4 = tmp + (uint32_t)15U; uint64_t *x1 = Hacl_Impl_Ed25519_ExtPoint_getx(p); uint64_t *y1 = Hacl_Impl_Ed25519_ExtPoint_gety(p); uint64_t *z1 = Hacl_Impl_Ed25519_ExtPoint_getz(p); Hacl_Bignum25519_fsquare(tmp1, x1); Hacl_Bignum25519_fsquare(tmp2, y1); Hacl_Bignum25519_fsquare(tmp3, z1); Hacl_Bignum25519_times_2(tmp4, tmp3); memcpy(tmp3, tmp1, (uint32_t)5U * sizeof tmp1[0U]); Hacl_Bignum25519_fsum(tmp3, tmp2); Hacl_Bignum25519_reduce_513(tmp3); } static void Hacl_Impl_Ed25519_PointDouble_point_double_step_2(uint64_t *p, uint64_t *tmp) { uint64_t *tmp1 = tmp; uint64_t *tmp2 = tmp + (uint32_t)5U; uint64_t *tmp3 = tmp + (uint32_t)10U; uint64_t *tmp4 = tmp + (uint32_t)15U; uint64_t *tmp5 = tmp + (uint32_t)20U; uint64_t *tmp6 = tmp + (uint32_t)25U; uint64_t *x1 = Hacl_Impl_Ed25519_ExtPoint_getx(p); uint64_t *y1 = Hacl_Impl_Ed25519_ExtPoint_gety(p); memcpy(tmp5, x1, (uint32_t)5U * sizeof x1[0U]); Hacl_Bignum25519_fsum(tmp5, y1); Hacl_Bignum25519_fsquare(tmp6, tmp5); memcpy(tmp5, tmp3, (uint32_t)5U * sizeof tmp3[0U]); Hacl_Bignum25519_fdifference(tmp6, tmp5); Hacl_Bignum25519_fdifference_reduced(tmp2, tmp1); Hacl_Bignum25519_reduce_513(tmp4); Hacl_Bignum25519_fsum(tmp4, tmp2); } static void Hacl_Impl_Ed25519_PointDouble_point_double_(uint64_t *out, uint64_t *p, uint64_t *tmp) { uint64_t *tmp2 = tmp + (uint32_t)5U; uint64_t *tmp3 = tmp + (uint32_t)10U; uint64_t *tmp4 = tmp + (uint32_t)15U; uint64_t *tmp6 = tmp + (uint32_t)25U; uint64_t *x3 = Hacl_Impl_Ed25519_ExtPoint_getx(out); uint64_t *y3 = Hacl_Impl_Ed25519_ExtPoint_gety(out); uint64_t *z3 = Hacl_Impl_Ed25519_ExtPoint_getz(out); uint64_t *t3 = Hacl_Impl_Ed25519_ExtPoint_gett(out); Hacl_Impl_Ed25519_PointDouble_point_double_step_1(p, tmp); Hacl_Impl_Ed25519_PointDouble_point_double_step_2(p, tmp); Hacl_Bignum25519_fmul(x3, tmp4, tmp6); Hacl_Bignum25519_fmul(y3, tmp2, tmp3); Hacl_Bignum25519_fmul(t3, tmp3, tmp6); Hacl_Bignum25519_fmul(z3, tmp4, tmp2); } static void Hacl_Impl_Ed25519_PointDouble_point_double(uint64_t *out, uint64_t *p) { uint64_t tmp[30U] = { 0U }; Hacl_Impl_Ed25519_PointDouble_point_double_(out, p, tmp); } static uint8_t Hacl_Impl_Ed25519_Ladder_Step_ith_bit(uint8_t *k1, uint32_t i) { uint32_t q1 = i >> (uint32_t)3U; uint32_t r = i & (uint32_t)7U; uint8_t kq = k1[q1]; return kq >> r & (uint8_t)1U; } static void Hacl_Impl_Ed25519_Ladder_Step_swap_cond_inplace(uint64_t *p, uint64_t *q1, uint64_t iswap) { Hacl_Impl_Ed25519_SwapConditional_swap_conditional_inplace(p, q1, iswap); } static void Hacl_Impl_Ed25519_Ladder_Step_swap_cond( uint64_t *p_, uint64_t *q_, uint64_t *p, uint64_t *q1, uint64_t iswap ) { Hacl_Impl_Ed25519_SwapConditional_swap_conditional(p_, q_, p, q1, iswap); } static void Hacl_Impl_Ed25519_Ladder_Step_loop_step_1(uint64_t *b, uint8_t *k1, uint32_t ctr, uint8_t i) { uint64_t *nq = b; uint64_t *nqpq = b + (uint32_t)20U; uint64_t bit = (uint64_t)i; Hacl_Impl_Ed25519_Ladder_Step_swap_cond_inplace(nq, nqpq, bit); } static void Hacl_Impl_Ed25519_Ladder_Step_loop_step_2(uint64_t *b, uint8_t *k1, uint32_t ctr) { uint64_t *nq = b; uint64_t *nqpq = b + (uint32_t)20U; uint64_t *nq2 = b + (uint32_t)40U; uint64_t *nqpq2 = b + (uint32_t)60U; Hacl_Impl_Ed25519_PointDouble_point_double(nq2, nq); Hacl_Impl_Ed25519_PointAdd_point_add(nqpq2, nq, nqpq); } static void Hacl_Impl_Ed25519_Ladder_Step_loop_step_3(uint64_t *b, uint8_t *k1, uint32_t ctr, uint8_t i) { uint64_t *nq = b; uint64_t *nqpq = b + (uint32_t)20U; uint64_t *nq2 = b + (uint32_t)40U; uint64_t *nqpq2 = b + (uint32_t)60U; uint64_t bit = (uint64_t)i; Hacl_Impl_Ed25519_Ladder_Step_swap_cond(nq, nqpq, nq2, nqpq2, bit); } static void Hacl_Impl_Ed25519_Ladder_Step_loop_step(uint64_t *b, uint8_t *k1, uint32_t ctr) { uint8_t bit = Hacl_Impl_Ed25519_Ladder_Step_ith_bit(k1, ctr); Hacl_Impl_Ed25519_Ladder_Step_loop_step_1(b, k1, ctr, bit); Hacl_Impl_Ed25519_Ladder_Step_loop_step_2(b, k1, ctr); Hacl_Impl_Ed25519_Ladder_Step_loop_step_3(b, k1, ctr, bit); } static void Hacl_Impl_Ed25519_Ladder_point_mul_(uint64_t *b, uint8_t *k1) { for (uint32_t i = (uint32_t)0U; i < (uint32_t)256U; i = i + (uint32_t)1U) Hacl_Impl_Ed25519_Ladder_Step_loop_step(b, k1, (uint32_t)256U - i - (uint32_t)1U); } static void Hacl_Impl_Ed25519_Ladder_make_point_inf(uint64_t *b) { uint64_t *x = b; uint64_t *y = b + (uint32_t)5U; uint64_t *z = b + (uint32_t)10U; uint64_t *t = b + (uint32_t)15U; uint64_t zero1 = (uint64_t)0U; Hacl_Lib_Create64_make_h64_5(x, zero1, zero1, zero1, zero1, zero1); uint64_t zero10 = (uint64_t)0U; uint64_t one10 = (uint64_t)1U; Hacl_Lib_Create64_make_h64_5(y, one10, zero10, zero10, zero10, zero10); uint64_t zero11 = (uint64_t)0U; uint64_t one1 = (uint64_t)1U; Hacl_Lib_Create64_make_h64_5(z, one1, zero11, zero11, zero11, zero11); uint64_t zero12 = (uint64_t)0U; Hacl_Lib_Create64_make_h64_5(t, zero12, zero12, zero12, zero12, zero12); } static void Hacl_Impl_Ed25519_Ladder_point_mul(uint64_t *result, uint8_t *scalar, uint64_t *q1) { uint64_t b[80U] = { 0U }; uint64_t *nq = b; uint64_t *nqpq = b + (uint32_t)20U; Hacl_Impl_Ed25519_Ladder_make_point_inf(nq); Hacl_Impl_Ed25519_SwapConditional_copy(nqpq, q1); Hacl_Impl_Ed25519_Ladder_point_mul_(b, scalar); Hacl_Impl_Ed25519_SwapConditional_copy(result, nq); } static void Hacl_Hash_Lib_LoadStore_uint64s_from_be_bytes(uint64_t *output, uint8_t *input, uint32_t len1) { for (uint32_t i = (uint32_t)0U; i < len1; i = i + (uint32_t)1U) { uint8_t *x0 = input + (uint32_t)8U * i; uint64_t inputi = load64_be(x0); output[i] = inputi; } } static void Hacl_Hash_Lib_LoadStore_uint64s_to_be_bytes(uint8_t *output, uint64_t *input, uint32_t len1) { for (uint32_t i = (uint32_t)0U; i < len1; i = i + (uint32_t)1U) { uint64_t hd1 = input[i]; uint8_t *x0 = output + (uint32_t)8U * i; store64_be(x0, hd1); } } static void Hacl_Impl_SHA2_512_init(uint64_t *state) { uint64_t *k1 = state; uint64_t *h_01 = state + (uint32_t)160U; uint64_t *p10 = k1; uint64_t *p20 = k1 + (uint32_t)16U; uint64_t *p3 = k1 + (uint32_t)32U; uint64_t *p4 = k1 + (uint32_t)48U; uint64_t *p5 = k1 + (uint32_t)64U; uint64_t *p11 = p10; uint64_t *p21 = p10 + (uint32_t)8U; uint64_t *p12 = p11; uint64_t *p22 = p11 + (uint32_t)4U; p12[0U] = (uint64_t)0x428a2f98d728ae22U; p12[1U] = (uint64_t)0x7137449123ef65cdU; p12[2U] = (uint64_t)0xb5c0fbcfec4d3b2fU; p12[3U] = (uint64_t)0xe9b5dba58189dbbcU; p22[0U] = (uint64_t)0x3956c25bf348b538U; p22[1U] = (uint64_t)0x59f111f1b605d019U; p22[2U] = (uint64_t)0x923f82a4af194f9bU; p22[3U] = (uint64_t)0xab1c5ed5da6d8118U; uint64_t *p13 = p21; uint64_t *p23 = p21 + (uint32_t)4U; p13[0U] = (uint64_t)0xd807aa98a3030242U; p13[1U] = (uint64_t)0x12835b0145706fbeU; p13[2U] = (uint64_t)0x243185be4ee4b28cU; p13[3U] = (uint64_t)0x550c7dc3d5ffb4e2U; p23[0U] = (uint64_t)0x72be5d74f27b896fU; p23[1U] = (uint64_t)0x80deb1fe3b1696b1U; p23[2U] = (uint64_t)0x9bdc06a725c71235U; p23[3U] = (uint64_t)0xc19bf174cf692694U; uint64_t *p14 = p20; uint64_t *p24 = p20 + (uint32_t)8U; uint64_t *p15 = p14; uint64_t *p25 = p14 + (uint32_t)4U; p15[0U] = (uint64_t)0xe49b69c19ef14ad2U; p15[1U] = (uint64_t)0xefbe4786384f25e3U; p15[2U] = (uint64_t)0x0fc19dc68b8cd5b5U; p15[3U] = (uint64_t)0x240ca1cc77ac9c65U; p25[0U] = (uint64_t)0x2de92c6f592b0275U; p25[1U] = (uint64_t)0x4a7484aa6ea6e483U; p25[2U] = (uint64_t)0x5cb0a9dcbd41fbd4U; p25[3U] = (uint64_t)0x76f988da831153b5U; uint64_t *p16 = p24; uint64_t *p26 = p24 + (uint32_t)4U; p16[0U] = (uint64_t)0x983e5152ee66dfabU; p16[1U] = (uint64_t)0xa831c66d2db43210U; p16[2U] = (uint64_t)0xb00327c898fb213fU; p16[3U] = (uint64_t)0xbf597fc7beef0ee4U; p26[0U] = (uint64_t)0xc6e00bf33da88fc2U; p26[1U] = (uint64_t)0xd5a79147930aa725U; p26[2U] = (uint64_t)0x06ca6351e003826fU; p26[3U] = (uint64_t)0x142929670a0e6e70U; uint64_t *p17 = p3; uint64_t *p27 = p3 + (uint32_t)8U; uint64_t *p18 = p17; uint64_t *p28 = p17 + (uint32_t)4U; p18[0U] = (uint64_t)0x27b70a8546d22ffcU; p18[1U] = (uint64_t)0x2e1b21385c26c926U; p18[2U] = (uint64_t)0x4d2c6dfc5ac42aedU; p18[3U] = (uint64_t)0x53380d139d95b3dfU; p28[0U] = (uint64_t)0x650a73548baf63deU; p28[1U] = (uint64_t)0x766a0abb3c77b2a8U; p28[2U] = (uint64_t)0x81c2c92e47edaee6U; p28[3U] = (uint64_t)0x92722c851482353bU; uint64_t *p19 = p27; uint64_t *p29 = p27 + (uint32_t)4U; p19[0U] = (uint64_t)0xa2bfe8a14cf10364U; p19[1U] = (uint64_t)0xa81a664bbc423001U; p19[2U] = (uint64_t)0xc24b8b70d0f89791U; p19[3U] = (uint64_t)0xc76c51a30654be30U; p29[0U] = (uint64_t)0xd192e819d6ef5218U; p29[1U] = (uint64_t)0xd69906245565a910U; p29[2U] = (uint64_t)0xf40e35855771202aU; p29[3U] = (uint64_t)0x106aa07032bbd1b8U; uint64_t *p110 = p4; uint64_t *p210 = p4 + (uint32_t)8U; uint64_t *p111 = p110; uint64_t *p211 = p110 + (uint32_t)4U; p111[0U] = (uint64_t)0x19a4c116b8d2d0c8U; p111[1U] = (uint64_t)0x1e376c085141ab53U; p111[2U] = (uint64_t)0x2748774cdf8eeb99U; p111[3U] = (uint64_t)0x34b0bcb5e19b48a8U; p211[0U] = (uint64_t)0x391c0cb3c5c95a63U; p211[1U] = (uint64_t)0x4ed8aa4ae3418acbU; p211[2U] = (uint64_t)0x5b9cca4f7763e373U; p211[3U] = (uint64_t)0x682e6ff3d6b2b8a3U; uint64_t *p112 = p210; uint64_t *p212 = p210 + (uint32_t)4U; p112[0U] = (uint64_t)0x748f82ee5defb2fcU; p112[1U] = (uint64_t)0x78a5636f43172f60U; p112[2U] = (uint64_t)0x84c87814a1f0ab72U; p112[3U] = (uint64_t)0x8cc702081a6439ecU; p212[0U] = (uint64_t)0x90befffa23631e28U; p212[1U] = (uint64_t)0xa4506cebde82bde9U; p212[2U] = (uint64_t)0xbef9a3f7b2c67915U; p212[3U] = (uint64_t)0xc67178f2e372532bU; uint64_t *p113 = p5; uint64_t *p213 = p5 + (uint32_t)8U; uint64_t *p1 = p113; uint64_t *p214 = p113 + (uint32_t)4U; p1[0U] = (uint64_t)0xca273eceea26619cU; p1[1U] = (uint64_t)0xd186b8c721c0c207U; p1[2U] = (uint64_t)0xeada7dd6cde0eb1eU; p1[3U] = (uint64_t)0xf57d4f7fee6ed178U; p214[0U] = (uint64_t)0x06f067aa72176fbaU; p214[1U] = (uint64_t)0x0a637dc5a2c898a6U; p214[2U] = (uint64_t)0x113f9804bef90daeU; p214[3U] = (uint64_t)0x1b710b35131c471bU; uint64_t *p114 = p213; uint64_t *p215 = p213 + (uint32_t)4U; p114[0U] = (uint64_t)0x28db77f523047d84U; p114[1U] = (uint64_t)0x32caab7b40c72493U; p114[2U] = (uint64_t)0x3c9ebe0a15c9bebcU; p114[3U] = (uint64_t)0x431d67c49c100d4cU; p215[0U] = (uint64_t)0x4cc5d4becb3e42b6U; p215[1U] = (uint64_t)0x597f299cfc657e2aU; p215[2U] = (uint64_t)0x5fcb6fab3ad6faecU; p215[3U] = (uint64_t)0x6c44198c4a475817U; uint64_t *p115 = h_01; uint64_t *p2 = h_01 + (uint32_t)4U; p115[0U] = (uint64_t)0x6a09e667f3bcc908U; p115[1U] = (uint64_t)0xbb67ae8584caa73bU; p115[2U] = (uint64_t)0x3c6ef372fe94f82bU; p115[3U] = (uint64_t)0xa54ff53a5f1d36f1U; p2[0U] = (uint64_t)0x510e527fade682d1U; p2[1U] = (uint64_t)0x9b05688c2b3e6c1fU; p2[2U] = (uint64_t)0x1f83d9abfb41bd6bU; p2[3U] = (uint64_t)0x5be0cd19137e2179U; } static void Hacl_Impl_SHA2_512_update(uint64_t *state, uint8_t *data) { KRML_CHECK_SIZE((uint64_t)(uint32_t)0U, (uint32_t)16U); uint64_t data_w[16U]; for (uint32_t _i = 0U; _i < (uint32_t)16U; ++_i) data_w[_i] = (uint64_t)(uint32_t)0U; Hacl_Hash_Lib_LoadStore_uint64s_from_be_bytes(data_w, data, (uint32_t)16U); uint64_t *hash_w = state + (uint32_t)160U; uint64_t *ws_w = state + (uint32_t)80U; uint64_t *k_w = state; uint64_t *counter_w = state + (uint32_t)168U; for (uint32_t i = (uint32_t)0U; i < (uint32_t)16U; i = i + (uint32_t)1U) { uint64_t b = data_w[i]; ws_w[i] = b; } for (uint32_t i = (uint32_t)16U; i < (uint32_t)80U; i = i + (uint32_t)1U) { uint64_t t16 = ws_w[i - (uint32_t)16U]; uint64_t t15 = ws_w[i - (uint32_t)15U]; uint64_t t7 = ws_w[i - (uint32_t)7U]; uint64_t t2 = ws_w[i - (uint32_t)2U]; ws_w[i] = ((t2 >> (uint32_t)19U | t2 << ((uint32_t)64U - (uint32_t)19U)) ^ ((t2 >> (uint32_t)61U | t2 << ((uint32_t)64U - (uint32_t)61U)) ^ t2 >> (uint32_t)6U)) + t7 + ((t15 >> (uint32_t)1U | t15 << ((uint32_t)64U - (uint32_t)1U)) ^ ((t15 >> (uint32_t)8U | t15 << ((uint32_t)64U - (uint32_t)8U)) ^ t15 >> (uint32_t)7U)) + t16; } uint64_t hash_0[8U] = { 0U }; memcpy(hash_0, hash_w, (uint32_t)8U * sizeof hash_w[0U]); for (uint32_t i = (uint32_t)0U; i < (uint32_t)80U; i = i + (uint32_t)1U) { uint64_t a = hash_0[0U]; uint64_t b = hash_0[1U]; uint64_t c = hash_0[2U]; uint64_t d1 = hash_0[3U]; uint64_t e = hash_0[4U]; uint64_t f1 = hash_0[5U]; uint64_t g1 = hash_0[6U]; uint64_t h = hash_0[7U]; uint64_t k_t = k_w[i]; uint64_t ws_t = ws_w[i]; uint64_t t1 = h + ((e >> (uint32_t)14U | e << ((uint32_t)64U - (uint32_t)14U)) ^ ((e >> (uint32_t)18U | e << ((uint32_t)64U - (uint32_t)18U)) ^ (e >> (uint32_t)41U | e << ((uint32_t)64U - (uint32_t)41U)))) + ((e & f1) ^ (~e & g1)) + k_t + ws_t; uint64_t t2 = ((a >> (uint32_t)28U | a << ((uint32_t)64U - (uint32_t)28U)) ^ ((a >> (uint32_t)34U | a << ((uint32_t)64U - (uint32_t)34U)) ^ (a >> (uint32_t)39U | a << ((uint32_t)64U - (uint32_t)39U)))) + ((a & b) ^ ((a & c) ^ (b & c))); uint64_t x1 = t1 + t2; uint64_t x5 = d1 + t1; uint64_t *p1 = hash_0; uint64_t *p2 = hash_0 + (uint32_t)4U; p1[0U] = x1; p1[1U] = a; p1[2U] = b; p1[3U] = c; p2[0U] = x5; p2[1U] = e; p2[2U] = f1; p2[3U] = g1; } for (uint32_t i = (uint32_t)0U; i < (uint32_t)8U; i = i + (uint32_t)1U) { uint64_t xi = hash_w[i]; uint64_t yi = hash_0[i]; hash_w[i] = xi + yi; } uint64_t c0 = counter_w[0U]; uint64_t one1 = (uint64_t)(uint32_t)1U; counter_w[0U] = c0 + one1; } static void Hacl_Impl_SHA2_512_update_multi(uint64_t *state, uint8_t *data, uint32_t n1) { for (uint32_t i = (uint32_t)0U; i < n1; i = i + (uint32_t)1U) { uint8_t *b = data + i * (uint32_t)128U; Hacl_Impl_SHA2_512_update(state, b); } } static void Hacl_Impl_SHA2_512_update_last(uint64_t *state, uint8_t *data, uint64_t len1) { uint8_t blocks[256U] = { 0U }; uint32_t nb; if (len1 < (uint64_t)112U) nb = (uint32_t)1U; else nb = (uint32_t)2U; uint8_t *final_blocks; if (len1 < (uint64_t)112U) final_blocks = blocks + (uint32_t)128U; else final_blocks = blocks; memcpy(final_blocks, data, (uint32_t)len1 * sizeof data[0U]); uint64_t n1 = state[168U]; uint8_t *padding = final_blocks + (uint32_t)len1; FStar_UInt128_t encodedlen = FStar_UInt128_shift_left(FStar_UInt128_add(FStar_UInt128_mul_wide(n1, (uint64_t)(uint32_t)128U), FStar_UInt128_uint64_to_uint128(len1)), (uint32_t)3U); uint32_t pad0len = ((uint32_t)256U - ((uint32_t)len1 + (uint32_t)16U + (uint32_t)1U)) % (uint32_t)128U; uint8_t *buf1 = padding; uint8_t *buf2 = padding + (uint32_t)1U + pad0len; buf1[0U] = (uint8_t)0x80U; store128_be(buf2, encodedlen); Hacl_Impl_SHA2_512_update_multi(state, final_blocks, nb); } static void Hacl_Impl_SHA2_512_finish(uint64_t *state, uint8_t *hash1) { uint64_t *hash_w = state + (uint32_t)160U; Hacl_Hash_Lib_LoadStore_uint64s_to_be_bytes(hash1, hash_w, (uint32_t)8U); } static void Hacl_Impl_SHA2_512_hash(uint8_t *hash1, uint8_t *input, uint32_t len1) { KRML_CHECK_SIZE((uint64_t)(uint32_t)0U, (uint32_t)169U); uint64_t state[169U]; for (uint32_t _i = 0U; _i < (uint32_t)169U; ++_i) state[_i] = (uint64_t)(uint32_t)0U; uint32_t n1 = len1 / (uint32_t)128U; uint32_t r = len1 % (uint32_t)128U; uint8_t *input_blocks = input; uint8_t *input_last = input + n1 * (uint32_t)128U; Hacl_Impl_SHA2_512_init(state); Hacl_Impl_SHA2_512_update_multi(state, input_blocks, n1); Hacl_Impl_SHA2_512_update_last(state, input_last, (uint64_t)r); Hacl_Impl_SHA2_512_finish(state, hash1); } static void Hacl_SHA2_512_hash(uint8_t *hash1, uint8_t *input, uint32_t len1) { Hacl_Impl_SHA2_512_hash(hash1, input, len1); } static void Hacl_Impl_Ed25519_SecretExpand_secret_expand(uint8_t *expanded, uint8_t *secret) { Hacl_SHA2_512_hash(expanded, secret, (uint32_t)32U); uint8_t *h_low = expanded; uint8_t h_low0 = h_low[0U]; uint8_t h_low31 = h_low[31U]; h_low[0U] = h_low0 & (uint8_t)0xf8U; h_low[31U] = (h_low31 & (uint8_t)127U) | (uint8_t)64U; } static void Hacl_Impl_Ed25519_SecretToPublic_point_mul_g(uint64_t *result, uint8_t *scalar) { uint64_t g1[20U] = { 0U }; Hacl_Impl_Ed25519_G_make_g(g1); Hacl_Impl_Ed25519_Ladder_point_mul(result, scalar, g1); } static void Hacl_Impl_Ed25519_SecretToPublic_secret_to_public_( uint8_t *out, uint8_t *secret, uint8_t *expanded_secret ) { uint8_t *a = expanded_secret; uint64_t res[20U] = { 0U }; Hacl_Impl_Ed25519_SecretToPublic_point_mul_g(res, a); Hacl_Impl_Ed25519_PointCompress_point_compress(out, res); } static void Hacl_Impl_Ed25519_SecretToPublic_secret_to_public(uint8_t *out, uint8_t *secret) { uint8_t expanded[64U] = { 0U }; Hacl_Impl_Ed25519_SecretExpand_secret_expand(expanded, secret); Hacl_Impl_Ed25519_SecretToPublic_secret_to_public_(out, secret, expanded); } static bool Hacl_Impl_Ed25519_PointEqual_gte_q(uint64_t *s) { uint64_t s0 = s[0U]; uint64_t s1 = s[1U]; uint64_t s2 = s[2U]; uint64_t s3 = s[3U]; uint64_t s4 = s[4U]; if (s4 > (uint64_t)0x00000010000000U) return true; else if (s4 < (uint64_t)0x00000010000000U) return false; else if (s3 > (uint64_t)0x00000000000000U) return true; else if (s2 > (uint64_t)0x000000000014deU) return true; else if (s2 < (uint64_t)0x000000000014deU) return false; else if (s1 > (uint64_t)0xf9dea2f79cd658U) return true; else if (s1 < (uint64_t)0xf9dea2f79cd658U) return false; else if (s0 >= (uint64_t)0x12631a5cf5d3edU) return true; else return false; } static bool Hacl_Impl_Ed25519_PointEqual_eq(uint64_t *a, uint64_t *b) { uint64_t a0 = a[0U]; uint64_t a1 = a[1U]; uint64_t a2 = a[2U]; uint64_t a3 = a[3U]; uint64_t a4 = a[4U]; uint64_t b0 = b[0U]; uint64_t b1 = b[1U]; uint64_t b2 = b[2U]; uint64_t b3 = b[3U]; uint64_t b4 = b[4U]; bool z = a0 == b0 && a1 == b1 && a2 == b2 && a3 == b3 && a4 == b4; return z; } static bool Hacl_Impl_Ed25519_PointEqual_point_equal_1(uint64_t *p, uint64_t *q1, uint64_t *tmp) { uint64_t *pxqz = tmp; uint64_t *qxpz = tmp + (uint32_t)5U; Hacl_Bignum25519_fmul(pxqz, Hacl_Impl_Ed25519_ExtPoint_getx(p), Hacl_Impl_Ed25519_ExtPoint_getz(q1)); Hacl_Bignum25519_reduce(pxqz); Hacl_Bignum25519_fmul(qxpz, Hacl_Impl_Ed25519_ExtPoint_getx(q1), Hacl_Impl_Ed25519_ExtPoint_getz(p)); Hacl_Bignum25519_reduce(qxpz); bool b = Hacl_Impl_Ed25519_PointEqual_eq(pxqz, qxpz); return b; } static bool Hacl_Impl_Ed25519_PointEqual_point_equal_2(uint64_t *p, uint64_t *q1, uint64_t *tmp) { uint64_t *pyqz = tmp + (uint32_t)10U; uint64_t *qypz = tmp + (uint32_t)15U; Hacl_Bignum25519_fmul(pyqz, Hacl_Impl_Ed25519_ExtPoint_gety(p), Hacl_Impl_Ed25519_ExtPoint_getz(q1)); Hacl_Bignum25519_reduce(pyqz); Hacl_Bignum25519_fmul(qypz, Hacl_Impl_Ed25519_ExtPoint_gety(q1), Hacl_Impl_Ed25519_ExtPoint_getz(p)); Hacl_Bignum25519_reduce(qypz); bool b = Hacl_Impl_Ed25519_PointEqual_eq(pyqz, qypz); return b; } static bool Hacl_Impl_Ed25519_PointEqual_point_equal_(uint64_t *p, uint64_t *q1, uint64_t *tmp) { bool b = Hacl_Impl_Ed25519_PointEqual_point_equal_1(p, q1, tmp); if (b == true) return Hacl_Impl_Ed25519_PointEqual_point_equal_2(p, q1, tmp); else return false; } static bool Hacl_Impl_Ed25519_PointEqual_point_equal(uint64_t *p, uint64_t *q1) { uint64_t tmp[20U] = { 0U }; bool res = Hacl_Impl_Ed25519_PointEqual_point_equal_(p, q1, tmp); return res; } static void Hacl_Impl_Load56_load_64_bytes(uint64_t *out, uint8_t *b) { uint8_t *b80 = b; uint64_t z = load64_le(b80); uint64_t z_ = z & (uint64_t)0xffffffffffffffU; uint64_t b0 = z_; uint8_t *b81 = b + (uint32_t)7U; uint64_t z0 = load64_le(b81); uint64_t z_0 = z0 & (uint64_t)0xffffffffffffffU; uint64_t b1 = z_0; uint8_t *b82 = b + (uint32_t)14U; uint64_t z1 = load64_le(b82); uint64_t z_1 = z1 & (uint64_t)0xffffffffffffffU; uint64_t b2 = z_1; uint8_t *b83 = b + (uint32_t)21U; uint64_t z2 = load64_le(b83); uint64_t z_2 = z2 & (uint64_t)0xffffffffffffffU; uint64_t b3 = z_2; uint8_t *b84 = b + (uint32_t)28U; uint64_t z3 = load64_le(b84); uint64_t z_3 = z3 & (uint64_t)0xffffffffffffffU; uint64_t b4 = z_3; uint8_t *b85 = b + (uint32_t)35U; uint64_t z4 = load64_le(b85); uint64_t z_4 = z4 & (uint64_t)0xffffffffffffffU; uint64_t b5 = z_4; uint8_t *b86 = b + (uint32_t)42U; uint64_t z5 = load64_le(b86); uint64_t z_5 = z5 & (uint64_t)0xffffffffffffffU; uint64_t b6 = z_5; uint8_t *b87 = b + (uint32_t)49U; uint64_t z6 = load64_le(b87); uint64_t z_6 = z6 & (uint64_t)0xffffffffffffffU; uint64_t b7 = z_6; uint8_t *b8 = b + (uint32_t)56U; uint64_t z7 = load64_le(b8); uint64_t z_7 = z7 & (uint64_t)0xffffffffffffffU; uint64_t b88 = z_7; uint8_t b63 = b[63U]; uint64_t b9 = (uint64_t)b63; Hacl_Lib_Create64_make_h64_10(out, b0, b1, b2, b3, b4, b5, b6, b7, b88, b9); } static void Hacl_Impl_Load56_load_32_bytes(uint64_t *out, uint8_t *b) { uint8_t *b80 = b; uint64_t z = load64_le(b80); uint64_t z_ = z & (uint64_t)0xffffffffffffffU; uint64_t b0 = z_; uint8_t *b81 = b + (uint32_t)7U; uint64_t z0 = load64_le(b81); uint64_t z_0 = z0 & (uint64_t)0xffffffffffffffU; uint64_t b1 = z_0; uint8_t *b82 = b + (uint32_t)14U; uint64_t z1 = load64_le(b82); uint64_t z_1 = z1 & (uint64_t)0xffffffffffffffU; uint64_t b2 = z_1; uint8_t *b8 = b + (uint32_t)21U; uint64_t z2 = load64_le(b8); uint64_t z_2 = z2 & (uint64_t)0xffffffffffffffU; uint64_t b3 = z_2; uint8_t *x0 = b + (uint32_t)28U; uint32_t b4 = load32_le(x0); uint64_t b41 = (uint64_t)b4; Hacl_Lib_Create64_make_h64_5(out, b0, b1, b2, b3, b41); } inline static void Hacl_Impl_Ed25519_Pow2_252m2_pow2_252m2(uint64_t *out, uint64_t *z) { Hacl_Bignum_Crecip_crecip_(out, z); } static bool Hacl_Impl_Ed25519_RecoverX_is_0(uint64_t *x) { uint64_t x0 = x[0U]; uint64_t x1 = x[1U]; uint64_t x2 = x[2U]; uint64_t x3 = x[3U]; uint64_t x4 = x[4U]; return x0 == (uint64_t)0U && x1 == (uint64_t)0U && x2 == (uint64_t)0U && x3 == (uint64_t)0U && x4 == (uint64_t)0U; } static void Hacl_Impl_Ed25519_RecoverX_recover_x_step_5(uint64_t *x, uint64_t sign1, uint64_t *tmp) { uint64_t *x3 = tmp + (uint32_t)5U; uint64_t *t0 = tmp + (uint32_t)10U; uint64_t x0 = x3[0U]; uint64_t x00 = x0 & (uint64_t)1U; if (!(x00 == sign1)) { uint64_t zero1 = (uint64_t)0U; Hacl_Lib_Create64_make_h64_5(t0, zero1, zero1, zero1, zero1, zero1); Hacl_Bignum25519_fdifference(x3, t0); Hacl_Bignum25519_reduce_513(x3); Hacl_Bignum25519_reduce(x3); } memcpy(x, x3, (uint32_t)5U * sizeof x3[0U]); } static bool Hacl_Impl_Ed25519_RecoverX_recover_x_(uint64_t *x, uint64_t *y, uint64_t sign1, uint64_t *tmp) { uint64_t *x20 = tmp; uint64_t x0 = y[0U]; uint64_t x1 = y[1U]; uint64_t x2 = y[2U]; uint64_t x30 = y[3U]; uint64_t x4 = y[4U]; bool b = x0 >= (uint64_t)0x7ffffffffffedU && x1 == (uint64_t)0x7ffffffffffffU && x2 == (uint64_t)0x7ffffffffffffU && x30 == (uint64_t)0x7ffffffffffffU && x4 == (uint64_t)0x7ffffffffffffU; if (b) return false; else { uint64_t tmp0[25U] = { 0U }; uint64_t *one10 = tmp0; uint64_t *y2 = tmp0 + (uint32_t)5U; uint64_t *dyyi = tmp0 + (uint32_t)10U; uint64_t *dyy = tmp0 + (uint32_t)15U; uint64_t zero10 = (uint64_t)0U; uint64_t one1 = (uint64_t)1U; Hacl_Lib_Create64_make_h64_5(one10, one1, zero10, zero10, zero10, zero10); Hacl_Bignum25519_fsquare(y2, y); Hacl_Bignum25519_times_d(dyy, y2); Hacl_Bignum25519_fsum(dyy, one10); Hacl_Bignum25519_reduce_513(dyy); Hacl_Bignum25519_inverse(dyyi, dyy); Hacl_Bignum25519_fdifference(one10, y2); Hacl_Bignum25519_fmul(x20, dyyi, one10); Hacl_Bignum25519_reduce(x20); bool x2_is_0 = Hacl_Impl_Ed25519_RecoverX_is_0(x20); uint8_t z; if (x2_is_0) { uint8_t ite; if (sign1 == (uint64_t)0U) { uint64_t zero1 = (uint64_t)0U; Hacl_Lib_Create64_make_h64_5(x, zero1, zero1, zero1, zero1, zero1); ite = (uint8_t)1U; } else ite = (uint8_t)0U; z = ite; } else z = (uint8_t)2U; if (z == (uint8_t)0U) return false; else if (z == (uint8_t)1U) return true; else { uint64_t *x2 = tmp; uint64_t *x30 = tmp + (uint32_t)5U; uint64_t *t00 = tmp + (uint32_t)10U; uint64_t *t10 = tmp + (uint32_t)15U; Hacl_Impl_Ed25519_Pow2_252m2_pow2_252m2(x30, x2); Hacl_Bignum25519_fsquare(t00, x30); memcpy(t10, x2, (uint32_t)5U * sizeof x2[0U]); Hacl_Bignum25519_fdifference(t10, t00); Hacl_Bignum25519_reduce_513(t10); Hacl_Bignum25519_reduce(t10); bool t1_is_0 = Hacl_Impl_Ed25519_RecoverX_is_0(t10); if (!t1_is_0) { uint64_t sqrt_m1[5U] = { 0U }; Hacl_Lib_Create64_make_h64_5(sqrt_m1, (uint64_t)0x00061b274a0ea0b0U, (uint64_t)0x0000d5a5fc8f189dU, (uint64_t)0x0007ef5e9cbd0c60U, (uint64_t)0x00078595a6804c9eU, (uint64_t)0x0002b8324804fc1dU); Hacl_Bignum25519_fmul(x30, x30, sqrt_m1); } Hacl_Bignum25519_reduce(x30); uint64_t *x20 = tmp; uint64_t *x3 = tmp + (uint32_t)5U; uint64_t *t0 = tmp + (uint32_t)10U; uint64_t *t1 = tmp + (uint32_t)15U; Hacl_Bignum25519_fsquare(t0, x3); memcpy(t1, x20, (uint32_t)5U * sizeof x20[0U]); Hacl_Bignum25519_fdifference(t1, t0); Hacl_Bignum25519_reduce_513(t1); Hacl_Bignum25519_reduce(t1); bool z1 = Hacl_Impl_Ed25519_RecoverX_is_0(t1); if (z1 == false) return false; else { Hacl_Impl_Ed25519_RecoverX_recover_x_step_5(x, sign1, tmp); return true; } } } } static bool Hacl_Impl_Ed25519_RecoverX_recover_x(uint64_t *x, uint64_t *y, uint64_t sign1) { uint64_t tmp[20U] = { 0U }; bool res = Hacl_Impl_Ed25519_RecoverX_recover_x_(x, y, sign1, tmp); return res; } static void Hacl_Impl_Load51_load_51(uint64_t *output, uint8_t *input) { Hacl_EC_Format_fexpand(output, input); } static bool Hacl_Impl_Ed25519_PointDecompress_point_decompress(uint64_t *out, uint8_t *s) { uint64_t tmp[10U] = { 0U }; uint64_t *y0 = tmp; uint64_t *x0 = tmp + (uint32_t)5U; uint64_t *y = tmp; uint64_t *x = tmp + (uint32_t)5U; uint8_t s31 = s[31U]; uint64_t sign1 = (uint64_t)(s31 >> (uint32_t)7U); Hacl_Impl_Load51_load_51(y, s); bool z = Hacl_Impl_Ed25519_RecoverX_recover_x(x, y, sign1); bool z0 = z; bool res; if (z0 == false) res = false; else { uint64_t *outx = Hacl_Impl_Ed25519_ExtPoint_getx(out); uint64_t *outy = Hacl_Impl_Ed25519_ExtPoint_gety(out); uint64_t *outz = Hacl_Impl_Ed25519_ExtPoint_getz(out); uint64_t *outt = Hacl_Impl_Ed25519_ExtPoint_gett(out); memcpy(outx, x0, (uint32_t)5U * sizeof x0[0U]); memcpy(outy, y0, (uint32_t)5U * sizeof y0[0U]); uint64_t zero1 = (uint64_t)0U; uint64_t one1 = (uint64_t)1U; Hacl_Lib_Create64_make_h64_5(outz, one1, zero1, zero1, zero1, zero1); Hacl_Bignum25519_fmul(outt, x0, y0); res = true; } return res; } static void Hacl_Impl_Store56_store_56(uint8_t *out, uint64_t *b) { uint64_t b0 = b[0U]; uint64_t b1 = b[1U]; uint64_t b2 = b[2U]; uint64_t b3 = b[3U]; uint64_t b4 = b[4U]; uint32_t b41 = (uint32_t)b4; uint8_t *b8 = out; store64_le(b8, b0); uint8_t *b80 = out + (uint32_t)7U; store64_le(b80, b1); uint8_t *b81 = out + (uint32_t)14U; store64_le(b81, b2); uint8_t *b82 = out + (uint32_t)21U; store64_le(b82, b3); uint8_t *x0 = out + (uint32_t)28U; store32_le(x0, b41); } static void Hacl_Impl_SHA512_Ed25519_2_hash_block_and_rest( uint8_t *out, uint8_t *block, uint8_t *msg, uint32_t len1 ) { uint32_t nblocks = len1 >> (uint32_t)7U; uint64_t rest = (uint64_t)(len1 & (uint32_t)127U); uint64_t st[169U] = { 0U }; Hacl_Impl_SHA2_512_init(st); Hacl_Impl_SHA2_512_update(st, block); Hacl_Impl_SHA2_512_update_multi(st, msg, nblocks); Hacl_Impl_SHA2_512_update_last(st, msg + (uint32_t)128U * nblocks, rest); Hacl_Impl_SHA2_512_finish(st, out); } static void Hacl_Impl_SHA512_Ed25519_1_copy_bytes(uint8_t *output, uint8_t *input, uint32_t len1) { memcpy(output, input, len1 * sizeof input[0U]); } static void Hacl_Impl_SHA512_Ed25519_1_concat_2(uint8_t *out, uint8_t *pre, uint8_t *msg, uint32_t len1) { Hacl_Impl_SHA512_Ed25519_1_copy_bytes(out, pre, (uint32_t)32U); Hacl_Impl_SHA512_Ed25519_1_copy_bytes(out + (uint32_t)32U, msg, len1); } static void Hacl_Impl_SHA512_Ed25519_1_concat_3( uint8_t *out, uint8_t *pre, uint8_t *pre2, uint8_t *msg, uint32_t len1 ) { Hacl_Impl_SHA512_Ed25519_1_copy_bytes(out, pre, (uint32_t)32U); Hacl_Impl_SHA512_Ed25519_1_copy_bytes(out + (uint32_t)32U, pre2, (uint32_t)32U); Hacl_Impl_SHA512_Ed25519_1_copy_bytes(out + (uint32_t)64U, msg, len1); } static void Hacl_Impl_SHA512_Ed25519_1_sha512_pre_msg_1( uint8_t *h, uint8_t *prefix, uint8_t *input, uint32_t len1 ) { uint8_t block[128U] = { 0U }; uint8_t *block_ = block; Hacl_Impl_SHA512_Ed25519_1_concat_2(block_, prefix, input, len1); Hacl_Impl_SHA2_512_hash(h, block_, len1 + (uint32_t)32U); } static void Hacl_Impl_SHA512_Ed25519_1_sha512_pre_pre2_msg_1( uint8_t *h, uint8_t *prefix, uint8_t *prefix2, uint8_t *input, uint32_t len1 ) { uint8_t block[128U] = { 0U }; uint8_t *block_ = block; Hacl_Impl_SHA512_Ed25519_1_concat_3(block_, prefix, prefix2, input, len1); Hacl_Impl_SHA2_512_hash(h, block_, len1 + (uint32_t)64U); } static void Hacl_Impl_SHA512_Ed25519_3_sha512_pre_msg_2( uint8_t *h, uint8_t *prefix, uint8_t *input, uint32_t len1 ) { uint8_t *input11 = input; uint8_t *input21 = input + (uint32_t)96U; uint8_t block[128U] = { 0U }; Hacl_Impl_SHA512_Ed25519_1_concat_2(block, prefix, input11, (uint32_t)96U); Hacl_Impl_SHA512_Ed25519_2_hash_block_and_rest(h, block, input21, len1 - (uint32_t)96U); } static void Hacl_Impl_SHA512_Ed25519_3_sha512_pre_msg( uint8_t *h, uint8_t *prefix, uint8_t *input, uint32_t len1 ) { if (len1 <= (uint32_t)96U) Hacl_Impl_SHA512_Ed25519_1_sha512_pre_msg_1(h, prefix, input, len1); else Hacl_Impl_SHA512_Ed25519_3_sha512_pre_msg_2(h, prefix, input, len1); } static void Hacl_Impl_SHA512_Ed25519_3_sha512_pre_pre2_msg_2( uint8_t *h, uint8_t *prefix, uint8_t *prefix2, uint8_t *input, uint32_t len1 ) { uint8_t *input11 = input; uint8_t *input21 = input + (uint32_t)64U; uint8_t block[128U] = { 0U }; Hacl_Impl_SHA512_Ed25519_1_concat_3(block, prefix, prefix2, input11, (uint32_t)64U); Hacl_Impl_SHA512_Ed25519_2_hash_block_and_rest(h, block, input21, len1 - (uint32_t)64U); } static void Hacl_Impl_SHA512_Ed25519_3_sha512_pre_pre2_msg( uint8_t *h, uint8_t *prefix, uint8_t *prefix2, uint8_t *input, uint32_t len1 ) { if (len1 <= (uint32_t)64U) Hacl_Impl_SHA512_Ed25519_1_sha512_pre_pre2_msg_1(h, prefix, prefix2, input, len1); else Hacl_Impl_SHA512_Ed25519_3_sha512_pre_pre2_msg_2(h, prefix, prefix2, input, len1); } static void Hacl_Impl_SHA512_Ed25519_sha512_pre_msg( uint8_t *h, uint8_t *prefix, uint8_t *input, uint32_t len1 ) { Hacl_Impl_SHA512_Ed25519_3_sha512_pre_msg(h, prefix, input, len1); } static void Hacl_Impl_SHA512_Ed25519_sha512_pre_pre2_msg( uint8_t *h, uint8_t *prefix, uint8_t *prefix2, uint8_t *input, uint32_t len1 ) { Hacl_Impl_SHA512_Ed25519_3_sha512_pre_pre2_msg(h, prefix, prefix2, input, len1); } static void Hacl_Impl_Sha512_sha512_pre_msg(uint8_t *h, uint8_t *prefix, uint8_t *input, uint32_t len1) { Hacl_Impl_SHA512_Ed25519_sha512_pre_msg(h, prefix, input, len1); } static void Hacl_Impl_Sha512_sha512_pre_pre2_msg( uint8_t *h, uint8_t *prefix, uint8_t *prefix2, uint8_t *input, uint32_t len1 ) { Hacl_Impl_SHA512_Ed25519_sha512_pre_pre2_msg(h, prefix, prefix2, input, len1); } static void Hacl_Lib_Create128_make_h128_9( FStar_UInt128_t *b, FStar_UInt128_t s0, FStar_UInt128_t s1, FStar_UInt128_t s2, FStar_UInt128_t s3, FStar_UInt128_t s4, FStar_UInt128_t s5, FStar_UInt128_t s6, FStar_UInt128_t s7, FStar_UInt128_t s8 ) { b[0U] = s0; b[1U] = s1; b[2U] = s2; b[3U] = s3; b[4U] = s4; b[5U] = s5; b[6U] = s6; b[7U] = s7; b[8U] = s8; } static void Hacl_Impl_BignumQ_Mul_make_m(uint64_t *m1) { Hacl_Lib_Create64_make_h64_5(m1, (uint64_t)0x12631a5cf5d3edU, (uint64_t)0xf9dea2f79cd658U, (uint64_t)0x000000000014deU, (uint64_t)0x00000000000000U, (uint64_t)0x00000010000000U); } static void Hacl_Impl_BignumQ_Mul_make_mu(uint64_t *m1) { Hacl_Lib_Create64_make_h64_5(m1, (uint64_t)0x9ce5a30a2c131bU, (uint64_t)0x215d086329a7edU, (uint64_t)0xffffffffeb2106U, (uint64_t)0xffffffffffffffU, (uint64_t)0x00000fffffffffU); } static void Hacl_Impl_BignumQ_Mul_choose(uint64_t *z, uint64_t *x, uint64_t *y, uint64_t b) { uint64_t mask = b - (uint64_t)1U; uint64_t x0 = x[0U]; uint64_t x1 = x[1U]; uint64_t x2 = x[2U]; uint64_t x3 = x[3U]; uint64_t x4 = x[4U]; uint64_t y0 = y[0U]; uint64_t y1 = y[1U]; uint64_t y2 = y[2U]; uint64_t y3 = y[3U]; uint64_t y4 = y[4U]; uint64_t z0 = ((y0 ^ x0) & mask) ^ x0; uint64_t z1 = ((y1 ^ x1) & mask) ^ x1; uint64_t z2 = ((y2 ^ x2) & mask) ^ x2; uint64_t z3 = ((y3 ^ x3) & mask) ^ x3; uint64_t z4 = ((y4 ^ x4) & mask) ^ x4; Hacl_Lib_Create64_make_h64_5(z, z0, z1, z2, z3, z4); } static uint64_t Hacl_Impl_BignumQ_Mul_lt(uint64_t a, uint64_t b) { return (a - b) >> (uint32_t)63U; } static uint64_t Hacl_Impl_BignumQ_Mul_shiftl_56(uint64_t b) { return b << (uint32_t)56U; } static void Hacl_Impl_BignumQ_Mul_sub_mod_264(uint64_t *z, uint64_t *x, uint64_t *y) { uint64_t x0 = x[0U]; uint64_t x1 = x[1U]; uint64_t x2 = x[2U]; uint64_t x3 = x[3U]; uint64_t x4 = x[4U]; uint64_t y0 = y[0U]; uint64_t y1 = y[1U]; uint64_t y2 = y[2U]; uint64_t y3 = y[3U]; uint64_t y4 = y[4U]; uint64_t b = Hacl_Impl_BignumQ_Mul_lt(x0, y0); uint64_t t0 = Hacl_Impl_BignumQ_Mul_shiftl_56(b) + x0 - y0; uint64_t y11 = y1 + b; uint64_t b1 = Hacl_Impl_BignumQ_Mul_lt(x1, y11); uint64_t t1 = Hacl_Impl_BignumQ_Mul_shiftl_56(b1) + x1 - y11; uint64_t y21 = y2 + b1; uint64_t b2 = Hacl_Impl_BignumQ_Mul_lt(x2, y21); uint64_t t2 = Hacl_Impl_BignumQ_Mul_shiftl_56(b2) + x2 - y21; uint64_t y31 = y3 + b2; uint64_t b3 = Hacl_Impl_BignumQ_Mul_lt(x3, y31); uint64_t t3 = Hacl_Impl_BignumQ_Mul_shiftl_56(b3) + x3 - y31; uint64_t y41 = y4 + b3; uint64_t b4 = Hacl_Impl_BignumQ_Mul_lt(x4, y41); uint64_t t4 = (b4 << (uint32_t)40U) + x4 - y41; Hacl_Lib_Create64_make_h64_5(z, t0, t1, t2, t3, t4); } static void Hacl_Impl_BignumQ_Mul_subm_conditional(uint64_t *z, uint64_t *x) { uint64_t tmp[5U] = { 0U }; uint64_t x0 = x[0U]; uint64_t x1 = x[1U]; uint64_t x2 = x[2U]; uint64_t x3 = x[3U]; uint64_t x4 = x[4U]; Hacl_Lib_Create64_make_h64_5(tmp, x0, x1, x2, x3, x4); uint64_t y0 = (uint64_t)0x12631a5cf5d3edU; uint64_t y1 = (uint64_t)0xf9dea2f79cd658U; uint64_t y2 = (uint64_t)0x000000000014deU; uint64_t y3 = (uint64_t)0x00000000000000U; uint64_t y4 = (uint64_t)0x00000010000000U; uint64_t b = Hacl_Impl_BignumQ_Mul_lt(x0, y0); uint64_t t0 = Hacl_Impl_BignumQ_Mul_shiftl_56(b) + x0 - y0; uint64_t y11 = y1 + b; uint64_t b1 = Hacl_Impl_BignumQ_Mul_lt(x1, y11); uint64_t t1 = Hacl_Impl_BignumQ_Mul_shiftl_56(b1) + x1 - y11; uint64_t y21 = y2 + b1; uint64_t b2 = Hacl_Impl_BignumQ_Mul_lt(x2, y21); uint64_t t2 = Hacl_Impl_BignumQ_Mul_shiftl_56(b2) + x2 - y21; uint64_t y31 = y3 + b2; uint64_t b3 = Hacl_Impl_BignumQ_Mul_lt(x3, y31); uint64_t t3 = Hacl_Impl_BignumQ_Mul_shiftl_56(b3) + x3 - y31; uint64_t y41 = y4 + b3; uint64_t b4 = Hacl_Impl_BignumQ_Mul_lt(x4, y41); uint64_t t4 = Hacl_Impl_BignumQ_Mul_shiftl_56(b4) + x4 - y41; Hacl_Lib_Create64_make_h64_5(z, t0, t1, t2, t3, t4); Hacl_Impl_BignumQ_Mul_choose(z, tmp, z, b4); } static void Hacl_Impl_BignumQ_Mul_low_mul_5(uint64_t *z, uint64_t *x, uint64_t *y) { uint64_t x0 = x[0U]; uint64_t x1 = x[1U]; uint64_t x2 = x[2U]; uint64_t x3 = x[3U]; uint64_t x4 = x[4U]; uint64_t y0 = y[0U]; uint64_t y1 = y[1U]; uint64_t y2 = y[2U]; uint64_t y3 = y[3U]; uint64_t y4 = y[4U]; FStar_UInt128_t xy00 = FStar_UInt128_mul_wide(x0, y0); FStar_UInt128_t xy01 = FStar_UInt128_mul_wide(x0, y1); FStar_UInt128_t xy02 = FStar_UInt128_mul_wide(x0, y2); FStar_UInt128_t xy03 = FStar_UInt128_mul_wide(x0, y3); FStar_UInt128_t xy04 = FStar_UInt128_mul_wide(x0, y4); FStar_UInt128_t xy10 = FStar_UInt128_mul_wide(x1, y0); FStar_UInt128_t xy11 = FStar_UInt128_mul_wide(x1, y1); FStar_UInt128_t xy12 = FStar_UInt128_mul_wide(x1, y2); FStar_UInt128_t xy13 = FStar_UInt128_mul_wide(x1, y3); FStar_UInt128_t xy20 = FStar_UInt128_mul_wide(x2, y0); FStar_UInt128_t xy21 = FStar_UInt128_mul_wide(x2, y1); FStar_UInt128_t xy22 = FStar_UInt128_mul_wide(x2, y2); FStar_UInt128_t xy30 = FStar_UInt128_mul_wide(x3, y0); FStar_UInt128_t xy31 = FStar_UInt128_mul_wide(x3, y1); FStar_UInt128_t xy40 = FStar_UInt128_mul_wide(x4, y0); FStar_UInt128_t x5 = xy00; FStar_UInt128_t carry1 = FStar_UInt128_shift_right(x5, (uint32_t)56U); uint64_t t = FStar_UInt128_uint128_to_uint64(x5) & (uint64_t)0xffffffffffffffU; uint64_t t0 = t; FStar_UInt128_t x6 = FStar_UInt128_add(FStar_UInt128_add(xy01, xy10), carry1); FStar_UInt128_t carry2 = FStar_UInt128_shift_right(x6, (uint32_t)56U); uint64_t t1 = FStar_UInt128_uint128_to_uint64(x6) & (uint64_t)0xffffffffffffffU; uint64_t t11 = t1; FStar_UInt128_t x7 = FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_add(xy02, xy11), xy20), carry2); FStar_UInt128_t carry3 = FStar_UInt128_shift_right(x7, (uint32_t)56U); uint64_t t2 = FStar_UInt128_uint128_to_uint64(x7) & (uint64_t)0xffffffffffffffU; uint64_t t21 = t2; FStar_UInt128_t x8 = FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_add(xy03, xy12), xy21), xy30), carry3); FStar_UInt128_t carry4 = FStar_UInt128_shift_right(x8, (uint32_t)56U); uint64_t t3 = FStar_UInt128_uint128_to_uint64(x8) & (uint64_t)0xffffffffffffffU; uint64_t t31 = t3; uint64_t t4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_add(xy04, xy13), xy22), xy31), xy40), carry4)) & (uint64_t)0xffffffffffU; Hacl_Lib_Create64_make_h64_5(z, t0, t11, t21, t31, t4); } static void Hacl_Impl_BignumQ_Mul_mul_5(FStar_UInt128_t *z, uint64_t *x, uint64_t *y) { uint64_t x0 = x[0U]; uint64_t x1 = x[1U]; uint64_t x2 = x[2U]; uint64_t x3 = x[3U]; uint64_t x4 = x[4U]; uint64_t y0 = y[0U]; uint64_t y1 = y[1U]; uint64_t y2 = y[2U]; uint64_t y3 = y[3U]; uint64_t y4 = y[4U]; FStar_UInt128_t xy00 = FStar_UInt128_mul_wide(x0, y0); FStar_UInt128_t xy01 = FStar_UInt128_mul_wide(x0, y1); FStar_UInt128_t xy02 = FStar_UInt128_mul_wide(x0, y2); FStar_UInt128_t xy03 = FStar_UInt128_mul_wide(x0, y3); FStar_UInt128_t xy04 = FStar_UInt128_mul_wide(x0, y4); FStar_UInt128_t xy10 = FStar_UInt128_mul_wide(x1, y0); FStar_UInt128_t xy11 = FStar_UInt128_mul_wide(x1, y1); FStar_UInt128_t xy12 = FStar_UInt128_mul_wide(x1, y2); FStar_UInt128_t xy13 = FStar_UInt128_mul_wide(x1, y3); FStar_UInt128_t xy14 = FStar_UInt128_mul_wide(x1, y4); FStar_UInt128_t xy20 = FStar_UInt128_mul_wide(x2, y0); FStar_UInt128_t xy21 = FStar_UInt128_mul_wide(x2, y1); FStar_UInt128_t xy22 = FStar_UInt128_mul_wide(x2, y2); FStar_UInt128_t xy23 = FStar_UInt128_mul_wide(x2, y3); FStar_UInt128_t xy24 = FStar_UInt128_mul_wide(x2, y4); FStar_UInt128_t xy30 = FStar_UInt128_mul_wide(x3, y0); FStar_UInt128_t xy31 = FStar_UInt128_mul_wide(x3, y1); FStar_UInt128_t xy32 = FStar_UInt128_mul_wide(x3, y2); FStar_UInt128_t xy33 = FStar_UInt128_mul_wide(x3, y3); FStar_UInt128_t xy34 = FStar_UInt128_mul_wide(x3, y4); FStar_UInt128_t xy40 = FStar_UInt128_mul_wide(x4, y0); FStar_UInt128_t xy41 = FStar_UInt128_mul_wide(x4, y1); FStar_UInt128_t xy42 = FStar_UInt128_mul_wide(x4, y2); FStar_UInt128_t xy43 = FStar_UInt128_mul_wide(x4, y3); FStar_UInt128_t xy44 = FStar_UInt128_mul_wide(x4, y4); FStar_UInt128_t z0 = xy00; FStar_UInt128_t z1 = FStar_UInt128_add(xy01, xy10); FStar_UInt128_t z2 = FStar_UInt128_add(FStar_UInt128_add(xy02, xy11), xy20); FStar_UInt128_t z3 = FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_add(xy03, xy12), xy21), xy30); FStar_UInt128_t z4 = FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_add(xy04, xy13), xy22), xy31), xy40); FStar_UInt128_t z5 = FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_add(xy14, xy23), xy32), xy41); FStar_UInt128_t z6 = FStar_UInt128_add(FStar_UInt128_add(xy24, xy33), xy42); FStar_UInt128_t z7 = FStar_UInt128_add(xy34, xy43); FStar_UInt128_t z8 = xy44; Hacl_Lib_Create128_make_h128_9(z, z0, z1, z2, z3, z4, z5, z6, z7, z8); } static void Hacl_Impl_BignumQ_Mul_carry(uint64_t *out, FStar_UInt128_t *z) { FStar_UInt128_t z0 = z[0U]; FStar_UInt128_t z1 = z[1U]; FStar_UInt128_t z2 = z[2U]; FStar_UInt128_t z3 = z[3U]; FStar_UInt128_t z4 = z[4U]; FStar_UInt128_t z5 = z[5U]; FStar_UInt128_t z6 = z[6U]; FStar_UInt128_t z7 = z[7U]; FStar_UInt128_t z8 = z[8U]; FStar_UInt128_t x = z0; FStar_UInt128_t y = z1; FStar_UInt128_t carry1 = FStar_UInt128_shift_right(x, (uint32_t)56U); uint64_t t = FStar_UInt128_uint128_to_uint64(x) & (uint64_t)0xffffffffffffffU; uint64_t x0 = t; FStar_UInt128_t z1_ = FStar_UInt128_add(y, carry1); FStar_UInt128_t x1 = z1_; FStar_UInt128_t y1 = z2; FStar_UInt128_t carry2 = FStar_UInt128_shift_right(x1, (uint32_t)56U); uint64_t t1 = FStar_UInt128_uint128_to_uint64(x1) & (uint64_t)0xffffffffffffffU; uint64_t x11 = t1; FStar_UInt128_t z2_ = FStar_UInt128_add(y1, carry2); FStar_UInt128_t x2 = z2_; FStar_UInt128_t y2 = z3; FStar_UInt128_t carry3 = FStar_UInt128_shift_right(x2, (uint32_t)56U); uint64_t t2 = FStar_UInt128_uint128_to_uint64(x2) & (uint64_t)0xffffffffffffffU; uint64_t x21 = t2; FStar_UInt128_t z3_ = FStar_UInt128_add(y2, carry3); FStar_UInt128_t x3 = z3_; FStar_UInt128_t y3 = z4; FStar_UInt128_t carry4 = FStar_UInt128_shift_right(x3, (uint32_t)56U); uint64_t t3 = FStar_UInt128_uint128_to_uint64(x3) & (uint64_t)0xffffffffffffffU; uint64_t x31 = t3; FStar_UInt128_t z4_ = FStar_UInt128_add(y3, carry4); FStar_UInt128_t x4 = z4_; FStar_UInt128_t y4 = z5; FStar_UInt128_t carry5 = FStar_UInt128_shift_right(x4, (uint32_t)56U); uint64_t t4 = FStar_UInt128_uint128_to_uint64(x4) & (uint64_t)0xffffffffffffffU; uint64_t x41 = t4; FStar_UInt128_t z5_ = FStar_UInt128_add(y4, carry5); FStar_UInt128_t x5 = z5_; FStar_UInt128_t y5 = z6; FStar_UInt128_t carry6 = FStar_UInt128_shift_right(x5, (uint32_t)56U); uint64_t t5 = FStar_UInt128_uint128_to_uint64(x5) & (uint64_t)0xffffffffffffffU; uint64_t x51 = t5; FStar_UInt128_t z6_ = FStar_UInt128_add(y5, carry6); FStar_UInt128_t x6 = z6_; FStar_UInt128_t y6 = z7; FStar_UInt128_t carry7 = FStar_UInt128_shift_right(x6, (uint32_t)56U); uint64_t t6 = FStar_UInt128_uint128_to_uint64(x6) & (uint64_t)0xffffffffffffffU; uint64_t x61 = t6; FStar_UInt128_t z7_ = FStar_UInt128_add(y6, carry7); FStar_UInt128_t x7 = z7_; FStar_UInt128_t y7 = z8; FStar_UInt128_t carry8 = FStar_UInt128_shift_right(x7, (uint32_t)56U); uint64_t t7 = FStar_UInt128_uint128_to_uint64(x7) & (uint64_t)0xffffffffffffffU; uint64_t x71 = t7; FStar_UInt128_t z8_ = FStar_UInt128_add(y7, carry8); FStar_UInt128_t x8 = z8_; FStar_UInt128_t y8 = FStar_UInt128_uint64_to_uint128((uint64_t)0U); FStar_UInt128_t carry9 = FStar_UInt128_shift_right(x8, (uint32_t)56U); uint64_t t8 = FStar_UInt128_uint128_to_uint64(x8) & (uint64_t)0xffffffffffffffU; uint64_t x81 = t8; FStar_UInt128_t z9_ = FStar_UInt128_add(y8, carry9); uint64_t x9 = FStar_UInt128_uint128_to_uint64(z9_); Hacl_Lib_Create64_make_h64_10(out, x0, x11, x21, x31, x41, x51, x61, x71, x81, x9); } static void Hacl_Impl_BignumQ_Mul_mod_264(uint64_t *r, uint64_t *t) { uint64_t x0 = t[0U]; uint64_t x1 = t[1U]; uint64_t x2 = t[2U]; uint64_t x3 = t[3U]; uint64_t x4 = t[4U]; uint64_t x4_ = x4 & (uint64_t)0xffffffffffU; Hacl_Lib_Create64_make_h64_5(r, x0, x1, x2, x3, x4_); } static void Hacl_Impl_BignumQ_Mul_div_248(uint64_t *out, uint64_t *t) { uint64_t x4 = t[4U]; uint64_t x5 = t[5U]; uint64_t x6 = t[6U]; uint64_t x7 = t[7U]; uint64_t x8 = t[8U]; uint64_t x9 = t[9U]; uint64_t z0 = (x5 & (uint64_t)0xffffffU) << (uint32_t)32U | x4 >> (uint32_t)24U; uint64_t z1 = (x6 & (uint64_t)0xffffffU) << (uint32_t)32U | x5 >> (uint32_t)24U; uint64_t z2 = (x7 & (uint64_t)0xffffffU) << (uint32_t)32U | x6 >> (uint32_t)24U; uint64_t z3 = (x8 & (uint64_t)0xffffffU) << (uint32_t)32U | x7 >> (uint32_t)24U; uint64_t z4 = (x9 & (uint64_t)0xffffffU) << (uint32_t)32U | x8 >> (uint32_t)24U; Hacl_Lib_Create64_make_h64_5(out, z0, z1, z2, z3, z4); } static void Hacl_Impl_BignumQ_Mul_div_264(uint64_t *out, uint64_t *t) { uint64_t x4 = t[4U]; uint64_t x5 = t[5U]; uint64_t x6 = t[6U]; uint64_t x7 = t[7U]; uint64_t x8 = t[8U]; uint64_t x9 = t[9U]; uint64_t z0 = (x5 & (uint64_t)0xffffffffffU) << (uint32_t)16U | x4 >> (uint32_t)40U; uint64_t z1 = (x6 & (uint64_t)0xffffffffffU) << (uint32_t)16U | x5 >> (uint32_t)40U; uint64_t z2 = (x7 & (uint64_t)0xffffffffffU) << (uint32_t)16U | x6 >> (uint32_t)40U; uint64_t z3 = (x8 & (uint64_t)0xffffffffffU) << (uint32_t)16U | x7 >> (uint32_t)40U; uint64_t z4 = (x9 & (uint64_t)0xffffffffffU) << (uint32_t)16U | x8 >> (uint32_t)40U; Hacl_Lib_Create64_make_h64_5(out, z0, z1, z2, z3, z4); } static void Hacl_Impl_BignumQ_Mul_barrett_reduction__1( FStar_UInt128_t *qmu, uint64_t *t, uint64_t *mu1, uint64_t *tmp ) { uint64_t *q1 = tmp; uint64_t *qmu_ = tmp + (uint32_t)10U; uint64_t *qmu_264 = tmp + (uint32_t)20U; Hacl_Impl_BignumQ_Mul_div_248(q1, t); Hacl_Impl_BignumQ_Mul_mul_5(qmu, q1, mu1); Hacl_Impl_BignumQ_Mul_carry(qmu_, qmu); Hacl_Impl_BignumQ_Mul_div_264(qmu_264, qmu_); } static void Hacl_Impl_BignumQ_Mul_barrett_reduction__2(uint64_t *t, uint64_t *m1, uint64_t *tmp) { uint64_t *qmul = tmp; uint64_t *r = tmp + (uint32_t)5U; uint64_t *qmu_264 = tmp + (uint32_t)20U; uint64_t *s = tmp + (uint32_t)25U; Hacl_Impl_BignumQ_Mul_mod_264(r, t); Hacl_Impl_BignumQ_Mul_low_mul_5(qmul, qmu_264, m1); Hacl_Impl_BignumQ_Mul_sub_mod_264(s, r, qmul); } static void Hacl_Impl_BignumQ_Mul_barrett_reduction__( uint64_t *z, uint64_t *t, uint64_t *m1, uint64_t *mu1, uint64_t *tmp ) { uint64_t *s = tmp + (uint32_t)25U; KRML_CHECK_SIZE(FStar_UInt128_uint64_to_uint128((uint64_t)0U), (uint32_t)9U); FStar_UInt128_t qmu[9U]; for (uint32_t _i = 0U; _i < (uint32_t)9U; ++_i) qmu[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U); Hacl_Impl_BignumQ_Mul_barrett_reduction__1(qmu, t, mu1, tmp); Hacl_Impl_BignumQ_Mul_barrett_reduction__2(t, m1, tmp); Hacl_Impl_BignumQ_Mul_subm_conditional(z, s); } static void Hacl_Impl_BignumQ_Mul_barrett_reduction_(uint64_t *z, uint64_t *t) { uint64_t tmp[40U] = { 0U }; uint64_t *m1 = tmp; uint64_t *mu1 = tmp + (uint32_t)5U; uint64_t *tmp1 = tmp + (uint32_t)10U; Hacl_Impl_BignumQ_Mul_make_m(m1); Hacl_Impl_BignumQ_Mul_make_mu(mu1); Hacl_Impl_BignumQ_Mul_barrett_reduction__(z, t, m1, mu1, tmp1); } static void Hacl_Impl_BignumQ_Mul_barrett_reduction(uint64_t *z, uint64_t *t) { Hacl_Impl_BignumQ_Mul_barrett_reduction_(z, t); } static void Hacl_Impl_BignumQ_Mul_mul_modq(uint64_t *out, uint64_t *x, uint64_t *y) { uint64_t z_[10U] = { 0U }; KRML_CHECK_SIZE(FStar_UInt128_uint64_to_uint128((uint64_t)0U), (uint32_t)9U); FStar_UInt128_t z[9U]; for (uint32_t _i = 0U; _i < (uint32_t)9U; ++_i) z[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U); Hacl_Impl_BignumQ_Mul_mul_5(z, x, y); Hacl_Impl_BignumQ_Mul_carry(z_, z); Hacl_Impl_BignumQ_Mul_barrett_reduction_(out, z_); } static void Hacl_Impl_BignumQ_Mul_add_modq_(uint64_t *out, uint64_t *x, uint64_t *y) { uint64_t tmp[5U] = { 0U }; uint64_t x0 = x[0U]; uint64_t x1 = x[1U]; uint64_t x2 = x[2U]; uint64_t x3 = x[3U]; uint64_t x4 = x[4U]; uint64_t y0 = y[0U]; uint64_t y1 = y[1U]; uint64_t y2 = y[2U]; uint64_t y3 = y[3U]; uint64_t y4 = y[4U]; uint64_t z0 = x0 + y0; uint64_t z1 = x1 + y1; uint64_t z2 = x2 + y2; uint64_t z3 = x3 + y3; uint64_t z4 = x4 + y4; uint64_t x5 = z0; uint64_t y5 = z1; uint64_t carry1 = x5 >> (uint32_t)56U; uint64_t t = x5 & (uint64_t)0xffffffffffffffU; uint64_t x01 = t; uint64_t z1_ = y5 + carry1; uint64_t x6 = z1_; uint64_t y6 = z2; uint64_t carry2 = x6 >> (uint32_t)56U; uint64_t t1 = x6 & (uint64_t)0xffffffffffffffU; uint64_t x11 = t1; uint64_t z2_ = y6 + carry2; uint64_t x7 = z2_; uint64_t y7 = z3; uint64_t carry3 = x7 >> (uint32_t)56U; uint64_t t2 = x7 & (uint64_t)0xffffffffffffffU; uint64_t x21 = t2; uint64_t z3_ = y7 + carry3; uint64_t x8 = z3_; uint64_t y8 = z4; uint64_t carry4 = x8 >> (uint32_t)56U; uint64_t t3 = x8 & (uint64_t)0xffffffffffffffU; uint64_t x31 = t3; uint64_t x41 = y8 + carry4; Hacl_Lib_Create64_make_h64_5(tmp, x01, x11, x21, x31, x41); Hacl_Impl_BignumQ_Mul_subm_conditional(out, tmp); } static void Hacl_Impl_BignumQ_Mul_add_modq(uint64_t *out, uint64_t *x, uint64_t *y) { Hacl_Impl_BignumQ_Mul_add_modq_(out, x, y); } static void Hacl_Impl_SHA512_ModQ_sha512_modq_pre_( uint64_t *out, uint8_t *prefix, uint8_t *input, uint32_t len1, uint64_t *tmp ) { uint8_t hash1[64U] = { 0U }; Hacl_Impl_Sha512_sha512_pre_msg(hash1, prefix, input, len1); Hacl_Impl_Load56_load_64_bytes(tmp, hash1); Hacl_Impl_BignumQ_Mul_barrett_reduction(out, tmp); } static void Hacl_Impl_SHA512_ModQ_sha512_modq_pre( uint64_t *out, uint8_t *prefix, uint8_t *input, uint32_t len1 ) { uint64_t tmp[10U] = { 0U }; Hacl_Impl_SHA512_ModQ_sha512_modq_pre_(out, prefix, input, len1, tmp); } static void Hacl_Impl_SHA512_ModQ_sha512_modq_pre_pre2_( uint64_t *out, uint8_t *prefix, uint8_t *prefix2, uint8_t *input, uint32_t len1, uint64_t *tmp ) { uint8_t hash1[64U] = { 0U }; Hacl_Impl_Sha512_sha512_pre_pre2_msg(hash1, prefix, prefix2, input, len1); Hacl_Impl_Load56_load_64_bytes(tmp, hash1); Hacl_Impl_BignumQ_Mul_barrett_reduction(out, tmp); } static void Hacl_Impl_SHA512_ModQ_sha512_modq_pre_pre2( uint64_t *out, uint8_t *prefix, uint8_t *prefix2, uint8_t *input, uint32_t len1 ) { uint64_t tmp[10U] = { 0U }; Hacl_Impl_SHA512_ModQ_sha512_modq_pre_pre2_(out, prefix, prefix2, input, len1, tmp); } static bool Hacl_Impl_Ed25519_Verify_Steps_verify_step_1(uint64_t *r_, uint8_t *signature) { uint8_t *rs = signature; bool b_ = Hacl_Impl_Ed25519_PointDecompress_point_decompress(r_, rs); return b_; } static void Hacl_Impl_Ed25519_Verify_Steps_verify_step_2( uint8_t *r, uint8_t *msg, uint32_t len1, uint8_t *rs, uint8_t *public ) { uint64_t r_[5U] = { 0U }; Hacl_Impl_SHA512_ModQ_sha512_modq_pre_pre2(r_, rs, public, msg, len1); Hacl_Impl_Store56_store_56(r, r_); } static void Hacl_Impl_Ed25519_Verify_Steps_point_mul_g(uint64_t *result, uint8_t *scalar) { uint64_t g1[20U] = { 0U }; Hacl_Impl_Ed25519_G_make_g(g1); Hacl_Impl_Ed25519_Ladder_point_mul(result, scalar, g1); } static bool Hacl_Impl_Ed25519_Verify_Steps_verify_step_4( uint8_t *s, uint8_t *h_, uint64_t *a_, uint64_t *r_ ) { uint64_t tmp[60U] = { 0U }; uint64_t *hA = tmp; uint64_t *rhA = tmp + (uint32_t)20U; uint64_t *sB = tmp + (uint32_t)40U; Hacl_Impl_Ed25519_Verify_Steps_point_mul_g(sB, s); Hacl_Impl_Ed25519_Ladder_point_mul(hA, h_, a_); Hacl_Impl_Ed25519_PointAdd_point_add(rhA, r_, hA); bool b = Hacl_Impl_Ed25519_PointEqual_point_equal(sB, rhA); return b; } static bool Hacl_Impl_Ed25519_Verify_verify__( uint8_t *public, uint8_t *msg, uint32_t len1, uint8_t *signature, uint64_t *tmp, uint8_t *tmp_ ) { uint64_t *a_ = tmp; uint64_t *r_ = tmp + (uint32_t)20U; uint64_t *s = tmp + (uint32_t)40U; uint8_t *h_ = tmp_; bool b = Hacl_Impl_Ed25519_PointDecompress_point_decompress(a_, public); if (b) { uint8_t *rs = signature; bool b_ = Hacl_Impl_Ed25519_Verify_Steps_verify_step_1(r_, signature); if (b_) { Hacl_Impl_Load56_load_32_bytes(s, signature + (uint32_t)32U); bool b__ = Hacl_Impl_Ed25519_PointEqual_gte_q(s); if (b__) return false; else { Hacl_Impl_Ed25519_Verify_Steps_verify_step_2(h_, msg, len1, rs, public); bool b1 = Hacl_Impl_Ed25519_Verify_Steps_verify_step_4(signature + (uint32_t)32U, h_, a_, r_); return b1; } } else return false; } else return false; } static bool Hacl_Impl_Ed25519_Verify_verify_( uint8_t *public, uint8_t *msg, uint32_t len1, uint8_t *signature ) { uint64_t tmp[45U] = { 0U }; uint8_t tmp_[32U] = { 0U }; bool res = Hacl_Impl_Ed25519_Verify_verify__(public, msg, len1, signature, tmp, tmp_); return res; } static bool Hacl_Impl_Ed25519_Verify_verify( uint8_t *public, uint8_t *msg, uint32_t len1, uint8_t *signature ) { return Hacl_Impl_Ed25519_Verify_verify_(public, msg, len1, signature); } static void Hacl_Impl_Ed25519_Sign_Steps_point_mul_g(uint64_t *result, uint8_t *scalar) { uint64_t g1[20U] = { 0U }; Hacl_Impl_Ed25519_G_make_g(g1); Hacl_Impl_Ed25519_Ladder_point_mul(result, scalar, g1); } static void Hacl_Impl_Ed25519_Sign_Steps_point_mul_g_compress(uint8_t *out, uint8_t *s) { uint64_t tmp[20U] = { 0U }; Hacl_Impl_Ed25519_Sign_Steps_point_mul_g(tmp, s); Hacl_Impl_Ed25519_PointCompress_point_compress(out, tmp); } static void Hacl_Impl_Ed25519_Sign_Steps_copy_bytes(uint8_t *output, uint8_t *input, uint32_t len1) { memcpy(output, input, len1 * sizeof input[0U]); } static void Hacl_Impl_Ed25519_Sign_Steps_sign_step_1(uint8_t *secret, uint8_t *tmp_bytes) { uint8_t *a__ = tmp_bytes + (uint32_t)96U; uint8_t *apre = tmp_bytes + (uint32_t)224U; uint8_t *a = apre; Hacl_Impl_Ed25519_SecretExpand_secret_expand(apre, secret); Hacl_Impl_Ed25519_Sign_Steps_point_mul_g_compress(a__, a); } static void Hacl_Impl_Ed25519_Sign_Steps_sign_step_2( uint8_t *msg, uint32_t len1, uint8_t *tmp_bytes, uint64_t *tmp_ints ) { uint64_t *r = tmp_ints + (uint32_t)20U; uint8_t *apre = tmp_bytes + (uint32_t)224U; uint8_t *prefix = apre + (uint32_t)32U; Hacl_Impl_SHA512_ModQ_sha512_modq_pre(r, prefix, msg, len1); } static void Hacl_Impl_Ed25519_Sign_Steps_sign_step_4( uint8_t *msg, uint32_t len1, uint8_t *tmp_bytes, uint64_t *tmp_ints ) { uint64_t *h = tmp_ints + (uint32_t)60U; uint8_t *a__ = tmp_bytes + (uint32_t)96U; uint8_t *rs_ = tmp_bytes + (uint32_t)160U; uint8_t *apre = tmp_bytes + (uint32_t)224U; Hacl_Impl_SHA512_ModQ_sha512_modq_pre_pre2(h, rs_, a__, msg, len1); } static void Hacl_Impl_Ed25519_Sign_Steps_sign_step_5(uint8_t *tmp_bytes, uint64_t *tmp_ints) { uint64_t *r = tmp_ints + (uint32_t)20U; uint64_t *aq = tmp_ints + (uint32_t)45U; uint64_t *ha = tmp_ints + (uint32_t)50U; uint64_t *s = tmp_ints + (uint32_t)55U; uint64_t *h = tmp_ints + (uint32_t)60U; uint8_t *s_ = tmp_bytes + (uint32_t)192U; uint8_t *a = tmp_bytes + (uint32_t)224U; Hacl_Impl_Load56_load_32_bytes(aq, a); Hacl_Impl_BignumQ_Mul_mul_modq(ha, h, aq); Hacl_Impl_BignumQ_Mul_add_modq(s, r, ha); Hacl_Impl_Store56_store_56(s_, s); } static void Hacl_Impl_Ed25519_Sign_append_to_sig(uint8_t *signature, uint8_t *a, uint8_t *b) { Hacl_Impl_Ed25519_Sign_Steps_copy_bytes(signature, a, (uint32_t)32U); Hacl_Impl_Ed25519_Sign_Steps_copy_bytes(signature + (uint32_t)32U, b, (uint32_t)32U); } static void Hacl_Impl_Ed25519_Sign_sign_(uint8_t *signature, uint8_t *secret, uint8_t *msg, uint32_t len1) { uint8_t tmp_bytes[352U] = { 0U }; uint64_t tmp_ints[65U] = { 0U }; uint8_t *rs_ = tmp_bytes + (uint32_t)160U; uint8_t *s_ = tmp_bytes + (uint32_t)192U; Hacl_Impl_Ed25519_Sign_Steps_sign_step_1(secret, tmp_bytes); Hacl_Impl_Ed25519_Sign_Steps_sign_step_2(msg, len1, tmp_bytes, tmp_ints); uint8_t rb[32U] = { 0U }; uint64_t *r = tmp_ints + (uint32_t)20U; uint8_t *rs_0 = tmp_bytes + (uint32_t)160U; Hacl_Impl_Store56_store_56(rb, r); Hacl_Impl_Ed25519_Sign_Steps_point_mul_g_compress(rs_0, rb); Hacl_Impl_Ed25519_Sign_Steps_sign_step_4(msg, len1, tmp_bytes, tmp_ints); Hacl_Impl_Ed25519_Sign_Steps_sign_step_5(tmp_bytes, tmp_ints); Hacl_Impl_Ed25519_Sign_append_to_sig(signature, rs_, s_); } static void Hacl_Impl_Ed25519_Sign_sign(uint8_t *signature, uint8_t *secret, uint8_t *msg, uint32_t len1) { Hacl_Impl_Ed25519_Sign_sign_(signature, secret, msg, len1); } void Hacl_Ed25519_sign(uint8_t *signature, uint8_t *secret, uint8_t *msg, uint32_t len1) { Hacl_Impl_Ed25519_Sign_sign(signature, secret, msg, len1); } bool Hacl_Ed25519_verify(uint8_t *public, uint8_t *msg, uint32_t len1, uint8_t *signature) { return Hacl_Impl_Ed25519_Verify_verify(public, msg, len1, signature); } void Hacl_Ed25519_secret_to_public(uint8_t *out, uint8_t *secret) { Hacl_Impl_Ed25519_SecretToPublic_secret_to_public(out, secret); }