Trait SPRoundTripDpsRecBody 

pub trait SPRoundTripDpsRecBody: NonTailFmtRecBody
where
    Self::Body: SPRoundTripDps + NonTailFmt,
{
    // Required method
    proof fn lemma_body_sp_roundtrip_dps_inv_preservation(
        &self,
        param: Self::Param,
        rec: ParamRecSpecs<Self::Param, Self::T>,
    );
}

DPS serialize-parse roundtrip preservation for recursive bodies. Similar to Star, the body must also be NonTailFmt.

Required Methods

proof fn lemma_body_sp_roundtrip_dps_inv_preservation( &self, param: Self::Param, rec: ParamRecSpecs<Self::Param, Self::T>, )

requires

forall |p: Self::Param| rec(p).unambiguous(),

forall |p: Self::Param| rec(p).serialize_dps_inv(),

ensures

self.spec_body(param, rec).unambiguous(),

Implementors

impl<Body: StrictRecBody> SPRoundTripDpsRecBody for Body

where Body::Body: StrictCombinator,

impl<const DET: bool> SPRoundTripDpsRecBody for CborRecBody<DET>

impl<const MINIMAL: bool> SPRoundTripDpsRecBody for ULeb128RecBody<MINIMAL>