rpms/nss
7
0
Fork 0
Code Issues Pull Requests Releases Activity
5b2f53fc24
nss/nss-3.94-HACL-p256.patch

4307 lines
170 KiB
Diff
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

# HG changeset patch
# User Karthikeyan Bhargavan <karthik.bhargavan@gmail.com>
# Date 1694025109 0
# Node ID 88262a8e60126b5168d0b96306ed5fd2de4867bb
# Parent ffb50bee6680491dddbdc9a3fa723c86332f15f9
Bug 1615555 - P-256 ECDH and ECDSA from HACL*. r=jschanck
Differential Revision: https://phabricator.services.mozilla.com/D185341
diff --git a/lib/freebl/Makefile b/lib/freebl/Makefile
--- a/lib/freebl/Makefile
+++ b/lib/freebl/Makefile
@@ -602,17 +602,17 @@ ifndef NSS_DISABLE_CHACHAPOLY
EXTRA_SRCS += Hacl_Poly1305_128.c Hacl_Chacha20_Vec128.c Hacl_Chacha20Poly1305_128.c
DEFINES += -DHACL_CAN_COMPILE_VEC128
endif
endif # x86_64
VERIFIED_SRCS += Hacl_Poly1305_32.c Hacl_Chacha20.c Hacl_Chacha20Poly1305_32.c
endif # NSS_DISABLE_CHACHAPOLY
-VERIFIED_SRCS += Hacl_Hash_SHA3.c
+VERIFIED_SRCS += Hacl_Hash_SHA3.c 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
VERIFIED_SRCS += Hacl_Curve25519_51.c
else
# All other architectures get the generic 32 bit implementation
ECL_SRCS += curve25519_32.c
diff --git a/lib/freebl/blapi.h b/lib/freebl/blapi.h
--- a/lib/freebl/blapi.h
+++ b/lib/freebl/blapi.h
@@ -1886,11 +1886,16 @@ extern SECStatus EC_DecodeParams(const S
extern SECStatus EC_CopyParams(PLArenaPool *arena, ECParams *dstParams,
const ECParams *srcParams);
/*
* use the internal table to get the size in bytes of a single EC point
*/
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 --git a/lib/freebl/ec.c b/lib/freebl/ec.c
--- a/lib/freebl/ec.c
+++ b/lib/freebl/ec.c
@@ -16,17 +16,25 @@
#include "ec.h"
#include "ecl.h"
#define EC_DOUBLECHECK PR_FALSE
static const ECMethod kMethods[] = {
{ ECCurve25519,
ec_Curve25519_pt_mul,
- ec_Curve25519_pt_validate }
+ ec_Curve25519_pt_validate,
+ NULL, NULL },
+ {
+ ECCurve_NIST_P256,
+ ec_secp256r1_pt_mul,
+ ec_secp256r1_pt_validate,
+ ec_secp256r1_sign_digest,
+ ec_secp256r1_verify_digest,
+ }
};
static const ECMethod *
ec_get_method_from_name(ECCurveName name)
{
unsigned long i;
for (i = 0; i < sizeof(kMethods) / sizeof(kMethods[0]); ++i) {
if (kMethods[i].name == name) {
@@ -282,17 +290,21 @@ ec_NewKey(ECParams *ecParams, ECPrivateK
if (ecParams->fieldID.type == ec_field_plain) {
const ECMethod *method = ec_get_method_from_name(ecParams->name);
if (method == NULL || method->mul == NULL) {
/* unknown curve */
rv = SECFailure;
goto cleanup;
}
rv = method->mul(&key->publicValue, &key->privateValue, NULL);
- goto done;
+ if (rv != SECSuccess) {
+ goto cleanup;
+ } else {
+ goto done;
+ }
}
CHECK_MPI_OK(mp_init(&k));
CHECK_MPI_OK(mp_read_unsigned_octets(&k, key->privateValue.data,
(mp_size)len));
rv = ec_points_mul(ecParams, &k, NULL, NULL, &(key->publicValue));
if (rv != SECSuccess) {
@@ -367,16 +379,17 @@ ec_GenerateRandomPrivateKey(const unsign
CHECK_MPI_OK(mp_read_unsigned_octets(&privKeyVal, privKeyBytes, 2 * len));
CHECK_MPI_OK(mp_read_unsigned_octets(&order_1, order, len));
CHECK_MPI_OK(mp_set_int(&one, 1));
CHECK_MPI_OK(mp_sub(&order_1, &one, &order_1));
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);
+
cleanup:
mp_clear(&privKeyVal);
mp_clear(&order_1);
mp_clear(&one);
if (err < MP_OKAY) {
MP_TO_SEC_ERROR(err);
rv = SECFailure;
}
@@ -435,28 +448,34 @@ EC_ValidatePublicKey(ECParams *ecParams,
ECGroup *group = NULL;
SECStatus rv = SECFailure;
mp_err err = MP_OKAY;
unsigned int len;
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) {
/* unknown curve */
PORT_SetError(SEC_ERROR_INVALID_ARGS);
- return SECFailure;
+ rv = SECFailure;
+ return rv;
}
- return method->validate(publicValue);
+ rv = method->validate(publicValue);
+ if (rv != SECSuccess) {
+ PORT_SetError(SEC_ERROR_BAD_KEY);
+ }
+ return rv;
}
/* NOTE: We only support uncompressed points for now */
len = (((unsigned int)ecParams->fieldID.size) + 7) >> 3;
if (publicValue->data[0] != EC_POINT_FORM_UNCOMPRESSED) {
PORT_SetError(SEC_ERROR_UNSUPPORTED_EC_POINT_FORM);
return SECFailure;
} else if (publicValue->len != (2 * len + 1)) {
@@ -505,16 +524,17 @@ EC_ValidatePublicKey(ECParams *ecParams,
}
rv = SECSuccess;
cleanup:
ECGroup_free(group);
mp_clear(&Px);
mp_clear(&Py);
+
if (err) {
MP_TO_SEC_ERROR(err);
rv = SECFailure;
}
return rv;
}
/*
@@ -531,61 +551,66 @@ SECStatus
ECDH_Derive(SECItem *publicValue,
ECParams *ecParams,
SECItem *privateValue,
PRBool withCofactor,
SECItem *derivedSecret)
{
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;
}
/*
* Make sure the point is on the requested curve to avoid
* certain small subgroup attacks.
*/
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) {
PORT_SetError(SEC_ERROR_UNSUPPORTED_ELLIPTIC_CURVE);
- return SECFailure;
+ rv = SECFailure;
+ goto done;
}
rv = method->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.
*/
if (ec_point_at_infinity(publicValue)) {
PORT_SetError(SEC_ERROR_BAD_KEY);
return SECFailure;
}
@@ -633,84 +658,108 @@ ECDH_Derive(SECItem *publicValue,
for (i = 0; i < derivedSecret->len; i++)
printf("%02x:", derivedSecret->data[i]);
printf("\n");
#endif
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;
}
/* Computes the ECDSA signature (a concatenation of two values r and s)
* on the digest using the given key and the random value kb (used in
* computing s).
*/
static SECStatus
ec_SignDigestWithSeed(ECPrivateKey *key, SECItem *signature,
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 char *t2 = NULL;
unsigned obits; /* length in bits of the base point order */
- unsigned char *t2 = NULL;
#if EC_DEBUG
char mpstr[256];
#endif
/* Initialize MPI integers. */
/* must happen before the first potential call to cleanup */
MP_DIGITS(&x1) = 0;
MP_DIGITS(&d) = 0;
MP_DIGITS(&k) = 0;
MP_DIGITS(&r) = 0;
MP_DIGITS(&s) = 0;
MP_DIGITS(&n) = 0;
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));
CHECK_MPI_OK(mp_init(&r));
CHECK_MPI_OK(mp_init(&s));
CHECK_MPI_OK(mp_init(&n));
CHECK_MPI_OK(mp_init(&t));
CHECK_MPI_OK(mp_init(&ar));
@@ -846,21 +895,21 @@ ec_SignDigestWithSeed(ECPrivateKey *key,
}
/*
**
** Signature is tuple (r, s)
*/
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;
-
rv = SECSuccess;
err = MP_OKAY;
+
cleanup:
mp_clear(&x1);
mp_clear(&d);
mp_clear(&k);
mp_clear(&r);
mp_clear(&s);
mp_clear(&n);
mp_clear(&t);
@@ -869,16 +918,17 @@ cleanup:
if (t2) {
PORT_ZFree(t2, 2 * ecParams->order.len);
}
if (kGpoint.data) {
PORT_ZFree(kGpoint.data, kGpoint.len);
}
+done:
if (err) {
MP_TO_SEC_ERROR(err);
rv = SECFailure;
}
#if EC_DEBUG
printf("ECDSA signing with seed %s\n",
(rv == SECSuccess) ? "succeeded" : "failed");
@@ -887,22 +937,22 @@ cleanup:
return rv;
}
SECStatus
ECDSA_SignDigestWithSeed(ECPrivateKey *key, SECItem *signature,
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 {
rv = SECFailure;
}
#if EC_DEBUG
printf("ECDSA signing with seed %s after signing twice\n", (rv == SECSuccess) ? "succeeded" : "failed");
@@ -961,60 +1011,78 @@ cleanup:
** of this function is undefined. In cases where a public key might
** not be valid, use EC_ValidatePublicKey to check.
*/
SECStatus
ECDSA_VerifyDigest(ECPublicKey *key, const SECItem *signature,
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 */
unsigned olen; /* length in bytes of the base point order */
unsigned obits; /* length in bits of the base point order */
#if EC_DEBUG
char mpstr[256];
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;
MP_DIGITS(&s_) = 0;
MP_DIGITS(&c) = 0;
MP_DIGITS(&u1) = 0;
MP_DIGITS(&u2) = 0;
MP_DIGITS(&x1) = 0;
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.
*/
SECITEM_AllocItem(NULL, &pointC, EC_GetPointSize(ecParams));
if (pointC.data == NULL) {
goto cleanup;
}
@@ -1151,16 +1219,18 @@ cleanup:
mp_clear(&u1);
mp_clear(&u2);
mp_clear(&x1);
mp_clear(&v);
mp_clear(&n);
if (pointC.data)
SECITEM_ZfreeItem(&pointC, PR_FALSE);
+
+done:
if (err) {
MP_TO_SEC_ERROR(err);
rv = SECFailure;
}
#if EC_DEBUG
printf("ECDSA verification %s\n",
(rv == SECSuccess) ? "succeeded" : "failed");
diff --git a/lib/freebl/ec.h b/lib/freebl/ec.h
--- a/lib/freebl/ec.h
+++ b/lib/freebl/ec.h
@@ -10,12 +10,14 @@
#define ANSI_X962_CURVE_OID_TOTAL_LEN 10
#define SECG_CURVE_OID_TOTAL_LEN 7
#define PKIX_NEWCURVES_OID_TOTAL_LEN 11
struct ECMethodStr {
ECCurveName name;
SECStatus (*mul)(SECItem *result, SECItem *scalar, SECItem *point);
SECStatus (*validate)(const SECItem *point);
+ 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;
#endif /* __ec_h_ */
diff --git a/lib/freebl/ecdecode.c b/lib/freebl/ecdecode.c
--- a/lib/freebl/ecdecode.c
+++ b/lib/freebl/ecdecode.c
@@ -150,17 +150,17 @@ EC_FillParams(PLArenaPool *arena, const
#endif
switch (tag) {
case SEC_OID_ANSIX962_EC_PRIME256V1:
/* Populate params for prime256v1 aka secp256r1
* (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:
/* Populate params for secp384r1
* (the NIST P-384 curve)
*/
CHECK_SEC_OK(gf_populate_params_bytes(ECCurve_SECG_PRIME_384R1,
ec_field_GFp, params));
@@ -171,17 +171,18 @@ EC_FillParams(PLArenaPool *arena, const
* (the NIST P-521 curve)
*/
CHECK_SEC_OK(gf_populate_params_bytes(ECCurve_SECG_PRIME_521R1,
ec_field_GFp, params));
break;
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;
default:
break;
};
cleanup:
@@ -245,8 +246,23 @@ EC_GetPointSize(const ECParams *params)
return sizeInBytes * 2 + 1;
}
if (name == ECCurve25519) {
/* Only X here */
return curveParams->scalarSize;
}
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 --git a/lib/freebl/ecl/ecl.h b/lib/freebl/ecl/ecl.h
--- a/lib/freebl/ecl/ecl.h
+++ b/lib/freebl/ecl/ecl.h
@@ -41,9 +41,18 @@ mp_err ECPoints_mul(const ECGroup *group
* Returns MP_YES if the public key is valid, MP_NO if the public key
* is invalid, or an error code if the validation could not be
* performed. */
mp_err ECPoint_validate(const ECGroup *group, const mp_int *px, const mp_int *py);
SECStatus ec_Curve25519_pt_mul(SECItem *X, SECItem *k, SECItem *P);
SECStatus ec_Curve25519_pt_validate(const SECItem *px);
+SECStatus ec_secp256r1_pt_mul(SECItem *X, SECItem *k, SECItem *P);
+SECStatus ec_secp256r1_pt_validate(const SECItem *px);
+
+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 --git a/lib/freebl/ecl/ecp_secp256r1.c b/lib/freebl/ecl/ecp_secp256r1.c
new file mode 100644
--- /dev/null
+++ b/lib/freebl/ecl/ecp_secp256r1.c
@@ -0,0 +1,229 @@
+/* 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 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 --git a/lib/freebl/freebl.gyp b/lib/freebl/freebl.gyp
--- a/lib/freebl/freebl.gyp
+++ b/lib/freebl/freebl.gyp
@@ -838,24 +838,26 @@
'MP_IS_LITTLE_ENDIAN',
],
}],
# Poly1305_256 requires the flag to run
['target_arch=="x64"', {
'defines':[
'HACL_CAN_COMPILE_VEC128',
'HACL_CAN_COMPILE_VEC256',
+ 'HACL_CAN_COMPILE_INTRINSICS',
],
}],
# MSVC has no __int128 type. Use emulated int128 and leave
# have_int128_support as-is for Curve25519 impl. selection.
[ 'have_int128_support==1 and (OS!="win" or cc_is_clang==1 or cc_is_gcc==1)', {
'defines': [
# The Makefile does version-tests on GCC, but we're not doing that here.
'HAVE_INT128_SUPPORT',
+ 'HACL_CAN_COMPILE_UINT128'
],
}, {
'defines': [
'KRML_VERIFIED_UINT128',
],
}],
[ 'OS=="linux"', {
'defines': [
diff --git a/lib/freebl/freebl_base.gypi b/lib/freebl/freebl_base.gypi
--- a/lib/freebl/freebl_base.gypi
+++ b/lib/freebl/freebl_base.gypi
@@ -29,18 +29,20 @@
'ecl/ecp_256.c',
'ecl/ecp_256_32.c',
'ecl/ecp_384.c',
'ecl/ecp_521.c',
'ecl/ecp_aff.c',
'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',
'gcm.c',
'hmacct.c',
'jpake.c',
'ldvector.c',
'md2.c',
diff --git a/lib/freebl/manifest.mn b/lib/freebl/manifest.mn
--- a/lib/freebl/manifest.mn
+++ b/lib/freebl/manifest.mn
@@ -102,17 +102,17 @@ PRIVATE_EXPORTS = \
MPI_HDRS = mpi-config.h mpi.h mpi-priv.h mplogic.h mpprime.h logtab.h mp_gf2m.h
MPI_SRCS = mpprime.c mpmontg.c mplogic.c mpi.c mp_gf2m.c
ECL_HDRS = ecl-exp.h ecl.h ecp.h ecl-priv.h
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)
CSRCS = \
freeblver.c \
ldvector.c \
sysrand.c \
diff --git a/lib/freebl/verified/Hacl_P256.c b/lib/freebl/verified/Hacl_P256.c
new file mode 100644
--- /dev/null
+++ b/lib/freebl/verified/Hacl_P256.c
@@ -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 --git a/lib/freebl/verified/Hacl_P256.h b/lib/freebl/verified/Hacl_P256.h
new file mode 100644
--- /dev/null
+++ b/lib/freebl/verified/Hacl_P256.h
@@ -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 --git a/lib/freebl/verified/internal/Hacl_Bignum_Base.h b/lib/freebl/verified/internal/Hacl_Bignum_Base.h
new file mode 100644
--- /dev/null
+++ b/lib/freebl/verified/internal/Hacl_Bignum_Base.h
@@ -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 --git a/lib/freebl/verified/internal/Hacl_IntTypes_Intrinsics.h b/lib/freebl/verified/internal/Hacl_IntTypes_Intrinsics.h
new file mode 100644
--- /dev/null
+++ b/lib/freebl/verified/internal/Hacl_IntTypes_Intrinsics.h
@@ -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 --git a/lib/freebl/verified/internal/Hacl_IntTypes_Intrinsics_128.h b/lib/freebl/verified/internal/Hacl_IntTypes_Intrinsics_128.h
new file mode 100644
--- /dev/null
+++ b/lib/freebl/verified/internal/Hacl_IntTypes_Intrinsics_128.h
@@ -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 --git a/lib/freebl/verified/internal/Hacl_P256.h b/lib/freebl/verified/internal/Hacl_P256.h
new file mode 100644
--- /dev/null
+++ b/lib/freebl/verified/internal/Hacl_P256.h
@@ -0,0 +1,56 @@
+/* MIT License
+ *
+ * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation
+ * Copyright (c) 2022-2023 HACL* Contributors
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the Software is
+ * furnished to do so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+ * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+ * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+ * SOFTWARE.
+ */
+
+#ifndef __internal_Hacl_P256_H
+#define __internal_Hacl_P256_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
+#include <string.h>
+#include "krml/internal/types.h"
+#include "krml/lowstar_endianness.h"
+#include "krml/internal/target.h"
+
+#include "internal/Hacl_P256_PrecompTable.h"
+#include "internal/Hacl_Krmllib.h"
+#include "internal/Hacl_Bignum_Base.h"
+#include "../Hacl_P256.h"
+//#include "lib_intrinsics.h"
+
+bool Hacl_Impl_P256_DH_ecp256dh_i(uint8_t *public_key, uint8_t *private_key);
+
+bool
+Hacl_Impl_P256_DH_ecp256dh_r(
+ uint8_t *shared_secret,
+ uint8_t *their_pubkey,
+ uint8_t *private_key);
+
+#if defined(__cplusplus)
+}
+#endif
+
+#define __internal_Hacl_P256_H_DEFINED
+#endif
diff --git a/lib/freebl/verified/internal/Hacl_P256_PrecompTable.h b/lib/freebl/verified/internal/Hacl_P256_PrecompTable.h
new file mode 100644
--- /dev/null
+++ b/lib/freebl/verified/internal/Hacl_P256_PrecompTable.h
@@ -0,0 +1,508 @@
+/* MIT License
+ *
+ * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation
+ * Copyright (c) 2022-2023 HACL* Contributors
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the Software is
+ * furnished to do so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+ * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+ * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+ * SOFTWARE.
+ */
+
+#ifndef __internal_Hacl_P256_PrecompTable_H
+#define __internal_Hacl_P256_PrecompTable_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
+#include <string.h>
+#include "krml/internal/types.h"
+#include "krml/lowstar_endianness.h"
+#include "krml/internal/target.h"
+
+static const uint64_t
+ Hacl_P256_PrecompTable_precomp_basepoint_table_w4[192U] = {
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)1U,
+ (uint64_t)18446744069414584320U, (uint64_t)18446744073709551615U, (uint64_t)4294967294U,
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)8784043285714375740U,
+ (uint64_t)8483257759279461889U, (uint64_t)8789745728267363600U, (uint64_t)1770019616739251654U,
+ (uint64_t)15992936863339206154U, (uint64_t)10037038012062884956U,
+ (uint64_t)15197544864945402661U, (uint64_t)9615747158586711429U, (uint64_t)1U,
+ (uint64_t)18446744069414584320U, (uint64_t)18446744073709551615U, (uint64_t)4294967294U,
+ (uint64_t)10634854829044225757U, (uint64_t)351552716085025155U, (uint64_t)10645315080955407736U,
+ (uint64_t)3609262091244858135U, (uint64_t)15760741698986874125U,
+ (uint64_t)14936374388219697827U, (uint64_t)15751360096993017895U,
+ (uint64_t)18012233706239762398U, (uint64_t)1993877568177495041U,
+ (uint64_t)10345888787846536528U, (uint64_t)7746511691117935375U,
+ (uint64_t)14517043990409914413U, (uint64_t)14122549297570634151U,
+ (uint64_t)16934610359517083771U, (uint64_t)5724511325497097418U, (uint64_t)8983432969107448705U,
+ (uint64_t)2687429970334080245U, (uint64_t)16525396802810050288U, (uint64_t)7602596488871585854U,
+ (uint64_t)4813919589149203084U, (uint64_t)7680395813780804519U, (uint64_t)6687709583048023590U,
+ (uint64_t)18086445169104142027U, (uint64_t)9637814708330203929U,
+ (uint64_t)14785108459960679090U, (uint64_t)3838023279095023581U, (uint64_t)3555615526157830307U,
+ (uint64_t)5177066488380472871U, (uint64_t)18218186719108038403U,
+ (uint64_t)16281556341699656105U, (uint64_t)1524227924561461191U, (uint64_t)4148060517641909597U,
+ (uint64_t)2858290374115363433U, (uint64_t)8942772026334130620U, (uint64_t)3034451298319885113U,
+ (uint64_t)8447866036736640940U, (uint64_t)11204933433076256578U,
+ (uint64_t)18333595740249588297U, (uint64_t)8259597024804538246U, (uint64_t)9539734295777539786U,
+ (uint64_t)9797290423046626413U, (uint64_t)5777303437849646537U, (uint64_t)8739356909899132020U,
+ (uint64_t)14815960973766782158U, (uint64_t)15286581798204509801U,
+ (uint64_t)17597362577777019682U, (uint64_t)13259283710820519742U,
+ (uint64_t)10501322996899164670U, (uint64_t)1221138904338319642U,
+ (uint64_t)14586685489551951885U, (uint64_t)895326705426031212U, (uint64_t)14398171728560617847U,
+ (uint64_t)9592550823745097391U, (uint64_t)17240998489162206026U, (uint64_t)8085479283308189196U,
+ (uint64_t)14844657737893882826U, (uint64_t)15923425394150618234U,
+ (uint64_t)2997808084773249525U, (uint64_t)494323555453660587U, (uint64_t)1215695327517794764U,
+ (uint64_t)9476207381098391690U, (uint64_t)7480789678419122995U, (uint64_t)15212230329321082489U,
+ (uint64_t)436189395349576388U, (uint64_t)17377474396456660834U, (uint64_t)15237013929655017939U,
+ (uint64_t)11444428846883781676U, (uint64_t)5112749694521428575U, (uint64_t)950829367509872073U,
+ (uint64_t)17665036182057559519U, (uint64_t)17205133339690002313U,
+ (uint64_t)16233765170251334549U, (uint64_t)10122775683257972591U,
+ (uint64_t)3352514236455632420U, (uint64_t)9143148522359954691U, (uint64_t)601191684005658860U,
+ (uint64_t)13398772186646349998U, (uint64_t)15512696600132928431U,
+ (uint64_t)9128416073728948653U, (uint64_t)11233051033546138578U, (uint64_t)6769345682610122833U,
+ (uint64_t)10823233224575054288U, (uint64_t)9997725227559980175U, (uint64_t)6733425642852897415U,
+ (uint64_t)16302206918151466066U, (uint64_t)1669330822143265921U, (uint64_t)2661645605036546002U,
+ (uint64_t)17182558479745802165U, (uint64_t)1165082692376932040U, (uint64_t)9470595929011488359U,
+ (uint64_t)6142147329285324932U, (uint64_t)4829075085998111287U, (uint64_t)10231370681107338930U,
+ (uint64_t)9591876895322495239U, (uint64_t)10316468561384076618U,
+ (uint64_t)11592503647238064235U, (uint64_t)13395813606055179632U, (uint64_t)511127033980815508U,
+ (uint64_t)12434976573147649880U, (uint64_t)3425094795384359127U, (uint64_t)6816971736303023445U,
+ (uint64_t)15444670609021139344U, (uint64_t)9464349818322082360U,
+ (uint64_t)16178216413042376883U, (uint64_t)9595540370774317348U, (uint64_t)7229365182662875710U,
+ (uint64_t)4601177649460012843U, (uint64_t)5455046447382487090U, (uint64_t)10854066421606187521U,
+ (uint64_t)15913416821879788071U, (uint64_t)2297365362023460173U, (uint64_t)2603252216454941350U,
+ (uint64_t)6768791943870490934U, (uint64_t)15705936687122754810U, (uint64_t)9537096567546600694U,
+ (uint64_t)17580538144855035062U, (uint64_t)4496542856965746638U, (uint64_t)8444341625922124942U,
+ (uint64_t)12191263903636183168U, (uint64_t)17427332907535974165U,
+ (uint64_t)14307569739254103736U, (uint64_t)13900598742063266169U,
+ (uint64_t)7176996424355977650U, (uint64_t)5709008170379717479U, (uint64_t)14471312052264549092U,
+ (uint64_t)1464519909491759867U, (uint64_t)3328154641049602121U, (uint64_t)13020349337171136774U,
+ (uint64_t)2772166279972051938U, (uint64_t)10854476939425975292U, (uint64_t)1967189930534630940U,
+ (uint64_t)2802919076529341959U, (uint64_t)14792226094833519208U,
+ (uint64_t)14675640928566522177U, (uint64_t)14838974364643800837U,
+ (uint64_t)17631460696099549980U, (uint64_t)17434186275364935469U,
+ (uint64_t)2665648200587705473U, (uint64_t)13202122464492564051U, (uint64_t)7576287350918073341U,
+ (uint64_t)2272206013910186424U, (uint64_t)14558761641743937843U, (uint64_t)5675729149929979729U,
+ (uint64_t)9043135187561613166U, (uint64_t)11750149293830589225U, (uint64_t)740555197954307911U,
+ (uint64_t)9871738005087190699U, (uint64_t)17178667634283502053U,
+ (uint64_t)18046255991533013265U, (uint64_t)4458222096988430430U, (uint64_t)8452427758526311627U,
+ (uint64_t)13825286929656615266U, (uint64_t)13956286357198391218U,
+ (uint64_t)15875692916799995079U, (uint64_t)10634895319157013920U,
+ (uint64_t)13230116118036304207U, (uint64_t)8795317393614625606U, (uint64_t)7001710806858862020U,
+ (uint64_t)7949746088586183478U, (uint64_t)14677556044923602317U,
+ (uint64_t)11184023437485843904U, (uint64_t)11215864722023085094U,
+ (uint64_t)6444464081471519014U, (uint64_t)1706241174022415217U, (uint64_t)8243975633057550613U,
+ (uint64_t)15502902453836085864U, (uint64_t)3799182188594003953U, (uint64_t)3538840175098724094U
+ };
+
+static const uint64_t
+ Hacl_P256_PrecompTable_precomp_g_pow2_64_table_w4[192U] = {
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)1U,
+ (uint64_t)18446744069414584320U, (uint64_t)18446744073709551615U, (uint64_t)4294967294U,
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)1499621593102562565U,
+ (uint64_t)16692369783039433128U, (uint64_t)15337520135922861848U,
+ (uint64_t)5455737214495366228U, (uint64_t)17827017231032529600U,
+ (uint64_t)12413621606240782649U, (uint64_t)2290483008028286132U,
+ (uint64_t)15752017553340844820U, (uint64_t)4846430910634234874U,
+ (uint64_t)10861682798464583253U, (uint64_t)15404737222404363049U, (uint64_t)363586619281562022U,
+ (uint64_t)9866710912401645115U, (uint64_t)1162548847543228595U, (uint64_t)7649967190445130486U,
+ (uint64_t)5212340432230915749U, (uint64_t)7572620550182916491U, (uint64_t)14876145112448665096U,
+ (uint64_t)2063227348838176167U, (uint64_t)3519435548295415847U, (uint64_t)8390400282019023103U,
+ (uint64_t)17666843593163037841U, (uint64_t)9450204148816496323U, (uint64_t)8483374507652916768U,
+ (uint64_t)6254661047265818424U, (uint64_t)16382127809582285023U, (uint64_t)125359443771153172U,
+ (uint64_t)1374336701588437897U, (uint64_t)11362596098420127726U, (uint64_t)2101654420738681387U,
+ (uint64_t)12772780342444840510U, (uint64_t)12546934328908550060U,
+ (uint64_t)8331880412333790397U, (uint64_t)11687262051473819904U, (uint64_t)8926848496503457587U,
+ (uint64_t)9603974142010467857U, (uint64_t)13199952163826973175U, (uint64_t)2189856264898797734U,
+ (uint64_t)11356074861870267226U, (uint64_t)2027714896422561895U, (uint64_t)5261606367808050149U,
+ (uint64_t)153855954337762312U, (uint64_t)6375919692894573986U, (uint64_t)12364041207536146533U,
+ (uint64_t)1891896010455057160U, (uint64_t)1568123795087313171U, (uint64_t)18138710056556660101U,
+ (uint64_t)6004886947510047736U, (uint64_t)4811859325589542932U, (uint64_t)3618763430148954981U,
+ (uint64_t)11434521746258554122U, (uint64_t)10086341535864049427U,
+ (uint64_t)8073421629570399570U, (uint64_t)12680586148814729338U, (uint64_t)9619958020761569612U,
+ (uint64_t)15827203580658384478U, (uint64_t)12832694810937550406U,
+ (uint64_t)14977975484447400910U, (uint64_t)5478002389061063653U,
+ (uint64_t)14731136312639060880U, (uint64_t)4317867687275472033U, (uint64_t)6642650962855259884U,
+ (uint64_t)2514254944289495285U, (uint64_t)14231405641534478436U, (uint64_t)4045448346091518946U,
+ (uint64_t)8985477013445972471U, (uint64_t)8869039454457032149U, (uint64_t)4356978486208692970U,
+ (uint64_t)10805288613335538577U, (uint64_t)12832353127812502042U,
+ (uint64_t)4576590051676547490U, (uint64_t)6728053735138655107U, (uint64_t)17814206719173206184U,
+ (uint64_t)79790138573994940U, (uint64_t)17920293215101822267U, (uint64_t)13422026625585728864U,
+ (uint64_t)5018058010492547271U, (uint64_t)110232326023384102U, (uint64_t)10834264070056942976U,
+ (uint64_t)15222249086119088588U, (uint64_t)15119439519142044997U,
+ (uint64_t)11655511970063167313U, (uint64_t)1614477029450566107U, (uint64_t)3619322817271059794U,
+ (uint64_t)9352862040415412867U, (uint64_t)14017522553242747074U,
+ (uint64_t)13138513643674040327U, (uint64_t)3610195242889455765U, (uint64_t)8371069193996567291U,
+ (uint64_t)12670227996544662654U, (uint64_t)1205961025092146303U,
+ (uint64_t)13106709934003962112U, (uint64_t)4350113471327723407U,
+ (uint64_t)15060941403739680459U, (uint64_t)13639127647823205030U,
+ (uint64_t)10790943339357725715U, (uint64_t)498760574280648264U, (uint64_t)17922071907832082887U,
+ (uint64_t)15122670976670152145U, (uint64_t)6275027991110214322U, (uint64_t)7250912847491816402U,
+ (uint64_t)15206617260142982380U, (uint64_t)3385668313694152877U,
+ (uint64_t)17522479771766801905U, (uint64_t)2965919117476170655U, (uint64_t)1553238516603269404U,
+ (uint64_t)5820770015631050991U, (uint64_t)4999445222232605348U, (uint64_t)9245650860833717444U,
+ (uint64_t)1508811811724230728U, (uint64_t)5190684913765614385U, (uint64_t)15692927070934536166U,
+ (uint64_t)12981978499190500902U, (uint64_t)5143491963193394698U, (uint64_t)7705698092144084129U,
+ (uint64_t)581120653055084783U, (uint64_t)13886552864486459714U, (uint64_t)6290301270652587255U,
+ (uint64_t)8663431529954393128U, (uint64_t)17033405846475472443U, (uint64_t)5206780355442651635U,
+ (uint64_t)12580364474736467688U, (uint64_t)17934601912005283310U,
+ (uint64_t)15119491731028933652U, (uint64_t)17848231399859044858U,
+ (uint64_t)4427673319524919329U, (uint64_t)2673607337074368008U, (uint64_t)14034876464294699949U,
+ (uint64_t)10938948975420813697U, (uint64_t)15202340615298669183U,
+ (uint64_t)5496603454069431071U, (uint64_t)2486526142064906845U, (uint64_t)4507882119510526802U,
+ (uint64_t)13888151172411390059U, (uint64_t)15049027856908071726U,
+ (uint64_t)9667231543181973158U, (uint64_t)6406671575277563202U, (uint64_t)3395801050331215139U,
+ (uint64_t)9813607433539108308U, (uint64_t)2681417728820980381U, (uint64_t)18407064643927113994U,
+ (uint64_t)7707177692113485527U, (uint64_t)14218149384635317074U, (uint64_t)3658668346206375919U,
+ (uint64_t)15404713991002362166U, (uint64_t)10152074687696195207U,
+ (uint64_t)10926946599582128139U, (uint64_t)16907298600007085320U,
+ (uint64_t)16544287219664720279U, (uint64_t)11007075933432813205U,
+ (uint64_t)8652245965145713599U, (uint64_t)7857626748965990384U, (uint64_t)5602306604520095870U,
+ (uint64_t)2525139243938658618U, (uint64_t)14405696176872077447U,
+ (uint64_t)18432270482137885332U, (uint64_t)9913880809120071177U,
+ (uint64_t)16896141737831216972U, (uint64_t)7484791498211214829U,
+ (uint64_t)15635259968266497469U, (uint64_t)8495118537612215624U, (uint64_t)4915477980562575356U,
+ (uint64_t)16453519279754924350U, (uint64_t)14462108244565406969U,
+ (uint64_t)14837837755237096687U, (uint64_t)14130171078892575346U,
+ (uint64_t)15423793222528491497U, (uint64_t)5460399262075036084U,
+ (uint64_t)16085440580308415349U, (uint64_t)26873200736954488U, (uint64_t)5603655807457499550U,
+ (uint64_t)3342202915871129617U, (uint64_t)1604413932150236626U, (uint64_t)9684226585089458974U,
+ (uint64_t)1213229904006618539U, (uint64_t)6782978662408837236U, (uint64_t)11197029877749307372U,
+ (uint64_t)14085968786551657744U, (uint64_t)17352273610494009342U,
+ (uint64_t)7876582961192434984U
+ };
+
+static const uint64_t
+ Hacl_P256_PrecompTable_precomp_g_pow2_128_table_w4[192U] = {
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)1U,
+ (uint64_t)18446744069414584320U, (uint64_t)18446744073709551615U, (uint64_t)4294967294U,
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)14619254753077084366U,
+ (uint64_t)13913835116514008593U, (uint64_t)15060744674088488145U,
+ (uint64_t)17668414598203068685U, (uint64_t)10761169236902342334U,
+ (uint64_t)15467027479157446221U, (uint64_t)14989185522423469618U,
+ (uint64_t)14354539272510107003U, (uint64_t)14298211796392133693U,
+ (uint64_t)13270323784253711450U, (uint64_t)13380964971965046957U,
+ (uint64_t)8686204248456909699U, (uint64_t)17434630286744937066U, (uint64_t)1355903775279084720U,
+ (uint64_t)7554695053550308662U, (uint64_t)11354971222741863570U, (uint64_t)564601613420749879U,
+ (uint64_t)8466325837259054896U, (uint64_t)10752965181772434263U,
+ (uint64_t)11405876547368426319U, (uint64_t)13791894568738930940U,
+ (uint64_t)8230587134406354675U, (uint64_t)12415514098722758608U,
+ (uint64_t)18414183046995786744U, (uint64_t)15508000368227372870U,
+ (uint64_t)5781062464627999307U, (uint64_t)15339429052219195590U,
+ (uint64_t)16038703753810741903U, (uint64_t)9587718938298980714U, (uint64_t)4822658817952386407U,
+ (uint64_t)1376351024833260660U, (uint64_t)1120174910554766702U, (uint64_t)1730170933262569274U,
+ (uint64_t)5187428548444533500U, (uint64_t)16242053503368957131U, (uint64_t)3036811119519868279U,
+ (uint64_t)1760267587958926638U, (uint64_t)170244572981065185U, (uint64_t)8063080791967388171U,
+ (uint64_t)4824892826607692737U, (uint64_t)16286391083472040552U,
+ (uint64_t)11945158615253358747U, (uint64_t)14096887760410224200U,
+ (uint64_t)1613720831904557039U, (uint64_t)14316966673761197523U,
+ (uint64_t)17411006201485445341U, (uint64_t)8112301506943158801U, (uint64_t)2069889233927989984U,
+ (uint64_t)10082848378277483927U, (uint64_t)3609691194454404430U, (uint64_t)6110437205371933689U,
+ (uint64_t)9769135977342231601U, (uint64_t)11977962151783386478U,
+ (uint64_t)18088718692559983573U, (uint64_t)11741637975753055U, (uint64_t)11110390325701582190U,
+ (uint64_t)1341402251566067019U, (uint64_t)3028229550849726478U, (uint64_t)10438984083997451310U,
+ (uint64_t)12730851885100145709U, (uint64_t)11524169532089894189U,
+ (uint64_t)4523375903229602674U, (uint64_t)2028602258037385622U, (uint64_t)17082839063089388410U,
+ (uint64_t)6103921364634113167U, (uint64_t)17066180888225306102U,
+ (uint64_t)11395680486707876195U, (uint64_t)10952892272443345484U,
+ (uint64_t)8792831960605859401U, (uint64_t)14194485427742325139U,
+ (uint64_t)15146020821144305250U, (uint64_t)1654766014957123343U, (uint64_t)7955526243090948551U,
+ (uint64_t)3989277566080493308U, (uint64_t)12229385116397931231U,
+ (uint64_t)13430548930727025562U, (uint64_t)3434892688179800602U, (uint64_t)8431998794645622027U,
+ (uint64_t)12132530981596299272U, (uint64_t)2289461608863966999U,
+ (uint64_t)18345870950201487179U, (uint64_t)13517947207801901576U,
+ (uint64_t)5213113244172561159U, (uint64_t)17632986594098340879U, (uint64_t)4405251818133148856U,
+ (uint64_t)11783009269435447793U, (uint64_t)9332138983770046035U,
+ (uint64_t)12863411548922539505U, (uint64_t)3717030292816178224U,
+ (uint64_t)10026078446427137374U, (uint64_t)11167295326594317220U,
+ (uint64_t)12425328773141588668U, (uint64_t)5760335125172049352U, (uint64_t)9016843701117277863U,
+ (uint64_t)5657892835694680172U, (uint64_t)11025130589305387464U, (uint64_t)1368484957977406173U,
+ (uint64_t)17361351345281258834U, (uint64_t)1907113641956152700U,
+ (uint64_t)16439233413531427752U, (uint64_t)5893322296986588932U,
+ (uint64_t)14000206906171746627U, (uint64_t)14979266987545792900U,
+ (uint64_t)6926291766898221120U, (uint64_t)7162023296083360752U, (uint64_t)14762747553625382529U,
+ (uint64_t)12610831658612406849U, (uint64_t)10462926899548715515U,
+ (uint64_t)4794017723140405312U, (uint64_t)5234438200490163319U, (uint64_t)8019519110339576320U,
+ (uint64_t)7194604241290530100U, (uint64_t)12626770134810813246U,
+ (uint64_t)10793074474236419890U, (uint64_t)11323224347913978783U,
+ (uint64_t)16831128015895380245U, (uint64_t)18323094195124693378U,
+ (uint64_t)2361097165281567692U, (uint64_t)15755578675014279498U,
+ (uint64_t)14289876470325854580U, (uint64_t)12856787656093616839U,
+ (uint64_t)3578928531243900594U, (uint64_t)3847532758790503699U, (uint64_t)8377953190224748743U,
+ (uint64_t)3314546646092744596U, (uint64_t)800810188859334358U, (uint64_t)4626344124229343596U,
+ (uint64_t)6620381605850876621U, (uint64_t)11422073570955989527U,
+ (uint64_t)12676813626484814469U, (uint64_t)16725029886764122240U,
+ (uint64_t)16648497372773830008U, (uint64_t)9135702594931291048U,
+ (uint64_t)16080949688826680333U, (uint64_t)11528096561346602947U,
+ (uint64_t)2632498067099740984U, (uint64_t)11583842699108800714U, (uint64_t)8378404864573610526U,
+ (uint64_t)1076560261627788534U, (uint64_t)13836015994325032828U,
+ (uint64_t)11234295937817067909U, (uint64_t)5893659808396722708U,
+ (uint64_t)11277421142886984364U, (uint64_t)8968549037166726491U,
+ (uint64_t)14841374331394032822U, (uint64_t)9967344773947889341U, (uint64_t)8799244393578496085U,
+ (uint64_t)5094686877301601410U, (uint64_t)8780316747074726862U, (uint64_t)9119697306829835718U,
+ (uint64_t)15381243327921855368U, (uint64_t)2686250164449435196U,
+ (uint64_t)16466917280442198358U, (uint64_t)13791704489163125216U,
+ (uint64_t)16955859337117924272U, (uint64_t)17112836394923783642U,
+ (uint64_t)4639176427338618063U, (uint64_t)16770029310141094964U,
+ (uint64_t)11049953922966416185U, (uint64_t)12012669590884098968U,
+ (uint64_t)4859326885929417214U, (uint64_t)896380084392586061U, (uint64_t)7153028362977034008U,
+ (uint64_t)10540021163316263301U, (uint64_t)9318277998512936585U,
+ (uint64_t)18344496977694796523U, (uint64_t)11374737400567645494U,
+ (uint64_t)17158800051138212954U, (uint64_t)18343197867863253153U,
+ (uint64_t)18204799297967861226U, (uint64_t)15798973531606348828U,
+ (uint64_t)9870158263408310459U, (uint64_t)17578869832774612627U, (uint64_t)8395748875822696932U,
+ (uint64_t)15310679007370670872U, (uint64_t)11205576736030808860U,
+ (uint64_t)10123429210002838967U, (uint64_t)5910544144088393959U,
+ (uint64_t)14016615653353687369U, (uint64_t)11191676704772957822U
+ };
+
+static const uint64_t
+ Hacl_P256_PrecompTable_precomp_g_pow2_192_table_w4[192U] = {
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)1U,
+ (uint64_t)18446744069414584320U, (uint64_t)18446744073709551615U, (uint64_t)4294967294U,
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)7870395003430845958U,
+ (uint64_t)18001862936410067720U, (uint64_t)8006461232116967215U, (uint64_t)5921313779532424762U,
+ (uint64_t)10702113371959864307U, (uint64_t)8070517410642379879U, (uint64_t)7139806720777708306U,
+ (uint64_t)8253938546650739833U, (uint64_t)17490482834545705718U, (uint64_t)1065249776797037500U,
+ (uint64_t)5018258455937968775U, (uint64_t)14100621120178668337U, (uint64_t)8392845221328116213U,
+ (uint64_t)14630296398338540788U, (uint64_t)4268947906723414372U, (uint64_t)9231207002243517909U,
+ (uint64_t)14261219637616504262U, (uint64_t)7786881626982345356U,
+ (uint64_t)11412720751765882139U, (uint64_t)14119585051365330009U,
+ (uint64_t)15281626286521302128U, (uint64_t)6350171933454266732U,
+ (uint64_t)16559468304937127866U, (uint64_t)13200760478271693417U,
+ (uint64_t)6733381546280350776U, (uint64_t)3801404890075189193U, (uint64_t)2741036364686993903U,
+ (uint64_t)3218612940540174008U, (uint64_t)10894914335165419505U,
+ (uint64_t)11862941430149998362U, (uint64_t)4223151729402839584U, (uint64_t)2913215088487087887U,
+ (uint64_t)14562168920104952953U, (uint64_t)2170089393468287453U,
+ (uint64_t)10520900655016579352U, (uint64_t)7040362608949989273U, (uint64_t)8376510559381705307U,
+ (uint64_t)9142237200448131532U, (uint64_t)5696859948123854080U, (uint64_t)925422306716081180U,
+ (uint64_t)11155545953469186421U, (uint64_t)1888208646862572812U,
+ (uint64_t)11151095998248845721U, (uint64_t)15793503271680275267U,
+ (uint64_t)7729877044494854851U, (uint64_t)6235134673193032913U, (uint64_t)7364280682182401564U,
+ (uint64_t)5479679373325519985U, (uint64_t)17966037684582301763U,
+ (uint64_t)14140891609330279185U, (uint64_t)5814744449740463867U, (uint64_t)5652588426712591652U,
+ (uint64_t)774745682988690912U, (uint64_t)13228255573220500373U, (uint64_t)11949122068786859397U,
+ (uint64_t)8021166392900770376U, (uint64_t)7994323710948720063U, (uint64_t)9924618472877849977U,
+ (uint64_t)17618517523141194266U, (uint64_t)2750424097794401714U,
+ (uint64_t)15481749570715253207U, (uint64_t)14646964509921760497U,
+ (uint64_t)1037442848094301355U, (uint64_t)6295995947389299132U, (uint64_t)16915049722317579514U,
+ (uint64_t)10493877400992990313U, (uint64_t)18391008753060553521U, (uint64_t)483942209623707598U,
+ (uint64_t)2017775662838016613U, (uint64_t)5933251998459363553U, (uint64_t)11789135019970707407U,
+ (uint64_t)5484123723153268336U, (uint64_t)13246954648848484954U, (uint64_t)4774374393926023505U,
+ (uint64_t)14863995618704457336U, (uint64_t)13220153167104973625U,
+ (uint64_t)5988445485312390826U, (uint64_t)17580359464028944682U, (uint64_t)7297100131969874771U,
+ (uint64_t)379931507867989375U, (uint64_t)10927113096513421444U, (uint64_t)17688881974428340857U,
+ (uint64_t)4259872578781463333U, (uint64_t)8573076295966784472U, (uint64_t)16389829450727275032U,
+ (uint64_t)1667243868963568259U, (uint64_t)17730726848925960919U,
+ (uint64_t)11408899874569778008U, (uint64_t)3576527582023272268U,
+ (uint64_t)16492920640224231656U, (uint64_t)7906130545972460130U,
+ (uint64_t)13878604278207681266U, (uint64_t)41446695125652041U, (uint64_t)8891615271337333503U,
+ (uint64_t)2594537723613594470U, (uint64_t)7699579176995770924U, (uint64_t)147458463055730655U,
+ (uint64_t)12120406862739088406U, (uint64_t)12044892493010567063U,
+ (uint64_t)8554076749615475136U, (uint64_t)1005097692260929999U, (uint64_t)2687202654471188715U,
+ (uint64_t)9457588752176879209U, (uint64_t)17472884880062444019U, (uint64_t)9792097892056020166U,
+ (uint64_t)2525246678512797150U, (uint64_t)15958903035313115662U,
+ (uint64_t)11336038170342247032U, (uint64_t)11560342382835141123U,
+ (uint64_t)6212009033479929024U, (uint64_t)8214308203775021229U, (uint64_t)8475469210070503698U,
+ (uint64_t)13287024123485719563U, (uint64_t)12956951963817520723U,
+ (uint64_t)10693035819908470465U, (uint64_t)11375478788224786725U,
+ (uint64_t)16934625208487120398U, (uint64_t)10094585729115874495U,
+ (uint64_t)2763884524395905776U, (uint64_t)13535890148969964883U,
+ (uint64_t)13514657411765064358U, (uint64_t)9903074440788027562U,
+ (uint64_t)17324720726421199990U, (uint64_t)2273931039117368789U, (uint64_t)3442641041506157854U,
+ (uint64_t)1119853641236409612U, (uint64_t)12037070344296077989U, (uint64_t)581736433335671746U,
+ (uint64_t)6019150647054369174U, (uint64_t)14864096138068789375U, (uint64_t)6652995210998318662U,
+ (uint64_t)12773883697029175304U, (uint64_t)12751275631451845119U,
+ (uint64_t)11449095003038250478U, (uint64_t)1025805267334366480U, (uint64_t)2764432500300815015U,
+ (uint64_t)18274564429002844381U, (uint64_t)10445634195592600351U,
+ (uint64_t)11814099592837202735U, (uint64_t)5006796893679120289U, (uint64_t)6908397253997261914U,
+ (uint64_t)13266696965302879279U, (uint64_t)7768715053015037430U, (uint64_t)3569923738654785686U,
+ (uint64_t)5844853453464857549U, (uint64_t)1837340805629559110U, (uint64_t)1034657624388283114U,
+ (uint64_t)711244516069456460U, (uint64_t)12519286026957934814U, (uint64_t)2613464944620837619U,
+ (uint64_t)10003023321338286213U, (uint64_t)7291332092642881376U, (uint64_t)9832199564117004897U,
+ (uint64_t)3280736694860799890U, (uint64_t)6416452202849179874U, (uint64_t)7326961381798642069U,
+ (uint64_t)8435688798040635029U, (uint64_t)16630141263910982958U,
+ (uint64_t)17222635514422533318U, (uint64_t)9482787389178881499U, (uint64_t)836561194658263905U,
+ (uint64_t)3405319043337616649U, (uint64_t)2786146577568026518U, (uint64_t)7625483685691626321U,
+ (uint64_t)6728084875304656716U, (uint64_t)1140997959232544268U, (uint64_t)12847384827606303792U,
+ (uint64_t)1719121337754572070U, (uint64_t)12863589482936438532U, (uint64_t)3880712899640530862U,
+ (uint64_t)2748456882813671564U, (uint64_t)4775988900044623019U, (uint64_t)8937847374382191162U,
+ (uint64_t)3767367347172252295U, (uint64_t)13468672401049388646U,
+ (uint64_t)14359032216842397576U, (uint64_t)2002555958685443975U,
+ (uint64_t)16488678606651526810U, (uint64_t)11826135409597474760U,
+ (uint64_t)15296495673182508601U
+ };
+
+static const uint64_t
+ Hacl_P256_PrecompTable_precomp_basepoint_table_w5[384U] = {
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)1U,
+ (uint64_t)18446744069414584320U, (uint64_t)18446744073709551615U, (uint64_t)4294967294U,
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)8784043285714375740U,
+ (uint64_t)8483257759279461889U, (uint64_t)8789745728267363600U, (uint64_t)1770019616739251654U,
+ (uint64_t)15992936863339206154U, (uint64_t)10037038012062884956U,
+ (uint64_t)15197544864945402661U, (uint64_t)9615747158586711429U, (uint64_t)1U,
+ (uint64_t)18446744069414584320U, (uint64_t)18446744073709551615U, (uint64_t)4294967294U,
+ (uint64_t)10634854829044225757U, (uint64_t)351552716085025155U, (uint64_t)10645315080955407736U,
+ (uint64_t)3609262091244858135U, (uint64_t)15760741698986874125U,
+ (uint64_t)14936374388219697827U, (uint64_t)15751360096993017895U,
+ (uint64_t)18012233706239762398U, (uint64_t)1993877568177495041U,
+ (uint64_t)10345888787846536528U, (uint64_t)7746511691117935375U,
+ (uint64_t)14517043990409914413U, (uint64_t)14122549297570634151U,
+ (uint64_t)16934610359517083771U, (uint64_t)5724511325497097418U, (uint64_t)8983432969107448705U,
+ (uint64_t)2687429970334080245U, (uint64_t)16525396802810050288U, (uint64_t)7602596488871585854U,
+ (uint64_t)4813919589149203084U, (uint64_t)7680395813780804519U, (uint64_t)6687709583048023590U,
+ (uint64_t)18086445169104142027U, (uint64_t)9637814708330203929U,
+ (uint64_t)14785108459960679090U, (uint64_t)3838023279095023581U, (uint64_t)3555615526157830307U,
+ (uint64_t)5177066488380472871U, (uint64_t)18218186719108038403U,
+ (uint64_t)16281556341699656105U, (uint64_t)1524227924561461191U, (uint64_t)4148060517641909597U,
+ (uint64_t)2858290374115363433U, (uint64_t)8942772026334130620U, (uint64_t)3034451298319885113U,
+ (uint64_t)8447866036736640940U, (uint64_t)11204933433076256578U,
+ (uint64_t)18333595740249588297U, (uint64_t)8259597024804538246U, (uint64_t)9539734295777539786U,
+ (uint64_t)9797290423046626413U, (uint64_t)5777303437849646537U, (uint64_t)8739356909899132020U,
+ (uint64_t)14815960973766782158U, (uint64_t)15286581798204509801U,
+ (uint64_t)17597362577777019682U, (uint64_t)13259283710820519742U,
+ (uint64_t)10501322996899164670U, (uint64_t)1221138904338319642U,
+ (uint64_t)14586685489551951885U, (uint64_t)895326705426031212U, (uint64_t)14398171728560617847U,
+ (uint64_t)9592550823745097391U, (uint64_t)17240998489162206026U, (uint64_t)8085479283308189196U,
+ (uint64_t)14844657737893882826U, (uint64_t)15923425394150618234U,
+ (uint64_t)2997808084773249525U, (uint64_t)494323555453660587U, (uint64_t)1215695327517794764U,
+ (uint64_t)9476207381098391690U, (uint64_t)7480789678419122995U, (uint64_t)15212230329321082489U,
+ (uint64_t)436189395349576388U, (uint64_t)17377474396456660834U, (uint64_t)15237013929655017939U,
+ (uint64_t)11444428846883781676U, (uint64_t)5112749694521428575U, (uint64_t)950829367509872073U,
+ (uint64_t)17665036182057559519U, (uint64_t)17205133339690002313U,
+ (uint64_t)16233765170251334549U, (uint64_t)10122775683257972591U,
+ (uint64_t)3352514236455632420U, (uint64_t)9143148522359954691U, (uint64_t)601191684005658860U,
+ (uint64_t)13398772186646349998U, (uint64_t)15512696600132928431U,
+ (uint64_t)9128416073728948653U, (uint64_t)11233051033546138578U, (uint64_t)6769345682610122833U,
+ (uint64_t)10823233224575054288U, (uint64_t)9997725227559980175U, (uint64_t)6733425642852897415U,
+ (uint64_t)16302206918151466066U, (uint64_t)1669330822143265921U, (uint64_t)2661645605036546002U,
+ (uint64_t)17182558479745802165U, (uint64_t)1165082692376932040U, (uint64_t)9470595929011488359U,
+ (uint64_t)6142147329285324932U, (uint64_t)4829075085998111287U, (uint64_t)10231370681107338930U,
+ (uint64_t)9591876895322495239U, (uint64_t)10316468561384076618U,
+ (uint64_t)11592503647238064235U, (uint64_t)13395813606055179632U, (uint64_t)511127033980815508U,
+ (uint64_t)12434976573147649880U, (uint64_t)3425094795384359127U, (uint64_t)6816971736303023445U,
+ (uint64_t)15444670609021139344U, (uint64_t)9464349818322082360U,
+ (uint64_t)16178216413042376883U, (uint64_t)9595540370774317348U, (uint64_t)7229365182662875710U,
+ (uint64_t)4601177649460012843U, (uint64_t)5455046447382487090U, (uint64_t)10854066421606187521U,
+ (uint64_t)15913416821879788071U, (uint64_t)2297365362023460173U, (uint64_t)2603252216454941350U,
+ (uint64_t)6768791943870490934U, (uint64_t)15705936687122754810U, (uint64_t)9537096567546600694U,
+ (uint64_t)17580538144855035062U, (uint64_t)4496542856965746638U, (uint64_t)8444341625922124942U,
+ (uint64_t)12191263903636183168U, (uint64_t)17427332907535974165U,
+ (uint64_t)14307569739254103736U, (uint64_t)13900598742063266169U,
+ (uint64_t)7176996424355977650U, (uint64_t)5709008170379717479U, (uint64_t)14471312052264549092U,
+ (uint64_t)1464519909491759867U, (uint64_t)3328154641049602121U, (uint64_t)13020349337171136774U,
+ (uint64_t)2772166279972051938U, (uint64_t)10854476939425975292U, (uint64_t)1967189930534630940U,
+ (uint64_t)2802919076529341959U, (uint64_t)14792226094833519208U,
+ (uint64_t)14675640928566522177U, (uint64_t)14838974364643800837U,
+ (uint64_t)17631460696099549980U, (uint64_t)17434186275364935469U,
+ (uint64_t)2665648200587705473U, (uint64_t)13202122464492564051U, (uint64_t)7576287350918073341U,
+ (uint64_t)2272206013910186424U, (uint64_t)14558761641743937843U, (uint64_t)5675729149929979729U,
+ (uint64_t)9043135187561613166U, (uint64_t)11750149293830589225U, (uint64_t)740555197954307911U,
+ (uint64_t)9871738005087190699U, (uint64_t)17178667634283502053U,
+ (uint64_t)18046255991533013265U, (uint64_t)4458222096988430430U, (uint64_t)8452427758526311627U,
+ (uint64_t)13825286929656615266U, (uint64_t)13956286357198391218U,
+ (uint64_t)15875692916799995079U, (uint64_t)10634895319157013920U,
+ (uint64_t)13230116118036304207U, (uint64_t)8795317393614625606U, (uint64_t)7001710806858862020U,
+ (uint64_t)7949746088586183478U, (uint64_t)14677556044923602317U,
+ (uint64_t)11184023437485843904U, (uint64_t)11215864722023085094U,
+ (uint64_t)6444464081471519014U, (uint64_t)1706241174022415217U, (uint64_t)8243975633057550613U,
+ (uint64_t)15502902453836085864U, (uint64_t)3799182188594003953U, (uint64_t)3538840175098724094U,
+ (uint64_t)13240193491554624643U, (uint64_t)12365034249541329920U,
+ (uint64_t)2924326828590977357U, (uint64_t)5687195797140589099U, (uint64_t)16880427227292834531U,
+ (uint64_t)9691471435758991112U, (uint64_t)16642385273732487288U,
+ (uint64_t)12173806747523009914U, (uint64_t)13142722756877876849U,
+ (uint64_t)8370377548305121979U, (uint64_t)17988526053752025426U, (uint64_t)4818750752684100334U,
+ (uint64_t)5669241919350361655U, (uint64_t)4964810303238518540U, (uint64_t)16709712747671533191U,
+ (uint64_t)4461414404267448242U, (uint64_t)3971798785139504238U, (uint64_t)6276818948740422136U,
+ (uint64_t)1426735892164275762U, (uint64_t)7943622674892418919U, (uint64_t)9864274225563929680U,
+ (uint64_t)57815533745003233U, (uint64_t)10893588105168960233U, (uint64_t)15739162732907069535U,
+ (uint64_t)3923866849462073470U, (uint64_t)12279826158399226875U, (uint64_t)1533015761334846582U,
+ (uint64_t)15860156818568437510U, (uint64_t)8252625373831297988U, (uint64_t)9666953804812706358U,
+ (uint64_t)8767785238646914634U, (uint64_t)14382179044941403551U,
+ (uint64_t)10401039907264254245U, (uint64_t)8584860003763157350U, (uint64_t)3120462679504470266U,
+ (uint64_t)8670255778748340069U, (uint64_t)5313789577940369984U, (uint64_t)16977072364454789224U,
+ (uint64_t)12199578693972188324U, (uint64_t)18211098771672599237U,
+ (uint64_t)12868831556008795030U, (uint64_t)5310155061431048194U,
+ (uint64_t)18114153238435112606U, (uint64_t)14482365809278304512U,
+ (uint64_t)12520721662723001511U, (uint64_t)405943624021143002U, (uint64_t)8146944101507657423U,
+ (uint64_t)181739317780393495U, (uint64_t)81743892273670099U, (uint64_t)14759561962550473930U,
+ (uint64_t)4592623849546992939U, (uint64_t)6916440441743449719U, (uint64_t)1304610503530809833U,
+ (uint64_t)5464930909232486441U, (uint64_t)15414883617496224671U, (uint64_t)8129283345256790U,
+ (uint64_t)18294252198413739489U, (uint64_t)17394115281884857288U,
+ (uint64_t)7808348415224731235U, (uint64_t)13195566655747230608U, (uint64_t)8568194219353949094U,
+ (uint64_t)15329813048672122440U, (uint64_t)9604275495885785744U, (uint64_t)1577712551205219835U,
+ (uint64_t)15964209008022052790U, (uint64_t)15087297920782098160U,
+ (uint64_t)3946031512438511898U, (uint64_t)10050061168984440631U,
+ (uint64_t)11382452014533138316U, (uint64_t)6313670788911952792U,
+ (uint64_t)12015989229696164014U, (uint64_t)5946702628076168852U, (uint64_t)5219995658774362841U,
+ (uint64_t)12230141881068377972U, (uint64_t)12361195202673441956U,
+ (uint64_t)4732862275653856711U, (uint64_t)17221430380805252370U,
+ (uint64_t)15397525953897375810U, (uint64_t)16557437297239563045U,
+ (uint64_t)10101683801868971351U, (uint64_t)1402611372245592868U, (uint64_t)1931806383735563658U,
+ (uint64_t)10991705207471512479U, (uint64_t)861333583207471392U, (uint64_t)15207766844626322355U,
+ (uint64_t)9224628129811432393U, (uint64_t)3497069567089055613U, (uint64_t)11956632757898590316U,
+ (uint64_t)8733729372586312960U, (uint64_t)18091521051714930927U, (uint64_t)77582787724373283U,
+ (uint64_t)9922437373519669237U, (uint64_t)3079321456325704615U, (uint64_t)12171198408512478457U,
+ (uint64_t)17179130884012147596U, (uint64_t)6839115479620367181U, (uint64_t)4421032569964105406U,
+ (uint64_t)10353331468657256053U, (uint64_t)17400988720335968824U,
+ (uint64_t)17138855889417480540U, (uint64_t)4507980080381370611U,
+ (uint64_t)10703175719793781886U, (uint64_t)12598516658725890426U,
+ (uint64_t)8353463412173898932U, (uint64_t)17703029389228422404U, (uint64_t)9313111267107226233U,
+ (uint64_t)5441322942995154196U, (uint64_t)8952817660034465484U, (uint64_t)17571113341183703118U,
+ (uint64_t)7375087953801067019U, (uint64_t)13381466302076453648U, (uint64_t)3218165271423914596U,
+ (uint64_t)16956372157249382685U, (uint64_t)509080090049418841U, (uint64_t)13374233893294084913U,
+ (uint64_t)2988537624204297086U, (uint64_t)4979195832939384620U, (uint64_t)3803931594068976394U,
+ (uint64_t)10731535883829627646U, (uint64_t)12954845047607194278U,
+ (uint64_t)10494298062560667399U, (uint64_t)4967351022190213065U,
+ (uint64_t)13391917938145756456U, (uint64_t)951370484866918160U, (uint64_t)13531334179067685307U,
+ (uint64_t)12868421357919390599U, (uint64_t)15918857042998130258U,
+ (uint64_t)17769743831936974016U, (uint64_t)7137921979260368809U,
+ (uint64_t)12461369180685892062U, (uint64_t)827476514081935199U, (uint64_t)15107282134224767230U,
+ (uint64_t)10084765752802805748U, (uint64_t)3303739059392464407U,
+ (uint64_t)17859532612136591428U, (uint64_t)10949414770405040164U,
+ (uint64_t)12838613589371008785U, (uint64_t)5554397169231540728U,
+ (uint64_t)18375114572169624408U, (uint64_t)15649286703242390139U,
+ (uint64_t)2957281557463706877U, (uint64_t)14000350446219393213U,
+ (uint64_t)14355199721749620351U, (uint64_t)2730856240099299695U,
+ (uint64_t)17528131000714705752U, (uint64_t)2537498525883536360U, (uint64_t)6121058967084509393U,
+ (uint64_t)16897667060435514221U, (uint64_t)12367869599571112440U,
+ (uint64_t)3388831797050807508U, (uint64_t)16791449724090982798U, (uint64_t)2673426123453294928U,
+ (uint64_t)11369313542384405846U, (uint64_t)15641960333586432634U,
+ (uint64_t)15080962589658958379U, (uint64_t)7747943772340226569U, (uint64_t)8075023376199159152U,
+ (uint64_t)8485093027378306528U, (uint64_t)13503706844122243648U, (uint64_t)8401961362938086226U,
+ (uint64_t)8125426002124226402U, (uint64_t)9005399361407785203U, (uint64_t)6847968030066906634U,
+ (uint64_t)11934937736309295197U, (uint64_t)5116750888594772351U, (uint64_t)2817039227179245227U,
+ (uint64_t)17724206901239332980U, (uint64_t)4985702708254058578U, (uint64_t)5786345435756642871U,
+ (uint64_t)17772527414940936938U, (uint64_t)1201320251272957006U,
+ (uint64_t)15787430120324348129U, (uint64_t)6305488781359965661U,
+ (uint64_t)12423900845502858433U, (uint64_t)17485949424202277720U,
+ (uint64_t)2062237315546855852U, (uint64_t)10353639467860902375U, (uint64_t)2315398490451287299U,
+ (uint64_t)15394572894814882621U, (uint64_t)232866113801165640U, (uint64_t)7413443736109338926U,
+ (uint64_t)902719806551551191U, (uint64_t)16568853118619045174U, (uint64_t)14202214862428279177U,
+ (uint64_t)11719595395278861192U, (uint64_t)5890053236389907647U, (uint64_t)9996196494965833627U,
+ (uint64_t)12967056942364782577U, (uint64_t)9034128755157395787U,
+ (uint64_t)17898204904710512655U, (uint64_t)8229373445062993977U,
+ (uint64_t)13580036169519833644U
+ };
+
+#if defined(__cplusplus)
+}
+#endif
+
+#define __internal_Hacl_P256_PrecompTable_H_DEFINED
+#endif
diff --git a/lib/freebl/verified/internal/lib_intrinsics.h b/lib/freebl/verified/internal/lib_intrinsics.h
new file mode 100644
--- /dev/null
+++ b/lib/freebl/verified/internal/lib_intrinsics.h
@@ -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 --git a/lib/freebl/verified/karamel/include/krml/internal/target.h b/lib/freebl/verified/karamel/include/krml/internal/target.h
--- a/lib/freebl/verified/karamel/include/krml/internal/target.h
+++ b/lib/freebl/verified/karamel/include/krml/internal/target.h
@@ -1,21 +1,21 @@
/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
Licensed under the Apache 2.0 License. */
#ifndef __KRML_TARGET_H
#define __KRML_TARGET_H
-#include <stdlib.h>
+#include <assert.h>
+#include <inttypes.h>
+#include <limits.h>
+#include <stdbool.h>
#include <stddef.h>
#include <stdio.h>
-#include <stdbool.h>
-#include <inttypes.h>
-#include <limits.h>
-#include <assert.h>
+#include <stdlib.h>
/* Since KaRaMeL emits the inline keyword unconditionally, we follow the
* guidelines at https://gcc.gnu.org/onlinedocs/gcc/Inline.html and make this
* __inline__ to ensure the code compiles with -std=c90 and earlier. */
#ifdef __GNUC__
#define inline __inline__
#endif
@@ -52,16 +52,29 @@
#ifndef KRML_HOST_FREE
#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))
#else
#define KRML_PRE_ALIGN(X)
#endif
#endif
@@ -75,32 +88,36 @@
/* MinGW-W64 does not support C11 aligned_alloc, but it supports
* MSVC's _aligned_malloc.
*/
#ifndef KRML_ALIGNED_MALLOC
#ifdef __MINGW32__
#include <_mingw.h>
#endif
-#if (defined(_MSC_VER) || (defined(__MINGW32__) && defined(__MINGW64_VERSION_MAJOR)))
+#if ( \
+ defined(_MSC_VER) || \
+ (defined(__MINGW32__) && defined(__MINGW64_VERSION_MAJOR)))
#define KRML_ALIGNED_MALLOC(X, Y) _aligned_malloc(Y, X)
#else
#define KRML_ALIGNED_MALLOC(X, Y) aligned_alloc(X, Y)
#endif
#endif
/* Since aligned allocations with MinGW-W64 are done with
* _aligned_malloc (see above), such pointers must be freed with
* _aligned_free.
*/
#ifndef KRML_ALIGNED_FREE
#ifdef __MINGW32__
#include <_mingw.h>
#endif
-#if (defined(_MSC_VER) || (defined(__MINGW32__) && defined(__MINGW64_VERSION_MAJOR)))
+#if ( \
+ defined(_MSC_VER) || \
+ (defined(__MINGW32__) && defined(__MINGW64_VERSION_MAJOR)))
#define KRML_ALIGNED_FREE(X) _aligned_free(X)
#else
#define KRML_ALIGNED_FREE(X) free(X)
#endif
#endif
#ifndef KRML_HOST_TIME
@@ -148,17 +165,18 @@ krml_time(void)
"Maximum allocatable size exceeded, aborting before overflow at " \
"%s:%d\n", \
__FILE__, __LINE__); \
KRML_HOST_EXIT(253); \
} \
} while (0)
#if defined(_MSC_VER) && _MSC_VER < 1900
-#define KRML_HOST_SNPRINTF(buf, sz, fmt, arg) _snprintf_s(buf, sz, _TRUNCATE, fmt, arg)
+#define KRML_HOST_SNPRINTF(buf, sz, fmt, arg) \
+ _snprintf_s(buf, sz, _TRUNCATE, fmt, arg)
#else
#define KRML_HOST_SNPRINTF(buf, sz, fmt, arg) snprintf(buf, sz, fmt, arg)
#endif
#if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ > 4))
#define KRML_DEPRECATED(x) __attribute__((deprecated(x)))
#elif defined(__GNUC__)
/* deprecated attribute is not defined in GCC < 4.5. */
@@ -167,16 +185,17 @@ krml_time(void)
#define KRML_DEPRECATED(x) __declspec(deprecated(x))
#endif
/* Macros for prettier unrolling of loops */
#define KRML_LOOP1(i, n, x) \
{ \
x \
i += n; \
+ (void)i; \
}
#define KRML_LOOP2(i, n, x) \
KRML_LOOP1(i, n, x) \
KRML_LOOP1(i, n, x)
#define KRML_LOOP3(i, n, x) \
KRML_LOOP2(i, n, x) \
diff --git a/lib/freebl/verified/karamel/krmllib/dist/minimal/FStar_UInt_8_16_32_64.h b/lib/freebl/verified/karamel/krmllib/dist/minimal/FStar_UInt_8_16_32_64.h
--- a/lib/freebl/verified/karamel/krmllib/dist/minimal/FStar_UInt_8_16_32_64.h
+++ b/lib/freebl/verified/karamel/krmllib/dist/minimal/FStar_UInt_8_16_32_64.h
@@ -8,25 +8,35 @@
#include <inttypes.h>
#include <stdbool.h>
#include "krml/internal/compat.h"
#include "krml/lowstar_endianness.h"
#include "krml/internal/types.h"
#include "krml/internal/target.h"
-extern Prims_int FStar_UInt64_n;
+#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;
extern uint64_t FStar_UInt64_one;
extern uint64_t FStar_UInt64_minus(uint64_t a);
extern uint32_t FStar_UInt64_n_minus_one;
@@ -58,25 +68,25 @@ FStar_UInt64_gte_mask(uint64_t a, uint64
extern Prims_string FStar_UInt64_to_string(uint64_t uu___);
extern Prims_string FStar_UInt64_to_string_hex(uint64_t uu___);
extern Prims_string FStar_UInt64_to_string_hex_pad(uint64_t uu___);
extern uint64_t FStar_UInt64_of_string(Prims_string uu___);
-extern Prims_int FStar_UInt32_n;
+extern 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;
extern uint32_t FStar_UInt32_one;
extern uint32_t FStar_UInt32_minus(uint32_t a);
extern uint32_t FStar_UInt32_n_minus_one;
@@ -108,25 +118,25 @@ FStar_UInt32_gte_mask(uint32_t a, uint32
extern Prims_string FStar_UInt32_to_string(uint32_t uu___);
extern Prims_string FStar_UInt32_to_string_hex(uint32_t uu___);
extern Prims_string FStar_UInt32_to_string_hex_pad(uint32_t uu___);
extern uint32_t FStar_UInt32_of_string(Prims_string uu___);
-extern Prims_int FStar_UInt16_n;
+extern 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;
extern uint16_t FStar_UInt16_one;
extern uint16_t FStar_UInt16_minus(uint16_t a);
extern uint32_t FStar_UInt16_n_minus_one;
@@ -158,25 +168,25 @@ FStar_UInt16_gte_mask(uint16_t a, uint16
extern Prims_string FStar_UInt16_to_string(uint16_t uu___);
extern Prims_string FStar_UInt16_to_string_hex(uint16_t uu___);
extern Prims_string FStar_UInt16_to_string_hex_pad(uint16_t uu___);
extern uint16_t FStar_UInt16_of_string(Prims_string uu___);
-extern Prims_int FStar_UInt8_n;
+extern 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;
extern uint8_t FStar_UInt8_one;
extern uint8_t FStar_UInt8_minus(uint8_t a);
extern uint32_t FStar_UInt8_n_minus_one;
@@ -210,10 +220,18 @@ extern Prims_string FStar_UInt8_to_strin
extern Prims_string FStar_UInt8_to_string_hex(uint8_t uu___);
extern Prims_string FStar_UInt8_to_string_hex_pad(uint8_t uu___);
extern uint8_t FStar_UInt8_of_string(Prims_string uu___);
typedef uint8_t FStar_UInt8_byte;
+#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
Reference in New Issue View Git Blame Copy Permalink