Function utc_time_bytes 

pub open spec fn utc_time_bytes(value: UtcTime) -> Seq<u8>

{
    let year = (value.datetime.year as int % 100) as u8;
    decimal2_bytes(year)@ + decimal2_bytes(value.datetime.month)@
        + decimal2_bytes(value.datetime.day)@ + decimal2_bytes(value.datetime.hour)@
        + decimal2_bytes(value.datetime.minute)@
        + if value.precision == TimePrecision::Second {
            decimal2_bytes(value.datetime.second)@ + seq![ASCII_Z]
        } else {
            seq![ASCII_Z]
        }
}

Spec function mapping UtcTime to serialized UTCTime bytes (YYMMDDhhmmssZ or YYMMDDhhmmZ).