diff --git a/mlkem/cbd.c b/mlkem/cbd.c
index d72b17cc8..231b4943c 100644
--- a/mlkem/cbd.c
+++ b/mlkem/cbd.c
@@ -61,7 +61,7 @@ static void cbd2(poly *r, const uint8_t buf[2 * MLKEM_N / 4]) {
   for (i = 0; i < MLKEM_N / 8; i++)  // clang-format off
     ASSIGNS(i, j, a, b, t, d, OBJECT_WHOLE(r))
     INVARIANT(i >= 0 && i <= MLKEM_N / 8)
-    INVARIANT(ARRAY_IN_BOUNDS(int, k, 0, (8 * i - 1), r->coeffs, -2, +2))  // clang-format on
+    INVARIANT(ARRAY_IN_BOUNDS(0, (8 * i - 1), r->coeffs, -2, +2))  // clang-format on
     {
       t = load32_littleendian(buf + 4 * i);
       d = t & 0x55555555;
@@ -70,7 +70,7 @@ static void cbd2(poly *r, const uint8_t buf[2 * MLKEM_N / 4]) {
       for (j = 0; j < 8; j++)  // clang-format off
         ASSIGNS(j, a, b, OBJECT_WHOLE(r))
         INVARIANT(i >= 0 && i <= MLKEM_N / 8 && j >= 0 && j <= 8)
-        INVARIANT(ARRAY_IN_BOUNDS(int, k, 0, 8 * i + j - 1, r->coeffs, -2, +2))  // clang-format on
+        INVARIANT(ARRAY_IN_BOUNDS(0, 8 * i + j - 1, r->coeffs, -2, +2))  // clang-format on
         {
           a = (d >> (4 * j + 0)) & 0x3;
           b = (d >> (4 * j + 2)) & 0x3;
@@ -99,7 +99,7 @@ static void cbd3(poly *r, const uint8_t buf[3 * MLKEM_N / 4]) {
   for (i = 0; i < MLKEM_N / 4; i++)  // clang-format off
     ASSIGNS(i, j, a, b, t, d, OBJECT_WHOLE(r))
     INVARIANT(i >= 0 && i <= MLKEM_N / 4)
-    INVARIANT(ARRAY_IN_BOUNDS(int, k, 0, (4 * i - 1), r->coeffs, -3, +3))  // clang-format on
+    INVARIANT(ARRAY_IN_BOUNDS(0, (4 * i - 1), r->coeffs, -3, +3))  // clang-format on
     {
       t = load24_littleendian(buf + 3 * i);
       d = t & 0x00249249;
@@ -109,7 +109,7 @@ static void cbd3(poly *r, const uint8_t buf[3 * MLKEM_N / 4]) {
       for (j = 0; j < 4; j++)  // clang-format off
         ASSIGNS(j, a, b, OBJECT_WHOLE(r))
         INVARIANT(i >= 0 && i <= MLKEM_N / 4 && j >= 0 && j <= 4)
-        INVARIANT(ARRAY_IN_BOUNDS(int, k, 0, 4 * i + j - 1, r->coeffs, -3, +3))  // clang-format on
+        INVARIANT(ARRAY_IN_BOUNDS(0, 4 * i + j - 1, r->coeffs, -3, +3))  // clang-format on
         {
           a = (d >> (6 * j + 0)) & 0x7;
           b = (d >> (6 * j + 3)) & 0x7;
diff --git a/mlkem/cbd.h b/mlkem/cbd.h
index fdca3e694..4148481c0 100644
--- a/mlkem/cbd.h
+++ b/mlkem/cbd.h
@@ -23,7 +23,7 @@ void poly_cbd_eta1(
 REQUIRES(IS_FRESH(r, sizeof(poly)))
 REQUIRES(IS_FRESH(buf, MLKEM_ETA1 * MLKEM_N / 4))
 ASSIGNS(OBJECT_UPTO(r, sizeof(poly)))
-ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, -MLKEM_ETA1, MLKEM_ETA1));
+ENSURES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r->coeffs, -MLKEM_ETA1, MLKEM_ETA1));
 // clang-format on
 
 #define poly_cbd_eta2 MLKEM_NAMESPACE(poly_cbd_eta2)
@@ -43,7 +43,7 @@ void poly_cbd_eta2(
 REQUIRES(IS_FRESH(r, sizeof(poly)))
 REQUIRES(IS_FRESH(buf, MLKEM_ETA2 * MLKEM_N / 4))
 ASSIGNS(OBJECT_UPTO(r, sizeof(poly)))
-ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, -MLKEM_ETA2, MLKEM_ETA2));
+ENSURES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r->coeffs, -MLKEM_ETA2, MLKEM_ETA2));
 // clang-format on
 
 #endif
diff --git a/mlkem/cbmc.h b/mlkem/cbmc.h
index 2ed331801..c43c1bef6 100644
--- a/mlkem/cbmc.h
+++ b/mlkem/cbmc.h
@@ -107,15 +107,18 @@
 // range value_lb .. value_ub (inclusive)"
 //
 // Example:
-//  ARRAY_IN_BOUNDS(unsigned, k, 0, MLKEM_N-1, a->coeffs, -(MLKEM_Q - 1),
-//  MLKEM_Q - 1)
+//  ARRAY_IN_BOUNDS(0, MLKEM_N-1, a->coeffs, -(MLKEM_Q - 1), MLKEM_Q - 1)
 // expands to
-//  __CPROVER_forall { unsigned k; (0 <= k && k <= MLKEM_N-1) ==> ( (-(MLKEM_Q -
+//  __CPROVER_forall { int k; (0 <= k && k <= MLKEM_N-1) ==> ( (-(MLKEM_Q -
 //  1) <= a->coeffs[k]) && (a->coeffs[k] <= (MLKEM_Q - 1))) }
 
 // Prevent clang-format from corrupting CBMC's special ==> operator
 // clang-format off
-#define ARRAY_IN_BOUNDS(indextype, qvar, qvar_lb, qvar_ub, array_var, \
+
+#define CBMC_CONCAT_(left, right) left##right
+#define CBMC_CONCAT(left, right) CBMC_CONCAT_(left,right)
+
+#define ARRAY_IN_BOUNDS_CORE(indextype, qvar, qvar_lb, qvar_ub, array_var, \
                         value_lb, value_ub)                           \
   __CPROVER_forall                                                    \
   {                                                                   \
@@ -124,6 +127,12 @@
           (((value_lb) <= (array_var[(qvar)])) &&                     \
            ((array_var[(qvar)]) <= (value_ub)))                       \
   }
+
+#define ARRAY_IN_BOUNDS(qvar_lb, qvar_ub, array_var,            \
+                        value_lb, value_ub)                     \
+    ARRAY_IN_BOUNDS_CORE(int, CBMC_CONCAT(_cbmc_idx,__LINE__),  \
+     (qvar_lb), (qvar_ub), (array_var), (value_lb), (value_ub))
+
 // clang-format on
 
 #endif
