Struct BerBitStringFmt 

pub struct BerBitStringFmt<const LIMIT: usize>(pub Tag);

BER BIT STRING with bounded constructed nesting and a configurable outer tag identity.

Parsing accepts primitive and constructed definite/indefinite forms. Serialization always emits a primitive definite-length BER encoding.

Tuple Fields

0: Tag

Implementations

impl<const LIMIT: usize> BerBitStringFmt<LIMIT>

pub const exec fn universal() -> Self

returns

Self(TagFmt::BIT_STRING),

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

returns

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

Trait Implementations

impl<T, const LIMIT: usize> ByteLen<T> for BerBitStringFmt<LIMIT>

where T: DeepView<V = BitStringSpec> + ?Sized, ASN1Fmt<BitStringFmt<BER>, BER>: ByteLen<T>,

open spec fn exec_inv(&self) -> bool

{
    <ASN1Fmt<
        BitStringFmt<BER>,
        BER,
    > as ByteLen<T>>::exec_inv(&ber_bit_string_normalized_fmt(self.0))
}

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

impl<const LIMIT: usize> Clone for BerBitStringFmt<LIMIT>

fn clone(&self) -> BerBitStringFmt<LIMIT>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<const LIMIT: usize> Consistency for BerBitStringFmt<LIMIT>

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

{ ber_bit_string_normalized_fmt(self.0).consistent(value) }

type Val = BitStringSpec

The type of values whose consistency is being checked.

impl<const LIMIT: usize> EquivSerializers for BerBitStringFmt<LIMIT>

proof fn lemma_serialize_equiv_on_empty(&self, value: BitStringSpec)

fn equiv_inv(&self) -> bool

impl<const LIMIT: usize> EquivSerializersGeneral for BerBitStringFmt<LIMIT>

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

fn equiv_general_inv(&self) -> bool

impl<const LIMIT: usize> GoodSerializer for BerBitStringFmt<LIMIT>

proof fn lemma_serialize_len(&self, value: BitStringSpec)

fn serialize_inv(&self) -> bool

impl<const LIMIT: usize> HasAsn1Start for BerBitStringFmt<LIMIT>

Recursive BER BIT STRING accepts primitive and constructed forms of one tag identity.

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<const LIMIT: usize> NonTailFmt for BerBitStringFmt<LIMIT>

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

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

fn serialize_dps_inv(&self) -> bool

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

Available on crate feature alloc only.

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

type PT = BitStringOwned

Executable value returned by this parser.

fn exec_inv(&self) -> bool

impl<T, const LIMIT: usize> Prepare<T> for BerBitStringFmt<LIMIT>

where T: DeepView<V = BitStringSpec> + ?Sized, ASN1Fmt<BitStringFmt<BER>, BER>: Prepare<T>,

open spec fn exec_inv(&self) -> bool

{
    <ASN1Fmt<
        BitStringFmt<BER>,
        BER,
    > as Prepare<T>>::exec_inv(&ber_bit_string_normalized_fmt(self.0))
}

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

impl<const LIMIT: usize> Productive for BerBitStringFmt<LIMIT>

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

fn productive_inv(&self) -> bool

impl<const LIMIT: usize> Retaggable for BerBitStringFmt<LIMIT>

Supports IMPLICIT tagging of recursive BER BIT STRING values.

The outer identity is replaced and normalized to primitive form; parsing still accepts both primitive and constructed forms, while nested fragments retain universal tag 3.

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

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

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

impl<const LIMIT: usize> SPRoundTripDps for BerBitStringFmt<LIMIT>

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

fn unambiguous(&self) -> bool

impl<const LIMIT: usize> SafeParser for BerBitStringFmt<LIMIT>

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

fn safe_inv(&self) -> bool

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

where Output: OutputBuf, T: DeepView<V = BitStringSpec> + ?Sized, ASN1Fmt<BitStringFmt<BER>, BER>: Serializer<Output, T>,

open spec fn exec_inv(&self) -> bool

{
    <ASN1Fmt<
        BitStringFmt<BER>,
        BER,
    > as Serializer<Output, T>>::exec_inv(&ber_bit_string_normalized_fmt(self.0))
}

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

impl<const LIMIT: usize> SpecByteLen for BerBitStringFmt<LIMIT>

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

{ ber_bit_string_normalized_fmt(self.0).byte_len(value) }

type T = BitStringSpec

The type of values whose byte length is being computed.

impl<const LIMIT: usize> SpecParser for BerBitStringFmt<LIMIT>

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

{ FixWith::<LIMIT, _, _>(BerBitStringRecBody, self.0).spec_parse(ibuf) }

type PVal = BitStringSpec

The type of parsed values.

impl<const LIMIT: usize> SpecSerializer for BerBitStringFmt<LIMIT>

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

{ ber_bit_string_normalized_fmt(self.0).spec_serialize(value) }

type SVal = BitStringSpec

The type of values to be serialized.

impl<const LIMIT: usize> SpecSerializerDps for BerBitStringFmt<LIMIT>

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

{ ber_bit_string_normalized_fmt(self.0).spec_serialize_dps(value, obuf) }

type SValue = BitStringSpec

The type of values to be serialized.

impl<const LIMIT: usize> Copy for BerBitStringFmt<LIMIT>