Remove SUPERCOP API from kem.[ch]

mlkem/mlkem_native.S

@@ -205,15 +205,14 @@
 #undef mlk_indcpa_enc
 #undef mlk_indcpa_keypair_derand
 /* mlkem/src/kem.h */
-#undef MLK_CONFIG_NO_SUPERCOP
 #undef MLK_KEM_H
-#undef crypto_kem_check_pk
-#undef crypto_kem_check_sk
-#undef crypto_kem_dec
-#undef crypto_kem_enc
-#undef crypto_kem_enc_derand
-#undef crypto_kem_keypair
-#undef crypto_kem_keypair_derand
+#undef mlk_kem_check_pk
+#undef mlk_kem_check_sk
+#undef mlk_kem_dec
+#undef mlk_kem_enc
+#undef mlk_kem_enc_derand
+#undef mlk_kem_keypair
+#undef mlk_kem_keypair_derand
 /* mlkem/src/params.h */
 #undef MLKEM_DU
 #undef MLKEM_DV

mlkem/mlkem_native.c

@@ -194,15 +194,14 @@
 #undef mlk_indcpa_enc
 #undef mlk_indcpa_keypair_derand
 /* mlkem/src/kem.h */
-#undef MLK_CONFIG_NO_SUPERCOP
 #undef MLK_KEM_H
-#undef crypto_kem_check_pk
-#undef crypto_kem_check_sk
-#undef crypto_kem_dec
-#undef crypto_kem_enc
-#undef crypto_kem_enc_derand
-#undef crypto_kem_keypair
-#undef crypto_kem_keypair_derand
+#undef mlk_kem_check_pk
+#undef mlk_kem_check_sk
+#undef mlk_kem_dec
+#undef mlk_kem_enc
+#undef mlk_kem_enc_derand
+#undef mlk_kem_keypair
+#undef mlk_kem_keypair_derand
 /* mlkem/src/params.h */
 #undef MLKEM_DU
 #undef MLKEM_DV

mlkem/src/kem.c

@@ -41,7 +41,7 @@
 /* Reference: Not implemented in the reference implementation @[REF]. */
 MLK_EXTERNAL_API
 MLK_MUST_CHECK_RETURN_VALUE
