Skip to content

HOL-Light: Add HOL Light proof and CBMC contracts for x86 poly_caddq#1068

Draft
jakemas wants to merge 7 commits intomainfrom
x86-poly-caddq-hol-light
Draft

HOL-Light: Add HOL Light proof and CBMC contracts for x86 poly_caddq#1068
jakemas wants to merge 7 commits intomainfrom
x86-poly-caddq-hol-light

Conversation

@jakemas
Copy link
Copy Markdown
Contributor

@jakemas jakemas commented Apr 28, 2026 •
edited
Loading

Resolves #492

Summary

  • Port x86 AVX2 poly_caddq HOL Light formal proof from s2n-bignum (awslabs/s2n-bignum#398)
  • Add CBMC contract for mld_poly_caddq_avx2 and new poly_caddq_native_x86_64 CBMC proof
  • Fix MAP_UNTIL_TARGET_PC in x86_64 mldsa_utils.ml (was matching eventually arm instead of eventually x86)

Details

The HOL Light proof verifies that for each coefficient with |ival(x)| < Q, the output satisfies ival(output) = ival(x) rem Q. The proof is adapted for mldsa-native's looped assembly (8 iterations of 4 AVX2 vectors) vs s2n-bignum's fully unrolled version, using MAP_UNTIL_TARGET_PC for loop handling.

Depends on: s2n-bignum #397 (VPCMPGTD instruction model)

@jakemas
x86: Add HOL Light proof and CBMC contracts for poly_caddq
a21d952 
Port the x86 AVX2 poly_caddq formal verification from s2n-bignum
(awslabs/s2n-bignum#398) to mldsa-native. The proof verifies that for
inputs with |ival(x)| < Q, the output satisfies ival(output) = ival(x) rem Q.

Adapted for mldsa-native's looped assembly (8 iterations of 4 vectors)
vs s2n-bignum's fully unrolled version, using MAP_UNTIL_TARGET_PC for
loop handling.

Also adds CBMC contract for mld_poly_caddq_avx2 and a new x86_64 CBMC
proof (poly_caddq_native_x86_64), plus a fix for MAP_UNTIL_TARGET_PC
in x86_64 mldsa_utils.ml (was matching `eventually arm` instead of
`eventually x86`).

Depends on s2n-bignum PR #397 (VPCMPGTD instruction model).

Signed-off-by: Jake Massimo <jakemas@amazon.com>
@jakemas jakemas requested a review from a team as a code owner April 28, 2026 18:53
jakemas added 2 commits April 28, 2026 18:59
@jakemas
nix: Bump s2n-bignum to include VPCMPGTD instruction model
bb50a9d 
Point s2n-bignum at awslabs/s2n-bignum#398 branch which includes
the VPCMPGTD/VPCMPGTW instruction models needed for the x86
poly_caddq HOL Light proof.

Signed-off-by: Jake Massimo <jakemas@amazon.com>
@jakemas
autogen: Update BIBLIOGRAPHY.md for poly_caddq
b9894f5 
Signed-off-by: Jake Massimo <jakemas@amazon.com>
@jakemas jakemas marked this pull request as draft April 28, 2026 19:04
@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Apr 28, 2026 •
edited
Loading

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

Full Results (195 proofs)
Proof Status Current Previous Change
**TOTAL** ✅ 1614s 1715s -5.9%
sign_verify_internal ✅ 121s 129s -6%
poly_pointwise_montgomery_c ✅ 111s 124s -10%
rej_uniform_native ✅ 108s 111s -3%
mld_invntt_layer ✅ 103s 114s -10%
polyvec_matrix_pointwise_montgomery ✅ 91s 98s -7%
mld_ct_memcmp ✅ 76s 80s -5%
polyvec_matrix_pointwise_montgomery_yvec ✅ 70s 74s -5%
mld_ntt_layer ✅ 44s 47s -6%
fqmul ✅ 28s 29s -3%
mld_attempt_signature_generation ✅ 26s 31s -16%
sign_keypair_internal ✅ 25s 25s +0%
keccakf1600x4_permute_native ✅ 23s 22s +5%
polyveck_decompose ✅ 20s 20s +0%
sign_pk_from_sk ✅ 19s 19s +0%
mld_ntt_butterfly_block ✅ 17s 17s +0%
poly_chknorm_c ✅ 14s 16s -12%
polyt0_unpack ✅ 14s 16s -12%
polyveck_power2round ✅ 14s 15s -7%
poly_add ✅ 13s 12s +8%
poly_uniform_eta_4x ✅ 13s 12s +8%
polyvecl_chknorm ✅ 13s 14s -7%
polyveck_add ✅ 12s 12s +0%
keccak_absorb_once_x4 ✅ 10s 9s +11%
mld_check_pct ✅ 10s 8s +25%
poly_invntt_tomont_c ✅ 10s 9s +11%
rej_uniform ✅ 9s 9s +0%
keccakf1600_permute_native ✅ 8s 6s +33%
poly_caddq_c ✅ 8s 8s +0%
polyveck_invntt_tomont ✅ 8s 6s +33%
polyveck_ntt ✅ 8s 9s -11%
polyveck_pointwise_poly_montgomery ✅ 8s 9s -11%
polyveck_reduce ✅ 8s 7s +14%
polyveck_sub ✅ 8s 6s +33%
polyveck_use_hint ✅ 8s 8s +0%
sign ✅ 8s 7s +14%
keccak_absorb ✅ 7s 7s +0%
keccakf1600_permute ✅ 7s 7s +0%
polyeta_unpack ✅ 7s 6s +17%
polyveck_pack_eta ✅ 7s 2s +250%
rej_uniform_c ✅ 7s 9s -22%
sign_signature_extmu ✅ 7s 7s +0%
mld_compute_pack_z ✅ 6s 7s -14%
poly_shiftl ✅ 6s 6s +0%
poly_uniform_eta ✅ 6s 5s +20%
polyvecl_ntt ✅ 6s 9s -33%
sign_open ✅ 6s 5s +20%
sign_signature_internal ✅ 6s 7s -14%
sign_verify_extmu ✅ 6s 4s +50%
keccak_squeezeblocks_x4 ✅ 5s 3s +67%
make_hint ✅ 5s 2s +150%
mld_ct_sel_int32 ✅ 5s 1s +400%
pointwise_acc_native_aarch64 ✅ 5s 7s -29%
pointwise_acc_native_x86_64 ✅ 5s 6s -17%
poly_caddq_native_aarch64 ✅ 5s 4s +25%
poly_challenge ✅ 5s 3s +67%
poly_ntt_native ✅ 5s 4s +25%
poly_permute_bitrev_to_custom_optional ✅ 5s 3s +67%
poly_uniform ✅ 5s 5s +0%
polyveck_pack_t0 ✅ 5s 4s +25%
polyveck_shiftl ✅ 5s 6s -17%
polyveck_unpack_t0 ✅ 5s 3s +67%
shake256x4_absorb_once ✅ 5s 4s +25%
sign_verify_pre_hash_shake256 ✅ 5s 4s +25%
sk_t0hat_get_poly ✅ 5s 5s +0%
unpack_hints ✅ 5s 7s -29%
intt_native_x86_64 ✅ 4s 4s +0%
keccakf1600_extract_bytes (big endian) ✅ 4s 3s +33%
keccakf1600x4_extract_bytes ✅ 4s 4s +0%
mld_ct_cmask_nonzero_u32 ✅ 4s 4s +0%
mld_h ✅ 4s 4s +0%
mld_prepare_domain_separation_prefix ✅ 4s 3s +33%
mld_sample_s1_s2 ✅ 4s 4s +0%
mld_sample_s1_s2_serial ✅ 4s 5s -20%
mld_value_barrier_u8 ✅ 4s 5s -20%
pack_pk ✅ 4s 3s +33%
poly_decompose ✅ 4s 3s +33%
poly_invntt_tomont_native ✅ 4s 6s -33%
poly_ntt_c ✅ 4s 5s -20%
poly_uniform_4x ✅ 4s 4s +0%
poly_use_hint ✅ 4s 5s -20%
polyt0_pack ✅ 4s 2s +100%
polyvec_matrix_expand_serial ✅ 4s 2s +100%
polyveck_caddq ✅ 4s 7s -43%
polyveck_chknorm ✅ 4s 5s -20%
polyvecl_uniform_gamma1_serial ✅ 4s 3s +33%
polyvecl_unpack_z ✅ 4s 4s +0%
reduce32 ✅ 4s 4s +0%
rej_eta ✅ 4s 3s +33%
rej_eta_c ✅ 4s 3s +33%
rej_eta_native ✅ 4s 3s +33%
sign_keypair ✅ 4s 4s +0%
sign_signature_pre_hash_internal ✅ 4s 6s -33%
sign_signature_pre_hash_shake256 ✅ 4s 6s -33%
sign_verify_pre_hash_internal ✅ 4s 6s -33%
caddq ✅ 3s 4s -25%
fqscale ✅ 3s 2s +50%
keccak_f1600_x1_native_aarch64 ✅ 3s 3s +0%
keccak_f1600_x4_native_aarch64_v84a ✅ 3s 3s +0%
keccak_squeeze ✅ 3s 2s +50%
keccakf1600_xor_bytes (big endian) ✅ 3s 4s -25%
keccakf1600x4_permute ✅ 3s 3s +0%
mld_ct_cmask_nonzero_u8 ✅ 3s 6s -50%
mld_ct_get_optblocker_u32 ✅ 3s 2s +50%
mld_keccakf1600_extract_bytes ✅ 3s 2s +50%
mld_polymat_expand_entry ✅ 3s 2s +50%
mld_value_barrier_u32 ✅ 3s 3s +0%
montgomery_reduce ✅ 3s 4s -25%
nttunpack_native_x86_64 ✅ 3s 3s +0%
pack_sig_c ✅ 3s 2s +50%
pack_sig_h_poly ✅ 3s 4s -25%
pack_sk_s1 ✅ 3s 3s +0%
pointwise_native_aarch64 ✅ 3s 2s +50%
poly_caddq_native ✅ 3s 2s +50%
poly_decompose_c ✅ 3s 5s -40%
poly_decompose_native ✅ 3s 2s +50%
poly_pointwise_montgomery ✅ 3s 3s +0%
poly_reduce ✅ 3s 3s +0%
poly_sub ✅ 3s 2s +50%
poly_uniform_gamma1 ✅ 3s 3s +0%
poly_use_hint_c ✅ 3s 3s +0%
poly_use_hint_native ✅ 3s 3s +0%
polyeta_pack ✅ 3s 4s -25%
polyveck_pack_w1 ✅ 3s 4s -25%
polyvecl_pack_eta ✅ 3s 4s -25%
polyvecl_pointwise_acc_montgomery ✅ 3s 3s +0%
polyvecl_uniform_gamma1 ✅ 3s 2s +50%
polyvecl_unpack_eta ✅ 3s 2s +50%
polyz_unpack ✅ 3s 3s +0%
polyz_unpack_c ✅ 3s 5s -40%
polyz_unpack_native ✅ 3s 2s +50%
power2round ✅ 3s 3s +0%
shake128_absorb ✅ 3s 2s +50%
shake128_release ✅ 3s 4s -25%
shake128x4_absorb_once ✅ 3s 2s +50%
shake256_absorb ✅ 3s 3s +0%
shake256_init ✅ 3s 2s +50%
shake256_squeeze ✅ 3s 3s +0%
sk_s1hat_get_poly ✅ 3s 2s +50%
sys_check_capability ✅ 3s 3s +0%
unpack_pk ✅ 3s 3s +0%
unpack_sk ✅ 3s 3s +0%
unpack_sk_s1hat ✅ 3s 3s +0%
unpack_sk_t0hat ✅ 3s 2s +50%
use_hint ✅ 3s 3s +0%
decompose ✅ 2s 1s +100%
keccak_f1600_x1_native_aarch64_v84a ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid ✅ 2s 4s -50%
keccak_finalize ✅ 2s 2s +0%
keccakf1600_xor_bytes ✅ 2s 2s +0%
keccakf1600x4_xor_bytes ✅ 2s 1s +100%
mld_ct_abs_i32 ✅ 2s 2s +0%
mld_ct_cmask_neg_i32 ✅ 2s 3s -33%
mld_ct_get_optblocker_i64 ✅ 2s 3s -33%
mld_value_barrier_i64 ✅ 2s 4s -50%
ntt_native_x86_64 ✅ 2s 2s +0%
pack_sig_z ✅ 2s 2s +0%
pack_sk_rho_key_tr_s2_t0 ✅ 2s 3s -33%
pointwise_native_x86_64 ✅ 2s 3s -33%
poly_caddq ✅ 2s 4s -50%
poly_chknorm ✅ 2s 4s -50%
poly_chknorm_native ✅ 2s 3s -33%
poly_chknorm_native_aarch64 ✅ 2s 4s -50%
poly_invntt_tomont ✅ 2s 3s -33%
poly_make_hint ✅ 2s 2s +0%
poly_ntt ✅ 2s 3s -33%
poly_permute_bitrev_to_custom_optional_native ✅ 2s 4s -50%
poly_power2round ✅ 2s 5s -60%
poly_uniform_gamma1_4x ✅ 2s 3s -33%
polyt1_pack ✅ 2s 5s -60%
polyt1_unpack ✅ 2s 3s -33%
polyvec_matrix_expand ✅ 2s 3s -33%
polyveck_unpack_eta ✅ 2s 4s -50%
polyvecl_pointwise_acc_montgomery_c ✅ 2s 4s -50%
polyvecl_pointwise_acc_montgomery_native ✅ 2s 4s -50%
polyz_pack ✅ 2s 2s +0%
shake128_init ✅ 2s 5s -60%
shake128_squeeze ✅ 2s 3s -33%
shake256 ✅ 2s 2s +0%
shake256_finalize ✅ 2s 5s -60%
shake256x4_squeezeblocks ✅ 2s 4s -50%
sign_signature ✅ 2s 5s -60%
sign_verify ✅ 2s 6s -67%
sk_s2hat_get_poly ✅ 2s 2s +0%
unpack_sig ✅ 2s 3s -33%
unpack_sk_s2hat ✅ 2s 4s -50%
keccak_init ✅ 1s 2s -50%
mld_ct_get_optblocker_u8 ✅ 1s 4s -75%
ntt_native_aarch64 ✅ 1s 3s -67%
poly_caddq_native_x86_64 ✅ 1s - new
poly_pointwise_montgomery_native ✅ 1s 3s -67%
polyw1_pack ✅ 1s 3s -67%
shake128_finalize ✅ 1s 2s -50%
shake128x4_squeezeblocks ✅ 1s 3s -67%
shake256_release ✅ 1s 2s -50%

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Apr 28, 2026 •
edited
Loading

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

Full Results (195 proofs)
Proof Status Current Previous Change
**TOTAL** ✅ 1497s 1470s +1.8%
rej_uniform_native ✅ 109s 108s +1%
poly_pointwise_montgomery_c ✅ 105s 104s +1%
sign_verify_internal ✅ 105s 101s +4%
mld_invntt_layer ✅ 102s 98s +4%
mld_ct_memcmp ✅ 71s 75s -5%
polyvec_matrix_pointwise_montgomery_yvec ✅ 64s 67s -4%
polyvec_matrix_pointwise_montgomery ✅ 50s 48s +4%
mld_ntt_layer ✅ 43s 41s +5%
fqmul ✅ 28s 26s +8%
keccakf1600x4_permute_native ✅ 23s 21s +10%
polyvecl_chknorm ✅ 23s 20s +15%
polyveck_power2round ✅ 22s 21s +5%
mld_attempt_signature_generation ✅ 20s 20s +0%
polyeta_unpack ✅ 18s 17s +6%
poly_chknorm_c ✅ 15s 15s +0%
polyt0_unpack ✅ 14s 15s -7%
sign_keypair_internal ✅ 14s 12s +17%
mld_check_pct ✅ 13s 12s +8%
mld_ntt_butterfly_block ✅ 13s 15s -13%
poly_uniform_eta_4x ✅ 12s 13s -8%
polyz_unpack_c ✅ 12s 10s +20%
keccak_absorb_once_x4 ✅ 10s 8s +25%
poly_add ✅ 10s 12s -17%
poly_caddq_c ✅ 10s 7s +43%
sign_pk_from_sk ✅ 10s 12s -17%
mld_prepare_domain_separation_prefix ✅ 9s 4s +125%
polyveck_decompose ✅ 9s 7s +29%
rej_uniform_c ✅ 9s 7s +29%
keccakf1600_permute ✅ 8s 7s +14%
poly_decompose_c ✅ 8s 7s +14%
polyvecl_ntt ✅ 8s 5s +60%
rej_uniform ✅ 8s 7s +14%
keccak_absorb ✅ 7s 6s +17%
poly_invntt_tomont_c ✅ 7s 8s -12%
poly_shiftl ✅ 7s 7s +0%
keccakf1600_permute_native ✅ 6s 8s -25%
pointwise_acc_native_aarch64 ✅ 6s 4s +50%
polyt0_pack ✅ 6s 3s +100%
polyveck_add ✅ 6s 8s -25%
polyveck_invntt_tomont ✅ 6s 4s +50%
polyvecl_uniform_gamma1 ✅ 6s 2s +200%
sign ✅ 6s 6s +0%
sign_verify_pre_hash_shake256 ✅ 6s 2s +200%
keccakf1600_extract_bytes (big endian) ✅ 5s 3s +67%
keccakf1600x4_xor_bytes ✅ 5s 3s +67%
mld_ct_get_optblocker_u8 ✅ 5s 4s +25%
pack_sig_h_poly ✅ 5s 6s -17%
poly_challenge ✅ 5s 4s +25%
poly_chknorm ✅ 5s 5s +0%
poly_permute_bitrev_to_custom_optional_native ✅ 5s 4s +25%
poly_pointwise_montgomery_native ✅ 5s 3s +67%
poly_uniform_eta ✅ 5s 4s +25%
polyveck_reduce ✅ 5s 5s +0%
polyveck_unpack_t0 ✅ 5s 3s +67%
polyz_unpack ✅ 5s 4s +25%
shake128_finalize ✅ 5s 4s +25%
sign_signature_internal ✅ 5s 4s +25%
sign_signature_pre_hash_internal ✅ 5s 3s +67%
sk_t0hat_get_poly ✅ 5s 2s +150%
keccak_init ✅ 4s 2s +100%
keccakf1600_xor_bytes ✅ 4s 2s +100%
mld_compute_pack_z ✅ 4s 6s -33%
mld_ct_cmask_neg_i32 ✅ 4s 2s +100%
ntt_native_x86_64 ✅ 4s 4s +0%
nttunpack_native_x86_64 ✅ 4s 5s -20%
pointwise_acc_native_x86_64 ✅ 4s 7s -43%
poly_permute_bitrev_to_custom_optional ✅ 4s 4s +0%
poly_reduce ✅ 4s 3s +33%
poly_sub ✅ 4s 3s +33%
poly_uniform_gamma1 ✅ 4s 2s +100%
poly_use_hint ✅ 4s 2s +100%
poly_use_hint_c ✅ 4s 6s -33%
poly_use_hint_native ✅ 4s 4s +0%
polyt1_pack ✅ 4s 3s +33%
polyt1_unpack ✅ 4s 5s -20%
polyveck_caddq ✅ 4s 3s +33%
polyveck_chknorm ✅ 4s 4s +0%
polyveck_ntt ✅ 4s 7s -43%
polyveck_pack_eta ✅ 4s 4s +0%
polyveck_shiftl ✅ 4s 5s -20%
polyveck_sub ✅ 4s 5s -20%
polyveck_use_hint ✅ 4s 2s +100%
polyz_unpack_native ✅ 4s 3s +33%
power2round ✅ 4s 1s +300%
rej_eta_c ✅ 4s 5s -20%
shake256_finalize ✅ 4s 2s +100%
sign_signature ✅ 4s 3s +33%
sign_signature_pre_hash_shake256 ✅ 4s 4s +0%
sign_verify_pre_hash_internal ✅ 4s 6s -33%
unpack_sk_s2hat ✅ 4s 2s +100%
caddq ✅ 3s 1s +200%
decompose ✅ 3s 3s +0%
fqscale ✅ 3s 3s +0%
keccak_f1600_x1_native_aarch64 ✅ 3s 3s +0%
keccak_f1600_x4_native_aarch64_v84a ✅ 3s 2s +50%
keccak_squeeze ✅ 3s 2s +50%
keccak_squeezeblocks_x4 ✅ 3s 6s -50%
make_hint ✅ 3s 1s +200%
mld_ct_cmask_nonzero_u8 ✅ 3s 3s +0%
mld_h ✅ 3s 6s -50%
mld_sample_s1_s2 ✅ 3s 3s +0%
mld_sample_s1_s2_serial ✅ 3s 3s +0%
pack_pk ✅ 3s 4s -25%
pack_sig_z ✅ 3s 2s +50%
pack_sk_s1 ✅ 3s 3s +0%
pointwise_native_x86_64 ✅ 3s 3s +0%
poly_chknorm_native ✅ 3s 3s +0%
poly_decompose ✅ 3s 2s +50%
poly_decompose_native ✅ 3s 4s -25%
poly_invntt_tomont ✅ 3s 2s +50%
poly_make_hint ✅ 3s 2s +50%
poly_ntt_native ✅ 3s 3s +0%
poly_uniform ✅ 3s 5s -40%
poly_uniform_4x ✅ 3s 4s -25%
poly_uniform_gamma1_4x ✅ 3s 3s +0%
polyvec_matrix_expand_serial ✅ 3s 3s +0%
polyveck_pointwise_poly_montgomery ✅ 3s 3s +0%
polyveck_unpack_eta ✅ 3s 2s +50%
polyvecl_pointwise_acc_montgomery ✅ 3s 2s +50%
polyvecl_pointwise_acc_montgomery_c ✅ 3s 1s +200%
polyvecl_pointwise_acc_montgomery_native ✅ 3s 2s +50%
polyvecl_unpack_eta ✅ 3s 3s +0%
polyw1_pack ✅ 3s 3s +0%
reduce32 ✅ 3s 3s +0%
rej_eta_native ✅ 3s 3s +0%
shake128_squeeze ✅ 3s 3s +0%
shake128x4_absorb_once ✅ 3s 2s +50%
shake256_init ✅ 3s 2s +50%
shake256_release ✅ 3s 1s +200%
shake256_squeeze ✅ 3s 2s +50%
shake256x4_squeezeblocks ✅ 3s 2s +50%
sign_keypair ✅ 3s 3s +0%
sign_verify ✅ 3s 5s -40%
sign_verify_extmu ✅ 3s 3s +0%
sk_s1hat_get_poly ✅ 3s 3s +0%
sk_s2hat_get_poly ✅ 3s 5s -40%
sys_check_capability ✅ 3s 4s -25%
unpack_hints ✅ 3s 4s -25%
unpack_pk ✅ 3s 5s -40%
unpack_sk ✅ 3s 2s +50%
unpack_sk_t0hat ✅ 3s 4s -25%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid ✅ 2s 2s +0%
keccak_finalize ✅ 2s 2s +0%
keccakf1600_xor_bytes (big endian) ✅ 2s 2s +0%
keccakf1600x4_extract_bytes ✅ 2s 3s -33%
keccakf1600x4_permute ✅ 2s 2s +0%
mld_ct_abs_i32 ✅ 2s 1s +100%
mld_ct_cmask_nonzero_u32 ✅ 2s 3s -33%
mld_ct_get_optblocker_u32 ✅ 2s 2s +0%
mld_ct_sel_int32 ✅ 2s 1s +100%
mld_keccakf1600_extract_bytes ✅ 2s 2s +0%
mld_polymat_expand_entry ✅ 2s 2s +0%
mld_value_barrier_u8 ✅ 2s 3s -33%
montgomery_reduce ✅ 2s 4s -50%
ntt_native_aarch64 ✅ 2s 2s +0%
pack_sig_c ✅ 2s 4s -50%
pack_sk_rho_key_tr_s2_t0 ✅ 2s 4s -50%
pointwise_native_aarch64 ✅ 2s 3s -33%
poly_caddq ✅ 2s 2s +0%
poly_caddq_native ✅ 2s 2s +0%
poly_caddq_native_aarch64 ✅ 2s 2s +0%
poly_caddq_native_x86_64 ✅ 2s - new
poly_invntt_tomont_native ✅ 2s 2s +0%
poly_ntt ✅ 2s 2s +0%
poly_ntt_c ✅ 2s 1s +100%
poly_pointwise_montgomery ✅ 2s 4s -50%
poly_power2round ✅ 2s 3s -33%
polyeta_pack ✅ 2s 3s -33%
polyveck_pack_w1 ✅ 2s 3s -33%
polyvecl_pack_eta ✅ 2s 1s +100%
polyvecl_uniform_gamma1_serial ✅ 2s 4s -50%
polyvecl_unpack_z ✅ 2s 2s +0%
polyz_pack ✅ 2s 5s -60%
rej_eta ✅ 2s 2s +0%
shake128_absorb ✅ 2s 2s +0%
shake128_init ✅ 2s 2s +0%
shake128_release ✅ 2s 3s -33%
shake128x4_squeezeblocks ✅ 2s 2s +0%
shake256_absorb ✅ 2s 4s -50%
sign_open ✅ 2s 5s -60%
sign_signature_extmu ✅ 2s 4s -50%
unpack_sig ✅ 2s 4s -50%
use_hint ✅ 2s 2s +0%
intt_native_x86_64 ✅ 1s 4s -75%
keccak_f1600_x1_native_aarch64_v84a ✅ 1s 2s -50%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid ✅ 1s 2s -50%
mld_ct_get_optblocker_i64 ✅ 1s 1s +0%
mld_value_barrier_i64 ✅ 1s 4s -75%
mld_value_barrier_u32 ✅ 1s 3s -67%
poly_chknorm_native_aarch64 ✅ 1s 2s -50%
polyvec_matrix_expand ✅ 1s 3s -67%
polyveck_pack_t0 ✅ 1s 2s -50%
shake256 ✅ 1s 3s -67%
shake256x4_absorb_once ✅ 1s 4s -75%
unpack_sk_s1hat ✅ 1s 4s -75%

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Apr 28, 2026 •
edited
Loading

CBMC Results (ML-DSA-65)

Full Results (195 proofs)
Proof Status Current Previous Change
**TOTAL** ✅ 2082s 2024s +2.9%
polyvecl_pointwise_acc_montgomery_c ✅ 211s 210s +0%
sign_verify_internal ✅ 191s 193s -1%
polyvec_matrix_expand ✅ 135s 127s +6%
rej_uniform_native ✅ 129s 125s +3%
poly_pointwise_montgomery_c ✅ 117s 113s +4%
mld_invntt_layer ✅ 102s 98s +4%
mld_ct_memcmp ✅ 86s 81s +6%
mld_attempt_signature_generation ✅ 69s 69s +0%
mld_ntt_layer ✅ 45s 43s +5%
fqmul ✅ 31s 30s +3%
sign_keypair_internal ✅ 26s 27s -4%
keccakf1600x4_permute_native ✅ 24s 22s +9%
polyvec_matrix_expand_serial ✅ 24s 22s +9%
rej_uniform ✅ 24s 22s +9%
sign_pk_from_sk ✅ 24s 20s +20%
sign_signature_internal ✅ 22s 24s -8%
polyt0_unpack ✅ 21s 20s +5%
poly_chknorm_c ✅ 20s 17s +18%
mld_ntt_butterfly_block ✅ 18s 16s +12%
poly_uniform_eta_4x ✅ 18s 13s +38%
polyveck_power2round ✅ 16s 17s -6%
polyveck_decompose ✅ 14s 13s +8%
rej_uniform_c ✅ 14s 16s -12%
poly_add ✅ 13s 12s +8%
mld_compute_pack_z ✅ 12s 11s +9%
keccak_absorb_once_x4 ✅ 10s 11s -9%
polyveck_add ✅ 10s 9s +11%
polyveck_caddq ✅ 10s 8s +25%
polyveck_shiftl ✅ 10s 8s +25%
mld_check_pct ✅ 9s 10s -10%
poly_uniform_4x ✅ 9s 10s -10%
polyveck_ntt ✅ 9s 10s -10%
polyveck_use_hint ✅ 9s 10s -10%
keccak_absorb ✅ 8s 6s +33%
keccakf1600_permute ✅ 8s 7s +14%
poly_invntt_tomont_c ✅ 8s 9s -11%
polyveck_chknorm ✅ 8s 6s +33%
polyveck_pack_w1 ✅ 8s 2s +300%
polyveck_pointwise_poly_montgomery ✅ 8s 7s +14%
polyveck_sub ✅ 8s 5s +60%
polyvecl_chknorm ✅ 8s 10s -20%
sign_signature ✅ 8s 7s +14%
sign_verify_pre_hash_shake256 ✅ 8s 6s +33%
unpack_hints ✅ 8s 4s +100%
keccakf1600_permute_native ✅ 7s 7s +0%
pointwise_acc_native_x86_64 ✅ 7s 8s -12%
poly_uniform ✅ 7s 3s +133%
polyveck_reduce ✅ 7s 8s -12%
polyvecl_ntt ✅ 7s 7s +0%
polyz_unpack_c ✅ 7s 8s -12%
sign ✅ 7s 9s -22%
mld_sample_s1_s2 ✅ 6s 6s +0%
mld_sample_s1_s2_serial ✅ 6s 4s +50%
montgomery_reduce ✅ 6s 2s +200%
pointwise_acc_native_aarch64 ✅ 6s 6s +0%
poly_caddq_c ✅ 6s 4s +50%
poly_power2round ✅ 6s 8s -25%
poly_shiftl ✅ 6s 3s +100%
polyt1_pack ✅ 6s 3s +100%
polyvec_matrix_pointwise_montgomery_yvec ✅ 6s 4s +50%
sign_signature_pre_hash_internal ✅ 6s 4s +50%
sign_signature_pre_hash_shake256 ✅ 6s 4s +50%
caddq ✅ 5s 3s +67%
keccak_squeezeblocks_x4 ✅ 5s 7s -29%
pack_sig_h_poly ✅ 5s 5s +0%
pack_sk_rho_key_tr_s2_t0 ✅ 5s 2s +150%
poly_make_hint ✅ 5s 3s +67%
poly_uniform_gamma1_4x ✅ 5s 7s -29%
polyveck_invntt_tomont ✅ 5s 6s -17%
rej_eta_c ✅ 5s 2s +150%
rej_eta_native ✅ 5s 3s +67%
sk_s2hat_get_poly ✅ 5s 4s +25%
unpack_sk_t0hat ✅ 5s 3s +67%
fqscale ✅ 4s 1s +300%
intt_native_x86_64 ✅ 4s 3s +33%
ntt_native_aarch64 ✅ 4s 2s +100%
pack_sig_z ✅ 4s 3s +33%
poly_caddq ✅ 4s 5s -20%
poly_challenge ✅ 4s 5s -20%
poly_chknorm_native ✅ 4s 3s +33%
poly_chknorm_native_aarch64 ✅ 4s 4s +0%
poly_invntt_tomont_native ✅ 4s 4s +0%
poly_permute_bitrev_to_custom_optional ✅ 4s 3s +33%
poly_pointwise_montgomery_native ✅ 4s 3s +33%
poly_sub ✅ 4s 1s +300%
poly_uniform_eta ✅ 4s 4s +0%
poly_uniform_gamma1 ✅ 4s 3s +33%
polyeta_unpack ✅ 4s 6s -33%
polyveck_unpack_eta ✅ 4s 5s -20%
polyveck_unpack_t0 ✅ 4s 4s +0%
polyvecl_pack_eta ✅ 4s 3s +33%
polyvecl_pointwise_acc_montgomery_native ✅ 4s 3s +33%
power2round ✅ 4s 5s -20%
shake128_release ✅ 4s 1s +300%
shake256_finalize ✅ 4s 2s +100%
shake256_init ✅ 4s 4s +0%
shake256_release ✅ 4s 3s +33%
sign_keypair ✅ 4s 5s -20%
sign_signature_extmu ✅ 4s 3s +33%
sk_t0hat_get_poly ✅ 4s 3s +33%
sys_check_capability ✅ 4s 2s +100%
unpack_sk_s1hat ✅ 4s 3s +33%
decompose ✅ 3s 3s +0%
keccak_f1600_x1_native_aarch64 ✅ 3s 2s +50%
keccak_finalize ✅ 3s 4s -25%
keccakf1600_xor_bytes ✅ 3s 1s +200%
keccakf1600_xor_bytes (big endian) ✅ 3s 1s +200%
keccakf1600x4_extract_bytes ✅ 3s 2s +50%
keccakf1600x4_xor_bytes ✅ 3s 2s +50%
make_hint ✅ 3s 3s +0%
mld_ct_cmask_nonzero_u8 ✅ 3s 4s -25%
mld_ct_get_optblocker_i64 ✅ 3s 3s +0%
mld_h ✅ 3s 4s -25%
mld_keccakf1600_extract_bytes ✅ 3s 4s -25%
mld_polymat_expand_entry ✅ 3s 6s -50%
mld_prepare_domain_separation_prefix ✅ 3s 4s -25%
mld_value_barrier_u8 ✅ 3s 2s +50%
ntt_native_x86_64 ✅ 3s 3s +0%
pack_sig_c ✅ 3s 4s -25%
pack_sk_s1 ✅ 3s 2s +50%
pointwise_native_aarch64 ✅ 3s 4s -25%
pointwise_native_x86_64 ✅ 3s 2s +50%
poly_caddq_native_aarch64 ✅ 3s 3s +0%
poly_chknorm ✅ 3s 4s -25%
poly_decompose ✅ 3s 6s -50%
poly_decompose_c ✅ 3s 4s -25%
poly_decompose_native ✅ 3s 4s -25%
poly_ntt ✅ 3s 5s -40%
poly_permute_bitrev_to_custom_optional_native ✅ 3s 2s +50%
poly_use_hint ✅ 3s 3s +0%
poly_use_hint_native ✅ 3s 3s +0%
polyt0_pack ✅ 3s 5s -40%
polyvec_matrix_pointwise_montgomery ✅ 3s 4s -25%
polyveck_pack_t0 ✅ 3s 3s +0%
polyvecl_uniform_gamma1 ✅ 3s 4s -25%
polyvecl_unpack_z ✅ 3s 3s +0%
polyw1_pack ✅ 3s 5s -40%
polyz_pack ✅ 3s 2s +50%
polyz_unpack_native ✅ 3s 5s -40%
rej_eta ✅ 3s 4s -25%
shake128_init ✅ 3s 2s +50%
shake128_squeeze ✅ 3s 1s +200%
shake256_absorb ✅ 3s 2s +50%
shake256_squeeze ✅ 3s 3s +0%
sign_open ✅ 3s 5s -40%
sign_verify_extmu ✅ 3s 2s +50%
sign_verify_pre_hash_internal ✅ 3s 4s -25%
unpack_pk ✅ 3s 2s +50%
unpack_sig ✅ 3s 4s -25%
unpack_sk ✅ 3s 3s +0%
use_hint ✅ 3s 3s +0%
keccak_f1600_x1_native_aarch64_v84a ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v84a ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid ✅ 2s 4s -50%
keccakf1600_extract_bytes (big endian) ✅ 2s 2s +0%
keccakf1600x4_permute ✅ 2s 3s -33%
mld_ct_abs_i32 ✅ 2s 2s +0%
mld_ct_get_optblocker_u32 ✅ 2s 2s +0%
mld_ct_get_optblocker_u8 ✅ 2s 2s +0%
mld_value_barrier_i64 ✅ 2s 3s -33%
mld_value_barrier_u32 ✅ 2s 3s -33%
nttunpack_native_x86_64 ✅ 2s 2s +0%
poly_caddq_native ✅ 2s 4s -50%
poly_caddq_native_x86_64 ✅ 2s - new
poly_invntt_tomont ✅ 2s 2s +0%
poly_ntt_c ✅ 2s 3s -33%
poly_ntt_native ✅ 2s 3s -33%
poly_pointwise_montgomery ✅ 2s 2s +0%
poly_reduce ✅ 2s 5s -60%
poly_use_hint_c ✅ 2s 4s -50%
polyeta_pack ✅ 2s 3s -33%
polyt1_unpack ✅ 2s 3s -33%
polyveck_pack_eta ✅ 2s 4s -50%
polyvecl_pointwise_acc_montgomery ✅ 2s 3s -33%
polyvecl_uniform_gamma1_serial ✅ 2s 3s -33%
polyvecl_unpack_eta ✅ 2s 4s -50%
polyz_unpack ✅ 2s 2s +0%
reduce32 ✅ 2s 2s +0%
shake128_absorb ✅ 2s 2s +0%
shake128_finalize ✅ 2s 3s -33%
shake128x4_absorb_once ✅ 2s 4s -50%
shake128x4_squeezeblocks ✅ 2s 1s +100%
shake256x4_absorb_once ✅ 2s 3s -33%
shake256x4_squeezeblocks ✅ 2s 1s +100%
sign_verify ✅ 2s 4s -50%
unpack_sk_s2hat ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid ✅ 1s 3s -67%
keccak_init ✅ 1s 4s -75%
keccak_squeeze ✅ 1s 2s -50%
mld_ct_cmask_neg_i32 ✅ 1s 3s -67%
mld_ct_cmask_nonzero_u32 ✅ 1s 3s -67%
mld_ct_sel_int32 ✅ 1s 1s +0%
pack_pk ✅ 1s 2s -50%
shake256 ✅ 1s 2s -50%
sk_s1hat_get_poly ✅ 1s 3s -67%

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Apr 28, 2026 •
edited
Loading

CBMC Results (ML-DSA-87)

Full Results (195 proofs)
Proof Status Current Previous Change
**TOTAL** ✅ 2417s 2249s +7.5%
sign_verify_internal ✅ 364s 345s +6%
polyvecl_pointwise_acc_montgomery_c ✅ 267s 243s +10%
polyvec_matrix_expand ✅ 169s 157s +8%
rej_uniform_native ✅ 132s 120s +10%
poly_pointwise_montgomery_c ✅ 112s 101s +11%
mld_invntt_layer ✅ 101s 94s +7%
mld_ct_memcmp ✅ 85s 76s +12%
mld_attempt_signature_generation ✅ 69s 66s +5%
sign_keypair_internal ✅ 59s 54s +9%
polyvec_matrix_expand_serial ✅ 47s 45s +4%
mld_ntt_layer ✅ 46s 45s +2%
sign_signature_internal ✅ 36s 34s +6%
sign_pk_from_sk ✅ 35s 32s +9%
fqmul ✅ 32s 28s +14%
keccakf1600x4_permute_native ✅ 23s 22s +5%
rej_uniform ✅ 22s 20s +10%
poly_chknorm_c ✅ 19s 18s +6%
polyt0_unpack ✅ 19s 17s +12%
mld_ntt_butterfly_block ✅ 16s 15s +7%
polyveck_chknorm ✅ 15s 13s +15%
poly_uniform_eta_4x ✅ 13s 15s -13%
polyveck_power2round ✅ 13s 12s +8%
rej_uniform_c ✅ 13s 14s -7%
poly_add ✅ 12s 12s +0%
polyveck_add ✅ 12s 9s +33%
polyveck_decompose ✅ 12s 11s +9%
polyvecl_chknorm ✅ 12s 10s +20%
mld_compute_pack_z ✅ 11s 9s +22%
poly_invntt_tomont_c ✅ 10s 8s +25%
poly_uniform_4x ✅ 10s 10s +0%
polyveck_use_hint ✅ 10s 11s -9%
keccak_absorb_once_x4 ✅ 9s 9s +0%
polyvec_matrix_pointwise_montgomery ✅ 9s 7s +29%
sign ✅ 9s 6s +50%
keccakf1600_permute_native ✅ 8s 6s +33%
mld_check_pct ✅ 8s 10s -20%
pointwise_acc_native_aarch64 ✅ 8s 8s +0%
pointwise_acc_native_x86_64 ✅ 8s 8s +0%
polyveck_caddq ✅ 8s 10s -20%
mld_prepare_domain_separation_prefix ✅ 7s 4s +75%
mld_sample_s1_s2 ✅ 7s 6s +17%
mld_sample_s1_s2_serial ✅ 7s 6s +17%
poly_decompose_c ✅ 7s 6s +17%
polyeta_unpack ✅ 7s 4s +75%
polyveck_pack_t0 ✅ 7s 3s +133%
polyvecl_uniform_gamma1 ✅ 7s 2s +250%
keccak_absorb ✅ 6s 7s -14%
keccakf1600_permute ✅ 6s 8s -25%
poly_power2round ✅ 6s 6s +0%
polyveck_reduce ✅ 6s 5s +20%
polyveck_sub ✅ 6s 4s +50%
polyveck_unpack_eta ✅ 6s 4s +50%
polyvecl_ntt ✅ 6s 7s -14%
shake128_finalize ✅ 6s 1s +500%
unpack_hints ✅ 6s 6s +0%
intt_native_x86_64 ✅ 5s 3s +67%
keccak_squeezeblocks_x4 ✅ 5s 5s +0%
ntt_native_x86_64 ✅ 5s 3s +67%
poly_caddq_c ✅ 5s 3s +67%
poly_chknorm_native ✅ 5s 2s +150%
poly_decompose_native ✅ 5s 3s +67%
poly_shiftl ✅ 5s 6s -17%
poly_uniform_eta ✅ 5s 5s +0%
poly_uniform_gamma1_4x ✅ 5s 3s +67%
polyvec_matrix_pointwise_montgomery_yvec ✅ 5s 4s +25%
polyveck_invntt_tomont ✅ 5s 5s +0%
polyveck_pointwise_poly_montgomery ✅ 5s 5s +0%
polyveck_shiftl ✅ 5s 6s -17%
polyz_unpack_native ✅ 5s 1s +400%
power2round ✅ 5s 3s +67%
rej_eta_c ✅ 5s 5s +0%
sign_signature ✅ 5s 4s +25%
sign_signature_pre_hash_shake256 ✅ 5s 4s +25%
sign_verify_extmu ✅ 5s 4s +25%
sk_s2hat_get_poly ✅ 5s 5s +0%
unpack_sk ✅ 5s 4s +25%
unpack_sk_s2hat ✅ 5s 4s +25%
caddq ✅ 4s 2s +100%
keccakf1600x4_extract_bytes ✅ 4s 2s +100%
keccakf1600x4_xor_bytes ✅ 4s 3s +33%
mld_ct_cmask_nonzero_u32 ✅ 4s 4s +0%
mld_ct_cmask_nonzero_u8 ✅ 4s 1s +300%
mld_h ✅ 4s 3s +33%
mld_polymat_expand_entry ✅ 4s 3s +33%
montgomery_reduce ✅ 4s 5s -20%
ntt_native_aarch64 ✅ 4s 2s +100%
nttunpack_native_x86_64 ✅ 4s 3s +33%
pointwise_native_aarch64 ✅ 4s 2s +100%
pointwise_native_x86_64 ✅ 4s 2s +100%
poly_chknorm ✅ 4s 3s +33%
poly_ntt ✅ 4s 3s +33%
poly_permute_bitrev_to_custom_optional_native ✅ 4s 4s +0%
poly_uniform ✅ 4s 3s +33%
poly_uniform_gamma1 ✅ 4s 3s +33%
poly_use_hint_c ✅ 4s 2s +100%
polyt0_pack ✅ 4s 3s +33%
polyveck_ntt ✅ 4s 5s -20%
polyveck_pack_w1 ✅ 4s 3s +33%
polyveck_unpack_t0 ✅ 4s 3s +33%
polyvecl_uniform_gamma1_serial ✅ 4s 4s +0%
polyz_unpack ✅ 4s 2s +100%
polyz_unpack_c ✅ 4s 4s +0%
shake128_absorb ✅ 4s 5s -20%
sign_verify ✅ 4s 4s +0%
sign_verify_pre_hash_internal ✅ 4s 5s -20%
sk_t0hat_get_poly ✅ 4s 2s +100%
sys_check_capability ✅ 4s 4s +0%
unpack_sk_t0hat ✅ 4s 4s +0%
use_hint ✅ 4s 2s +100%
decompose ✅ 3s 3s +0%
fqscale ✅ 3s 4s -25%
keccak_f1600_x1_native_aarch64 ✅ 3s 4s -25%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid ✅ 3s 4s -25%
keccak_finalize ✅ 3s 3s +0%
keccakf1600_xor_bytes ✅ 3s 1s +200%
keccakf1600x4_permute ✅ 3s 2s +50%
mld_ct_cmask_neg_i32 ✅ 3s 2s +50%
mld_ct_get_optblocker_u8 ✅ 3s 2s +50%
mld_ct_sel_int32 ✅ 3s 1s +200%
mld_value_barrier_i64 ✅ 3s 4s -25%
mld_value_barrier_u8 ✅ 3s 2s +50%
pack_pk ✅ 3s 3s +0%
pack_sig_c ✅ 3s 3s +0%
pack_sig_z ✅ 3s 2s +50%
pack_sk_rho_key_tr_s2_t0 ✅ 3s 4s -25%
pack_sk_s1 ✅ 3s 2s +50%
poly_caddq ✅ 3s 3s +0%
poly_caddq_native_aarch64 ✅ 3s 3s +0%
poly_caddq_native_x86_64 ✅ 3s - new
poly_challenge ✅ 3s 4s -25%
poly_invntt_tomont ✅ 3s 4s -25%
poly_invntt_tomont_native ✅ 3s 2s +50%
poly_ntt_c ✅ 3s 2s +50%
poly_ntt_native ✅ 3s 2s +50%
poly_permute_bitrev_to_custom_optional ✅ 3s 2s +50%
poly_pointwise_montgomery ✅ 3s 4s -25%
poly_pointwise_montgomery_native ✅ 3s 3s +0%
poly_reduce ✅ 3s 2s +50%
poly_use_hint ✅ 3s 5s -40%
polyveck_pack_eta ✅ 3s 3s +0%
polyvecl_pack_eta ✅ 3s 3s +0%
polyvecl_pointwise_acc_montgomery ✅ 3s 3s +0%
polyvecl_unpack_eta ✅ 3s 4s -25%
polyvecl_unpack_z ✅ 3s 4s -25%
polyw1_pack ✅ 3s 3s +0%
polyz_pack ✅ 3s 1s +200%
rej_eta ✅ 3s 3s +0%
rej_eta_native ✅ 3s 3s +0%
shake128x4_squeezeblocks ✅ 3s 3s +0%
sign_open ✅ 3s 3s +0%
sign_verify_pre_hash_shake256 ✅ 3s 3s +0%
sk_s1hat_get_poly ✅ 3s 3s +0%
unpack_pk ✅ 3s 3s +0%
unpack_sig ✅ 3s 2s +50%
unpack_sk_s1hat ✅ 3s 4s -25%
keccak_f1600_x1_native_aarch64_v84a ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v84a ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid ✅ 2s 4s -50%
keccak_init ✅ 2s 2s +0%
keccak_squeeze ✅ 2s 3s -33%
keccakf1600_extract_bytes (big endian) ✅ 2s 5s -60%
keccakf1600_xor_bytes (big endian) ✅ 2s 5s -60%
make_hint ✅ 2s 3s -33%
mld_ct_get_optblocker_i64 ✅ 2s 4s -50%
mld_keccakf1600_extract_bytes ✅ 2s 3s -33%
mld_value_barrier_u32 ✅ 2s 4s -50%
pack_sig_h_poly ✅ 2s 3s -33%
poly_caddq_native ✅ 2s 4s -50%
poly_chknorm_native_aarch64 ✅ 2s 3s -33%
poly_decompose ✅ 2s 4s -50%
poly_make_hint ✅ 2s 3s -33%
poly_sub ✅ 2s 2s +0%
poly_use_hint_native ✅ 2s 4s -50%
polyeta_pack ✅ 2s 5s -60%
polyt1_pack ✅ 2s 2s +0%
polyt1_unpack ✅ 2s 3s -33%
polyvecl_pointwise_acc_montgomery_native ✅ 2s 3s -33%
reduce32 ✅ 2s 4s -50%
shake128_release ✅ 2s 2s +0%
shake128x4_absorb_once ✅ 2s 3s -33%
shake256 ✅ 2s 4s -50%
shake256_absorb ✅ 2s 2s +0%
shake256_finalize ✅ 2s 2s +0%
shake256_init ✅ 2s 2s +0%
shake256_release ✅ 2s 3s -33%
shake256x4_absorb_once ✅ 2s 2s +0%
shake256x4_squeezeblocks ✅ 2s 4s -50%
sign_keypair ✅ 2s 5s -60%
sign_signature_extmu ✅ 2s 3s -33%
sign_signature_pre_hash_internal ✅ 2s 3s -33%
mld_ct_abs_i32 ✅ 1s 3s -67%
mld_ct_get_optblocker_u32 ✅ 1s 1s +0%
shake128_init ✅ 1s 2s -50%
shake128_squeeze ✅ 1s 2s -50%
shake256_squeeze ✅ 1s 3s -67%

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Apr 28, 2026 •
edited
Loading

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

Full Results (195 proofs)
Proof Status Current Previous Change
**TOTAL** ✅ 2230s 2077s +7.4%
polyvec_matrix_pointwise_montgomery ✅ 609s 519s +17%
sign_verify_internal ✅ 184s 173s +6%
poly_pointwise_montgomery_c ✅ 112s 103s +9%
rej_uniform_native ✅ 112s 104s +8%
mld_invntt_layer ✅ 107s 97s +10%
polyvec_matrix_pointwise_montgomery_yvec ✅ 96s 89s +8%
mld_ct_memcmp ✅ 77s 71s +8%
mld_ntt_layer ✅ 44s 41s +7%
fqmul ✅ 30s 28s +7%
sign_keypair_internal ✅ 28s 31s -10%
keccakf1600x4_permute_native ✅ 23s 22s +5%
mld_attempt_signature_generation ✅ 20s 23s -13%
polyeta_unpack ✅ 17s 18s -6%
polyvecl_chknorm ✅ 17s 16s +6%
mld_ntt_butterfly_block ✅ 15s 16s -6%
poly_chknorm_c ✅ 15s 15s +0%
poly_uniform_eta_4x ✅ 14s 12s +17%
polyt0_unpack ✅ 14s 14s +0%
sign_pk_from_sk ✅ 14s 17s -18%
mld_check_pct ✅ 13s 10s +30%
poly_add ✅ 13s 12s +8%
polyveck_decompose ✅ 13s 15s -13%
keccak_absorb_once_x4 ✅ 10s 9s +11%
polyveck_add ✅ 10s 10s +0%
polyveck_caddq ✅ 10s 11s -9%
rej_uniform ✅ 10s 8s +25%
polyveck_power2round ✅ 9s 7s +29%
mld_sample_s1_s2 ✅ 8s 5s +60%
keccakf1600_permute ✅ 7s 6s +17%
mld_sample_s1_s2_serial ✅ 7s 6s +17%
pointwise_acc_native_aarch64 ✅ 7s 8s -12%
pointwise_acc_native_x86_64 ✅ 7s 6s +17%
poly_caddq_c ✅ 7s 10s -30%
poly_invntt_tomont_c ✅ 7s 8s -12%
polyveck_invntt_tomont ✅ 7s 4s +75%
polyveck_pointwise_poly_montgomery ✅ 7s 7s +0%
polyveck_use_hint ✅ 7s 6s +17%
rej_uniform_c ✅ 7s 8s -12%
keccak_absorb ✅ 6s 5s +20%
keccak_squeezeblocks_x4 ✅ 6s 4s +50%
polyveck_chknorm ✅ 6s 4s +50%
polyveck_ntt ✅ 6s 5s +20%
polyveck_shiftl ✅ 6s 5s +20%
polyveck_unpack_eta ✅ 6s 4s +50%
polyvecl_ntt ✅ 6s 6s +0%
polyvecl_unpack_z ✅ 6s 3s +100%
sign ✅ 6s 6s +0%
sign_verify_pre_hash_shake256 ✅ 6s 3s +100%
sk_t0hat_get_poly ✅ 6s 2s +200%
unpack_hints ✅ 6s 5s +20%
keccakf1600_permute_native ✅ 5s 7s -29%
keccakf1600x4_permute ✅ 5s 2s +150%
mld_compute_pack_z ✅ 5s 6s -17%
mld_ct_cmask_nonzero_u32 ✅ 5s 3s +67%
mld_ct_get_optblocker_u32 ✅ 5s 4s +25%
mld_keccakf1600_extract_bytes ✅ 5s 3s +67%
mld_prepare_domain_separation_prefix ✅ 5s 4s +25%
pack_sk_rho_key_tr_s2_t0 ✅ 5s 5s +0%
pointwise_native_aarch64 ✅ 5s 5s +0%
poly_chknorm_native_aarch64 ✅ 5s 2s +150%
poly_decompose_c ✅ 5s 4s +25%
poly_shiftl ✅ 5s 5s +0%
poly_uniform_gamma1_4x ✅ 5s 3s +67%
poly_use_hint ✅ 5s 3s +67%
polyveck_reduce ✅ 5s 5s +0%
polyveck_sub ✅ 5s 5s +0%
polyveck_unpack_t0 ✅ 5s 3s +67%
polyvecl_pointwise_acc_montgomery_native ✅ 5s 2s +150%
polyz_unpack ✅ 5s 4s +25%
rej_eta_c ✅ 5s 5s +0%
rej_eta_native ✅ 5s 5s +0%
sign_open ✅ 5s 4s +25%
sign_signature_extmu ✅ 5s 2s +150%
sign_verify_extmu ✅ 5s 5s +0%
unpack_sk_s2hat ✅ 5s 2s +150%
intt_native_x86_64 ✅ 4s 4s +0%
keccak_init ✅ 4s 4s +0%
keccakf1600x4_xor_bytes ✅ 4s 3s +33%
mld_value_barrier_i64 ✅ 4s 2s +100%
mld_value_barrier_u32 ✅ 4s 2s +100%
pointwise_native_x86_64 ✅ 4s 4s +0%
poly_caddq ✅ 4s 2s +100%
poly_chknorm_native ✅ 4s 2s +100%
poly_decompose ✅ 4s 3s +33%
poly_invntt_tomont_native ✅ 4s 4s +0%
poly_make_hint ✅ 4s 4s +0%
poly_uniform ✅ 4s 3s +33%
polyt1_pack ✅ 4s 4s +0%
polyveck_pack_eta ✅ 4s 2s +100%
polyveck_pack_t0 ✅ 4s 3s +33%
polyw1_pack ✅ 4s 3s +33%
power2round ✅ 4s 4s +0%
shake256_finalize ✅ 4s 3s +33%
shake256_init ✅ 4s 1s +300%
sign_signature ✅ 4s 6s -33%
sign_verify ✅ 4s 4s +0%
sign_verify_pre_hash_internal ✅ 4s 4s +0%
unpack_sig ✅ 4s 3s +33%
unpack_sk ✅ 4s 3s +33%
caddq ✅ 3s 3s +0%
decompose ✅ 3s 3s +0%
keccak_f1600_x1_native_aarch64_v84a ✅ 3s 3s +0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid ✅ 3s 2s +50%
keccak_finalize ✅ 3s 4s -25%
keccakf1600_extract_bytes (big endian) ✅ 3s 4s -25%
keccakf1600_xor_bytes (big endian) ✅ 3s 2s +50%
keccakf1600x4_extract_bytes ✅ 3s 4s -25%
mld_ct_abs_i32 ✅ 3s 2s +50%
mld_ct_cmask_nonzero_u8 ✅ 3s 3s +0%
mld_ct_get_optblocker_i64 ✅ 3s 4s -25%
mld_ct_get_optblocker_u8 ✅ 3s 3s +0%
mld_h ✅ 3s 2s +50%
ntt_native_aarch64 ✅ 3s 4s -25%
pack_pk ✅ 3s 2s +50%
pack_sk_s1 ✅ 3s 1s +200%
poly_caddq_native_x86_64 ✅ 3s - new
poly_challenge ✅ 3s 2s +50%
poly_chknorm ✅ 3s 3s +0%
poly_decompose_native ✅ 3s 3s +0%
poly_permute_bitrev_to_custom_optional ✅ 3s 4s -25%
poly_permute_bitrev_to_custom_optional_native ✅ 3s 3s +0%
poly_pointwise_montgomery_native ✅ 3s 5s -40%
poly_power2round ✅ 3s 5s -40%
poly_reduce ✅ 3s 1s +200%
poly_uniform_eta ✅ 3s 4s -25%
poly_uniform_gamma1 ✅ 3s 2s +50%
polyeta_pack ✅ 3s 2s +50%
polyt1_unpack ✅ 3s 3s +0%
polyveck_pack_w1 ✅ 3s 1s +200%
polyvecl_pointwise_acc_montgomery ✅ 3s 5s -40%
polyvecl_uniform_gamma1 ✅ 3s 2s +50%
polyvecl_uniform_gamma1_serial ✅ 3s 2s +50%
polyvecl_unpack_eta ✅ 3s 4s -25%
polyz_unpack_c ✅ 3s 3s +0%
polyz_unpack_native ✅ 3s 4s -25%
shake128_absorb ✅ 3s 3s +0%
shake128x4_absorb_once ✅ 3s 2s +50%
shake256 ✅ 3s 2s +50%
shake256_release ✅ 3s 2s +50%
shake256x4_absorb_once ✅ 3s 2s +50%
sign_signature_internal ✅ 3s 4s -25%
sign_signature_pre_hash_internal ✅ 3s 4s -25%
sign_signature_pre_hash_shake256 ✅ 3s 5s -40%
sys_check_capability ✅ 3s 5s -40%
unpack_sk_s1hat ✅ 3s 2s +50%
keccak_f1600_x4_native_aarch64_v84a ✅ 2s 1s +100%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid ✅ 2s 2s +0%
keccakf1600_xor_bytes ✅ 2s 2s +0%
make_hint ✅ 2s 3s -33%
mld_polymat_expand_entry ✅ 2s 3s -33%
mld_value_barrier_u8 ✅ 2s 2s +0%
ntt_native_x86_64 ✅ 2s 4s -50%
nttunpack_native_x86_64 ✅ 2s 3s -33%
pack_sig_c ✅ 2s 4s -50%
pack_sig_z ✅ 2s 3s -33%
poly_caddq_native_aarch64 ✅ 2s 4s -50%
poly_invntt_tomont ✅ 2s 2s +0%
poly_ntt_c ✅ 2s 2s +0%
poly_ntt_native ✅ 2s 4s -50%
poly_pointwise_montgomery ✅ 2s 2s +0%
poly_sub ✅ 2s 5s -60%
poly_uniform_4x ✅ 2s 4s -50%
poly_use_hint_c ✅ 2s 3s -33%
poly_use_hint_native ✅ 2s 3s -33%
polyvec_matrix_expand ✅ 2s 2s +0%
polyvec_matrix_expand_serial ✅ 2s 5s -60%
polyvecl_pack_eta ✅ 2s 2s +0%
reduce32 ✅ 2s 1s +100%
rej_eta ✅ 2s 2s +0%
shake128_finalize ✅ 2s 1s +100%
shake128_init ✅ 2s 2s +0%
shake128_squeeze ✅ 2s 2s +0%
shake128x4_squeezeblocks ✅ 2s 1s +100%
shake256x4_squeezeblocks ✅ 2s 3s -33%
sign_keypair ✅ 2s 3s -33%
sk_s1hat_get_poly ✅ 2s 4s -50%
sk_s2hat_get_poly ✅ 2s 2s +0%
unpack_pk ✅ 2s 4s -50%
unpack_sk_t0hat ✅ 2s 4s -50%
use_hint ✅ 2s 2s +0%
fqscale ✅ 1s 5s -80%
keccak_f1600_x1_native_aarch64 ✅ 1s 2s -50%
keccak_squeeze ✅ 1s 4s -75%
mld_ct_cmask_neg_i32 ✅ 1s 3s -67%
mld_ct_sel_int32 ✅ 1s 2s -50%
montgomery_reduce ✅ 1s 6s -83%
pack_sig_h_poly ✅ 1s 5s -80%
poly_caddq_native ✅ 1s 2s -50%
poly_ntt ✅ 1s 3s -67%
polyt0_pack ✅ 1s 5s -80%
polyvecl_pointwise_acc_montgomery_c ✅ 1s 2s -50%
polyz_pack ✅ 1s 4s -75%
shake128_release ✅ 1s 5s -80%
shake256_absorb ✅ 1s 3s -67%
shake256_squeeze ✅ 1s 3s -67%

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Apr 28, 2026 •
edited
Loading

CBMC Results (ML-DSA-44)

Full Results (195 proofs)
Proof Status Current Previous Change
**TOTAL** ✅ 2838s 2623s +8.2%
polyvecl_pointwise_acc_montgomery_c ✅ 1160s 1019s +14%
sign_verify_internal ✅ 229s 233s -2%
rej_uniform_native ✅ 131s 124s +6%
poly_pointwise_montgomery_c ✅ 113s 106s +7%
mld_invntt_layer ✅ 99s 97s +2%
mld_ct_memcmp ✅ 82s 77s +6%
mld_attempt_signature_generation ✅ 54s 52s +4%
mld_ntt_layer ✅ 47s 44s +7%
polyvec_matrix_expand ✅ 32s 28s +14%
fqmul ✅ 31s 28s +11%
sign_keypair_internal ✅ 23s 22s +5%
keccakf1600x4_permute_native ✅ 22s 23s -4%
rej_uniform ✅ 22s 21s +5%
polyt0_unpack ✅ 21s 21s +0%
sign_signature_internal ✅ 21s 16s +31%
rej_uniform_c ✅ 19s 14s +36%
poly_chknorm_c ✅ 18s 20s -10%
mld_ntt_butterfly_block ✅ 17s 19s -11%
sign_pk_from_sk ✅ 16s 15s +7%
poly_add ✅ 13s 11s +18%
poly_uniform_eta_4x ✅ 13s 14s -7%
poly_uniform_4x ✅ 12s 10s +20%
polyz_unpack_c ✅ 11s 10s +10%
keccak_absorb_once_x4 ✅ 10s 10s +0%
keccak_absorb ✅ 9s 6s +50%
mld_check_pct ✅ 9s 8s +12%
keccakf1600_permute ✅ 8s 8s +0%
pointwise_acc_native_x86_64 ✅ 8s 4s +100%
poly_invntt_tomont_c ✅ 8s 8s +0%
poly_power2round ✅ 8s 7s +14%
keccakf1600_permute_native ✅ 7s 8s -12%
polyveck_add ✅ 7s 8s -12%
sign_signature ✅ 7s 3s +133%
unpack_sk_s2hat ✅ 7s 4s +75%
fqscale ✅ 6s 2s +200%
keccak_squeezeblocks_x4 ✅ 6s 6s +0%
mld_compute_pack_z ✅ 6s 6s +0%
poly_uniform_eta ✅ 6s 4s +50%
polyveck_chknorm ✅ 6s 5s +20%
polyveck_decompose ✅ 6s 7s -14%
polyveck_power2round ✅ 6s 4s +50%
polyvecl_ntt ✅ 6s 4s +50%
polyvecl_pointwise_acc_montgomery_native ✅ 6s 5s +20%
rej_eta_c ✅ 6s 3s +100%
sign ✅ 6s 5s +20%
sign_keypair ✅ 6s 3s +100%
sign_verify_extmu ✅ 6s 3s +100%
mld_sample_s1_s2 ✅ 5s 5s +0%
pack_sig_c ✅ 5s 4s +25%
pointwise_acc_native_aarch64 ✅ 5s 4s +25%
pointwise_native_x86_64 ✅ 5s 1s +400%
poly_caddq_c ✅ 5s 4s +25%
poly_chknorm_native ✅ 5s 5s +0%
poly_uniform_gamma1 ✅ 5s 2s +150%
polyeta_unpack ✅ 5s 5s +0%
polyvec_matrix_expand_serial ✅ 5s 5s +0%
polyveck_caddq ✅ 5s 4s +25%
polyveck_pointwise_poly_montgomery ✅ 5s 2s +150%
polyveck_shiftl ✅ 5s 6s -17%
polyvecl_pointwise_acc_montgomery ✅ 5s 6s -17%
polyvecl_uniform_gamma1 ✅ 5s 5s +0%
rej_eta ✅ 5s 3s +67%
rej_eta_native ✅ 5s 4s +25%
shake128_init ✅ 5s 3s +67%
shake128_release ✅ 5s 4s +25%
sign_open ✅ 5s 6s -17%
sign_verify_pre_hash_internal ✅ 5s 4s +25%
sk_s2hat_get_poly ✅ 5s 2s +150%
unpack_hints ✅ 5s 6s -17%
caddq ✅ 4s 2s +100%
keccak_f1600_x1_native_aarch64 ✅ 4s 2s +100%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid ✅ 4s 1s +300%
keccakf1600x4_permute ✅ 4s 3s +33%
keccakf1600x4_xor_bytes ✅ 4s 2s +100%
mld_ct_cmask_neg_i32 ✅ 4s 4s +0%
mld_keccakf1600_extract_bytes ✅ 4s 2s +100%
nttunpack_native_x86_64 ✅ 4s 4s +0%
pack_sig_h_poly ✅ 4s 1s +300%
pack_sk_rho_key_tr_s2_t0 ✅ 4s 4s +0%
poly_caddq_native ✅ 4s 5s -20%
poly_caddq_native_aarch64 ✅ 4s 3s +33%
poly_challenge ✅ 4s 5s -20%
poly_decompose_native ✅ 4s 3s +33%
poly_ntt ✅ 4s 6s -33%
poly_permute_bitrev_to_custom_optional ✅ 4s 2s +100%
poly_reduce ✅ 4s 4s +0%
poly_uniform ✅ 4s 3s +33%
poly_uniform_gamma1_4x ✅ 4s 3s +33%
poly_use_hint_c ✅ 4s 7s -43%
polyeta_pack ✅ 4s 2s +100%
polyveck_invntt_tomont ✅ 4s 7s -43%
polyveck_ntt ✅ 4s 5s -20%
polyveck_reduce ✅ 4s 4s +0%
polyveck_sub ✅ 4s 5s -20%
polyvecl_chknorm ✅ 4s 4s +0%
polyvecl_pack_eta ✅ 4s 3s +33%
sign_signature_pre_hash_internal ✅ 4s 5s -20%
sign_signature_pre_hash_shake256 ✅ 4s 3s +33%
sign_verify_pre_hash_shake256 ✅ 4s 2s +100%
sk_s1hat_get_poly ✅ 4s 2s +100%
unpack_sk_s1hat ✅ 4s 4s +0%
use_hint ✅ 4s 2s +100%
keccak_init ✅ 3s 3s +0%
keccakf1600_extract_bytes (big endian) ✅ 3s 3s +0%
make_hint ✅ 3s 2s +50%
mld_ct_cmask_nonzero_u32 ✅ 3s 2s +50%
mld_h ✅ 3s 4s -25%
mld_polymat_expand_entry ✅ 3s 2s +50%
mld_prepare_domain_separation_prefix ✅ 3s 3s +0%
mld_value_barrier_i64 ✅ 3s 3s +0%
mld_value_barrier_u32 ✅ 3s 1s +200%
mld_value_barrier_u8 ✅ 3s 4s -25%
pack_pk ✅ 3s 3s +0%
pack_sig_z ✅ 3s 2s +50%
pack_sk_s1 ✅ 3s 4s -25%
poly_caddq ✅ 3s 4s -25%
poly_caddq_native_x86_64 ✅ 3s - new
poly_chknorm ✅ 3s 2s +50%
poly_chknorm_native_aarch64 ✅ 3s 4s -25%
poly_decompose_c ✅ 3s 3s +0%
poly_invntt_tomont_native ✅ 3s 4s -25%
poly_make_hint ✅ 3s 2s +50%
poly_permute_bitrev_to_custom_optional_native ✅ 3s 2s +50%
poly_pointwise_montgomery ✅ 3s 3s +0%
poly_pointwise_montgomery_native ✅ 3s 2s +50%
poly_shiftl ✅ 3s 5s -40%
polyt1_pack ✅ 3s 3s +0%
polyvec_matrix_pointwise_montgomery ✅ 3s 4s -25%
polyvec_matrix_pointwise_montgomery_yvec ✅ 3s 5s -40%
polyveck_pack_eta ✅ 3s 3s +0%
polyveck_unpack_eta ✅ 3s 3s +0%
polyveck_unpack_t0 ✅ 3s 2s +50%
polyveck_use_hint ✅ 3s 4s -25%
polyvecl_uniform_gamma1_serial ✅ 3s 2s +50%
polyvecl_unpack_z ✅ 3s 2s +50%
polyw1_pack ✅ 3s 3s +0%
polyz_pack ✅ 3s 3s +0%
reduce32 ✅ 3s 3s +0%
shake128_finalize ✅ 3s 4s -25%
shake128x4_absorb_once ✅ 3s 2s +50%
shake128x4_squeezeblocks ✅ 3s 1s +200%
shake256 ✅ 3s 3s +0%
shake256x4_absorb_once ✅ 3s 4s -25%
shake256x4_squeezeblocks ✅ 3s 4s -25%
sign_signature_extmu ✅ 3s 3s +0%
sign_verify ✅ 3s 4s -25%
sk_t0hat_get_poly ✅ 3s 4s -25%
intt_native_x86_64 ✅ 2s 2s +0%
keccak_f1600_x1_native_aarch64_v84a ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v84a ✅ 2s 2s +0%
keccak_finalize ✅ 2s 1s +100%
keccakf1600_xor_bytes ✅ 2s 3s -33%
keccakf1600_xor_bytes (big endian) ✅ 2s 3s -33%
keccakf1600x4_extract_bytes ✅ 2s 3s -33%
mld_ct_cmask_nonzero_u8 ✅ 2s 2s +0%
mld_ct_get_optblocker_i64 ✅ 2s 2s +0%
mld_ct_get_optblocker_u32 ✅ 2s 3s -33%
mld_ct_sel_int32 ✅ 2s 2s +0%
mld_sample_s1_s2_serial ✅ 2s 4s -50%
montgomery_reduce ✅ 2s 4s -50%
ntt_native_aarch64 ✅ 2s 5s -60%
ntt_native_x86_64 ✅ 2s 4s -50%
pointwise_native_aarch64 ✅ 2s 2s +0%
poly_decompose ✅ 2s 2s +0%
poly_invntt_tomont ✅ 2s 2s +0%
poly_ntt_c ✅ 2s 4s -50%
poly_ntt_native ✅ 2s 4s -50%
poly_sub ✅ 2s 4s -50%
poly_use_hint ✅ 2s 2s +0%
poly_use_hint_native ✅ 2s 4s -50%
polyt0_pack ✅ 2s 5s -60%
polyt1_unpack ✅ 2s 3s -33%
polyveck_pack_t0 ✅ 2s 3s -33%
polyveck_pack_w1 ✅ 2s 2s +0%
polyvecl_unpack_eta ✅ 2s 3s -33%
polyz_unpack ✅ 2s 2s +0%
polyz_unpack_native ✅ 2s 3s -33%
shake128_absorb ✅ 2s 3s -33%
shake128_squeeze ✅ 2s 2s +0%
shake256_absorb ✅ 2s 3s -33%
shake256_finalize ✅ 2s 3s -33%
shake256_init ✅ 2s 2s +0%
shake256_squeeze ✅ 2s 3s -33%
sys_check_capability ✅ 2s 1s +100%
unpack_pk ✅ 2s 3s -33%
unpack_sig ✅ 2s 3s -33%
unpack_sk ✅ 2s 3s -33%
unpack_sk_t0hat ✅ 2s 3s -33%
decompose ✅ 1s 2s -50%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid ✅ 1s 3s -67%
keccak_squeeze ✅ 1s 1s +0%
mld_ct_abs_i32 ✅ 1s 2s -50%
mld_ct_get_optblocker_u8 ✅ 1s 1s +0%
power2round ✅ 1s 3s -67%
shake256_release ✅ 1s 3s -67%

jakemas added 3 commits April 28, 2026 21:15
@jakemas
x86: Fix mldsa_poly_caddq bytecode annotations
b22d68f 
Update instruction comments to match autogen output from the
s2n-bignum VPCMPGTD decoder, and include the RET byte in the
machine code definition.

Signed-off-by: Jake Massimo <jakemas@amazon.com>
@jakemas
x86: Fix REWRITE_CONV type error in mldsa_poly_caddq proof
1495728 
Wrap REWRITE_CONV in CONV_TAC — REWRITE_CONV is a conv, not a tactic.

Signed-off-by: Jake Massimo <jakemas@amazon.com>
@jakemas
x86: Use define_trimmed/X86_MK_CORE_EXEC_RULE for mldsa_poly_caddq
5073550 
Port the TMC (trimmed machine code) handling from the s2n-bignum proof
to use define_trimmed and X86_MK_CORE_EXEC_RULE instead of a broken
BUTLAST_CLAUSES SPEC approach. The NOIBT subroutine proof now correctly
uses mldsa_poly_caddq_tmc.

Signed-off-by: Jake Massimo <jakemas@amazon.com>
@jakemas jakemas changed the title x86: Add HOL Light proof and CBMC contracts for poly_caddq HOL-Light: Add HOL Light proof and CBMC contracts for x86 poly_caddq Apr 28, 2026
@jakemas jakemas force-pushed the x86-poly-caddq-hol-light branch from 2953562 to dcc44a1 Compare April 28, 2026 23:52
@jakemas
Fix x86 poly_caddq proof: use SIMD_SIMPLIFY_TAC to avoid stack overflow
297acb1 
Replace TOP_DEPTH_CONV WORD_SIMPLE_SUBWORD_CONV with SIMD_SIMPLIFY_TAC
and use bytes256 (AVX2 YMM) memory merging instead of bytes128. The old
approach caused exponential assumption growth leading to stack overflow
after ~97 minutes in CI.

Signed-off-by: Jake Massimo <jakemas@amazon.com>
@jakemas jakemas force-pushed the x86-poly-caddq-hol-light branch from dcc44a1 to 297acb1 Compare April 29, 2026 02:06
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.

HOL-Light: Prove AVX2 poly_caddq

2 participants

@jakemas @oqs-bot