nss/SOURCES/nss_p256_scalar_validated.patch

diff -up ./lib/freebl/blapi.h.p256 ./lib/freebl/blapi.h
--- ./lib/freebl/blapi.h.p256	2023-06-04 01:42:53.000000000 -0700
+++ ./lib/freebl/blapi.h	2024-01-09 11:25:43.802382184 -0800
@@ -1791,6 +1791,11 @@ extern SECStatus EC_CopyParams(PLArenaPo
  */
 extern int EC_GetPointSize(const ECParams *params);
 
+/*
+ * use the internal table to get the size in bytes of a single EC coordinate
+ */
+extern int EC_GetScalarSize(const ECParams *params);
+
 SEC_END_PROTOS
 
 #endif /* _BLAPI_H_ */
diff -up ./lib/freebl/ec.c.p256 ./lib/freebl/ec.c
--- ./lib/freebl/ec.c.p256	2023-06-04 01:42:53.000000000 -0700
+++ ./lib/freebl/ec.c	2024-01-09 11:43:03.868335326 -0800
@@ -21,7 +21,17 @@
 static const ECMethod kMethods[] = {
     { ECCurve25519,
       ec_Curve25519_pt_mul,
-      ec_Curve25519_pt_validate }
+      ec_Curve25519_pt_validate,
+      ec_Curve25519_scalar_validate,
+      NULL, NULL },
+    {
+        ECCurve_NIST_P256,
+        ec_secp256r1_pt_mul,
+        ec_secp256r1_pt_validate,
+        ec_secp256r1_scalar_validate,
+        ec_secp256r1_sign_digest,
+        ec_secp256r1_verify_digest,
+    }
 };
 
 static const ECMethod *
