Function der_real_binary_wf 

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

{
    if bytes.len() < 3 {
        false
    } else {
        let info = bytes[0];
        let form = info & 0x03u8;
        let exponent_offset: int = if form == 0x03u8 { 2 } else { 1 };
        let exponent_len: int = match form {
            0x00u8 => 1,
            0x01u8 => 2,
            0x02u8 => 3,
            _ => bytes[1] as int,
        };
        let mantissa_offset = exponent_offset + exponent_len;
        &&& info & 0x80u8 != 0
        &&& info & 0x30u8 == 0
        &&& info & 0x0cu8 == 0
        &&& (form == 0x03u8 ==> exponent_len >= 4)
        &&& der_real_exponent_minimal(bytes, exponent_offset, exponent_len)
        &&& mantissa_offset < bytes.len()
        &&& bytes[mantissa_offset] != 0
        &&& bytes.last() & 1u8 == 1u8

    }
}

Canonical DER binary REAL contents.