update to account for trait-impl checks

kernel/Cargo.toml

@@ -16,7 +16,8 @@ tock-registers = { path = "../libraries/tock-register-interface" }
 tock-cells = { path = "../libraries/tock-cells" }
 tock-tbf = { path = "../libraries/tock-tbf" }
 flux_support = { path = "../flux_support" }
-flux-rs = { git  = "https://github.com/flux-rs/flux.git" }
+# flux-rs = { git  = "https://github.com/flux-rs/flux.git" }
+flux-rs = { path = "../../flux/lib/flux-rs" }
 
 # In general, Tock discourages the use of cargo features. However for certain
 # kernel crate configuration, we have not found reasonable alternatives to

kernel/src/collections/queue.rs

@@ -16,23 +16,29 @@ pub trait Queue<T> {
 
     /// If the queue isn't full, add a new element to the back of the queue.
     /// Returns whether the element was added.
+    #[flux_rs::trusted_impl]
     fn enqueue(&mut self, val: T) -> bool;
 
     /// Add a new element to the back of the queue, poping one from the front if necessary.
+    #[flux_rs::trusted_impl]
     fn push(&mut self, val: T) -> Option<T>;
 
     /// Remove the element from the front of the queue.
+    #[flux_rs::trusted_impl]
     fn dequeue(&mut self) -> Option<T>;
 
     /// Remove and return one (the first) element that matches the predicate.
+    #[flux_rs::trusted_impl]
     fn remove_first_matching<F>(&mut self, f: F) -> Option<T>
     where
         F: Fn(&T) -> bool;
 
     /// Remove all elements from the ring buffer.
+    #[flux_rs::trusted_impl]
     fn empty(&mut self);
 
     /// Retains only the elements that satisfy the predicate.
+    #[flux_rs::trusted_impl]
     fn retain<F>(&mut self, f: F)
     where
         F: FnMut(&T) -> bool;

kernel/src/hil/time.rs

@@ -134,6 +134,7 @@ pub trait Ticks: Clone + Copy + From<u32> + fmt::Debug + Ord + PartialOrd + Eq {
 
     /// Scales the ticks by the specified numerator and denominator. If the resulting value would
     /// be greater than u32,`u32::MAX` is returned instead
+    #[flux_rs::sig(fn(Self, u32, u32{denom: denom > 0}) -> u32)]
     fn saturating_scale(self, numerator: u32, denominator: u32) -> u32;
 }
 
@@ -402,6 +403,7 @@ pub trait Timer<'a>: Time {
 #[derive(Debug)]
 pub enum Freq100MHz {}
 impl Frequency for Freq100MHz {
+    #[flux_rs::sig(fn() -> u32{r: r > 0})]
     fn frequency() -> u32 {
         100_000_000
     }
@@ -411,6 +413,7 @@ impl Frequency for Freq100MHz {
 #[derive(Debug)]
 pub enum Freq16MHz {}
 impl Frequency for Freq16MHz {
+    #[flux_rs::sig(fn() -> u32{r: r > 0})]
     fn frequency() -> u32 {
         16_000_000
     }
@@ -419,6 +422,7 @@ impl Frequency for Freq16MHz {
 /// 10MHz `Frequency`
 pub enum Freq10MHz {}
 impl Frequency for Freq10MHz {
+    #[flux_rs::sig(fn() -> u32{r: r > 0})]
     fn frequency() -> u32 {
         10_000_000
     }
@@ -428,6 +432,7 @@ impl Frequency for Freq10MHz {
 #[derive(Debug)]
 pub enum Freq1MHz {}
 impl Frequency for Freq1MHz {
+    #[flux_rs::sig(fn() -> u32{r: r > 0})]
     fn frequency() -> u32 {
         1_000_000
     }
@@ -437,6 +442,7 @@ impl Frequency for Freq1MHz {
 #[derive(Debug)]
 pub enum Freq32KHz {}
 impl Frequency for Freq32KHz {
+    #[flux_rs::sig(fn() -> u32{r: r > 0})]
     fn frequency() -> u32 {
         32_768
     }
@@ -446,6 +452,7 @@ impl Frequency for Freq32KHz {
 #[derive(Debug)]
 pub enum Freq16KHz {}
 impl Frequency for Freq16KHz {
+    #[flux_rs::sig(fn() -> u32{r: r > 0})]
     fn frequency() -> u32 {
         16_000
     }
@@ -455,6 +462,7 @@ impl Frequency for Freq16KHz {
 #[derive(Debug)]
 pub enum Freq1KHz {}
 impl Frequency for Freq1KHz {
+    #[flux_rs::sig(fn() -> u32{r: r > 0})]
     fn frequency() -> u32 {
         1_000
     }

kernel/src/processbuffer.rs

@@ -868,7 +868,8 @@ impl Index<usize> for ReadableProcessSlice {
     // Cell to read-only operations
     type Output = ReadableProcessByte;
 
-    #[flux_rs::sig(fn(self: &ReadableProcessSlice[@len], idx: usize) -> &Self::Output requires len > idx)]
+    #[flux_rs::trusted_impl]
+    #[flux_rs::sig(fn(self: &ReadableProcessSlice[@len], idx: usize ) -> &Self::Output requires len > idx)]
     fn index(&self, idx: usize) -> &Self::Output {
         // As ReadableProcessSlice is a transparent wrapper around its
         // inner type, [ReadableProcessByte], we can use the regular
@@ -1108,6 +1109,7 @@ impl Index<usize> for WriteableProcessSlice {
     // mutating the memory contents is allowed.
     type Output = Cell<u8>;
 
+    #[flux_rs::trusted_impl]
     #[flux_rs::sig(fn(self: &WriteableProcessSlice[@len], idx: usize) -> &Self::Output requires len > idx)]
     fn index(&self, idx: usize) -> &Self::Output {
         // As WriteableProcessSlice is a transparent wrapper around

rust-toolchain.toml

@@ -1,8 +1,3 @@
-# Licensed under the Apache License, Version 2.0 or the MIT License.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
-# Copyright Tock Contributors 2023.
-
 [toolchain]
-channel = "nightly-2024-07-08"
-components = ["miri", "llvm-tools", "rust-src", "rustfmt", "clippy"]
-targets = ["thumbv6m-none-eabi", "thumbv7em-none-eabi", "thumbv7em-none-eabihf", "riscv32imc-unknown-none-elf", "riscv32imac-unknown-none-elf"]
+channel = "nightly-2024-08-20"
+components = ["rust-src", "rustc-dev", "llvm-tools", "rustfmt"]