Skip to content

Add HOL Light rej_uniform_eta proofs for AArch64#1040

Open
jakemas wants to merge 1 commit into
mainfrom
add-hol-light-rej-uniform-eta4
Open

Add HOL Light rej_uniform_eta proofs for AArch64#1040
jakemas wants to merge 1 commit into
mainfrom
add-hol-light-rej-uniform-eta4

Conversation

@jakemas
Copy link
Copy Markdown
Contributor

@jakemas jakemas commented Apr 14, 2026 •
edited
Loading

Resolves #924

Some (development) notes:

I've moved the theorems that may be shared with future x86 proof to mldsa_specs.ml. Should it occur that more could be shared during the development of the x86 proof, then we can pull what we need at that point.

The CI gives a nice break down on how long each of the CORRECT and MEMSAFE proofs take. I was able to optimize the full eta2 proof quite a bit from 1h7m to just 31m, which is great considering the CORRECT takes ~24min.

CORRECT proof:
HOL-Light / AArch64 HOL Light proof for rej_uniform_eta4_aarch64_asm.S (pull_request) Successful in 11m
HOL-Light / AArch64 HOL Light proof for rej_uniform_eta2_aarch64_asm.S (pull_request) Successful in 24m

CORRECT + MEMSAFE proof:
HOL-Light / AArch64 HOL Light proof for rej_uniform_eta4_aarch64_asm.S (pull_request) Successful in 21m
HOL-Light / AArch64 HOL Light proof for rej_uniform_eta2_aarch64_asm.S (pull_request) Successful in 1h7m

Optimizations CORRECT + MEMSAFE proof:
HOL-Light / AArch64 HOL Light proof for rej_uniform_eta4_aarch64_asm.S succeeded in 18m 40s
HOL-Light / AArch64 HOL Light proof for rej_uniform_eta2_aarch64_asm.S succeeded in 31m 29s

Built with Claude Opus 4.7 1m. Using the Hol-Light MCP. About 4 weeks of effort.

@jakemas jakemas requested a review from a team as a code owner April 14, 2026 21:41
@jakemas jakemas marked this pull request as draft April 14, 2026 21:41
@jakemas jakemas force-pushed the add-hol-light-rej-uniform-eta4 branch 7 times, most recently from a3673e9 to 0213d92 Compare April 14, 2026 22:00
@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Apr 14, 2026 •
edited
Loading

CBMC Results (ML-DSA-44)

