Add signing hooks for observing signature attempts and implementing restartable signing by hanno-becker · Pull Request #1237 · pq-code-package/mldsa-native

hanno-becker · 2026-06-28T13:39:21Z

Based on common: Split context-parameter machinery into context.h #1238

sign: Add configurable signing hooks (resume/attempt/finish)

The runtime of ML-DSA signatures is theoretically unbounded. Even the
bound of max 814 signature attempts -- approved by NIST as lowering the
chance of signing failure below 2^{-256} -- leaves a performance
distribution whose peak percentiles can be unacceptable for constrained
systems with strict timing requirements.

The library already provides MLD_CONFIG_MAX_SIGNING_ATTEMPTS to cap the
number of signing attempts. However, FIPS 204 forbids lowering that bound
below 814, rendering the option non-compliant in constrained environments.

As a remedy, this commit introduces three optional 'signing hooks' around
the core rejection-sampling loop, keyed by the attempt counter (the loop
iteration; the spec counter is kappa = attempt*MLDSA_L):

- `attempt = sign_resume()`: Return the attempt to resume the operation
  from. `0` for an initial / non-restartable signing operation.
- `sign_attempt(attempt)`: Called before each attempt. Returns 0 to
  proceed, or non-zero to pause: signing then returns MLD_ERR_SIGNING_PAUSED
  with `attempt` as the resume point.
- `sign_finish(attempt)`: Called on success with the succeeding attempt.

Together, resume + attempt make signing _restartable_: a caller can pause
after a bounded number of attempts and later resume from the recorded
attempt, bounding per-call runtime while keeping a FIPS-compliant overall
bound and reproducing the same signature as an uninterrupted run.

This only works if the consumer drives the deterministic internal API: the
randomized API would choose a fresh seed on each (re-)start, so the resume
hook requires MLD_CONFIG_NO_RANDOMIZED_API and is incompatible with
MLD_CONFIG_KEYGEN_PCT (whose one-shot internal signature cannot be resumed).
The attempt and finish hooks also serve standalone uses with any API, e.g.
logging or benchmarking the per-signature attempt distribution.

Pausing is independent of MLD_CONFIG_MAX_SIGNING_ATTEMPTS, the upper bound on
the total number of attempts (>= 814 for FIPS 204 compliance) after which
signing gives up with the distinct error MLD_ERR_SIGN_ATTEMPTS_EXHAUSTED; it
must not be lowered as a restart mechanism.

sign_{resume|attempt|finish} can be implemented on mutable globals or on a
context, so they are introduced under the existing MLD_CONFIG_CONTEXT_PARAMETER
wrapper, which lets functions be called with or without an
application-specific context pointer.

Concretely, this commit:

- Adds independent MLD_CONFIG_SIGN_HOOK_{RESUME,ATTEMPT,FINISH} options. When
  set, the integration provides, respectively:

  - `attempt = mld_sign_hook_resume([ctx])`: provide initial/resume attempt
  - `mld_sign_hook_attempt(attempt [, ctx])`: per-attempt hook; pause via
    non-zero return
  - `mld_sign_hook_finish(attempt [, ctx])`: note the succeeding attempt

  The unset dummies leave the default build (and its proofs) unchanged.

- Adds the MLD_ERR_SIGNING_PAUSED error code returned when the attempt hook
  pauses signing.

- Adds CBMC proofs for the three hooks and threads them through the existing
  signing proofs.

- Adds test/src/test_sign_hook.c (a new `sign_hook` test), which checks that
  restartable signing -- single-step and with random attempts-per-call --
  reproduces one-shot signing exactly, and gathers an attempts-per-signature
  distribution that it checks against the expected geometric mean per
  parameter set.

oqs-bot · 2026-06-28T21:26:47Z

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

Full Results (209 proofs)

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

oqs-bot · 2026-06-28T21:29:22Z

CBMC Results (ML-DSA-65)

