Rename mlk_keypair_getnoise() to mlk_keypair_getnoise_eta1()

Signed-off-by: Rod Chapman <rodchap@amazon.com>

Author: rod-chapman

mlkem/src/indcpa.c

@@ -39,7 +39,7 @@
   MLK_ADD_PARAM_SET(mlk_polyvec_permute_bitrev_to_custom)
 #define mlk_polymat_permute_bitrev_to_custom \
   MLK_ADD_PARAM_SET(mlk_polymat_permute_bitrev_to_custom)
-#define mlk_keypair_getnoise MLK_ADD_PARAM_SET(mlk_keypair_getnoise)
+#define mlk_keypair_getnoise_eta1 MLK_ADD_PARAM_SET(mlk_keypair_getnoise_eta1)
 /* End of parameter set namespacing */
 
 /*************************************************
@@ -367,10 +367,10 @@ __contract__(
 }
 
 /*************************************************
- * Name:        mlk_keypair_getnoise
+ * Name:        mlk_keypair_getnoise_eta1
  *
  * Description: Computes and fills the pv and e polyvec
- *              structures needed by mlk_keypair_derand()
+ *              structures needed by mlk_keypair_derand().
  *
  * Arguments:   - pv: Pointer to output polynomial vector
  *              - e:  Pointer to output polynomial vector
@@ -379,8 +379,8 @@ __contract__(
  * Specification: Implements @[FIPS203, Algorithm 13 (K-PKE.KeyGen)].
  *                steps 8 - 15
  **************************************************/
