HOL-Light: Avoid repeated work in proof loops by hanno-becker · Pull Request #1962 · pq-code-package/mlkem-native

hanno-becker · 2026-10-26T05:13:08Z

Port of HOL-Light: Tweaks for better proof performance mldsa-native#1499

Instruction loops apply the same step and SIMD tactics after each instruction. Constructing them inside callbacks rebuilds rewrite conversions and helper predicates for every step, making long arithmetic proofs spend time preparing unchanged work.

Prepare ARM/x86 step tactics and SIMD simplifiers once outside all matching ML-KEM loops. In SIMD_SIMPLIFY_ABBREV_TAC, also prepare the conversion and local-definition predicate once while still reading arithmetic equations from the current proof context.

After NTT congruences are reduced to real polynomials, REAL_INTEGER_TAC needs no execution assumptions. Drop those assumptions before the four AArch64/x86_64 NTT and inverse NTT closure calls.

The prepared conversions capture their rewrite rules when the tactic is built. Rebuild the tactic if those rules change.

Instruction loops apply the same step and SIMD tactics after each instruction. Constructing them inside callbacks rebuilds rewrite conversions and helper predicates for every step, making long arithmetic proofs spend time preparing unchanged work. Prepare ARM/x86 step tactics and SIMD simplifiers once outside all matching ML-KEM loops. In SIMD_SIMPLIFY_ABBREV_TAC, also prepare the conversion and local-definition predicate once while still reading arithmetic equations from the current proof context. After NTT congruences are reduced to real polynomials, REAL_INTEGER_TAC needs no execution assumptions. Drop those assumptions before the four AArch64/x86_64 NTT and inverse NTT closure calls. The prepared conversions capture their rewrite rules when the tactic is built. Rebuild the tactic if those rules change. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

oqs-bot · 2026-10-26T06:01:00Z

CBMC Results (ML-KEM-768)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`kem_enc`	LP64	bitwuzla	⚠️	31s	2s	+1450%
`kem_keypair`	LP64	cadical	⚠️	179s	2s	+8850%
`mlk_gen_matrix`	LP64	cadical	⚠️	58s	2s	+2800%
`mlk_gen_matrix_serial`	LP64	cadical	⚠️	60s	2s	+2900%
`mlk_indcpa_dec`	LP64	cadical	⚠️	80s	10s	+700%
	LP64	z3*	⚠️	21s	10s	+110%
`mlk_indcpa_enc`	LP64	z3_smt_only*	⚠️	456s	252s	+81%
`mlk_keccak_squeeze_once`	LP64	z3	⚠️	33s	7s	+371%
`mlk_keccak_squeezeblocks`	LP64	cvc5_arrays_exp	⚠️	21s	8s	+162%
`mlk_matvec_mul`	LP64	cadical	⚠️	23s	4s	+475%
`mlk_ntt_butterfly_block`	LP64	z3*	⚠️	288s	7s	+4014%
`mlk_poly_add`	LP64	bitwuzla	⚠️	65s	7s	+829%
`mlk_poly_getnoise_eta1_4x`	LP64	cvc5_enum_inst	⚠️	81s	2s	+3950%
`mlk_poly_invntt_tomont_c`	LP64	bitwuzla	⚠️	41s	2s	+1950%
`mlk_poly_ntt_c`	LP64	bitwuzla	⚠️	66s	1s	+6500%
`mlk_poly_sub`	LP64	bitwuzla	⚠️	32s	10s	+220%
`mlk_polymat_permute_bitrev_to_custom`	LP64	cadical	⚠️	38s	3s	+1167%
`mlk_polyvec_add`	LP64	cadical	⚠️	74s	12s	+517%
`mlk_polyvec_basemul_acc_montgomery_cached`	LP64	bitwuzla	⚠️	20s	4s	+400%
`mlk_polyvec_basemul_acc_montgomery_cached_c`	LP64	z3*	⚠️	76s	46s	+65%
`mlk_shake256x4`	LP64	cvc5_arrays_exp	⚠️	30s	3s	+900%
`ntt_native_x86_64`	LP64	bitwuzla	⚠️	20s	3s	+567%
`nttunpack_native_x86_64`	LP64	cvc5_enum_inst	⚠️	70s	3s	+2233%
`rej_uniform_native`	LP64	z3_smt_only	⚠️	39s	2s	+1850%
`rej_uniform_native_x86_64`	LP64	z3*	⚠️	117s	55s	+113%

