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)

Full Results (182 proofs)

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

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

CBMC Results (ML-DSA-44)

Full Results (182 proofs)

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

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

CBMC Results (ML-DSA-87)

Full Results (182 proofs)

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

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 5 times, most recently from 1fcede9 to 2740fdf Compare February 27, 2026 06:57

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

willieyz force-pushed the port-hol-light-keccak-f1600 branch from 2740fdf to 598a7de Compare March 23, 2026 16:32

willieyz added 2 commits March 25, 2026 11:00

willieyz force-pushed the port-hol-light-keccak-f1600 branch from 598a7de to d0b8f77 Compare March 25, 2026 03:01

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