Full Results (209 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	1815s	1784s	+1.7%
`polyvecl_pointwise_acc_montgomery_c`	✅	208s	210s	-1%
`sign_verify_internal`	✅	168s	177s	-5%
`poly_pointwise_montgomery_c`	✅	126s	125s	+1%
`polyvec_matrix_expand`	✅	108s	110s	-2%
`mld_invntt_layer`	✅	103s	109s	-6%
`mld_attempt_signature_generation`	✅	63s	63s	+0%
`sign_signature_internal`	✅	61s	55s	+11%
`mld_ntt_layer`	✅	45s	41s	+10%
`fqmul`	✅	42s	40s	+5%
`polyvec_matrix_expand_serial`	✅	29s	27s	+7%
`keccakf1600x4_permute_native`	✅	24s	23s	+4%
`mld_ntt_butterfly_block`	✅	23s	24s	-4%
`polyvec_matrix_pointwise_montgomery_yvec`	✅	20s	18s	+11%
`poly_ntt_c`	✅	19s	19s	+0%
`compute_pack_t0_t1`	✅	17s	13s	+31%
`poly_chknorm_c`	✅	15s	15s	+0%
`polyt0_unpack`	✅	15s	16s	-6%
`mld_check_pct`	✅	14s	14s	+0%
`poly_uniform_eta_4x`	✅	14s	14s	+0%
`polyveck_decompose`	✅	14s	12s	+17%
`rej_uniform`	✅	14s	18s	-22%
`rej_uniform_c`	✅	14s	14s	+0%
`poly_uniform_4x`	✅	13s	13s	+0%
`poly_invntt_tomont_c`	✅	11s	11s	+0%
`polyz_unpack_c`	✅	11s	13s	-15%
`keccak_absorb_once_x4`	✅	9s	8s	+12%
`mld_keccakf1600_permute_c`	✅	8s	6s	+33%
`pointwise_acc_native_aarch64`	✅	8s	6s	+33%
`polyveck_ntt`	✅	8s	7s	+14%
`rej_uniform_native_x86_64`	✅	8s	-	new
`mld_compute_pack_z`	✅	7s	7s	+0%
`poly_add`	✅	7s	9s	-22%
`poly_decompose_c`	✅	7s	5s	+40%
`polyveck_caddq`	✅	7s	6s	+17%
`polyveck_invntt_tomont`	✅	7s	8s	-12%
`rej_uniform_native`	✅	7s	4s	+75%
`sign_pk_from_sk`	✅	7s	6s	+17%
`poly_invntt_tomont_native`	✅	6s	2s	+200%
`shake256_release`	✅	6s	2s	+200%
`sign_signature`	✅	6s	6s	+0%
`sign_signature_pre_hash_internal`	✅	6s	3s	+100%
`keccak_absorb`	✅	5s	3s	+67%
`mld_h`	✅	5s	2s	+150%
`mld_polymat_expand_entry`	✅	5s	4s	+25%
`mld_value_barrier_i64`	✅	5s	2s	+150%
`pointwise_acc_native_x86_64`	✅	5s	8s	-38%
`poly_decompose_32_native_aarch64`	✅	5s	3s	+67%
`poly_invntt_tomont`	✅	5s	3s	+67%
`poly_ntt`	✅	5s	2s	+150%
`poly_power2round`	✅	5s	4s	+25%
`poly_uniform_gamma1`	✅	5s	3s	+67%
`poly_use_hint_c`	✅	5s	5s	+0%
`polyeta_unpack`	✅	5s	8s	-38%
`polyz_unpack_native`	✅	5s	4s	+25%
`rej_uniform_native_aarch64`	✅	5s	3s	+67%
`sign_keypair`	✅	5s	3s	+67%
`sign_signature_pre_hash_shake256`	✅	5s	3s	+67%
`sign_verify_extmu`	✅	5s	3s	+67%
`sign_verify_pre_hash_internal`	✅	5s	5s	+0%
`sign_verify_pre_hash_shake256`	✅	5s	5s	+0%
`sk_s1hat_get_poly`	✅	5s	6s	-17%
`yvec_init`	✅	5s	3s	+67%
`caddq`	✅	4s	3s	+33%
`intt_native_x86_64`	✅	4s	3s	+33%
`keccak_squeezeblocks_x4`	✅	4s	5s	-20%
`keccakf1600_extract_bytes (big endian)`	✅	4s	2s	+100%
`keccakf1600_permute_native`	✅	4s	3s	+33%
`keccakf1600x4_xor_bytes_native`	✅	4s	3s	+33%
`mld_sample_s1_s2`	✅	4s	6s	-33%
`mld_sign_attempt`	✅	4s	-	new
`mld_sign_resume`	✅	4s	-	new
`ntt_native_x86_64`	✅	4s	2s	+100%
`poly_caddq_native_x86_64`	✅	4s	3s	+33%
`poly_challenge`	✅	4s	6s	-33%
`poly_chknorm_native_x86_64`	✅	4s	3s	+33%
`poly_decompose`	✅	4s	2s	+100%
`poly_pointwise_montgomery_native`	✅	4s	3s	+33%
`poly_shiftl`	✅	4s	3s	+33%
`poly_uniform`	✅	4s	4s	+0%
`poly_use_hint_native`	✅	4s	2s	+100%
`polyeta_pack`	✅	4s	3s	+33%
`polyt1_unpack`	✅	4s	5s	-20%
`polyveck_chknorm`	✅	4s	6s	-33%
`polyveck_pack_w1`	✅	4s	3s	+33%
`polyveck_unpack_eta`	✅	4s	6s	-33%
`polyvecl_chknorm`	✅	4s	7s	-43%
`polyvecl_ntt`	✅	4s	4s	+0%
`polyvecl_pointwise_acc_montgomery_native`	✅	4s	2s	+100%
`polyvecl_uniform_gamma1`	✅	4s	2s	+100%
`polyvecl_uniform_gamma1_serial`	✅	4s	3s	+33%
`rej_eta`	✅	4s	2s	+100%
`shake128_squeeze`	✅	4s	2s	+100%
`shake128x4_absorb_once`	✅	4s	3s	+33%
`unpack_pk_t1`	✅	4s	5s	-20%
`unpack_sk_s1hat`	✅	4s	2s	+100%
`unpack_sk_t0hat`	✅	4s	5s	-20%
`decompose`	✅	3s	1s	+200%
`fqscale`	✅	3s	3s	+0%
`keccak_f1600_x1_native_aarch64`	✅	3s	2s	+50%
`keccak_f1600_x1_native_aarch64_v84a`	✅	3s	3s	+0%
`keccak_f1600_x4_native_aarch64_v84a`	✅	3s	4s	-25%
`keccak_squeeze`	✅	3s	4s	-25%
`keccakf1600_xor_bytes`	✅	3s	2s	+50%
`keccakf1600x4_extract_bytes_native`	✅	3s	4s	-25%
`keccakf1600x4_permute`	✅	3s	4s	-25%
`make_hint`	✅	3s	2s	+50%
`mld_ct_cmask_nonzero_u32`	✅	3s	4s	-25%
`mld_ct_cmask_nonzero_u8`	✅	3s	3s	+0%
`mld_ct_get_optblocker_i64`	✅	3s	2s	+50%
`mld_ct_get_optblocker_u8`	✅	3s	2s	+50%
`mld_ct_memcmp`	✅	3s	2s	+50%
`mld_ct_sel_int32`	✅	3s	3s	+0%
`mld_keccakf1600x4_extract_bytes_c`	✅	3s	3s	+0%
`mld_prepare_domain_separation_prefix`	✅	3s	2s	+50%
`mld_sample_s1_s2_serial`	✅	3s	4s	-25%
`montgomery_reduce`	✅	3s	4s	-25%
`ntt_native_aarch64`	✅	3s	2s	+50%
`pack_sig_c`	✅	3s	5s	-40%
`pack_sig_h`	✅	3s	5s	-40%
`pack_sig_z`	✅	3s	2s	+50%
`pack_sk_s1`	✅	3s	5s	-40%
`poly_caddq_native`	✅	3s	2s	+50%
`poly_caddq_native_aarch64`	✅	3s	2s	+50%
`poly_chknorm_native_aarch64`	✅	3s	3s	+0%
`poly_decompose_88_native_aarch64`	✅	3s	1s	+200%
`poly_decompose_native_x86_64`	✅	3s	3s	+0%
`poly_reduce`	✅	3s	3s	+0%
`poly_sub`	✅	3s	3s	+0%
`poly_uniform_eta`	✅	3s	4s	-25%
`polyt1_pack`	✅	3s	3s	+0%
`polyveck_reduce`	✅	3s	4s	-25%
`polyvecl_unpack_eta`	✅	3s	3s	+0%
`polyvecl_unpack_z`	✅	3s	3s	+0%
`polyw1_pack`	✅	3s	4s	-25%
`polyw1_pack_88`	✅	3s	2s	+50%
`polyz_unpack`	✅	3s	3s	+0%
`rej_eta_c`	✅	3s	5s	-40%
`rej_eta_native`	✅	3s	3s	+0%
`rej_uniform_eta_native_aarch64`	✅	3s	4s	-25%
`shake128_init`	✅	3s	2s	+50%
`shake128_release`	✅	3s	3s	+0%
`shake256_absorb`	✅	3s	2s	+50%
`shake256x4_absorb_once`	✅	3s	3s	+0%
`sig_unpack_hints`	✅	3s	2s	+50%
`sign_keypair_internal`	✅	3s	5s	-40%
`sign_verify`	✅	3s	3s	+0%
`sk_s2hat_get_poly`	✅	3s	2s	+50%
`unpack_sk_s2hat`	✅	3s	4s	-25%
`yvec_get_poly`	✅	3s	3s	+0%
`intt_native_aarch64`	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	2s	2s	+0%
`keccak_f1600_x4_native_avx2`	✅	2s	2s	+0%
`keccakf1600_permute`	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes`	✅	2s	4s	-50%
`mld_ct_abs_i32`	✅	2s	2s	+0%
`mld_ct_cmask_neg_i32`	✅	2s	2s	+0%
`mld_ct_get_optblocker_u32`	✅	2s	3s	-33%
`mld_keccakf1600_extract_bytes`	✅	2s	1s	+100%
`mld_keccakf1600x4_xor_bytes_c`	✅	2s	2s	+0%
`mld_sign_finish`	✅	2s	-	new
`mld_value_barrier_u8`	✅	2s	3s	-33%
`nttunpack_native_x86_64`	✅	2s	3s	-33%
`pack_sk_rho_key_tr_s2`	✅	2s	2s	+0%
`pointwise_native_aarch64`	✅	2s	5s	-60%
`pointwise_native_x86_64`	✅	2s	3s	-33%
`poly_caddq`	✅	2s	2s	+0%
`poly_caddq_c`	✅	2s	2s	+0%
`poly_chknorm`	✅	2s	4s	-50%
`poly_chknorm_native`	✅	2s	2s	+0%
`poly_ntt_native`	✅	2s	4s	-50%
`poly_permute_bitrev_to_custom_optional`	✅	2s	2s	+0%
`poly_permute_bitrev_to_custom_optional_native`	✅	2s	4s	-50%
`poly_uniform_gamma1_4x`	✅	2s	4s	-50%
`poly_use_hint`	✅	2s	3s	-33%
`poly_use_hint_native_aarch64`	✅	2s	3s	-33%
`poly_use_hint_native_x86_64`	✅	2s	-	new
`polyvec_matrix_pointwise_montgomery_row`	✅	2s	1s	+100%
`polyveck_pack_eta`	✅	2s	4s	-50%
`polyvecl_pack_eta`	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery`	✅	2s	3s	-33%
`polyz_pack`	✅	2s	3s	-33%
`polyz_unpack_17_native_aarch64`	✅	2s	3s	-33%
`polyz_unpack_19_native_aarch64`	✅	2s	3s	-33%
`polyz_unpack_native_x86_64`	✅	2s	3s	-33%
`power2round`	✅	2s	1s	+100%
`reduce32`	✅	2s	3s	-33%
`shake128_absorb`	✅	2s	2s	+0%
`shake128_finalize`	✅	2s	1s	+100%
`shake128x4_squeezeblocks`	✅	2s	3s	-33%
`shake256`	✅	2s	2s	+0%
`shake256_finalize`	✅	2s	1s	+100%
`shake256_squeeze`	✅	2s	3s	-33%
`shake256x4_squeezeblocks`	✅	2s	2s	+0%
`sign_signature_extmu`	✅	2s	2s	+0%
`sk_t0hat_get_poly`	✅	2s	2s	+0%
`sys_check_capability`	✅	2s	4s	-50%
`unpack_sk`	✅	2s	3s	-33%
`use_hint`	✅	2s	2s	+0%
`keccak_finalize`	✅	1s	2s	-50%
`keccak_init`	✅	1s	1s	+0%
`keccakf1600_xor_bytes (big endian)`	✅	1s	2s	-50%
`keccakf1600x4_xor_bytes`	✅	1s	1s	+0%
`mld_value_barrier_u32`	✅	1s	3s	-67%
`poly_decompose_native`	✅	1s	3s	-67%
`poly_pointwise_montgomery`	✅	1s	3s	-67%
`polyt0_pack`	✅	1s	3s	-67%
`polyw1_pack_32`	✅	1s	4s	-75%
`shake256_init`	✅	1s	2s	-50%

oqs-bot · 2026-06-28T21:30:52Z

CBMC Results (ML-DSA-44)

Full Results (209 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	1625s	1514s	+7.3%
`polyvecl_pointwise_acc_montgomery_c`	✅	152s	131s	+16%
`poly_pointwise_montgomery_c`	✅	128s	114s	+12%
`sign_verify_internal`	✅	124s	114s	+9%
`mld_invntt_layer`	✅	114s	107s	+7%
`mld_attempt_signature_generation`	✅	60s	58s	+3%
`compute_pack_t0_t1`	✅	51s	50s	+2%
`mld_ntt_layer`	✅	45s	42s	+7%
`fqmul`	✅	40s	39s	+3%
`polyvec_matrix_expand`	✅	28s	28s	+0%
`sign_signature_internal`	✅	27s	26s	+4%
`keccakf1600x4_permute_native`	✅	23s	22s	+5%
`mld_ntt_butterfly_block`	✅	21s	23s	-9%
`poly_ntt_c`	✅	19s	19s	+0%
`polyvec_matrix_pointwise_montgomery_yvec`	✅	17s	15s	+13%
`polyeta_unpack`	✅	16s	14s	+14%
`polyt0_unpack`	✅	16s	15s	+7%
`rej_uniform`	✅	16s	18s	-11%
`rej_uniform_c`	✅	16s	15s	+7%
`poly_chknorm_c`	✅	15s	17s	-12%
`poly_invntt_tomont_c`	✅	15s	11s	+36%
`poly_uniform_4x`	✅	13s	14s	-7%
`mld_check_pct`	✅	12s	14s	-14%
`poly_uniform_eta_4x`	✅	12s	11s	+9%
`polyvecl_chknorm`	✅	10s	10s	+0%
`polyz_unpack_c`	✅	10s	11s	-9%
`rej_uniform_native_x86_64`	✅	10s	-	new
`polyvec_matrix_expand_serial`	✅	9s	8s	+12%
`keccak_absorb_once_x4`	✅	8s	9s	-11%
`mld_compute_pack_z`	✅	8s	7s	+14%
`pointwise_acc_native_x86_64`	✅	8s	7s	+14%
`poly_decompose_32_native_aarch64`	✅	8s	2s	+300%
`poly_add`	✅	7s	7s	+0%
`mld_keccakf1600_permute_c`	✅	6s	8s	-25%
`mld_prepare_domain_separation_prefix`	✅	6s	4s	+50%
`poly_chknorm_native`	✅	6s	4s	+50%
`poly_decompose_native_x86_64`	✅	6s	3s	+100%
`poly_power2round`	✅	6s	4s	+50%
`poly_uniform`	✅	6s	6s	+0%
`polyt1_unpack`	✅	6s	5s	+20%
`polyveck_chknorm`	✅	6s	5s	+20%
`power2round`	✅	6s	3s	+100%
`rej_uniform_native`	✅	6s	4s	+50%
`keccak_squeeze`	✅	5s	1s	+400%
`mld_h`	✅	5s	4s	+25%
`mld_polymat_expand_entry`	✅	5s	3s	+67%
`poly_caddq_native_aarch64`	✅	5s	4s	+25%
`poly_challenge`	✅	5s	3s	+67%
`poly_decompose_c`	✅	5s	4s	+25%
`poly_uniform_eta`	✅	5s	5s	+0%
`polyveck_invntt_tomont`	✅	5s	5s	+0%
`polyvecl_ntt`	✅	5s	2s	+150%
`polyw1_pack`	✅	5s	3s	+67%
`polyw1_pack_32`	✅	5s	2s	+150%
`polyz_pack`	✅	5s	2s	+150%
`polyz_unpack_17_native_aarch64`	✅	5s	5s	+0%
`polyz_unpack_native_x86_64`	✅	5s	3s	+67%
`sign_keypair`	✅	5s	4s	+25%
`sign_signature_pre_hash_shake256`	✅	5s	3s	+67%
`sign_verify`	✅	5s	4s	+25%
`sign_verify_pre_hash_shake256`	✅	5s	5s	+0%
`sk_s1hat_get_poly`	✅	5s	3s	+67%
`caddq`	✅	4s	2s	+100%
`intt_native_x86_64`	✅	4s	4s	+0%
`keccak_f1600_x1_native_aarch64_v84a`	✅	4s	3s	+33%
`keccakf1600_extract_bytes (big endian)`	✅	4s	2s	+100%
`keccakf1600x4_xor_bytes`	✅	4s	2s	+100%
`mld_ct_cmask_neg_i32`	✅	4s	3s	+33%
`mld_ct_get_optblocker_u8`	✅	4s	1s	+300%
`mld_ct_memcmp`	✅	4s	3s	+33%
`mld_sample_s1_s2`	✅	4s	4s	+0%
`mld_sign_resume`	✅	4s	-	new
`pack_sig_c`	✅	4s	2s	+100%
`pack_sk_rho_key_tr_s2`	✅	4s	3s	+33%
`pointwise_acc_native_aarch64`	✅	4s	4s	+0%
`pointwise_native_x86_64`	✅	4s	4s	+0%
`poly_caddq_c`	✅	4s	2s	+100%
`poly_chknorm_native_aarch64`	✅	4s	4s	+0%
`poly_decompose_native`	✅	4s	3s	+33%
`poly_ntt`	✅	4s	3s	+33%
`poly_reduce`	✅	4s	3s	+33%
`poly_use_hint_c`	✅	4s	3s	+33%
`polyt0_pack`	✅	4s	2s	+100%
`polyveck_caddq`	✅	4s	3s	+33%
`polyveck_decompose`	✅	4s	4s	+0%
`polyveck_ntt`	✅	4s	5s	-20%
`polyveck_reduce`	✅	4s	5s	-20%
`polyveck_unpack_eta`	✅	4s	2s	+100%
`polyvecl_pointwise_acc_montgomery_native`	✅	4s	2s	+100%
`reduce32`	✅	4s	2s	+100%
`rej_uniform_eta_native_aarch64`	✅	4s	2s	+100%
`rej_uniform_native_aarch64`	✅	4s	5s	-20%
`sig_unpack_hints`	✅	4s	2s	+100%
`sign_pk_from_sk`	✅	4s	5s	-20%
`sign_verify_pre_hash_internal`	✅	4s	3s	+33%
`unpack_sk_s1hat`	✅	4s	1s	+300%
`unpack_sk_t0hat`	✅	4s	3s	+33%
`decompose`	✅	3s	2s	+50%
`intt_native_aarch64`	✅	3s	9s	-67%
`keccak_absorb`	✅	3s	5s	-40%
`keccak_f1600_x4_native_aarch64_v84a`	✅	3s	2s	+50%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	3s	1s	+200%
`keccak_squeezeblocks_x4`	✅	3s	4s	-25%
`keccakf1600_permute_native`	✅	3s	3s	+0%
`keccakf1600x4_extract_bytes_native`	✅	3s	3s	+0%
`keccakf1600x4_permute`	✅	3s	4s	-25%
`make_hint`	✅	3s	3s	+0%
`mld_ct_cmask_nonzero_u32`	✅	3s	2s	+50%
`mld_ct_get_optblocker_i64`	✅	3s	4s	-25%
`mld_keccakf1600x4_xor_bytes_c`	✅	3s	2s	+50%
`mld_sample_s1_s2_serial`	✅	3s	3s	+0%
`mld_sign_finish`	✅	3s	-	new
`mld_value_barrier_i64`	✅	3s	2s	+50%
`montgomery_reduce`	✅	3s	3s	+0%
`ntt_native_x86_64`	✅	3s	3s	+0%
`pack_sk_s1`	✅	3s	2s	+50%
`poly_caddq_native`	✅	3s	5s	-40%
`poly_caddq_native_x86_64`	✅	3s	4s	-25%
`poly_decompose`	✅	3s	3s	+0%
`poly_decompose_88_native_aarch64`	✅	3s	4s	-25%
`poly_invntt_tomont`	✅	3s	4s	-25%
`poly_invntt_tomont_native`	✅	3s	4s	-25%
`poly_permute_bitrev_to_custom_optional_native`	✅	3s	4s	-25%
`poly_pointwise_montgomery`	✅	3s	3s	+0%
`poly_shiftl`	✅	3s	3s	+0%
`poly_sub`	✅	3s	3s	+0%
`poly_uniform_gamma1_4x`	✅	3s	5s	-40%
`poly_use_hint_native`	✅	3s	4s	-25%
`poly_use_hint_native_aarch64`	✅	3s	2s	+50%
`poly_use_hint_native_x86_64`	✅	3s	-	new
`polyeta_pack`	✅	3s	3s	+0%
`polyvec_matrix_pointwise_montgomery_row`	✅	3s	2s	+50%
`polyveck_pack_eta`	✅	3s	2s	+50%
`polyvecl_pack_eta`	✅	3s	3s	+0%
`polyvecl_unpack_z`	✅	3s	2s	+50%
`polyw1_pack_88`	✅	3s	1s	+200%
`rej_eta`	✅	3s	3s	+0%
`rej_eta_c`	✅	3s	4s	-25%
`rej_eta_native`	✅	3s	6s	-50%
`shake256`	✅	3s	1s	+200%
`shake256_release`	✅	3s	2s	+50%
`shake256x4_absorb_once`	✅	3s	3s	+0%
`shake256x4_squeezeblocks`	✅	3s	4s	-25%
`sign_keypair_internal`	✅	3s	4s	-25%
`sign_signature`	✅	3s	3s	+0%
`sign_signature_extmu`	✅	3s	4s	-25%
`sk_s2hat_get_poly`	✅	3s	2s	+50%
`unpack_pk_t1`	✅	3s	5s	-40%
`unpack_sk`	✅	3s	3s	+0%
`yvec_get_poly`	✅	3s	3s	+0%
`fqscale`	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64`	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	2s	3s	-33%
`keccak_f1600_x4_native_avx2`	✅	2s	3s	-33%
`keccak_finalize`	✅	2s	3s	-33%
`keccakf1600_permute`	✅	2s	2s	+0%
`keccakf1600_xor_bytes`	✅	2s	1s	+100%
`keccakf1600_xor_bytes (big endian)`	✅	2s	4s	-50%
`keccakf1600x4_extract_bytes`	✅	2s	2s	+0%
`keccakf1600x4_xor_bytes_native`	✅	2s	3s	-33%
`mld_ct_cmask_nonzero_u8`	✅	2s	2s	+0%
`mld_keccakf1600x4_extract_bytes_c`	✅	2s	2s	+0%
`mld_sign_attempt`	✅	2s	-	new
`mld_value_barrier_u8`	✅	2s	3s	-33%
`ntt_native_aarch64`	✅	2s	3s	-33%
`nttunpack_native_x86_64`	✅	2s	1s	+100%
`pack_sig_h`	✅	2s	3s	-33%
`pack_sig_z`	✅	2s	4s	-50%
`pointwise_native_aarch64`	✅	2s	5s	-60%
`poly_caddq`	✅	2s	2s	+0%
`poly_chknorm`	✅	2s	4s	-50%
`poly_chknorm_native_x86_64`	✅	2s	2s	+0%
`poly_ntt_native`	✅	2s	5s	-60%
`poly_permute_bitrev_to_custom_optional`	✅	2s	2s	+0%
`poly_pointwise_montgomery_native`	✅	2s	2s	+0%
`poly_uniform_gamma1`	✅	2s	4s	-50%
`poly_use_hint`	✅	2s	4s	-50%
`polyt1_pack`	✅	2s	4s	-50%
`polyveck_pack_w1`	✅	2s	1s	+100%
`polyvecl_pointwise_acc_montgomery`	✅	2s	4s	-50%
`polyvecl_uniform_gamma1`	✅	2s	3s	-33%
`polyvecl_uniform_gamma1_serial`	✅	2s	2s	+0%
`polyvecl_unpack_eta`	✅	2s	2s	+0%
`polyz_unpack`	✅	2s	3s	-33%
`polyz_unpack_19_native_aarch64`	✅	2s	5s	-60%
`polyz_unpack_native`	✅	2s	2s	+0%
`shake128_absorb`	✅	2s	2s	+0%
`shake128_finalize`	✅	2s	2s	+0%
`shake128_init`	✅	2s	3s	-33%
`shake128_release`	✅	2s	1s	+100%
`shake128_squeeze`	✅	2s	1s	+100%
`shake128x4_absorb_once`	✅	2s	3s	-33%
`shake256_absorb`	✅	2s	3s	-33%
`shake256_finalize`	✅	2s	2s	+0%
`shake256_init`	✅	2s	3s	-33%
`shake256_squeeze`	✅	2s	2s	+0%
`sign_signature_pre_hash_internal`	✅	2s	6s	-67%
`sign_verify_extmu`	✅	2s	3s	-33%
`sk_t0hat_get_poly`	✅	2s	2s	+0%
`sys_check_capability`	✅	2s	4s	-50%
`unpack_sk_s2hat`	✅	2s	4s	-50%
`use_hint`	✅	2s	2s	+0%
`yvec_init`	✅	2s	3s	-33%
`keccak_init`	✅	1s	3s	-67%
`mld_ct_abs_i32`	✅	1s	2s	-50%
`mld_ct_get_optblocker_u32`	✅	1s	1s	+0%
`mld_ct_sel_int32`	✅	1s	2s	-50%
`mld_keccakf1600_extract_bytes`	✅	1s	2s	-50%
`mld_value_barrier_u32`	✅	1s	2s	-50%
`shake128x4_squeezeblocks`	✅	1s	1s	+0%

oqs-bot · 2026-06-28T21:34:58Z

CBMC Results (ML-DSA-87)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`sign_signature_internal`	⚠️	113s	42s	+169%

Full Results (209 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	2187s	2151s	+1.7%
`polyvecl_pointwise_acc_montgomery_c`	✅	357s	353s	+1%
`polyvec_matrix_expand`	✅	311s	324s	-4%
`poly_pointwise_montgomery_c`	✅	129s	144s	-10%
`mld_invntt_layer`	✅	117s	115s	+2%
`sign_signature_internal`	⚠️	113s	42s	+169%
`sign_verify_internal`	✅	98s	97s	+1%
`mld_attempt_signature_generation`	✅	55s	55s	+0%
`mld_ntt_layer`	✅	44s	45s	-2%
`fqmul`	✅	42s	43s	-2%
`polyvec_matrix_expand_serial`	✅	37s	38s	-3%
`mld_ntt_butterfly_block`	✅	23s	24s	-4%
`keccakf1600x4_permute_native`	✅	22s	23s	-4%
`poly_ntt_c`	✅	21s	21s	+0%
`compute_pack_t0_t1`	✅	20s	19s	+5%
`polyvec_matrix_pointwise_montgomery_yvec`	✅	18s	18s	+0%
`poly_chknorm_c`	✅	17s	15s	+13%
`polyeta_unpack`	✅	17s	17s	+0%
`polyt0_unpack`	✅	16s	14s	+14%
`mld_check_pct`	✅	15s	16s	-6%
`rej_uniform`	✅	15s	15s	+0%
`poly_uniform_4x`	✅	13s	13s	+0%
`poly_uniform_eta_4x`	✅	13s	11s	+18%
`rej_uniform_c`	✅	13s	19s	-32%
`mld_compute_pack_z`	✅	12s	8s	+50%
`keccak_absorb_once_x4`	✅	11s	9s	+22%
`poly_invntt_tomont_c`	✅	11s	12s	-8%
`polyveck_caddq`	✅	11s	8s	+38%
`polyveck_ntt`	✅	10s	11s	-9%
`rej_uniform_native_x86_64`	✅	10s	-	new
`pointwise_acc_native_x86_64`	✅	9s	6s	+50%
`polyveck_decompose`	✅	9s	13s	-31%
`mld_keccakf1600_permute_c`	✅	8s	7s	+14%
`pointwise_acc_native_aarch64`	✅	8s	6s	+33%
`polyvecl_ntt`	✅	8s	7s	+14%
`poly_challenge`	✅	7s	5s	+40%
`sign_verify_pre_hash_internal`	✅	7s	3s	+133%
`mld_sample_s1_s2`	✅	6s	6s	+0%
`pointwise_native_x86_64`	✅	6s	2s	+200%
`poly_chknorm`	✅	6s	3s	+100%
`poly_pointwise_montgomery`	✅	6s	4s	+50%
`polyveck_invntt_tomont`	✅	6s	9s	-33%
`polyvecl_chknorm`	✅	6s	7s	-14%
`rej_uniform_native`	✅	6s	8s	-25%
`sign_signature_pre_hash_internal`	✅	6s	5s	+20%
`mld_sample_s1_s2_serial`	✅	5s	8s	-38%
`mld_sign_attempt`	✅	5s	-	new
`poly_add`	✅	5s	6s	-17%
`poly_ntt`	✅	5s	3s	+67%
`poly_permute_bitrev_to_custom_optional`	✅	5s	3s	+67%
`polyvecl_uniform_gamma1`	✅	5s	2s	+150%
`sign_keypair`	✅	5s	4s	+25%
`sign_keypair_internal`	✅	5s	6s	-17%
`sign_signature_pre_hash_shake256`	✅	5s	6s	-17%
`unpack_sk_t0hat`	✅	5s	7s	-29%
`intt_native_aarch64`	✅	4s	3s	+33%
`intt_native_x86_64`	✅	4s	3s	+33%
`keccak_f1600_x1_native_aarch64`	✅	4s	1s	+300%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	4s	4s	+0%
`keccakf1600x4_permute`	✅	4s	3s	+33%
`mld_prepare_domain_separation_prefix`	✅	4s	4s	+0%
`mld_sign_finish`	✅	4s	-	new
`mld_sign_resume`	✅	4s	-	new
`ntt_native_aarch64`	✅	4s	6s	-33%
`ntt_native_x86_64`	✅	4s	2s	+100%
`pack_sk_s1`	✅	4s	1s	+300%
`pointwise_native_aarch64`	✅	4s	5s	-20%
`poly_caddq_c`	✅	4s	3s	+33%
`poly_caddq_native`	✅	4s	4s	+0%
`poly_chknorm_native_aarch64`	✅	4s	4s	+0%
`poly_decompose_c`	✅	4s	5s	-20%
`poly_uniform`	✅	4s	4s	+0%
`poly_uniform_eta`	✅	4s	4s	+0%
`poly_use_hint`	✅	4s	1s	+300%
`poly_use_hint_native_x86_64`	✅	4s	-	new
`polyeta_pack`	✅	4s	4s	+0%
`polyt1_unpack`	✅	4s	4s	+0%
`polyveck_pack_eta`	✅	4s	6s	-33%
`polyveck_pack_w1`	✅	4s	3s	+33%
`polyvecl_unpack_eta`	✅	4s	5s	-20%
`polyw1_pack`	✅	4s	4s	+0%
`polyz_pack`	✅	4s	5s	-20%
`polyz_unpack_19_native_aarch64`	✅	4s	4s	+0%
`polyz_unpack_native`	✅	4s	4s	+0%
`power2round`	✅	4s	4s	+0%
`rej_eta_c`	✅	4s	5s	-20%
`rej_eta_native`	✅	4s	6s	-33%
`rej_uniform_native_aarch64`	✅	4s	2s	+100%
`sign_pk_from_sk`	✅	4s	6s	-33%
`sign_signature`	✅	4s	5s	-20%
`sign_signature_extmu`	✅	4s	4s	+0%
`sign_verify`	✅	4s	5s	-20%
`sk_s2hat_get_poly`	✅	4s	3s	+33%
`sys_check_capability`	✅	4s	3s	+33%
`unpack_pk_t1`	✅	4s	1s	+300%
`unpack_sk`	✅	4s	5s	-20%
`unpack_sk_s1hat`	✅	4s	2s	+100%
`fqscale`	✅	3s	3s	+0%
`keccak_absorb`	✅	3s	3s	+0%
`keccak_f1600_x4_native_aarch64_v84a`	✅	3s	4s	-25%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	3s	3s	+0%
`keccak_f1600_x4_native_avx2`	✅	3s	2s	+50%
`keccak_finalize`	✅	3s	1s	+200%
`keccak_squeeze`	✅	3s	2s	+50%
`keccakf1600_extract_bytes (big endian)`	✅	3s	3s	+0%
`keccakf1600_xor_bytes`	✅	3s	3s	+0%
`keccakf1600x4_xor_bytes`	✅	3s	3s	+0%
`make_hint`	✅	3s	3s	+0%
`mld_ct_cmask_neg_i32`	✅	3s	4s	-25%
`mld_ct_sel_int32`	✅	3s	3s	+0%
`mld_h`	✅	3s	3s	+0%
`mld_keccakf1600x4_extract_bytes_c`	✅	3s	2s	+50%
`mld_keccakf1600x4_xor_bytes_c`	✅	3s	4s	-25%
`mld_polymat_expand_entry`	✅	3s	3s	+0%
`mld_value_barrier_i64`	✅	3s	1s	+200%
`mld_value_barrier_u32`	✅	3s	2s	+50%
`mld_value_barrier_u8`	✅	3s	3s	+0%
`pack_sig_c`	✅	3s	4s	-25%
`pack_sig_h`	✅	3s	4s	-25%
`pack_sk_rho_key_tr_s2`	✅	3s	3s	+0%
`poly_caddq_native_x86_64`	✅	3s	2s	+50%
`poly_chknorm_native_x86_64`	✅	3s	2s	+50%
`poly_decompose_32_native_aarch64`	✅	3s	5s	-40%
`poly_decompose_88_native_aarch64`	✅	3s	2s	+50%
`poly_decompose_native_x86_64`	✅	3s	2s	+50%
`poly_pointwise_montgomery_native`	✅	3s	5s	-40%
`poly_reduce`	✅	3s	2s	+50%
`poly_shiftl`	✅	3s	4s	-25%
`poly_sub`	✅	3s	3s	+0%
`poly_uniform_gamma1`	✅	3s	4s	-25%
`poly_uniform_gamma1_4x`	✅	3s	3s	+0%
`poly_use_hint_c`	✅	3s	2s	+50%
`poly_use_hint_native`	✅	3s	3s	+0%
`poly_use_hint_native_aarch64`	✅	3s	2s	+50%
`polyt0_pack`	✅	3s	4s	-25%
`polyveck_reduce`	✅	3s	3s	+0%
`polyveck_unpack_eta`	✅	3s	4s	-25%
`polyvecl_pack_eta`	✅	3s	3s	+0%
`polyvecl_pointwise_acc_montgomery_native`	✅	3s	3s	+0%
`polyvecl_uniform_gamma1_serial`	✅	3s	4s	-25%
`polyw1_pack_32`	✅	3s	4s	-25%
`polyw1_pack_88`	✅	3s	3s	+0%
`polyz_unpack_c`	✅	3s	3s	+0%
`rej_eta`	✅	3s	4s	-25%
`shake128_absorb`	✅	3s	4s	-25%
`shake128_finalize`	✅	3s	2s	+50%
`shake128_init`	✅	3s	1s	+200%
`shake128x4_squeezeblocks`	✅	3s	3s	+0%
`shake256`	✅	3s	2s	+50%
`shake256x4_squeezeblocks`	✅	3s	1s	+200%
`sig_unpack_hints`	✅	3s	3s	+0%
`sign_verify_extmu`	✅	3s	3s	+0%
`sign_verify_pre_hash_shake256`	✅	3s	3s	+0%
`sk_s1hat_get_poly`	✅	3s	3s	+0%
`unpack_sk_s2hat`	✅	3s	3s	+0%
`use_hint`	✅	3s	3s	+0%
`yvec_get_poly`	✅	3s	4s	-25%
`caddq`	✅	2s	4s	-50%
`decompose`	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64_v84a`	✅	2s	1s	+100%
`keccak_init`	✅	2s	3s	-33%
`keccak_squeezeblocks_x4`	✅	2s	4s	-50%
`keccakf1600_permute_native`	✅	2s	4s	-50%
`keccakf1600_xor_bytes (big endian)`	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes`	✅	2s	2s	+0%
`keccakf1600x4_xor_bytes_native`	✅	2s	3s	-33%
`mld_ct_abs_i32`	✅	2s	3s	-33%
`mld_ct_cmask_nonzero_u32`	✅	2s	2s	+0%
`mld_ct_cmask_nonzero_u8`	✅	2s	3s	-33%
`mld_ct_get_optblocker_u8`	✅	2s	3s	-33%
`mld_ct_memcmp`	✅	2s	3s	-33%
`mld_keccakf1600_extract_bytes`	✅	2s	4s	-50%
`montgomery_reduce`	✅	2s	3s	-33%
`nttunpack_native_x86_64`	✅	2s	3s	-33%
`pack_sig_z`	✅	2s	5s	-60%
`poly_caddq`	✅	2s	2s	+0%
`poly_caddq_native_aarch64`	✅	2s	3s	-33%
`poly_chknorm_native`	✅	2s	4s	-50%
`poly_decompose_native`	✅	2s	2s	+0%
`poly_invntt_tomont`	✅	2s	1s	+100%
`poly_permute_bitrev_to_custom_optional_native`	✅	2s	5s	-60%
`poly_power2round`	✅	2s	3s	-33%
`polyt1_pack`	✅	2s	3s	-33%
`polyvec_matrix_pointwise_montgomery_row`	✅	2s	3s	-33%
`polyveck_chknorm`	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery`	✅	2s	5s	-60%
`polyvecl_unpack_z`	✅	2s	4s	-50%
`polyz_unpack`	✅	2s	2s	+0%
`polyz_unpack_17_native_aarch64`	✅	2s	3s	-33%
`polyz_unpack_native_x86_64`	✅	2s	3s	-33%
`reduce32`	✅	2s	3s	-33%
`rej_uniform_eta_native_aarch64`	✅	2s	5s	-60%
`shake128_release`	✅	2s	4s	-50%
`shake128_squeeze`	✅	2s	2s	+0%
`shake256_absorb`	✅	2s	2s	+0%
`shake256_finalize`	✅	2s	2s	+0%
`shake256_init`	✅	2s	2s	+0%
`shake256_release`	✅	2s	3s	-33%
`keccakf1600_permute`	✅	1s	3s	-67%
`keccakf1600x4_extract_bytes_native`	✅	1s	2s	-50%
`mld_ct_get_optblocker_i64`	✅	1s	3s	-67%
`mld_ct_get_optblocker_u32`	✅	1s	2s	-50%
`poly_decompose`	✅	1s	3s	-67%
`poly_invntt_tomont_native`	✅	1s	5s	-80%
`poly_ntt_native`	✅	1s	3s	-67%
`shake128x4_absorb_once`	✅	1s	5s	-80%
`shake256_squeeze`	✅	1s	2s	-50%
`shake256x4_absorb_once`	✅	1s	2s	-50%
`sk_t0hat_get_poly`	✅	1s	4s	-75%
`yvec_init`	✅	1s	4s	-75%

oqs-bot · 2026-06-29T05:04:12Z

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

Full Results (209 proofs)

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

oqs-bot · 2026-06-29T05:04:28Z

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

Full Results (209 proofs)

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

hanno-becker · 2026-07-13T10:27:40Z

@mkannwischer Thank you for the review!

I changed the distribution test so that a) by default, 2000 iterations are run and a wide error margin allowed, b) a dedicated CI job exercises a larger number of iterations and accordingly checks for a narrower error.