diff --git a/mlkem/indcpa.c b/mlkem/indcpa.c
index 3e5343760..4418f5c24 100644
--- a/mlkem/indcpa.c
+++ b/mlkem/indcpa.c
@@ -38,7 +38,7 @@ REQUIRES(IS_FRESH(r, MLKEM_INDCPA_PUBLICKEYBYTES))
 REQUIRES(IS_FRESH(pk, sizeof(polyvec)))
 REQUIRES(IS_FRESH(seed, MLKEM_SYMBYTES))
 REQUIRES(FORALL(int, k0, 0, MLKEM_K - 1,
-  ARRAY_IN_BOUNDS(int, k1, 0, MLKEM_N - 1, pk->vec[k0].coeffs, 0, (MLKEM_Q - 1))))
+  ARRAY_IN_BOUNDS(0, MLKEM_N - 1, pk->vec[k0].coeffs, 0, (MLKEM_Q - 1))))
 ASSIGNS(OBJECT_WHOLE(r))  // clang-format on
 {
   POLYVEC_BOUND(pk, MLKEM_Q);
@@ -66,7 +66,7 @@ REQUIRES(IS_FRESH(packedpk, MLKEM_INDCPA_PUBLICKEYBYTES))
 REQUIRES(IS_FRESH(pk, sizeof(polyvec)))
 REQUIRES(IS_FRESH(seed, MLKEM_SYMBYTES))
 ENSURES(FORALL(int, k0, 0, MLKEM_K - 1,
-  ARRAY_IN_BOUNDS(int, k1, 0, MLKEM_N - 1, pk->vec[k0].coeffs, 0, (MLKEM_Q - 1))))
+  ARRAY_IN_BOUNDS(0, MLKEM_N - 1, pk->vec[k0].coeffs, 0, (MLKEM_Q - 1))))
 ASSIGNS(OBJECT_WHOLE(pk))
 ASSIGNS(OBJECT_WHOLE(seed))  // clang-format on
 {
@@ -94,7 +94,7 @@ void pack_sk(uint8_t r[MLKEM_INDCPA_SECRETKEYBYTES],
 REQUIRES(IS_FRESH(r, MLKEM_INDCPA_SECRETKEYBYTES))
 REQUIRES(IS_FRESH(sk, sizeof(polyvec)))
 REQUIRES(FORALL(int, k0, 0, MLKEM_K - 1,
-  ARRAY_IN_BOUNDS(int, k1, 0, MLKEM_N - 1, sk->vec[k0].coeffs, 0, (MLKEM_Q - 1))))
+  ARRAY_IN_BOUNDS(0, MLKEM_N - 1, sk->vec[k0].coeffs, 0, (MLKEM_Q - 1))))
 ASSIGNS(OBJECT_WHOLE(r))
 // clang-format on
 {
@@ -119,7 +119,7 @@ void unpack_sk(
 REQUIRES(IS_FRESH(packedsk, MLKEM_INDCPA_SECRETKEYBYTES))
 REQUIRES(IS_FRESH(sk, sizeof(polyvec)))
 ENSURES(FORALL(int, k0, 0, MLKEM_K - 1,
-  ARRAY_IN_BOUNDS(int, k1, 0, MLKEM_N - 1, sk->vec[k0].coeffs, 0, (MLKEM_Q - 1))))
+  ARRAY_IN_BOUNDS(0, MLKEM_N - 1, sk->vec[k0].coeffs, 0, (MLKEM_Q - 1))))
 ASSIGNS(OBJECT_WHOLE(sk))  // clang-format on
 {
   polyvec_frombytes(sk, packedsk);
@@ -173,10 +173,10 @@ void gen_matrix_entry_x4(poly *vec, uint8_t *seed[4])  // clang-format off
   REQUIRES(IS_FRESH(seed[2], MLKEM_SYMBYTES + 2))
   REQUIRES(IS_FRESH(seed[3], MLKEM_SYMBYTES + 2))
   ASSIGNS(OBJECT_UPTO(vec, sizeof(poly) * 4))
-  ENSURES(ARRAY_IN_BOUNDS(int, k0, 0, MLKEM_N - 1, vec[0].coeffs, 0, (MLKEM_Q - 1)))
-  ENSURES(ARRAY_IN_BOUNDS(int, k1, 0, MLKEM_N - 1, vec[1].coeffs, 0, (MLKEM_Q - 1)))
-  ENSURES(ARRAY_IN_BOUNDS(int, k2, 0, MLKEM_N - 1, vec[2].coeffs, 0, (MLKEM_Q - 1)))
-  ENSURES(ARRAY_IN_BOUNDS(int, k3, 0, MLKEM_N - 1, vec[3].coeffs, 0, (MLKEM_Q - 1)))
+  ENSURES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, vec[0].coeffs, 0, (MLKEM_Q - 1)))
+  ENSURES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, vec[1].coeffs, 0, (MLKEM_Q - 1)))
+  ENSURES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, vec[2].coeffs, 0, (MLKEM_Q - 1)))
+  ENSURES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, vec[3].coeffs, 0, (MLKEM_Q - 1)))
 // clang-format on
 {
   // Temporary buffers for XOF output before rejection sampling
@@ -212,10 +212,10 @@ void gen_matrix_entry_x4(poly *vec, uint8_t *seed[4])  // clang-format off
        OBJECT_WHOLE(buf1), OBJECT_WHOLE(buf2), OBJECT_WHOLE(buf3))
     INVARIANT(ctr[0] <= MLKEM_N && ctr[1] <= MLKEM_N)
     INVARIANT(ctr[2] <= MLKEM_N && ctr[3] <= MLKEM_N)