Full Results (379 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1998s	1645s	+21.5%
`intt_native_aarch64`	LP64	bitwuzla	✅	11s	5s	+120%
	LP64	z3*	✅	2s	5s	-60%
`intt_native_x86_64`	LP64	bitwuzla	✅	10s	3s	+233%
	LP64	z3*	✅	1s	3s	-67%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	1s	1s	+0%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	3s	3s	+0%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	2s	1s	+100%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	3s	2s	+50%
`keccakf1600_permute_native`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	3s	3s	+0%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	3s	3s	+0%
`keccakf1600x4_permute_native_x4`	LP64	bitwuzla*	✅	17s	21s	-19%
	LP64	z3	✅	17s	21s	-19%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	1s	2s	-50%
`kem_check_pk`	LP64	z3*	✅	3s	2s	+50%
`kem_check_sk`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`kem_dec`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	6s	5s	+20%
`kem_enc`	LP64	bitwuzla	⚠️	31s	2s	+1450%
	LP64	z3*	✅	2s	2s	+0%
`kem_enc_derand`	LP64	cadical	✅	8s	3s	+167%
	LP64	z3*	✅	2s	3s	-33%
`kem_keypair`	LP64	cadical	⚠️	179s	2s	+8850%
	LP64	z3*	✅	2s	2s	+0%
`kem_keypair_derand`	LP64	bitwuzla	✅	9s	2s	+350%
	LP64	z3*	✅	3s	2s	+50%
`mlk_barrett_reduce`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mlk_check_pct`	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3	✅	4s	3s	+33%
`mlk_ct_cmask_neg_i16`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`mlk_ct_cmask_nonzero_u16`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	1s	4s	-75%
`mlk_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	3s	4s	-25%
`mlk_ct_cmov_zero`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	cvc5_mbqi_enum	✅	3s	3s	+0%
`mlk_ct_get_optblocker_i32`	ILP32	bitwuzla	✅	4s	1s	+300%
	ILP32	cvc5_arrays_exp	✅	2s	1s	+100%
	ILP32	z3	✅	1s	1s	+0%
	LP64	bitwuzla*	✅	4s	1s	+300%
	LP64	cvc5_arrays_exp	✅	1s	1s	+0%
	LP64	z3	✅	4s	1s	+300%
`mlk_ct_get_optblocker_u32`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3	✅	2s	1s	+100%
`mlk_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
`mlk_ct_memcmp`	LP64	bitwuzla*	✅	4s	4s	+0%
	LP64	cvc5_enum_inst	✅	4s	4s	+0%
`mlk_ct_sel_int16`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	3s	+0%
`mlk_ct_sel_uint8`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	4s	1s	+300%
`mlk_enc_getnoise_eta1_eta2`	LP64	cvc5_enum_inst	✅	11s	3s	+267%
	LP64	z3*	✅	4s	3s	+33%
`mlk_fqmul`	LP64	bitwuzla	✅	4s	16s	-75%
	LP64	z3*	✅	4s	16s	-75%
`mlk_gen_matrix`	LP64	cadical	⚠️	58s	2s	+2800%
	LP64	z3*	✅	4s	2s	+100%
`mlk_gen_matrix_serial`	LP64	cadical	⚠️	60s	2s	+2900%
	LP64	z3*	✅	2s	2s	+0%
`mlk_indcpa_dec`	LP64	cadical	⚠️	80s	10s	+700%
	LP64	z3*	⚠️	21s	10s	+110%
`mlk_indcpa_enc`	LP64	z3_smt_only*	⚠️	456s	252s	+81%
`mlk_indcpa_keypair_derand`	LP64	z3*	✅	115s	318s	-64%
`mlk_invntt_layer`	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	5s	4s	+25%
`mlk_keccak_absorb_once`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	3s	3s	+0%
`mlk_keccak_absorb_once_x4`	LP64	bitwuzla*	✅	7s	5s	+40%
	LP64	z3	✅	5s	5s	+0%
`mlk_keccak_squeeze_once`	LP64	bitwuzla*	✅	10s	7s	+43%
	LP64	z3	⚠️	33s	7s	+371%
`mlk_keccak_squeezeblocks`	LP64	bitwuzla*	✅	7s	8s	-12%
	LP64	cvc5_arrays_exp	⚠️	21s	8s	+162%
`mlk_keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	27s	24s	+12%
	LP64	cvc5_arrays_exp	✅	19s	24s	-21%
`mlk_keccakf1600_extract_bytes`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3	✅	2s	4s	-50%
`mlk_keccakf1600_extract_bytes (big endian)`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
`mlk_keccakf1600_permute`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	1s	1s	+0%
`mlk_keccakf1600_permute_c`	LP64	bitwuzla	✅	7s	6s	+17%
	LP64	z3*	✅	4s	6s	-33%
`mlk_keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	2s	3s	-33%
`mlk_keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	1s	1s	+0%
`mlk_keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3	✅	5s	4s	+25%
`mlk_keccakf1600x4_extract_bytes_c`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	4s	2s	+100%
`mlk_keccakf1600x4_permute`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	2s	4s	-50%
`mlk_keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	1s	2s	-50%
`mlk_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	3s	1s	+200%
`mlk_keypair_getnoise_eta1`	LP64	cvc5_mbqi_enum	✅	16s	2s	+700%
	LP64	z3*	✅	2s	2s	+0%
`mlk_matvec_mul`	LP64	cadical	⚠️	23s	4s	+475%
	LP64	z3*	✅	5s	4s	+25%
`mlk_montgomery_reduce`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`mlk_ntt_butterfly_block`	LP64	bitwuzla	✅	11s	7s	+57%
	LP64	z3*	⚠️	288s	7s	+4014%
`mlk_ntt_layer`	LP64	bitwuzla	✅	30s	29s	+3%
	LP64	z3*	✅	7s	29s	-76%
`mlk_poly_add`	LP64	bitwuzla	⚠️	65s	7s	+829%
	LP64	z3*	✅	5s	7s	-29%
`mlk_poly_cbd_eta1`	LP64	bitwuzla	✅	15s	1s	+1400%
	LP64	z3*	✅	2s	1s	+100%
`mlk_poly_cbd_eta2`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`mlk_poly_compress_d10`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	3s	2s	+50%
`mlk_poly_compress_d10_c`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	1s	2s	-50%
`mlk_poly_compress_d10_native`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	3s	2s	+50%
`mlk_poly_compress_d11`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3	✅	3s	1s	+200%
`mlk_poly_compress_d11_c`	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	3s	1s	+200%
`mlk_poly_compress_d11_native`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3	✅	3s	4s	-25%
`mlk_poly_compress_d4`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	2s	3s	-33%
`mlk_poly_compress_d4_c`	LP64	bitwuzla	✅	11s	1s	+1000%
	LP64	z3*	✅	4s	1s	+300%
`mlk_poly_compress_d4_native`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	1s	3s	-67%
`mlk_poly_compress_d5`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	3s	2s	+50%
`mlk_poly_compress_d5_c`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	3s	1s	+200%
`mlk_poly_compress_d5_native`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
`mlk_poly_compress_du`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	5s	1s	+400%
`mlk_poly_compress_dv`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3	✅	1s	1s	+0%
`mlk_poly_decompress_d10`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	3s	2s	+50%
`mlk_poly_decompress_d10_c`	LP64	bitwuzla	✅	7s	1s	+600%
	LP64	z3*	✅	2s	1s	+100%
`mlk_poly_decompress_d10_native`	LP64	bitwuzla*	✅	13s	15s	-13%
	LP64	z3	✅	1s	15s	-93%
`mlk_poly_decompress_d11`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	3s	2s	+50%
`mlk_poly_decompress_d11_c`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`mlk_poly_decompress_d11_native`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	3s	1s	+200%
`mlk_poly_decompress_d4`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	1s	3s	-67%
`mlk_poly_decompress_d4_c`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	3s	4s	-25%
`mlk_poly_decompress_d4_native`	LP64	bitwuzla*	✅	15s	12s	+25%
	LP64	z3	✅	3s	12s	-75%
`mlk_poly_decompress_d5`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
`mlk_poly_decompress_d5_c`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`mlk_poly_decompress_d5_native`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	3s	3s	+0%
`mlk_poly_decompress_du`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	2s	1s	+100%
`mlk_poly_decompress_dv`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
`mlk_poly_frombytes`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	3s	2s	+50%
`mlk_poly_frombytes_c`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	4s	-25%
`mlk_poly_frombytes_native`	LP64	bitwuzla*	✅	14s	8s	+75%
	LP64	z3	✅	2s	8s	-75%
`mlk_poly_frommsg`	LP64	bitwuzla	✅	9s	9s	+0%
	LP64	z3*	✅	2s	9s	-78%
`mlk_poly_getnoise_eta1122_4x`	LP64	cvc5_mbqi_enum	✅	2s	1s	+100%
	LP64	z3*	✅	5s	1s	+400%
`mlk_poly_getnoise_eta1122_4x_serial`	LP64	cvc5_enum_inst	✅	3s	-	new
	LP64	z3*	✅	3s	-	new
`mlk_poly_getnoise_eta1_4x`	LP64	cvc5_enum_inst	⚠️	81s	2s	+3950%
	LP64	z3*	✅	3s	2s	+50%
`mlk_poly_getnoise_eta1_4x_serial`	LP64	cvc5_enum_inst	✅	86s	-	new
	LP64	z3*	✅	3s	-	new
`mlk_poly_getnoise_eta2`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mlk_poly_invntt_tomont`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	4s	4s	+0%
`mlk_poly_invntt_tomont_c`	LP64	bitwuzla	⚠️	41s	2s	+1950%
	LP64	z3*	✅	1s	2s	-50%
`mlk_poly_mulcache_compute`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`mlk_poly_mulcache_compute_c`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	5s	2s	+150%
`mlk_poly_mulcache_compute_native`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	1s	1s	+0%
`mlk_poly_ntt`	LP64	bitwuzla*	✅	10s	5s	+100%
	LP64	z3	✅	1s	5s	-80%
`mlk_poly_ntt_c`	LP64	bitwuzla	⚠️	66s	1s	+6500%
	LP64	z3*	✅	1s	1s	+0%
`mlk_poly_reduce`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
`mlk_poly_reduce_c`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	1s	3s	-67%
`mlk_poly_reduce_native`	LP64	bitwuzla*	✅	31s	34s	-9%
	LP64	z3	✅	1s	34s	-97%
`mlk_poly_rej_uniform`	LP64	bitwuzla*	✅	38s	129s	-71%
	LP64	z3	✅	3s	129s	-98%
`mlk_poly_rej_uniform_x4`	LP64	z3*	✅	6s	5s	+20%
`mlk_poly_sub`	LP64	bitwuzla	⚠️	32s	10s	+220%
	LP64	z3*	✅	8s	10s	-20%
`mlk_poly_tobytes`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	1s	3s	-67%
`mlk_poly_tobytes_c`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`mlk_poly_tobytes_native`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	1s	1s	+0%
`mlk_poly_tomont`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`mlk_poly_tomont_c`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`mlk_poly_tomont_native`	LP64	bitwuzla	✅	12s	3s	+300%
	LP64	z3*	✅	3s	3s	+0%
`mlk_poly_tomsg`	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3	✅	1s	3s	-67%
`mlk_polymat_permute_bitrev_to_custom`	LP64	cadical	⚠️	38s	3s	+1167%
	LP64	z3*	✅	3s	3s	+0%
`mlk_polymat_permute_bitrev_to_custom_native`	LP64	z3*	✅	69s	-	new
`mlk_polyvec_add`	LP64	cadical	⚠️	74s	12s	+517%
	LP64	z3*	✅	15s	12s	+25%
`mlk_polyvec_basemul_acc_montgomery_cached`	LP64	bitwuzla	⚠️	20s	4s	+400%
	LP64	z3*	✅	1s	4s	-75%
`mlk_polyvec_basemul_acc_montgomery_cached_c`	LP64	cadical	✅	17s	46s	-63%
	LP64	z3*	⚠️	76s	46s	+65%
`mlk_polyvec_compress_du`	LP64	cadical	✅	8s	1s	+700%
	LP64	z3*	✅	2s	1s	+100%
`mlk_polyvec_decompress_du`	LP64	cvc5_enum_inst	✅	5s	4s	+25%
	LP64	z3*	✅	5s	4s	+25%
`mlk_polyvec_frombytes`	LP64	cvc5_enum_inst	✅	9s	3s	+200%
	LP64	z3*	✅	1s	3s	-67%
`mlk_polyvec_invntt_tomont`	LP64	cvc5_enum_inst	✅	6s	1s	+500%
	LP64	z3*	✅	2s	1s	+100%
`mlk_polyvec_mulcache_compute`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`mlk_polyvec_ntt`	LP64	cadical	✅	19s	4s	+375%
	LP64	z3*	✅	3s	4s	-25%
`mlk_polyvec_reduce`	LP64	cvc5_enum_inst	✅	7s	1s	+600%
	LP64	z3*	✅	3s	1s	+200%
`mlk_polyvec_tobytes`	LP64	cvc5_mbqi_enum	✅	6s	1s	+500%
	LP64	z3*	✅	3s	1s	+200%
`mlk_polyvec_tomont`	LP64	cvc5_enum_inst	✅	6s	1s	+500%
	LP64	z3*	✅	2s	1s	+100%
`mlk_rej_uniform`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	12s	1s	+1100%
`mlk_rej_uniform_c`	LP64	bitwuzla	✅	1s	114s	-99%
	LP64	z3*	✅	153s	114s	+34%
`mlk_scalar_compress_d1`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mlk_scalar_compress_d10`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`mlk_scalar_compress_d11`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	1s	1s	+0%
`mlk_scalar_compress_d4`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mlk_scalar_compress_d5`	LP64	bitwuzla	✅	4s	1s	+300%
	LP64	z3*	✅	2s	1s	+100%
`mlk_scalar_decompress_d10`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`mlk_scalar_decompress_d11`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`mlk_scalar_decompress_d4`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mlk_scalar_decompress_d5`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`mlk_scalar_signed_to_unsigned_q`	LP64	bitwuzla	✅	1s	5s	-80%
	LP64	z3*	✅	2s	5s	-60%
`mlk_sha3_256`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	1s	2s	-50%
`mlk_sha3_512`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	2s	3s	-33%
`mlk_shake128_absorb_once`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	2s	1s	+100%
`mlk_shake128_squeezeblocks`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	3s	3s	+0%
`mlk_shake128x4_absorb_once`	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3	✅	1s	3s	-67%
`mlk_shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3	✅	1s	1s	+0%
`mlk_shake256`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	1s	2s	-50%
`mlk_shake256x4`	LP64	bitwuzla*	✅	5s	3s	+67%
	LP64	cvc5_arrays_exp	⚠️	30s	3s	+900%
`mlk_value_barrier_i32`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	1s	2s	-50%
`mlk_value_barrier_u32`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	3s	2s	+50%
`mlk_value_barrier_u8`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	2s	2s	+0%
`ntt_native_aarch64`	LP64	bitwuzla	✅	19s	3s	+533%
	LP64	z3*	✅	2s	3s	-33%
`ntt_native_x86_64`	LP64	bitwuzla	⚠️	20s	3s	+567%
	LP64	z3*	✅	2s	3s	-33%
`nttunpack_native_x86_64`	LP64	cvc5_enum_inst	⚠️	70s	3s	+2233%
	LP64	z3*	✅	2s	3s	-33%
`poly_compress_d10_native_x86_64`	LP64	bitwuzla*	✅	3s	5s	-40%
	LP64	z3	✅	1s	5s	-80%
`poly_compress_d11_native_x86_64`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	1s	3s	-67%
`poly_compress_d4_native_x86_64`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	1s	3s	-67%
`poly_compress_d5_native_x86_64`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	2s	2s	+0%
`poly_decompress_d10_native_x86_64`	LP64	bitwuzla*	✅	3s	5s	-40%
	LP64	z3	✅	3s	5s	-40%
`poly_decompress_d11_native_x86_64`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	2s	1s	+100%
`poly_decompress_d4_native_x86_64`	LP64	bitwuzla*	✅	6s	6s	+0%
	LP64	z3	✅	3s	6s	-50%
`poly_decompress_d5_native_x86_64`	LP64	bitwuzla*	✅	4s	4s	+0%
	LP64	z3	✅	1s	4s	-75%
`poly_frombytes_native_x86_64`	LP64	bitwuzla*	✅	5s	5s	+0%
	LP64	z3	✅	3s	5s	-40%
`poly_invntt_tomont_native`	LP64	bitwuzla	✅	8s	2s	+300%
	LP64	z3*	✅	3s	2s	+50%
`poly_mulcache_compute_native_aarch64`	LP64	bitwuzla	✅	3s	6s	-50%
	LP64	z3*	✅	2s	6s	-67%
`poly_mulcache_compute_native_x86_64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`poly_ntt_native`	LP64	bitwuzla	✅	31s	39s	-21%
	LP64	z3*	✅	2s	39s	-95%
`poly_reduce_native_aarch64`	LP64	bitwuzla	✅	11s	2s	+450%
	LP64	z3*	✅	3s	2s	+50%
`poly_reduce_native_x86_64`	LP64	bitwuzla	✅	13s	2s	+550%
	LP64	z3*	✅	1s	2s	-50%
`poly_tobytes_native_aarch64`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	5s	1s	+400%
`poly_tobytes_native_x86_64`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`poly_tomont_native_aarch64`	LP64	bitwuzla	✅	11s	1s	+1000%
	LP64	z3*	✅	4s	1s	+300%
`poly_tomont_native_x86_64`	LP64	bitwuzla	✅	10s	1s	+900%
	LP64	z3*	✅	3s	1s	+200%
`polyvec_basemul_acc_montgomery_cached_k2_native_aarch64`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	4s	3s	+33%
`polyvec_basemul_acc_montgomery_cached_k2_native_x86_64`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	3s	4s	-25%
`polyvec_basemul_acc_montgomery_cached_k3_native_aarch64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`polyvec_basemul_acc_montgomery_cached_k3_native_x86_64`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`polyvec_basemul_acc_montgomery_cached_k4_native_aarch64`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	3s	1s	+200%
`polyvec_basemul_acc_montgomery_cached_k4_native_x86_64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`polyvec_basemul_acc_montgomery_cached_native`	LP64	cadical	✅	9s	14s	-36%
	LP64	z3*	✅	13s	14s	-7%
`rej_uniform_native`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3_smt_only	⚠️	39s	2s	+1850%
`rej_uniform_native_aarch64`	LP64	bitwuzla	✅	1s	45s	-98%
	LP64	z3*	✅	42s	45s	-7%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	2s	55s	-96%
	LP64	z3*	⚠️	117s	55s	+113%
`sys_check_capability`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%

oqs-bot · 2026-10-26T06:04:04Z

CBMC Results (ML-KEM-1024)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`kem_enc`	LP64	bitwuzla	⚠️	86s	2s	+4200%
`kem_keypair`	LP64	cadical	⚠️	99s	2s	+4850%
`kem_keypair_derand`	LP64	bitwuzla	⚠️	50s	1s	+4900%
`mlk_enc_getnoise_eta1_eta2`	LP64	cvc5_enum_inst	⚠️	22s	4s	+450%
`mlk_gen_matrix`	LP64	cadical	⚠️	106s	2s	+5200%
`mlk_gen_matrix_serial`	LP64	cadical	⚠️	114s	4s	+2750%
`mlk_indcpa_dec`	LP64	cadical	⚠️	86s	11s	+682%
`mlk_keccak_squeeze_once`	LP64	z3	⚠️	37s	10s	+270%
`mlk_keccak_squeezeblocks`	LP64	cvc5_arrays_exp	⚠️	20s	9s	+122%
`mlk_matvec_mul`	LP64	cadical	⚠️	35s	5s	+600%
`mlk_ntt_butterfly_block`	LP64	z3*	⚠️	302s	9s	+3256%
`mlk_poly_add`	LP64	bitwuzla	⚠️	57s	5s	+1040%
`mlk_poly_getnoise_eta1_4x`	LP64	cvc5_enum_inst	⚠️	80s	2s	+3900%
`mlk_poly_invntt_tomont_c`	LP64	bitwuzla	⚠️	57s	2s	+2750%
`mlk_poly_ntt_c`	LP64	bitwuzla	⚠️	68s	1s	+6700%
`mlk_poly_sub`	LP64	bitwuzla	⚠️	32s	8s	+300%
`mlk_polymat_permute_bitrev_to_custom`	LP64	cadical	⚠️	68s	5s	+1260%
`mlk_polyvec_add`	LP64	cadical	⚠️	118s	18s	+556%
`mlk_polyvec_basemul_acc_montgomery_cached_c`	LP64	z3*	⚠️	132s	79s	+67%
`mlk_polyvec_ntt`	LP64	cadical	⚠️	24s	12s	+100%
`mlk_shake256x4`	LP64	cvc5_arrays_exp	⚠️	34s	4s	+750%
`ntt_native_aarch64`	LP64	bitwuzla	⚠️	21s	3s	+600%
`ntt_native_x86_64`	LP64	bitwuzla	⚠️	21s	2s	+950%
`nttunpack_native_x86_64`	LP64	cvc5_enum_inst	⚠️	66s	2s	+3200%
`rej_uniform_native`	LP64	z3_smt_only	⚠️	35s	1s	+3400%
`rej_uniform_native_x86_64`	LP64	z3*	⚠️	112s	67s	+67%

Full Results (379 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	2144s	1885s	+13.7%
`intt_native_aarch64`	LP64	bitwuzla	✅	10s	3s	+233%
	LP64	z3*	✅	5s	3s	+67%
`intt_native_x86_64`	LP64	bitwuzla	✅	10s	2s	+400%
	LP64	z3*	✅	2s	2s	+0%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	3s	1s	+200%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	3s	2s	+50%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	1s	3s	-67%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	2s	3s	-33%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3	✅	1s	2s	-50%
`keccakf1600_permute_native`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3	✅	2s	2s	+0%
`keccakf1600x4_permute_native_x4`	LP64	bitwuzla*	✅	14s	15s	-7%
	LP64	z3	✅	19s	15s	+27%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	3s	2s	+50%
`kem_check_pk`	LP64	z3*	✅	5s	4s	+25%
`kem_check_sk`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`kem_dec`	LP64	bitwuzla	✅	5s	5s	+0%
	LP64	z3*	✅	7s	5s	+40%
`kem_enc`	LP64	bitwuzla	⚠️	86s	2s	+4200%
	LP64	z3*	✅	3s	2s	+50%
`kem_enc_derand`	LP64	cadical	✅	19s	3s	+533%
	LP64	z3*	✅	3s	3s	+0%
`kem_keypair`	LP64	cadical	⚠️	99s	2s	+4850%
	LP64	z3*	✅	3s	2s	+50%
`kem_keypair_derand`	LP64	bitwuzla	⚠️	50s	1s	+4900%
	LP64	z3*	✅	3s	1s	+200%
`mlk_barrett_reduce`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	4s	2s	+100%
`mlk_check_pct`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	4s	1s	+300%
`mlk_ct_cmask_neg_i16`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`mlk_ct_cmask_nonzero_u16`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mlk_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
`mlk_ct_cmov_zero`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	cvc5_mbqi_enum	✅	4s	3s	+33%
`mlk_ct_get_optblocker_i32`	ILP32	bitwuzla	✅	1s	3s	-67%
	ILP32	cvc5_arrays_exp	✅	1s	3s	-67%
	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*	✅	2s	3s	-33%
	LP64	z3	✅	3s	3s	+0%
`mlk_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	3s	2s	+50%
`mlk_ct_memcmp`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	cvc5_enum_inst	✅	2s	3s	-33%
`mlk_ct_sel_int16`	LP64	bitwuzla	✅	2s	4s	-50%
	LP64	z3*	✅	1s	4s	-75%
`mlk_ct_sel_uint8`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	2s	+100%
`mlk_enc_getnoise_eta1_eta2`	LP64	cvc5_enum_inst	⚠️	22s	4s	+450%
	LP64	z3*	✅	3s	4s	-25%
`mlk_fqmul`	LP64	bitwuzla	✅	2s	20s	-90%
	LP64	z3*	✅	5s	20s	-75%
`mlk_gen_matrix`	LP64	cadical	⚠️	106s	2s	+5200%
	LP64	z3*	✅	4s	2s	+100%
`mlk_gen_matrix_serial`	LP64	cadical	⚠️	114s	4s	+2750%
	LP64	z3*	✅	7s	4s	+75%
`mlk_indcpa_dec`	LP64	cadical	⚠️	86s	11s	+682%
	LP64	z3*	✅	17s	11s	+55%
`mlk_indcpa_enc`	LP64	z3_smt_only*	✅	445s	402s	+11%
`mlk_indcpa_keypair_derand`	LP64	z3*	✅	149s	176s	-15%
`mlk_invntt_layer`	LP64	bitwuzla	✅	3s	6s	-50%
	LP64	z3*	✅	5s	6s	-17%
`mlk_keccak_absorb_once`	LP64	bitwuzla*	✅	4s	4s	+0%
	LP64	z3	✅	2s	4s	-50%
`mlk_keccak_absorb_once_x4`	LP64	bitwuzla*	✅	9s	5s	+80%
	LP64	z3	✅	5s	5s	+0%
`mlk_keccak_squeeze_once`	LP64	bitwuzla*	✅	8s	10s	-20%
	LP64	z3	⚠️	37s	10s	+270%
`mlk_keccak_squeezeblocks`	LP64	bitwuzla*	✅	8s	9s	-11%
	LP64	cvc5_arrays_exp	⚠️	20s	9s	+122%
`mlk_keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	34s	26s	+31%
	LP64	cvc5_arrays_exp	✅	19s	26s	-27%
`mlk_keccakf1600_extract_bytes`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
`mlk_keccakf1600_extract_bytes (big endian)`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	1s	2s	-50%
`mlk_keccakf1600_permute`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mlk_keccakf1600_permute_c`	LP64	bitwuzla	✅	7s	6s	+17%
	LP64	z3*	✅	5s	6s	-17%
`mlk_keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3	✅	2s	1s	+100%
`mlk_keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	2s	2s	+0%
`mlk_keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	2s	2s	+0%
`mlk_keccakf1600x4_extract_bytes_c`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`mlk_keccakf1600x4_permute`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mlk_keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	2s	2s	+0%
`mlk_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	1s	5s	-80%
	LP64	z3*	✅	1s	5s	-80%
`mlk_keypair_getnoise_eta1`	LP64	cvc5_mbqi_enum	✅	17s	5s	+240%
	LP64	z3*	✅	2s	5s	-60%
`mlk_matvec_mul`	LP64	cadical	⚠️	35s	5s	+600%
	LP64	z3*	✅	2s	5s	-60%
`mlk_montgomery_reduce`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mlk_ntt_butterfly_block`	LP64	bitwuzla	✅	13s	9s	+44%
	LP64	z3*	⚠️	302s	9s	+3256%
`mlk_ntt_layer`	LP64	bitwuzla	✅	33s	38s	-13%
	LP64	z3*	✅	6s	38s	-84%
`mlk_poly_add`	LP64	bitwuzla	⚠️	57s	5s	+1040%
	LP64	z3*	✅	6s	5s	+20%
`mlk_poly_cbd_eta1`	LP64	bitwuzla	✅	16s	3s	+433%
	LP64	z3*	✅	2s	3s	-33%
`mlk_poly_cbd_eta2`	LP64	bitwuzla	✅	14s	3s	+367%
	LP64	z3*	✅	1s	3s	-67%
`mlk_poly_compress_d10`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
`mlk_poly_compress_d10_c`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`mlk_poly_compress_d10_native`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	3s	3s	+0%
`mlk_poly_compress_d11`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	1s	3s	-67%
`mlk_poly_compress_d11_c`	LP64	bitwuzla	✅	9s	4s	+125%
	LP64	z3*	✅	4s	4s	+0%
`mlk_poly_compress_d11_native`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	1s	3s	-67%
`mlk_poly_compress_d4`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	2s	3s	-33%
`mlk_poly_compress_d4_c`	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	2s	4s	-50%
`mlk_poly_compress_d4_native`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	1s	2s	-50%
`mlk_poly_compress_d5`	LP64	bitwuzla*	✅	2s	5s	-60%
	LP64	z3	✅	2s	5s	-60%
`mlk_poly_compress_d5_c`	LP64	bitwuzla	✅	8s	4s	+100%
	LP64	z3*	✅	3s	4s	-25%
`mlk_poly_compress_d5_native`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3	✅	1s	4s	-75%
`mlk_poly_compress_du`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	3s	2s	+50%
`mlk_poly_compress_dv`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	4s	1s	+300%
`mlk_poly_decompress_d10`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	3s	2s	+50%
`mlk_poly_decompress_d10_c`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`mlk_poly_decompress_d10_native`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	2s	2s	+0%
`mlk_poly_decompress_d11`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	3s	3s	+0%
`mlk_poly_decompress_d11_c`	LP64	bitwuzla	✅	11s	2s	+450%
	LP64	z3*	✅	2s	2s	+0%
`mlk_poly_decompress_d11_native`	LP64	bitwuzla*	✅	15s	16s	-6%
	LP64	z3	✅	1s	16s	-94%
`mlk_poly_decompress_d4`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	2s	3s	-33%
`mlk_poly_decompress_d4_c`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	3s	4s	-25%
`mlk_poly_decompress_d4_native`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	2s	3s	-33%
`mlk_poly_decompress_d5`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	1s	3s	-67%
`mlk_poly_decompress_d5_c`	LP64	bitwuzla	✅	12s	2s	+500%
	LP64	z3*	✅	1s	2s	-50%
`mlk_poly_decompress_d5_native`	LP64	bitwuzla*	✅	12s	18s	-33%
	LP64	z3	✅	3s	18s	-83%
`mlk_poly_decompress_du`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	3s	1s	+200%
`mlk_poly_decompress_dv`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	3s	2s	+50%
`mlk_poly_frombytes`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3	✅	3s	2s	+50%
`mlk_poly_frombytes_c`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	4s	3s	+33%
`mlk_poly_frombytes_native`	LP64	bitwuzla*	✅	13s	10s	+30%
	LP64	z3	✅	1s	10s	-90%
`mlk_poly_frommsg`	LP64	bitwuzla	✅	13s	10s	+30%
	LP64	z3*	✅	5s	10s	-50%
`mlk_poly_getnoise_eta1122_4x`	LP64	cvc5_mbqi_enum	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`mlk_poly_getnoise_eta1122_4x_serial`	LP64	cvc5_enum_inst	✅	2s	-	new
	LP64	z3*	✅	3s	-	new
`mlk_poly_getnoise_eta1_4x`	LP64	cvc5_enum_inst	⚠️	80s	2s	+3900%
	LP64	z3*	✅	2s	2s	+0%
`mlk_poly_getnoise_eta1_4x_serial`	LP64	cvc5_enum_inst	✅	85s	-	new
	LP64	z3*	✅	1s	-	new
`mlk_poly_getnoise_eta2`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
`mlk_poly_invntt_tomont`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`mlk_poly_invntt_tomont_c`	LP64	bitwuzla	⚠️	57s	2s	+2750%
	LP64	z3*	✅	2s	2s	+0%
`mlk_poly_mulcache_compute`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	1s	2s	-50%
`mlk_poly_mulcache_compute_c`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`mlk_poly_mulcache_compute_native`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`mlk_poly_ntt`	LP64	bitwuzla*	✅	9s	8s	+12%
	LP64	z3	✅	2s	8s	-75%
`mlk_poly_ntt_c`	LP64	bitwuzla	⚠️	68s	1s	+6700%
	LP64	z3*	✅	1s	1s	+0%
`mlk_poly_reduce`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	3s	2s	+50%
`mlk_poly_reduce_c`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	2s	1s	+100%
`mlk_poly_reduce_native`	LP64	bitwuzla*	✅	34s	40s	-15%
	LP64	z3	✅	4s	40s	-90%
`mlk_poly_rej_uniform`	LP64	bitwuzla*	✅	36s	161s	-78%
	LP64	z3	✅	3s	161s	-98%
`mlk_poly_rej_uniform_x4`	LP64	z3*	✅	7s	7s	+0%
`mlk_poly_sub`	LP64	bitwuzla	⚠️	32s	8s	+300%
	LP64	z3*	✅	7s	8s	-12%
`mlk_poly_tobytes`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	1s	3s	-67%
`mlk_poly_tobytes_c`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	4s	4s	+0%
`mlk_poly_tobytes_native`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	2s	1s	+100%
`mlk_poly_tomont`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mlk_poly_tomont_c`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	1s	3s	-67%
`mlk_poly_tomont_native`	LP64	bitwuzla	✅	13s	4s	+225%
	LP64	z3*	✅	3s	4s	-25%
`mlk_poly_tomsg`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	1s	3s	-67%
`mlk_polymat_permute_bitrev_to_custom`	LP64	cadical	⚠️	68s	5s	+1260%
	LP64	z3*	✅	4s	5s	-20%
`mlk_polymat_permute_bitrev_to_custom_native`	LP64	z3*	✅	111s	-	new
`mlk_polyvec_add`	LP64	cadical	⚠️	118s	18s	+556%
	LP64	z3*	✅	19s	18s	+6%
`mlk_polyvec_basemul_acc_montgomery_cached`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`mlk_polyvec_basemul_acc_montgomery_cached_c`	LP64	cadical	✅	24s	79s	-70%
	LP64	z3*	⚠️	132s	79s	+67%
`mlk_polyvec_compress_du`	LP64	cadical	✅	11s	3s	+267%
	LP64	z3*	✅	2s	3s	-33%
`mlk_polyvec_decompress_du`	LP64	cvc5_enum_inst	✅	10s	2s	+400%
	LP64	z3*	✅	2s	2s	+0%
`mlk_polyvec_frombytes`	LP64	cvc5_enum_inst	✅	9s	5s	+80%
	LP64	z3*	✅	2s	5s	-60%
`mlk_polyvec_invntt_tomont`	LP64	cvc5_enum_inst	✅	10s	1s	+900%
	LP64	z3*	✅	3s	1s	+200%
`mlk_polyvec_mulcache_compute`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	3s	4s	-25%
`mlk_polyvec_ntt`	LP64	cadical	⚠️	24s	12s	+100%
	LP64	z3*	✅	5s	12s	-58%
`mlk_polyvec_reduce`	LP64	cvc5_enum_inst	✅	10s	2s	+400%
	LP64	z3*	✅	4s	2s	+100%
`mlk_polyvec_tobytes`	LP64	cvc5_mbqi_enum	✅	7s	1s	+600%
	LP64	z3*	✅	2s	1s	+100%
`mlk_polyvec_tomont`	LP64	cvc5_enum_inst	✅	10s	2s	+400%
	LP64	z3*	✅	2s	2s	+0%
`mlk_rej_uniform`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	15s	2s	+650%
`mlk_rej_uniform_c`	LP64	bitwuzla	✅	2s	144s	-99%
	LP64	z3*	✅	158s	144s	+10%
`mlk_scalar_compress_d1`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`mlk_scalar_compress_d10`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`mlk_scalar_compress_d11`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	2s	4s	-50%
`mlk_scalar_compress_d4`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`mlk_scalar_compress_d5`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	2s	4s	-50%
`mlk_scalar_decompress_d10`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mlk_scalar_decompress_d11`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`mlk_scalar_decompress_d4`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`mlk_scalar_decompress_d5`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mlk_scalar_signed_to_unsigned_q`	LP64	bitwuzla	✅	4s	3s	+33%
	LP64	z3*	✅	1s	3s	-67%
`mlk_sha3_256`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	4s	2s	+100%
`mlk_sha3_512`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	2s	1s	+100%
`mlk_shake128_absorb_once`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	2s	2s	+0%
`mlk_shake128_squeezeblocks`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3	✅	3s	1s	+200%
`mlk_shake128x4_absorb_once`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	1s	2s	-50%
`mlk_shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
`mlk_shake256`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	2s	1s	+100%
`mlk_shake256x4`	LP64	bitwuzla*	✅	5s	4s	+25%
	LP64	cvc5_arrays_exp	⚠️	34s	4s	+750%
`mlk_value_barrier_i32`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	2s	3s	-33%
`mlk_value_barrier_u32`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	3s	3s	+0%
`mlk_value_barrier_u8`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	2s	1s	+100%
`ntt_native_aarch64`	LP64	bitwuzla	⚠️	21s	3s	+600%
	LP64	z3*	✅	3s	3s	+0%
`ntt_native_x86_64`	LP64	bitwuzla	⚠️	21s	2s	+950%
	LP64	z3*	✅	3s	2s	+50%
`nttunpack_native_x86_64`	LP64	cvc5_enum_inst	⚠️	66s	2s	+3200%
	LP64	z3*	✅	2s	2s	+0%
`poly_compress_d10_native_x86_64`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	4s	2s	+100%
`poly_compress_d11_native_x86_64`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	3s	3s	+0%
`poly_compress_d4_native_x86_64`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
`poly_compress_d5_native_x86_64`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3	✅	4s	4s	+0%
`poly_decompress_d10_native_x86_64`	LP64	bitwuzla*	✅	4s	4s	+0%
	LP64	z3	✅	4s	4s	+0%
`poly_decompress_d11_native_x86_64`	LP64	bitwuzla*	✅	5s	5s	+0%
	LP64	z3	✅	1s	5s	-80%
`poly_decompress_d4_native_x86_64`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	3s	2s	+50%
`poly_decompress_d5_native_x86_64`	LP64	bitwuzla*	✅	4s	5s	-20%
	LP64	z3	✅	4s	5s	-20%
`poly_frombytes_native_x86_64`	LP64	bitwuzla*	✅	4s	5s	-20%
	LP64	z3	✅	3s	5s	-40%
`poly_invntt_tomont_native`	LP64	bitwuzla	✅	8s	3s	+167%
	LP64	z3*	✅	2s	3s	-33%
`poly_mulcache_compute_native_aarch64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	1s	3s	-67%
`poly_mulcache_compute_native_x86_64`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	3s	5s	-40%
`poly_ntt_native`	LP64	bitwuzla	✅	34s	43s	-21%
	LP64	z3*	✅	3s	43s	-93%
`poly_reduce_native_aarch64`	LP64	bitwuzla	✅	12s	2s	+500%
	LP64	z3*	✅	3s	2s	+50%
`poly_reduce_native_x86_64`	LP64	bitwuzla	✅	16s	3s	+433%
	LP64	z3*	✅	4s	3s	+33%
`poly_tobytes_native_aarch64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`poly_tobytes_native_x86_64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`poly_tomont_native_aarch64`	LP64	bitwuzla	✅	11s	3s	+267%
	LP64	z3*	✅	2s	3s	-33%
`poly_tomont_native_x86_64`	LP64	bitwuzla	✅	12s	2s	+500%
	LP64	z3*	✅	1s	2s	-50%
`polyvec_basemul_acc_montgomery_cached_k2_native_aarch64`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	3s	1s	+200%
`polyvec_basemul_acc_montgomery_cached_k2_native_x86_64`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	4s	2s	+100%
`polyvec_basemul_acc_montgomery_cached_k3_native_aarch64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`polyvec_basemul_acc_montgomery_cached_k3_native_x86_64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyvec_basemul_acc_montgomery_cached_k4_native_aarch64`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	3s	2s	+50%
`polyvec_basemul_acc_montgomery_cached_k4_native_x86_64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`polyvec_basemul_acc_montgomery_cached_native`	LP64	cadical	✅	8s	31s	-74%
	LP64	z3*	✅	27s	31s	-13%
`rej_uniform_native`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3_smt_only	⚠️	35s	1s	+3400%
`rej_uniform_native_aarch64`	LP64	bitwuzla	✅	2s	53s	-96%
	LP64	z3*	✅	44s	53s	-17%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	3s	67s	-96%
	LP64	z3*	⚠️	112s	67s	+67%
`sys_check_capability`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%

oqs-bot · 2026-10-26T06:05:52Z

CBMC Results (ML-KEM-512)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	⚠️	2160s	1614s	+33.8%
`kem_enc`	LP64	bitwuzla	⚠️	24s	2s	+1100%
`kem_keypair`	LP64	cadical	⚠️	107s	4s	+2575%
`kem_keypair_derand`	LP64	bitwuzla	⚠️	27s	3s	+800%
`mlk_gen_matrix`	LP64	cadical	⚠️	23s	2s	+1050%
`mlk_gen_matrix_serial`	LP64	cadical	⚠️	23s	3s	+667%
`mlk_indcpa_dec`	LP64	cadical	⚠️	80s	14s	+471%
	LP64	z3*	⚠️	21s	14s	+50%
`mlk_keccak_squeeze_once`	LP64	z3	⚠️	35s	8s	+338%
`mlk_ntt_butterfly_block`	LP64	z3*	⚠️	325s	9s	+3511%
`mlk_poly_add`	LP64	bitwuzla	⚠️	93s	4s	+2225%
`mlk_poly_getnoise_eta1122_4x`	LP64	cvc5_mbqi_enum	⚠️	208s	3s	+6833%
`mlk_poly_getnoise_eta1_4x`	LP64	cvc5_enum_inst	⚠️	116s	5s	+2220%
`mlk_poly_invntt_tomont_c`	LP64	bitwuzla	⚠️	52s	3s	+1633%
`mlk_poly_ntt_c`	LP64	bitwuzla	⚠️	80s	2s	+3900%
`mlk_poly_sub`	LP64	bitwuzla	⚠️	38s	6s	+533%
`mlk_poly_tomont_native`	LP64	bitwuzla	⚠️	20s	2s	+900%
`mlk_polyvec_add`	LP64	cadical	⚠️	68s	11s	+518%
`mlk_polyvec_basemul_acc_montgomery_cached`	LP64	bitwuzla	⚠️	25s	1s	+2400%
`mlk_shake256x4`	LP64	cvc5_arrays_exp	⚠️	31s	5s	+520%
`ntt_native_aarch64`	LP64	bitwuzla	⚠️	23s	2s	+1050%
`ntt_native_x86_64`	LP64	bitwuzla	⚠️	28s	2s	+1300%
`nttunpack_native_x86_64`	LP64	cvc5_enum_inst	⚠️	69s	2s	+3350%
`rej_uniform_native`	LP64	z3_smt_only	⚠️	51s	1s	+5000%
`rej_uniform_native_x86_64`	LP64	z3*	⚠️	163s	57s	+186%

Full Results (379 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	⚠️	2160s	1614s	+33.8%
`intt_native_aarch64`	LP64	bitwuzla	✅	13s	2s	+550%
	LP64	z3*	✅	2s	2s	+0%
`intt_native_x86_64`	LP64	bitwuzla	✅	10s	2s	+400%
	LP64	z3*	✅	2s	2s	+0%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	4s	2s	+100%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	1s	3s	-67%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	1s	3s	-67%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	3s	3s	+0%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	2s	2s	+0%
`keccakf1600_permute_native`	LP64	bitwuzla*	✅	4s	1s	+300%
	LP64	z3	✅	1s	1s	+0%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	3s	1s	+200%
`keccakf1600x4_permute_native_x4`	LP64	bitwuzla*	✅	20s	16s	+25%
	LP64	z3	✅	18s	16s	+12%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	1s	1s	+0%
`kem_check_pk`	LP64	z3*	✅	3s	4s	-25%
`kem_check_sk`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`kem_dec`	LP64	bitwuzla	✅	4s	5s	-20%
	LP64	z3*	✅	12s	5s	+140%
`kem_enc`	LP64	bitwuzla	⚠️	24s	2s	+1100%
	LP64	z3*	✅	2s	2s	+0%
`kem_enc_derand`	LP64	cadical	✅	10s	3s	+233%
	LP64	z3*	✅	3s	3s	+0%
`kem_keypair`	LP64	cadical	⚠️	107s	4s	+2575%
	LP64	z3*	✅	4s	4s	+0%
`kem_keypair_derand`	LP64	bitwuzla	⚠️	27s	3s	+800%
	LP64	z3*	✅	2s	3s	-33%
`mlk_barrett_reduce`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mlk_check_pct`	LP64	bitwuzla*	✅	2s	5s	-60%
	LP64	z3	✅	5s	5s	+0%
`mlk_ct_cmask_neg_i16`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`mlk_ct_cmask_nonzero_u16`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`mlk_ct_cmask_nonzero_u8`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	1s	1s	+0%
`mlk_ct_cmov_zero`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	cvc5_mbqi_enum	✅	4s	3s	+33%
`mlk_ct_get_optblocker_i32`	ILP32	bitwuzla	✅	1s	2s	-50%
	ILP32	cvc5_arrays_exp	✅	2s	2s	+0%
	ILP32	z3	✅	2s	2s	+0%
	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3	✅	3s	2s	+50%
`mlk_ct_get_optblocker_u32`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	1s	3s	-67%
`mlk_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	1s	2s	-50%
`mlk_ct_memcmp`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	cvc5_enum_inst	✅	2s	3s	-33%
`mlk_ct_sel_int16`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	3s	1s	+200%
`mlk_ct_sel_uint8`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	4s	2s	+100%
`mlk_enc_getnoise_eta1_eta2`	LP64	cvc5_enum_inst	✅	12s	2s	+500%
	LP64	z3*	✅	2s	2s	+0%
`mlk_fqmul`	LP64	bitwuzla	✅	1s	17s	-94%
	LP64	z3*	✅	4s	17s	-76%
`mlk_gen_matrix`	LP64	cadical	⚠️	23s	2s	+1050%
	LP64	z3*	✅	5s	2s	+150%
`mlk_gen_matrix_serial`	LP64	cadical	⚠️	23s	3s	+667%
	LP64	z3*	✅	3s	3s	+0%
`mlk_indcpa_dec`	LP64	cadical	⚠️	80s	14s	+471%
	LP64	z3*	⚠️	21s	14s	+50%
`mlk_indcpa_enc`	LP64	z3_smt_only*	✅	369s	255s	+45%
`mlk_indcpa_keypair_derand`	LP64	z3*	✅	262s	213s	+23%
`mlk_invntt_layer`	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	8s	4s	+100%
`mlk_keccak_absorb_once`	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3	✅	3s	3s	+0%
`mlk_keccak_absorb_once_x4`	LP64	bitwuzla*	✅	7s	5s	+40%
	LP64	z3	✅	7s	5s	+40%
`mlk_keccak_squeeze_once`	LP64	bitwuzla*	✅	10s	8s	+25%
	LP64	z3	⚠️	35s	8s	+338%
`mlk_keccak_squeezeblocks`	LP64	bitwuzla*	✅	11s	9s	+22%
	LP64	cvc5_arrays_exp	✅	18s	9s	+100%
`mlk_keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	30s	26s	+15%
	LP64	cvc5_arrays_exp	✅	21s	26s	-19%
`mlk_keccakf1600_extract_bytes`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	2s	2s	+0%
`mlk_keccakf1600_extract_bytes (big endian)`	LP64	bitwuzla*	✅	2s	5s	-60%
	LP64	z3	✅	1s	5s	-80%
`mlk_keccakf1600_permute`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	1s	1s	+0%
`mlk_keccakf1600_permute_c`	LP64	bitwuzla	✅	6s	5s	+20%
	LP64	z3*	✅	5s	5s	+0%
`mlk_keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	3s	1s	+200%
`mlk_keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	4s	2s	+100%
`mlk_keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3	✅	2s	2s	+0%
`mlk_keccakf1600x4_extract_bytes_c`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	5s	3s	+67%
`mlk_keccakf1600x4_permute`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	2s	4s	-50%
`mlk_keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3	✅	1s	2s	-50%
`mlk_keccakf1600x4_xor_bytes_c`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`mlk_keypair_getnoise_eta1`	LP64	cvc5_mbqi_enum	✅	14s	1s	+1300%
	LP64	z3*	✅	2s	1s	+100%
`mlk_matvec_mul`	LP64	cadical	✅	8s	3s	+167%
	LP64	z3*	✅	3s	3s	+0%
`mlk_montgomery_reduce`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`mlk_ntt_butterfly_block`	LP64	bitwuzla	✅	15s	9s	+67%
	LP64	z3*	⚠️	325s	9s	+3511%
`mlk_ntt_layer`	LP64	bitwuzla	✅	41s	32s	+28%
	LP64	z3*	✅	6s	32s	-81%
`mlk_poly_add`	LP64	bitwuzla	⚠️	93s	4s	+2225%
	LP64	z3*	✅	5s	4s	+25%
`mlk_poly_cbd_eta1`	LP64	bitwuzla	✅	11s	2s	+450%
	LP64	z3*	✅	6s	2s	+200%
`mlk_poly_cbd_eta2`	LP64	bitwuzla	✅	14s	3s	+367%
	LP64	z3*	✅	2s	3s	-33%
`mlk_poly_compress_d10`	LP64	bitwuzla*	✅	2s	4s	-50%
	LP64	z3	✅	1s	4s	-75%
`mlk_poly_compress_d10_c`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
`mlk_poly_compress_d10_native`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	4s	1s	+300%
`mlk_poly_compress_d11`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	3s	3s	+0%
`mlk_poly_compress_d11_c`	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`mlk_poly_compress_d11_native`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	3s	3s	+0%
`mlk_poly_compress_d4`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	3s	3s	+0%
`mlk_poly_compress_d4_c`	LP64	bitwuzla	✅	13s	3s	+333%
	LP64	z3*	✅	4s	3s	+33%
`mlk_poly_compress_d4_native`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	6s	2s	+200%
`mlk_poly_compress_d5`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	2s	2s	+0%
`mlk_poly_compress_d5_c`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`mlk_poly_compress_d5_native`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	4s	3s	+33%
`mlk_poly_compress_du`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	3s	3s	+0%
`mlk_poly_compress_dv`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	2s	3s	-33%
`mlk_poly_decompress_d10`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	3s	2s	+50%
`mlk_poly_decompress_d10_c`	LP64	bitwuzla	✅	5s	4s	+25%
	LP64	z3*	✅	2s	4s	-50%
`mlk_poly_decompress_d10_native`	LP64	bitwuzla*	✅	16s	15s	+7%
	LP64	z3	✅	2s	15s	-87%
`mlk_poly_decompress_d11`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	3s	2s	+50%
`mlk_poly_decompress_d11_c`	LP64	bitwuzla	✅	4s	2s	+100%
	LP64	z3*	✅	2s	2s	+0%
`mlk_poly_decompress_d11_native`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	2s	3s	-33%
`mlk_poly_decompress_d4`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	4s	3s	+33%
`mlk_poly_decompress_d4_c`	LP64	bitwuzla	✅	4s	7s	-43%
	LP64	z3*	✅	3s	7s	-57%
`mlk_poly_decompress_d4_native`	LP64	bitwuzla*	✅	15s	14s	+7%
	LP64	z3	✅	2s	14s	-86%
`mlk_poly_decompress_d5`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	3s	1s	+200%
`mlk_poly_decompress_d5_c`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	5s	1s	+400%
`mlk_poly_decompress_d5_native`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
`mlk_poly_decompress_du`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	1s	2s	-50%
`mlk_poly_decompress_dv`	LP64	bitwuzla*	✅	1s	2s	-50%
	LP64	z3	✅	4s	2s	+100%
`mlk_poly_frombytes`	LP64	bitwuzla*	✅	1s	1s	+0%
	LP64	z3	✅	2s	1s	+100%
`mlk_poly_frombytes_c`	LP64	bitwuzla	✅	3s	4s	-25%
	LP64	z3*	✅	5s	4s	+25%
`mlk_poly_frombytes_native`	LP64	bitwuzla*	✅	11s	8s	+38%
	LP64	z3	✅	4s	8s	-50%
`mlk_poly_frommsg`	LP64	bitwuzla	✅	12s	10s	+20%
	LP64	z3*	✅	2s	10s	-80%
`mlk_poly_getnoise_eta1122_4x`	LP64	cvc5_mbqi_enum	⚠️	208s	3s	+6833%
	LP64	z3*	✅	2s	3s	-33%
`mlk_poly_getnoise_eta1122_4x_serial`	LP64	cvc5_enum_inst	✅	12s	-	new
	LP64	z3*	✅	3s	-	new
`mlk_poly_getnoise_eta1_4x`	LP64	cvc5_enum_inst	⚠️	116s	5s	+2220%
	LP64	z3*	✅	6s	5s	+20%
`mlk_poly_getnoise_eta1_4x_serial`	LP64	cvc5_enum_inst	✅	109s	-	new
	LP64	z3*	✅	3s	-	new
`mlk_poly_getnoise_eta2`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	2s	3s	-33%
`mlk_poly_invntt_tomont`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`mlk_poly_invntt_tomont_c`	LP64	bitwuzla	⚠️	52s	3s	+1633%
	LP64	z3*	✅	2s	3s	-33%
`mlk_poly_mulcache_compute`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	1s	2s	-50%
`mlk_poly_mulcache_compute_c`	LP64	bitwuzla	✅	1s	4s	-75%
	LP64	z3*	✅	5s	4s	+25%
`mlk_poly_mulcache_compute_native`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`mlk_poly_ntt`	LP64	bitwuzla*	✅	10s	5s	+100%
	LP64	z3	✅	2s	5s	-60%
`mlk_poly_ntt_c`	LP64	bitwuzla	⚠️	80s	2s	+3900%
	LP64	z3*	✅	3s	2s	+50%
`mlk_poly_reduce`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	3s	1s	+200%
`mlk_poly_reduce_c`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`mlk_poly_reduce_native`	LP64	bitwuzla*	✅	38s	35s	+9%
	LP64	z3	✅	3s	35s	-91%
`mlk_poly_rej_uniform`	LP64	bitwuzla*	✅	37s	150s	-75%
	LP64	z3	✅	2s	150s	-99%
`mlk_poly_rej_uniform_x4`	LP64	z3*	✅	9s	8s	+12%
`mlk_poly_sub`	LP64	bitwuzla	⚠️	38s	6s	+533%
	LP64	z3*	✅	8s	6s	+33%
`mlk_poly_tobytes`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	2s	3s	-33%
`mlk_poly_tobytes_c`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`mlk_poly_tobytes_native`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	3s	2s	+50%
`mlk_poly_tomont`	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`mlk_poly_tomont_c`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`mlk_poly_tomont_native`	LP64	bitwuzla	⚠️	20s	2s	+900%
	LP64	z3*	✅	3s	2s	+50%
`mlk_poly_tomsg`	LP64	bitwuzla*	✅	3s	3s	+0%
	LP64	z3	✅	3s	3s	+0%
`mlk_polymat_permute_bitrev_to_custom`	LP64	cadical	✅	15s	2s	+650%
	LP64	z3*	✅	2s	2s	+0%
`mlk_polymat_permute_bitrev_to_custom_native`	LP64	z3*	✅	33s	-	new
`mlk_polyvec_add`	LP64	cadical	⚠️	68s	11s	+518%
	LP64	z3*	✅	12s	11s	+9%
`mlk_polyvec_basemul_acc_montgomery_cached`	LP64	bitwuzla	⚠️	25s	1s	+2400%
	LP64	z3*	✅	1s	1s	+0%
`mlk_polyvec_basemul_acc_montgomery_cached_c`	LP64	cadical	✅	11s	55s	-80%
	LP64	z3*	✅	73s	55s	+33%
`mlk_polyvec_compress_du`	LP64	cadical	✅	8s	2s	+300%
	LP64	z3*	✅	3s	2s	+50%
`mlk_polyvec_decompress_du`	LP64	cvc5_enum_inst	✅	5s	2s	+150%
	LP64	z3*	✅	3s	2s	+50%
`mlk_polyvec_frombytes`	LP64	cvc5_enum_inst	✅	5s	2s	+150%
	LP64	z3*	✅	4s	2s	+100%
`mlk_polyvec_invntt_tomont`	LP64	cvc5_enum_inst	✅	7s	3s	+133%
	LP64	z3*	✅	1s	3s	-67%
`mlk_polyvec_mulcache_compute`	LP64	bitwuzla	✅	2s	5s	-60%
	LP64	z3*	✅	4s	5s	-20%
`mlk_polyvec_ntt`	LP64	cadical	✅	12s	1s	+1100%
	LP64	z3*	✅	2s	1s	+100%
`mlk_polyvec_reduce`	LP64	cvc5_enum_inst	✅	4s	2s	+100%
	LP64	z3*	✅	3s	2s	+50%
`mlk_polyvec_tobytes`	LP64	cvc5_mbqi_enum	✅	5s	3s	+67%
	LP64	z3*	✅	1s	3s	-67%
`mlk_polyvec_tomont`	LP64	cvc5_enum_inst	✅	5s	1s	+400%
	LP64	z3*	✅	3s	1s	+200%
`mlk_rej_uniform`	LP64	bitwuzla*	✅	2s	5s	-60%
	LP64	z3	✅	13s	5s	+160%
`mlk_rej_uniform_c`	LP64	bitwuzla	✅	1s	135s	-99%
	LP64	z3*	✅	164s	135s	+21%
`mlk_scalar_compress_d1`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mlk_scalar_compress_d10`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mlk_scalar_compress_d11`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`mlk_scalar_compress_d4`	LP64	bitwuzla	✅	3s	1s	+200%
	LP64	z3*	✅	3s	1s	+200%
`mlk_scalar_compress_d5`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	3s	2s	+50%
`mlk_scalar_decompress_d10`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mlk_scalar_decompress_d11`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	1s	2s	-50%
`mlk_scalar_decompress_d4`	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	z3*	✅	3s	3s	+0%
`mlk_scalar_decompress_d5`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`mlk_scalar_signed_to_unsigned_q`	LP64	bitwuzla	✅	5s	1s	+400%
	LP64	z3*	✅	2s	1s	+100%
`mlk_sha3_256`	LP64	bitwuzla*	✅	4s	2s	+100%
	LP64	z3	✅	2s	2s	+0%
`mlk_sha3_512`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	1s	2s	-50%
`mlk_shake128_absorb_once`	LP64	bitwuzla*	✅	1s	3s	-67%
	LP64	z3	✅	1s	3s	-67%
`mlk_shake128_squeezeblocks`	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3	✅	2s	3s	-33%
`mlk_shake128x4_absorb_once`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	3s	2s	+50%
`mlk_shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	4s	1s	+300%
`mlk_shake256`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	3s	2s	+50%
`mlk_shake256x4`	LP64	bitwuzla*	✅	3s	5s	-40%
	LP64	cvc5_arrays_exp	⚠️	31s	5s	+520%
`mlk_value_barrier_i32`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	2s	2s	+0%
`mlk_value_barrier_u32`	LP64	bitwuzla*	✅	2s	3s	-33%
	LP64	z3	✅	2s	3s	-33%
`mlk_value_barrier_u8`	LP64	bitwuzla*	✅	3s	4s	-25%
	LP64	z3	✅	4s	4s	+0%
`ntt_native_aarch64`	LP64	bitwuzla	⚠️	23s	2s	+1050%
	LP64	z3*	✅	2s	2s	+0%
`ntt_native_x86_64`	LP64	bitwuzla	⚠️	28s	2s	+1300%
	LP64	z3*	✅	3s	2s	+50%
`nttunpack_native_x86_64`	LP64	cvc5_enum_inst	⚠️	69s	2s	+3350%
	LP64	z3*	✅	2s	2s	+0%
`poly_compress_d10_native_x86_64`	LP64	bitwuzla*	✅	4s	3s	+33%
	LP64	z3	✅	4s	3s	+33%
`poly_compress_d11_native_x86_64`	LP64	bitwuzla*	✅	2s	2s	+0%
	LP64	z3	✅	4s	2s	+100%
`poly_compress_d4_native_x86_64`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3	✅	4s	1s	+300%
`poly_compress_d5_native_x86_64`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	3s	2s	+50%
`poly_decompress_d10_native_x86_64`	LP64	bitwuzla*	✅	6s	9s	-33%
	LP64	z3	✅	4s	9s	-56%
`poly_decompress_d11_native_x86_64`	LP64	bitwuzla*	✅	2s	1s	+100%
	LP64	z3	✅	1s	1s	+0%
`poly_decompress_d4_native_x86_64`	LP64	bitwuzla*	✅	6s	4s	+50%
	LP64	z3	✅	2s	4s	-50%
`poly_decompress_d5_native_x86_64`	LP64	bitwuzla*	✅	3s	2s	+50%
	LP64	z3	✅	1s	2s	-50%
`poly_frombytes_native_x86_64`	LP64	bitwuzla*	✅	3s	5s	-40%
	LP64	z3	✅	3s	5s	-40%
`poly_invntt_tomont_native`	LP64	bitwuzla	✅	11s	2s	+450%
	LP64	z3*	✅	3s	2s	+50%
`poly_mulcache_compute_native_aarch64`	LP64	bitwuzla	✅	5s	3s	+67%
	LP64	z3*	✅	4s	3s	+33%
`poly_mulcache_compute_native_x86_64`	LP64	bitwuzla	✅	7s	1s	+600%
	LP64	z3*	✅	2s	1s	+100%
`poly_ntt_native`	LP64	bitwuzla	✅	32s	45s	-29%
	LP64	z3*	✅	1s	45s	-98%
`poly_reduce_native_aarch64`	LP64	bitwuzla	✅	17s	1s	+1600%
	LP64	z3*	✅	2s	1s	+100%
`poly_reduce_native_x86_64`	LP64	bitwuzla	✅	16s	2s	+700%
	LP64	z3*	✅	2s	2s	+0%
`poly_tobytes_native_aarch64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`poly_tobytes_native_x86_64`	LP64	bitwuzla	✅	5s	1s	+400%
	LP64	z3*	✅	1s	1s	+0%
`poly_tomont_native_aarch64`	LP64	bitwuzla	✅	13s	2s	+550%
	LP64	z3*	✅	1s	2s	-50%
`poly_tomont_native_x86_64`	LP64	bitwuzla	✅	14s	2s	+600%
	LP64	z3*	✅	2s	2s	+0%
`polyvec_basemul_acc_montgomery_cached_k2_native_aarch64`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`polyvec_basemul_acc_montgomery_cached_k2_native_x86_64`	LP64	bitwuzla	✅	2s	3s	-33%
	LP64	z3*	✅	3s	3s	+0%
`polyvec_basemul_acc_montgomery_cached_k3_native_aarch64`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	3s	3s	+0%
`polyvec_basemul_acc_montgomery_cached_k3_native_x86_64`	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	z3*	✅	3s	2s	+50%
`polyvec_basemul_acc_montgomery_cached_k4_native_aarch64`	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	z3*	✅	2s	3s	-33%
`polyvec_basemul_acc_montgomery_cached_k4_native_x86_64`	LP64	bitwuzla	✅	3s	2s	+50%
	LP64	z3*	✅	2s	2s	+0%
`polyvec_basemul_acc_montgomery_cached_native`	LP64	cadical	✅	9s	8s	+12%
	LP64	z3*	✅	13s	8s	+62%
`rej_uniform_native`	LP64	bitwuzla*	✅	3s	1s	+200%
	LP64	z3_smt_only	⚠️	51s	1s	+5000%
`rej_uniform_native_aarch64`	LP64	bitwuzla	✅	3s	43s	-93%
	LP64	z3*	✅	52s	43s	+21%
`rej_uniform_native_x86_64`	LP64	bitwuzla	✅	3s	57s	-95%
	LP64	z3*	⚠️	163s	57s	+186%
`sys_check_capability`	LP64	bitwuzla	✅	1s	1s	+0%
	LP64	z3*	✅	2s	1s	+100%

mkannwischer

Thank you!

hanno-becker requested a review from a team as a code owner October 26, 2026 05:13

hanno-becker added enhancement New feature or request hol-light labels Oct 26, 2026

hanno-becker requested a review from mkannwischer October 26, 2026 05:13

mkannwischer approved these changes Oct 26, 2026

View reviewed changes

mkannwischer enabled auto-merge October 26, 2026 06:31

mkannwischer added this pull request to the merge queue Oct 26, 2026

Merged via the queue into main with commit 5093600 Oct 26, 2026
411 checks passed

mkannwischer deleted the hol-speedup branch October 26, 2026 08:38

mkannwischer mentioned this pull request Oct 26, 2026

Port: HOL-Light: Tweaks for better proof performance #1963

Closed

Navigation Menu

Repository navigation

HOL-Light: Avoid repeated work in proof loops - #1962

HOL-Light: Avoid repeated work in proof loops#1962
mkannwischer merged 1 commit into
mainfrom
hol-speedup

hanno-becker commented Oct 26, 2026

Uh oh!

oqs-bot commented Oct 26, 2026

Uh oh!

oqs-bot commented Oct 26, 2026

Uh oh!

oqs-bot commented Oct 26, 2026

Uh oh!

mkannwischer left a comment

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

hanno-becker commented Oct 26, 2026

Uh oh!

oqs-bot commented Oct 26, 2026

CBMC Results (ML-KEM-768)

Uh oh!

oqs-bot commented Oct 26, 2026

CBMC Results (ML-KEM-1024)

Uh oh!

oqs-bot commented Oct 26, 2026

CBMC Results (ML-KEM-512)

Uh oh!

mkannwischer left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants