Library import 16 (#2433)

Co-authored-by: robot-piglet <[email protected]>
Co-authored-by: deshevoy <[email protected]>
Co-authored-by: robot-contrib <[email protected]>
Co-authored-by: thegeorg <[email protected]>
Co-authored-by: robot-ya-builder <[email protected]>
Co-authored-by: svidyuk <[email protected]>
Co-authored-by: shadchin <[email protected]>
Co-authored-by: robot-ratatosk <[email protected]>
Co-authored-by: innokentii <[email protected]>
Co-authored-by: arkady-e1ppa <[email protected]>
Co-authored-by: snermolaev <[email protected]>
Co-authored-by: dimdim11 <[email protected]>
Co-authored-by: kickbutt <[email protected]>
Co-authored-by: abdullinsaid <[email protected]>
Co-authored-by: korsunandrei <[email protected]>
Co-authored-by: petrk <[email protected]>
Co-authored-by: miroslav2 <[email protected]>
Co-authored-by: serjflint <[email protected]>
Co-authored-by: akhropov <[email protected]>
Co-authored-by: prettyboy <[email protected]>
Co-authored-by: ilikepugs <[email protected]>
Co-authored-by: hiddenpath <[email protected]>
Co-authored-by: mikhnenko <[email protected]>
Co-authored-by: spreis <[email protected]>
Co-authored-by: andreyshspb <[email protected]>
Co-authored-by: dimaandreev <[email protected]>
Co-authored-by: rashid <[email protected]>
Co-authored-by: robot-ydb-importer <[email protected]>
Co-authored-by: r-vetrov <[email protected]>
Co-authored-by: ypodlesov <[email protected]>
Co-authored-by: zaverden <[email protected]>
Co-authored-by: vpozdyayev <[email protected]>
Co-authored-by: robot-cozmo <[email protected]>
Co-authored-by: v-korovin <[email protected]>
Co-authored-by: arikon <[email protected]>
Co-authored-by: khoden <[email protected]>
Co-authored-by: psydmm <[email protected]>
Co-authored-by: robot-javacom <[email protected]>
Co-authored-by: dtorilov <[email protected]>
Co-authored-by: sennikovmv <[email protected]>
Co-authored-by: hcpp <[email protected]>

6 files changed, 1032 insertions, 0 deletions

diff --git a/contrib/tools/python3/Modules/_hacl/include/krml/FStar_UInt128_Verified.h b/contrib/tools/python3/Modules/_hacl/include/krml/FStar_UInt128_Verified.h
new file mode 100644
index 00000000000..3d36d440735
--- /dev/null
+++ b/contrib/tools/python3/Modules/_hacl/include/krml/FStar_UInt128_Verified.h
@@ -0,0 +1,346 @@
+/*
+  Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
+  Licensed under the Apache 2.0 License.
+*/
+
+
+#ifndef __FStar_UInt128_Verified_H
+#define __FStar_UInt128_Verified_H
+
+#include "FStar_UInt_8_16_32_64.h"
+#include <inttypes.h>
+#include <stdbool.h>
+#include "krml/types.h"
+#include "krml/internal/target.h"
+
+static inline uint64_t FStar_UInt128_constant_time_carry(uint64_t a, uint64_t b)
+{
+  return (a ^ ((a ^ b) | ((a - b) ^ b))) >> (uint32_t)63U;
+}
+
+static inline uint64_t FStar_UInt128_carry(uint64_t a, uint64_t b)
+{
+  return FStar_UInt128_constant_time_carry(a, b);
+}
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_add(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  FStar_UInt128_uint128 lit;
+  lit.low = a.low + b.low;
+  lit.high = a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low);
+  return lit;
+}
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_add_underspec(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  FStar_UInt128_uint128 lit;
+  lit.low = a.low + b.low;
+  lit.high = a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low);
+  return lit;
+}
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_add_mod(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  FStar_UInt128_uint128 lit;
+  lit.low = a.low + b.low;
+  lit.high = a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low);
+  return lit;
+}
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_sub(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  FStar_UInt128_uint128 lit;
+  lit.low = a.low - b.low;
+  lit.high = a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low);
+  return lit;
+}
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_sub_underspec(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  FStar_UInt128_uint128 lit;
+  lit.low = a.low - b.low;
+  lit.high = a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low);
+  return lit;
+}
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_sub_mod_impl(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  FStar_UInt128_uint128 lit;
+  lit.low = a.low - b.low;
+  lit.high = a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low);
+  return lit;
+}
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_sub_mod(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  return FStar_UInt128_sub_mod_impl(a, b);
+}
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_logand(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  FStar_UInt128_uint128 lit;
+  lit.low = a.low & b.low;
+  lit.high = a.high & b.high;
+  return lit;
+}
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_logxor(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  FStar_UInt128_uint128 lit;
+  lit.low = a.low ^ b.low;
+  lit.high = a.high ^ b.high;
+  return lit;
+}
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_logor(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  FStar_UInt128_uint128 lit;
+  lit.low = a.low | b.low;
+  lit.high = a.high | b.high;
+  return lit;
+}
+
+static inline FStar_UInt128_uint128 FStar_UInt128_lognot(FStar_UInt128_uint128 a)
+{
+  FStar_UInt128_uint128 lit;
+  lit.low = ~a.low;
+  lit.high = ~a.high;
+  return lit;
+}
+
+static uint32_t FStar_UInt128_u32_64 = (uint32_t)64U;
+
+static inline uint64_t FStar_UInt128_add_u64_shift_left(uint64_t hi, uint64_t lo, uint32_t s)
+{
+  return (hi << s) + (lo >> (FStar_UInt128_u32_64 - s));
+}
+
+static inline uint64_t
+FStar_UInt128_add_u64_shift_left_respec(uint64_t hi, uint64_t lo, uint32_t s)
+{
+  return FStar_UInt128_add_u64_shift_left(hi, lo, s);
+}
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_shift_left_small(FStar_UInt128_uint128 a, uint32_t s)
+{
+  if (s == (uint32_t)0U)
+  {
+    return a;
+  }
+  else
+  {
+    FStar_UInt128_uint128 lit;
+    lit.low = a.low << s;
+    lit.high = FStar_UInt128_add_u64_shift_left_respec(a.high, a.low, s);
+    return lit;
+  }
+}
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_shift_left_large(FStar_UInt128_uint128 a, uint32_t s)
+{
+  FStar_UInt128_uint128 lit;
+  lit.low = (uint64_t)0U;
+  lit.high = a.low << (s - FStar_UInt128_u32_64);
+  return lit;
+}
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_shift_left(FStar_UInt128_uint128 a, uint32_t s)
+{
+  if (s < FStar_UInt128_u32_64)
+  {
+    return FStar_UInt128_shift_left_small(a, s);
+  }
+  else
+  {
+    return FStar_UInt128_shift_left_large(a, s);
+  }
+}
+
+static inline uint64_t FStar_UInt128_add_u64_shift_right(uint64_t hi, uint64_t lo, uint32_t s)
+{
+  return (lo >> s) + (hi << (FStar_UInt128_u32_64 - s));
+}
+
+static inline uint64_t
+FStar_UInt128_add_u64_shift_right_respec(uint64_t hi, uint64_t lo, uint32_t s)
+{
+  return FStar_UInt128_add_u64_shift_right(hi, lo, s);
+}
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_shift_right_small(FStar_UInt128_uint128 a, uint32_t s)
+{
+  if (s == (uint32_t)0U)
+  {
+    return a;
+  }
+  else
+  {
+    FStar_UInt128_uint128 lit;
+    lit.low = FStar_UInt128_add_u64_shift_right_respec(a.high, a.low, s);
+    lit.high = a.high >> s;
+    return lit;
+  }
+}
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_shift_right_large(FStar_UInt128_uint128 a, uint32_t s)
+{
+  FStar_UInt128_uint128 lit;
+  lit.low = a.high >> (s - FStar_UInt128_u32_64);
+  lit.high = (uint64_t)0U;
+  return lit;
+}
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_shift_right(FStar_UInt128_uint128 a, uint32_t s)
+{
+  if (s < FStar_UInt128_u32_64)
+  {
+    return FStar_UInt128_shift_right_small(a, s);
+  }
+  else
+  {
+    return FStar_UInt128_shift_right_large(a, s);
+  }
+}
+
+static inline bool FStar_UInt128_eq(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  return a.low == b.low && a.high == b.high;
+}
+
+static inline bool FStar_UInt128_gt(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  return a.high > b.high || (a.high == b.high && a.low > b.low);
+}
+
+static inline bool FStar_UInt128_lt(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  return a.high < b.high || (a.high == b.high && a.low < b.low);
+}
+
+static inline bool FStar_UInt128_gte(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  return a.high > b.high || (a.high == b.high && a.low >= b.low);
+}
+
+static inline bool FStar_UInt128_lte(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  return a.high < b.high || (a.high == b.high && a.low <= b.low);
+}
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_eq_mask(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  FStar_UInt128_uint128 lit;
+  lit.low = FStar_UInt64_eq_mask(a.low, b.low) & FStar_UInt64_eq_mask(a.high, b.high);
+  lit.high = FStar_UInt64_eq_mask(a.low, b.low) & FStar_UInt64_eq_mask(a.high, b.high);
+  return lit;
+}
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_gte_mask(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+  FStar_UInt128_uint128 lit;
+  lit.low =
+    (FStar_UInt64_gte_mask(a.high, b.high) & ~FStar_UInt64_eq_mask(a.high, b.high))
+    | (FStar_UInt64_eq_mask(a.high, b.high) & FStar_UInt64_gte_mask(a.low, b.low));
+  lit.high =
+    (FStar_UInt64_gte_mask(a.high, b.high) & ~FStar_UInt64_eq_mask(a.high, b.high))
+    | (FStar_UInt64_eq_mask(a.high, b.high) & FStar_UInt64_gte_mask(a.low, b.low));
+  return lit;
+}
+
+static inline FStar_UInt128_uint128 FStar_UInt128_uint64_to_uint128(uint64_t a)
+{
+  FStar_UInt128_uint128 lit;
+  lit.low = a;
+  lit.high = (uint64_t)0U;
+  return lit;
+}
+
+static inline uint64_t FStar_UInt128_uint128_to_uint64(FStar_UInt128_uint128 a)
+{
+  return a.low;
+}
+
+static inline uint64_t FStar_UInt128_u64_mod_32(uint64_t a)
+{
+  return a & (uint64_t)0xffffffffU;
+}
+
+static uint32_t FStar_UInt128_u32_32 = (uint32_t)32U;
+
+static inline uint64_t FStar_UInt128_u32_combine(uint64_t hi, uint64_t lo)
+{
+  return lo + (hi << FStar_UInt128_u32_32);
+}
+
+static inline FStar_UInt128_uint128 FStar_UInt128_mul32(uint64_t x, uint32_t y)
+{
+  FStar_UInt128_uint128 lit;
+  lit.low =
+    FStar_UInt128_u32_combine((x >> FStar_UInt128_u32_32)
+      * (uint64_t)y
+      + (FStar_UInt128_u64_mod_32(x) * (uint64_t)y >> FStar_UInt128_u32_32),
+      FStar_UInt128_u64_mod_32(FStar_UInt128_u64_mod_32(x) * (uint64_t)y));
+  lit.high =
+    ((x >> FStar_UInt128_u32_32)
+    * (uint64_t)y
+    + (FStar_UInt128_u64_mod_32(x) * (uint64_t)y >> FStar_UInt128_u32_32))
+    >> FStar_UInt128_u32_32;
+  return lit;
+}
+
+static inline uint64_t FStar_UInt128_u32_combine_(uint64_t hi, uint64_t lo)
+{
+  return lo + (hi << FStar_UInt128_u32_32);
+}
+
+static inline FStar_UInt128_uint128 FStar_UInt128_mul_wide(uint64_t x, uint64_t y)
+{
+  FStar_UInt128_uint128 lit;
+  lit.low =
+    FStar_UInt128_u32_combine_(FStar_UInt128_u64_mod_32(x)
+      * (y >> FStar_UInt128_u32_32)
+      +
+        FStar_UInt128_u64_mod_32((x >> FStar_UInt128_u32_32)
+          * FStar_UInt128_u64_mod_32(y)
+          + (FStar_UInt128_u64_mod_32(x) * FStar_UInt128_u64_mod_32(y) >> FStar_UInt128_u32_32)),
+      FStar_UInt128_u64_mod_32(FStar_UInt128_u64_mod_32(x) * FStar_UInt128_u64_mod_32(y)));
+  lit.high =
+    (x >> FStar_UInt128_u32_32)
+    * (y >> FStar_UInt128_u32_32)
+    +
+      (((x >> FStar_UInt128_u32_32)
+      * FStar_UInt128_u64_mod_32(y)
+      + (FStar_UInt128_u64_mod_32(x) * FStar_UInt128_u64_mod_32(y) >> FStar_UInt128_u32_32))
+      >> FStar_UInt128_u32_32)
+    +
+      ((FStar_UInt128_u64_mod_32(x)
+      * (y >> FStar_UInt128_u32_32)
+      +
+        FStar_UInt128_u64_mod_32((x >> FStar_UInt128_u32_32)
+          * FStar_UInt128_u64_mod_32(y)
+          + (FStar_UInt128_u64_mod_32(x) * FStar_UInt128_u64_mod_32(y) >> FStar_UInt128_u32_32)))
+      >> FStar_UInt128_u32_32);
+  return lit;
+}
+
+
+#define __FStar_UInt128_Verified_H_DEFINED
+#endif
diff --git a/contrib/tools/python3/Modules/_hacl/include/krml/FStar_UInt_8_16_32_64.h b/contrib/tools/python3/Modules/_hacl/include/krml/FStar_UInt_8_16_32_64.h
new file mode 100644
index 00000000000..a56c7d61349
--- /dev/null
+++ b/contrib/tools/python3/Modules/_hacl/include/krml/FStar_UInt_8_16_32_64.h
@@ -0,0 +1,107 @@
+/*
+  Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
+  Licensed under the Apache 2.0 License.
+*/
+
+
+#ifndef __FStar_UInt_8_16_32_64_H
+#define __FStar_UInt_8_16_32_64_H
+
+#include <inttypes.h>
+#include <stdbool.h>
+
+#include "krml/lowstar_endianness.h"
+#include "krml/types.h"
+#include "krml/internal/target.h"
+
+static inline 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;
+}
+
+static inline 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;
+}
+
+static inline 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;
+}
+
+static inline 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;
+}
+
+static inline 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;
+}
+
+static inline 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;
+}
+
+static inline 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;
+}
+
+static inline 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;
+}
+
+
+#define __FStar_UInt_8_16_32_64_H_DEFINED
+#endif
diff --git a/contrib/tools/python3/Modules/_hacl/include/krml/fstar_uint128_struct_endianness.h b/contrib/tools/python3/Modules/_hacl/include/krml/fstar_uint128_struct_endianness.h
new file mode 100644
index 00000000000..e2b6d62859a
--- /dev/null
+++ b/contrib/tools/python3/Modules/_hacl/include/krml/fstar_uint128_struct_endianness.h
@@ -0,0 +1,68 @@
+/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
+   Licensed under the Apache 2.0 License. */
+
+#ifndef FSTAR_UINT128_STRUCT_ENDIANNESS_H
+#define FSTAR_UINT128_STRUCT_ENDIANNESS_H
+
+/* Hand-written implementation of endianness-related uint128 functions
+ * for the extracted uint128 implementation */
+
+/* Access 64-bit fields within the int128. */
+#define HIGH64_OF(x) ((x)->high)
+#define LOW64_OF(x)  ((x)->low)
+
+/* A series of definitions written using pointers. */
+
+inline static void load128_le_(uint8_t *b, uint128_t *r) {
+  LOW64_OF(r) = load64_le(b);
+  HIGH64_OF(r) = load64_le(b + 8);
+}
+
+inline static void store128_le_(uint8_t *b, uint128_t *n) {
+  store64_le(b, LOW64_OF(n));
+  store64_le(b + 8, HIGH64_OF(n));
+}
+
+inline static void load128_be_(uint8_t *b, uint128_t *r) {
+  HIGH64_OF(r) = load64_be(b);
+  LOW64_OF(r) = load64_be(b + 8);
+}
+
+inline static void store128_be_(uint8_t *b, uint128_t *n) {
+  store64_be(b, HIGH64_OF(n));
+  store64_be(b + 8, LOW64_OF(n));
+}
+
+#ifndef KRML_NOSTRUCT_PASSING
+
+inline static uint128_t load128_le(uint8_t *b) {
+  uint128_t r;
+  load128_le_(b, &r);
+  return r;
+}
+
+inline static void store128_le(uint8_t *b, uint128_t n) {
+  store128_le_(b, &n);
+}
+
+inline static uint128_t load128_be(uint8_t *b) {
+  uint128_t r;
+  load128_be_(b, &r);
+  return r;
+}
+
+inline static void store128_be(uint8_t *b, uint128_t n) {
+  store128_be_(b, &n);
+}
+
+#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_
+
+#endif /* KRML_STRUCT_PASSING */
+
+#endif
diff --git a/contrib/tools/python3/Modules/_hacl/include/krml/internal/target.h b/contrib/tools/python3/Modules/_hacl/include/krml/internal/target.h
new file mode 100644
index 00000000000..5a2f94eb2ec
--- /dev/null
+++ b/contrib/tools/python3/Modules/_hacl/include/krml/internal/target.h
@@ -0,0 +1,266 @@
+/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
+   Licensed under the Apache 2.0 License. */
+
+#ifndef __KRML_TARGET_H
+#define __KRML_TARGET_H
+
+#include <stdlib.h>
+#include <stddef.h>
+#include <stdio.h>
+#include <stdbool.h>
+#include <inttypes.h>
+#include <limits.h>
+#include <assert.h>
+
+/* Since KaRaMeL emits the inline keyword unconditionally, we follow the
+ * guidelines at https://gcc.gnu.org/onlinedocs/gcc/Inline.html and make this
+ * __inline__ to ensure the code compiles with -std=c90 and earlier. */
+#ifdef __GNUC__
+#  define inline __inline__
+#endif
+
+/******************************************************************************/
+/* Macros that KaRaMeL will generate.                                         */
+/******************************************************************************/
+
+/* For "bare" targets that do not have a C stdlib, the user might want to use
+ * [-add-early-include '"mydefinitions.h"'] and override these. */
+#ifndef KRML_HOST_PRINTF
+#  define KRML_HOST_PRINTF printf
+#endif
+
+#if (                                                                          \
+    (defined __STDC_VERSION__) && (__STDC_VERSION__ >= 199901L) &&             \
+    (!(defined KRML_HOST_EPRINTF)))
+#  define KRML_HOST_EPRINTF(...) fprintf(stderr, __VA_ARGS__)
+#elif !(defined KRML_HOST_EPRINTF) && defined(_MSC_VER)
+#  define KRML_HOST_EPRINTF(...) fprintf(stderr, __VA_ARGS__)
+#endif
+
+#ifndef KRML_HOST_EXIT
+#  define KRML_HOST_EXIT exit
+#endif
+
+#ifndef KRML_HOST_MALLOC
+#  define KRML_HOST_MALLOC malloc
+#endif
+
+#ifndef KRML_HOST_CALLOC
+#  define KRML_HOST_CALLOC calloc
+#endif
+
+#ifndef KRML_HOST_FREE
+#  define KRML_HOST_FREE free
+#endif
+
+#ifndef KRML_HOST_IGNORE
+#  define KRML_HOST_IGNORE(x) (void)(x)
+#endif
+
+/* In FStar.Buffer.fst, the size of arrays is uint32_t, but it's a number of
+ * *elements*. Do an ugly, run-time check (some of which KaRaMeL can eliminate).
+ */
+#if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ > 4))
+#  define _KRML_CHECK_SIZE_PRAGMA                                              \
+    _Pragma("GCC diagnostic ignored \"-Wtype-limits\"")
+#else
+#  define _KRML_CHECK_SIZE_PRAGMA
+#endif
+
+#define KRML_CHECK_SIZE(size_elt, sz)                                          \
+  do {                                                                         \
+    _KRML_CHECK_SIZE_PRAGMA                                                    \
+    if (((size_t)(sz)) > ((size_t)(SIZE_MAX / (size_elt)))) {                  \
+      KRML_HOST_PRINTF(                                                        \
+          "Maximum allocatable size exceeded, aborting before overflow at "    \
+          "%s:%d\n",                                                           \
+          __FILE__, __LINE__);                                                 \
+      KRML_HOST_EXIT(253);                                                     \
+    }                                                                          \
+  } while (0)
+
+/* Macros for prettier unrolling of loops */
+#define KRML_LOOP1(i, n, x) { \
+  x \
+  i += n; \
+}
+
+#define KRML_LOOP2(i, n, x) \
+  KRML_LOOP1(i, n, x) \
+  KRML_LOOP1(i, n, x)
+
+#define KRML_LOOP3(i, n, x) \
+  KRML_LOOP2(i, n, x) \
+  KRML_LOOP1(i, n, x)
+
+#define KRML_LOOP4(i, n, x) \
+  KRML_LOOP2(i, n, x) \
+  KRML_LOOP2(i, n, x)
+
+#define KRML_LOOP5(i, n, x) \
+  KRML_LOOP4(i, n, x) \
+  KRML_LOOP1(i, n, x)
+
+#define KRML_LOOP6(i, n, x) \
+  KRML_LOOP4(i, n, x) \
+  KRML_LOOP2(i, n, x)
+
+#define KRML_LOOP7(i, n, x) \
+  KRML_LOOP4(i, n, x) \
+  KRML_LOOP3(i, n, x)
+
+#define KRML_LOOP8(i, n, x) \
+  KRML_LOOP4(i, n, x) \
+  KRML_LOOP4(i, n, x)
+
+#define KRML_LOOP9(i, n, x) \
+  KRML_LOOP8(i, n, x) \
+  KRML_LOOP1(i, n, x)
+
+#define KRML_LOOP10(i, n, x) \
+  KRML_LOOP8(i, n, x) \
+  KRML_LOOP2(i, n, x)
+
+#define KRML_LOOP11(i, n, x) \
+  KRML_LOOP8(i, n, x) \
+  KRML_LOOP3(i, n, x)
+
+#define KRML_LOOP12(i, n, x) \
+  KRML_LOOP8(i, n, x) \
+  KRML_LOOP4(i, n, x)
+
+#define KRML_LOOP13(i, n, x) \
+  KRML_LOOP8(i, n, x) \
+  KRML_LOOP5(i, n, x)
+
+#define KRML_LOOP14(i, n, x) \
+  KRML_LOOP8(i, n, x) \
+  KRML_LOOP6(i, n, x)
+
+#define KRML_LOOP15(i, n, x) \
+  KRML_LOOP8(i, n, x) \
+  KRML_LOOP7(i, n, x)
+
+#define KRML_LOOP16(i, n, x) \
+  KRML_LOOP8(i, n, x) \
+  KRML_LOOP8(i, n, x)
+
+#define KRML_UNROLL_FOR(i, z, n, k, x) do { \
+  uint32_t i = z; \
+  KRML_LOOP##n(i, k, x) \
+} while (0)
+
+#define KRML_ACTUAL_FOR(i, z, n, k, x) \
+  do { \
+    for (uint32_t i = z; i < n; i += k) { \
+      x \
+    } \
+  } while (0)
+
+#ifndef KRML_UNROLL_MAX
+#define KRML_UNROLL_MAX 16
+#endif
+
+/* 1 is the number of loop iterations, i.e. (n - z)/k as evaluated by krml */
+#if 0 <= KRML_UNROLL_MAX
+#define KRML_MAYBE_FOR0(i, z, n, k, x)
+#else
+#define KRML_MAYBE_FOR0(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
+#endif
+
+#if 1 <= KRML_UNROLL_MAX
+#define KRML_MAYBE_FOR1(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 1, k, x)
+#else
+#define KRML_MAYBE_FOR1(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
+#endif
+
+#if 2 <= KRML_UNROLL_MAX
+#define KRML_MAYBE_FOR2(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 2, k, x)
+#else
+#define KRML_MAYBE_FOR2(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
+#endif
+
+#if 3 <= KRML_UNROLL_MAX
+#define KRML_MAYBE_FOR3(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 3, k, x)
+#else
+#define KRML_MAYBE_FOR3(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
+#endif
+
+#if 4 <= KRML_UNROLL_MAX
+#define KRML_MAYBE_FOR4(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 4, k, x)
+#else
+#define KRML_MAYBE_FOR4(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
+#endif
+
+#if 5 <= KRML_UNROLL_MAX
+#define KRML_MAYBE_FOR5(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 5, k, x)
+#else
+#define KRML_MAYBE_FOR5(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
+#endif
+
+#if 6 <= KRML_UNROLL_MAX
+#define KRML_MAYBE_FOR6(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 6, k, x)
+#else
+#define KRML_MAYBE_FOR6(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
+#endif
+
+#if 7 <= KRML_UNROLL_MAX
+#define KRML_MAYBE_FOR7(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 7, k, x)
+#else
+#define KRML_MAYBE_FOR7(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
+#endif
+
+#if 8 <= KRML_UNROLL_MAX
+#define KRML_MAYBE_FOR8(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 8, k, x)
+#else
+#define KRML_MAYBE_FOR8(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
+#endif
+
+#if 9 <= KRML_UNROLL_MAX
+#define KRML_MAYBE_FOR9(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 9, k, x)
+#else
+#define KRML_MAYBE_FOR9(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
+#endif
+
+#if 10 <= KRML_UNROLL_MAX
+#define KRML_MAYBE_FOR10(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 10, k, x)
+#else
+#define KRML_MAYBE_FOR10(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
+#endif
+
+#if 11 <= KRML_UNROLL_MAX
+#define KRML_MAYBE_FOR11(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 11, k, x)
+#else
+#define KRML_MAYBE_FOR11(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
+#endif
+
+#if 12 <= KRML_UNROLL_MAX
+#define KRML_MAYBE_FOR12(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 12, k, x)
+#else
+#define KRML_MAYBE_FOR12(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
+#endif
+
+#if 13 <= KRML_UNROLL_MAX
+#define KRML_MAYBE_FOR13(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 13, k, x)
+#else
+#define KRML_MAYBE_FOR13(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
+#endif
+
+#if 14 <= KRML_UNROLL_MAX
+#define KRML_MAYBE_FOR14(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 14, k, x)
+#else
+#define KRML_MAYBE_FOR14(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
+#endif
+
+#if 15 <= KRML_UNROLL_MAX
+#define KRML_MAYBE_FOR15(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 15, k, x)
+#else
+#define KRML_MAYBE_FOR15(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
+#endif
+
+#if 16 <= KRML_UNROLL_MAX
+#define KRML_MAYBE_FOR16(i, z, n, k, x) KRML_UNROLL_FOR(i, z, 16, k, x)
+#else
+#define KRML_MAYBE_FOR16(i, z, n, k, x) KRML_ACTUAL_FOR(i, z, n, k, x)
+#endif
+#endif
diff --git a/contrib/tools/python3/Modules/_hacl/include/krml/lowstar_endianness.h b/contrib/tools/python3/Modules/_hacl/include/krml/lowstar_endianness.h
new file mode 100644
index 00000000000..b6c648602b9
--- /dev/null
+++ b/contrib/tools/python3/Modules/_hacl/include/krml/lowstar_endianness.h
@@ -0,0 +1,231 @@
+/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
+   Licensed under the Apache 2.0 License. */
+
+#ifndef __LOWSTAR_ENDIANNESS_H
+#define __LOWSTAR_ENDIANNESS_H
+
+#include <string.h>
+#include <inttypes.h>
+
+/******************************************************************************/
+/* Implementing C.fst (part 2: endian-ness macros)                            */
+/******************************************************************************/
+
+/* ... for Linux */
+#if defined(__linux__) || defined(__CYGWIN__) || defined (__USE_SYSTEM_ENDIAN_H__) || defined(__GLIBC__)
+#  include <endian.h>
+
+/* ... for OSX */
+#elif defined(__APPLE__)
+#  include <libkern/OSByteOrder.h>
+#  define htole64(x) OSSwapHostToLittleInt64(x)
+#  define le64toh(x) OSSwapLittleToHostInt64(x)
+#  define htobe64(x) OSSwapHostToBigInt64(x)
+#  define be64toh(x) OSSwapBigToHostInt64(x)
+
+#  define htole16(x) OSSwapHostToLittleInt16(x)
+#  define le16toh(x) OSSwapLittleToHostInt16(x)
+#  define htobe16(x) OSSwapHostToBigInt16(x)
+#  define be16toh(x) OSSwapBigToHostInt16(x)
+
+#  define htole32(x) OSSwapHostToLittleInt32(x)
+#  define le32toh(x) OSSwapLittleToHostInt32(x)
+#  define htobe32(x) OSSwapHostToBigInt32(x)
+#  define be32toh(x) OSSwapBigToHostInt32(x)
+
+/* ... for Solaris */
+#elif defined(__sun__)
+#  error #include <sys/byteorder.h>
+#  define htole64(x) LE_64(x)
+#  define le64toh(x) LE_64(x)
+#  define htobe64(x) BE_64(x)
+#  define be64toh(x) BE_64(x)
+
+#  define htole16(x) LE_16(x)
+#  define le16toh(x) LE_16(x)
+#  define htobe16(x) BE_16(x)
+#  define be16toh(x) BE_16(x)
+
+#  define htole32(x) LE_32(x)
+#  define le32toh(x) LE_32(x)
+#  define htobe32(x) BE_32(x)
+#  define be32toh(x) BE_32(x)
+
+/* ... for the BSDs */
+#elif defined(__FreeBSD__) || defined(__NetBSD__) || defined(__DragonFly__)
+#  include <sys/endian.h>
+#elif defined(__OpenBSD__)
+#  include <endian.h>
+
+/* ... for Windows (MSVC)... not targeting XBOX 360! */
+#elif defined(_MSC_VER)
+
+#  include <stdlib.h>
+#  define htobe16(x) _byteswap_ushort(x)
+#  define htole16(x) (x)
+#  define be16toh(x) _byteswap_ushort(x)
+#  define le16toh(x) (x)
+
+#  define htobe32(x) _byteswap_ulong(x)
+#  define htole32(x) (x)
+#  define be32toh(x) _byteswap_ulong(x)
+#  define le32toh(x) (x)
+
+#  define htobe64(x) _byteswap_uint64(x)
+#  define htole64(x) (x)
+#  define be64toh(x) _byteswap_uint64(x)
+#  define le64toh(x) (x)
+
+/* ... for Windows (GCC-like, e.g. mingw or clang) */
+#elif (defined(_WIN32) || defined(_WIN64) || defined(__EMSCRIPTEN__)) &&       \
+    (defined(__GNUC__) || defined(__clang__))
+
+#  define htobe16(x) __builtin_bswap16(x)
+#  define htole16(x) (x)
+#  define be16toh(x) __builtin_bswap16(x)
+#  define le16toh(x) (x)
+
+#  define htobe32(x) __builtin_bswap32(x)
+#  define htole32(x) (x)
+#  define be32toh(x) __builtin_bswap32(x)
+#  define le32toh(x) (x)
+
+#  define htobe64(x) __builtin_bswap64(x)
+#  define htole64(x) (x)
+#  define be64toh(x) __builtin_bswap64(x)
+#  define le64toh(x) (x)
+
+/* ... generic big-endian fallback code */
+/* ... AIX doesn't have __BYTE_ORDER__ (with XLC compiler) & is always big-endian */
+#elif (defined(__BYTE_ORDER__) && __BYTE_ORDER__ == __ORDER_BIG_ENDIAN__) || defined(_AIX)
+
+/* byte swapping code inspired by:
+ * https://github.com/rweather/arduinolibs/blob/master/libraries/Crypto/utility/EndianUtil.h
+ * */
+
+#  define htobe32(x) (x)
+#  define be32toh(x) (x)
+#  define htole32(x)                                                           \
+    (__extension__({                                                           \
+      uint32_t _temp = (x);                                                    \
+      ((_temp >> 24) & 0x000000FF) | ((_temp >> 8) & 0x0000FF00) |             \
+          ((_temp << 8) & 0x00FF0000) | ((_temp << 24) & 0xFF000000);          \
+    }))
+#  define le32toh(x) (htole32((x)))
+
+#  define htobe64(x) (x)
+#  define be64toh(x) (x)
+#  define htole64(x)                                                           \
+    (__extension__({                                                           \
+      uint64_t __temp = (x);                                                   \
+      uint32_t __low = htobe32((uint32_t)__temp);                              \
+      uint32_t __high = htobe32((uint32_t)(__temp >> 32));                     \
+      (((uint64_t)__low) << 32) | __high;                                      \
+    }))
+#  define le64toh(x) (htole64((x)))
+
+/* ... generic little-endian fallback code */
+#elif defined(__BYTE_ORDER__) && __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
+
+#  define htole32(x) (x)
+#  define le32toh(x) (x)
+#  define htobe32(x)                                                           \
+    (__extension__({                                                           \
+      uint32_t _temp = (x);                                                    \
+      ((_temp >> 24) & 0x000000FF) | ((_temp >> 8) & 0x0000FF00) |             \
+          ((_temp << 8) & 0x00FF0000) | ((_temp << 24) & 0xFF000000);          \
+    }))
+#  define be32toh(x) (htobe32((x)))
+
+#  define htole64(x) (x)
+#  define le64toh(x) (x)
+#  define htobe64(x)                                                           \
+    (__extension__({                                                           \
+      uint64_t __temp = (x);                                                   \
+      uint32_t __low = htobe32((uint32_t)__temp);                              \
+      uint32_t __high = htobe32((uint32_t)(__temp >> 32));                     \
+      (((uint64_t)__low) << 32) | __high;                                      \
+    }))
+#  define be64toh(x) (htobe64((x)))
+
+/* ... couldn't determine endian-ness of the target platform */
+#else
+#  error "Please define __BYTE_ORDER__!"
+
+#endif /* defined(__linux__) || ... */
+
+/* Loads and stores. These avoid undefined behavior due to unaligned memory
+ * accesses, via memcpy. */
+
+inline static uint16_t load16(uint8_t *b) {
+  uint16_t x;
+  memcpy(&x, b, 2);
+  return x;
+}
+
+inline static uint32_t load32(uint8_t *b) {
+  uint32_t x;
+  memcpy(&x, b, 4);
+  return x;
+}
+
+inline static uint64_t load64(uint8_t *b) {
+  uint64_t x;
+  memcpy(&x, b, 8);
+  return x;
+}
+
+inline static void store16(uint8_t *b, uint16_t i) {
+  memcpy(b, &i, 2);
+}
+
+inline static void store32(uint8_t *b, uint32_t i) {
+  memcpy(b, &i, 4);
+}
+
+inline static void store64(uint8_t *b, uint64_t i) {
+  memcpy(b, &i, 8);
+}
+
+/* Legacy accessors so that this header can serve as an implementation of
+ * C.Endianness */
+#define load16_le(b) (le16toh(load16(b)))
+#define store16_le(b, i) (store16(b, htole16(i)))
+#define load16_be(b) (be16toh(load16(b)))
+#define store16_be(b, i) (store16(b, htobe16(i)))
+
+#define load32_le(b) (le32toh(load32(b)))
+#define store32_le(b, i) (store32(b, htole32(i)))
+#define load32_be(b) (be32toh(load32(b)))
+#define store32_be(b, i) (store32(b, htobe32(i)))
+
+#define load64_le(b) (le64toh(load64(b)))
+#define store64_le(b, i) (store64(b, htole64(i)))
+#define load64_be(b) (be64toh(load64(b)))
+#define store64_be(b, i) (store64(b, htobe64(i)))
+
+/* Co-existence of LowStar.Endianness and FStar.Endianness generates name
+ * conflicts, because of course both insist on having no prefixes. Until a
+ * prefix is added, or until we truly retire FStar.Endianness, solve this issue
+ * in an elegant way. */
+#define load16_le0 load16_le
+#define store16_le0 store16_le
+#define load16_be0 load16_be
+#define store16_be0 store16_be
+
+#define load32_le0 load32_le
+#define store32_le0 store32_le
+#define load32_be0 load32_be
+#define store32_be0 store32_be
+
+#define load64_le0 load64_le
+#define store64_le0 store64_le
+#define load64_be0 load64_be
+#define store64_be0 store64_be
+
+#define load128_le0 load128_le
+#define store128_le0 store128_le
+#define load128_be0 load128_be
+#define store128_be0 store128_be
+
+#endif
diff --git a/contrib/tools/python3/Modules/_hacl/include/krml/types.h b/contrib/tools/python3/Modules/_hacl/include/krml/types.h
new file mode 100644
index 00000000000..509f555536e
--- /dev/null
+++ b/contrib/tools/python3/Modules/_hacl/include/krml/types.h
@@ -0,0 +1,14 @@
+#pragma once
+
+#include <inttypes.h>
+
+typedef struct FStar_UInt128_uint128_s {
+  uint64_t low;
+  uint64_t high;
+} FStar_UInt128_uint128, uint128_t;
+
+#define KRML_VERIFIED_UINT128
+
+#include "krml/lowstar_endianness.h"
+#include "krml/fstar_uint128_struct_endianness.h"
+#include "krml/FStar_UInt128_Verified.h"