Skip to content

Commit 97b2a78

Browse files
hanno-beckerhanno-becker
committed
CBMC: Pass uninitialized pointers in all verification harnesses
Previously, when a function under proof would assume a pointer to a structure, the verification harness would construct an instance of that structure on the stack and pass its address. This approach is unsound, because it adds to the contractual assumptions of the function the specifics of the function invocation in the test harness. For example, a missing bounds constraint in the spec might go undetected just because the stack-allocated variable happens to satisfy it. The most robust way to deal with this, so it seems, is to minimize the harnesses to merely pass uninitialized variables of the right type to the function under proof. In particular, where a pointer is expected, pass an uninitialized pointer, rather than the address of a stack allocated structure. Also, remove redundant `x != NULL` preconditions when `IS_FRESH(x,...)` is assumed. This is not only redundant, but also error prone because of diffblue/cbmc#8492. This commit implements those changes for all harnesses implemented so far. As it turns out, a few specs were incorrect because of missing IS_FRESH annotations, hidden by the correct allocation in the harness. Signed-off-by: Hanno Becker <[email protected]>
1 parent a364e4b commit 97b2a78

File tree

23 files changed

+91
-90
lines changed

23 files changed

+91
-90
lines changed

‎cbmc/proofs/basemul_cached/basemul_cached_harness.c

+1-1
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@
2323
*
2424
*/
2525
void harness(void) {
26-
int16_t a[2], b[2], r[2], b_cached;
26+
int16_t *a, *b, *r, b_cached;
2727

2828
basemul_cached(r, a, b, b_cached);
2929
}

‎cbmc/proofs/cmov_int16/cmov_int16_harness.c

+2-2
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@
2323
*/
2424
void harness(void) {
2525
uint16_t b;
26-
int16_t r, v;
26+
int16_t *r, v;
2727

28-
cmov_int16(&r, v, b);
28+
cmov_int16(r, v, b);
2929
}

‎cbmc/proofs/poly_basemul_montgomery_cached/poly_basemul_montgomery_cached_harness.c

+3-3
Original file line numberDiff line numberDiff line change
@@ -22,8 +22,8 @@
2222
*
2323
*/
2424
void harness(void) {
25-
poly r, a, b;
26-
poly_mulcache b_cached;
25+
poly *r, *a, *b;
26+
poly_mulcache *b_cached;
2727

28-
poly_basemul_montgomery_cached(&r, &a, &b, &b_cached);
28+
poly_basemul_montgomery_cached(r, a, b, b_cached);
2929
}

‎cbmc/proofs/poly_cbd_eta1/poly_cbd_eta1_harness.c

+3-3
Original file line numberDiff line numberDiff line change
@@ -22,8 +22,8 @@
2222
*
2323
*/
2424
void harness(void) {
25-
uint8_t buf[MLKEM_ETA1 * MLKEM_N / 4];
26-
poly a;
25+
uint8_t *buf;
26+
poly *a;
2727

28-
poly_cbd_eta1(&a, buf);
28+
poly_cbd_eta1(a, buf);
2929
}

‎cbmc/proofs/poly_cbd_eta2/poly_cbd_eta2_harness.c

+3-3
Original file line numberDiff line numberDiff line change
@@ -22,8 +22,8 @@
2222
*
2323
*/
2424
void harness(void) {
25-
uint8_t buf[MLKEM_ETA2 * MLKEM_N / 4];
26-
poly a;
25+
uint8_t *buf;
26+
poly *a;
2727

28-
poly_cbd_eta2(&a, buf);
28+
poly_cbd_eta2(a, buf);
2929
}

‎cbmc/proofs/poly_compress/poly_compress_harness.c

+3-3
Original file line numberDiff line numberDiff line change
@@ -22,8 +22,8 @@
2222
*
2323
*/
2424
void harness(void) {
25-
poly r;
26-
uint8_t a[MLKEM_POLYCOMPRESSEDBYTES];
25+
poly *r;
26+
uint8_t *a;
2727

28-
poly_compress(a, &r);
28+
poly_compress(a, r);
2929
}

‎cbmc/proofs/poly_decompress/poly_decompress_harness.c

+3-3
Original file line numberDiff line numberDiff line change
@@ -22,8 +22,8 @@
2222
*
2323
*/
2424
void harness(void) {
25-
poly r;
26-
uint8_t a[MLKEM_POLYCOMPRESSEDBYTES];
25+
poly *r;
26+
uint8_t *a;
2727

28-
poly_decompress(&r, a);
28+
poly_decompress(r, a);
2929
}