@@ -281,13 +291,17 @@ ec_NewKey(ECParams *ecParams, ECPrivateK
     /* Use curve specific code for point multiplication */
     if (ecParams->fieldID.type == ec_field_plain) {
         const ECMethod *method = ec_get_method_from_name(ecParams->name);
-        if (method == NULL || method->mul == NULL) {
+        if (method == NULL || method->pt_mul == NULL) {
             /* unknown curve */
             rv = SECFailure;
             goto cleanup;
         }
-        rv = method->mul(&key->publicValue, &key->privateValue, NULL);
-        goto done;
+        rv = method->pt_mul(&key->publicValue, &key->privateValue, NULL);
+        if (rv != SECSuccess) {
+            goto cleanup;
+        } else {
+            goto done;
+        }
     }
 
     CHECK_MPI_OK(mp_init(&k));
@@ -330,25 +344,54 @@ EC_NewKeyFromSeed(ECParams *ecParams, EC
     return rv;
 }
 
-/* Generate a random private key using the algorithm A.4.1 of ANSI X9.62,
+/* Generate a random private key using the algorithm A.4.1 or A.4.2 of ANSI X9.62,
  * modified a la FIPS 186-2 Change Notice 1 to eliminate the bias in the
  * random number generator.
- *
- * Parameters
- * - order: a buffer that holds the curve's group order
- * - len: the length in octets of the order buffer
- *
- * Return Value
- * Returns a buffer of len octets that holds the private key. The caller
- * is responsible for freeing the buffer with PORT_ZFree.
  */
-static unsigned char *
-ec_GenerateRandomPrivateKey(const unsigned char *order, int len)
+
+SECStatus
+ec_GenerateRandomPrivateKey(ECParams *ecParams, SECItem *privKey)
 {
     SECStatus rv = SECSuccess;
     mp_err err;
-    unsigned char *privKeyBytes = NULL;
+
+    unsigned int len = EC_GetScalarSize(ecParams);
+
+    if (privKey->len != len || privKey->data == NULL) {
+        PORT_SetError(SEC_ERROR_INVALID_ARGS);
+        return SECFailure;
+    }
+
+    /* For known curves, use rejection sampling A.4.2 */
+    if (ecParams->fieldID.type == ec_field_plain) {
+        const ECMethod *method = ec_get_method_from_name(ecParams->name);
+        rv = SECFailure;
+        if (method == NULL || method->scalar_validate == NULL) {
+            /* unknown curve */
+            PORT_SetError(SEC_ERROR_INVALID_ARGS);
+            goto done;
+        }
+        int count = 100;
+        while (rv != SECSuccess && count >= 0) {
+            rv = RNG_GenerateGlobalRandomBytes(privKey->data, len);
+            if (rv != SECSuccess) {
+                PORT_SetError(SEC_ERROR_NEED_RANDOM);
+                goto done;
+            }
+            rv = method->scalar_validate(privKey);
+            count--;
+        }
+        if (rv != SECSuccess) {
+            PORT_SetError(SEC_ERROR_BAD_KEY);
+        }
+        goto done;
+    }
+
+    /* For unknown curves, use algotithm A.4.1 */
+
+    unsigned char *order = ecParams->order.data;
     mp_int privKeyVal, order_1, one;
+    unsigned char *privKeyBytes = NULL;
 
     MP_DIGITS(&privKeyVal) = 0;
     MP_DIGITS(&order_1) = 0;
@@ -361,8 +404,13 @@ ec_GenerateRandomPrivateKey(const unsign
      * (which implements Algorithm 1 of FIPS 186-2 Change Notice 1) then
      * reduces modulo the group order.
      */
-    if ((privKeyBytes = PORT_Alloc(2 * len)) == NULL)
+
+    if ((privKeyBytes = PORT_Alloc(2 * len)) == NULL) {
+        PORT_SetError(SEC_ERROR_NO_MEMORY);
+        rv = SECFailure;
         goto cleanup;
+    }
+
     CHECK_SEC_OK(RNG_GenerateGlobalRandomBytes(privKeyBytes, 2 * len));
     CHECK_MPI_OK(mp_read_unsigned_octets(&privKeyVal, privKeyBytes, 2 * len));
     CHECK_MPI_OK(mp_read_unsigned_octets(&order_1, order, len));
@@ -371,20 +419,26 @@ ec_GenerateRandomPrivateKey(const unsign
     CHECK_MPI_OK(mp_mod(&privKeyVal, &order_1, &privKeyVal));
     CHECK_MPI_OK(mp_add(&privKeyVal, &one, &privKeyVal));
     CHECK_MPI_OK(mp_to_fixlen_octets(&privKeyVal, privKeyBytes, len));
-    memset(privKeyBytes + len, 0, len);
+    memcpy(privKey->data, privKeyBytes, len);
+
 cleanup:
     mp_clear(&privKeyVal);
     mp_clear(&order_1);
     mp_clear(&one);
+    if (privKeyBytes) {
+        PORT_ZFree(privKeyBytes, 2 * len);
+    }
     if (err < MP_OKAY) {
         MP_TO_SEC_ERROR(err);
         rv = SECFailure;
     }
-    if (rv != SECSuccess && privKeyBytes) {
-        PORT_ZFree(privKeyBytes, 2 * len);
-        privKeyBytes = NULL;
+
+done:
+    if (rv != SECSuccess && privKey->data) {
+        SECITEM_ZfreeItem(privKey, PR_FALSE);
+        return rv;
     }
-    return privKeyBytes;
+    return rv;
 }
 
 /* Generates a new EC key pair. The private key is a random value and
@@ -395,24 +449,28 @@ SECStatus
 EC_NewKey(ECParams *ecParams, ECPrivateKey **privKey)
 {
     SECStatus rv = SECFailure;
-    int len;
-    unsigned char *privKeyBytes = NULL;
+    SECItem privKeyRand = { siBuffer, NULL, 0 };
 
     if (!ecParams || ecParams->name == ECCurve_noName || !privKey) {
         PORT_SetError(SEC_ERROR_INVALID_ARGS);
         return SECFailure;
     }
 
-    len = ecParams->order.len;
-    privKeyBytes = ec_GenerateRandomPrivateKey(ecParams->order.data, len);
-    if (privKeyBytes == NULL)
+    SECITEM_AllocItem(NULL, &privKeyRand, EC_GetScalarSize(ecParams));
+    if (privKeyRand.data == NULL) {
+        PORT_SetError(SEC_ERROR_NO_MEMORY);
+        rv = SECFailure;
+        goto cleanup;
+    }
+    rv = ec_GenerateRandomPrivateKey(ecParams, &privKeyRand);
+    if (rv != SECSuccess || privKeyRand.data == NULL)
         goto cleanup;
     /* generate public key */
-    CHECK_SEC_OK(ec_NewKey(ecParams, privKey, privKeyBytes, len));
+    CHECK_SEC_OK(ec_NewKey(ecParams, privKey, privKeyRand.data, privKeyRand.len));
 
 cleanup:
-    if (privKeyBytes) {
-        PORT_ZFree(privKeyBytes, len);
+    if (privKeyRand.data) {
+        SECITEM_ZfreeItem(&privKeyRand, PR_FALSE);
     }
 #if EC_DEBUG
     printf("EC_NewKey returning %s\n",
@@ -440,18 +498,24 @@ EC_ValidatePublicKey(ECParams *ecParams,
     if (!ecParams || ecParams->name == ECCurve_noName ||
         !publicValue || !publicValue->len) {
         PORT_SetError(SEC_ERROR_INVALID_ARGS);
-        return SECFailure;
+        rv = SECFailure;
+        return rv;
     }
 
     /* Uses curve specific code for point validation. */
     if (ecParams->fieldID.type == ec_field_plain) {
         const ECMethod *method = ec_get_method_from_name(ecParams->name);
-        if (method == NULL || method->validate == NULL) {
+        if (method == NULL || method->pt_validate == NULL) {
             /* unknown curve */
             PORT_SetError(SEC_ERROR_INVALID_ARGS);
-            return SECFailure;
+            rv = SECFailure;
+            return rv;
         }
-        return method->validate(publicValue);
+        rv = method->pt_validate(publicValue);
+        if (rv != SECSuccess) {
+            PORT_SetError(SEC_ERROR_BAD_KEY);
+        }
+        return rv;
     }
 
     /* NOTE: We only support uncompressed points for now */
@@ -510,6 +574,7 @@ cleanup:
     ECGroup_free(group);
     mp_clear(&Px);
     mp_clear(&Py);
+
     if (err) {
         MP_TO_SEC_ERROR(err);
         rv = SECFailure;
@@ -536,18 +601,14 @@ ECDH_Derive(SECItem *publicValue,
 {
     SECStatus rv = SECFailure;
     unsigned int len = 0;
-    SECItem pointQ = { siBuffer, NULL, 0 };
-    mp_int k; /* to hold the private value */
     mp_err err = MP_OKAY;
-#if EC_DEBUG
-    int i;
-#endif
 
     if (!publicValue || !publicValue->len ||
         !ecParams || ecParams->name == ECCurve_noName ||
         !privateValue || !privateValue->len || !derivedSecret) {
         PORT_SetError(SEC_ERROR_INVALID_ARGS);
-        return SECFailure;
+        rv = SECFailure;
+        return rv;
     }
 
     /*
@@ -556,31 +617,40 @@ ECDH_Derive(SECItem *publicValue,
      */
     if (EC_ValidatePublicKey(ecParams, publicValue) != SECSuccess) {
         PORT_SetError(SEC_ERROR_BAD_KEY);
-        return SECFailure;
+        rv = SECFailure;
+        return rv;
     }
 
     /* Perform curve specific multiplication using ECMethod */
     if (ecParams->fieldID.type == ec_field_plain) {
         const ECMethod *method;
         memset(derivedSecret, 0, sizeof(*derivedSecret));
-        derivedSecret = SECITEM_AllocItem(NULL, derivedSecret, EC_GetPointSize(ecParams));
+        derivedSecret = SECITEM_AllocItem(NULL, derivedSecret, EC_GetScalarSize(ecParams));
         if (derivedSecret == NULL) {
             PORT_SetError(SEC_ERROR_NO_MEMORY);
-            return SECFailure;
+            rv = SECFailure;
+            return rv;
         }
         method = ec_get_method_from_name(ecParams->name);
-        if (method == NULL || method->validate == NULL ||
-            method->mul == NULL) {
+        if (method == NULL || method->pt_validate == NULL ||
+            method->pt_mul == NULL) {
             PORT_SetError(SEC_ERROR_UNSUPPORTED_ELLIPTIC_CURVE);
-            return SECFailure;
+            rv = SECFailure;
+            goto done;
         }
-        rv = method->mul(derivedSecret, privateValue, publicValue);
+        rv = method->pt_mul(derivedSecret, privateValue, publicValue);
         if (rv != SECSuccess) {
-            SECITEM_ZfreeItem(derivedSecret, PR_FALSE);
+            PORT_SetError(SEC_ERROR_BAD_KEY);
         }
-        return rv;
+        goto done;
     }
 
+    SECItem pointQ = { siBuffer, NULL, 0 };
+    mp_int k; /* to hold the private value */
+#if EC_DEBUG
+    int i;
+#endif
+
     /*
      * We fail if the public value is the point at infinity, since
      * this produces predictable results.
@@ -638,14 +708,18 @@ ECDH_Derive(SECItem *publicValue,
 cleanup:
     mp_clear(&k);
 
-    if (err) {
-        MP_TO_SEC_ERROR(err);
-    }
-
     if (pointQ.data) {
         PORT_ZFree(pointQ.data, pointQ.len);
     }
 
+done:
+
+    if (err) {
+        MP_TO_SEC_ERROR(err);
+    }
+    if (rv != SECSuccess) {
+        SECITEM_ZfreeItem(derivedSecret, PR_FALSE);
+    }
     return rv;
 }
 
@@ -659,19 +733,57 @@ ec_SignDigestWithSeed(ECPrivateKey *key,
                       const SECItem *digest, const unsigned char *kb, const int kblen)
 {
     SECStatus rv = SECFailure;
+    ECParams *ecParams = NULL;
+    mp_err err = MP_OKAY;
+    int flen = 0;  /* length in bytes of the field size */
+    unsigned olen; /* length in bytes of the base point order */
+
+    /* Check args */
+    if (!key || !signature || !digest || !kb || (kblen <= 0)) {
+        PORT_SetError(SEC_ERROR_INVALID_ARGS);
+        rv = SECFailure;
+        goto done;
+    }
+
+    ecParams = &(key->ecParams);
+    flen = (ecParams->fieldID.size + 7) >> 3;
+    olen = ecParams->order.len;
+    if (signature->data == NULL) {
+        /* a call to get the signature length only */
+        signature->len = 2 * olen;
+        rv = SECSuccess;
+        goto done;
+    }
+    if (signature->len < 2 * olen) {
+        PORT_SetError(SEC_ERROR_OUTPUT_LEN);
+        rv = SECFailure;
+        goto done;
+    }
+
+    /* Perform curve specific signature using ECMethod */
+    if (ecParams->fieldID.type == ec_field_plain) {
+        const ECMethod *method = ec_get_method_from_name(ecParams->name);
+        if (method == NULL || method->sign_digest == NULL) {
+            PORT_SetError(SEC_ERROR_UNSUPPORTED_ELLIPTIC_CURVE);
+            rv = SECFailure;
+            goto done;
+        }
+        rv = method->sign_digest(key, signature, digest, kb, kblen);
+        if (rv != SECSuccess) {
+            PORT_SetError(SEC_ERROR_INVALID_ARGS);
+        }
+        goto done;
+    }
+
     mp_int x1;
     mp_int d, k; /* private key, random integer */
     mp_int r, s; /* tuple (r, s) is the signature */
     mp_int t;    /* holding tmp values */
     mp_int n;
     mp_int ar; /* blinding value */
-    mp_err err = MP_OKAY;
-    ECParams *ecParams = NULL;
     SECItem kGpoint = { siBuffer, NULL, 0 };
-    int flen = 0;   /* length in bytes of the field size */
-    unsigned olen;  /* length in bytes of the base point order */
-    unsigned obits; /* length in bits  of the base point order */
     unsigned char *t2 = NULL;
+    unsigned obits; /* length in bits  of the base point order */
 
 #if EC_DEBUG
     char mpstr[256];
@@ -688,24 +800,6 @@ ec_SignDigestWithSeed(ECPrivateKey *key,
     MP_DIGITS(&t) = 0;
     MP_DIGITS(&ar) = 0;
 
-    /* Check args */
-    if (!key || !signature || !digest || !kb || (kblen < 0)) {
-        PORT_SetError(SEC_ERROR_INVALID_ARGS);
-        goto cleanup;
-    }
-
-    ecParams = &(key->ecParams);
-    flen = (ecParams->fieldID.size + 7) >> 3;
-    olen = ecParams->order.len;
-    if (signature->data == NULL) {
-        /* a call to get the signature length only */
-        goto finish;
-    }
-    if (signature->len < 2 * olen) {
-        PORT_SetError(SEC_ERROR_OUTPUT_LEN);
-        goto cleanup;
-    }
-
     CHECK_MPI_OK(mp_init(&x1));
     CHECK_MPI_OK(mp_init(&d));
     CHECK_MPI_OK(mp_init(&k));
@@ -851,11 +945,11 @@ ec_SignDigestWithSeed(ECPrivateKey *key,
     */
     CHECK_MPI_OK(mp_to_fixlen_octets(&r, signature->data, olen));
     CHECK_MPI_OK(mp_to_fixlen_octets(&s, signature->data + olen, olen));
-finish:
-    signature->len = 2 * olen;
 
+    signature->len = 2 * olen;
     rv = SECSuccess;
     err = MP_OKAY;
+
 cleanup:
     mp_clear(&x1);
     mp_clear(&d);
@@ -874,6 +968,7 @@ cleanup:
         PORT_ZFree(kGpoint.data, kGpoint.len);
     }
 
+done:
     if (err) {
         MP_TO_SEC_ERROR(err);
         rv = SECFailure;
@@ -892,12 +987,12 @@ ECDSA_SignDigestWithSeed(ECPrivateKey *k
                          const SECItem *digest, const unsigned char *kb, const int kblen)
 {
 #if EC_DEBUG || EC_DOUBLECHECK
-
     SECItem *signature2 = SECITEM_AllocItem(NULL, NULL, signature->len);
     SECStatus signSuccess = ec_SignDigestWithSeed(key, signature, digest, kb, kblen);
     SECStatus signSuccessDouble = ec_SignDigestWithSeed(key, signature2, digest, kb, kblen);
-    int signaturesEqual = NSS_SecureMemcmp(signature, signature2, signature->len);
+    int signaturesEqual = NSS_SecureMemcmp(signature->data, signature2->data, signature->len);
     SECStatus rv;
+
     if ((signaturesEqual == 0) && (signSuccess == SECSuccess) && (signSuccessDouble == SECSuccess)) {
         rv = SECSuccess;
     } else {
@@ -923,8 +1018,7 @@ SECStatus
 ECDSA_SignDigest(ECPrivateKey *key, SECItem *signature, const SECItem *digest)
 {
     SECStatus rv = SECFailure;
-    int len;
-    unsigned char *kBytes = NULL;
+    SECItem nonceRand = { siBuffer, NULL, 0 };
 
     if (!key) {
         PORT_SetError(SEC_ERROR_INVALID_ARGS);
@@ -932,17 +1026,22 @@ ECDSA_SignDigest(ECPrivateKey *key, SECI
     }
 
     /* Generate random value k */
-    len = key->ecParams.order.len;
-    kBytes = ec_GenerateRandomPrivateKey(key->ecParams.order.data, len);
-    if (kBytes == NULL)
+    SECITEM_AllocItem(NULL, &nonceRand, EC_GetScalarSize(&key->ecParams));
+    if (nonceRand.data == NULL) {
+        PORT_SetError(SEC_ERROR_NO_MEMORY);
+        rv = SECFailure;
+        goto cleanup;
+    }
+    rv = ec_GenerateRandomPrivateKey(&key->ecParams, &nonceRand);
+    if (rv != SECSuccess || nonceRand.data == NULL)
         goto cleanup;
 
     /* Generate ECDSA signature with the specified k value */
-    rv = ECDSA_SignDigestWithSeed(key, signature, digest, kBytes, len);
+    rv = ECDSA_SignDigestWithSeed(key, signature, digest, nonceRand.data, nonceRand.len);
 
 cleanup:
-    if (kBytes) {
-        PORT_ZFree(kBytes, len);
+    if (nonceRand.data) {
+        SECITEM_ZfreeItem(&nonceRand, PR_FALSE);
     }
 
 #if EC_DEBUG
@@ -966,12 +1065,37 @@ ECDSA_VerifyDigest(ECPublicKey *key, con
                    const SECItem *digest)
 {
     SECStatus rv = SECFailure;
+    ECParams *ecParams = NULL;
+    mp_err err = MP_OKAY;
+
+    /* Check args */
+    if (!key || !signature || !digest) {
+        PORT_SetError(SEC_ERROR_INVALID_ARGS);
+        rv = SECFailure;
+        goto done;
+    }
+
+    ecParams = &(key->ecParams);
+
+    /* Perform curve specific signature verification using ECMethod */
+    if (ecParams->fieldID.type == ec_field_plain) {
+        const ECMethod *method = ec_get_method_from_name(ecParams->name);
+        if (method == NULL || method->verify_digest == NULL) {
+            PORT_SetError(SEC_ERROR_UNSUPPORTED_ELLIPTIC_CURVE);
+            rv = SECFailure;
+            goto done;
+        }
+        rv = method->verify_digest(key, signature, digest);
+        if (rv != SECSuccess) {
+            PORT_SetError(SEC_ERROR_BAD_SIGNATURE);
+        }
+        goto done;
+    }
+
     mp_int r_, s_;       /* tuple (r', s') is received signature) */
     mp_int c, u1, u2, v; /* intermediate values used in verification */
     mp_int x1;
     mp_int n;
-    mp_err err = MP_OKAY;
-    ECParams *ecParams = NULL;
     SECItem pointC = { siBuffer, NULL, 0 };
     int slen;       /* length in bytes of a half signature (r or s) */
     int flen;       /* length in bytes of the field size */
@@ -983,6 +1107,15 @@ ECDSA_VerifyDigest(ECPublicKey *key, con
     printf("ECDSA verification called\n");
 #endif
 
+    flen = (ecParams->fieldID.size + 7) >> 3;
+    olen = ecParams->order.len;
+    if (signature->len == 0 || signature->len % 2 != 0 ||
+        signature->len > 2 * olen) {
+        PORT_SetError(SEC_ERROR_INPUT_LEN);
+        goto cleanup;
+    }
+    slen = signature->len / 2;
+
     /* Initialize MPI integers. */
     /* must happen before the first potential call to cleanup */
     MP_DIGITS(&r_) = 0;
@@ -994,22 +1127,6 @@ ECDSA_VerifyDigest(ECPublicKey *key, con
     MP_DIGITS(&v) = 0;
     MP_DIGITS(&n) = 0;
 
-    /* Check args */
-    if (!key || !signature || !digest) {
-        PORT_SetError(SEC_ERROR_INVALID_ARGS);
-        goto cleanup;
-    }
-
-    ecParams = &(key->ecParams);
-    flen = (ecParams->fieldID.size + 7) >> 3;
-    olen = ecParams->order.len;
-    if (signature->len == 0 || signature->len % 2 != 0 ||
-        signature->len > 2 * olen) {
-        PORT_SetError(SEC_ERROR_INPUT_LEN);
-        goto cleanup;
-    }
-    slen = signature->len / 2;
-
     /*
      * The incoming point has been verified in sftk_handlePublicKeyObject.
      */
@@ -1156,6 +1273,8 @@ cleanup:
 
     if (pointC.data)
         SECITEM_ZfreeItem(&pointC, PR_FALSE);
+
+done:
     if (err) {
         MP_TO_SEC_ERROR(err);
         rv = SECFailure;
diff -up ./lib/freebl/ecdecode.c.p256 ./lib/freebl/ecdecode.c
--- ./lib/freebl/ecdecode.c.p256	2023-06-04 01:42:53.000000000 -0700
+++ ./lib/freebl/ecdecode.c	2024-01-09 11:25:43.802382184 -0800
@@ -155,7 +155,7 @@ EC_FillParams(PLArenaPool *arena, const
              * (the NIST P-256 curve)
              */
             CHECK_SEC_OK(gf_populate_params_bytes(ECCurve_X9_62_PRIME_256V1,
-                                                  ec_field_GFp, params));
+                                                  ec_field_plain, params));
             break;
 
         case SEC_OID_SECG_EC_SECP384R1:
@@ -176,7 +176,8 @@ EC_FillParams(PLArenaPool *arena, const
 
         case SEC_OID_CURVE25519:
             /* Populate params for Curve25519 */
-            CHECK_SEC_OK(gf_populate_params_bytes(ECCurve25519, ec_field_plain,
+            CHECK_SEC_OK(gf_populate_params_bytes(ECCurve25519,
+                                                  ec_field_plain,
                                                   params));
             break;
 
@@ -250,3 +251,18 @@ EC_GetPointSize(const ECParams *params)
     }
     return curveParams->pointSize - 1;
 }
+
+int
+EC_GetScalarSize(const ECParams *params)
+{
+    ECCurveName name = params->name;
+    const ECCurveBytes *curveParams;
+
+    if ((name < ECCurve_noName) || (name > ECCurve_pastLastCurve) ||
+        ((curveParams = ecCurve_map[name]) == NULL)) {
+        /* unknown curve, calculate scalar size from field size in params */
+        int sizeInBytes = (params->fieldID.size + 7) / 8;
+        return sizeInBytes;
+    }
+    return curveParams->scalarSize;
+}
diff -up ./lib/freebl/ec.h.p256 ./lib/freebl/ec.h
--- ./lib/freebl/ec.h.p256	2023-06-04 01:42:53.000000000 -0700
+++ ./lib/freebl/ec.h	2024-01-09 11:43:03.868335326 -0800
@@ -13,8 +13,11 @@
 
 struct ECMethodStr {
     ECCurveName name;
-    SECStatus (*mul)(SECItem *result, SECItem *scalar, SECItem *point);
-    SECStatus (*validate)(const SECItem *point);
+    SECStatus (*pt_mul)(SECItem *result, SECItem *scalar, SECItem *point);
+    SECStatus (*pt_validate)(const SECItem *point);
+    SECStatus (*scalar_validate)(const SECItem *scalar);
+    SECStatus (*sign_digest)(ECPrivateKey *key, SECItem *signature, const SECItem *digest, const unsigned char *kb, const unsigned int kblen);
+    SECStatus (*verify_digest)(ECPublicKey *key, const SECItem *signature, const SECItem *digest);
 };
 typedef struct ECMethodStr ECMethod;
 
diff -up ./lib/freebl/ecl/ecl.h.p256 ./lib/freebl/ecl/ecl.h
--- ./lib/freebl/ecl/ecl.h.p256	2023-06-04 01:42:53.000000000 -0700
+++ ./lib/freebl/ecl/ecl.h	2024-01-09 11:43:03.868335326 -0800
@@ -45,5 +45,16 @@ mp_err ECPoint_validate(const ECGroup *g
 
 SECStatus ec_Curve25519_pt_mul(SECItem *X, SECItem *k, SECItem *P);
 SECStatus ec_Curve25519_pt_validate(const SECItem *px);
+SECStatus ec_Curve25519_scalar_validate(const SECItem *scalar);
+
+SECStatus ec_secp256r1_pt_mul(SECItem *X, SECItem *k, SECItem *P);
+SECStatus ec_secp256r1_pt_validate(const SECItem *px);
+SECStatus ec_secp256r1_scalar_validate(const SECItem *scalar);
+
+SECStatus ec_secp256r1_sign_digest(ECPrivateKey *key, SECItem *signature,
+                                   const SECItem *digest, const unsigned char *kb,
+                                   const unsigned int kblen);
+SECStatus ec_secp256r1_verify_digest(ECPublicKey *key, const SECItem *signature,
+                                     const SECItem *digest);
 
 #endif /* __ecl_h_ */
diff -up ./lib/freebl/ecl/ecp_25519.c.p256 ./lib/freebl/ecl/ecp_25519.c
--- ./lib/freebl/ecl/ecp_25519.c.p256	2023-06-04 01:42:53.000000000 -0700
+++ ./lib/freebl/ecl/ecp_25519.c	2024-01-09 11:43:03.868335326 -0800
@@ -15,6 +15,7 @@
 #include "mpi-priv.h"
 #include "secmpi.h"
 #include "secitem.h"
+#include "secerr.h"
 #include "secport.h"
 #include <stdlib.h>
 #include <stdio.h>
@@ -94,6 +95,24 @@ ec_Curve25519_pt_validate(const SECItem
     return SECSuccess;
 }
 
+/*
+ * scalar validation is not necessary. 
+ */
+SECStatus
+ec_Curve25519_scalar_validate(const SECItem *scalar)
+{
+    if (!scalar || !scalar->data) {
+        PORT_SetError(SEC_ERROR_INVALID_ARGS);
+        return SECFailure;
+    }
+
+    if (scalar->len != 32) {
+        PORT_SetError(SEC_ERROR_BAD_KEY);
+        return SECFailure;
+    }
+    return SECSuccess;
+}
+
 /*
  * Scalar multiplication for Curve25519.
  * If P == NULL, the base point is used.
diff -up ./lib/freebl/ecl/ecp_secp256r1.c.p256 ./lib/freebl/ecl/ecp_secp256r1.c
--- ./lib/freebl/ecl/ecp_secp256r1.c.p256	2024-01-09 11:25:43.802382184 -0800
+++ ./lib/freebl/ecl/ecp_secp256r1.c	2024-01-09 11:43:03.868335326 -0800
@@ -0,0 +1,258 @@
+/* P-256 from HACL* */
+
+#ifdef FREEBL_NO_DEPEND
+#include "../stubs.h"
+#endif
+
+#include "ecl-priv.h"
+#include "secitem.h"
+#include "secerr.h"
+#include "secmpi.h"
+#include "../verified/Hacl_P256.h"
+
+/*
+ * Point Validation for P-256.
+ */
+
+SECStatus
+ec_secp256r1_pt_validate(const SECItem *pt)
+{
+    SECStatus res = SECSuccess;
+    if (!pt || !pt->data) {
+        PORT_SetError(SEC_ERROR_INVALID_ARGS);
+        res = SECFailure;
+        return res;
+    }
+
+    if (pt->len != 65) {
+        PORT_SetError(SEC_ERROR_BAD_KEY);
+        res = SECFailure;
+        return res;
+    }
+
+    if (pt->data[0] != EC_POINT_FORM_UNCOMPRESSED) {
+        PORT_SetError(SEC_ERROR_UNSUPPORTED_EC_POINT_FORM);
+        res = SECFailure;
+        return res;
+    }
+
+    bool b = Hacl_P256_validate_public_key(pt->data + 1);
+
+    if (!b) {
+        PORT_SetError(SEC_ERROR_BAD_KEY);
+        res = SECFailure;
+    }
+    return res;
+}
+
+/*
+ * Scalar Validation for P-256.
+ */
+
+SECStatus
+ec_secp256r1_scalar_validate(const SECItem *scalar)
+{
+    SECStatus res = SECSuccess;
+    if (!scalar || !scalar->data) {
+        PORT_SetError(SEC_ERROR_INVALID_ARGS);
+        res = SECFailure;
+        return res;
+    }
+
+    if (scalar->len != 32) {
+        PORT_SetError(SEC_ERROR_BAD_KEY);
+        res = SECFailure;
+        return res;
+    }
+
+    bool b = Hacl_P256_validate_private_key(scalar->data);
+
+    if (!b) {
+        PORT_SetError(SEC_ERROR_BAD_KEY);
+        res = SECFailure;
+    }
+    return res;
+}
+
+/*
+ * Scalar multiplication for P-256.
+ * If P == NULL, the base point is used.
+ * Returns X = k*P
+ */
+
+SECStatus
+ec_secp256r1_pt_mul(SECItem *X, SECItem *k, SECItem *P)
+{
+    SECStatus res = SECSuccess;
+    if (!P) {
+        uint8_t derived[64] = { 0 };
+
+        if (!X || !k || !X->data || !k->data ||
+            X->len < 65 || k->len != 32) {
+            PORT_SetError(SEC_ERROR_INVALID_ARGS);
+            res = SECFailure;
+            return res;
+        }
+
+        bool b = Hacl_P256_dh_initiator(derived, k->data);
+
+        if (!b) {
+            PORT_SetError(SEC_ERROR_BAD_KEY);
+            res = SECFailure;
+            return res;
+        }
+
+        X->len = 65;
+        X->data[0] = EC_POINT_FORM_UNCOMPRESSED;
+        memcpy(X->data + 1, derived, 64);
+
+    } else {
+        uint8_t full_key[32] = { 0 };
+        uint8_t *key;
+        uint8_t derived[64] = { 0 };
+
+        if (!X || !k || !P || !X->data || !k->data || !P->data ||
+            X->len < 32 || P->len != 65 ||
+            P->data[0] != EC_POINT_FORM_UNCOMPRESSED) {
+            PORT_SetError(SEC_ERROR_INVALID_ARGS);
+            res = SECFailure;
+            return res;
+        }
+
+        /* We consider keys of up to size 32, or of size 33 with a single leading 0 */
+        if (k->len < 32) {
+            memcpy(full_key + 32 - k->len, k->data, k->len);
+            key = full_key;
+        } else if (k->len == 32) {
+            key = k->data;
+        } else if (k->len == 33 && k->data[0] == 0) {
+            key = k->data + 1;
+        } else {
+            PORT_SetError(SEC_ERROR_INVALID_ARGS);
+            res = SECFailure;
+            return res;
+        }
+
+        bool b = Hacl_P256_dh_responder(derived, P->data + 1, key);
+
+        if (!b) {
+            PORT_SetError(SEC_ERROR_BAD_KEY);
+            res = SECFailure;
+            return res;
+        }
+
+        X->len = 32;
+        memcpy(X->data, derived, 32);
+    }
+
+    return res;
+}
+
+/*
+ * ECDSA Signature for P-256
+ */
+
+SECStatus
+ec_secp256r1_sign_digest(ECPrivateKey *key, SECItem *signature,
+                         const SECItem *digest, const unsigned char *kb,
+                         const unsigned int kblen)
+{
+    SECStatus res = SECSuccess;
+
+    if (!key || !signature || !digest || !kb ||
+        !key->privateValue.data ||
+        !signature->data || !digest->data ||
+        key->ecParams.name != ECCurve_NIST_P256) {
+        PORT_SetError(SEC_ERROR_INVALID_ARGS);
+        res = SECFailure;
+        return res;
+    }
+
+    if (key->privateValue.len != 32 ||
+        kblen == 0 ||
+        digest->len == 0 ||
+        signature->len < 64) {
+        PORT_SetError(SEC_ERROR_INPUT_LEN);
+        res = SECFailure;
+        return res;
+    }
+
+    uint8_t hash[32] = { 0 };
+    if (digest->len < 32) {
+        memcpy(hash + 32 - digest->len, digest->data, digest->len);
+    } else {
+        memcpy(hash, digest->data, 32);
+    }
+
+    uint8_t nonce[32] = { 0 };
+    if (kblen < 32) {
+        memcpy(nonce + 32 - kblen, kb, kblen);
+    } else {
+        memcpy(nonce, kb, 32);
+    }
+
+    bool b = Hacl_P256_ecdsa_sign_p256_without_hash(
+        signature->data, 32, hash,
+        key->privateValue.data, nonce);
+    if (!b) {
+        PORT_SetError(SEC_ERROR_BAD_KEY);
+        res = SECFailure;
+        return res;
+    }
+
+    signature->len = 64;
+    return res;
+}
+
+/*
+ * ECDSA Signature Verification for P-256
+ */
+
+SECStatus
+ec_secp256r1_verify_digest(ECPublicKey *key, const SECItem *signature,
+                           const SECItem *digest)
+{
+    SECStatus res = SECSuccess;
+
+    if (!key || !signature || !digest ||
+        !key->publicValue.data ||
+        !signature->data || !digest->data ||
+        key->ecParams.name != ECCurve_NIST_P256) {
+        PORT_SetError(SEC_ERROR_INVALID_ARGS);
+        res = SECFailure;
+        return res;
+    }
+
+    if (key->publicValue.len != 65 ||
+        digest->len == 0 ||
+        signature->len != 64) {
+        PORT_SetError(SEC_ERROR_INPUT_LEN);
+        res = SECFailure;
+        return res;
+    }
+
+    if (key->publicValue.data[0] != EC_POINT_FORM_UNCOMPRESSED) {
+        PORT_SetError(SEC_ERROR_UNSUPPORTED_EC_POINT_FORM);
+        res = SECFailure;
+        return res;
+    }
+
+    uint8_t hash[32] = { 0 };
+    if (digest->len < 32) {
+        memcpy(hash + 32 - digest->len, digest->data, digest->len);
+    } else {
+        memcpy(hash, digest->data, 32);
+    }
+
+    bool b = Hacl_P256_ecdsa_verif_without_hash(
+        32, hash,
+        key->publicValue.data + 1,
+        signature->data, signature->data + 32);
+    if (!b) {
+        PORT_SetError(SEC_ERROR_BAD_SIGNATURE);
+        res = SECFailure;
+        return res;
+    }
+
+    return res;
+}
diff -up ./lib/freebl/freebl_base.gypi.p256 ./lib/freebl/freebl_base.gypi
--- ./lib/freebl/freebl_base.gypi.p256	2024-01-09 11:22:17.628127464 -0800
+++ ./lib/freebl/freebl_base.gypi	2024-01-09 11:25:43.802382184 -0800
@@ -34,8 +34,10 @@
     'ecl/ecp_jac.c',
     'ecl/ecp_jm.c',
     'ecl/ecp_mont.c',
+    'ecl/ecp_secp256r1.c',
     'ecl/ecp_secp384r1.c',
     'ecl/ecp_secp521r1.c',
+    'verified/Hacl_P256.c',
     'fipsfreebl.c',
     'blinit.c',
     'freeblver.c',
diff -up ./lib/freebl/freebl.gyp.p256 ./lib/freebl/freebl.gyp
--- ./lib/freebl/freebl.gyp.p256	2024-01-09 11:22:17.628127464 -0800
+++ ./lib/freebl/freebl.gyp	2024-01-09 11:25:43.802382184 -0800
@@ -839,6 +839,7 @@
         'defines':[
           'HACL_CAN_COMPILE_VEC128',
           'HACL_CAN_COMPILE_VEC256',
+          'HACL_CAN_COMPILE_INTRINSICS',
         ],
       }],
       # MSVC has no __int128 type. Use emulated int128 and leave
@@ -847,6 +848,7 @@
         'defines': [
           # The Makefile does version-tests on GCC, but we're not doing that here.
           'HAVE_INT128_SUPPORT',
+          'HACL_CAN_COMPILE_UINT128'
         ],
       }, {
         'defines': [
diff -up ./lib/freebl/Makefile.p256 ./lib/freebl/Makefile
--- ./lib/freebl/Makefile.p256	2024-01-09 11:25:43.802382184 -0800
+++ ./lib/freebl/Makefile	2024-01-09 11:27:42.154676474 -0800
@@ -612,6 +612,8 @@ ifndef NSS_DISABLE_CHACHAPOLY
     VERIFIED_SRCS += Hacl_Poly1305_32.c Hacl_Chacha20.c Hacl_Chacha20Poly1305_32.c
 endif # NSS_DISABLE_CHACHAPOLY
 
+VERIFIED_SRCS += Hacl_P256.c
+
 ifeq (,$(filter-out x86_64 aarch64,$(CPU_ARCH)))
     # All 64-bit architectures get the 64 bit version.
     ECL_SRCS += curve25519_64.c
diff -up ./lib/freebl/manifest.mn.p256 ./lib/freebl/manifest.mn
--- ./lib/freebl/manifest.mn.p256	2023-06-04 01:42:53.000000000 -0700
+++ ./lib/freebl/manifest.mn	2024-01-09 11:25:43.803382195 -0800
@@ -107,7 +107,7 @@ ECL_HDRS = ecl-exp.h ecl.h ecp.h ecl-pri
 ECL_SRCS = ecl.c ecl_mult.c ecl_gf.c \
 	ecp_aff.c ecp_jac.c ecp_mont.c \
 	ec_naf.c ecp_jm.c ecp_256.c ecp_384.c ecp_521.c \
-	ecp_256_32.c ecp_25519.c ecp_secp384r1.c ecp_secp521r1.c
+	ecp_256_32.c ecp_25519.c ecp_secp256r1.c ecp_secp384r1.c ecp_secp521r1.c
 SHA_SRCS = sha_fast.c
 MPCPU_SRCS = mpcpucache.c
 VERIFIED_SRCS = $(NULL)
diff -up ./lib/freebl/verified/Hacl_P256.c.p256 ./lib/freebl/verified/Hacl_P256.c
--- ./lib/freebl/verified/Hacl_P256.c.p256	2024-01-09 11:25:43.803382195 -0800
+++ ./lib/freebl/verified/Hacl_P256.c	2024-01-09 11:25:43.803382195 -0800
@@ -0,0 +1,1832 @@
+/* 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.
+ */
+
+#include "internal/Hacl_P256.h"
+
+#include "internal/Hacl_P256_PrecompTable.h"
+#include "internal/Hacl_Krmllib.h"
+#include "internal/Hacl_Bignum_Base.h"
+#include "lib_intrinsics.h"
+
+static inline uint64_t
+bn_is_zero_mask4(uint64_t *f)
+{
+    uint64_t bn_zero[4U] = { 0U };
+    uint64_t mask = (uint64_t)0xFFFFFFFFFFFFFFFFU;
+    KRML_MAYBE_FOR4(i,
+                    (uint32_t)0U,
+                    (uint32_t)4U,
+                    (uint32_t)1U,
+                    uint64_t uu____0 = FStar_UInt64_eq_mask(f[i], bn_zero[i]);
+                    mask = uu____0 & mask;);
+    uint64_t mask1 = mask;
+    uint64_t res = mask1;
+    return res;
+}
+
+static inline bool
+bn_is_zero_vartime4(uint64_t *f)
+{
+    uint64_t m = bn_is_zero_mask4(f);
+    return m == (uint64_t)0xFFFFFFFFFFFFFFFFU;
+}
+
+static inline uint64_t
+bn_is_eq_mask4(uint64_t *a, uint64_t *b)
+{
+    uint64_t mask = (uint64_t)0xFFFFFFFFFFFFFFFFU;
+    KRML_MAYBE_FOR4(i,
+                    (uint32_t)0U,
+                    (uint32_t)4U,
+                    (uint32_t)1U,
+                    uint64_t uu____0 = FStar_UInt64_eq_mask(a[i], b[i]);
+                    mask = uu____0 & mask;);
+    uint64_t mask1 = mask;
+    return mask1;
+}
+
+static inline bool
+bn_is_eq_vartime4(uint64_t *a, uint64_t *b)
+{
+    uint64_t m = bn_is_eq_mask4(a, b);
+    return m == (uint64_t)0xFFFFFFFFFFFFFFFFU;
+}
+
+static inline void
+bn_cmovznz4(uint64_t *res, uint64_t cin, uint64_t *x, uint64_t *y)
+{
+    uint64_t mask = ~FStar_UInt64_eq_mask(cin, (uint64_t)0U);
+    KRML_MAYBE_FOR4(i,
+                    (uint32_t)0U,
+                    (uint32_t)4U,
+                    (uint32_t)1U,
+                    uint64_t *os = res;
+                    uint64_t uu____0 = x[i];
+                    uint64_t x1 = uu____0 ^ (mask & (y[i] ^ uu____0));
+                    os[i] = x1;);
+}
+
+static inline void
+bn_add_mod4(uint64_t *res, uint64_t *n, uint64_t *x, uint64_t *y)
+{
+    uint64_t c0 = (uint64_t)0U;
+    {
+        uint64_t t1 = x[(uint32_t)4U * (uint32_t)0U];
+        uint64_t t20 = y[(uint32_t)4U * (uint32_t)0U];
+        uint64_t *res_i0 = res + (uint32_t)4U * (uint32_t)0U;
+        c0 = Lib_IntTypes_Intrinsics_add_carry_u64(c0, t1, t20, res_i0);
+        uint64_t t10 = x[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U];
+        uint64_t t21 = y[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U];
+        uint64_t *res_i1 = res + (uint32_t)4U * (uint32_t)0U + (uint32_t)1U;
+        c0 = Lib_IntTypes_Intrinsics_add_carry_u64(c0, t10, t21, res_i1);
+        uint64_t t11 = x[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U];
+        uint64_t t22 = y[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U];
+        uint64_t *res_i2 = res + (uint32_t)4U * (uint32_t)0U + (uint32_t)2U;
+        c0 = Lib_IntTypes_Intrinsics_add_carry_u64(c0, t11, t22, res_i2);
+        uint64_t t12 = x[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U];
+        uint64_t t2 = y[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U];
+        uint64_t *res_i = res + (uint32_t)4U * (uint32_t)0U + (uint32_t)3U;
+        c0 = Lib_IntTypes_Intrinsics_add_carry_u64(c0, t12, t2, res_i);
+    }
+    uint64_t c00 = c0;
+    uint64_t tmp[4U] = { 0U };
+    uint64_t c = (uint64_t)0U;
+    {
+        uint64_t t1 = res[(uint32_t)4U * (uint32_t)0U];
+        uint64_t t20 = n[(uint32_t)4U * (uint32_t)0U];
+        uint64_t *res_i0 = tmp + (uint32_t)4U * (uint32_t)0U;
+        c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t1, t20, res_i0);
+        uint64_t t10 = res[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U];
+        uint64_t t21 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U];
+        uint64_t *res_i1 = tmp + (uint32_t)4U * (uint32_t)0U + (uint32_t)1U;
+        c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t10, t21, res_i1);
+        uint64_t t11 = res[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U];
+        uint64_t t22 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U];
+        uint64_t *res_i2 = tmp + (uint32_t)4U * (uint32_t)0U + (uint32_t)2U;
+        c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t11, t22, res_i2);
+        uint64_t t12 = res[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U];
+        uint64_t t2 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U];
+        uint64_t *res_i = tmp + (uint32_t)4U * (uint32_t)0U + (uint32_t)3U;
+        c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t12, t2, res_i);
+    }
+    uint64_t c1 = c;
+    uint64_t c2 = c00 - c1;
+    KRML_MAYBE_FOR4(i,
+                    (uint32_t)0U,
+                    (uint32_t)4U,
+                    (uint32_t)1U,
+                    uint64_t *os = res;
+                    uint64_t x1 = (c2 & res[i]) | (~c2 & tmp[i]);
+                    os[i] = x1;);
+}
+
+static inline uint64_t
+bn_sub4(uint64_t *res, uint64_t *x, uint64_t *y)
+{
+    uint64_t c = (uint64_t)0U;
+    {
+        uint64_t t1 = x[(uint32_t)4U * (uint32_t)0U];
+        uint64_t t20 = y[(uint32_t)4U * (uint32_t)0U];
+        uint64_t *res_i0 = res + (uint32_t)4U * (uint32_t)0U;
+        c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t1, t20, res_i0);
+        uint64_t t10 = x[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U];
+        uint64_t t21 = y[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U];
+        uint64_t *res_i1 = res + (uint32_t)4U * (uint32_t)0U + (uint32_t)1U;
+        c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t10, t21, res_i1);
+        uint64_t t11 = x[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U];
+        uint64_t t22 = y[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U];
+        uint64_t *res_i2 = res + (uint32_t)4U * (uint32_t)0U + (uint32_t)2U;
+        c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t11, t22, res_i2);
+        uint64_t t12 = x[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U];
+        uint64_t t2 = y[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U];
+        uint64_t *res_i = res + (uint32_t)4U * (uint32_t)0U + (uint32_t)3U;
+        c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t12, t2, res_i);
+    }
+    uint64_t c0 = c;
+    return c0;
+}
+
+static inline void
+bn_sub_mod4(uint64_t *res, uint64_t *n, uint64_t *x, uint64_t *y)
+{
+    uint64_t c0 = (uint64_t)0U;
+    {
+        uint64_t t1 = x[(uint32_t)4U * (uint32_t)0U];
+        uint64_t t20 = y[(uint32_t)4U * (uint32_t)0U];
+        uint64_t *res_i0 = res + (uint32_t)4U * (uint32_t)0U;
+        c0 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c0, t1, t20, res_i0);
+        uint64_t t10 = x[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U];
+        uint64_t t21 = y[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U];
+        uint64_t *res_i1 = res + (uint32_t)4U * (uint32_t)0U + (uint32_t)1U;
+        c0 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c0, t10, t21, res_i1);
+        uint64_t t11 = x[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U];
+        uint64_t t22 = y[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U];
+        uint64_t *res_i2 = res + (uint32_t)4U * (uint32_t)0U + (uint32_t)2U;
+        c0 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c0, t11, t22, res_i2);
+        uint64_t t12 = x[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U];
+        uint64_t t2 = y[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U];
+        uint64_t *res_i = res + (uint32_t)4U * (uint32_t)0U + (uint32_t)3U;
+        c0 = Lib_IntTypes_Intrinsics_sub_borrow_u64(c0, t12, t2, res_i);
+    }
+    uint64_t c00 = c0;
+    uint64_t tmp[4U] = { 0U };
+    uint64_t c = (uint64_t)0U;
+    {
+        uint64_t t1 = res[(uint32_t)4U * (uint32_t)0U];
+        uint64_t t20 = n[(uint32_t)4U * (uint32_t)0U];
+        uint64_t *res_i0 = tmp + (uint32_t)4U * (uint32_t)0U;
+        c = Lib_IntTypes_Intrinsics_add_carry_u64(c, t1, t20, res_i0);
+        uint64_t t10 = res[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U];
+        uint64_t t21 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U];
+        uint64_t *res_i1 = tmp + (uint32_t)4U * (uint32_t)0U + (uint32_t)1U;
+        c = Lib_IntTypes_Intrinsics_add_carry_u64(c, t10, t21, res_i1);
+        uint64_t t11 = res[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U];
+        uint64_t t22 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U];
+        uint64_t *res_i2 = tmp + (uint32_t)4U * (uint32_t)0U + (uint32_t)2U;
+        c = Lib_IntTypes_Intrinsics_add_carry_u64(c, t11, t22, res_i2);
+        uint64_t t12 = res[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U];
+        uint64_t t2 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U];
+        uint64_t *res_i = tmp + (uint32_t)4U * (uint32_t)0U + (uint32_t)3U;
+        c = Lib_IntTypes_Intrinsics_add_carry_u64(c, t12, t2, res_i);
+    }
+    uint64_t c1 = c;
+    // TODO: remove unused variable
+    (void)c1;
+    uint64_t c2 = (uint64_t)0U - c00;
+    KRML_MAYBE_FOR4(i,
+                    (uint32_t)0U,
+                    (uint32_t)4U,
+                    (uint32_t)1U,
+                    uint64_t *os = res;
+                    uint64_t x1 = (c2 & tmp[i]) | (~c2 & res[i]);
+                    os[i] = x1;);
+}
+
+static inline void
+bn_mul4(uint64_t *res, uint64_t *x, uint64_t *y)
+{
+    memset(res, 0U, (uint32_t)8U * sizeof(uint64_t));
+    KRML_MAYBE_FOR4(
+        i0,
+        (uint32_t)0U,
+        (uint32_t)4U,
+        (uint32_t)1U,
+        uint64_t bj = y[i0];
+        uint64_t *res_j = res + i0;
+        uint64_t c = (uint64_t)0U;
+        {
+            uint64_t a_i = x[(uint32_t)4U * (uint32_t)0U];
+            uint64_t *res_i0 = res_j + (uint32_t)4U * (uint32_t)0U;
+            c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, bj, c, res_i0);
+            uint64_t a_i0 = x[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U];
+            uint64_t *res_i1 = res_j + (uint32_t)4U * (uint32_t)0U + (uint32_t)1U;
+            c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i0, bj, c, res_i1);
+            uint64_t a_i1 = x[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U];
+            uint64_t *res_i2 = res_j + (uint32_t)4U * (uint32_t)0U + (uint32_t)2U;
+            c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i1, bj, c, res_i2);
+            uint64_t a_i2 = x[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U];
+            uint64_t *res_i = res_j + (uint32_t)4U * (uint32_t)0U + (uint32_t)3U;
+            c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i2, bj, c, res_i);
+        } uint64_t r = c;
+        res[(uint32_t)4U + i0] = r;);
+}
+
+static inline void
+bn_sqr4(uint64_t *res, uint64_t *x)
+{
+    memset(res, 0U, (uint32_t)8U * sizeof(uint64_t));
+    KRML_MAYBE_FOR4(
+        i0,
+        (uint32_t)0U,
+        (uint32_t)4U,
+        (uint32_t)1U,
+        uint64_t *ab = x;
+        uint64_t a_j = x[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((uint32_t)8U, res, res, res);
+    // TODO: remove unused variable
+    (void)c0;
+    uint64_t tmp[8U] = { 0U };
+    KRML_MAYBE_FOR4(i,
+                    (uint32_t)0U,
+                    (uint32_t)4U,
+                    (uint32_t)1U,
+                    FStar_UInt128_uint128 res1 = FStar_UInt128_mul_wide(x[i], x[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((uint32_t)8U, res, tmp, res);
+    // TODO: remove unused variable
+    (void)c1;
+}
+
+static inline void
+bn_to_bytes_be4(uint8_t *res, uint64_t *f)
+{
+    KRML_MAYBE_FOR4(i,
+                    (uint32_t)0U,
+                    (uint32_t)4U,
+                    (uint32_t)1U,
+                    store64_be(res + i * (uint32_t)8U, f[(uint32_t)4U - i - (uint32_t)1U]););
+}
+
+static inline void
+bn_from_bytes_be4(uint64_t *res, uint8_t *b)
+{
+    KRML_MAYBE_FOR4(i,
+                    (uint32_t)0U,
+                    (uint32_t)4U,
+                    (uint32_t)1U,
+                    uint64_t *os = res;
+                    uint64_t u = load64_be(b + ((uint32_t)4U - i - (uint32_t)1U) * (uint32_t)8U);
+                    uint64_t x = u;
+                    os[i] = x;);
+}
+
+static inline void
+bn2_to_bytes_be4(uint8_t *res, uint64_t *x, uint64_t *y)
+{
+    bn_to_bytes_be4(res, x);
+    bn_to_bytes_be4(res + (uint32_t)32U, y);
+}
+
+static inline void
+make_prime(uint64_t *n)
+{
+    n[0U] = (uint64_t)0xffffffffffffffffU;
+    n[1U] = (uint64_t)0xffffffffU;
+    n[2U] = (uint64_t)0x0U;
+    n[3U] = (uint64_t)0xffffffff00000001U;
+}
+
+static inline void
+make_order(uint64_t *n)
+{
+    n[0U] = (uint64_t)0xf3b9cac2fc632551U;
+    n[1U] = (uint64_t)0xbce6faada7179e84U;
+    n[2U] = (uint64_t)0xffffffffffffffffU;
+    n[3U] = (uint64_t)0xffffffff00000000U;
+}
+
+static inline void
+make_a_coeff(uint64_t *a)
+{
+    a[0U] = (uint64_t)0xfffffffffffffffcU;
+    a[1U] = (uint64_t)0x3ffffffffU;
+    a[2U] = (uint64_t)0x0U;
+    a[3U] = (uint64_t)0xfffffffc00000004U;
+}
+
+static inline void
+make_b_coeff(uint64_t *b)
+{
+    b[0U] = (uint64_t)0xd89cdf6229c4bddfU;
+    b[1U] = (uint64_t)0xacf005cd78843090U;
+    b[2U] = (uint64_t)0xe5a220abf7212ed6U;
+    b[3U] = (uint64_t)0xdc30061d04874834U;
+}
+
+static inline void
+make_g_x(uint64_t *n)
+{
+    n[0U] = (uint64_t)0x79e730d418a9143cU;
+    n[1U] = (uint64_t)0x75ba95fc5fedb601U;
+    n[2U] = (uint64_t)0x79fb732b77622510U;
+    n[3U] = (uint64_t)0x18905f76a53755c6U;
+}
+
+static inline void
+make_g_y(uint64_t *n)
+{
+    n[0U] = (uint64_t)0xddf25357ce95560aU;
+    n[1U] = (uint64_t)0x8b4ab8e4ba19e45cU;
+    n[2U] = (uint64_t)0xd2e88688dd21f325U;
+    n[3U] = (uint64_t)0x8571ff1825885d85U;
+}
+
+static inline void
+make_fmont_R2(uint64_t *n)
+{
+    n[0U] = (uint64_t)0x3U;
+    n[1U] = (uint64_t)0xfffffffbffffffffU;
+    n[2U] = (uint64_t)0xfffffffffffffffeU;
+    n[3U] = (uint64_t)0x4fffffffdU;
+}
+
+static inline void
+make_fzero(uint64_t *n)
+{
+    n[0U] = (uint64_t)0U;
+    n[1U] = (uint64_t)0U;
+    n[2U] = (uint64_t)0U;
+    n[3U] = (uint64_t)0U;
+}
+
+static inline void
+make_fone(uint64_t *n)
+{
+    n[0U] = (uint64_t)0x1U;
+    n[1U] = (uint64_t)0xffffffff00000000U;
+    n[2U] = (uint64_t)0xffffffffffffffffU;
+    n[3U] = (uint64_t)0xfffffffeU;
+}
+
+static inline uint64_t
+bn_is_lt_prime_mask4(uint64_t *f)
+{
+    uint64_t tmp[4U] = { 0U };
+    make_prime(tmp);
+    uint64_t c = bn_sub4(tmp, f, tmp);
+    return (uint64_t)0U - c;
+}
+
+static inline uint64_t
+feq_mask(uint64_t *a, uint64_t *b)
+{
+    uint64_t r = bn_is_eq_mask4(a, b);
+    return r;
+}
+
+static inline void
+fadd0(uint64_t *res, uint64_t *x, uint64_t *y)
+{
+    uint64_t n[4U] = { 0U };
+    make_prime(n);
+    bn_add_mod4(res, n, x, y);
+}
+
+static inline void
+fsub0(uint64_t *res, uint64_t *x, uint64_t *y)
+{
+    uint64_t n[4U] = { 0U };
+    make_prime(n);
+    bn_sub_mod4(res, n, x, y);
+}
+
+static inline void
+fnegate_conditional_vartime(uint64_t *f, bool is_negate)
+{
+    uint64_t zero[4U] = { 0U };
+    if (is_negate) {
+        fsub0(f, zero, f);
+    }
+}
+
+static inline void
+mont_reduction(uint64_t *res, uint64_t *x)
+{
+    uint64_t n[4U] = { 0U };
+    make_prime(n);
+    uint64_t c0 = (uint64_t)0U;
+    KRML_MAYBE_FOR4(
+        i0,
+        (uint32_t)0U,
+        (uint32_t)4U,
+        (uint32_t)1U,
+        uint64_t qj = (uint64_t)1U * x[i0];
+        uint64_t *res_j0 = x + i0;
+        uint64_t c = (uint64_t)0U;
+        {
+            uint64_t a_i = n[(uint32_t)4U * (uint32_t)0U];
+            uint64_t *res_i0 = res_j0 + (uint32_t)4U * (uint32_t)0U;
+            c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, qj, c, res_i0);
+            uint64_t a_i0 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U];
+            uint64_t *res_i1 = res_j0 + (uint32_t)4U * (uint32_t)0U + (uint32_t)1U;
+            c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i0, qj, c, res_i1);
+            uint64_t a_i1 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U];
+            uint64_t *res_i2 = res_j0 + (uint32_t)4U * (uint32_t)0U + (uint32_t)2U;
+            c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i1, qj, c, res_i2);
+            uint64_t a_i2 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U];
+            uint64_t *res_i = res_j0 + (uint32_t)4U * (uint32_t)0U + (uint32_t)3U;
+            c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i2, qj, c, res_i);
+        } uint64_t r = c;
+        uint64_t c1 = r;
+        uint64_t *resb = x + (uint32_t)4U + i0;
+        uint64_t res_j = x[(uint32_t)4U + i0];
+        c0 = Lib_IntTypes_Intrinsics_add_carry_u64(c0, c1, res_j, resb););
+    memcpy(res, x + (uint32_t)4U, (uint32_t)4U * sizeof(uint64_t));
+    uint64_t c00 = c0;
+    uint64_t tmp[4U] = { 0U };
+    uint64_t c = (uint64_t)0U;
+    {
+        uint64_t t1 = res[(uint32_t)4U * (uint32_t)0U];
+        uint64_t t20 = n[(uint32_t)4U * (uint32_t)0U];
+        uint64_t *res_i0 = tmp + (uint32_t)4U * (uint32_t)0U;
+        c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t1, t20, res_i0);
+        uint64_t t10 = res[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U];
+        uint64_t t21 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U];
+        uint64_t *res_i1 = tmp + (uint32_t)4U * (uint32_t)0U + (uint32_t)1U;
+        c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t10, t21, res_i1);
+        uint64_t t11 = res[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U];
+        uint64_t t22 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U];
+        uint64_t *res_i2 = tmp + (uint32_t)4U * (uint32_t)0U + (uint32_t)2U;
+        c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t11, t22, res_i2);
+        uint64_t t12 = res[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U];
+        uint64_t t2 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U];
+        uint64_t *res_i = tmp + (uint32_t)4U * (uint32_t)0U + (uint32_t)3U;
+        c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t12, t2, res_i);
+    }
+    uint64_t c1 = c;
+    uint64_t c2 = c00 - c1;
+    KRML_MAYBE_FOR4(i,
+                    (uint32_t)0U,
+                    (uint32_t)4U,
+                    (uint32_t)1U,
+                    uint64_t *os = res;
+                    uint64_t x1 = (c2 & res[i]) | (~c2 & tmp[i]);
+                    os[i] = x1;);
+}
+
+static inline void
+fmul0(uint64_t *res, uint64_t *x, uint64_t *y)
+{
+    uint64_t tmp[8U] = { 0U };
+    bn_mul4(tmp, x, y);
+    mont_reduction(res, tmp);
+}
+
+static inline void
+fsqr0(uint64_t *res, uint64_t *x)
+{
+    uint64_t tmp[8U] = { 0U };
+    bn_sqr4(tmp, x);
+    mont_reduction(res, tmp);
+}
+
+static inline void
+from_mont(uint64_t *res, uint64_t *a)
+{
+    uint64_t tmp[8U] = { 0U };
+    memcpy(tmp, a, (uint32_t)4U * sizeof(uint64_t));
+    mont_reduction(res, tmp);
+}
+
+static inline void
+to_mont(uint64_t *res, uint64_t *a)
+{
+    uint64_t r2modn[4U] = { 0U };
+    make_fmont_R2(r2modn);
+    fmul0(res, a, r2modn);
+}
+
+static inline void
+fmul_by_b_coeff(uint64_t *res, uint64_t *x)
+{
+    uint64_t b_coeff[4U] = { 0U };
+    make_b_coeff(b_coeff);
+    fmul0(res, b_coeff, x);
+}
+
+static inline void
+fcube(uint64_t *res, uint64_t *x)
+{
+    fsqr0(res, x);
+    fmul0(res, res, x);
+}
+
+static inline void
+finv(uint64_t *res, uint64_t *a)
+{
+    uint64_t tmp[16U] = { 0U };
+    uint64_t *x30 = tmp;
+    uint64_t *x2 = tmp + (uint32_t)4U;
+    uint64_t *tmp1 = tmp + (uint32_t)8U;
+    uint64_t *tmp2 = tmp + (uint32_t)12U;
+    memcpy(x2, a, (uint32_t)4U * sizeof(uint64_t));
+    {
+        fsqr0(x2, x2);
+    }
+    fmul0(x2, x2, a);
+    memcpy(x30, x2, (uint32_t)4U * sizeof(uint64_t));
+    {
+        fsqr0(x30, x30);
+    }
+    fmul0(x30, x30, a);
+    memcpy(tmp1, x30, (uint32_t)4U * sizeof(uint64_t));
+    KRML_MAYBE_FOR3(i, (uint32_t)0U, (uint32_t)3U, (uint32_t)1U, fsqr0(tmp1, tmp1););
+    fmul0(tmp1, tmp1, x30);
+    memcpy(tmp2, tmp1, (uint32_t)4U * sizeof(uint64_t));
+    KRML_MAYBE_FOR6(i, (uint32_t)0U, (uint32_t)6U, (uint32_t)1U, fsqr0(tmp2, tmp2););
+    fmul0(tmp2, tmp2, tmp1);
+    memcpy(tmp1, tmp2, (uint32_t)4U * sizeof(uint64_t));
+    KRML_MAYBE_FOR3(i, (uint32_t)0U, (uint32_t)3U, (uint32_t)1U, fsqr0(tmp1, tmp1););
+    fmul0(tmp1, tmp1, x30);
+    memcpy(x30, tmp1, (uint32_t)4U * sizeof(uint64_t));
+    KRML_MAYBE_FOR15(i, (uint32_t)0U, (uint32_t)15U, (uint32_t)1U, fsqr0(x30, x30););
+    fmul0(x30, x30, tmp1);
+    memcpy(tmp1, x30, (uint32_t)4U * sizeof(uint64_t));
+    KRML_MAYBE_FOR2(i, (uint32_t)0U, (uint32_t)2U, (uint32_t)1U, fsqr0(tmp1, tmp1););
+    fmul0(tmp1, tmp1, x2);
+    memcpy(x2, tmp1, (uint32_t)4U * sizeof(uint64_t));
+    for (uint32_t i = (uint32_t)0U; i < (uint32_t)32U; i++) {
+        fsqr0(x2, x2);
+    }
+    fmul0(x2, x2, a);
+    for (uint32_t i = (uint32_t)0U; i < (uint32_t)128U; i++) {
+        fsqr0(x2, x2);
+    }
+    fmul0(x2, x2, tmp1);
+    for (uint32_t i = (uint32_t)0U; i < (uint32_t)32U; i++) {
+        fsqr0(x2, x2);
+    }
+    fmul0(x2, x2, tmp1);
+    for (uint32_t i = (uint32_t)0U; i < (uint32_t)30U; i++) {
+        fsqr0(x2, x2);
+    }
+    fmul0(x2, x2, x30);
+    KRML_MAYBE_FOR2(i, (uint32_t)0U, (uint32_t)2U, (uint32_t)1U, fsqr0(x2, x2););
+    fmul0(tmp1, x2, a);
+    memcpy(res, tmp1, (uint32_t)4U * sizeof(uint64_t));
+}
+
+static inline void
+fsqrt(uint64_t *res, uint64_t *a)
+{
+    uint64_t tmp[8U] = { 0U };
+    uint64_t *tmp1 = tmp;
+    uint64_t *tmp2 = tmp + (uint32_t)4U;
+    memcpy(tmp1, a, (uint32_t)4U * sizeof(uint64_t));
+    {
+        fsqr0(tmp1, tmp1);
+    }
+    fmul0(tmp1, tmp1, a);
+    memcpy(tmp2, tmp1, (uint32_t)4U * sizeof(uint64_t));
+    KRML_MAYBE_FOR2(i, (uint32_t)0U, (uint32_t)2U, (uint32_t)1U, fsqr0(tmp2, tmp2););
+    fmul0(tmp2, tmp2, tmp1);
+    memcpy(tmp1, tmp2, (uint32_t)4U * sizeof(uint64_t));
+    KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, fsqr0(tmp1, tmp1););
+    fmul0(tmp1, tmp1, tmp2);
+    memcpy(tmp2, tmp1, (uint32_t)4U * sizeof(uint64_t));
+    KRML_MAYBE_FOR8(i, (uint32_t)0U, (uint32_t)8U, (uint32_t)1U, fsqr0(tmp2, tmp2););
+    fmul0(tmp2, tmp2, tmp1);
+    memcpy(tmp1, tmp2, (uint32_t)4U * sizeof(uint64_t));
+    KRML_MAYBE_FOR16(i, (uint32_t)0U, (uint32_t)16U, (uint32_t)1U, fsqr0(tmp1, tmp1););
+    fmul0(tmp1, tmp1, tmp2);
+    memcpy(tmp2, tmp1, (uint32_t)4U * sizeof(uint64_t));
+    for (uint32_t i = (uint32_t)0U; i < (uint32_t)32U; i++) {
+        fsqr0(tmp2, tmp2);
+    }
+    fmul0(tmp2, tmp2, a);
+    for (uint32_t i = (uint32_t)0U; i < (uint32_t)96U; i++) {
+        fsqr0(tmp2, tmp2);
+    }
+    fmul0(tmp2, tmp2, a);
+    for (uint32_t i = (uint32_t)0U; i < (uint32_t)94U; i++) {
+        fsqr0(tmp2, tmp2);
+    }
+    memcpy(res, tmp2, (uint32_t)4U * sizeof(uint64_t));
+}
+
+static inline void
+make_base_point(uint64_t *p)
+{
+    uint64_t *x = p;
+    uint64_t *y = p + (uint32_t)4U;
+    uint64_t *z = p + (uint32_t)8U;
+    make_g_x(x);
+    make_g_y(y);
+    make_fone(z);
+}
+
+static inline void
+make_point_at_inf(uint64_t *p)
+{
+    uint64_t *x = p;
+    uint64_t *y = p + (uint32_t)4U;
+    uint64_t *z = p + (uint32_t)8U;
+    make_fzero(x);
+    make_fone(y);
+    make_fzero(z);
+}
+
+static inline bool
+is_point_at_inf_vartime(uint64_t *p)
+{
+    uint64_t *pz = p + (uint32_t)8U;
+    return bn_is_zero_vartime4(pz);
+}
+
+static inline void
+to_aff_point(uint64_t *res, uint64_t *p)
+{
+    uint64_t zinv[4U] = { 0U };
+    uint64_t *px = p;
+    uint64_t *py = p + (uint32_t)4U;
+    uint64_t *pz = p + (uint32_t)8U;
+    uint64_t *x = res;
+    uint64_t *y = res + (uint32_t)4U;
+    finv(zinv, pz);
+    fmul0(x, px, zinv);
+    fmul0(y, py, zinv);
+    from_mont(x, x);
+    from_mont(y, y);
+}
+
+static inline void
+to_aff_point_x(uint64_t *res, uint64_t *p)
+{
+    uint64_t zinv[4U] = { 0U };
+    uint64_t *px = p;
+    uint64_t *pz = p + (uint32_t)8U;
+    finv(zinv, pz);
+    fmul0(res, px, zinv);
+    from_mont(res, res);
+}
+
+static inline void
+to_proj_point(uint64_t *res, uint64_t *p)
+{
+    uint64_t *px = p;
+    uint64_t *py = p + (uint32_t)4U;
+    uint64_t *rx = res;
+    uint64_t *ry = res + (uint32_t)4U;
+    uint64_t *rz = res + (uint32_t)8U;
+    to_mont(rx, px);
+    to_mont(ry, py);
+    make_fone(rz);
+}
+
+static inline bool
+is_on_curve_vartime(uint64_t *p)
+{
+    uint64_t rp[4U] = { 0U };
+    uint64_t tx[4U] = { 0U };
+    uint64_t ty[4U] = { 0U };
+    uint64_t *px = p;
+    uint64_t *py = p + (uint32_t)4U;
+    to_mont(tx, px);
+    to_mont(ty, py);
+    uint64_t tmp[4U] = { 0U };
+    fcube(rp, tx);
+    make_a_coeff(tmp);
+    fmul0(tmp, tmp, tx);
+    fadd0(rp, tmp, rp);
+    make_b_coeff(tmp);
+    fadd0(rp, tmp, rp);
+    fsqr0(ty, ty);
+    uint64_t r = feq_mask(ty, rp);
+    bool r0 = r == (uint64_t)0xFFFFFFFFFFFFFFFFU;
+    return r0;
+}
+
+static inline void
+aff_point_store(uint8_t *res, uint64_t *p)
+{
+    uint64_t *px = p;
+    uint64_t *py = p + (uint32_t)4U;
+    bn2_to_bytes_be4(res, px, py);
+}
+
+static inline void
+point_store(uint8_t *res, uint64_t *p)
+{
+    uint64_t aff_p[8U] = { 0U };
+    to_aff_point(aff_p, p);
+    aff_point_store(res, aff_p);
+}
+
+static inline bool
+aff_point_load_vartime(uint64_t *p, uint8_t *b)
+{
+    uint8_t *p_x = b;
+    uint8_t *p_y = b + (uint32_t)32U;
+    uint64_t *bn_p_x = p;
+    uint64_t *bn_p_y = p + (uint32_t)4U;
+    bn_from_bytes_be4(bn_p_x, p_x);
+    bn_from_bytes_be4(bn_p_y, p_y);
+    uint64_t *px = p;
+    uint64_t *py = p + (uint32_t)4U;
+    uint64_t lessX = bn_is_lt_prime_mask4(px);
+    uint64_t lessY = bn_is_lt_prime_mask4(py);
+    uint64_t res = lessX & lessY;
+    bool is_xy_valid = res == (uint64_t)0xFFFFFFFFFFFFFFFFU;
+    if (!is_xy_valid) {
+        return false;
+    }
+    return is_on_curve_vartime(p);
+}
+
+static inline bool
+load_point_vartime(uint64_t *p, uint8_t *b)
+{
+    uint64_t p_aff[8U] = { 0U };
+    bool res = aff_point_load_vartime(p_aff, b);
+    if (res) {
+        to_proj_point(p, p_aff);
+    }
+    return res;
+}
+
+static inline bool
+aff_point_decompress_vartime(uint64_t *x, uint64_t *y, uint8_t *s)
+{
+    uint8_t s0 = s[0U];
+    uint8_t s01 = s0;
+    if (!(s01 == (uint8_t)0x02U || s01 == (uint8_t)0x03U)) {
+        return false;
+    }
+    uint8_t *xb = s + (uint32_t)1U;
+    bn_from_bytes_be4(x, xb);
+    uint64_t is_x_valid = bn_is_lt_prime_mask4(x);
+    bool is_x_valid1 = is_x_valid == (uint64_t)0xFFFFFFFFFFFFFFFFU;
+    bool is_y_odd = s01 == (uint8_t)0x03U;
+    if (!is_x_valid1) {
+        return false;
+    }
+    uint64_t y2M[4U] = { 0U };
+    uint64_t xM[4U] = { 0U };
+    uint64_t yM[4U] = { 0U };
+    to_mont(xM, x);
+    uint64_t tmp[4U] = { 0U };
+    fcube(y2M, xM);
+    make_a_coeff(tmp);
+    fmul0(tmp, tmp, xM);
+    fadd0(y2M, tmp, y2M);
+    make_b_coeff(tmp);
+    fadd0(y2M, tmp, y2M);
+    fsqrt(yM, y2M);
+    from_mont(y, yM);
+    fsqr0(yM, yM);
+    uint64_t r = feq_mask(yM, y2M);
+    bool is_y_valid = r == (uint64_t)0xFFFFFFFFFFFFFFFFU;
+    bool is_y_valid0 = is_y_valid;
+    if (!is_y_valid0) {
+        return false;
+    }
+    uint64_t is_y_odd1 = y[0U] & (uint64_t)1U;
+    bool is_y_odd2 = is_y_odd1 == (uint64_t)1U;
+    fnegate_conditional_vartime(y, is_y_odd2 != is_y_odd);
+    return true;
+}
+
+static inline void
+point_double(uint64_t *res, uint64_t *p)
+{
+    uint64_t tmp[20U] = { 0U };
+    uint64_t *x = p;
+    uint64_t *z = p + (uint32_t)8U;
+    uint64_t *x3 = res;
+    uint64_t *y3 = res + (uint32_t)4U;
+    uint64_t *z3 = res + (uint32_t)8U;
+    uint64_t *t0 = tmp;
+    uint64_t *t1 = tmp + (uint32_t)4U;
+    uint64_t *t2 = tmp + (uint32_t)8U;
+    uint64_t *t3 = tmp + (uint32_t)12U;
+    uint64_t *t4 = tmp + (uint32_t)16U;
+    uint64_t *x1 = p;
+    uint64_t *y = p + (uint32_t)4U;
+    uint64_t *z1 = p + (uint32_t)8U;
+    fsqr0(t0, x1);
+    fsqr0(t1, y);
+    fsqr0(t2, z1);
+    fmul0(t3, x1, y);
+    fadd0(t3, t3, t3);
+    fmul0(t4, y, z1);
+    fmul0(z3, x, z);
+    fadd0(z3, z3, z3);
+    fmul_by_b_coeff(y3, t2);
+    fsub0(y3, y3, z3);
+    fadd0(x3, y3, y3);
+    fadd0(y3, x3, y3);
+    fsub0(x3, t1, y3);
+    fadd0(y3, t1, y3);
+    fmul0(y3, x3, y3);
+    fmul0(x3, x3, t3);
+    fadd0(t3, t2, t2);
+    fadd0(t2, t2, t3);
+    fmul_by_b_coeff(z3, z3);
+    fsub0(z3, z3, t2);
+    fsub0(z3, z3, t0);
+    fadd0(t3, z3, z3);
+    fadd0(z3, z3, t3);
+    fadd0(t3, t0, t0);
+    fadd0(t0, t3, t0);
+    fsub0(t0, t0, t2);
+    fmul0(t0, t0, z3);
+    fadd0(y3, y3, t0);
+    fadd0(t0, t4, t4);
+    fmul0(z3, t0, z3);
+    fsub0(x3, x3, z3);
+    fmul0(z3, t0, t1);
+    fadd0(z3, z3, z3);
+    fadd0(z3, z3, z3);
+}
+
+static inline void
+point_add(uint64_t *res, uint64_t *p, uint64_t *q)
+{
+    uint64_t tmp[36U] = { 0U };
+    uint64_t *t0 = tmp;
+    uint64_t *t1 = tmp + (uint32_t)24U;
+    uint64_t *x3 = t1;
+    uint64_t *y3 = t1 + (uint32_t)4U;
+    uint64_t *z3 = t1 + (uint32_t)8U;
+    uint64_t *t01 = t0;
+    uint64_t *t11 = t0 + (uint32_t)4U;
+    uint64_t *t2 = t0 + (uint32_t)8U;
+    uint64_t *t3 = t0 + (uint32_t)12U;
+    uint64_t *t4 = t0 + (uint32_t)16U;
+    uint64_t *t5 = t0 + (uint32_t)20U;
+    uint64_t *x1 = p;
+    uint64_t *y1 = p + (uint32_t)4U;
+    uint64_t *z10 = p + (uint32_t)8U;
+    uint64_t *x20 = q;
+    uint64_t *y20 = q + (uint32_t)4U;
+    uint64_t *z20 = q + (uint32_t)8U;
+    fmul0(t01, x1, x20);
+    fmul0(t11, y1, y20);
+    fmul0(t2, z10, z20);
+    fadd0(t3, x1, y1);
+    fadd0(t4, x20, y20);
+    fmul0(t3, t3, t4);
+    fadd0(t4, t01, t11);
+    uint64_t *y10 = p + (uint32_t)4U;
+    uint64_t *z11 = p + (uint32_t)8U;
+    uint64_t *y2 = q + (uint32_t)4U;
+    uint64_t *z21 = q + (uint32_t)8U;
+    fsub0(t3, t3, t4);
+    fadd0(t4, y10, z11);
+    fadd0(t5, y2, z21);
+    fmul0(t4, t4, t5);
+    fadd0(t5, t11, t2);
+    fsub0(t4, t4, t5);
+    uint64_t *x10 = p;
+    uint64_t *z1 = p + (uint32_t)8U;
+    uint64_t *x2 = q;
+    uint64_t *z2 = q + (uint32_t)8U;
+    fadd0(x3, x10, z1);
+    fadd0(y3, x2, z2);
+    fmul0(x3, x3, y3);
+    fadd0(y3, t01, t2);
+    fsub0(y3, x3, y3);
+    fmul_by_b_coeff(z3, t2);
+    fsub0(x3, y3, z3);
+    fadd0(z3, x3, x3);
+    fadd0(x3, x3, z3);
+    fsub0(z3, t11, x3);
+    fadd0(x3, t11, x3);
+    fmul_by_b_coeff(y3, y3);
+    fadd0(t11, t2, t2);
+    fadd0(t2, t11, t2);
+    fsub0(y3, y3, t2);
+    fsub0(y3, y3, t01);
+    fadd0(t11, y3, y3);
+    fadd0(y3, t11, y3);
+    fadd0(t11, t01, t01);
+    fadd0(t01, t11, t01);
+    fsub0(t01, t01, t2);
+    fmul0(t11, t4, y3);
+    fmul0(t2, t01, y3);
+    fmul0(y3, x3, z3);
+    fadd0(y3, y3, t2);
+    fmul0(x3, t3, x3);
+    fsub0(x3, x3, t11);
+    fmul0(z3, t4, z3);
+    fmul0(t11, t3, t01);
+    fadd0(z3, z3, t11);
+    memcpy(res, t1, (uint32_t)12U * sizeof(uint64_t));
+}
+
+static inline void
+point_mul(uint64_t *res, uint64_t *scalar, uint64_t *p)
+{
+    uint64_t table[192U] = { 0U };
+    uint64_t tmp[12U] = { 0U };
+    uint64_t *t0 = table;
+    uint64_t *t1 = table + (uint32_t)12U;
+    make_point_at_inf(t0);
+    memcpy(t1, p, (uint32_t)12U * sizeof(uint64_t));
+    KRML_MAYBE_FOR7(i,
+                    (uint32_t)0U,
+                    (uint32_t)7U,
+                    (uint32_t)1U,
+                    uint64_t *t11 = table + (i + (uint32_t)1U) * (uint32_t)12U;
+                    point_double(tmp, t11);
+                    memcpy(table + ((uint32_t)2U * i + (uint32_t)2U) * (uint32_t)12U,
+                           tmp,
+                           (uint32_t)12U * sizeof(uint64_t));
+                    uint64_t *t2 = table + ((uint32_t)2U * i + (uint32_t)2U) * (uint32_t)12U;
+                    point_add(tmp, p, t2);
+                    memcpy(table + ((uint32_t)2U * i + (uint32_t)3U) * (uint32_t)12U,
+                           tmp,
+                           (uint32_t)12U * sizeof(uint64_t)););
+    make_point_at_inf(res);
+    uint64_t tmp0[12U] = { 0U };
+    for (uint32_t i0 = (uint32_t)0U; i0 < (uint32_t)64U; i0++) {
+        KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, point_double(res, res););
+        uint32_t k = (uint32_t)256U - (uint32_t)4U * i0 - (uint32_t)4U;
+        uint64_t bits_l = Hacl_Bignum_Lib_bn_get_bits_u64((uint32_t)4U, scalar, k, (uint32_t)4U);
+        memcpy(tmp0, (uint64_t *)table, (uint32_t)12U * sizeof(uint64_t));
+        KRML_MAYBE_FOR15(i1,
+                         (uint32_t)0U,
+                         (uint32_t)15U,
+                         (uint32_t)1U,
+                         uint64_t c = FStar_UInt64_eq_mask(bits_l, (uint64_t)(i1 + (uint32_t)1U));
+                         const uint64_t *res_j = table + (i1 + (uint32_t)1U) * (uint32_t)12U;
+                         KRML_MAYBE_FOR12(i,
+                                          (uint32_t)0U,
+                                          (uint32_t)12U,
+                                          (uint32_t)1U,
+                                          uint64_t *os = tmp0;
+                                          uint64_t x = (c & res_j[i]) | (~c & tmp0[i]);
+                                          os[i] = x;););
+        point_add(res, res, tmp0);
+    }
+}
+
+static inline void
+precomp_get_consttime(const uint64_t *table, uint64_t bits_l, uint64_t *tmp)
+{
+    memcpy(tmp, (uint64_t *)table, (uint32_t)12U * sizeof(uint64_t));
+    KRML_MAYBE_FOR15(i0,
+                     (uint32_t)0U,
+                     (uint32_t)15U,
+                     (uint32_t)1U,
+                     uint64_t c = FStar_UInt64_eq_mask(bits_l, (uint64_t)(i0 + (uint32_t)1U));
+                     const uint64_t *res_j = table + (i0 + (uint32_t)1U) * (uint32_t)12U;
+                     KRML_MAYBE_FOR12(i,
+                                      (uint32_t)0U,
+                                      (uint32_t)12U,
+                                      (uint32_t)1U,
+                                      uint64_t *os = tmp;
+                                      uint64_t x = (c & res_j[i]) | (~c & tmp[i]);
+                                      os[i] = x;););
+}
+
+static inline void
+point_mul_g(uint64_t *res, uint64_t *scalar)
+{
+    uint64_t q1[12U] = { 0U };
+    make_base_point(q1);
+    /*
+    uint64_t
+    q2[12U] =
+      {
+        (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
+    q3[12U] =
+      {
+        (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
+    q4[12U] =
+      {
+        (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 *r1 = scalar;
+    uint64_t *r2 = scalar + (uint32_t)1U;
+    uint64_t *r3 = scalar + (uint32_t)2U;
+    uint64_t *r4 = scalar + (uint32_t)3U;
+    make_point_at_inf(res);
+    uint64_t tmp[12U] = { 0U };
+    KRML_MAYBE_FOR16(i,
+                     (uint32_t)0U,
+                     (uint32_t)16U,
+                     (uint32_t)1U,
+                     KRML_MAYBE_FOR4(i0, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, point_double(res, res););
+                     uint32_t k = (uint32_t)64U - (uint32_t)4U * i - (uint32_t)4U;
+                     uint64_t bits_l = Hacl_Bignum_Lib_bn_get_bits_u64((uint32_t)1U, r4, k, (uint32_t)4U);
+                     precomp_get_consttime(Hacl_P256_PrecompTable_precomp_g_pow2_192_table_w4, bits_l, tmp);
+                     point_add(res, res, tmp);
+                     uint32_t k0 = (uint32_t)64U - (uint32_t)4U * i - (uint32_t)4U;
+                     uint64_t bits_l0 = Hacl_Bignum_Lib_bn_get_bits_u64((uint32_t)1U, r3, k0, (uint32_t)4U);
+                     precomp_get_consttime(Hacl_P256_PrecompTable_precomp_g_pow2_128_table_w4, bits_l0, tmp);
+                     point_add(res, res, tmp);
+                     uint32_t k1 = (uint32_t)64U - (uint32_t)4U * i - (uint32_t)4U;
+                     uint64_t bits_l1 = Hacl_Bignum_Lib_bn_get_bits_u64((uint32_t)1U, r2, k1, (uint32_t)4U);
+                     precomp_get_consttime(Hacl_P256_PrecompTable_precomp_g_pow2_64_table_w4, bits_l1, tmp);
+                     point_add(res, res, tmp);
+                     uint32_t k2 = (uint32_t)64U - (uint32_t)4U * i - (uint32_t)4U;
+                     uint64_t bits_l2 = Hacl_Bignum_Lib_bn_get_bits_u64((uint32_t)1U, r1, k2, (uint32_t)4U);
+                     precomp_get_consttime(Hacl_P256_PrecompTable_precomp_basepoint_table_w4, bits_l2, tmp);
+                     point_add(res, res, tmp););
+}
+
+static inline void
+point_mul_double_g(uint64_t *res, uint64_t *scalar1, uint64_t *scalar2, uint64_t *q2)
+{
+    uint64_t q1[12U] = { 0U };
+    make_base_point(q1);
+    uint64_t table2[384U] = { 0U };
+    uint64_t tmp[12U] = { 0U };
+    uint64_t *t0 = table2;
+    uint64_t *t1 = table2 + (uint32_t)12U;
+    make_point_at_inf(t0);
+    memcpy(t1, q2, (uint32_t)12U * sizeof(uint64_t));
+    KRML_MAYBE_FOR15(i,
+                     (uint32_t)0U,
+                     (uint32_t)15U,
+                     (uint32_t)1U,
+                     uint64_t *t11 = table2 + (i + (uint32_t)1U) * (uint32_t)12U;
+                     point_double(tmp, t11);
+                     memcpy(table2 + ((uint32_t)2U * i + (uint32_t)2U) * (uint32_t)12U,
+                            tmp,
+                            (uint32_t)12U * sizeof(uint64_t));
+                     uint64_t *t2 = table2 + ((uint32_t)2U * i + (uint32_t)2U) * (uint32_t)12U;
+                     point_add(tmp, q2, t2);
+                     memcpy(table2 + ((uint32_t)2U * i + (uint32_t)3U) * (uint32_t)12U,
+                            tmp,
+                            (uint32_t)12U * sizeof(uint64_t)););
+    uint64_t tmp0[12U] = { 0U };
+    uint32_t i0 = (uint32_t)255U;
+    uint64_t bits_c = Hacl_Bignum_Lib_bn_get_bits_u64((uint32_t)4U, scalar1, i0, (uint32_t)5U);
+    uint32_t bits_l32 = (uint32_t)bits_c;
+    const uint64_t
+        *a_bits_l = Hacl_P256_PrecompTable_precomp_basepoint_table_w5 + bits_l32 * (uint32_t)12U;
+    memcpy(res, (uint64_t *)a_bits_l, (uint32_t)12U * sizeof(uint64_t));
+    uint32_t i1 = (uint32_t)255U;
+    uint64_t bits_c0 = Hacl_Bignum_Lib_bn_get_bits_u64((uint32_t)4U, scalar2, i1, (uint32_t)5U);
+    uint32_t bits_l320 = (uint32_t)bits_c0;
+    const uint64_t *a_bits_l0 = table2 + bits_l320 * (uint32_t)12U;
+    memcpy(tmp0, (uint64_t *)a_bits_l0, (uint32_t)12U * sizeof(uint64_t));
+    point_add(res, res, tmp0);
+    uint64_t tmp1[12U] = { 0U };
+    for (uint32_t i = (uint32_t)0U; i < (uint32_t)51U; i++) {
+        KRML_MAYBE_FOR5(i2, (uint32_t)0U, (uint32_t)5U, (uint32_t)1U, point_double(res, res););
+        uint32_t k = (uint32_t)255U - (uint32_t)5U * i - (uint32_t)5U;
+        uint64_t bits_l = Hacl_Bignum_Lib_bn_get_bits_u64((uint32_t)4U, scalar2, k, (uint32_t)5U);
+        uint32_t bits_l321 = (uint32_t)bits_l;
+        const uint64_t *a_bits_l1 = table2 + bits_l321 * (uint32_t)12U;
+        memcpy(tmp1, (uint64_t *)a_bits_l1, (uint32_t)12U * sizeof(uint64_t));
+        point_add(res, res, tmp1);
+        uint32_t k0 = (uint32_t)255U - (uint32_t)5U * i - (uint32_t)5U;
+        uint64_t bits_l0 = Hacl_Bignum_Lib_bn_get_bits_u64((uint32_t)4U, scalar1, k0, (uint32_t)5U);
+        uint32_t bits_l322 = (uint32_t)bits_l0;
+        const uint64_t
+            *a_bits_l2 = Hacl_P256_PrecompTable_precomp_basepoint_table_w5 + bits_l322 * (uint32_t)12U;
+        memcpy(tmp1, (uint64_t *)a_bits_l2, (uint32_t)12U * sizeof(uint64_t));
+        point_add(res, res, tmp1);
+    }
+}
+
+static inline uint64_t
+bn_is_lt_order_mask4(uint64_t *f)
+{
+    uint64_t tmp[4U] = { 0U };
+    make_order(tmp);
+    uint64_t c = bn_sub4(tmp, f, tmp);
+    return (uint64_t)0U - c;
+}
+
+static inline uint64_t
+bn_is_lt_order_and_gt_zero_mask4(uint64_t *f)
+{
+    uint64_t is_lt_order = bn_is_lt_order_mask4(f);
+    uint64_t is_eq_zero = bn_is_zero_mask4(f);
+    return is_lt_order & ~is_eq_zero;
+}
+
+static inline void
+qmod_short(uint64_t *res, uint64_t *x)
+{
+    uint64_t tmp[4U] = { 0U };
+    make_order(tmp);
+    uint64_t c = bn_sub4(tmp, x, tmp);
+    bn_cmovznz4(res, c, tmp, x);
+}
+
+static inline void
+qadd(uint64_t *res, uint64_t *x, uint64_t *y)
+{
+    uint64_t n[4U] = { 0U };
+    make_order(n);
+    bn_add_mod4(res, n, x, y);
+}
+
+static inline void
+qmont_reduction(uint64_t *res, uint64_t *x)
+{
+    uint64_t n[4U] = { 0U };
+    make_order(n);
+    uint64_t c0 = (uint64_t)0U;
+    KRML_MAYBE_FOR4(
+        i0,
+        (uint32_t)0U,
+        (uint32_t)4U,
+        (uint32_t)1U,
+        uint64_t qj = (uint64_t)0xccd1c8aaee00bc4fU * x[i0];
+        uint64_t *res_j0 = x + i0;
+        uint64_t c = (uint64_t)0U;
+        {
+            uint64_t a_i = n[(uint32_t)4U * (uint32_t)0U];
+            uint64_t *res_i0 = res_j0 + (uint32_t)4U * (uint32_t)0U;
+            c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i, qj, c, res_i0);
+            uint64_t a_i0 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U];
+            uint64_t *res_i1 = res_j0 + (uint32_t)4U * (uint32_t)0U + (uint32_t)1U;
+            c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i0, qj, c, res_i1);
+            uint64_t a_i1 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U];
+            uint64_t *res_i2 = res_j0 + (uint32_t)4U * (uint32_t)0U + (uint32_t)2U;
+            c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i1, qj, c, res_i2);
+            uint64_t a_i2 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U];
+            uint64_t *res_i = res_j0 + (uint32_t)4U * (uint32_t)0U + (uint32_t)3U;
+            c = Hacl_Bignum_Base_mul_wide_add2_u64(a_i2, qj, c, res_i);
+        } uint64_t r = c;
+        uint64_t c1 = r;
+        uint64_t *resb = x + (uint32_t)4U + i0;
+        uint64_t res_j = x[(uint32_t)4U + i0];
+        c0 = Lib_IntTypes_Intrinsics_add_carry_u64(c0, c1, res_j, resb););
+    memcpy(res, x + (uint32_t)4U, (uint32_t)4U * sizeof(uint64_t));
+    uint64_t c00 = c0;
+    uint64_t tmp[4U] = { 0U };
+    uint64_t c = (uint64_t)0U;
+    {
+        uint64_t t1 = res[(uint32_t)4U * (uint32_t)0U];
+        uint64_t t20 = n[(uint32_t)4U * (uint32_t)0U];
+        uint64_t *res_i0 = tmp + (uint32_t)4U * (uint32_t)0U;
+        c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t1, t20, res_i0);
+        uint64_t t10 = res[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U];
+        uint64_t t21 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)1U];
+        uint64_t *res_i1 = tmp + (uint32_t)4U * (uint32_t)0U + (uint32_t)1U;
+        c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t10, t21, res_i1);
+        uint64_t t11 = res[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U];
+        uint64_t t22 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)2U];
+        uint64_t *res_i2 = tmp + (uint32_t)4U * (uint32_t)0U + (uint32_t)2U;
+        c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t11, t22, res_i2);
+        uint64_t t12 = res[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U];
+        uint64_t t2 = n[(uint32_t)4U * (uint32_t)0U + (uint32_t)3U];
+        uint64_t *res_i = tmp + (uint32_t)4U * (uint32_t)0U + (uint32_t)3U;
+        c = Lib_IntTypes_Intrinsics_sub_borrow_u64(c, t12, t2, res_i);
+    }
+    uint64_t c1 = c;
+    uint64_t c2 = c00 - c1;
+    KRML_MAYBE_FOR4(i,
+                    (uint32_t)0U,
+                    (uint32_t)4U,
+                    (uint32_t)1U,
+                    uint64_t *os = res;
+                    uint64_t x1 = (c2 & res[i]) | (~c2 & tmp[i]);
+                    os[i] = x1;);
+}
+
+static inline void
+from_qmont(uint64_t *res, uint64_t *x)
+{
+    uint64_t tmp[8U] = { 0U };
+    memcpy(tmp, x, (uint32_t)4U * sizeof(uint64_t));
+    qmont_reduction(res, tmp);
+}
+
+static inline void
+qmul(uint64_t *res, uint64_t *x, uint64_t *y)
+{
+    uint64_t tmp[8U] = { 0U };
+    bn_mul4(tmp, x, y);
+    qmont_reduction(res, tmp);
+}
+
+static inline void
+qsqr(uint64_t *res, uint64_t *x)
+{
+    uint64_t tmp[8U] = { 0U };
+    bn_sqr4(tmp, x);
+    qmont_reduction(res, tmp);
+}
+
+bool
+Hacl_Impl_P256_DH_ecp256dh_i(uint8_t *public_key, uint8_t *private_key)
+{
+    uint64_t tmp[16U] = { 0U };
+    uint64_t *sk = tmp;
+    uint64_t *pk = tmp + (uint32_t)4U;
+    bn_from_bytes_be4(sk, private_key);
+    uint64_t is_b_valid = bn_is_lt_order_and_gt_zero_mask4(sk);
+    uint64_t oneq[4U] = { 0U };
+    oneq[0U] = (uint64_t)1U;
+    oneq[1U] = (uint64_t)0U;
+    oneq[2U] = (uint64_t)0U;
+    oneq[3U] = (uint64_t)0U;
+    KRML_MAYBE_FOR4(i,
+                    (uint32_t)0U,
+                    (uint32_t)4U,
+                    (uint32_t)1U,
+                    uint64_t *os = sk;
+                    uint64_t uu____0 = oneq[i];
+                    uint64_t x = uu____0 ^ (is_b_valid & (sk[i] ^ uu____0));
+                    os[i] = x;);
+    uint64_t is_sk_valid = is_b_valid;
+    point_mul_g(pk, sk);
+    point_store(public_key, pk);
+    return is_sk_valid == (uint64_t)0xFFFFFFFFFFFFFFFFU;
+}
+
+bool
+Hacl_Impl_P256_DH_ecp256dh_r(
+    uint8_t *shared_secret,
+    uint8_t *their_pubkey,
+    uint8_t *private_key)
+{
+    uint64_t tmp[16U] = { 0U };
+    uint64_t *sk = tmp;
+    uint64_t *pk = tmp + (uint32_t)4U;
+    bool is_pk_valid = load_point_vartime(pk, their_pubkey);
+    bn_from_bytes_be4(sk, private_key);
+    uint64_t is_b_valid = bn_is_lt_order_and_gt_zero_mask4(sk);
+    uint64_t oneq[4U] = { 0U };
+    oneq[0U] = (uint64_t)1U;
+    oneq[1U] = (uint64_t)0U;
+    oneq[2U] = (uint64_t)0U;
+    oneq[3U] = (uint64_t)0U;
+    KRML_MAYBE_FOR4(i,
+                    (uint32_t)0U,
+                    (uint32_t)4U,
+                    (uint32_t)1U,
+                    uint64_t *os = sk;
+                    uint64_t uu____0 = oneq[i];
+                    uint64_t x = uu____0 ^ (is_b_valid & (sk[i] ^ uu____0));
+                    os[i] = x;);
+    uint64_t is_sk_valid = is_b_valid;
+    uint64_t ss_proj[12U] = { 0U };
+    if (is_pk_valid) {
+        point_mul(ss_proj, sk, pk);
+        point_store(shared_secret, ss_proj);
+    }
+    return is_sk_valid == (uint64_t)0xFFFFFFFFFFFFFFFFU && is_pk_valid;
+}
+
+static inline void
+qinv(uint64_t *res, uint64_t *r)
+{
+    uint64_t tmp[28U] = { 0U };
+    uint64_t *x6 = tmp;
+    uint64_t *x_11 = tmp + (uint32_t)4U;
+    uint64_t *x_101 = tmp + (uint32_t)8U;
+    uint64_t *x_111 = tmp + (uint32_t)12U;
+    uint64_t *x_1111 = tmp + (uint32_t)16U;
+    uint64_t *x_10101 = tmp + (uint32_t)20U;
+    uint64_t *x_101111 = tmp + (uint32_t)24U;
+    memcpy(x6, r, (uint32_t)4U * sizeof(uint64_t));
+    {
+        qsqr(x6, x6);
+    }
+    qmul(x_11, x6, r);
+    qmul(x_101, x6, x_11);
+    qmul(x_111, x6, x_101);
+    memcpy(x6, x_101, (uint32_t)4U * sizeof(uint64_t));
+    {
+        qsqr(x6, x6);
+    }
+    qmul(x_1111, x_101, x6);
+    {
+        qsqr(x6, x6);
+    }
+    qmul(x_10101, x6, r);
+    memcpy(x6, x_10101, (uint32_t)4U * sizeof(uint64_t));
+    {
+        qsqr(x6, x6);
+    }
+    qmul(x_101111, x_101, x6);
+    qmul(x6, x_10101, x6);
+    uint64_t tmp1[4U] = { 0U };
+    KRML_MAYBE_FOR2(i, (uint32_t)0U, (uint32_t)2U, (uint32_t)1U, qsqr(x6, x6););
+    qmul(x6, x6, x_11);
+    memcpy(tmp1, x6, (uint32_t)4U * sizeof(uint64_t));
+    KRML_MAYBE_FOR8(i, (uint32_t)0U, (uint32_t)8U, (uint32_t)1U, qsqr(tmp1, tmp1););
+    qmul(tmp1, tmp1, x6);
+    memcpy(x6, tmp1, (uint32_t)4U * sizeof(uint64_t));
+    KRML_MAYBE_FOR16(i, (uint32_t)0U, (uint32_t)16U, (uint32_t)1U, qsqr(x6, x6););
+    qmul(x6, x6, tmp1);
+    memcpy(tmp1, x6, (uint32_t)4U * sizeof(uint64_t));
+    for (uint32_t i = (uint32_t)0U; i < (uint32_t)64U; i++) {
+        qsqr(tmp1, tmp1);
+    }
+    qmul(tmp1, tmp1, x6);
+    for (uint32_t i = (uint32_t)0U; i < (uint32_t)32U; i++) {
+        qsqr(tmp1, tmp1);
+    }
+    qmul(tmp1, tmp1, x6);
+    KRML_MAYBE_FOR6(i, (uint32_t)0U, (uint32_t)6U, (uint32_t)1U, qsqr(tmp1, tmp1););
+    qmul(tmp1, tmp1, x_101111);
+    KRML_MAYBE_FOR5(i, (uint32_t)0U, (uint32_t)5U, (uint32_t)1U, qsqr(tmp1, tmp1););
+    qmul(tmp1, tmp1, x_111);
+    KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, qsqr(tmp1, tmp1););
+    qmul(tmp1, tmp1, x_11);
+    KRML_MAYBE_FOR5(i, (uint32_t)0U, (uint32_t)5U, (uint32_t)1U, qsqr(tmp1, tmp1););
+    qmul(tmp1, tmp1, x_1111);
+    KRML_MAYBE_FOR5(i, (uint32_t)0U, (uint32_t)5U, (uint32_t)1U, qsqr(tmp1, tmp1););
+    qmul(tmp1, tmp1, x_10101);
+    KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, qsqr(tmp1, tmp1););
+    qmul(tmp1, tmp1, x_101);
+    KRML_MAYBE_FOR3(i, (uint32_t)0U, (uint32_t)3U, (uint32_t)1U, qsqr(tmp1, tmp1););
+    qmul(tmp1, tmp1, x_101);
+    KRML_MAYBE_FOR3(i, (uint32_t)0U, (uint32_t)3U, (uint32_t)1U, qsqr(tmp1, tmp1););
+    qmul(tmp1, tmp1, x_101);
+    KRML_MAYBE_FOR5(i, (uint32_t)0U, (uint32_t)5U, (uint32_t)1U, qsqr(tmp1, tmp1););
+    qmul(tmp1, tmp1, x_111);
+    KRML_MAYBE_FOR9(i, (uint32_t)0U, (uint32_t)9U, (uint32_t)1U, qsqr(tmp1, tmp1););
+    qmul(tmp1, tmp1, x_101111);
+    KRML_MAYBE_FOR6(i, (uint32_t)0U, (uint32_t)6U, (uint32_t)1U, qsqr(tmp1, tmp1););
+    qmul(tmp1, tmp1, x_1111);
+    KRML_MAYBE_FOR2(i, (uint32_t)0U, (uint32_t)2U, (uint32_t)1U, qsqr(tmp1, tmp1););
+    qmul(tmp1, tmp1, r);
+    KRML_MAYBE_FOR5(i, (uint32_t)0U, (uint32_t)5U, (uint32_t)1U, qsqr(tmp1, tmp1););
+    qmul(tmp1, tmp1, r);
+    KRML_MAYBE_FOR6(i, (uint32_t)0U, (uint32_t)6U, (uint32_t)1U, qsqr(tmp1, tmp1););
+    qmul(tmp1, tmp1, x_1111);
+    KRML_MAYBE_FOR5(i, (uint32_t)0U, (uint32_t)5U, (uint32_t)1U, qsqr(tmp1, tmp1););
+    qmul(tmp1, tmp1, x_111);
+    KRML_MAYBE_FOR4(i, (uint32_t)0U, (uint32_t)4U, (uint32_t)1U, qsqr(tmp1, tmp1););
+    qmul(tmp1, tmp1, x_111);
+    KRML_MAYBE_FOR5(i, (uint32_t)0U, (uint32_t)5U, (uint32_t)1U, qsqr(tmp1, tmp1););
+    qmul(tmp1, tmp1, x_111);
+    KRML_MAYBE_FOR5(i, (uint32_t)0U, (uint32_t)5U, (uint32_t)1U, qsqr(tmp1, tmp1););
+    qmul(tmp1, tmp1, x_101);
+    KRML_MAYBE_FOR3(i, (uint32_t)0U, (uint32_t)3U, (uint32_t)1U, qsqr(tmp1, tmp1););
+    qmul(tmp1, tmp1, x_11);
+    KRML_MAYBE_FOR10(i, (uint32_t)0U, (uint32_t)10U, (uint32_t)1U, qsqr(tmp1, tmp1););
+    qmul(tmp1, tmp1, x_101111);
+    KRML_MAYBE_FOR2(i, (uint32_t)0U, (uint32_t)2U, (uint32_t)1U, qsqr(tmp1, tmp1););
+    qmul(tmp1, tmp1, x_11);
+    KRML_MAYBE_FOR5(i, (uint32_t)0U, (uint32_t)5U, (uint32_t)1U, qsqr(tmp1, tmp1););
+    qmul(tmp1, tmp1, x_11);
+    KRML_MAYBE_FOR5(i, (uint32_t)0U, (uint32_t)5U, (uint32_t)1U, qsqr(tmp1, tmp1););
+    qmul(tmp1, tmp1, x_11);
+    KRML_MAYBE_FOR3(i, (uint32_t)0U, (uint32_t)3U, (uint32_t)1U, qsqr(tmp1, tmp1););
+    qmul(tmp1, tmp1, r);
+    KRML_MAYBE_FOR7(i, (uint32_t)0U, (uint32_t)7U, (uint32_t)1U, qsqr(tmp1, tmp1););
+    qmul(tmp1, tmp1, x_10101);
+    KRML_MAYBE_FOR6(i, (uint32_t)0U, (uint32_t)6U, (uint32_t)1U, qsqr(tmp1, tmp1););
+    qmul(tmp1, tmp1, x_1111);
+    memcpy(x6, tmp1, (uint32_t)4U * sizeof(uint64_t));
+    memcpy(res, x6, (uint32_t)4U * sizeof(uint64_t));
+}
+
+static inline void
+qmul_mont(uint64_t *sinv, uint64_t *b, uint64_t *res)
+{
+    uint64_t tmp[4U] = { 0U };
+    from_qmont(tmp, b);
+    qmul(res, sinv, tmp);
+}
+
+static inline bool
+ecdsa_verify_msg_as_qelem(
+    uint64_t *m_q,
+    uint8_t *public_key,
+    uint8_t *signature_r,
+    uint8_t *signature_s)
+{
+    uint64_t tmp[28U] = { 0U };
+    uint64_t *pk = tmp;
+    uint64_t *r_q = tmp + (uint32_t)12U;
+    uint64_t *s_q = tmp + (uint32_t)16U;
+    uint64_t *u1 = tmp + (uint32_t)20U;
+    uint64_t *u2 = tmp + (uint32_t)24U;
+    bool is_pk_valid = load_point_vartime(pk, public_key);
+    bn_from_bytes_be4(r_q, signature_r);
+    bn_from_bytes_be4(s_q, signature_s);
+    uint64_t is_r_valid = bn_is_lt_order_and_gt_zero_mask4(r_q);
+    uint64_t is_s_valid = bn_is_lt_order_and_gt_zero_mask4(s_q);
+    bool
+        is_rs_valid =
+            is_r_valid == (uint64_t)0xFFFFFFFFFFFFFFFFU && is_s_valid == (uint64_t)0xFFFFFFFFFFFFFFFFU;
+    if (!(is_pk_valid && is_rs_valid)) {
+        return false;
+    }
+    uint64_t sinv[4U] = { 0U };
+    qinv(sinv, s_q);
+    qmul_mont(sinv, m_q, u1);
+    qmul_mont(sinv, r_q, u2);
+    uint64_t res[12U] = { 0U };
+    point_mul_double_g(res, u1, u2, pk);
+    if (is_point_at_inf_vartime(res)) {
+        return false;
+    }
+    uint64_t x[4U] = { 0U };
+    to_aff_point_x(x, res);
+    qmod_short(x, x);
+    bool res1 = bn_is_eq_vartime4(x, r_q);
+    return res1;
+}
+
+static inline bool
+ecdsa_sign_msg_as_qelem(
+    uint8_t *signature,
+    uint64_t *m_q,
+    uint8_t *private_key,
+    uint8_t *nonce)
+{
+    uint64_t rsdk_q[16U] = { 0U };
+    uint64_t *r_q = rsdk_q;
+    uint64_t *s_q = rsdk_q + (uint32_t)4U;
+    uint64_t *d_a = rsdk_q + (uint32_t)8U;
+    uint64_t *k_q = rsdk_q + (uint32_t)12U;
+    bn_from_bytes_be4(d_a, private_key);
+    uint64_t is_b_valid0 = bn_is_lt_order_and_gt_zero_mask4(d_a);
+    uint64_t oneq0[4U] = { 0U };
+    oneq0[0U] = (uint64_t)1U;
+    oneq0[1U] = (uint64_t)0U;
+    oneq0[2U] = (uint64_t)0U;
+    oneq0[3U] = (uint64_t)0U;
+    KRML_MAYBE_FOR4(i,
+                    (uint32_t)0U,
+                    (uint32_t)4U,
+                    (uint32_t)1U,
+                    uint64_t *os = d_a;
+                    uint64_t uu____0 = oneq0[i];
+                    uint64_t x = uu____0 ^ (is_b_valid0 & (d_a[i] ^ uu____0));
+                    os[i] = x;);
+    uint64_t is_sk_valid = is_b_valid0;
+    bn_from_bytes_be4(k_q, nonce);
+    uint64_t is_b_valid = bn_is_lt_order_and_gt_zero_mask4(k_q);
+    uint64_t oneq[4U] = { 0U };
+    oneq[0U] = (uint64_t)1U;
+    oneq[1U] = (uint64_t)0U;
+    oneq[2U] = (uint64_t)0U;
+    oneq[3U] = (uint64_t)0U;
+    KRML_MAYBE_FOR4(i,
+                    (uint32_t)0U,
+                    (uint32_t)4U,
+                    (uint32_t)1U,
+                    uint64_t *os = k_q;
+                    uint64_t uu____1 = oneq[i];
+                    uint64_t x = uu____1 ^ (is_b_valid & (k_q[i] ^ uu____1));
+                    os[i] = x;);
+    uint64_t is_nonce_valid = is_b_valid;
+    uint64_t are_sk_nonce_valid = is_sk_valid & is_nonce_valid;
+    uint64_t p[12U] = { 0U };
+    point_mul_g(p, k_q);
+    to_aff_point_x(r_q, p);
+    qmod_short(r_q, r_q);
+    uint64_t kinv[4U] = { 0U };
+    qinv(kinv, k_q);
+    qmul(s_q, r_q, d_a);
+    from_qmont(m_q, m_q);
+    qadd(s_q, m_q, s_q);
+    qmul(s_q, kinv, s_q);
+    bn2_to_bytes_be4(signature, r_q, s_q);
+    uint64_t is_r_zero = bn_is_zero_mask4(r_q);
+    uint64_t is_s_zero = bn_is_zero_mask4(s_q);
+    uint64_t m = are_sk_nonce_valid & (~is_r_zero & ~is_s_zero);
+    bool res = m == (uint64_t)0xFFFFFFFFFFFFFFFFU;
+    return res;
+}
+
+/*******************************************************************************
+
+ Verified C library for ECDSA and ECDH functions over the P-256 NIST curve.
+
+ This module implements signing and verification, key validation, conversions
+ between various point representations, and ECDH key agreement.
+
+*******************************************************************************/
+
+/*****************/
+/* ECDSA signing */
+/*****************/
+
+/**
+Create an ECDSA signature WITHOUT hashing first.
+
+  This function is intended to receive a hash of the input.
+  For convenience, we recommend using one of the hash-and-sign combined functions above.
+
+  The argument `msg` MUST be at least 32 bytes (i.e. `msg_len >= 32`).
+
+  NOTE: The equivalent functions in OpenSSL and Fiat-Crypto both accept inputs
+  smaller than 32 bytes. These libraries left-pad the input with enough zeroes to
+  reach the minimum 32 byte size. Clients who need behavior identical to OpenSSL
+  need to perform the left-padding themselves.
+
+  The function returns `true` for successful creation of an ECDSA signature and `false` otherwise.
+
+  The outparam `signature` (R || S) points to 64 bytes of valid memory, i.e., uint8_t[64].
+  The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].
+  The arguments `private_key` and `nonce` point to 32 bytes of valid memory, i.e., uint8_t[32].
+
+  The function also checks whether `private_key` and `nonce` are valid values:
+    • 0 < `private_key` < the order of the curve
+    • 0 < `nonce` < the order of the curve
+*/
+bool
+Hacl_P256_ecdsa_sign_p256_without_hash(
+    uint8_t *signature,
+    uint32_t msg_len,
+    uint8_t *msg,
+    uint8_t *private_key,
+    uint8_t *nonce)
+{
+    uint64_t m_q[4U] = { 0U };
+    uint8_t mHash[32U] = { 0U };
+    memcpy(mHash, msg, (uint32_t)32U * sizeof(uint8_t));
+    uint8_t *mHash32 = mHash;
+    bn_from_bytes_be4(m_q, mHash32);
+    qmod_short(m_q, m_q);
+    bool res = ecdsa_sign_msg_as_qelem(signature, m_q, private_key, nonce);
+    return res;
+}
+
+/**********************/
+/* ECDSA verification */
+/**********************/
+
+/**
+Verify an ECDSA signature WITHOUT hashing first.
+
+  This function is intended to receive a hash of the input.
+  For convenience, we recommend using one of the hash-and-verify combined functions above.
+
+  The argument `msg` MUST be at least 32 bytes (i.e. `msg_len >= 32`).
+
+  The function returns `true` if the signature is valid and `false` otherwise.
+
+  The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].
+  The argument `public_key` (x || y) points to 64 bytes of valid memory, i.e., uint8_t[64].
+  The arguments `signature_r` and `signature_s` point to 32 bytes of valid memory, i.e., uint8_t[32].
+
+  The function also checks whether `public_key` is valid
+*/
+bool
+Hacl_P256_ecdsa_verif_without_hash(
+    uint32_t msg_len,
+    uint8_t *msg,
+    uint8_t *public_key,
+    uint8_t *signature_r,
+    uint8_t *signature_s)
+{
+    uint64_t m_q[4U] = { 0U };
+    uint8_t mHash[32U] = { 0U };
+    memcpy(mHash, msg, (uint32_t)32U * sizeof(uint8_t));
+    uint8_t *mHash32 = mHash;
+    bn_from_bytes_be4(m_q, mHash32);
+    qmod_short(m_q, m_q);
+    bool res = ecdsa_verify_msg_as_qelem(m_q, public_key, signature_r, signature_s);
+    return res;
+}
+
+/******************/
+/* Key validation */
+/******************/
+
+/**
+Public key validation.
+
+  The function returns `true` if a public key is valid and `false` otherwise.
+
+  The argument `public_key` points to 64 bytes of valid memory, i.e., uint8_t[64].
+
+  The public key (x || y) is valid (with respect to SP 800-56A):
+    • the public key is not the “point at infinity”, represented as O.
+    • the affine x and y coordinates of the point represented by the public key are
+      in the range [0, p – 1] where p is the prime defining the finite field.
+    • y^2 = x^3 + ax + b where a and b are the coefficients of the curve equation.
+  The last extract is taken from: https://neilmadden.blog/2017/05/17/so-how-do-you-validate-nist-ecdh-public-keys/
+*/
+bool
+Hacl_P256_validate_public_key(uint8_t *public_key)
+{
+    uint64_t point_jac[12U] = { 0U };
+    bool res = load_point_vartime(point_jac, public_key);
+    return res;
+}
+
+/**
+Private key validation.
+
+  The function returns `true` if a private key is valid and `false` otherwise.
+
+  The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
+
+  The private key is valid:
+    • 0 < `private_key` < the order of the curve
+*/
+bool
+Hacl_P256_validate_private_key(uint8_t *private_key)
+{
+    uint64_t bn_sk[4U] = { 0U };
+    bn_from_bytes_be4(bn_sk, private_key);
+    uint64_t res = bn_is_lt_order_and_gt_zero_mask4(bn_sk);
+    return res == (uint64_t)0xFFFFFFFFFFFFFFFFU;
+}
+
+/*******************************************************************************
+  Parsing and Serializing public keys.
+
+  A public key is a point (x, y) on the P-256 NIST curve.
+
+  The point can be represented in the following three ways.
+    • raw          = [ x || y ], 64 bytes
+    • uncompressed = [ 0x04 || x || y ], 65 bytes
+    • compressed   = [ (0x02 for even `y` and 0x03 for odd `y`) || x ], 33 bytes
+
+*******************************************************************************/
+
+/**
+Convert a public key from uncompressed to its raw form.
+
+  The function returns `true` for successful conversion of a public key and `false` otherwise.
+
+  The outparam `pk_raw` points to 64 bytes of valid memory, i.e., uint8_t[64].
+  The argument `pk` points to 65 bytes of valid memory, i.e., uint8_t[65].
+
+  The function DOESN'T check whether (x, y) is a valid point.
+*/
+bool
+Hacl_P256_uncompressed_to_raw(uint8_t *pk, uint8_t *pk_raw)
+{
+    uint8_t pk0 = pk[0U];
+    if (pk0 != (uint8_t)0x04U) {
+        return false;
+    }
+    memcpy(pk_raw, pk + (uint32_t)1U, (uint32_t)64U * sizeof(uint8_t));
+    return true;
+}
+
+/**
+Convert a public key from compressed to its raw form.
+
+  The function returns `true` for successful conversion of a public key and `false` otherwise.
+
+  The outparam `pk_raw` points to 64 bytes of valid memory, i.e., uint8_t[64].
+  The argument `pk` points to 33 bytes of valid memory, i.e., uint8_t[33].
+
+  The function also checks whether (x, y) is a valid point.
+*/
+bool
+Hacl_P256_compressed_to_raw(uint8_t *pk, uint8_t *pk_raw)
+{
+    uint64_t xa[4U] = { 0U };
+    uint64_t ya[4U] = { 0U };
+    uint8_t *pk_xb = pk + (uint32_t)1U;
+    bool b = aff_point_decompress_vartime(xa, ya, pk);
+    if (b) {
+        memcpy(pk_raw, pk_xb, (uint32_t)32U * sizeof(uint8_t));
+        bn_to_bytes_be4(pk_raw + (uint32_t)32U, ya);
+    }
+    return b;
+}
+
+/**
+Convert a public key from raw to its uncompressed form.
+
+  The outparam `pk` points to 65 bytes of valid memory, i.e., uint8_t[65].
+  The argument `pk_raw` points to 64 bytes of valid memory, i.e., uint8_t[64].
+
+  The function DOESN'T check whether (x, y) is a valid point.
+*/
+void
+Hacl_P256_raw_to_uncompressed(uint8_t *pk_raw, uint8_t *pk)
+{
+    pk[0U] = (uint8_t)0x04U;
+    memcpy(pk + (uint32_t)1U, pk_raw, (uint32_t)64U * sizeof(uint8_t));
+}
+
+/**
+Convert a public key from raw to its compressed form.
+
+  The outparam `pk` points to 33 bytes of valid memory, i.e., uint8_t[33].
+  The argument `pk_raw` points to 64 bytes of valid memory, i.e., uint8_t[64].
+
+  The function DOESN'T check whether (x, y) is a valid point.
+*/
+void
+Hacl_P256_raw_to_compressed(uint8_t *pk_raw, uint8_t *pk)
+{
+    uint8_t *pk_x = pk_raw;
+    uint8_t *pk_y = pk_raw + (uint32_t)32U;
+    uint64_t bn_f[4U] = { 0U };
+    bn_from_bytes_be4(bn_f, pk_y);
+    uint64_t is_odd_f = bn_f[0U] & (uint64_t)1U;
+    pk[0U] = (uint8_t)is_odd_f + (uint8_t)0x02U;
+    memcpy(pk + (uint32_t)1U, pk_x, (uint32_t)32U * sizeof(uint8_t));
+}
+
+/******************/
+/* ECDH agreement */
+/******************/
+
+/**
+Compute the public key from the private key.
+
+  The function returns `true` if a private key is valid and `false` otherwise.
+
+  The outparam `public_key`  points to 64 bytes of valid memory, i.e., uint8_t[64].
+  The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
+
+  The private key is valid:
+    • 0 < `private_key` < the order of the curve.
+*/
+bool
+Hacl_P256_dh_initiator(uint8_t *public_key, uint8_t *private_key)
+{
+    return Hacl_Impl_P256_DH_ecp256dh_i(public_key, private_key);
+}
+
+/**
+Execute the diffie-hellmann key exchange.
+
+  The function returns `true` for successful creation of an ECDH shared secret and
+  `false` otherwise.
+
+  The outparam `shared_secret` points to 64 bytes of valid memory, i.e., uint8_t[64].
+  The argument `their_pubkey` points to 64 bytes of valid memory, i.e., uint8_t[64].
+  The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
+
+  The function also checks whether `private_key` and `their_pubkey` are valid.
+*/
+bool
+Hacl_P256_dh_responder(uint8_t *shared_secret, uint8_t *their_pubkey, uint8_t *private_key)
+{
+    return Hacl_Impl_P256_DH_ecp256dh_r(shared_secret, their_pubkey, private_key);
+}
+
diff -up ./lib/freebl/verified/Hacl_P256.h.p256 ./lib/freebl/verified/Hacl_P256.h
--- ./lib/freebl/verified/Hacl_P256.h.p256	2024-01-09 11:25:43.803382195 -0800
+++ ./lib/freebl/verified/Hacl_P256.h	2024-01-09 11:25:43.803382195 -0800
@@ -0,0 +1,237 @@
+/* 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 __Hacl_P256_H
+#define __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 "Hacl_Krmllib.h"
+#include "lib_intrinsics.h"
+
+/*******************************************************************************
+
+ Verified C library for ECDSA and ECDH functions over the P-256 NIST curve.
+
+ This module implements signing and verification, key validation, conversions
+ between various point representations, and ECDH key agreement.
+
+*******************************************************************************/
+
+/*****************/
+/* ECDSA signing */
+/*****************/
+
+/**
+Create an ECDSA signature WITHOUT hashing first.
+
+  This function is intended to receive a hash of the input.
+  For convenience, we recommend using one of the hash-and-sign combined functions above.
+
+  The argument `msg` MUST be at least 32 bytes (i.e. `msg_len >= 32`).
+
+  NOTE: The equivalent functions in OpenSSL and Fiat-Crypto both accept inputs
+  smaller than 32 bytes. These libraries left-pad the input with enough zeroes to
+  reach the minimum 32 byte size. Clients who need behavior identical to OpenSSL
+  need to perform the left-padding themselves.
+
+  The function returns `true` for successful creation of an ECDSA signature and `false` otherwise.
+
+  The outparam `signature` (R || S) points to 64 bytes of valid memory, i.e., uint8_t[64].
+  The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].
+  The arguments `private_key` and `nonce` point to 32 bytes of valid memory, i.e., uint8_t[32].
+
+  The function also checks whether `private_key` and `nonce` are valid values:
+    • 0 < `private_key` < the order of the curve
+    • 0 < `nonce` < the order of the curve
+*/
+bool
+Hacl_P256_ecdsa_sign_p256_without_hash(
+    uint8_t *signature,
+    uint32_t msg_len,
+    uint8_t *msg,
+    uint8_t *private_key,
+    uint8_t *nonce);
+
+/**********************/
+/* ECDSA verification */
+/**********************/
+
+/**
+Verify an ECDSA signature WITHOUT hashing first.
+
+  This function is intended to receive a hash of the input.
+  For convenience, we recommend using one of the hash-and-verify combined functions above.
+
+  The argument `msg` MUST be at least 32 bytes (i.e. `msg_len >= 32`).
+
+  The function returns `true` if the signature is valid and `false` otherwise.
+
+  The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].
+  The argument `public_key` (x || y) points to 64 bytes of valid memory, i.e., uint8_t[64].
+  The arguments `signature_r` and `signature_s` point to 32 bytes of valid memory, i.e., uint8_t[32].
+
+  The function also checks whether `public_key` is valid
+*/
+bool
+Hacl_P256_ecdsa_verif_without_hash(
+    uint32_t msg_len,
+    uint8_t *msg,
+    uint8_t *public_key,
+    uint8_t *signature_r,
+    uint8_t *signature_s);
+
+/******************/
+/* Key validation */
+/******************/
+
+/**
+Public key validation.
+
+  The function returns `true` if a public key is valid and `false` otherwise.
+
+  The argument `public_key` points to 64 bytes of valid memory, i.e., uint8_t[64].
+
+  The public key (x || y) is valid (with respect to SP 800-56A):
+    • the public key is not the “point at infinity”, represented as O.
+    • the affine x and y coordinates of the point represented by the public key are
+      in the range [0, p – 1] where p is the prime defining the finite field.
+    • y^2 = x^3 + ax + b where a and b are the coefficients of the curve equation.
+  The last extract is taken from: https://neilmadden.blog/2017/05/17/so-how-do-you-validate-nist-ecdh-public-keys/
+*/
+bool Hacl_P256_validate_public_key(uint8_t *public_key);
+
+/**
+Private key validation.
+
+  The function returns `true` if a private key is valid and `false` otherwise.
+
+  The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
+
+  The private key is valid:
+    • 0 < `private_key` < the order of the curve
+*/
+bool Hacl_P256_validate_private_key(uint8_t *private_key);
+
+/*******************************************************************************
+  Parsing and Serializing public keys.
+
+  A public key is a point (x, y) on the P-256 NIST curve.
+
+  The point can be represented in the following three ways.
+    • raw          = [ x || y ], 64 bytes
+    • uncompressed = [ 0x04 || x || y ], 65 bytes
+    • compressed   = [ (0x02 for even `y` and 0x03 for odd `y`) || x ], 33 bytes
+
+*******************************************************************************/
+
+/**
+Convert a public key from uncompressed to its raw form.
+
+  The function returns `true` for successful conversion of a public key and `false` otherwise.
+
+  The outparam `pk_raw` points to 64 bytes of valid memory, i.e., uint8_t[64].
+  The argument `pk` points to 65 bytes of valid memory, i.e., uint8_t[65].
+
+  The function DOESN'T check whether (x, y) is a valid point.
+*/
+bool Hacl_P256_uncompressed_to_raw(uint8_t *pk, uint8_t *pk_raw);
+
+/**
+Convert a public key from compressed to its raw form.
+
+  The function returns `true` for successful conversion of a public key and `false` otherwise.
+
+  The outparam `pk_raw` points to 64 bytes of valid memory, i.e., uint8_t[64].
+  The argument `pk` points to 33 bytes of valid memory, i.e., uint8_t[33].
+
+  The function also checks whether (x, y) is a valid point.
+*/
+bool Hacl_P256_compressed_to_raw(uint8_t *pk, uint8_t *pk_raw);
+
+/**
+Convert a public key from raw to its uncompressed form.
+
+  The outparam `pk` points to 65 bytes of valid memory, i.e., uint8_t[65].
+  The argument `pk_raw` points to 64 bytes of valid memory, i.e., uint8_t[64].
+
+  The function DOESN'T check whether (x, y) is a valid point.
+*/
+void Hacl_P256_raw_to_uncompressed(uint8_t *pk_raw, uint8_t *pk);
+
+/**
+Convert a public key from raw to its compressed form.
+
+  The outparam `pk` points to 33 bytes of valid memory, i.e., uint8_t[33].
+  The argument `pk_raw` points to 64 bytes of valid memory, i.e., uint8_t[64].
+
+  The function DOESN'T check whether (x, y) is a valid point.
+*/
+void Hacl_P256_raw_to_compressed(uint8_t *pk_raw, uint8_t *pk);
+
+/******************/
+/* ECDH agreement */
+/******************/
+
+/**
+Compute the public key from the private key.
+
+  The function returns `true` if a private key is valid and `false` otherwise.
+
+  The outparam `public_key`  points to 64 bytes of valid memory, i.e., uint8_t[64].
+  The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
+
+  The private key is valid:
+    • 0 < `private_key` < the order of the curve.
+*/
+bool Hacl_P256_dh_initiator(uint8_t *public_key, uint8_t *private_key);
+
+/**
+Execute the diffie-hellmann key exchange.
+
+  The function returns `true` for successful creation of an ECDH shared secret and
+  `false` otherwise.
+
+  The outparam `shared_secret` points to 64 bytes of valid memory, i.e., uint8_t[64].
+  The argument `their_pubkey` points to 64 bytes of valid memory, i.e., uint8_t[64].
+  The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
+
+  The function also checks whether `private_key` and `their_pubkey` are valid.
+*/
+bool
+Hacl_P256_dh_responder(uint8_t *shared_secret, uint8_t *their_pubkey, uint8_t *private_key);
+
+#if defined(__cplusplus)
+}
+#endif
+
+#define __Hacl_P256_H_DEFINED
+#endif
diff -up ./lib/freebl/verified/internal/Hacl_Bignum_Base.h.p256 ./lib/freebl/verified/internal/Hacl_Bignum_Base.h
--- ./lib/freebl/verified/internal/Hacl_Bignum_Base.h.p256	2024-01-09 11:25:43.803382195 -0800
+++ ./lib/freebl/verified/internal/Hacl_Bignum_Base.h	2024-01-09 11:25:43.803382195 -0800
@@ -0,0 +1,114 @@
+/* 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/lowstar_endianness.h"
+#include "krml/internal/target.h"
+
+#include "internal/Hacl_Krmllib.h"
+#include "Hacl_Krmllib.h"
+#include "internal/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 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 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;
+}
+
+#if defined(__cplusplus)
+}
+#endif
+
+#define __internal_Hacl_Bignum_Base_H_DEFINED
+#endif
diff -up ./lib/freebl/verified/internal/Hacl_IntTypes_Intrinsics_128.h.p256 ./lib/freebl/verified/internal/Hacl_IntTypes_Intrinsics_128.h
--- ./lib/freebl/verified/internal/Hacl_IntTypes_Intrinsics_128.h.p256	2024-01-09 11:25:43.803382195 -0800
+++ ./lib/freebl/verified/internal/Hacl_IntTypes_Intrinsics_128.h	2024-01-09 11:25:43.803382195 -0800
@@ -0,0 +1,72 @@
+/* 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 __Hacl_IntTypes_Intrinsics_128_H
+#define __Hacl_IntTypes_Intrinsics_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_Krmllib.h"
+
+static inline uint64_t
+Hacl_IntTypes_Intrinsics_128_add_carry_u64(uint64_t cin, uint64_t x, uint64_t y, uint64_t *r)
+{
+    FStar_UInt128_uint128
+        res =
+            FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_uint64_to_uint128(x),
+                                                        FStar_UInt128_uint64_to_uint128(cin)),
+                                  FStar_UInt128_uint64_to_uint128(y));
+    uint64_t c = FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(res, (uint32_t)64U));
+    r[0U] = FStar_UInt128_uint128_to_uint64(res);
+    return c;
+}
+
+static inline uint64_t
+Hacl_IntTypes_Intrinsics_128_sub_borrow_u64(uint64_t cin, uint64_t x, uint64_t y, uint64_t *r)
+{
+    FStar_UInt128_uint128
+        res =
+            FStar_UInt128_sub_mod(FStar_UInt128_sub_mod(FStar_UInt128_uint64_to_uint128(x),
+                                                        FStar_UInt128_uint64_to_uint128(y)),
+                                  FStar_UInt128_uint64_to_uint128(cin));
+    uint64_t
+        c =
+            FStar_UInt128_uint128_to_uint64(FStar_UInt128_shift_right(res, (uint32_t)64U)) & (uint64_t)1U;
+    r[0U] = FStar_UInt128_uint128_to_uint64(res);
+    return c;
+}
+
+#if defined(__cplusplus)
+}
+#endif
+
+#define __Hacl_IntTypes_Intrinsics_128_H_DEFINED
+#endif
diff -up ./lib/freebl/verified/internal/Hacl_IntTypes_Intrinsics.h.p256 ./lib/freebl/verified/internal/Hacl_IntTypes_Intrinsics.h
--- ./lib/freebl/verified/internal/Hacl_IntTypes_Intrinsics.h.p256	2024-01-09 11:25:43.803382195 -0800
+++ ./lib/freebl/verified/internal/Hacl_IntTypes_Intrinsics.h	2024-01-09 11:25:43.803382195 -0800
@@ -0,0 +1,83 @@
+/* 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 __Hacl_IntTypes_Intrinsics_H
+#define __Hacl_IntTypes_Intrinsics_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 inline uint32_t
+Hacl_IntTypes_Intrinsics_add_carry_u32(uint32_t cin, uint32_t x, uint32_t y, uint32_t *r)
+{
+    uint64_t res = (uint64_t)x + (uint64_t)cin + (uint64_t)y;
+    uint32_t c = (uint32_t)(res >> (uint32_t)32U);
+    r[0U] = (uint32_t)res;
+    return c;
+}
+
+static inline uint32_t
+Hacl_IntTypes_Intrinsics_sub_borrow_u32(uint32_t cin, uint32_t x, uint32_t y, uint32_t *r)
+{
+    uint64_t res = (uint64_t)x - (uint64_t)y - (uint64_t)cin;
+    uint32_t c = (uint32_t)(res >> (uint32_t)32U) & (uint32_t)1U;
+    r[0U] = (uint32_t)res;
+    return c;
+}
+
+static inline uint64_t
+Hacl_IntTypes_Intrinsics_add_carry_u64(uint64_t cin, uint64_t x, uint64_t y, uint64_t *r)
+{
+    uint64_t res = x + cin + y;
+    uint64_t
+        c = (~FStar_UInt64_gte_mask(res, x) | (FStar_UInt64_eq_mask(res, x) & cin)) & (uint64_t)1U;
+    r[0U] = res;
+    return c;
+}
+
+static inline uint64_t
+Hacl_IntTypes_Intrinsics_sub_borrow_u64(uint64_t cin, uint64_t x, uint64_t y, uint64_t *r)
+{
+    uint64_t res = x - y - cin;
+    uint64_t
+        c =
+            ((FStar_UInt64_gte_mask(res, x) & ~FStar_UInt64_eq_mask(res, x)) | (FStar_UInt64_eq_mask(res, x) & cin)) & (uint64_t)1U;
+    r[0U] = res;
+    return c;
+}
+
+#if defined(__cplusplus)
+}
+#endif
+
+#define __Hacl_IntTypes_Intrinsics_H_DEFINED
+#endif
diff -up ./lib/freebl/verified/internal/Hacl_P256.h.p256 ./lib/freebl/verified/internal/Hacl_P256.h
--- ./lib/freebl/verified/internal/Hacl_P256.h.p256	2024-01-09 11:25:43.803382195 -0800
+++ ./lib/freebl/verified/internal/Hacl_P256.h	2024-01-09 11:25:43.803382195 -0800
@@ -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 -up ./lib/freebl/verified/internal/Hacl_P256_PrecompTable.h.p256 ./lib/freebl/verified/internal/Hacl_P256_PrecompTable.h
--- ./lib/freebl/verified/internal/Hacl_P256_PrecompTable.h.p256	2024-01-09 11:25:43.803382195 -0800
+++ ./lib/freebl/verified/internal/Hacl_P256_PrecompTable.h	2024-01-09 11:25:43.803382195 -0800
@@ -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 -up ./lib/freebl/verified/internal/lib_intrinsics.h.p256 ./lib/freebl/verified/internal/lib_intrinsics.h
--- ./lib/freebl/verified/internal/lib_intrinsics.h.p256	2024-01-09 11:25:43.803382195 -0800
+++ ./lib/freebl/verified/internal/lib_intrinsics.h	2024-01-09 11:25:43.803382195 -0800
@@ -0,0 +1,81 @@
+#pragma once
+
+#include <sys/types.h>
+
+#if defined(__has_include)
+#if __has_include("config.h")
+#include "config.h"
+#endif
+#endif
+
+#if !defined(HACL_CAN_COMPILE_INTRINSICS) || \
+    (defined(__clang__) && (__clang_major__ < 5))
+
+#include "Hacl_IntTypes_Intrinsics.h"
+
+#if defined(HACL_CAN_COMPILE_UINT128)
+
+#include "Hacl_IntTypes_Intrinsics_128.h"
+
+#define Lib_IntTypes_Intrinsics_add_carry_u64(x1, x2, x3, x4) \
+    (Hacl_IntTypes_Intrinsics_128_add_carry_u64(x1, x2, x3, x4))
+
+#define Lib_IntTypes_Intrinsics_sub_borrow_u64(x1, x2, x3, x4) \
+    (Hacl_IntTypes_Intrinsics_128_sub_borrow_u64(x1, x2, x3, x4))
+
+#else
+
+#define Lib_IntTypes_Intrinsics_add_carry_u64(x1, x2, x3, x4) \
+    (Hacl_IntTypes_Intrinsics_add_carry_u64(x1, x2, x3, x4))
+
+#define Lib_IntTypes_Intrinsics_sub_borrow_u64(x1, x2, x3, x4) \
+    (Hacl_IntTypes_Intrinsics_sub_borrow_u64(x1, x2, x3, x4))
+
+#endif // defined(HACL_CAN_COMPILE_UINT128)
+
+#define Lib_IntTypes_Intrinsics_add_carry_u32(x1, x2, x3, x4) \
+    (Hacl_IntTypes_Intrinsics_add_carry_u32(x1, x2, x3, x4))
+
+#define Lib_IntTypes_Intrinsics_sub_borrow_u32(x1, x2, x3, x4) \
+    (Hacl_IntTypes_Intrinsics_sub_borrow_u32(x1, x2, x3, x4))
+
+#else // !defined(HACL_CAN_COMPILE_INTRINSICS)
+
+#if defined(_MSC_VER)
+#include <immintrin.h>
+#else
+#include <x86intrin.h>
+#endif
+
+#define Lib_IntTypes_Intrinsics_add_carry_u32(x1, x2, x3, x4) \
+    (_addcarry_u32(x1, x2, x3, (unsigned int *)x4))
+
+#define Lib_IntTypes_Intrinsics_add_carry_u64(x1, x2, x3, x4) \
+    (_addcarry_u64(x1, x2, x3, (long long unsigned int *)x4))
+
+/*
+   GCC versions prior to 7.2 pass arguments to _subborrow_u{32,64}
+   in an incorrect order.
+
+   See https://gcc.gnu.org/bugzilla/show_bug.cgi?id=81294
+*/
+#if defined(__GNUC__) && !defined(__clang__) && \
+    (__GNUC__ < 7 || (__GNUC__ == 7 && (__GNUC_MINOR__ < 2)))
+
+#define Lib_IntTypes_Intrinsics_sub_borrow_u32(x1, x2, x3, x4) \
+    (_subborrow_u32(x1, x3, x2, (unsigned int *)x4))
+
+#define Lib_IntTypes_Intrinsics_sub_borrow_u64(x1, x2, x3, x4) \
+    (_subborrow_u64(x1, x3, x2, (long long unsigned int *)x4))
+
+#else
+
+#define Lib_IntTypes_Intrinsics_sub_borrow_u32(x1, x2, x3, x4) \
+    (_subborrow_u32(x1, x2, x3, (unsigned int *)x4))
+
+#define Lib_IntTypes_Intrinsics_sub_borrow_u64(x1, x2, x3, x4) \
+    (_subborrow_u64(x1, x2, x3, (long long unsigned int *)x4))
+
+#endif // GCC < 7.2
+
+#endif // !HACL_CAN_COMPILE_INTRINSICS
diff -up ./lib/freebl/verified/karamel/include/krml/internal/target.h.p256 ./lib/freebl/verified/karamel/include/krml/internal/target.h
--- ./lib/freebl/verified/karamel/include/krml/internal/target.h.p256	2023-06-04 01:42:53.000000000 -0700
+++ ./lib/freebl/verified/karamel/include/krml/internal/target.h	2024-01-09 11:35:15.323632291 -0800
@@ -4,11 +4,13 @@
 #ifndef __KRML_TARGET_H
 #define __KRML_TARGET_H
 
