Skip to content

CBMC: Pass uninitialized pointers in all verification harnesses #340

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

Merged
merged 1 commit into from
Nov 5, 2024
Merged

CBMC: Pass uninitialized pointers in all verification harnesses #340

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
2 changes: 1 addition & 1 deletion cbmc/proofs/basemul_cached/basemul_cached_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@
*
*/
void harness(void) {
int16_t a[2], b[2], r[2], b_cached;
int16_t *a, *b, *r, b_cached;

basemul_cached(r, a, b, b_cached);
}
4 changes: 2 additions & 2 deletions cbmc/proofs/cmov_int16/cmov_int16_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@
*/
void harness(void) {
uint16_t b;
int16_t r, v;
int16_t *r, v;

cmov_int16(&r, v, b);
cmov_int16(r, v, b);
}
6 changes: 3 additions & 3 deletions cbmc/proofs/poly_basemul_montgomery_cached/poly_basemul_montgomery_cached_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,8 @@
*
*/
void harness(void) {
poly r, a, b;
poly_mulcache b_cached;
poly *r, *a, *b;
poly_mulcache *b_cached;

poly_basemul_montgomery_cached(&r, &a, &b, &b_cached);
poly_basemul_montgomery_cached(r, a, b, b_cached);
}
6 changes: 3 additions & 3 deletions cbmc/proofs/poly_cbd_eta1/poly_cbd_eta1_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,8 @@
*
*/
void harness(void) {
uint8_t buf[MLKEM_ETA1 * MLKEM_N / 4];
poly a;
uint8_t *buf;
poly *a;

poly_cbd_eta1(&a, buf);
poly_cbd_eta1(a, buf);
}
6 changes: 3 additions & 3 deletions cbmc/proofs/poly_cbd_eta2/poly_cbd_eta2_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,8 @@
*
*/
void harness(void) {
uint8_t buf[MLKEM_ETA2 * MLKEM_N / 4];
poly a;
uint8_t *buf;
poly *a;

poly_cbd_eta2(&a, buf);
poly_cbd_eta2(a, buf);
}
6 changes: 3 additions & 3 deletions cbmc/proofs/poly_compress/poly_compress_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,8 @@
*
*/
void harness(void) {
poly r;
uint8_t a[MLKEM_POLYCOMPRESSEDBYTES];
poly *r;
uint8_t *a;

poly_compress(a, &r);
poly_compress(a, r);
}
6 changes: 3 additions & 3 deletions cbmc/proofs/poly_decompress/poly_decompress_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,8 @@
*
*/
void harness(void) {
poly r;
uint8_t a[MLKEM_POLYCOMPRESSEDBYTES];
poly *r;
uint8_t *a;

poly_decompress(&r, a);
poly_decompress(r, a);
}
6 changes: 3 additions & 3 deletions cbmc/proofs/poly_frombytes/poly_frombytes_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,9 +22,9 @@
*
*/
void harness(void) {
poly a;
uint8_t r[MLKEM_POLYBYTES];
poly *a;
uint8_t *r;

/* Contracts for this function are in poly.h */
poly_frombytes(&a, r);
poly_frombytes(a, r);
}
6 changes: 3 additions & 3 deletions cbmc/proofs/poly_getnoise_eta1122_4x/poly_getnoise_eta1122_4x_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,10 +22,10 @@
*
*/
void harness(void) {
uint8_t seed[MLKEM_SYMBYTES];
poly r0, r1, r2, r3;
uint8_t *seed;
poly *r0, *r1, *r2, *r3;
uint8_t nonce0, nonce1, nonce2, nonce3;

poly_getnoise_eta1122_4x(&r0, &r1, &r2, &r3, seed, nonce0, nonce1, nonce2,
poly_getnoise_eta1122_4x(r0, r1, r2, r3, seed, nonce0, nonce1, nonce2,
nonce3);
}
7 changes: 3 additions & 4 deletions cbmc/proofs/poly_getnoise_eta1_4x/poly_getnoise_eta1_4x_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,10 +22,9 @@
*
*/
void harness(void) {
uint8_t seed[MLKEM_SYMBYTES];
poly r0, r1, r2, r3;
uint8_t *seed;
poly *r0, *r1, *r2, *r3;
uint8_t nonce0, nonce1, nonce2, nonce3;

poly_getnoise_eta1_4x(&r0, &r1, &r2, &r3, seed, nonce0, nonce1, nonce2,
nonce3);
poly_getnoise_eta1_4x(r0, r1, r2, r3, seed, nonce0, nonce1, nonce2, nonce3);
}
6 changes: 3 additions & 3 deletions cbmc/proofs/poly_getnoise_eta2/poly_getnoise_eta2_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,9 +22,9 @@
*
*/
void harness(void) {
uint8_t seed[MLKEM_SYMBYTES];
poly r;
uint8_t *seed;
poly *r;
uint8_t nonce;

poly_getnoise_eta2(&r, seed, nonce);
poly_getnoise_eta2(r, seed, nonce);
}
7 changes: 3 additions & 4 deletions cbmc/proofs/poly_getnoise_eta2_4x/poly_getnoise_eta2_4x_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,10 +22,9 @@
*
*/
void harness(void) {
uint8_t seed[MLKEM_SYMBYTES];
poly r0, r1, r2, r3;
uint8_t *seed;
poly *r0, *r1, *r2, *r3;
uint8_t nonce0, nonce1, nonce2, nonce3;

poly_getnoise_eta2_4x(&r0, &r1, &r2, &r3, seed, nonce0, nonce1, nonce2,
nonce3);
poly_getnoise_eta2_4x(r0, r1, r2, r3, seed, nonce0, nonce1, nonce2, nonce3);
}
6 changes: 3 additions & 3 deletions cbmc/proofs/poly_mulcache_compute/poly_mulcache_compute_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,8 +23,8 @@
*
*/
void harness(void) {
poly_mulcache x;
poly a;
poly_mulcache *x;
poly *a;

poly_mulcache_compute(&x, &a);
poly_mulcache_compute(x, a);
}
4 changes: 2 additions & 2 deletions cbmc/proofs/poly_reduce/poly_reduce_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,8 @@
*
*/
void harness(void) {
poly a;
poly *a;

/* Contracts for this function are in poly.h */
poly_reduce(&a);
poly_reduce(a);
}
6 changes: 3 additions & 3 deletions cbmc/proofs/poly_tobytes/poly_tobytes_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,9 +22,9 @@
*
*/
void harness(void) {
poly a;
uint8_t r[MLKEM_POLYBYTES];
poly *a;
uint8_t *r;

/* Contracts for this function are in poly.h */
poly_tobytes(r, &a);
poly_tobytes(r, a);
}
4 changes: 2 additions & 2 deletions cbmc/proofs/poly_tomont/poly_tomont_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@
*
*/
void harness(void) {
poly a;
poly *a;

poly_tomont(&a);
poly_tomont(a);
}
6 changes: 3 additions & 3 deletions cbmc/proofs/polyvec_mulcache_compute/polyvec_mulcache_compute_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,8 @@
*
*/
void harness(void) {
polyvec_mulcache x;
polyvec a;
polyvec_mulcache *x;
polyvec *a;

polyvec_mulcache_compute(&x, &a);
polyvec_mulcache_compute(x, a);
}
8 changes: 4 additions & 4 deletions mlkem/cbd.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,8 @@
**************************************************/
void poly_cbd_eta1(poly *r, const uint8_t buf[MLKEM_ETA1 * MLKEM_N / 4])
// clang-format off
REQUIRES(r != NULL && IS_FRESH(r, sizeof(poly)))
REQUIRES(buf != NULL && IS_FRESH(buf, MLKEM_ETA1 * MLKEM_N / 4))
REQUIRES(IS_FRESH(r, sizeof(poly)))
REQUIRES(IS_FRESH(buf, MLKEM_ETA1 * MLKEM_N / 4))
ASSIGNS(OBJECT_WHOLE(r))
ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, -MLKEM_ETA1, MLKEM_ETA1));
// clang-format on
Expand All @@ -38,8 +38,8 @@ ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, -MLKEM_ETA1, MLKEM_ET
**************************************************/
void poly_cbd_eta2(poly *r, const uint8_t buf[MLKEM_ETA2 * MLKEM_N / 4])
// clang-format off
REQUIRES(r != NULL && IS_FRESH(r, sizeof(poly)))
REQUIRES(buf != NULL && IS_FRESH(buf, MLKEM_ETA2 * MLKEM_N / 4))
REQUIRES(IS_FRESH(r, sizeof(poly)))
REQUIRES(IS_FRESH(buf, MLKEM_ETA2 * MLKEM_N / 4))
ASSIGNS(OBJECT_WHOLE(r))
ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, -MLKEM_ETA2, MLKEM_ETA2));
// clang-format on
Expand Down
6 changes: 3 additions & 3 deletions mlkem/ntt.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,9 +47,9 @@ void poly_invntt_tomont(poly *r);
void basemul_cached(int16_t r[2], const int16_t a[2], const int16_t b[2],
int16_t b_cached)
// clang-format off
REQUIRES(r != NULL && IS_FRESH(r, 2 * sizeof(int16_t)))
REQUIRES(a != NULL && IS_FRESH(a, 2 * sizeof(int16_t)))
REQUIRES(b != NULL && IS_FRESH(b, 2 * sizeof(int16_t)))
REQUIRES(IS_FRESH(r, 2 * sizeof(int16_t)))
REQUIRES(IS_FRESH(a, 2 * sizeof(int16_t)))
REQUIRES(IS_FRESH(b, 2 * sizeof(int16_t)))
REQUIRES(ARRAY_IN_BOUNDS(int, k, 0, 1, a, -(MLKEM_Q - 1), (MLKEM_Q - 1)))
ASSIGNS(OBJECT_UPTO(r, 2 * sizeof(int16_t)))
ENSURES(ARRAY_IN_BOUNDS(int, k, 0, 1, r, -3 * HALF_Q + 1, 3 * HALF_Q - 1));
Expand Down
64 changes: 33 additions & 31 deletions mlkem/poly.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -70,8 +70,8 @@ ENSURES(RETURN_VALUE == (int32_t)c + (((int32_t)c < 0) * MLKEM_Q));
#define poly_compress MLKEM_NAMESPACE(poly_compress)
void poly_compress(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES], const poly *a)
// clang-format off
REQUIRES(r != NULL && IS_FRESH(r, MLKEM_POLYCOMPRESSEDBYTES))
REQUIRES(a != NULL && IS_FRESH(a, sizeof(poly)))
REQUIRES(IS_FRESH(r, MLKEM_POLYCOMPRESSEDBYTES))
REQUIRES(IS_FRESH(a, sizeof(poly)))
REQUIRES(ARRAY_IN_BOUNDS(int, k, 0, (MLKEM_N - 1), a->coeffs, 0, (MLKEM_Q - 1)))
ASSIGNS(OBJECT_WHOLE(r));
// clang-format on
Expand Down Expand Up @@ -188,16 +188,17 @@ static inline uint16_t scalar_signed_to_unsigned_q_16(int16_t c) {
#define poly_decompress MLKEM_NAMESPACE(poly_decompress)
void poly_decompress(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES])
// clang-format off
REQUIRES(a != NULL && IS_FRESH(a, MLKEM_POLYCOMPRESSEDBYTES))
REQUIRES(r != NULL && IS_FRESH(r, sizeof(poly)))
REQUIRES(IS_FRESH(a, MLKEM_POLYCOMPRESSEDBYTES))
REQUIRES(IS_FRESH(r, sizeof(poly)))
ASSIGNS(OBJECT_WHOLE(r))
ENSURES(ARRAY_IN_BOUNDS(int, k, 0, (MLKEM_N - 1), r->coeffs, 0, (MLKEM_Q - 1)));
// clang-format on

