Skip to content

Commit bd18425

Browse files
committed
[pointer][WIP] Transmute
gherrit-pr-id: Iad14813bc6d933312bc8d7a1ddcf1aafc7126938
1 parent feb5ccf commit bd18425

File tree

2 files changed

+91
-0
lines changed

2 files changed

+91
-0
lines changed

src/pointer/mod.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ mod inner;
1212
#[doc(hidden)]
1313
pub mod invariant;
1414
mod ptr;
15+
mod transmute;
1516

1617
#[doc(hidden)]
1718
pub use invariant::{BecauseExclusive, BecauseImmutable, Read};

src/pointer/transmute.rs

Lines changed: 90 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,90 @@
1+
// Copyright 2025 The Fuchsia Authors
2+
//
3+
// Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
4+
// <LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
5+
// license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
6+
// This file may not be copied, modified, or distributed except according to
7+
// those terms.
8+
9+
use crate::{Immutable, pointer::invariant::*};
10+
11+
/// # Safety
12+
///
13+
/// ## Post-conditions
14+
///
15+
/// Given `Dst: TryTransmuteFromPtr<Src, A, _>`, callers may assume the
16+
/// following:
17+
///
18+
/// Given `src: Ptr<Src, SI>` where `SI: Invariants<Aliasing = A, Validity =
19+
/// SV>`, if the referent of `src` contains a `Dst` which conforms to the
20+
/// validity `DV`, then it is sound to transmute `src` into `dst: Ptr<Dst, DI>`
21+
/// whre `DI: Invariants<Aliasing = A, Validity = DV>`.
22+
///
23+
/// TODO: Mention alignment
24+
///
25+
/// ## Pre-conditions
26+
///
27+
/// Given `src: Ptr<Src, SI>`, `dst: Ptr<Dst, DI>`, `SI: Invariants<Aliasing =
28+
/// A, Validity = SV>`, and `DV: Invariants<Aliasing = A, Validity = DV>`, `Dst:
29+
/// TryTransmuteFromPtr<Src, A, _>` is sound if all of the following
30+
/// hold:
31+
/// - Forwards transmutation: Any of the following hold:
32+
/// - So long as `dst` is active, no mutation of `dst`'s referent is allowed
33+
/// except via `dst` itself
34+
/// - The set of `DV`-valid `Dst`s is a superset of the set of `SV`-valid
35+
/// `Src`s
36+
/// - Reverse transmutation: Any of the following hold:
37+
/// - `dst` does not permit mutation of its referent
38+
/// - The set of `DV`-valid `Dst`s is a subset of the set of `SV`-valid
39+
/// `Src`s
40+
/// - Interior mutation: TODO (ie, at least one of `Exclusive` or `Immutable`
41+
/// required)
42+
///
43+
/// ## Proof
44+
///
45+
/// TODO: Prove that the pre-conditions imply the post-conditions.
46+
#[cfg_attr(__ZEROCOPY_INTERNAL_USE_ONLY_NIGHTLY_FEATURES_IN_TESTS, marker)]
47+
pub(crate) unsafe trait TryTransmuteFromPtr<Src, A: Aliasing, SV: Validity, DV: Validity, R>:
48+
Validity
49+
{
50+
}
51+
52+
pub(crate) enum BecauseRead {}
53+
54+
// SAFETY:
55+
// - Forwards transmutation: Since `Src::Inner: Read<A, R>`, one of the
56+
// following holds:
57+
// - `Src: Immutable`, so no mutation of `dst`'s referent is permitted via
58+
// `src`. No other references to the same referent may exist which are typed
59+
// using `T: !Immutable`, as this would permit violating `Src: Immutable`'s
60+
// soundness precondition.
61+
// - Aliasing `A` is `Exclusive`, so `dst` is the only reference permitted to
62+
// mutate its referent.
63+
// - Reverse transmutation: Since `Src: TransmuteFrom<Dst>`, `Dst`'s validity
64+
// set is a subset of `Src`'s validity set.
65+
// - Since `Src::Inner: Read` and `Dst::Inner: Read`, one of the following
66+
// holds:
67+
// - Aliasing `A` is `Exclusive`, in which case `UnsafeCell`s do not need to
68+
// agree
69+
// - `Src::Inner: Immutable` and `Dst::Inner: Immutable`, in which case
70+
// `UnsafeCell`s trivially agree
71+
unsafe impl<Src, Dst, SV, DV, A, R> TryTransmuteFromPtr<Src, A, SV, DV, (BecauseRead, R)> for Dst
72+
where
73+
A: Aliasing,
74+
SV: Validity,
75+
DV: Validity,
76+
Src: TransmuteFrom<Dst, DV, SV> + Read<A, R>,
77+
Dst: Read<A, R>,
78+
{
79+
}
80+
81+
unsafe impl<Src, Dst, SV, DV> TryTransmuteFromPtr<Src, Shared, SV, DV, BecauseImmutable> for Dst
82+
where
83+
SV: Validity,
84+
DV: Validity,
85+
Src: Immutable,
86+
Dst: Immutable,
87+
{
88+
}
89+
90+
unsafe trait TransmuteFrom<Src, SV, DV> {}

0 commit comments

Comments
 (0)