Re-format with clang-format and add decreases contract

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

Author: rod-chapman

mlkem/src/indcpa.c

@@ -195,20 +195,21 @@ __contract__(
     assigns(i, j, memory_slice(a, sizeof(mlk_polymat)))
     invariant(i <= MLKEM_K)
     invariant(forall(x2, 0, MLKEM_K, forall(y2, 0, MLKEM_K,
-      array_bound(a->vec[x2].vec[y2].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))))
+                                            array_bound(a->vec[x2].vec[y2].coeffs, 0, MLKEM_N, 0, MLKEM_Q))))
     decreases(MLKEM_K - i))
-    {
-      for (j = 0; j < MLKEM_K; j++)
-      __loop__(
+  {
+    for (j = 0; j < MLKEM_K; j++)
+    __loop__(
       assigns(j, memory_slice(a, sizeof(mlk_polymat)))
       invariant(i <= MLKEM_K)
       invariant(j <= MLKEM_K)
       invariant(forall(x3, 0, MLKEM_K, forall(y3, 0, MLKEM_K,
-                                              array_bound(a->vec[x3].vec[y3].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))))
-      {
-        mlk_poly_permute_bitrev_to_custom(a->vec[i].vec[j].coeffs);
-      }
+                                              array_bound(a->vec[x3].vec[y3].coeffs, 0, MLKEM_N, 0, MLKEM_Q))))
+      decreases(MLKEM_K - j))
+    {
+      mlk_poly_permute_bitrev_to_custom(a->vec[i].vec[j].coeffs);
     }
+  }
 #else  /* MLK_USE_NATIVE_NTT_CUSTOM_ORDER */
   /* Nothing to do */
   (void)a;