Function class_bits 

pub open spec fn class_bits(class: Class) -> u8

{
    match class {
        Class::Universal => 0b0000_0000u8,
        Class::Application => 0b0100_0000u8,
        Class::ContextSpecific => 0b1000_0000u8,
        Class::Private => 0b1100_0000u8,
    }
}