mod heap {
#[derive(Default)]
pub struct HeapArray<T, const N: usize> {
  inner: Box<[T; N]>,
}

impl<T, const N: usize> HeapArray<T, N> {
  pub fn set(&mut self, val: T, idx: usize) {
  }
}
}

mod other {
  struct Stack<T> {
     buf: HeapArray,
     next: usize,
  }

  impl<T> Stack<T> {
    #[modifies(buf)] // This is not enough today
    #[kani::ensures(|_| self.contains(val))]
    fn enqueue(&mut self, val: T) {
      assert!(!self.is_full());
      self.buf.set(val, next);
    }
  }
}