#define poly_tobytes MLKEM_NAMESPACE(poly_tobytes)
void poly_tobytes(uint8_t r[MLKEM_POLYBYTES], const poly *a)
// clang-format off
REQUIRES(a != NULL && IS_FRESH(a, sizeof(poly)))
REQUIRES(IS_FRESH(r, MLKEM_POLYBYTES))
REQUIRES(IS_FRESH(a, sizeof(poly)))
REQUIRES(ARRAY_IN_BOUNDS(int, k, 0, (MLKEM_N - 1), a->coeffs, 0, (MLKEM_Q - 1)))
ASSIGNS(OBJECT_WHOLE(r));
// clang-format on
Expand All @@ -206,8 +207,8 @@ ASSIGNS(OBJECT_WHOLE(r));
#define poly_frombytes MLKEM_NAMESPACE(poly_frombytes)
void poly_frombytes(poly *r, const uint8_t a[MLKEM_POLYBYTES])
// clang-format off
REQUIRES(a != NULL && IS_FRESH(a, MLKEM_POLYBYTES))
REQUIRES(r != NULL && IS_FRESH(r, sizeof(poly)))
REQUIRES(IS_FRESH(a, MLKEM_POLYBYTES))
REQUIRES(IS_FRESH(r, sizeof(poly)))
ASSIGNS(OBJECT_WHOLE(r))
ENSURES(ARRAY_IN_BOUNDS(int, k, 0, (MLKEM_N - 1), r->coeffs, 0, 4095));
// clang-format on
Expand All @@ -234,11 +235,11 @@ void poly_getnoise_eta1_4x(poly *r0, poly *r1, poly *r2, poly *r3,
const uint8_t seed[MLKEM_SYMBYTES], uint8_t nonce0,
uint8_t nonce1, uint8_t nonce2,
uint8_t nonce3) // clang-format off
REQUIRES(r0 != NULL && IS_FRESH(r0, sizeof(poly)))
REQUIRES(r1 != NULL && IS_FRESH(r1, sizeof(poly)))
REQUIRES(r2 != NULL && IS_FRESH(r2, sizeof(poly)))
REQUIRES(r3 != NULL && IS_FRESH(r3, sizeof(poly)))
REQUIRES(seed != NULL && IS_FRESH(seed, MLKEM_SYMBYTES))
REQUIRES(IS_FRESH(r0, sizeof(poly)))
REQUIRES(IS_FRESH(r1, sizeof(poly)))
REQUIRES(IS_FRESH(r2, sizeof(poly)))
REQUIRES(IS_FRESH(r3, sizeof(poly)))
REQUIRES(IS_FRESH(seed, MLKEM_SYMBYTES))
ASSIGNS(OBJECT_WHOLE(r0), OBJECT_WHOLE(r1), OBJECT_WHOLE(r2), OBJECT_WHOLE(r3))
ENSURES( \
ARRAY_IN_BOUNDS(int, k0, 0, MLKEM_N - 1, r0->coeffs, -MLKEM_ETA1, MLKEM_ETA1) \
Expand All @@ -262,8 +263,8 @@ ENSURES(
**************************************************/
void poly_getnoise_eta2(poly *r, const uint8_t seed[MLKEM_SYMBYTES],
uint8_t nonce) // clang-format off
REQUIRES(r != NULL && IS_FRESH(r, sizeof(poly)))
REQUIRES(seed != NULL && IS_FRESH(seed, MLKEM_SYMBYTES))
REQUIRES(IS_FRESH(r, sizeof(poly)))
REQUIRES(IS_FRESH(seed, MLKEM_SYMBYTES))
ASSIGNS(OBJECT_WHOLE(r))
ENSURES(ARRAY_IN_BOUNDS(int, k0, 0, MLKEM_N - 1, r->coeffs, -MLKEM_ETA2, MLKEM_ETA2));
// clang-format on
Expand All @@ -285,11 +286,11 @@ void poly_getnoise_eta2_4x(poly *r0, poly *r1, poly *r2, poly *r3,
const uint8_t seed[MLKEM_SYMBYTES], uint8_t nonce0,
uint8_t nonce1, uint8_t nonce2,
uint8_t nonce3) // clang-format off
REQUIRES(r0 != NULL && IS_FRESH(r0, sizeof(poly)))
REQUIRES(r1 != NULL && IS_FRESH(r1, sizeof(poly)))
REQUIRES(r2 != NULL && IS_FRESH(r2, sizeof(poly)))
REQUIRES(r3 != NULL && IS_FRESH(r3, sizeof(poly)))
REQUIRES(seed != NULL && IS_FRESH(seed, MLKEM_SYMBYTES))
REQUIRES(IS_FRESH(r0, sizeof(poly)))
REQUIRES(IS_FRESH(r1, sizeof(poly)))
REQUIRES(IS_FRESH(r2, sizeof(poly)))
REQUIRES(IS_FRESH(r3, sizeof(poly)))
REQUIRES(IS_FRESH(seed, MLKEM_SYMBYTES))
ASSIGNS(OBJECT_WHOLE(r0), OBJECT_WHOLE(r1), OBJECT_WHOLE(r2), OBJECT_WHOLE(r3))
ENSURES( \
ARRAY_IN_BOUNDS(int, k0, 0, MLKEM_N - 1, r0->coeffs, -MLKEM_ETA2, MLKEM_ETA2) \
Expand All @@ -315,11 +316,11 @@ void poly_getnoise_eta1122_4x(poly *r0, poly *r1, poly *r2, poly *r3,
const uint8_t seed[MLKEM_SYMBYTES],
uint8_t nonce0, uint8_t nonce1, uint8_t nonce2,
uint8_t nonce3) // clang-format off
REQUIRES(r0 != NULL && IS_FRESH(r0, sizeof(poly)))
REQUIRES(r1 != NULL && IS_FRESH(r1, sizeof(poly)))
REQUIRES(r2 != NULL && IS_FRESH(r2, sizeof(poly)))
REQUIRES(r3 != NULL && IS_FRESH(r3, sizeof(poly)))
REQUIRES(seed != NULL && IS_FRESH(seed, MLKEM_SYMBYTES))
REQUIRES(IS_FRESH(r0, sizeof(poly)))
REQUIRES(IS_FRESH(r1, sizeof(poly)))
REQUIRES(IS_FRESH(r2, sizeof(poly)))
REQUIRES(IS_FRESH(r3, sizeof(poly)))
REQUIRES(IS_FRESH(seed, MLKEM_SYMBYTES))
ASSIGNS(OBJECT_WHOLE(r0), OBJECT_WHOLE(r1), OBJECT_WHOLE(r2), OBJECT_WHOLE(r3))
ENSURES( \
ARRAY_IN_BOUNDS(int, k0, 0, MLKEM_N - 1, r0->coeffs, -MLKEM_ETA1, MLKEM_ETA1) \
Expand Down Expand Up @@ -351,10 +352,10 @@ ENSURES(
void poly_basemul_montgomery_cached(poly *r, const poly *a, const poly *b,
const poly_mulcache *b_cache)
// clang-format off
REQUIRES(r != NULL && IS_FRESH(r, sizeof(poly)))
REQUIRES(a != NULL && IS_FRESH(a, sizeof(poly)))
REQUIRES(b != NULL && IS_FRESH(b, sizeof(poly)))
REQUIRES(b_cache != NULL && IS_FRESH(b_cache, sizeof(poly_mulcache)))
REQUIRES(IS_FRESH(r, sizeof(poly)))
REQUIRES(IS_FRESH(a, sizeof(poly)))
REQUIRES(IS_FRESH(b, sizeof(poly)))
REQUIRES(IS_FRESH(b_cache, sizeof(poly_mulcache)))
REQUIRES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, a->coeffs, -(MLKEM_Q - 1), (MLKEM_Q - 1)))
ASSIGNS(OBJECT_WHOLE(r))
ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, -3 * HALF_Q + 1, 3 * HALF_Q - 1));
Expand All @@ -373,7 +374,7 @@ ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, -3 * HALF_Q + 1, 3 *
**************************************************/
void poly_tomont(poly *r)
// clang-format off
REQUIRES(r != NULL && IS_FRESH(r, sizeof(poly)))
REQUIRES(IS_FRESH(r, sizeof(poly)))
ASSIGNS(OBJECT_WHOLE(r))
ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, -(MLKEM_Q - 1), (MLKEM_Q - 1)));
// clang-format on
Expand Down Expand Up @@ -402,7 +403,8 @@ ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, -(MLKEM_Q - 1), (MLKE
// higher level safety proofs, and thus not part of the spec.
void poly_mulcache_compute(poly_mulcache *x, const poly *a)
// clang-format off
REQUIRES(a != NULL && IS_FRESH(a, sizeof(poly)))
REQUIRES(IS_FRESH(x, sizeof(poly_mulcache)))
REQUIRES(IS_FRESH(a, sizeof(poly)))
ASSIGNS(OBJECT_WHOLE(x));
// clang-format on

Expand All @@ -424,7 +426,7 @@ ASSIGNS(OBJECT_WHOLE(x));
// use of poly_reduce() in the context of (de)serialization.
void poly_reduce(poly *r)
// clang-format off
REQUIRES(r != NULL && IS_FRESH(r, sizeof(poly)))
REQUIRES(IS_FRESH(r, sizeof(poly)))
ASSIGNS(OBJECT_WHOLE(r))
ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, 0, MLKEM_Q - 1));
// clang-format on
Expand Down
3 changes: 2 additions & 1 deletion mlkem/polyvec.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,8 @@ void polyvec_basemul_acc_montgomery_cached(poly *r, const polyvec *a,
// higher level safety proofs, and thus not part of the spec.
void polyvec_mulcache_compute(polyvec_mulcache *x, const polyvec *a)
// clang-format off
REQUIRES(a != NULL && IS_FRESH(a, sizeof(polyvec)))
REQUIRES(IS_FRESH(x, sizeof(polyvec_mulcache)))
REQUIRES(IS_FRESH(a, sizeof(polyvec)))
ASSIGNS(OBJECT_WHOLE(x));
// clang-format on

Expand Down
Loading