Skip to content

HOL-Light: improve tooling and CI#1634

Open
L-series wants to merge 2 commits into
mainfrom
HOL-Light-CI
Open

HOL-Light: improve tooling and CI#1634
L-series wants to merge 2 commits into
mainfrom
HOL-Light-CI

Conversation

@L-series
Copy link
Copy Markdown
Contributor

@L-series L-series commented Mar 20, 2026 •
edited
Loading

This commit aims to resolve the two following issues:

Note that the check-theorems script will currently fail the HOL-Light CI because for AArch, the naming convention for the memory safety proof (usually _SAFE) is not respected in mlkem_rej_uniform (it uses _MEMSAFE). @hanno-becker please advise if I should modify this.

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Mar 20, 2026 •
edited
Loading

CBMC Results (ML-KEM-768)

Full Results (191 proofs)
Proof Status Current Previous Change
**TOTAL** ✅ 1207s 1265s -4.6%
mlk_indcpa_keypair_derand ✅ 183s 200s -8%
mlk_indcpa_enc ✅ 160s 174s -8%
mlk_rej_uniform_c ✅ 115s 142s -19%
mlk_polyvec_basemul_acc_montgomery_cached_c ✅ 47s 40s +18%
mlk_ntt_layer ✅ 32s 27s +19%
mlk_poly_rej_uniform ✅ 29s 30s -3%
mlk_keccak_squeezeblocks_x4 ✅ 25s 24s +4%
poly_ntt_native ✅ 24s 30s -20%
mlk_poly_reduce_native ✅ 19s 23s -17%
polyvec_basemul_acc_montgomery_cached_native ✅ 18s 18s +0%
mlk_fqmul ✅ 17s 17s +0%
keccakf1600x4_permute_native_x4 ✅ 16s 16s +0%
mlk_indcpa_dec ✅ 16s 13s +23%
mlk_poly_decompress_d4_native ✅ 15s 16s -6%
mlk_poly_decompress_d10_native ✅ 13s 13s +0%
mlk_keccak_squeezeblocks ✅ 10s 10s +0%
mlk_keccak_squeeze_once ✅ 8s 8s +0%
mlk_poly_frommsg ✅ 8s 9s -11%
mlk_poly_ntt ✅ 8s 8s +0%
mlk_polyvec_add ✅ 8s 13s -38%
mlk_invntt_layer ✅ 7s 5s +40%
mlk_poly_frombytes_native ✅ 7s 8s -12%
mlk_gen_matrix ✅ 6s 3s +100%
mlk_gen_matrix_serial ✅ 6s 5s +20%
mlk_ntt_butterfly_block ✅ 6s 7s -14%
mlk_poly_rej_uniform_x4 ✅ 6s 6s +0%
kem_dec ✅ 5s 5s +0%
mlk_keccak_absorb_once_x4 ✅ 5s 6s -17%
mlk_keccakf1600_permute_c ✅ 5s 6s -17%
mlk_poly_decompress_d10_c ✅ 5s 2s +150%
mlk_polyvec_ntt ✅ 5s 1s +400%
mlk_scalar_compress_d11 ✅ 5s 2s +150%
poly_decompress_d10_native_x86_64 ✅ 5s 5s +0%
poly_decompress_d4_native_x86_64 ✅ 5s 6s -17%
poly_frombytes_native_x86_64 ✅ 5s 5s +0%
rej_uniform_native_aarch64 ✅ 5s 1s +400%
rej_uniform_native_x86_64 ✅ 5s 5s +0%
keccakf1600x4_xor_bytes_native ✅ 4s 2s +100%
mlk_ct_sel_int16 ✅ 4s 2s +100%
mlk_poly_compress_d10 ✅ 4s 1s +300%
mlk_poly_compress_d11 ✅ 4s 4s +0%
mlk_poly_compress_d11_c ✅ 4s 2s +100%
mlk_poly_compress_d4_c ✅ 4s 2s +100%
mlk_poly_decompress_d4_c ✅ 4s 2s +100%
mlk_poly_tomont ✅ 4s 1s +300%
mlk_poly_tomont_native ✅ 4s 3s +33%
mlk_polyvec_compress_du ✅ 4s 3s +33%
mlk_scalar_compress_d4 ✅ 4s 2s +100%
mlk_scalar_decompress_d5 ✅ 4s 2s +100%
intt_native_x86_64 ✅ 3s 2s +50%
keccakf1600x4_extract_bytes_native ✅ 3s 2s +50%
mlk_ct_get_optblocker_u8 ✅ 3s 3s +0%
mlk_ct_memcmp ✅ 3s 2s +50%
mlk_keccakf1600_extract_bytes (big endian) ✅ 3s 2s +50%
mlk_keccakf1600x4_extract_bytes_c ✅ 3s 2s +50%
mlk_keccakf1600x4_permute ✅ 3s 2s +50%
mlk_poly_compress_d5_c ✅ 3s 1s +200%
mlk_poly_compress_d5_native ✅ 3s 5s -40%
mlk_poly_decompress_d11 ✅ 3s 1s +200%
mlk_poly_decompress_d11_native ✅ 3s 3s +0%
mlk_poly_decompress_d4 ✅ 3s 2s +50%
mlk_poly_decompress_du ✅ 3s 2s +50%
mlk_poly_getnoise_eta1122_4x ✅ 3s 2s +50%
mlk_poly_getnoise_eta1_4x_native ✅ 3s 1s +200%
mlk_poly_mulcache_compute ✅ 3s 2s +50%
mlk_poly_sub ✅ 3s 3s +0%
mlk_poly_tobytes_c ✅ 3s 2s +50%
mlk_poly_tomsg ✅ 3s 2s +50%
mlk_polyvec_basemul_acc_montgomery_cached ✅ 3s 3s +0%
mlk_polyvec_permute_bitrev_to_custom ✅ 3s 1s +200%
mlk_polyvec_permute_bitrev_to_custom_native ✅ 3s 5s -40%
mlk_polyvec_reduce ✅ 3s 2s +50%
mlk_rej_uniform ✅ 3s 1s +200%
mlk_scalar_compress_d1 ✅ 3s 2s +50%
mlk_scalar_compress_d5 ✅ 3s 1s +200%
mlk_sha3_512 ✅ 3s 2s +50%
mlk_shake128x4_squeezeblocks ✅ 3s 1s +200%
mlk_shake256x4 ✅ 3s 4s -25%
mlk_value_barrier_u32 ✅ 3s 1s +200%
mlk_value_barrier_u8 ✅ 3s 2s +50%
nttunpack_native_x86_64 ✅ 3s 4s -25%
poly_compress_d10_native_x86_64 ✅ 3s 2s +50%
poly_decompress_d11_native_x86_64 ✅ 3s 3s +0%
poly_decompress_d5_native_x86_64 ✅ 3s 2s +50%
poly_tomont_native_aarch64 ✅ 3s 2s +50%
poly_tomont_native_x86_64 ✅ 3s 2s +50%
polyvec_basemul_acc_montgomery_cached_k2_native_aarch64 ✅ 3s 2s +50%
polyvec_basemul_acc_montgomery_cached_k2_native_x86_64 ✅ 3s 3s +0%
polyvec_basemul_acc_montgomery_cached_k4_native_aarch64 ✅ 3s 3s +0%
intt_native_aarch64 ✅ 2s 2s +0%
keccak_f1600_x1_native_aarch64_v84a ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v84a ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid ✅ 2s 1s +100%
keccak_f1600_x4_native_avx2 ✅ 2s 2s +0%
kem_check_pk ✅ 2s 4s -50%
kem_keypair ✅ 2s 3s -33%
kem_keypair_derand ✅ 2s 4s -50%
mlk_barrett_reduce ✅ 2s 3s -33%
mlk_check_pct ✅ 2s 4s -50%
mlk_ct_cmask_neg_i16 ✅ 2s 3s -33%
mlk_ct_cmask_nonzero_u16 ✅ 2s 3s -33%
mlk_ct_cmask_nonzero_u8 ✅ 2s 2s +0%
mlk_ct_get_optblocker_i32 ✅ 2s 2s +0%
mlk_ct_get_optblocker_u32 ✅ 2s 2s +0%
mlk_ct_sel_uint8 ✅ 2s 2s +0%
mlk_enc_getnoise_eta1_eta2 ✅ 2s 2s +0%
mlk_keccak_absorb_once ✅ 2s 4s -50%
mlk_keccakf1600_extract_bytes ✅ 2s 2s +0%
mlk_keccakf1600_xor_bytes ✅ 2s 2s +0%
mlk_keccakf1600_xor_bytes (big endian) ✅ 2s 2s +0%
mlk_keccakf1600x4_extract_bytes ✅ 2s 2s +0%
mlk_matvec_mul ✅ 2s 1s +100%
mlk_montgomery_reduce ✅ 2s 1s +100%
mlk_poly_add ✅ 2s 2s +0%
mlk_poly_cbd_eta1 ✅ 2s 1s +100%
mlk_poly_cbd_eta2 ✅ 2s 3s -33%
mlk_poly_compress_d10_c ✅ 2s 3s -33%
mlk_poly_compress_d10_native ✅ 2s 1s +100%
mlk_poly_compress_d11_native ✅ 2s 1s +100%
mlk_poly_compress_d4 ✅ 2s 3s -33%
mlk_poly_compress_d5 ✅ 2s 3s -33%
mlk_poly_decompress_d10 ✅ 2s 3s -33%
mlk_poly_decompress_d5 ✅ 2s 2s +0%
mlk_poly_decompress_d5_c ✅ 2s 4s -50%
mlk_poly_decompress_d5_native ✅ 2s 3s -33%
mlk_poly_frombytes ✅ 2s 1s +100%
mlk_poly_getnoise_eta1_4x ✅ 2s 2s +0%
mlk_poly_getnoise_eta2 ✅ 2s 3s -33%
mlk_poly_invntt_tomont_c ✅ 2s 1s +100%
mlk_poly_mulcache_compute_c ✅ 2s 4s -50%
mlk_poly_ntt_c ✅ 2s 3s -33%
mlk_poly_reduce ✅ 2s 1s +100%
mlk_poly_reduce_c ✅ 2s 1s +100%
mlk_poly_tomont_c ✅ 2s 2s +0%
mlk_polymat_permute_bitrev_to_custom ✅ 2s 3s -33%
mlk_polyvec_decompress_du ✅ 2s 1s +100%
mlk_polyvec_mulcache_compute ✅ 2s 3s -33%
mlk_polyvec_tobytes ✅ 2s 4s -50%
mlk_polyvec_tomont ✅ 2s 2s +0%
mlk_scalar_compress_d10 ✅ 2s 2s +0%
mlk_scalar_decompress_d10 ✅ 2s 3s -33%
mlk_scalar_decompress_d11 ✅ 2s 2s +0%
mlk_scalar_decompress_d4 ✅ 2s 2s +0%
mlk_scalar_signed_to_unsigned_q ✅ 2s 1s +100%
mlk_sha3_256 ✅ 2s 2s +0%
mlk_shake128_squeezeblocks ✅ 2s 2s +0%
mlk_shake128x4_absorb_once ✅ 2s 3s -33%
mlk_value_barrier_i32 ✅ 2s 3s -33%
ntt_native_aarch64 ✅ 2s 4s -50%
ntt_native_x86_64 ✅ 2s 4s -50%
poly_compress_d11_native_x86_64 ✅ 2s 3s -33%
poly_compress_d5_native_x86_64 ✅ 2s 2s +0%
poly_invntt_tomont_native ✅ 2s 2s +0%
poly_mulcache_compute_native_aarch64 ✅ 2s 2s +0%
poly_mulcache_compute_native_x86_64 ✅ 2s 4s -50%
poly_reduce_native_x86_64 ✅ 2s 3s -33%
poly_tobytes_native_aarch64 ✅ 2s 2s +0%
poly_tobytes_native_x86_64 ✅ 2s 3s -33%
polyvec_basemul_acc_montgomery_cached_k3_native_aarch64 ✅ 2s 4s -50%
polyvec_basemul_acc_montgomery_cached_k4_native_x86_64 ✅ 2s 3s -33%
sys_check_capability ✅ 2s 4s -50%
keccak_f1600_x1_native_aarch64 ✅ 1s 2s -50%
keccakf1600_permute_native ✅ 1s 2s -50%
kem_check_sk ✅ 1s 1s +0%
kem_enc ✅ 1s 3s -67%
kem_enc_derand ✅ 1s 2s -50%
mlk_ct_cmov_zero ✅ 1s 3s -67%
mlk_keccakf1600_permute ✅ 1s 3s -67%
mlk_keccakf1600x4_xor_bytes ✅ 1s 1s +0%
mlk_keccakf1600x4_xor_bytes_c ✅ 1s 2s -50%
mlk_keypair_getnoise_eta1 ✅ 1s 4s -75%
mlk_poly_compress_d4_native ✅ 1s 2s -50%
mlk_poly_compress_du ✅ 1s 2s -50%
mlk_poly_compress_dv ✅ 1s 2s -50%
mlk_poly_decompress_d11_c ✅ 1s 1s +0%
mlk_poly_decompress_dv ✅ 1s 3s -67%
mlk_poly_frombytes_c ✅ 1s 2s -50%
mlk_poly_invntt_tomont ✅ 1s 2s -50%
mlk_poly_mulcache_compute_native ✅ 1s 1s +0%
mlk_poly_tobytes ✅ 1s 1s +0%
mlk_poly_tobytes_native ✅ 1s 2s -50%
mlk_polyvec_frombytes ✅ 1s 2s -50%
mlk_polyvec_invntt_tomont ✅ 1s 3s -67%
mlk_shake128_absorb_once ✅ 1s 2s -50%
mlk_shake256 ✅ 1s 2s -50%
poly_compress_d4_native_x86_64 ✅ 1s 3s -67%
poly_getnoise_eta1122_4x_native ✅ 1s 1s +0%
poly_reduce_native_aarch64 ✅ 1s 1s +0%
polyvec_basemul_acc_montgomery_cached_k3_native_x86_64 ✅ 1s 2s -50%
rej_uniform_native ✅ 1s 4s -75%

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Mar 20, 2026 •
edited
Loading