Full Results (201 proofs)
Proof Status Current Previous Change
**TOTAL** ✅ 1631s 1674s -2.6%
polyvecl_pointwise_acc_montgomery_c ✅ 243s 249s -2%
rej_uniform_native ✅ 114s 124s -8%
poly_pointwise_montgomery_c ✅ 92s 97s -5%
mld_invntt_layer ✅ 89s 96s -7%
mld_ct_memcmp ✅ 68s 67s +1%
mld_attempt_signature_generation ✅ 53s 58s -9%
mld_ntt_layer ✅ 44s 43s +2%
fqmul ✅ 29s 29s +0%
polyvec_matrix_expand ✅ 28s 29s -3%
sign_signature_internal ✅ 28s 28s +0%
sign_verify_internal ✅ 26s 27s -4%
keccakf1600x4_permute_native ✅ 24s 21s +14%
mld_check_pct ✅ 18s 17s +6%
rej_uniform_c ✅ 18s 20s -10%
rej_uniform ✅ 16s 16s +0%
compute_pack_t0_t1 ✅ 15s 15s +0%
mld_ntt_butterfly_block ✅ 15s 16s -6%
poly_chknorm_c ✅ 15s 17s -12%
polyt0_unpack ✅ 15s 15s +0%
polyvec_matrix_pointwise_montgomery_yvec ✅ 15s 13s +15%
polyvecl_chknorm ✅ 14s 15s -7%
poly_uniform_4x ✅ 13s 12s +8%
polyz_unpack_c ✅ 13s 11s +18%
poly_uniform_eta_4x ✅ 12s 14s -14%
polyeta_unpack ✅ 12s 12s +0%
polyvec_matrix_expand_serial ✅ 12s 11s +9%
mld_compute_pack_z ✅ 11s 8s +38%
poly_power2round ✅ 10s 10s +0%
keccak_absorb_once_x4 ✅ 9s 8s +12%
poly_add ✅ 9s 11s -18%
poly_invntt_tomont_c ✅ 8s 9s -11%
poly_uniform_gamma1_4x ✅ 8s 5s +60%
sign ✅ 8s 7s +14%
pointwise_acc_native_aarch64 ✅ 7s 5s +40%
poly_decompose_c ✅ 7s 8s -12%
rej_eta_c ✅ 7s 4s +75%
keccak_absorb ✅ 6s 6s +0%
poly_challenge ✅ 6s 4s +50%
polyveck_decompose ✅ 6s 6s +0%
rej_eta_native ✅ 6s 5s +20%
keccak_squeezeblocks_x4 ✅ 5s 4s +25%
mld_keccakf1600_permute_c ✅ 5s 8s -38%
nttunpack_native_x86_64 ✅ 5s 5s +0%
pointwise_acc_native_x86_64 ✅ 5s 6s -17%
pointwise_native_x86_64 ✅ 5s 5s +0%
poly_caddq_native_x86_64 ✅ 5s - new
poly_invntt_tomont ✅ 5s 3s +67%
polyveck_ntt ✅ 5s 3s +67%
polyvecl_ntt ✅ 5s 7s -29%
sig_unpack_hints ✅ 5s 4s +25%
sign_pk_from_sk ✅ 5s 5s +0%
sign_verify ✅ 5s 3s +67%
unpack_sk_t0hat ✅ 5s 4s +25%
yvec_get_poly ✅ 5s 2s +150%
keccak_f1600_x4_native_aarch64_v84a ✅ 4s 2s +100%
keccakf1600_extract_bytes (big endian) ✅ 4s 4s +0%
keccakf1600_xor_bytes ✅ 4s 2s +100%
keccakf1600x4_xor_bytes_native ✅ 4s 3s +33%
mld_h ✅ 4s 2s +100%
mld_prepare_domain_separation_prefix ✅ 4s 4s +0%
mld_value_barrier_u32 ✅ 4s 1s +300%
montgomery_reduce ✅ 4s 3s +33%
pack_sig_c ✅ 4s 2s +100%
pack_sk_s1 ✅ 4s 3s +33%
pointwise_native_aarch64 ✅ 4s 2s +100%
poly_decompose_32_native_aarch64 ✅ 4s 1s +300%
poly_decompose_native ✅ 4s 3s +33%
poly_invntt_tomont_native ✅ 4s 4s +0%
poly_ntt_c ✅ 4s 3s +33%
poly_sub ✅ 4s 2s +100%
poly_uniform ✅ 4s 4s +0%
poly_use_hint_c ✅ 4s 5s -20%
polyeta_pack ✅ 4s 2s +100%
polyt1_unpack ✅ 4s 3s +33%
polyvec_matrix_pointwise_montgomery_row ✅ 4s 3s +33%
polyveck_caddq ✅ 4s 2s +100%
polyveck_pack_w1 ✅ 4s 3s +33%
reduce32 ✅ 4s 4s +0%
rej_eta ✅ 4s 1s +300%
shake128_init ✅ 4s 3s +33%
sign_keypair_internal ✅ 4s 5s -20%
sign_open ✅ 4s 4s +0%
sign_signature ✅ 4s 6s -33%
sign_signature_pre_hash_shake256 ✅ 4s 4s +0%
sign_verify_extmu ✅ 4s 5s -20%
sign_verify_pre_hash_internal ✅ 4s 4s +0%
sign_verify_pre_hash_shake256 ✅ 4s 3s +33%
sk_s1hat_get_poly ✅ 4s 4s +0%
sk_s2hat_get_poly ✅ 4s 3s +33%
decompose ✅ 3s 2s +50%
fqscale ✅ 3s 2s +50%
intt_native_x86_64 ✅ 3s 6s -50%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid ✅ 3s 2s +50%
keccak_f1600_x4_native_avx2 ✅ 3s 2s +50%
keccak_finalize ✅ 3s 2s +50%
keccak_init ✅ 3s 4s -25%
keccak_squeeze ✅ 3s 2s +50%
keccakf1600x4_extract_bytes ✅ 3s 3s +0%
keccakf1600x4_extract_bytes_native ✅ 3s 3s +0%
keccakf1600x4_permute ✅ 3s 2s +50%
keccakf1600x4_xor_bytes ✅ 3s 2s +50%
make_hint ✅ 3s 2s +50%
mld_ct_get_optblocker_i64 ✅ 3s 4s -25%
mld_keccakf1600x4_extract_bytes_c ✅ 3s 4s -25%
mld_polymat_expand_entry ✅ 3s 2s +50%
mld_sample_s1_s2 ✅ 3s 4s -25%
mld_value_barrier_u8 ✅ 3s 3s +0%
ntt_native_aarch64 ✅ 3s 4s -25%
pack_sig_z ✅ 3s 1s +200%
pack_sk_rho_key_tr_s2 ✅ 3s 4s -25%
poly_caddq ✅ 3s 3s +0%
poly_caddq_c ✅ 3s 3s +0%
poly_chknorm ✅ 3s 4s -25%
poly_chknorm_native_aarch64 ✅ 3s 2s +50%
poly_decompose ✅ 3s 5s -40%
poly_decompose_88_native_aarch64 ✅ 3s 4s -25%
poly_ntt ✅ 3s 1s +200%
poly_ntt_native ✅ 3s 7s -57%
poly_pointwise_montgomery ✅ 3s 6s -50%
poly_shiftl ✅ 3s 4s -25%
poly_uniform_eta ✅ 3s 4s -25%
poly_use_hint_native_aarch64 ✅ 3s 3s +0%
polyt0_pack ✅ 3s 6s -50%
polyt1_pack ✅ 3s 3s +0%
polyveck_chknorm ✅ 3s 5s -40%
polyveck_invntt_tomont ✅ 3s 5s -40%
polyveck_reduce ✅ 3s 3s +0%
polyvecl_pointwise_acc_montgomery ✅ 3s 3s +0%
polyvecl_pointwise_acc_montgomery_native ✅ 3s 2s +50%
polyvecl_uniform_gamma1_serial ✅ 3s 3s +0%
polyvecl_unpack_eta ✅ 3s 1s +200%
polyvecl_unpack_z ✅ 3s 3s +0%
polyz_unpack_17_native_aarch64 ✅ 3s 5s -40%
polyz_unpack_19_native_aarch64 ✅ 3s 5s -40%
rej_uniform_native_aarch64 ✅ 3s 3s +0%
shake128x4_squeezeblocks ✅ 3s 1s +200%
shake256_init ✅ 3s 3s +0%
shake256x4_squeezeblocks ✅ 3s 3s +0%
sign_keypair ✅ 3s 6s -50%
sign_signature_extmu ✅ 3s 4s -25%
unpack_pk_t1 ✅ 3s 2s +50%
unpack_sk ✅ 3s 3s +0%
use_hint ✅ 3s 5s -40%
yvec_init ✅ 3s 4s -25%
caddq ✅ 2s 4s -50%
intt_native_aarch64 ✅ 2s 4s -50%
keccak_f1600_x1_native_aarch64 ✅ 2s 1s +100%
keccakf1600_permute ✅ 2s 2s +0%
keccakf1600_permute_native ✅ 2s 1s +100%
keccakf1600_xor_bytes (big endian) ✅ 2s 2s +0%
mld_ct_abs_i32 ✅ 2s 3s -33%
mld_ct_cmask_neg_i32 ✅ 2s 2s +0%
mld_ct_cmask_nonzero_u32 ✅ 2s 2s +0%
mld_ct_cmask_nonzero_u8 ✅ 2s 5s -60%
mld_ct_get_optblocker_u32 ✅ 2s 3s -33%
mld_ct_sel_int32 ✅ 2s 2s +0%
mld_keccakf1600_extract_bytes ✅ 2s 2s +0%
mld_keccakf1600x4_xor_bytes_c ✅ 2s 2s +0%
mld_sample_s1_s2_serial ✅ 2s 3s -33%
mld_value_barrier_i64 ✅ 2s 3s -33%
ntt_native_x86_64 ✅ 2s 4s -50%
pack_sig_h ✅ 2s 1s +100%
poly_caddq_native ✅ 2s 5s -60%
poly_caddq_native_aarch64 ✅ 2s 4s -50%
poly_chknorm_native ✅ 2s 3s -33%
poly_permute_bitrev_to_custom_optional_native ✅ 2s 3s -33%
poly_pointwise_montgomery_native ✅ 2s 2s +0%
poly_reduce ✅ 2s 3s -33%
poly_uniform_gamma1 ✅ 2s 3s -33%
poly_use_hint ✅ 2s 2s +0%
poly_use_hint_native ✅ 2s 6s -67%
polyveck_pack_eta ✅ 2s 3s -33%
polyveck_unpack_eta ✅ 2s 4s -50%
polyvecl_pack_eta ✅ 2s 3s -33%
polyvecl_uniform_gamma1 ✅ 2s 2s +0%
polyw1_pack ✅ 2s 3s -33%
polyz_pack ✅ 2s 3s -33%
polyz_unpack ✅ 2s 3s -33%
polyz_unpack_native ✅ 2s 3s -33%
rej_uniform_eta_native_aarch64 ✅ 2s - new
shake128_absorb ✅ 2s 4s -50%
shake128_finalize ✅ 2s 3s -33%
shake128_release ✅ 2s 3s -33%
shake128x4_absorb_once ✅ 2s 3s -33%
shake256_absorb ✅ 2s 3s -33%
shake256_finalize ✅ 2s 1s +100%
shake256_release ✅ 2s 1s +100%
shake256_squeeze ✅ 2s 4s -50%
shake256x4_absorb_once ✅ 2s 2s +0%
sign_signature_pre_hash_internal ✅ 2s 3s -33%
sk_t0hat_get_poly ✅ 2s 3s -33%
sys_check_capability ✅ 2s 5s -60%
unpack_sk_s1hat ✅ 2s 3s -33%
unpack_sk_s2hat ✅ 2s 2s +0%
keccak_f1600_x1_native_aarch64_v84a ✅ 1s 2s -50%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid ✅ 1s 2s -50%
mld_ct_get_optblocker_u8 ✅ 1s 1s +0%
poly_permute_bitrev_to_custom_optional ✅ 1s 3s -67%
power2round ✅ 1s 1s +0%
shake128_squeeze ✅ 1s 1s +0%
shake256 ✅ 1s 3s -67%

