From 3135421dad87bf2a4c2b4ca6b9e19f51ffa1ebb0 Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Wed, 20 Nov 2024 11:59:50 +0800 Subject: [PATCH 1/6] Pull poly_{,de}compress_du into function from polyvec_{,de}compress In ML-KEM, we need 3 types of compressions and their resp. decompression: Compress_du, Compress_dv, and Compress_1. Currently Compress_dv is implemented in poly_compress, Compress_du is implemented in polyvec_compress (as it's only needed for vectors), and Compress_1 is implemented in poly_tomsg. This is somewhat confusing. This commit is the frist step to unify this by splitting up polyvec_compress and polyvec_decompress and having them call new functions called poly_compress_du and poly_decompress_du. Signed-off-by: Matthias J. Kannwischer --- cbmc/proofs/polyvec_compress/Makefile | 2 +- cbmc/proofs/polyvec_decompress/Makefile | 8 +- mlkem/params.h | 9 +- mlkem/poly.c | 120 ++++++++++++++++ mlkem/poly.h | 47 +++++++ mlkem/polyvec.c | 173 ++---------------------- mlkem/polyvec.h | 11 ++ 7 files changed, 199 insertions(+), 171 deletions(-) diff --git a/cbmc/proofs/polyvec_compress/Makefile b/cbmc/proofs/polyvec_compress/Makefile index 676a84e28..942ffa318 100644 --- a/cbmc/proofs/polyvec_compress/Makefile +++ b/cbmc/proofs/polyvec_compress/Makefile @@ -19,7 +19,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/polyvec.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_compress -USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_compress_d10 $(MLKEM_NAMESPACE)scalar_compress_d11 +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_compress_du APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/cbmc/proofs/polyvec_decompress/Makefile b/cbmc/proofs/polyvec_decompress/Makefile index 19a1b291d..5cca56a17 100644 --- a/cbmc/proofs/polyvec_decompress/Makefile +++ b/cbmc/proofs/polyvec_decompress/Makefile @@ -13,18 +13,14 @@ DEFINES += INCLUDES += REMOVE_FUNCTION_BODY += -UNWINDSET += +UNWINDSET += $(MLKEM_NAMESPACE)polyvec_decompress.0:4 # Largest value of MLKEM_K PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/polyvec.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_decompress -ifeq ($(MLKEM_K),4) -USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_decompress_d11 -else -USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_decompress_d10 -endif +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_decompress_du APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/mlkem/params.h b/mlkem/params.h index d9f8842d8..addbdf067 100644 --- a/mlkem/params.h +++ b/mlkem/params.h @@ -35,15 +35,18 @@ #if MLKEM_K == 2 #define MLKEM_ETA1 3 #define MLKEM_POLYCOMPRESSEDBYTES 128 -#define MLKEM_POLYVECCOMPRESSEDBYTES (MLKEM_K * 320) +#define MLKEM_POLYCOMPRESSEDBYTES_DU 320 +#define MLKEM_POLYVECCOMPRESSEDBYTES (MLKEM_K * MLKEM_POLYCOMPRESSEDBYTES_DU) #elif MLKEM_K == 3 #define MLKEM_ETA1 2 #define MLKEM_POLYCOMPRESSEDBYTES 128 -#define MLKEM_POLYVECCOMPRESSEDBYTES (MLKEM_K * 320) +#define MLKEM_POLYCOMPRESSEDBYTES_DU 320 +#define MLKEM_POLYVECCOMPRESSEDBYTES (MLKEM_K * MLKEM_POLYCOMPRESSEDBYTES_DU) #elif MLKEM_K == 4 #define MLKEM_ETA1 2 #define MLKEM_POLYCOMPRESSEDBYTES 160 -#define MLKEM_POLYVECCOMPRESSEDBYTES (MLKEM_K * 352) +#define MLKEM_POLYCOMPRESSEDBYTES_DU 352 +#define MLKEM_POLYVECCOMPRESSEDBYTES (MLKEM_K * MLKEM_POLYCOMPRESSEDBYTES_DU) #endif #define MLKEM_ETA2 2 diff --git a/mlkem/poly.c b/mlkem/poly.c index 25c63e072..1b4347d97 100644 --- a/mlkem/poly.c +++ b/mlkem/poly.c @@ -14,6 +14,126 @@ #include "arith_native.h" #include "debug/debug.h" +void poly_compress_du(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_DU], const poly *a) { +#if (MLKEM_POLYCOMPRESSEDBYTES_DU == 352) + uint16_t t[8]; + for (int j = 0; j < MLKEM_N / 8; j++) // clang-format off + ASSIGNS(j, OBJECT_WHOLE(t), OBJECT_WHOLE(r)) + INVARIANT(j >= 0 && j <= MLKEM_N / 8) + { // clang-format on + for (int k = 0; k < 8; k++) // clang-format off + ASSIGNS(k, OBJECT_WHOLE(t), OBJECT_WHOLE(r)) + INVARIANT(k >= 0 && k <= 8) + INVARIANT(FORALL(int, r, 0, k - 1, t[r] < (1u << 11))) + { // clang-format on + t[k] = scalar_compress_d11(a->coeffs[8 * j + k]); + } + + // REF-CHANGE: Use array indexing into + // r rather than pointer-arithmetic to simplify verification + // + // Make all implicit truncation explicit. No data is being + // truncated for the LHS's since each t[i] is 11-bit in size. + r[11 * j + 0] = (t[0] >> 0) & 0xFF; + r[11 * j + 1] = (t[0] >> 8) | ((t[1] << 3) & 0xFF); + r[11 * j + 2] = (t[1] >> 5) | ((t[2] << 6) & 0xFF); + r[11 * j + 3] = (t[2] >> 2) & 0xFF; + r[11 * j + 4] = (t[2] >> 10) | ((t[3] << 1) & 0xFF); + r[11 * j + 5] = (t[3] >> 7) | ((t[4] << 4) & 0xFF); + r[11 * j + 6] = (t[4] >> 4) | ((t[5] << 7) & 0xFF); + r[11 * j + 7] = (t[5] >> 1) & 0xFF; + r[11 * j + 8] = (t[5] >> 9) | ((t[6] << 2) & 0xFF); + r[11 * j + 9] = (t[6] >> 6) | ((t[7] << 5) & 0xFF); + r[11 * j + 10] = (t[7] >> 3); + } +#elif (MLKEM_POLYCOMPRESSEDBYTES_DU == 320) + uint16_t t[4]; + for (int j = 0; j < MLKEM_N / 4; j++) // clang-format off + ASSIGNS(j, OBJECT_WHOLE(t), OBJECT_WHOLE(r)) + INVARIANT(j >= 0 && j <= MLKEM_N / 4) + { // clang-format on + for (int k = 0; k < 4; k++) // clang-format off + ASSIGNS(k, OBJECT_WHOLE(t)) + INVARIANT(k >= 0 && k <= 4) + INVARIANT(FORALL(int, r, 0, k - 1, t[r] < (1u << 10))) + { // clang-format on + t[k] = scalar_compress_d10(a->coeffs[4 * j + k]); + } + + // REF-CHANGE: Use array indexing into + // r rather than pointer-arithmetic to simplify verification + // + // Make all implicit truncation explicit. No data is being + // truncated for the LHS's since each t[i] is 10-bit in size. + r[5 * j + 0] = (t[0] >> 0) & 0xFF; + r[5 * j + 1] = (t[0] >> 8) | ((t[1] << 2) & 0xFF); + r[5 * j + 2] = (t[1] >> 6) | ((t[2] << 4) & 0xFF); + r[5 * j + 3] = (t[2] >> 4) | ((t[3] << 6) & 0xFF); + r[5 * j + 4] = (t[3] >> 2); + } +#else +#error "MLKEM_POLYCOMPRESSEDBYTES_DU needs to be in {320,352}" +#endif +} + + +void poly_decompress_du(poly *r, + const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_DU]) { +#if (MLKEM_POLYCOMPRESSEDBYTES_DU == 352) + 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(ARRAY_BOUND(r->coeffs, 0, 8 * j - 1, 0, (MLKEM_Q - 1))) + { // clang-format on + uint16_t t[8]; + uint8_t const *base = &a[11 * j]; + t[0] = 0x7FF & ((base[0] >> 0) | ((uint16_t)base[1] << 8)); + t[1] = 0x7FF & ((base[1] >> 3) | ((uint16_t)base[2] << 5)); + t[2] = 0x7FF & ((base[2] >> 6) | ((uint16_t)base[3] << 2) | + ((uint16_t)base[4] << 10)); + t[3] = 0x7FF & ((base[4] >> 1) | ((uint16_t)base[5] << 7)); + t[4] = 0x7FF & ((base[5] >> 4) | ((uint16_t)base[6] << 4)); + t[5] = 0x7FF & ((base[6] >> 7) | ((uint16_t)base[7] << 1) | + ((uint16_t)base[8] << 9)); + t[6] = 0x7FF & ((base[8] >> 2) | ((uint16_t)base[9] << 6)); + t[7] = 0x7FF & ((base[9] >> 5) | ((uint16_t)base[10] << 3)); + + for (int k = 0; k < 8; k++) // clang-format off + ASSIGNS(k, OBJECT_WHOLE(r)) + INVARIANT(0 <= k && k <= 8) + INVARIANT(ARRAY_BOUND(r->coeffs, 0, 8 * j + k - 1, 0, (MLKEM_Q - 1))) + { // clang-format on + r->coeffs[8 * j + k] = scalar_decompress_d11(t[k]); + } + } +#elif (MLKEM_POLYCOMPRESSEDBYTES_DU == 320) + 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(ARRAY_BOUND(r->coeffs, 0, 4 * j - 1, 0, (MLKEM_Q - 1))) + { // clang-format on + uint16_t t[4]; + uint8_t const *base = &a[5 * j]; + + t[0] = 0x3FF & ((base[0] >> 0) | ((uint16_t)base[1] << 8)); + t[1] = 0x3FF & ((base[1] >> 2) | ((uint16_t)base[2] << 6)); + t[2] = 0x3FF & ((base[2] >> 4) | ((uint16_t)base[3] << 4)); + t[3] = 0x3FF & ((base[3] >> 6) | ((uint16_t)base[4] << 2)); + + for (int k = 0; k < 4; k++) // clang-format off + ASSIGNS(k, OBJECT_WHOLE(r)) + INVARIANT(0 <= k && k <= 4) + INVARIANT(ARRAY_BOUND(r->coeffs, 0, 4 * j + k - 1, 0, (MLKEM_Q - 1))) + // clang-format on + { + r->coeffs[4 * j + k] = scalar_decompress_d10(t[k]); + } + } +#else +#error "MLKEM_POLYCOMPRESSEDBYTES_DU needs to be in {320,352}" +#endif +} + void poly_compress(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES], const poly *a) { POLY_UBOUND(a, MLKEM_Q); uint8_t t[8] = {0}; diff --git a/mlkem/poly.h b/mlkem/poly.h index 62dc452cd..87576ada8 100644 --- a/mlkem/poly.h +++ b/mlkem/poly.h @@ -304,6 +304,53 @@ uint16_t scalar_signed_to_unsigned_q(int16_t c) // clang-format off return (uint16_t)c; } + +#define poly_compress_du MLKEM_NAMESPACE(poly_compress_du) +/************************************************* + * Name: poly_compress_du + * + * Description: Compression (du bits) and subsequent serialization of a + *polynomial + * + * Arguments: - uint8_t *r: pointer to output byte array + * (of length MLKEM_POLYCOMPRESSEDBYTES) + * - const poly *a: pointer to input polynomial + * Coefficients must be unsigned canonical, + * i.e. in [0,1,..,MLKEM_Q-1]. + **************************************************/ +void poly_compress_du(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_DU], + const poly *a) // clang-format off +REQUIRES(IS_FRESH(r, MLKEM_POLYCOMPRESSEDBYTES_DU)) +REQUIRES(IS_FRESH(a, sizeof(poly))) +REQUIRES(ARRAY_BOUND(a->coeffs, 0, (MLKEM_N - 1), 0, (MLKEM_Q - 1))) +ASSIGNS(OBJECT_UPTO(r, MLKEM_POLYCOMPRESSEDBYTES_DU)); +// clang-format on + + +#define poly_decompress_du MLKEM_NAMESPACE(poly_decompress_du) +/************************************************* + * Name: poly_decompress_du + * + * Description: De-serialization and subsequent decompression (du bits) of a + *polynomial; approximate inverse of poly_compress_du + * + * Arguments: - poly *r: pointer to output polynomial + * - const uint8_t *a: pointer to input byte array + * (of length MLKEM_POLYCOMPRESSEDBYTES bytes) + * + * Upon return, the coefficients of the output polynomial are unsigned-canonical + * (non-negative and smaller than MLKEM_Q). + * + **************************************************/ +void poly_decompress_du( + poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_DU]) // clang-format off +REQUIRES(IS_FRESH(a, MLKEM_POLYCOMPRESSEDBYTES_DU)) +REQUIRES(IS_FRESH(r, sizeof(poly))) +ASSIGNS(OBJECT_UPTO(r, sizeof(poly))) +ENSURES(ARRAY_BOUND(r->coeffs, 0, (MLKEM_N - 1), 0, (MLKEM_Q - 1))); +// clang-format on + + #define poly_compress MLKEM_NAMESPACE(poly_compress) /************************************************* * Name: poly_compress diff --git a/mlkem/polyvec.c b/mlkem/polyvec.c index 9a6d85926..ef569ac66 100644 --- a/mlkem/polyvec.c +++ b/mlkem/polyvec.c @@ -10,177 +10,28 @@ #include "debug/debug.h" void polyvec_compress(uint8_t r[MLKEM_POLYVECCOMPRESSEDBYTES], const polyvec *a) { + unsigned int i; POLYVEC_UBOUND(a, MLKEM_Q); -#if (MLKEM_POLYVECCOMPRESSEDBYTES == (MLKEM_K * 352)) - uint16_t t[8]; - for (int i = 0; i < MLKEM_K; i++) // clang-format off - ASSIGNS(i, OBJECT_WHOLE(t), OBJECT_WHOLE(r)) - INVARIANT(i >= 0 && i <= MLKEM_K) // clang-format on + for (i = 0; i < MLKEM_K; i++) // clang-format off + ASSIGNS(i, OBJECT_WHOLE(r)) + INVARIANT(i <= MLKEM_K) + // clang-format on { - for (int j = 0; j < MLKEM_N / 8; j++) // clang-format off - ASSIGNS(j, OBJECT_WHOLE(t), OBJECT_WHOLE(r)) - INVARIANT(j >= 0 && j <= MLKEM_N / 8) - { // clang-format on - for (int k = 0; k < 8; k++) // clang-format off - ASSIGNS(k, OBJECT_WHOLE(t), OBJECT_WHOLE(r)) - INVARIANT(k >= 0 && k <= 8) - INVARIANT(FORALL(int, r, 0, k - 1, t[r] < (1u << 11))) - { // clang-format on - t[k] = scalar_compress_d11(a->vec[i].coeffs[8 * j + k]); - } - - // REF-CHANGE: Use array indexing into - // r rather than pointer-arithmetic to simplify verification - // - // Make all implicit truncation explicit. No data is being - // truncated for the LHS's since each t[i] is 11-bit in size. - r[11 * (i * (MLKEM_N / 8) + j) + 0] = (t[0] >> 0) & 0xFF; - r[11 * (i * (MLKEM_N / 8) + j) + 1] = - (t[0] >> 8) | ((t[1] << 3) & 0xFF); - r[11 * (i * (MLKEM_N / 8) + j) + 2] = - (t[1] >> 5) | ((t[2] << 6) & 0xFF); - r[11 * (i * (MLKEM_N / 8) + j) + 3] = (t[2] >> 2) & 0xFF; - r[11 * (i * (MLKEM_N / 8) + j) + 4] = - (t[2] >> 10) | ((t[3] << 1) & 0xFF); - r[11 * (i * (MLKEM_N / 8) + j) + 5] = - (t[3] >> 7) | ((t[4] << 4) & 0xFF); - r[11 * (i * (MLKEM_N / 8) + j) + 6] = - (t[4] >> 4) | ((t[5] << 7) & 0xFF); - r[11 * (i * (MLKEM_N / 8) + j) + 7] = (t[5] >> 1) & 0xFF; - r[11 * (i * (MLKEM_N / 8) + j) + 8] = - (t[5] >> 9) | ((t[6] << 2) & 0xFF); - r[11 * (i * (MLKEM_N / 8) + j) + 9] = - (t[6] >> 6) | ((t[7] << 5) & 0xFF); - r[11 * (i * (MLKEM_N / 8) + j) + 10] = (t[7] >> 3); - } + poly_compress_du(r + i * MLKEM_POLYCOMPRESSEDBYTES_DU, &a->vec[i]); } -#elif (MLKEM_POLYVECCOMPRESSEDBYTES == (MLKEM_K * 320)) - uint16_t t[4]; - for (int i = 0; i < MLKEM_K; i++) // clang-format off - ASSIGNS(i, OBJECT_WHOLE(t), OBJECT_WHOLE(r)) - INVARIANT(i >= 0 && i <= MLKEM_K) - { // clang-format on - for (int j = 0; j < MLKEM_N / 4; j++) // clang-format off - ASSIGNS(j, OBJECT_WHOLE(t), OBJECT_WHOLE(r)) - INVARIANT(j >= 0 && j <= MLKEM_N / 4) - { // clang-format on - for (int k = 0; k < 4; k++) // clang-format off - ASSIGNS(k, OBJECT_WHOLE(t)) - INVARIANT(k >= 0 && k <= 4) - INVARIANT(FORALL(int, r, 0, k - 1, t[r] < (1u << 10))) - { // clang-format on - t[k] = scalar_compress_d10(a->vec[i].coeffs[4 * j + k]); - } - - // REF-CHANGE: Use array indexing into - // r rather than pointer-arithmetic to simplify verification - // - // Make all implicit truncation explicit. No data is being - // truncated for the LHS's since each t[i] is 10-bit in size. - r[5 * (i * (MLKEM_N / 4) + j) + 0] = (t[0] >> 0) & 0xFF; - r[5 * (i * (MLKEM_N / 4) + j) + 1] = - (t[0] >> 8) | ((t[1] << 2) & 0xFF); - r[5 * (i * (MLKEM_N / 4) + j) + 2] = - (t[1] >> 6) | ((t[2] << 4) & 0xFF); - r[5 * (i * (MLKEM_N / 4) + j) + 3] = - (t[2] >> 4) | ((t[3] << 6) & 0xFF); - r[5 * (i * (MLKEM_N / 4) + j) + 4] = (t[3] >> 2); - } - } -#else -#error "MLKEM_POLYVECCOMPRESSEDBYTES needs to be in {320*MLKEM_K, 352*MLKEM_K}" -#endif } -/************************************************* - * Name: polyvec_decompress - * - * Description: De-serialize and decompress vector of polynomials; - * approximate inverse of polyvec_compress - * - * Arguments: - polyvec *r: pointer to output vector of polynomials - * - const uint8_t *a: pointer to input byte array - * (of length MLKEM_POLYVECCOMPRESSEDBYTES) - **************************************************/ void polyvec_decompress(polyvec *r, const uint8_t a[MLKEM_POLYVECCOMPRESSEDBYTES]) { -#if (MLKEM_POLYVECCOMPRESSEDBYTES == (MLKEM_K * 352)) - for (int i = 0; i < MLKEM_K; i++) // clang-format off - ASSIGNS(i, OBJECT_WHOLE(r)) - INVARIANT(0 <= i && i <= MLKEM_K) - INVARIANT(FORALL(int, r0, 0, i - 1, - ARRAY_BOUND(r->vec[r0].coeffs,0, MLKEM_N - 1, 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_BOUND(r->vec[r0].coeffs, 0, MLKEM_N - 1, 0, (MLKEM_Q - 1)))) - INVARIANT(ARRAY_BOUND(r->vec[i].coeffs, 0, 8 * j - 1, 0, (MLKEM_Q - 1))) - { // clang-format on - uint16_t t[8]; - uint8_t const *base = &a[11 * (i * (MLKEM_N / 8) + j)]; - t[0] = 0x7FF & ((base[0] >> 0) | ((uint16_t)base[1] << 8)); - t[1] = 0x7FF & ((base[1] >> 3) | ((uint16_t)base[2] << 5)); - t[2] = 0x7FF & ((base[2] >> 6) | ((uint16_t)base[3] << 2) | - ((uint16_t)base[4] << 10)); - t[3] = 0x7FF & ((base[4] >> 1) | ((uint16_t)base[5] << 7)); - t[4] = 0x7FF & ((base[5] >> 4) | ((uint16_t)base[6] << 4)); - t[5] = 0x7FF & ((base[6] >> 7) | ((uint16_t)base[7] << 1) | - ((uint16_t)base[8] << 9)); - t[6] = 0x7FF & ((base[8] >> 2) | ((uint16_t)base[9] << 6)); - t[7] = 0x7FF & ((base[9] >> 5) | ((uint16_t)base[10] << 3)); - - for (int k = 0; k < 8; k++) // clang-format off - ASSIGNS(k, OBJECT_WHOLE(r)) - INVARIANT(0 <= k && k <= 8) - INVARIANT(FORALL(int, r0, 0, i - 1, - ARRAY_BOUND(r->vec[r0].coeffs, 0, MLKEM_N - 1, - 0, (MLKEM_Q - 1)))) - INVARIANT(ARRAY_BOUND(r->vec[i].coeffs, 0, 8 * j + k - 1, - 0, (MLKEM_Q - 1))) - { // clang-format on - r->vec[i].coeffs[8 * j + k] = scalar_decompress_d11(t[k]); - } - } - } -#elif (MLKEM_POLYVECCOMPRESSEDBYTES == (MLKEM_K * 320)) - for (int i = 0; i < MLKEM_K; i++) // clang-format off + unsigned int i; + for (i = 0; i < MLKEM_K; i++) // clang-format off ASSIGNS(i, OBJECT_WHOLE(r)) - INVARIANT(0 <= i && i <= MLKEM_K) - INVARIANT(FORALL(int, r0, 0, i - 1, - ARRAY_BOUND(r->vec[r0].coeffs, 0, MLKEM_N - 1, 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_BOUND(r->vec[r0].coeffs, 0, MLKEM_N - 1, 0, (MLKEM_Q - 1)))) - INVARIANT(ARRAY_BOUND(r->vec[i].coeffs, 0, 4 * j - 1, 0, (MLKEM_Q - 1))) - { // clang-format on - uint16_t t[4]; - uint8_t const *base = &a[5 * (i * (MLKEM_N / 4) + j)]; - - t[0] = 0x3FF & ((base[0] >> 0) | ((uint16_t)base[1] << 8)); - t[1] = 0x3FF & ((base[1] >> 2) | ((uint16_t)base[2] << 6)); - t[2] = 0x3FF & ((base[2] >> 4) | ((uint16_t)base[3] << 4)); - t[3] = 0x3FF & ((base[3] >> 6) | ((uint16_t)base[4] << 2)); - - for (int k = 0; k < 4; k++) // clang-format off - ASSIGNS(k, OBJECT_WHOLE(r)) - INVARIANT(0 <= k && k <= 4) - INVARIANT(FORALL(int, r0, 0, i - 1, - ARRAY_BOUND(r->vec[r0].coeffs, 0, MLKEM_N - 1, 0, (MLKEM_Q - 1)))) - INVARIANT(ARRAY_BOUND(r->vec[i].coeffs, 0, 4 * j + k - 1, 0, (MLKEM_Q - 1))) - { // clang-format on - r->vec[i].coeffs[4 * j + k] = scalar_decompress_d10(t[k]); - } - } + INVARIANT(i <= MLKEM_K) + // clang-format on + { + poly_decompress_du(&r->vec[i], a + i * MLKEM_POLYCOMPRESSEDBYTES_DU); } -#else -#error "MLKEM_POLYVECCOMPRESSEDBYTES needs to be in {320*MLKEM_K, 352*MLKEM_K}" -#endif POLYVEC_UBOUND(r, MLKEM_Q); } diff --git a/mlkem/polyvec.h b/mlkem/polyvec.h index 0a74e6f58..22e32c6be 100644 --- a/mlkem/polyvec.h +++ b/mlkem/polyvec.h @@ -37,6 +37,17 @@ REQUIRES(FORALL(int, k0, 0, MLKEM_K - 1, // clang-format on #define polyvec_decompress MLKEM_NAMESPACE(polyvec_decompress) +/************************************************* + * Name: polyvec_decompress + * + * Description: De-serialize and decompress vector of polynomials; + * approximate inverse of polyvec_compress + * + * Arguments: - polyvec *r: pointer to output vector of polynomials. + * Output will have coefficients normalized to [0,..,q-1]. + * - const uint8_t *a: pointer to input byte array + * (of length MLKEM_POLYVECCOMPRESSEDBYTES) + **************************************************/ void polyvec_decompress( polyvec *r, const uint8_t a[MLKEM_POLYVECCOMPRESSEDBYTES]) // clang-format off From 88534c5240f18ce0abb299f3b991e2a3f192b29a Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Wed, 20 Nov 2024 13:55:08 +0800 Subject: [PATCH 2/6] Rename poly_[de]compress to poly_[de]compress_dv Signed-off-by: Matthias J. Kannwischer --- cbmc/proofs/indcpa_dec/Makefile | 2 +- cbmc/proofs/indcpa_enc/Makefile | 2 +- .../Makefile | 8 ++--- .../cbmc-proof.txt | 0 .../poly_compress_dv_harness.c} | 6 ++-- .../Makefile | 8 ++--- .../cbmc-proof.txt | 0 .../poly_decompress_dv_harness.c} | 6 ++-- mlkem/indcpa.c | 4 +-- mlkem/params.h | 8 ++--- mlkem/poly.c | 17 +++++----- mlkem/poly.h | 33 ++++++++++--------- test/bench_components_mlkem.c | 9 ++--- 13 files changed, 53 insertions(+), 50 deletions(-) rename cbmc/proofs/{poly_compress => poly_compress_dv}/Makefile (91%) rename cbmc/proofs/{poly_compress => poly_compress_dv}/cbmc-proof.txt (100%) rename cbmc/proofs/{poly_compress/poly_compress_harness.c => poly_compress_dv/poly_compress_dv_harness.c} (76%) rename cbmc/proofs/{poly_decompress => poly_decompress_dv}/Makefile (91%) rename cbmc/proofs/{poly_decompress => poly_decompress_dv}/cbmc-proof.txt (100%) rename cbmc/proofs/{poly_decompress/poly_decompress_harness.c => poly_decompress_dv/poly_decompress_dv_harness.c} (76%) diff --git a/cbmc/proofs/indcpa_dec/Makefile b/cbmc/proofs/indcpa_dec/Makefile index 58372cd5e..51ee7ce87 100644 --- a/cbmc/proofs/indcpa_dec/Makefile +++ b/cbmc/proofs/indcpa_dec/Makefile @@ -27,7 +27,7 @@ USED_FUNCTIONS += poly_sub USED_FUNCTIONS += poly_reduce USED_FUNCTIONS += poly_tomsg USED_FUNCTIONS += polyvec_decompress -USED_FUNCTIONS += poly_decompress +USED_FUNCTIONS += poly_decompress_dv USED_FUNCTIONS += polyvec_frombytes USED_FUNCTIONS += polyvec_reduce USE_FUNCTION_CONTRACTS=$(addprefix $(MLKEM_NAMESPACE),$(USED_FUNCTIONS)) diff --git a/cbmc/proofs/indcpa_enc/Makefile b/cbmc/proofs/indcpa_enc/Makefile index 312853d61..c87024a61 100644 --- a/cbmc/proofs/indcpa_enc/Makefile +++ b/cbmc/proofs/indcpa_enc/Makefile @@ -42,7 +42,7 @@ USED_FUNCTIONS += poly_add USED_FUNCTIONS += polyvec_reduce USED_FUNCTIONS += poly_reduce USED_FUNCTIONS += polyvec_compress -USED_FUNCTIONS += poly_compress +USED_FUNCTIONS += poly_compress_dv USED_FUNCTIONS += polyvec_frombytes USE_FUNCTION_CONTRACTS=matvec_mul $(addprefix $(MLKEM_NAMESPACE),$(USED_FUNCTIONS)) diff --git a/cbmc/proofs/poly_compress/Makefile b/cbmc/proofs/poly_compress_dv/Makefile similarity index 91% rename from cbmc/proofs/poly_compress/Makefile rename to cbmc/proofs/poly_compress_dv/Makefile index f9f224f53..737e1e564 100644 --- a/cbmc/proofs/poly_compress/Makefile +++ b/cbmc/proofs/poly_compress_dv/Makefile @@ -3,11 +3,11 @@ include ../Makefile_params.common HARNESS_ENTRY = harness -HARNESS_FILE = poly_compress_harness +HARNESS_FILE = poly_compress_dv_harness # This should be a unique identifier for this proof, and will appear on the # Litani dashboard. It can be human-readable and contain spaces if you wish. -PROOF_UID = poly_compress +PROOF_UID = poly_compress_dv DEFINES += INCLUDES += @@ -19,7 +19,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c PROJECT_SOURCES += $(SRCDIR)/mlkem/verify.c -CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_compress +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_compress_dv USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = $(MLKEM_NAMESPACE)poly_compress +FUNCTION_NAME = $(MLKEM_NAMESPACE)poly_compress_dv # If this proof is found to consume huge amounts of RAM, you can set the # EXPENSIVE variable. With new enough versions of the proof tools, this will diff --git a/cbmc/proofs/poly_compress/cbmc-proof.txt b/cbmc/proofs/poly_compress_dv/cbmc-proof.txt similarity index 100% rename from cbmc/proofs/poly_compress/cbmc-proof.txt rename to cbmc/proofs/poly_compress_dv/cbmc-proof.txt diff --git a/cbmc/proofs/poly_compress/poly_compress_harness.c b/cbmc/proofs/poly_compress_dv/poly_compress_dv_harness.c similarity index 76% rename from cbmc/proofs/poly_compress/poly_compress_harness.c rename to cbmc/proofs/poly_compress_dv/poly_compress_dv_harness.c index dc4832972..bfd61dc14 100644 --- a/cbmc/proofs/poly_compress/poly_compress_harness.c +++ b/cbmc/proofs/poly_compress_dv/poly_compress_dv_harness.c @@ -6,8 +6,8 @@ */ /** - * @file poly_compress_harness.c - * @brief Implements the proof harness for poly_compress function. + * @file poly_compress_dv_harness.c + * @brief Implements the proof harness for poly_compress_dv function. */ #include "poly.h" @@ -25,5 +25,5 @@ void harness(void) { poly *r; uint8_t *a; - poly_compress(a, r); + poly_compress_dv(a, r); } diff --git a/cbmc/proofs/poly_decompress/Makefile b/cbmc/proofs/poly_decompress_dv/Makefile similarity index 91% rename from cbmc/proofs/poly_decompress/Makefile rename to cbmc/proofs/poly_decompress_dv/Makefile index a72676df2..45bbabe0c 100644 --- a/cbmc/proofs/poly_decompress/Makefile +++ b/cbmc/proofs/poly_decompress_dv/Makefile @@ -3,11 +3,11 @@ include ../Makefile_params.common HARNESS_ENTRY = harness -HARNESS_FILE = poly_decompress_harness +HARNESS_FILE = poly_decompress_dv_harness # This should be a unique identifier for this proof, and will appear on the # Litani dashboard. It can be human-readable and contain spaces if you wish. -PROOF_UID = poly_decompress +PROOF_UID = poly_decompress_dv DEFINES += INCLUDES += @@ -19,7 +19,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c PROJECT_SOURCES += $(SRCDIR)/mlkem/verify.c -CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_decompress +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_decompress_dv # For K = 2 or 3, the code calls scalar_decompress_d4, so ifeq ($(MLKEM_K),4) @@ -35,7 +35,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--bitwuzla -FUNCTION_NAME = $(MLKEM_NAMESPACE)poly_decompress +FUNCTION_NAME = $(MLKEM_NAMESPACE)poly_decompress_dv # If this proof is found to consume huge amounts of RAM, you can set the # EXPENSIVE variable. With new enough versions of the proof tools, this will diff --git a/cbmc/proofs/poly_decompress/cbmc-proof.txt b/cbmc/proofs/poly_decompress_dv/cbmc-proof.txt similarity index 100% rename from cbmc/proofs/poly_decompress/cbmc-proof.txt rename to cbmc/proofs/poly_decompress_dv/cbmc-proof.txt diff --git a/cbmc/proofs/poly_decompress/poly_decompress_harness.c b/cbmc/proofs/poly_decompress_dv/poly_decompress_dv_harness.c similarity index 76% rename from cbmc/proofs/poly_decompress/poly_decompress_harness.c rename to cbmc/proofs/poly_decompress_dv/poly_decompress_dv_harness.c index 516eeca0d..7b8e557a6 100644 --- a/cbmc/proofs/poly_decompress/poly_decompress_harness.c +++ b/cbmc/proofs/poly_decompress_dv/poly_decompress_dv_harness.c @@ -6,8 +6,8 @@ */ /** - * @file poly_decompress_harness.c - * @brief Implements the proof harness for poly_decompress function. + * @file poly_decompress_dv_harness.c + * @brief Implements the proof harness for poly_decompress_dv function. */ /* @@ -25,5 +25,5 @@ void harness(void) { poly *r; uint8_t *a; - poly_decompress(r, a); + poly_decompress_dv(r, a); } diff --git a/mlkem/indcpa.c b/mlkem/indcpa.c index 869ba1fdf..9afc543ad 100644 --- a/mlkem/indcpa.c +++ b/mlkem/indcpa.c @@ -105,7 +105,7 @@ static void unpack_sk(polyvec *sk, static void pack_ciphertext(uint8_t r[MLKEM_INDCPA_BYTES], polyvec *b, poly *v) { polyvec_compress(r, b); - poly_compress(r + MLKEM_POLYVECCOMPRESSEDBYTES, v); + poly_compress_dv(r + MLKEM_POLYVECCOMPRESSEDBYTES, v); } /************************************************* @@ -121,7 +121,7 @@ static void pack_ciphertext(uint8_t r[MLKEM_INDCPA_BYTES], polyvec *b, static void unpack_ciphertext(polyvec *b, poly *v, const uint8_t c[MLKEM_INDCPA_BYTES]) { polyvec_decompress(b, c); - poly_decompress(v, c + MLKEM_POLYVECCOMPRESSEDBYTES); + poly_decompress_dv(v, c + MLKEM_POLYVECCOMPRESSEDBYTES); } #ifndef MLKEM_GEN_MATRIX_NBLOCKS diff --git a/mlkem/params.h b/mlkem/params.h index addbdf067..c94aa461f 100644 --- a/mlkem/params.h +++ b/mlkem/params.h @@ -34,17 +34,17 @@ #if MLKEM_K == 2 #define MLKEM_ETA1 3 -#define MLKEM_POLYCOMPRESSEDBYTES 128 +#define MLKEM_POLYCOMPRESSEDBYTES_DV 128 #define MLKEM_POLYCOMPRESSEDBYTES_DU 320 #define MLKEM_POLYVECCOMPRESSEDBYTES (MLKEM_K * MLKEM_POLYCOMPRESSEDBYTES_DU) #elif MLKEM_K == 3 #define MLKEM_ETA1 2 -#define MLKEM_POLYCOMPRESSEDBYTES 128 +#define MLKEM_POLYCOMPRESSEDBYTES_DV 128 #define MLKEM_POLYCOMPRESSEDBYTES_DU 320 #define MLKEM_POLYVECCOMPRESSEDBYTES (MLKEM_K * MLKEM_POLYCOMPRESSEDBYTES_DU) #elif MLKEM_K == 4 #define MLKEM_ETA1 2 -#define MLKEM_POLYCOMPRESSEDBYTES 160 +#define MLKEM_POLYCOMPRESSEDBYTES_DV 160 #define MLKEM_POLYCOMPRESSEDBYTES_DU 352 #define MLKEM_POLYVECCOMPRESSEDBYTES (MLKEM_K * MLKEM_POLYCOMPRESSEDBYTES_DU) #endif @@ -55,7 +55,7 @@ #define MLKEM_INDCPA_PUBLICKEYBYTES (MLKEM_POLYVECBYTES + MLKEM_SYMBYTES) #define MLKEM_INDCPA_SECRETKEYBYTES (MLKEM_POLYVECBYTES) #define MLKEM_INDCPA_BYTES \ - (MLKEM_POLYVECCOMPRESSEDBYTES + MLKEM_POLYCOMPRESSEDBYTES) + (MLKEM_POLYVECCOMPRESSEDBYTES + MLKEM_POLYCOMPRESSEDBYTES_DV) #define MLKEM_PUBLICKEYBYTES (MLKEM_INDCPA_PUBLICKEYBYTES) /* 32 bytes of additional space to save H(pk) */ diff --git a/mlkem/poly.c b/mlkem/poly.c index 1b4347d97..4a8a97b95 100644 --- a/mlkem/poly.c +++ b/mlkem/poly.c @@ -134,11 +134,11 @@ void poly_decompress_du(poly *r, #endif } -void poly_compress(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES], const poly *a) { +void poly_compress_dv(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_DV], const poly *a) { POLY_UBOUND(a, MLKEM_Q); uint8_t t[8] = {0}; -#if (MLKEM_POLYCOMPRESSEDBYTES == 128) +#if (MLKEM_POLYCOMPRESSEDBYTES_DV == 128) for (int i = 0; i < MLKEM_N / 8; i++) // clang-format off ASSIGNS(i, OBJECT_WHOLE(t), OBJECT_WHOLE(r)) INVARIANT(i >= 0 && i <= MLKEM_N / 8) // clang-format on @@ -159,7 +159,7 @@ void poly_compress(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES], const poly *a) { r[i * 4 + 2] = t[4] | (t[5] << 4); r[i * 4 + 3] = t[6] | (t[7] << 4); } -#elif (MLKEM_POLYCOMPRESSEDBYTES == 160) +#elif (MLKEM_POLYCOMPRESSEDBYTES_DV == 160) for (int i = 0; i < MLKEM_N / 8; i++) // clang-format off ASSIGNS(i, OBJECT_WHOLE(t), OBJECT_WHOLE(r)) INVARIANT(i >= 0 && i <= MLKEM_N / 8) // clang-format on @@ -183,12 +183,13 @@ void poly_compress(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES], const poly *a) { r[i * 5 + 4] = 0xFF & ((t[6] >> 2) | (t[7] << 3)); } #else -#error "MLKEM_POLYCOMPRESSEDBYTES needs to be in {128, 160}" +#error "MLKEM_POLYCOMPRESSEDBYTES_DV needs to be in {128, 160}" #endif } -void poly_decompress(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES]) { -#if (MLKEM_POLYCOMPRESSEDBYTES == 128) +void poly_decompress_dv(poly *r, + const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_DV]) { +#if (MLKEM_POLYCOMPRESSEDBYTES_DV == 128) for (int i = 0; i < MLKEM_N / 2; i++) // clang-format off ASSIGNS(i, OBJECT_WHOLE(r)) INVARIANT(i >= 0 && i <= MLKEM_N / 2) @@ -198,7 +199,7 @@ void poly_decompress(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES]) { r->coeffs[2 * i + 0] = scalar_decompress_d4((a[i] >> 0) & 0xF); r->coeffs[2 * i + 1] = scalar_decompress_d4((a[i] >> 4) & 0xF); } -#elif (MLKEM_POLYCOMPRESSEDBYTES == 160) +#elif (MLKEM_POLYCOMPRESSEDBYTES_DV == 160) for (int i = 0; i < MLKEM_N / 8; i++) // clang-format off ASSIGNS(i, OBJECT_WHOLE(r)) INVARIANT(i >= 0 && i <= MLKEM_N / 8) @@ -232,7 +233,7 @@ void poly_decompress(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES]) { } } #else -#error "MLKEM_POLYCOMPRESSEDBYTES needs to be in {128, 160}" +#error "MLKEM_POLYCOMPRESSEDBYTES_DV needs to be in {128, 160}" #endif POLY_UBOUND(r, MLKEM_Q); diff --git a/mlkem/poly.h b/mlkem/poly.h index 87576ada8..533582e28 100644 --- a/mlkem/poly.h +++ b/mlkem/poly.h @@ -350,45 +350,46 @@ ASSIGNS(OBJECT_UPTO(r, sizeof(poly))) ENSURES(ARRAY_BOUND(r->coeffs, 0, (MLKEM_N - 1), 0, (MLKEM_Q - 1))); // clang-format on - -#define poly_compress MLKEM_NAMESPACE(poly_compress) +#define poly_compress_dv MLKEM_NAMESPACE(poly_compress_dv) /************************************************* - * Name: poly_compress + * Name: poly_compress_dv * - * Description: Compression and subsequent serialization of a polynomial + * Description: Compression (dv bits) and subsequent serialization of a + *polynomial * * Arguments: - uint8_t *r: pointer to output byte array - * (of length MLKEM_POLYCOMPRESSEDBYTES) + * (of length MLKEM_POLYCOMPRESSEDBYTES_DV) * - const poly *a: pointer to input polynomial * Coefficients must be unsigned canonical, * i.e. in [0,1,..,MLKEM_Q-1]. **************************************************/ -void poly_compress(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES], - const poly *a) // clang-format off -REQUIRES(IS_FRESH(r, MLKEM_POLYCOMPRESSEDBYTES)) +void poly_compress_dv(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_DV], + const poly *a) // clang-format off +REQUIRES(IS_FRESH(r, MLKEM_POLYCOMPRESSEDBYTES_DV)) REQUIRES(IS_FRESH(a, sizeof(poly))) REQUIRES(ARRAY_BOUND(a->coeffs, 0, (MLKEM_N - 1), 0, (MLKEM_Q - 1))) ASSIGNS(OBJECT_WHOLE(r)); // clang-format on -#define poly_decompress MLKEM_NAMESPACE(poly_decompress) +#define poly_decompress_dv MLKEM_NAMESPACE(poly_decompress_dv) /************************************************* - * Name: poly_decompress + * Name: poly_decompress_dv * - * Description: De-serialization and subsequent decompression of a polynomial; - * approximate inverse of poly_compress + * Description: De-serialization and subsequent decompression (dv bits) of a + *polynomial; approximate inverse of poly_compress * * Arguments: - poly *r: pointer to output polynomial * - const uint8_t *a: pointer to input byte array - * (of length MLKEM_POLYCOMPRESSEDBYTES bytes) + * (of length MLKEM_POLYCOMPRESSEDBYTES_DV + *bytes) * * Upon return, the coefficients of the output polynomial are unsigned-canonical * (non-negative and smaller than MLKEM_Q). * **************************************************/ -void poly_decompress( - poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES]) // clang-format off -REQUIRES(IS_FRESH(a, MLKEM_POLYCOMPRESSEDBYTES)) +void poly_decompress_dv( + poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_DV]) // clang-format off +REQUIRES(IS_FRESH(a, MLKEM_POLYCOMPRESSEDBYTES_DV)) REQUIRES(IS_FRESH(r, sizeof(poly))) ASSIGNS(OBJECT_WHOLE(r)) ENSURES(ARRAY_BOUND(r->coeffs, 0, (MLKEM_N - 1), 0, (MLKEM_Q - 1))); diff --git a/test/bench_components_mlkem.c b/test/bench_components_mlkem.c index e3a10f6c2..c2596cb2a 100644 --- a/test/bench_components_mlkem.c +++ b/test/bench_components_mlkem.c @@ -67,11 +67,12 @@ static int bench(void) { 1 * SHAKE128_RATE)) /* poly */ - // poly_compress - BENCH("poly_compress", poly_compress((uint8_t *)data0, (poly *)data1)) + // poly_compress_dv + BENCH("poly_compress_dv", poly_compress_dv((uint8_t *)data0, (poly *)data1)) - // poly_decompress - BENCH("poly_decompress", poly_decompress((poly *)data0, (uint8_t *)data1)) + // poly_decompress_dv + BENCH("poly_decompress_dv", + poly_decompress_dv((poly *)data0, (uint8_t *)data1)) // poly_tobytes BENCH("poly_tobytes", poly_tobytes((uint8_t *)data0, (poly *)data1)) From 551f53b2532bdc64ac7291ec7d56e8d237bf70d0 Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Wed, 20 Nov 2024 14:48:17 +0800 Subject: [PATCH 3/6] rename polyvec_{,de}compress to polyvec_{,de}compress_du Signed-off-by: Matthias J. Kannwischer --- cbmc/proofs/indcpa_dec/Makefile | 2 +- cbmc/proofs/indcpa_enc/Makefile | 2 +- .../Makefile | 8 +++--- .../cbmc-proof.txt | 0 .../polyvec_compress_du_harness.c} | 6 ++--- .../Makefile | 10 +++---- .../cbmc-proof.txt | 0 .../polyvec_decompress_du_harness.c} | 6 ++--- mlkem/indcpa.c | 8 +++--- mlkem/params.h | 8 +++--- mlkem/polyvec.c | 8 +++--- mlkem/polyvec.h | 26 +++++++++---------- test/bench_components_mlkem.c | 12 ++++----- 13 files changed, 48 insertions(+), 48 deletions(-) rename cbmc/proofs/{polyvec_compress => polyvec_compress_du}/Makefile (90%) rename cbmc/proofs/{polyvec_compress => polyvec_compress_du}/cbmc-proof.txt (100%) rename cbmc/proofs/{polyvec_compress/polyvec_compress_harness.c => polyvec_compress_du/polyvec_compress_du_harness.c} (76%) rename cbmc/proofs/{polyvec_decompress => polyvec_decompress_du}/Makefile (86%) rename cbmc/proofs/{polyvec_decompress => polyvec_decompress_du}/cbmc-proof.txt (100%) rename cbmc/proofs/{polyvec_decompress/polyvec_decompress_harness.c => polyvec_decompress_du/polyvec_decompress_du_harness.c} (78%) diff --git a/cbmc/proofs/indcpa_dec/Makefile b/cbmc/proofs/indcpa_dec/Makefile index 51ee7ce87..8a9f961b8 100644 --- a/cbmc/proofs/indcpa_dec/Makefile +++ b/cbmc/proofs/indcpa_dec/Makefile @@ -26,7 +26,7 @@ USED_FUNCTIONS += poly_invntt_tomont USED_FUNCTIONS += poly_sub USED_FUNCTIONS += poly_reduce USED_FUNCTIONS += poly_tomsg -USED_FUNCTIONS += polyvec_decompress +USED_FUNCTIONS += polyvec_decompress_du USED_FUNCTIONS += poly_decompress_dv USED_FUNCTIONS += polyvec_frombytes USED_FUNCTIONS += polyvec_reduce diff --git a/cbmc/proofs/indcpa_enc/Makefile b/cbmc/proofs/indcpa_enc/Makefile index c87024a61..b3ee761e9 100644 --- a/cbmc/proofs/indcpa_enc/Makefile +++ b/cbmc/proofs/indcpa_enc/Makefile @@ -41,7 +41,7 @@ USED_FUNCTIONS += polyvec_add USED_FUNCTIONS += poly_add USED_FUNCTIONS += polyvec_reduce USED_FUNCTIONS += poly_reduce -USED_FUNCTIONS += polyvec_compress +USED_FUNCTIONS += polyvec_compress_du USED_FUNCTIONS += poly_compress_dv USED_FUNCTIONS += polyvec_frombytes diff --git a/cbmc/proofs/polyvec_compress/Makefile b/cbmc/proofs/polyvec_compress_du/Makefile similarity index 90% rename from cbmc/proofs/polyvec_compress/Makefile rename to cbmc/proofs/polyvec_compress_du/Makefile index 942ffa318..42e520302 100644 --- a/cbmc/proofs/polyvec_compress/Makefile +++ b/cbmc/proofs/polyvec_compress_du/Makefile @@ -3,11 +3,11 @@ include ../Makefile_params.common HARNESS_ENTRY = harness -HARNESS_FILE = polyvec_compress_harness +HARNESS_FILE = polyvec_compress_du_harness # This should be a unique identifier for this proof, and will appear on the # Litani dashboard. It can be human-readable and contain spaces if you wish. -PROOF_UID = polyvec_compress +PROOF_UID = polyvec_compress_du DEFINES += INCLUDES += @@ -18,7 +18,7 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_compress +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_compress_du USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_compress_du APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = $(MLKEM_NAMESPACE)polyvec_compress +FUNCTION_NAME = $(MLKEM_NAMESPACE)polyvec_compress_du # If this proof is found to consume huge amounts of RAM, you can set the # EXPENSIVE variable. With new enough versions of the proof tools, this will diff --git a/cbmc/proofs/polyvec_compress/cbmc-proof.txt b/cbmc/proofs/polyvec_compress_du/cbmc-proof.txt similarity index 100% rename from cbmc/proofs/polyvec_compress/cbmc-proof.txt rename to cbmc/proofs/polyvec_compress_du/cbmc-proof.txt diff --git a/cbmc/proofs/polyvec_compress/polyvec_compress_harness.c b/cbmc/proofs/polyvec_compress_du/polyvec_compress_du_harness.c similarity index 76% rename from cbmc/proofs/polyvec_compress/polyvec_compress_harness.c rename to cbmc/proofs/polyvec_compress_du/polyvec_compress_du_harness.c index c5347604a..053d12a24 100644 --- a/cbmc/proofs/polyvec_compress/polyvec_compress_harness.c +++ b/cbmc/proofs/polyvec_compress_du/polyvec_compress_du_harness.c @@ -6,8 +6,8 @@ */ /** - * @file polyvec_compress_harness.c - * @brief Implements the proof harness for polyvec_compress function. + * @file polyvec_compress_du_harness.c + * @brief Implements the proof harness for polyvec_compress_du function. */ #include "poly.h" #include "polyvec.h" @@ -26,5 +26,5 @@ void harness(void) { polyvec *r; uint8_t *a; - polyvec_compress(a, r); + polyvec_compress_du(a, r); } diff --git a/cbmc/proofs/polyvec_decompress/Makefile b/cbmc/proofs/polyvec_decompress_du/Makefile similarity index 86% rename from cbmc/proofs/polyvec_decompress/Makefile rename to cbmc/proofs/polyvec_decompress_du/Makefile index 5cca56a17..2ad128295 100644 --- a/cbmc/proofs/polyvec_decompress/Makefile +++ b/cbmc/proofs/polyvec_decompress_du/Makefile @@ -3,22 +3,22 @@ include ../Makefile_params.common HARNESS_ENTRY = harness -HARNESS_FILE = polyvec_decompress_harness +HARNESS_FILE = polyvec_decompress_du_harness # This should be a unique identifier for this proof, and will appear on the # Litani dashboard. It can be human-readable and contain spaces if you wish. -PROOF_UID = polyvec_decompress +PROOF_UID = polyvec_decompress_du DEFINES += INCLUDES += REMOVE_FUNCTION_BODY += -UNWINDSET += $(MLKEM_NAMESPACE)polyvec_decompress.0:4 # Largest value of MLKEM_K +UNWINDSET += $(MLKEM_NAMESPACE)polyvec_decompress_du.0:4 # Largest value of MLKEM_K PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/polyvec.c -CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_decompress +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_decompress_du USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_decompress_du APPLY_LOOP_CONTRACTS=on @@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = $(MLKEM_NAMESPACE)polyvec_decompress +FUNCTION_NAME = $(MLKEM_NAMESPACE)polyvec_decompress_du # If this proof is found to consume huge amounts of RAM, you can set the # EXPENSIVE variable. With new enough versions of the proof tools, this will diff --git a/cbmc/proofs/polyvec_decompress/cbmc-proof.txt b/cbmc/proofs/polyvec_decompress_du/cbmc-proof.txt similarity index 100% rename from cbmc/proofs/polyvec_decompress/cbmc-proof.txt rename to cbmc/proofs/polyvec_decompress_du/cbmc-proof.txt diff --git a/cbmc/proofs/polyvec_decompress/polyvec_decompress_harness.c b/cbmc/proofs/polyvec_decompress_du/polyvec_decompress_du_harness.c similarity index 78% rename from cbmc/proofs/polyvec_decompress/polyvec_decompress_harness.c rename to cbmc/proofs/polyvec_decompress_du/polyvec_decompress_du_harness.c index 6a6e1ae02..36c4c50db 100644 --- a/cbmc/proofs/polyvec_decompress/polyvec_decompress_harness.c +++ b/cbmc/proofs/polyvec_decompress_du/polyvec_decompress_du_harness.c @@ -6,8 +6,8 @@ */ /** - * @file polyvec_decompress_harness.c - * @brief Implements the proof harness for polyvec_decompress function. + * @file polyvec_decompress_du_harness.c + * @brief Implements the proof harness for polyvec_decompress_du function. */ #include "poly.h" #include "polyvec.h" @@ -29,5 +29,5 @@ void harness(void) { // TODO: remove cbmc-viewer.json // TODO: remove the README for all proofs - polyvec_decompress(a, r); + polyvec_decompress_du(a, r); } diff --git a/mlkem/indcpa.c b/mlkem/indcpa.c index 9afc543ad..a37559c88 100644 --- a/mlkem/indcpa.c +++ b/mlkem/indcpa.c @@ -104,8 +104,8 @@ static void unpack_sk(polyvec *sk, **************************************************/ static void pack_ciphertext(uint8_t r[MLKEM_INDCPA_BYTES], polyvec *b, poly *v) { - polyvec_compress(r, b); - poly_compress_dv(r + MLKEM_POLYVECCOMPRESSEDBYTES, v); + polyvec_compress_du(r, b); + poly_compress_dv(r + MLKEM_POLYVECCOMPRESSEDBYTES_DU, v); } /************************************************* @@ -120,8 +120,8 @@ static void pack_ciphertext(uint8_t r[MLKEM_INDCPA_BYTES], polyvec *b, **************************************************/ static void unpack_ciphertext(polyvec *b, poly *v, const uint8_t c[MLKEM_INDCPA_BYTES]) { - polyvec_decompress(b, c); - poly_decompress_dv(v, c + MLKEM_POLYVECCOMPRESSEDBYTES); + polyvec_decompress_du(b, c); + poly_decompress_dv(v, c + MLKEM_POLYVECCOMPRESSEDBYTES_DU); } #ifndef MLKEM_GEN_MATRIX_NBLOCKS diff --git a/mlkem/params.h b/mlkem/params.h index c94aa461f..440235e06 100644 --- a/mlkem/params.h +++ b/mlkem/params.h @@ -36,17 +36,17 @@ #define MLKEM_ETA1 3 #define MLKEM_POLYCOMPRESSEDBYTES_DV 128 #define MLKEM_POLYCOMPRESSEDBYTES_DU 320 -#define MLKEM_POLYVECCOMPRESSEDBYTES (MLKEM_K * MLKEM_POLYCOMPRESSEDBYTES_DU) +#define MLKEM_POLYVECCOMPRESSEDBYTES_DU (MLKEM_K * MLKEM_POLYCOMPRESSEDBYTES_DU) #elif MLKEM_K == 3 #define MLKEM_ETA1 2 #define MLKEM_POLYCOMPRESSEDBYTES_DV 128 #define MLKEM_POLYCOMPRESSEDBYTES_DU 320 -#define MLKEM_POLYVECCOMPRESSEDBYTES (MLKEM_K * MLKEM_POLYCOMPRESSEDBYTES_DU) +#define MLKEM_POLYVECCOMPRESSEDBYTES_DU (MLKEM_K * MLKEM_POLYCOMPRESSEDBYTES_DU) #elif MLKEM_K == 4 #define MLKEM_ETA1 2 #define MLKEM_POLYCOMPRESSEDBYTES_DV 160 #define MLKEM_POLYCOMPRESSEDBYTES_DU 352 -#define MLKEM_POLYVECCOMPRESSEDBYTES (MLKEM_K * MLKEM_POLYCOMPRESSEDBYTES_DU) +#define MLKEM_POLYVECCOMPRESSEDBYTES_DU (MLKEM_K * MLKEM_POLYCOMPRESSEDBYTES_DU) #endif #define MLKEM_ETA2 2 @@ -55,7 +55,7 @@ #define MLKEM_INDCPA_PUBLICKEYBYTES (MLKEM_POLYVECBYTES + MLKEM_SYMBYTES) #define MLKEM_INDCPA_SECRETKEYBYTES (MLKEM_POLYVECBYTES) #define MLKEM_INDCPA_BYTES \ - (MLKEM_POLYVECCOMPRESSEDBYTES + MLKEM_POLYCOMPRESSEDBYTES_DV) + (MLKEM_POLYVECCOMPRESSEDBYTES_DU + MLKEM_POLYCOMPRESSEDBYTES_DV) #define MLKEM_PUBLICKEYBYTES (MLKEM_INDCPA_PUBLICKEYBYTES) /* 32 bytes of additional space to save H(pk) */ diff --git a/mlkem/polyvec.c b/mlkem/polyvec.c index ef569ac66..22c036741 100644 --- a/mlkem/polyvec.c +++ b/mlkem/polyvec.c @@ -8,8 +8,8 @@ #include "poly.h" #include "debug/debug.h" -void polyvec_compress(uint8_t r[MLKEM_POLYVECCOMPRESSEDBYTES], - const polyvec *a) { +void polyvec_compress_du(uint8_t r[MLKEM_POLYVECCOMPRESSEDBYTES_DU], + const polyvec *a) { unsigned int i; POLYVEC_UBOUND(a, MLKEM_Q); @@ -22,8 +22,8 @@ void polyvec_compress(uint8_t r[MLKEM_POLYVECCOMPRESSEDBYTES], } } -void polyvec_decompress(polyvec *r, - const uint8_t a[MLKEM_POLYVECCOMPRESSEDBYTES]) { +void polyvec_decompress_du(polyvec *r, + const uint8_t a[MLKEM_POLYVECCOMPRESSEDBYTES_DU]) { unsigned int i; for (i = 0; i < MLKEM_K; i++) // clang-format off ASSIGNS(i, OBJECT_WHOLE(r)) diff --git a/mlkem/polyvec.h b/mlkem/polyvec.h index 22e32c6be..d85cc285d 100644 --- a/mlkem/polyvec.h +++ b/mlkem/polyvec.h @@ -15,43 +15,43 @@ typedef struct { poly_mulcache vec[MLKEM_K]; } polyvec_mulcache; -#define polyvec_compress MLKEM_NAMESPACE(polyvec_compress) +#define polyvec_compress_du MLKEM_NAMESPACE(polyvec_compress_du) /************************************************* - * Name: polyvec_compress + * Name: polyvec_compress_du * * Description: Compress and serialize vector of polynomials * * Arguments: - uint8_t *r: pointer to output byte array - * (needs space for MLKEM_POLYVECCOMPRESSEDBYTES) + * (needs space for MLKEM_POLYVECCOMPRESSEDBYTES_DU) * - const polyvec *a: pointer to input vector of polynomials. * Coefficients must be unsigned canonical, * i.e. in [0,1,..,MLKEM_Q-1]. **************************************************/ -void polyvec_compress(uint8_t r[MLKEM_POLYVECCOMPRESSEDBYTES], - const polyvec *a) // clang-format off -REQUIRES(IS_FRESH(r, MLKEM_POLYVECCOMPRESSEDBYTES)) +void polyvec_compress_du(uint8_t r[MLKEM_POLYVECCOMPRESSEDBYTES_DU], + const polyvec *a) // clang-format off +REQUIRES(IS_FRESH(r, MLKEM_POLYVECCOMPRESSEDBYTES_DU)) REQUIRES(IS_FRESH(a, sizeof(polyvec))) ASSIGNS(OBJECT_WHOLE(r)) REQUIRES(FORALL(int, k0, 0, MLKEM_K - 1, ARRAY_BOUND(a->vec[k0].coeffs, 0, (MLKEM_N - 1), 0, (MLKEM_Q - 1)))); // clang-format on -#define polyvec_decompress MLKEM_NAMESPACE(polyvec_decompress) +#define polyvec_decompress_du MLKEM_NAMESPACE(polyvec_decompress_du) /************************************************* - * Name: polyvec_decompress + * Name: polyvec_decompress_du * * Description: De-serialize and decompress vector of polynomials; - * approximate inverse of polyvec_compress + * approximate inverse of polyvec_compress_du * * Arguments: - polyvec *r: pointer to output vector of polynomials. * Output will have coefficients normalized to [0,..,q-1]. * - const uint8_t *a: pointer to input byte array - * (of length MLKEM_POLYVECCOMPRESSEDBYTES) + * (of length MLKEM_POLYVECCOMPRESSEDBYTES_DU) **************************************************/ -void polyvec_decompress( +void polyvec_decompress_du( polyvec *r, - const uint8_t a[MLKEM_POLYVECCOMPRESSEDBYTES]) // clang-format off -REQUIRES(IS_FRESH(a, MLKEM_POLYVECCOMPRESSEDBYTES)) + const uint8_t a[MLKEM_POLYVECCOMPRESSEDBYTES_DU]) // clang-format off +REQUIRES(IS_FRESH(a, MLKEM_POLYVECCOMPRESSEDBYTES_DU)) REQUIRES(IS_FRESH(r, sizeof(polyvec))) ASSIGNS(OBJECT_WHOLE(r)) ENSURES(FORALL(int, k0, 0, MLKEM_K - 1, diff --git a/test/bench_components_mlkem.c b/test/bench_components_mlkem.c index c2596cb2a..53b6f3da3 100644 --- a/test/bench_components_mlkem.c +++ b/test/bench_components_mlkem.c @@ -124,13 +124,13 @@ static int bench(void) { BENCH("poly_sub", poly_sub((poly *)data0, (poly *)data1)) /* polyvec */ - // polyvec_compress - BENCH("polyvec_compress", - polyvec_compress((uint8_t *)data0, (polyvec *)data1)) + // polyvec_compress_du + BENCH("polyvec_compress_du", + polyvec_compress_du((uint8_t *)data0, (polyvec *)data1)) - // polyvec_decompress - BENCH("polyvec_decompress", - polyvec_decompress((polyvec *)data0, (uint8_t *)data1)) + // polyvec_decompress_du + BENCH("polyvec_decompress_du", + polyvec_decompress_du((polyvec *)data0, (uint8_t *)data1)) // polyvec_tobytes BENCH("polyvec_tobytes", polyvec_tobytes((uint8_t *)data0, (polyvec *)data1)) From 9f06fd80276cc0b66eaa4917dd242cfb646c1c13 Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Wed, 20 Nov 2024 15:30:59 +0800 Subject: [PATCH 4/6] CBMC: Proof poly_compress_du poly_decompress_du Signed-off-by: Matthias J. Kannwischer --- cbmc/proofs/poly_compress_du/Makefile | 61 ++++++++++++++++++ cbmc/proofs/poly_compress_du/cbmc-proof.txt | 3 + .../poly_compress_du_harness.c | 29 +++++++++ cbmc/proofs/poly_decompress_du/Makefile | 62 +++++++++++++++++++ cbmc/proofs/poly_decompress_du/cbmc-proof.txt | 3 + .../poly_decompress_du_harness.c | 29 +++++++++ .../polyvec_decompress_du_harness.c | 3 - 7 files changed, 187 insertions(+), 3 deletions(-) create mode 100644 cbmc/proofs/poly_compress_du/Makefile create mode 100644 cbmc/proofs/poly_compress_du/cbmc-proof.txt create mode 100644 cbmc/proofs/poly_compress_du/poly_compress_du_harness.c create mode 100644 cbmc/proofs/poly_decompress_du/Makefile create mode 100644 cbmc/proofs/poly_decompress_du/cbmc-proof.txt create mode 100644 cbmc/proofs/poly_decompress_du/poly_decompress_du_harness.c diff --git a/cbmc/proofs/poly_compress_du/Makefile b/cbmc/proofs/poly_compress_du/Makefile new file mode 100644 index 000000000..ff7ecef3c --- /dev/null +++ b/cbmc/proofs/poly_compress_du/Makefile @@ -0,0 +1,61 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = poly_compress_du_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = poly_compress_du + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/verify.c + +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_compress_du +# For K = 2 or 3, the code calls scalar_compress_d10, so +ifeq ($(MLKEM_K),4) +USE_FUNCTION_CONTRACTS = $(MLKEM_NAMESPACE)scalar_compress_d11 +else +USE_FUNCTION_CONTRACTS = $(MLKEM_NAMESPACE)scalar_compress_d10 +endif + +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = $(MLKEM_NAMESPACE)poly_compress_du + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 10 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mlkem/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/cbmc/proofs/poly_compress_du/cbmc-proof.txt b/cbmc/proofs/poly_compress_du/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/cbmc/proofs/poly_compress_du/cbmc-proof.txt @@ -0,0 +1,3 @@ +# SPDX-License-Identifier: Apache-2.0 + +# This file marks this directory as containing a CBMC proof. diff --git a/cbmc/proofs/poly_compress_du/poly_compress_du_harness.c b/cbmc/proofs/poly_compress_du/poly_compress_du_harness.c new file mode 100644 index 000000000..3779e8433 --- /dev/null +++ b/cbmc/proofs/poly_compress_du/poly_compress_du_harness.c @@ -0,0 +1,29 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 AND Apache-2.0 + +/* + * Insert copyright notice + */ + +/** + * @file poly_compress_du_harness.c + * @brief Implements the proof harness for poly_compress_du function. + */ +#include "poly.h" + +/* + * Insert project header files that + * - include the declaration of the function + * - include the types needed to declare function arguments + */ + +/** + * @brief Starting point for formal analysis + * + */ +void harness(void) { + poly *r; + uint8_t *a; + + poly_compress_du(a, r); +} diff --git a/cbmc/proofs/poly_decompress_du/Makefile b/cbmc/proofs/poly_decompress_du/Makefile new file mode 100644 index 000000000..625a2f88a --- /dev/null +++ b/cbmc/proofs/poly_decompress_du/Makefile @@ -0,0 +1,62 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = poly_decompress_du_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = poly_decompress_du + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/verify.c + +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_decompress_du + +# For K = 2 or 3, the code calls scalar_decompress_d10, so +ifeq ($(MLKEM_K),4) +USE_FUNCTION_CONTRACTS = $(MLKEM_NAMESPACE)scalar_decompress_d11 +else +USE_FUNCTION_CONTRACTS = $(MLKEM_NAMESPACE)scalar_decompress_d10 +endif + +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = $(MLKEM_NAMESPACE)poly_decompress_du + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 12 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mlkem/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/cbmc/proofs/poly_decompress_du/cbmc-proof.txt b/cbmc/proofs/poly_decompress_du/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/cbmc/proofs/poly_decompress_du/cbmc-proof.txt @@ -0,0 +1,3 @@ +# SPDX-License-Identifier: Apache-2.0 + +# This file marks this directory as containing a CBMC proof. diff --git a/cbmc/proofs/poly_decompress_du/poly_decompress_du_harness.c b/cbmc/proofs/poly_decompress_du/poly_decompress_du_harness.c new file mode 100644 index 000000000..b8401b71e --- /dev/null +++ b/cbmc/proofs/poly_decompress_du/poly_decompress_du_harness.c @@ -0,0 +1,29 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 AND Apache-2.0 + +/* + * Insert copyright notice + */ + +/** + * @file poly_decompress_du_harness.c + * @brief Implements the proof harness for poly_decompress_du function. + */ + +/* + * Insert project header files that + * - include the declaration of the function + * - include the types needed to declare function arguments + */ +#include "poly.h" + +/** + * @brief Starting point for formal analysis + * + */ +void harness(void) { + poly *r; + uint8_t *a; + + poly_decompress_du(r, a); +} diff --git a/cbmc/proofs/polyvec_decompress_du/polyvec_decompress_du_harness.c b/cbmc/proofs/polyvec_decompress_du/polyvec_decompress_du_harness.c index 36c4c50db..927470af4 100644 --- a/cbmc/proofs/polyvec_decompress_du/polyvec_decompress_du_harness.c +++ b/cbmc/proofs/polyvec_decompress_du/polyvec_decompress_du_harness.c @@ -26,8 +26,5 @@ void harness(void) { polyvec *a; uint8_t *r; - // TODO: remove cbmc-viewer.json - // TODO: remove the README for all proofs - polyvec_decompress_du(a, r); } From 1b3c6316d3a574335d0a48d9879f94a26271a7fa Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Wed, 20 Nov 2024 15:34:20 +0800 Subject: [PATCH 5/6] CBMC: poly_getnoise_eta1122_4x - increace CBMC_OBJECT_BITS to 9 After unrelated changes in 2a23fda1ab6199307b47e0d500febcff79030ddc, the CBMC proof for poly_getnoise_eta1122_4x failed with the following error: too many addressed objects: maximum number of objects is set to 2^n=256 (with n=8); use the `--object-bits n` option to increase the maximum number Changing CBMC_OBJECT_BITS to 9 solves that. Signed-off-by: Matthias J. Kannwischer --- cbmc/proofs/poly_getnoise_eta1122_4x/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cbmc/proofs/poly_getnoise_eta1122_4x/Makefile b/cbmc/proofs/poly_getnoise_eta1122_4x/Makefile index d59da7323..45fad13ed 100644 --- a/cbmc/proofs/poly_getnoise_eta1122_4x/Makefile +++ b/cbmc/proofs/poly_getnoise_eta1122_4x/Makefile @@ -43,7 +43,7 @@ FUNCTION_NAME = $(MLKEM_NAMESPACE)poly_getnoise_eta1122_4x # EXPENSIVE = true # This function is large enough to need... -CBMC_OBJECT_BITS = 8 +CBMC_OBJECT_BITS = 9 # If you require access to a file-local ("static") function or object to conduct # your proof, set the following (and do not include the original source file From 3f2f383d5fabeaff97803ac123b6250e40d5ac2d Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Wed, 20 Nov 2024 15:38:51 +0800 Subject: [PATCH 6/6] Add component benchmark for poly_compress_du + poly_decompress_du Signed-off-by: Matthias J. Kannwischer --- test/bench_components_mlkem.c | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/test/bench_components_mlkem.c b/test/bench_components_mlkem.c index 53b6f3da3..2e2774530 100644 --- a/test/bench_components_mlkem.c +++ b/test/bench_components_mlkem.c @@ -67,6 +67,13 @@ static int bench(void) { 1 * SHAKE128_RATE)) /* poly */ + // poly_compress_du + BENCH("poly_compress_du", poly_compress_du((uint8_t *)data0, (poly *)data1)) + + // poly_decompress_du + BENCH("poly_decompress_du", + poly_decompress_du((poly *)data0, (uint8_t *)data1)) + // poly_compress_dv BENCH("poly_compress_dv", poly_compress_dv((uint8_t *)data0, (poly *)data1))