CBMC Results (ML-KEM-512)

Full Results (191 proofs)
Proof Status Current Previous Change
**TOTAL** ✅ 1294s 1297s -0.2%
mlk_indcpa_keypair_derand ✅ 249s 237s +5%
mlk_indcpa_enc ✅ 168s 165s +2%
mlk_rej_uniform_c ✅ 122s 121s +1%
mlk_polyvec_basemul_acc_montgomery_cached_c ✅ 52s 50s +4%
mlk_ntt_layer ✅ 33s 32s +3%
mlk_poly_rej_uniform ✅ 30s 30s +0%
poly_ntt_native ✅ 25s 23s +9%
mlk_keccak_squeezeblocks_x4 ✅ 24s 27s -11%
mlk_poly_reduce_native ✅ 21s 19s +11%
keccakf1600x4_permute_native_x4 ✅ 17s 17s +0%
mlk_fqmul ✅ 16s 15s +7%
mlk_indcpa_dec ✅ 15s 14s +7%
mlk_poly_decompress_d10_native ✅ 13s 14s -7%
mlk_poly_decompress_d4_native ✅ 13s 15s -13%
mlk_polyvec_add ✅ 10s 10s +0%
mlk_keccak_squeeze_once ✅ 8s 9s -11%
mlk_keccak_squeezeblocks ✅ 8s 9s -11%
mlk_poly_rej_uniform_x4 ✅ 8s 6s +33%
polyvec_basemul_acc_montgomery_cached_native ✅ 8s 6s +33%
mlk_poly_frombytes_native ✅ 7s 7s +0%
mlk_poly_frommsg ✅ 7s 7s +0%
mlk_keccak_absorb_once_x4 ✅ 6s 6s +0%
mlk_matvec_mul ✅ 6s 3s +100%
mlk_ntt_butterfly_block ✅ 6s 8s -25%
mlk_poly_ntt ✅ 6s 8s -25%
rej_uniform_native_x86_64 ✅ 6s 6s +0%
kem_enc_derand ✅ 5s 1s +400%
mlk_ct_cmask_nonzero_u8 ✅ 5s 3s +67%
mlk_keccakf1600x4_extract_bytes ✅ 5s 1s +400%
mlk_montgomery_reduce ✅ 5s 1s +400%
mlk_poly_cbd_eta2 ✅ 5s 5s +0%
mlk_poly_decompress_d5_c ✅ 5s 2s +150%
mlk_poly_tomsg ✅ 5s 3s +67%
poly_decompress_d4_native_x86_64 ✅ 5s 4s +25%
poly_frombytes_native_x86_64 ✅ 5s 5s +0%
keccak_f1600_x4_native_avx2 ✅ 4s 1s +300%
kem_enc ✅ 4s 2s +100%
mlk_invntt_layer ✅ 4s 5s -20%
mlk_keccakf1600_permute_c ✅ 4s 4s +0%
mlk_poly_compress_d5 ✅ 4s 2s +100%
mlk_poly_compress_d5_native ✅ 4s 3s +33%
mlk_poly_compress_du ✅ 4s 2s +100%
mlk_poly_decompress_d5_native ✅ 4s 1s +300%
mlk_poly_invntt_tomont_c ✅ 4s 2s +100%
mlk_polyvec_basemul_acc_montgomery_cached ✅ 4s 5s -20%
mlk_polyvec_frombytes ✅ 4s 3s +33%
mlk_polyvec_invntt_tomont ✅ 4s 2s +100%
mlk_scalar_compress_d5 ✅ 4s 2s +100%
mlk_shake256x4 ✅ 4s 5s -20%
poly_compress_d10_native_x86_64 ✅ 4s 2s +100%
poly_decompress_d10_native_x86_64 ✅ 4s 5s -20%
polyvec_basemul_acc_montgomery_cached_k2_native_aarch64 ✅ 4s 2s +100%
polyvec_basemul_acc_montgomery_cached_k4_native_x86_64 ✅ 4s 2s +100%
intt_native_x86_64 ✅ 3s 4s -25%
keccakf1600_permute_native ✅ 3s 4s -25%
keccakf1600x4_xor_bytes_native ✅ 3s 2s +50%
kem_check_pk ✅ 3s 3s +0%
kem_check_sk ✅ 3s 3s +0%
kem_keypair ✅ 3s 2s +50%
mlk_gen_matrix ✅ 3s 3s +0%
mlk_gen_matrix_serial ✅ 3s 2s +50%
mlk_keccak_absorb_once ✅ 3s 3s +0%
mlk_keccakf1600_permute ✅ 3s 3s +0%
mlk_keccakf1600_xor_bytes ✅ 3s 2s +50%
mlk_keccakf1600x4_xor_bytes ✅ 3s 2s +50%
mlk_keccakf1600x4_xor_bytes_c ✅ 3s 3s +0%
mlk_poly_cbd_eta1 ✅ 3s 4s -25%
mlk_poly_compress_d11_c ✅ 3s 3s +0%
mlk_poly_compress_d11_native ✅ 3s 1s +200%
mlk_poly_compress_d4_c ✅ 3s 2s +50%
mlk_poly_compress_d4_native ✅ 3s 2s +50%
mlk_poly_compress_dv ✅ 3s 3s +0%
mlk_poly_decompress_d10_c ✅ 3s 2s +50%
mlk_poly_decompress_d4_c ✅ 3s 4s -25%
mlk_poly_getnoise_eta2 ✅ 3s 2s +50%
mlk_poly_invntt_tomont ✅ 3s 1s +200%
mlk_poly_mulcache_compute_c ✅ 3s 5s -40%
mlk_poly_mulcache_compute_native ✅ 3s 2s +50%
mlk_poly_ntt_c ✅ 3s 4s -25%
mlk_poly_reduce ✅ 3s 1s +200%
mlk_poly_tomont_native ✅ 3s 3s +0%
mlk_polyvec_decompress_du ✅ 3s 5s -40%
mlk_polyvec_ntt ✅ 3s 1s +200%
mlk_polyvec_permute_bitrev_to_custom ✅ 3s 3s +0%
mlk_polyvec_permute_bitrev_to_custom_native ✅ 3s 2s +50%
mlk_polyvec_tobytes ✅ 3s 3s +0%
mlk_scalar_compress_d11 ✅ 3s 2s +50%
mlk_scalar_decompress_d10 ✅ 3s 3s +0%
mlk_scalar_decompress_d11 ✅ 3s 2s +50%
mlk_sha3_256 ✅ 3s 2s +50%
mlk_value_barrier_i32 ✅ 3s 4s -25%
mlk_value_barrier_u32 ✅ 3s 2s +50%
ntt_native_aarch64 ✅ 3s 2s +50%
nttunpack_native_x86_64 ✅ 3s 4s -25%
poly_getnoise_eta1122_4x_native ✅ 3s 4s -25%
poly_reduce_native_x86_64 ✅ 3s 3s +0%
poly_tobytes_native_aarch64 ✅ 3s 3s +0%
poly_tomont_native_x86_64 ✅ 3s 3s +0%
polyvec_basemul_acc_montgomery_cached_k2_native_x86_64 ✅ 3s 4s -25%
polyvec_basemul_acc_montgomery_cached_k3_native_x86_64 ✅ 3s 2s +50%
rej_uniform_native ✅ 3s 3s +0%
intt_native_aarch64 ✅ 2s 1s +100%
keccak_f1600_x1_native_aarch64 ✅ 2s 2s +0%
keccak_f1600_x1_native_aarch64_v84a ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v84a ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid ✅ 2s 4s -50%
kem_dec ✅ 2s 5s -60%
kem_keypair_derand ✅ 2s 2s +0%
mlk_barrett_reduce ✅ 2s 2s +0%
mlk_ct_cmask_neg_i16 ✅ 2s 2s +0%
mlk_ct_cmov_zero ✅ 2s 3s -33%
mlk_ct_memcmp ✅ 2s 3s -33%
mlk_ct_sel_int16 ✅ 2s 1s +100%
mlk_ct_sel_uint8 ✅ 2s 5s -60%
mlk_enc_getnoise_eta1_eta2 ✅ 2s 6s -67%
mlk_keccakf1600_extract_bytes (big endian) ✅ 2s 3s -33%
mlk_keccakf1600x4_extract_bytes_c ✅ 2s 1s +100%
mlk_poly_add ✅ 2s 2s +0%
mlk_poly_compress_d10 ✅ 2s 1s +100%
mlk_poly_compress_d10_c ✅ 2s 5s -60%
mlk_poly_compress_d5_c ✅ 2s 4s -50%
mlk_poly_decompress_d11 ✅ 2s 1s +100%
mlk_poly_decompress_d11_c ✅ 2s 3s -33%
mlk_poly_decompress_d11_native ✅ 2s 2s +0%
mlk_poly_decompress_d5 ✅ 2s 2s +0%
mlk_poly_frombytes_c ✅ 2s 4s -50%
mlk_poly_getnoise_eta1122_4x ✅ 2s 4s -50%
mlk_poly_getnoise_eta1_4x ✅ 2s 2s +0%
mlk_poly_getnoise_eta1_4x_native ✅ 2s 3s -33%
mlk_poly_reduce_c ✅ 2s 1s +100%
mlk_poly_tobytes ✅ 2s 2s +0%
mlk_poly_tobytes_c ✅ 2s 1s +100%
mlk_poly_tobytes_native ✅ 2s 1s +100%
mlk_poly_tomont ✅ 2s 3s -33%
mlk_polymat_permute_bitrev_to_custom ✅ 2s 2s +0%
mlk_polyvec_mulcache_compute ✅ 2s 3s -33%
mlk_polyvec_tomont ✅ 2s 2s +0%
mlk_rej_uniform ✅ 2s 2s +0%
mlk_scalar_compress_d1 ✅ 2s 5s -60%
mlk_scalar_compress_d10 ✅ 2s 1s +100%
mlk_scalar_compress_d4 ✅ 2s 2s +0%
mlk_scalar_decompress_d4 ✅ 2s 1s +100%
mlk_scalar_decompress_d5 ✅ 2s 3s -33%
mlk_sha3_512 ✅ 2s 1s +100%
mlk_shake128_absorb_once ✅ 2s 3s -33%
mlk_shake128x4_absorb_once ✅ 2s 2s +0%
mlk_value_barrier_u8 ✅ 2s 1s +100%
ntt_native_x86_64 ✅ 2s 3s -33%
poly_compress_d11_native_x86_64 ✅ 2s 3s -33%
poly_compress_d4_native_x86_64 ✅ 2s 2s +0%
poly_compress_d5_native_x86_64 ✅ 2s 1s +100%
poly_decompress_d11_native_x86_64 ✅ 2s 5s -60%
poly_decompress_d5_native_x86_64 ✅ 2s 3s -33%
poly_mulcache_compute_native_aarch64 ✅ 2s 4s -50%
poly_mulcache_compute_native_x86_64 ✅ 2s 3s -33%
poly_reduce_native_aarch64 ✅ 2s 4s -50%
poly_tobytes_native_x86_64 ✅ 2s 1s +100%
polyvec_basemul_acc_montgomery_cached_k4_native_aarch64 ✅ 2s 3s -33%
rej_uniform_native_aarch64 ✅ 2s 3s -33%
sys_check_capability ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid ✅ 1s 2s -50%
keccakf1600x4_extract_bytes_native ✅ 1s 3s -67%
mlk_check_pct ✅ 1s 3s -67%
mlk_ct_cmask_nonzero_u16 ✅ 1s 1s +0%
mlk_ct_get_optblocker_i32 ✅ 1s 2s -50%
mlk_ct_get_optblocker_u32 ✅ 1s 4s -75%
mlk_ct_get_optblocker_u8 ✅ 1s 3s -67%
mlk_keccakf1600_extract_bytes ✅ 1s 3s -67%
mlk_keccakf1600_xor_bytes (big endian) ✅ 1s 4s -75%
mlk_keccakf1600x4_permute ✅ 1s 4s -75%
mlk_keypair_getnoise_eta1 ✅ 1s 2s -50%
mlk_poly_compress_d10_native ✅ 1s 2s -50%
mlk_poly_compress_d11 ✅ 1s 1s +0%
mlk_poly_compress_d4 ✅ 1s 2s -50%
mlk_poly_decompress_d10 ✅ 1s 2s -50%
mlk_poly_decompress_d4 ✅ 1s 2s -50%
mlk_poly_decompress_du ✅ 1s 2s -50%
mlk_poly_decompress_dv ✅ 1s 2s -50%
mlk_poly_frombytes ✅ 1s 3s -67%
mlk_poly_mulcache_compute ✅ 1s 2s -50%
mlk_poly_sub ✅ 1s 2s -50%
mlk_poly_tomont_c ✅ 1s 3s -67%
mlk_polyvec_compress_du ✅ 1s 2s -50%
mlk_polyvec_reduce ✅ 1s 4s -75%
mlk_scalar_signed_to_unsigned_q ✅ 1s 3s -67%
mlk_shake128_squeezeblocks ✅ 1s 2s -50%
mlk_shake128x4_squeezeblocks ✅ 1s 3s -67%
mlk_shake256 ✅ 1s 1s +0%
poly_invntt_tomont_native ✅ 1s 2s -50%
poly_tomont_native_aarch64 ✅ 1s 2s -50%
polyvec_basemul_acc_montgomery_cached_k3_native_aarch64 ✅ 1s 3s -67%

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Mar 20, 2026 •
edited
Loading

