Add const_assume and check some conditions at compile-time

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(),

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

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) {}