Function utc_time_fields_wf 

pub open spec fn utc_time_fields_wf(bytes: Seq<u8>, has_seconds: bool) -> bool

{
    let second_end = if has_seconds { 12 } else { 10 };
    &&& digits(bytes, 0, second_end)
    &&& datetime_wf(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 },
    })

}

Helper spec function to validate the date and time digit fields of a UTCTime string (YYMMDDhhmm[ss]).