-#include <stdlib.h>
-#include <stdio.h>
-#include <stdbool.h>
+#include <assert.h>
 #include <inttypes.h>
 #include <limits.h>
+#include <stdbool.h>
+#include <stddef.h>
+#include <stdio.h>
+#include <stdlib.h>
 
 #include "krml/internal/callconv.h"
 
@@ -46,6 +48,23 @@
 #define KRML_HOST_FREE free
 #endif
 
+#ifndef KRML_HOST_IGNORE
+#define KRML_HOST_IGNORE(x) (void)(x)
+#endif
+
+#ifndef KRML_NOINLINE
+#if defined(_MSC_VER)
+#define KRML_NOINLINE __declspec(noinline)
+#elif defined(__GNUC__)
+#define KRML_NOINLINE __attribute__((noinline))
+#else
+#define KRML_NOINLINE
+#warning "The KRML_NOINLINE macro is not defined for this toolchain!"
+#warning "The compiler may defeat side-channel resistance with optimizations."
+#warning "Please locate target.h and try to fill it out with a suitable definition for this compiler."
+#endif
+#endif
+
 #ifndef KRML_PRE_ALIGN
 #ifdef _MSC_VER
 #define KRML_PRE_ALIGN(X) __declspec(align(X))
@@ -130,7 +149,8 @@ krml_time()
     } while (0)
 
 #if defined(_MSC_VER) && _MSC_VER < 1900