CBMC Results (ML-KEM-1024)

Full Results (191 proofs)
Proof Status Current Previous Change
**TOTAL** ✅ 1270s 1172s +8.4%
mlk_indcpa_enc ✅ 151s 139s +9%
mlk_rej_uniform_c ✅ 135s 113s +19%
mlk_indcpa_keypair_derand ✅ 132s 120s +10%
mlk_polyvec_basemul_acc_montgomery_cached_c ✅ 81s 73s +11%
mlk_ntt_layer ✅ 37s 31s +19%
polyvec_basemul_acc_montgomery_cached_native ✅ 37s 33s +12%
mlk_poly_rej_uniform ✅ 33s 29s +14%
poly_ntt_native ✅ 28s 24s +17%
mlk_keccak_squeezeblocks_x4 ✅ 24s 23s +4%
mlk_poly_reduce_native ✅ 22s 21s +5%
mlk_fqmul ✅ 18s 15s +20%
keccakf1600x4_permute_native_x4 ✅ 15s 18s -17%
mlk_poly_decompress_d11_native ✅ 15s 14s +7%
mlk_poly_decompress_d5_native ✅ 15s 14s +7%
mlk_polyvec_add ✅ 11s 11s +0%
mlk_poly_frombytes_native ✅ 10s 8s +25%
mlk_gen_matrix_serial ✅ 9s 4s +125%
mlk_poly_ntt ✅ 9s 4s +125%
mlk_indcpa_dec ✅ 8s 7s +14%
mlk_keccak_squeeze_once ✅ 8s 7s +14%
mlk_poly_frommsg ✅ 8s 8s +0%
mlk_poly_rej_uniform_x4 ✅ 8s 7s +14%
mlk_keccak_absorb_once_x4 ✅ 7s 5s +40%
mlk_keccak_squeezeblocks ✅ 7s 7s +0%
mlk_poly_compress_d11_c ✅ 7s 6s +17%
mlk_ntt_butterfly_block ✅ 6s 8s -25%
mlk_polymat_permute_bitrev_to_custom ✅ 6s 5s +20%
kem_check_pk ✅ 5s 2s +150%
mlk_gen_matrix ✅ 5s 5s +0%
mlk_invntt_layer ✅ 5s 5s +0%
mlk_keccakf1600_permute_c ✅ 5s 4s +25%
mlk_poly_mulcache_compute_native ✅ 5s 3s +67%
mlk_polyvec_ntt ✅ 5s 3s +67%
poly_frombytes_native_x86_64 ✅ 5s 3s +67%
rej_uniform_native_x86_64 ✅ 5s 5s +0%
keccakf1600_permute_native ✅ 4s 3s +33%
kem_dec ✅ 4s 4s +0%
mlk_ct_cmask_neg_i16 ✅ 4s 4s +0%
mlk_matvec_mul ✅ 4s 5s -20%
mlk_poly_add ✅ 4s 1s +300%
mlk_poly_decompress_d11_c ✅ 4s 4s +0%
mlk_poly_decompress_d4_native ✅ 4s 3s +33%
mlk_poly_mulcache_compute ✅ 4s 3s +33%
mlk_poly_reduce ✅ 4s 3s +33%
mlk_poly_reduce_c ✅ 4s 2s +100%
mlk_poly_tomont_c ✅ 4s 2s +100%
mlk_poly_tomont_native ✅ 4s 1s +300%
mlk_polyvec_reduce ✅ 4s 2s +100%
mlk_polyvec_tomont ✅ 4s 2s +100%
mlk_scalar_compress_d10 ✅ 4s 3s +33%
mlk_scalar_compress_d5 ✅ 4s 1s +300%
mlk_shake256x4 ✅ 4s 3s +33%
nttunpack_native_x86_64 ✅ 4s 2s +100%
poly_compress_d11_native_x86_64 ✅ 4s 1s +300%
poly_decompress_d11_native_x86_64 ✅ 4s 3s +33%
poly_decompress_d5_native_x86_64 ✅ 4s 6s -33%
intt_native_aarch64 ✅ 3s 2s +50%
keccak_f1600_x1_native_aarch64 ✅ 3s 2s +50%
keccak_f1600_x1_native_aarch64_v84a ✅ 3s 5s -40%
keccak_f1600_x4_native_aarch64_v84a ✅ 3s 1s +200%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid ✅ 3s 3s +0%
keccakf1600x4_xor_bytes_native ✅ 3s 2s +50%
kem_check_sk ✅ 3s 3s +0%
kem_keypair ✅ 3s 3s +0%
mlk_ct_cmask_nonzero_u8 ✅ 3s 5s -40%
mlk_ct_sel_int16 ✅ 3s 2s +50%
mlk_enc_getnoise_eta1_eta2 ✅ 3s 4s -25%
mlk_keccak_absorb_once ✅ 3s 3s +0%
mlk_keccakf1600_xor_bytes ✅ 3s 2s +50%
mlk_poly_compress_d10_c ✅ 3s 3s +0%
mlk_poly_compress_d10_native ✅ 3s 3s +0%
mlk_poly_compress_d11_native ✅ 3s 3s +0%
mlk_poly_compress_d4_native ✅ 3s 3s +0%
mlk_poly_compress_d5 ✅ 3s 2s +50%
mlk_poly_decompress_d10 ✅ 3s 1s +200%
mlk_poly_decompress_d4_c ✅ 3s 3s +0%
mlk_poly_decompress_dv ✅ 3s 1s +200%
mlk_poly_getnoise_eta1_4x ✅ 3s 3s +0%
mlk_poly_getnoise_eta2 ✅ 3s 4s -25%
mlk_poly_invntt_tomont_c ✅ 3s 2s +50%
mlk_poly_ntt_c ✅ 3s 4s -25%
mlk_poly_tobytes ✅ 3s 1s +200%
mlk_poly_tomont ✅ 3s 2s +50%
mlk_poly_tomsg ✅ 3s 1s +200%
mlk_polyvec_basemul_acc_montgomery_cached ✅ 3s 5s -40%
mlk_polyvec_frombytes ✅ 3s 2s +50%
mlk_polyvec_invntt_tomont ✅ 3s 2s +50%
mlk_polyvec_mulcache_compute ✅ 3s 5s -40%
mlk_scalar_compress_d1 ✅ 3s 2s +50%
mlk_scalar_decompress_d11 ✅ 3s 2s +50%
mlk_scalar_decompress_d4 ✅ 3s 2s +50%
mlk_scalar_decompress_d5 ✅ 3s 1s +200%
mlk_scalar_signed_to_unsigned_q ✅ 3s 4s -25%
mlk_shake128_absorb_once ✅ 3s 2s +50%
mlk_value_barrier_i32 ✅ 3s 3s +0%
mlk_value_barrier_u8 ✅ 3s 2s +50%
poly_compress_d10_native_x86_64 ✅ 3s 2s +50%
poly_decompress_d10_native_x86_64 ✅ 3s 3s +0%
poly_getnoise_eta1122_4x_native ✅ 3s 2s +50%
poly_invntt_tomont_native ✅ 3s 3s +0%
poly_mulcache_compute_native_aarch64 ✅ 3s 3s +0%
poly_mulcache_compute_native_x86_64 ✅ 3s 3s +0%
poly_tobytes_native_x86_64 ✅ 3s 4s -25%
poly_tomont_native_aarch64 ✅ 3s 2s +50%
poly_tomont_native_x86_64 ✅ 3s 2s +50%
polyvec_basemul_acc_montgomery_cached_k2_native_x86_64 ✅ 3s 3s +0%
polyvec_basemul_acc_montgomery_cached_k4_native_x86_64 ✅ 3s 3s +0%
rej_uniform_native ✅ 3s 1s +200%
rej_uniform_native_aarch64 ✅ 3s 2s +50%
sys_check_capability ✅ 3s 2s +50%
intt_native_x86_64 ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid ✅ 2s 2s +0%
keccakf1600x4_extract_bytes_native ✅ 2s 1s +100%
kem_enc ✅ 2s 1s +100%
kem_keypair_derand ✅ 2s 1s +100%
mlk_barrett_reduce ✅ 2s 2s +0%
mlk_check_pct ✅ 2s 3s -33%
mlk_ct_cmov_zero ✅ 2s 2s +0%
mlk_ct_get_optblocker_i32 ✅ 2s 1s +100%
mlk_ct_get_optblocker_u32 ✅ 2s 1s +100%
mlk_ct_get_optblocker_u8 ✅ 2s 4s -50%
mlk_ct_memcmp ✅ 2s 2s +0%
mlk_ct_sel_uint8 ✅ 2s 2s +0%
mlk_keccakf1600_extract_bytes (big endian) ✅ 2s 2s +0%
mlk_keccakf1600_permute ✅ 2s 4s -50%
mlk_keccakf1600x4_extract_bytes ✅ 2s 4s -50%
mlk_keccakf1600x4_extract_bytes_c ✅ 2s 3s -33%
mlk_keccakf1600x4_xor_bytes_c ✅ 2s 4s -50%
mlk_keypair_getnoise_eta1 ✅ 2s 3s -33%
mlk_montgomery_reduce ✅ 2s 4s -50%
mlk_poly_cbd_eta1 ✅ 2s 4s -50%
mlk_poly_cbd_eta2 ✅ 2s 2s +0%
mlk_poly_compress_d11 ✅ 2s 3s -33%
mlk_poly_compress_d4 ✅ 2s 2s +0%
mlk_poly_compress_d4_c ✅ 2s 2s +0%
mlk_poly_compress_d5_c ✅ 2s 1s +100%
mlk_poly_compress_d5_native ✅ 2s 1s +100%
mlk_poly_compress_du ✅ 2s 2s +0%
mlk_poly_decompress_d10_c ✅ 2s 1s +100%
mlk_poly_decompress_d10_native ✅ 2s 1s +100%
mlk_poly_decompress_d4 ✅ 2s 3s -33%
mlk_poly_decompress_d5 ✅ 2s 3s -33%
mlk_poly_frombytes_c ✅ 2s 3s -33%
mlk_poly_getnoise_eta1122_4x ✅ 2s 3s -33%
mlk_poly_getnoise_eta1_4x_native ✅ 2s 2s +0%
mlk_poly_mulcache_compute_c ✅ 2s 1s +100%
mlk_poly_sub ✅ 2s 2s +0%
mlk_poly_tobytes_c ✅ 2s 3s -33%
mlk_polyvec_compress_du ✅ 2s 3s -33%
mlk_polyvec_decompress_du ✅ 2s 2s +0%
mlk_polyvec_permute_bitrev_to_custom_native ✅ 2s 3s -33%
mlk_polyvec_tobytes ✅ 2s 3s -33%
mlk_scalar_compress_d11 ✅ 2s 2s +0%
mlk_scalar_compress_d4 ✅ 2s 2s +0%
mlk_scalar_decompress_d10 ✅ 2s 2s +0%
mlk_value_barrier_u32 ✅ 2s 2s +0%
ntt_native_aarch64 ✅ 2s 4s -50%
ntt_native_x86_64 ✅ 2s 2s +0%
poly_compress_d4_native_x86_64 ✅ 2s 4s -50%
poly_compress_d5_native_x86_64 ✅ 2s 3s -33%
poly_decompress_d4_native_x86_64 ✅ 2s 1s +100%
poly_tobytes_native_aarch64 ✅ 2s 4s -50%
polyvec_basemul_acc_montgomery_cached_k2_native_aarch64 ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k3_native_aarch64 ✅ 2s 5s -60%
polyvec_basemul_acc_montgomery_cached_k3_native_x86_64 ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k4_native_aarch64 ✅ 2s 1s +100%
keccak_f1600_x4_native_avx2 ✅ 1s 1s +0%
kem_enc_derand ✅ 1s 2s -50%
mlk_ct_cmask_nonzero_u16 ✅ 1s 3s -67%
mlk_keccakf1600_extract_bytes ✅ 1s 1s +0%
mlk_keccakf1600_xor_bytes (big endian) ✅ 1s 1s +0%
mlk_keccakf1600x4_permute ✅ 1s 3s -67%
mlk_keccakf1600x4_xor_bytes ✅ 1s 2s -50%
mlk_poly_compress_d10 ✅ 1s 3s -67%
mlk_poly_compress_dv ✅ 1s 5s -80%
mlk_poly_decompress_d11 ✅ 1s 2s -50%
mlk_poly_decompress_d5_c ✅ 1s 2s -50%
mlk_poly_decompress_du ✅ 1s 2s -50%
mlk_poly_frombytes ✅ 1s 3s -67%
mlk_poly_invntt_tomont ✅ 1s 1s +0%
mlk_poly_tobytes_native ✅ 1s 1s +0%
mlk_polyvec_permute_bitrev_to_custom ✅ 1s 3s -67%
mlk_rej_uniform ✅ 1s 2s -50%
mlk_sha3_256 ✅ 1s 5s -80%
mlk_sha3_512 ✅ 1s 1s +0%
mlk_shake128_squeezeblocks ✅ 1s 1s +0%
mlk_shake128x4_absorb_once ✅ 1s 2s -50%
mlk_shake128x4_squeezeblocks ✅ 1s 2s -50%
mlk_shake256 ✅ 1s 1s +0%
poly_reduce_native_aarch64 ✅ 1s 2s -50%
poly_reduce_native_x86_64 ✅ 1s 4s -75%

