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

static inline void add_mod_n(uint64_t *n, uint64_t *a, uint64_t *b, uint64_t *res)
{
  uint64_t c2 = (uint64_t)0U;
  uint64_t c0;
  {
    uint32_t i;
    for (i = (uint32_t)0U; i < (uint32_t)8U; i++)
    {
      uint64_t t1 = a[(uint32_t)4U * i];
      uint64_t t20 = b[(uint32_t)4U * i];
      uint64_t *res_i0 = res + (uint32_t)4U * i;
      c2 = Lib_IntTypes_Intrinsics_add_carry_u64(c2, t1, t20, res_i0);
      {
        uint64_t t10 = a[(uint32_t)4U * i + (uint32_t)1U];
        uint64_t t21 = b[(uint32_t)4U * i + (uint32_t)1U];
        uint64_t *res_i1 = res + (uint32_t)4U * i + (uint32_t)1U;
        c2 = Lib_IntTypes_Intrinsics_add_carry_u64(c2, t10, t21, res_i1);
        {
          uint64_t t11 = a[(uint32_t)4U * i + (uint32_t)2U];
          uint64_t t22 = b[(uint32_t)4U * i + (uint32_t)2U];
          uint64_t *res_i2 = res + (uint32_t)4U * i + (uint32_t)2U;
          c2 = Lib_IntTypes_Intrinsics_add_carry_u64(c2, t11, t22, res_i2);
          {
            uint64_t t12 = a[(uint32_t)4U * i + (uint32_t)3U];
            uint64_t t2 = b[(uint32_t)4U * i + (uint32_t)3U];
            uint64_t *res_i = res + (uint32_t)4U * i + (uint32_t)3U;
            c2 = Lib_IntTypes_Intrinsics_add_carry_u64(c2, t12, t2, res_i);
          }
        }
      }
    }
  }
  {
    uint32_t i;
    for (i = (uint32_t)32U; i < (uint32_t)32U; i++)
    {
      uint64_t t1 = a[i];
      uint64_t t2 = b[i];
      uint64_t *res_i = res + i;
      c2 = Lib_IntTypes_Intrinsics_add_carry_u64(c2, t1, t2, res_i);
    }
  }
  c0 = c2;
  {
    uint64_t tmp[32U] = { 0U };
    uint64_t c3 = (uint64_t)0U;
    uint64_t c1;
    uint64_t c;
    {
      uint32_t i;
      for (i = (uint32_t)0U; i < (uint32_t)8U; i++)
      {
        uint64_t t1 = res[(uint32_t)4U * i];
        uint64_t t20 = n[(uint32_t)4U * i];
        uint64_t *res_i0 = tmp + (uint32_t)4U * i;
        c3 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c3, t1, t20, res_i0);
        {
          uint64_t t10 = res[(uint32_t)4U * i + (uint32_t)1U];
          uint64_t t21 = n[(uint32_t)4U * i + (uint32_t)1U];
          uint64_t *res_i1 = tmp + (uint32_t)4U * i + (uint32_t)1U;
          c3 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c3, t10, t21, res_i1);
          {
            uint64_t t11 = res[(uint32_t)4U * i + (uint32_t)2U];
            uint64_t t22 = n[(uint32_t)4U * i + (uint32_t)2U];
            uint64_t *res_i2 = tmp + (uint32_t)4U * i + (uint32_t)2U;
            c3 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c3, t11, t22, res_i2);
            {
              uint64_t t12 = res[(uint32_t)4U * i + (uint32_t)3U];
              uint64_t t2 = n[(uint32_t)4U * i + (uint32_t)3U];
              uint64_t *res_i = tmp + (uint32_t)4U * i + (uint32_t)3U;
              c3 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c3, t12, t2, res_i);
            }
          }
        }
      }
    }
    {
      uint32_t i;
      for (i = (uint32_t)32U; i < (uint32_t)32U; i++)
      {
        uint64_t t1 = res[i];
        uint64_t t2 = n[i];
        uint64_t *res_i = tmp + i;
        c3 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c3, t1, t2, res_i);
      }
    }
    c1 = c3;
    c = c0 - c1;
    {
      uint32_t i;
      for (i = (uint32_t)0U; i < (uint32_t)32U; i++)
      {
        uint64_t *os = res;
        uint64_t x = (c & res[i]) | (~c & tmp[i]);
        os[i] = x;
      }
    }
  }
}

