Rust programs typically panic when you index into a slice with an out-of-bounds usize index.
Is that panic actually guaranteed to happen? Can I rely on the panic when reasoning about the soundness of (unsafe) code?
The Index trait docs do not strictly require a panic. And the specific implementation on slice does not provide any further comments.
While the answer for arbitrary SliceIndex types is also interesting, I am specifically asking about indexing with a usize. And I am less interested in looking at any current implementation, and more in documentation that I can rely on indefinitely.
Yes, this is documented.
The implementation on Index for slices reads as:
impl<T, I> Index<I> for [T]
where
I: SliceIndex<[T]>
So, we can index a slice of [T] by anything that implements SliceIndex<[T]>. The Index implementation for [T] simply delegates to the appropriate method of SliceIndex.
If we look at the documentation for impl<T> SliceIndex<[T]> for usize, it says:
The methods
indexandindex_mutpanic if the index is out of bounds.
However, unless you are writing generic code around Index, indexing a slice does not actually invoke this code path. Indexing a slice is a compiler-intrinsic operation, just like dereferencing a reference does not invoke Deref (or DerefMut) -- in fact, the Deref implementation for references just returns self.
The behavior of slices is defined in the Rust reference. In particular, type.slice.safe says:
All elements of slices are always initialized, and access to a slice is always bounds-checked in safe methods and operators.
The indexing operator is obviously safe, or you would only be able to use it from unsafe code.
Documentation aside, one of the goals of Rust is that non-unsafe could should never result in unsoundness. As explained by someone in a comment, unsafe does not change behavior but only changes what operations you are allowed to perform.
If we assume that out-of-bounds indexing of slices could result in unsound code in an unsafe block, we must conclude that it could also result in unsound code outside of them, which would be a pretty glaring soundness issue and would substantially undermine the goals of the language.
While not formal, this is kind of a reductio ad absurdum informal proof.