@@ -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/// 
@@ -96,9 +105,15 @@ impl Aliasing for Any {
96105    // 
97106    // [1] https://doc.rust-lang.org/1.81.0/reference/subtyping.html#variance 
98107    type  Variance < ' a ,  T :  ' a  + ?Sized >  = fn ( & ' a  T )  -> & ' a  T ; 
108+ 
109+     type  MappedTo < M :  AliasingMapping >  = M :: FromAny ; 
110+ } 
111+ impl  Alignment  for  Any  { 
112+     type  MappedTo < M :  AlignmentMapping >  = M :: FromAny ; 
113+ } 
114+ impl  Validity  for  Any  { 
115+     type  MappedTo < M :  ValidityMapping >  = M :: FromAny ; 
99116} 
100- impl  Alignment  for  Any  { } 
101- impl  Validity  for  Any  { } 
102117
103118/// The `Ptr<'a, T>` adheres to the aliasing rules of a `&'a T`. 
104119/// 
@@ -112,6 +127,7 @@ pub enum Shared {}
112127impl  Aliasing  for  Shared  { 
113128    const  IS_EXCLUSIVE :  bool  = false ; 
114129    type  Variance < ' a ,  T :  ' a  + ?Sized >  = & ' a  T ; 
130+     type  MappedTo < M :  AliasingMapping >  = M :: FromShared ; 
115131} 
116132impl  Reference  for  Shared  { } 
117133
@@ -124,51 +140,60 @@ pub enum Exclusive {}
124140impl  Aliasing  for  Exclusive  { 
125141    const  IS_EXCLUSIVE :  bool  = true ; 
126142    type  Variance < ' a ,  T :  ' a  + ?Sized >  = & ' a  mut  T ; 
143+     type  MappedTo < M :  AliasingMapping >  = M :: FromExclusive ; 
127144} 
128145impl  Reference  for  Exclusive  { } 
129146
130- /// The referent is aligned: for `Ptr<T>`, the referent's address is a multiple  
131- /// of the `T`'s alignment. 
147+ /// The referent is aligned: for `Ptr<T>`, the referent's address is a 
148+ /// multiple  of the `T`'s alignment. 
132149pub  enum  Aligned  { } 
133- impl  Alignment  for  Aligned  { } 
150+ impl  Alignment  for  Aligned  { 
151+     type  MappedTo < M :  AlignmentMapping >  = M :: FromAligned ; 
152+ } 
134153
135154/// The byte ranges initialized in `T` are also initialized in the referent. 
136155/// 
137156/// Formally: uninitialized bytes may only be present in `Ptr<T>`'s referent 
138- /// where they are guaranteed to be present in `T`. This is a dynamic 
139- /// property:  if, at a particular byte offset, a valid enum discriminant is 
140- /// set, the  subsequent bytes may only have uninitialized bytes as 
141- /// specificed by the  corresponding enum. 
157+ /// where they are guaranteed to be present in `T`. This is a dynamic property:  
158+ /// if, at a particular byte offset, a valid enum discriminant is set, the  
159+ /// subsequent bytes may only have uninitialized bytes as specificed by the  
160+ /// corresponding enum. 
142161/// 
143- /// Formally, given `len = size_of_val_raw(ptr)`, at every byte offset, `b`, 
144- /// in  the range `[0, len)`: 
145- /// - If, in any instance `t: T` of length `len`, the byte at offset `b` in 
146- ///   `t`  is initialized, then the byte at offset `b` within `*ptr` must be 
162+ /// Formally, given `len = size_of_val_raw(ptr)`, at every byte offset, `b`, in  
163+ /// the range `[0, len)`: 
164+ /// - If, in any instance `t: T` of length `len`, the byte at offset `b` in `t`  
165+ ///   is initialized, then the byte at offset `b` within `*ptr` must be 
147166///   initialized. 
148- /// - Let `c` be the contents of the byte range `[0, b)` in `*ptr`. Let `S` 
149- ///   be  the subset of valid instances of `T` of length `len` which contain 
150- ///   `c` in  the offset range `[0, b)`. If, in any instance of `t: T` in 
151- ///   `S`, the byte  at offset `b` in `t` is initialized, then the byte at 
152- ///   offset `b` in `*ptr`  must be initialized. 
167+ /// - Let `c` be the contents of the byte range `[0, b)` in `*ptr`. Let `S` be  
168+ ///   the subset of valid instances of `T` of length `len` which contain `c` in  
169+ ///   the offset range `[0, b)`. If, in any instance of `t: T` in `S`, the byte  
170+ ///   at offset `b` in `t` is initialized, then the byte at offset `b` in `*ptr`  
171+ ///   must be initialized. 
153172/// 
154- ///   Pragmatically, this means that if `*ptr` is guaranteed to contain an 
155- ///   enum  type at a particular offset, and the enum discriminant stored in 
156- ///   `*ptr`  corresponds to a valid variant of that enum type, then it is 
157- ///   guaranteed  that the appropriate bytes of `*ptr` are initialized as 
158- ///   defined by that  variant's bit validity (although note that the variant 
159- ///   may contain another  enum type, in which case the same rules apply 
160- ///   depending on the state of  its discriminant, and so on recursively). 
173+ ///   Pragmatically, this means that if `*ptr` is guaranteed to contain an enum  
174+ ///   type at a particular offset, and the enum discriminant stored in `*ptr`  
175+ ///   corresponds to a valid variant of that enum type, then it is guaranteed  
176+ ///   that the appropriate bytes of `*ptr` are initialized as defined by that  
177+ ///   variant's bit validity (although note that the variant may contain another  
178+ ///   enum type, in which case the same rules apply depending on the state of  
179+ ///   its discriminant, and so on recursively). 
161180pub  enum  AsInitialized  { } 
162- impl  Validity  for  AsInitialized  { } 
181+ impl  Validity  for  AsInitialized  { 
182+     type  MappedTo < M :  ValidityMapping >  = M :: FromAsInitialized ; 
183+ } 
163184
164185/// The byte ranges in the referent are fully initialized. In other words, if 
165186/// the referent is `N` bytes long, then it contains a bit-valid `[u8; N]`. 
166187pub  enum  Initialized  { } 
167- impl  Validity  for  Initialized  { } 
188+ impl  Validity  for  Initialized  { 
189+     type  MappedTo < M :  ValidityMapping >  = M :: FromInitialized ; 
190+ } 
168191
169192/// The referent is bit-valid for `T`. 
170193pub  enum  Valid  { } 
171- impl  Validity  for  Valid  { } 
194+ impl  Validity  for  Valid  { 
195+     type  MappedTo < M :  ValidityMapping >  = M :: FromValid ; 
196+ } 
172197
173198pub  mod  aliasing_safety { 
174199    use  super :: * ; 
@@ -266,3 +291,76 @@ mod sealed {
266291    impl  Sealed  for  super :: aliasing_safety:: BecauseImmutable  { } 
267292    impl < S :  Sealed >  Sealed  for  ( S , )  { } 
268293} 
294+ 
295+ pub  use  mapping:: * ; 
296+ mod  mapping { 
297+     use  super :: * ; 
298+ 
299+     pub  trait  AliasingMapping  { 
300+         type  FromAny :  Aliasing ; 
301+         type  FromShared :  Aliasing ; 
302+         type  FromExclusive :  Aliasing ; 
303+     } 
304+ 
305+     pub  trait  AlignmentMapping  { 
306+         type  FromAny :  Alignment ; 
307+         type  FromAligned :  Alignment ; 
308+     } 
309+ 
310+     pub  trait  ValidityMapping  { 
311+         type  FromAny :  Validity ; 
312+         type  FromAsInitialized :  Validity ; 
313+         type  FromInitialized :  Validity ; 
314+         type  FromValid :  Validity ; 
315+     } 
316+ 
317+     #[ allow( type_alias_bounds) ]  
318+     pub  type  MappedAliasing < I :  Aliasing ,  M :  AliasingMapping >  = I :: MappedTo < M > ; 
319+ 
320+     #[ allow( type_alias_bounds) ]  
321+     pub  type  MappedAlignment < I :  Alignment ,  M :  AlignmentMapping >  = I :: MappedTo < M > ; 
322+ 
323+     #[ allow( type_alias_bounds) ]  
324+     pub  type  MappedValidity < I :  Validity ,  M :  ValidityMapping >  = I :: MappedTo < M > ; 
325+ 
326+     impl < FromAny :  Aliasing ,  FromShared :  Aliasing ,  FromExclusive :  Aliasing >  AliasingMapping 
327+         for  ( ( Any ,  FromAny ) ,  ( Shared ,  FromShared ) ,  ( Exclusive ,  FromExclusive ) ) 
328+     { 
329+         type  FromAny  = FromAny ; 
330+         type  FromShared  = FromShared ; 
331+         type  FromExclusive  = FromExclusive ; 
332+     } 
333+ 
334+     impl < FromAny :  Alignment ,  FromAligned :  Alignment >  AlignmentMapping 
335+         for  ( ( Any ,  FromAny ) ,  ( Shared ,  FromAligned ) ) 
336+     { 
337+         type  FromAny  = FromAny ; 
338+         type  FromAligned  = FromAligned ; 
339+     } 
340+ 
341+     impl < 
342+             FromAny :  Validity , 
343+             FromAsInitialized :  Validity , 
344+             FromInitialized :  Validity , 
345+             FromValid :  Validity , 
346+         >  ValidityMapping 
347+         for  ( 
348+             ( Any ,  FromAny ) , 
349+             ( AsInitialized ,  FromAsInitialized ) , 
350+             ( Initialized ,  FromInitialized ) , 
351+             ( Valid ,  FromValid ) , 
352+         ) 
353+     { 
354+         type  FromAny  = FromAny ; 
355+         type  FromAsInitialized  = FromAsInitialized ; 
356+         type  FromInitialized  = FromInitialized ; 
357+         type  FromValid  = FromValid ; 
358+     } 
359+ 
360+     impl < FromInitialized :  Validity >  ValidityMapping  for  ( Initialized ,  FromInitialized )  { 
361+         type  FromAny  = Any ; 
362+         type  FromAsInitialized  = Any ; 
363+         type  FromInitialized  = FromInitialized ; 
364+         type  FromValid  = Any ; 
365+     } 
366+ } 
0 commit comments