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)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`mlk_ntt_layer`	⚠️	42s	27s	+56%

Full Results (191 proofs)

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

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

CBMC Results (ML-KEM-512)

Full Results (191 proofs)

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

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

CBMC Results (ML-KEM-1024)

Full Results (191 proofs)

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

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!

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

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

mkannwischer · 2026-04-22T01:47:02Z

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

mkannwischer · 2026-05-03T04:24:18Z

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

L-series · 2026-05-20T01:01:00Z

@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 · 2026-05-20T03:15:27Z

@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.

mkannwischer · 2026-05-26T08:23:01Z

@L-series, is this ready for review? Thanks for the work!

L-series · 2026-05-26T13:50:38Z

@mkannwischer Yes it is! Please let me know if the renaming scheme is appropriate. Given that the HOL proofing CI is passing I assume I didn't break any of the proofs 😅

hanno-becker · 2026-05-28T10:16:43Z

+        if ! grep -qE "^[[:space:]]*let ${theorem}[[:space:]]+=[[:space:]]+(time[[:space:]]+)?prove" "$file"; then
+          gh_error "${routine}" "" "Missing theorem" "${file}: ${theorem} not found"
+          success=false


Suggestion: Can we complement list_proofs.sh by list_thms.sh which runs this grep and emits all (so-declared) theorems? I'd like to have a little logic as possible in lint itself.

I don't think this is done yet, is it?

hanno-becker · 2026-05-28T10:18:07Z

+      local expected=(
+        "${prefix}_CORRECT"
+        "${prefix}_SUBROUTINE_CORRECT"
+        "${prefix}_SUBROUTINE_${safe}"
+      )
+      if [[ $arch == "x86_64" ]]; then
+        expected+=(
+          "${prefix}_${safe}"
+          "${prefix}_NOIBT_SUBROUTINE_CORRECT"
+          "${prefix}_NOIBT_SUBROUTINE_${safe}"
+        )
+      fi


It would be nice to make this logic and exception more prominent... I wonder if one could define this in some TOML/YAML in proofs/{arch}... not sure if it's worth it. Ideas?

Hmm.. I think the advantages of such a move are twofold:

It would make the maintaining the naming conventions and exceptions such as rej_uniform simpler and more visible as they are in the same directory as the proofs.

It could be useful if there are any ideas to reuse or refer to the naming conventions elsewhere in the project.

However, if the sole use is within the linting script for CI, I think that it would be preferable to keep it as is as we would not have to add any additional files or TOML/YAML parsing logic.

L-series

I just realized that the comments I had written many weeks ago as well as last week which were labelled "pending", were in a "pending to be submitted" not a "pending to be reviewed" state. I wasn't aware that one had to submit the comments through the files changed page 😓

L-series · 2026-06-02T13:40:25Z

+        if ! grep -qE "^[[:space:]]*let ${theorem}[[:space:]]+=[[:space:]]+(time[[:space:]]+)?prove" "$file"; then
+          gh_error "${routine}" "" "Missing theorem" "${file}: ${theorem} not found"
+          success=false


L-series · 2026-06-02T14:12:14Z

+      local expected=(
+        "${prefix}_CORRECT"
+        "${prefix}_SUBROUTINE_CORRECT"
+        "${prefix}_SUBROUTINE_${safe}"
+      )
+      if [[ $arch == "x86_64" ]]; then
+        expected+=(
+          "${prefix}_${safe}"
+          "${prefix}_NOIBT_SUBROUTINE_CORRECT"
+          "${prefix}_NOIBT_SUBROUTINE_${safe}"
+        )
+      fi


Hmm.. I think the advantages of such a move are twofold:

It would make the maintaining the naming conventions and exceptions such as rej_uniform simpler and more visible as they are in the same directory as the proofs.

It could be useful if there are any ideas to reuse or refer to the naming conventions elsewhere in the project.

However, if the sole use is within the linting script for CI, I think that it would be preferable to keep it as is as we would not have to add any additional files or TOML/YAML parsing logic.

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>

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 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

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

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

Comment thread scripts/lint Outdated

Comment thread scripts/lint Outdated

mkannwischer reviewed Apr 3, 2026

View reviewed changes

Comment thread proofs/hol_light/aarch64/proofs/mlkem_rej_uniform.ml Outdated

L-series force-pushed the HOL-Light-CI branch from 3226ad6 to c6c4c85 Compare May 20, 2026 00:52

L-series force-pushed the HOL-Light-CI branch from c6c4c85 to 858f60c Compare May 20, 2026 01:03

L-series force-pushed the HOL-Light-CI branch 2 times, most recently from 318c17a to ac97d80 Compare May 25, 2026 14:53

L-series force-pushed the HOL-Light-CI branch 3 times, most recently from 8a3f6d0 to a583d82 Compare May 27, 2026 15:42

hanno-becker reviewed May 28, 2026

View reviewed changes

L-series force-pushed the HOL-Light-CI branch from a583d82 to d799dc5 Compare June 2, 2026 14:12

L-series commented Jun 4, 2026

View reviewed changes

L-series added 2 commits June 10, 2026 11:00

L-series force-pushed the HOL-Light-CI branch from d799dc5 to e6a3e47 Compare June 10, 2026 15:00

L-series requested a review from hanno-becker June 10, 2026 17:06

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!

Uh oh!

L-series commented Apr 3, 2026

Uh oh!

mkannwischer left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mkannwischer commented Apr 12, 2026

Uh oh!

mkannwischer commented Apr 22, 2026

Uh oh!

mkannwischer commented May 3, 2026

Uh oh!

L-series commented May 20, 2026

Uh oh!

mkannwischer commented May 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mkannwischer commented May 26, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

L-series commented May 26, 2026

Uh oh!

hanno-becker May 28, 2026

Choose a reason for hiding this comment

Uh oh!

L-series Jun 2, 2026

Choose a reason for hiding this comment

Uh oh!

mkannwischer Jun 16, 2026

Choose a reason for hiding this comment

Uh oh!

hanno-becker May 28, 2026

Choose a reason for hiding this comment

Uh oh!

L-series Jun 2, 2026

Choose a reason for hiding this comment

Uh oh!

L-series left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

L-series Jun 2, 2026

Choose a reason for hiding this comment

Uh oh!

L-series Jun 2, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

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

mkannwischer commented May 20, 2026 •

edited

Loading

mkannwischer commented May 26, 2026 •

edited

Loading