Function utc_time_value 

pub open spec fn utc_time_value(bytes: Seq<u8>) -> Option<UtcTime>

{
    let has_seconds = bytes.len() == 13 || bytes.len() == 17;
    let local = DateTime {
        year: utc_year(decimal2(bytes, 0)),
        month: decimal2(bytes, 2),
        day: decimal2(bytes, 4),
        hour: decimal2(bytes, 6),
        minute: decimal2(bytes, 8),
        second: if has_seconds { decimal2(bytes, 10) } else { 0 },
    };
    let precision = if has_seconds {
        TimePrecision::Second
    } else {
        TimePrecision::Minute
    };
    if bytes.len() == 11 || bytes.len() == 13 {
        Some(UtcTime {
            datetime: local,
            precision,
        })
    } else {
        let pos: usize = if has_seconds { 12 } else { 10 };
        match normalize_offset(
            local,
            bytes[pos as int] == ASCII_PLUS,
            decimal2(bytes, (pos as int + 1) as usize),
            decimal2(bytes, (pos as int + 3) as usize),
        ) {
            Some(datetime) => Some(UtcTime { datetime, precision }),
            None => None,
        }
    }
}

Spec function parsing the UTCTime bytes into a structured UtcTime. Properly normalizes the timezone offset (UTC = local - offset) if present.