#[flux::refined_by(ring_len: int, head: int, tail: int)]
#[flux::invariant(0 < ring_len)]
pub struct RingBuffer<'a, T: 'a> {
    #[flux::field({&mut [T][ring_len] | ring_len > 0})]
    ring: &'a mut [T],
    #[flux::field({usize[head] | head < ring_len})]
    head: usize,
    #[flux::field({usize[tail] | tail < ring_len})]
    tail: usize,
    #[flux::field({usize[ring_len] | ring_len > 0})]
    length: usize,
}

impl<'a, T: Copy + 'a> RingBuffer<'a, T> {
    fn is_full(&self) -> bool {
        todo!()
    }

    fn ring_len(&self) -> usize {
        todo!()
    }

    fn push(&mut self, val: T) -> Option<T> {
        let result = if self.is_full() {
            let val = self.ring[self.head];
            self.head = (self.head + 1) % self.ring_len();
            Some(val) // error[E0999]: error jumping to join point
        } else {
            None
        };

        self.ring[self.tail] = val;
        self.tail = (self.tail + 1) % self.ring_len();
        result
    }
}