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

Resolves Port: HOL-Light: improve tooling and CI #1280

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

CBMC Results (ML-DSA-44)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`compute_pack_t0_t1`	⚠️	104s	50s	+108%
`mld_attempt_signature_generation`	⚠️	307s	58s	+429%
`sig_unpack_hints`	⚠️	21s	2s	+950%
`sign_pk_from_sk`	⚠️	36s	5s	+620%
`sign_signature_internal`	⚠️	99s	26s	+281%
`sign_verify_internal`	⚠️	297s	114s	+161%

Full Results (210 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	1847s	1514s	+22.0%
`mld_attempt_signature_generation`	⚠️	307s	58s	+429%
`sign_verify_internal`	⚠️	297s	114s	+161%
`polyvecl_pointwise_acc_montgomery_c`	✅	149s	131s	+14%
`poly_pointwise_montgomery_c`	✅	140s	114s	+23%
`compute_pack_t0_t1`	⚠️	104s	50s	+108%
`sign_signature_internal`	⚠️	99s	26s	+281%
`mld_invntt_layer`	✅	59s	107s	-45%
`sign_pk_from_sk`	⚠️	36s	5s	+620%
`fqmul`	✅	23s	39s	-41%
`mld_ntt_layer`	✅	23s	42s	-45%
`sig_unpack_hints`	⚠️	21s	2s	+950%
`polyvec_matrix_expand`	✅	18s	28s	-36%
`sign_keypair_internal`	✅	18s	4s	+350%
`mld_ntt_butterfly_block`	✅	12s	23s	-48%
`keccakf1600x4_permute_native`	✅	11s	22s	-50%
`polyt0_unpack`	✅	10s	15s	-33%
`poly_ntt_c`	✅	9s	19s	-53%
`rej_uniform`	✅	9s	18s	-50%
`rej_uniform_native_x86_64`	✅	9s	-	new
`poly_uniform_eta_4x`	✅	8s	11s	-27%
`polyeta_unpack`	✅	8s	14s	-43%
`polyvec_matrix_pointwise_montgomery_yvec`	✅	8s	15s	-47%
`poly_uniform_4x`	✅	7s	14s	-50%
`polyz_unpack_c`	✅	7s	11s	-36%
`rej_uniform_c`	✅	7s	15s	-53%
`mld_check_pct`	✅	6s	14s	-57%
`mld_compute_pack_z`	✅	6s	7s	-14%
`poly_chknorm_c`	✅	6s	17s	-65%
`poly_invntt_tomont_c`	✅	6s	11s	-45%
`keccak_absorb_once_x4`	✅	5s	9s	-44%
`mld_h`	✅	5s	4s	+25%
`mld_polymat_expand_entry`	✅	5s	3s	+67%
`poly_ntt_native`	✅	5s	5s	+0%
`polyvecl_ntt`	✅	5s	2s	+150%
`sign_signature_pre_hash_internal`	✅	5s	6s	-17%
`sign_signature_pre_hash_shake256`	✅	5s	3s	+67%
`sk_t0hat_get_poly`	✅	5s	2s	+150%
`intt_native_aarch64`	✅	4s	9s	-56%
`keccak_absorb`	✅	4s	5s	-20%
`keccakf1600_permute_native`	✅	4s	3s	+33%
`mld_ct_cmask_neg_i32`	✅	4s	3s	+33%
`mld_keccakf1600_permute_c`	✅	4s	8s	-50%
`mld_sign_attempt`	✅	4s	-	new
`pack_sig_h`	✅	4s	3s	+33%
`pointwise_acc_native_aarch64`	✅	4s	4s	+0%
`pointwise_native_x86_64`	✅	4s	4s	+0%
`poly_chknorm_native`	✅	4s	4s	+0%
`poly_chknorm_native_aarch64`	✅	4s	4s	+0%
`poly_decompose`	✅	4s	3s	+33%
`poly_uniform`	✅	4s	6s	-33%
`polyveck_invntt_tomont`	✅	4s	5s	-20%
`polyveck_unpack_eta`	✅	4s	2s	+100%
`rej_uniform_native_aarch64`	✅	4s	5s	-20%
`sign_keypair`	✅	4s	4s	+0%
`yvec_init`	✅	4s	3s	+33%
`caddq`	✅	3s	2s	+50%
`decompose`	✅	3s	2s	+50%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	3s	1s	+200%
`keccak_squeeze`	✅	3s	1s	+200%
`keccakf1600_extract_bytes (big endian)`	✅	3s	2s	+50%
`keccakf1600x4_extract_bytes_native`	✅	3s	3s	+0%
`keccakf1600x4_xor_bytes`	✅	3s	2s	+50%
`make_hint`	✅	3s	3s	+0%
`mld_ct_abs_i32`	✅	3s	2s	+50%
`mld_sign_finish`	✅	3s	-	new
`pack_sig_c`	✅	3s	2s	+50%
`pack_sk_rho_key_tr_s2`	✅	3s	3s	+0%
`pointwise_acc_native_x86_64`	✅	3s	7s	-57%
`poly_add`	✅	3s	7s	-57%
`poly_caddq_c`	✅	3s	2s	+50%
`poly_caddq_native`	✅	3s	5s	-40%
`poly_caddq_native_aarch64`	✅	3s	4s	-25%
`poly_caddq_native_x86_64`	✅	3s	4s	-25%
`poly_challenge`	✅	3s	3s	+0%
`poly_decompose_32_native_aarch64`	✅	3s	2s	+50%
`poly_decompose_native`	✅	3s	3s	+0%
`poly_permute_bitrev_to_custom_optional`	✅	3s	2s	+50%
`poly_power2round`	✅	3s	4s	-25%
`poly_reduce`	✅	3s	3s	+0%
`poly_sub`	✅	3s	3s	+0%
`poly_uniform_gamma1_4x`	✅	3s	5s	-40%
`polyt0_pack`	✅	3s	2s	+50%
`polyvec_matrix_expand_serial`	✅	3s	8s	-62%
`polyveck_caddq`	✅	3s	3s	+0%
`polyveck_chknorm`	✅	3s	5s	-40%
`polyvecl_pack_eta`	✅	3s	3s	+0%
`polyvecl_pointwise_acc_montgomery`	✅	3s	4s	-25%
`polyvecl_pointwise_acc_montgomery_native`	✅	3s	2s	+50%
`polyvecl_uniform_gamma1`	✅	3s	3s	+0%
`polyw1_pack_32`	✅	3s	2s	+50%
`polyz_pack`	✅	3s	2s	+50%
`polyz_unpack`	✅	3s	3s	+0%
`polyz_unpack_native`	✅	3s	2s	+50%
`rej_uniform_native`	✅	3s	4s	-25%
`shake128_absorb`	✅	3s	2s	+50%
`shake128_init`	✅	3s	3s	+0%
`shake128x4_absorb_once`	✅	3s	3s	+0%
`shake256`	✅	3s	1s	+200%
`shake256_absorb`	✅	3s	3s	+0%
`sign_signature`	✅	3s	3s	+0%
`sign_verify_extmu`	✅	3s	3s	+0%
`unpack_pk_t1`	✅	3s	5s	-40%
`unpack_sk_t0hat`	✅	3s	3s	+0%
`use_hint`	✅	3s	2s	+50%
`fqscale`	✅	2s	3s	-33%
`intt_native_x86_64`	✅	2s	4s	-50%
`keccak_f1600_x1_native_aarch64`	✅	2s	2s	+0%
`keccak_f1600_x4_native_avx2`	✅	2s	3s	-33%
`keccak_finalize`	✅	2s	3s	-33%
`keccak_init`	✅	2s	3s	-33%
`keccakf1600_permute`	✅	2s	2s	+0%
`keccakf1600_xor_bytes (big endian)`	✅	2s	4s	-50%
`mld_ct_cmask_nonzero_u32`	✅	2s	2s	+0%
`mld_ct_cmask_nonzero_u8`	✅	2s	2s	+0%
`mld_ct_get_optblocker_u32`	✅	2s	1s	+100%
`mld_ct_sel_int32`	✅	2s	2s	+0%
`mld_keccakf1600_extract_bytes`	✅	2s	2s	+0%
`mld_keccakf1600x4_xor_bytes_c`	✅	2s	2s	+0%
`mld_prepare_domain_separation_prefix`	✅	2s	4s	-50%
`mld_sample_s1_s2`	✅	2s	4s	-50%
`mld_sample_s1_s2_serial`	✅	2s	3s	-33%
`mld_sign_resume`	✅	2s	-	new
`mld_value_barrier_i64`	✅	2s	2s	+0%
`mld_value_barrier_u8`	✅	2s	3s	-33%
`montgomery_reduce`	✅	2s	3s	-33%
`ntt_native_aarch64`	✅	2s	3s	-33%
`pack_sk_s1`	✅	2s	2s	+0%
`pointwise_native_aarch64`	✅	2s	5s	-60%
`poly_chknorm`	✅	2s	4s	-50%
`poly_decompose_c`	✅	2s	4s	-50%
`poly_decompose_native_x86_64`	✅	2s	3s	-33%
`poly_invntt_tomont`	✅	2s	4s	-50%
`poly_invntt_tomont_native`	✅	2s	4s	-50%
`poly_permute_bitrev_to_custom_optional_native`	✅	2s	4s	-50%
`poly_pointwise_montgomery_native`	✅	2s	2s	+0%
`poly_uniform_eta`	✅	2s	5s	-60%
`poly_uniform_gamma1`	✅	2s	4s	-50%
`poly_use_hint_c`	✅	2s	3s	-33%
`poly_use_hint_native`	✅	2s	4s	-50%
`poly_use_hint_native_x86_64`	✅	2s	-	new
`polyt1_unpack`	✅	2s	5s	-60%
`polyveck_ntt`	✅	2s	5s	-60%
`polyveck_pack_eta`	✅	2s	2s	+0%
`polyvecl_chknorm`	✅	2s	10s	-80%
`polyvecl_unpack_z`	✅	2s	2s	+0%
`polyz_unpack_native_x86_64`	✅	2s	3s	-33%
`power2round`	✅	2s	3s	-33%
`rej_eta`	✅	2s	3s	-33%
`rej_eta_c`	✅	2s	4s	-50%
`rej_eta_native`	✅	2s	6s	-67%
`rej_uniform_eta_native_x86_64`	✅	2s	-	new
`shake128_finalize`	✅	2s	2s	+0%
`shake128_release`	✅	2s	1s	+100%
`shake256_finalize`	✅	2s	2s	+0%
`shake256_init`	✅	2s	3s	-33%
`shake256_squeeze`	✅	2s	2s	+0%
`shake256x4_absorb_once`	✅	2s	3s	-33%
`shake256x4_squeezeblocks`	✅	2s	4s	-50%
`sign_verify`	✅	2s	4s	-50%
`sign_verify_pre_hash_internal`	✅	2s	3s	-33%
`sign_verify_pre_hash_shake256`	✅	2s	5s	-60%
`sys_check_capability`	✅	2s	4s	-50%
`unpack_sk`	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64_v84a`	✅	1s	3s	-67%
`keccak_f1600_x4_native_aarch64_v84a`	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	1s	3s	-67%
`keccak_squeezeblocks_x4`	✅	1s	4s	-75%
`keccakf1600_xor_bytes`	✅	1s	1s	+0%
`keccakf1600x4_extract_bytes`	✅	1s	2s	-50%
`keccakf1600x4_permute`	✅	1s	4s	-75%
`keccakf1600x4_xor_bytes_native`	✅	1s	3s	-67%
`mld_ct_get_optblocker_i64`	✅	1s	4s	-75%
`mld_ct_get_optblocker_u8`	✅	1s	1s	+0%
`mld_ct_memcmp`	✅	1s	3s	-67%
`mld_keccakf1600x4_extract_bytes_c`	✅	1s	2s	-50%
`mld_value_barrier_u32`	✅	1s	2s	-50%
`ntt_native_x86_64`	✅	1s	3s	-67%
`nttunpack_native_x86_64`	✅	1s	1s	+0%
`pack_sig_z`	✅	1s	4s	-75%
`poly_caddq`	✅	1s	2s	-50%
`poly_chknorm_native_x86_64`	✅	1s	2s	-50%
`poly_decompose_88_native_aarch64`	✅	1s	4s	-75%
`poly_ntt`	✅	1s	3s	-67%
`poly_pointwise_montgomery`	✅	1s	3s	-67%
`poly_shiftl`	✅	1s	3s	-67%
`poly_use_hint`	✅	1s	4s	-75%
`poly_use_hint_native_aarch64`	✅	1s	2s	-50%
`polyeta_pack`	✅	1s	3s	-67%
`polyt1_pack`	✅	1s	4s	-75%
`polyvec_matrix_pointwise_montgomery_row`	✅	1s	2s	-50%
`polyveck_decompose`	✅	1s	4s	-75%
`polyveck_pack_w1`	✅	1s	1s	+0%
`polyveck_reduce`	✅	1s	5s	-80%
`polyvecl_uniform_gamma1_serial`	✅	1s	2s	-50%
`polyvecl_unpack_eta`	✅	1s	2s	-50%
`polyw1_pack`	✅	1s	3s	-67%
`polyw1_pack_88`	✅	1s	1s	+0%
`polyz_unpack_17_native_aarch64`	✅	1s	5s	-80%
`polyz_unpack_19_native_aarch64`	✅	1s	5s	-80%
`reduce32`	✅	1s	2s	-50%
`rej_uniform_eta_native_aarch64`	✅	1s	2s	-50%
`shake128_squeeze`	✅	1s	1s	+0%
`shake128x4_squeezeblocks`	✅	1s	1s	+0%
`shake256_release`	✅	1s	2s	-50%
`sign_signature_extmu`	✅	1s	4s	-75%
`sk_s1hat_get_poly`	✅	1s	3s	-67%
`sk_s2hat_get_poly`	✅	1s	2s	-50%
`unpack_sk_s1hat`	✅	1s	1s	+0%
`unpack_sk_s2hat`	✅	1s	4s	-75%
`yvec_get_poly`	✅	1s	3s	-67%

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

CBMC Results (ML-DSA-65)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`compute_pack_t0_t1`	⚠️	124s	13s	+854%
`mld_attempt_signature_generation`	⚠️	237s	63s	+276%
`sig_unpack_hints`	⚠️	26s	2s	+1200%
`sign_keypair_internal`	⚠️	20s	5s	+300%
`sign_pk_from_sk`	⚠️	39s	6s	+550%
`sign_signature_internal`	⚠️	182s	55s	+231%
`sign_verify_internal`	⚠️	367s	177s	+107%

Full Results (210 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	2068s	1784s	+15.9%
`sign_verify_internal`	⚠️	367s	177s	+107%
`mld_attempt_signature_generation`	⚠️	237s	63s	+276%
`sign_signature_internal`	⚠️	182s	55s	+231%
`polyvecl_pointwise_acc_montgomery_c`	✅	166s	210s	-21%
`poly_pointwise_montgomery_c`	✅	131s	125s	+5%
`compute_pack_t0_t1`	⚠️	124s	13s	+854%
`polyvec_matrix_expand`	✅	75s	110s	-32%
`mld_invntt_layer`	✅	56s	109s	-49%
`sign_pk_from_sk`	⚠️	39s	6s	+550%
`sig_unpack_hints`	⚠️	26s	2s	+1200%
`fqmul`	✅	22s	40s	-45%
`mld_ntt_layer`	✅	21s	41s	-49%
`sign_keypair_internal`	⚠️	20s	5s	+300%
`polyvec_matrix_expand_serial`	✅	16s	27s	-41%
`polyveck_ntt`	✅	14s	7s	+100%
`keccakf1600x4_permute_native`	✅	12s	23s	-48%
`mld_ntt_butterfly_block`	✅	12s	24s	-50%
`polyveck_decompose`	✅	11s	12s	-8%
`poly_ntt_c`	✅	10s	19s	-47%
`rej_uniform`	✅	10s	18s	-44%
`polyvec_matrix_pointwise_montgomery_yvec`	✅	9s	18s	-50%
`poly_chknorm_c`	✅	8s	15s	-47%
`poly_uniform_4x`	✅	8s	13s	-38%
`polyt0_unpack`	✅	8s	16s	-50%
`rej_uniform_c`	✅	8s	14s	-43%
`rej_uniform_native_x86_64`	✅	8s	-	new
`poly_invntt_tomont_c`	✅	7s	11s	-36%
`poly_uniform_eta_4x`	✅	7s	14s	-50%
`poly_add`	✅	6s	9s	-33%
`poly_decompose_c`	✅	6s	5s	+20%
`polyveck_invntt_tomont`	✅	6s	8s	-25%
`sign_signature_extmu`	✅	6s	2s	+200%
`unpack_sk_s2hat`	✅	6s	4s	+50%
`keccak_absorb`	✅	5s	3s	+67%
`keccak_absorb_once_x4`	✅	5s	8s	-38%
`mld_check_pct`	✅	5s	14s	-64%
`mld_compute_pack_z`	✅	5s	7s	-29%
`pack_sig_h`	✅	5s	5s	+0%
`pointwise_acc_native_x86_64`	✅	5s	8s	-38%
`poly_invntt_tomont`	✅	5s	3s	+67%
`poly_power2round`	✅	5s	4s	+25%
`polyveck_caddq`	✅	5s	6s	-17%
`polyveck_pack_eta`	✅	5s	4s	+25%
`sign_keypair`	✅	5s	3s	+67%
`keccakf1600x4_extract_bytes`	✅	4s	4s	+0%
`mld_keccakf1600_extract_bytes`	✅	4s	1s	+300%
`mld_prepare_domain_separation_prefix`	✅	4s	2s	+100%
`mld_sign_attempt`	✅	4s	-	new
`pack_sig_z`	✅	4s	2s	+100%
`poly_chknorm_native`	✅	4s	2s	+100%
`poly_uniform_gamma1`	✅	4s	3s	+33%
`poly_use_hint_native_x86_64`	✅	4s	-	new
`polyeta_pack`	✅	4s	3s	+33%
`polyveck_pack_w1`	✅	4s	3s	+33%
`polyvecl_ntt`	✅	4s	4s	+0%
`polyvecl_uniform_gamma1`	✅	4s	2s	+100%
`polyw1_pack`	✅	4s	4s	+0%
`polyz_unpack_c`	✅	4s	13s	-69%
`reduce32`	✅	4s	3s	+33%
`rej_uniform_eta_native_x86_64`	✅	4s	-	new
`shake128_init`	✅	4s	2s	+100%
`shake256x4_squeezeblocks`	✅	4s	2s	+100%
`sign_signature_pre_hash_internal`	✅	4s	3s	+33%
`sign_signature_pre_hash_shake256`	✅	4s	3s	+33%
`sign_verify_pre_hash_shake256`	✅	4s	5s	-20%
`sk_s1hat_get_poly`	✅	4s	6s	-33%
`sk_t0hat_get_poly`	✅	4s	2s	+100%
`unpack_sk`	✅	4s	3s	+33%
`unpack_sk_t0hat`	✅	4s	5s	-20%
`decompose`	✅	3s	1s	+200%
`fqscale`	✅	3s	3s	+0%
`keccakf1600_permute`	✅	3s	2s	+50%
`keccakf1600x4_xor_bytes`	✅	3s	1s	+200%
`make_hint`	✅	3s	2s	+50%
`mld_h`	✅	3s	2s	+50%
`mld_keccakf1600x4_xor_bytes_c`	✅	3s	2s	+50%
`mld_sign_resume`	✅	3s	-	new
`mld_value_barrier_u8`	✅	3s	3s	+0%
`montgomery_reduce`	✅	3s	4s	-25%
`pointwise_acc_native_aarch64`	✅	3s	6s	-50%
`poly_caddq_c`	✅	3s	2s	+50%
`poly_invntt_tomont_native`	✅	3s	2s	+50%
`poly_pointwise_montgomery`	✅	3s	3s	+0%
`poly_reduce`	✅	3s	3s	+0%
`poly_uniform`	✅	3s	4s	-25%
`poly_uniform_gamma1_4x`	✅	3s	4s	-25%
`poly_use_hint_c`	✅	3s	5s	-40%
`poly_use_hint_native_aarch64`	✅	3s	3s	+0%
`polyt0_pack`	✅	3s	3s	+0%
`polyt1_unpack`	✅	3s	5s	-40%
`polyveck_unpack_eta`	✅	3s	6s	-50%
`polyvecl_chknorm`	✅	3s	7s	-57%
`polyvecl_unpack_eta`	✅	3s	3s	+0%
`polyw1_pack_32`	✅	3s	4s	-25%
`polyw1_pack_88`	✅	3s	2s	+50%
`polyz_unpack_native_x86_64`	✅	3s	3s	+0%
`power2round`	✅	3s	1s	+200%
`rej_uniform_eta_native_aarch64`	✅	3s	4s	-25%
`shake128_squeeze`	✅	3s	2s	+50%
`shake256_release`	✅	3s	2s	+50%
`sign_verify`	✅	3s	3s	+0%
`sign_verify_pre_hash_internal`	✅	3s	5s	-40%
`unpack_pk_t1`	✅	3s	5s	-40%
`caddq`	✅	2s	3s	-33%
`intt_native_aarch64`	✅	2s	3s	-33%
`intt_native_x86_64`	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	2s	2s	+0%
`keccak_f1600_x4_native_avx2`	✅	2s	2s	+0%
`keccak_finalize`	✅	2s	2s	+0%
`keccak_squeeze`	✅	2s	4s	-50%
`keccak_squeezeblocks_x4`	✅	2s	5s	-60%
`mld_ct_cmask_neg_i32`	✅	2s	2s	+0%
`mld_ct_cmask_nonzero_u8`	✅	2s	3s	-33%
`mld_ct_get_optblocker_i64`	✅	2s	2s	+0%
`mld_ct_get_optblocker_u32`	✅	2s	3s	-33%
`mld_keccakf1600_permute_c`	✅	2s	6s	-67%
`mld_keccakf1600x4_extract_bytes_c`	✅	2s	3s	-33%
`mld_polymat_expand_entry`	✅	2s	4s	-50%
`mld_sample_s1_s2`	✅	2s	6s	-67%
`mld_sample_s1_s2_serial`	✅	2s	4s	-50%
`mld_sign_finish`	✅	2s	-	new
`mld_value_barrier_i64`	✅	2s	2s	+0%
`ntt_native_aarch64`	✅	2s	2s	+0%
`ntt_native_x86_64`	✅	2s	2s	+0%
`pack_sig_c`	✅	2s	5s	-60%
`pack_sk_s1`	✅	2s	5s	-60%
`pointwise_native_aarch64`	✅	2s	5s	-60%
`poly_caddq`	✅	2s	2s	+0%
`poly_caddq_native`	✅	2s	2s	+0%
`poly_caddq_native_x86_64`	✅	2s	3s	-33%
`poly_chknorm`	✅	2s	4s	-50%
`poly_chknorm_native_aarch64`	✅	2s	3s	-33%
`poly_chknorm_native_x86_64`	✅	2s	3s	-33%
`poly_decompose`	✅	2s	2s	+0%
`poly_decompose_32_native_aarch64`	✅	2s	3s	-33%
`poly_ntt`	✅	2s	2s	+0%
`poly_ntt_native`	✅	2s	4s	-50%
`poly_permute_bitrev_to_custom_optional`	✅	2s	2s	+0%
`poly_pointwise_montgomery_native`	✅	2s	3s	-33%
`poly_use_hint`	✅	2s	3s	-33%
`poly_use_hint_native`	✅	2s	2s	+0%
`polyeta_unpack`	✅	2s	8s	-75%
`polyt1_pack`	✅	2s	3s	-33%
`polyvec_matrix_pointwise_montgomery_row`	✅	2s	1s	+100%
`polyveck_chknorm`	✅	2s	6s	-67%
`polyvecl_pack_eta`	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery_native`	✅	2s	2s	+0%
`polyz_pack`	✅	2s	3s	-33%
`polyz_unpack`	✅	2s	3s	-33%
`polyz_unpack_17_native_aarch64`	✅	2s	3s	-33%
`rej_eta_c`	✅	2s	5s	-60%
`rej_uniform_native_aarch64`	✅	2s	3s	-33%
`shake128_absorb`	✅	2s	2s	+0%
`shake128_release`	✅	2s	3s	-33%
`shake128x4_absorb_once`	✅	2s	3s	-33%
`shake128x4_squeezeblocks`	✅	2s	3s	-33%
`shake256`	✅	2s	2s	+0%
`shake256_init`	✅	2s	2s	+0%
`shake256x4_absorb_once`	✅	2s	3s	-33%
`sign_signature`	✅	2s	6s	-67%
`sk_s2hat_get_poly`	✅	2s	2s	+0%
`yvec_get_poly`	✅	2s	3s	-33%
`yvec_init`	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64`	✅	1s	2s	-50%
`keccak_f1600_x1_native_aarch64_v84a`	✅	1s	3s	-67%
`keccak_f1600_x4_native_aarch64_v84a`	✅	1s	4s	-75%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	1s	2s	-50%
`keccak_init`	✅	1s	1s	+0%
`keccakf1600_extract_bytes (big endian)`	✅	1s	2s	-50%
`keccakf1600_permute_native`	✅	1s	3s	-67%
`keccakf1600_xor_bytes`	✅	1s	2s	-50%
`keccakf1600_xor_bytes (big endian)`	✅	1s	2s	-50%
`keccakf1600x4_extract_bytes_native`	✅	1s	4s	-75%
`keccakf1600x4_permute`	✅	1s	4s	-75%
`keccakf1600x4_xor_bytes_native`	✅	1s	3s	-67%
`mld_ct_abs_i32`	✅	1s	2s	-50%
`mld_ct_cmask_nonzero_u32`	✅	1s	4s	-75%
`mld_ct_get_optblocker_u8`	✅	1s	2s	-50%
`mld_ct_memcmp`	✅	1s	2s	-50%
`mld_ct_sel_int32`	✅	1s	3s	-67%
`mld_value_barrier_u32`	✅	1s	3s	-67%
`nttunpack_native_x86_64`	✅	1s	3s	-67%
`pack_sk_rho_key_tr_s2`	✅	1s	2s	-50%
`pointwise_native_x86_64`	✅	1s	3s	-67%
`poly_caddq_native_aarch64`	✅	1s	2s	-50%
`poly_challenge`	✅	1s	6s	-83%
`poly_decompose_88_native_aarch64`	✅	1s	1s	+0%
`poly_decompose_native`	✅	1s	3s	-67%
`poly_decompose_native_x86_64`	✅	1s	3s	-67%
`poly_permute_bitrev_to_custom_optional_native`	✅	1s	4s	-75%
`poly_shiftl`	✅	1s	3s	-67%
`poly_sub`	✅	1s	3s	-67%
`poly_uniform_eta`	✅	1s	4s	-75%
`polyveck_reduce`	✅	1s	4s	-75%
`polyvecl_pointwise_acc_montgomery`	✅	1s	3s	-67%
`polyvecl_uniform_gamma1_serial`	✅	1s	3s	-67%
`polyvecl_unpack_z`	✅	1s	3s	-67%
`polyz_unpack_19_native_aarch64`	✅	1s	3s	-67%
`polyz_unpack_native`	✅	1s	4s	-75%
`rej_eta`	✅	1s	2s	-50%
`rej_eta_native`	✅	1s	3s	-67%
`rej_uniform_native`	✅	1s	4s	-75%
`shake128_finalize`	✅	1s	1s	+0%
`shake256_absorb`	✅	1s	2s	-50%
`shake256_finalize`	✅	1s	1s	+0%
`shake256_squeeze`	✅	1s	3s	-67%
`sign_verify_extmu`	✅	1s	3s	-67%
`sys_check_capability`	✅	1s	4s	-75%
`unpack_sk_s1hat`	✅	1s	2s	-50%
`use_hint`	✅	1s	2s	-50%

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

CBMC Results (ML-DSA-87)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`TOTAL`	⚠️	2784s	2151s	+29.4%
`compute_pack_t0_t1`	⚠️	185s	19s	+874%
`mld_attempt_signature_generation`	⚠️	288s	55s	+424%
`sig_unpack_hints`	⚠️	26s	3s	+767%
`sign_keypair_internal`	⚠️	51s	6s	+750%
`sign_pk_from_sk`	⚠️	47s	6s	+683%
`sign_signature_internal`	⚠️	312s	42s	+643%
`sign_verify_internal`	⚠️	711s	97s	+633%

Full Results (210 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	⚠️	2784s	2151s	+29.4%
`sign_verify_internal`	⚠️	711s	97s	+633%
`sign_signature_internal`	⚠️	312s	42s	+643%
`mld_attempt_signature_generation`	⚠️	288s	55s	+424%
`polyvecl_pointwise_acc_montgomery_c`	✅	215s	353s	-39%
`compute_pack_t0_t1`	⚠️	185s	19s	+874%
`poly_pointwise_montgomery_c`	✅	133s	144s	-8%
`polyvec_matrix_expand`	✅	83s	324s	-74%
`mld_invntt_layer`	✅	60s	115s	-48%
`sign_keypair_internal`	⚠️	51s	6s	+750%
`sign_pk_from_sk`	⚠️	47s	6s	+683%
`sig_unpack_hints`	⚠️	26s	3s	+767%
`polyvec_matrix_expand_serial`	✅	23s	38s	-39%
`mld_ntt_layer`	✅	22s	45s	-51%
`fqmul`	✅	21s	43s	-51%
`keccakf1600x4_permute_native`	✅	13s	23s	-43%
`mld_ntt_butterfly_block`	✅	13s	24s	-46%
`poly_ntt_c`	✅	11s	21s	-48%
`polyt0_unpack`	✅	10s	14s	-29%
`polyvec_matrix_pointwise_montgomery_yvec`	✅	10s	18s	-44%
`poly_chknorm_c`	✅	9s	15s	-40%
`polyeta_unpack`	✅	9s	17s	-47%
`poly_uniform_4x`	✅	8s	13s	-38%
`rej_uniform_native_x86_64`	✅	8s	-	new
`mld_compute_pack_z`	✅	7s	8s	-12%
`poly_uniform_eta_4x`	✅	7s	11s	-36%
`rej_uniform`	✅	7s	15s	-53%
`sign_keypair`	✅	7s	4s	+75%
`keccak_absorb_once_x4`	✅	6s	9s	-33%
`mld_check_pct`	✅	6s	16s	-62%
`polyveck_decompose`	✅	6s	13s	-54%
`rej_uniform_c`	✅	6s	19s	-68%
`mld_sample_s1_s2_serial`	✅	5s	8s	-38%
`mld_sign_finish`	✅	5s	-	new
`poly_invntt_tomont_c`	✅	5s	12s	-58%
`poly_power2round`	✅	5s	3s	+67%
`polyveck_invntt_tomont`	✅	5s	9s	-44%
`polyveck_ntt`	✅	5s	11s	-55%
`polyvecl_pointwise_acc_montgomery_native`	✅	5s	3s	+67%
`polyz_unpack_c`	✅	5s	3s	+67%
`rej_eta_native`	✅	5s	6s	-17%
`rej_uniform_native`	✅	5s	8s	-38%
`shake256_absorb`	✅	5s	2s	+150%
`sign_signature`	✅	5s	5s	+0%
`sign_signature_extmu`	✅	5s	4s	+25%
`keccak_f1600_x4_native_aarch64_v84a`	✅	4s	4s	+0%
`mld_h`	✅	4s	3s	+33%
`mld_keccakf1600_permute_c`	✅	4s	7s	-43%
`mld_polymat_expand_entry`	✅	4s	3s	+33%
`mld_sample_s1_s2`	✅	4s	6s	-33%
`mld_sign_attempt`	✅	4s	-	new
`pack_sk_rho_key_tr_s2`	✅	4s	3s	+33%
`pack_sk_s1`	✅	4s	1s	+300%
`pointwise_acc_native_aarch64`	✅	4s	6s	-33%
`poly_challenge`	✅	4s	5s	-20%
`poly_chknorm_native_aarch64`	✅	4s	4s	+0%
`poly_decompose_88_native_aarch64`	✅	4s	2s	+100%
`poly_use_hint`	✅	4s	1s	+300%
`poly_use_hint_c`	✅	4s	2s	+100%
`polyt1_pack`	✅	4s	3s	+33%
`polyveck_caddq`	✅	4s	8s	-50%
`polyveck_reduce`	✅	4s	3s	+33%
`polyvecl_chknorm`	✅	4s	7s	-43%
`polyvecl_ntt`	✅	4s	7s	-43%
`polyw1_pack_32`	✅	4s	4s	+0%
`rej_uniform_native_aarch64`	✅	4s	2s	+100%
`sign_signature_pre_hash_shake256`	✅	4s	6s	-33%
`unpack_pk_t1`	✅	4s	1s	+300%
`yvec_init`	✅	4s	4s	+0%
`intt_native_aarch64`	✅	3s	3s	+0%
`keccak_absorb`	✅	3s	3s	+0%
`keccak_squeezeblocks_x4`	✅	3s	4s	-25%
`keccakf1600_xor_bytes`	✅	3s	3s	+0%
`make_hint`	✅	3s	3s	+0%
`mld_ct_cmask_nonzero_u8`	✅	3s	3s	+0%
`mld_ct_get_optblocker_u32`	✅	3s	2s	+50%
`mld_ct_get_optblocker_u8`	✅	3s	3s	+0%
`mld_prepare_domain_separation_prefix`	✅	3s	4s	-25%
`montgomery_reduce`	✅	3s	3s	+0%
`ntt_native_x86_64`	✅	3s	2s	+50%
`pack_sig_c`	✅	3s	4s	-25%
`pack_sig_z`	✅	3s	5s	-40%
`pointwise_acc_native_x86_64`	✅	3s	6s	-50%
`pointwise_native_x86_64`	✅	3s	2s	+50%
`poly_chknorm`	✅	3s	3s	+0%
`poly_chknorm_native`	✅	3s	4s	-25%
`poly_decompose_c`	✅	3s	5s	-40%
`poly_decompose_native`	✅	3s	2s	+50%
`poly_invntt_tomont_native`	✅	3s	5s	-40%
`poly_ntt`	✅	3s	3s	+0%
`poly_permute_bitrev_to_custom_optional_native`	✅	3s	5s	-40%
`poly_uniform`	✅	3s	4s	-25%
`poly_uniform_eta`	✅	3s	4s	-25%
`poly_uniform_gamma1`	✅	3s	4s	-25%
`poly_uniform_gamma1_4x`	✅	3s	3s	+0%
`poly_use_hint_native`	✅	3s	3s	+0%
`poly_use_hint_native_x86_64`	✅	3s	-	new
`polyt1_unpack`	✅	3s	4s	-25%
`polyvec_matrix_pointwise_montgomery_row`	✅	3s	3s	+0%
`polyveck_chknorm`	✅	3s	3s	+0%
`polyveck_pack_w1`	✅	3s	3s	+0%
`polyvecl_uniform_gamma1`	✅	3s	2s	+50%
`polyz_pack`	✅	3s	5s	-40%
`polyz_unpack_17_native_aarch64`	✅	3s	3s	+0%
`polyz_unpack_19_native_aarch64`	✅	3s	4s	-25%
`power2round`	✅	3s	4s	-25%
`reduce32`	✅	3s	3s	+0%
`rej_eta_c`	✅	3s	5s	-40%
`rej_uniform_eta_native_x86_64`	✅	3s	-	new
`shake128_init`	✅	3s	1s	+200%
`shake128_squeeze`	✅	3s	2s	+50%
`shake128x4_squeezeblocks`	✅	3s	3s	+0%
`shake256_init`	✅	3s	2s	+50%
`shake256_release`	✅	3s	3s	+0%
`shake256_squeeze`	✅	3s	2s	+50%
`sign_signature_pre_hash_internal`	✅	3s	5s	-40%
`sign_verify_extmu`	✅	3s	3s	+0%
`sign_verify_pre_hash_shake256`	✅	3s	3s	+0%
`sk_t0hat_get_poly`	✅	3s	4s	-25%
`unpack_sk_s1hat`	✅	3s	2s	+50%
`unpack_sk_s2hat`	✅	3s	3s	+0%
`decompose`	✅	2s	3s	-33%
`fqscale`	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64_v84a`	✅	2s	1s	+100%
`keccak_finalize`	✅	2s	1s	+100%
`keccak_init`	✅	2s	3s	-33%
`keccak_squeeze`	✅	2s	2s	+0%
`keccakf1600_extract_bytes (big endian)`	✅	2s	3s	-33%
`keccakf1600_xor_bytes (big endian)`	✅	2s	2s	+0%
`keccakf1600x4_permute`	✅	2s	3s	-33%
`keccakf1600x4_xor_bytes`	✅	2s	3s	-33%
`mld_ct_abs_i32`	✅	2s	3s	-33%
`mld_ct_cmask_nonzero_u32`	✅	2s	2s	+0%
`mld_ct_memcmp`	✅	2s	3s	-33%
`mld_keccakf1600x4_extract_bytes_c`	✅	2s	2s	+0%
`mld_keccakf1600x4_xor_bytes_c`	✅	2s	4s	-50%
`mld_sign_resume`	✅	2s	-	new
`mld_value_barrier_u32`	✅	2s	2s	+0%
`mld_value_barrier_u8`	✅	2s	3s	-33%
`ntt_native_aarch64`	✅	2s	6s	-67%
`pack_sig_h`	✅	2s	4s	-50%
`pointwise_native_aarch64`	✅	2s	5s	-60%
`poly_add`	✅	2s	6s	-67%
`poly_caddq_c`	✅	2s	3s	-33%
`poly_caddq_native_x86_64`	✅	2s	2s	+0%
`poly_chknorm_native_x86_64`	✅	2s	2s	+0%
`poly_decompose`	✅	2s	3s	-33%
`poly_decompose_32_native_aarch64`	✅	2s	5s	-60%
`poly_decompose_native_x86_64`	✅	2s	2s	+0%
`poly_invntt_tomont`	✅	2s	1s	+100%
`poly_ntt_native`	✅	2s	3s	-33%
`poly_permute_bitrev_to_custom_optional`	✅	2s	3s	-33%
`poly_pointwise_montgomery`	✅	2s	4s	-50%
`poly_reduce`	✅	2s	2s	+0%
`poly_sub`	✅	2s	3s	-33%
`poly_use_hint_native_aarch64`	✅	2s	2s	+0%
`polyeta_pack`	✅	2s	4s	-50%
`polyt0_pack`	✅	2s	4s	-50%
`polyveck_unpack_eta`	✅	2s	4s	-50%
`polyvecl_pointwise_acc_montgomery`	✅	2s	5s	-60%
`polyvecl_unpack_eta`	✅	2s	5s	-60%
`polyvecl_unpack_z`	✅	2s	4s	-50%
`polyw1_pack_88`	✅	2s	3s	-33%
`polyz_unpack_native`	✅	2s	4s	-50%
`rej_uniform_eta_native_aarch64`	✅	2s	5s	-60%
`shake128_release`	✅	2s	4s	-50%
`shake128x4_absorb_once`	✅	2s	5s	-60%
`shake256`	✅	2s	2s	+0%
`shake256_finalize`	✅	2s	2s	+0%
`shake256x4_absorb_once`	✅	2s	2s	+0%
`shake256x4_squeezeblocks`	✅	2s	1s	+100%
`sign_verify`	✅	2s	5s	-60%
`sign_verify_pre_hash_internal`	✅	2s	3s	-33%
`sk_s1hat_get_poly`	✅	2s	3s	-33%
`sys_check_capability`	✅	2s	3s	-33%
`unpack_sk`	✅	2s	5s	-60%
`use_hint`	✅	2s	3s	-33%
`yvec_get_poly`	✅	2s	4s	-50%
`caddq`	✅	1s	4s	-75%
`intt_native_x86_64`	✅	1s	3s	-67%
`keccak_f1600_x1_native_aarch64`	✅	1s	1s	+0%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	1s	3s	-67%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	1s	4s	-75%
`keccak_f1600_x4_native_avx2`	✅	1s	2s	-50%
`keccakf1600_permute`	✅	1s	3s	-67%
`keccakf1600_permute_native`	✅	1s	4s	-75%
`keccakf1600x4_extract_bytes`	✅	1s	2s	-50%
`keccakf1600x4_extract_bytes_native`	✅	1s	2s	-50%
`keccakf1600x4_xor_bytes_native`	✅	1s	3s	-67%
`mld_ct_cmask_neg_i32`	✅	1s	4s	-75%
`mld_ct_get_optblocker_i64`	✅	1s	3s	-67%
`mld_ct_sel_int32`	✅	1s	3s	-67%
`mld_keccakf1600_extract_bytes`	✅	1s	4s	-75%
`mld_value_barrier_i64`	✅	1s	1s	+0%
`nttunpack_native_x86_64`	✅	1s	3s	-67%
`poly_caddq`	✅	1s	2s	-50%
`poly_caddq_native`	✅	1s	4s	-75%
`poly_caddq_native_aarch64`	✅	1s	3s	-67%
`poly_pointwise_montgomery_native`	✅	1s	5s	-80%
`poly_shiftl`	✅	1s	4s	-75%
`polyveck_pack_eta`	✅	1s	6s	-83%
`polyvecl_pack_eta`	✅	1s	3s	-67%
`polyvecl_uniform_gamma1_serial`	✅	1s	4s	-75%
`polyw1_pack`	✅	1s	4s	-75%
`polyz_unpack`	✅	1s	2s	-50%
`polyz_unpack_native_x86_64`	✅	1s	3s	-67%
`rej_eta`	✅	1s	4s	-75%
`shake128_absorb`	✅	1s	4s	-75%
`shake128_finalize`	✅	1s	2s	-50%
`sk_s2hat_get_poly`	✅	1s	3s	-67%
`unpack_sk_t0hat`	✅	1s	7s	-86%

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 · 2026-08-03T02:04:38Z

Hello @mkannwischer @hanno-becker, appologies for the delay with this, I got quite distracted with a math paper i was working on this last month 😆 . This should be ready for review now, the check theorems script is slightly different here than what it is in mlkem as it also treats the IBT case.

oqs-bot · 2026-08-03T02:20:17Z

CBMC Results (ML-DSA-44, REDUCE-RAM)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`compute_pack_t0_t1`	⚠️	29s	12s	+142%
`mld_attempt_signature_generation`	⚠️	145s	19s	+663%
`sign_pk_from_sk`	⚠️	41s	5s	+720%
`sign_verify_internal`	⚠️	158s	49s	+222%

Full Results (210 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	1233s	1364s	-9.6%
`sign_verify_internal`	⚠️	158s	49s	+222%
`mld_attempt_signature_generation`	⚠️	145s	19s	+663%
`polyvec_matrix_pointwise_montgomery_yvec`	✅	95s	149s	-36%
`poly_pointwise_montgomery_c`	✅	65s	112s	-42%
`mld_invntt_layer`	✅	52s	105s	-50%
`sign_pk_from_sk`	⚠️	41s	5s	+720%
`compute_pack_t0_t1`	⚠️	29s	12s	+142%
`fqmul`	✅	21s	39s	-46%
`mld_ntt_layer`	✅	20s	41s	-51%
`sign_keypair_internal`	✅	19s	4s	+375%
`keccakf1600x4_permute_native`	✅	12s	22s	-45%
`sign_signature_internal`	✅	12s	4s	+200%
`poly_ntt_c`	✅	11s	21s	-48%
`rej_uniform_c`	✅	10s	16s	-38%
`sig_unpack_hints`	✅	10s	2s	+400%
`mld_ntt_butterfly_block`	✅	9s	23s	-61%
`poly_uniform_eta_4x`	✅	9s	12s	-25%
`polyt0_unpack`	✅	9s	12s	-25%
`rej_uniform`	✅	9s	8s	+12%
`mld_check_pct`	✅	8s	15s	-47%
`poly_chknorm_c`	✅	8s	11s	-27%
`poly_invntt_tomont_c`	✅	7s	11s	-36%
`polyeta_unpack`	✅	7s	14s	-50%
`polyz_unpack_c`	✅	7s	8s	-12%
`rej_uniform_native_x86_64`	✅	7s	-	new
`sign_verify_extmu`	✅	7s	5s	+40%
`keccak_absorb_once_x4`	✅	6s	8s	-25%
`pointwise_acc_native_x86_64`	✅	6s	4s	+50%
`polyvec_matrix_pointwise_montgomery_row`	✅	6s	6s	+0%
`sign_keypair`	✅	6s	5s	+20%
`keccak_squeezeblocks_x4`	✅	5s	3s	+67%
`ntt_native_x86_64`	✅	5s	3s	+67%
`polyt1_unpack`	✅	5s	2s	+150%
`rej_uniform_native_aarch64`	✅	5s	3s	+67%
`keccak_absorb`	✅	4s	3s	+33%
`keccakf1600_permute_native`	✅	4s	3s	+33%
`keccakf1600x4_xor_bytes`	✅	4s	3s	+33%
`mld_ct_get_optblocker_i64`	✅	4s	4s	+0%
`mld_ct_sel_int32`	✅	4s	3s	+33%
`mld_keccakf1600_permute_c`	✅	4s	7s	-43%
`mld_sample_s1_s2`	✅	4s	1s	+300%
`pack_sk_rho_key_tr_s2`	✅	4s	5s	-20%
`poly_add`	✅	4s	7s	-43%
`poly_caddq`	✅	4s	4s	+0%
`poly_caddq_native_aarch64`	✅	4s	3s	+33%
`poly_decompose_native`	✅	4s	2s	+100%
`poly_pointwise_montgomery`	✅	4s	3s	+33%
`poly_uniform_gamma1`	✅	4s	3s	+33%
`poly_use_hint_c`	✅	4s	5s	-20%
`polyveck_unpack_eta`	✅	4s	2s	+100%
`polyvecl_chknorm`	✅	4s	11s	-64%
`polyz_unpack_17_native_aarch64`	✅	4s	2s	+100%
`polyz_unpack_native`	✅	4s	3s	+33%
`polyz_unpack_native_x86_64`	✅	4s	3s	+33%
`sign_signature_pre_hash_internal`	✅	4s	4s	+0%
`sign_signature_pre_hash_shake256`	✅	4s	4s	+0%
`sign_verify`	✅	4s	4s	+0%
`fqscale`	✅	3s	2s	+50%
`keccak_f1600_x1_native_aarch64`	✅	3s	3s	+0%
`keccak_f1600_x4_native_aarch64_v84a`	✅	3s	3s	+0%
`keccak_squeeze`	✅	3s	2s	+50%
`keccakf1600_extract_bytes (big endian)`	✅	3s	4s	-25%
`keccakf1600_xor_bytes (big endian)`	✅	3s	6s	-50%
`make_hint`	✅	3s	3s	+0%
`mld_compute_pack_z`	✅	3s	6s	-50%
`mld_ct_cmask_nonzero_u8`	✅	3s	2s	+50%
`mld_h`	✅	3s	4s	-25%
`mld_sign_attempt`	✅	3s	-	new
`mld_sign_resume`	✅	3s	-	new
`mld_value_barrier_u32`	✅	3s	1s	+200%
`mld_value_barrier_u8`	✅	3s	4s	-25%
`nttunpack_native_x86_64`	✅	3s	4s	-25%
`pack_sig_h`	✅	3s	4s	-25%
`pointwise_acc_native_aarch64`	✅	3s	6s	-50%
`pointwise_native_aarch64`	✅	3s	2s	+50%
`poly_challenge`	✅	3s	6s	-50%
`poly_chknorm_native_aarch64`	✅	3s	2s	+50%
`poly_chknorm_native_x86_64`	✅	3s	2s	+50%
`poly_decompose_32_native_aarch64`	✅	3s	4s	-25%
`poly_decompose_88_native_aarch64`	✅	3s	3s	+0%
`poly_invntt_tomont`	✅	3s	2s	+50%
`poly_reduce`	✅	3s	4s	-25%
`poly_uniform`	✅	3s	3s	+0%
`poly_uniform_4x`	✅	3s	3s	+0%
`poly_use_hint`	✅	3s	2s	+50%
`poly_use_hint_native_aarch64`	✅	3s	3s	+0%
`polyveck_decompose`	✅	3s	7s	-57%
`polyvecl_ntt`	✅	3s	3s	+0%
`polyvecl_pointwise_acc_montgomery`	✅	3s	3s	+0%
`polyvecl_uniform_gamma1`	✅	3s	2s	+50%
`polyvecl_uniform_gamma1_serial`	✅	3s	2s	+50%
`polyvecl_unpack_eta`	✅	3s	4s	-25%
`shake128x4_squeezeblocks`	✅	3s	2s	+50%
`shake256`	✅	3s	1s	+200%
`shake256_finalize`	✅	3s	2s	+50%
`shake256_init`	✅	3s	4s	-25%
`shake256_squeeze`	✅	3s	2s	+50%
`shake256x4_squeezeblocks`	✅	3s	2s	+50%
`sign_signature`	✅	3s	6s	-50%
`sign_verify_pre_hash_shake256`	✅	3s	5s	-40%
`sk_s2hat_get_poly`	✅	3s	5s	-40%
`caddq`	✅	2s	6s	-67%
`decompose`	✅	2s	3s	-33%
`intt_native_aarch64`	✅	2s	3s	-33%
`intt_native_x86_64`	✅	2s	2s	+0%
`keccak_f1600_x1_native_aarch64_v84a`	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	2s	3s	-33%
`keccak_f1600_x4_native_avx2`	✅	2s	2s	+0%
`keccakf1600x4_xor_bytes_native`	✅	2s	5s	-60%
`mld_ct_cmask_neg_i32`	✅	2s	2s	+0%
`mld_ct_cmask_nonzero_u32`	✅	2s	3s	-33%
`mld_ct_get_optblocker_u8`	✅	2s	2s	+0%
`mld_ct_memcmp`	✅	2s	1s	+100%
`mld_keccakf1600x4_xor_bytes_c`	✅	2s	4s	-50%
`mld_polymat_expand_entry`	✅	2s	2s	+0%
`mld_prepare_domain_separation_prefix`	✅	2s	3s	-33%
`mld_sample_s1_s2_serial`	✅	2s	4s	-50%
`mld_value_barrier_i64`	✅	2s	3s	-33%
`montgomery_reduce`	✅	2s	2s	+0%
`pack_sig_z`	✅	2s	2s	+0%
`pack_sk_s1`	✅	2s	3s	-33%
`pointwise_native_x86_64`	✅	2s	4s	-50%
`poly_caddq_c`	✅	2s	3s	-33%
`poly_caddq_native_x86_64`	✅	2s	4s	-50%
`poly_chknorm`	✅	2s	3s	-33%
`poly_chknorm_native`	✅	2s	4s	-50%
`poly_decompose`	✅	2s	2s	+0%
`poly_decompose_c`	✅	2s	5s	-60%
`poly_decompose_native_x86_64`	✅	2s	2s	+0%
`poly_ntt_native`	✅	2s	3s	-33%
`poly_pointwise_montgomery_native`	✅	2s	2s	+0%
`poly_power2round`	✅	2s	4s	-50%
`poly_shiftl`	✅	2s	4s	-50%
`poly_use_hint_native_x86_64`	✅	2s	-	new
`polyeta_pack`	✅	2s	3s	-33%
`polyt0_pack`	✅	2s	4s	-50%
`polyvec_matrix_expand`	✅	2s	3s	-33%
`polyveck_chknorm`	✅	2s	67s	-97%
`polyveck_invntt_tomont`	✅	2s	5s	-60%
`polyveck_ntt`	✅	2s	2s	+0%
`polyveck_pack_eta`	✅	2s	4s	-50%
`polyveck_reduce`	✅	2s	4s	-50%
`polyvecl_pack_eta`	✅	2s	2s	+0%
`polyvecl_pointwise_acc_montgomery_c`	✅	2s	4s	-50%
`polyvecl_pointwise_acc_montgomery_native`	✅	2s	3s	-33%
`polyw1_pack`	✅	2s	4s	-50%
`polyw1_pack_32`	✅	2s	3s	-33%
`polyw1_pack_88`	✅	2s	2s	+0%
`polyz_unpack_19_native_aarch64`	✅	2s	4s	-50%
`reduce32`	✅	2s	3s	-33%
`rej_eta`	✅	2s	5s	-60%
`rej_eta_native`	✅	2s	3s	-33%
`rej_uniform_eta_native_aarch64`	✅	2s	3s	-33%
`rej_uniform_eta_native_x86_64`	✅	2s	-	new
`rej_uniform_native`	✅	2s	5s	-60%
`shake128_absorb`	✅	2s	3s	-33%
`shake128_finalize`	✅	2s	3s	-33%
`shake128_init`	✅	2s	2s	+0%
`shake128_release`	✅	2s	2s	+0%
`shake128_squeeze`	✅	2s	2s	+0%
`shake256_absorb`	✅	2s	2s	+0%
`shake256x4_absorb_once`	✅	2s	1s	+100%
`sign_signature_extmu`	✅	2s	4s	-50%
`sign_verify_pre_hash_internal`	✅	2s	5s	-60%
`sk_s1hat_get_poly`	✅	2s	2s	+0%
`sys_check_capability`	✅	2s	2s	+0%
`unpack_sk_s1hat`	✅	2s	3s	-33%
`unpack_sk_s2hat`	✅	2s	4s	-50%
`unpack_sk_t0hat`	✅	2s	2s	+0%
`yvec_init`	✅	2s	1s	+100%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	1s	2s	-50%
`keccak_finalize`	✅	1s	2s	-50%
`keccak_init`	✅	1s	3s	-67%
`keccakf1600_permute`	✅	1s	2s	-50%
`keccakf1600_xor_bytes`	✅	1s	3s	-67%
`keccakf1600x4_extract_bytes`	✅	1s	2s	-50%
`keccakf1600x4_extract_bytes_native`	✅	1s	4s	-75%
`keccakf1600x4_permute`	✅	1s	4s	-75%
`mld_ct_abs_i32`	✅	1s	3s	-67%
`mld_ct_get_optblocker_u32`	✅	1s	2s	-50%
`mld_keccakf1600_extract_bytes`	✅	1s	2s	-50%
`mld_keccakf1600x4_extract_bytes_c`	✅	1s	4s	-75%
`mld_sign_finish`	✅	1s	-	new
`ntt_native_aarch64`	✅	1s	4s	-75%
`pack_sig_c`	✅	1s	5s	-80%
`poly_caddq_native`	✅	1s	3s	-67%
`poly_invntt_tomont_native`	✅	1s	3s	-67%
`poly_ntt`	✅	1s	3s	-67%
`poly_permute_bitrev_to_custom_optional`	✅	1s	5s	-80%
`poly_permute_bitrev_to_custom_optional_native`	✅	1s	3s	-67%
`poly_sub`	✅	1s	3s	-67%
`poly_uniform_eta`	✅	1s	2s	-50%
`poly_uniform_gamma1_4x`	✅	1s	5s	-80%
`poly_use_hint_native`	✅	1s	3s	-67%
`polyt1_pack`	✅	1s	3s	-67%
`polyvec_matrix_expand_serial`	✅	1s	4s	-75%
`polyveck_caddq`	✅	1s	3s	-67%
`polyveck_pack_w1`	✅	1s	3s	-67%
`polyvecl_unpack_z`	✅	1s	3s	-67%
`polyz_pack`	✅	1s	2s	-50%
`polyz_unpack`	✅	1s	3s	-67%
`power2round`	✅	1s	2s	-50%
`rej_eta_c`	✅	1s	4s	-75%
`shake128x4_absorb_once`	✅	1s	2s	-50%
`shake256_release`	✅	1s	1s	+0%
`sk_t0hat_get_poly`	✅	1s	1s	+0%
`unpack_pk_t1`	✅	1s	3s	-67%
`unpack_sk`	✅	1s	3s	-67%
`use_hint`	✅	1s	2s	-50%
`yvec_get_poly`	✅	1s	3s	-67%

oqs-bot · 2026-08-03T02:20:21Z

CBMC Results (ML-DSA-87, REDUCE-RAM)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`compute_pack_t0_t1`	⚠️	27s	12s	+125%
`mld_attempt_signature_generation`	⚠️	233s	34s	+585%
`sign_keypair_internal`	⚠️	44s	6s	+633%
`sign_pk_from_sk`	⚠️	60s	6s	+900%
`sign_verify_internal`	⚠️	299s	47s	+536%

Full Results (210 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	1611s	1436s	+12.2%
`sign_verify_internal`	⚠️	299s	47s	+536%
`mld_attempt_signature_generation`	⚠️	233s	34s	+585%
`polyvec_matrix_pointwise_montgomery_yvec`	✅	192s	196s	-2%
`poly_pointwise_montgomery_c`	✅	63s	125s	-50%
`sign_pk_from_sk`	⚠️	60s	6s	+900%
`mld_invntt_layer`	✅	54s	111s	-51%
`sign_keypair_internal`	⚠️	44s	6s	+633%
`compute_pack_t0_t1`	⚠️	27s	12s	+125%
`fqmul`	✅	22s	39s	-44%
`mld_ntt_layer`	✅	19s	44s	-57%
`keccakf1600x4_permute_native`	✅	14s	25s	-44%
`sig_unpack_hints`	✅	13s	4s	+225%
`sign_signature_internal`	✅	13s	3s	+333%
`poly_ntt_c`	✅	10s	19s	-47%
`rej_uniform_c`	✅	10s	18s	-44%
`mld_ntt_butterfly_block`	✅	9s	23s	-61%
`polyt0_unpack`	✅	9s	14s	-36%
`rej_uniform`	✅	9s	7s	+29%
`polyeta_unpack`	✅	8s	13s	-38%
`rej_uniform_native_x86_64`	✅	8s	-	new
`polyveck_decompose`	✅	7s	12s	-42%
`keccak_absorb_once_x4`	✅	6s	8s	-25%
`pointwise_acc_native_aarch64`	✅	6s	5s	+20%
`poly_chknorm_c`	✅	6s	13s	-54%
`poly_invntt_tomont_c`	✅	6s	9s	-33%
`poly_uniform_eta_4x`	✅	6s	12s	-50%
`polyveck_invntt_tomont`	✅	6s	4s	+50%
`sign_keypair`	✅	6s	4s	+50%
`mld_check_pct`	✅	5s	15s	-67%
`mld_keccakf1600_permute_c`	✅	5s	8s	-38%
`mld_keccakf1600x4_extract_bytes_c`	✅	5s	3s	+67%
`mld_polymat_expand_entry`	✅	5s	4s	+25%
`mld_sample_s1_s2_serial`	✅	5s	6s	-17%
`poly_use_hint_native_x86_64`	✅	5s	-	new
`rej_uniform_native`	✅	5s	5s	+0%
`sign_signature_extmu`	✅	5s	4s	+25%
`sign_signature_pre_hash_shake256`	✅	5s	3s	+67%
`sys_check_capability`	✅	5s	2s	+150%
`caddq`	✅	4s	3s	+33%
`keccak_f1600_x1_native_aarch64_v84a`	✅	4s	2s	+100%
`mld_ct_memcmp`	✅	4s	1s	+300%
`mld_keccakf1600_extract_bytes`	✅	4s	1s	+300%
`pack_sig_c`	✅	4s	2s	+100%
`pointwise_acc_native_x86_64`	✅	4s	8s	-50%
`poly_decompose_32_native_aarch64`	✅	4s	3s	+33%
`poly_decompose_c`	✅	4s	6s	-33%
`poly_use_hint_c`	✅	4s	4s	+0%
`polyt1_pack`	✅	4s	5s	-20%
`polyvec_matrix_expand`	✅	4s	3s	+33%
`polyveck_unpack_eta`	✅	4s	3s	+33%
`polyvecl_chknorm`	✅	4s	38s	-89%
`polyvecl_ntt`	✅	4s	8s	-50%
`polyz_unpack_native_x86_64`	✅	4s	3s	+33%
`power2round`	✅	4s	3s	+33%
`shake256x4_absorb_once`	✅	4s	5s	-20%
`sign_verify_pre_hash_shake256`	✅	4s	7s	-43%
`yvec_init`	✅	4s	4s	+0%
`decompose`	✅	3s	2s	+50%
`intt_native_aarch64`	✅	3s	4s	-25%
`intt_native_x86_64`	✅	3s	4s	-25%
`keccak_absorb`	✅	3s	4s	-25%
`keccak_f1600_x4_native_aarch64_v84a`	✅	3s	1s	+200%
`keccak_squeeze`	✅	3s	5s	-40%
`keccak_squeezeblocks_x4`	✅	3s	4s	-25%
`keccakf1600_permute`	✅	3s	2s	+50%
`make_hint`	✅	3s	2s	+50%
`mld_compute_pack_z`	✅	3s	6s	-50%
`mld_ct_get_optblocker_u32`	✅	3s	2s	+50%
`mld_h`	✅	3s	2s	+50%
`mld_keccakf1600x4_xor_bytes_c`	✅	3s	1s	+200%
`mld_prepare_domain_separation_prefix`	✅	3s	3s	+0%
`mld_value_barrier_u8`	✅	3s	2s	+50%
`montgomery_reduce`	✅	3s	2s	+50%
`pack_sig_z`	✅	3s	3s	+0%
`pointwise_native_x86_64`	✅	3s	5s	-40%
`poly_caddq`	✅	3s	5s	-40%
`poly_caddq_native_aarch64`	✅	3s	3s	+0%
`poly_chknorm_native`	✅	3s	1s	+200%
`poly_chknorm_native_x86_64`	✅	3s	2s	+50%
`poly_permute_bitrev_to_custom_optional_native`	✅	3s	3s	+0%
`poly_reduce`	✅	3s	4s	-25%
`poly_use_hint`	✅	3s	4s	-25%
`poly_use_hint_native`	✅	3s	1s	+200%
`polyt1_unpack`	✅	3s	3s	+0%
`polyvec_matrix_expand_serial`	✅	3s	3s	+0%
`polyvec_matrix_pointwise_montgomery_row`	✅	3s	13s	-77%
`polyveck_caddq`	✅	3s	8s	-62%
`polyveck_chknorm`	✅	3s	9s	-67%
`polyveck_reduce`	✅	3s	6s	-50%
`polyvecl_pack_eta`	✅	3s	2s	+50%
`polyvecl_pointwise_acc_montgomery`	✅	3s	2s	+50%
`polyvecl_uniform_gamma1`	✅	3s	3s	+0%
`polyvecl_uniform_gamma1_serial`	✅	3s	2s	+50%
`polyz_unpack`	✅	3s	3s	+0%
`polyz_unpack_17_native_aarch64`	✅	3s	4s	-25%
`reduce32`	✅	3s	3s	+0%
`rej_eta_native`	✅	3s	4s	-25%
`rej_uniform_eta_native_aarch64`	✅	3s	3s	+0%
`rej_uniform_native_aarch64`	✅	3s	3s	+0%
`shake128_absorb`	✅	3s	2s	+50%
`shake256_finalize`	✅	3s	3s	+0%
`shake256_init`	✅	3s	3s	+0%
`shake256x4_squeezeblocks`	✅	3s	4s	-25%
`sign_signature`	✅	3s	4s	-25%
`sign_verify`	✅	3s	2s	+50%
`sign_verify_extmu`	✅	3s	4s	-25%
`unpack_sk_s1hat`	✅	3s	3s	+0%
`unpack_sk_t0hat`	✅	3s	4s	-25%
`fqscale`	✅	2s	1s	+100%
`keccak_f1600_x1_native_aarch64`	✅	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%
`keccakf1600_extract_bytes (big endian)`	✅	2s	3s	-33%
`keccakf1600_permute_native`	✅	2s	3s	-33%
`keccakf1600_xor_bytes`	✅	2s	1s	+100%
`keccakf1600x4_extract_bytes_native`	✅	2s	4s	-50%
`keccakf1600x4_xor_bytes_native`	✅	2s	2s	+0%
`mld_ct_cmask_nonzero_u32`	✅	2s	5s	-60%
`mld_ct_cmask_nonzero_u8`	✅	2s	2s	+0%
`mld_ct_get_optblocker_u8`	✅	2s	3s	-33%
`mld_ct_sel_int32`	✅	2s	2s	+0%
`mld_sample_s1_s2`	✅	2s	8s	-75%
`mld_sign_finish`	✅	2s	-	new
`mld_sign_resume`	✅	2s	-	new
`mld_value_barrier_u32`	✅	2s	3s	-33%
`ntt_native_aarch64`	✅	2s	4s	-50%
`ntt_native_x86_64`	✅	2s	2s	+0%
`nttunpack_native_x86_64`	✅	2s	3s	-33%
`pack_sig_h`	✅	2s	3s	-33%
`pack_sk_rho_key_tr_s2`	✅	2s	2s	+0%
`pack_sk_s1`	✅	2s	2s	+0%
`pointwise_native_aarch64`	✅	2s	4s	-50%
`poly_add`	✅	2s	8s	-75%
`poly_caddq_c`	✅	2s	3s	-33%
`poly_caddq_native`	✅	2s	3s	-33%
`poly_chknorm_native_aarch64`	✅	2s	5s	-60%
`poly_decompose`	✅	2s	2s	+0%
`poly_decompose_88_native_aarch64`	✅	2s	2s	+0%
`poly_invntt_tomont`	✅	2s	4s	-50%
`poly_invntt_tomont_native`	✅	2s	2s	+0%
`poly_ntt_native`	✅	2s	4s	-50%
`poly_permute_bitrev_to_custom_optional`	✅	2s	2s	+0%
`poly_power2round`	✅	2s	7s	-71%
`poly_sub`	✅	2s	5s	-60%
`poly_uniform`	✅	2s	4s	-50%
`poly_uniform_4x`	✅	2s	3s	-33%
`poly_use_hint_native_aarch64`	✅	2s	3s	-33%
`polyt0_pack`	✅	2s	3s	-33%
`polyveck_ntt`	✅	2s	3s	-33%
`polyveck_pack_eta`	✅	2s	5s	-60%
`polyveck_pack_w1`	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery_c`	✅	2s	2s	+0%
`polyvecl_pointwise_acc_montgomery_native`	✅	2s	2s	+0%
`polyw1_pack_32`	✅	2s	3s	-33%
`polyz_pack`	✅	2s	4s	-50%
`polyz_unpack_19_native_aarch64`	✅	2s	5s	-60%
`polyz_unpack_c`	✅	2s	7s	-71%
`polyz_unpack_native`	✅	2s	1s	+100%
`rej_eta`	✅	2s	2s	+0%
`rej_eta_c`	✅	2s	4s	-50%
`shake128_init`	✅	2s	2s	+0%
`shake128_release`	✅	2s	3s	-33%
`shake128_squeeze`	✅	2s	1s	+100%
`shake256`	✅	2s	3s	-33%
`shake256_squeeze`	✅	2s	2s	+0%
`sign_signature_pre_hash_internal`	✅	2s	2s	+0%
`sign_verify_pre_hash_internal`	✅	2s	3s	-33%
`sk_t0hat_get_poly`	✅	2s	3s	-33%
`unpack_sk`	✅	2s	4s	-50%
`unpack_sk_s2hat`	✅	2s	3s	-33%
`use_hint`	✅	2s	3s	-33%
`yvec_get_poly`	✅	2s	2s	+0%
`keccak_finalize`	✅	1s	1s	+0%
`keccak_init`	✅	1s	1s	+0%
`keccakf1600_xor_bytes (big endian)`	✅	1s	2s	-50%
`keccakf1600x4_extract_bytes`	✅	1s	1s	+0%
`keccakf1600x4_permute`	✅	1s	2s	-50%
`keccakf1600x4_xor_bytes`	✅	1s	1s	+0%
`mld_ct_abs_i32`	✅	1s	1s	+0%
`mld_ct_cmask_neg_i32`	✅	1s	2s	-50%
`mld_ct_get_optblocker_i64`	✅	1s	2s	-50%
`mld_sign_attempt`	✅	1s	-	new
`mld_value_barrier_i64`	✅	1s	2s	-50%
`poly_caddq_native_x86_64`	✅	1s	3s	-67%
`poly_challenge`	✅	1s	4s	-75%
`poly_chknorm`	✅	1s	4s	-75%
`poly_decompose_native`	✅	1s	2s	-50%
`poly_decompose_native_x86_64`	✅	1s	3s	-67%
`poly_ntt`	✅	1s	2s	-50%
`poly_pointwise_montgomery`	✅	1s	3s	-67%
`poly_pointwise_montgomery_native`	✅	1s	3s	-67%
`poly_shiftl`	✅	1s	4s	-75%
`poly_uniform_eta`	✅	1s	5s	-80%
`poly_uniform_gamma1`	✅	1s	3s	-67%
`poly_uniform_gamma1_4x`	✅	1s	3s	-67%
`polyeta_pack`	✅	1s	3s	-67%
`polyvecl_unpack_eta`	✅	1s	3s	-67%
`polyvecl_unpack_z`	✅	1s	3s	-67%
`polyw1_pack`	✅	1s	2s	-50%
`polyw1_pack_88`	✅	1s	2s	-50%
`rej_uniform_eta_native_x86_64`	✅	1s	-	new
`shake128_finalize`	✅	1s	2s	-50%
`shake128x4_absorb_once`	✅	1s	4s	-75%
`shake128x4_squeezeblocks`	✅	1s	1s	+0%
`shake256_absorb`	✅	1s	3s	-67%
`shake256_release`	✅	1s	5s	-80%
`sk_s1hat_get_poly`	✅	1s	3s	-67%
`sk_s2hat_get_poly`	✅	1s	2s	-50%
`unpack_pk_t1`	✅	1s	2s	-50%

oqs-bot · 2026-08-03T02:24:11Z

CBMC Results (ML-DSA-65, REDUCE-RAM)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`compute_pack_t0_t1`	⚠️	32s	7s	+357%
`mld_attempt_signature_generation`	⚠️	154s	31s	+397%
`sign_keypair_internal`	⚠️	30s	3s	+900%
`sign_pk_from_sk`	⚠️	59s	5s	+1080%
`sign_verify_internal`	⚠️	183s	71s	+158%

Full Results (210 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	1428s	1482s	-3.6%
`sign_verify_internal`	⚠️	183s	71s	+158%
`mld_attempt_signature_generation`	⚠️	154s	31s	+397%
`polyvec_matrix_pointwise_montgomery_yvec`	✅	147s	201s	-27%
`poly_pointwise_montgomery_c`	✅	70s	116s	-40%
`mld_invntt_layer`	✅	59s	108s	-45%
`sign_pk_from_sk`	⚠️	59s	5s	+1080%
`polyvecl_chknorm`	✅	57s	43s	+33%
`compute_pack_t0_t1`	⚠️	32s	7s	+357%
`sign_keypair_internal`	⚠️	30s	3s	+900%
`fqmul`	✅	24s	40s	-40%
`mld_ntt_layer`	✅	22s	43s	-49%
`rej_uniform_c`	✅	13s	16s	-19%
`keccakf1600x4_permute_native`	✅	12s	22s	-45%
`sign_signature_internal`	✅	12s	6s	+100%
`sig_unpack_hints`	✅	11s	1s	+1000%
`mld_ntt_butterfly_block`	✅	10s	25s	-60%
`polyt0_unpack`	✅	10s	13s	-23%
`poly_ntt_c`	✅	9s	22s	-59%
`poly_uniform_eta_4x`	✅	9s	13s	-31%
`polyveck_decompose`	✅	9s	14s	-36%
`rej_uniform`	✅	9s	7s	+29%
`rej_uniform_native_x86_64`	✅	8s	-	new
`polyveck_caddq`	✅	7s	7s	+0%
`poly_invntt_tomont_c`	✅	6s	10s	-40%
`sign_keypair`	✅	6s	4s	+50%
`sign_signature`	✅	6s	5s	+20%
`keccak_absorb_once_x4`	✅	5s	10s	-50%
`mld_check_pct`	✅	5s	12s	-58%
`mld_compute_pack_z`	✅	5s	5s	+0%
`mld_keccakf1600_permute_c`	✅	5s	7s	-29%
`pointwise_acc_native_x86_64`	✅	5s	5s	+0%
`poly_power2round`	✅	5s	7s	-29%
`poly_use_hint`	✅	5s	3s	+67%
`polyeta_unpack`	✅	5s	4s	+25%
`polyvec_matrix_expand`	✅	5s	6s	-17%
`polyveck_invntt_tomont`	✅	5s	7s	-29%
`polyvecl_ntt`	✅	5s	7s	-29%
`polyz_unpack_native_x86_64`	✅	5s	3s	+67%
`rej_uniform_eta_native_aarch64`	✅	5s	5s	+0%
`caddq`	✅	4s	2s	+100%
`keccak_absorb`	✅	4s	3s	+33%
`mld_h`	✅	4s	3s	+33%
`mld_sign_attempt`	✅	4s	-	new
`mld_sign_finish`	✅	4s	-	new
`mld_sign_resume`	✅	4s	-	new
`mld_value_barrier_u8`	✅	4s	1s	+300%
`poly_add`	✅	4s	7s	-43%
`poly_chknorm_c`	✅	4s	13s	-69%
`poly_decompose`	✅	4s	2s	+100%
`poly_invntt_tomont_native`	✅	4s	5s	-20%
`poly_ntt`	✅	4s	2s	+100%
`polyvec_matrix_pointwise_montgomery_row`	✅	4s	8s	-50%
`polyveck_reduce`	✅	4s	6s	-33%
`polyvecl_pointwise_acc_montgomery`	✅	4s	3s	+33%
`polyz_unpack_native`	✅	4s	3s	+33%
`rej_uniform_native`	✅	4s	4s	+0%
`shake256_finalize`	✅	4s	1s	+300%
`sign_signature_extmu`	✅	4s	4s	+0%
`sign_signature_pre_hash_shake256`	✅	4s	7s	-43%
`intt_native_aarch64`	✅	3s	2s	+50%
`keccakf1600x4_extract_bytes`	✅	3s	4s	-25%
`keccakf1600x4_extract_bytes_native`	✅	3s	1s	+200%
`make_hint`	✅	3s	3s	+0%
`mld_ct_get_optblocker_u32`	✅	3s	3s	+0%
`mld_ct_get_optblocker_u8`	✅	3s	4s	-25%
`mld_ct_memcmp`	✅	3s	4s	-25%
`mld_keccakf1600x4_extract_bytes_c`	✅	3s	2s	+50%
`mld_sample_s1_s2_serial`	✅	3s	3s	+0%
`ntt_native_x86_64`	✅	3s	5s	-40%
`nttunpack_native_x86_64`	✅	3s	3s	+0%
`pack_sig_z`	✅	3s	1s	+200%
`pack_sk_rho_key_tr_s2`	✅	3s	2s	+50%
`pointwise_acc_native_aarch64`	✅	3s	6s	-50%
`pointwise_native_aarch64`	✅	3s	3s	+0%
`poly_caddq`	✅	3s	3s	+0%
`poly_caddq_native`	✅	3s	4s	-25%
`poly_chknorm_native`	✅	3s	4s	-25%
`poly_chknorm_native_x86_64`	✅	3s	4s	-25%
`poly_decompose_32_native_aarch64`	✅	3s	4s	-25%
`poly_decompose_c`	✅	3s	8s	-62%
`poly_decompose_native_x86_64`	✅	3s	2s	+50%
`poly_ntt_native`	✅	3s	2s	+50%
`poly_pointwise_montgomery`	✅	3s	2s	+50%
`poly_sub`	✅	3s	4s	-25%
`poly_uniform_gamma1`	✅	3s	3s	+0%
`poly_use_hint_c`	✅	3s	2s	+50%
`poly_use_hint_native`	✅	3s	7s	-57%
`polyvec_matrix_expand_serial`	✅	3s	3s	+0%
`polyveck_chknorm`	✅	3s	36s	-92%
`polyveck_pack_w1`	✅	3s	4s	-25%
`polyveck_unpack_eta`	✅	3s	3s	+0%
`polyvecl_pointwise_acc_montgomery_native`	✅	3s	3s	+0%
`polyw1_pack`	✅	3s	3s	+0%
`polyz_unpack_c`	✅	3s	9s	-67%
`rej_uniform_native_aarch64`	✅	3s	5s	-40%
`shake128_finalize`	✅	3s	2s	+50%
`shake128x4_squeezeblocks`	✅	3s	2s	+50%
`shake256_init`	✅	3s	4s	-25%
`sign_verify_pre_hash_internal`	✅	3s	5s	-40%
`sign_verify_pre_hash_shake256`	✅	3s	6s	-50%
`sk_s2hat_get_poly`	✅	3s	1s	+200%
`sys_check_capability`	✅	3s	1s	+200%
`fqscale`	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64`	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	2s	3s	-33%
`keccak_f1600_x4_native_avx2`	✅	2s	2s	+0%
`keccak_finalize`	✅	2s	2s	+0%
`keccak_init`	✅	2s	4s	-50%
`keccak_squeezeblocks_x4`	✅	2s	4s	-50%
`keccakf1600_extract_bytes (big endian)`	✅	2s	3s	-33%
`keccakf1600_xor_bytes`	✅	2s	4s	-50%
`keccakf1600x4_permute`	✅	2s	1s	+100%
`keccakf1600x4_xor_bytes_native`	✅	2s	2s	+0%
`mld_ct_abs_i32`	✅	2s	6s	-67%
`mld_ct_cmask_neg_i32`	✅	2s	3s	-33%
`mld_ct_cmask_nonzero_u32`	✅	2s	3s	-33%
`mld_ct_cmask_nonzero_u8`	✅	2s	2s	+0%
`mld_ct_get_optblocker_i64`	✅	2s	1s	+100%
`mld_keccakf1600x4_xor_bytes_c`	✅	2s	2s	+0%
`mld_sample_s1_s2`	✅	2s	6s	-67%
`mld_value_barrier_u32`	✅	2s	4s	-50%
`montgomery_reduce`	✅	2s	1s	+100%
`ntt_native_aarch64`	✅	2s	3s	-33%
`pack_sig_c`	✅	2s	3s	-33%
`poly_caddq_c`	✅	2s	5s	-60%
`poly_caddq_native_x86_64`	✅	2s	1s	+100%
`poly_challenge`	✅	2s	5s	-60%
`poly_chknorm`	✅	2s	3s	-33%
`poly_chknorm_native_aarch64`	✅	2s	2s	+0%
`poly_decompose_88_native_aarch64`	✅	2s	2s	+0%
`poly_decompose_native`	✅	2s	5s	-60%
`poly_invntt_tomont`	✅	2s	5s	-60%
`poly_permute_bitrev_to_custom_optional`	✅	2s	3s	-33%
`poly_permute_bitrev_to_custom_optional_native`	✅	2s	3s	-33%
`poly_pointwise_montgomery_native`	✅	2s	4s	-50%
`poly_reduce`	✅	2s	4s	-50%
`poly_shiftl`	✅	2s	3s	-33%
`poly_uniform`	✅	2s	2s	+0%
`poly_uniform_eta`	✅	2s	5s	-60%
`poly_uniform_gamma1_4x`	✅	2s	3s	-33%
`poly_use_hint_native_aarch64`	✅	2s	4s	-50%
`poly_use_hint_native_x86_64`	✅	2s	-	new
`polyt0_pack`	✅	2s	5s	-60%
`polyt1_pack`	✅	2s	3s	-33%
`polyveck_ntt`	✅	2s	4s	-50%
`polyveck_pack_eta`	✅	2s	3s	-33%
`polyvecl_uniform_gamma1`	✅	2s	4s	-50%
`polyvecl_unpack_eta`	✅	2s	2s	+0%
`polyvecl_unpack_z`	✅	2s	1s	+100%
`polyw1_pack_32`	✅	2s	2s	+0%
`polyz_pack`	✅	2s	3s	-33%
`polyz_unpack`	✅	2s	3s	-33%
`polyz_unpack_17_native_aarch64`	✅	2s	2s	+0%
`polyz_unpack_19_native_aarch64`	✅	2s	5s	-60%
`power2round`	✅	2s	2s	+0%
`reduce32`	✅	2s	2s	+0%
`rej_eta`	✅	2s	5s	-60%
`rej_eta_c`	✅	2s	4s	-50%
`rej_eta_native`	✅	2s	3s	-33%
`rej_uniform_eta_native_x86_64`	✅	2s	-	new
`shake128_absorb`	✅	2s	2s	+0%
`shake128_release`	✅	2s	2s	+0%
`shake128_squeeze`	✅	2s	3s	-33%
`shake256_absorb`	✅	2s	4s	-50%
`shake256_release`	✅	2s	3s	-33%
`sign_verify`	✅	2s	6s	-67%
`sign_verify_extmu`	✅	2s	2s	+0%
`sk_s1hat_get_poly`	✅	2s	3s	-33%
`sk_t0hat_get_poly`	✅	2s	1s	+100%
`unpack_pk_t1`	✅	2s	2s	+0%
`unpack_sk`	✅	2s	3s	-33%
`unpack_sk_s1hat`	✅	2s	1s	+100%
`unpack_sk_s2hat`	✅	2s	3s	-33%
`yvec_get_poly`	✅	2s	3s	-33%
`decompose`	✅	1s	4s	-75%
`intt_native_x86_64`	✅	1s	4s	-75%
`keccak_f1600_x1_native_aarch64_v84a`	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v84a`	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	1s	3s	-67%
`keccak_squeeze`	✅	1s	2s	-50%
`keccakf1600_permute`	✅	1s	4s	-75%
`keccakf1600_permute_native`	✅	1s	2s	-50%
`keccakf1600_xor_bytes (big endian)`	✅	1s	2s	-50%
`keccakf1600x4_xor_bytes`	✅	1s	2s	-50%
`mld_ct_sel_int32`	✅	1s	2s	-50%
`mld_keccakf1600_extract_bytes`	✅	1s	2s	-50%
`mld_polymat_expand_entry`	✅	1s	3s	-67%
`mld_prepare_domain_separation_prefix`	✅	1s	4s	-75%
`mld_value_barrier_i64`	✅	1s	2s	-50%
`pack_sig_h`	✅	1s	2s	-50%
`pack_sk_s1`	✅	1s	3s	-67%
`pointwise_native_x86_64`	✅	1s	2s	-50%
`poly_caddq_native_aarch64`	✅	1s	2s	-50%
`poly_uniform_4x`	✅	1s	4s	-75%
`polyeta_pack`	✅	1s	1s	+0%
`polyt1_unpack`	✅	1s	3s	-67%
`polyvecl_pack_eta`	✅	1s	2s	-50%
`polyvecl_pointwise_acc_montgomery_c`	✅	1s	3s	-67%
`polyvecl_uniform_gamma1_serial`	✅	1s	1s	+0%
`polyw1_pack_88`	✅	1s	3s	-67%
`shake128_init`	✅	1s	6s	-83%
`shake128x4_absorb_once`	✅	1s	2s	-50%
`shake256`	✅	1s	2s	-50%
`shake256_squeeze`	✅	1s	4s	-75%
`shake256x4_absorb_once`	✅	1s	2s	-50%
`shake256x4_squeezeblocks`	✅	1s	2s	-50%
`sign_signature_pre_hash_internal`	✅	1s	3s	-67%
`unpack_sk_t0hat`	✅	1s	4s	-75%
`use_hint`	✅	1s	2s	-50%
`yvec_init`	✅	1s	5s	-80%

mkannwischer · 2026-08-03T02:33:07Z

Hello @mkannwischer @hanno-becker, appologies for the delay with this, I got quite distracted with a math paper i was working on this last month 😆 .

No worries. Thanks for porting this!

This should be ready for review now, the check theorems script is slightly different here than what it is in mlkem as it also treats the IBT case.

Can you elaborate why it needs to be slightly different? IBT isn't something that's specific to mldsa. Should it be ported to mlkem, too?

mkannwischer · 2026-08-03T05:36:08Z

@L-series can you please fix the DCO signoff?

L-series · 2026-08-03T20:01:02Z

Can you elaborate why it needs to be slightly different? IBT isn't something that's specific to mldsa. Should it be ported to mlkem, too?

@mkannwischer the logic for capturing the let PROVE = ... blocks in mlkem is somehow simpler than in mldsa as all the proof declarations exist on a single line and thus the grep can catch them.

In mldsa, some of the proofs occur with the following slightly more complicated patterns:

let MLDSA_NTT_SAFE =
  REWRITE_RULE [...]
  (time prove (...));;

and

 let MLDSA_REJ_UNIFORM_ETA2_NOIBT_SUBROUTINE_CORRECT =
   let correct_bound = prove ... in
   let th = prove ... in
   th;;

This occurs around a dozen times.

To generalize the logic in the list_thms script, I've made it so that we scan for the theorem producing declaration within the entire top level let NAME = xyz block.

There might be some simpler way of doing this however. Please let me know what you think!

mkannwischer

@L-series, sorry for the delay.
A few things should still be changed before we can merge this one.

mkannwischer · 2026-08-10T06:30:15Z

This file doesn't seem to align to the one in mlkem-native. Was that done intentionally?

Yes indeed, as I mentioned in the comment above, there is a divergence in the format of some of the proofs in mldsa as compared to mlkem. The grep which is used in the mlkem version of list_thms cannot capture these differences, so instead I modified the script to look at entire let name = ... prove blocks and search for the correct patterns.

This commit introduces a new flag --arch to the hol_light command of the tests script that allows user specification of which architecture to run/list the proofs for. If not passed, the behavior is unchanged. Signed-off-by: Andreas Hatziiliou <andreas.hatziiliou@savoirfairelinux.com>

L-series

The small issues are resolved, however the question of the difference in the list_thms script still persists. Please let me know if you think this approach is correct.

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. Unlike the ML-KEM theorem lister, the ML-DSA list_thms scripts scan complete top-level let bindings instead of only direct let NAME = prove lines. Several ML-DSA x86_64 safety theorems are wrapped in REWRITE_RULE around time prove, and the eta rejection-sampling subroutine theorems are built via local prove blocks or ADD_IBT_RULE aliases. The broader scan keeps those exported theorem names visible to lint without changing the proof structure. 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

L-series force-pushed the HOL-Light-CI branch 2 times, most recently from 6fbd4ae to 13638f7 Compare August 3, 2026 01:57

L-series marked this pull request as ready for review August 3, 2026 02:08

L-series force-pushed the HOL-Light-CI branch 3 times, most recently from 79190ea to 61dfaa0 Compare August 3, 2026 19:55

L-series force-pushed the HOL-Light-CI branch from 61dfaa0 to f27ff85 Compare August 3, 2026 20:03

mkannwischer added this to the v2.1 milestone Aug 4, 2026

mkannwischer requested changes Aug 10, 2026

View reviewed changes

L-series force-pushed the HOL-Light-CI branch from f27ff85 to cfc38b5 Compare August 17, 2026 00:31

L-series commented Aug 17, 2026

View reviewed changes

L-series force-pushed the HOL-Light-CI branch from cfc38b5 to fc5bb9d Compare August 17, 2026 01:17

Uh oh!

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

CBMC Results (ML-DSA-44)

Uh oh!

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

Uh oh!

CBMC Results (ML-DSA-65)

Uh oh!

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

Uh oh!

CBMC Results (ML-DSA-87)

Uh oh!

mkannwischer commented Apr 2, 2026

Uh oh!

L-series commented Aug 3, 2026

Uh oh!

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

Uh oh!

CBMC Results (ML-DSA-44, REDUCE-RAM)

Uh oh!

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

Uh oh!

CBMC Results (ML-DSA-87, REDUCE-RAM)

Uh oh!

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

Uh oh!

CBMC Results (ML-DSA-65, REDUCE-RAM)

Uh oh!

mkannwischer commented Aug 3, 2026

Uh oh!

mkannwischer commented Aug 3, 2026

Uh oh!

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

Uh oh!

Uh oh!

mkannwischer left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mkannwischer Aug 10, 2026

Choose a reason for hiding this comment

Uh oh!

L-series Aug 17, 2026

Choose a reason for hiding this comment

Uh oh!

L-series left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

L-series commented Apr 1, 2026 •

edited by mkannwischer

Loading

oqs-bot commented Apr 1, 2026 •

edited

Loading

oqs-bot commented Apr 1, 2026 •

edited

Loading

oqs-bot commented Apr 1, 2026 •

edited

Loading

oqs-bot commented Aug 3, 2026 •

edited

Loading

oqs-bot commented Aug 3, 2026 •

edited

Loading

oqs-bot commented Aug 3, 2026 •

edited

Loading

L-series commented Aug 3, 2026 •

edited

Loading