Struct BerOctetStringFmt 

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

BER OCTET STRING with bounded recursive nesting and a configurable outer tag identity.

Use Self::universal for an ordinary OCTET STRING or Self::implicit for an IMPLICIT-tagged value. The stored tag’s constructed bit is normalized away: parsing accepts either primitive or constructed form and serialization always emits primitive definite form.

Tuple Fields

0: Tag

Implementations

impl<const LIMIT: usize> BerOctetStringFmt<LIMIT>

pub const exec fn universal() -> Self

returns

Self(TagFmt::OCTET_STRING),

Ordinary universal OCTET 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),
}),

An IMPLICIT-tagged OCTET STRING. Only the outermost tag identity is replaced.

Trait Implementations

impl<const LIMIT: usize> ByteLen<[u8]> for BerOctetStringFmt<LIMIT>

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

fn exec_inv(&self) -> bool

impl<const LIMIT: usize> ByteLen<Vec<u8>> for BerOctetStringFmt<LIMIT>

Available on crate feature alloc only.

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

fn exec_inv(&self) -> bool

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

fn clone(&self) -> BerOctetStringFmt<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 BerOctetStringFmt<LIMIT>

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

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

type Val = Seq<u8>

The type of values whose consistency is being checked.

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

proof fn lemma_serialize_equiv_on_empty(&self, value: Seq<u8>)

fn equiv_inv(&self) -> bool

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

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

fn equiv_general_inv(&self) -> bool

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

proof fn lemma_serialize_len(&self, value: Seq<u8>)

fn serialize_inv(&self) -> bool

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

Recursive BER OCTET 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 BerOctetStringFmt<LIMIT>

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

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

fn serialize_dps_inv(&self) -> bool

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

Available on crate feature alloc only.

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

type PT = Vec<u8>

Executable value returned by this parser.

fn exec_inv(&self) -> bool

impl<const LIMIT: usize> Prepare<[u8]> for BerOctetStringFmt<LIMIT>

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

fn exec_inv(&self) -> bool

impl<const LIMIT: usize> Prepare<Vec<u8>> for BerOctetStringFmt<LIMIT>

Available on crate feature alloc only.

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

fn exec_inv(&self) -> bool

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

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

fn productive_inv(&self) -> bool

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

Supports IMPLICIT tagging of recursive BER OCTET STRING values.

The stored tag is normalized to the primitive form with the replacement class and number; this is fine since the parser permits both primitive and constructed forms. Recursive fragments keep universal tag 4 (see BerOctetStringFmt).

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 BerOctetStringFmt<LIMIT>

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

fn unambiguous(&self) -> bool

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

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

fn safe_inv(&self) -> bool

impl<const LIMIT: usize, Output: OutputBuf> Serializer<Output, [u8]> for BerOctetStringFmt<LIMIT>

exec fn serialize_into(&self, value: &[u8], obuf: &mut Output)

fn exec_inv(&self) -> bool

impl<const LIMIT: usize, Output: OutputBuf> Serializer<Output, Vec<u8>> for BerOctetStringFmt<LIMIT>

Available on crate feature alloc only.

exec fn serialize_into(&self, value: &Vec<u8>, obuf: &mut Output)

fn exec_inv(&self) -> bool

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

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

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

type T = Seq<u8>

The type of values whose byte length is being computed.

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

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

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

type PVal = Seq<u8>

The type of parsed values.

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

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

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

type SVal = Seq<u8>

The type of values to be serialized.

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

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

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

type SValue = Seq<u8>

The type of values to be serialized.

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