Skip to content

x86_64 + HOL-Light: Replace rej_uniform_eta2/eta4 intrinsics with hand-written assembly and HOL-Light proofs - #1188

Merged
mkannwischer merged 1 commit into
mainfrom
jakemas/rej-uniform-eta-asm
Jul 17, 2026
Merged

x86_64 + HOL-Light: Replace rej_uniform_eta2/eta4 intrinsics with hand-written assembly and HOL-Light proofs#1188
mkannwischer merged 1 commit into
mainfrom
jakemas/rej-uniform-eta-asm

Conversation

@jakemas

@jakemas jakemas commented Jun 16, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Summary

Replaces the AVX2 intrinsics implementations of rej_uniform_eta2 and rej_uniform_eta4 with hand-written x86_64 assembly, and adds HOL-Light functional-correctness and memory-safety proofs for both routines. Follows the same approach as #1014:

  • Table passed as a parameter (consistent with the aarch64 approach), avoiding external symbol references for simpasm compatibility.
  • All constants constructed from immediates (no .rodata), enabling HOL-Light formal verification.
  • __contract__ annotations on the asm entry points (CBMC), kept in sync with the HOL-Light specs.
  • meta.h wires both eta2 and eta4 to the new asm, so the functional test suite exercises both paths.
  • The x86_64 HOL-Light Makefile and dump_bytecode.ml register the eta2/eta4 bytecode dump targets; ABI-checker tests added for both.
  • Adds a poly_uniform_eta_4x component benchmark.

s2n-bignum dependency

The proofs use the VPBROADCASTW instruction, added in awslabs/s2n-bignum#421. Until that merges, the nix pin (nix/s2n_bignum/default.nix) is temporarily pointed at the jakemas/s2n-bignum fork branch so CI can decode the instruction; it will be repointed to awslabs main once #421 lands.

@jakemas
jakemas force-pushed the jakemas/rej-uniform-eta-asm branch 5 times, most recently from f789e8d to 1e78719 Compare June 16, 2026 23:56
@oqs-bot

oqs-bot commented Jun 17, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

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

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

@oqs-bot

oqs-bot commented Jun 17, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

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

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

@oqs-bot

oqs-bot commented Jun 17, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

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

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

@oqs-bot

oqs-bot commented Jun 17, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-65)

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

@oqs-bot

oqs-bot commented Jun 17, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-44)

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

@oqs-bot

oqs-bot commented Jun 17, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-87)

⚠️ Attention Required

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

@jakemas
jakemas force-pushed the jakemas/rej-uniform-eta-asm branch from 1e78719 to 7c13c63 Compare June 17, 2026 01:36
jakemas
jakemas commented Jun 17, 2026
View reviewed changes
Comment thread dev/x86_64/src/rej_uniform_eta2_avx2_asm.S Resolved
github-actions[bot]
github-actions Bot reviewed Jun 17, 2026
View reviewed changes

@github-actions github-actions Bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Mac Mini (M1, 2020) benchmarks (opt)

Details
Benchmark suite Current: 237e387 Previous: 31300ad Ratio
ML-DSA-44 keypair 46524 cycles 46501 cycles 1.00
ML-DSA-44 sign 131156 cycles 131159 cycles 1.00
ML-DSA-44 verify 47325 cycles 47327 cycles 1.00
ML-DSA-65 keypair 81696 cycles 81682 cycles 1.00
ML-DSA-65 sign 215403 cycles 215381 cycles 1.00
ML-DSA-65 verify 79311 cycles 79309 cycles 1.00
ML-DSA-87 keypair 132415 cycles 132436 cycles 1.00
ML-DSA-87 sign 277406 cycles 277663 cycles 1.00
ML-DSA-87 verify 134055 cycles 134051 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

github-actions[bot]
github-actions Bot reviewed Jun 17, 2026
View reviewed changes

@github-actions github-actions Bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Mac Mini (M1, 2020) benchmarks (no-opt)