Move the kappa upper bound MLD_MAX_KAPPA -- the largest counter kappa keeping the y-sampling nonces within uint16_t -- from sign.c to params.h, beside MLDSA_L which it derives from. Replace the open-coded `UINT16_MAX - MLDSA_L` in the polyvec contracts and comments with it. No functional change. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

Functions carrying the optional MLD_CONFIG_CONTEXT_PARAMETER that do not otherwise use it must consume it to avoid -Wunused-parameter, but only when a context is actually configured. This was previously done via an #if-guarded ((void)context). Introduce MLD_CONTEXT_UNUSED(context) in context.h, expanding to ((void)(context)) when a context parameter is configured and to an empty statement otherwise, and use it in the default (stack) MLD_FREE and in the skip-PCT stub. No functional change. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

Redefine MLD_MAX_SIGNING_ATTEMPTS as the effective bound on signing attempts: the configured MLD_CONFIG_MAX_SIGNING_ATTEMPTS if set, otherwise the hard type-safety bound MLD_MAX_KAPPA / MLDSA_L. mld_get_max_signing_attempts() returns it directly, and its contract bounds the result by MLD_MAX_KAPPA / MLDSA_L (the hard bound), independent of the configured value. This keeps the type-safety bound (used by the loop and casts) distinct from the configured attempt limit, and prepares for the signing hooks, which clamp the resume point against the effective bound. No functional change. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

