Make poly_pointwise_montgomery destructive by mkannwischer · Pull Request #1067 · pq-code-package/mldsa-native

mkannwischer · 2026-04-28T12:57:02Z

Rework mld_poly_pointwise_montgomery from (c, a, b) to in-place (a, b) where a := a * b * R^{-1} mod q. The change propagates through the C wrapper, the native dispatcher, the Arm aarch64 and x86_64 AVX2 assembly, all call sites, the test harness, and the allocation constants.

This allows eliminating one temporary polynomial in the the REDUCE_RAM definition in polymat, and it will also enable further memory optimizations in follow-up PRs.

CBMC and HOL Light proofs are not yet updated.

Depends on CBMC: Add contracts and proofs for yvec init/get_poly #1066

oqs-bot · 2026-04-28T13:15:54Z

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

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`poly_pointwise_montgomery_c`	⚠️	171s	110s	+55%

Full Results (197 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	1520s	1591s	-4.5%
`poly_pointwise_montgomery_c`	⚠️	171s	110s	+55%
`rej_uniform_native`	✅	108s	105s	+3%
`mld_invntt_layer`	✅	106s	105s	+1%
`sign_verify_internal`	✅	77s	119s	-35%
`mld_ct_memcmp`	✅	73s	72s	+1%
`polyvec_matrix_pointwise_montgomery_yvec`	✅	61s	91s	-33%
`mld_ntt_layer`	✅	42s	41s	+2%
`fqmul`	✅	30s	28s	+7%
`mld_attempt_signature_generation`	✅	24s	30s	-20%
`keccakf1600x4_permute_native`	✅	20s	23s	-13%
`rej_uniform`	✅	19s	8s	+138%
`mld_ntt_butterfly_block`	✅	18s	14s	+29%
`polyeta_unpack`	✅	18s	17s	+6%
`rej_uniform_c`	✅	18s	7s	+157%
`sign_keypair_internal`	✅	15s	16s	-6%
`poly_chknorm_c`	✅	14s	16s	-12%
`poly_uniform_eta_4x`	✅	12s	12s	+0%
`polyt0_unpack`	✅	12s	15s	-20%
`sign_pk_from_sk`	✅	12s	11s	+9%
`poly_add`	✅	10s	11s	-9%
`mld_check_pct`	✅	9s	9s	+0%
`poly_decompose_c`	✅	9s	8s	+12%
`polyz_unpack_c`	✅	9s	10s	-10%
`keccak_absorb`	✅	8s	7s	+14%
`keccak_absorb_once_x4`	✅	8s	10s	-20%
`keccakf1600_permute`	✅	8s	7s	+14%
`polyveck_pointwise_poly_montgomery`	✅	8s	5s	+60%
`sign`	✅	8s	5s	+60%
`poly_caddq_c`	✅	7s	7s	+0%
`poly_challenge`	✅	7s	5s	+40%
`poly_invntt_tomont_c`	✅	7s	8s	-12%
`poly_shiftl`	✅	7s	6s	+17%
`poly_use_hint_c`	✅	7s	3s	+133%
`polyveck_chknorm`	✅	7s	13s	-46%
`polyveck_power2round`	✅	7s	5s	+40%
`polyvecl_ntt`	✅	7s	6s	+17%
`sign_verify_extmu`	✅	7s	3s	+133%
`make_hint`	✅	6s	1s	+500%
`mld_compute_pack_z`	✅	6s	7s	-14%
`poly_power2round`	✅	6s	4s	+50%
`polyt1_unpack`	✅	6s	4s	+50%
`polyvec_matrix_expand`	✅	6s	3s	+100%
`polyveck_decompose`	✅	6s	12s	-50%
`polyveck_use_hint`	✅	6s	5s	+20%
`polyz_unpack_native`	✅	6s	1s	+500%
`rej_eta_c`	✅	6s	5s	+20%
`rej_eta_native`	✅	6s	4s	+50%
`sign_signature`	✅	6s	4s	+50%
`keccak_squeezeblocks_x4`	✅	5s	5s	+0%
`keccakf1600_permute_native`	✅	5s	6s	-17%
`mld_prepare_domain_separation_prefix`	✅	5s	2s	+150%
`mld_value_barrier_u32`	✅	5s	3s	+67%
`nttunpack_native_x86_64`	✅	5s	3s	+67%
`pointwise_acc_native_x86_64`	✅	5s	7s	-29%
`poly_caddq_native_aarch64`	✅	5s	3s	+67%
`poly_uniform_eta`	✅	5s	2s	+150%
`polyt0_pack`	✅	5s	2s	+150%
`polyveck_caddq`	✅	5s	3s	+67%
`polyveck_invntt_tomont`	✅	5s	5s	+0%
`polyveck_pack_eta`	✅	5s	2s	+150%
`polyveck_reduce`	✅	5s	4s	+25%
`polyveck_sub`	✅	5s	3s	+67%
`polyvecl_chknorm`	✅	5s	7s	-29%
`polyz_pack`	✅	5s	3s	+67%
`shake128_squeeze`	✅	5s	3s	+67%
`shake256`	✅	5s	2s	+150%
`sign_signature_extmu`	✅	5s	6s	-17%
`sign_verify`	✅	5s	7s	-29%
`sign_verify_pre_hash_shake256`	✅	5s	5s	+0%
`caddq`	✅	4s	4s	+0%
`fqscale`	✅	4s	1s	+300%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	4s	2s	+100%
`keccakf1600_xor_bytes`	✅	4s	3s	+33%
`mld_ct_cmask_neg_i32`	✅	4s	1s	+300%
`mld_ct_get_optblocker_i64`	✅	4s	2s	+100%
`mld_ct_get_optblocker_u8`	✅	4s	2s	+100%
`mld_polymat_expand_entry`	✅	4s	1s	+300%
`mld_sample_s1_s2_serial`	✅	4s	2s	+100%
`montgomery_reduce`	✅	4s	2s	+100%
`pack_pk`	✅	4s	2s	+100%
`pack_sig_c`	✅	4s	2s	+100%
`pointwise_native_x86_64`	✅	4s	4s	+0%
`poly_caddq_native`	✅	4s	3s	+33%
`poly_chknorm`	✅	4s	5s	-20%
`poly_chknorm_native_aarch64`	✅	4s	2s	+100%
`poly_decompose`	✅	4s	4s	+0%
`poly_ntt_c`	✅	4s	3s	+33%
`poly_ntt_native`	✅	4s	4s	+0%
`poly_permute_bitrev_to_custom_optional_native`	✅	4s	4s	+0%
`poly_uniform`	✅	4s	4s	+0%
`polyvec_matrix_expand_serial`	✅	4s	4s	+0%
`polyvec_matrix_pointwise_montgomery_row`	✅	4s	106s	-96%
`polyveck_add`	✅	4s	7s	-43%
`polyveck_ntt`	✅	4s	5s	-20%
`polyveck_shiftl`	✅	4s	2s	+100%
`polyveck_unpack_eta`	✅	4s	2s	+100%
`polyvecl_uniform_gamma1`	✅	4s	2s	+100%
`polyvecl_unpack_eta`	✅	4s	3s	+33%
`shake256_finalize`	✅	4s	3s	+33%
`sign_open`	✅	4s	5s	-20%
`sign_signature_pre_hash_internal`	✅	4s	4s	+0%
`unpack_sig`	✅	4s	2s	+100%
`decompose`	✅	3s	4s	-25%
`intt_native_x86_64`	✅	3s	3s	+0%
`keccak_squeeze`	✅	3s	2s	+50%
`keccakf1600x4_extract_bytes`	✅	3s	3s	+0%
`keccakf1600x4_permute`	✅	3s	3s	+0%
`keccakf1600x4_xor_bytes`	✅	3s	4s	-25%
`mld_ct_cmask_nonzero_u8`	✅	3s	1s	+200%
`mld_ct_get_optblocker_u32`	✅	3s	6s	-50%
`mld_h`	✅	3s	4s	-25%
`mld_sample_s1_s2`	✅	3s	3s	+0%
`mld_value_barrier_u8`	✅	3s	3s	+0%
`ntt_native_aarch64`	✅	3s	3s	+0%
`ntt_native_x86_64`	✅	3s	7s	-57%
`pack_sk_rho_key_tr_s2_t0`	✅	3s	3s	+0%
`pack_sk_s1`	✅	3s	3s	+0%
`pointwise_acc_native_aarch64`	✅	3s	7s	-57%
`poly_decompose_native`	✅	3s	2s	+50%
`poly_invntt_tomont`	✅	3s	3s	+0%
`poly_invntt_tomont_native`	✅	3s	2s	+50%
`poly_make_hint`	✅	3s	5s	-40%
`poly_ntt`	✅	3s	2s	+50%
`poly_pointwise_montgomery`	✅	3s	1s	+200%
`poly_reduce`	✅	3s	2s	+50%
`poly_uniform_gamma1`	✅	3s	2s	+50%
`poly_uniform_gamma1_4x`	✅	3s	3s	+0%
`poly_use_hint_native`	✅	3s	3s	+0%
`polyvec_matrix_pointwise_montgomery`	✅	3s	2s	+50%
`polyveck_pack_t0`	✅	3s	3s	+0%
`polyveck_unpack_t0`	✅	3s	3s	+0%
`polyvecl_pointwise_acc_montgomery`	✅	3s	3s	+0%
`polyvecl_pointwise_acc_montgomery_c`	✅	3s	2s	+50%
`polyvecl_pointwise_acc_montgomery_native`	✅	3s	2s	+50%
`polyvecl_unpack_z`	✅	3s	3s	+0%
`shake128_init`	✅	3s	4s	-25%
`shake128_release`	✅	3s	3s	+0%
`shake128x4_squeezeblocks`	✅	3s	4s	-25%
`shake256_init`	✅	3s	3s	+0%
`shake256_release`	✅	3s	3s	+0%
`sign_keypair`	✅	3s	4s	-25%
`sign_signature_internal`	✅	3s	3s	+0%
`sign_signature_pre_hash_shake256`	✅	3s	3s	+0%
`sk_t0hat_get_poly`	✅	3s	4s	-25%
`unpack_hints`	✅	3s	6s	-50%
`unpack_pk`	✅	3s	3s	+0%
`unpack_sk`	✅	3s	3s	+0%
`unpack_sk_t0hat`	✅	3s	4s	-25%
`keccak_f1600_x1_native_aarch64`	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	2s	2s	+0%
`keccak_finalize`	✅	2s	2s	+0%
`keccak_init`	✅	2s	2s	+0%
`keccakf1600_extract_bytes (big endian)`	✅	2s	2s	+0%
`mld_ct_abs_i32`	✅	2s	3s	-33%
`mld_ct_cmask_nonzero_u32`	✅	2s	4s	-50%
`mld_ct_sel_int32`	✅	2s	3s	-33%
`mld_keccakf1600_extract_bytes`	✅	2s	2s	+0%
`pack_sig_h_poly`	✅	2s	2s	+0%
`pack_sig_z`	✅	2s	2s	+0%
`pointwise_native_aarch64`	✅	2s	4s	-50%
`poly_caddq`	✅	2s	3s	-33%
`poly_chknorm_native`	✅	2s	2s	+0%
`poly_permute_bitrev_to_custom_optional`	✅	2s	1s	+100%
`poly_pointwise_montgomery_native`	✅	2s	5s	-60%
`poly_sub`	✅	2s	4s	-50%
`poly_use_hint`	✅	2s	2s	+0%
`polyeta_pack`	✅	2s	2s	+0%
`polyt1_pack`	✅	2s	5s	-60%
`polyveck_pack_w1`	✅	2s	3s	-33%
`polyvecl_pack_eta`	✅	2s	3s	-33%
`polyvecl_uniform_gamma1_serial`	✅	2s	3s	-33%
`polyw1_pack`	✅	2s	2s	+0%
`polyz_unpack`	✅	2s	2s	+0%
`power2round`	✅	2s	3s	-33%
`reduce32`	✅	2s	3s	-33%
`rej_eta`	✅	2s	4s	-50%
`shake128_absorb`	✅	2s	2s	+0%
`shake128x4_absorb_once`	✅	2s	2s	+0%
`shake256_absorb`	✅	2s	1s	+100%
`shake256_squeeze`	✅	2s	2s	+0%
`shake256x4_absorb_once`	✅	2s	3s	-33%
`sign_verify_pre_hash_internal`	✅	2s	5s	-60%
`sk_s1hat_get_poly`	✅	2s	4s	-50%
`sys_check_capability`	✅	2s	4s	-50%
`unpack_sk_s1hat`	✅	2s	3s	-33%
`unpack_sk_s2hat`	✅	2s	2s	+0%
`use_hint`	✅	2s	3s	-33%
`yvec_get_poly`	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64_v84a`	✅	1s	5s	-80%
`keccak_f1600_x4_native_aarch64_v84a`	✅	1s	2s	-50%
`keccakf1600_xor_bytes (big endian)`	✅	1s	2s	-50%
`mld_value_barrier_i64`	✅	1s	3s	-67%
`poly_uniform_4x`	✅	1s	4s	-75%
`shake128_finalize`	✅	1s	2s	-50%
`shake256x4_squeezeblocks`	✅	1s	2s	-50%
`sk_s2hat_get_poly`	✅	1s	3s	-67%
`yvec_init`	✅	1s	5s	-80%

oqs-bot · 2026-04-28T13:17:53Z

CBMC Results (ML-DSA-65)

Full Results (197 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	2591s	2506s	+3.4%
`polyvecl_pointwise_acc_montgomery_c`	✅	680s	569s	+20%
`sign_verify_internal`	✅	195s	283s	-31%
`polyvec_matrix_expand`	✅	139s	134s	+4%
`rej_uniform_native`	✅	133s	127s	+5%
`poly_pointwise_montgomery_c`	✅	114s	114s	+0%
`mld_invntt_layer`	✅	102s	102s	+0%
`mld_ct_memcmp`	✅	87s	80s	+9%
`mld_attempt_signature_generation`	✅	51s	49s	+4%
`mld_ntt_layer`	✅	45s	44s	+2%
`sign_signature_internal`	✅	32s	31s	+3%
`sign_keypair_internal`	✅	31s	31s	+0%
`fqmul`	✅	30s	30s	+0%
`polyvec_matrix_expand_serial`	✅	26s	25s	+4%
`keccakf1600x4_permute_native`	✅	25s	23s	+9%
`polyvec_matrix_pointwise_montgomery`	✅	24s	22s	+9%
`sign_pk_from_sk`	✅	22s	22s	+0%
`polyvec_matrix_pointwise_montgomery_yvec`	✅	21s	20s	+5%
`mld_ntt_butterfly_block`	✅	19s	17s	+12%
`poly_chknorm_c`	✅	19s	18s	+6%
`rej_uniform_c`	✅	19s	15s	+27%
`polyveck_decompose`	✅	18s	12s	+50%
`polyveck_power2round`	✅	18s	10s	+80%
`poly_uniform_4x`	✅	17s	12s	+42%
`rej_uniform`	✅	17s	23s	-26%
`polyt0_unpack`	✅	15s	19s	-21%
`poly_uniform_eta_4x`	✅	13s	12s	+8%
`poly_add`	✅	12s	12s	+0%
`poly_power2round`	✅	11s	7s	+57%
`poly_invntt_tomont_c`	✅	10s	8s	+25%
`polyveck_add`	✅	10s	11s	-9%
`keccak_absorb_once_x4`	✅	9s	9s	+0%
`mld_check_pct`	✅	9s	10s	-10%
`polyveck_use_hint`	✅	9s	10s	-10%
`mld_compute_pack_z`	✅	8s	7s	+14%
`pointwise_acc_native_x86_64`	✅	8s	7s	+14%
`polyveck_ntt`	✅	8s	7s	+14%
`polyveck_pointwise_poly_montgomery`	✅	8s	6s	+33%
`polyveck_shiftl`	✅	8s	7s	+14%
`keccak_absorb`	✅	7s	6s	+17%
`keccak_squeezeblocks_x4`	✅	7s	5s	+40%
`pack_pk`	✅	7s	2s	+250%
`polyveck_invntt_tomont`	✅	7s	8s	-12%
`polyveck_unpack_eta`	✅	7s	2s	+250%
`polyvecl_chknorm`	✅	7s	6s	+17%
`polyz_unpack_c`	✅	7s	9s	-22%
`sign`	✅	7s	7s	+0%
`keccakf1600_permute`	✅	6s	8s	-25%
`mld_prepare_domain_separation_prefix`	✅	6s	4s	+50%
`mld_sample_s1_s2`	✅	6s	5s	+20%
`poly_caddq_c`	✅	6s	4s	+50%
`poly_uniform`	✅	6s	4s	+50%
`polyveck_caddq`	✅	6s	7s	-14%
`polyveck_reduce`	✅	6s	5s	+20%
`polyvecl_ntt`	✅	6s	8s	-25%
`sign_signature_extmu`	✅	6s	4s	+50%
`sign_signature_pre_hash_shake256`	✅	6s	6s	+0%
`sign_verify_extmu`	✅	6s	6s	+0%
`unpack_sig`	✅	6s	3s	+100%
`unpack_sk`	✅	6s	3s	+100%
`keccakf1600_extract_bytes (big endian)`	✅	5s	4s	+25%
`keccakf1600_permute_native`	✅	5s	8s	-38%
`mld_ct_get_optblocker_u32`	✅	5s	1s	+400%
`nttunpack_native_x86_64`	✅	5s	2s	+150%
`pack_sk_rho_key_tr_s2_t0`	✅	5s	3s	+67%
`pointwise_acc_native_aarch64`	✅	5s	6s	-17%
`poly_chknorm_native`	✅	5s	4s	+25%
`poly_ntt`	✅	5s	3s	+67%
`poly_uniform_gamma1_4x`	✅	5s	3s	+67%
`polyvec_matrix_pointwise_montgomery_row`	✅	5s	4s	+25%
`polyveck_chknorm`	✅	5s	10s	-50%
`polyveck_sub`	✅	5s	7s	-29%
`polyvecl_pack_eta`	✅	5s	2s	+150%
`polyvecl_uniform_gamma1`	✅	5s	4s	+25%
`reduce32`	✅	5s	4s	+25%
`shake128_init`	✅	5s	5s	+0%
`shake256x4_absorb_once`	✅	5s	4s	+25%
`sign_signature`	✅	5s	4s	+25%
`sign_verify`	✅	5s	6s	-17%
`sign_verify_pre_hash_internal`	✅	5s	4s	+25%
`unpack_sk_s2hat`	✅	5s	5s	+0%
`unpack_sk_t0hat`	✅	5s	2s	+150%
`keccakf1600x4_extract_bytes`	✅	4s	4s	+0%
`make_hint`	✅	4s	4s	+0%
`mld_ct_get_optblocker_i64`	✅	4s	2s	+100%
`mld_h`	✅	4s	2s	+100%
`mld_sample_s1_s2_serial`	✅	4s	4s	+0%
`pointwise_native_x86_64`	✅	4s	2s	+100%
`poly_caddq_native_aarch64`	✅	4s	3s	+33%
`poly_ntt_c`	✅	4s	3s	+33%
`poly_permute_bitrev_to_custom_optional`	✅	4s	4s	+0%
`poly_permute_bitrev_to_custom_optional_native`	✅	4s	3s	+33%
`poly_pointwise_montgomery_native`	✅	4s	2s	+100%
`poly_uniform_eta`	✅	4s	4s	+0%
`poly_use_hint_c`	✅	4s	2s	+100%
`polyeta_unpack`	✅	4s	3s	+33%
`polyt0_pack`	✅	4s	3s	+33%
`polyt1_unpack`	✅	4s	4s	+0%
`polyveck_pack_eta`	✅	4s	3s	+33%
`polyveck_unpack_t0`	✅	4s	3s	+33%
`polyvecl_pointwise_acc_montgomery`	✅	4s	2s	+100%
`polyw1_pack`	✅	4s	4s	+0%
`rej_eta`	✅	4s	3s	+33%
`shake256_squeeze`	✅	4s	3s	+33%
`sign_keypair`	✅	4s	4s	+0%
`use_hint`	✅	4s	3s	+33%
`caddq`	✅	3s	5s	-40%
`decompose`	✅	3s	3s	+0%
`intt_native_x86_64`	✅	3s	3s	+0%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	3s	4s	-25%
`keccak_squeeze`	✅	3s	1s	+200%
`keccakf1600_xor_bytes (big endian)`	✅	3s	5s	-40%
`keccakf1600x4_xor_bytes`	✅	3s	4s	-25%
`mld_ct_abs_i32`	✅	3s	2s	+50%
`mld_ct_cmask_neg_i32`	✅	3s	3s	+0%
`mld_ct_cmask_nonzero_u8`	✅	3s	1s	+200%
`mld_ct_get_optblocker_u8`	✅	3s	4s	-25%
`mld_polymat_expand_entry`	✅	3s	2s	+50%
`mld_value_barrier_u32`	✅	3s	2s	+50%
`mld_value_barrier_u8`	✅	3s	3s	+0%
`ntt_native_aarch64`	✅	3s	3s	+0%
`ntt_native_x86_64`	✅	3s	2s	+50%
`pack_sig_c`	✅	3s	2s	+50%
`pack_sig_h_poly`	✅	3s	1s	+200%
`pack_sk_s1`	✅	3s	3s	+0%
`poly_caddq`	✅	3s	3s	+0%
`poly_caddq_native`	✅	3s	3s	+0%
`poly_challenge`	✅	3s	4s	-25%
`poly_chknorm`	✅	3s	4s	-25%
`poly_decompose`	✅	3s	3s	+0%
`poly_decompose_c`	✅	3s	3s	+0%
`poly_ntt_native`	✅	3s	2s	+50%
`poly_shiftl`	✅	3s	7s	-57%
`poly_sub`	✅	3s	3s	+0%
`poly_uniform_gamma1`	✅	3s	6s	-50%
`poly_use_hint`	✅	3s	4s	-25%
`polyeta_pack`	✅	3s	4s	-25%
`polyveck_pack_t0`	✅	3s	2s	+50%
`polyveck_pack_w1`	✅	3s	2s	+50%
`polyvecl_uniform_gamma1_serial`	✅	3s	2s	+50%
`polyvecl_unpack_eta`	✅	3s	4s	-25%
`polyvecl_unpack_z`	✅	3s	2s	+50%
`polyz_pack`	✅	3s	3s	+0%
`polyz_unpack`	✅	3s	2s	+50%
`polyz_unpack_native`	✅	3s	6s	-50%
`rej_eta_c`	✅	3s	4s	-25%
`shake128_squeeze`	✅	3s	3s	+0%
`shake128x4_absorb_once`	✅	3s	2s	+50%
`shake128x4_squeezeblocks`	✅	3s	3s	+0%
`shake256`	✅	3s	1s	+200%
`shake256_finalize`	✅	3s	3s	+0%
`shake256_release`	✅	3s	2s	+50%
`shake256x4_squeezeblocks`	✅	3s	2s	+50%
`sign_open`	✅	3s	4s	-25%
`sign_signature_pre_hash_internal`	✅	3s	4s	-25%
`sign_verify_pre_hash_shake256`	✅	3s	3s	+0%
`sk_t0hat_get_poly`	✅	3s	2s	+50%
`unpack_hints`	✅	3s	7s	-57%
`yvec_get_poly`	✅	3s	2s	+50%
`fqscale`	✅	2s	4s	-50%
`keccak_f1600_x1_native_aarch64`	✅	2s	1s	+100%
`keccak_f1600_x4_native_aarch64_v84a`	✅	2s	3s	-33%
`keccak_finalize`	✅	2s	2s	+0%
`keccak_init`	✅	2s	4s	-50%
`keccakf1600x4_permute`	✅	2s	2s	+0%
`mld_ct_cmask_nonzero_u32`	✅	2s	2s	+0%
`mld_ct_sel_int32`	✅	2s	2s	+0%
`mld_keccakf1600_extract_bytes`	✅	2s	3s	-33%
`mld_value_barrier_i64`	✅	2s	2s	+0%
`pack_sig_z`	✅	2s	4s	-50%
`pointwise_native_aarch64`	✅	2s	3s	-33%
`poly_chknorm_native_aarch64`	✅	2s	2s	+0%
`poly_decompose_native`	✅	2s	5s	-60%
`poly_invntt_tomont`	✅	2s	2s	+0%
`poly_invntt_tomont_native`	✅	2s	6s	-67%
`poly_make_hint`	✅	2s	5s	-60%
`poly_pointwise_montgomery`	✅	2s	2s	+0%
`poly_reduce`	✅	2s	3s	-33%
`poly_use_hint_native`	✅	2s	3s	-33%
`polyt1_pack`	✅	2s	5s	-60%
`polyvecl_pointwise_acc_montgomery_native`	✅	2s	3s	-33%
`rej_eta_native`	✅	2s	4s	-50%
`shake128_release`	✅	2s	5s	-60%
`shake256_absorb`	✅	2s	2s	+0%
`shake256_init`	✅	2s	2s	+0%
`sk_s2hat_get_poly`	✅	2s	3s	-33%
`sys_check_capability`	✅	2s	4s	-50%
`unpack_pk`	✅	2s	3s	-33%
`unpack_sk_s1hat`	✅	2s	3s	-33%
`yvec_init`	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64_v84a`	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	1s	3s	-67%
`keccakf1600_xor_bytes`	✅	1s	1s	+0%
`montgomery_reduce`	✅	1s	1s	+0%
`power2round`	✅	1s	3s	-67%
`shake128_absorb`	✅	1s	4s	-75%
`shake128_finalize`	✅	1s	2s	-50%
`sk_s1hat_get_poly`	✅	1s	3s	-67%

oqs-bot · 2026-04-28T13:18:48Z

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

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`poly_pointwise_montgomery_c`	⚠️	195s	110s	+77%
`rej_uniform`	⚠️	23s	11s	+109%
`rej_uniform_c`	⚠️	21s	9s	+133%

Full Results (197 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	1667s	1653s	+0.8%
`poly_pointwise_montgomery_c`	⚠️	195s	110s	+77%
`mld_invntt_layer`	✅	116s	112s	+4%
`rej_uniform_native`	✅	115s	114s	+1%
`mld_ct_memcmp`	✅	83s	81s	+2%
`polyvec_matrix_pointwise_montgomery_yvec`	✅	78s	68s	+15%
`sign_verify_internal`	✅	73s	180s	-59%
`mld_ntt_layer`	✅	46s	46s	+0%
`fqmul`	✅	33s	30s	+10%
`mld_attempt_signature_generation`	✅	28s	31s	-10%
`sign_keypair_internal`	✅	25s	20s	+25%
`rej_uniform`	⚠️	23s	11s	+109%
`keccakf1600x4_permute_native`	✅	22s	22s	+0%
`rej_uniform_c`	⚠️	21s	9s	+133%
`polyveck_decompose`	✅	18s	15s	+20%
`mld_ntt_butterfly_block`	✅	17s	19s	-11%
`polyveck_power2round`	✅	17s	14s	+21%
`polyvec_matrix_pointwise_montgomery_row`	✅	15s	8s	+88%
`polyt0_unpack`	✅	14s	18s	-22%
`poly_chknorm_c`	✅	13s	13s	+0%
`poly_uniform_eta_4x`	✅	13s	12s	+8%
`sign_pk_from_sk`	✅	13s	14s	-7%
`mld_check_pct`	✅	12s	13s	-8%
`polyveck_add`	✅	12s	12s	+0%
`poly_add`	✅	11s	10s	+10%
`polyvecl_chknorm`	✅	11s	8s	+38%
`polyveck_pointwise_poly_montgomery`	✅	10s	7s	+43%
`poly_invntt_tomont_c`	✅	9s	11s	-18%
`polyveck_invntt_tomont`	✅	9s	8s	+12%
`keccak_absorb_once_x4`	✅	8s	11s	-27%
`keccakf1600_permute`	✅	8s	7s	+14%
`mld_compute_pack_z`	✅	8s	5s	+60%
`poly_caddq_c`	✅	8s	7s	+14%
`polyveck_caddq`	✅	8s	7s	+14%
`polyveck_reduce`	✅	8s	8s	+0%
`sign`	✅	8s	9s	-11%
`keccak_absorb`	✅	7s	5s	+40%
`keccakf1600_permute_native`	✅	7s	7s	+0%
`poly_power2round`	✅	7s	3s	+133%
`polyveck_chknorm`	✅	7s	21s	-67%
`polyveck_ntt`	✅	7s	8s	-12%
`polyveck_use_hint`	✅	7s	9s	-22%
`polyvecl_ntt`	✅	7s	6s	+17%
`sign_keypair`	✅	7s	5s	+40%
`sign_open`	✅	7s	7s	+0%
`sign_verify`	✅	7s	5s	+40%
`keccak_squeezeblocks_x4`	✅	6s	5s	+20%
`pack_pk`	✅	6s	2s	+200%
`polyeta_unpack`	✅	6s	7s	-14%
`polyz_unpack_c`	✅	6s	3s	+100%
`sign_signature`	✅	6s	6s	+0%
`unpack_sig`	✅	6s	2s	+200%
`unpack_sk`	✅	6s	3s	+100%
`keccak_finalize`	✅	5s	2s	+150%
`mld_sample_s1_s2`	✅	5s	6s	-17%
`mld_sample_s1_s2_serial`	✅	5s	4s	+25%
`ntt_native_aarch64`	✅	5s	3s	+67%
`pack_sig_h_poly`	✅	5s	3s	+67%
`pack_sk_s1`	✅	5s	3s	+67%
`pointwise_acc_native_aarch64`	✅	5s	5s	+0%
`pointwise_acc_native_x86_64`	✅	5s	7s	-29%
`poly_decompose_c`	✅	5s	8s	-38%
`poly_decompose_native`	✅	5s	5s	+0%
`polyvec_matrix_expand`	✅	5s	3s	+67%
`polyveck_pack_t0`	✅	5s	3s	+67%
`polyveck_shiftl`	✅	5s	7s	-29%
`polyveck_sub`	✅	5s	6s	-17%
`sign_signature_pre_hash_shake256`	✅	5s	4s	+25%
`sk_s1hat_get_poly`	✅	5s	2s	+150%
`sys_check_capability`	✅	5s	2s	+150%
`caddq`	✅	4s	3s	+33%
`decompose`	✅	4s	2s	+100%
`keccakf1600_xor_bytes (big endian)`	✅	4s	3s	+33%
`keccakf1600x4_extract_bytes`	✅	4s	2s	+100%
`keccakf1600x4_permute`	✅	4s	3s	+33%
`make_hint`	✅	4s	3s	+33%
`mld_prepare_domain_separation_prefix`	✅	4s	3s	+33%
`ntt_native_x86_64`	✅	4s	2s	+100%
`nttunpack_native_x86_64`	✅	4s	2s	+100%
`pack_sk_rho_key_tr_s2_t0`	✅	4s	4s	+0%
`poly_caddq_native_aarch64`	✅	4s	4s	+0%
`poly_challenge`	✅	4s	6s	-33%
`poly_invntt_tomont`	✅	4s	2s	+100%
`poly_ntt_native`	✅	4s	3s	+33%
`poly_permute_bitrev_to_custom_optional_native`	✅	4s	3s	+33%
`poly_pointwise_montgomery_native`	✅	4s	5s	-20%
`poly_shiftl`	✅	4s	6s	-33%
`poly_uniform_eta`	✅	4s	3s	+33%
`poly_use_hint`	✅	4s	4s	+0%
`polyt1_unpack`	✅	4s	5s	-20%
`polyvec_matrix_pointwise_montgomery`	✅	4s	5s	-20%
`polyveck_pack_w1`	✅	4s	4s	+0%
`polyveck_unpack_eta`	✅	4s	3s	+33%
`polyvecl_unpack_eta`	✅	4s	4s	+0%
`rej_eta_native`	✅	4s	3s	+33%
`shake256_finalize`	✅	4s	2s	+100%
`shake256x4_absorb_once`	✅	4s	3s	+33%
`sign_signature_extmu`	✅	4s	5s	-20%
`sign_verify_pre_hash_shake256`	✅	4s	4s	+0%
`sk_t0hat_get_poly`	✅	4s	3s	+33%
`use_hint`	✅	4s	1s	+300%
`yvec_init`	✅	4s	4s	+0%
`fqscale`	✅	3s	4s	-25%
`keccak_f1600_x1_native_aarch64`	✅	3s	2s	+50%
`keccak_f1600_x1_native_aarch64_v84a`	✅	3s	2s	+50%
`keccak_init`	✅	3s	2s	+50%
`keccakf1600_extract_bytes (big endian)`	✅	3s	3s	+0%
`keccakf1600_xor_bytes`	✅	3s	1s	+200%
`keccakf1600x4_xor_bytes`	✅	3s	2s	+50%
`mld_ct_abs_i32`	✅	3s	2s	+50%
`mld_ct_cmask_neg_i32`	✅	3s	1s	+200%
`mld_ct_get_optblocker_u32`	✅	3s	2s	+50%
`mld_ct_get_optblocker_u8`	✅	3s	3s	+0%
`mld_keccakf1600_extract_bytes`	✅	3s	2s	+50%
`pointwise_native_aarch64`	✅	3s	2s	+50%
`poly_caddq_native`	✅	3s	2s	+50%
`poly_chknorm_native`	✅	3s	3s	+0%
`poly_decompose`	✅	3s	2s	+50%
`poly_invntt_tomont_native`	✅	3s	3s	+0%
`poly_make_hint`	✅	3s	3s	+0%
`poly_ntt`	✅	3s	2s	+50%
`poly_ntt_c`	✅	3s	3s	+0%
`poly_permute_bitrev_to_custom_optional`	✅	3s	2s	+50%
`poly_sub`	✅	3s	4s	-25%
`poly_uniform_4x`	✅	3s	2s	+50%
`poly_uniform_gamma1`	✅	3s	3s	+0%
`poly_use_hint_c`	✅	3s	4s	-25%
`polyt0_pack`	✅	3s	3s	+0%
`polyveck_unpack_t0`	✅	3s	5s	-40%
`polyvecl_pack_eta`	✅	3s	4s	-25%
`polyvecl_pointwise_acc_montgomery_c`	✅	3s	3s	+0%
`polyvecl_uniform_gamma1`	✅	3s	3s	+0%
`polyvecl_uniform_gamma1_serial`	✅	3s	6s	-50%
`polyvecl_unpack_z`	✅	3s	3s	+0%
`polyw1_pack`	✅	3s	2s	+50%
`polyz_unpack`	✅	3s	3s	+0%
`polyz_unpack_native`	✅	3s	2s	+50%
`reduce32`	✅	3s	6s	-50%
`rej_eta_c`	✅	3s	5s	-40%
`shake128_finalize`	✅	3s	2s	+50%
`shake128_init`	✅	3s	1s	+200%
`shake128x4_absorb_once`	✅	3s	2s	+50%
`shake128x4_squeezeblocks`	✅	3s	2s	+50%
`shake256x4_squeezeblocks`	✅	3s	3s	+0%
`sign_signature_pre_hash_internal`	✅	3s	5s	-40%
`sign_verify_extmu`	✅	3s	3s	+0%
`sign_verify_pre_hash_internal`	✅	3s	5s	-40%
`sk_s2hat_get_poly`	✅	3s	4s	-25%
`unpack_hints`	✅	3s	6s	-50%
`unpack_sk_s1hat`	✅	3s	5s	-40%
`unpack_sk_s2hat`	✅	3s	3s	+0%
`unpack_sk_t0hat`	✅	3s	3s	+0%
`yvec_get_poly`	✅	3s	2s	+50%
`intt_native_x86_64`	✅	2s	6s	-67%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	2s	3s	-33%
`mld_ct_cmask_nonzero_u32`	✅	2s	6s	-67%
`mld_ct_cmask_nonzero_u8`	✅	2s	4s	-50%
`mld_ct_sel_int32`	✅	2s	4s	-50%
`mld_h`	✅	2s	3s	-33%
`mld_polymat_expand_entry`	✅	2s	3s	-33%
`mld_value_barrier_u32`	✅	2s	2s	+0%
`montgomery_reduce`	✅	2s	1s	+100%
`pack_sig_c`	✅	2s	4s	-50%
`pack_sig_z`	✅	2s	2s	+0%
`pointwise_native_x86_64`	✅	2s	3s	-33%
`poly_caddq`	✅	2s	7s	-71%
`poly_chknorm`	✅	2s	3s	-33%
`poly_chknorm_native_aarch64`	✅	2s	5s	-60%
`poly_pointwise_montgomery`	✅	2s	2s	+0%
`poly_uniform`	✅	2s	3s	-33%
`poly_uniform_gamma1_4x`	✅	2s	5s	-60%
`poly_use_hint_native`	✅	2s	4s	-50%
`polyt1_pack`	✅	2s	3s	-33%
`polyvec_matrix_expand_serial`	✅	2s	3s	-33%
`polyveck_pack_eta`	✅	2s	2s	+0%
`polyvecl_pointwise_acc_montgomery`	✅	2s	6s	-67%
`polyvecl_pointwise_acc_montgomery_native`	✅	2s	4s	-50%
`polyz_pack`	✅	2s	3s	-33%
`power2round`	✅	2s	3s	-33%
`rej_eta`	✅	2s	3s	-33%
`shake128_absorb`	✅	2s	2s	+0%
`shake128_release`	✅	2s	5s	-60%
`shake128_squeeze`	✅	2s	3s	-33%
`shake256_absorb`	✅	2s	3s	-33%
`shake256_init`	✅	2s	3s	-33%
`shake256_squeeze`	✅	2s	2s	+0%
`sign_signature_internal`	✅	2s	4s	-50%
`unpack_pk`	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v84a`	✅	1s	4s	-75%
`keccak_squeeze`	✅	1s	4s	-75%
`mld_ct_get_optblocker_i64`	✅	1s	2s	-50%
`mld_value_barrier_i64`	✅	1s	1s	+0%
`mld_value_barrier_u8`	✅	1s	3s	-67%
`poly_reduce`	✅	1s	1s	+0%
`polyeta_pack`	✅	1s	2s	-50%
`shake256`	✅	1s	2s	-50%
`shake256_release`	✅	1s	3s	-67%

oqs-bot · 2026-04-28T13:19:04Z

CBMC Results (ML-DSA-87)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`polyveck_power2round`	⚠️	32s	8s	+300%

Full Results (197 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	2349s	2392s	-1.8%
`polyvecl_pointwise_acc_montgomery_c`	✅	349s	331s	+5%
`sign_verify_internal`	✅	263s	335s	-21%
`polyvec_matrix_expand`	✅	171s	156s	+10%
`rej_uniform_native`	✅	124s	119s	+4%
`poly_pointwise_montgomery_c`	✅	100s	99s	+1%
`mld_invntt_layer`	✅	99s	94s	+5%
`mld_ct_memcmp`	✅	77s	72s	+7%
`mld_attempt_signature_generation`	✅	58s	77s	-25%
`polyvec_matrix_expand_serial`	✅	56s	57s	-2%
`sign_keypair_internal`	✅	54s	51s	+6%
`mld_ntt_layer`	✅	43s	41s	+5%
`sign_signature_internal`	✅	33s	33s	+0%
`polyveck_power2round`	⚠️	32s	8s	+300%
`sign_pk_from_sk`	✅	32s	35s	-9%
`fqmul`	✅	30s	27s	+11%
`polyvec_matrix_pointwise_montgomery`	✅	28s	29s	-3%
`keccakf1600x4_permute_native`	✅	21s	22s	-5%
`polyvec_matrix_pointwise_montgomery_yvec`	✅	18s	20s	-10%
`rej_uniform`	✅	17s	21s	-19%
`rej_uniform_c`	✅	17s	14s	+21%
`mld_ntt_butterfly_block`	✅	16s	16s	+0%
`poly_chknorm_c`	✅	15s	18s	-17%
`polyt0_unpack`	✅	14s	19s	-26%
`polyveck_use_hint`	✅	14s	6s	+133%
`polyveck_add`	✅	12s	11s	+9%
`poly_add`	✅	11s	13s	-15%
`poly_uniform_4x`	✅	11s	11s	+0%
`poly_uniform_eta_4x`	✅	11s	13s	-15%
`polyveck_decompose`	✅	11s	22s	-50%
`mld_check_pct`	✅	10s	9s	+11%
`polyveck_ntt`	✅	10s	12s	-17%
`keccak_absorb_once_x4`	✅	9s	7s	+29%
`mld_compute_pack_z`	✅	9s	8s	+12%
`pointwise_acc_native_x86_64`	✅	8s	8s	+0%
`poly_decompose_c`	✅	8s	6s	+33%
`poly_power2round`	✅	8s	6s	+33%
`polyveck_pointwise_poly_montgomery`	✅	8s	6s	+33%
`polyveck_reduce`	✅	8s	6s	+33%
`polyveck_shiftl`	✅	8s	7s	+14%
`polyvecl_ntt`	✅	8s	6s	+33%
`sign`	✅	8s	6s	+33%
`keccak_absorb`	✅	7s	9s	-22%
`keccakf1600_permute_native`	✅	7s	8s	-12%
`poly_invntt_tomont_c`	✅	7s	11s	-36%
`polyveck_chknorm`	✅	7s	4s	+75%
`caddq`	✅	6s	5s	+20%
`mld_sample_s1_s2`	✅	6s	6s	+0%
`rej_eta_native`	✅	6s	4s	+50%
`sign_signature`	✅	6s	4s	+50%
`sign_verify_pre_hash_internal`	✅	6s	4s	+50%
`unpack_sk_s2hat`	✅	6s	4s	+50%
`keccak_f1600_x1_native_aarch64_v84a`	✅	5s	2s	+150%
`keccakf1600_permute`	✅	5s	6s	-17%
`mld_ct_sel_int32`	✅	5s	2s	+150%
`mld_sample_s1_s2_serial`	✅	5s	7s	-29%
`montgomery_reduce`	✅	5s	4s	+25%
`pack_sk_rho_key_tr_s2_t0`	✅	5s	4s	+25%
`pointwise_acc_native_aarch64`	✅	5s	6s	-17%
`poly_caddq_c`	✅	5s	6s	-17%
`poly_caddq_native_aarch64`	✅	5s	2s	+150%
`poly_decompose`	✅	5s	3s	+67%
`polyt0_pack`	✅	5s	4s	+25%
`polyveck_caddq`	✅	5s	4s	+25%
`polyveck_invntt_tomont`	✅	5s	5s	+0%
`polyveck_sub`	✅	5s	7s	-29%
`polyveck_unpack_eta`	✅	5s	4s	+25%
`polyvecl_uniform_gamma1_serial`	✅	5s	4s	+25%
`sign_signature_extmu`	✅	5s	2s	+150%
`decompose`	✅	4s	3s	+33%
`keccak_squeezeblocks_x4`	✅	4s	4s	+0%
`keccakf1600x4_permute`	✅	4s	2s	+100%
`make_hint`	✅	4s	2s	+100%
`mld_h`	✅	4s	2s	+100%
`mld_prepare_domain_separation_prefix`	✅	4s	3s	+33%
`ntt_native_aarch64`	✅	4s	3s	+33%
`ntt_native_x86_64`	✅	4s	5s	-20%
`pack_sig_h_poly`	✅	4s	4s	+0%
`pack_sig_z`	✅	4s	1s	+300%
`poly_caddq`	✅	4s	3s	+33%
`poly_challenge`	✅	4s	4s	+0%
`poly_chknorm`	✅	4s	4s	+0%
`poly_invntt_tomont`	✅	4s	2s	+100%
`poly_invntt_tomont_native`	✅	4s	6s	-33%
`poly_make_hint`	✅	4s	2s	+100%
`poly_ntt_native`	✅	4s	5s	-20%
`poly_reduce`	✅	4s	3s	+33%
`poly_uniform_gamma1_4x`	✅	4s	4s	+0%
`poly_use_hint_c`	✅	4s	4s	+0%
`polyeta_unpack`	✅	4s	8s	-50%
`polyveck_pack_eta`	✅	4s	3s	+33%
`polyveck_pack_t0`	✅	4s	3s	+33%
`polyvecl_chknorm`	✅	4s	4s	+0%
`polyvecl_pointwise_acc_montgomery`	✅	4s	2s	+100%
`polyvecl_uniform_gamma1`	✅	4s	2s	+100%
`polyz_pack`	✅	4s	4s	+0%
`shake256_release`	✅	4s	2s	+100%
`shake256x4_absorb_once`	✅	4s	1s	+300%
`shake256x4_squeezeblocks`	✅	4s	4s	+0%
`sign_signature_pre_hash_internal`	✅	4s	4s	+0%
`sign_signature_pre_hash_shake256`	✅	4s	2s	+100%
`sign_verify`	✅	4s	6s	-33%
`sys_check_capability`	✅	4s	5s	-20%
`unpack_hints`	✅	4s	6s	-33%
`unpack_sk_s1hat`	✅	4s	4s	+0%
`fqscale`	✅	3s	2s	+50%
`keccak_f1600_x4_native_aarch64_v84a`	✅	3s	4s	-25%
`keccakf1600_extract_bytes (big endian)`	✅	3s	2s	+50%
`keccakf1600x4_xor_bytes`	✅	3s	3s	+0%
`mld_ct_abs_i32`	✅	3s	1s	+200%
`mld_ct_cmask_nonzero_u8`	✅	3s	4s	-25%
`mld_ct_get_optblocker_u32`	✅	3s	2s	+50%
`mld_polymat_expand_entry`	✅	3s	4s	-25%
`pointwise_native_x86_64`	✅	3s	3s	+0%
`poly_caddq_native`	✅	3s	3s	+0%
`poly_chknorm_native`	✅	3s	4s	-25%
`poly_chknorm_native_aarch64`	✅	3s	3s	+0%
`poly_ntt`	✅	3s	3s	+0%
`poly_ntt_c`	✅	3s	4s	-25%
`poly_permute_bitrev_to_custom_optional`	✅	3s	2s	+50%
`poly_shiftl`	✅	3s	5s	-40%
`polyvec_matrix_pointwise_montgomery_row`	✅	3s	2s	+50%
`polyveck_pack_w1`	✅	3s	4s	-25%
`polyveck_unpack_t0`	✅	3s	4s	-25%
`polyvecl_pointwise_acc_montgomery_native`	✅	3s	3s	+0%
`polyvecl_unpack_eta`	✅	3s	5s	-40%
`polyz_unpack`	✅	3s	2s	+50%
`polyz_unpack_c`	✅	3s	4s	-25%
`power2round`	✅	3s	1s	+200%
`reduce32`	✅	3s	4s	-25%
`rej_eta`	✅	3s	2s	+50%
`rej_eta_c`	✅	3s	4s	-25%
`shake128_finalize`	✅	3s	1s	+200%
`shake128_init`	✅	3s	1s	+200%
`shake128_release`	✅	3s	2s	+50%
`shake128x4_absorb_once`	✅	3s	2s	+50%
`shake256_absorb`	✅	3s	4s	-25%
`shake256_init`	✅	3s	3s	+0%
`shake256_squeeze`	✅	3s	4s	-25%
`sign_keypair`	✅	3s	2s	+50%
`sign_open`	✅	3s	6s	-50%
`sign_verify_extmu`	✅	3s	3s	+0%
`sign_verify_pre_hash_shake256`	✅	3s	4s	-25%
`sk_s2hat_get_poly`	✅	3s	3s	+0%
`sk_t0hat_get_poly`	✅	3s	3s	+0%
`unpack_pk`	✅	3s	3s	+0%
`unpack_sig`	✅	3s	2s	+50%
`use_hint`	✅	3s	4s	-25%
`intt_native_x86_64`	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	2s	1s	+100%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	2s	2s	+0%
`keccak_finalize`	✅	2s	6s	-67%
`keccak_init`	✅	2s	2s	+0%
`keccak_squeeze`	✅	2s	4s	-50%
`keccakf1600_xor_bytes`	✅	2s	2s	+0%
`mld_ct_cmask_nonzero_u32`	✅	2s	2s	+0%
`mld_keccakf1600_extract_bytes`	✅	2s	2s	+0%
`mld_value_barrier_i64`	✅	2s	2s	+0%
`mld_value_barrier_u8`	✅	2s	4s	-50%
`nttunpack_native_x86_64`	✅	2s	3s	-33%
`pack_pk`	✅	2s	3s	-33%
`pack_sig_c`	✅	2s	3s	-33%
`pack_sk_s1`	✅	2s	4s	-50%
`pointwise_native_aarch64`	✅	2s	5s	-60%
`poly_decompose_native`	✅	2s	3s	-33%
`poly_pointwise_montgomery_native`	✅	2s	3s	-33%
`poly_sub`	✅	2s	3s	-33%
`poly_uniform`	✅	2s	3s	-33%
`poly_uniform_gamma1`	✅	2s	5s	-60%
`poly_use_hint_native`	✅	2s	2s	+0%
`polyeta_pack`	✅	2s	1s	+100%
`polyt1_pack`	✅	2s	3s	-33%
`polyt1_unpack`	✅	2s	2s	+0%
`polyvecl_pack_eta`	✅	2s	3s	-33%
`polyvecl_unpack_z`	✅	2s	2s	+0%
`polyw1_pack`	✅	2s	2s	+0%
`polyz_unpack_native`	✅	2s	3s	-33%
`shake128_absorb`	✅	2s	3s	-33%
`shake128x4_squeezeblocks`	✅	2s	2s	+0%
`shake256`	✅	2s	2s	+0%
`shake256_finalize`	✅	2s	4s	-50%
`sk_s1hat_get_poly`	✅	2s	5s	-60%
`unpack_sk`	✅	2s	4s	-50%
`unpack_sk_t0hat`	✅	2s	3s	-33%
`yvec_get_poly`	✅	2s	2s	+0%
`yvec_init`	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64`	✅	1s	3s	-67%
`keccakf1600_xor_bytes (big endian)`	✅	1s	4s	-75%
`keccakf1600x4_extract_bytes`	✅	1s	2s	-50%
`mld_ct_cmask_neg_i32`	✅	1s	2s	-50%
`mld_ct_get_optblocker_i64`	✅	1s	3s	-67%
`mld_ct_get_optblocker_u8`	✅	1s	2s	-50%
`mld_value_barrier_u32`	✅	1s	5s	-80%
`poly_permute_bitrev_to_custom_optional_native`	✅	1s	4s	-75%
`poly_pointwise_montgomery`	✅	1s	2s	-50%
`poly_uniform_eta`	✅	1s	4s	-75%
`poly_use_hint`	✅	1s	2s	-50%
`shake128_squeeze`	✅	1s	3s	-67%

oqs-bot · 2026-04-28T13:28:13Z

CBMC Results (ML-DSA-44)

Full Results (197 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	1612s	1867s	-13.7%
`rej_uniform_native`	✅	120s	124s	-3%
`polyvecl_pointwise_acc_montgomery_c`	✅	112s	126s	-11%
`sign_verify_internal`	✅	106s	281s	-62%
`mld_invntt_layer`	✅	94s	96s	-2%
`poly_pointwise_montgomery_c`	✅	91s	109s	-17%
`mld_ct_memcmp`	✅	76s	80s	-5%
`mld_attempt_signature_generation`	✅	47s	71s	-34%
`mld_ntt_layer`	✅	42s	45s	-7%
`fqmul`	✅	29s	28s	+4%
`polyvec_matrix_expand`	✅	25s	26s	-4%
`keccakf1600x4_permute_native`	✅	24s	22s	+9%
`sign_keypair_internal`	✅	24s	24s	+0%
`polyvec_matrix_pointwise_montgomery`	✅	23s	25s	-8%
`sign_pk_from_sk`	✅	22s	19s	+16%
`mld_ntt_butterfly_block`	✅	20s	18s	+11%
`rej_uniform`	✅	18s	21s	-14%
`polyveck_chknorm`	✅	17s	17s	+0%
`rej_uniform_c`	✅	17s	16s	+6%
`poly_chknorm_c`	✅	16s	19s	-16%
`polyt0_unpack`	✅	15s	18s	-17%
`sign_signature_internal`	✅	15s	15s	+0%
`polyvec_matrix_pointwise_montgomery_yvec`	✅	13s	12s	+8%
`poly_uniform_eta_4x`	✅	12s	12s	+0%
`poly_add`	✅	11s	11s	+0%
`poly_uniform_4x`	✅	11s	10s	+10%
`poly_invntt_tomont_c`	✅	10s	9s	+11%
`poly_power2round`	✅	10s	8s	+25%
`keccak_absorb_once_x4`	✅	9s	10s	-10%
`polyz_unpack_c`	✅	9s	15s	-40%
`mld_check_pct`	✅	8s	8s	+0%
`keccakf1600_permute_native`	✅	7s	5s	+40%
`mld_compute_pack_z`	✅	7s	9s	-22%
`pointwise_acc_native_aarch64`	✅	7s	7s	+0%
`keccak_absorb`	✅	6s	5s	+20%
`keccakf1600_permute`	✅	6s	7s	-14%
`pointwise_acc_native_x86_64`	✅	6s	7s	-14%
`poly_caddq`	✅	6s	2s	+200%
`poly_decompose_c`	✅	6s	5s	+20%
`polyveck_decompose`	✅	6s	7s	-14%
`polyveck_pack_w1`	✅	6s	3s	+100%
`polyveck_reduce`	✅	6s	5s	+20%
`sign_signature`	✅	6s	5s	+20%
`sign_verify_pre_hash_shake256`	✅	6s	4s	+50%
`unpack_hints`	✅	6s	4s	+50%
`yvec_get_poly`	✅	6s	3s	+100%
`fqscale`	✅	5s	3s	+67%
`mld_prepare_domain_separation_prefix`	✅	5s	5s	+0%
`poly_challenge`	✅	5s	5s	+0%
`poly_decompose`	✅	5s	4s	+25%
`poly_shiftl`	✅	5s	5s	+0%
`polyvec_matrix_expand_serial`	✅	5s	7s	-29%
`polyveck_add`	✅	5s	5s	+0%
`polyveck_ntt`	✅	5s	5s	+0%
`polyveck_pointwise_poly_montgomery`	✅	5s	5s	+0%
`polyveck_power2round`	✅	5s	5s	+0%
`polyveck_unpack_eta`	✅	5s	2s	+150%
`polyvecl_chknorm`	✅	5s	5s	+0%
`polyvecl_ntt`	✅	5s	6s	-17%
`shake128x4_absorb_once`	✅	5s	2s	+150%
`shake128x4_squeezeblocks`	✅	5s	1s	+400%
`sign`	✅	5s	5s	+0%
`sign_open`	✅	5s	7s	-29%
`sign_signature_pre_hash_shake256`	✅	5s	4s	+25%
`sk_s1hat_get_poly`	✅	5s	5s	+0%
`unpack_sk_s1hat`	✅	5s	2s	+150%
`yvec_init`	✅	5s	2s	+150%
`keccak_squeezeblocks_x4`	✅	4s	4s	+0%
`keccakf1600x4_permute`	✅	4s	2s	+100%
`mld_ct_cmask_nonzero_u32`	✅	4s	3s	+33%
`mld_ct_get_optblocker_u8`	✅	4s	2s	+100%
`mld_value_barrier_i64`	✅	4s	2s	+100%
`nttunpack_native_x86_64`	✅	4s	3s	+33%
`pack_pk`	✅	4s	2s	+100%
`pack_sig_h_poly`	✅	4s	3s	+33%
`pack_sig_z`	✅	4s	5s	-20%
`pack_sk_rho_key_tr_s2_t0`	✅	4s	2s	+100%
`pack_sk_s1`	✅	4s	3s	+33%
`pointwise_native_aarch64`	✅	4s	2s	+100%
`poly_caddq_c`	✅	4s	3s	+33%
`poly_caddq_native`	✅	4s	2s	+100%
`poly_caddq_native_aarch64`	✅	4s	2s	+100%
`poly_chknorm`	✅	4s	3s	+33%
`poly_chknorm_native_aarch64`	✅	4s	2s	+100%
`poly_invntt_tomont_native`	✅	4s	2s	+100%
`poly_ntt`	✅	4s	4s	+0%
`poly_ntt_c`	✅	4s	2s	+100%
`poly_pointwise_montgomery`	✅	4s	2s	+100%
`poly_reduce`	✅	4s	1s	+300%
`poly_uniform`	✅	4s	5s	-20%
`poly_uniform_gamma1`	✅	4s	4s	+0%
`poly_use_hint`	✅	4s	2s	+100%
`poly_use_hint_c`	✅	4s	4s	+0%
`polyeta_unpack`	✅	4s	6s	-33%
`polyveck_caddq`	✅	4s	6s	-33%
`polyveck_sub`	✅	4s	6s	-33%
`polyveck_use_hint`	✅	4s	3s	+33%
`polyvecl_pointwise_acc_montgomery`	✅	4s	4s	+0%
`polyvecl_uniform_gamma1_serial`	✅	4s	4s	+0%
`polyz_pack`	✅	4s	5s	-20%
`power2round`	✅	4s	2s	+100%
`rej_eta_c`	✅	4s	5s	-20%
`shake128_absorb`	✅	4s	2s	+100%
`shake128_squeeze`	✅	4s	3s	+33%
`shake256_finalize`	✅	4s	2s	+100%
`sign_signature_extmu`	✅	4s	5s	-20%
`sign_signature_pre_hash_internal`	✅	4s	3s	+33%
`sign_verify`	✅	4s	3s	+33%
`sign_verify_extmu`	✅	4s	5s	-20%
`sign_verify_pre_hash_internal`	✅	4s	4s	+0%
`sk_s2hat_get_poly`	✅	4s	2s	+100%
`caddq`	✅	3s	2s	+50%
`intt_native_x86_64`	✅	3s	5s	-40%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	3s	1s	+200%
`keccakf1600x4_xor_bytes`	✅	3s	2s	+50%
`make_hint`	✅	3s	3s	+0%
`mld_ct_abs_i32`	✅	3s	2s	+50%
`mld_ct_cmask_nonzero_u8`	✅	3s	2s	+50%
`mld_h`	✅	3s	3s	+0%
`mld_polymat_expand_entry`	✅	3s	3s	+0%
`montgomery_reduce`	✅	3s	3s	+0%
`ntt_native_aarch64`	✅	3s	3s	+0%
`ntt_native_x86_64`	✅	3s	4s	-25%
`pointwise_native_x86_64`	✅	3s	5s	-40%
`poly_chknorm_native`	✅	3s	3s	+0%
`poly_decompose_native`	✅	3s	5s	-40%
`poly_invntt_tomont`	✅	3s	3s	+0%
`poly_permute_bitrev_to_custom_optional`	✅	3s	3s	+0%
`poly_uniform_eta`	✅	3s	3s	+0%
`polyeta_pack`	✅	3s	2s	+50%
`polyt0_pack`	✅	3s	2s	+50%
`polyt1_pack`	✅	3s	3s	+0%
`polyveck_invntt_tomont`	✅	3s	6s	-50%
`polyveck_pack_t0`	✅	3s	3s	+0%
`polyveck_shiftl`	✅	3s	3s	+0%
`polyveck_unpack_t0`	✅	3s	3s	+0%
`polyvecl_pack_eta`	✅	3s	2s	+50%
`polyvecl_unpack_eta`	✅	3s	2s	+50%
`reduce32`	✅	3s	3s	+0%
`rej_eta`	✅	3s	2s	+50%
`shake128_init`	✅	3s	3s	+0%
`shake128_release`	✅	3s	3s	+0%
`shake256_init`	✅	3s	4s	-25%
`sign_keypair`	✅	3s	5s	-40%
`sk_t0hat_get_poly`	✅	3s	1s	+200%
`unpack_sig`	✅	3s	5s	-40%
`decompose`	✅	2s	2s	+0%
`keccak_f1600_x1_native_aarch64`	✅	2s	1s	+100%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	2s	2s	+0%
`keccak_finalize`	✅	2s	3s	-33%
`keccak_init`	✅	2s	2s	+0%
`keccak_squeeze`	✅	2s	4s	-50%
`keccakf1600_extract_bytes (big endian)`	✅	2s	1s	+100%
`keccakf1600_xor_bytes`	✅	2s	4s	-50%
`keccakf1600_xor_bytes (big endian)`	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes`	✅	2s	4s	-50%
`mld_ct_cmask_neg_i32`	✅	2s	2s	+0%
`mld_ct_get_optblocker_u32`	✅	2s	2s	+0%
`mld_keccakf1600_extract_bytes`	✅	2s	2s	+0%
`mld_sample_s1_s2`	✅	2s	6s	-67%
`mld_sample_s1_s2_serial`	✅	2s	4s	-50%
`mld_value_barrier_u32`	✅	2s	3s	-33%
`mld_value_barrier_u8`	✅	2s	3s	-33%
`pack_sig_c`	✅	2s	5s	-60%
`poly_make_hint`	✅	2s	4s	-50%
`poly_ntt_native`	✅	2s	4s	-50%
`poly_uniform_gamma1_4x`	✅	2s	4s	-50%
`poly_use_hint_native`	✅	2s	4s	-50%
`polyt1_unpack`	✅	2s	4s	-50%
`polyvec_matrix_pointwise_montgomery_row`	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery_native`	✅	2s	2s	+0%
`polyvecl_unpack_z`	✅	2s	3s	-33%
`polyw1_pack`	✅	2s	3s	-33%
`polyz_unpack`	✅	2s	5s	-60%
`shake256`	✅	2s	2s	+0%
`shake256_release`	✅	2s	1s	+100%
`unpack_pk`	✅	2s	5s	-60%
`unpack_sk`	✅	2s	4s	-50%
`unpack_sk_s2hat`	✅	2s	2s	+0%
`unpack_sk_t0hat`	✅	2s	3s	-33%
`use_hint`	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64_v84a`	✅	1s	1s	+0%
`keccak_f1600_x4_native_aarch64_v84a`	✅	1s	3s	-67%
`mld_ct_get_optblocker_i64`	✅	1s	1s	+0%
`mld_ct_sel_int32`	✅	1s	4s	-75%
`poly_permute_bitrev_to_custom_optional_native`	✅	1s	4s	-75%
`poly_pointwise_montgomery_native`	✅	1s	1s	+0%
`poly_sub`	✅	1s	5s	-80%
`polyveck_pack_eta`	✅	1s	4s	-75%
`polyvecl_uniform_gamma1`	✅	1s	1s	+0%
`polyz_unpack_native`	✅	1s	3s	-67%
`rej_eta_native`	✅	1s	7s	-86%
`shake128_finalize`	✅	1s	2s	-50%
`shake256_absorb`	✅	1s	2s	-50%
`shake256_squeeze`	✅	1s	3s	-67%
`shake256x4_absorb_once`	✅	1s	3s	-67%
`shake256x4_squeezeblocks`	✅	1s	2s	-50%
`sys_check_capability`	✅	1s	2s	-50%

oqs-bot · 2026-04-28T13:44:25Z

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

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`poly_pointwise_montgomery_c`	⚠️	190s	100s	+90%
`rej_uniform`	⚠️	22s	7s	+214%

Full Results (197 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	1762s	1599s	+10.2%
`poly_pointwise_montgomery_c`	⚠️	190s	100s	+90%
`polyvec_matrix_pointwise_montgomery_yvec`	✅	149s	114s	+31%
`sign_verify_internal`	✅	131s	157s	-17%
`rej_uniform_native`	✅	114s	107s	+7%
`mld_invntt_layer`	✅	109s	101s	+8%
`mld_ct_memcmp`	✅	82s	74s	+11%
`mld_ntt_layer`	✅	44s	40s	+10%
`sign_keypair_internal`	✅	31s	32s	-3%
`fqmul`	✅	28s	27s	+4%
`keccakf1600x4_permute_native`	✅	24s	24s	+0%
`mld_attempt_signature_generation`	✅	24s	34s	-29%
`rej_uniform`	⚠️	22s	7s	+214%
`sign_pk_from_sk`	✅	20s	22s	-9%
`rej_uniform_c`	✅	19s	7s	+171%
`polyeta_unpack`	✅	18s	16s	+12%
`mld_ntt_butterfly_block`	✅	16s	15s	+7%
`polyvec_matrix_pointwise_montgomery_row`	✅	15s	8s	+88%
`poly_uniform_eta_4x`	✅	14s	12s	+17%
`polyveck_decompose`	✅	14s	9s	+56%
`mld_check_pct`	✅	13s	12s	+8%
`poly_chknorm_c`	✅	13s	16s	-19%
`poly_add`	✅	11s	10s	+10%
`polyt0_unpack`	✅	11s	16s	-31%
`keccak_absorb_once_x4`	✅	10s	10s	+0%
`pointwise_acc_native_x86_64`	✅	9s	5s	+80%
`polyveck_invntt_tomont`	✅	9s	9s	+0%
`poly_caddq_c`	✅	8s	5s	+60%
`poly_invntt_tomont_c`	✅	8s	8s	+0%
`poly_power2round`	✅	8s	4s	+100%
`polyvec_matrix_pointwise_montgomery`	✅	8s	7s	+14%
`polyveck_add`	✅	8s	9s	-11%
`polyveck_shiftl`	✅	8s	6s	+33%
`keccakf1600_permute`	✅	7s	8s	-12%
`keccakf1600_permute_native`	✅	7s	5s	+40%
`mld_sample_s1_s2`	✅	7s	7s	+0%
`pointwise_acc_native_aarch64`	✅	7s	8s	-12%
`poly_decompose_c`	✅	7s	5s	+40%
`polyveck_pointwise_poly_montgomery`	✅	7s	8s	-12%
`polyveck_power2round`	✅	7s	25s	-72%
`mld_compute_pack_z`	✅	6s	7s	-14%
`pack_sk_s1`	✅	6s	1s	+500%
`polyvec_matrix_expand`	✅	6s	2s	+200%
`polyveck_caddq`	✅	6s	7s	-14%
`polyveck_chknorm`	✅	6s	6s	+0%
`polyveck_ntt`	✅	6s	8s	-25%
`polyveck_reduce`	✅	6s	5s	+20%
`polyveck_sub`	✅	6s	4s	+50%
`polyveck_use_hint`	✅	6s	9s	-33%
`polyvecl_pointwise_acc_montgomery_native`	✅	6s	4s	+50%
`polyz_unpack_c`	✅	6s	4s	+50%
`sign_signature_pre_hash_internal`	✅	6s	3s	+100%
`sign_signature_pre_hash_shake256`	✅	6s	2s	+200%
`keccak_absorb`	✅	5s	6s	-17%
`mld_sample_s1_s2_serial`	✅	5s	5s	+0%
`ntt_native_aarch64`	✅	5s	4s	+25%
`pack_sk_rho_key_tr_s2_t0`	✅	5s	4s	+25%
`poly_chknorm_native_aarch64`	✅	5s	4s	+25%
`poly_decompose_native`	✅	5s	4s	+25%
`poly_ntt_c`	✅	5s	2s	+150%
`poly_uniform_eta`	✅	5s	3s	+67%
`polyveck_unpack_eta`	✅	5s	2s	+150%
`polyvecl_ntt`	✅	5s	6s	-17%
`polyvecl_pointwise_acc_montgomery`	✅	5s	2s	+150%
`rej_eta_native`	✅	5s	3s	+67%
`sign`	✅	5s	7s	-29%
`sign_open`	✅	5s	2s	+150%
`sign_verify_extmu`	✅	5s	4s	+25%
`sk_s2hat_get_poly`	✅	5s	3s	+67%
`unpack_hints`	✅	5s	7s	-29%
`keccak_squeezeblocks_x4`	✅	4s	3s	+33%
`mld_polymat_expand_entry`	✅	4s	3s	+33%
`mld_value_barrier_u8`	✅	4s	1s	+300%
`poly_caddq`	✅	4s	4s	+0%
`poly_challenge`	✅	4s	5s	-20%
`poly_invntt_tomont_native`	✅	4s	3s	+33%
`poly_pointwise_montgomery_native`	✅	4s	3s	+33%
`poly_shiftl`	✅	4s	8s	-50%
`poly_uniform`	✅	4s	5s	-20%
`poly_uniform_4x`	✅	4s	3s	+33%
`poly_uniform_gamma1`	✅	4s	3s	+33%
`polyt1_pack`	✅	4s	4s	+0%
`polyveck_pack_eta`	✅	4s	4s	+0%
`polyveck_pack_t0`	✅	4s	4s	+0%
`polyveck_unpack_t0`	✅	4s	3s	+33%
`polyvecl_chknorm`	✅	4s	8s	-50%
`polyvecl_uniform_gamma1`	✅	4s	1s	+300%
`polyvecl_unpack_eta`	✅	4s	5s	-20%
`polyz_unpack_native`	✅	4s	4s	+0%
`reduce32`	✅	4s	1s	+300%
`rej_eta_c`	✅	4s	3s	+33%
`shake128_init`	✅	4s	3s	+33%
`shake256`	✅	4s	2s	+100%
`shake256_init`	✅	4s	1s	+300%
`sign_keypair`	✅	4s	5s	-20%
`sign_signature`	✅	4s	2s	+100%
`sign_signature_internal`	✅	4s	7s	-43%
`sign_verify`	✅	4s	5s	-20%
`sign_verify_pre_hash_internal`	✅	4s	3s	+33%
`sys_check_capability`	✅	4s	2s	+100%
`unpack_pk`	✅	4s	2s	+100%
`unpack_sig`	✅	4s	2s	+100%
`unpack_sk_t0hat`	✅	4s	2s	+100%
`yvec_init`	✅	4s	2s	+100%
`decompose`	✅	3s	3s	+0%
`intt_native_x86_64`	✅	3s	2s	+50%
`keccak_f1600_x1_native_aarch64`	✅	3s	3s	+0%
`keccak_f1600_x4_native_aarch64_v84a`	✅	3s	2s	+50%
`keccak_finalize`	✅	3s	3s	+0%
`keccakf1600_xor_bytes`	✅	3s	2s	+50%
`keccakf1600_xor_bytes (big endian)`	✅	3s	4s	-25%
`keccakf1600x4_permute`	✅	3s	4s	-25%
`mld_ct_abs_i32`	✅	3s	2s	+50%
`mld_ct_cmask_nonzero_u32`	✅	3s	2s	+50%
`mld_ct_get_optblocker_u8`	✅	3s	1s	+200%
`mld_ct_sel_int32`	✅	3s	2s	+50%
`mld_keccakf1600_extract_bytes`	✅	3s	2s	+50%
`mld_prepare_domain_separation_prefix`	✅	3s	5s	-40%
`mld_value_barrier_i64`	✅	3s	3s	+0%
`mld_value_barrier_u32`	✅	3s	1s	+200%
`montgomery_reduce`	✅	3s	3s	+0%
`nttunpack_native_x86_64`	✅	3s	2s	+50%
`pack_pk`	✅	3s	2s	+50%
`pack_sig_c`	✅	3s	3s	+0%
`pack_sig_h_poly`	✅	3s	4s	-25%
`pack_sig_z`	✅	3s	2s	+50%
`pointwise_native_x86_64`	✅	3s	2s	+50%
`poly_caddq_native`	✅	3s	3s	+0%
`poly_chknorm`	✅	3s	4s	-25%
`poly_chknorm_native`	✅	3s	3s	+0%
`poly_make_hint`	✅	3s	4s	-25%
`poly_ntt`	✅	3s	2s	+50%
`poly_pointwise_montgomery`	✅	3s	3s	+0%
`poly_use_hint`	✅	3s	2s	+50%
`polyt0_pack`	✅	3s	5s	-40%
`polyveck_pack_w1`	✅	3s	3s	+0%
`polyvecl_pack_eta`	✅	3s	2s	+50%
`polyz_unpack`	✅	3s	2s	+50%
`power2round`	✅	3s	4s	-25%
`shake128x4_absorb_once`	✅	3s	3s	+0%
`shake256_absorb`	✅	3s	3s	+0%
`shake256_finalize`	✅	3s	1s	+200%
`shake256_release`	✅	3s	2s	+50%
`shake256_squeeze`	✅	3s	1s	+200%
`sign_verify_pre_hash_shake256`	✅	3s	4s	-25%
`sk_s1hat_get_poly`	✅	3s	3s	+0%
`sk_t0hat_get_poly`	✅	3s	5s	-40%
`unpack_sk`	✅	3s	4s	-25%
`unpack_sk_s1hat`	✅	3s	4s	-25%
`use_hint`	✅	3s	3s	+0%
`caddq`	✅	2s	5s	-60%
`fqscale`	✅	2s	2s	+0%
`keccak_f1600_x1_native_aarch64_v84a`	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	2s	1s	+100%
`keccak_init`	✅	2s	2s	+0%
`keccak_squeeze`	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes`	✅	2s	1s	+100%
`keccakf1600x4_xor_bytes`	✅	2s	2s	+0%
`make_hint`	✅	2s	2s	+0%
`mld_ct_cmask_nonzero_u8`	✅	2s	2s	+0%
`mld_ct_get_optblocker_i64`	✅	2s	2s	+0%
`mld_ct_get_optblocker_u32`	✅	2s	3s	-33%
`mld_h`	✅	2s	5s	-60%
`ntt_native_x86_64`	✅	2s	4s	-50%
`pointwise_native_aarch64`	✅	2s	3s	-33%
`poly_caddq_native_aarch64`	✅	2s	3s	-33%
`poly_decompose`	✅	2s	4s	-50%
`poly_invntt_tomont`	✅	2s	3s	-33%
`poly_ntt_native`	✅	2s	4s	-50%
`poly_permute_bitrev_to_custom_optional_native`	✅	2s	4s	-50%
`poly_reduce`	✅	2s	3s	-33%
`poly_sub`	✅	2s	5s	-60%
`poly_use_hint_c`	✅	2s	1s	+100%
`poly_use_hint_native`	✅	2s	2s	+0%
`polyeta_pack`	✅	2s	2s	+0%
`polyt1_unpack`	✅	2s	3s	-33%
`polyvec_matrix_expand_serial`	✅	2s	5s	-60%
`polyvecl_pointwise_acc_montgomery_c`	✅	2s	2s	+0%
`polyvecl_uniform_gamma1_serial`	✅	2s	2s	+0%
`polyvecl_unpack_z`	✅	2s	3s	-33%
`polyw1_pack`	✅	2s	2s	+0%
`polyz_pack`	✅	2s	4s	-50%
`rej_eta`	✅	2s	2s	+0%
`shake128_absorb`	✅	2s	2s	+0%
`shake128_squeeze`	✅	2s	2s	+0%
`shake128x4_squeezeblocks`	✅	2s	3s	-33%
`shake256x4_absorb_once`	✅	2s	2s	+0%
`sign_signature_extmu`	✅	2s	4s	-50%
`unpack_sk_s2hat`	✅	2s	2s	+0%
`yvec_get_poly`	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	1s	3s	-67%
`keccakf1600_extract_bytes (big endian)`	✅	1s	2s	-50%
`mld_ct_cmask_neg_i32`	✅	1s	3s	-67%
`poly_permute_bitrev_to_custom_optional`	✅	1s	4s	-75%
`poly_uniform_gamma1_4x`	✅	1s	3s	-67%
`shake128_finalize`	✅	1s	1s	+0%
`shake128_release`	✅	1s	4s	-75%
`shake256x4_squeezeblocks`	✅	1s	5s	-80%

Rework mld_poly_pointwise_montgomery from (c, a, b) to in-place (a, b) where a := a * b * R^{-1} mod q. The change propagates through the C wrapper, the native dispatcher, the Arm aarch64 and x86_64 AVX2 assembly, all call sites, the test harness, and the allocation constants. This allows eliminating one temporary polynomial in the the REDUCE_RAM definition in polymat, and it will also enable further memory optimizations in follow-up PRs. CBMC harnesses are adjusted. HOL Light proofs are updated. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

hanno-becker

In sign.c it seems that perhaps further memory optimizations can be unlocked -- I didn't check in detail -- but this may be what you're alluding to in the PR description?

Otherwise, this looks clean to me. Sweet that the proofs just continue working.

mkannwischer · 2026-04-29T12:25:07Z

In sign.c it seems that perhaps further memory optimizations can be unlocked -- I didn't check in detail -- but this may be what you're alluding to in the PR description?

Otherwise, this looks clean to me. Sweet that the proofs just continue working.

Yes, one of the optimizations will be done for verification in #1007.

mkannwischer added the low-ram label Apr 28, 2026

mkannwischer force-pushed the destructive-poly-pointwise-montgomery branch from 923c839 to 554f977 Compare April 28, 2026 13:08

mkannwischer force-pushed the destructive-poly-pointwise-montgomery branch 3 times, most recently from 04147e7 to 39ec8f4 Compare April 29, 2026 05:27

This was referenced Apr 29, 2026

Make poly_use_hint destructive #1070

Merged

Lowram: Share buffers with non-overlapping lifetimes in verify #1007

Merged

mkannwischer force-pushed the destructive-poly-pointwise-montgomery branch 2 times, most recently from a7eb2f7 to 6bbf9d1 Compare April 29, 2026 08:23

mkannwischer marked this pull request as ready for review April 29, 2026 08:49

mkannwischer requested a review from a team as a code owner April 29, 2026 08:49

mkannwischer force-pushed the destructive-poly-pointwise-montgomery branch from 87b9244 to b70053d Compare April 29, 2026 10:11

hanno-becker approved these changes Apr 29, 2026

View reviewed changes

mkannwischer merged commit 208ebe7 into main Apr 29, 2026
437 checks passed

mkannwischer deleted the destructive-poly-pointwise-montgomery branch April 29, 2026 13:57

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Make poly_pointwise_montgomery destructive#1067

Make poly_pointwise_montgomery destructive#1067
mkannwischer merged 1 commit intomainfrom
destructive-poly-pointwise-montgomery

mkannwischer commented Apr 28, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Apr 28, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Apr 28, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Apr 28, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Apr 28, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Apr 28, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Apr 28, 2026 •

edited

Loading

Uh oh!

hanno-becker left a comment

Uh oh!

mkannwischer commented Apr 29, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

mkannwischer commented Apr 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

oqs-bot commented Apr 28, 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 Apr 28, 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 Apr 28, 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 Apr 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-DSA-87)

Uh oh!

oqs-bot commented Apr 28, 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 Apr 28, 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!

hanno-becker left a comment

Choose a reason for hiding this comment

Uh oh!

mkannwischer commented Apr 29, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

mkannwischer commented Apr 28, 2026 •

edited

Loading

oqs-bot commented Apr 28, 2026 •

edited

Loading

oqs-bot commented Apr 28, 2026 •

edited

Loading

oqs-bot commented Apr 28, 2026 •

edited

Loading

oqs-bot commented Apr 28, 2026 •

edited

Loading

oqs-bot commented Apr 28, 2026 •

edited

Loading

oqs-bot commented Apr 28, 2026 •

edited

Loading