From d0ec687b7069106bd126927f9b697a6cc9027ad9 Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Mon, 11 Nov 2024 15:00:15 +0000 Subject: [PATCH] Improve CBMC proof for forward NTT --- cbmc/proofs/ntt_butterfly_block_at/Makefile | 2 +- .../ntt_butterfly_block_at_harness.c | 5 +- mlkem/cbmc.h | 9 ++ mlkem/ntt.c | 95 ++++++------------- 4 files changed, 43 insertions(+), 68 deletions(-) diff --git a/cbmc/proofs/ntt_butterfly_block_at/Makefile b/cbmc/proofs/ntt_butterfly_block_at/Makefile index e34a1be3f..e6777279c 100644 --- a/cbmc/proofs/ntt_butterfly_block_at/Makefile +++ b/cbmc/proofs/ntt_butterfly_block_at/Makefile @@ -19,7 +19,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/ntt.c CHECK_FUNCTION_CONTRACTS=ntt_butterfly_block_at -USE_FUNCTION_CONTRACTS= ntt_butterfly_block +USE_FUNCTION_CONTRACTS= $(MLKEM_NAMESPACE)fqmul #ntt_butterfly_block APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/cbmc/proofs/ntt_butterfly_block_at/ntt_butterfly_block_at_harness.c b/cbmc/proofs/ntt_butterfly_block_at/ntt_butterfly_block_at_harness.c index c8f57e8bb..44c65ed54 100644 --- a/cbmc/proofs/ntt_butterfly_block_at/ntt_butterfly_block_at_harness.c +++ b/cbmc/proofs/ntt_butterfly_block_at/ntt_butterfly_block_at_harness.c @@ -10,8 +10,7 @@ * @brief Implements the proof harness for ntt_butterfly_block_at function. */ #include -void ntt_butterfly_block_at(int16_t *p, int16_t root, int sz, int base, - int stride, int bound); +void ntt_butterfly_block_at(int16_t *r, int16_t root, int start, int len, int bound); /** * @brief Starting point for formal analysis @@ -20,5 +19,5 @@ void ntt_butterfly_block_at(int16_t *p, int16_t root, int sz, int base, void harness(void) { int16_t *r, root; int sz, base, stride, bound; - ntt_butterfly_block_at(r, root, sz, base, stride, bound); + ntt_butterfly_block_at(r, root, base, stride, bound); } diff --git a/mlkem/cbmc.h b/mlkem/cbmc.h index 2ed331801..d4d4d86d5 100644 --- a/mlkem/cbmc.h +++ b/mlkem/cbmc.h @@ -4,6 +4,8 @@ // Basic replacements for __CPROVER_XXX contracts /////////////////////////////////////////////////// +#include "common.h" + #ifndef CBMC #define STATIC_TESTABLE static @@ -126,4 +128,11 @@ } // clang-format on +// Helper macros to make NTT contracts and invariants more readable +// TODO: Consolidate this with the macros in cbmc.h +#define SCALAR_ABS_BOUND(a, k) (-(k) <= (a) && (a) <= (k)) +#define ARRAY_ABS_BOUND(arr, lb, ub, k) \ + ARRAY_IN_BOUNDS(int, MLKEM_CONCAT(i, __LINE__), (lb), (ub), (arr), \ + (-(k) + 1), ((k) - 1)) + #endif diff --git a/mlkem/ntt.c b/mlkem/ntt.c index f31b76498..49ebab430 100644 --- a/mlkem/ntt.c +++ b/mlkem/ntt.c @@ -74,82 +74,49 @@ const int16_t zetas[128] = { **************************************************/ #if !defined(MLKEM_USE_NATIVE_NTT) -// Helper macros to make NTT contracts and invariants more readable -// TODO: Consolidate this with the macros in cbmc.h -#define SCALAR_IN_BOUNDS(a, lb, ub) ((lb) <= (a) && (a) <= (ub)) -#define SCALAR_Q_BOUND(a, k) \ - SCALAR_IN_BOUNDS((a), (-(k) * MLKEM_Q + 1), ((k) * MLKEM_Q - 1)) -#define ARRAY_Q_BOUND(arr, lb, ub, k) \ - ARRAY_IN_BOUNDS(int, MLKEM_CONCAT(i, __LINE__), (lb), (ub), (arr), \ - (-(k) * MLKEM_Q + 1), ((k) * MLKEM_Q - 1)) - // Compute a block CT butterflies with a fixed twiddle factor -STATIC_TESTABLE // clang-format off -void ntt_butterfly_block(int16_t *r, int16_t root, int stride, int bound) - REQUIRES(1 <= stride && stride <= 128) - REQUIRES(1 <= bound && bound <= 7) - REQUIRES(IS_FRESH(r, 4 * stride)) - REQUIRES(SCALAR_IN_BOUNDS(root, -HALF_Q + 1, HALF_Q - 1)) - REQUIRES(ARRAY_Q_BOUND(r, 0, (2 * stride - 1), bound)) - ASSIGNS(OBJECT_UPTO(r, sizeof(int16_t) * 2 * stride)) - ENSURES(ARRAY_Q_BOUND(r, 0, (2 * stride - 1), bound+1)) +STATIC_TESTABLE // clang-format off +void ntt_butterfly_block_at(int16_t *r, int16_t root, int start, int len, int bound) + REQUIRES(0 <= start && start < MLKEM_N && 1 <= len && len <= MLKEM_N / 2 && start + 2 * len <= MLKEM_N) + REQUIRES(0 <= bound && bound < INT16_MAX - MLKEM_Q) + REQUIRES(IS_FRESH(r, sizeof(int16_t) * MLKEM_N)) + REQUIRES(SCALAR_ABS_BOUND(root, HALF_Q - 1)) + REQUIRES(ARRAY_ABS_BOUND(r, 0, start - 1, bound + MLKEM_Q)) + REQUIRES(ARRAY_ABS_BOUND(r, start, MLKEM_N - 1, bound)) + ASSIGNS(OBJECT_UPTO(r, sizeof(int16_t) * MLKEM_N)) + ENSURES(ARRAY_ABS_BOUND(r, 0, start + 2*len - 1, bound + MLKEM_Q)) + ENSURES(ARRAY_ABS_BOUND(r, start + 2 * len, MLKEM_N - 1, bound)) +// clang-format on { - // Used for the specification only - ((void) bound); + // Parameter only used in the CBMC specification + ((void)bound); // clang-format off - for (int j = 0; j < stride; j++) - ASSIGNS(j, OBJECT_UPTO(r, sizeof(int16_t) * 2 * stride)) - INVARIANT(0 <= j && j <= stride) - INVARIANT(ARRAY_Q_BOUND(r, 0, j-1, bound+1)) - INVARIANT(ARRAY_Q_BOUND(r, stride, stride + j - 1, bound+1)) - INVARIANT(ARRAY_Q_BOUND(r, j, stride - 1, bound)) - INVARIANT(ARRAY_Q_BOUND(r, stride + j, 2*stride - 1, bound)) + for (int j = start; j < start + len; j++) + ASSIGNS(j, OBJECT_UPTO(r, sizeof(int16_t) * MLKEM_N)) + INVARIANT(start <= j && j <= start + len) + INVARIANT(ARRAY_ABS_BOUND(r, 0, j - 1, bound + MLKEM_Q)) + INVARIANT(ARRAY_ABS_BOUND(r, j, start + len - 1, bound)) + INVARIANT(ARRAY_ABS_BOUND(r, start + len, j + len - 1, bound + MLKEM_Q)) + INVARIANT(ARRAY_ABS_BOUND(r, j + len, MLKEM_N - 1, bound)) // clang-format on { int16_t t; - t = fqmul(r[j + stride], root); - r[j + stride] = r[j] - t; + t = fqmul(r[j + len], root); + r[j + len] = r[j] - t; r[j] = r[j] + t; } } -// Framed version of ntt_bufferly_block -// -// TODO: This only exists because inlining ntt_butterfly_block() leads to -// much longer proof times (in fact, I have not witnessed it finishing so far). -// Even this proof, while seemingly a trivial framing, takes longer than all -// of the 'actual' NTT proof. +// Compute one layer of forward NTT STATIC_TESTABLE -// clang-format off -void ntt_butterfly_block_at(int16_t *p, int16_t root, int sz, int base, int stride, int bound) - REQUIRES(2 <= sz && sz <= 256 && (sz & 1) == 0) - REQUIRES(0 <= base && base < sz && 1 <= stride && stride <= sz / 2 && base + 2 * stride <= sz) - REQUIRES((stride & (stride - 1)) == 0) - REQUIRES((base & (stride - 1)) == 0) - REQUIRES(1 <= bound && bound <= 7) - REQUIRES(IS_FRESH(p, sizeof(int16_t) * sz)) - REQUIRES(SCALAR_IN_BOUNDS(root, -HALF_Q + 1, HALF_Q - 1)) - REQUIRES(ARRAY_Q_BOUND(p, 0, base - 1, bound + 1)) - REQUIRES(ARRAY_Q_BOUND(p, base, sz - 1, bound)) - ASSIGNS(OBJECT_UPTO(p, sizeof(int16_t) * sz)) - ENSURES(ARRAY_Q_BOUND(p, 0, base + 2*stride - 1, bound + 1)) - ENSURES(ARRAY_Q_BOUND(p, base + 2 * stride, sz - 1, bound)) -// clang-format on -{ - // Parameter only used in the CBMC specification - ((void)sz); - ntt_butterfly_block(p + base, root, stride, bound); -} - -STATIC_TESTABLE -// clang-format off void ntt_layer(poly *p, int layer) +// clang-format off REQUIRES(IS_FRESH(p, sizeof(poly))) REQUIRES(1 <= layer && layer <= 7) - REQUIRES(ARRAY_Q_BOUND(p->coeffs, 0, MLKEM_N - 1, layer)) + REQUIRES(ARRAY_ABS_BOUND(p->coeffs, 0, MLKEM_N - 1, layer * MLKEM_Q)) ASSIGNS(OBJECT_UPTO(p, sizeof(poly))) - ENSURES(ARRAY_Q_BOUND(p->coeffs, 0, MLKEM_N - 1, layer + 1)) + ENSURES(ARRAY_ABS_BOUND(p->coeffs, 0, MLKEM_N - 1, (layer + 1) * MLKEM_Q)) // clang-format on { int16_t *r = p->coeffs; @@ -160,12 +127,12 @@ void ntt_layer(poly *p, int layer) ASSIGNS(i, OBJECT_UPTO(r, sizeof(poly))) INVARIANT(1 <= layer && layer <= 7) INVARIANT(0 <= i && i <= blocks) - INVARIANT(ARRAY_Q_BOUND(r, 2 * i * len, MLKEM_N - 1, layer)) - INVARIANT(ARRAY_Q_BOUND(r, 0, 2 * i * len - 1, layer + 1)) + INVARIANT(ARRAY_ABS_BOUND(r, 2 * i * len, MLKEM_N - 1, layer * MLKEM_Q)) + INVARIANT(ARRAY_ABS_BOUND(r, 0, 2 * i * len - 1, layer * MLKEM_Q + MLKEM_Q)) // clang-format off { int16_t zeta = zetas[blocks + i]; - ntt_butterfly_block_at(r, zeta, MLKEM_N, 2 * i * len, len, layer); + ntt_butterfly_block_at(r, zeta, 2 * i * len, len, layer * MLKEM_Q); } } @@ -188,7 +155,7 @@ void poly_ntt(poly *p) { for (int layer = 1; layer < 8; layer++) ASSIGNS(layer, OBJECT_UPTO(p, sizeof(poly))) INVARIANT(1 <= layer && layer <= 8) - INVARIANT(ARRAY_Q_BOUND(p->coeffs, 0, MLKEM_N - 1, layer)) + INVARIANT(ARRAY_ABS_BOUND(p->coeffs, 0, MLKEM_N - 1, layer * MLKEM_Q)) // clang-format on { ntt_layer(p, layer);