nix: Bump z3 to 4.16.0 from nixpkgs-unstable by mkannwischer · Pull Request #1702 · pq-code-package/mlkem-native

mkannwischer · 2026-05-22T01:34:32Z

It is somewhat inconvienent for developers having to compile z3 from source. While this a one-off step, I would still like to avoid it if possible.

This commit sources z3 from nixpkgs-unstable rather than the local override so we pick up the binary cache, and aligns the pinned version with what nixpkgs 26.05 will ship.

It is somewhat inconvienent for developers having to compile z3 from source. While this a one-off step, I would still like to avoid it if possible. This commit sources z3 from nixpkgs-unstable rather than the local override so we pick up the binary cache, and aligns the pinned version with what nixpkgs 26.05 will ship. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

oqs-bot · 2026-05-22T01:56:11Z

CBMC Results (ML-KEM-1024)

Full Results (191 proofs)

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

oqs-bot · 2026-05-22T01:56:14Z

CBMC Results (ML-KEM-512)

Full Results (191 proofs)

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

oqs-bot · 2026-05-22T01:56:20Z

CBMC Results (ML-KEM-768)

Full Results (191 proofs)

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

mkannwischer · 2026-05-23T04:12:26Z

Let's hold this back until we have #1703 has been addressed.

mkannwischer added the needs-mldsa-native-port label May 22, 2026

mkannwischer mentioned this pull request May 22, 2026

nix: Bump z3 to 4.16.0 from nixpkgs-unstable pq-code-package/mldsa-native#1125

Draft

mkannwischer removed the needs-mldsa-native-port label May 22, 2026

mkannwischer marked this pull request as ready for review May 22, 2026 03:06

mkannwischer requested a review from a team as a code owner May 22, 2026 03:06

mkannwischer added the DO-NOT-MERGE label May 23, 2026

mkannwischer marked this pull request as draft May 23, 2026 04:12

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

nix: Bump z3 to 4.16.0 from nixpkgs-unstable#1702

nix: Bump z3 to 4.16.0 from nixpkgs-unstable#1702
mkannwischer wants to merge 1 commit into
mainfrom
nix-z3-4.16.0

mkannwischer commented May 22, 2026

Uh oh!

oqs-bot commented May 22, 2026

Uh oh!

oqs-bot commented May 22, 2026

Uh oh!

oqs-bot commented May 22, 2026

Uh oh!

mkannwischer commented May 23, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

mkannwischer commented May 22, 2026

Uh oh!

oqs-bot commented May 22, 2026

CBMC Results (ML-KEM-1024)

Uh oh!

oqs-bot commented May 22, 2026

CBMC Results (ML-KEM-512)

Uh oh!

oqs-bot commented May 22, 2026

CBMC Results (ML-KEM-768)

Uh oh!

mkannwischer commented May 23, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants