Use gcc and minimal libc headers for all CBMC proofs by rod-chapman · Pull Request #1879 · pq-code-package/mlkem-native

rod-chapman · 2026-08-24T15:53:11Z

CBMC Makefile.common now always uses gcc for pre-processing.
Specify -nostdinc for pre-processing, so host-dependent include files are NOT used, since this leads to proof instability across platforms.
Instead, specify and add our own minimal set the the standard LibC header files, but only what we need for mlkem-native and nothing else, all based solely on what is required by ISO C99 (7.17 - 7.21)
First two sets of header files are for

4.1. The "LP64" data model, where "Long and Pointers are 64 bits", which is that used by common 64-bit platforms such as AArch64/Linux, x86_64/Linux and AArch64/macOS.

4.2. The "ILP32" data model, for 32-bit systems such as 32-bit ARM, RV32, and most embedded 32-bit microcontrollers.

A third set of headers for the LLP64 (64-bit Windows) will follow.
Environment variable CBMC_DM controls selection of the data-model in Makefile.common. It defaults to "LP64"
Update four proofs to use Z3 instead of bitwuzla, which turn out to be more efficient with CBMC 6.11 and these header files.

oqs-bot · 2026-08-24T16:52:01Z

CBMC Results (ML-KEM-1024)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`mlk_ntt_butterfly_block`	⚠️	287s	9s	+3089%
`mlk_polyvec_basemul_acc_montgomery_cached_c`	⚠️	123s	79s	+56%

Full Results (191 proofs)

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

oqs-bot · 2026-08-24T16:53:43Z

CBMC Results (ML-KEM-768)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`mlk_indcpa_dec`	⚠️	21s	10s	+110%
`mlk_ntt_butterfly_block`	⚠️	253s	7s	+3514%

