Struct TagFmt 

pub struct TagFmt;

ASN.1 tag format combinator.

Only the canonical DER form is accepted:

• Tag numbers 0–30 must use the short (1-byte) form.
• High tag numbers must have no leading zero in the base-128 encoding.

Implementations

impl TagFmt

pub const EOC: Tag

pub const BOOLEAN: Tag

pub const INTEGER: Tag

pub const NULL: Tag

pub const OBJECT_IDENTIFIER: Tag

pub const REAL: Tag

pub const ENUMERATED: Tag

pub const RELATIVE_OID: Tag

pub const BIT_STRING: Tag

pub const OCTET_STRING: Tag

pub const UTF8_STRING: Tag

pub const NUMERIC_STRING: Tag

pub const PRINTABLE_STRING: Tag

pub const TELETEX_STRING: Tag

pub const VIDEOTEX_STRING: Tag

pub const IA5_STRING: Tag

pub const UTC_TIME: Tag

pub const GENERALIZED_TIME: Tag

pub const VISIBLE_STRING: Tag

pub const GENERAL_STRING: Tag

pub const UNIVERSAL_STRING: Tag

pub const BMP_STRING: Tag

pub const BIT_STRING_CONSTRUCTED: Tag

pub const OCTET_STRING_CONSTRUCTED: Tag

pub const UTF8_STRING_CONSTRUCTED: Tag

pub const NUMERIC_STRING_CONSTRUCTED: Tag

pub const PRINTABLE_STRING_CONSTRUCTED: Tag

pub const TELETEX_STRING_CONSTRUCTED: Tag

pub const VIDEOTEX_STRING_CONSTRUCTED: Tag

pub const IA5_STRING_CONSTRUCTED: Tag

pub const UTC_TIME_CONSTRUCTED: Tag

pub const GENERALIZED_TIME_CONSTRUCTED: Tag

pub const VISIBLE_STRING_CONSTRUCTED: Tag

pub const GENERAL_STRING_CONSTRUCTED: Tag

pub const UNIVERSAL_STRING_CONSTRUCTED: Tag

pub const BMP_STRING_CONSTRUCTED: Tag

pub const SEQUENCE: Tag

pub const SET: Tag

Trait Implementations

impl ByteLen<Tag> for TagFmt

exec fn length(&self, v: &Tag) -> usize

fn exec_inv(&self) -> bool

impl Clone for TagFmt

fn clone(&self) -> TagFmt

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Consistency for TagFmt

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

type Val = Tag

The type of values whose consistency is being checked.

impl DerOrd<Tag> for TagFmt

proof fn lemma_der_serialize_len(&self, tag: Tag)

open spec fn der_remaining(&self, tag: Tag, state: TagDerState) -> Seq<u8>

{ self.spec_serialize(tag).skip(state.pos as int) }

open spec fn der_state_valid(&self, tag: Tag, state: TagDerState) -> bool

{
    &&& state.pos <= state.len
    &&& state.len <= state.bytes@.len()
    &&& state.len == self.spec_serialize(tag).len()
    &&& state.bytes@.take(state.len as int) == self.spec_serialize(tag)

}

exec fn der_start(&self, t: &Tag) -> state : TagDerState

exec fn der_next(&self, t: &Tag, state: &mut TagDerState) -> next : Option<u8>

fn der_leq(&self, left: &T, right: &T) -> bool

impl DerState for TagFmt

type State = TagDerState

impl EquivSerializers for TagFmt

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

fn equiv_inv(&self) -> bool

impl EquivSerializersGeneral for TagFmt

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

fn equiv_general_inv(&self) -> bool

impl GoodSerializer for TagFmt

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

fn serialize_inv(&self) -> bool

impl NoLookAhead for TagFmt

proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>)

fn no_lookahead_inv(&self) -> bool

fn corollary_non_extensible(&self, i1: Seq<u8>, i2: Seq<u8>)

impl NonMalleable for TagFmt

proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>)

fn nonmal_inv(&self) -> bool

impl NonTailFmt for TagFmt

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

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

fn serialize_dps_inv(&self) -> bool

impl Parser<&[u8]> for TagFmt

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

type PT = Tag

Executable value returned by this parser.

fn exec_inv(&self) -> bool

impl Prepare<Tag> for TagFmt

exec fn prepare(&self, v: &Tag) -> Result<usize, PreSerializeError>

fn exec_inv(&self) -> bool

impl Productive for TagFmt

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

fn productive_inv(&self) -> bool

impl SPRoundTripDps for TagFmt

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

fn unambiguous(&self) -> bool

impl SafeParser for TagFmt

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

fn safe_inv(&self) -> bool

impl<Output: OutputBuf> Serializer<Output, Tag> for TagFmt

exec fn serialize_into(&self, v: &Tag, obuf: &mut Output)

fn exec_inv(&self) -> bool

impl SoundParser for TagFmt

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

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

fn sound_inv(&self) -> bool

impl SpecByteLen for TagFmt

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

type T = Tag

The type of values whose byte length is being computed.

impl SpecParser for TagFmt

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

type PVal = Tag

The type of parsed values.

impl SpecSerializer for TagFmt

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

type SVal = Tag

The type of values to be serialized.

impl SpecSerializerDps for TagFmt

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

type SValue = Tag

The type of values to be serialized.

impl Copy for TagFmt