Skip to content

HOL-Light: improve tooling and CI - #1009

Open
L-series wants to merge 2 commits into
mainfrom
HOL-Light-CI
Open

HOL-Light: improve tooling and CI#1009
L-series wants to merge 2 commits into
mainfrom
HOL-Light-CI

Conversation

@L-series

@L-series L-series commented Apr 1, 2026 •
edited by mkannwischer
Loading

Copy link
Copy Markdown
Contributor

This PR is a port from: pq-code-package/mlkem-native#1634

Note that this is currently blocked by: #1001

@L-series
L-series requested a review from a team as a code owner April 1, 2026 15:53
@mkannwischer mkannwischer self-assigned this Apr 1, 2026
@oqs-bot

oqs-bot commented Apr 1, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-44)

⚠️ Attention Required

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

@oqs-bot

oqs-bot commented Apr 1, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-65)

⚠️ Attention Required

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

@oqs-bot

oqs-bot commented Apr 1, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-87)

⚠️ Attention Required

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

@mkannwischer

mkannwischer commented Apr 2, 2026

Copy link
Copy Markdown
Contributor

Thanks @L-series. Let's first get this merged in mlkem-native and then align this one. Changing back to draft for now.

Safety proofs are not fully implemented yet here for all proves. We should skip those for now and open an issue to add it later.

@mkannwischer
mkannwischer marked this pull request as draft April 2, 2026 09:38
@L-series
L-series force-pushed the HOL-Light-CI branch 2 times, most recently from 6fbd4ae to 13638f7 Compare August 3, 2026 01:57
@L-series

L-series commented Aug 3, 2026

Copy link
Copy Markdown
Contributor Author

Hello @mkannwischer @hanno-becker, appologies for the delay with this, I got quite distracted with a math paper i was working on this last month 😆 . This should be ready for review now, the check theorems script is slightly different here than what it is in mlkem as it also treats the IBT case.

@L-series
L-series marked this pull request as ready for review August 3, 2026 02:08
@oqs-bot

oqs-bot commented Aug 3, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

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

⚠️ Attention Required

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

@oqs-bot

oqs-bot commented Aug 3, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

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

⚠️ Attention Required

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

@oqs-bot

oqs-bot commented Aug 3, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

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

⚠️ Attention Required

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

@mkannwischer

mkannwischer commented Aug 3, 2026

Copy link
Copy Markdown
Contributor

Hello @mkannwischer @hanno-becker, appologies for the delay with this, I got quite distracted with a math paper i was working on this last month 😆 .

No worries. Thanks for porting this!

This should be ready for review now, the check theorems script is slightly different here than what it is in mlkem as it also treats the IBT case.

Can you elaborate why it needs to be slightly different? IBT isn't something that's specific to mldsa. Should it be ported to mlkem, too?

@mkannwischer

mkannwischer commented Aug 3, 2026

Copy link
Copy Markdown
Contributor

@L-series can you please fix the DCO signoff?

@L-series
L-series force-pushed the HOL-Light-CI branch 3 times, most recently from 79190ea to 61dfaa0 Compare August 3, 2026 19:55
@L-series

L-series commented Aug 3, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor Author

Can you elaborate why it needs to be slightly different? IBT isn't something that's specific to mldsa. Should it be ported to mlkem, too?

@mkannwischer the logic for capturing the let PROVE = ... blocks in mlkem is somehow simpler than in mldsa as all the proof declarations exist on a single line and thus the grep can catch them.

In mldsa, some of the proofs occur with the following slightly more complicated patterns:

let MLDSA_NTT_SAFE =
  REWRITE_RULE [...]
  (time prove (...));;

and

 let MLDSA_REJ_UNIFORM_ETA2_NOIBT_SUBROUTINE_CORRECT =
   let correct_bound = prove ... in
   let th = prove ... in
   th;;

This occurs around a dozen times.

To generalize the logic in the list_thms script, I've made it so that we scan for the theorem producing declaration within the entire top level let NAME = xyz block.

There might be some simpler way of doing this however. Please let me know what you think!

L-series added 2 commits August 3, 2026 16:02
@L-series
testing: HOL-Light: add support for cross-proofing
ee924d1 
This commit introduces a new flag --arch to the hol_light command of the
tests script that allows user specification of which architecture to
run/list the proofs for. If not passed, the behavior is unchanged.

Signed-off-by: Andreas Hatziiliou <andreas.hatziiliou@savoirfairelinux.com>
@L-series
lint: verify that all expected theorems are present
f27ff85 
Add a check-theorems lint step that verifies each HOL-Light assembly proof exposes the expected correctness and safety theorems for its architecture.

The ML-DSA port accounts for rejection-sampling MEMSAFE proofs and x86_64 NOIBT theorem variants. Rejection-sampling routines are detected by substring so renamed mldsa_rej_uniform* files still use MEMSAFE rather than SAFE.

Unlike the ML-KEM theorem lister, the ML-DSA list_thms scripts scan complete top-level let bindings instead of only direct let NAME = prove lines. Several ML-DSA x86_64 safety theorems are wrapped in REWRITE_RULE around time prove, and the eta rejection-sampling subroutine theorems are built via local prove blocks or ADD_IBT_RULE aliases. The broader scan keeps those exported theorem names visible to lint without changing the proof structure.

Signed-off-by: Andreas Hatziiliou <andreas.hatziiliou@savoirfairelinux.com>
@mkannwischer mkannwischer added this to the v2.1 milestone Aug 4, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

@mkannwischer mkannwischer

Labels

None yet

Projects

None yet

Milestone

v2.1

Development

Successfully merging this pull request may close these issues.

Port: HOL-Light: improve tooling and CI

3 participants

@L-series @oqs-bot @mkannwischer