Skip to main content

Repr

vstd_extra::cast_ptr

Trait Repr 

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

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

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

Required Associated Types§

Source

type ReprPerm

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::ReprPerm) -> bool

Source

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

Source

exec fn to_repr(self, Tracked(perm): Tracked<&mut Self::ReprPerm>) -> 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::ReprPerm) -> Self

Source

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

requires
Self::wf(r, *perm),
returns
Self::from_repr_spec(r, *perm),
Source

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

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

exec fn from_borrowed_mut<'a>( r: &'a mut R, Tracked(perm): Tracked<&'a mut Self::ReprPerm>, ) -> res : &'a mut Self

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

Mutable counterpart of Self::from_borrowed. Implementations must project the same in-place representation as from_borrowed and keep the representation permission synchronized with mutations through the returned reference.

Source

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

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::ReprPerm)

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::ReprPerm)

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§