-    INVARIANT(ctr[0] > 0 ==> ARRAY_IN_BOUNDS(int, k0, 0, ctr[0] - 1, vec[0].coeffs, 0, (MLKEM_Q - 1)))
-    INVARIANT(ctr[1] > 0 ==> ARRAY_IN_BOUNDS(int, k1, 0, ctr[1] - 1, vec[1].coeffs, 0, (MLKEM_Q - 1)))
-    INVARIANT(ctr[2] > 0 ==> ARRAY_IN_BOUNDS(int, k2, 0, ctr[2] - 1, vec[2].coeffs, 0, (MLKEM_Q - 1)))
-    INVARIANT(ctr[3] > 0 ==> ARRAY_IN_BOUNDS(int, k3, 0, ctr[3] - 1, vec[3].coeffs, 0, (MLKEM_Q - 1)))
+    INVARIANT(ctr[0] > 0 ==> ARRAY_IN_BOUNDS(0, ctr[0] - 1, vec[0].coeffs, 0, (MLKEM_Q - 1)))
+    INVARIANT(ctr[1] > 0 ==> ARRAY_IN_BOUNDS(0, ctr[1] - 1, vec[1].coeffs, 0, (MLKEM_Q - 1)))
+    INVARIANT(ctr[2] > 0 ==> ARRAY_IN_BOUNDS(0, ctr[2] - 1, vec[2].coeffs, 0, (MLKEM_Q - 1)))
+    INVARIANT(ctr[3] > 0 ==> ARRAY_IN_BOUNDS(0, ctr[3] - 1, vec[3].coeffs, 0, (MLKEM_Q - 1)))
                             // clang-format on
     {
       shake128x4_squeezeblocks(buf0, buf1, buf2, buf3, 1, &statex);
@@ -236,7 +236,7 @@ void gen_matrix_entry(poly *entry,
   REQUIRES(IS_FRESH(entry, sizeof(poly)))
   REQUIRES(IS_FRESH(seed, MLKEM_SYMBYTES + 2))
   ASSIGNS(OBJECT_UPTO(entry, sizeof(poly)))
-  ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, entry->coeffs, 0, (MLKEM_Q - 1)))
+  ENSURES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, entry->coeffs, 0, (MLKEM_Q - 1)))
 {  // clang-format on
   shake128ctx state;
   uint8_t buf[GEN_MATRIX_NBLOCKS * SHAKE128_RATE];
@@ -255,7 +255,7 @@ void gen_matrix_entry(poly *entry,
   while (ctr < MLKEM_N)  // clang-format off
     ASSIGNS(ctr, state, OBJECT_UPTO(entry, sizeof(poly)), OBJECT_WHOLE(buf))
     INVARIANT(0 <= ctr && ctr <= MLKEM_N)
-    INVARIANT(ctr > 0 ==> ARRAY_IN_BOUNDS(int, k, 0, ctr - 1, entry->coeffs,
+    INVARIANT(ctr > 0 ==> ARRAY_IN_BOUNDS(0, ctr - 1, entry->coeffs,
                                           0, (MLKEM_Q - 1)))  // clang-format on
     {
       shake128_squeezeblocks(buf, 1, &state);
@@ -366,14 +366,14 @@ void gen_matrix(polyvec *a, const uint8_t seed[MLKEM_SYMBYTES],
  **************************************************/
 STATIC_TESTABLE
 void matvec_mul(polyvec *out, const polyvec a[MLKEM_K], const polyvec *v,
-    const polyvec_mulcache *vc) // clang-format off
+                const polyvec_mulcache *vc)  // clang-format off
   REQUIRES(IS_FRESH(out, sizeof(polyvec)))
   REQUIRES(IS_FRESH(a, sizeof(polyvec) * MLKEM_K))
   REQUIRES(IS_FRESH(v, sizeof(polyvec)))
   REQUIRES(IS_FRESH(vc, sizeof(polyvec_mulcache)))
   REQUIRES(FORALL(int, k0, 0, MLKEM_K - 1,
    FORALL(int, k1, 0, MLKEM_K - 1,
-     ARRAY_IN_BOUNDS(int, k2, 0, MLKEM_N - 1,
+     ARRAY_IN_BOUNDS(0, MLKEM_N - 1,
        a[k0].vec[k1].coeffs, -(MLKEM_Q - 1), (MLKEM_Q - 1)))))
   ASSIGNS(OBJECT_WHOLE(out))
 // clang-format on
diff --git a/mlkem/indcpa.h b/mlkem/indcpa.h
index a14b08d43..ec4e98976 100644
--- a/mlkem/indcpa.h
+++ b/mlkem/indcpa.h
@@ -17,7 +17,7 @@ REQUIRES(IS_FRESH(seed, MLKEM_SYMBYTES))
 REQUIRES(transposed == 0 || transposed == 1)
 ASSIGNS(OBJECT_WHOLE(a))
 ENSURES(FORALL(int, x, 0, MLKEM_K - 1, FORALL(int, y, 0, MLKEM_K - 1,
-  ARRAY_IN_BOUNDS(int, i, 0, MLKEM_N - 1, a[x].vec[y].coeffs, 0, (MLKEM_Q - 1)))));
+  ARRAY_IN_BOUNDS(0, MLKEM_N - 1, a[x].vec[y].coeffs, 0, (MLKEM_Q - 1)))));
 // clang-format on
 
 #define indcpa_keypair_derand MLKEM_NAMESPACE(indcpa_keypair_derand)
diff --git a/mlkem/ntt.h b/mlkem/ntt.h
index 54cbbc2cc..dc7e3c4a7 100644
--- a/mlkem/ntt.h
+++ b/mlkem/ntt.h
@@ -43,9 +43,9 @@ void basemul_cached(int16_t r[2], const int16_t a[2], const int16_t b[2],
 REQUIRES(IS_FRESH(r, 2 * sizeof(int16_t)))
 REQUIRES(IS_FRESH(a, 2 * sizeof(int16_t)))
 REQUIRES(IS_FRESH(b, 2 * sizeof(int16_t)))
-REQUIRES(ARRAY_IN_BOUNDS(int, k, 0, 1, a, -(MLKEM_Q - 1), (MLKEM_Q - 1)))
+REQUIRES(ARRAY_IN_BOUNDS(0, 1, a, -(MLKEM_Q - 1), (MLKEM_Q - 1)))
 ASSIGNS(OBJECT_UPTO(r, 2 * sizeof(int16_t)))
-ENSURES(ARRAY_IN_BOUNDS(int, k, 0, 1, r, -(3 * HALF_Q - 1), (3 * HALF_Q - 1)));
+ENSURES(ARRAY_IN_BOUNDS(0, 1, r, -(3 * HALF_Q - 1), (3 * HALF_Q - 1)));
 // clang-format on
 
 
diff --git a/mlkem/poly.c b/mlkem/poly.c
index f0fea60f6..6eef39902 100644
--- a/mlkem/poly.c
+++ b/mlkem/poly.c
@@ -26,7 +26,7 @@ void poly_compress(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES], const poly *a) {
       for (int j = 0; j < 8; j++)  // clang-format off
         ASSIGNS(j, OBJECT_WHOLE(t))
         INVARIANT(i >= 0 && i <= MLKEM_N / 8 && j >= 0 && j <= 8)
-        INVARIANT(ARRAY_IN_BOUNDS(int, k2, 0, (j-1), t, 0, 15))
+        INVARIANT(ARRAY_IN_BOUNDS(0, (j-1), t, 0, 15))
         {  // clang-format on
           // REF-CHANGE: Precondition change, we assume unsigned canonical data
           t[j] = scalar_compress_d4(a->coeffs[8 * i + j]);
@@ -47,7 +47,7 @@ void poly_compress(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES], const poly *a) {
       for (int j = 0; j < 8; j++)  // clang-format off
         ASSIGNS(j, OBJECT_WHOLE(t))
         INVARIANT(i >= 0 && i <= MLKEM_N / 8 && j >= 0 && j <= 8)
-        INVARIANT(ARRAY_IN_BOUNDS(int, k2, 0, (j-1), t, 0, 31))
+        INVARIANT(ARRAY_IN_BOUNDS(0, (j-1), t, 0, 31))
         {  // clang-format on
           // REF-CHANGE: Precondition change, we assume unsigned canonical data
           t[j] = scalar_compress_d5(a->coeffs[8 * i + j]);
@@ -72,7 +72,7 @@ void poly_decompress(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES]) {
   for (int i = 0; i < MLKEM_N / 2; i++)  // clang-format off
         ASSIGNS(i, OBJECT_WHOLE(r))
         INVARIANT(i >= 0 && i <= MLKEM_N / 2)
-        INVARIANT(ARRAY_IN_BOUNDS(int, k, 0, (2 * i - 1), r->coeffs, 0, (MLKEM_Q - 1)))
+        INVARIANT(ARRAY_IN_BOUNDS(0, (2 * i - 1), r->coeffs, 0, (MLKEM_Q - 1)))
     {  // clang-format on
       // REF-CHANGE: Hoist scalar decompression into separate function
       r->coeffs[2 * i + 0] = scalar_decompress_d4((a[i] >> 0) & 0xF);
@@ -82,7 +82,7 @@ void poly_decompress(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES]) {
   for (int i = 0; i < MLKEM_N / 8; i++)  // clang-format off
     ASSIGNS(i, OBJECT_WHOLE(r))
     INVARIANT(i >= 0 && i <= MLKEM_N / 8)
-    INVARIANT(ARRAY_IN_BOUNDS(int, k, 0, (8 * i - 1), r->coeffs, 0, (MLKEM_Q - 1)))
+    INVARIANT(ARRAY_IN_BOUNDS(0, (8 * i - 1), r->coeffs, 0, (MLKEM_Q - 1)))
     {  // clang-format on
       uint8_t t[8];
       const int offset = i * 5;
@@ -105,7 +105,7 @@ void poly_decompress(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES]) {
       for (int j = 0; j < 8; j++)  // clang-format off
         ASSIGNS(j, OBJECT_WHOLE(r))
         INVARIANT(j >= 0 && j <= 8 && i >= 0 && i <= MLKEM_N / 8)
-        INVARIANT(ARRAY_IN_BOUNDS(int, k, 0, (8 * i + j - 1), r->coeffs, 0, (MLKEM_Q - 1)))
+        INVARIANT(ARRAY_IN_BOUNDS(0, (8 * i + j - 1), r->coeffs, 0, (MLKEM_Q - 1)))
         {  // clang-format on
           // REF-CHANGE: Hoist scalar decompression into separate function
           r->coeffs[8 * i + j] = scalar_decompress_d5(t[j]);
@@ -162,7 +162,7 @@ void poly_frombytes(poly *r, const uint8_t a[MLKEM_POLYBYTES]) {
   for (i = 0; i < MLKEM_N / 2; i++)  // clang-format off
     ASSIGNS(i, OBJECT_WHOLE(r))
     INVARIANT(i >= 0 && i <= MLKEM_N / 2)
-    INVARIANT(ARRAY_IN_BOUNDS(int, k, 0, (2 * i - 1), r->coeffs, 0, 4095))
+    INVARIANT(ARRAY_IN_BOUNDS(0, (2 * i - 1), r->coeffs, 0, 4095))
     {  // clang-format on
       // REF-CHANGE: Introduce some locals for better readability
       const uint8_t t0 = a[3 * i + 0];
@@ -189,12 +189,12 @@ void poly_frommsg(poly *r, const uint8_t msg[MLKEM_INDCPA_MSGBYTES]) {
   for (int i = 0; i < MLKEM_N / 8; i++)  // clang-format off
     ASSIGNS(i, OBJECT_WHOLE(r))
     INVARIANT(i >= 0 && i <= MLKEM_N / 8)
-    INVARIANT(ARRAY_IN_BOUNDS(int, k, 0, (8 * i - 1), r->coeffs, 0, (MLKEM_Q - 1)))
-    {      // clang-format on
+    INVARIANT(ARRAY_IN_BOUNDS(0, (8 * i - 1), r->coeffs, 0, (MLKEM_Q - 1)))
+    {          // clang-format on
       for (int j = 0; j < 8; j++)  // clang-format off
         ASSIGNS(j, OBJECT_WHOLE(r))
         INVARIANT(i >= 0 && i <  MLKEM_N / 8 && j >= 0 && j <= 8)
-        INVARIANT(ARRAY_IN_BOUNDS(int, k, 0, (8 * i + j - 1), r->coeffs, 0, (MLKEM_Q - 1)))
+        INVARIANT(ARRAY_IN_BOUNDS(0, (8 * i + j - 1), r->coeffs, 0, (MLKEM_Q - 1)))
         {  // clang-format on
           r->coeffs[8 * i + j] = 0;
           cmov_int16(&r->coeffs[8 * i + j], HALF_Q, (msg[i] >> j) & 1);
@@ -299,7 +299,7 @@ void poly_basemul_montgomery_cached(poly *r, const poly *a, const poly *b,
   for (i = 0; i < MLKEM_N / 4; i++)  // clang-format off
     ASSIGNS(i, OBJECT_WHOLE(r))
     INVARIANT(i >= 0 && i <= MLKEM_N / 4)
-    INVARIANT(ARRAY_IN_BOUNDS(int, k, 0, (4 * i - 1), r->coeffs, -(3 * HALF_Q - 1), (3 * HALF_Q - 1)))
+    INVARIANT(ARRAY_IN_BOUNDS(0, (4 * i - 1), r->coeffs, -(3 * HALF_Q - 1), (3 * HALF_Q - 1)))
     {  // clang-format on
       basemul_cached(&r->coeffs[4 * i], &a->coeffs[4 * i], &b->coeffs[4 * i],
                      b_cache->coeffs[2 * i]);
@@ -315,7 +315,7 @@ void poly_tomont(poly *r) {
   for (i = 0; i < MLKEM_N; i++)  // clang-format off
     ASSIGNS(i, OBJECT_WHOLE(r))
     INVARIANT(i >= 0 && i <= MLKEM_N)
-    INVARIANT(ARRAY_IN_BOUNDS(int, k, 0, (i - 1), r->coeffs, -(MLKEM_Q - 1), (MLKEM_Q - 1)))
+    INVARIANT(ARRAY_IN_BOUNDS(0, (i - 1), r->coeffs, -(MLKEM_Q - 1), (MLKEM_Q - 1)))
     {  // clang-format on
       r->coeffs[i] = fqmul(r->coeffs[i], f);
     }
@@ -335,7 +335,7 @@ void poly_reduce(poly *r) {
   for (i = 0; i < MLKEM_N; i++)  // clang-format off
     ASSIGNS(i, OBJECT_WHOLE(r))
     INVARIANT(i >= 0 && i <= MLKEM_N)
-    INVARIANT(ARRAY_IN_BOUNDS(int, k, 0, (i - 1), r->coeffs, 0, (MLKEM_Q - 1)))
+    INVARIANT(ARRAY_IN_BOUNDS(0, (i - 1), r->coeffs, 0, (MLKEM_Q - 1)))
     {  // clang-format on
       // Barrett reduction, giving signed canonical representative
       int16_t t = barrett_reduce(r->coeffs[i]);
diff --git a/mlkem/poly.h b/mlkem/poly.h
index db42a72a8..f773548b9 100644
--- a/mlkem/poly.h
+++ b/mlkem/poly.h
@@ -320,7 +320,7 @@ void poly_compress(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES],
                    const poly *a)  // clang-format off
 REQUIRES(IS_FRESH(r, MLKEM_POLYCOMPRESSEDBYTES))
 REQUIRES(IS_FRESH(a, sizeof(poly)))
-REQUIRES(ARRAY_IN_BOUNDS(int, k, 0, (MLKEM_N - 1), a->coeffs, 0, (MLKEM_Q - 1)))
+REQUIRES(ARRAY_IN_BOUNDS(0, (MLKEM_N - 1), a->coeffs, 0, (MLKEM_Q - 1)))
 ASSIGNS(OBJECT_WHOLE(r));
 // clang-format on
 
@@ -344,7 +344,7 @@ void poly_decompress(
 REQUIRES(IS_FRESH(a, MLKEM_POLYCOMPRESSEDBYTES))
 REQUIRES(IS_FRESH(r, sizeof(poly)))
 ASSIGNS(OBJECT_WHOLE(r))
-ENSURES(ARRAY_IN_BOUNDS(int, k, 0, (MLKEM_N - 1), r->coeffs, 0, (MLKEM_Q - 1)));
+ENSURES(ARRAY_IN_BOUNDS(0, (MLKEM_N - 1), r->coeffs, 0, (MLKEM_Q - 1)));
 // clang-format on
 
 #define poly_tobytes MLKEM_NAMESPACE(poly_tobytes)
@@ -366,7 +366,7 @@ void poly_tobytes(uint8_t r[MLKEM_POLYBYTES],
                   const poly *a)  // clang-format off
 REQUIRES(IS_FRESH(r, MLKEM_POLYBYTES))
 REQUIRES(IS_FRESH(a, sizeof(poly)))
-REQUIRES(ARRAY_IN_BOUNDS(int, k, 0, (MLKEM_N - 1), a->coeffs, 0, (MLKEM_Q - 1)))
+REQUIRES(ARRAY_IN_BOUNDS(0, (MLKEM_N - 1), a->coeffs, 0, (MLKEM_Q - 1)))
 ASSIGNS(OBJECT_WHOLE(r));
 // clang-format on
 
@@ -390,7 +390,7 @@ void poly_frombytes(poly *r,
 REQUIRES(IS_FRESH(a, MLKEM_POLYBYTES))
 REQUIRES(IS_FRESH(r, sizeof(poly)))
 ASSIGNS(OBJECT_UPTO(r, sizeof(poly)))
-ENSURES(ARRAY_IN_BOUNDS(int, k, 0, (MLKEM_N - 1), r->coeffs, 0, 4095));
+ENSURES(ARRAY_IN_BOUNDS(0, (MLKEM_N - 1), r->coeffs, 0, 4095));
 // clang-format on
 
 
@@ -408,7 +408,7 @@ void poly_frommsg(poly *r,
 REQUIRES(IS_FRESH(msg, MLKEM_INDCPA_MSGBYTES))
 REQUIRES(IS_FRESH(r, sizeof(poly)))
 ASSIGNS(OBJECT_WHOLE(r))
-ENSURES(ARRAY_IN_BOUNDS(int, k, 0, (MLKEM_N - 1), r->coeffs, 0, (MLKEM_Q - 1)));
+ENSURES(ARRAY_IN_BOUNDS(0, (MLKEM_N - 1), r->coeffs, 0, (MLKEM_Q - 1)));
 // clang-format on
 
 
@@ -426,7 +426,7 @@ void poly_tomsg(uint8_t msg[MLKEM_INDCPA_MSGBYTES],
                 const poly *r)  // clang-format off
 REQUIRES(IS_FRESH(msg, MLKEM_INDCPA_MSGBYTES))
 REQUIRES(IS_FRESH(r, sizeof(poly)))
-REQUIRES(ARRAY_IN_BOUNDS(int, k, 0, (MLKEM_N - 1), r->coeffs, 0, (MLKEM_Q - 1)))
+REQUIRES(ARRAY_IN_BOUNDS(0, (MLKEM_N - 1), r->coeffs, 0, (MLKEM_Q - 1)))
 ASSIGNS(OBJECT_WHOLE(msg));
 // clang-format on
 
@@ -473,10 +473,10 @@ ASSIGNS(OBJECT_UPTO(r1, sizeof(poly)))
 ASSIGNS(OBJECT_UPTO(r2, sizeof(poly)))
 ASSIGNS(OBJECT_UPTO(r3, sizeof(poly)))
 ENSURES(
-    ARRAY_IN_BOUNDS(int, k0, 0, MLKEM_N - 1, r0->coeffs, -MLKEM_ETA1, MLKEM_ETA1)
- && ARRAY_IN_BOUNDS(int, k1, 0, MLKEM_N - 1, r1->coeffs, -MLKEM_ETA1, MLKEM_ETA1)
- && ARRAY_IN_BOUNDS(int, k2, 0, MLKEM_N - 1, r2->coeffs, -MLKEM_ETA1, MLKEM_ETA1)
- && ARRAY_IN_BOUNDS(int, k3, 0, MLKEM_N - 1, r3->coeffs, -MLKEM_ETA1, MLKEM_ETA1));
+    ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r0->coeffs, -MLKEM_ETA1, MLKEM_ETA1)
+ && ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r1->coeffs, -MLKEM_ETA1, MLKEM_ETA1)
+ && ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r2->coeffs, -MLKEM_ETA1, MLKEM_ETA1)
+ && ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r3->coeffs, -MLKEM_ETA1, MLKEM_ETA1));
 // clang-format on
 
 #define poly_getnoise_eta2 MLKEM_NAMESPACE(poly_getnoise_eta2)
@@ -497,7 +497,7 @@ void poly_getnoise_eta2(poly *r, const uint8_t seed[MLKEM_SYMBYTES],
 REQUIRES(IS_FRESH(r, sizeof(poly)))
 REQUIRES(IS_FRESH(seed, MLKEM_SYMBYTES))
 ASSIGNS(OBJECT_WHOLE(r))
-ENSURES(ARRAY_IN_BOUNDS(int, k0, 0, MLKEM_N - 1, r->coeffs, -MLKEM_ETA2, MLKEM_ETA2));
+ENSURES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r->coeffs, -MLKEM_ETA2, MLKEM_ETA2));
 // clang-format on
 
 #define poly_getnoise_eta1122_4x MLKEM_NAMESPACE(poly_getnoise_eta1122_4x)
@@ -524,10 +524,10 @@ REQUIRES(IS_FRESH(r3, sizeof(poly)))
 REQUIRES(IS_FRESH(seed, MLKEM_SYMBYTES))
 ASSIGNS(OBJECT_WHOLE(r0), OBJECT_WHOLE(r1), OBJECT_WHOLE(r2), OBJECT_WHOLE(r3))
 ENSURES(                                                                          \
-    ARRAY_IN_BOUNDS(int, k0, 0, MLKEM_N - 1, r0->coeffs, -MLKEM_ETA1, MLKEM_ETA1) \
- && ARRAY_IN_BOUNDS(int, k1, 0, MLKEM_N - 1, r1->coeffs, -MLKEM_ETA1, MLKEM_ETA1) \
- && ARRAY_IN_BOUNDS(int, k2, 0, MLKEM_N - 1, r2->coeffs, -MLKEM_ETA2, MLKEM_ETA2) \
- && ARRAY_IN_BOUNDS(int, k3, 0, MLKEM_N - 1, r3->coeffs, -MLKEM_ETA2, MLKEM_ETA2));
+    ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r0->coeffs, -MLKEM_ETA1, MLKEM_ETA1) \
+ && ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r1->coeffs, -MLKEM_ETA1, MLKEM_ETA1) \
+ && ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r2->coeffs, -MLKEM_ETA2, MLKEM_ETA2) \
+ && ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r3->coeffs, -MLKEM_ETA2, MLKEM_ETA2));
 // clang-format on
 
 #define poly_basemul_montgomery_cached \
@@ -559,9 +559,9 @@ REQUIRES(IS_FRESH(r, sizeof(poly)))
 REQUIRES(IS_FRESH(a, sizeof(poly)))
 REQUIRES(IS_FRESH(b, sizeof(poly)))
 REQUIRES(IS_FRESH(b_cache, sizeof(poly_mulcache)))
-REQUIRES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, a->coeffs, -(MLKEM_Q - 1), (MLKEM_Q - 1)))
+REQUIRES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, a->coeffs, -(MLKEM_Q - 1), (MLKEM_Q - 1)))
 ASSIGNS(OBJECT_WHOLE(r))
-ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, -(3 * HALF_Q - 1), (3 * HALF_Q - 1)));
+ENSURES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r->coeffs, -(3 * HALF_Q - 1), (3 * HALF_Q - 1)));
 // clang-format on
 
 #define poly_tomont MLKEM_NAMESPACE(poly_tomont)
@@ -578,7 +578,7 @@ ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, -(3 * HALF_Q - 1), (3
 void poly_tomont(poly *r)  // clang-format off
 REQUIRES(IS_FRESH(r, sizeof(poly)))
 ASSIGNS(OBJECT_UPTO(r, sizeof(poly)))
-ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, -(MLKEM_Q - 1), (MLKEM_Q - 1)));
+ENSURES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r->coeffs, -(MLKEM_Q - 1), (MLKEM_Q - 1)));
 // clang-format on
 
 // REF-CHANGE: This function does not exist in the reference implementation
@@ -628,7 +628,7 @@ ASSIGNS(OBJECT_WHOLE(x));
 void poly_reduce(poly *r)  // clang-format off
 REQUIRES(IS_FRESH(r, sizeof(poly)))
 ASSIGNS(OBJECT_UPTO(r, sizeof(poly)))
-ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, 0, (MLKEM_Q - 1)));
+ENSURES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r->coeffs, 0, (MLKEM_Q - 1)));
 // clang-format on
 
 #define poly_add MLKEM_NAMESPACE(poly_add)
diff --git a/mlkem/polyvec.c b/mlkem/polyvec.c
index 0764639f6..d7a9ec25e 100644
--- a/mlkem/polyvec.c
+++ b/mlkem/polyvec.c
@@ -110,14 +110,14 @@ void polyvec_decompress(polyvec *r,
     ASSIGNS(i, OBJECT_WHOLE(r))
     INVARIANT(0 <= i && i <= MLKEM_K)
     INVARIANT(FORALL(int, r0, 0, i - 1,
-      ARRAY_IN_BOUNDS(int, r1, 0, MLKEM_N - 1, r->vec[r0].coeffs, 0, (MLKEM_Q - 1))))
-    {           // clang-format on
+      ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r->vec[r0].coeffs, 0, (MLKEM_Q - 1))))
+    {  // clang-format on
       for (int j = 0; j < MLKEM_N / 8; j++)  // clang-format off
         ASSIGNS(j, OBJECT_WHOLE(r))
         INVARIANT(0 <= j && j <= MLKEM_N / 8)
         INVARIANT(FORALL(int, r0, 0, i - 1,
-          ARRAY_IN_BOUNDS(int, r1, 0, MLKEM_N - 1, r->vec[r0].coeffs, 0, (MLKEM_Q - 1))))
-        INVARIANT(ARRAY_IN_BOUNDS(int, r0, 0, 8 * j - 1, r->vec[i].coeffs, 0, (MLKEM_Q - 1)))
+          ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r->vec[r0].coeffs, 0, (MLKEM_Q - 1))))
+        INVARIANT(ARRAY_IN_BOUNDS(0, 8 * j - 1, r->vec[i].coeffs, 0, (MLKEM_Q - 1)))
         {  // clang-format on
           uint16_t t[8];
           uint8_t const *base = &a[11 * (i * (MLKEM_N / 8) + j)];
@@ -136,9 +136,9 @@ void polyvec_decompress(polyvec *r,
             ASSIGNS(k, OBJECT_WHOLE(r))
             INVARIANT(0 <= k && k <= 8)
             INVARIANT(FORALL(int, r0, 0, i - 1,
-              ARRAY_IN_BOUNDS(int, r1, 0, MLKEM_N - 1,
+              ARRAY_IN_BOUNDS(0, MLKEM_N - 1,
                 r->vec[r0].coeffs, 0, (MLKEM_Q - 1))))
-            INVARIANT(ARRAY_IN_BOUNDS(int, r0, 0, 8 * j + k - 1,
+            INVARIANT(ARRAY_IN_BOUNDS(0, 8 * j + k - 1,
               r->vec[i].coeffs, 0, (MLKEM_Q - 1)))
             {  // clang-format on
               r->vec[i].coeffs[8 * j + k] = scalar_decompress_d11(t[k]);
@@ -150,14 +150,14 @@ void polyvec_decompress(polyvec *r,
     ASSIGNS(i, OBJECT_WHOLE(r))
     INVARIANT(0 <= i && i <= MLKEM_K)
     INVARIANT(FORALL(int, r0, 0, i - 1,
-    ARRAY_IN_BOUNDS(int, r1, 0, MLKEM_N - 1, r->vec[r0].coeffs, 0, (MLKEM_Q - 1))))
-    {           // clang-format on
+    ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r->vec[r0].coeffs, 0, (MLKEM_Q - 1))))
+    {  // clang-format on
       for (int j = 0; j < MLKEM_N / 4; j++)  // clang-format off
         ASSIGNS(j, OBJECT_WHOLE(r))
         INVARIANT(0 <= j && j <= MLKEM_N / 4)
         INVARIANT(FORALL(int, r0, 0, i - 1,
-          ARRAY_IN_BOUNDS(int, r1, 0, MLKEM_N - 1, r->vec[r0].coeffs, 0, (MLKEM_Q - 1))))
-        INVARIANT(ARRAY_IN_BOUNDS(int, r0, 0, 4 * j - 1, r->vec[i].coeffs, 0, (MLKEM_Q - 1)))
+          ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r->vec[r0].coeffs, 0, (MLKEM_Q - 1))))
+        INVARIANT(ARRAY_IN_BOUNDS(0, 4 * j - 1, r->vec[i].coeffs, 0, (MLKEM_Q - 1)))
         {  // clang-format on
           uint16_t t[4];
           uint8_t const *base = &a[5 * (i * (MLKEM_N / 4) + j)];
@@ -171,8 +171,8 @@ void polyvec_decompress(polyvec *r,
             ASSIGNS(k, OBJECT_WHOLE(r))
             INVARIANT(0 <= k && k <= 4)
             INVARIANT(FORALL(int, r0, 0, i - 1,
-              ARRAY_IN_BOUNDS(int, r1, 0, MLKEM_N - 1, r->vec[r0].coeffs, 0, (MLKEM_Q - 1))))
-            INVARIANT(ARRAY_IN_BOUNDS(int, r0, 0, 4 * j + k - 1, r->vec[i].coeffs, 0, (MLKEM_Q - 1)))
+              ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r->vec[r0].coeffs, 0, (MLKEM_Q - 1))))
+            INVARIANT(ARRAY_IN_BOUNDS(0, 4 * j + k - 1, r->vec[i].coeffs, 0, (MLKEM_Q - 1)))
             {  // clang-format on
               r->vec[i].coeffs[4 * j + k] = scalar_decompress_d10(t[k]);
             }
@@ -264,7 +264,7 @@ void polyvec_basemul_acc_montgomery_cached(poly *r, const polyvec *a,
   for (i = 1; i < MLKEM_K; i++)  // clang-format off
     ASSIGNS(i, t, OBJECT_WHOLE(r))
     INVARIANT(i >= 1 && i <= MLKEM_K)
-    INVARIANT(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs,
+    INVARIANT(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r->coeffs,
                               i * (-(3 * HALF_Q - 1)), i * (3 * HALF_Q - 1)))
     DECREASES(MLKEM_K - i)
     // clang-format on
@@ -278,10 +278,10 @@ void polyvec_basemul_acc_montgomery_cached(poly *r, const polyvec *a,
   // Those bounds are true for the C implementation, but not needed
   // in the higher level bounds reasoning. It is thus best to omit
   // them from the spec to not unnecessarily constraint native implementations.
-  ASSERT(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs,
-                         MLKEM_K * (-(3 * HALF_Q - 1)),
-                         MLKEM_K * (3 * HALF_Q - 1)),
-         "polyvec_basemul_acc_montgomery_cached output bounds");
+  ASSERT(
+      ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r->coeffs, MLKEM_K * (-(3 * HALF_Q - 1)),
+                      MLKEM_K * (3 * HALF_Q - 1)),
+      "polyvec_basemul_acc_montgomery_cached output bounds");
   // TODO: Integrate CBMC assertion into POLY_BOUND if CBMC is set
   POLY_BOUND(r, MLKEM_K * 3 * HALF_Q);
 }
diff --git a/mlkem/polyvec.h b/mlkem/polyvec.h
index 214a24f88..8afe82901 100644
--- a/mlkem/polyvec.h
+++ b/mlkem/polyvec.h
@@ -33,7 +33,7 @@ REQUIRES(IS_FRESH(r, MLKEM_POLYVECCOMPRESSEDBYTES))
 REQUIRES(IS_FRESH(a, sizeof(polyvec)))
 ASSIGNS(OBJECT_WHOLE(r))
 REQUIRES(FORALL(int, k0, 0, MLKEM_K - 1,
-         ARRAY_IN_BOUNDS(int, k1, 0, (MLKEM_N - 1), a->vec[k0].coeffs, 0, (MLKEM_Q - 1))));
+         ARRAY_IN_BOUNDS(0, (MLKEM_N - 1), a->vec[k0].coeffs, 0, (MLKEM_Q - 1))));
 // clang-format on
 
 #define polyvec_decompress MLKEM_NAMESPACE(polyvec_decompress)
