Skip to content

CBMC: Add functional spec for runtime bounds check - #1937

Closed
hanno-becker wants to merge 3 commits into
mainfrom
debug-cbmc
Closed

CBMC: Add functional spec for runtime bounds check#1937
hanno-becker wants to merge 3 commits into
mainfrom
debug-cbmc

Conversation

@hanno-becker

@hanno-becker hanno-becker commented Oct 12, 2026

Copy link
Copy Markdown
Contributor

No description provided.

@hanno-becker hanno-becker added enhancement New feature or request testing CBMC labels Oct 12, 2026
@hanno-becker
hanno-becker force-pushed the debug-cbmc branch 2 times, most recently from ee8422c to 030f4c1 Compare October 17, 2026 04:34
@hanno-becker
CBMC: Prove debug bounds logic
93e86ff 
`mlk_debug_check_bounds_report()` scans an `int16_t` array and reports
values outside exclusive bounds. Prove that its return value equals
`array_bound(ptr, 0, len, lower_bound_exclusive + 1,
upper_bound_exclusive)`. The loop invariant establishes the same claim
for each processed prefix. The `+ 1` conversion assumes
`lower_bound_exclusive < INT32_MAX`.

Also check the public bounds wrapper and assertion helper for safety.
Pass `file_len` through the debug APIs and require a nonempty fresh
range ending in a null byte. Macros pass `sizeof(__FILE__)`; harnesses
keep the inputs arbitrary. Use an explicit length because CBMC 6.11's
string predicates do not work with the current dynamic-frame pass.

CBMC's `vfprintf` model does not parse formats or inspect variadic
arguments. These proofs therefore do not establish memory safety or
output behavior of the real `fprintf`; they check only the surrounding
C code under CBMC's library model.

Declare `exit` in the shared data-model shims. Diagnostics, ordering,
and exit behavior are unchanged.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
@oqs-bot

