Function asn1_start_exact_uint 

pub open spec fn asn1_start_exact_uint(
    class: Class,
    constructed: bool,
    number: u64,
) -> Asn1StartDomain

{
    let low = if number < 31u64 { number } else { 31u64 };
    let index = if constructed { low | 32u64 } else { low };
    let bit = 1u64 << index;
    Asn1StartDomain {
        accepts_empty: false,
        tags: match class {
            Class::Universal => {
                Asn1TagLeadMask {
                    universal: bit,
                    application: 0,
                    context_specific: 0,
                    private: 0,
                }
            }
            Class::Application => {
                Asn1TagLeadMask {
                    universal: 0,
                    application: bit,
                    context_specific: 0,
                    private: 0,
                }
            }
            Class::ContextSpecific => {
                Asn1TagLeadMask {
                    universal: 0,
                    application: 0,
                    context_specific: bit,
                    private: 0,
                }
            }
            Class::Private => {
                Asn1TagLeadMask {
                    universal: 0,
                    application: 0,
                    context_specific: 0,
                    private: bit,
                }
            }
        },
    }
}

FIRST certificate for a tag whose number is kept in its numeric representation.

Generated nominal formats store their retaggable tag as (Class, u64). Keeping their public certificate in that same representation avoids repeatedly normalizing through the TagNumber enum merely to select one bitmap bit.