[Pre-RFC] A tiny internal change to `reverse`, `copy_from_slice`, `swap_with_slice`

Lysxia:

Indeed, even outside of formal verification, one could argue that self.as_mut_ptr() "morally borrows" from self, so calling self.len() while the raw pointer self.as_mut_ptr() is still in use is kinda smelly.

I realised a while ago that raw pointers conceptually have a lifetime (which is the lifetime of their provenance, not the lifetime of the thing they point to). Under that model, you would indeed have to copy the length out of a slice reference before convering it to a pointer, if you wanted to use it at the same time as the pointer.

With current (and all likely future) Rust operational semantics, Rust code is allowed to violate the mutable borrow rules as long as they don't access any bytes of memory that the mutable reference is also used to access. As such, the following is sound (although it can't be written using safe Rust):

fn f(s: &mut [u8;2]) -> u8 {
    let p = s.as_mut_ptr();
    s[1] = 4;
    unsafe { p.write(5); }
    s[1]
}

but if you wrote s[0] twice rather than s[1], it would be undefined behaviour.

The current Rust code for swap_with_slice is effectively doing the same thing: it's creating what are conceptually overlapping mutable references, but they're accessing disjoint memory (the length and the slice contents) and thus no actual breach of unsafe Rust's rules has occurred.

In general, I'd be in favour of rewriting it to put the len() first, because (as you say) it makes the soundness analysis vastly simpler – there's no longer a need to rely on a somewhat obscure rule that is specific to unsafe Rust, meaning that proof tools that think along safe-Rust lines will be much better at understanding what is going on. (On the other hand, code like the existing code is to many programmers "obviously correct", so it's important that unsafe Rust's operational semantics permits it: there would be too much of a chance of people writing undefined code by mistake otherwise.)

I don't make the decisions, but if I did, I would probably move the len() call first with a comment saying something like "it is easier for automated proof tools to prove this code correct if it doesn't attempt to read the length through a mutable reference while a pointer derived from it is currently in use" (but ideally with better / more succinct wording).