From 5a1ebc08e3458ae3267f7007c269b7f6e4c715b2 Mon Sep 17 00:00:00 2001
From: Nico Lehmann <nico.lehmannm@gmail.com>
Date: Tue, 19 Aug 2025 16:08:23 -0700
Subject: [PATCH] Add const_assume and check some conditions at compile-time

---
 arch/cortex-m/src/mpu.rs | 2 +-
 arch/rv32i/src/pmp.rs    | 6 +++---
 flux_support/src/lib.rs  | 8 ++++++++
 3 files changed, 12 insertions(+), 4 deletions(-)

diff --git a/arch/cortex-m/src/mpu.rs b/arch/cortex-m/src/mpu.rs
index 64dd4ee3aa..00cdb678db 100644
--- a/arch/cortex-m/src/mpu.rs
+++ b/arch/cortex-m/src/mpu.rs
@@ -150,7 +150,7 @@ pub struct MPU<const NUM_REGIONS: usize, const MIN_REGION_SIZE: usize> {
 
 impl<const NUM_REGIONS: usize, const MIN_REGION_SIZE: usize> MPU<NUM_REGIONS, MIN_REGION_SIZE> {
     pub const unsafe fn new() -> Self {
-        assume(NUM_REGIONS == 8 || NUM_REGIONS == 16); // TODO: const-generic
+        flux_support::const_assume!(NUM_REGIONS == 8 || NUM_REGIONS == 16);
         Self {
             registers: MPU_BASE_ADDRESS,
             hardware_is_configured_for: OptionalCell::empty(),
diff --git a/arch/rv32i/src/pmp.rs b/arch/rv32i/src/pmp.rs
index 08e781f09b..99cb9a9f89 100644
--- a/arch/rv32i/src/pmp.rs
+++ b/arch/rv32i/src/pmp.rs
@@ -1777,7 +1777,7 @@ pub mod simple {
             // establish some verification specific details
             let mut hardware_state = HardwareState::new();
             all_available_regions_setup_up_to_base(&hardware_state);
-            flux_support::assume(AVAILABLE_ENTRIES > 0); // TODO: const-generic
+            flux_support::const_assume!(AVAILABLE_ENTRIES > 0);
 
             configure_initial_pmp_tail(0, &mut hardware_state, AVAILABLE_ENTRIES)?;
 
@@ -2176,7 +2176,7 @@ pub mod kernel_protection {
                 );
             }
 
-            flux_support::assume(AVAILABLE_ENTRIES >= 7); // TODO: const-generic
+            flux_support::const_assume!(AVAILABLE_ENTRIES >= 7);
 
             // Set the kernel `.text`, flash, RAM and MMIO regions, in no
             // particular order, with the exception of `.text` and flash:
@@ -2684,7 +2684,7 @@ pub mod kernel_protection_mml_epmp {
                 );
             }
 
-            flux_support::assume(AVAILABLE_ENTRIES >= 3); // TODO: const-generic
+            flux_support::const_assume!(AVAILABLE_ENTRIES >= 3);
             // Set the kernel `.text`, flash, RAM and MMIO regions, in no
             // particular order, with the exception of `.text` and flash:
             // `.text` must precede flash, as otherwise we'd be revoking execute
diff --git a/flux_support/src/lib.rs b/flux_support/src/lib.rs
index 2eedc00953..610aee8556 100644
--- a/flux_support/src/lib.rs
+++ b/flux_support/src/lib.rs
@@ -15,6 +15,14 @@ pub use flux_range::*;
 pub use flux_register_interface::*;
 pub use math::*;
 
+#[macro_export]
+macro_rules! const_assume {
+    ($cond:expr) => {
+        const { assert!($cond) };
+        $crate::assume($cond);
+    }
+}
+
 #[allow(dead_code)]
 #[flux_rs::sig(fn(x: bool[true]))]
 pub const fn assert(_x: bool) {}