Invariant-parameterize Ptr

[jswrenn]

In #406, we introduced the Ptr type to describe pointers that lie somewhere between the invariants of NonNull<T> and &T. This type has both reduced the labor required to track invariants in our documentation, and revealed further opportunities for improvement. Namely: do actually do many things with a Ptr, you must do so through unsafe methods that have further unencapsulated requirements.

I propose that we extend Ptr to handle these conditional invariants, by encoding them as const generic parameters; e.g.:

/// A raw pointer with more restrictions.
///
/// `Ptr<T>` is similar to `NonNull<T>`, but it is more restrictive in the
/// following ways:
/// - It must derive from a valid allocation
/// - It must reference a byte range which is contained inside the
///   allocation from which it derives
///   - As a consequence, the byte range it references must have a size
///     which does not overflow `isize`
/// - `ptr` conforms to the aliasing invariant of `ASSUME_ALIASING`
/// - If `ASSUME_ALIGNMENT`, it must satisfy `T`'s alignment requirement
/// - If `ASSUME_VALIDITY`, it must satisfy `T`'s bit validity requirement
///
/// Thanks to these restrictions, it is easier to prove the soundness of
/// some operations using `Ptr`s.
///
/// `Ptr<'a, T>` is [covariant] in `'a` and `T`.
///
/// [covariant]: https://doc.rust-lang.org/reference/subtyping.html
pub struct Ptr<
    'a,
    T,
    const ASSUME_ALIASING: invariant::Aliasing,
    const ASSUME_ALIGNMENT: bool,
    const ASSUME_VALIDITY: bool,
> where
    T: 'a + ?Sized,
{
    /// INVARIANTS:
    /// 0. `ptr` is derived from some valid Rust allocation, `A`
    /// 1. `ptr` has the same provenance as `A`
    /// 2. `ptr` addresses a byte range which is entirely contained in `A`
    /// 3. `ptr` addresses a byte range whose length fits in an `isize`
    /// 4. `ptr` addresses a byte range which does not wrap around the address
    ///     space
    /// 5. `A` is guaranteed to live for at least `'a`
    /// 6. `T: 'a`
    /// 7. `ptr` conforms to the aliasing invariant of `ASSUME_ALIASING`
    /// 8. If `ASSUME_ALIGNMENT`, `ptr` is validly-aligned for `T`
    /// 9. If `ASSUME_VALIDITY`, `ptr` is validly-initialized for `T`
    ptr: NonNull<T>,
    _lifetime: PhantomData<&'a ()>,
}

// TODO: Replace this module with enums, once it becomes possible to do so.
// Use a unique integer for each invariant kind.
pub mod invariant {
    pub type Aliasing = u8;

    /// No invariants.
    pub const None: Aliasing = 0;
    
    /// The pointer adheres to the aliasing rules of a `&T`.
    pub const Shared: Aliasing = 1;
    
    /// The pointer adheres to the aliasing rules of a `&mut T`. 
    pub const Unique: Aliasing = 2;
}

We would then provide methods for asserting invariants; e.g.:

/// Assumes that `Ptr` adheres to the aliasing requirements of a `&T` reference.
///
/// # Safety
///
/// The caller promises that `Ptr` adheres to the aliasing requirements of a
/// `&T` reference.
impl<
        'a,
        T,
        const ASSUME_ALIASING: invariant::Aliasing,
        const ASSUME_ALIGNMENT: bool,
        const ASSUME_VALIDITY: bool,
    > Ptr<'a, T, ASSUME_ALIASING, ASSUME_ALIGNMENT, ASSUME_VALIDITY>
where
    T: 'a + ?Sized,
{
    pub unsafe fn assume_unique(
        self,
    ) -> Ptr<'a, T, {invariant::Unique}, ASSUME_ALIGNMENT, ASSUME_VALIDITY> {
        // SAFETY: The caller has promised that `Ptr` adheres to the aliasing
        // requirements of a `&T` reference.
        unsafe { Ptr::new(self.ptr) }
    }
}

...forgetting invariants; e.g.:

impl<
        'a,
        T,
        const ASSUME_ALIASING: invariant::Aliasing,
        const ASSUME_ALIGNMENT: bool,
        const ASSUME_VALIDITY: bool,
    > Ptr<'a, T, ASSUME_ALIASING, ASSUME_ALIGNMENT, ASSUME_VALIDITY>
where
    T: 'a + ?Sized,
{
    /// Forgets that `Ptr` has a validity invariant.
    pub fn forget_valid(self) -> Ptr<'a, T, ASSUME_ALIASING, ASSUME_ALIGNMENT, false> {
        // SAFETY: The invariants of `Ptr` when `ASSUME_VALIDITY = false` are a
        // strict subset of the obligations when `ASSUME_VALIDITY = true`.
        unsafe { Ptr::new(self.ptr) }
    }
}