Details
Benchmark suite Current: 237e387 Previous: 31300ad Ratio
ML-DSA-44 keypair 113028 cycles 112820 cycles 1.00
ML-DSA-44 sign 402081 cycles 401084 cycles 1.00
ML-DSA-44 verify 119691 cycles 119458 cycles 1.00
ML-DSA-65 keypair 192981 cycles 192907 cycles 1.00
ML-DSA-65 sign 650273 cycles 649936 cycles 1.00
ML-DSA-65 verify 192931 cycles 192844 cycles 1.00
ML-DSA-87 keypair 318799 cycles 318799 cycles 1
ML-DSA-87 sign 828743 cycles 828921 cycles 1.00
ML-DSA-87 verify 326813 cycles 326734 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

github-actions[bot]
github-actions Bot reviewed Jun 17, 2026
View reviewed changes

@github-actions github-actions Bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Arm Cortex-A72 (Raspberry Pi 4) benchmarks (opt)

Details
Benchmark suite Current: 237e387 Previous: 31300ad Ratio
ML-DSA-44 keypair 222141 cycles 223446 cycles 0.99
ML-DSA-44 sign 614240 cycles 634283 cycles 0.97
ML-DSA-44 verify 226725 cycles 223226 cycles 1.02
ML-DSA-65 keypair 385352 cycles 393894 cycles 0.98
ML-DSA-65 sign 1003734 cycles 1022240 cycles 0.98
ML-DSA-65 verify 372158 cycles 378918 cycles 0.98
ML-DSA-87 keypair 650198 cycles 644349 cycles 1.01
ML-DSA-87 sign 1362778 cycles 1332260 cycles 1.02
ML-DSA-87 verify 638012 cycles 627970 cycles 1.02

This comment was automatically generated by workflow using github-action-benchmark.

github-actions[bot]
github-actions Bot reviewed Jun 17, 2026
View reviewed changes

@github-actions github-actions Bot left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'Arm Cortex-A72 (Raspberry Pi 4) benchmarks (opt)'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.03.

Benchmark suite Current: 7c13c63 Previous: 70fdba0 Ratio
ML-DSA-44 keypair 227496 cycles 219616 cycles 1.04
ML-DSA-44 verify 235419 cycles 214195 cycles 1.10
ML-DSA-87 keypair 661599 cycles 635525 cycles 1.04
ML-DSA-87 sign 1369715 cycles 1306530 cycles 1.05
ML-DSA-87 verify 645122 cycles 616298 cycles 1.05

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Jun 17, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Intel Xeon 4th gen (c7i)

Details
Benchmark suite Current: 237e387 Previous: 31300ad Ratio
ML-DSA-44 keypair 43323 cycles 43311 cycles 1.00
ML-DSA-44 sign 129973 cycles 130234 cycles 1.00
ML-DSA-44 verify 45201 cycles 45328 cycles 1.00
ML-DSA-65 keypair 75758 cycles 75678 cycles 1.00
ML-DSA-65 sign 213832 cycles 214141 cycles 1.00
ML-DSA-65 verify 74325 cycles 74551 cycles 1.00
ML-DSA-87 keypair 123264 cycles 122951 cycles 1.00
ML-DSA-87 sign 270347 cycles 270036 cycles 1.00
ML-DSA-87 verify 120938 cycles 120608 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Jun 17, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Intel Xeon 4th gen (c7i) (no-opt)

Details
Benchmark suite Current: 237e387 Previous: 31300ad Ratio
ML-DSA-44 keypair 91475 cycles 91650 cycles 1.00
ML-DSA-44 sign 352301 cycles 353391 cycles 1.00
ML-DSA-44 verify 99818 cycles 100249 cycles 1.00
ML-DSA-65 keypair 153858 cycles 153883 cycles 1.00
ML-DSA-65 sign 572079 cycles 571341 cycles 1.00
ML-DSA-65 verify 159979 cycles 159780 cycles 1.00
ML-DSA-87 keypair 255344 cycles 255804 cycles 1.00
ML-DSA-87 sign 726579 cycles 726454 cycles 1.00
ML-DSA-87 verify 264184 cycles 264128 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Jun 17, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

AMD EPYC 3rd gen (c6a)

