Struct BerOctetStringRecBody 

pub struct BerOctetStringRecBody;

Trait Implementations

impl<'i> ParserRecBody<&'i [u8]> for BerOctetStringRecBody

Available on crate feature alloc only.

exec fn parse_body<Exec>( &self, expected: &Tag, Ghost(spec_rec): Ghost<ParamRecSpecs<Tag, Seq<u8>>>, exec_rec: Exec, ibuf: &&'i [u8], ) -> PResult<Vec<u8>>

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

type EP = Tag

type O = Vec<u8>

impl ProductiveRecBody for BerOctetStringRecBody

proof fn lemma_body_productive_inv_preservation( &self, tag: Tag, rec: ParamRecSpecs<Tag, Seq<u8>>, )

impl SafeParserRecBody for BerOctetStringRecBody

proof fn lemma_body_safe_inv_preservation( &self, tag: Tag, rec: ParamRecSpecs<Tag, Seq<u8>>, )

impl SpecRecBody for BerOctetStringRecBody

open spec fn spec_body( &self, tag: Self::Param, rec: ParamRecSpecs<Self::Param, Self::T>, ) -> Self::Body

{ ber_octet_string_rec_body(tag, rec) }

type Param = Tag

type T = Seq<u8>

type Body = Mapped<Bind<TagFmt, FnSpec<(Tag,), Sum<Bind<LengthFmt<BER>, FnSpec<(usize,), ExactLen<Tail, usize>>>, Sum<Bind<BerLengthFmt, FnSpec<(BerLength,), Sum<ExactLen<RepeatTillEnd<(FnSpec<(Seq<u8>,), bool>, FnSpec<(Seq<u8>,), nat>, FnSpec<(Seq<u8>,), Option<(int, Seq<u8>)>>, FnSpec<(Seq<u8>,), Seq<u8>>, FnSpec<(Seq<u8>, Seq<u8>), Seq<u8>>)>, usize>, Repeat<(FnSpec<(Seq<u8>,), bool>, FnSpec<(Seq<u8>,), nat>, FnSpec<(Seq<u8>,), Option<(int, Seq<u8>)>>, FnSpec<(Seq<u8>,), Seq<u8>>, FnSpec<(Seq<u8>, Seq<u8>), Seq<u8>>), Pair<Const<TagFmt, Tag>, Const<U8, u8>>>>>>, Void>>>>, (FnSpec<((Tag, Sum<(usize, Seq<u8>), Sum<(BerLength, Sum<Seq<Seq<u8>>, (Seq<Seq<u8>>, (Tag, u8))>), ExecNever>>),), Seq<u8>>, FnSpec<(Seq<u8>,), (Tag, Sum<(usize, Seq<u8>), Sum<(BerLength, Sum<Seq<Seq<u8>>, (Seq<Seq<u8>>, (Tag, u8))>), ExecNever>>)>)>