nix: Take HOL Light from nixpkgs-unstable instead of pinning it by hanno-becker · Pull Request #1433 · pq-code-package/mldsa-native

hanno-becker · 2026-09-23T13:41:53Z

Based on HOL-Light/RV32-IM: Add correctness, safety and constant-time proof for arithmetic backend #1426

oqs-bot · 2026-09-23T14:16:48Z

CBMC Results (ML-DSA-44, REDUCE-RAM)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	31s	12s	+158%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	138s	19s	+626%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	43s	5s	+760%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	171s	49s	+249%

Full Results (229 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1240s	1364s	-9.1%
`caddq`	LP64	z3*	✅	2s	6s	-67%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	31s	12s	+158%
`decompose`	LP64	z3*	✅	3s	3s	+0%
`fqmul`	LP64	bitwuzla*	✅	24s	39s	-38%
`fqscale`	LP64	bitwuzla*	✅	4s	2s	+100%
`intt_native_aarch64`	LP64	z3*	✅	3s	3s	+0%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	3s	-	new
	LP64	z3	✅	1s	-	new
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	3s	-	new
`intt_native_x86_64`	LP64	z3*	✅	3s	2s	+50%
`keccak_absorb`	LP64	z3*	✅	3s	3s	+0%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	6s	8s	-25%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	4s	2s	+100%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	3s	-33%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	1s	2s	-50%
`keccak_finalize`	LP64	z3*	✅	2s	2s	+0%
`keccak_init`	LP64	z3*	✅	2s	3s	-33%
`keccak_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	1s	3s	-67%
`keccakf1600_extract_bytes (big endian)`	LP64	z3*	✅	2s	4s	-50%
`keccakf1600_permute`	LP64	z3*	✅	1s	2s	-50%
`keccakf1600_permute_native`	LP64	z3*	✅	1s	3s	-67%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	1s	3s	-67%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	2s	6s	-67%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	1s	4s	-75%
`keccakf1600x4_permute`	LP64	z3*	✅	2s	4s	-50%
`keccakf1600x4_permute_native`	LP64	z3*	✅	12s	22s	-45%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	1s	3s	-67%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	2s	5s	-60%
`make_hint`	LP64	z3*	✅	4s	3s	+33%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	138s	19s	+626%
`mld_check_pct`	LP64	z3*	✅	5s	15s	-67%
`mld_compute_pack_z`	LP64	z3_no_bv_extract*	✅	1s	6s	-83%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	2s	3s	-33%
	ILP32	cvc5_arrays_exp	✅	2s	3s	-33%
	ILP32	z3	✅	1s	3s	-67%
	LP64	bitwuzla	✅	3s	3s	+0%
	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`mld_ct_cmask_neg_i32`	LP64	z3*	✅	1s	2s	-50%
`mld_ct_cmask_nonzero_u32`	LP64	z3*	✅	1s	3s	-67%
`mld_ct_cmask_nonzero_u8`	LP64	z3*	✅	2s	2s	+0%
`mld_ct_get_optblocker_i64`	LP64	z3*	✅	3s	4s	-25%
`mld_ct_get_optblocker_u32`	LP64	z3*	✅	2s	2s	+0%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	3s	2s	+50%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	1s	1s	+0%
`mld_ct_sel_int32`	LP64	z3*	✅	1s	3s	-67%
`mld_h`	LP64	z3*	✅	3s	4s	-25%
`mld_invntt_layer`	LP64	bitwuzla*	✅	61s	105s	-42%
`mld_keccakf1600_extract_bytes`	LP64	z3*	✅	1s	2s	-50%
`mld_keccakf1600_permute_c`	LP64	z3*	✅	5s	7s	-29%
`mld_keccakf1600x4_extract_bytes_c`	LP64	z3*	✅	2s	4s	-50%
`mld_keccakf1600x4_xor_bytes_c`	LP64	z3*	✅	1s	4s	-75%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	14s	23s	-39%
`mld_ntt_layer`	LP64	bitwuzla*	✅	24s	41s	-41%
`mld_polymat_expand_entry`	LP64	z3*	✅	2s	2s	+0%
`mld_prepare_domain_separation_prefix`	LP64	z3*	✅	3s	3s	+0%
`mld_sample_s1_s2`	LP64	z3*	✅	4s	1s	+300%
`mld_sample_s1_s2_serial`	LP64	z3*	✅	3s	4s	-25%
`mld_sign_attempt`	LP64	z3*	✅	3s	-	new
`mld_sign_finish`	LP64	z3*	✅	5s	-	new
`mld_sign_resume`	LP64	z3*	✅	2s	-	new
`mld_value_barrier_i64`	LP64	z3*	✅	2s	3s	-33%
`mld_value_barrier_u32`	LP64	z3*	✅	2s	1s	+100%
`mld_value_barrier_u8`	LP64	z3*	✅	1s	4s	-75%
`montgomery_reduce`	LP64	z3*	✅	2s	2s	+0%
`ntt_native_aarch64`	LP64	z3*	✅	3s	4s	-25%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	1s	-	new
	LP64	z3	✅	2s	-	new
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	2s	-	new
`ntt_native_x86_64`	LP64	z3*	✅	1s	3s	-67%
`nttunpack_native_x86_64`	LP64	z3*	✅	4s	4s	+0%
`pack_sig_c`	LP64	z3*	✅	3s	5s	-40%
`pack_sig_h`	LP64	z3_no_bv_extract*	✅	2s	4s	-50%
`pack_sig_z`	LP64	z3*	✅	1s	2s	-50%
`pack_sk_rho_key_tr_s2`	LP64	z3*	✅	2s	5s	-60%
`pack_sk_s1`	LP64	z3*	✅	3s	3s	+0%
`pointwise_acc_native_aarch64`	LP64	z3_smt_only*	✅	4s	6s	-33%
`pointwise_acc_native_x86_64`	LP64	z3_smt_only*	✅	3s	4s	-25%
`pointwise_native_aarch64`	LP64	z3*	✅	2s	2s	+0%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	2s	-	new
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	1s	-	new
	LP64	z3	✅	1s	-	new
`pointwise_native_x86_64`	LP64	z3*	✅	1s	4s	-75%
`poly_add`	LP64	z3*	✅	5s	7s	-29%
`poly_caddq`	LP64	z3*	✅	2s	4s	-50%
`poly_caddq_c`	LP64	z3*	✅	4s	3s	+33%
`poly_caddq_native`	LP64	z3*	✅	3s	3s	+0%
`poly_caddq_native_aarch64`	LP64	z3*	✅	2s	3s	-33%
`poly_caddq_native_x86_64`	LP64	z3*	✅	1s	4s	-75%
`poly_challenge`	LP64	z3*	✅	2s	6s	-67%
`poly_chknorm`	LP64	z3*	✅	3s	3s	+0%
`poly_chknorm_c`	LP64	z3*	✅	7s	11s	-36%
`poly_chknorm_native`	LP64	z3*	✅	4s	4s	+0%
`poly_chknorm_native_aarch64`	LP64	z3*	✅	2s	2s	+0%
`poly_chknorm_native_x86_64`	LP64	z3*	✅	2s	2s	+0%
`poly_decompose`	LP64	z3*	✅	3s	2s	+50%
`poly_decompose_32_native_aarch64`	LP64	z3*	✅	1s	4s	-75%
`poly_decompose_88_native_aarch64`	LP64	z3*	✅	1s	3s	-67%
`poly_decompose_c`	LP64	z3*	✅	3s	5s	-40%
`poly_decompose_native`	LP64	z3*	✅	2s	2s	+0%
`poly_decompose_native_x86_64`	LP64	z3*	✅	1s	2s	-50%
`poly_invntt_tomont`	LP64	z3*	✅	2s	2s	+0%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	5s	11s	-55%
`poly_invntt_tomont_native`	LP64	z3*	✅	2s	3s	-33%
`poly_ntt`	LP64	z3*	✅	2s	3s	-33%
`poly_ntt_c`	LP64	z3_smt_only*	✅	10s	21s	-52%
`poly_ntt_native`	LP64	z3*	✅	2s	3s	-33%
`poly_permute_bitrev_to_custom_optional`	LP64	z3*	✅	2s	5s	-60%
`poly_permute_bitrev_to_custom_optional_native`	LP64	z3*	✅	3s	3s	+0%
`poly_pointwise_montgomery`	LP64	z3*	✅	1s	3s	-67%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	67s	112s	-40%
`poly_pointwise_montgomery_native`	LP64	z3*	✅	2s	2s	+0%
`poly_power2round`	LP64	z3*	✅	4s	4s	+0%
`poly_reduce`	LP64	z3*	✅	2s	4s	-50%
`poly_shiftl`	LP64	z3*	✅	1s	4s	-75%
`poly_sub`	LP64	z3*	✅	2s	3s	-33%
`poly_uniform`	LP64	z3*	✅	2s	3s	-33%
`poly_uniform_4x`	LP64	z3*	✅	1s	3s	-67%
`poly_uniform_eta`	LP64	z3*	✅	1s	2s	-50%
`poly_uniform_eta_4x`	LP64	z3*	✅	9s	12s	-25%
`poly_uniform_gamma1`	LP64	z3*	✅	2s	3s	-33%
`poly_uniform_gamma1_4x`	LP64	z3*	✅	4s	5s	-20%
`poly_use_hint`	LP64	z3*	✅	1s	2s	-50%
`poly_use_hint_c`	LP64	z3*	✅	4s	5s	-20%
`poly_use_hint_native`	LP64	z3*	✅	1s	3s	-67%
`poly_use_hint_native_aarch64`	LP64	z3*	✅	1s	3s	-67%
`poly_use_hint_native_x86_64`	LP64	z3*	✅	1s	-	new
`polyeta_pack`	LP64	z3*	✅	2s	3s	-33%
`polyeta_unpack`	LP64	z3*	✅	6s	14s	-57%
`polyt0_pack`	LP64	z3*	✅	4s	4s	+0%
`polyt0_unpack`	LP64	z3*	✅	8s	12s	-33%
`polyt1_pack`	LP64	z3*	✅	3s	3s	+0%
`polyt1_unpack`	LP64	z3*	✅	1s	2s	-50%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	2s	3s	-33%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	1s	4s	-75%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	5s	6s	-17%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	96s	149s	-36%
`polyveck_caddq`	LP64	z3*	✅	5s	3s	+67%
`polyveck_chknorm`	LP64	z3*	✅	3s	67s	-96%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	3s	-	new
`polyveck_invntt_tomont`	LP64	z3*	✅	4s	5s	-20%
`polyveck_ntt`	LP64	z3*	✅	2s	2s	+0%
`polyveck_pack_eta`	LP64	z3*	✅	1s	4s	-75%
`polyveck_reduce`	LP64	z3*	✅	3s	4s	-25%
`polyveck_unpack_eta`	LP64	z3*	✅	4s	2s	+100%
`polyvecl_chknorm`	LP64	z3*	✅	2s	11s	-82%
`polyvecl_ntt`	LP64	z3*	✅	3s	3s	+0%
`polyvecl_pack_eta`	LP64	z3*	✅	2s	2s	+0%
`polyvecl_pointwise_acc_montgomery`	LP64	z3_smt_only*	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	✅	2s	4s	-50%
`polyvecl_pointwise_acc_montgomery_native`	LP64	z3_smt_only*	✅	2s	3s	-33%
`polyvecl_uniform_gamma1`	LP64	z3*	✅	2s	2s	+0%
`polyvecl_uniform_gamma1_serial`	LP64	z3*	✅	1s	2s	-50%
`polyvecl_unpack_eta`	LP64	z3*	✅	1s	4s	-75%
`polyvecl_unpack_z`	LP64	z3*	✅	4s	3s	+33%
`polyw1_pack`	LP64	z3*	✅	4s	4s	+0%
`polyw1_pack_32`	LP64	z3*	✅	6s	3s	+100%
`polyw1_pack_88`	LP64	z3*	✅	1s	2s	-50%
`polyw1_unpack`	LP64	z3*	✅	3s	-	new
`polyw1_unpack_32`	LP64	z3*	✅	2s	-	new
`polyw1_unpack_88`	LP64	z3*	✅	3s	-	new
`polyz_pack`	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack`	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_17_native_aarch64`	LP64	z3*	✅	1s	2s	-50%
`polyz_unpack_19_native_aarch64`	LP64	z3*	✅	3s	4s	-25%
`polyz_unpack_c`	LP64	z3*	✅	6s	8s	-25%
`polyz_unpack_native`	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_native_x86_64`	LP64	z3*	✅	1s	3s	-67%
`power2round`	LP64	z3*	✅	1s	2s	-50%
`reduce32`	LP64	z3*	✅	2s	3s	-33%
`rej_eta`	LP64	bitwuzla*	✅	3s	5s	-40%
`rej_eta_c`	LP64	bitwuzla*	✅	1s	4s	-75%
`rej_eta_native`	LP64	bitwuzla*	✅	4s	3s	+33%
`rej_uniform`	LP64	z3*	✅	4s	8s	-50%
`rej_uniform_c`	LP64	z3*	✅	8s	16s	-50%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	1s	3s	-67%
`rej_uniform_eta_native_x86_64`	LP64	z3_smt_only*	✅	3s	-	new
`rej_uniform_native`	LP64	bitwuzla*	✅	3s	5s	-40%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	3s	3s	+0%
`rej_uniform_native_x86_64`	LP64	z3_smt_only*	✅	9s	-	new
`shake128_absorb`	LP64	z3*	✅	2s	3s	-33%
`shake128_finalize`	LP64	z3*	✅	2s	3s	-33%
`shake128_init`	LP64	z3*	✅	3s	2s	+50%
`shake128_release`	LP64	z3*	✅	1s	2s	-50%
`shake128_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	2s	2s	+0%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	2s	+0%
`shake256`	LP64	z3*	✅	2s	1s	+100%
`shake256_absorb`	LP64	z3*	✅	1s	2s	-50%
`shake256_finalize`	LP64	z3*	✅	2s	2s	+0%
`shake256_init`	LP64	z3*	✅	2s	4s	-50%
`shake256_release`	LP64	z3*	✅	3s	1s	+200%
`shake256_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	3s	1s	+200%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	2s	-50%
`sig_unpack_hints`	LP64	z3*	✅	12s	2s	+500%
`sign_keypair`	LP64	z3*	✅	4s	5s	-20%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	✅	15s	4s	+275%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	43s	5s	+760%
`sign_signature`	LP64	z3*	✅	2s	6s	-67%
`sign_signature_extmu`	LP64	z3*	✅	5s	4s	+25%
`sign_signature_internal`	LP64	z3_no_bv_extract*	✅	13s	4s	+225%
`sign_signature_pre_hash_internal`	LP64	z3*	✅	3s	4s	-25%
`sign_signature_pre_hash_shake256`	LP64	z3*	✅	5s	4s	+25%
`sign_verify`	LP64	z3*	✅	3s	4s	-25%
`sign_verify_extmu`	LP64	z3*	✅	2s	5s	-60%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	171s	49s	+249%
`sign_verify_pre_hash_internal`	LP64	z3*	✅	3s	5s	-40%
`sign_verify_pre_hash_shake256`	LP64	z3*	✅	2s	5s	-60%
`sk_s1hat_get_poly`	LP64	z3*	✅	2s	2s	+0%
`sk_s2hat_get_poly`	LP64	z3*	✅	1s	5s	-80%
`sk_t0hat_get_poly`	LP64	z3*	✅	2s	1s	+100%
`sys_check_capability`	LP64	z3*	✅	2s	2s	+0%
`unpack_pk_t1`	LP64	z3*	✅	2s	3s	-33%
`unpack_sk`	LP64	z3*	✅	2s	3s	-33%
`unpack_sk_s1hat`	LP64	z3*	✅	2s	3s	-33%
`unpack_sk_s2hat`	LP64	z3*	✅	2s	4s	-50%
`unpack_sk_t0hat`	LP64	z3*	✅	2s	2s	+0%
`use_hint`	LP64	z3*	✅	1s	2s	-50%
`yvec_get_poly`	LP64	z3*	✅	2s	3s	-33%
`yvec_init`	LP64	z3*	✅	4s	1s	+300%

oqs-bot · 2026-09-23T14:17:23Z

CBMC Results (ML-DSA-65, REDUCE-RAM)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	33s	7s	+371%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	108s	31s	+248%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	28s	3s	+833%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	55s	5s	+1000%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	186s	71s	+162%

Full Results (229 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1301s	1482s	-12.2%
`caddq`	LP64	z3*	✅	4s	2s	+100%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	33s	7s	+371%
`decompose`	LP64	z3*	✅	1s	4s	-75%
`fqmul`	LP64	bitwuzla*	✅	23s	40s	-43%
`fqscale`	LP64	bitwuzla*	✅	3s	3s	+0%
`intt_native_aarch64`	LP64	z3*	✅	2s	2s	+0%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	1s	-	new
	LP64	z3	✅	3s	-	new
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	3s	-	new
	LP64	z3	✅	2s	-	new
`intt_native_x86_64`	LP64	z3*	✅	3s	4s	-25%
`keccak_absorb`	LP64	z3*	✅	3s	3s	+0%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	3s	10s	-70%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	2s	2s	+0%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	3s	-33%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	1s	2s	-50%
`keccak_finalize`	LP64	z3*	✅	2s	2s	+0%
`keccak_init`	LP64	z3*	✅	3s	4s	-25%
`keccak_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	2s	4s	-50%
`keccakf1600_extract_bytes (big endian)`	LP64	z3*	✅	2s	3s	-33%
`keccakf1600_permute`	LP64	z3*	✅	1s	4s	-75%
`keccakf1600_permute_native`	LP64	z3*	✅	1s	2s	-50%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	4s	4s	+0%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	3s	2s	+50%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	2s	4s	-50%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	2s	1s	+100%
`keccakf1600x4_permute`	LP64	z3*	✅	2s	1s	+100%
`keccakf1600x4_permute_native`	LP64	z3*	✅	11s	22s	-50%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	2s	2s	+0%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	2s	2s	+0%
`make_hint`	LP64	z3*	✅	3s	3s	+0%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	108s	31s	+248%
`mld_check_pct`	LP64	z3*	✅	5s	12s	-58%
`mld_compute_pack_z`	LP64	z3_no_bv_extract*	✅	3s	5s	-40%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	2s	6s	-67%
	ILP32	cvc5_arrays_exp	✅	2s	6s	-67%
	ILP32	z3	✅	1s	6s	-83%
	LP64	bitwuzla	✅	2s	6s	-67%
	LP64	cvc5_arrays_exp	✅	1s	6s	-83%
	LP64	z3*	✅	1s	6s	-83%
`mld_ct_cmask_neg_i32`	LP64	z3*	✅	3s	3s	+0%
`mld_ct_cmask_nonzero_u32`	LP64	z3*	✅	2s	3s	-33%
`mld_ct_cmask_nonzero_u8`	LP64	z3*	✅	3s	2s	+50%
`mld_ct_get_optblocker_i64`	LP64	z3*	✅	2s	1s	+100%
`mld_ct_get_optblocker_u32`	LP64	z3*	✅	2s	3s	-33%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	3s	4s	-25%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	2s	4s	-50%
`mld_ct_sel_int32`	LP64	z3*	✅	1s	2s	-50%
`mld_h`	LP64	z3*	✅	3s	3s	+0%
`mld_invntt_layer`	LP64	bitwuzla*	✅	57s	108s	-47%
`mld_keccakf1600_extract_bytes`	LP64	z3*	✅	2s	2s	+0%
`mld_keccakf1600_permute_c`	LP64	z3*	✅	3s	7s	-57%
`mld_keccakf1600x4_extract_bytes_c`	LP64	z3*	✅	2s	2s	+0%
`mld_keccakf1600x4_xor_bytes_c`	LP64	z3*	✅	2s	2s	+0%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	12s	25s	-52%
`mld_ntt_layer`	LP64	bitwuzla*	✅	23s	43s	-47%
`mld_polymat_expand_entry`	LP64	z3*	✅	1s	3s	-67%
`mld_prepare_domain_separation_prefix`	LP64	z3*	✅	3s	4s	-25%
`mld_sample_s1_s2`	LP64	z3*	✅	3s	6s	-50%
`mld_sample_s1_s2_serial`	LP64	z3*	✅	3s	3s	+0%
`mld_sign_attempt`	LP64	z3*	✅	2s	-	new
`mld_sign_finish`	LP64	z3*	✅	4s	-	new
`mld_sign_resume`	LP64	z3*	✅	2s	-	new
`mld_value_barrier_i64`	LP64	z3*	✅	3s	2s	+50%
`mld_value_barrier_u32`	LP64	z3*	✅	1s	4s	-75%
`mld_value_barrier_u8`	LP64	z3*	✅	2s	1s	+100%
`montgomery_reduce`	LP64	z3*	✅	2s	1s	+100%
`ntt_native_aarch64`	LP64	z3*	✅	2s	3s	-33%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	3s	-	new
	LP64	z3	✅	2s	-	new
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	1s	-	new
	LP64	z3	✅	1s	-	new
`ntt_native_x86_64`	LP64	z3*	✅	2s	5s	-60%
`nttunpack_native_x86_64`	LP64	z3*	✅	2s	3s	-33%
`pack_sig_c`	LP64	z3*	✅	2s	3s	-33%
`pack_sig_h`	LP64	z3_no_bv_extract*	✅	3s	2s	+50%
`pack_sig_z`	LP64	z3*	✅	2s	1s	+100%
`pack_sk_rho_key_tr_s2`	LP64	z3*	✅	2s	2s	+0%
`pack_sk_s1`	LP64	z3*	✅	1s	3s	-67%
`pointwise_acc_native_aarch64`	LP64	z3_smt_only*	✅	3s	6s	-50%
`pointwise_acc_native_x86_64`	LP64	z3_smt_only*	✅	6s	5s	+20%
`pointwise_native_aarch64`	LP64	z3*	✅	3s	3s	+0%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	3s	-	new
	LP64	z3	✅	2s	-	new
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	3s	-	new
`pointwise_native_x86_64`	LP64	z3*	✅	5s	2s	+150%
`poly_add`	LP64	z3*	✅	4s	7s	-43%
`poly_caddq`	LP64	z3*	✅	5s	3s	+67%
`poly_caddq_c`	LP64	z3*	✅	3s	5s	-40%
`poly_caddq_native`	LP64	z3*	✅	2s	4s	-50%
`poly_caddq_native_aarch64`	LP64	z3*	✅	1s	2s	-50%
`poly_caddq_native_x86_64`	LP64	z3*	✅	2s	1s	+100%
`poly_challenge`	LP64	z3*	✅	2s	5s	-60%
`poly_chknorm`	LP64	z3*	✅	2s	3s	-33%
`poly_chknorm_c`	LP64	z3*	✅	8s	13s	-38%
`poly_chknorm_native`	LP64	z3*	✅	3s	4s	-25%
`poly_chknorm_native_aarch64`	LP64	z3*	✅	1s	2s	-50%
`poly_chknorm_native_x86_64`	LP64	z3*	✅	3s	4s	-25%
`poly_decompose`	LP64	z3*	✅	1s	2s	-50%
`poly_decompose_32_native_aarch64`	LP64	z3*	✅	2s	4s	-50%
`poly_decompose_88_native_aarch64`	LP64	z3*	✅	1s	2s	-50%
`poly_decompose_c`	LP64	z3*	✅	3s	8s	-62%
`poly_decompose_native`	LP64	z3*	✅	2s	5s	-60%
`poly_decompose_native_x86_64`	LP64	z3*	✅	1s	2s	-50%
`poly_invntt_tomont`	LP64	z3*	✅	1s	5s	-80%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	7s	10s	-30%
`poly_invntt_tomont_native`	LP64	z3*	✅	1s	5s	-80%
`poly_ntt`	LP64	z3*	✅	3s	2s	+50%
`poly_ntt_c`	LP64	z3_smt_only*	✅	11s	22s	-50%
`poly_ntt_native`	LP64	z3*	✅	3s	2s	+50%
`poly_permute_bitrev_to_custom_optional`	LP64	z3*	✅	2s	3s	-33%
`poly_permute_bitrev_to_custom_optional_native`	LP64	z3*	✅	1s	3s	-67%
`poly_pointwise_montgomery`	LP64	z3*	✅	1s	2s	-50%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	69s	116s	-41%
`poly_pointwise_montgomery_native`	LP64	z3*	✅	2s	4s	-50%
`poly_power2round`	LP64	z3*	✅	3s	7s	-57%
`poly_reduce`	LP64	z3*	✅	3s	4s	-25%
`poly_shiftl`	LP64	z3*	✅	2s	3s	-33%
`poly_sub`	LP64	z3*	✅	2s	4s	-50%
`poly_uniform`	LP64	z3*	✅	2s	2s	+0%
`poly_uniform_4x`	LP64	z3*	✅	3s	4s	-25%
`poly_uniform_eta`	LP64	z3*	✅	1s	5s	-80%
`poly_uniform_eta_4x`	LP64	z3*	✅	9s	13s	-31%
`poly_uniform_gamma1`	LP64	z3*	✅	2s	3s	-33%
`poly_uniform_gamma1_4x`	LP64	z3*	✅	3s	3s	+0%
`poly_use_hint`	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint_c`	LP64	z3*	✅	1s	2s	-50%
`poly_use_hint_native`	LP64	z3*	✅	3s	7s	-57%
`poly_use_hint_native_aarch64`	LP64	z3*	✅	2s	4s	-50%
`poly_use_hint_native_x86_64`	LP64	z3*	✅	2s	-	new
`polyeta_pack`	LP64	z3*	✅	1s	1s	+0%
`polyeta_unpack`	LP64	z3*	✅	4s	4s	+0%
`polyt0_pack`	LP64	z3*	✅	2s	5s	-60%
`polyt0_unpack`	LP64	z3*	✅	7s	13s	-46%
`polyt1_pack`	LP64	z3*	✅	3s	3s	+0%
`polyt1_unpack`	LP64	z3*	✅	2s	3s	-33%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	3s	6s	-50%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	1s	3s	-67%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	4s	8s	-50%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	156s	201s	-22%
`polyveck_caddq`	LP64	z3*	✅	4s	7s	-43%
`polyveck_chknorm`	LP64	z3*	✅	7s	36s	-81%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	5s	-	new
`polyveck_invntt_tomont`	LP64	z3*	✅	4s	7s	-43%
`polyveck_ntt`	LP64	z3*	✅	2s	4s	-50%
`polyveck_pack_eta`	LP64	z3*	✅	2s	3s	-33%
`polyveck_reduce`	LP64	z3*	✅	5s	6s	-17%
`polyveck_unpack_eta`	LP64	z3*	✅	1s	3s	-67%
`polyvecl_chknorm`	LP64	z3*	✅	5s	43s	-88%
`polyvecl_ntt`	LP64	z3*	✅	4s	7s	-43%
`polyvecl_pack_eta`	LP64	z3*	✅	1s	2s	-50%
`polyvecl_pointwise_acc_montgomery`	LP64	z3_smt_only*	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery_native`	LP64	z3_smt_only*	✅	3s	3s	+0%
`polyvecl_uniform_gamma1`	LP64	z3*	✅	4s	4s	+0%
`polyvecl_uniform_gamma1_serial`	LP64	z3*	✅	1s	1s	+0%
`polyvecl_unpack_eta`	LP64	z3*	✅	4s	2s	+100%
`polyvecl_unpack_z`	LP64	z3*	✅	3s	1s	+200%
`polyw1_pack`	LP64	z3*	✅	3s	3s	+0%
`polyw1_pack_32`	LP64	z3*	✅	1s	2s	-50%
`polyw1_pack_88`	LP64	z3*	✅	2s	3s	-33%
`polyw1_unpack`	LP64	z3*	✅	3s	-	new
`polyw1_unpack_32`	LP64	z3*	✅	2s	-	new
`polyw1_unpack_88`	LP64	z3*	✅	4s	-	new
`polyz_pack`	LP64	z3*	✅	1s	3s	-67%
`polyz_unpack`	LP64	z3*	✅	1s	3s	-67%
`polyz_unpack_17_native_aarch64`	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_19_native_aarch64`	LP64	z3*	✅	1s	5s	-80%
`polyz_unpack_c`	LP64	z3*	✅	4s	9s	-56%
`polyz_unpack_native`	LP64	z3*	✅	1s	3s	-67%
`polyz_unpack_native_x86_64`	LP64	z3*	✅	2s	3s	-33%
`power2round`	LP64	z3*	✅	1s	2s	-50%
`reduce32`	LP64	z3*	✅	3s	2s	+50%
`rej_eta`	LP64	bitwuzla*	✅	1s	5s	-80%
`rej_eta_c`	LP64	bitwuzla*	✅	1s	4s	-75%
`rej_eta_native`	LP64	bitwuzla*	✅	3s	3s	+0%
`rej_uniform`	LP64	z3*	✅	5s	7s	-29%
`rej_uniform_c`	LP64	z3*	✅	9s	16s	-44%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	1s	5s	-80%
`rej_uniform_eta_native_x86_64`	LP64	z3_smt_only*	✅	1s	-	new
`rej_uniform_native`	LP64	bitwuzla*	✅	4s	4s	+0%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	2s	5s	-60%
`rej_uniform_native_x86_64`	LP64	z3_smt_only*	✅	7s	-	new
`shake128_absorb`	LP64	z3*	✅	1s	2s	-50%
`shake128_finalize`	LP64	z3*	✅	2s	2s	+0%
`shake128_init`	LP64	z3*	✅	1s	6s	-83%
`shake128_release`	LP64	z3*	✅	2s	2s	+0%
`shake128_squeeze`	LP64	bitwuzla*	✅	2s	3s	-33%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	1s	2s	-50%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	2s	+0%
`shake256`	LP64	z3*	✅	2s	2s	+0%
`shake256_absorb`	LP64	z3*	✅	1s	4s	-75%
`shake256_finalize`	LP64	z3*	✅	2s	1s	+100%
`shake256_init`	LP64	z3*	✅	2s	4s	-50%
`shake256_release`	LP64	z3*	✅	1s	3s	-67%
`shake256_squeeze`	LP64	bitwuzla*	✅	1s	4s	-75%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	2s	2s	+0%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	2s	+0%
`sig_unpack_hints`	LP64	z3*	✅	11s	1s	+1000%
`sign_keypair`	LP64	z3*	✅	5s	4s	+25%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	28s	3s	+833%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	55s	5s	+1000%
`sign_signature`	LP64	z3*	✅	4s	5s	-20%
`sign_signature_extmu`	LP64	z3*	✅	3s	4s	-25%
`sign_signature_internal`	LP64	z3_no_bv_extract*	✅	13s	6s	+117%
`sign_signature_pre_hash_internal`	LP64	z3*	✅	1s	3s	-67%
`sign_signature_pre_hash_shake256`	LP64	z3*	✅	4s	7s	-43%
`sign_verify`	LP64	z3*	✅	2s	6s	-67%
`sign_verify_extmu`	LP64	z3*	✅	2s	2s	+0%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	186s	71s	+162%
`sign_verify_pre_hash_internal`	LP64	z3*	✅	2s	5s	-60%
`sign_verify_pre_hash_shake256`	LP64	z3*	✅	5s	6s	-17%
`sk_s1hat_get_poly`	LP64	z3*	✅	3s	3s	+0%
`sk_s2hat_get_poly`	LP64	z3*	✅	3s	1s	+200%
`sk_t0hat_get_poly`	LP64	z3*	✅	3s	1s	+200%
`sys_check_capability`	LP64	z3*	✅	2s	1s	+100%
`unpack_pk_t1`	LP64	z3*	✅	1s	2s	-50%
`unpack_sk`	LP64	z3*	✅	1s	3s	-67%
`unpack_sk_s1hat`	LP64	z3*	✅	2s	1s	+100%
`unpack_sk_s2hat`	LP64	z3*	✅	1s	3s	-67%
`unpack_sk_t0hat`	LP64	z3*	✅	1s	4s	-75%
`use_hint`	LP64	z3*	✅	2s	2s	+0%
`yvec_get_poly`	LP64	z3*	✅	2s	3s	-33%
`yvec_init`	LP64	z3*	✅	1s	5s	-80%

oqs-bot · 2026-09-23T14:17:43Z

CBMC Results (ML-DSA-87, REDUCE-RAM)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	27s	12s	+125%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	131s	34s	+285%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	36s	6s	+500%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	81s	6s	+1250%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	197s	47s	+319%

Full Results (229 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1357s	1436s	-5.5%
`caddq`	LP64	z3*	✅	2s	3s	-33%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	27s	12s	+125%
`decompose`	LP64	z3*	✅	1s	2s	-50%
`fqmul`	LP64	bitwuzla*	✅	25s	39s	-36%
`fqscale`	LP64	bitwuzla*	✅	2s	1s	+100%
`intt_native_aarch64`	LP64	z3*	✅	2s	4s	-50%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	4s	-	new
	LP64	z3	✅	2s	-	new
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	1s	-	new
	LP64	z3	✅	2s	-	new
`intt_native_x86_64`	LP64	z3*	✅	2s	4s	-50%
`keccak_absorb`	LP64	z3*	✅	2s	4s	-50%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	4s	8s	-50%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	1s	2s	-50%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	1s	1s	+0%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	3s	2s	+50%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	2s	3s	-33%
`keccak_finalize`	LP64	z3*	✅	2s	1s	+100%
`keccak_init`	LP64	z3*	✅	2s	1s	+100%
`keccak_squeeze`	LP64	bitwuzla*	✅	3s	5s	-40%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	4s	4s	+0%
`keccakf1600_extract_bytes (big endian)`	LP64	z3*	✅	1s	3s	-67%
`keccakf1600_permute`	LP64	z3*	✅	4s	2s	+100%
`keccakf1600_permute_native`	LP64	z3*	✅	2s	3s	-33%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	2s	1s	+100%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	1s	2s	-50%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	1s	1s	+0%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	3s	4s	-25%
`keccakf1600x4_permute`	LP64	z3*	✅	1s	2s	-50%
`keccakf1600x4_permute_native`	LP64	z3*	✅	13s	25s	-48%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	1s	1s	+0%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	1s	2s	-50%
`make_hint`	LP64	z3*	✅	3s	2s	+50%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	131s	34s	+285%
`mld_check_pct`	LP64	z3*	✅	4s	15s	-73%
`mld_compute_pack_z`	LP64	z3_no_bv_extract*	✅	2s	6s	-67%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	4s	1s	+300%
	ILP32	cvc5_arrays_exp	✅	3s	1s	+200%
	ILP32	z3	✅	1s	1s	+0%
	LP64	bitwuzla	✅	2s	1s	+100%
	LP64	cvc5_arrays_exp	✅	2s	1s	+100%
	LP64	z3*	✅	2s	1s	+100%
`mld_ct_cmask_neg_i32`	LP64	z3*	✅	2s	2s	+0%
`mld_ct_cmask_nonzero_u32`	LP64	z3*	✅	1s	5s	-80%
`mld_ct_cmask_nonzero_u8`	LP64	z3*	✅	4s	2s	+100%
`mld_ct_get_optblocker_i64`	LP64	z3*	✅	4s	2s	+100%
`mld_ct_get_optblocker_u32`	LP64	z3*	✅	2s	2s	+0%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	1s	3s	-67%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	1s	1s	+0%
`mld_ct_sel_int32`	LP64	z3*	✅	1s	2s	-50%
`mld_h`	LP64	z3*	✅	1s	2s	-50%
`mld_invntt_layer`	LP64	bitwuzla*	✅	57s	111s	-49%
`mld_keccakf1600_extract_bytes`	LP64	z3*	✅	1s	1s	+0%
`mld_keccakf1600_permute_c`	LP64	z3*	✅	4s	8s	-50%
`mld_keccakf1600x4_extract_bytes_c`	LP64	z3*	✅	3s	3s	+0%
`mld_keccakf1600x4_xor_bytes_c`	LP64	z3*	✅	3s	1s	+200%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	9s	23s	-61%
`mld_ntt_layer`	LP64	bitwuzla*	✅	22s	44s	-50%
`mld_polymat_expand_entry`	LP64	z3*	✅	1s	4s	-75%
`mld_prepare_domain_separation_prefix`	LP64	z3*	✅	2s	3s	-33%
`mld_sample_s1_s2`	LP64	z3*	✅	3s	8s	-62%
`mld_sample_s1_s2_serial`	LP64	z3*	✅	2s	6s	-67%
`mld_sign_attempt`	LP64	z3*	✅	2s	-	new
`mld_sign_finish`	LP64	z3*	✅	2s	-	new
`mld_sign_resume`	LP64	z3*	✅	4s	-	new
`mld_value_barrier_i64`	LP64	z3*	✅	2s	2s	+0%
`mld_value_barrier_u32`	LP64	z3*	✅	4s	3s	+33%
`mld_value_barrier_u8`	LP64	z3*	✅	2s	2s	+0%
`montgomery_reduce`	LP64	z3*	✅	3s	2s	+50%
`ntt_native_aarch64`	LP64	z3*	✅	2s	4s	-50%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	2s	-	new
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	3s	-	new
	LP64	z3	✅	2s	-	new
`ntt_native_x86_64`	LP64	z3*	✅	4s	2s	+100%
`nttunpack_native_x86_64`	LP64	z3*	✅	3s	3s	+0%
`pack_sig_c`	LP64	z3*	✅	1s	2s	-50%
`pack_sig_h`	LP64	z3_no_bv_extract*	✅	1s	3s	-67%
`pack_sig_z`	LP64	z3*	✅	1s	3s	-67%
`pack_sk_rho_key_tr_s2`	LP64	z3*	✅	1s	2s	-50%
`pack_sk_s1`	LP64	z3*	✅	3s	2s	+50%
`pointwise_acc_native_aarch64`	LP64	z3_smt_only*	✅	4s	5s	-20%
`pointwise_acc_native_x86_64`	LP64	z3_smt_only*	✅	5s	8s	-38%
`pointwise_native_aarch64`	LP64	z3*	✅	3s	4s	-25%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	2s	-	new
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	1s	-	new
`pointwise_native_x86_64`	LP64	z3*	✅	1s	5s	-80%
`poly_add`	LP64	z3*	✅	2s	8s	-75%
`poly_caddq`	LP64	z3*	✅	2s	5s	-60%
`poly_caddq_c`	LP64	z3*	✅	3s	3s	+0%
`poly_caddq_native`	LP64	z3*	✅	1s	3s	-67%
`poly_caddq_native_aarch64`	LP64	z3*	✅	3s	3s	+0%
`poly_caddq_native_x86_64`	LP64	z3*	✅	3s	3s	+0%
`poly_challenge`	LP64	z3*	✅	3s	4s	-25%
`poly_chknorm`	LP64	z3*	✅	3s	4s	-25%
`poly_chknorm_c`	LP64	z3*	✅	9s	13s	-31%
`poly_chknorm_native`	LP64	z3*	✅	2s	1s	+100%
`poly_chknorm_native_aarch64`	LP64	z3*	✅	2s	5s	-60%
`poly_chknorm_native_x86_64`	LP64	z3*	✅	2s	2s	+0%
`poly_decompose`	LP64	z3*	✅	2s	2s	+0%
`poly_decompose_32_native_aarch64`	LP64	z3*	✅	2s	3s	-33%
`poly_decompose_88_native_aarch64`	LP64	z3*	✅	1s	2s	-50%
`poly_decompose_c`	LP64	z3*	✅	4s	6s	-33%
`poly_decompose_native`	LP64	z3*	✅	2s	2s	+0%
`poly_decompose_native_x86_64`	LP64	z3*	✅	3s	3s	+0%
`poly_invntt_tomont`	LP64	z3*	✅	3s	4s	-25%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	4s	9s	-56%
`poly_invntt_tomont_native`	LP64	z3*	✅	2s	2s	+0%
`poly_ntt`	LP64	z3*	✅	1s	2s	-50%
`poly_ntt_c`	LP64	z3_smt_only*	✅	10s	19s	-47%
`poly_ntt_native`	LP64	z3*	✅	5s	4s	+25%
`poly_permute_bitrev_to_custom_optional`	LP64	z3*	✅	2s	2s	+0%
`poly_permute_bitrev_to_custom_optional_native`	LP64	z3*	✅	3s	3s	+0%
`poly_pointwise_montgomery`	LP64	z3*	✅	2s	3s	-33%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	68s	125s	-46%
`poly_pointwise_montgomery_native`	LP64	z3*	✅	2s	3s	-33%
`poly_power2round`	LP64	z3*	✅	3s	7s	-57%
`poly_reduce`	LP64	z3*	✅	2s	4s	-50%
`poly_shiftl`	LP64	z3*	✅	1s	4s	-75%
`poly_sub`	LP64	z3*	✅	2s	5s	-60%
`poly_uniform`	LP64	z3*	✅	3s	4s	-25%
`poly_uniform_4x`	LP64	z3*	✅	3s	3s	+0%
`poly_uniform_eta`	LP64	z3*	✅	3s	5s	-40%
`poly_uniform_eta_4x`	LP64	z3*	✅	8s	12s	-33%
`poly_uniform_gamma1`	LP64	z3*	✅	2s	3s	-33%
`poly_uniform_gamma1_4x`	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint`	LP64	z3*	✅	3s	4s	-25%
`poly_use_hint_c`	LP64	z3*	✅	1s	4s	-75%
`poly_use_hint_native`	LP64	z3*	✅	3s	1s	+200%
`poly_use_hint_native_aarch64`	LP64	z3*	✅	3s	3s	+0%
`poly_use_hint_native_x86_64`	LP64	z3*	✅	2s	-	new
`polyeta_pack`	LP64	z3*	✅	2s	3s	-33%
`polyeta_unpack`	LP64	z3*	✅	8s	13s	-38%
`polyt0_pack`	LP64	z3*	✅	4s	3s	+33%
`polyt0_unpack`	LP64	z3*	✅	7s	14s	-50%
`polyt1_pack`	LP64	z3*	✅	2s	5s	-60%
`polyt1_unpack`	LP64	z3*	✅	2s	3s	-33%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	1s	3s	-67%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	4s	3s	+33%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	5s	13s	-62%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	117s	196s	-40%
`polyveck_caddq`	LP64	z3*	✅	6s	8s	-25%
`polyveck_chknorm`	LP64	z3*	✅	3s	9s	-67%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	6s	-	new
`polyveck_invntt_tomont`	LP64	z3*	✅	2s	4s	-50%
`polyveck_ntt`	LP64	z3*	✅	2s	3s	-33%
`polyveck_pack_eta`	LP64	z3*	✅	2s	5s	-60%
`polyveck_reduce`	LP64	z3*	✅	3s	6s	-50%
`polyveck_unpack_eta`	LP64	z3*	✅	4s	3s	+33%
`polyvecl_chknorm`	LP64	z3*	✅	4s	38s	-89%
`polyvecl_ntt`	LP64	z3*	✅	4s	8s	-50%
`polyvecl_pack_eta`	LP64	z3*	✅	2s	2s	+0%
`polyvecl_pointwise_acc_montgomery`	LP64	z3_smt_only*	✅	2s	2s	+0%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	✅	3s	2s	+50%
`polyvecl_pointwise_acc_montgomery_native`	LP64	z3_smt_only*	✅	2s	2s	+0%
`polyvecl_uniform_gamma1`	LP64	z3*	✅	2s	3s	-33%
`polyvecl_uniform_gamma1_serial`	LP64	z3*	✅	2s	2s	+0%
`polyvecl_unpack_eta`	LP64	z3*	✅	1s	3s	-67%
`polyvecl_unpack_z`	LP64	z3*	✅	2s	3s	-33%
`polyw1_pack`	LP64	z3*	✅	1s	2s	-50%
`polyw1_pack_32`	LP64	z3*	✅	3s	3s	+0%
`polyw1_pack_88`	LP64	z3*	✅	2s	2s	+0%
`polyw1_unpack`	LP64	z3*	✅	3s	-	new
`polyw1_unpack_32`	LP64	z3*	✅	3s	-	new
`polyw1_unpack_88`	LP64	z3*	✅	2s	-	new
`polyz_pack`	LP64	z3*	✅	2s	4s	-50%
`polyz_unpack`	LP64	z3*	✅	3s	3s	+0%
`polyz_unpack_17_native_aarch64`	LP64	z3*	✅	2s	4s	-50%
`polyz_unpack_19_native_aarch64`	LP64	z3*	✅	2s	5s	-60%
`polyz_unpack_c`	LP64	z3*	✅	4s	7s	-43%
`polyz_unpack_native`	LP64	z3*	✅	1s	1s	+0%
`polyz_unpack_native_x86_64`	LP64	z3*	✅	3s	3s	+0%
`power2round`	LP64	z3*	✅	1s	3s	-67%
`reduce32`	LP64	z3*	✅	2s	3s	-33%
`rej_eta`	LP64	bitwuzla*	✅	1s	2s	-50%
`rej_eta_c`	LP64	bitwuzla*	✅	2s	4s	-50%
`rej_eta_native`	LP64	bitwuzla*	✅	1s	4s	-75%
`rej_uniform`	LP64	z3*	✅	3s	7s	-57%
`rej_uniform_c`	LP64	z3*	✅	8s	18s	-56%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	4s	3s	+33%
`rej_uniform_eta_native_x86_64`	LP64	z3_smt_only*	✅	3s	-	new
`rej_uniform_native`	LP64	bitwuzla*	✅	4s	5s	-20%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	2s	3s	-33%
`rej_uniform_native_x86_64`	LP64	z3_smt_only*	✅	8s	-	new
`shake128_absorb`	LP64	z3*	✅	5s	2s	+150%
`shake128_finalize`	LP64	z3*	✅	2s	2s	+0%
`shake128_init`	LP64	z3*	✅	3s	2s	+50%
`shake128_release`	LP64	z3*	✅	2s	3s	-33%
`shake128_squeeze`	LP64	bitwuzla*	✅	2s	1s	+100%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	2s	4s	-50%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	1s	+100%
`shake256`	LP64	z3*	✅	2s	3s	-33%
`shake256_absorb`	LP64	z3*	✅	2s	3s	-33%
`shake256_finalize`	LP64	z3*	✅	2s	3s	-33%
`shake256_init`	LP64	z3*	✅	3s	3s	+0%
`shake256_release`	LP64	z3*	✅	3s	5s	-40%
`shake256_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	2s	5s	-60%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	4s	4s	+0%
`sig_unpack_hints`	LP64	z3*	✅	11s	4s	+175%
`sign_keypair`	LP64	z3*	✅	5s	4s	+25%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	36s	6s	+500%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	81s	6s	+1250%
`sign_signature`	LP64	z3*	✅	3s	4s	-25%
`sign_signature_extmu`	LP64	z3*	✅	5s	4s	+25%
`sign_signature_internal`	LP64	z3_no_bv_extract*	✅	16s	3s	+433%
`sign_signature_pre_hash_internal`	LP64	z3*	✅	4s	2s	+100%
`sign_signature_pre_hash_shake256`	LP64	z3*	✅	6s	3s	+100%
`sign_verify`	LP64	z3*	✅	3s	2s	+50%
`sign_verify_extmu`	LP64	z3*	✅	3s	4s	-25%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	197s	47s	+319%
`sign_verify_pre_hash_internal`	LP64	z3*	✅	3s	3s	+0%
`sign_verify_pre_hash_shake256`	LP64	z3*	✅	5s	7s	-29%
`sk_s1hat_get_poly`	LP64	z3*	✅	2s	3s	-33%
`sk_s2hat_get_poly`	LP64	z3*	✅	2s	2s	+0%
`sk_t0hat_get_poly`	LP64	z3*	✅	3s	3s	+0%
`sys_check_capability`	LP64	z3*	✅	2s	2s	+0%
`unpack_pk_t1`	LP64	z3*	✅	1s	2s	-50%
`unpack_sk`	LP64	z3*	✅	2s	4s	-50%
`unpack_sk_s1hat`	LP64	z3*	✅	4s	3s	+33%
`unpack_sk_s2hat`	LP64	z3*	✅	2s	3s	-33%
`unpack_sk_t0hat`	LP64	z3*	✅	2s	4s	-50%
`use_hint`	LP64	z3*	✅	3s	3s	+0%
`yvec_get_poly`	LP64	z3*	✅	2s	2s	+0%
`yvec_init`	LP64	z3*	✅	3s	4s	-25%

oqs-bot · 2026-09-23T14:19:26Z

CBMC Results (ML-DSA-44)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	92s	50s	+84%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	136s	58s	+134%
`polyveck_chknorm`	LP64	z3*	⚠️	54s	5s	+980%
`sig_unpack_hints`	LP64	z3*	⚠️	21s	2s	+950%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	33s	5s	+560%
`sign_signature_internal`	LP64	z3_no_bv_extract*	⚠️	105s	26s	+304%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	264s	114s	+132%

Full Results (229 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1559s	1514s	+3.0%
`caddq`	LP64	z3*	✅	1s	2s	-50%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	92s	50s	+84%
`decompose`	LP64	z3*	✅	2s	2s	+0%
`fqmul`	LP64	bitwuzla*	✅	22s	39s	-44%
`fqscale`	LP64	bitwuzla*	✅	2s	3s	-33%
`intt_native_aarch64`	LP64	z3*	✅	3s	9s	-67%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	1s	-	new
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	3s	-	new
`intt_native_x86_64`	LP64	z3*	✅	1s	4s	-75%
`keccak_absorb`	LP64	z3*	✅	4s	5s	-20%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	4s	9s	-56%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	2s	2s	+0%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	3s	3s	+0%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	1s	+100%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	2s	3s	-33%
`keccak_finalize`	LP64	z3*	✅	4s	3s	+33%
`keccak_init`	LP64	z3*	✅	3s	3s	+0%
`keccak_squeeze`	LP64	bitwuzla*	✅	1s	1s	+0%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	2s	4s	-50%
`keccakf1600_extract_bytes (big endian)`	LP64	z3*	✅	1s	2s	-50%
`keccakf1600_permute`	LP64	z3*	✅	3s	2s	+50%
`keccakf1600_permute_native`	LP64	z3*	✅	2s	3s	-33%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	1s	1s	+0%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	1s	4s	-75%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	1s	2s	-50%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	2s	3s	-33%
`keccakf1600x4_permute`	LP64	z3*	✅	3s	4s	-25%
`keccakf1600x4_permute_native`	LP64	z3*	✅	12s	22s	-45%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	4s	2s	+100%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	3s	3s	+0%
`make_hint`	LP64	z3*	✅	1s	3s	-67%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	136s	58s	+134%
`mld_check_pct`	LP64	z3*	✅	7s	14s	-50%
`mld_compute_pack_z`	LP64	z3_no_bv_extract*	✅	4s	7s	-43%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	1s	2s	-50%
	ILP32	cvc5_arrays_exp	✅	2s	2s	+0%
	ILP32	z3	✅	1s	2s	-50%
	LP64	bitwuzla	✅	1s	2s	-50%
	LP64	cvc5_arrays_exp	✅	2s	2s	+0%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_cmask_neg_i32`	LP64	z3*	✅	1s	3s	-67%
`mld_ct_cmask_nonzero_u32`	LP64	z3*	✅	3s	2s	+50%
`mld_ct_cmask_nonzero_u8`	LP64	z3*	✅	2s	2s	+0%
`mld_ct_get_optblocker_i64`	LP64	z3*	✅	2s	4s	-50%
`mld_ct_get_optblocker_u32`	LP64	z3*	✅	3s	1s	+200%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	1s	1s	+0%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	3s	3s	+0%
`mld_ct_sel_int32`	LP64	z3*	✅	3s	2s	+50%
`mld_h`	LP64	z3*	✅	3s	4s	-25%
`mld_invntt_layer`	LP64	bitwuzla*	✅	57s	107s	-47%
`mld_keccakf1600_extract_bytes`	LP64	z3*	✅	1s	2s	-50%
`mld_keccakf1600_permute_c`	LP64	z3*	✅	4s	8s	-50%
`mld_keccakf1600x4_extract_bytes_c`	LP64	z3*	✅	1s	2s	-50%
`mld_keccakf1600x4_xor_bytes_c`	LP64	z3*	✅	1s	2s	-50%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	11s	23s	-52%
`mld_ntt_layer`	LP64	bitwuzla*	✅	21s	42s	-50%
`mld_polymat_expand_entry`	LP64	z3*	✅	1s	3s	-67%
`mld_prepare_domain_separation_prefix`	LP64	z3*	✅	1s	4s	-75%
`mld_sample_s1_s2`	LP64	z3*	✅	2s	4s	-50%
`mld_sample_s1_s2_serial`	LP64	z3*	✅	3s	3s	+0%
`mld_sign_attempt`	LP64	z3*	✅	1s	-	new
`mld_sign_finish`	LP64	z3*	✅	2s	-	new
`mld_sign_resume`	LP64	z3*	✅	3s	-	new
`mld_value_barrier_i64`	LP64	z3*	✅	1s	2s	-50%
`mld_value_barrier_u32`	LP64	z3*	✅	2s	2s	+0%
`mld_value_barrier_u8`	LP64	z3*	✅	1s	3s	-67%
`montgomery_reduce`	LP64	z3*	✅	1s	3s	-67%
`ntt_native_aarch64`	LP64	z3*	✅	3s	3s	+0%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	1s	-	new
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	2s	-	new
`ntt_native_x86_64`	LP64	z3*	✅	1s	3s	-67%
`nttunpack_native_x86_64`	LP64	z3*	✅	1s	1s	+0%
`pack_sig_c`	LP64	z3*	✅	2s	2s	+0%
`pack_sig_h`	LP64	z3_no_bv_extract*	✅	2s	3s	-33%
`pack_sig_z`	LP64	z3*	✅	1s	4s	-75%
`pack_sk_rho_key_tr_s2`	LP64	z3*	✅	5s	3s	+67%
`pack_sk_s1`	LP64	z3*	✅	2s	2s	+0%
`pointwise_acc_native_aarch64`	LP64	z3_smt_only*	✅	3s	4s	-25%
`pointwise_acc_native_x86_64`	LP64	z3_smt_only*	✅	4s	7s	-43%
`pointwise_native_aarch64`	LP64	z3*	✅	3s	5s	-40%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	1s	-	new
	LP64	z3	✅	1s	-	new
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	2s	-	new
`pointwise_native_x86_64`	LP64	z3*	✅	4s	4s	+0%
`poly_add`	LP64	z3*	✅	3s	7s	-57%
`poly_caddq`	LP64	z3*	✅	3s	2s	+50%
`poly_caddq_c`	LP64	z3*	✅	2s	2s	+0%
`poly_caddq_native`	LP64	z3*	✅	3s	5s	-40%
`poly_caddq_native_aarch64`	LP64	z3*	✅	1s	4s	-75%
`poly_caddq_native_x86_64`	LP64	z3*	✅	1s	4s	-75%
`poly_challenge`	LP64	z3*	✅	3s	3s	+0%
`poly_chknorm`	LP64	z3*	✅	2s	4s	-50%
`poly_chknorm_c`	LP64	z3*	✅	7s	17s	-59%
`poly_chknorm_native`	LP64	z3*	✅	3s	4s	-25%
`poly_chknorm_native_aarch64`	LP64	z3*	✅	2s	4s	-50%
`poly_chknorm_native_x86_64`	LP64	z3*	✅	2s	2s	+0%
`poly_decompose`	LP64	z3*	✅	3s	3s	+0%
`poly_decompose_32_native_aarch64`	LP64	z3*	✅	3s	2s	+50%
`poly_decompose_88_native_aarch64`	LP64	z3*	✅	2s	4s	-50%
`poly_decompose_c`	LP64	z3*	✅	4s	4s	+0%
`poly_decompose_native`	LP64	z3*	✅	5s	3s	+67%
`poly_decompose_native_x86_64`	LP64	z3*	✅	1s	3s	-67%
`poly_invntt_tomont`	LP64	z3*	✅	2s	4s	-50%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	5s	11s	-55%
`poly_invntt_tomont_native`	LP64	z3*	✅	1s	4s	-75%
`poly_ntt`	LP64	z3*	✅	1s	3s	-67%
`poly_ntt_c`	LP64	z3_smt_only*	✅	10s	19s	-47%
`poly_ntt_native`	LP64	z3*	✅	1s	5s	-80%
`poly_permute_bitrev_to_custom_optional`	LP64	z3*	✅	2s	2s	+0%
`poly_permute_bitrev_to_custom_optional_native`	LP64	z3*	✅	2s	4s	-50%
`poly_pointwise_montgomery`	LP64	z3*	✅	3s	3s	+0%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	43s	114s	-62%
`poly_pointwise_montgomery_native`	LP64	z3*	✅	3s	2s	+50%
`poly_power2round`	LP64	z3*	✅	3s	4s	-25%
`poly_reduce`	LP64	z3*	✅	1s	3s	-67%
`poly_shiftl`	LP64	z3*	✅	3s	3s	+0%
`poly_sub`	LP64	z3*	✅	2s	3s	-33%
`poly_uniform`	LP64	z3*	✅	1s	6s	-83%
`poly_uniform_4x`	LP64	z3*	✅	7s	14s	-50%
`poly_uniform_eta`	LP64	z3*	✅	1s	5s	-80%
`poly_uniform_eta_4x`	LP64	z3*	✅	6s	11s	-45%
`poly_uniform_gamma1`	LP64	z3*	✅	2s	4s	-50%
`poly_uniform_gamma1_4x`	LP64	z3*	✅	2s	5s	-60%
`poly_use_hint`	LP64	z3*	✅	5s	4s	+25%
`poly_use_hint_c`	LP64	z3*	✅	3s	3s	+0%
`poly_use_hint_native`	LP64	z3*	✅	1s	4s	-75%
`poly_use_hint_native_aarch64`	LP64	z3*	✅	1s	2s	-50%
`poly_use_hint_native_x86_64`	LP64	z3*	✅	3s	-	new
`polyeta_pack`	LP64	z3*	✅	2s	3s	-33%
`polyeta_unpack`	LP64	z3*	✅	4s	14s	-71%
`polyt0_pack`	LP64	z3*	✅	2s	2s	+0%
`polyt0_unpack`	LP64	z3*	✅	7s	15s	-53%
`polyt1_pack`	LP64	z3*	✅	3s	4s	-25%
`polyt1_unpack`	LP64	z3*	✅	2s	5s	-60%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	16s	28s	-43%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	3s	8s	-62%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	2s	2s	+0%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	9s	15s	-40%
`polyveck_caddq`	LP64	z3*	✅	3s	3s	+0%
`polyveck_chknorm`	LP64	z3*	⚠️	54s	5s	+980%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	4s	-	new
`polyveck_invntt_tomont`	LP64	z3*	✅	2s	5s	-60%
`polyveck_ntt`	LP64	z3*	✅	2s	5s	-60%
`polyveck_pack_eta`	LP64	z3*	✅	1s	2s	-50%
`polyveck_reduce`	LP64	z3*	✅	2s	5s	-60%
`polyveck_unpack_eta`	LP64	z3*	✅	2s	2s	+0%
`polyvecl_chknorm`	LP64	z3*	✅	3s	10s	-70%
`polyvecl_ntt`	LP64	z3*	✅	3s	2s	+50%
`polyvecl_pack_eta`	LP64	z3*	✅	4s	3s	+33%
`polyvecl_pointwise_acc_montgomery`	LP64	z3_smt_only*	✅	1s	4s	-75%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	✅	136s	131s	+4%
`polyvecl_pointwise_acc_montgomery_native`	LP64	z3_smt_only*	✅	3s	2s	+50%
`polyvecl_uniform_gamma1`	LP64	z3*	✅	4s	3s	+33%
`polyvecl_uniform_gamma1_serial`	LP64	z3*	✅	3s	2s	+50%
`polyvecl_unpack_eta`	LP64	z3*	✅	2s	2s	+0%
`polyvecl_unpack_z`	LP64	z3*	✅	1s	2s	-50%
`polyw1_pack`	LP64	z3*	✅	3s	3s	+0%
`polyw1_pack_32`	LP64	z3*	✅	4s	2s	+100%
`polyw1_pack_88`	LP64	z3*	✅	1s	1s	+0%
`polyw1_unpack`	LP64	z3*	✅	1s	-	new
`polyw1_unpack_32`	LP64	z3*	✅	3s	-	new
`polyw1_unpack_88`	LP64	z3*	✅	5s	-	new
`polyz_pack`	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack`	LP64	z3*	✅	3s	3s	+0%
`polyz_unpack_17_native_aarch64`	LP64	z3*	✅	1s	5s	-80%
`polyz_unpack_19_native_aarch64`	LP64	z3*	✅	2s	5s	-60%
`polyz_unpack_c`	LP64	z3*	✅	5s	11s	-55%
`polyz_unpack_native`	LP64	z3*	✅	2s	2s	+0%
`polyz_unpack_native_x86_64`	LP64	z3*	✅	2s	3s	-33%
`power2round`	LP64	z3*	✅	3s	3s	+0%
`reduce32`	LP64	z3*	✅	4s	2s	+100%
`rej_eta`	LP64	bitwuzla*	✅	4s	3s	+33%
`rej_eta_c`	LP64	bitwuzla*	✅	2s	4s	-50%
`rej_eta_native`	LP64	bitwuzla*	✅	3s	6s	-50%
`rej_uniform`	LP64	z3*	✅	10s	18s	-44%
`rej_uniform_c`	LP64	z3*	✅	8s	15s	-47%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	1s	2s	-50%
`rej_uniform_eta_native_x86_64`	LP64	z3_smt_only*	✅	2s	-	new
`rej_uniform_native`	LP64	bitwuzla*	✅	4s	4s	+0%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	1s	5s	-80%
`rej_uniform_native_x86_64`	LP64	z3_smt_only*	✅	6s	-	new
`shake128_absorb`	LP64	z3*	✅	1s	2s	-50%
`shake128_finalize`	LP64	z3*	✅	1s	2s	-50%
`shake128_init`	LP64	z3*	✅	2s	3s	-33%
`shake128_release`	LP64	z3*	✅	1s	1s	+0%
`shake128_squeeze`	LP64	bitwuzla*	✅	1s	1s	+0%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	1s	3s	-67%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	1s	+0%
`shake256`	LP64	z3*	✅	1s	1s	+0%
`shake256_absorb`	LP64	z3*	✅	2s	3s	-33%
`shake256_finalize`	LP64	z3*	✅	3s	2s	+50%
`shake256_init`	LP64	z3*	✅	1s	3s	-67%
`shake256_release`	LP64	z3*	✅	4s	2s	+100%
`shake256_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	1s	3s	-67%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	4s	-75%
`sig_unpack_hints`	LP64	z3*	⚠️	21s	2s	+950%
`sign_keypair`	LP64	z3*	✅	7s	4s	+75%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	✅	17s	4s	+325%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	33s	5s	+560%
`sign_signature`	LP64	z3*	✅	3s	3s	+0%
`sign_signature_extmu`	LP64	z3*	✅	1s	4s	-75%
`sign_signature_internal`	LP64	z3_no_bv_extract*	⚠️	105s	26s	+304%
`sign_signature_pre_hash_internal`	LP64	z3*	✅	2s	6s	-67%
`sign_signature_pre_hash_shake256`	LP64	z3*	✅	5s	3s	+67%
`sign_verify`	LP64	z3*	✅	3s	4s	-25%
`sign_verify_extmu`	LP64	z3*	✅	1s	3s	-67%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	264s	114s	+132%
`sign_verify_pre_hash_internal`	LP64	z3*	✅	3s	3s	+0%
`sign_verify_pre_hash_shake256`	LP64	z3*	✅	4s	5s	-20%
`sk_s1hat_get_poly`	LP64	z3*	✅	5s	3s	+67%
`sk_s2hat_get_poly`	LP64	z3*	✅	2s	2s	+0%
`sk_t0hat_get_poly`	LP64	z3*	✅	1s	2s	-50%
`sys_check_capability`	LP64	z3*	✅	2s	4s	-50%
`unpack_pk_t1`	LP64	z3*	✅	2s	5s	-60%
`unpack_sk`	LP64	z3*	✅	3s	3s	+0%
`unpack_sk_s1hat`	LP64	z3*	✅	2s	1s	+100%
`unpack_sk_s2hat`	LP64	z3*	✅	2s	4s	-50%
`unpack_sk_t0hat`	LP64	z3*	✅	2s	3s	-33%
`use_hint`	LP64	z3*	✅	3s	2s	+50%
`yvec_get_poly`	LP64	z3*	✅	1s	3s	-67%
`yvec_init`	LP64	z3*	✅	2s	3s	-33%

oqs-bot · 2026-09-23T14:25:48Z

CBMC Results (ML-DSA-65)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	123s	13s	+846%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	191s	63s	+203%
`sig_unpack_hints`	LP64	z3*	⚠️	26s	2s	+1200%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	24s	5s	+380%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	48s	6s	+700%
`sign_signature_internal`	LP64	z3_no_bv_extract*	⚠️	169s	55s	+207%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	367s	177s	+107%

Full Results (229 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	1888s	1784s	+5.8%
`caddq`	LP64	z3*	✅	2s	3s	-33%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	123s	13s	+846%
`decompose`	LP64	z3*	✅	2s	1s	+100%
`fqmul`	LP64	bitwuzla*	✅	23s	40s	-43%
`fqscale`	LP64	bitwuzla*	✅	3s	3s	+0%
`intt_native_aarch64`	LP64	z3*	✅	2s	3s	-33%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	4s	-	new
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	3s	-	new
	LP64	z3	✅	4s	-	new
`intt_native_x86_64`	LP64	z3*	✅	3s	3s	+0%
`keccak_absorb`	LP64	z3*	✅	4s	3s	+33%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	4s	8s	-50%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	1s	2s	-50%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	1s	3s	-67%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	1s	4s	-75%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	2s	2s	+0%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	2s	2s	+0%
`keccak_finalize`	LP64	z3*	✅	2s	2s	+0%
`keccak_init`	LP64	z3*	✅	2s	1s	+100%
`keccak_squeeze`	LP64	bitwuzla*	✅	2s	4s	-50%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	5s	5s	+0%
`keccakf1600_extract_bytes (big endian)`	LP64	z3*	✅	1s	2s	-50%
`keccakf1600_permute`	LP64	z3*	✅	1s	2s	-50%
`keccakf1600_permute_native`	LP64	z3*	✅	3s	3s	+0%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	1s	2s	-50%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	2s	4s	-50%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	2s	4s	-50%
`keccakf1600x4_permute`	LP64	z3*	✅	3s	4s	-25%
`keccakf1600x4_permute_native`	LP64	z3*	✅	14s	23s	-39%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	2s	1s	+100%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	3s	3s	+0%
`make_hint`	LP64	z3*	✅	3s	2s	+50%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	191s	63s	+203%
`mld_check_pct`	LP64	z3*	✅	4s	14s	-71%
`mld_compute_pack_z`	LP64	z3_no_bv_extract*	✅	4s	7s	-43%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	3s	2s	+50%
	ILP32	cvc5_arrays_exp	✅	3s	2s	+50%
	ILP32	z3	✅	2s	2s	+0%
	LP64	bitwuzla	✅	2s	2s	+0%
	LP64	cvc5_arrays_exp	✅	1s	2s	-50%
	LP64	z3*	✅	2s	2s	+0%
`mld_ct_cmask_neg_i32`	LP64	z3*	✅	1s	2s	-50%
`mld_ct_cmask_nonzero_u32`	LP64	z3*	✅	2s	4s	-50%
`mld_ct_cmask_nonzero_u8`	LP64	z3*	✅	1s	3s	-67%
`mld_ct_get_optblocker_i64`	LP64	z3*	✅	1s	2s	-50%
`mld_ct_get_optblocker_u32`	LP64	z3*	✅	2s	3s	-33%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	1s	2s	-50%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	2s	2s	+0%
`mld_ct_sel_int32`	LP64	z3*	✅	3s	3s	+0%
`mld_h`	LP64	z3*	✅	2s	2s	+0%
`mld_invntt_layer`	LP64	bitwuzla*	✅	57s	109s	-48%
`mld_keccakf1600_extract_bytes`	LP64	z3*	✅	3s	1s	+200%
`mld_keccakf1600_permute_c`	LP64	z3*	✅	3s	6s	-50%
`mld_keccakf1600x4_extract_bytes_c`	LP64	z3*	✅	2s	3s	-33%
`mld_keccakf1600x4_xor_bytes_c`	LP64	z3*	✅	4s	2s	+100%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	10s	24s	-58%
`mld_ntt_layer`	LP64	bitwuzla*	✅	19s	41s	-54%
`mld_polymat_expand_entry`	LP64	z3*	✅	3s	4s	-25%
`mld_prepare_domain_separation_prefix`	LP64	z3*	✅	3s	2s	+50%
`mld_sample_s1_s2`	LP64	z3*	✅	2s	6s	-67%
`mld_sample_s1_s2_serial`	LP64	z3*	✅	3s	4s	-25%
`mld_sign_attempt`	LP64	z3*	✅	2s	-	new
`mld_sign_finish`	LP64	z3*	✅	2s	-	new
`mld_sign_resume`	LP64	z3*	✅	1s	-	new
`mld_value_barrier_i64`	LP64	z3*	✅	2s	2s	+0%
`mld_value_barrier_u32`	LP64	z3*	✅	1s	3s	-67%
`mld_value_barrier_u8`	LP64	z3*	✅	3s	3s	+0%
`montgomery_reduce`	LP64	z3*	✅	1s	4s	-75%
`ntt_native_aarch64`	LP64	z3*	✅	2s	2s	+0%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	2s	-	new
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	3s	-	new
	LP64	z3	✅	1s	-	new
`ntt_native_x86_64`	LP64	z3*	✅	4s	2s	+100%
`nttunpack_native_x86_64`	LP64	z3*	✅	4s	3s	+33%
`pack_sig_c`	LP64	z3*	✅	2s	5s	-60%
`pack_sig_h`	LP64	z3_no_bv_extract*	✅	1s	5s	-80%
`pack_sig_z`	LP64	z3*	✅	2s	2s	+0%
`pack_sk_rho_key_tr_s2`	LP64	z3*	✅	3s	2s	+50%
`pack_sk_s1`	LP64	z3*	✅	3s	5s	-40%
`pointwise_acc_native_aarch64`	LP64	z3_smt_only*	✅	4s	6s	-33%
`pointwise_acc_native_x86_64`	LP64	z3_smt_only*	✅	4s	8s	-50%
`pointwise_native_aarch64`	LP64	z3*	✅	2s	5s	-60%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	1s	-	new
	LP64	z3	✅	3s	-	new
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	3s	-	new
`pointwise_native_x86_64`	LP64	z3*	✅	1s	3s	-67%
`poly_add`	LP64	z3*	✅	2s	9s	-78%
`poly_caddq`	LP64	z3*	✅	1s	2s	-50%
`poly_caddq_c`	LP64	z3*	✅	2s	2s	+0%
`poly_caddq_native`	LP64	z3*	✅	3s	2s	+50%
`poly_caddq_native_aarch64`	LP64	z3*	✅	4s	2s	+100%
`poly_caddq_native_x86_64`	LP64	z3*	✅	2s	3s	-33%
`poly_challenge`	LP64	z3*	✅	2s	6s	-67%
`poly_chknorm`	LP64	z3*	✅	4s	4s	+0%
`poly_chknorm_c`	LP64	z3*	✅	5s	15s	-67%
`poly_chknorm_native`	LP64	z3*	✅	3s	2s	+50%
`poly_chknorm_native_aarch64`	LP64	z3*	✅	2s	3s	-33%
`poly_chknorm_native_x86_64`	LP64	z3*	✅	3s	3s	+0%
`poly_decompose`	LP64	z3*	✅	1s	2s	-50%
`poly_decompose_32_native_aarch64`	LP64	z3*	✅	1s	3s	-67%
`poly_decompose_88_native_aarch64`	LP64	z3*	✅	3s	1s	+200%
`poly_decompose_c`	LP64	z3*	✅	1s	5s	-80%
`poly_decompose_native`	LP64	z3*	✅	2s	3s	-33%
`poly_decompose_native_x86_64`	LP64	z3*	✅	2s	3s	-33%
`poly_invntt_tomont`	LP64	z3*	✅	1s	3s	-67%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	6s	11s	-45%
`poly_invntt_tomont_native`	LP64	z3*	✅	1s	2s	-50%
`poly_ntt`	LP64	z3*	✅	3s	2s	+50%
`poly_ntt_c`	LP64	z3_smt_only*	✅	9s	19s	-53%
`poly_ntt_native`	LP64	z3*	✅	2s	4s	-50%
`poly_permute_bitrev_to_custom_optional`	LP64	z3*	✅	4s	2s	+100%
`poly_permute_bitrev_to_custom_optional_native`	LP64	z3*	✅	3s	4s	-25%
`poly_pointwise_montgomery`	LP64	z3*	✅	3s	3s	+0%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	41s	125s	-67%
`poly_pointwise_montgomery_native`	LP64	z3*	✅	2s	3s	-33%
`poly_power2round`	LP64	z3*	✅	4s	4s	+0%
`poly_reduce`	LP64	z3*	✅	1s	3s	-67%
`poly_shiftl`	LP64	z3*	✅	1s	3s	-67%
`poly_sub`	LP64	z3*	✅	2s	3s	-33%
`poly_uniform`	LP64	z3*	✅	4s	4s	+0%
`poly_uniform_4x`	LP64	z3*	✅	6s	13s	-54%
`poly_uniform_eta`	LP64	z3*	✅	3s	4s	-25%
`poly_uniform_eta_4x`	LP64	z3*	✅	7s	14s	-50%
`poly_uniform_gamma1`	LP64	z3*	✅	2s	3s	-33%
`poly_uniform_gamma1_4x`	LP64	z3*	✅	1s	4s	-75%
`poly_use_hint`	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint_c`	LP64	z3*	✅	3s	5s	-40%
`poly_use_hint_native`	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint_native_aarch64`	LP64	z3*	✅	2s	3s	-33%
`poly_use_hint_native_x86_64`	LP64	z3*	✅	4s	-	new
`polyeta_pack`	LP64	z3*	✅	4s	3s	+33%
`polyeta_unpack`	LP64	z3*	✅	4s	8s	-50%
`polyt0_pack`	LP64	z3*	✅	2s	3s	-33%
`polyt0_unpack`	LP64	z3*	✅	7s	16s	-56%
`polyt1_pack`	LP64	z3*	✅	2s	3s	-33%
`polyt1_unpack`	LP64	z3*	✅	1s	5s	-80%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	66s	110s	-40%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	12s	27s	-56%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	3s	1s	+200%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	14s	18s	-22%
`polyveck_caddq`	LP64	z3*	✅	4s	6s	-33%
`polyveck_chknorm`	LP64	z3*	✅	2s	6s	-67%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	4s	-	new
`polyveck_invntt_tomont`	LP64	z3*	✅	3s	8s	-62%
`polyveck_ntt`	LP64	z3*	✅	4s	7s	-43%
`polyveck_pack_eta`	LP64	z3*	✅	3s	4s	-25%
`polyveck_reduce`	LP64	z3*	✅	1s	4s	-75%
`polyveck_unpack_eta`	LP64	z3*	✅	3s	6s	-50%
`polyvecl_chknorm`	LP64	z3*	✅	3s	7s	-57%
`polyvecl_ntt`	LP64	z3*	✅	3s	4s	-25%
`polyvecl_pack_eta`	LP64	z3*	✅	3s	3s	+0%
`polyvecl_pointwise_acc_montgomery`	LP64	z3_smt_only*	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	✅	163s	210s	-22%
`polyvecl_pointwise_acc_montgomery_native`	LP64	z3_smt_only*	✅	2s	2s	+0%
`polyvecl_uniform_gamma1`	LP64	z3*	✅	4s	2s	+100%
`polyvecl_uniform_gamma1_serial`	LP64	z3*	✅	4s	3s	+33%
`polyvecl_unpack_eta`	LP64	z3*	✅	1s	3s	-67%
`polyvecl_unpack_z`	LP64	z3*	✅	2s	3s	-33%
`polyw1_pack`	LP64	z3*	✅	3s	4s	-25%
`polyw1_pack_32`	LP64	z3*	✅	3s	4s	-25%
`polyw1_pack_88`	LP64	z3*	✅	3s	2s	+50%
`polyw1_unpack`	LP64	z3*	✅	2s	-	new
`polyw1_unpack_32`	LP64	z3*	✅	2s	-	new
`polyw1_unpack_88`	LP64	z3*	✅	3s	-	new
`polyz_pack`	LP64	z3*	✅	3s	3s	+0%
`polyz_unpack`	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_17_native_aarch64`	LP64	z3*	✅	3s	3s	+0%
`polyz_unpack_19_native_aarch64`	LP64	z3*	✅	2s	3s	-33%
`polyz_unpack_c`	LP64	z3*	✅	4s	13s	-69%
`polyz_unpack_native`	LP64	z3*	✅	1s	4s	-75%
`polyz_unpack_native_x86_64`	LP64	z3*	✅	3s	3s	+0%
`power2round`	LP64	z3*	✅	2s	1s	+100%
`reduce32`	LP64	z3*	✅	2s	3s	-33%
`rej_eta`	LP64	bitwuzla*	✅	2s	2s	+0%
`rej_eta_c`	LP64	bitwuzla*	✅	3s	5s	-40%
`rej_eta_native`	LP64	bitwuzla*	✅	3s	3s	+0%
`rej_uniform`	LP64	z3*	✅	9s	18s	-50%
`rej_uniform_c`	LP64	z3*	✅	9s	14s	-36%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	2s	4s	-50%
`rej_uniform_eta_native_x86_64`	LP64	z3_smt_only*	✅	1s	-	new
`rej_uniform_native`	LP64	bitwuzla*	✅	3s	4s	-25%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	3s	3s	+0%
`rej_uniform_native_x86_64`	LP64	z3_smt_only*	✅	9s	-	new
`shake128_absorb`	LP64	z3*	✅	2s	2s	+0%
`shake128_finalize`	LP64	z3*	✅	2s	1s	+100%
`shake128_init`	LP64	z3*	✅	2s	2s	+0%
`shake128_release`	LP64	z3*	✅	2s	3s	-33%
`shake128_squeeze`	LP64	bitwuzla*	✅	1s	2s	-50%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	1s	3s	-67%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	1s	3s	-67%
`shake256`	LP64	z3*	✅	2s	2s	+0%
`shake256_absorb`	LP64	z3*	✅	2s	2s	+0%
`shake256_finalize`	LP64	z3*	✅	3s	1s	+200%
`shake256_init`	LP64	z3*	✅	1s	2s	-50%
`shake256_release`	LP64	z3*	✅	4s	2s	+100%
`shake256_squeeze`	LP64	bitwuzla*	✅	2s	3s	-33%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	3s	3s	+0%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	2s	+0%
`sig_unpack_hints`	LP64	z3*	⚠️	26s	2s	+1200%
`sign_keypair`	LP64	z3*	✅	5s	3s	+67%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	24s	5s	+380%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	48s	6s	+700%
`sign_signature`	LP64	z3*	✅	2s	6s	-67%
`sign_signature_extmu`	LP64	z3*	✅	2s	2s	+0%
`sign_signature_internal`	LP64	z3_no_bv_extract*	⚠️	169s	55s	+207%
`sign_signature_pre_hash_internal`	LP64	z3*	✅	6s	3s	+100%
`sign_signature_pre_hash_shake256`	LP64	z3*	✅	3s	3s	+0%
`sign_verify`	LP64	z3*	✅	1s	3s	-67%
`sign_verify_extmu`	LP64	z3*	✅	2s	3s	-33%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	367s	177s	+107%
`sign_verify_pre_hash_internal`	LP64	z3*	✅	4s	5s	-20%
`sign_verify_pre_hash_shake256`	LP64	z3*	✅	2s	5s	-60%
`sk_s1hat_get_poly`	LP64	z3*	✅	1s	6s	-83%
`sk_s2hat_get_poly`	LP64	z3*	✅	2s	2s	+0%
`sk_t0hat_get_poly`	LP64	z3*	✅	1s	2s	-50%
`sys_check_capability`	LP64	z3*	✅	3s	4s	-25%
`unpack_pk_t1`	LP64	z3*	✅	3s	5s	-40%
`unpack_sk`	LP64	z3*	✅	4s	3s	+33%
`unpack_sk_s1hat`	LP64	z3*	✅	1s	2s	-50%
`unpack_sk_s2hat`	LP64	z3*	✅	2s	4s	-50%
`unpack_sk_t0hat`	LP64	z3*	✅	2s	5s	-60%
`use_hint`	LP64	z3*	✅	1s	2s	-50%
`yvec_get_poly`	LP64	z3*	✅	1s	3s	-67%
`yvec_init`	LP64	z3*	✅	1s	3s	-67%

oqs-bot · 2026-09-23T14:28:38Z

CBMC Results (ML-DSA-87)

* default.

⚠️ Attention Required

Proof	DM	Solver	Status	Current	Previous	Change
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	186s	19s	+879%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	334s	55s	+507%
`sig_unpack_hints`	LP64	z3*	⚠️	25s	3s	+733%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	41s	6s	+583%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	50s	6s	+733%
`sign_signature_internal`	LP64	z3_no_bv_extract*	⚠️	349s	42s	+731%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	589s	97s	+507%

Full Results (229 configurations)

Proof	DM	Solver	Status	Current	Previous	Change
`TOTAL`	-	-	✅	2597s	2151s	+20.7%
`caddq`	LP64	z3*	✅	2s	4s	-50%
`compute_pack_t0_t1`	LP64	z3_no_bv_extract*	⚠️	186s	19s	+879%
`decompose`	LP64	z3*	✅	2s	3s	-33%
`fqmul`	LP64	bitwuzla*	✅	22s	43s	-49%
`fqscale`	LP64	bitwuzla*	✅	2s	3s	-33%
`intt_native_aarch64`	LP64	z3*	✅	5s	3s	+67%
`intt_native_rv32im_fastmul`	ILP32	z3*	✅	3s	-	new
	LP64	z3	✅	1s	-	new
`intt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	3s	-	new
`intt_native_x86_64`	LP64	z3*	✅	3s	3s	+0%
`keccak_absorb`	LP64	z3*	✅	2s	3s	-33%
`keccak_absorb_once_x4`	LP64	bitwuzla*	✅	3s	9s	-67%
`keccak_f1600_x1_native_aarch64`	LP64	bitwuzla*	✅	1s	1s	+0%
`keccak_f1600_x1_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	1s	+100%
`keccak_f1600_x4_native_aarch64_v84a`	LP64	bitwuzla*	✅	2s	4s	-50%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	LP64	bitwuzla*	✅	1s	3s	-67%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	LP64	bitwuzla*	✅	1s	4s	-75%
`keccak_f1600_x4_native_avx2`	LP64	bitwuzla*	✅	2s	2s	+0%
`keccak_finalize`	LP64	z3*	✅	1s	1s	+0%
`keccak_init`	LP64	z3*	✅	2s	3s	-33%
`keccak_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
`keccak_squeezeblocks_x4`	LP64	bitwuzla*	✅	2s	4s	-50%
`keccakf1600_extract_bytes (big endian)`	LP64	z3*	✅	1s	3s	-67%
`keccakf1600_permute`	LP64	z3*	✅	3s	3s	+0%
`keccakf1600_permute_native`	LP64	z3*	✅	1s	4s	-75%
`keccakf1600_xor_bytes`	LP64	bitwuzla*	✅	3s	3s	+0%
`keccakf1600_xor_bytes (big endian)`	LP64	bitwuzla*	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes`	LP64	bitwuzla*	✅	3s	2s	+50%
`keccakf1600x4_extract_bytes_native`	LP64	bitwuzla*	✅	1s	2s	-50%
`keccakf1600x4_permute`	LP64	z3*	✅	2s	3s	-33%
`keccakf1600x4_permute_native`	LP64	z3*	✅	11s	23s	-52%
`keccakf1600x4_xor_bytes`	LP64	bitwuzla*	✅	1s	3s	-67%
`keccakf1600x4_xor_bytes_native`	LP64	bitwuzla*	✅	1s	3s	-67%
`make_hint`	LP64	z3*	✅	1s	3s	-67%
`mld_attempt_signature_generation`	LP64	z3_no_bv_extract*	⚠️	334s	55s	+507%
`mld_check_pct`	LP64	z3*	✅	5s	16s	-69%
`mld_compute_pack_z`	LP64	z3_no_bv_extract*	✅	6s	8s	-25%
`mld_ct_abs_i32`	ILP32	bitwuzla	✅	1s	3s	-67%
	ILP32	cvc5_arrays_exp	✅	2s	3s	-33%
	ILP32	z3	✅	1s	3s	-67%
	LP64	bitwuzla	✅	1s	3s	-67%
	LP64	cvc5_arrays_exp	✅	2s	3s	-33%
	LP64	z3*	✅	2s	3s	-33%
`mld_ct_cmask_neg_i32`	LP64	z3*	✅	2s	4s	-50%
`mld_ct_cmask_nonzero_u32`	LP64	z3*	✅	2s	2s	+0%
`mld_ct_cmask_nonzero_u8`	LP64	z3*	✅	3s	3s	+0%
`mld_ct_get_optblocker_i64`	LP64	z3*	✅	2s	3s	-33%
`mld_ct_get_optblocker_u32`	LP64	z3*	✅	1s	2s	-50%
`mld_ct_get_optblocker_u8`	LP64	bitwuzla*	✅	3s	3s	+0%
`mld_ct_memcmp`	LP64	bitwuzla*	✅	2s	3s	-33%
`mld_ct_sel_int32`	LP64	z3*	✅	2s	3s	-33%
`mld_h`	LP64	z3*	✅	4s	3s	+33%
`mld_invntt_layer`	LP64	bitwuzla*	✅	55s	115s	-52%
`mld_keccakf1600_extract_bytes`	LP64	z3*	✅	3s	4s	-25%
`mld_keccakf1600_permute_c`	LP64	z3*	✅	4s	7s	-43%
`mld_keccakf1600x4_extract_bytes_c`	LP64	z3*	✅	2s	2s	+0%
`mld_keccakf1600x4_xor_bytes_c`	LP64	z3*	✅	2s	4s	-50%
`mld_ntt_butterfly_block`	LP64	bitwuzla*	✅	11s	24s	-54%
`mld_ntt_layer`	LP64	bitwuzla*	✅	21s	45s	-53%
`mld_polymat_expand_entry`	LP64	z3*	✅	2s	3s	-33%
`mld_prepare_domain_separation_prefix`	LP64	z3*	✅	1s	4s	-75%
`mld_sample_s1_s2`	LP64	z3*	✅	2s	6s	-67%
`mld_sample_s1_s2_serial`	LP64	z3*	✅	5s	8s	-38%
`mld_sign_attempt`	LP64	z3*	✅	1s	-	new
`mld_sign_finish`	LP64	z3*	✅	3s	-	new
`mld_sign_resume`	LP64	z3*	✅	3s	-	new
`mld_value_barrier_i64`	LP64	z3*	✅	1s	1s	+0%
`mld_value_barrier_u32`	LP64	z3*	✅	2s	2s	+0%
`mld_value_barrier_u8`	LP64	z3*	✅	2s	3s	-33%
`montgomery_reduce`	LP64	z3*	✅	1s	3s	-67%
`ntt_native_aarch64`	LP64	z3*	✅	2s	6s	-67%
`ntt_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	3s	-	new
`ntt_native_rv32im_slowmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	3s	-	new
`ntt_native_x86_64`	LP64	z3*	✅	2s	2s	+0%
`nttunpack_native_x86_64`	LP64	z3*	✅	2s	3s	-33%
`pack_sig_c`	LP64	z3*	✅	3s	4s	-25%
`pack_sig_h`	LP64	z3_no_bv_extract*	✅	1s	4s	-75%
`pack_sig_z`	LP64	z3*	✅	3s	5s	-40%
`pack_sk_rho_key_tr_s2`	LP64	z3*	✅	3s	3s	+0%
`pack_sk_s1`	LP64	z3*	✅	3s	1s	+200%
`pointwise_acc_native_aarch64`	LP64	z3_smt_only*	✅	2s	6s	-67%
`pointwise_acc_native_x86_64`	LP64	z3_smt_only*	✅	3s	6s	-50%
`pointwise_native_aarch64`	LP64	z3*	✅	3s	5s	-40%
`pointwise_native_rv32im_fastmul`	ILP32	z3*	✅	2s	-	new
	LP64	z3	✅	1s	-	new
`pointwise_native_rv32im_slowmul`	ILP32	z3*	✅	1s	-	new
	LP64	z3	✅	2s	-	new
`pointwise_native_x86_64`	LP64	z3*	✅	3s	2s	+50%
`poly_add`	LP64	z3*	✅	2s	6s	-67%
`poly_caddq`	LP64	z3*	✅	3s	2s	+50%
`poly_caddq_c`	LP64	z3*	✅	1s	3s	-67%
`poly_caddq_native`	LP64	z3*	✅	3s	4s	-25%
`poly_caddq_native_aarch64`	LP64	z3*	✅	2s	3s	-33%
`poly_caddq_native_x86_64`	LP64	z3*	✅	2s	2s	+0%
`poly_challenge`	LP64	z3*	✅	3s	5s	-40%
`poly_chknorm`	LP64	z3*	✅	3s	3s	+0%
`poly_chknorm_c`	LP64	z3*	✅	6s	15s	-60%
`poly_chknorm_native`	LP64	z3*	✅	2s	4s	-50%
`poly_chknorm_native_aarch64`	LP64	z3*	✅	2s	4s	-50%
`poly_chknorm_native_x86_64`	LP64	z3*	✅	2s	2s	+0%
`poly_decompose`	LP64	z3*	✅	3s	3s	+0%
`poly_decompose_32_native_aarch64`	LP64	z3*	✅	1s	5s	-80%
`poly_decompose_88_native_aarch64`	LP64	z3*	✅	1s	2s	-50%
`poly_decompose_c`	LP64	z3*	✅	3s	5s	-40%
`poly_decompose_native`	LP64	z3*	✅	1s	2s	-50%
`poly_decompose_native_x86_64`	LP64	z3*	✅	2s	2s	+0%
`poly_invntt_tomont`	LP64	z3*	✅	2s	1s	+100%
`poly_invntt_tomont_c`	LP64	z3_smt_only*	✅	4s	12s	-67%
`poly_invntt_tomont_native`	LP64	z3*	✅	2s	5s	-60%
`poly_ntt`	LP64	z3*	✅	1s	3s	-67%
`poly_ntt_c`	LP64	z3_smt_only*	✅	11s	21s	-48%
`poly_ntt_native`	LP64	z3*	✅	2s	3s	-33%
`poly_permute_bitrev_to_custom_optional`	LP64	z3*	✅	1s	3s	-67%
`poly_permute_bitrev_to_custom_optional_native`	LP64	z3*	✅	3s	5s	-40%
`poly_pointwise_montgomery`	LP64	z3*	✅	2s	4s	-50%
`poly_pointwise_montgomery_c`	LP64	z3*	✅	43s	144s	-70%
`poly_pointwise_montgomery_native`	LP64	z3*	✅	1s	5s	-80%
`poly_power2round`	LP64	z3*	✅	3s	3s	+0%
`poly_reduce`	LP64	z3*	✅	3s	2s	+50%
`poly_shiftl`	LP64	z3*	✅	2s	4s	-50%
`poly_sub`	LP64	z3*	✅	2s	3s	-33%
`poly_uniform`	LP64	z3*	✅	2s	4s	-50%
`poly_uniform_4x`	LP64	z3*	✅	7s	13s	-46%
`poly_uniform_eta`	LP64	z3*	✅	1s	4s	-75%
`poly_uniform_eta_4x`	LP64	z3*	✅	8s	11s	-27%
`poly_uniform_gamma1`	LP64	z3*	✅	3s	4s	-25%
`poly_uniform_gamma1_4x`	LP64	z3*	✅	1s	3s	-67%
`poly_use_hint`	LP64	z3*	✅	2s	1s	+100%
`poly_use_hint_c`	LP64	z3*	✅	3s	2s	+50%
`poly_use_hint_native`	LP64	z3*	✅	3s	3s	+0%
`poly_use_hint_native_aarch64`	LP64	z3*	✅	2s	2s	+0%
`poly_use_hint_native_x86_64`	LP64	z3*	✅	2s	-	new
`polyeta_pack`	LP64	z3*	✅	2s	4s	-50%
`polyeta_unpack`	LP64	z3*	✅	4s	17s	-76%
`polyt0_pack`	LP64	z3*	✅	4s	4s	+0%
`polyt0_unpack`	LP64	z3*	✅	9s	14s	-36%
`polyt1_pack`	LP64	z3*	✅	2s	3s	-33%
`polyt1_unpack`	LP64	z3*	✅	2s	4s	-50%
`polyvec_matrix_expand`	LP64	z3_no_bv_extract*	✅	100s	324s	-69%
`polyvec_matrix_expand_serial`	LP64	z3*	✅	16s	38s	-58%
`polyvec_matrix_pointwise_montgomery_row`	LP64	z3_no_bv_extract*	✅	1s	3s	-67%
`polyvec_matrix_pointwise_montgomery_yvec`	LP64	z3*	✅	9s	18s	-50%
`polyveck_caddq`	LP64	z3*	✅	5s	8s	-38%
`polyveck_chknorm`	LP64	z3*	✅	2s	3s	-33%
`polyveck_decompose_pack_w1`	LP64	z3*	✅	8s	-	new
`polyveck_invntt_tomont`	LP64	z3*	✅	6s	9s	-33%
`polyveck_ntt`	LP64	z3*	✅	2s	11s	-82%
`polyveck_pack_eta`	LP64	z3*	✅	1s	6s	-83%
`polyveck_reduce`	LP64	z3*	✅	2s	3s	-33%
`polyveck_unpack_eta`	LP64	z3*	✅	2s	4s	-50%
`polyvecl_chknorm`	LP64	z3*	✅	2s	7s	-71%
`polyvecl_ntt`	LP64	z3*	✅	3s	7s	-57%
`polyvecl_pack_eta`	LP64	z3*	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery`	LP64	z3_smt_only*	✅	2s	5s	-60%
`polyvecl_pointwise_acc_montgomery_c`	LP64	z3*	✅	216s	353s	-39%
`polyvecl_pointwise_acc_montgomery_native`	LP64	z3_smt_only*	✅	2s	3s	-33%
`polyvecl_uniform_gamma1`	LP64	z3*	✅	3s	2s	+50%
`polyvecl_uniform_gamma1_serial`	LP64	z3*	✅	2s	4s	-50%
`polyvecl_unpack_eta`	LP64	z3*	✅	4s	5s	-20%
`polyvecl_unpack_z`	LP64	z3*	✅	3s	4s	-25%
`polyw1_pack`	LP64	z3*	✅	2s	4s	-50%
`polyw1_pack_32`	LP64	z3*	✅	1s	4s	-75%
`polyw1_pack_88`	LP64	z3*	✅	1s	3s	-67%
`polyw1_unpack`	LP64	z3*	✅	3s	-	new
`polyw1_unpack_32`	LP64	z3*	✅	1s	-	new
`polyw1_unpack_88`	LP64	z3*	✅	1s	-	new
`polyz_pack`	LP64	z3*	✅	1s	5s	-80%
`polyz_unpack`	LP64	z3*	✅	1s	2s	-50%
`polyz_unpack_17_native_aarch64`	LP64	z3*	✅	1s	3s	-67%
`polyz_unpack_19_native_aarch64`	LP64	z3*	✅	3s	4s	-25%
`polyz_unpack_c`	LP64	z3*	✅	4s	3s	+33%
`polyz_unpack_native`	LP64	z3*	✅	3s	4s	-25%
`polyz_unpack_native_x86_64`	LP64	z3*	✅	2s	3s	-33%
`power2round`	LP64	z3*	✅	2s	4s	-50%
`reduce32`	LP64	z3*	✅	2s	3s	-33%
`rej_eta`	LP64	bitwuzla*	✅	1s	4s	-75%
`rej_eta_c`	LP64	bitwuzla*	✅	3s	5s	-40%
`rej_eta_native`	LP64	bitwuzla*	✅	3s	6s	-50%
`rej_uniform`	LP64	z3*	✅	11s	15s	-27%
`rej_uniform_c`	LP64	z3*	✅	10s	19s	-47%
`rej_uniform_eta_native_aarch64`	LP64	bitwuzla*	✅	3s	5s	-40%
`rej_uniform_eta_native_x86_64`	LP64	z3_smt_only*	✅	1s	-	new
`rej_uniform_native`	LP64	bitwuzla*	✅	2s	8s	-75%
`rej_uniform_native_aarch64`	LP64	bitwuzla*	✅	2s	2s	+0%
`rej_uniform_native_x86_64`	LP64	z3_smt_only*	✅	9s	-	new
`shake128_absorb`	LP64	z3*	✅	1s	4s	-75%
`shake128_finalize`	LP64	z3*	✅	3s	2s	+50%
`shake128_init`	LP64	z3*	✅	2s	1s	+100%
`shake128_release`	LP64	z3*	✅	1s	4s	-75%
`shake128_squeeze`	LP64	bitwuzla*	✅	1s	2s	-50%
`shake128x4_absorb_once`	LP64	bitwuzla*	✅	1s	5s	-80%
`shake128x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	3s	-33%
`shake256`	LP64	z3*	✅	3s	2s	+50%
`shake256_absorb`	LP64	z3*	✅	3s	2s	+50%
`shake256_finalize`	LP64	z3*	✅	2s	2s	+0%
`shake256_init`	LP64	z3*	✅	3s	2s	+50%
`shake256_release`	LP64	z3*	✅	1s	3s	-67%
`shake256_squeeze`	LP64	bitwuzla*	✅	2s	2s	+0%
`shake256x4_absorb_once`	LP64	bitwuzla*	✅	2s	2s	+0%
`shake256x4_squeezeblocks`	LP64	bitwuzla*	✅	2s	1s	+100%
`sig_unpack_hints`	LP64	z3*	⚠️	25s	3s	+733%
`sign_keypair`	LP64	z3*	✅	5s	4s	+25%
`sign_keypair_internal`	LP64	z3_no_bv_extract*	⚠️	41s	6s	+583%
`sign_pk_from_sk`	LP64	z3_no_bv_extract*	⚠️	50s	6s	+733%
`sign_signature`	LP64	z3*	✅	6s	5s	+20%
`sign_signature_extmu`	LP64	z3*	✅	1s	4s	-75%
`sign_signature_internal`	LP64	z3_no_bv_extract*	⚠️	349s	42s	+731%
`sign_signature_pre_hash_internal`	LP64	z3*	✅	2s	5s	-60%
`sign_signature_pre_hash_shake256`	LP64	z3*	✅	3s	6s	-50%
`sign_verify`	LP64	z3*	✅	4s	5s	-20%
`sign_verify_extmu`	LP64	z3*	✅	2s	3s	-33%
`sign_verify_internal`	LP64	z3_no_bv_extract*	⚠️	589s	97s	+507%
`sign_verify_pre_hash_internal`	LP64	z3*	✅	3s	3s	+0%
`sign_verify_pre_hash_shake256`	LP64	z3*	✅	5s	3s	+67%
`sk_s1hat_get_poly`	LP64	z3*	✅	1s	3s	-67%
`sk_s2hat_get_poly`	LP64	z3*	✅	1s	3s	-67%
`sk_t0hat_get_poly`	LP64	z3*	✅	4s	4s	+0%
`sys_check_capability`	LP64	z3*	✅	2s	3s	-33%
`unpack_pk_t1`	LP64	z3*	✅	1s	1s	+0%
`unpack_sk`	LP64	z3*	✅	4s	5s	-20%
`unpack_sk_s1hat`	LP64	z3*	✅	2s	2s	+0%
`unpack_sk_s2hat`	LP64	z3*	✅	3s	3s	+0%
`unpack_sk_t0hat`	LP64	z3*	✅	5s	7s	-29%
`use_hint`	LP64	z3*	✅	4s	3s	+33%
`yvec_get_poly`	LP64	z3*	✅	3s	4s	-25%
`yvec_init`	LP64	z3*	✅	2s	4s	-50%

mkannwischer

Thanks this looks good.

nixpkgs-unstable now ships a HOL Light recent enough for the RV32 proofs, so drop the custom override and use it directly. Take the OCaml toolchain from nixpkgs-unstable as well so it matches the one HOL Light was built with. Co-authored-by: Hanno Becker <beckphan@amazon.co.uk> Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

mkannwischer · 2026-10-06T10:35:18Z

I took the liberty to rebase this PR on top of the merged RV32 proof and remove the overly verbose comment.

hanno-becker mentioned this pull request Sep 23, 2026

HOL-Light/RV32-IM: Add correctness, safety and constant-time proof for arithmetic backend #1426

Merged

mkannwischer approved these changes Sep 23, 2026

View reviewed changes

Comment thread flake.nix Outdated

mkannwischer force-pushed the rv32-proof-followup branch from 3ece3a1 to 40bffea Compare October 6, 2026 10:34

mkannwischer marked this pull request as ready for review October 6, 2026 10:46

mkannwischer requested a review from a team as a code owner October 6, 2026 10:46

mkannwischer enabled auto-merge October 6, 2026 10:46

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

Merged via the queue into main with commit d086e67 Oct 6, 2026
450 checks passed

mkannwischer deleted the rv32-proof-followup branch October 6, 2026 15:55

Navigation Menu

Repository navigation

nix: Take HOL Light from nixpkgs-unstable instead of pinning it - #1433

nix: Take HOL Light from nixpkgs-unstable instead of pinning it#1433
mkannwischer merged 1 commit into
mainfrom
rv32-proof-followup

hanno-becker commented Sep 23, 2026

Uh oh!

oqs-bot commented Sep 23, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Sep 23, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Sep 23, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Sep 23, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Sep 23, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Sep 23, 2026 •

edited

Loading

Uh oh!

mkannwischer left a comment

Uh oh!

Uh oh!

mkannwischer commented Oct 6, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

hanno-becker commented Sep 23, 2026

Uh oh!

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

Uh oh!

CBMC Results (ML-DSA-44, REDUCE-RAM)

Uh oh!

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

Uh oh!

CBMC Results (ML-DSA-65, REDUCE-RAM)

Uh oh!

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

Uh oh!

CBMC Results (ML-DSA-87, REDUCE-RAM)

Uh oh!

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

Uh oh!

CBMC Results (ML-DSA-44)

Uh oh!

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

Uh oh!

CBMC Results (ML-DSA-65)

Uh oh!

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

Uh oh!

CBMC Results (ML-DSA-87)

Uh oh!

mkannwischer left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

mkannwischer commented Oct 6, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

oqs-bot commented Sep 23, 2026 •

edited

Loading

oqs-bot commented Sep 23, 2026 •

edited

Loading

oqs-bot commented Sep 23, 2026 •

edited

Loading

oqs-bot commented Sep 23, 2026 •

edited

Loading

oqs-bot commented Sep 23, 2026 •

edited

Loading

oqs-bot commented Sep 23, 2026 •

edited

Loading