@jakemas jakemas force-pushed the add-hol-light-rej-uniform-eta4 branch from 0213d92 to 4558665 Compare April 14, 2026 22:03
@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Apr 14, 2026 •
edited
Loading

CBMC Results (ML-DSA-65)

Full Results (201 proofs)
Proof Status Current Previous Change
**TOTAL** ✅ 1834s 2016s -9.0%
polyvecl_pointwise_acc_montgomery_c ✅ 257s 319s -19%
polyvec_matrix_expand ✅ 142s 154s -8%
rej_uniform_native ✅ 119s 133s -11%
mld_invntt_layer ✅ 94s 97s -3%
poly_pointwise_montgomery_c ✅ 94s 103s -9%
mld_attempt_signature_generation ✅ 68s 70s -3%
sign_verify_internal ✅ 68s 70s -3%
mld_ct_memcmp ✅ 62s 76s -18%
sign_signature_internal ✅ 47s 47s +0%
mld_ntt_layer ✅ 41s 45s -9%
fqmul ✅ 28s 27s +4%
polyvec_matrix_pointwise_montgomery_yvec ✅ 27s 29s -7%
polyvec_matrix_expand_serial ✅ 23s 25s -8%
keccakf1600x4_permute_native ✅ 22s 23s -4%
rej_uniform ✅ 18s 17s +6%
mld_ntt_butterfly_block ✅ 17s 18s -6%
rej_uniform_c ✅ 17s 22s -23%
poly_chknorm_c ✅ 16s 16s +0%
mld_check_pct ✅ 14s 14s +0%
polyt0_unpack ✅ 14s 16s -12%
compute_pack_t0_t1 ✅ 13s 12s +8%
polyveck_decompose ✅ 13s 15s -13%
poly_uniform_eta_4x ✅ 12s 13s -8%
poly_add ✅ 11s 12s -8%
poly_uniform_4x ✅ 11s 12s -8%
keccak_absorb_once_x4 ✅ 9s 9s +0%
polyveck_chknorm ✅ 9s 11s -18%
keccak_absorb ✅ 8s 7s +14%
mld_keccakf1600_permute_c ✅ 8s 6s +33%
poly_invntt_tomont_c ✅ 8s 10s -20%
poly_power2round ✅ 8s 9s -11%
mld_compute_pack_z ✅ 7s 7s +0%
poly_challenge ✅ 7s 5s +40%
poly_decompose_c ✅ 7s 8s -12%
polyveck_caddq ✅ 7s 7s +0%
polyveck_invntt_tomont ✅ 7s 9s -22%
polyveck_ntt ✅ 7s 7s +0%
sign ✅ 7s 12s -42%
pointwise_acc_native_x86_64 ✅ 6s 6s +0%
polyvecl_ntt ✅ 6s 9s -33%
sign_pk_from_sk ✅ 6s 7s -14%
unpack_sk_t0hat ✅ 6s 5s +20%
decompose ✅ 5s 2s +150%
intt_native_x86_64 ✅ 5s 5s +0%
keccak_squeezeblocks_x4 ✅ 5s 4s +25%
poly_caddq_c ✅ 5s 5s +0%
poly_use_hint_native_aarch64 ✅ 5s 2s +150%
polyz_unpack_19_native_aarch64 ✅ 5s 5s +0%
rej_eta_native ✅ 5s 4s +25%
shake128_squeeze ✅ 5s 3s +67%
sign_open ✅ 5s 5s +0%
sign_signature ✅ 5s 5s +0%
sign_signature_pre_hash_internal ✅ 5s 3s +67%
sign_signature_pre_hash_shake256 ✅ 5s 3s +67%
sign_verify ✅ 5s 6s -17%
sign_verify_pre_hash_internal ✅ 5s 4s +25%
intt_native_aarch64 ✅ 4s 3s +33%
keccakf1600_xor_bytes ✅ 4s 2s +100%
mld_ct_cmask_nonzero_u32 ✅ 4s 1s +300%
mld_ct_cmask_nonzero_u8 ✅ 4s 3s +33%
mld_keccakf1600_extract_bytes ✅ 4s 2s +100%
mld_sample_s1_s2 ✅ 4s 4s +0%
mld_sample_s1_s2_serial ✅ 4s 4s +0%
nttunpack_native_x86_64 ✅ 4s 2s +100%
pack_sk_s1 ✅ 4s 2s +100%
pointwise_acc_native_aarch64 ✅ 4s 6s -33%
pointwise_native_aarch64 ✅ 4s 3s +33%
poly_caddq_native ✅ 4s 2s +100%
poly_caddq_native_aarch64 ✅ 4s 2s +100%
poly_decompose ✅ 4s 2s +100%
poly_reduce ✅ 4s 2s +100%
poly_uniform_gamma1 ✅ 4s 2s +100%
polyt0_pack ✅ 4s 3s +33%
polyveck_pack_w1 ✅ 4s 4s +0%
polyveck_unpack_eta ✅ 4s 2s +100%
polyvecl_chknorm ✅ 4s 5s -20%
polyvecl_pointwise_acc_montgomery_native ✅ 4s 4s +0%
polyz_unpack_c ✅ 4s 2s +100%
reduce32 ✅ 4s 2s +100%
rej_uniform_native_aarch64 ✅ 4s 2s +100%
shake128_absorb ✅ 4s 3s +33%
shake128_finalize ✅ 4s 2s +100%
shake128x4_absorb_once ✅ 4s 3s +33%
shake256x4_absorb_once ✅ 4s 3s +33%
sign_keypair ✅ 4s 5s -20%
sign_verify_extmu ✅ 4s 7s -43%
use_hint ✅ 4s 3s +33%
keccak_f1600_x1_native_aarch64 ✅ 3s 5s -40%
keccak_f1600_x1_native_aarch64_v84a ✅ 3s 3s +0%
keccak_init ✅ 3s 2s +50%
keccak_squeeze ✅ 3s 4s -25%
keccakf1600_extract_bytes (big endian) ✅ 3s 3s +0%
keccakf1600x4_permute ✅ 3s 3s +0%
keccakf1600x4_xor_bytes ✅ 3s 2s +50%
mld_ct_abs_i32 ✅ 3s 1s +200%
mld_ct_get_optblocker_u32 ✅ 3s 2s +50%
mld_ct_get_optblocker_u8 ✅ 3s 1s +200%
mld_keccakf1600x4_extract_bytes_c ✅ 3s 4s -25%
mld_polymat_expand_entry ✅ 3s 2s +50%
mld_prepare_domain_separation_prefix ✅ 3s 5s -40%
mld_value_barrier_u8 ✅ 3s 3s +0%
montgomery_reduce ✅ 3s 2s +50%
ntt_native_aarch64 ✅ 3s 2s +50%
pack_sig_h ✅ 3s 4s -25%
pack_sk_rho_key_tr_s2 ✅ 3s 5s -40%
poly_caddq_native_x86_64 ✅ 3s - new
poly_chknorm_native_aarch64 ✅ 3s 4s -25%
poly_decompose_native ✅ 3s 5s -40%
poly_invntt_tomont ✅ 3s 4s -25%
poly_ntt ✅ 3s 2s +50%
poly_ntt_c ✅ 3s 3s +0%
poly_permute_bitrev_to_custom_optional_native ✅ 3s 4s -25%
poly_pointwise_montgomery ✅ 3s 3s +0%
poly_pointwise_montgomery_native ✅ 3s 4s -25%
poly_uniform ✅ 3s 4s -25%
poly_use_hint ✅ 3s 3s +0%
polyeta_pack ✅ 3s 3s +0%
polyeta_unpack ✅ 3s 4s -25%
polyvec_matrix_pointwise_montgomery_row ✅ 3s 3s +0%
polyveck_pack_eta ✅ 3s 3s +0%
polyvecl_pack_eta ✅ 3s 4s -25%
polyvecl_pointwise_acc_montgomery ✅ 3s 4s -25%
polyvecl_uniform_gamma1 ✅ 3s 5s -40%
polyvecl_unpack_eta ✅ 3s 3s +0%
polyz_unpack_17_native_aarch64 ✅ 3s 3s +0%
polyz_unpack_native ✅ 3s 2s +50%
rej_eta ✅ 3s 3s +0%
rej_eta_c ✅ 3s 3s +0%
rej_uniform_eta_native_aarch64 ✅ 3s - new
shake128_release ✅ 3s 1s +200%
shake256_init ✅ 3s 2s +50%
sign_keypair_internal ✅ 3s 2s +50%
sign_signature_extmu ✅ 3s 3s +0%
sign_verify_pre_hash_shake256 ✅ 3s 2s +50%
sk_s1hat_get_poly ✅ 3s 4s -25%
sk_s2hat_get_poly ✅ 3s 4s -25%
sk_t0hat_get_poly ✅ 3s 2s +50%
unpack_pk_t1 ✅ 3s 4s -25%
unpack_sk ✅ 3s 3s +0%
caddq ✅ 2s 2s +0%
fqscale ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v84a ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid ✅ 2s 1s +100%
keccak_f1600_x4_native_avx2 ✅ 2s 2s +0%
keccak_finalize ✅ 2s 3s -33%
keccakf1600_xor_bytes (big endian) ✅ 2s 5s -60%
keccakf1600x4_extract_bytes ✅ 2s 3s -33%
keccakf1600x4_extract_bytes_native ✅ 2s 3s -33%
make_hint ✅ 2s 4s -50%
mld_ct_get_optblocker_i64 ✅ 2s 2s +0%
mld_ct_sel_int32 ✅ 2s 3s -33%
mld_h ✅ 2s 4s -50%
mld_keccakf1600x4_xor_bytes_c ✅ 2s 2s +0%
mld_value_barrier_u32 ✅ 2s 2s +0%
ntt_native_x86_64 ✅ 2s 4s -50%
pack_sig_c ✅ 2s 1s +100%
pack_sig_z ✅ 2s 2s +0%
pointwise_native_x86_64 ✅ 2s 6s -67%
poly_caddq ✅ 2s 3s -33%
poly_chknorm_native ✅ 2s 5s -60%
poly_decompose_32_native_aarch64 ✅ 2s 2s +0%
poly_decompose_88_native_aarch64 ✅ 2s 4s -50%
poly_invntt_tomont_native ✅ 2s 3s -33%
poly_ntt_native ✅ 2s 4s -50%
poly_permute_bitrev_to_custom_optional ✅ 2s 5s -60%
poly_shiftl ✅ 2s 3s -33%
poly_sub ✅ 2s 3s -33%
poly_uniform_gamma1_4x ✅ 2s 5s -60%
poly_use_hint_c ✅ 2s 3s -33%
poly_use_hint_native ✅ 2s 3s -33%
polyt1_pack ✅ 2s 4s -50%
polyveck_reduce ✅ 2s 4s -50%
polyvecl_uniform_gamma1_serial ✅ 2s 5s -60%
polyvecl_unpack_z ✅ 2s 3s -33%
polyw1_pack ✅ 2s 6s -67%
polyz_unpack ✅ 2s 5s -60%
power2round ✅ 2s 3s -33%
shake128_init ✅ 2s 4s -50%
shake128x4_squeezeblocks ✅ 2s 1s +100%
shake256_absorb ✅ 2s 2s +0%
shake256_finalize ✅ 2s 1s +100%
shake256_release ✅ 2s 2s +0%
shake256_squeeze ✅ 2s 1s +100%
shake256x4_squeezeblocks ✅ 2s 3s -33%
sig_unpack_hints ✅ 2s 3s -33%
sys_check_capability ✅ 2s 4s -50%
unpack_sk_s1hat ✅ 2s 3s -33%
unpack_sk_s2hat ✅ 2s 3s -33%
yvec_get_poly ✅ 2s 3s -33%
yvec_init ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid ✅ 1s 1s +0%
keccakf1600_permute ✅ 1s 1s +0%
keccakf1600_permute_native ✅ 1s 3s -67%
keccakf1600x4_xor_bytes_native ✅ 1s 5s -80%
mld_ct_cmask_neg_i32 ✅ 1s 3s -67%
mld_value_barrier_i64 ✅ 1s 2s -50%
poly_chknorm ✅ 1s 4s -75%
poly_uniform_eta ✅ 1s 5s -80%
polyt1_unpack ✅ 1s 4s -75%
polyz_pack ✅ 1s 2s -50%
shake256 ✅ 1s 4s -75%

