diff --git a/cbmc/proofs/proof_guide.md b/cbmc/proofs/proof_guide.md
index daa2c18b8..4262f0a17 100644
--- a/cbmc/proofs/proof_guide.md
+++ b/cbmc/proofs/proof_guide.md
@@ -374,12 +374,12 @@ We can use the macros in `cbmc.h` to help, thus:
 void poly_tobytes(uint8_t r[MLKEM_POLYBYTES], const poly *a)
      // clang-format off
 REQUIRES(IS_FRESH(a, sizeof(poly)))
-REQUIRES(ARRAY_IN_BOUNDS(int, k, 0, (MLKEM_N - 1), a->coeffs, 0, (MLKEM_Q - 1)))
+REQUIRES(ARRAY_BOUND(a->coeffs, 0, (MLKEM_N - 1), 0, (MLKEM_Q - 1)))
 ASSIGNS(OBJECT_WHOLE(r));
 // clang-format on
 ```
 
-`ARRAY_IN_BOUNDS` is a macro that expands to a quantified expression that expresses that the elemtns of `a->coeffs` between index values `0` and `(MLKEM_N - 1)` (inclusive) are in the range `0` through `(MLKEM_Q - 1)` (also inclusive). See the macro definition in `mlkem/cbmc.h` for details.
+`ARRAY_BOUND` is a macro that expands to a quantified expression that expresses that the elemtns of `a->coeffs` between index values `0` and `(MLKEM_N - 1)` (inclusive) are in the range `0` through `(MLKEM_Q - 1)` (also inclusive). See the macro definition in `mlkem/cbmc.h` for details.
 
 ### Interior contracts and loop invariants
 
diff --git a/mlkem/cbmc.h b/mlkem/cbmc.h
index 6a5b2bc64..f421a64f3 100644
--- a/mlkem/cbmc.h
+++ b/mlkem/cbmc.h
@@ -109,7 +109,7 @@
 // range value_lb .. value_ub (inclusive)"
 //
 // Example:
-//  ARRAY_IN_BOUNDS(0, MLKEM_N-1, a->coeffs, -(MLKEM_Q - 1), MLKEM_Q - 1)
+//  ARRAY_BOUND(a->coeffs, 0, MLKEM_N-1, -(MLKEM_Q - 1), MLKEM_Q - 1)
 // expands to
 //  __CPROVER_forall { int k; (0 <= k && k <= MLKEM_N-1) ==> ( (-(MLKEM_Q -
 //  1) <= a->coeffs[k]) && (a->coeffs[k] <= (MLKEM_Q - 1))) }
@@ -120,7 +120,7 @@
 #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, \
+#define ARRAY_BOUND_CORE(indextype, qvar, qvar_lb, qvar_ub, array_var, \
                         value_lb, value_ub)                           \
   __CPROVER_forall                                                    \
   {                                                                   \
@@ -130,15 +130,15 @@
            ((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__),  \
+#define ARRAY_BOUND(array_var, qvar_lb, qvar_ub,                  \
+                        value_lb, value_ub)                           \
+    ARRAY_BOUND_CORE(int, CBMC_CONCAT(_cbmc_idx,__LINE__),        \
      (qvar_lb), (qvar_ub), (array_var), (value_lb), (value_ub))
 
 // clang-format on
 
-// Wrapper around ARRAY_IN_BOUNDS operating on absolute values
+// Wrapper around ARRAY_BOUND operating on absolute values
 #define ARRAY_ABS_BOUND(arr, lb, ub, k) \
-  ARRAY_IN_BOUNDS((lb), (ub), (arr), (-(k)), (k))
+  ARRAY_BOUND((arr), (lb), (ub), (-(k)), (k))
 
 #endif
diff --git a/mlkem/indcpa.c b/mlkem/indcpa.c
index e749cdc52..5132f569c 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(0, MLKEM_N - 1, pk->vec[k0].coeffs, 0, (MLKEM_Q - 1))))
+  ARRAY_BOUND(pk->vec[k0].coeffs, 0, MLKEM_N - 1, 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(0, MLKEM_N - 1, pk->vec[k0].coeffs, 0, (MLKEM_Q - 1))))
+  ARRAY_BOUND(pk->vec[k0].coeffs, 0, MLKEM_N - 1, 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(0, MLKEM_N - 1, sk->vec[k0].coeffs, 0, (MLKEM_Q - 1))))
+  ARRAY_BOUND(sk->vec[k0].coeffs, 0, MLKEM_N - 1,  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(0, MLKEM_N - 1, sk->vec[k0].coeffs, 0, (MLKEM_Q - 1))))
+  ARRAY_BOUND(sk->vec[k0].coeffs, 0, MLKEM_N - 1,  0, (MLKEM_Q - 1))))
 ASSIGNS(OBJECT_WHOLE(sk))  // clang-format on
 {
   polyvec_frombytes(sk, packedsk);
@@ -184,10 +184,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(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)))
+  ENSURES(ARRAY_BOUND(vec[0].coeffs, 0, MLKEM_N - 1, 0, (MLKEM_Q - 1)))
+  ENSURES(ARRAY_BOUND(vec[1].coeffs, 0, MLKEM_N - 1, 0, (MLKEM_Q - 1)))
+  ENSURES(ARRAY_BOUND(vec[2].coeffs, 0, MLKEM_N - 1, 0, (MLKEM_Q - 1)))
+  ENSURES(ARRAY_BOUND(vec[3].coeffs, 0, MLKEM_N - 1, 0, (MLKEM_Q - 1)))
 // clang-format on
 {
   // Temporary buffers for XOF output before rejection sampling
@@ -223,10 +223,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(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)))
+    INVARIANT(ctr[0] > 0 ==> ARRAY_BOUND(vec[0].coeffs, 0, ctr[0] - 1, 0, (MLKEM_Q - 1)))
+    INVARIANT(ctr[1] > 0 ==> ARRAY_BOUND(vec[1].coeffs, 0, ctr[1] - 1, 0, (MLKEM_Q - 1)))
+    INVARIANT(ctr[2] > 0 ==> ARRAY_BOUND(vec[2].coeffs, 0, ctr[2] - 1, 0, (MLKEM_Q - 1)))
+    INVARIANT(ctr[3] > 0 ==> ARRAY_BOUND(vec[3].coeffs, 0, ctr[3] - 1, 0, (MLKEM_Q - 1)))
                             // clang-format on
     {
       shake128x4_squeezeblocks(buf0, buf1, buf2, buf3, 1, &statex);
@@ -247,7 +247,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(0, MLKEM_N - 1, entry->coeffs, 0, (MLKEM_Q - 1)))
+  ENSURES(ARRAY_BOUND(entry->coeffs, 0, MLKEM_N - 1, 0, (MLKEM_Q - 1)))
 {  // clang-format on
   shake128ctx state;
   uint8_t buf[GEN_MATRIX_NBLOCKS * SHAKE128_RATE];
@@ -266,7 +266,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(0, ctr - 1, entry->coeffs,
+    INVARIANT(ctr > 0 ==> ARRAY_BOUND(entry->coeffs, 0, ctr - 1, 
                                           0, (MLKEM_Q - 1)))  // clang-format on
     {
       shake128_squeezeblocks(buf, 1, &state);
diff --git a/mlkem/indcpa.h b/mlkem/indcpa.h
index a62b9b4a3..8647cc111 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(0, MLKEM_N - 1, a[x].vec[y].coeffs, 0, (MLKEM_Q - 1)))));
+  ARRAY_BOUND(a[x].vec[y].coeffs, 0, MLKEM_N - 1, 0, (MLKEM_Q - 1)))));
 // clang-format on
 
 #define indcpa_keypair_derand MLKEM_NAMESPACE(indcpa_keypair_derand)
diff --git a/mlkem/poly.c b/mlkem/poly.c
index 642f3e490..cafab2e05 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(0, (j-1), t, 0, 15))
+        INVARIANT(ARRAY_BOUND(t, 0, (j-1), 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(0, (j-1), t, 0, 31))
+        INVARIANT(ARRAY_BOUND(t, 0, (j-1), 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(0, (2 * i - 1), r->coeffs, 0, (MLKEM_Q - 1)))
+        INVARIANT(ARRAY_BOUND(r->coeffs, 0, (2 * i - 1), 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(0, (8 * i - 1), r->coeffs, 0, (MLKEM_Q - 1)))
+    INVARIANT(ARRAY_BOUND(r->coeffs, 0, (8 * i - 1), 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(0, (8 * i + j - 1), r->coeffs, 0, (MLKEM_Q - 1)))
+        INVARIANT(ARRAY_BOUND(r->coeffs, 0, (8 * i + j - 1), 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(0, (2 * i - 1), r->coeffs, 0, 4095))
+    INVARIANT(ARRAY_BOUND(r->coeffs, 0, (2 * i - 1), 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(0, (8 * i - 1), r->coeffs, 0, (MLKEM_Q - 1)))
+    INVARIANT(ARRAY_BOUND(r->coeffs, 0, (8 * i - 1), 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(0, (8 * i + j - 1), r->coeffs, 0, (MLKEM_Q - 1)))
+        INVARIANT(ARRAY_BOUND(r->coeffs, 0, (8 * i + j - 1), 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);
@@ -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(0, (i - 1), r->coeffs, 0, (MLKEM_Q - 1)))
+    INVARIANT(ARRAY_BOUND(r->coeffs, 0, (i - 1), 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 9a26c279c..62dc452cd 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(0, (MLKEM_N - 1), a->coeffs, 0, (MLKEM_Q - 1)))
+REQUIRES(ARRAY_BOUND(a->coeffs, 0, (MLKEM_N - 1), 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(0, (MLKEM_N - 1), r->coeffs, 0, (MLKEM_Q - 1)));
+ENSURES(ARRAY_BOUND(r->coeffs, 0, (MLKEM_N - 1), 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(0, (MLKEM_N - 1), a->coeffs, 0, (MLKEM_Q - 1)))
+REQUIRES(ARRAY_BOUND(a->coeffs, 0, (MLKEM_N - 1), 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(0, (MLKEM_N - 1), r->coeffs, 0, 4095));
+ENSURES(ARRAY_BOUND(r->coeffs, 0, (MLKEM_N - 1), 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(0, (MLKEM_N - 1), r->coeffs, 0, (MLKEM_Q - 1)));
+ENSURES(ARRAY_BOUND(r->coeffs, 0, (MLKEM_N - 1), 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(0, (MLKEM_N - 1), r->coeffs, 0, (MLKEM_Q - 1)))
+REQUIRES(ARRAY_BOUND(r->coeffs, 0, (MLKEM_N - 1), 0, (MLKEM_Q - 1)))
 ASSIGNS(OBJECT_WHOLE(msg));
 // clang-format on
 
@@ -627,7 +627,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(0, MLKEM_N - 1, r->coeffs, 0, (MLKEM_Q - 1)));
+ENSURES(ARRAY_BOUND(r->coeffs, 0, MLKEM_N - 1, 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 6f34c3a78..9a6d85926 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(0, MLKEM_N - 1, r->vec[r0].coeffs, 0, (MLKEM_Q - 1))))
+      ARRAY_BOUND(r->vec[r0].coeffs,0, MLKEM_N - 1, 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(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)))
+          ARRAY_BOUND(r->vec[r0].coeffs, 0, MLKEM_N - 1, 0, (MLKEM_Q - 1))))
+        INVARIANT(ARRAY_BOUND(r->vec[i].coeffs, 0, 8 * j - 1, 0, (MLKEM_Q - 1)))
         {  // clang-format on
           uint16_t t[8];
           uint8_t const *base = &a[11 * (i * (MLKEM_N / 8) + j)];
@@ -136,10 +136,10 @@ 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(0, MLKEM_N - 1,
-                r->vec[r0].coeffs, 0, (MLKEM_Q - 1))))
-            INVARIANT(ARRAY_IN_BOUNDS(0, 8 * j + k - 1,
-              r->vec[i].coeffs, 0, (MLKEM_Q - 1)))
+              ARRAY_BOUND(r->vec[r0].coeffs, 0, MLKEM_N - 1,
+                0, (MLKEM_Q - 1))))
+            INVARIANT(ARRAY_BOUND(r->vec[i].coeffs, 0, 8 * j + k - 1,
+              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(0, MLKEM_N - 1, r->vec[r0].coeffs, 0, (MLKEM_Q - 1))))
+    ARRAY_BOUND(r->vec[r0].coeffs, 0, MLKEM_N - 1, 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(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)))
+          ARRAY_BOUND(r->vec[r0].coeffs, 0, MLKEM_N - 1, 0, (MLKEM_Q - 1))))
+        INVARIANT(ARRAY_BOUND(r->vec[i].coeffs, 0, 4 * j - 1, 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(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)))
+              ARRAY_BOUND(r->vec[r0].coeffs, 0, MLKEM_N - 1, 0, (MLKEM_Q - 1))))
+            INVARIANT(ARRAY_BOUND(r->vec[i].coeffs, 0, 4 * j + k - 1, 0, (MLKEM_Q - 1)))
             {  // clang-format on
               r->vec[i].coeffs[4 * j + k] = scalar_decompress_d10(t[k]);
             }
diff --git a/mlkem/polyvec.h b/mlkem/polyvec.h
index 4ed3a4c42..53cc96bf5 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(0, (MLKEM_N - 1), a->vec[k0].coeffs, 0, (MLKEM_Q - 1))));
+         ARRAY_BOUND(a->vec[k0].coeffs, 0, (MLKEM_N - 1), 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(0, (MLKEM_N - 1), r->vec[k0].coeffs, 0, (MLKEM_Q - 1))));
+         ARRAY_BOUND(r->vec[k0].coeffs, 0, (MLKEM_N - 1), 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(0, (MLKEM_N - 1), a->vec[k0].coeffs, 0, (MLKEM_Q - 1))))
+         ARRAY_BOUND(a->vec[k0].coeffs, 0, (MLKEM_N - 1), 0, (MLKEM_Q - 1))))
 ASSIGNS(OBJECT_WHOLE(r));
 // clang-format on
 
@@ -84,8 +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(0, (MLKEM_N - 1),
-                        r->vec[k0].coeffs, 0, 4095)))
+        ARRAY_BOUND(r->vec[k0].coeffs, 0, (MLKEM_N - 1), 0, 4095)))
 ASSIGNS(OBJECT_WHOLE(r));  // clang-format on
 
 #define polyvec_ntt MLKEM_NAMESPACE(polyvec_ntt)
@@ -224,7 +223,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(0, MLKEM_N - 1, r->vec[k0].coeffs, 0, (MLKEM_Q - 1))));
+  ARRAY_BOUND(r->vec[k0].coeffs, 0, MLKEM_N - 1, 0, (MLKEM_Q - 1))));
 // clang-format on
 
 #define polyvec_add MLKEM_NAMESPACE(polyvec_add)
diff --git a/mlkem/rej_uniform.c b/mlkem/rej_uniform.c
index 2a8c11398..748670a6c 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(0, ctr - 1, r, 0, (MLKEM_Q - 1)))  // clang-format on
+    INVARIANT(ctr > 0 ==> ARRAY_BOUND(r, 0, ctr - 1, 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 c731ca06b..8be7fd6fc 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(0, offset - 1, r, 0, (MLKEM_Q - 1)))
+REQUIRES(offset > 0 ==> ARRAY_BOUND(r, 0, offset - 1, 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(0, RETURN_VALUE - 1, r, 0, (MLKEM_Q - 1)));
+ENSURES(RETURN_VALUE > 0 ==> ARRAY_BOUND(r, 0, RETURN_VALUE - 1, 0, (MLKEM_Q - 1)));
 // clang-format on
 #endif