Struct ObjectIdentifier 

pub struct ObjectIdentifier { /* private fields */ }

Executable OBJECT IDENTIFIER value.

Keeping the first two arcs separate avoids a second allocation when parsing: the remaining subidentifiers are already produced as one Vec by RepeatTillEnd.

Implementations

impl ObjectIdentifier

pub exec fn new(first: UInt, second: UInt, rest: Vec<UInt>) -> Self

pub exec fn first(&self) -> first : UInt

ensures

first == self.deep_view().first,

pub exec fn second(&self) -> second : UInt

ensures

second == self.deep_view().second,

pub exec fn rest(&self) -> &[UInt]

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 DeepView for ObjectIdentifier

Available on crate feature alloc only.

closed spec fn deep_view(&self) -> Self::V

type V = ObjectIdentifierSpec

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