Skip to main content

lemma_asn1_start_exact_uint

vest_lib::asn1::disjoint

Function lemma_asn1_start_exact_uint 

Source 
pub proof fn lemma_asn1_start_exact_uint(class: Class, constructed: bool, number: u64)
Expand description
ensures
asn1_start_exact(Tag {
    class,
    constructed,
    number: tag_num_from_uint(number),
}) == asn1_start_exact_uint(class, constructed, number),

Numeric and TagNumber singleton certificates denote the same identifier lead octet.