Skip to content

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

Open
jakemas wants to merge 1 commit into
mainfrom
jakemas/rej-uniform-eta-asm
Open

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

Conversation

@jakemas

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

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

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

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

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

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

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

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

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

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

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.

oqs-bot
oqs-bot reviewed Jul 7, 2026
View reviewed changes

@oqs-bot oqs-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.

Graviton5 (no-opt)

Details
Benchmark suite Current: 237e387 Previous: 31300ad Ratio
ML-DSA-44 keypair 100037 cycles 100026 cycles 1.00
ML-DSA-44 sign 368981 cycles 369108 cycles 1.00
ML-DSA-44 verify 110162 cycles 110142 cycles 1.00
ML-DSA-65 keypair 174279 cycles 174573 cycles 1.00
ML-DSA-65 sign 599035 cycles 599096 cycles 1.00
ML-DSA-65 verify 177906 cycles 178198 cycles 1.00
ML-DSA-87 keypair 285478 cycles 285839 cycles 1.00
ML-DSA-87 sign 760123 cycles 759674 cycles 1.00
ML-DSA-87 verify 296766 cycles 296320 cycles 1.00

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

mkannwischer
mkannwischer requested changes Jul 9, 2026
View reviewed changes

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

Many thanks @jakemas for tackling the last two proofs. Looks like a massive amount of work.
The proven specifications are aligned with the aarch64 specs and look good to me!

There are a couple blocking issues:

  1. The CBMC specs are off by one.
  2. There are many dead lemmas that should be trimmed. Can you remove that is not needed here?
  3. There are many comments that don't help the reader understand the proof . Some read like status updates, some are an artifact of how you got there (search for cheat and dates 2026-xx-yy). Can you do a pass though the comments and keep only what is useful?

Could you tackle those please?

Comment thread nix/s2n_bignum/default.nix
Comment thread dev/x86_64/src/arith_native_x86_64.h Outdated
Comment thread dev/x86_64/src/arith_native_x86_64.h Outdated
Comment thread scripts/autogen
Comment thread mldsa/src/native/x86_64/meta.h Outdated
Comment thread proofs/hol_light/x86_64/proofs/rej_uniform_eta4_avx2_asm.ml Outdated
Comment thread proofs/hol_light/x86_64/proofs/rej_uniform_eta4_avx2_asm.ml Outdated
Comment thread proofs/hol_light/x86_64/proofs/rej_uniform_eta4_avx2_asm.ml Outdated
Comment thread proofs/hol_light/x86_64/proofs/rej_uniform_eta4_avx2_asm.ml Outdated
Comment thread proofs/hol_light/x86_64/proofs/rej_uniform_eta4_avx2_asm.ml Outdated
@jakemas jakemas force-pushed the jakemas/rej-uniform-eta-asm branch 7 times, most recently from 908d880 to b157440 Compare July 13, 2026 19:33
@jakemas

jakemas commented Jul 13, 2026

Copy link
Copy Markdown
Contributor Author

ok, all review addressed! @mkannwischer

mkannwischer
mkannwischer requested changes Jul 14, 2026
View reviewed changes

@mkannwischer mkannwischer 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, there are still quite a few dead theorems:

  rej_uniform_eta4_avx2_asm.ml (21):
  L424  PSHUFB_TABLE_GATHER          L3011 SUB_LIST_256_FROM_PARTIAL_REJ
  L835  wzx256                       L3030 SCALAR_TAIL_N_EQ_17
  L1198 POPCNT_VPMOVMSKB_LOW8        L3047 LENGTH_OUTLIST0_LE_280
  L1800 REJ_SAMPLE_ETA4_BYTES_16_AS_4 L3128 NIBLEN_BOUND_FROM_WOP
  L2236 POPCNT_NIBBLES_4_BYTES_BRIDGE L3239 REJ_PREFIX_STEP_4
  L2792 SUBITER1_VALUE               L3259 GATHER_WIDE
  L2903 SUBITER_OUTLEN_STEP_4        L3269 MASK_WIDE
  L2965 WORD_SUB_4_NIBBLE_INT32_AS_SX L3296 SIMD2_EXPAND_CONV
  L3307 MASKBIT_PF_TAC               L4018 SI2_GATHER_TO_STORE
  L4286 SI3_GATHER                   L4536 SI4_GATHER
  L7813 DISCARD_OLDSTATE_KEEP_EVENTS_TAC

  rej_uniform_eta2_avx2_asm.ml (12):
  L506  PSHUFB_TABLE_GATHER          L2649 SUBITER_GATHER_NIB_ETA2
  L1278 POPCNT_VPMOVMSKB_LOW8        L2675 SUBITER_MASK_NIB_ETA2
  L1489 SUBITER_STORE_POSTCOND       L2680 MASK_ACCEPT_ETA2
  L2023 POPCNT_NIBBLES_4_BYTES_BRIDGE L2849 REJ_PREFIX_STEP_4
  L2065 ETA_GATHER                   L3244 ETA2_SI1_REDUCE_REFOLD_TAC
  L2086 REDUCE32_LANE_ETA2           L6578 MIDGUARD_NOT_TAKEN_CLEAN_ETA2

(Claude found those, I randomly checked a few)
Could you remove those as well, please?

The comments in the eta4 file are now much cleaner, thank you! In the eta2 files I still see what looks like debugging commentary (particularly the ★CASE4 FIX comments). Could you please clean those up too?

Comment thread proofs/hol_light/x86_64/proofs/rej_uniform_eta4_avx2_asm.ml Outdated
Comment thread proofs/hol_light/x86_64/proofs/rej_uniform_eta2_avx2_asm.ml Outdated
@jakemas jakemas force-pushed the jakemas/rej-uniform-eta-asm branch from b157440 to b6fce4e Compare July 14, 2026 17:16
@jakemas

jakemas commented Jul 14, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor Author

Thanks @mkannwischer! Both addressed in the latest push:

Dead theorems — removed all 21 flagged in eta4 and all 12 in eta2. While doing eta2 I also dropped three now-orphaned private helpers (gen_gather, gen_mask, mask_tac) that only fed the removed SUBITER_GATHER_NIB_ETA2/SUBITER_MASK_NIB_ETA2, so they don't become the next round of dead code.

eta2 debugging commentary — cleaned up all the ★ CASE4 FIX #N markers.

@jakemas jakemas force-pushed the jakemas/rej-uniform-eta-asm branch 7 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
x86_64 + HOL-Light: Replace rej_uniform_eta2/eta4 intrinsics with han…
fcd0999 
…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. The
proofs use the VPBROADCASTW instruction, so the s2n-bignum nix pin is
temporarily moved to the fork branch of awslabs/s2n-bignum#421 until it
lands on main.

Signed-off-by: Jake Massimo <jakemas@amazon.com>
@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.

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 left review comments
@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 DO-NOT-MERGE

Projects

None yet

Milestone

No milestone

4 participants

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