@L-series L-series changed the title HOL-Light: improve tooling and CI" HOL-Light: improve tooling and CI Mar 20, 2026
@L-series L-series force-pushed the HOL-Light-CI branch 2 times, most recently from 724e0b1 to 9a3e91a Compare March 23, 2026 14:16
@L-series L-series marked this pull request as ready for review March 23, 2026 14:16
@L-series L-series requested a review from a team as a code owner March 23, 2026 14:16
@L-series
Copy link
Copy Markdown
Contributor Author

L-series commented Mar 23, 2026

Modified the two remaining occurences of _MEMSAFE to _SAFE in order to fit the expected format for aarch proofs.

@L-series L-series force-pushed the HOL-Light-CI branch 2 times, most recently from 25cad96 to 3e258d8 Compare March 23, 2026 14:55
@L-series L-series mentioned this pull request Apr 1, 2026
Draft
@mkannwischer mkannwischer self-assigned this Apr 2, 2026
mkannwischer
mkannwischer requested changes Apr 2, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@mkannwischer mkannwischer left a comment

Choose a reason for hiding this comment

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

Thanks @L-series - I left a couple of comments.

This PR actually takes another approach that I had in mind: I thought that after running each HOL-Light proof we check for the expected theorems to be present.
The approach implemented here is more like a linter. But I support the addition!
The -a flag is highly appreciated - thank you!

