/* MIT License

 *

 * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation

 * Copyright (c) 2022-2023 HACL* Contributors

 *

 * 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 "internal/Hacl_Ed25519.h"

#include "internal/Hacl_Krmllib.h"

#include "internal/Hacl_Ed25519_PrecompTable.h"

#include "internal/Hacl_Curve25519_51.h"

#include "internal/Hacl_Bignum_Base.h"

#include "internal/Hacl_Bignum25519_51.h"

#include "../Hacl_Hash_SHA2_shim.h"

static inline void

fsum(uint64_t *out, uint64_t *a, uint64_t *b)

{

    Hacl_Impl_Curve25519_Field51_fadd(out, a, b);

}

static inline void

fdifference(uint64_t *out, uint64_t *a, uint64_t *b)

{

    Hacl_Impl_Curve25519_Field51_fsub(out, a, b);

}

void

Hacl_Bignum25519_reduce_513(uint64_t *a)

{

    uint64_t f0 = a[0U];

    uint64_t f1 = a[1U];

    uint64_t f2 = a[2U];

    uint64_t f3 = a[3U];

    uint64_t f4 = a[4U];

    uint64_t l_ = f0 + (uint64_t)0U;

    uint64_t tmp0 = l_ & (uint64_t)0x7ffffffffffffU;

    uint64_t c0 = l_ >> (uint32_t)51U;

    uint64_t l_0 = f1 + c0;

    uint64_t tmp1 = l_0 & (uint64_t)0x7ffffffffffffU;

    uint64_t c1 = l_0 >> (uint32_t)51U;

    uint64_t l_1 = f2 + c1;

    uint64_t tmp2 = l_1 & (uint64_t)0x7ffffffffffffU;

    uint64_t c2 = l_1 >> (uint32_t)51U;

    uint64_t l_2 = f3 + c2;

    uint64_t tmp3 = l_2 & (uint64_t)0x7ffffffffffffU;

    uint64_t c3 = l_2 >> (uint32_t)51U;

    uint64_t l_3 = f4 + c3;

    uint64_t tmp4 = l_3 & (uint64_t)0x7ffffffffffffU;

    uint64_t c4 = l_3 >> (uint32_t)51U;

    uint64_t l_4 = tmp0 + c4 * (uint64_t)19U;

    uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;

    uint64_t c5 = l_4 >> (uint32_t)51U;

    a[0U] = tmp0_;

    a[1U] = tmp1 + c5;

    a[2U] = tmp2;

    a[3U] = tmp3;

    a[4U] = tmp4;

}

static inline void

fmul0(uint64_t *output, uint64_t *input, uint64_t *input2)

{

    FStar_UInt128_uint128 tmp[10U];

    for (uint32_t _i = 0U; _i < (uint32_t)10U; ++_i)

        tmp[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U);

    Hacl_Impl_Curve25519_Field51_fmul(output, input, input2, tmp);

}

static inline void

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;

    out[0U] = o0;

    out[1U] = o1;

    out[2U] = o2;

    out[3U] = o3;

    out[4U] = o4;

}

static inline void

times_d(uint64_t *out, uint64_t *a)

{

    uint64_t d[5U] = { 0U };

    d[0U] = (uint64_t)0x00034dca135978a3U;

    d[1U] = (uint64_t)0x0001a8283b156ebdU;

    d[2U] = (uint64_t)0x0005e7a26001c029U;

    d[3U] = (uint64_t)0x000739c663a03cbbU;

    d[4U] = (uint64_t)0x00052036cee2b6ffU;

    fmul0(out, d, a);

}

static inline void

times_2d(uint64_t *out, uint64_t *a)

{

    uint64_t d2[5U] = { 0U };

    d2[0U] = (uint64_t)0x00069b9426b2f159U;

    d2[1U] = (uint64_t)0x00035050762add7aU;

    d2[2U] = (uint64_t)0x0003cf44c0038052U;

    d2[3U] = (uint64_t)0x0006738cc7407977U;

    d2[4U] = (uint64_t)0x0002406d9dc56dffU;

    fmul0(out, d2, a);

}

static inline void

fsquare(uint64_t *out, uint64_t *a)

{

    FStar_UInt128_uint128 tmp[5U];

    for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i)

        tmp[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U);

    Hacl_Impl_Curve25519_Field51_fsqr(out, a, tmp);

}

static inline void

fsquare_times(uint64_t *output, uint64_t *input, uint32_t count)

{

    FStar_UInt128_uint128 tmp[5U];

    for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i)

        tmp[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U);

    Hacl_Curve25519_51_fsquare_times(output, input, tmp, count);

}

static inline void

fsquare_times_inplace(uint64_t *output, uint32_t count)

{

    FStar_UInt128_uint128 tmp[5U];

    for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i)

        tmp[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U);

    Hacl_Curve25519_51_fsquare_times(output, output, tmp, count);

}

void

Hacl_Bignum25519_inverse(uint64_t *out, uint64_t *a)

{

    FStar_UInt128_uint128 tmp[10U];

    for (uint32_t _i = 0U; _i < (uint32_t)10U; ++_i)

        tmp[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U);

    Hacl_Curve25519_51_finv(out, a, tmp);

}

static inline void

reduce(uint64_t *out)

{

    uint64_t o0 = out[0U];

    uint64_t o1 = out[1U];

    uint64_t o2 = out[2U];

    uint64_t o3 = out[3U];

    uint64_t o4 = out[4U];

    uint64_t l_ = o0 + (uint64_t)0U;

    uint64_t tmp0 = l_ & (uint64_t)0x7ffffffffffffU;

    uint64_t c0 = l_ >> (uint32_t)51U;

    uint64_t l_0 = o1 + c0;

    uint64_t tmp1 = l_0 & (uint64_t)0x7ffffffffffffU;

    uint64_t c1 = l_0 >> (uint32_t)51U;

    uint64_t l_1 = o2 + c1;

    uint64_t tmp2 = l_1 & (uint64_t)0x7ffffffffffffU;

    uint64_t c2 = l_1 >> (uint32_t)51U;

    uint64_t l_2 = o3 + c2;

    uint64_t tmp3 = l_2 & (uint64_t)0x7ffffffffffffU;

    uint64_t c3 = l_2 >> (uint32_t)51U;

    uint64_t l_3 = o4 + c3;

    uint64_t tmp4 = l_3 & (uint64_t)0x7ffffffffffffU;

    uint64_t c4 = l_3 >> (uint32_t)51U;

    uint64_t l_4 = tmp0 + c4 * (uint64_t)19U;

    uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;

    uint64_t c5 = l_4 >> (uint32_t)51U;

    uint64_t f0 = tmp0_;

    uint64_t f1 = tmp1 + c5;

    uint64_t f2 = tmp2;

    uint64_t f3 = tmp3;

    uint64_t f4 = tmp4;

    uint64_t m0 = FStar_UInt64_gte_mask(f0, (uint64_t)0x7ffffffffffedU);

    uint64_t m1 = FStar_UInt64_eq_mask(f1, (uint64_t)0x7ffffffffffffU);

    uint64_t m2 = FStar_UInt64_eq_mask(f2, (uint64_t)0x7ffffffffffffU);

    uint64_t m3 = FStar_UInt64_eq_mask(f3, (uint64_t)0x7ffffffffffffU);

    uint64_t m4 = FStar_UInt64_eq_mask(f4, (uint64_t)0x7ffffffffffffU);

    uint64_t mask = (((m0 & m1) & m2) & m3) & m4;

    uint64_t f0_ = f0 - (mask & (uint64_t)0x7ffffffffffedU);

    uint64_t f1_ = f1 - (mask & (uint64_t)0x7ffffffffffffU);

    uint64_t f2_ = f2 - (mask & (uint64_t)0x7ffffffffffffU);

    uint64_t f3_ = f3 - (mask & (uint64_t)0x7ffffffffffffU);

    uint64_t f4_ = f4 - (mask & (uint64_t)0x7ffffffffffffU);

    uint64_t f01 = f0_;

    uint64_t f11 = f1_;

    uint64_t f21 = f2_;

    uint64_t f31 = f3_;

    uint64_t f41 = f4_;

    out[0U] = f01;

    out[1U] = f11;

    out[2U] = f21;

    out[3U] = f31;

    out[4U] = f41;

}

void

Hacl_Bignum25519_load_51(uint64_t *output, uint8_t *input)

{

    uint64_t u64s[4U] = { 0U };

    KRML_MAYBE_FOR4(i,

                    (uint32_t)0U,

                    (uint32_t)4U,

                    (uint32_t)1U,

                    uint64_t *os = u64s;

                    uint8_t *bj = input + i * (uint32_t)8U;

                    uint64_t u = load64_le(bj);

                    uint64_t r = u;

                    uint64_t x = r;

                    os[i] = x;);

    uint64_t u64s3 = u64s[3U];

    u64s[3U] = u64s3 & (uint64_t)0x7fffffffffffffffU;

    output[0U] = u64s[0U] & (uint64_t)0x7ffffffffffffU;

    output[1U] = u64s[0U] >> (uint32_t)51U | (u64s[1U] & (uint64_t)0x3fffffffffU) << (uint32_t)13U;

    output[2U] = u64s[1U] >> (uint32_t)38U | (u64s[2U] & (uint64_t)0x1ffffffU) << (uint32_t)26U;

    output[3U] = u64s[2U] >> (uint32_t)25U | (u64s[3U] & (uint64_t)0xfffU) << (uint32_t)39U;

    output[4U] = u64s[3U] >> (uint32_t)12U;

}

void

Hacl_Bignum25519_store_51(uint8_t *output, uint64_t *input)

{

    uint64_t u64s[4U] = { 0U };

    Hacl_Impl_Curve25519_Field51_store_felem(u64s, input);

    KRML_MAYBE_FOR4(i,

                    (uint32_t)0U,

                    (uint32_t)4U,

                    (uint32_t)1U,

                    store64_le(output + i * (uint32_t)8U, u64s[i]););

}

void

Hacl_Impl_Ed25519_PointDouble_point_double(uint64_t *out, uint64_t *p)

{

    uint64_t tmp[20U] = { 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 *x10 = p;

    uint64_t *y10 = p + (uint32_t)5U;

    uint64_t *z1 = p + (uint32_t)10U;

    fsquare(tmp1, x10);

    fsquare(tmp20, y10);

    fsum(tmp30, tmp1, tmp20);

    fdifference(tmp40, tmp1, tmp20);

    fsquare(tmp1, z1);

    times_2(tmp1, tmp1);

    uint64_t *tmp10 = 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 = p;

    uint64_t *y1 = p + (uint32_t)5U;

    fsum(tmp2, x1, y1);

    fsquare(tmp2, tmp2);

    Hacl_Bignum25519_reduce_513(tmp3);

    fdifference(tmp2, tmp3, tmp2);

    Hacl_Bignum25519_reduce_513(tmp10);

    Hacl_Bignum25519_reduce_513(tmp4);

    fsum(tmp10, tmp10, tmp4);

    uint64_t *tmp_f = tmp;

    uint64_t *tmp_e = tmp + (uint32_t)5U;

    uint64_t *tmp_h = tmp + (uint32_t)10U;

    uint64_t *tmp_g = tmp + (uint32_t)15U;

    uint64_t *x3 = out;

    uint64_t *y3 = out + (uint32_t)5U;

    uint64_t *z3 = out + (uint32_t)10U;

    uint64_t *t3 = out + (uint32_t)15U;

    fmul0(x3, tmp_e, tmp_f);

    fmul0(y3, tmp_g, tmp_h);

    fmul0(t3, tmp_e, tmp_h);

    fmul0(z3, tmp_f, tmp_g);

}

void

Hacl_Impl_Ed25519_PointAdd_point_add(uint64_t *out, uint64_t *p, uint64_t *q)

{

    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 = p;

    uint64_t *y1 = p + (uint32_t)5U;

    uint64_t *x2 = q;

    uint64_t *y2 = q + (uint32_t)5U;

    fdifference(tmp1, y1, x1);

    fdifference(tmp20, y2, x2);

    fmul0(tmp30, tmp1, tmp20);

    fsum(tmp1, y1, x1);

    fsum(tmp20, y2, x2);

    fmul0(tmp40, tmp1, tmp20);

    uint64_t *tmp10 = 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 *z1 = p + (uint32_t)10U;

    uint64_t *t1 = p + (uint32_t)15U;

    uint64_t *z2 = q + (uint32_t)10U;

    uint64_t *t2 = q + (uint32_t)15U;

    times_2d(tmp10, t1);

    fmul0(tmp10, tmp10, t2);

    times_2(tmp2, z1);

    fmul0(tmp2, tmp2, z2);

    fdifference(tmp5, tmp4, tmp3);

    fdifference(tmp6, tmp2, tmp10);

    fsum(tmp10, tmp2, tmp10);

    fsum(tmp2, tmp4, tmp3);

    uint64_t *tmp_g = tmp;

    uint64_t *tmp_h = tmp + (uint32_t)5U;

    uint64_t *tmp_e = tmp + (uint32_t)20U;

    uint64_t *tmp_f = tmp + (uint32_t)25U;

    uint64_t *x3 = out;

    uint64_t *y3 = out + (uint32_t)5U;

    uint64_t *z3 = out + (uint32_t)10U;

    uint64_t *t3 = out + (uint32_t)15U;

    fmul0(x3, tmp_e, tmp_f);

    fmul0(y3, tmp_g, tmp_h);

    fmul0(t3, tmp_e, tmp_h);

    fmul0(z3, tmp_f, tmp_g);

}

void

Hacl_Impl_Ed25519_PointConstants_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;

    x[0U] = (uint64_t)0U;

    x[1U] = (uint64_t)0U;

    x[2U] = (uint64_t)0U;

    x[3U] = (uint64_t)0U;

    x[4U] = (uint64_t)0U;

    y[0U] = (uint64_t)1U;

    y[1U] = (uint64_t)0U;

    y[2U] = (uint64_t)0U;

    y[3U] = (uint64_t)0U;

    y[4U] = (uint64_t)0U;

    z[0U] = (uint64_t)1U;

    z[1U] = (uint64_t)0U;

    z[2U] = (uint64_t)0U;

    z[3U] = (uint64_t)0U;

    z[4U] = (uint64_t)0U;

    t[0U] = (uint64_t)0U;

    t[1U] = (uint64_t)0U;

    t[2U] = (uint64_t)0U;

    t[3U] = (uint64_t)0U;

    t[4U] = (uint64_t)0U;

}

static inline void

pow2_252m2(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;

    uint64_t *c0 = buf + (uint32_t)15U;

    fsquare_times(a, z, (uint32_t)1U);

    fsquare_times(t00, a, (uint32_t)2U);

    fmul0(b0, t00, z);

    fmul0(a, b0, a);

    fsquare_times(t00, a, (uint32_t)1U);

    fmul0(b0, t00, b0);

    fsquare_times(t00, b0, (uint32_t)5U);

    fmul0(b0, t00, b0);

    fsquare_times(t00, b0, (uint32_t)10U);

    fmul0(c0, t00, b0);

    fsquare_times(t00, c0, (uint32_t)20U);

    fmul0(t00, t00, c0);

    fsquare_times_inplace(t00, (uint32_t)10U);

    fmul0(b0, t00, b0);

    fsquare_times(t00, b0, (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;

    fsquare_times(a0, z, (uint32_t)1U);

    fmul0(c, t0, b);

    fsquare_times(t0, c, (uint32_t)100U);

    fmul0(t0, t0, c);

    fsquare_times_inplace(t0, (uint32_t)50U);

    fmul0(t0, t0, b);

    fsquare_times_inplace(t0, (uint32_t)2U);

    fmul0(out, t0, a0);

}

static inline bool

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 inline void

mul_modp_sqrt_m1(uint64_t *x)

{

    uint64_t sqrt_m1[5U] = { 0U };

    sqrt_m1[0U] = (uint64_t)0x00061b274a0ea0b0U;

    sqrt_m1[1U] = (uint64_t)0x0000d5a5fc8f189dU;

    sqrt_m1[2U] = (uint64_t)0x0007ef5e9cbd0c60U;

    sqrt_m1[3U] = (uint64_t)0x00078595a6804c9eU;

    sqrt_m1[4U] = (uint64_t)0x0002b8324804fc1dU;

    fmul0(x, x, sqrt_m1);

}

static inline bool

recover_x(uint64_t *x, uint64_t *y, uint64_t sign)

{

    uint64_t tmp[15U] = { 0U };

    uint64_t *x2 = tmp;

    uint64_t x00 = y[0U];

    uint64_t x1 = y[1U];

    uint64_t x21 = y[2U];

    uint64_t x30 = y[3U];

    uint64_t x4 = y[4U];

    bool

        b =

            x00 >= (uint64_t)0x7ffffffffffedU && x1 == (uint64_t)0x7ffffffffffffU && x21 == (uint64_t)0x7ffffffffffffU && x30 == (uint64_t)0x7ffffffffffffU && x4 == (uint64_t)0x7ffffffffffffU;

    bool res;

    if (b) {

        res = false;

    } else {

        uint64_t tmp1[20U] = { 0U };

        uint64_t *one = tmp1;

        uint64_t *y2 = tmp1 + (uint32_t)5U;

        uint64_t *dyyi = tmp1 + (uint32_t)10U;

        uint64_t *dyy = tmp1 + (uint32_t)15U;

        one[0U] = (uint64_t)1U;

        one[1U] = (uint64_t)0U;

        one[2U] = (uint64_t)0U;

        one[3U] = (uint64_t)0U;

        one[4U] = (uint64_t)0U;

        fsquare(y2, y);

        times_d(dyy, y2);

        fsum(dyy, dyy, one);

        Hacl_Bignum25519_reduce_513(dyy);

        Hacl_Bignum25519_inverse(dyyi, dyy);

        fdifference(x2, y2, one);

        fmul0(x2, x2, dyyi);

        reduce(x2);

        bool x2_is_0 = is_0(x2);

        uint8_t z;

        if (x2_is_0) {

            if (sign == (uint64_t)0U) {

                x[0U] = (uint64_t)0U;

                x[1U] = (uint64_t)0U;

                x[2U] = (uint64_t)0U;

                x[3U] = (uint64_t)0U;

                x[4U] = (uint64_t)0U;

                z = (uint8_t)1U;

            } else {

                z = (uint8_t)0U;

            }

        } else {

            z = (uint8_t)2U;

        }

        if (z == (uint8_t)0U) {

            res = false;

        } else if (z == (uint8_t)1U) {

            res = true;

        } else {

            uint64_t *x210 = tmp;

            uint64_t *x31 = tmp + (uint32_t)5U;

            uint64_t *t00 = tmp + (uint32_t)10U;

            pow2_252m2(x31, x210);

            fsquare(t00, x31);

            fdifference(t00, t00, x210);

            Hacl_Bignum25519_reduce_513(t00);

            reduce(t00);

            bool t0_is_0 = is_0(t00);

            if (!t0_is_0) {

                mul_modp_sqrt_m1(x31);

            }

            uint64_t *x211 = tmp;

            uint64_t *x3 = tmp + (uint32_t)5U;

            uint64_t *t01 = tmp + (uint32_t)10U;

            fsquare(t01, x3);

            fdifference(t01, t01, x211);

            Hacl_Bignum25519_reduce_513(t01);

            reduce(t01);

            bool z1 = is_0(t01);

            if (z1 == false) {

                res = false;

            } else {

                uint64_t *x32 = tmp + (uint32_t)5U;

                uint64_t *t0 = tmp + (uint32_t)10U;

                reduce(x32);

                uint64_t x0 = x32[0U];

                uint64_t x01 = x0 & (uint64_t)1U;

                if (!(x01 == sign)) {

                    t0[0U] = (uint64_t)0U;

                    t0[1U] = (uint64_t)0U;

                    t0[2U] = (uint64_t)0U;

                    t0[3U] = (uint64_t)0U;

                    t0[4U] = (uint64_t)0U;

                    fdifference(x32, t0, x32);

                    Hacl_Bignum25519_reduce_513(x32);

                    reduce(x32);

                }

                memcpy(x, x32, (uint32_t)5U * sizeof(uint64_t));

                res = true;

            }

        }

    }

    bool res0 = res;

    return res0;

}

bool

Hacl_Impl_Ed25519_PointDecompress_point_decompress(uint64_t *out, uint8_t *s)

{

    uint64_t tmp[10U] = { 0U };

    uint64_t *y = tmp;

    uint64_t *x = tmp + (uint32_t)5U;

    uint8_t s31 = s[31U];

    uint8_t z = s31 >> (uint32_t)7U;

    uint64_t sign = (uint64_t)z;

    Hacl_Bignum25519_load_51(y, s);

    bool z0 = recover_x(x, y, sign);

    bool res;

    if (z0 == false) {

        res = false;

    } else {

        uint64_t *outx = out;

        uint64_t *outy = out + (uint32_t)5U;

        uint64_t *outz = out + (uint32_t)10U;

        uint64_t *outt = out + (uint32_t)15U;

        memcpy(outx, x, (uint32_t)5U * sizeof(uint64_t));

        memcpy(outy, y, (uint32_t)5U * sizeof(uint64_t));

        outz[0U] = (uint64_t)1U;

        outz[1U] = (uint64_t)0U;

        outz[2U] = (uint64_t)0U;

        outz[3U] = (uint64_t)0U;

        outz[4U] = (uint64_t)0U;

        fmul0(outt, x, y);

        res = true;

    }

    bool res0 = res;

    return res0;

}

void

Hacl_Impl_Ed25519_PointCompress_point_compress(uint8_t *z, uint64_t *p)

{

    uint64_t tmp[15U] = { 0U };

    uint64_t *x = tmp + (uint32_t)5U;

    uint64_t *out = tmp + (uint32_t)10U;

    uint64_t *zinv1 = tmp;

    uint64_t *x1 = tmp + (uint32_t)5U;

    uint64_t *out1 = tmp + (uint32_t)10U;

    uint64_t *px = p;

    uint64_t *py = p + (uint32_t)5U;

    uint64_t *pz = p + (uint32_t)10U;

    Hacl_Bignum25519_inverse(zinv1, pz);

    fmul0(x1, px, zinv1);

    reduce(x1);

    fmul0(out1, py, zinv1);

    Hacl_Bignum25519_reduce_513(out1);

    uint64_t x0 = x[0U];

    uint64_t b = x0 & (uint64_t)1U;

    Hacl_Bignum25519_store_51(z, out);

    uint8_t xbyte = (uint8_t)b;

    uint8_t o31 = z[31U];

    z[31U] = o31 + (xbyte << (uint32_t)7U);

}

static inline void

barrett_reduction(uint64_t *z, uint64_t *t)

{

    uint64_t t0 = t[0U];

    uint64_t t1 = t[1U];

    uint64_t t2 = t[2U];

    uint64_t t3 = t[3U];

    uint64_t t4 = t[4U];

    uint64_t t5 = t[5U];

    uint64_t t6 = t[6U];

    uint64_t t7 = t[7U];

    uint64_t t8 = t[8U];

    uint64_t t9 = t[9U];

    uint64_t m00 = (uint64_t)0x12631a5cf5d3edU;

    uint64_t m10 = (uint64_t)0xf9dea2f79cd658U;

    uint64_t m20 = (uint64_t)0x000000000014deU;

    uint64_t m30 = (uint64_t)0x00000000000000U;

    uint64_t m40 = (uint64_t)0x00000010000000U;

    uint64_t m0 = m00;

    uint64_t m1 = m10;

    uint64_t m2 = m20;

    uint64_t m3 = m30;

    uint64_t m4 = m40;

    uint64_t m010 = (uint64_t)0x9ce5a30a2c131bU;

    uint64_t m110 = (uint64_t)0x215d086329a7edU;

    uint64_t m210 = (uint64_t)0xffffffffeb2106U;

    uint64_t m310 = (uint64_t)0xffffffffffffffU;

    uint64_t m410 = (uint64_t)0x00000fffffffffU;

    uint64_t mu0 = m010;

    uint64_t mu1 = m110;

    uint64_t mu2 = m210;

    uint64_t mu3 = m310;

    uint64_t mu4 = m410;

    uint64_t y_ = (t5 & (uint64_t)0xffffffU) << (uint32_t)32U;

    uint64_t x_ = t4 >> (uint32_t)24U;

    uint64_t z00 = x_ | y_;

    uint64_t y_0 = (t6 & (uint64_t)0xffffffU) << (uint32_t)32U;

    uint64_t x_0 = t5 >> (uint32_t)24U;

    uint64_t z10 = x_0 | y_0;

    uint64_t y_1 = (t7 & (uint64_t)0xffffffU) << (uint32_t)32U;

    uint64_t x_1 = t6 >> (uint32_t)24U;

    uint64_t z20 = x_1 | y_1;

    uint64_t y_2 = (t8 & (uint64_t)0xffffffU) << (uint32_t)32U;

    uint64_t x_2 = t7 >> (uint32_t)24U;

    uint64_t z30 = x_2 | y_2;

    uint64_t y_3 = (t9 & (uint64_t)0xffffffU) << (uint32_t)32U;

    uint64_t x_3 = t8 >> (uint32_t)24U;

    uint64_t z40 = x_3 | y_3;

    uint64_t q0 = z00;

    uint64_t q1 = z10;

    uint64_t q2 = z20;

    uint64_t q3 = z30;

    uint64_t q4 = z40;

    FStar_UInt128_uint128 xy000 = FStar_UInt128_mul_wide(q0, mu0);

    FStar_UInt128_uint128 xy010 = FStar_UInt128_mul_wide(q0, mu1);

    FStar_UInt128_uint128 xy020 = FStar_UInt128_mul_wide(q0, mu2);

    FStar_UInt128_uint128 xy030 = FStar_UInt128_mul_wide(q0, mu3);

    FStar_UInt128_uint128 xy040 = FStar_UInt128_mul_wide(q0, mu4);

    FStar_UInt128_uint128 xy100 = FStar_UInt128_mul_wide(q1, mu0);

    FStar_UInt128_uint128 xy110 = FStar_UInt128_mul_wide(q1, mu1);

    FStar_UInt128_uint128 xy120 = FStar_UInt128_mul_wide(q1, mu2);

    FStar_UInt128_uint128 xy130 = FStar_UInt128_mul_wide(q1, mu3);

    FStar_UInt128_uint128 xy14 = FStar_UInt128_mul_wide(q1, mu4);

    FStar_UInt128_uint128 xy200 = FStar_UInt128_mul_wide(q2, mu0);

    FStar_UInt128_uint128 xy210 = FStar_UInt128_mul_wide(q2, mu1);

    FStar_UInt128_uint128 xy220 = FStar_UInt128_mul_wide(q2, mu2);

    FStar_UInt128_uint128 xy23 = FStar_UInt128_mul_wide(q2, mu3);

    FStar_UInt128_uint128 xy24 = FStar_UInt128_mul_wide(q2, mu4);

    FStar_UInt128_uint128 xy300 = FStar_UInt128_mul_wide(q3, mu0);

    FStar_UInt128_uint128 xy310 = FStar_UInt128_mul_wide(q3, mu1);

    FStar_UInt128_uint128 xy32 = FStar_UInt128_mul_wide(q3, mu2);

    FStar_UInt128_uint128 xy33 = FStar_UInt128_mul_wide(q3, mu3);

    FStar_UInt128_uint128 xy34 = FStar_UInt128_mul_wide(q3, mu4);

    FStar_UInt128_uint128 xy400 = FStar_UInt128_mul_wide(q4, mu0);

    FStar_UInt128_uint128 xy41 = FStar_UInt128_mul_wide(q4, mu1);

    FStar_UInt128_uint128 xy42 = FStar_UInt128_mul_wide(q4, mu2);

    FStar_UInt128_uint128 xy43 = FStar_UInt128_mul_wide(q4, mu3);

    FStar_UInt128_uint128 xy44 = FStar_UInt128_mul_wide(q4, mu4);

    FStar_UInt128_uint128 z01 = xy000;

    FStar_UInt128_uint128 z11 = FStar_UInt128_add_mod(xy010, xy100);

    FStar_UInt128_uint128 z21 = FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy020, xy110), xy200);

    FStar_UInt128_uint128

        z31 =

            FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy030, xy120), xy210),

                                  xy300);

    FStar_UInt128_uint128

        z41 =

            FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy040,

                                                                                                    xy130),

                                                                              xy220),

                                                        xy310),

                                  xy400);

    FStar_UInt128_uint128

        z5 =

            FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy14, xy23), xy32),

                                  xy41);

    FStar_UInt128_uint128 z6 = FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy24, xy33), xy42);

    FStar_UInt128_uint128 z7 = FStar_UInt128_add_mod(xy34, xy43);

    FStar_UInt128_uint128 z8 = xy44;

    FStar_UInt128_uint128 carry0 = FStar_UInt128_shift_right(z01, (uint32_t)56U);

    FStar_UInt128_uint128 c00 = carry0;

    FStar_UInt128_uint128

        carry1 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z11, c00), (uint32_t)56U);

    FStar_UInt128_uint128 c10 = carry1;

    FStar_UInt128_uint128

        carry2 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z21, c10), (uint32_t)56U);

    FStar_UInt128_uint128 c20 = carry2;

    FStar_UInt128_uint128

        carry3 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z31, c20), (uint32_t)56U);

    FStar_UInt128_uint128 c30 = carry3;

    FStar_UInt128_uint128

        carry4 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z41, c30), (uint32_t)56U);

    uint64_t

        t100 =

            FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z41, c30)) & (uint64_t)0xffffffffffffffU;

    FStar_UInt128_uint128 c40 = carry4;

    uint64_t t410 = t100;

    FStar_UInt128_uint128

        carry5 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z5, c40), (uint32_t)56U);

    uint64_t

        t101 =

            FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z5, c40)) & (uint64_t)0xffffffffffffffU;

    FStar_UInt128_uint128 c5 = carry5;

    uint64_t t51 = t101;

    FStar_UInt128_uint128

        carry6 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z6, c5), (uint32_t)56U);

    uint64_t

        t102 =

            FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z6, c5)) & (uint64_t)0xffffffffffffffU;

    FStar_UInt128_uint128 c6 = carry6;

    uint64_t t61 = t102;

    FStar_UInt128_uint128

        carry7 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z7, c6), (uint32_t)56U);

    uint64_t

        t103 =

            FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z7, c6)) & (uint64_t)0xffffffffffffffU;

    FStar_UInt128_uint128 c7 = carry7;

    uint64_t t71 = t103;

    FStar_UInt128_uint128

        carry8 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z8, c7), (uint32_t)56U);

    uint64_t

        t104 =

            FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z8, c7)) & (uint64_t)0xffffffffffffffU;

    FStar_UInt128_uint128 c8 = carry8;

    uint64_t t81 = t104;

    uint64_t t91 = FStar_UInt128_uint128_to_uint64(c8);

    uint64_t qmu4_ = t410;

    uint64_t qmu5_ = t51;

    uint64_t qmu6_ = t61;

    uint64_t qmu7_ = t71;

    uint64_t qmu8_ = t81;

    uint64_t qmu9_ = t91;

    uint64_t y_4 = (qmu5_ & (uint64_t)0xffffffffffU) << (uint32_t)16U;

    uint64_t x_4 = qmu4_ >> (uint32_t)40U;

    uint64_t z02 = x_4 | y_4;

    uint64_t y_5 = (qmu6_ & (uint64_t)0xffffffffffU) << (uint32_t)16U;

    uint64_t x_5 = qmu5_ >> (uint32_t)40U;

    uint64_t z12 = x_5 | y_5;

    uint64_t y_6 = (qmu7_ & (uint64_t)0xffffffffffU) << (uint32_t)16U;

    uint64_t x_6 = qmu6_ >> (uint32_t)40U;

    uint64_t z22 = x_6 | y_6;

    uint64_t y_7 = (qmu8_ & (uint64_t)0xffffffffffU) << (uint32_t)16U;

    uint64_t x_7 = qmu7_ >> (uint32_t)40U;

    uint64_t z32 = x_7 | y_7;

    uint64_t y_8 = (qmu9_ & (uint64_t)0xffffffffffU) << (uint32_t)16U;

    uint64_t x_8 = qmu8_ >> (uint32_t)40U;

    uint64_t z42 = x_8 | y_8;

    uint64_t qdiv0 = z02;

    uint64_t qdiv1 = z12;

    uint64_t qdiv2 = z22;

    uint64_t qdiv3 = z32;

    uint64_t qdiv4 = z42;

    uint64_t r0 = t0;

    uint64_t r1 = t1;

    uint64_t r2 = t2;

    uint64_t r3 = t3;

    uint64_t r4 = t4 & (uint64_t)0xffffffffffU;

    FStar_UInt128_uint128 xy00 = FStar_UInt128_mul_wide(qdiv0, m0);

    FStar_UInt128_uint128 xy01 = FStar_UInt128_mul_wide(qdiv0, m1);

    FStar_UInt128_uint128 xy02 = FStar_UInt128_mul_wide(qdiv0, m2);

    FStar_UInt128_uint128 xy03 = FStar_UInt128_mul_wide(qdiv0, m3);

    FStar_UInt128_uint128 xy04 = FStar_UInt128_mul_wide(qdiv0, m4);

    FStar_UInt128_uint128 xy10 = FStar_UInt128_mul_wide(qdiv1, m0);

    FStar_UInt128_uint128 xy11 = FStar_UInt128_mul_wide(qdiv1, m1);

    FStar_UInt128_uint128 xy12 = FStar_UInt128_mul_wide(qdiv1, m2);

    FStar_UInt128_uint128 xy13 = FStar_UInt128_mul_wide(qdiv1, m3);

    FStar_UInt128_uint128 xy20 = FStar_UInt128_mul_wide(qdiv2, m0);

    FStar_UInt128_uint128 xy21 = FStar_UInt128_mul_wide(qdiv2, m1);

    FStar_UInt128_uint128 xy22 = FStar_UInt128_mul_wide(qdiv2, m2);

    FStar_UInt128_uint128 xy30 = FStar_UInt128_mul_wide(qdiv3, m0);

    FStar_UInt128_uint128 xy31 = FStar_UInt128_mul_wide(qdiv3, m1);

    FStar_UInt128_uint128 xy40 = FStar_UInt128_mul_wide(qdiv4, m0);

    FStar_UInt128_uint128 carry9 = FStar_UInt128_shift_right(xy00, (uint32_t)56U);

    uint64_t t105 = FStar_UInt128_uint128_to_uint64(xy00) & (uint64_t)0xffffffffffffffU;

    FStar_UInt128_uint128 c0 = carry9;

    uint64_t t010 = t105;

    FStar_UInt128_uint128

        carry10 =

            FStar_UInt128_shift_right(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy01, xy10), c0),

                                      (uint32_t)56U);

    uint64_t

        t106 =

            FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy01, xy10), c0)) & (uint64_t)0xffffffffffffffU;

    FStar_UInt128_uint128 c11 = carry10;

    uint64_t t110 = t106;

    FStar_UInt128_uint128

        carry11 =

            FStar_UInt128_shift_right(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy02,

                                                                                                        xy11),

                                                                                  xy20),

                                                            c11),

                                      (uint32_t)56U);

    uint64_t

        t107 =

            FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy02,

                                                                                                              xy11),

                                                                                        xy20),

                                                                  c11)) &

            (uint64_t)0xffffffffffffffU;

    FStar_UInt128_uint128 c21 = carry11;

    uint64_t t210 = t107;

    FStar_UInt128_uint128

        carry =

            FStar_UInt128_shift_right(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy03,

                                                                                                                              xy12),

                                                                                                        xy21),

                                                                                  xy30),

                                                            c21),

                                      (uint32_t)56U);

    uint64_t

        t108 =

            FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy03,

                                                                                                                                    xy12),

                                                                                                              xy21),

                                                                                        xy30),

                                                                  c21)) &

            (uint64_t)0xffffffffffffffU;

    FStar_UInt128_uint128 c31 = carry;

    uint64_t t310 = t108;

    uint64_t

        t411 =

            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,

                                                                                                                                                          xy13),

                                                                                                                                    xy22),

                                                                                                              xy31),

                                                                                        xy40),

                                                                  c31)) &

            (uint64_t)0xffffffffffU;

    uint64_t qmul0 = t010;

    uint64_t qmul1 = t110;

    uint64_t qmul2 = t210;

    uint64_t qmul3 = t310;

    uint64_t qmul4 = t411;

    uint64_t b5 = (r0 - qmul0) >> (uint32_t)63U;

    uint64_t t109 = (b5 << (uint32_t)56U) + r0 - qmul0;

    uint64_t c1 = b5;

    uint64_t t011 = t109;

    uint64_t b6 = (r1 - (qmul1 + c1)) >> (uint32_t)63U;

    uint64_t t1010 = (b6 << (uint32_t)56U) + r1 - (qmul1 + c1);

    uint64_t c2 = b6;

    uint64_t t111 = t1010;

    uint64_t b7 = (r2 - (qmul2 + c2)) >> (uint32_t)63U;

    uint64_t t1011 = (b7 << (uint32_t)56U) + r2 - (qmul2 + c2);

    uint64_t c3 = b7;

    uint64_t t211 = t1011;

    uint64_t b8 = (r3 - (qmul3 + c3)) >> (uint32_t)63U;

    uint64_t t1012 = (b8 << (uint32_t)56U) + r3 - (qmul3 + c3);

    uint64_t c4 = b8;

    uint64_t t311 = t1012;

    uint64_t b9 = (r4 - (qmul4 + c4)) >> (uint32_t)63U;

    uint64_t t1013 = (b9 << (uint32_t)40U) + r4 - (qmul4 + c4);

    uint64_t t412 = t1013;

    uint64_t s0 = t011;

    uint64_t s1 = t111;

    uint64_t s2 = t211;

    uint64_t s3 = t311;

    uint64_t s4 = t412;

    uint64_t m01 = (uint64_t)0x12631a5cf5d3edU;

    uint64_t m11 = (uint64_t)0xf9dea2f79cd658U;

    uint64_t m21 = (uint64_t)0x000000000014deU;

    uint64_t m31 = (uint64_t)0x00000000000000U;

    uint64_t m41 = (uint64_t)0x00000010000000U;

    uint64_t y0 = m01;

    uint64_t y1 = m11;

    uint64_t y2 = m21;

    uint64_t y3 = m31;

    uint64_t y4 = m41;

    uint64_t b10 = (s0 - y0) >> (uint32_t)63U;

    uint64_t t1014 = (b10 << (uint32_t)56U) + s0 - y0;

    uint64_t b0 = b10;

    uint64_t t01 = t1014;

    uint64_t b11 = (s1 - (y1 + b0)) >> (uint32_t)63U;

    uint64_t t1015 = (b11 << (uint32_t)56U) + s1 - (y1 + b0);

    uint64_t b1 = b11;

    uint64_t t11 = t1015;

    uint64_t b12 = (s2 - (y2 + b1)) >> (uint32_t)63U;

    uint64_t t1016 = (b12 << (uint32_t)56U) + s2 - (y2 + b1);

    uint64_t b2 = b12;