Trait SerializerRecBody 

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

    // Required method
    exec fn serialize_body<Exec>(
        &self,
        param: &Self::EP,
        Ghost(spec_rec): Ghost<ParamRecSpecs<Self::Param, Self::T>>,
        exec_rec: Exec,
        v: &T,
        obuf: &mut Output,
    )
       where Exec: Fn(&Self::EP, &T, &mut Output);
}

Executable serialization for one recursive unfolding.

Required Associated Types

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

Required Methods

exec fn serialize_body<Exec>( &self, param: &Self::EP, Ghost(spec_rec): Ghost<ParamRecSpecs<Self::Param, Self::T>>, exec_rec: Exec, v: &T, obuf: &mut Output, )

where Exec: Fn(&Self::EP, &T, &mut Output),

requires

self.spec_body(param.deep_view(), spec_rec).consistent(v.deep_view()),

old(obuf).fits(self.spec_body(param.deep_view(), spec_rec).byte_len(v.deep_view())),

forall |pp: &Self::EP, vv: &T, out: &mut Output| (
    {
        &&& spec_rec(pp.deep_view()).0(vv.deep_view())
        &&& out.fits(spec_rec(pp.deep_view()).1(vv.deep_view()))

    } ==> call_requires(exec_rec, (pp, vv, out))
),

forall |pp: &Self::EP, vv: &T, out: &mut Output| {
    call_ensures(exec_rec, (pp, vv, out), ())
        ==> {
            &&& final(out)@ == out@ + spec_rec(pp.deep_view()).3(vv.deep_view())
            &&& forall |n| {
                out.fits(spec_rec(pp.deep_view()).1(vv.deep_view()) + n) <==> #[trigger]
                    final(out).fits(n)
            }
            &&& out.same_destination(final(out))

        }
},

ensures

final(obuf)@
    == old(obuf)@
        + self.spec_body(param.deep_view(), spec_rec).spec_serialize(v.deep_view()),

forall |n| {
    old(obuf)
        .fits(self.spec_body(param.deep_view(), spec_rec).byte_len(v.deep_view()) + n)
        <==> #[trigger] final(obuf).fits(n)
},

old(obuf).same_destination(final(obuf)),

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, Output: OutputBuf, const DET: bool> SerializerRecBody<Output, CborValue<'i>> for CborRecBody<DET>

type EP = ()