Skip to content

CI: Add merge queue support#1264

Merged
mkannwischer merged 2 commits into
mainfrom
mjk/merge-queue
Jul 3, 2026
Merged

CI: Add merge queue support#1264
mkannwischer merged 2 commits into
mainfrom
mjk/merge-queue

Conversation

@mkannwischer

@mkannwischer mkannwischer commented Jul 2, 2026

Copy link
Copy Markdown
Contributor

Run CI on merge_group events and add a "CI Summary" gate job intended as the single required status check. Add a workflow reporting the "DCO" check on merge groups since the DCO app does not support them (dcoapp/app#199); DCO is still enforced on the PR before it can enter the queue. Also run the HOL-Light proofs (self-gated by their changed-files check) and the legacy compiler tests on merge groups.

@oqs-bot

oqs-bot commented Jul 2, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

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

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

@oqs-bot

oqs-bot commented Jul 2, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-44)

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

@oqs-bot

oqs-bot commented Jul 2, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

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

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

@oqs-bot

oqs-bot commented Jul 2, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

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

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

@oqs-bot

oqs-bot commented Jul 2, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-65)

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

@oqs-bot

oqs-bot commented Jul 2, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-87)

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

@mkannwischer mkannwischer marked this pull request as ready for review July 3, 2026 01:33
@mkannwischer mkannwischer requested a review from a team as a code owner July 3, 2026 01:33
hanno-becker
hanno-becker approved these changes Jul 3, 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.

Let's try it.

@mkannwischer mkannwischer added this pull request to the merge queue Jul 3, 2026
@mkannwischer mkannwischer removed this pull request from the merge queue due to a manual request Jul 3, 2026
@mkannwischer mkannwischer force-pushed the mjk/merge-queue branch 2 times, most recently from 8f18ea5 to 88a4afe Compare July 3, 2026 04:14
@mkannwischer mkannwischer added this pull request to the merge queue Jul 3, 2026
@mkannwischer mkannwischer removed this pull request from the merge queue due to a manual request Jul 3, 2026
@mkannwischer
CI: Add merge queue support
4e3c1e7 
Run CI on merge_group events and add a "CI Summary" gate job intended
as the single required status check. Add a workflow reporting the
"DCO" check on merge groups since the DCO app does not support them
(dcoapp/app#199); DCO is still enforced on the PR before it can enter
the queue. Also run the HOL-Light proofs (self-gated by their
changed-files check) and the legacy compiler tests on merge groups.

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
@mkannwischer
CI: Do not run on pushes to main
5164e63 
All merges go through the merge queue, which already tested the
identical commit on the merge group branch. The nix caches can only be
refreshed from main, so a dedicated workflow keeps running there.

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
@mkannwischer mkannwischer added this pull request to the merge queue Jul 3, 2026
@mkannwischer mkannwischer removed this pull request from the merge queue due to a manual request Jul 3, 2026
@mkannwischer mkannwischer added this pull request to the merge queue Jul 3, 2026
Merged via the queue into main with commit 529a89d Jul 3, 2026
422 checks passed
@mkannwischer mkannwischer deleted the mjk/merge-queue branch July 3, 2026 07:57
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

Assignees

No one assigned

Labels

needs-mlkem-native-port

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@mkannwischer @oqs-bot @hanno-becker