Skip to content

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

Merged
mkannwischer merged 2 commits intomainfrom
port-hol-light-keccak-f1600
Apr 6, 2026
Merged

HOL-Light/AArch64: Port proofs from mlkem-native#965
mkannwischer merged 2 commits intomainfrom
port-hol-light-keccak-f1600

Conversation

@willieyz
Copy link
Copy Markdown
Contributor

@willieyz willieyz commented Feb 12, 2026

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:

  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.

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Feb 12, 2026 •
edited
Loading

CBMC Results (ML-DSA-65)

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

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Feb 12, 2026 •
edited
Loading

CBMC Results (ML-DSA-44)

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

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Feb 12, 2026 •
edited
Loading

CBMC Results (ML-DSA-87)

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

@willieyz willieyz marked this pull request as ready for review February 12, 2026 12:01
@willieyz willieyz requested a review from a team as a code owner February 12, 2026 12:01
mkannwischer
mkannwischer requested changes Feb 17, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@mkannwischer mkannwischer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks @willieyz. Happy Near Year!

@willieyz 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 willieyz force-pushed the port-hol-light-keccak-f1600 branch 2 times, most recently from 598a7de to d0b8f77 Compare March 25, 2026 03:01
@mkannwischer mkannwischer self-assigned this Apr 2, 2026
@mkannwischer mkannwischer force-pushed the port-hol-light-keccak-f1600 branch from d0b8f77 to 66a79da Compare April 3, 2026 02:35
mkannwischer
mkannwischer approved these changes Apr 3, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@mkannwischer mkannwischer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks @willieyz! Sorry for the very long wait. I made a few minor changes to comments, but the rest looks very good.

We still need to port the safety proofs and align it with the x86_64 Keccak - but this can be one in a follow-up.

@mkannwischer mkannwischer force-pushed the port-hol-light-keccak-f1600 branch 2 times, most recently from 257397c to 5cbde12 Compare April 6, 2026 01:58
willieyz added 2 commits April 6, 2026 10:33
@willieyz @mkannwischer
HOL-Light/AArch64: Port proofs from mlkem-native
1cbbe23 
This commit ports the HOL-Light correctness proof of the shared AArch64
Keccak routines from mlkem-native.

Signed-off-by: willieyz <willie.zhao@chelpis.com>
@willieyz @mkannwischer
CBMC/AArch64: Port native Keccak F1600 CBMC proofs
24d5679 
This commit adds the CBMC proofs for the native AArch64 Keccak routines from
mlkem-native. This shows that the native contracts fulfills our API contracts.

Signed-off-by: willieyz <willie.zhao@chelpis.com>
@mkannwischer mkannwischer force-pushed the port-hol-light-keccak-f1600 branch from 5cbde12 to 24d5679 Compare April 6, 2026 02:35
@mkannwischer mkannwischer merged commit 094b907 into main Apr 6, 2026
385 checks passed
@mkannwischer mkannwischer deleted the port-hol-light-keccak-f1600 branch April 6, 2026 04:53
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@mkannwischer mkannwischer mkannwischer approved these changes

Assignees

@mkannwischer mkannwischer

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

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

3 participants

@willieyz @oqs-bot @mkannwischer