Trait PrepareRecBody 

pub trait PrepareRecBody<T>: SpecRecBody
where
    T: DeepView<V = Self::T>,
{
    type EP: DeepView<V = Self::Param>;

    // Required method
    exec fn prepare_body<Exec>(
        &self,
        param: &Self::EP,
        Ghost(spec_rec): Ghost<ParamRecSpecs<Self::Param, Self::T>>,
        exec_rec: Exec,
        v: &T,
    ) -> checked : Result<usize, PreSerializeError>
       where Exec: Fn(&Self::EP, &T) -> Result<usize, PreSerializeError>;
}

Executable pre-serialization analysis for one recursive unfolding.

Required Associated Types

type EP: DeepView<V = Self::Param>

Required Methods

exec fn prepare_body<Exec>( &self, param: &Self::EP, Ghost(spec_rec): Ghost<ParamRecSpecs<Self::Param, Self::T>>, exec_rec: Exec, v: &T, ) -> checked : Result<usize, PreSerializeError>

where Exec: Fn(&Self::EP, &T) -> Result<usize, PreSerializeError>,

requires

forall |pp: &Self::EP, vv: &T| call_requires(exec_rec, (pp, vv)),

forall |pp: &Self::EP, vv: &T, rr: Result<usize, PreSerializeError>| {
    call_ensures(exec_rec, (pp, vv), rr)
        ==> (rr matches Ok(
            len,
        ) ==> {
            &&& spec_rec(pp.deep_view()).0(vv.deep_view())
            &&& len == spec_rec(pp.deep_view()).1(vv.deep_view())

        })
},

ensures

checked matches Ok(
    len,
) ==> {
    &&& self.spec_body(param.deep_view(), spec_rec).consistent(v.deep_view())
    &&& len == self.spec_body(param.deep_view(), spec_rec).byte_len(v.deep_view())

},

Execute one recursive unfolding, using exec_rec for all recursive positions in the body.

spec_rec is the ghost/spec callback bundle corresponding to exec_rec.

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

impl<'i> PrepareRecBody<CborValue<'i>> for CborRecBody<false>

where CborRecBody<false>: SpecRecBody<Param = (), T = CborValueSpec, Body = CborBodyFmt<false>>,

type EP = ()

impl<'i> PrepareRecBody<CborValue<'i>> for CborRecBody<true>

where CborRecBody<true>: SpecRecBody<Param = (), T = CborValueSpec, Body = CborBodyFmt<true>>,

type EP = ()