Comment thread scripts/tests Outdated
Comment thread scripts/tests Outdated
Comment thread scripts/check-theorems Outdated
Comment thread .github/workflows/hol_light.yml Outdated
Comment thread scripts/check-theorems Outdated
Comment thread scripts/check-theorems Outdated
[[ $ARCH == "x86_64" && $routine == "mlkem_rej_uniform" ]] && suffixes=("CORRECT")

for sfx in "${suffixes[@]}"; do
if ! grep -q "_${sfx}" "$PROOFS_DIR/${routine}.ml"; then
Copy link
Copy Markdown
Contributor

@mkannwischer mkannwischer Apr 2, 2026

Choose a reason for hiding this comment

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

can you actually grep for {suffix} = prove or {suffix} = time prove?

Copy link
Copy Markdown
Contributor Author

@L-series L-series Apr 3, 2026 •
edited
Loading

Choose a reason for hiding this comment

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

Done, however please note that I modified some of the proofs as they included double whitespaces before the = prove. I opted for this as it seems cleaner than having a more complicated regexp. As an aside, perhaps there is some tool to apply standard formatting onto the *.ml files?

@L-series
Copy link
Copy Markdown
Contributor Author

L-series commented Apr 3, 2026

Thanks @L-series - I left a couple of comments.

