From 4795e3c844be62c3dfecd8b5505e5b929a69cd70 Mon Sep 17 00:00:00 2001
From: Evan Johnson <e5johnso@eng.ucsd.edu>
Date: Fri, 22 Nov 2024 10:27:09 -0800
Subject: [PATCH] clean up ring buffer spec a bit

---
 kernel/src/collections/ring_buffer.rs | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/kernel/src/collections/ring_buffer.rs b/kernel/src/collections/ring_buffer.rs
index aac1ab4776..21b1307bcd 100644
--- a/kernel/src/collections/ring_buffer.rs
+++ b/kernel/src/collections/ring_buffer.rs
@@ -102,9 +102,6 @@ impl<T: Copy> queue::Queue<T> for RingBuffer<'_, T> {
     #[flux_rs::sig(
         fn(self: &strg RingBuffer<T>[@old], _) -> bool 
             ensures self: RingBuffer<T>{ new: 
-                // shouldn't be empty post-enqueue
-                !empty(new)
-                && 
                 // either we're full and don't update
                 (full(old) => new.tl == old.tl && new.hd == old.hd)
                 &&
@@ -126,9 +123,6 @@ impl<T: Copy> queue::Queue<T> for RingBuffer<'_, T> {
     #[flux_rs::sig(
         fn(self: &strg RingBuffer<T>[@old], _) -> Option<T> 
             ensures self: RingBuffer<T>{ new: 
-                // shouldn't be empty post-push
-                !empty(new)
-                && 
                 // the buffer is full so we dequeue and then enqueue 
                 (full(old) => (new.hd == next_hd(old) && new.tl == next_tl(old)))
                 &&