nix: Use HOL-Light from nixpkgs by mkannwischer · Pull Request #1712 · pq-code-package/mlkem-native

mkannwischer · 2026-05-30T11:59:55Z

I'm trying to upstream the latest HOL-Light to make it useable for us here: hol_light: build against the default OCaml (5.4) NixOS/nixpkgs#525966

oqs-bot · 2026-05-30T12:58:53Z

CBMC Results (ML-KEM-512)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`mlk_poly_reduce_native`	⚠️	37s	19s	+95%
`mlk_poly_rej_uniform`	⚠️	135s	32s	+322%

Full Results (191 proofs)

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

oqs-bot · 2026-05-30T12:58:55Z

CBMC Results (ML-KEM-768)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`mlk_poly_reduce_native`	⚠️	34s	21s	+62%
`mlk_poly_rej_uniform`	⚠️	149s	33s	+352%
`poly_ntt_native`	⚠️	41s	26s	+58%

Full Results (191 proofs)

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

oqs-bot · 2026-05-30T12:59:37Z

CBMC Results (ML-KEM-1024)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`mlk_poly_rej_uniform`	⚠️	141s	35s	+303%
`poly_ntt_native`	⚠️	42s	28s	+50%

Full Results (191 proofs)

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

Update the nixpkgs input from nixos-25.11 to nixos-26.05 and adjust the flake to the new package set: - Default gcc changed from 14.3.0 to 15.2.0 - slothy: use the new pkgs.slothy from nixpkgs instead of the custom build; nix/slothy/default.nix now just re-exports it with a commented override for pinning a specific upstream revision. Drops the python3-for-slothy (unstable ortools) workaround. - hol_light: nixpkgs pins hol_light to the non-default OCaml 5.3 set (5.4.1 is the 26.05 default) and downgrades camlp5 to 8.03.2, which is not in the binary cache. Build against the default 5.4 set with the cached default camlp5 8.05.01 instead, and add patch 0007 so the pa_j chooser accepts camlp5 8.05 (mapped to pa_j_5.4_8.04.00.ml). - python: provide script dependencies (pyparsing, sympy, ...) via python3.withPackages instead of bare python3Packages entries in a symlinkJoin, which no longer reach sys.path. Fixes autogen's "No module named 'pyparsing'". - autogen: use the snake_case pyparsing API (parse_string/parse_all) to silence the deprecation warning from the newer pyparsing. - cbmc: bitwuzla version 0.8.2 -> 0.9.0. - autogen: Reformatted with newer ruff version - platform tests: Increase disk on x86 from 20 GiB to 30 GiB as nix derivation does not fit anymore otherwise. - clang 18: Clang 18 from 26.05 no longer compiles on MacOS - take it from the 24.05 channel instead. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

mkannwischer · 2026-06-02T03:20:15Z

My upstream changes have been merged and backported to 26.05, so we can include the changes in #1711.

mkannwischer force-pushed the hol-light-from-nixpkgs branch from 4b396e9 to 3c6a5db Compare May 30, 2026 13:57

mkannwischer mentioned this pull request May 30, 2026

hol_light: build against the default OCaml (5.4) NixOS/nixpkgs#525966

Merged

14 tasks

mkannwischer force-pushed the hol-light-from-nixpkgs branch from 3c6a5db to d0e0eb5 Compare May 30, 2026 14:28

nix: use hol_light from nixpkgs instead of a local override

e64d34d

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

mkannwischer force-pushed the hol-light-from-nixpkgs branch from d0e0eb5 to e64d34d Compare May 30, 2026 14:47

mkannwischer closed this Jun 2, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

nix: Use HOL-Light from nixpkgs#1712

nix: Use HOL-Light from nixpkgs#1712
mkannwischer wants to merge 2 commits into
mainfrom
hol-light-from-nixpkgs

mkannwischer commented May 30, 2026 •

edited

Loading

Uh oh!

oqs-bot commented May 30, 2026 •

edited

Loading

Uh oh!

oqs-bot commented May 30, 2026 •

edited

Loading

Uh oh!

oqs-bot commented May 30, 2026 •

edited

Loading

Uh oh!

mkannwischer commented Jun 2, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

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

Uh oh!

Uh oh!

oqs-bot commented May 30, 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 May 30, 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 May 30, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-KEM-1024)

Uh oh!

mkannwischer commented Jun 2, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

mkannwischer commented May 30, 2026 •

edited

Loading

oqs-bot commented May 30, 2026 •

edited

Loading

oqs-bot commented May 30, 2026 •

edited

Loading

oqs-bot commented May 30, 2026 •

edited

Loading