Armv8.1-M: regenerate Keccak x1 for Cortex-M55 by bremoran · Pull Request #1356 · pq-code-package/mldsa-native

bremoran · 2026-08-05T12:47:53Z

Depends on #1277.
Fixes #1336.

Summary

Regenerate the scalar single-state Keccak-f[1600] schedule using SLOTHY's
Armv8.1-M / Cortex-M55r1 model.

Pin SLOTHY to fed47d3f1e40b9c1f202f759f1d6c4100fe14f4d
(slothy-optimizer/slothy#464).
Generate and ship the M55-specific
keccak_f1600_x1_armv7m_opt_m55.S artifact.
Update the development Makefile, autogen routing, ABI-check job list,
monolithic assembly include, and bibliography.
Preserve the scalar ABI contract (Features: []); this change does not
require MVE.
Remove the unused embedded round-constant table from the clean input. The
wrapper already supplies the round constants; removing the unused table
ensures the exported assembly function remains at offset zero for
simpasm.

Validation

nix develop .#cross-autogen --command python3 ./scripts/autogen --dry-run --force-cross
QEMU functional tests on mps3-an547 with OPT=1 AUTO=0:
ML-DSA-44, -65, and -87 passed.
QEMU Armv8.1-M ABI checks on mps3-an547 with OPT=1 AUTO=0:
keccak_f1600_x1_armv7m_asm passed.
NUCLEO-N657X0-Q component benchmark executed successfully for ML-DSA-44,
-65, and -87.

Build the ABI checker and assembly sources directly with Zephyr's target toolchain. Select the Armv8.1-M checker for M55 and preserve OPT/AUTO through the run stage so the checker is actually executed. Signed-off-by: Brendan Moran <brendan.moran@arm.com>

Include OPT, the selected FIPS202 backend, and configurable test counts in the active build marker so changes to those inputs rebuild stale Zephyr binaries. Track the native assembly amalgamation and its direct development-source include as explicit dependencies, and allow QEMU execution timeouts to be overridden. Signed-off-by: Brendan Moran <brendan.moran@arm.com>

Signed-off-by: Brendan Moran <brendan.moran@arm.com>

The lazy/eager polyvector unit test allocates both ML-DSA-87 representations and their scratch space through MLD_ALLOC. The default MLD_ALLOC implementation expands to aligned automatic arrays, so this single test exceeds the Zephyr test thread stack on the Cortex-M55 test configuration. Use test-local, aligned static buffers for this workspace. The TEST_STATIC_ALLOC and TEST_STATIC_FREE helpers are deliberately scoped to test_unit.c: they preserve cleanup by zeroizing every buffer and clearing its pointer, without changing the allocator used by production code or other tests. Only test/src/test_unit.c changes. The test inputs, comparisons, and coverage remain the same; this commit changes where its temporary workspace is stored. Signed-off-by: Brendan Moran <brendan.moran@arm.com>

Generated ABI checks normally fill every assembly argument buffer with random bytes. That is unsuitable for interfaces containing control data. The Armv8.1-M Keccak x1 permutation consumes 49 round-constant words and requires the final word to be 0x000000ff as a loop terminator. Leaving that word random can make the checker read beyond the supplied buffer. Add an optional test_bytes mapping to buffer entries in the assembly ABI YAML. scripts/autogen validates that offsets are integers within the buffer and that values are bytes, sorts the overrides, and emits them after randombytes initializes the rest of the buffer. Existing ABI metadata without test_bytes retains its current behaviour. Document the new metadata in test/abicheck/README.md. The generic facility is introduced here before its Keccak x1 consumer so the following backend commit contains only feature-specific metadata and generated checks. Signed-off-by: Brendan Moran <brendan.moran@arm.com>

Add the first of three deliberately separated Cortex-M55 Keccak changes: a known-good scalar baseline derived from the Adomnicai/XKCP Armv7-M implementation. Measurements made while preparing the series showed that the existing Cortex-M7 schedule runs faster on Cortex-M55 than the Cortex-M4 schedule, so this commit establishes the M7-scheduled implementation before later commits introduce an M55 scheduling model and a 64-bit load/store-aware scalar input. The code in this commit is scalar and does not require or use MVE. Keep the Keccak state in the even/odd bit-interleaved representation across permutations. Native xor and extract hooks convert only the lanes crossing the byte interface, and a private round-constant table supplies the 24 interleaved constants and loop terminator expected by the permutation. Organize the implementation so its origin and generated form remain reviewable. dev/fips202/armv81m_clean contains only the unscheduled permutation input. dev/fips202/armv81m_opt contains the SLOTHY driver, Makefile, concise development README, C wrapper, scheduled permutation, and separate scalar xor and extract assembly sources. Splitting the helpers gives every assembly file one external entry point and lets the normal loop-label check cover all x1 sources. Teach scripts/autogen to merge the existing Armv8.1-M and new x1 development directories into the production directory. The retained filename set is derived from both inputs, replacing the hard-coded keep list and ensuring removed or renamed files cannot leave stale output. The helper assembly is simplified and synchronized like other production assembly, so mldsa_native_asm.S includes only files under mldsa/ and no longer reaches into dev/. Zephyr custom builds track all production assembly inputs for reliable rebuilds. Describe and generate AAPCS32 checks for all three external assembly routines: permutation, xor, and extract. The scalar routines carry no MVE feature requirement. Add focused xor and extract tests for zero length, unaligned starts, 7/8/9-byte lane boundaries, cross-lane ranges, final-lane ranges, and the complete 200-byte state; canary-filled extraction buffers also detect writes beyond the requested length. Existing representation-aware permutation tests continue to compare against the portable reference. Update the bibliography and license material for the imported XKCP, Adomnicai, and SLOTHY work. Keep the x1 header, constants, sources, generation path, tests, and ABI metadata separate from the established parallel implementation so no x4 source file is changed. Signed-off-by: Brendan Moran <brendan.moran@arm.com>

Make the clean M7 Keccak source self-contained so SLOTHY retains its ABI metadata and integration guards during regeneration. Signed-off-by: Brendan Moran <brendan.moran@arm.com>

Regenerate the scalar Keccak-f[1600] x1 schedule with the Armv8.1-M Cortex-M55 SLOTHY model, retain scalar ABI metadata, and wire the generated M55 artifact through autogen and production assembly. Hypothesis: H_SLOTHY_001_LDRD_STRD_MODEL Signed-off-by: Brendan Moran <brendan.moran@arm.com>

oqs-bot · 2026-08-05T13:27:23Z

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

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`TOTAL`	⚠️	2025s	1436s	+41.0%
`compute_pack_t0_t1`	⚠️	41s	12s	+242%
`mld_attempt_signature_generation`	⚠️	217s	34s	+538%
`sig_unpack_hints`	⚠️	22s	4s	+450%
`sign_pk_from_sk`	⚠️	56s	6s	+833%
`sign_verify_internal`	⚠️	260s	47s	+453%

Full Results (210 proofs)

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

oqs-bot · 2026-08-05T13:27:43Z

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

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`TOTAL`	⚠️	2007s	1364s	+47.1%
`compute_pack_t0_t1`	⚠️	43s	12s	+258%
`mld_attempt_signature_generation`	⚠️	193s	19s	+916%
`rej_uniform`	⚠️	22s	8s	+175%
`sig_unpack_hints`	⚠️	39s	2s	+1850%
`sign_pk_from_sk`	⚠️	41s	5s	+720%
`sign_verify_internal`	⚠️	270s	49s	+451%

Full Results (210 proofs)

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

oqs-bot · 2026-08-05T13:29:10Z

CBMC Results (ML-DSA-44)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`TOTAL`	⚠️	2220s	1514s	+46.6%
`compute_pack_t0_t1`	⚠️	98s	50s	+96%
`mld_attempt_signature_generation`	⚠️	339s	58s	+484%
`sig_unpack_hints`	⚠️	44s	2s	+2100%
`sign_pk_from_sk`	⚠️	42s	5s	+740%
`sign_signature_internal`	⚠️	74s	26s	+185%
`sign_verify_internal`	⚠️	267s	114s	+134%

Full Results (210 proofs)

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

oqs-bot · 2026-08-05T13:30:12Z

CBMC Results (ML-DSA-65)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`TOTAL`	⚠️	2728s	1784s	+52.9%
`compute_pack_t0_t1`	⚠️	77s	13s	+492%
`mld_attempt_signature_generation`	⚠️	418s	63s	+563%
`sig_unpack_hints`	⚠️	32s	2s	+1500%
`sign_pk_from_sk`	⚠️	52s	6s	+767%
`sign_signature_internal`	⚠️	107s	55s	+95%
`sign_verify_internal`	⚠️	407s	177s	+130%

Full Results (210 proofs)

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

oqs-bot · 2026-08-05T13:30:44Z

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

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`TOTAL`	⚠️	2318s	1482s	+56.4%
`compute_pack_t0_t1`	⚠️	50s	7s	+614%
`mld_attempt_signature_generation`	⚠️	453s	31s	+1361%
`rej_uniform`	⚠️	21s	7s	+200%
`sign_pk_from_sk`	⚠️	45s	5s	+800%
`sign_signature_internal`	⚠️	20s	6s	+233%
`sign_verify_internal`	⚠️	264s	71s	+272%

Full Results (210 proofs)

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

oqs-bot · 2026-08-05T13:31:54Z

CBMC Results (ML-DSA-87)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`TOTAL`	⚠️	3074s	2151s	+42.9%
`compute_pack_t0_t1`	⚠️	81s	19s	+326%
`mld_attempt_signature_generation`	⚠️	362s	55s	+558%
`sig_unpack_hints`	⚠️	27s	3s	+800%
`sign_pk_from_sk`	⚠️	45s	6s	+650%
`sign_signature_internal`	⚠️	155s	42s	+269%
`sign_verify_internal`	⚠️	515s	97s	+431%

Full Results (210 proofs)

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

bremoran added 8 commits August 3, 2026 17:16

Test: Preserve build mode when running tests

c4a6ece

Signed-off-by: Brendan Moran <brendan.moran@arm.com>

Armv8.1-M: preserve Keccak metadata through SLOTHY

962c9f9

Make the clean M7 Keccak source self-contained so SLOTHY retains its ABI metadata and integration guards during regeneration. Signed-off-by: Brendan Moran <brendan.moran@arm.com>

bremoran requested a review from a team as a code owner August 5, 2026 12:47

Navigation Menu

Uh oh!

Armv8.1-M: regenerate Keccak x1 for Cortex-M55 - #1356

Armv8.1-M: regenerate Keccak x1 for Cortex-M55#1356
bremoran wants to merge 8 commits into
mainfrom
issue-1336-regenerate-m55-keccak

bremoran commented Aug 5, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Aug 5, 2026

Uh oh!

oqs-bot commented Aug 5, 2026

Uh oh!

oqs-bot commented Aug 5, 2026

Uh oh!

oqs-bot commented Aug 5, 2026

Uh oh!

oqs-bot commented Aug 5, 2026

Uh oh!

oqs-bot commented Aug 5, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

bremoran commented Aug 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Validation

Uh oh!

oqs-bot commented Aug 5, 2026

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

Uh oh!

oqs-bot commented Aug 5, 2026

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

Uh oh!

oqs-bot commented Aug 5, 2026

CBMC Results (ML-DSA-44)

Uh oh!

oqs-bot commented Aug 5, 2026

CBMC Results (ML-DSA-65)

Uh oh!

oqs-bot commented Aug 5, 2026

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

Uh oh!

oqs-bot commented Aug 5, 2026

CBMC Results (ML-DSA-87)

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

bremoran commented Aug 5, 2026 •

edited

Loading