Struct BerEndFmt 

pub struct BerEndFmt;

Zero-width boundary marker for the contents of a schema-defined BER constructed value.

It succeeds at the end of a definite-length input or immediately before EOC. In the latter case it deliberately leaves EOC unconsumed for the enclosing indefinite-length framing combinator. Serialization emits no bytes.

Trait Implementations

impl AdmitsUniqueVal for BerEndFmt

proof fn lemma_unique_consistent_val(&self, _left: Self::Val, _right: Self::Val)

impl ByteLen<()> for BerEndFmt

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

fn exec_inv(&self) -> bool

impl Clone for BerEndFmt

fn clone(&self) -> BerEndFmt

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Consistency for BerEndFmt

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

{ true }

type Val = ()

The type of values whose consistency is being checked.

impl EquivSerializers for BerEndFmt

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

fn equiv_inv(&self) -> bool

impl GoodSerializer for BerEndFmt

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

fn serialize_inv(&self) -> bool

impl HasAsn1Start for BerEndFmt

BER_END recognizes either EOF or an EOC prefix without consuming it.

open spec fn asn1_start(&self) -> Asn1StartDomain

{ asn1_start_ber_boundary() }

proof fn lemma_parse_implies_asn1_start(&self, input: Seq<u8>)

impl<'i> Parser<&'i [u8]> for BerEndFmt

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

type PT = ()

Executable value returned by this parser.

fn exec_inv(&self) -> bool

impl Prepare<()> for BerEndFmt

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

fn exec_inv(&self) -> bool

impl Productive for BerEndFmt

open spec fn productive_inv(&self) -> bool

{ false }

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

impl SPRoundTripDps for BerEndFmt

proof fn theorem_serialize_dps_parse_roundtrip(&self, _value: Self::T, _obuf: Seq<u8>)

fn unambiguous(&self) -> bool

impl SafeParser for BerEndFmt

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

fn safe_inv(&self) -> bool

impl<Output: OutputBuf> Serializer<Output, ()> for BerEndFmt

exec fn serialize_into(&self, _value: &(), _obuf: &mut Output)

fn exec_inv(&self) -> bool

impl SpecByteLen for BerEndFmt

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

{ 0 }

type T = ()

The type of values whose byte length is being computed.

impl SpecParser for BerEndFmt

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

{ if at_ber_end(input) { Some((0, ())) } else { None } }

type PVal = ()

The type of parsed values.

impl SpecSerializer for BerEndFmt

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

{ Seq::empty() }

type SVal = ()

The type of values to be serialized.

impl SpecSerializerDps for BerEndFmt

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

{ Seq::empty() }

type SValue = ()

The type of values to be serialized.

impl Copy for BerEndFmt