Function utc_time_lexical_wf 

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

{
    if DER {
        bytes.len() == 13 && bytes[12] == ASCII_Z && utc_time_fields_wf(bytes, true)
    } else {
        ||| bytes.len() == 11 && bytes[10] == ASCII_Z && utc_time_fields_wf(bytes, false)
        ||| bytes.len() == 13 && bytes[12] == ASCII_Z && utc_time_fields_wf(bytes, true)
        ||| bytes.len() == 15 && utc_time_fields_wf(bytes, false)
            && utc_offset_wf(bytes, 10)
        ||| bytes.len() == 17 && utc_time_fields_wf(bytes, true)
            && utc_offset_wf(bytes, 12)

    }
}

Spec function validating the lexical syntax of UTCTime bytes. Under DER (X.690 §11.8.1), the timezone offset MUST be Zulu (‘Z’). Offsets like “+hhmm” or “-hhmm” are only permitted under BER/CER.