static inline void mul(uint64_t *a, uint64_t *b, uint64_t *res)
{
  uint64_t tmp[128U] = { 0U };
  Hacl_Bignum_Karatsuba_bn_karatsuba_mul_uint64((uint32_t)32U, a, b, tmp, res);
}

static inline void precomp(uint32_t nBits, uint64_t *n, uint64_t *res)
{
  uint32_t i0;
  uint32_t j;
  uint32_t i;
  memset(res, 0U, (uint32_t)32U * sizeof (uint64_t));
  i0 = nBits / (uint32_t)64U;
  j = nBits % (uint32_t)64U;
  res[i0] = res[i0] | (uint64_t)1U << j;
  for (i = (uint32_t)0U; i < (uint32_t)4096U - nBits; i++)
  {
    add_mod_n(n, res, res, res);
  }
}

static inline void reduction(uint64_t *n, uint64_t nInv, uint64_t *c, uint64_t *res)
{
  uint64_t c0 = (uint64_t)0U;
  uint64_t c01;
  {
    uint32_t i0;
    for (i0 = (uint32_t)0U; i0 < (uint32_t)32U; i0++)
    {
      uint64_t qj = nInv * c[i0];
      uint64_t *res_j0 = c + i0;
      uint64_t c1 = (uint64_t)0U;
      {
        uint32_t i;
        for (i = (uint32_t)0U; i < (uint32_t)8U; i++)
        {
          uint64_t a_i = n[(uint32_t)4U * i];
          uint64_t *res_i0 = res_j0 + (uint32_t)4U * i;
          c1 = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, qj, c1, res_i0);
          {
            uint64_t a_i0 = n[(uint32_t)4U * i + (uint32_t)1U];
            uint64_t *res_i1 = res_j0 + (uint32_t)4U * i + (uint32_t)1U;
            c1 = Hacl_Bignum_Base_mul_wide_add2_u64(a_i0, qj, c1, res_i1);
            {
              uint64_t a_i1 = n[(uint32_t)4U * i + (uint32_t)2U];
              uint64_t *res_i2 = res_j0 + (uint32_t)4U * i + (uint32_t)2U;
              c1 = Hacl_Bignum_Base_mul_wide_add2_u64(a_i1, qj, c1, res_i2);
              {
                uint64_t a_i2 = n[(uint32_t)4U * i + (uint32_t)3U];
                uint64_t *res_i = res_j0 + (uint32_t)4U * i + (uint32_t)3U;
                c1 = Hacl_Bignum_Base_mul_wide_add2_u64(a_i2, qj, c1, res_i);
              }
            }
          }
        }
      }
      {
        uint32_t i;
        for (i = (uint32_t)32U; i < (uint32_t)32U; i++)
        {
          uint64_t a_i = n[i];
          uint64_t *res_i = res_j0 + i;
          c1 = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, qj, c1, res_i);
        }
      }
      {
        uint64_t r = c1;
        uint64_t c10 = r;
        uint64_t *resb = c + (uint32_t)32U + i0;
        uint64_t res_j = c[(uint32_t)32U + i0];
        c0 = Lib_IntTypes_Intrinsics_add_carry_u64(c0, c10, res_j, resb);
      }
    }
  }
  memcpy(res, c + (uint32_t)32U, (uint32_t)32U * sizeof (uint64_t));
  c01 = c0;
  {
    uint64_t tmp[32U] = { 0U };
    uint64_t c10 = (uint64_t)0U;
    uint64_t c1;
    uint64_t c2;
    {
      uint32_t i;
      for (i = (uint32_t)0U; i < (uint32_t)8U; i++)
      {
        uint64_t t1 = res[(uint32_t)4U * i];
        uint64_t t20 = n[(uint32_t)4U * i];
        uint64_t *res_i0 = tmp + (uint32_t)4U * i;
        c10 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c10, t1, t20, res_i0);
        {
          uint64_t t10 = res[(uint32_t)4U * i + (uint32_t)1U];
          uint64_t t21 = n[(uint32_t)4U * i + (uint32_t)1U];
          uint64_t *res_i1 = tmp + (uint32_t)4U * i + (uint32_t)1U;
          c10 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c10, t10, t21, res_i1);
          {
            uint64_t t11 = res[(uint32_t)4U * i + (uint32_t)2U];
            uint64_t t22 = n[(uint32_t)4U * i + (uint32_t)2U];
            uint64_t *res_i2 = tmp + (uint32_t)4U * i + (uint32_t)2U;
            c10 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c10, t11, t22, res_i2);
            {
              uint64_t t12 = res[(uint32_t)4U * i + (uint32_t)3U];
              uint64_t t2 = n[(uint32_t)4U * i + (uint32_t)3U];
              uint64_t *res_i = tmp + (uint32_t)4U * i + (uint32_t)3U;
              c10 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c10, t12, t2, res_i);
            }
          }
        }
      }
    }
    {
      uint32_t i;
      for (i = (uint32_t)32U; i < (uint32_t)32U; i++)
      {
        uint64_t t1 = res[i];
        uint64_t t2 = n[i];
        uint64_t *res_i = tmp + i;
        c10 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c10, t1, t2, res_i);
      }
    }
    c1 = c10;
    c2 = c01 - c1;
    {
      uint32_t i;
      for (i = (uint32_t)0U; i < (uint32_t)32U; i++)
      {
        uint64_t *os = res;
        uint64_t x = (c2 & res[i]) | (~c2 & tmp[i]);
        os[i] = x;
      }
    }
  }
}