@@ -44,7 +44,7 @@ REQUIRES(IS_FRESH(a, MLKEM_POLYVECCOMPRESSEDBYTES))
 REQUIRES(IS_FRESH(r, sizeof(polyvec)))
 ASSIGNS(OBJECT_WHOLE(r))
 ENSURES(FORALL(int, k0, 0, MLKEM_K - 1,
-         ARRAY_IN_BOUNDS(int, k1, 0, (MLKEM_N - 1), r->vec[k0].coeffs, 0, (MLKEM_Q - 1))));
+         ARRAY_IN_BOUNDS(0, (MLKEM_N - 1), r->vec[k0].coeffs, 0, (MLKEM_Q - 1))));
 // clang-format on
 
 #define polyvec_tobytes MLKEM_NAMESPACE(polyvec_tobytes)
@@ -63,7 +63,7 @@ void polyvec_tobytes(uint8_t r[MLKEM_POLYVECBYTES],
 REQUIRES(IS_FRESH(a, sizeof(polyvec)))
 REQUIRES(IS_FRESH(r, MLKEM_POLYVECBYTES))
 REQUIRES(FORALL(int, k0, 0, MLKEM_K - 1,
-         ARRAY_IN_BOUNDS(int, k1, 0, (MLKEM_N - 1), a->vec[k0].coeffs, 0, (MLKEM_Q - 1))))
+         ARRAY_IN_BOUNDS(0, (MLKEM_N - 1), a->vec[k0].coeffs, 0, (MLKEM_Q - 1))))
 ASSIGNS(OBJECT_WHOLE(r));
 // clang-format on
 
