Repr

vstd_extra::cast_ptr

Trait Repr 

Source 
pub trait Repr<R: Sized>: Sized {
    type Perm;

    // Required methods
    spec fn wf(r: R, perm: Self::Perm) -> bool;
    spec fn to_repr_spec(self, perm: Self::Perm) -> (R, Self::Perm);
    exec fn to_repr(self, Tracked(perm): Tracked<&mut Self::Perm>) -> res : R;
    spec fn from_repr_spec(r: R, perm: Self::Perm) -> Self;
    exec fn from_repr(r: R, Tracked(perm): Tracked<&Self::Perm>) -> res : Self;
    exec fn from_borrowed<'a>(
        r: &'a R,
        verus_tmp_perm: Tracked<&'a Self::Perm>,
    ) -> res : &'a Self;
    proof fn from_to_repr(self, perm: Self::Perm);
    proof fn to_from_repr(r: R, perm: Self::Perm);
    proof fn to_repr_wf(self, perm: Self::Perm);
}

Required Associated Types§

Source

type Perm

If the underlying representation contains cells, the translation may require permission objects that access them.

Required Methods§

Source

spec fn wf(r: R, perm: Self::Perm) -> bool

Source

spec fn to_repr_spec(self, perm: Self::Perm) -> (R, Self::Perm)

Source

exec fn to_repr(self, Tracked(perm): Tracked<&mut Self::Perm>) -> res : R

ensures
res == self.to_repr_spec(*old(perm)).0,
*perm == self.to_repr_spec(*old(perm)).1,
Source

spec fn from_repr_spec(r: R, perm: Self::Perm) -> Self

Source

exec fn from_repr(r: R, Tracked(perm): Tracked<&Self::Perm>) -> res : Self

requires
Self::wf(r, *perm),
ensures
res == Self::from_repr_spec(r, *perm),
Source

exec fn from_borrowed<'a>( r: &'a R, verus_tmp_perm: Tracked<&'a Self::Perm>, ) -> res : &'a Self

requires
Self::wf(*r, *perm),
ensures
*res == Self::from_repr_spec(*r, *perm),
Source

proof fn from_to_repr(self, perm: Self::Perm)

ensures
Self::from_repr_spec(self.to_repr_spec(perm).0, self.to_repr_spec(perm).1) == self,
Source

proof fn to_from_repr(r: R, perm: Self::Perm)

requires
Self::wf(r, perm),
ensures
Self::from_repr_spec(r, perm).to_repr_spec(perm) == (r, perm),
Source

proof fn to_repr_wf(self, perm: Self::Perm)

ensures
Self::wf(self.to_repr_spec(perm).0, self.to_repr_spec(perm).1),

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§