CBMC: Improve performance of polyvec_basemul_acc_montgomery proof

Signed-off-by: Hanno Becker <[email protected]>

Author: hanno-becker

mlkem/poly_k.c

@@ -138,22 +138,19 @@ void mlk_polyvec_basemul_acc_montgomery_cached(
     invariant(array_abs_bound(r->coeffs, 0, 2 * i, INT16_MAX/2)))
   {
     unsigned k;
-    int32_t t0 = 0, t1 = 0;
+    int32_t t[2] = {0};
     for (k = 0; k < MLKEM_K; k++)
     __loop__(
-      invariant(k <= MLKEM_K && i <= MLKEM_N / 2 &&
-         t0 <=   ((int32_t) k * 2 * MLKEM_UINT12_LIMIT * MLK_NTT_BOUND) &&
-	 t0 >= - ((int32_t) k * 2 * MLKEM_UINT12_LIMIT * MLK_NTT_BOUND) &&
-         t1 <=   ((int32_t) k * 2 * MLKEM_UINT12_LIMIT * MLK_NTT_BOUND) &&
-         t1 >= - ((int32_t) k * 2 * MLKEM_UINT12_LIMIT * MLK_NTT_BOUND)))
+      invariant(k <= MLKEM_K && i <= MLKEM_N / 2)
+      invariant(array_abs_bound(t, 0, 2, k * 2 * MLKEM_UINT12_LIMIT * MLK_NTT_BOUND + 1)))
     {
-      t0 += (int32_t)a->vec[k].coeffs[2 * i + 1] * b_cache->vec[k].coeffs[i];
-      t0 += (int32_t)a->vec[k].coeffs[2 * i] * b->vec[k].coeffs[2 * i];
-      t1 += (int32_t)a->vec[k].coeffs[2 * i] * b->vec[k].coeffs[2 * i + 1];
-      t1 += (int32_t)a->vec[k].coeffs[2 * i + 1] * b->vec[k].coeffs[2 * i];
+      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(t0);
-    r->coeffs[2 * i + 1] = mlk_montgomery_reduce(t1);
+    r->coeffs[2 * i + 0] = mlk_montgomery_reduce(t[0]);
+    r->coeffs[2 * i + 1] = mlk_montgomery_reduce(t[1]);
   }
 }