Merge pull request #381 from pq-code-package/cbmc-cleanup

CBMC: More minor clean-up

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
 

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(0, (8 * i - 1), r->coeffs, -2, +2))  // clang-format on
+    INVARIANT(ARRAY_ABS_BOUND(r->coeffs, 0, (8 * i - 1), 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(0, 8 * i + j - 1, r->coeffs, -2, +2))  // clang-format on
+        INVARIANT(ARRAY_ABS_BOUND(r->coeffs, 0, 8 * i + j - 1, 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(0, (4 * i - 1), r->coeffs, -3, +3))  // clang-format on
+    INVARIANT(ARRAY_ABS_BOUND(r->coeffs, 0, (4 * i - 1), 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(0, 4 * i + j - 1, r->coeffs, -3, +3))  // clang-format on
+        INVARIANT(ARRAY_ABS_BOUND(r->coeffs, 0, 4 * i + j - 1, 3))  // clang-format on
         {
           a = (d >> (6 * j + 0)) & 0x7;
           b = (d >> (6 * j + 3)) & 0x7;

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(0, MLKEM_N - 1, r->coeffs, -MLKEM_ETA1, MLKEM_ETA1));
+ENSURES(ARRAY_ABS_BOUND(r->coeffs, 0, MLKEM_N - 1, 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(0, MLKEM_N - 1, r->coeffs, -MLKEM_ETA2, MLKEM_ETA2));
+ENSURES(ARRAY_ABS_BOUND(r->coeffs, 0, MLKEM_N - 1, MLKEM_ETA2));
 // clang-format on
 
 #endif

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

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);
@@ -162,8 +162,8 @@ REQUIRES(IS_FRESH(c, MLKEM_INDCPA_BYTES))
 ASSIGNS(OBJECT_WHOLE(b))
 ASSIGNS(OBJECT_WHOLE(v))
 ENSURES(FORALL(int, k0, 0, MLKEM_K - 1,
-         ARRAY_IN_BOUNDS(0, (MLKEM_N - 1), b->vec[k0].coeffs, 0, (MLKEM_Q - 1))))
-ENSURES(ARRAY_IN_BOUNDS(0, (MLKEM_N - 1), v->coeffs, 0, (MLKEM_Q - 1)))
+         ARRAY_BOUND(b->vec[k0].coeffs, 0, (MLKEM_N - 1), 0, (MLKEM_Q - 1))))
+ENSURES(ARRAY_BOUND(v->coeffs, 0, (MLKEM_N - 1), 0, (MLKEM_Q - 1)))
 // clang-format on
 {
   polyvec_decompress(b, c);
@@ -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);
@@ -384,8 +384,7 @@ void matvec_mul(polyvec *out, const polyvec a[MLKEM_K], const polyvec *v,
   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(0, MLKEM_N - 1,
-       a[k0].vec[k1].coeffs, -(MLKEM_Q - 1), (MLKEM_Q - 1)))))
+     ARRAY_ABS_BOUND(a[k0].vec[k1].coeffs, 0, MLKEM_N - 1, (MLKEM_Q - 1)))))
   ASSIGNS(OBJECT_WHOLE(out))
 // clang-format on
 {

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)

mlkem/ntt.h

@@ -33,9 +33,9 @@ extern const int16_t zetas[128];
 #define poly_ntt MLKEM_NAMESPACE(poly_ntt)
 void poly_ntt(poly *r)  // clang-format off
 REQUIRES(IS_FRESH(r, sizeof(poly)))
-REQUIRES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r->coeffs, -(MLKEM_Q - 1), MLKEM_Q - 1))
+REQUIRES(ARRAY_ABS_BOUND(r->coeffs, 0, MLKEM_N - 1, MLKEM_Q - 1))
 ASSIGNS(OBJECT_UPTO(r, sizeof(poly)))
-ENSURES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r->coeffs, -(NTT_BOUND - 1), NTT_BOUND - 1));
+ENSURES(ARRAY_ABS_BOUND(r->coeffs, 0, MLKEM_N - 1, NTT_BOUND - 1));
 // clang-format on
 
 /*************************************************
@@ -58,7 +58,7 @@ ENSURES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r->coeffs, -(NTT_BOUND - 1), NTT_BOUND -
 void poly_invntt_tomont(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, -(INVNTT_BOUND - 1), INVNTT_BOUND - 1));
+ENSURES(ARRAY_ABS_BOUND(r->coeffs, 0, MLKEM_N - 1, INVNTT_BOUND - 1));
 // clang-format on
 
 #define basemul_cached MLKEM_NAMESPACE(basemul_cached)
@@ -87,9 +87,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(0, 1, a, -(MLKEM_Q - 1), (MLKEM_Q - 1)))
+REQUIRES(ARRAY_ABS_BOUND(a, 0, 1, MLKEM_Q - 1))
 ASSIGNS(OBJECT_UPTO(r, 2 * sizeof(int16_t)))
-ENSURES(ARRAY_IN_BOUNDS(0, 1, r, -(3 * HALF_Q - 1), (3 * HALF_Q - 1)));
+ENSURES(ARRAY_ABS_BOUND(r, 0, 1, (3 * HALF_Q - 1)));
 // clang-format on
 
 

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);
@@ -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(0, (4 * i - 1), r->coeffs, -(3 * HALF_Q - 1), (3 * HALF_Q - 1)))
+    INVARIANT(ARRAY_ABS_BOUND(r->coeffs, 0, (4 * i - 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(0, (i - 1), r->coeffs, -(MLKEM_Q - 1), (MLKEM_Q - 1)))
+    INVARIANT(ARRAY_ABS_BOUND(r->coeffs ,0, (i - 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(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]);