Trait NonMalleableRecBody 

pub trait NonMalleableRecBody: SafeParserRecBody + SoundParserRecBody
where
    Self::Body: NonMalleable + SoundParser,
{
    // Required method
    proof fn lemma_body_nonmal_inv_preservation(
        &self,
        param: Self::Param,
        rec: ParamRecSpecs<Self::Param, Self::T>,
    );
}

Non-malleability preservation for recursive bodies.

Required Methods

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

requires

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

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

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

ensures

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

Implementors

impl NonMalleableRecBody for CborRecBody<true>

impl NonMalleableRecBody for ULeb128RecBody<true>

impl<Body: StrictRecBody> NonMalleableRecBody for Body

where Body::Body: StrictCombinator,