Migrate to qualified flux defs

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" {

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

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

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 {

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)]

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);

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::*;

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,

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.

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)]

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.
 ///

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,

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`].
 ///