From d12da27d9699da70b4acef8e079c8e48c8cd9b3c Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Tue, 18 Nov 2025 14:56:29 -0800 Subject: [PATCH 01/14] Add extern specs --- flux_support/src/extern_specs/cmp.rs | 3 +++ flux_support/src/extern_specs/mod.rs | 3 ++- flux_support/src/extern_specs/slice.rs | 1 + 3 files changed, 6 insertions(+), 1 deletion(-) create mode 100644 flux_support/src/extern_specs/cmp.rs diff --git a/flux_support/src/extern_specs/cmp.rs b/flux_support/src/extern_specs/cmp.rs new file mode 100644 index 0000000000..2110b3d9a9 --- /dev/null +++ b/flux_support/src/extern_specs/cmp.rs @@ -0,0 +1,3 @@ +#[flux_rs::extern_spec(core::cmp)] +#[flux_rs::no_panic] +fn min(v1: T, v2: T) -> T; \ No newline at end of file diff --git a/flux_support/src/extern_specs/mod.rs b/flux_support/src/extern_specs/mod.rs index 568e0aff94..b3313f6c51 100644 --- a/flux_support/src/extern_specs/mod.rs +++ b/flux_support/src/extern_specs/mod.rs @@ -1,3 +1,4 @@ +mod cmp; mod iter; mod mem; mod non_null; @@ -6,4 +7,4 @@ mod option; mod partial_cmp; mod range; mod result; -mod slice; +mod slice; \ No newline at end of file diff --git a/flux_support/src/extern_specs/slice.rs b/flux_support/src/extern_specs/slice.rs index 04c7a9b2a5..af341a667c 100644 --- a/flux_support/src/extern_specs/slice.rs +++ b/flux_support/src/extern_specs/slice.rs @@ -15,6 +15,7 @@ use core::slice::{self, Iter, SliceIndex}; #[flux_rs::extern_spec] impl [T] { + #[flux_rs::no_panic] #[flux_rs::sig(fn(&[T][@len]) -> usize[len])] fn len(v: &[T]) -> usize; From 1c5933c13d1a02ae475134ca60417668b61683b7 Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Tue, 18 Nov 2025 15:48:44 -0800 Subject: [PATCH 02/14] Turn on no_panic at module level --- capsules/core/Cargo.toml | 1 + 1 file changed, 1 insertion(+) diff --git a/capsules/core/Cargo.toml b/capsules/core/Cargo.toml index 559c3f9d61..b022693278 100644 --- a/capsules/core/Cargo.toml +++ b/capsules/core/Cargo.toml @@ -16,6 +16,7 @@ tickv = { path = "../../libraries/tickv" } [package.metadata.flux] enabled = true check_overflow = "lazy" +no_panic = true include = [ "src/button.rs", "src/led.rs", "src/console.rs", "src/alarm.rs", "src/spi_peripheral.rs", "src/stream.rs" ] [lints] From 2110fae6ac2ae416df65c60dbfc445b70f2ad7eb Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Wed, 19 Nov 2025 14:16:57 -0800 Subject: [PATCH 03/14] Some low hanging fruit --- flux_support/src/extern_specs/cell.rs | 19 +++++++++++++++++++ flux_support/src/extern_specs/mod.rs | 1 + flux_support/src/extern_specs/option.rs | 7 +++++++ 3 files changed, 27 insertions(+) create mode 100644 flux_support/src/extern_specs/cell.rs diff --git a/flux_support/src/extern_specs/cell.rs b/flux_support/src/extern_specs/cell.rs new file mode 100644 index 0000000000..cf808e877a --- /dev/null +++ b/flux_support/src/extern_specs/cell.rs @@ -0,0 +1,19 @@ +use core::cell::Cell; + +#[flux_rs::extern_spec(core::cell)] +struct Cell; + +#[flux_rs::extern_spec(core::cell)] +impl Cell { + #[flux_rs::no_panic] + fn get(&self) -> T; +} + +#[flux_rs::extern_spec(core::cell)] +impl Cell { + #[flux_rs::no_panic] + fn new(value: T) -> Cell; + + #[flux_rs::no_panic] + fn set(&self, value: T); +} \ No newline at end of file diff --git a/flux_support/src/extern_specs/mod.rs b/flux_support/src/extern_specs/mod.rs index b3313f6c51..63d0c44820 100644 --- a/flux_support/src/extern_specs/mod.rs +++ b/flux_support/src/extern_specs/mod.rs @@ -1,3 +1,4 @@ +mod cell; mod cmp; mod iter; mod mem; diff --git a/flux_support/src/extern_specs/option.rs b/flux_support/src/extern_specs/option.rs index ae070d769f..46daa6c586 100644 --- a/flux_support/src/extern_specs/option.rs +++ b/flux_support/src/extern_specs/option.rs @@ -14,4 +14,11 @@ impl Option { #[sig(fn(&Option[@b]) -> bool[!b])] const fn is_none(&self) -> bool; + + #[flux_rs::no_panic] + fn unwrap_or_default(self) -> T + where + T: Default; + + } From 4760f905f59d3d70ede5676b6d1684b5288fce47 Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Wed, 19 Nov 2025 18:02:56 -0800 Subject: [PATCH 04/14] More extern specs --- flux_support/src/extern_specs/iter.rs | 20 ++++++++++++++++++++ flux_support/src/extern_specs/partial_cmp.rs | 12 +++++------- 2 files changed, 25 insertions(+), 7 deletions(-) diff --git a/flux_support/src/extern_specs/iter.rs b/flux_support/src/extern_specs/iter.rs index 8d8dfa6f84..5ac46ff3ba 100644 --- a/flux_support/src/extern_specs/iter.rs +++ b/flux_support/src/extern_specs/iter.rs @@ -1,11 +1,31 @@ #![allow(unused)] use crate::assert; use core::slice::Iter; +use core::iter::IntoIterator; #[flux_rs::extern_spec(core::slice)] #[flux_rs::refined_by(idx: int, len: int)] struct Iter<'a, T>; +#[flux_rs::extern_spec] +trait FromIterator {} + +#[flux_rs::extern_spec(core::iter)] +trait IntoIterator { + #[flux_rs::spec(fn(self: Self) -> Self::IntoIter)] + #[flux_rs::no_panic] + fn into_iter(self) -> Self::IntoIter + where + Self: Sized; +} + +#[flux_rs::extern_spec(core::ops)] +impl IntoIterator for I { + #[flux_rs::spec(fn(self: I[@s]) -> I[s])] + #[flux_rs::no_panic] + fn into_iter(self) -> I; +} + // #[flux_rs::extern_spec(std::iter)] // #[flux_rs::refined_by(idx: int, inner: I)] // struct Enumerate; diff --git a/flux_support/src/extern_specs/partial_cmp.rs b/flux_support/src/extern_specs/partial_cmp.rs index 1dc6d0d1cd..9826b302e6 100644 --- a/flux_support/src/extern_specs/partial_cmp.rs +++ b/flux_support/src/extern_specs/partial_cmp.rs @@ -2,10 +2,8 @@ use core::cmp::PartialOrd; -// #[flux_rs::extern_spec(core::cmp)] -// #[flux_rs::assoc(fn lt(this: Self, other: Self) -> bool)] -// #[flux_rs::assoc(fn le(this: Self, other: Self) -> bool)] -// trait PartialOrd: PartialEq { -// fn lt(&self, other: &Rhs) -> bool; -// fn le(&self, other: &Rhs) -> bool; -// } +#[flux_rs::extern_spec(core::cmp)] +trait PartialOrd: PartialEq { + fn lt(&self, other: &Rhs) -> bool; + fn le(&self, other: &Rhs) -> bool; +} From deb8ddb84b5089576dd007ff22301e296ff86fe0 Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Wed, 19 Nov 2025 18:07:05 -0800 Subject: [PATCH 05/14] Extern spec for min --- flux_support/src/extern_specs/partial_cmp.rs | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/flux_support/src/extern_specs/partial_cmp.rs b/flux_support/src/extern_specs/partial_cmp.rs index 9826b302e6..76e3de6cdb 100644 --- a/flux_support/src/extern_specs/partial_cmp.rs +++ b/flux_support/src/extern_specs/partial_cmp.rs @@ -2,8 +2,17 @@ use core::cmp::PartialOrd; +#[flux_rs::extern_spec(core::cmp)] +trait Ord { + #[flux_rs::no_panic] + fn min(self, other: Self) -> Self + where + Self: Sized; +} + #[flux_rs::extern_spec(core::cmp)] trait PartialOrd: PartialEq { + #[flux_rs::no_panic] fn lt(&self, other: &Rhs) -> bool; fn le(&self, other: &Rhs) -> bool; } From eca4d6e536dfa9edc395892f48e6f7079972c058 Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Thu, 20 Nov 2025 20:06:20 -0800 Subject: [PATCH 06/14] Squish all kernel::hil panics --- flux_support/src/extern_specs/num.rs | 3 +++ kernel/src/hil/gpio.rs | 11 +++++++++++ kernel/src/hil/led.rs | 4 ++++ kernel/src/hil/spi.rs | 5 +++++ kernel/src/hil/time.rs | 15 +++++++++++++++ kernel/src/hil/uart.rs | 3 +++ kernel/src/syscall_driver.rs | 3 +++ 7 files changed, 44 insertions(+) diff --git a/flux_support/src/extern_specs/num.rs b/flux_support/src/extern_specs/num.rs index 14ad22ac5e..e0f64154df 100644 --- a/flux_support/src/extern_specs/num.rs +++ b/flux_support/src/extern_specs/num.rs @@ -9,6 +9,9 @@ impl u32 { #[sig(fn(num: u32) -> u32{r: (num == 0 => r == 32) && (num != 0 =>r <= 31) })] fn trailing_zeros(self) -> u32; + + #[flux_rs::no_panic] + fn saturating_sub(self, rhs: u32) -> u32; } #[flux_rs::extern_spec] diff --git a/kernel/src/hil/gpio.rs b/kernel/src/hil/gpio.rs index f974909e32..898ca4c512 100644 --- a/kernel/src/hil/gpio.rs +++ b/kernel/src/hil/gpio.rs @@ -96,6 +96,7 @@ pub trait Configure { /// Make the pin an input, returning the current configuration, /// which should be ither `Configuration::Input` or /// `Configuration::InputOutput`. + #[flux_rs::no_panic] fn make_input(&self) -> Configuration; /// Disable the pin as an input, returning the current configuration. fn disable_input(&self) -> Configuration; @@ -109,6 +110,7 @@ pub trait Configure { fn deactivate_to_low_power(&self); /// Set the floating state of the pin. + #[flux_rs::no_panic] fn set_floating_state(&self, state: FloatingState); /// Return the current floating state of the pin. fn floating_state(&self) -> FloatingState; @@ -180,9 +182,11 @@ pub trait Input { /// Get the current state of an input GPIO pin. For an output /// pin, return the output; for an input pin, return the input; /// for disabled or function pins the value is undefined. + #[flux_rs::no_panic] fn read(&self) -> bool; /// Get the current state of a GPIO pin, for a given activation mode. + #[flux_rs::no_panic] fn read_activation(&self, mode: ActivationMode) -> ActivationState { let value = self.read(); match (mode, value) { @@ -203,9 +207,11 @@ pub trait Interrupt<'a>: Input { /// Enable an interrupt on the GPIO pin. This does not /// configure the pin except to enable an interrupt: it /// should be separately configured as an input, etc. + #[flux_rs::no_panic] fn enable_interrupts(&self, mode: InterruptEdge); /// Disable interrupts for the GPIO pin. + #[flux_rs::no_panic] fn disable_interrupts(&self); /// Return whether this interrupt is pending @@ -288,6 +294,7 @@ impl<'a, IP: InterruptPin<'a>> InterruptValueWrapper<'a, IP> { } impl<'a, IP: InterruptPin<'a>> InterruptWithValue<'a> for InterruptValueWrapper<'a, IP> { + #[flux_rs::no_panic] fn set_value(&self, value: u32) { self.value.set(value); } @@ -304,11 +311,13 @@ impl<'a, IP: InterruptPin<'a>> InterruptWithValue<'a> for InterruptValueWrapper< self.source.is_pending() } + #[flux_rs::no_panic] fn enable_interrupts(&self, edge: InterruptEdge) -> Result<(), ErrorCode> { self.source.enable_interrupts(edge); Ok(()) } + #[flux_rs::no_panic] fn disable_interrupts(&self) { self.source.disable_interrupts(); } @@ -333,6 +342,7 @@ impl<'a, IP: InterruptPin<'a>> Configure for InterruptValueWrapper<'a, IP> { self.source.disable_output() } + #[flux_rs::no_panic] fn make_input(&self) -> Configuration { self.source.make_input() } @@ -345,6 +355,7 @@ impl<'a, IP: InterruptPin<'a>> Configure for InterruptValueWrapper<'a, IP> { self.source.deactivate_to_low_power(); } + #[flux_rs::no_panic] fn set_floating_state(&self, state: FloatingState) { self.source.set_floating_state(state); } diff --git a/kernel/src/hil/led.rs b/kernel/src/hil/led.rs index 3589d0d315..5ca7be308d 100644 --- a/kernel/src/hil/led.rs +++ b/kernel/src/hil/led.rs @@ -16,15 +16,19 @@ use crate::hil::gpio; /// well. pub trait Led { /// Initialize the LED. Must be called before the LED is used. + #[flux_rs::no_panic] fn init(&self); /// Turn the LED on. + #[flux_rs::no_panic] fn on(&self); /// Turn the LED off. + #[flux_rs::no_panic] fn off(&self); /// Toggle the LED. + #[flux_rs::no_panic] fn toggle(&self); /// Return the on/off state of the LED. `true` if the LED is on, `false` if diff --git a/kernel/src/hil/spi.rs b/kernel/src/hil/spi.rs index 9731ebbc17..1cbea0a26a 100644 --- a/kernel/src/hil/spi.rs +++ b/kernel/src/hil/spi.rs @@ -435,6 +435,7 @@ pub trait SpiSlaveDevice<'a> { /// - Err(INVAL): the `len` parameter is 0 /// /// `Err` return values return the passed buffer `Option`s. + #[flux_rs::no_panic] fn read_write_bytes( &self, write_buffer: Option<&'static mut [u8]>, @@ -453,8 +454,10 @@ pub trait SpiSlaveDevice<'a> { /// - Err(BUSY): the SPI bus is busy with a `read_write_bytes` /// operation whose callback hasn't been called yet. /// - Err(FAIL): other failure + #[flux_rs::no_panic] fn set_polarity(&self, polarity: ClockPolarity) -> Result<(), ErrorCode>; /// Return the current bus polarity. + #[flux_rs::no_panic] fn get_polarity(&self) -> ClockPolarity; /// Set the bus phase (whether data is sent/received on leading or @@ -463,8 +466,10 @@ pub trait SpiSlaveDevice<'a> { /// - Err(BUSY): the SPI bus is busy with a `read_write_bytes` /// operation whose callback hasn't been called yet. /// - Err(FAIL): other failure + #[flux_rs::no_panic] fn set_phase(&self, phase: ClockPhase) -> Result<(), ErrorCode>; /// Return the current bus phase. + #[flux_rs::no_panic] fn get_phase(&self) -> ClockPhase; } diff --git a/kernel/src/hil/time.rs b/kernel/src/hil/time.rs index 7d3da0ac2c..8a625f593d 100644 --- a/kernel/src/hil/time.rs +++ b/kernel/src/hil/time.rs @@ -32,11 +32,13 @@ pub trait Ticks: Clone + Copy + From + fmt::Debug + Ord + PartialOrd + Eq { /// The return value is a `u32`, in accordance with the bit widths /// specified using the BITS associated const on Rust integer /// types. + #[flux_rs::no_panic] fn width() -> u32; /// Converts the type into a `usize`, stripping the higher bits /// it if it is larger than `usize` and filling the higher bits /// with 0 if it is smaller than `usize`. + #[flux_rs::no_panic] fn into_usize(self) -> usize; /// The amount of bits required to left-justify this ticks value @@ -44,6 +46,7 @@ pub trait Ticks: Clone + Copy + From + fmt::Debug + Ord + PartialOrd + Eq { /// usize::BITS) - 1` bits. For timers with a `width` larger than /// usize, this value will be `0` (i.e., they can simply be /// truncated to usize::BITS bits). + #[flux_rs::no_panic] fn usize_padding() -> u32 { usize::BITS.saturating_sub(Self::width()) } @@ -64,6 +67,7 @@ pub trait Ticks: Clone + Copy + From + fmt::Debug + Ord + PartialOrd + Eq { /// Convert the generic [`Frequency`] argument into a frequency /// (Hertz) describing a left-justified ticks value as returned by /// [`Ticks::into_usize_left_justified`]. + #[flux_rs::no_panic] fn usize_left_justified_scale_freq() -> u32 { F::frequency() << Self::usize_padding() } @@ -73,6 +77,7 @@ pub trait Ticks: Clone + Copy + From + fmt::Debug + Ord + PartialOrd + Eq { /// with 0 if it is smaller than `u32`. Included as a simple /// helper since Tock uses `u32` pervasively and most platforms /// are 32 bits. + #[flux_rs::no_panic] fn into_u32(self) -> u32; /// The amount of bits required to left-justify this ticks value @@ -84,6 +89,7 @@ pub trait Ticks: Clone + Copy + From + fmt::Debug + Ord + PartialOrd + Eq { /// The return value is a `u32`, in accordance with the bit widths /// specified using the BITS associated const on Rust integer /// types. + #[flux_rs::no_panic] fn u32_padding() -> u32 { u32::BITS.saturating_sub(Self::width()) } @@ -97,6 +103,7 @@ pub trait Ticks: Clone + Copy + From + fmt::Debug + Ord + PartialOrd + Eq { /// `2 ** u32_padding()`). Use `u32_left_justified_scale_freq` to /// convert the underlying timer's frequency into the padded ticks /// frequency in Hertz. + #[flux_rs::no_panic] fn into_u32_left_justified(self) -> u32 { self.into_u32() << Self::u32_padding() } @@ -104,15 +111,18 @@ pub trait Ticks: Clone + Copy + From + fmt::Debug + Ord + PartialOrd + Eq { /// Convert the generic [`Frequency`] argument into a frequency /// (Hertz) describing a left-justified ticks value as returned by /// [`Ticks::into_u32_left_justified`]. + #[flux_rs::no_panic] fn u32_left_justified_scale_freq() -> u32 { F::frequency() << Self::u32_padding() } /// Add two values, wrapping around on overflow using standard /// unsigned arithmetic. + #[flux_rs::no_panic] fn wrapping_add(self, other: Self) -> Self; /// Subtract two values, wrapping around on underflow using standard /// unsigned arithmetic. + #[flux_rs::no_panic] fn wrapping_sub(self, other: Self) -> Self; /// Returns whether the value is in the range of [`start, `end`) using @@ -120,6 +130,7 @@ pub trait Ticks: Clone + Copy + From + fmt::Debug + Ord + PartialOrd + Eq { /// if, incrementing from `start`, the value will be reached before `end`. /// Put another way, it returns `(self - start) < (end - start)` in /// unsigned arithmetic. + #[flux_rs::no_panic] fn within_range(self, start: Self, end: Self) -> bool; /// Returns the maximum value of this type, which should be (2^width)-1. @@ -143,6 +154,7 @@ pub trait Ticks: Clone + Copy + From + fmt::Debug + Ord + PartialOrd + Eq { /// an associated type for an implementation of the `Time` trait. pub trait Frequency { /// Returns frequency in Hz. + #[flux_rs::no_panic] #[flux_rs::sig(fn() -> u32{r: r > 0})] fn frequency() -> u32; } @@ -159,6 +171,7 @@ pub trait Time { /// a sample of a counter; if an implementation relies on /// it being constant or changing it should use `Timestamp` /// or `Counter`. + #[flux_rs::no_panic] fn now(&self) -> Self::Ticks; } @@ -305,6 +318,7 @@ pub trait Alarm<'a>: Time { /// and `dt` rather than a single value denoting the counter value so it /// can distinguish between alarms which have very recently already /// passed and those in the far far future (see #1651). + #[flux_rs::no_panic] fn set_alarm(&self, reference: Self::Ticks, dt: Self::Ticks); /// Return the current alarm value. This is undefined at boot and @@ -317,6 +331,7 @@ pub trait Alarm<'a>: Time { /// the callback in the future /// - `Err(ErrorCode::FAIL)` the alarm could not be disarmed and will invoke /// the callback in the future + #[flux_rs::no_panic] fn disarm(&self) -> Result<(), ErrorCode>; /// Returns whether the alarm is currently armed. Note that this diff --git a/kernel/src/hil/uart.rs b/kernel/src/hil/uart.rs index 4614b1000d..439bd6ca12 100644 --- a/kernel/src/hil/uart.rs +++ b/kernel/src/hil/uart.rs @@ -115,6 +115,7 @@ pub trait Transmit<'a> { /// /// Calling `transmit_buffer` while there is an outstanding /// `transmit_buffer` or `transmit_word` operation will return BUSY. + #[flux_rs::no_panic] fn transmit_buffer( &self, tx_buffer: &'static mut [u8], @@ -184,6 +185,7 @@ pub trait Receive<'a> { /// should use `receive_word`. Calling `receive_buffer` while /// there is an outstanding `receive_buffer` or `receive_word` /// operation will return `Err(BUSY, rx_buffer)`. + #[flux_rs::no_panic] fn receive_buffer( &self, rx_buffer: &'static mut [u8], @@ -215,6 +217,7 @@ pub trait Receive<'a> { /// of `CANCEL`. If there was a reception outstanding, which is /// not cancelled successfully, then `FAIL` will be returned and /// there will be a later callback. + #[flux_rs::no_panic] fn receive_abort(&self) -> Result<(), ErrorCode>; } diff --git a/kernel/src/syscall_driver.rs b/kernel/src/syscall_driver.rs index e37f3f239b..abfa4d8370 100644 --- a/kernel/src/syscall_driver.rs +++ b/kernel/src/syscall_driver.rs @@ -30,6 +30,7 @@ impl CommandReturn { } /// Command error + #[flux_rs::no_panic] pub fn failure(rc: ErrorCode) -> Self { CommandReturn(SyscallReturn::Failure(rc)) } @@ -50,11 +51,13 @@ impl CommandReturn { } /// Successful command + #[flux_rs::no_panic] pub fn success() -> Self { CommandReturn(SyscallReturn::Success) } /// Successful command with an additional 32-bit data field + #[flux_rs::no_panic] pub fn success_u32(data0: u32) -> Self { CommandReturn(SyscallReturn::SuccessU32(data0)) } From 40f19f6cb74f91b7ada17ebcd7391d41fb0654dd Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Fri, 21 Nov 2025 14:11:28 -0800 Subject: [PATCH 07/14] Progress on the way to resolving processbuffer panics --- flux_support/src/extern_specs/func.rs | 5 +++++ flux_support/src/extern_specs/mod.rs | 1 + flux_support/src/extern_specs/option.rs | 5 +++++ flux_support/src/extern_specs/partial_cmp.rs | 7 +++++++ flux_support/src/extern_specs/slice.rs | 3 ++- 5 files changed, 20 insertions(+), 1 deletion(-) create mode 100644 flux_support/src/extern_specs/func.rs diff --git a/flux_support/src/extern_specs/func.rs b/flux_support/src/extern_specs/func.rs new file mode 100644 index 0000000000..2d9bb3f1e6 --- /dev/null +++ b/flux_support/src/extern_specs/func.rs @@ -0,0 +1,5 @@ +// #[flux_rs::extern_spec] +// trait FnOnce { +// #[flux_rs::no_panic] +// fn call_once(&self) -> Self::Output; +// } \ No newline at end of file diff --git a/flux_support/src/extern_specs/mod.rs b/flux_support/src/extern_specs/mod.rs index 63d0c44820..bff6a0be40 100644 --- a/flux_support/src/extern_specs/mod.rs +++ b/flux_support/src/extern_specs/mod.rs @@ -1,5 +1,6 @@ mod cell; mod cmp; +mod func; mod iter; mod mem; mod non_null; diff --git a/flux_support/src/extern_specs/option.rs b/flux_support/src/extern_specs/option.rs index 46daa6c586..a3d9b685f9 100644 --- a/flux_support/src/extern_specs/option.rs +++ b/flux_support/src/extern_specs/option.rs @@ -15,6 +15,11 @@ impl Option { #[sig(fn(&Option[@b]) -> bool[!b])] const fn is_none(&self) -> bool; + #[flux_rs::no_panic] + fn map_or(self, default: U, f: F) -> U + where + F: FnOnce(T) -> U; + #[flux_rs::no_panic] fn unwrap_or_default(self) -> T where diff --git a/flux_support/src/extern_specs/partial_cmp.rs b/flux_support/src/extern_specs/partial_cmp.rs index 76e3de6cdb..62b57ac717 100644 --- a/flux_support/src/extern_specs/partial_cmp.rs +++ b/flux_support/src/extern_specs/partial_cmp.rs @@ -16,3 +16,10 @@ trait PartialOrd: PartialEq { fn lt(&self, other: &Rhs) -> bool; fn le(&self, other: &Rhs) -> bool; } + + +#[flux_rs::extern_spec(core::cmp)] +trait PartialEq { + #[flux_rs::no_panic] + fn eq(&self, other: &Rhs) -> bool; +} \ No newline at end of file diff --git a/flux_support/src/extern_specs/slice.rs b/flux_support/src/extern_specs/slice.rs index af341a667c..d9d828b628 100644 --- a/flux_support/src/extern_specs/slice.rs +++ b/flux_support/src/extern_specs/slice.rs @@ -23,5 +23,6 @@ impl [T] { fn iter(v: &[T]) -> Iter<'_, T>; // #[flux_rs::sig(fn(&[T][@len], I[@idx]) -> Option<_>[>::in_bounds(idx, len)])] - // fn get(&self, index: I) -> Option<&>::Output>; + #[flux_rs::no_panic] + fn get>(&self, index: I) -> Option<&>::Output>; } From 4966c7074cb1bf20404803fab860b9be5df8831e Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Fri, 21 Nov 2025 14:12:02 -0800 Subject: [PATCH 08/14] Mark kernel functions trusted/no_panic --- kernel/src/kernel.rs | 3 +++ kernel/src/process.rs | 2 ++ kernel/src/processbuffer.rs | 7 +++++++ 3 files changed, 12 insertions(+) diff --git a/kernel/src/kernel.rs b/kernel/src/kernel.rs index 2caa39a857..9c2e4bb4a3 100644 --- a/kernel/src/kernel.rs +++ b/kernel/src/kernel.rs @@ -100,6 +100,7 @@ impl Kernel { /// Helper function that moves all non-generic portions of process_map_or /// into a non-generic function to reduce code bloat from monomorphization. + #[flux_rs::no_panic] pub(crate) fn get_process(&self, processid: ProcessId) -> Option<&dyn process::Process> { // We use the index in the [`ProcessId`] so we can do a direct lookup. // However, we are not guaranteed that the app still exists at that @@ -129,6 +130,8 @@ impl Kernel { /// different index in the processes array. Note that a match _will_ be /// found if the process still exists in the correct location in the array /// but is in any "stopped" state. + #[flux_rs::trusted] + #[flux_rs::no_panic] pub(crate) fn process_map_or(&self, default: R, processid: ProcessId, closure: F) -> R where F: FnOnce(&dyn process::Process) -> R, diff --git a/kernel/src/process.rs b/kernel/src/process.rs index e162fd74d9..abfe3c8f9c 100644 --- a/kernel/src/process.rs +++ b/kernel/src/process.rs @@ -94,6 +94,7 @@ pub struct ProcessId { } impl PartialEq for ProcessId { + #[flux_rs::no_panic] fn eq(&self, other: &ProcessId) -> bool { self.identifier == other.identifier } @@ -330,6 +331,7 @@ impl BinaryVersion { /// schedule. pub trait Process { /// Returns the process's identifier. + #[flux_rs::no_panic] fn processid(&self) -> ProcessId; /// Returns the [`ShortId`] generated by the application binary checker at diff --git a/kernel/src/processbuffer.rs b/kernel/src/processbuffer.rs index 63dc71083c..ce3068a43a 100644 --- a/kernel/src/processbuffer.rs +++ b/kernel/src/processbuffer.rs @@ -51,6 +51,8 @@ use flux_support::*; /// /// It is sound for multiple overlapping [`ReadableProcessSlice`]s or /// [`WriteableProcessSlice`]s to be in scope at the same time. +#[flux_rs::trusted] +#[flux_rs::no_panic] unsafe fn raw_processbuf_to_roprocessslice<'a>( ptr: FluxPtrU8Mut, len: usize, @@ -158,6 +160,7 @@ pub trait ReadableProcessBuffer { /// # Default Process Buffer /// /// A default instance of a process buffer must return 0. + #[flux_rs::no_panic] fn len(&self) -> usize; /// Pointer to the first byte of the userspace memory region. @@ -189,6 +192,7 @@ pub trait ReadableProcessBuffer { /// A default instance of a process buffer must return /// `Err(process::Error::NoSuchApp)` without executing the passed /// closure. + #[flux_rs::no_panic] fn enter(&self, fun: F) -> Result where F: FnOnce(&ReadableProcessSlice) -> R; @@ -311,6 +315,7 @@ impl ReadOnlyProcessBuffer { impl ReadableProcessBuffer for ReadOnlyProcessBuffer { /// Return the length of the buffer in bytes. + #[flux_rs::no_panic] fn len(&self) -> usize { self.process_id .map_or(0, |pid| pid.kernel.process_map_or(0, pid, |_| self.len)) @@ -329,6 +334,8 @@ impl ReadableProcessBuffer for ReadOnlyProcessBuffer { /// /// This verifies the process is still valid before accessing the underlying /// memory. + #[flux_rs::no_panic] + #[flux_rs::trusted] fn enter(&self, fun: F) -> Result where F: FnOnce(&ReadableProcessSlice) -> R, From d124834192a497672f63c54c19a6a5b8788084dd Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Fri, 21 Nov 2025 14:40:52 -0800 Subject: [PATCH 09/14] I have eliminated processbuffer panics... yes... --- flux_support/src/extern_specs/slice.rs | 7 +++++++ kernel/src/grant.rs | 2 ++ kernel/src/processbuffer.rs | 18 ++++++++++++++++++ 3 files changed, 27 insertions(+) diff --git a/flux_support/src/extern_specs/slice.rs b/flux_support/src/extern_specs/slice.rs index d9d828b628..8e8bf728e4 100644 --- a/flux_support/src/extern_specs/slice.rs +++ b/flux_support/src/extern_specs/slice.rs @@ -19,6 +19,7 @@ impl [T] { #[flux_rs::sig(fn(&[T][@len]) -> usize[len])] fn len(v: &[T]) -> usize; + #[flux_rs::no_panic] #[flux_rs::sig(fn(&[T][@len]) -> Iter[0, len])] fn iter(v: &[T]) -> Iter<'_, T>; @@ -26,3 +27,9 @@ impl [T] { #[flux_rs::no_panic] fn get>(&self, index: I) -> Option<&>::Output>; } + +#[flux_rs::extern_spec] +impl> core::ops::Index for [T] { + #[flux_rs::no_panic] + fn index(&self, index: I) -> &I::Output; +} \ No newline at end of file diff --git a/kernel/src/grant.rs b/kernel/src/grant.rs index d086ef6e8f..12c1b4d515 100644 --- a/kernel/src/grant.rs +++ b/kernel/src/grant.rs @@ -542,12 +542,14 @@ impl<'a, T: 'a + ?Sized> GrantData<'a, T> { impl<'a, T: 'a + ?Sized> Deref for GrantData<'a, T> { type Target = T; + #[flux_rs::no_panic] fn deref(&self) -> &T { self.data } } impl<'a, T: 'a + ?Sized> DerefMut for GrantData<'a, T> { + #[flux_rs::no_panic] fn deref_mut(&mut self) -> &mut T { self.data } diff --git a/kernel/src/processbuffer.rs b/kernel/src/processbuffer.rs index ce3068a43a..f58cd7cb0b 100644 --- a/kernel/src/processbuffer.rs +++ b/kernel/src/processbuffer.rs @@ -406,6 +406,7 @@ impl ReadOnlyProcessBufferRef<'_> { impl Deref for ReadOnlyProcessBufferRef<'_> { type Target = ReadOnlyProcessBuffer; + #[flux_rs::no_panic] fn deref(&self) -> &Self::Target { &self.buf } @@ -533,6 +534,7 @@ impl ReadWriteProcessBuffer { impl ReadableProcessBuffer for ReadWriteProcessBuffer { /// Return the length of the buffer in bytes. #[flux_rs::sig(fn (&Self[@p]) -> usize{len: valid_size(p.ptr + len)})] + #[flux_rs::no_panic] fn len(&self) -> usize { self.process_id .map_or(0, |pid| pid.kernel.process_map_or(0, pid, |_| self.len)) @@ -586,6 +588,8 @@ impl ReadableProcessBuffer for ReadWriteProcessBuffer { } impl WriteableProcessBuffer for ReadWriteProcessBuffer { + #[flux_rs::trusted] + #[flux_rs::no_panic] fn mut_enter(&self, fun: F) -> Result where F: FnOnce(&WriteableProcessSlice) -> R, @@ -653,6 +657,7 @@ impl ReadWriteProcessBufferRef<'_> { impl Deref for ReadWriteProcessBufferRef<'_> { type Target = ReadWriteProcessBuffer; + #[flux_rs::no_panic] fn deref(&self) -> &Self::Target { &self.buf } @@ -690,6 +695,7 @@ pub struct ReadableProcessByte { impl ReadableProcessByte { #[inline] + #[flux_rs::no_panic] pub fn get(&self) -> u8 { self.cell.get() } @@ -712,6 +718,8 @@ pub struct ReadableProcessSlice { slice: [ReadableProcessByte], } +#[flux_rs::trusted] +#[flux_rs::no_panic] fn cast_byte_slice_to_process_slice(byte_slice: &[ReadableProcessByte]) -> &ReadableProcessSlice { // As ReadableProcessSlice is a transparent wrapper around its inner type, // [ReadableProcessByte], we can safely transmute a reference to the inner @@ -805,11 +813,13 @@ impl ReadableProcessSlice { } /// Return the length of the slice in bytes. + #[flux_rs::no_panic] pub fn len(&self) -> usize { self.slice.len() } /// Return an iterator over the bytes of the slice. + #[flux_rs::no_panic] pub fn iter(&self) -> core::slice::Iter<'_, ReadableProcessByte> { self.slice.iter() } @@ -827,6 +837,7 @@ impl ReadableProcessSlice { /// Access a portion of the slice with bounds checking. If the access is not /// within the slice then `None` is returned. + #[flux_rs::no_panic] pub fn get(&self, range: Range) -> Option<&ReadableProcessSlice> { if let Some(slice) = self.slice.get(range) { Some(cast_byte_slice_to_process_slice(slice)) @@ -860,6 +871,7 @@ impl Index> for ReadableProcessSlice { // Subslicing will still yield a ReadableProcessSlice reference type Output = Self; + #[flux_rs::no_panic] fn index(&self, idx: Range) -> &Self::Output { cast_byte_slice_to_process_slice(&self.slice[idx]) } @@ -914,6 +926,8 @@ pub struct WriteableProcessSlice { slice: [Cell], } +#[flux_rs::trusted] +#[flux_rs::no_panic] fn cast_cell_slice_to_process_slice(cell_slice: &[Cell]) -> &WriteableProcessSlice { // # Safety // @@ -1046,11 +1060,13 @@ impl WriteableProcessSlice { } /// Return the length of the slice in bytes. + #[flux_rs::no_panic] pub fn len(&self) -> usize { self.slice.len() } /// Return an iterator over the slice. + #[flux_rs::no_panic] pub fn iter(&self) -> core::slice::Iter<'_, Cell> { self.slice.iter() } @@ -1101,6 +1117,7 @@ impl Index> for WriteableProcessSlice { // Subslicing will still yield a WriteableProcessSlice reference. type Output = Self; + #[flux_rs::no_panic] fn index(&self, idx: Range) -> &Self::Output { cast_cell_slice_to_process_slice(&self.slice[idx]) } @@ -1131,6 +1148,7 @@ impl Index for WriteableProcessSlice { #[flux_rs::trusted_impl(reason = "needs associated refinement on Index trait")] #[flux_rs::sig(fn(self: &WriteableProcessSlice[@len], idx: usize) -> &Self::Output requires len > idx)] + #[flux_rs::no_panic] fn index(&self, idx: usize) -> &Self::Output { // As WriteableProcessSlice is a transparent wrapper around // its inner type, [Cell], we can use the regular slicing From be0ac5c4ee40fd4f70973e1cfb6e874e8b4e579d Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Sun, 30 Nov 2025 16:00:48 -0800 Subject: [PATCH 10/14] Stomped everything in the kernel --- flux_support/src/extern_specs/cell.rs | 9 ++++++ flux_support/src/extern_specs/cmp.rs | 6 +++- flux_support/src/extern_specs/default.rs | 5 ++++ flux_support/src/extern_specs/fmt.rs | 0 flux_support/src/extern_specs/iter.rs | 21 ++++++++------ flux_support/src/extern_specs/mem.rs | 7 +++++ flux_support/src/extern_specs/mod.rs | 3 ++ flux_support/src/extern_specs/num.rs | 3 ++ flux_support/src/extern_specs/option.rs | 10 +++++++ flux_support/src/extern_specs/ptr.rs | 15 ++++++++++ flux_support/src/extern_specs/range.rs | 13 +++++++++ flux_support/src/extern_specs/result.rs | 13 +++++++++ flux_support/src/extern_specs/slice.rs | 6 ++++ flux_support/src/lib.rs | 4 +++ kernel/src/errorcode.rs | 1 + kernel/src/grant.rs | 34 +++++++++++++++++++++++ kernel/src/process.rs | 4 +++ kernel/src/processbuffer.rs | 4 +++ kernel/src/upcall.rs | 8 ++++++ libraries/tock-cells/Cargo.toml | 8 ++++++ libraries/tock-cells/src/optional_cell.rs | 13 +++++++++ libraries/tock-cells/src/take_cell.rs | 8 ++++++ 22 files changed, 185 insertions(+), 10 deletions(-) create mode 100644 flux_support/src/extern_specs/default.rs create mode 100644 flux_support/src/extern_specs/fmt.rs create mode 100644 flux_support/src/extern_specs/ptr.rs diff --git a/flux_support/src/extern_specs/cell.rs b/flux_support/src/extern_specs/cell.rs index cf808e877a..995dbcb63c 100644 --- a/flux_support/src/extern_specs/cell.rs +++ b/flux_support/src/extern_specs/cell.rs @@ -16,4 +16,13 @@ impl Cell { #[flux_rs::no_panic] fn set(&self, value: T); + + #[flux_rs::no_panic] + fn replace(&self, val: T) -> T; +} + +#[flux_rs::extern_spec(core::cell)] +impl Cell { + #[flux_rs::no_panic] + fn take(&self) -> T; } \ No newline at end of file diff --git a/flux_support/src/extern_specs/cmp.rs b/flux_support/src/extern_specs/cmp.rs index 2110b3d9a9..0ad6166780 100644 --- a/flux_support/src/extern_specs/cmp.rs +++ b/flux_support/src/extern_specs/cmp.rs @@ -1,3 +1,7 @@ #[flux_rs::extern_spec(core::cmp)] #[flux_rs::no_panic] -fn min(v1: T, v2: T) -> T; \ No newline at end of file +fn min(v1: T, v2: T) -> T; + +#[flux_rs::extern_spec(core::cmp)] +#[flux_rs::no_panic] +fn max(v1: T, v2: T) -> T; \ No newline at end of file diff --git a/flux_support/src/extern_specs/default.rs b/flux_support/src/extern_specs/default.rs new file mode 100644 index 0000000000..49179fd666 --- /dev/null +++ b/flux_support/src/extern_specs/default.rs @@ -0,0 +1,5 @@ +#[flux_rs::extern_spec(core::default)] +trait Default { + #[flux_rs::no_panic] + fn default() -> Self; +} \ No newline at end of file diff --git a/flux_support/src/extern_specs/fmt.rs b/flux_support/src/extern_specs/fmt.rs new file mode 100644 index 0000000000..e69de29bb2 diff --git a/flux_support/src/extern_specs/iter.rs b/flux_support/src/extern_specs/iter.rs index 5ac46ff3ba..f03fcc72de 100644 --- a/flux_support/src/extern_specs/iter.rs +++ b/flux_support/src/extern_specs/iter.rs @@ -33,15 +33,18 @@ impl IntoIterator for I { // #[flux_rs::extern_spec(std::iter)] // #[flux_rs::assoc(fn done(self: Self) -> bool )] // #[flux_rs::assoc(fn step(self: Self, other: Self) -> bool )] -// trait Iterator { -// #[flux_rs::sig(fn(self: &strg Self[@curr_s]) -> Option[!::done(curr_s)] ensures self: Self{next_s: ::step(curr_s, next_s)})] -// fn next(&mut self) -> Option; - -// #[flux_rs::sig(fn(Self[@s]) -> Enumerate[0, s])] -// fn enumerate(self) -> Enumerate -// where -// Self: Sized; -// } + +#[flux_rs::extern_spec(core::iter)] +trait Iterator { + #[flux_rs::no_panic] + fn find_map(&mut self, f: F) -> Option + where + Self: Sized, + F: FnMut(Self::Item) -> Option; + + #[flux_rs::no_panic] + fn next(&mut self) -> Option; +} // #[flux_rs::extern_spec(std::slice)] // #[flux_rs::assoc(fn done(x: Iter) -> bool { x.idx >= x.len })] diff --git a/flux_support/src/extern_specs/mem.rs b/flux_support/src/extern_specs/mem.rs index 6479a63993..d2aab51e05 100644 --- a/flux_support/src/extern_specs/mem.rs +++ b/flux_support/src/extern_specs/mem.rs @@ -2,4 +2,11 @@ // https://doc.rust-lang.org/reference/type-layout.html #[flux_rs::extern_spec(core::mem)] #[flux_rs::sig(fn() -> usize{align: align > 0})] +#[flux_rs::no_panic] fn align_of() -> usize; + + + +#[flux_rs::extern_spec(core::mem)] +#[flux_rs::no_panic] +fn size_of() -> usize; \ No newline at end of file diff --git a/flux_support/src/extern_specs/mod.rs b/flux_support/src/extern_specs/mod.rs index bff6a0be40..d03251e2d0 100644 --- a/flux_support/src/extern_specs/mod.rs +++ b/flux_support/src/extern_specs/mod.rs @@ -1,12 +1,15 @@ mod cell; mod cmp; +mod default; mod func; +mod fmt; mod iter; mod mem; mod non_null; mod num; mod option; mod partial_cmp; +mod ptr; mod range; mod result; mod slice; \ No newline at end of file diff --git a/flux_support/src/extern_specs/num.rs b/flux_support/src/extern_specs/num.rs index e0f64154df..af199dcd44 100644 --- a/flux_support/src/extern_specs/num.rs +++ b/flux_support/src/extern_specs/num.rs @@ -12,6 +12,9 @@ impl u32 { #[flux_rs::no_panic] fn saturating_sub(self, rhs: u32) -> u32; + + #[flux_rs::no_panic] + fn from_be_bytes(bytes: [u8; 4]) -> u32; } #[flux_rs::extern_spec] diff --git a/flux_support/src/extern_specs/option.rs b/flux_support/src/extern_specs/option.rs index a3d9b685f9..193646d2a6 100644 --- a/flux_support/src/extern_specs/option.rs +++ b/flux_support/src/extern_specs/option.rs @@ -10,9 +10,11 @@ enum Option { #[flux_rs::extern_spec] impl Option { #[sig(fn(&Option[@b]) -> bool[b])] + #[flux_rs::no_panic] const fn is_some(&self) -> bool; #[sig(fn(&Option[@b]) -> bool[!b])] + #[flux_rs::no_panic] const fn is_none(&self) -> bool; #[flux_rs::no_panic] @@ -25,5 +27,13 @@ impl Option { where T: Default; + #[flux_rs::no_panic] + fn map_or_else(self, default: D, f: F) -> U + where + // Andrew note: why does this not match up with source? + D: FnOnce() -> U, + F: FnOnce(T) -> U; + #[flux_rs::no_panic] + fn ok_or(self, err: E) -> Result; } diff --git a/flux_support/src/extern_specs/ptr.rs b/flux_support/src/extern_specs/ptr.rs new file mode 100644 index 0000000000..fa171a86bd --- /dev/null +++ b/flux_support/src/extern_specs/ptr.rs @@ -0,0 +1,15 @@ +use core::marker::PointeeSized; + +#[flux_rs::extern_spec(core::ptr)] +impl NonNull { + #[flux_rs::no_panic] + fn as_ptr(self) -> *mut T; + + #[flux_rs::no_panic] + fn cast(self) -> NonNull; +} + +#[flux_rs::extern_spec(core::ptr)] +#[flux_rs::no_panic] +fn null_mut() -> *mut T; + diff --git a/flux_support/src/extern_specs/range.rs b/flux_support/src/extern_specs/range.rs index 1902df310c..90f10c685b 100644 --- a/flux_support/src/extern_specs/range.rs +++ b/flux_support/src/extern_specs/range.rs @@ -1,7 +1,10 @@ #![allow(unused)] use core::ops::Bound; +use core::ops; use core::ops::{Range, RangeBounds}; +use core::iter::Step; + #[flux_rs::extern_spec] #[flux_rs::refined_by(included: bool, unbounded: bool)] @@ -54,6 +57,16 @@ trait RangeBounds { // } } + +#[flux_rs::extern_spec(core::iter)] +trait Step {} + +#[flux_rs::extern_spec(core::ops)] +impl Iterator for ops::Range { + #[flux_rs::no_panic] + fn next(&mut self) -> Option; +} + #[flux_rs::extern_spec(core::ops)] #[flux_rs::assoc(fn start(self: Range) -> T { self.end })] #[flux_rs::assoc(fn end(self: Range) -> T { self.end })] diff --git a/flux_support/src/extern_specs/result.rs b/flux_support/src/extern_specs/result.rs index 77fae5ae98..c2abfa62a4 100644 --- a/flux_support/src/extern_specs/result.rs +++ b/flux_support/src/extern_specs/result.rs @@ -12,6 +12,19 @@ impl Result { #[sig(fn(&Result[@b]) -> bool[b])] const fn is_ok(&self) -> bool; + #[flux_rs::no_panic] #[sig(fn(&Result[@b]) -> bool[!b])] const fn is_err(&self) -> bool; } + +#[flux_rs::extern_spec(core::ops)] +impl Try for Result { + #[flux_rs::no_panic] + fn branch(self) -> ControlFlow< as core::ops::Try>::Residual, as core::ops::Try>::Output>; +} + +#[flux_rs::extern_spec(core::ops)] +impl> FromResidual> for Result { + #[flux_rs::no_panic] + fn from_residual(residual: Result) -> Self; +} \ No newline at end of file diff --git a/flux_support/src/extern_specs/slice.rs b/flux_support/src/extern_specs/slice.rs index 8e8bf728e4..e30871ecd3 100644 --- a/flux_support/src/extern_specs/slice.rs +++ b/flux_support/src/extern_specs/slice.rs @@ -28,6 +28,12 @@ impl [T] { fn get>(&self, index: I) -> Option<&>::Output>; } +#[flux_rs::extern_spec(core::slice)] +impl<'a, T> Iterator for Iter<'a, T> { + #[flux_rs::no_panic] + fn next(&mut self) -> Option<&'a T>; +} + #[flux_rs::extern_spec] impl> core::ops::Index for [T] { #[flux_rs::no_panic] diff --git a/flux_support/src/lib.rs b/flux_support/src/lib.rs index 6aa9e5ceed..06f8d45395 100644 --- a/flux_support/src/lib.rs +++ b/flux_support/src/lib.rs @@ -1,4 +1,8 @@ #![no_std] +#![cfg_attr(flux, feature(step_trait))] +#![feature(try_trait_v2)] +#![feature(sized_hierarchy)] +#![feature(ptr_metadata)] mod extern_specs; mod flux_arr; diff --git a/kernel/src/errorcode.rs b/kernel/src/errorcode.rs index 887140617b..0ff9602364 100644 --- a/kernel/src/errorcode.rs +++ b/kernel/src/errorcode.rs @@ -117,6 +117,7 @@ impl From for Result<(), ErrorCode> { /// is that [`ErrorCode`], which only expresses errors, is assigned fixed /// values, but does not use value 0 by convention. This allows us to use 0 as /// success in StatusCode. +#[flux_rs::no_panic] pub fn into_statuscode(r: Result<(), ErrorCode>) -> usize { match r { Ok(()) => 0, diff --git a/kernel/src/grant.rs b/kernel/src/grant.rs index 12c1b4d515..2f759a4b1d 100644 --- a/kernel/src/grant.rs +++ b/kernel/src/grant.rs @@ -310,6 +310,12 @@ impl<'a> EnteredGrantKernelManagedLayout<'a> { /// not be any other `EnteredGrantKernelManagedLayout` for /// the given `base_ptr` at the same time, otherwise multiple mutable /// references to the same upcall/allow slices could be created. + #[flux_rs::no_panic] + // Andrew note: this is here because marking this as _not_ trusted + // yields a lot of verification burden about core::ptr::* that is a lot right now. + // We can come back to it, but I don't think flux even lets you write extern + // specs for those functions yet. + #[flux_rs::trusted] unsafe fn initialize_from_counts( base_ptr: NonNull, upcalls_num_val: UpcallItems, @@ -350,6 +356,7 @@ impl<'a> EnteredGrantKernelManagedLayout<'a> { /// which is guaranteed from align_of rust calls. #[flux_rs::opts(check_overflow = "none")] // TRUSTED: Not relevant for proof #[flux_rs::sig(fn(UpcallItems, AllowRoItems, AllowRwItems, GrantDataSize[@data_sz], GrantDataAlign{g: g > 0}) -> usize{alloc_sz: alloc_sz >= data_sz})] + #[flux_rs::no_panic] fn grant_size( upcalls_num: UpcallItems, allow_ro_num: AllowRoItems, @@ -359,6 +366,7 @@ impl<'a> EnteredGrantKernelManagedLayout<'a> { ) -> usize { #[flux_rs::trusted(reason = "arithmetic operation may overflow (bitwise arithmetic)")] #[flux_rs::sig(fn(usize, align:usize{0 < align}) -> usize{n: 0 < n && n < align})] + #[flux_rs::no_panic] fn calc_padding(kernel_managed_size: usize, align: usize) -> usize { // We know that grant_t_align is a power of 2, so we can make a mask // that will save only the remainder bits. @@ -367,6 +375,8 @@ impl<'a> EnteredGrantKernelManagedLayout<'a> { // Determine padding to get to the next multiple of grant_t_align by // taking the remainder and subtracting that from the alignment, then // ensuring a full alignment value maps to 0. + // Andrew note: This might overflow, but it seems that this is trusted and + // we don't care? (align - (kernel_managed_size & grant_t_align_mask)) & grant_t_align_mask } @@ -384,6 +394,7 @@ impl<'a> EnteredGrantKernelManagedLayout<'a> { /// Returns the alignment of the entire grant region based on the alignment /// of data T. + #[flux_rs::no_panic] fn grant_align(grant_t_align: GrantDataAlign) -> usize { // The kernel owned memory all aligned to usize. We need to use the // higher of the two alignment to ensure our padding calculations work @@ -399,6 +410,8 @@ impl<'a> EnteredGrantKernelManagedLayout<'a> { /// least the alignment of T and points to a grant that is of size /// grant_size bytes. #[flux_rs::sig(fn(NonNull, usize[@grant_sz], GrantDataSize{data_sz: data_sz <= grant_sz}) -> NonNull)] + #[flux_rs::no_panic] + #[flux_rs::trusted] unsafe fn offset_of_grant_data_t( base_ptr: NonNull, grant_size: usize, @@ -610,6 +623,7 @@ impl<'a> GrantKernelData<'a> { /// identified by the `subscribe_num`, which must match the subscribe number /// used when the upcall was originally subscribed by a process. /// `subscribe_num`s are indexed starting at zero. + #[flux_rs::no_panic] pub fn schedule_upcall( &self, subscribe_num: usize, @@ -652,6 +666,7 @@ impl<'a> GrantKernelData<'a> { /// returns a [`crate::process::Error`] to allow for easy chaining of this /// function with the `ReadOnlyProcessBuffer::enter()` function with /// `and_then`. + #[flux_rs::no_panic] pub fn get_readonly_processbuffer( &self, allow_ro_num: usize, @@ -693,6 +708,7 @@ impl<'a> GrantKernelData<'a> { /// returns a [`crate::process::Error`] to allow for easy chaining of this /// function with the `ReadWriteProcessBuffer::enter()` function with /// `and_then`. + #[flux_rs::no_panic] pub fn get_readwrite_processbuffer( &self, allow_rw_num: usize, @@ -779,6 +795,8 @@ impl Default for SavedAllowRw { /// function is called. The memory does not need to be initialized yet. If it /// already does contain initialized memory, then those contents will be /// overwritten without being `Drop`ed first. +#[flux_rs::no_panic] +#[flux_rs::trusted] unsafe fn write_default_array(base: *mut T, num: usize) { for i in 0..num { base.add(i).write(T::default()); @@ -1014,6 +1032,8 @@ impl<'a, T: Default, Upcalls: UpcallSize, AllowROs: AllowRoSize, AllowRWs: Allow /// If the grant is already allocated or could be allocated, and the process /// is valid, this returns `Ok(ProcessGrant)`. Otherwise it returns a /// relevant error. + #[flux_rs::no_panic] + #[flux_rs::trusted] fn new( grant: &Grant, processid: ProcessId, @@ -1196,6 +1216,7 @@ impl<'a, T: Default, Upcalls: UpcallSize, AllowROs: AllowRoSize, AllowRWs: Allow /// Return a [`ProcessGrant`] for a grant in a process if the process is /// valid and that process grant has already been allocated, or `None` /// otherwise. + #[flux_rs::no_panic] fn new_if_allocated( grant: &Grant, process: &'a dyn Process, @@ -1220,6 +1241,7 @@ impl<'a, T: Default, Upcalls: UpcallSize, AllowROs: AllowRoSize, AllowRWs: Allow /// Return the [`ProcessId`] of the process this [`ProcessGrant`] is /// associated with. + #[flux_rs::no_panic] pub fn processid(&self) -> ProcessId { self.process.processid() } @@ -1234,6 +1256,11 @@ impl<'a, T: Default, Upcalls: UpcallSize, AllowROs: AllowRoSize, AllowRWs: Allow /// Note, a grant can only be entered once at a time. Attempting to call /// `.enter()` on a grant while it is already entered will result in a /// `panic!()`. See the comment in `access_grant()` for more information. + // Andrew note: We need to actually add a no_panic spec which tracks if + // this grant is entered or not. The tricky part will be that entering + // a grant is implemented in the process, so I'm not sure how to handle this. + #[flux_rs::trusted] + #[flux_rs::no_panic] pub fn enter(self, fun: F) -> R where F: FnOnce(&mut GrantData, &GrantKernelData) -> R, @@ -1734,6 +1761,7 @@ impl(&self, processid: ProcessId, fun: F) -> Result where F: FnOnce(&mut GrantData, &GrantKernelData) -> R, @@ -1780,6 +1808,10 @@ impl(&self, mut fun: F) where F: FnMut(ProcessId, &mut GrantData, &GrantKernelData), @@ -1798,6 +1830,7 @@ impl Iter<'_, T, Upcalls, AllowROs, AllowRWs> { Iter { @@ -1830,6 +1863,7 @@ impl<'a, T: Default, Upcalls: UpcallSize, AllowROs: AllowRoSize, AllowRWs: Allow { type Item = ProcessGrant<'a, T, Upcalls, AllowROs, AllowRWs>; + #[flux_rs::no_panic] fn next(&mut self) -> Option { let grant = self.grant; // Get the next `ProcessId` from the kernel processes array that is diff --git a/kernel/src/process.rs b/kernel/src/process.rs index abfe3c8f9c..a208ecba8f 100644 --- a/kernel/src/process.rs +++ b/kernel/src/process.rs @@ -373,6 +373,7 @@ pub trait Process { /// there is insufficient space in the internal task queue. /// /// Other return values must be treated as kernel-internal errors. + #[flux_rs::no_panic] fn enqueue_task(&self, task: Task) -> Result<(), ErrorCode>; /// Remove the scheduled operation from the front of the queue and return it @@ -696,6 +697,7 @@ pub trait Process { /// - There is not enough available memory to do the allocation, or /// - The grant_num is invalid, or /// - The grant_num already has an allocated grant. + #[flux_rs::no_panic] fn allocate_grant( &self, grant_num: usize, @@ -708,6 +710,7 @@ pub trait Process { /// /// Returns `None` if the process is not active. Otherwise, returns `true` /// if the grant has been allocated, `false` otherwise. + #[flux_rs::no_panic] fn grant_is_allocated(&self, grant_num: usize) -> Option; /// Allocate memory from the grant region that is `size` bytes long and @@ -733,6 +736,7 @@ pub trait Process { /// is invalid, if the grant has not been allocated, or if the grant is /// already entered. If this returns `Ok()` then the pointer points to the /// previously allocated memory for this grant. + #[flux_rs::no_panic] fn enter_grant(&self, grant_num: usize) -> Result, Error>; /// Enter a custom grant based on the `identifier`. diff --git a/kernel/src/processbuffer.rs b/kernel/src/processbuffer.rs index f58cd7cb0b..9dde6c3281 100644 --- a/kernel/src/processbuffer.rs +++ b/kernel/src/processbuffer.rs @@ -396,6 +396,8 @@ impl ReadOnlyProcessBufferRef<'_> { /// [`ReadOnlyProcessBuffer::new_external`]. The derived lifetime can /// help enforce the invariant that this incoming pointer may only /// be access for a certain duration. + #[flux_rs::trusted] + #[flux_rs::no_panic] pub(crate) unsafe fn new(ptr: FluxPtrU8Mut, len: usize, process_id: ProcessId) -> Self { Self { buf: ReadOnlyProcessBuffer::new(ptr, len, process_id), @@ -447,6 +449,7 @@ impl ReadWriteProcessBuffer { /// Refer to the safety requirements of /// [`ReadWriteProcessBuffer::new_external`]. #[flux_rs::sig(fn (FluxPtrU8Mut[@ptr], len:usize{valid_size(ptr+len)}, ProcessId) -> Self)] + #[flux_rs::no_panic] pub(crate) unsafe fn new(ptr: FluxPtrU8Mut, len: usize, process_id: ProcessId) -> Self { ReadWriteProcessBuffer { ptr, @@ -647,6 +650,7 @@ impl ReadWriteProcessBufferRef<'_> { /// help enforce the invariant that this incoming pointer may only /// be access for a certain duration. #[flux_rs::sig(fn (FluxPtrU8Mut[@ptr], len:usize{valid_size(ptr+len)}, _) -> Self)] + #[flux_rs::no_panic] pub(crate) unsafe fn new(ptr: FluxPtrU8Mut, len: usize, process_id: ProcessId) -> Self { Self { buf: ReadWriteProcessBuffer::new(ptr, len, process_id), diff --git a/kernel/src/upcall.rs b/kernel/src/upcall.rs index a719f3d37d..ffcf6b1da9 100644 --- a/kernel/src/upcall.rs +++ b/kernel/src/upcall.rs @@ -95,6 +95,7 @@ pub(crate) struct Upcall { } impl Upcall { + #[flux_rs::no_panic] pub(crate) fn new( process_id: ProcessId, upcall_id: UpcallId, @@ -124,6 +125,13 @@ impl Upcall { /// parameter so we take advantage of it. If in the future that is not the /// case we could have `process` be an Option and just do the search with /// the stored [`ProcessId`]. + #[flux_rs::no_panic] + #[flux_rs::trusted] + // Andrew note: marking this as trusted because the debug! call introduces + // verification burden to annotated core::fmt::rt::blah as no_panic!. + // The symbols referred to in core::fmt::rt are things like new_v1_formatted, + // which may have been patched out? In any case, it's hard to get working on + // my machine. pub(crate) fn schedule( &self, process: &dyn process::Process, diff --git a/libraries/tock-cells/Cargo.toml b/libraries/tock-cells/Cargo.toml index 882e8540f0..1937d6d03f 100644 --- a/libraries/tock-cells/Cargo.toml +++ b/libraries/tock-cells/Cargo.toml @@ -11,3 +11,11 @@ edition = "2021" [lints] workspace = true + +[dependencies] +flux-rs = { git = "https://github.com/flux-rs/flux.git" } +flux_support = { path = "../../flux_support" } + +[package.metadata.flux] +enabled = true +check_overflow = "lazy" \ No newline at end of file diff --git a/libraries/tock-cells/src/optional_cell.rs b/libraries/tock-cells/src/optional_cell.rs index b0e15e5c11..29b7b95a48 100644 --- a/libraries/tock-cells/src/optional_cell.rs +++ b/libraries/tock-cells/src/optional_cell.rs @@ -6,6 +6,8 @@ use core::cell::Cell; +use flux_support::*; + /// `OptionalCell` is a `Cell` that wraps an `Option`. This is helper type /// that makes keeping types that can be `None` a little cleaner. pub struct OptionalCell { @@ -14,6 +16,7 @@ pub struct OptionalCell { impl OptionalCell { /// Create a new OptionalCell. + #[flux_rs::no_panic] pub const fn new(val: T) -> OptionalCell { OptionalCell { value: Cell::new(Some(val)), @@ -21,6 +24,7 @@ impl OptionalCell { } /// Create an empty `OptionalCell` (contains just `None`). + #[flux_rs::no_panic] pub const fn empty() -> OptionalCell { OptionalCell { value: Cell::new(None), @@ -28,6 +32,7 @@ impl OptionalCell { } /// Update the stored value. + #[flux_rs::no_panic] pub fn set(&self, val: T) { self.value.set(Some(val)); } @@ -48,11 +53,13 @@ impl OptionalCell { } /// Reset the stored value to `None`. + #[flux_rs::no_panic] pub fn clear(&self) { self.value.set(None); } /// Check if the cell contains something. + #[flux_rs::no_panic] pub fn is_some(&self) -> bool { let value = self.value.take(); let out = value.is_some(); @@ -61,6 +68,7 @@ impl OptionalCell { } /// Check if the cell is None. + #[flux_rs::no_panic] pub fn is_none(&self) -> bool { let value = self.value.take(); let out = value.is_none(); @@ -137,6 +145,7 @@ impl OptionalCell { } /// Return the contained value and replace it with None. + #[flux_rs::no_panic] pub fn take(&self) -> Option { self.value.take() } @@ -211,6 +220,8 @@ impl OptionalCell { } /// Call a closure on the value if the value exists. + #[flux_rs::no_panic] + #[flux_rs::trusted] pub fn map(&self, closure: F) -> Option where F: FnOnce(T) -> R, @@ -220,6 +231,8 @@ impl OptionalCell { /// Call a closure on the value if the value exists, or return the /// default if the value is `None`. + #[flux_rs::no_panic] + #[flux_rs::trusted] pub fn map_or(&self, default: R, closure: F) -> R where F: FnOnce(T) -> R, diff --git a/libraries/tock-cells/src/take_cell.rs b/libraries/tock-cells/src/take_cell.rs index d52e01d5ae..f220c1eba5 100644 --- a/libraries/tock-cells/src/take_cell.rs +++ b/libraries/tock-cells/src/take_cell.rs @@ -24,17 +24,20 @@ impl<'a, T: ?Sized> TakeCell<'a, T> { val: Cell::new(None), }; + #[flux_rs::no_panic] pub const fn empty() -> TakeCell<'a, T> { Self::EMPTY } /// Creates a new `TakeCell` containing `value` + #[flux_rs::no_panic] pub fn new(value: &'a mut T) -> TakeCell<'a, T> { TakeCell { val: Cell::new(Some(value)), } } + #[flux_rs::no_panic] pub fn is_none(&self) -> bool { let inner = self.take(); let return_val = inner.is_none(); @@ -64,17 +67,20 @@ impl<'a, T: ?Sized> TakeCell<'a, T> { /// x.take(); /// assert_eq!(y.take(), None); /// ``` + #[flux_rs::no_panic] pub fn take(&self) -> Option<&'a mut T> { self.val.replace(None) } /// Stores `val` in the `TakeCell` + #[flux_rs::no_panic] pub fn put(&self, val: Option<&'a mut T>) { self.val.replace(val); } /// Replaces the contents of the `TakeCell` with `val`. If the cell was not /// empty, the previous value is returned, otherwise `None` is returned. + #[flux_rs::no_panic] pub fn replace(&self, val: &'a mut T) -> Option<&'a mut T> { self.val.replace(Some(val)) } @@ -125,6 +131,8 @@ impl<'a, T: ?Sized> TakeCell<'a, T> { } /// Performs a `map` or returns a default value if the `TakeCell` is empty + #[flux_rs::trusted] // Andrew: marking as trusted because of FnOnce::call_once + #[flux_rs::no_panic] pub fn map_or(&self, default: R, closure: F) -> R where F: FnOnce(&mut T) -> R, From 5ceab217ead03ea7494ff6e4d5635fccd446f2b8 Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Sun, 30 Nov 2025 16:20:23 -0800 Subject: [PATCH 11/14] Squash option, result --- flux_support/src/extern_specs/option.rs | 11 +++++++ flux_support/src/extern_specs/result.rs | 39 +++++++++++++++++++++++++ 2 files changed, 50 insertions(+) diff --git a/flux_support/src/extern_specs/option.rs b/flux_support/src/extern_specs/option.rs index 193646d2a6..6121679d27 100644 --- a/flux_support/src/extern_specs/option.rs +++ b/flux_support/src/extern_specs/option.rs @@ -22,6 +22,17 @@ impl Option { where F: FnOnce(T) -> U; + + #[flux_rs::no_panic] + fn map(self, op: F) -> Option + where + F: FnOnce(T) -> U; + + #[flux_rs::no_panic] + fn inspect(self, op: F) -> Self + where + F: FnOnce(&T); + #[flux_rs::no_panic] fn unwrap_or_default(self) -> T where diff --git a/flux_support/src/extern_specs/result.rs b/flux_support/src/extern_specs/result.rs index c2abfa62a4..32dc8612b8 100644 --- a/flux_support/src/extern_specs/result.rs +++ b/flux_support/src/extern_specs/result.rs @@ -15,6 +15,45 @@ impl Result { #[flux_rs::no_panic] #[sig(fn(&Result[@b]) -> bool[!b])] const fn is_err(&self) -> bool; + + #[flux_rs::no_panic] + fn and_then(self, op: F) -> Result + where + F: FnOnce(T) -> Result; + + #[flux_rs::no_panic] + fn map_err(self, op: O) -> Result + where + O: FnOnce(E) -> F; + + #[flux_rs::no_panic] + fn map_or(self, default: U, f: F) -> U + where + F: FnOnce(T) -> U; + + #[flux_rs::no_panic] + fn map_or_else(self, default: D, f: F) -> U + where + D: FnOnce(E) -> U, + F: FnOnce(T) -> U; + + #[flux_rs::no_panic] + fn ok(self) -> Option; + + #[flux_rs::no_panic] + fn unwrap_or(self, default: T) -> T; + + #[flux_rs::no_panic] + fn unwrap_or_default(self) -> T + where + T: Default; + + #[flux_rs::no_panic] + fn unwrap_or_else(self, op: F) -> T + where + F: FnOnce(E) -> T; + + } #[flux_rs::extern_spec(core::ops)] From 3cdbe557d0695f055f9592c34c02aed5cf5d7f89 Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Sun, 30 Nov 2025 17:36:46 -0800 Subject: [PATCH 12/14] Add extern specifications for From trait and enhance Iterator trait methods --- flux_support/src/extern_specs/from.rs | 13 +++++++ flux_support/src/extern_specs/iter.rs | 49 ++++++++++++++++++++++++++- flux_support/src/extern_specs/mod.rs | 1 + 3 files changed, 62 insertions(+), 1 deletion(-) create mode 100644 flux_support/src/extern_specs/from.rs diff --git a/flux_support/src/extern_specs/from.rs b/flux_support/src/extern_specs/from.rs new file mode 100644 index 0000000000..de0497feb8 --- /dev/null +++ b/flux_support/src/extern_specs/from.rs @@ -0,0 +1,13 @@ +#[flux_rs::extern_spec(core::convert)] +trait From: Sized { + #[flux_rs::no_panic] + fn from(value: T) -> Self; +} + +// #[flux_rs::extern_spec(core::convert)] +// impl Into for T { +// #[flux_rs::no_panic] +// fn into(self) -> U +// where +// U: From; +// } \ No newline at end of file diff --git a/flux_support/src/extern_specs/iter.rs b/flux_support/src/extern_specs/iter.rs index f03fcc72de..6193dd5d3a 100644 --- a/flux_support/src/extern_specs/iter.rs +++ b/flux_support/src/extern_specs/iter.rs @@ -1,6 +1,7 @@ #![allow(unused)] use crate::assert; -use core::slice::Iter; +use core::iter::Enumerate; +use core::iter::FilterMap; use core::iter::IntoIterator; #[flux_rs::extern_spec(core::slice)] @@ -36,6 +37,12 @@ impl IntoIterator for I { #[flux_rs::extern_spec(core::iter)] trait Iterator { + #[flux_rs::no_panic] + fn filter_map(self, f: F) -> FilterMap + where + Self: Sized, + F: FnMut(Self::Item) -> Option; + #[flux_rs::no_panic] fn find_map(&mut self, f: F) -> Option where @@ -44,8 +51,48 @@ trait Iterator { #[flux_rs::no_panic] fn next(&mut self) -> Option; + + #[flux_rs::no_panic] + fn enumerate(self) -> Enumerate + where + Self: Sized; + + #[flux_rs::no_panic] + fn rev(self) -> Rev + where + Self: Sized + DoubleEndedIterator; + + #[flux_rs::no_panic] + fn take(self, n: usize) -> Take + where + Self: Sized; + + #[flux_rs::no_panic] + fn zip(self, other: U) -> Zip + where + Self: Sized, + U: IntoIterator; } +#[flux_rs::extern_spec(core::iter)] +struct Enumerate; + +#[flux_rs::extern_spec(core::iter)] +impl Iterator for Enumerate { + // Andrew note: This indeed can panic! + // Don't merge until we create a refinement for this so that + // we can't call it unless we're sure it won't panic. + #[flux_rs::no_panic] + fn next(&mut self) -> Option<(usize, I::Item)>; +} + +#[flux_rs::extern_spec(core::iter)] +impl Iterator for Zip { + #[flux_rs::no_panic] + fn next(&mut self) -> Option< as Iterator>::Item>; +} + + // #[flux_rs::extern_spec(std::slice)] // #[flux_rs::assoc(fn done(x: Iter) -> bool { x.idx >= x.len })] // #[flux_rs::assoc(fn step(x: Iter, y: Iter) -> bool { x.idx + 1 == y.idx && x.len == y.len})] diff --git a/flux_support/src/extern_specs/mod.rs b/flux_support/src/extern_specs/mod.rs index d03251e2d0..64e71694f0 100644 --- a/flux_support/src/extern_specs/mod.rs +++ b/flux_support/src/extern_specs/mod.rs @@ -3,6 +3,7 @@ mod cmp; mod default; mod func; mod fmt; +mod from; mod iter; mod mem; mod non_null; From a7f83d68c9914f6ccd8a441512b6e4e793a5390c Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Sun, 30 Nov 2025 17:53:59 -0800 Subject: [PATCH 13/14] The last of it --- capsules/core/Cargo.toml | 1 + capsules/core/src/alarm.rs | 7 ++++++- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/capsules/core/Cargo.toml b/capsules/core/Cargo.toml index b022693278..56aa411949 100644 --- a/capsules/core/Cargo.toml +++ b/capsules/core/Cargo.toml @@ -12,6 +12,7 @@ edition.workspace = true kernel = { path = "../../kernel" } enum_primitive = { path = "../../libraries/enum_primitive" } tickv = { path = "../../libraries/tickv" } +flux-rs = { git = "https://github.com/flux-rs/flux.git" } [package.metadata.flux] enabled = true diff --git a/capsules/core/src/alarm.rs b/capsules/core/src/alarm.rs index cbab6e5234..780088ef2a 100644 --- a/capsules/core/src/alarm.rs +++ b/capsules/core/src/alarm.rs @@ -9,6 +9,7 @@ use kernel::grant::{AllowRoCount, AllowRwCount, Grant, UpcallCount}; use kernel::hil::time::{self, Alarm, Ticks}; use kernel::syscall::{CommandReturn, SyscallDriver}; use kernel::{ErrorCode, ProcessId}; +use kernel::process; /// Syscall driver number. use crate::driver; @@ -76,6 +77,8 @@ impl<'a, A: Alarm<'a>> AlarmDriver<'a, A> { /// To stop iteration on any expired [`Expiration`], its callback can return /// `Some(R)`. Then this function will return `Err(Expiration, UD, R)`. /// This avoids consuming the entire iterator. + #[flux_rs::no_panic] + #[flux_rs::trusted] // Andrew note: trusted because of closure usage fn earliest_alarm, &UD) -> Option>( now: A::Ticks, expirations: impl Iterator, UD, F)>, @@ -150,6 +153,8 @@ impl<'a, A: Alarm<'a>> AlarmDriver<'a, A> { /// - invoke upcalls for all expired app alarms, resetting them afterwards, /// - re-arming the alarm for the next earliest [`Expiration`], or /// - disarming the alarm if no unexpired [`Expiration`] is found. + #[flux_rs::no_panic] + #[flux_rs::trusted] // Andrew note: The `unreachable!()` here needs to be a refinement fn process_rearm_or_callback(&self) { // Ask the clock about a current reference once. This can incur a // volatile read, and this may not be optimized if done in a loop: @@ -501,7 +506,7 @@ impl<'a, A: Alarm<'a>> SyscallDriver for AlarmDriver<'a, A> { } }) .map_or_else( - |err| CommandReturn::failure(err.into()), + |err: process::Error| CommandReturn::failure(err.into()), |(retval, rearm_timer)| { if rearm_timer { self.process_rearm_or_callback(); From d4e3f926777da238bff299652cea79e90652bfd8 Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Sun, 30 Nov 2025 18:06:46 -0800 Subject: [PATCH 14/14] Last extern specs --- flux_support/src/extern_specs/from.rs | 19 ++++++++++++------- flux_support/src/extern_specs/slice.rs | 10 ++++++++++ 2 files changed, 22 insertions(+), 7 deletions(-) diff --git a/flux_support/src/extern_specs/from.rs b/flux_support/src/extern_specs/from.rs index de0497feb8..70beec2b10 100644 --- a/flux_support/src/extern_specs/from.rs +++ b/flux_support/src/extern_specs/from.rs @@ -4,10 +4,15 @@ trait From: Sized { fn from(value: T) -> Self; } -// #[flux_rs::extern_spec(core::convert)] -// impl Into for T { -// #[flux_rs::no_panic] -// fn into(self) -> U -// where -// U: From; -// } \ No newline at end of file +#[flux_rs::extern_spec(core::convert)] +trait Into: Sized { + #[flux_rs::no_panic] + fn into(self) -> T; +} + + +#[flux_rs::extern_spec(core::convert)] +impl> Into for T { + #[flux_rs::no_panic] + fn into(self) -> U; +} \ No newline at end of file diff --git a/flux_support/src/extern_specs/slice.rs b/flux_support/src/extern_specs/slice.rs index e30871ecd3..f9d2cb3ff4 100644 --- a/flux_support/src/extern_specs/slice.rs +++ b/flux_support/src/extern_specs/slice.rs @@ -26,6 +26,10 @@ impl [T] { // #[flux_rs::sig(fn(&[T][@len], I[@idx]) -> Option<_>[>::in_bounds(idx, len)])] #[flux_rs::no_panic] fn get>(&self, index: I) -> Option<&>::Output>; + + #[flux_rs::no_panic] + fn copy_from_slice(&mut self, src: &[T]) where + T: Copy; } #[flux_rs::extern_spec(core::slice)] @@ -38,4 +42,10 @@ impl<'a, T> Iterator for Iter<'a, T> { impl> core::ops::Index for [T] { #[flux_rs::no_panic] fn index(&self, index: I) -> &I::Output; +} + +#[flux_rs::extern_spec] +impl> core::ops::IndexMut for [T] { + #[flux_rs::no_panic] + fn index_mut(&mut self, index: I) -> &mut I::Output; } \ No newline at end of file