Skip to main content

lemma_ber_real_bytes_cases

vest_lib::asn1::real

Function lemma_ber_real_bytes_cases 

Source 
pub proof fn lemma_ber_real_bytes_cases(bytes: Seq<u8>)
Expand description
ensures
bytes.len() == 0 ==> ber_real_bytes_wf(bytes),
bytes.len() == 1 ==> (ber_real_bytes_wf(bytes) <==> der_real_special_wf(bytes)),
bytes.len() > 1 && bytes[0] & 0x80u8 != 0
    ==> (ber_real_bytes_wf(bytes) <==> ber_real_binary_wf(bytes)),
bytes.len() > 1 && bytes[0] & 0x80u8 == 0
    ==> (ber_real_bytes_wf(bytes) <==> ber_real_decimal_wf(bytes)),