The runtime of ML-DSA signatures is theoretically unbounded. Even the bound of max 814 signature attempts -- approved by NIST as lowering the chance of signing failure below 2^{-256} -- leaves a performance distribution whose peak percentiles can be unacceptable for constrained systems with strict timing requirements. The library already provides MLD_CONFIG_MAX_SIGNING_ATTEMPTS to cap the number of signing attempts. However, FIPS 204 forbids lowering that bound below 814, rendering the option non-compliant in constrained environments. As a remedy, this commit introduces three optional 'signing hooks' around the core rejection-sampling loop, keyed by the attempt counter (the loop iteration; the spec counter is kappa = attempt*MLDSA_L): - `attempt = sign_resume()`: Return the attempt to resume the operation from. `0` for an initial / non-restartable signing operation. - `sign_attempt(attempt)`: Called before each attempt. Returns 0 to proceed, or non-zero to pause: signing then returns MLD_ERR_SIGNING_PAUSED with `attempt` as the resume point. - `sign_finish(attempt)`: Called on success with the succeeding attempt. Together, resume + attempt make signing _restartable_: a caller can pause after a bounded number of attempts and later resume from the recorded attempt, bounding per-call runtime while keeping a FIPS-compliant overall bound and reproducing the same signature as an uninterrupted run. This only works if the consumer drives the deterministic internal API: the randomized API would choose a fresh seed on each (re-)start, so restarting could not reproduce the uninterrupted signature. Enabling any of the three hooks therefore requires MLD_CONFIG_NO_RANDOMIZED_API, which in turn is incompatible with MLD_CONFIG_KEYGEN_PCT (whose one-shot internal signature cannot be resumed). A logging-only use -- the attempt hook always returns 0, with resume/finish merely observing, e.g. to benchmark the per-signature attempt distribution -- would be safe with the randomized API too, but the restriction is imposed uniformly on all three hooks for now. Pausing is independent of MLD_CONFIG_MAX_SIGNING_ATTEMPTS, the upper bound on the total number of attempts (>= 814 for FIPS 204 compliance) after which signing gives up with the distinct error MLD_ERR_SIGN_ATTEMPTS_EXHAUSTED; it must not be lowered as a restart mechanism. sign_{resume|attempt|finish} can be implemented on mutable globals or on a context, so they are introduced under the existing MLD_CONFIG_CONTEXT_PARAMETER wrapper, which lets functions be called with or without an application-specific context pointer. This commit adds the core machinery in mldsa/: - Independent MLD_CONFIG_SIGN_HOOK_{RESUME,ATTEMPT,FINISH} options. When set, the integration provides, respectively: - `attempt = mld_sign_hook_resume([ctx])`: provide initial/resume attempt - `mld_sign_hook_attempt(attempt [, ctx])`: per-attempt hook; pause via non-zero return - `mld_sign_hook_finish(attempt [, ctx])`: note the succeeding attempt The unset dummies leave the default build unchanged. - The MLD_ERR_SIGNING_PAUSED error code, returned when the attempt hook pauses. CBMC proofs, a test, and the regenerated configs follow in separate commits. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