@@ -84,7 +84,7 @@ void polyvec_frombytes(polyvec *r,
 REQUIRES(IS_FRESH(r, sizeof(polyvec)))
 REQUIRES(IS_FRESH(a, MLKEM_POLYVECBYTES))
 ENSURES(FORALL(int, k0, 0, MLKEM_K - 1,
-        ARRAY_IN_BOUNDS(int, k1, 0, (MLKEM_N - 1),
+        ARRAY_IN_BOUNDS(0, (MLKEM_N - 1),
                         r->vec[k0].coeffs, 0, 4095)))
 ASSIGNS(OBJECT_WHOLE(r));  // clang-format on
 
@@ -93,7 +93,7 @@ void polyvec_ntt(polyvec *r)  // clang-format off
   REQUIRES(IS_FRESH(r, sizeof(polyvec)))
   ASSIGNS(OBJECT_WHOLE(r))
   ENSURES(FORALL(int, j, 0, MLKEM_K - 1,
-    ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1,
+    ARRAY_IN_BOUNDS(0, MLKEM_N - 1,
                     r->vec[j].coeffs, -(NTT_BOUND - 1), (NTT_BOUND - 1))));
 // clang-format on
 
@@ -134,7 +134,7 @@ REQUIRES(IS_FRESH(b, sizeof(polyvec)))
 REQUIRES(IS_FRESH(b_cache, sizeof(polyvec_mulcache)))
 // Input is coefficient-wise < q in absolute value
 REQUIRES(FORALL(int, k1, 0, MLKEM_K - 1,
- ARRAY_IN_BOUNDS(int, k2, 0, MLKEM_N - 1,
+ ARRAY_IN_BOUNDS(0, MLKEM_N - 1,
    a->vec[k1].coeffs, -(MLKEM_Q - 1), (MLKEM_Q - 1))))
 ASSIGNS(OBJECT_UPTO(r, sizeof(poly)));
 // clang-format on
@@ -190,7 +190,7 @@ void polyvec_reduce(polyvec *r)  // clang-format off
 REQUIRES(IS_FRESH(r, sizeof(polyvec)))
 ASSIGNS(OBJECT_WHOLE(r))
 ENSURES(FORALL(int, k0, 0, MLKEM_K - 1,
-  ARRAY_IN_BOUNDS(int, k1, 0, MLKEM_N - 1, r->vec[k0].coeffs, 0, (MLKEM_Q - 1))));
+  ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r->vec[k0].coeffs, 0, (MLKEM_Q - 1))));
 // clang-format on
 
 #define polyvec_add MLKEM_NAMESPACE(polyvec_add)
