diff --git a/kernel/src/collections/queue.rs b/kernel/src/collections/queue.rs
index 906f80d3eb..25df54bf02 100644
--- a/kernel/src/collections/queue.rs
+++ b/kernel/src/collections/queue.rs
@@ -29,12 +29,14 @@ pub trait Queue<T> {
 
     /// Remove and return one (the first) element that matches the predicate.
     #[flux_rs::trusted_impl]
+    // #[flux_rs::sig(fn(self: &strg Self, _) -> Option<_> ensures self: Self)]
     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]
+    // #[flux_rs::sig(fn(self: &strg Self) ensures self: Self)]
     fn empty(&mut self);
 
     /// Retains only the elements that satisfy the predicate.
diff --git a/kernel/src/collections/ring_buffer.rs b/kernel/src/collections/ring_buffer.rs
index 54157462d9..aac1ab4776 100644
--- a/kernel/src/collections/ring_buffer.rs
+++ b/kernel/src/collections/ring_buffer.rs
@@ -176,7 +176,7 @@ impl<T: Copy> queue::Queue<T> for RingBuffer<'_, T> {
     ///
     /// If an element was removed, this function returns it as `Some(elem)`.
     #[flux_rs::sig(
-        fn(self: &strg RingBuffer<T>, _) -> Option<T> ensures self: RingBuffer<T>
+        fn(self: &strg Self, _) -> Option<_> ensures self: Self
     )]
     fn remove_first_matching<F>(&mut self, f: F) -> Option<T>
     where