@@ -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,76 @@ 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+     pub  trait  AliasingMapping  { 
264+         type  FromInaccessible :  Aliasing ; 
265+         type  FromShared :  Aliasing ; 
266+         type  FromExclusive :  Aliasing ; 
267+     } 
268+ 
269+     pub  trait  AlignmentMapping  { 
270+         type  FromUnknown :  Alignment ; 
271+         type  FromAligned :  Alignment ; 
272+     } 
273+ 
274+     pub  trait  ValidityMapping  { 
275+         type  FromUnknown :  Validity ; 
276+         type  FromAsInitialized :  Validity ; 
277+         type  FromInitialized :  Validity ; 
278+         type  FromValid :  Validity ; 
279+     } 
280+ 
281+     #[ allow( type_alias_bounds) ]  
282+     pub  type  MappedAliasing < I :  Aliasing ,  M :  AliasingMapping >  = I :: MappedTo < M > ; 
283+ 
284+     #[ allow( type_alias_bounds) ]  
285+     pub  type  MappedAlignment < I :  Alignment ,  M :  AlignmentMapping >  = I :: MappedTo < M > ; 
286+ 
287+     #[ allow( type_alias_bounds) ]  
288+     pub  type  MappedValidity < I :  Validity ,  M :  ValidityMapping >  = I :: MappedTo < M > ; 
289+ 
290+     impl < FromInaccessible :  Aliasing ,  FromShared :  Aliasing ,  FromExclusive :  Aliasing >  AliasingMapping 
291+         for  ( ( Inaccessible ,  FromInaccessible ) ,  ( Shared ,  FromShared ) ,  ( Exclusive ,  FromExclusive ) ) 
292+     { 
293+         type  FromInaccessible  = FromInaccessible ; 
294+         type  FromShared  = FromShared ; 
295+         type  FromExclusive  = FromExclusive ; 
296+     } 
297+ 
298+     impl < FromUnknown :  Alignment ,  FromAligned :  Alignment >  AlignmentMapping 
299+         for  ( ( Unknown ,  FromUnknown ) ,  ( Shared ,  FromAligned ) ) 
300+     { 
301+         type  FromUnknown  = FromUnknown ; 
302+         type  FromAligned  = FromAligned ; 
303+     } 
304+ 
305+     impl < 
306+             FromUnknown :  Validity , 
307+             FromAsInitialized :  Validity , 
308+             FromInitialized :  Validity , 
309+             FromValid :  Validity , 
310+         >  ValidityMapping 
311+         for  ( 
312+             ( Unknown ,  FromUnknown ) , 
313+             ( AsInitialized ,  FromAsInitialized ) , 
314+             ( Initialized ,  FromInitialized ) , 
315+             ( Valid ,  FromValid ) , 
316+         ) 
317+     { 
318+         type  FromUnknown  = FromUnknown ; 
319+         type  FromAsInitialized  = FromAsInitialized ; 
320+         type  FromInitialized  = FromInitialized ; 
321+         type  FromValid  = FromValid ; 
322+     } 
323+ 
324+     impl < FromInitialized :  Validity >  ValidityMapping  for  ( Initialized ,  FromInitialized )  { 
325+         type  FromUnknown  = Unknown ; 
326+         type  FromAsInitialized  = Unknown ; 
327+         type  FromInitialized  = FromInitialized ; 
328+         type  FromValid  = Unknown ; 
329+     } 
330+ } 
0 commit comments