Adding upstream version 115.7.0esr.upstream/115.7.0esr

Signed-off-by: Daniel Baumann <daniel.baumann@progress-linux.org>

10 files changed, 1597 insertions, 0 deletions

diff --git a/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/FStar_UInt128.h b/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/FStar_UInt128.h
new file mode 100644
index 0000000000..4affcee353
--- /dev/null
+++ b/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/FStar_UInt128.h
@@ -0,0 +1,75 @@
+/*
+  Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
+  Licensed under the Apache 2.0 License.
+*/
+
+#ifndef __FStar_UInt128_H
+#define __FStar_UInt128_H
+
+#include <inttypes.h>
+#include <stdbool.h>
+#include "krml/internal/compat.h"
+#include "krml/lowstar_endianness.h"
+#include "krml/internal/types.h"
+#include "krml/internal/target.h"
+static inline FStar_UInt128_uint128
+FStar_UInt128_add(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_add_underspec(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_add_mod(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_sub(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_sub_underspec(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_sub_mod(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_logand(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_logxor(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_logor(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+static inline FStar_UInt128_uint128 FStar_UInt128_lognot(FStar_UInt128_uint128 a);
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_shift_left(FStar_UInt128_uint128 a, uint32_t s);
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_shift_right(FStar_UInt128_uint128 a, uint32_t s);
+
+static inline bool FStar_UInt128_eq(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+static inline bool FStar_UInt128_gt(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+static inline bool FStar_UInt128_lt(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+static inline bool FStar_UInt128_gte(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+static inline bool FStar_UInt128_lte(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_eq_mask(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_gte_mask(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
+
+static inline FStar_UInt128_uint128 FStar_UInt128_uint64_to_uint128(uint64_t a);
+
+static inline uint64_t FStar_UInt128_uint128_to_uint64(FStar_UInt128_uint128 a);
+
+static inline FStar_UInt128_uint128 FStar_UInt128_mul32(uint64_t x, uint32_t y);
+
+static inline FStar_UInt128_uint128 FStar_UInt128_mul_wide(uint64_t x, uint64_t y);
+
+#define __FStar_UInt128_H_DEFINED
+#endif
diff --git a/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/FStar_UInt128_Verified.h b/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/FStar_UInt128_Verified.h
new file mode 100644
index 0000000000..8f235c3146
--- /dev/null
+++ b/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/FStar_UInt128_Verified.h
@@ -0,0 +1,327 @@
+/*
+  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/internal/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/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/FStar_UInt_8_16_32_64.h b/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/FStar_UInt_8_16_32_64.h
new file mode 100644
index 0000000000..51f3eead1e
--- /dev/null
+++ b/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/FStar_UInt_8_16_32_64.h
@@ -0,0 +1,218 @@
+/*
+  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/internal/compat.h"
+#include "krml/lowstar_endianness.h"
+#include "krml/internal/types.h"
+#include "krml/internal/target.h"
+extern Prims_int FStar_UInt64_n;
+
+extern bool FStar_UInt64_uu___is_Mk(uint64_t projectee);
+
+extern Prims_int FStar_UInt64___proj__Mk__item__v(uint64_t projectee);
+
+extern Prims_int FStar_UInt64_v(uint64_t x);
+
+extern uint64_t FStar_UInt64_uint_to_t(Prims_int x);
+
+extern uint64_t FStar_UInt64_zero;
+
+extern uint64_t FStar_UInt64_one;
+
+extern uint64_t FStar_UInt64_minus(uint64_t a);
+
+extern uint32_t FStar_UInt64_n_minus_one;
+
+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;
+}
+
+extern Prims_string FStar_UInt64_to_string(uint64_t uu___);
+
+extern Prims_string FStar_UInt64_to_string_hex(uint64_t uu___);
+
+extern Prims_string FStar_UInt64_to_string_hex_pad(uint64_t uu___);
+
+extern uint64_t FStar_UInt64_of_string(Prims_string uu___);
+
+extern Prims_int FStar_UInt32_n;
+
+extern bool FStar_UInt32_uu___is_Mk(uint32_t projectee);
+
+extern Prims_int FStar_UInt32___proj__Mk__item__v(uint32_t projectee);
+
+extern Prims_int FStar_UInt32_v(uint32_t x);
+
+extern uint32_t FStar_UInt32_uint_to_t(Prims_int x);
+
+extern uint32_t FStar_UInt32_zero;
+
+extern uint32_t FStar_UInt32_one;
+
+extern uint32_t FStar_UInt32_minus(uint32_t a);
+
+extern uint32_t FStar_UInt32_n_minus_one;
+
+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;
+}
+
+extern Prims_string FStar_UInt32_to_string(uint32_t uu___);
+
+extern Prims_string FStar_UInt32_to_string_hex(uint32_t uu___);
+
+extern Prims_string FStar_UInt32_to_string_hex_pad(uint32_t uu___);
+
+extern uint32_t FStar_UInt32_of_string(Prims_string uu___);
+
+extern Prims_int FStar_UInt16_n;
+
+extern bool FStar_UInt16_uu___is_Mk(uint16_t projectee);
+
+extern Prims_int FStar_UInt16___proj__Mk__item__v(uint16_t projectee);
+
+extern Prims_int FStar_UInt16_v(uint16_t x);
+
+extern uint16_t FStar_UInt16_uint_to_t(Prims_int x);
+
+extern uint16_t FStar_UInt16_zero;
+
+extern uint16_t FStar_UInt16_one;
+
+extern uint16_t FStar_UInt16_minus(uint16_t a);
+
+extern uint32_t FStar_UInt16_n_minus_one;
+
+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;
+}
+
+extern Prims_string FStar_UInt16_to_string(uint16_t uu___);
+
+extern Prims_string FStar_UInt16_to_string_hex(uint16_t uu___);
+
+extern Prims_string FStar_UInt16_to_string_hex_pad(uint16_t uu___);
+
+extern uint16_t FStar_UInt16_of_string(Prims_string uu___);
+
+extern Prims_int FStar_UInt8_n;
+
+extern bool FStar_UInt8_uu___is_Mk(uint8_t projectee);
+
+extern Prims_int FStar_UInt8___proj__Mk__item__v(uint8_t projectee);
+
+extern Prims_int FStar_UInt8_v(uint8_t x);
+
+extern uint8_t FStar_UInt8_uint_to_t(Prims_int x);
+
+extern uint8_t FStar_UInt8_zero;
+
+extern uint8_t FStar_UInt8_one;
+
+extern uint8_t FStar_UInt8_minus(uint8_t a);
+
+extern uint32_t FStar_UInt8_n_minus_one;
+
+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;
+}
+
+extern Prims_string FStar_UInt8_to_string(uint8_t uu___);
+
+extern Prims_string FStar_UInt8_to_string_hex(uint8_t uu___);
+
+extern Prims_string FStar_UInt8_to_string_hex_pad(uint8_t uu___);
+
+extern uint8_t FStar_UInt8_of_string(Prims_string uu___);
+
+typedef uint8_t FStar_UInt8_byte;
+
+#define __FStar_UInt_8_16_32_64_H_DEFINED
+#endif
diff --git a/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/LowStar_Endianness.h b/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/LowStar_Endianness.h
new file mode 100644
index 0000000000..5feb077a48
--- /dev/null
+++ b/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/LowStar_Endianness.h
@@ -0,0 +1,25 @@
+/*
+  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 "FStar_UInt128.h"
+#include <inttypes.h>
+#include <stdbool.h>
+#include "krml/internal/compat.h"
+#include "krml/lowstar_endianness.h"
+#include "krml/internal/types.h"
+#include "krml/internal/target.h"
+static inline void store128_le(uint8_t *x0, FStar_UInt128_uint128 x1);
+
+static inline FStar_UInt128_uint128 load128_le(uint8_t *x0);
+
+static inline void store128_be(uint8_t *x0, FStar_UInt128_uint128 x1);
+
+static inline FStar_UInt128_uint128 load128_be(uint8_t *x0);
+
+#define __LowStar_Endianness_H_DEFINED
+#endif
diff --git a/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/Makefile.basic b/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/Makefile.basic
new file mode 100644
index 0000000000..672b58015c
--- /dev/null
+++ b/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/Makefile.basic
@@ -0,0 +1,56 @@
+# A basic Makefile that KaRaMeL copies in the output directory; this is not
+# guaranteed to work and will only work well for very simple projects. This
+# Makefile uses:
+# - the custom C files passed to your krml invocation
+# - the custom C flags passed to your krml invocation
+# - the -o option passed to your krml invocation
+
+include Makefile.include
+
+ifeq (,$(KRML_HOME))
+  $(error please define KRML_HOME to point to the root of your KaRaMeL git checkout)
+endif
+
+CFLAGS 	+= -I. -I $(KRML_HOME)/include -I $(KRML_HOME)/krmllib/dist/minimal
+CFLAGS 	+= -Wall -Wextra -Werror -std=c11 -Wno-unused-variable \
+  -Wno-unknown-warning-option -Wno-unused-but-set-variable -Wno-unused-function \
+  -Wno-unused-parameter -Wno-infinite-recursion \
+  -g -fwrapv -D_BSD_SOURCE -D_DEFAULT_SOURCE
+ifeq ($(OS),Windows_NT)
+CFLAGS 	+= -D__USE_MINGW_ANSI_STDIO
+else
+CFLAGS 	+= -fPIC
+endif
+CFLAGS 	+= $(USER_CFLAGS)
+
+SOURCES += $(ALL_C_FILES) $(USER_C_FILES)
+ifneq (,$(BLACKLIST))
+  SOURCES := $(filter-out $(BLACKLIST),$(SOURCES))
+endif
+OBJS 	+= $(patsubst %.c,%.o,$(SOURCES))
+
+all: $(USER_TARGET)
+
+$(USER_TARGET): $(OBJS)
+
+AR ?= ar
+
+%.a:
+	$(AR) cr $@ $^
+
+%.exe:
+	$(CC) $(CFLAGS) -o $@ $^ $(KRML_HOME)/krmllib/dist/generic/libkrmllib.a
+
+%.so:
+	$(CC) $(CFLAGS) -shared -o $@ $^
+
+%.d: %.c
+	@set -e; rm -f $@; \
+	  $(CC) -MM $(CFLAGS) $< > $@.$$$$; \
+	  sed 's,\($(notdir $*)\)\.o[ :]*,$(dir $@)\1.o $@ : ,g' < $@.$$$$ > $@; \
+	  rm -f $@.$$$$
+
+include $(patsubst %.c,%.d,$(SOURCES))
+
+clean:
+	rm -rf *.o *.d $(USER_TARGET)
diff --git a/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/Makefile.include b/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/Makefile.include
new file mode 100644
index 0000000000..ad53217184
--- /dev/null
+++ b/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/Makefile.include
@@ -0,0 +1,5 @@
+USER_TARGET=libkrmllib.a
+USER_CFLAGS=
+USER_C_FILES=fstar_uint128.c
+ALL_C_FILES=
+ALL_H_FILES=FStar_UInt128.h FStar_UInt_8_16_32_64.h LowStar_Endianness.h
diff --git a/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/fstar_uint128_gcc64.h b/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/fstar_uint128_gcc64.h
new file mode 100644
index 0000000000..33cff6b6d4
--- /dev/null
+++ b/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/fstar_uint128_gcc64.h
@@ -0,0 +1,225 @@
+/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
+   Licensed under the Apache 2.0 License. */
+
+/******************************************************************************/
+/* Machine integers (128-bit arithmetic)                                      */
+/******************************************************************************/
+
+/* This header contains two things.
+ *
+ * First, an implementation of 128-bit arithmetic suitable for 64-bit GCC and
+ * Clang, i.e. all the operations from FStar.UInt128.
+ *
+ * Second, 128-bit operations from C.Endianness (or LowStar.Endianness),
+ * suitable for any compiler and platform (via a series of ifdefs). This second
+ * part is unfortunate, and should be fixed by moving {load,store}128_{be,le} to
+ * FStar.UInt128 to avoid a maze of preprocessor guards and hand-written code.
+ * */
+
+/* This file is used for both the minimal and generic krmllib distributions. As
+ * such, it assumes that the machine integers have been bundled the exact same
+ * way in both cases. */
+
+#ifndef FSTAR_UINT128_GCC64
+#define FSTAR_UINT128_GCC64
+
+#include "FStar_UInt128.h"
+#include "FStar_UInt_8_16_32_64.h"
+#include "LowStar_Endianness.h"
+
+/* GCC + using native unsigned __int128 support */
+
+inline static 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);
+}
+
+inline static void
+store128_le(uint8_t *b, uint128_t n)
+{
+    store64_le(b, (uint64_t)n);
+    store64_le(b + 8, (uint64_t)(n >> 64));
+}
+
+inline static 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);
+}
+
+inline static void
+store128_be(uint8_t *b, uint128_t n)
+{
+    store64_be(b, (uint64_t)(n >> 64));
+    store64_be(b + 8, (uint64_t)n);
+}
+
+inline static uint128_t
+FStar_UInt128_add(uint128_t x, uint128_t y)
+{
+    return x + y;
+}
+
+inline static uint128_t
+FStar_UInt128_mul(uint128_t x, uint128_t y)
+{
+    return x * y;
+}
+
+inline static uint128_t
+FStar_UInt128_add_mod(uint128_t x, uint128_t y)
+{
+    return x + y;
+}
+
+inline static uint128_t
+FStar_UInt128_sub(uint128_t x, uint128_t y)
+{
+    return x - y;
+}
+
+inline static uint128_t
+FStar_UInt128_sub_mod(uint128_t x, uint128_t y)
+{
+    return x - y;
+}
+
+inline static uint128_t
+FStar_UInt128_logand(uint128_t x, uint128_t y)
+{
+    return x & y;
+}
+
+inline static uint128_t
+FStar_UInt128_logor(uint128_t x, uint128_t y)
+{
+    return x | y;
+}
+
+inline static uint128_t
+FStar_UInt128_logxor(uint128_t x, uint128_t y)
+{
+    return x ^ y;
+}
+
+inline static uint128_t
+FStar_UInt128_lognot(uint128_t x)
+{
+    return ~x;
+}
+
+inline static uint128_t
+FStar_UInt128_shift_left(uint128_t x, uint32_t y)
+{
+    return x << y;
+}
+
+inline static uint128_t
+FStar_UInt128_shift_right(uint128_t x, uint32_t y)
+{
+    return x >> y;
+}
+
+inline static uint128_t
+FStar_UInt128_uint64_to_uint128(uint64_t x)
+{
+    return (uint128_t)x;
+}
+
+inline static uint64_t
+FStar_UInt128_uint128_to_uint64(uint128_t x)
+{
+    return (uint64_t)x;
+}
+
+inline static uint128_t
+FStar_UInt128_mul_wide(uint64_t x, uint64_t y)
+{
+    return ((uint128_t)x) * y;
+}
+
+inline static 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;
+}
+
+inline static 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;
+}
+
+inline static uint64_t
+FStar_UInt128___proj__Mkuint128__item__low(uint128_t x)
+{
+    return (uint64_t)x;
+}
+
+inline static uint64_t
+FStar_UInt128___proj__Mkuint128__item__high(uint128_t x)
+{
+    return (uint64_t)(x >> 64);
+}
+
+inline static uint128_t
+FStar_UInt128_add_underspec(uint128_t x, uint128_t y)
+{
+    return x + y;
+}
+
+inline static uint128_t
+FStar_UInt128_sub_underspec(uint128_t x, uint128_t y)
+{
+    return x - y;
+}
+
+inline static bool
+FStar_UInt128_eq(uint128_t x, uint128_t y)
+{
+    return x == y;
+}
+
+inline static bool
+FStar_UInt128_gt(uint128_t x, uint128_t y)
+{
+    return x > y;
+}
+
+inline static bool
+FStar_UInt128_lt(uint128_t x, uint128_t y)
+{
+    return x < y;
+}
+
+inline static bool
+FStar_UInt128_gte(uint128_t x, uint128_t y)
+{
+    return x >= y;
+}
+
+inline static bool
+FStar_UInt128_lte(uint128_t x, uint128_t y)
+{
+    return x <= y;
+}
+
+inline static uint128_t
+FStar_UInt128_mul32(uint64_t x, uint32_t y)
+{
+    return (uint128_t)x * (uint128_t)y;
+}
+
+#endif
diff --git a/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/fstar_uint128_msvc.h b/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/fstar_uint128_msvc.h
new file mode 100644
index 0000000000..e9b366e259
--- /dev/null
+++ b/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/fstar_uint128_msvc.h
@@ -0,0 +1,571 @@
+/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
+   Licensed under the Apache 2.0 License. */
+
+/* This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
+ * then hand-edited to use MSVC intrinsics KaRaMeL invocation:
+ * C:\users\barrybo\mitls2c\karamel\_build\src\Karamel.native -minimal -fnouint128 C:/users/barrybo/mitls2c/FStar/ulib/FStar.UInt128.fst -tmpdir ../secure_api/out/runtime_switch/uint128 -skip-compilation -add-include "krmllib0.h" -drop FStar.Int.Cast.Full -bundle FStar.UInt128=FStar.*,Prims
+ * F* version: 15104ff8
+ * KaRaMeL version: 318b7fa8
+ */
+
+#ifndef FSTAR_UINT128_MSVC
+#define FSTAR_UINT128_MSVC
+
+#include "krml/internal/types.h"
+#include "FStar_UInt128.h"
+#include "FStar_UInt_8_16_32_64.h"
+
+#ifndef _MSC_VER
+#error This file only works with the MSVC compiler
+#endif
+
+/* JP: need to rip out HAS_OPTIMIZED since the header guards in types.h are now
+ * done properly and only include this file when we know for sure we are on
+ * 64-bit MSVC. */
+
+#if defined(_M_X64) && !defined(KRML_VERIFIED_UINT128)
+#define HAS_OPTIMIZED 1
+#else
+#define HAS_OPTIMIZED 0
+#endif
+
+// Define .low and .high in terms of the __m128i fields, to reduce
+// the amount of churn in this file.
+#if HAS_OPTIMIZED
+#include <intrin.h>
+#include <immintrin.h>
+#define low m128i_u64[0]
+#define high m128i_u64[1]
+#endif
+
+inline static FStar_UInt128_uint128
+load128_le(uint8_t *b)
+{
+#if HAS_OPTIMIZED
+    return _mm_loadu_si128((__m128i *)b);
+#else
+    FStar_UInt128_uint128 lit;
+    lit.low = load64_le(b);
+    lit.high = load64_le(b + 8);
+    return lit;
+#endif
+}
+
+inline static void
+store128_le(uint8_t *b, FStar_UInt128_uint128 n)
+{
+    store64_le(b, n.low);
+    store64_le(b + 8, n.high);
+}
+
+inline static FStar_UInt128_uint128
+load128_be(uint8_t *b)
+{
+    uint64_t l = load64_be(b + 8);
+    uint64_t h = load64_be(b);
+#if HAS_OPTIMIZED
+    return _mm_set_epi64x(h, l);
+#else
+    FStar_UInt128_uint128 lit;
+    lit.low = l;
+    lit.high = h;
+    return lit;
+#endif
+}
+
+inline static void
+store128_be(uint8_t *b, uint128_t n)
+{
+    store64_be(b, n.high);
+    store64_be(b + 8, n.low);
+}
+
+inline static uint64_t
+FStar_UInt128_constant_time_carry(uint64_t a, uint64_t b)
+{
+    return (a ^ (a ^ b | a - b ^ b)) >> (uint32_t)63U;
+}
+
+inline static uint64_t
+FStar_UInt128_carry(uint64_t a, uint64_t b)
+{
+    return FStar_UInt128_constant_time_carry(a, b);
+}
+
+inline static FStar_UInt128_uint128
+FStar_UInt128_add(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+#if HAS_OPTIMIZED
+    uint64_t l, h;
+
+    unsigned char carry =
+        _addcarry_u64(0, a.low, b.low, &l);   // low/CF = a.low+b.low+0
+    _addcarry_u64(carry, a.high, b.high, &h); // high   = a.high+b.high+CF
+    return _mm_set_epi64x(h, l);
+#else
+    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;
+#endif
+}
+
+inline static FStar_UInt128_uint128
+FStar_UInt128_add_underspec(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+#if HAS_OPTIMIZED
+    return FStar_UInt128_add(a, b);
+#else
+    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;
+#endif
+}
+
+inline static FStar_UInt128_uint128
+FStar_UInt128_add_mod(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+#if HAS_OPTIMIZED
+    return FStar_UInt128_add(a, b);
+#else
+    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;
+#endif
+}
+
+inline static FStar_UInt128_uint128
+FStar_UInt128_sub(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+#if HAS_OPTIMIZED
+    uint64_t l, h;
+
+    unsigned char borrow = _subborrow_u64(0, a.low, b.low, &l);
+    _subborrow_u64(borrow, a.high, b.high, &h);
+    return _mm_set_epi64x(h, l);
+#else
+    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;
+#endif
+}
+
+inline static FStar_UInt128_uint128
+FStar_UInt128_sub_underspec(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+#if HAS_OPTIMIZED
+    return FStar_UInt128_sub(a, b);
+#else
+    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;
+#endif
+}
+
+inline static 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;
+}
+
+inline static FStar_UInt128_uint128
+FStar_UInt128_sub_mod(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+#if HAS_OPTIMIZED
+    return FStar_UInt128_sub(a, b);
+#else
+    return FStar_UInt128_sub_mod_impl(a, b);
+#endif
+}
+
+inline static FStar_UInt128_uint128
+FStar_UInt128_logand(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+#if HAS_OPTIMIZED
+    return _mm_and_si128(a, b);
+#else
+    FStar_UInt128_uint128 lit;
+    lit.low = a.low & b.low;
+    lit.high = a.high & b.high;
+    return lit;
+#endif
+}
+
+inline static FStar_UInt128_uint128
+FStar_UInt128_logxor(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+#if HAS_OPTIMIZED
+    return _mm_xor_si128(a, b);
+#else
+    FStar_UInt128_uint128 lit;
+    lit.low = a.low ^ b.low;
+    lit.high = a.high ^ b.high;
+    return lit;
+#endif
+}
+
+inline static FStar_UInt128_uint128
+FStar_UInt128_logor(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+#if HAS_OPTIMIZED
+    return _mm_or_si128(a, b);
+#else
+    FStar_UInt128_uint128 lit;
+    lit.low = a.low | b.low;
+    lit.high = a.high | b.high;
+    return lit;
+#endif
+}
+
+inline static FStar_UInt128_uint128
+FStar_UInt128_lognot(FStar_UInt128_uint128 a)
+{
+#if HAS_OPTIMIZED
+    return _mm_andnot_si128(a, a);
+#else
+    FStar_UInt128_uint128 lit;
+    lit.low = ~a.low;
+    lit.high = ~a.high;
+    return lit;
+#endif
+}
+
+static const uint32_t FStar_UInt128_u32_64 = (uint32_t)64U;
+
+inline static 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);
+}
+
+inline static 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);
+}
+
+inline static 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;
+    }
+}
+
+inline static 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;
+}
+
+inline static FStar_UInt128_uint128
+FStar_UInt128_shift_left(FStar_UInt128_uint128 a, uint32_t s)
+{
+#if HAS_OPTIMIZED
+    if (s == 0) {
+        return a;
+    } else if (s < FStar_UInt128_u32_64) {
+        uint64_t l = a.low << s;
+        uint64_t h = __shiftleft128(a.low, a.high, (unsigned char)s);
+        return _mm_set_epi64x(h, l);
+    } else {
+        return _mm_set_epi64x(a.low << (s - FStar_UInt128_u32_64), 0);
+    }
+#else
+    if (s < FStar_UInt128_u32_64)
+        return FStar_UInt128_shift_left_small(a, s);
+    else
+        return FStar_UInt128_shift_left_large(a, s);
+#endif
+}
+
+inline static 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);
+}
+
+inline static 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);
+}
+
+inline static 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;
+    }
+}
+
+inline static 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;
+}
+
+inline static FStar_UInt128_uint128
+FStar_UInt128_shift_right(FStar_UInt128_uint128 a, uint32_t s)
+{
+#if HAS_OPTIMIZED
+    if (s == 0) {
+        return a;
+    } else if (s < FStar_UInt128_u32_64) {
+        uint64_t l = __shiftright128(a.low, a.high, (unsigned char)s);
+        uint64_t h = a.high >> s;
+        return _mm_set_epi64x(h, l);
+    } else {
+        return _mm_set_epi64x(0, a.high >> (s - FStar_UInt128_u32_64));
+    }
+#else
+    if (s < FStar_UInt128_u32_64)
+        return FStar_UInt128_shift_right_small(a, s);
+    else
+        return FStar_UInt128_shift_right_large(a, s);
+#endif
+}
+
+inline static bool
+FStar_UInt128_eq(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+    return a.low == b.low && a.high == b.high;
+}
+
+inline static 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;
+}
+
+inline static 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;
+}
+
+inline static 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;
+}
+
+inline static 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;
+}
+
+inline static FStar_UInt128_uint128
+FStar_UInt128_eq_mask(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+#if HAS_OPTIMIZED
+    // PCMPW to produce 4 32-bit values, all either 0x0 or 0xffffffff
+    __m128i r32 = _mm_cmpeq_epi32(a, b);
+    // Shuffle 3,2,1,0 into 2,3,0,1 (swapping dwords inside each half)
+    __m128i s32 = _mm_shuffle_epi32(r32, _MM_SHUFFLE(2, 3, 0, 1));
+    // Bitwise and to compute (3&2),(2&3),(1&0),(0&1)
+    __m128i ret64 = _mm_and_si128(r32, s32);
+    // Swap the two 64-bit values to form s64
+    __m128i s64 =
+        _mm_shuffle_epi32(ret64, _MM_SHUFFLE(1, 0, 3, 2)); // 3,2,1,0 -> 1,0,3,2
+    // And them together
+    return _mm_and_si128(ret64, s64);
+#else
+    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;
+#endif
+}
+
+inline static FStar_UInt128_uint128
+FStar_UInt128_gte_mask(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b)
+{
+#if HAS_OPTIMIZED && 0
+    // ge - compare 3,2,1,0 for >= and generating 0 or 0xffffffff for each
+    // eq - compare 3,2,1,0 for == and generating 0 or 0xffffffff for each
+    // slot 0 = ge0 | (eq0 & ge1) | (eq0 & eq1 & ge2) | (eq0 & eq1 & eq2 & ge3)
+    // then splat slot 0 to 3,2,1,0
+    __m128i gt = _mm_cmpgt_epi32(a, b);
+    __m128i eq = _mm_cmpeq_epi32(a, b);
+    __m128i ge = _mm_or_si128(gt, eq);
+    __m128i ge0 = ge;
+    __m128i eq0 = eq;
+    __m128i ge1 = _mm_srli_si128(ge, 4); // shift ge from 3,2,1,0 to 0x0,3,2,1
+    __m128i t1 = _mm_and_si128(eq0, ge1);
+    __m128i ret = _mm_or_si128(ge, t1);  // ge0 | (eq0 & ge1) is now in 0
+    __m128i eq1 = _mm_srli_si128(eq, 4); // shift eq from 3,2,1,0 to 0x0,3,2,1
+    __m128i ge2 =
+        _mm_srli_si128(ge1, 4); // shift original ge from 3,2,1,0 to 0x0,0x0,3,2
+    __m128i t2 =
+        _mm_and_si128(eq0, _mm_and_si128(eq1, ge2)); // t2 = (eq0 & eq1 & ge2)
+    ret = _mm_or_si128(ret, t2);
+    __m128i eq2 = _mm_srli_si128(eq1, 4); // shift eq from 3,2,1,0 to 0x0,00,00,3
+    __m128i ge3 =
+        _mm_srli_si128(ge2, 4); // shift original ge from 3,2,1,0 to 0x0,0x0,0x0,3
+    __m128i t3 = _mm_and_si128(
+        eq0, _mm_and_si128(
+                 eq1, _mm_and_si128(eq2, ge3))); // t3 = (eq0 & eq1 & eq2 & ge3)
+    ret = _mm_or_si128(ret, t3);
+    return _mm_shuffle_epi32(
+        ret,
+        _MM_SHUFFLE(0, 0, 0, 0)); // the result is in 0.  Shuffle into all dwords.
+#else
+    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;
+#endif
+}
+
+inline static FStar_UInt128_uint128
+FStar_UInt128_uint64_to_uint128(uint64_t a)
+{
+#if HAS_OPTIMIZED
+    return _mm_set_epi64x(0, a);
+#else
+    FStar_UInt128_uint128 lit;
+    lit.low = a;
+    lit.high = (uint64_t)0U;
+    return lit;
+#endif
+}
+
+inline static uint64_t
+FStar_UInt128_uint128_to_uint64(FStar_UInt128_uint128 a)
+{
+    return a.low;
+}
+
+inline static 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;
+
+inline static uint64_t
+FStar_UInt128_u32_combine(uint64_t hi, uint64_t lo)
+{
+    return lo + (hi << FStar_UInt128_u32_32);
+}
+
+inline static FStar_UInt128_uint128
+FStar_UInt128_mul32(uint64_t x, uint32_t y)
+{
+#if HAS_OPTIMIZED
+    uint64_t l, h;
+    l = _umul128(x, (uint64_t)y, &h);
+    return _mm_set_epi64x(h, l);
+#else
+    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;
+#endif
+}
+
+/* Note: static headers bring scope collision issues when they define types!
+ * Because now client (karamel-generated) code will include this header and
+ * there might be type collisions if the client code uses quadruples of uint64s.
+ * So, we cannot use the karamel-generated name. */
+typedef struct K_quad_s {
+    uint64_t fst;
+    uint64_t snd;
+    uint64_t thd;
+    uint64_t f3;
+} K_quad;
+
+inline static K_quad
+FStar_UInt128_mul_wide_impl_t_(uint64_t x, uint64_t y)
+{
+    K_quad tmp;
+    tmp.fst = FStar_UInt128_u64_mod_32(x);
+    tmp.snd = FStar_UInt128_u64_mod_32(
+        FStar_UInt128_u64_mod_32(x) * FStar_UInt128_u64_mod_32(y));
+    tmp.thd = x >> FStar_UInt128_u32_32;
+    tmp.f3 = (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);
+    return tmp;
+}
+
+static uint64_t
+FStar_UInt128_u32_combine_(uint64_t hi, uint64_t lo)
+{
+    return lo + (hi << FStar_UInt128_u32_32);
+}
+
+inline static FStar_UInt128_uint128
+FStar_UInt128_mul_wide_impl(uint64_t x, uint64_t y)
+{
+    K_quad scrut =
+        FStar_UInt128_mul_wide_impl_t_(x, y);
+    uint64_t u1 = scrut.fst;
+    uint64_t w3 = scrut.snd;
+    uint64_t x_ = scrut.thd;
+    uint64_t t_ = scrut.f3;
+    FStar_UInt128_uint128 lit;
+    lit.low = FStar_UInt128_u32_combine_(
+        u1 * (y >> FStar_UInt128_u32_32) + FStar_UInt128_u64_mod_32(t_), w3);
+    lit.high =
+        x_ * (y >> FStar_UInt128_u32_32) + (t_ >> FStar_UInt128_u32_32) +
+        (u1 * (y >> FStar_UInt128_u32_32) + FStar_UInt128_u64_mod_32(t_) >>
+         FStar_UInt128_u32_32);
+    return lit;
+}
+
+inline static FStar_UInt128_uint128
+FStar_UInt128_mul_wide(uint64_t x, uint64_t y)
+{
+#if HAS_OPTIMIZED
+    uint64_t l, h;
+    l = _umul128(x, y, &h);
+    return _mm_set_epi64x(h, l);
+#else
+    return FStar_UInt128_mul_wide_impl(x, y);
+#endif
+}
+
+#undef low
+#undef high
+
+#endif
diff --git a/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/fstar_uint128_struct_endianness.h b/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/fstar_uint128_struct_endianness.h
new file mode 100644
index 0000000000..61fe85c49e
--- /dev/null
+++ b/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/fstar_uint128_struct_endianness.h
@@ -0,0 +1,84 @@
+/* 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/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/libkrmllib.def b/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/libkrmllib.def
new file mode 100644
index 0000000000..c4ab8e38ed
--- /dev/null
+++ b/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/libkrmllib.def
@@ -0,0 +1,11 @@
+LIBRARY libkrmllib
+
+EXPORTS
+  FStar_UInt64_eq_mask
+  FStar_UInt64_gte_mask
+  FStar_UInt32_eq_mask
+  FStar_UInt32_gte_mask
+  FStar_UInt16_eq_mask
+  FStar_UInt16_gte_mask
+  FStar_UInt8_eq_mask
+  FStar_UInt8_gte_mask