Simplify signature of mld_poly_uniform_eta_4x

mld_poly_uniform_eta_4x  before was taking 4 separate nonce values.
However, we were using only consecutive nonces in all call sites (except for
the irrelevant values - which were 0xFF).
This commit changes the function signature to take only a single nonce.

This aligns mld_poly_uniform_eta_4x with mld_poly_uniform_gamma1_4x which
was adjusted in the previous commit.

Signed-off-by: Matthias J. Kannwischer <[email protected]>

Author: mkannwischer

mldsa/poly.h

@@ -391,30 +391,31 @@ __contract__(
  *
  * Description: Sample four polynomials with uniformly random coefficients
  *              in [-MLDSA_ETA,MLDSA_ETA] by performing rejection sampling on
- *              the output stream from SHAKE256(seed|nonce_i)
+ *              the output streams of
+ *              SHAKE256(seed|nonce),
+ *              SHAKE256(seed|nonce + 1),
+ *              SHAKE256(seed|nonce + 2),
+ *              SHAKE256(seed|nonce + 3).
  *
  * Arguments:   - mld_poly *r0: pointer to first output polynomial
  *              - mld_poly *r1: pointer to second output polynomial
  *              - mld_poly *r2: pointer to third output polynomial
  *              - mld_poly *r3: pointer to fourth output polynomial
  *              - const uint8_t seed[]: byte array with seed of length
  *                MLDSA_CRHBYTES
- *              - uint8_t nonce0: first nonce
- *              - uint8_t nonce1: second nonce
- *              - uint8_t nonce2: third nonce
- *              - uint8_t nonce3: fourth nonce
+ *              - uint8_t nonce: 16-bit nonce
  **************************************************/
 MLD_INTERNAL_API
 void mld_poly_uniform_eta_4x(mld_poly *r0, mld_poly *r1, mld_poly *r2,
                              mld_poly *r3, const uint8_t seed[MLDSA_CRHBYTES],
-                             uint8_t nonce0, uint8_t nonce1, uint8_t nonce2,
-                             uint8_t nonce3)
+                             uint8_t nonce)
 __contract__(
   requires(memory_no_alias(r0, sizeof(mld_poly)))
   requires(memory_no_alias(r1, sizeof(mld_poly)))
   requires(memory_no_alias(r2, sizeof(mld_poly)))
   requires(memory_no_alias(r3, sizeof(mld_poly)))
   requires(memory_no_alias(seed, MLDSA_CRHBYTES))
+  requires(nonce <= UINT8_MAX - 3)
   assigns(memory_slice(r0, sizeof(mld_poly)))
   assigns(memory_slice(r1, sizeof(mld_poly)))
   assigns(memory_slice(r2, sizeof(mld_poly)))

mldsa/poly_kl.c

@@ -321,8 +321,7 @@ __contract__(
 MLD_INTERNAL_API
 void mld_poly_uniform_eta_4x(mld_poly *r0, mld_poly *r1, mld_poly *r2,
                              mld_poly *r3, const uint8_t seed[MLDSA_CRHBYTES],
-                             uint8_t nonce0, uint8_t nonce1, uint8_t nonce2,
-                             uint8_t nonce3)
+                             uint8_t nonce)
 {
   /* Temporary buffers for XOF output before rejection sampling */
   MLD_ALIGN uint8_t
@@ -339,10 +338,11 @@ void mld_poly_uniform_eta_4x(mld_poly *r0, mld_poly *r1, mld_poly *r2,
   mld_memcpy(extseed[1], seed, MLDSA_CRHBYTES);
   mld_memcpy(extseed[2], seed, MLDSA_CRHBYTES);
   mld_memcpy(extseed[3], seed, MLDSA_CRHBYTES);
-  extseed[0][MLDSA_CRHBYTES] = nonce0;
-  extseed[1][MLDSA_CRHBYTES] = nonce1;
-  extseed[2][MLDSA_CRHBYTES] = nonce2;
-  extseed[3][MLDSA_CRHBYTES] = nonce3;
+  /* Safety: Truncation is safe because nonce it at most 11 */
+  extseed[0][MLDSA_CRHBYTES] = nonce;
+  extseed[1][MLDSA_CRHBYTES] = (uint8_t)(nonce + 1);
+  extseed[2][MLDSA_CRHBYTES] = (uint8_t)(nonce + 2);
+  extseed[3][MLDSA_CRHBYTES] = (uint8_t)(nonce + 3);
   extseed[0][MLDSA_CRHBYTES + 1] = 0;
   extseed[1][MLDSA_CRHBYTES + 1] = 0;
   extseed[2][MLDSA_CRHBYTES + 1] = 0;

mldsa/sign.c

@@ -120,27 +120,25 @@ __contract__(
 /* Sample short vectors s1 and s2 */
 #if MLD_CONFIG_PARAMETER_SET == 44
   mld_poly_uniform_eta_4x(&s1->vec[0], &s1->vec[1], &s1->vec[2], &s1->vec[3],
-                          seed, 0, 1, 2, 3);
+                          seed, 0);
   mld_poly_uniform_eta_4x(&s2->vec[0], &s2->vec[1], &s2->vec[2], &s2->vec[3],
-                          seed, 4, 5, 6, 7);
+                          seed, 4);
 #elif MLD_CONFIG_PARAMETER_SET == 65
   mld_poly_uniform_eta_4x(&s1->vec[0], &s1->vec[1], &s1->vec[2], &s1->vec[3],
-                          seed, 0, 1, 2, 3);
+                          seed, 0);
   mld_poly_uniform_eta_4x(&s1->vec[4], &s2->vec[0], &s2->vec[1],
-                          &s2->vec[2] /* irrelevant */, seed, 4, 5, 6,
-                          0xFF /* irrelevant */);
+                          &s2->vec[2] /* irrelevant */, seed, 4);
   mld_poly_uniform_eta_4x(&s2->vec[2], &s2->vec[3], &s2->vec[4], &s2->vec[5],
-                          seed, 7, 8, 9, 10);
+                          seed, 7);
 #elif MLD_CONFIG_PARAMETER_SET == 87
   mld_poly_uniform_eta_4x(&s1->vec[0], &s1->vec[1], &s1->vec[2], &s1->vec[3],
-                          seed, 0, 1, 2, 3);
+                          seed, 0);
   mld_poly_uniform_eta_4x(&s1->vec[4], &s1->vec[5], &s1->vec[6],
-                          &s2->vec[0] /* irrelevant */, seed, 4, 5, 6,
-                          0xFF /* irrelevant */);
+                          &s2->vec[0] /* irrelevant */, seed, 4);
   mld_poly_uniform_eta_4x(&s2->vec[0], &s2->vec[1], &s2->vec[2], &s2->vec[3],
-                          seed, 7, 8, 9, 10);
+                          seed, 7);
   mld_poly_uniform_eta_4x(&s2->vec[4], &s2->vec[5], &s2->vec[6], &s2->vec[7],
-                          seed, 11, 12, 13, 14);
+                          seed, 11);
 #endif /* MLD_CONFIG_PARAMETER_SET == 87 */
 }
 

proofs/cbmc/poly_uniform_eta_4x/poly_uniform_eta_4x_harness.c

@@ -7,7 +7,7 @@ void harness(void)
 {
   mld_poly *r0, *r1, *r2, *r3;
   const uint8_t *seed;
-  uint8_t n0, n1, n2, n3;
+  uint8_t nonce;
 
-  mld_poly_uniform_eta_4x(r0, r1, r2, r3, seed, n0, n1, n2, n3);
+  mld_poly_uniform_eta_4x(r0, r1, r2, r3, seed, nonce);
 }