Skip to main content

der_long_len_bytes_minimal

vest_lib::asn1::length

Function der_long_len_bytes_minimal 

Source 
pub open spec fn der_long_len_bytes_minimal(bytes: Seq<u8>) -> bool
Expand description
{
    &&& bytes.len() == 1 ==> bytes[0] > SHORT_FORM_MAX
    &&& bytes.len() > 1 ==> bytes[0] != 0x00u8

}

DER requires minimality, so

  1. for single-byte length in the long form, the value must be > 127 (i.e. not encodable in short form)
  2. for multi-byte length in the long form, the first byte must be non-zero (i.e. no leading zeros)