static inline void
mont_mul(uint64_t *n, uint64_t nInv_u64, uint64_t *aM, uint64_t *bM, uint64_t *resM)
{
  uint64_t c[64U] = { 0U };
  uint64_t tmp[128U] = { 0U };
  Hacl_Bignum_Karatsuba_bn_karatsuba_mul_uint64((uint32_t)32U, aM, bM, tmp, c);
  reduction(n, nInv_u64, c, resM);
}

static inline void mont_sqr(uint64_t *n, uint64_t nInv_u64, uint64_t *aM, uint64_t *resM)
{
  uint64_t c[64U] = { 0U };
  uint64_t tmp[128U] = { 0U };
  Hacl_Bignum_Karatsuba_bn_karatsuba_sqr_uint64((uint32_t)32U, aM, tmp, c);
  reduction(n, nInv_u64, c, resM);
}

static inline void
mod_exp_raw_precompr2(
  uint64_t *n,
  uint64_t *a,
  uint32_t bBits,
  uint64_t *b,
  uint64_t *r2,
  uint64_t *res
)
{
  uint64_t nInv = Hacl_Bignum_ModInvLimb_mod_inv_uint64(n[0U]);
  uint64_t aM[32U] = { 0U };
  uint64_t accM[32U] = { 0U };
  uint64_t c0[64U] = { 0U };
  mul(a, r2, c0);
  reduction(n, nInv, c0, aM);
  {
    uint64_t one[32U] = { 0U };
    memset(one, 0U, (uint32_t)32U * sizeof (uint64_t));
    one[0U] = (uint64_t)1U;
    {
      uint64_t c[64U] = { 0U };
      mul(one, r2, c);
      reduction(n, nInv, c, accM);
      {
        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))
          {
            mont_mul(n, nInv, accM, aM, accM);
          }
          mont_sqr(n, nInv, aM, aM);
        }
      }
      {
        uint64_t tmp[64U] = { 0U };
        memcpy(tmp, accM, (uint32_t)32U * sizeof (uint64_t));
        reduction(n, nInv, tmp, res);
      }
    }
  }
}

