Armv8.1-M: Add clean x4 Keccak code and SLOTHY Makefile by mkannwischer · Pull Request #1527 · pq-code-package/mlkem-native

mkannwischer · 2026-01-28T09:35:35Z

Add the clean (non-optimized) Keccak x4 assembly and Makefile to enable regeneration of the SLOTHY-optimized assembly.

Extend autogen --slothy to support new function, and also add --slothy armv81m and --slothy aarch64 group options. Update CI to only run aarch64 SLOTHY targets.

Optimization of Armv8.1-M assembly is not currently tested in CI, but has been tested locally.

Update SLOTHY to version 0.1.10 as the code requires disabling the address offset fixup which is not supported for Armv8.1-M in the older versionf of SLOTHY.

Resolves Armv8.1-M: Add Keccak x4 assembly and SLOTHY Makefile #1510

oqs-bot · 2026-01-28T10:24:20Z

CBMC Results (ML-KEM-768)

Full Results (187 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	1570s	1432s	+9.6%
`mlk_indcpa_enc`	✅	293s	287s	+2%
`mlk_indcpa_keypair_derand`	✅	257s	221s	+16%
`mlk_rej_uniform_c`	✅	101s	90s	+12%
`polyvec_basemul_acc_montgomery_cached_native`	✅	74s	66s	+12%
`mlk_polyvec_basemul_acc_montgomery_cached_c`	✅	65s	63s	+3%
`mlk_poly_rej_uniform`	✅	44s	40s	+10%
`poly_ntt_native`	✅	33s	32s	+3%
`mlk_polyvec_add`	✅	32s	31s	+3%
`mlk_keccak_squeezeblocks_x4`	✅	29s	27s	+7%
`mlk_poly_reduce_native`	✅	19s	17s	+12%
`keccakf1600x4_permute_native_x4`	✅	18s	19s	-5%
`mlk_ntt_layer`	✅	18s	15s	+20%
`mlk_indcpa_dec`	✅	17s	15s	+13%
`mlk_poly_decompress_d10_native`	✅	16s	16s	+0%
`mlk_poly_decompress_d4_native`	✅	15s	14s	+7%
`mlk_poly_frommsg`	✅	14s	12s	+17%
`mlk_keccak_absorb_once_x4`	✅	10s	9s	+11%
`mlk_keccak_squeeze_once`	✅	9s	6s	+50%
`mlk_ntt_butterfly_block`	✅	9s	8s	+12%
`mlk_poly_frombytes_native`	✅	9s	9s	+0%
`mlk_poly_rej_uniform_x4`	✅	8s	8s	+0%
`mlk_polymat_permute_bitrev_to_custom`	✅	8s	7s	+14%
`mlk_invntt_layer`	✅	7s	6s	+17%
`mlk_keccak_squeezeblocks`	✅	7s	8s	-12%
`mlk_shake256x4`	✅	7s	3s	+133%
`poly_frombytes_native_x86_64`	✅	7s	6s	+17%
`keccakf1600_permute_native`	✅	6s	5s	+20%
`mlk_fqmul`	✅	6s	5s	+20%
`mlk_keccakf1600_permute`	✅	6s	2s	+200%
`poly_decompress_d10_native_x86_64`	✅	6s	3s	+100%
`kem_dec`	✅	5s	5s	+0%
`mlk_gen_matrix`	✅	5s	3s	+67%
`mlk_keccak_absorb_once`	✅	5s	5s	+0%
`mlk_poly_add`	✅	5s	7s	-29%
`mlk_poly_compress_d10_c`	✅	5s	3s	+67%
`mlk_poly_compress_d4_c`	✅	5s	4s	+25%
`mlk_poly_decompress_d11`	✅	5s	4s	+25%
`mlk_polyvec_permute_bitrev_to_custom`	✅	5s	1s	+400%
`mlk_scalar_signed_to_unsigned_q`	✅	5s	3s	+67%
`mlk_value_barrier_u32`	✅	5s	1s	+400%
`mlk_value_barrier_u8`	✅	5s	2s	+150%
`ntt_native_aarch64`	✅	5s	2s	+150%
`poly_decompress_d4_native_x86_64`	✅	5s	4s	+25%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	4s	2s	+100%
`keccakf1600x4_extract_bytes_native`	✅	4s	3s	+33%
`keccakf1600x4_xor_bytes_native`	✅	4s	4s	+0%
`mlk_ct_sel_int16`	✅	4s	2s	+100%
`mlk_gen_matrix_serial`	✅	4s	3s	+33%
`mlk_keccakf1600_extract_bytes`	✅	4s	2s	+100%
`mlk_matvec_mul`	✅	4s	2s	+100%
`mlk_poly_compress_d5_native`	✅	4s	3s	+33%
`mlk_poly_decompress_d10_c`	✅	4s	3s	+33%
`mlk_poly_decompress_d11_c`	✅	4s	2s	+100%
`mlk_poly_mulcache_compute`	✅	4s	4s	+0%
`mlk_poly_mulcache_compute_c`	✅	4s	3s	+33%
`mlk_poly_reduce_c`	✅	4s	2s	+100%
`mlk_poly_tomont_native`	✅	4s	1s	+300%
`mlk_polyvec_basemul_acc_montgomery_cached`	✅	4s	3s	+33%
`mlk_polyvec_compress_du`	✅	4s	3s	+33%
`mlk_polyvec_tobytes`	✅	4s	2s	+100%
`mlk_scalar_compress_d11`	✅	4s	2s	+100%
`mlk_shake128x4_squeezeblocks`	✅	4s	1s	+300%
`ntt_native_x86_64`	✅	4s	3s	+33%
`poly_invntt_tomont_native`	✅	4s	2s	+100%
`polyvec_basemul_acc_montgomery_cached_k3_native_x86_64`	✅	4s	4s	+0%
`polyvec_basemul_acc_montgomery_cached_k4_native_x86_64`	✅	4s	3s	+33%
`sys_check_capability`	✅	4s	2s	+100%
`keccak_f1600_x1_native_aarch64_v84a`	✅	3s	2s	+50%
`kem_check_pk`	✅	3s	4s	-25%
`kem_enc_derand`	✅	3s	1s	+200%
`kem_keypair_derand`	✅	3s	2s	+50%
`mlk_ct_cmask_nonzero_u16`	✅	3s	1s	+200%
`mlk_ct_cmov_zero`	✅	3s	2s	+50%
`mlk_ct_get_optblocker_i32`	✅	3s	4s	-25%
`mlk_ct_sel_uint8`	✅	3s	2s	+50%
`mlk_keccakf1600x4_extract_bytes`	✅	3s	5s	-40%
`mlk_keccakf1600x4_permute`	✅	3s	4s	-25%
`mlk_poly_cbd_eta1`	✅	3s	2s	+50%
`mlk_poly_compress_d10_native`	✅	3s	1s	+200%
`mlk_poly_compress_d11`	✅	3s	2s	+50%
`mlk_poly_compress_d4`	✅	3s	2s	+50%
`mlk_poly_compress_d5`	✅	3s	2s	+50%
`mlk_poly_compress_d5_c`	✅	3s	2s	+50%
`mlk_poly_decompress_d4_c`	✅	3s	1s	+200%
`mlk_poly_decompress_d5_c`	✅	3s	2s	+50%
`mlk_poly_decompress_d5_native`	✅	3s	2s	+50%
`mlk_poly_getnoise_eta1122_4x`	✅	3s	2s	+50%
`mlk_poly_getnoise_eta1_4x_native`	✅	3s	1s	+200%
`mlk_poly_tobytes`	✅	3s	2s	+50%
`mlk_poly_tobytes_c`	✅	3s	2s	+50%
`mlk_poly_tomont`	✅	3s	3s	+0%
`mlk_poly_tomsg`	✅	3s	1s	+200%
`mlk_polyvec_invntt_tomont`	✅	3s	2s	+50%
`mlk_polyvec_mulcache_compute`	✅	3s	2s	+50%
`mlk_polyvec_permute_bitrev_to_custom_native`	✅	3s	1s	+200%
`mlk_polyvec_reduce`	✅	3s	4s	-25%
`mlk_rej_uniform`	✅	3s	4s	-25%
`mlk_scalar_compress_d10`	✅	3s	2s	+50%
`mlk_scalar_decompress_d10`	✅	3s	1s	+200%
`mlk_scalar_decompress_d5`	✅	3s	1s	+200%
`mlk_shake128_absorb_once`	✅	3s	2s	+50%
`mlk_shake128x4_absorb_once`	✅	3s	2s	+50%
`poly_compress_d10_native_x86_64`	✅	3s	1s	+200%
`poly_compress_d5_native_x86_64`	✅	3s	4s	-25%
`poly_decompress_d11_native_x86_64`	✅	3s	3s	+0%
`poly_mulcache_compute_native_aarch64`	✅	3s	3s	+0%
`poly_reduce_native_aarch64`	✅	3s	2s	+50%
`poly_reduce_native_x86_64`	✅	3s	5s	-40%
`poly_tobytes_native_aarch64`	✅	3s	3s	+0%
`poly_tomont_native_x86_64`	✅	3s	2s	+50%
`polyvec_basemul_acc_montgomery_cached_k4_native_aarch64`	✅	3s	1s	+200%
`keccak_f1600_x1_native_aarch64`	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	2s	1s	+100%
`keccak_f1600_x4_native_avx2`	✅	2s	3s	-33%
`kem_check_sk`	✅	2s	1s	+100%
`kem_enc`	✅	2s	3s	-33%
`kem_keypair`	✅	2s	2s	+0%
`mlk_barrett_reduce`	✅	2s	2s	+0%
`mlk_check_pct`	✅	2s	2s	+0%
`mlk_ct_cmask_neg_i16`	✅	2s	4s	-50%
`mlk_ct_cmask_nonzero_u8`	✅	2s	2s	+0%
`mlk_ct_memcmp`	✅	2s	2s	+0%
`mlk_keccakf1600_extract_bytes (big endian)`	✅	2s	4s	-50%
`mlk_keccakf1600_xor_bytes`	✅	2s	3s	-33%
`mlk_keypair_getnoise_eta1`	✅	2s	2s	+0%
`mlk_montgomery_reduce`	✅	2s	1s	+100%
`mlk_poly_cbd_eta2`	✅	2s	2s	+0%
`mlk_poly_compress_d10`	✅	2s	3s	-33%
`mlk_poly_compress_d11_c`	✅	2s	1s	+100%
`mlk_poly_compress_d4_native`	✅	2s	2s	+0%
`mlk_poly_compress_dv`	✅	2s	2s	+0%
`mlk_poly_decompress_d10`	✅	2s	2s	+0%
`mlk_poly_decompress_du`	✅	2s	2s	+0%
`mlk_poly_decompress_dv`	✅	2s	2s	+0%
`mlk_poly_frombytes`	✅	2s	3s	-33%
`mlk_poly_frombytes_c`	✅	2s	2s	+0%
`mlk_poly_getnoise_eta1_4x`	✅	2s	3s	-33%
`mlk_poly_invntt_tomont`	✅	2s	2s	+0%
`mlk_poly_invntt_tomont_c`	✅	2s	2s	+0%
`mlk_poly_mulcache_compute_native`	✅	2s	2s	+0%
`mlk_poly_ntt`	✅	2s	5s	-60%
`mlk_poly_reduce`	✅	2s	2s	+0%
`mlk_poly_tobytes_native`	✅	2s	4s	-50%
`mlk_poly_tomont_c`	✅	2s	2s	+0%
`mlk_polyvec_decompress_du`	✅	2s	2s	+0%
`mlk_polyvec_ntt`	✅	2s	1s	+100%
`mlk_polyvec_tomont`	✅	2s	2s	+0%
`mlk_scalar_compress_d4`	✅	2s	2s	+0%
`mlk_scalar_compress_d5`	✅	2s	3s	-33%
`mlk_scalar_decompress_d11`	✅	2s	2s	+0%
`mlk_scalar_decompress_d4`	✅	2s	1s	+100%
`mlk_sha3_512`	✅	2s	3s	-33%
`mlk_shake256`	✅	2s	2s	+0%
`mlk_value_barrier_i32`	✅	2s	1s	+100%
`nttunpack_native_x86_64`	✅	2s	4s	-50%
`poly_compress_d11_native_x86_64`	✅	2s	1s	+100%
`poly_compress_d4_native_x86_64`	✅	2s	3s	-33%
`poly_tobytes_native_x86_64`	✅	2s	3s	-33%
`polyvec_basemul_acc_montgomery_cached_k2_native_x86_64`	✅	2s	2s	+0%
`rej_uniform_native`	✅	2s	3s	-33%
`rej_uniform_native_aarch64`	✅	2s	5s	-60%
`rej_uniform_native_x86_64`	✅	2s	3s	-33%
`intt_native_aarch64`	✅	1s	3s	-67%
`intt_native_x86_64`	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v84a`	✅	1s	2s	-50%
`mlk_ct_get_optblocker_u32`	✅	1s	2s	-50%
`mlk_ct_get_optblocker_u8`	✅	1s	3s	-67%
`mlk_keccakf1600_xor_bytes (big endian)`	✅	1s	2s	-50%
`mlk_keccakf1600x4_xor_bytes`	✅	1s	4s	-75%
`mlk_poly_compress_d11_native`	✅	1s	3s	-67%
`mlk_poly_compress_du`	✅	1s	3s	-67%
`mlk_poly_decompress_d11_native`	✅	1s	2s	-50%
`mlk_poly_decompress_d4`	✅	1s	2s	-50%
`mlk_poly_decompress_d5`	✅	1s	3s	-67%
`mlk_poly_getnoise_eta2`	✅	1s	2s	-50%
`mlk_poly_ntt_c`	✅	1s	3s	-67%
`mlk_poly_sub`	✅	1s	3s	-67%
`mlk_polyvec_frombytes`	✅	1s	1s	+0%
`mlk_scalar_compress_d1`	✅	1s	2s	-50%
`mlk_sha3_256`	✅	1s	3s	-67%
`mlk_shake128_squeezeblocks`	✅	1s	1s	+0%
`poly_decompress_d5_native_x86_64`	✅	1s	2s	-50%
`poly_getnoise_eta1122_4x_native`	✅	1s	2s	-50%
`poly_mulcache_compute_native_x86_64`	✅	1s	2s	-50%
`poly_tomont_native_aarch64`	✅	1s	3s	-67%
`polyvec_basemul_acc_montgomery_cached_k2_native_aarch64`	✅	1s	2s	-50%
`polyvec_basemul_acc_montgomery_cached_k3_native_aarch64`	✅	1s	1s	+0%

oqs-bot · 2026-01-28T10:24:50Z

CBMC Results (ML-KEM-512)

Full Results (187 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	1074s	1123s	-4.4%
`mlk_indcpa_keypair_derand`	✅	149s	148s	+1%
`mlk_indcpa_enc`	✅	137s	133s	+3%
`mlk_rej_uniform_c`	✅	66s	67s	-1%
`mlk_polyvec_basemul_acc_montgomery_cached_c`	✅	65s	62s	+5%
`mlk_poly_rej_uniform`	✅	35s	38s	-8%
`poly_ntt_native`	✅	25s	30s	-17%
`mlk_keccak_squeezeblocks_x4`	✅	24s	24s	+0%
`keccakf1600x4_permute_native_x4`	✅	18s	18s	+0%
`polyvec_basemul_acc_montgomery_cached_native`	✅	17s	20s	-15%
`mlk_polyvec_add`	✅	15s	16s	-6%
`mlk_poly_reduce_native`	✅	13s	13s	+0%
`mlk_poly_decompress_d10_native`	✅	12s	14s	-14%
`mlk_poly_decompress_d4_native`	✅	12s	13s	-8%
`mlk_indcpa_dec`	✅	11s	15s	-27%
`mlk_ntt_layer`	✅	10s	13s	-23%
`mlk_poly_frombytes_native`	✅	9s	8s	+12%
`mlk_poly_frommsg`	✅	9s	11s	-18%
`mlk_keccak_absorb_once_x4`	✅	8s	9s	-11%
`mlk_keccak_squeeze_once`	✅	7s	6s	+17%
`mlk_ntt_butterfly_block`	✅	7s	7s	+0%
`mlk_poly_rej_uniform_x4`	✅	7s	6s	+17%
`mlk_polymat_permute_bitrev_to_custom`	✅	7s	9s	-22%
`keccakf1600_permute_native`	✅	6s	7s	-14%
`mlk_keccak_squeezeblocks`	✅	6s	5s	+20%
`poly_decompress_d4_native_x86_64`	✅	6s	8s	-25%
`kem_check_pk`	✅	5s	5s	+0%
`mlk_fqmul`	✅	5s	6s	-17%
`mlk_keccak_absorb_once`	✅	5s	4s	+25%
`mlk_poly_mulcache_compute_c`	✅	5s	4s	+25%
`mlk_poly_mulcache_compute_native`	✅	5s	4s	+25%
`mlk_poly_ntt_c`	✅	5s	2s	+150%
`mlk_polyvec_permute_bitrev_to_custom`	✅	5s	3s	+67%
`poly_decompress_d10_native_x86_64`	✅	5s	5s	+0%
`poly_frombytes_native_x86_64`	✅	5s	3s	+67%
`keccak_f1600_x1_native_aarch64_v84a`	✅	4s	1s	+300%
`keccakf1600x4_extract_bytes_native`	✅	4s	2s	+100%
`kem_dec`	✅	4s	6s	-33%
`kem_enc`	✅	4s	1s	+300%
`kem_keypair_derand`	✅	4s	2s	+100%
`mlk_gen_matrix`	✅	4s	5s	-20%
`mlk_keccakf1600_extract_bytes (big endian)`	✅	4s	4s	+0%
`mlk_poly_add`	✅	4s	5s	-20%
`mlk_poly_cbd_eta2`	✅	4s	5s	-20%
`mlk_poly_compress_d10`	✅	4s	2s	+100%
`mlk_poly_compress_d5`	✅	4s	2s	+100%
`mlk_poly_decompress_d5`	✅	4s	1s	+300%
`mlk_poly_getnoise_eta1_4x_native`	✅	4s	5s	-20%
`mlk_poly_tobytes`	✅	4s	3s	+33%
`mlk_polyvec_ntt`	✅	4s	3s	+33%
`mlk_polyvec_tomont`	✅	4s	2s	+100%
`mlk_rej_uniform`	✅	4s	2s	+100%
`mlk_scalar_signed_to_unsigned_q`	✅	4s	2s	+100%
`ntt_native_aarch64`	✅	4s	3s	+33%
`poly_mulcache_compute_native_aarch64`	✅	4s	1s	+300%
`rej_uniform_native_x86_64`	✅	4s	3s	+33%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	3s	3s	+0%
`mlk_gen_matrix_serial`	✅	3s	3s	+0%
`mlk_invntt_layer`	✅	3s	5s	-40%
`mlk_keccakf1600x4_xor_bytes`	✅	3s	3s	+0%
`mlk_matvec_mul`	✅	3s	4s	-25%
`mlk_poly_compress_d10_c`	✅	3s	3s	+0%
`mlk_poly_compress_d4_c`	✅	3s	2s	+50%
`mlk_poly_compress_d4_native`	✅	3s	2s	+50%
`mlk_poly_decompress_d10_c`	✅	3s	3s	+0%
`mlk_poly_decompress_du`	✅	3s	2s	+50%
`mlk_poly_getnoise_eta1_4x`	✅	3s	4s	-25%
`mlk_poly_invntt_tomont_c`	✅	3s	5s	-40%
`mlk_poly_ntt`	✅	3s	3s	+0%
`mlk_poly_tobytes_native`	✅	3s	1s	+200%
`mlk_poly_tomont`	✅	3s	2s	+50%
`mlk_polyvec_basemul_acc_montgomery_cached`	✅	3s	4s	-25%
`mlk_polyvec_decompress_du`	✅	3s	5s	-40%
`mlk_polyvec_mulcache_compute`	✅	3s	3s	+0%
`mlk_polyvec_tobytes`	✅	3s	2s	+50%
`mlk_scalar_compress_d1`	✅	3s	3s	+0%
`mlk_scalar_compress_d10`	✅	3s	2s	+50%
`mlk_scalar_compress_d11`	✅	3s	2s	+50%
`mlk_scalar_decompress_d11`	✅	3s	2s	+50%
`mlk_sha3_512`	✅	3s	4s	-25%
`mlk_shake256x4`	✅	3s	5s	-40%
`mlk_value_barrier_u32`	✅	3s	2s	+50%
`poly_decompress_d11_native_x86_64`	✅	3s	2s	+50%
`poly_decompress_d5_native_x86_64`	✅	3s	3s	+0%
`poly_invntt_tomont_native`	✅	3s	3s	+0%
`polyvec_basemul_acc_montgomery_cached_k3_native_aarch64`	✅	3s	3s	+0%
`polyvec_basemul_acc_montgomery_cached_k4_native_aarch64`	✅	3s	2s	+50%
`rej_uniform_native_aarch64`	✅	3s	2s	+50%
`intt_native_aarch64`	✅	2s	1s	+100%
`intt_native_x86_64`	✅	2s	1s	+100%
`keccakf1600x4_xor_bytes_native`	✅	2s	3s	-33%
`kem_check_sk`	✅	2s	1s	+100%
`kem_enc_derand`	✅	2s	3s	-33%
`kem_keypair`	✅	2s	3s	-33%
`mlk_barrett_reduce`	✅	2s	2s	+0%
`mlk_check_pct`	✅	2s	4s	-50%
`mlk_ct_cmask_neg_i16`	✅	2s	2s	+0%
`mlk_ct_cmask_nonzero_u8`	✅	2s	2s	+0%
`mlk_ct_cmov_zero`	✅	2s	1s	+100%
`mlk_ct_get_optblocker_i32`	✅	2s	2s	+0%
`mlk_ct_get_optblocker_u32`	✅	2s	3s	-33%
`mlk_keccakf1600_extract_bytes`	✅	2s	2s	+0%
`mlk_keccakf1600_permute`	✅	2s	4s	-50%
`mlk_keccakf1600_xor_bytes (big endian)`	✅	2s	2s	+0%
`mlk_keccakf1600x4_extract_bytes`	✅	2s	3s	-33%
`mlk_keypair_getnoise_eta1`	✅	2s	4s	-50%
`mlk_poly_cbd_eta1`	✅	2s	2s	+0%
`mlk_poly_compress_d11_c`	✅	2s	3s	-33%
`mlk_poly_compress_d11_native`	✅	2s	3s	-33%
`mlk_poly_compress_d4`	✅	2s	1s	+100%
`mlk_poly_compress_du`	✅	2s	2s	+0%
`mlk_poly_compress_dv`	✅	2s	1s	+100%
`mlk_poly_decompress_d10`	✅	2s	1s	+100%
`mlk_poly_decompress_d11`	✅	2s	1s	+100%
`mlk_poly_decompress_d11_native`	✅	2s	2s	+0%
`mlk_poly_decompress_d4`	✅	2s	1s	+100%
`mlk_poly_decompress_d4_c`	✅	2s	4s	-50%
`mlk_poly_decompress_d5_native`	✅	2s	1s	+100%
`mlk_poly_decompress_dv`	✅	2s	3s	-33%
`mlk_poly_frombytes`	✅	2s	3s	-33%
`mlk_poly_getnoise_eta2`	✅	2s	4s	-50%
`mlk_poly_mulcache_compute`	✅	2s	2s	+0%
`mlk_poly_reduce`	✅	2s	3s	-33%
`mlk_poly_reduce_c`	✅	2s	2s	+0%
`mlk_poly_sub`	✅	2s	1s	+100%
`mlk_poly_tobytes_c`	✅	2s	4s	-50%
`mlk_poly_tomont_c`	✅	2s	3s	-33%
`mlk_poly_tomont_native`	✅	2s	3s	-33%
`mlk_poly_tomsg`	✅	2s	1s	+100%
`mlk_polyvec_compress_du`	✅	2s	3s	-33%
`mlk_polyvec_frombytes`	✅	2s	3s	-33%
`mlk_polyvec_permute_bitrev_to_custom_native`	✅	2s	4s	-50%
`mlk_polyvec_reduce`	✅	2s	4s	-50%
`mlk_scalar_compress_d4`	✅	2s	1s	+100%
`mlk_scalar_decompress_d10`	✅	2s	5s	-60%
`mlk_scalar_decompress_d5`	✅	2s	1s	+100%
`mlk_sha3_256`	✅	2s	2s	+0%
`mlk_shake128_absorb_once`	✅	2s	2s	+0%
`mlk_shake128_squeezeblocks`	✅	2s	2s	+0%
`mlk_shake128x4_absorb_once`	✅	2s	2s	+0%
`mlk_shake128x4_squeezeblocks`	✅	2s	2s	+0%
`mlk_shake256`	✅	2s	1s	+100%
`poly_compress_d10_native_x86_64`	✅	2s	2s	+0%
`poly_compress_d11_native_x86_64`	✅	2s	4s	-50%
`poly_compress_d4_native_x86_64`	✅	2s	2s	+0%
`poly_compress_d5_native_x86_64`	✅	2s	3s	-33%
`poly_getnoise_eta1122_4x_native`	✅	2s	1s	+100%
`poly_reduce_native_x86_64`	✅	2s	2s	+0%
`poly_tobytes_native_aarch64`	✅	2s	3s	-33%
`poly_tobytes_native_x86_64`	✅	2s	2s	+0%
`poly_tomont_native_aarch64`	✅	2s	1s	+100%
`polyvec_basemul_acc_montgomery_cached_k2_native_aarch64`	✅	2s	1s	+100%
`polyvec_basemul_acc_montgomery_cached_k2_native_x86_64`	✅	2s	3s	-33%
`polyvec_basemul_acc_montgomery_cached_k3_native_x86_64`	✅	2s	2s	+0%
`rej_uniform_native`	✅	2s	5s	-60%
`sys_check_capability`	✅	2s	2s	+0%
`keccak_f1600_x1_native_aarch64`	✅	1s	3s	-67%
`keccak_f1600_x4_native_aarch64_v84a`	✅	1s	3s	-67%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	1s	2s	-50%
`keccak_f1600_x4_native_avx2`	✅	1s	2s	-50%
`mlk_ct_cmask_nonzero_u16`	✅	1s	2s	-50%
`mlk_ct_get_optblocker_u8`	✅	1s	1s	+0%
`mlk_ct_memcmp`	✅	1s	2s	-50%
`mlk_ct_sel_int16`	✅	1s	2s	-50%
`mlk_ct_sel_uint8`	✅	1s	4s	-75%
`mlk_keccakf1600_xor_bytes`	✅	1s	4s	-75%
`mlk_keccakf1600x4_permute`	✅	1s	2s	-50%
`mlk_montgomery_reduce`	✅	1s	3s	-67%
`mlk_poly_compress_d10_native`	✅	1s	3s	-67%
`mlk_poly_compress_d11`	✅	1s	2s	-50%
`mlk_poly_compress_d5_c`	✅	1s	1s	+0%
`mlk_poly_compress_d5_native`	✅	1s	2s	-50%
`mlk_poly_decompress_d11_c`	✅	1s	1s	+0%
`mlk_poly_decompress_d5_c`	✅	1s	1s	+0%
`mlk_poly_frombytes_c`	✅	1s	4s	-75%
`mlk_poly_getnoise_eta1122_4x`	✅	1s	3s	-67%
`mlk_poly_invntt_tomont`	✅	1s	2s	-50%
`mlk_polyvec_invntt_tomont`	✅	1s	3s	-67%
`mlk_scalar_compress_d5`	✅	1s	1s	+0%
`mlk_scalar_decompress_d4`	✅	1s	4s	-75%
`mlk_value_barrier_i32`	✅	1s	2s	-50%
`mlk_value_barrier_u8`	✅	1s	3s	-67%
`ntt_native_x86_64`	✅	1s	1s	+0%
`nttunpack_native_x86_64`	✅	1s	2s	-50%
`poly_mulcache_compute_native_x86_64`	✅	1s	1s	+0%
`poly_reduce_native_aarch64`	✅	1s	1s	+0%
`poly_tomont_native_x86_64`	✅	1s	3s	-67%
`polyvec_basemul_acc_montgomery_cached_k4_native_x86_64`	✅	1s	4s	-75%

oqs-bot · 2026-01-28T10:29:25Z

CBMC Results (ML-KEM-1024)

Full Results (187 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	1257s	1333s	-5.7%
`mlk_indcpa_enc`	✅	236s	255s	-7%
`polyvec_basemul_acc_montgomery_cached_native`	✅	122s	125s	-2%
`mlk_indcpa_keypair_derand`	✅	77s	81s	-5%
`mlk_polyvec_basemul_acc_montgomery_cached_c`	✅	69s	71s	-3%
`mlk_rej_uniform_c`	✅	65s	75s	-13%
`mlk_poly_rej_uniform`	✅	31s	34s	-9%
`poly_ntt_native`	✅	28s	33s	-15%
`mlk_keccak_squeezeblocks_x4`	✅	26s	24s	+8%
`mlk_polyvec_add`	✅	22s	28s	-21%
`keccakf1600x4_permute_native_x4`	✅	19s	23s	-17%
`mlk_poly_reduce_native`	✅	15s	16s	-6%
`mlk_ntt_layer`	✅	13s	14s	-7%
`mlk_poly_decompress_d11_native`	✅	13s	13s	+0%
`mlk_poly_decompress_d5_native`	✅	13s	12s	+8%
`mlk_polyvec_ntt`	✅	12s	12s	+0%
`mlk_indcpa_dec`	✅	10s	12s	-17%
`mlk_poly_compress_d11_c`	✅	10s	7s	+43%
`mlk_polymat_permute_bitrev_to_custom`	✅	10s	9s	+11%
`mlk_keccak_absorb_once_x4`	✅	9s	10s	-10%
`mlk_poly_rej_uniform_x4`	✅	9s	8s	+12%
`mlk_keccak_squeeze_once`	✅	8s	5s	+60%
`mlk_ntt_butterfly_block`	✅	8s	8s	+0%
`mlk_poly_frommsg`	✅	8s	12s	-33%
`mlk_fqmul`	✅	7s	7s	+0%
`mlk_gen_matrix`	✅	7s	6s	+17%
`mlk_gen_matrix_serial`	✅	7s	5s	+40%
`kem_dec`	✅	6s	6s	+0%
`mlk_keccak_squeezeblocks`	✅	6s	6s	+0%
`mlk_poly_add`	✅	6s	5s	+20%
`mlk_poly_frombytes_native`	✅	6s	9s	-33%
`mlk_shake256x4`	✅	6s	4s	+50%
`mlk_invntt_layer`	✅	5s	4s	+25%
`mlk_poly_mulcache_compute_c`	✅	5s	3s	+67%
`mlk_polyvec_tobytes`	✅	5s	3s	+67%
`poly_compress_d5_native_x86_64`	✅	5s	2s	+150%
`polyvec_basemul_acc_montgomery_cached_k2_native_aarch64`	✅	5s	1s	+400%
`keccakf1600_permute_native`	✅	4s	5s	-20%
`keccakf1600x4_xor_bytes_native`	✅	4s	4s	+0%
`kem_check_pk`	✅	4s	6s	-33%
`mlk_barrett_reduce`	✅	4s	4s	+0%
`mlk_keccakf1600_xor_bytes (big endian)`	✅	4s	2s	+100%
`mlk_matvec_mul`	✅	4s	2s	+100%
`mlk_poly_getnoise_eta1_4x`	✅	4s	5s	-20%
`mlk_poly_getnoise_eta1_4x_native`	✅	4s	4s	+0%
`mlk_poly_tobytes`	✅	4s	2s	+100%
`mlk_scalar_decompress_d5`	✅	4s	4s	+0%
`mlk_shake128_absorb_once`	✅	4s	1s	+300%
`poly_decompress_d5_native_x86_64`	✅	4s	5s	-20%
`poly_frombytes_native_x86_64`	✅	4s	4s	+0%
`poly_mulcache_compute_native_x86_64`	✅	4s	3s	+33%
`poly_tobytes_native_aarch64`	✅	4s	3s	+33%
`poly_tobytes_native_x86_64`	✅	4s	3s	+33%
`polyvec_basemul_acc_montgomery_cached_k2_native_x86_64`	✅	4s	4s	+0%
`rej_uniform_native_aarch64`	✅	4s	1s	+300%
`rej_uniform_native_x86_64`	✅	4s	3s	+33%
`intt_native_x86_64`	✅	3s	1s	+200%
`keccak_f1600_x1_native_aarch64_v84a`	✅	3s	2s	+50%
`keccakf1600x4_extract_bytes_native`	✅	3s	2s	+50%
`kem_check_sk`	✅	3s	2s	+50%
`kem_enc`	✅	3s	2s	+50%
`kem_enc_derand`	✅	3s	4s	-25%
`kem_keypair`	✅	3s	3s	+0%
`kem_keypair_derand`	✅	3s	3s	+0%
`mlk_check_pct`	✅	3s	4s	-25%
`mlk_ct_cmask_neg_i16`	✅	3s	2s	+50%
`mlk_ct_get_optblocker_u8`	✅	3s	3s	+0%
`mlk_ct_sel_int16`	✅	3s	2s	+50%
`mlk_keccak_absorb_once`	✅	3s	4s	-25%
`mlk_keccakf1600_xor_bytes`	✅	3s	2s	+50%
`mlk_poly_compress_d10_c`	✅	3s	2s	+50%
`mlk_poly_compress_d11_native`	✅	3s	2s	+50%
`mlk_poly_compress_d4_native`	✅	3s	2s	+50%
`mlk_poly_compress_d5`	✅	3s	1s	+200%
`mlk_poly_compress_d5_c`	✅	3s	1s	+200%
`mlk_poly_decompress_d4_native`	✅	3s	2s	+50%
`mlk_poly_decompress_d5_c`	✅	3s	2s	+50%
`mlk_poly_decompress_du`	✅	3s	1s	+200%
`mlk_poly_reduce_c`	✅	3s	2s	+50%
`mlk_poly_tobytes_c`	✅	3s	2s	+50%
`mlk_poly_tobytes_native`	✅	3s	2s	+50%
`mlk_poly_tomsg`	✅	3s	5s	-40%
`mlk_polyvec_permute_bitrev_to_custom_native`	✅	3s	4s	-25%
`mlk_scalar_compress_d1`	✅	3s	2s	+50%
`mlk_scalar_compress_d4`	✅	3s	3s	+0%
`mlk_scalar_decompress_d10`	✅	3s	2s	+50%
`mlk_sha3_512`	✅	3s	2s	+50%
`mlk_value_barrier_u32`	✅	3s	2s	+50%
`poly_decompress_d11_native_x86_64`	✅	3s	4s	-25%
`intt_native_aarch64`	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64`	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v84a`	✅	2s	4s	-50%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	2s	3s	-33%
`keccak_f1600_x4_native_avx2`	✅	2s	1s	+100%
`mlk_ct_cmov_zero`	✅	2s	1s	+100%
`mlk_ct_get_optblocker_u32`	✅	2s	2s	+0%
`mlk_ct_memcmp`	✅	2s	2s	+0%
`mlk_ct_sel_uint8`	✅	2s	2s	+0%
`mlk_keccakf1600_extract_bytes`	✅	2s	2s	+0%
`mlk_keccakf1600_extract_bytes (big endian)`	✅	2s	2s	+0%
`mlk_keccakf1600_permute`	✅	2s	2s	+0%
`mlk_keccakf1600x4_extract_bytes`	✅	2s	2s	+0%
`mlk_keccakf1600x4_permute`	✅	2s	4s	-50%
`mlk_keccakf1600x4_xor_bytes`	✅	2s	2s	+0%
`mlk_montgomery_reduce`	✅	2s	2s	+0%
`mlk_poly_cbd_eta1`	✅	2s	7s	-71%
`mlk_poly_cbd_eta2`	✅	2s	5s	-60%
`mlk_poly_compress_d10`	✅	2s	1s	+100%
`mlk_poly_compress_d10_native`	✅	2s	3s	-33%
`mlk_poly_compress_d11`	✅	2s	1s	+100%
`mlk_poly_compress_d4`	✅	2s	1s	+100%
`mlk_poly_compress_d5_native`	✅	2s	3s	-33%
`mlk_poly_compress_du`	✅	2s	2s	+0%
`mlk_poly_compress_dv`	✅	2s	3s	-33%
`mlk_poly_decompress_d10`	✅	2s	2s	+0%
`mlk_poly_decompress_d10_native`	✅	2s	2s	+0%
`mlk_poly_decompress_d11`	✅	2s	5s	-60%
`mlk_poly_decompress_d4`	✅	2s	1s	+100%
`mlk_poly_decompress_d4_c`	✅	2s	4s	-50%
`mlk_poly_decompress_d5`	✅	2s	4s	-50%
`mlk_poly_frombytes`	✅	2s	4s	-50%
`mlk_poly_frombytes_c`	✅	2s	3s	-33%
`mlk_poly_getnoise_eta1122_4x`	✅	2s	2s	+0%
`mlk_poly_invntt_tomont`	✅	2s	3s	-33%
`mlk_poly_invntt_tomont_c`	✅	2s	2s	+0%
`mlk_poly_mulcache_compute_native`	✅	2s	3s	-33%
`mlk_poly_ntt`	✅	2s	2s	+0%
`mlk_poly_ntt_c`	✅	2s	3s	-33%
`mlk_poly_reduce`	✅	2s	2s	+0%
`mlk_poly_tomont`	✅	2s	3s	-33%
`mlk_polyvec_basemul_acc_montgomery_cached`	✅	2s	2s	+0%
`mlk_polyvec_compress_du`	✅	2s	3s	-33%
`mlk_polyvec_decompress_du`	✅	2s	2s	+0%
`mlk_polyvec_frombytes`	✅	2s	2s	+0%
`mlk_polyvec_invntt_tomont`	✅	2s	3s	-33%
`mlk_polyvec_mulcache_compute`	✅	2s	1s	+100%
`mlk_polyvec_reduce`	✅	2s	4s	-50%
`mlk_polyvec_tomont`	✅	2s	3s	-33%
`mlk_rej_uniform`	✅	2s	3s	-33%
`mlk_scalar_compress_d10`	✅	2s	2s	+0%
`mlk_scalar_compress_d11`	✅	2s	1s	+100%
`mlk_scalar_compress_d5`	✅	2s	1s	+100%
`mlk_scalar_decompress_d4`	✅	2s	2s	+0%
`mlk_shake128_squeezeblocks`	✅	2s	1s	+100%
`mlk_shake256`	✅	2s	3s	-33%
`mlk_value_barrier_u8`	✅	2s	1s	+100%
`ntt_native_aarch64`	✅	2s	2s	+0%
`ntt_native_x86_64`	✅	2s	2s	+0%
`poly_compress_d11_native_x86_64`	✅	2s	2s	+0%
`poly_compress_d4_native_x86_64`	✅	2s	1s	+100%
`poly_decompress_d10_native_x86_64`	✅	2s	2s	+0%
`poly_decompress_d4_native_x86_64`	✅	2s	2s	+0%
`poly_getnoise_eta1122_4x_native`	✅	2s	2s	+0%
`poly_invntt_tomont_native`	✅	2s	3s	-33%
`poly_mulcache_compute_native_aarch64`	✅	2s	4s	-50%
`poly_reduce_native_aarch64`	✅	2s	1s	+100%
`poly_reduce_native_x86_64`	✅	2s	3s	-33%
`poly_tomont_native_x86_64`	✅	2s	4s	-50%
`polyvec_basemul_acc_montgomery_cached_k3_native_x86_64`	✅	2s	4s	-50%
`polyvec_basemul_acc_montgomery_cached_k4_native_aarch64`	✅	2s	3s	-33%
`polyvec_basemul_acc_montgomery_cached_k4_native_x86_64`	✅	2s	3s	-33%
`sys_check_capability`	✅	2s	2s	+0%
`mlk_ct_cmask_nonzero_u16`	✅	1s	2s	-50%
`mlk_ct_cmask_nonzero_u8`	✅	1s	1s	+0%
`mlk_ct_get_optblocker_i32`	✅	1s	4s	-75%
`mlk_keypair_getnoise_eta1`	✅	1s	3s	-67%
`mlk_poly_compress_d4_c`	✅	1s	1s	+0%
`mlk_poly_decompress_d10_c`	✅	1s	1s	+0%
`mlk_poly_decompress_d11_c`	✅	1s	3s	-67%
`mlk_poly_decompress_dv`	✅	1s	3s	-67%
`mlk_poly_getnoise_eta2`	✅	1s	2s	-50%
`mlk_poly_mulcache_compute`	✅	1s	2s	-50%
`mlk_poly_sub`	✅	1s	3s	-67%
`mlk_poly_tomont_c`	✅	1s	2s	-50%
`mlk_poly_tomont_native`	✅	1s	1s	+0%
`mlk_polyvec_permute_bitrev_to_custom`	✅	1s	1s	+0%
`mlk_scalar_decompress_d11`	✅	1s	3s	-67%
`mlk_scalar_signed_to_unsigned_q`	✅	1s	2s	-50%
`mlk_sha3_256`	✅	1s	3s	-67%
`mlk_shake128x4_absorb_once`	✅	1s	4s	-75%
`mlk_shake128x4_squeezeblocks`	✅	1s	2s	-50%
`mlk_value_barrier_i32`	✅	1s	2s	-50%
`nttunpack_native_x86_64`	✅	1s	3s	-67%
`poly_compress_d10_native_x86_64`	✅	1s	1s	+0%
`poly_tomont_native_aarch64`	✅	1s	2s	-50%
`polyvec_basemul_acc_montgomery_cached_k3_native_aarch64`	✅	1s	3s	-67%
`rej_uniform_native`	✅	1s	4s	-75%

Add the clean (non-optimized) Keccak x4 assembly and Makefile to enable regeneration of the SLOTHY-optimized assembly. Extend autogen --slothy to support new function, and also add --slothy armv81m and --slothy aarch64 group options. Update CI to only run aarch64 SLOTHY targets. Optimization of Armv8.1-M assembly is not currently tested in CI, but has been tested locally. Update SLOTHY to version 0.1.10 as the code requires disabling the address offset fixup which is not supported for Armv8.1-M in the older versionf of SLOTHY. Co-Authored-By: Brendan Moran <brendan.moran@arm.com> Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>

mkannwischer · 2026-04-02T09:59:42Z

+.global MLK_ASM_NAMESPACE(keccak_f1600_x4_mve_asm)
+MLK_ASM_FN_SYMBOL(keccak_f1600_x4_mve_asm)
+
+    push {r3,r4,r5,r6,r7,r8,r9,r10,r11,r12,lr}


This actually got changed in #1558 - we should align that once it gets merged.

The x4 MVE Keccak permutation no longer needs to preserve r3 or r12 across the function body, so remove them from the saved core register set in the prologue and epilogue. Update the ABI stack metadata in the symbolic/source assembly and generated mlkem copy to reflect the reduced 228-byte frame. This aligns the x4 implementation with the stack usage expected by #1558. Signed-off-by: Brendan Moran <brendan.moran@arm.com>

hanno-becker · 2026-06-14T05:06:07Z

 stdenvNoCC.mkDerivation rec {
  pname = "slothy-cli";
-  version = "915c224166207ce07b31152194305c3b6687d09b";
+  version = "0.1.10";


Is this still the right version to update to?

No. we should take 0.2.2

hanno-becker · 2026-06-14T05:07:03Z

@@ -4175,6 +4177,11 @@ def _main():
        "keccak_f1600_x4_v8a_scalar_hybrid_asm",
        "keccak_f1600_x4_v8a_v84a_scalar_hybrid_asm",
    ]
+    slothy_armv81m_targets = [
+        "keccak_f1600_x4_mve",
+    ]
+    slothy_all_targets = slothy_aarch64_targets + slothy_armv81m_targets
+    slothy_choices = slothy_all_targets + ["aarch64", "armv81m"]


Can we explicitly prefix the targets with the architecture? E.g. --slothy aarch64/* mve/*?

hanno-becker

We need a CI job which re-runs SLOTHY on the MVE kernel and then runs the baremetal tests.

mkannwischer force-pushed the slothy-keccak-x4-mve branch from c1dfb78 to bb4c3a4 Compare January 28, 2026 09:40

mkannwischer marked this pull request as ready for review January 28, 2026 10:19

mkannwischer requested a review from a team as a code owner January 28, 2026 10:19

mkannwischer force-pushed the slothy-keccak-x4-mve branch from bb4c3a4 to d0a737c Compare April 2, 2026 09:58

mkannwischer commented Apr 2, 2026

View reviewed changes

mkannwischer assigned hanno-becker Apr 2, 2026

hanno-becker reviewed Jun 14, 2026

View reviewed changes

hanno-becker requested changes Jun 14, 2026

View reviewed changes

hanno-becker assigned mkannwischer and unassigned hanno-becker Jun 18, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Armv8.1-M: Add clean x4 Keccak code and SLOTHY Makefile#1527

Armv8.1-M: Add clean x4 Keccak code and SLOTHY Makefile#1527
mkannwischer wants to merge 2 commits into
mainfrom
slothy-keccak-x4-mve

mkannwischer commented Jan 28, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Jan 28, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Jan 28, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Jan 28, 2026 •

edited

Loading

Uh oh!

mkannwischer Apr 2, 2026

Uh oh!

hanno-becker Jun 14, 2026

Uh oh!

mkannwischer Jun 14, 2026

Uh oh!

hanno-becker Jun 14, 2026

Uh oh!

hanno-becker left a comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

CBMC Results (ML-KEM-768)

Uh oh!

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

Uh oh!

CBMC Results (ML-KEM-512)

Uh oh!

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

Uh oh!

CBMC Results (ML-KEM-1024)

Uh oh!

mkannwischer Apr 2, 2026

Choose a reason for hiding this comment

Uh oh!

hanno-becker Jun 14, 2026

Choose a reason for hiding this comment

Uh oh!

mkannwischer Jun 14, 2026

Choose a reason for hiding this comment

Uh oh!

hanno-becker Jun 14, 2026

Choose a reason for hiding this comment

Uh oh!

hanno-becker left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

mkannwischer commented Jan 28, 2026 •

edited

Loading

oqs-bot commented Jan 28, 2026 •

edited

Loading

oqs-bot commented Jan 28, 2026 •

edited

Loading

oqs-bot commented Jan 28, 2026 •

edited

Loading