Skip to content

HOL-Light: Consolidate AArch64 poly_use_hint_32 _CORRECT theorems#1136

Open
jakemas wants to merge 1 commit into
mainfrom
consolidate-poly-use-hint-32
Open

HOL-Light: Consolidate AArch64 poly_use_hint_32 _CORRECT theorems#1136
jakemas wants to merge 1 commit into
mainfrom
consolidate-poly-use-hint-32

Conversation

@jakemas
Copy link
Copy Markdown
Contributor

@jakemas jakemas commented May 29, 2026 •
edited
Loading

Summary

Consolidates the poly_use_hint_32 AArch64 HOL-Light proofs to use the same _CORRECT / _SUBROUTINE_CORRECT shape as every other proof in the codebase, addressing #1085.

The _CORRECT_CODE / _CORRECT_BOUND_CODE / _SUBROUTINE_CORRECT_CODE intermediates are removed; the public _CORRECT is now stated directly in FIPS 204 terms (mldsa_use_hint_32) with the < 16 bound as a corollary, following the pattern outlined in #1037 (comment):

  • The FIPS 204 / code-aligned equivalence section (MLDSA_USE_HINT_32_EQUIV) moves above the correctness proof.
  • _CORRECT uses ENSURES_STRENGTHEN_POST to bridge the FIPS-aligned postcondition to the code-aligned form before symbolic execution; the strengthening branch closes via IMP_REWRITE_TAC[MLDSA_USE_HINT_32_EQUIV] and a short bound discharge.
  • _SUBROUTINE_CORRECT derives directly from _CORRECT via ARM_ADD_RETURN_NOSTACK_TAC.

The _88 variant will follow in a separate PR.

Validated end-to-end against the equivalent file in s2n-bignum (arm/proofs/mldsa_poly_use_hint_32.ml), where the same refactor proves in 25:10 wall time.

Closes part of #1085. If we are happy with _32 I can make the same changes to _88

Test plan

  • CI: AArch64 HOL Light proof for poly_use_hint_32_aarch64_asm.S passes
  • Public theorems POLY_USE_HINT_32_AARCH64_ASM_SUBROUTINE_CORRECT and POLY_USE_HINT_32_AARCH64_ASM_SUBROUTINE_SAFE retain identical signatures (verified locally)

@jakemas jakemas requested a review from a team as a code owner May 29, 2026 20:19
@jakemas jakemas marked this pull request as draft May 29, 2026 20:19
@jakemas jakemas force-pushed the consolidate-poly-use-hint-32 branch from c078a93 to 843eb2d Compare May 29, 2026 20:21
@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented May 29, 2026 •
edited
Loading

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

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

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented May 29, 2026 •
edited
Loading

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

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

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented May 29, 2026 •
edited
Loading

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

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

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented May 29, 2026 •
edited
Loading

CBMC Results (ML-DSA-87)

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

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented May 29, 2026 •
edited
Loading

CBMC Results (ML-DSA-44)

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

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented May 29, 2026 •
edited
Loading

CBMC Results (ML-DSA-65)

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

@jakemas jakemas marked this pull request as ready for review May 29, 2026 21:07
@jakemas
HOL-Light: Consolidate AArch64 poly_use_hint_32 _CORRECT theorems
ba270a2 
Per #1085, the poly_use_hint proofs from #1037 expose a non-standard
_CORRECT / _CORRECT_CODE split that doesn't appear in any other proof
in mlkem-native or mldsa-native.

This consolidates poly_use_hint_32 into a single FIPS 204-aligned
_CORRECT theorem and a single _SUBROUTINE_CORRECT, matching the
convention used by every other proof in the codebase. Internal
intermediates _CORRECT_CODE, _CORRECT_BOUND_CODE, and
_SUBROUTINE_CORRECT_CODE are removed.

The new _CORRECT places the input-bound antecedents
(val(x i) < 8380417 /\ val(y i) <= 1) inside the postcondition
(decompose-style), matching the shape used by poly_decompose_32 /
poly_decompose_88. The ARM symbolic execution doesn't depend on
input ranges; the bounds are picked up after stepping to discharge
the FIPS-equivalence and val < 16 corollary.

Mechanics:
  - The FIPS 204 / code-aligned equivalence section
    (MLDSA_USE_HINT_32_EQUIV) moves above the correctness proof.
  - _CORRECT runs the 878-step ARM symbolic execution unconditionally,
    then picks up the bound antecedents from the postcondition.
  - Per-element FIPS-equality closed via a derived EC_FINAL helper
    after IMP_REWRITE_TAC[MLDSA_USE_HINT_32_EQUIV].
  - val < 16 corollary closed by reducing val(word ..) to MOD via
    VAL_WORD and discharging via the bound on mldsa_use_hint_32_code.
  - _SUBROUTINE_CORRECT derives from _CORRECT via
    ARM_ADD_RETURN_NOSTACK_TAC.

The _88 variant will follow in a separate PR.

Verified end-to-end: the new proof closes in 19:01 wall time, exit 0,
no axioms.

Closes part of #1085.

Signed-off-by: Jake Massimo <jakemas@amazon.com>
@jakemas jakemas force-pushed the consolidate-poly-use-hint-32 branch from 843eb2d to ba270a2 Compare May 30, 2026 02:50
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@jakemas @oqs-bot