static inline void
mod_exp_fw_ct_precompr2(
  uint64_t *n,
  uint64_t *a,
  uint32_t bBits,
  uint64_t *b,
  uint32_t l,
  uint64_t *r2,
  uint64_t *res
)
{
  uint32_t bLen = (bBits - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U;
  uint64_t nInv = Hacl_Bignum_ModInvLimb_mod_inv_uint64(n[0U]);
  uint64_t aM[32U] = { 0U };
  uint64_t accM[32U] = { 0U };
  uint64_t c0[64U] = { 0U };
  mul(a, r2, c0);
  reduction(n, nInv, c0, aM);
  {
    uint64_t one[32U] = { 0U };
    memset(one, 0U, (uint32_t)32U * sizeof (uint64_t));
    one[0U] = (uint64_t)1U;
    {
      uint64_t c2[64U] = { 0U };
      mul(one, r2, c2);
      reduction(n, nInv, c2, accM);
      {
        uint32_t table_len = (uint32_t)1U << l;
        KRML_CHECK_SIZE(sizeof (uint64_t), table_len * (uint32_t)32U);
        {
          uint64_t table[table_len * (uint32_t)32U];
          memset(table, 0U, table_len * (uint32_t)32U * sizeof (uint64_t));
          {
            uint64_t *t1;
            memcpy(table, accM, (uint32_t)32U * sizeof (uint64_t));
            t1 = table + (uint32_t)32U;
            memcpy(t1, aM, (uint32_t)32U * sizeof (uint64_t));
            {
              uint32_t i;
              for (i = (uint32_t)0U; i < table_len - (uint32_t)2U; i++)
              {
                uint64_t *t11 = table + (i + (uint32_t)1U) * (uint32_t)32U;
                uint64_t *t2 = table + (i + (uint32_t)2U) * (uint32_t)32U;
                mont_mul(n, nInv, t11, aM, t2);
              }
            }
            {
              uint32_t i0;
              for (i0 = (uint32_t)0U; i0 < bBits / l; i0++)
              {
                uint64_t mask_l = ((uint64_t)1U << l) - (uint64_t)1U;
                uint32_t i1 = (bBits - l * i0 - l) / (uint32_t)64U;
                uint32_t j = (bBits - l * i0 - l) % (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;
                  uint64_t a_bits_l[32U] = { 0U };
                  memcpy(a_bits_l, table, (uint32_t)32U * sizeof (uint64_t));
                  {
                    uint32_t i2;
                    for (i2 = (uint32_t)0U; i2 < table_len - (uint32_t)1U; 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) * (uint32_t)32U;
                      {
                        uint32_t i;
                        for (i = (uint32_t)0U; i < (uint32_t)32U; i++)
                        {
                          uint64_t *os = a_bits_l;
                          uint64_t x = (c & res_j[i]) | (~c & a_bits_l[i]);
                          os[i] = x;
                        }
                      }
                    }
                  }
                  {
                    uint32_t i;
                    for (i = (uint32_t)0U; i < l; i++)
                    {
                      mont_sqr(n, nInv, accM, accM);
                    }
                  }
                  mont_mul(n, nInv, accM, a_bits_l, accM);
                }
              }
            }
            if (!(bBits % l == (uint32_t)0U))
            {
              uint32_t c = bBits % l;
              uint32_t c10 = bBits % l;
              uint64_t mask_l = ((uint64_t)1U << c10) - (uint64_t)1U;
              uint32_t i0 = (uint32_t)0U;
              uint32_t j = (uint32_t)0U;
              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;
                uint64_t bits_c0 = bits_c;
                uint64_t a_bits_c[32U] = { 0U };
                memcpy(a_bits_c, table, (uint32_t)32U * sizeof (uint64_t));
                {
                  uint32_t i1;
                  for (i1 = (uint32_t)0U; i1 < table_len - (uint32_t)1U; i1++)
                  {
                    uint64_t c1 = FStar_UInt64_eq_mask(bits_c0, (uint64_t)(i1 + (uint32_t)1U));
                    uint64_t *res_j = table + (i1 + (uint32_t)1U) * (uint32_t)32U;
                    {
                      uint32_t i;
                      for (i = (uint32_t)0U; i < (uint32_t)32U; i++)
                      {
                        uint64_t *os = a_bits_c;
                        uint64_t x = (c1 & res_j[i]) | (~c1 & a_bits_c[i]);
                        os[i] = x;
                      }
                    }
                  }
                }
                {
                  uint32_t i;
                  for (i = (uint32_t)0U; i < c; i++)
                  {
                    mont_sqr(n, nInv, accM, accM);
                  }
                }
                mont_mul(n, nInv, accM, a_bits_c, accM);
              }
            }
            {
              uint64_t tmp[64U] = { 0U };
              memcpy(tmp, accM, (uint32_t)32U * sizeof (uint64_t));
              reduction(n, nInv, tmp, res);
            }
          }
        }
      }
    }
  }
}

