Skip to main content

tag_number_wf

vest_lib::asn1::tag

Function tag_number_wf 

Source 
pub open spec fn tag_number_wf(num: TagNumber) -> bool
Expand description
{
    num matches TagNumber::Other {
        tag_num,
    } ==> {
        &&& !matches!(
            tag_num, 0 | 1 | 2 | 3 | 4 | 5 | 6 | 9 | 10 | 12 | 13 | 16 | 17 | 18 | 19 |
            20 | 21 | 22 | 23 | 24 | 26 | 27 | 28 | 30
        )
        &&& nat_to_base128(tag_num as nat).len() <= BASE128_MAX_BYTES

    }
}