Add a FAQ entry to README.md pointing users with real-time / bounded-runtime requirements at the signing hooks and the examples/restartable_sign example. Documentation only. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

Verify the three signing-hook call sites added in the previous commit: mld_sign_resume, mld_sign_attempt and mld_sign_finish. In the CBMC configuration the hooks reduce to their contract dummies, so each harness just checks the call-by-contract stub against its (empty) contract, mirroring how sign.c invokes them (the CBMC config carries no context parameter, so the `context` argument is consumed by the call macro exactly as at the call sites). Also refresh the sign_signature_internal harness Makefile for the reworked signing loop. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

Add a test analogous to test_alloc, driven by a custom config (test_sign_hook_config.h) that enables the three signing-hook options and forward-declares the hook context; the context type and the hook implementations live in the test. The hooks pause signing after a configurable number of attempts and resume from the recorded attempt, letting one context drive: - a known-answer smoke test, reproducing the test-vector signature both one-shot and single-step; - a restartable-signing equivalence test, checking that pausing after a random number of attempts and resuming yields the same signature as an uninterrupted run, over many random signing-randomness draws; - a distribution test, gathering the attempts-per-signature histogram over many one-shot signatures and checking the measured attempts/signature ratio against the expected geometric mean for the parameter set. The test requires the internal signing API, so it compiles to a no-op main under MLD_CONFIG_NO_SIGN_API. The distribution test additionally generates a fresh key per iteration (the other two use the fixed test-vector key), so it alone is compiled out under MLD_CONFIG_NO_KEYPAIR_API. Statistics are printed via printf only (no putchar), so freestanding platforms with a minimal stdio shim can run it. Wire it up in the Makefile, the test make fragments and scripts/tests (new --sign-hook subcommand). Mirror alloc's CI plumbing: add a sign_hook input to the functest / multi-functest actions and disable it for the config variations it is incompatible with -- those passing their own MLD_CONFIG_FILE (would clash with the test's fixed config) and those enabling MLD_CONFIG_KEYGEN_PCT (the signing hooks require MLD_CONFIG_NO_RANDOMIZED_API, which is incompatible with the PCT). The generated configs follow in a separate commit. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