-#define KRML_HOST_SNPRINTF(buf, sz, fmt, arg) _snprintf_s(buf, sz, _TRUNCATE, fmt, arg)
+#define KRML_HOST_SNPRINTF(buf, sz, fmt, arg) \
+    _snprintf_s(buf, sz, _TRUNCATE, fmt, arg)
 #else
 #define KRML_HOST_SNPRINTF(buf, sz, fmt, arg) snprintf(buf, sz, fmt, arg)
 #endif
@@ -149,6 +169,7 @@ krml_time()
     {                       \
         x                   \
             i += n;         \
+        (void)i;            \
     }
 
 #define KRML_LOOP2(i, n, x) \
diff -up ./lib/freebl/verified/karamel/krmllib/dist/minimal/FStar_UInt_8_16_32_64.h.p256 ./lib/freebl/verified/karamel/krmllib/dist/minimal/FStar_UInt_8_16_32_64.h
--- ./lib/freebl/verified/karamel/krmllib/dist/minimal/FStar_UInt_8_16_32_64.h.p256	2023-06-04 01:42:53.000000000 -0700
+++ ./lib/freebl/verified/karamel/krmllib/dist/minimal/FStar_UInt_8_16_32_64.h	2024-01-09 11:41:47.873587264 -0800
@@ -12,15 +12,26 @@
 #include "krml/lowstar_endianness.h"
 #include "krml/internal/types.h"
 #include "krml/internal/target.h"
