peel back trusted and ignored

kernel/src/collections/mod.rs

@@ -3,9 +3,6 @@
 // Copyright Tock Contributors 2022.
 
 //! Data structures.
-#[flux::ignore]
 pub mod list;
-//#[flux::ignore]
 pub mod queue;
-// #[flux::ignore]
 pub mod ring_buffer;

kernel/src/collections/ring_buffer.rs

@@ -35,7 +35,6 @@ impl<'a, T: Copy> RingBuffer<'a, T> {
     }
 
     /// Returns the number of elements that can be enqueued until the ring buffer is full.
-    // #[flux::ignore]
     pub fn available_len(&self) -> usize {
         // The maximum capacity of the queue is ring_len - 1, because head == tail for the empty
         // queue.

kernel/src/hil/gpio.rs

@@ -273,6 +273,7 @@ pub struct InterruptValueWrapper<'a, IP: InterruptPin<'a>> {
 }
 
 impl<'a, IP: InterruptPin<'a>> InterruptValueWrapper<'a, IP> {
+    #[flux::trusted]
     pub fn new(pin: &'a IP) -> Self {
         Self {
             value: Cell::new(0),

kernel/src/hil/led.rs

@@ -43,12 +43,14 @@ pub struct LedLow<'a, P: gpio::Pin> {
 }
 
 impl<'a, P: gpio::Pin> LedHigh<'a, P> {
+    #[flux::trusted]
     pub fn new(p: &'a P) -> Self {
         Self { pin: p }
     }
 }
 
 impl<'a, P: gpio::Pin> LedLow<'a, P> {
+    #[flux::trusted]
     pub fn new(p: &'a P) -> Self {
         Self { pin: p }
     }

kernel/src/hil/mod.rs

@@ -18,17 +18,14 @@ pub mod digest;
 pub mod eic;
 pub mod entropy;
 pub mod flash;
-#[flux::ignore]
 pub mod gpio;
 pub mod gpio_async;
 pub mod hasher;
 pub mod i2c;
 pub mod kv;
-#[flux::ignore]
 pub mod led;
 pub mod log;
 pub mod nonvolatile_storage;
-// #[flux::ignore]
 pub mod public_key_crypto;
 pub mod pwm;
 pub mod radio;
@@ -38,7 +35,6 @@ pub mod sensors;
 pub mod spi;
 pub mod symmetric_encryption;
 pub mod text_screen;
-#[flux::ignore]
 pub mod time;
 pub mod touch;
 pub mod uart;

kernel/src/hil/time.rs

@@ -18,6 +18,7 @@
 use crate::ErrorCode;
 use core::cmp::Ordering;
 use core::fmt;
+use flux_support::assume;
 
 /// An integer type defining the width of a time value, which allows
 /// clients to know when wraparound will occur.
@@ -438,6 +439,7 @@ impl Ticks for Ticks32 {
 
     #[inline]
     fn saturating_scale(self, numerator: u32, denominator: u32) -> u32 {
+        assume(denominator > 0);
         let scaled = self.0 as u64 * numerator as u64 / denominator as u64;
         if scaled < u32::MAX as u64 {
             scaled as u32
@@ -519,6 +521,7 @@ impl Ticks for Ticks24 {
 
     #[inline]
     fn saturating_scale(self, numerator: u32, denominator: u32) -> u32 {
+        assume(denominator > 0);
         let scaled = self.0 as u64 * numerator as u64 / denominator as u64;
         if scaled < u32::MAX as u64 {
             scaled as u32
@@ -612,6 +615,7 @@ impl Ticks for Ticks16 {
 
     #[inline]
     fn saturating_scale(self, numerator: u32, denominator: u32) -> u32 {
+        assume(denominator > 0);
         let scaled = self.0 as u64 * numerator as u64 / denominator as u64;
         if scaled < u32::MAX as u64 {
             scaled as u32
@@ -701,6 +705,7 @@ impl Ticks for Ticks64 {
 
     #[inline]
     fn saturating_scale(self, num: u32, den: u32) -> u32 {
+        assume(den > 0);
         let scaled = self.0.saturating_mul(num as u64) / den as u64;
         if scaled < u32::MAX as u64 {
             scaled as u32

kernel/src/ipc.rs

@@ -23,7 +23,7 @@ pub const DRIVER_NUM: usize = 0x10000;
 mod ro_allow {
     pub(super) const SEARCH: usize = 0;
     /// The number of allow buffers the kernel stores for this grant.
-    pub(super) const COUNT: u8 = 1;
+    pub(super) const COUNT: u8 = 1; // VTOCK-NOTE: just replaced this with constant 1
 }
 
 /// Enum to mark which type of upcall is scheduled for the IPC mechanism.
@@ -98,7 +98,6 @@ impl<const NUM_PROCS: u8> IPC<NUM_PROCS> {
     }
 }
 
-// #[flux::ignore]
 impl<const NUM_PROCS: u8> SyscallDriver for IPC<NUM_PROCS> {
     /// command is how notify() is implemented.
     /// Notifying an IPC service is done by setting client_or_svc to 0,

kernel/src/kernel.rs

@@ -369,7 +369,6 @@ impl Kernel {
     /// This function has one configuration option: `no_sleep`. If that argument
     /// is set to true, the kernel will never attempt to put the chip to sleep,
     /// and this function can be called again immediately.
-    #[flux::ignore]
     pub fn kernel_loop_operation<KR: KernelResources<C>, C: Chip, const NUM_PROCS: u8>(
         &self,
         resources: &KR,
@@ -437,7 +436,6 @@ impl Kernel {
     ///
     /// Most of the behavior of this loop is controlled by the `Scheduler`
     /// implementation in use.
-    #[flux::ignore]
     pub fn kernel_loop<KR: KernelResources<C>, C: Chip, const NUM_PROCS: u8>(
         &self,
         resources: &KR,
@@ -484,7 +482,7 @@ impl Kernel {
     /// cooperatively). Notably, time spent in this function by the kernel,
     /// executing system calls or merely setting up the switch to/from
     /// userspace, is charged to the process.
-    #[flux::ignore]
+    #[flux::trusted]
     fn do_process<KR: KernelResources<C>, C: Chip, const NUM_PROCS: u8>(
         &self,
         resources: &KR,

kernel/src/lib.rs

@@ -118,7 +118,6 @@ pub mod platform;
 pub mod process;
 pub mod process_checker;
 pub mod processbuffer;
-#[flux::ignore]
 pub mod scheduler;
 pub mod storage_permissions;
 pub mod syscall;

kernel/src/memop.rs

@@ -42,7 +42,6 @@ use flux_support::*;
 ///   where the app has put the start of its heap. This is not strictly
 ///   necessary for correct operation, but allows for better debugging if the
 ///   app crashes.
-#[flux::ignore]
 pub(crate) fn memop(process: &dyn Process, op_type: usize, r1: usize) -> SyscallReturn {
     match op_type {
         // Op Type 0: BRK

kernel/src/platform/mod.rs

@@ -7,7 +7,6 @@
 //! Implementations of these traits are used by the core kernel.
 pub mod chip;
 pub mod mpu;
-#[flux::ignore]
 pub mod scheduler_timer;
 pub mod watchdog;
 

kernel/src/platform/scheduler_timer.rs

@@ -215,6 +215,7 @@ impl<A: 'static + time::Alarm<'static>> SchedulerTimer for VirtualSchedulerTimer
             None
         } else {
             let hertz = A::Frequency::frequency() as u64;
+            flux_support::assume(hertz > 0);
             Some(((diff * 1_000_000) / hertz) as u32)
         }
     }

kernel/src/scheduler/cooperative.rs

@@ -56,6 +56,7 @@ impl<'a> CooperativeSched<'a> {
 }
 
 impl<'a, C: Chip> Scheduler<C> for CooperativeSched<'a> {
+    #[flux::trusted]
     fn next(&self) -> SchedulingDecision {
         let mut first_head = None;
         let mut next = None;

kernel/src/scheduler/mlfq.rs

@@ -73,7 +73,7 @@ impl<'a, A: 'static + time::Alarm<'static>> MLFQSched<'a, A> {
     /// How often to restore all processes to max priority
     pub const PRIORITY_REFRESH_PERIOD_MS: u32 = 5000;
     pub const NUM_QUEUES: usize = 3;
-
+    #[flux::trusted]
     pub fn new(alarm: &'static A) -> Self {
         Self {
             alarm,
@@ -106,6 +106,7 @@ impl<'a, A: 'static + time::Alarm<'static>> MLFQSched<'a, A> {
     /// Returns the process at the head of the highest priority queue containing a process
     /// that is ready to execute (as determined by `has_tasks()`)
     /// This method moves that node to the head of its queue.
+    #[flux::trusted]
     fn get_next_ready_process_node(&self) -> (Option<&MLFQProcessNode<'a>>, usize) {
         for (idx, queue) in self.processes.iter().enumerate() {
             let next = queue
@@ -135,6 +136,7 @@ impl<'a, A: 'static + time::Alarm<'static>> MLFQSched<'a, A> {
 }
 
 impl<'a, A: 'static + time::Alarm<'static>, C: Chip> Scheduler<C> for MLFQSched<'a, A> {
+    #[flux::trusted]
     fn next(&self) -> SchedulingDecision {
         let now = self.alarm.now();
         let next_reset = self.next_reset.get();
@@ -162,6 +164,7 @@ impl<'a, A: 'static + time::Alarm<'static>, C: Chip> Scheduler<C> for MLFQSched<
         SchedulingDecision::RunProcess((next, Some(timeslice)))
     }
 
+    #[flux::trusted]
     fn result(&self, result: StoppedExecutingReason, execution_time_us: Option<u32>) {
         let execution_time_us = execution_time_us.unwrap(); // should never fail as we never run cooperatively
         let queue_idx = self.last_queue_idx.get();

kernel/src/scheduler/priority.rs

@@ -38,6 +38,7 @@ impl PrioritySched {
 }
 
 impl<C: Chip> Scheduler<C> for PrioritySched {
+    #[flux::trusted]
     fn next(&self) -> SchedulingDecision {
         // Iterates in-order through the process array, always running the
         // first process it finds that is ready to run. This enforces the
@@ -54,6 +55,7 @@ impl<C: Chip> Scheduler<C> for PrioritySched {
         })
     }
 
+    #[flux::trusted]
     unsafe fn continue_process(&self, _: ProcessId, chip: &C) -> bool {
         // In addition to checking for interrupts, also checks if any higher
         // priority processes have become ready. This check is necessary because

kernel/src/scheduler/round_robin.rs

@@ -74,6 +74,7 @@ impl<'a> RoundRobinSched<'a> {
 }
 
 impl<'a, C: Chip> Scheduler<C> for RoundRobinSched<'a> {
+    #[flux::trusted]
     fn next(&self) -> SchedulingDecision {
         let mut first_head = None;
         let mut next = None;
@@ -125,6 +126,7 @@ impl<'a, C: Chip> Scheduler<C> for RoundRobinSched<'a> {
         SchedulingDecision::RunProcess((next, Some(timeslice)))
     }
 
+    #[flux::trusted]
     fn result(&self, result: StoppedExecutingReason, execution_time_us: Option<u32>) {
         let execution_time_us = execution_time_us.unwrap(); // should never fail
         let reschedule = match result {

kernel/src/storage_permissions.rs

@@ -72,7 +72,6 @@ impl StoragePermissions {
     /// kernel to read/update any stored item, and allows the kernel to write
     /// items that will not be accessible to any clients without superuser
     /// permissions.
-    #[flux::ignore]
     pub fn new_kernel_permissions(_cap: &dyn capabilities::KerneluserStorageCapability) -> Self {
         let read_permissions: [u32; 8] = [0; 8];
         let modify_permissions: [u32; 8] = [0; 8];

kernel/src/utilities/helpers.rs

@@ -46,7 +46,6 @@ macro_rules! count_expressions {
 /// Compute a POSIX-style CRC32 checksum of a slice.
 ///
 /// Online calculator: <https://crccalc.com/>
-#[flux::ignore]
 pub fn crc32_posix(b: &[u8]) -> u32 {
     let mut crc: u32 = 0;
 

kernel/src/utilities/math.rs

@@ -6,7 +6,6 @@
 
 use core::f32;
 
-
 // VTOCK-TODO: supplementary Z3 proofs for these two functions
 
 /// Get closest power of two greater than the given number.
@@ -39,7 +38,6 @@ pub fn closest_power_of_two_usize(mut num: usize) -> usize {
     num
 }
 
-
 #[derive(Copy, Clone, Debug, PartialEq, PartialOrd, Eq, Ord)]
 pub struct PowerOfTwo(u32);
 
@@ -100,7 +98,6 @@ pub fn log_base_two_u32_usize(num: usize) -> u32 {
     }
 }
 
-
 /// Log base 2 of 64 bit unsigned integers.
 #[flux::trusted]
 #[flux::sig(fn(num: u64) -> u32{r: r < 64 && (num > 1 => r > 0)})]
@@ -116,7 +113,6 @@ pub fn log_base_two_u64(num: u64) -> u32 {
 const EXPONENT_MASK: u32 = 0b01111111_10000000_00000000_00000000;
 const EXPONENT_BIAS: u32 = 127;
 
-#[flux::ignore]
 pub fn abs(n: f32) -> f32 {
     f32::from_bits(n.to_bits() & 0x7FFF_FFFF)
 }
@@ -125,12 +121,10 @@ fn extract_exponent_bits(x: f32) -> u32 {
     (x.to_bits() & EXPONENT_MASK).overflowing_shr(23).0
 }
 
-#[flux::ignore]
 fn extract_exponent_value(x: f32) -> i32 {
     (extract_exponent_bits(x) as i32) - EXPONENT_BIAS as i32
 }
 
-#[flux::ignore]
 fn ln_1to2_series_approximation(x: f32) -> f32 {
     // idea from https://stackoverflow.com/a/44232045/
     // modified to not be restricted to int range and only values of x above 1.0.
@@ -168,7 +162,6 @@ fn ln_1to2_series_approximation(x: f32) -> f32 {
     }
 }
 
-#[flux::ignore]
 pub fn log10(x: f32) -> f32 {
     //using change of base log10(x) = ln(x)/ln(10)
     let ln10_recip = f32::consts::LOG10_E;

kernel/src/utilities/mod.rs

@@ -3,7 +3,6 @@
 // Copyright Tock Contributors 2022.
 
 //! Utility functions and macros provided by the kernel crate.
-// #[flux::ignore]
 pub mod binary_write;
 pub mod copy_slice;
 pub mod helpers;