Macro bitflags 

macro_rules! bitflags {
    (
        $(#[$outer:meta])*
        $vis:vis struct $name:ident: $T:ty {
            $(
                $(#[$inner:ident $($args:tt)*])*
                const $Flag:ident = $value:literal;
            )*
        }

        $($t:tt)*
    ) => { ... };
}

A macro wrapper for quickly defining bitflags with verified properties in Verus. It only supports literal values for the bits.

Example

bitflags! {
    pub struct Flags: u32 {
        const A = 0b00000001;
        const B = 0b00000010;
        const C = 0b00000100;
        const ABC = 0b00000111;
    }
}

let f = Flags::A | Flags::B;
assert!(f.contains(Flags::A));