-extern Prims_int FStar_UInt64_n;
+
+#if defined(__clang__)
+#pragma clang diagnostic push
+#pragma clang diagnostic ignored "-Wunused-function"
+#endif
+
+#if defined(__GNUC__)
+#pragma GCC diagnostic push
+#pragma GCC diagnostic ignored "-Wunused-function"
+#endif
+
+extern krml_checked_int_t FStar_UInt64_n;
 
 extern bool FStar_UInt64_uu___is_Mk(uint64_t projectee);
 
-extern Prims_int FStar_UInt64___proj__Mk__item__v(uint64_t projectee);
+extern krml_checked_int_t FStar_UInt64___proj__Mk__item__v(uint64_t projectee);
 
-extern Prims_int FStar_UInt64_v(uint64_t x);
+extern krml_checked_int_t FStar_UInt64_v(uint64_t x);
 
-extern uint64_t FStar_UInt64_uint_to_t(Prims_int x);
+extern uint64_t FStar_UInt64_uint_to_t(krml_checked_int_t x);
 
 extern uint64_t FStar_UInt64_zero;
 
@@ -62,15 +73,15 @@ extern Prims_string FStar_UInt64_to_stri
 
 extern uint64_t FStar_UInt64_of_string(Prims_string uu___);
 
-extern Prims_int FStar_UInt32_n;
+extern krml_checked_int_t FStar_UInt32_n;
 
 extern bool FStar_UInt32_uu___is_Mk(uint32_t projectee);
 
