Skip to content

Doc improvements - #1935

Merged
mkannwischer merged 4 commits into
mainfrom
doc-improvements
Oct 12, 2026
Merged

Doc improvements#1935
mkannwischer merged 4 commits into
mainfrom
doc-improvements

Conversation

@mkannwischer

@mkannwischer mkannwischer commented Oct 10, 2026

Copy link
Copy Markdown
Contributor

See individual commit messages.

@oqs-bot

oqs-bot commented Oct 10, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-768)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
mlk_indcpa_dec LP64 z3* ⚠️ 22s 10s +120%
mlk_indcpa_enc LP64 z3_smt_only* ⚠️ 483s 252s +92%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 303s 7s +4229%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ⚠️ 75s 46s +63%
mlk_rej_uniform_c LP64 z3* ⚠️ 173s 114s +52%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 119s 55s +116%
Full Results (195 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 2044s 1645s +24.3%
intt_native_aarch64 LP64 z3* ✅ 3s 5s -40%
intt_native_x86_64 LP64 z3* ✅ 1s 3s -67%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 3s 1s +200%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 3s 3s +0%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 5s 3s +67%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 1s 1s +0%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 2s 2s +0%
keccakf1600_permute_native LP64 bitwuzla* ✅ 1s 3s -67%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 3s 3s +0%
keccakf1600x4_permute_native_x4 LP64 bitwuzla* ✅ 17s 21s -19%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 3s 2s +50%
kem_check_pk LP64 z3* ✅ 3s 2s +50%
kem_check_sk LP64 z3* ✅ 3s 2s +50%
kem_dec LP64 z3* ✅ 6s 5s +20%
kem_enc LP64 z3* ✅ 2s 2s +0%
kem_enc_derand LP64 z3* ✅ 3s 3s +0%
kem_keypair LP64 z3* ✅ 3s 2s +50%
kem_keypair_derand LP64 z3* ✅ 3s 2s +50%
mlk_barrett_reduce LP64 z3* ✅ 3s 2s +50%
mlk_check_pct LP64 bitwuzla* ✅ 3s 3s +0%
mlk_ct_cmask_neg_i16 LP64 z3* ✅ 3s 3s +0%
mlk_ct_cmask_nonzero_u16 LP64 z3* ✅ 2s 4s -50%
mlk_ct_cmask_nonzero_u8 LP64 z3* ✅ 2s 4s -50%
mlk_ct_cmov_zero LP64 bitwuzla* ✅ 2s 3s -33%
mlk_ct_get_optblocker_i32 ILP32 bitwuzla ✅ 2s 1s +100%
ILP32 cvc5_arrays_exp ✅ 2s 1s +100%
ILP32 z3 ✅ 3s 1s +200%
LP64 bitwuzla* ✅ 2s 1s +100%
LP64 cvc5_arrays_exp ✅ 1s 1s +0%
LP64 z3 ✅ 3s 1s +200%
mlk_ct_get_optblocker_u32 LP64 bitwuzla* ✅ 2s 1s +100%
mlk_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_ct_memcmp LP64 bitwuzla* ✅ 4s 4s +0%
mlk_ct_sel_int16 LP64 z3* ✅ 3s 3s +0%
mlk_ct_sel_uint8 LP64 z3* ✅ 2s 1s +100%
mlk_enc_getnoise_eta1_eta2 LP64 z3* ✅ 2s 3s -33%
mlk_fqmul LP64 z3* ✅ 3s 16s -81%
mlk_gen_matrix LP64 z3* ✅ 2s 2s +0%
mlk_gen_matrix_serial LP64 z3* ✅ 4s 2s +100%
mlk_indcpa_dec LP64 z3* ⚠️ 22s 10s +120%
mlk_indcpa_enc LP64 z3_smt_only* ⚠️ 483s 252s +92%
mlk_indcpa_keypair_derand LP64 z3* ✅ 114s 318s -64%
mlk_invntt_layer LP64 z3* ✅ 7s 4s +75%
mlk_keccak_absorb_once LP64 bitwuzla* ✅ 5s 3s +67%
mlk_keccak_absorb_once_x4 LP64 bitwuzla* ✅ 6s 5s +20%
mlk_keccak_squeeze_once LP64 bitwuzla* ✅ 9s 7s +29%
mlk_keccak_squeezeblocks LP64 bitwuzla* ✅ 7s 8s -12%
mlk_keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 27s 24s +12%
mlk_keccakf1600_extract_bytes LP64 bitwuzla* ✅ 1s 4s -75%
mlk_keccakf1600_extract_bytes (big endian) LP64 bitwuzla* ✅ 3s 2s +50%
mlk_keccakf1600_permute LP64 z3* ✅ 5s 1s +400%
mlk_keccakf1600_permute_c LP64 z3* ✅ 3s 6s -50%
mlk_keccakf1600_xor_bytes LP64 bitwuzla* ✅ 1s 3s -67%
mlk_keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 1s 1s +0%
mlk_keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 2s 4s -50%
mlk_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 3s 2s +50%
mlk_keccakf1600x4_permute LP64 z3* ✅ 3s 4s -25%
mlk_keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 2s 2s +0%
mlk_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 3s 1s +200%
mlk_keypair_getnoise_eta1 LP64 z3* ✅ 2s 2s +0%
mlk_matvec_mul LP64 z3* ✅ 2s 4s -50%
mlk_montgomery_reduce LP64 z3* ✅ 1s 1s +0%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 303s 7s +4229%
mlk_ntt_layer LP64 z3* ✅ 8s 29s -72%
mlk_poly_add LP64 z3* ✅ 6s 7s -14%
mlk_poly_cbd_eta1 LP64 z3* ✅ 1s 1s +0%
mlk_poly_cbd_eta2 LP64 z3* ✅ 1s 2s -50%
mlk_poly_compress_d10 LP64 bitwuzla* ✅ 1s 2s -50%
mlk_poly_compress_d10_c LP64 z3* ✅ 4s 2s +100%
mlk_poly_compress_d10_native LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_compress_d11 LP64 bitwuzla* ✅ 3s 1s +200%
mlk_poly_compress_d11_c LP64 z3* ✅ 2s 1s +100%
mlk_poly_compress_d11_native LP64 bitwuzla* ✅ 2s 4s -50%
mlk_poly_compress_d4 LP64 bitwuzla* ✅ 5s 3s +67%
mlk_poly_compress_d4_c LP64 z3* ✅ 2s 1s +100%
mlk_poly_compress_d4_native LP64 bitwuzla* ✅ 3s 3s +0%
mlk_poly_compress_d5 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_compress_d5_c LP64 z3* ✅ 1s 1s +0%
mlk_poly_compress_d5_native LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_compress_du LP64 bitwuzla* ✅ 1s 1s +0%
mlk_poly_compress_dv LP64 bitwuzla* ✅ 2s 1s +100%
mlk_poly_decompress_d10 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_decompress_d10_c LP64 z3* ✅ 2s 1s +100%
mlk_poly_decompress_d10_native LP64 bitwuzla* ✅ 16s 15s +7%
mlk_poly_decompress_d11 LP64 bitwuzla* ✅ 1s 2s -50%
mlk_poly_decompress_d11_c LP64 z3* ✅ 2s 3s -33%
mlk_poly_decompress_d11_native LP64 bitwuzla* ✅ 2s 1s +100%
mlk_poly_decompress_d4 LP64 bitwuzla* ✅ 1s 3s -67%
mlk_poly_decompress_d4_c LP64 z3* ✅ 2s 4s -50%
mlk_poly_decompress_d4_native LP64 bitwuzla* ✅ 15s 12s +25%
mlk_poly_decompress_d5 LP64 bitwuzla* ✅ 4s 2s +100%
mlk_poly_decompress_d5_c LP64 z3* ✅ 4s 3s +33%
mlk_poly_decompress_d5_native LP64 bitwuzla* ✅ 1s 3s -67%
mlk_poly_decompress_du LP64 bitwuzla* ✅ 4s 1s +300%
mlk_poly_decompress_dv LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_frombytes LP64 bitwuzla* ✅ 4s 2s +100%
mlk_poly_frombytes_c LP64 z3* ✅ 3s 4s -25%
mlk_poly_frombytes_native LP64 bitwuzla* ✅ 15s 8s +88%
mlk_poly_frommsg LP64 z3* ✅ 1s 9s -89%
mlk_poly_getnoise_eta1122_4x LP64 z3* ✅ 2s 1s +100%
mlk_poly_getnoise_eta1122_4x_serial LP64 z3* ✅ 2s - new
mlk_poly_getnoise_eta1_4x LP64 z3* ✅ 2s 2s +0%
mlk_poly_getnoise_eta1_4x_serial LP64 z3* ✅ 4s - new
mlk_poly_getnoise_eta2 LP64 z3* ✅ 1s 2s -50%
mlk_poly_invntt_tomont LP64 z3* ✅ 2s 4s -50%
mlk_poly_invntt_tomont_c LP64 z3* ✅ 3s 2s +50%
mlk_poly_mulcache_compute LP64 z3* ✅ 3s 2s +50%
mlk_poly_mulcache_compute_c LP64 z3* ✅ 3s 2s +50%
mlk_poly_mulcache_compute_native LP64 z3* ✅ 1s 1s +0%
mlk_poly_ntt LP64 bitwuzla* ✅ 8s 5s +60%
mlk_poly_ntt_c LP64 z3* ✅ 2s 1s +100%
mlk_poly_reduce LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_reduce_c LP64 z3* ✅ 1s 3s -67%
mlk_poly_reduce_native LP64 bitwuzla* ✅ 37s 34s +9%
mlk_poly_rej_uniform LP64 bitwuzla* ✅ 38s 129s -71%
mlk_poly_rej_uniform_x4 LP64 z3* ✅ 6s 5s +20%
mlk_poly_sub LP64 z3* ✅ 7s 10s -30%
mlk_poly_tobytes LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_tobytes_c LP64 z3* ✅ 2s 1s +100%
mlk_poly_tobytes_native LP64 bitwuzla* ✅ 2s 1s +100%
mlk_poly_tomont LP64 z3* ✅ 2s 1s +100%
mlk_poly_tomont_c LP64 z3* ✅ 2s 3s -33%
mlk_poly_tomont_native LP64 z3* ✅ 2s 3s -33%
mlk_poly_tomsg LP64 bitwuzla* ✅ 4s 3s +33%
mlk_polymat_permute_bitrev_to_custom LP64 z3* ✅ 2s 3s -33%
mlk_polymat_permute_bitrev_to_custom_native LP64 z3* ✅ 69s - new
mlk_polyvec_add LP64 z3* ✅ 13s 12s +8%
mlk_polyvec_basemul_acc_montgomery_cached LP64 z3* ✅ 3s 4s -25%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ⚠️ 75s 46s +63%
mlk_polyvec_compress_du LP64 z3* ✅ 2s 1s +100%
mlk_polyvec_decompress_du LP64 z3* ✅ 1s 4s -75%
mlk_polyvec_frombytes LP64 z3* ✅ 2s 3s -33%
mlk_polyvec_invntt_tomont LP64 z3* ✅ 3s 1s +200%
mlk_polyvec_mulcache_compute LP64 z3* ✅ 2s 2s +0%
mlk_polyvec_ntt LP64 z3* ✅ 4s 4s +0%
mlk_polyvec_reduce LP64 z3* ✅ 4s 1s +300%
mlk_polyvec_tobytes LP64 z3* ✅ 1s 1s +0%
mlk_polyvec_tomont LP64 z3* ✅ 3s 1s +200%
mlk_rej_uniform LP64 bitwuzla* ✅ 2s 1s +100%
mlk_rej_uniform_c LP64 z3* ⚠️ 173s 114s +52%
mlk_scalar_compress_d1 LP64 z3* ✅ 1s 2s -50%
mlk_scalar_compress_d10 LP64 z3* ✅ 1s 2s -50%
mlk_scalar_compress_d11 LP64 z3* ✅ 2s 1s +100%
mlk_scalar_compress_d4 LP64 z3* ✅ 1s 2s -50%
mlk_scalar_compress_d5 LP64 z3* ✅ 2s 1s +100%
mlk_scalar_decompress_d10 LP64 z3* ✅ 3s 2s +50%
mlk_scalar_decompress_d11 LP64 z3* ✅ 2s 3s -33%
mlk_scalar_decompress_d4 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_decompress_d5 LP64 z3* ✅ 1s 2s -50%
mlk_scalar_signed_to_unsigned_q LP64 z3* ✅ 2s 5s -60%
mlk_sha3_256 LP64 bitwuzla* ✅ 3s 2s +50%
mlk_sha3_512 LP64 bitwuzla* ✅ 3s 3s +0%
mlk_shake128_absorb_once LP64 bitwuzla* ✅ 3s 1s +200%
mlk_shake128_squeezeblocks LP64 bitwuzla* ✅ 2s 3s -33%
mlk_shake128x4_absorb_once LP64 bitwuzla* ✅ 2s 3s -33%
mlk_shake128x4_squeezeblocks LP64 bitwuzla* ✅ 2s 1s +100%
mlk_shake256 LP64 bitwuzla* ✅ 1s 2s -50%
mlk_shake256x4 LP64 bitwuzla* ✅ 5s 3s +67%
mlk_value_barrier_i32 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_value_barrier_u32 LP64 bitwuzla* ✅ 4s 2s +100%
mlk_value_barrier_u8 LP64 bitwuzla* ✅ 1s 2s -50%
ntt_native_aarch64 LP64 z3* ✅ 3s 3s +0%
ntt_native_x86_64 LP64 z3* ✅ 2s 3s -33%
nttunpack_native_x86_64 LP64 z3* ✅ 3s 3s +0%
poly_compress_d10_native_x86_64 LP64 bitwuzla* ✅ 2s 5s -60%
poly_compress_d11_native_x86_64 LP64 bitwuzla* ✅ 2s 3s -33%
poly_compress_d4_native_x86_64 LP64 bitwuzla* ✅ 1s 3s -67%
poly_compress_d5_native_x86_64 LP64 bitwuzla* ✅ 3s 2s +50%
poly_decompress_d10_native_x86_64 LP64 bitwuzla* ✅ 4s 5s -20%
poly_decompress_d11_native_x86_64 LP64 bitwuzla* ✅ 3s 1s +200%
poly_decompress_d4_native_x86_64 LP64 bitwuzla* ✅ 3s 6s -50%
poly_decompress_d5_native_x86_64 LP64 bitwuzla* ✅ 5s 4s +25%
poly_frombytes_native_x86_64 LP64 bitwuzla* ✅ 5s 5s +0%
poly_invntt_tomont_native LP64 z3* ✅ 2s 2s +0%
poly_mulcache_compute_native_aarch64 LP64 z3* ✅ 1s 6s -83%
poly_mulcache_compute_native_x86_64 LP64 z3* ✅ 1s 3s -67%
poly_ntt_native LP64 z3* ✅ 3s 39s -92%
poly_reduce_native_aarch64 LP64 z3* ✅ 2s 2s +0%
poly_reduce_native_x86_64 LP64 z3* ✅ 2s 2s +0%
poly_tobytes_native_aarch64 LP64 z3* ✅ 1s 1s +0%
poly_tobytes_native_x86_64 LP64 z3* ✅ 1s 3s -67%
poly_tomont_native_aarch64 LP64 z3* ✅ 2s 1s +100%
poly_tomont_native_x86_64 LP64 z3* ✅ 3s 1s +200%
polyvec_basemul_acc_montgomery_cached_k2_native_aarch64 LP64 z3* ✅ 1s 3s -67%
polyvec_basemul_acc_montgomery_cached_k2_native_x86_64 LP64 z3* ✅ 2s 4s -50%
polyvec_basemul_acc_montgomery_cached_k3_native_aarch64 LP64 z3* ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k3_native_x86_64 LP64 z3* ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k4_native_aarch64 LP64 z3* ✅ 2s 1s +100%
polyvec_basemul_acc_montgomery_cached_k4_native_x86_64 LP64 z3* ✅ 1s 2s -50%
polyvec_basemul_acc_montgomery_cached_native LP64 z3* ✅ 16s 14s +14%
rej_uniform_native LP64 bitwuzla* ✅ 1s 2s -50%
rej_uniform_native_aarch64 LP64 z3* ✅ 45s 45s +0%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 119s 55s +116%
sys_check_capability LP64 z3* ✅ 2s 3s -33%

@oqs-bot

oqs-bot commented Oct 10, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-1024)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
mlk_ntt_butterfly_block LP64 z3* ⚠️ 303s 9s +3267%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ⚠️ 139s 79s +76%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 120s 67s +79%
Full Results (195 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 2198s 1885s +16.6%
intt_native_aarch64 LP64 z3* ✅ 3s 3s +0%
intt_native_x86_64 LP64 z3* ✅ 3s 2s +50%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 2s 1s +100%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 3s 2s +50%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 2s 3s -33%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 3s 2s +50%
keccakf1600_permute_native LP64 bitwuzla* ✅ 2s 2s +0%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 2s 2s +0%
keccakf1600x4_permute_native_x4 LP64 bitwuzla* ✅ 17s 15s +13%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 2s 2s +0%
kem_check_pk LP64 z3* ✅ 5s 4s +25%
kem_check_sk LP64 z3* ✅ 2s 3s -33%
kem_dec LP64 z3* ✅ 10s 5s +100%
kem_enc LP64 z3* ✅ 3s 2s +50%
kem_enc_derand LP64 z3* ✅ 2s 3s -33%
kem_keypair LP64 z3* ✅ 5s 2s +150%
kem_keypair_derand LP64 z3* ✅ 1s 1s +0%
mlk_barrett_reduce LP64 z3* ✅ 2s 2s +0%
mlk_check_pct LP64 bitwuzla* ✅ 2s 1s +100%
mlk_ct_cmask_neg_i16 LP64 z3* ✅ 2s 3s -33%
mlk_ct_cmask_nonzero_u16 LP64 z3* ✅ 2s 2s +0%
mlk_ct_cmask_nonzero_u8 LP64 z3* ✅ 4s 1s +300%
mlk_ct_cmov_zero LP64 bitwuzla* ✅ 1s 3s -67%
mlk_ct_get_optblocker_i32 ILP32 bitwuzla ✅ 2s 3s -33%
ILP32 cvc5_arrays_exp ✅ 3s 3s +0%
ILP32 z3 ✅ 1s 3s -67%
LP64 bitwuzla* ✅ 2s 3s -33%
LP64 cvc5_arrays_exp ✅ 2s 3s -33%
LP64 z3 ✅ 2s 3s -33%
mlk_ct_get_optblocker_u32 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_ct_memcmp LP64 bitwuzla* ✅ 2s 3s -33%
mlk_ct_sel_int16 LP64 z3* ✅ 1s 4s -75%
mlk_ct_sel_uint8 LP64 z3* ✅ 2s 2s +0%
mlk_enc_getnoise_eta1_eta2 LP64 z3* ✅ 3s 4s -25%
mlk_fqmul LP64 z3* ✅ 3s 20s -85%
mlk_gen_matrix LP64 z3* ✅ 6s 2s +200%
mlk_gen_matrix_serial LP64 z3* ✅ 4s 4s +0%
mlk_indcpa_dec LP64 z3* ✅ 18s 11s +64%
mlk_indcpa_enc LP64 z3_smt_only* ✅ 448s 402s +11%
mlk_indcpa_keypair_derand LP64 z3* ✅ 163s 176s -7%
mlk_invntt_layer LP64 z3* ✅ 6s 6s +0%
mlk_keccak_absorb_once LP64 bitwuzla* ✅ 3s 4s -25%
mlk_keccak_absorb_once_x4 LP64 bitwuzla* ✅ 7s 5s +40%
mlk_keccak_squeeze_once LP64 bitwuzla* ✅ 7s 10s -30%
mlk_keccak_squeezeblocks LP64 bitwuzla* ✅ 9s 9s +0%
mlk_keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 28s 26s +8%
mlk_keccakf1600_extract_bytes LP64 bitwuzla* ✅ 2s 2s +0%
mlk_keccakf1600_extract_bytes (big endian) LP64 bitwuzla* ✅ 2s 2s +0%
mlk_keccakf1600_permute LP64 z3* ✅ 5s 2s +150%
mlk_keccakf1600_permute_c LP64 z3* ✅ 3s 6s -50%
mlk_keccakf1600_xor_bytes LP64 bitwuzla* ✅ 1s 1s +0%
mlk_keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 3s 2s +50%
mlk_keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 2s 2s +0%
mlk_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 1s 3s -67%
mlk_keccakf1600x4_permute LP64 z3* ✅ 3s 2s +50%
mlk_keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 2s 2s +0%
mlk_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 2s 5s -60%
mlk_keypair_getnoise_eta1 LP64 z3* ✅ 1s 5s -80%
mlk_matvec_mul LP64 z3* ✅ 3s 5s -40%
mlk_montgomery_reduce LP64 z3* ✅ 2s 2s +0%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 303s 9s +3267%
mlk_ntt_layer LP64 z3* ✅ 7s 38s -82%
mlk_poly_add LP64 z3* ✅ 7s 5s +40%
mlk_poly_cbd_eta1 LP64 z3* ✅ 6s 3s +100%
mlk_poly_cbd_eta2 LP64 z3* ✅ 2s 3s -33%
mlk_poly_compress_d10 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_compress_d10_c LP64 z3* ✅ 2s 3s -33%
mlk_poly_compress_d10_native LP64 bitwuzla* ✅ 1s 3s -67%
mlk_poly_compress_d11 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_compress_d11_c LP64 z3* ✅ 3s 4s -25%
mlk_poly_compress_d11_native LP64 bitwuzla* ✅ 1s 3s -67%
mlk_poly_compress_d4 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_compress_d4_c LP64 z3* ✅ 2s 4s -50%
mlk_poly_compress_d4_native LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_compress_d5 LP64 bitwuzla* ✅ 3s 5s -40%
mlk_poly_compress_d5_c LP64 z3* ✅ 5s 4s +25%
mlk_poly_compress_d5_native LP64 bitwuzla* ✅ 4s 4s +0%
mlk_poly_compress_du LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_compress_dv LP64 bitwuzla* ✅ 2s 1s +100%
mlk_poly_decompress_d10 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_decompress_d10_c LP64 z3* ✅ 1s 2s -50%
mlk_poly_decompress_d10_native LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_decompress_d11 LP64 bitwuzla* ✅ 3s 3s +0%
mlk_poly_decompress_d11_c LP64 z3* ✅ 2s 2s +0%
mlk_poly_decompress_d11_native LP64 bitwuzla* ✅ 14s 16s -12%
mlk_poly_decompress_d4 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_decompress_d4_c LP64 z3* ✅ 1s 4s -75%
mlk_poly_decompress_d4_native LP64 bitwuzla* ✅ 4s 3s +33%
mlk_poly_decompress_d5 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_decompress_d5_c LP64 z3* ✅ 3s 2s +50%
mlk_poly_decompress_d5_native LP64 bitwuzla* ✅ 15s 18s -17%
mlk_poly_decompress_du LP64 bitwuzla* ✅ 2s 1s +100%
mlk_poly_decompress_dv LP64 bitwuzla* ✅ 1s 2s -50%
mlk_poly_frombytes LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_frombytes_c LP64 z3* ✅ 6s 3s +100%
mlk_poly_frombytes_native LP64 bitwuzla* ✅ 13s 10s +30%
mlk_poly_frommsg LP64 z3* ✅ 3s 10s -70%
mlk_poly_getnoise_eta1122_4x LP64 z3* ✅ 5s 3s +67%
mlk_poly_getnoise_eta1122_4x_serial LP64 z3* ✅ 1s - new
mlk_poly_getnoise_eta1_4x LP64 z3* ✅ 2s 2s +0%
mlk_poly_getnoise_eta1_4x_serial LP64 z3* ✅ 4s - new
mlk_poly_getnoise_eta2 LP64 z3* ✅ 1s 1s +0%
mlk_poly_invntt_tomont LP64 z3* ✅ 3s 3s +0%
mlk_poly_invntt_tomont_c LP64 z3* ✅ 4s 2s +100%
mlk_poly_mulcache_compute LP64 z3* ✅ 2s 2s +0%
mlk_poly_mulcache_compute_c LP64 z3* ✅ 3s 3s +0%
mlk_poly_mulcache_compute_native LP64 z3* ✅ 3s 3s +0%
mlk_poly_ntt LP64 bitwuzla* ✅ 8s 8s +0%
mlk_poly_ntt_c LP64 z3* ✅ 2s 1s +100%
mlk_poly_reduce LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_reduce_c LP64 z3* ✅ 2s 1s +100%
mlk_poly_reduce_native LP64 bitwuzla* ✅ 36s 40s -10%
mlk_poly_rej_uniform LP64 bitwuzla* ✅ 37s 161s -77%
mlk_poly_rej_uniform_x4 LP64 z3* ✅ 6s 7s -14%
mlk_poly_sub LP64 z3* ✅ 8s 8s +0%
mlk_poly_tobytes LP64 bitwuzla* ✅ 5s 3s +67%
mlk_poly_tobytes_c LP64 z3* ✅ 2s 4s -50%
mlk_poly_tobytes_native LP64 bitwuzla* ✅ 3s 1s +200%
mlk_poly_tomont LP64 z3* ✅ 3s 2s +50%
mlk_poly_tomont_c LP64 z3* ✅ 3s 3s +0%
mlk_poly_tomont_native LP64 z3* ✅ 1s 4s -75%
mlk_poly_tomsg LP64 bitwuzla* ✅ 4s 3s +33%
mlk_polymat_permute_bitrev_to_custom LP64 z3* ✅ 4s 5s -20%
mlk_polymat_permute_bitrev_to_custom_native LP64 z3* ✅ 110s - new
mlk_polyvec_add LP64 z3* ✅ 20s 18s +11%
mlk_polyvec_basemul_acc_montgomery_cached LP64 z3* ✅ 2s 2s +0%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ⚠️ 139s 79s +76%
mlk_polyvec_compress_du LP64 z3* ✅ 2s 3s -33%
mlk_polyvec_decompress_du LP64 z3* ✅ 4s 2s +100%
mlk_polyvec_frombytes LP64 z3* ✅ 2s 5s -60%
mlk_polyvec_invntt_tomont LP64 z3* ✅ 3s 1s +200%
mlk_polyvec_mulcache_compute LP64 z3* ✅ 2s 4s -50%
mlk_polyvec_ntt LP64 z3* ✅ 4s 12s -67%
mlk_polyvec_reduce LP64 z3* ✅ 2s 2s +0%
mlk_polyvec_tobytes LP64 z3* ✅ 2s 1s +100%
mlk_polyvec_tomont LP64 z3* ✅ 1s 2s -50%
mlk_rej_uniform LP64 bitwuzla* ✅ 1s 2s -50%
mlk_rej_uniform_c LP64 z3* ✅ 164s 144s +14%
mlk_scalar_compress_d1 LP64 z3* ✅ 2s 3s -33%
mlk_scalar_compress_d10 LP64 z3* ✅ 4s 2s +100%
mlk_scalar_compress_d11 LP64 z3* ✅ 1s 4s -75%
mlk_scalar_compress_d4 LP64 z3* ✅ 3s 1s +200%
mlk_scalar_compress_d5 LP64 z3* ✅ 2s 4s -50%
mlk_scalar_decompress_d10 LP64 z3* ✅ 3s 2s +50%
mlk_scalar_decompress_d11 LP64 z3* ✅ 3s 2s +50%
mlk_scalar_decompress_d4 LP64 z3* ✅ 3s 3s +0%
mlk_scalar_decompress_d5 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_signed_to_unsigned_q LP64 z3* ✅ 4s 3s +33%
mlk_sha3_256 LP64 bitwuzla* ✅ 3s 2s +50%
mlk_sha3_512 LP64 bitwuzla* ✅ 1s 1s +0%
mlk_shake128_absorb_once LP64 bitwuzla* ✅ 2s 2s +0%
mlk_shake128_squeezeblocks LP64 bitwuzla* ✅ 2s 1s +100%
mlk_shake128x4_absorb_once LP64 bitwuzla* ✅ 1s 2s -50%
mlk_shake128x4_squeezeblocks LP64 bitwuzla* ✅ 2s 2s +0%
mlk_shake256 LP64 bitwuzla* ✅ 1s 1s +0%
mlk_shake256x4 LP64 bitwuzla* ✅ 6s 4s +50%
mlk_value_barrier_i32 LP64 bitwuzla* ✅ 1s 3s -67%
mlk_value_barrier_u32 LP64 bitwuzla* ✅ 1s 3s -67%
mlk_value_barrier_u8 LP64 bitwuzla* ✅ 2s 1s +100%
ntt_native_aarch64 LP64 z3* ✅ 4s 3s +33%
ntt_native_x86_64 LP64 z3* ✅ 2s 2s +0%
nttunpack_native_x86_64 LP64 z3* ✅ 2s 2s +0%
poly_compress_d10_native_x86_64 LP64 bitwuzla* ✅ 3s 2s +50%
poly_compress_d11_native_x86_64 LP64 bitwuzla* ✅ 3s 3s +0%
poly_compress_d4_native_x86_64 LP64 bitwuzla* ✅ 2s 2s +0%
poly_compress_d5_native_x86_64 LP64 bitwuzla* ✅ 2s 4s -50%
poly_decompress_d10_native_x86_64 LP64 bitwuzla* ✅ 1s 4s -75%
poly_decompress_d11_native_x86_64 LP64 bitwuzla* ✅ 6s 5s +20%
poly_decompress_d4_native_x86_64 LP64 bitwuzla* ✅ 3s 2s +50%
poly_decompress_d5_native_x86_64 LP64 bitwuzla* ✅ 5s 5s +0%
poly_frombytes_native_x86_64 LP64 bitwuzla* ✅ 5s 5s +0%
poly_invntt_tomont_native LP64 z3* ✅ 2s 3s -33%
poly_mulcache_compute_native_aarch64 LP64 z3* ✅ 2s 3s -33%
poly_mulcache_compute_native_x86_64 LP64 z3* ✅ 1s 5s -80%
poly_ntt_native LP64 z3* ✅ 2s 43s -95%
poly_reduce_native_aarch64 LP64 z3* ✅ 2s 2s +0%
poly_reduce_native_x86_64 LP64 z3* ✅ 3s 3s +0%
poly_tobytes_native_aarch64 LP64 z3* ✅ 2s 3s -33%
poly_tobytes_native_x86_64 LP64 z3* ✅ 2s 3s -33%
poly_tomont_native_aarch64 LP64 z3* ✅ 2s 3s -33%
poly_tomont_native_x86_64 LP64 z3* ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k2_native_aarch64 LP64 z3* ✅ 2s 1s +100%
polyvec_basemul_acc_montgomery_cached_k2_native_x86_64 LP64 z3* ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k3_native_aarch64 LP64 z3* ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k3_native_x86_64 LP64 z3* ✅ 3s 2s +50%
polyvec_basemul_acc_montgomery_cached_k4_native_aarch64 LP64 z3* ✅ 1s 2s -50%
polyvec_basemul_acc_montgomery_cached_k4_native_x86_64 LP64 z3* ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_native LP64 z3* ✅ 29s 31s -6%
rej_uniform_native LP64 bitwuzla* ✅ 2s 1s +100%
rej_uniform_native_aarch64 LP64 z3* ✅ 41s 53s -23%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 120s 67s +79%
sys_check_capability LP64 z3* ✅ 4s 2s +100%

@oqs-bot

oqs-bot commented Oct 10, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-512)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 2203s 1614s +36.5%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 375s 9s +4067%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ⚠️ 85s 55s +55%
mlk_rej_uniform_c LP64 z3* ⚠️ 207s 135s +53%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 140s 57s +146%
Full Results (195 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 2203s 1614s +36.5%
intt_native_aarch64 LP64 z3* ✅ 2s 2s +0%
intt_native_x86_64 LP64 z3* ✅ 3s 2s +50%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 1s 2s -50%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 2s -50%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 4s 3s +33%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 3s 3s +0%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 2s 2s +0%
keccakf1600_permute_native LP64 bitwuzla* ✅ 3s 1s +200%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 2s 1s +100%
keccakf1600x4_permute_native_x4 LP64 bitwuzla* ✅ 16s 16s +0%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 1s 1s +0%
kem_check_pk LP64 z3* ✅ 5s 4s +25%
kem_check_sk LP64 z3* ✅ 2s 2s +0%
kem_dec LP64 z3* ✅ 10s 5s +100%
kem_enc LP64 z3* ✅ 3s 2s +50%
kem_enc_derand LP64 z3* ✅ 4s 3s +33%
kem_keypair LP64 z3* ✅ 2s 4s -50%
kem_keypair_derand LP64 z3* ✅ 3s 3s +0%
mlk_barrett_reduce LP64 z3* ✅ 3s 2s +50%
mlk_check_pct LP64 bitwuzla* ✅ 2s 5s -60%
mlk_ct_cmask_neg_i16 LP64 z3* ✅ 5s 3s +67%
mlk_ct_cmask_nonzero_u16 LP64 z3* ✅ 2s 2s +0%
mlk_ct_cmask_nonzero_u8 LP64 z3* ✅ 3s 1s +200%
mlk_ct_cmov_zero LP64 bitwuzla* ✅ 2s 3s -33%
mlk_ct_get_optblocker_i32 ILP32 bitwuzla ✅ 3s 2s +50%
ILP32 cvc5_arrays_exp ✅ 2s 2s +0%
ILP32 z3 ✅ 1s 2s -50%
LP64 bitwuzla* ✅ 1s 2s -50%
LP64 cvc5_arrays_exp ✅ 3s 2s +50%
LP64 z3 ✅ 2s 2s +0%
mlk_ct_get_optblocker_u32 LP64 bitwuzla* ✅ 3s 3s +0%
mlk_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_ct_memcmp LP64 bitwuzla* ✅ 2s 3s -33%
mlk_ct_sel_int16 LP64 z3* ✅ 2s 1s +100%
mlk_ct_sel_uint8 LP64 z3* ✅ 1s 2s -50%
mlk_enc_getnoise_eta1_eta2 LP64 z3* ✅ 4s 2s +100%
mlk_fqmul LP64 z3* ✅ 3s 17s -82%
mlk_gen_matrix LP64 z3* ✅ 4s 2s +100%
mlk_gen_matrix_serial LP64 z3* ✅ 3s 3s +0%
mlk_indcpa_dec LP64 z3* ✅ 19s 14s +36%
mlk_indcpa_enc LP64 z3_smt_only* ✅ 360s 255s +41%
mlk_indcpa_keypair_derand LP64 z3* ✅ 249s 213s +17%
mlk_invntt_layer LP64 z3* ✅ 9s 4s +125%
mlk_keccak_absorb_once LP64 bitwuzla* ✅ 4s 3s +33%
mlk_keccak_absorb_once_x4 LP64 bitwuzla* ✅ 6s 5s +20%
mlk_keccak_squeeze_once LP64 bitwuzla* ✅ 7s 8s -12%
mlk_keccak_squeezeblocks LP64 bitwuzla* ✅ 10s 9s +11%
mlk_keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 29s 26s +12%
mlk_keccakf1600_extract_bytes LP64 bitwuzla* ✅ 3s 2s +50%
mlk_keccakf1600_extract_bytes (big endian) LP64 bitwuzla* ✅ 2s 5s -60%
mlk_keccakf1600_permute LP64 z3* ✅ 2s 1s +100%
mlk_keccakf1600_permute_c LP64 z3* ✅ 4s 5s -20%
mlk_keccakf1600_xor_bytes LP64 bitwuzla* ✅ 2s 1s +100%
mlk_keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 2s 2s +0%
mlk_keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 2s 2s +0%
mlk_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 1s 3s -67%
mlk_keccakf1600x4_permute LP64 z3* ✅ 4s 4s +0%
mlk_keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 2s 2s +0%
mlk_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 1s 2s -50%
mlk_keypair_getnoise_eta1 LP64 z3* ✅ 1s 1s +0%
mlk_matvec_mul LP64 z3* ✅ 2s 3s -33%
mlk_montgomery_reduce LP64 z3* ✅ 1s 2s -50%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 375s 9s +4067%
mlk_ntt_layer LP64 z3* ✅ 8s 32s -75%
mlk_poly_add LP64 z3* ✅ 4s 4s +0%
mlk_poly_cbd_eta1 LP64 z3* ✅ 2s 2s +0%
mlk_poly_cbd_eta2 LP64 z3* ✅ 3s 3s +0%
mlk_poly_compress_d10 LP64 bitwuzla* ✅ 4s 4s +0%
mlk_poly_compress_d10_c LP64 z3* ✅ 2s 2s +0%
mlk_poly_compress_d10_native LP64 bitwuzla* ✅ 2s 1s +100%
mlk_poly_compress_d11 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_compress_d11_c LP64 z3* ✅ 3s 2s +50%
mlk_poly_compress_d11_native LP64 bitwuzla* ✅ 3s 3s +0%
mlk_poly_compress_d4 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_compress_d4_c LP64 z3* ✅ 1s 3s -67%
mlk_poly_compress_d4_native LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_compress_d5 LP64 bitwuzla* ✅ 1s 2s -50%
mlk_poly_compress_d5_c LP64 z3* ✅ 1s 3s -67%
mlk_poly_compress_d5_native LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_compress_du LP64 bitwuzla* ✅ 4s 3s +33%
mlk_poly_compress_dv LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_decompress_d10 LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_decompress_d10_c LP64 z3* ✅ 2s 4s -50%
mlk_poly_decompress_d10_native LP64 bitwuzla* ✅ 17s 15s +13%
mlk_poly_decompress_d11 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_decompress_d11_c LP64 z3* ✅ 4s 2s +100%
mlk_poly_decompress_d11_native LP64 bitwuzla* ✅ 3s 3s +0%
mlk_poly_decompress_d4 LP64 bitwuzla* ✅ 1s 3s -67%
mlk_poly_decompress_d4_c LP64 z3* ✅ 2s 7s -71%
mlk_poly_decompress_d4_native LP64 bitwuzla* ✅ 15s 14s +7%
mlk_poly_decompress_d5 LP64 bitwuzla* ✅ 2s 1s +100%
mlk_poly_decompress_d5_c LP64 z3* ✅ 2s 1s +100%
mlk_poly_decompress_d5_native LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_decompress_du LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_decompress_dv LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_frombytes LP64 bitwuzla* ✅ 3s 1s +200%
mlk_poly_frombytes_c LP64 z3* ✅ 4s 4s +0%
mlk_poly_frombytes_native LP64 bitwuzla* ✅ 12s 8s +50%
mlk_poly_frommsg LP64 z3* ✅ 2s 10s -80%
mlk_poly_getnoise_eta1122_4x LP64 z3* ✅ 3s 3s +0%
mlk_poly_getnoise_eta1122_4x_serial LP64 z3* ✅ 2s - new
mlk_poly_getnoise_eta1_4x LP64 z3* ✅ 2s 5s -60%
mlk_poly_getnoise_eta1_4x_serial LP64 z3* ✅ 6s - new
mlk_poly_getnoise_eta2 LP64 z3* ✅ 3s 3s +0%
mlk_poly_invntt_tomont LP64 z3* ✅ 1s 2s -50%
mlk_poly_invntt_tomont_c LP64 z3* ✅ 3s 3s +0%
mlk_poly_mulcache_compute LP64 z3* ✅ 2s 2s +0%
mlk_poly_mulcache_compute_c LP64 z3* ✅ 4s 4s +0%
mlk_poly_mulcache_compute_native LP64 z3* ✅ 3s 2s +50%
mlk_poly_ntt LP64 bitwuzla* ✅ 9s 5s +80%
mlk_poly_ntt_c LP64 z3* ✅ 3s 2s +50%
mlk_poly_reduce LP64 bitwuzla* ✅ 3s 1s +200%
mlk_poly_reduce_c LP64 z3* ✅ 4s 3s +33%
mlk_poly_reduce_native LP64 bitwuzla* ✅ 44s 35s +26%
mlk_poly_rej_uniform LP64 bitwuzla* ✅ 44s 150s -71%
mlk_poly_rej_uniform_x4 LP64 z3* ✅ 6s 8s -25%
mlk_poly_sub LP64 z3* ✅ 8s 6s +33%
mlk_poly_tobytes LP64 bitwuzla* ✅ 1s 3s -67%
mlk_poly_tobytes_c LP64 z3* ✅ 3s 3s +0%
mlk_poly_tobytes_native LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_tomont LP64 z3* ✅ 3s 1s +200%
mlk_poly_tomont_c LP64 z3* ✅ 2s 2s +0%
mlk_poly_tomont_native LP64 z3* ✅ 3s 2s +50%
mlk_poly_tomsg LP64 bitwuzla* ✅ 3s 3s +0%
mlk_polymat_permute_bitrev_to_custom LP64 z3* ✅ 2s 2s +0%
mlk_polymat_permute_bitrev_to_custom_native LP64 z3* ✅ 33s - new
mlk_polyvec_add LP64 z3* ✅ 11s 11s +0%
mlk_polyvec_basemul_acc_montgomery_cached LP64 z3* ✅ 2s 1s +100%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ⚠️ 85s 55s +55%
mlk_polyvec_compress_du LP64 z3* ✅ 2s 2s +0%
mlk_polyvec_decompress_du LP64 z3* ✅ 3s 2s +50%
mlk_polyvec_frombytes LP64 z3* ✅ 2s 2s +0%
mlk_polyvec_invntt_tomont LP64 z3* ✅ 1s 3s -67%
mlk_polyvec_mulcache_compute LP64 z3* ✅ 3s 5s -40%
mlk_polyvec_ntt LP64 z3* ✅ 2s 1s +100%
mlk_polyvec_reduce LP64 z3* ✅ 2s 2s +0%
mlk_polyvec_tobytes LP64 z3* ✅ 4s 3s +33%
mlk_polyvec_tomont LP64 z3* ✅ 4s 1s +300%
mlk_rej_uniform LP64 bitwuzla* ✅ 3s 5s -40%
mlk_rej_uniform_c LP64 z3* ⚠️ 207s 135s +53%
mlk_scalar_compress_d1 LP64 z3* ✅ 3s 2s +50%
mlk_scalar_compress_d10 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_compress_d11 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_compress_d4 LP64 z3* ✅ 1s 1s +0%
mlk_scalar_compress_d5 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_decompress_d10 LP64 z3* ✅ 3s 2s +50%
mlk_scalar_decompress_d11 LP64 z3* ✅ 1s 2s -50%
mlk_scalar_decompress_d4 LP64 z3* ✅ 2s 3s -33%
mlk_scalar_decompress_d5 LP64 z3* ✅ 2s 3s -33%
mlk_scalar_signed_to_unsigned_q LP64 z3* ✅ 1s 1s +0%
mlk_sha3_256 LP64 bitwuzla* ✅ 3s 2s +50%
mlk_sha3_512 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_shake128_absorb_once LP64 bitwuzla* ✅ 3s 3s +0%
mlk_shake128_squeezeblocks LP64 bitwuzla* ✅ 2s 3s -33%
mlk_shake128x4_absorb_once LP64 bitwuzla* ✅ 2s 2s +0%
mlk_shake128x4_squeezeblocks LP64 bitwuzla* ✅ 2s 1s +100%
mlk_shake256 LP64 bitwuzla* ✅ 3s 2s +50%
mlk_shake256x4 LP64 bitwuzla* ✅ 6s 5s +20%
mlk_value_barrier_i32 LP64 bitwuzla* ✅ 1s 2s -50%
mlk_value_barrier_u32 LP64 bitwuzla* ✅ 1s 3s -67%
mlk_value_barrier_u8 LP64 bitwuzla* ✅ 4s 4s +0%
ntt_native_aarch64 LP64 z3* ✅ 4s 2s +100%
ntt_native_x86_64 LP64 z3* ✅ 3s 2s +50%
nttunpack_native_x86_64 LP64 z3* ✅ 5s 2s +150%
poly_compress_d10_native_x86_64 LP64 bitwuzla* ✅ 2s 3s -33%
poly_compress_d11_native_x86_64 LP64 bitwuzla* ✅ 5s 2s +150%
poly_compress_d4_native_x86_64 LP64 bitwuzla* ✅ 3s 1s +200%
poly_compress_d5_native_x86_64 LP64 bitwuzla* ✅ 2s 2s +0%
poly_decompress_d10_native_x86_64 LP64 bitwuzla* ✅ 7s 9s -22%
poly_decompress_d11_native_x86_64 LP64 bitwuzla* ✅ 3s 1s +200%
poly_decompress_d4_native_x86_64 LP64 bitwuzla* ✅ 3s 4s -25%
poly_decompress_d5_native_x86_64 LP64 bitwuzla* ✅ 1s 2s -50%
poly_frombytes_native_x86_64 LP64 bitwuzla* ✅ 3s 5s -40%
poly_invntt_tomont_native LP64 z3* ✅ 3s 2s +50%
poly_mulcache_compute_native_aarch64 LP64 z3* ✅ 2s 3s -33%
poly_mulcache_compute_native_x86_64 LP64 z3* ✅ 5s 1s +400%
poly_ntt_native LP64 z3* ✅ 2s 45s -96%
poly_reduce_native_aarch64 LP64 z3* ✅ 5s 1s +400%
poly_reduce_native_x86_64 LP64 z3* ✅ 3s 2s +50%
poly_tobytes_native_aarch64 LP64 z3* ✅ 3s 2s +50%
poly_tobytes_native_x86_64 LP64 z3* ✅ 1s 1s +0%
poly_tomont_native_aarch64 LP64 z3* ✅ 4s 2s +100%
poly_tomont_native_x86_64 LP64 z3* ✅ 4s 2s +100%
polyvec_basemul_acc_montgomery_cached_k2_native_aarch64 LP64 z3* ✅ 3s 3s +0%
polyvec_basemul_acc_montgomery_cached_k2_native_x86_64 LP64 z3* ✅ 2s 3s -33%
polyvec_basemul_acc_montgomery_cached_k3_native_aarch64 LP64 z3* ✅ 3s 3s +0%
polyvec_basemul_acc_montgomery_cached_k3_native_x86_64 LP64 z3* ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k4_native_aarch64 LP64 z3* ✅ 1s 3s -67%
polyvec_basemul_acc_montgomery_cached_k4_native_x86_64 LP64 z3* ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_native LP64 z3* ✅ 10s 8s +25%
rej_uniform_native LP64 bitwuzla* ✅ 2s 1s +100%
rej_uniform_native_aarch64 LP64 z3* ✅ 46s 43s +7%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 140s 57s +146%
sys_check_capability LP64 z3* ✅ 1s 1s +0%

@mkannwischer
mkannwischer marked this pull request as ready for review October 10, 2026 19:30
@mkannwischer
mkannwischer requested a review from a team as a code owner October 10, 2026 19:30
hanno-becker
hanno-becker reviewed Oct 11, 2026
View reviewed changes
Comment thread README.md Outdated
hanno-becker
hanno-becker reviewed Oct 11, 2026
View reviewed changes
Comment thread SOUNDNESS.md
hanno-becker
hanno-becker reviewed Oct 11, 2026
View reviewed changes
Comment thread API-CONVENTIONS.md
hanno-becker
hanno-becker requested changes Oct 11, 2026
View reviewed changes

@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.

Those are good findings, but I think we need to do a bit more to either address or appropriately document the limitations.

@mkannwischer
API-CONVENTIONS: State that buffers must not overlap
8b86309 
All public API contracts require their buffers to be disjoint, but
this was not documented.

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
@mkannwischer
README: Document constant-time multiplication requirement
75b41e2 
The C code is only constant-time if multiplications are, which is not
the case on all targets.

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
@mkannwischer
README: Exclude unproven backends and debug code from the CBMC claim
0c0714e 
The backends for platforms other than AArch64 and x86_64 (e.g. the RVV
C code) and the debug code have no CBMC proofs, matching the scope
stated in SOUNDNESS.md.

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
@mkannwischer
SOUNDNESS: State the scope of the constant-time tests
825af92 
The valgrind constant-time tests only run on x86_64 and AArch64 in
the default configuration.

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
hanno-becker
hanno-becker approved these changes Oct 12, 2026
View reviewed changes

@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.

LGTM

@hanno-becker
hanno-becker added this pull request to the merge queue Oct 12, 2026
@github-merge-queue
github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Oct 12, 2026
@mkannwischer
mkannwischer added this pull request to the merge queue Oct 12, 2026
Merged via the queue into main with commit c2827a8 Oct 12, 2026
361 checks passed
@mkannwischer
mkannwischer deleted the doc-improvements branch October 12, 2026 22:31
@github-actions github-actions Bot mentioned this pull request Oct 12, 2026
Closed
@mkannwischer mkannwischer mentioned this pull request Oct 13, 2026
Merged
AppelJr pushed a commit to AppelJr/mldsa-native that referenced this pull request Oct 16, 2026
@mkannwischer @hanno-becker
Doc improvements
1f8ff64 
State in API-CONVENTIONS.md and mldsa_native.h that buffers passed to
the same function must not overlap, document that the C code assumes
constant-time 32x32->32 and 32x32->64 multiplication, and exclude the
Armv8.1-M backend and the debug code from the CBMC claim in the README,
as in mlkem-native.

Ports pq-code-package/mlkem-native#1935.
The SOUNDNESS.md change is not ported: mldsa-native's SOUNDNESS.md
defers to mlkem-native's analysis, which now includes it.

 - Resolves pq-code-package#1463

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@hanno-becker hanno-becker hanno-becker approved these changes

Assignees

No one assigned

Labels

needs-mldsa-native-port

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@mkannwischer @oqs-bot @hanno-becker