From d18e99516e66ac416a36fdc779585d7c23af2a74 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Fri, 18 Oct 2024 15:26:33 +0100 Subject: [PATCH] Prevent clang-format from formatting CBMC contracts on function declarations Wrap function declaration contracts in // clang-format off // clang-format on pairs to prevent reformatting of these sections. Signed-off-by: Rod Chapman --- mlkem/poly.h | 63 ++++++++++++++++++++++++++++++++------------------ mlkem/reduce.h | 12 ++++++---- 2 files changed, 48 insertions(+), 27 deletions(-) diff --git a/mlkem/poly.h b/mlkem/poly.h index 173263ec7..6471a6e03 100644 --- a/mlkem/poly.h +++ b/mlkem/poly.h @@ -34,32 +34,46 @@ typedef struct { KYBER_NAMESPACE(scalar_signed_to_unsigned_q_16) static inline uint32_t scalar_compress_q_16(int32_t u) - REQUIRES(0 <= u && u <= (KYBER_Q - 1)) ENSURES(RETURN_VALUE < 16) - ENSURES(RETURN_VALUE == - (((uint32_t)u * 16 + KYBER_Q / 2) / KYBER_Q) % 16); + // clang-format off +REQUIRES(0 <= u && u <= (KYBER_Q - 1)) +ENSURES(RETURN_VALUE < 16) +ENSURES(RETURN_VALUE == (((uint32_t)u * 16 + KYBER_Q / 2) / KYBER_Q) % 16); +// clang-format on static inline uint32_t scalar_decompress_q_16(uint32_t u) - REQUIRES(0 <= u && u < 16) ENSURES(RETURN_VALUE <= (KYBER_Q - 1)); + // clang-format off +REQUIRES(0 <= u && u < 16) +ENSURES(RETURN_VALUE <= (KYBER_Q - 1)); +// clang-format on static inline uint32_t scalar_compress_q_32(int32_t u) - REQUIRES(0 <= u && u <= (KYBER_Q - 1)) ENSURES(RETURN_VALUE < 32) - ENSURES(RETURN_VALUE == - (((uint32_t)u * 32 + KYBER_Q / 2) / KYBER_Q) % 32); + // clang-format off +REQUIRES(0 <= u && u <= (KYBER_Q - 1)) +ENSURES(RETURN_VALUE < 32) +ENSURES(RETURN_VALUE == (((uint32_t)u * 32 + KYBER_Q / 2) / KYBER_Q) % 32); +// clang-format on static inline uint32_t scalar_decompress_q_32(uint32_t u) - REQUIRES(0 <= u && u < 32) ENSURES(RETURN_VALUE <= (KYBER_Q - 1)); + // clang-format off +REQUIRES(0 <= u && u < 32) +ENSURES(RETURN_VALUE <= (KYBER_Q - 1)); +// clang-format on static inline uint16_t scalar_signed_to_unsigned_q_16(int16_t c) - REQUIRES(c >= -(KYBER_Q - 1) && c <= (KYBER_Q - 1)) - ENSURES(RETURN_VALUE >= 0 && RETURN_VALUE <= (KYBER_Q - 1)) - ENSURES(RETURN_VALUE == (int32_t)c + (((int32_t)c < 0) * KYBER_Q)); + // clang-format off +REQUIRES(c >= -(KYBER_Q - 1) && c <= (KYBER_Q - 1)) +ENSURES(RETURN_VALUE >= 0 && RETURN_VALUE <= (KYBER_Q - 1)) +ENSURES(RETURN_VALUE == (int32_t)c + (((int32_t)c < 0) * KYBER_Q)); +// clang-format on #define poly_compress KYBER_NAMESPACE(poly_compress) void poly_compress(uint8_t r[KYBER_POLYCOMPRESSEDBYTES], const poly *a) - REQUIRES(r != NULL && IS_FRESH(r, KYBER_POLYCOMPRESSEDBYTES)) - REQUIRES(a != NULL && IS_FRESH(a, sizeof(poly))) - REQUIRES(ARRAY_IN_BOUNDS(int, k, 0, (KYBER_N - 1), a->coeffs, 0, - (KYBER_Q - 1))) ASSIGNS(OBJECT_WHOLE(r)); + // clang-format off +REQUIRES(r != NULL && IS_FRESH(r, KYBER_POLYCOMPRESSEDBYTES)) +REQUIRES(a != NULL && IS_FRESH(a, sizeof(poly))) +REQUIRES(ARRAY_IN_BOUNDS(int, k, 0, (KYBER_N - 1), a->coeffs, 0, (KYBER_Q - 1))) +ASSIGNS(OBJECT_WHOLE(r)); +// clang-format on /************************************************************ * Name: scalar_compress_q_16 @@ -172,17 +186,20 @@ static inline uint16_t scalar_signed_to_unsigned_q_16(int16_t c) { #define poly_decompress KYBER_NAMESPACE(poly_decompress) void poly_decompress(poly *r, const uint8_t a[KYBER_POLYCOMPRESSEDBYTES]) - REQUIRES(a != NULL && IS_FRESH(a, KYBER_POLYCOMPRESSEDBYTES)) - REQUIRES(r != NULL && IS_FRESH(r, sizeof(poly))) - ASSIGNS(OBJECT_WHOLE(r)) - ENSURES(ARRAY_IN_BOUNDS(int, k, 0, (KYBER_N - 1), r->coeffs, 0, - (KYBER_Q - 1))); + // clang-format off +REQUIRES(a != NULL && IS_FRESH(a, KYBER_POLYCOMPRESSEDBYTES)) +REQUIRES(r != NULL && IS_FRESH(r, sizeof(poly))) +ASSIGNS(OBJECT_WHOLE(r)) +ENSURES(ARRAY_IN_BOUNDS(int, k, 0, (KYBER_N - 1), r->coeffs, 0, (KYBER_Q - 1))); +// clang-format on #define poly_tobytes KYBER_NAMESPACE(poly_tobytes) void poly_tobytes(uint8_t r[KYBER_POLYBYTES], const poly *a) - REQUIRES(a != NULL && IS_FRESH(a, sizeof(poly))) - REQUIRES(ARRAY_IN_BOUNDS(int, k, 0, (KYBER_N - 1), a->coeffs, 0, - (KYBER_Q - 1))) ASSIGNS(OBJECT_WHOLE(r)); + // clang-format off +REQUIRES(a != NULL && IS_FRESH(a, sizeof(poly))) +REQUIRES(ARRAY_IN_BOUNDS(int, k, 0, (KYBER_N - 1), a->coeffs, 0, (KYBER_Q - 1))) +ASSIGNS(OBJECT_WHOLE(r)); +// clang-format on #define poly_frombytes KYBER_NAMESPACE(poly_frombytes) diff --git a/mlkem/reduce.h b/mlkem/reduce.h index 46df6b1e4..7859961dd 100644 --- a/mlkem/reduce.h +++ b/mlkem/reduce.h @@ -11,13 +11,17 @@ #define montgomery_reduce KYBER_NAMESPACE(montgomery_reduce) int16_t montgomery_reduce(int32_t a) - REQUIRES(a >= INT32_MIN + (32768 * KYBER_Q)) - REQUIRES(a <= INT32_MAX - (32768 * KYBER_Q)) - ENSURES(RETURN_VALUE >= INT16_MIN && RETURN_VALUE <= INT16_MAX); + // clang-format off +REQUIRES(a >= INT32_MIN + (32768 * KYBER_Q)) +REQUIRES(a <= INT32_MAX - (32768 * KYBER_Q)) +ENSURES(RETURN_VALUE >= INT16_MIN && RETURN_VALUE <= INT16_MAX); +// clang-format on #define barrett_reduce KYBER_NAMESPACE(barrett_reduce) int16_t barrett_reduce(int16_t a) - ENSURES(RETURN_VALUE >= -HALF_Q && RETURN_VALUE <= HALF_Q); + // clang-format off +ENSURES(RETURN_VALUE >= -HALF_Q && RETURN_VALUE <= HALF_Q); +// clang-format on /************************************************* * Name: fqmul