-extern Prims_int FStar_UInt32___proj__Mk__item__v(uint32_t projectee);
+extern krml_checked_int_t FStar_UInt32___proj__Mk__item__v(uint32_t projectee);
 
-extern Prims_int FStar_UInt32_v(uint32_t x);
+extern krml_checked_int_t FStar_UInt32_v(uint32_t x);
 
-extern uint32_t FStar_UInt32_uint_to_t(Prims_int x);
+extern uint32_t FStar_UInt32_uint_to_t(krml_checked_int_t x);
 
 extern uint32_t FStar_UInt32_zero;
 
@@ -112,15 +123,15 @@ extern Prims_string FStar_UInt32_to_stri
 
 extern uint32_t FStar_UInt32_of_string(Prims_string uu___);
 
-extern Prims_int FStar_UInt16_n;
+extern krml_checked_int_t FStar_UInt16_n;
 
 extern bool FStar_UInt16_uu___is_Mk(uint16_t projectee);
 
-extern Prims_int FStar_UInt16___proj__Mk__item__v(uint16_t projectee);
+extern krml_checked_int_t FStar_UInt16___proj__Mk__item__v(uint16_t projectee);
 
-extern Prims_int FStar_UInt16_v(uint16_t x);
+extern krml_checked_int_t FStar_UInt16_v(uint16_t x);
 
