text: /* This file was generated by KreMLin <https, 0x//github.com/FStarLang/kremlin>
   * KreMLin invocation, 0x /home/jonathan/Code/everest/kremlin/krml -I /home/jonathan/Code/everest/hacl-star/code/lib/kremlin -I /home/jonathan/Code/everest/kremlin/kremlib/compat -I /home/jonathan/Code/everest/hacl-star/specs -I /home/jonathan/Code/everest/hacl-star/specs/old -I . -ccopt -march=native -verbose -ldopt -flto -I ../bignum -tmpdir poly-c -fparentheses -skip-compilation -add-include "kremlib.h" -minimal -bundle Hacl_Poly1305_64=* poly-c/out.krml -o poly-c/Hacl_Poly1305_64.c
   * F* version, 0x 8f0ddba4
   * KreMLin version, 0x 9768dccd
   */
  
  #include "Hacl_Poly1305_64.h"
  
  extern FStar_UInt128_uint128
  FStar_UInt128_add(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1);
  
  extern FStar_UInt128_uint128
  FStar_UInt128_add_mod(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1);
  
  extern FStar_UInt128_uint128
  FStar_UInt128_logand(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1);
  
  extern FStar_UInt128_uint128
  FStar_UInt128_logor(FStar_UInt128_uint128 x0, FStar_UInt128_uint128 x1);
  
  extern FStar_UInt128_uint128 FStar_UInt128_shift_left(FStar_UInt128_uint128 x0, uint32_t x1);
  
  extern FStar_UInt128_uint128 FStar_UInt128_shift_right(FStar_UInt128_uint128 x0, uint32_t x1);
  
  extern FStar_UInt128_uint128 FStar_UInt128_uint64_to_uint128(uint64_t x0);
  
  extern uint64_t FStar_UInt128_uint128_to_uint64(FStar_UInt128_uint128 x0);
  
  extern FStar_UInt128_uint128 FStar_UInt128_mul_wide(uint64_t x0, uint64_t x1);
  
  extern uint64_t FStar_UInt64_eq_mask(uint64_t x0, uint64_t x1);
  
  extern uint64_t FStar_UInt64_gte_mask(uint64_t x0, uint64_t x1);
  
  inline static void
  Hacl_Bignum_Fproduct_copy_from_wide_(uint64_t *output, FStar_UInt128_uint128 *input)
  {
    for (uint32_t i = (uint32_t)0U; i < (uint32_t)3U; i = i + (uint32_t)1U)
    {
      FStar_UInt128_uint128 xi = input[i];
      output[i] = FStar_UInt128_uint128_to_uint64(xi);
    }
  }
  
  inline static void
  Hacl_Bignum_Fproduct_sum_scalar_multiplication_(
    FStar_UInt128_uint128 *output,
    uint64_t *input,
    uint64_t s
  )
  {
    for (uint32_t i = (uint32_t)0U; i < (uint32_t)3U; i = i + (uint32_t)1U)
    {
      FStar_UInt128_uint128 xi = output[i];
      uint64_t yi = input[i];
      output[i] = FStar_UInt128_add_mod(xi, FStar_UInt128_mul_wide(yi, s));
    }
  }
  
  inline static void Hacl_Bignum_Fproduct_carry_wide_(FStar_UInt128_uint128 *tmp)
  {
    for (uint32_t i = (uint32_t)0U; i < (uint32_t)2U; i = i + (uint32_t)1U)
    {
      uint32_t ctr = i;
      FStar_UInt128_uint128 tctr = tmp[ctr];
      FStar_UInt128_uint128 tctrp1 = tmp[ctr + (uint32_t)1U];
      uint64_t r0 = FStar_UInt128_uint128_to_uint64(tctr) & (uint64_t)0xfffffffffffU;
      FStar_UInt128_uint128 c = FStar_UInt128_shift_right(tctr, (uint32_t)44U);
      tmp[ctr] = FStar_UInt128_uint64_to_uint128(r0);
      tmp[ctr + (uint32_t)1U] = FStar_UInt128_add(tctrp1, c);
    }
  }
  
  inline static void Hacl_Bignum_Fproduct_carry_limb_(uint64_t *tmp)
  {
    for (uint32_t i = (uint32_t)0U; i < (uint32_t)2U; i = i + (uint32_t)1U)
    {
      uint32_t ctr = i;
      uint64_t tctr = tmp[ctr];
      uint64_t tctrp1 = tmp[ctr + (uint32_t)1U];
      uint64_t r0 = tctr & (uint64_t)0xfffffffffffU;
      uint64_t c = tctr >> (uint32_t)44U;
      tmp[ctr] = r0;
      tmp[ctr + (uint32_t)1U] = tctrp1 + c;
    }
  }
  
  inline static void Hacl_Bignum_Modulo_reduce(uint64_t *b)
  {
    uint64_t b0 = b[0U];
    b[0U] = (b0 << (uint32_t)4U) + (b0 << (uint32_t)2U);
  }
  
  inline static void Hacl_Bignum_Modulo_carry_top(uint64_t *b)
  {
    uint64_t b2 = b[2U];
    uint64_t b0 = b[0U];
    uint64_t b2_42 = b2 >> (uint32_t)42U;
    b[2U] = b2 & (uint64_t)0x3ffffffffffU;
    b[0U] = (b2_42 << (uint32_t)2U) + b2_42 + b0;
  }
  
  inline static void Hacl_Bignum_Modulo_carry_top_wide(FStar_UInt128_uint128 *b)
  {
    FStar_UInt128_uint128 b2 = b[2U];
    FStar_UInt128_uint128 b0 = b[0U];
    FStar_UInt128_uint128
    b2_ = FStar_UInt128_logand(b2, FStar_UInt128_uint64_to_uint128((uint64_t)0x3ffffffffffU));
    uint64_t b2_42 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(b2, (uint32_t)42U));
    FStar_UInt128_uint128
    b0_ = FStar_UInt128_add(b0, FStar_UInt128_uint64_to_uint128((b2_42 << (uint32_t)2U) + b2_42));
    b[2U] = b2_;
    b[0U] = b0_;
  }
  
  inline static void Hacl_Bignum_Fmul_shift_reduce(uint64_t *output)
  {
    uint64_t tmp = output[2U];
    for (uint32_t i = (uint32_t)0U; i < (uint32_t)2U; i = i + (uint32_t)1U)
    {
      uint32_t ctr = (uint32_t)3U - i - (uint32_t)1U;
      uint64_t z = output[ctr - (uint32_t)1U];
      output[ctr] = z;
    }
    output[0U] = tmp;
    Hacl_Bignum_Modulo_reduce(output);
  }
  
  static void
  Hacl_Bignum_Fmul_mul_shift_reduce_(
    FStar_UInt128_uint128 *output,
    uint64_t *input,
    uint64_t *input2
  )
  {
    for (uint32_t i = (uint32_t)0U; i < (uint32_t)2U; i = i + (uint32_t)1U)
    {
      uint64_t input2i = input2[i];
      Hacl_Bignum_Fproduct_sum_scalar_multiplication_(output, input, input2i);
      Hacl_Bignum_Fmul_shift_reduce(input);
    }
    uint32_t i = (uint32_t)2U;
    uint64_t input2i = input2[i];
    Hacl_Bignum_Fproduct_sum_scalar_multiplication_(output, input, input2i);
  }
  
  inline static void Hacl_Bignum_Fmul_fmul(uint64_t *output, uint64_t *input, uint64_t *input2)
  {
    uint64_t tmp[3U] = { 0U };
    memcpy(tmp, input, (uint32_t)3U * sizeof input[0U]);
    KRML_CHECK_SIZE(sizeof (FStar_UInt128_uint128), (uint32_t)3U);
    FStar_UInt128_uint128 t[3U];
    for (uint32_t _i = 0U; _i < (uint32_t)3U; ++_i)
      t[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U);
    Hacl_Bignum_Fmul_mul_shift_reduce_(t, tmp, input2);
    Hacl_Bignum_Fproduct_carry_wide_(t);
    Hacl_Bignum_Modulo_carry_top_wide(t);
    Hacl_Bignum_Fproduct_copy_from_wide_(output, t);
    uint64_t i0 = output[0U];
    uint64_t i1 = output[1U];
    uint64_t i0_ = i0 & (uint64_t)0xfffffffffffU;
    uint64_t i1_ = i1 + (i0 >> (uint32_t)44U);
    output[0U] = i0_;
    output[1U] = i1_;
  }
  
  inline static void
  Hacl_Bignum_AddAndMultiply_add_and_multiply(uint64_t *acc, uint64_t *block, uint64_t *r)
  {
    for (uint32_t i = (uint32_t)0U; i < (uint32_t)3U; i = i + (uint32_t)1U)
    {
      uint64_t xi = acc[i];
      uint64_t yi = block[i];
      acc[i] = xi + yi;
    }
    Hacl_Bignum_Fmul_fmul(acc, acc, r);
  }
  
  typedef struct Hacl_Impl_Poly1305_64_State_poly1305_state_s
  {
    uint64_t *r;
    uint64_t *h;
  }
  Hacl_Impl_Poly1305_64_State_poly1305_state;
  
  extern FStar_UInt128_uint128 load128_le(uint8_t *x0);
  
  extern void store128_le(uint8_t *x0, FStar_UInt128_uint128 x1);
  
  inline static void
  Hacl_Impl_Poly1305_64_poly1305_update(
    Hacl_Impl_Poly1305_64_State_poly1305_state st,
    uint8_t *m
  )
  {
    uint64_t *acc = st.h;
    uint64_t *r = st.r;
    uint64_t tmp[3U] = { 0U };
    FStar_UInt128_uint128 m0 = load128_le(m);
    uint64_t r0 = FStar_UInt128_uint128_to_uint64(m0) & (uint64_t)0xfffffffffffU;
    uint64_t
    r1 =
      FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(m0, (uint32_t)44U))
      & (uint64_t)0xfffffffffffU;
    uint64_t r2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(m0, (uint32_t)88U));
    tmp[0U] = r0;
    tmp[1U] = r1;
    tmp[2U] = r2;
    uint64_t b2 = tmp[2U];
    uint64_t b2_ = (uint64_t)0x10000000000U | b2;
    tmp[2U] = b2_;
    Hacl_Bignum_AddAndMultiply_add_and_multiply(acc, tmp, r);
  }
  
  inline static void
  Hacl_Impl_Poly1305_64_poly1305_process_last_block_(
    uint8_t *block,
    Hacl_Impl_Poly1305_64_State_poly1305_state st,
    uint8_t *m,
    uint64_t rem_
  )
  {
    uint64_t tmp[3U] = { 0U };
    FStar_UInt128_uint128 m0 = load128_le(block);
    uint64_t r0 = FStar_UInt128_uint128_to_uint64(m0) & (uint64_t)0xfffffffffffU;
    uint64_t
    r1 =
      FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(m0, (uint32_t)44U))
      & (uint64_t)0xfffffffffffU;
    uint64_t r2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(m0, (uint32_t)88U));
    tmp[0U] = r0;
    tmp[1U] = r1;
    tmp[2U] = r2;
    Hacl_Bignum_AddAndMultiply_add_and_multiply(st.h, tmp, st.r);
  }
  
  inline static void
  Hacl_Impl_Poly1305_64_poly1305_process_last_block(
    Hacl_Impl_Poly1305_64_State_poly1305_state st,
    uint8_t *m,
    uint64_t rem_
  )
  {
    uint8_t zero1 = (uint8_t)0U;
    uint8_t block[16U];
    for (uint32_t _i = 0U; _i < (uint32_t)16U; ++_i)
      block[_i] = zero1;
    uint32_t i0 = (uint32_t)rem_;
    uint32_t i = (uint32_t)rem_;
    memcpy(block, m, i * sizeof m[0U]);
    block[i0] = (uint8_t)1U;
    Hacl_Impl_Poly1305_64_poly1305_process_last_block_(block, st, m, rem_);
  }
  
  static void Hacl_Impl_Poly1305_64_poly1305_last_pass(uint64_t *acc)
  {
    Hacl_Bignum_Fproduct_carry_limb_(acc);
    Hacl_Bignum_Modulo_carry_top(acc);
    uint64_t a0 = acc[0U];
    uint64_t a10 = acc[1U];
    uint64_t a20 = acc[2U];
    uint64_t a0_ = a0 & (uint64_t)0xfffffffffffU;
    uint64_t r0 = a0 >> (uint32_t)44U;
    uint64_t a1_ = (a10 + r0) & (uint64_t)0xfffffffffffU;
    uint64_t r1 = (a10 + r0) >> (uint32_t)44U;
    uint64_t a2_ = a20 + r1;
    acc[0U] = a0_;
    acc[1U] = a1_;
    acc[2U] = a2_;
    Hacl_Bignum_Modulo_carry_top(acc);
    uint64_t i0 = acc[0U];
    uint64_t i1 = acc[1U];
    uint64_t i0_ = i0 & (uint64_t)0xfffffffffffU;
    uint64_t i1_ = i1 + (i0 >> (uint32_t)44U);
    acc[0U] = i0_;
    acc[1U] = i1_;
    uint64_t a00 = acc[0U];
    uint64_t a1 = acc[1U];
    uint64_t a2 = acc[2U];
    uint64_t mask0 = FStar_UInt64_gte_mask(a00, (uint64_t)0xffffffffffbU);
    uint64_t mask1 = FStar_UInt64_eq_mask(a1, (uint64_t)0xfffffffffffU);
    uint64_t mask2 = FStar_UInt64_eq_mask(a2, (uint64_t)0x3ffffffffffU);
    uint64_t mask = (mask0 & mask1) & mask2;
    uint64_t a0_0 = a00 - ((uint64_t)0xffffffffffbU & mask);
    uint64_t a1_0 = a1 - ((uint64_t)0xfffffffffffU & mask);
    uint64_t a2_0 = a2 - ((uint64_t)0x3ffffffffffU & mask);
    acc[0U] = a0_0;
    acc[1U] = a1_0;
    acc[2U] = a2_0;
  }
  
  static Hacl_Impl_Poly1305_64_State_poly1305_state
  Hacl_Impl_Poly1305_64_mk_state(uint64_t *r, uint64_t *h)
  {
    return ((Hacl_Impl_Poly1305_64_State_poly1305_state){ .r = r, .h = h });
  }
  
  static void
  Hacl_Standalone_Poly1305_64_poly1305_blocks(
    Hacl_Impl_Poly1305_64_State_poly1305_state st,
    uint8_t *m,
    uint64_t len1
  )
  {
    if (!(len1 == (uint64_t)0U))
    {
      uint8_t *block = m;
      uint8_t *tail1 = m + (uint32_t)16U;
      Hacl_Impl_Poly1305_64_poly1305_update(st, block);
      uint64_t len2 = len1 - (uint64_t)1U;
      Hacl_Standalone_Poly1305_64_poly1305_blocks(st, tail1, len2);
    }
  }
  
  static void
  Hacl_Standalone_Poly1305_64_poly1305_partial(
    Hacl_Impl_Poly1305_64_State_poly1305_state st,
    uint8_t *input,
    uint64_t len1,
    uint8_t *kr
  )
  {
    uint64_t *x0 = st.r;
    FStar_UInt128_uint128 k1 = load128_le(kr);
    FStar_UInt128_uint128
    hs =
      FStar_UInt128_shift_left(FStar_UInt128_uint64_to_uint128((uint64_t)0x0ffffffc0ffffffcU),
        (uint32_t)64U);
    FStar_UInt128_uint128 ls = FStar_UInt128_uint64_to_uint128((uint64_t)0x0ffffffc0fffffffU);
    FStar_UInt128_uint128 k_clamped = FStar_UInt128_logand(k1, FStar_UInt128_logor(hs, ls));
    uint64_t r0 = FStar_UInt128_uint128_to_uint64(k_clamped) & (uint64_t)0xfffffffffffU;
    uint64_t
    r1 =
      FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(k_clamped, (uint32_t)44U))
      & (uint64_t)0xfffffffffffU;
    uint64_t
    r2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(k_clamped, (uint32_t)88U));
    x0[0U] = r0;
    x0[1U] = r1;
    x0[2U] = r2;
    uint64_t *x00 = st.h;
    x00[0U] = (uint64_t)0U;
    x00[1U] = (uint64_t)0U;
    x00[2U] = (uint64_t)0U;
    Hacl_Standalone_Poly1305_64_poly1305_blocks(st, input, len1);
  }
  
  static void
  Hacl_Standalone_Poly1305_64_poly1305_complete(
    Hacl_Impl_Poly1305_64_State_poly1305_state st,
    uint8_t *m,
    uint64_t len1,
    uint8_t *k1
  )
  {
    uint8_t *kr = k1;
    uint64_t len16 = len1 >> (uint32_t)4U;
    uint64_t rem16 = len1 & (uint64_t)0xfU;
    uint8_t *part_input = m;
    uint8_t *last_block = m + (uint32_t)((uint64_t)16U * len16);
    Hacl_Standalone_Poly1305_64_poly1305_partial(st, part_input, len16, kr);
    if (!(rem16 == (uint64_t)0U))
      Hacl_Impl_Poly1305_64_poly1305_process_last_block(st, last_block, rem16);
    uint64_t *acc = st.h;
    Hacl_Impl_Poly1305_64_poly1305_last_pass(acc);
  }
  
  static void
  Hacl_Standalone_Poly1305_64_crypto_onetimeauth_(
    uint8_t *output,
    uint8_t *input,
    uint64_t len1,
    uint8_t *k1
  )
  {
    uint64_t buf[6U] = { 0U };
    uint64_t *r = buf;
    uint64_t *h = buf + (uint32_t)3U;
    Hacl_Impl_Poly1305_64_State_poly1305_state st = Hacl_Impl_Poly1305_64_mk_state(r, h);
    uint8_t *key_s = k1 + (uint32_t)16U;
    Hacl_Standalone_Poly1305_64_poly1305_complete(st, input, len1, k1);
    uint64_t *acc = st.h;
    FStar_UInt128_uint128 k_ = load128_le(key_s);
    uint64_t h0 = acc[0U];
    uint64_t h1 = acc[1U];
    uint64_t h2 = acc[2U];
    uint64_t accl = h1 << (uint32_t)44U | h0;
    uint64_t acch = h2 << (uint32_t)24U | h1 >> (uint32_t)20U;
    FStar_UInt128_uint128
    acc_ =
      FStar_UInt128_logor(FStar_UInt128_shift_left(FStar_UInt128_uint64_to_uint128(acch),
          (uint32_t)64U),
        FStar_UInt128_uint64_to_uint128(accl));
    FStar_UInt128_uint128 acc_0 = acc_;
    FStar_UInt128_uint128 mac_ = FStar_UInt128_add_mod(acc_0, k_);
    store128_le(output, mac_);
  }
  
  static void
  Hacl_Standalone_Poly1305_64_crypto_onetimeauth(
    uint8_t *output,
    uint8_t *input,
    uint64_t len1,
    uint8_t *k1
  )
  {
    Hacl_Standalone_Poly1305_64_crypto_onetimeauth_(output, input, len1, k1);
  }
  
  void
  Hacl_Poly1305_64_crypto_onetimeauth(
    uint8_t *output,
    uint8_t *input,
    uint64_t len1,
    uint8_t *k1
  )
  {
    Hacl_Standalone_Poly1305_64_crypto_onetimeauth(output, input, len1, k1);
  }
  
  /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
     Licensed under the Apache 2.0 License. */
  
  /******************************************************************************/
  /* Machine integers (128-bit arithmetic)                                      */
  /******************************************************************************/
  
  /* This header makes KreMLin-generated C code work with, 0x
   * - the default setting where we assume the target compiler defines __int128
   * - the setting where we use FStar.UInt128's implementation instead; in that
   *   case, generated C files must be compiled with -DKRML_VERIFIED_UINT128
   * - a refinement of the case above, wherein all structures are passed by
   *   reference, a.k.a. "-fnostruct-passing", meaning that the KreMLin-generated
   *   must be compiled with -DKRML_NOSTRUCT_PASSING
   * Note, 0x no MSVC support in this file.
   */
  
  /* This file is used for both the minimal and generic kremlib distributions. As
   * such, it assumes that the machine integers have been bundled the exact same
   * way in both cases. */
  
  #include "FStar_UInt128.h"
  #include "FStar_UInt_8_16_32_64.h"
  #include "C_Endianness.h"
  
  #if !defined(KRML_VERIFIED_UINT128) && !defined(_MSC_VER)
  
  /* GCC + using native unsigned __int128 support */
  
  uint128_t load128_le(uint8_t *b) {
    uint128_t l = (uint128_t)load64_le(b);
    uint128_t h = (uint128_t)load64_le(b + 8);
    return (h << 64 | l);
  }
  
  void store128_le(uint8_t *b, uint128_t n) {
    store64_le(b, (uint64_t)n);
  
    store64_le(b + 8, (uint64_t)(n >> 64));
  }
  
  uint128_t load128_be(uint8_t *b) {
    uint128_t h = (uint128_t)load64_be(b);
    uint128_t l = (uint128_t)load64_be(b + 8);
    return (h << 64 | l);
  }
  
  void store128_be(uint8_t *b, uint128_t n) {
    store64_be(b, (uint64_t)(n >> 64));
    store64_be(b + 8, (uint64_t)n);
  }
  
  uint128_t FStar_UInt128_add(uint128_t x, uint128_t y) {
    return x + y;
  }
  
  uint128_t FStar_UInt128_mul(uint128_t x, uint128_t y) {
    return x * y;
  }
  
  uint128_t FStar_UInt128_add_mod(uint128_t x, uint128_t y) {
    return x + y;
  }
  
  uint128_t FStar_UInt128_sub(uint128_t x, uint128_t y) {
    return x - y;
  }
  
  uint128_t FStar_UInt128_sub_mod(uint128_t x, uint128_t y) {
    return x - y;
  }
  
  uint128_t FStar_UInt128_logand(uint128_t x, uint128_t y) {
    return x & y;
  }
  
  uint128_t FStar_UInt128_logor(uint128_t x, uint128_t y) {
    return x | y;
  }
  
  uint128_t FStar_UInt128_logxor(uint128_t x, uint128_t y) {
    return x ^ y;
  }
  
  uint128_t FStar_UInt128_lognot(uint128_t x) {
    return ~x;
  }
  
  uint128_t FStar_UInt128_shift_left(uint128_t x, uint32_t y) {
    return x << y;
  }
  
  uint128_t FStar_UInt128_shift_right(uint128_t x, uint32_t y) {
    return x >> y;
  }
  
  uint128_t FStar_UInt128_uint64_to_uint128(uint64_t x) {
    return (uint128_t)x;
  }
  
  uint64_t FStar_UInt128_uint128_to_uint64(uint128_t x) {
    return (uint64_t)x;
  }
  
  uint128_t FStar_UInt128_mul_wide(uint64_t x, uint64_t y) {
    return ((uint128_t) x) * y;
  }
  
  uint128_t FStar_UInt128_eq_mask(uint128_t x, uint128_t y) {
    uint64_t mask =
        FStar_UInt64_eq_mask((uint64_t)(x >> 64), (uint64_t)(y >> 64)) &
        FStar_UInt64_eq_mask(x, y);
    return ((uint128_t)mask) << 64 | mask;
  }
  
  uint128_t FStar_UInt128_gte_mask(uint128_t x, uint128_t y) {
    uint64_t mask =
        (FStar_UInt64_gte_mask(x >> 64, y >> 64) &
         ~(FStar_UInt64_eq_mask(x >> 64, y >> 64))) |
        (FStar_UInt64_eq_mask(x >> 64, y >> 64) & FStar_UInt64_gte_mask(x, y));
    return ((uint128_t)mask) << 64 | mask;
  }
  
  uint128_t FStar_Int_Cast_Full_uint64_to_uint128(uint64_t x) {
    return x;
  }
  
  uint64_t FStar_Int_Cast_Full_uint128_to_uint64(uint128_t x) {
    return x;
  }
  
  #elif !defined(_MSC_VER) && defined(KRML_VERIFIED_UINT128)
  
  /* Verified uint128 implementation. */
  
  /* Access 64-bit fields within the int128. */
  #define HIGH64_OF(x) ((x)->high)
  #define LOW64_OF(x)  ((x)->low)
  
  typedef FStar_UInt128_uint128 FStar_UInt128_t_, uint128_t;
  
  /* A series of definitions written using pointers. */
  
  void load128_le_(uint8_t *b, uint128_t *r) {
    LOW64_OF(r) = load64_le(b);
    HIGH64_OF(r) = load64_le(b + 8);
  }
  
  void store128_le_(uint8_t *b, uint128_t *n) {
    store64_le(b, LOW64_OF(n));
    store64_le(b + 8, HIGH64_OF(n));
  }
  
  void load128_be_(uint8_t *b, uint128_t *r) {
    HIGH64_OF(r) = load64_be(b);
    LOW64_OF(r) = load64_be(b + 8);
  }
  
  void store128_be_(uint8_t *b, uint128_t *n) {
    store64_be(b, HIGH64_OF(n));
    store64_be(b + 8, LOW64_OF(n));
  }
  
  void
  FStar_Int_Cast_Full_uint64_to_uint128_(uint64_t x, uint128_t *dst) {
    /* C89 */
    LOW64_OF(dst) = x;
    HIGH64_OF(dst) = 0;
  }
  
  uint64_t FStar_Int_Cast_Full_uint128_to_uint64_(uint128_t *x) {
    return LOW64_OF(x);
  }
  
  #    ifndef KRML_NOSTRUCT_PASSING
  
  uint128_t load128_le(uint8_t *b) {
    uint128_t r;
    load128_le_(b, &r);
    return r;
  }
  
  void store128_le(uint8_t *b, uint128_t n) {
    store128_le_(b, &n);
  }
  
  uint128_t load128_be(uint8_t *b) {
    uint128_t r;
    load128_be_(b, &r);
    return r;
  }
  
  void store128_be(uint8_t *b, uint128_t n) {
    store128_be_(b, &n);
  }
  
  uint128_t FStar_Int_Cast_Full_uint64_to_uint128(uint64_t x) {
    uint128_t dst;
    FStar_Int_Cast_Full_uint64_to_uint128_(x, &dst);
    return dst;
  }
  
  uint64_t FStar_Int_Cast_Full_uint128_to_uint64(uint128_t x) {
    return FStar_Int_Cast_Full_uint128_to_uint64_(&x);
  }
  
  #    else /* !defined(KRML_STRUCT_PASSING) */
  
  #      define print128 print128_
  #      define load128_le load128_le_
  #      define store128_le store128_le_
  #      define load128_be load128_be_
  #      define store128_be store128_be_
  #      define FStar_Int_Cast_Full_uint128_to_uint64                            \
          FStar_Int_Cast_Full_uint128_to_uint64_
  #      define FStar_Int_Cast_Full_uint64_to_uint128                            \
          FStar_Int_Cast_Full_uint64_to_uint128_
  
  #    endif /* KRML_STRUCT_PASSING */
  
  #endif
  
  #include "FStar_UInt_8_16_32_64.h"
  
  uint64_t FStar_UInt64_eq_mask(uint64_t a, uint64_t b)
  {
    uint64_t x = a ^ b;
    uint64_t minus_x = ~x + (uint64_t)1U;
    uint64_t x_or_minus_x = x | minus_x;
    uint64_t xnx = x_or_minus_x >> (uint32_t)63U;
    return xnx - (uint64_t)1U;
  }
  
  uint64_t FStar_UInt64_gte_mask(uint64_t a, uint64_t b)
  {
    uint64_t x = a;
    uint64_t y = b;
    uint64_t x_xor_y = x ^ y;
    uint64_t x_sub_y = x - y;
    uint64_t x_sub_y_xor_y = x_sub_y ^ y;
    uint64_t q = x_xor_y | x_sub_y_xor_y;
    uint64_t x_xor_q = x ^ q;
    uint64_t x_xor_q_ = x_xor_q >> (uint32_t)63U;
    return x_xor_q_ - (uint64_t)1U;
  }
  
  uint32_t FStar_UInt32_eq_mask(uint32_t a, uint32_t b)
  {
    uint32_t x = a ^ b;
    uint32_t minus_x = ~x + (uint32_t)1U;
    uint32_t x_or_minus_x = x | minus_x;
    uint32_t xnx = x_or_minus_x >> (uint32_t)31U;
    return xnx - (uint32_t)1U;
  }
  
  uint32_t FStar_UInt32_gte_mask(uint32_t a, uint32_t b)
  {
    uint32_t x = a;
    uint32_t y = b;
    uint32_t x_xor_y = x ^ y;
    uint32_t x_sub_y = x - y;
    uint32_t x_sub_y_xor_y = x_sub_y ^ y;
    uint32_t q = x_xor_y | x_sub_y_xor_y;
    uint32_t x_xor_q = x ^ q;
    uint32_t x_xor_q_ = x_xor_q >> (uint32_t)31U;
    return x_xor_q_ - (uint32_t)1U;
  }
  
  uint16_t FStar_UInt16_eq_mask(uint16_t a, uint16_t b)
  {
    uint16_t x = a ^ b;
    uint16_t minus_x = ~x + (uint16_t)1U;
    uint16_t x_or_minus_x = x | minus_x;
    uint16_t xnx = x_or_minus_x >> (uint32_t)15U;
    return xnx - (uint16_t)1U;
  }
  
  uint16_t FStar_UInt16_gte_mask(uint16_t a, uint16_t b)
  {
    uint16_t x = a;
    uint16_t y = b;
    uint16_t x_xor_y = x ^ y;
    uint16_t x_sub_y = x - y;
    uint16_t x_sub_y_xor_y = x_sub_y ^ y;
    uint16_t q = x_xor_y | x_sub_y_xor_y;
    uint16_t x_xor_q = x ^ q;
    uint16_t x_xor_q_ = x_xor_q >> (uint32_t)15U;
    return x_xor_q_ - (uint16_t)1U;
  }
  
  uint8_t FStar_UInt8_eq_mask(uint8_t a, uint8_t b)
  {
    uint8_t x = a ^ b;
    uint8_t minus_x = ~x + (uint8_t)1U;
    uint8_t x_or_minus_x = x | minus_x;
    uint8_t xnx = x_or_minus_x >> (uint32_t)7U;
    return xnx - (uint8_t)1U;
  }
  
  uint8_t FStar_UInt8_gte_mask(uint8_t a, uint8_t b)
  {
    uint8_t x = a;
    uint8_t y = b;
    uint8_t x_xor_y = x ^ y;
    uint8_t x_sub_y = x - y;
    uint8_t x_sub_y_xor_y = x_sub_y ^ y;
    uint8_t q = x_xor_y | x_sub_y_xor_y;
    uint8_t x_xor_q = x ^ q;
    uint8_t x_xor_q_ = x_xor_q >> (uint32_t)7U;
    return x_xor_q_ - (uint8_t)1U;
  }
  
  int main() {
    uint8_t msg[] = "Cryptographic Forum Research Group";
    uint8_t key[] = {
      0x85, 0xd6, 0xbe, 0x78, 0x57, 0x55, 0x6d, 0x33,
      0x7f, 0x44, 0x52, 0xfe, 0x42, 0xd5, 0x06, 0xa8,
      0x01, 0x03, 0x80, 0x8a, 0xfb, 0x0d, 0xb2, 0xfd,
      0x4a, 0xbf, 0xf6, 0xaf, 0x41, 0x49, 0xf5, 0x1b
    };
    uint8_t outp[36];
    uint8_t tag[] = {
      0xa8, 0x06, 0x1d, 0xc1, 0x30, 0x51, 0x36, 0xc6,
      0xc2, 0x2b, 0x8b, 0xaf, 0x0c, 0x01, 0x27, 0xa9
    };
    Hacl_Poly1305_64_crypto_onetimeauth(outp, msg, sizeof msg - 1, key);
    if (memcmp(tag, outp, 16) != 0)
      abort();
  }
  
  