Switches to use "unsigned" not "int" for all coefficient indexes.

Consistent with a similar change to the reference code on main branch.

Signed-off-by: Rod Chapman <[email protected]>

Author: rod-chapman

mlkem/ntt.c

@@ -121,8 +121,8 @@
 /* contracts, so it is "inlined for proof" by CBMC      */
 /* This allows CBMC to keep track of the ranges of the  */
 /* modified coefficients in the calling functions.      */
-static INLINE void ct_butterfly(int16_t r[MLKEM_N], const int coeff1_index,
-                                const int coeff2_index, const int16_t zeta)
+static INLINE void ct_butterfly(int16_t r[MLKEM_N], const unsigned coeff1_index,
+                                const unsigned coeff2_index, const int16_t zeta)
 {
   int16_t t1 = r[coeff1_index];
   int16_t t2 = fqmul(r[coeff2_index], zeta);
@@ -166,14 +166,14 @@ __contract__(
   {
     /* 8 coeffifient indexes, starting at element j */
     /* and increasing in strides of 32              */
-    const int ci0 = j;
-    const int ci1 = ci0 + 32;
-    const int ci2 = ci0 + 64;
-    const int ci3 = ci0 + 96;
-    const int ci4 = ci0 + 128;
-    const int ci5 = ci0 + 160;
-    const int ci6 = ci0 + 192;
-    const int ci7 = ci0 + 224;
+    const unsigned ci0 = j;
+    const unsigned ci1 = ci0 + 32;
+    const unsigned ci2 = ci0 + 64;
+    const unsigned ci3 = ci0 + 96;
+    const unsigned ci4 = ci0 + 128;
+    const unsigned ci5 = ci0 + 160;
+    const unsigned ci6 = ci0 + 192;
+    const unsigned ci7 = ci0 + 224;
 
     /* Layer 1 */
     ct_butterfly(r, ci0, ci4, l1zeta1);
@@ -226,10 +226,10 @@ __contract__(
   {
     /* 4 coeffifient indexes, starting at element j + start */
     /* and increasing in strides of 8                       */
-    const int ci1 = j + start;
-    const int ci2 = ci1 + 8;
-    const int ci3 = ci1 + 16;
-    const int ci4 = ci1 + 24;
+    const unsigned ci1 = j + start;
+    const unsigned ci2 = ci1 + 8;
+    const unsigned ci3 = ci1 + 16;
+    const unsigned ci4 = ci1 + 24;
 
     /* Layer 4 */
     ct_butterfly(r, ci1, ci3, z1);
@@ -286,8 +286,8 @@ __contract__(
     invariant(array_abs_bound(r,     start + 4, start + j + 4, NTT_BOUND7))
     invariant(array_abs_bound(r, start + j + 4,       MLKEM_N, NTT_BOUND6)))
   {
-    const int ci1 = j + start;
-    const int ci2 = ci1 + 4;
+    const unsigned ci1 = j + start;
+    const unsigned ci2 = ci1 + 4;
 
     ct_butterfly(r, ci1, ci2, zeta);
   }
@@ -325,10 +325,10 @@ __contract__(
   ensures (array_abs_bound(r, start + 4,   MLKEM_N, NTT_BOUND7)))
 {
   const int32_t zeta = (int32_t)layer7_zetas[zeta_index];
-  const unsigned int ci0 = start;
-  const unsigned int ci1 = ci0 + 1;
-  const unsigned int ci2 = ci0 + 2;
-  const unsigned int ci3 = ci0 + 3;
+  const unsigned ci0 = start;
+  const unsigned ci1 = ci0 + 1;
+  const unsigned ci2 = ci0 + 2;
+  const unsigned ci3 = ci0 + 3;
 
   ct_butterfly(r, ci0, ci2, zeta);
   ct_butterfly(r, ci1, ci3, zeta);
@@ -457,8 +457,8 @@ void poly_ntt(poly *p)
 /* Like ct_butterfly(), this functions is inlined       */
 /* for both compilation and proof.                      */
 static INLINE void gs_butterfly_reduce(int16_t r[MLKEM_N],
-                                       const int coeff1_index,
-                                       const int coeff2_index,
+                                       const unsigned coeff1_index,
+                                       const unsigned coeff2_index,
                                        const int16_t zeta)
 {
   const int16_t t1 = r[coeff1_index];
@@ -470,8 +470,8 @@ static INLINE void gs_butterfly_reduce(int16_t r[MLKEM_N],
 /* As gs_butterfly_reduce(), but does not reduce the */
 /* coefficient denoted by coeff1_index               */
 static INLINE void gs_butterfly_defer(int16_t r[MLKEM_N],
-                                      const int coeff1_index,
-                                      const int coeff2_index,
+                                      const unsigned coeff1_index,
+                                      const unsigned coeff2_index,
                                       const int16_t zeta)
 {
   const int16_t t1 = r[coeff1_index];
@@ -495,10 +495,10 @@ __contract__(
 )
 {
   const int32_t zeta = (int32_t)layer7_zetas[zeta_index];
-  const int ci0 = start;
-  const int ci1 = ci0 + 1;
-  const int ci2 = ci0 + 2;
-  const int ci3 = ci0 + 3;
+  const unsigned ci0 = start;
+  const unsigned ci1 = ci0 + 1;
+  const unsigned ci2 = ci0 + 2;
+  const unsigned ci3 = ci0 + 3;
 
   /* Invert and reduce all coefficients here the first time they */
   /* are read. This is efficient, and also means we can accept   */
@@ -547,14 +547,14 @@ __contract__(
 )
 {
   const int32_t zeta = (int32_t)layer6_zetas[zeta_index];
-  const int ci0 = start;
-  const int ci1 = ci0 + 1;
-  const int ci2 = ci0 + 2;
-  const int ci3 = ci0 + 3;
-  const int ci4 = ci0 + 4;
-  const int ci5 = ci0 + 5;
-  const int ci6 = ci0 + 6;
-  const int ci7 = ci0 + 7;
+  const unsigned ci0 = start;
+  const unsigned ci1 = ci0 + 1;
+  const unsigned ci2 = ci0 + 2;
+  const unsigned ci3 = ci0 + 3;
+  const unsigned ci4 = ci0 + 4;
+  const unsigned ci5 = ci0 + 5;
+  const unsigned ci6 = ci0 + 6;
+  const unsigned ci7 = ci0 + 7;
 
   /* Defer reduction of coefficients 0, 1, 2, and 3 here so they */
   /* are bounded to NTT_BOUND2 after Layer6                      */
@@ -618,10 +618,10 @@ __contract__(
     invariant(array_abs_bound(r,     start + 24, start + j + 24, NTT_BOUND1))
     invariant(array_abs_bound(r, start + j + 24,        MLKEM_N, NTT_BOUND2)))
   {
-    const int ci0 = j + start;
-    const int ci8 = ci0 + 8;
-    const int ci16 = ci0 + 16;
-    const int ci24 = ci0 + 24;
+    const unsigned ci0 = j + start;
+    const unsigned ci8 = ci0 + 8;
+    const unsigned ci16 = ci0 + 16;
+    const unsigned ci24 = ci0 + 24;
 
     /* Layer 5 - Defer reduction of coeffs 0 and 16 here */
     gs_butterfly_defer(r, ci0, ci8, l5zeta2);
@@ -675,14 +675,14 @@ __contract__(
     invariant(array_abs_bound(r,  j + 96,     128, NTT_BOUND1))
     invariant(array_abs_bound(r,     128, MLKEM_N, NTT_BOUND1)))
   {
-    const int ci0 = j + 0;
-    const int ci32 = j + 32;
-    const int ci64 = j + 64;
-    const int ci96 = j + 96;
-    const int ci128 = j + 128;
-    const int ci160 = j + 160;
-    const int ci192 = j + 192;
-    const int ci224 = j + 224;
+    const unsigned ci0 = j + 0;
+    const unsigned ci32 = j + 32;
+    const unsigned ci64 = j + 64;
+    const unsigned ci96 = j + 96;
+    const unsigned ci128 = j + 128;
+    const unsigned ci160 = j + 160;
+    const unsigned ci192 = j + 192;
+    const unsigned ci224 = j + 224;
 
     /* Layer 3 */
     gs_butterfly_defer(r, ci0, ci32, l3zeta7);