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`	✅	3472s	3439s	+1.0%
`polyvecl_pointwise_acc_montgomery_c`	✅	1280s	1264s	+1%
`sign_verify_internal`	✅	246s	243s	+1%
`polyvec_matrix_expand`	✅	181s	179s	+1%
`poly_pointwise_montgomery_c`	✅	167s	165s	+1%
`rej_uniform_native`	✅	144s	144s	+0%
`polyvec_matrix_expand_serial`	✅	122s	120s	+2%
`mld_attempt_signature_generation`	✅	91s	92s	-1%
`mld_ct_memcmp`	✅	79s	79s	+0%
`mld_invntt_layer`	✅	68s	68s	+0%
`mld_ntt_layer`	✅	53s	54s	-2%
`sign_keypair_internal`	✅	48s	48s	+0%
`sign_signature_internal`	✅	34s	37s	-8%
`polyveck_invntt_tomont`	✅	29s	32s	-9%
`polymat_permute_bitrev_to_custom`	✅	27s	29s	-7%
`polyveck_decompose`	✅	24s	22s	+9%
`sign_pk_from_sk`	✅	24s	24s	+0%
`rej_uniform`	✅	23s	23s	+0%
`poly_chknorm_c`	✅	20s	19s	+5%
`fqmul`	✅	19s	20s	-5%
`poly_uniform_4x`	✅	17s	14s	+21%
`poly_uniform_eta_4x`	✅	17s	18s	-6%
`keccakf1600x4_permute_native`	✅	14s	14s	+0%
`polyeta_unpack`	✅	14s	18s	-22%
`polyt0_unpack`	✅	14s	16s	-12%
`rej_uniform_c`	✅	13s	17s	-24%
`poly_add`	✅	12s	12s	+0%
`keccak_absorb_once_x4`	✅	11s	10s	+10%
`mld_ntt_butterfly_block`	✅	11s	11s	+0%
`mld_polyvecl_permute_bitrev_to_custom_native`	✅	11s	10s	+10%
`polyveck_add`	✅	11s	11s	+0%
`polyveck_caddq`	✅	11s	8s	+38%
`polyveck_power2round`	✅	11s	9s	+22%
`keccakf1600_permute`	✅	10s	7s	+43%
`keccakf1600_permute_native`	✅	10s	9s	+11%
`mld_check_pct`	✅	10s	9s	+11%
`pointwise_acc_native_aarch64`	✅	10s	8s	+25%
`pointwise_acc_native_x86_64`	✅	10s	8s	+25%
`polyveck_ntt`	✅	10s	7s	+43%
`polyveck_reduce`	✅	10s	8s	+25%
`unpack_sk`	✅	10s	10s	+0%
`poly_uniform_eta`	✅	9s	6s	+50%
`polyvecl_ntt`	✅	9s	10s	-10%
`polyveck_use_hint`	✅	8s	8s	+0%
`polyz_unpack`	✅	8s	4s	+100%
`polyz_unpack_c`	✅	8s	8s	+0%
`rej_eta_c`	✅	8s	8s	+0%
`mld_sample_s1_s2`	✅	7s	8s	-12%
`polyvec_matrix_pointwise_montgomery`	✅	7s	8s	-12%
`polyveck_sub`	✅	7s	8s	-12%
`polyvecl_chknorm`	✅	7s	5s	+40%
`rej_eta_native`	✅	7s	6s	+17%
`sign`	✅	7s	6s	+17%
`sign_verify_pre_hash_shake256`	✅	7s	5s	+40%
`keccak_absorb`	✅	6s	5s	+20%
`mld_compute_pack_z`	✅	6s	7s	-14%
`mld_h`	✅	6s	3s	+100%
`poly_caddq_c`	✅	6s	5s	+20%
`poly_decompose_c`	✅	6s	8s	-25%
`poly_invntt_tomont_c`	✅	6s	7s	-14%
`poly_invntt_tomont_native`	✅	6s	3s	+100%
`poly_power2round`	✅	6s	7s	-14%
`polyveck_pack_eta`	✅	6s	3s	+100%
`polyveck_pointwise_poly_montgomery`	✅	6s	7s	-14%
`polyveck_shiftl`	✅	6s	7s	-14%
`polyveck_unpack_t0`	✅	6s	2s	+200%
`polyvecl_uniform_gamma1`	✅	6s	4s	+50%
`sign_keypair`	✅	6s	2s	+200%
`intt_native_x86_64`	✅	5s	2s	+150%
`mld_sample_s1_s2_serial`	✅	5s	5s	+0%
`pack_pk`	✅	5s	2s	+150%
`pack_sig_c`	✅	5s	2s	+150%
`polyt0_pack`	✅	5s	4s	+25%
`polyveck_unpack_eta`	✅	5s	3s	+67%
`shake128_absorb`	✅	5s	2s	+150%
`shake256x4_absorb_once`	✅	5s	4s	+25%
`sign_signature_pre_hash_shake256`	✅	5s	3s	+67%
`sign_verify`	✅	5s	5s	+0%
`sign_verify_pre_hash_internal`	✅	5s	4s	+25%
`unpack_hints`	✅	5s	6s	-17%
`keccak_squeeze`	✅	4s	4s	+0%
`keccak_squeezeblocks_x4`	✅	4s	4s	+0%
`mld_prepare_domain_separation_prefix`	✅	4s	2s	+100%
`mld_value_barrier_u32`	✅	4s	3s	+33%
`pack_sig_h_poly`	✅	4s	2s	+100%
`pack_sig_z`	✅	4s	2s	+100%
`pack_sk_rho_key_tr_s2_t0`	✅	4s	3s	+33%
`pointwise_native_x86_64`	✅	4s	4s	+0%
`poly_caddq_native`	✅	4s	4s	+0%
`poly_invntt_tomont`	✅	4s	2s	+100%
`poly_ntt_c`	✅	4s	3s	+33%
`poly_ntt_native`	✅	4s	2s	+100%
`poly_sub`	✅	4s	3s	+33%
`poly_uniform_gamma1_4x`	✅	4s	5s	-20%
`poly_use_hint_c`	✅	4s	2s	+100%
`poly_use_hint_native`	✅	4s	3s	+33%
`polyt1_unpack`	✅	4s	3s	+33%
`polyveck_chknorm`	✅	4s	6s	-33%
`polyveck_pack_w1`	✅	4s	3s	+33%
`polyvecl_permute_bitrev_to_custom`	✅	4s	3s	+33%
`shake256_absorb`	✅	4s	2s	+100%
`shake256_finalize`	✅	4s	1s	+300%
`shake256_squeeze`	✅	4s	2s	+100%
`sign_open`	✅	4s	5s	-20%
`sign_signature`	✅	4s	4s	+0%
`sign_signature_extmu`	✅	4s	5s	-20%
`sign_signature_pre_hash_internal`	✅	4s	5s	-20%
`sys_check_capability`	✅	4s	2s	+100%
`caddq`	✅	3s	4s	-25%
`decompose`	✅	3s	4s	-25%
`keccak_f1600_x4_native_aarch64_v84a`	✅	3s	3s	+0%
`keccak_init`	✅	3s	4s	-25%
`keccakf1600_extract_bytes (big endian)`	✅	3s	1s	+200%
`keccakf1600x4_extract_bytes`	✅	3s	2s	+50%
`make_hint`	✅	3s	2s	+50%
`mld_ct_abs_i32`	✅	3s	2s	+50%
`mld_ct_cmask_neg_i32`	✅	3s	1s	+200%
`mld_ct_get_optblocker_i64`	✅	3s	4s	-25%
`mld_ct_get_optblocker_u8`	✅	3s	2s	+50%
`mld_keccakf1600_extract_bytes`	✅	3s	1s	+200%
`mld_value_barrier_u8`	✅	3s	3s	+0%
`ntt_native_x86_64`	✅	3s	4s	-25%
`pack_sk_s1`	✅	3s	4s	-25%
`pointwise_native_aarch64`	✅	3s	5s	-40%
`poly_caddq`	✅	3s	2s	+50%
`poly_chknorm`	✅	3s	2s	+50%
`poly_chknorm_native`	✅	3s	3s	+0%
`poly_chknorm_native_aarch64`	✅	3s	5s	-40%
`poly_decompose`	✅	3s	4s	-25%
`poly_ntt`	✅	3s	3s	+0%
`poly_uniform`	✅	3s	4s	-25%
`poly_uniform_gamma1`	✅	3s	2s	+50%
`polyt1_pack`	✅	3s	4s	-25%
`polyveck_pack_t0`	✅	3s	3s	+0%
`polyvecl_pack_eta`	✅	3s	4s	-25%
`polyvecl_pointwise_acc_montgomery`	✅	3s	3s	+0%
`polyvecl_unpack_z`	✅	3s	3s	+0%
`polyw1_pack`	✅	3s	2s	+50%
`polyz_pack`	✅	3s	3s	+0%
`rej_eta`	✅	3s	3s	+0%
`shake256`	✅	3s	2s	+50%
`shake256_release`	✅	3s	2s	+50%
`sign_verify_extmu`	✅	3s	5s	-40%
`unpack_pk`	✅	3s	4s	-25%
`fqscale`	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	2s	4s	-50%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	2s	1s	+100%
`keccak_finalize`	✅	2s	3s	-33%
`keccakf1600_xor_bytes`	✅	2s	4s	-50%
`keccakf1600_xor_bytes (big endian)`	✅	2s	3s	-33%
`keccakf1600x4_permute`	✅	2s	2s	+0%
`keccakf1600x4_xor_bytes`	✅	2s	1s	+100%
`mld_ct_cmask_nonzero_u32`	✅	2s	4s	-50%
`mld_ct_cmask_nonzero_u8`	✅	2s	1s	+100%
`mld_ct_get_optblocker_u32`	✅	2s	4s	-50%
`mld_value_barrier_i64`	✅	2s	2s	+0%
`montgomery_reduce`	✅	2s	2s	+0%
`ntt_native_aarch64`	✅	2s	3s	-33%
`nttunpack_native_x86_64`	✅	2s	-	new
`poly_caddq_native_aarch64`	✅	2s	5s	-60%
`poly_challenge`	✅	2s	4s	-50%
`poly_decompose_native`	✅	2s	4s	-50%
`poly_make_hint`	✅	2s	3s	-33%
`poly_pointwise_montgomery`	✅	2s	3s	-33%
`poly_pointwise_montgomery_native`	✅	2s	4s	-50%
`poly_reduce`	✅	2s	3s	-33%
`poly_shiftl`	✅	2s	5s	-60%
`poly_use_hint`	✅	2s	3s	-33%
`polyeta_pack`	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery_native`	✅	2s	4s	-50%
`polyvecl_uniform_gamma1_serial`	✅	2s	6s	-67%
`polyvecl_unpack_eta`	✅	2s	4s	-50%
`polyz_unpack_native`	✅	2s	3s	-33%
`power2round`	✅	2s	5s	-60%
`reduce32`	✅	2s	3s	-33%
`shake128_finalize`	✅	2s	3s	-33%
`shake128_init`	✅	2s	2s	+0%
`shake128_release`	✅	2s	4s	-50%
`shake128_squeeze`	✅	2s	4s	-50%
`shake128x4_squeezeblocks`	✅	2s	2s	+0%
`shake256x4_squeezeblocks`	✅	2s	5s	-60%
`unpack_sig`	✅	2s	5s	-60%
`use_hint`	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64`	✅	1s	3s	-67%
`keccak_f1600_x1_native_aarch64_v84a`	✅	1s	5s	-80%
`mld_ct_sel_int32`	✅	1s	3s	-67%
`shake128x4_absorb_once`	✅	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`	✅	1758s	1763s	-0.3%
`polyvecl_pointwise_acc_montgomery_c`	✅	161s	167s	-4%
`sign_verify_internal`	✅	158s	155s	+2%
`poly_pointwise_montgomery_c`	✅	142s	154s	-8%
`rej_uniform_native`	✅	136s	135s	+1%
`mld_ct_memcmp`	✅	74s	74s	+0%
`mld_invntt_layer`	✅	63s	65s	-3%
`mld_attempt_signature_generation`	✅	51s	53s	-4%
`mld_ntt_layer`	✅	50s	51s	-2%
`polymat_permute_bitrev_to_custom`	✅	28s	27s	+4%
`polyvec_matrix_expand`	✅	25s	26s	-4%
`rej_uniform`	✅	21s	21s	+0%
`fqmul`	✅	20s	21s	-5%
`sign_keypair_internal`	✅	20s	22s	-9%
`poly_chknorm_c`	✅	19s	22s	-14%
`sign_pk_from_sk`	✅	18s	19s	-5%
`poly_uniform_eta_4x`	✅	16s	17s	-6%
`sign_signature_internal`	✅	16s	18s	-11%
`keccakf1600x4_permute_native`	✅	15s	15s	+0%
`polyeta_unpack`	✅	15s	16s	-6%
`rej_uniform_c`	✅	15s	15s	+0%
`poly_uniform_4x`	✅	14s	13s	+8%
`polyt0_unpack`	✅	14s	14s	+0%
`keccak_absorb_once_x4`	✅	12s	10s	+20%
`poly_add`	✅	11s	11s	+0%
`polyz_unpack_c`	✅	11s	14s	-21%
`mld_check_pct`	✅	10s	9s	+11%
`polyvec_matrix_pointwise_montgomery`	✅	10s	7s	+43%
`polyveck_power2round`	✅	10s	10s	+0%
`mld_ntt_butterfly_block`	✅	9s	12s	-25%
`poly_decompose_c`	✅	9s	11s	-18%
`polyveck_use_hint`	✅	9s	6s	+50%
`rej_eta_native`	✅	9s	6s	+50%
`polyvec_matrix_expand_serial`	✅	8s	9s	-11%
`keccakf1600_permute`	✅	7s	7s	+0%
`keccakf1600_permute_native`	✅	7s	8s	-12%
`polyveck_shiftl`	✅	7s	6s	+17%
`polyveck_sub`	✅	7s	5s	+40%
`keccak_absorb`	✅	6s	5s	+20%
`keccak_squeezeblocks_x4`	✅	6s	6s	+0%
`mld_compute_pack_z`	✅	6s	7s	-14%
`mld_h`	✅	6s	2s	+200%
`mld_sample_s1_s2_serial`	✅	6s	5s	+20%
`pointwise_acc_native_aarch64`	✅	6s	6s	+0%
`poly_invntt_tomont_c`	✅	6s	5s	+20%
`poly_uniform`	✅	6s	4s	+50%
`poly_uniform_eta`	✅	6s	5s	+20%
`polyveck_add`	✅	6s	8s	-25%
`polyveck_caddq`	✅	6s	5s	+20%
`polyveck_decompose`	✅	6s	4s	+50%
`polyvecl_ntt`	✅	6s	3s	+100%
`sign_open`	✅	6s	5s	+20%
`unpack_hints`	✅	6s	4s	+50%
`unpack_sk`	✅	6s	8s	-25%
`decompose`	✅	5s	2s	+150%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	5s	3s	+67%
`mld_polyvecl_permute_bitrev_to_custom_native`	✅	5s	5s	+0%
`nttunpack_native_x86_64`	✅	5s	-	new
`pointwise_acc_native_x86_64`	✅	5s	5s	+0%
`poly_chknorm_native_aarch64`	✅	5s	4s	+25%
`poly_invntt_tomont_native`	✅	5s	4s	+25%
`poly_ntt_c`	✅	5s	3s	+67%
`poly_pointwise_montgomery`	✅	5s	4s	+25%
`poly_pointwise_montgomery_native`	✅	5s	3s	+67%
`rej_eta_c`	✅	5s	7s	-29%
`sign`	✅	5s	5s	+0%
`sign_signature_pre_hash_internal`	✅	5s	4s	+25%
`sign_signature_pre_hash_shake256`	✅	5s	4s	+25%
`sign_verify_extmu`	✅	5s	6s	-17%
`sign_verify_pre_hash_shake256`	✅	5s	5s	+0%
`caddq`	✅	4s	2s	+100%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	4s	1s	+300%
`keccak_finalize`	✅	4s	2s	+100%
`keccakf1600_extract_bytes (big endian)`	✅	4s	2s	+100%
`keccakf1600_xor_bytes`	✅	4s	2s	+100%
`keccakf1600x4_xor_bytes`	✅	4s	2s	+100%
`mld_ct_cmask_nonzero_u8`	✅	4s	3s	+33%
`mld_ct_get_optblocker_i64`	✅	4s	3s	+33%
`mld_prepare_domain_separation_prefix`	✅	4s	3s	+33%
`mld_sample_s1_s2`	✅	4s	4s	+0%
`ntt_native_aarch64`	✅	4s	2s	+100%
`ntt_native_x86_64`	✅	4s	3s	+33%
`pack_pk`	✅	4s	2s	+100%
`pack_sig_z`	✅	4s	3s	+33%
`pack_sk_s1`	✅	4s	4s	+0%
`pointwise_native_x86_64`	✅	4s	4s	+0%
`poly_caddq`	✅	4s	2s	+100%
`poly_caddq_c`	✅	4s	4s	+0%
`poly_challenge`	✅	4s	6s	-33%
`poly_decompose`	✅	4s	2s	+100%
`poly_invntt_tomont`	✅	4s	4s	+0%
`poly_ntt`	✅	4s	4s	+0%
`poly_power2round`	✅	4s	6s	-33%
`poly_shiftl`	✅	4s	4s	+0%
`poly_sub`	✅	4s	3s	+33%
`poly_uniform_gamma1_4x`	✅	4s	3s	+33%
`poly_use_hint_c`	✅	4s	5s	-20%
`polyt1_pack`	✅	4s	3s	+33%
`polyveck_chknorm`	✅	4s	5s	-20%
`polyveck_invntt_tomont`	✅	4s	5s	-20%
`polyveck_ntt`	✅	4s	4s	+0%
`polyveck_pointwise_poly_montgomery`	✅	4s	5s	-20%
`polyveck_reduce`	✅	4s	5s	-20%
`polyveck_unpack_t0`	✅	4s	2s	+100%
`polyvecl_pack_eta`	✅	4s	4s	+0%
`polyvecl_permute_bitrev_to_custom`	✅	4s	2s	+100%
`polyvecl_pointwise_acc_montgomery_native`	✅	4s	3s	+33%
`polyvecl_uniform_gamma1`	✅	4s	5s	-20%
`polyvecl_uniform_gamma1_serial`	✅	4s	4s	+0%
`polyvecl_unpack_eta`	✅	4s	4s	+0%
`polyvecl_unpack_z`	✅	4s	2s	+100%
`polyz_unpack`	✅	4s	2s	+100%
`shake128x4_squeezeblocks`	✅	4s	3s	+33%
`sign_keypair`	✅	4s	5s	-20%
`sign_signature_extmu`	✅	4s	3s	+33%
`sign_verify`	✅	4s	5s	-20%
`sign_verify_pre_hash_internal`	✅	4s	4s	+0%
`unpack_sig`	✅	4s	3s	+33%
`fqscale`	✅	3s	2s	+50%
`intt_native_x86_64`	✅	3s	3s	+0%
`keccak_squeeze`	✅	3s	4s	-25%
`mld_ct_get_optblocker_u32`	✅	3s	3s	+0%
`mld_ct_sel_int32`	✅	3s	1s	+200%
`pack_sig_h_poly`	✅	3s	4s	-25%
`pointwise_native_aarch64`	✅	3s	2s	+50%
`poly_caddq_native`	✅	3s	4s	-25%
`poly_chknorm_native`	✅	3s	4s	-25%
`poly_decompose_native`	✅	3s	3s	+0%
`poly_ntt_native`	✅	3s	5s	-40%
`poly_uniform_gamma1`	✅	3s	3s	+0%
`poly_use_hint`	✅	3s	5s	-40%
`poly_use_hint_native`	✅	3s	4s	-25%
`polyeta_pack`	✅	3s	5s	-40%
`polyveck_pack_eta`	✅	3s	1s	+200%
`polyveck_pack_t0`	✅	3s	3s	+0%
`polyvecl_chknorm`	✅	3s	4s	-25%
`polyvecl_pointwise_acc_montgomery`	✅	3s	3s	+0%
`polyw1_pack`	✅	3s	3s	+0%
`polyz_pack`	✅	3s	4s	-25%
`polyz_unpack_native`	✅	3s	3s	+0%
`power2round`	✅	3s	3s	+0%
`reduce32`	✅	3s	5s	-40%
`shake128_absorb`	✅	3s	3s	+0%
`shake128_init`	✅	3s	3s	+0%
`shake128x4_absorb_once`	✅	3s	1s	+200%
`shake256_init`	✅	3s	3s	+0%
`shake256_release`	✅	3s	3s	+0%
`shake256x4_absorb_once`	✅	3s	4s	-25%
`shake256x4_squeezeblocks`	✅	3s	2s	+50%
`sign_signature`	✅	3s	4s	-25%
`sys_check_capability`	✅	3s	5s	-40%
`use_hint`	✅	3s	3s	+0%
`keccak_f1600_x1_native_aarch64`	✅	2s	4s	-50%
`keccak_f1600_x4_native_aarch64_v84a`	✅	2s	4s	-50%
`keccak_init`	✅	2s	1s	+100%
`keccakf1600x4_extract_bytes`	✅	2s	2s	+0%
`keccakf1600x4_permute`	✅	2s	4s	-50%
`make_hint`	✅	2s	3s	-33%
`mld_ct_abs_i32`	✅	2s	3s	-33%
`mld_ct_get_optblocker_u8`	✅	2s	1s	+100%
`mld_value_barrier_u32`	✅	2s	1s	+100%
`mld_value_barrier_u8`	✅	2s	3s	-33%
`montgomery_reduce`	✅	2s	3s	-33%
`pack_sig_c`	✅	2s	3s	-33%
`pack_sk_rho_key_tr_s2_t0`	✅	2s	3s	-33%
`poly_caddq_native_aarch64`	✅	2s	2s	+0%
`poly_reduce`	✅	2s	2s	+0%
`polyt1_unpack`	✅	2s	4s	-50%
`polyveck_pack_w1`	✅	2s	2s	+0%
`rej_eta`	✅	2s	4s	-50%
`shake128_finalize`	✅	2s	2s	+0%
`shake128_release`	✅	2s	2s	+0%
`shake128_squeeze`	✅	2s	2s	+0%
`shake256`	✅	2s	2s	+0%
`shake256_absorb`	✅	2s	3s	-33%
`shake256_squeeze`	✅	2s	2s	+0%
`unpack_pk`	✅	2s	1s	+100%
`keccak_f1600_x1_native_aarch64_v84a`	✅	1s	1s	+0%
`keccakf1600_xor_bytes (big endian)`	✅	1s	2s	-50%
`mld_ct_cmask_neg_i32`	✅	1s	3s	-67%
`mld_ct_cmask_nonzero_u32`	✅	1s	6s	-83%
`mld_keccakf1600_extract_bytes`	✅	1s	1s	+0%
`mld_value_barrier_i64`	✅	1s	1s	+0%
`poly_chknorm`	✅	1s	4s	-75%
`poly_make_hint`	✅	1s	2s	-50%
`polyt0_pack`	✅	1s	3s	-67%
`polyveck_unpack_eta`	✅	1s	4s	-75%
`shake256_finalize`	✅	1s	1s	+0%

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

