melinoe 0.10.0

Zero-sized, branded, multi-token phantom capabilities for compile-time data-access and thread-synchronization proofs (a generalized evolution of GhostCell) for the Mnemosyne memory ecosystem.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78

//! Sealed capability traits shared by every Melinoe token family.
//!
//! A *permit* is evidence, materialised in the borrow checker, that the holder
//! may access branded data in a particular mode. Permits are produced only by
//! the token types in this crate; the traits are [sealed] so downstream crates
//! cannot forge a permit by implementing the trait on a foreign type.
//!
//! The capability lattice is intentionally tiny:
//!
//! ```text
//!   WritePermit<'brand>  ⊑  ReadPermit<'brand>
//! ```
//!
//! Every write permit is also a read permit; the reverse does not hold.
//!
//! [sealed]: https://rust-lang.github.io/api-guidelines/future-proofing.html

/// Crate-private supertrait used to seal the public capability traits.
///
/// The module is `pub(crate)`, so the trait is nameable in bounds inside this
/// crate yet unreachable—and therefore unimplementable—from any other crate.
pub(crate) mod private {
    /// Sealing marker. Implemented only for the in-crate permit carriers.
    pub trait Sealed {}

    /// Sealing marker for unique brand-owning tokens.
    pub trait BrandOwner {}
}

/// Unique brand owner whose borrows carry Melinoe's read/write permits.
///
/// # Safety
///
/// Implementors must be the sole owning token for their `'brand`, such that a
/// shared borrow proves read access and a mutable borrow proves exclusive write
/// access for the entire branded region.
pub(crate) unsafe trait BrandOwner<'brand>: private::BrandOwner {}

/// Evidence that the bearer may obtain a shared (`&T`) view of any
/// [`MelinoeCell`](crate::MelinoeCell) carrying the matching `'brand`.
///
/// # Safety
///
/// This trait is `unsafe` because [`MelinoeCell`](crate::MelinoeCell) relies on
/// implementors to uphold the brand's exclusion invariant: while *any*
/// `ReadPermit<'brand>` value is borrowed, no `&mut` token for the same
/// `'brand` may simultaneously exist. Every in-crate implementor discharges
/// this obligation through the borrow checker (the permit either *is* a borrow
/// of the unique token, or carries one in a `PhantomData`). External crates
/// cannot implement this trait because of the private `Sealed` supertrait.
pub unsafe trait ReadPermit<'brand>: private::Sealed {}

/// Evidence that the bearer may obtain an exclusive (`&mut T`) view of any
/// [`MelinoeCell`](crate::MelinoeCell) carrying the matching `'brand`.
///
/// # Safety
///
/// Implementors must additionally guarantee that holding a `WritePermit<'brand>`
/// excludes every other read *and* write permit of the same brand for the
/// duration of the borrow. In practice the only implementors are exclusive
/// `&mut` borrows of a brand's unique owning token, which the borrow checker
/// proves disjoint from all other token borrows.
pub unsafe trait WritePermit<'brand>: ReadPermit<'brand> {}

impl<'brand, T> private::Sealed for &T where T: BrandOwner<'brand> {}

impl<'brand, T> private::Sealed for &mut T where T: BrandOwner<'brand> {}

// SAFETY: every `BrandOwner` implementor represents the unique token of its
// brand, so a shared borrow is sufficient evidence that no mutable borrow of
// that token, and hence no write permit, coexists for the same brand.
unsafe impl<'brand, T> ReadPermit<'brand> for &T where T: BrandOwner<'brand> {}

// SAFETY: a mutable borrow of a unique `BrandOwner` token excludes all other
// shared and mutable borrows of that token, which is exactly the brand-wide XOR
// guarantee required for both read and write access.
unsafe impl<'brand, T> ReadPermit<'brand> for &mut T where T: BrandOwner<'brand> {}
unsafe impl<'brand, T> WritePermit<'brand> for &mut T where T: BrandOwner<'brand> {}