Function asn1_start_mask 

pub open spec fn asn1_start_mask(
    accepts_empty: bool,
    universal: u64,
    application: u64,
    context_specific: u64,
    private: u64,
) -> Asn1StartDomain

{
    Asn1StartDomain {
        accepts_empty,
        tags: Asn1TagLeadMask {
            universal,
            application,
            context_specific,
            private,
        },
    }
}

Construct a canonical, fixed-size ASN.1 FIRST certificate from its four bitmap words.