Function generalized_fields_wf 

pub open spec fn generalized_fields_wf(bytes: Seq<u8>, main_end: usize) -> bool

{
    &&& (main_end == 10 || main_end == 12 || main_end == 14)
    &&& digits(bytes, 0, main_end as int)
    &&& datetime_wf(DateTime {
        year: decimal4(bytes, 0),
        month: decimal2(bytes, 4),
        day: decimal2(bytes, 6),
        hour: decimal2(bytes, 8),
        minute: if main_end >= 12 { decimal2(bytes, 10) } else { 0 },
        second: if main_end == 14 { decimal2(bytes, 12) } else { 0 },
    })

}

Helper spec function to validate the prefix date-time fields (YYYYMMDDhh[mm[ss]]).