[pointer] Document validity safety invariant

Document the semantics of `Ptr` validity invariants on the `Validity`
trait.

TODO:
- [ ] Prove that this safety invariant is upheld at all transmute sites
- [ ] Consume this safety invariant wherever it's relevant

Makes progress on #2226, #1866

gherrit-pr-id: Ie66db9044be1dc310a6b7280a73652a357878376

Author: joshlf

src/pointer/invariant.rs

@@ -42,6 +42,45 @@ pub trait Aliasing: Sealed {
 pub trait Alignment: Sealed {}
 
 /// The validity invariant of a [`Ptr`][super::Ptr].
+///
+/// # Safety
+///
+/// In this section, we will use `Ptr<T, V>` as a shorthand for `Ptr<T, I:
+/// Invariants<Validity = V>>` for brevity.
+///
+/// Each `V: Validity` defines a set of bit values which may appear in the
+/// referent of a `Ptr<T, V>`. Each `V: Validity`, in its documentation,
+/// provides a definition of this set in terms of any referent type (in other
+/// words, this definition holds for all `T: ?Sized`).
+///
+/// Let `S(T, V)` be the set of bit values permitted to appear in the referent
+/// of a `ptr: Ptr<T, V>` (as defined by and documented on `V`). It is
+/// guaranteed that the referent of `ptr` is a member of `S(T, V)`. Unsafe code
+/// producing a `Ptr<T, V>` must ensure that this guarantee will be upheld.
+///
+/// An important implication of this guarantee is that it restricts what
+/// transmutes are sound, where "transmute" is used in this context to refer to
+/// changing the referent type or validity invariant of a `Ptr`, as either
+/// change may change the set of bit values permitted to appear in the referent.
+/// In particular, the following are necessary (but not sufficient) conditions
+/// in order for a transmute from `src: Ptr<T, V>` to `dst: Ptr<U, W>` to be
+/// sound:
+/// - If `S(T, V) = S(U, W)`, then no restrictions apply; otherwise,
+/// - If `dst` permits mutation of its referent (e.g. via `Exclusive` aliasing
+///   or interior mutation under `Shared` aliasing), then it must hold that
+///   `S(T, V) ⊇ S(U, W)` - in other words, the transmute must not expand the
+///   set of allowed referent bit patterns. A violation of this requirement
+///   would permit using `dst` to write `x` where `x ∈ S(U, W)` but `x ∉ S(T,
+///   V)`, which would violate the guarantee that `src`'s referent may only
+///   contain values in `S(T, V)`.
+/// - If the referent may be mutated without going through `dst` while `dst` is
+///   live (e.g. via interior mutation on a `Shared`-aliased `Ptr` or `&`
+///   reference), then it must hold that `S(T, V) ⊆ S(U, W)` - in other words,
+///   the transmute must not shrink the set of allowed referent bit patterns. A
+///   violation of this requirement would permit using `src` or another
+///   mechanism (e.g. a `&` reference used to derive `src`) to write `x` where
+///   `x ∈ S(T, V)` but `x ∉ S(U, W)`, which would violate the guarantee that
+///   `dst`'s referent may only contain values in `S(U, W)`.
 pub trait Validity: Sealed {}
 
 /// An [`Aliasing`] invariant which is either [`Shared`] or [`Exclusive`].