|
34 | 34 | * unsigned canonical coefficients here.
|
35 | 35 | * The reference implementation works with coefficients
|
36 | 36 | * in the range (-MLKEM_Q+1,...,MLKEM_Q-1). */
|
37 |
| -static void mlk_poly_compress_d4_c(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D4], |
38 |
| - const mlk_poly *a) |
| 37 | +MLK_STATIC_TESTABLE void mlk_poly_compress_d4_c( |
| 38 | + uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D4], const mlk_poly *a) |
39 | 39 | {
|
40 | 40 | unsigned i;
|
41 | 41 | mlk_assert_bound(a, MLKEM_N, 0, MLKEM_Q);
|
@@ -83,8 +83,8 @@ void mlk_poly_compress_d4(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D4],
|
83 | 83 | * unsigned canonical coefficients here.
|
84 | 84 | * The reference implementation works with coefficients
|
85 | 85 | * in the range (-MLKEM_Q+1,...,MLKEM_Q-1). */
|
86 |
| -static void mlk_poly_compress_d10_c(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D10], |
87 |
| - const mlk_poly *a) |
| 86 | +MLK_STATIC_TESTABLE void mlk_poly_compress_d10_c( |
| 87 | + uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D10], const mlk_poly *a) |
88 | 88 | {
|
89 | 89 | unsigned j;
|
90 | 90 | mlk_assert_bound(a, MLKEM_N, 0, MLKEM_Q);
|
@@ -132,7 +132,7 @@ void mlk_poly_compress_d10(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D10],
|
132 | 132 |
|
133 | 133 | /* Reference: `poly_decompress()` in the reference implementation @[REF],
|
134 | 134 | * for ML-KEM-{512,768}. */
|
135 |
| -static void mlk_poly_decompress_d4_c( |
| 135 | +MLK_STATIC_TESTABLE void mlk_poly_decompress_d4_c( |
136 | 136 | mlk_poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_D4])
|
137 | 137 | {
|
138 | 138 | unsigned i;
|
@@ -167,7 +167,7 @@ void mlk_poly_decompress_d4(mlk_poly *r,
|
167 | 167 |
|
168 | 168 | /* Reference: Embedded into `polyvec_decompress()` in the
|
169 | 169 | * reference implementation, for ML-KEM-{512,768}. */
|
170 |
| -static void mlk_poly_decompress_d10_c( |
| 170 | +MLK_STATIC_TESTABLE void mlk_poly_decompress_d10_c( |
171 | 171 | mlk_poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_D10])
|
172 | 172 | {
|
173 | 173 | unsigned j;
|
@@ -222,8 +222,8 @@ void mlk_poly_decompress_d10(mlk_poly *r,
|
222 | 222 | * unsigned canonical coefficients here.
|
223 | 223 | * The reference implementation works with coefficients
|
224 | 224 | * in the range (-MLKEM_Q+1,...,MLKEM_Q-1). */
|
225 |
| -static void mlk_poly_compress_d5_c(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D5], |
226 |
| - const mlk_poly *a) |
| 225 | +MLK_STATIC_TESTABLE void mlk_poly_compress_d5_c( |
| 226 | + uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D5], const mlk_poly *a) |
227 | 227 | {
|
228 | 228 | unsigned i;
|
229 | 229 | mlk_assert_bound(a, MLKEM_N, 0, MLKEM_Q);
|
@@ -277,8 +277,8 @@ void mlk_poly_compress_d5(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D5],
|
277 | 277 | * unsigned canonical coefficients here.
|
278 | 278 | * The reference implementation works with coefficients
|
279 | 279 | * in the range (-MLKEM_Q+1,...,MLKEM_Q-1). */
|
280 |
| -static void mlk_poly_compress_d11_c(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D11], |
281 |
| - const mlk_poly *a) |
| 280 | +MLK_STATIC_TESTABLE void mlk_poly_compress_d11_c( |
| 281 | + uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D11], const mlk_poly *a) |
282 | 282 | {
|
283 | 283 | unsigned j;
|
284 | 284 | mlk_assert_bound(a, MLKEM_N, 0, MLKEM_Q);
|
@@ -333,7 +333,7 @@ void mlk_poly_compress_d11(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D11],
|
333 | 333 |
|
334 | 334 | /* Reference: `poly_decompress()` in the reference implementation @[REF],
|
335 | 335 | * for ML-KEM-1024. */
|
336 |
| -static void mlk_poly_decompress_d5_c( |
| 336 | +MLK_STATIC_TESTABLE void mlk_poly_decompress_d5_c( |
337 | 337 | mlk_poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_D5])
|
338 | 338 | {
|
339 | 339 | unsigned i;
|
@@ -396,7 +396,7 @@ void mlk_poly_decompress_d5(mlk_poly *r,
|
396 | 396 |
|
397 | 397 | /* Reference: Embedded into `polyvec_decompress()` in the
|
398 | 398 | * reference implementation, for ML-KEM-1024. */
|
399 |
| -static void mlk_poly_decompress_d11_c( |
| 399 | +MLK_STATIC_TESTABLE void mlk_poly_decompress_d11_c( |
400 | 400 | mlk_poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_D11])
|
401 | 401 | {
|
402 | 402 | unsigned j;
|
@@ -455,7 +455,8 @@ void mlk_poly_decompress_d11(mlk_poly *r,
|
455 | 455 | * unsigned canonical coefficients here.
|
456 | 456 | * The reference implementation works with coefficients
|
457 | 457 | * in the range (-MLKEM_Q+1,...,MLKEM_Q-1). */
|
458 |
| -static void mlk_poly_tobytes_c(uint8_t r[MLKEM_POLYBYTES], const mlk_poly *a) |
| 458 | +MLK_STATIC_TESTABLE void mlk_poly_tobytes_c(uint8_t r[MLKEM_POLYBYTES], |
| 459 | + const mlk_poly *a) |
459 | 460 | __contract__(
|
460 | 461 | requires(memory_no_alias(r, MLKEM_POLYBYTES))
|
461 | 462 | requires(memory_no_alias(a, sizeof(mlk_poly)))
|
@@ -509,7 +510,8 @@ void mlk_poly_tobytes(uint8_t r[MLKEM_POLYBYTES], const mlk_poly *a)
|
509 | 510 | }
|
510 | 511 |
|
511 | 512 | /* Reference: `poly_frombytes()` in the reference implementation @[REF]. */
|
512 |
| -static void mlk_poly_frombytes_c(mlk_poly *r, const uint8_t a[MLKEM_POLYBYTES]) |
| 513 | +MLK_STATIC_TESTABLE void mlk_poly_frombytes_c(mlk_poly *r, |
| 514 | + const uint8_t a[MLKEM_POLYBYTES]) |
513 | 515 | __contract__(
|
514 | 516 | requires(memory_no_alias(a, MLKEM_POLYBYTES))
|
515 | 517 | requires(memory_no_alias(r, sizeof(mlk_poly)))
|
|
0 commit comments