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

L-series · 2026-04-01T15:53:43Z

This PR is a port from: pq-code-package/mlkem-native#1634

Note that this is currently blocked by: #1001

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

Add the check-theorems script to the HOL-Light CI action. Fail the CI if any of the required proofs are not present. Signed-off-by: Andreas Hatziiliou <andreas.hatziiliou@savoirfairelinux.com>

oqs-bot · 2026-04-01T16:11:46Z

CBMC Results (ML-DSA-44)

Full Results (177 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	2004s	2066s	-3.0%
`mld_attempt_signature_generation`	✅	228s	234s	-3%
`polyvecl_pointwise_acc_montgomery_c`	✅	211s	233s	-9%
`poly_pointwise_montgomery_c`	✅	155s	162s	-4%
`rej_uniform_native`	✅	139s	145s	-4%
`sign_verify_internal`	✅	125s	127s	-2%
`mld_invntt_layer`	✅	89s	86s	+3%
`mld_ct_memcmp`	✅	73s	82s	-11%
`mld_ntt_layer`	✅	54s	57s	-5%
`keccak_squeezeblocks_x4`	✅	41s	42s	-2%
`sign_signature_internal`	✅	31s	33s	-6%
`polyvec_matrix_expand`	✅	27s	28s	-4%
`fqmul`	✅	21s	21s	+0%
`poly_chknorm_c`	✅	20s	23s	-13%
`rej_uniform`	✅	19s	22s	-14%
`polyeta_unpack`	✅	18s	18s	+0%
`poly_uniform_eta_4x`	✅	17s	18s	-6%
`polyt0_unpack`	✅	15s	17s	-12%
`rej_uniform_c`	✅	15s	18s	-17%
`poly_uniform_4x`	✅	14s	14s	+0%
`polymat_permute_bitrev_to_custom`	✅	14s	16s	-12%
`polyveck_power2round`	✅	14s	14s	+0%
`mld_compute_t0_t1_tr_from_sk_components`	✅	13s	13s	+0%
`keccakf1600x4_permute_native`	✅	12s	12s	+0%
`mld_ntt_butterfly_block`	✅	12s	14s	-14%
`polyvec_matrix_expand_serial`	✅	12s	11s	+9%
`polyz_unpack_c`	✅	12s	11s	+9%
`poly_add`	✅	11s	13s	-15%
`polyvec_matrix_pointwise_montgomery`	✅	11s	15s	-27%
`keccak_absorb_once_x4`	✅	10s	10s	+0%
`polyveck_ntt`	✅	9s	4s	+125%
`keccak_absorb`	✅	8s	9s	-11%
`keccakf1600_permute_native`	✅	8s	7s	+14%
`mld_polyvecl_permute_bitrev_to_custom_native`	✅	8s	10s	-20%
`poly_uniform_gamma1_4x`	✅	8s	4s	+100%
`sign_pk_from_sk`	✅	8s	7s	+14%
`keccakf1600_permute`	✅	7s	7s	+0%
`mld_check_pct`	✅	7s	8s	-12%
`mld_compute_pack_z`	✅	7s	6s	+17%
`mld_sample_s1_s2_serial`	✅	7s	5s	+40%
`polyveck_decompose`	✅	7s	7s	+0%
`sign`	✅	7s	7s	+0%
`unpack_hints`	✅	7s	6s	+17%
`keccak_squeeze`	✅	6s	4s	+50%
`mld_sample_s1_s2`	✅	6s	3s	+100%
`poly_caddq_c`	✅	6s	6s	+0%
`poly_challenge`	✅	6s	5s	+20%
`poly_chknorm_native_aarch64`	✅	6s	3s	+100%
`polyveck_add`	✅	6s	5s	+20%
`polyveck_use_hint`	✅	6s	5s	+20%
`sign_signature_extmu`	✅	6s	3s	+100%
`caddq`	✅	5s	5s	+0%
`mld_h`	✅	5s	6s	-17%
`mld_prepare_domain_separation_prefix`	✅	5s	6s	-17%
`poly_caddq_native_aarch64`	✅	5s	3s	+67%
`poly_decompose_c`	✅	5s	3s	+67%
`poly_invntt_tomont_c`	✅	5s	7s	-29%
`poly_ntt`	✅	5s	4s	+25%
`poly_ntt_c`	✅	5s	3s	+67%
`poly_shiftl`	✅	5s	4s	+25%
`poly_uniform`	✅	5s	5s	+0%
`poly_uniform_eta`	✅	5s	5s	+0%
`poly_use_hint_c`	✅	5s	5s	+0%
`polyveck_caddq`	✅	5s	7s	-29%
`polyveck_chknorm`	✅	5s	7s	-29%
`polyveck_shiftl`	✅	5s	6s	-17%
`polyveck_sub`	✅	5s	4s	+25%
`polyvecl_chknorm`	✅	5s	3s	+67%
`polyvecl_ntt`	✅	5s	3s	+67%
`polyvecl_pointwise_acc_montgomery_native`	✅	5s	7s	-29%
`polyvecl_unpack_eta`	✅	5s	3s	+67%
`polyvecl_unpack_z`	✅	5s	3s	+67%
`polyw1_pack`	✅	5s	3s	+67%
`shake128_absorb`	✅	5s	2s	+150%
`sign_open`	✅	5s	5s	+0%
`sign_signature`	✅	5s	2s	+150%
`sign_signature_pre_hash_shake256`	✅	5s	2s	+150%
`sign_verify_extmu`	✅	5s	5s	+0%
`unpack_pk`	✅	5s	2s	+150%
`decompose`	✅	4s	4s	+0%
`intt_native_x86_64`	✅	4s	5s	-20%
`keccakf1600_extract_bytes (big endian)`	✅	4s	4s	+0%
`keccakf1600_xor_bytes`	✅	4s	4s	+0%
`keccakf1600x4_extract_bytes`	✅	4s	2s	+100%
`mld_ct_abs_i32`	✅	4s	3s	+33%
`mld_ct_cmask_nonzero_u32`	✅	4s	3s	+33%
`mld_keccakf1600_extract_bytes`	✅	4s	3s	+33%
`pack_pk`	✅	4s	7s	-43%
`pack_sig_c_h`	✅	4s	2s	+100%
`pack_sig_z`	✅	4s	3s	+33%
`pack_sk`	✅	4s	2s	+100%
`poly_chknorm`	✅	4s	2s	+100%
`poly_invntt_tomont_native`	✅	4s	4s	+0%
`poly_make_hint`	✅	4s	2s	+100%
`poly_pointwise_montgomery_native`	✅	4s	4s	+0%
`poly_reduce`	✅	4s	4s	+0%
`polyt1_pack`	✅	4s	2s	+100%
`polyveck_make_hint`	✅	4s	2s	+100%
`polyveck_pack_w1`	✅	4s	3s	+33%
`polyveck_pointwise_poly_montgomery`	✅	4s	4s	+0%
`polyveck_unpack_eta`	✅	4s	3s	+33%
`polyvecl_pack_eta`	✅	4s	6s	-33%
`polyvecl_permute_bitrev_to_custom`	✅	4s	3s	+33%
`polyvecl_uniform_gamma1`	✅	4s	3s	+33%
`polyvecl_uniform_gamma1_serial`	✅	4s	4s	+0%
`power2round`	✅	4s	2s	+100%
`rej_eta_native`	✅	4s	4s	+0%
`shake256`	✅	4s	2s	+100%
`sign_verify`	✅	4s	7s	-43%
`sign_verify_pre_hash_shake256`	✅	4s	3s	+33%
`unpack_sk`	✅	4s	5s	-20%
`use_hint`	✅	4s	4s	+0%
`keccak_init`	✅	3s	2s	+50%
`keccakf1600_xor_bytes (big endian)`	✅	3s	2s	+50%
`mld_ct_cmask_neg_i32`	✅	3s	3s	+0%
`mld_ct_cmask_nonzero_u8`	✅	3s	3s	+0%
`ntt_native_aarch64`	✅	3s	3s	+0%
`poly_caddq`	✅	3s	3s	+0%
`poly_chknorm_native`	✅	3s	3s	+0%
`poly_decompose`	✅	3s	3s	+0%
`poly_invntt_tomont`	✅	3s	4s	-25%
`poly_ntt_native`	✅	3s	3s	+0%
`poly_power2round`	✅	3s	6s	-50%
`poly_uniform_gamma1`	✅	3s	3s	+0%
`polyt1_unpack`	✅	3s	5s	-40%
`polyveck_invntt_tomont`	✅	3s	3s	+0%
`polyveck_pack_eta`	✅	3s	3s	+0%
`polyveck_reduce`	✅	3s	5s	-40%
`polyveck_unpack_t0`	✅	3s	5s	-40%
`polyvecl_pointwise_acc_montgomery`	✅	3s	3s	+0%
`polyz_unpack`	✅	3s	6s	-50%
`rej_eta_c`	✅	3s	4s	-25%
`shake128_init`	✅	3s	2s	+50%
`shake128_release`	✅	3s	4s	-25%
`shake128x4_squeezeblocks`	✅	3s	2s	+50%
`shake256_finalize`	✅	3s	3s	+0%
`shake256_init`	✅	3s	2s	+50%
`shake256x4_squeezeblocks`	✅	3s	1s	+200%
`sign_keypair`	✅	3s	3s	+0%
`sign_signature_pre_hash_internal`	✅	3s	4s	-25%
`sign_verify_pre_hash_internal`	✅	3s	3s	+0%
`fqscale`	✅	2s	3s	-33%
`keccak_finalize`	✅	2s	2s	+0%
`keccakf1600x4_permute`	✅	2s	5s	-60%
`make_hint`	✅	2s	2s	+0%
`mld_ct_get_optblocker_u32`	✅	2s	2s	+0%
`mld_ct_get_optblocker_u8`	✅	2s	2s	+0%
`mld_ct_sel_int32`	✅	2s	2s	+0%
`mld_value_barrier_i64`	✅	2s	2s	+0%
`montgomery_reduce`	✅	2s	3s	-33%
`ntt_native_x86_64`	✅	2s	2s	+0%
`poly_caddq_native`	✅	2s	4s	-50%
`poly_decompose_native`	✅	2s	3s	-33%
`poly_pointwise_montgomery`	✅	2s	4s	-50%
`poly_sub`	✅	2s	4s	-50%
`poly_use_hint`	✅	2s	2s	+0%
`poly_use_hint_native`	✅	2s	2s	+0%
`polyeta_pack`	✅	2s	4s	-50%
`polyt0_pack`	✅	2s	4s	-50%
`polyveck_pack_t0`	✅	2s	4s	-50%
`polyz_unpack_native`	✅	2s	3s	-33%
`rej_eta`	✅	2s	2s	+0%
`shake128_finalize`	✅	2s	2s	+0%
`shake128x4_absorb_once`	✅	2s	2s	+0%
`shake256_absorb`	✅	2s	2s	+0%
`shake256_squeeze`	✅	2s	2s	+0%
`shake256x4_absorb_once`	✅	2s	2s	+0%
`sign_keypair_internal`	✅	2s	5s	-60%
`sys_check_capability`	✅	2s	3s	-33%
`unpack_sig`	✅	2s	2s	+0%
`keccakf1600x4_xor_bytes`	✅	1s	3s	-67%
`mld_ct_get_optblocker_i64`	✅	1s	3s	-67%
`mld_value_barrier_u32`	✅	1s	2s	-50%
`mld_value_barrier_u8`	✅	1s	5s	-80%
`polyz_pack`	✅	1s	3s	-67%
`reduce32`	✅	1s	3s	-67%
`shake128_squeeze`	✅	1s	3s	-67%
`shake256_release`	✅	1s	2s	-50%

oqs-bot · 2026-04-01T16:14:17Z

CBMC Results (ML-DSA-65)

Full Results (177 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	2699s	2488s	+8.5%
`sign_verify_internal`	✅	369s	341s	+8%
`mld_attempt_signature_generation`	✅	293s	278s	+5%
`polyvecl_pointwise_acc_montgomery_c`	✅	227s	190s	+19%
`poly_pointwise_montgomery_c`	✅	184s	160s	+15%
`rej_uniform_native`	✅	158s	145s	+9%
`polyvec_matrix_expand`	✅	136s	128s	+6%
`mld_invntt_layer`	✅	106s	96s	+10%
`mld_ct_memcmp`	✅	84s	77s	+9%
`polyvec_matrix_expand_serial`	✅	71s	70s	+1%
`mld_ntt_layer`	✅	60s	54s	+11%
`keccak_squeezeblocks_x4`	✅	45s	42s	+7%
`sign_signature_internal`	✅	39s	37s	+5%
`polymat_permute_bitrev_to_custom`	✅	31s	29s	+7%
`mld_compute_t0_t1_tr_from_sk_components`	✅	27s	27s	+0%
`rej_uniform`	✅	24s	23s	+4%
`fqmul`	✅	23s	18s	+28%
`poly_chknorm_c`	✅	21s	22s	-5%
`rej_uniform_c`	✅	20s	17s	+18%
`poly_uniform_eta_4x`	✅	18s	16s	+12%
`poly_uniform_4x`	✅	17s	15s	+13%
`polyt0_unpack`	✅	17s	14s	+21%
`keccakf1600x4_permute_native`	✅	15s	13s	+15%
`polyveck_decompose`	✅	14s	14s	+0%
`mld_ntt_butterfly_block`	✅	13s	13s	+0%
`poly_add`	✅	13s	11s	+18%
`polyveck_add`	✅	13s	7s	+86%
`polyvecl_chknorm`	✅	13s	13s	+0%
`polyvec_matrix_pointwise_montgomery`	✅	12s	11s	+9%
`keccak_absorb_once_x4`	✅	11s	9s	+22%
`polyveck_sub`	✅	11s	10s	+10%
`mld_compute_pack_z`	✅	10s	8s	+25%
`polyveck_power2round`	✅	10s	11s	-9%
`keccak_absorb`	✅	9s	7s	+29%
`keccakf1600_permute_native`	✅	9s	9s	+0%
`mld_polyvecl_permute_bitrev_to_custom_native`	✅	9s	8s	+12%
`polyveck_invntt_tomont`	✅	9s	10s	-10%
`polyveck_ntt`	✅	9s	11s	-18%
`polyveck_reduce`	✅	9s	6s	+50%
`polyveck_shiftl`	✅	9s	8s	+12%
`sign_pk_from_sk`	✅	9s	7s	+29%
`keccakf1600_permute`	✅	8s	10s	-20%
`poly_caddq_c`	✅	8s	4s	+100%
`poly_invntt_tomont_c`	✅	8s	10s	-20%
`polyveck_use_hint`	✅	8s	8s	+0%
`mld_sample_s1_s2`	✅	7s	6s	+17%
`poly_decompose_c`	✅	7s	7s	+0%
`poly_power2round`	✅	7s	4s	+75%
`poly_uniform_eta`	✅	7s	6s	+17%
`polyveck_caddq`	✅	7s	7s	+0%
`polyveck_pointwise_poly_montgomery`	✅	7s	6s	+17%
`polyvecl_ntt`	✅	7s	8s	-12%
`sign_keypair_internal`	✅	7s	6s	+17%
`mld_h`	✅	6s	5s	+20%
`poly_chknorm_native`	✅	6s	3s	+100%
`polyeta_unpack`	✅	6s	6s	+0%
`polyveck_make_hint`	✅	6s	6s	+0%
`rej_eta`	✅	6s	2s	+200%
`rej_eta_c`	✅	6s	4s	+50%
`sign`	✅	6s	8s	-25%
`sign_signature_pre_hash_internal`	✅	6s	4s	+50%
`sign_signature_pre_hash_shake256`	✅	6s	5s	+20%
`unpack_hints`	✅	6s	6s	+0%
`intt_native_x86_64`	✅	5s	3s	+67%
`keccakf1600_extract_bytes (big endian)`	✅	5s	3s	+67%
`keccakf1600x4_xor_bytes`	✅	5s	2s	+150%
`mld_check_pct`	✅	5s	8s	-38%
`mld_ct_cmask_nonzero_u32`	✅	5s	3s	+67%
`mld_ct_cmask_nonzero_u8`	✅	5s	3s	+67%
`mld_prepare_domain_separation_prefix`	✅	5s	7s	-29%
`mld_sample_s1_s2_serial`	✅	5s	6s	-17%
`poly_ntt`	✅	5s	4s	+25%
`poly_uniform`	✅	5s	2s	+150%
`poly_uniform_gamma1`	✅	5s	4s	+25%
`poly_use_hint`	✅	5s	3s	+67%
`polyeta_pack`	✅	5s	2s	+150%
`polyt0_pack`	✅	5s	5s	+0%
`polyt1_unpack`	✅	5s	4s	+25%
`polyveck_chknorm`	✅	5s	5s	+0%
`polyvecl_pointwise_acc_montgomery_native`	✅	5s	3s	+67%
`polyvecl_unpack_z`	✅	5s	3s	+67%
`rej_eta_native`	✅	5s	4s	+25%
`shake128_absorb`	✅	5s	2s	+150%
`sign_signature`	✅	5s	6s	-17%
`sign_verify`	✅	5s	4s	+25%
`sign_verify_extmu`	✅	5s	3s	+67%
`sign_verify_pre_hash_internal`	✅	5s	6s	-17%
`unpack_pk`	✅	5s	3s	+67%
`mld_ct_abs_i32`	✅	4s	2s	+100%
`mld_ct_cmask_neg_i32`	✅	4s	1s	+300%
`pack_pk`	✅	4s	3s	+33%
`poly_challenge`	✅	4s	5s	-20%
`poly_decompose_native`	✅	4s	5s	-20%
`poly_uniform_gamma1_4x`	✅	4s	3s	+33%
`polyt1_pack`	✅	4s	3s	+33%
`polyveck_unpack_eta`	✅	4s	5s	-20%
`polyvecl_unpack_eta`	✅	4s	4s	+0%
`polyz_pack`	✅	4s	3s	+33%
`polyz_unpack`	✅	4s	2s	+100%
`power2round`	✅	4s	1s	+300%
`shake128x4_absorb_once`	✅	4s	3s	+33%
`shake256_squeeze`	✅	4s	4s	+0%
`sign_open`	✅	4s	5s	-20%
`sign_signature_extmu`	✅	4s	4s	+0%
`sign_verify_pre_hash_shake256`	✅	4s	5s	-20%
`unpack_sk`	✅	4s	6s	-33%
`use_hint`	✅	4s	4s	+0%
`fqscale`	✅	3s	3s	+0%
`keccak_squeeze`	✅	3s	4s	-25%
`make_hint`	✅	3s	2s	+50%
`mld_ct_get_optblocker_i64`	✅	3s	2s	+50%
`mld_ct_get_optblocker_u8`	✅	3s	2s	+50%
`mld_value_barrier_u32`	✅	3s	3s	+0%
`mld_value_barrier_u8`	✅	3s	3s	+0%
`ntt_native_x86_64`	✅	3s	4s	-25%
`pack_sk`	✅	3s	5s	-40%
`poly_caddq_native`	✅	3s	3s	+0%
`poly_caddq_native_aarch64`	✅	3s	4s	-25%
`poly_chknorm_native_aarch64`	✅	3s	4s	-25%
`poly_invntt_tomont`	✅	3s	2s	+50%
`poly_invntt_tomont_native`	✅	3s	4s	-25%
`poly_ntt_c`	✅	3s	3s	+0%
`poly_ntt_native`	✅	3s	2s	+50%
`poly_pointwise_montgomery_native`	✅	3s	4s	-25%
`poly_reduce`	✅	3s	2s	+50%
`poly_use_hint_c`	✅	3s	3s	+0%
`poly_use_hint_native`	✅	3s	3s	+0%
`polyveck_pack_eta`	✅	3s	4s	-25%
`polyveck_pack_t0`	✅	3s	4s	-25%
`polyveck_pack_w1`	✅	3s	4s	-25%
`polyveck_unpack_t0`	✅	3s	3s	+0%
`polyvecl_uniform_gamma1`	✅	3s	2s	+50%
`polyvecl_uniform_gamma1_serial`	✅	3s	5s	-40%
`polyw1_pack`	✅	3s	4s	-25%
`polyz_unpack_c`	✅	3s	2s	+50%
`reduce32`	✅	3s	2s	+50%
`shake128_init`	✅	3s	1s	+200%
`shake128_squeeze`	✅	3s	4s	-25%
`shake256`	✅	3s	2s	+50%
`shake256_finalize`	✅	3s	2s	+50%
`shake256_init`	✅	3s	3s	+0%
`shake256_release`	✅	3s	3s	+0%
`shake256x4_absorb_once`	✅	3s	4s	-25%
`sign_keypair`	✅	3s	2s	+50%
`caddq`	✅	2s	3s	-33%
`decompose`	✅	2s	3s	-33%
`keccak_init`	✅	2s	1s	+100%
`keccakf1600_xor_bytes`	✅	2s	1s	+100%
`keccakf1600_xor_bytes (big endian)`	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes`	✅	2s	3s	-33%
`keccakf1600x4_permute`	✅	2s	4s	-50%
`mld_ct_get_optblocker_u32`	✅	2s	1s	+100%
`mld_keccakf1600_extract_bytes`	✅	2s	2s	+0%
`mld_value_barrier_i64`	✅	2s	3s	-33%
`montgomery_reduce`	✅	2s	3s	-33%
`ntt_native_aarch64`	✅	2s	3s	-33%
`pack_sig_c_h`	✅	2s	2s	+0%
`pack_sig_z`	✅	2s	3s	-33%
`poly_caddq`	✅	2s	3s	-33%
`poly_decompose`	✅	2s	3s	-33%
`poly_make_hint`	✅	2s	3s	-33%
`poly_pointwise_montgomery`	✅	2s	4s	-50%
`poly_sub`	✅	2s	4s	-50%
`polyvecl_pack_eta`	✅	2s	2s	+0%
`polyvecl_permute_bitrev_to_custom`	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery`	✅	2s	4s	-50%
`polyz_unpack_native`	✅	2s	2s	+0%
`shake128_finalize`	✅	2s	3s	-33%
`shake128_release`	✅	2s	1s	+100%
`shake256_absorb`	✅	2s	6s	-67%
`shake256x4_squeezeblocks`	✅	2s	2s	+0%
`unpack_sig`	✅	2s	2s	+0%
`keccak_finalize`	✅	1s	3s	-67%
`mld_ct_sel_int32`	✅	1s	5s	-80%
`poly_chknorm`	✅	1s	3s	-67%
`poly_shiftl`	✅	1s	3s	-67%
`shake128x4_squeezeblocks`	✅	1s	2s	-50%
`sys_check_capability`	✅	1s	1s	+0%

oqs-bot · 2026-04-01T16:14:36Z

CBMC Results (ML-DSA-87)

Full Results (177 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	2681s	2703s	-0.8%
`sign_verify_internal`	✅	327s	334s	-2%
`polyvecl_pointwise_acc_montgomery_c`	✅	281s	281s	+0%
`mld_attempt_signature_generation`	✅	237s	240s	-1%
`polyvec_matrix_expand`	✅	172s	175s	-2%
`poly_pointwise_montgomery_c`	✅	160s	158s	+1%
`rej_uniform_native`	✅	150s	146s	+3%
`mld_invntt_layer`	✅	98s	95s	+3%
`polyvec_matrix_expand_serial`	✅	83s	80s	+4%
`mld_ct_memcmp`	✅	74s	74s	+0%
`polyveck_decompose`	✅	59s	60s	-2%
`mld_ntt_layer`	✅	54s	56s	-4%
`sign_signature_internal`	✅	54s	55s	-2%
`polymat_permute_bitrev_to_custom`	✅	47s	45s	+4%
`keccak_squeezeblocks_x4`	✅	43s	42s	+2%
`mld_compute_t0_t1_tr_from_sk_components`	✅	23s	25s	-8%
`fqmul`	✅	21s	19s	+11%
`rej_uniform`	✅	21s	22s	-5%
`poly_chknorm_c`	✅	20s	19s	+5%
`polyeta_unpack`	✅	18s	17s	+6%
`poly_uniform_4x`	✅	16s	17s	-6%
`polyt0_unpack`	✅	16s	15s	+7%
`keccakf1600x4_permute_native`	✅	15s	13s	+15%
`poly_uniform_eta_4x`	✅	15s	17s	-12%
`rej_uniform_c`	✅	14s	14s	+0%
`mld_ntt_butterfly_block`	✅	13s	13s	+0%
`polyvec_matrix_pointwise_montgomery`	✅	13s	12s	+8%
`poly_add`	✅	12s	12s	+0%
`polyveck_use_hint`	✅	12s	13s	-8%
`polyveck_add`	✅	11s	9s	+22%
`polyz_unpack_c`	✅	11s	11s	+0%
`keccak_absorb_once_x4`	✅	10s	11s	-9%
`mld_polyvecl_permute_bitrev_to_custom_native`	✅	10s	14s	-29%
`polyveck_invntt_tomont`	✅	10s	8s	+25%
`polyvecl_ntt`	✅	10s	11s	-9%
`sign_pk_from_sk`	✅	10s	8s	+25%
`keccakf1600_permute`	✅	9s	9s	+0%
`keccakf1600_permute_native`	✅	9s	8s	+12%
`polyveck_shiftl`	✅	9s	7s	+29%
`mld_check_pct`	✅	8s	9s	-11%
`mld_h`	✅	8s	4s	+100%
`mld_sample_s1_s2_serial`	✅	8s	9s	-11%
`poly_uniform_eta`	✅	8s	5s	+60%
`polyveck_caddq`	✅	8s	8s	+0%
`polyveck_reduce`	✅	8s	9s	-11%
`polyveck_sub`	✅	8s	7s	+14%
`sign`	✅	8s	8s	+0%
`sign_keypair_internal`	✅	8s	5s	+60%
`keccak_absorb`	✅	7s	8s	-12%
`polyveck_pointwise_poly_montgomery`	✅	7s	6s	+17%
`polyveck_power2round`	✅	7s	10s	-30%
`sign_signature_pre_hash_shake256`	✅	7s	3s	+133%
`unpack_hints`	✅	7s	5s	+40%
`intt_native_x86_64`	✅	6s	3s	+100%
`keccak_squeeze`	✅	6s	6s	+0%
`mld_compute_pack_z`	✅	6s	7s	-14%
`mld_sample_s1_s2`	✅	6s	7s	-14%
`poly_decompose_c`	✅	6s	7s	-14%
`poly_invntt_tomont_c`	✅	6s	7s	-14%
`poly_power2round`	✅	6s	5s	+20%
`polyveck_ntt`	✅	6s	8s	-25%
`polyveck_pack_w1`	✅	6s	4s	+50%
`sign_signature_pre_hash_internal`	✅	6s	2s	+200%
`unpack_sig`	✅	6s	3s	+100%
`decompose`	✅	5s	4s	+25%
`poly_caddq_c`	✅	5s	7s	-29%
`poly_decompose`	✅	5s	4s	+25%
`polyt0_pack`	✅	5s	5s	+0%
`polyveck_make_hint`	✅	5s	8s	-38%
`polyvecl_uniform_gamma1_serial`	✅	5s	5s	+0%
`polyvecl_unpack_z`	✅	5s	1s	+400%
`polyw1_pack`	✅	5s	4s	+25%
`sign_verify_extmu`	✅	5s	3s	+67%
`sign_verify_pre_hash_internal`	✅	5s	4s	+25%
`fqscale`	✅	4s	4s	+0%
`keccakf1600_xor_bytes`	✅	4s	1s	+300%
`keccakf1600_xor_bytes (big endian)`	✅	4s	2s	+100%
`keccakf1600x4_xor_bytes`	✅	4s	3s	+33%
`ntt_native_aarch64`	✅	4s	6s	-33%
`pack_sig_c_h`	✅	4s	3s	+33%
`poly_caddq_native`	✅	4s	4s	+0%
`poly_caddq_native_aarch64`	✅	4s	2s	+100%
`poly_challenge`	✅	4s	4s	+0%
`poly_invntt_tomont`	✅	4s	3s	+33%
`poly_ntt`	✅	4s	4s	+0%
`poly_sub`	✅	4s	3s	+33%
`polyt1_pack`	✅	4s	3s	+33%
`polyt1_unpack`	✅	4s	2s	+100%
`polyveck_unpack_eta`	✅	4s	3s	+33%
`polyveck_unpack_t0`	✅	4s	4s	+0%
`polyvecl_unpack_eta`	✅	4s	4s	+0%
`rej_eta_native`	✅	4s	4s	+0%
`shake256_finalize`	✅	4s	3s	+33%
`sign_open`	✅	4s	7s	-43%
`sign_signature`	✅	4s	3s	+33%
`sign_signature_extmu`	✅	4s	5s	-20%
`sign_verify_pre_hash_shake256`	✅	4s	4s	+0%
`unpack_pk`	✅	4s	4s	+0%
`unpack_sk`	✅	4s	5s	-20%
`use_hint`	✅	4s	3s	+33%
`keccak_finalize`	✅	3s	4s	-25%
`keccak_init`	✅	3s	4s	-25%
`make_hint`	✅	3s	3s	+0%
`mld_ct_cmask_nonzero_u8`	✅	3s	3s	+0%
`mld_ct_get_optblocker_u32`	✅	3s	4s	-25%
`mld_value_barrier_u32`	✅	3s	2s	+50%
`ntt_native_x86_64`	✅	3s	4s	-25%
`pack_sig_z`	✅	3s	3s	+0%
`pack_sk`	✅	3s	3s	+0%
`poly_caddq`	✅	3s	3s	+0%
`poly_chknorm`	✅	3s	1s	+200%
`poly_chknorm_native_aarch64`	✅	3s	2s	+50%
`poly_invntt_tomont_native`	✅	3s	3s	+0%
`poly_make_hint`	✅	3s	2s	+50%
`poly_ntt_native`	✅	3s	4s	-25%
`poly_reduce`	✅	3s	4s	-25%
`poly_uniform`	✅	3s	4s	-25%
`poly_uniform_gamma1`	✅	3s	4s	-25%
`poly_uniform_gamma1_4x`	✅	3s	4s	-25%
`poly_use_hint_c`	✅	3s	3s	+0%
`poly_use_hint_native`	✅	3s	4s	-25%
`polyveck_chknorm`	✅	3s	5s	-40%
`polyveck_pack_eta`	✅	3s	3s	+0%
`polyvecl_chknorm`	✅	3s	6s	-50%
`polyvecl_pointwise_acc_montgomery`	✅	3s	2s	+50%
`polyz_pack`	✅	3s	2s	+50%
`polyz_unpack_native`	✅	3s	4s	-25%
`reduce32`	✅	3s	4s	-25%
`rej_eta_c`	✅	3s	5s	-40%
`shake128_init`	✅	3s	3s	+0%
`shake128_squeeze`	✅	3s	2s	+50%
`shake256_absorb`	✅	3s	2s	+50%
`shake256_release`	✅	3s	5s	-40%
`shake256x4_absorb_once`	✅	3s	2s	+50%
`sign_keypair`	✅	3s	2s	+50%
`sys_check_capability`	✅	3s	2s	+50%
`caddq`	✅	2s	1s	+100%
`keccakf1600_extract_bytes (big endian)`	✅	2s	1s	+100%
`keccakf1600x4_permute`	✅	2s	3s	-33%
`mld_ct_abs_i32`	✅	2s	2s	+0%
`mld_ct_cmask_neg_i32`	✅	2s	3s	-33%
`mld_ct_cmask_nonzero_u32`	✅	2s	3s	-33%
`mld_ct_get_optblocker_i64`	✅	2s	3s	-33%
`mld_ct_get_optblocker_u8`	✅	2s	2s	+0%
`mld_keccakf1600_extract_bytes`	✅	2s	4s	-50%
`mld_prepare_domain_separation_prefix`	✅	2s	7s	-71%
`mld_value_barrier_i64`	✅	2s	2s	+0%
`mld_value_barrier_u8`	✅	2s	4s	-50%
`montgomery_reduce`	✅	2s	3s	-33%
`pack_pk`	✅	2s	5s	-60%
`poly_chknorm_native`	✅	2s	5s	-60%
`poly_decompose_native`	✅	2s	4s	-50%
`poly_ntt_c`	✅	2s	3s	-33%
`poly_pointwise_montgomery`	✅	2s	3s	-33%
`poly_pointwise_montgomery_native`	✅	2s	3s	-33%
`poly_shiftl`	✅	2s	3s	-33%
`poly_use_hint`	✅	2s	2s	+0%
`polyeta_pack`	✅	2s	3s	-33%
`polyveck_pack_t0`	✅	2s	4s	-50%
`polyvecl_pack_eta`	✅	2s	4s	-50%
`polyvecl_permute_bitrev_to_custom`	✅	2s	4s	-50%
`polyvecl_pointwise_acc_montgomery_native`	✅	2s	2s	+0%
`polyvecl_uniform_gamma1`	✅	2s	3s	-33%
`polyz_unpack`	✅	2s	3s	-33%
`power2round`	✅	2s	3s	-33%
`shake128_absorb`	✅	2s	3s	-33%
`shake128_release`	✅	2s	4s	-50%
`shake128x4_absorb_once`	✅	2s	2s	+0%
`shake128x4_squeezeblocks`	✅	2s	2s	+0%
`shake256`	✅	2s	3s	-33%
`shake256_init`	✅	2s	1s	+100%
`shake256_squeeze`	✅	2s	3s	-33%
`sign_verify`	✅	2s	5s	-60%
`keccakf1600x4_extract_bytes`	✅	1s	2s	-50%
`mld_ct_sel_int32`	✅	1s	2s	-50%
`rej_eta`	✅	1s	4s	-75%
`shake128_finalize`	✅	1s	2s	-50%
`shake256x4_squeezeblocks`	✅	1s	3s	-67%

mkannwischer · 2026-04-02T09:38:01Z

Thanks @L-series. Let's first get this merged in mlkem-native and then align this one. Changing back to draft for now.

Safety proofs are not fully implemented yet here for all proves. We should skip those for now and open an issue to add it later.

L-series added 3 commits April 1, 2026 11:41

scripts: verify that all expected theorems are present

1f2840e

We add a 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>

CI: HOL-Light: ensure necessary theorems are proven

02bc1dc

Add the check-theorems script to the HOL-Light CI action. Fail the CI if any of the required proofs are not present. Signed-off-by: Andreas Hatziiliou <andreas.hatziiliou@savoirfairelinux.com>

L-series requested a review from a team as a code owner April 1, 2026 15:53

mkannwischer self-assigned this Apr 1, 2026

mkannwischer marked this pull request as draft April 2, 2026 09:38

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

HOL-Light: improve tooling and CI#1009

HOL-Light: improve tooling and CI#1009
L-series wants to merge 3 commits intomainfrom
HOL-Light-CI

L-series commented Apr 1, 2026

Uh oh!

oqs-bot commented Apr 1, 2026

Uh oh!

oqs-bot commented Apr 1, 2026

Uh oh!

oqs-bot commented Apr 1, 2026

Uh oh!

mkannwischer commented Apr 2, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

L-series commented Apr 1, 2026

Uh oh!

oqs-bot commented Apr 1, 2026

CBMC Results (ML-DSA-44)

Uh oh!

oqs-bot commented Apr 1, 2026

CBMC Results (ML-DSA-65)

Uh oh!

oqs-bot commented Apr 1, 2026

CBMC Results (ML-DSA-87)

Uh oh!

mkannwischer commented Apr 2, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants