Function asn1_start_ber_boundary 

pub open spec fn asn1_start_ber_boundary() -> Asn1StartDomain

{
    Asn1StartDomain {
        accepts_empty: true,
        tags: tag_lead_mask(TagFmt::EOC),
    }
}