/* MIT License
 *
 * Copyright (c) 2016-2020 INRIA, CMU 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_GenericField64.h"

#include "internal/Hacl_Bignum.h"

/*******************************************************************************

A verified field arithmetic library.

This is a 64-bit optimized version, where bignums are represented as an array
of `len` unsigned 64-bit integers, i.e. uint64_t[len].

All the arithmetic operations are performed in the Montgomery domain.

All the functions below preserve the following invariant for a bignum `aM` in
Montgomery form.
  • aM < n

*******************************************************************************/


/*
Check whether this library will work for a modulus `n`.

  The function returns false if any of the following preconditions are violated,
  true otherwise.
  • n % 2 = 1
  • 1 < n
*/
bool Hacl_GenericField64_field_modulus_check(uint32_t len, uint64_t *n)
{
  uint64_t m = Hacl_Bignum_Montgomery_bn_check_modulus_u64(len, n);
  return m == (uint64_t)0xFFFFFFFFFFFFFFFFU;
}

/*
Heap-allocate and initialize a montgomery context.

  The argument n is meant to be `len` limbs in size, i.e. uint64_t[len].

  Before calling this function, the caller will need to ensure that the following
  preconditions are observed.
  • n % 2 = 1
  • 1 < n

  The caller will need to call Hacl_GenericField64_field_free on the return value
  to avoid memory leaks.
*/
Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64
*Hacl_GenericField64_field_init(uint32_t len, uint64_t *n)
{
  KRML_CHECK_SIZE(sizeof (uint64_t), len);
  {
    uint64_t *r2 = (uint64_t *)KRML_HOST_CALLOC(len, sizeof (uint64_t));
    KRML_CHECK_SIZE(sizeof (uint64_t), len);
    {
      uint64_t *n1 = (uint64_t *)KRML_HOST_CALLOC(len, sizeof (uint64_t));
      uint64_t *r21 = r2;
      uint64_t *n11 = n1;
      uint32_t nBits;
      uint64_t mu;
      memcpy(n11, n, len * sizeof (uint64_t));
      nBits = (uint32_t)64U * (uint32_t)Hacl_Bignum_Lib_bn_get_top_index_u64(len, n);
      Hacl_Bignum_Montgomery_bn_precomp_r2_mod_n_u64(len, nBits, n, r21);
      mu = Hacl_Bignum_ModInvLimb_mod_inv_uint64(n[0U]);
      {
        Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 res;
        res.len = len;
        res.n = n11;
        res.mu = mu;
        res.r2 = r21;
        KRML_CHECK_SIZE(sizeof (Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64), (uint32_t)1U);
        {
          Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64
          *buf =
            (Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 *)KRML_HOST_MALLOC(sizeof (
                Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64
              ));
          buf[0U] = res;
          return buf;
        }
      }
    }
  }
}

/*
Deallocate the memory previously allocated by Hacl_GenericField64_field_init.

  The argument k is a montgomery context obtained through Hacl_GenericField64_field_init.
*/
void Hacl_GenericField64_field_free(Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 *k)
{
  Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 k1 = *k;
  uint64_t *n = k1.n;
  uint64_t *r2 = k1.r2;
  KRML_HOST_FREE(n);
  KRML_HOST_FREE(r2);
  KRML_HOST_FREE(k);
}

/*
Return the size of a modulus `n` in limbs.

  The argument k is a montgomery context obtained through Hacl_GenericField64_field_init.
*/
uint32_t Hacl_GenericField64_field_get_len(Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 *k)
{
  Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 k1 = *k;
  return k1.len;
}

/*
Convert a bignum from the regular representation to the Montgomery representation.

  Write `a * R mod n` in `aM`.

  The argument a and the outparam aM are meant to be `len` limbs in size, i.e. uint64_t[len].
  The argument k is a montgomery context obtained through Hacl_GenericField64_field_init.
*/
void
Hacl_GenericField64_to_field(
  Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 *k,
  uint64_t *a,
  uint64_t *aM
)
{
  uint32_t len1 = Hacl_GenericField64_field_get_len(k);
  Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 k1 = *k;
  Hacl_Bignum_Montgomery_bn_to_mont_u64(len1, k1.n, k1.mu, k1.r2, a, aM);
}

/*
Convert a result back from the Montgomery representation to the regular representation.

  Write `aM / R mod n` in `a`, i.e.
  Hacl_GenericField64_from_field(k, Hacl_GenericField64_to_field(k, a)) == a % n

  The argument aM and the outparam a are meant to be `len` limbs in size, i.e. uint64_t[len].
  The argument k is a montgomery context obtained through Hacl_GenericField64_field_init.
*/
void
Hacl_GenericField64_from_field(
  Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 *k,
  uint64_t *aM,
  uint64_t *a
)
{
  uint32_t len1 = Hacl_GenericField64_field_get_len(k);
  Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 k1 = *k;
  Hacl_Bignum_Montgomery_bn_from_mont_u64(len1, k1.n, k1.mu, aM, a);
}

/*
Write `aM + bM mod n` in `cM`.

  The arguments aM, bM, and the outparam cM are meant to be `len` limbs in size, i.e. uint64_t[len].
  The argument k is a montgomery context obtained through Hacl_GenericField64_field_init.
*/
void
Hacl_GenericField64_add(
  Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 *k,
  uint64_t *aM,
  uint64_t *bM,
  uint64_t *cM
)
{
  uint32_t len1 = Hacl_GenericField64_field_get_len(k);
  Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 k1 = *k;
  Hacl_Bignum_bn_add_mod_n_u64(len1, k1.n, aM, bM, cM);
}

/*
Write `aM - bM mod n` to `cM`.

  The arguments aM, bM, and the outparam cM are meant to be `len` limbs in size, i.e. uint64_t[len].
  The argument k is a montgomery context obtained through Hacl_GenericField64_field_init.
*/
void
Hacl_GenericField64_sub(
  Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 *k,
  uint64_t *aM,
  uint64_t *bM,
  uint64_t *cM
)
{
  uint32_t len1 = Hacl_GenericField64_field_get_len(k);
  Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 k1 = *k;
  Hacl_Bignum_bn_sub_mod_n_u64(len1, k1.n, aM, bM, cM);
}

/*
Write `aM * bM mod n` in `cM`.

  The arguments aM, bM, and the outparam cM are meant to be `len` limbs in size, i.e. uint64_t[len].
  The argument k is a montgomery context obtained through Hacl_GenericField64_field_init.
*/
void
Hacl_GenericField64_mul(
  Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 *k,
  uint64_t *aM,
  uint64_t *bM,
  uint64_t *cM
)
{
  uint32_t len1 = Hacl_GenericField64_field_get_len(k);
  Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 k1 = *k;
  Hacl_Bignum_Montgomery_bn_mont_mul_u64(len1, k1.n, k1.mu, aM, bM, cM);
}

/*
Write `aM * aM mod n` in `cM`.

  The argument aM and the outparam cM are meant to be `len` limbs in size, i.e. uint64_t[len].
  The argument k is a montgomery context obtained through Hacl_GenericField64_field_init.
*/
void
Hacl_GenericField64_sqr(
  Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 *k,
  uint64_t *aM,
  uint64_t *cM
)
{
  uint32_t len1 = Hacl_GenericField64_field_get_len(k);
  Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 k1 = *k;
  Hacl_Bignum_Montgomery_bn_mont_sqr_u64(len1, k1.n, k1.mu, aM, cM);
}

/*
Convert a bignum `one` to its Montgomery representation.

  The outparam oneM is meant to be `len` limbs in size, i.e. uint64_t[len].
  The argument k is a montgomery context obtained through Hacl_GenericField64_field_init.
*/
void Hacl_GenericField64_one(Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 *k, uint64_t *oneM)
{
  uint32_t len1 = Hacl_GenericField64_field_get_len(k);
  Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 k1 = *k;
  Hacl_Bignum_Montgomery_bn_from_mont_u64(len1, k1.n, k1.mu, k1.r2, oneM);
}

