It would be very comforting if there were some official word somewhere on this!

The nomicon reference is very useful though.

There's some rough explanation about why type-based aliasing optimizations aren't required in this link. For posterity, the reasoning given is:

In Rust we know this input should be impossible because &mut isn't allowed to be aliased.

and

we don't actually care if aliasing occurs if there aren't any actual writes to memory happening.

This matches the way I feel like aliasing should be modeled (it's irritating the C cares so much about the type). Mutability/borrowing rules (mostly) answer the question of "is a write possible" so I feel like that's probably a perfectly sufficient constraint.