Add Value type with invariant support to resolve invariant inconsistencies and support generic transmutations

[joshlf]

This design obsoletes or incorporates the following pre-existing issues:

• Obsoletes Extend Ptr to store unboxed values #1875
• Obsoletes Overhaul Ptr's validity invariant modeling #1866
• Incorporates Generic transmutability #1359 with the exception that invariant types will now live on the new Value type instead of on Ptr

Co-authored with @jswrenn

Overview

• Add a new Value type which tracks a value's alignment and validity
• Remove the alignment and validity invariants from Ptr
• Replace Ptr<T> with Ptr<Value<T>> as appropriate
• Support generic transmutation as described in Generic transmutability #1359

Background

Recent issues such as #1866, #1889, and #2226 have demonstrated that our existing conception of invariants in Ptr is flawed. In particular, we have historically conceived of invariants as being monotonically increasing in strictness (e.g., Valid is a subset of AsInitialized). We've recently realized that this is incomplete: sometimes invariants also impose a upper- as well as a lower-bound on behavior. See #1866 for a detailed discussion of how this can lead to unsoundness.

Mental model

We've come to the following mental model that provides a unified explanation for all of these issues.

A naive understanding of Ptr invariants suggests that they simply encode knowledge. For example, a ptr: Ptr<T, Valid> encodes the knowledge that ptr's referent is a bit-valid T. However, reborrowing complicates this story.

Consider, as outlined in #1866, t: Ptr<T>. Naively, I should be able to convert this to mu: Ptr<MaybeUninit<T>, Valid> regardless of t's validity invariant; after all, all byte sequences are valid instances of MaybeUninit<T>. However, if we rephrase this in terms of references, that's clearly invalid! Going from &mut T to &mut MaybeUninit<T> is unsound, as the latter reference can be used to write arbitrary bytes to a memory location which is referenced as a &mut T.

This highlights that we need to not only consider the current type (i.e., the T in Ptr<T>), but also the types of all references/Ptrs from which the current Ptr is reborrowed (its "ancestors", to coin a phrase). If we do this, then we can reconceptualize the invariant as not only providing knowledge about the current value of the Ptr's referent, but also a constraint about what values are permitted to be written to the referent. In particular, all values written to the referent must be valid for all ancestor references/Ptrs.

Note that this only affects validity, but not aliasing or alignment. Aliasing is a compile-time property, and so it cannot change at runtime. Alignment is a property of a particular Ptr (and not of its ancestors) and so it really is just a matter of knowledge, not a constraint (in other words, "forgetting" that a Ptr is aligned can never cause problems).

Thus, we can reconceptualize the validity invariant in the following way:

• A Ptr<T, Validity> has type T and validity Validity
• A pair of type and validity, (T, Validity), defines a set of valid values, V. For example, (bool, Valid) defines the set {0x00, 0x01}, and (bool, AsInitialized) defines the set {0x00, ..., 0x255}. Note that changing the type and changing the validity can both affect V.
• Code is permitted to assume that only values in V will be present in the referent
• Code must promise to only write values in V to the referent
• Code may only change V in a way that doesn't violate the preceding two requirements. As mentioned above, this implicates both invariant changes and type transmutations.

In this conception, a pair of type and validity has more degrees of freedom than we actually need. We can change both the type and the validity, but at the end of the day, all we care about is the set of valid values.* In fact, "set of valid values" is really what a type is. This suggests that we just need a type-level representation of... types? Yes!

* Except that type implicates pointer metadata, but that's orthogonal to the present discussion.

In particular, we need the ability for Ptr<T> to encode the invariants that we currently encode separately (alignment and validity). In theory, we could do this using "memory gadgets" like Unalign, MaybeUninit, and a hypothetical future MaybeValid (TODO: Reference issue number). However, we've found that these can have expressivity issues regarding Sized-ness, and nesting gets especially weird (e.g., how do support transmuting Unalign<T> to Unalign<MaybeUninit<T>>?).

Instead, this issue proposes a generic Value type which is the generalization of Unalign, MaybeUninit, and MaybeValid. We still encode alignment and validity in type-level parameters as we do today, but we move these from Ptr to Value, leaving Ptr with only an aliasing invariant.

Design

• Need type-level representation of alignment so that we can write impl TransmuteFromPtr<Src>: TransmuteFrom<Src> where Src::Alignment: Gt<Dst::Alignment> {}
  • Requires us to drop support for repr(Rust) types

[joshlf]

Folding this back into #1866