Adding upstream version 115.7.0esr.upstream/115.7.0esr

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

21 files changed, 2563 insertions, 0 deletions

diff --git a/security/nss/lib/freebl/verified/karamel/include/krml/c_endianness.h b/security/nss/lib/freebl/verified/karamel/include/krml/c_endianness.h
new file mode 100644
index 0000000000..21d7e1b4f9
--- /dev/null
+++ b/security/nss/lib/freebl/verified/karamel/include/krml/c_endianness.h
@@ -0,0 +1,13 @@
+/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
+   Licensed under the Apache 2.0 License. */
+
+#ifndef __KRML_ENDIAN_H
+#define __KRML_ENDIAN_H
+
+#ifdef __GNUC__
+#warning "c_endianness.h is deprecated, include lowstar_endianness.h instead"
+#endif
+
+#include "lowstar_endianness.h"
+
+#endif
diff --git a/security/nss/lib/freebl/verified/karamel/include/krml/fstar_int.h b/security/nss/lib/freebl/verified/karamel/include/krml/fstar_int.h
new file mode 100644
index 0000000000..c7a5afb50a
--- /dev/null
+++ b/security/nss/lib/freebl/verified/karamel/include/krml/fstar_int.h
@@ -0,0 +1,89 @@
+#ifndef __FSTAR_INT_H
+#define __FSTAR_INT_H
+
+#include "internal/types.h"
+
+/*
+ * Arithmetic Shift Right operator
+ *
+ * In all C standards, a >> b is implementation-defined when a has a signed
+ * type and a negative value. See e.g. 6.5.7 in
+ * http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2310.pdf
+ *
+ * GCC, MSVC, and Clang implement a >> b as an arithmetic shift.
+ *
+ * GCC: https://gcc.gnu.org/onlinedocs/gcc-9.1.0/gcc/Integers-implementation.html#Integers-implementation
+ * MSVC: https://docs.microsoft.com/en-us/cpp/cpp/left-shift-and-right-shift-operators-input-and-output?view=vs-2019#right-shifts
+ * Clang: tested that Clang 7, 8 and 9 compile this to an arithmetic shift
+ *
+ * We implement arithmetic shift right simply as >> in these compilers
+ * and bail out in others.
+ */
+
+#if !(defined(_MSC_VER) || defined(__GNUC__) || (defined(__clang__) && (__clang_major__ >= 7)))
+
+static inline int8_t
+FStar_Int8_shift_arithmetic_right(int8_t a, uint32_t b)
+{
+    do {
+        KRML_HOST_EPRINTF("Could not identify compiler so could not provide an implementation of signed arithmetic shift right.\n");
+        KRML_HOST_EXIT(255);
+    } while (0);
+}
+
+static inline int16_t
+FStar_Int16_shift_arithmetic_right(int16_t a, uint32_t b)
+{
+    do {
+        KRML_HOST_EPRINTF("Could not identify compiler so could not provide an implementation of signed arithmetic shift right.\n");
+        KRML_HOST_EXIT(255);
+    } while (0);
+}
+
+static inline int32_t
+FStar_Int32_shift_arithmetic_right(int32_t a, uint32_t b)
+{
+    do {
+        KRML_HOST_EPRINTF("Could not identify compiler so could not provide an implementation of signed arithmetic shift right.\n");
+        KRML_HOST_EXIT(255);
+    } while (0);
+}
+
+static inline int64_t
+FStar_Int64_shift_arithmetic_right(int64_t a, uint32_t b)
+{
+    do {
+        KRML_HOST_EPRINTF("Could not identify compiler so could not provide an implementation of signed arithmetic shift right.\n");
+        KRML_HOST_EXIT(255);
+    } while (0);
+}
+
+#else
+
+static inline int8_t
+FStar_Int8_shift_arithmetic_right(int8_t a, uint32_t b)
+{
+    return (a >> b);
+}
+
+static inline int16_t
+FStar_Int16_shift_arithmetic_right(int16_t a, uint32_t b)
+{
+    return (a >> b);
+}
+
+static inline int32_t
+FStar_Int32_shift_arithmetic_right(int32_t a, uint32_t b)
+{
+    return (a >> b);
+}
+
+static inline int64_t
+FStar_Int64_shift_arithmetic_right(int64_t a, uint32_t b)
+{
+    return (a >> b);
+}
+
+#endif /* !(defined(_MSC_VER) ... ) */
+
+#endif /* __FSTAR_INT_H */
diff --git a/security/nss/lib/freebl/verified/karamel/include/krml/internal/builtin.h b/security/nss/lib/freebl/verified/karamel/include/krml/internal/builtin.h
new file mode 100644
index 0000000000..f55e5f824e
--- /dev/null
+++ b/security/nss/lib/freebl/verified/karamel/include/krml/internal/builtin.h
@@ -0,0 +1,16 @@
+/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
+   Licensed under the Apache 2.0 License. */
+
+#ifndef __KRML_BUILTIN_H
+#define __KRML_BUILTIN_H
+
+/* For alloca, when using KaRaMeL's -falloca */
+#if (defined(_WIN32) || defined(_WIN64))
+#include <malloc.h>
+#endif
+
+/* If some globals need to be initialized before the main, then karamel will
+ * generate and try to link last a function with this type: */
+void krmlinit_globals(void);
+
+#endif
diff --git a/security/nss/lib/freebl/verified/karamel/include/krml/internal/callconv.h b/security/nss/lib/freebl/verified/karamel/include/krml/internal/callconv.h
new file mode 100644
index 0000000000..0d250c4450
--- /dev/null
+++ b/security/nss/lib/freebl/verified/karamel/include/krml/internal/callconv.h
@@ -0,0 +1,46 @@
+/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
+   Licensed under the Apache 2.0 License. */
+
+#ifndef __KRML_CALLCONV_H
+#define __KRML_CALLCONV_H
+
+/******************************************************************************/
+/* Some macros to ease compatibility                                          */
+/******************************************************************************/
+
+/* We want to generate __cdecl safely without worrying about it being undefined.
+ * When using MSVC, these are always defined. When using MinGW, these are
+ * defined too. They have no meaning for other platforms, so we define them to
+ * be empty macros in other situations. */
+#ifndef _MSC_VER
+#ifndef __cdecl
+#define __cdecl
+#endif
+#ifndef __stdcall
+#define __stdcall
+#endif
+#ifndef __fastcall
+#define __fastcall
+#endif
+#endif
+
+/* 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
+
+/* GCC-specific attribute syntax; everyone else gets the standard C inline
+ * attribute. */
+#ifdef __GNU_C__
+#ifndef __clang__
+#define force_inline inline __attribute__((always_inline))
+#else
+#define force_inline inline
+#endif
+#else
+#define force_inline inline
+#endif
+
+#endif
diff --git a/security/nss/lib/freebl/verified/karamel/include/krml/internal/compat.h b/security/nss/lib/freebl/verified/karamel/include/krml/internal/compat.h
new file mode 100644
index 0000000000..964d1c52aa
--- /dev/null
+++ b/security/nss/lib/freebl/verified/karamel/include/krml/internal/compat.h
@@ -0,0 +1,32 @@
+/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
+   Licensed under the Apache 2.0 License. */
+
+#ifndef KRML_COMPAT_H
+#define KRML_COMPAT_H
+
+#include <inttypes.h>
+
+/* A series of macros that define C implementations of types that are not Low*,
+ * to facilitate porting programs to Low*. */
+
+typedef struct {
+    uint32_t length;
+    const char *data;
+} FStar_Bytes_bytes;
+
+typedef int32_t Prims_pos, Prims_nat, Prims_nonzero, Prims_int,
+    krml_checked_int_t;
+
+#define RETURN_OR(x)                                                         \
+    do {                                                                     \
+        int64_t __ret = x;                                                   \
+        if (__ret < INT32_MIN || INT32_MAX < __ret) {                        \
+            KRML_HOST_PRINTF(                                                \
+                "Prims.{int,nat,pos} integer overflow at %s:%d\n", __FILE__, \
+                __LINE__);                                                   \
+            KRML_HOST_EXIT(252);                                             \
+        }                                                                    \
+        return (int32_t)__ret;                                               \
+    } while (0)
+
+#endif
diff --git a/security/nss/lib/freebl/verified/karamel/include/krml/internal/debug.h b/security/nss/lib/freebl/verified/karamel/include/krml/internal/debug.h
new file mode 100644
index 0000000000..f70006bd3f
--- /dev/null
+++ b/security/nss/lib/freebl/verified/karamel/include/krml/internal/debug.h
@@ -0,0 +1,57 @@
+/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
+   Licensed under the Apache 2.0 License. */
+
+#ifndef __KRML_DEBUG_H
+#define __KRML_DEBUG_H
+
+#include <inttypes.h>
+
+#include "krml/internal/target.h"
+
+/******************************************************************************/
+/* Debugging helpers - intended only for KaRaMeL developers                   */
+/******************************************************************************/
+
+/* In support of "-wasm -d force-c": we might need this function to be
+ * forward-declared, because the dependency on WasmSupport appears very late,
+ * after SimplifyWasm, and sadly, after the topological order has been done. */
+void WasmSupport_check_buffer_size(uint32_t s);
+
+/* A series of GCC atrocities to trace function calls (karamel's [-d c-calls]
+ * option). Useful when trying to debug, say, Wasm, to compare traces. */
+/* clang-format off */
+#ifdef __GNUC__
+#define KRML_FORMAT(X) _Generic((X),                                           \
+  uint8_t : "0x%08" PRIx8,                                                     \
+  uint16_t: "0x%08" PRIx16,                                                    \
+  uint32_t: "0x%08" PRIx32,                                                    \
+  uint64_t: "0x%08" PRIx64,                                                    \
+  int8_t  : "0x%08" PRIx8,                                                     \
+  int16_t : "0x%08" PRIx16,                                                    \
+  int32_t : "0x%08" PRIx32,                                                    \
+  int64_t : "0x%08" PRIx64,                                                    \
+  default : "%s")
+
+#define KRML_FORMAT_ARG(X) _Generic((X),                                       \
+  uint8_t : X,                                                                 \
+  uint16_t: X,                                                                 \
+  uint32_t: X,                                                                 \
+  uint64_t: X,                                                                 \
+  int8_t  : X,                                                                 \
+  int16_t : X,                                                                 \
+  int32_t : X,                                                                 \
+  int64_t : X,                                                                 \
+  default : "unknown")
+/* clang-format on */
+
+#define KRML_DEBUG_RETURN(X)                                        \
+    ({                                                              \
+        __auto_type _ret = (X);                                     \
+        KRML_HOST_PRINTF("returning: ");                            \
+        KRML_HOST_PRINTF(KRML_FORMAT(_ret), KRML_FORMAT_ARG(_ret)); \
+        KRML_HOST_PRINTF(" \n");                                    \
+        _ret;                                                       \
+    })
+#endif
+
+#endif
diff --git a/security/nss/lib/freebl/verified/karamel/include/krml/internal/target.h b/security/nss/lib/freebl/verified/karamel/include/krml/internal/target.h
new file mode 100644
index 0000000000..929abe8081
--- /dev/null
+++ b/security/nss/lib/freebl/verified/karamel/include/krml/internal/target.h
@@ -0,0 +1,333 @@
+/* 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 <stdio.h>
+#include <stdbool.h>
+#include <inttypes.h>
+#include <limits.h>
+
+#include "krml/internal/callconv.h"
+
+/******************************************************************************/
+/* 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_PRE_ALIGN
+#ifdef _MSC_VER
+#define KRML_PRE_ALIGN(X) __declspec(align(X))
+#else
+#define KRML_PRE_ALIGN(X)
+#endif
+#endif
+
+#ifndef KRML_POST_ALIGN
+#ifdef _MSC_VER
+#define KRML_POST_ALIGN(X)
+#else
+#define KRML_POST_ALIGN(X) __attribute__((aligned(X)))
+#endif
+#endif
+
+#ifndef KRML_ALIGNED_MALLOC
+#ifdef _MSC_VER
+#define KRML_ALIGNED_MALLOC(X, Y) _aligned_malloc(Y, X)
+#else
+#define KRML_ALIGNED_MALLOC(X, Y) aligned_alloc(X, Y)
+#endif
+#endif
+
+#ifndef KRML_ALIGNED_FREE
+#ifdef _MSC_VER
+#define KRML_ALIGNED_FREE(X) _aligned_free(X)
+#else
+#define KRML_ALIGNED_FREE(X) free(X)
+#endif
+#endif
+
+#ifndef KRML_HOST_TIME
+
+#include <time.h>
+
+/* Prims_nat not yet in scope */
+inline static int32_t
+krml_time()
+{
+    return (int32_t)time(NULL);
+}
+
+#define KRML_HOST_TIME krml_time
+#endif
+
+/* In statement position, exiting is easy. */
+#define KRML_EXIT                                                                  \
+    do {                                                                           \
+        KRML_HOST_PRINTF("Unimplemented function at %s:%d\n", __FILE__, __LINE__); \
+        KRML_HOST_EXIT(254);                                                       \
+    } while (0)
+
+/* In expression position, use the comma-operator and a malloc to return an
+ * expression of the right size. KaRaMeL passes t as the parameter to the macro.
+ */
+#define KRML_EABORT(t, msg)                                                     \
+    (KRML_HOST_PRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, msg), \
+     KRML_HOST_EXIT(255), *((t *)KRML_HOST_MALLOC(sizeof(t))))
+
+/* 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)
+
+#if defined(_MSC_VER) && _MSC_VER < 1900
+#define KRML_HOST_SNPRINTF(buf, sz, fmt, arg) _snprintf_s(buf, sz, _TRUNCATE, fmt, arg)
+#else
+#define KRML_HOST_SNPRINTF(buf, sz, fmt, arg) snprintf(buf, sz, fmt, arg)
+#endif
+
+#if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ > 4))
+#define KRML_DEPRECATED(x) __attribute__((deprecated(x)))
+#elif defined(__GNUC__)
+/* deprecated attribute is not defined in GCC < 4.5. */
+#define KRML_DEPRECATED(x)
+#elif defined(_MSC_VER)
+#define KRML_DEPRECATED(x) __declspec(deprecated(x))
+#endif
+
+/* 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/security/nss/lib/freebl/verified/karamel/include/krml/internal/types.h b/security/nss/lib/freebl/verified/karamel/include/krml/internal/types.h
new file mode 100644
index 0000000000..2cf1887adf
--- /dev/null
+++ b/security/nss/lib/freebl/verified/karamel/include/krml/internal/types.h
@@ -0,0 +1,105 @@
+/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
+   Licensed under the Apache 2.0 License. */
+
+#ifndef KRML_TYPES_H
+#define KRML_TYPES_H
+
+#include <inttypes.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <stdint.h>
+
+/* Types which are either abstract, meaning that have to be implemented in C, or
+ * which are models, meaning that they are swapped out at compile-time for
+ * hand-written C types (in which case they're marked as noextract). */
+
+typedef uint64_t FStar_UInt64_t, FStar_UInt64_t_;
+typedef int64_t FStar_Int64_t, FStar_Int64_t_;
+typedef uint32_t FStar_UInt32_t, FStar_UInt32_t_;
+typedef int32_t FStar_Int32_t, FStar_Int32_t_;
+typedef uint16_t FStar_UInt16_t, FStar_UInt16_t_;
+typedef int16_t FStar_Int16_t, FStar_Int16_t_;
+typedef uint8_t FStar_UInt8_t, FStar_UInt8_t_;
+typedef int8_t FStar_Int8_t, FStar_Int8_t_;
+
+/* Only useful when building krmllib, because it's in the dependency graph of
+ * FStar.Int.Cast. */
+typedef uint64_t FStar_UInt63_t, FStar_UInt63_t_;
+typedef int64_t FStar_Int63_t, FStar_Int63_t_;
+
+typedef double FStar_Float_float;
+typedef uint32_t FStar_Char_char;
+typedef FILE *FStar_IO_fd_read, *FStar_IO_fd_write;
+
+typedef void *FStar_Dyn_dyn;
+
+typedef const char *C_String_t, *C_String_t_, *C_Compat_String_t, *C_Compat_String_t_;
+
+typedef int exit_code;
+typedef FILE *channel;
+
+typedef unsigned long long TestLib_cycles;
+
+typedef uint64_t FStar_Date_dateTime, FStar_Date_timeSpan;
+
+/* Now Prims.string is no longer illegal with the new model in LowStar.Printf;
+ * it's operations that produce Prims_string which are illegal. Bring the
+ * definition into scope by default. */
+typedef const char *Prims_string;
+
+#if (defined(_MSC_VER) && defined(_M_X64) && !defined(__clang__))
+#define IS_MSVC64 1
+#endif
+
+/* This code makes a number of assumptions and should be refined. In particular,
+ * it assumes that: any non-MSVC amd64 compiler supports int128. Maybe it would
+ * be easier to just test for defined(__SIZEOF_INT128__) only? */
+#if (defined(__x86_64__) ||                                          \
+     defined(__x86_64) ||                                            \
+     defined(__aarch64__) ||                                         \
+     (defined(__powerpc64__) && defined(__LITTLE_ENDIAN__)) ||       \
+     defined(__s390x__) ||                                           \
+     (defined(_MSC_VER) && defined(_M_X64) && defined(__clang__)) || \
+     (defined(__mips__) && defined(__LP64__)) ||                     \
+     (defined(__riscv) && __riscv_xlen == 64) ||                     \
+     defined(__SIZEOF_INT128__))
+#define HAS_INT128 1
+#endif
+
+/* The uint128 type is a special case since we offer several implementations of
+ * it, depending on the compiler and whether the user wants the verified
+ * implementation or not. */
+#if !defined(KRML_VERIFIED_UINT128) && defined(IS_MSVC64)
+#include <emmintrin.h>
+typedef __m128i FStar_UInt128_uint128;
+#elif !defined(KRML_VERIFIED_UINT128) && defined(HAS_INT128)
+typedef unsigned __int128 FStar_UInt128_uint128;
+#else
+typedef struct FStar_UInt128_uint128_s {
+    uint64_t low;
+    uint64_t high;
+} FStar_UInt128_uint128;
+#endif
+
+/* The former is defined once, here (otherwise, conflicts for test-c89. The
+ * latter is for internal use. */
+typedef FStar_UInt128_uint128 FStar_UInt128_t, uint128_t;
+
+#include "krml/lowstar_endianness.h"
+
+#endif
+
+/* Avoid a circular loop: if this header is included via FStar_UInt8_16_32_64,
+ * then don't bring the uint128 definitions into scope. */
+#ifndef __FStar_UInt_8_16_32_64_H
+
+#if !defined(KRML_VERIFIED_UINT128) && defined(IS_MSVC64)
+#include "fstar_uint128_msvc.h"
+#elif !defined(KRML_VERIFIED_UINT128) && defined(HAS_INT128)
+#include "fstar_uint128_gcc64.h"
+#else
+#include "FStar_UInt128_Verified.h"
+#include "fstar_uint128_struct_endianness.h"
+#endif
+
+#endif
diff --git a/security/nss/lib/freebl/verified/karamel/include/krml/internal/wasmsupport.h b/security/nss/lib/freebl/verified/karamel/include/krml/internal/wasmsupport.h
new file mode 100644
index 0000000000..b44fa3f75d
--- /dev/null
+++ b/security/nss/lib/freebl/verified/karamel/include/krml/internal/wasmsupport.h
@@ -0,0 +1,5 @@
+/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
+   Licensed under the Apache 2.0 License. */
+
+/* This file is automatically included when compiling with -wasm -d force-c */
+#define WasmSupport_check_buffer_size(X)
diff --git a/security/nss/lib/freebl/verified/karamel/include/krml/lowstar_endianness.h b/security/nss/lib/freebl/verified/karamel/include/krml/lowstar_endianness.h
new file mode 100644
index 0000000000..48e9fd5795
--- /dev/null
+++ b/security/nss/lib/freebl/verified/karamel/include/krml/lowstar_endianness.h
@@ -0,0 +1,242 @@
+/* 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__)
+#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(__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 */
+#elif defined(__BYTE_ORDER__) && __BYTE_ORDER__ == __ORDER_BIG_ENDIAN__
+
+/* 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/security/nss/lib/freebl/verified/karamel/include/krmllib.h b/security/nss/lib/freebl/verified/karamel/include/krmllib.h
new file mode 100644
index 0000000000..1f461f351c
--- /dev/null
+++ b/security/nss/lib/freebl/verified/karamel/include/krmllib.h
@@ -0,0 +1,28 @@
+#ifndef __KRMLLIB_H
+#define __KRMLLIB_H
+
+/******************************************************************************/
+/* The all-in-one krmllib.h header                                            */
+/******************************************************************************/
+
+/* This is a meta-header that is included by default in KaRaMeL generated
+ * programs. If you wish to have a more lightweight set of headers, or are
+ * targeting an environment where controlling these macros yourself is
+ * important, consider using:
+ *
+ *   krml -minimal
+ *
+ * to disable the inclusion of this file (note: this also disables the default
+ * argument "-bundle FStar.*"). You can then include the headers of your choice
+ * one by one, using -add-early-include. */
+
+#include "krml/internal/target.h"
+#include "krml/internal/callconv.h"
+#include "krml/internal/builtin.h"
+#include "krml/internal/debug.h"
+#include "krml/internal/types.h"
+
+#include "krml/lowstar_endianness.h"
+#include "krml/fstar_int.h"
+
+#endif /* __KRMLLIB_H */
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