static inline bool load_pkey(uint32_t eBits, uint8_t *nb, uint8_t *eb, uint64_t *pkey)
{
  uint32_t nbLen = ((uint32_t)2048U - (uint32_t)1U) / (uint32_t)8U + (uint32_t)1U;
  uint32_t ebLen = (eBits - (uint32_t)1U) / (uint32_t)8U + (uint32_t)1U;
  uint32_t nLen = ((uint32_t)2048U - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U;
  uint64_t *n = pkey;
  uint64_t *r2 = pkey + nLen;
  uint64_t *e = pkey + nLen + nLen;
  uint64_t m0;
  uint64_t m1;
  uint64_t m;
  Hacl_Bignum_Convert_bn_from_bytes_be_uint64(nbLen, nb, n);
  precomp((uint32_t)2047U, n, r2);
  Hacl_Bignum_Convert_bn_from_bytes_be_uint64(ebLen, eb, e);
  m0 = Hacl_Impl_RSAPSS_Keys_check_modulus_u64((uint32_t)2048U, n);
  m1 = Hacl_Impl_RSAPSS_Keys_check_exponent_u64(eBits, e);
  m = m0 & m1;
  return m == (uint64_t)0xFFFFFFFFFFFFFFFFU;
}

static inline bool
load_skey(
  uint32_t eBits,
  uint32_t dBits,
  uint8_t *nb,
  uint8_t *eb,
  uint8_t *db,
  uint64_t *skey
)
{
  uint32_t dbLen = (dBits - (uint32_t)1U) / (uint32_t)8U + (uint32_t)1U;
  uint32_t nLen = ((uint32_t)2048U - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U;
  uint32_t eLen = (eBits - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U;
  uint32_t pkeyLen = nLen + nLen + eLen;
  uint64_t *pkey = skey;
  uint64_t *d = skey + pkeyLen;
  bool b = load_pkey(eBits, nb, eb, pkey);
  uint64_t m1;
  Hacl_Bignum_Convert_bn_from_bytes_be_uint64(dbLen, db, d);
  m1 = Hacl_Impl_RSAPSS_Keys_check_exponent_u64(dBits, d);
  return b && m1 == (uint64_t)0xFFFFFFFFFFFFFFFFU;
}

bool
Hacl_RSAPSS2048_SHA256_rsapss_sign(
  uint32_t eBits,
  uint32_t dBits,
  uint64_t *skey,
  uint32_t sLen,
  uint8_t *salt,
  uint32_t msgLen,
  uint8_t *msg,
  uint8_t *sgnt
)
{
  uint32_t hLen = Hacl_Impl_RSAPSS_MGF_hash_len(Spec_Hash_Definitions_SHA2_256);
  bool
  b =
    sLen
    <= (uint32_t)0xffffffffU - hLen - (uint32_t)8U
    && sLen + hLen + (uint32_t)2U <= ((uint32_t)2047U - (uint32_t)1U) / (uint32_t)8U + (uint32_t)1U;
  if (b)
  {
    uint32_t nLen = ((uint32_t)2048U - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U;
    KRML_CHECK_SIZE(sizeof (uint64_t), nLen);
    {
      uint64_t m[nLen];
      memset(m, 0U, nLen * sizeof (uint64_t));
      {
        uint32_t emBits = (uint32_t)2047U;
        uint32_t emLen = (emBits - (uint32_t)1U) / (uint32_t)8U + (uint32_t)1U;
        KRML_CHECK_SIZE(sizeof (uint8_t), emLen);
        {
          uint8_t em[emLen];
          memset(em, 0U, emLen * sizeof (uint8_t));
          Hacl_Impl_RSAPSS_Padding_pss_encode(Spec_Hash_Definitions_SHA2_256,
            sLen,
            salt,
            msgLen,
            msg,
            emBits,
            em);
          Hacl_Bignum_Convert_bn_from_bytes_be_uint64(emLen, em, m);
          {
            uint32_t nLen1 = ((uint32_t)2048U - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U;
            uint32_t k = ((uint32_t)2048U - (uint32_t)1U) / (uint32_t)8U + (uint32_t)1U;
            KRML_CHECK_SIZE(sizeof (uint64_t), nLen1);
            {
              uint64_t s[nLen1];
              memset(s, 0U, nLen1 * sizeof (uint64_t));
              KRML_CHECK_SIZE(sizeof (uint64_t), nLen1);
              {
                uint64_t m_[nLen1];
                memset(m_, 0U, nLen1 * sizeof (uint64_t));
                {
                  uint32_t nLen2 = ((uint32_t)2048U - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U;
                  uint32_t eLen = (eBits - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U;
                  uint64_t *n = skey;
                  uint64_t *r2 = skey + nLen2;
                  uint64_t *e = skey + nLen2 + nLen2;
                  uint64_t *d = skey + nLen2 + nLen2 + eLen;
                  mod_exp_fw_ct_precompr2(n, m, dBits, d, (uint32_t)4U, r2, s);
                  mod_exp_raw_precompr2(n, s, eBits, e, r2, m_);
                  {
                    uint64_t mask = (uint64_t)0xFFFFFFFFFFFFFFFFU;
                    {
                      uint32_t i;
                      for (i = (uint32_t)0U; i < nLen2; i++)
                      {
                        uint64_t uu____0 = FStar_UInt64_eq_mask(m[i], m_[i]);
                        mask = uu____0 & mask;
                      }
                    }
                    {
                      uint64_t mask1 = mask;
                      uint64_t eq_m = mask1;
                      {
                        uint32_t i;
                        for (i = (uint32_t)0U; i < nLen2; i++)
                        {
                          uint64_t *os = s;
                          uint64_t x = s[i];
                          uint64_t x0 = eq_m & x;
                          os[i] = x0;
                        }
                      }
                      {
                        bool eq_b = eq_m == (uint64_t)0xFFFFFFFFFFFFFFFFU;
                        Hacl_Bignum_Convert_bn_to_bytes_be_uint64(k, s, sgnt);
                        {
                          bool eq_b0 = eq_b;
                          return eq_b0;
                        }
                      }
                    }
                  }
                }
              }
            }
          }
        }
      }
    }
  }
  return false;
}

bool
Hacl_RSAPSS2048_SHA256_rsapss_verify(
  uint32_t eBits,
  uint64_t *pkey,
  uint32_t sLen,
  uint32_t k,
  uint8_t *sgnt,
  uint32_t msgLen,
  uint8_t *msg
)
{
  uint32_t hLen = Hacl_Impl_RSAPSS_MGF_hash_len(Spec_Hash_Definitions_SHA2_256);
  bool
  b =
    sLen
    <= (uint32_t)0xffffffffU - hLen - (uint32_t)8U
    && k == ((uint32_t)2048U - (uint32_t)1U) / (uint32_t)8U + (uint32_t)1U;
  if (b)
  {
    uint32_t nLen = ((uint32_t)2048U - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U;
    KRML_CHECK_SIZE(sizeof (uint64_t), nLen);
    {
      uint64_t m[nLen];
      memset(m, 0U, nLen * sizeof (uint64_t));
      {
        uint32_t nLen1 = ((uint32_t)2048U - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U;
        uint32_t k1 = ((uint32_t)2048U - (uint32_t)1U) / (uint32_t)8U + (uint32_t)1U;
        KRML_CHECK_SIZE(sizeof (uint64_t), nLen1);
        {
          uint64_t s[nLen1];
          memset(s, 0U, nLen1 * sizeof (uint64_t));
          Hacl_Bignum_Convert_bn_from_bytes_be_uint64(k1, sgnt, s);
          {
            uint32_t nLen2 = ((uint32_t)2048U - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U;
            uint64_t *n = pkey;
            uint64_t *r2 = pkey + nLen2;
            uint64_t *e = pkey + nLen2 + nLen2;
            uint64_t acc = (uint64_t)0U;
            {
              uint32_t i;
              for (i = (uint32_t)0U; i < nLen2; i++)
              {
                uint64_t beq = FStar_UInt64_eq_mask(s[i], n[i]);
                uint64_t blt = ~FStar_UInt64_gte_mask(s[i], n[i]);
                acc =
                  (beq & acc)
                  | (~beq & ((blt & (uint64_t)0xFFFFFFFFFFFFFFFFU) | (~blt & (uint64_t)0U)));
              }
            }
            {
              uint64_t mask = acc;
              bool res;
              if (mask == (uint64_t)0xFFFFFFFFFFFFFFFFU)
              {
                mod_exp_raw_precompr2(n, s, eBits, e, r2, m);
                {
                  bool ite;
                  if (!((uint32_t)7U == (uint32_t)0U))
                  {
                    ite = true;
                  }
                  else
                  {
                    uint32_t i = (uint32_t)31U;
                    uint32_t j = (uint32_t)63U;
                    uint64_t tmp = m[i];
                    uint64_t get_bit = tmp >> j & (uint64_t)1U;
                    ite = get_bit == (uint64_t)0U;
                  }
                  if (ite)
                  {
                    res = true;
                  }
                  else
                  {
                    res = false;
                  }
                }
              }
              else
              {
                res = false;
              }
              {
                bool b1 = res;
                bool b10 = b1;
                if (b10)
                {
                  uint32_t emBits = (uint32_t)2047U;
                  uint32_t emLen = (emBits - (uint32_t)1U) / (uint32_t)8U + (uint32_t)1U;
                  KRML_CHECK_SIZE(sizeof (uint8_t), emLen);
                  {
                    uint8_t em[emLen];
                    memset(em, 0U, emLen * sizeof (uint8_t));
                    {
                      uint64_t *m1 = m;
                      Hacl_Bignum_Convert_bn_to_bytes_be_uint64(emLen, m1, em);
                      {
                        bool
                        res0 =
                          Hacl_Impl_RSAPSS_Padding_pss_verify(Spec_Hash_Definitions_SHA2_256,
                            sLen,
                            msgLen,
                            msg,
                            emBits,
                            em);
                        return res0;
                      }
                    }
                  }
                }
                return false;
              }
            }
          }
        }
      }
    }
  }
  return false;
}

uint64_t *Hacl_RSAPSS2048_SHA256_new_rsapss_load_pkey(uint32_t eBits, uint8_t *nb, uint8_t *eb)
{
  uint32_t nLen = ((uint32_t)2048U - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U;
  uint32_t eLen = (eBits - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U;
  uint32_t pkeyLen = nLen + nLen + eLen;
  uint32_t nLen1 = ((uint32_t)2048U - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U;
  uint32_t eLen1 = (eBits - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U;
  if
  (
    !((uint32_t)1U
    < (uint32_t)2048U
    && (uint32_t)0U < eBits
    && nLen1 <= (uint32_t)33554431U
    && eLen1 <= (uint32_t)67108863U
    && nLen1 + nLen1 <= (uint32_t)0xffffffffU - eLen1)
  )
  {
    return NULL;
  }
  KRML_CHECK_SIZE(sizeof (uint64_t), pkeyLen);
  {
    uint64_t *pkey = KRML_HOST_CALLOC(pkeyLen, sizeof (uint64_t));
    if (pkey == NULL)
    {
      return pkey;
    }
    {
      uint64_t *pkey1 = pkey;
      uint64_t *pkey2 = pkey1;
      bool b = load_pkey(eBits, nb, eb, pkey2);
      if (b)
      {
        return pkey2;
      }
      return NULL;
    }
  }
}

uint64_t
*Hacl_RSAPSS2048_SHA256_new_rsapss_load_skey(
  uint32_t eBits,
  uint32_t dBits,
  uint8_t *nb,
  uint8_t *eb,
  uint8_t *db
)
{
  uint32_t nLen = ((uint32_t)2048U - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U;
  uint32_t eLen = (eBits - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U;
  uint32_t dLen = (dBits - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U;
  uint32_t skeyLen = nLen + nLen + eLen + dLen;
  uint32_t nLen1 = ((uint32_t)2048U - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U;
  uint32_t eLen1 = (eBits - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U;
  uint32_t dLen1 = (dBits - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U;
  uint32_t nLen2 = ((uint32_t)2048U - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U;
  uint32_t eLen2 = (eBits - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U;
  if
  (
    !((uint32_t)1U
    < (uint32_t)2048U
    && (uint32_t)0U < eBits
    && nLen2 <= (uint32_t)33554431U
    && eLen2 <= (uint32_t)67108863U
    && nLen2 + nLen2 <= (uint32_t)0xffffffffU - eLen2
    && (uint32_t)0U < dBits
    && dLen1 <= (uint32_t)67108863U
    && (uint32_t)2U * nLen1 <= (uint32_t)0xffffffffU - eLen1 - dLen1)
  )
  {
    return NULL;
  }
  KRML_CHECK_SIZE(sizeof (uint64_t), skeyLen);
  {
    uint64_t *skey = KRML_HOST_CALLOC(skeyLen, sizeof (uint64_t));
    if (skey == NULL)
    {
      return skey;
    }
    {
      uint64_t *skey1 = skey;
      uint64_t *skey2 = skey1;
      bool b = load_skey(eBits, dBits, nb, eb, db, skey2);
      if (b)
      {
        return skey2;
      }
      return NULL;
    }
  }
}

bool
Hacl_RSAPSS2048_SHA256_rsapss_skey_sign(
  uint32_t eBits,
  uint32_t dBits,
  uint8_t *nb,
  uint8_t *eb,
  uint8_t *db,
  uint32_t sLen,
  uint8_t *salt,
  uint32_t msgLen,
  uint8_t *msg,
  uint8_t *sgnt
)
{
  KRML_CHECK_SIZE(sizeof (uint64_t),
    (uint32_t)2U
    * (((uint32_t)2048U - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U)
    + (eBits - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U
    + (dBits - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U);
  {
    uint64_t
    skey[(uint32_t)2U
    * (((uint32_t)2048U - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U)
    + (eBits - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U
    + (dBits - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U];
    memset(skey,
      0U,
      ((uint32_t)2U
      * (((uint32_t)2048U - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U)
      + (eBits - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U
      + (dBits - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U)
      * sizeof (uint64_t));
    {
      bool b = load_skey(eBits, dBits, nb, eb, db, skey);
      if (b)
      {
        return
          Hacl_RSAPSS2048_SHA256_rsapss_sign(eBits,
            dBits,
            skey,
            sLen,
            salt,
            msgLen,
            msg,
            sgnt);
      }
      return false;
    }
  }
}

bool
Hacl_RSAPSS2048_SHA256_rsapss_pkey_verify(
  uint32_t eBits,
  uint8_t *nb,
  uint8_t *eb,
  uint32_t sLen,
  uint32_t k,
  uint8_t *sgnt,
  uint32_t msgLen,
  uint8_t *msg
)
{
  KRML_CHECK_SIZE(sizeof (uint64_t),
    (uint32_t)2U
    * (((uint32_t)2048U - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U)
    + (eBits - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U);
  {
    uint64_t
    pkey[(uint32_t)2U
    * (((uint32_t)2048U - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U)
    + (eBits - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U];
    memset(pkey,
      0U,
      ((uint32_t)2U
      * (((uint32_t)2048U - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U)
      + (eBits - (uint32_t)1U) / (uint32_t)64U + (uint32_t)1U)
      * sizeof (uint64_t));
    {
      bool b = load_pkey(eBits, nb, eb, pkey);
      if (b)
      {
        return Hacl_RSAPSS2048_SHA256_rsapss_verify(eBits, pkey, sLen, k, sgnt, msgLen, msg);
      }
      return false;
    }
  }
}