Skip to content

Enforce ML-DSA x86 native assumptions#1244

Open
tob-joe wants to merge 2 commits into
mainfrom
ptp/mldsa-enforce-x86-native-assumptions
Open

Enforce ML-DSA x86 native assumptions#1244
tob-joe wants to merge 2 commits into
mainfrom
ptp/mldsa-enforce-x86-native-assumptions

Conversation

@tob-joe

@tob-joe tob-joe commented Jun 29, 2026

Copy link
Copy Markdown

Enforce ML-DSA x86 native assumptions

Summary

  • Add assembler-time guards that fail the AVX2 NTT/INTT assembly build if the qdata table offsets drift away from the hard-coded displacements.
  • Strengthen the native API, dev-source declarations, and generated x86 implementation contracts for AVX2 polynomial routines that require 32-byte-aligned polynomial buffers.
  • Keep the public native wrapper contracts, implementation declarations, and proof-facing assumptions aligned for poly_caddq, poly_use_hint, and polyz_unpack.

Why

The x86_64 NTT/INTT assembly uses fixed qdata displacements after simplification. The dev source includes the symbolic layout, but the checked-in simplified assembly has numeric offsets; the new assembler guards make a future qdata layout mismatch fail at build time instead of silently preserving stale displacements.

Several AVX2 polynomial routines also use aligned loads or stores, and the HOL/CBMC proof assumptions already model aligned polynomial buffers. The in-tree typed callers pass mld_poly storage, which is declared with the project alignment attribute; this patch makes that precondition explicit at the native API and raw x86 contract boundary.

Verification

  • ./scripts/tests cbmc -kl ALL -p poly_use_hint_native --single-step -j1
  • ./scripts/tests cbmc -kl ALL -p poly_caddq_native_x86_64 --single-step -j1
  • ./scripts/tests cbmc -kl 44 -p polyz_unpack_native_x86_64 --single-step -j1
  • ./scripts/tests cbmc -kl 65 -p polyz_unpack_native_x86_64 --single-step -j1
  • ./scripts/tests cbmc -kl 87 -p polyz_unpack_native_x86_64 --single-step -j1
  • ./scripts/tests cbmc -kl ALL -p polyz_unpack_native --single-step -j1

Co-authored-by: Codex [email protected]
Signed-off-by: Joe Doyle [email protected]

This work was completed by Trail of Bits as part of the Patch The Planet project in collaboration with OpenAI. The issue was identified primarily by the Codex coding agent, and manually reviewed before submission.

@tob-joe tob-joe requested a review from a team as a code owner June 29, 2026 21:59
mkannwischer
mkannwischer reviewed Jun 30, 2026
View reviewed changes
Comment thread dev/x86_64/src/arith_native_x86_64.h
* in proofs/hol_light/x86_64/proofs/poly_caddq_avx2_asm.ml */
__contract__(
requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
requires(((uintptr_t)r % MLD_DEFAULT_ALIGN) == 0)

@mkannwischer mkannwischer Jun 30, 2026

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.

Unfortunately, this doesn't work. There is no way to guarantee alignment with CBMC iirc.

@mkannwischer

mkannwischer commented Jun 30, 2026

Copy link
Copy Markdown
Contributor

As far as I know, there is no way to model an alignment precondition in CBMC.

Maybe we can consider not using uint32_t * for the native APIs, but instead something that guarantees alignment via MLD_ALIGN. It still won't be formally proven, but we can rely on the compiler to yell at us if we try to change the frontend in a way that breaks alignment for the backend.

@oqs-bot

oqs-bot commented Jun 30, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-44)

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

@oqs-bot

oqs-bot commented Jun 30, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

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

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

@oqs-bot

oqs-bot commented Jun 30, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

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

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

@oqs-bot

oqs-bot commented Jun 30, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

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

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

@oqs-bot

oqs-bot commented Jun 30, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-65)

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

@oqs-bot

oqs-bot commented Jun 30, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-87)

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

@tob-joe tob-joe force-pushed the ptp/mldsa-enforce-x86-native-assumptions branch from 2848b20 to 81fab1d Compare July 5, 2026 23:59
tob-joe and others added 2 commits July 7, 2026 17:18
@tob-joe @codex
Enforce ML-DSA x86 native assumptions
76ced79 
Add assembly-time guards for AVX2 qdata offsets and make the x86 native entry contracts require the alignment assumed by the assembly implementations.

This keeps the public native wrappers, implementation declarations, and proof-facing assumptions aligned for the affected x86 routines.

Verification:
- ./scripts/tests cbmc -kl ALL -p poly_use_hint_native --single-step -j1
- ./scripts/tests cbmc -kl ALL -p poly_caddq_native_x86_64 --single-step -j1
- ./scripts/tests cbmc -kl 44 -p polyz_unpack_native_x86_64 --single-step -j1
- ./scripts/tests cbmc -kl 65 -p polyz_unpack_native_x86_64 --single-step -j1
- ./scripts/tests cbmc -kl 87 -p polyz_unpack_native_x86_64 --single-step -j1
- ./scripts/tests cbmc -kl ALL -p polyz_unpack_native --single-step -j1

Co-authored-by: Codex <[email protected]>
Signed-off-by: Joe Doyle <[email protected]>
@tob-joe @codex
Fix ML-DSA x86 qdata guard autogen
fe9c7ce 
Move the AVX2 qdata layout assertions out of the simpasm header region. The assertions still check the dev assembly source against consts.h, but simpasm no longer carries them into the generated assembly it reassembles without that macro context.

Regenerate the affected x86_64 native and HOL-Light assembly copies so lint and the x86_64 Intel-syntax autogen job can run past assembly generation.

Co-authored-by: Codex <[email protected]>
Signed-off-by: Joe Doyle <[email protected]>
@tob-joe tob-joe force-pushed the ptp/mldsa-enforce-x86-native-assumptions branch from 81fab1d to fe9c7ce Compare July 7, 2026 21:30
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@mkannwischer mkannwischer mkannwischer left review comments

At least 1 approving review is required to merge this pull request.

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@tob-joe @mkannwischer @oqs-bot