Struct CborRecBody 

pub struct CborRecBody<const DET: bool>;

Trait Implementations

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

proof fn lemma_s_body_equiv_general_inv_preservation( &self, _param: (), _rec: ParamRecSpecs<(), CborValueSpec>, )

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

proof fn lemma_s_body_serialize_inv_preservation( &self, _param: (), _rec: ParamRecSpecs<(), CborValueSpec>, )

impl NonMalleableRecBody for CborRecBody<true>

proof fn lemma_body_nonmal_inv_preservation( &self, _param: (), _rec: ParamRecSpecs<(), CborValueSpec>, )

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

proof fn lemma_s_body_dps_serialize_dps_inv_preservation( &self, _param: (), _rec: ParamRecSpecs<(), CborValueSpec>, )

impl<'i> ParserRecBody<&'i [u8]> for CborRecBody<false>

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

exec fn parse_body<Exec>( &self, param: &(), spec_rec: Ghost<ParamRecSpecs<(), CborValueSpec>>, exec_rec: Exec, input: &&'i [u8], ) -> PResult<Self::O>

where Exec: Fn(&(), &&'i [u8]) -> PResult<Self::O>,

type EP = ()

type O = CborValue<'i>

impl<'i> ParserRecBody<&'i [u8]> for CborRecBody<true>

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

exec fn parse_body<Exec>( &self, param: &(), spec_rec: Ghost<ParamRecSpecs<(), CborValueSpec>>, exec_rec: Exec, input: &&'i [u8], ) -> PResult<Self::O>

where Exec: Fn(&(), &&'i [u8]) -> PResult<Self::O>,

type EP = ()

type O = CborValue<'i>

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

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

exec fn prepare_body<Exec>( &self, _param: &(), spec_rec: Ghost<ParamRecSpecs<(), CborValueSpec>>, exec_rec: Exec, value: &CborValue<'i>, ) -> Result<usize, PreSerializeError>

where Exec: Fn(&(), &CborValue<'i>) -> Result<usize, PreSerializeError>,

type EP = ()

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

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

exec fn prepare_body<Exec>( &self, _param: &(), spec_rec: Ghost<ParamRecSpecs<(), CborValueSpec>>, exec_rec: Exec, value: &CborValue<'i>, ) -> Result<usize, PreSerializeError>

where Exec: Fn(&(), &CborValue<'i>) -> Result<usize, PreSerializeError>,

type EP = ()

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

proof fn lemma_body_productive_inv_preservation( &self, _param: (), _rec: ParamRecSpecs<(), CborValueSpec>, )

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

proof fn lemma_body_sp_roundtrip_dps_inv_preservation( &self, _param: (), _rec: ParamRecSpecs<(), CborValueSpec>, )

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

proof fn lemma_body_safe_inv_preservation( &self, _param: (), _rec: ParamRecSpecs<(), CborValueSpec>, )

impl<'i, Output: OutputBuf, const DET: bool> SerializerRecBody<Output, CborValue<'i>> for CborRecBody<DET>

exec fn serialize_body<Exec>( &self, _param: &(), Ghost(spec_rec): Ghost<ParamRecSpecs<(), CborValueSpec>>, exec_rec: Exec, value: &CborValue<'i>, out: &mut Output, )

where Exec: Fn(&(), &CborValue<'i>, &mut Output),

type EP = ()

impl SoundParserRecBody for CborRecBody<true>

proof fn lemma_body_sound_inv_preservation( &self, _param: (), _rec: ParamRecSpecs<(), CborValueSpec>, )

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

open spec fn spec_body( &self, _param: (), rec: ParamRecSpecs<(), CborValueSpec>, ) -> Self::Body

{ cbor_body::<DET>(rec) }

type Param = ()

type T = CborValueSpec

type Body = CborBodyFmt<DET>