SAFETY documentation may be inconsistent with soundness verification specifications

I recently read about the concept of library-level invariants and language-level invariants. It happens to me that there may be some gaps between the SAFETY requirements and how verification community writes their specifications. In short, someone may think that SAFETY documentation serves as good sources to write soundness specifications of unsafe functions. However, the concept of library-level invariants make this wrong: impl<T, A> Vec<T, A> { pub fn split_off(&mut self, at: usize) -> S...