Skip to content

Commit

Permalink
[pointer][WIP] Transmute
Browse files Browse the repository at this point in the history
gherrit-pr-id: Iad14813bc6d933312bc8d7a1ddcf1aafc7126938
  • Loading branch information
joshlf committed Feb 28, 2025
1 parent feb5ccf commit bd18425
Show file tree
Hide file tree
Showing 2 changed files with 91 additions and 0 deletions.
1 change: 1 addition & 0 deletions src/pointer/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ mod inner;
#[doc(hidden)]
pub mod invariant;
mod ptr;
mod transmute;

#[doc(hidden)]
pub use invariant::{BecauseExclusive, BecauseImmutable, Read};
Expand Down
90 changes: 90 additions & 0 deletions src/pointer/transmute.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,90 @@
// Copyright 2025 The Fuchsia Authors
//
// Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
// <LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
// license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
// This file may not be copied, modified, or distributed except according to
// those terms.

use crate::{Immutable, pointer::invariant::*};

/// # Safety
///
/// ## Post-conditions
///
/// Given `Dst: TryTransmuteFromPtr<Src, A, _>`, callers may assume the
/// following:
///
/// Given `src: Ptr<Src, SI>` where `SI: Invariants<Aliasing = A, Validity =
/// SV>`, if the referent of `src` contains a `Dst` which conforms to the
/// validity `DV`, then it is sound to transmute `src` into `dst: Ptr<Dst, DI>`
/// whre `DI: Invariants<Aliasing = A, Validity = DV>`.
///
/// TODO: Mention alignment
///
/// ## Pre-conditions
///
/// Given `src: Ptr<Src, SI>`, `dst: Ptr<Dst, DI>`, `SI: Invariants<Aliasing =
/// A, Validity = SV>`, and `DV: Invariants<Aliasing = A, Validity = DV>`, `Dst:
/// TryTransmuteFromPtr<Src, A, _>` is sound if all of the following
/// hold:
/// - Forwards transmutation: Any of the following hold:
/// - So long as `dst` is active, no mutation of `dst`'s referent is allowed
/// except via `dst` itself
/// - The set of `DV`-valid `Dst`s is a superset of the set of `SV`-valid
/// `Src`s
/// - Reverse transmutation: Any of the following hold:
/// - `dst` does not permit mutation of its referent
/// - The set of `DV`-valid `Dst`s is a subset of the set of `SV`-valid
/// `Src`s
/// - Interior mutation: TODO (ie, at least one of `Exclusive` or `Immutable`
/// required)
///
/// ## Proof
///
/// TODO: Prove that the pre-conditions imply the post-conditions.
#[cfg_attr(__ZEROCOPY_INTERNAL_USE_ONLY_NIGHTLY_FEATURES_IN_TESTS, marker)]
pub(crate) unsafe trait TryTransmuteFromPtr<Src, A: Aliasing, SV: Validity, DV: Validity, R>:
Validity
{
}

pub(crate) enum BecauseRead {}

// SAFETY:
// - Forwards transmutation: Since `Src::Inner: Read<A, R>`, one of the
// following holds:
// - `Src: Immutable`, so no mutation of `dst`'s referent is permitted via
// `src`. No other references to the same referent may exist which are typed
// using `T: !Immutable`, as this would permit violating `Src: Immutable`'s
// soundness precondition.
// - Aliasing `A` is `Exclusive`, so `dst` is the only reference permitted to
// mutate its referent.
// - Reverse transmutation: Since `Src: TransmuteFrom<Dst>`, `Dst`'s validity
// set is a subset of `Src`'s validity set.
// - Since `Src::Inner: Read` and `Dst::Inner: Read`, one of the following
// holds:
// - Aliasing `A` is `Exclusive`, in which case `UnsafeCell`s do not need to
// agree
// - `Src::Inner: Immutable` and `Dst::Inner: Immutable`, in which case
// `UnsafeCell`s trivially agree
unsafe impl<Src, Dst, SV, DV, A, R> TryTransmuteFromPtr<Src, A, SV, DV, (BecauseRead, R)> for Dst
where
A: Aliasing,
SV: Validity,
DV: Validity,
Src: TransmuteFrom<Dst, DV, SV> + Read<A, R>,
Dst: Read<A, R>,
{
}

unsafe impl<Src, Dst, SV, DV> TryTransmuteFromPtr<Src, Shared, SV, DV, BecauseImmutable> for Dst
where
SV: Validity,
DV: Validity,
Src: Immutable,
Dst: Immutable,
{
}

unsafe trait TransmuteFrom<Src, SV, DV> {}

0 comments on commit bd18425

Please sign in to comment.