@jakemas jakemas force-pushed the add-hol-light-rej-uniform-eta4 branch from 4558665 to 73d8d61 Compare April 14, 2026 22:14
@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Apr 14, 2026 •
edited
Loading

CBMC Results (ML-DSA-87)

Full Results (201 proofs)
Proof Status Current Previous Change
**TOTAL** ✅ 2096s 2060s +1.7%
polyvecl_pointwise_acc_montgomery_c ✅ 290s 261s +11%
polyvec_matrix_expand ✅ 180s 177s +2%
rej_uniform_native ✅ 129s 128s +1%
poly_pointwise_montgomery_c ✅ 107s 96s +11%
mld_attempt_signature_generation ✅ 106s 102s +4%
mld_invntt_layer ✅ 99s 93s +6%
sign_verify_internal ✅ 91s 87s +5%
mld_ct_memcmp ✅ 69s 70s -1%
sign_signature_internal ✅ 52s 52s +0%
mld_ntt_layer ✅ 44s 45s -2%
polyvec_matrix_expand_serial ✅ 39s 40s -3%
fqmul ✅ 31s 26s +19%
compute_pack_t0_t1 ✅ 27s 25s +8%
keccakf1600x4_permute_native ✅ 23s 23s +0%
polyvec_matrix_pointwise_montgomery_yvec ✅ 21s 21s +0%
mld_ntt_butterfly_block ✅ 19s 15s +27%
rej_uniform_c ✅ 18s 17s +6%
poly_chknorm_c ✅ 17s 16s +6%
rej_uniform ✅ 16s 17s -6%
poly_uniform_4x ✅ 15s 10s +50%
polyt0_unpack ✅ 15s 16s -6%
polyeta_unpack ✅ 14s 14s +0%
mld_check_pct ✅ 13s 16s -19%
poly_uniform_eta_4x ✅ 13s 15s -13%
poly_add ✅ 12s 12s +0%
polyveck_decompose ✅ 12s 11s +9%
polyveck_invntt_tomont ✅ 11s 10s +10%
keccak_absorb_once_x4 ✅ 10s 10s +0%
mld_compute_pack_z ✅ 9s 9s +0%
polyveck_ntt ✅ 9s 9s +0%
poly_challenge ✅ 8s 3s +167%
poly_power2round ✅ 8s 10s -20%
polyz_unpack_c ✅ 8s 7s +14%
sign ✅ 8s 8s +0%
pointwise_acc_native_aarch64 ✅ 7s 5s +40%
pointwise_acc_native_x86_64 ✅ 7s 7s +0%
poly_invntt_tomont_c ✅ 7s 7s +0%
polyveck_caddq ✅ 7s 9s -22%
polyveck_chknorm ✅ 7s 8s -12%
sign_keypair_internal ✅ 7s 4s +75%
unpack_sk_t0hat ✅ 7s 5s +40%
mld_keccakf1600_permute_c ✅ 6s 8s -25%
mld_prepare_domain_separation_prefix ✅ 6s 5s +20%
mld_sample_s1_s2_serial ✅ 6s 4s +50%
poly_uniform_eta ✅ 6s 2s +200%
polyvecl_ntt ✅ 6s 7s -14%
polyz_unpack_19_native_aarch64 ✅ 6s 4s +50%
sign_verify ✅ 6s 6s +0%
keccak_absorb ✅ 5s 5s +0%
keccak_squeezeblocks_x4 ✅ 5s 4s +25%
mld_ct_cmask_neg_i32 ✅ 5s 3s +67%
mld_sample_s1_s2 ✅ 5s 5s +0%
ntt_native_x86_64 ✅ 5s 3s +67%
nttunpack_native_x86_64 ✅ 5s 3s +67%
pack_sig_h ✅ 5s 3s +67%
poly_uniform ✅ 5s 7s -29%
polyt1_pack ✅ 5s 2s +150%
polyt1_unpack ✅ 5s 2s +150%
polyveck_unpack_eta ✅ 5s 4s +25%
polyvecl_chknorm ✅ 5s 6s -17%
polyvecl_pointwise_acc_montgomery_native ✅ 5s 3s +67%
polyvecl_uniform_gamma1 ✅ 5s 4s +25%
sign_open ✅ 5s 3s +67%
sign_pk_from_sk ✅ 5s 6s -17%
unpack_sk ✅ 5s 4s +25%
unpack_sk_s2hat ✅ 5s 4s +25%
yvec_init ✅ 5s 4s +25%
keccak_finalize ✅ 4s 3s +33%
keccakf1600x4_xor_bytes ✅ 4s 3s +33%
mld_polymat_expand_entry ✅ 4s 3s +33%
pack_sk_s1 ✅ 4s 4s +0%
pointwise_native_x86_64 ✅ 4s 4s +0%
poly_caddq_native ✅ 4s 3s +33%
poly_chknorm ✅ 4s 6s -33%
poly_chknorm_native_aarch64 ✅ 4s 2s +100%
poly_decompose ✅ 4s 5s -20%
poly_decompose_c ✅ 4s 3s +33%
poly_ntt_native ✅ 4s 5s -20%
poly_permute_bitrev_to_custom_optional ✅ 4s 3s +33%
poly_pointwise_montgomery_native ✅ 4s 3s +33%
poly_use_hint_c ✅ 4s 4s +0%
polyvecl_pointwise_acc_montgomery ✅ 4s 6s -33%
polyvecl_unpack_z ✅ 4s 2s +100%
polyw1_pack ✅ 4s 4s +0%
polyz_unpack_native ✅ 4s 2s +100%
rej_eta ✅ 4s 3s +33%
rej_eta_native ✅ 4s 4s +0%
shake256 ✅ 4s 3s +33%
shake256_squeeze ✅ 4s 4s +0%
shake256x4_absorb_once ✅ 4s 2s +100%
sign_keypair ✅ 4s 5s -20%
sign_signature_pre_hash_internal ✅ 4s 6s -33%
sign_signature_pre_hash_shake256 ✅ 4s 5s -20%
sign_verify_pre_hash_shake256 ✅ 4s 6s -33%
sk_s2hat_get_poly ✅ 4s 3s +33%
sys_check_capability ✅ 4s 4s +0%
use_hint ✅ 4s 5s -20%
decompose ✅ 3s 4s -25%
intt_native_x86_64 ✅ 3s 5s -40%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid ✅ 3s 2s +50%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid ✅ 3s 2s +50%
keccak_f1600_x4_native_avx2 ✅ 3s 3s +0%
keccak_init ✅ 3s 2s +50%
keccak_squeeze ✅ 3s 3s +0%
keccakf1600_permute_native ✅ 3s 3s +0%
keccakf1600x4_extract_bytes_native ✅ 3s 5s -40%
keccakf1600x4_permute ✅ 3s 5s -40%
mld_ct_cmask_nonzero_u32 ✅ 3s 3s +0%
mld_ct_cmask_nonzero_u8 ✅ 3s 3s +0%
mld_ct_get_optblocker_u8 ✅ 3s 3s +0%
mld_keccakf1600x4_xor_bytes_c ✅ 3s 3s +0%
mld_value_barrier_i64 ✅ 3s 3s +0%
mld_value_barrier_u8 ✅ 3s 3s +0%
montgomery_reduce ✅ 3s 2s +50%
ntt_native_aarch64 ✅ 3s 3s +0%
pack_sig_c ✅ 3s 2s +50%
pack_sig_z ✅ 3s 3s +0%
pack_sk_rho_key_tr_s2 ✅ 3s 3s +0%
poly_caddq_c ✅ 3s 4s -25%
poly_caddq_native_aarch64 ✅ 3s 3s +0%
poly_caddq_native_x86_64 ✅ 3s - new
poly_chknorm_native ✅ 3s 3s +0%
poly_decompose_32_native_aarch64 ✅ 3s 3s +0%
poly_ntt ✅ 3s 3s +0%
poly_permute_bitrev_to_custom_optional_native ✅ 3s 4s -25%
poly_pointwise_montgomery ✅ 3s 2s +50%
poly_reduce ✅ 3s 2s +50%
poly_shiftl ✅ 3s 4s -25%
poly_uniform_gamma1_4x ✅ 3s 5s -40%
poly_use_hint ✅ 3s 5s -40%
polyeta_pack ✅ 3s 3s +0%
polyveck_reduce ✅ 3s 1s +200%
polyvecl_pack_eta ✅ 3s 3s +0%
polyvecl_uniform_gamma1_serial ✅ 3s 4s -25%
polyvecl_unpack_eta ✅ 3s 6s -50%
polyz_unpack_17_native_aarch64 ✅ 3s 6s -50%
reduce32 ✅ 3s 2s +50%
rej_eta_c ✅ 3s 3s +0%
rej_uniform_native_aarch64 ✅ 3s 7s -57%
shake128_finalize ✅ 3s 1s +200%
shake128_init ✅ 3s 3s +0%
shake256_absorb ✅ 3s 2s +50%
sig_unpack_hints ✅ 3s 5s -40%
sign_signature ✅ 3s 3s +0%
sign_signature_extmu ✅ 3s 5s -40%
sign_verify_pre_hash_internal ✅ 3s 2s +50%
sk_s1hat_get_poly ✅ 3s 4s -25%
unpack_sk_s1hat ✅ 3s 4s -25%
caddq ✅ 2s 4s -50%
fqscale ✅ 2s 2s +0%
keccak_f1600_x1_native_aarch64 ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v84a ✅ 2s 3s -33%
keccakf1600_permute ✅ 2s 4s -50%
keccakf1600_xor_bytes ✅ 2s 2s +0%
keccakf1600x4_extract_bytes ✅ 2s 3s -33%
keccakf1600x4_xor_bytes_native ✅ 2s 2s +0%
mld_ct_abs_i32 ✅ 2s 3s -33%
mld_ct_get_optblocker_u32 ✅ 2s 2s +0%
mld_ct_sel_int32 ✅ 2s 1s +100%
mld_h ✅ 2s 2s +0%
mld_keccakf1600_extract_bytes ✅ 2s 2s +0%
mld_value_barrier_u32 ✅ 2s 1s +100%
poly_caddq ✅ 2s 3s -33%
poly_decompose_88_native_aarch64 ✅ 2s 3s -33%
poly_decompose_native ✅ 2s 4s -50%
poly_invntt_tomont ✅ 2s 2s +0%
poly_ntt_c ✅ 2s 3s -33%
poly_sub ✅ 2s 5s -60%
poly_uniform_gamma1 ✅ 2s 2s +0%
poly_use_hint_native ✅ 2s 4s -50%
poly_use_hint_native_aarch64 ✅ 2s 2s +0%
polyt0_pack ✅ 2s 3s -33%
polyvec_matrix_pointwise_montgomery_row ✅ 2s 3s -33%
polyveck_pack_w1 ✅ 2s 3s -33%
polyz_pack ✅ 2s 2s +0%
polyz_unpack ✅ 2s 3s -33%
power2round ✅ 2s 2s +0%
rej_uniform_eta_native_aarch64 ✅ 2s - new
shake128_absorb ✅ 2s 4s -50%
shake128_release ✅ 2s 3s -33%
shake128_squeeze ✅ 2s 3s -33%
shake128x4_absorb_once ✅ 2s 2s +0%
shake128x4_squeezeblocks ✅ 2s 4s -50%
shake256_finalize ✅ 2s 3s -33%
shake256_release ✅ 2s 2s +0%
shake256x4_squeezeblocks ✅ 2s 1s +100%
sign_verify_extmu ✅ 2s 4s -50%
unpack_pk_t1 ✅ 2s 1s +100%
yvec_get_poly ✅ 2s 6s -67%
intt_native_aarch64 ✅ 1s 5s -80%
keccak_f1600_x1_native_aarch64_v84a ✅ 1s 2s -50%
keccakf1600_extract_bytes (big endian) ✅ 1s 4s -75%
keccakf1600_xor_bytes (big endian) ✅ 1s 3s -67%
make_hint ✅ 1s 6s -83%
mld_ct_get_optblocker_i64 ✅ 1s 1s +0%
mld_keccakf1600x4_extract_bytes_c ✅ 1s 3s -67%
pointwise_native_aarch64 ✅ 1s 3s -67%
poly_invntt_tomont_native ✅ 1s 5s -80%
polyveck_pack_eta ✅ 1s 3s -67%
shake256_init ✅ 1s 2s -50%
sk_t0hat_get_poly ✅ 1s 3s -67%

