Repr

vstd_extra::cast_ptr

Trait Repr 

Source 
pub trait Repr<R: Sized>: Sized {
    // Required methods
    spec fn wf(r: R) -> bool;
    spec fn to_repr_spec(self) -> R;
    exec fn to_repr(self) -> res : R;
    spec fn from_repr_spec(r: R) -> Self;
    exec fn from_repr(r: R) -> res : Self;
    exec fn from_borrowed<'a>(r: &'a R) -> res : &'a Self;
    proof fn from_to_repr(self);
    proof fn to_from_repr(r: R);
    proof fn to_repr_wf(self);
}

Required Methods§

Source

spec fn wf(r: R) -> bool

Source

spec fn to_repr_spec(self) -> R

Source

exec fn to_repr(self) -> res : R

ensures
res == self.to_repr_spec(),
Source

spec fn from_repr_spec(r: R) -> Self

Source

exec fn from_repr(r: R) -> res : Self

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

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

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

proof fn from_to_repr(self)

ensures
Self::from_repr(self.to_repr()) == self,
Source

proof fn to_from_repr(r: R)

requires
Self::wf(r),
ensures
Self::from_repr(r).to_repr() == r,
Source

proof fn to_repr_wf(self)

ensures
Self::wf(self.to_repr()),

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§