Skip to content

CBMC: Refine bounds for input and output of base multiplication #906

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

Draft
wants to merge 9 commits into
base: main
Choose a base branch
from
Draft

CBMC: Refine bounds for input and output of base multiplication #906

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
b539fc3
Switch mlk_polyvec and mlk_polymat to struct wrappers
hanno-becker Jul 9, 2025
12e886a
CBMC: Refine bounds for input and output of base multiplication
hanno-becker Mar 24, 2025
6b1f693
Use --arrays-uf-always here to improve proof speed.
rod-chapman Jun 9, 2025
8e8cff4
Fix merge conflicts and complete rebase again main branch.
rod-chapman Oct 7, 2025
ebb480d
Use C90 comments /* */ not C99 // style.
rod-chapman Oct 7, 2025
5a5d566
Update component testing code for new type signatures.
rod-chapman Oct 7, 2025
62a3bb6
Re-generate auto-generated files to meet lint requirements.
rod-chapman Oct 7, 2025
6d54ddb
Update post-condition on native implementions of
rod-chapman Oct 7, 2025
65200d7
Update master copies of AArch64 arithmetic back-end specs.
rod-chapman Oct 7, 2025
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
12 changes: 12 additions & 0 deletions dev/aarch64_clean/src/arith_native_aarch64.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -116,13 +116,17 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k2(
/* This must be kept in sync with the HOL-Light specification in
* proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml.
*/
/* TODO - refine_bounds branch - Check HOL-Light specification has the
* INT16_MAX/2 bound on post-condition and re-prove/
*/
__contract__(
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
requires(memory_no_alias(a, sizeof(int16_t) * 2 * MLKEM_N))
requires(memory_no_alias(b, sizeof(int16_t) * 2 * MLKEM_N))
requires(memory_no_alias(b_cache, sizeof(int16_t) * 2 * (MLKEM_N / 2)))
requires(array_abs_bound(a, 0, 2 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
);

#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k3 \
Expand All @@ -133,13 +137,17 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k3(
/* This must be kept in sync with the HOL-Light specification in
* proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml.
*/
/* TODO - refine_bounds branch - Check HOL-Light specification has the
* INT16_MAX/2 bound on post-condition and re-prove/
*/
__contract__(
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
requires(memory_no_alias(a, sizeof(int16_t) * 3 * MLKEM_N))
requires(memory_no_alias(b, sizeof(int16_t) * 3 * MLKEM_N))
requires(memory_no_alias(b_cache, sizeof(int16_t) * 3 * (MLKEM_N / 2)))
requires(array_abs_bound(a, 0, 3 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
);

#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k4 \
Expand All @@ -150,13 +158,17 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k4(
/* This must be kept in sync with the HOL-Light specification in
* proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml.
*/
/* TODO - refine_bounds branch - Check HOL-Light specification has the
* INT16_MAX/2 bound on post-condition and re-prove/
*/
__contract__(
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
requires(memory_no_alias(a, sizeof(int16_t) * 4 * MLKEM_N))
requires(memory_no_alias(b, sizeof(int16_t) * 4 * MLKEM_N))
requires(memory_no_alias(b_cache, sizeof(int16_t) * 4 * (MLKEM_N / 2)))
requires(array_abs_bound(a, 0, 4 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
);

#define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm)
Expand Down
12 changes: 12 additions & 0 deletions dev/aarch64_opt/src/arith_native_aarch64.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -116,13 +116,17 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k2(
/* This must be kept in sync with the HOL-Light specification in
* proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml.
*/
/* TODO - refine_bounds branch - Check HOL-Light specification has the
* INT16_MAX/2 bound on post-condition and re-prove/
*/
__contract__(
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
requires(memory_no_alias(a, sizeof(int16_t) * 2 * MLKEM_N))
requires(memory_no_alias(b, sizeof(int16_t) * 2 * MLKEM_N))
requires(memory_no_alias(b_cache, sizeof(int16_t) * 2 * (MLKEM_N / 2)))
requires(array_abs_bound(a, 0, 2 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
);

#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k3 \
Expand All @@ -133,13 +137,17 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k3(
/* This must be kept in sync with the HOL-Light specification in
* proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml.
*/
/* TODO - refine_bounds branch - Check HOL-Light specification has the
* INT16_MAX/2 bound on post-condition and re-prove/
*/
__contract__(
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
requires(memory_no_alias(a, sizeof(int16_t) * 3 * MLKEM_N))
requires(memory_no_alias(b, sizeof(int16_t) * 3 * MLKEM_N))
requires(memory_no_alias(b_cache, sizeof(int16_t) * 3 * (MLKEM_N / 2)))
requires(array_abs_bound(a, 0, 3 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
);

#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k4 \
Expand All @@ -150,13 +158,17 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k4(
/* This must be kept in sync with the HOL-Light specification in
* proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml.
*/
/* TODO - refine_bounds branch - Check HOL-Light specification has the
* INT16_MAX/2 bound on post-condition and re-prove/
*/
__contract__(
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
requires(memory_no_alias(a, sizeof(int16_t) * 4 * MLKEM_N))
requires(memory_no_alias(b, sizeof(int16_t) * 4 * MLKEM_N))
requires(memory_no_alias(b_cache, sizeof(int16_t) * 4 * (MLKEM_N / 2)))
requires(array_abs_bound(a, 0, 4 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
);

#define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm)
Expand Down
50 changes: 38 additions & 12 deletions mlkem/src/indcpa.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -289,9 +289,11 @@ void mlk_gen_matrix(mlk_polymat a, const uint8_t seed[MLKEM_SYMBYTES],
* - mlk_polymat a: Input matrix. Must be in NTT domain
* and have coefficients of absolute value < 4096.
* - mlk_polyvec v: Input polynomial vector. Must be in NTT
* domain.
* domain and have coefficients of absolute value
* < MLK_NTT_BOUND.
* - mlk_polyvec vc: Mulcache for v, computed via
* mlk_polyvec_mulcache_compute().
* mlk_polyvec_mulcache_compute(). Must have coefficients
* of absolute value < MLKEM_Q.
*
* Specification: Implements @[FIPS203, Section 2.4.7, Eq (2.12), (2.13)]
*
Expand All @@ -304,17 +306,41 @@ __contract__(
requires(memory_no_alias(v, sizeof(mlk_polyvec)))
requires(memory_no_alias(vc, sizeof(mlk_polyvec_mulcache)))
requires(forall(k0, 0, MLKEM_K * MLKEM_K,
array_bound(a[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
assigns(object_whole(out)))
array_bound(a[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
requires(forall(k1, 0, MLKEM_K,
array_abs_bound(v[k1].coeffs, 0, MLKEM_N, MLK_NTT_BOUND)))
requires(forall(k2, 0, MLKEM_K,
array_abs_bound(vc[k2].coeffs, 0, MLKEM_N/2, MLKEM_Q)))
assigns(object_whole(out))
ensures(forall(k3, 0, MLKEM_K,
array_abs_bound(out[k3].coeffs, 0, MLKEM_N, INT16_MAX/2))))
{
unsigned i;
for (i = 0; i < MLKEM_K; i++)
__loop__(
assigns(i, object_whole(out))
invariant(i <= MLKEM_K))
{
mlk_polyvec_basemul_acc_montgomery_cached(&out[i], &a[MLKEM_K * i], v, vc);
}
/* Temporary on the "refine-bounds" branch - unroll to a simple
* sequence of calls for each possible value of MLKEM_K to
* simplify proof.
*/
mlk_polyvec_basemul_acc_montgomery_cached(&out[0], &a[0], v, vc);
mlk_polyvec_basemul_acc_montgomery_cached(&out[1], &a[MLKEM_K], v, vc);

#if MLKEM_K == 3
mlk_polyvec_basemul_acc_montgomery_cached(&out[2], &a[MLKEM_K * 2], v, vc);
#elif MLKEM_K == 4
mlk_polyvec_basemul_acc_montgomery_cached(&out[2], &a[MLKEM_K * 2], v, vc);
mlk_polyvec_basemul_acc_montgomery_cached(&out[3], &a[MLKEM_K * 3], v, vc);
#endif

/* unsigned i;
* for (i = 0; i < MLKEM_K; i++)
* __loop__(
* assigns(i, object_whole(out))
* invariant(i <= MLKEM_K)
* invariant(forall(k, 0, i,
* array_abs_bound(out[k].coeffs, 0, MLKEM_N, INT16_MAX/2))))
* {
* mlk_polyvec_basemul_acc_montgomery_cached(&out[i], &a[MLKEM_K * i], v,
* vc);
* }
*/
}

/* Reference: `indcpa_keypair_derand()` in the reference implementation @[REF].
Expand Down
12 changes: 12 additions & 0 deletions mlkem/src/native/aarch64/src/arith_native_aarch64.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -116,13 +116,17 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k2(
/* This must be kept in sync with the HOL-Light specification in
* proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml.
*/
/* TODO - refine_bounds branch - Check HOL-Light specification has the
* INT16_MAX/2 bound on post-condition and re-prove/
*/
__contract__(
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
requires(memory_no_alias(a, sizeof(int16_t) * 2 * MLKEM_N))
requires(memory_no_alias(b, sizeof(int16_t) * 2 * MLKEM_N))
requires(memory_no_alias(b_cache, sizeof(int16_t) * 2 * (MLKEM_N / 2)))
requires(array_abs_bound(a, 0, 2 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
);

#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k3 \
Expand All @@ -133,13 +137,17 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k3(
/* This must be kept in sync with the HOL-Light specification in
* proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml.
*/
/* TODO - refine_bounds branch - Check HOL-Light specification has the
* INT16_MAX/2 bound on post-condition and re-prove/
*/
__contract__(
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
requires(memory_no_alias(a, sizeof(int16_t) * 3 * MLKEM_N))
requires(memory_no_alias(b, sizeof(int16_t) * 3 * MLKEM_N))
requires(memory_no_alias(b_cache, sizeof(int16_t) * 3 * (MLKEM_N / 2)))
requires(array_abs_bound(a, 0, 3 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
);

#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k4 \
Expand All @@ -150,13 +158,17 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k4(
/* This must be kept in sync with the HOL-Light specification in
* proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml.
*/
/* TODO - refine_bounds branch - Check HOL-Light specification has the
* INT16_MAX/2 bound on post-condition and re-prove/
*/
__contract__(
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
requires(memory_no_alias(a, sizeof(int16_t) * 4 * MLKEM_N))
requires(memory_no_alias(b, sizeof(int16_t) * 4 * MLKEM_N))
requires(memory_no_alias(b_cache, sizeof(int16_t) * 4 * (MLKEM_N / 2)))
requires(array_abs_bound(a, 0, 4 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
);

#define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm)
Expand Down
4 changes: 4 additions & 0 deletions mlkem/src/native/api.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -155,6 +155,7 @@ __contract__(
static MLK_INLINE int mlk_intt_native(int16_t p[MLKEM_N])
__contract__(
requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
requires(array_abs_bound(p, 0, MLKEM_N, INT16_MAX/2))
assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N))
ensures(return_value == MLK_NATIVE_FUNC_FALLBACK || return_value == MLK_NATIVE_FUNC_SUCCESS)
ensures((return_value == MLK_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(p, 0, MLKEM_N, MLK_INVNTT_BOUND))
Expand Down Expand Up @@ -264,6 +265,7 @@ __contract__(
requires(array_bound(a, 0, 2 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
ensures(return_value == MLK_NATIVE_FUNC_FALLBACK || return_value == MLK_NATIVE_FUNC_SUCCESS)
ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
);
#endif /* MLK_CONFIG_MULTILEVEL_WITH_SHARED || MLKEM_K == 2 */

Expand Down Expand Up @@ -298,6 +300,7 @@ __contract__(
requires(array_bound(a, 0, 3 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
ensures(return_value == MLK_NATIVE_FUNC_FALLBACK || return_value == MLK_NATIVE_FUNC_SUCCESS)
ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
);
#endif /* MLK_CONFIG_MULTILEVEL_WITH_SHARED || MLKEM_K == 3 */

Expand Down Expand Up @@ -332,6 +335,7 @@ __contract__(
requires(array_bound(a, 0, 4 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
ensures(return_value == MLK_NATIVE_FUNC_FALLBACK || return_value == MLK_NATIVE_FUNC_SUCCESS)
ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
);
#endif /* MLK_CONFIG_MULTILEVEL_WITH_SHARED || MLKEM_K == 4 */
#endif /* MLK_USE_NATIVE_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED */
Expand Down
1 change: 1 addition & 0 deletions mlkem/src/poly.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -273,6 +273,7 @@ __contract__(
requires(memory_no_alias(x, sizeof(mlk_poly_mulcache)))
requires(memory_no_alias(a, sizeof(mlk_poly)))
assigns(object_whole(x))
ensures(array_abs_bound(x->coeffs, 0, MLKEM_N/2, MLKEM_Q))
)
{
unsigned i;
Expand Down
27 changes: 13 additions & 14 deletions mlkem/src/poly.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -89,14 +89,16 @@ static MLK_ALWAYS_INLINE int16_t mlk_cast_uint16_to_int16(uint16_t x)
**************************************************/
static MLK_ALWAYS_INLINE int16_t mlk_montgomery_reduce(int32_t a)
__contract__(
requires(a < +(INT32_MAX - (((int32_t)1 << 15) * MLKEM_Q)) &&
a > -(INT32_MAX - (((int32_t)1 << 15) * MLKEM_Q)))
/* We don't attempt to express an input-dependent output bound
* as the post-condition here. There are two call-sites for this
* function:
* - The base multiplication: Here, we need no output bound.
* - mlk_fqmul: Here, we inline this function and prove another spec
* for mlk_fqmul which does have a post-condition bound. */
/* This specification is only relevant for Montgomery reduction
* during base multiplication, and the input bound is tailored to that.
* The output bound, albeit weak, allows one addition/subtraction prior
* to risk of overflow; this can be useful for the inverse NTT, for example.
*
* For the use of montgomery_reduce in fqmul, we inline this
* function instead of calling it by contract. */
requires(a <= +(4 * 2 * MLKEM_UINT12_LIMIT * MLK_NTT_BOUND) &&
a >= -(4 * 2 * MLKEM_UINT12_LIMIT * MLK_NTT_BOUND))
ensures(return_value < (INT16_MAX / 2) && return_value > -(INT16_MAX / 2))
)
{
/* check-magic: 62209 == unsigned_mod(pow(MLKEM_Q, -1, 2^16), 2^16) */
Expand Down Expand Up @@ -177,17 +179,13 @@ __contract__(
* - Caches `b_1 * \gamma` in @[FIPS203, Algorithm 12, BaseCaseMultiply, L1]
*
************************************************************/
/*
* NOTE: The default C implementation of this function populates
* the mulcache with values in (-q,q), but this is not needed for the
* higher level safety proofs, and thus not part of the spec.
*/
MLK_INTERNAL_API
void mlk_poly_mulcache_compute(mlk_poly_mulcache *x, const mlk_poly *a)
__contract__(
requires(memory_no_alias(x, sizeof(mlk_poly_mulcache)))
requires(memory_no_alias(a, sizeof(mlk_poly)))
assigns(object_whole(x))
assigns(memory_slice(x, sizeof(mlk_poly_mulcache)))
ensures(array_abs_bound(x->coeffs, 0, MLKEM_N/2, MLKEM_Q))
);

#define mlk_poly_reduce MLK_NAMESPACE(poly_reduce)
Expand Down Expand Up @@ -339,6 +337,7 @@ MLK_INTERNAL_API
void mlk_poly_invntt_tomont(mlk_poly *r)
__contract__(
requires(memory_no_alias(r, sizeof(mlk_poly)))
requires(array_abs_bound(r->coeffs, 0, MLKEM_N, INT16_MAX/2))
assigns(memory_slice(r, sizeof(mlk_poly)))
ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, MLK_INVNTT_BOUND))
);
Expand Down
19 changes: 13 additions & 6 deletions mlkem/src/poly_k.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -158,24 +158,31 @@ __contract__(
requires(memory_no_alias(b_cache, sizeof(mlk_polyvec_mulcache)))
requires(forall(k1, 0, MLKEM_K,
array_bound(a[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
requires(forall(k2, 0, MLKEM_K,
array_abs_bound(b[k2].coeffs, 0, MLKEM_N, MLK_NTT_BOUND)))
requires(forall(k3, 0, MLKEM_K,
array_abs_bound(b_cache[k3].coeffs, 0, MLKEM_N/2, MLKEM_Q)))
assigns(object_whole(r))
ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, INT16_MAX/2))
)
{
unsigned i;
mlk_assert_bound_2d(a, MLKEM_K, MLKEM_N, 0, MLKEM_UINT12_LIMIT);

mlk_assert_abs_bound_2d(b, MLKEM_K, MLKEM_N, MLK_NTT_BOUND);
mlk_assert_abs_bound_2d(b_cache, MLKEM_K, MLKEM_N / 2, MLKEM_Q);

for (i = 0; i < MLKEM_N / 2; i++)
__loop__(invariant(i <= MLKEM_N / 2))
__loop__(
invariant(i <= MLKEM_N / 2)
invariant(array_abs_bound(r->coeffs, 0, 2 * i, INT16_MAX/2)))
{
unsigned k;
int32_t t[2] = {0};
for (k = 0; k < MLKEM_K; k++)
__loop__(
invariant(k <= MLKEM_K &&
t[0] <= (int32_t) k * 2 * MLKEM_UINT12_LIMIT * 32768 &&
t[0] >= - ((int32_t) k * 2 * MLKEM_UINT12_LIMIT * 32768) &&
t[1] <= ((int32_t) k * 2 * MLKEM_UINT12_LIMIT * 32768) &&
t[1] >= - ((int32_t) k * 2 * MLKEM_UINT12_LIMIT * 32768)))
invariant(k <= MLKEM_K && i <= MLKEM_N / 2)
invariant(array_abs_bound(t, 0, 2, k * 2 * MLKEM_UINT12_LIMIT * MLK_NTT_BOUND + 1)))
{
t[0] += (int32_t)a[k].coeffs[2 * i + 1] * b_cache[k].coeffs[i];
t[0] += (int32_t)a[k].coeffs[2 * i] * b[k].coeffs[2 * i];
Expand Down
Loading
Loading