Function generalized_zone_start 

pub open spec fn generalized_zone_start(bytes: Seq<u8>) -> usize

{
    let len = bytes.len();
    if len > 0 && bytes[len - 1] == 0x5a {
        (len - 1) as usize
    } else if len >= 3 && (bytes[len - 3] == 0x2b || bytes[len - 3] == 0x2d) {
        (len - 3) as usize
    } else if len >= 5 && (bytes[len - 5] == 0x2b || bytes[len - 5] == 0x2d) {
        (len - 5) as usize
    } else {
        len as usize
    }
}

Spec function identifying the start index of the timezone suffix in GeneralizedTime bytes. The timezone suffix can be ‘Z’ (Zulu), ‘+hhmm’, ‘-hhmm’, ‘+hh’, ‘-hh’, or omitted (local time).