This PR actually takes another approach that I had in mind: I thought that after running each HOL-Light proof we check for the expected theorems to be present. The approach implemented here is more like a linter. But I support the addition! The -a flag is highly appreciated - thank you!

Thank you for the review! Indeed, the idea I had in mind was that one should avoid using compute on proofs which do not contain the required theorems. However, I see now that there is still value running the HOL CI even if the routine is only partially proven.

mkannwischer
mkannwischer requested changes Apr 3, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@mkannwischer mkannwischer left a comment

Choose a reason for hiding this comment

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

Thanks @L-series for the changes! I'm happy with the overall approach now.

Two comments still need to be addressed. Thank you!

Comment thread scripts/lint Outdated
if [[ $arch == "x86_64" && ${routine} == "mlkem_rej_uniform" ]]; then
suffixes=("CORRECT")
elif [[ $arch == "x86_64" ]]; then
suffixes+=("SUBROUTINE_CORRECT" "NOIBT_SUBROUTINE_CORRECT" "NOIBT_SUBROUTINE_SAFE")
Copy link
Copy Markdown
Contributor

@mkannwischer mkannwischer Apr 3, 2026

Choose a reason for hiding this comment

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

I tried removing the SUBROUTINE_SAFE proof from the mlkem_poly_compress_d4.ml proof and the script did not catch it. Is that because NOIBT_SUBROUTINE_SAFE matches the SUBROUTINE_SAFE suffix? That should be fixed.

