Struct BerSequenceFmt 

pub struct BerSequenceFmt<C>(pub Tag, pub C);

BER SEQUENCE codec with a configurable outer tag.

Parsing accepts definite and indefinite framing for one schema body. Serialization always emits the normalized definite-length form.

Tuple Fields

0: Tag

1: C

Implementations

impl<C: Copy> BerSequenceFmt<C>

pub const exec fn universal(content: C) -> Self

returns

Self(TagFmt::SEQUENCE, content),

Ordinary universal SEQUENCE.

pub const exec fn implicit(class: Class, number: u64, content: C) -> Self

returns

Self(
    Tag {
        class,
        constructed: true,
        number: crate::asn1::tag::tag_num_from_uint(number),
    },
    content,
),

An IMPLICIT-tagged SEQUENCE.

Trait Implementations

impl<C, T> ByteLen<T> for BerSequenceFmt<C>

where T: DeepView + ?Sized, C: SpecCombinator + ByteLen<T> + Copy,

open spec fn exec_inv(&self) -> bool

{ <C as ByteLen<T>>::exec_inv(&self.1) }

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

impl<C: Clone> Clone for BerSequenceFmt<C>

exec fn clone(&self) -> cloned : Self

ensures

cloned.0 == self.0,

call_ensures(C::clone, (&self.1,), cloned.1),

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

Performs copy-assignment from source.

impl<C: SpecCombinator> Consistency for BerSequenceFmt<C>

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

{ ber_sequence_fmt(self.0, self.1).consistent(value) }

type Val = <C as SpecByteLen>::T

The type of values whose consistency is being checked.

impl<C: SpecCombinator + EquivSerializers> EquivSerializers for BerSequenceFmt<C>

open spec fn equiv_inv(&self) -> bool

{ self.1.equiv_inv() }

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

impl<C: SpecCombinator + EquivSerializers> EquivSerializersGeneral for BerSequenceFmt<C>

open spec fn equiv_general_inv(&self) -> bool

{ self.1.equiv_inv() }

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

impl<C: SpecCombinator + GoodSerializer> GoodSerializer for BerSequenceFmt<C>

open spec fn serialize_inv(&self) -> bool

{ self.1.serialize_inv() }

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

impl<Content: SpecCombinator> HasAsn1Start for BerSequenceFmt<Content>

BER SEQUENCE has one exact, necessarily constructed outer tag.

open spec fn asn1_start(&self) -> Asn1StartDomain

{
    asn1_start_exact_uint(
        self.0.class,
        self.0.constructed,
        tag_num_to_uint(self.0.number),
    )
}

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

impl<C: SpecCombinator + GoodSerializer + EquivSerializers> NonTailFmt for BerSequenceFmt<C>

open spec fn serialize_dps_inv(&self) -> bool

{
    &&& self.1.serialize_inv()
    &&& self.1.equiv_inv()

}

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

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

impl<'i, C> Parser<&'i [u8]> for BerSequenceFmt<C>

where C: SpecCombinator + Parser<&'i [u8]> + SafeParser + Copy,

open spec fn exec_inv(&self) -> bool

{
    &&& self.1.exec_inv()
    &&& self.1.safe_inv()

}

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

type PT = <C as Parser<&'i [u8]>>::PT

Executable value returned by this parser.

impl<C, T> Prepare<T> for BerSequenceFmt<C>

where T: DeepView + ?Sized, C: SpecCombinator + Prepare<T> + Copy,

open spec fn exec_inv(&self) -> bool

{ <C as Prepare<T>>::exec_inv(&self.1) }

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

impl<C: SpecCombinator + SafeParser + Productive> Productive for BerSequenceFmt<C>

open spec fn productive_inv(&self) -> bool

{ self.1.safe_inv() }

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

impl<C: Copy> Retaggable for BerSequenceFmt<C>

Supports IMPLICIT tagging of a BER SEQUENCE or EXPLICIT wrapper without losing its definite/indefinite-length framing.

Retagging replaces the tag class and number, forces the required constructed form, and preserves the schema-defined content format.

open spec fn spec_retagged(&self, tag: Tag) -> Self

{
    Self(
        Tag {
            class: tag.class,
            constructed: true,
            number: tag.number,
        },
        self.1,
    )
}

exec fn retagged(&self, tag: Tag) -> Self

impl<C> SPRoundTripDps for BerSequenceFmt<C>

where C: SpecCombinator + GoodSerializer + EquivSerializers + SPRoundTripDps,

open spec fn unambiguous(&self) -> bool

{ ber_sequence_normalized_fmt(self.0, self.1).unambiguous() }

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

impl<C: SpecCombinator + SafeParser> SafeParser for BerSequenceFmt<C>

open spec fn safe_inv(&self) -> bool

{ self.1.safe_inv() }

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

impl<Output: OutputBuf, C, T> Serializer<Output, T> for BerSequenceFmt<C>

where T: DeepView + ?Sized, C: SpecCombinator + Serializer<Output, T> + ByteLen<T> + Copy,

open spec fn exec_inv(&self) -> bool

{
    &&& <C as Serializer<Output, T>>::exec_inv(&self.1)
    &&& <C as ByteLen<T>>::exec_inv(&self.1)

}

exec fn serialize_into(&self, value: &T, obuf: &mut Output)

impl<C: SpecCombinator> SpecByteLen for BerSequenceFmt<C>

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

{ ber_sequence_fmt(self.0, self.1).byte_len(value) }

type T = <C as SpecByteLen>::T

The type of values whose byte length is being computed.

impl<C: SpecCombinator> SpecParser for BerSequenceFmt<C>

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

{ ber_sequence_fmt(self.0, self.1).spec_parse(ibuf) }

type PVal = <C as SpecByteLen>::T

The type of parsed values.

impl<C: SpecCombinator> SpecSerializer for BerSequenceFmt<C>

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

{ ber_sequence_fmt(self.0, self.1).spec_serialize(value) }

type SVal = <C as SpecByteLen>::T

The type of values to be serialized.

impl<C: SpecCombinator> SpecSerializerDps for BerSequenceFmt<C>

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

{ ber_sequence_fmt(self.0, self.1).spec_serialize_dps(value, obuf) }

type SValue = <C as SpecByteLen>::T

The type of values to be serialized.

impl<C: Copy> Copy for BerSequenceFmt<C>