@jakemas jakemas force-pushed the add-hol-light-rej-uniform-eta4 branch from 73d8d61 to a7cc582 Compare April 15, 2026 11:06
@jakemas jakemas changed the title Add HOL Light rej_uniform_eta4 proof for AArch64 Add HOL Light rej_uniform_eta proofs for AArch64 Apr 15, 2026
@jakemas jakemas force-pushed the add-hol-light-rej-uniform-eta4 branch 9 times, most recently from 77cb935 to f986df8 Compare April 15, 2026 17:09
@mkannwischer mkannwischer self-assigned this Apr 22, 2026
@jakemas jakemas force-pushed the add-hol-light-rej-uniform-eta4 branch 3 times, most recently from 37dfafd to ddd97de Compare April 24, 2026 20:10
@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Apr 24, 2026 •
edited
Loading

CBMC Results (ML-DSA-44, REDUCE-RAM)

Full Results (201 proofs)
Proof Status Current Previous Change
**TOTAL** ✅ 1513s 1437s +5.3%
poly_pointwise_montgomery_c ✅ 192s 171s +12%
rej_uniform_native ✅ 114s 105s +9%
mld_invntt_layer ✅ 109s 106s +3%
polyvec_matrix_pointwise_montgomery_yvec ✅ 94s 93s +1%
mld_ct_memcmp ✅ 68s 67s +1%
mld_ntt_layer ✅ 44s 42s +5%
fqmul ✅ 29s 29s +0%
mld_attempt_signature_generation ✅ 26s 24s +8%
keccakf1600x4_permute_native ✅ 23s 24s -4%
rej_uniform ✅ 22s 20s +10%
sign_verify_internal ✅ 21s 22s -5%
rej_uniform_c ✅ 19s 16s +19%
mld_check_pct ✅ 18s 16s +12%
mld_ntt_butterfly_block ✅ 18s 17s +6%
polyeta_unpack ✅ 15s 17s -12%
polyveck_chknorm ✅ 14s 9s +56%
poly_chknorm_c ✅ 12s 12s +0%
poly_uniform_eta_4x ✅ 12s 10s +20%
poly_add ✅ 11s 10s +10%
polyt0_unpack ✅ 11s 12s -8%
polyvec_matrix_pointwise_montgomery_row ✅ 11s 8s +38%
polyz_unpack_c ✅ 11s 15s -27%
poly_invntt_tomont_c ✅ 10s 7s +43%
keccak_absorb_once_x4 ✅ 9s 10s -10%
poly_caddq_c ✅ 8s 10s -20%
polyveck_reduce ✅ 8s 4s +100%
compute_pack_t0_t1 ✅ 7s 8s -12%
pointwise_acc_native_x86_64 ✅ 7s 6s +17%
poly_decompose_c ✅ 7s 10s -30%
poly_power2round ✅ 7s 8s -12%
sign_signature_internal ✅ 7s 5s +40%
keccak_absorb ✅ 6s 7s -14%
mld_compute_pack_z ✅ 6s 6s +0%
mld_h ✅ 6s 3s +100%
poly_ntt_native ✅ 6s 4s +50%
poly_uniform ✅ 6s 5s +20%
polyveck_decompose ✅ 6s 6s +0%
sig_unpack_hints ✅ 6s 3s +100%
sign ✅ 6s 7s -14%
sign_pk_from_sk ✅ 6s 6s +0%
sign_signature_extmu ✅ 6s 4s +50%
mld_ct_sel_int32 ✅ 5s 3s +67%
mld_keccakf1600_permute_c ✅ 5s 7s -29%
mld_keccakf1600x4_extract_bytes_c ✅ 5s 5s +0%
mld_value_barrier_u32 ✅ 5s 2s +150%
pack_sig_h ✅ 5s 3s +67%
pointwise_acc_native_aarch64 ✅ 5s 5s +0%
pointwise_native_x86_64 ✅ 5s 2s +150%
poly_caddq_native ✅ 5s 5s +0%
poly_chknorm_native ✅ 5s 3s +67%
poly_invntt_tomont ✅ 5s 2s +150%
poly_invntt_tomont_native ✅ 5s 4s +25%
poly_shiftl ✅ 5s 6s -17%
poly_sub ✅ 5s 2s +150%
poly_uniform_4x ✅ 5s 3s +67%
poly_use_hint ✅ 5s 1s +400%
polyt1_unpack ✅ 5s 2s +150%
polyvec_matrix_expand ✅ 5s 3s +67%
polyvecl_chknorm ✅ 5s 7s -29%
polyvecl_ntt ✅ 5s 4s +25%
polyz_unpack ✅ 5s 2s +150%
rej_eta_c ✅ 5s 3s +67%
rej_eta_native ✅ 5s 5s +0%
shake128_squeeze ✅ 5s 2s +150%
sign_keypair_internal ✅ 5s 3s +67%
sign_open ✅ 5s 5s +0%
sign_verify ✅ 5s 3s +67%
sign_verify_extmu ✅ 5s 5s +0%
fqscale ✅ 4s 4s +0%
keccak_f1600_x1_native_aarch64 ✅ 4s 3s +33%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid ✅ 4s 1s +300%
keccak_squeezeblocks_x4 ✅ 4s 5s -20%
mld_prepare_domain_separation_prefix ✅ 4s 5s -20%
mld_sample_s1_s2 ✅ 4s 2s +100%
pack_sk_rho_key_tr_s2 ✅ 4s 3s +33%
pointwise_native_aarch64 ✅ 4s 2s +100%
poly_challenge ✅ 4s 4s +0%
poly_decompose_88_native_aarch64 ✅ 4s 3s +33%
poly_permute_bitrev_to_custom_optional_native ✅ 4s 3s +33%
poly_reduce ✅ 4s 3s +33%
poly_uniform_gamma1_4x ✅ 4s 5s -20%
poly_use_hint_c ✅ 4s 2s +100%
polyeta_pack ✅ 4s 3s +33%
polyveck_invntt_tomont ✅ 4s 3s +33%
polyveck_pack_w1 ✅ 4s 1s +300%
polyvecl_pointwise_acc_montgomery_c ✅ 4s 2s +100%
polyvecl_pointwise_acc_montgomery_native ✅ 4s 3s +33%
polyvecl_unpack_eta ✅ 4s 3s +33%
polyz_unpack_native ✅ 4s 3s +33%
rej_eta ✅ 4s 3s +33%
rej_uniform_native_aarch64 ✅ 4s 5s -20%
shake128_release ✅ 4s 1s +300%
shake256x4_squeezeblocks ✅ 4s 2s +100%
sign_keypair ✅ 4s 3s +33%
sign_signature_pre_hash_shake256 ✅ 4s 3s +33%
sign_verify_pre_hash_internal ✅ 4s 2s +100%
unpack_pk_t1 ✅ 4s 2s +100%
unpack_sk_s2hat ✅ 4s 2s +100%
intt_native_aarch64 ✅ 3s 3s +0%
intt_native_x86_64 ✅ 3s 7s -57%
keccak_f1600_x4_native_aarch64_v84a ✅ 3s 2s +50%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid ✅ 3s 3s +0%
keccak_squeeze ✅ 3s 4s -25%
keccakf1600_extract_bytes (big endian) ✅ 3s 2s +50%
keccakf1600_permute_native ✅ 3s 3s +0%
keccakf1600x4_extract_bytes_native ✅ 3s 2s +50%
mld_ct_cmask_nonzero_u8 ✅ 3s 3s +0%
ntt_native_aarch64 ✅ 3s 3s +0%
ntt_native_x86_64 ✅ 3s 2s +50%
nttunpack_native_x86_64 ✅ 3s 5s -40%
pack_sk_s1 ✅ 3s 3s +0%
poly_caddq ✅ 3s 2s +50%
poly_caddq_native_aarch64 ✅ 3s 3s +0%
poly_decompose ✅ 3s 3s +0%
poly_decompose_32_native_aarch64 ✅ 3s 2s +50%
poly_decompose_native ✅ 3s 2s +50%
poly_ntt_c ✅ 3s 4s -25%
poly_pointwise_montgomery ✅ 3s 2s +50%
poly_pointwise_montgomery_native ✅ 3s 5s -40%
poly_uniform_eta ✅ 3s 5s -40%
poly_use_hint_native ✅ 3s 4s -25%
polyt0_pack ✅ 3s 3s +0%
polyveck_ntt ✅ 3s 2s +50%
polyveck_unpack_eta ✅ 3s 2s +50%
polyvecl_uniform_gamma1 ✅ 3s 3s +0%
polyw1_pack ✅ 3s 2s +50%
polyz_pack ✅ 3s 2s +50%
polyz_unpack_17_native_aarch64 ✅ 3s 3s +0%
shake128_init ✅ 3s 2s +50%
shake128x4_absorb_once ✅ 3s 3s +0%
shake128x4_squeezeblocks ✅ 3s 4s -25%
shake256_squeeze ✅ 3s 3s +0%
shake256x4_absorb_once ✅ 3s 3s +0%
sign_signature_pre_hash_internal ✅ 3s 3s +0%
sign_verify_pre_hash_shake256 ✅ 3s 4s -25%
sys_check_capability ✅ 3s 4s -25%
unpack_sk_s1hat ✅ 3s 1s +200%
yvec_get_poly ✅ 3s 4s -25%
yvec_init ✅ 3s 1s +200%
caddq ✅ 2s 2s +0%
decompose ✅ 2s 3s -33%
keccak_finalize ✅ 2s 3s -33%
keccak_init ✅ 2s 2s +0%
keccakf1600_permute ✅ 2s 3s -33%
keccakf1600_xor_bytes (big endian) ✅ 2s 2s +0%
keccakf1600x4_extract_bytes ✅ 2s 2s +0%
keccakf1600x4_xor_bytes_native ✅ 2s 4s -50%
make_hint ✅ 2s 3s -33%
mld_ct_cmask_neg_i32 ✅ 2s 3s -33%
mld_ct_get_optblocker_i64 ✅ 2s 1s +100%
mld_ct_get_optblocker_u8 ✅ 2s 2s +0%
mld_keccakf1600_extract_bytes ✅ 2s 4s -50%
mld_keccakf1600x4_xor_bytes_c ✅ 2s 2s +0%
mld_polymat_expand_entry ✅ 2s 2s +0%
mld_sample_s1_s2_serial ✅ 2s 5s -60%
mld_value_barrier_i64 ✅ 2s 5s -60%
mld_value_barrier_u8 ✅ 2s 2s +0%
montgomery_reduce ✅ 2s 3s -33%
pack_sig_c ✅ 2s 3s -33%
pack_sig_z ✅ 2s 5s -60%
poly_caddq_native_x86_64 ✅ 2s - new
poly_chknorm ✅ 2s 3s -33%
poly_chknorm_native_aarch64 ✅ 2s 2s +0%
polyt1_pack ✅ 2s 2s +0%
polyvec_matrix_expand_serial ✅ 2s 5s -60%
polyveck_caddq ✅ 2s 4s -50%
polyveck_pack_eta ✅ 2s 2s +0%
polyvecl_pack_eta ✅ 2s 4s -50%
polyvecl_pointwise_acc_montgomery ✅ 2s 2s +0%
polyvecl_uniform_gamma1_serial ✅ 2s 3s -33%
polyvecl_unpack_z ✅ 2s 2s +0%
polyz_unpack_19_native_aarch64 ✅ 2s 2s +0%
reduce32 ✅ 2s 1s +100%
rej_uniform_eta_native_aarch64 ✅ 2s - new
shake128_absorb ✅ 2s 4s -50%
shake128_finalize ✅ 2s 2s +0%
shake256 ✅ 2s 3s -33%
shake256_absorb ✅ 2s 3s -33%
shake256_finalize ✅ 2s 2s +0%
shake256_init ✅ 2s 4s -50%
shake256_release ✅ 2s 2s +0%
sign_signature ✅ 2s 3s -33%
sk_s1hat_get_poly ✅ 2s 3s -33%
sk_s2hat_get_poly ✅ 2s 2s +0%
sk_t0hat_get_poly ✅ 2s 2s +0%
unpack_sk ✅ 2s 2s +0%
unpack_sk_t0hat ✅ 2s 3s -33%
use_hint ✅ 2s 3s -33%
keccak_f1600_x1_native_aarch64_v84a ✅ 1s 2s -50%
keccak_f1600_x4_native_avx2 ✅ 1s 2s -50%
keccakf1600_xor_bytes ✅ 1s 2s -50%
keccakf1600x4_permute ✅ 1s 3s -67%
keccakf1600x4_xor_bytes ✅ 1s 3s -67%
mld_ct_abs_i32 ✅ 1s 2s -50%
mld_ct_cmask_nonzero_u32 ✅ 1s 3s -67%
mld_ct_get_optblocker_u32 ✅ 1s 3s -67%
poly_ntt ✅ 1s 1s +0%
poly_permute_bitrev_to_custom_optional ✅ 1s 3s -67%
poly_uniform_gamma1 ✅ 1s 3s -67%
poly_use_hint_native_aarch64 ✅ 1s 3s -67%
power2round ✅ 1s 6s -83%