Rerun scripts/autogen after the preceding commits, updating various files. Done separately to ease reviewing of the core of the changes. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

Add examples/restartable_sign, demonstrating the MLD_CONFIG_SIGN_HOOK_{RESUME, ATTEMPT,FINISH} hooks. The example provides the three hooks over a single global, drives the deterministic signing API in a loop that pauses (via MLD_ERR_SIGNING_PAUSED) after every attempt and resumes from the recorded point, and checks that the split, single-step run reproduces both the one-shot signature and the reference test vector. Wire it into the examples README, the examples CI job, and scripts/tests. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

hanno-becker changed the title ~~Sign hooks~~ Add signing hooks for observing signature attempts and implementing restartable signing Jun 28, 2026

hanno-becker changed the title ~~Add signing hooks for observing signature attempts and implementing restartable signing~~ [WIP] Add signing hooks for observing signature attempts and implementing restartable signing Jun 28, 2026

hanno-becker force-pushed the sign_hooks branch from 3388463 to 35fc751 Compare June 28, 2026 21:06

hanno-becker force-pushed the sign_hooks branch 3 times, most recently from ba5df63 to 004fcc0 Compare June 29, 2026 04:43

hanno-becker force-pushed the sign_hooks branch 8 times, most recently from b2ef39d to 4acce0a Compare June 29, 2026 10:33

