Hoist noise generation in encaps into separate helper

mlkem/src/indcpa.c

@@ -40,6 +40,7 @@
 #define mlk_polymat_permute_bitrev_to_custom \
   MLK_ADD_PARAM_SET(mlk_polymat_permute_bitrev_to_custom)
 #define mlk_keypair_getnoise_eta1 MLK_ADD_PARAM_SET(mlk_keypair_getnoise_eta1)
+#define mlk_enc_getnoise_eta1_eta2 MLK_ADD_PARAM_SET(mlk_enc_getnoise_eta1_eta2)
 /* End of parameter set namespacing */
 
 /*************************************************
@@ -371,6 +372,8 @@ __contract__(
  *
  * Description: Computes and fills the pv and e polyvec
  *              structures needed by mlk_keypair_derand().
+ *              Uses x4-batched versions of `poly_getnoise` to leverage
+ *              batched x4-batched Keccak-f1600.
  *
  * Arguments:   - pv: Pointer to output polynomial vector
  *              - e:  Pointer to output polynomial vector
@@ -413,10 +416,63 @@ __contract__(
 #endif /* MLKEM_K == 4 */
 }
 
+/*************************************************
+ * Name:        mlk_enc_getnoise_eta1_eta2
+ *
+ * Description: Computes and fills the sp, ep, and epp polynomial
+ *              structures needed by mlk_indcpa_enc().
+ *              Uses x4-batched versions of `poly_getnoise` to leverage
+ *              batched x4-batched Keccak-f1600.
+ *
+ * Arguments:   - sp:   Pointer to output polynomial vector
+ *              - ep:   Pointer to output polynomial vector
+ *              - epp:  Pointer to output polynomial
+ *              - coins: seed bytes for sampling
+ *
+ * Specification: Implements @[FIPS203, Algorithm 14 (K-PKE.Encrypt)].
+ *                steps 9 - 16
+ **************************************************/
+static void mlk_enc_getnoise_eta1_eta2(mlk_polyvec *sp, mlk_polyvec *ep,
+                                       mlk_poly *epp,
+                                       const uint8_t coins[MLKEM_SYMBYTES])
+__contract__(
+  requires(memory_no_alias(sp, sizeof(mlk_polyvec)))
+  requires(memory_no_alias(ep, sizeof(mlk_polyvec)))
+  requires(memory_no_alias(epp, sizeof(mlk_poly)))
+  requires(memory_no_alias(coins, MLKEM_SYMBYTES))
+  assigns(memory_slice(sp, sizeof(mlk_polyvec)))
+  assigns(memory_slice(ep, sizeof(mlk_polyvec)))
+  assigns(memory_slice(epp, sizeof(mlk_poly)))
+  ensures(forall(k0, 0, MLKEM_K, array_abs_bound(sp->vec[k0].coeffs, 0, MLKEM_N, MLKEM_ETA1 + 1)))
+  ensures(forall(k1, 0, MLKEM_K, array_abs_bound(ep->vec[k1].coeffs, 0, MLKEM_N, MLKEM_ETA2 + 1)))
+  ensures(array_abs_bound(epp->coeffs, 0, MLKEM_N, MLKEM_ETA2 + 1))
+)
+{
+#if MLKEM_K == 2
+  mlk_poly_getnoise_eta1122_4x(&sp->vec[0], &sp->vec[1], &ep->vec[0],
+                               &ep->vec[1], coins, 0, 1, 2, 3);
+  mlk_poly_getnoise_eta2(epp, coins, 4);
+#elif MLKEM_K == 3
+  /*
+   * In this call, only the first three output buffers are needed.
+   * The last parameter is a dummy that's overwritten later.
+   */
+  mlk_poly_getnoise_eta1_4x(&sp->vec[0], &sp->vec[1], &sp->vec[2], NULL, coins,
+                            0, 1, 2, 0xFF /* irrelevant */);
+  /* The fourth output buffer in this call _is_ used. */
+  mlk_poly_getnoise_eta2_4x(&ep->vec[0], &ep->vec[1], &ep->vec[2], epp, coins,
+                            3, 4, 5, 6);
+#elif MLKEM_K == 4
+  mlk_poly_getnoise_eta1_4x(&sp->vec[0], &sp->vec[1], &sp->vec[2], &sp->vec[3],
+                            coins, 0, 1, 2, 3);
+  mlk_poly_getnoise_eta2_4x(&ep->vec[0], &ep->vec[1], &ep->vec[2], &ep->vec[3],
+                            coins, 4, 5, 6, 7);
+  mlk_poly_getnoise_eta2(epp, coins, 8);
+#endif /* MLKEM_K == 4 */
+}
+
 
 /* Reference: `indcpa_keypair_derand()` in the reference implementation @[REF].
- *            - We use x4-batched versions of `poly_getnoise` to leverage
- *              batched x4-batched Keccak-f1600.
  *            - We use a different implementation of `gen_matrix()` which
  *              uses x4-batched Keccak-f1600 (see `mlk_gen_matrix()` above).
  *            - We use a mulcache to speed up matrix-vector multiplication.
@@ -541,27 +597,7 @@ int mlk_indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES],
 
   mlk_gen_matrix(at, seed, 1 /* transpose */);
 
