Struct ObjectIdentifierSpec 

pub struct ObjectIdentifierSpec {
    pub first: UInt,
    pub second: UInt,
    pub rest: Seq<UInt>,
}

Exact semantic representation of an OBJECT IDENTIFIER.

Fields

first: UInt

second: UInt

rest: Seq<UInt>

Implementations

impl ObjectIdentifierSpec

pub open spec fn wf(&self) -> bool

{
    &&& self.first <= 2
    &&& (self.first < 2 ==> self.second < 40)
    &&& (self.first == 2 ==> self.second <= UInt::MAX - 80)

}

Structural restrictions imposed by X.690 §8.19, plus the finite UInt backend bound on the combined first subidentifier.