diff --git a/arch/cortex-m/src/lib.rs b/arch/cortex-m/src/lib.rs
index 9c7178e7035..8a9cefe9f2c 100644
--- a/arch/cortex-m/src/lib.rs
+++ b/arch/cortex-m/src/lib.rs
@@ -32,7 +32,7 @@ pub mod syscall;
 pub mod systick;
 
 pub mod mpu;
-mod tcb;
+pub(crate) mod tcb;
 
 // These constants are defined in the linker script.
 extern "C" {
diff --git a/arch/cortex-m/src/mpu.rs b/arch/cortex-m/src/mpu.rs
index 339a49522b3..373fd7d3028 100644
--- a/arch/cortex-m/src/mpu.rs
+++ b/arch/cortex-m/src/mpu.rs
@@ -22,6 +22,17 @@ use kernel::utilities::math;
 use kernel::utilities::registers::interfaces::{Readable, Writeable};
 use kernel::utilities::registers::{FieldValue, ReadOnly, ReadWrite};
 
+flux_rs::defs! {
+    use flux_support::{flux_ptr::valid_size, flux_register_interface::bv32};
+    use crate::tcb::defs::{
+        rbar_region_number, rbar_region_start, rbar_valid_bit_set, rasr_global_region_enabled, rasr_region_size, 
+        first_subregion_from_logical, last_subregion_from_logical, 
+        subregions_enabled_exactly, subregions_enabled_bit_set, subregions_disabled_bit_set, 
+        perms_match_exactly, enabled_srd_mask, half_max, pow2, aligned, exp2, octet, least_five_bits,
+        region_overlaps
+    };
+}
+
 extern crate flux_core;
 /// MPU Registers for the Cortex-M3, Cortex-M4 and Cortex-M7 families
 /// Described in section 4.5 of
diff --git a/arch/cortex-m/src/tcb/defs.rs b/arch/cortex-m/src/tcb/defs.rs
index 5a52ff12213..4f95ff78efa 100644
--- a/arch/cortex-m/src/tcb/defs.rs
+++ b/arch/cortex-m/src/tcb/defs.rs
@@ -4,10 +4,10 @@ use kernel::platform::mpu;
 
 /* our actual flux defs */
 flux_rs::defs! {
-    fn valid_size(x: int) -> bool { 0 <= x && x <= u32::MAX }
+    use flux_support::{flux_register_interface::bv32, flux_ptr::valid_size};
+
     fn half_max(r: int) -> bool { r <= u32::MAX / 2 + 1}
 
-    fn bv32(x:int) -> bitvec<32> { bv_int_to_bv32(x) }
     fn bit(reg: bitvec<32>, power_of_two: bitvec<32>) -> bool { reg & power_of_two != 0}
     fn extract(reg: bitvec<32>, mask:int, offset: int) -> bitvec<32> { (reg & bv32(mask)) >> bv32(offset) }
 
diff --git a/arch/cortex-m/src/tcb/math.rs b/arch/cortex-m/src/tcb/math.rs
index eba76aae34a..fb12e4323fd 100644
--- a/arch/cortex-m/src/tcb/math.rs
+++ b/arch/cortex-m/src/tcb/math.rs
@@ -1,5 +1,11 @@
  use flux_support::FluxPtrU8;
 
+flux_rs::defs! {
+    use flux_support::{flux_ptr::valid_size, flux_register_interface::bv32};
+    use crate::tcb::defs::{pow2, exp2, enabled_srd_mask, least_five_bits, aligned, to_pow2, half_max};
+}
+
+
 #[flux_rs::trusted(reason = "bitwise arith")]
 #[flux_rs::sig(fn(num: u32) -> u32{r: (r < 32) && (num > 1 => r > 0) && (pow2(num) => (bv32(num) == exp2(bv32(r))))})]
 pub fn log_base_two(num: u32) -> u32 {
diff --git a/arch/cortex-m/src/tcb/theorems.rs b/arch/cortex-m/src/tcb/theorems.rs
index 0a12808c8a5..86b40940c7a 100644
--- a/arch/cortex-m/src/tcb/theorems.rs
+++ b/arch/cortex-m/src/tcb/theorems.rs
@@ -2,6 +2,14 @@
 use crate::mpu::RegionAttributes;
 use flux_support::{FieldValueU32, FluxPtr};
 
+flux_rs::defs! {
+    use flux_support::flux_register_interface::bv32;
+    use crate::tcb::defs::{
+        aligned, pow2, least_five_bits, octet, last_subregion_from_logical, subregions_disabled_bit_set, to_pow2,
+        first_subregion_from_logical, enabled_srd_mask, disabled_srd_mask,
+    };
+}
+
 /* a bunch of theorems and proof code */
 #[flux_rs::reveal(aligned)]
 #[flux_rs::sig(fn (usize[@x], usize[@y]) requires x > 0 && aligned(x, y) ensures x >= y)]
diff --git a/arch/rv32i/src/pmp.rs b/arch/rv32i/src/pmp.rs
index b4ec93541d3..a9698ccab08 100644
--- a/arch/rv32i/src/pmp.rs
+++ b/arch/rv32i/src/pmp.rs
@@ -17,8 +17,7 @@ use kernel::utilities::cells::OptionalCell;
 use kernel::utilities::registers::FieldValue;
 
 flux_rs::defs! {
-
-    fn valid_size(x: int) -> bool { 0 <= x && x <= u32::MAX }
+    use flux_support::flux_ptr::valid_size;
 
     fn is_empty(r: PMPUserRegion) -> bool {
         r.start >= r.end
@@ -1624,6 +1623,7 @@ pub mod simple {
     }
 
     flux_rs::defs! {
+        use super::{extract, bit, all_regions_configured_correctly_up_to};
 
         fn available_region_setup(i: int, old: HardwareState, new: HardwareState) -> bool {
             let cfg = map_select(new.pmpcfg_registers, i / 4);
diff --git a/flux_support/src/lib.rs b/flux_support/src/lib.rs
index 6aa9e5ceed1..bd4f6fad423 100644
--- a/flux_support/src/lib.rs
+++ b/flux_support/src/lib.rs
@@ -3,9 +3,9 @@
 mod extern_specs;
 mod flux_arr;
 mod flux_pair;
-mod flux_ptr;
+pub mod flux_ptr;
 mod flux_range;
-mod flux_register_interface;
+pub mod flux_register_interface;
 mod math;
 use core::panic;
 pub use flux_arr::*;
diff --git a/kernel/src/allocator.rs b/kernel/src/allocator.rs
index 48cdf15847d..bb9db8500bb 100644
--- a/kernel/src/allocator.rs
+++ b/kernel/src/allocator.rs
@@ -7,6 +7,10 @@ use crate::{
     process::{Error, ProcessCustomGrantIdentifier},
 };
 
+flux_rs::defs! {
+    use flux_support::flux_ptr::valid_size;
+}
+
 pub(crate) enum AllocateAppMemoryError {
     HeapError,
     FlashError,
diff --git a/kernel/src/grant.rs b/kernel/src/grant.rs
index d086ef6e8f1..4061b00926f 100644
--- a/kernel/src/grant.rs
+++ b/kernel/src/grant.rs
@@ -142,6 +142,10 @@ use crate::ErrorCode;
 #[allow(clippy::wildcard_imports)]
 use flux_support::*;
 
+flux_rs::defs! {
+    use flux_support::flux_ptr::valid_size;
+}
+
 /// Tracks how many upcalls a grant instance supports automatically.
 pub trait UpcallSize {
     /// The number of upcalls the grant supports.
diff --git a/kernel/src/platform/mpu.rs b/kernel/src/platform/mpu.rs
index e973fc9d7d0..92933a31cc9 100644
--- a/kernel/src/platform/mpu.rs
+++ b/kernel/src/platform/mpu.rs
@@ -10,9 +10,7 @@ use flux_support::capability::*;
 use flux_support::*;
 
 flux_rs::defs! {
-    fn valid_size(x: int) -> bool {
-        0 <= x && x <= u32::MAX
-    }
+    use flux_support::flux_ptr::valid_size;
 }
 
 #[derive(Copy, Clone, Debug)]
diff --git a/kernel/src/process.rs b/kernel/src/process.rs
index e162fd74d90..185eb7e1975 100644
--- a/kernel/src/process.rs
+++ b/kernel/src/process.rs
@@ -35,6 +35,10 @@ pub use crate::process_policies::ProcessFaultPolicy;
 pub use crate::process_printer::{ProcessPrinter, ProcessPrinterContext};
 pub use crate::process_standard::ProcessStandard;
 
+flux_rs::defs! {
+    use flux_support::flux_ptr::valid_size;
+}
+
 use flux_support::capability::*;
 /// Userspace process identifier.
 ///
diff --git a/kernel/src/process_standard.rs b/kernel/src/process_standard.rs
index b762fdf748f..df8593c0e69 100644
--- a/kernel/src/process_standard.rs
+++ b/kernel/src/process_standard.rs
@@ -43,6 +43,10 @@ use crate::utilities::cells::{MapCell, NumericCellExt, OptionalCell};
 
 use tock_tbf::types::CommandPermissions;
 
+flux_rs::defs! {
+    use flux_support::flux_ptr::valid_size;
+}
+
 /// State for helping with debugging apps.
 ///
 /// These pointers and counters are not strictly required for kernel operation,
diff --git a/kernel/src/processbuffer.rs b/kernel/src/processbuffer.rs
index 63dc71083c5..f9b003c100c 100644
--- a/kernel/src/processbuffer.rs
+++ b/kernel/src/processbuffer.rs
@@ -33,6 +33,10 @@ use core::ops::{Deref, Index, Range, RangeFrom, RangeTo};
 #[allow(clippy::wildcard_imports)]
 use flux_support::*;
 
+flux_rs::defs! {
+    use flux_support::flux_ptr::valid_size;
+}
+
 /// Convert a process buffer's internal representation to a
 /// [`ReadableProcessSlice`].
 ///