Struct UtcTime 

pub struct UtcTime {
    pub datetime: DateTime,
    pub precision: TimePrecision,
}

Represents a parsed ASN.1 UTCTime value (X.680 clause 47). UTCTime consists of a calendar date (YYMMDD), time to a precision of minutes or seconds, and an optional local time differential from UTC.

Fields

datetime: DateTime

precision: TimePrecision

Implementations

impl UtcTime

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

{
    &&& datetime_wf(self.datetime)
    &&& 1950 <= self.datetime.year <= 2049
    &&& (self.precision == TimePrecision::Minute
        || self.precision == TimePrecision::Second)
    &&& (self.precision == TimePrecision::Second || self.datetime.second == 0)

}

Validates semantic well-formedness of the UTCTime value. Under X.680 clause 47.3, year is limited to the range 1950 to 2049.

Trait Implementations

impl<const DER: bool> ByteLen<UtcTime> for UtcTimeFmt<DER>

exec fn length(&self, value: &UtcTime) -> usize

fn exec_inv(&self) -> bool

impl Clone for UtcTime

fn clone(&self) -> UtcTime

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for UtcTime

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl DeepView for UtcTime

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

type V = UtcTime

impl DeepViewIdentity for UtcTime

proof fn lemma_deep_view_identity(&self)

impl DerOrd<UtcTime> for UtcTimeFmt<true>

proof fn lemma_der_serialize_len(&self, value: UtcTime)

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

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

open spec fn der_state_valid(&self, value: UtcTime, state: UtcTimeDerState) -> bool

{
    &&& state.pos <= 13
    &&& state.bytes@ == self.spec_serialize(value)

}

exec fn der_start(&self, t: &UtcTime) -> state : UtcTimeDerState

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

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

impl PartialEq for UtcTime

fn eq(&self, other: &UtcTime) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl PartialEqSpecImpl for UtcTime

fn obeys_eq_spec() -> bool

fn eq_spec(&self, other: &Self) -> bool

impl<const DER: bool> Prepare<UtcTime> for UtcTimeFmt<DER>

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

fn exec_inv(&self) -> bool

impl<Output: OutputBuf, const DER: bool> Serializer<Output, UtcTime> for UtcTimeFmt<DER>

exec fn serialize_into(&self, value: &UtcTime, obuf: &mut Output)

fn exec_inv(&self) -> bool

impl Copy for UtcTime

impl Eq for UtcTime

impl Structural for UtcTime

impl StructuralPartialEq for UtcTime