hanno-becker changed the title ~~[WIP] Add signing hooks for observing signature attempts and implementing restartable signing~~ Add signing hooks for observing signature attempts and implementing restartable signing Jun 29, 2026

hanno-becker force-pushed the sign_hooks branch 9 times, most recently from ec79a2c to 9686b66 Compare July 1, 2026 18:25

hanno-becker force-pushed the sign_hooks branch 8 times, most recently from ebcd246 to 815f90d Compare July 12, 2026 18:33

hanno-becker marked this pull request as draft July 12, 2026 21:08

hanno-becker force-pushed the sign_hooks branch 4 times, most recently from 8772ce2 to 915038e Compare July 13, 2026 10:14

hanno-becker requested a review from mkannwischer July 13, 2026 10:19

hanno-becker marked this pull request as ready for review July 13, 2026 10:20

hanno-becker force-pushed the sign_hooks branch from 915038e to 32899f3 Compare July 13, 2026 10:25

hanno-becker force-pushed the sign_hooks branch 2 times, most recently from cc67609 to a8420d3 Compare July 13, 2026 12:04

mkannwischer added this to the v1.0.0 milestone Jul 14, 2026

hanno-becker added 9 commits July 14, 2026 06:53

autogen: Regenerate configs for the signing hooks

8aa05ac

