Struct BerCharStringFmt 

pub struct BerCharStringFmt<C, const LIMIT: usize>(pub Tag, pub C);

BER restricted character string represented as an IMPLICITly tagged BER OCTET STRING.

Parsing accepts primitive, definite constructed, indefinite constructed, and nested forms. Only the outermost tag is configurable; recursive components retain the universal OCTET STRING tag. Serialization is normalized to primitive definite form.

Tuple Fields

0: Tag

1: C

Implementations

impl<C: Copy, const LIMIT: usize> BerCharStringFmt<C, LIMIT>

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

returns

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

impl<const LIMIT: usize> BerCharStringFmt<Utf8StringFmt, LIMIT>

pub const exec fn universal() -> Self

returns

Self(TagFmt::UTF8_STRING, Utf8StringFmt),

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

returns

Self::with_implicit_tag(Utf8StringFmt, class, number),

impl<const LIMIT: usize> BerCharStringFmt<PrintableStringFmt, LIMIT>

pub const exec fn universal() -> Self

returns

Self(TagFmt::PRINTABLE_STRING, PrintableStringFmt),

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

returns

Self::with_implicit_tag(PrintableStringFmt, class, number),

impl<const LIMIT: usize> BerCharStringFmt<Ia5StringFmt, LIMIT>

pub const exec fn universal() -> Self

returns

Self(TagFmt::IA5_STRING, Ia5StringFmt),

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

returns

Self::with_implicit_tag(Ia5StringFmt, class, number),

impl<const LIMIT: usize> BerCharStringFmt<TeletexStringFmt, LIMIT>

pub const exec fn universal() -> Self

returns

Self(TagFmt::TELETEX_STRING, TeletexStringFmt),

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

returns

Self::with_implicit_tag(TeletexStringFmt, class, number),

impl<const LIMIT: usize> BerCharStringFmt<BmpStringFmt, LIMIT>

pub const exec fn universal() -> Self

returns

Self(TagFmt::BMP_STRING, BmpStringFmt),

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

returns

Self::with_implicit_tag(BmpStringFmt, class, number),

impl<const LIMIT: usize> BerCharStringFmt<Refined<PrintableStringFmt, NumericStringChars>, LIMIT>

pub const exec fn universal() -> Self

returns

Self(TagFmt::NUMERIC_STRING, NumericStringFmt),

impl<const LIMIT: usize> BerCharStringFmt<UniversalStringFmt, LIMIT>

pub const exec fn universal() -> Self

returns

Self(TagFmt::UNIVERSAL_STRING, UniversalStringFmt),

Trait Implementations

impl<C, T, const LIMIT: usize> ByteLen<T> for BerCharStringFmt<C, LIMIT>

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

open spec fn exec_inv(&self) -> bool

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

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

impl<C: Clone, const LIMIT: usize> Clone for BerCharStringFmt<C, LIMIT>

fn clone(&self) -> BerCharStringFmt<C, LIMIT>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<C: SpecCombinator, const LIMIT: usize> Consistency for BerCharStringFmt<C, LIMIT>

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

{
    &&& self.1.consistent(value)
    &&& ber_char_string_fmt::<C, LIMIT>(self.0, self.1).consistent(value)

}

type Val = <C as SpecByteLen>::T

The type of values whose consistency is being checked.

impl<C: SpecCombinator, const LIMIT: usize> EquivSerializers for BerCharStringFmt<C, LIMIT>

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

fn equiv_inv(&self) -> bool

impl<C: SpecCombinator, const LIMIT: usize> EquivSerializersGeneral for BerCharStringFmt<C, LIMIT>

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

fn equiv_general_inv(&self) -> bool

impl<C: SpecCombinator, const LIMIT: usize> GoodSerializer for BerCharStringFmt<C, LIMIT>

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

fn serialize_inv(&self) -> bool

impl<Content: SpecCombinator, const LIMIT: usize> HasAsn1Start for BerCharStringFmt<Content, LIMIT>

BER restricted character strings inherit the primitive/constructed identity of their underlying recursive OCTET STRING.

open spec fn asn1_start(&self) -> Asn1StartDomain

{ asn1_start_identity_uint(self.0.class, tag_num_to_uint(self.0.number)) }

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

impl<C: SpecCombinator, const LIMIT: usize> NonTailFmt for BerCharStringFmt<C, LIMIT>

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>)

fn serialize_dps_inv(&self) -> bool

impl<'i, C, const LIMIT: usize> Parser<&'i [u8]> for BerCharStringFmt<C, LIMIT>

where C: BerDecoderOwned,

Available on crate feature alloc only.

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

type PT = <C as BerDecoderOwned>::Owned

Executable value returned by this parser.

fn exec_inv(&self) -> bool

impl<C, T, const LIMIT: usize> Prepare<T> for BerCharStringFmt<C, LIMIT>

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

open spec fn exec_inv(&self) -> bool

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

}

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

impl<C: SpecCombinator, const LIMIT: usize> Productive for BerCharStringFmt<C, LIMIT>

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

fn productive_inv(&self) -> bool

impl<C: Copy, const LIMIT: usize> Retaggable for BerCharStringFmt<C, LIMIT>

Supports IMPLICIT tagging of a BER restricted character string layered over OCTET STRING.

The outer tag is normalized to the primitive form with the replacement class and number, while OCTET STRING fragment tags, the character-content format, and the recursion limit are preserved.

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

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

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

impl<C: SpecCombinator + SPRoundTrip, const LIMIT: usize> SPRoundTripDps for BerCharStringFmt<C, LIMIT>

open spec fn unambiguous(&self) -> bool

{ self.1.sp_roundtrip_inv() }

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

impl<C: SpecCombinator, const LIMIT: usize> SafeParser for BerCharStringFmt<C, LIMIT>

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

fn safe_inv(&self) -> bool

impl<Output, C, T, const LIMIT: usize> Serializer<Output, T> for BerCharStringFmt<C, LIMIT>

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

open spec fn exec_inv(&self) -> bool

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

}

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

impl<C: SpecCombinator, const LIMIT: usize> SpecByteLen for BerCharStringFmt<C, LIMIT>

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

{ ber_char_string_fmt::<C, LIMIT>(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, const LIMIT: usize> SpecParser for BerCharStringFmt<C, LIMIT>

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

{ ber_char_string_fmt::<C, LIMIT>(self.0, self.1).spec_parse(ibuf) }

type PVal = <C as SpecByteLen>::T

The type of parsed values.

impl<C: SpecCombinator, const LIMIT: usize> SpecSerializer for BerCharStringFmt<C, LIMIT>

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

{ ber_char_string_fmt::<C, LIMIT>(self.0, self.1).spec_serialize(value) }

type SVal = <C as SpecByteLen>::T

The type of values to be serialized.

impl<C: SpecCombinator, const LIMIT: usize> SpecSerializerDps for BerCharStringFmt<C, LIMIT>

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

{ ber_char_string_fmt::<C, LIMIT>(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, const LIMIT: usize> Copy for BerCharStringFmt<C, LIMIT>