Correct contracts following rebase

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

Author: rod-chapman

mlkem/src/indcpa.c

@@ -353,20 +353,20 @@ __contract__(
     forall(k1, 0, MLKEM_K,
       array_bound(a->vec[k0].vec[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))))
   requires(forall(k1, 0, MLKEM_K,
-     array_abs_bound(v[k1].coeffs, 0, MLKEM_N, MLK_NTT_BOUND)))
+     array_abs_bound(v->vec[k1].coeffs, 0, MLKEM_N, MLK_NTT_BOUND)))
   requires(forall(k2, 0, MLKEM_K,
-     array_abs_bound(vc[k2].coeffs, 0, MLKEM_N/2, MLKEM_Q)))
+     array_abs_bound(vc->vec[k2].coeffs, 0, MLKEM_N/2, MLKEM_Q)))
   assigns(object_whole(out))
   ensures(forall(k3, 0, MLKEM_K,
-    array_abs_bound(out[k3].coeffs, 0, MLKEM_N, INT16_MAX/2))))
+    array_abs_bound(out->vec[k3].coeffs, 0, MLKEM_N, INT16_MAX/2))))
 {
   unsigned i;
   for (i = 0; i < MLKEM_K; i++)
   __loop__(
     assigns(i, object_whole(out))
     invariant(i <= MLKEM_K)
     invariant(forall(k, 0, i,
-                     array_abs_bound(out[k].coeffs, 0, MLKEM_N, INT16_MAX/2)))
+                     array_abs_bound(out->vec[k].coeffs, 0, MLKEM_N, INT16_MAX/2)))
   )
   {
     mlk_polyvec_basemul_acc_montgomery_cached(&out->vec[i], &a->vec[i], v, vc);

mlkem/src/poly_k.c

@@ -156,9 +156,9 @@ __contract__(
   requires(forall(k1, 0, MLKEM_K,
      array_bound(a->vec[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
   requires(forall(k2, 0, MLKEM_K,
-     array_abs_bound(b[k2].coeffs, 0, MLKEM_N, MLK_NTT_BOUND)))
+     array_abs_bound(b->vec[k2].coeffs, 0, MLKEM_N, MLK_NTT_BOUND)))
   requires(forall(k3, 0, MLKEM_K,
-     array_abs_bound(b_cache[k3].coeffs, 0, MLKEM_N/2, MLKEM_Q)))
+     array_abs_bound(b_cache->vec[k3].coeffs, 0, MLKEM_N/2, MLKEM_Q)))
   assigns(memory_slice(r, sizeof(mlk_poly)))
   ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, INT16_MAX/2))
 )

mlkem/src/poly_k.h

@@ -406,9 +406,9 @@ __contract__(
   requires(forall(k1, 0, MLKEM_K,
      array_bound(a->vec[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
   requires(forall(k2, 0, MLKEM_K,
-     array_abs_bound(b[k2].coeffs, 0, MLKEM_N, MLK_NTT_BOUND)))
+     array_abs_bound(b->vec[k2].coeffs, 0, MLKEM_N, MLK_NTT_BOUND)))
   requires(forall(k3, 0, MLKEM_K,
-     array_abs_bound(b_cache[k3].coeffs, 0, MLKEM_N/2, MLKEM_Q)))
+     array_abs_bound(b_cache->vec[k3].coeffs, 0, MLKEM_N/2, MLKEM_Q)))
   assigns(memory_slice(r, sizeof(mlk_poly)))
   ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, INT16_MAX/2))
 );
@@ -451,7 +451,7 @@ __contract__(
   requires(memory_no_alias(a, sizeof(mlk_polyvec)))
   assigns(memory_slice(x, sizeof(mlk_polyvec_mulcache)))
   ensures(forall(k0, 0, MLKEM_K,
-    array_abs_bound(x[k0].coeffs, 0, MLKEM_N/2, MLKEM_Q)))
+    array_abs_bound(x->vec[k0].coeffs, 0, MLKEM_N/2, MLKEM_Q)))
 );
 
 #define mlk_polyvec_reduce MLK_NAMESPACE_K(polyvec_reduce)