Full Results (191 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	1658s	1645s	+0.8%
`mlk_indcpa_enc`	✅	338s	252s	+34%
`mlk_ntt_butterfly_block`	⚠️	253s	7s	+3514%
`mlk_rej_uniform_c`	✅	143s	114s	+25%
`mlk_indcpa_keypair_derand`	✅	140s	318s	-56%
`mlk_polyvec_basemul_acc_montgomery_cached_c`	✅	68s	46s	+48%
`rej_uniform_native_aarch64`	✅	41s	45s	-9%
`rej_uniform_native_x86_64`	✅	36s	55s	-35%
`mlk_poly_rej_uniform`	✅	33s	129s	-74%
`mlk_poly_reduce_native`	✅	31s	34s	-9%
`mlk_keccak_squeezeblocks_x4`	✅	23s	24s	-4%
`mlk_indcpa_dec`	⚠️	21s	10s	+110%
`polyvec_basemul_acc_montgomery_cached_native`	✅	19s	14s	+36%
`keccakf1600x4_permute_native_x4`	✅	17s	21s	-19%
`mlk_poly_decompress_d4_native`	✅	16s	12s	+33%
`mlk_poly_decompress_d10_native`	✅	14s	15s	-7%
`mlk_polyvec_add`	✅	10s	12s	-17%
`mlk_poly_rej_uniform_x4`	✅	9s	5s	+80%
`mlk_keccak_absorb_once_x4`	✅	7s	5s	+40%
`mlk_keccak_squeeze_once`	✅	7s	7s	+0%
`mlk_poly_frombytes_native`	✅	7s	8s	-12%
`mlk_poly_ntt`	✅	7s	5s	+40%
`mlk_poly_sub`	✅	7s	10s	-30%
`kem_dec`	✅	6s	5s	+20%
`mlk_gen_matrix_serial`	✅	6s	2s	+200%
`mlk_keccak_squeezeblocks`	✅	6s	8s	-25%
`mlk_ntt_layer`	✅	6s	29s	-79%
`mlk_poly_getnoise_eta2`	✅	6s	2s	+200%
`mlk_shake256x4`	✅	6s	3s	+100%
`mlk_check_pct`	✅	5s	3s	+67%
`mlk_invntt_layer`	✅	5s	4s	+25%
`mlk_keccakf1600_permute_c`	✅	5s	6s	-17%
`mlk_poly_cbd_eta2`	✅	5s	2s	+150%
`keccak_f1600_x4_native_aarch64_v84a`	✅	4s	2s	+100%
`mlk_ct_sel_int16`	✅	4s	3s	+33%
`mlk_keccakf1600_xor_bytes (big endian)`	✅	4s	1s	+300%
`mlk_poly_add`	✅	4s	7s	-43%
`mlk_poly_cbd_eta1`	✅	4s	1s	+300%
`mlk_poly_getnoise_eta1_4x`	✅	4s	2s	+100%
`mlk_poly_getnoise_eta1_4x_native`	✅	4s	3s	+33%
`mlk_poly_tobytes`	✅	4s	3s	+33%
`mlk_polymat_permute_bitrev_to_custom`	✅	4s	3s	+33%
`mlk_polyvec_ntt`	✅	4s	4s	+0%
`poly_compress_d10_native_x86_64`	✅	4s	5s	-20%
`poly_decompress_d10_native_x86_64`	✅	4s	5s	-20%
`polyvec_basemul_acc_montgomery_cached_k3_native_x86_64`	✅	4s	2s	+100%
`sys_check_capability`	✅	4s	3s	+33%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	3s	1s	+200%
`keccakf1600_permute_native`	✅	3s	3s	+0%
`kem_enc`	✅	3s	2s	+50%
`mlk_ct_cmov_zero`	✅	3s	3s	+0%
`mlk_ct_get_optblocker_u32`	✅	3s	1s	+200%
`mlk_ct_sel_uint8`	✅	3s	1s	+200%
`mlk_fqmul`	✅	3s	16s	-81%
`mlk_gen_matrix`	✅	3s	2s	+50%
`mlk_keccak_absorb_once`	✅	3s	3s	+0%
`mlk_keypair_getnoise_eta1`	✅	3s	2s	+50%
`mlk_montgomery_reduce`	✅	3s	1s	+200%
`mlk_poly_decompress_d10`	✅	3s	2s	+50%
`mlk_poly_decompress_d4`	✅	3s	3s	+0%
`mlk_poly_decompress_d4_c`	✅	3s	4s	-25%
`mlk_poly_decompress_d5_c`	✅	3s	3s	+0%
`mlk_poly_decompress_d5_native`	✅	3s	3s	+0%
`mlk_poly_frombytes`	✅	3s	2s	+50%
`mlk_poly_frombytes_c`	✅	3s	4s	-25%
`mlk_poly_frommsg`	✅	3s	9s	-67%
`mlk_poly_getnoise_eta1122_4x`	✅	3s	1s	+200%
`mlk_poly_invntt_tomont`	✅	3s	4s	-25%
`mlk_poly_mulcache_compute`	✅	3s	2s	+50%
`mlk_poly_mulcache_compute_c`	✅	3s	2s	+50%
`mlk_poly_reduce`	✅	3s	2s	+50%
`mlk_poly_reduce_c`	✅	3s	3s	+0%
`mlk_poly_tobytes_c`	✅	3s	1s	+200%
`mlk_poly_tomont_native`	✅	3s	3s	+0%
`mlk_polyvec_basemul_acc_montgomery_cached`	✅	3s	4s	-25%
`mlk_polyvec_frombytes`	✅	3s	3s	+0%
`mlk_polyvec_reduce`	✅	3s	1s	+200%
`mlk_rej_uniform`	✅	3s	1s	+200%
`mlk_scalar_compress_d11`	✅	3s	1s	+200%
`mlk_scalar_compress_d5`	✅	3s	1s	+200%
`mlk_shake128_absorb_once`	✅	3s	1s	+200%
`mlk_value_barrier_u8`	✅	3s	2s	+50%
`ntt_native_aarch64`	✅	3s	3s	+0%
`poly_decompress_d4_native_x86_64`	✅	3s	6s	-50%
`poly_decompress_d5_native_x86_64`	✅	3s	4s	-25%
`poly_frombytes_native_x86_64`	✅	3s	5s	-40%
`poly_ntt_native`	✅	3s	39s	-92%
`poly_reduce_native_aarch64`	✅	3s	2s	+50%
`poly_tobytes_native_x86_64`	✅	3s	3s	+0%
`poly_tomont_native_aarch64`	✅	3s	1s	+200%
`rej_uniform_native`	✅	3s	2s	+50%
`intt_native_aarch64`	✅	2s	5s	-60%
`keccak_f1600_x1_native_aarch64`	✅	2s	1s	+100%
`keccak_f1600_x1_native_aarch64_v84a`	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	2s	3s	-33%
`keccakf1600x4_xor_bytes_native`	✅	2s	2s	+0%
`kem_check_pk`	✅	2s	2s	+0%
`kem_check_sk`	✅	2s	2s	+0%
`kem_enc_derand`	✅	2s	3s	-33%
`kem_keypair_derand`	✅	2s	2s	+0%
`mlk_barrett_reduce`	✅	2s	2s	+0%
`mlk_ct_cmask_nonzero_u16`	✅	2s	4s	-50%
`mlk_ct_cmask_nonzero_u8`	✅	2s	4s	-50%
`mlk_keccakf1600_extract_bytes`	✅	2s	4s	-50%
`mlk_keccakf1600_extract_bytes (big endian)`	✅	2s	2s	+0%
`mlk_keccakf1600x4_extract_bytes_c`	✅	2s	2s	+0%
`mlk_keccakf1600x4_permute`	✅	2s	4s	-50%
`mlk_keccakf1600x4_xor_bytes`	✅	2s	2s	+0%
`mlk_keccakf1600x4_xor_bytes_c`	✅	2s	1s	+100%
`mlk_matvec_mul`	✅	2s	4s	-50%
`mlk_poly_compress_d10`	✅	2s	2s	+0%
`mlk_poly_compress_d10_c`	✅	2s	2s	+0%
`mlk_poly_compress_d10_native`	✅	2s	2s	+0%
`mlk_poly_compress_d4`	✅	2s	3s	-33%
`mlk_poly_compress_d4_native`	✅	2s	3s	-33%
`mlk_poly_compress_d5`	✅	2s	2s	+0%
`mlk_poly_compress_d5_native`	✅	2s	2s	+0%
`mlk_poly_compress_du`	✅	2s	1s	+100%
`mlk_poly_compress_dv`	✅	2s	1s	+100%
`mlk_poly_decompress_d10_c`	✅	2s	1s	+100%
`mlk_poly_decompress_d11`	✅	2s	2s	+0%
`mlk_poly_decompress_d11_c`	✅	2s	3s	-33%
`mlk_poly_decompress_d11_native`	✅	2s	1s	+100%
`mlk_poly_decompress_du`	✅	2s	1s	+100%
`mlk_poly_invntt_tomont_c`	✅	2s	2s	+0%
`mlk_poly_mulcache_compute_native`	✅	2s	1s	+100%
`mlk_poly_ntt_c`	✅	2s	1s	+100%
`mlk_poly_tobytes_native`	✅	2s	1s	+100%
`mlk_poly_tomont_c`	✅	2s	3s	-33%
`mlk_poly_tomsg`	✅	2s	3s	-33%
`mlk_polyvec_compress_du`	✅	2s	1s	+100%
`mlk_polyvec_decompress_du`	✅	2s	4s	-50%
`mlk_polyvec_invntt_tomont`	✅	2s	1s	+100%
`mlk_scalar_compress_d1`	✅	2s	2s	+0%
`mlk_scalar_compress_d10`	✅	2s	2s	+0%
`mlk_scalar_decompress_d10`	✅	2s	2s	+0%
`mlk_scalar_decompress_d11`	✅	2s	3s	-33%
`mlk_scalar_decompress_d4`	✅	2s	2s	+0%
`mlk_scalar_decompress_d5`	✅	2s	2s	+0%
`mlk_sha3_256`	✅	2s	2s	+0%
`mlk_sha3_512`	✅	2s	3s	-33%
`mlk_shake128x4_absorb_once`	✅	2s	3s	-33%
`mlk_shake256`	✅	2s	2s	+0%
`mlk_value_barrier_i32`	✅	2s	2s	+0%
`mlk_value_barrier_u32`	✅	2s	2s	+0%
`nttunpack_native_x86_64`	✅	2s	3s	-33%
`poly_compress_d4_native_x86_64`	✅	2s	3s	-33%
`poly_compress_d5_native_x86_64`	✅	2s	2s	+0%
`poly_getnoise_eta1122_4x_native`	✅	2s	1s	+100%
`poly_invntt_tomont_native`	✅	2s	2s	+0%
`poly_mulcache_compute_native_aarch64`	✅	2s	6s	-67%
`poly_mulcache_compute_native_x86_64`	✅	2s	3s	-33%
`poly_reduce_native_x86_64`	✅	2s	2s	+0%
`poly_tomont_native_x86_64`	✅	2s	1s	+100%
`polyvec_basemul_acc_montgomery_cached_k2_native_aarch64`	✅	2s	3s	-33%
`polyvec_basemul_acc_montgomery_cached_k2_native_x86_64`	✅	2s	4s	-50%
`polyvec_basemul_acc_montgomery_cached_k4_native_aarch64`	✅	2s	1s	+100%
`intt_native_x86_64`	✅	1s	3s	-67%
`keccak_f1600_x4_native_avx2`	✅	1s	2s	-50%
`keccakf1600x4_extract_bytes_native`	✅	1s	3s	-67%
`kem_keypair`	✅	1s	2s	-50%
`mlk_ct_cmask_neg_i16`	✅	1s	3s	-67%
`mlk_ct_get_optblocker_i32`	✅	1s	1s	+0%
`mlk_ct_get_optblocker_u8`	✅	1s	2s	-50%
`mlk_ct_memcmp`	✅	1s	4s	-75%
`mlk_enc_getnoise_eta1_eta2`	✅	1s	3s	-67%
`mlk_keccakf1600_permute`	✅	1s	1s	+0%
`mlk_keccakf1600_xor_bytes`	✅	1s	3s	-67%
`mlk_keccakf1600x4_extract_bytes`	✅	1s	4s	-75%
`mlk_poly_compress_d11`	✅	1s	1s	+0%
`mlk_poly_compress_d11_c`	✅	1s	1s	+0%
`mlk_poly_compress_d11_native`	✅	1s	4s	-75%
`mlk_poly_compress_d4_c`	✅	1s	1s	+0%
`mlk_poly_compress_d5_c`	✅	1s	1s	+0%
`mlk_poly_decompress_d5`	✅	1s	2s	-50%
`mlk_poly_decompress_dv`	✅	1s	2s	-50%
`mlk_poly_tomont`	✅	1s	1s	+0%
`mlk_polyvec_mulcache_compute`	✅	1s	2s	-50%
`mlk_polyvec_permute_bitrev_to_custom`	✅	1s	1s	+0%
`mlk_polyvec_permute_bitrev_to_custom_native`	✅	1s	2s	-50%
`mlk_polyvec_tobytes`	✅	1s	1s	+0%
`mlk_polyvec_tomont`	✅	1s	1s	+0%
`mlk_scalar_compress_d4`	✅	1s	2s	-50%
`mlk_scalar_signed_to_unsigned_q`	✅	1s	5s	-80%
`mlk_shake128_squeezeblocks`	✅	1s	3s	-67%
`mlk_shake128x4_squeezeblocks`	✅	1s	1s	+0%
`ntt_native_x86_64`	✅	1s	3s	-67%
`poly_compress_d11_native_x86_64`	✅	1s	3s	-67%
`poly_decompress_d11_native_x86_64`	✅	1s	1s	+0%
`poly_tobytes_native_aarch64`	✅	1s	1s	+0%
`polyvec_basemul_acc_montgomery_cached_k3_native_aarch64`	✅	1s	2s	-50%
`polyvec_basemul_acc_montgomery_cached_k4_native_x86_64`	✅	1s	2s	-50%

oqs-bot · 2026-08-24T16:53:46Z

CBMC Results (ML-KEM-512)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`mlk_indcpa_dec`	⚠️	23s	14s	+64%
`mlk_ntt_butterfly_block`	⚠️	326s	9s	+3522%

Full Results (191 proofs)

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

hanno-becker · 2026-08-26T03:24:02Z


 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
 EXTERNAL_SAT_SOLVER=
-CBMCFLAGS=--bitwuzla


Those solver changes seem unrelated or at least unexplained.

Just maintaining reasonable performance for the current CI runs seemed a reasonable thing to do under the auspices of this PR. As as I said below, adding new CI runs to cover ILP32 requires some thinking and budget decisions that are best handled separately.

hanno-becker · 2026-08-26T03:24:22Z

+# or  "LP64"  - 64-bit systems where "long and pointer are 64-bit"
+#
+# if CBMC_DM is not set, default to LP64
+CBMC_DM ?= LP64


Can you plumb that into tests cbmc ... as well please?

hanno-becker · 2026-08-26T03:24:34Z

+  CBMC_DM_FLAG = --LP64
+  PROOF_INCLUDE = $(CBMC_ROOT)/cbmc/include/LP64
+else ifeq ($(strip $(CBMC_DM)),ILP32)
+  GOTO_CC_DM_FLAG = --32


Does the 32-bit mode work?

Yes... but running it locally on my Mac I observed some proofs became really slow. Some tweaking of proof Makefiles might be required (i.e. the setting of CBMC_OBJECT_BITS to suit the smaller value of SIZE_MAX), but I hope to address that under a new PR.

hanno-becker

Thanks @rod-chapman, it's great to see progress in this direction.

Please can you confirm the status of the 32-bit model? I don't think we should include it without also testing it in CI. If we are not ready for that, yet, I suggest trimming down the PR to the addition of the infrastructure and the 64-bit header.

Please also integrate the choice of data model into tests cbmc.

Please also clean up the CI; the second commit message is insufficient, and there are solver changes in the first commit which are unrelated and/or unexplained.

rod-chapman · 2026-08-26T08:03:22Z

Thanks for your thoughts.

Yes... we need the CI runners to change to add at least 1 32-bit proof run, but I wanted to discuss that separately, under a new PR. How many CI runs in 32-bit mode should we do? What will that cost in terms of runners? I thought that a policy discussion was warranted on those topics before going ahead.

With the proof changes - I noticed that several proofs became slower with bitwuzla. I tried switching them back to z3, and they got faster. I don't have an "explanation" for this per se... they're just faster with z3 now.

rod-chapman · 2026-08-26T08:11:15Z

I see this PR as adding the plumbing to support multiple data models. I had hoped to add the "porcelain" layer (i.e. updating "tests cbmc" and CI actions) following requirements and policy decisions that I don't feel qualified to make alone.

rod-chapman · 2026-08-26T10:02:46Z

I am looking at the proof performance for ntt_butterfly_block() on my Grv4 machine now. I will update commit messages as soon as I have good data.

hanno-becker · 2026-08-27T03:21:52Z

@rod-chapman Yes, it's fine to add the plumbing, but let's add 32-bit only when we can actually exercise at least a few functions with it. I think the management of the proof dimensions (function, solver, data model) could be piggy backed atop the draft pq-code-package/mldsa-native#1122 for supporting multiple solvers (needs to be ported to mlkem-native; I can do that). Please use Claude, precedent, and your judgement, to make the necessary changes to tests cbmc -- I think a --lp={lp64,...} is all we need and should be simple to implement.

rod-chapman · 2026-08-27T07:27:54Z

OK... I will update "tests" as part of the "plumbing" in this PR.

I think "multi-solver" support is still a long way off, and independent of this work on stabilization and multi-data-model support. As I said, my local benchmarks have cvc5 a long way behind z3 on CBMC-generated problems, but it would be a good way to drive improvement of cvc5 in the long term.

rod-chapman · 2026-08-27T16:19:58Z

As I feared, proofs for some functions with ILP32 are very slow. For example - over 1 hour for indcpa_enc(). We may need assistance of CBMC team to diagnose this, so suggest we defer actual CI runs for ILP32 until a later PR.

hanno-becker · 2026-08-28T02:49:28Z

I think "multi-solver" support is still a long way off, and independent of this work on stabilization and multi-data-model support. As I said, my local benchmarks have cvc5 a long way behind z3 on CBMC-generated problems, but it would be a good way to drive improvement of cvc5 in the long term.

I don't think it's so far off -- one should not approach it as a monolithic change, but as a gradual one. And it relates to this PR insofar as it, too, adds a verification dimension to CBMC, and we need a way to manage them.

1. CBMC Makefile.common now always uses gcc for pre-processing. 2. Specify -nostdinc for pre-processing, so host-dependent include files are NOT used, since this leads to proof instability across platforms. 3. Instead, specify and add our own minimal set the the standard LibC header files, but only what we need for mlkem-native and nothing else, all based solely on what is required by ISO C99 (7.17 - 7.21) 4. First two sets of header files are for 4.1. The "LP64" data model, where "Long and Pointers are 64 bits", which is that used by common 64-bit platforms such as AArch64/Linux, x86_64/Linux and AArch64/macOS. 4.2. The "ILP32" data model, for 32-bit systems such as 32-bit ARM, RV32, and most embedded 32-bit microcontrollers. A third set of headers for the LLP64 (64-bit Windows) will follow. 5. Environment variable CBMC_DM controls selection of the data-model in Makefile.common. It defaults to "LP64" 6. Update four proofs to use Z3 instead of bitwuzla, which turn out to be more efficient with CBMC 6.11 and these header files. Signed-off-by: Rod Chapman <rodchap@amazon.com>

Proof timing experiments on this functions on Grv4/Ubuntu: Constant parameters: CBMC 6.11, z3 4.15.3, LP64 data model CBMC_OBJECT_BITS=B below 1. z3 default, K=2, B=12: unsat in 3m59s 2. z3 smt_only, K=2, B=12: unsat in 6m26s 3. z3 default, K=2, B=9: unsat in 20m7s 4. z3 smt_only, K=2, B=9: unsat in 4m18s So far, case 1 is winning, so let's try modulating B: 5. z3 default, K=2, B=13: unsat in 3m10s 6. z3 default, K=2, B=14: unsat in 3m15s So case 5 now winning. Let's try other values of K 7. z3 default, K=3, B=13: unsat in 3m11s 8. z3 default, K=4, B=13: unsat in 3m11s I also find that macOS is fine with those settings, in similar times. I also find that using z3 5.1.0 with case 5 terminates in 2m47s, so we can expect a small improvement with we upgrade to 5.1.0 Signed-off-by: Rod Chapman <rodchap@amazon.com>

1. CBMC's Makefile.common runs proofs with the chosen data model based on the setting of the CBMC_DM environment variable. If not set, this defaults to LP64. The "result", "smt" and "report" makefile targets are updated to report the setting of MLKEM_K and CBMC_DM to the user to confirm what is being run. 2. The run-cbmc-proofs.py script is similarly updated to use CBMC_DM (or LP64 by default), and to confirm the setting of MLKEM_K and CBMC_DM to the user before spawning litani. 3. Finally, the top-level "tests cbmc" script is updated to add a new command-line option "--dm" with legal values "LP64" and "ILP32", also defaulting to "LP64" if not specified. Updates to GitHub actions to exercise these new options are TBD. Signed-off-by: Rod Chapman <rodchap@amazon.com>

rod-chapman requested a review from mkannwischer August 24, 2026 15:53

rod-chapman self-assigned this Aug 24, 2026

rod-chapman added the CBMC label Aug 24, 2026

rod-chapman requested a review from a team as a code owner August 24, 2026 15:53

rod-chapman force-pushed the minimal-libc-for-cbmc branch from 010bb0e to 9cc67d2 Compare August 25, 2026 13:40

hanno-becker reviewed Aug 26, 2026

View reviewed changes

hanno-becker requested changes Aug 26, 2026

View reviewed changes

rod-chapman force-pushed the minimal-libc-for-cbmc branch from 9cc67d2 to 979c068 Compare August 26, 2026 10:02

rod-chapman force-pushed the minimal-libc-for-cbmc branch from 979c068 to 173b172 Compare August 26, 2026 16:22

rod-chapman force-pushed the minimal-libc-for-cbmc branch from 0eab717 to 60a8c71 Compare August 27, 2026 12:28

hanno-becker mentioned this pull request Aug 28, 2026

Add CBMC target platform support #1760

Closed

rod-chapman added 3 commits August 28, 2026 14:46

rod-chapman force-pushed the minimal-libc-for-cbmc branch from 60a8c71 to d4b81e6 Compare August 28, 2026 13:46

Uh oh!

Conversation

rod-chapman commented Aug 24, 2026

Uh oh!

oqs-bot commented Aug 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-KEM-1024)

