Skip to content

Commit

Permalink
CBMC: Switch to exclusive coefficient upper bounds
Browse files Browse the repository at this point in the history 
Previously, the coefficient bounds in `array_bound(...)` and
`array_abs_bound(...)` were inclusive. This was somewhat inconvenient
since (a) it required a lot of `-1` in places where the exclusive upper
bound was more natural to work woth, and (b) it was a deviation from the
runtime debug assertions `POLY_BOUND` which would use exclusive bounds.

This commit switches `array_bound` to use an exclusive upper bound.
The lower bound remains inclusive. For `array_abs_bound`, we switch
to an exclusive absolute bound.

The macro `UINT12_MAX` (mapping to 4095) is replaced by UINT12_LIMIT,
mapping to 4096. Uses of `array_abs_bound(..., UINT12_MAX) are replaced
by `array_bound(..., 0, UINT12_LIMIT)`, since we never deal with negative
numbers bound by UINT12_LIMIT.

Signed-off-by: Hanno Becker <[email protected]>
  • Loading branch information
@hanno-becker
hanno-becker committed Jan 11, 2025
1 parent 20e5b15 commit 8f80920
Show file tree
Hide file tree
Showing 14 changed files with 105 additions and 102 deletions.
8 changes: 4 additions & 4 deletions mlkem/cbd.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,7 @@ static void cbd2(poly *r, const uint8_t buf[2 * MLKEM_N / 4])
for (i = 0; i < MLKEM_N / 8; i++)
__loop__(
invariant(i >= 0 && i <= MLKEM_N / 8)
invariant(array_abs_bound(r->coeffs, 0, 8 * i, 2)))
invariant(array_abs_bound(r->coeffs, 0, 8 * i, 3)))
{
unsigned j;
uint32_t t = load32_littleendian(buf + 4 * i);
Expand All @@ -83,7 +83,7 @@ static void cbd2(poly *r, const uint8_t buf[2 * MLKEM_N / 4])
for (j = 0; j < 8; j++)
__loop__(
invariant(i >= 0 && i <= MLKEM_N / 8 && j >= 0 && j <= 8)
invariant(array_abs_bound(r->coeffs, 0, 8 * i + j, 2)))
invariant(array_abs_bound(r->coeffs, 0, 8 * i + j, 3)))
{
const int16_t a = (d >> (4 * j + 0)) & 0x3;
const int16_t b = (d >> (4 * j + 2)) & 0x3;
Expand All @@ -110,7 +110,7 @@ static void cbd3(poly *r, const uint8_t buf[3 * MLKEM_N / 4])
for (i = 0; i < MLKEM_N / 4; i++)
__loop__(
invariant(i >= 0 && i <= MLKEM_N / 4)
invariant(array_abs_bound(r->coeffs, 0, 4 * i, 3)))
invariant(array_abs_bound(r->coeffs, 0, 4 * i, 4)))
{
unsigned j;
const uint32_t t = load24_littleendian(buf + 3 * i);
Expand All @@ -121,7 +121,7 @@ static void cbd3(poly *r, const uint8_t buf[3 * MLKEM_N / 4])
for (j = 0; j < 4; j++)
__loop__(
invariant(i >= 0 && i <= MLKEM_N / 4 && j >= 0 && j <= 4)
invariant(array_abs_bound(r->coeffs, 0, 4 * i + j, 3)))
invariant(array_abs_bound(r->coeffs, 0, 4 * i + j, 4)))
{
const int16_t a = (d >> (6 * j + 0)) & 0x7;
const int16_t b = (d >> (6 * j + 3)) & 0x7;
Expand Down
21 changes: 12 additions & 9 deletions mlkem/cbmc.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -98,12 +98,12 @@

/*
* Boolean-value predidate that asserts that "all values of array_var are in
* range value_lb .. value_ub (inclusive)"
* range value_lb (inclusive) .. value_ub (exclusive)"
* Example:
* array_bound(a->coeffs, 0, MLKEM_N, -(MLKEM_Q - 1), MLKEM_Q - 1)
* array_bound(a->coeffs, 0, MLKEM_N, 0, MLKEM_Q)
* expands to
* __CPROVER_forall { int k; (0 <= k && k <= MLKEM_N-1) ==> ( (-(MLKEM_Q -
* 1) <= a->coeffs[k]) && (a->coeffs[k] <= (MLKEM_Q - 1))) }
* __CPROVER_forall { int k; (0 <= k && k <= MLKEM_N-1) ==> (
* 0 <= a->coeffs[k]) && a->coeffs[k] < MLKEM_Q)) }
*/

/*
Expand All @@ -120,17 +120,20 @@
unsigned qvar; \
((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> \
(((value_lb) <= (array_var[(qvar)])) && \
((array_var[(qvar)]) <= (value_ub))) \
((array_var[(qvar)]) < (value_ub))) \
}

#define array_bound(array_var, qvar_lb, qvar_ub, value_lb, value_ub) \
array_bound_core(CBMC_CONCAT(_cbmc_idx, __LINE__), (qvar_lb), \
(qvar_ub), (array_var), (value_lb), (value_ub))
/* clang-format on */


/* Wrapper around array_bound operating on absolute values */
/* Wrapper around array_bound operating on absolute values.
*
* Note that since the absolute bound is inclusive, but the lower
* bound in array_bound is inclusive, we have to raise it by 1.
*/
#define array_abs_bound(arr, lb, ub, k) \
array_bound((arr), (lb), (ub), (-(k)), (k))
/* clang-format on */
array_bound((arr), (lb), (ub), -(k) + 1, (k))

#endif
26 changes: 13 additions & 13 deletions mlkem/indcpa.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -163,10 +163,10 @@ __contract__(
requires(memory_no_alias(seed[2], MLKEM_SYMBYTES + 2))
requires(memory_no_alias(seed[3], MLKEM_SYMBYTES + 2))
assigns(memory_slice(vec, sizeof(poly) * 4))
ensures(array_bound(vec[0].coeffs, 0, MLKEM_N, 0, (MLKEM_Q - 1)))
ensures(array_bound(vec[1].coeffs, 0, MLKEM_N, 0, (MLKEM_Q - 1)))
ensures(array_bound(vec[2].coeffs, 0, MLKEM_N, 0, (MLKEM_Q - 1)))
ensures(array_bound(vec[3].coeffs, 0, MLKEM_N, 0, (MLKEM_Q - 1))))
ensures(array_bound(vec[0].coeffs, 0, MLKEM_N, 0, MLKEM_Q))
ensures(array_bound(vec[1].coeffs, 0, MLKEM_N, 0, MLKEM_Q))
ensures(array_bound(vec[2].coeffs, 0, MLKEM_N, 0, MLKEM_Q))
ensures(array_bound(vec[3].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
{
/* Temporary buffers for XOF output before rejection sampling */
uint8_t buf0[MLKEM_GEN_MATRIX_NBLOCKS * XOF_RATE];
Expand Down Expand Up @@ -207,10 +207,10 @@ __contract__(
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_bound(vec[0].coeffs, 0, ctr[0], 0, (MLKEM_Q - 1)))
invariant(ctr[1] > 0 ==> array_bound(vec[1].coeffs, 0, ctr[1], 0, (MLKEM_Q - 1)))
invariant(ctr[2] > 0 ==> array_bound(vec[2].coeffs, 0, ctr[2], 0, (MLKEM_Q - 1)))
invariant(ctr[3] > 0 ==> array_bound(vec[3].coeffs, 0, ctr[3], 0, (MLKEM_Q - 1))))
invariant(ctr[0] > 0 ==> array_bound(vec[0].coeffs, 0, ctr[0], 0, MLKEM_Q))
invariant(ctr[1] > 0 ==> array_bound(vec[1].coeffs, 0, ctr[1], 0, MLKEM_Q))
invariant(ctr[2] > 0 ==> array_bound(vec[2].coeffs, 0, ctr[2], 0, MLKEM_Q))
invariant(ctr[3] > 0 ==> array_bound(vec[3].coeffs, 0, ctr[3], 0, MLKEM_Q)))
{
xof_x4_squeezeblocks(buf0, buf1, buf2, buf3, 1, &statex);
ctr[0] = rej_uniform(vec[0].coeffs, MLKEM_N, ctr[0], buf0, buflen);
Expand All @@ -231,7 +231,7 @@ __contract__(
requires(memory_no_alias(entry, sizeof(poly)))
requires(memory_no_alias(seed, MLKEM_SYMBYTES + 2))
assigns(memory_slice(entry, sizeof(poly)))
ensures(array_bound(entry->coeffs, 0, MLKEM_N, 0, (MLKEM_Q - 1))))
ensures(array_bound(entry->coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
{
xof_ctx state;
uint8_t buf[MLKEM_GEN_MATRIX_NBLOCKS * XOF_RATE];
Expand All @@ -253,7 +253,7 @@ __contract__(
assigns(ctr, state, memory_slice(entry, sizeof(poly)), object_whole(buf))
invariant(0 <= ctr && ctr <= MLKEM_N)
invariant(ctr > 0 ==> array_bound(entry->coeffs, 0, ctr,
0, (MLKEM_Q - 1))))
0, MLKEM_Q)))
{
xof_squeezeblocks(buf, 1, &state);
ctr = rej_uniform(entry->coeffs, MLKEM_N, ctr, buf, buflen);
Expand All @@ -273,9 +273,9 @@ __contract__(
/* We don't specify that this should be a permutation, but only
* that it does not change the bound established at the end of gen_matrix. */
requires(memory_no_alias(data, sizeof(poly)))
requires(array_bound(data->coeffs, 0, MLKEM_N, 0, MLKEM_Q - 1))
requires(array_bound(data->coeffs, 0, MLKEM_N, 0, MLKEM_Q))
assigns(memory_slice(data, sizeof(poly)))
ensures(array_bound(data->coeffs, 0, MLKEM_N, 0, MLKEM_Q - 1))) { ((void)data); }
ensures(array_bound(data->coeffs, 0, MLKEM_N, 0, MLKEM_Q))) { ((void)data); }
#endif /* MLKEM_USE_NATIVE_NTT_CUSTOM_ORDER */

/* Not static for benchmarking */
Expand Down Expand Up @@ -392,7 +392,7 @@ __contract__(
requires(memory_no_alias(vc, sizeof(polyvec_mulcache)))
requires(forall(k0, 0, MLKEM_K,
forall(k1, 0, MLKEM_K,
array_abs_bound(a[k0].vec[k1].coeffs, 0, MLKEM_N, UINT12_MAX))))
array_bound(a[k0].vec[k1].coeffs, 0, MLKEM_N, 0, UINT12_LIMIT))))
assigns(object_whole(out)))
{
unsigned i;
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 @@ -31,7 +31,7 @@ __contract__(
requires(transposed == 0 || transposed == 1)
assigns(object_whole(a))
ensures(forall(x, 0, MLKEM_K, forall(y, 0, MLKEM_K,
array_bound(a[x].vec[y].coeffs, 0, MLKEM_N, 0, (MLKEM_Q - 1)))));
array_bound(a[x].vec[y].coeffs, 0, MLKEM_N, 0, MLKEM_Q))));
);

#define indcpa_keypair_derand MLKEM_NAMESPACE(indcpa_keypair_derand)
Expand Down
12 changes: 6 additions & 6 deletions mlkem/ntt.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -97,9 +97,9 @@ static void ntt_layer(int16_t r[MLKEM_N], int len, int layer)
__contract__(
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
requires(1 <= layer && layer <= 7 && len == (MLKEM_N >> layer))
requires(array_abs_bound(r, 0, MLKEM_N, layer * MLKEM_Q - 1))
requires(array_abs_bound(r, 0, MLKEM_N, layer * MLKEM_Q))
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
ensures(array_abs_bound(r, 0, MLKEM_N, (layer + 1) * MLKEM_Q - 1)))
ensures(array_abs_bound(r, 0, MLKEM_N, (layer + 1) * MLKEM_Q)))
{
int start, k;
/* `layer` is a ghost variable only needed in the CBMC specification */
Expand All @@ -110,11 +110,11 @@ __contract__(
__loop__(
invariant(0 <= start && start < MLKEM_N + 2 * len)
invariant(0 <= k && k <= MLKEM_N / 2 && 2 * len * k == start + MLKEM_N)
invariant(array_abs_bound(r, 0, start, (layer * MLKEM_Q - 1) + MLKEM_Q))
invariant(array_abs_bound(r, start, MLKEM_N, layer * MLKEM_Q - 1)))
invariant(array_abs_bound(r, 0, start, layer * MLKEM_Q + MLKEM_Q))
invariant(array_abs_bound(r, start, MLKEM_N, layer * MLKEM_Q)))
{
int16_t zeta = zetas[k++];
ntt_butterfly_block(r, zeta, start, len, layer * MLKEM_Q - 1);
ntt_butterfly_block(r, zeta, start, len, layer * MLKEM_Q);
}
}

Expand All @@ -138,7 +138,7 @@ void poly_ntt(poly *p)
for (len = 128, layer = 1; len >= 2; len >>= 1, layer++)
__loop__(
invariant(1 <= layer && layer <= 8 && len == (MLKEM_N >> layer))
invariant(array_abs_bound(r, 0, MLKEM_N, layer * MLKEM_Q - 1)))
invariant(array_abs_bound(r, 0, MLKEM_N, layer * MLKEM_Q)))
{
ntt_layer(r, len, layer);
}
Expand Down
10 changes: 5 additions & 5 deletions mlkem/ntt.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,9 +36,9 @@ MLKEM_NATIVE_INTERNAL_API
void poly_ntt(poly *r)
__contract__(
requires(memory_no_alias(r, sizeof(poly)))
requires(array_abs_bound(r->coeffs, 0, MLKEM_N, MLKEM_Q - 1))
requires(array_abs_bound(r->coeffs, 0, MLKEM_N, MLKEM_Q))
assigns(memory_slice(r, sizeof(poly)))
ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, NTT_BOUND - 1))
ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, NTT_BOUND))
);

#define poly_invntt_tomont MLKEM_NAMESPACE(poly_invntt_tomont)
Expand All @@ -63,7 +63,7 @@ void poly_invntt_tomont(poly *r)
__contract__(
requires(memory_no_alias(r, sizeof(poly)))
assigns(memory_slice(r, sizeof(poly)))
ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, INVNTT_BOUND - 1))
ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, INVNTT_BOUND))
);

#define basemul_cached MLKEM_NAMESPACE(basemul_cached)
Expand Down Expand Up @@ -94,9 +94,9 @@ __contract__(
requires(memory_no_alias(r, 2 * sizeof(int16_t)))
requires(memory_no_alias(a, 2 * sizeof(int16_t)))
requires(memory_no_alias(b, 2 * sizeof(int16_t)))
requires(array_abs_bound(a, 0, 2, UINT12_MAX))
requires(array_abs_bound(a, 0, 2, 0, UINT12_LIMIT))
assigns(memory_slice(r, 2 * sizeof(int16_t)))
ensures(array_abs_bound(r, 0, 2, 2 * MLKEM_Q - 1))
ensures(array_abs_bound(r, 0, 2, 2 * MLKEM_Q))
);


Expand Down
2 changes: 1 addition & 1 deletion mlkem/params.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@

#define MLKEM_N 256
#define MLKEM_Q 3329
#define UINT12_MAX 4095
#define UINT12_LIMIT 4096

#define MLKEM_SYMBYTES 32 /* size in bytes of hashes, and seeds */
#define MLKEM_SSBYTES 32 /* size in bytes of shared key */
Expand Down
30 changes: 15 additions & 15 deletions mlkem/poly.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -89,7 +89,7 @@ void poly_decompress_du(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_DU])
for (j = 0; j < MLKEM_N / 8; j++)
__loop__(
invariant(0 <= j && j <= MLKEM_N / 8)
invariant(array_bound(r->coeffs, 0, 8 * j, 0, (MLKEM_Q - 1))))
invariant(array_bound(r->coeffs, 0, 8 * j, 0, MLKEM_Q)))
{
int k;
uint16_t t[8];
Expand All @@ -108,7 +108,7 @@ void poly_decompress_du(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_DU])
for (k = 0; k < 8; k++)
__loop__(
invariant(0 <= k && k <= 8)
invariant(array_bound(r->coeffs, 0, 8 * j + k, 0, (MLKEM_Q - 1))))
invariant(array_bound(r->coeffs, 0, 8 * j + k, 0, MLKEM_Q)))
{
r->coeffs[8 * j + k] = scalar_decompress_d11(t[k]);
}
Expand All @@ -117,7 +117,7 @@ void poly_decompress_du(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_DU])
for (j = 0; j < MLKEM_N / 4; j++)
__loop__(
invariant(0 <= j && j <= MLKEM_N / 4)
invariant(array_bound(r->coeffs, 0, 4 * j, 0, (MLKEM_Q - 1))))
invariant(array_bound(r->coeffs, 0, 4 * j, 0, MLKEM_Q)))
{
int k;
uint16_t t[4];
Expand All @@ -131,7 +131,7 @@ void poly_decompress_du(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_DU])
for (k = 0; k < 4; k++)
__loop__(
invariant(0 <= k && k <= 4)
invariant(array_bound(r->coeffs, 0, 4 * j + k, 0, (MLKEM_Q - 1))))
invariant(array_bound(r->coeffs, 0, 4 * j + k, 0, MLKEM_Q)))
{
r->coeffs[4 * j + k] = scalar_decompress_d10(t[k]);
}
Expand All @@ -156,7 +156,7 @@ void poly_compress_dv(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_DV], const poly *a)
for (j = 0; j < 8; j++)
__loop__(
invariant(i >= 0 && i <= MLKEM_N / 8 && j >= 0 && j <= 8)
invariant(array_bound(t, 0, j, 0, 15)))
invariant(array_bound(t, 0, j, 0, 16)))
{
t[j] = scalar_compress_d4(a->coeffs[8 * i + j]);
}
Expand All @@ -175,7 +175,7 @@ void poly_compress_dv(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_DV], const poly *a)
for (j = 0; j < 8; j++)
__loop__(
invariant(i >= 0 && i <= MLKEM_N / 8 && j >= 0 && j <= 8)
invariant(array_bound(t, 0, j, 0, 31)))
invariant(array_bound(t, 0, j, 0, 32)))
{
t[j] = scalar_compress_d5(a->coeffs[8 * i + j]);
}
Expand Down Expand Up @@ -204,7 +204,7 @@ void poly_decompress_dv(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_DV])
for (i = 0; i < MLKEM_N / 2; i++)
__loop__(
invariant(i >= 0 && i <= MLKEM_N / 2)
invariant(array_bound(r->coeffs, 0, 2 * i, 0, (MLKEM_Q - 1))))
invariant(array_bound(r->coeffs, 0, 2 * i, 0, MLKEM_Q)))
{
r->coeffs[2 * i + 0] = scalar_decompress_d4((a[i] >> 0) & 0xF);
r->coeffs[2 * i + 1] = scalar_decompress_d4((a[i] >> 4) & 0xF);
Expand All @@ -213,7 +213,7 @@ void poly_decompress_dv(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_DV])
for (i = 0; i < MLKEM_N / 8; i++)
__loop__(
invariant(i >= 0 && i <= MLKEM_N / 8)
invariant(array_bound(r->coeffs, 0, 8 * i, 0, (MLKEM_Q - 1))))
invariant(array_bound(r->coeffs, 0, 8 * i, 0, MLKEM_Q)))
{
unsigned j;
uint8_t t[8];
Expand Down Expand Up @@ -241,7 +241,7 @@ void poly_decompress_dv(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_DV])
for (j = 0; j < 8; j++)
__loop__(
invariant(j >= 0 && j <= 8 && i >= 0 && i <= MLKEM_N / 8)
invariant(array_bound(r->coeffs, 0, 8 * i + j, 0, (MLKEM_Q - 1))))
invariant(array_bound(r->coeffs, 0, 8 * i + j, 0, MLKEM_Q)))
{
r->coeffs[8 * i + j] = scalar_decompress_d5(t[j]);
}
Expand Down Expand Up @@ -303,7 +303,7 @@ void poly_frombytes(poly *r, const uint8_t a[MLKEM_POLYBYTES])
for (i = 0; i < MLKEM_N / 2; i++)
__loop__(
invariant(i >= 0 && i <= MLKEM_N / 2)
invariant(array_bound(r->coeffs, 0, 2 * i, 0, UINT12_MAX)))
invariant(array_bound(r->coeffs, 0, 2 * i, 0, UINT12_LIMIT)))
{
const uint8_t t0 = a[3 * i + 0];
const uint8_t t1 = a[3 * i + 1];
Expand Down Expand Up @@ -334,13 +334,13 @@ void poly_frommsg(poly *r, const uint8_t msg[MLKEM_INDCPA_MSGBYTES])
for (i = 0; i < MLKEM_N / 8; i++)
__loop__(
invariant(i >= 0 && i <= MLKEM_N / 8)
invariant(array_bound(r->coeffs, 0, 8 * i, 0, (MLKEM_Q - 1))))
invariant(array_bound(r->coeffs, 0, 8 * i, 0, MLKEM_Q)))
{
unsigned j;
for (j = 0; j < 8; j++)
__loop__(
invariant(i >= 0 && i < MLKEM_N / 8 && j >= 0 && j <= 8)
invariant(array_bound(r->coeffs, 0, 8 * i + j, 0, (MLKEM_Q - 1))))
invariant(array_bound(r->coeffs, 0, 8 * i + j, 0, MLKEM_Q)))
{
/* Prevent the compiler from recognizing this as a bit selection */
uint8_t mask = value_barrier_u8(1u << j);
Expand Down Expand Up @@ -469,7 +469,7 @@ void poly_basemul_montgomery_cached(poly *r, const poly *a, const poly *b,
__loop__(
assigns(i, object_whole(r))
invariant(i >= 0 && i <= MLKEM_N / 4)
invariant(array_abs_bound(r->coeffs, 0, 4 * i, 2 * MLKEM_Q - 1)))
invariant(array_abs_bound(r->coeffs, 0, 4 * i, 2 * MLKEM_Q)))
{
basemul_cached(&r->coeffs[4 * i], &a->coeffs[4 * i], &b->coeffs[4 * i],
b_cache->coeffs[2 * i]);
Expand All @@ -487,7 +487,7 @@ void poly_tomont(poly *r)
for (i = 0; i < MLKEM_N; i++)
__loop__(
invariant(i >= 0 && i <= MLKEM_N)
invariant(array_abs_bound(r->coeffs ,0, i, (MLKEM_Q - 1))))
invariant(array_abs_bound(r->coeffs ,0, i, MLKEM_Q)))
{
r->coeffs[i] = fqmul(r->coeffs[i], f);
}
Expand All @@ -511,7 +511,7 @@ void poly_reduce(poly *r)
for (i = 0; i < MLKEM_N; i++)
__loop__(
invariant(i >= 0 && i <= MLKEM_N)
invariant(array_bound(r->coeffs, 0, i, 0, (MLKEM_Q - 1))))
invariant(array_bound(r->coeffs, 0, i, 0, MLKEM_Q)))
{
/* Barrett reduction, giving signed canonical representative */
int16_t t = barrett_reduce(r->coeffs[i]);
Expand Down
Loading

0 comments on commit 8f80920

Please sign in to comment.