Skip to content

CBMC: Add and prove x86_64 backend contracts #1393

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

Open
willieyz wants to merge 2 commits into
base: main
Choose a base branch
from
Open

CBMC: Add and prove x86_64 backend contracts #1393

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
d1d85fe
CBMC: Add x86-64 HOL-Light-based contracts and proofs
willieyz Dec 15, 2025
bc7522e
add symmetric note to all .ML HOL-LIGHT proofs
willieyz Jan 2, 2026
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
146 changes: 130 additions & 16 deletions dev/x86_64/src/arith_native_x86_64.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,65 +7,179 @@

#include "../../../common.h"

#include <immintrin.h>
#include <stdint.h>
#include "consts.h"

#define MLK_AVX2_REJ_UNIFORM_BUFLEN \
(3 * 168) /* REJ_UNIFORM_NBLOCKS * SHAKE128_RATE */

#define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm)
uint64_t mlk_rej_uniform_asm(int16_t *r, const uint8_t *buf, unsigned buflen,
const uint8_t *table);

#define mlk_rej_uniform_table MLK_NAMESPACE(rej_uniform_table)
extern const uint8_t mlk_rej_uniform_table[];

#define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm)
uint64_t mlk_rej_uniform_asm(int16_t *r, const uint8_t *buf, unsigned buflen,
const uint8_t *table)
/* This must be kept in sync with the HOL-Light specification
* in proofs/hol_light/x86_64/proofs/mlkem_rej_uniform.ml. */
__contract__(
requires(buflen % 12 == 0)
requires(memory_no_alias(buf, buflen))
requires(table == mlk_rej_uniform_table)
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
ensures(return_value <= MLKEM_N)
ensures(array_bound(r, 0, (unsigned) return_value, 0, MLKEM_Q))
);

#define mlk_ntt_avx2 MLK_NAMESPACE(ntt_avx2)
void mlk_ntt_avx2(int16_t *r, const int16_t *mlk_qdata);
void mlk_ntt_avx2(int16_t *r, const int16_t *qdata)
/* This must be kept in sync with the HOL-Light specification
* in proofs/hol_light/x86_64/proofs/mlkem_ntt.ml */
__contract__(
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
requires(array_abs_bound(r, 0, MLKEM_N, 8192))
requires(qdata == mlk_qdata)
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
/* check-magic: off */
ensures(array_abs_bound(r, 0, MLKEM_N, 23595))
/* check-magic: on */
);

#define mlk_invntt_avx2 MLK_NAMESPACE(invntt_avx2)
void mlk_invntt_avx2(int16_t *r, const int16_t *mlk_qdata);
void mlk_invntt_avx2(int16_t *r, const int16_t *qdata)
/* This must be kept in sync with the HOL-Light specification
* in proofs/hol_light/x86_64/proofs/mlkem_intt.ml */
__contract__(
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
requires(qdata == mlk_qdata)
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
/* check-magic: off */
ensures(array_abs_bound(r, 0, MLKEM_N, 26632))
/* check-magic: on */
);

#define mlk_nttunpack_avx2 MLK_NAMESPACE(nttunpack_avx2)
void mlk_nttunpack_avx2(int16_t *r);
void mlk_nttunpack_avx2(int16_t *r)
/* This must be kept in sync with the HOL-Light specification
* in proofs/hol_light/x86_64/proofs/mlkem_unpack.ml */
__contract__(
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
requires(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))
);

#define mlk_reduce_avx2 MLK_NAMESPACE(reduce_avx2)
void mlk_reduce_avx2(int16_t *r);
void mlk_reduce_avx2(int16_t *r)
/* This must be kept in sync with the HOL-Light specification
* in proofs/hol_light/x86_64/proofs/mlkem_reduce.ml */
__contract__(
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))
);