Rerun scripts/autogen after the preceding commits, updating various files. Done separately to ease reviewing of the core of the changes. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

hanno-becker force-pushed the sign_hooks branch from a8420d3 to 96fda9e Compare July 14, 2026 06:11

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Add signing hooks for observing signature attempts and implementing restartable signing#1237

Add signing hooks for observing signature attempts and implementing restartable signing#1237
hanno-becker wants to merge 9 commits into
mainfrom
sign_hooks

hanno-becker commented Jun 28, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Jun 28, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Jun 28, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Jun 28, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Jun 28, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Jun 29, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Jun 29, 2026 •

edited

Loading

Uh oh!

hanno-becker commented Jul 13, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

hanno-becker commented Jun 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

oqs-bot commented Jun 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 Jun 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 Jun 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 Jun 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 Jun 29, 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 Jun 29, 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 commented Jul 13, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

hanno-becker commented Jun 28, 2026 •

edited

Loading

oqs-bot commented Jun 28, 2026 •

edited

Loading

oqs-bot commented Jun 28, 2026 •

edited

Loading

oqs-bot commented Jun 28, 2026 •

edited

Loading

oqs-bot commented Jun 28, 2026 •

edited

Loading

oqs-bot commented Jun 29, 2026 •

edited

Loading

oqs-bot commented Jun 29, 2026 •

edited

Loading