‎cbmc/proofs/poly_frombytes/poly_frombytes_harness.c

+3-3
Original file line numberDiff line numberDiff line change
@@ -22,9 +22,9 @@
2222
*
2323
*/
2424
void harness(void) {
25-
poly a;
26-
uint8_t r[MLKEM_POLYBYTES];
25+
poly *a;
26+
uint8_t *r;
2727

2828
/* Contracts for this function are in poly.h */
29-
poly_frombytes(&a, r);
29+
poly_frombytes(a, r);
3030
}

‎cbmc/proofs/poly_getnoise_eta1122_4x/poly_getnoise_eta1122_4x_harness.c

+3-3
Original file line numberDiff line numberDiff line change
@@ -22,10 +22,10 @@
2222
*
2323
*/
2424
void harness(void) {
25-
uint8_t seed[MLKEM_SYMBYTES];
26-
poly r0, r1, r2, r3;
25+
uint8_t *seed;
26+
poly *r0, *r1, *r2, *r3;
2727
uint8_t nonce0, nonce1, nonce2, nonce3;
2828

29-
poly_getnoise_eta1122_4x(&r0, &r1, &r2, &r3, seed, nonce0, nonce1, nonce2,
29+
poly_getnoise_eta1122_4x(r0, r1, r2, r3, seed, nonce0, nonce1, nonce2,
3030
nonce3);
3131
}

‎cbmc/proofs/poly_getnoise_eta1_4x/poly_getnoise_eta1_4x_harness.c

+3-4
Original file line numberDiff line numberDiff line change
@@ -22,10 +22,9 @@
2222
*
2323
*/
2424
void harness(void) {
25-
uint8_t seed[MLKEM_SYMBYTES];
26-
poly r0, r1, r2, r3;
25+
uint8_t *seed;
26+
poly *r0, *r1, *r2, *r3;
2727
uint8_t nonce0, nonce1, nonce2, nonce3;
2828

29-
poly_getnoise_eta1_4x(&r0, &r1, &r2, &r3, seed, nonce0, nonce1, nonce2,
30-
nonce3);
29+
poly_getnoise_eta1_4x(r0, r1, r2, r3, seed, nonce0, nonce1, nonce2, nonce3);
3130
}

‎cbmc/proofs/poly_getnoise_eta2/poly_getnoise_eta2_harness.c

+3-3
Original file line numberDiff line numberDiff line change
@@ -22,9 +22,9 @@
2222
*
2323
*/
2424
void harness(void) {
25-
uint8_t seed[MLKEM_SYMBYTES];
26-
poly r;
25+
uint8_t *seed;
26+
poly *r;
2727
uint8_t nonce;
2828

29-
poly_getnoise_eta2(&r, seed, nonce);
29+
poly_getnoise_eta2(r, seed, nonce);
3030
}

‎cbmc/proofs/poly_getnoise_eta2_4x/poly_getnoise_eta2_4x_harness.c

+3-4
Original file line numberDiff line numberDiff line change
@@ -22,10 +22,9 @@
2222
*
2323
*/
2424
void harness(void) {
25-
uint8_t seed[MLKEM_SYMBYTES];
26-
poly r0, r1, r2, r3;
25+
uint8_t *seed;
26+
poly *r0, *r1, *r2, *r3;
2727
uint8_t nonce0, nonce1, nonce2, nonce3;
2828

29-
poly_getnoise_eta2_4x(&r0, &r1, &r2, &r3, seed, nonce0, nonce1, nonce2,
30-
nonce3);
29+
poly_getnoise_eta2_4x(r0, r1, r2, r3, seed, nonce0, nonce1, nonce2, nonce3);
3130
}

‎cbmc/proofs/poly_mulcache_compute/poly_mulcache_compute_harness.c

+3-3
Original file line numberDiff line numberDiff line change
@@ -23,8 +23,8 @@
2323
*
2424
*/
2525
void harness(void) {
26-
poly_mulcache x;
27-
poly a;
26+
poly_mulcache *x;
27+
poly *a;
2828

29-
poly_mulcache_compute(&x, &a);
29+
poly_mulcache_compute(x, a);
3030
}

‎cbmc/proofs/poly_reduce/poly_reduce_harness.c

+2-2
Original file line numberDiff line numberDiff line change
@@ -22,8 +22,8 @@
2222
*
2323
*/
2424
void harness(void) {
25-
poly a;
25+
poly *a;
2626

2727
/* Contracts for this function are in poly.h */
28-
poly_reduce(&a);
28+
poly_reduce(a);
2929
}

‎cbmc/proofs/poly_tobytes/poly_tobytes_harness.c

+3-3
Original file line numberDiff line numberDiff line change
@@ -22,9 +22,9 @@
2222
*
2323
*/
2424
void harness(void) {
25-
poly a;
26-
uint8_t r[MLKEM_POLYBYTES];
25+
poly *a;
26+
uint8_t *r;
2727

2828
/* Contracts for this function are in poly.h */
29-
poly_tobytes(r, &a);
29+
poly_tobytes(r, a);
3030
}

‎cbmc/proofs/poly_tomont/poly_tomont_harness.c

+2-2
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@
2222
*
2323
*/
2424
void harness(void) {
25-
poly a;
25+
poly *a;
2626

27-
poly_tomont(&a);
27+
poly_tomont(a);
2828
}

‎cbmc/proofs/polyvec_mulcache_compute/polyvec_mulcache_compute_harness.c

+3-3
Original file line numberDiff line numberDiff line change
@@ -22,8 +22,8 @@
2222
*
2323
*/
2424
void harness(void) {
25-
polyvec_mulcache x;
26-
polyvec a;
25+
polyvec_mulcache *x;
26+
polyvec *a;
2727

28-
polyvec_mulcache_compute(&x, &a);
28+
polyvec_mulcache_compute(x, a);
2929
}

‎mlkem/cbd.h

+4-4
Original file line numberDiff line numberDiff line change
@@ -19,8 +19,8 @@
1919
**************************************************/
2020
void poly_cbd_eta1(poly *r, const uint8_t buf[MLKEM_ETA1 * MLKEM_N / 4])
2121
// clang-format off
22-
REQUIRES(r != NULL && IS_FRESH(r, sizeof(poly)))
23-
REQUIRES(buf != NULL && IS_FRESH(buf, MLKEM_ETA1 * MLKEM_N / 4))
22+
REQUIRES(IS_FRESH(r, sizeof(poly)))
23+
REQUIRES(IS_FRESH(buf, MLKEM_ETA1 * MLKEM_N / 4))
2424
ASSIGNS(OBJECT_WHOLE(r))
2525
ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, -MLKEM_ETA1, MLKEM_ETA1));
2626
// clang-format on
@@ -38,8 +38,8 @@ ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, -MLKEM_ETA1, MLKEM_ET
3838
**************************************************/
3939
void poly_cbd_eta2(poly *r, const uint8_t buf[MLKEM_ETA2 * MLKEM_N / 4])
4040
// clang-format off
41-
REQUIRES(r != NULL && IS_FRESH(r, sizeof(poly)))
42-
REQUIRES(buf != NULL && IS_FRESH(buf, MLKEM_ETA2 * MLKEM_N / 4))
41+
REQUIRES(IS_FRESH(r, sizeof(poly)))
42+
REQUIRES(IS_FRESH(buf, MLKEM_ETA2 * MLKEM_N / 4))
4343
ASSIGNS(OBJECT_WHOLE(r))
4444
ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, -MLKEM_ETA2, MLKEM_ETA2));
4545
// clang-format on

