Function generalized_zone_wf 

pub open spec fn generalized_zone_wf<const DER: bool>(
    bytes: Seq<u8>,
    zone_start: usize,
) -> bool

{
    if DER {
        zone_start + 1 == bytes.len() && bytes[zone_start as int] == 0x5a
    } else {
        ||| zone_start == bytes.len()
        ||| zone_start + 1 == bytes.len() && bytes[zone_start as int] == 0x5a
        ||| zone_start + 3 == bytes.len()
            && (bytes[zone_start as int] == 0x2b || bytes[zone_start as int] == 0x2d)
            && digits(bytes, zone_start as int + 1, zone_start as int + 3)
            && decimal2(bytes, (zone_start as int + 1) as usize) <= 23
        ||| zone_start + 5 == bytes.len()
            && (bytes[zone_start as int] == 0x2b || bytes[zone_start as int] == 0x2d)
            && digits(bytes, zone_start as int + 1, zone_start as int + 5)
            && decimal2(bytes, (zone_start as int + 1) as usize) <= 23
            && decimal2(bytes, (zone_start as int + 3) as usize) <= 59

    }
}

Spec function validating the timezone suffix (Zulu or UTC offset). Under DER (X.690 §11.7.1), only Zulu (‘Z’) is allowed. Under BER, UTC offsets like +hhmm, -hhmm, +hh, or -hh (omitting minutes component) are allowed.