CBMC Results (ML-DSA-65)

Full Results (187 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	2300s	2454s	-6.3%
`polyvecl_pointwise_acc_montgomery_c`	✅	509s	578s	-12%
`sign_verify_internal`	✅	214s	221s	-3%
`rej_uniform_native`	✅	134s	142s	-6%
`poly_pointwise_montgomery_c`	✅	131s	153s	-14%
`polyvec_matrix_expand`	✅	86s	89s	-3%
`mld_ct_memcmp`	✅	68s	76s	-11%
`mld_attempt_signature_generation`	✅	63s	65s	-3%
`mld_invntt_layer`	✅	63s	65s	-3%
`mld_ntt_layer`	✅	51s	53s	-4%
`polyvec_matrix_expand_serial`	✅	47s	49s	-4%
`polymat_permute_bitrev_to_custom`	✅	33s	35s	-6%
`sign_keypair_internal`	✅	28s	29s	-3%
`sign_signature_internal`	✅	22s	25s	-12%
`sign_pk_from_sk`	✅	20s	19s	+5%
`fqmul`	✅	18s	20s	-10%
`rej_uniform`	✅	18s	21s	-14%
`poly_chknorm_c`	✅	17s	21s	-19%
`poly_uniform_4x`	✅	16s	18s	-11%
`poly_uniform_eta_4x`	✅	16s	15s	+7%
`keccakf1600x4_permute_native`	✅	15s	17s	-12%
`polyveck_power2round`	✅	15s	16s	-6%
`rej_uniform_c`	✅	15s	13s	+15%
`polyt0_unpack`	✅	14s	12s	+17%
`polyveck_add`	✅	13s	11s	+18%
`polyveck_decompose`	✅	13s	14s	-7%
`polyvec_matrix_pointwise_montgomery`	✅	12s	12s	+0%
`keccak_absorb_once_x4`	✅	11s	11s	+0%
`mld_ntt_butterfly_block`	✅	11s	11s	+0%
`poly_add`	✅	11s	11s	+0%
`keccakf1600_permute`	✅	10s	7s	+43%
`keccak_absorb`	✅	9s	7s	+29%
`polyveck_caddq`	✅	9s	11s	-18%
`mld_compute_pack_z`	✅	8s	6s	+33%
`polyvecl_ntt`	✅	8s	9s	-11%
`sign`	✅	8s	8s	+0%
`sign_signature`	✅	8s	4s	+100%
`unpack_sk`	✅	8s	8s	+0%
`keccakf1600_permute_native`	✅	7s	8s	-12%
`mld_check_pct`	✅	7s	7s	+0%
`mld_polyvecl_permute_bitrev_to_custom_native`	✅	7s	6s	+17%
`pointwise_acc_native_x86_64`	✅	7s	5s	+40%
`poly_decompose_c`	✅	7s	6s	+17%
`polyeta_unpack`	✅	7s	3s	+133%
`polyveck_ntt`	✅	7s	7s	+0%
`polyveck_sub`	✅	7s	9s	-22%
`sign_open`	✅	7s	3s	+133%
`mld_sample_s1_s2`	✅	6s	5s	+20%
`poly_decompose`	✅	6s	4s	+50%
`poly_power2round`	✅	6s	7s	-14%
`poly_sub`	✅	6s	3s	+100%
`poly_uniform_eta`	✅	6s	5s	+20%
`poly_use_hint_c`	✅	6s	4s	+50%
`polyveck_invntt_tomont`	✅	6s	6s	+0%
`polyveck_pointwise_poly_montgomery`	✅	6s	5s	+20%
`polyveck_reduce`	✅	6s	7s	-14%
`polyveck_use_hint`	✅	6s	6s	+0%
`polyz_unpack_c`	✅	6s	4s	+50%
`sign_keypair`	✅	6s	7s	-14%
`unpack_hints`	✅	6s	6s	+0%
`unpack_sig`	✅	6s	4s	+50%
`use_hint`	✅	6s	3s	+100%
`keccak_squeezeblocks_x4`	✅	5s	4s	+25%
`mld_sample_s1_s2_serial`	✅	5s	8s	-38%
`pointwise_acc_native_aarch64`	✅	5s	7s	-29%
`poly_caddq_c`	✅	5s	5s	+0%
`poly_caddq_native`	✅	5s	5s	+0%
`poly_invntt_tomont_native`	✅	5s	5s	+0%
`poly_pointwise_montgomery`	✅	5s	3s	+67%
`poly_uniform_gamma1_4x`	✅	5s	4s	+25%
`poly_use_hint_native`	✅	5s	4s	+25%
`polyt1_unpack`	✅	5s	5s	+0%
`polyveck_shiftl`	✅	5s	9s	-44%
`polyvecl_chknorm`	✅	5s	3s	+67%
`polyvecl_unpack_z`	✅	5s	6s	-17%
`sign_signature_pre_hash_shake256`	✅	5s	5s	+0%
`caddq`	✅	4s	3s	+33%
`intt_native_x86_64`	✅	4s	2s	+100%
`keccak_finalize`	✅	4s	2s	+100%
`keccakf1600_xor_bytes (big endian)`	✅	4s	2s	+100%
`mld_ct_get_optblocker_i64`	✅	4s	4s	+0%
`mld_prepare_domain_separation_prefix`	✅	4s	4s	+0%
`ntt_native_aarch64`	✅	4s	5s	-20%
`pack_pk`	✅	4s	5s	-20%
`pack_sig_h_poly`	✅	4s	2s	+100%
`poly_caddq_native_aarch64`	✅	4s	2s	+100%
`poly_challenge`	✅	4s	4s	+0%
`poly_invntt_tomont`	✅	4s	3s	+33%
`poly_invntt_tomont_c`	✅	4s	5s	-20%
`poly_pointwise_montgomery_native`	✅	4s	4s	+0%
`polyt0_pack`	✅	4s	4s	+0%
`polyt1_pack`	✅	4s	2s	+100%
`polyveck_chknorm`	✅	4s	5s	-20%
`polyveck_pack_eta`	✅	4s	4s	+0%
`polyveck_unpack_eta`	✅	4s	5s	-20%
`polyveck_unpack_t0`	✅	4s	4s	+0%
`polyvecl_pointwise_acc_montgomery_native`	✅	4s	6s	-33%
`polyz_unpack`	✅	4s	4s	+0%
`rej_eta_c`	✅	4s	3s	+33%
`rej_eta_native`	✅	4s	4s	+0%
`shake128x4_squeezeblocks`	✅	4s	2s	+100%
`shake256_finalize`	✅	4s	3s	+33%
`shake256_squeeze`	✅	4s	3s	+33%
`shake256x4_absorb_once`	✅	4s	3s	+33%
`sign_signature_extmu`	✅	4s	4s	+0%
`sign_verify_pre_hash_internal`	✅	4s	2s	+100%
`sign_verify_pre_hash_shake256`	✅	4s	7s	-43%
`sys_check_capability`	✅	4s	2s	+100%
`decompose`	✅	3s	1s	+200%
`fqscale`	✅	3s	2s	+50%
`keccak_init`	✅	3s	2s	+50%
`keccakf1600_xor_bytes`	✅	3s	4s	-25%
`keccakf1600x4_xor_bytes`	✅	3s	4s	-25%
`make_hint`	✅	3s	2s	+50%
`mld_ct_abs_i32`	✅	3s	5s	-40%
`mld_ct_cmask_nonzero_u8`	✅	3s	2s	+50%
`mld_ct_get_optblocker_u32`	✅	3s	4s	-25%
`mld_ct_sel_int32`	✅	3s	3s	+0%
`mld_h`	✅	3s	9s	-67%
`mld_value_barrier_u8`	✅	3s	1s	+200%
`ntt_native_x86_64`	✅	3s	4s	-25%
`nttunpack_native_x86_64`	✅	3s	-	new
`pack_sig_c`	✅	3s	2s	+50%
`pack_sig_z`	✅	3s	3s	+0%
`pack_sk_s1`	✅	3s	4s	-25%
`pointwise_native_aarch64`	✅	3s	2s	+50%
`poly_caddq`	✅	3s	2s	+50%
`poly_chknorm_native`	✅	3s	5s	-40%
`poly_decompose_native`	✅	3s	4s	-25%
`poly_ntt`	✅	3s	3s	+0%
`poly_ntt_c`	✅	3s	1s	+200%
`poly_ntt_native`	✅	3s	3s	+0%
`poly_shiftl`	✅	3s	3s	+0%
`poly_uniform`	✅	3s	6s	-50%
`poly_uniform_gamma1`	✅	3s	3s	+0%
`poly_use_hint`	✅	3s	2s	+50%
`polyveck_pack_t0`	✅	3s	3s	+0%
`polyveck_pack_w1`	✅	3s	4s	-25%
`polyvecl_pointwise_acc_montgomery`	✅	3s	4s	-25%
`polyvecl_uniform_gamma1`	✅	3s	3s	+0%
`polyz_pack`	✅	3s	2s	+50%
`polyz_unpack_native`	✅	3s	3s	+0%
`reduce32`	✅	3s	2s	+50%
`shake128_absorb`	✅	3s	3s	+0%
`shake128_finalize`	✅	3s	3s	+0%
`shake128x4_absorb_once`	✅	3s	3s	+0%
`shake256`	✅	3s	5s	-40%
`shake256_init`	✅	3s	3s	+0%
`shake256_release`	✅	3s	2s	+50%
`sign_signature_pre_hash_internal`	✅	3s	6s	-50%
`sign_verify`	✅	3s	3s	+0%
`sign_verify_extmu`	✅	3s	3s	+0%
`unpack_pk`	✅	3s	4s	-25%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	2s	2s	+0%
`keccak_squeeze`	✅	2s	2s	+0%
`keccakf1600_extract_bytes (big endian)`	✅	2s	3s	-33%
`keccakf1600x4_permute`	✅	2s	3s	-33%
`mld_ct_cmask_neg_i32`	✅	2s	2s	+0%
`mld_ct_cmask_nonzero_u32`	✅	2s	2s	+0%
`mld_ct_get_optblocker_u8`	✅	2s	4s	-50%
`mld_keccakf1600_extract_bytes`	✅	2s	3s	-33%
`mld_value_barrier_i64`	✅	2s	5s	-60%
`mld_value_barrier_u32`	✅	2s	2s	+0%
`montgomery_reduce`	✅	2s	5s	-60%
`pack_sk_rho_key_tr_s2_t0`	✅	2s	5s	-60%
`pointwise_native_x86_64`	✅	2s	7s	-71%
`poly_chknorm`	✅	2s	4s	-50%
`poly_chknorm_native_aarch64`	✅	2s	4s	-50%
`poly_reduce`	✅	2s	2s	+0%
`polyeta_pack`	✅	2s	4s	-50%
`polyvecl_pack_eta`	✅	2s	3s	-33%
`polyvecl_permute_bitrev_to_custom`	✅	2s	3s	-33%
`polyvecl_unpack_eta`	✅	2s	2s	+0%
`polyw1_pack`	✅	2s	3s	-33%
`power2round`	✅	2s	5s	-60%
`rej_eta`	✅	2s	3s	-33%
`shake128_init`	✅	2s	4s	-50%
`shake128_release`	✅	2s	4s	-50%
`shake128_squeeze`	✅	2s	4s	-50%
`shake256_absorb`	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64`	✅	1s	3s	-67%
`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	2s	-50%
`keccakf1600x4_extract_bytes`	✅	1s	4s	-75%
`poly_make_hint`	✅	1s	2s	-50%
`polyvecl_uniform_gamma1_serial`	✅	1s	2s	-50%
`shake256x4_squeezeblocks`	✅	1s	3s	-67%

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 4 times, most recently from 9b2b218 to 690baeb Compare April 17, 2026 10:22

HOL-Light: Add x86 AVX2 nttunpack proof

2a5bfdc

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

jakemas force-pushed the mldsa-nttunpack-proof branch from 690baeb to 2a5bfdc Compare April 17, 2026 15:02

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