-extern uint16_t FStar_UInt16_uint_to_t(Prims_int x);
+extern uint16_t FStar_UInt16_uint_to_t(krml_checked_int_t x);
 
 extern uint16_t FStar_UInt16_zero;
 
@@ -162,15 +173,15 @@ extern Prims_string FStar_UInt16_to_stri
 
 extern uint16_t FStar_UInt16_of_string(Prims_string uu___);
 
-extern Prims_int FStar_UInt8_n;
+extern krml_checked_int_t FStar_UInt8_n;
 
 extern bool FStar_UInt8_uu___is_Mk(uint8_t projectee);
 
-extern Prims_int FStar_UInt8___proj__Mk__item__v(uint8_t projectee);
+extern krml_checked_int_t FStar_UInt8___proj__Mk__item__v(uint8_t projectee);
 
-extern Prims_int FStar_UInt8_v(uint8_t x);
+extern krml_checked_int_t FStar_UInt8_v(uint8_t x);
 
-extern uint8_t FStar_UInt8_uint_to_t(Prims_int x);
+extern uint8_t FStar_UInt8_uint_to_t(krml_checked_int_t x);
 
 extern uint8_t FStar_UInt8_zero;
 
@@ -214,5 +225,13 @@ extern uint8_t FStar_UInt8_of_string(Pri
 
 typedef uint8_t FStar_UInt8_byte;
 
+#if defined(__clang__)
+#pragma clang diagnostic pop
+#endif
+
+#if defined(__GNUC__)
+#pragma GCC diagnostic pop
+#endif
+
 #define __FStar_UInt_8_16_32_64_H_DEFINED
 #endif