Uh oh!

oqs-bot commented Aug 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-KEM-768)

Uh oh!

oqs-bot commented Aug 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-KEM-512)

Uh oh!

hanno-becker Aug 26, 2026

Choose a reason for hiding this comment

Uh oh!

rod-chapman Aug 26, 2026

Choose a reason for hiding this comment

Uh oh!

hanno-becker Aug 26, 2026

Choose a reason for hiding this comment

Uh oh!

hanno-becker Aug 26, 2026

Choose a reason for hiding this comment

Uh oh!

rod-chapman Aug 26, 2026

Choose a reason for hiding this comment

Uh oh!

hanno-becker left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

rod-chapman commented Aug 26, 2026

Uh oh!

rod-chapman commented Aug 26, 2026

Uh oh!

rod-chapman commented Aug 26, 2026

Uh oh!

hanno-becker commented Aug 27, 2026

Uh oh!

rod-chapman commented Aug 27, 2026

Uh oh!

rod-chapman commented Aug 27, 2026

Uh oh!

hanno-becker commented Aug 28, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

oqs-bot commented Aug 24, 2026 •

edited

Loading

oqs-bot commented Aug 24, 2026 •

edited

Loading

oqs-bot commented Aug 24, 2026 •

edited

Loading

hanno-becker left a comment •

edited

Loading