Struct BerSequenceOfFmt 

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

BER SEQUENCE OF codec with a configurable outer tag.

Parsing accepts either a definite-length contents or an indefinite-length sequence terminated by EOC. Each element must be a productive, complete ASN.1 TLV; in particular, its parser must not accept EOC as an element. Serialization always emits definite-length BER.

Tuple Fields

0: Tag

1: C

Implementations

impl<C: Copy> BerSequenceOfFmt<C>

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

returns

Self(TagFmt::SEQUENCE, content),

Ordinary universal SEQUENCE OF.

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 OF.

Trait Implementations

impl<C, T> ByteLen<&[T]> for BerSequenceOfFmt<C>

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

open spec fn exec_inv(&self) -> bool

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

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

impl<C, T> ByteLen<Vec<T>> for BerSequenceOfFmt<C>

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

Available on crate feature alloc only.

open spec fn exec_inv(&self) -> bool

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

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

impl<C: Clone> Clone for BerSequenceOfFmt<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 BerSequenceOfFmt<C>

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

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

type Val = Seq<<C as SpecByteLen>::T>

The type of values whose consistency is being checked.

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

open spec fn equiv_inv(&self) -> bool

{ self.1.equiv_general_inv() }

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

impl<C: SpecCombinator + EquivSerializersGeneral> EquivSerializersGeneral for BerSequenceOfFmt<C>

open spec fn equiv_general_inv(&self) -> bool

{ self.1.equiv_general_inv() }

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

impl<C: SpecCombinator + GoodSerializer> GoodSerializer for BerSequenceOfFmt<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 BerSequenceOfFmt<Content>

BER SEQUENCE OF 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 + EquivSerializersGeneral> NonTailFmt for BerSequenceOfFmt<C>

open spec fn serialize_dps_inv(&self) -> bool

{
    &&& self.1.serialize_inv()
    &&& self.1.equiv_general_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 BerSequenceOfFmt<C>

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

Available on crate feature alloc only.

open spec fn exec_inv(&self) -> bool

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

}

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

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

Executable value returned by this parser.

impl<C, T> Prepare<&[T]> for BerSequenceOfFmt<C>

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

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, T> Prepare<Vec<T>> for BerSequenceOfFmt<C>

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

Available on crate feature alloc only.

open spec fn exec_inv(&self) -> bool

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

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

impl<C: SpecCombinator + SafeParser> Productive for BerSequenceOfFmt<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 BerSequenceOfFmt<C>

Supports IMPLICIT tagging of a BER SEQUENCE OF/SET OF while retaining its specialized definite/indefinite-length handling.

Retagging replaces the tag class and number, forces the required constructed form, and preserves the element 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 BerSequenceOfFmt<C>

where C: SpecCombinator + Productive + GoodSerializer + NonTailFmt + SPRoundTripDps + EquivSerializersGeneral,

open spec fn unambiguous(&self) -> bool

{
    &&& RepeatTillEnd(self.1).sp_roundtrip_inv()
    &&& disjoint_domains(self.1, EOC)

}

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

impl<C: SpecCombinator + SafeParser> SafeParser for BerSequenceOfFmt<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 BerSequenceOfFmt<C>

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

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<Output: OutputBuf, C, T> Serializer<Output, Vec<T>> for BerSequenceOfFmt<C>

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

Available on crate feature alloc only.

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: &Vec<T>, obuf: &mut Output)

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

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

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

type T = Seq<<C as SpecByteLen>::T>

The type of values whose byte length is being computed.

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

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

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

type PVal = Seq<<C as SpecByteLen>::T>

The type of parsed values.

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

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

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

type SVal = Seq<<C as SpecByteLen>::T>

The type of values to be serialized.

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

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

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

type SValue = Seq<<C as SpecByteLen>::T>

The type of values to be serialized.

impl<C: Copy> Copy for BerSequenceOfFmt<C>