-int crypto_kem_check_pk(const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES])
+int mlk_kem_check_pk(const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES])
 {
   typedef struct
   {
@@ -78,7 +78,7 @@ int crypto_kem_check_pk(const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES])
 /* Reference: Not implemented in the reference implementation @[REF]. */
 MLK_EXTERNAL_API
 MLK_MUST_CHECK_RETURN_VALUE
-int crypto_kem_check_sk(const uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES])
+int mlk_kem_check_sk(const uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES])
 {
   int ret = 0;
   MLK_ALLOC(test, uint8_t, MLKEM_SYMBYTES);
@@ -154,13 +154,13 @@ static int mlk_check_pct(uint8_t const pk[MLKEM_INDCCA_PUBLICKEYBYTES],
     goto cleanup;
   }
 
-  ret = crypto_kem_enc(ws->ct, ws->ss_enc, pk);
+  ret = mlk_kem_enc(ws->ct, ws->ss_enc, pk);
   if (ret != 0)
   {
     goto cleanup;
   }
 
-  ret = crypto_kem_dec(ws->ss_dec, ws->ct, sk);
+  ret = mlk_kem_dec(ws->ss_dec, ws->ct, sk);
   if (ret != 0)
   {
     goto cleanup;
@@ -208,9 +208,9 @@ static int mlk_check_pct(uint8_t const pk[MLKEM_INDCCA_PUBLICKEYBYTES],
  *            - We optionally include PCT which is not present in
  *              the reference code. */
 MLK_EXTERNAL_API
-int crypto_kem_keypair_derand(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
-                              uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES],
-                              const uint8_t coins[2 * MLKEM_SYMBYTES])
+int mlk_kem_keypair_derand(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
+                           uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES],
+                           const uint8_t coins[2 * MLKEM_SYMBYTES])
 {
   int ret;
 
@@ -244,8 +244,8 @@ int crypto_kem_keypair_derand(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
 /* Reference: `crypto_kem_keypair()` in the reference implementation @[REF]
  *            - We zeroize the stack buffer */
 MLK_EXTERNAL_API
-int crypto_kem_keypair(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
-                       uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES])
+int mlk_kem_keypair(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
+                    uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES])
 {
   int ret = 0;
   MLK_ALLOC(coins, uint8_t, 2 * MLKEM_SYMBYTES);
@@ -260,7 +260,7 @@ int crypto_kem_keypair(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
   mlk_randombytes(coins, 2 * MLKEM_SYMBYTES);
   MLK_CT_TESTING_SECRET(coins, 2 * MLKEM_SYMBYTES);
 
-  ret = crypto_kem_keypair_derand(pk, sk, coins);
+  ret = mlk_kem_keypair_derand(pk, sk, coins);
 
 cleanup:
   /* Specification: Partially implements
@@ -274,10 +274,10 @@ int crypto_kem_keypair(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
  *            - We include public key check
  *            - We include stack buffer zeroization */
 MLK_EXTERNAL_API
-int crypto_kem_enc_derand(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
-                          uint8_t ss[MLKEM_SSBYTES],
-                          const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
-                          const uint8_t coins[MLKEM_SYMBYTES])
+int mlk_kem_enc_derand(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
+                       uint8_t ss[MLKEM_SSBYTES],
+                       const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
+                       const uint8_t coins[MLKEM_SYMBYTES])
 {
   typedef struct
   {
@@ -295,7 +295,7 @@ int crypto_kem_enc_derand(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
   }
 
   /* Specification: Implements @[FIPS203, Section 7.2, Modulus check] */
-  ret = crypto_kem_check_pk(pk);
+  ret = mlk_kem_check_pk(pk);
   if (ret != 0)
   {
     goto cleanup;
@@ -327,9 +327,9 @@ int crypto_kem_enc_derand(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
 /* Reference: `crypto_kem_enc()` in the reference implementation @[REF]
  *            - We include stack buffer zeroization */
 MLK_EXTERNAL_API
-int crypto_kem_enc(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
-                   uint8_t ss[MLKEM_SSBYTES],
-                   const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES])
+int mlk_kem_enc(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
+                uint8_t ss[MLKEM_SSBYTES],
+                const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES])
 {
   int ret = 0;
   MLK_ALLOC(coins, uint8_t, MLKEM_SYMBYTES);
@@ -343,7 +343,7 @@ int crypto_kem_enc(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
   mlk_randombytes(coins, MLKEM_SYMBYTES);
   MLK_CT_TESTING_SECRET(coins, MLKEM_SYMBYTES);
 
-  ret = crypto_kem_enc_derand(ct, ss, pk, coins);
+  ret = mlk_kem_enc_derand(ct, ss, pk, coins);
 
 cleanup:
   /* Specification: Partially implements
@@ -357,9 +357,9 @@ int crypto_kem_enc(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
  *            - We include secret key check
  *            - We include stack buffer zeroization */
 MLK_EXTERNAL_API
-int crypto_kem_dec(uint8_t ss[MLKEM_SSBYTES],
-                   const uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
-                   const uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES])
+int mlk_kem_dec(uint8_t ss[MLKEM_SSBYTES],
+                const uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
+                const uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES])
 {
   typedef struct
   {
@@ -380,7 +380,7 @@ int crypto_kem_dec(uint8_t ss[MLKEM_SSBYTES],
   }
 
   /* Specification: Implements @[FIPS203, Section 7.3, Hash check] */
-  ret = crypto_kem_check_sk(sk);
+  ret = mlk_kem_check_sk(sk);
   if (ret != 0)
   {
     goto cleanup;

mlkem/src/kem.h

@@ -28,9 +28,7 @@
 #if defined(MLK_CHECK_APIS)
 /* Include to ensure consistency between internal kem.h
  * and external mlkem_native.h. */
-#define MLK_CONFIG_NO_SUPERCOP
 #include "mlkem_native.h"
-#undef MLK_CONFIG_NO_SUPERCOP
 
 #if MLKEM_INDCCA_SECRETKEYBYTES != \
     MLKEM_SECRETKEYBYTES(MLK_CONFIG_PARAMETER_SET)
@@ -49,18 +47,16 @@
 
 #endif /* MLK_CHECK_APIS */
 
-#define crypto_kem_keypair_derand MLK_NAMESPACE_K(keypair_derand)
-#define crypto_kem_keypair MLK_NAMESPACE_K(keypair)
-#define crypto_kem_enc_derand MLK_NAMESPACE_K(enc_derand)
-#define crypto_kem_enc MLK_NAMESPACE_K(enc)
-#define crypto_kem_dec MLK_NAMESPACE_K(dec)
-#define crypto_kem_check_pk MLK_NAMESPACE_K(check_pk)
-#define crypto_kem_check_sk MLK_NAMESPACE_K(check_sk)
-
-
+#define mlk_kem_keypair_derand MLK_NAMESPACE_K(keypair_derand)
+#define mlk_kem_keypair MLK_NAMESPACE_K(keypair)
+#define mlk_kem_enc_derand MLK_NAMESPACE_K(enc_derand)
+#define mlk_kem_enc MLK_NAMESPACE_K(enc)
+#define mlk_kem_dec MLK_NAMESPACE_K(dec)
+#define mlk_kem_check_pk MLK_NAMESPACE_K(check_pk)
+#define mlk_kem_check_sk MLK_NAMESPACE_K(check_sk)
 
 /*************************************************
- * Name:        crypto_kem_check_pk
+ * Name:        mlk_kem_check_pk
  *
  * Description: Implements modulus check mandated by FIPS 203,
  *              i.e., ensures that coefficients are in [0,q-1].
@@ -81,7 +77,7 @@
 /* Reference: Not implemented in the reference implementation @[REF]. */
 MLK_EXTERNAL_API
 MLK_MUST_CHECK_RETURN_VALUE
-int crypto_kem_check_pk(const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES])
+int mlk_kem_check_pk(const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES])
 __contract__(
   requires(memory_no_alias(pk, MLKEM_INDCCA_PUBLICKEYBYTES))
   ensures(return_value == 0 || return_value == MLK_ERR_FAIL ||
@@ -90,7 +86,7 @@ __contract__(
 
 
 /*************************************************
- * Name:        crypto_kem_check_sk
+ * Name:        mlk_kem_check_sk
  *
  * Description: Implements public key hash check mandated by FIPS 203,
  *              i.e., ensures that
@@ -112,15 +108,15 @@ __contract__(
 /* Reference: Not implemented in the reference implementation @[REF]. */
 MLK_EXTERNAL_API
 MLK_MUST_CHECK_RETURN_VALUE
-int crypto_kem_check_sk(const uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES])
+int mlk_kem_check_sk(const uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES])
 __contract__(
   requires(memory_no_alias(sk, MLKEM_INDCCA_SECRETKEYBYTES))
   ensures(return_value == 0 || return_value == MLK_ERR_FAIL ||
           return_value == MLK_ERR_OUT_OF_MEMORY)
 );
 
 /*************************************************
- * Name:        crypto_kem_keypair_derand
+ * Name:        mlk_kem_keypair_derand
  *
  * Description: Generates public and private key
  *              for CCA-secure ML-KEM key encapsulation mechanism
@@ -146,9 +142,9 @@ __contract__(
  **************************************************/
 MLK_EXTERNAL_API
 MLK_MUST_CHECK_RETURN_VALUE
-int crypto_kem_keypair_derand(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
-                              uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES],
-                              const uint8_t coins[2 * MLKEM_SYMBYTES])
+int mlk_kem_keypair_derand(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
+                           uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES],
+                           const uint8_t coins[2 * MLKEM_SYMBYTES])
 __contract__(
   requires(memory_no_alias(pk, MLKEM_INDCCA_PUBLICKEYBYTES))
   requires(memory_no_alias(sk, MLKEM_INDCCA_SECRETKEYBYTES))
@@ -160,7 +156,7 @@ __contract__(
 );
 
 /*************************************************
- * Name:        crypto_kem_keypair
+ * Name:        mlk_kem_keypair
  *
  * Description: Generates public and private key
  *              for CCA-secure ML-KEM key encapsulation mechanism
@@ -183,8 +179,8 @@ __contract__(
  **************************************************/
 MLK_EXTERNAL_API
 MLK_MUST_CHECK_RETURN_VALUE
-int crypto_kem_keypair(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
-                       uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES])
+int mlk_kem_keypair(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
+                    uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES])
 __contract__(
   requires(memory_no_alias(pk, MLKEM_INDCCA_PUBLICKEYBYTES))
   requires(memory_no_alias(sk, MLKEM_INDCCA_SECRETKEYBYTES))
@@ -195,7 +191,7 @@ __contract__(
 );
 
 /*************************************************
- * Name:        crypto_kem_enc_derand
+ * Name:        mlk_kem_enc_derand
  *
  * Description: Generates cipher text and shared
  *              secret for given public key
@@ -223,10 +219,10 @@ __contract__(
  **************************************************/
 MLK_EXTERNAL_API
 MLK_MUST_CHECK_RETURN_VALUE
-int crypto_kem_enc_derand(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
-                          uint8_t ss[MLKEM_SSBYTES],
-                          const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
-                          const uint8_t coins[MLKEM_SYMBYTES])
+int mlk_kem_enc_derand(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
+                       uint8_t ss[MLKEM_SSBYTES],
+                       const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
+                       const uint8_t coins[MLKEM_SYMBYTES])
 __contract__(
   requires(memory_no_alias(ct, MLKEM_INDCCA_CIPHERTEXTBYTES))
   requires(memory_no_alias(ss, MLKEM_SSBYTES))
@@ -239,7 +235,7 @@ __contract__(
 );
 
 /*************************************************
- * Name:        crypto_kem_enc
+ * Name:        mlk_kem_enc
  *
  * Description: Generates cipher text and shared
  *              secret for given public key
@@ -264,9 +260,9 @@ __contract__(
  **************************************************/
 MLK_EXTERNAL_API
 MLK_MUST_CHECK_RETURN_VALUE
-int crypto_kem_enc(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
-                   uint8_t ss[MLKEM_SSBYTES],
-                   const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES])
+int mlk_kem_enc(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
+                uint8_t ss[MLKEM_SSBYTES],
+                const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES])
 __contract__(
   requires(memory_no_alias(ct, MLKEM_INDCCA_CIPHERTEXTBYTES))
   requires(memory_no_alias(ss, MLKEM_SSBYTES))
@@ -278,7 +274,7 @@ __contract__(
 );
 
 /*************************************************
- * Name:        crypto_kem_dec
+ * Name:        mlk_kem_dec
  *
  * Description: Generates shared secret for given
  *              cipher text and private key
@@ -303,9 +299,9 @@ __contract__(
  **************************************************/
 MLK_EXTERNAL_API
 MLK_MUST_CHECK_RETURN_VALUE
-int crypto_kem_dec(uint8_t ss[MLKEM_SSBYTES],
-                   const uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
-                   const uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES])
+int mlk_kem_dec(uint8_t ss[MLKEM_SSBYTES],
+                const uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
+                const uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES])
 __contract__(
   requires(memory_no_alias(ss, MLKEM_SSBYTES))
   requires(memory_no_alias(ct, MLKEM_INDCCA_CIPHERTEXTBYTES))

proofs/cbmc/crypto_kem_check_pk/Makefile → proofs/cbmc/kem_check_pk/Makefile

@@ -4,11 +4,11 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = crypto_kem_check_pk_harness
+HARNESS_FILE = kem_check_pk_harness
 
 # This should be a unique identifier for this proof, and will appear on the
 # Litani dashboard. It can be human-readable and contain spaces if you wish.
-PROOF_UID = crypto_kem_check_pk
+PROOF_UID = kem_check_pk
 
 DEFINES +=
 INCLUDES +=

proofs/cbmc/crypto_kem_check_pk/crypto_kem_check_pk_harness.c → proofs/cbmc/kem_check_pk/kem_check_pk_harness.c

@@ -7,5 +7,5 @@
 void harness(void)
 {
   uint8_t *a;
-  crypto_kem_check_pk(a);
+  mlk_kem_check_pk(a);
 }

proofs/cbmc/crypto_kem_check_sk/Makefile → proofs/cbmc/kem_check_sk/Makefile

@@ -4,11 +4,11 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = crypto_kem_check_sk_harness
+HARNESS_FILE = kem_check_sk_harness
 
 # This should be a unique identifier for this proof, and will appear on the
 # Litani dashboard. It can be human-readable and contain spaces if you wish.
-PROOF_UID = crypto_kem_check_sk
+PROOF_UID = kem_check_sk
 
 DEFINES +=
 INCLUDES +=

proofs/cbmc/crypto_kem_check_sk/crypto_kem_check_sk_harness.c → proofs/cbmc/kem_check_sk/kem_check_sk_harness.c

@@ -7,5 +7,5 @@
 void harness(void)
 {
   uint8_t *a;
-  crypto_kem_check_sk(a);
+  mlk_kem_check_sk(a);
 }