Details
Benchmark suite Current: 237e387 Previous: 31300ad Ratio
ML-DSA-44 keypair 55494 cycles 55575 cycles 1.00
ML-DSA-44 sign 158449 cycles 159176 cycles 1.00
ML-DSA-44 verify 57633 cycles 58038 cycles 0.99
ML-DSA-65 keypair 96318 cycles 95925 cycles 1.00
ML-DSA-65 sign 258646 cycles 259688 cycles 1.00
ML-DSA-65 verify 95634 cycles 96324 cycles 0.99
ML-DSA-87 keypair 155356 cycles 154620 cycles 1.00
ML-DSA-87 sign 323135 cycles 323315 cycles 1.00
ML-DSA-87 verify 151250 cycles 151152 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

github-actions[bot]
github-actions Bot reviewed Jun 17, 2026
View reviewed changes

@github-actions github-actions Bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Arm Cortex-A72 (Raspberry Pi 4) benchmarks (no-opt)

Details
Benchmark suite Current: 237e387 Previous: 31300ad Ratio
ML-DSA-44 keypair 298957 cycles 309045 cycles 0.97
ML-DSA-44 sign 1130396 cycles 1181040 cycles 0.96
ML-DSA-44 verify 327888 cycles 338438 cycles 0.97
ML-DSA-65 keypair 557436 cycles 569427 cycles 0.98
ML-DSA-65 sign 1888548 cycles 1984198 cycles 0.95
ML-DSA-65 verify 538964 cycles 570461 cycles 0.94
ML-DSA-87 keypair 861727 cycles 894629 cycles 0.96
ML-DSA-87 sign 2454019 cycles 2499364 cycles 0.98
ML-DSA-87 verify 907684 cycles 918394 cycles 0.99

This comment was automatically generated by workflow using github-action-benchmark.

github-actions[bot]
github-actions Bot reviewed Jun 17, 2026
View reviewed changes

@github-actions github-actions Bot left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'Arm Cortex-A72 (Raspberry Pi 4) benchmarks (no-opt)'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.03.

Benchmark suite Current: 7c13c63 Previous: 70fdba0 Ratio
ML-DSA-44 keypair 312772 cycles 294913 cycles 1.06
ML-DSA-44 sign 1193382 cycles 1147432 cycles 1.04
ML-DSA-87 keypair 904673 cycles 847930 cycles 1.07
ML-DSA-87 sign 2468732 cycles 2393137 cycles 1.03
ML-DSA-87 verify 906571 cycles 874118 cycles 1.04

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Jun 17, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

AMD EPYC 3rd gen (c6a) (no-opt)

Details
Benchmark suite Current: 237e387 Previous: 31300ad Ratio
ML-DSA-44 keypair 133692 cycles 133431 cycles 1.00
ML-DSA-44 sign 520225 cycles 519219 cycles 1.00
ML-DSA-44 verify 146942 cycles 146686 cycles 1.00
ML-DSA-65 keypair 223592 cycles 224467 cycles 1.00
ML-DSA-65 sign 841919 cycles 843782 cycles 1.00
ML-DSA-65 verify 233762 cycles 234011 cycles 1.00
ML-DSA-87 keypair 366674 cycles 367264 cycles 1.00
ML-DSA-87 sign 1057851 cycles 1060362 cycles 1.00
ML-DSA-87 verify 380118 cycles 381078 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Jun 17, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Graviton2

Details
Benchmark suite Current: 237e387 Previous: 31300ad Ratio
ML-DSA-44 keypair 112327 cycles 112432 cycles 1.00
ML-DSA-44 sign 354085 cycles 353829 cycles 1.00
ML-DSA-44 verify 117505 cycles 117251 cycles 1.00
ML-DSA-65 keypair 194501 cycles 194915 cycles 1.00
ML-DSA-65 sign 584403 cycles 584545 cycles 1.00
ML-DSA-65 verify 193506 cycles 193060 cycles 1.00
ML-DSA-87 keypair 320982 cycles 321247 cycles 1.00
ML-DSA-87 sign 747665 cycles 747767 cycles 1.00
ML-DSA-87 verify 318354 cycles 318871 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Jun 17, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Graviton4