@jakemas jakemas mentioned this pull request May 6, 2026
Open
@jakemas jakemas force-pushed the add-hol-light-rej-uniform-eta4 branch from 9cacda6 to da5f60b Compare May 6, 2026 20:53
@jakemas jakemas mentioned this pull request May 9, 2026
Open
@jakemas jakemas force-pushed the add-hol-light-rej-uniform-eta4 branch 24 times, most recently from 7429b71 to 0c8ed0a Compare May 22, 2026 00:03
@jakemas jakemas marked this pull request as ready for review May 22, 2026 01:54
@jakemas
HOL-Light: Add AArch64 rej_uniform_eta_{2,4} correctness, memory-safe…
63f752b 
…ty proofs

Add functional correctness, subroutine correctness, memory-safety and
subroutine-safety proofs for the AArch64 assembly implementations of
rej_uniform_eta for both eta variants:
- rej_uniform_eta2 (eta=2, used in ML-DSA-44)
- rej_uniform_eta4 (eta=4, used in ML-DSA-65/87)

Memory safety follows the mlkem_rej_uniform_VARIABLE_TIME pattern in
s2n-bignum because the loop count is data-dependent (which nibbles
pass the < 9 / < 15 filter).

Written with the assistance of Claude Opus 4.7.

Signed-off-by: Jake Massimo <jakemas@amazon.com>
@jakemas jakemas force-pushed the add-hol-light-rej-uniform-eta4 branch from 0c8ed0a to 63f752b Compare May 22, 2026 18:30
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

@mkannwischer mkannwischer

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

HOL-Light: Prove AArch64 rej_uniform_eta

3 participants

@jakemas @oqs-bot @mkannwischer