text: /* 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_SHA2_512.h"
  
  static void
  Hacl_Hash_Lib_LoadStore_uint64s_from_be_bytes(uint64_t *output, uint8_t *input, uint32_t len)
  {
    for (uint32_t i = (uint32_t)0U; i < len; 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 len)
  {
    for (uint32_t i = (uint32_t)0U; i < len; 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 *n1 = state + (uint32_t)168U;
    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;
    n1[0U] = (uint64_t)0U;
  }
  
  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 d = hash_0[3U];
      uint64_t e = hash_0[4U];
      uint64_t f1 = hash_0[5U];
      uint64_t g = 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 & g))
        + 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 = d + 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] = g;
    }
    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 len)
  {
    uint8_t blocks[256U] = { 0U };
    uint32_t nb;
    if (len < (uint64_t)112U)
      nb = (uint32_t)1U;
    else
      nb = (uint32_t)2U;
    uint8_t *final_blocks;
    if (len < (uint64_t)112U)
      final_blocks = blocks + (uint32_t)128U;
    else
      final_blocks = blocks;
    memcpy(final_blocks, data, (uint32_t)len * sizeof data[0U]);
    uint64_t n1 = state[168U];
    uint8_t *padding = final_blocks + (uint32_t)len;
    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(len)),
        (uint32_t)3U);
    uint32_t
    pad0len = ((uint32_t)256U - ((uint32_t)len + (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 len)
  {
    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 = len / (uint32_t)128U;
    uint32_t r = len % (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);
  }
  
  uint32_t Hacl_SHA2_512_size_word = (uint32_t)8U;
  
  uint32_t Hacl_SHA2_512_size_hash_w = (uint32_t)8U;
  
  uint32_t Hacl_SHA2_512_size_block_w = (uint32_t)16U;
  
  uint32_t Hacl_SHA2_512_size_hash = (uint32_t)64U;
  
  uint32_t Hacl_SHA2_512_size_block = (uint32_t)128U;
  
  uint32_t Hacl_SHA2_512_size_k_w = (uint32_t)80U;
  
  uint32_t Hacl_SHA2_512_size_ws_w = (uint32_t)80U;
  
  uint32_t Hacl_SHA2_512_size_whash_w = (uint32_t)8U;
  
  uint32_t Hacl_SHA2_512_size_count_w = (uint32_t)1U;
  
  uint32_t Hacl_SHA2_512_size_len_8 = (uint32_t)16U;
  
  uint32_t Hacl_SHA2_512_size_state = (uint32_t)169U;
  
  uint32_t Hacl_SHA2_512_pos_k_w = (uint32_t)0U;
  
  uint32_t Hacl_SHA2_512_pos_ws_w = (uint32_t)80U;
  
  uint32_t Hacl_SHA2_512_pos_whash_w = (uint32_t)160U;
  
  uint32_t Hacl_SHA2_512_pos_count_w = (uint32_t)168U;
  
  void Hacl_SHA2_512_init(uint64_t *state)
  {
    Hacl_Impl_SHA2_512_init(state);
  }
  
  void Hacl_SHA2_512_update(uint64_t *state, uint8_t *data)
  {
    Hacl_Impl_SHA2_512_update(state, data);
  }
  
  void Hacl_SHA2_512_update_multi(uint64_t *state, uint8_t *data, uint32_t n1)
  {
    Hacl_Impl_SHA2_512_update_multi(state, data, n1);
  }
  
  void Hacl_SHA2_512_update_last(uint64_t *state, uint8_t *data, uint64_t len)
  {
    Hacl_Impl_SHA2_512_update_last(state, data, len);
  }
  
  void Hacl_SHA2_512_finish(uint64_t *state, uint8_t *hash1)
  {
    Hacl_Impl_SHA2_512_finish(state, hash1);
  }
  
  void Hacl_SHA2_512_hash(uint8_t *hash1, uint8_t *input, uint32_t len)
  {
    Hacl_Impl_SHA2_512_hash(hash1, input, len);
  }
  
  