Skip to main content

generalized_time_bytes_wf

Function generalized_time_bytes_wf 

Source
pub open spec fn generalized_time_bytes_wf<const DER: bool>(bytes: Seq<u8>) -> bool
Expand description
{
    let zone_start = generalized_zone_start(bytes);
    if DER {
        generalized_candidate_wf::<true>(bytes, 14, zone_start)
    } else {
        ||| generalized_candidate_wf::<false>(bytes, 10, zone_start)
        ||| generalized_candidate_wf::<false>(bytes, 12, zone_start)
        ||| generalized_candidate_wf::<false>(bytes, 14, zone_start)

    }
}

Spec function validating the overall structure of GeneralizedTime bytes. Under DER, it forces main_end = 14 (seconds component must always be present). Under BER, it permits main_end to be 10 (hours), 12 (minutes), or 14 (seconds).