Details
Benchmark suite Current: 237e387 Previous: 31300ad Ratio
ML-DSA-44 keypair 67271 cycles 67334 cycles 1.00
ML-DSA-44 sign 198182 cycles 198212 cycles 1.00
ML-DSA-44 verify 70155 cycles 70164 cycles 1.00
ML-DSA-65 keypair 119526 cycles 119314 cycles 1.00
ML-DSA-65 sign 326414 cycles 326337 cycles 1.00
ML-DSA-65 verify 116796 cycles 116812 cycles 1.00
ML-DSA-87 keypair 196482 cycles 196615 cycles 1.00
ML-DSA-87 sign 421379 cycles 421442 cycles 1.00
ML-DSA-87 verify 193268 cycles 192981 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Jun 17, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

AMD EPYC 4th gen (c7a)

Details
Benchmark suite Current: 237e387 Previous: 31300ad Ratio
ML-DSA-44 keypair 48126 cycles 46837 cycles 1.03
ML-DSA-44 sign 138997 cycles 140005 cycles 0.99
ML-DSA-44 verify 49819 cycles 49295 cycles 1.01
ML-DSA-65 keypair 82346 cycles 85296 cycles 0.97
ML-DSA-65 sign 226618 cycles 235771 cycles 0.96
ML-DSA-65 verify 82230 cycles 83871 cycles 0.98
ML-DSA-87 keypair 130321 cycles 132099 cycles 0.99
ML-DSA-87 sign 281743 cycles 282238 cycles 1.00
ML-DSA-87 verify 129649 cycles 129367 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Jun 17, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Graviton4 (no-opt)

Details
Benchmark suite Current: 237e387 Previous: 31300ad Ratio
ML-DSA-44 keypair 127610 cycles 127745 cycles 1.00
ML-DSA-44 sign 441047 cycles 440937 cycles 1.00
ML-DSA-44 verify 136381 cycles 136447 cycles 1.00
ML-DSA-65 keypair 220529 cycles 220468 cycles 1.00
ML-DSA-65 sign 714603 cycles 714745 cycles 1.00
ML-DSA-65 verify 220923 cycles 221459 cycles 1.00
ML-DSA-87 keypair 364675 cycles 364373 cycles 1.00
ML-DSA-87 sign 915835 cycles 915833 cycles 1.00
ML-DSA-87 verify 370946 cycles 371331 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Jun 17, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Intel Xeon 3rd gen (c6i)

Details
Benchmark suite Current: 237e387 Previous: 31300ad Ratio
ML-DSA-44 keypair 61559 cycles 61513 cycles 1.00
ML-DSA-44 sign 188176 cycles 187961 cycles 1.00
ML-DSA-44 verify 66304 cycles 66502 cycles 1.00
ML-DSA-65 keypair 110399 cycles 108141 cycles 1.02
ML-DSA-65 sign 314455 cycles 311311 cycles 1.01
ML-DSA-65 verify 111028 cycles 108776 cycles 1.02
ML-DSA-87 keypair 173234 cycles 171604 cycles 1.01
ML-DSA-87 sign 378684 cycles 380707 cycles 0.99
ML-DSA-87 verify 171059 cycles 172479 cycles 0.99

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Jun 17, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Graviton2 (no-opt)

Details
Benchmark suite Current: 237e387 Previous: 31300ad Ratio
ML-DSA-44 keypair 212157 cycles 211410 cycles 1.00
ML-DSA-44 sign 761446 cycles 758945 cycles 1.00
ML-DSA-44 verify 229897 cycles 228936 cycles 1.00
ML-DSA-65 keypair 378864 cycles 377838 cycles 1.00
ML-DSA-65 sign 1248060 cycles 1248443 cycles 1.00
ML-DSA-65 verify 373372 cycles 372800 cycles 1.00
ML-DSA-87 keypair 602524 cycles 600578 cycles 1.00
ML-DSA-87 sign 1584621 cycles 1583512 cycles 1.00
ML-DSA-87 verify 618342 cycles 616106 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@jakemas
jakemas force-pushed the jakemas/rej-uniform-eta-asm branch 6 times, most recently from df464ba to 44c3af7 Compare July 14, 2026 23:19
mkannwischer
mkannwischer approved these changes Jul 15, 2026
View reviewed changes

@mkannwischer mkannwischer left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Thanks @jakemas for the improvements.
This proof looks good to me now (except for the s2n-bignum pin - tagging as DO-NOT-MERGE accordingly so this does not get merged accidentally).