#define mlk_poly_mulcache_compute_avx2 MLK_NAMESPACE(poly_mulcache_compute_avx2)
void mlk_poly_mulcache_compute_avx2(int16_t *out, const int16_t *in,
const int16_t *mlk_qdata);
const int16_t *qdata)
/* This must be kept in sync with the HOL-Light specification
* in proofs/hol_light/x86_64/proofs/mlkem_mulcache_compute.ml */
__contract__(
requires(memory_no_alias(out, sizeof(int16_t) * (MLKEM_N / 2)))
requires(memory_no_alias(in, sizeof(int16_t) * MLKEM_N))
requires(qdata == mlk_qdata)
assigns(memory_slice(out, sizeof(int16_t) * (MLKEM_N / 2)))
ensures(array_abs_bound(out, 0, MLKEM_N/2, 3329))
);

#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k2 \
MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k2)
void mlk_polyvec_basemul_acc_montgomery_cached_asm_k2(int16_t *r,
const int16_t *a,
const int16_t *b,
const int16_t *b_cache);
const int16_t *b_cache)
/* This must be kept in sync with the HOL-Light specification in
* proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml.
*/
__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))
);

#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k3 \
MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k3)
void mlk_polyvec_basemul_acc_montgomery_cached_asm_k3(int16_t *r,
const int16_t *a,
const int16_t *b,
const int16_t *b_cache);
const int16_t *b_cache)
/* This must be kept in sync with the HOL-Light specification in
* proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml.
*/
__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))
);

#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k4 \
MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k4)
void mlk_polyvec_basemul_acc_montgomery_cached_asm_k4(int16_t *r,
const int16_t *a,
const int16_t *b,
const int16_t *b_cache);
const int16_t *b_cache)
/* This must be kept in sync with the HOL-Light specification in
* proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml.
*/
__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))
);

#define mlk_ntttobytes_avx2 MLK_NAMESPACE(ntttobytes_avx2)
void mlk_ntttobytes_avx2(uint8_t *r, const int16_t *a);
void mlk_ntttobytes_avx2(uint8_t *r, const int16_t *a)
/* This must be kept in sync with the HOL-Light specification in
* proofs/hol_light/x86_64/proofs/mlkem_tobytes.ml.
*/
__contract__(
requires(memory_no_alias(r, MLKEM_POLYBYTES))
requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_Q))
assigns(object_whole(r))
);

#define mlk_nttfrombytes_avx2 MLK_NAMESPACE(nttfrombytes_avx2)
void mlk_nttfrombytes_avx2(int16_t *r, const uint8_t *a);
void mlk_nttfrombytes_avx2(int16_t *r, const uint8_t *a)
Comment on lines -65 to +162
Copy link
Contributor

@hanno-becker hanno-becker Jan 15, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We need to think about if/how we can capture alignment constraints.

Contrary to AArch64, 32-byte parameter alignment is mandatory for most of the AVX2 backend, and indeed part of the HOL-Light specs. However, we don't express this in the C signature, nor in the CBMC contract (and we probably can't).

/* This must be kept in sync with the HOL-Light specification in
* proofs/hol_light/x86_64/proofs/mlkem_frombytes.ml.
*/
__contract__(
requires(memory_no_alias(a, MLKEM_POLYBYTES))
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))
);

#define mlk_tomont_avx2 MLK_NAMESPACE(tomont_avx2)
void mlk_tomont_avx2(int16_t *r);
void mlk_tomont_avx2(int16_t *r)
/* This must be kept in sync with the HOL-Light specification in
* proofs/hol_light/x86_64/proofs/mlkem_tomont.ml.
*/
__contract__(
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
ensures(array_abs_bound(r, 0, MLKEM_N, 3329))
);

#define mlk_poly_compress_d4_avx2 MLK_NAMESPACE(poly_compress_d4_avx2)
void mlk_poly_compress_d4_avx2(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D4],
Expand Down
146 changes: 130 additions & 16 deletions mlkem/src/native/x86_64/src/arith_native_x86_64.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,65 +7,179 @@

#include "../../../common.h"

#include <immintrin.h>
#include <stdint.h>
#include "consts.h"

