Struct GeneralizedTimeSpec 

pub struct GeneralizedTimeSpec {
    pub datetime: DateTime,
    pub precision: TimePrecision,
    pub fraction: Seq<u8>,
    pub zone: TimeZone,
}

Logical specification of an ASN.1 GeneralizedTime value (X.680 clause 46). Consists of a calendar date (YYYYMMDD), local time of day, optional fractional seconds, and a timezone offset or Zulu UTC indicator.

Fields

datetime: DateTime

precision: TimePrecision

fraction: Seq<u8>

zone: TimeZone

Implementations

impl GeneralizedTimeSpec

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

{
    &&& datetime_wf(self.datetime)
    &&& self.datetime.year <= 9999
    &&& digits(self.fraction, 0, self.fraction.len() as int)
    &&& (self.precision == TimePrecision::Hour || self.precision == TimePrecision::Minute
        || self.precision == TimePrecision::Second)
    &&& (self.precision != TimePrecision::Hour
        || (self.datetime.minute == 0 && self.datetime.second == 0))
    &&& (self.precision != TimePrecision::Minute || self.datetime.second == 0)

}

Validates semantic well-formedness of the GeneralizedTime value. Year must be represented using 4 digits (up to 9999).

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

{
    &&& self.wf()
    &&& self.zone == TimeZone::Utc
    &&& self.precision == TimePrecision::Second
    &&& (self.fraction.len() == 0 || self.fraction.last() != 0x30)

}

Validates DER-specific restrictions for GeneralizedTime (X.690 §11.7):

• The encoding MUST terminate with ‘Z’ (meaning UTC only).
• The seconds element MUST always be present.
• Fractional seconds, if present, MUST omit all trailing zeros (and cannot end in ‘0’).