Function ber_real_decimal_wf 

pub open spec fn ber_real_decimal_wf(bytes: Seq<u8>) -> bool

{
    &&& bytes.len() > 1
    &&& match bytes[0] {
        0x01u8 => ber_real_decimal_nr1_wf(bytes),
        0x02u8 => ber_real_decimal_nr2_wf(bytes),
        0x03u8 => ber_real_decimal_nr3_wf(bytes),
        _ => false,
    }

}

BER decimal REAL contents using an ISO 6093 NR1, NR2, or NR3 field.

X.690 §8.5.8 permits all three forms. Leading spaces and either case of the exponent mark follow ISO 6093; NR2/NR3 require an explicit decimal mark and NR3 requires a signed exponent. A decimal spelling of zero is rejected because X.690 §8.5.2 and §8.5.3 give zero dedicated encodings.