HOL-Light: Add x86 AVX2 nttunpack proof by jakemas · Pull Request #955 · pq-code-package/mldsa-native

jakemas · 2026-02-06T19:27:05Z

Resolves HOL-Light: Prove AVX2 nttunpack #913

oqs-bot · 2026-02-06T20:13:19Z

CBMC Results (ML-DSA-87)

Full Results (187 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	3341s	3296s	+1.4%
`polyvecl_pointwise_acc_montgomery_c`	✅	1087s	1162s	-6%
`mld_attempt_signature_generation`	✅	241s	228s	+6%
`polyvec_matrix_expand`	✅	186s	180s	+3%
`sign_verify_internal`	✅	177s	166s	+7%
`poly_pointwise_montgomery_c`	✅	167s	155s	+8%
`rej_uniform_native`	✅	149s	145s	+3%
`polyvec_matrix_expand_serial`	✅	127s	123s	+3%
`mld_ct_memcmp`	✅	84s	77s	+9%
`mld_invntt_layer`	✅	69s	64s	+8%
`mld_ntt_layer`	✅	53s	55s	-4%
`sign_signature_internal`	✅	38s	36s	+6%
`polymat_permute_bitrev_to_custom`	✅	29s	28s	+4%
`polyveck_invntt_tomont`	✅	29s	30s	-3%
`mld_compute_t0_t1_tr_from_sk_components`	✅	23s	24s	-4%
`poly_chknorm_c`	✅	23s	20s	+15%
`rej_uniform`	✅	22s	22s	+0%
`fqmul`	✅	20s	18s	+11%
`poly_uniform_eta_4x`	✅	20s	18s	+11%
`poly_uniform_4x`	✅	16s	14s	+14%
`rej_uniform_c`	✅	16s	16s	+0%
`keccakf1600x4_permute_native`	✅	15s	15s	+0%
`polyeta_unpack`	✅	15s	16s	-6%
`polyt0_unpack`	✅	14s	13s	+8%
`polyveck_decompose`	✅	14s	13s	+8%
`polyveck_add`	✅	13s	12s	+8%
`poly_add`	✅	12s	12s	+0%
`polyveck_power2round`	✅	12s	11s	+9%
`keccak_absorb_once_x4`	✅	11s	9s	+22%
`mld_check_pct`	✅	10s	9s	+11%
`mld_ntt_butterfly_block`	✅	10s	12s	-17%
`polyvec_matrix_pointwise_montgomery`	✅	10s	11s	-9%
`sign_pk_from_sk`	✅	10s	7s	+43%
`keccakf1600_permute_native`	✅	9s	9s	+0%
`mld_polyvecl_permute_bitrev_to_custom_native`	✅	9s	9s	+0%
`polyveck_caddq`	✅	9s	8s	+12%
`polyveck_sub`	✅	9s	5s	+80%
`unpack_sk`	✅	9s	9s	+0%
`keccak_absorb`	✅	8s	6s	+33%
`keccakf1600_permute`	✅	8s	6s	+33%
`mld_compute_pack_z`	✅	8s	4s	+100%
`mld_sample_s1_s2_serial`	✅	8s	7s	+14%
`pointwise_acc_native_x86_64`	✅	8s	6s	+33%
`poly_decompose_c`	✅	8s	7s	+14%
`polyveck_ntt`	✅	8s	8s	+0%
`polyveck_reduce`	✅	8s	11s	-27%
`polyveck_use_hint`	✅	8s	7s	+14%
`polyvecl_chknorm`	✅	8s	6s	+33%
`polyvecl_ntt`	✅	8s	8s	+0%
`polyz_unpack_c`	✅	8s	11s	-27%
`sign_open`	✅	8s	3s	+167%
`keccak_squeezeblocks_x4`	✅	7s	5s	+40%
`mld_sample_s1_s2`	✅	7s	7s	+0%
`pack_sig_z`	✅	7s	3s	+133%
`polyveck_pack_t0`	✅	7s	3s	+133%
`rej_eta_native`	✅	7s	6s	+17%
`sign_verify_pre_hash_shake256`	✅	7s	3s	+133%
`pointwise_acc_native_aarch64`	✅	6s	8s	-25%
`poly_caddq_c`	✅	6s	5s	+20%
`poly_challenge`	✅	6s	5s	+20%
`poly_invntt_tomont_native`	✅	6s	2s	+200%
`poly_pointwise_montgomery_native`	✅	6s	4s	+50%
`poly_uniform`	✅	6s	7s	-14%
`poly_uniform_eta`	✅	6s	5s	+20%
`polyveck_pointwise_poly_montgomery`	✅	6s	8s	-25%
`polyveck_shiftl`	✅	6s	6s	+0%
`unpack_hints`	✅	6s	8s	-25%
`unpack_sig`	✅	6s	2s	+200%
`keccak_squeeze`	✅	5s	3s	+67%
`poly_caddq`	✅	5s	3s	+67%
`poly_invntt_tomont`	✅	5s	3s	+67%
`poly_invntt_tomont_c`	✅	5s	3s	+67%
`poly_power2round`	✅	5s	5s	+0%
`poly_uniform_gamma1_4x`	✅	5s	3s	+67%
`polyt1_unpack`	✅	5s	1s	+400%
`polyveck_chknorm`	✅	5s	6s	-17%
`polyveck_unpack_eta`	✅	5s	5s	+0%
`polyveck_unpack_t0`	✅	5s	5s	+0%
`polyvecl_uniform_gamma1`	✅	5s	3s	+67%
`polyvecl_unpack_z`	✅	5s	4s	+25%
`sign`	✅	5s	7s	-29%
`sign_signature`	✅	5s	6s	-17%
`sign_signature_pre_hash_internal`	✅	5s	5s	+0%
`keccak_finalize`	✅	4s	2s	+100%
`keccakf1600_xor_bytes (big endian)`	✅	4s	3s	+33%
`mld_h`	✅	4s	4s	+0%
`mld_prepare_domain_separation_prefix`	✅	4s	5s	-20%
`pack_sk`	✅	4s	3s	+33%
`poly_chknorm`	✅	4s	5s	-20%
`poly_chknorm_native`	✅	4s	3s	+33%
`poly_chknorm_native_aarch64`	✅	4s	4s	+0%
`poly_decompose`	✅	4s	3s	+33%
`poly_shiftl`	✅	4s	1s	+300%
`poly_sub`	✅	4s	3s	+33%
`polyt0_pack`	✅	4s	2s	+100%
`polyveck_pack_w1`	✅	4s	2s	+100%
`polyvecl_pack_eta`	✅	4s	3s	+33%
`polyvecl_pointwise_acc_montgomery`	✅	4s	3s	+33%
`polyvecl_pointwise_acc_montgomery_native`	✅	4s	2s	+100%
`polyvecl_unpack_eta`	✅	4s	1s	+300%
`rej_eta`	✅	4s	3s	+33%
`rej_eta_c`	✅	4s	4s	+0%
`shake128_release`	✅	4s	3s	+33%
`sign_keypair_internal`	✅	4s	7s	-43%
`sign_verify`	✅	4s	6s	-33%
`sign_verify_extmu`	✅	4s	5s	-20%
`unpack_pk`	✅	4s	3s	+33%
`use_hint`	✅	4s	3s	+33%
`decompose`	✅	3s	1s	+200%
`keccak_f1600_x1_native_aarch64_v84a`	✅	3s	3s	+0%
`keccakf1600x4_extract_bytes`	✅	3s	1s	+200%
`keccakf1600x4_xor_bytes`	✅	3s	2s	+50%
`make_hint`	✅	3s	3s	+0%
`mld_ct_cmask_nonzero_u32`	✅	3s	2s	+50%
`mld_ct_get_optblocker_i64`	✅	3s	1s	+200%
`mld_ct_sel_int32`	✅	3s	2s	+50%
`mld_keccakf1600_extract_bytes`	✅	3s	2s	+50%
`mld_value_barrier_i64`	✅	3s	2s	+50%
`nttunpack_native_x86_64`	✅	3s	-	new
`pack_pk`	✅	3s	2s	+50%
`pack_sig_c`	✅	3s	6s	-50%
`pack_sig_h_poly`	✅	3s	2s	+50%
`poly_caddq_native`	✅	3s	2s	+50%
`poly_caddq_native_aarch64`	✅	3s	3s	+0%
`poly_ntt_native`	✅	3s	5s	-40%
`poly_pointwise_montgomery`	✅	3s	2s	+50%
`poly_reduce`	✅	3s	1s	+200%
`poly_use_hint`	✅	3s	2s	+50%
`poly_use_hint_native`	✅	3s	3s	+0%
`polyveck_pack_eta`	✅	3s	4s	-25%
`polyvecl_permute_bitrev_to_custom`	✅	3s	4s	-25%
`polyvecl_uniform_gamma1_serial`	✅	3s	4s	-25%
`polyw1_pack`	✅	3s	3s	+0%
`polyz_unpack`	✅	3s	4s	-25%
`reduce32`	✅	3s	2s	+50%
`shake128_absorb`	✅	3s	1s	+200%
`shake128_squeeze`	✅	3s	2s	+50%
`shake128x4_squeezeblocks`	✅	3s	2s	+50%
`shake256`	✅	3s	3s	+0%
`shake256_squeeze`	✅	3s	3s	+0%
`shake256x4_absorb_once`	✅	3s	3s	+0%
`sign_keypair`	✅	3s	3s	+0%
`sign_signature_extmu`	✅	3s	5s	-40%
`sign_verify_pre_hash_internal`	✅	3s	4s	-25%
`fqscale`	✅	2s	2s	+0%
`intt_native_x86_64`	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v84a`	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	2s	2s	+0%
`keccak_init`	✅	2s	4s	-50%
`keccakf1600_extract_bytes (big endian)`	✅	2s	1s	+100%
`keccakf1600_xor_bytes`	✅	2s	2s	+0%
`keccakf1600x4_permute`	✅	2s	4s	-50%
`mld_ct_abs_i32`	✅	2s	2s	+0%
`mld_ct_cmask_neg_i32`	✅	2s	2s	+0%
`mld_ct_cmask_nonzero_u8`	✅	2s	2s	+0%
`mld_value_barrier_u32`	✅	2s	2s	+0%
`montgomery_reduce`	✅	2s	4s	-50%
`ntt_native_aarch64`	✅	2s	4s	-50%
`ntt_native_x86_64`	✅	2s	3s	-33%
`pointwise_native_aarch64`	✅	2s	1s	+100%
`pointwise_native_x86_64`	✅	2s	4s	-50%
`poly_decompose_native`	✅	2s	4s	-50%
`poly_make_hint`	✅	2s	4s	-50%
`poly_ntt`	✅	2s	2s	+0%
`poly_ntt_c`	✅	2s	3s	-33%
`poly_uniform_gamma1`	✅	2s	4s	-50%
`poly_use_hint_c`	✅	2s	3s	-33%
`polyeta_pack`	✅	2s	3s	-33%
`polyt1_pack`	✅	2s	4s	-50%
`polyz_unpack_native`	✅	2s	3s	-33%
`shake128_finalize`	✅	2s	2s	+0%
`shake128_init`	✅	2s	1s	+100%
`shake128x4_absorb_once`	✅	2s	2s	+0%
`shake256_absorb`	✅	2s	2s	+0%
`shake256_finalize`	✅	2s	3s	-33%
`shake256_release`	✅	2s	3s	-33%
`shake256x4_squeezeblocks`	✅	2s	1s	+100%
`sign_signature_pre_hash_shake256`	✅	2s	4s	-50%
`sys_check_capability`	✅	2s	1s	+100%
`caddq`	✅	1s	3s	-67%
`keccak_f1600_x1_native_aarch64`	✅	1s	6s	-83%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	1s	1s	+0%
`mld_ct_get_optblocker_u32`	✅	1s	2s	-50%
`mld_ct_get_optblocker_u8`	✅	1s	2s	-50%
`mld_value_barrier_u8`	✅	1s	4s	-75%
`polyz_pack`	✅	1s	1s	+0%
`power2round`	✅	1s	3s	-67%
`shake256_init`	✅	1s	3s	-67%

oqs-bot · 2026-02-06T20:13:42Z

CBMC Results (ML-DSA-44)

Full Results (187 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	1836s	1828s	+0.4%
`sign_verify_internal`	✅	213s	217s	-2%
`polyvecl_pointwise_acc_montgomery_c`	✅	157s	155s	+1%
`poly_pointwise_montgomery_c`	✅	153s	139s	+10%
`rej_uniform_native`	✅	137s	136s	+1%
`mld_attempt_signature_generation`	✅	124s	123s	+1%
`mld_ct_memcmp`	✅	71s	74s	-4%
`mld_invntt_layer`	✅	64s	61s	+5%
`mld_ntt_layer`	✅	50s	50s	+0%
`polymat_permute_bitrev_to_custom`	✅	28s	27s	+4%
`polyvec_matrix_expand`	✅	25s	27s	-7%
`rej_uniform`	✅	22s	22s	+0%
`sign_signature_internal`	✅	22s	21s	+5%
`fqmul`	✅	18s	22s	-18%
`poly_chknorm_c`	✅	18s	18s	+0%
`poly_uniform_eta_4x`	✅	16s	18s	-11%
`polyeta_unpack`	✅	14s	13s	+8%
`poly_uniform_4x`	✅	13s	14s	-7%
`rej_uniform_c`	✅	13s	14s	-7%
`keccakf1600x4_permute_native`	✅	12s	13s	-8%
`mld_compute_t0_t1_tr_from_sk_components`	✅	12s	14s	-14%
`mld_ntt_butterfly_block`	✅	12s	11s	+9%
`poly_add`	✅	12s	11s	+9%
`polyt0_unpack`	✅	12s	14s	-14%
`polyz_unpack_c`	✅	12s	12s	+0%
`polyvec_matrix_expand_serial`	✅	11s	7s	+57%
`keccak_absorb_once_x4`	✅	10s	10s	+0%
`polyvec_matrix_pointwise_montgomery`	✅	10s	7s	+43%
`polyveck_decompose`	✅	10s	10s	+0%
`polyveck_add`	✅	9s	8s	+12%
`keccakf1600_permute`	✅	8s	8s	+0%
`keccakf1600_permute_native`	✅	8s	7s	+14%
`mld_check_pct`	✅	8s	10s	-20%
`sign`	✅	8s	9s	-11%
`keccak_absorb`	✅	7s	5s	+40%
`mld_compute_pack_z`	✅	7s	7s	+0%
`poly_decompose_c`	✅	7s	8s	-12%
`polyveck_caddq`	✅	7s	3s	+133%
`polyveck_ntt`	✅	7s	5s	+40%
`polyveck_pointwise_poly_montgomery`	✅	7s	6s	+17%
`polyveck_sub`	✅	7s	7s	+0%
`mld_h`	✅	6s	5s	+20%
`pack_sig_z`	✅	6s	4s	+50%
`pointwise_acc_native_aarch64`	✅	6s	4s	+50%
`poly_invntt_tomont_c`	✅	6s	5s	+20%
`poly_use_hint_native`	✅	6s	4s	+50%
`polyveck_shiftl`	✅	6s	7s	-14%
`rej_eta_native`	✅	6s	7s	-14%
`sign_pk_from_sk`	✅	6s	9s	-33%
`unpack_sk`	✅	6s	7s	-14%
`keccak_init`	✅	5s	3s	+67%
`mld_polyvecl_permute_bitrev_to_custom_native`	✅	5s	3s	+67%
`mld_prepare_domain_separation_prefix`	✅	5s	3s	+67%
`mld_sample_s1_s2_serial`	✅	5s	4s	+25%
`pointwise_acc_native_x86_64`	✅	5s	5s	+0%
`pointwise_native_aarch64`	✅	5s	3s	+67%
`poly_caddq_c`	✅	5s	5s	+0%
`poly_challenge`	✅	5s	4s	+25%
`poly_uniform_gamma1_4x`	✅	5s	2s	+150%
`poly_use_hint_c`	✅	5s	4s	+25%
`polyveck_power2round`	✅	5s	4s	+25%
`polyveck_reduce`	✅	5s	4s	+25%
`polyveck_use_hint`	✅	5s	4s	+25%
`polyvecl_ntt`	✅	5s	6s	-17%
`polyvecl_pointwise_acc_montgomery_native`	✅	5s	3s	+67%
`polyz_unpack_native`	✅	5s	2s	+150%
`sign_keypair_internal`	✅	5s	4s	+25%
`sign_signature_extmu`	✅	5s	4s	+25%
`sign_signature_pre_hash_internal`	✅	5s	4s	+25%
`fqscale`	✅	4s	3s	+33%
`keccak_f1600_x1_native_aarch64_v84a`	✅	4s	2s	+100%
`keccakf1600_extract_bytes (big endian)`	✅	4s	2s	+100%
`mld_sample_s1_s2`	✅	4s	5s	-20%
`mld_value_barrier_i64`	✅	4s	2s	+100%
`pack_pk`	✅	4s	2s	+100%
`pack_sig_h_poly`	✅	4s	2s	+100%
`poly_invntt_tomont_native`	✅	4s	4s	+0%
`poly_ntt_native`	✅	4s	3s	+33%
`poly_uniform_eta`	✅	4s	7s	-43%
`polyt1_pack`	✅	4s	3s	+33%
`polyveck_invntt_tomont`	✅	4s	5s	-20%
`polyveck_pack_w1`	✅	4s	1s	+300%
`polyveck_unpack_eta`	✅	4s	2s	+100%
`polyvecl_pack_eta`	✅	4s	3s	+33%
`polyvecl_pointwise_acc_montgomery`	✅	4s	2s	+100%
`polyz_pack`	✅	4s	3s	+33%
`power2round`	✅	4s	3s	+33%
`shake128_absorb`	✅	4s	4s	+0%
`shake128x4_absorb_once`	✅	4s	2s	+100%
`shake256x4_absorb_once`	✅	4s	3s	+33%
`sign_signature`	✅	4s	2s	+100%
`sign_signature_pre_hash_shake256`	✅	4s	4s	+0%
`sign_verify_pre_hash_internal`	✅	4s	2s	+100%
`sys_check_capability`	✅	4s	2s	+100%
`unpack_hints`	✅	4s	7s	-43%
`unpack_sig`	✅	4s	2s	+100%
`caddq`	✅	3s	2s	+50%
`intt_native_x86_64`	✅	3s	4s	-25%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	3s	2s	+50%
`keccak_finalize`	✅	3s	3s	+0%
`keccak_squeeze`	✅	3s	4s	-25%
`keccak_squeezeblocks_x4`	✅	3s	5s	-40%
`keccakf1600x4_permute`	✅	3s	3s	+0%
`make_hint`	✅	3s	4s	-25%
`mld_ct_cmask_nonzero_u8`	✅	3s	3s	+0%
`mld_ct_get_optblocker_i64`	✅	3s	2s	+50%
`mld_ct_get_optblocker_u32`	✅	3s	3s	+0%
`mld_ct_get_optblocker_u8`	✅	3s	3s	+0%
`mld_value_barrier_u8`	✅	3s	4s	-25%
`ntt_native_aarch64`	✅	3s	4s	-25%
`nttunpack_native_x86_64`	✅	3s	-	new
`pack_sig_c`	✅	3s	4s	-25%
`pack_sk`	✅	3s	2s	+50%
`pointwise_native_x86_64`	✅	3s	5s	-40%
`poly_caddq`	✅	3s	3s	+0%
`poly_chknorm_native`	✅	3s	4s	-25%
`poly_decompose`	✅	3s	3s	+0%
`poly_invntt_tomont`	✅	3s	2s	+50%
`poly_make_hint`	✅	3s	4s	-25%
`poly_ntt`	✅	3s	3s	+0%
`poly_pointwise_montgomery_native`	✅	3s	5s	-40%
`poly_power2round`	✅	3s	4s	-25%
`poly_shiftl`	✅	3s	5s	-40%
`poly_uniform_gamma1`	✅	3s	3s	+0%
`polyt0_pack`	✅	3s	3s	+0%
`polyt1_unpack`	✅	3s	3s	+0%
`polyveck_chknorm`	✅	3s	4s	-25%
`polyveck_pack_t0`	✅	3s	2s	+50%
`polyvecl_chknorm`	✅	3s	5s	-40%
`polyvecl_uniform_gamma1_serial`	✅	3s	4s	-25%
`polyvecl_unpack_eta`	✅	3s	3s	+0%
`rej_eta_c`	✅	3s	5s	-40%
`shake128_squeeze`	✅	3s	3s	+0%
`shake256_init`	✅	3s	7s	-57%
`shake256x4_squeezeblocks`	✅	3s	2s	+50%
`sign_open`	✅	3s	3s	+0%
`sign_verify`	✅	3s	6s	-50%
`sign_verify_pre_hash_shake256`	✅	3s	3s	+0%
`use_hint`	✅	3s	2s	+50%
`decompose`	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64`	✅	2s	1s	+100%
`keccak_f1600_x4_native_aarch64_v84a`	✅	2s	1s	+100%
`keccakf1600_xor_bytes`	✅	2s	3s	-33%
`keccakf1600_xor_bytes (big endian)`	✅	2s	2s	+0%
`mld_ct_abs_i32`	✅	2s	1s	+100%
`mld_ct_cmask_neg_i32`	✅	2s	1s	+100%
`mld_ct_cmask_nonzero_u32`	✅	2s	4s	-50%
`mld_ct_sel_int32`	✅	2s	1s	+100%
`mld_value_barrier_u32`	✅	2s	2s	+0%
`ntt_native_x86_64`	✅	2s	3s	-33%
`poly_caddq_native`	✅	2s	4s	-50%
`poly_caddq_native_aarch64`	✅	2s	2s	+0%
`poly_chknorm`	✅	2s	5s	-60%
`poly_chknorm_native_aarch64`	✅	2s	3s	-33%
`poly_decompose_native`	✅	2s	2s	+0%
`poly_ntt_c`	✅	2s	3s	-33%
`poly_pointwise_montgomery`	✅	2s	3s	-33%
`poly_reduce`	✅	2s	6s	-67%
`poly_sub`	✅	2s	4s	-50%
`poly_uniform`	✅	2s	5s	-60%
`poly_use_hint`	✅	2s	5s	-60%
`polyeta_pack`	✅	2s	1s	+100%
`polyveck_pack_eta`	✅	2s	4s	-50%
`polyveck_unpack_t0`	✅	2s	4s	-50%
`polyvecl_permute_bitrev_to_custom`	✅	2s	6s	-67%
`polyvecl_uniform_gamma1`	✅	2s	1s	+100%
`polyvecl_unpack_z`	✅	2s	2s	+0%
`polyz_unpack`	✅	2s	4s	-50%
`reduce32`	✅	2s	1s	+100%
`rej_eta`	✅	2s	3s	-33%
`shake128_init`	✅	2s	2s	+0%
`shake128x4_squeezeblocks`	✅	2s	1s	+100%
`shake256`	✅	2s	3s	-33%
`shake256_finalize`	✅	2s	2s	+0%
`shake256_release`	✅	2s	2s	+0%
`shake256_squeeze`	✅	2s	1s	+100%
`sign_keypair`	✅	2s	3s	-33%
`sign_verify_extmu`	✅	2s	5s	-60%
`unpack_pk`	✅	2s	1s	+100%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	1s	2s	-50%
`keccakf1600x4_extract_bytes`	✅	1s	2s	-50%
`keccakf1600x4_xor_bytes`	✅	1s	5s	-80%
`mld_keccakf1600_extract_bytes`	✅	1s	2s	-50%
`montgomery_reduce`	✅	1s	1s	+0%
`polyw1_pack`	✅	1s	2s	-50%
`shake128_finalize`	✅	1s	4s	-75%
`shake128_release`	✅	1s	2s	-50%
`shake256_absorb`	✅	1s	2s	-50%

oqs-bot · 2026-02-06T20:14:46Z

CBMC Results (ML-DSA-65)

Full Results (187 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	2743s	2577s	+6.4%
`polyvecl_pointwise_acc_montgomery_c`	✅	715s	646s	+11%
`sign_verify_internal`	✅	283s	269s	+5%
`poly_pointwise_montgomery_c`	✅	184s	162s	+14%
`rej_uniform_native`	✅	152s	142s	+7%
`polyvec_matrix_expand`	✅	90s	85s	+6%
`mld_attempt_signature_generation`	✅	88s	83s	+6%
`mld_ct_memcmp`	✅	83s	78s	+6%
`mld_invntt_layer`	✅	68s	69s	-1%
`mld_ntt_layer`	✅	57s	52s	+10%
`polyvec_matrix_expand_serial`	✅	52s	51s	+2%
`polymat_permute_bitrev_to_custom`	✅	39s	35s	+11%
`mld_compute_t0_t1_tr_from_sk_components`	✅	27s	27s	+0%
`sign_signature_internal`	✅	27s	28s	-4%
`rej_uniform`	✅	24s	23s	+4%
`fqmul`	✅	21s	21s	+0%
`poly_chknorm_c`	✅	20s	21s	-5%
`polyveck_decompose`	✅	18s	19s	-5%
`poly_uniform_eta_4x`	✅	17s	20s	-15%
`rej_uniform_c`	✅	16s	15s	+7%
`poly_uniform_4x`	✅	15s	15s	+0%
`keccakf1600x4_permute_native`	✅	14s	14s	+0%
`polyt0_unpack`	✅	14s	13s	+8%
`polyvec_matrix_pointwise_montgomery`	✅	14s	13s	+8%
`polyveck_power2round`	✅	14s	12s	+17%
`keccak_absorb_once_x4`	✅	12s	11s	+9%
`mld_check_pct`	✅	12s	12s	+0%
`mld_ntt_butterfly_block`	✅	12s	11s	+9%
`poly_add`	✅	12s	10s	+20%
`polyveck_add`	✅	11s	10s	+10%
`keccakf1600_permute`	✅	10s	8s	+25%
`keccakf1600_permute_native`	✅	10s	10s	+0%
`polyveck_caddq`	✅	10s	9s	+11%
`polyvecl_ntt`	✅	10s	9s	+11%
`polyveck_invntt_tomont`	✅	9s	7s	+29%
`polyveck_use_hint`	✅	9s	8s	+12%
`keccak_squeezeblocks_x4`	✅	8s	5s	+60%
`mld_compute_pack_z`	✅	8s	10s	-20%
`pointwise_acc_native_aarch64`	✅	8s	6s	+33%
`polyveck_pointwise_poly_montgomery`	✅	8s	8s	+0%
`polyveck_sub`	✅	8s	9s	-11%
`sign_pk_from_sk`	✅	8s	7s	+14%
`keccak_absorb`	✅	7s	8s	-12%
`poly_caddq_c`	✅	7s	5s	+40%
`poly_uniform`	✅	7s	4s	+75%
`polyveck_ntt`	✅	7s	6s	+17%
`polyveck_reduce`	✅	7s	7s	+0%
`polyveck_shiftl`	✅	7s	7s	+0%
`unpack_sk`	✅	7s	9s	-22%
`mld_polyvecl_permute_bitrev_to_custom_native`	✅	6s	3s	+100%
`pointwise_acc_native_x86_64`	✅	6s	8s	-25%
`polyeta_unpack`	✅	6s	5s	+20%
`polyvecl_pointwise_acc_montgomery`	✅	6s	4s	+50%
`sign`	✅	6s	7s	-14%
`sign_keypair_internal`	✅	6s	6s	+0%
`sign_open`	✅	6s	6s	+0%
`unpack_sig`	✅	6s	4s	+50%
`intt_native_x86_64`	✅	5s	3s	+67%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	5s	1s	+400%
`keccakf1600_xor_bytes (big endian)`	✅	5s	3s	+67%
`pointwise_native_x86_64`	✅	5s	4s	+25%
`poly_chknorm_native_aarch64`	✅	5s	4s	+25%
`poly_decompose_c`	✅	5s	6s	-17%
`poly_invntt_tomont_c`	✅	5s	7s	-29%
`poly_uniform_gamma1_4x`	✅	5s	3s	+67%
`poly_use_hint_native`	✅	5s	3s	+67%
`polyt1_pack`	✅	5s	4s	+25%
`polyt1_unpack`	✅	5s	2s	+150%
`polyveck_chknorm`	✅	5s	5s	+0%
`polyveck_unpack_t0`	✅	5s	5s	+0%
`polyvecl_pointwise_acc_montgomery_native`	✅	5s	4s	+25%
`sign_keypair`	✅	5s	4s	+25%
`unpack_hints`	✅	5s	5s	+0%
`caddq`	✅	4s	2s	+100%
`keccak_f1600_x1_native_aarch64_v84a`	✅	4s	2s	+100%
`keccak_f1600_x4_native_aarch64_v84a`	✅	4s	2s	+100%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	4s	2s	+100%
`keccak_init`	✅	4s	2s	+100%
`keccakf1600x4_extract_bytes`	✅	4s	3s	+33%
`keccakf1600x4_permute`	✅	4s	3s	+33%
`keccakf1600x4_xor_bytes`	✅	4s	3s	+33%
`mld_ct_cmask_nonzero_u32`	✅	4s	4s	+0%
`mld_ct_get_optblocker_u32`	✅	4s	2s	+100%
`mld_sample_s1_s2`	✅	4s	7s	-43%
`mld_sample_s1_s2_serial`	✅	4s	7s	-43%
`mld_value_barrier_u32`	✅	4s	2s	+100%
`montgomery_reduce`	✅	4s	4s	+0%
`ntt_native_aarch64`	✅	4s	4s	+0%
`ntt_native_x86_64`	✅	4s	3s	+33%
`nttunpack_native_x86_64`	✅	4s	-	new
`pack_sig_h_poly`	✅	4s	3s	+33%
`pack_sk`	✅	4s	3s	+33%
`pointwise_native_aarch64`	✅	4s	3s	+33%
`poly_caddq_native`	✅	4s	3s	+33%
`poly_challenge`	✅	4s	6s	-33%
`poly_chknorm`	✅	4s	1s	+300%
`poly_invntt_tomont_native`	✅	4s	4s	+0%
`poly_ntt`	✅	4s	3s	+33%
`poly_ntt_c`	✅	4s	2s	+100%
`poly_ntt_native`	✅	4s	5s	-20%
`poly_pointwise_montgomery`	✅	4s	2s	+100%
`poly_shiftl`	✅	4s	3s	+33%
`poly_sub`	✅	4s	1s	+300%
`poly_use_hint`	✅	4s	2s	+100%
`poly_use_hint_c`	✅	4s	3s	+33%
`polyt0_pack`	✅	4s	3s	+33%
`polyvecl_chknorm`	✅	4s	2s	+100%
`polyvecl_unpack_eta`	✅	4s	5s	-20%
`polyvecl_unpack_z`	✅	4s	3s	+33%
`polyz_unpack_c`	✅	4s	2s	+100%
`rej_eta_native`	✅	4s	5s	-20%
`shake128_absorb`	✅	4s	2s	+100%
`shake256_absorb`	✅	4s	3s	+33%
`sign_signature`	✅	4s	4s	+0%
`sign_verify`	✅	4s	5s	-20%
`sign_verify_pre_hash_shake256`	✅	4s	4s	+0%
`fqscale`	✅	3s	1s	+200%
`keccak_finalize`	✅	3s	4s	-25%
`keccakf1600_xor_bytes`	✅	3s	4s	-25%
`make_hint`	✅	3s	1s	+200%
`mld_ct_abs_i32`	✅	3s	2s	+50%
`mld_ct_cmask_neg_i32`	✅	3s	2s	+50%
`mld_ct_get_optblocker_u8`	✅	3s	2s	+50%
`mld_h`	✅	3s	6s	-50%
`mld_prepare_domain_separation_prefix`	✅	3s	6s	-50%
`mld_value_barrier_u8`	✅	3s	3s	+0%
`pack_pk`	✅	3s	4s	-25%
`pack_sig_z`	✅	3s	3s	+0%
`poly_caddq_native_aarch64`	✅	3s	5s	-40%
`poly_chknorm_native`	✅	3s	4s	-25%
`poly_decompose`	✅	3s	3s	+0%
`poly_invntt_tomont`	✅	3s	2s	+50%
`poly_pointwise_montgomery_native`	✅	3s	4s	-25%
`poly_power2round`	✅	3s	4s	-25%
`poly_reduce`	✅	3s	2s	+50%
`poly_uniform_eta`	✅	3s	3s	+0%
`poly_uniform_gamma1`	✅	3s	4s	-25%
`polyveck_pack_t0`	✅	3s	2s	+50%
`polyveck_pack_w1`	✅	3s	5s	-40%
`polyveck_unpack_eta`	✅	3s	4s	-25%
`polyvecl_permute_bitrev_to_custom`	✅	3s	2s	+50%
`polyvecl_uniform_gamma1`	✅	3s	3s	+0%
`polyvecl_uniform_gamma1_serial`	✅	3s	6s	-50%
`polyw1_pack`	✅	3s	4s	-25%
`polyz_pack`	✅	3s	3s	+0%
`polyz_unpack_native`	✅	3s	3s	+0%
`power2round`	✅	3s	2s	+50%
`rej_eta_c`	✅	3s	6s	-50%
`shake128x4_absorb_once`	✅	3s	5s	-40%
`shake256_init`	✅	3s	2s	+50%
`sign_signature_extmu`	✅	3s	4s	-25%
`sign_signature_pre_hash_shake256`	✅	3s	4s	-25%
`sign_verify_extmu`	✅	3s	2s	+50%
`use_hint`	✅	3s	1s	+200%
`decompose`	✅	2s	2s	+0%
`keccak_f1600_x1_native_aarch64`	✅	2s	1s	+100%
`keccak_squeeze`	✅	2s	3s	-33%
`keccakf1600_extract_bytes (big endian)`	✅	2s	6s	-67%
`mld_ct_cmask_nonzero_u8`	✅	2s	3s	-33%
`mld_ct_get_optblocker_i64`	✅	2s	3s	-33%
`mld_ct_sel_int32`	✅	2s	3s	-33%
`mld_keccakf1600_extract_bytes`	✅	2s	2s	+0%
`pack_sig_c`	✅	2s	3s	-33%
`poly_caddq`	✅	2s	3s	-33%
`poly_decompose_native`	✅	2s	1s	+100%
`poly_make_hint`	✅	2s	2s	+0%
`polyeta_pack`	✅	2s	4s	-50%
`polyvecl_pack_eta`	✅	2s	4s	-50%
`polyz_unpack`	✅	2s	2s	+0%
`rej_eta`	✅	2s	3s	-33%
`shake128_finalize`	✅	2s	2s	+0%
`shake128_init`	✅	2s	2s	+0%
`shake128_release`	✅	2s	1s	+100%
`shake128x4_squeezeblocks`	✅	2s	2s	+0%
`shake256`	✅	2s	4s	-50%
`shake256_release`	✅	2s	4s	-50%
`shake256_squeeze`	✅	2s	2s	+0%
`shake256x4_absorb_once`	✅	2s	3s	-33%
`shake256x4_squeezeblocks`	✅	2s	3s	-33%
`sign_signature_pre_hash_internal`	✅	2s	5s	-60%
`sign_verify_pre_hash_internal`	✅	2s	7s	-71%
`sys_check_capability`	✅	2s	3s	-33%
`unpack_pk`	✅	2s	2s	+0%
`mld_value_barrier_i64`	✅	1s	2s	-50%
`polyveck_pack_eta`	✅	1s	5s	-80%
`reduce32`	✅	1s	5s	-80%
`shake128_squeeze`	✅	1s	2s	-50%
`shake256_finalize`	✅	1s	2s	-50%

hanno-becker

Looks good, @jakemas, thank you! Can you please to the CBMC spec+proof at the same time? You can express in C that the output is a permutation of the input.

jakemas · 2026-02-13T18:44:26Z

Looks good, @jakemas, thank you! Can you please to the CBMC spec+proof at the same time? You can express in C that the output is a permutation of the input.

Thanks! Added CBMC contract.

hanno-becker · 2026-02-13T21:35:55Z

+let nttunpack_order = new_definition
+  `nttunpack_order i =
+   let block = i DIV 64 in
+   let pos = i MOD 64 in
+   let lane = pos DIV 8 in
+   let offset = pos MOD 8 in
+   64 * block + 8 * offset + lane`;;
+
+let nttunpack_unorder = new_definition
+  `nttunpack_unorder i =
+   let block = i DIV 64 in
+   let pos = i MOD 64 in
+   let lane = pos MOD 8 in
+   let offset = pos DIV 8 in
+   64 * block + 8 * lane + offset`;;


This reordering is the same as used for the specification of the [inv]NTT, or not? It determines how the custom NTT domain differs from the normal bitreversed one.

If I understand that correctly, we should reuse the same definition(s) as for the [inv]NTT proofs.

The nttunpack order is the intra-block component of the full AVX2 NTT order, specifically, mldsa_avx2_ntt_order = bitreverse8 * nttunpack_order. They're related but not identical, since the NTT order additionally applies bitreverse8 on top.

I've moved nttunpack_order/nttunpack_unorder to common/mldsa_specs.ml so the definitions are shared. A follow-up could refactor mldsa_avx2_ntt_order to be expressed in terms of nttunpack_order and prove the composition relationship as a lemma. This may require changes to ntt/intt as the pattern matching may no longer work. I'll test it out.

Ok, I’ve refactored mldsa_avx2_ntt_order to be defined as bitreverse8(nttunpack_order i) directly. All downstream clause computations (MLDSA_AVX2_NTT_ORDER_CLAUSES, MLDSA_FORWARD_NTT_CONV, etc.) work with the new definition. The NTT/iNTT proofs re-running in CI to confirm.

I tried redefining mldsa_avx2_ntt_order directly in terms of nttunpack_order, but the NTT proof breaks, it pattern-matches on the expanded arithmetic form during simulation. Keeping the original definition with the decomposition lemma alongside it seemed like the right tradeoff. Proposing a follow up to clean this up, but don't want to block the addition of the proof on it longer. iNTT/NTT proofs are ~3hours to run.

hanno-becker

As I understand, the permutation here should be the same as for the [inv]NTT, so we should have only one set of HOL definition for those in mlkem_specs.ml.

mkannwischer · 2026-04-06T01:49:43Z

@jakemas, could you please rebase this and address @hanno-becker's feedback?

mkannwischer · 2026-04-12T15:46:38Z

@jakemas: Gentle ping. Could you please get this into shape for merging?

jakemas · 2026-04-14T14:39:51Z

@hanno-becker @mkannwischer Okay, shaped up and ready for merge. I've added a mldsa_avx2_ntt_order and nttunpack_order connection proof, and will investigate reformatting the ntt/intt proofs as a follow up.

(* mldsa_avx2_ntt_order decomposes as bitreverse8 after nttunpack_order.     *)
let MLDSA_AVX2_NTT_ORDER_DECOMPOSE = prove
 (`!i. i < 256
       ==> mldsa_avx2_ntt_order i = bitreverse8(nttunpack_order i)`,
  CONV_TAC EXPAND_CASES_CONV THEN CONV_TAC NUM_REDUCE_CONV THEN
  REWRITE_TAC[mldsa_avx2_ntt_order; nttunpack_order; LET_DEF; LET_END_DEF] THEN
  CONV_TAC NUM_REDUCE_CONV THEN
  REWRITE_TAC[bitreverse8] THEN CONV_TAC(DEPTH_CONV WORD_RED_CONV));;

Signed-off-by: Jake Massimo <jakemas@amazon.com>

jakemas added the hol-light label Feb 6, 2026

jakemas force-pushed the mldsa-nttunpack-proof branch from 3811162 to 1f57321 Compare February 6, 2026 19:34

jakemas force-pushed the mldsa-nttunpack-proof branch from 2458351 to 8185ec7 Compare February 6, 2026 20:16

hanno-becker requested changes Feb 7, 2026

View reviewed changes

jakemas force-pushed the mldsa-nttunpack-proof branch 3 times, most recently from cca5edc to 99ba911 Compare February 13, 2026 18:44

jakemas marked this pull request as ready for review February 13, 2026 18:47

jakemas requested a review from a team as a code owner February 13, 2026 18:47

hanno-becker reviewed Feb 13, 2026

View reviewed changes

hanno-becker requested changes Feb 13, 2026

View reviewed changes

jakemas mentioned this pull request Mar 4, 2026

HOL-Light: Prove AVX2 nttunpack #913

Open

mkannwischer self-assigned this Apr 1, 2026

jakemas force-pushed the mldsa-nttunpack-proof branch 5 times, most recently from 8886dcd to 223ba07 Compare April 14, 2026 12:00

jakemas force-pushed the mldsa-nttunpack-proof branch from 223ba07 to 497f6c3 Compare April 14, 2026 18:00

HOL-Light: Add x86 AVX2 nttunpack proof

2405606

Signed-off-by: Jake Massimo <jakemas@amazon.com>

jakemas force-pushed the mldsa-nttunpack-proof branch from 497f6c3 to 2405606 Compare April 15, 2026 08:40

Conversation

jakemas commented Feb 6, 2026

Uh oh!

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

Uh oh!

CBMC Results (ML-DSA-87)

Uh oh!

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

Uh oh!

CBMC Results (ML-DSA-65)

Uh oh!

hanno-becker left a comment

Choose a reason for hiding this comment

Uh oh!

jakemas commented Feb 13, 2026

Uh oh!

hanno-becker Feb 13, 2026

Choose a reason for hiding this comment

Uh oh!

jakemas Apr 14, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jakemas Apr 14, 2026

Choose a reason for hiding this comment

Uh oh!

jakemas Apr 14, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

hanno-becker left a comment

Choose a reason for hiding this comment

Uh oh!

mkannwischer commented Apr 6, 2026

Uh oh!

mkannwischer commented Apr 12, 2026

Uh oh!

jakemas commented Apr 14, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

oqs-bot commented Feb 6, 2026 •

edited

Loading

oqs-bot commented Feb 6, 2026 •

edited

Loading

oqs-bot commented Feb 6, 2026 •

edited

Loading

jakemas Apr 14, 2026 •

edited

Loading

jakemas Apr 14, 2026 •

edited

Loading