Struct BerBitStringRecBody 

pub struct BerBitStringRecBody;

Trait Implementations

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

Available on crate feature alloc only.

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

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

type EP = Tag

type O = BitStringOwned

impl ProductiveRecBody for BerBitStringRecBody

proof fn lemma_body_productive_inv_preservation( &self, _tag: Tag, _rec: ParamRecSpecs<Tag, BitStringSpec>, )

impl SafeParserRecBody for BerBitStringRecBody

proof fn lemma_body_safe_inv_preservation( &self, _tag: Tag, _rec: ParamRecSpecs<Tag, BitStringSpec>, )

impl SpecRecBody for BerBitStringRecBody

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

{ ber_bit_string_rec_body(tag, rec) }

type Param = Tag

type T = BitStringSpec

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