Function utc_time_bytes_wf 

pub open spec fn utc_time_bytes_wf<const DER: bool>(bytes: Seq<u8>) -> bool

{
    &&& utc_time_lexical_wf::<DER>(bytes)
    &&& utc_time_value(bytes) matches Some(value) ==> value.wf()
    &&& utc_time_value(bytes).is_some()

}

Spec function validating semantic well-formedness of parsed UTCTime bytes. Under DER (X.690 §11.8.2), the seconds element MUST always be present.