Skip to content

Port Baremetal: Add Cortex-M33 MPS3-AN524 platform support#1579

Draft
willieyz wants to merge 2 commits intomainfrom
port-m33-an524
Draft

Port Baremetal: Add Cortex-M33 MPS3-AN524 platform support#1579
willieyz wants to merge 2 commits intomainfrom
port-m33-an524

Conversation

@willieyz
Copy link
Copy Markdown
Contributor

@willieyz willieyz commented Feb 25, 2026 •
edited
Loading

Add bare-metal platform support for ARM Cortex-M33 on MPS3-AN524 FPGA. Works on both QEMU (qemu-system-arm -M mps3-an524) and real hardware.

Notice that the configuration ML*_CONFIG_REDUCE_RAM did not implement in mlkem-native, we skip this option during this porting.

  • CMSIS patches for AN524 board configuration
  • UART driver at 0x41303000 (32 MHz, 115200 baud)
  • Memory: 512KB Flash @ 0x10000000, 128KB SRAM @ 0x20000000
  • 96KB stack for ML-DSA-87 support
  • CI integration for automated testing

@willieyz willieyz force-pushed the port-m33-an524 branch 3 times, most recently from a61e82c to bae13fa Compare February 25, 2026 13:21
@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Feb 25, 2026 •
edited
Loading

CBMC Results (ML-KEM-512)

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

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Feb 25, 2026 •
edited
Loading

CBMC Results (ML-KEM-768)

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

@willieyz willieyz force-pushed the port-m33-an524 branch 3 times, most recently from aca0c50 to 23ae351 Compare February 25, 2026 15:04
@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Feb 25, 2026 •
edited
Loading

CBMC Results (ML-KEM-1024)

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

@willieyz willieyz force-pushed the port-m33-an524 branch 8 times, most recently from 9510d04 to 6a14b70 Compare March 3, 2026 09:06
@willieyz
Port: Baremetal: Add Cortex-M33 MPS3-AN524 platform support
1a2628f 
Add bare-metal platform support for Cortex-M33 on MPS3-AN524,
tested via qemu (qemu-system-arm -M mps3-an524).
Notice that the configuration *_CONFIG_REDUCE_RAM did not implement in
mlkem-native, we skip this option during this porting.

- Add platform makefile and qemu exec wrapper for M33-AN524
- Platform files are provided by pqmx, see slothy-optimizer/pqmx#116
- Add Cortex-M33 DWT cycle counter support in HAL
  (distinct from Cortex-M55 PMU-based counting)
- Generalize Nix package from m55-an547 to pqmx to serve
  both M55-AN547 and M33-AN524 platforms
- Allow MLD_BUMP_ALLOC_SIZE to be overridden at compile time
  (we only have a  96 KiB stack)
- Add M33 baremetal test to CI matrix

Signed-off-by: willieyz <willie.zhao@chelpis.com>
@willieyz
Debug: Adding sp address printing for debug the HardFaultHandler problem
1f8ccbe 
Signed-off-by: willieyz <willie.zhao@chelpis.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Port: Baremetal: Add Cortex-M33 MPS3-AN524 platform support

2 participants

@willieyz @oqs-bot