...and safe methods conditioned on those invariants:

impl<'a, T> Ptr<'a, T, { invariant::Shared }, true, true>
where
    T: 'a + ?Sized,
{
    pub fn as_ref(self) -> &'a T {
        // SAFETY:
        // By invariant on `Ptr`:
        // 0. `ptr` is derived from some valid Rust allocation, `A`
        // 1. `ptr` has the same provenance as `A`
        // 2. `ptr` addresses a byte range which is entirely contained in `A`
        // 3. `ptr` addresses a byte range whose length fits in an `isize`
        // 4. `ptr` addresses a byte range which does not wrap around the address
        //     space
        // 5. `A` is guaranteed to live for at least `'a`
        // 6. `T: 'a`
        // 7. `ptr` conforms to the aliasing invariant of a shared reference,
        //    because `ASSUME_ALIASING = invariant::Shared`
        // 8. `ptr` is validly-aligned for `T` because `ASSUME_ALIGNMENT = true`
        // 9. `ptr` is validly-initialized for `T` because `ASSUME_VALIDITY = true`
        unsafe { self.ptr.as_ref() }
    }
}

Why should we do this?

Doing this will help us maintain and document the safety invariants on Ptr and its methods. The above proposal has enough fidelity that we will be able to remove caller-enforced safety conditions on TryFromBytes::is_bit_valid to type invariants on a Ptr<'_, Self, ASSUME_ALIASING = {invariants::Shared}, ASSUME_ALIGNMENT = false, ASSUME_VALIDITY = false> and make is_bit_valid safe.

Unresolved Questions

How should we name things? Does ASSUME_VALIDITY have enough fidelity? How should we express maybe-invalid-but-has-unsafecells-in-the-right-places?

Prototype

https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=f4e7f9df5377bda62ab7e17c0287128a

[joshlf]

Review comments for this prototype:

Invariant comments

        /// 7. `ptr` conforms to the aliasing invariant of `ALIASING_INVARIANT`
        /// 8. `ptr` conforms to the alignment invariant of `ALIGNMENT_INVARIANT`
        /// 9. `ptr` conforms to the validity invariant of `VALIDITY_INVARIANT`

Can we describe the invariants locally so it's easier to see what needs to be upheld? Something like:

        /// 7. `ptr` conforms to the aliasing invariant of `ALIASING_INVARIANT`; in particular:
        ///     - If `ALIASING_INVARIANT` is `Shared`, ...
        ///     - If `ALIASING_INVARIANT` is `Unique`, ...

Invariant descriptions

Aliasing

    /// The pointer adheres to the aliasing rules of a `&T`.
    pub(crate) const Shared: Aliasing = 1 << 2;

    /// The pointer adheres to the aliasing rules of a `&mut T`.
    pub(crate) const Unique: Aliasing = 1 << 3;

Can we actually specify what these are? (And also wherever the description of the rules is inlined, as in the previous comment.)

Alignment

    /// The referent is aligned.
    pub(crate) const Aligned: Alignment = 1 << 5;

Same comment; maybe:

    /// The address of this `Ptr<T>` satisfies `T`'s alignment requirement.
    pub(crate) const Aligned: Alignment = 1 << 5;

Validity

    /// Totally bit-valid.
    pub(crate) const Valid: Validity = 1 << 8;

Same comment; maybe:

    /// The referent of this `Ptr<T>` is initialized to a bit pattern which is a
    /// valid instance of `T`.
    pub(crate) const Valid: Validity = 1 << 8;

UnsafeCell location

    /// Has unsafe cells in the same places.
    pub(crate) const UnsafeCells: Validity = 1 << 7;

Same comment; maybe:

    /// All references to this memory treat the memory as having `UnsafeCell`s
    /// at the same byte ranges.
    pub(crate) const UnsafeCells: Validity = 1 << 7;

UnsafeCells

Two comments:

• The presence/absence/location of UnsafeCells isn't a bit validity property, but rather a property of the type used to reference a region of memory, so const UnsafeCells shouldn't have the type Validity.
• Right now, we always require UnsafeCells in all of our uses of Ptr, so we should be able to not encode it using a separate invariant type and just treat it as true in all of our impl blocks.

Capitalization

We're currently using the constants in the invariants module as if they were enums, and naming them using enum style (namely, camel case), which is different from the recommended style for constant names. Can we add a comment somewhere explaining why we do this?

[joshlf]

More review comments for this prototype:

Provenance

In various places, we have the following language:

ptr has the same provenance as A

Based on this discussion, I think a more accurate phrasing would be:

ptr has valid provenance for A