Skip to content

Commit

Permalink
CBMC: Remove index variable from ARRAY_IN_BOUNDS
Browse files Browse the repository at this point in the history 
The helper macro ARRAY_IN_BOUNDS unfolds to a CBMC annotation
asserting that the coefficients of an array are within specified
bounds.

Previously, this macro would require the caller to explicitly state
the type and name of the index variable, even though this would not
actually feature anywhere else in the macro. The original reason for
this was that CBMC does not like the same variable name be used twice
in block of annotations (precondition, postcondition, loop invariants).

This commit simplifies ARRAY_IN_BOUNDS by always picking `int` as the
index type, and auto-generating the variable name. Name clashes are
avoided by internally appending the line number to the index variable.

Signed-off-by: Hanno Becker <[email protected]>
  • Loading branch information
@hanno-becker
hanno-becker committed Nov 12, 2024
1 parent 326d0b2 commit 6925a9d
Show file tree
Hide file tree
Showing 12 changed files with 97 additions and 88 deletions.
8 changes: 4 additions & 4 deletions mlkem/cbd.c
View file
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(int, k, 0, (8 * i - 1), r->coeffs, -2, +2)) // clang-format on
INVARIANT(ARRAY_IN_BOUNDS(0, (8 * i - 1), r->coeffs, -2, +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(int, k, 0, 8 * i + j - 1, r->coeffs, -2, +2)) // clang-format on
INVARIANT(ARRAY_IN_BOUNDS(0, 8 * i + j - 1, r->coeffs, -2, +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(int, k, 0, (4 * i - 1), r->coeffs, -3, +3)) // clang-format on
INVARIANT(ARRAY_IN_BOUNDS(0, (4 * i - 1), r->coeffs, -3, +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(int, k, 0, 4 * i + j - 1, r->coeffs, -3, +3)) // clang-format on
INVARIANT(ARRAY_IN_BOUNDS(0, 4 * i + j - 1, r->coeffs, -3, +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
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(int, k, 0, MLKEM_N - 1, r->coeffs, -MLKEM_ETA1, MLKEM_ETA1));
ENSURES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r->coeffs, -MLKEM_ETA1, 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(int, k, 0, MLKEM_N - 1, r->coeffs, -MLKEM_ETA2, MLKEM_ETA2));
ENSURES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r->coeffs, -MLKEM_ETA2, MLKEM_ETA2));
// clang-format on

#endif
17 changes: 13 additions & 4 deletions mlkem/cbmc.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -107,15 +107,18 @@
// range value_lb .. value_ub (inclusive)"
//
// Example:
// ARRAY_IN_BOUNDS(unsigned, k, 0, MLKEM_N-1, a->coeffs, -(MLKEM_Q - 1),
// MLKEM_Q - 1)
// ARRAY_IN_BOUNDS(0, MLKEM_N-1, a->coeffs, -(MLKEM_Q - 1), MLKEM_Q - 1)
// expands to
// __CPROVER_forall { unsigned k; (0 <= k && k <= MLKEM_N-1) ==> ( (-(MLKEM_Q -
// __CPROVER_forall { int k; (0 <= k && k <= MLKEM_N-1) ==> ( (-(MLKEM_Q -
// 1) <= a->coeffs[k]) && (a->coeffs[k] <= (MLKEM_Q - 1))) }

// Prevent clang-format from corrupting CBMC's special ==> operator
// clang-format off
#define ARRAY_IN_BOUNDS(indextype, qvar, qvar_lb, qvar_ub, array_var, \

#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, \
value_lb, value_ub) \
__CPROVER_forall \
{ \
Expand All @@ -124,6 +127,12 @@
(((value_lb) <= (array_var[(qvar)])) && \
((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__), \
(qvar_lb), (qvar_ub), (array_var), (value_lb), (value_ub))

// clang-format on

#endif
32 changes: 16 additions & 16 deletions mlkem/indcpa.c
View file
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(int, k1, 0, MLKEM_N - 1, pk->vec[k0].coeffs, 0, (MLKEM_Q - 1))))
ARRAY_IN_BOUNDS(0, MLKEM_N - 1, pk->vec[k0].coeffs, 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(int, k1, 0, MLKEM_N - 1, pk->vec[k0].coeffs, 0, (MLKEM_Q - 1))))
ARRAY_IN_BOUNDS(0, MLKEM_N - 1, pk->vec[k0].coeffs, 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(int, k1, 0, MLKEM_N - 1, sk->vec[k0].coeffs, 0, (MLKEM_Q - 1))))
ARRAY_IN_BOUNDS(0, MLKEM_N - 1, sk->vec[k0].coeffs, 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(int, k1, 0, MLKEM_N - 1, sk->vec[k0].coeffs, 0, (MLKEM_Q - 1))))
ARRAY_IN_BOUNDS(0, MLKEM_N - 1, sk->vec[k0].coeffs, 0, (MLKEM_Q - 1))))
ASSIGNS(OBJECT_WHOLE(sk)) // clang-format on
{
polyvec_frombytes(sk, packedsk);
Expand Down Expand Up @@ -173,10 +173,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(int, k0, 0, MLKEM_N - 1, vec[0].coeffs, 0, (MLKEM_Q - 1)))
ENSURES(ARRAY_IN_BOUNDS(int, k1, 0, MLKEM_N - 1, vec[1].coeffs, 0, (MLKEM_Q - 1)))
ENSURES(ARRAY_IN_BOUNDS(int, k2, 0, MLKEM_N - 1, vec[2].coeffs, 0, (MLKEM_Q - 1)))
ENSURES(ARRAY_IN_BOUNDS(int, k3, 0, MLKEM_N - 1, vec[3].coeffs, 0, (MLKEM_Q - 1)))
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)))
// clang-format on
{
// Temporary buffers for XOF output before rejection sampling
Expand Down Expand Up @@ -212,10 +212,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(int, k0, 0, ctr[0] - 1, vec[0].coeffs, 0, (MLKEM_Q - 1)))
INVARIANT(ctr[1] > 0 ==> ARRAY_IN_BOUNDS(int, k1, 0, ctr[1] - 1, vec[1].coeffs, 0, (MLKEM_Q - 1)))
INVARIANT(ctr[2] > 0 ==> ARRAY_IN_BOUNDS(int, k2, 0, ctr[2] - 1, vec[2].coeffs, 0, (MLKEM_Q - 1)))
INVARIANT(ctr[3] > 0 ==> ARRAY_IN_BOUNDS(int, k3, 0, ctr[3] - 1, vec[3].coeffs, 0, (MLKEM_Q - 1)))
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)))
// clang-format on
{
shake128x4_squeezeblocks(buf0, buf1, buf2, buf3, 1, &statex);
Expand All @@ -236,7 +236,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(int, k, 0, MLKEM_N - 1, entry->coeffs, 0, (MLKEM_Q - 1)))
ENSURES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, entry->coeffs, 0, (MLKEM_Q - 1)))
{ // clang-format on
shake128ctx state;
uint8_t buf[GEN_MATRIX_NBLOCKS * SHAKE128_RATE];
Expand All @@ -255,7 +255,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(int, k, 0, ctr - 1, entry->coeffs,
INVARIANT(ctr > 0 ==> ARRAY_IN_BOUNDS(0, ctr - 1, entry->coeffs,
0, (MLKEM_Q - 1))) // clang-format on
{
shake128_squeezeblocks(buf, 1, &state);
Expand Down Expand Up @@ -366,14 +366,14 @@ void gen_matrix(polyvec *a, const uint8_t seed[MLKEM_SYMBYTES],
**************************************************/
STATIC_TESTABLE
void matvec_mul(polyvec *out, const polyvec a[MLKEM_K], const polyvec *v,
const polyvec_mulcache *vc) // clang-format off
const polyvec_mulcache *vc) // clang-format off
REQUIRES(IS_FRESH(out, sizeof(polyvec)))
REQUIRES(IS_FRESH(a, sizeof(polyvec) * MLKEM_K))
REQUIRES(IS_FRESH(v, sizeof(polyvec)))
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(int, k2, 0, MLKEM_N - 1,
ARRAY_IN_BOUNDS(0, MLKEM_N - 1,
a[k0].vec[k1].coeffs, -(MLKEM_Q - 1), (MLKEM_Q - 1)))))
ASSIGNS(OBJECT_WHOLE(out))
// clang-format on
Expand Down
2 changes: 1 addition & 1 deletion mlkem/indcpa.h
View file
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(int, i, 0, MLKEM_N - 1, a[x].vec[y].coeffs, 0, (MLKEM_Q - 1)))));
ARRAY_IN_BOUNDS(0, MLKEM_N - 1, a[x].vec[y].coeffs, 0, (MLKEM_Q - 1)))));
// clang-format on

