@@ -57,7 +57,7 @@ impl<A: Aliasing, AA: Alignment, V: Validity> Invariants for (A, AA, V) {
5757/// The aliasing invariant of a [`Ptr`][super::Ptr].
5858///
5959/// All aliasing invariants must permit reading from the bytes of a pointer's
60- /// referent which are not covered by [`UnsafeCell`]s.
60+ /// referent which are not covered by [`UnsafeCell`](core::cell::UnsafeCell) s.
6161pub trait Aliasing : Sealed {
6262 /// Is `Self` [`Exclusive`]?
6363 #[ doc( hidden) ]
@@ -70,18 +70,56 @@ pub trait Aliasing: Sealed {
7070 type Variance < ' a , T : ' a + ?Sized > ;
7171}
7272
73- /// The alignment invariant of a [`Ptr`][super::Ptr].
74- pub trait Alignment : Sealed {
75- #[ doc( hidden) ]
73+ // NOTE: The `AlignmentInner`/`Alignment` distinction is required so that we can
74+ // add a `MappedTo<Preserved> = Self` bound. For an explanation of the design
75+ // space (and prior attempts), see:
76+ // https://users.rust-lang.org/t/how-to-implement-a-type-level-map-with-an-identity-function/119745
77+ #[ doc( hidden) ]
78+ pub trait AlignmentInner : Sealed {
7679 type MappedTo < M : AlignmentMapping > : Alignment ;
7780}
7881
79- /// The validity invariant of a [`Ptr`][super::Ptr].
80- pub trait Validity : Sealed {
81- #[ doc( hidden) ]
82+ /// The alignment invariant of a [`Ptr`][super::Ptr].
83+ pub trait Alignment :
84+ AlignmentInner < MappedTo < Preserved > = Self >
85+ + AlignmentInner < MappedTo < Unknown > = Unknown >
86+ + AlignmentInner < MappedTo < Aligned > = Aligned >
87+ + Sealed
88+ {
89+ }
90+ impl <
91+ A : AlignmentInner < MappedTo < Preserved > = Self >
92+ + AlignmentInner < MappedTo < Unknown > = Unknown >
93+ + AlignmentInner < MappedTo < Aligned > = Aligned > ,
94+ > Alignment for A
95+ {
96+ }
97+
98+ #[ doc( hidden) ]
99+ pub trait ValidityInner : Sealed {
82100 type MappedTo < M : ValidityMapping > : Validity ;
83101}
84102
103+ /// The validity invariant of a [`Ptr`][super::Ptr].
104+ pub trait Validity :
105+ ValidityInner < MappedTo < Preserved > = Self >
106+ + ValidityInner < MappedTo < Unknown > = Unknown >
107+ + ValidityInner < MappedTo < AsInitialized > = AsInitialized >
108+ + ValidityInner < MappedTo < Initialized > = Initialized >
109+ + ValidityInner < MappedTo < Valid > = Valid >
110+ + Sealed
111+ {
112+ }
113+ impl <
114+ V : ValidityInner < MappedTo < Preserved > = Self >
115+ + ValidityInner < MappedTo < Unknown > = Unknown >
116+ + ValidityInner < MappedTo < AsInitialized > = AsInitialized >
117+ + ValidityInner < MappedTo < Initialized > = Initialized >
118+ + ValidityInner < MappedTo < Valid > = Valid > ,
119+ > Validity for V
120+ {
121+ }
122+
85123/// An [`Aliasing`] invariant which is either [`Shared`] or [`Exclusive`].
86124///
87125/// # Safety
@@ -93,10 +131,10 @@ pub trait Reference: Aliasing + Sealed {}
93131/// It is unknown whether any invariant holds.
94132pub enum Unknown { }
95133
96- impl Alignment for Unknown {
134+ impl AlignmentInner for Unknown {
97135 type MappedTo < M : AlignmentMapping > = M :: FromUnknown ;
98136}
99- impl Validity for Unknown {
137+ impl ValidityInner for Unknown {
100138 type MappedTo < M : ValidityMapping > = M :: FromUnknown ;
101139}
102140
@@ -127,10 +165,10 @@ impl Aliasing for Exclusive {
127165}
128166impl Reference for Exclusive { }
129167
130- /// The referent is aligned: for `Ptr<T>`, the referent's address is a
131- /// multiple of the `T`'s alignment.
168+ /// The referent is aligned: for `Ptr<T>`, the referent's address is a multiple
169+ /// of the `T`'s alignment.
132170pub enum Aligned { }
133- impl Alignment for Aligned {
171+ impl AlignmentInner for Aligned {
134172 type MappedTo < M : AlignmentMapping > = M :: FromAligned ;
135173}
136174
@@ -161,20 +199,20 @@ impl Alignment for Aligned {
161199/// enum type, in which case the same rules apply depending on the state of
162200/// its discriminant, and so on recursively).
163201pub enum AsInitialized { }
164- impl Validity for AsInitialized {
202+ impl ValidityInner for AsInitialized {
165203 type MappedTo < M : ValidityMapping > = M :: FromAsInitialized ;
166204}
167205
168- /// The byte ranges in the referent are fully initialized. In other words, if
169- /// the referent is `N` bytes long, then it contains a bit-valid `[u8; N]`.
206+ /// The byte ranges in the referent are fully initialized. In other words,
207+ /// if the referent is `N` bytes long, then it contains a bit-valid `[u8; N]`.
170208pub enum Initialized { }
171- impl Validity for Initialized {
209+ impl ValidityInner for Initialized {
172210 type MappedTo < M : ValidityMapping > = M :: FromInitialized ;
173211}
174212
175213/// The referent is bit-valid for `T`.
176214pub enum Valid { }
177- impl Validity for Valid {
215+ impl ValidityInner for Valid {
178216 type MappedTo < M : ValidityMapping > = M :: FromValid ;
179217}
180218
@@ -272,6 +310,12 @@ mod mapping {
272310 type FromValid : Validity ;
273311 }
274312
313+ /// A mapping which preserves all invariants as-is.
314+ ///
315+ /// `Preserved` is a valid type for any mapping trait ([`AlignmentMapping`]
316+ /// and [`ValidityMapping`]).
317+ pub enum Preserved { }
318+
275319 /// The application of the [`AlignmentMapping`] `M` to the [`Alignment`] `A`.
276320 #[ allow( type_alias_bounds) ]
277321 pub type MappedAlignment < A : Alignment , M : AlignmentMapping > = A :: MappedTo < M > ;
@@ -281,12 +325,27 @@ mod mapping {
281325 pub type MappedValidity < V : Validity , M : ValidityMapping > = V :: MappedTo < M > ;
282326
283327 impl < FromUnknown : Alignment , FromAligned : Alignment > AlignmentMapping
284- for ( ( Unknown , FromUnknown ) , ( Shared , FromAligned ) )
328+ for ( ( Unknown , FromUnknown ) , ( Aligned , FromAligned ) )
285329 {
286330 type FromUnknown = FromUnknown ;
287331 type FromAligned = FromAligned ;
288332 }
289333
334+ impl AlignmentMapping for Unknown {
335+ type FromUnknown = Unknown ;
336+ type FromAligned = Unknown ;
337+ }
338+
339+ impl AlignmentMapping for Preserved {
340+ type FromUnknown = Unknown ;
341+ type FromAligned = Aligned ;
342+ }
343+
344+ impl AlignmentMapping for Aligned {
345+ type FromUnknown = Aligned ;
346+ type FromAligned = Aligned ;
347+ }
348+
290349 impl <
291350 FromUnknown : Validity ,
292351 FromAsInitialized : Validity ,
@@ -312,4 +371,39 @@ mod mapping {
312371 type FromInitialized = FromInitialized ;
313372 type FromValid = Unknown ;
314373 }
374+
375+ impl ValidityMapping for Unknown {
376+ type FromUnknown = Unknown ;
377+ type FromAsInitialized = Unknown ;
378+ type FromInitialized = Unknown ;
379+ type FromValid = Unknown ;
380+ }
381+
382+ impl ValidityMapping for Preserved {
383+ type FromUnknown = Unknown ;
384+ type FromAsInitialized = AsInitialized ;
385+ type FromInitialized = Initialized ;
386+ type FromValid = Valid ;
387+ }
388+
389+ impl ValidityMapping for AsInitialized {
390+ type FromUnknown = AsInitialized ;
391+ type FromAsInitialized = AsInitialized ;
392+ type FromInitialized = AsInitialized ;
393+ type FromValid = AsInitialized ;
394+ }
395+
396+ impl ValidityMapping for Initialized {
397+ type FromUnknown = Initialized ;
398+ type FromAsInitialized = Initialized ;
399+ type FromInitialized = Initialized ;
400+ type FromValid = Initialized ;
401+ }
402+
403+ impl ValidityMapping for Valid {
404+ type FromUnknown = Valid ;
405+ type FromAsInitialized = Valid ;
406+ type FromInitialized = Valid ;
407+ type FromValid = Valid ;
408+ }
315409}
0 commit comments