Struct PCellOwn

pub struct PCellOwn<T: ?Sized> {
    pub id: Id,
    pub val: Box<T>,
    /* private fields */
}

Token that represents the ownership of a PCell object.

A PCellOwn only exists in the ghost world, and it must be used in conjunction with PCell in order to read or write the value.

Fields

id: Id

val: Box<T>

Implementations

impl<T> PCellOwn<T>

where T: ?Sized,

pub fn id(self) -> Id

Returns the logical identity of the cell.

To use a [Pcell], this and PCell::id must agree.

logic

self.id

pub fn val(self) -> SizedW<T>

Get the logical value.

logic

self.val

pub fn disjoint_lemma(own1: &mut PCellOwn<T>, own2: &PCellOwn<T>)

If one owns two PCellOwns in ghost code, then they have different ids.

pure

ensures

own1.id() != own2.id()

ensures

*own1 == ^own1

Trait Implementations

impl<T> View for PCellOwn<T>

fn view(self) -> Self::ViewTy

logic

*self.val

type ViewTy = T