Crate verified_bitflags 

A verified version of the bitflags crate.

The macro bitflags! generates a single struct whose layout matches the one produced by the upstream bitflags crate (see [bitflags::example_generated::Flags]):

pub struct Flags { bits: T } // bits is private
impl Flags {
    pub const fn A() -> Self;   // one factory per declared flag
    ...
    pub const fn empty() -> Self;
    pub const fn all() -> Self;
    pub const fn bits(&self) -> T;
    pub const fn from_bits(bits: T) -> Option<Self>;
    pub const fn from_bits_truncate(bits: T) -> Self;
    pub const fn contains(&self, other: Self) -> bool;
    pub const fn intersects(&self, other: Self) -> bool;
    pub fn insert(&mut self, other: Self);
    pub fn toggle(&mut self, other: Self);
}

NOTE: unlike upstream bitflags, the per-flag accessors are pub const fn factories (Flags::A()) instead of associated constants (Flags::A). This is required because the bits field is private: Verus refuses to publish a constructor for an opaque datatype through a pub const.

Only literal values are supported for each flag.

Re-exports

pub use paste;

Macros

bitflags

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

bitflags_quick

Defines quick named compositions of existing flags.

Structs

Flags

Enums

__ghostFlags