oqs-bot commented Oct 17, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-512)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 2067s 1614s +28.1%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 300s 9s +3233%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 121s 57s +112%
Full Results (201 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 2067s 1614s +28.1%
intt_native_aarch64 LP64 z3* ✅ 3s 2s +50%
intt_native_x86_64 LP64 z3* ✅ 2s 2s +0%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 3s 2s +50%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 2s -50%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 3s 3s +0%
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* ✅ 2s 2s +0%
keccakf1600_permute_native LP64 bitwuzla* ✅ 1s 1s +0%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 1s 1s +0%
keccakf1600x4_permute_native_x4 LP64 bitwuzla* ✅ 15s 16s -6%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 3s 1s +200%
kem_check_pk LP64 z3* ✅ 1s 4s -75%
kem_check_sk LP64 z3* ✅ 2s 2s +0%
kem_dec LP64 z3* ✅ 10s 5s +100%
kem_enc LP64 z3* ✅ 2s 2s +0%
kem_enc_derand LP64 z3* ✅ 5s 3s +67%
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* ✅ 3s 3s +0%
mlk_ct_cmask_nonzero_u16 LP64 z3* ✅ 2s 2s +0%
mlk_ct_cmask_nonzero_u8 LP64 z3* ✅ 2s 1s +100%
mlk_ct_cmov_zero LP64 bitwuzla* ✅ 1s 3s -67%
mlk_ct_get_optblocker_i32 ILP32 bitwuzla ✅ 3s 2s +50%
ILP32 cvc5_arrays_exp ✅ 1s 2s -50%
ILP32 z3 ✅ 2s 2s +0%
LP64 bitwuzla* ✅ 3s 2s +50%
LP64 cvc5_arrays_exp ✅ 2s 2s +0%
LP64 z3 ✅ 1s 2s -50%
mlk_ct_get_optblocker_u32 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 4s 2s +100%
mlk_ct_memcmp LP64 bitwuzla* ✅ 4s 3s +33%
mlk_ct_sel_int16 LP64 z3* ✅ 2s 1s +100%
mlk_ct_sel_uint8 LP64 z3* ✅ 1s 2s -50%
mlk_debug_check_assert ILP32 z3 ✅ 2s - new
LP64 z3* ✅ 2s - new
mlk_debug_check_bounds ILP32 z3 ✅ 1s - new
LP64 z3* ✅ 1s - new
mlk_debug_check_bounds_report ILP32 z3 ✅ 173s - new
LP64 z3* ✅ 100s - new
mlk_enc_getnoise_eta1_eta2 LP64 z3* ✅ 3s 2s +50%
mlk_fqmul LP64 z3* ✅ 4s 17s -76%
mlk_gen_matrix LP64 z3* ✅ 3s 2s +50%
mlk_gen_matrix_serial LP64 z3* ✅ 2s 3s -33%
mlk_indcpa_dec LP64 z3* ✅ 17s 14s +21%
mlk_indcpa_enc LP64 z3_smt_only* ✅ 340s 255s +33%
mlk_indcpa_keypair_derand LP64 z3* ✅ 235s 213s +10%
mlk_invntt_layer LP64 z3* ✅ 8s 4s +100%
mlk_keccak_absorb_once LP64 bitwuzla* ✅ 5s 3s +67%
mlk_keccak_absorb_once_x4 LP64 bitwuzla* ✅ 5s 5s +0%
mlk_keccak_squeeze_once LP64 bitwuzla* ✅ 6s 8s -25%
mlk_keccak_squeezeblocks LP64 bitwuzla* ✅ 8s 9s -11%
mlk_keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 26s 26s +0%
mlk_keccakf1600_extract_bytes LP64 bitwuzla* ✅ 1s 2s -50%
mlk_keccakf1600_extract_bytes (big endian) LP64 bitwuzla* ✅ 4s 5s -20%
mlk_keccakf1600_permute LP64 z3* ✅ 3s 1s +200%
mlk_keccakf1600_permute_c LP64 z3* ✅ 5s 5s +0%
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* ✅ 2s 3s -33%
mlk_keccakf1600x4_permute LP64 z3* ✅ 2s 4s -50%
mlk_keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 3s 2s +50%
mlk_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 1s 2s -50%
mlk_keypair_getnoise_eta1 LP64 z3* ✅ 4s 1s +300%
mlk_matvec_mul LP64 z3* ✅ 1s 3s -67%
mlk_montgomery_reduce LP64 z3* ✅ 3s 2s +50%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 300s 9s +3233%
mlk_ntt_layer LP64 z3* ✅ 7s 32s -78%
mlk_poly_add LP64 z3* ✅ 5s 4s +25%
mlk_poly_cbd_eta1 LP64 z3* ✅ 2s 2s +0%
mlk_poly_cbd_eta2 LP64 z3* ✅ 2s 3s -33%
mlk_poly_compress_d10 LP64 bitwuzla* ✅ 2s 4s -50%
mlk_poly_compress_d10_c LP64 z3* ✅ 3s 2s +50%
mlk_poly_compress_d10_native LP64 bitwuzla* ✅ 4s 1s +300%
mlk_poly_compress_d11 LP64 bitwuzla* ✅ 3s 3s +0%
mlk_poly_compress_d11_c LP64 z3* ✅ 2s 2s +0%
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* ✅ 1s 3s -67%
mlk_poly_compress_d4_native LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_compress_d5 LP64 bitwuzla* ✅ 2s 2s +0%
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* ✅ 2s 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* ✅ 1s 4s -75%
mlk_poly_decompress_d10_native LP64 bitwuzla* ✅ 17s 15s +13%
mlk_poly_decompress_d11 LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_decompress_d11_c LP64 z3* ✅ 1s 2s -50%
mlk_poly_decompress_d11_native LP64 bitwuzla* ✅ 1s 3s -67%
mlk_poly_decompress_d4 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_decompress_d4_c LP64 z3* ✅ 2s 7s -71%
mlk_poly_decompress_d4_native LP64 bitwuzla* ✅ 12s 14s -14%
mlk_poly_decompress_d5 LP64 bitwuzla* ✅ 2s 1s +100%
mlk_poly_decompress_d5_c LP64 z3* ✅ 3s 1s +200%
mlk_poly_decompress_d5_native LP64 bitwuzla* ✅ 1s 2s -50%
mlk_poly_decompress_du LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_decompress_dv LP64 bitwuzla* ✅ 1s 2s -50%
mlk_poly_frombytes LP64 bitwuzla* ✅ 1s 1s +0%
mlk_poly_frombytes_c LP64 z3* ✅ 4s 4s +0%
mlk_poly_frombytes_native LP64 bitwuzla* ✅ 11s 8s +38%
mlk_poly_frommsg LP64 z3* ✅ 2s 10s -80%
mlk_poly_getnoise_eta1122_4x LP64 z3* ✅ 4s 3s +33%
mlk_poly_getnoise_eta1122_4x_serial LP64 z3* ✅ 5s - new
mlk_poly_getnoise_eta1_4x LP64 z3* ✅ 3s 5s -40%
mlk_poly_getnoise_eta1_4x_serial LP64 z3* ✅ 4s - 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* ✅ 2s 3s -33%
mlk_poly_mulcache_compute LP64 z3* ✅ 1s 2s -50%
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* ✅ 5s 5s +0%
mlk_poly_ntt_c LP64 z3* ✅ 2s 2s +0%
mlk_poly_reduce LP64 bitwuzla* ✅ 2s 1s +100%
mlk_poly_reduce_c LP64 z3* ✅ 2s 3s -33%
mlk_poly_reduce_native LP64 bitwuzla* ✅ 33s 35s -6%
mlk_poly_rej_uniform LP64 bitwuzla* ✅ 49s 150s -67%
mlk_poly_rej_uniform_x4 LP64 z3* ✅ 6s 8s -25%
mlk_poly_sub LP64 z3* ✅ 5s 6s -17%
mlk_poly_tobytes LP64 bitwuzla* ✅ 1s 3s -67%
mlk_poly_tobytes_c LP64 z3* ✅ 2s 3s -33%
mlk_poly_tobytes_native LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_tomont LP64 z3* ✅ 4s 1s +300%
mlk_poly_tomont_c LP64 z3* ✅ 3s 2s +50%
mlk_poly_tomont_native LP64 z3* ✅ 2s 2s +0%
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* ✅ 78s 55s +42%
mlk_polyvec_compress_du LP64 z3* ✅ 3s 2s +50%
mlk_polyvec_decompress_du LP64 z3* ✅ 4s 2s +100%
mlk_polyvec_frombytes LP64 z3* ✅ 1s 2s -50%
mlk_polyvec_invntt_tomont LP64 z3* ✅ 2s 3s -33%
mlk_polyvec_mulcache_compute LP64 z3* ✅ 3s 5s -40%
mlk_polyvec_ntt LP64 z3* ✅ 2s 1s +100%
mlk_polyvec_reduce LP64 z3* ✅ 3s 2s +50%
mlk_polyvec_tobytes LP64 z3* ✅ 2s 3s -33%
mlk_polyvec_tomont LP64 z3* ✅ 2s 1s +100%
mlk_rej_uniform LP64 bitwuzla* ✅ 2s 5s -60%
mlk_rej_uniform_c LP64 z3* ✅ 157s 135s +16%
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* ✅ 2s 2s +0%
mlk_scalar_decompress_d11 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_decompress_d4 LP64 z3* ✅ 1s 3s -67%
mlk_scalar_decompress_d5 LP64 z3* ✅ 2s 3s -33%
mlk_scalar_signed_to_unsigned_q LP64 z3* ✅ 3s 1s +200%
mlk_sha3_256 LP64 bitwuzla* ✅ 3s 2s +50%
mlk_sha3_512 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_shake128_absorb_once LP64 bitwuzla* ✅ 1s 3s -67%
mlk_shake128_squeezeblocks LP64 bitwuzla* ✅ 2s 3s -33%
mlk_shake128x4_absorb_once LP64 bitwuzla* ✅ 2s 2s +0%
mlk_shake128x4_squeezeblocks LP64 bitwuzla* ✅ 3s 1s +200%
mlk_shake256 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_shake256x4 LP64 bitwuzla* ✅ 5s 5s +0%
mlk_value_barrier_i32 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_value_barrier_u32 LP64 bitwuzla* ✅ 3s 3s +0%
mlk_value_barrier_u8 LP64 bitwuzla* ✅ 3s 4s -25%
ntt_native_aarch64 LP64 z3* ✅ 2s 2s +0%
ntt_native_x86_64 LP64 z3* ✅ 3s 2s +50%
nttunpack_native_x86_64 LP64 z3* ✅ 3s 2s +50%
poly_compress_d10_native_x86_64 LP64 bitwuzla* ✅ 3s 3s +0%
poly_compress_d11_native_x86_64 LP64 bitwuzla* ✅ 2s 2s +0%
poly_compress_d4_native_x86_64 LP64 bitwuzla* ✅ 5s 1s +400%
poly_compress_d5_native_x86_64 LP64 bitwuzla* ✅ 2s 2s +0%
poly_decompress_d10_native_x86_64 LP64 bitwuzla* ✅ 5s 9s -44%
poly_decompress_d11_native_x86_64 LP64 bitwuzla* ✅ 1s 1s +0%
poly_decompress_d4_native_x86_64 LP64 bitwuzla* ✅ 6s 4s +50%
poly_decompress_d5_native_x86_64 LP64 bitwuzla* ✅ 2s 2s +0%
poly_frombytes_native_x86_64 LP64 bitwuzla* ✅ 4s 5s -20%
poly_invntt_tomont_native LP64 z3* ✅ 3s 2s +50%
poly_mulcache_compute_native_aarch64 LP64 z3* ✅ 3s 3s +0%
poly_mulcache_compute_native_x86_64 LP64 z3* ✅ 2s 1s +100%
poly_ntt_native LP64 z3* ✅ 2s 45s -96%
poly_reduce_native_aarch64 LP64 z3* ✅ 2s 1s +100%
poly_reduce_native_x86_64 LP64 z3* ✅ 1s 2s -50%
poly_tobytes_native_aarch64 LP64 z3* ✅ 5s 2s +150%
poly_tobytes_native_x86_64 LP64 z3* ✅ 2s 1s +100%
poly_tomont_native_aarch64 LP64 z3* ✅ 2s 2s +0%
poly_tomont_native_x86_64 LP64 z3* ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k2_native_aarch64 LP64 z3* ✅ 2s 3s -33%
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* ✅ 4s 2s +100%
polyvec_basemul_acc_montgomery_cached_native LP64 z3* ✅ 7s 8s -12%
rej_uniform_native LP64 bitwuzla* ✅ 2s 1s +100%
rej_uniform_native_aarch64 LP64 z3* ✅ 47s 43s +9%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 121s 57s +112%
sys_check_capability LP64 z3* ✅ 2s 1s +100%

@oqs-bot

oqs-bot commented Oct 17, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-768)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 2453s 1645s +49.1%
mlk_indcpa_dec LP64 z3* ⚠️ 24s 10s +140%
mlk_indcpa_enc LP64 z3_smt_only* ⚠️ 516s 252s +105%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 327s 7s +4571%
mlk_poly_reduce_native LP64 bitwuzla* ⚠️ 51s 34s +50%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ⚠️ 107s 46s +133%
mlk_rej_uniform_c LP64 z3* ⚠️ 212s 114s +86%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 183s 55s +233%
Full Results (201 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 2453s 1645s +49.1%
intt_native_aarch64 LP64 z3* ✅ 2s 5s -60%
intt_native_x86_64 LP64 z3* ✅ 5s 3s +67%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 2s 1s +100%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 3s 3s +0%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 2s -50%
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* ✅ 1s 2s -50%
keccakf1600_permute_native LP64 bitwuzla* ✅ 2s 3s -33%
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* ✅ 4s 2s +100%
kem_check_sk LP64 z3* ✅ 2s 2s +0%
kem_dec LP64 z3* ✅ 7s 5s +40%
kem_enc LP64 z3* ✅ 3s 2s +50%
kem_enc_derand LP64 z3* ✅ 3s 3s +0%
kem_keypair LP64 z3* ✅ 2s 2s +0%
kem_keypair_derand LP64 z3* ✅ 4s 2s +100%
mlk_barrett_reduce LP64 z3* ✅ 2s 2s +0%
mlk_check_pct LP64 bitwuzla* ✅ 5s 3s +67%
mlk_ct_cmask_neg_i16 LP64 z3* ✅ 2s 3s -33%
mlk_ct_cmask_nonzero_u16 LP64 z3* ✅ 1s 4s -75%
mlk_ct_cmask_nonzero_u8 LP64 z3* ✅ 3s 4s -25%
mlk_ct_cmov_zero LP64 bitwuzla* ✅ 3s 3s +0%
mlk_ct_get_optblocker_i32 ILP32 bitwuzla ✅ 2s 1s +100%
ILP32 cvc5_arrays_exp ✅ 3s 1s +200%
ILP32 z3 ✅ 2s 1s +100%
LP64 bitwuzla* ✅ 3s 1s +200%
LP64 cvc5_arrays_exp ✅ 3s 1s +200%
LP64 z3 ✅ 2s 1s +100%
mlk_ct_get_optblocker_u32 LP64 bitwuzla* ✅ 1s 1s +0%
mlk_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_ct_memcmp LP64 bitwuzla* ✅ 2s 4s -50%
mlk_ct_sel_int16 LP64 z3* ✅ 2s 3s -33%
mlk_ct_sel_uint8 LP64 z3* ✅ 1s 1s +0%
mlk_debug_check_assert ILP32 z3 ✅ 1s - new
LP64 z3* ✅ 2s - new
mlk_debug_check_bounds ILP32 z3 ✅ 2s - new
LP64 z3* ✅ 2s - new
mlk_debug_check_bounds_report ILP32 z3 ✅ 234s - new
LP64 z3* ✅ 109s - new
mlk_enc_getnoise_eta1_eta2 LP64 z3* ✅ 3s 3s +0%
mlk_fqmul LP64 z3* ✅ 3s 16s -81%
mlk_gen_matrix LP64 z3* ✅ 4s 2s +100%
mlk_gen_matrix_serial LP64 z3* ✅ 4s 2s +100%
mlk_indcpa_dec LP64 z3* ⚠️ 24s 10s +140%
mlk_indcpa_enc LP64 z3_smt_only* ⚠️ 516s 252s +105%
mlk_indcpa_keypair_derand LP64 z3* ✅ 140s 318s -56%
mlk_invntt_layer LP64 z3* ✅ 5s 4s +25%
mlk_keccak_absorb_once LP64 bitwuzla* ✅ 4s 3s +33%
mlk_keccak_absorb_once_x4 LP64 bitwuzla* ✅ 7s 5s +40%
mlk_keccak_squeeze_once LP64 bitwuzla* ✅ 8s 7s +14%
mlk_keccak_squeezeblocks LP64 bitwuzla* ✅ 11s 8s +38%
mlk_keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 32s 24s +33%
mlk_keccakf1600_extract_bytes LP64 bitwuzla* ✅ 4s 4s +0%
mlk_keccakf1600_extract_bytes (big endian) LP64 bitwuzla* ✅ 3s 2s +50%
mlk_keccakf1600_permute LP64 z3* ✅ 3s 1s +200%
mlk_keccakf1600_permute_c LP64 z3* ✅ 5s 6s -17%
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* ✅ 3s 4s -25%
mlk_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 2s 2s +0%
mlk_keccakf1600x4_permute LP64 z3* ✅ 1s 4s -75%
mlk_keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 3s 2s +50%
mlk_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 2s 1s +100%
mlk_keypair_getnoise_eta1 LP64 z3* ✅ 3s 2s +50%
mlk_matvec_mul LP64 z3* ✅ 2s 4s -50%
mlk_montgomery_reduce LP64 z3* ✅ 2s 1s +100%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 327s 7s +4571%
mlk_ntt_layer LP64 z3* ✅ 9s 29s -69%
mlk_poly_add LP64 z3* ✅ 7s 7s +0%
mlk_poly_cbd_eta1 LP64 z3* ✅ 2s 1s +100%
mlk_poly_cbd_eta2 LP64 z3* ✅ 2s 2s +0%
mlk_poly_compress_d10 LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_compress_d10_c LP64 z3* ✅ 2s 2s +0%
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* ✅ 1s 1s +0%
mlk_poly_compress_d11_native LP64 bitwuzla* ✅ 2s 4s -50%
mlk_poly_compress_d4 LP64 bitwuzla* ✅ 4s 3s +33%
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* ✅ 3s 2s +50%
mlk_poly_compress_d5_c LP64 z3* ✅ 2s 1s +100%
mlk_poly_compress_d5_native LP64 bitwuzla* ✅ 1s 2s -50%
mlk_poly_compress_du LP64 bitwuzla* ✅ 3s 1s +200%
mlk_poly_compress_dv LP64 bitwuzla* ✅ 3s 1s +200%
mlk_poly_decompress_d10 LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_decompress_d10_c LP64 z3* ✅ 3s 1s +200%
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* ✅ 2s 3s -33%
mlk_poly_decompress_d11_native LP64 bitwuzla* ✅ 3s 1s +200%
mlk_poly_decompress_d4 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_decompress_d4_c LP64 z3* ✅ 4s 4s +0%
mlk_poly_decompress_d4_native LP64 bitwuzla* ✅ 14s 12s +17%
mlk_poly_decompress_d5 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_decompress_d5_c LP64 z3* ✅ 4s 3s +33%
mlk_poly_decompress_d5_native LP64 bitwuzla* ✅ 4s 3s +33%
mlk_poly_decompress_du LP64 bitwuzla* ✅ 3s 1s +200%
mlk_poly_decompress_dv LP64 bitwuzla* ✅ 1s 2s -50%
mlk_poly_frombytes LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_frombytes_c LP64 z3* ✅ 5s 4s +25%
mlk_poly_frombytes_native LP64 bitwuzla* ✅ 13s 8s +62%
mlk_poly_frommsg LP64 z3* ✅ 2s 9s -78%
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* ✅ 2s - new
mlk_poly_getnoise_eta2 LP64 z3* ✅ 2s 2s +0%
mlk_poly_invntt_tomont LP64 z3* ✅ 4s 4s +0%
mlk_poly_invntt_tomont_c LP64 z3* ✅ 1s 2s -50%
mlk_poly_mulcache_compute LP64 z3* ✅ 3s 2s +50%
mlk_poly_mulcache_compute_c LP64 z3* ✅ 4s 2s +100%
mlk_poly_mulcache_compute_native LP64 z3* ✅ 3s 1s +200%
mlk_poly_ntt LP64 bitwuzla* ✅ 10s 5s +100%
mlk_poly_ntt_c LP64 z3* ✅ 1s 1s +0%
mlk_poly_reduce LP64 bitwuzla* ✅ 1s 2s -50%
mlk_poly_reduce_c LP64 z3* ✅ 3s 3s +0%
mlk_poly_reduce_native LP64 bitwuzla* ⚠️ 51s 34s +50%
mlk_poly_rej_uniform LP64 bitwuzla* ✅ 41s 129s -68%
mlk_poly_rej_uniform_x4 LP64 z3* ✅ 6s 5s +20%
mlk_poly_sub LP64 z3* ✅ 8s 10s -20%
mlk_poly_tobytes LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_tobytes_c LP64 z3* ✅ 1s 1s +0%
mlk_poly_tobytes_native LP64 bitwuzla* ✅ 3s 1s +200%
mlk_poly_tomont LP64 z3* ✅ 3s 1s +200%
mlk_poly_tomont_c LP64 z3* ✅ 4s 3s +33%
mlk_poly_tomont_native LP64 z3* ✅ 2s 3s -33%
mlk_poly_tomsg LP64 bitwuzla* ✅ 2s 3s -33%
mlk_polymat_permute_bitrev_to_custom LP64 z3* ✅ 3s 3s +0%
mlk_polymat_permute_bitrev_to_custom_native LP64 z3* ✅ 72s - new
mlk_polyvec_add LP64 z3* ✅ 11s 12s -8%
mlk_polyvec_basemul_acc_montgomery_cached LP64 z3* ✅ 2s 4s -50%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ⚠️ 107s 46s +133%
mlk_polyvec_compress_du LP64 z3* ✅ 4s 1s +300%
mlk_polyvec_decompress_du LP64 z3* ✅ 4s 4s +0%
mlk_polyvec_frombytes LP64 z3* ✅ 1s 3s -67%
mlk_polyvec_invntt_tomont LP64 z3* ✅ 1s 1s +0%
mlk_polyvec_mulcache_compute LP64 z3* ✅ 3s 2s +50%
mlk_polyvec_ntt LP64 z3* ✅ 1s 4s -75%
mlk_polyvec_reduce LP64 z3* ✅ 2s 1s +100%
mlk_polyvec_tobytes LP64 z3* ✅ 2s 1s +100%
mlk_polyvec_tomont LP64 z3* ✅ 2s 1s +100%
mlk_rej_uniform LP64 bitwuzla* ✅ 2s 1s +100%
mlk_rej_uniform_c LP64 z3* ⚠️ 212s 114s +86%
mlk_scalar_compress_d1 LP64 z3* ✅ 1s 2s -50%
mlk_scalar_compress_d10 LP64 z3* ✅ 3s 2s +50%
mlk_scalar_compress_d11 LP64 z3* ✅ 2s 1s +100%
mlk_scalar_compress_d4 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_compress_d5 LP64 z3* ✅ 1s 1s +0%
mlk_scalar_decompress_d10 LP64 z3* ✅ 1s 2s -50%
mlk_scalar_decompress_d11 LP64 z3* ✅ 3s 3s +0%
mlk_scalar_decompress_d4 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_decompress_d5 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_signed_to_unsigned_q LP64 z3* ✅ 3s 5s -40%
mlk_sha3_256 LP64 bitwuzla* ✅ 1s 2s -50%
mlk_sha3_512 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_shake128_absorb_once LP64 bitwuzla* ✅ 2s 1s +100%
mlk_shake128_squeezeblocks LP64 bitwuzla* ✅ 2s 3s -33%
mlk_shake128x4_absorb_once LP64 bitwuzla* ✅ 3s 3s +0%
mlk_shake128x4_squeezeblocks LP64 bitwuzla* ✅ 2s 1s +100%
mlk_shake256 LP64 bitwuzla* ✅ 3s 2s +50%
mlk_shake256x4 LP64 bitwuzla* ✅ 5s 3s +67%
mlk_value_barrier_i32 LP64 bitwuzla* ✅ 1s 2s -50%
mlk_value_barrier_u32 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_value_barrier_u8 LP64 bitwuzla* ✅ 1s 2s -50%
ntt_native_aarch64 LP64 z3* ✅ 4s 3s +33%
ntt_native_x86_64 LP64 z3* ✅ 1s 3s -67%
nttunpack_native_x86_64 LP64 z3* ✅ 2s 3s -33%
poly_compress_d10_native_x86_64 LP64 bitwuzla* ✅ 2s 5s -60%
poly_compress_d11_native_x86_64 LP64 bitwuzla* ✅ 4s 3s +33%
poly_compress_d4_native_x86_64 LP64 bitwuzla* ✅ 2s 3s -33%
poly_compress_d5_native_x86_64 LP64 bitwuzla* ✅ 1s 2s -50%
poly_decompress_d10_native_x86_64 LP64 bitwuzla* ✅ 6s 5s +20%
poly_decompress_d11_native_x86_64 LP64 bitwuzla* ✅ 2s 1s +100%
poly_decompress_d4_native_x86_64 LP64 bitwuzla* ✅ 5s 6s -17%
poly_decompress_d5_native_x86_64 LP64 bitwuzla* ✅ 3s 4s -25%
poly_frombytes_native_x86_64 LP64 bitwuzla* ✅ 4s 5s -20%
poly_invntt_tomont_native LP64 z3* ✅ 4s 2s +100%
poly_mulcache_compute_native_aarch64 LP64 z3* ✅ 2s 6s -67%
poly_mulcache_compute_native_x86_64 LP64 z3* ✅ 4s 3s +33%
poly_ntt_native LP64 z3* ✅ 3s 39s -92%
poly_reduce_native_aarch64 LP64 z3* ✅ 3s 2s +50%
poly_reduce_native_x86_64 LP64 z3* ✅ 3s 2s +50%
poly_tobytes_native_aarch64 LP64 z3* ✅ 2s 1s +100%
poly_tobytes_native_x86_64 LP64 z3* ✅ 1s 3s -67%
poly_tomont_native_aarch64 LP64 z3* ✅ 3s 1s +200%
poly_tomont_native_x86_64 LP64 z3* ✅ 4s 1s +300%
polyvec_basemul_acc_montgomery_cached_k2_native_aarch64 LP64 z3* ✅ 2s 3s -33%
polyvec_basemul_acc_montgomery_cached_k2_native_x86_64 LP64 z3* ✅ 4s 4s +0%
polyvec_basemul_acc_montgomery_cached_k3_native_aarch64 LP64 z3* ✅ 4s 2s +100%
polyvec_basemul_acc_montgomery_cached_k3_native_x86_64 LP64 z3* ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k4_native_aarch64 LP64 z3* ✅ 3s 1s +200%
polyvec_basemul_acc_montgomery_cached_k4_native_x86_64 LP64 z3* ✅ 1s 2s -50%
polyvec_basemul_acc_montgomery_cached_native LP64 z3* ✅ 19s 14s +36%
rej_uniform_native LP64 bitwuzla* ✅ 3s 2s +50%
rej_uniform_native_aarch64 LP64 z3* ✅ 54s 45s +20%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 183s 55s +233%
sys_check_capability LP64 z3* ✅ 3s 3s +0%

@oqs-bot

oqs-bot commented Oct 17, 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* ⚠️ 325s 9s +3511%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 104s 67s +55%
Full Results (201 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 2331s 1885s +23.7%
intt_native_aarch64 LP64 z3* ✅ 2s 3s -33%
intt_native_x86_64 LP64 z3* ✅ 5s 2s +150%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 2s 1s +100%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 5s 3s +67%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 3s 3s +0%
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* ✅ 19s 15s +27%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 2s 2s +0%
kem_check_pk LP64 z3* ✅ 3s 4s -25%
kem_check_sk LP64 z3* ✅ 4s 3s +33%
kem_dec LP64 z3* ✅ 9s 5s +80%
kem_enc LP64 z3* ✅ 2s 2s +0%
kem_enc_derand LP64 z3* ✅ 3s 3s +0%
kem_keypair LP64 z3* ✅ 4s 2s +100%
kem_keypair_derand LP64 z3* ✅ 2s 1s +100%
mlk_barrett_reduce LP64 z3* ✅ 2s 2s +0%
mlk_check_pct LP64 bitwuzla* ✅ 4s 1s +300%
mlk_ct_cmask_neg_i16 LP64 z3* ✅ 1s 3s -67%
mlk_ct_cmask_nonzero_u16 LP64 z3* ✅ 1s 2s -50%
mlk_ct_cmask_nonzero_u8 LP64 z3* ✅ 4s 1s +300%
mlk_ct_cmov_zero LP64 bitwuzla* ✅ 2s 3s -33%
mlk_ct_get_optblocker_i32 ILP32 bitwuzla ✅ 2s 3s -33%
ILP32 cvc5_arrays_exp ✅ 3s 3s +0%
ILP32 z3 ✅ 2s 3s -33%
LP64 bitwuzla* ✅ 1s 3s -67%
LP64 cvc5_arrays_exp ✅ 2s 3s -33%
LP64 z3 ✅ 3s 3s +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* ✅ 4s 3s +33%
mlk_ct_sel_int16 LP64 z3* ✅ 3s 4s -25%
mlk_ct_sel_uint8 LP64 z3* ✅ 3s 2s +50%
mlk_debug_check_assert ILP32 z3 ✅ 2s - new
LP64 z3* ✅ 1s - new
mlk_debug_check_bounds ILP32 z3 ✅ 3s - new
LP64 z3* ✅ 2s - new
mlk_debug_check_bounds_report ILP32 z3 ✅ 174s - new
LP64 z3* ✅ 96s - new
mlk_enc_getnoise_eta1_eta2 LP64 z3* ✅ 3s 4s -25%
mlk_fqmul LP64 z3* ✅ 4s 20s -80%
mlk_gen_matrix LP64 z3* ✅ 4s 2s +100%
mlk_gen_matrix_serial LP64 z3* ✅ 5s 4s +25%
mlk_indcpa_dec LP64 z3* ✅ 16s 11s +45%
mlk_indcpa_enc LP64 z3_smt_only* ✅ 498s 402s +24%
mlk_indcpa_keypair_derand LP64 z3* ✅ 164s 176s -7%
mlk_invntt_layer LP64 z3* ✅ 5s 6s -17%
mlk_keccak_absorb_once LP64 bitwuzla* ✅ 2s 4s -50%
mlk_keccak_absorb_once_x4 LP64 bitwuzla* ✅ 6s 5s +20%
mlk_keccak_squeeze_once LP64 bitwuzla* ✅ 7s 10s -30%
mlk_keccak_squeezeblocks LP64 bitwuzla* ✅ 9s 9s +0%
mlk_keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 23s 26s -12%
mlk_keccakf1600_extract_bytes LP64 bitwuzla* ✅ 2s 2s +0%
mlk_keccakf1600_extract_bytes (big endian) LP64 bitwuzla* ✅ 3s 2s +50%
mlk_keccakf1600_permute LP64 z3* ✅ 1s 2s -50%
mlk_keccakf1600_permute_c LP64 z3* ✅ 8s 6s +33%
mlk_keccakf1600_xor_bytes LP64 bitwuzla* ✅ 4s 1s +300%
mlk_keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 3s 2s +50%
mlk_keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 4s 2s +100%
mlk_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 1s 3s -67%
mlk_keccakf1600x4_permute LP64 z3* ✅ 2s 2s +0%
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* ✅ 2s 5s -60%
mlk_matvec_mul LP64 z3* ✅ 3s 5s -40%
mlk_montgomery_reduce LP64 z3* ✅ 2s 2s +0%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 325s 9s +3511%
mlk_ntt_layer LP64 z3* ✅ 7s 38s -82%
mlk_poly_add LP64 z3* ✅ 5s 5s +0%
mlk_poly_cbd_eta1 LP64 z3* ✅ 4s 3s +33%
mlk_poly_cbd_eta2 LP64 z3* ✅ 1s 3s -67%
mlk_poly_compress_d10 LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_compress_d10_c LP64 z3* ✅ 3s 3s +0%
mlk_poly_compress_d10_native LP64 bitwuzla* ✅ 3s 3s +0%
mlk_poly_compress_d11 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_compress_d11_c LP64 z3* ✅ 2s 4s -50%
mlk_poly_compress_d11_native LP64 bitwuzla* ✅ 1s 3s -67%
mlk_poly_compress_d4 LP64 bitwuzla* ✅ 1s 3s -67%
mlk_poly_compress_d4_c LP64 z3* ✅ 2s 4s -50%
mlk_poly_compress_d4_native LP64 bitwuzla* ✅ 1s 2s -50%
mlk_poly_compress_d5 LP64 bitwuzla* ✅ 2s 5s -60%
mlk_poly_compress_d5_c LP64 z3* ✅ 2s 4s -50%
mlk_poly_compress_d5_native LP64 bitwuzla* ✅ 1s 4s -75%
mlk_poly_compress_du LP64 bitwuzla* ✅ 4s 2s +100%
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* ✅ 3s 2s +50%
mlk_poly_decompress_d10_native LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_decompress_d11 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_decompress_d11_c LP64 z3* ✅ 2s 2s +0%
mlk_poly_decompress_d11_native LP64 bitwuzla* ✅ 16s 16s +0%
mlk_poly_decompress_d4 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_decompress_d4_c LP64 z3* ✅ 2s 4s -50%
mlk_poly_decompress_d4_native LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_decompress_d5 LP64 bitwuzla* ✅ 3s 3s +0%
mlk_poly_decompress_d5_c LP64 z3* ✅ 3s 2s +50%
mlk_poly_decompress_d5_native LP64 bitwuzla* ✅ 12s 18s -33%
mlk_poly_decompress_du LP64 bitwuzla* ✅ 2s 1s +100%
mlk_poly_decompress_dv LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_frombytes LP64 bitwuzla* ✅ 4s 2s +100%
mlk_poly_frombytes_c LP64 z3* ✅ 7s 3s +133%
mlk_poly_frombytes_native LP64 bitwuzla* ✅ 12s 10s +20%
mlk_poly_frommsg LP64 z3* ✅ 1s 10s -90%
mlk_poly_getnoise_eta1122_4x LP64 z3* ✅ 2s 3s -33%
mlk_poly_getnoise_eta1122_4x_serial LP64 z3* ✅ 3s - 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* ✅ 2s 3s -33%
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 3s +0%
mlk_poly_mulcache_compute_native LP64 z3* ✅ 1s 3s -67%
mlk_poly_ntt LP64 bitwuzla* ✅ 8s 8s +0%
mlk_poly_ntt_c LP64 z3* ✅ 3s 1s +200%
mlk_poly_reduce LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_reduce_c LP64 z3* ✅ 1s 1s +0%
mlk_poly_reduce_native LP64 bitwuzla* ✅ 35s 40s -12%
mlk_poly_rej_uniform LP64 bitwuzla* ✅ 38s 161s -76%
mlk_poly_rej_uniform_x4 LP64 z3* ✅ 7s 7s +0%
mlk_poly_sub LP64 z3* ✅ 6s 8s -25%
mlk_poly_tobytes LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_tobytes_c LP64 z3* ✅ 3s 4s -25%
mlk_poly_tobytes_native LP64 bitwuzla* ✅ 4s 1s +300%
mlk_poly_tomont LP64 z3* ✅ 4s 2s +100%
mlk_poly_tomont_c LP64 z3* ✅ 2s 3s -33%
mlk_poly_tomont_native LP64 z3* ✅ 5s 4s +25%
mlk_poly_tomsg LP64 bitwuzla* ✅ 2s 3s -33%
mlk_polymat_permute_bitrev_to_custom LP64 z3* ✅ 3s 5s -40%
mlk_polymat_permute_bitrev_to_custom_native LP64 z3* ✅ 99s - new
mlk_polyvec_add LP64 z3* ✅ 16s 18s -11%
mlk_polyvec_basemul_acc_montgomery_cached LP64 z3* ✅ 2s 2s +0%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ✅ 117s 79s +48%
mlk_polyvec_compress_du LP64 z3* ✅ 3s 3s +0%
mlk_polyvec_decompress_du LP64 z3* ✅ 4s 2s +100%
mlk_polyvec_frombytes LP64 z3* ✅ 4s 5s -20%
mlk_polyvec_invntt_tomont LP64 z3* ✅ 2s 1s +100%
mlk_polyvec_mulcache_compute LP64 z3* ✅ 2s 4s -50%
mlk_polyvec_ntt LP64 z3* ✅ 3s 12s -75%
mlk_polyvec_reduce LP64 z3* ✅ 4s 2s +100%
mlk_polyvec_tobytes LP64 z3* ✅ 2s 1s +100%
mlk_polyvec_tomont LP64 z3* ✅ 3s 2s +50%
mlk_rej_uniform LP64 bitwuzla* ✅ 1s 2s -50%
mlk_rej_uniform_c LP64 z3* ✅ 179s 144s +24%
mlk_scalar_compress_d1 LP64 z3* ✅ 1s 3s -67%
mlk_scalar_compress_d10 LP64 z3* ✅ 1s 2s -50%
mlk_scalar_compress_d11 LP64 z3* ✅ 2s 4s -50%
mlk_scalar_compress_d4 LP64 z3* ✅ 3s 1s +200%
mlk_scalar_compress_d5 LP64 z3* ✅ 2s 4s -50%
mlk_scalar_decompress_d10 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_decompress_d11 LP64 z3* ✅ 1s 2s -50%
mlk_scalar_decompress_d4 LP64 z3* ✅ 3s 3s +0%
mlk_scalar_decompress_d5 LP64 z3* ✅ 3s 2s +50%
mlk_scalar_signed_to_unsigned_q LP64 z3* ✅ 1s 3s -67%
mlk_sha3_256 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_sha3_512 LP64 bitwuzla* ✅ 4s 1s +300%
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* ✅ 3s 2s +50%
mlk_shake256 LP64 bitwuzla* ✅ 1s 1s +0%
mlk_shake256x4 LP64 bitwuzla* ✅ 4s 4s +0%
mlk_value_barrier_i32 LP64 bitwuzla* ✅ 4s 3s +33%
mlk_value_barrier_u32 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_value_barrier_u8 LP64 bitwuzla* ✅ 2s 1s +100%
ntt_native_aarch64 LP64 z3* ✅ 2s 3s -33%
ntt_native_x86_64 LP64 z3* ✅ 3s 2s +50%
nttunpack_native_x86_64 LP64 z3* ✅ 1s 2s -50%
poly_compress_d10_native_x86_64 LP64 bitwuzla* ✅ 2s 2s +0%
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* ✅ 3s 4s -25%
poly_decompress_d10_native_x86_64 LP64 bitwuzla* ✅ 2s 4s -50%
poly_decompress_d11_native_x86_64 LP64 bitwuzla* ✅ 4s 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* ✅ 6s 5s +20%
poly_invntt_tomont_native LP64 z3* ✅ 1s 3s -67%
poly_mulcache_compute_native_aarch64 LP64 z3* ✅ 3s 3s +0%
poly_mulcache_compute_native_x86_64 LP64 z3* ✅ 3s 5s -40%
poly_ntt_native LP64 z3* ✅ 2s 43s -95%
poly_reduce_native_aarch64 LP64 z3* ✅ 2s 2s +0%
poly_reduce_native_x86_64 LP64 z3* ✅ 2s 3s -33%
poly_tobytes_native_aarch64 LP64 z3* ✅ 3s 3s +0%
poly_tobytes_native_x86_64 LP64 z3* ✅ 2s 3s -33%
poly_tomont_native_aarch64 LP64 z3* ✅ 3s 3s +0%
poly_tomont_native_x86_64 LP64 z3* ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k2_native_aarch64 LP64 z3* ✅ 1s 1s +0%
polyvec_basemul_acc_montgomery_cached_k2_native_x86_64 LP64 z3* ✅ 3s 2s +50%
polyvec_basemul_acc_montgomery_cached_k3_native_aarch64 LP64 z3* ✅ 4s 2s +100%
polyvec_basemul_acc_montgomery_cached_k3_native_x86_64 LP64 z3* ✅ 4s 2s +100%
polyvec_basemul_acc_montgomery_cached_k4_native_aarch64 LP64 z3* ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k4_native_x86_64 LP64 z3* ✅ 3s 2s +50%
polyvec_basemul_acc_montgomery_cached_native LP64 z3* ✅ 27s 31s -13%
rej_uniform_native LP64 bitwuzla* ✅ 5s 1s +400%
rej_uniform_native_aarch64 LP64 z3* ✅ 41s 53s -23%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 104s 67s +55%
sys_check_capability LP64 z3* ✅ 2s 2s +0%

@hanno-becker
RV64: Remove m2 debug helper and guard m1 spill
51d5701 
RVV debug bounds checks spill active vector lanes into scalar arrays
before calling the generic checker. In-tree assertions use only the m1
adapter; the m2 helper and macros have no callers. The m1 adapter sizes
its buffer to `MLKEM_N` but does not check `vl` before the vector store.

Remove the m2 function, macros, and generated single-compilation-unit
undefinitions. Assert `vl <= MLKEM_N` before `__riscv_vse16_v_i16m1`.
Include `riscv_vector.h` in the debug-only header branch. Preserve the
compilation-unit guard and give `MLKEM_DEBUG` priority over `CBMC`,
as the scalar helpers do. The CBMC-only vector macros remain no-ops.

Pass `file_len` through the remaining m1 adapter so calls to the scalar
debug helpers preserve their bounded filename contracts. Its macro
passes `sizeof(__FILE__)`.

Contract lint finds proofs by directory name. The bounds reporter and
wrapper previously shared `debug_check_bounds`, so the reporter had no
matching proof directory and lint rejected its contract.

Give `mlk_debug_check_bounds_report` its own harness and proof
directory. Keep `debug_check_bounds` for the wrapper and use the
reporter's contract there. Both proofs retain the existing LP64 and
ILP32 configurations and CBMC library model.

Keep `MLKEM_DEBUG` enabled in the scalar debug-helper proofs so they
compile the runtime implementations rather than the assertion macros
used by ordinary CBMC proofs.

The debug proofs include native stdio headers. On Linux, Nix enables
glibc's fortified `fprintf` wrapper, whose `__builtin_va_arg_pack` call
has no CBMC model. The assertion and bounds-reporter proofs therefore
fail when they take a diagnostic path.

Disable `fortify` in the CBMC Nix shell to retain calls to the modeled
libc functions. Keep hardening in other shells unchanged.

CBMC's `fprintf` model does not inspect variadic arguments. These scalar
proofs do not establish memory safety or output behavior of the real
`fprintf`, or cover the RVV store intrinsic.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
@hanno-becker
hanno-becker marked this pull request as ready for review October 19, 2026 19:43
@hanno-becker
hanno-becker requested a review from a team as a code owner October 19, 2026 19:43
@hanno-becker
CBMC: Include scalar debug helpers in coverage docs
e76f0dc 
The README excludes all debug code from the CBMC safety claim, even
though dedicated proofs now cover the scalar helpers.

Remove that exclusion from both coverage statements. State in
`SOUNDNESS.md` that the proofs use libc models which do not parse
`fprintf` formats or inspect variadic arguments, and therefore do not
establish safety or output behavior of real formatted diagnostics.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
mkannwischer
mkannwischer requested changes Oct 22, 2026
View reviewed changes

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

Thanks @hanno-becker. Are you sure that the value added by this PR justifies the added complexity? A few things definitely have to be addressed before we can merge it.

Comment thread mlkem/src/debug.c
Comment on lines +20 to +23
* Spell out C-string validity using a length because CBMC 6.11 ignores
* __CPROVER_is_cstring and ignores __CPROVER_is_zero_string without string
* abstraction. String abstraction is incompatible with the dynamic-frame
* contract pass used by these proofs.

@mkannwischer mkannwischer Oct 22, 2026

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.

Should this be a TODO with a corresponding issue? If this is unlikely to be fixed in 6.12 maybe trim down the comment as I can see this going stale very quickly otherwise.

Comment thread flake.nix
Comment on lines +132 to +134
# Fortified glibc stdio wrappers use __builtin_va_arg_pack, which
# CBMC does not model. Keep the calls to the modeled libc functions.
hardeningDisable = [ "fortify" ];

@mkannwischer mkannwischer Oct 22, 2026

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.

I'm not very happy about this introduction of complexity.
This also means that it will only work in the cbmc development shell and will fail in the default shell. That definitely needs to be fixed.

Comment thread proofs/cbmc/debug_check_assert/Makefile
USE_DYNAMIC_FRAMES = 1

# Supported CBMC configurations
CBMC_SUPPORTED_CONFIGS = LP64:z3 ILP32:z3

@mkannwischer mkannwischer Oct 22, 2026

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.

This proof fails for me with

make clean && CBMC_DM=ILP32 make result

That likely means this never runs in CI which is bad.

Comment thread mlkem/src/debug.c
int valid = 1;
unsigned i;

(void)file_len;

@mkannwischer mkannwischer Oct 22, 2026

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.

What's this file_len argument for? it seems it's never used anyway?

@hanno-becker

hanno-becker commented Oct 22, 2026

Copy link
Copy Markdown
Contributor Author

@mkannwischer I think your question is fair, yes. Until we find a more convincing solution, we can close the PR.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@mkannwischer mkannwischer mkannwischer requested changes

Assignees

No one assigned

Labels

CBMC enhancement New feature or request needs-mldsa-native-port testing

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@hanno-becker @oqs-bot @mkannwischer