Skip to content

Proofs/Isabelle: Add Neon NTT formalization and conformance harness#1135

Open
hanno-becker wants to merge 1 commit into
mainfrom
barrett_isabelle
Open

Proofs/Isabelle: Add Neon NTT formalization and conformance harness#1135
hanno-becker wants to merge 1 commit into
mainfrom
barrett_isabelle

Conversation

@hanno-becker
Copy link
Copy Markdown
Contributor

@hanno-becker hanno-becker commented May 29, 2026 •
edited
Loading

This commit adds additional formal documentation of the approach to
modular arithmetic used in various assembly kernels in mldsa-native
and mlkem-native.

Specifically, it adds source and final PDF document for an Isabelle/HOL
formalization of the original "Neon NTT" paper [1] of Becker, Hwang,
Kannwischer, Yang, and Yang.

The documentation was obtained as human-directed auto-formalization
using Claude Opus 4.7 + the AutoCorrode I/Q + I/R AI integration
infrastructure for Isabelle.

The commit also adds a conformance testing harness to empirically
validate that the ad-hoc instructions models used in the formalization
match concrete execution on an AArch64 host.

CI is extended to re-build the PDF and build+run the conformance testing.

[1]:

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented May 29, 2026 •
edited
Loading

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

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

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented May 29, 2026 •
edited
Loading

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

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

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented May 29, 2026 •
edited
Loading

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

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

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented May 29, 2026 •
edited
Loading

CBMC Results (ML-DSA-44)

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

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented May 29, 2026 •
edited
Loading

CBMC Results (ML-DSA-87)

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

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented May 29, 2026 •
edited
Loading

CBMC Results (ML-DSA-65)

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

@hanno-becker hanno-becker force-pushed the barrett_isabelle branch 2 times, most recently from 2d3a07e to 9dd281e Compare May 30, 2026 07:09
@hanno-becker hanno-becker marked this pull request as ready for review May 31, 2026 03:34
@hanno-becker hanno-becker requested a review from a team as a code owner May 31, 2026 03:34
@hanno-becker hanno-becker force-pushed the barrett_isabelle branch 4 times, most recently from 76deab1 to c6d01a3 Compare May 31, 2026 05:34
@hanno-becker
Proofs/Isabelle: Add Neon NTT README and conformance Makefile target
436dce7 
This commit adds additional formal documentation of the approach to
modular arithmetic used in various assembly kernels in mldsa-native
and mlkem-native.

Specifically, it adds source and final PDF document for an Isabelle/HOL
formalization of the original "Neon NTT" paper [1] of Becker, Hwang,
Kannwischer, Yang, and Yang.

The documentation was obtained as human-directed auto-formalization
using Claude Opus 4.7 + the AutoCorrode I/Q + I/R AI integration
infrastructure for Isabelle.

The commit also adds a conformance testing harness to empirically
validate that the ad-hoc instructions models used in the formalization
match concrete execution on an AArch64 host.

CI is extended to re-build the PDF and build+run the conformance testing.

[1]:
  - Becker, Hwang, Kannwischer, Yang, Yang
  - Neon NTT: Faster Dilithium, Kyber, and Saber on Cortex-A72 and Apple M1
  - [https://eprint.iacr.org/2021/986](https://eprint.iacr.org/2021/986)

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@hanno-becker @oqs-bot