HOL-Light/AArch64: Port proofs from mlkem-native by willieyz · Pull Request #965 · pq-code-package/mldsa-native

willieyz · 2026-02-12T08:40:07Z

Resolves: HOL-Light/AArch64: Port proofs from mlkem-native #949

After PR #948 merged, mldsa-native and mlkem-native use identical AArch64 assembly for Keccak-F1600. Therefore, the HOL-light proofs on mlkem-native for Keccak-F1600 can also apply to mldsa-native as well.

This PR port the hol-light proof for AArch64 FIPS202 backend from mlkem-native to mldsa-native, also update to CI workflow.

The PR changes according to follwoing step:

Added keccak_f1600_*.S assembly files to proofs/hol_light/aarch64/, copied from mldsa/src/fips202/native/aarch64/src/ and modified with reference to mlkem.
Ported the HOL-Light proofs keccak_f1600_*.ml and keccak_spec.ml from mlkem-native to mldsa-native.
Updated the Makefile to include all newly added keccak_f1600_*.o objects.
Tested locally using tests hol_light.
Updated the CI workflow .github/workflows/hol_light.yml to add the series of Keccak F1600 HOL-Light proofs to the hol_light_proofs field.

oqs-bot · 2026-02-12T08:58:30Z

CBMC Results (ML-DSA-65)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`TOTAL`	⚠️	3396s	2495s	+36.1%
`fqmul`	⚠️	35s	22s	+59%
`mld_check_pct`	⚠️	23s	12s	+92%
`mld_compute_t0_t1_tr_from_sk_components`	⚠️	39s	26s	+50%
`mld_ct_memcmp`	⚠️	149s	87s	+71%
`poly_chknorm_c`	⚠️	31s	19s	+63%
`poly_pointwise_montgomery_c`	⚠️	250s	166s	+51%
`rej_uniform_c`	⚠️	36s	20s	+80%

