Function der_real_decimal_at 

pub open spec fn der_real_decimal_at(bytes: Seq<u8>, dot: int) -> bool

{
    let start = decimal_mantissa_start(bytes);
    let exponent = dot + 2;
    &&& bytes.len() >= 6
    &&& bytes[0] == REAL_DECIMAL_NR3
    &&& start < dot < bytes.len()
    &&& ascii_digits(bytes, start, dot)
    &&& bytes[start] != ASCII_ZERO
    &&& bytes[dot - 1] != ASCII_ZERO
    &&& dot + 2 <= bytes.len()
    &&& bytes[dot] == ASCII_FULL_STOP
    &&& bytes[dot + 1] == ASCII_E
    &&& {
        ||| exponent + 2 == bytes.len() && bytes[exponent] == ASCII_PLUS
            && bytes[exponent + 1] == ASCII_ZERO
        ||| {
            let digits = if exponent < bytes.len() && bytes[exponent] == ASCII_MINUS {
                exponent + 1
            } else {
                exponent
            };
            &&& exponent < bytes.len()
            &&& bytes[exponent] != ASCII_PLUS
            &&& digits < bytes.len()
            &&& ASCII_ONE <= bytes[digits] <= ASCII_NINE
            &&& ascii_digits(bytes, digits, bytes.len() as int)

        }

    }

}

Canonical DER NR3 form (X.690 §11.3) at a proposed mantissa-terminating full stop.