@@ -14,7 +14,7 @@ use core::{
1414
1515use crate :: {
1616 pointer:: {
17- cast:: { self , CastExact , CastSizedExact } ,
17+ cast:: { self , Cast , CastExact , CastSizedExact } ,
1818 invariant:: * ,
1919 } ,
2020 FromBytes , Immutable , IntoBytes , Unalign ,
@@ -36,9 +36,9 @@ use crate::{
3636/// Given `Dst: TryTransmuteFromPtr<Src, A, SV, DV, C, _>`, callers may assume
3737/// the following:
3838///
39- /// Given `src: Ptr<'a, Src, (A, _, SV)>`, if the referent of `src` is
40- /// `DV`-valid for `Dst`, then it is sound to transmute `src` into `dst: Ptr<'a,
41- /// Dst, (A, Unaligned, DV)>` using `C `.
39+ /// Given `src: Ptr<'a, Src, (A, _, SV)>`, let `dst` be the result of casting
40+ /// from `src` using `C`. If `dst`'s referent is `DV`-valid for `Dst`, then it
41+ /// is sound to treat it as a `Ptr<'a, Dst, (A, Unaligned, DV)>`.
4242///
4343/// ## Pre-conditions
4444///
@@ -49,42 +49,50 @@ use crate::{
4949/// - So long as `dst` is active, no mutation of `dst`'s referent is allowed
5050/// except via `dst` itself
5151/// - The set of `DV`-valid referents of `dst` is a superset of the set of
52- /// `SV`-valid referents of `src` (NOTE: this condition effectively bans
53- /// shrinking or overwriting transmutes, which cannot satisfy this
54- /// condition)
52+ /// (the prefixes of) `SV`-valid referents of `src`. The "prefix" caveat is
53+ /// necessary since this may be a shrinking transmute – ie, `dst` addresses
54+ /// a smaller referent than `src`.
5555/// - Reverse transmutation: Either of the following hold:
5656/// - `dst` does not permit mutation of its referent
57- /// - The set of `DV`-valid referents of `dst` is a subset of the set of
58- /// `SV`-valid referents of `src` (NOTE: this condition effectively bans
59- /// shrinking or overwriting transmutes, which cannot satisfy this
60- /// condition)
57+ /// - `C: CastExact`, and the set of `DV`-valid referents of `dst` is a
58+ /// subset of the set of `SV`-valid referents of `src`
6159/// - No safe code, given access to `src` and `dst`, can cause undefined
6260/// behavior: Any of the following hold:
63- /// - `A` is `Exclusive`
61+ /// - `A` is `Exclusive`*
6462/// - `Src: Immutable` and `Dst: Immutable`
6563/// - It is sound for shared code to operate on a `&Src` and `&Dst` which
6664/// reference the same byte range at the same time
6765///
66+ /// * TODO: This assumes that `dst` shadows *all* of `src` (ie, `src` isn't
67+ /// split into `dst` and some other pointer/reference). Should we just restrict
68+ /// this trait's invariant to require that, if `A` is `Exclusive`, then `src`
69+ /// is inaccessible so long as `dst` is alive?
70+ ///
6871/// ## Proof
6972///
7073/// Given:
7174/// - `src: Ptr<'a, Src, (A, _, SV)>`
72- /// - `src`'s referent is `DV`-valid for `Dst`
75+ /// - `dst` is constructed by casting from `src` using `C`
76+ /// - `dst`'s referent is `DV`-valid for `Dst`
77+ ///
78+ /// We are trying to prove that it is sound to perform this cast from `src` to
79+ /// `dst` using `C` and treat `dst` as having invariants `(A, Unaligned, DV)`.
80+ /// We need to prove that such a cast does not violate any of `src`'s
81+ /// invariants, and that it satisfies all invariants of the destination `Ptr`
82+ /// type (`Ptr<'a, Dst, (A, Unaligned, DV)>`).
7383///
74- /// We are trying to prove that it is sound to perform a cast from `src` to a
75- /// `dst: Ptr<'a, Dst, (A, Unaligned, DV)>` using `C`. We need to prove that
76- /// such a cast does not violate any of `src`'s invariants, and that it
77- /// satisfies all invariants of the destination `Ptr` type.
84+ /// TODO: What does this first sentence even mean?
7885///
79- /// First, by `C: CastExact `, `src`'s address is unchanged, so it still satisfies
80- /// its alignment. Since `dst`'s alignment is `Unaligned`, it trivially satisfies
81- /// its alignment.
86+ /// First, by `C: Cast `, `src`'s address is unchanged, so it still satisfies its
87+ /// alignment. Since `dst`'s alignment is `Unaligned`, it trivially satisfies its
88+ /// alignment.
8289///
8390/// Second, aliasing is either `Exclusive` or `Shared`:
8491/// - If it is `Exclusive`, then both `src` and `dst` satisfy `Exclusive`
8592/// aliasing trivially: since `src` and `dst` have the same lifetime, `src` is
8693/// inaccessible so long as `dst` is alive, and no other live `Ptr`s or
87- /// references may reference the same referent.
94+ /// references may reference the same referent. (TODO: Add the following?)
95+ /// This holds even if `dst` addresses a subset of `src`'s referent.
8896/// - If it is `Shared`, then either:
8997/// - `Src: Immutable` and `Dst: Immutable`, and so `UnsafeCell`s trivially
9098/// cover the same byte ranges in both types.
@@ -95,8 +103,9 @@ use crate::{
95103/// as an `SV`-valid `Src`. It is guaranteed to remain so, as either of the
96104/// following hold:
97105/// - `dst` does not permit mutation of its referent.
98- /// - The set of `DV`-valid referents of `dst` is a subset of the set of
99- /// `SV`-valid referents of `src`. Thus, any value written via `dst` is
106+ /// - `C: CastExact`, and the set of `DV`-valid referents of `dst` is a subset
107+ /// of the set of `SV`-valid referents of `src`. By `CastExact`, `src` and
108+ /// `dst` address the same referent. Thus, any value written via `dst` is
100109/// guaranteed to be an `SV`-valid referent of `src`.
101110///
102111/// Fourth, `dst`'s validity is satisfied. It is a given of this proof that the
@@ -105,14 +114,15 @@ use crate::{
105114/// - So long as `dst` is active, no mutation of the referent is allowed except
106115/// via `dst` itself.
107116/// - The set of `DV`-valid referents of `dst` is a superset of the set of
108- /// `SV`-valid referents of `src`. Thus, any value written via `src` is
109- /// guaranteed to be a `DV`-valid referent of `dst`.
117+ /// (the prefixes of) `SV`-valid referents of `src`. Thus, (the prefix of) any
118+ /// value written via `src` is guaranteed to be a `DV`-valid referent of
119+ /// `dst`.
110120pub unsafe trait TryTransmuteFromPtr <
111121 Src : ?Sized ,
112122 A : Aliasing ,
113123 SV : Validity ,
114124 DV : Validity ,
115- C : CastExact < Src , Self > ,
125+ C : Cast < Src , Self > ,
116126 R ,
117127>
118128{
@@ -130,14 +140,13 @@ pub enum BecauseMutationCompatible {}
130140// exists, no mutation is permitted except via that `Ptr`
131141// - Aliasing is `Shared`, `Src: Immutable`, and `Dst: Immutable`, in which
132142// case no mutation is possible via either `Ptr`
133- // - Since the underlying cast is size-preserving, `dst` addresses the same
134- // referent as `src`. By `Dst: TransmuteFrom<Src, SV, DV>`, the set of
135- // `DV`-valid referents of `dst` is a superset of the set of `SV`-valid
136- // referents of `src`.
137- // - Reverse transmutation: Since the underlying cast is size-preserving, `dst`
138- // addresses the same referent as `src`. By `Src: TransmuteFrom<Dst, DV, SV>`,
139- // the set of `DV`-valid referents of `src` is a subset of the set of
140- // `SV`-valid referents of `dst`.
143+ // - By `Dst: TransmuteFrom<Src, SV, DV>`, the set of `DV`-valid referents of
144+ // `dst` is a supserset of the set of (the prefixes of) `SV`-valid referents
145+ // of `src`.
146+ // - Reverse transmutation: Since `C: CastExact`, `dst` addresses the same
147+ // referent as `src`. By `Src: TransmuteFrom<Dst, DV, SV>`, the set of
148+ // `DV`-valid referents of `dst` is a subset of the set of `SV`-valid referents
149+ // of `src`.
141150// - No safe code, given access to `src` and `dst`, can cause undefined
142151// behavior: By `Dst: MutationCompatible<Src, A, SV, DV, _>`, at least one of
143152// the following holds:
@@ -171,7 +180,7 @@ where
171180 DV : Validity ,
172181 Src : Immutable + ?Sized ,
173182 Dst : Immutable + ?Sized ,
174- C : CastExact < Src , Dst > ,
183+ C : Cast < Src , Dst > ,
175184{
176185}
177186
@@ -268,28 +277,27 @@ pub unsafe trait TransmuteFromPtr<
268277 A : Aliasing ,
269278 SV : Validity ,
270279 DV : Validity ,
271- C : CastExact < Src , Self > ,
280+ C : Cast < Src , Self > ,
272281 R ,
273282> : TryTransmuteFromPtr < Src , A , SV , DV , C , R > + TransmuteFrom < Src , SV , DV >
274283{
275284}
276285
277286// SAFETY: The `where` bounds are equivalent to the safety invariant on
278287// `TransmuteFromPtr`.
279- unsafe impl <
280- Src : ?Sized ,
281- Dst : ?Sized ,
282- A : Aliasing ,
283- SV : Validity ,
284- DV : Validity ,
285- C : CastExact < Src , Dst > ,
286- R ,
287- > TransmuteFromPtr < Src , A , SV , DV , C , R > for Dst
288+ unsafe impl < Src : ?Sized , Dst : ?Sized , A : Aliasing , SV : Validity , DV : Validity , C : Cast < Src , Dst > , R >
289+ TransmuteFromPtr < Src , A , SV , DV , C , R > for Dst
288290where
289291 Dst : TransmuteFrom < Src , SV , DV > + TryTransmuteFromPtr < Src , A , SV , DV , C , R > ,
290292{
291293}
292294
295+ // TODO: We need to update the invariant of `TransmuteFrom` in order to make the
296+ // "reverse transmutation" impl of `TryTransmuteFromPtr` sound – currently, it
297+ // says that `Dst: TransmuteFrom<Src>` guarantees transmutation *even in the
298+ // case of a shrinking transmute*, but that's not currently guaranteed by
299+ // `TransmuteFrom`'s safety invariant.
300+
293301/// Denotes that any `SV`-valid `Src` may soundly be transmuted into a
294302/// `DV`-valid `Self`.
295303///
@@ -315,12 +323,12 @@ pub unsafe trait TransmuteFrom<Src: ?Sized, SV, DV> {}
315323///
316324/// `SizeEq` on its own conveys no safety guarantee. Any safety guarantees come
317325/// from the safety invariants on the associated [`CastFrom`] type, specifically
318- /// the [`CastExact `] bound.
326+ /// the [`Cast `] bound.
319327///
320328/// [`CastFrom`]: SizeEq::CastFrom
321- /// [`CastExact `]: CastExact
329+ /// [`Cast `]: cast::Cast
322330pub trait SizeEq < Src : ?Sized > {
323- type CastFrom : CastExact < Src , Self > ;
331+ type CastFrom : cast :: Cast < Src , Self > ;
324332}
325333
326334impl < T : ?Sized > SizeEq < T > for T {
0 commit comments