‎mlkem/ntt.h

+3-3
Original file line numberDiff line numberDiff line change
@@ -47,9 +47,9 @@ void poly_invntt_tomont(poly *r);
4747
void basemul_cached(int16_t r[2], const int16_t a[2], const int16_t b[2],
4848
int16_t b_cached)
4949
// clang-format off
50-
REQUIRES(r != NULL && IS_FRESH(r, 2 * sizeof(int16_t)))
51-
REQUIRES(a != NULL && IS_FRESH(a, 2 * sizeof(int16_t)))
52-
REQUIRES(b != NULL && IS_FRESH(b, 2 * sizeof(int16_t)))
50+
REQUIRES(IS_FRESH(r, 2 * sizeof(int16_t)))
51+
REQUIRES(IS_FRESH(a, 2 * sizeof(int16_t)))
52+
REQUIRES(IS_FRESH(b, 2 * sizeof(int16_t)))
5353
REQUIRES(ARRAY_IN_BOUNDS(int, k, 0, 1, a, -(MLKEM_Q - 1), (MLKEM_Q - 1)))
5454
ASSIGNS(OBJECT_UPTO(r, 2 * sizeof(int16_t)))
5555
ENSURES(ARRAY_IN_BOUNDS(int, k, 0, 1, r, -3 * HALF_Q + 1, 3 * HALF_Q - 1));

