Function generalized_time_wf 

pub open spec fn generalized_time_wf<const DER: bool>(bytes: Seq<u8>) -> bool

{
    &&& generalized_time_bytes_wf::<DER>(bytes)
    &&& generalized_time_value(bytes) matches Some(value) ==> value.wf()
    &&& generalized_time_value(bytes).is_some()
    &&& bytes.len() <= usize::MAX

}

Spec function validating full well-formedness of GeneralizedTime bytes.