summaryrefslogtreecommitdiffstats
path: root/security/nss/lib
diff options
context:
space:
mode:
Diffstat (limited to 'security/nss/lib')
-rw-r--r--security/nss/lib/cryptohi/keythi.h1
-rw-r--r--security/nss/lib/cryptohi/seckey.c129
-rw-r--r--security/nss/lib/cryptohi/secvfy.c2
-rw-r--r--security/nss/lib/freebl/Hacl_Hash_SHA2_shim.h38
-rw-r--r--security/nss/lib/freebl/Makefile3
-rw-r--r--security/nss/lib/freebl/blapi.h21
-rw-r--r--security/nss/lib/freebl/blapit.h5
-rw-r--r--security/nss/lib/freebl/ec.c142
-rw-r--r--security/nss/lib/freebl/ec.h4
-rw-r--r--security/nss/lib/freebl/ecdecode.c15
-rw-r--r--security/nss/lib/freebl/ecl/ecl-curve.h10
-rw-r--r--security/nss/lib/freebl/ecl/ecl-exp.h1
-rw-r--r--security/nss/lib/freebl/freebl_base.gypi2
-rw-r--r--security/nss/lib/freebl/ldvector.c5
-rw-r--r--security/nss/lib/freebl/loader.c28
-rw-r--r--security/nss/lib/freebl/loader.h7
-rw-r--r--security/nss/lib/freebl/verified/Hacl_Chacha20_Vec128.c6
-rw-r--r--security/nss/lib/freebl/verified/Hacl_Chacha20_Vec256.c6
-rw-r--r--security/nss/lib/freebl/verified/Hacl_Curve25519_64.c18
-rw-r--r--security/nss/lib/freebl/verified/Hacl_Ed25519.c1853
-rw-r--r--security/nss/lib/freebl/verified/Hacl_Ed25519.h114
-rw-r--r--security/nss/lib/freebl/verified/Hacl_Hash_SHA3.c7
-rw-r--r--security/nss/lib/freebl/verified/internal/Hacl_Bignum25519_51.h4
-rw-r--r--security/nss/lib/freebl/verified/internal/Hacl_Ed25519.h73
-rw-r--r--security/nss/lib/freebl/verified/internal/Hacl_Ed25519_PrecompTable.h687
-rw-r--r--security/nss/lib/freebl/verified/karamel/include/krml/internal/target.h8
-rw-r--r--security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/fstar_uint128_gcc64.h4
-rw-r--r--security/nss/lib/nss/nss.h4
-rw-r--r--security/nss/lib/pk11wrap/pk11akey.c61
-rw-r--r--security/nss/lib/pk11wrap/pk11cert.c4
-rw-r--r--security/nss/lib/pk11wrap/pk11mech.c9
-rw-r--r--security/nss/lib/pk11wrap/pk11obj.c2
-rw-r--r--security/nss/lib/pk11wrap/pk11pars.c2
-rw-r--r--security/nss/lib/pk11wrap/pk11pk12.c80
-rw-r--r--security/nss/lib/pk11wrap/pk11skey.c5
-rw-r--r--security/nss/lib/pk11wrap/pk11slot.c3
-rw-r--r--security/nss/lib/smime/cms.h3
-rw-r--r--security/nss/lib/smime/cmsrecinfo.c24
-rw-r--r--security/nss/lib/smime/smime.def6
-rw-r--r--security/nss/lib/softoken/lowkey.c19
-rw-r--r--security/nss/lib/softoken/lowpbe.c17
-rw-r--r--security/nss/lib/softoken/pkcs11.c21
-rw-r--r--security/nss/lib/softoken/pkcs11c.c167
-rw-r--r--security/nss/lib/softoken/softkver.h4
-rw-r--r--security/nss/lib/ssl/ssl3ext.h10
-rw-r--r--security/nss/lib/ssl/sslexp.h8
-rw-r--r--security/nss/lib/ssl/sslimpl.h15
-rw-r--r--security/nss/lib/ssl/sslsock.c1
-rw-r--r--security/nss/lib/ssl/sslt.h17
-rw-r--r--security/nss/lib/util/nssutil.h4
-rw-r--r--security/nss/lib/util/secoid.c30
-rw-r--r--security/nss/lib/util/secoidt.h3
52 files changed, 3589 insertions, 123 deletions
diff --git a/security/nss/lib/cryptohi/keythi.h b/security/nss/lib/cryptohi/keythi.h
index 1dd8a557c5..086d83ae6b 100644
--- a/security/nss/lib/cryptohi/keythi.h
+++ b/security/nss/lib/cryptohi/keythi.h
@@ -36,6 +36,7 @@ typedef enum {
rsaPssKey = 7,
rsaOaepKey = 8,
kyberKey = 9,
+ edKey = 10,
} KeyType;
/*
diff --git a/security/nss/lib/cryptohi/seckey.c b/security/nss/lib/cryptohi/seckey.c
index 1762c1a143..1a68104978 100644
--- a/security/nss/lib/cryptohi/seckey.c
+++ b/security/nss/lib/cryptohi/seckey.c
@@ -235,6 +235,33 @@ SECKEY_CreateECPrivateKey(SECKEYECParams *param, SECKEYPublicKey **pubk, void *c
return (privk);
}
+SECKEYPrivateKey *
+SECKEY_CreateEDPrivateKey(SECKEYECParams *param, SECKEYPublicKey **pubk, void *cx)
+{
+ SECKEYPrivateKey *privk;
+ PK11SlotInfo *slot = PK11_GetBestSlot(CKM_EC_EDWARDS_KEY_PAIR_GEN, cx);
+ if (!slot) {
+ return NULL;
+ }
+
+ privk = PK11_GenerateKeyPairWithOpFlags(slot, CKM_EC_EDWARDS_KEY_PAIR_GEN,
+ param, pubk,
+ PK11_ATTR_SESSION |
+ PK11_ATTR_INSENSITIVE |
+ PK11_ATTR_PUBLIC,
+ CKF_SIGN, CKF_SIGN, cx);
+ if (!privk)
+ privk = PK11_GenerateKeyPairWithOpFlags(slot, CKM_EC_EDWARDS_KEY_PAIR_GEN,
+ param, pubk,
+ PK11_ATTR_SESSION |
+ PK11_ATTR_SENSITIVE |
+ PK11_ATTR_PRIVATE,
+ CKF_SIGN, CKF_SIGN, cx);
+
+ PK11_FreeSlot(slot);
+ return (privk);
+}
+
void
SECKEY_DestroyPrivateKey(SECKEYPrivateKey *privk)
{
@@ -329,7 +356,7 @@ seckey_UpdateCertPQGChain(CERTCertificate *subjectCert, int count)
*
* Question: do we really need to do this for EC keys. They don't have
* PQG parameters, but they do have parameters. The question is does
- * the child cert inherit thost parameters for EC from the parent, or
+ * the child cert inherit those parameters for EC from the parent, or
* do we always include those parameters in each cert.
*/
@@ -339,6 +366,7 @@ seckey_UpdateCertPQGChain(CERTCertificate *subjectCert, int count)
(tag != SEC_OID_NIST_DSA_SIGNATURE_WITH_SHA256_DIGEST) &&
(tag != SEC_OID_BOGUS_DSA_SIGNATURE_WITH_SHA1_DIGEST) &&
(tag != SEC_OID_SDN702_DSA_SIGNATURE) &&
+ (tag != SEC_OID_ED25519_PUBLIC_KEY) &&
(tag != SEC_OID_ANSIX962_EC_PUBLIC_KEY)) {
return SECSuccess;
@@ -383,6 +411,7 @@ seckey_UpdateCertPQGChain(CERTCertificate *subjectCert, int count)
(tag != SEC_OID_NIST_DSA_SIGNATURE_WITH_SHA256_DIGEST) &&
(tag != SEC_OID_BOGUS_DSA_SIGNATURE_WITH_SHA1_DIGEST) &&
(tag != SEC_OID_SDN702_DSA_SIGNATURE) &&
+ (tag != SEC_OID_ED25519_PUBLIC_KEY) &&
(tag != SEC_OID_ANSIX962_EC_PUBLIC_KEY)) {
rv = SECFailure;
goto loser;
@@ -521,6 +550,9 @@ seckey_GetKeyType(SECOidTag tag)
case SEC_OID_ANSIX962_EC_PUBLIC_KEY:
keyType = ecKey;
break;
+ case SEC_OID_ED25519_PUBLIC_KEY:
+ keyType = edKey;
+ break;
/* accommodate applications that hand us a signature type when they
* should be handing us a cipher type */
case SEC_OID_PKCS1_MD5_WITH_RSA_ENCRYPTION:
@@ -637,6 +669,37 @@ seckey_ExtractPublicKey(const CERTSubjectPublicKeyInfo *spki)
if (rv == SECSuccess)
return pubk;
break;
+ case SEC_OID_ED25519_PUBLIC_KEY:
+ /* A basic consistency check on inputs. */
+ if (newOs.len == 0) {
+ PORT_SetError(SEC_ERROR_INPUT_LEN);
+ break;
+ }
+
+ /* Currently supporting only (Pure)Ed25519 .*/
+ if (spki->algorithm.parameters.len != 0) {
+ PORT_SetError(SEC_ERROR_UNSUPPORTED_KEYALG);
+ break;
+ }
+
+ pubk->keyType = edKey;
+ pubk->u.ec.size = 0;
+
+ SECOidData *oidEd25519 = SECOID_FindOIDByTag(SEC_OID_ED25519_PUBLIC_KEY);
+
+ if (!SECITEM_AllocItem(arena, &pubk->u.ec.DEREncodedParams, oidEd25519->oid.len + 2)) {
+ rv = SECFailure;
+ break;
+ }
+ pubk->u.ec.DEREncodedParams.data[0] = SEC_ASN1_OBJECT_ID;
+ pubk->u.ec.DEREncodedParams.data[1] = oidEd25519->oid.len;
+ PORT_Memcpy(pubk->u.ec.DEREncodedParams.data + 2, oidEd25519->oid.data, oidEd25519->oid.len);
+
+ rv = SECITEM_CopyItem(arena, &pubk->u.ec.publicValue, &newOs);
+ if (rv != SECSuccess) {
+ break;
+ }
+ return pubk;
case SEC_OID_ANSIX962_EC_PUBLIC_KEY:
/* A basic sanity check on inputs. */
if (spki->algorithm.parameters.len == 0 || newOs.len == 0) {
@@ -811,6 +874,7 @@ SECKEY_ECParamsToKeySize(const SECItem *encodedParams)
return 571;
case SEC_OID_CURVE25519:
+ case SEC_OID_ED25519_PUBLIC_KEY:
return 255;
default:
@@ -961,6 +1025,7 @@ SECKEY_ECParamsToBasePointOrderLen(const SECItem *encodedParams)
return 570;
case SEC_OID_CURVE25519:
+ case SEC_OID_ED25519_PUBLIC_KEY:
return 255;
default:
@@ -1032,6 +1097,7 @@ SECKEY_PublicKeyStrengthInBits(const SECKEYPublicKey *pubk)
bitSize = SECKEY_BigIntegerBitLength(&pubk->u.dh.prime);
break;
case ecKey:
+ case edKey:
bitSize = SECKEY_ECParamsToKeySize(&pubk->u.ec.DEREncodedParams);
break;
default:
@@ -1113,6 +1179,7 @@ SECKEY_SignatureLen(const SECKEYPublicKey *pubk)
case dsaKey:
return pubk->u.dsa.params.subPrime.len * 2;
case ecKey:
+ case edKey:
/* Get the base point order length in bits and adjust */
size = SECKEY_ECParamsToBasePointOrderLen(
&pubk->u.ec.DEREncodedParams);
@@ -1239,6 +1306,7 @@ SECKEY_CopyPublicKey(const SECKEYPublicKey *pubk)
&pubk->u.dh.publicValue);
break;
case ecKey:
+ case edKey:
copyk->u.ec.size = pubk->u.ec.size;
rv = seckey_HasCurveOID(pubk);
if (rv != SECSuccess) {
@@ -1465,6 +1533,28 @@ SECKEY_ConvertToPublicKey(SECKEYPrivateKey *privk)
* overwrite the old value */
pubk->u.ec.publicValue = decodedPoint;
}
+
+ pubk->u.ec.encoding = ECPoint_Undefined;
+ return pubk;
+ case edKey:
+ rv = PK11_ReadAttribute(privk->pkcs11Slot, privk->pkcs11ID,
+ CKA_EC_PARAMS, arena, &pubk->u.ec.DEREncodedParams);
+ if (rv != SECSuccess) {
+ break;
+ }
+ rv = PK11_ReadAttribute(privk->pkcs11Slot, privk->pkcs11ID,
+ CKA_EC_POINT, arena, &pubk->u.ec.publicValue);
+ if (rv != SECSuccess || pubk->u.ec.publicValue.len == 0) {
+ pubKeyHandle = seckey_FindPublicKeyHandle(privk, pubk);
+ if (pubKeyHandle == CK_INVALID_HANDLE) {
+ break;
+ }
+ rv = PK11_ReadAttribute(privk->pkcs11Slot, pubKeyHandle,
+ CKA_EC_POINT, arena, &pubk->u.ec.publicValue);
+ if (rv != SECSuccess) {
+ break;
+ }
+ }
pubk->u.ec.encoding = ECPoint_Undefined;
return pubk;
default:
@@ -1483,6 +1573,7 @@ seckey_CreateSubjectPublicKeyInfo_helper(SECKEYPublicKey *pubk)
CERTSubjectPublicKeyInfo *spki;
PLArenaPool *arena;
SECItem params = { siBuffer, NULL, 0 };
+ SECOidTag tag;
arena = PORT_NewArena(DER_DEFAULT_CHUNKSIZE);
if (arena == NULL) {
@@ -1555,14 +1646,41 @@ seckey_CreateSubjectPublicKeyInfo_helper(SECKEYPublicKey *pubk)
case ecKey:
rv = SECITEM_CopyItem(arena, &params,
&pubk->u.ec.DEREncodedParams);
- if (rv != SECSuccess)
+ if (rv != SECSuccess) {
break;
+ }
+ tag = SEC_OID_ANSIX962_EC_PUBLIC_KEY;
rv = SECOID_SetAlgorithmID(arena, &spki->algorithm,
- SEC_OID_ANSIX962_EC_PUBLIC_KEY,
+ tag,
&params);
- if (rv != SECSuccess)
+ if (rv != SECSuccess) {
+ break;
+ }
+
+ rv = SECITEM_CopyItem(arena, &spki->subjectPublicKey,
+ &pubk->u.ec.publicValue);
+
+ if (rv == SECSuccess) {
+ /*
+ * The stored value is supposed to be a BIT_STRING,
+ * so convert the length.
+ */
+ spki->subjectPublicKey.len <<= 3;
+ /*
+ * We got a good one; return it.
+ */
+ return spki;
+ }
+ break;
+ case edKey:
+ tag = SECKEY_GetECCOid(&pubk->u.ec.DEREncodedParams);
+ rv = SECOID_SetAlgorithmID(arena, &spki->algorithm,
+ tag,
+ &params);
+ if (rv != SECSuccess) {
break;
+ }
rv = SECITEM_CopyItem(arena, &spki->subjectPublicKey,
&pubk->u.ec.publicValue);
@@ -1669,8 +1787,9 @@ SECKEY_DecodeDERSubjectPublicKeyInfo(const SECItem *spkider)
rv = SEC_QuickDERDecodeItem(arena, spki,
CERT_SubjectPublicKeyInfoTemplate, &newSpkider);
}
- if (rv == SECSuccess)
+ if (rv == SECSuccess) {
return spki;
+ }
} else {
PORT_SetError(SEC_ERROR_NO_MEMORY);
}
diff --git a/security/nss/lib/cryptohi/secvfy.c b/security/nss/lib/cryptohi/secvfy.c
index 8c9dc2d87d..04c755a001 100644
--- a/security/nss/lib/cryptohi/secvfy.c
+++ b/security/nss/lib/cryptohi/secvfy.c
@@ -306,7 +306,7 @@ sec_GetEncAlgFromSigAlg(SECOidTag sigAlg)
* encalg: address of a SECOidTag which will be set with the signing alg.
*
* Returns: SECSuccess if the algorithm was acceptable, SECFailure if the
- * algorithm was not found or was not a signing algorithm.
+ * algorithm was not found or was not a signing algorithm.
*/
SECStatus
sec_DecodeSigAlg(const SECKEYPublicKey *key, SECOidTag sigAlg,
diff --git a/security/nss/lib/freebl/Hacl_Hash_SHA2_shim.h b/security/nss/lib/freebl/Hacl_Hash_SHA2_shim.h
new file mode 100644
index 0000000000..8e510e914d
--- /dev/null
+++ b/security/nss/lib/freebl/Hacl_Hash_SHA2_shim.h
@@ -0,0 +1,38 @@
+#include "blapi.h"
+#include "../pqg.h"
+
+static inline void
+sha512_pre_msg(uint8_t *hash, uint8_t *prefix, uint32_t len, uint8_t *input)
+{
+ SHA512Context *ctx = SHA512_NewContext();
+ uint32_t l = SHA512_LENGTH;
+ SHA512_Begin(ctx);
+ SHA512_Update(ctx, prefix, 32);
+ SHA512_Update(ctx, input, len);
+ SHA512_End(ctx, hash, &l, SHA512_LENGTH);
+ SHA512_DestroyContext(ctx, PR_TRUE);
+}
+
+static inline void
+sha512_pre_pre2_msg(
+ uint8_t *hash,
+ uint8_t *prefix,
+ uint8_t *prefix2,
+ uint32_t len,
+ uint8_t *input)
+{
+ SHA512Context *ctx = SHA512_NewContext();
+ uint32_t l = SHA512_LENGTH;
+ SHA512_Begin(ctx);
+ SHA512_Update(ctx, prefix, 32);
+ SHA512_Update(ctx, prefix2, 32);
+ SHA512_Update(ctx, input, len);
+ SHA512_End(ctx, hash, &l, SHA512_LENGTH);
+ SHA512_DestroyContext(ctx, PR_TRUE);
+}
+
+static void
+Hacl_Streaming_SHA2_hash_512(uint8_t *secret, uint32_t len, uint8_t *expanded)
+{
+ SHA512_HashBuf(expanded, secret, len);
+} \ No newline at end of file
diff --git a/security/nss/lib/freebl/Makefile b/security/nss/lib/freebl/Makefile
index eeee90a97f..78dc2621ea 100644
--- a/security/nss/lib/freebl/Makefile
+++ b/security/nss/lib/freebl/Makefile
@@ -608,11 +608,12 @@ ifndef NSS_DISABLE_CHACHAPOLY
endif # NSS_DISABLE_CHACHAPOLY
VERIFIED_SRCS += Hacl_Hash_SHA3.c Hacl_P256.c Hacl_P384.c Hacl_P521.c
+VERIFIED_SRCS += Hacl_Ed25519.c
+VERIFIED_SRCS += Hacl_Curve25519_51.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/security/nss/lib/freebl/blapi.h b/security/nss/lib/freebl/blapi.h
index 4b4de66916..b9d0c0a8aa 100644
--- a/security/nss/lib/freebl/blapi.h
+++ b/security/nss/lib/freebl/blapi.h
@@ -1921,6 +1921,27 @@ extern SECStatus Kyber_Encapsulate(KyberParams params, const SECItem *seed, cons
*/
extern SECStatus Kyber_Decapsulate(KyberParams params, const SECItem *privKey, const SECItem *ciphertext, SECItem *secret);
+/* EdDSA (only ed25519)
+** On input, msg == buffer containing message to be signed.
+** key == key to be used for signature.
+** Output, signature == Buffer containing the signature.
+*/
+extern SECStatus ED_SignMessage(ECPrivateKey *key, SECItem *signature,
+ const SECItem *msg);
+
+/* On input, signature == buffer holding the signature.
+** msg == buffer holding the message.
+** key == key used to verify the signature.
+** Output, whether the signature is valid or not.
+*/
+extern SECStatus ED_VerifyMessage(ECPublicKey *key, const SECItem *signature,
+ const SECItem *msg);
+
+/* EdDSA (only ed25519)
+ * Derive the public key `publicKey` from the private key `privateKey`.
+ */
+extern SECStatus ED_DerivePublicKey(const SECItem *privateKey, SECItem *publicKey);
+
SEC_END_PROTOS
#endif /* _BLAPI_H_ */
diff --git a/security/nss/lib/freebl/blapit.h b/security/nss/lib/freebl/blapit.h
index 7b59a812b0..e5300313d6 100644
--- a/security/nss/lib/freebl/blapit.h
+++ b/security/nss/lib/freebl/blapit.h
@@ -29,6 +29,8 @@
#define DES_KEY_LENGTH 8 /* Bytes */
+#define ED25519_SIGN_LEN 64U /* Bytes */
+
/* AES operation modes */
#define NSS_AES 0
#define NSS_AES_CBC 1
@@ -81,6 +83,9 @@ typedef int __BLAPI_DEPRECATED __attribute__((deprecated));
#define EC_MAX_KEY_BITS 521 /* in bits */
#define EC_MIN_KEY_BITS 256 /* in bits */
+#define ECD_MAX_KEY_BITS 255 /* in bits */
+#define ECD_MIN_KEY_BITS 255 /* in bits */
+
/* EC point compression format */
#define EC_POINT_FORM_COMPRESSED_Y0 0x02
#define EC_POINT_FORM_COMPRESSED_Y1 0x03
diff --git a/security/nss/lib/freebl/ec.c b/security/nss/lib/freebl/ec.c
index 35a848395c..cd6a88c7b0 100644
--- a/security/nss/lib/freebl/ec.c
+++ b/security/nss/lib/freebl/ec.c
@@ -18,6 +18,7 @@
#include "verified/Hacl_P384.h"
#include "verified/Hacl_P521.h"
#include "secport.h"
+#include "verified/Hacl_Ed25519.h"
#define EC_DOUBLECHECK PR_FALSE
@@ -65,6 +66,27 @@ ec_secp521r1_scalar_validate(const SECItem *scalar)
return SECSuccess;
}
+SECStatus
+ec_ED25519_pt_validate(const SECItem *px)
+{
+ if (!px || !px->data || px->len != Ed25519_PUBLIC_KEYLEN) {
+ PORT_SetError(SEC_ERROR_INVALID_ARGS);
+ return SECFailure;
+ }
+ return SECSuccess;
+}
+
+SECStatus
+ec_ED25519_scalar_validate(const SECItem *scalar)
+{
+ if (!scalar || !scalar->data || scalar->len != Ed25519_PRIVATE_KEYLEN) {
+ PORT_SetError(SEC_ERROR_INVALID_ARGS);
+ return SECFailure;
+ }
+
+ return SECSuccess;
+}
+
static const ECMethod kMethods[] = {
{ ECCurve25519,
ec_Curve25519_pt_mul,
@@ -96,6 +118,12 @@ static const ECMethod kMethods[] = {
NULL,
NULL,
},
+ { ECCurve_Ed25519,
+ NULL,
+ ec_ED25519_pt_validate,
+ ec_ED25519_scalar_validate,
+ NULL,
+ NULL },
};
static const ECMethod *
@@ -353,6 +381,16 @@ ec_NewKey(ECParams *ecParams, ECPrivateKey **privKey,
/* Compute corresponding public key */
/* Use curve specific code for point multiplication */
+
+ if (ecParams->name == ECCurve_Ed25519) {
+ rv = ED_DerivePublicKey(&key->privateValue, &key->publicValue);
+ if (rv != SECSuccess) {
+ goto cleanup;
+ }
+ NSS_DECLASSIFY(key->publicValue.data, key->publicValue.len); /* Declassifying public key to avoid false positive */
+ goto done;
+ }
+
if (ecParams->fieldID.type == ec_field_plain) {
const ECMethod *method = ec_get_method_from_name(ecParams->name);
if (method == NULL || method->pt_mul == NULL) {
@@ -435,6 +473,7 @@ ec_GenerateRandomPrivateKey(ECParams *ecParams, SECItem *privKey)
uint8_t leading_coeff_mask;
switch (ecParams->name) {
+ case ECCurve_Ed25519:
case ECCurve25519:
case ECCurve_NIST_P256:
case ECCurve_NIST_P384:
@@ -490,8 +529,9 @@ EC_NewKey(ECParams *ecParams, ECPrivateKey **privKey)
goto cleanup;
}
rv = ec_GenerateRandomPrivateKey(ecParams, &privKeyRand);
- if (rv != SECSuccess || privKeyRand.data == NULL)
+ if (rv != SECSuccess || privKeyRand.data == NULL) {
goto cleanup;
+ }
/* generate public key */
CHECK_SEC_OK(ec_NewKey(ecParams, privKey, privKeyRand.data, privKeyRand.len));
@@ -1317,3 +1357,103 @@ done:
return rv;
}
+
+/*EdDSA: Currently only Ed22519 is implemented.*/
+
+/*
+** Computes the EdDSA signature on the message using the given key.
+*/
+
+SECStatus
+ec_ED25519_public_key_validate(const ECPublicKey *key)
+{
+ if (!key || !(key->ecParams.name == ECCurve_Ed25519)) {
+ PORT_SetError(SEC_ERROR_INVALID_ARGS);
+ return SECFailure;
+ }
+ return ec_ED25519_pt_validate(&key->publicValue);
+}
+
+SECStatus
+ec_ED25519_private_key_validate(const ECPrivateKey *key)
+{
+ if (!key || !(key->ecParams.name == ECCurve_Ed25519)) {
+
+ PORT_SetError(SEC_ERROR_INVALID_ARGS);
+ return SECFailure;
+ }
+ return ec_ED25519_scalar_validate(&key->privateValue);
+}
+
+SECStatus
+ED_SignMessage(ECPrivateKey *key, SECItem *signature, const SECItem *msg)
+{
+ if (!msg || !signature || signature->len != Ed25519_SIGN_LEN) {
+ PORT_SetError(SEC_ERROR_INVALID_ARGS);
+ return SECFailure;
+ }
+
+ if (ec_ED25519_private_key_validate(key) != SECSuccess) {
+ return SECFailure; /* error code set by ec_ED25519_scalar_validate. */
+ }
+
+ if (signature->data) {
+ Hacl_Ed25519_sign(signature->data, key->privateValue.data, msg->len,
+ msg->data);
+ }
+ signature->len = ED25519_SIGN_LEN;
+ BLAPI_CLEAR_STACK(2048);
+ return SECSuccess;
+}
+
+/*
+** Checks the signature on the given message using the key provided.
+*/
+
+SECStatus
+ED_VerifyMessage(ECPublicKey *key, const SECItem *signature,
+ const SECItem *msg)
+{
+ if (!msg || !signature || !signature->data || signature->len != Ed25519_SIGN_LEN) {
+ PORT_SetError(SEC_ERROR_INVALID_ARGS);
+ return SECFailure;
+ }
+
+ if (ec_ED25519_public_key_validate(key) != SECSuccess) {
+ return SECFailure; /* error code set by ec_ED25519_pt_validate. */
+ }
+
+ bool rv = Hacl_Ed25519_verify(key->publicValue.data, msg->len, msg->data,
+ signature->data);
+ BLAPI_CLEAR_STACK(2048);
+
+#if EC_DEBUG
+ printf("ED_VerifyMessage returning %s\n",
+ (rv) ? "success" : "failure");
+#endif
+
+ if (rv) {
+ return SECSuccess;
+ }
+
+ PORT_SetError(SEC_ERROR_BAD_SIGNATURE);
+ return SECFailure;
+}
+
+SECStatus
+ED_DerivePublicKey(const SECItem *privateKey, SECItem *publicKey)
+{
+ /* Currently supporting only Ed25519.*/
+ if (!privateKey || privateKey->len == 0 || !publicKey || publicKey->len != Ed25519_PUBLIC_KEYLEN) {
+ PORT_SetError(SEC_ERROR_INVALID_ARGS);
+ return SECFailure;
+ }
+
+ if (ec_ED25519_scalar_validate(privateKey) != SECSuccess) {
+ PORT_SetError(SEC_ERROR_INVALID_ARGS);
+ return SECFailure;
+ }
+
+ Hacl_Ed25519_secret_to_public(publicKey->data, privateKey->data);
+ return SECSuccess;
+} \ No newline at end of file
diff --git a/security/nss/lib/freebl/ec.h b/security/nss/lib/freebl/ec.h
index f4b8ee7334..c38f623d4a 100644
--- a/security/nss/lib/freebl/ec.h
+++ b/security/nss/lib/freebl/ec.h
@@ -10,6 +10,10 @@
#define ANSI_X962_CURVE_OID_TOTAL_LEN 10
#define SECG_CURVE_OID_TOTAL_LEN 7
#define PKIX_NEWCURVES_OID_TOTAL_LEN 11
+#define ED25519_OID_TOTAL_LEN 5
+#define Ed25519_PRIVATE_KEYLEN 32
+#define Ed25519_PUBLIC_KEYLEN 32
+#define Ed25519_SIGN_LEN 64
struct ECMethodStr {
ECCurveName name;
diff --git a/security/nss/lib/freebl/ecdecode.c b/security/nss/lib/freebl/ecdecode.c
index 24ba11f3b1..c78eedf373 100644
--- a/security/nss/lib/freebl/ecdecode.c
+++ b/security/nss/lib/freebl/ecdecode.c
@@ -120,7 +120,8 @@ EC_FillParams(PLArenaPool *arena, const SECItem *encodedParams,
if ((encodedParams->len != ANSI_X962_CURVE_OID_TOTAL_LEN) &&
(encodedParams->len != SECG_CURVE_OID_TOTAL_LEN) &&
- (encodedParams->len != PKIX_NEWCURVES_OID_TOTAL_LEN)) {
+ (encodedParams->len != PKIX_NEWCURVES_OID_TOTAL_LEN) &&
+ (encodedParams->len != ED25519_OID_TOTAL_LEN)) {
PORT_SetError(SEC_ERROR_UNSUPPORTED_ELLIPTIC_CURVE);
return SECFailure;
};
@@ -174,6 +175,13 @@ EC_FillParams(PLArenaPool *arena, const SECItem *encodedParams,
ec_field_GFp, params));
break;
+ case SEC_OID_ED25519_PUBLIC_KEY:
+ params->type = ec_params_edwards_named;
+ CHECK_SEC_OK(gf_populate_params_bytes(ECCurve_Ed25519,
+ ec_field_plain, params));
+
+ break;
+
case SEC_OID_CURVE25519:
/* Populate params for Curve25519 */
params->type = ec_params_montgomery_named;
@@ -246,10 +254,11 @@ EC_GetPointSize(const ECParams *params)
int sizeInBytes = (params->fieldID.size + 7) / 8;
return sizeInBytes * 2 + 1;
}
- if (name == ECCurve25519) {
- /* Only X here */
+
+ if (params->type == ec_params_edwards_named || params->type == ec_params_montgomery_named) {
return curveParams->scalarSize;
}
+
return curveParams->pointSize - 1;
}
diff --git a/security/nss/lib/freebl/ecl/ecl-curve.h b/security/nss/lib/freebl/ecl/ecl-curve.h
index dec3ce387d..1c9cb5db53 100644
--- a/security/nss/lib/freebl/ecl/ecl-curve.h
+++ b/security/nss/lib/freebl/ecl/ecl-curve.h
@@ -178,6 +178,13 @@ static const ECCurveBytes ecCurve_25519 = {
KU_KEY_AGREEMENT
};
+static const ECCurveBytes ecCurve_Ed25519 = {
+ "ED25119", ECField_GFp, 255,
+ NULL, NULL, NULL, NULL, NULL, NULL, NULL,
+ 8, 128, 66, 32,
+ KU_DIGITAL_SIGNATURE
+};
+
/* mapping between ECCurveName enum and pointers to ECCurveParams */
static const ECCurveBytes *ecCurve_map[] = {
NULL, /* ECCurve_noName */
@@ -239,7 +246,8 @@ static const ECCurveBytes *ecCurve_map[] = {
NULL, /* ECCurve_WTLS_8 */
NULL, /* ECCurve_WTLS_9 */
&ecCurve_25519, /* ECCurve25519 */
- NULL /* ECCurve_pastLastCurve */
+ &ecCurve_Ed25519,
+ NULL /* ECCurve_pastLastCurve */
};
#endif
diff --git a/security/nss/lib/freebl/ecl/ecl-exp.h b/security/nss/lib/freebl/ecl/ecl-exp.h
index 44adb8a1cd..14263c70f4 100644
--- a/security/nss/lib/freebl/ecl/ecl-exp.h
+++ b/security/nss/lib/freebl/ecl/ecl-exp.h
@@ -132,6 +132,7 @@ typedef enum {
/* ECCurve_WTLS_12 == ECCurve_NIST_P224 */
ECCurve25519,
+ ECCurve_Ed25519,
ECCurve_pastLastCurve
} ECCurveName;
diff --git a/security/nss/lib/freebl/freebl_base.gypi b/security/nss/lib/freebl/freebl_base.gypi
index 8ef46da630..2a6bd5e5c5 100644
--- a/security/nss/lib/freebl/freebl_base.gypi
+++ b/security/nss/lib/freebl/freebl_base.gypi
@@ -73,6 +73,8 @@
'verified/Hacl_Hash_SHA3.c',
'sha3.c',
'shake.c',
+ 'verified/Hacl_Curve25519_51.c',
+ 'verified/Hacl_Ed25519.c',
],
'defines': [
# For kyber-pqcrystals-ref.c. If we ever decide to support Kyber512 or
diff --git a/security/nss/lib/freebl/ldvector.c b/security/nss/lib/freebl/ldvector.c
index 14ecfcaa25..641340b8c7 100644
--- a/security/nss/lib/freebl/ldvector.c
+++ b/security/nss/lib/freebl/ldvector.c
@@ -438,6 +438,11 @@ static const struct FREEBLVectorStr vector = {
Kyber_Decapsulate,
/* End of version 3.027 */
+
+ ED_SignMessage,
+ ED_VerifyMessage,
+ ED_DerivePublicKey,
+ /* End of version 3.028 */
};
const FREEBLVector*
diff --git a/security/nss/lib/freebl/loader.c b/security/nss/lib/freebl/loader.c
index 473169264c..22c468fda7 100644
--- a/security/nss/lib/freebl/loader.c
+++ b/security/nss/lib/freebl/loader.c
@@ -2854,3 +2854,31 @@ Kyber_Decapsulate(KyberParams params, const SECItem *privKey, const SECItem *cip
return SECFailure;
return (vector->p_Kyber_Decapsulate)(params, privKey, ciphertext, secret);
}
+
+/* ============== New for 3.0028 =============================== */
+
+SECStatus
+ED_SignMessage(ECPrivateKey *key, SECItem *signature,
+ const SECItem *msg)
+{
+ if (!vector && PR_SUCCESS != freebl_RunLoaderOnce())
+ return SECFailure;
+ return (vector->p_ED_SignMessage)(key, signature, msg);
+}
+
+SECStatus
+ED_VerifyMessage(ECPublicKey *key, const SECItem *signature,
+ const SECItem *msg)
+{
+ if (!vector && PR_SUCCESS != freebl_RunLoaderOnce())
+ return SECFailure;
+ return (vector->p_ED_VerifyMessage)(key, signature, msg);
+}
+
+SECStatus
+ED_DerivePublicKey(const SECItem *privateKey, SECItem *publicKey)
+{
+ if (!vector && PR_SUCCESS != freebl_RunLoaderOnce())
+ return SECFailure;
+ return (vector->p_ED_DerivePublicKey)(privateKey, publicKey);
+}
diff --git a/security/nss/lib/freebl/loader.h b/security/nss/lib/freebl/loader.h
index 62159d88c7..5c51f48213 100644
--- a/security/nss/lib/freebl/loader.h
+++ b/security/nss/lib/freebl/loader.h
@@ -918,6 +918,13 @@ struct FREEBLVectorStr {
/* Version 3.027 came to here */
+ SECStatus (*p_ED_SignMessage)(ECPrivateKey *key, SECItem *signature, const SECItem *msg);
+ SECStatus (*p_ED_VerifyMessage)(ECPublicKey *key, const SECItem *signature,
+ const SECItem *msg);
+
+ SECStatus (*p_ED_DerivePublicKey)(const SECItem *privateKey, SECItem *publicKey);
+ /* Version 3.028 came to here */
+
/* Add new function pointers at the end of this struct and bump
* FREEBL_VERSION at the beginning of this file. */
};
diff --git a/security/nss/lib/freebl/verified/Hacl_Chacha20_Vec128.c b/security/nss/lib/freebl/verified/Hacl_Chacha20_Vec128.c
index a15820273c..bf2cc651ce 100644
--- a/security/nss/lib/freebl/verified/Hacl_Chacha20_Vec128.c
+++ b/security/nss/lib/freebl/verified/Hacl_Chacha20_Vec128.c
@@ -368,9 +368,8 @@ Hacl_Chacha20_Vec128_chacha20_encrypt_128(
}
if (rem1 > (uint32_t)0U) {
uint8_t *uu____2 = out + nb * (uint32_t)256U;
- uint8_t *uu____3 = text + nb * (uint32_t)256U;
uint8_t plain[256U] = { 0U };
- memcpy(plain, uu____3, rem * sizeof(uint8_t));
+ memcpy(plain, text + nb * (uint32_t)256U, rem * sizeof(uint8_t));
KRML_PRE_ALIGN(16)
Lib_IntVector_Intrinsics_vec128 k[16U] KRML_POST_ALIGN(16) = { 0U };
chacha20_core_128(k, ctx, nb);
@@ -674,9 +673,8 @@ Hacl_Chacha20_Vec128_chacha20_decrypt_128(
}
if (rem1 > (uint32_t)0U) {
uint8_t *uu____2 = out + nb * (uint32_t)256U;
- uint8_t *uu____3 = cipher + nb * (uint32_t)256U;
uint8_t plain[256U] = { 0U };
- memcpy(plain, uu____3, rem * sizeof(uint8_t));
+ memcpy(plain, cipher + nb * (uint32_t)256U, rem * sizeof(uint8_t));
KRML_PRE_ALIGN(16)
Lib_IntVector_Intrinsics_vec128 k[16U] KRML_POST_ALIGN(16) = { 0U };
chacha20_core_128(k, ctx, nb);
diff --git a/security/nss/lib/freebl/verified/Hacl_Chacha20_Vec256.c b/security/nss/lib/freebl/verified/Hacl_Chacha20_Vec256.c
index e184598e4a..98ff9c346f 100644
--- a/security/nss/lib/freebl/verified/Hacl_Chacha20_Vec256.c
+++ b/security/nss/lib/freebl/verified/Hacl_Chacha20_Vec256.c
@@ -468,9 +468,8 @@ Hacl_Chacha20_Vec256_chacha20_encrypt_256(
}
if (rem1 > (uint32_t)0U) {
uint8_t *uu____2 = out + nb * (uint32_t)512U;
- uint8_t *uu____3 = text + nb * (uint32_t)512U;
uint8_t plain[512U] = { 0U };
- memcpy(plain, uu____3, rem * sizeof(uint8_t));
+ memcpy(plain, text + nb * (uint32_t)512U, rem * sizeof(uint8_t));
KRML_PRE_ALIGN(32)
Lib_IntVector_Intrinsics_vec256 k[16U] KRML_POST_ALIGN(32) = { 0U };
chacha20_core_256(k, ctx, nb);
@@ -966,9 +965,8 @@ Hacl_Chacha20_Vec256_chacha20_decrypt_256(
}
if (rem1 > (uint32_t)0U) {
uint8_t *uu____2 = out + nb * (uint32_t)512U;
- uint8_t *uu____3 = cipher + nb * (uint32_t)512U;
uint8_t plain[512U] = { 0U };
- memcpy(plain, uu____3, rem * sizeof(uint8_t));
+ memcpy(plain, cipher + nb * (uint32_t)512U, rem * sizeof(uint8_t));
KRML_PRE_ALIGN(32)
Lib_IntVector_Intrinsics_vec256 k[16U] KRML_POST_ALIGN(32) = { 0U };
chacha20_core_256(k, ctx, nb);
diff --git a/security/nss/lib/freebl/verified/Hacl_Curve25519_64.c b/security/nss/lib/freebl/verified/Hacl_Curve25519_64.c
index 6dbdf736f9..7ba332cba6 100644
--- a/security/nss/lib/freebl/verified/Hacl_Curve25519_64.c
+++ b/security/nss/lib/freebl/verified/Hacl_Curve25519_64.c
@@ -35,7 +35,7 @@ add_scalar0(uint64_t *out, uint64_t *f1, uint64_t f2)
#if HACL_CAN_COMPILE_INLINE_ASM
add_scalar(out, f1, f2);
#else
- uint64_t uu____0 = add_scalar_e(out, f1, f2);
+ KRML_HOST_IGNORE(add_scalar_e(out, f1, f2));
#endif
}
@@ -45,7 +45,7 @@ fadd0(uint64_t *out, uint64_t *f1, uint64_t *f2)
#if HACL_CAN_COMPILE_INLINE_ASM
fadd(out, f1, f2);
#else
- uint64_t uu____0 = fadd_e(out, f1, f2);
+ KRML_HOST_IGNORE(fadd_e(out, f1, f2));
#endif
}
@@ -55,7 +55,7 @@ fsub0(uint64_t *out, uint64_t *f1, uint64_t *f2)
#if HACL_CAN_COMPILE_INLINE_ASM
fsub(out, f1, f2);
#else
- uint64_t uu____0 = fsub_e(out, f1, f2);
+ KRML_HOST_IGNORE(fsub_e(out, f1, f2));
#endif
}
@@ -65,7 +65,7 @@ fmul0(uint64_t *out, uint64_t *f1, uint64_t *f2, uint64_t *tmp)
#if HACL_CAN_COMPILE_INLINE_ASM
fmul(out, f1, f2, tmp);
#else
- uint64_t uu____0 = fmul_e(tmp, f1, out, f2);
+ KRML_HOST_IGNORE(fmul_e(tmp, f1, out, f2));
#endif
}
@@ -75,7 +75,7 @@ fmul20(uint64_t *out, uint64_t *f1, uint64_t *f2, uint64_t *tmp)
#if HACL_CAN_COMPILE_INLINE_ASM
fmul2(out, f1, f2, tmp);
#else
- uint64_t uu____0 = fmul2_e(tmp, f1, out, f2);
+ KRML_HOST_IGNORE(fmul2_e(tmp, f1, out, f2));
#endif
}
@@ -85,7 +85,7 @@ fmul_scalar0(uint64_t *out, uint64_t *f1, uint64_t f2)
#if HACL_CAN_COMPILE_INLINE_ASM
fmul_scalar(out, f1, f2);
#else
- uint64_t uu____0 = fmul_scalar_e(out, f1, f2);
+ KRML_HOST_IGNORE(fmul_scalar_e(out, f1, f2));
#endif
}
@@ -95,7 +95,7 @@ fsqr0(uint64_t *out, uint64_t *f1, uint64_t *tmp)
#if HACL_CAN_COMPILE_INLINE_ASM
fsqr(out, f1, tmp);
#else
- uint64_t uu____0 = fsqr_e(tmp, f1, out);
+ KRML_HOST_IGNORE(fsqr_e(tmp, f1, out));
#endif
}
@@ -105,7 +105,7 @@ fsqr20(uint64_t *out, uint64_t *f, uint64_t *tmp)
#if HACL_CAN_COMPILE_INLINE_ASM
fsqr2(out, f, tmp);
#else
- uint64_t uu____0 = fsqr2_e(tmp, f, out);
+ KRML_HOST_IGNORE(fsqr2_e(tmp, f, out));
#endif
}
@@ -115,7 +115,7 @@ cswap20(uint64_t bit, uint64_t *p1, uint64_t *p2)
#if HACL_CAN_COMPILE_INLINE_ASM
cswap2(bit, p1, p2);
#else
- uint64_t uu____0 = cswap2_e(bit, p1, p2);
+ KRML_HOST_IGNORE(cswap2_e(bit, p1, p2));
#endif
}
diff --git a/security/nss/lib/freebl/verified/Hacl_Ed25519.c b/security/nss/lib/freebl/verified/Hacl_Ed25519.c
new file mode 100644
index 0000000000..f7a5ea6d75
--- /dev/null
+++ b/security/nss/lib/freebl/verified/Hacl_Ed25519.c
@@ -0,0 +1,1853 @@
+/* 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_Ed25519.h"
+
+#include "internal/Hacl_Krmllib.h"
+#include "internal/Hacl_Ed25519_PrecompTable.h"
+#include "internal/Hacl_Curve25519_51.h"
+#include "internal/Hacl_Bignum_Base.h"
+#include "internal/Hacl_Bignum25519_51.h"
+
+#include "../Hacl_Hash_SHA2_shim.h"
+
+static inline void
+fsum(uint64_t *out, uint64_t *a, uint64_t *b)
+{
+ Hacl_Impl_Curve25519_Field51_fadd(out, a, b);
+}
+
+static inline void
+fdifference(uint64_t *out, uint64_t *a, uint64_t *b)
+{
+ Hacl_Impl_Curve25519_Field51_fsub(out, a, b);
+}
+
+void
+Hacl_Bignum25519_reduce_513(uint64_t *a)
+{
+ uint64_t f0 = a[0U];
+ uint64_t f1 = a[1U];
+ uint64_t f2 = a[2U];
+ uint64_t f3 = a[3U];
+ uint64_t f4 = a[4U];
+ uint64_t l_ = f0 + (uint64_t)0U;
+ uint64_t tmp0 = l_ & (uint64_t)0x7ffffffffffffU;
+ uint64_t c0 = l_ >> (uint32_t)51U;
+ uint64_t l_0 = f1 + c0;
+ uint64_t tmp1 = l_0 & (uint64_t)0x7ffffffffffffU;
+ uint64_t c1 = l_0 >> (uint32_t)51U;
+ uint64_t l_1 = f2 + c1;
+ uint64_t tmp2 = l_1 & (uint64_t)0x7ffffffffffffU;
+ uint64_t c2 = l_1 >> (uint32_t)51U;
+ uint64_t l_2 = f3 + c2;
+ uint64_t tmp3 = l_2 & (uint64_t)0x7ffffffffffffU;
+ uint64_t c3 = l_2 >> (uint32_t)51U;
+ uint64_t l_3 = f4 + c3;
+ uint64_t tmp4 = l_3 & (uint64_t)0x7ffffffffffffU;
+ uint64_t c4 = l_3 >> (uint32_t)51U;
+ uint64_t l_4 = tmp0 + c4 * (uint64_t)19U;
+ uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
+ uint64_t c5 = l_4 >> (uint32_t)51U;
+ a[0U] = tmp0_;
+ a[1U] = tmp1 + c5;
+ a[2U] = tmp2;
+ a[3U] = tmp3;
+ a[4U] = tmp4;
+}
+
+static inline void
+fmul0(uint64_t *output, uint64_t *input, uint64_t *input2)
+{
+ FStar_UInt128_uint128 tmp[10U];
+ for (uint32_t _i = 0U; _i < (uint32_t)10U; ++_i)
+ tmp[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U);
+ Hacl_Impl_Curve25519_Field51_fmul(output, input, input2, tmp);
+}
+
+static inline void
+times_2(uint64_t *out, uint64_t *a)
+{
+ uint64_t a0 = a[0U];
+ uint64_t a1 = a[1U];
+ uint64_t a2 = a[2U];
+ uint64_t a3 = a[3U];
+ uint64_t a4 = a[4U];
+ uint64_t o0 = (uint64_t)2U * a0;
+ uint64_t o1 = (uint64_t)2U * a1;
+ uint64_t o2 = (uint64_t)2U * a2;
+ uint64_t o3 = (uint64_t)2U * a3;
+ uint64_t o4 = (uint64_t)2U * a4;
+ out[0U] = o0;
+ out[1U] = o1;
+ out[2U] = o2;
+ out[3U] = o3;
+ out[4U] = o4;
+}
+
+static inline void
+times_d(uint64_t *out, uint64_t *a)
+{
+ uint64_t d[5U] = { 0U };
+ d[0U] = (uint64_t)0x00034dca135978a3U;
+ d[1U] = (uint64_t)0x0001a8283b156ebdU;
+ d[2U] = (uint64_t)0x0005e7a26001c029U;
+ d[3U] = (uint64_t)0x000739c663a03cbbU;
+ d[4U] = (uint64_t)0x00052036cee2b6ffU;
+ fmul0(out, d, a);
+}
+
+static inline void
+times_2d(uint64_t *out, uint64_t *a)
+{
+ uint64_t d2[5U] = { 0U };
+ d2[0U] = (uint64_t)0x00069b9426b2f159U;
+ d2[1U] = (uint64_t)0x00035050762add7aU;
+ d2[2U] = (uint64_t)0x0003cf44c0038052U;
+ d2[3U] = (uint64_t)0x0006738cc7407977U;
+ d2[4U] = (uint64_t)0x0002406d9dc56dffU;
+ fmul0(out, d2, a);
+}
+
+static inline void
+fsquare(uint64_t *out, uint64_t *a)
+{
+ FStar_UInt128_uint128 tmp[5U];
+ for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i)
+ tmp[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U);
+ Hacl_Impl_Curve25519_Field51_fsqr(out, a, tmp);
+}
+
+static inline void
+fsquare_times(uint64_t *output, uint64_t *input, uint32_t count)
+{
+ FStar_UInt128_uint128 tmp[5U];
+ for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i)
+ tmp[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U);
+ Hacl_Curve25519_51_fsquare_times(output, input, tmp, count);
+}
+
+static inline void
+fsquare_times_inplace(uint64_t *output, uint32_t count)
+{
+ FStar_UInt128_uint128 tmp[5U];
+ for (uint32_t _i = 0U; _i < (uint32_t)5U; ++_i)
+ tmp[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U);
+ Hacl_Curve25519_51_fsquare_times(output, output, tmp, count);
+}
+
+void
+Hacl_Bignum25519_inverse(uint64_t *out, uint64_t *a)
+{
+ FStar_UInt128_uint128 tmp[10U];
+ for (uint32_t _i = 0U; _i < (uint32_t)10U; ++_i)
+ tmp[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U);
+ Hacl_Curve25519_51_finv(out, a, tmp);
+}
+
+static inline void
+reduce(uint64_t *out)
+{
+ uint64_t o0 = out[0U];
+ uint64_t o1 = out[1U];
+ uint64_t o2 = out[2U];
+ uint64_t o3 = out[3U];
+ uint64_t o4 = out[4U];
+ uint64_t l_ = o0 + (uint64_t)0U;
+ uint64_t tmp0 = l_ & (uint64_t)0x7ffffffffffffU;
+ uint64_t c0 = l_ >> (uint32_t)51U;
+ uint64_t l_0 = o1 + c0;
+ uint64_t tmp1 = l_0 & (uint64_t)0x7ffffffffffffU;
+ uint64_t c1 = l_0 >> (uint32_t)51U;
+ uint64_t l_1 = o2 + c1;
+ uint64_t tmp2 = l_1 & (uint64_t)0x7ffffffffffffU;
+ uint64_t c2 = l_1 >> (uint32_t)51U;
+ uint64_t l_2 = o3 + c2;
+ uint64_t tmp3 = l_2 & (uint64_t)0x7ffffffffffffU;
+ uint64_t c3 = l_2 >> (uint32_t)51U;
+ uint64_t l_3 = o4 + c3;
+ uint64_t tmp4 = l_3 & (uint64_t)0x7ffffffffffffU;
+ uint64_t c4 = l_3 >> (uint32_t)51U;
+ uint64_t l_4 = tmp0 + c4 * (uint64_t)19U;
+ uint64_t tmp0_ = l_4 & (uint64_t)0x7ffffffffffffU;
+ uint64_t c5 = l_4 >> (uint32_t)51U;
+ uint64_t f0 = tmp0_;
+ uint64_t f1 = tmp1 + c5;
+ uint64_t f2 = tmp2;
+ uint64_t f3 = tmp3;
+ uint64_t f4 = tmp4;
+ uint64_t m0 = FStar_UInt64_gte_mask(f0, (uint64_t)0x7ffffffffffedU);
+ uint64_t m1 = FStar_UInt64_eq_mask(f1, (uint64_t)0x7ffffffffffffU);
+ uint64_t m2 = FStar_UInt64_eq_mask(f2, (uint64_t)0x7ffffffffffffU);
+ uint64_t m3 = FStar_UInt64_eq_mask(f3, (uint64_t)0x7ffffffffffffU);
+ uint64_t m4 = FStar_UInt64_eq_mask(f4, (uint64_t)0x7ffffffffffffU);
+ uint64_t mask = (((m0 & m1) & m2) & m3) & m4;
+ uint64_t f0_ = f0 - (mask & (uint64_t)0x7ffffffffffedU);
+ uint64_t f1_ = f1 - (mask & (uint64_t)0x7ffffffffffffU);
+ uint64_t f2_ = f2 - (mask & (uint64_t)0x7ffffffffffffU);
+ uint64_t f3_ = f3 - (mask & (uint64_t)0x7ffffffffffffU);
+ uint64_t f4_ = f4 - (mask & (uint64_t)0x7ffffffffffffU);
+ uint64_t f01 = f0_;
+ uint64_t f11 = f1_;
+ uint64_t f21 = f2_;
+ uint64_t f31 = f3_;
+ uint64_t f41 = f4_;
+ out[0U] = f01;
+ out[1U] = f11;
+ out[2U] = f21;
+ out[3U] = f31;
+ out[4U] = f41;
+}
+
+void
+Hacl_Bignum25519_load_51(uint64_t *output, uint8_t *input)
+{
+ uint64_t u64s[4U] = { 0U };
+ KRML_MAYBE_FOR4(i,
+ (uint32_t)0U,
+ (uint32_t)4U,
+ (uint32_t)1U,
+ uint64_t *os = u64s;
+ uint8_t *bj = input + i * (uint32_t)8U;
+ uint64_t u = load64_le(bj);
+ uint64_t r = u;
+ uint64_t x = r;
+ os[i] = x;);
+ uint64_t u64s3 = u64s[3U];
+ u64s[3U] = u64s3 & (uint64_t)0x7fffffffffffffffU;
+ output[0U] = u64s[0U] & (uint64_t)0x7ffffffffffffU;
+ output[1U] = u64s[0U] >> (uint32_t)51U | (u64s[1U] & (uint64_t)0x3fffffffffU) << (uint32_t)13U;
+ output[2U] = u64s[1U] >> (uint32_t)38U | (u64s[2U] & (uint64_t)0x1ffffffU) << (uint32_t)26U;
+ output[3U] = u64s[2U] >> (uint32_t)25U | (u64s[3U] & (uint64_t)0xfffU) << (uint32_t)39U;
+ output[4U] = u64s[3U] >> (uint32_t)12U;
+}
+
+void
+Hacl_Bignum25519_store_51(uint8_t *output, uint64_t *input)
+{
+ uint64_t u64s[4U] = { 0U };
+ Hacl_Impl_Curve25519_Field51_store_felem(u64s, input);
+ KRML_MAYBE_FOR4(i,
+ (uint32_t)0U,
+ (uint32_t)4U,
+ (uint32_t)1U,
+ store64_le(output + i * (uint32_t)8U, u64s[i]););
+}
+
+void
+Hacl_Impl_Ed25519_PointDouble_point_double(uint64_t *out, uint64_t *p)
+{
+ uint64_t tmp[20U] = { 0U };
+ uint64_t *tmp1 = tmp;
+ uint64_t *tmp20 = tmp + (uint32_t)5U;
+ uint64_t *tmp30 = tmp + (uint32_t)10U;
+ uint64_t *tmp40 = tmp + (uint32_t)15U;
+ uint64_t *x10 = p;
+ uint64_t *y10 = p + (uint32_t)5U;
+ uint64_t *z1 = p + (uint32_t)10U;
+ fsquare(tmp1, x10);
+ fsquare(tmp20, y10);
+ fsum(tmp30, tmp1, tmp20);
+ fdifference(tmp40, tmp1, tmp20);
+ fsquare(tmp1, z1);
+ times_2(tmp1, tmp1);
+ uint64_t *tmp10 = tmp;
+ uint64_t *tmp2 = tmp + (uint32_t)5U;
+ uint64_t *tmp3 = tmp + (uint32_t)10U;
+ uint64_t *tmp4 = tmp + (uint32_t)15U;
+ uint64_t *x1 = p;
+ uint64_t *y1 = p + (uint32_t)5U;
+ fsum(tmp2, x1, y1);
+ fsquare(tmp2, tmp2);
+ Hacl_Bignum25519_reduce_513(tmp3);
+ fdifference(tmp2, tmp3, tmp2);
+ Hacl_Bignum25519_reduce_513(tmp10);
+ Hacl_Bignum25519_reduce_513(tmp4);
+ fsum(tmp10, tmp10, tmp4);
+ uint64_t *tmp_f = tmp;
+ uint64_t *tmp_e = tmp + (uint32_t)5U;
+ uint64_t *tmp_h = tmp + (uint32_t)10U;
+ uint64_t *tmp_g = tmp + (uint32_t)15U;
+ uint64_t *x3 = out;
+ uint64_t *y3 = out + (uint32_t)5U;
+ uint64_t *z3 = out + (uint32_t)10U;
+ uint64_t *t3 = out + (uint32_t)15U;
+ fmul0(x3, tmp_e, tmp_f);
+ fmul0(y3, tmp_g, tmp_h);
+ fmul0(t3, tmp_e, tmp_h);
+ fmul0(z3, tmp_f, tmp_g);
+}
+
+void
+Hacl_Impl_Ed25519_PointAdd_point_add(uint64_t *out, uint64_t *p, uint64_t *q)
+{
+ uint64_t tmp[30U] = { 0U };
+ uint64_t *tmp1 = tmp;
+ uint64_t *tmp20 = tmp + (uint32_t)5U;
+ uint64_t *tmp30 = tmp + (uint32_t)10U;
+ uint64_t *tmp40 = tmp + (uint32_t)15U;
+ uint64_t *x1 = p;
+ uint64_t *y1 = p + (uint32_t)5U;
+ uint64_t *x2 = q;
+ uint64_t *y2 = q + (uint32_t)5U;
+ fdifference(tmp1, y1, x1);
+ fdifference(tmp20, y2, x2);
+ fmul0(tmp30, tmp1, tmp20);
+ fsum(tmp1, y1, x1);
+ fsum(tmp20, y2, x2);
+ fmul0(tmp40, tmp1, tmp20);
+ uint64_t *tmp10 = tmp;
+ uint64_t *tmp2 = tmp + (uint32_t)5U;
+ uint64_t *tmp3 = tmp + (uint32_t)10U;
+ uint64_t *tmp4 = tmp + (uint32_t)15U;
+ uint64_t *tmp5 = tmp + (uint32_t)20U;
+ uint64_t *tmp6 = tmp + (uint32_t)25U;
+ uint64_t *z1 = p + (uint32_t)10U;
+ uint64_t *t1 = p + (uint32_t)15U;
+ uint64_t *z2 = q + (uint32_t)10U;
+ uint64_t *t2 = q + (uint32_t)15U;
+ times_2d(tmp10, t1);
+ fmul0(tmp10, tmp10, t2);
+ times_2(tmp2, z1);
+ fmul0(tmp2, tmp2, z2);
+ fdifference(tmp5, tmp4, tmp3);
+ fdifference(tmp6, tmp2, tmp10);
+ fsum(tmp10, tmp2, tmp10);
+ fsum(tmp2, tmp4, tmp3);
+ uint64_t *tmp_g = tmp;
+ uint64_t *tmp_h = tmp + (uint32_t)5U;
+ uint64_t *tmp_e = tmp + (uint32_t)20U;
+ uint64_t *tmp_f = tmp + (uint32_t)25U;
+ uint64_t *x3 = out;
+ uint64_t *y3 = out + (uint32_t)5U;
+ uint64_t *z3 = out + (uint32_t)10U;
+ uint64_t *t3 = out + (uint32_t)15U;
+ fmul0(x3, tmp_e, tmp_f);
+ fmul0(y3, tmp_g, tmp_h);
+ fmul0(t3, tmp_e, tmp_h);
+ fmul0(z3, tmp_f, tmp_g);
+}
+
+void
+Hacl_Impl_Ed25519_PointConstants_make_point_inf(uint64_t *b)
+{
+ uint64_t *x = b;
+ uint64_t *y = b + (uint32_t)5U;
+ uint64_t *z = b + (uint32_t)10U;
+ uint64_t *t = b + (uint32_t)15U;
+ x[0U] = (uint64_t)0U;
+ x[1U] = (uint64_t)0U;
+ x[2U] = (uint64_t)0U;
+ x[3U] = (uint64_t)0U;
+ x[4U] = (uint64_t)0U;
+ y[0U] = (uint64_t)1U;
+ y[1U] = (uint64_t)0U;
+ y[2U] = (uint64_t)0U;
+ y[3U] = (uint64_t)0U;
+ y[4U] = (uint64_t)0U;
+ z[0U] = (uint64_t)1U;
+ z[1U] = (uint64_t)0U;
+ z[2U] = (uint64_t)0U;
+ z[3U] = (uint64_t)0U;
+ z[4U] = (uint64_t)0U;
+ t[0U] = (uint64_t)0U;
+ t[1U] = (uint64_t)0U;
+ t[2U] = (uint64_t)0U;
+ t[3U] = (uint64_t)0U;
+ t[4U] = (uint64_t)0U;
+}
+
+static inline void
+pow2_252m2(uint64_t *out, uint64_t *z)
+{
+ uint64_t buf[20U] = { 0U };
+ uint64_t *a = buf;
+ uint64_t *t00 = buf + (uint32_t)5U;
+ uint64_t *b0 = buf + (uint32_t)10U;
+ uint64_t *c0 = buf + (uint32_t)15U;
+ fsquare_times(a, z, (uint32_t)1U);
+ fsquare_times(t00, a, (uint32_t)2U);
+ fmul0(b0, t00, z);
+ fmul0(a, b0, a);
+ fsquare_times(t00, a, (uint32_t)1U);
+ fmul0(b0, t00, b0);
+ fsquare_times(t00, b0, (uint32_t)5U);
+ fmul0(b0, t00, b0);
+ fsquare_times(t00, b0, (uint32_t)10U);
+ fmul0(c0, t00, b0);
+ fsquare_times(t00, c0, (uint32_t)20U);
+ fmul0(t00, t00, c0);
+ fsquare_times_inplace(t00, (uint32_t)10U);
+ fmul0(b0, t00, b0);
+ fsquare_times(t00, b0, (uint32_t)50U);
+ uint64_t *a0 = buf;
+ uint64_t *t0 = buf + (uint32_t)5U;
+ uint64_t *b = buf + (uint32_t)10U;
+ uint64_t *c = buf + (uint32_t)15U;
+ fsquare_times(a0, z, (uint32_t)1U);
+ fmul0(c, t0, b);
+ fsquare_times(t0, c, (uint32_t)100U);
+ fmul0(t0, t0, c);
+ fsquare_times_inplace(t0, (uint32_t)50U);
+ fmul0(t0, t0, b);
+ fsquare_times_inplace(t0, (uint32_t)2U);
+ fmul0(out, t0, a0);
+}
+
+static inline bool
+is_0(uint64_t *x)
+{
+ uint64_t x0 = x[0U];
+ uint64_t x1 = x[1U];
+ uint64_t x2 = x[2U];
+ uint64_t x3 = x[3U];
+ uint64_t x4 = x[4U];
+ return x0 == (uint64_t)0U && x1 == (uint64_t)0U && x2 == (uint64_t)0U && x3 == (uint64_t)0U && x4 == (uint64_t)0U;
+}
+
+static inline void
+mul_modp_sqrt_m1(uint64_t *x)
+{
+ uint64_t sqrt_m1[5U] = { 0U };
+ sqrt_m1[0U] = (uint64_t)0x00061b274a0ea0b0U;
+ sqrt_m1[1U] = (uint64_t)0x0000d5a5fc8f189dU;
+ sqrt_m1[2U] = (uint64_t)0x0007ef5e9cbd0c60U;
+ sqrt_m1[3U] = (uint64_t)0x00078595a6804c9eU;
+ sqrt_m1[4U] = (uint64_t)0x0002b8324804fc1dU;
+ fmul0(x, x, sqrt_m1);
+}
+
+static inline bool
+recover_x(uint64_t *x, uint64_t *y, uint64_t sign)
+{
+ uint64_t tmp[15U] = { 0U };
+ uint64_t *x2 = tmp;
+ uint64_t x00 = y[0U];
+ uint64_t x1 = y[1U];
+ uint64_t x21 = y[2U];
+ uint64_t x30 = y[3U];
+ uint64_t x4 = y[4U];
+ bool
+ b =
+ x00 >= (uint64_t)0x7ffffffffffedU && x1 == (uint64_t)0x7ffffffffffffU && x21 == (uint64_t)0x7ffffffffffffU && x30 == (uint64_t)0x7ffffffffffffU && x4 == (uint64_t)0x7ffffffffffffU;
+ bool res;
+ if (b) {
+ res = false;
+ } else {
+ uint64_t tmp1[20U] = { 0U };
+ uint64_t *one = tmp1;
+ uint64_t *y2 = tmp1 + (uint32_t)5U;
+ uint64_t *dyyi = tmp1 + (uint32_t)10U;
+ uint64_t *dyy = tmp1 + (uint32_t)15U;
+ one[0U] = (uint64_t)1U;
+ one[1U] = (uint64_t)0U;
+ one[2U] = (uint64_t)0U;
+ one[3U] = (uint64_t)0U;
+ one[4U] = (uint64_t)0U;
+ fsquare(y2, y);
+ times_d(dyy, y2);
+ fsum(dyy, dyy, one);
+ Hacl_Bignum25519_reduce_513(dyy);
+ Hacl_Bignum25519_inverse(dyyi, dyy);
+ fdifference(x2, y2, one);
+ fmul0(x2, x2, dyyi);
+ reduce(x2);
+ bool x2_is_0 = is_0(x2);
+ uint8_t z;
+ if (x2_is_0) {
+ if (sign == (uint64_t)0U) {
+ x[0U] = (uint64_t)0U;
+ x[1U] = (uint64_t)0U;
+ x[2U] = (uint64_t)0U;
+ x[3U] = (uint64_t)0U;
+ x[4U] = (uint64_t)0U;
+ z = (uint8_t)1U;
+ } else {
+ z = (uint8_t)0U;
+ }
+ } else {
+ z = (uint8_t)2U;
+ }
+ if (z == (uint8_t)0U) {
+ res = false;
+ } else if (z == (uint8_t)1U) {
+ res = true;
+ } else {
+ uint64_t *x210 = tmp;
+ uint64_t *x31 = tmp + (uint32_t)5U;
+ uint64_t *t00 = tmp + (uint32_t)10U;
+ pow2_252m2(x31, x210);
+ fsquare(t00, x31);
+ fdifference(t00, t00, x210);
+ Hacl_Bignum25519_reduce_513(t00);
+ reduce(t00);
+ bool t0_is_0 = is_0(t00);
+ if (!t0_is_0) {
+ mul_modp_sqrt_m1(x31);
+ }
+ uint64_t *x211 = tmp;
+ uint64_t *x3 = tmp + (uint32_t)5U;
+ uint64_t *t01 = tmp + (uint32_t)10U;
+ fsquare(t01, x3);
+ fdifference(t01, t01, x211);
+ Hacl_Bignum25519_reduce_513(t01);
+ reduce(t01);
+ bool z1 = is_0(t01);
+ if (z1 == false) {
+ res = false;
+ } else {
+ uint64_t *x32 = tmp + (uint32_t)5U;
+ uint64_t *t0 = tmp + (uint32_t)10U;
+ reduce(x32);
+ uint64_t x0 = x32[0U];
+ uint64_t x01 = x0 & (uint64_t)1U;
+ if (!(x01 == sign)) {
+ t0[0U] = (uint64_t)0U;
+ t0[1U] = (uint64_t)0U;
+ t0[2U] = (uint64_t)0U;
+ t0[3U] = (uint64_t)0U;
+ t0[4U] = (uint64_t)0U;
+ fdifference(x32, t0, x32);
+ Hacl_Bignum25519_reduce_513(x32);
+ reduce(x32);
+ }
+ memcpy(x, x32, (uint32_t)5U * sizeof(uint64_t));
+ res = true;
+ }
+ }
+ }
+ bool res0 = res;
+ return res0;
+}
+
+bool
+Hacl_Impl_Ed25519_PointDecompress_point_decompress(uint64_t *out, uint8_t *s)
+{
+ uint64_t tmp[10U] = { 0U };
+ uint64_t *y = tmp;
+ uint64_t *x = tmp + (uint32_t)5U;
+ uint8_t s31 = s[31U];
+ uint8_t z = s31 >> (uint32_t)7U;
+ uint64_t sign = (uint64_t)z;
+ Hacl_Bignum25519_load_51(y, s);
+ bool z0 = recover_x(x, y, sign);
+ bool res;
+ if (z0 == false) {
+ res = false;
+ } else {
+ uint64_t *outx = out;
+ uint64_t *outy = out + (uint32_t)5U;
+ uint64_t *outz = out + (uint32_t)10U;
+ uint64_t *outt = out + (uint32_t)15U;
+ memcpy(outx, x, (uint32_t)5U * sizeof(uint64_t));
+ memcpy(outy, y, (uint32_t)5U * sizeof(uint64_t));
+ outz[0U] = (uint64_t)1U;
+ outz[1U] = (uint64_t)0U;
+ outz[2U] = (uint64_t)0U;
+ outz[3U] = (uint64_t)0U;
+ outz[4U] = (uint64_t)0U;
+ fmul0(outt, x, y);
+ res = true;
+ }
+ bool res0 = res;
+ return res0;
+}
+
+void
+Hacl_Impl_Ed25519_PointCompress_point_compress(uint8_t *z, uint64_t *p)
+{
+ uint64_t tmp[15U] = { 0U };
+ uint64_t *x = tmp + (uint32_t)5U;
+ uint64_t *out = tmp + (uint32_t)10U;
+ uint64_t *zinv1 = tmp;
+ uint64_t *x1 = tmp + (uint32_t)5U;
+ uint64_t *out1 = tmp + (uint32_t)10U;
+ uint64_t *px = p;
+ uint64_t *py = p + (uint32_t)5U;
+ uint64_t *pz = p + (uint32_t)10U;
+ Hacl_Bignum25519_inverse(zinv1, pz);
+ fmul0(x1, px, zinv1);
+ reduce(x1);
+ fmul0(out1, py, zinv1);
+ Hacl_Bignum25519_reduce_513(out1);
+ uint64_t x0 = x[0U];
+ uint64_t b = x0 & (uint64_t)1U;
+ Hacl_Bignum25519_store_51(z, out);
+ uint8_t xbyte = (uint8_t)b;
+ uint8_t o31 = z[31U];
+ z[31U] = o31 + (xbyte << (uint32_t)7U);
+}
+
+static inline void
+barrett_reduction(uint64_t *z, uint64_t *t)
+{
+ uint64_t t0 = t[0U];
+ uint64_t t1 = t[1U];
+ uint64_t t2 = t[2U];
+ uint64_t t3 = t[3U];
+ uint64_t t4 = t[4U];
+ uint64_t t5 = t[5U];
+ uint64_t t6 = t[6U];
+ uint64_t t7 = t[7U];
+ uint64_t t8 = t[8U];
+ uint64_t t9 = t[9U];
+ uint64_t m00 = (uint64_t)0x12631a5cf5d3edU;
+ uint64_t m10 = (uint64_t)0xf9dea2f79cd658U;
+ uint64_t m20 = (uint64_t)0x000000000014deU;
+ uint64_t m30 = (uint64_t)0x00000000000000U;
+ uint64_t m40 = (uint64_t)0x00000010000000U;
+ uint64_t m0 = m00;
+ uint64_t m1 = m10;
+ uint64_t m2 = m20;
+ uint64_t m3 = m30;
+ uint64_t m4 = m40;
+ uint64_t m010 = (uint64_t)0x9ce5a30a2c131bU;
+ uint64_t m110 = (uint64_t)0x215d086329a7edU;
+ uint64_t m210 = (uint64_t)0xffffffffeb2106U;
+ uint64_t m310 = (uint64_t)0xffffffffffffffU;
+ uint64_t m410 = (uint64_t)0x00000fffffffffU;
+ uint64_t mu0 = m010;
+ uint64_t mu1 = m110;
+ uint64_t mu2 = m210;
+ uint64_t mu3 = m310;
+ uint64_t mu4 = m410;
+ uint64_t y_ = (t5 & (uint64_t)0xffffffU) << (uint32_t)32U;
+ uint64_t x_ = t4 >> (uint32_t)24U;
+ uint64_t z00 = x_ | y_;
+ uint64_t y_0 = (t6 & (uint64_t)0xffffffU) << (uint32_t)32U;
+ uint64_t x_0 = t5 >> (uint32_t)24U;
+ uint64_t z10 = x_0 | y_0;
+ uint64_t y_1 = (t7 & (uint64_t)0xffffffU) << (uint32_t)32U;
+ uint64_t x_1 = t6 >> (uint32_t)24U;
+ uint64_t z20 = x_1 | y_1;
+ uint64_t y_2 = (t8 & (uint64_t)0xffffffU) << (uint32_t)32U;
+ uint64_t x_2 = t7 >> (uint32_t)24U;
+ uint64_t z30 = x_2 | y_2;
+ uint64_t y_3 = (t9 & (uint64_t)0xffffffU) << (uint32_t)32U;
+ uint64_t x_3 = t8 >> (uint32_t)24U;
+ uint64_t z40 = x_3 | y_3;
+ uint64_t q0 = z00;
+ uint64_t q1 = z10;
+ uint64_t q2 = z20;
+ uint64_t q3 = z30;
+ uint64_t q4 = z40;
+ FStar_UInt128_uint128 xy000 = FStar_UInt128_mul_wide(q0, mu0);
+ FStar_UInt128_uint128 xy010 = FStar_UInt128_mul_wide(q0, mu1);
+ FStar_UInt128_uint128 xy020 = FStar_UInt128_mul_wide(q0, mu2);
+ FStar_UInt128_uint128 xy030 = FStar_UInt128_mul_wide(q0, mu3);
+ FStar_UInt128_uint128 xy040 = FStar_UInt128_mul_wide(q0, mu4);
+ FStar_UInt128_uint128 xy100 = FStar_UInt128_mul_wide(q1, mu0);
+ FStar_UInt128_uint128 xy110 = FStar_UInt128_mul_wide(q1, mu1);
+ FStar_UInt128_uint128 xy120 = FStar_UInt128_mul_wide(q1, mu2);
+ FStar_UInt128_uint128 xy130 = FStar_UInt128_mul_wide(q1, mu3);
+ FStar_UInt128_uint128 xy14 = FStar_UInt128_mul_wide(q1, mu4);
+ FStar_UInt128_uint128 xy200 = FStar_UInt128_mul_wide(q2, mu0);
+ FStar_UInt128_uint128 xy210 = FStar_UInt128_mul_wide(q2, mu1);
+ FStar_UInt128_uint128 xy220 = FStar_UInt128_mul_wide(q2, mu2);
+ FStar_UInt128_uint128 xy23 = FStar_UInt128_mul_wide(q2, mu3);
+ FStar_UInt128_uint128 xy24 = FStar_UInt128_mul_wide(q2, mu4);
+ FStar_UInt128_uint128 xy300 = FStar_UInt128_mul_wide(q3, mu0);
+ FStar_UInt128_uint128 xy310 = FStar_UInt128_mul_wide(q3, mu1);
+ FStar_UInt128_uint128 xy32 = FStar_UInt128_mul_wide(q3, mu2);
+ FStar_UInt128_uint128 xy33 = FStar_UInt128_mul_wide(q3, mu3);
+ FStar_UInt128_uint128 xy34 = FStar_UInt128_mul_wide(q3, mu4);
+ FStar_UInt128_uint128 xy400 = FStar_UInt128_mul_wide(q4, mu0);
+ FStar_UInt128_uint128 xy41 = FStar_UInt128_mul_wide(q4, mu1);
+ FStar_UInt128_uint128 xy42 = FStar_UInt128_mul_wide(q4, mu2);
+ FStar_UInt128_uint128 xy43 = FStar_UInt128_mul_wide(q4, mu3);
+ FStar_UInt128_uint128 xy44 = FStar_UInt128_mul_wide(q4, mu4);
+ FStar_UInt128_uint128 z01 = xy000;
+ FStar_UInt128_uint128 z11 = FStar_UInt128_add_mod(xy010, xy100);
+ FStar_UInt128_uint128 z21 = FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy020, xy110), xy200);
+ FStar_UInt128_uint128
+ z31 =
+ FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy030, xy120), xy210),
+ xy300);
+ FStar_UInt128_uint128
+ z41 =
+ FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy040,
+ xy130),
+ xy220),
+ xy310),
+ xy400);
+ FStar_UInt128_uint128
+ z5 =
+ FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy14, xy23), xy32),
+ xy41);
+ FStar_UInt128_uint128 z6 = FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy24, xy33), xy42);
+ FStar_UInt128_uint128 z7 = FStar_UInt128_add_mod(xy34, xy43);
+ FStar_UInt128_uint128 z8 = xy44;
+ FStar_UInt128_uint128 carry0 = FStar_UInt128_shift_right(z01, (uint32_t)56U);
+ FStar_UInt128_uint128 c00 = carry0;
+ FStar_UInt128_uint128
+ carry1 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z11, c00), (uint32_t)56U);
+ FStar_UInt128_uint128 c10 = carry1;
+ FStar_UInt128_uint128
+ carry2 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z21, c10), (uint32_t)56U);
+ FStar_UInt128_uint128 c20 = carry2;
+ FStar_UInt128_uint128
+ carry3 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z31, c20), (uint32_t)56U);
+ FStar_UInt128_uint128 c30 = carry3;
+ FStar_UInt128_uint128
+ carry4 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z41, c30), (uint32_t)56U);
+ uint64_t
+ t100 =
+ FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z41, c30)) & (uint64_t)0xffffffffffffffU;
+ FStar_UInt128_uint128 c40 = carry4;
+ uint64_t t410 = t100;
+ FStar_UInt128_uint128
+ carry5 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z5, c40), (uint32_t)56U);
+ uint64_t
+ t101 =
+ FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z5, c40)) & (uint64_t)0xffffffffffffffU;
+ FStar_UInt128_uint128 c5 = carry5;
+ uint64_t t51 = t101;
+ FStar_UInt128_uint128
+ carry6 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z6, c5), (uint32_t)56U);
+ uint64_t
+ t102 =
+ FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z6, c5)) & (uint64_t)0xffffffffffffffU;
+ FStar_UInt128_uint128 c6 = carry6;
+ uint64_t t61 = t102;
+ FStar_UInt128_uint128
+ carry7 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z7, c6), (uint32_t)56U);
+ uint64_t
+ t103 =
+ FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z7, c6)) & (uint64_t)0xffffffffffffffU;
+ FStar_UInt128_uint128 c7 = carry7;
+ uint64_t t71 = t103;
+ FStar_UInt128_uint128
+ carry8 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z8, c7), (uint32_t)56U);
+ uint64_t
+ t104 =
+ FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z8, c7)) & (uint64_t)0xffffffffffffffU;
+ FStar_UInt128_uint128 c8 = carry8;
+ uint64_t t81 = t104;
+ uint64_t t91 = FStar_UInt128_uint128_to_uint64(c8);
+ uint64_t qmu4_ = t410;
+ uint64_t qmu5_ = t51;
+ uint64_t qmu6_ = t61;
+ uint64_t qmu7_ = t71;
+ uint64_t qmu8_ = t81;
+ uint64_t qmu9_ = t91;
+ uint64_t y_4 = (qmu5_ & (uint64_t)0xffffffffffU) << (uint32_t)16U;
+ uint64_t x_4 = qmu4_ >> (uint32_t)40U;
+ uint64_t z02 = x_4 | y_4;
+ uint64_t y_5 = (qmu6_ & (uint64_t)0xffffffffffU) << (uint32_t)16U;
+ uint64_t x_5 = qmu5_ >> (uint32_t)40U;
+ uint64_t z12 = x_5 | y_5;
+ uint64_t y_6 = (qmu7_ & (uint64_t)0xffffffffffU) << (uint32_t)16U;
+ uint64_t x_6 = qmu6_ >> (uint32_t)40U;
+ uint64_t z22 = x_6 | y_6;
+ uint64_t y_7 = (qmu8_ & (uint64_t)0xffffffffffU) << (uint32_t)16U;
+ uint64_t x_7 = qmu7_ >> (uint32_t)40U;
+ uint64_t z32 = x_7 | y_7;
+ uint64_t y_8 = (qmu9_ & (uint64_t)0xffffffffffU) << (uint32_t)16U;
+ uint64_t x_8 = qmu8_ >> (uint32_t)40U;
+ uint64_t z42 = x_8 | y_8;
+ uint64_t qdiv0 = z02;
+ uint64_t qdiv1 = z12;
+ uint64_t qdiv2 = z22;
+ uint64_t qdiv3 = z32;
+ uint64_t qdiv4 = z42;
+ uint64_t r0 = t0;
+ uint64_t r1 = t1;
+ uint64_t r2 = t2;
+ uint64_t r3 = t3;
+ uint64_t r4 = t4 & (uint64_t)0xffffffffffU;
+ FStar_UInt128_uint128 xy00 = FStar_UInt128_mul_wide(qdiv0, m0);
+ FStar_UInt128_uint128 xy01 = FStar_UInt128_mul_wide(qdiv0, m1);
+ FStar_UInt128_uint128 xy02 = FStar_UInt128_mul_wide(qdiv0, m2);
+ FStar_UInt128_uint128 xy03 = FStar_UInt128_mul_wide(qdiv0, m3);
+ FStar_UInt128_uint128 xy04 = FStar_UInt128_mul_wide(qdiv0, m4);
+ FStar_UInt128_uint128 xy10 = FStar_UInt128_mul_wide(qdiv1, m0);
+ FStar_UInt128_uint128 xy11 = FStar_UInt128_mul_wide(qdiv1, m1);
+ FStar_UInt128_uint128 xy12 = FStar_UInt128_mul_wide(qdiv1, m2);
+ FStar_UInt128_uint128 xy13 = FStar_UInt128_mul_wide(qdiv1, m3);
+ FStar_UInt128_uint128 xy20 = FStar_UInt128_mul_wide(qdiv2, m0);
+ FStar_UInt128_uint128 xy21 = FStar_UInt128_mul_wide(qdiv2, m1);
+ FStar_UInt128_uint128 xy22 = FStar_UInt128_mul_wide(qdiv2, m2);
+ FStar_UInt128_uint128 xy30 = FStar_UInt128_mul_wide(qdiv3, m0);
+ FStar_UInt128_uint128 xy31 = FStar_UInt128_mul_wide(qdiv3, m1);
+ FStar_UInt128_uint128 xy40 = FStar_UInt128_mul_wide(qdiv4, m0);
+ FStar_UInt128_uint128 carry9 = FStar_UInt128_shift_right(xy00, (uint32_t)56U);
+ uint64_t t105 = FStar_UInt128_uint128_to_uint64(xy00) & (uint64_t)0xffffffffffffffU;
+ FStar_UInt128_uint128 c0 = carry9;
+ uint64_t t010 = t105;
+ FStar_UInt128_uint128
+ carry10 =
+ FStar_UInt128_shift_right(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy01, xy10), c0),
+ (uint32_t)56U);
+ uint64_t
+ t106 =
+ FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy01, xy10), c0)) & (uint64_t)0xffffffffffffffU;
+ FStar_UInt128_uint128 c11 = carry10;
+ uint64_t t110 = t106;
+ FStar_UInt128_uint128
+ carry11 =
+ FStar_UInt128_shift_right(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy02,
+ xy11),
+ xy20),
+ c11),
+ (uint32_t)56U);
+ uint64_t
+ t107 =
+ FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy02,
+ xy11),
+ xy20),
+ c11)) &
+ (uint64_t)0xffffffffffffffU;
+ FStar_UInt128_uint128 c21 = carry11;
+ uint64_t t210 = t107;
+ FStar_UInt128_uint128
+ carry =
+ FStar_UInt128_shift_right(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy03,
+ xy12),
+ xy21),
+ xy30),
+ c21),
+ (uint32_t)56U);
+ uint64_t
+ t108 =
+ FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy03,
+ xy12),
+ xy21),
+ xy30),
+ c21)) &
+ (uint64_t)0xffffffffffffffU;
+ FStar_UInt128_uint128 c31 = carry;
+ uint64_t t310 = t108;
+ uint64_t
+ t411 =
+ FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy04,
+ xy13),
+ xy22),
+ xy31),
+ xy40),
+ c31)) &
+ (uint64_t)0xffffffffffU;
+ uint64_t qmul0 = t010;
+ uint64_t qmul1 = t110;
+ uint64_t qmul2 = t210;
+ uint64_t qmul3 = t310;
+ uint64_t qmul4 = t411;
+ uint64_t b5 = (r0 - qmul0) >> (uint32_t)63U;
+ uint64_t t109 = (b5 << (uint32_t)56U) + r0 - qmul0;
+ uint64_t c1 = b5;
+ uint64_t t011 = t109;
+ uint64_t b6 = (r1 - (qmul1 + c1)) >> (uint32_t)63U;
+ uint64_t t1010 = (b6 << (uint32_t)56U) + r1 - (qmul1 + c1);
+ uint64_t c2 = b6;
+ uint64_t t111 = t1010;
+ uint64_t b7 = (r2 - (qmul2 + c2)) >> (uint32_t)63U;
+ uint64_t t1011 = (b7 << (uint32_t)56U) + r2 - (qmul2 + c2);
+ uint64_t c3 = b7;
+ uint64_t t211 = t1011;
+ uint64_t b8 = (r3 - (qmul3 + c3)) >> (uint32_t)63U;
+ uint64_t t1012 = (b8 << (uint32_t)56U) + r3 - (qmul3 + c3);
+ uint64_t c4 = b8;
+ uint64_t t311 = t1012;
+ uint64_t b9 = (r4 - (qmul4 + c4)) >> (uint32_t)63U;
+ uint64_t t1013 = (b9 << (uint32_t)40U) + r4 - (qmul4 + c4);
+ uint64_t t412 = t1013;
+ uint64_t s0 = t011;
+ uint64_t s1 = t111;
+ uint64_t s2 = t211;
+ uint64_t s3 = t311;
+ uint64_t s4 = t412;
+ uint64_t m01 = (uint64_t)0x12631a5cf5d3edU;
+ uint64_t m11 = (uint64_t)0xf9dea2f79cd658U;
+ uint64_t m21 = (uint64_t)0x000000000014deU;
+ uint64_t m31 = (uint64_t)0x00000000000000U;
+ uint64_t m41 = (uint64_t)0x00000010000000U;
+ uint64_t y0 = m01;
+ uint64_t y1 = m11;
+ uint64_t y2 = m21;
+ uint64_t y3 = m31;
+ uint64_t y4 = m41;
+ uint64_t b10 = (s0 - y0) >> (uint32_t)63U;
+ uint64_t t1014 = (b10 << (uint32_t)56U) + s0 - y0;
+ uint64_t b0 = b10;
+ uint64_t t01 = t1014;
+ uint64_t b11 = (s1 - (y1 + b0)) >> (uint32_t)63U;
+ uint64_t t1015 = (b11 << (uint32_t)56U) + s1 - (y1 + b0);
+ uint64_t b1 = b11;
+ uint64_t t11 = t1015;
+ uint64_t b12 = (s2 - (y2 + b1)) >> (uint32_t)63U;
+ uint64_t t1016 = (b12 << (uint32_t)56U) + s2 - (y2 + b1);
+ uint64_t b2 = b12;
+ uint64_t t21 = t1016;
+ uint64_t b13 = (s3 - (y3 + b2)) >> (uint32_t)63U;
+ uint64_t t1017 = (b13 << (uint32_t)56U) + s3 - (y3 + b2);
+ uint64_t b3 = b13;
+ uint64_t t31 = t1017;
+ uint64_t b = (s4 - (y4 + b3)) >> (uint32_t)63U;
+ uint64_t t10 = (b << (uint32_t)56U) + s4 - (y4 + b3);
+ uint64_t b4 = b;
+ uint64_t t41 = t10;
+ uint64_t mask = b4 - (uint64_t)1U;
+ uint64_t z03 = s0 ^ (mask & (s0 ^ t01));
+ uint64_t z13 = s1 ^ (mask & (s1 ^ t11));
+ uint64_t z23 = s2 ^ (mask & (s2 ^ t21));
+ uint64_t z33 = s3 ^ (mask & (s3 ^ t31));
+ uint64_t z43 = s4 ^ (mask & (s4 ^ t41));
+ uint64_t z04 = z03;
+ uint64_t z14 = z13;
+ uint64_t z24 = z23;
+ uint64_t z34 = z33;
+ uint64_t z44 = z43;
+ uint64_t o0 = z04;
+ uint64_t o1 = z14;
+ uint64_t o2 = z24;
+ uint64_t o3 = z34;
+ uint64_t o4 = z44;
+ uint64_t z0 = o0;
+ uint64_t z1 = o1;
+ uint64_t z2 = o2;
+ uint64_t z3 = o3;
+ uint64_t z4 = o4;
+ z[0U] = z0;
+ z[1U] = z1;
+ z[2U] = z2;
+ z[3U] = z3;
+ z[4U] = z4;
+}
+
+static inline void
+mul_modq(uint64_t *out, uint64_t *x, uint64_t *y)
+{
+ uint64_t tmp[10U] = { 0U };
+ uint64_t x0 = x[0U];
+ uint64_t x1 = x[1U];
+ uint64_t x2 = x[2U];
+ uint64_t x3 = x[3U];
+ uint64_t x4 = x[4U];
+ uint64_t y0 = y[0U];
+ uint64_t y1 = y[1U];
+ uint64_t y2 = y[2U];
+ uint64_t y3 = y[3U];
+ uint64_t y4 = y[4U];
+ FStar_UInt128_uint128 xy00 = FStar_UInt128_mul_wide(x0, y0);
+ FStar_UInt128_uint128 xy01 = FStar_UInt128_mul_wide(x0, y1);
+ FStar_UInt128_uint128 xy02 = FStar_UInt128_mul_wide(x0, y2);
+ FStar_UInt128_uint128 xy03 = FStar_UInt128_mul_wide(x0, y3);
+ FStar_UInt128_uint128 xy04 = FStar_UInt128_mul_wide(x0, y4);
+ FStar_UInt128_uint128 xy10 = FStar_UInt128_mul_wide(x1, y0);
+ FStar_UInt128_uint128 xy11 = FStar_UInt128_mul_wide(x1, y1);
+ FStar_UInt128_uint128 xy12 = FStar_UInt128_mul_wide(x1, y2);
+ FStar_UInt128_uint128 xy13 = FStar_UInt128_mul_wide(x1, y3);
+ FStar_UInt128_uint128 xy14 = FStar_UInt128_mul_wide(x1, y4);
+ FStar_UInt128_uint128 xy20 = FStar_UInt128_mul_wide(x2, y0);
+ FStar_UInt128_uint128 xy21 = FStar_UInt128_mul_wide(x2, y1);
+ FStar_UInt128_uint128 xy22 = FStar_UInt128_mul_wide(x2, y2);
+ FStar_UInt128_uint128 xy23 = FStar_UInt128_mul_wide(x2, y3);
+ FStar_UInt128_uint128 xy24 = FStar_UInt128_mul_wide(x2, y4);
+ FStar_UInt128_uint128 xy30 = FStar_UInt128_mul_wide(x3, y0);
+ FStar_UInt128_uint128 xy31 = FStar_UInt128_mul_wide(x3, y1);
+ FStar_UInt128_uint128 xy32 = FStar_UInt128_mul_wide(x3, y2);
+ FStar_UInt128_uint128 xy33 = FStar_UInt128_mul_wide(x3, y3);
+ FStar_UInt128_uint128 xy34 = FStar_UInt128_mul_wide(x3, y4);
+ FStar_UInt128_uint128 xy40 = FStar_UInt128_mul_wide(x4, y0);
+ FStar_UInt128_uint128 xy41 = FStar_UInt128_mul_wide(x4, y1);
+ FStar_UInt128_uint128 xy42 = FStar_UInt128_mul_wide(x4, y2);
+ FStar_UInt128_uint128 xy43 = FStar_UInt128_mul_wide(x4, y3);
+ FStar_UInt128_uint128 xy44 = FStar_UInt128_mul_wide(x4, y4);
+ FStar_UInt128_uint128 z00 = xy00;
+ FStar_UInt128_uint128 z10 = FStar_UInt128_add_mod(xy01, xy10);
+ FStar_UInt128_uint128 z20 = FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy02, xy11), xy20);
+ FStar_UInt128_uint128
+ z30 =
+ FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy03, xy12), xy21),
+ xy30);
+ FStar_UInt128_uint128
+ z40 =
+ FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy04,
+ xy13),
+ xy22),
+ xy31),
+ xy40);
+ FStar_UInt128_uint128
+ z50 =
+ FStar_UInt128_add_mod(FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy14, xy23), xy32),
+ xy41);
+ FStar_UInt128_uint128 z60 = FStar_UInt128_add_mod(FStar_UInt128_add_mod(xy24, xy33), xy42);
+ FStar_UInt128_uint128 z70 = FStar_UInt128_add_mod(xy34, xy43);
+ FStar_UInt128_uint128 z80 = xy44;
+ FStar_UInt128_uint128 carry0 = FStar_UInt128_shift_right(z00, (uint32_t)56U);
+ uint64_t t10 = FStar_UInt128_uint128_to_uint64(z00) & (uint64_t)0xffffffffffffffU;
+ FStar_UInt128_uint128 c0 = carry0;
+ uint64_t t0 = t10;
+ FStar_UInt128_uint128
+ carry1 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z10, c0), (uint32_t)56U);
+ uint64_t
+ t11 =
+ FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z10, c0)) & (uint64_t)0xffffffffffffffU;
+ FStar_UInt128_uint128 c1 = carry1;
+ uint64_t t1 = t11;
+ FStar_UInt128_uint128
+ carry2 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z20, c1), (uint32_t)56U);
+ uint64_t
+ t12 =
+ FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z20, c1)) & (uint64_t)0xffffffffffffffU;
+ FStar_UInt128_uint128 c2 = carry2;
+ uint64_t t2 = t12;
+ FStar_UInt128_uint128
+ carry3 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z30, c2), (uint32_t)56U);
+ uint64_t
+ t13 =
+ FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z30, c2)) & (uint64_t)0xffffffffffffffU;
+ FStar_UInt128_uint128 c3 = carry3;
+ uint64_t t3 = t13;
+ FStar_UInt128_uint128
+ carry4 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z40, c3), (uint32_t)56U);
+ uint64_t
+ t14 =
+ FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z40, c3)) & (uint64_t)0xffffffffffffffU;
+ FStar_UInt128_uint128 c4 = carry4;
+ uint64_t t4 = t14;
+ FStar_UInt128_uint128
+ carry5 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z50, c4), (uint32_t)56U);
+ uint64_t
+ t15 =
+ FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z50, c4)) & (uint64_t)0xffffffffffffffU;
+ FStar_UInt128_uint128 c5 = carry5;
+ uint64_t t5 = t15;
+ FStar_UInt128_uint128
+ carry6 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z60, c5), (uint32_t)56U);
+ uint64_t
+ t16 =
+ FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z60, c5)) & (uint64_t)0xffffffffffffffU;
+ FStar_UInt128_uint128 c6 = carry6;
+ uint64_t t6 = t16;
+ FStar_UInt128_uint128
+ carry7 = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z70, c6), (uint32_t)56U);
+ uint64_t
+ t17 =
+ FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z70, c6)) & (uint64_t)0xffffffffffffffU;
+ FStar_UInt128_uint128 c7 = carry7;
+ uint64_t t7 = t17;
+ FStar_UInt128_uint128
+ carry = FStar_UInt128_shift_right(FStar_UInt128_add_mod(z80, c7), (uint32_t)56U);
+ uint64_t
+ t =
+ FStar_UInt128_uint128_to_uint64(FStar_UInt128_add_mod(z80, c7)) & (uint64_t)0xffffffffffffffU;
+ FStar_UInt128_uint128 c8 = carry;
+ uint64_t t8 = t;
+ uint64_t t9 = FStar_UInt128_uint128_to_uint64(c8);
+ uint64_t z0 = t0;
+ uint64_t z1 = t1;
+ uint64_t z2 = t2;
+ uint64_t z3 = t3;
+ uint64_t z4 = t4;
+ uint64_t z5 = t5;
+ uint64_t z6 = t6;
+ uint64_t z7 = t7;
+ uint64_t z8 = t8;
+ uint64_t z9 = t9;
+ tmp[0U] = z0;
+ tmp[1U] = z1;
+ tmp[2U] = z2;
+ tmp[3U] = z3;
+ tmp[4U] = z4;
+ tmp[5U] = z5;
+ tmp[6U] = z6;
+ tmp[7U] = z7;
+ tmp[8U] = z8;
+ tmp[9U] = z9;
+ barrett_reduction(out, tmp);
+}
+
+static inline void
+add_modq(uint64_t *out, uint64_t *x, uint64_t *y)
+{
+ uint64_t x0 = x[0U];
+ uint64_t x1 = x[1U];
+ uint64_t x2 = x[2U];
+ uint64_t x3 = x[3U];
+ uint64_t x4 = x[4U];
+ uint64_t y0 = y[0U];
+ uint64_t y1 = y[1U];
+ uint64_t y2 = y[2U];
+ uint64_t y3 = y[3U];
+ uint64_t y4 = y[4U];
+ uint64_t carry0 = (x0 + y0) >> (uint32_t)56U;
+ uint64_t t0 = (x0 + y0) & (uint64_t)0xffffffffffffffU;
+ uint64_t t00 = t0;
+ uint64_t c0 = carry0;
+ uint64_t carry1 = (x1 + y1 + c0) >> (uint32_t)56U;
+ uint64_t t1 = (x1 + y1 + c0) & (uint64_t)0xffffffffffffffU;
+ uint64_t t10 = t1;
+ uint64_t c1 = carry1;
+ uint64_t carry2 = (x2 + y2 + c1) >> (uint32_t)56U;
+ uint64_t t2 = (x2 + y2 + c1) & (uint64_t)0xffffffffffffffU;
+ uint64_t t20 = t2;
+ uint64_t c2 = carry2;
+ uint64_t carry = (x3 + y3 + c2) >> (uint32_t)56U;
+ uint64_t t3 = (x3 + y3 + c2) & (uint64_t)0xffffffffffffffU;
+ uint64_t t30 = t3;
+ uint64_t c3 = carry;
+ uint64_t t4 = x4 + y4 + c3;
+ uint64_t m0 = (uint64_t)0x12631a5cf5d3edU;
+ uint64_t m1 = (uint64_t)0xf9dea2f79cd658U;
+ uint64_t m2 = (uint64_t)0x000000000014deU;
+ uint64_t m3 = (uint64_t)0x00000000000000U;
+ uint64_t m4 = (uint64_t)0x00000010000000U;
+ uint64_t y01 = m0;
+ uint64_t y11 = m1;
+ uint64_t y21 = m2;
+ uint64_t y31 = m3;
+ uint64_t y41 = m4;
+ uint64_t b5 = (t00 - y01) >> (uint32_t)63U;
+ uint64_t t5 = (b5 << (uint32_t)56U) + t00 - y01;
+ uint64_t b0 = b5;
+ uint64_t t01 = t5;
+ uint64_t b6 = (t10 - (y11 + b0)) >> (uint32_t)63U;
+ uint64_t t6 = (b6 << (uint32_t)56U) + t10 - (y11 + b0);
+ uint64_t b1 = b6;
+ uint64_t t11 = t6;
+ uint64_t b7 = (t20 - (y21 + b1)) >> (uint32_t)63U;
+ uint64_t t7 = (b7 << (uint32_t)56U) + t20 - (y21 + b1);
+ uint64_t b2 = b7;
+ uint64_t t21 = t7;
+ uint64_t b8 = (t30 - (y31 + b2)) >> (uint32_t)63U;
+ uint64_t t8 = (b8 << (uint32_t)56U) + t30 - (y31 + b2);
+ uint64_t b3 = b8;
+ uint64_t t31 = t8;
+ uint64_t b = (t4 - (y41 + b3)) >> (uint32_t)63U;
+ uint64_t t = (b << (uint32_t)56U) + t4 - (y41 + b3);
+ uint64_t b4 = b;
+ uint64_t t41 = t;
+ uint64_t mask = b4 - (uint64_t)1U;
+ uint64_t z00 = t00 ^ (mask & (t00 ^ t01));
+ uint64_t z10 = t10 ^ (mask & (t10 ^ t11));
+ uint64_t z20 = t20 ^ (mask & (t20 ^ t21));
+ uint64_t z30 = t30 ^ (mask & (t30 ^ t31));
+ uint64_t z40 = t4 ^ (mask & (t4 ^ t41));
+ uint64_t z01 = z00;
+ uint64_t z11 = z10;
+ uint64_t z21 = z20;
+ uint64_t z31 = z30;
+ uint64_t z41 = z40;
+ uint64_t o0 = z01;
+ uint64_t o1 = z11;
+ uint64_t o2 = z21;
+ uint64_t o3 = z31;
+ uint64_t o4 = z41;
+ uint64_t z0 = o0;
+ uint64_t z1 = o1;
+ uint64_t z2 = o2;
+ uint64_t z3 = o3;
+ uint64_t z4 = o4;
+ out[0U] = z0;
+ out[1U] = z1;
+ out[2U] = z2;
+ out[3U] = z3;
+ out[4U] = z4;
+}
+
+static inline bool
+gte_q(uint64_t *s)
+{
+ uint64_t s0 = s[0U];
+ uint64_t s1 = s[1U];
+ uint64_t s2 = s[2U];
+ uint64_t s3 = s[3U];
+ uint64_t s4 = s[4U];
+ if (s4 > (uint64_t)0x00000010000000U) {
+ return true;
+ }
+ if (s4 < (uint64_t)0x00000010000000U) {
+ return false;
+ }
+ if (s3 > (uint64_t)0x00000000000000U) {
+ return true;
+ }
+ if (s2 > (uint64_t)0x000000000014deU) {
+ return true;
+ }
+ if (s2 < (uint64_t)0x000000000014deU) {
+ return false;
+ }
+ if (s1 > (uint64_t)0xf9dea2f79cd658U) {
+ return true;
+ }
+ if (s1 < (uint64_t)0xf9dea2f79cd658U) {
+ return false;
+ }
+ if (s0 >= (uint64_t)0x12631a5cf5d3edU) {
+ return true;
+ }
+ return false;
+}
+
+static inline bool
+eq(uint64_t *a, uint64_t *b)
+{
+ uint64_t a0 = a[0U];
+ uint64_t a1 = a[1U];
+ uint64_t a2 = a[2U];
+ uint64_t a3 = a[3U];
+ uint64_t a4 = a[4U];
+ uint64_t b0 = b[0U];
+ uint64_t b1 = b[1U];
+ uint64_t b2 = b[2U];
+ uint64_t b3 = b[3U];
+ uint64_t b4 = b[4U];
+ return a0 == b0 && a1 == b1 && a2 == b2 && a3 == b3 && a4 == b4;
+}
+
+bool
+Hacl_Impl_Ed25519_PointEqual_point_equal(uint64_t *p, uint64_t *q)
+{
+ uint64_t tmp[20U] = { 0U };
+ uint64_t *pxqz = tmp;
+ uint64_t *qxpz = tmp + (uint32_t)5U;
+ fmul0(pxqz, p, q + (uint32_t)10U);
+ reduce(pxqz);
+ fmul0(qxpz, q, p + (uint32_t)10U);
+ reduce(qxpz);
+ bool b = eq(pxqz, qxpz);
+ if (b) {
+ uint64_t *pyqz = tmp + (uint32_t)10U;
+ uint64_t *qypz = tmp + (uint32_t)15U;
+ fmul0(pyqz, p + (uint32_t)5U, q + (uint32_t)10U);
+ reduce(pyqz);
+ fmul0(qypz, q + (uint32_t)5U, p + (uint32_t)10U);
+ reduce(qypz);
+ return eq(pyqz, qypz);
+ }
+ return false;
+}
+
+void
+Hacl_Impl_Ed25519_PointNegate_point_negate(uint64_t *p, uint64_t *out)
+{
+ uint64_t zero[5U] = { 0U };
+ zero[0U] = (uint64_t)0U;
+ zero[1U] = (uint64_t)0U;
+ zero[2U] = (uint64_t)0U;
+ zero[3U] = (uint64_t)0U;
+ zero[4U] = (uint64_t)0U;
+ uint64_t *x = p;
+ uint64_t *y = p + (uint32_t)5U;
+ uint64_t *z = p + (uint32_t)10U;
+ uint64_t *t = p + (uint32_t)15U;
+ uint64_t *x1 = out;
+ uint64_t *y1 = out + (uint32_t)5U;
+ uint64_t *z1 = out + (uint32_t)10U;
+ uint64_t *t1 = out + (uint32_t)15U;
+ fdifference(x1, zero, x);
+ Hacl_Bignum25519_reduce_513(x1);
+ memcpy(y1, y, (uint32_t)5U * sizeof(uint64_t));
+ memcpy(z1, z, (uint32_t)5U * sizeof(uint64_t));
+ fdifference(t1, zero, t);
+ Hacl_Bignum25519_reduce_513(t1);
+}
+
+void
+Hacl_Impl_Ed25519_Ladder_point_mul(uint64_t *out, uint8_t *scalar, uint64_t *q)
+{
+ uint64_t bscalar[4U] = { 0U };
+ KRML_MAYBE_FOR4(i,
+ (uint32_t)0U,
+ (uint32_t)4U,
+ (uint32_t)1U,
+ uint64_t *os = bscalar;
+ uint8_t *bj = scalar + i * (uint32_t)8U;
+ uint64_t u = load64_le(bj);
+ uint64_t r = u;
+ uint64_t x = r;
+ os[i] = x;);
+ uint64_t table[320U] = { 0U };
+ uint64_t tmp[20U] = { 0U };
+ uint64_t *t0 = table;
+ uint64_t *t1 = table + (uint32_t)20U;
+ Hacl_Impl_Ed25519_PointConstants_make_point_inf(t0);
+ memcpy(t1, q, (uint32_t)20U * 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)20U;
+ Hacl_Impl_Ed25519_PointDouble_point_double(tmp, t11);
+ memcpy(table + ((uint32_t)2U * i + (uint32_t)2U) * (uint32_t)20U,
+ tmp,
+ (uint32_t)20U * sizeof(uint64_t));
+ uint64_t *t2 = table + ((uint32_t)2U * i + (uint32_t)2U) * (uint32_t)20U;
+ Hacl_Impl_Ed25519_PointAdd_point_add(tmp, q, t2);
+ memcpy(table + ((uint32_t)2U * i + (uint32_t)3U) * (uint32_t)20U,
+ tmp,
+ (uint32_t)20U * sizeof(uint64_t)););
+ Hacl_Impl_Ed25519_PointConstants_make_point_inf(out);
+ uint64_t tmp0[20U] = { 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,
+ Hacl_Impl_Ed25519_PointDouble_point_double(out, out););
+ 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, bscalar, k, (uint32_t)4U);
+ memcpy(tmp0, (uint64_t *)table, (uint32_t)20U * 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)20U;
+ for (uint32_t i = (uint32_t)0U; i < (uint32_t)20U; i++) {
+ uint64_t *os = tmp0;
+ uint64_t x = (c & res_j[i]) | (~c & tmp0[i]);
+ os[i] = x;
+ });
+ Hacl_Impl_Ed25519_PointAdd_point_add(out, out, 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)20U * 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)20U;
+ for (uint32_t i = (uint32_t)0U; i < (uint32_t)20U; i++) {
+ 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 *out, uint8_t *scalar)
+{
+ uint64_t bscalar[4U] = { 0U };
+ KRML_MAYBE_FOR4(i,
+ (uint32_t)0U,
+ (uint32_t)4U,
+ (uint32_t)1U,
+ uint64_t *os = bscalar;
+ uint8_t *bj = scalar + i * (uint32_t)8U;
+ uint64_t u = load64_le(bj);
+ uint64_t r = u;
+ uint64_t x = r;
+ os[i] = x;);
+ uint64_t q1[20U] = { 0U };
+ uint64_t *gx = q1;
+ uint64_t *gy = q1 + (uint32_t)5U;
+ uint64_t *gz = q1 + (uint32_t)10U;
+ uint64_t *gt = q1 + (uint32_t)15U;
+ gx[0U] = (uint64_t)0x00062d608f25d51aU;
+ gx[1U] = (uint64_t)0x000412a4b4f6592aU;
+ gx[2U] = (uint64_t)0x00075b7171a4b31dU;
+ gx[3U] = (uint64_t)0x0001ff60527118feU;
+ gx[4U] = (uint64_t)0x000216936d3cd6e5U;
+ gy[0U] = (uint64_t)0x0006666666666658U;
+ gy[1U] = (uint64_t)0x0004ccccccccccccU;
+ gy[2U] = (uint64_t)0x0001999999999999U;
+ gy[3U] = (uint64_t)0x0003333333333333U;
+ gy[4U] = (uint64_t)0x0006666666666666U;
+ gz[0U] = (uint64_t)1U;
+ gz[1U] = (uint64_t)0U;
+ gz[2U] = (uint64_t)0U;
+ gz[3U] = (uint64_t)0U;
+ gz[4U] = (uint64_t)0U;
+ gt[0U] = (uint64_t)0x00068ab3a5b7dda3U;
+ gt[1U] = (uint64_t)0x00000eea2a5eadbbU;
+ gt[2U] = (uint64_t)0x0002af8df483c27eU;
+ gt[3U] = (uint64_t)0x000332b375274732U;
+ gt[4U] = (uint64_t)0x00067875f0fd78b7U;
+ uint64_t
+ q2[20U] = {
+ (uint64_t)13559344787725U, (uint64_t)2051621493703448U, (uint64_t)1947659315640708U,
+ (uint64_t)626856790370168U, (uint64_t)1592804284034836U, (uint64_t)1781728767459187U,
+ (uint64_t)278818420518009U, (uint64_t)2038030359908351U, (uint64_t)910625973862690U,
+ (uint64_t)471887343142239U, (uint64_t)1298543306606048U, (uint64_t)794147365642417U,
+ (uint64_t)129968992326749U, (uint64_t)523140861678572U, (uint64_t)1166419653909231U,
+ (uint64_t)2009637196928390U, (uint64_t)1288020222395193U, (uint64_t)1007046974985829U,
+ (uint64_t)208981102651386U, (uint64_t)2074009315253380U
+ };
+ uint64_t
+ q3[20U] = {
+ (uint64_t)557549315715710U, (uint64_t)196756086293855U, (uint64_t)846062225082495U,
+ (uint64_t)1865068224838092U, (uint64_t)991112090754908U, (uint64_t)522916421512828U,
+ (uint64_t)2098523346722375U, (uint64_t)1135633221747012U, (uint64_t)858420432114866U,
+ (uint64_t)186358544306082U, (uint64_t)1044420411868480U, (uint64_t)2080052304349321U,
+ (uint64_t)557301814716724U, (uint64_t)1305130257814057U, (uint64_t)2126012765451197U,
+ (uint64_t)1441004402875101U, (uint64_t)353948968859203U, (uint64_t)470765987164835U,
+ (uint64_t)1507675957683570U, (uint64_t)1086650358745097U
+ };
+ uint64_t
+ q4[20U] = {
+ (uint64_t)1129953239743101U, (uint64_t)1240339163956160U, (uint64_t)61002583352401U,
+ (uint64_t)2017604552196030U, (uint64_t)1576867829229863U, (uint64_t)1508654942849389U,
+ (uint64_t)270111619664077U, (uint64_t)1253097517254054U, (uint64_t)721798270973250U,
+ (uint64_t)161923365415298U, (uint64_t)828530877526011U, (uint64_t)1494851059386763U,
+ (uint64_t)662034171193976U, (uint64_t)1315349646974670U, (uint64_t)2199229517308806U,
+ (uint64_t)497078277852673U, (uint64_t)1310507715989956U, (uint64_t)1881315714002105U,
+ (uint64_t)2214039404983803U, (uint64_t)1331036420272667U
+ };
+ uint64_t *r1 = bscalar;
+ uint64_t *r2 = bscalar + (uint32_t)1U;
+ uint64_t *r3 = bscalar + (uint32_t)2U;
+ uint64_t *r4 = bscalar + (uint32_t)3U;
+ Hacl_Impl_Ed25519_PointConstants_make_point_inf(out);
+ uint64_t tmp[20U] = { 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,
+ Hacl_Impl_Ed25519_PointDouble_point_double(out, out););
+ 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_Ed25519_PrecompTable_precomp_g_pow2_192_table_w4, bits_l, tmp);
+ Hacl_Impl_Ed25519_PointAdd_point_add(out, out, 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_Ed25519_PrecompTable_precomp_g_pow2_128_table_w4, bits_l0, tmp);
+ Hacl_Impl_Ed25519_PointAdd_point_add(out, out, 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_Ed25519_PrecompTable_precomp_g_pow2_64_table_w4, bits_l1, tmp);
+ Hacl_Impl_Ed25519_PointAdd_point_add(out, out, 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_Ed25519_PrecompTable_precomp_basepoint_table_w4, bits_l2, tmp);
+ Hacl_Impl_Ed25519_PointAdd_point_add(out, out, tmp););
+ KRML_HOST_IGNORE(q2);
+ KRML_HOST_IGNORE(q3);
+ KRML_HOST_IGNORE(q4);
+}
+
+static inline void
+point_mul_g_double_vartime(uint64_t *out, uint8_t *scalar1, uint8_t *scalar2, uint64_t *q2)
+{
+ uint64_t tmp[28U] = { 0U };
+ uint64_t *g = tmp;
+ uint64_t *bscalar1 = tmp + (uint32_t)20U;
+ uint64_t *bscalar2 = tmp + (uint32_t)24U;
+ uint64_t *gx = g;
+ uint64_t *gy = g + (uint32_t)5U;
+ uint64_t *gz = g + (uint32_t)10U;
+ uint64_t *gt = g + (uint32_t)15U;
+ gx[0U] = (uint64_t)0x00062d608f25d51aU;
+ gx[1U] = (uint64_t)0x000412a4b4f6592aU;
+ gx[2U] = (uint64_t)0x00075b7171a4b31dU;
+ gx[3U] = (uint64_t)0x0001ff60527118feU;
+ gx[4U] = (uint64_t)0x000216936d3cd6e5U;
+ gy[0U] = (uint64_t)0x0006666666666658U;
+ gy[1U] = (uint64_t)0x0004ccccccccccccU;
+ gy[2U] = (uint64_t)0x0001999999999999U;
+ gy[3U] = (uint64_t)0x0003333333333333U;
+ gy[4U] = (uint64_t)0x0006666666666666U;
+ gz[0U] = (uint64_t)1U;
+ gz[1U] = (uint64_t)0U;
+ gz[2U] = (uint64_t)0U;
+ gz[3U] = (uint64_t)0U;
+ gz[4U] = (uint64_t)0U;
+ gt[0U] = (uint64_t)0x00068ab3a5b7dda3U;
+ gt[1U] = (uint64_t)0x00000eea2a5eadbbU;
+ gt[2U] = (uint64_t)0x0002af8df483c27eU;
+ gt[3U] = (uint64_t)0x000332b375274732U;
+ gt[4U] = (uint64_t)0x00067875f0fd78b7U;
+ KRML_MAYBE_FOR4(i,
+ (uint32_t)0U,
+ (uint32_t)4U,
+ (uint32_t)1U,
+ uint64_t *os = bscalar1;
+ uint8_t *bj = scalar1 + i * (uint32_t)8U;
+ uint64_t u = load64_le(bj);
+ uint64_t r = u;
+ uint64_t x = r;
+ os[i] = x;);
+ KRML_MAYBE_FOR4(i,
+ (uint32_t)0U,
+ (uint32_t)4U,
+ (uint32_t)1U,
+ uint64_t *os = bscalar2;
+ uint8_t *bj = scalar2 + i * (uint32_t)8U;
+ uint64_t u = load64_le(bj);
+ uint64_t r = u;
+ uint64_t x = r;
+ os[i] = x;);
+ uint64_t table2[640U] = { 0U };
+ uint64_t tmp1[20U] = { 0U };
+ uint64_t *t0 = table2;
+ uint64_t *t1 = table2 + (uint32_t)20U;
+ Hacl_Impl_Ed25519_PointConstants_make_point_inf(t0);
+ memcpy(t1, q2, (uint32_t)20U * 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)20U;
+ Hacl_Impl_Ed25519_PointDouble_point_double(tmp1, t11);
+ memcpy(table2 + ((uint32_t)2U * i + (uint32_t)2U) * (uint32_t)20U,
+ tmp1,
+ (uint32_t)20U * sizeof(uint64_t));
+ uint64_t *t2 = table2 + ((uint32_t)2U * i + (uint32_t)2U) * (uint32_t)20U;
+ Hacl_Impl_Ed25519_PointAdd_point_add(tmp1, q2, t2);
+ memcpy(table2 + ((uint32_t)2U * i + (uint32_t)3U) * (uint32_t)20U,
+ tmp1,
+ (uint32_t)20U * sizeof(uint64_t)););
+ uint64_t tmp10[20U] = { 0U };
+ uint32_t i0 = (uint32_t)255U;
+ uint64_t bits_c = Hacl_Bignum_Lib_bn_get_bits_u64((uint32_t)4U, bscalar1, i0, (uint32_t)5U);
+ uint32_t bits_l32 = (uint32_t)bits_c;
+ const uint64_t
+ *a_bits_l = Hacl_Ed25519_PrecompTable_precomp_basepoint_table_w5 + bits_l32 * (uint32_t)20U;
+ memcpy(out, (uint64_t *)a_bits_l, (uint32_t)20U * sizeof(uint64_t));
+ uint32_t i1 = (uint32_t)255U;
+ uint64_t bits_c0 = Hacl_Bignum_Lib_bn_get_bits_u64((uint32_t)4U, bscalar2, i1, (uint32_t)5U);
+ uint32_t bits_l320 = (uint32_t)bits_c0;
+ const uint64_t *a_bits_l0 = table2 + bits_l320 * (uint32_t)20U;
+ memcpy(tmp10, (uint64_t *)a_bits_l0, (uint32_t)20U * sizeof(uint64_t));
+ Hacl_Impl_Ed25519_PointAdd_point_add(out, out, tmp10);
+ uint64_t tmp11[20U] = { 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,
+ Hacl_Impl_Ed25519_PointDouble_point_double(out, out););
+ 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, bscalar2, k, (uint32_t)5U);
+ uint32_t bits_l321 = (uint32_t)bits_l;
+ const uint64_t *a_bits_l1 = table2 + bits_l321 * (uint32_t)20U;
+ memcpy(tmp11, (uint64_t *)a_bits_l1, (uint32_t)20U * sizeof(uint64_t));
+ Hacl_Impl_Ed25519_PointAdd_point_add(out, out, tmp11);
+ 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, bscalar1, k0, (uint32_t)5U);
+ uint32_t bits_l322 = (uint32_t)bits_l0;
+ const uint64_t
+ *a_bits_l2 = Hacl_Ed25519_PrecompTable_precomp_basepoint_table_w5 + bits_l322 * (uint32_t)20U;
+ memcpy(tmp11, (uint64_t *)a_bits_l2, (uint32_t)20U * sizeof(uint64_t));
+ Hacl_Impl_Ed25519_PointAdd_point_add(out, out, tmp11);
+ }
+}
+
+static inline void
+point_negate_mul_double_g_vartime(
+ uint64_t *out,
+ uint8_t *scalar1,
+ uint8_t *scalar2,
+ uint64_t *q2)
+{
+ uint64_t q2_neg[20U] = { 0U };
+ Hacl_Impl_Ed25519_PointNegate_point_negate(q2, q2_neg);
+ point_mul_g_double_vartime(out, scalar1, scalar2, q2_neg);
+}
+
+static inline void
+store_56(uint8_t *out, uint64_t *b)
+{
+ uint64_t b0 = b[0U];
+ uint64_t b1 = b[1U];
+ uint64_t b2 = b[2U];
+ uint64_t b3 = b[3U];
+ uint64_t b4 = b[4U];
+ uint32_t b4_ = (uint32_t)b4;
+ uint8_t *b8 = out;
+ store64_le(b8, b0);
+ uint8_t *b80 = out + (uint32_t)7U;
+ store64_le(b80, b1);
+ uint8_t *b81 = out + (uint32_t)14U;
+ store64_le(b81, b2);
+ uint8_t *b82 = out + (uint32_t)21U;
+ store64_le(b82, b3);
+ store32_le(out + (uint32_t)28U, b4_);
+}
+
+static inline void
+load_64_bytes(uint64_t *out, uint8_t *b)
+{
+ uint8_t *b80 = b;
+ uint64_t u = load64_le(b80);
+ uint64_t z = u;
+ uint64_t b0 = z & (uint64_t)0xffffffffffffffU;
+ uint8_t *b81 = b + (uint32_t)7U;
+ uint64_t u0 = load64_le(b81);
+ uint64_t z0 = u0;
+ uint64_t b1 = z0 & (uint64_t)0xffffffffffffffU;
+ uint8_t *b82 = b + (uint32_t)14U;
+ uint64_t u1 = load64_le(b82);
+ uint64_t z1 = u1;
+ uint64_t b2 = z1 & (uint64_t)0xffffffffffffffU;
+ uint8_t *b83 = b + (uint32_t)21U;
+ uint64_t u2 = load64_le(b83);
+ uint64_t z2 = u2;
+ uint64_t b3 = z2 & (uint64_t)0xffffffffffffffU;
+ uint8_t *b84 = b + (uint32_t)28U;
+ uint64_t u3 = load64_le(b84);
+ uint64_t z3 = u3;
+ uint64_t b4 = z3 & (uint64_t)0xffffffffffffffU;
+ uint8_t *b85 = b + (uint32_t)35U;
+ uint64_t u4 = load64_le(b85);
+ uint64_t z4 = u4;
+ uint64_t b5 = z4 & (uint64_t)0xffffffffffffffU;
+ uint8_t *b86 = b + (uint32_t)42U;
+ uint64_t u5 = load64_le(b86);
+ uint64_t z5 = u5;
+ uint64_t b6 = z5 & (uint64_t)0xffffffffffffffU;
+ uint8_t *b87 = b + (uint32_t)49U;
+ uint64_t u6 = load64_le(b87);
+ uint64_t z6 = u6;
+ uint64_t b7 = z6 & (uint64_t)0xffffffffffffffU;
+ uint8_t *b8 = b + (uint32_t)56U;
+ uint64_t u7 = load64_le(b8);
+ uint64_t z7 = u7;
+ uint64_t b88 = z7 & (uint64_t)0xffffffffffffffU;
+ uint8_t b63 = b[63U];
+ uint64_t b9 = (uint64_t)b63;
+ out[0U] = b0;
+ out[1U] = b1;
+ out[2U] = b2;
+ out[3U] = b3;
+ out[4U] = b4;
+ out[5U] = b5;
+ out[6U] = b6;
+ out[7U] = b7;
+ out[8U] = b88;
+ out[9U] = b9;
+}
+
+static inline void
+load_32_bytes(uint64_t *out, uint8_t *b)
+{
+ uint8_t *b80 = b;
+ uint64_t u0 = load64_le(b80);
+ uint64_t z = u0;
+ uint64_t b0 = z & (uint64_t)0xffffffffffffffU;
+ uint8_t *b81 = b + (uint32_t)7U;
+ uint64_t u1 = load64_le(b81);
+ uint64_t z0 = u1;
+ uint64_t b1 = z0 & (uint64_t)0xffffffffffffffU;
+ uint8_t *b82 = b + (uint32_t)14U;
+ uint64_t u2 = load64_le(b82);
+ uint64_t z1 = u2;
+ uint64_t b2 = z1 & (uint64_t)0xffffffffffffffU;
+ uint8_t *b8 = b + (uint32_t)21U;
+ uint64_t u3 = load64_le(b8);
+ uint64_t z2 = u3;
+ uint64_t b3 = z2 & (uint64_t)0xffffffffffffffU;
+ uint32_t u = load32_le(b + (uint32_t)28U);
+ uint32_t b4 = u;
+ uint64_t b41 = (uint64_t)b4;
+ out[0U] = b0;
+ out[1U] = b1;
+ out[2U] = b2;
+ out[3U] = b3;
+ out[4U] = b41;
+}
+
+static inline void
+sha512_modq_pre(uint64_t *out, uint8_t *prefix, uint32_t len, uint8_t *input)
+{
+ uint64_t tmp[10U] = { 0U };
+ uint8_t hash[64U] = { 0U };
+ sha512_pre_msg(hash, prefix, len, input);
+ load_64_bytes(tmp, hash);
+ barrett_reduction(out, tmp);
+}
+
+static inline void
+sha512_modq_pre_pre2(
+ uint64_t *out,
+ uint8_t *prefix,
+ uint8_t *prefix2,
+ uint32_t len,
+ uint8_t *input)
+{
+ uint64_t tmp[10U] = { 0U };
+ uint8_t hash[64U] = { 0U };
+ sha512_pre_pre2_msg(hash, prefix, prefix2, len, input);
+ load_64_bytes(tmp, hash);
+ barrett_reduction(out, tmp);
+}
+
+static inline void
+point_mul_g_compress(uint8_t *out, uint8_t *s)
+{
+ uint64_t tmp[20U] = { 0U };
+ point_mul_g(tmp, s);
+ Hacl_Impl_Ed25519_PointCompress_point_compress(out, tmp);
+}
+
+static inline void
+secret_expand(uint8_t *expanded, uint8_t *secret)
+{
+ Hacl_Streaming_SHA2_hash_512(secret, (uint32_t)32U, expanded);
+ uint8_t *h_low = expanded;
+ uint8_t h_low0 = h_low[0U];
+ uint8_t h_low31 = h_low[31U];
+ h_low[0U] = h_low0 & (uint8_t)0xf8U;
+ h_low[31U] = (h_low31 & (uint8_t)127U) | (uint8_t)64U;
+}
+
+/********************************************************************************
+ Verified C library for EdDSA signing and verification on the edwards25519 curve.
+********************************************************************************/
+
+/**
+Compute the public key from the private key.
+
+ The outparam `public_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
+ The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
+*/
+void
+Hacl_Ed25519_secret_to_public(uint8_t *public_key, uint8_t *private_key)
+{
+ uint8_t expanded_secret[64U] = { 0U };
+ secret_expand(expanded_secret, private_key);
+ uint8_t *a = expanded_secret;
+ point_mul_g_compress(public_key, a);
+}
+
+/**
+Compute the expanded keys for an Ed25519 signature.
+
+ The outparam `expanded_keys` points to 96 bytes of valid memory, i.e., uint8_t[96].
+ The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
+
+ If one needs to sign several messages under the same private key, it is more efficient
+ to call `expand_keys` only once and `sign_expanded` multiple times, for each message.
+*/
+void
+Hacl_Ed25519_expand_keys(uint8_t *expanded_keys, uint8_t *private_key)
+{
+ uint8_t *public_key = expanded_keys;
+ uint8_t *s_prefix = expanded_keys + (uint32_t)32U;
+ uint8_t *s = expanded_keys + (uint32_t)32U;
+ secret_expand(s_prefix, private_key);
+ point_mul_g_compress(public_key, s);
+}
+
+/**
+Create an Ed25519 signature with the (precomputed) expanded keys.
+
+ The outparam `signature` points to 64 bytes of valid memory, i.e., uint8_t[64].
+ The argument `expanded_keys` points to 96 bytes of valid memory, i.e., uint8_t[96].
+ The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].
+
+ The argument `expanded_keys` is obtained through `expand_keys`.
+
+ If one needs to sign several messages under the same private key, it is more efficient
+ to call `expand_keys` only once and `sign_expanded` multiple times, for each message.
+*/
+void
+Hacl_Ed25519_sign_expanded(
+ uint8_t *signature,
+ uint8_t *expanded_keys,
+ uint32_t msg_len,
+ uint8_t *msg)
+{
+ uint8_t *rs = signature;
+ uint8_t *ss = signature + (uint32_t)32U;
+ uint64_t rq[5U] = { 0U };
+ uint64_t hq[5U] = { 0U };
+ uint8_t rb[32U] = { 0U };
+ uint8_t *public_key = expanded_keys;
+ uint8_t *s = expanded_keys + (uint32_t)32U;
+ uint8_t *prefix = expanded_keys + (uint32_t)64U;
+ sha512_modq_pre(rq, prefix, msg_len, msg);
+ store_56(rb, rq);
+ point_mul_g_compress(rs, rb);
+ sha512_modq_pre_pre2(hq, rs, public_key, msg_len, msg);
+ uint64_t aq[5U] = { 0U };
+ load_32_bytes(aq, s);
+ mul_modq(aq, hq, aq);
+ add_modq(aq, rq, aq);
+ store_56(ss, aq);
+}
+
+/**
+Create an Ed25519 signature.
+
+ The outparam `signature` 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 argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].
+
+ The function first calls `expand_keys` and then invokes `sign_expanded`.
+
+ If one needs to sign several messages under the same private key, it is more efficient
+ to call `expand_keys` only once and `sign_expanded` multiple times, for each message.
+*/
+void
+Hacl_Ed25519_sign(uint8_t *signature, uint8_t *private_key, uint32_t msg_len, uint8_t *msg)
+{
+ uint8_t expanded_keys[96U] = { 0U };
+ Hacl_Ed25519_expand_keys(expanded_keys, private_key);
+ Hacl_Ed25519_sign_expanded(signature, expanded_keys, msg_len, msg);
+}
+
+/**
+Verify an Ed25519 signature.
+
+ The function returns `true` if the signature is valid and `false` otherwise.
+
+ The argument `public_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
+ The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].
+ The argument `signature` points to 64 bytes of valid memory, i.e., uint8_t[64].
+*/
+bool
+Hacl_Ed25519_verify(uint8_t *public_key, uint32_t msg_len, uint8_t *msg, uint8_t *signature)
+{
+ uint64_t a_[20U] = { 0U };
+ bool b = Hacl_Impl_Ed25519_PointDecompress_point_decompress(a_, public_key);
+ if (b) {
+ uint64_t r_[20U] = { 0U };
+ uint8_t *rs = signature;
+ bool b_ = Hacl_Impl_Ed25519_PointDecompress_point_decompress(r_, rs);
+ if (b_) {
+ uint8_t hb[32U] = { 0U };
+ uint8_t *rs1 = signature;
+ uint8_t *sb = signature + (uint32_t)32U;
+ uint64_t tmp[5U] = { 0U };
+ load_32_bytes(tmp, sb);
+ bool b1 = gte_q(tmp);
+ bool b10 = b1;
+ if (b10) {
+ return false;
+ }
+ uint64_t tmp0[5U] = { 0U };
+ sha512_modq_pre_pre2(tmp0, rs1, public_key, msg_len, msg);
+ store_56(hb, tmp0);
+ uint64_t exp_d[20U] = { 0U };
+ point_negate_mul_double_g_vartime(exp_d, sb, hb, a_);
+ bool b2 = Hacl_Impl_Ed25519_PointEqual_point_equal(exp_d, r_);
+ return b2;
+ }
+ return false;
+ }
+ return false;
+}
diff --git a/security/nss/lib/freebl/verified/Hacl_Ed25519.h b/security/nss/lib/freebl/verified/Hacl_Ed25519.h
new file mode 100644
index 0000000000..7d6f87dff2
--- /dev/null
+++ b/security/nss/lib/freebl/verified/Hacl_Ed25519.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 __Hacl_Ed25519_H
+#define __Hacl_Ed25519_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_Streaming_Types.h"
+#include "Hacl_Krmllib.h"
+
+/********************************************************************************
+ Verified C library for EdDSA signing and verification on the edwards25519 curve.
+********************************************************************************/
+
+/**
+Compute the public key from the private key.
+
+ The outparam `public_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
+ The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
+*/
+void Hacl_Ed25519_secret_to_public(uint8_t *public_key, uint8_t *private_key);
+
+/**
+Compute the expanded keys for an Ed25519 signature.
+
+ The outparam `expanded_keys` points to 96 bytes of valid memory, i.e., uint8_t[96].
+ The argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
+
+ If one needs to sign several messages under the same private key, it is more efficient
+ to call `expand_keys` only once and `sign_expanded` multiple times, for each message.
+*/
+void Hacl_Ed25519_expand_keys(uint8_t *expanded_keys, uint8_t *private_key);
+
+/**
+Create an Ed25519 signature with the (precomputed) expanded keys.
+
+ The outparam `signature` points to 64 bytes of valid memory, i.e., uint8_t[64].
+ The argument `expanded_keys` points to 96 bytes of valid memory, i.e., uint8_t[96].
+ The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].
+
+ The argument `expanded_keys` is obtained through `expand_keys`.
+
+ If one needs to sign several messages under the same private key, it is more efficient
+ to call `expand_keys` only once and `sign_expanded` multiple times, for each message.
+*/
+void
+Hacl_Ed25519_sign_expanded(
+ uint8_t *signature,
+ uint8_t *expanded_keys,
+ uint32_t msg_len,
+ uint8_t *msg);
+
+/**
+Create an Ed25519 signature.
+
+ The outparam `signature` 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 argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].
+
+ The function first calls `expand_keys` and then invokes `sign_expanded`.
+
+ If one needs to sign several messages under the same private key, it is more efficient
+ to call `expand_keys` only once and `sign_expanded` multiple times, for each message.
+*/
+void
+Hacl_Ed25519_sign(uint8_t *signature, uint8_t *private_key, uint32_t msg_len, uint8_t *msg);
+
+/**
+Verify an Ed25519 signature.
+
+ The function returns `true` if the signature is valid and `false` otherwise.
+
+ The argument `public_key` points to 32 bytes of valid memory, i.e., uint8_t[32].
+ The argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].
+ The argument `signature` points to 64 bytes of valid memory, i.e., uint8_t[64].
+*/
+bool
+Hacl_Ed25519_verify(uint8_t *public_key, uint32_t msg_len, uint8_t *msg, uint8_t *signature);
+
+#if defined(__cplusplus)
+}
+#endif
+
+#define __Hacl_Ed25519_H_DEFINED
+#endif
diff --git a/security/nss/lib/freebl/verified/Hacl_Hash_SHA3.c b/security/nss/lib/freebl/verified/Hacl_Hash_SHA3.c
index 3cd1091267..8fb5a86dbb 100644
--- a/security/nss/lib/freebl/verified/Hacl_Hash_SHA3.c
+++ b/security/nss/lib/freebl/verified/Hacl_Hash_SHA3.c
@@ -105,10 +105,9 @@ Hacl_Hash_SHA3_update_last_sha3(
uint32_t len = block_len(a);
if (input_len == len) {
Hacl_Impl_SHA3_absorb_inner(len, input, s);
- uint8_t *uu____0 = input + input_len;
uint8_t lastBlock_[200U] = { 0U };
uint8_t *lastBlock = lastBlock_;
- memcpy(lastBlock, uu____0, (uint32_t)0U * sizeof(uint8_t));
+ memcpy(lastBlock, input + input_len, (uint32_t)0U * sizeof(uint8_t));
lastBlock[0U] = suffix;
Hacl_Impl_SHA3_loadState(len, lastBlock, s);
if (!((suffix & (uint8_t)0x80U) == (uint8_t)0U) && (uint32_t)0U == len - (uint32_t)1U) {
@@ -144,8 +143,7 @@ typedef struct hash_buf2_s {
Spec_Hash_Definitions_hash_alg
Hacl_Streaming_Keccak_get_alg(Hacl_Streaming_Keccak_state *s)
{
- Hacl_Streaming_Keccak_state scrut = *s;
- Hacl_Streaming_Keccak_hash_buf block_state = scrut.block_state;
+ Hacl_Streaming_Keccak_hash_buf block_state = (*s).block_state;
return block_state.fst;
}
@@ -706,6 +704,7 @@ Hacl_Impl_SHA3_keccak(
uint32_t outputByteLen,
uint8_t *output)
{
+ KRML_HOST_IGNORE(capacity);
uint32_t rateInBytes = rate / (uint32_t)8U;
uint64_t s[25U] = { 0U };
absorb(s, rateInBytes, inputByteLen, input, delimitedSuffix);
diff --git a/security/nss/lib/freebl/verified/internal/Hacl_Bignum25519_51.h b/security/nss/lib/freebl/verified/internal/Hacl_Bignum25519_51.h
index c3e86ca512..162dd66edf 100644
--- a/security/nss/lib/freebl/verified/internal/Hacl_Bignum25519_51.h
+++ b/security/nss/lib/freebl/verified/internal/Hacl_Bignum25519_51.h
@@ -84,6 +84,7 @@ Hacl_Impl_Curve25519_Field51_fmul(
uint64_t *f2,
FStar_UInt128_uint128 *uu___)
{
+ KRML_HOST_IGNORE(uu___);
uint64_t f10 = f1[0U];
uint64_t f11 = f1[1U];
uint64_t f12 = f1[2U];
@@ -166,6 +167,7 @@ Hacl_Impl_Curve25519_Field51_fmul2(
uint64_t *f2,
FStar_UInt128_uint128 *uu___)
{
+ KRML_HOST_IGNORE(uu___);
uint64_t f10 = f1[0U];
uint64_t f11 = f1[1U];
uint64_t f12 = f1[2U];
@@ -371,6 +373,7 @@ Hacl_Impl_Curve25519_Field51_fmul1(uint64_t *out, uint64_t *f1, uint64_t f2)
static inline void
Hacl_Impl_Curve25519_Field51_fsqr(uint64_t *out, uint64_t *f, FStar_UInt128_uint128 *uu___)
{
+ KRML_HOST_IGNORE(uu___);
uint64_t f0 = f[0U];
uint64_t f1 = f[1U];
uint64_t f2 = f[2U];
@@ -446,6 +449,7 @@ Hacl_Impl_Curve25519_Field51_fsqr(uint64_t *out, uint64_t *f, FStar_UInt128_uint
static inline void
Hacl_Impl_Curve25519_Field51_fsqr2(uint64_t *out, uint64_t *f, FStar_UInt128_uint128 *uu___)
{
+ KRML_HOST_IGNORE(uu___);
uint64_t f10 = f[0U];
uint64_t f11 = f[1U];
uint64_t f12 = f[2U];
diff --git a/security/nss/lib/freebl/verified/internal/Hacl_Ed25519.h b/security/nss/lib/freebl/verified/internal/Hacl_Ed25519.h
new file mode 100644
index 0000000000..ad36672b92
--- /dev/null
+++ b/security/nss/lib/freebl/verified/internal/Hacl_Ed25519.h
@@ -0,0 +1,73 @@
+/* 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_Ed25519_H
+#define __internal_Hacl_Ed25519_H
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
+#include <string.h>
+#include "krml/internal/types.h"
+#include "krml/lowstar_endianness.h"
+#include "krml/internal/target.h"
+
+#include "internal/Hacl_Krmllib.h"
+#include "internal/Hacl_Ed25519_PrecompTable.h"
+#include "internal/Hacl_Curve25519_51.h"
+#include "internal/Hacl_Bignum_Base.h"
+#include "internal/Hacl_Bignum25519_51.h"
+#include "../Hacl_Ed25519.h"
+
+void Hacl_Bignum25519_reduce_513(uint64_t *a);
+
+void Hacl_Bignum25519_inverse(uint64_t *out, uint64_t *a);
+
+void Hacl_Bignum25519_load_51(uint64_t *output, uint8_t *input);
+
+void Hacl_Bignum25519_store_51(uint8_t *output, uint64_t *input);
+
+void Hacl_Impl_Ed25519_PointDouble_point_double(uint64_t *out, uint64_t *p);
+
+void Hacl_Impl_Ed25519_PointAdd_point_add(uint64_t *out, uint64_t *p, uint64_t *q);
+
+void Hacl_Impl_Ed25519_PointConstants_make_point_inf(uint64_t *b);
+
+bool Hacl_Impl_Ed25519_PointDecompress_point_decompress(uint64_t *out, uint8_t *s);
+
+void Hacl_Impl_Ed25519_PointCompress_point_compress(uint8_t *z, uint64_t *p);
+
+bool Hacl_Impl_Ed25519_PointEqual_point_equal(uint64_t *p, uint64_t *q);
+
+void Hacl_Impl_Ed25519_PointNegate_point_negate(uint64_t *p, uint64_t *out);
+
+void Hacl_Impl_Ed25519_Ladder_point_mul(uint64_t *out, uint8_t *scalar, uint64_t *q);
+
+#if defined(__cplusplus)
+}
+#endif
+
+#define __internal_Hacl_Ed25519_H_DEFINED
+#endif
diff --git a/security/nss/lib/freebl/verified/internal/Hacl_Ed25519_PrecompTable.h b/security/nss/lib/freebl/verified/internal/Hacl_Ed25519_PrecompTable.h
new file mode 100644
index 0000000000..fe852f31a9
--- /dev/null
+++ b/security/nss/lib/freebl/verified/internal/Hacl_Ed25519_PrecompTable.h
@@ -0,0 +1,687 @@
+/* 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_Ed25519_PrecompTable_H
+#define __internal_Hacl_Ed25519_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_Ed25519_PrecompTable_precomp_basepoint_table_w4[320U] = {
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)1U,
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)1U, (uint64_t)0U,
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U,
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)1738742601995546U, (uint64_t)1146398526822698U,
+ (uint64_t)2070867633025821U, (uint64_t)562264141797630U, (uint64_t)587772402128613U,
+ (uint64_t)1801439850948184U, (uint64_t)1351079888211148U, (uint64_t)450359962737049U,
+ (uint64_t)900719925474099U, (uint64_t)1801439850948198U, (uint64_t)1U, (uint64_t)0U,
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)1841354044333475U,
+ (uint64_t)16398895984059U, (uint64_t)755974180946558U, (uint64_t)900171276175154U,
+ (uint64_t)1821297809914039U, (uint64_t)1661154287933054U, (uint64_t)284530020860578U,
+ (uint64_t)1390261174866914U, (uint64_t)1524110943907984U, (uint64_t)1045603498418422U,
+ (uint64_t)928651508580478U, (uint64_t)1383326941296346U, (uint64_t)961937908925785U,
+ (uint64_t)80455759693706U, (uint64_t)904734540352947U, (uint64_t)1507481815385608U,
+ (uint64_t)2223447444246085U, (uint64_t)1083941587175919U, (uint64_t)2059929906842505U,
+ (uint64_t)1581435440146976U, (uint64_t)782730187692425U, (uint64_t)9928394897574U,
+ (uint64_t)1539449519985236U, (uint64_t)1923587931078510U, (uint64_t)552919286076056U,
+ (uint64_t)376925408065760U, (uint64_t)447320488831784U, (uint64_t)1362918338468019U,
+ (uint64_t)1470031896696846U, (uint64_t)2189796996539902U, (uint64_t)1337552949959847U,
+ (uint64_t)1762287177775726U, (uint64_t)237994495816815U, (uint64_t)1277840395970544U,
+ (uint64_t)543972849007241U, (uint64_t)1224692671618814U, (uint64_t)162359533289271U,
+ (uint64_t)282240927125249U, (uint64_t)586909166382289U, (uint64_t)17726488197838U,
+ (uint64_t)377014554985659U, (uint64_t)1433835303052512U, (uint64_t)702061469493692U,
+ (uint64_t)1142253108318154U, (uint64_t)318297794307551U, (uint64_t)954362646308543U,
+ (uint64_t)517363881452320U, (uint64_t)1868013482130416U, (uint64_t)262562472373260U,
+ (uint64_t)902232853249919U, (uint64_t)2107343057055746U, (uint64_t)462368348619024U,
+ (uint64_t)1893758677092974U, (uint64_t)2177729767846389U, (uint64_t)2168532543559143U,
+ (uint64_t)443867094639821U, (uint64_t)730169342581022U, (uint64_t)1564589016879755U,
+ (uint64_t)51218195700649U, (uint64_t)76684578423745U, (uint64_t)560266272480743U,
+ (uint64_t)922517457707697U, (uint64_t)2066645939860874U, (uint64_t)1318277348414638U,
+ (uint64_t)1576726809084003U, (uint64_t)1817337608563665U, (uint64_t)1874240939237666U,
+ (uint64_t)754733726333910U, (uint64_t)97085310406474U, (uint64_t)751148364309235U,
+ (uint64_t)1622159695715187U, (uint64_t)1444098819684916U, (uint64_t)130920805558089U,
+ (uint64_t)1260449179085308U, (uint64_t)1860021740768461U, (uint64_t)110052860348509U,
+ (uint64_t)193830891643810U, (uint64_t)164148413933881U, (uint64_t)180017794795332U,
+ (uint64_t)1523506525254651U, (uint64_t)465981629225956U, (uint64_t)559733514964572U,
+ (uint64_t)1279624874416974U, (uint64_t)2026642326892306U, (uint64_t)1425156829982409U,
+ (uint64_t)2160936383793147U, (uint64_t)1061870624975247U, (uint64_t)2023497043036941U,
+ (uint64_t)117942212883190U, (uint64_t)490339622800774U, (uint64_t)1729931303146295U,
+ (uint64_t)422305932971074U, (uint64_t)529103152793096U, (uint64_t)1211973233775992U,
+ (uint64_t)721364955929681U, (uint64_t)1497674430438813U, (uint64_t)342545521275073U,
+ (uint64_t)2102107575279372U, (uint64_t)2108462244669966U, (uint64_t)1382582406064082U,
+ (uint64_t)2206396818383323U, (uint64_t)2109093268641147U, (uint64_t)10809845110983U,
+ (uint64_t)1605176920880099U, (uint64_t)744640650753946U, (uint64_t)1712758897518129U,
+ (uint64_t)373410811281809U, (uint64_t)648838265800209U, (uint64_t)813058095530999U,
+ (uint64_t)513987632620169U, (uint64_t)465516160703329U, (uint64_t)2136322186126330U,
+ (uint64_t)1979645899422932U, (uint64_t)1197131006470786U, (uint64_t)1467836664863979U,
+ (uint64_t)1340751381374628U, (uint64_t)1810066212667962U, (uint64_t)1009933588225499U,
+ (uint64_t)1106129188080873U, (uint64_t)1388980405213901U, (uint64_t)533719246598044U,
+ (uint64_t)1169435803073277U, (uint64_t)198920999285821U, (uint64_t)487492330629854U,
+ (uint64_t)1807093008537778U, (uint64_t)1540899012923865U, (uint64_t)2075080271659867U,
+ (uint64_t)1527990806921523U, (uint64_t)1323728742908002U, (uint64_t)1568595959608205U,
+ (uint64_t)1388032187497212U, (uint64_t)2026968840050568U, (uint64_t)1396591153295755U,
+ (uint64_t)820416950170901U, (uint64_t)520060313205582U, (uint64_t)2016404325094901U,
+ (uint64_t)1584709677868520U, (uint64_t)272161374469956U, (uint64_t)1567188603996816U,
+ (uint64_t)1986160530078221U, (uint64_t)553930264324589U, (uint64_t)1058426729027503U,
+ (uint64_t)8762762886675U, (uint64_t)2216098143382988U, (uint64_t)1835145266889223U,
+ (uint64_t)1712936431558441U, (uint64_t)1017009937844974U, (uint64_t)585361667812740U,
+ (uint64_t)2114711541628181U, (uint64_t)2238729632971439U, (uint64_t)121257546253072U,
+ (uint64_t)847154149018345U, (uint64_t)211972965476684U, (uint64_t)287499084460129U,
+ (uint64_t)2098247259180197U, (uint64_t)839070411583329U, (uint64_t)339551619574372U,
+ (uint64_t)1432951287640743U, (uint64_t)526481249498942U, (uint64_t)931991661905195U,
+ (uint64_t)1884279965674487U, (uint64_t)200486405604411U, (uint64_t)364173020594788U,
+ (uint64_t)518034455936955U, (uint64_t)1085564703965501U, (uint64_t)16030410467927U,
+ (uint64_t)604865933167613U, (uint64_t)1695298441093964U, (uint64_t)498856548116159U,
+ (uint64_t)2193030062787034U, (uint64_t)1706339802964179U, (uint64_t)1721199073493888U,
+ (uint64_t)820740951039755U, (uint64_t)1216053436896834U, (uint64_t)23954895815139U,
+ (uint64_t)1662515208920491U, (uint64_t)1705443427511899U, (uint64_t)1957928899570365U,
+ (uint64_t)1189636258255725U, (uint64_t)1795695471103809U, (uint64_t)1691191297654118U,
+ (uint64_t)282402585374360U, (uint64_t)460405330264832U, (uint64_t)63765529445733U,
+ (uint64_t)469763447404473U, (uint64_t)733607089694996U, (uint64_t)685410420186959U,
+ (uint64_t)1096682630419738U, (uint64_t)1162548510542362U, (uint64_t)1020949526456676U,
+ (uint64_t)1211660396870573U, (uint64_t)613126398222696U, (uint64_t)1117829165843251U,
+ (uint64_t)742432540886650U, (uint64_t)1483755088010658U, (uint64_t)942392007134474U,
+ (uint64_t)1447834130944107U, (uint64_t)489368274863410U, (uint64_t)23192985544898U,
+ (uint64_t)648442406146160U, (uint64_t)785438843373876U, (uint64_t)249464684645238U,
+ (uint64_t)170494608205618U, (uint64_t)335112827260550U, (uint64_t)1462050123162735U,
+ (uint64_t)1084803668439016U, (uint64_t)853459233600325U, (uint64_t)215777728187495U,
+ (uint64_t)1965759433526974U, (uint64_t)1349482894446537U, (uint64_t)694163317612871U,
+ (uint64_t)860536766165036U, (uint64_t)1178788094084321U, (uint64_t)1652739626626996U,
+ (uint64_t)2115723946388185U, (uint64_t)1577204379094664U, (uint64_t)1083882859023240U,
+ (uint64_t)1768759143381635U, (uint64_t)1737180992507258U, (uint64_t)246054513922239U,
+ (uint64_t)577253134087234U, (uint64_t)356340280578042U, (uint64_t)1638917769925142U,
+ (uint64_t)223550348130103U, (uint64_t)470592666638765U, (uint64_t)22663573966996U,
+ (uint64_t)596552461152400U, (uint64_t)364143537069499U, (uint64_t)3942119457699U,
+ (uint64_t)107951982889287U, (uint64_t)1843471406713209U, (uint64_t)1625773041610986U,
+ (uint64_t)1466141092501702U, (uint64_t)1043024095021271U, (uint64_t)310429964047508U,
+ (uint64_t)98559121500372U, (uint64_t)152746933782868U, (uint64_t)259407205078261U,
+ (uint64_t)828123093322585U, (uint64_t)1576847274280091U, (uint64_t)1170871375757302U,
+ (uint64_t)1588856194642775U, (uint64_t)984767822341977U, (uint64_t)1141497997993760U,
+ (uint64_t)809325345150796U, (uint64_t)1879837728202511U, (uint64_t)201340910657893U,
+ (uint64_t)1079157558888483U, (uint64_t)1052373448588065U, (uint64_t)1732036202501778U,
+ (uint64_t)2105292670328445U, (uint64_t)679751387312402U, (uint64_t)1679682144926229U,
+ (uint64_t)1695823455818780U, (uint64_t)498852317075849U, (uint64_t)1786555067788433U,
+ (uint64_t)1670727545779425U, (uint64_t)117945875433544U, (uint64_t)407939139781844U,
+ (uint64_t)854632120023778U, (uint64_t)1413383148360437U, (uint64_t)286030901733673U,
+ (uint64_t)1207361858071196U, (uint64_t)461340408181417U, (uint64_t)1096919590360164U,
+ (uint64_t)1837594897475685U, (uint64_t)533755561544165U, (uint64_t)1638688042247712U,
+ (uint64_t)1431653684793005U, (uint64_t)1036458538873559U, (uint64_t)390822120341779U,
+ (uint64_t)1920929837111618U, (uint64_t)543426740024168U, (uint64_t)645751357799929U,
+ (uint64_t)2245025632994463U, (uint64_t)1550778638076452U, (uint64_t)223738153459949U,
+ (uint64_t)1337209385492033U, (uint64_t)1276967236456531U, (uint64_t)1463815821063071U,
+ (uint64_t)2070620870191473U, (uint64_t)1199170709413753U, (uint64_t)273230877394166U,
+ (uint64_t)1873264887608046U, (uint64_t)890877152910775U
+ };
+
+static const uint64_t
+ Hacl_Ed25519_PrecompTable_precomp_g_pow2_64_table_w4[320U] = {
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)1U,
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)1U, (uint64_t)0U,
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U,
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)13559344787725U, (uint64_t)2051621493703448U,
+ (uint64_t)1947659315640708U, (uint64_t)626856790370168U, (uint64_t)1592804284034836U,
+ (uint64_t)1781728767459187U, (uint64_t)278818420518009U, (uint64_t)2038030359908351U,
+ (uint64_t)910625973862690U, (uint64_t)471887343142239U, (uint64_t)1298543306606048U,
+ (uint64_t)794147365642417U, (uint64_t)129968992326749U, (uint64_t)523140861678572U,
+ (uint64_t)1166419653909231U, (uint64_t)2009637196928390U, (uint64_t)1288020222395193U,
+ (uint64_t)1007046974985829U, (uint64_t)208981102651386U, (uint64_t)2074009315253380U,
+ (uint64_t)1564056062071967U, (uint64_t)276822668750618U, (uint64_t)206621292512572U,
+ (uint64_t)470304361809269U, (uint64_t)895215438398493U, (uint64_t)1527859053868686U,
+ (uint64_t)1624967223409369U, (uint64_t)811821865979736U, (uint64_t)350450534838340U,
+ (uint64_t)219143807921807U, (uint64_t)507994540371254U, (uint64_t)986513794574720U,
+ (uint64_t)1142661369967121U, (uint64_t)621278293399257U, (uint64_t)556189161519781U,
+ (uint64_t)351964007865066U, (uint64_t)2011573453777822U, (uint64_t)1367125527151537U,
+ (uint64_t)1691316722438196U, (uint64_t)731328817345164U, (uint64_t)1284781192709232U,
+ (uint64_t)478439299539269U, (uint64_t)204842178076429U, (uint64_t)2085125369913651U,
+ (uint64_t)1980773492792985U, (uint64_t)1480264409524940U, (uint64_t)688389585376233U,
+ (uint64_t)612962643526972U, (uint64_t)165595382536676U, (uint64_t)1850300069212263U,
+ (uint64_t)1176357203491551U, (uint64_t)1880164984292321U, (uint64_t)10786153104736U,
+ (uint64_t)1242293560510203U, (uint64_t)1358399951884084U, (uint64_t)1901358796610357U,
+ (uint64_t)1385092558795806U, (uint64_t)1734893785311348U, (uint64_t)2046201851951191U,
+ (uint64_t)1233811309557352U, (uint64_t)1531160168656129U, (uint64_t)1543287181303358U,
+ (uint64_t)516121446374119U, (uint64_t)723422668089935U, (uint64_t)1228176774959679U,
+ (uint64_t)1598014722726267U, (uint64_t)1630810326658412U, (uint64_t)1343833067463760U,
+ (uint64_t)1024397964362099U, (uint64_t)1157142161346781U, (uint64_t)56422174971792U,
+ (uint64_t)544901687297092U, (uint64_t)1291559028869009U, (uint64_t)1336918672345120U,
+ (uint64_t)1390874603281353U, (uint64_t)1127199512010904U, (uint64_t)992644979940964U,
+ (uint64_t)1035213479783573U, (uint64_t)36043651196100U, (uint64_t)1220961519321221U,
+ (uint64_t)1348190007756977U, (uint64_t)579420200329088U, (uint64_t)1703819961008985U,
+ (uint64_t)1993919213460047U, (uint64_t)2225080008232251U, (uint64_t)392785893702372U,
+ (uint64_t)464312521482632U, (uint64_t)1224525362116057U, (uint64_t)810394248933036U,
+ (uint64_t)932513521649107U, (uint64_t)592314953488703U, (uint64_t)586334603791548U,
+ (uint64_t)1310888126096549U, (uint64_t)650842674074281U, (uint64_t)1596447001791059U,
+ (uint64_t)2086767406328284U, (uint64_t)1866377645879940U, (uint64_t)1721604362642743U,
+ (uint64_t)738502322566890U, (uint64_t)1851901097729689U, (uint64_t)1158347571686914U,
+ (uint64_t)2023626733470827U, (uint64_t)329625404653699U, (uint64_t)563555875598551U,
+ (uint64_t)516554588079177U, (uint64_t)1134688306104598U, (uint64_t)186301198420809U,
+ (uint64_t)1339952213563300U, (uint64_t)643605614625891U, (uint64_t)1947505332718043U,
+ (uint64_t)1722071694852824U, (uint64_t)601679570440694U, (uint64_t)1821275721236351U,
+ (uint64_t)1808307842870389U, (uint64_t)1654165204015635U, (uint64_t)1457334100715245U,
+ (uint64_t)217784948678349U, (uint64_t)1820622417674817U, (uint64_t)1946121178444661U,
+ (uint64_t)597980757799332U, (uint64_t)1745271227710764U, (uint64_t)2010952890941980U,
+ (uint64_t)339811849696648U, (uint64_t)1066120666993872U, (uint64_t)261276166508990U,
+ (uint64_t)323098645774553U, (uint64_t)207454744271283U, (uint64_t)941448672977675U,
+ (uint64_t)71890920544375U, (uint64_t)840849789313357U, (uint64_t)1223996070717926U,
+ (uint64_t)196832550853408U, (uint64_t)115986818309231U, (uint64_t)1586171527267675U,
+ (uint64_t)1666169080973450U, (uint64_t)1456454731176365U, (uint64_t)44467854369003U,
+ (uint64_t)2149656190691480U, (uint64_t)283446383597589U, (uint64_t)2040542647729974U,
+ (uint64_t)305705593840224U, (uint64_t)475315822269791U, (uint64_t)648133452550632U,
+ (uint64_t)169218658835720U, (uint64_t)24960052338251U, (uint64_t)938907951346766U,
+ (uint64_t)425970950490510U, (uint64_t)1037622011013183U, (uint64_t)1026882082708180U,
+ (uint64_t)1635699409504916U, (uint64_t)1644776942870488U, (uint64_t)2151820331175914U,
+ (uint64_t)824120674069819U, (uint64_t)835744976610113U, (uint64_t)1991271032313190U,
+ (uint64_t)96507354724855U, (uint64_t)400645405133260U, (uint64_t)343728076650825U,
+ (uint64_t)1151585441385566U, (uint64_t)1403339955333520U, (uint64_t)230186314139774U,
+ (uint64_t)1736248861506714U, (uint64_t)1010804378904572U, (uint64_t)1394932289845636U,
+ (uint64_t)1901351256960852U, (uint64_t)2187471430089807U, (uint64_t)1003853262342670U,
+ (uint64_t)1327743396767461U, (uint64_t)1465160415991740U, (uint64_t)366625359144534U,
+ (uint64_t)1534791405247604U, (uint64_t)1790905930250187U, (uint64_t)1255484115292738U,
+ (uint64_t)2223291365520443U, (uint64_t)210967717407408U, (uint64_t)26722916813442U,
+ (uint64_t)1919574361907910U, (uint64_t)468825088280256U, (uint64_t)2230011775946070U,
+ (uint64_t)1628365642214479U, (uint64_t)568871869234932U, (uint64_t)1066987968780488U,
+ (uint64_t)1692242903745558U, (uint64_t)1678903997328589U, (uint64_t)214262165888021U,
+ (uint64_t)1929686748607204U, (uint64_t)1790138967989670U, (uint64_t)1790261616022076U,
+ (uint64_t)1559824537553112U, (uint64_t)1230364591311358U, (uint64_t)147531939886346U,
+ (uint64_t)1528207085815487U, (uint64_t)477957922927292U, (uint64_t)285670243881618U,
+ (uint64_t)264430080123332U, (uint64_t)1163108160028611U, (uint64_t)373201522147371U,
+ (uint64_t)34903775270979U, (uint64_t)1750870048600662U, (uint64_t)1319328308741084U,
+ (uint64_t)1547548634278984U, (uint64_t)1691259592202927U, (uint64_t)2247758037259814U,
+ (uint64_t)329611399953677U, (uint64_t)1385555496268877U, (uint64_t)2242438354031066U,
+ (uint64_t)1329523854843632U, (uint64_t)399895373846055U, (uint64_t)678005703193452U,
+ (uint64_t)1496357700997771U, (uint64_t)71909969781942U, (uint64_t)1515391418612349U,
+ (uint64_t)470110837888178U, (uint64_t)1981307309417466U, (uint64_t)1259888737412276U,
+ (uint64_t)669991710228712U, (uint64_t)1048546834514303U, (uint64_t)1678323291295512U,
+ (uint64_t)2172033978088071U, (uint64_t)1529278455500556U, (uint64_t)901984601941894U,
+ (uint64_t)780867622403807U, (uint64_t)550105677282793U, (uint64_t)975860231176136U,
+ (uint64_t)525188281689178U, (uint64_t)49966114807992U, (uint64_t)1776449263836645U,
+ (uint64_t)267851776380338U, (uint64_t)2225969494054620U, (uint64_t)2016794225789822U,
+ (uint64_t)1186108678266608U, (uint64_t)1023083271408882U, (uint64_t)1119289418565906U,
+ (uint64_t)1248185897348801U, (uint64_t)1846081539082697U, (uint64_t)23756429626075U,
+ (uint64_t)1441999021105403U, (uint64_t)724497586552825U, (uint64_t)1287761623605379U,
+ (uint64_t)685303359654224U, (uint64_t)2217156930690570U, (uint64_t)163769288918347U,
+ (uint64_t)1098423278284094U, (uint64_t)1391470723006008U, (uint64_t)570700152353516U,
+ (uint64_t)744804507262556U, (uint64_t)2200464788609495U, (uint64_t)624141899161992U,
+ (uint64_t)2249570166275684U, (uint64_t)378706441983561U, (uint64_t)122486379999375U,
+ (uint64_t)430741162798924U, (uint64_t)113847463452574U, (uint64_t)266250457840685U,
+ (uint64_t)2120743625072743U, (uint64_t)222186221043927U, (uint64_t)1964290018305582U,
+ (uint64_t)1435278008132477U, (uint64_t)1670867456663734U, (uint64_t)2009989552599079U,
+ (uint64_t)1348024113448744U, (uint64_t)1158423886300455U, (uint64_t)1356467152691569U,
+ (uint64_t)306943042363674U, (uint64_t)926879628664255U, (uint64_t)1349295689598324U,
+ (uint64_t)725558330071205U, (uint64_t)536569987519948U, (uint64_t)116436990335366U,
+ (uint64_t)1551888573800376U, (uint64_t)2044698345945451U, (uint64_t)104279940291311U,
+ (uint64_t)251526570943220U, (uint64_t)754735828122925U, (uint64_t)33448073576361U,
+ (uint64_t)994605876754543U, (uint64_t)546007584022006U, (uint64_t)2217332798409487U,
+ (uint64_t)706477052561591U, (uint64_t)131174619428653U, (uint64_t)2148698284087243U,
+ (uint64_t)239290486205186U, (uint64_t)2161325796952184U, (uint64_t)1713452845607994U,
+ (uint64_t)1297861562938913U, (uint64_t)1779539876828514U, (uint64_t)1926559018603871U,
+ (uint64_t)296485747893968U, (uint64_t)1859208206640686U, (uint64_t)538513979002718U,
+ (uint64_t)103998826506137U, (uint64_t)2025375396538469U, (uint64_t)1370680785701206U,
+ (uint64_t)1698557311253840U, (uint64_t)1411096399076595U, (uint64_t)2132580530813677U,
+ (uint64_t)2071564345845035U, (uint64_t)498581428556735U, (uint64_t)1136010486691371U,
+ (uint64_t)1927619356993146U
+ };
+
+static const uint64_t
+ Hacl_Ed25519_PrecompTable_precomp_g_pow2_128_table_w4[320U] = {
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)1U,
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)1U, (uint64_t)0U,
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U,
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)557549315715710U, (uint64_t)196756086293855U,
+ (uint64_t)846062225082495U, (uint64_t)1865068224838092U, (uint64_t)991112090754908U,
+ (uint64_t)522916421512828U, (uint64_t)2098523346722375U, (uint64_t)1135633221747012U,
+ (uint64_t)858420432114866U, (uint64_t)186358544306082U, (uint64_t)1044420411868480U,
+ (uint64_t)2080052304349321U, (uint64_t)557301814716724U, (uint64_t)1305130257814057U,
+ (uint64_t)2126012765451197U, (uint64_t)1441004402875101U, (uint64_t)353948968859203U,
+ (uint64_t)470765987164835U, (uint64_t)1507675957683570U, (uint64_t)1086650358745097U,
+ (uint64_t)1911913434398388U, (uint64_t)66086091117182U, (uint64_t)1137511952425971U,
+ (uint64_t)36958263512141U, (uint64_t)2193310025325256U, (uint64_t)1085191426269045U,
+ (uint64_t)1232148267909446U, (uint64_t)1449894406170117U, (uint64_t)1241416717139557U,
+ (uint64_t)1940876999212868U, (uint64_t)829758415918121U, (uint64_t)309608450373449U,
+ (uint64_t)2228398547683851U, (uint64_t)1580623271960188U, (uint64_t)1675601502456740U,
+ (uint64_t)1360363115493548U, (uint64_t)1098397313096815U, (uint64_t)1809255384359797U,
+ (uint64_t)1458261916834384U, (uint64_t)210682545649705U, (uint64_t)1606836641068115U,
+ (uint64_t)1230478270405318U, (uint64_t)1843192771547802U, (uint64_t)1794596343564051U,
+ (uint64_t)229060710252162U, (uint64_t)2169742775467181U, (uint64_t)701467067318072U,
+ (uint64_t)696018499035555U, (uint64_t)521051885339807U, (uint64_t)158329567901874U,
+ (uint64_t)740426481832143U, (uint64_t)1369811177301441U, (uint64_t)503351589084015U,
+ (uint64_t)1781114827942261U, (uint64_t)1650493549693035U, (uint64_t)2174562418345156U,
+ (uint64_t)456517194809244U, (uint64_t)2052761522121179U, (uint64_t)2233342271123682U,
+ (uint64_t)1445872925177435U, (uint64_t)1131882576902813U, (uint64_t)220765848055241U,
+ (uint64_t)1280259961403769U, (uint64_t)1581497080160712U, (uint64_t)1477441080108824U,
+ (uint64_t)218428165202767U, (uint64_t)1970598141278907U, (uint64_t)643366736173069U,
+ (uint64_t)2167909426804014U, (uint64_t)834993711408259U, (uint64_t)1922437166463212U,
+ (uint64_t)1900036281472252U, (uint64_t)513794844386304U, (uint64_t)1297904164900114U,
+ (uint64_t)1147626295373268U, (uint64_t)1910101606251299U, (uint64_t)182933838633381U,
+ (uint64_t)806229530787362U, (uint64_t)155511666433200U, (uint64_t)290522463375462U,
+ (uint64_t)534373523491751U, (uint64_t)1302938814480515U, (uint64_t)1664979184120445U,
+ (uint64_t)304235649499423U, (uint64_t)339284524318609U, (uint64_t)1881717946973483U,
+ (uint64_t)1670802286833842U, (uint64_t)2223637120675737U, (uint64_t)135818919485814U,
+ (uint64_t)1144856572842792U, (uint64_t)2234981613434386U, (uint64_t)963917024969826U,
+ (uint64_t)402275378284993U, (uint64_t)141532417412170U, (uint64_t)921537468739387U,
+ (uint64_t)963905069722607U, (uint64_t)1405442890733358U, (uint64_t)1567763927164655U,
+ (uint64_t)1664776329195930U, (uint64_t)2095924165508507U, (uint64_t)994243110271379U,
+ (uint64_t)1243925610609353U, (uint64_t)1029845815569727U, (uint64_t)1001968867985629U,
+ (uint64_t)170368934002484U, (uint64_t)1100906131583801U, (uint64_t)1825190326449569U,
+ (uint64_t)1462285121182096U, (uint64_t)1545240767016377U, (uint64_t)797859025652273U,
+ (uint64_t)1062758326657530U, (uint64_t)1125600735118266U, (uint64_t)739325756774527U,
+ (uint64_t)1420144485966996U, (uint64_t)1915492743426702U, (uint64_t)752968196344993U,
+ (uint64_t)882156396938351U, (uint64_t)1909097048763227U, (uint64_t)849058590685611U,
+ (uint64_t)840754951388500U, (uint64_t)1832926948808323U, (uint64_t)2023317100075297U,
+ (uint64_t)322382745442827U, (uint64_t)1569741341737601U, (uint64_t)1678986113194987U,
+ (uint64_t)757598994581938U, (uint64_t)29678659580705U, (uint64_t)1239680935977986U,
+ (uint64_t)1509239427168474U, (uint64_t)1055981929287006U, (uint64_t)1894085471158693U,
+ (uint64_t)916486225488490U, (uint64_t)642168890366120U, (uint64_t)300453362620010U,
+ (uint64_t)1858797242721481U, (uint64_t)2077989823177130U, (uint64_t)510228455273334U,
+ (uint64_t)1473284798689270U, (uint64_t)5173934574301U, (uint64_t)765285232030050U,
+ (uint64_t)1007154707631065U, (uint64_t)1862128712885972U, (uint64_t)168873464821340U,
+ (uint64_t)1967853269759318U, (uint64_t)1489896018263031U, (uint64_t)592451806166369U,
+ (uint64_t)1242298565603883U, (uint64_t)1838918921339058U, (uint64_t)697532763910695U,
+ (uint64_t)294335466239059U, (uint64_t)135687058387449U, (uint64_t)2133734403874176U,
+ (uint64_t)2121911143127699U, (uint64_t)20222476737364U, (uint64_t)1200824626476747U,
+ (uint64_t)1397731736540791U, (uint64_t)702378430231418U, (uint64_t)59059527640068U,
+ (uint64_t)460992547183981U, (uint64_t)1016125857842765U, (uint64_t)1273530839608957U,
+ (uint64_t)96724128829301U, (uint64_t)1313433042425233U, (uint64_t)3543822857227U,
+ (uint64_t)761975685357118U, (uint64_t)110417360745248U, (uint64_t)1079634164577663U,
+ (uint64_t)2044574510020457U, (uint64_t)338709058603120U, (uint64_t)94541336042799U,
+ (uint64_t)127963233585039U, (uint64_t)94427896272258U, (uint64_t)1143501979342182U,
+ (uint64_t)1217958006212230U, (uint64_t)2153887831492134U, (uint64_t)1519219513255575U,
+ (uint64_t)251793195454181U, (uint64_t)392517349345200U, (uint64_t)1507033011868881U,
+ (uint64_t)2208494254670752U, (uint64_t)1364389582694359U, (uint64_t)2214069430728063U,
+ (uint64_t)1272814257105752U, (uint64_t)741450148906352U, (uint64_t)1105776675555685U,
+ (uint64_t)824447222014984U, (uint64_t)528745219306376U, (uint64_t)589427609121575U,
+ (uint64_t)1501786838809155U, (uint64_t)379067373073147U, (uint64_t)184909476589356U,
+ (uint64_t)1346887560616185U, (uint64_t)1932023742314082U, (uint64_t)1633302311869264U,
+ (uint64_t)1685314821133069U, (uint64_t)1836610282047884U, (uint64_t)1595571594397150U,
+ (uint64_t)615441688872198U, (uint64_t)1926435616702564U, (uint64_t)235632180396480U,
+ (uint64_t)1051918343571810U, (uint64_t)2150570051687050U, (uint64_t)879198845408738U,
+ (uint64_t)1443966275205464U, (uint64_t)481362545245088U, (uint64_t)512807443532642U,
+ (uint64_t)641147578283480U, (uint64_t)1594276116945596U, (uint64_t)1844812743300602U,
+ (uint64_t)2044559316019485U, (uint64_t)202620777969020U, (uint64_t)852992984136302U,
+ (uint64_t)1500869642692910U, (uint64_t)1085216217052457U, (uint64_t)1736294372259758U,
+ (uint64_t)2009666354486552U, (uint64_t)1262389020715248U, (uint64_t)1166527705256867U,
+ (uint64_t)1409917450806036U, (uint64_t)1705819160057637U, (uint64_t)1116901782584378U,
+ (uint64_t)1278460472285473U, (uint64_t)257879811360157U, (uint64_t)40314007176886U,
+ (uint64_t)701309846749639U, (uint64_t)1380457676672777U, (uint64_t)631519782380272U,
+ (uint64_t)1196339573466793U, (uint64_t)955537708940017U, (uint64_t)532725633381530U,
+ (uint64_t)641190593731833U, (uint64_t)7214357153807U, (uint64_t)481922072107983U,
+ (uint64_t)1634886189207352U, (uint64_t)1247659758261633U, (uint64_t)1655809614786430U,
+ (uint64_t)43105797900223U, (uint64_t)76205809912607U, (uint64_t)1936575107455823U,
+ (uint64_t)1107927314642236U, (uint64_t)2199986333469333U, (uint64_t)802974829322510U,
+ (uint64_t)718173128143482U, (uint64_t)539385184235615U, (uint64_t)2075693785611221U,
+ (uint64_t)953281147333690U, (uint64_t)1623571637172587U, (uint64_t)655274535022250U,
+ (uint64_t)1568078078819021U, (uint64_t)101142125049712U, (uint64_t)1488441673350881U,
+ (uint64_t)1457969561944515U, (uint64_t)1492622544287712U, (uint64_t)2041460689280803U,
+ (uint64_t)1961848091392887U, (uint64_t)461003520846938U, (uint64_t)934728060399807U,
+ (uint64_t)117723291519705U, (uint64_t)1027773762863526U, (uint64_t)56765304991567U,
+ (uint64_t)2184028379550479U, (uint64_t)1768767711894030U, (uint64_t)1304432068983172U,
+ (uint64_t)498080974452325U, (uint64_t)2134905654858163U, (uint64_t)1446137427202647U,
+ (uint64_t)551613831549590U, (uint64_t)680288767054205U, (uint64_t)1278113339140386U,
+ (uint64_t)378149431842614U, (uint64_t)80520494426960U, (uint64_t)2080985256348782U,
+ (uint64_t)673432591799820U, (uint64_t)739189463724560U, (uint64_t)1847191452197509U,
+ (uint64_t)527737312871602U, (uint64_t)477609358840073U, (uint64_t)1891633072677946U,
+ (uint64_t)1841456828278466U, (uint64_t)2242502936489002U, (uint64_t)524791829362709U,
+ (uint64_t)276648168514036U, (uint64_t)991706903257619U, (uint64_t)512580228297906U,
+ (uint64_t)1216855104975946U, (uint64_t)67030930303149U, (uint64_t)769593945208213U,
+ (uint64_t)2048873385103577U, (uint64_t)455635274123107U, (uint64_t)2077404927176696U,
+ (uint64_t)1803539634652306U, (uint64_t)1837579953843417U, (uint64_t)1564240068662828U,
+ (uint64_t)1964310918970435U, (uint64_t)832822906252492U, (uint64_t)1516044634195010U,
+ (uint64_t)770571447506889U, (uint64_t)602215152486818U, (uint64_t)1760828333136947U,
+ (uint64_t)730156776030376U
+ };
+
+static const uint64_t
+ Hacl_Ed25519_PrecompTable_precomp_g_pow2_192_table_w4[320U] = {
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)1U,
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)1U, (uint64_t)0U,
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U,
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)1129953239743101U, (uint64_t)1240339163956160U,
+ (uint64_t)61002583352401U, (uint64_t)2017604552196030U, (uint64_t)1576867829229863U,
+ (uint64_t)1508654942849389U, (uint64_t)270111619664077U, (uint64_t)1253097517254054U,
+ (uint64_t)721798270973250U, (uint64_t)161923365415298U, (uint64_t)828530877526011U,
+ (uint64_t)1494851059386763U, (uint64_t)662034171193976U, (uint64_t)1315349646974670U,
+ (uint64_t)2199229517308806U, (uint64_t)497078277852673U, (uint64_t)1310507715989956U,
+ (uint64_t)1881315714002105U, (uint64_t)2214039404983803U, (uint64_t)1331036420272667U,
+ (uint64_t)296286697520787U, (uint64_t)1179367922639127U, (uint64_t)25348441419697U,
+ (uint64_t)2200984961703188U, (uint64_t)150893128908291U, (uint64_t)1978614888570852U,
+ (uint64_t)1539657347172046U, (uint64_t)553810196523619U, (uint64_t)246017573977646U,
+ (uint64_t)1440448985385485U, (uint64_t)346049108099981U, (uint64_t)601166606218546U,
+ (uint64_t)855822004151713U, (uint64_t)1957521326383188U, (uint64_t)1114240380430887U,
+ (uint64_t)1349639675122048U, (uint64_t)957375954499040U, (uint64_t)111551795360136U,
+ (uint64_t)618586733648988U, (uint64_t)490708840688866U, (uint64_t)1267002049697314U,
+ (uint64_t)1130723224930028U, (uint64_t)215603029480828U, (uint64_t)1277138555414710U,
+ (uint64_t)1556750324971322U, (uint64_t)1407903521793741U, (uint64_t)1836836546590749U,
+ (uint64_t)576500297444199U, (uint64_t)2074707599091135U, (uint64_t)1826239864380012U,
+ (uint64_t)1935365705983312U, (uint64_t)239501825683682U, (uint64_t)1594236669034980U,
+ (uint64_t)1283078975055301U, (uint64_t)856745636255925U, (uint64_t)1342128647959981U,
+ (uint64_t)945216428379689U, (uint64_t)938746202496410U, (uint64_t)105775123333919U,
+ (uint64_t)1379852610117266U, (uint64_t)1770216827500275U, (uint64_t)1016017267535704U,
+ (uint64_t)1902885522469532U, (uint64_t)994184703730489U, (uint64_t)2227487538793763U,
+ (uint64_t)53155967096055U, (uint64_t)1264120808114350U, (uint64_t)1334928769376729U,
+ (uint64_t)393911808079997U, (uint64_t)826229239481845U, (uint64_t)1827903006733192U,
+ (uint64_t)1449283706008465U, (uint64_t)1258040415217849U, (uint64_t)1641484112868370U,
+ (uint64_t)1140150841968176U, (uint64_t)391113338021313U, (uint64_t)162138667815833U,
+ (uint64_t)742204396566060U, (uint64_t)110709233440557U, (uint64_t)90179377432917U,
+ (uint64_t)530511949644489U, (uint64_t)911568635552279U, (uint64_t)135869304780166U,
+ (uint64_t)617719999563692U, (uint64_t)1802525001631319U, (uint64_t)1836394639510490U,
+ (uint64_t)1862739456475085U, (uint64_t)1378284444664288U, (uint64_t)1617882529391756U,
+ (uint64_t)876124429891172U, (uint64_t)1147654641445091U, (uint64_t)1476943370400542U,
+ (uint64_t)688601222759067U, (uint64_t)2120281968990205U, (uint64_t)1387113236912611U,
+ (uint64_t)2125245820685788U, (uint64_t)1030674016350092U, (uint64_t)1594684598654247U,
+ (uint64_t)1165939511879820U, (uint64_t)271499323244173U, (uint64_t)546587254515484U,
+ (uint64_t)945603425742936U, (uint64_t)1242252568170226U, (uint64_t)561598728058142U,
+ (uint64_t)604827091794712U, (uint64_t)19869753585186U, (uint64_t)565367744708915U,
+ (uint64_t)536755754533603U, (uint64_t)1767258313589487U, (uint64_t)907952975936127U,
+ (uint64_t)292851652613937U, (uint64_t)163573546237963U, (uint64_t)837601408384564U,
+ (uint64_t)591996990118301U, (uint64_t)2126051747693057U, (uint64_t)182247548824566U,
+ (uint64_t)908369044122868U, (uint64_t)1335442699947273U, (uint64_t)2234292296528612U,
+ (uint64_t)689537529333034U, (uint64_t)2174778663790714U, (uint64_t)1011407643592667U,
+ (uint64_t)1856130618715473U, (uint64_t)1557437221651741U, (uint64_t)2250285407006102U,
+ (uint64_t)1412384213410827U, (uint64_t)1428042038612456U, (uint64_t)962709733973660U,
+ (uint64_t)313995703125919U, (uint64_t)1844969155869325U, (uint64_t)787716782673657U,
+ (uint64_t)622504542173478U, (uint64_t)930119043384654U, (uint64_t)2128870043952488U,
+ (uint64_t)537781531479523U, (uint64_t)1556666269904940U, (uint64_t)417333635741346U,
+ (uint64_t)1986743846438415U, (uint64_t)877620478041197U, (uint64_t)2205624582983829U,
+ (uint64_t)595260668884488U, (uint64_t)2025159350373157U, (uint64_t)2091659716088235U,
+ (uint64_t)1423634716596391U, (uint64_t)653686638634080U, (uint64_t)1972388399989956U,
+ (uint64_t)795575741798014U, (uint64_t)889240107997846U, (uint64_t)1446156876910732U,
+ (uint64_t)1028507012221776U, (uint64_t)1071697574586478U, (uint64_t)1689630411899691U,
+ (uint64_t)604092816502174U, (uint64_t)1909917373896122U, (uint64_t)1602544877643837U,
+ (uint64_t)1227177032923867U, (uint64_t)62684197535630U, (uint64_t)186146290753883U,
+ (uint64_t)414449055316766U, (uint64_t)1560555880866750U, (uint64_t)157579947096755U,
+ (uint64_t)230526795502384U, (uint64_t)1197673369665894U, (uint64_t)593779215869037U,
+ (uint64_t)214638834474097U, (uint64_t)1796344443484478U, (uint64_t)493550548257317U,
+ (uint64_t)1628442824033694U, (uint64_t)1410811655893495U, (uint64_t)1009361960995171U,
+ (uint64_t)604736219740352U, (uint64_t)392445928555351U, (uint64_t)1254295770295706U,
+ (uint64_t)1958074535046128U, (uint64_t)508699942241019U, (uint64_t)739405911261325U,
+ (uint64_t)1678760393882409U, (uint64_t)517763708545996U, (uint64_t)640040257898722U,
+ (uint64_t)384966810872913U, (uint64_t)407454748380128U, (uint64_t)152604679407451U,
+ (uint64_t)185102854927662U, (uint64_t)1448175503649595U, (uint64_t)100328519208674U,
+ (uint64_t)1153263667012830U, (uint64_t)1643926437586490U, (uint64_t)609632142834154U,
+ (uint64_t)980984004749261U, (uint64_t)855290732258779U, (uint64_t)2186022163021506U,
+ (uint64_t)1254052618626070U, (uint64_t)1850030517182611U, (uint64_t)162348933090207U,
+ (uint64_t)1948712273679932U, (uint64_t)1331832516262191U, (uint64_t)1219400369175863U,
+ (uint64_t)89689036937483U, (uint64_t)1554886057235815U, (uint64_t)1520047528432789U,
+ (uint64_t)81263957652811U, (uint64_t)146612464257008U, (uint64_t)2207945627164163U,
+ (uint64_t)919846660682546U, (uint64_t)1925694087906686U, (uint64_t)2102027292388012U,
+ (uint64_t)887992003198635U, (uint64_t)1817924871537027U, (uint64_t)746660005584342U,
+ (uint64_t)753757153275525U, (uint64_t)91394270908699U, (uint64_t)511837226544151U,
+ (uint64_t)736341543649373U, (uint64_t)1256371121466367U, (uint64_t)1977778299551813U,
+ (uint64_t)817915174462263U, (uint64_t)1602323381418035U, (uint64_t)190035164572930U,
+ (uint64_t)603796401391181U, (uint64_t)2152666873671669U, (uint64_t)1813900316324112U,
+ (uint64_t)1292622433358041U, (uint64_t)888439870199892U, (uint64_t)978918155071994U,
+ (uint64_t)534184417909805U, (uint64_t)466460084317313U, (uint64_t)1275223140288685U,
+ (uint64_t)786407043883517U, (uint64_t)1620520623925754U, (uint64_t)1753625021290269U,
+ (uint64_t)751937175104525U, (uint64_t)905301961820613U, (uint64_t)697059847245437U,
+ (uint64_t)584919033981144U, (uint64_t)1272165506533156U, (uint64_t)1532180021450866U,
+ (uint64_t)1901407354005301U, (uint64_t)1421319720492586U, (uint64_t)2179081609765456U,
+ (uint64_t)2193253156667632U, (uint64_t)1080248329608584U, (uint64_t)2158422436462066U,
+ (uint64_t)759167597017850U, (uint64_t)545759071151285U, (uint64_t)641600428493698U,
+ (uint64_t)943791424499848U, (uint64_t)469571542427864U, (uint64_t)951117845222467U,
+ (uint64_t)1780538594373407U, (uint64_t)614611122040309U, (uint64_t)1354826131886963U,
+ (uint64_t)221898131992340U, (uint64_t)1145699723916219U, (uint64_t)798735379961769U,
+ (uint64_t)1843560518208287U, (uint64_t)1424523160161545U, (uint64_t)205549016574779U,
+ (uint64_t)2239491587362749U, (uint64_t)1918363582399888U, (uint64_t)1292183072788455U,
+ (uint64_t)1783513123192567U, (uint64_t)1584027954317205U, (uint64_t)1890421443925740U,
+ (uint64_t)1718459319874929U, (uint64_t)1522091040748809U, (uint64_t)399467600667219U,
+ (uint64_t)1870973059066576U, (uint64_t)287514433150348U, (uint64_t)1397845311152885U,
+ (uint64_t)1880440629872863U, (uint64_t)709302939340341U, (uint64_t)1813571361109209U,
+ (uint64_t)86598795876860U, (uint64_t)1146964554310612U, (uint64_t)1590956584862432U,
+ (uint64_t)2097004628155559U, (uint64_t)656227622102390U, (uint64_t)1808500445541891U,
+ (uint64_t)958336726523135U, (uint64_t)2007604569465975U, (uint64_t)313504950390997U,
+ (uint64_t)1399686004953620U, (uint64_t)1759732788465234U, (uint64_t)1562539721055836U,
+ (uint64_t)1575722765016293U, (uint64_t)793318366641259U, (uint64_t)443876859384887U,
+ (uint64_t)547308921989704U, (uint64_t)636698687503328U, (uint64_t)2179175835287340U,
+ (uint64_t)498333551718258U, (uint64_t)932248760026176U, (uint64_t)1612395686304653U,
+ (uint64_t)2179774103745626U, (uint64_t)1359658123541018U, (uint64_t)171488501802442U,
+ (uint64_t)1625034951791350U, (uint64_t)520196922773633U, (uint64_t)1873787546341877U,
+ (uint64_t)303457823885368U
+ };
+
+static const uint64_t
+ Hacl_Ed25519_PrecompTable_precomp_basepoint_table_w5[640U] = {
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)1U,
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)1U, (uint64_t)0U,
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)0U,
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)1738742601995546U, (uint64_t)1146398526822698U,
+ (uint64_t)2070867633025821U, (uint64_t)562264141797630U, (uint64_t)587772402128613U,
+ (uint64_t)1801439850948184U, (uint64_t)1351079888211148U, (uint64_t)450359962737049U,
+ (uint64_t)900719925474099U, (uint64_t)1801439850948198U, (uint64_t)1U, (uint64_t)0U,
+ (uint64_t)0U, (uint64_t)0U, (uint64_t)0U, (uint64_t)1841354044333475U,
+ (uint64_t)16398895984059U, (uint64_t)755974180946558U, (uint64_t)900171276175154U,
+ (uint64_t)1821297809914039U, (uint64_t)1661154287933054U, (uint64_t)284530020860578U,
+ (uint64_t)1390261174866914U, (uint64_t)1524110943907984U, (uint64_t)1045603498418422U,
+ (uint64_t)928651508580478U, (uint64_t)1383326941296346U, (uint64_t)961937908925785U,
+ (uint64_t)80455759693706U, (uint64_t)904734540352947U, (uint64_t)1507481815385608U,
+ (uint64_t)2223447444246085U, (uint64_t)1083941587175919U, (uint64_t)2059929906842505U,
+ (uint64_t)1581435440146976U, (uint64_t)782730187692425U, (uint64_t)9928394897574U,
+ (uint64_t)1539449519985236U, (uint64_t)1923587931078510U, (uint64_t)552919286076056U,
+ (uint64_t)376925408065760U, (uint64_t)447320488831784U, (uint64_t)1362918338468019U,
+ (uint64_t)1470031896696846U, (uint64_t)2189796996539902U, (uint64_t)1337552949959847U,
+ (uint64_t)1762287177775726U, (uint64_t)237994495816815U, (uint64_t)1277840395970544U,
+ (uint64_t)543972849007241U, (uint64_t)1224692671618814U, (uint64_t)162359533289271U,
+ (uint64_t)282240927125249U, (uint64_t)586909166382289U, (uint64_t)17726488197838U,
+ (uint64_t)377014554985659U, (uint64_t)1433835303052512U, (uint64_t)702061469493692U,
+ (uint64_t)1142253108318154U, (uint64_t)318297794307551U, (uint64_t)954362646308543U,
+ (uint64_t)517363881452320U, (uint64_t)1868013482130416U, (uint64_t)262562472373260U,
+ (uint64_t)902232853249919U, (uint64_t)2107343057055746U, (uint64_t)462368348619024U,
+ (uint64_t)1893758677092974U, (uint64_t)2177729767846389U, (uint64_t)2168532543559143U,
+ (uint64_t)443867094639821U, (uint64_t)730169342581022U, (uint64_t)1564589016879755U,
+ (uint64_t)51218195700649U, (uint64_t)76684578423745U, (uint64_t)560266272480743U,
+ (uint64_t)922517457707697U, (uint64_t)2066645939860874U, (uint64_t)1318277348414638U,
+ (uint64_t)1576726809084003U, (uint64_t)1817337608563665U, (uint64_t)1874240939237666U,
+ (uint64_t)754733726333910U, (uint64_t)97085310406474U, (uint64_t)751148364309235U,
+ (uint64_t)1622159695715187U, (uint64_t)1444098819684916U, (uint64_t)130920805558089U,
+ (uint64_t)1260449179085308U, (uint64_t)1860021740768461U, (uint64_t)110052860348509U,
+ (uint64_t)193830891643810U, (uint64_t)164148413933881U, (uint64_t)180017794795332U,
+ (uint64_t)1523506525254651U, (uint64_t)465981629225956U, (uint64_t)559733514964572U,
+ (uint64_t)1279624874416974U, (uint64_t)2026642326892306U, (uint64_t)1425156829982409U,
+ (uint64_t)2160936383793147U, (uint64_t)1061870624975247U, (uint64_t)2023497043036941U,
+ (uint64_t)117942212883190U, (uint64_t)490339622800774U, (uint64_t)1729931303146295U,
+ (uint64_t)422305932971074U, (uint64_t)529103152793096U, (uint64_t)1211973233775992U,
+ (uint64_t)721364955929681U, (uint64_t)1497674430438813U, (uint64_t)342545521275073U,
+ (uint64_t)2102107575279372U, (uint64_t)2108462244669966U, (uint64_t)1382582406064082U,
+ (uint64_t)2206396818383323U, (uint64_t)2109093268641147U, (uint64_t)10809845110983U,
+ (uint64_t)1605176920880099U, (uint64_t)744640650753946U, (uint64_t)1712758897518129U,
+ (uint64_t)373410811281809U, (uint64_t)648838265800209U, (uint64_t)813058095530999U,
+ (uint64_t)513987632620169U, (uint64_t)465516160703329U, (uint64_t)2136322186126330U,
+ (uint64_t)1979645899422932U, (uint64_t)1197131006470786U, (uint64_t)1467836664863979U,
+ (uint64_t)1340751381374628U, (uint64_t)1810066212667962U, (uint64_t)1009933588225499U,
+ (uint64_t)1106129188080873U, (uint64_t)1388980405213901U, (uint64_t)533719246598044U,
+ (uint64_t)1169435803073277U, (uint64_t)198920999285821U, (uint64_t)487492330629854U,
+ (uint64_t)1807093008537778U, (uint64_t)1540899012923865U, (uint64_t)2075080271659867U,
+ (uint64_t)1527990806921523U, (uint64_t)1323728742908002U, (uint64_t)1568595959608205U,
+ (uint64_t)1388032187497212U, (uint64_t)2026968840050568U, (uint64_t)1396591153295755U,
+ (uint64_t)820416950170901U, (uint64_t)520060313205582U, (uint64_t)2016404325094901U,
+ (uint64_t)1584709677868520U, (uint64_t)272161374469956U, (uint64_t)1567188603996816U,
+ (uint64_t)1986160530078221U, (uint64_t)553930264324589U, (uint64_t)1058426729027503U,
+ (uint64_t)8762762886675U, (uint64_t)2216098143382988U, (uint64_t)1835145266889223U,
+ (uint64_t)1712936431558441U, (uint64_t)1017009937844974U, (uint64_t)585361667812740U,
+ (uint64_t)2114711541628181U, (uint64_t)2238729632971439U, (uint64_t)121257546253072U,
+ (uint64_t)847154149018345U, (uint64_t)211972965476684U, (uint64_t)287499084460129U,
+ (uint64_t)2098247259180197U, (uint64_t)839070411583329U, (uint64_t)339551619574372U,
+ (uint64_t)1432951287640743U, (uint64_t)526481249498942U, (uint64_t)931991661905195U,
+ (uint64_t)1884279965674487U, (uint64_t)200486405604411U, (uint64_t)364173020594788U,
+ (uint64_t)518034455936955U, (uint64_t)1085564703965501U, (uint64_t)16030410467927U,
+ (uint64_t)604865933167613U, (uint64_t)1695298441093964U, (uint64_t)498856548116159U,
+ (uint64_t)2193030062787034U, (uint64_t)1706339802964179U, (uint64_t)1721199073493888U,
+ (uint64_t)820740951039755U, (uint64_t)1216053436896834U, (uint64_t)23954895815139U,
+ (uint64_t)1662515208920491U, (uint64_t)1705443427511899U, (uint64_t)1957928899570365U,
+ (uint64_t)1189636258255725U, (uint64_t)1795695471103809U, (uint64_t)1691191297654118U,
+ (uint64_t)282402585374360U, (uint64_t)460405330264832U, (uint64_t)63765529445733U,
+ (uint64_t)469763447404473U, (uint64_t)733607089694996U, (uint64_t)685410420186959U,
+ (uint64_t)1096682630419738U, (uint64_t)1162548510542362U, (uint64_t)1020949526456676U,
+ (uint64_t)1211660396870573U, (uint64_t)613126398222696U, (uint64_t)1117829165843251U,
+ (uint64_t)742432540886650U, (uint64_t)1483755088010658U, (uint64_t)942392007134474U,
+ (uint64_t)1447834130944107U, (uint64_t)489368274863410U, (uint64_t)23192985544898U,
+ (uint64_t)648442406146160U, (uint64_t)785438843373876U, (uint64_t)249464684645238U,
+ (uint64_t)170494608205618U, (uint64_t)335112827260550U, (uint64_t)1462050123162735U,
+ (uint64_t)1084803668439016U, (uint64_t)853459233600325U, (uint64_t)215777728187495U,
+ (uint64_t)1965759433526974U, (uint64_t)1349482894446537U, (uint64_t)694163317612871U,
+ (uint64_t)860536766165036U, (uint64_t)1178788094084321U, (uint64_t)1652739626626996U,
+ (uint64_t)2115723946388185U, (uint64_t)1577204379094664U, (uint64_t)1083882859023240U,
+ (uint64_t)1768759143381635U, (uint64_t)1737180992507258U, (uint64_t)246054513922239U,
+ (uint64_t)577253134087234U, (uint64_t)356340280578042U, (uint64_t)1638917769925142U,
+ (uint64_t)223550348130103U, (uint64_t)470592666638765U, (uint64_t)22663573966996U,
+ (uint64_t)596552461152400U, (uint64_t)364143537069499U, (uint64_t)3942119457699U,
+ (uint64_t)107951982889287U, (uint64_t)1843471406713209U, (uint64_t)1625773041610986U,
+ (uint64_t)1466141092501702U, (uint64_t)1043024095021271U, (uint64_t)310429964047508U,
+ (uint64_t)98559121500372U, (uint64_t)152746933782868U, (uint64_t)259407205078261U,
+ (uint64_t)828123093322585U, (uint64_t)1576847274280091U, (uint64_t)1170871375757302U,
+ (uint64_t)1588856194642775U, (uint64_t)984767822341977U, (uint64_t)1141497997993760U,
+ (uint64_t)809325345150796U, (uint64_t)1879837728202511U, (uint64_t)201340910657893U,
+ (uint64_t)1079157558888483U, (uint64_t)1052373448588065U, (uint64_t)1732036202501778U,
+ (uint64_t)2105292670328445U, (uint64_t)679751387312402U, (uint64_t)1679682144926229U,
+ (uint64_t)1695823455818780U, (uint64_t)498852317075849U, (uint64_t)1786555067788433U,
+ (uint64_t)1670727545779425U, (uint64_t)117945875433544U, (uint64_t)407939139781844U,
+ (uint64_t)854632120023778U, (uint64_t)1413383148360437U, (uint64_t)286030901733673U,
+ (uint64_t)1207361858071196U, (uint64_t)461340408181417U, (uint64_t)1096919590360164U,
+ (uint64_t)1837594897475685U, (uint64_t)533755561544165U, (uint64_t)1638688042247712U,
+ (uint64_t)1431653684793005U, (uint64_t)1036458538873559U, (uint64_t)390822120341779U,
+ (uint64_t)1920929837111618U, (uint64_t)543426740024168U, (uint64_t)645751357799929U,
+ (uint64_t)2245025632994463U, (uint64_t)1550778638076452U, (uint64_t)223738153459949U,
+ (uint64_t)1337209385492033U, (uint64_t)1276967236456531U, (uint64_t)1463815821063071U,
+ (uint64_t)2070620870191473U, (uint64_t)1199170709413753U, (uint64_t)273230877394166U,
+ (uint64_t)1873264887608046U, (uint64_t)890877152910775U, (uint64_t)983226445635730U,
+ (uint64_t)44873798519521U, (uint64_t)697147127512130U, (uint64_t)961631038239304U,
+ (uint64_t)709966160696826U, (uint64_t)1706677689540366U, (uint64_t)502782733796035U,
+ (uint64_t)812545535346033U, (uint64_t)1693622521296452U, (uint64_t)1955813093002510U,
+ (uint64_t)1259937612881362U, (uint64_t)1873032503803559U, (uint64_t)1140330566016428U,
+ (uint64_t)1675726082440190U, (uint64_t)60029928909786U, (uint64_t)170335608866763U,
+ (uint64_t)766444312315022U, (uint64_t)2025049511434113U, (uint64_t)2200845622430647U,
+ (uint64_t)1201269851450408U, (uint64_t)590071752404907U, (uint64_t)1400995030286946U,
+ (uint64_t)2152637413853822U, (uint64_t)2108495473841983U, (uint64_t)3855406710349U,
+ (uint64_t)1726137673168580U, (uint64_t)51004317200100U, (uint64_t)1749082328586939U,
+ (uint64_t)1704088976144558U, (uint64_t)1977318954775118U, (uint64_t)2062602253162400U,
+ (uint64_t)948062503217479U, (uint64_t)361953965048030U, (uint64_t)1528264887238440U,
+ (uint64_t)62582552172290U, (uint64_t)2241602163389280U, (uint64_t)156385388121765U,
+ (uint64_t)2124100319761492U, (uint64_t)388928050571382U, (uint64_t)1556123596922727U,
+ (uint64_t)979310669812384U, (uint64_t)113043855206104U, (uint64_t)2023223924825469U,
+ (uint64_t)643651703263034U, (uint64_t)2234446903655540U, (uint64_t)1577241261424997U,
+ (uint64_t)860253174523845U, (uint64_t)1691026473082448U, (uint64_t)1091672764933872U,
+ (uint64_t)1957463109756365U, (uint64_t)530699502660193U, (uint64_t)349587141723569U,
+ (uint64_t)674661681919563U, (uint64_t)1633727303856240U, (uint64_t)708909037922144U,
+ (uint64_t)2160722508518119U, (uint64_t)1302188051602540U, (uint64_t)976114603845777U,
+ (uint64_t)120004758721939U, (uint64_t)1681630708873780U, (uint64_t)622274095069244U,
+ (uint64_t)1822346309016698U, (uint64_t)1100921177951904U, (uint64_t)2216952659181677U,
+ (uint64_t)1844020550362490U, (uint64_t)1976451368365774U, (uint64_t)1321101422068822U,
+ (uint64_t)1189859436282668U, (uint64_t)2008801879735257U, (uint64_t)2219413454333565U,
+ (uint64_t)424288774231098U, (uint64_t)359793146977912U, (uint64_t)270293357948703U,
+ (uint64_t)587226003677000U, (uint64_t)1482071926139945U, (uint64_t)1419630774650359U,
+ (uint64_t)1104739070570175U, (uint64_t)1662129023224130U, (uint64_t)1609203612533411U,
+ (uint64_t)1250932720691980U, (uint64_t)95215711818495U, (uint64_t)498746909028150U,
+ (uint64_t)158151296991874U, (uint64_t)1201379988527734U, (uint64_t)561599945143989U,
+ (uint64_t)2211577425617888U, (uint64_t)2166577612206324U, (uint64_t)1057590354233512U,
+ (uint64_t)1968123280416769U, (uint64_t)1316586165401313U, (uint64_t)762728164447634U,
+ (uint64_t)2045395244316047U, (uint64_t)1531796898725716U, (uint64_t)315385971670425U,
+ (uint64_t)1109421039396756U, (uint64_t)2183635256408562U, (uint64_t)1896751252659461U,
+ (uint64_t)840236037179080U, (uint64_t)796245792277211U, (uint64_t)508345890111193U,
+ (uint64_t)1275386465287222U, (uint64_t)513560822858784U, (uint64_t)1784735733120313U,
+ (uint64_t)1346467478899695U, (uint64_t)601125231208417U, (uint64_t)701076661112726U,
+ (uint64_t)1841998436455089U, (uint64_t)1156768600940434U, (uint64_t)1967853462343221U,
+ (uint64_t)2178318463061452U, (uint64_t)481885520752741U, (uint64_t)675262828640945U,
+ (uint64_t)1033539418596582U, (uint64_t)1743329872635846U, (uint64_t)159322641251283U,
+ (uint64_t)1573076470127113U, (uint64_t)954827619308195U, (uint64_t)778834750662635U,
+ (uint64_t)619912782122617U, (uint64_t)515681498488209U, (uint64_t)1675866144246843U,
+ (uint64_t)811716020969981U, (uint64_t)1125515272217398U, (uint64_t)1398917918287342U,
+ (uint64_t)1301680949183175U, (uint64_t)726474739583734U, (uint64_t)587246193475200U,
+ (uint64_t)1096581582611864U, (uint64_t)1469911826213486U, (uint64_t)1990099711206364U,
+ (uint64_t)1256496099816508U, (uint64_t)2019924615195672U, (uint64_t)1251232456707555U,
+ (uint64_t)2042971196009755U, (uint64_t)214061878479265U, (uint64_t)115385726395472U,
+ (uint64_t)1677875239524132U, (uint64_t)756888883383540U, (uint64_t)1153862117756233U,
+ (uint64_t)503391530851096U, (uint64_t)946070017477513U, (uint64_t)1878319040542579U,
+ (uint64_t)1101349418586920U, (uint64_t)793245696431613U, (uint64_t)397920495357645U,
+ (uint64_t)2174023872951112U, (uint64_t)1517867915189593U, (uint64_t)1829855041462995U,
+ (uint64_t)1046709983503619U, (uint64_t)424081940711857U, (uint64_t)2112438073094647U,
+ (uint64_t)1504338467349861U, (uint64_t)2244574127374532U, (uint64_t)2136937537441911U,
+ (uint64_t)1741150838990304U, (uint64_t)25894628400571U, (uint64_t)512213526781178U,
+ (uint64_t)1168384260796379U, (uint64_t)1424607682379833U, (uint64_t)938677789731564U,
+ (uint64_t)872882241891896U, (uint64_t)1713199397007700U, (uint64_t)1410496326218359U,
+ (uint64_t)854379752407031U, (uint64_t)465141611727634U, (uint64_t)315176937037857U,
+ (uint64_t)1020115054571233U, (uint64_t)1856290111077229U, (uint64_t)2028366269898204U,
+ (uint64_t)1432980880307543U, (uint64_t)469932710425448U, (uint64_t)581165267592247U,
+ (uint64_t)496399148156603U, (uint64_t)2063435226705903U, (uint64_t)2116841086237705U,
+ (uint64_t)498272567217048U, (uint64_t)1829438076967906U, (uint64_t)1573925801278491U,
+ (uint64_t)460763576329867U, (uint64_t)1705264723728225U, (uint64_t)999514866082412U,
+ (uint64_t)29635061779362U, (uint64_t)1884233592281020U, (uint64_t)1449755591461338U,
+ (uint64_t)42579292783222U, (uint64_t)1869504355369200U, (uint64_t)495506004805251U,
+ (uint64_t)264073104888427U, (uint64_t)2088880861028612U, (uint64_t)104646456386576U,
+ (uint64_t)1258445191399967U, (uint64_t)1348736801545799U, (uint64_t)2068276361286613U,
+ (uint64_t)884897216646374U, (uint64_t)922387476801376U, (uint64_t)1043886580402805U,
+ (uint64_t)1240883498470831U, (uint64_t)1601554651937110U, (uint64_t)804382935289482U,
+ (uint64_t)512379564477239U, (uint64_t)1466384519077032U, (uint64_t)1280698500238386U,
+ (uint64_t)211303836685749U, (uint64_t)2081725624793803U, (uint64_t)545247644516879U,
+ (uint64_t)215313359330384U, (uint64_t)286479751145614U, (uint64_t)2213650281751636U,
+ (uint64_t)2164927945999874U, (uint64_t)2072162991540882U, (uint64_t)1443769115444779U,
+ (uint64_t)1581473274363095U, (uint64_t)434633875922699U, (uint64_t)340456055781599U,
+ (uint64_t)373043091080189U, (uint64_t)839476566531776U, (uint64_t)1856706858509978U,
+ (uint64_t)931616224909153U, (uint64_t)1888181317414065U, (uint64_t)213654322650262U,
+ (uint64_t)1161078103416244U, (uint64_t)1822042328851513U, (uint64_t)915817709028812U,
+ (uint64_t)1828297056698188U, (uint64_t)1212017130909403U, (uint64_t)60258343247333U,
+ (uint64_t)342085800008230U, (uint64_t)930240559508270U, (uint64_t)1549884999174952U,
+ (uint64_t)809895264249462U, (uint64_t)184726257947682U, (uint64_t)1157065433504828U,
+ (uint64_t)1209999630381477U, (uint64_t)999920399374391U, (uint64_t)1714770150788163U,
+ (uint64_t)2026130985413228U, (uint64_t)506776632883140U, (uint64_t)1349042668246528U,
+ (uint64_t)1937232292976967U, (uint64_t)942302637530730U, (uint64_t)160211904766226U,
+ (uint64_t)1042724500438571U, (uint64_t)212454865139142U, (uint64_t)244104425172642U,
+ (uint64_t)1376990622387496U, (uint64_t)76126752421227U, (uint64_t)1027540886376422U,
+ (uint64_t)1912210655133026U, (uint64_t)13410411589575U, (uint64_t)1475856708587773U,
+ (uint64_t)615563352691682U, (uint64_t)1446629324872644U, (uint64_t)1683670301784014U,
+ (uint64_t)1049873327197127U, (uint64_t)1826401704084838U, (uint64_t)2032577048760775U,
+ (uint64_t)1922203607878853U, (uint64_t)836708788764806U, (uint64_t)2193084654695012U,
+ (uint64_t)1342923183256659U, (uint64_t)849356986294271U, (uint64_t)1228863973965618U,
+ (uint64_t)94886161081867U, (uint64_t)1423288430204892U, (uint64_t)2016167528707016U,
+ (uint64_t)1633187660972877U, (uint64_t)1550621242301752U, (uint64_t)340630244512994U,
+ (uint64_t)2103577710806901U, (uint64_t)221625016538931U, (uint64_t)421544147350960U,
+ (uint64_t)580428704555156U, (uint64_t)1479831381265617U, (uint64_t)518057926544698U,
+ (uint64_t)955027348790630U, (uint64_t)1326749172561598U, (uint64_t)1118304625755967U,
+ (uint64_t)1994005916095176U, (uint64_t)1799757332780663U, (uint64_t)751343129396941U,
+ (uint64_t)1468672898746144U, (uint64_t)1451689964451386U, (uint64_t)755070293921171U,
+ (uint64_t)904857405877052U, (uint64_t)1276087530766984U, (uint64_t)403986562858511U,
+ (uint64_t)1530661255035337U, (uint64_t)1644972908910502U, (uint64_t)1370170080438957U,
+ (uint64_t)139839536695744U, (uint64_t)909930462436512U, (uint64_t)1899999215356933U,
+ (uint64_t)635992381064566U, (uint64_t)788740975837654U, (uint64_t)224241231493695U,
+ (uint64_t)1267090030199302U, (uint64_t)998908061660139U, (uint64_t)1784537499699278U,
+ (uint64_t)859195370018706U, (uint64_t)1953966091439379U, (uint64_t)2189271820076010U,
+ (uint64_t)2039067059943978U, (uint64_t)1526694380855202U, (uint64_t)2040321513194941U,
+ (uint64_t)329922071218689U, (uint64_t)1953032256401326U, (uint64_t)989631424403521U,
+ (uint64_t)328825014934242U, (uint64_t)9407151397696U, (uint64_t)63551373671268U,
+ (uint64_t)1624728632895792U, (uint64_t)1608324920739262U, (uint64_t)1178239350351945U,
+ (uint64_t)1198077399579702U, (uint64_t)277620088676229U, (uint64_t)1775359437312528U,
+ (uint64_t)1653558177737477U, (uint64_t)1652066043408850U, (uint64_t)1063359889686622U,
+ (uint64_t)1975063804860653U
+ };
+
+#if defined(__cplusplus)
+}
+#endif
+
+#define __internal_Hacl_Ed25519_PrecompTable_H_DEFINED
+#endif
diff --git a/security/nss/lib/freebl/verified/karamel/include/krml/internal/target.h b/security/nss/lib/freebl/verified/karamel/include/krml/internal/target.h
index b63967f480..198d65f64b 100644
--- a/security/nss/lib/freebl/verified/karamel/include/krml/internal/target.h
+++ b/security/nss/lib/freebl/verified/karamel/include/krml/internal/target.h
@@ -57,6 +57,14 @@
#define KRML_HOST_IGNORE(x) (void)(x)
#endif
+#ifndef KRML_MAYBE_UNUSED
+#if defined(__GNUC__)
+#define KRML_MAYBE_UNUSED __attribute__((unused))
+#else
+#define KRML_MAYBE_UNUSED
+#endif
+#endif
+
#ifndef KRML_NOINLINE
#if defined(_MSC_VER)
#define KRML_NOINLINE __declspec(noinline)
diff --git a/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/fstar_uint128_gcc64.h b/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/fstar_uint128_gcc64.h
index 33cff6b6d4..51c2325854 100644
--- a/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/fstar_uint128_gcc64.h
+++ b/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/fstar_uint128_gcc64.h
@@ -148,7 +148,7 @@ FStar_UInt128_eq_mask(uint128_t x, uint128_t y)
{
uint64_t mask =
FStar_UInt64_eq_mask((uint64_t)(x >> 64), (uint64_t)(y >> 64)) &
- FStar_UInt64_eq_mask(x, y);
+ FStar_UInt64_eq_mask((uint64_t)x, (uint64_t)y);
return ((uint128_t)mask) << 64 | mask;
}
@@ -158,7 +158,7 @@ FStar_UInt128_gte_mask(uint128_t x, uint128_t y)
uint64_t mask =
(FStar_UInt64_gte_mask(x >> 64, y >> 64) &
~(FStar_UInt64_eq_mask(x >> 64, y >> 64))) |
- (FStar_UInt64_eq_mask(x >> 64, y >> 64) & FStar_UInt64_gte_mask(x, y));
+ (FStar_UInt64_eq_mask(x >> 64, y >> 64) & FStar_UInt64_gte_mask((uint64_t)x, (uint64_t)y));
return ((uint128_t)mask) << 64 | mask;
}
diff --git a/security/nss/lib/nss/nss.h b/security/nss/lib/nss/nss.h
index 67272f98a6..f3608b5813 100644
--- a/security/nss/lib/nss/nss.h
+++ b/security/nss/lib/nss/nss.h
@@ -22,9 +22,9 @@
* The format of the version string should be
* "<major version>.<minor version>[.<patch level>[.<build number>]][ <ECC>][ <Beta>]"
*/
-#define NSS_VERSION "3.98" _NSS_CUSTOMIZED
+#define NSS_VERSION "3.99" _NSS_CUSTOMIZED
#define NSS_VMAJOR 3
-#define NSS_VMINOR 98
+#define NSS_VMINOR 99
#define NSS_VPATCH 0
#define NSS_VBUILD 0
#define NSS_BETA PR_FALSE
diff --git a/security/nss/lib/pk11wrap/pk11akey.c b/security/nss/lib/pk11wrap/pk11akey.c
index 343a5bdef5..b797b54aef 100644
--- a/security/nss/lib/pk11wrap/pk11akey.c
+++ b/security/nss/lib/pk11wrap/pk11akey.c
@@ -41,6 +41,7 @@ pk11_MakeIDFromPublicKey(SECKEYPublicKey *pubKey)
case dhKey:
pubKeyIndex = &pubKey->u.dh.publicValue;
break;
+ case edKey:
case ecKey:
pubKeyIndex = &pubKey->u.ec.publicValue;
break;
@@ -190,6 +191,19 @@ PK11_ImportPublicKey(PK11SlotInfo *slot, SECKEYPublicKey *pubKey,
pubKey->u.dh.publicValue.len);
attrs++;
break;
+ case edKey:
+ keyType = CKK_EC_EDWARDS;
+ PK11_SETATTRS(attrs, CKA_VERIFY, &cktrue, sizeof(CK_BBOOL));
+ attrs++;
+ PK11_SETATTRS(attrs, CKA_EC_PARAMS,
+ pubKey->u.ec.DEREncodedParams.data,
+ pubKey->u.ec.DEREncodedParams.len);
+ attrs++;
+ PK11_SETATTRS(attrs, CKA_EC_POINT,
+ pubKey->u.ec.publicValue.data,
+ pubKey->u.ec.publicValue.len);
+ attrs++;
+ break;
case ecKey:
keyType = CKK_EC;
PK11_SETATTRS(attrs, CKA_VERIFY, &cktrue, sizeof(CK_BBOOL));
@@ -248,7 +262,7 @@ PK11_ImportPublicKey(PK11SlotInfo *slot, SECKEYPublicKey *pubKey,
}
templateCount = attrs - theTemplate;
PORT_Assert(templateCount <= (sizeof(theTemplate) / sizeof(CK_ATTRIBUTE)));
- if (pubKey->keyType != ecKey && pubKey->keyType != kyberKey) {
+ if (pubKey->keyType != ecKey && pubKey->keyType != kyberKey && pubKey->keyType != edKey) {
PORT_Assert(signedattr);
signedcount = attrs - signedattr;
for (attrs = signedattr; signedcount; attrs++, signedcount--) {
@@ -407,6 +421,7 @@ pk11_get_EC_PointLenInBytes(PLArenaPool *arena, const SECItem *ecParams,
case SEC_OID_SECG_EC_SECT571R1:
return 145; /*curve len in bytes = 72 bytes */
case SEC_OID_CURVE25519:
+ case SEC_OID_ED25519_PUBLIC_KEY:
*plain = PR_TRUE;
return 32; /* curve len in bytes = 32 bytes (only X) */
/* unknown or unrecognized OIDs. return unknown length */
@@ -642,6 +657,9 @@ PK11_ExtractPublicKey(PK11SlotInfo *slot, KeyType keyType, CK_OBJECT_HANDLE id)
case CKK_EC:
keyType = ecKey;
break;
+ case CKK_EC_EDWARDS:
+ keyType = edKey;
+ break;
case CKK_NSS_KYBER:
keyType = kyberKey;
break;
@@ -771,6 +789,7 @@ PK11_ExtractPublicKey(PK11SlotInfo *slot, KeyType keyType, CK_OBJECT_HANDLE id)
if (crv != CKR_OK)
break;
break;
+ case edKey:
case ecKey:
pubKey->u.ec.size = 0;
ecparams = attrs;
@@ -785,7 +804,7 @@ PK11_ExtractPublicKey(PK11SlotInfo *slot, KeyType keyType, CK_OBJECT_HANDLE id)
if (crv != CKR_OK)
break;
- if ((keyClass != CKO_PUBLIC_KEY) || (pk11KeyType != CKK_EC)) {
+ if ((keyClass != CKO_PUBLIC_KEY) || (pk11KeyType != CKK_EC && pk11KeyType != CKK_EC_EDWARDS)) {
crv = CKR_OBJECT_HANDLE_INVALID;
break;
}
@@ -886,6 +905,9 @@ PK11_MakePrivKey(PK11SlotInfo *slot, KeyType keyType,
case CKK_EC:
keyType = ecKey;
break;
+ case CKK_EC_EDWARDS:
+ keyType = edKey;
+ break;
case CKK_NSS_KYBER:
keyType = kyberKey;
break;
@@ -1093,6 +1115,7 @@ pk11_loadPrivKeyWithFlags(PK11SlotInfo *slot, SECKEYPrivateKey *privKey,
extra_count++;
break;
case ecKey:
+ case edKey:
ap->type = CKA_EC_PARAMS;
ap++;
count++;
@@ -1101,10 +1124,13 @@ pk11_loadPrivKeyWithFlags(PK11SlotInfo *slot, SECKEYPrivateKey *privKey,
ap++;
count++;
extra_count++;
- ap->type = CKA_DERIVE;
- ap++;
- count++;
- extra_count++;
+ if (privKey->keyType == ecKey) {
+ ap->type = CKA_DERIVE;
+ ap++;
+ count++;
+ extra_count++;
+ }
+
ap->type = CKA_SIGN;
ap++;
count++;
@@ -1143,7 +1169,7 @@ pk11_loadPrivKeyWithFlags(PK11SlotInfo *slot, SECKEYPrivateKey *privKey,
* them the raw data as unsigned. The exception is EC,
* where the values are encoded or zero-preserving
* per-RFC5915 */
- if (privKey->keyType != ecKey) {
+ if (privKey->keyType != ecKey && privKey->keyType != edKey) {
for (ap = attrs; extra_count; ap++, extra_count--) {
pk11_SignedToUnsigned(ap);
}
@@ -1499,6 +1525,16 @@ PK11_GenerateKeyPairWithOpFlags(PK11SlotInfo *slot, CK_MECHANISM_TYPE type,
keyType = kyberKey;
test_mech.mechanism = CKM_NSS_KYBER;
break;
+ case CKM_EC_EDWARDS_KEY_PAIR_GEN:
+ ecParams = (SECKEYECParams *)param;
+ attrs = ecPubTemplate;
+ PK11_SETATTRS(attrs, CKA_EC_PARAMS, ecParams->data,
+ ecParams->len);
+ attrs++;
+ pubTemplate = ecPubTemplate;
+ keyType = edKey;
+ test_mech.mechanism = CKM_EDDSA;
+ break;
default:
PORT_SetError(SEC_ERROR_BAD_KEY);
return NULL;
@@ -1555,6 +1591,10 @@ PK11_GenerateKeyPairWithOpFlags(PK11SlotInfo *slot, CK_MECHANISM_TYPE type,
case CKM_ECDSA:
mechanism_info.flags = CKF_SIGN | CKF_VERIFY;
break;
+ case CKM_EDDSA:
+ mechanism_info.flags = CKF_SIGN | CKF_VERIFY;
+ break;
+
default:
break;
}
@@ -1835,6 +1875,7 @@ SECKEY_SetPublicValue(SECKEYPrivateKey *privKey, SECItem *publicValue)
rv = PK11_ReadAttribute(slot, privKeyID, CKA_BASE,
arena, &pubKey.u.dh.base);
break;
+ case edKey:
case ecKey:
pubKey.u.ec.publicValue = *publicValue;
pubKey.u.ec.encoding = ECPoint_Undefined;
@@ -1905,6 +1946,7 @@ PK11_ImportEncryptedPrivateKeyInfoAndReturnKey(PK11SlotInfo *slot,
CK_ATTRIBUTE_TYPE dsaUsage[] = { CKA_SIGN };
CK_ATTRIBUTE_TYPE dhUsage[] = { CKA_DERIVE };
CK_ATTRIBUTE_TYPE ecUsage[] = { CKA_SIGN, CKA_DERIVE };
+ CK_ATTRIBUTE_TYPE edUsage[] = { CKA_SIGN };
if ((epki == NULL) || (pwitem == NULL))
return SECFailure;
@@ -1959,6 +2001,11 @@ PK11_ImportEncryptedPrivateKeyInfoAndReturnKey(PK11SlotInfo *slot,
break;
}
break;
+ case edKey:
+ key_type = CKK_EC_EDWARDS;
+ usage = edUsage;
+ usageCount = 1;
+ break;
}
try_faulty_3des:
diff --git a/security/nss/lib/pk11wrap/pk11cert.c b/security/nss/lib/pk11wrap/pk11cert.c
index 580d02b613..fb37b713ed 100644
--- a/security/nss/lib/pk11wrap/pk11cert.c
+++ b/security/nss/lib/pk11wrap/pk11cert.c
@@ -171,6 +171,7 @@ PK11_IsUserCert(PK11SlotInfo *slot, CERTCertificate *cert,
pubKey->u.dh.publicValue.len);
break;
case ecKey:
+ case edKey:
PK11_SETATTRS(&theTemplate, CKA_EC_POINT,
pubKey->u.ec.publicValue.data,
pubKey->u.ec.publicValue.len);
@@ -187,7 +188,7 @@ PK11_IsUserCert(PK11SlotInfo *slot, CERTCertificate *cert,
SECKEY_DestroyPublicKey(pubKey);
return PR_FALSE;
}
- if (pubKey->keyType != ecKey) {
+ if (pubKey->keyType != ecKey && pubKey->keyType != edKey) {
pk11_SignedToUnsigned(&theTemplate);
}
if (pk11_FindObjectByTemplate(slot, &theTemplate, 1) != CK_INVALID_HANDLE) {
@@ -1113,6 +1114,7 @@ PK11_GetPubIndexKeyID(CERTCertificate *cert)
newItem = SECITEM_DupItem(&pubk->u.dh.publicValue);
break;
case ecKey:
+ case edKey:
newItem = SECITEM_DupItem(&pubk->u.ec.publicValue);
break;
case fortezzaKey:
diff --git a/security/nss/lib/pk11wrap/pk11mech.c b/security/nss/lib/pk11wrap/pk11mech.c
index 54e55c6da2..df7e3455bc 100644
--- a/security/nss/lib/pk11wrap/pk11mech.c
+++ b/security/nss/lib/pk11wrap/pk11mech.c
@@ -198,6 +198,8 @@ PK11_GetKeyMechanism(CK_KEY_TYPE type)
return CKM_KEA_KEY_DERIVE;
case CKK_EC: /* CKK_ECDSA is deprecated */
return CKM_ECDSA;
+ case CKK_EC_EDWARDS:
+ return CKM_EDDSA;
case CKK_HKDF:
return CKM_HKDF_DERIVE;
case CKK_GENERIC_SECRET:
@@ -388,6 +390,9 @@ PK11_GetKeyType(CK_MECHANISM_TYPE type, unsigned long len)
case CKM_EC_KEY_PAIR_GEN: /* aka CKM_ECDSA_KEY_PAIR_GEN */
case CKM_ECDH1_DERIVE:
return CKK_EC; /* CKK_ECDSA is deprecated */
+ case CKM_EC_EDWARDS_KEY_PAIR_GEN:
+ case CKM_EDDSA:
+ return CKK_EC_EDWARDS;
case CKM_HKDF_KEY_GEN:
case CKM_HKDF_DERIVE:
case CKM_HKDF_DATA:
@@ -603,6 +608,8 @@ PK11_GetKeyGenWithSize(CK_MECHANISM_TYPE type, int size)
case CKM_EC_KEY_PAIR_GEN: /* aka CKM_ECDSA_KEY_PAIR_GEN */
case CKM_ECDH1_DERIVE:
return CKM_EC_KEY_PAIR_GEN;
+ case CKM_EDDSA:
+ return CKM_EC_EDWARDS_KEY_PAIR_GEN;
case CKM_SSL3_PRE_MASTER_KEY_GEN:
case CKM_SSL3_MASTER_KEY_DERIVE:
case CKM_SSL3_KEY_AND_MAC_DERIVE:
@@ -1917,6 +1924,8 @@ PK11_MapSignKeyType(KeyType keyType)
return CKM_DSA;
case ecKey:
return CKM_ECDSA;
+ case edKey:
+ return CKM_EDDSA;
case dhKey:
default:
break;
diff --git a/security/nss/lib/pk11wrap/pk11obj.c b/security/nss/lib/pk11wrap/pk11obj.c
index 1661bcb2b4..5759408a27 100644
--- a/security/nss/lib/pk11wrap/pk11obj.c
+++ b/security/nss/lib/pk11wrap/pk11obj.c
@@ -575,7 +575,7 @@ PK11_SignatureLen(SECKEYPrivateKey *key)
return length * 2;
}
return pk11_backupGetSignLength(key);
-
+ case edKey:
case ecKey:
rv = PK11_ReadAttribute(key->pkcs11Slot, key->pkcs11ID, CKA_EC_PARAMS,
NULL, &attributeItem);
diff --git a/security/nss/lib/pk11wrap/pk11pars.c b/security/nss/lib/pk11wrap/pk11pars.c
index bda4ab688a..45b4a5934a 100644
--- a/security/nss/lib/pk11wrap/pk11pars.c
+++ b/security/nss/lib/pk11wrap/pk11pars.c
@@ -402,6 +402,8 @@ static const oidValDef signOptList[] = {
NSS_USE_ALG_IN_SSL_KX | NSS_USE_ALG_IN_SIGNATURE },
{ CIPHER_NAME("ECDSA"), SEC_OID_ANSIX962_EC_PUBLIC_KEY,
NSS_USE_ALG_IN_SSL_KX | NSS_USE_ALG_IN_SIGNATURE },
+ { CIPHER_NAME("ED25519"), SEC_OID_ED25519_PUBLIC_KEY,
+ NSS_USE_ALG_IN_SIGNATURE },
};
typedef struct {
diff --git a/security/nss/lib/pk11wrap/pk11pk12.c b/security/nss/lib/pk11wrap/pk11pk12.c
index 917b7f0f67..5d8b00d3d0 100644
--- a/security/nss/lib/pk11wrap/pk11pk12.c
+++ b/security/nss/lib/pk11wrap/pk11pk12.c
@@ -180,6 +180,13 @@ const SEC_ASN1Template SECKEY_ECPrivateKeyExportTemplate[] = {
{ 0 }
};
+/* The template operates a private key consisting only of private key. */
+const SEC_ASN1Template SECKEY_EDPrivateKeyExportTemplate[] = {
+ { SEC_ASN1_OCTET_STRING,
+ offsetof(SECKEYRawPrivateKey, u.ec.privateValue) },
+ { 0 }
+};
+
const SEC_ASN1Template SECKEY_EncryptedPrivateKeyInfoTemplate[] = {
{ SEC_ASN1_SEQUENCE,
0, NULL, sizeof(SECKEYEncryptedPrivateKeyInfo) },
@@ -270,8 +277,10 @@ PK11_ImportDERPrivateKeyInfoAndReturnKey(PK11SlotInfo *slot, SECItem *derPKI,
SECStatus rv = SECFailure;
temparena = PORT_NewArena(DER_DEFAULT_CHUNKSIZE);
- if (!temparena)
+ if (!temparena) {
return rv;
+ }
+
pki = PORT_ArenaZNew(temparena, SECKEYPrivateKeyInfo);
if (!pki) {
PORT_FreeArena(temparena, PR_FALSE);
@@ -523,13 +532,31 @@ PK11_ImportAndReturnPrivateKey(PK11SlotInfo *slot, SECKEYRawPrivateKey *lpk,
lpk->u.ec.publicValue.len);
attrs++;
break;
+ case edKey:
+ keyType = CKK_EC_EDWARDS;
+ PK11_SETATTRS(attrs, CKA_SIGN, &cktrue, sizeof(CK_BBOOL));
+ attrs++;
+ if (nickname) {
+ PK11_SETATTRS(attrs, CKA_LABEL, nickname->data, nickname->len);
+ attrs++;
+ }
+
+ /* No signed attrs for EC */
+ /* curveOID always is a copy of AlgorithmID.parameters. */
+ PK11_SETATTRS(attrs, CKA_EC_PARAMS, lpk->u.ec.curveOID.data,
+ lpk->u.ec.curveOID.len);
+ attrs++;
+ PK11_SETATTRS(attrs, CKA_VALUE, lpk->u.ec.privateValue.data,
+ lpk->u.ec.privateValue.len);
+ attrs++;
+ break;
default:
PORT_SetError(SEC_ERROR_BAD_KEY);
goto loser;
}
templateCount = attrs - theTemplate;
PORT_Assert(templateCount <= sizeof(theTemplate) / sizeof(CK_ATTRIBUTE));
- if (lpk->keyType != ecKey) {
+ if (lpk->keyType != ecKey && lpk->keyType != edKey) {
PORT_Assert(signedattr);
signedcount = attrs - signedattr;
for (ap = signedattr; signedcount; ap++, signedcount--) {
@@ -604,6 +631,12 @@ PK11_ImportPrivateKeyInfoAndReturnKey(PK11SlotInfo *slot,
paramDest = NULL;
lpk->keyType = dhKey;
break;
+ case SEC_OID_ED25519_PUBLIC_KEY:
+ keyTemplate = SECKEY_EDPrivateKeyExportTemplate;
+ paramTemplate = NULL;
+ paramDest = NULL;
+ lpk->keyType = edKey;
+ break;
case SEC_OID_ANSIX962_EC_PUBLIC_KEY:
prepare_ec_priv_key_export_for_asn1(lpk);
keyTemplate = SECKEY_ECPrivateKeyExportTemplate;
@@ -641,6 +674,26 @@ PK11_ImportPrivateKeyInfoAndReturnKey(PK11SlotInfo *slot,
}
}
+ if (lpk->keyType == edKey) {
+ /* Convert length in bits to length in bytes. */
+ lpk->u.ec.publicValue.len >>= 3;
+
+ if (pki->algorithm.parameters.len != 0) {
+ /* Currently supporting only (Pure)Ed25519 .*/
+ PORT_SetError(SEC_ERROR_UNSUPPORTED_KEYALG);
+ goto loser;
+ }
+
+ SECOidData *oidEd25519 = SECOID_FindOIDByTag(SEC_OID_ED25519_PUBLIC_KEY);
+
+ if (!SECITEM_AllocItem(arena, &lpk->u.ec.curveOID, oidEd25519->oid.len + 2)) {
+ goto loser;
+ }
+ lpk->u.ec.curveOID.data[0] = SEC_ASN1_OBJECT_ID;
+ lpk->u.ec.curveOID.data[1] = oidEd25519->oid.len;
+ PORT_Memcpy(lpk->u.ec.curveOID.data + 2, oidEd25519->oid.data, oidEd25519->oid.len);
+ }
+
if (paramDest && paramTemplate) {
rv = SEC_ASN1DecodeItem(arena, paramDest, paramTemplate,
&(pki->algorithm.parameters));
@@ -651,7 +704,6 @@ PK11_ImportPrivateKeyInfoAndReturnKey(PK11SlotInfo *slot,
rv = PK11_ImportAndReturnPrivateKey(slot, lpk, nickname, publicValue, isPerm,
isPrivate, keyUsage, privk, wincx);
-
loser:
if (arena != NULL) {
PORT_FreeArena(arena, PR_TRUE);
@@ -800,6 +852,28 @@ PK11_ExportPrivKeyInfo(SECKEYPrivateKey *pk, void *wincx)
}
} break;
+ case edKey: {
+ rawKey.u.ec.version.type = siUnsignedInteger;
+ rawKey.u.ec.version.data = (unsigned char *)PORT_ArenaAlloc(arena, 1);
+ if (!rawKey.u.ec.version.data) {
+ goto loser;
+ }
+ rawKey.u.ec.version.data[0] = ecVersion;
+ rawKey.u.ec.version.len = 1;
+
+ if (!ReadAttribute(pk, CKA_VALUE, arena,
+ &rawKey.u.ec.privateValue)) {
+ goto loser;
+ }
+
+ keyTemplate = SECKEY_EDPrivateKeyExportTemplate;
+ /* Currently, ED25519 does not support any parameter. */
+ rv = SECOID_SetAlgorithmID(arena, &pki->algorithm, SEC_OID_ED25519_PUBLIC_KEY, NULL);
+ if (rv != SECSuccess) {
+ goto loser;
+ }
+
+ } break;
default: {
PORT_SetError(PR_NOT_IMPLEMENTED_ERROR);
goto loser;
diff --git a/security/nss/lib/pk11wrap/pk11skey.c b/security/nss/lib/pk11wrap/pk11skey.c
index f09519ee27..02db85b6bf 100644
--- a/security/nss/lib/pk11wrap/pk11skey.c
+++ b/security/nss/lib/pk11wrap/pk11skey.c
@@ -2097,7 +2097,7 @@ PK11_DerivePubKeyFromPrivKey(SECKEYPrivateKey *privKey)
/*
* This Generates a wrapping key based on a privateKey, publicKey, and two
* random numbers. For Mail usage RandomB should be NULL. In the Sender's
- * case RandomA is generate, outherwize it is passed.
+ * case RandomA is generate, otherwise it is passed.
*/
PK11SymKey *
PK11_PubDerive(SECKEYPrivateKey *privKey, SECKEYPublicKey *pubKey,
@@ -2218,6 +2218,9 @@ PK11_PubDerive(SECKEYPrivateKey *privKey, SECKEYPublicKey *pubKey,
return symKey;
PORT_SetError(PK11_MapError(crv));
} break;
+ case edKey:
+ PORT_SetError(SEC_ERROR_BAD_KEY);
+ break;
case ecKey: {
CK_BBOOL cktrue = CK_TRUE;
CK_OBJECT_CLASS keyClass = CKO_SECRET_KEY;
diff --git a/security/nss/lib/pk11wrap/pk11slot.c b/security/nss/lib/pk11wrap/pk11slot.c
index d61d0f750d..90a429d952 100644
--- a/security/nss/lib/pk11wrap/pk11slot.c
+++ b/security/nss/lib/pk11wrap/pk11slot.c
@@ -36,6 +36,7 @@ const PK11DefaultArrayEntry PK11_DefaultArray[] = {
{ "RSA", SECMOD_RSA_FLAG, CKM_RSA_PKCS },
{ "DSA", SECMOD_DSA_FLAG, CKM_DSA },
{ "ECC", SECMOD_ECC_FLAG, CKM_ECDSA },
+ { "EDDSA", SECMOD_ECC_FLAG, CKM_EDDSA },
{ "DH", SECMOD_DH_FLAG, CKM_DH_PKCS_DERIVE },
{ "RC2", SECMOD_RC2_FLAG, CKM_RC2_CBC },
{ "RC4", SECMOD_RC4_FLAG, CKM_RC4 },
@@ -940,6 +941,8 @@ PK11_GetSlotList(CK_MECHANISM_TYPE type)
case CKM_DH_PKCS_KEY_PAIR_GEN:
case CKM_DH_PKCS_DERIVE:
return &pk11_dhSlotList;
+ case CKM_EDDSA:
+ case CKM_EC_EDWARDS_KEY_PAIR_GEN:
case CKM_ECDSA:
case CKM_ECDSA_SHA1:
case CKM_EC_KEY_PAIR_GEN: /* aka CKM_ECDSA_KEY_PAIR_GEN */
diff --git a/security/nss/lib/smime/cms.h b/security/nss/lib/smime/cms.h
index f4a8a39e9e..fb803e1f79 100644
--- a/security/nss/lib/smime/cms.h
+++ b/security/nss/lib/smime/cms.h
@@ -815,6 +815,9 @@ NSS_CMSEnvelopedData_Decode_AfterEnd(NSSCMSEnvelopedData *envd);
* cmsrecinfo.c - CMS recipientInfo methods
************************************************************************/
+extern PRBool
+NSS_CMSRecipient_IsSupported(CERTCertificate *cert);
+
/*
* NSS_CMSRecipientInfo_Create - create a recipientinfo
*
diff --git a/security/nss/lib/smime/cmsrecinfo.c b/security/nss/lib/smime/cmsrecinfo.c
index 20dd698e8f..6cf2c68c31 100644
--- a/security/nss/lib/smime/cmsrecinfo.c
+++ b/security/nss/lib/smime/cmsrecinfo.c
@@ -118,6 +118,8 @@ nss_cmsrecipientinfo_create(NSSCMSMessage *cmsg,
certalgtag = SECOID_GetAlgorithmTag(&(spki->algorithm));
rid = &ri->ri.keyTransRecipientInfo.recipientIdentifier;
+
+ // This switch must match the switch in NSS_CMSRecipient_IsSupported.
switch (certalgtag) {
case SEC_OID_PKCS1_RSA_ENCRYPTION:
ri->recipientInfoType = NSSCMSRecipientInfoID_KeyTrans;
@@ -258,6 +260,28 @@ loser:
}
/*
+ * NSS_CMSRecipient_IsSupported - checks for a support certificate
+ *
+ * Use this function to confirm that the given certificate will be
+ * accepted by NSS_CMSRecipientInfo_Create, which means that the
+ * certificate can be used with a supported encryption algorithm.
+ */
+PRBool
+NSS_CMSRecipient_IsSupported(CERTCertificate *cert)
+{
+ CERTSubjectPublicKeyInfo *spki = &(cert->subjectPublicKeyInfo);
+ SECOidTag certalgtag = SECOID_GetAlgorithmTag(&(spki->algorithm));
+
+ switch (certalgtag) {
+ case SEC_OID_PKCS1_RSA_ENCRYPTION:
+ case SEC_OID_X942_DIFFIE_HELMAN_KEY: /* dh-public-number */
+ return PR_TRUE;
+ default:
+ return PR_FALSE;
+ }
+}
+
+/*
* NSS_CMSRecipientInfo_Create - create a recipientinfo
*
* we currently do not create KeyAgreement recipientinfos with multiple
diff --git a/security/nss/lib/smime/smime.def b/security/nss/lib/smime/smime.def
index ba9d09d8cb..d5cff92f37 100644
--- a/security/nss/lib/smime/smime.def
+++ b/security/nss/lib/smime/smime.def
@@ -291,3 +291,9 @@ NSS_CMSSignerInfo_GetDigestAlgTag;
;+ local:
;+ *;
;+};
+;+NSS_3.99 { # NSS 3.99 release
+;+ global:
+NSS_CMSRecipient_IsSupported;
+;+ local:
+;+ *;
+;+};
diff --git a/security/nss/lib/softoken/lowkey.c b/security/nss/lib/softoken/lowkey.c
index f47bda231d..5adae04263 100644
--- a/security/nss/lib/softoken/lowkey.c
+++ b/security/nss/lib/softoken/lowkey.c
@@ -9,6 +9,7 @@
#include "secasn1.h"
#include "secerr.h"
#include "softoken.h"
+#include "ec.h"
SEC_ASN1_MKSUB(SEC_AnyTemplate)
SEC_ASN1_MKSUB(SEC_BitStringTemplate)
@@ -381,6 +382,24 @@ nsslowkey_ConvertToPublicKey(NSSLOWKEYPrivateKey *privk)
pubk->arena = arena;
pubk->keyType = privk->keyType;
+
+ /* if the public key value doesn't exist, calculate it */
+ if (privk->u.ec.publicValue.len == 0) {
+ /* Checking if it's an ed25519 key. */
+ SECOidTag privKeyOIDTag = SECOID_FindOIDTag(&privk->u.ec.ecParams.curveOID);
+ if (privKeyOIDTag == SEC_OID_ED25519_PUBLIC_KEY) {
+ PORT_Memset(&privk->u.ec.publicValue, 0, sizeof(privk->u.ec.publicValue));
+ if (SECITEM_AllocItem(privk->arena, &privk->u.ec.publicValue, Ed25519_PUBLIC_KEYLEN) == NULL) {
+ break;
+ }
+
+ rv = ED_DerivePublicKey(&privk->u.ec.privateValue, &privk->u.ec.publicValue);
+ if (rv != CKR_OK) {
+ break;
+ }
+ }
+ }
+
rv = SECITEM_CopyItem(arena, &pubk->u.ec.publicValue,
&privk->u.ec.publicValue);
if (rv != SECSuccess)
diff --git a/security/nss/lib/softoken/lowpbe.c b/security/nss/lib/softoken/lowpbe.c
index ff80f573ff..68c19aaaf4 100644
--- a/security/nss/lib/softoken/lowpbe.c
+++ b/security/nss/lib/softoken/lowpbe.c
@@ -803,13 +803,7 @@ nsspkcs5_ComputeKeyAndIV(NSSPKCS5PBEParameter *pbe_param, SECItem *pwitem,
goto loser;
}
- if (pbe_param->is2KeyDES) {
- PORT_Memcpy(key->data, hash->data, (key->len * 2) / 3);
- PORT_Memcpy(&(key->data[(key->len * 2) / 3]), key->data,
- key->len / 3);
- } else {
- PORT_Memcpy(key->data, hash->data, key->len);
- }
+ PORT_Memcpy(key->data, hash->data, key->len);
SECITEM_ZfreeItem(hash, PR_TRUE);
return key;
@@ -878,10 +872,15 @@ nsspkcs5_FillInParam(SECOidTag algorithm, HASH_HashType hashType,
/* DES3 Algorithms */
case SEC_OID_PKCS12_V2_PBE_WITH_SHA1_AND_2KEY_TRIPLE_DES_CBC:
pbe_param->is2KeyDES = PR_TRUE;
- /* fall through */
+ pbe_param->pbeType = NSSPKCS5_PKCS12_V2;
+ pbe_param->keyLen = 16;
+ pbe_param->encAlg = SEC_OID_DES_EDE3_CBC;
+ break;
case SEC_OID_PKCS12_V2_PBE_WITH_SHA1_AND_3KEY_TRIPLE_DES_CBC:
pbe_param->pbeType = NSSPKCS5_PKCS12_V2;
- /* fall through */
+ pbe_param->keyLen = 24;
+ pbe_param->encAlg = SEC_OID_DES_EDE3_CBC;
+ break;
case SEC_OID_PKCS12_PBE_WITH_SHA1_AND_TRIPLE_DES_CBC:
pbe_param->keyLen = 24;
pbe_param->encAlg = SEC_OID_DES_EDE3_CBC;
diff --git a/security/nss/lib/softoken/pkcs11.c b/security/nss/lib/softoken/pkcs11.c
index 9c0d93e317..768c7c2669 100644
--- a/security/nss/lib/softoken/pkcs11.c
+++ b/security/nss/lib/softoken/pkcs11.c
@@ -310,6 +310,7 @@ struct mechanismList {
#define CKF_EC_PNU CKF_EC_F_P | CKF_EC_NAMEDCURVE | CKF_EC_UNCOMPRESS
#define CKF_EC_BPNU CKF_EC_F_2M | CKF_EC_PNU
+#define CKF_EC_POC CKF_EC_F_P | CKF_EC_OID | CKF_EC_COMPRESS
#define CK_MAX 0xffffffff
@@ -379,6 +380,8 @@ static const struct mechanismList mechanisms[] = {
{ CKM_ECDSA_SHA256, { EC_MIN_KEY_BITS, EC_MAX_KEY_BITS, CKF_SN_VR | CKF_EC_BPNU }, PR_TRUE },
{ CKM_ECDSA_SHA384, { EC_MIN_KEY_BITS, EC_MAX_KEY_BITS, CKF_SN_VR | CKF_EC_BPNU }, PR_TRUE },
{ CKM_ECDSA_SHA512, { EC_MIN_KEY_BITS, EC_MAX_KEY_BITS, CKF_SN_VR | CKF_EC_BPNU }, PR_TRUE },
+ { CKM_EC_EDWARDS_KEY_PAIR_GEN, { ECD_MIN_KEY_BITS, ECD_MAX_KEY_BITS, CKF_GENERATE_KEY_PAIR }, PR_TRUE },
+ { CKM_EDDSA, { ECD_MIN_KEY_BITS, ECD_MAX_KEY_BITS, CKF_SN_VR | CKF_EC_POC }, PR_TRUE },
/* ------------------------- RC2 Operations --------------------------- */
{ CKM_RC2_KEY_GEN, { 1, 128, CKF_GENERATE }, PR_TRUE },
{ CKM_RC2_ECB, { 1, 128, CKF_EN_DE_WR_UN }, PR_TRUE },
@@ -1074,6 +1077,8 @@ sftk_handlePublicKeyObject(SFTKSession *session, SFTKObject *object,
recover = CK_FALSE;
wrap = CK_FALSE;
break;
+ case CKK_EC_MONTGOMERY:
+ case CKK_EC_EDWARDS:
case CKK_EC:
if (!sftk_hasAttribute(object, CKA_EC_PARAMS)) {
return CKR_TEMPLATE_INCOMPLETE;
@@ -1081,8 +1086,9 @@ sftk_handlePublicKeyObject(SFTKSession *session, SFTKObject *object,
if (!sftk_hasAttribute(object, CKA_EC_POINT)) {
return CKR_TEMPLATE_INCOMPLETE;
}
- derive = CK_TRUE; /* for ECDH */
- verify = CK_TRUE; /* for ECDSA */
+ /* for ECDSA and EDDSA. Change if the structure of any of them is modified. */
+ derive = (key_type == CKK_EC_EDWARDS) ? CK_FALSE : CK_TRUE; /* CK_TRUE for ECDH */
+ verify = CK_TRUE; /* for ECDSA */
encrypt = CK_FALSE;
recover = CK_FALSE;
wrap = CK_FALSE;
@@ -1129,7 +1135,7 @@ sftk_handlePublicKeyObject(SFTKSession *session, SFTKObject *object,
object->infoFree = (SFTKFree)nsslowkey_DestroyPublicKey;
/* Check that an imported EC key is valid */
- if (key_type == CKK_EC) {
+ if (key_type == CKK_EC || key_type == CKK_EC_EDWARDS || key_type == CKK_EC_MONTGOMERY) {
NSSLOWKEYPublicKey *pubKey = (NSSLOWKEYPublicKey *)object->objectInfo;
SECStatus rv = EC_ValidatePublicKey(&pubKey->u.ec.ecParams,
&pubKey->u.ec.publicValue);
@@ -1271,6 +1277,8 @@ sftk_handlePrivateKeyObject(SFTKSession *session, SFTKObject *object, CK_KEY_TYP
wrap = CK_FALSE;
break;
case CKK_EC:
+ case CKK_EC_EDWARDS:
+ case CKK_EC_MONTGOMERY:
if (!sftk_hasAttribute(object, CKA_EC_PARAMS)) {
return CKR_TEMPLATE_INCOMPLETE;
}
@@ -1926,6 +1934,8 @@ sftk_GetPubKey(SFTKObject *object, CK_KEY_TYPE key_type,
crv = sftk_Attribute2SSecItem(arena, &pubKey->u.dh.publicValue,
object, CKA_VALUE);
break;
+ case CKK_EC_EDWARDS:
+ case CKK_EC_MONTGOMERY:
case CKK_EC:
pubKey->keyType = NSSLOWKEYECKey;
crv = sftk_Attribute2SSecItem(arena,
@@ -2098,7 +2108,8 @@ sftk_mkPrivKey(SFTKObject *object, CK_KEY_TYPE key_type, CK_RV *crvp)
/* privKey was zero'd so public value is already set to NULL, 0
* if we don't set it explicitly */
break;
-
+ case CKK_EC_EDWARDS:
+ case CKK_EC_MONTGOMERY:
case CKK_EC:
privKey->keyType = NSSLOWKEYECKey;
crv = sftk_Attribute2SSecItem(arena,
@@ -2414,6 +2425,8 @@ sftk_PutPubKey(SFTKObject *publicKey, SFTKObject *privateKey, CK_KEY_TYPE keyTyp
sftk_item_expand(&pubKey->u.dh.publicValue));
break;
case CKK_EC:
+ case CKK_EC_MONTGOMERY:
+ case CKK_EC_EDWARDS:
sftk_DeleteAttributeType(publicKey, CKA_EC_PARAMS);
sftk_DeleteAttributeType(publicKey, CKA_EC_POINT);
crv = sftk_AddAttributeType(publicKey, CKA_EC_PARAMS,
diff --git a/security/nss/lib/softoken/pkcs11c.c b/security/nss/lib/softoken/pkcs11c.c
index 856c98e7cf..758a7eba45 100644
--- a/security/nss/lib/softoken/pkcs11c.c
+++ b/security/nss/lib/softoken/pkcs11c.c
@@ -2668,13 +2668,9 @@ static SECStatus
nsc_DSA_Verify_Stub(void *ctx, void *sigBuf, unsigned int sigLen,
void *dataBuf, unsigned int dataLen)
{
- SECItem signature, digest;
+ SECItem signature = { siBuffer, (unsigned char *)sigBuf, sigLen };
+ SECItem digest = { siBuffer, (unsigned char *)dataBuf, dataLen };
NSSLOWKEYPublicKey *key = (NSSLOWKEYPublicKey *)ctx;
-
- signature.data = (unsigned char *)sigBuf;
- signature.len = sigLen;
- digest.data = (unsigned char *)dataBuf;
- digest.len = dataLen;
return DSA_VerifyDigest(&(key->u.dsa), &signature, &digest);
}
@@ -2683,15 +2679,10 @@ nsc_DSA_Sign_Stub(void *ctx, void *sigBuf,
unsigned int *sigLen, unsigned int maxSigLen,
void *dataBuf, unsigned int dataLen)
{
- SECItem signature, digest;
- SECStatus rv;
NSSLOWKEYPrivateKey *key = (NSSLOWKEYPrivateKey *)ctx;
-
- signature.data = (unsigned char *)sigBuf;
- signature.len = maxSigLen;
- digest.data = (unsigned char *)dataBuf;
- digest.len = dataLen;
- rv = DSA_SignDigest(&(key->u.dsa), &signature, &digest);
+ SECItem signature = { siBuffer, (unsigned char *)sigBuf, maxSigLen };
+ SECItem digest = { siBuffer, (unsigned char *)dataBuf, dataLen };
+ SECStatus rv = DSA_SignDigest(&(key->u.dsa), &signature, &digest);
if (rv != SECSuccess && PORT_GetError() == SEC_ERROR_LIBRARY_FAILURE) {
sftk_fatalError = PR_TRUE;
}
@@ -2703,13 +2694,9 @@ static SECStatus
nsc_ECDSAVerifyStub(void *ctx, void *sigBuf, unsigned int sigLen,
void *dataBuf, unsigned int dataLen)
{
- SECItem signature, digest;
+ SECItem signature = { siBuffer, (unsigned char *)sigBuf, sigLen };
+ SECItem digest = { siBuffer, (unsigned char *)dataBuf, dataLen };
NSSLOWKEYPublicKey *key = (NSSLOWKEYPublicKey *)ctx;
-
- signature.data = (unsigned char *)sigBuf;
- signature.len = sigLen;
- digest.data = (unsigned char *)dataBuf;
- digest.len = dataLen;
return ECDSA_VerifyDigest(&(key->u.ec), &signature, &digest);
}
@@ -2718,15 +2705,38 @@ nsc_ECDSASignStub(void *ctx, void *sigBuf,
unsigned int *sigLen, unsigned int maxSigLen,
void *dataBuf, unsigned int dataLen)
{
- SECItem signature, digest;
- SECStatus rv;
NSSLOWKEYPrivateKey *key = (NSSLOWKEYPrivateKey *)ctx;
+ SECItem signature = { siBuffer, (unsigned char *)sigBuf, maxSigLen };
+ SECItem digest = { siBuffer, (unsigned char *)dataBuf, dataLen };
- signature.data = (unsigned char *)sigBuf;
- signature.len = maxSigLen;
- digest.data = (unsigned char *)dataBuf;
- digest.len = dataLen;
- rv = ECDSA_SignDigest(&(key->u.ec), &signature, &digest);
+ SECStatus rv = ECDSA_SignDigest(&(key->u.ec), &signature, &digest);
+ if (rv != SECSuccess && PORT_GetError() == SEC_ERROR_LIBRARY_FAILURE) {
+ sftk_fatalError = PR_TRUE;
+ }
+ *sigLen = signature.len;
+ return rv;
+}
+
+static SECStatus
+nsc_EDDSAVerifyStub(void *ctx, void *sigBuf, unsigned int sigLen,
+ void *dataBuf, unsigned int dataLen)
+{
+ SECItem signature = { siBuffer, (unsigned char *)sigBuf, sigLen };
+ SECItem digest = { siBuffer, (unsigned char *)dataBuf, dataLen };
+ NSSLOWKEYPublicKey *key = (NSSLOWKEYPublicKey *)ctx;
+ return ED_VerifyMessage(&(key->u.ec), &signature, &digest);
+}
+
+static SECStatus
+nsc_EDDSASignStub(void *ctx, void *sigBuf,
+ unsigned int *sigLen, unsigned int maxSigLen,
+ void *dataBuf, unsigned int dataLen)
+{
+ NSSLOWKEYPrivateKey *key = (NSSLOWKEYPrivateKey *)ctx;
+ SECItem signature = { siBuffer, (unsigned char *)sigBuf, maxSigLen };
+ SECItem digest = { siBuffer, (unsigned char *)dataBuf, dataLen };
+
+ SECStatus rv = ED_SignMessage(&(key->u.ec), &signature, &digest);
if (rv != SECSuccess && PORT_GetError() == SEC_ERROR_LIBRARY_FAILURE) {
sftk_fatalError = PR_TRUE;
}
@@ -2953,6 +2963,29 @@ NSC_SignInit(CK_SESSION_HANDLE hSession,
break;
+ case CKM_EDDSA:
+ if (key_type != CKK_EC_EDWARDS) {
+ crv = CKR_KEY_TYPE_INCONSISTENT;
+ break;
+ }
+
+ if (pMechanism->pParameter) {
+ crv = CKR_MECHANISM_PARAM_INVALID;
+ break;
+ }
+
+ privKey = sftk_GetPrivKey(key, CKK_EC_EDWARDS, &crv);
+ if (privKey == NULL) {
+ crv = CKR_HOST_MEMORY;
+ break;
+ }
+ context->cipherInfo = privKey;
+ context->update = (SFTKCipher)nsc_EDDSASignStub;
+ context->destroy = (privKey == key->objectInfo) ? (SFTKDestroy)sftk_Null : (SFTKDestroy)sftk_FreePrivKey;
+ context->maxLen = MAX_ECKEY_LEN * 2;
+
+ break;
+
#define INIT_HMAC_MECH(mmm) \
case CKM_##mmm##_HMAC_GENERAL: \
PORT_Assert(pMechanism->pParameter); \
@@ -3736,6 +3769,27 @@ NSC_VerifyInit(CK_SESSION_HANDLE hSession,
INIT_HMAC_MECH(SHA3_384)
INIT_HMAC_MECH(SHA3_512)
+ case CKM_EDDSA:
+ if (key_type != CKK_EC_EDWARDS) {
+ crv = CKR_KEY_TYPE_INCONSISTENT;
+ break;
+ }
+ pubKey = sftk_GetPubKey(key, CKK_EC_EDWARDS, &crv);
+ if (pubKey == NULL) {
+ crv = CKR_HOST_MEMORY;
+ break;
+ }
+
+ if (pMechanism->pParameter) {
+ crv = CKR_FUNCTION_NOT_SUPPORTED;
+ break;
+ }
+
+ context->cipherInfo = pubKey;
+ context->verify = (SFTKVerify)nsc_EDDSAVerifyStub;
+ context->destroy = sftk_Null;
+ break;
+
case CKM_SSL3_MD5_MAC:
PORT_Assert(pMechanism->pParameter);
if (!pMechanism->pParameter) {
@@ -5070,6 +5124,10 @@ sftk_PairwiseConsistencyCheck(CK_SESSION_HANDLE hSession, SFTKSlot *slot,
signature_length = MAX_ECKEY_LEN * 2;
mech.mechanism = CKM_ECDSA;
break;
+ case CKK_EC_EDWARDS:
+ signature_length = ED25519_SIGN_LEN;
+ mech.mechanism = CKM_EDDSA;
+ break;
default:
return CKR_DEVICE_ERROR;
}
@@ -5749,6 +5807,61 @@ NSC_GenerateKeyPair(CK_SESSION_HANDLE hSession,
SECITEM_FreeItem(&pubKey, PR_FALSE);
break;
+ case CKM_EC_EDWARDS_KEY_PAIR_GEN:
+ sftk_DeleteAttributeType(privateKey, CKA_EC_PARAMS);
+ sftk_DeleteAttributeType(privateKey, CKA_VALUE);
+ sftk_DeleteAttributeType(privateKey, CKA_NSS_DB);
+ key_type = CKK_EC_EDWARDS;
+
+ /* extract the necessary parameters and copy them to private keys */
+ crv = sftk_Attribute2SSecItem(NULL, &ecEncodedParams, publicKey,
+ CKA_EC_PARAMS);
+ if (crv != CKR_OK) {
+ break;
+ }
+
+ crv = sftk_AddAttributeType(privateKey, CKA_EC_PARAMS,
+ sftk_item_expand(&ecEncodedParams));
+ if (crv != CKR_OK) {
+ SECITEM_ZfreeItem(&ecEncodedParams, PR_FALSE);
+ break;
+ }
+
+ /* Decode ec params before calling EC_NewKey */
+ rv = EC_DecodeParams(&ecEncodedParams, &ecParams);
+ SECITEM_ZfreeItem(&ecEncodedParams, PR_FALSE);
+ if (rv != SECSuccess) {
+ crv = sftk_MapCryptError(PORT_GetError());
+ break;
+ }
+
+ rv = EC_NewKey(ecParams, &ecPriv);
+ if (rv != SECSuccess) {
+ if (PORT_GetError() == SEC_ERROR_LIBRARY_FAILURE) {
+ sftk_fatalError = PR_TRUE;
+ }
+ PORT_FreeArena(ecParams->arena, PR_TRUE);
+ crv = sftk_MapCryptError(PORT_GetError());
+ break;
+ }
+ PORT_FreeArena(ecParams->arena, PR_TRUE);
+ crv = sftk_AddAttributeType(publicKey, CKA_EC_POINT,
+ sftk_item_expand(&ecPriv->publicValue));
+ if (crv != CKR_OK)
+ goto edgn_done;
+
+ crv = sftk_AddAttributeType(privateKey, CKA_VALUE,
+ sftk_item_expand(&ecPriv->privateValue));
+ if (crv != CKR_OK)
+ goto edgn_done;
+
+ crv = sftk_AddAttributeType(privateKey, CKA_NSS_DB,
+ sftk_item_expand(&ecPriv->publicValue));
+ edgn_done:
+ /* should zeroize, since this function doesn't. */
+ PORT_FreeArena(ecPriv->ecParams.arena, PR_TRUE);
+ break;
+
default:
crv = CKR_MECHANISM_INVALID;
}
diff --git a/security/nss/lib/softoken/softkver.h b/security/nss/lib/softoken/softkver.h
index 1a203f56f2..ae4ebbe017 100644
--- a/security/nss/lib/softoken/softkver.h
+++ b/security/nss/lib/softoken/softkver.h
@@ -17,9 +17,9 @@
* The format of the version string should be
* "<major version>.<minor version>[.<patch level>[.<build number>]][ <ECC>][ <Beta>]"
*/
-#define SOFTOKEN_VERSION "3.98" SOFTOKEN_ECC_STRING
+#define SOFTOKEN_VERSION "3.99" SOFTOKEN_ECC_STRING
#define SOFTOKEN_VMAJOR 3
-#define SOFTOKEN_VMINOR 98
+#define SOFTOKEN_VMINOR 99
#define SOFTOKEN_VPATCH 0
#define SOFTOKEN_VBUILD 0
#define SOFTOKEN_BETA PR_FALSE
diff --git a/security/nss/lib/ssl/ssl3ext.h b/security/nss/lib/ssl/ssl3ext.h
index c1bed29901..6176bd5c9e 100644
--- a/security/nss/lib/ssl/ssl3ext.h
+++ b/security/nss/lib/ssl/ssl3ext.h
@@ -30,16 +30,6 @@ typedef struct {
sslExtensionBuilderFunc ex_sender;
} sslExtensionBuilder;
-/* RFC 8879: TLS Certificate Compression - 3. Negotiating Certificate Compression
-** enum {
-** zlib(1),
-** brotli(2),
-** zstd(3),
-** (65535)
-** } CertificateCompressionAlgorithm;
-*/
-typedef PRUint16 SSLCertificateCompressionAlgorithmID;
-
struct TLSExtensionDataStr {
/* registered callbacks that send server hello extensions */
sslExtensionBuilder serverHelloSenders[SSL_MAX_EXTENSIONS];
diff --git a/security/nss/lib/ssl/sslexp.h b/security/nss/lib/ssl/sslexp.h
index b26afd9b17..b51d224d50 100644
--- a/security/nss/lib/ssl/sslexp.h
+++ b/security/nss/lib/ssl/sslexp.h
@@ -1079,10 +1079,10 @@ typedef struct SSLMaskingContextStr {
* The function SSL_SetCertificateCompressionAlgorithm() adds a certificate
* compression mechanism to the socket fd. */
-#define SSL_SetCertificateCompressionAlgorithm(fd, t) \
- SSL_EXPERIMENTAL_API("SSL_SetCertificateCompressionAlgorithm", \
- (PRFileDesc * _fd, \
- SSLCertificateCompressionAlgorithmType t), \
+#define SSL_SetCertificateCompressionAlgorithm(fd, t) \
+ SSL_EXPERIMENTAL_API("SSL_SetCertificateCompressionAlgorithm", \
+ (PRFileDesc * _fd, \
+ SSLCertificateCompressionAlgorithm t), \
(fd, t))
/* Deprecated experimental APIs */
diff --git a/security/nss/lib/ssl/sslimpl.h b/security/nss/lib/ssl/sslimpl.h
index 7a5757b6db..973a5db9f7 100644
--- a/security/nss/lib/ssl/sslimpl.h
+++ b/security/nss/lib/ssl/sslimpl.h
@@ -26,6 +26,8 @@
#include "pkcs11t.h"
#if defined(XP_UNIX)
#include "unistd.h"
+#elif defined(XP_WIN)
+#include <process.h>
#endif
#include "nssrwlk.h"
#include "prthread.h"
@@ -733,8 +735,8 @@ typedef struct SSL3HandshakeStateStr {
PRUint32 rtRetries; /* The retry counter */
SECItem srvVirtName; /* for server: name that was negotiated
- * with a client. For client - is
- * always set to NULL.*/
+ * with a client. For client - is
+ * always set to NULL.*/
/* This group of values is used for TLS 1.3 and above */
PK11SymKey *currentSecret; /* The secret down the "left hand side"
@@ -815,14 +817,6 @@ typedef struct SSL3HandshakeStateStr {
PORT_Assert(ss->ssl3.hs.messages.len == 0); \
PORT_Assert(ss->ssl3.hs.echInnerMessages.len == 0); \
} while (0)
-
-typedef struct SSLCertificateCompressionAlgorithmStr {
- SSLCertificateCompressionAlgorithmID id;
- const char *name;
- SECStatus (*encode)(const SECItem *input, SECItem *output);
- SECStatus (*decode)(const SECItem *input, SECItem *output, size_t expectedLenDecodedCertificate);
-} SSLCertificateCompressionAlgorithm;
-
/*
** This is the "ssl3" struct, as in "ss->ssl3".
** note:
@@ -2039,7 +2033,6 @@ SEC_END_PROTOS
#if defined(XP_UNIX) || defined(XP_OS2)
#define SSL_GETPID getpid
#elif defined(WIN32)
-extern int __cdecl _getpid(void);
#define SSL_GETPID _getpid
#else
#define SSL_GETPID() 0
diff --git a/security/nss/lib/ssl/sslsock.c b/security/nss/lib/ssl/sslsock.c
index 8f6c50c67c..befa4eda43 100644
--- a/security/nss/lib/ssl/sslsock.c
+++ b/security/nss/lib/ssl/sslsock.c
@@ -4376,6 +4376,7 @@ struct {
EXP(SetResumptionToken),
EXP(SetServerEchConfigs),
EXP(SetTimeFunc),
+ EXP(SetCertificateCompressionAlgorithm),
#endif
{ "", NULL }
};
diff --git a/security/nss/lib/ssl/sslt.h b/security/nss/lib/ssl/sslt.h
index 133ae6a296..d8927319c2 100644
--- a/security/nss/lib/ssl/sslt.h
+++ b/security/nss/lib/ssl/sslt.h
@@ -585,4 +585,21 @@ typedef enum {
ssl_dhe_group_max
} SSLDHEGroupType;
+/* RFC 8879: TLS Certificate Compression - 3. Negotiating Certificate Compression
+** enum {
+** zlib(1),
+** brotli(2),
+** zstd(3),
+** (65535)
+** } CertificateCompressionAlgorithm;
+*/
+typedef PRUint16 SSLCertificateCompressionAlgorithmID;
+
+typedef struct SSLCertificateCompressionAlgorithmStr {
+ SSLCertificateCompressionAlgorithmID id;
+ const char* name;
+ SECStatus (*encode)(const SECItem* input, SECItem* output);
+ SECStatus (*decode)(const SECItem* input, SECItem* output, size_t expectedLenDecodedCertificate);
+} SSLCertificateCompressionAlgorithm;
+
#endif /* __sslt_h_ */
diff --git a/security/nss/lib/util/nssutil.h b/security/nss/lib/util/nssutil.h
index b1a7c5fc59..d49a6890c1 100644
--- a/security/nss/lib/util/nssutil.h
+++ b/security/nss/lib/util/nssutil.h
@@ -19,9 +19,9 @@
* The format of the version string should be
* "<major version>.<minor version>[.<patch level>[.<build number>]][ <Beta>]"
*/
-#define NSSUTIL_VERSION "3.98"
+#define NSSUTIL_VERSION "3.99"
#define NSSUTIL_VMAJOR 3
-#define NSSUTIL_VMINOR 98
+#define NSSUTIL_VMINOR 99
#define NSSUTIL_VPATCH 0
#define NSSUTIL_VBUILD 0
#define NSSUTIL_BETA PR_FALSE
diff --git a/security/nss/lib/util/secoid.c b/security/nss/lib/util/secoid.c
index 800cc7ff62..05208eeffa 100644
--- a/security/nss/lib/util/secoid.c
+++ b/security/nss/lib/util/secoid.c
@@ -613,6 +613,22 @@ CONST_OID evIncorporationCountry[] = { EV_NAME_ATTRIBUTE, 3 };
*/
CONST_OID curve25519[] = { 0x2B, 0x06, 0x01, 0x04, 0x01, 0xDA, 0x47, 0x0F, 0x01 };
+/*
+ https://oid-rep.orange-labs.fr/get/1.3.101.112
+ A.1. ASN.1 Object for Ed25519
+ id-Ed25519 OBJECT IDENTIFIER ::= { 1.3.101.112 }
+ Parameters are absent. Length is 7 bytes.
+ Binary encoding: 3005 0603 2B65 70
+
+ The same algorithm identifiers are used for identifying a public key,
+ a private key, and a signature (for the two EdDSA related OIDs).
+ Additional encoding information is provided below for each of these
+ locations.
+*/
+
+CONST_OID ed25519PublicKey[] = { 0x2B, 0x65, 0x70 };
+CONST_OID ed25519Signature[] = { 0x2B, 0x65, 0x70 };
+
#define OI(x) \
{ \
siDEROID, (unsigned char *)x, sizeof x \
@@ -1819,6 +1835,13 @@ const static SECOidData oids[SEC_OID_TOTAL] = {
ODE(SEC_OID_XYBER768D00,
"X25519+Kyber768 key exchange", CKM_INVALID_MECHANISM, INVALID_CERT_EXTENSION),
+
+ OD(ed25519Signature, SEC_OID_ED25519_SIGNATURE, "X9.62 EDDSA signature", CKM_EDDSA,
+ INVALID_CERT_EXTENSION),
+
+ OD(ed25519PublicKey, SEC_OID_ED25519_PUBLIC_KEY,
+ "X9.62 elliptic edwards curve public key", CKM_EC_EDWARDS_KEY_PAIR_GEN, INVALID_CERT_EXTENSION),
+
};
/* PRIVATE EXTENDED SECOID Table
@@ -2133,10 +2156,9 @@ SECOID_Init(void)
for (i = 0; i < SEC_OID_TOTAL; i++) {
oid = &oids[i];
-
PORT_Assert(oid->offset == i);
-
entry = PL_HashTableAdd(oidhash, &oid->oid, (void *)oid);
+
if (entry == NULL) {
PORT_SetError(SEC_ERROR_LIBRARY_FAILURE);
PORT_Assert(0); /*This function should never fail. */
@@ -2196,7 +2218,6 @@ SECOID_FindOID(const SECItem *oid)
PORT_SetError(SEC_ERROR_UNRECOGNIZED_OID);
}
}
-
return (ret);
}
@@ -2206,8 +2227,9 @@ SECOID_FindOIDTag(const SECItem *oid)
SECOidData *oiddata;
oiddata = SECOID_FindOID(oid);
- if (oiddata == NULL)
+ if (oiddata == NULL) {
return SEC_OID_UNKNOWN;
+ }
return oiddata->offset;
}
diff --git a/security/nss/lib/util/secoidt.h b/security/nss/lib/util/secoidt.h
index 3ab0d6cc74..f2618d62cb 100644
--- a/security/nss/lib/util/secoidt.h
+++ b/security/nss/lib/util/secoidt.h
@@ -514,6 +514,9 @@ typedef enum {
SEC_OID_XYBER768D00 = 372,
+ SEC_OID_ED25519_SIGNATURE = 373,
+ SEC_OID_ED25519_PUBLIC_KEY = 374,
+
SEC_OID_TOTAL
} SECOidTag;