#define MLK_AVX2_REJ_UNIFORM_BUFLEN \
(3 * 168) /* REJ_UNIFORM_NBLOCKS * SHAKE128_RATE */

#define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm)
uint64_t mlk_rej_uniform_asm(int16_t *r, const uint8_t *buf, unsigned buflen,
const uint8_t *table);

#define mlk_rej_uniform_table MLK_NAMESPACE(rej_uniform_table)
extern const uint8_t mlk_rej_uniform_table[];

#define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm)
uint64_t mlk_rej_uniform_asm(int16_t *r, const uint8_t *buf, unsigned buflen,
const uint8_t *table)
/* This must be kept in sync with the HOL-Light specification
* in proofs/hol_light/x86_64/proofs/mlkem_rej_uniform.ml. */
__contract__(
requires(buflen % 12 == 0)
requires(memory_no_alias(buf, buflen))
requires(table == mlk_rej_uniform_table)
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
ensures(return_value <= MLKEM_N)
ensures(array_bound(r, 0, (unsigned) return_value, 0, MLKEM_Q))
);

#define mlk_ntt_avx2 MLK_NAMESPACE(ntt_avx2)
void mlk_ntt_avx2(int16_t *r, const int16_t *mlk_qdata);
void mlk_ntt_avx2(int16_t *r, const int16_t *qdata)
/* This must be kept in sync with the HOL-Light specification
* in proofs/hol_light/x86_64/proofs/mlkem_ntt.ml */
__contract__(
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
requires(array_abs_bound(r, 0, MLKEM_N, 8192))
requires(qdata == mlk_qdata)
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
/* check-magic: off */
ensures(array_abs_bound(r, 0, MLKEM_N, 23595))
/* check-magic: on */
);

#define mlk_invntt_avx2 MLK_NAMESPACE(invntt_avx2)
void mlk_invntt_avx2(int16_t *r, const int16_t *mlk_qdata);
void mlk_invntt_avx2(int16_t *r, const int16_t *qdata)
/* This must be kept in sync with the HOL-Light specification
* in proofs/hol_light/x86_64/proofs/mlkem_intt.ml */
__contract__(
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
requires(qdata == mlk_qdata)
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
/* check-magic: off */
ensures(array_abs_bound(r, 0, MLKEM_N, 26632))
/* check-magic: on */
);

#define mlk_nttunpack_avx2 MLK_NAMESPACE(nttunpack_avx2)
void mlk_nttunpack_avx2(int16_t *r);
void mlk_nttunpack_avx2(int16_t *r)
/* This must be kept in sync with the HOL-Light specification
* in proofs/hol_light/x86_64/proofs/mlkem_unpack.ml */
__contract__(
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
requires(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))
Comment on lines +67 to +69
Copy link
Contributor

@hanno-becker hanno-becker Jan 15, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The HOL-Light proof does not have any bounds requires/ensures clauses.

Copy link
Contributor

@mkannwischer mkannwischer Jan 16, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Doesn't the HOL-LIght spec say the output is a permutation of the input?
That would imply that the bounds are maintained, wouldn't it?

Copy link
Contributor

@hanno-becker hanno-becker Jan 18, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, that's of course true, but we aim for as little logic in the translation between HOL-Light and CBMC specs as possible, because it's not checked automatically. I would prefer a solution where every clause in the CBMC spec is explicitly part of the HOL-Light spec.

Alternative, one could see if CBMC allows us to express the permutation spec, and infer the bounds preservation.

Copy link
Contributor

@hanno-becker hanno-becker Jan 18, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more. 

  /* Output is a permutation of input: every output coefficient
   * is some input coefficient */
  ensures(forall(i, 0, MLKEM_N, exists(j, 0, MLKEM_N,
    r[i] == old(*(int16_t (*)[MLKEM_N])r)[j])))

this seems to work with

#define exists(qvar, qvar_lb, qvar_ub, predicate)               \
  __CPROVER_exists                                              \
  {                                                             \
    unsigned qvar;                                              \
    ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) && (predicate)  \
  }