/*
Write `aM ^ b mod n` in `resM`.

  The argument aM and the outparam resM are meant to be `len` limbs in size, i.e. uint64_t[len].
  The argument k is a montgomery context obtained through Hacl_GenericField64_field_init.

  The argument b is a bignum of any size, and bBits is an upper bound on the
  number of significant bits of b. A tighter bound results in faster execution
  time. When in doubt, the number of bits for the bignum size is always a safe
  default, e.g. if b is a 256-bit bignum, bBits should be 256.

  This function is constant-time over its argument b, at the cost of a slower
  execution time than exp_vartime.

  Before calling this function, the caller will need to ensure that the following
  precondition is observed.
  • b < pow2 bBits
*/
void
Hacl_GenericField64_exp_consttime(
  Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 *k,
  uint64_t *aM,
  uint32_t bBits,
  uint64_t *b,
  uint64_t *resM
)
{
  uint32_t len1 = Hacl_GenericField64_field_get_len(k);
  Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 k1 = *k;
  KRML_CHECK_SIZE(sizeof (uint64_t), k1.len);
  {
    uint64_t aMc[k1.len];
    memset(aMc, 0U, k1.len * sizeof (uint64_t));
    memcpy(aMc, aM, k1.len * sizeof (uint64_t));
    if (bBits < (uint32_t)200U)
    {
      Hacl_Bignum_Montgomery_bn_from_mont_u64(len1, k1.n, k1.mu, k1.r2, resM);
      {
        uint64_t sw = (uint64_t)0U;
        {
          uint32_t i0;
          for (i0 = (uint32_t)0U; i0 < bBits; i0++)
          {
            uint32_t i1 = (bBits - i0 - (uint32_t)1U) / (uint32_t)64U;
            uint32_t j = (bBits - i0 - (uint32_t)1U) % (uint32_t)64U;
            uint64_t tmp = b[i1];
            uint64_t bit = tmp >> j & (uint64_t)1U;
            uint64_t sw1 = bit ^ sw;
            {
              uint32_t i;
              for (i = (uint32_t)0U; i < len1; i++)
              {
                uint64_t dummy = ((uint64_t)0U - sw1) & (resM[i] ^ aMc[i]);
                resM[i] = resM[i] ^ dummy;
                aMc[i] = aMc[i] ^ dummy;
              }
            }
            Hacl_Bignum_Montgomery_bn_mont_mul_u64(len1, k1.n, k1.mu, aMc, resM, aMc);
            Hacl_Bignum_Montgomery_bn_mont_sqr_u64(len1, k1.n, k1.mu, resM, resM);
            sw = bit;
          }
        }
        {
          uint64_t sw0 = sw;
          {
            uint32_t i;
            for (i = (uint32_t)0U; i < len1; i++)
            {
              uint64_t dummy = ((uint64_t)0U - sw0) & (resM[i] ^ aMc[i]);
              resM[i] = resM[i] ^ dummy;
              aMc[i] = aMc[i] ^ dummy;
            }
          }
        }
      }
    }
    else
    {
      uint32_t bLen;
      if (bBits == (uint32_t)0U)
      {
        bLen = (uint32_t)1U;
      }
      else
      {
        bLen = (bBits - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U;
      }
      Hacl_Bignum_Montgomery_bn_from_mont_u64(len1, k1.n, k1.mu, k1.r2, resM);
      KRML_CHECK_SIZE(sizeof (uint64_t), (uint32_t)16U * len1);
      {
        uint64_t table[(uint32_t)16U * len1];
        memset(table, 0U, (uint32_t)16U * len1 * sizeof (uint64_t));
        memcpy(table, resM, len1 * sizeof (uint64_t));
        {
          uint64_t *t1 = table + len1;
          memcpy(t1, aMc, len1 * sizeof (uint64_t));
          {
            uint32_t i;
            for (i = (uint32_t)0U; i < (uint32_t)14U; i++)
            {
              uint64_t *t11 = table + (i + (uint32_t)1U) * len1;
              uint64_t *t2 = table + (i + (uint32_t)2U) * len1;
              Hacl_Bignum_Montgomery_bn_mont_mul_u64(len1, k1.n, k1.mu, t11, aMc, t2);
            }
          }
          if (bBits % (uint32_t)4U != (uint32_t)0U)
          {
            uint64_t mask_l = (uint64_t)16U - (uint64_t)1U;
            uint32_t i0 = bBits / (uint32_t)4U * (uint32_t)4U / (uint32_t)64U;
            uint32_t j = bBits / (uint32_t)4U * (uint32_t)4U % (uint32_t)64U;
            uint64_t p1 = b[i0] >> j;
            uint64_t ite;
            if (i0 + (uint32_t)1U < bLen && (uint32_t)0U < j)
            {
              ite = p1 | b[i0 + (uint32_t)1U] << ((uint32_t)64U - j);
            }
            else
            {
              ite = p1;
            }
            {
              uint64_t bits_c = ite & mask_l;
              memcpy(resM, table, len1 * sizeof (uint64_t));
              {
                uint32_t i1;
                for (i1 = (uint32_t)0U; i1 < (uint32_t)15U; i1++)
                {
                  uint64_t c = FStar_UInt64_eq_mask(bits_c, (uint64_t)(i1 + (uint32_t)1U));
                  uint64_t *res_j = table + (i1 + (uint32_t)1U) * len1;
                  {
                    uint32_t i;
                    for (i = (uint32_t)0U; i < len1; i++)
                    {
                      uint64_t *os = resM;
                      uint64_t x = (c & res_j[i]) | (~c & resM[i]);
                      os[i] = x;
                    }
                  }
                }
              }
            }
          }
          {
            uint32_t i0;
            for (i0 = (uint32_t)0U; i0 < bBits / (uint32_t)4U; i0++)
            {
              {
                uint32_t i;
                for (i = (uint32_t)0U; i < (uint32_t)4U; i++)
                {
                  Hacl_Bignum_Montgomery_bn_mont_sqr_u64(len1, k1.n, k1.mu, resM, resM);
                }
              }
              {
                uint32_t bk = bBits - bBits % (uint32_t)4U;
                uint64_t mask_l = (uint64_t)16U - (uint64_t)1U;
                uint32_t i1 = (bk - (uint32_t)4U * i0 - (uint32_t)4U) / (uint32_t)64U;
                uint32_t j = (bk - (uint32_t)4U * i0 - (uint32_t)4U) % (uint32_t)64U;
                uint64_t p1 = b[i1] >> j;
                uint64_t ite;
                if (i1 + (uint32_t)1U < bLen && (uint32_t)0U < j)
                {
                  ite = p1 | b[i1 + (uint32_t)1U] << ((uint32_t)64U - j);
                }
                else
                {
                  ite = p1;
                }
                {
                  uint64_t bits_l = ite & mask_l;
                  KRML_CHECK_SIZE(sizeof (uint64_t), len1);
                  {
                    uint64_t a_bits_l[len1];
                    memset(a_bits_l, 0U, len1 * sizeof (uint64_t));
                    memcpy(a_bits_l, table, len1 * sizeof (uint64_t));
                    {
                      uint32_t i2;
                      for (i2 = (uint32_t)0U; i2 < (uint32_t)15U; i2++)
                      {
                        uint64_t c = FStar_UInt64_eq_mask(bits_l, (uint64_t)(i2 + (uint32_t)1U));
                        uint64_t *res_j = table + (i2 + (uint32_t)1U) * len1;
                        {
                          uint32_t i;
                          for (i = (uint32_t)0U; i < len1; i++)
                          {
                            uint64_t *os = a_bits_l;
                            uint64_t x = (c & res_j[i]) | (~c & a_bits_l[i]);
                            os[i] = x;
                          }
                        }
                      }
                    }
                    Hacl_Bignum_Montgomery_bn_mont_mul_u64(len1, k1.n, k1.mu, resM, a_bits_l, resM);
                  }
                }
              }
            }
          }
        }
      }
    }
  }
}

/*
Write `aM ^ b mod n` in `resM`.

  The argument aM and the outparam resM are meant to be `len` limbs in size, i.e. uint64_t[len].
  The argument k is a montgomery context obtained through Hacl_GenericField64_field_init.

  The argument b is a bignum of any size, and bBits is an upper bound on the
  number of significant bits of b. A tighter bound results in faster execution
  time. When in doubt, the number of bits for the bignum size is always a safe
  default, e.g. if b is a 256-bit bignum, bBits should be 256.

  The function is *NOT* constant-time on the argument b. See the
  exp_consttime function for constant-time variant.

  Before calling this function, the caller will need to ensure that the following
  precondition is observed.
  • b < pow2 bBits
*/
void
Hacl_GenericField64_exp_vartime(
  Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 *k,
  uint64_t *aM,
  uint32_t bBits,
  uint64_t *b,
  uint64_t *resM
)
{
  uint32_t len1 = Hacl_GenericField64_field_get_len(k);
  Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 k1 = *k;
  KRML_CHECK_SIZE(sizeof (uint64_t), k1.len);
  {
    uint64_t aMc[k1.len];
    memset(aMc, 0U, k1.len * sizeof (uint64_t));
    memcpy(aMc, aM, k1.len * sizeof (uint64_t));
    if (bBits < (uint32_t)200U)
    {
      Hacl_Bignum_Montgomery_bn_from_mont_u64(len1, k1.n, k1.mu, k1.r2, resM);
      {
        uint32_t i;
        for (i = (uint32_t)0U; i < bBits; i++)
        {
          uint32_t i1 = i / (uint32_t)64U;
          uint32_t j = i % (uint32_t)64U;
          uint64_t tmp = b[i1];
          uint64_t bit = tmp >> j & (uint64_t)1U;
          if (!(bit == (uint64_t)0U))
          {
            Hacl_Bignum_Montgomery_bn_mont_mul_u64(len1, k1.n, k1.mu, resM, aMc, resM);
          }
          Hacl_Bignum_Montgomery_bn_mont_sqr_u64(len1, k1.n, k1.mu, aMc, aMc);
        }
      }
    }
    else
    {
      uint32_t bLen;
      if (bBits == (uint32_t)0U)
      {
        bLen = (uint32_t)1U;
      }
      else
      {
        bLen = (bBits - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U;
      }
      Hacl_Bignum_Montgomery_bn_from_mont_u64(len1, k1.n, k1.mu, k1.r2, resM);
      KRML_CHECK_SIZE(sizeof (uint64_t), (uint32_t)16U * len1);
      {
        uint64_t table[(uint32_t)16U * len1];
        memset(table, 0U, (uint32_t)16U * len1 * sizeof (uint64_t));
        memcpy(table, resM, len1 * sizeof (uint64_t));
        {
          uint64_t *t1 = table + len1;
          memcpy(t1, aMc, len1 * sizeof (uint64_t));
          {
            uint32_t i;
            for (i = (uint32_t)0U; i < (uint32_t)14U; i++)
            {
              uint64_t *t11 = table + (i + (uint32_t)1U) * len1;
              uint64_t *t2 = table + (i + (uint32_t)2U) * len1;
              Hacl_Bignum_Montgomery_bn_mont_mul_u64(len1, k1.n, k1.mu, t11, aMc, t2);
            }
          }
          if (bBits % (uint32_t)4U != (uint32_t)0U)
          {
            uint64_t mask_l = (uint64_t)16U - (uint64_t)1U;
            uint32_t i = bBits / (uint32_t)4U * (uint32_t)4U / (uint32_t)64U;
            uint32_t j = bBits / (uint32_t)4U * (uint32_t)4U % (uint32_t)64U;
            uint64_t p1 = b[i] >> j;
            uint64_t ite;
            if (i + (uint32_t)1U < bLen && (uint32_t)0U < j)
            {
              ite = p1 | b[i + (uint32_t)1U] << ((uint32_t)64U - j);
            }
            else
            {
              ite = p1;
            }
            {
              uint64_t bits_c = ite & mask_l;
              uint32_t bits_l32 = (uint32_t)bits_c;
              uint64_t *a_bits_l = table + bits_l32 * len1;
              memcpy(resM, a_bits_l, len1 * sizeof (uint64_t));
            }
          }
          {
            uint32_t i;
            for (i = (uint32_t)0U; i < bBits / (uint32_t)4U; i++)
            {
              {
                uint32_t i0;
                for (i0 = (uint32_t)0U; i0 < (uint32_t)4U; i0++)
                {
                  Hacl_Bignum_Montgomery_bn_mont_sqr_u64(len1, k1.n, k1.mu, resM, resM);
                }
              }
              {
                uint32_t bk = bBits - bBits % (uint32_t)4U;
                uint64_t mask_l = (uint64_t)16U - (uint64_t)1U;
                uint32_t i1 = (bk - (uint32_t)4U * i - (uint32_t)4U) / (uint32_t)64U;
                uint32_t j = (bk - (uint32_t)4U * i - (uint32_t)4U) % (uint32_t)64U;
                uint64_t p1 = b[i1] >> j;
                uint64_t ite;
                if (i1 + (uint32_t)1U < bLen && (uint32_t)0U < j)
                {
                  ite = p1 | b[i1 + (uint32_t)1U] << ((uint32_t)64U - j);
                }
                else
                {
                  ite = p1;
                }
                {
                  uint64_t bits_l = ite & mask_l;
                  KRML_CHECK_SIZE(sizeof (uint64_t), len1);
                  {
                    uint64_t a_bits_l[len1];
                    memset(a_bits_l, 0U, len1 * sizeof (uint64_t));
                    {
                      uint32_t bits_l32 = (uint32_t)bits_l;
                      uint64_t *a_bits_l1 = table + bits_l32 * len1;
                      memcpy(a_bits_l, a_bits_l1, len1 * sizeof (uint64_t));
                      Hacl_Bignum_Montgomery_bn_mont_mul_u64(len1,
                        k1.n,
                        k1.mu,
                        resM,
                        a_bits_l,
                        resM);
                    }
                  }
                }
              }
            }
          }
        }
      }
    }
  }
}

/*
Write `aM ^ (-1) mod n` in `aInvM`.

  The argument aM and the outparam aInvM are meant to be `len` limbs in size, i.e. uint64_t[len].
  The argument k is a montgomery context obtained through Hacl_GenericField64_field_init.

  Before calling this function, the caller will need to ensure that the following
  preconditions are observed.
  • n is a prime
  • 0 < aM
*/
void
Hacl_GenericField64_inverse(
  Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 *k,
  uint64_t *aM,
  uint64_t *aInvM
)
{
  Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 k1 = *k;
  uint32_t len1 = k1.len;
  KRML_CHECK_SIZE(sizeof (uint64_t), len1);
  {
    uint64_t n2[len1];
    memset(n2, 0U, len1 * sizeof (uint64_t));
    {
      uint64_t
      c0 = Lib_IntTypes_Intrinsics_sub_borrow_u64((uint64_t)0U, k1.n[0U], (uint64_t)2U, n2);
      uint64_t c1;
      if ((uint32_t)1U < len1)
      {
        uint32_t rLen = len1 - (uint32_t)1U;
        uint64_t *a1 = k1.n + (uint32_t)1U;
        uint64_t *res1 = n2 + (uint32_t)1U;
        uint64_t c = c0;
        {
          uint32_t i;
          for (i = (uint32_t)0U; i < rLen / (uint32_t)4U; i++)
          {
            uint64_t t1 = a1[(uint32_t)4U * i];
            uint64_t *res_i0 = res1 + (uint32_t)4U * i;
            c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t1, (uint64_t)0U, res_i0);
            {
              uint64_t t10 = a1[(uint32_t)4U * i + (uint32_t)1U];
              uint64_t *res_i1 = res1 + (uint32_t)4U * i + (uint32_t)1U;
              c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t10, (uint64_t)0U, res_i1);
              {
                uint64_t t11 = a1[(uint32_t)4U * i + (uint32_t)2U];
                uint64_t *res_i2 = res1 + (uint32_t)4U * i + (uint32_t)2U;
                c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t11, (uint64_t)0U, res_i2);
                {
                  uint64_t t12 = a1[(uint32_t)4U * i + (uint32_t)3U];
                  uint64_t *res_i = res1 + (uint32_t)4U * i + (uint32_t)3U;
                  c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t12, (uint64_t)0U, res_i);
                }
              }
            }
          }
        }
        {
          uint32_t i;
          for (i = rLen / (uint32_t)4U * (uint32_t)4U; i < rLen; i++)
          {
            uint64_t t1 = a1[i];
            uint64_t *res_i = res1 + i;
            c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t1, (uint64_t)0U, res_i);
          }
        }
        {
          uint64_t c10 = c;
          c1 = c10;
        }
      }
      else
      {
        c1 = c0;
      }
      Hacl_GenericField64_exp_vartime(k, aM, k1.len * (uint32_t)64U, n2, aInvM);
    }
  }
}