@hanno-becker could you please take a look at this proof too?

hanno-becker
hanno-becker reviewed Jul 15, 2026
View reviewed changes

@hanno-becker hanno-becker left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Thanks @jakemas, it looks like a massive effort! Kudos for getting it through.

I am bit concerned and certainly surprised about the size-creep in our proofs. The AArch64 proofs for the rejection sampling routines are ~3kLOC, but for x86_64 we're looking at 7kLOC for rej_uniform and now 10kLOC for rej_uniform_eta{2,4}.

Why are these proofs so long, and esp. so much longer than for AArch64? There must be something to learn here... either they're unnecesarily complex -- in which case we should simplify them -- or something is fundamentally more difficult (both between AArch64 and x86_64, and between rej_uniform and rej_uniform_eta{2,4}) -- in that case, too, it would be good to know what that is.

@jakemas

jakemas commented Jul 15, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor Author

Thanks @jakemas, it looks like a massive effort! Kudos for getting it through.

I am bit concerned and certainly surprised about the size-creep in our proofs. The AArch64 proofs for the rejection sampling routines are ~3kLOC, but for x86_64 we're looking at 7kLOC for rej_uniform and now 10kLOC for rej_uniform_eta{2,4}.

Why are these proofs so long, and esp. so much longer than for AArch64? There must be something to learn here... either they're unnecesarily complex -- in which case we should simplify them -- or something is fundamentally more difficult (both between AArch64 and x86_64, and between rej_uniform and rej_uniform_eta{2,4}) -- in that case, too, it would be good to know what that is.

Right, I agree they are big. I thought the same thing, and have been through rounds of parametrization, clean up, optimization. One note, in the last PR you asked for more comments and descriptions of the larger proofs, so there are ~2000 lines of comments in each of those proof files.

I'll do another pass now and look for ways this can be size reduced/optimized.

@jakemas
jakemas force-pushed the jakemas/rej-uniform-eta-asm branch from 44c3af7 to c4987d6 Compare July 15, 2026 20:15
@jakemas

jakemas commented Jul 15, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor Author

ok was able to make some large reductions:

  • rej_uniform_eta4_avx2_asm.ml: 9535 → 7995 (−1540, −16%), 2,151 comment lines, so 5800 with no comments, now completes in 11min
  • rej_uniform_eta2_avx2_asm.ml: 10149 → 9385 (−764, −8%), 1,182 comment lines, so 8200 with no comments, now completes in 48min

@mkannwischer

mkannwischer commented Jul 16, 2026

Copy link
Copy Markdown
Contributor

ok was able to make some large reductions:

  • rej_uniform_eta4_avx2_asm.ml: 9535 → 7995 (−1540, −16%), 2,151 comment lines, so 5800 with no comments, now completes in 11min
  • rej_uniform_eta2_avx2_asm.ml: 10149 → 9385 (−764, −8%), 1,182 comment lines, so 8200 with no comments, now completes in 48min

Thanks, these are welcome simplifications! Do you have an intuition why the proofs are more sizable than the corresponding Arm proofs?

At this point, I think we shouldn't block this PR due to proof complexity concerns (unless there are soundness concerns related to it). To me, getting v1 out is much more important. However, understanding what complexity is inherent to the code and what can be eliminated with more time would be good. Maybe we can open some follow-up issues.
@hanno-becker, WDYT?

@jakemas, do you know when we can expect the s2n-bignum PR to be merged? Is there anything I can help with?

@jakemas
jakemas force-pushed the jakemas/rej-uniform-eta-asm branch from 5901af9 to fcd0999 Compare July 16, 2026 02:52
@jakemas

jakemas commented Jul 16, 2026

Copy link
Copy Markdown
Contributor Author

I just pushed a new version, cleaning up the eta2 proof a little more and speeding it up slightly.

Thanks, these are welcome simplifications! Do you have an intuition why the proofs are more sizable than the corresponding Arm proofs?