‎mlkem/poly.h

+33-31
Original file line numberDiff line numberDiff line change
@@ -70,8 +70,8 @@ ENSURES(RETURN_VALUE == (int32_t)c + (((int32_t)c < 0) * MLKEM_Q));
7070
#define poly_compress MLKEM_NAMESPACE(poly_compress)
7171
void poly_compress(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES], const poly *a)
7272
// clang-format off
73-
REQUIRES(r != NULL && IS_FRESH(r, MLKEM_POLYCOMPRESSEDBYTES))
74-
REQUIRES(a != NULL && IS_FRESH(a, sizeof(poly)))
73+
REQUIRES(IS_FRESH(r, MLKEM_POLYCOMPRESSEDBYTES))
74+
REQUIRES(IS_FRESH(a, sizeof(poly)))
7575
REQUIRES(ARRAY_IN_BOUNDS(int, k, 0, (MLKEM_N - 1), a->coeffs, 0, (MLKEM_Q - 1)))
7676
ASSIGNS(OBJECT_WHOLE(r));
7777
// clang-format on
@@ -188,16 +188,17 @@ static inline uint16_t scalar_signed_to_unsigned_q_16(int16_t c) {
188188
#define poly_decompress MLKEM_NAMESPACE(poly_decompress)
189189
void poly_decompress(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES])
190190
// clang-format off
191-
REQUIRES(a != NULL && IS_FRESH(a, MLKEM_POLYCOMPRESSEDBYTES))
192-
REQUIRES(r != NULL && IS_FRESH(r, sizeof(poly)))
191+
REQUIRES(IS_FRESH(a, MLKEM_POLYCOMPRESSEDBYTES))
192+
REQUIRES(IS_FRESH(r, sizeof(poly)))
193193
ASSIGNS(OBJECT_WHOLE(r))
194194
ENSURES(ARRAY_IN_BOUNDS(int, k, 0, (MLKEM_N - 1), r->coeffs, 0, (MLKEM_Q - 1)));
195195
// clang-format on
196196

