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.

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. 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>

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

CBMC Results (ML-DSA-65)

Full Results (175 proofs)

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

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

CBMC Results (ML-DSA-44)

Full Results (175 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	2059s	2185s	-5.8%
`mld_attempt_signature_generation`	✅	308s	330s	-7%
`polyvecl_pointwise_acc_montgomery_c`	✅	202s	217s	-7%
`sign_verify_internal`	✅	188s	192s	-2%
`rej_uniform_native`	✅	136s	151s	-10%
`poly_pointwise_montgomery_c`	✅	130s	148s	-12%
`mld_invntt_layer`	✅	115s	124s	-7%
`mld_ct_memcmp`	✅	78s	88s	-11%
`mld_ntt_layer`	✅	45s	49s	-8%
`keccak_squeezeblocks_x4`	✅	41s	43s	-5%
`sign_signature_internal`	✅	22s	22s	+0%
`fqmul`	✅	19s	20s	-5%
`rej_uniform`	✅	19s	22s	-14%
`polyt0_unpack`	✅	17s	18s	-6%
`rej_uniform_c`	✅	17s	20s	-15%
`poly_uniform_eta_4x`	✅	16s	17s	-6%
`polymat_permute_bitrev_to_custom`	✅	16s	16s	+0%
`polyeta_unpack`	✅	15s	15s	+0%
`polyvec_matrix_expand`	✅	15s	16s	-6%
`keccakf1600x4_permute_native`	✅	14s	13s	+8%
`mld_compute_t0_t1_tr_from_sk_components`	✅	14s	15s	-7%
`keccak_absorb_once_x4`	✅	13s	14s	-7%
`mld_ntt_butterfly_block`	✅	13s	13s	+0%
`poly_uniform_4x`	✅	13s	13s	+0%
`mld_polyvecl_permute_bitrev_to_custom_native`	✅	12s	15s	-20%
`polyveck_add`	✅	12s	9s	+33%
`polyz_unpack_c`	✅	11s	14s	-21%
`poly_chknorm_c`	✅	10s	14s	-29%
`polyveck_reduce`	✅	9s	5s	+80%
`keccakf1600_permute`	✅	8s	7s	+14%
`keccakf1600_permute_native`	✅	7s	9s	-22%
`mld_compute_pack_z`	✅	7s	7s	+0%
`polyvec_matrix_pointwise_montgomery`	✅	7s	6s	+17%
`sign_pk_from_sk`	✅	7s	7s	+0%
`sign_signature_extmu`	✅	7s	4s	+75%
`sign_signature_pre_hash_shake256`	✅	7s	6s	+17%
`keccak_absorb`	✅	6s	6s	+0%
`mld_h`	✅	6s	7s	-14%
`poly_invntt_tomont_c`	✅	6s	8s	-25%
`poly_ntt_c`	✅	6s	1s	+500%
`polyvec_matrix_expand_serial`	✅	6s	5s	+20%
`polyveck_caddq`	✅	6s	5s	+20%
`polyveck_make_hint`	✅	6s	5s	+20%
`polyveck_sub`	✅	6s	5s	+20%
`polyvecl_unpack_z`	✅	6s	3s	+100%
`shake256`	✅	6s	3s	+100%
`shake256x4_squeezeblocks`	✅	6s	2s	+200%
`sign`	✅	6s	9s	-33%
`sign_signature_pre_hash_internal`	✅	6s	3s	+100%
`mld_check_pct`	✅	5s	8s	-38%
`mld_ct_get_optblocker_u32`	✅	5s	1s	+400%
`mld_prepare_domain_separation_prefix`	✅	5s	3s	+67%
`pack_pk`	✅	5s	5s	+0%
`poly_chknorm_native`	✅	5s	2s	+150%
`poly_decompose_c`	✅	5s	3s	+67%
`poly_power2round`	✅	5s	4s	+25%
`poly_sub`	✅	5s	1s	+400%
`poly_uniform_eta`	✅	5s	4s	+25%
`polyt1_unpack`	✅	5s	4s	+25%
`polyveck_decompose`	✅	5s	5s	+0%
`polyveck_invntt_tomont`	✅	5s	5s	+0%
`polyveck_ntt`	✅	5s	7s	-29%
`polyveck_pointwise_poly_montgomery`	✅	5s	7s	-29%
`polyveck_power2round`	✅	5s	5s	+0%
`polyveck_use_hint`	✅	5s	6s	-17%
`polyvecl_chknorm`	✅	5s	5s	+0%
`polyvecl_pointwise_acc_montgomery_native`	✅	5s	3s	+67%
`polyz_unpack_native`	✅	5s	3s	+67%
`power2round`	✅	5s	2s	+150%
`sign_verify_extmu`	✅	5s	3s	+67%
`unpack_pk`	✅	5s	3s	+67%
`unpack_sk`	✅	5s	3s	+67%
`keccakf1600_xor_bytes`	✅	4s	3s	+33%
`mld_ct_abs_i32`	✅	4s	2s	+100%
`mld_sample_s1_s2_serial`	✅	4s	4s	+0%
`pack_sig_c_h`	✅	4s	3s	+33%
`poly_add`	✅	4s	6s	-33%
`poly_challenge`	✅	4s	4s	+0%
`poly_decompose`	✅	4s	2s	+100%
`poly_ntt`	✅	4s	3s	+33%
`poly_pointwise_montgomery`	✅	4s	1s	+300%
`poly_reduce`	✅	4s	2s	+100%
`poly_uniform`	✅	4s	5s	-20%
`poly_uniform_gamma1`	✅	4s	4s	+0%
`poly_use_hint`	✅	4s	5s	-20%
`poly_use_hint_c`	✅	4s	5s	-20%
`polyt0_pack`	✅	4s	3s	+33%
`polyveck_chknorm`	✅	4s	3s	+33%
`polyveck_pack_eta`	✅	4s	5s	-20%
`polyvecl_ntt`	✅	4s	7s	-43%
`polyvecl_uniform_gamma1_serial`	✅	4s	4s	+0%
`polyz_unpack`	✅	4s	4s	+0%
`reduce32`	✅	4s	2s	+100%
`shake256_absorb`	✅	4s	8s	-50%
`sign_keypair`	✅	4s	5s	-20%
`sign_keypair_internal`	✅	4s	5s	-20%
`sign_open`	✅	4s	4s	+0%
`sign_signature`	✅	4s	6s	-33%
`sign_verify`	✅	4s	7s	-43%
`sign_verify_pre_hash_internal`	✅	4s	3s	+33%
`sys_check_capability`	✅	4s	3s	+33%
`unpack_sig`	✅	4s	2s	+100%
`use_hint`	✅	4s	2s	+100%
`intt_native_x86_64`	✅	3s	4s	-25%
`keccak_init`	✅	3s	3s	+0%
`keccak_squeeze`	✅	3s	2s	+50%
`keccakf1600_extract_bytes (big endian)`	✅	3s	2s	+50%
`keccakf1600x4_permute`	✅	3s	2s	+50%
`keccakf1600x4_xor_bytes`	✅	3s	3s	+0%
`mld_ct_cmask_nonzero_u8`	✅	3s	3s	+0%
`mld_sample_s1_s2`	✅	3s	4s	-25%
`mld_value_barrier_u8`	✅	3s	3s	+0%
`ntt_native_x86_64`	✅	3s	4s	-25%
`pack_sk`	✅	3s	3s	+0%
`poly_caddq`	✅	3s	3s	+0%
`poly_caddq_native`	✅	3s	4s	-25%
`poly_caddq_native_aarch64`	✅	3s	4s	-25%
`poly_decompose_native`	✅	3s	4s	-25%
`poly_invntt_tomont_native`	✅	3s	2s	+50%
`poly_make_hint`	✅	3s	3s	+0%
`poly_ntt_native`	✅	3s	3s	+0%
`poly_shiftl`	✅	3s	3s	+0%
`poly_uniform_gamma1_4x`	✅	3s	4s	-25%
`polyeta_pack`	✅	3s	2s	+50%
`polyt1_pack`	✅	3s	3s	+0%
`polyveck_pack_t0`	✅	3s	3s	+0%
`polyveck_pack_w1`	✅	3s	2s	+50%
`polyveck_shiftl`	✅	3s	5s	-40%
`polyveck_unpack_eta`	✅	3s	3s	+0%
`polyvecl_permute_bitrev_to_custom`	✅	3s	4s	-25%
`polyz_pack`	✅	3s	4s	-25%
`rej_eta`	✅	3s	4s	-25%
`shake128_finalize`	✅	3s	2s	+50%
`shake128_release`	✅	3s	1s	+200%
`shake256_finalize`	✅	3s	2s	+50%
`shake256_release`	✅	3s	3s	+0%
`sign_verify_pre_hash_shake256`	✅	3s	3s	+0%
`unpack_hints`	✅	3s	6s	-50%
`caddq`	✅	2s	3s	-33%
`decompose`	✅	2s	3s	-33%
`fqscale`	✅	2s	4s	-50%
`keccakf1600_xor_bytes (big endian)`	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes`	✅	2s	2s	+0%
`make_hint`	✅	2s	3s	-33%
`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_ct_sel_int32`	✅	2s	2s	+0%
`mld_keccakf1600_extract_bytes`	✅	2s	3s	-33%
`montgomery_reduce`	✅	2s	3s	-33%
`pack_sig_z`	✅	2s	4s	-50%
`poly_chknorm`	✅	2s	4s	-50%
`poly_invntt_tomont`	✅	2s	5s	-60%
`poly_pointwise_montgomery_native`	✅	2s	4s	-50%
`polyveck_unpack_t0`	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery`	✅	2s	5s	-60%
`polyvecl_uniform_gamma1`	✅	2s	4s	-50%
`polyvecl_unpack_eta`	✅	2s	2s	+0%
`polyw1_pack`	✅	2s	4s	-50%
`rej_eta_c`	✅	2s	4s	-50%
`rej_eta_native`	✅	2s	4s	-50%
`shake128_absorb`	✅	2s	3s	-33%
`shake128_squeeze`	✅	2s	2s	+0%
`shake128x4_absorb_once`	✅	2s	3s	-33%
`shake256_init`	✅	2s	2s	+0%
`shake256_squeeze`	✅	2s	2s	+0%
`shake256x4_absorb_once`	✅	2s	3s	-33%
`keccak_finalize`	✅	1s	5s	-80%
`mld_ct_get_optblocker_i64`	✅	1s	4s	-75%
`mld_value_barrier_i64`	✅	1s	3s	-67%
`mld_value_barrier_u32`	✅	1s	2s	-50%
`poly_caddq_c`	✅	1s	3s	-67%
`poly_use_hint_native`	✅	1s	4s	-75%
`polyvecl_pack_eta`	✅	1s	3s	-67%
`shake128_init`	✅	1s	2s	-50%
`shake128x4_squeezeblocks`	✅	1s	3s	-67%

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

CBMC Results (ML-DSA-87)

Full Results (175 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	2611s	2484s	+5.1%
`sign_verify_internal`	✅	315s	313s	+1%
`mld_attempt_signature_generation`	✅	230s	218s	+6%
`polyvecl_pointwise_acc_montgomery_c`	✅	198s	183s	+8%
`polyvec_matrix_expand`	✅	167s	165s	+1%
`poly_pointwise_montgomery_c`	✅	157s	133s	+18%
`rej_uniform_native`	✅	151s	144s	+5%
`mld_invntt_layer`	✅	126s	122s	+3%
`polyvec_matrix_expand_serial`	✅	109s	108s	+1%
`mld_ct_memcmp`	✅	88s	81s	+9%
`sign_signature_internal`	✅	75s	73s	+3%
`mld_ntt_layer`	✅	50s	44s	+14%
`keccak_squeezeblocks_x4`	✅	44s	43s	+2%
`polymat_permute_bitrev_to_custom`	✅	26s	27s	-4%
`mld_compute_t0_t1_tr_from_sk_components`	✅	25s	25s	+0%
`fqmul`	✅	20s	18s	+11%
`rej_uniform`	✅	20s	20s	+0%
`rej_uniform_c`	✅	18s	18s	+0%
`poly_chknorm_c`	✅	17s	18s	-6%
`polyeta_unpack`	✅	17s	12s	+42%
`polyveck_power2round`	✅	17s	13s	+31%
`polyt0_unpack`	✅	16s	15s	+7%
`polyveck_add`	✅	16s	15s	+7%
`keccakf1600x4_permute_native`	✅	15s	15s	+0%
`poly_uniform_4x`	✅	15s	16s	-6%
`polyvec_matrix_pointwise_montgomery`	✅	15s	13s	+15%
`poly_uniform_eta_4x`	✅	14s	14s	+0%
`polyveck_use_hint`	✅	13s	10s	+30%
`keccak_absorb_once_x4`	✅	12s	11s	+9%
`mld_ntt_butterfly_block`	✅	12s	13s	-8%
`polyveck_reduce`	✅	12s	9s	+33%
`polyveck_invntt_tomont`	✅	10s	7s	+43%
`sign`	✅	10s	7s	+43%
`mld_polyvecl_permute_bitrev_to_custom_native`	✅	9s	8s	+12%
`mld_sample_s1_s2`	✅	9s	8s	+12%
`poly_decompose_c`	✅	9s	8s	+12%
`polyveck_caddq`	✅	9s	8s	+12%
`polyvecl_ntt`	✅	9s	8s	+12%
`keccakf1600_permute`	✅	8s	5s	+60%
`keccakf1600_permute_native`	✅	8s	9s	-11%
`mld_check_pct`	✅	8s	11s	-27%
`mld_compute_pack_z`	✅	8s	11s	-27%
`mld_sample_s1_s2_serial`	✅	8s	8s	+0%
`poly_invntt_tomont_c`	✅	8s	7s	+14%
`polyveck_chknorm`	✅	8s	11s	-27%
`polyveck_ntt`	✅	8s	6s	+33%
`polyveck_pointwise_poly_montgomery`	✅	8s	8s	+0%
`polyveck_shiftl`	✅	8s	6s	+33%
`polyveck_sub`	✅	8s	7s	+14%
`unpack_sk`	✅	8s	8s	+0%
`polyveck_decompose`	✅	7s	8s	-12%
`polyz_unpack_c`	✅	7s	5s	+40%
`sign_pk_from_sk`	✅	7s	10s	-30%
`keccak_absorb`	✅	6s	6s	+0%
`mld_h`	✅	6s	4s	+50%
`polyt0_pack`	✅	6s	4s	+50%
`polyveck_make_hint`	✅	6s	4s	+50%
`polyvecl_chknorm`	✅	6s	4s	+50%
`power2round`	✅	6s	2s	+200%
`rej_eta_native`	✅	6s	3s	+100%
`sign_keypair_internal`	✅	6s	6s	+0%
`sign_signature`	✅	6s	6s	+0%
`sign_signature_pre_hash_shake256`	✅	6s	6s	+0%
`intt_native_x86_64`	✅	5s	3s	+67%
`keccak_squeeze`	✅	5s	4s	+25%
`mld_ct_cmask_nonzero_u32`	✅	5s	3s	+67%
`pack_pk`	✅	5s	2s	+150%
`pack_sig_z`	✅	5s	2s	+150%
`poly_caddq_c`	✅	5s	3s	+67%
`poly_caddq_native_aarch64`	✅	5s	4s	+25%
`poly_chknorm_native`	✅	5s	3s	+67%
`poly_pointwise_montgomery_native`	✅	5s	3s	+67%
`poly_uniform`	✅	5s	2s	+150%
`poly_uniform_gamma1`	✅	5s	4s	+25%
`polyveck_unpack_t0`	✅	5s	4s	+25%
`polyvecl_pack_eta`	✅	5s	3s	+67%
`shake128_finalize`	✅	5s	2s	+150%
`sign_verify_extmu`	✅	5s	4s	+25%
`sign_verify_pre_hash_internal`	✅	5s	3s	+67%
`unpack_hints`	✅	5s	5s	+0%
`keccak_init`	✅	4s	2s	+100%
`make_hint`	✅	4s	3s	+33%
`mld_prepare_domain_separation_prefix`	✅	4s	5s	-20%
`montgomery_reduce`	✅	4s	4s	+0%
`pack_sig_c_h`	✅	4s	7s	-43%
`poly_add`	✅	4s	3s	+33%
`poly_caddq`	✅	4s	4s	+0%
`poly_decompose`	✅	4s	3s	+33%
`poly_invntt_tomont_native`	✅	4s	2s	+100%
`poly_ntt_native`	✅	4s	3s	+33%
`poly_shiftl`	✅	4s	5s	-20%
`poly_uniform_eta`	✅	4s	5s	-20%
`poly_use_hint`	✅	4s	4s	+0%
`poly_use_hint_native`	✅	4s	3s	+33%
`polyveck_pack_t0`	✅	4s	3s	+33%
`polyveck_pack_w1`	✅	4s	3s	+33%
`polyveck_unpack_eta`	✅	4s	5s	-20%
`polyvecl_unpack_eta`	✅	4s	5s	-20%
`polyvecl_unpack_z`	✅	4s	6s	-33%
`polyz_unpack`	✅	4s	3s	+33%
`polyz_unpack_native`	✅	4s	3s	+33%
`rej_eta_c`	✅	4s	4s	+0%
`sign_keypair`	✅	4s	4s	+0%
`sign_open`	✅	4s	3s	+33%
`sign_signature_extmu`	✅	4s	6s	-33%
`sign_signature_pre_hash_internal`	✅	4s	6s	-33%
`unpack_pk`	✅	4s	5s	-20%
`use_hint`	✅	4s	3s	+33%
`caddq`	✅	3s	4s	-25%
`fqscale`	✅	3s	2s	+50%
`keccakf1600_extract_bytes (big endian)`	✅	3s	3s	+0%
`keccakf1600x4_permute`	✅	3s	2s	+50%
`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_value_barrier_u32`	✅	3s	3s	+0%
`pack_sk`	✅	3s	3s	+0%
`poly_challenge`	✅	3s	4s	-25%
`poly_chknorm`	✅	3s	2s	+50%
`poly_ntt_c`	✅	3s	3s	+0%
`poly_pointwise_montgomery`	✅	3s	2s	+50%
`poly_power2round`	✅	3s	1s	+200%
`poly_reduce`	✅	3s	2s	+50%
`poly_uniform_gamma1_4x`	✅	3s	2s	+50%
`polyeta_pack`	✅	3s	2s	+50%
`polyt1_pack`	✅	3s	4s	-25%
`polyt1_unpack`	✅	3s	3s	+0%
`polyvecl_permute_bitrev_to_custom`	✅	3s	2s	+50%
`polyvecl_pointwise_acc_montgomery`	✅	3s	3s	+0%
`polyvecl_pointwise_acc_montgomery_native`	✅	3s	4s	-25%
`polyvecl_uniform_gamma1`	✅	3s	3s	+0%
`polyw1_pack`	✅	3s	4s	-25%
`polyz_pack`	✅	3s	2s	+50%
`shake128_absorb`	✅	3s	4s	-25%
`shake256_init`	✅	3s	3s	+0%
`shake256_release`	✅	3s	2s	+50%
`shake256x4_absorb_once`	✅	3s	4s	-25%
`sign_verify`	✅	3s	2s	+50%
`sign_verify_pre_hash_shake256`	✅	3s	3s	+0%
`unpack_sig`	✅	3s	5s	-40%
`decompose`	✅	2s	3s	-33%
`keccak_finalize`	✅	2s	3s	-33%
`keccakf1600_xor_bytes`	✅	2s	3s	-33%
`keccakf1600_xor_bytes (big endian)`	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes`	✅	2s	2s	+0%
`keccakf1600x4_xor_bytes`	✅	2s	4s	-50%
`mld_ct_abs_i32`	✅	2s	3s	-33%
`mld_ct_cmask_neg_i32`	✅	2s	3s	-33%
`mld_ct_sel_int32`	✅	2s	1s	+100%
`mld_value_barrier_u8`	✅	2s	2s	+0%
`ntt_native_x86_64`	✅	2s	5s	-60%
`poly_caddq_native`	✅	2s	5s	-60%
`poly_decompose_native`	✅	2s	3s	-33%
`poly_invntt_tomont`	✅	2s	4s	-50%
`poly_make_hint`	✅	2s	2s	+0%
`poly_ntt`	✅	2s	2s	+0%
`poly_sub`	✅	2s	4s	-50%
`poly_use_hint_c`	✅	2s	2s	+0%
`polyveck_pack_eta`	✅	2s	3s	-33%
`polyvecl_uniform_gamma1_serial`	✅	2s	3s	-33%
`reduce32`	✅	2s	2s	+0%
`rej_eta`	✅	2s	2s	+0%
`shake128_init`	✅	2s	2s	+0%
`shake128_release`	✅	2s	3s	-33%
`shake128x4_absorb_once`	✅	2s	3s	-33%
`shake128x4_squeezeblocks`	✅	2s	2s	+0%
`shake256`	✅	2s	3s	-33%
`shake256_finalize`	✅	2s	2s	+0%
`shake256x4_squeezeblocks`	✅	2s	4s	-50%
`sys_check_capability`	✅	2s	2s	+0%
`mld_ct_get_optblocker_u8`	✅	1s	2s	-50%
`mld_keccakf1600_extract_bytes`	✅	1s	2s	-50%
`mld_value_barrier_i64`	✅	1s	2s	-50%
`shake128_squeeze`	✅	1s	3s	-67%
`shake256_absorb`	✅	1s	2s	-50%
`shake256_squeeze`	✅	1s	4s	-75%

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

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

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.

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

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 1 commit intomainfrom
port-hol-light-keccak-f1600

willieyz commented Feb 12, 2026

Uh oh!

oqs-bot commented Feb 12, 2026

Uh oh!

oqs-bot commented Feb 12, 2026

Uh oh!

oqs-bot commented Feb 12, 2026

Uh oh!

mkannwischer left a comment

Uh oh!

mkannwischer Feb 17, 2026

Uh oh!

mkannwischer Feb 17, 2026

Uh oh!

mkannwischer Feb 17, 2026

Uh oh!

mkannwischer Feb 17, 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

CBMC Results (ML-DSA-65)

Uh oh!

oqs-bot commented Feb 12, 2026

CBMC Results (ML-DSA-44)

Uh oh!

oqs-bot commented Feb 12, 2026

CBMC Results (ML-DSA-87)

Uh oh!

mkannwischer left a comment

Choose a reason for hiding this comment

Uh oh!

mkannwischer Feb 17, 2026

Choose a reason for hiding this comment

Uh oh!

mkannwischer Feb 17, 2026

Choose a reason for hiding this comment

Uh oh!

mkannwischer Feb 17, 2026

Choose a reason for hiding this comment

Uh oh!

mkannwischer Feb 17, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants