From 6925a9dd9472605a3c4e83d4e2cb8109d3850a4a Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Tue, 12 Nov 2024 05:28:54 +0000 Subject: [PATCH] CBMC: Remove index variable from ARRAY_IN_BOUNDS The helper macro ARRAY_IN_BOUNDS unfolds to a CBMC annotation asserting that the coefficients of an array are within specified bounds. Previously, this macro would require the caller to explicitly state the type and name of the index variable, even though this would not actually feature anywhere else in the macro. The original reason for this was that CBMC does not like the same variable name be used twice in block of annotations (precondition, postcondition, loop invariants). This commit simplifies ARRAY_IN_BOUNDS by always picking `int` as the index type, and auto-generating the variable name. Name clashes are avoided by internally appending the line number to the index variable. Signed-off-by: Hanno Becker --- mlkem/cbd.c | 8 ++++---- mlkem/cbd.h | 4 ++-- mlkem/cbmc.h | 17 +++++++++++++---- mlkem/indcpa.c | 32 ++++++++++++++++---------------- mlkem/indcpa.h | 2 +- mlkem/ntt.h | 4 ++-- mlkem/poly.c | 24 ++++++++++++------------ mlkem/poly.h | 38 +++++++++++++++++++------------------- mlkem/polyvec.c | 34 +++++++++++++++++----------------- mlkem/polyvec.h | 16 ++++++++-------- mlkem/rej_uniform.c | 2 +- mlkem/rej_uniform.h | 4 ++-- 12 files changed, 97 insertions(+), 88 deletions(-) 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