Trait StrictRecBody 

pub trait StrictRecBody: SpecRecBody
where
    Self::Body: StrictCombinator,
{
    // Required method
    proof fn lemma_body_all_inv_preservation(
        &self,
        param: Self::Param,
        rec: ParamRecSpecs<Self::Param, Self::T>,
    );
}

Convenience trait bundling the standard recursive-body preservation obligations.

Implementing this once is enough to derive the individual *RecBody traits via blanket impls.

Required Methods

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

ensures

(forall |p: Self::Param| rec(p).safe_inv()) ==> self.spec_body(param, rec).safe_inv(),

(forall |p: Self::Param| rec(p).productive_inv())
    ==> self.spec_body(param, rec).productive_inv(),

(forall |p: Self::Param| rec(p).sound_inv()) ==> self.spec_body(param, rec).sound_inv(),

(forall |p: Self::Param| rec(p).safe_inv())
    && (forall |p: Self::Param| rec(p).sound_inv())
    && (forall |p: Self::Param| rec(p).nonmal_inv())
    ==> self.spec_body(param, rec).nonmal_inv(),

(forall |p: Self::Param| rec(p).serialize_inv())
    ==> self.spec_body(param, rec).serialize_inv(),

(forall |p: Self::Param| rec(p).serialize_dps_inv())
    ==> self.spec_body(param, rec).serialize_dps_inv(),

(forall |p: Self::Param| rec(p).unambiguous())
    && (forall |p: Self::Param| rec(p).serialize_dps_inv())
    ==> self.spec_body(param, rec).unambiguous(),

(forall |p: Self::Param| rec(p).equiv_general_inv())
    ==> self.spec_body(param, rec).equiv_general_inv(),

Implementors