Correct loop contracts to add decreases clauses

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

Author: rod-chapman

mlkem/src/poly_k.c

@@ -173,26 +173,27 @@ __contract__(
   for (i = 0; i < MLKEM_N / 2; i++)
   __loop__(
     invariant(i <= MLKEM_N / 2)
-    invariant(array_abs_bound(r->coeffs, 0, 2 * i, INT16_MAX/2)))
-    decreases(MLKEM_N / 2 - i))
-    {
-      unsigned k;
-      int32_t t[2] = {0};
-      for (k = 0; k < MLKEM_K; k++)
-      __loop__(
+    invariant(array_abs_bound(r->coeffs, 0, 2 * i, INT16_MAX/2))
+    decreases(MLKEM_N / 2 - i)
+  )
+  {
+    unsigned k;
+    int32_t t[2] = {0};
+    for (k = 0; k < MLKEM_K; k++)
+    __loop__(
       invariant(k <= MLKEM_K && i <= MLKEM_N / 2)
-      invariant(array_abs_bound(t, 0, 2, k * 2 * MLKEM_UINT12_LIMIT * MLK_NTT_BOUND + 1)))
-      decreases(MLKEM_K - k))
-      {
-        t[0] +=
-            (int32_t)a->vec[k].coeffs[2 * i + 1] * b_cache->vec[k].coeffs[i];
-        t[0] += (int32_t)a->vec[k].coeffs[2 * i] * b->vec[k].coeffs[2 * i];
-        t[1] += (int32_t)a->vec[k].coeffs[2 * i] * b->vec[k].coeffs[2 * i + 1];
-        t[1] += (int32_t)a->vec[k].coeffs[2 * i + 1] * b->vec[k].coeffs[2 * i];
-      }
-      r->coeffs[2 * i + 0] = mlk_montgomery_reduce(t[0]);
-      r->coeffs[2 * i + 1] = mlk_montgomery_reduce(t[1]);
+      invariant(array_abs_bound(t, 0, 2, k * 2 * MLKEM_UINT12_LIMIT * MLK_NTT_BOUND + 1))
+      decreases(MLKEM_K - k)
+    )
+    {
+      t[0] += (int32_t)a->vec[k].coeffs[2 * i + 1] * b_cache->vec[k].coeffs[i];
+      t[0] += (int32_t)a->vec[k].coeffs[2 * i] * b->vec[k].coeffs[2 * i];
+      t[1] += (int32_t)a->vec[k].coeffs[2 * i] * b->vec[k].coeffs[2 * i + 1];
+      t[1] += (int32_t)a->vec[k].coeffs[2 * i + 1] * b->vec[k].coeffs[2 * i];
     }
+    r->coeffs[2 * i + 0] = mlk_montgomery_reduce(t[0]);
+    r->coeffs[2 * i + 1] = mlk_montgomery_reduce(t[1]);
+  }
 }
 
 MLK_INTERNAL_API