diff --git a/arch/rv32i/src/pmp.rs b/arch/rv32i/src/pmp.rs
index a5ba5d8ec5..a19c8282a2 100644
--- a/arch/rv32i/src/pmp.rs
+++ b/arch/rv32i/src/pmp.rs
@@ -98,6 +98,7 @@ impl From<mpu::Permissions> for TORUserPMPCFG {
 
 /// A RISC-V PMP memory region specification, configured in NAPOT mode.
 ///
+/// // VTOCK-TODO: (samir) should add refinements for these properties
 /// This type checks that the supplied `start` and `size` values meet the RISC-V
 /// NAPOT requirements, namely that
 ///
@@ -110,22 +111,28 @@ impl From<mpu::Permissions> for TORUserPMPCFG {
 /// [`NAPOTRegionSpec::napot_addr`] convenience method to retrieve an `pmpaddrX`
 /// CSR value encoding this region's address and length.
 #[derive(Copy, Clone, Debug)]
-// #[flux::refined_by(a: u32)]
+#[flux::refined_by(size: int)]
 pub struct NAPOTRegionSpec {
     start: *const u8,
-    // #[flux::field({ u32[a] | a > 0 })]
+    #[flux::field({ usize[size] | size > 0 })]
     size: usize,
 }
-
-#[flux::ignore]
+#[flux::sig(fn(b:bool) ensures b)]
+pub fn assume(b: bool) {
+    if !b {
+        panic!("assume fails")
+    }
+}
+// #[flux::ignore]
 impl NAPOTRegionSpec {
     /// Construct a new [`NAPOTRegionSpec`]
     ///
     /// This method accepts a `start` address and a region length. It returns
     /// `Some(region)` when all constraints specified in the
     /// [`NAPOTRegionSpec`]'s documentation are satisfied, otherwise `None`.
-    #[flux::ignore]
+    // #[flux::ignore]
     pub fn new(start: *const u8, size: usize) -> Option<Self> {
+        assume(size > 0); // I thought the struct has already refined this property?
         if !size.is_power_of_two() || (start as usize) % size != 0 || size < 8 {
             None
         } else {
@@ -213,7 +220,7 @@ impl TORRegionSpec {
 /// ranges.
 // #[flux::sig(fn() -> usize{v: v < FORTY_TWO})]
 // Other size should be > 0
-#[flux::ignore]
+// #[flux::ignore]
 fn region_overlaps(
     region: &(TORUserPMPCFG, *const u8, *const u8),
     other_start: *const u8,
@@ -242,14 +249,16 @@ fn region_overlaps(
     // This implementation is simple and stupid, and can be optimized. We leave
     // that as an exercise to the compiler.
 
-    let end = region_range.end - 1;
+    if (region_range.start < region_range.end) && (other_range.start < other_range.end) {
+        let end = region_range.end - 1;
 
-    !region_range.is_empty()
-        && !other_range.is_empty()
-        && (region_range.contains(&other_range.start)
+        region_range.contains(&other_range.start)
             || region_range.contains(&(other_range.end - 1))
             || other_range.contains(&region_range.start)
-            || other_range.contains(&(end)))
+            || other_range.contains(&(end))
+    } else {
+        false
+    }
 }
 
 /// Print a table of the configured PMP regions, read from  the HW CSRs.
@@ -490,8 +499,8 @@ pub trait TORUserPMP<const MAX_REGIONS: usize> {
 }
 
 /// Struct storing userspace memory protection regions for the [`PMPUserMPU`].
-// #[flux::invariant(MAX_REGIONS > 0)]
-// #[flux::invariant(MAX_REGIONS <= 16)]
+// VTOCK-TODO: This invariant should be fixed, pending const generic issues with flux
+// #[flux::invariant(MAX_REGIONS > 0 && MAX_REGIONS <= 16)]
 pub struct PMPUserMPUConfig<const MAX_REGIONS: usize> {
     /// PMP config identifier, as generated by the issuing PMP implementation.
     id: NonZeroUsize,
@@ -499,7 +508,7 @@ pub struct PMPUserMPUConfig<const MAX_REGIONS: usize> {
     /// written to hardware.
     is_dirty: Cell<bool>,
     /// Array of MPU regions. Each region requires two physical PMP entries.
-    // #[flux::field({ ? | MAX_REGIONS > 0 })]
+    // #[flux::field({NonZeroUsize | MAX_REGIONS > 0 && MAX_REGIONS <= 16})]
     regions: [(TORUserPMPCFG, *const u8, *const u8); MAX_REGIONS],
     /// Which region index (into the `regions` array above) is used
     /// for app memory (if it has been configured).