From a9ca3d5cd98c89510109610873bbaed1beeda737 Mon Sep 17 00:00:00 2001
From: Tony Arcieri <bascule@gmail.com>
Date: Thu, 29 Oct 2026 10:18:18 -0600
Subject: [PATCH] ml-kem: partial `riscv32` support for `cargo checkct`

The others seem to be some sort of combinatorial explosion in the
analysis that are causing it to fail. This at least enables the checks
on a 32-bit RISC-V target, but disables the ones that aren't currently
working until we're able to better understand why.
---
 ml-kem/checkct/.cargo/config.toml   | 3 +--
 ml-kem/checkct/driver/src/driver.rs | 7 ++++++-
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/ml-kem/checkct/.cargo/config.toml b/ml-kem/checkct/.cargo/config.toml
index 969ef51..aeb3543 100644
--- a/ml-kem/checkct/.cargo/config.toml
+++ b/ml-kem/checkct/.cargo/config.toml
@@ -1,7 +1,6 @@
 [build]
 target = [
-    # TODO(tarcieri): full encapsulation exceeds analysis budget on `riscv32`
-    # "riscv32imac-unknown-none-elf",
+    "riscv32imac-unknown-none-elf",
     "thumbv6m-none-eabi",
     "thumbv7em-none-eabihf",
     "x86_64-unknown-linux-gnu",
diff --git a/ml-kem/checkct/driver/src/driver.rs b/ml-kem/checkct/driver/src/driver.rs
index 742af35..797d349 100644
--- a/ml-kem/checkct/driver/src/driver.rs
+++ b/ml-kem/checkct/driver/src/driver.rs
@@ -1,12 +1,15 @@
 use crate::rng::{PrivateRng, PublicRng};
 use checkct_macros::checkct;
 use core::hint::black_box;
-use ml_kem::{B32, EncapsulationKey};
 
 macro_rules! check_encapsulation {
     ($name:ident, $kem:ident, $key_len:expr) => {
+        // TODO: enable on RISC-V once full encapsulation fits the analysis budget.
+        #[cfg(not(target_arch = "riscv32"))]
         #[checkct]
         pub fn $name() {
+            use ml_kem::{B32, EncapsulationKey};
+
             // The generated BINSEC script references both RNG hooks.
             black_box(PublicRng.next_u32());
 
@@ -45,6 +48,8 @@ pub fn small_reduce_u32() {
 // Expanded-key import avoids treating key generation's public rho as secret.
 macro_rules! check_decapsulation {
     ($name:ident, $kem:ident, $sk_len:expr, $fixture:literal) => {
+        // TODO: enable on RISC-V once full decapsulation fits the analysis budget.
+        #[cfg(not(target_arch = "riscv32"))]
         #[checkct]
         #[allow(deprecated)]
         pub fn $name() {