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

CBMC: More minor clean-up #381

Merged
merged 3 commits into from
Nov 13, 2024
Merged

CBMC: More minor clean-up #381

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
c359d84
remove cbmc/sources
mkannwischer Nov 12, 2024
34c7890
CBMC: Use ARRAY_ABS_BOUND everywhere
mkannwischer Nov 12, 2024
4d9a005
Rename ARRAY_IN_BOUNDS to ARRAY_BOUND and change argument order
mkannwischer Nov 12, 2024
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
4 changes: 2 additions & 2 deletions cbmc/proofs/proof_guide.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -374,12 +374,12 @@ We can use the macros in `cbmc.h` to help, thus:
void poly_tobytes(uint8_t r[MLKEM_POLYBYTES], const poly *a)
// clang-format off
REQUIRES(IS_FRESH(a, sizeof(poly)))
REQUIRES(ARRAY_IN_BOUNDS(int, k, 0, (MLKEM_N - 1), a->coeffs, 0, (MLKEM_Q - 1)))
REQUIRES(ARRAY_BOUND(a->coeffs, 0, (MLKEM_N - 1), 0, (MLKEM_Q - 1)))
ASSIGNS(OBJECT_WHOLE(r));
// clang-format on
```

`ARRAY_IN_BOUNDS` is a macro that expands to a quantified expression that expresses that the elemtns of `a->coeffs` between index values `0` and `(MLKEM_N - 1)` (inclusive) are in the range `0` through `(MLKEM_Q - 1)` (also inclusive). See the macro definition in `mlkem/cbmc.h` for details.
`ARRAY_BOUND` is a macro that expands to a quantified expression that expresses that the elemtns of `a->coeffs` between index values `0` and `(MLKEM_N - 1)` (inclusive) are in the range `0` through `(MLKEM_Q - 1)` (also inclusive). See the macro definition in `mlkem/cbmc.h` for details.

### Interior contracts and loop invariants

Expand Down
8 changes: 0 additions & 8 deletions cbmc/sources/README.md
View file
Open in desktop

This file was deleted.

8 changes: 4 additions & 4 deletions mlkem/cbd.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,7 @@ static void cbd2(poly *r, const uint8_t buf[2 * MLKEM_N / 4]) {
for (i = 0; i < MLKEM_N / 8; i++) // clang-format off
ASSIGNS(i, j, a, b, t, d, OBJECT_WHOLE(r))
INVARIANT(i >= 0 && i <= MLKEM_N / 8)
INVARIANT(ARRAY_IN_BOUNDS(0, (8 * i - 1), r->coeffs, -2, +2)) // clang-format on
INVARIANT(ARRAY_ABS_BOUND(r->coeffs, 0, (8 * i - 1), 2)) // clang-format on
{
t = load32_littleendian(buf + 4 * i);
d = t & 0x55555555;
Expand All @@ -70,7 +70,7 @@ static void cbd2(poly *r, const uint8_t buf[2 * MLKEM_N / 4]) {
for (j = 0; j < 8; j++) // clang-format off
ASSIGNS(j, a, b, OBJECT_WHOLE(r))
INVARIANT(i >= 0 && i <= MLKEM_N / 8 && j >= 0 && j <= 8)
INVARIANT(ARRAY_IN_BOUNDS(0, 8 * i + j - 1, r->coeffs, -2, +2)) // clang-format on
INVARIANT(ARRAY_ABS_BOUND(r->coeffs, 0, 8 * i + j - 1, 2)) // clang-format on
{
a = (d >> (4 * j + 0)) & 0x3;
b = (d >> (4 * j + 2)) & 0x3;
Expand Down Expand Up @@ -99,7 +99,7 @@ static void cbd3(poly *r, const uint8_t buf[3 * MLKEM_N / 4]) {
for (i = 0; i < MLKEM_N / 4; i++) // clang-format off
ASSIGNS(i, j, a, b, t, d, OBJECT_WHOLE(r))
INVARIANT(i >= 0 && i <= MLKEM_N / 4)
INVARIANT(ARRAY_IN_BOUNDS(0, (4 * i - 1), r->coeffs, -3, +3)) // clang-format on
INVARIANT(ARRAY_ABS_BOUND(r->coeffs, 0, (4 * i - 1), 3)) // clang-format on
{
t = load24_littleendian(buf + 3 * i);
d = t & 0x00249249;
Expand All @@ -109,7 +109,7 @@ static void cbd3(poly *r, const uint8_t buf[3 * MLKEM_N / 4]) {
for (j = 0; j < 4; j++) // clang-format off
ASSIGNS(j, a, b, OBJECT_WHOLE(r))
INVARIANT(i >= 0 && i <= MLKEM_N / 4 && j >= 0 && j <= 4)
INVARIANT(ARRAY_IN_BOUNDS(0, 4 * i + j - 1, r->coeffs, -3, +3)) // clang-format on
INVARIANT(ARRAY_ABS_BOUND(r->coeffs, 0, 4 * i + j - 1, 3)) // clang-format on
{
a = (d >> (6 * j + 0)) & 0x7;
b = (d >> (6 * j + 3)) & 0x7;
Expand Down
4 changes: 2 additions & 2 deletions mlkem/cbd.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ void poly_cbd_eta1(
REQUIRES(IS_FRESH(r, sizeof(poly)))
REQUIRES(IS_FRESH(buf, MLKEM_ETA1 * MLKEM_N / 4))
ASSIGNS(OBJECT_UPTO(r, sizeof(poly)))
ENSURES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r->coeffs, -MLKEM_ETA1, MLKEM_ETA1));
ENSURES(ARRAY_ABS_BOUND(r->coeffs, 0, MLKEM_N - 1, MLKEM_ETA1));
// clang-format on

#define poly_cbd_eta2 MLKEM_NAMESPACE(poly_cbd_eta2)
Expand All @@ -43,7 +43,7 @@ void poly_cbd_eta2(
REQUIRES(IS_FRESH(r, sizeof(poly)))
REQUIRES(IS_FRESH(buf, MLKEM_ETA2 * MLKEM_N / 4))
ASSIGNS(OBJECT_UPTO(r, sizeof(poly)))
ENSURES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r->coeffs, -MLKEM_ETA2, MLKEM_ETA2));
ENSURES(ARRAY_ABS_BOUND(r->coeffs, 0, MLKEM_N - 1, MLKEM_ETA2));
// clang-format on

#endif
14 changes: 7 additions & 7 deletions mlkem/cbmc.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -109,7 +109,7 @@
// range value_lb .. value_ub (inclusive)"
//
// Example:
// ARRAY_IN_BOUNDS(0, MLKEM_N-1, a->coeffs, -(MLKEM_Q - 1), MLKEM_Q - 1)
// ARRAY_BOUND(a->coeffs, 0, MLKEM_N-1, -(MLKEM_Q - 1), MLKEM_Q - 1)
// expands to
// __CPROVER_forall { int k; (0 <= k && k <= MLKEM_N-1) ==> ( (-(MLKEM_Q -
// 1) <= a->coeffs[k]) && (a->coeffs[k] <= (MLKEM_Q - 1))) }
Expand All @@ -120,7 +120,7 @@
#define CBMC_CONCAT_(left, right) left##right
#define CBMC_CONCAT(left, right) CBMC_CONCAT_(left,right)

#define ARRAY_IN_BOUNDS_CORE(indextype, qvar, qvar_lb, qvar_ub, array_var, \
#define ARRAY_BOUND_CORE(indextype, qvar, qvar_lb, qvar_ub, array_var, \
value_lb, value_ub) \
__CPROVER_forall \
{ \
Expand All @@ -130,15 +130,15 @@
((array_var[(qvar)]) <= (value_ub))) \
}

#define ARRAY_IN_BOUNDS(qvar_lb, qvar_ub, array_var, \
value_lb, value_ub) \
ARRAY_IN_BOUNDS_CORE(int, CBMC_CONCAT(_cbmc_idx,__LINE__), \
#define ARRAY_BOUND(array_var, qvar_lb, qvar_ub, \
value_lb, value_ub) \
ARRAY_BOUND_CORE(int, CBMC_CONCAT(_cbmc_idx,__LINE__), \
(qvar_lb), (qvar_ub), (array_var), (value_lb), (value_ub))

// clang-format on

// Wrapper around ARRAY_IN_BOUNDS operating on absolute values
// Wrapper around ARRAY_BOUND operating on absolute values
#define ARRAY_ABS_BOUND(arr, lb, ub, k) \
ARRAY_IN_BOUNDS((lb), (ub), (arr), (-(k)), (k))
ARRAY_BOUND((arr), (lb), (ub), (-(k)), (k))

#endif
35 changes: 17 additions & 18 deletions mlkem/indcpa.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ REQUIRES(IS_FRESH(r, MLKEM_INDCPA_PUBLICKEYBYTES))
REQUIRES(IS_FRESH(pk, sizeof(polyvec)))
REQUIRES(IS_FRESH(seed, MLKEM_SYMBYTES))
REQUIRES(FORALL(int, k0, 0, MLKEM_K - 1,
ARRAY_IN_BOUNDS(0, MLKEM_N - 1, pk->vec[k0].coeffs, 0, (MLKEM_Q - 1))))
ARRAY_BOUND(pk->vec[k0].coeffs, 0, MLKEM_N - 1, 0, (MLKEM_Q - 1))))
ASSIGNS(OBJECT_WHOLE(r)) // clang-format on
{
POLYVEC_BOUND(pk, MLKEM_Q);
Expand Down Expand Up @@ -66,7 +66,7 @@ REQUIRES(IS_FRESH(packedpk, MLKEM_INDCPA_PUBLICKEYBYTES))
REQUIRES(IS_FRESH(pk, sizeof(polyvec)))
REQUIRES(IS_FRESH(seed, MLKEM_SYMBYTES))
ENSURES(FORALL(int, k0, 0, MLKEM_K - 1,
ARRAY_IN_BOUNDS(0, MLKEM_N - 1, pk->vec[k0].coeffs, 0, (MLKEM_Q - 1))))
ARRAY_BOUND(pk->vec[k0].coeffs, 0, MLKEM_N - 1, 0, (MLKEM_Q - 1))))
ASSIGNS(OBJECT_WHOLE(pk))
ASSIGNS(OBJECT_WHOLE(seed)) // clang-format on
{
Expand Down Expand Up @@ -94,7 +94,7 @@ void pack_sk(uint8_t r[MLKEM_INDCPA_SECRETKEYBYTES],
REQUIRES(IS_FRESH(r, MLKEM_INDCPA_SECRETKEYBYTES))
REQUIRES(IS_FRESH(sk, sizeof(polyvec)))
REQUIRES(FORALL(int, k0, 0, MLKEM_K - 1,
ARRAY_IN_BOUNDS(0, MLKEM_N - 1, sk->vec[k0].coeffs, 0, (MLKEM_Q - 1))))
ARRAY_BOUND(sk->vec[k0].coeffs, 0, MLKEM_N - 1, 0, (MLKEM_Q - 1))))
ASSIGNS(OBJECT_WHOLE(r))
// clang-format on
{
Expand All @@ -119,7 +119,7 @@ void unpack_sk(
REQUIRES(IS_FRESH(packedsk, MLKEM_INDCPA_SECRETKEYBYTES))
REQUIRES(IS_FRESH(sk, sizeof(polyvec)))
ENSURES(FORALL(int, k0, 0, MLKEM_K - 1,
ARRAY_IN_BOUNDS(0, MLKEM_N - 1, sk->vec[k0].coeffs, 0, (MLKEM_Q - 1))))
ARRAY_BOUND(sk->vec[k0].coeffs, 0, MLKEM_N - 1, 0, (MLKEM_Q - 1))))
ASSIGNS(OBJECT_WHOLE(sk)) // clang-format on
{
polyvec_frombytes(sk, packedsk);
Expand Down Expand Up @@ -162,8 +162,8 @@ REQUIRES(IS_FRESH(c, MLKEM_INDCPA_BYTES))
ASSIGNS(OBJECT_WHOLE(b))
ASSIGNS(OBJECT_WHOLE(v))
ENSURES(FORALL(int, k0, 0, MLKEM_K - 1,
ARRAY_IN_BOUNDS(0, (MLKEM_N - 1), b->vec[k0].coeffs, 0, (MLKEM_Q - 1))))
ENSURES(ARRAY_IN_BOUNDS(0, (MLKEM_N - 1), v->coeffs, 0, (MLKEM_Q - 1)))
ARRAY_BOUND(b->vec[k0].coeffs, 0, (MLKEM_N - 1), 0, (MLKEM_Q - 1))))
ENSURES(ARRAY_BOUND(v->coeffs, 0, (MLKEM_N - 1), 0, (MLKEM_Q - 1)))
// clang-format on
{
polyvec_decompress(b, c);
Expand All @@ -184,10 +184,10 @@ void gen_matrix_entry_x4(poly *vec, uint8_t *seed[4]) // clang-format off
REQUIRES(IS_FRESH(seed[2], MLKEM_SYMBYTES + 2))
REQUIRES(IS_FRESH(seed[3], MLKEM_SYMBYTES + 2))
ASSIGNS(OBJECT_UPTO(vec, sizeof(poly) * 4))
ENSURES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, vec[0].coeffs, 0, (MLKEM_Q - 1)))
ENSURES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, vec[1].coeffs, 0, (MLKEM_Q - 1)))
ENSURES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, vec[2].coeffs, 0, (MLKEM_Q - 1)))
ENSURES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, vec[3].coeffs, 0, (MLKEM_Q - 1)))
ENSURES(ARRAY_BOUND(vec[0].coeffs, 0, MLKEM_N - 1, 0, (MLKEM_Q - 1)))
ENSURES(ARRAY_BOUND(vec[1].coeffs, 0, MLKEM_N - 1, 0, (MLKEM_Q - 1)))
ENSURES(ARRAY_BOUND(vec[2].coeffs, 0, MLKEM_N - 1, 0, (MLKEM_Q - 1)))
ENSURES(ARRAY_BOUND(vec[3].coeffs, 0, MLKEM_N - 1, 0, (MLKEM_Q - 1)))
// clang-format on
{
// Temporary buffers for XOF output before rejection sampling
Expand Down Expand Up @@ -223,10 +223,10 @@ void gen_matrix_entry_x4(poly *vec, uint8_t *seed[4]) // clang-format off
OBJECT_WHOLE(buf1), OBJECT_WHOLE(buf2), OBJECT_WHOLE(buf3))
INVARIANT(ctr[0] <= MLKEM_N && ctr[1] <= MLKEM_N)
INVARIANT(ctr[2] <= MLKEM_N && ctr[3] <= MLKEM_N)
INVARIANT(ctr[0] > 0 ==> ARRAY_IN_BOUNDS(0, ctr[0] - 1, vec[0].coeffs, 0, (MLKEM_Q - 1)))
INVARIANT(ctr[1] > 0 ==> ARRAY_IN_BOUNDS(0, ctr[1] - 1, vec[1].coeffs, 0, (MLKEM_Q - 1)))
INVARIANT(ctr[2] > 0 ==> ARRAY_IN_BOUNDS(0, ctr[2] - 1, vec[2].coeffs, 0, (MLKEM_Q - 1)))
INVARIANT(ctr[3] > 0 ==> ARRAY_IN_BOUNDS(0, ctr[3] - 1, vec[3].coeffs, 0, (MLKEM_Q - 1)))
INVARIANT(ctr[0] > 0 ==> ARRAY_BOUND(vec[0].coeffs, 0, ctr[0] - 1, 0, (MLKEM_Q - 1)))
INVARIANT(ctr[1] > 0 ==> ARRAY_BOUND(vec[1].coeffs, 0, ctr[1] - 1, 0, (MLKEM_Q - 1)))
INVARIANT(ctr[2] > 0 ==> ARRAY_BOUND(vec[2].coeffs, 0, ctr[2] - 1, 0, (MLKEM_Q - 1)))
INVARIANT(ctr[3] > 0 ==> ARRAY_BOUND(vec[3].coeffs, 0, ctr[3] - 1, 0, (MLKEM_Q - 1)))
// clang-format on
{
shake128x4_squeezeblocks(buf0, buf1, buf2, buf3, 1, &statex);
Expand All @@ -247,7 +247,7 @@ void gen_matrix_entry(poly *entry,
REQUIRES(IS_FRESH(entry, sizeof(poly)))
REQUIRES(IS_FRESH(seed, MLKEM_SYMBYTES + 2))
ASSIGNS(OBJECT_UPTO(entry, sizeof(poly)))
ENSURES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, entry->coeffs, 0, (MLKEM_Q - 1)))
ENSURES(ARRAY_BOUND(entry->coeffs, 0, MLKEM_N - 1, 0, (MLKEM_Q - 1)))
{ // clang-format on
shake128ctx state;
uint8_t buf[GEN_MATRIX_NBLOCKS * SHAKE128_RATE];
Expand All @@ -266,7 +266,7 @@ void gen_matrix_entry(poly *entry,
while (ctr < MLKEM_N) // clang-format off
ASSIGNS(ctr, state, OBJECT_UPTO(entry, sizeof(poly)), OBJECT_WHOLE(buf))
INVARIANT(0 <= ctr && ctr <= MLKEM_N)
INVARIANT(ctr > 0 ==> ARRAY_IN_BOUNDS(0, ctr - 1, entry->coeffs,
INVARIANT(ctr > 0 ==> ARRAY_BOUND(entry->coeffs, 0, ctr - 1,
0, (MLKEM_Q - 1))) // clang-format on
{
shake128_squeezeblocks(buf, 1, &state);
Expand Down Expand Up @@ -384,8 +384,7 @@ void matvec_mul(polyvec *out, const polyvec a[MLKEM_K], const polyvec *v,
REQUIRES(IS_FRESH(vc, sizeof(polyvec_mulcache)))
REQUIRES(FORALL(int, k0, 0, MLKEM_K - 1,
FORALL(int, k1, 0, MLKEM_K - 1,
ARRAY_IN_BOUNDS(0, MLKEM_N - 1,
a[k0].vec[k1].coeffs, -(MLKEM_Q - 1), (MLKEM_Q - 1)))))
ARRAY_ABS_BOUND(a[k0].vec[k1].coeffs, 0, MLKEM_N - 1, (MLKEM_Q - 1)))))
ASSIGNS(OBJECT_WHOLE(out))
// clang-format on
{
Expand Down
2 changes: 1 addition & 1 deletion mlkem/indcpa.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ REQUIRES(IS_FRESH(seed, MLKEM_SYMBYTES))
REQUIRES(transposed == 0 || transposed == 1)
ASSIGNS(OBJECT_WHOLE(a))
ENSURES(FORALL(int, x, 0, MLKEM_K - 1, FORALL(int, y, 0, MLKEM_K - 1,
ARRAY_IN_BOUNDS(0, MLKEM_N - 1, a[x].vec[y].coeffs, 0, (MLKEM_Q - 1)))));
ARRAY_BOUND(a[x].vec[y].coeffs, 0, MLKEM_N - 1, 0, (MLKEM_Q - 1)))));
// clang-format on

#define indcpa_keypair_derand MLKEM_NAMESPACE(indcpa_keypair_derand)
Expand Down
10 changes: 5 additions & 5 deletions mlkem/ntt.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,9 +33,9 @@ extern const int16_t zetas[128];
#define poly_ntt MLKEM_NAMESPACE(poly_ntt)
void poly_ntt(poly *r) // clang-format off
REQUIRES(IS_FRESH(r, sizeof(poly)))
REQUIRES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r->coeffs, -(MLKEM_Q - 1), MLKEM_Q - 1))
REQUIRES(ARRAY_ABS_BOUND(r->coeffs, 0, MLKEM_N - 1, MLKEM_Q - 1))
ASSIGNS(OBJECT_UPTO(r, sizeof(poly)))
ENSURES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r->coeffs, -(NTT_BOUND - 1), NTT_BOUND - 1));
ENSURES(ARRAY_ABS_BOUND(r->coeffs, 0, MLKEM_N - 1, NTT_BOUND - 1));
// clang-format on

/*************************************************
Expand All @@ -58,7 +58,7 @@ ENSURES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r->coeffs, -(NTT_BOUND - 1), NTT_BOUND -
void poly_invntt_tomont(poly *r) // clang-format off
REQUIRES(IS_FRESH(r, sizeof(poly)))
ASSIGNS(OBJECT_UPTO(r, sizeof(poly)))
ENSURES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r->coeffs, -(INVNTT_BOUND - 1), INVNTT_BOUND - 1));
ENSURES(ARRAY_ABS_BOUND(r->coeffs, 0, MLKEM_N - 1, INVNTT_BOUND - 1));
// clang-format on

#define basemul_cached MLKEM_NAMESPACE(basemul_cached)
Expand Down Expand Up @@ -87,9 +87,9 @@ void basemul_cached(int16_t r[2], const int16_t a[2], const int16_t b[2],
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(0, 1, a, -(MLKEM_Q - 1), (MLKEM_Q - 1)))
REQUIRES(ARRAY_ABS_BOUND(a, 0, 1, MLKEM_Q - 1))
ASSIGNS(OBJECT_UPTO(r, 2 * sizeof(int16_t)))
ENSURES(ARRAY_IN_BOUNDS(0, 1, r, -(3 * HALF_Q - 1), (3 * HALF_Q - 1)));
ENSURES(ARRAY_ABS_BOUND(r, 0, 1, (3 * HALF_Q - 1)));
// clang-format on


Expand Down
22 changes: 11 additions & 11 deletions mlkem/poly.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ void poly_compress(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES], const poly *a) {
for (int j = 0; j < 8; j++) // clang-format off
ASSIGNS(j, OBJECT_WHOLE(t))
INVARIANT(i >= 0 && i <= MLKEM_N / 8 && j >= 0 && j <= 8)
INVARIANT(ARRAY_IN_BOUNDS(0, (j-1), t, 0, 15))
INVARIANT(ARRAY_BOUND(t, 0, (j-1), 0, 15))
{ // clang-format on
// REF-CHANGE: Precondition change, we assume unsigned canonical data
t[j] = scalar_compress_d4(a->coeffs[8 * i + j]);
Expand All @@ -47,7 +47,7 @@ void poly_compress(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES], const poly *a) {
for (int j = 0; j < 8; j++) // clang-format off
ASSIGNS(j, OBJECT_WHOLE(t))
INVARIANT(i >= 0 && i <= MLKEM_N / 8 && j >= 0 && j <= 8)
INVARIANT(ARRAY_IN_BOUNDS(0, (j-1), t, 0, 31))
INVARIANT(ARRAY_BOUND(t, 0, (j-1), 0, 31))
{ // clang-format on
// REF-CHANGE: Precondition change, we assume unsigned canonical data
t[j] = scalar_compress_d5(a->coeffs[8 * i + j]);
Expand All @@ -72,7 +72,7 @@ void poly_decompress(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES]) {
for (int i = 0; i < MLKEM_N / 2; i++) // clang-format off
ASSIGNS(i, OBJECT_WHOLE(r))
INVARIANT(i >= 0 && i <= MLKEM_N / 2)
INVARIANT(ARRAY_IN_BOUNDS(0, (2 * i - 1), r->coeffs, 0, (MLKEM_Q - 1)))
INVARIANT(ARRAY_BOUND(r->coeffs, 0, (2 * i - 1), 0, (MLKEM_Q - 1)))
{ // clang-format on
// REF-CHANGE: Hoist scalar decompression into separate function
r->coeffs[2 * i + 0] = scalar_decompress_d4((a[i] >> 0) & 0xF);
Expand All @@ -82,7 +82,7 @@ void poly_decompress(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES]) {
for (int i = 0; i < MLKEM_N / 8; i++) // clang-format off
ASSIGNS(i, OBJECT_WHOLE(r))
INVARIANT(i >= 0 && i <= MLKEM_N / 8)
INVARIANT(ARRAY_IN_BOUNDS(0, (8 * i - 1), r->coeffs, 0, (MLKEM_Q - 1)))
INVARIANT(ARRAY_BOUND(r->coeffs, 0, (8 * i - 1), 0, (MLKEM_Q - 1)))
{ // clang-format on
uint8_t t[8];
const int offset = i * 5;
Expand All @@ -105,7 +105,7 @@ void poly_decompress(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES]) {
for (int j = 0; j < 8; j++) // clang-format off
ASSIGNS(j, OBJECT_WHOLE(r))
INVARIANT(j >= 0 && j <= 8 && i >= 0 && i <= MLKEM_N / 8)
INVARIANT(ARRAY_IN_BOUNDS(0, (8 * i + j - 1), r->coeffs, 0, (MLKEM_Q - 1)))
INVARIANT(ARRAY_BOUND(r->coeffs, 0, (8 * i + j - 1), 0, (MLKEM_Q - 1)))
{ // clang-format on
// REF-CHANGE: Hoist scalar decompression into separate function
r->coeffs[8 * i + j] = scalar_decompress_d5(t[j]);
Expand Down Expand Up @@ -162,7 +162,7 @@ void poly_frombytes(poly *r, const uint8_t a[MLKEM_POLYBYTES]) {
for (i = 0; i < MLKEM_N / 2; i++) // clang-format off
ASSIGNS(i, OBJECT_WHOLE(r))
INVARIANT(i >= 0 && i <= MLKEM_N / 2)
INVARIANT(ARRAY_IN_BOUNDS(0, (2 * i - 1), r->coeffs, 0, 4095))
INVARIANT(ARRAY_BOUND(r->coeffs, 0, (2 * i - 1), 0, 4095))
{ // clang-format on
// REF-CHANGE: Introduce some locals for better readability
const uint8_t t0 = a[3 * i + 0];
Expand All @@ -189,12 +189,12 @@ void poly_frommsg(poly *r, const uint8_t msg[MLKEM_INDCPA_MSGBYTES]) {
for (int i = 0; i < MLKEM_N / 8; i++) // clang-format off
ASSIGNS(i, OBJECT_WHOLE(r))
INVARIANT(i >= 0 && i <= MLKEM_N / 8)
INVARIANT(ARRAY_IN_BOUNDS(0, (8 * i - 1), r->coeffs, 0, (MLKEM_Q - 1)))
INVARIANT(ARRAY_BOUND(r->coeffs, 0, (8 * i - 1), 0, (MLKEM_Q - 1)))
{ // clang-format on
for (int j = 0; j < 8; j++) // clang-format off
ASSIGNS(j, OBJECT_WHOLE(r))
INVARIANT(i >= 0 && i < MLKEM_N / 8 && j >= 0 && j <= 8)
INVARIANT(ARRAY_IN_BOUNDS(0, (8 * i + j - 1), r->coeffs, 0, (MLKEM_Q - 1)))
INVARIANT(ARRAY_BOUND(r->coeffs, 0, (8 * i + j - 1), 0, (MLKEM_Q - 1)))
{ // clang-format on
r->coeffs[8 * i + j] = 0;
cmov_int16(&r->coeffs[8 * i + j], HALF_Q, (msg[i] >> j) & 1);
Expand Down Expand Up @@ -299,7 +299,7 @@ void poly_basemul_montgomery_cached(poly *r, const poly *a, const poly *b,
for (i = 0; i < MLKEM_N / 4; i++) // clang-format off
ASSIGNS(i, OBJECT_WHOLE(r))
INVARIANT(i >= 0 && i <= MLKEM_N / 4)
INVARIANT(ARRAY_IN_BOUNDS(0, (4 * i - 1), r->coeffs, -(3 * HALF_Q - 1), (3 * HALF_Q - 1)))
INVARIANT(ARRAY_ABS_BOUND(r->coeffs, 0, (4 * i - 1), (3 * HALF_Q - 1)))
{ // clang-format on
basemul_cached(&r->coeffs[4 * i], &a->coeffs[4 * i], &b->coeffs[4 * i],
b_cache->coeffs[2 * i]);
Expand All @@ -315,7 +315,7 @@ void poly_tomont(poly *r) {
for (i = 0; i < MLKEM_N; i++) // clang-format off
ASSIGNS(i, OBJECT_WHOLE(r))
INVARIANT(i >= 0 && i <= MLKEM_N)
INVARIANT(ARRAY_IN_BOUNDS(0, (i - 1), r->coeffs, -(MLKEM_Q - 1), (MLKEM_Q - 1)))
INVARIANT(ARRAY_ABS_BOUND(r->coeffs ,0, (i - 1), (MLKEM_Q - 1)))
{ // clang-format on
r->coeffs[i] = fqmul(r->coeffs[i], f);
}
Expand All @@ -335,7 +335,7 @@ void poly_reduce(poly *r) {
for (i = 0; i < MLKEM_N; i++) // clang-format off
ASSIGNS(i, OBJECT_WHOLE(r))
INVARIANT(i >= 0 && i <= MLKEM_N)
INVARIANT(ARRAY_IN_BOUNDS(0, (i - 1), r->coeffs, 0, (MLKEM_Q - 1)))
INVARIANT(ARRAY_BOUND(r->coeffs, 0, (i - 1), 0, (MLKEM_Q - 1)))
{ // clang-format on
// Barrett reduction, giving signed canonical representative
int16_t t = barrett_reduce(r->coeffs[i]);
Expand Down
Loading