Full Results (180 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	⚠️	3396s	2495s	+36.1%
`polyvecl_pointwise_acc_montgomery_c`	✅	384s	270s	+42%
`mld_attempt_signature_generation`	✅	258s	219s	+18%
`poly_pointwise_montgomery_c`	⚠️	250s	166s	+51%
`sign_verify_internal`	✅	232s	193s	+20%
`polyvec_matrix_expand`	✅	204s	158s	+29%
`rej_uniform_native`	✅	199s	161s	+24%
`mld_invntt_layer`	✅	169s	132s	+28%
`mld_ct_memcmp`	⚠️	149s	87s	+71%
`polyvec_matrix_expand_serial`	✅	95s	70s	+36%
`sign_signature_internal`	✅	79s	53s	+49%
`mld_ntt_layer`	✅	68s	49s	+39%
`keccak_squeezeblocks_x4`	✅	59s	46s	+28%
`mld_compute_t0_t1_tr_from_sk_components`	⚠️	39s	26s	+50%
`rej_uniform_c`	⚠️	36s	20s	+80%
`fqmul`	⚠️	35s	22s	+59%
`rej_uniform`	✅	32s	22s	+45%
`poly_chknorm_c`	⚠️	31s	19s	+63%
`polymat_permute_bitrev_to_custom`	✅	29s	23s	+26%
`polyveck_decompose`	✅	28s	19s	+47%
`mld_check_pct`	⚠️	23s	12s	+92%
`mld_ntt_butterfly_block`	✅	22s	15s	+47%
`poly_uniform_eta_4x`	✅	22s	17s	+29%
`polyt0_unpack`	✅	22s	16s	+38%
`polyvec_matrix_pointwise_montgomery`	✅	22s	20s	+10%
`polyveck_use_hint`	✅	21s	15s	+40%
`mld_polyvecl_permute_bitrev_to_custom_native`	✅	20s	14s	+43%
`poly_uniform_4x`	✅	20s	16s	+25%
`poly_invntt_tomont_c`	✅	17s	11s	+55%
`keccak_absorb_once_x4`	✅	16s	12s	+33%
`keccakf1600x4_permute_native`	✅	16s	15s	+7%
`polyveck_add`	✅	15s	11s	+36%
`polyveck_ntt`	✅	15s	10s	+50%
`polyveck_shiftl`	✅	14s	8s	+75%
`sign`	✅	14s	10s	+40%
`keccakf1600_permute_native`	✅	13s	10s	+30%
`polyveck_invntt_tomont`	✅	13s	9s	+44%
`sign_pk_from_sk`	✅	13s	9s	+44%
`mld_compute_pack_z`	✅	12s	6s	+100%
`poly_decompose_c`	✅	12s	7s	+71%
`polyveck_power2round`	✅	12s	11s	+9%
`polyveck_reduce`	✅	12s	8s	+50%
`polyveck_caddq`	✅	11s	10s	+10%
`polyveck_sub`	✅	11s	7s	+57%
`polyvecl_ntt`	✅	11s	8s	+38%
`keccakf1600_permute`	✅	10s	10s	+0%
`polyvecl_chknorm`	✅	10s	6s	+67%
`polyveck_pointwise_poly_montgomery`	✅	9s	6s	+50%
`unpack_hints`	✅	9s	7s	+29%
`keccak_absorb`	✅	8s	5s	+60%
`poly_use_hint_c`	✅	8s	4s	+100%
`polyeta_unpack`	✅	8s	5s	+60%
`sign_keypair`	✅	8s	4s	+100%
`sign_signature`	✅	8s	4s	+100%
`sign_signature_pre_hash_internal`	✅	8s	4s	+100%
`sign_verify_pre_hash_internal`	✅	8s	2s	+300%
`sign_verify_pre_hash_shake256`	✅	8s	2s	+300%
`mld_prepare_domain_separation_prefix`	✅	7s	6s	+17%
`poly_add`	✅	7s	5s	+40%
`poly_challenge`	✅	7s	5s	+40%
`poly_decompose_native`	✅	7s	2s	+250%
`poly_power2round`	✅	7s	4s	+75%
`polyvecl_pointwise_acc_montgomery`	✅	7s	1s	+600%
`rej_eta_c`	✅	7s	3s	+133%
`sign_keypair_internal`	✅	7s	3s	+133%
`unpack_sk`	✅	7s	4s	+75%
`mld_h`	✅	6s	5s	+20%
`mld_sample_s1_s2`	✅	6s	3s	+100%
`ntt_native_x86_64`	✅	6s	3s	+100%
`poly_caddq_native`	✅	6s	3s	+100%
`poly_chknorm_native`	✅	6s	5s	+20%
`poly_ntt_c`	✅	6s	2s	+200%
`polyt1_pack`	✅	6s	3s	+100%
`polyveck_make_hint`	✅	6s	6s	+0%
`polyvecl_permute_bitrev_to_custom`	✅	6s	4s	+50%
`polyvecl_pointwise_acc_montgomery_native`	✅	6s	4s	+50%
`polyz_unpack_c`	✅	6s	6s	+0%
`rej_eta_native`	✅	6s	4s	+50%
`decompose`	✅	5s	4s	+25%
`fqscale`	✅	5s	3s	+67%
`intt_native_x86_64`	✅	5s	4s	+25%
`make_hint`	✅	5s	3s	+67%
`mld_sample_s1_s2_serial`	✅	5s	4s	+25%
`pack_sig_z`	✅	5s	4s	+25%
`poly_chknorm`	✅	5s	3s	+67%
`poly_decompose`	✅	5s	6s	-17%
`poly_invntt_tomont_native`	✅	5s	4s	+25%
`poly_make_hint`	✅	5s	4s	+25%
`poly_pointwise_montgomery`	✅	5s	2s	+150%
`poly_pointwise_montgomery_native`	✅	5s	4s	+25%
`poly_reduce`	✅	5s	5s	+0%
`poly_uniform`	✅	5s	5s	+0%
`poly_uniform_eta`	✅	5s	5s	+0%
`poly_uniform_gamma1`	✅	5s	5s	+0%
`polyveck_chknorm`	✅	5s	6s	-17%
`polyveck_pack_eta`	✅	5s	4s	+25%
`polyvecl_uniform_gamma1_serial`	✅	5s	2s	+150%
`polyvecl_unpack_eta`	✅	5s	3s	+67%
`polyz_pack`	✅	5s	3s	+67%
`rej_eta`	✅	5s	3s	+67%
`shake128_finalize`	✅	5s	3s	+67%
`shake128_init`	✅	5s	3s	+67%
`shake256`	✅	5s	1s	+400%
`sign_open`	✅	5s	3s	+67%
`sign_signature_extmu`	✅	5s	3s	+67%
`sign_signature_pre_hash_shake256`	✅	5s	5s	+0%
`sign_verify`	✅	5s	3s	+67%
`sign_verify_extmu`	✅	5s	2s	+150%
`unpack_sig`	✅	5s	2s	+150%
`caddq`	✅	4s	3s	+33%
`keccak_f1600_x1_native_aarch64`	✅	4s	-	new
`keccak_init`	✅	4s	2s	+100%
`keccak_squeeze`	✅	4s	3s	+33%
`keccakf1600x4_permute`	✅	4s	3s	+33%
`keccakf1600x4_xor_bytes`	✅	4s	3s	+33%
`mld_ct_abs_i32`	✅	4s	3s	+33%
`mld_ct_sel_int32`	✅	4s	2s	+100%
`mld_keccakf1600_extract_bytes`	✅	4s	2s	+100%
`mld_value_barrier_u32`	✅	4s	4s	+0%
`montgomery_reduce`	✅	4s	3s	+33%
`pack_sig_c_h`	✅	4s	4s	+0%
`poly_caddq`	✅	4s	2s	+100%
`poly_invntt_tomont`	✅	4s	3s	+33%
`poly_uniform_gamma1_4x`	✅	4s	4s	+0%
`poly_use_hint`	✅	4s	3s	+33%
`polyeta_pack`	✅	4s	3s	+33%
`polyt0_pack`	✅	4s	5s	-20%
`polyveck_pack_w1`	✅	4s	4s	+0%
`polyveck_unpack_eta`	✅	4s	5s	-20%
`polyveck_unpack_t0`	✅	4s	3s	+33%
`polyvecl_uniform_gamma1`	✅	4s	4s	+0%
`polyw1_pack`	✅	4s	3s	+33%
`polyz_unpack_native`	✅	4s	3s	+33%
`reduce32`	✅	4s	3s	+33%
`shake128_absorb`	✅	4s	2s	+100%
`shake128_release`	✅	4s	5s	-20%
`shake128_squeeze`	✅	4s	1s	+300%
`shake256_init`	✅	4s	2s	+100%
`shake256_release`	✅	4s	2s	+100%
`shake256x4_absorb_once`	✅	4s	2s	+100%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	3s	-	new
`keccak_finalize`	✅	3s	3s	+0%
`keccakf1600_xor_bytes`	✅	3s	2s	+50%
`keccakf1600x4_extract_bytes`	✅	3s	3s	+0%
`mld_ct_cmask_neg_i32`	✅	3s	3s	+0%
`mld_ct_cmask_nonzero_u32`	✅	3s	3s	+0%
`mld_ct_get_optblocker_u32`	✅	3s	1s	+200%
`pack_sk`	✅	3s	2s	+50%
`poly_caddq_c`	✅	3s	3s	+0%
`poly_caddq_native_aarch64`	✅	3s	2s	+50%
`poly_ntt_native`	✅	3s	3s	+0%
`poly_shiftl`	✅	3s	1s	+200%
`poly_sub`	✅	3s	4s	-25%
`polyt1_unpack`	✅	3s	5s	-40%
`polyveck_pack_t0`	✅	3s	2s	+50%
`polyvecl_pack_eta`	✅	3s	6s	-50%
`polyvecl_unpack_z`	✅	3s	3s	+0%
`power2round`	✅	3s	4s	-25%
`shake128x4_absorb_once`	✅	3s	4s	-25%
`shake128x4_squeezeblocks`	✅	3s	3s	+0%
`shake256_absorb`	✅	3s	2s	+50%
`shake256_finalize`	✅	3s	1s	+200%
`unpack_pk`	✅	3s	4s	-25%
`use_hint`	✅	3s	4s	-25%
`keccak_f1600_x1_native_aarch64_v84a`	✅	2s	-	new
`keccak_f1600_x4_native_aarch64_v84a`	✅	2s	-	new
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	2s	-	new
`keccakf1600_extract_bytes (big endian)`	✅	2s	3s	-33%
`keccakf1600_xor_bytes (big endian)`	✅	2s	4s	-50%
`mld_ct_cmask_nonzero_u8`	✅	2s	3s	-33%
`mld_ct_get_optblocker_i64`	✅	2s	4s	-50%
`mld_value_barrier_i64`	✅	2s	1s	+100%
`mld_value_barrier_u8`	✅	2s	1s	+100%
`pack_pk`	✅	2s	4s	-50%
`poly_ntt`	✅	2s	4s	-50%
`poly_use_hint_native`	✅	2s	4s	-50%
`polyz_unpack`	✅	2s	2s	+0%
`shake256_squeeze`	✅	2s	4s	-50%
`shake256x4_squeezeblocks`	✅	2s	1s	+100%
`sys_check_capability`	✅	2s	5s	-60%
`mld_ct_get_optblocker_u8`	✅	1s	3s	-67%

oqs-bot · 2026-02-12T08:59:22Z

CBMC Results (ML-DSA-44)

Full Results (180 proofs)

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

oqs-bot · 2026-02-12T09:00:02Z

CBMC Results (ML-DSA-87)

Full Results (180 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	2616s	2686s	-2.6%
`sign_verify_internal`	✅	377s	383s	-2%
`mld_attempt_signature_generation`	✅	244s	250s	-2%
`polyvecl_pointwise_acc_montgomery_c`	✅	198s	204s	-3%
`polyvec_matrix_expand`	✅	159s	161s	-1%
`poly_pointwise_montgomery_c`	✅	151s	160s	-6%
`rej_uniform_native`	✅	150s	152s	-1%
`mld_invntt_layer`	✅	122s	125s	-2%
`polyvec_matrix_expand_serial`	✅	108s	111s	-3%
`mld_ct_memcmp`	✅	88s	92s	-4%
`sign_signature_internal`	✅	47s	49s	-4%
`mld_ntt_layer`	✅	46s	50s	-8%
`keccak_squeezeblocks_x4`	✅	44s	45s	-2%
`mld_compute_t0_t1_tr_from_sk_components`	✅	29s	28s	+4%
`polymat_permute_bitrev_to_custom`	✅	25s	25s	+0%
`rej_uniform`	✅	22s	20s	+10%
`rej_uniform_c`	✅	20s	20s	+0%
`fqmul`	✅	19s	21s	-10%
`poly_chknorm_c`	✅	18s	20s	-10%
`poly_uniform_eta_4x`	✅	18s	16s	+12%
`poly_uniform_4x`	✅	16s	15s	+7%
`polyeta_unpack`	✅	15s	14s	+7%
`polyt0_unpack`	✅	15s	18s	-17%
`polyveck_add`	✅	14s	16s	-12%
`keccakf1600x4_permute_native`	✅	13s	13s	+0%
`mld_ntt_butterfly_block`	✅	12s	12s	+0%
`polyvec_matrix_pointwise_montgomery`	✅	12s	17s	-29%
`polyveck_power2round`	✅	11s	12s	-8%
`keccak_absorb_once_x4`	✅	10s	11s	-9%
`keccakf1600_permute_native`	✅	10s	7s	+43%
`poly_invntt_tomont_c`	✅	10s	9s	+11%
`polyveck_reduce`	✅	10s	10s	+0%
`poly_decompose_c`	✅	9s	9s	+0%
`polyveck_pointwise_poly_montgomery`	✅	9s	7s	+29%
`sign_pk_from_sk`	✅	9s	9s	+0%
`mld_check_pct`	✅	8s	8s	+0%
`mld_polyvecl_permute_bitrev_to_custom_native`	✅	8s	8s	+0%
`polyveck_shiftl`	✅	8s	7s	+14%
`polyveck_use_hint`	✅	8s	12s	-33%
`polyvecl_ntt`	✅	8s	8s	+0%
`rej_eta_native`	✅	8s	4s	+100%
`sign_verify_pre_hash_internal`	✅	8s	2s	+300%
`keccakf1600_permute`	✅	7s	8s	-12%
`mld_sample_s1_s2`	✅	7s	6s	+17%
`poly_ntt`	✅	7s	3s	+133%
`poly_uniform_eta`	✅	7s	5s	+40%
`polyveck_chknorm`	✅	7s	10s	-30%
`polyveck_invntt_tomont`	✅	7s	8s	-12%
`polyveck_ntt`	✅	7s	8s	-12%
`polyz_unpack_c`	✅	7s	6s	+17%
`sign`	✅	7s	8s	-12%
`intt_native_x86_64`	✅	6s	4s	+50%
`keccak_absorb`	✅	6s	6s	+0%
`mld_compute_pack_z`	✅	6s	8s	-25%
`mld_sample_s1_s2_serial`	✅	6s	6s	+0%
`polyveck_caddq`	✅	6s	10s	-40%
`polyveck_decompose`	✅	6s	7s	-14%
`polyvecl_pointwise_acc_montgomery_native`	✅	6s	5s	+20%
`rej_eta_c`	✅	6s	5s	+20%
`shake128_squeeze`	✅	6s	3s	+100%
`shake256_absorb`	✅	6s	3s	+100%
`sign_signature`	✅	6s	5s	+20%
`sign_signature_extmu`	✅	6s	3s	+100%
`unpack_sk`	✅	6s	5s	+20%
`pack_sk`	✅	5s	4s	+25%
`poly_caddq_native`	✅	5s	3s	+67%
`poly_chknorm`	✅	5s	4s	+25%
`poly_pointwise_montgomery_native`	✅	5s	3s	+67%
`polyeta_pack`	✅	5s	6s	-17%
`polyt0_pack`	✅	5s	4s	+25%
`polyt1_pack`	✅	5s	6s	-17%
`polyveck_make_hint`	✅	5s	5s	+0%
`polyveck_pack_t0`	✅	5s	2s	+150%
`polyveck_sub`	✅	5s	6s	-17%
`polyvecl_unpack_eta`	✅	5s	6s	-17%
`sign_keypair_internal`	✅	5s	7s	-29%
`sign_open`	✅	5s	2s	+150%
`sign_signature_pre_hash_internal`	✅	5s	3s	+67%
`sign_verify`	✅	5s	5s	+0%
`sign_verify_extmu`	✅	5s	5s	+0%
`unpack_pk`	✅	5s	3s	+67%
`fqscale`	✅	4s	3s	+33%
`keccak_init`	✅	4s	2s	+100%
`make_hint`	✅	4s	2s	+100%
`mld_h`	✅	4s	6s	-33%
`montgomery_reduce`	✅	4s	3s	+33%
`pack_sig_z`	✅	4s	3s	+33%
`poly_add`	✅	4s	5s	-20%
`poly_challenge`	✅	4s	3s	+33%
`poly_make_hint`	✅	4s	2s	+100%
`poly_ntt_native`	✅	4s	4s	+0%
`poly_pointwise_montgomery`	✅	4s	3s	+33%
`poly_uniform`	✅	4s	4s	+0%
`poly_uniform_gamma1_4x`	✅	4s	4s	+0%
`poly_use_hint`	✅	4s	3s	+33%
`polyveck_pack_eta`	✅	4s	3s	+33%
`polyveck_unpack_eta`	✅	4s	3s	+33%
`polyveck_unpack_t0`	✅	4s	5s	-20%
`polyvecl_chknorm`	✅	4s	3s	+33%
`polyvecl_uniform_gamma1`	✅	4s	5s	-20%
`polyw1_pack`	✅	4s	3s	+33%
`shake128x4_squeezeblocks`	✅	4s	4s	+0%
`sign_signature_pre_hash_shake256`	✅	4s	3s	+33%
`unpack_hints`	✅	4s	8s	-50%
`use_hint`	✅	4s	3s	+33%
`decompose`	✅	3s	3s	+0%
`keccak_f1600_x4_native_aarch64_v84a`	✅	3s	-	new
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	3s	-	new
`keccak_squeeze`	✅	3s	5s	-40%
`mld_ct_abs_i32`	✅	3s	4s	-25%
`mld_ct_cmask_nonzero_u32`	✅	3s	6s	-50%
`mld_value_barrier_u8`	✅	3s	2s	+50%
`ntt_native_x86_64`	✅	3s	3s	+0%
`pack_pk`	✅	3s	3s	+0%
`poly_caddq`	✅	3s	3s	+0%
`poly_caddq_native_aarch64`	✅	3s	4s	-25%
`poly_chknorm_native`	✅	3s	4s	-25%
`poly_invntt_tomont`	✅	3s	4s	-25%
`poly_invntt_tomont_native`	✅	3s	5s	-40%
`poly_ntt_c`	✅	3s	3s	+0%
`poly_reduce`	✅	3s	2s	+50%
`poly_shiftl`	✅	3s	4s	-25%
`poly_uniform_gamma1`	✅	3s	4s	-25%
`poly_use_hint_native`	✅	3s	4s	-25%
`polyt1_unpack`	✅	3s	4s	-25%
`polyveck_pack_w1`	✅	3s	4s	-25%
`polyvecl_pointwise_acc_montgomery`	✅	3s	4s	-25%
`polyvecl_uniform_gamma1_serial`	✅	3s	7s	-57%
`polyvecl_unpack_z`	✅	3s	5s	-40%
`polyz_pack`	✅	3s	4s	-25%
`polyz_unpack`	✅	3s	3s	+0%
`power2round`	✅	3s	3s	+0%
`rej_eta`	✅	3s	4s	-25%
`shake128_finalize`	✅	3s	3s	+0%
`shake256x4_squeezeblocks`	✅	3s	5s	-40%
`sign_keypair`	✅	3s	2s	+50%
`sign_verify_pre_hash_shake256`	✅	3s	4s	-25%
`sys_check_capability`	✅	3s	4s	-25%
`caddq`	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64`	✅	2s	-	new
`keccak_f1600_x1_native_aarch64_v84a`	✅	2s	-	new
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	2s	-	new
`keccak_finalize`	✅	2s	2s	+0%
`keccakf1600_extract_bytes (big endian)`	✅	2s	3s	-33%
`keccakf1600_xor_bytes`	✅	2s	2s	+0%
`keccakf1600x4_permute`	✅	2s	3s	-33%
`mld_ct_cmask_neg_i32`	✅	2s	4s	-50%
`mld_ct_cmask_nonzero_u8`	✅	2s	3s	-33%
`mld_ct_get_optblocker_i64`	✅	2s	1s	+100%
`mld_ct_get_optblocker_u32`	✅	2s	2s	+0%
`mld_ct_get_optblocker_u8`	✅	2s	3s	-33%
`mld_ct_sel_int32`	✅	2s	3s	-33%
`mld_keccakf1600_extract_bytes`	✅	2s	3s	-33%
`mld_prepare_domain_separation_prefix`	✅	2s	4s	-50%
`mld_value_barrier_i64`	✅	2s	4s	-50%
`pack_sig_c_h`	✅	2s	3s	-33%
`poly_caddq_c`	✅	2s	4s	-50%
`poly_decompose`	✅	2s	4s	-50%
`poly_decompose_native`	✅	2s	4s	-50%
`poly_power2round`	✅	2s	4s	-50%
`poly_sub`	✅	2s	3s	-33%
`poly_use_hint_c`	✅	2s	3s	-33%
`polyvecl_pack_eta`	✅	2s	4s	-50%
`polyvecl_permute_bitrev_to_custom`	✅	2s	1s	+100%
`polyz_unpack_native`	✅	2s	5s	-60%
`reduce32`	✅	2s	2s	+0%
`shake128x4_absorb_once`	✅	2s	2s	+0%
`shake256`	✅	2s	3s	-33%
`shake256_finalize`	✅	2s	4s	-50%
`shake256_init`	✅	2s	3s	-33%
`shake256_release`	✅	2s	2s	+0%
`shake256_squeeze`	✅	2s	4s	-50%
`shake256x4_absorb_once`	✅	2s	2s	+0%
`unpack_sig`	✅	2s	2s	+0%
`keccakf1600_xor_bytes (big endian)`	✅	1s	3s	-67%
`keccakf1600x4_extract_bytes`	✅	1s	2s	-50%
`keccakf1600x4_xor_bytes`	✅	1s	1s	+0%
`mld_value_barrier_u32`	✅	1s	1s	+0%
`shake128_absorb`	✅	1s	4s	-75%
`shake128_init`	✅	1s	1s	+0%
`shake128_release`	✅	1s	3s	-67%

mkannwischer

Thanks @willieyz. Happy Near Year!

mkannwischer · 2026-02-17T07:18:16Z

proofs/hol_light/aarch64/Makefile

+      mldsa/keccak_f1600_x1_scalar.o                    \
+      mldsa/keccak_f1600_x1_v84a.o                      \
+      mldsa/keccak_f1600_x2_v84a.o                      \
+      mldsa/keccak_f1600_x4_v8a_scalar.o         \


Here something is off in terms of whitespace.

mkannwischer · 2026-02-17T07:19:01Z

proofs/hol_light/aarch64/mldsa/keccak_f1600_x1_scalar.S

These files should be autogenerated, see https://github.com/pq-code-package/mlkem-native/blob/ab3e6c00ac3d335e890929ef61791315e9192142/scripts/autogen#L2464

Fixed. I have added the corresponding pattern to autogen script, updated the list joblist_aarch64 in def gen_hol_light_asm() and regenerated the related files from autogen.

mkannwischer · 2026-02-17T07:20:01Z

proofs/hol_light/aarch64/proofs/keccak_f1600_x1_v84a.ml

@@ -0,0 +1,297 @@
+(*
+ * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+ * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT-0


Please update the HOL-Light README, see https://github.com/pq-code-package/mlkem-native/blob/main/proofs/hol_light/README.md

Fixed.

I have added description related to these five hol-ight proof in proofs/hol_light/README.md under the chapter "What is covered?".

Regarding the copyright notice for the *.ml files: I noticed that the original keccak_*.ml files in mlkem-native do not include

Copyright (c) The mlkem-native project authors

Therefore, I have left the copyright section unchanged and did not add

Copyright (c) The mldsa-native project authors

Is this ok for you?

mkannwischer · 2026-02-17T07:23:07Z

proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_scalar.ml

+ (`!a rc A1 A2 A3 A4 pc stackpointer.
+      aligned 16 stackpointer /\
+      nonoverlapping (a,800) (stackpointer,216) /\
+      ALLPAIRS nonoverlapping
+               [(a,800); (stackpointer,216)]
+               [(word pc,LENGTH keccak_f1600_x4_v8a_scalar_mc); (rc,192)]
+      ==> ensures arm
+           (\s. aligned_bytes_loaded s (word pc) keccak_f1600_x4_v8a_scalar_mc /\
+                read PC s = word (pc + KECCAK_F1600_X4_V8A_SCALAR_CORE_START) /\
+                read SP s = stackpointer /\
+                C_ARGUMENTS [a; rc] s /\
+                wordlist_from_memory(a,25) s = A1 /\
+                wordlist_from_memory(word_add a (word 200),25) s = A2 /\
+                wordlist_from_memory(word_add a (word 400),25) s = A3 /\
+                wordlist_from_memory(word_add a (word 600),25) s = A4 /\
+                wordlist_from_memory(rc,24) s = round_constants)
+           (\s. read PC s = word(pc + KECCAK_F1600_X4_V8A_SCALAR_CORE_END) /\
+                wordlist_from_memory(a,25) s = keccak 24 A1 /\
+                wordlist_from_memory(word_add a (word 200),25) s =
+                keccak 24 A2 /\
+                wordlist_from_memory(word_add a (word 400),25) s =
+                keccak 24 A3 /\
+                wordlist_from_memory(word_add a (word 600),25) s =
+                keccak 24 A4)


Please also add the corresponding CBMC proofs for those functions - i think the contract are alreaday there.

Hello, Matthias, thank you for your review and help!

I had add the corresponding CBMC proofs, and keep them in new commit: 2740fdf,
Also test with make result for reach five new added cbmc proofs,
If there is any problem, please kindly let me know, and I will fix it as soon as possible, many thanks!

After PR #948 merged, mldsa-native and mlkem-native use identical AArch64 assembly for Keccak-F1600. Therefore, the HOL-light proofs on mlkem-native for Keccak-F1600 can also apply to mldsa-native as well. This commit port the hol-light proof for AArch64 FIPS202 backend from mlkem-native to mldsa-native, also update to CI workflow. The commit changes according to follwoing step: 1. Added keccak_f1600_*.S assembly files to proofs/hol_light/aarch64/, copied from mldsa/src/fips202/native/aarch64/src/ and modified with reference to mlkem. 2. Ported the HOL-Light proofs keccak_f1600_*.ml and keccak_spec.ml from mlkem-native to mldsa-native. 3. Updated the Makefile to include all newly added keccak_f1600_*.o objects, also update the description in `proofs/hol_light/README.md` to cover the new added keccak_f1600 hol-light proofs. 4. Tested locally using `tests hol_light`. 5. Updated the CI workflow .github/workflows/hol_light.yml to add the series of Keccak F1600 HOL-Light proofs to the hol_light_proofs field. Signed-off-by: willieyz <willie.zhao@chelpis.com>

After merging PR #948, `mldsa-native` and `mlkem-native` now share identical AArch64 assembly implementations. In addition to adding the HOL-Light proofs, we also need to provide the corresponding Keccak F1600 CBMC proofs. Since the contracts are already present there: - `x1_scalar.h` - `x1_v84a.h` - `x2_v84a.h` - `x4_v8a_scalar.h` - `x4_v8a_v84a_scalar.h` this commit ports the corresponding CBMC proofs from `mlkem-native`, adds the necessary Makefile entries and harnesses for these 5 contracts. Signed-off-by: willieyz <willie.zhao@chelpis.com>

willieyz marked this pull request as ready for review February 12, 2026 12:01

willieyz requested a review from a team as a code owner February 12, 2026 12:01

mkannwischer requested changes Feb 17, 2026

View reviewed changes

willieyz force-pushed the port-hol-light-keccak-f1600 branch 4 times, most recently from 1aae0c5 to 1fcede9 Compare February 27, 2026 05:41

willieyz added 2 commits February 27, 2026 14:55

willieyz force-pushed the port-hol-light-keccak-f1600 branch from 1fcede9 to 2740fdf Compare February 27, 2026 06:57

willieyz requested a review from mkannwischer February 27, 2026 10:09

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

HOL-Light/AArch64: Port proofs from mlkem-native#965

HOL-Light/AArch64: Port proofs from mlkem-native#965
willieyz wants to merge 2 commits intomainfrom
port-hol-light-keccak-f1600

willieyz commented Feb 12, 2026

Uh oh!

oqs-bot commented Feb 12, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Feb 12, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Feb 12, 2026 •

edited

Loading

Uh oh!

mkannwischer left a comment

Uh oh!

mkannwischer Feb 17, 2026

Uh oh!

willieyz Feb 27, 2026

Uh oh!

mkannwischer Feb 17, 2026

Uh oh!

willieyz Feb 27, 2026

Uh oh!

mkannwischer Feb 17, 2026

Uh oh!

willieyz Feb 27, 2026

Uh oh!

mkannwischer Feb 17, 2026

Uh oh!

willieyz Feb 27, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

willieyz commented Feb 12, 2026

Uh oh!

oqs-bot commented Feb 12, 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 Feb 12, 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 12, 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 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

oqs-bot commented Feb 12, 2026 •

edited

Loading

oqs-bot commented Feb 12, 2026 •

edited

Loading

oqs-bot commented Feb 12, 2026 •

edited

Loading