@@ -65,13 +65,22 @@ pub trait Aliasing: Sealed {
6565 /// Aliasing>::Variance<'a, T>` to inherit this variance.
6666 #[ doc( hidden) ]
6767 type Variance < ' a , T : ' a + ?Sized > ;
68+
69+ #[ doc( hidden) ]
70+ type MappedTo < M : AliasingMapping > : Aliasing ;
6871}
6972
7073/// The alignment invariant of a [`Ptr`][super::Ptr].
71- pub trait Alignment : Sealed { }
74+ pub trait Alignment : Sealed {
75+ #[ doc( hidden) ]
76+ type MappedTo < M : AlignmentMapping > : Alignment ;
77+ }
7278
7379/// The validity invariant of a [`Ptr`][super::Ptr].
74- pub trait Validity : Sealed { }
80+ pub trait Validity : Sealed {
81+ #[ doc( hidden) ]
82+ type MappedTo < M : ValidityMapping > : Validity ;
83+ }
7584
7685/// An [`Aliasing`] invariant which is either [`Shared`] or [`Exclusive`].
7786///
@@ -84,8 +93,12 @@ pub trait Reference: Aliasing + Sealed {}
8493/// It is unknown whether any invariant holds.
8594pub enum Unknown { }
8695
87- impl Alignment for Unknown { }
88- impl Validity for Unknown { }
96+ impl Alignment for Unknown {
97+ type MappedTo < M : AlignmentMapping > = M :: FromUnknown ;
98+ }
99+ impl Validity for Unknown {
100+ type MappedTo < M : ValidityMapping > = M :: FromUnknown ;
101+ }
89102
90103/// The `Ptr<'a, T>` does not permit any reads or writes from or to its referent.
91104pub enum Inaccessible { }
@@ -100,6 +113,7 @@ impl Aliasing for Inaccessible {
100113 //
101114 // [1] https://doc.rust-lang.org/1.81.0/reference/subtyping.html#variance
102115 type Variance < ' a , T : ' a + ?Sized > = & ' a T ;
116+ type MappedTo < M : AliasingMapping > = M :: FromInaccessible ;
103117}
104118
105119/// The `Ptr<'a, T>` adheres to the aliasing rules of a `&'a T`.
@@ -114,6 +128,7 @@ pub enum Shared {}
114128impl Aliasing for Shared {
115129 const IS_EXCLUSIVE : bool = false ;
116130 type Variance < ' a , T : ' a + ?Sized > = & ' a T ;
131+ type MappedTo < M : AliasingMapping > = M :: FromShared ;
117132}
118133impl Reference for Shared { }
119134
@@ -126,51 +141,60 @@ pub enum Exclusive {}
126141impl Aliasing for Exclusive {
127142 const IS_EXCLUSIVE : bool = true ;
128143 type Variance < ' a , T : ' a + ?Sized > = & ' a mut T ;
144+ type MappedTo < M : AliasingMapping > = M :: FromExclusive ;
129145}
130146impl Reference for Exclusive { }
131147
132- /// The referent is aligned: for `Ptr<T>`, the referent's address is a multiple
133- /// of the `T`'s alignment.
148+ /// The referent is aligned: for `Ptr<T>`, the referent's address is a
149+ /// multiple of the `T`'s alignment.
134150pub enum Aligned { }
135- impl Alignment for Aligned { }
151+ impl Alignment for Aligned {
152+ type MappedTo < M : AlignmentMapping > = M :: FromAligned ;
153+ }
136154
137155/// The byte ranges initialized in `T` are also initialized in the referent.
138156///
139157/// Formally: uninitialized bytes may only be present in `Ptr<T>`'s referent
140- /// where they are guaranteed to be present in `T`. This is a dynamic
141- /// property: if, at a particular byte offset, a valid enum discriminant is
142- /// set, the subsequent bytes may only have uninitialized bytes as
143- /// specificed by the corresponding enum.
158+ /// where they are guaranteed to be present in `T`. This is a dynamic property:
159+ /// if, at a particular byte offset, a valid enum discriminant is set, the
160+ /// subsequent bytes may only have uninitialized bytes as specificed by the
161+ /// corresponding enum.
144162///
145- /// Formally, given `len = size_of_val_raw(ptr)`, at every byte offset, `b`,
146- /// in the range `[0, len)`:
147- /// - If, in any instance `t: T` of length `len`, the byte at offset `b` in
148- /// `t` is initialized, then the byte at offset `b` within `*ptr` must be
163+ /// Formally, given `len = size_of_val_raw(ptr)`, at every byte offset, `b`, in
164+ /// the range `[0, len)`:
165+ /// - If, in any instance `t: T` of length `len`, the byte at offset `b` in `t`
166+ /// is initialized, then the byte at offset `b` within `*ptr` must be
149167/// initialized.
150- /// - Let `c` be the contents of the byte range `[0, b)` in `*ptr`. Let `S`
151- /// be the subset of valid instances of `T` of length `len` which contain
152- /// `c` in the offset range `[0, b)`. If, in any instance of `t: T` in
153- /// `S`, the byte at offset `b` in `t` is initialized, then the byte at
154- /// offset `b` in `*ptr` must be initialized.
168+ /// - Let `c` be the contents of the byte range `[0, b)` in `*ptr`. Let `S` be
169+ /// the subset of valid instances of `T` of length `len` which contain `c` in
170+ /// the offset range `[0, b)`. If, in any instance of `t: T` in `S`, the byte
171+ /// at offset `b` in `t` is initialized, then the byte at offset `b` in `*ptr`
172+ /// must be initialized.
155173///
156- /// Pragmatically, this means that if `*ptr` is guaranteed to contain an
157- /// enum type at a particular offset, and the enum discriminant stored in
158- /// `*ptr` corresponds to a valid variant of that enum type, then it is
159- /// guaranteed that the appropriate bytes of `*ptr` are initialized as
160- /// defined by that variant's bit validity (although note that the variant
161- /// may contain another enum type, in which case the same rules apply
162- /// depending on the state of its discriminant, and so on recursively).
174+ /// Pragmatically, this means that if `*ptr` is guaranteed to contain an enum
175+ /// type at a particular offset, and the enum discriminant stored in `*ptr`
176+ /// corresponds to a valid variant of that enum type, then it is guaranteed
177+ /// that the appropriate bytes of `*ptr` are initialized as defined by that
178+ /// variant's bit validity (although note that the variant may contain another
179+ /// enum type, in which case the same rules apply depending on the state of
180+ /// its discriminant, and so on recursively).
163181pub enum AsInitialized { }
164- impl Validity for AsInitialized { }
182+ impl Validity for AsInitialized {
183+ type MappedTo < M : ValidityMapping > = M :: FromAsInitialized ;
184+ }
165185
166186/// The byte ranges in the referent are fully initialized. In other words, if
167187/// the referent is `N` bytes long, then it contains a bit-valid `[u8; N]`.
168188pub enum Initialized { }
169- impl Validity for Initialized { }
189+ impl Validity for Initialized {
190+ type MappedTo < M : ValidityMapping > = M :: FromInitialized ;
191+ }
170192
171193/// The referent is bit-valid for `T`.
172194pub enum Valid { }
173- impl Validity for Valid { }
195+ impl Validity for Valid {
196+ type MappedTo < M : ValidityMapping > = M :: FromValid ;
197+ }
174198
175199/// [`Ptr`](crate::Ptr) referents that permit unsynchronized read operations.
176200///
@@ -231,3 +255,112 @@ mod sealed {
231255 impl Sealed for BecauseImmutable { }
232256 impl Sealed for BecauseExclusive { }
233257}
258+
259+ pub use mapping:: * ;
260+ mod mapping {
261+ use super :: * ;
262+
263+ /// A mapping from one [`Aliasing`] type to another.
264+ ///
265+ /// An `AliasingMapping` is a type-level map which maps one `Aliasing` type
266+ /// to another. It is always "total" in the sense of having a mapping for
267+ /// any `A: Aliasing`.
268+ ///
269+ /// Given `A: Aliasing` and `M: AliasingMapping`, `M` can be applied to `A`
270+ /// as [`MappedAliasing<A, M>`](MappedAliasing).
271+ ///
272+ /// Mappings are used by [`Ptr`](crate::Ptr) conversion methods to preserve
273+ /// or modify invariants as required by each method's semantics.
274+ pub trait AliasingMapping {
275+ type FromInaccessible : Aliasing ;
276+ type FromShared : Aliasing ;
277+ type FromExclusive : Aliasing ;
278+ }
279+
280+ /// A mapping from one [`Alignment`] type to another.
281+ ///
282+ /// An `AlignmentMapping` is a type-level map which maps one `Alignment`
283+ /// type to another. It is always "total" in the sense of having a mapping
284+ /// for any `A: Alignment`.
285+ ///
286+ /// Given `A: Alignment` and `M: AlignmentMapping`, `M` can be applied to
287+ /// `A` as [`MappedAlignment<A, M>`](MappedAlignment).
288+ ///
289+ /// Mappings are used by [`Ptr`](crate::Ptr) conversion methods to preserve
290+ /// or modify invariants as required by each method's semantics.
291+ pub trait AlignmentMapping {
292+ type FromUnknown : Alignment ;
293+ type FromAligned : Alignment ;
294+ }
295+
296+ /// A mapping from one [`Validity`] type to another.
297+ ///
298+ /// An `ValidityMapping` is a type-level map which maps one `Validity` type
299+ /// to another. It is always "total" in the sense of having a mapping for
300+ /// any `A: Validity`.
301+ ///
302+ /// Given `V: Validity` and `M: ValidityMapping`, `M` can be applied to `V`
303+ /// as [`MappedValidity<A, M>`](MappedValidity).
304+ ///
305+ /// Mappings are used by [`Ptr`](crate::Ptr) conversion methods to preserve
306+ /// or modify invariants as required by each method's semantics.
307+ pub trait ValidityMapping {
308+ type FromUnknown : Validity ;
309+ type FromAsInitialized : Validity ;
310+ type FromInitialized : Validity ;
311+ type FromValid : Validity ;
312+ }
313+
314+ /// The application of the [`AliasingMapping`] `M` to the [`Aliasing`] `A`.
315+ #[ allow( type_alias_bounds) ]
316+ pub type MappedAliasing < A : Aliasing , M : AliasingMapping > = A :: MappedTo < M > ;
317+
318+ /// The application of the [`AlignmentMapping`] `M` to the [`Alignment`] `A`.
319+ #[ allow( type_alias_bounds) ]
320+ pub type MappedAlignment < A : Alignment , M : AlignmentMapping > = A :: MappedTo < M > ;
321+
322+ /// The application of the [`ValidityMapping`] `M` to the [`Validity`] `A`.
323+ #[ allow( type_alias_bounds) ]
324+ pub type MappedValidity < V : Validity , M : ValidityMapping > = V :: MappedTo < M > ;
325+
326+ impl < FromInaccessible : Aliasing , FromShared : Aliasing , FromExclusive : Aliasing > AliasingMapping
327+ for ( ( Inaccessible , FromInaccessible ) , ( Shared , FromShared ) , ( Exclusive , FromExclusive ) )
328+ {
329+ type FromInaccessible = FromInaccessible ;
330+ type FromShared = FromShared ;
331+ type FromExclusive = FromExclusive ;
332+ }
333+
334+ impl < FromUnknown : Alignment , FromAligned : Alignment > AlignmentMapping
335+ for ( ( Unknown , FromUnknown ) , ( Shared , FromAligned ) )
336+ {
337+ type FromUnknown = FromUnknown ;
338+ type FromAligned = FromAligned ;
339+ }
340+
341+ impl <
342+ FromUnknown : Validity ,
343+ FromAsInitialized : Validity ,
344+ FromInitialized : Validity ,
345+ FromValid : Validity ,
346+ > ValidityMapping
347+ for (
348+ ( Unknown , FromUnknown ) ,
349+ ( AsInitialized , FromAsInitialized ) ,
350+ ( Initialized , FromInitialized ) ,
351+ ( Valid , FromValid ) ,
352+ )
353+ {
354+ type FromUnknown = FromUnknown ;
355+ type FromAsInitialized = FromAsInitialized ;
356+ type FromInitialized = FromInitialized ;
357+ type FromValid = FromValid ;
358+ }
359+
360+ impl < FromInitialized : Validity > ValidityMapping for ( Initialized , FromInitialized ) {
361+ type FromUnknown = Unknown ;
362+ type FromAsInitialized = Unknown ;
363+ type FromInitialized = FromInitialized ;
364+ type FromValid = Unknown ;
365+ }
366+ }
0 commit comments