Skip to main content

lemma_der_real_bytes_cases

vest_lib::asn1::real

Function lemma_der_real_bytes_cases 

Source 
pub proof fn lemma_der_real_bytes_cases(bytes: Seq<u8>)
Expand description
ensures
bytes.len() == 0 ==> der_real_bytes_wf(bytes),
bytes.len() == 1 ==> (der_real_bytes_wf(bytes) <==> der_real_special_wf(bytes)),
bytes.len() > 1 && bytes[0] & 0x80u8 != 0
    ==> (der_real_bytes_wf(bytes) <==> der_real_binary_wf(bytes)),
bytes.len() > 1 && bytes[0] & 0x80u8 == 0 && bytes[0] == REAL_DECIMAL_NR3
    ==> (der_real_bytes_wf(bytes) <==> der_real_decimal_wf(bytes)),
bytes.len() > 1 && bytes[0] & 0x80u8 == 0 && bytes[0] != REAL_DECIMAL_NR3
    ==> !der_real_bytes_wf(bytes),