Yeah, a few things compound here, and it's mostly instruction-set semantics rather than the algorithm, both sides run the same 256-entry mask-indexed lookup-table method (Arm via TBL, x86 via PSHUFB). I think the lane-crossing in AVX2 is the big one. Arm's TBL does a full cross-register 128-bit table lookup in one instruction, so there's no per-lane decomposition to reason about. More generally, in my experience the x86 proofs have consistently been more involved to write than their Arm counterparts, it feels like some of this gap is inherent to the platform rather than to this routine.

At this point, I think we shouldn't block this PR due to proof complexity concerns (unless there are soundness concerns related to it). To me, getting v1 out is much more important. However, understanding what complexity is inherent to the code and what can be eliminated with more time would be good. Maybe we can open some follow-up issues. @hanno-becker, WDYT?

I agree we shouldn't block on this, i'm happy to follow-up issues to track which of the remaining complexity is inherent vs. reducible with more time.

@jakemas, do you know when we can expect the s2n-bignum PR to be merged? Is there anything I can help with?

As for the instruction PR, I pinged John today to remind him to review. I also asked if he could take a look at this PR and check out the eta4/2 proofs to see if he can spot any further optimizations, or simpler tactics to use. I can follow up with any suggestion John may make, I'll also PR into s2n-bignum once we're merged here (I don't want to PR any asm that isn't stable here into s2n-bignum), so John will get a look at it then in review and may have ideas. But also, as I said, Hanno asked for more comments on the complex proofs, so there are 1000-2000 lines of comments, the files are now 9000 and 8000 lines, so we're at the ~7k bar from uniform_rej.

@jakemas
x86_64 + HOL-Light: Replace rej_uniform_eta2/eta4 intrinsics with han…
e249c22 
…d-written assembly and HOL-Light proofs

Replaces the rej_uniform_eta2 and rej_uniform_eta4 AVX2 intrinsics with
hand-written assembly, and adds HOL-Light functional-correctness and
memory-safety proofs for both x86_64 routines, plus the CBMC proof for the
native wrapper. Both routines are variable-time, so — as for the AArch64
eta proofs — only functional correctness and memory safety are proven, not
constant time.

The table is passed as a parameter and all constants are built from
immediates (no .rodata), following the rej_uniform approach in #1014.

Signed-off-by: Jake Massimo <jakemas@amazon.com>
@jakemas
jakemas force-pushed the jakemas/rej-uniform-eta-asm branch from fcd0999 to e249c22 Compare July 16, 2026 22:25
@jakemas

jakemas commented Jul 16, 2026

Copy link
Copy Markdown
Contributor Author

ok #421 is merged, updated nix hash. @mkannwischer :)

@mkannwischer

mkannwischer commented Jul 17, 2026

Copy link
Copy Markdown
Contributor

ok #421 is merged, updated nix hash. @mkannwischer :)

Amazing! Thanks - looks good. I've removed the DO-NOT-MERGE label accordingly.
Now waiting for @hanno-becker to take a look.

hanno-becker
hanno-becker reviewed Jul 17, 2026
View reviewed changes
Comment thread SOUNDNESS.md Resolved
hanno-becker
hanno-becker approved these changes Jul 17, 2026
View reviewed changes

@hanno-becker hanno-becker left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

LGTM.

This is a milestone. Many thanks @jakemas for all your hard work and perseverance in providing the HOL-Light proofs and navigating our requests!

@hanno-becker hanno-becker mentioned this pull request Jul 17, 2026
Merged
@mkannwischer
mkannwischer added this pull request to the merge queue Jul 17, 2026
Merged via the queue into main with commit 1dbd70f Jul 17, 2026
641 of 700 checks passed
@mkannwischer
mkannwischer deleted the jakemas/rej-uniform-eta-asm branch July 17, 2026 08:02
@mkannwischer mkannwischer mentioned this pull request Jul 17, 2026
Closed
This was referenced Aug 31, 2026
Merged
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@hanno-becker hanno-becker hanno-becker approved these changes
@github-actions github-actions[bot] github-actions[bot] left review comments
@oqs-bot oqs-bot oqs-bot left review comments
@mkannwischer mkannwischer mkannwischer approved these changes

Assignees

No one assigned

Labels

benchmark

Projects

None yet

Milestone

No milestone

4 participants

@jakemas @oqs-bot @mkannwischer @hanno-becker