197197
#define poly_tobytes MLKEM_NAMESPACE(poly_tobytes)
198198
void poly_tobytes(uint8_t r[MLKEM_POLYBYTES], const poly *a)
199199
// clang-format off
200-
REQUIRES(a != NULL && IS_FRESH(a, sizeof(poly)))
200+
REQUIRES(IS_FRESH(r, MLKEM_POLYBYTES))
201+
REQUIRES(IS_FRESH(a, sizeof(poly)))
201202
REQUIRES(ARRAY_IN_BOUNDS(int, k, 0, (MLKEM_N - 1), a->coeffs, 0, (MLKEM_Q - 1)))
202203
ASSIGNS(OBJECT_WHOLE(r));
203204
// clang-format on
@@ -206,8 +207,8 @@ ASSIGNS(OBJECT_WHOLE(r));
206207
#define poly_frombytes MLKEM_NAMESPACE(poly_frombytes)
207208
void poly_frombytes(poly *r, const uint8_t a[MLKEM_POLYBYTES])
208209
// clang-format off
209-
REQUIRES(a != NULL && IS_FRESH(a, MLKEM_POLYBYTES))
210-
REQUIRES(r != NULL && IS_FRESH(r, sizeof(poly)))
210+
REQUIRES(IS_FRESH(a, MLKEM_POLYBYTES))
211+
REQUIRES(IS_FRESH(r, sizeof(poly)))
211212
ASSIGNS(OBJECT_WHOLE(r))
212213
ENSURES(ARRAY_IN_BOUNDS(int, k, 0, (MLKEM_N - 1), r->coeffs, 0, 4095));
213214
// clang-format on
@@ -234,11 +235,11 @@ void poly_getnoise_eta1_4x(poly *r0, poly *r1, poly *r2, poly *r3,
234235
const uint8_t seed[MLKEM_SYMBYTES], uint8_t nonce0,
235236
uint8_t nonce1, uint8_t nonce2,
236237
uint8_t nonce3) // clang-format off
237-
REQUIRES(r0 != NULL && IS_FRESH(r0, sizeof(poly)))
238-
REQUIRES(r1 != NULL && IS_FRESH(r1, sizeof(poly)))
239-
REQUIRES(r2 != NULL && IS_FRESH(r2, sizeof(poly)))
240-
REQUIRES(r3 != NULL && IS_FRESH(r3, sizeof(poly)))
241-
REQUIRES(seed != NULL && IS_FRESH(seed, MLKEM_SYMBYTES))
238+
REQUIRES(IS_FRESH(r0, sizeof(poly)))
239+
REQUIRES(IS_FRESH(r1, sizeof(poly)))
240+
REQUIRES(IS_FRESH(r2, sizeof(poly)))
241+
REQUIRES(IS_FRESH(r3, sizeof(poly)))
242+
REQUIRES(IS_FRESH(seed, MLKEM_SYMBYTES))
242243
ASSIGNS(OBJECT_WHOLE(r0), OBJECT_WHOLE(r1), OBJECT_WHOLE(r2), OBJECT_WHOLE(r3))
243244
ENSURES( \
244245
ARRAY_IN_BOUNDS(int, k0, 0, MLKEM_N - 1, r0->coeffs, -MLKEM_ETA1, MLKEM_ETA1) \
@@ -262,8 +263,8 @@ ENSURES(
262263
**************************************************/
263264
void poly_getnoise_eta2(poly *r, const uint8_t seed[MLKEM_SYMBYTES],
264265
uint8_t nonce) // clang-format off
265-
REQUIRES(r != NULL && IS_FRESH(r, sizeof(poly)))
266-
REQUIRES(seed != NULL && IS_FRESH(seed, MLKEM_SYMBYTES))
266+
REQUIRES(IS_FRESH(r, sizeof(poly)))
267+
REQUIRES(IS_FRESH(seed, MLKEM_SYMBYTES))
267268
ASSIGNS(OBJECT_WHOLE(r))
268269
ENSURES(ARRAY_IN_BOUNDS(int, k0, 0, MLKEM_N - 1, r->coeffs, -MLKEM_ETA2, MLKEM_ETA2));
269270
// clang-format on
@@ -285,11 +286,11 @@ void poly_getnoise_eta2_4x(poly *r0, poly *r1, poly *r2, poly *r3,
285286
const uint8_t seed[MLKEM_SYMBYTES], uint8_t nonce0,
286287
uint8_t nonce1, uint8_t nonce2,
287288
uint8_t nonce3) // clang-format off
288-
REQUIRES(r0 != NULL && IS_FRESH(r0, sizeof(poly)))
289-
REQUIRES(r1 != NULL && IS_FRESH(r1, sizeof(poly)))
290-
REQUIRES(r2 != NULL && IS_FRESH(r2, sizeof(poly)))
291-
REQUIRES(r3 != NULL && IS_FRESH(r3, sizeof(poly)))
292-
REQUIRES(seed != NULL && IS_FRESH(seed, MLKEM_SYMBYTES))
289+
REQUIRES(IS_FRESH(r0, sizeof(poly)))
290+
REQUIRES(IS_FRESH(r1, sizeof(poly)))
291+
REQUIRES(IS_FRESH(r2, sizeof(poly)))
292+
REQUIRES(IS_FRESH(r3, sizeof(poly)))
293+
REQUIRES(IS_FRESH(seed, MLKEM_SYMBYTES))
293294
ASSIGNS(OBJECT_WHOLE(r0), OBJECT_WHOLE(r1), OBJECT_WHOLE(r2), OBJECT_WHOLE(r3))
294295
ENSURES( \
295296
ARRAY_IN_BOUNDS(int, k0, 0, MLKEM_N - 1, r0->coeffs, -MLKEM_ETA2, MLKEM_ETA2) \
@@ -315,11 +316,11 @@ void poly_getnoise_eta1122_4x(poly *r0, poly *r1, poly *r2, poly *r3,
315316
const uint8_t seed[MLKEM_SYMBYTES],
316317
uint8_t nonce0, uint8_t nonce1, uint8_t nonce2,
317318
uint8_t nonce3) // clang-format off
318-
REQUIRES(r0 != NULL && IS_FRESH(r0, sizeof(poly)))
319-
REQUIRES(r1 != NULL && IS_FRESH(r1, sizeof(poly)))
320-
REQUIRES(r2 != NULL && IS_FRESH(r2, sizeof(poly)))
321-
REQUIRES(r3 != NULL && IS_FRESH(r3, sizeof(poly)))
322-
REQUIRES(seed != NULL && IS_FRESH(seed, MLKEM_SYMBYTES))
319+
REQUIRES(IS_FRESH(r0, sizeof(poly)))
320+
REQUIRES(IS_FRESH(r1, sizeof(poly)))
321+
REQUIRES(IS_FRESH(r2, sizeof(poly)))
322+
REQUIRES(IS_FRESH(r3, sizeof(poly)))
323+
REQUIRES(IS_FRESH(seed, MLKEM_SYMBYTES))
323324
ASSIGNS(OBJECT_WHOLE(r0), OBJECT_WHOLE(r1), OBJECT_WHOLE(r2), OBJECT_WHOLE(r3))
324325
ENSURES( \
325326
ARRAY_IN_BOUNDS(int, k0, 0, MLKEM_N - 1, r0->coeffs, -MLKEM_ETA1, MLKEM_ETA1) \
@@ -351,10 +352,10 @@ ENSURES(
351352
void poly_basemul_montgomery_cached(poly *r, const poly *a, const poly *b,
352353
const poly_mulcache *b_cache)
353354
// clang-format off
354-
REQUIRES(r != NULL && IS_FRESH(r, sizeof(poly)))
355-
REQUIRES(a != NULL && IS_FRESH(a, sizeof(poly)))
356-
REQUIRES(b != NULL && IS_FRESH(b, sizeof(poly)))
357-
REQUIRES(b_cache != NULL && IS_FRESH(b_cache, sizeof(poly_mulcache)))
355+
REQUIRES(IS_FRESH(r, sizeof(poly)))
356+
REQUIRES(IS_FRESH(a, sizeof(poly)))
357+
REQUIRES(IS_FRESH(b, sizeof(poly)))
358+
REQUIRES(IS_FRESH(b_cache, sizeof(poly_mulcache)))
358359
REQUIRES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, a->coeffs, -(MLKEM_Q - 1), (MLKEM_Q - 1)))
359360
ASSIGNS(OBJECT_WHOLE(r))
360361
ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, -3 * HALF_Q + 1, 3 * HALF_Q - 1));
@@ -373,7 +374,7 @@ ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, -3 * HALF_Q + 1, 3 *
373374
**************************************************/
374375
void poly_tomont(poly *r)
375376
// clang-format off
376-
REQUIRES(r != NULL && IS_FRESH(r, sizeof(poly)))
377+
REQUIRES(IS_FRESH(r, sizeof(poly)))
377378
ASSIGNS(OBJECT_WHOLE(r))
378379
ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, -(MLKEM_Q - 1), (MLKEM_Q - 1)));
379380
// clang-format on
@@ -402,7 +403,8 @@ ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, -(MLKEM_Q - 1), (MLKE
402403
// higher level safety proofs, and thus not part of the spec.
403404
void poly_mulcache_compute(poly_mulcache *x, const poly *a)
404405
// clang-format off
405-
REQUIRES(a != NULL && IS_FRESH(a, sizeof(poly)))
406+
REQUIRES(IS_FRESH(x, sizeof(poly_mulcache)))
407+
REQUIRES(IS_FRESH(a, sizeof(poly)))
406408
ASSIGNS(OBJECT_WHOLE(x));
407409
// clang-format on
408410

@@ -424,7 +426,7 @@ ASSIGNS(OBJECT_WHOLE(x));
424426
// use of poly_reduce() in the context of (de)serialization.
425427
void poly_reduce(poly *r)
426428
// clang-format off
427-
REQUIRES(r != NULL && IS_FRESH(r, sizeof(poly)))
429+
REQUIRES(IS_FRESH(r, sizeof(poly)))
428430
ASSIGNS(OBJECT_WHOLE(r))
429431
ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, 0, MLKEM_Q - 1));
430432
// clang-format on

‎mlkem/polyvec.h

+2-1
Original file line numberDiff line numberDiff line change
@@ -71,7 +71,8 @@ void polyvec_basemul_acc_montgomery_cached(poly *r, const polyvec *a,
7171
// higher level safety proofs, and thus not part of the spec.
7272
void polyvec_mulcache_compute(polyvec_mulcache *x, const polyvec *a)
7373
// clang-format off
74-
REQUIRES(a != NULL && IS_FRESH(a, sizeof(polyvec)))
74+
REQUIRES(IS_FRESH(x, sizeof(polyvec_mulcache)))
75+
REQUIRES(IS_FRESH(a, sizeof(polyvec)))
7576
ASSIGNS(OBJECT_WHOLE(x));
7677
// clang-format on
7778

0 commit comments

Comments
 (0)