@@ -236,7 +236,7 @@ void polyvec_tomont(polyvec *r)  // clang-format off
   REQUIRES(IS_FRESH(r, sizeof(polyvec)))
   ASSIGNS(OBJECT_UPTO(r, sizeof(polyvec)))
   ENSURES(FORALL(int, j, 0, MLKEM_K - 1,
-    ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1,
+    ARRAY_IN_BOUNDS(0, MLKEM_N - 1,
                     r->vec[j].coeffs, -(MLKEM_Q - 1), (MLKEM_Q - 1))))
   ASSIGNS(OBJECT_WHOLE(r));
 // clang-format on
diff --git a/mlkem/rej_uniform.c b/mlkem/rej_uniform.c
index 895b73a11..2a8c11398 100644
--- a/mlkem/rej_uniform.c
+++ b/mlkem/rej_uniform.c
@@ -45,7 +45,7 @@ static unsigned int rej_uniform_scalar(int16_t *r, unsigned int target,
   while (ctr < target && pos + 3 <= buflen)  // clang-format off
     ASSIGNS(ctr, val0, val1, pos, OBJECT_WHOLE(r))
     INVARIANT(offset <= ctr && ctr <= target && pos <= buflen)
-    INVARIANT(ctr > 0 ==> ARRAY_IN_BOUNDS(int, k, 0, ctr - 1, r, 0, (MLKEM_Q - 1)))  // clang-format on
+    INVARIANT(ctr > 0 ==> ARRAY_IN_BOUNDS(0, ctr - 1, r, 0, (MLKEM_Q - 1)))  // clang-format on
     {
       val0 = ((buf[pos + 0] >> 0) | ((uint16_t)buf[pos + 1] << 8)) & 0xFFF;
       val1 = ((buf[pos + 1] >> 4) | ((uint16_t)buf[pos + 2] << 4)) & 0xFFF;
diff --git a/mlkem/rej_uniform.h b/mlkem/rej_uniform.h
index ccfa6befe..c731ca06b 100644
--- a/mlkem/rej_uniform.h
+++ b/mlkem/rej_uniform.h
@@ -48,9 +48,9 @@ unsigned int rej_uniform(int16_t *r, unsigned int target, unsigned int offset,
 REQUIRES(offset <= target && target <= 4096 && buflen <= 4096 && buflen % 3 == 0)
 REQUIRES(IS_FRESH(r, sizeof(int16_t) * target))
 REQUIRES(IS_FRESH(buf, buflen))
-REQUIRES(offset > 0 ==> ARRAY_IN_BOUNDS(int, k, 0, offset - 1, r, 0, (MLKEM_Q - 1)))
+REQUIRES(offset > 0 ==> ARRAY_IN_BOUNDS(0, offset - 1, r, 0, (MLKEM_Q - 1)))
 ASSIGNS(OBJECT_UPTO(r, sizeof(int16_t) * target))
 ENSURES(offset <= RETURN_VALUE && RETURN_VALUE <= target)
-ENSURES(RETURN_VALUE > 0 ==> ARRAY_IN_BOUNDS(int, k, 0, RETURN_VALUE - 1, r, 0, (MLKEM_Q - 1)));
+ENSURES(RETURN_VALUE > 0 ==> ARRAY_IN_BOUNDS(0, RETURN_VALUE - 1, r, 0, (MLKEM_Q - 1)));
 // clang-format on
 #endif