Struct ObjectIdentifierFmt 

pub struct ObjectIdentifierFmt;

ASN.1 OBJECT IDENTIFIER contents format.

Trait Implementations

impl ByteLen<ObjectIdentifier> for ObjectIdentifierFmt

Available on crate feature alloc only.

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

fn exec_inv(&self) -> bool

impl Clone for ObjectIdentifierFmt

fn clone(&self) -> ObjectIdentifierFmt

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Consistency for ObjectIdentifierFmt

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

{ v.wf() && object_identifier_inner().consistent(oid_to_subidentifiers(v)) }

type Val = ObjectIdentifierSpec

The type of values whose consistency is being checked.

impl DerOrd<ObjectIdentifier> for ObjectIdentifierFmt

Available on crate feature alloc only.

proof fn lemma_der_serialize_len(&self, value: ObjectIdentifierSpec)

open spec fn der_remaining( &self, value: ObjectIdentifierSpec, state: ObjectIdentifierDerState, ) -> Seq<u8>

{
    if state.in_left {
        Base128Fmt::<true>
            .der_remaining(crate::asn1::oid::oid_first_subidentifier(value), state.left)
            + RepeatTillEnd(Base128Fmt::<true>).der_remaining(value.rest, state.right)
    } else {
        RepeatTillEnd(Base128Fmt::<true>).der_remaining(value.rest, state.right)
    }
}

open spec fn der_state_valid( &self, value: ObjectIdentifierSpec, state: ObjectIdentifierDerState, ) -> bool

{
    &&& Base128Fmt::<true>
        .der_state_valid(crate::asn1::oid::oid_first_subidentifier(value), state.left)
    &&& RepeatTillEnd(Base128Fmt::<true>).der_state_valid(value.rest, state.right)
    &&& !state.in_left
        ==> Base128Fmt::<true>
            .der_remaining(crate::asn1::oid::oid_first_subidentifier(value), state.left)
            .len() == 0

}

exec fn der_start(&self, o: &ObjectIdentifier) -> state : ObjectIdentifierDerState

exec fn der_next( &self, o: &ObjectIdentifier, state: &mut ObjectIdentifierDerState, ) -> next : Option<u8>

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

impl DerState for ObjectIdentifierFmt

Available on crate feature alloc only.

type State = PairDerState<Base128DerState, StarDerState<Base128DerState>>

impl EquivSerializers for ObjectIdentifierFmt

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

fn equiv_inv(&self) -> bool

impl GoodSerializer for ObjectIdentifierFmt

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

fn serialize_inv(&self) -> bool

impl NonMalleable for ObjectIdentifierFmt

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

fn nonmal_inv(&self) -> bool

impl Parser<&[u8]> for ObjectIdentifierFmt

Available on crate feature alloc only.

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

type PT = ObjectIdentifier

Executable value returned by this parser.

fn exec_inv(&self) -> bool

impl Prepare<ObjectIdentifier> for ObjectIdentifierFmt

Available on crate feature alloc only.

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

fn exec_inv(&self) -> bool

impl Productive for ObjectIdentifierFmt

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

fn productive_inv(&self) -> bool

impl SPRoundTripDps for ObjectIdentifierFmt

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

fn unambiguous(&self) -> bool

impl SafeParser for ObjectIdentifierFmt

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

fn safe_inv(&self) -> bool

impl<Output: OutputBuf> Serializer<Output, ObjectIdentifier> for ObjectIdentifierFmt

Available on crate feature alloc only.

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

fn exec_inv(&self) -> bool

impl SoundParser for ObjectIdentifierFmt

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 ObjectIdentifierFmt

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

{ object_identifier_inner().byte_len(oid_to_subidentifiers(v)) }

type T = ObjectIdentifierSpec

The type of values whose byte length is being computed.

impl SpecParser for ObjectIdentifierFmt

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

{
    match object_identifier_inner().spec_parse(ibuf) {
        Some((n, (first, rest))) => Some((n, oid_from_subidentifiers(first, rest))),
        None => None,
    }
}

type PVal = ObjectIdentifierSpec

The type of parsed values.

impl SpecSerializer for ObjectIdentifierFmt

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

{ object_identifier_inner().spec_serialize(oid_to_subidentifiers(v)) }

type SVal = ObjectIdentifierSpec

The type of values to be serialized.

impl SpecSerializerDps for ObjectIdentifierFmt

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

{ object_identifier_inner().spec_serialize_dps(oid_to_subidentifiers(v), obuf) }

type SValue = ObjectIdentifierSpec

The type of values to be serialized.

impl Copy for ObjectIdentifierFmt