Adding upstream version 124.0.1.upstream/124.0.1

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

13 files changed, 2584 insertions, 0 deletions

diff --git a/security/nss/lib/freebl/verified/internal/Hacl_Bignum.h b/security/nss/lib/freebl/verified/internal/Hacl_Bignum.h
new file mode 100644
index 0000000000..bc4ed6f0fa
--- /dev/null
+++ b/security/nss/lib/freebl/verified/internal/Hacl_Bignum.h
@@ -0,0 +1,315 @@
+/* MIT License
+ *
+ * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation
+ * Copyright (c) 2022-2023 HACL* Contributors
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the Software is
+ * furnished to do so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+ * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+ * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+ * SOFTWARE.
+ */
+
+#ifndef __internal_Hacl_Bignum_H
+#define __internal_Hacl_Bignum_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
+#include <string.h>
+#include "krml/internal/types.h"
+#include "krml/lowstar_endianness.h"
+#include "krml/internal/target.h"
+
+#include "internal/Hacl_Krmllib.h"
+#include "internal/Hacl_Bignum_Base.h"
+#include "../Hacl_Bignum.h"
+#include "lib_intrinsics.h"
+
+void
+Hacl_Bignum_Karatsuba_bn_karatsuba_mul_uint32(
+    uint32_t aLen,
+    uint32_t *a,
+    uint32_t *b,
+    uint32_t *tmp,
+    uint32_t *res);
+
+void
+Hacl_Bignum_Karatsuba_bn_karatsuba_mul_uint64(
+    uint32_t aLen,
+    uint64_t *a,
+    uint64_t *b,
+    uint64_t *tmp,
+    uint64_t *res);
+
+void
+Hacl_Bignum_Karatsuba_bn_karatsuba_sqr_uint32(
+    uint32_t aLen,
+    uint32_t *a,
+    uint32_t *tmp,
+    uint32_t *res);
+
+void
+Hacl_Bignum_Karatsuba_bn_karatsuba_sqr_uint64(
+    uint32_t aLen,
+    uint64_t *a,
+    uint64_t *tmp,
+    uint64_t *res);
+
+void
+Hacl_Bignum_bn_add_mod_n_u32(
+    uint32_t len1,
+    uint32_t *n,
+    uint32_t *a,
+    uint32_t *b,
+    uint32_t *res);
+
+void
+Hacl_Bignum_bn_add_mod_n_u64(
+    uint32_t len1,
+    uint64_t *n,
+    uint64_t *a,
+    uint64_t *b,
+    uint64_t *res);
+
+void
+Hacl_Bignum_bn_sub_mod_n_u32(
+    uint32_t len1,
+    uint32_t *n,
+    uint32_t *a,
+    uint32_t *b,
+    uint32_t *res);
+
+void
+Hacl_Bignum_bn_sub_mod_n_u64(
+    uint32_t len1,
+    uint64_t *n,
+    uint64_t *a,
+    uint64_t *b,
+    uint64_t *res);
+
+uint32_t Hacl_Bignum_ModInvLimb_mod_inv_uint32(uint32_t n0);
+
+uint64_t Hacl_Bignum_ModInvLimb_mod_inv_uint64(uint64_t n0);
+
+uint32_t Hacl_Bignum_Montgomery_bn_check_modulus_u32(uint32_t len, uint32_t *n);
+
+void
+Hacl_Bignum_Montgomery_bn_precomp_r2_mod_n_u32(
+    uint32_t len,
+    uint32_t nBits,
+    uint32_t *n,
+    uint32_t *res);
+
+void
+Hacl_Bignum_Montgomery_bn_mont_reduction_u32(
+    uint32_t len,
+    uint32_t *n,
+    uint32_t nInv,
+    uint32_t *c,
+    uint32_t *res);
+
+void
+Hacl_Bignum_Montgomery_bn_to_mont_u32(
+    uint32_t len,
+    uint32_t *n,
+    uint32_t nInv,
+    uint32_t *r2,
+    uint32_t *a,
+    uint32_t *aM);
+
+void
+Hacl_Bignum_Montgomery_bn_from_mont_u32(
+    uint32_t len,
+    uint32_t *n,
+    uint32_t nInv_u64,
+    uint32_t *aM,
+    uint32_t *a);
+
+void
+Hacl_Bignum_Montgomery_bn_mont_mul_u32(
+    uint32_t len,
+    uint32_t *n,
+    uint32_t nInv_u64,
+    uint32_t *aM,
+    uint32_t *bM,
+    uint32_t *resM);
+
+void
+Hacl_Bignum_Montgomery_bn_mont_sqr_u32(
+    uint32_t len,
+    uint32_t *n,
+    uint32_t nInv_u64,
+    uint32_t *aM,
+    uint32_t *resM);
+
+uint64_t Hacl_Bignum_Montgomery_bn_check_modulus_u64(uint32_t len, uint64_t *n);
+
+void
+Hacl_Bignum_Montgomery_bn_precomp_r2_mod_n_u64(
+    uint32_t len,
+    uint32_t nBits,
+    uint64_t *n,
+    uint64_t *res);
+
+void
+Hacl_Bignum_Montgomery_bn_mont_reduction_u64(
+    uint32_t len,
+    uint64_t *n,
+    uint64_t nInv,
+    uint64_t *c,
+    uint64_t *res);
+
+void
+Hacl_Bignum_Montgomery_bn_to_mont_u64(
+    uint32_t len,
+    uint64_t *n,
+    uint64_t nInv,
+    uint64_t *r2,
+    uint64_t *a,
+    uint64_t *aM);
+
+void
+Hacl_Bignum_Montgomery_bn_from_mont_u64(
+    uint32_t len,
+    uint64_t *n,
+    uint64_t nInv_u64,
+    uint64_t *aM,
+    uint64_t *a);
+
+void
+Hacl_Bignum_Montgomery_bn_mont_mul_u64(
+    uint32_t len,
+    uint64_t *n,
+    uint64_t nInv_u64,
+    uint64_t *aM,
+    uint64_t *bM,
+    uint64_t *resM);
+
+void
+Hacl_Bignum_Montgomery_bn_mont_sqr_u64(
+    uint32_t len,
+    uint64_t *n,
+    uint64_t nInv_u64,
+    uint64_t *aM,
+    uint64_t *resM);
+
+uint32_t
+Hacl_Bignum_Exponentiation_bn_check_mod_exp_u32(
+    uint32_t len,
+    uint32_t *n,
+    uint32_t *a,
+    uint32_t bBits,
+    uint32_t *b);
+
+void
+Hacl_Bignum_Exponentiation_bn_mod_exp_vartime_precomp_u32(
+    uint32_t len,
+    uint32_t *n,
+    uint32_t mu,
+    uint32_t *r2,
+    uint32_t *a,
+    uint32_t bBits,
+    uint32_t *b,
+    uint32_t *res);
+
+void
+Hacl_Bignum_Exponentiation_bn_mod_exp_consttime_precomp_u32(
+    uint32_t len,
+    uint32_t *n,
+    uint32_t mu,
+    uint32_t *r2,
+    uint32_t *a,
+    uint32_t bBits,
+    uint32_t *b,
+    uint32_t *res);
+
+void
+Hacl_Bignum_Exponentiation_bn_mod_exp_vartime_u32(
+    uint32_t len,
+    uint32_t nBits,
+    uint32_t *n,
+    uint32_t *a,
+    uint32_t bBits,
+    uint32_t *b,
+    uint32_t *res);
+
+void
+Hacl_Bignum_Exponentiation_bn_mod_exp_consttime_u32(
+    uint32_t len,
+    uint32_t nBits,
+    uint32_t *n,
+    uint32_t *a,
+    uint32_t bBits,
+    uint32_t *b,
+    uint32_t *res);
+
+uint64_t
+Hacl_Bignum_Exponentiation_bn_check_mod_exp_u64(
+    uint32_t len,
+    uint64_t *n,
+    uint64_t *a,
+    uint32_t bBits,
+    uint64_t *b);
+
+void
+Hacl_Bignum_Exponentiation_bn_mod_exp_vartime_precomp_u64(
+    uint32_t len,
+    uint64_t *n,
+    uint64_t mu,
+    uint64_t *r2,
+    uint64_t *a,
+    uint32_t bBits,
+    uint64_t *b,
+    uint64_t *res);
+
+void
+Hacl_Bignum_Exponentiation_bn_mod_exp_consttime_precomp_u64(
+    uint32_t len,
+    uint64_t *n,
+    uint64_t mu,
+    uint64_t *r2,
+    uint64_t *a,
+    uint32_t bBits,
+    uint64_t *b,
+    uint64_t *res);
+
+void
+Hacl_Bignum_Exponentiation_bn_mod_exp_vartime_u64(
+    uint32_t len,
+    uint32_t nBits,
+    uint64_t *n,
+    uint64_t *a,
+    uint32_t bBits,
+    uint64_t *b,
+    uint64_t *res);
+
+void
+Hacl_Bignum_Exponentiation_bn_mod_exp_consttime_u64(
+    uint32_t len,
+    uint32_t nBits,
+    uint64_t *n,
+    uint64_t *a,
+    uint32_t bBits,
+    uint64_t *b,
+    uint64_t *res);
+
+#if defined(__cplusplus)
+}
+#endif
+
+#define __internal_Hacl_Bignum_H_DEFINED
+#endif
diff --git a/security/nss/lib/freebl/verified/internal/Hacl_Bignum25519_51.h b/security/nss/lib/freebl/verified/internal/Hacl_Bignum25519_51.h
new file mode 100644
index 0000000000..c3e86ca512
--- /dev/null
+++ b/security/nss/lib/freebl/verified/internal/Hacl_Bignum25519_51.h
@@ -0,0 +1,680 @@
+/* MIT License
+ *
+ * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation
+ * Copyright (c) 2022-2023 HACL* Contributors
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the Software is
+ * furnished to do so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+ * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+ * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+ * SOFTWARE.
+ */
+
+#ifndef __internal_Hacl_Bignum25519_51_H
+#define __internal_Hacl_Bignum25519_51_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
+#include <string.h>
+#include "krml/internal/types.h"
+#include "krml/lowstar_endianness.h"
+#include "krml/internal/target.h"
+
+#include "internal/Hacl_Krmllib.h"
+#include "Hacl_Krmllib.h"
+
+static inline void
+Hacl_Impl_Curve25519_Field51_fadd(uint64_t *out, uint64_t *f1, uint64_t *f2)
+{
+    uint64_t f10 = f1[0U];
+    uint64_t f20 = f2[0U];
+    uint64_t f11 = f1[1U];
+    uint64_t f21 = f2[1U];
+    uint64_t f12 = f1[2U];
+    uint64_t f22 = f2[2U];
+    uint64_t f13 = f1[3U];
+    uint64_t f23 = f2[3U];
+    uint64_t f14 = f1[4U];
+    uint64_t f24 = f2[4U];
+    out[0U] = f10 + f20;
+    out[1U] = f11 + f21;
+    out[2U] = f12 + f22;
+    out[3U] = f13 + f23;
+    out[4U] = f14 + f24;
+}
+
+static inline void
+Hacl_Impl_Curve25519_Field51_fsub(uint64_t *out, uint64_t *f1, uint64_t *f2)
+{
+    uint64_t f10 = f1[0U];
+    uint64_t f20 = f2[0U];
+    uint64_t f11 = f1[1U];
+    uint64_t f21 = f2[1U];
+    uint64_t f12 = f1[2U];
+    uint64_t f22 = f2[2U];
+    uint64_t f13 = f1[3U];
+    uint64_t f23 = f2[3U];
+    uint64_t f14 = f1[4U];
+    uint64_t f24 = f2[4U];
+    out[0U] = f10 + (uint64_t)0x3fffffffffff68U - f20;
+    out[1U] = f11 + (uint64_t)0x3ffffffffffff8U - f21;
+    out[2U] = f12 + (uint64_t)0x3ffffffffffff8U - f22;
+    out[3U] = f13 + (uint64_t)0x3ffffffffffff8U - f23;
+    out[4U] = f14 + (uint64_t)0x3ffffffffffff8U - f24;
+}
+
+static inline void
+Hacl_Impl_Curve25519_Field51_fmul(
+    uint64_t *out,
+    uint64_t *f1,
+    uint64_t *f2,
+    FStar_UInt128_uint128 *uu___)
+{
+    uint64_t f10 = f1[0U];
+    uint64_t f11 = f1[1U];
+    uint64_t f12 = f1[2U];
+    uint64_t f13 = f1[3U];
+    uint64_t f14 = f1[4U];
+    uint64_t f20 = f2[0U];
+    uint64_t f21 = f2[1U];
+    uint64_t f22 = f2[2U];
+    uint64_t f23 = f2[3U];
+    uint64_t f24 = f2[4U];
+    uint64_t tmp1 = f21 * (uint64_t)19U;
+    uint64_t tmp2 = f22 * (uint64_t)19U;
+    uint64_t tmp3 = f23 * (uint64_t)19U;
+    uint64_t tmp4 = f24 * (uint64_t)19U;
+    FStar_UInt128_uint128 o00 = FStar_UInt128_mul_wide(f10, f20);
+    FStar_UInt128_uint128 o10 = FStar_UInt128_mul_wide(f10, f21);
+    FStar_UInt128_uint128 o20 = FStar_UInt128_mul_wide(f10, f22);
+    FStar_UInt128_uint128 o30 = FStar_UInt128_mul_wide(f10, f23);
+    FStar_UInt128_uint128 o40 = FStar_UInt128_mul_wide(f10, f24);
+    FStar_UInt128_uint128 o01 = FStar_UInt128_add(o00, FStar_UInt128_mul_wide(f11, tmp4));
+    FStar_UInt128_uint128 o11 = FStar_UInt128_add(o10, FStar_UInt128_mul_wide(f11, f20));
+    FStar_UInt128_uint128 o21 = FStar_UInt128_add(o20, FStar_UInt128_mul_wide(f11, f21));
+    FStar_UInt128_uint128 o31 = FStar_UInt128_add(o30, FStar_UInt128_mul_wide(f11, f22));
+    FStar_UInt128_uint128 o41 = FStar_UInt128_add(o40, FStar_UInt128_mul_wide(f11, f23));
+    FStar_UInt128_uint128 o02 = FStar_UInt128_add(o01, FStar_UInt128_mul_wide(f12, tmp3));
+    FStar_UInt128_uint128 o12 = FStar_UInt128_add(o11, FStar_UInt128_mul_wide(f12, tmp4));
+    FStar_UInt128_uint128 o22 = FStar_UInt128_add(o21, FStar_UInt128_mul_wide(f12, f20));
+    FStar_UInt128_uint128 o32 = FStar_UInt128_add(o31, FStar_UInt128_mul_wide(f12, f21));
+    FStar_UInt128_uint128 o42 = FStar_UInt128_add(o41, FStar_UInt128_mul_wide(f12, f22));
+    FStar_UInt128_uint128 o03 = FStar_UInt128_add(o02, FStar_UInt128_mul_wide(f13, tmp2));
+    FStar_UInt128_uint128 o13 = FStar_UInt128_add(o12, FStar_UInt128_mul_wide(f13, tmp3));
+    FStar_UInt128_uint128 o23 = FStar_UInt128_add(o22, FStar_UInt128_mul_wide(f13, tmp4));
+    FStar_UInt128_uint128 o33 = FStar_UInt128_add(o32, FStar_UInt128_mul_wide(f13, f20));
+    FStar_UInt128_uint128 o43 = FStar_UInt128_add(o42, FStar_UInt128_mul_wide(f13, f21));
+    FStar_UInt128_uint128 o04 = FStar_UInt128_add(o03, FStar_UInt128_mul_wide(f14, tmp1));
+    FStar_UInt128_uint128 o14 = FStar_UInt128_add(o13, FStar_UInt128_mul_wide(f14, tmp2));
+    FStar_UInt128_uint128 o24 = FStar_UInt128_add(o23, FStar_UInt128_mul_wide(f14, tmp3));
+    FStar_UInt128_uint128 o34 = FStar_UInt128_add(o33, FStar_UInt128_mul_wide(f14, tmp4));
+    FStar_UInt128_uint128 o44 = FStar_UInt128_add(o43, FStar_UInt128_mul_wide(f14, f20));
+    FStar_UInt128_uint128 tmp_w0 = o04;
+    FStar_UInt128_uint128 tmp_w1 = o14;
+    FStar_UInt128_uint128 tmp_w2 = o24;
+    FStar_UInt128_uint128 tmp_w3 = o34;
+    FStar_UInt128_uint128 tmp_w4 = o44;
+    FStar_UInt128_uint128
+        l_ = FStar_UInt128_add(tmp_w0, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
+    uint64_t tmp01 = FStar_UInt128_uint128_to_uint64(l_) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c0 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_, (uint32_t)51U));
+    FStar_UInt128_uint128 l_0 = FStar_UInt128_add(tmp_w1, FStar_UInt128_uint64_to_uint128(c0));
+    uint64_t tmp11 = FStar_UInt128_uint128_to_uint64(l_0) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c1 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_0, (uint32_t)51U));
+    FStar_UInt128_uint128 l_1 = FStar_UInt128_add(tmp_w2, FStar_UInt128_uint64_to_uint128(c1));
+    uint64_t tmp21 = FStar_UInt128_uint128_to_uint64(l_1) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_1, (uint32_t)51U));
+    FStar_UInt128_uint128 l_2 = FStar_UInt128_add(tmp_w3, FStar_UInt128_uint64_to_uint128(c2));
+    uint64_t tmp31 = FStar_UInt128_uint128_to_uint64(l_2) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c3 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_2, (uint32_t)51U));
+    FStar_UInt128_uint128 l_3 = FStar_UInt128_add(tmp_w4, FStar_UInt128_uint64_to_uint128(c3));
+    uint64_t tmp41 = FStar_UInt128_uint128_to_uint64(l_3) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_3, (uint32_t)51U));
+    uint64_t l_4 = tmp01 + c4 * (uint64_t)19U;
+    uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
+    uint64_t c5 = l_4 >> (uint32_t)51U;
+    uint64_t o0 = tmp0_;
+    uint64_t o1 = tmp11 + c5;
+    uint64_t o2 = tmp21;
+    uint64_t o3 = tmp31;
+    uint64_t o4 = tmp41;
+    out[0U] = o0;
+    out[1U] = o1;
+    out[2U] = o2;
+    out[3U] = o3;
+    out[4U] = o4;
+}
+
+static inline void
+Hacl_Impl_Curve25519_Field51_fmul2(
+    uint64_t *out,
+    uint64_t *f1,
+    uint64_t *f2,
+    FStar_UInt128_uint128 *uu___)
+{
+    uint64_t f10 = f1[0U];
+    uint64_t f11 = f1[1U];
+    uint64_t f12 = f1[2U];
+    uint64_t f13 = f1[3U];
+    uint64_t f14 = f1[4U];
+    uint64_t f20 = f2[0U];
+    uint64_t f21 = f2[1U];
+    uint64_t f22 = f2[2U];
+    uint64_t f23 = f2[3U];
+    uint64_t f24 = f2[4U];
+    uint64_t f30 = f1[5U];
+    uint64_t f31 = f1[6U];
+    uint64_t f32 = f1[7U];
+    uint64_t f33 = f1[8U];
+    uint64_t f34 = f1[9U];
+    uint64_t f40 = f2[5U];
+    uint64_t f41 = f2[6U];
+    uint64_t f42 = f2[7U];
+    uint64_t f43 = f2[8U];
+    uint64_t f44 = f2[9U];
+    uint64_t tmp11 = f21 * (uint64_t)19U;
+    uint64_t tmp12 = f22 * (uint64_t)19U;
+    uint64_t tmp13 = f23 * (uint64_t)19U;
+    uint64_t tmp14 = f24 * (uint64_t)19U;
+    uint64_t tmp21 = f41 * (uint64_t)19U;
+    uint64_t tmp22 = f42 * (uint64_t)19U;
+    uint64_t tmp23 = f43 * (uint64_t)19U;
+    uint64_t tmp24 = f44 * (uint64_t)19U;
+    FStar_UInt128_uint128 o00 = FStar_UInt128_mul_wide(f10, f20);
+    FStar_UInt128_uint128 o15 = FStar_UInt128_mul_wide(f10, f21);
+    FStar_UInt128_uint128 o25 = FStar_UInt128_mul_wide(f10, f22);
+    FStar_UInt128_uint128 o30 = FStar_UInt128_mul_wide(f10, f23);
+    FStar_UInt128_uint128 o40 = FStar_UInt128_mul_wide(f10, f24);
+    FStar_UInt128_uint128 o010 = FStar_UInt128_add(o00, FStar_UInt128_mul_wide(f11, tmp14));
+    FStar_UInt128_uint128 o110 = FStar_UInt128_add(o15, FStar_UInt128_mul_wide(f11, f20));
+    FStar_UInt128_uint128 o210 = FStar_UInt128_add(o25, FStar_UInt128_mul_wide(f11, f21));
+    FStar_UInt128_uint128 o310 = FStar_UInt128_add(o30, FStar_UInt128_mul_wide(f11, f22));
+    FStar_UInt128_uint128 o410 = FStar_UInt128_add(o40, FStar_UInt128_mul_wide(f11, f23));
+    FStar_UInt128_uint128 o020 = FStar_UInt128_add(o010, FStar_UInt128_mul_wide(f12, tmp13));
+    FStar_UInt128_uint128 o120 = FStar_UInt128_add(o110, FStar_UInt128_mul_wide(f12, tmp14));
+    FStar_UInt128_uint128 o220 = FStar_UInt128_add(o210, FStar_UInt128_mul_wide(f12, f20));
+    FStar_UInt128_uint128 o320 = FStar_UInt128_add(o310, FStar_UInt128_mul_wide(f12, f21));
+    FStar_UInt128_uint128 o420 = FStar_UInt128_add(o410, FStar_UInt128_mul_wide(f12, f22));
+    FStar_UInt128_uint128 o030 = FStar_UInt128_add(o020, FStar_UInt128_mul_wide(f13, tmp12));
+    FStar_UInt128_uint128 o130 = FStar_UInt128_add(o120, FStar_UInt128_mul_wide(f13, tmp13));
+    FStar_UInt128_uint128 o230 = FStar_UInt128_add(o220, FStar_UInt128_mul_wide(f13, tmp14));
+    FStar_UInt128_uint128 o330 = FStar_UInt128_add(o320, FStar_UInt128_mul_wide(f13, f20));
+    FStar_UInt128_uint128 o430 = FStar_UInt128_add(o420, FStar_UInt128_mul_wide(f13, f21));
+    FStar_UInt128_uint128 o040 = FStar_UInt128_add(o030, FStar_UInt128_mul_wide(f14, tmp11));
+    FStar_UInt128_uint128 o140 = FStar_UInt128_add(o130, FStar_UInt128_mul_wide(f14, tmp12));
+    FStar_UInt128_uint128 o240 = FStar_UInt128_add(o230, FStar_UInt128_mul_wide(f14, tmp13));
+    FStar_UInt128_uint128 o340 = FStar_UInt128_add(o330, FStar_UInt128_mul_wide(f14, tmp14));
+    FStar_UInt128_uint128 o440 = FStar_UInt128_add(o430, FStar_UInt128_mul_wide(f14, f20));
+    FStar_UInt128_uint128 tmp_w10 = o040;
+    FStar_UInt128_uint128 tmp_w11 = o140;
+    FStar_UInt128_uint128 tmp_w12 = o240;
+    FStar_UInt128_uint128 tmp_w13 = o340;
+    FStar_UInt128_uint128 tmp_w14 = o440;
+    FStar_UInt128_uint128 o0 = FStar_UInt128_mul_wide(f30, f40);
+    FStar_UInt128_uint128 o1 = FStar_UInt128_mul_wide(f30, f41);
+    FStar_UInt128_uint128 o2 = FStar_UInt128_mul_wide(f30, f42);
+    FStar_UInt128_uint128 o3 = FStar_UInt128_mul_wide(f30, f43);
+    FStar_UInt128_uint128 o4 = FStar_UInt128_mul_wide(f30, f44);
+    FStar_UInt128_uint128 o01 = FStar_UInt128_add(o0, FStar_UInt128_mul_wide(f31, tmp24));
+    FStar_UInt128_uint128 o111 = FStar_UInt128_add(o1, FStar_UInt128_mul_wide(f31, f40));
+    FStar_UInt128_uint128 o211 = FStar_UInt128_add(o2, FStar_UInt128_mul_wide(f31, f41));
+    FStar_UInt128_uint128 o31 = FStar_UInt128_add(o3, FStar_UInt128_mul_wide(f31, f42));
+    FStar_UInt128_uint128 o41 = FStar_UInt128_add(o4, FStar_UInt128_mul_wide(f31, f43));
+    FStar_UInt128_uint128 o02 = FStar_UInt128_add(o01, FStar_UInt128_mul_wide(f32, tmp23));
+    FStar_UInt128_uint128 o121 = FStar_UInt128_add(o111, FStar_UInt128_mul_wide(f32, tmp24));
+    FStar_UInt128_uint128 o221 = FStar_UInt128_add(o211, FStar_UInt128_mul_wide(f32, f40));
+    FStar_UInt128_uint128 o32 = FStar_UInt128_add(o31, FStar_UInt128_mul_wide(f32, f41));
+    FStar_UInt128_uint128 o42 = FStar_UInt128_add(o41, FStar_UInt128_mul_wide(f32, f42));
+    FStar_UInt128_uint128 o03 = FStar_UInt128_add(o02, FStar_UInt128_mul_wide(f33, tmp22));
+    FStar_UInt128_uint128 o131 = FStar_UInt128_add(o121, FStar_UInt128_mul_wide(f33, tmp23));
+    FStar_UInt128_uint128 o231 = FStar_UInt128_add(o221, FStar_UInt128_mul_wide(f33, tmp24));
+    FStar_UInt128_uint128 o33 = FStar_UInt128_add(o32, FStar_UInt128_mul_wide(f33, f40));
+    FStar_UInt128_uint128 o43 = FStar_UInt128_add(o42, FStar_UInt128_mul_wide(f33, f41));
+    FStar_UInt128_uint128 o04 = FStar_UInt128_add(o03, FStar_UInt128_mul_wide(f34, tmp21));
+    FStar_UInt128_uint128 o141 = FStar_UInt128_add(o131, FStar_UInt128_mul_wide(f34, tmp22));
+    FStar_UInt128_uint128 o241 = FStar_UInt128_add(o231, FStar_UInt128_mul_wide(f34, tmp23));
+    FStar_UInt128_uint128 o34 = FStar_UInt128_add(o33, FStar_UInt128_mul_wide(f34, tmp24));
+    FStar_UInt128_uint128 o44 = FStar_UInt128_add(o43, FStar_UInt128_mul_wide(f34, f40));
+    FStar_UInt128_uint128 tmp_w20 = o04;
+    FStar_UInt128_uint128 tmp_w21 = o141;
+    FStar_UInt128_uint128 tmp_w22 = o241;
+    FStar_UInt128_uint128 tmp_w23 = o34;
+    FStar_UInt128_uint128 tmp_w24 = o44;
+    FStar_UInt128_uint128
+        l_ = FStar_UInt128_add(tmp_w10, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
+    uint64_t tmp00 = FStar_UInt128_uint128_to_uint64(l_) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c00 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_, (uint32_t)51U));
+    FStar_UInt128_uint128 l_0 = FStar_UInt128_add(tmp_w11, FStar_UInt128_uint64_to_uint128(c00));
+    uint64_t tmp10 = FStar_UInt128_uint128_to_uint64(l_0) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c10 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_0, (uint32_t)51U));
+    FStar_UInt128_uint128 l_1 = FStar_UInt128_add(tmp_w12, FStar_UInt128_uint64_to_uint128(c10));
+    uint64_t tmp20 = FStar_UInt128_uint128_to_uint64(l_1) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c20 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_1, (uint32_t)51U));
+    FStar_UInt128_uint128 l_2 = FStar_UInt128_add(tmp_w13, FStar_UInt128_uint64_to_uint128(c20));
+    uint64_t tmp30 = FStar_UInt128_uint128_to_uint64(l_2) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c30 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_2, (uint32_t)51U));
+    FStar_UInt128_uint128 l_3 = FStar_UInt128_add(tmp_w14, FStar_UInt128_uint64_to_uint128(c30));
+    uint64_t tmp40 = FStar_UInt128_uint128_to_uint64(l_3) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c40 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_3, (uint32_t)51U));
+    uint64_t l_4 = tmp00 + c40 * (uint64_t)19U;
+    uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
+    uint64_t c50 = l_4 >> (uint32_t)51U;
+    uint64_t o100 = tmp0_;
+    uint64_t o112 = tmp10 + c50;
+    uint64_t o122 = tmp20;
+    uint64_t o132 = tmp30;
+    uint64_t o142 = tmp40;
+    FStar_UInt128_uint128
+        l_5 = FStar_UInt128_add(tmp_w20, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
+    uint64_t tmp0 = FStar_UInt128_uint128_to_uint64(l_5) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c0 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_5, (uint32_t)51U));
+    FStar_UInt128_uint128 l_6 = FStar_UInt128_add(tmp_w21, FStar_UInt128_uint64_to_uint128(c0));
+    uint64_t tmp1 = FStar_UInt128_uint128_to_uint64(l_6) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c1 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_6, (uint32_t)51U));
+    FStar_UInt128_uint128 l_7 = FStar_UInt128_add(tmp_w22, FStar_UInt128_uint64_to_uint128(c1));
+    uint64_t tmp2 = FStar_UInt128_uint128_to_uint64(l_7) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_7, (uint32_t)51U));
+    FStar_UInt128_uint128 l_8 = FStar_UInt128_add(tmp_w23, FStar_UInt128_uint64_to_uint128(c2));
+    uint64_t tmp3 = FStar_UInt128_uint128_to_uint64(l_8) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c3 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_8, (uint32_t)51U));
+    FStar_UInt128_uint128 l_9 = FStar_UInt128_add(tmp_w24, FStar_UInt128_uint64_to_uint128(c3));
+    uint64_t tmp4 = FStar_UInt128_uint128_to_uint64(l_9) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_9, (uint32_t)51U));
+    uint64_t l_10 = tmp0 + c4 * (uint64_t)19U;
+    uint64_t tmp0_0 = l_10 & (uint64_t)0x7ffffffffffffU;
+    uint64_t c5 = l_10 >> (uint32_t)51U;
+    uint64_t o200 = tmp0_0;
+    uint64_t o212 = tmp1 + c5;
+    uint64_t o222 = tmp2;
+    uint64_t o232 = tmp3;
+    uint64_t o242 = tmp4;
+    uint64_t o10 = o100;
+    uint64_t o11 = o112;
+    uint64_t o12 = o122;
+    uint64_t o13 = o132;
+    uint64_t o14 = o142;
+    uint64_t o20 = o200;
+    uint64_t o21 = o212;
+    uint64_t o22 = o222;
+    uint64_t o23 = o232;
+    uint64_t o24 = o242;
+    out[0U] = o10;
+    out[1U] = o11;
+    out[2U] = o12;
+    out[3U] = o13;
+    out[4U] = o14;
+    out[5U] = o20;
+    out[6U] = o21;
+    out[7U] = o22;
+    out[8U] = o23;
+    out[9U] = o24;
+}
+
+static inline void
+Hacl_Impl_Curve25519_Field51_fmul1(uint64_t *out, uint64_t *f1, uint64_t f2)
+{
+    uint64_t f10 = f1[0U];
+    uint64_t f11 = f1[1U];
+    uint64_t f12 = f1[2U];
+    uint64_t f13 = f1[3U];
+    uint64_t f14 = f1[4U];
+    FStar_UInt128_uint128 tmp_w0 = FStar_UInt128_mul_wide(f2, f10);
+    FStar_UInt128_uint128 tmp_w1 = FStar_UInt128_mul_wide(f2, f11);
+    FStar_UInt128_uint128 tmp_w2 = FStar_UInt128_mul_wide(f2, f12);
+    FStar_UInt128_uint128 tmp_w3 = FStar_UInt128_mul_wide(f2, f13);
+    FStar_UInt128_uint128 tmp_w4 = FStar_UInt128_mul_wide(f2, f14);
+    FStar_UInt128_uint128
+        l_ = FStar_UInt128_add(tmp_w0, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
+    uint64_t tmp0 = FStar_UInt128_uint128_to_uint64(l_) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c0 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_, (uint32_t)51U));
+    FStar_UInt128_uint128 l_0 = FStar_UInt128_add(tmp_w1, FStar_UInt128_uint64_to_uint128(c0));
+    uint64_t tmp1 = FStar_UInt128_uint128_to_uint64(l_0) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c1 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_0, (uint32_t)51U));
+    FStar_UInt128_uint128 l_1 = FStar_UInt128_add(tmp_w2, FStar_UInt128_uint64_to_uint128(c1));
+    uint64_t tmp2 = FStar_UInt128_uint128_to_uint64(l_1) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_1, (uint32_t)51U));
+    FStar_UInt128_uint128 l_2 = FStar_UInt128_add(tmp_w3, FStar_UInt128_uint64_to_uint128(c2));
+    uint64_t tmp3 = FStar_UInt128_uint128_to_uint64(l_2) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c3 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_2, (uint32_t)51U));
+    FStar_UInt128_uint128 l_3 = FStar_UInt128_add(tmp_w4, FStar_UInt128_uint64_to_uint128(c3));
+    uint64_t tmp4 = FStar_UInt128_uint128_to_uint64(l_3) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_3, (uint32_t)51U));
+    uint64_t l_4 = tmp0 + c4 * (uint64_t)19U;
+    uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
+    uint64_t c5 = l_4 >> (uint32_t)51U;
+    uint64_t o0 = tmp0_;
+    uint64_t o1 = tmp1 + c5;
+    uint64_t o2 = tmp2;
+    uint64_t o3 = tmp3;
+    uint64_t o4 = tmp4;
+    out[0U] = o0;
+    out[1U] = o1;
+    out[2U] = o2;
+    out[3U] = o3;
+    out[4U] = o4;
+}
+
+static inline void
+Hacl_Impl_Curve25519_Field51_fsqr(uint64_t *out, uint64_t *f, FStar_UInt128_uint128 *uu___)
+{
+    uint64_t f0 = f[0U];
+    uint64_t f1 = f[1U];
+    uint64_t f2 = f[2U];
+    uint64_t f3 = f[3U];
+    uint64_t f4 = f[4U];
+    uint64_t d0 = (uint64_t)2U * f0;
+    uint64_t d1 = (uint64_t)2U * f1;
+    uint64_t d2 = (uint64_t)38U * f2;
+    uint64_t d3 = (uint64_t)19U * f3;
+    uint64_t d419 = (uint64_t)19U * f4;
+    uint64_t d4 = (uint64_t)2U * d419;
+    FStar_UInt128_uint128
+        s0 =
+            FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(f0, f0),
+                                                FStar_UInt128_mul_wide(d4, f1)),
+                              FStar_UInt128_mul_wide(d2, f3));
+    FStar_UInt128_uint128
+        s1 =
+            FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f1),
+                                                FStar_UInt128_mul_wide(d4, f2)),
+                              FStar_UInt128_mul_wide(d3, f3));
+    FStar_UInt128_uint128
+        s2 =
+            FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f2),
+                                                FStar_UInt128_mul_wide(f1, f1)),
+                              FStar_UInt128_mul_wide(d4, f3));
+    FStar_UInt128_uint128
+        s3 =
+            FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f3),
+                                                FStar_UInt128_mul_wide(d1, f2)),
+                              FStar_UInt128_mul_wide(f4, d419));
+    FStar_UInt128_uint128
+        s4 =
+            FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f4),
+                                                FStar_UInt128_mul_wide(d1, f3)),
+                              FStar_UInt128_mul_wide(f2, f2));
+    FStar_UInt128_uint128 o00 = s0;
+    FStar_UInt128_uint128 o10 = s1;
+    FStar_UInt128_uint128 o20 = s2;
+    FStar_UInt128_uint128 o30 = s3;
+    FStar_UInt128_uint128 o40 = s4;
+    FStar_UInt128_uint128
+        l_ = FStar_UInt128_add(o00, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
+    uint64_t tmp0 = FStar_UInt128_uint128_to_uint64(l_) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c0 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_, (uint32_t)51U));
+    FStar_UInt128_uint128 l_0 = FStar_UInt128_add(o10, FStar_UInt128_uint64_to_uint128(c0));
+    uint64_t tmp1 = FStar_UInt128_uint128_to_uint64(l_0) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c1 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_0, (uint32_t)51U));
+    FStar_UInt128_uint128 l_1 = FStar_UInt128_add(o20, FStar_UInt128_uint64_to_uint128(c1));
+    uint64_t tmp2 = FStar_UInt128_uint128_to_uint64(l_1) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_1, (uint32_t)51U));
+    FStar_UInt128_uint128 l_2 = FStar_UInt128_add(o30, FStar_UInt128_uint64_to_uint128(c2));
+    uint64_t tmp3 = FStar_UInt128_uint128_to_uint64(l_2) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c3 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_2, (uint32_t)51U));
+    FStar_UInt128_uint128 l_3 = FStar_UInt128_add(o40, FStar_UInt128_uint64_to_uint128(c3));
+    uint64_t tmp4 = FStar_UInt128_uint128_to_uint64(l_3) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_3, (uint32_t)51U));
+    uint64_t l_4 = tmp0 + c4 * (uint64_t)19U;
+    uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
+    uint64_t c5 = l_4 >> (uint32_t)51U;
+    uint64_t o0 = tmp0_;
+    uint64_t o1 = tmp1 + c5;
+    uint64_t o2 = tmp2;
+    uint64_t o3 = tmp3;
+    uint64_t o4 = tmp4;
+    out[0U] = o0;
+    out[1U] = o1;
+    out[2U] = o2;
+    out[3U] = o3;
+    out[4U] = o4;
+}
+
+static inline void
+Hacl_Impl_Curve25519_Field51_fsqr2(uint64_t *out, uint64_t *f, FStar_UInt128_uint128 *uu___)
+{
+    uint64_t f10 = f[0U];
+    uint64_t f11 = f[1U];
+    uint64_t f12 = f[2U];
+    uint64_t f13 = f[3U];
+    uint64_t f14 = f[4U];
+    uint64_t f20 = f[5U];
+    uint64_t f21 = f[6U];
+    uint64_t f22 = f[7U];
+    uint64_t f23 = f[8U];
+    uint64_t f24 = f[9U];
+    uint64_t d00 = (uint64_t)2U * f10;
+    uint64_t d10 = (uint64_t)2U * f11;
+    uint64_t d20 = (uint64_t)38U * f12;
+    uint64_t d30 = (uint64_t)19U * f13;
+    uint64_t d4190 = (uint64_t)19U * f14;
+    uint64_t d40 = (uint64_t)2U * d4190;
+    FStar_UInt128_uint128
+        s00 =
+            FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(f10, f10),
+                                                FStar_UInt128_mul_wide(d40, f11)),
+                              FStar_UInt128_mul_wide(d20, f13));
+    FStar_UInt128_uint128
+        s10 =
+            FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d00, f11),
+                                                FStar_UInt128_mul_wide(d40, f12)),
+                              FStar_UInt128_mul_wide(d30, f13));
+    FStar_UInt128_uint128
+        s20 =
+            FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d00, f12),
+                                                FStar_UInt128_mul_wide(f11, f11)),
+                              FStar_UInt128_mul_wide(d40, f13));
+    FStar_UInt128_uint128
+        s30 =
+            FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d00, f13),
+                                                FStar_UInt128_mul_wide(d10, f12)),
+                              FStar_UInt128_mul_wide(f14, d4190));
+    FStar_UInt128_uint128
+        s40 =
+            FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d00, f14),
+                                                FStar_UInt128_mul_wide(d10, f13)),
+                              FStar_UInt128_mul_wide(f12, f12));
+    FStar_UInt128_uint128 o100 = s00;
+    FStar_UInt128_uint128 o110 = s10;
+    FStar_UInt128_uint128 o120 = s20;
+    FStar_UInt128_uint128 o130 = s30;
+    FStar_UInt128_uint128 o140 = s40;
+    uint64_t d0 = (uint64_t)2U * f20;
+    uint64_t d1 = (uint64_t)2U * f21;
+    uint64_t d2 = (uint64_t)38U * f22;
+    uint64_t d3 = (uint64_t)19U * f23;
+    uint64_t d419 = (uint64_t)19U * f24;
+    uint64_t d4 = (uint64_t)2U * d419;
+    FStar_UInt128_uint128
+        s0 =
+            FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(f20, f20),
+                                                FStar_UInt128_mul_wide(d4, f21)),
+                              FStar_UInt128_mul_wide(d2, f23));
+    FStar_UInt128_uint128
+        s1 =
+            FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f21),
+                                                FStar_UInt128_mul_wide(d4, f22)),
+                              FStar_UInt128_mul_wide(d3, f23));
+    FStar_UInt128_uint128
+        s2 =
+            FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f22),
+                                                FStar_UInt128_mul_wide(f21, f21)),
+                              FStar_UInt128_mul_wide(d4, f23));
+    FStar_UInt128_uint128
+        s3 =
+            FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f23),
+                                                FStar_UInt128_mul_wide(d1, f22)),
+                              FStar_UInt128_mul_wide(f24, d419));
+    FStar_UInt128_uint128
+        s4 =
+            FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(d0, f24),
+                                                FStar_UInt128_mul_wide(d1, f23)),
+                              FStar_UInt128_mul_wide(f22, f22));
+    FStar_UInt128_uint128 o200 = s0;
+    FStar_UInt128_uint128 o210 = s1;
+    FStar_UInt128_uint128 o220 = s2;
+    FStar_UInt128_uint128 o230 = s3;
+    FStar_UInt128_uint128 o240 = s4;
+    FStar_UInt128_uint128
+        l_ = FStar_UInt128_add(o100, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
+    uint64_t tmp00 = FStar_UInt128_uint128_to_uint64(l_) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c00 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_, (uint32_t)51U));
+    FStar_UInt128_uint128 l_0 = FStar_UInt128_add(o110, FStar_UInt128_uint64_to_uint128(c00));
+    uint64_t tmp10 = FStar_UInt128_uint128_to_uint64(l_0) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c10 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_0, (uint32_t)51U));
+    FStar_UInt128_uint128 l_1 = FStar_UInt128_add(o120, FStar_UInt128_uint64_to_uint128(c10));
+    uint64_t tmp20 = FStar_UInt128_uint128_to_uint64(l_1) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c20 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_1, (uint32_t)51U));
+    FStar_UInt128_uint128 l_2 = FStar_UInt128_add(o130, FStar_UInt128_uint64_to_uint128(c20));
+    uint64_t tmp30 = FStar_UInt128_uint128_to_uint64(l_2) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c30 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_2, (uint32_t)51U));
+    FStar_UInt128_uint128 l_3 = FStar_UInt128_add(o140, FStar_UInt128_uint64_to_uint128(c30));
+    uint64_t tmp40 = FStar_UInt128_uint128_to_uint64(l_3) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c40 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_3, (uint32_t)51U));
+    uint64_t l_4 = tmp00 + c40 * (uint64_t)19U;
+    uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
+    uint64_t c50 = l_4 >> (uint32_t)51U;
+    uint64_t o101 = tmp0_;
+    uint64_t o111 = tmp10 + c50;
+    uint64_t o121 = tmp20;
+    uint64_t o131 = tmp30;
+    uint64_t o141 = tmp40;
+    FStar_UInt128_uint128
+        l_5 = FStar_UInt128_add(o200, FStar_UInt128_uint64_to_uint128((uint64_t)0U));
+    uint64_t tmp0 = FStar_UInt128_uint128_to_uint64(l_5) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c0 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_5, (uint32_t)51U));
+    FStar_UInt128_uint128 l_6 = FStar_UInt128_add(o210, FStar_UInt128_uint64_to_uint128(c0));
+    uint64_t tmp1 = FStar_UInt128_uint128_to_uint64(l_6) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c1 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_6, (uint32_t)51U));
+    FStar_UInt128_uint128 l_7 = FStar_UInt128_add(o220, FStar_UInt128_uint64_to_uint128(c1));
+    uint64_t tmp2 = FStar_UInt128_uint128_to_uint64(l_7) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c2 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_7, (uint32_t)51U));
+    FStar_UInt128_uint128 l_8 = FStar_UInt128_add(o230, FStar_UInt128_uint64_to_uint128(c2));
+    uint64_t tmp3 = FStar_UInt128_uint128_to_uint64(l_8) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c3 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_8, (uint32_t)51U));
+    FStar_UInt128_uint128 l_9 = FStar_UInt128_add(o240, FStar_UInt128_uint64_to_uint128(c3));
+    uint64_t tmp4 = FStar_UInt128_uint128_to_uint64(l_9) & (uint64_t)0x7ffffffffffffU;
+    uint64_t c4 = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(l_9, (uint32_t)51U));
+    uint64_t l_10 = tmp0 + c4 * (uint64_t)19U;
+    uint64_t tmp0_0 = l_10 & (uint64_t)0x7ffffffffffffU;
+    uint64_t c5 = l_10 >> (uint32_t)51U;
+    uint64_t o201 = tmp0_0;
+    uint64_t o211 = tmp1 + c5;
+    uint64_t o221 = tmp2;
+    uint64_t o231 = tmp3;
+    uint64_t o241 = tmp4;
+    uint64_t o10 = o101;
+    uint64_t o11 = o111;
+    uint64_t o12 = o121;
+    uint64_t o13 = o131;
+    uint64_t o14 = o141;
+    uint64_t o20 = o201;
+    uint64_t o21 = o211;
+    uint64_t o22 = o221;
+    uint64_t o23 = o231;
+    uint64_t o24 = o241;
+    out[0U] = o10;
+    out[1U] = o11;
+    out[2U] = o12;
+    out[3U] = o13;
+    out[4U] = o14;
+    out[5U] = o20;
+    out[6U] = o21;
+    out[7U] = o22;
+    out[8U] = o23;
+    out[9U] = o24;
+}
+
+static inline void
+Hacl_Impl_Curve25519_Field51_store_felem(uint64_t *u64s, uint64_t *f)
+{
+    uint64_t f0 = f[0U];
+    uint64_t f1 = f[1U];
+    uint64_t f2 = f[2U];
+    uint64_t f3 = f[3U];
+    uint64_t f4 = f[4U];
+    uint64_t l_ = f0 + (uint64_t)0U;
+    uint64_t tmp0 = l_ & (uint64_t)0x7ffffffffffffU;
+    uint64_t c0 = l_ >> (uint32_t)51U;
+    uint64_t l_0 = f1 + c0;
+    uint64_t tmp1 = l_0 & (uint64_t)0x7ffffffffffffU;
+    uint64_t c1 = l_0 >> (uint32_t)51U;
+    uint64_t l_1 = f2 + c1;
+    uint64_t tmp2 = l_1 & (uint64_t)0x7ffffffffffffU;
+    uint64_t c2 = l_1 >> (uint32_t)51U;
+    uint64_t l_2 = f3 + c2;
+    uint64_t tmp3 = l_2 & (uint64_t)0x7ffffffffffffU;
+    uint64_t c3 = l_2 >> (uint32_t)51U;
+    uint64_t l_3 = f4 + c3;
+    uint64_t tmp4 = l_3 & (uint64_t)0x7ffffffffffffU;
+    uint64_t c4 = l_3 >> (uint32_t)51U;
+    uint64_t l_4 = tmp0 + c4 * (uint64_t)19U;
+    uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
+    uint64_t c5 = l_4 >> (uint32_t)51U;
+    uint64_t f01 = tmp0_;
+    uint64_t f11 = tmp1 + c5;
+    uint64_t f21 = tmp2;
+    uint64_t f31 = tmp3;
+    uint64_t f41 = tmp4;
+    uint64_t m0 = FStar_UInt64_gte_mask(f01, (uint64_t)0x7ffffffffffedU);
+    uint64_t m1 = FStar_UInt64_eq_mask(f11, (uint64_t)0x7ffffffffffffU);
+    uint64_t m2 = FStar_UInt64_eq_mask(f21, (uint64_t)0x7ffffffffffffU);
+    uint64_t m3 = FStar_UInt64_eq_mask(f31, (uint64_t)0x7ffffffffffffU);
+    uint64_t m4 = FStar_UInt64_eq_mask(f41, (uint64_t)0x7ffffffffffffU);
+    uint64_t mask = (((m0 & m1) & m2) & m3) & m4;
+    uint64_t f0_ = f01 - (mask & (uint64_t)0x7ffffffffffedU);
+    uint64_t f1_ = f11 - (mask & (uint64_t)0x7ffffffffffffU);
+    uint64_t f2_ = f21 - (mask & (uint64_t)0x7ffffffffffffU);
+    uint64_t f3_ = f31 - (mask & (uint64_t)0x7ffffffffffffU);
+    uint64_t f4_ = f41 - (mask & (uint64_t)0x7ffffffffffffU);
+    uint64_t f02 = f0_;
+    uint64_t f12 = f1_;
+    uint64_t f22 = f2_;
+    uint64_t f32 = f3_;
+    uint64_t f42 = f4_;
+    uint64_t o00 = f02 | f12 << (uint32_t)51U;
+    uint64_t o10 = f12 >> (uint32_t)13U | f22 << (uint32_t)38U;
+    uint64_t o20 = f22 >> (uint32_t)26U | f32 << (uint32_t)25U;
+    uint64_t o30 = f32 >> (uint32_t)39U | f42 << (uint32_t)12U;
+    uint64_t o0 = o00;
+    uint64_t o1 = o10;
+    uint64_t o2 = o20;
+    uint64_t o3 = o30;
+    u64s[0U] = o0;
+    u64s[1U] = o1;
+    u64s[2U] = o2;
+    u64s[3U] = o3;
+}
+
+static inline void
+Hacl_Impl_Curve25519_Field51_cswap2(uint64_t bit, uint64_t *p1, uint64_t *p2)
+{
+    uint64_t mask = (uint64_t)0U - bit;
+    KRML_MAYBE_FOR10(i,
+                     (uint32_t)0U,
+                     (uint32_t)10U,
+                     (uint32_t)1U,
+                     uint64_t dummy = mask & (p1[i] ^ p2[i]);
+                     p1[i] = p1[i] ^ dummy;
+                     p2[i] = p2[i] ^ dummy;);
+}
+
+#if defined(__cplusplus)
+}
+#endif
+
+#define __internal_Hacl_Bignum25519_51_H_DEFINED
+#endif
diff --git a/security/nss/lib/freebl/verified/internal/Hacl_Bignum_Base.h b/security/nss/lib/freebl/verified/internal/Hacl_Bignum_Base.h
new file mode 100644
index 0000000000..a6e4fe63f0
--- /dev/null
+++ b/security/nss/lib/freebl/verified/internal/Hacl_Bignum_Base.h
@@ -0,0 +1,444 @@
+/* MIT License
+ *
+ * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation
+ * Copyright (c) 2022-2023 HACL* Contributors
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the Software is
+ * furnished to do so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+ * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+ * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+ * SOFTWARE.
+ */
+
+#ifndef __internal_Hacl_Bignum_Base_H
+#define __internal_Hacl_Bignum_Base_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
+#include <string.h>
+#include "krml/internal/types.h"
+#include "krml/internal/builtin.h"
+#include "krml/lowstar_endianness.h"
+#include "krml/internal/target.h"
+
+#include "internal/Hacl_Krmllib.h"
+#include "Hacl_Krmllib.h"
+#include "lib_intrinsics.h"
+
+static inline uint32_t
+Hacl_Bignum_Base_mul_wide_add2_u32(uint32_t a, uint32_t b, uint32_t c_in, uint32_t *out)
+{
+    uint32_t out0 = out[0U];
+    uint64_t res = (uint64_t)a * (uint64_t)b + (uint64_t)c_in + (uint64_t)out0;
+    out[0U] = (uint32_t)res;
+    return (uint32_t)(res >> (uint32_t)32U);
+}
+
+static inline uint64_t
+Hacl_Bignum_Base_mul_wide_add2_u64(uint64_t a, uint64_t b, uint64_t c_in, uint64_t *out)
+{
+    uint64_t out0 = out[0U];
+    FStar_UInt128_uint128
+        res =
+            FStar_UInt128_add(FStar_UInt128_add(FStar_UInt128_mul_wide(a, b),
+                                                FStar_UInt128_uint64_to_uint128(c_in)),
+                              FStar_UInt128_uint64_to_uint128(out0));
+    out[0U] = FStar_UInt128_uint128_to_uint64(res);
+    return FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(res, (uint32_t)64U));
+}
+
+static inline void
+Hacl_Bignum_Convert_bn_from_bytes_be_uint64(uint32_t len, uint8_t *b, uint64_t *res)
+{
+    uint32_t bnLen = (len - (uint32_t)1U) / (uint32_t)8U + (uint32_t)1U;
+    uint32_t tmpLen = (uint32_t)8U * bnLen;
+    KRML_CHECK_SIZE(sizeof(uint8_t), tmpLen);
+    uint8_t *tmp = (uint8_t *)alloca(tmpLen * sizeof(uint8_t));
+    memset(tmp, 0U, tmpLen * sizeof(uint8_t));
+    memcpy(tmp + tmpLen - len, b, len * sizeof(uint8_t));
+    for (uint32_t i = (uint32_t)0U; i < bnLen; i++) {
+        uint64_t *os = res;
+        uint64_t u = load64_be(tmp + (bnLen - i - (uint32_t)1U) * (uint32_t)8U);
+        uint64_t x = u;
+        os[i] = x;
+    }
+}
+
+static inline void
+Hacl_Bignum_Convert_bn_to_bytes_be_uint64(uint32_t len, uint64_t *b, uint8_t *res)
+{
+    uint32_t bnLen = (len - (uint32_t)1U) / (uint32_t)8U + (uint32_t)1U;
+    uint32_t tmpLen = (uint32_t)8U * bnLen;
+    KRML_CHECK_SIZE(sizeof(uint8_t), tmpLen);
+    uint8_t *tmp = (uint8_t *)alloca(tmpLen * sizeof(uint8_t));
+    memset(tmp, 0U, tmpLen * sizeof(uint8_t));
+    for (uint32_t i = (uint32_t)0U; i < bnLen; i++) {
+        store64_be(tmp + i * (uint32_t)8U, b[bnLen - i - (uint32_t)1U]);
+    }
+    memcpy(res, tmp + tmpLen - len, len * sizeof(uint8_t));
+}
+
+static inline uint32_t
+Hacl_Bignum_Lib_bn_get_top_index_u32(uint32_t len, uint32_t *b)
+{
+    uint32_t priv = (uint32_t)0U;
+    for (uint32_t i = (uint32_t)0U; i < len; i++) {
+        uint32_t mask = FStar_UInt32_eq_mask(b[i], (uint32_t)0U);
+        priv = (mask & priv) | (~mask & i);
+    }
+    return priv;
+}
+
+static inline uint64_t
+Hacl_Bignum_Lib_bn_get_top_index_u64(uint32_t len, uint64_t *b)
+{
+    uint64_t priv = (uint64_t)0U;
+    for (uint32_t i = (uint32_t)0U; i < len; i++) {
+        uint64_t mask = FStar_UInt64_eq_mask(b[i], (uint64_t)0U);
+        priv = (mask & priv) | (~mask & (uint64_t)i);
+    }
+    return priv;
+}
+
+static inline uint32_t
+Hacl_Bignum_Lib_bn_get_bits_u32(uint32_t len, uint32_t *b, uint32_t i, uint32_t l)
+{
+    uint32_t i1 = i / (uint32_t)32U;
+    uint32_t j = i % (uint32_t)32U;
+    uint32_t p1 = b[i1] >> j;
+    uint32_t ite;
+    if (i1 + (uint32_t)1U < len && (uint32_t)0U < j) {
+        ite = p1 | b[i1 + (uint32_t)1U] << ((uint32_t)32U - j);
+    } else {
+        ite = p1;
+    }
+    return ite & (((uint32_t)1U << l) - (uint32_t)1U);
+}
+
+static inline uint64_t
+Hacl_Bignum_Lib_bn_get_bits_u64(uint32_t len, uint64_t *b, uint32_t i, uint32_t l)
+{
+    uint32_t i1 = i / (uint32_t)64U;
+    uint32_t j = i % (uint32_t)64U;
+    uint64_t p1 = b[i1] >> j;
+    uint64_t ite;
+    if (i1 + (uint32_t)1U < len && (uint32_t)0U < j) {
+        ite = p1 | b[i1 + (uint32_t)1U] << ((uint32_t)64U - j);
+    } else {
+        ite = p1;
+    }
+    return ite & (((uint64_t)1U << l) - (uint64_t)1U);
+}
+
+static inline uint32_t
+Hacl_Bignum_Addition_bn_sub_eq_len_u32(uint32_t aLen, uint32_t *a, uint32_t *b, uint32_t *res)
+{
+    uint32_t c = (uint32_t)0U;
+    for (uint32_t i = (uint32_t)0U; i < aLen / (uint32_t)4U; i++) {
+        uint32_t t1 = a[(uint32_t)4U * i];
+        uint32_t t20 = b[(uint32_t)4U * i];
+        uint32_t *res_i0 = res + (uint32_t)4U * i;
+        c = Lib_IntTypes_Intrinsics_sub_borrow_u32(c, t1, t20, res_i0);
+        uint32_t t10 = a[(uint32_t)4U * i + (uint32_t)1U];
+        uint32_t t21 = b[(uint32_t)4U * i + (uint32_t)1U];
+        uint32_t *res_i1 = res + (uint32_t)4U * i + (uint32_t)1U;
+        c = Lib_IntTypes_Intrinsics_sub_borrow_u32(c, t10, t21, res_i1);
+        uint32_t t11 = a[(uint32_t)4U * i + (uint32_t)2U];
+        uint32_t t22 = b[(uint32_t)4U * i + (uint32_t)2U];
+        uint32_t *res_i2 = res + (uint32_t)4U * i + (uint32_t)2U;
+        c = Lib_IntTypes_Intrinsics_sub_borrow_u32(c, t11, t22, res_i2);
+        uint32_t t12 = a[(uint32_t)4U * i + (uint32_t)3U];
+        uint32_t t2 = b[(uint32_t)4U * i + (uint32_t)3U];
+        uint32_t *res_i = res + (uint32_t)4U * i + (uint32_t)3U;
+        c = Lib_IntTypes_Intrinsics_sub_borrow_u32(c, t12, t2, res_i);
+    }
+    for (uint32_t i = aLen / (uint32_t)4U * (uint32_t)4U; i < aLen; i++) {
+        uint32_t t1 = a[i];
+        uint32_t t2 = b[i];
+        uint32_t *res_i = res + i;
+        c = Lib_IntTypes_Intrinsics_sub_borrow_u32(c, t1, t2, res_i);
+    }
+    return c;
+}
+
+static inline uint64_t
+Hacl_Bignum_Addition_bn_sub_eq_len_u64(uint32_t aLen, uint64_t *a, uint64_t *b, uint64_t *res)
+{
+    uint64_t c = (uint64_t)0U;
+    for (uint32_t i = (uint32_t)0U; i < aLen / (uint32_t)4U; i++) {
+        uint64_t t1 = a[(uint32_t)4U * i];
+        uint64_t t20 = b[(uint32_t)4U * i];
+        uint64_t *res_i0 = res + (uint32_t)4U * i;
+        c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t1, t20, res_i0);
+        uint64_t t10 = a[(uint32_t)4U * i + (uint32_t)1U];
+        uint64_t t21 = b[(uint32_t)4U * i + (uint32_t)1U];
+        uint64_t *res_i1 = res + (uint32_t)4U * i + (uint32_t)1U;
+        c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t10, t21, res_i1);
+        uint64_t t11 = a[(uint32_t)4U * i + (uint32_t)2U];
+        uint64_t t22 = b[(uint32_t)4U * i + (uint32_t)2U];
+        uint64_t *res_i2 = res + (uint32_t)4U * i + (uint32_t)2U;
+        c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t11, t22, res_i2);
+        uint64_t t12 = a[(uint32_t)4U * i + (uint32_t)3U];
+        uint64_t t2 = b[(uint32_t)4U * i + (uint32_t)3U];
+        uint64_t *res_i = res + (uint32_t)4U * i + (uint32_t)3U;
+        c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t12, t2, res_i);
+    }
+    for (uint32_t i = aLen / (uint32_t)4U * (uint32_t)4U; i < aLen; i++) {
+        uint64_t t1 = a[i];
+        uint64_t t2 = b[i];
+        uint64_t *res_i = res + i;
+        c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t1, t2, res_i);
+    }
+    return c;
+}
+
+static inline uint32_t
+Hacl_Bignum_Addition_bn_add_eq_len_u32(uint32_t aLen, uint32_t *a, uint32_t *b, uint32_t *res)
+{
+    uint32_t c = (uint32_t)0U;
+    for (uint32_t i = (uint32_t)0U; i < aLen / (uint32_t)4U; i++) {
+        uint32_t t1 = a[(uint32_t)4U * i];
+        uint32_t t20 = b[(uint32_t)4U * i];
+        uint32_t *res_i0 = res + (uint32_t)4U * i;
+        c = Lib_IntTypes_Intrinsics_add_carry_u32(c, t1, t20, res_i0);
+        uint32_t t10 = a[(uint32_t)4U * i + (uint32_t)1U];
+        uint32_t t21 = b[(uint32_t)4U * i + (uint32_t)1U];
+        uint32_t *res_i1 = res + (uint32_t)4U * i + (uint32_t)1U;
+        c = Lib_IntTypes_Intrinsics_add_carry_u32(c, t10, t21, res_i1);
+        uint32_t t11 = a[(uint32_t)4U * i + (uint32_t)2U];
+        uint32_t t22 = b[(uint32_t)4U * i + (uint32_t)2U];
+        uint32_t *res_i2 = res + (uint32_t)4U * i + (uint32_t)2U;
+        c = Lib_IntTypes_Intrinsics_add_carry_u32(c, t11, t22, res_i2);
+        uint32_t t12 = a[(uint32_t)4U * i + (uint32_t)3U];
+        uint32_t t2 = b[(uint32_t)4U * i + (uint32_t)3U];
+        uint32_t *res_i = res + (uint32_t)4U * i + (uint32_t)3U;
+        c = Lib_IntTypes_Intrinsics_add_carry_u32(c, t12, t2, res_i);
+    }
+    for (uint32_t i = aLen / (uint32_t)4U * (uint32_t)4U; i < aLen; i++) {
+        uint32_t t1 = a[i];
+        uint32_t t2 = b[i];
+        uint32_t *res_i = res + i;
+        c = Lib_IntTypes_Intrinsics_add_carry_u32(c, t1, t2, res_i);
+    }
+    return c;
+}
+
+static inline uint64_t
+Hacl_Bignum_Addition_bn_add_eq_len_u64(uint32_t aLen, uint64_t *a, uint64_t *b, uint64_t *res)
+{
+    uint64_t c = (uint64_t)0U;
+    for (uint32_t i = (uint32_t)0U; i < aLen / (uint32_t)4U; i++) {
+        uint64_t t1 = a[(uint32_t)4U * i];
+        uint64_t t20 = b[(uint32_t)4U * i];
+        uint64_t *res_i0 = res + (uint32_t)4U * i;
+        c = Lib_IntTypes_Intrinsics_add_carry_u64(c, t1, t20, res_i0);
+        uint64_t t10 = a[(uint32_t)4U * i + (uint32_t)1U];
+        uint64_t t21 = b[(uint32_t)4U * i + (uint32_t)1U];
+        uint64_t *res_i1 = res + (uint32_t)4U * i + (uint32_t)1U;
+        c = Lib_IntTypes_Intrinsics_add_carry_u64(c, t10, t21, res_i1);
+        uint64_t t11 = a[(uint32_t)4U * i + (uint32_t)2U];
+        uint64_t t22 = b[(uint32_t)4U * i + (uint32_t)2U];
+        uint64_t *res_i2 = res + (uint32_t)4U * i + (uint32_t)2U;
+        c = Lib_IntTypes_Intrinsics_add_carry_u64(c, t11, t22, res_i2);
+        uint64_t t12 = a[(uint32_t)4U * i + (uint32_t)3U];
+        uint64_t t2 = b[(uint32_t)4U * i + (uint32_t)3U];
+        uint64_t *res_i = res + (uint32_t)4U * i + (uint32_t)3U;
+        c = Lib_IntTypes_Intrinsics_add_carry_u64(c, t12, t2, res_i);
+    }
+    for (uint32_t i = aLen / (uint32_t)4U * (uint32_t)4U; i < aLen; i++) {
+        uint64_t t1 = a[i];
+        uint64_t t2 = b[i];
+        uint64_t *res_i = res + i;
+        c = Lib_IntTypes_Intrinsics_add_carry_u64(c, t1, t2, res_i);
+    }
+    return c;
+}
+
+static inline void
+Hacl_Bignum_Multiplication_bn_mul_u32(
+    uint32_t aLen,
+    uint32_t *a,
+    uint32_t bLen,
+    uint32_t *b,
+    uint32_t *res)
+{
+    memset(res, 0U, (aLen + bLen) * sizeof(uint32_t));
+    for (uint32_t i0 = (uint32_t)0U; i0 < bLen; i0++) {
+        uint32_t bj = b[i0];
+        uint32_t *res_j = res + i0;
+        uint32_t c = (uint32_t)0U;
+        for (uint32_t i = (uint32_t)0U; i < aLen / (uint32_t)4U; i++) {
+            uint32_t a_i = a[(uint32_t)4U * i];
+            uint32_t *res_i0 = res_j + (uint32_t)4U * i;
+            c = Hacl_Bignum_Base_mul_wide_add2_u32(a_i, bj, c, res_i0);
+            uint32_t a_i0 = a[(uint32_t)4U * i + (uint32_t)1U];
+            uint32_t *res_i1 = res_j + (uint32_t)4U * i + (uint32_t)1U;
+            c = Hacl_Bignum_Base_mul_wide_add2_u32(a_i0, bj, c, res_i1);
+            uint32_t a_i1 = a[(uint32_t)4U * i + (uint32_t)2U];
+            uint32_t *res_i2 = res_j + (uint32_t)4U * i + (uint32_t)2U;
+            c = Hacl_Bignum_Base_mul_wide_add2_u32(a_i1, bj, c, res_i2);
+            uint32_t a_i2 = a[(uint32_t)4U * i + (uint32_t)3U];
+            uint32_t *res_i = res_j + (uint32_t)4U * i + (uint32_t)3U;
+            c = Hacl_Bignum_Base_mul_wide_add2_u32(a_i2, bj, c, res_i);
+        }
+        for (uint32_t i = aLen / (uint32_t)4U * (uint32_t)4U; i < aLen; i++) {
+            uint32_t a_i = a[i];
+            uint32_t *res_i = res_j + i;
+            c = Hacl_Bignum_Base_mul_wide_add2_u32(a_i, bj, c, res_i);
+        }
+        uint32_t r = c;
+        res[aLen + i0] = r;
+    }
+}
+
+static inline void
+Hacl_Bignum_Multiplication_bn_mul_u64(
+    uint32_t aLen,
+    uint64_t *a,
+    uint32_t bLen,
+    uint64_t *b,
+    uint64_t *res)
+{
+    memset(res, 0U, (aLen + bLen) * sizeof(uint64_t));
+    for (uint32_t i0 = (uint32_t)0U; i0 < bLen; i0++) {
+        uint64_t bj = b[i0];
+        uint64_t *res_j = res + i0;
+        uint64_t c = (uint64_t)0U;
+        for (uint32_t i = (uint32_t)0U; i < aLen / (uint32_t)4U; i++) {
+            uint64_t a_i = a[(uint32_t)4U * i];
+            uint64_t *res_i0 = res_j + (uint32_t)4U * i;
+            c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, bj, c, res_i0);
+            uint64_t a_i0 = a[(uint32_t)4U * i + (uint32_t)1U];
+            uint64_t *res_i1 = res_j + (uint32_t)4U * i + (uint32_t)1U;
+            c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i0, bj, c, res_i1);
+            uint64_t a_i1 = a[(uint32_t)4U * i + (uint32_t)2U];
+            uint64_t *res_i2 = res_j + (uint32_t)4U * i + (uint32_t)2U;
+            c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i1, bj, c, res_i2);
+            uint64_t a_i2 = a[(uint32_t)4U * i + (uint32_t)3U];
+            uint64_t *res_i = res_j + (uint32_t)4U * i + (uint32_t)3U;
+            c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i2, bj, c, res_i);
+        }
+        for (uint32_t i = aLen / (uint32_t)4U * (uint32_t)4U; i < aLen; i++) {
+            uint64_t a_i = a[i];
+            uint64_t *res_i = res_j + i;
+            c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, bj, c, res_i);
+        }
+        uint64_t r = c;
+        res[aLen + i0] = r;
+    }
+}
+
+static inline void
+Hacl_Bignum_Multiplication_bn_sqr_u32(uint32_t aLen, uint32_t *a, uint32_t *res)
+{
+    memset(res, 0U, (aLen + aLen) * sizeof(uint32_t));
+    for (uint32_t i0 = (uint32_t)0U; i0 < aLen; i0++) {
+        uint32_t *ab = a;
+        uint32_t a_j = a[i0];
+        uint32_t *res_j = res + i0;
+        uint32_t c = (uint32_t)0U;
+        for (uint32_t i = (uint32_t)0U; i < i0 / (uint32_t)4U; i++) {
+            uint32_t a_i = ab[(uint32_t)4U * i];
+            uint32_t *res_i0 = res_j + (uint32_t)4U * i;
+            c = Hacl_Bignum_Base_mul_wide_add2_u32(a_i, a_j, c, res_i0);
+            uint32_t a_i0 = ab[(uint32_t)4U * i + (uint32_t)1U];
+            uint32_t *res_i1 = res_j + (uint32_t)4U * i + (uint32_t)1U;
+            c = Hacl_Bignum_Base_mul_wide_add2_u32(a_i0, a_j, c, res_i1);
+            uint32_t a_i1 = ab[(uint32_t)4U * i + (uint32_t)2U];
+            uint32_t *res_i2 = res_j + (uint32_t)4U * i + (uint32_t)2U;
+            c = Hacl_Bignum_Base_mul_wide_add2_u32(a_i1, a_j, c, res_i2);
+            uint32_t a_i2 = ab[(uint32_t)4U * i + (uint32_t)3U];
+            uint32_t *res_i = res_j + (uint32_t)4U * i + (uint32_t)3U;
+            c = Hacl_Bignum_Base_mul_wide_add2_u32(a_i2, a_j, c, res_i);
+        }
+        for (uint32_t i = i0 / (uint32_t)4U * (uint32_t)4U; i < i0; i++) {
+            uint32_t a_i = ab[i];
+            uint32_t *res_i = res_j + i;
+            c = Hacl_Bignum_Base_mul_wide_add2_u32(a_i, a_j, c, res_i);
+        }
+        uint32_t r = c;
+        res[i0 + i0] = r;
+    }
+    uint32_t c0 = Hacl_Bignum_Addition_bn_add_eq_len_u32(aLen + aLen, res, res, res);
+    KRML_HOST_IGNORE(c0);
+    KRML_CHECK_SIZE(sizeof(uint32_t), aLen + aLen);
+    uint32_t *tmp = (uint32_t *)alloca((aLen + aLen) * sizeof(uint32_t));
+    memset(tmp, 0U, (aLen + aLen) * sizeof(uint32_t));
+    for (uint32_t i = (uint32_t)0U; i < aLen; i++) {
+        uint64_t res1 = (uint64_t)a[i] * (uint64_t)a[i];
+        uint32_t hi = (uint32_t)(res1 >> (uint32_t)32U);
+        uint32_t lo = (uint32_t)res1;
+        tmp[(uint32_t)2U * i] = lo;
+        tmp[(uint32_t)2U * i + (uint32_t)1U] = hi;
+    }
+    uint32_t c1 = Hacl_Bignum_Addition_bn_add_eq_len_u32(aLen + aLen, res, tmp, res);
+    KRML_HOST_IGNORE(c1);
+}
+
+static inline void
+Hacl_Bignum_Multiplication_bn_sqr_u64(uint32_t aLen, uint64_t *a, uint64_t *res)
+{
+    memset(res, 0U, (aLen + aLen) * sizeof(uint64_t));
+    for (uint32_t i0 = (uint32_t)0U; i0 < aLen; i0++) {
+        uint64_t *ab = a;
+        uint64_t a_j = a[i0];
+        uint64_t *res_j = res + i0;
+        uint64_t c = (uint64_t)0U;
+        for (uint32_t i = (uint32_t)0U; i < i0 / (uint32_t)4U; i++) {
+            uint64_t a_i = ab[(uint32_t)4U * i];
+            uint64_t *res_i0 = res_j + (uint32_t)4U * i;
+            c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, a_j, c, res_i0);
+            uint64_t a_i0 = ab[(uint32_t)4U * i + (uint32_t)1U];
+            uint64_t *res_i1 = res_j + (uint32_t)4U * i + (uint32_t)1U;
+            c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i0, a_j, c, res_i1);
+            uint64_t a_i1 = ab[(uint32_t)4U * i + (uint32_t)2U];
+            uint64_t *res_i2 = res_j + (uint32_t)4U * i + (uint32_t)2U;
+            c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i1, a_j, c, res_i2);
+            uint64_t a_i2 = ab[(uint32_t)4U * i + (uint32_t)3U];
+            uint64_t *res_i = res_j + (uint32_t)4U * i + (uint32_t)3U;
+            c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i2, a_j, c, res_i);
+        }
+        for (uint32_t i = i0 / (uint32_t)4U * (uint32_t)4U; i < i0; i++) {
+            uint64_t a_i = ab[i];
+            uint64_t *res_i = res_j + i;
+            c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, a_j, c, res_i);
+        }
+        uint64_t r = c;
+        res[i0 + i0] = r;
+    }
+    uint64_t c0 = Hacl_Bignum_Addition_bn_add_eq_len_u64(aLen + aLen, res, res, res);
+    KRML_HOST_IGNORE(c0);
+    KRML_CHECK_SIZE(sizeof(uint64_t), aLen + aLen);
+    uint64_t *tmp = (uint64_t *)alloca((aLen + aLen) * sizeof(uint64_t));
+    memset(tmp, 0U, (aLen + aLen) * sizeof(uint64_t));
+    for (uint32_t i = (uint32_t)0U; i < aLen; i++) {
+        FStar_UInt128_uint128 res1 = FStar_UInt128_mul_wide(a[i], a[i]);
+        uint64_t hi = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(res1, (uint32_t)64U));
+        uint64_t lo = FStar_UInt128_uint128_to_uint64(res1);
+        tmp[(uint32_t)2U * i] = lo;
+        tmp[(uint32_t)2U * i + (uint32_t)1U] = hi;
+    }
+    uint64_t c1 = Hacl_Bignum_Addition_bn_add_eq_len_u64(aLen + aLen, res, tmp, res);
+    KRML_HOST_IGNORE(c1);
+}
+
+#if defined(__cplusplus)
+}
+#endif
+
+#define __internal_Hacl_Bignum_Base_H_DEFINED
+#endif
diff --git a/security/nss/lib/freebl/verified/internal/Hacl_Chacha20.h b/security/nss/lib/freebl/verified/internal/Hacl_Chacha20.h
new file mode 100644
index 0000000000..d0edbc3cea
--- /dev/null
+++ b/security/nss/lib/freebl/verified/internal/Hacl_Chacha20.h
@@ -0,0 +1,51 @@
+/* MIT License
+ *
+ * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation
+ * Copyright (c) 2022-2023 HACL* Contributors
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the Software is
+ * furnished to do so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+ * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+ * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+ * SOFTWARE.
+ */
+
+#ifndef __internal_Hacl_Chacha20_H
+#define __internal_Hacl_Chacha20_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
+#include <string.h>
+#include "krml/internal/types.h"
+#include "krml/lowstar_endianness.h"
+#include "krml/internal/target.h"
+
+#include "../Hacl_Chacha20.h"
+
+extern const uint32_t Hacl_Impl_Chacha20_Vec_chacha20_constants[4U];
+
+void Hacl_Impl_Chacha20_chacha20_init(uint32_t *ctx, uint8_t *k, uint8_t *n, uint32_t ctr);
+
+void
+Hacl_Impl_Chacha20_chacha20_update(uint32_t *ctx, uint32_t len, uint8_t *out, uint8_t *text);
+
+#if defined(__cplusplus)
+}
+#endif
+
+#define __internal_Hacl_Chacha20_H_DEFINED
+#endif
diff --git a/security/nss/lib/freebl/verified/internal/Hacl_Curve25519_51.h b/security/nss/lib/freebl/verified/internal/Hacl_Curve25519_51.h
new file mode 100644
index 0000000000..cb4eb15ffa
--- /dev/null
+++ b/security/nss/lib/freebl/verified/internal/Hacl_Curve25519_51.h
@@ -0,0 +1,55 @@
+/* MIT License
+ *
+ * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation
+ * Copyright (c) 2022-2023 HACL* Contributors
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the Software is
+ * furnished to do so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+ * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+ * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+ * SOFTWARE.
+ */
+
+#ifndef __internal_Hacl_Curve25519_51_H
+#define __internal_Hacl_Curve25519_51_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
+#include <string.h>
+#include "krml/internal/types.h"
+#include "krml/lowstar_endianness.h"
+#include "krml/internal/target.h"
+
+#include "internal/Hacl_Krmllib.h"
+#include "internal/Hacl_Bignum25519_51.h"
+#include "../Hacl_Curve25519_51.h"
+
+void
+Hacl_Curve25519_51_fsquare_times(
+    uint64_t *o,
+    uint64_t *inp,
+    FStar_UInt128_uint128 *tmp,
+    uint32_t n);
+
+void Hacl_Curve25519_51_finv(uint64_t *o, uint64_t *i, FStar_UInt128_uint128 *tmp);
+
+#if defined(__cplusplus)
+}
+#endif
+
+#define __internal_Hacl_Curve25519_51_H_DEFINED
+#endif
diff --git a/security/nss/lib/freebl/verified/internal/Hacl_Hash_SHA3.h b/security/nss/lib/freebl/verified/internal/Hacl_Hash_SHA3.h
new file mode 100644
index 0000000000..fedbe967f5
--- /dev/null
+++ b/security/nss/lib/freebl/verified/internal/Hacl_Hash_SHA3.h
@@ -0,0 +1,62 @@
+/* MIT License
+ *
+ * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation
+ * Copyright (c) 2022-2023 HACL* Contributors
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the Software is
+ * furnished to do so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+ * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+ * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+ * SOFTWARE.
+ */
+
+#ifndef __internal_Hacl_Hash_SHA3_H
+#define __internal_Hacl_Hash_SHA3_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
+#include <string.h>
+#include "krml/internal/types.h"
+#include "krml/lowstar_endianness.h"
+#include "krml/internal/target.h"
+
+#include "../Hacl_Hash_SHA3.h"
+
+void
+Hacl_Hash_SHA3_update_multi_sha3(
+    Spec_Hash_Definitions_hash_alg a,
+    uint64_t *s,
+    uint8_t *blocks,
+    uint32_t n_blocks);
+
+void
+Hacl_Hash_SHA3_update_last_sha3(
+    Spec_Hash_Definitions_hash_alg a,
+    uint64_t *s,
+    uint8_t *input,
+    uint32_t input_len);
+
+void Hacl_Impl_SHA3_state_permute(uint64_t *s);
+
+void Hacl_Impl_SHA3_loadState(uint32_t rateInBytes, uint8_t *input, uint64_t *s);
+
+#if defined(__cplusplus)
+}
+#endif
+
+#define __internal_Hacl_Hash_SHA3_H_DEFINED
+#endif
diff --git a/security/nss/lib/freebl/verified/internal/Hacl_Krmllib.h b/security/nss/lib/freebl/verified/internal/Hacl_Krmllib.h
new file mode 100644
index 0000000000..79836ae790
--- /dev/null
+++ b/security/nss/lib/freebl/verified/internal/Hacl_Krmllib.h
@@ -0,0 +1,67 @@
+/* MIT License
+ *
+ * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation
+ * Copyright (c) 2022-2023 HACL* Contributors
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the Software is
+ * furnished to do so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+ * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+ * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+ * SOFTWARE.
+ */
+
+#ifndef __internal_Hacl_Krmllib_H
+#define __internal_Hacl_Krmllib_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
+#include <string.h>
+#include "krml/internal/types.h"
+#include "krml/lowstar_endianness.h"
+#include "krml/internal/target.h"
+
+#include "../Hacl_Krmllib.h"
+
+static KRML_NOINLINE uint32_t FStar_UInt32_eq_mask(uint32_t a, uint32_t b);
+
+static KRML_NOINLINE uint32_t FStar_UInt32_gte_mask(uint32_t a, uint32_t b);
+
+static KRML_NOINLINE uint8_t FStar_UInt8_eq_mask(uint8_t a, uint8_t b);
+
+static KRML_NOINLINE uint16_t FStar_UInt16_eq_mask(uint16_t a, uint16_t b);
+
+static inline FStar_UInt128_uint128
+FStar_UInt128_add(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_shift_left(FStar_UInt128_uint128 a, uint32_t s);
+
+static inline FStar_UInt128_uint128 FStar_UInt128_mul_wide(uint64_t x, uint64_t y);
+
+static inline void store128_be(uint8_t *x0, FStar_UInt128_uint128 x1);
+
+static inline FStar_UInt128_uint128 load128_be(uint8_t *x0);
+
+#if defined(__cplusplus)
+}
+#endif
+
+#define __internal_Hacl_Krmllib_H_DEFINED
+#endif
diff --git a/security/nss/lib/freebl/verified/internal/Hacl_P256.h b/security/nss/lib/freebl/verified/internal/Hacl_P256.h
new file mode 100644
index 0000000000..6e07194d53
--- /dev/null
+++ b/security/nss/lib/freebl/verified/internal/Hacl_P256.h
@@ -0,0 +1,56 @@
+/* MIT License
+ *
+ * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation
+ * Copyright (c) 2022-2023 HACL* Contributors
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the Software is
+ * furnished to do so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+ * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+ * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+ * SOFTWARE.
+ */
+
+#ifndef __internal_Hacl_P256_H
+#define __internal_Hacl_P256_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
+#include <string.h>
+#include "krml/internal/types.h"
+#include "krml/lowstar_endianness.h"
+#include "krml/internal/target.h"
+
+#include "internal/Hacl_P256_PrecompTable.h"
+#include "internal/Hacl_Krmllib.h"
+#include "internal/Hacl_Bignum_Base.h"
+#include "../Hacl_P256.h"
+#include "lib_intrinsics.h"
+
+bool Hacl_Impl_P256_DH_ecp256dh_i(uint8_t *public_key, uint8_t *private_key);
+
+bool
+Hacl_Impl_P256_DH_ecp256dh_r(
+    uint8_t *shared_secret,
+    uint8_t *their_pubkey,
+    uint8_t *private_key);
+
+#if defined(__cplusplus)
+}
+#endif
+
+#define __internal_Hacl_P256_H_DEFINED
+#endif
diff --git a/security/nss/lib/freebl/verified/internal/Hacl_P256_PrecompTable.h b/security/nss/lib/freebl/verified/internal/Hacl_P256_PrecompTable.h
new file mode 100644
index 0000000000..93e2591875
--- /dev/null
+++ b/security/nss/lib/freebl/verified/internal/Hacl_P256_PrecompTable.h
@@ -0,0 +1,508 @@
+/* MIT License
+ *
+ * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation
+ * Copyright (c) 2022-2023 HACL* Contributors
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the Software is
+ * furnished to do so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+ * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+ * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+ * SOFTWARE.
+ */
+
+#ifndef __internal_Hacl_P256_PrecompTable_H
+#define __internal_Hacl_P256_PrecompTable_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
+#include <string.h>
+#include "krml/internal/types.h"
+#include "krml/lowstar_endianness.h"
+#include "krml/internal/target.h"
+
+static const uint64_t
+    Hacl_P256_PrecompTable_precomp_basepoint_table_w4[192U] = {
+        (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)1U,
+        (uint64_t)18446744069414584320U, (uint64_t)18446744073709551615U, (uint64_t)4294967294U,
+        (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)8784043285714375740U,
+        (uint64_t)8483257759279461889U, (uint64_t)8789745728267363600U, (uint64_t)1770019616739251654U,
+        (uint64_t)15992936863339206154U, (uint64_t)10037038012062884956U,
+        (uint64_t)15197544864945402661U, (uint64_t)9615747158586711429U, (uint64_t)1U,
+        (uint64_t)18446744069414584320U, (uint64_t)18446744073709551615U, (uint64_t)4294967294U,
+        (uint64_t)10634854829044225757U, (uint64_t)351552716085025155U, (uint64_t)10645315080955407736U,
+        (uint64_t)3609262091244858135U, (uint64_t)15760741698986874125U,
+        (uint64_t)14936374388219697827U, (uint64_t)15751360096993017895U,
+        (uint64_t)18012233706239762398U, (uint64_t)1993877568177495041U,
+        (uint64_t)10345888787846536528U, (uint64_t)7746511691117935375U,
+        (uint64_t)14517043990409914413U, (uint64_t)14122549297570634151U,
+        (uint64_t)16934610359517083771U, (uint64_t)5724511325497097418U, (uint64_t)8983432969107448705U,
+        (uint64_t)2687429970334080245U, (uint64_t)16525396802810050288U, (uint64_t)7602596488871585854U,
+        (uint64_t)4813919589149203084U, (uint64_t)7680395813780804519U, (uint64_t)6687709583048023590U,
+        (uint64_t)18086445169104142027U, (uint64_t)9637814708330203929U,
+        (uint64_t)14785108459960679090U, (uint64_t)3838023279095023581U, (uint64_t)3555615526157830307U,
+        (uint64_t)5177066488380472871U, (uint64_t)18218186719108038403U,
+        (uint64_t)16281556341699656105U, (uint64_t)1524227924561461191U, (uint64_t)4148060517641909597U,
+        (uint64_t)2858290374115363433U, (uint64_t)8942772026334130620U, (uint64_t)3034451298319885113U,
+        (uint64_t)8447866036736640940U, (uint64_t)11204933433076256578U,
+        (uint64_t)18333595740249588297U, (uint64_t)8259597024804538246U, (uint64_t)9539734295777539786U,
+        (uint64_t)9797290423046626413U, (uint64_t)5777303437849646537U, (uint64_t)8739356909899132020U,
+        (uint64_t)14815960973766782158U, (uint64_t)15286581798204509801U,
+        (uint64_t)17597362577777019682U, (uint64_t)13259283710820519742U,
+        (uint64_t)10501322996899164670U, (uint64_t)1221138904338319642U,
+        (uint64_t)14586685489551951885U, (uint64_t)895326705426031212U, (uint64_t)14398171728560617847U,
+        (uint64_t)9592550823745097391U, (uint64_t)17240998489162206026U, (uint64_t)8085479283308189196U,
+        (uint64_t)14844657737893882826U, (uint64_t)15923425394150618234U,
+        (uint64_t)2997808084773249525U, (uint64_t)494323555453660587U, (uint64_t)1215695327517794764U,
+        (uint64_t)9476207381098391690U, (uint64_t)7480789678419122995U, (uint64_t)15212230329321082489U,
+        (uint64_t)436189395349576388U, (uint64_t)17377474396456660834U, (uint64_t)15237013929655017939U,
+        (uint64_t)11444428846883781676U, (uint64_t)5112749694521428575U, (uint64_t)950829367509872073U,
+        (uint64_t)17665036182057559519U, (uint64_t)17205133339690002313U,
+        (uint64_t)16233765170251334549U, (uint64_t)10122775683257972591U,
+        (uint64_t)3352514236455632420U, (uint64_t)9143148522359954691U, (uint64_t)601191684005658860U,
+        (uint64_t)13398772186646349998U, (uint64_t)15512696600132928431U,
+        (uint64_t)9128416073728948653U, (uint64_t)11233051033546138578U, (uint64_t)6769345682610122833U,
+        (uint64_t)10823233224575054288U, (uint64_t)9997725227559980175U, (uint64_t)6733425642852897415U,
+        (uint64_t)16302206918151466066U, (uint64_t)1669330822143265921U, (uint64_t)2661645605036546002U,
+        (uint64_t)17182558479745802165U, (uint64_t)1165082692376932040U, (uint64_t)9470595929011488359U,
+        (uint64_t)6142147329285324932U, (uint64_t)4829075085998111287U, (uint64_t)10231370681107338930U,
+        (uint64_t)9591876895322495239U, (uint64_t)10316468561384076618U,
+        (uint64_t)11592503647238064235U, (uint64_t)13395813606055179632U, (uint64_t)511127033980815508U,
+        (uint64_t)12434976573147649880U, (uint64_t)3425094795384359127U, (uint64_t)6816971736303023445U,
+        (uint64_t)15444670609021139344U, (uint64_t)9464349818322082360U,
+        (uint64_t)16178216413042376883U, (uint64_t)9595540370774317348U, (uint64_t)7229365182662875710U,
+        (uint64_t)4601177649460012843U, (uint64_t)5455046447382487090U, (uint64_t)10854066421606187521U,
+        (uint64_t)15913416821879788071U, (uint64_t)2297365362023460173U, (uint64_t)2603252216454941350U,
+        (uint64_t)6768791943870490934U, (uint64_t)15705936687122754810U, (uint64_t)9537096567546600694U,
+        (uint64_t)17580538144855035062U, (uint64_t)4496542856965746638U, (uint64_t)8444341625922124942U,
+        (uint64_t)12191263903636183168U, (uint64_t)17427332907535974165U,
+        (uint64_t)14307569739254103736U, (uint64_t)13900598742063266169U,
+        (uint64_t)7176996424355977650U, (uint64_t)5709008170379717479U, (uint64_t)14471312052264549092U,
+        (uint64_t)1464519909491759867U, (uint64_t)3328154641049602121U, (uint64_t)13020349337171136774U,
+        (uint64_t)2772166279972051938U, (uint64_t)10854476939425975292U, (uint64_t)1967189930534630940U,
+        (uint64_t)2802919076529341959U, (uint64_t)14792226094833519208U,
+        (uint64_t)14675640928566522177U, (uint64_t)14838974364643800837U,
+        (uint64_t)17631460696099549980U, (uint64_t)17434186275364935469U,
+        (uint64_t)2665648200587705473U, (uint64_t)13202122464492564051U, (uint64_t)7576287350918073341U,
+        (uint64_t)2272206013910186424U, (uint64_t)14558761641743937843U, (uint64_t)5675729149929979729U,
+        (uint64_t)9043135187561613166U, (uint64_t)11750149293830589225U, (uint64_t)740555197954307911U,
+        (uint64_t)9871738005087190699U, (uint64_t)17178667634283502053U,
+        (uint64_t)18046255991533013265U, (uint64_t)4458222096988430430U, (uint64_t)8452427758526311627U,
+        (uint64_t)13825286929656615266U, (uint64_t)13956286357198391218U,
+        (uint64_t)15875692916799995079U, (uint64_t)10634895319157013920U,
+        (uint64_t)13230116118036304207U, (uint64_t)8795317393614625606U, (uint64_t)7001710806858862020U,
+        (uint64_t)7949746088586183478U, (uint64_t)14677556044923602317U,
+        (uint64_t)11184023437485843904U, (uint64_t)11215864722023085094U,
+        (uint64_t)6444464081471519014U, (uint64_t)1706241174022415217U, (uint64_t)8243975633057550613U,
+        (uint64_t)15502902453836085864U, (uint64_t)3799182188594003953U, (uint64_t)3538840175098724094U
+    };
+
+static const uint64_t
+    Hacl_P256_PrecompTable_precomp_g_pow2_64_table_w4[192U] = {
+        (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)1U,
+        (uint64_t)18446744069414584320U, (uint64_t)18446744073709551615U, (uint64_t)4294967294U,
+        (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)1499621593102562565U,
+        (uint64_t)16692369783039433128U, (uint64_t)15337520135922861848U,
+        (uint64_t)5455737214495366228U, (uint64_t)17827017231032529600U,
+        (uint64_t)12413621606240782649U, (uint64_t)2290483008028286132U,
+        (uint64_t)15752017553340844820U, (uint64_t)4846430910634234874U,
+        (uint64_t)10861682798464583253U, (uint64_t)15404737222404363049U, (uint64_t)363586619281562022U,
+        (uint64_t)9866710912401645115U, (uint64_t)1162548847543228595U, (uint64_t)7649967190445130486U,
+        (uint64_t)5212340432230915749U, (uint64_t)7572620550182916491U, (uint64_t)14876145112448665096U,
+        (uint64_t)2063227348838176167U, (uint64_t)3519435548295415847U, (uint64_t)8390400282019023103U,
+        (uint64_t)17666843593163037841U, (uint64_t)9450204148816496323U, (uint64_t)8483374507652916768U,
+        (uint64_t)6254661047265818424U, (uint64_t)16382127809582285023U, (uint64_t)125359443771153172U,
+        (uint64_t)1374336701588437897U, (uint64_t)11362596098420127726U, (uint64_t)2101654420738681387U,
+        (uint64_t)12772780342444840510U, (uint64_t)12546934328908550060U,
+        (uint64_t)8331880412333790397U, (uint64_t)11687262051473819904U, (uint64_t)8926848496503457587U,
+        (uint64_t)9603974142010467857U, (uint64_t)13199952163826973175U, (uint64_t)2189856264898797734U,
+        (uint64_t)11356074861870267226U, (uint64_t)2027714896422561895U, (uint64_t)5261606367808050149U,
+        (uint64_t)153855954337762312U, (uint64_t)6375919692894573986U, (uint64_t)12364041207536146533U,
+        (uint64_t)1891896010455057160U, (uint64_t)1568123795087313171U, (uint64_t)18138710056556660101U,
+        (uint64_t)6004886947510047736U, (uint64_t)4811859325589542932U, (uint64_t)3618763430148954981U,
+        (uint64_t)11434521746258554122U, (uint64_t)10086341535864049427U,
+        (uint64_t)8073421629570399570U, (uint64_t)12680586148814729338U, (uint64_t)9619958020761569612U,
+        (uint64_t)15827203580658384478U, (uint64_t)12832694810937550406U,
+        (uint64_t)14977975484447400910U, (uint64_t)5478002389061063653U,
+        (uint64_t)14731136312639060880U, (uint64_t)4317867687275472033U, (uint64_t)6642650962855259884U,
+        (uint64_t)2514254944289495285U, (uint64_t)14231405641534478436U, (uint64_t)4045448346091518946U,
+        (uint64_t)8985477013445972471U, (uint64_t)8869039454457032149U, (uint64_t)4356978486208692970U,
+        (uint64_t)10805288613335538577U, (uint64_t)12832353127812502042U,
+        (uint64_t)4576590051676547490U, (uint64_t)6728053735138655107U, (uint64_t)17814206719173206184U,
+        (uint64_t)79790138573994940U, (uint64_t)17920293215101822267U, (uint64_t)13422026625585728864U,
+        (uint64_t)5018058010492547271U, (uint64_t)110232326023384102U, (uint64_t)10834264070056942976U,
+        (uint64_t)15222249086119088588U, (uint64_t)15119439519142044997U,
+        (uint64_t)11655511970063167313U, (uint64_t)1614477029450566107U, (uint64_t)3619322817271059794U,
+        (uint64_t)9352862040415412867U, (uint64_t)14017522553242747074U,
+        (uint64_t)13138513643674040327U, (uint64_t)3610195242889455765U, (uint64_t)8371069193996567291U,
+        (uint64_t)12670227996544662654U, (uint64_t)1205961025092146303U,
+        (uint64_t)13106709934003962112U, (uint64_t)4350113471327723407U,
+        (uint64_t)15060941403739680459U, (uint64_t)13639127647823205030U,
+        (uint64_t)10790943339357725715U, (uint64_t)498760574280648264U, (uint64_t)17922071907832082887U,
+        (uint64_t)15122670976670152145U, (uint64_t)6275027991110214322U, (uint64_t)7250912847491816402U,
+        (uint64_t)15206617260142982380U, (uint64_t)3385668313694152877U,
+        (uint64_t)17522479771766801905U, (uint64_t)2965919117476170655U, (uint64_t)1553238516603269404U,
+        (uint64_t)5820770015631050991U, (uint64_t)4999445222232605348U, (uint64_t)9245650860833717444U,
+        (uint64_t)1508811811724230728U, (uint64_t)5190684913765614385U, (uint64_t)15692927070934536166U,
+        (uint64_t)12981978499190500902U, (uint64_t)5143491963193394698U, (uint64_t)7705698092144084129U,
+        (uint64_t)581120653055084783U, (uint64_t)13886552864486459714U, (uint64_t)6290301270652587255U,
+        (uint64_t)8663431529954393128U, (uint64_t)17033405846475472443U, (uint64_t)5206780355442651635U,
+        (uint64_t)12580364474736467688U, (uint64_t)17934601912005283310U,
+        (uint64_t)15119491731028933652U, (uint64_t)17848231399859044858U,
+        (uint64_t)4427673319524919329U, (uint64_t)2673607337074368008U, (uint64_t)14034876464294699949U,
+        (uint64_t)10938948975420813697U, (uint64_t)15202340615298669183U,
+        (uint64_t)5496603454069431071U, (uint64_t)2486526142064906845U, (uint64_t)4507882119510526802U,
+        (uint64_t)13888151172411390059U, (uint64_t)15049027856908071726U,
+        (uint64_t)9667231543181973158U, (uint64_t)6406671575277563202U, (uint64_t)3395801050331215139U,
+        (uint64_t)9813607433539108308U, (uint64_t)2681417728820980381U, (uint64_t)18407064643927113994U,
+        (uint64_t)7707177692113485527U, (uint64_t)14218149384635317074U, (uint64_t)3658668346206375919U,
+        (uint64_t)15404713991002362166U, (uint64_t)10152074687696195207U,
+        (uint64_t)10926946599582128139U, (uint64_t)16907298600007085320U,
+        (uint64_t)16544287219664720279U, (uint64_t)11007075933432813205U,
+        (uint64_t)8652245965145713599U, (uint64_t)7857626748965990384U, (uint64_t)5602306604520095870U,
+        (uint64_t)2525139243938658618U, (uint64_t)14405696176872077447U,
+        (uint64_t)18432270482137885332U, (uint64_t)9913880809120071177U,
+        (uint64_t)16896141737831216972U, (uint64_t)7484791498211214829U,
+        (uint64_t)15635259968266497469U, (uint64_t)8495118537612215624U, (uint64_t)4915477980562575356U,
+        (uint64_t)16453519279754924350U, (uint64_t)14462108244565406969U,
+        (uint64_t)14837837755237096687U, (uint64_t)14130171078892575346U,
+        (uint64_t)15423793222528491497U, (uint64_t)5460399262075036084U,
+        (uint64_t)16085440580308415349U, (uint64_t)26873200736954488U, (uint64_t)5603655807457499550U,
+        (uint64_t)3342202915871129617U, (uint64_t)1604413932150236626U, (uint64_t)9684226585089458974U,
+        (uint64_t)1213229904006618539U, (uint64_t)6782978662408837236U, (uint64_t)11197029877749307372U,
+        (uint64_t)14085968786551657744U, (uint64_t)17352273610494009342U,
+        (uint64_t)7876582961192434984U
+    };
+
+static const uint64_t
+    Hacl_P256_PrecompTable_precomp_g_pow2_128_table_w4[192U] = {
+        (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)1U,
+        (uint64_t)18446744069414584320U, (uint64_t)18446744073709551615U, (uint64_t)4294967294U,
+        (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)14619254753077084366U,
+        (uint64_t)13913835116514008593U, (uint64_t)15060744674088488145U,
+        (uint64_t)17668414598203068685U, (uint64_t)10761169236902342334U,
+        (uint64_t)15467027479157446221U, (uint64_t)14989185522423469618U,
+        (uint64_t)14354539272510107003U, (uint64_t)14298211796392133693U,
+        (uint64_t)13270323784253711450U, (uint64_t)13380964971965046957U,
+        (uint64_t)8686204248456909699U, (uint64_t)17434630286744937066U, (uint64_t)1355903775279084720U,
+        (uint64_t)7554695053550308662U, (uint64_t)11354971222741863570U, (uint64_t)564601613420749879U,
+        (uint64_t)8466325837259054896U, (uint64_t)10752965181772434263U,
+        (uint64_t)11405876547368426319U, (uint64_t)13791894568738930940U,
+        (uint64_t)8230587134406354675U, (uint64_t)12415514098722758608U,
+        (uint64_t)18414183046995786744U, (uint64_t)15508000368227372870U,
+        (uint64_t)5781062464627999307U, (uint64_t)15339429052219195590U,
+        (uint64_t)16038703753810741903U, (uint64_t)9587718938298980714U, (uint64_t)4822658817952386407U,
+        (uint64_t)1376351024833260660U, (uint64_t)1120174910554766702U, (uint64_t)1730170933262569274U,
+        (uint64_t)5187428548444533500U, (uint64_t)16242053503368957131U, (uint64_t)3036811119519868279U,
+        (uint64_t)1760267587958926638U, (uint64_t)170244572981065185U, (uint64_t)8063080791967388171U,
+        (uint64_t)4824892826607692737U, (uint64_t)16286391083472040552U,
+        (uint64_t)11945158615253358747U, (uint64_t)14096887760410224200U,
+        (uint64_t)1613720831904557039U, (uint64_t)14316966673761197523U,
+        (uint64_t)17411006201485445341U, (uint64_t)8112301506943158801U, (uint64_t)2069889233927989984U,
+        (uint64_t)10082848378277483927U, (uint64_t)3609691194454404430U, (uint64_t)6110437205371933689U,
+        (uint64_t)9769135977342231601U, (uint64_t)11977962151783386478U,
+        (uint64_t)18088718692559983573U, (uint64_t)11741637975753055U, (uint64_t)11110390325701582190U,
+        (uint64_t)1341402251566067019U, (uint64_t)3028229550849726478U, (uint64_t)10438984083997451310U,
+        (uint64_t)12730851885100145709U, (uint64_t)11524169532089894189U,
+        (uint64_t)4523375903229602674U, (uint64_t)2028602258037385622U, (uint64_t)17082839063089388410U,
+        (uint64_t)6103921364634113167U, (uint64_t)17066180888225306102U,
+        (uint64_t)11395680486707876195U, (uint64_t)10952892272443345484U,
+        (uint64_t)8792831960605859401U, (uint64_t)14194485427742325139U,
+        (uint64_t)15146020821144305250U, (uint64_t)1654766014957123343U, (uint64_t)7955526243090948551U,
+        (uint64_t)3989277566080493308U, (uint64_t)12229385116397931231U,
+        (uint64_t)13430548930727025562U, (uint64_t)3434892688179800602U, (uint64_t)8431998794645622027U,
+        (uint64_t)12132530981596299272U, (uint64_t)2289461608863966999U,
+        (uint64_t)18345870950201487179U, (uint64_t)13517947207801901576U,
+        (uint64_t)5213113244172561159U, (uint64_t)17632986594098340879U, (uint64_t)4405251818133148856U,
+        (uint64_t)11783009269435447793U, (uint64_t)9332138983770046035U,
+        (uint64_t)12863411548922539505U, (uint64_t)3717030292816178224U,
+        (uint64_t)10026078446427137374U, (uint64_t)11167295326594317220U,
+        (uint64_t)12425328773141588668U, (uint64_t)5760335125172049352U, (uint64_t)9016843701117277863U,
+        (uint64_t)5657892835694680172U, (uint64_t)11025130589305387464U, (uint64_t)1368484957977406173U,
+        (uint64_t)17361351345281258834U, (uint64_t)1907113641956152700U,
+        (uint64_t)16439233413531427752U, (uint64_t)5893322296986588932U,
+        (uint64_t)14000206906171746627U, (uint64_t)14979266987545792900U,
+        (uint64_t)6926291766898221120U, (uint64_t)7162023296083360752U, (uint64_t)14762747553625382529U,
+        (uint64_t)12610831658612406849U, (uint64_t)10462926899548715515U,
+        (uint64_t)4794017723140405312U, (uint64_t)5234438200490163319U, (uint64_t)8019519110339576320U,
+        (uint64_t)7194604241290530100U, (uint64_t)12626770134810813246U,
+        (uint64_t)10793074474236419890U, (uint64_t)11323224347913978783U,
+        (uint64_t)16831128015895380245U, (uint64_t)18323094195124693378U,
+        (uint64_t)2361097165281567692U, (uint64_t)15755578675014279498U,
+        (uint64_t)14289876470325854580U, (uint64_t)12856787656093616839U,
+        (uint64_t)3578928531243900594U, (uint64_t)3847532758790503699U, (uint64_t)8377953190224748743U,
+        (uint64_t)3314546646092744596U, (uint64_t)800810188859334358U, (uint64_t)4626344124229343596U,
+        (uint64_t)6620381605850876621U, (uint64_t)11422073570955989527U,
+        (uint64_t)12676813626484814469U, (uint64_t)16725029886764122240U,
+        (uint64_t)16648497372773830008U, (uint64_t)9135702594931291048U,
+        (uint64_t)16080949688826680333U, (uint64_t)11528096561346602947U,
+        (uint64_t)2632498067099740984U, (uint64_t)11583842699108800714U, (uint64_t)8378404864573610526U,
+        (uint64_t)1076560261627788534U, (uint64_t)13836015994325032828U,
+        (uint64_t)11234295937817067909U, (uint64_t)5893659808396722708U,
+        (uint64_t)11277421142886984364U, (uint64_t)8968549037166726491U,
+        (uint64_t)14841374331394032822U, (uint64_t)9967344773947889341U, (uint64_t)8799244393578496085U,
+        (uint64_t)5094686877301601410U, (uint64_t)8780316747074726862U, (uint64_t)9119697306829835718U,
+        (uint64_t)15381243327921855368U, (uint64_t)2686250164449435196U,
+        (uint64_t)16466917280442198358U, (uint64_t)13791704489163125216U,
+        (uint64_t)16955859337117924272U, (uint64_t)17112836394923783642U,
+        (uint64_t)4639176427338618063U, (uint64_t)16770029310141094964U,
+        (uint64_t)11049953922966416185U, (uint64_t)12012669590884098968U,
+        (uint64_t)4859326885929417214U, (uint64_t)896380084392586061U, (uint64_t)7153028362977034008U,
+        (uint64_t)10540021163316263301U, (uint64_t)9318277998512936585U,
+        (uint64_t)18344496977694796523U, (uint64_t)11374737400567645494U,
+        (uint64_t)17158800051138212954U, (uint64_t)18343197867863253153U,
+        (uint64_t)18204799297967861226U, (uint64_t)15798973531606348828U,
+        (uint64_t)9870158263408310459U, (uint64_t)17578869832774612627U, (uint64_t)8395748875822696932U,
+        (uint64_t)15310679007370670872U, (uint64_t)11205576736030808860U,
+        (uint64_t)10123429210002838967U, (uint64_t)5910544144088393959U,
+        (uint64_t)14016615653353687369U, (uint64_t)11191676704772957822U
+    };
+
+static const uint64_t
+    Hacl_P256_PrecompTable_precomp_g_pow2_192_table_w4[192U] = {
+        (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)1U,
+        (uint64_t)18446744069414584320U, (uint64_t)18446744073709551615U, (uint64_t)4294967294U,
+        (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)7870395003430845958U,
+        (uint64_t)18001862936410067720U, (uint64_t)8006461232116967215U, (uint64_t)5921313779532424762U,
+        (uint64_t)10702113371959864307U, (uint64_t)8070517410642379879U, (uint64_t)7139806720777708306U,
+        (uint64_t)8253938546650739833U, (uint64_t)17490482834545705718U, (uint64_t)1065249776797037500U,
+        (uint64_t)5018258455937968775U, (uint64_t)14100621120178668337U, (uint64_t)8392845221328116213U,
+        (uint64_t)14630296398338540788U, (uint64_t)4268947906723414372U, (uint64_t)9231207002243517909U,
+        (uint64_t)14261219637616504262U, (uint64_t)7786881626982345356U,
+        (uint64_t)11412720751765882139U, (uint64_t)14119585051365330009U,
+        (uint64_t)15281626286521302128U, (uint64_t)6350171933454266732U,
+        (uint64_t)16559468304937127866U, (uint64_t)13200760478271693417U,
+        (uint64_t)6733381546280350776U, (uint64_t)3801404890075189193U, (uint64_t)2741036364686993903U,
+        (uint64_t)3218612940540174008U, (uint64_t)10894914335165419505U,
+        (uint64_t)11862941430149998362U, (uint64_t)4223151729402839584U, (uint64_t)2913215088487087887U,
+        (uint64_t)14562168920104952953U, (uint64_t)2170089393468287453U,
+        (uint64_t)10520900655016579352U, (uint64_t)7040362608949989273U, (uint64_t)8376510559381705307U,
+        (uint64_t)9142237200448131532U, (uint64_t)5696859948123854080U, (uint64_t)925422306716081180U,
+        (uint64_t)11155545953469186421U, (uint64_t)1888208646862572812U,
+        (uint64_t)11151095998248845721U, (uint64_t)15793503271680275267U,
+        (uint64_t)7729877044494854851U, (uint64_t)6235134673193032913U, (uint64_t)7364280682182401564U,
+        (uint64_t)5479679373325519985U, (uint64_t)17966037684582301763U,
+        (uint64_t)14140891609330279185U, (uint64_t)5814744449740463867U, (uint64_t)5652588426712591652U,
+        (uint64_t)774745682988690912U, (uint64_t)13228255573220500373U, (uint64_t)11949122068786859397U,
+        (uint64_t)8021166392900770376U, (uint64_t)7994323710948720063U, (uint64_t)9924618472877849977U,
+        (uint64_t)17618517523141194266U, (uint64_t)2750424097794401714U,
+        (uint64_t)15481749570715253207U, (uint64_t)14646964509921760497U,
+        (uint64_t)1037442848094301355U, (uint64_t)6295995947389299132U, (uint64_t)16915049722317579514U,
+        (uint64_t)10493877400992990313U, (uint64_t)18391008753060553521U, (uint64_t)483942209623707598U,
+        (uint64_t)2017775662838016613U, (uint64_t)5933251998459363553U, (uint64_t)11789135019970707407U,
+        (uint64_t)5484123723153268336U, (uint64_t)13246954648848484954U, (uint64_t)4774374393926023505U,
+        (uint64_t)14863995618704457336U, (uint64_t)13220153167104973625U,
+        (uint64_t)5988445485312390826U, (uint64_t)17580359464028944682U, (uint64_t)7297100131969874771U,
+        (uint64_t)379931507867989375U, (uint64_t)10927113096513421444U, (uint64_t)17688881974428340857U,
+        (uint64_t)4259872578781463333U, (uint64_t)8573076295966784472U, (uint64_t)16389829450727275032U,
+        (uint64_t)1667243868963568259U, (uint64_t)17730726848925960919U,
+        (uint64_t)11408899874569778008U, (uint64_t)3576527582023272268U,
+        (uint64_t)16492920640224231656U, (uint64_t)7906130545972460130U,
+        (uint64_t)13878604278207681266U, (uint64_t)41446695125652041U, (uint64_t)8891615271337333503U,
+        (uint64_t)2594537723613594470U, (uint64_t)7699579176995770924U, (uint64_t)147458463055730655U,
+        (uint64_t)12120406862739088406U, (uint64_t)12044892493010567063U,
+        (uint64_t)8554076749615475136U, (uint64_t)1005097692260929999U, (uint64_t)2687202654471188715U,
+        (uint64_t)9457588752176879209U, (uint64_t)17472884880062444019U, (uint64_t)9792097892056020166U,
+        (uint64_t)2525246678512797150U, (uint64_t)15958903035313115662U,
+        (uint64_t)11336038170342247032U, (uint64_t)11560342382835141123U,
+        (uint64_t)6212009033479929024U, (uint64_t)8214308203775021229U, (uint64_t)8475469210070503698U,
+        (uint64_t)13287024123485719563U, (uint64_t)12956951963817520723U,
+        (uint64_t)10693035819908470465U, (uint64_t)11375478788224786725U,
+        (uint64_t)16934625208487120398U, (uint64_t)10094585729115874495U,
+        (uint64_t)2763884524395905776U, (uint64_t)13535890148969964883U,
+        (uint64_t)13514657411765064358U, (uint64_t)9903074440788027562U,
+        (uint64_t)17324720726421199990U, (uint64_t)2273931039117368789U, (uint64_t)3442641041506157854U,
+        (uint64_t)1119853641236409612U, (uint64_t)12037070344296077989U, (uint64_t)581736433335671746U,
+        (uint64_t)6019150647054369174U, (uint64_t)14864096138068789375U, (uint64_t)6652995210998318662U,
+        (uint64_t)12773883697029175304U, (uint64_t)12751275631451845119U,
+        (uint64_t)11449095003038250478U, (uint64_t)1025805267334366480U, (uint64_t)2764432500300815015U,
+        (uint64_t)18274564429002844381U, (uint64_t)10445634195592600351U,
+        (uint64_t)11814099592837202735U, (uint64_t)5006796893679120289U, (uint64_t)6908397253997261914U,
+        (uint64_t)13266696965302879279U, (uint64_t)7768715053015037430U, (uint64_t)3569923738654785686U,
+        (uint64_t)5844853453464857549U, (uint64_t)1837340805629559110U, (uint64_t)1034657624388283114U,
+        (uint64_t)711244516069456460U, (uint64_t)12519286026957934814U, (uint64_t)2613464944620837619U,
+        (uint64_t)10003023321338286213U, (uint64_t)7291332092642881376U, (uint64_t)9832199564117004897U,
+        (uint64_t)3280736694860799890U, (uint64_t)6416452202849179874U, (uint64_t)7326961381798642069U,
+        (uint64_t)8435688798040635029U, (uint64_t)16630141263910982958U,
+        (uint64_t)17222635514422533318U, (uint64_t)9482787389178881499U, (uint64_t)836561194658263905U,
+        (uint64_t)3405319043337616649U, (uint64_t)2786146577568026518U, (uint64_t)7625483685691626321U,
+        (uint64_t)6728084875304656716U, (uint64_t)1140997959232544268U, (uint64_t)12847384827606303792U,
+        (uint64_t)1719121337754572070U, (uint64_t)12863589482936438532U, (uint64_t)3880712899640530862U,
+        (uint64_t)2748456882813671564U, (uint64_t)4775988900044623019U, (uint64_t)8937847374382191162U,
+        (uint64_t)3767367347172252295U, (uint64_t)13468672401049388646U,
+        (uint64_t)14359032216842397576U, (uint64_t)2002555958685443975U,
+        (uint64_t)16488678606651526810U, (uint64_t)11826135409597474760U,
+        (uint64_t)15296495673182508601U
+    };
+
+static const uint64_t
+    Hacl_P256_PrecompTable_precomp_basepoint_table_w5[384U] = {
+        (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)1U,
+        (uint64_t)18446744069414584320U, (uint64_t)18446744073709551615U, (uint64_t)4294967294U,
+        (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)8784043285714375740U,
+        (uint64_t)8483257759279461889U, (uint64_t)8789745728267363600U, (uint64_t)1770019616739251654U,
+        (uint64_t)15992936863339206154U, (uint64_t)10037038012062884956U,
+        (uint64_t)15197544864945402661U, (uint64_t)9615747158586711429U, (uint64_t)1U,
+        (uint64_t)18446744069414584320U, (uint64_t)18446744073709551615U, (uint64_t)4294967294U,
+        (uint64_t)10634854829044225757U, (uint64_t)351552716085025155U, (uint64_t)10645315080955407736U,
+        (uint64_t)3609262091244858135U, (uint64_t)15760741698986874125U,
+        (uint64_t)14936374388219697827U, (uint64_t)15751360096993017895U,
+        (uint64_t)18012233706239762398U, (uint64_t)1993877568177495041U,
+        (uint64_t)10345888787846536528U, (uint64_t)7746511691117935375U,
+        (uint64_t)14517043990409914413U, (uint64_t)14122549297570634151U,
+        (uint64_t)16934610359517083771U, (uint64_t)5724511325497097418U, (uint64_t)8983432969107448705U,
+        (uint64_t)2687429970334080245U, (uint64_t)16525396802810050288U, (uint64_t)7602596488871585854U,
+        (uint64_t)4813919589149203084U, (uint64_t)7680395813780804519U, (uint64_t)6687709583048023590U,
+        (uint64_t)18086445169104142027U, (uint64_t)9637814708330203929U,
+        (uint64_t)14785108459960679090U, (uint64_t)3838023279095023581U, (uint64_t)3555615526157830307U,
+        (uint64_t)5177066488380472871U, (uint64_t)18218186719108038403U,
+        (uint64_t)16281556341699656105U, (uint64_t)1524227924561461191U, (uint64_t)4148060517641909597U,
+        (uint64_t)2858290374115363433U, (uint64_t)8942772026334130620U, (uint64_t)3034451298319885113U,
+        (uint64_t)8447866036736640940U, (uint64_t)11204933433076256578U,
+        (uint64_t)18333595740249588297U, (uint64_t)8259597024804538246U, (uint64_t)9539734295777539786U,
+        (uint64_t)9797290423046626413U, (uint64_t)5777303437849646537U, (uint64_t)8739356909899132020U,
+        (uint64_t)14815960973766782158U, (uint64_t)15286581798204509801U,
+        (uint64_t)17597362577777019682U, (uint64_t)13259283710820519742U,
+        (uint64_t)10501322996899164670U, (uint64_t)1221138904338319642U,
+        (uint64_t)14586685489551951885U, (uint64_t)895326705426031212U, (uint64_t)14398171728560617847U,
+        (uint64_t)9592550823745097391U, (uint64_t)17240998489162206026U, (uint64_t)8085479283308189196U,
+        (uint64_t)14844657737893882826U, (uint64_t)15923425394150618234U,
+        (uint64_t)2997808084773249525U, (uint64_t)494323555453660587U, (uint64_t)1215695327517794764U,
+        (uint64_t)9476207381098391690U, (uint64_t)7480789678419122995U, (uint64_t)15212230329321082489U,
+        (uint64_t)436189395349576388U, (uint64_t)17377474396456660834U, (uint64_t)15237013929655017939U,
+        (uint64_t)11444428846883781676U, (uint64_t)5112749694521428575U, (uint64_t)950829367509872073U,
+        (uint64_t)17665036182057559519U, (uint64_t)17205133339690002313U,
+        (uint64_t)16233765170251334549U, (uint64_t)10122775683257972591U,
+        (uint64_t)3352514236455632420U, (uint64_t)9143148522359954691U, (uint64_t)601191684005658860U,
+        (uint64_t)13398772186646349998U, (uint64_t)15512696600132928431U,
+        (uint64_t)9128416073728948653U, (uint64_t)11233051033546138578U, (uint64_t)6769345682610122833U,
+        (uint64_t)10823233224575054288U, (uint64_t)9997725227559980175U, (uint64_t)6733425642852897415U,
+        (uint64_t)16302206918151466066U, (uint64_t)1669330822143265921U, (uint64_t)2661645605036546002U,
+        (uint64_t)17182558479745802165U, (uint64_t)1165082692376932040U, (uint64_t)9470595929011488359U,
+        (uint64_t)6142147329285324932U, (uint64_t)4829075085998111287U, (uint64_t)10231370681107338930U,
+        (uint64_t)9591876895322495239U, (uint64_t)10316468561384076618U,
+        (uint64_t)11592503647238064235U, (uint64_t)13395813606055179632U, (uint64_t)511127033980815508U,
+        (uint64_t)12434976573147649880U, (uint64_t)3425094795384359127U, (uint64_t)6816971736303023445U,
+        (uint64_t)15444670609021139344U, (uint64_t)9464349818322082360U,
+        (uint64_t)16178216413042376883U, (uint64_t)9595540370774317348U, (uint64_t)7229365182662875710U,
+        (uint64_t)4601177649460012843U, (uint64_t)5455046447382487090U, (uint64_t)10854066421606187521U,
+        (uint64_t)15913416821879788071U, (uint64_t)2297365362023460173U, (uint64_t)2603252216454941350U,
+        (uint64_t)6768791943870490934U, (uint64_t)15705936687122754810U, (uint64_t)9537096567546600694U,
+        (uint64_t)17580538144855035062U, (uint64_t)4496542856965746638U, (uint64_t)8444341625922124942U,
+        (uint64_t)12191263903636183168U, (uint64_t)17427332907535974165U,
+        (uint64_t)14307569739254103736U, (uint64_t)13900598742063266169U,
+        (uint64_t)7176996424355977650U, (uint64_t)5709008170379717479U, (uint64_t)14471312052264549092U,
+        (uint64_t)1464519909491759867U, (uint64_t)3328154641049602121U, (uint64_t)13020349337171136774U,
+        (uint64_t)2772166279972051938U, (uint64_t)10854476939425975292U, (uint64_t)1967189930534630940U,
+        (uint64_t)2802919076529341959U, (uint64_t)14792226094833519208U,
+        (uint64_t)14675640928566522177U, (uint64_t)14838974364643800837U,
+        (uint64_t)17631460696099549980U, (uint64_t)17434186275364935469U,
+        (uint64_t)2665648200587705473U, (uint64_t)13202122464492564051U, (uint64_t)7576287350918073341U,
+        (uint64_t)2272206013910186424U, (uint64_t)14558761641743937843U, (uint64_t)5675729149929979729U,
+        (uint64_t)9043135187561613166U, (uint64_t)11750149293830589225U, (uint64_t)740555197954307911U,
+        (uint64_t)9871738005087190699U, (uint64_t)17178667634283502053U,
+        (uint64_t)18046255991533013265U, (uint64_t)4458222096988430430U, (uint64_t)8452427758526311627U,
+        (uint64_t)13825286929656615266U, (uint64_t)13956286357198391218U,
+        (uint64_t)15875692916799995079U, (uint64_t)10634895319157013920U,
+        (uint64_t)13230116118036304207U, (uint64_t)8795317393614625606U, (uint64_t)7001710806858862020U,
+        (uint64_t)7949746088586183478U, (uint64_t)14677556044923602317U,
+        (uint64_t)11184023437485843904U, (uint64_t)11215864722023085094U,
+        (uint64_t)6444464081471519014U, (uint64_t)1706241174022415217U, (uint64_t)8243975633057550613U,
+        (uint64_t)15502902453836085864U, (uint64_t)3799182188594003953U, (uint64_t)3538840175098724094U,
+        (uint64_t)13240193491554624643U, (uint64_t)12365034249541329920U,
+        (uint64_t)2924326828590977357U, (uint64_t)5687195797140589099U, (uint64_t)16880427227292834531U,
+        (uint64_t)9691471435758991112U, (uint64_t)16642385273732487288U,
+        (uint64_t)12173806747523009914U, (uint64_t)13142722756877876849U,
+        (uint64_t)8370377548305121979U, (uint64_t)17988526053752025426U, (uint64_t)4818750752684100334U,
+        (uint64_t)5669241919350361655U, (uint64_t)4964810303238518540U, (uint64_t)16709712747671533191U,
+        (uint64_t)4461414404267448242U, (uint64_t)3971798785139504238U, (uint64_t)6276818948740422136U,
+        (uint64_t)1426735892164275762U, (uint64_t)7943622674892418919U, (uint64_t)9864274225563929680U,
+        (uint64_t)57815533745003233U, (uint64_t)10893588105168960233U, (uint64_t)15739162732907069535U,
+        (uint64_t)3923866849462073470U, (uint64_t)12279826158399226875U, (uint64_t)1533015761334846582U,
+        (uint64_t)15860156818568437510U, (uint64_t)8252625373831297988U, (uint64_t)9666953804812706358U,
+        (uint64_t)8767785238646914634U, (uint64_t)14382179044941403551U,
+        (uint64_t)10401039907264254245U, (uint64_t)8584860003763157350U, (uint64_t)3120462679504470266U,
+        (uint64_t)8670255778748340069U, (uint64_t)5313789577940369984U, (uint64_t)16977072364454789224U,
+        (uint64_t)12199578693972188324U, (uint64_t)18211098771672599237U,
+        (uint64_t)12868831556008795030U, (uint64_t)5310155061431048194U,
+        (uint64_t)18114153238435112606U, (uint64_t)14482365809278304512U,
+        (uint64_t)12520721662723001511U, (uint64_t)405943624021143002U, (uint64_t)8146944101507657423U,
+        (uint64_t)181739317780393495U, (uint64_t)81743892273670099U, (uint64_t)14759561962550473930U,
+        (uint64_t)4592623849546992939U, (uint64_t)6916440441743449719U, (uint64_t)1304610503530809833U,
+        (uint64_t)5464930909232486441U, (uint64_t)15414883617496224671U, (uint64_t)8129283345256790U,
+        (uint64_t)18294252198413739489U, (uint64_t)17394115281884857288U,
+        (uint64_t)7808348415224731235U, (uint64_t)13195566655747230608U, (uint64_t)8568194219353949094U,
+        (uint64_t)15329813048672122440U, (uint64_t)9604275495885785744U, (uint64_t)1577712551205219835U,
+        (uint64_t)15964209008022052790U, (uint64_t)15087297920782098160U,
+        (uint64_t)3946031512438511898U, (uint64_t)10050061168984440631U,
+        (uint64_t)11382452014533138316U, (uint64_t)6313670788911952792U,
+        (uint64_t)12015989229696164014U, (uint64_t)5946702628076168852U, (uint64_t)5219995658774362841U,
+        (uint64_t)12230141881068377972U, (uint64_t)12361195202673441956U,
+        (uint64_t)4732862275653856711U, (uint64_t)17221430380805252370U,
+        (uint64_t)15397525953897375810U, (uint64_t)16557437297239563045U,
+        (uint64_t)10101683801868971351U, (uint64_t)1402611372245592868U, (uint64_t)1931806383735563658U,
+        (uint64_t)10991705207471512479U, (uint64_t)861333583207471392U, (uint64_t)15207766844626322355U,
+        (uint64_t)9224628129811432393U, (uint64_t)3497069567089055613U, (uint64_t)11956632757898590316U,
+        (uint64_t)8733729372586312960U, (uint64_t)18091521051714930927U, (uint64_t)77582787724373283U,
+        (uint64_t)9922437373519669237U, (uint64_t)3079321456325704615U, (uint64_t)12171198408512478457U,
+        (uint64_t)17179130884012147596U, (uint64_t)6839115479620367181U, (uint64_t)4421032569964105406U,
+        (uint64_t)10353331468657256053U, (uint64_t)17400988720335968824U,
+        (uint64_t)17138855889417480540U, (uint64_t)4507980080381370611U,
+        (uint64_t)10703175719793781886U, (uint64_t)12598516658725890426U,
+        (uint64_t)8353463412173898932U, (uint64_t)17703029389228422404U, (uint64_t)9313111267107226233U,
+        (uint64_t)5441322942995154196U, (uint64_t)8952817660034465484U, (uint64_t)17571113341183703118U,
+        (uint64_t)7375087953801067019U, (uint64_t)13381466302076453648U, (uint64_t)3218165271423914596U,
+        (uint64_t)16956372157249382685U, (uint64_t)509080090049418841U, (uint64_t)13374233893294084913U,
+        (uint64_t)2988537624204297086U, (uint64_t)4979195832939384620U, (uint64_t)3803931594068976394U,
+        (uint64_t)10731535883829627646U, (uint64_t)12954845047607194278U,
+        (uint64_t)10494298062560667399U, (uint64_t)4967351022190213065U,
+        (uint64_t)13391917938145756456U, (uint64_t)951370484866918160U, (uint64_t)13531334179067685307U,
+        (uint64_t)12868421357919390599U, (uint64_t)15918857042998130258U,
+        (uint64_t)17769743831936974016U, (uint64_t)7137921979260368809U,
+        (uint64_t)12461369180685892062U, (uint64_t)827476514081935199U, (uint64_t)15107282134224767230U,
+        (uint64_t)10084765752802805748U, (uint64_t)3303739059392464407U,
+        (uint64_t)17859532612136591428U, (uint64_t)10949414770405040164U,
+        (uint64_t)12838613589371008785U, (uint64_t)5554397169231540728U,
+        (uint64_t)18375114572169624408U, (uint64_t)15649286703242390139U,
+        (uint64_t)2957281557463706877U, (uint64_t)14000350446219393213U,
+        (uint64_t)14355199721749620351U, (uint64_t)2730856240099299695U,
+        (uint64_t)17528131000714705752U, (uint64_t)2537498525883536360U, (uint64_t)6121058967084509393U,
+        (uint64_t)16897667060435514221U, (uint64_t)12367869599571112440U,
+        (uint64_t)3388831797050807508U, (uint64_t)16791449724090982798U, (uint64_t)2673426123453294928U,
+        (uint64_t)11369313542384405846U, (uint64_t)15641960333586432634U,
+        (uint64_t)15080962589658958379U, (uint64_t)7747943772340226569U, (uint64_t)8075023376199159152U,
+        (uint64_t)8485093027378306528U, (uint64_t)13503706844122243648U, (uint64_t)8401961362938086226U,
+        (uint64_t)8125426002124226402U, (uint64_t)9005399361407785203U, (uint64_t)6847968030066906634U,
+        (uint64_t)11934937736309295197U, (uint64_t)5116750888594772351U, (uint64_t)2817039227179245227U,
+        (uint64_t)17724206901239332980U, (uint64_t)4985702708254058578U, (uint64_t)5786345435756642871U,
+        (uint64_t)17772527414940936938U, (uint64_t)1201320251272957006U,
+        (uint64_t)15787430120324348129U, (uint64_t)6305488781359965661U,
+        (uint64_t)12423900845502858433U, (uint64_t)17485949424202277720U,
+        (uint64_t)2062237315546855852U, (uint64_t)10353639467860902375U, (uint64_t)2315398490451287299U,
+        (uint64_t)15394572894814882621U, (uint64_t)232866113801165640U, (uint64_t)7413443736109338926U,
+        (uint64_t)902719806551551191U, (uint64_t)16568853118619045174U, (uint64_t)14202214862428279177U,
+        (uint64_t)11719595395278861192U, (uint64_t)5890053236389907647U, (uint64_t)9996196494965833627U,
+        (uint64_t)12967056942364782577U, (uint64_t)9034128755157395787U,
+        (uint64_t)17898204904710512655U, (uint64_t)8229373445062993977U,
+        (uint64_t)13580036169519833644U
+    };
+
+#if defined(__cplusplus)
+}
+#endif
+
+#define __internal_Hacl_P256_PrecompTable_H_DEFINED
+#endif
diff --git a/security/nss/lib/freebl/verified/internal/Hacl_Poly1305_128.h b/security/nss/lib/freebl/verified/internal/Hacl_Poly1305_128.h
new file mode 100644
index 0000000000..ccd18281e4
--- /dev/null
+++ b/security/nss/lib/freebl/verified/internal/Hacl_Poly1305_128.h
@@ -0,0 +1,53 @@
+/* MIT License
+ *
+ * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation
+ * Copyright (c) 2022-2023 HACL* Contributors
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the Software is
+ * furnished to do so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+ * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+ * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+ * SOFTWARE.
+ */
+
+#ifndef __internal_Hacl_Poly1305_128_H
+#define __internal_Hacl_Poly1305_128_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
+#include <string.h>
+#include "krml/internal/types.h"
+#include "krml/lowstar_endianness.h"
+#include "krml/internal/target.h"
+
+#include "../Hacl_Poly1305_128.h"
+#include "libintvector.h"
+
+void
+Hacl_Impl_Poly1305_Field32xN_128_load_acc2(Lib_IntVector_Intrinsics_vec128 *acc, uint8_t *b);
+
+void
+Hacl_Impl_Poly1305_Field32xN_128_fmul_r2_normalize(
+    Lib_IntVector_Intrinsics_vec128 *out,
+    Lib_IntVector_Intrinsics_vec128 *p);
+
+#if defined(__cplusplus)
+}
+#endif
+
+#define __internal_Hacl_Poly1305_128_H_DEFINED
+#endif
diff --git a/security/nss/lib/freebl/verified/internal/Hacl_Poly1305_256.h b/security/nss/lib/freebl/verified/internal/Hacl_Poly1305_256.h
new file mode 100644
index 0000000000..b26f9dd67d
--- /dev/null
+++ b/security/nss/lib/freebl/verified/internal/Hacl_Poly1305_256.h
@@ -0,0 +1,53 @@
+/* MIT License
+ *
+ * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation
+ * Copyright (c) 2022-2023 HACL* Contributors
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the Software is
+ * furnished to do so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+ * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+ * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+ * SOFTWARE.
+ */
+
+#ifndef __internal_Hacl_Poly1305_256_H
+#define __internal_Hacl_Poly1305_256_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
+#include <string.h>
+#include "krml/internal/types.h"
+#include "krml/lowstar_endianness.h"
+#include "krml/internal/target.h"
+
+#include "../Hacl_Poly1305_256.h"
+#include "libintvector.h"
+
+void
+Hacl_Impl_Poly1305_Field32xN_256_load_acc4(Lib_IntVector_Intrinsics_vec256 *acc, uint8_t *b);
+
+void
+Hacl_Impl_Poly1305_Field32xN_256_fmul_r4_normalize(
+    Lib_IntVector_Intrinsics_vec256 *out,
+    Lib_IntVector_Intrinsics_vec256 *p);
+
+#if defined(__cplusplus)
+}
+#endif
+
+#define __internal_Hacl_Poly1305_256_H_DEFINED
+#endif
diff --git a/security/nss/lib/freebl/verified/internal/Hacl_Spec.h b/security/nss/lib/freebl/verified/internal/Hacl_Spec.h
new file mode 100644
index 0000000000..f717563d04
--- /dev/null
+++ b/security/nss/lib/freebl/verified/internal/Hacl_Spec.h
@@ -0,0 +1,55 @@
+/* MIT License
+ *
+ * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation
+ * Copyright (c) 2022-2023 HACL* Contributors
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the Software is
+ * furnished to do so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+ * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+ * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+ * SOFTWARE.
+ */
+
+#ifndef __internal_Hacl_Spec_H
+#define __internal_Hacl_Spec_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
+#include <string.h>
+#include "krml/internal/types.h"
+#include "krml/lowstar_endianness.h"
+#include "krml/internal/target.h"
+
+#include "../Hacl_Spec.h"
+
+#define Spec_Cipher_Expansion_Hacl_CHACHA20 0
+#define Spec_Cipher_Expansion_Vale_AES128 1
+#define Spec_Cipher_Expansion_Vale_AES256 2
+
+typedef uint8_t Spec_Cipher_Expansion_impl;
+
+#define Spec_Frodo_Params_SHAKE128 0
+#define Spec_Frodo_Params_AES128 1
+
+typedef uint8_t Spec_Frodo_Params_frodo_gen_a;
+
+#if defined(__cplusplus)
+}
+#endif
+
+#define __internal_Hacl_Spec_H_DEFINED
+#endif
diff --git a/security/nss/lib/freebl/verified/internal/Vale.h b/security/nss/lib/freebl/verified/internal/Vale.h
new file mode 100644
index 0000000000..17af6593c9
--- /dev/null
+++ b/security/nss/lib/freebl/verified/internal/Vale.h
@@ -0,0 +1,185 @@
+/* MIT License
+ *
+ * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation
+ * Copyright (c) 2022-2023 HACL* Contributors
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the Software is
+ * furnished to do so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+ * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+ * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+ * SOFTWARE.
+ */
+
+#ifndef __internal_Vale_H
+#define __internal_Vale_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
+#include <string.h>
+#include "krml/internal/types.h"
+#include "krml/lowstar_endianness.h"
+#include "krml/internal/target.h"
+
+extern uint64_t add_scalar_e(uint64_t *x0, uint64_t *x1, uint64_t x2);
+
+extern uint64_t fadd_e(uint64_t *x0, uint64_t *x1, uint64_t *x2);
+
+extern uint64_t sha256_update(uint32_t *x0, uint8_t *x1, uint64_t x2, uint32_t *x3);
+
+extern uint64_t x64_poly1305(uint8_t *x0, uint8_t *x1, uint64_t x2, uint64_t x3);
+
+extern uint64_t check_aesni(void);
+
+extern uint64_t check_sha(void);
+
+extern uint64_t check_adx_bmi2(void);
+
+extern uint64_t check_avx(void);
+
+extern uint64_t check_avx2(void);
+
+extern uint64_t check_movbe(void);
+
+extern uint64_t check_sse(void);
+
+extern uint64_t check_rdrand(void);
+
+extern uint64_t check_avx512(void);
+
+extern uint64_t check_osxsave(void);
+
+extern uint64_t check_avx_xcr0(void);
+
+extern uint64_t check_avx512_xcr0(void);
+
+extern uint64_t
+gcm128_decrypt_opt(
+    uint8_t *x0,
+    uint64_t x1,
+    uint64_t x2,
+    uint8_t *x3,
+    uint8_t *x4,
+    uint8_t *x5,
+    uint8_t *x6,
+    uint8_t *x7,
+    uint8_t *x8,
+    uint64_t x9,
+    uint8_t *x10,
+    uint8_t *x11,
+    uint64_t x12,
+    uint8_t *x13,
+    uint64_t x14,
+    uint8_t *x15,
+    uint8_t *x16);
+
+extern uint64_t
+gcm256_decrypt_opt(
+    uint8_t *x0,
+    uint64_t x1,
+    uint64_t x2,
+    uint8_t *x3,
+    uint8_t *x4,
+    uint8_t *x5,
+    uint8_t *x6,
+    uint8_t *x7,
+    uint8_t *x8,
+    uint64_t x9,
+    uint8_t *x10,
+    uint8_t *x11,
+    uint64_t x12,
+    uint8_t *x13,
+    uint64_t x14,
+    uint8_t *x15,
+    uint8_t *x16);
+
+extern uint64_t aes128_key_expansion(uint8_t *x0, uint8_t *x1);
+
+extern uint64_t aes256_key_expansion(uint8_t *x0, uint8_t *x1);
+
+extern uint64_t
+compute_iv_stdcall(
+    uint8_t *x0,
+    uint64_t x1,
+    uint64_t x2,
+    uint8_t *x3,
+    uint8_t *x4,
+    uint8_t *x5);
+
+extern uint64_t
+gcm128_encrypt_opt(
+    uint8_t *x0,
+    uint64_t x1,
+    uint64_t x2,
+    uint8_t *x3,
+    uint8_t *x4,
+    uint8_t *x5,
+    uint8_t *x6,
+    uint8_t *x7,
+    uint8_t *x8,
+    uint64_t x9,
+    uint8_t *x10,
+    uint8_t *x11,
+    uint64_t x12,
+    uint8_t *x13,
+    uint64_t x14,
+    uint8_t *x15,
+    uint8_t *x16);
+
+extern uint64_t
+gcm256_encrypt_opt(
+    uint8_t *x0,
+    uint64_t x1,
+    uint64_t x2,
+    uint8_t *x3,
+    uint8_t *x4,
+    uint8_t *x5,
+    uint8_t *x6,
+    uint8_t *x7,
+    uint8_t *x8,
+    uint64_t x9,
+    uint8_t *x10,
+    uint8_t *x11,
+    uint64_t x12,
+    uint8_t *x13,
+    uint64_t x14,
+    uint8_t *x15,
+    uint8_t *x16);
+
+extern uint64_t aes128_keyhash_init(uint8_t *x0, uint8_t *x1);
+
+extern uint64_t aes256_keyhash_init(uint8_t *x0, uint8_t *x1);
+
+extern uint64_t cswap2_e(uint64_t x0, uint64_t *x1, uint64_t *x2);
+
+extern uint64_t fsqr_e(uint64_t *x0, uint64_t *x1, uint64_t *x2);
+
+extern uint64_t fsqr2_e(uint64_t *x0, uint64_t *x1, uint64_t *x2);
+
+extern uint64_t fmul_e(uint64_t *x0, uint64_t *x1, uint64_t *x2, uint64_t *x3);
+
+extern uint64_t fmul2_e(uint64_t *x0, uint64_t *x1, uint64_t *x2, uint64_t *x3);
+
+extern uint64_t fmul_scalar_e(uint64_t *x0, uint64_t *x1, uint64_t x2);
+
+extern uint64_t fsub_e(uint64_t *x0, uint64_t *x1, uint64_t *x2);
+
+#if defined(__cplusplus)
+}
+#endif
+
+#define __internal_Vale_H_DEFINED
+#endif