From 6317a518ba25444e99b0517d064c8756636ebe71 Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Wed, 13 Nov 2024 19:36:46 +0000 Subject: [PATCH] CBMC: Minor cleanup in invNTT proof Signed-off-by: Hanno Becker --- mlkem/ntt.c | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/mlkem/ntt.c b/mlkem/ntt.c index 82521e0f9..dcb5a1dc2 100644 --- a/mlkem/ntt.c +++ b/mlkem/ntt.c @@ -143,7 +143,7 @@ void ntt_layer(int16_t r[MLKEM_N], int len, int layer) // clang-format off ENSURES(ARRAY_ABS_BOUND(r, 0, MLKEM_N - 1, (layer + 1) * MLKEM_Q - 1)) // clang-format on { - // `layer` is a ghost variable only needed in the specification + // `layer` is a ghost variable only needed in the CBMC specification ((void)layer); // Twiddle factors for layer n start at index 2^(layer-1) int k = MLKEM_N / (2 * len); @@ -208,11 +208,11 @@ STATIC_ASSERT(INVNTT_BOUND_REF <= INVNTT_BOUND, invntt_bound) // Compute one layer of inverse NTT STATIC_TESTABLE void invntt_layer(int16_t *r, int len, int layer) // clang-format off - REQUIRES(IS_FRESH(r, sizeof(poly))) + REQUIRES(IS_FRESH(r, sizeof(int16_t) * MLKEM_N)) REQUIRES(2 <= len && len <= 128 && 1 <= layer && layer <= 7) REQUIRES(len == (1 << (8 - layer))) REQUIRES(ARRAY_ABS_BOUND(r, 0, MLKEM_N - 1, MLKEM_Q)) - ASSIGNS(OBJECT_UPTO(r, sizeof(poly))) + ASSIGNS(OBJECT_UPTO(r, sizeof(int16_t) * MLKEM_N)) ENSURES(ARRAY_ABS_BOUND(r, 0, MLKEM_N - 1, MLKEM_Q)) // clang-format on { @@ -252,7 +252,7 @@ void poly_invntt_tomont(poly *p) { // absolute value < MLKEM_Q. for (int j = 0; j < MLKEM_N; j++) // clang-format off - ASSIGNS(j, OBJECT_UPTO(r, sizeof(poly))) + ASSIGNS(j, OBJECT_UPTO(r, sizeof(int16_t) * MLKEM_N)) INVARIANT(0 <= j && j <= MLKEM_N && ARRAY_ABS_BOUND(r, 0, j - 1, MLKEM_Q)) // clang-format on { @@ -262,7 +262,7 @@ void poly_invntt_tomont(poly *p) { // Run the invNTT layers for (int len = 2, layer = 7; len <= 128; len <<= 1, layer--) // clang-format off - ASSIGNS(len, layer, OBJECT_UPTO(r, sizeof(poly))) + ASSIGNS(len, layer, OBJECT_UPTO(r, sizeof(int16_t) * MLKEM_N)) INVARIANT(2 <= len && len <= 256 && 0 <= layer && layer <= 7 && len == (1 << (8 - layer))) INVARIANT(ARRAY_ABS_BOUND(r, 0, MLKEM_N - 1, MLKEM_Q)) // clang-format on