-static void mlk_keypair_getnoise(mlk_polyvec *pv, mlk_polyvec *e,
-                                 const uint8_t seed[MLKEM_SYMBYTES])
+static void mlk_keypair_getnoise_eta1(mlk_polyvec *pv, mlk_polyvec *e,
+                                      const uint8_t seed[MLKEM_SYMBYTES])
 __contract__(
   requires(memory_no_alias(pv, sizeof(mlk_polyvec)))
   requires(memory_no_alias(e, sizeof(mlk_polyvec)))
@@ -392,17 +392,19 @@ __contract__(
 )
 {
 #if MLKEM_K == 2
-  mlk_poly_getnoise_eta1_4x(&pv->vec[0], &pv->vec[1], &e->vec[0], &e->vec[1],
+  mlk_poly_getnoise_eta1_4x(&pv->vec[0], &pv->vec[1], /* Fill elements of pv */
+                            &e->vec[0], &e->vec[1], /* and two elements of e */
                             seed, 0, 1, 2, 3);
 #elif MLKEM_K == 3
   /*
-   * Only the first three output buffers are needed.
+   * Only the first three output buffers are needed, so we pass NULL as
+   * the fourth parameter, and 0xFF as its dummy nonce.
    */
   mlk_poly_getnoise_eta1_4x(&pv->vec[0], &pv->vec[1], &pv->vec[2], NULL, seed,
-                            0, 1, 2, 0xFF /* irrelevant */);
+                            0, 1, 2, 0xFF);
   /* Same here */
   mlk_poly_getnoise_eta1_4x(&e->vec[0], &e->vec[1], &e->vec[2], NULL, seed, 3,
-                            4, 5, 0xFF /* irrelevant */);
+                            4, 5, 0xFF);
 #elif MLKEM_K == 4
   mlk_poly_getnoise_eta1_4x(&pv->vec[0], &pv->vec[1], &pv->vec[2], &pv->vec[3],
                             seed, 0, 1, 2, 3);
@@ -463,7 +465,7 @@ int mlk_indcpa_keypair_derand(uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES],
 
   mlk_gen_matrix(a, publicseed, 0 /* no transpose */);
 
-  mlk_keypair_getnoise(skpv, e, noiseseed);
+  mlk_keypair_getnoise_eta1(skpv, e, noiseseed);
 
   mlk_polyvec_ntt(skpv);
   mlk_polyvec_ntt(e);
@@ -652,4 +654,4 @@ int mlk_indcpa_dec(uint8_t m[MLKEM_INDCPA_MSGBYTES],
 #undef mlk_matvec_mul
 #undef mlk_polyvec_permute_bitrev_to_custom
 #undef mlk_polymat_permute_bitrev_to_custom
-#undef mlk_keypair_getnoise
+#undef mlk_keypair_getnoise_eta1

proofs/cbmc/indcpa_keypair_derand/Makefile

@@ -23,7 +23,7 @@ CHECK_FUNCTION_CONTRACTS=mlk_indcpa_keypair_derand
 USE_FUNCTION_CONTRACTS = mlk_zeroize
 USE_FUNCTION_CONTRACTS += mlk_sha3_512
 USE_FUNCTION_CONTRACTS += mlk_gen_matrix
-USE_FUNCTION_CONTRACTS += mlk_keypair_getnoise
+USE_FUNCTION_CONTRACTS += mlk_keypair_getnoise_eta1
 USE_FUNCTION_CONTRACTS += mlk_polyvec_ntt
 USE_FUNCTION_CONTRACTS += mlk_polyvec_mulcache_compute
 USE_FUNCTION_CONTRACTS += mlk_matvec_mul

proofs/cbmc/keypair_getnoise/Makefile …oofs/cbmc/keypair_getnoise_eta1/Makefileproofs/cbmc/keypair_getnoise/Makefile renamed to proofs/cbmc/keypair_getnoise_eta1/Makefile proofs/cbmc/keypair_getnoise/Makefile renamed to proofs/cbmc/keypair_getnoise_eta1/Makefile

@@ -4,11 +4,11 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = keypair_getnoise_harness
+HARNESS_FILE = keypair_getnoise_eta1_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 = mlk_keypair_getnoise
+PROOF_UID = mlk_keypair_getnoise_eta1
 
 DEFINES +=
 INCLUDES +=
@@ -18,7 +18,7 @@ REMOVE_FUNCTION_BODY +=
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/src/indcpa.c
 
-CHECK_FUNCTION_CONTRACTS=mlk_keypair_getnoise
+CHECK_FUNCTION_CONTRACTS=mlk_keypair_getnoise_eta1
 USE_FUNCTION_CONTRACTS=mlk_poly_getnoise_eta1_4x
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
@@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--smt2 --slice-formula
 
-FUNCTION_NAME = mlk_keypair_getnoise
+FUNCTION_NAME = mlk_keypair_getnoise_eta1
 
 # If this proof is found to consume huge amounts of RAM, you can set the
 # EXPENSIVE variable. With new enough versions of the proof tools, this will

…pair_getnoise/keypair_getnoise_harness.c …ise_eta1/keypair_getnoise_eta1_harness.cproofs/cbmc/keypair_getnoise/keypair_getnoise_harness.c renamed to proofs/cbmc/keypair_getnoise_eta1/keypair_getnoise_eta1_harness.c proofs/cbmc/keypair_getnoise/keypair_getnoise_harness.c renamed to proofs/cbmc/keypair_getnoise_eta1/keypair_getnoise_eta1_harness.c

@@ -4,9 +4,9 @@
 
 #include <indcpa.h>
 
-#define mlk_keypair_getnoise MLK_NAMESPACE(keypair_getnoise)
-void mlk_keypair_getnoise(mlk_polyvec *pv, mlk_polyvec *e,
-                          const uint8_t seed[MLKEM_SYMBYTES]);
+#define mlk_keypair_getnoise_eta1 MLK_NAMESPACE(keypair_getnoise_eta1)
+void mlk_keypair_getnoise_eta1(mlk_polyvec *pv, mlk_polyvec *e,
+                               const uint8_t seed[MLKEM_SYMBYTES]);
 
 void harness(void)
 {
@@ -18,5 +18,5 @@ void harness(void)
     free(NULL);
   }
 
-  mlk_keypair_getnoise(a, b, seed);
+  mlk_keypair_getnoise_eta1(a, b, seed);
 }