peel back trusted

kernel/src/collections/queue.rs

@@ -16,23 +16,19 @@ 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] // Unexpected Evar
-    // #[flux_rs::sig(fn(self: &strg Self, _) -> bool ensures self: Self)]
+    #[flux_rs::sig(fn(self: &strg Self, _) -> bool ensures self: Self)]
     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] // Unexpected Evar
-    // #[flux_rs::sig(fn(self: &strg Self, _) -> Option<T> ensures self: Self)]
+    #[flux_rs::sig(fn(self: &strg Self, _) -> Option<T> ensures self: Self)]
     fn push(&mut self, val: T) -> Option<T>;
 
     /// Remove the element from the front of the queue.
-    #[flux_rs::trusted_impl] // Unexpected Evar
-    // #[flux_rs::sig(fn(self: &strg Self) -> Option<T> ensures self: Self)]
+    #[flux_rs::sig(fn(self: &strg Self) -> Option<T> ensures self: Self)]
     fn dequeue(&mut self) -> Option<T>;
 
     /// Remove and return one (the first) element that matches the predicate.
-    #[flux_rs::trusted_impl] // Unexpected evar
-    // #[flux_rs::sig(fn(self: &strg Self, _) -> Option<T> ensures self: Self)]
+    #[flux_rs::sig(fn(self: &strg Self, _) -> Option<T> ensures self: Self)]
     fn remove_first_matching<F>(&mut self, f: F) -> Option<T>
     where
         F: Fn(&T) -> bool;