Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support arbitrary invariant mappings #1945

Open
joshlf opened this issue Oct 19, 2024 · 0 comments
Open

Support arbitrary invariant mappings #1945

joshlf opened this issue Oct 19, 2024 · 0 comments
Assignees

Comments

@joshlf
Copy link
Member

joshlf commented Oct 19, 2024

This design is in progress in #1969.

In #1896, we added support for "invariant mappings". For a given I (where I = trait Alignment or I = trait Validity), and for all X: I, a mapping maps X to some Y: I.

The idea behind these mappings is that some operations modify the invariants of a Ptr. Historically, we had to be conservative and return a new Ptr with a single, concrete invariant. For example, Ptr::cast_unsized casts to a Ptr of a different type, and so it must conservatively assume that the resulting validity is Unknown. With mappings, we can encode that, regardless of the types involved, an Initialized validity will always map to an Initialized validity (because a Ptr whose referent bytes are all initialized retains this invariant regardless of what type is has).

However, even invariant mapping is more limited than it could be. In full generality, some operations are valid over multiple possible invariant mappings.

Consider, for example, performing a Ptr transmute from T to MaybeUninit<T>. We can observe that any of the following mappings would be valid:

  • Unknown -> Unknown, AsInitialized, Valid
  • Initialized -> Unknown, Initialized, AsInitialized, Valid
  • AsInitialized -> Unknown, AsInitialized, Valid
  • Valid -> Unknown, AsInitialized, Valid

This suggests that we in fact want to encode a family of mappings. In this case, there are 3 * 4 * 3 * 3 = 108 valid mappings in this family!

Of course we don't actually want to encode 108 mappings. Not only would that be patently ridiculous, it would also be too specific. The real information we need is merely that a given pair of invariants constitutes a valid transition. For example, that it's valid to map Valid to AsInitialized.

Likely the most natural way to encode this is as a trait:

// Implemented for pairs of `(Type, Validity)`. This won't actually work because it doesn't
// support `Type: ?Sized`, but something similar would.
unsafe trait FromValidity<T: ?Sized, V: Validity> {}

unsafe impl<T> FromValidity<T, Valid> for (MaybeUninit<T>, AsInitialized) {}
// ...

This would permit us to support an API like:

impl<'a, T, I> Ptr<'a, T, I>
where
    T: 'a + ?Sized,
    I: Invariants,
{
    pub fn transmute<U, A, V>(
        self,
    ) -> Ptr<'a, U, (I::Aliasing, A, V)>
    where
        U: ?Sized + FromAlignment<T, I::Alignment> + FromValidity<T, I::Validity>
    { ... }

This API as written might be unsound! We also need to make sure to handle bidirectional validity if the aliasing invariant permits writing to the returned Ptr. But the basic idea remains the same, so I haven't bothered to work out the details here.

This is maximally powerful, but will also cause inference ambiguities in many cases, requiring the user to manually specify the desired invariants. It may be useful to retain the more conservative existing notion of a mapping in order to provide reasonable defaults.

@joshlf joshlf self-assigned this Nov 18, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant