HOL-Light: improve tooling and CI by L-series · Pull Request #1634 · pq-code-package/mlkem-native

L-series · 2026-03-20T02:46:28Z

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 · 2026-03-20T03:07:30Z

CBMC Results (ML-KEM-768)

Full Results (187 proofs)

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

oqs-bot · 2026-03-20T03:07:42Z

CBMC Results (ML-KEM-512)

Full Results (187 proofs)

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

oqs-bot · 2026-03-20T03:09:49Z

CBMC Results (ML-KEM-1024)

Full Results (187 proofs)

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

L-series · 2026-03-23T14:17:26Z

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

mkannwischer

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!

scripts/tests

scripts/check-theorems

.github/workflows/hol_light.yml

scripts/check-theorems

mkannwischer · 2026-04-02T09:33:45Z

scripts/check-theorems

+  [[ $ARCH == "x86_64" && $routine == "mlkem_rej_uniform" ]] && suffixes=("CORRECT")
+
+  for sfx in "${suffixes[@]}"; do
+    if ! grep -q "_${sfx}" "$PROOFS_DIR/${routine}.ml"; then


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

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?

This commit introduces two new flags to the hol_light command of the tests script. The first allows user specification of which architecture to run/list the proofs for and the second allows for entering the nix cross-compilation devshell for that architecture. If either are not passed, the behavior is unchanged. Signed-off-by: Andreas Hatziiliou <andreas.hatziiliou@savoirfairelinux.com>

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>

L-series · 2026-04-03T02:14:06Z

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

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

Two comments still need to be addressed. Thank you!

mkannwischer · 2026-04-03T02:51:58Z

scripts/lint

+      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")


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.

mkannwischer · 2026-04-03T02:56:20Z

scripts/lint

+      if [[ $arch == "x86_64" && ${routine} == "mlkem_rej_uniform" ]]; then
+        suffixes=("CORRECT")


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

mkannwischer · 2026-04-03T03:02:43Z

proofs/hol_light/aarch64/proofs/mlkem_rej_uniform.ml

 (* ========================================================================= *)

-let MLKEM_REJ_UNIFORM_MEMSAFE = prove
+let MLKEM_REJ_UNIFORM_SAFE = prove


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 · 2026-04-12T15:41:56Z

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

L-series force-pushed the HOL-Light-CI branch from 5465c5d to 57f5402 Compare March 20, 2026 02:48

L-series changed the title ~~HOL-Light: improve tooling and CI"~~ HOL-Light: improve tooling and CI Mar 20, 2026

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 marked this pull request as ready for review March 23, 2026 14:16

L-series requested a review from a team as a code owner March 23, 2026 14:16

L-series force-pushed the HOL-Light-CI branch 2 times, most recently from 25cad96 to 3e258d8 Compare March 23, 2026 14:55

mkannwischer added the needs-mldsa-native-port label Mar 25, 2026

L-series mentioned this pull request Apr 1, 2026

HOL-Light: improve tooling and CI pq-code-package/mldsa-native#1009

Draft

mkannwischer self-assigned this Apr 2, 2026

mkannwischer requested changes Apr 2, 2026

View reviewed changes

L-series added 2 commits April 2, 2026 21:00

L-series force-pushed the HOL-Light-CI branch from 3e258d8 to 3226ad6 Compare April 3, 2026 01:54

mkannwischer requested changes Apr 3, 2026

View reviewed changes

mkannwischer reviewed Apr 3, 2026

View reviewed changes

		if [[ $arch == "x86_64" && ${routine} == "mlkem_rej_uniform" ]]; then
		suffixes=("CORRECT")

Conversation

L-series commented Mar 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

oqs-bot commented Mar 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-KEM-768)

Uh oh!

oqs-bot commented Mar 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-KEM-512)

Uh oh!

oqs-bot commented Mar 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-KEM-1024)

Uh oh!

L-series commented Mar 23, 2026

Uh oh!

mkannwischer left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mkannwischer Apr 2, 2026

Choose a reason for hiding this comment

Uh oh!

L-series Apr 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

L-series commented Apr 3, 2026

Uh oh!

mkannwischer left a comment

Choose a reason for hiding this comment

Uh oh!

mkannwischer Apr 3, 2026

Choose a reason for hiding this comment

Uh oh!

mkannwischer Apr 3, 2026

Choose a reason for hiding this comment

Uh oh!

mkannwischer Apr 3, 2026

Choose a reason for hiding this comment

Uh oh!

mkannwischer commented Apr 12, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

L-series commented Mar 20, 2026 •

edited

Loading

oqs-bot commented Mar 20, 2026 •

edited

Loading

oqs-bot commented Mar 20, 2026 •

edited

Loading

oqs-bot commented Mar 20, 2026 •

edited

Loading

L-series Apr 3, 2026 •

edited

Loading