kernel passes again

kernel/src/collections/ring_buffer.rs

@@ -34,7 +34,7 @@ impl<'a, T: Copy> RingBuffer<'a, T> {
     }
 
     /// Returns the number of elements that can be enqueued until the ring buffer is full.
-    #[flux::ignore]
+    // #[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.
@@ -69,7 +69,7 @@ impl<'a, T: Copy> RingBuffer<'a, T> {
     }
 }
 
-#[flux::ignore]
+#[flux::trusted]
 impl<T: Copy> queue::Queue<T> for RingBuffer<'_, T> {
     fn has_elements(&self) -> bool {
         self.head != self.tail

kernel/src/deferred_call.rs

@@ -80,6 +80,7 @@ pub trait DeferredCallClient: Sized {
 /// per instance, but this alternative stores only the data and function pointers,
 /// 8 bytes per instance.
 #[derive(Copy, Clone)]
+#[flux::opaque]
 struct DynDefCallRef<'a> {
     data: *const (),
     callback: fn(*const ()),

kernel/src/hil/mod.rs

@@ -28,7 +28,7 @@ pub mod kv;
 pub mod led;
 pub mod log;
 pub mod nonvolatile_storage;
-#[flux::ignore]
+// #[flux::ignore]
 pub mod public_key_crypto;
 pub mod pwm;
 pub mod radio;

kernel/src/hil/public_key_crypto/keys.rs

@@ -223,6 +223,7 @@ pub trait RsaKey: PubKey {
     /// The modulus is returned MSB (big endian)
     /// Returns `Some()` if the key exists and the closure was called,
     /// otherwise returns `None`.
+    #[flux::ignore]
     fn map_modulus(&self, closure: &dyn Fn(&[u8])) -> Option<()>;
 
     /// The the modulus if it exists.
@@ -241,6 +242,7 @@ pub trait RsaPrivKey: PubPrivKey + RsaKey {
     /// The exponent is returned MSB (big endian)
     /// Returns `Some()` if the key exists and the closure was called,
     /// otherwise returns `None`.
+    #[flux::ignore]
     fn map_exponent(&self, closure: &dyn Fn(&[u8])) -> Option<()>;
 
     /// The the private exponent if it exists.
@@ -256,6 +258,7 @@ pub trait RsaKeyMut: PubKeyMut {
     /// The modulus is returned MSB (big endian)
     /// Returns `Some()` if the key exists and the closure was called,
     /// otherwise returns `None`.
+    #[flux::ignore]
     fn map_modulus(&self, closure: &dyn Fn(&mut [u8])) -> Option<()>;
 
     /// The the modulus if it exists.
@@ -274,6 +277,7 @@ pub trait RsaPrivKeyMut: PubPrivKeyMut + RsaKeyMut {
     /// The exponent is returned MSB (big endian)
     /// Returns `Some()` if the key exists and the closure was called,
     /// otherwise returns `None`.
+    #[flux::ignore]
     fn map_exponent(&self, closure: &dyn Fn(&mut [u8])) -> Option<()>;
 
     /// The the private exponent if it exists.

kernel/src/lib.rs

@@ -108,7 +108,7 @@ pub mod capabilities;
 pub mod collections;
 pub mod component;
 pub mod debug;
-#[flux::ignore]
+#[flux::trusted]
 pub mod deferred_call;
 pub mod errorcode;
 #[flux::trusted]
@@ -119,7 +119,7 @@ pub mod introspection;
 pub mod ipc;
 pub mod platform;
 pub mod process;
-#[flux::ignore]
+// #[flux::ignore]
 pub mod process_checker;
 pub mod processbuffer;
 #[flux::ignore]
@@ -133,11 +133,9 @@ mod config;
 mod kernel;
 mod memop;
 mod process_binary;
-#[flux::ignore]
 mod process_loading;
 mod process_policies;
 mod process_printer;
-#[flux::ignore]
 mod process_standard;
 mod syscall_driver;
 

kernel/src/process_checker.rs

@@ -206,7 +206,9 @@ pub struct ProcessCheckerMachine {
     footer_index: Cell<usize>,
 }
 
+#[flux::trusted]
 impl ProcessCheckerMachine {
+    #[flux::trusted]
     pub fn new(policy: &'static dyn AppCredentialsPolicy<'static>) -> Self {
         Self {
             footer_index: Cell::new(0),

kernel/src/process_checker/basic.rs

@@ -32,6 +32,7 @@ pub struct AppCheckerSimulated<'a> {
 }
 
 impl<'a> AppCheckerSimulated<'a> {
+    #[flux::trusted]
     pub fn new() -> Self {
         Self {
             deferred_call: DeferredCall::new(),
@@ -43,6 +44,7 @@ impl<'a> AppCheckerSimulated<'a> {
 }
 
 impl<'a> DeferredCallClient for AppCheckerSimulated<'a> {
+    #[flux::trusted]
     fn handle_deferred_call(&self) {
         self.client.map(|c| {
             c.check_done(
@@ -77,7 +79,7 @@ impl<'a> AppCredentialsPolicy<'a> for AppCheckerSimulated<'a> {
             Err((ErrorCode::BUSY, credentials, binary))
         }
     }
-
+    #[flux::trusted]
     fn set_client(&self, client: &'a dyn AppCredentialsPolicyClient<'a>) {
         self.client.replace(client);
     }
@@ -137,6 +139,7 @@ pub struct AppCheckerSha256 {
 }
 
 impl AppCheckerSha256 {
+    #[flux::trusted]
     pub fn new(
         hash: &'static dyn Sha256Verifier<'static>,
         buffer: &'static mut [u8; 32],
@@ -155,7 +158,7 @@ impl AppCredentialsPolicy<'static> for AppCheckerSha256 {
     fn require_credentials(&self) -> bool {
         true
     }
-
+    #[flux::trusted]
     fn check_credentials(
         &self,
         credentials: TbfFooterV2Credentials,
@@ -176,15 +179,15 @@ impl AppCredentialsPolicy<'static> for AppCheckerSha256 {
             _ => Err((ErrorCode::NOSUPPORT, credentials, binary)),
         }
     }
-
+    #[flux::trusted]
     fn set_client(&self, client: &'static dyn AppCredentialsPolicyClient<'static>) {
         self.client.replace(client);
     }
 }
 
 impl ClientData<32_usize> for AppCheckerSha256 {
     fn add_mut_data_done(&self, _result: Result<(), ErrorCode>, _data: SubSliceMut<'static, u8>) {}
-
+    #[flux::trusted]
     fn add_data_done(&self, result: Result<(), ErrorCode>, data: SubSlice<'static, u8>) {
         match result {
             Err(e) => panic!("Internal error during application binary checking. SHA256 engine threw error in adding data: {:?}", e),
@@ -201,6 +204,7 @@ impl ClientData<32_usize> for AppCheckerSha256 {
 }
 
 impl ClientVerify<32_usize> for AppCheckerSha256 {
+    #[flux::trusted]
     fn verification_done(
         &self,
         result: Result<bool, ErrorCode>,
@@ -257,6 +261,7 @@ pub struct AppIdAssignerNames<'a, F: Fn(&'static str) -> u32> {
     hasher: &'a F,
 }
 
+#[flux::trusted]
 impl<'a, F: Fn(&'static str) -> u32> AppIdAssignerNames<'a, F> {
     pub fn new(hasher: &'a F) -> Self {
         Self { hasher }
@@ -286,6 +291,7 @@ impl<'a, F: Fn(&'static str) -> u32> AppUniqueness for AppIdAssignerNames<'a, F>
 }
 
 impl<'a, F: Fn(&'static str) -> u32> Compress for AppIdAssignerNames<'a, F> {
+    #[flux::trusted]
     fn to_short_id(&self, process: &ProcessBinary) -> ShortId {
         let name = process.header.get_package_name().unwrap_or("");
         let sum = (self.hasher)(name);
@@ -311,6 +317,7 @@ pub struct AppCheckerRsaSimulated<'a> {
     binary: OptionalCell<&'a [u8]>,
 }
 
+#[flux::trusted]
 impl<'a> AppCheckerRsaSimulated<'a> {
     pub fn new() -> AppCheckerRsaSimulated<'a> {
         Self {
@@ -323,6 +330,7 @@ impl<'a> AppCheckerRsaSimulated<'a> {
 }
 
 impl<'a> DeferredCallClient for AppCheckerRsaSimulated<'a> {
+    #[flux::trusted]
     fn handle_deferred_call(&self) {
         // This checker does not actually verify the RSA signature; it
         // assumes the signature is valid and so accepts any RSA
@@ -368,7 +376,7 @@ impl<'a> AppCredentialsPolicy<'a> for AppCheckerRsaSimulated<'a> {
             Err((ErrorCode::BUSY, credentials, binary))
         }
     }
-
+    #[flux::trusted]
     fn set_client(&self, client: &'a dyn AppCredentialsPolicyClient<'a>) {
         self.client.replace(client);
     }

kernel/src/process_checker/signature.rs

@@ -1,7 +1,6 @@
 // Licensed under the Apache License, Version 2.0 or the MIT License.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // Copyright Tock Contributors 2024.
-
 //! Signature credential checker for checking process credentials.
 
 use crate::hil;
@@ -47,6 +46,7 @@ impl<
         const SL: usize,
     > AppCheckerSignature<'a, S, H, HL, SL>
 {
+    #[flux::trusted]
     pub fn new(
         hasher: &'a H,
         verifier: &'a S,
@@ -76,7 +76,7 @@ impl<
     > hil::digest::ClientData<HL> for AppCheckerSignature<'a, S, H, HL, SL>
 {
     fn add_mut_data_done(&self, _result: Result<(), ErrorCode>, _data: SubSliceMut<'static, u8>) {}
-
+    #[flux::trusted]
     fn add_data_done(&self, result: Result<(), ErrorCode>, data: SubSlice<'static, u8>) {
         self.binary.set(data.take());
 
@@ -104,7 +104,7 @@ impl<
         }
     }
 }
-
+#[flux::trusted]
 impl<
         'a,
         S: hil::public_key_crypto::signature::SignatureVerify<'static, HL, SL>,
@@ -162,7 +162,7 @@ impl<
         // Needed to make the sha256 client work.
     }
 }
-
+#[flux::trusted]
 impl<
         'a,
         S: hil::public_key_crypto::signature::SignatureVerify<'static, HL, SL>,
@@ -194,7 +194,7 @@ impl<
         });
     }
 }
-
+#[flux::trusted]
 impl<
         'a,
         S: hil::public_key_crypto::signature::SignatureVerify<'static, HL, SL>,

kernel/src/process_loading.rs

@@ -181,6 +181,7 @@ pub fn load_processes<C: Chip>(
 /// `ProcessLoadError` if something goes wrong during TBF parsing or process
 /// creation.
 #[inline(always)]
+#[flux::trusted]
 fn load_processes_from_flash<C: Chip>(
     kernel: &'static Kernel,
     chip: &'static C,
@@ -275,6 +276,7 @@ fn load_processes_from_flash<C: Chip>(
 
 /// Find a process binary stored at the beginning of `flash` and create a
 /// `ProcessBinary` object if the process is viable to run on this kernel.
+#[flux::trusted]
 fn discover_process_binary(
     flash: &'static [u8],
 ) -> Result<(&'static [u8], ProcessBinary), (&'static [u8], ProcessBinaryError)> {
@@ -341,6 +343,7 @@ fn discover_process_binary(
 /// pool that its RAM should be allocated from. Returns `Ok` if the process
 /// object was created, `Err` with a relevant error if the process object could
 /// not be created.
+#[flux::trusted]
 fn load_process<C: Chip>(
     kernel: &'static Kernel,
     chip: &'static C,
@@ -485,6 +488,7 @@ impl<'a, C: Chip> SequentialProcessLoaderMachine<'a, C> {
     /// processes from slices of flash an memory is fundamentally unsafe.
     /// Therefore, we require the `ProcessManagementCapability` to call this
     /// function.
+    #[flux::trusted]
     pub fn new(
         checker: &'static ProcessCheckerMachine,
         procs: &'static mut [Option<&'static dyn Process>],
@@ -514,6 +518,7 @@ impl<'a, C: Chip> SequentialProcessLoaderMachine<'a, C> {
     }
 
     /// Find a slot in the `PROCESSES` array to store this process.
+    #[flux::trusted]
     fn find_open_process_slot(&self) -> Option<usize> {
         self.procs.map_or(None, |procs| {
             for (i, p) in procs.iter().enumerate() {
@@ -577,6 +582,7 @@ impl<'a, C: Chip> SequentialProcessLoaderMachine<'a, C> {
     ///
     /// Returns the process binary object or an error if a valid process
     /// binary could not be extracted.
+    #[flux::trusted]
     fn discover_process_binary(&self) -> Result<ProcessBinary, ProcessBinaryError> {
         let flash = self.flash.get();
 
@@ -640,6 +646,7 @@ impl<'a, C: Chip> SequentialProcessLoaderMachine<'a, C> {
     /// Create process objects from the discovered process binaries.
     ///
     /// This verifies that the discovered processes are valid to run.
+    #[flux::trusted]
     fn load_process_objects(&self) -> Result<(), ()> {
         let proc_binaries = self.proc_binaries.take().ok_or(())?;
         let proc_binaries_len = proc_binaries.len();
@@ -904,6 +911,7 @@ impl<'a, C: Chip> DeferredCallClient for SequentialProcessLoaderMachine<'a, C> {
 impl<'a, C: Chip> crate::process_checker::ProcessCheckerMachineClient
     for SequentialProcessLoaderMachine<'a, C>
 {
+    #[flux::trusted]
     fn done(
         &self,
         process_binary: ProcessBinary,

kernel/src/process_standard.rs

@@ -293,6 +293,7 @@ impl<C: Chip> Process for ProcessStandard<'_, C> {
             || self.state.get() == State::Running
     }
 
+    #[flux::trusted]
     fn remove_pending_upcalls(&self, upcall_id: UpcallId) {
         self.tasks.map(|tasks| {
             let count_before = tasks.len();
@@ -1162,6 +1163,7 @@ impl<C: Chip> Process for ProcessStandard<'_, C> {
         }
     }
 
+    #[flux::trusted]
     fn print_full_process(&self, writer: &mut dyn Write) {
         if !config::CONFIG.debug_panics {
             return;
@@ -1275,6 +1277,7 @@ impl<C: 'static + Chip> ProcessStandard<'_, C> {
     const PROCESS_STRUCT_OFFSET: usize = mem::size_of::<ProcessStandard<C>>();
 
     /// Create a `ProcessStandard` object based on the found `ProcessBinary`.
+    #[flux::trusted]
     pub(crate) unsafe fn create<'a>(
         kernel: &'static Kernel,
         chip: &'static C,
@@ -1885,6 +1888,7 @@ impl<C: 'static + Chip> ProcessStandard<'_, C> {
     /// at `app_break`). If this method returns `true`, the buffer is guaranteed
     /// to be accessible to the process and to not overlap with the grant
     /// region.
+    #[flux::trusted]
     fn in_app_owned_memory(&self, buf_start_addr: *const u8, size: usize) -> bool {
         let buf_end_addr = buf_start_addr.wrapping_add(size);
 
@@ -1897,6 +1901,7 @@ impl<C: 'static + Chip> ProcessStandard<'_, C> {
     /// are within the readable region of an application's flash memory.  If
     /// this method returns true, the buffer is guaranteed to be readable to the
     /// process.
+    #[flux::trusted]
     fn in_app_flash_memory(&self, buf_start_addr: *const u8, size: usize) -> bool {
         let buf_end_addr = buf_start_addr.wrapping_add(size);
 
@@ -1923,6 +1928,7 @@ impl<C: 'static + Chip> ProcessStandard<'_, C> {
     /// If there is not enough memory, or the MPU cannot isolate the process
     /// accessible region from the new kernel memory break after doing the
     /// allocation, then this will return `None`.
+    #[flux::trusted]
     fn allocate_in_grant_region_internal(&self, size: usize, align: usize) -> Option<NonNull<u8>> {
         self.mpu_config.and_then(|config| {
             // First, compute the candidate new pointer. Note that at this point
@@ -1982,6 +1988,7 @@ impl<C: 'static + Chip> ProcessStandard<'_, C> {
     ///
     /// We create this identifier by calculating the number of bytes between
     /// where the custom grant starts and the end of the process memory.
+    #[flux::trusted]
     fn create_custom_grant_identifier(&self, ptr: NonNull<u8>) -> ProcessCustomGrantIdentifier {
         let custom_grant_address = ptr.as_ptr() as usize;
         let process_memory_end = self.mem_end() as usize;
@@ -1995,6 +2002,7 @@ impl<C: 'static + Chip> ProcessStandard<'_, C> {
     /// custom grant.
     ///
     /// This reverses `create_custom_grant_identifier()`.
+    #[flux::trusted]
     fn get_custom_grant_address(&self, identifier: ProcessCustomGrantIdentifier) -> usize {
         let process_memory_end = self.mem_end() as usize;