-#if MLKEM_K == 2
-  mlk_poly_getnoise_eta1122_4x(&sp->vec[0], &sp->vec[1], &ep->vec[0],
-                               &ep->vec[1], coins, 0, 1, 2, 3);
-  mlk_poly_getnoise_eta2(epp, coins, 4);
-#elif MLKEM_K == 3
-  /*
-   * In this call, only the first three output buffers are needed.
-   * The last parameter is a dummy that's overwritten later.
-   */
-  mlk_poly_getnoise_eta1_4x(&sp->vec[0], &sp->vec[1], &sp->vec[2], NULL, coins,
-                            0, 1, 2, 0xFF /* irrelevant */);
-  /* The fourth output buffer in this call _is_ used. */
-  mlk_poly_getnoise_eta2_4x(&ep->vec[0], &ep->vec[1], &ep->vec[2], epp, coins,
-                            3, 4, 5, 6);
-#elif MLKEM_K == 4
-  mlk_poly_getnoise_eta1_4x(&sp->vec[0], &sp->vec[1], &sp->vec[2], &sp->vec[3],
-                            coins, 0, 1, 2, 3);
-  mlk_poly_getnoise_eta2_4x(&ep->vec[0], &ep->vec[1], &ep->vec[2], &ep->vec[3],
-                            coins, 4, 5, 6, 7);
-  mlk_poly_getnoise_eta2(epp, coins, 8);
-#endif /* MLKEM_K == 4 */
+  mlk_enc_getnoise_eta1_eta2(sp, ep, epp, coins);
 
   mlk_polyvec_ntt(sp);
 
@@ -655,3 +691,4 @@ int mlk_indcpa_dec(uint8_t m[MLKEM_INDCPA_MSGBYTES],
 #undef mlk_polyvec_permute_bitrev_to_custom
 #undef mlk_polymat_permute_bitrev_to_custom
 #undef mlk_keypair_getnoise_eta1
+#undef mlk_enc_getnoise_eta1_eta2

proofs/cbmc/enc_getnoise_eta1_eta2/Makefile

@@ -0,0 +1,66 @@
+# Copyright (c) The mlkem-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = enc_getnoise_eta1_eta2_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_enc_getnoise_eta1_eta2
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/src/indcpa.c
+
+CHECK_FUNCTION_CONTRACTS=mlk_enc_getnoise_eta1_eta2
+
+# Note that the called function mlk_poly_getnoise_eta2_4x() is actually
+# just #define'd to be mlk_poly_getnoise_eta1_4x()
+ifeq ($(MLKEM_K),2)
+USE_FUNCTION_CONTRACTS = mlk_poly_getnoise_eta1122_4x
+USE_FUNCTION_CONTRACTS += mlk_poly_getnoise_eta2
+else ifeq ($(MLKEM_K),3)
+USE_FUNCTION_CONTRACTS = mlk_poly_getnoise_eta1_4x
+else # MLKEM_K must be 4
+USE_FUNCTION_CONTRACTS = mlk_poly_getnoise_eta1_4x
+USE_FUNCTION_CONTRACTS += mlk_poly_getnoise_eta2
+endif
+
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--smt2 --slice-formula
+
+FUNCTION_NAME = mlk_enc_getnoise_eta1_eta2
+
+# 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
+# restrict the number of EXPENSIVE CBMC jobs running at once. See the
+# documentation in Makefile.common under the "Job Pools" heading for details.
+# EXPENSIVE = true
+
+# This function is large enough to need...
+CBMC_OBJECT_BITS = 10
+
+# If you require access to a file-local ("static") function or object to conduct
+# your proof, set the following (and do not include the original source file
+# ("mlkem/src/poly.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/src/poly.c
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
+# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
+# be set before including Makefile.common, but any use of variables on the
+# left-hand side requires those variables to be defined. Hence, _SOURCE,
+# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
+
+include ../Makefile.common

proofs/cbmc/enc_getnoise_eta1_eta2/enc_getnoise_eta1_eta2_harness.c

@@ -0,0 +1,23 @@
+// Copyright (c) The mlkem-native project authors
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: MIT-0
+
+#include <indcpa.h>
+
+#define mlk_enc_getnoise_eta1_eta2 MLK_NAMESPACE(enc_getnoise_eta1_eta2)
+void mlk_enc_getnoise_eta1_eta2(mlk_polyvec *sp, mlk_polyvec *ep, mlk_poly *epp,
+                                const uint8_t coins[MLKEM_SYMBYTES]);
+
+void harness(void)
+{
+  mlk_polyvec *sp, *ep;
+  mlk_poly *epp;
+  uint8_t *coins;
+
+  {
+    /* Dummy use of `free` to work around CBMC issue #8814. */
+    free(NULL);
+  }
+
+  mlk_enc_getnoise_eta1_eta2(sp, ep, epp, coins);
+}

proofs/cbmc/indcpa_enc/Makefile

@@ -22,15 +22,7 @@ PROJECT_SOURCES += $(SRCDIR)/mlkem/src/indcpa.c
 CHECK_FUNCTION_CONTRACTS=mlk_indcpa_enc
 USE_FUNCTION_CONTRACTS = mlk_poly_frommsg
 USE_FUNCTION_CONTRACTS += mlk_gen_matrix
-ifeq ($(MLKEM_K),2)
-USE_FUNCTION_CONTRACTS += mlk_poly_getnoise_eta1122_4x
-USE_FUNCTION_CONTRACTS += mlk_poly_getnoise_eta2
-else ifeq ($(MLKEM_K),3)
-USE_FUNCTION_CONTRACTS += mlk_poly_getnoise_eta1_4x
-else ifeq ($(MLKEM_K),4)
-USE_FUNCTION_CONTRACTS += mlk_poly_getnoise_eta1_4x
-USE_FUNCTION_CONTRACTS += mlk_poly_getnoise_eta2
-endif
+USE_FUNCTION_CONTRACTS += mlk_enc_getnoise_eta1_eta2
 
 USE_FUNCTION_CONTRACTS += mlk_polyvec_ntt
 USE_FUNCTION_CONTRACTS += mlk_polyvec_mulcache_compute