Function ber_real_binary_wf 

pub open spec fn ber_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 != 0x30u8
        &&& (form == 0x03u8
            ==> {
                &&& exponent_len > 0
                &&& der_real_exponent_minimal(bytes, exponent_offset, exponent_len)

            })
        &&& mantissa_offset < bytes.len()
        &&& exists |i: int| mantissa_offset <= i < bytes.len() && bytes[i] != 0u8

    }
}

BER binary REAL contents as specified by X.690 §8.5.7.