Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Prevent clang-format from formatting CBMC contracts on functions #258

Merged
merged 1 commit into from
Oct 18, 2024
Merged

Prevent clang-format from formatting CBMC contracts on functions #258

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
63 changes: 40 additions & 23 deletions mlkem/poly.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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)
Expand Down
12 changes: 8 additions & 4 deletions mlkem/reduce.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down