in mlkem/src/cbmc.h (we already have EXISTS defined like that, just rename it to exists in line with forall)

);

#define mlk_reduce_avx2 MLK_NAMESPACE(reduce_avx2)
void mlk_reduce_avx2(int16_t *r);
void mlk_reduce_avx2(int16_t *r)
/* This must be kept in sync with the HOL-Light specification
* in proofs/hol_light/x86_64/proofs/mlkem_reduce.ml */
__contract__(
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))
);

#define mlk_poly_mulcache_compute_avx2 MLK_NAMESPACE(poly_mulcache_compute_avx2)
void mlk_poly_mulcache_compute_avx2(int16_t *out, const int16_t *in,
const int16_t *mlk_qdata);
const int16_t *qdata)
/* This must be kept in sync with the HOL-Light specification
* in proofs/hol_light/x86_64/proofs/mlkem_mulcache_compute.ml */
__contract__(
requires(memory_no_alias(out, sizeof(int16_t) * (MLKEM_N / 2)))
requires(memory_no_alias(in, sizeof(int16_t) * MLKEM_N))
requires(qdata == mlk_qdata)
assigns(memory_slice(out, sizeof(int16_t) * (MLKEM_N / 2)))
ensures(array_abs_bound(out, 0, MLKEM_N/2, 3329))
);

#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k2 \
MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k2)
void mlk_polyvec_basemul_acc_montgomery_cached_asm_k2(int16_t *r,
const int16_t *a,
const int16_t *b,
const int16_t *b_cache);
const int16_t *b_cache)
/* This must be kept in sync with the HOL-Light specification in
* proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml.
*/
__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))
);

#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k3 \
MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k3)
void mlk_polyvec_basemul_acc_montgomery_cached_asm_k3(int16_t *r,
const int16_t *a,
const int16_t *b,
const int16_t *b_cache);
const int16_t *b_cache)
/* This must be kept in sync with the HOL-Light specification in
* proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml.
*/
__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))
);

#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k4 \
MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k4)
void mlk_polyvec_basemul_acc_montgomery_cached_asm_k4(int16_t *r,
const int16_t *a,
const int16_t *b,
const int16_t *b_cache);
const int16_t *b_cache)
/* This must be kept in sync with the HOL-Light specification in
* proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml.
*/
__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))
);

#define mlk_ntttobytes_avx2 MLK_NAMESPACE(ntttobytes_avx2)
void mlk_ntttobytes_avx2(uint8_t *r, const int16_t *a);
void mlk_ntttobytes_avx2(uint8_t *r, const int16_t *a)
/* This must be kept in sync with the HOL-Light specification in
* proofs/hol_light/x86_64/proofs/mlkem_tobytes.ml.
*/
__contract__(
requires(memory_no_alias(r, MLKEM_POLYBYTES))
requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_Q))
assigns(object_whole(r))
);

#define mlk_nttfrombytes_avx2 MLK_NAMESPACE(nttfrombytes_avx2)
void mlk_nttfrombytes_avx2(int16_t *r, const uint8_t *a);
void mlk_nttfrombytes_avx2(int16_t *r, const uint8_t *a)
/* This must be kept in sync with the HOL-Light specification in
* proofs/hol_light/x86_64/proofs/mlkem_frombytes.ml.
*/
__contract__(
requires(memory_no_alias(a, MLKEM_POLYBYTES))
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))
);

#define mlk_tomont_avx2 MLK_NAMESPACE(tomont_avx2)
void mlk_tomont_avx2(int16_t *r);
void mlk_tomont_avx2(int16_t *r)
/* This must be kept in sync with the HOL-Light specification in
* proofs/hol_light/x86_64/proofs/mlkem_tomont.ml.
*/
__contract__(
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
ensures(array_abs_bound(r, 0, MLKEM_N, 3329))
);

#define mlk_poly_compress_d4_avx2 MLK_NAMESPACE(poly_compress_d4_avx2)
void mlk_poly_compress_d4_avx2(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D4],
Expand Down
Loading