Function generalized_fraction_wf 

pub open spec fn generalized_fraction_wf<const DER: bool>(
    bytes: Seq<u8>,
    main_end: usize,
    zone_start: usize,
) -> bool

{
    if zone_start == main_end {
        true
    } else {
        &&& main_end + 1 < zone_start
        &&& (bytes[main_end as int] == 0x2e || (!DER && bytes[main_end as int] == 0x2c))
        &&& digits(bytes, main_end as int + 1, zone_start as int)
        &&& (!DER || bytes[zone_start as int - 1] != 0x30)

    }
}

Spec function validating the optional fractional-seconds element of GeneralizedTime. Under BER (X.680 46.3.a.2), either a comma (0x2c) or a full stop (0x2e) is allowed as the decimal separator. Under DER (X.690 §11.7.3–11.7.4):

• The decimal separator MUST be a full stop (0x2e / ‘.’).
• Trailing zeros are forbidden in the fractional part (i.e. cannot end with ASCII ‘0’).