@@ -35,7 +35,7 @@ use crate::{
3535///
3636/// Given `src: Ptr<'a, Src, (A, _, SV)>`, if the referent of `src` is
3737/// `DV`-valid for `Dst`, then it is sound to transmute `src` into `dst: Ptr<'a,
38- /// Dst, (A, Unaligned, DV)>` using `<Dst as SizeEq<Src>>::CastFrom::project` .
38+ /// Dst, (A, Unaligned, DV)>` using a address- and size-preserving cast .
3939///
4040/// ## Pre-conditions
4141///
@@ -67,17 +67,14 @@ use crate::{
6767/// Given:
6868/// - `src: Ptr<'a, Src, (A, _, SV)>`
6969/// - `src`'s referent is `DV`-valid for `Dst`
70- /// - `Dst: SizeEq<Src>`
7170///
72- /// We are trying to prove that it is sound to cast using `<Dst as
73- /// SizeEq<Src>>::CastFrom::project` from `src` to a `dst: Ptr<'a, Dst, (A,
74- /// Unaligned, DV)>`. We need to prove that such a transmute does not violate
75- /// any of `src`'s invariants, and that it satisfies all invariants of the
76- /// destination `Ptr` type.
71+ /// We are trying to prove that it is sound to perform a size-preserving cast
72+ /// from `src` to a `dst: Ptr<'a, Dst, (A, Unaligned, DV)>`. We need to prove
73+ /// that such a cast does not violate any of `src`'s invariants, and that it
74+ /// satisfies all invariants of the destination `Ptr` type.
7775///
78- /// First, by `SizeEq::CastFrom: CastExact`, `src`'s address is unchanged, so it
79- /// still satisfies its alignment. Since `dst`'s alignment is `Unaligned`, it
80- /// trivially satisfies its alignment.
76+ /// First, `src`'s address is unchanged, so it still satisfies its alignment.
77+ /// Since `dst`'s alignment is `Unaligned`, it trivially satisfies its alignment.
8178///
8279/// Second, aliasing is either `Exclusive` or `Shared`:
8380/// - If it is `Exclusive`, then both `src` and `dst` satisfy `Exclusive`
@@ -106,10 +103,7 @@ use crate::{
106103/// - The set of `DV`-valid referents of `dst` is a superset of the set of
107104/// `SV`-valid referents of `src`. Thus, any value written via `src` is
108105/// guaranteed to be a `DV`-valid referent of `dst`.
109- pub unsafe trait TryTransmuteFromPtr < Src : ?Sized , A : Aliasing , SV : Validity , DV : Validity , R > :
110- SizeEq < Src >
111- {
112- }
106+ pub unsafe trait TryTransmuteFromPtr < Src : ?Sized , A : Aliasing , SV : Validity , DV : Validity , R > { }
113107
114108#[ allow( missing_copy_implementations, missing_debug_implementations) ]
115109pub enum BecauseMutationCompatible { }
@@ -123,14 +117,14 @@ pub enum BecauseMutationCompatible {}
123117// exists, no mutation is permitted except via that `Ptr`
124118// - Aliasing is `Shared`, `Src: Immutable`, and `Dst: Immutable`, in which
125119// case no mutation is possible via either `Ptr`
126- // - Since the underlying cast is performed using `<Dst as SizeEq<Src>>
127- // ::CastFrom::project`, `dst` addresses the same bytes as `src`. By `Dst:
128- // TransmuteFrom<Src, SV, DV>`, the set of ` DV`-valid referents of `dst` is a
129- // supserset of the set of `SV`-valid referents of `src`.
130- // - Reverse transmutation: Since the underlying cast is performed using `<Dst
131- // as SizeEq<Src>>::CastFrom::project`, `dst` addresses the same bytes as
132- // `src`. By `Src: TransmuteFrom<Dst, DV, SV>`, the set of `DV `-valid
133- // referents of `dst` is a subset of the set of `SV`-valid referents of `src` .
120+ // - Since the underlying cast is size-preserving, `dst` addresses the same
121+ // bytes as `src`. By `Dst: TransmuteFrom<Src, SV, DV>`, the set of
122+ // ` DV`-valid referents of `dst` is a superset of the set of `SV`-valid
123+ // referents of `src`.
124+ // - Reverse transmutation: Since the underlying cast is size-preserving, `dst`
125+ // addresses the same bytes as `src`. By `Src: TransmuteFrom<Dst, DV, SV>`, the
126+ // set of `DV`-valid referents of `src` is a subset of the set of `SV `-valid
127+ // referents of `dst`.
134128// - No safe code, given access to `src` and `dst`, can cause undefined
135129// behavior: By `Dst: MutationCompatible<Src, A, SV, DV, _>`, at least one of
136130// the following holds:
@@ -145,7 +139,7 @@ where
145139 SV : Validity ,
146140 DV : Validity ,
147141 Src : TransmuteFrom < Dst , DV , SV > + ?Sized ,
148- Dst : MutationCompatible < Src , A , SV , DV , R > + SizeEq < Src > + ?Sized ,
142+ Dst : MutationCompatible < Src , A , SV , DV , R > + ?Sized ,
149143{
150144}
151145
@@ -161,7 +155,7 @@ where
161155 SV : Validity ,
162156 DV : Validity ,
163157 Src : Immutable + ?Sized ,
164- Dst : Immutable + SizeEq < Src > + ?Sized ,
158+ Dst : Immutable + ?Sized ,
165159{
166160}
167161
0 commit comments