We can actually check the full theorem name, not just the suffix. It should be possible to derive the theorem names from the file names - we should enforce that and adjust theorem names where needed.

Comment thread scripts/lint Outdated
Comment on lines +308 to +309
if [[ $arch == "x86_64" && ${routine} == "mlkem_rej_uniform" ]]; then
suffixes=("CORRECT")
Copy link
Copy Markdown
Contributor

@mkannwischer mkannwischer Apr 3, 2026

Choose a reason for hiding this comment

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

Why is there this exceptions? There are memory safety proofs for this routine?

mkannwischer
mkannwischer reviewed Apr 3, 2026
View reviewed changes
Comment thread proofs/hol_light/aarch64/proofs/mlkem_rej_uniform.ml Outdated
(* ========================================================================= *)

let MLKEM_REJ_UNIFORM_MEMSAFE = prove
let MLKEM_REJ_UNIFORM_SAFE = prove
Copy link
Copy Markdown
Contributor

@mkannwischer mkannwischer Apr 3, 2026

Choose a reason for hiding this comment

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

This was intentionally named this way and I would prefer to keep it like that because we do not have any constant time proofs at this time.
Can you implement it as: if mlkem_rej_uniform then MEMSAFE else SAFE? That would be better, I believe.

@mkannwischer
Copy link
Copy Markdown
Contributor

