Skip to main content

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);
}
Expand description

A trait for types that have a concrete representation type R.

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,
*final(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),
returns
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§