Struct singleton_trait::Erased

pub struct Erased<T> { /* fields omitted */ }

The Exists struct witnesses the logical ownership of a value of type T while remaining zero-sized. This can be used for ghost proofs of soundness.

Erased should be thought of a zero-sized owner of T.

NOTE: drop implementations will never be called, as Exists guarantees the existence of a valid T, which might not be true if they were called. On the other hand, since it does not hold a T, it cannot drop T when it is itself dropped

Secondly, keep in mind that while Exists serves as evidence, it does not include sufficient providence for either Stacked Borrows or LLVM, and so it is not sound in general to recover a reference from an Exists<&T> and *mut T or &UnsafeCell<T> even when T is Singleton, but this could be possible if T is zero-sized.

Implementations

impl<T> Erased<T>

pub const fn new(t: T) -> Self

pub const unsafe fn new_unchecked() -> Self

This function constructs a value of Erased without taking logical ownership of a T.

Safety

Constructing this asserts that there is a value of type T which has been leaked, or in which it is guaranteed that the program behaves the same up to observation as if a zero-sized copy of T were being passed.

pub fn borrow(&self) -> Erased<&T>

pub fn borrow_mut(&mut self) -> Erased<&mut T>

pub unsafe fn map<R, F: FnOnce(T) -> R>(self, _: impl Exists<F>) -> Erased<R>

Maps a function on the inside of the Erased body (existential induction).

Safety

Due to the strictness guarantees, the passed closure must not cause any visible side effects, including side effects caused by owning R

pub unsafe fn map_borrow<'a, R, F: FnOnce(&'a T) -> R>(
    &'a self,
    _: impl Exists<F>
) -> Erased<R>

Maps a function on the borrow of the Erased field (existential induction).

Safety

Due to the strictness guarantees, the passed closure must not cause any visible side effects, including side effects caused by owning R

pub unsafe fn map_borrow_mut<'a, R, F: FnOnce(&'a mut T) -> R>(
    &'a mut self,
    _: impl Exists<F>
) -> Erased<R>

Maps a function on the mutable borrow of the Erased field.

Safety

Due to the strictness guarantees, the passed closure must not cause any visible side effects, including side effects caused by owning R

impl<T> Erased<Erased<T>>

pub fn flatten(self) -> Erased<T>

An erased erased value can be flattened into a single erasure, since Erased is notionally equivalent to T

impl<'a, T> Erased<&'a mut T>

pub fn reborrow<'b>(&'b mut self) -> Erased<&'b mut T>

Trait Implementations

impl<T: Clone> Clone for Erased<T>

fn clone(&self) -> Erased<T>

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<T> From<T> for Erased<T>

fn from(t: T) -> Self

Performs the conversion.

impl<T: Copy> Copy for Erased<T>

impl<'a, T: Singleton> Singleton for Erased<T>