Struct BerLengthFmt 

pub struct BerLengthFmt;

BER length determinant accepting both definite and indefinite encodings.

Trait Implementations

impl ByteLen<BerLength> for BerLengthFmt

exec fn length(&self, v: &BerLength) -> usize

fn exec_inv(&self) -> bool

impl Clone for BerLengthFmt

fn clone(&self) -> BerLengthFmt

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Consistency for BerLengthFmt

open spec fn consistent(&self, v: Self::Val) -> bool

{ ber_length_fmt().consistent(v) }

type Val = BerLength

The type of values whose consistency is being checked.

impl EquivSerializers for BerLengthFmt

proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal)

fn equiv_inv(&self) -> bool

impl EquivSerializersGeneral for BerLengthFmt

proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>)

fn equiv_general_inv(&self) -> bool

impl GoodSerializer for BerLengthFmt

proof fn lemma_serialize_len(&self, v: Self::SVal)

fn serialize_inv(&self) -> bool

impl NoLookAhead for BerLengthFmt

proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>)

fn no_lookahead_inv(&self) -> bool

fn corollary_non_extensible(&self, i1: Seq<u8>, i2: Seq<u8>)

impl NonTailFmt for BerLengthFmt

proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>)

proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>)

fn serialize_dps_inv(&self) -> bool

impl Parser<&[u8]> for BerLengthFmt

exec fn parse(&self, ibuf: &&[u8]) -> PResult<Self::PT>

type PT = BerLength

Executable value returned by this parser.

fn exec_inv(&self) -> bool

impl Prepare<BerLength> for BerLengthFmt

exec fn prepare(&self, v: &BerLength) -> Result<usize, PreSerializeError>

fn exec_inv(&self) -> bool

impl Productive for BerLengthFmt

proof fn lemma_productive(&self, ibuf: Seq<u8>)

fn productive_inv(&self) -> bool

impl SPRoundTripDps for BerLengthFmt

proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>)

fn unambiguous(&self) -> bool

impl SafeParser for BerLengthFmt

proof fn lemma_parse_safe(&self, ibuf: Seq<u8>)

fn safe_inv(&self) -> bool

impl<Output: OutputBuf> Serializer<Output, BerLength> for BerLengthFmt

exec fn serialize_into(&self, v: &BerLength, obuf: &mut Output)

fn exec_inv(&self) -> bool

impl SpecByteLen for BerLengthFmt

open spec fn byte_len(&self, v: Self::T) -> nat

{ ber_length_fmt().byte_len(v) }

type T = BerLength

The type of values whose byte length is being computed.

impl SpecParser for BerLengthFmt

open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)>

{ ber_length_fmt().spec_parse(ibuf) }

type PVal = BerLength

The type of parsed values.

impl SpecSerializer for BerLengthFmt

open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8>

{ ber_length_fmt().spec_serialize(v) }

type SVal = BerLength

The type of values to be serialized.

impl SpecSerializerDps for BerLengthFmt

open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8>

{ ber_length_fmt().spec_serialize_dps(v, obuf) }

type SValue = BerLength

The type of values to be serialized.

impl Copy for BerLengthFmt