CBMC: Use ARRAY_ABS_BOUND everywhere

#371 introduced a new macro ARRAY_ABS_BOUND for bounds that are centered around zero. This commit makes use of that macro everywhere. Resolves #379 Signed-off-by: Matthias J. Kannwischer <[email protected]>
pq-code-package · Nov 12, 2024 · 6b0489b · 6b0489b
1 parent 705f78b
commit 6b0489b
Show file tree

Hide file tree

Showing 8 changed files with 34 additions and 43 deletions.
diff --git 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(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;

diff --git 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(0, MLKEM_N - 1, r->coeffs, -MLKEM_ETA1, MLKEM_ETA1));
+ENSURES(ARRAY_ABS_BOUND(r->coeff, 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
diff --git a/mlkem/indcpa.c b/mlkem/indcpa.c
@@ -373,8 +373,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
 {

diff --git a/mlkem/ntt.h b/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
 
 

diff --git a/mlkem/poly.c b/mlkem/poly.c
@@ -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);
     }

diff --git a/mlkem/poly.h b/mlkem/poly.h
@@ -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(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));
+    ARRAY_ABS_BOUND(r0->coeffs,0, MLKEM_N - 1, MLKEM_ETA1)
+ && ARRAY_ABS_BOUND(r1->coeffs,0, MLKEM_N - 1, MLKEM_ETA1)
+ && ARRAY_ABS_BOUND(r2->coeffs,0, MLKEM_N - 1, MLKEM_ETA1)
+ && ARRAY_ABS_BOUND(r3->coeffs,0, MLKEM_N - 1, 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(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
 
 #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(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));
+    ARRAY_ABS_BOUND(r0->coeffs,0, MLKEM_N - 1, MLKEM_ETA1) \
+ && ARRAY_ABS_BOUND(r1->coeffs,0, MLKEM_N - 1, MLKEM_ETA1) \
+ && ARRAY_ABS_BOUND(r2->coeffs,0, MLKEM_N - 1, MLKEM_ETA2) \
+ && ARRAY_ABS_BOUND(r3->coeffs,0, MLKEM_N - 1, 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(0, MLKEM_N - 1, a->coeffs, -(MLKEM_Q - 1), (MLKEM_Q - 1)))
+REQUIRES(ARRAY_ABS_BOUND(a->coeffs, 0, MLKEM_N - 1, (MLKEM_Q - 1)))
 ASSIGNS(OBJECT_WHOLE(r))
-ENSURES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r->coeffs, -(3 * HALF_Q - 1), (3 * HALF_Q - 1)));
+ENSURES(ARRAY_ABS_BOUND(r->coeffs, 0, MLKEM_N - 1, (3 * HALF_Q - 1)));
 // clang-format on
 
 #define poly_tomont MLKEM_NAMESPACE(poly_tomont)
@@ -578,7 +578,7 @@ ENSURES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r->coeffs, -(3 * HALF_Q - 1), (3 * HALF_
 void poly_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, -(MLKEM_Q - 1), (MLKEM_Q - 1)));
+ENSURES(ARRAY_ABS_BOUND(r->coeffs, 0, MLKEM_N - 1, (MLKEM_Q - 1)));
 // clang-format on
 
 // REF-CHANGE: This function does not exist in the reference implementation

diff --git a/mlkem/polyvec.c b/mlkem/polyvec.c
@@ -249,8 +249,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(0, MLKEM_N - 1, r->coeffs,
-                              i * (-(3 * HALF_Q - 1)), i * (3 * HALF_Q - 1)))
+    INVARIANT(ARRAY_ABS_BOUND(r->coeffs, 0, MLKEM_N - 1, i * (3 * HALF_Q - 1)))
     DECREASES(MLKEM_K - i)
     // clang-format on
     {
@@ -263,10 +262,8 @@ 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(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_ABS_BOUND(r->coeffs, 0, MLKEM_N - 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
@@ -106,12 +106,10 @@ ASSIGNS(OBJECT_WHOLE(r));  // clang-format on
 void polyvec_ntt(polyvec *r)  // clang-format off
   REQUIRES(IS_FRESH(r, sizeof(polyvec)))
   REQUIRES(FORALL(int, j, 0, MLKEM_K - 1,
-    ARRAY_IN_BOUNDS(0, MLKEM_N - 1,
-                    r->vec[j].coeffs, -(MLKEM_Q - 1), (MLKEM_Q - 1))))
+    ARRAY_ABS_BOUND(r->vec[j].coeffs, 0, MLKEM_N - 1, (MLKEM_Q - 1))))
   ASSIGNS(OBJECT_WHOLE(r))
   ENSURES(FORALL(int, j, 0, MLKEM_K - 1,
-    ARRAY_IN_BOUNDS(0, MLKEM_N - 1,
-                    r->vec[j].coeffs, -(NTT_BOUND - 1), (NTT_BOUND - 1))));
+    ARRAY_ABS_BOUND(r->vec[j].coeffs, 0, MLKEM_N - 1, (NTT_BOUND - 1))));
 // clang-format on
 
 #define polyvec_invntt_tomont MLKEM_NAMESPACE(polyvec_invntt_tomont)
@@ -134,8 +132,7 @@ void polyvec_invntt_tomont(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(0, MLKEM_N - 1,
-                    r->vec[j].coeffs, -(INVNTT_BOUND - 1), (INVNTT_BOUND - 1))));
+    ARRAY_ABS_BOUND(r->vec[j].coeffs, 0, MLKEM_N - 1, (INVNTT_BOUND - 1))));
 // clang-format on
 
 #define polyvec_basemul_acc_montgomery \
@@ -172,8 +169,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(0, MLKEM_N - 1,
-   a->vec[k1].coeffs, -(MLKEM_Q - 1), (MLKEM_Q - 1))))
+ ARRAY_ABS_BOUND(a->vec[k1].coeffs, 0, MLKEM_N - 1, (MLKEM_Q - 1))))
 ASSIGNS(OBJECT_UPTO(r, sizeof(poly)));
 // clang-format on
 
@@ -274,8 +270,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(0, MLKEM_N - 1,
-                    r->vec[j].coeffs, -(MLKEM_Q - 1), (MLKEM_Q - 1))))
+    ARRAY_ABS_BOUND(r->vec[j].coeffs, 0, MLKEM_N - 1, (MLKEM_Q - 1))))
   ASSIGNS(OBJECT_WHOLE(r));
 // clang-format on