#define indcpa_keypair_derand MLKEM_NAMESPACE(indcpa_keypair_derand)
Expand Down
4 changes: 2 additions & 2 deletions mlkem/ntt.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,9 +43,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(int, k, 0, 1, a, -(MLKEM_Q - 1), (MLKEM_Q - 1)))
REQUIRES(ARRAY_IN_BOUNDS(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)));
ENSURES(ARRAY_IN_BOUNDS(0, 1, r, -(3 * HALF_Q - 1), (3 * HALF_Q - 1)));
// clang-format on


Expand Down
24 changes: 12 additions & 12 deletions mlkem/poly.c
View file
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(int, k2, 0, (j-1), t, 0, 15))
INVARIANT(ARRAY_IN_BOUNDS(0, (j-1), t, 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(int, k2, 0, (j-1), t, 0, 31))
INVARIANT(ARRAY_IN_BOUNDS(0, (j-1), t, 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(int, k, 0, (2 * i - 1), r->coeffs, 0, (MLKEM_Q - 1)))
INVARIANT(ARRAY_IN_BOUNDS(0, (2 * i - 1), r->coeffs, 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(int, k, 0, (8 * i - 1), r->coeffs, 0, (MLKEM_Q - 1)))
INVARIANT(ARRAY_IN_BOUNDS(0, (8 * i - 1), r->coeffs, 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(int, k, 0, (8 * i + j - 1), r->coeffs, 0, (MLKEM_Q - 1)))
INVARIANT(ARRAY_IN_BOUNDS(0, (8 * i + j - 1), r->coeffs, 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(int, k, 0, (2 * i - 1), r->coeffs, 0, 4095))
INVARIANT(ARRAY_IN_BOUNDS(0, (2 * i - 1), r->coeffs, 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(int, k, 0, (8 * i - 1), r->coeffs, 0, (MLKEM_Q - 1)))
{ // clang-format on
INVARIANT(ARRAY_IN_BOUNDS(0, (8 * i - 1), r->coeffs, 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(int, k, 0, (8 * i + j - 1), r->coeffs, 0, (MLKEM_Q - 1)))
INVARIANT(ARRAY_IN_BOUNDS(0, (8 * i + j - 1), r->coeffs, 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(int, k, 0, (4 * i - 1), r->coeffs, -(3 * HALF_Q - 1), (3 * HALF_Q - 1)))
INVARIANT(ARRAY_IN_BOUNDS(0, (4 * i - 1), r->coeffs, -(3 * HALF_Q - 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(int, k, 0, (i - 1), r->coeffs, -(MLKEM_Q - 1), (MLKEM_Q - 1)))
INVARIANT(ARRAY_IN_BOUNDS(0, (i - 1), r->coeffs, -(MLKEM_Q - 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(int, k, 0, (i - 1), r->coeffs, 0, (MLKEM_Q - 1)))
INVARIANT(ARRAY_IN_BOUNDS(0, (i - 1), r->coeffs, 0, (MLKEM_Q - 1)))
{ // clang-format on
// Barrett reduction, giving signed canonical representative
int16_t t = barrett_reduce(r->coeffs[i]);
Expand Down
Loading

0 comments on commit 6925a9d

Please sign in to comment.