mkannwischer commented Apr 12, 2026

@L-series, gentle ping. Could you please adjust this PR so we can get this merged?

@mkannwischer
Copy link
Copy Markdown
Contributor

mkannwischer commented Apr 22, 2026

@L-series, are you still working on this?

@mkannwischer
Copy link
Copy Markdown
Contributor

mkannwischer commented May 3, 2026

@L-series, do you expect to finish this PR soon?

@L-series
testing: HOL-Light: add support for cross-proofing
66a7ccf 
This commit introduces a new flag --arch to the hol_light command of the
tests script that allows user specification of which architecture to
run/list the proofs for. If not passed, the behavior is unchanged.

Signed-off-by: Andreas Hatziiliou <andreas.hatziiliou@savoirfairelinux.com>
@L-series
Copy link
Copy Markdown
Contributor Author

L-series commented May 20, 2026

@L-series, do you expect to finish this PR soon?

Apologies for the long delay, I was away traveling this last month. I just pushed some changes and I've reworked check-theorems to derive the expected theorem prefix directly
from the filename (strip _aarch64_asm / _avx2_asm, uppercase, prepend MLKEM_ for
non-keccak) and grep for the fully-qualified theorem name. The only conditional is MEMSAFE
instead of SAFE for rej_uniform_*, per your earlier comment.

However, I just wanted to make sure that this is okay with you as it would require renaming around 15 proofs.

@mkannwischer
Copy link
Copy Markdown
Contributor

mkannwischer commented May 20, 2026 •
edited
Loading

@L-series, do you expect to finish this PR soon?

Apologies for the long delay, I was away traveling this last month. I just pushed some changes and I've reworked check-theorems to derive the expected theorem prefix directly from the filename (strip _aarch64_asm / _avx2_asm, uppercase, prepend MLKEM_ for non-keccak) and grep for the fully-qualified theorem name. The only conditional is MEMSAFE instead of SAFE for rej_uniform_*, per your earlier comment.

However, I just wanted to make sure that this is okay with you as it would require renaming around 15 proofs.

Thanks for picking this upa gain @L-series! Welcome back!
Renaming theorems to be uniform is no problem.

@L-series
lint: verify that all expected theorems are present
318c17a 
We add a check to the linting script called check-theorems that ensures that all HOL-Light
proofs provide the expected set of theorems depending on the
architecture.

Signed-off-by: Andreas Hatziiliou <andreas.hatziiliou@savoirfairelinux.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@mkannwischer mkannwischer mkannwischer requested changes

Requested changes must be addressed to merge this pull request.

Assignees

@mkannwischer mkannwischer

Labels

needs-mldsa-native-port

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@L-series @oqs-bot @mkannwischer