Skip to content

CI: Disable ABI checks on Zephyr targets - #1312

Closed
bremoran wants to merge 1 commit into
mainfrom
fix-zephyr-abicheck-custom-build
Closed

CI: Disable ABI checks on Zephyr targets#1312
bremoran wants to merge 1 commit into
mainfrom
fix-zephyr-abicheck-custom-build

Conversation

@bremoran

@bremoran bremoran commented Jul 24, 2026

Copy link
Copy Markdown
Contributor

Summary

  • add a default-enabled abicheck input to the functest composite action;
  • set abicheck: false for Zephyr functional-test jobs.

This follows the same action-input pattern used for the other optional test
suites. Existing functest callers retain ABI checking by default.

Why

The current ABI checker is not built as a Zephyr application. Normal Zephyr
tests go through the Zephyr CMake build, but abicheck uses the generic Make
rules and derives its architecture from the CI host. On ubuntu-latest, that
produces an x86_64 executable which the Zephyr wrapper then passes to
qemu-system-arm.

On #1277, all preceding Cortex-M55 functional, KAT, ACVP, and sign-hook tests
passed before that host ABI executable reached QEMU and hard-locked at PC=0:

Only M55 reached this path because it is the only Zephyr matrix target using
opt=all; ABI checking is enabled only for optimized builds.

This change makes the current Zephyr exclusion explicit without affecting the
standalone ABI-check command or other functest users. Supporting ABI checking
as a Zephyr application can be handled separately from the Armv8.1-M Keccak
backend work in #1277.

Validation

@bremoran
bremoran force-pushed the fix-zephyr-abicheck-custom-build branch from 055ba4a to 8bdc701 Compare July 24, 2026 16:02
@bremoran bremoran changed the title Test: Run ABI checks through Zephyr custom builds CI: Disable ABI checks on Zephyr targets Jul 24, 2026
@oqs-bot

oqs-bot commented Jul 24, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-44)

⚠️ Attention Required

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

@oqs-bot

oqs-bot commented Jul 24, 2026

Copy link
Copy Markdown
Contributor

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

⚠️ Attention Required

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

@oqs-bot

oqs-bot commented Jul 24, 2026

Copy link
Copy Markdown
Contributor

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

⚠️ Attention Required

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

@oqs-bot

oqs-bot commented Jul 24, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-65)

⚠️ Attention Required

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

@oqs-bot

oqs-bot commented Jul 24, 2026

Copy link
Copy Markdown
Contributor

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

⚠️ Attention Required

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

@oqs-bot

oqs-bot commented Jul 24, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-87)

⚠️ Attention Required

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

@hanno-becker hanno-becker left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why does the ABI checker fail? There's no reason it couldn't run on Zephyr targets, AFAIU.

@bremoran
bremoran force-pushed the fix-zephyr-abicheck-custom-build branch from 8bdc701 to c748ebe Compare July 27, 2026 06:05
@bremoran
bremoran marked this pull request as ready for review July 27, 2026 08:28
@bremoran
bremoran requested a review from a team as a code owner July 27, 2026 08:28
Comment thread .github/workflows/zephyr.yml Outdated
# Zephyr's CMake selects the target arch; disable the host-arch
# auto-detection that would otherwise leak into the forwarded CFLAGS.
extra_args: --no-auto
extra_args: --no-auto --no-abicheck

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Other tests are disabled via an argument to functest, so this is somewhat inconsistent.
Could you please use an Github action argument instead?

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks — addressed in 059167a7d. The functest action now exposes a default-enabled abicheck input and translates it to --abicheck / --no-abicheck, consistently with the other test selectors. The Zephyr workflow sets abicheck: false; extra_args is back to only --no-auto.

The exact-head Zephyr run passed all five targets. In the M55 job, the log shows abicheck: false, extra_args: --no-auto, and the resulting command contains --no-abicheck. Full PR CI is still running without failures.

@bremoran

Copy link
Copy Markdown
Contributor Author

Why does the ABI checker fail? There's no reason it couldn't run on Zephyr targets, AFAIU.

You’re right: there is no fundamental reason the ABI checker could not run on Zephyr. The issue is that it is not currently integrated as a Zephyr application.

Normal Zephyr tests are built as Arm firmware through Zephyr CMake. abicheck, however, follows the generic Make path and derives its architecture from the CI host. On ubuntu-latest, it therefore builds an x86_64 executable. The Zephyr wrapper then passes that executable to qemu-system-arm, which results in a HardFault at PC=0.

Only M55 encounters this because it is the sole Zephyr matrix target using opt=all; ABI checking runs only for optimized builds. The other targets use no_opt and never enter this path.

Because the current setup does not provide valid ABI-check coverage on Zephyr, I disabled it there as an issue orthogonal to the x1 optimization work in #1277. I also agree with @mkannwischer's consistency point: the exclusion should be expressed as a dedicated functest action argument rather than through extra_args.

A working Zephyr ABI checker would require us to:

  1. Select armv81m from the Zephyr target rather than the CI host.
  2. Build the ABI driver, call stub, self-tests, generated checks, and implementation assembly through Zephyr CMake.
  3. Preserve the per-source Arm/MVE feature flags.
  4. Integrate the checker’s entry point, output, and exit status with the Zephyr shim.
  5. Confirm that the checker’s deliberate register-corruption self-tests fail as expected before relying on kernel results.

I agree this would be useful. Could you clarify whether Zephyr-native ABI checking is a prerequisite for merging #1277? If so, we will prioritize it as such; otherwise, I suggest tracking it as a separate test-infrastructure follow-up.

Signed-off-by: Brendan Moran <brendan.moran@arm.com>
@bremoran

Copy link
Copy Markdown
Contributor Author

Superseded by #1318, which runs ABI checks as Zephyr applications instead of disabling them. Closing in favor of #1318.

@bremoran bremoran closed this Jul 30, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants