Bitflags

source/Cargo.toml

@@ -4,10 +4,15 @@ members = [
     "verismo_main",
     "verismo",
     "verismo_macro",
-    "verismo_tspec"
+    "verismo_tspec",
+    "bitflags_verus",
+    "bitflags_verus/tests"
 ]
 
 [workspace.dependencies]
+bitflags = "2.13"
+paste = "1.0"
+
 # Verus crates from crates.io.
 # `builtin` and `builtin_macros` are kept as the local crate names (via the
 # `package = ...` rename) so we don't have to touch the `use builtin::*;` /
@@ -17,6 +22,7 @@ builtin_macros = { package = "verus_builtin_macros", version = "=0.0.0-2026-05-2
 verus_state_machines_macros = { version = "=0.0.0-2026-05-24-0157", default-features = false }
 vstd = { version = "=0.0.0-2026-05-24-0157", features = ["alloc", "allow_panic"], default-features = false }
 
+
 # `syn_verus` and `prettyplease_verus` are used only by the project's own
 # proc-macro crates (`verismo_macro` and `verismo_verus`). They are pinned to
 # the old syn-1.x-based fork because the rest of those macros are written

source/bitflags_verus/Cargo.toml

@@ -0,0 +1,23 @@
+[package]
+name = "bitflags_verus"
+version = "0.1.0"
+edition = "2024"
+license = "MIT"
+description = "Verus specification for generated code by bitflags"
+homepage = "https://github.com/microsoft/verismo/tree/main/source/bitflags_verus"
+repository = "https://github.com/microsoft/verismo"
+readme = "README.md"
+keywords = ["verus", "verified-rust", "verification", "bitflags"]
+categories = ["specifications"]
+
+
+[dependencies]
+paste = {workspace = true}
+vstd = {workspace = true}
+bitflags = { workspace = true }
+
+[package.metadata.verus]
+verify = true
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(verus_only)'] }

source/bitflags_verus/README.md

@@ -0,0 +1,168 @@
+# bitflags_verus
+
+Formal [Verus](https://github.com/verus-lang/verus) specifications for Rust's [`bitflags`](https://docs.rs/bitflags) crate.
+
+`bitflags_verus` provides the `bitflags_verus!` macro—a drop-in wrapper around `bitflags::bitflags!` that emits Verus `assume_specification` annotations for every generated method and operator. Write verified code that reasons about bitflags values using their underlying integer representation, without giving up `bitflags` ergonomics.
+
+## Installation
+
+Add to your `Cargo.toml`:
+
+```toml
+[dependencies]
+bitflags = "2"
+bitflags_verus = "0.1"
+```
+
+## Quick Start
+
+```rust
+use bitflags_verus::*;
+
+bitflags_verus! {
+    #[derive(Copy, Clone, Debug, Default)]
+    pub struct Permissions: u32 {
+        const READ    = 1 << 0;
+        const WRITE   = 1 << 1;
+        const EXECUTE = 1 << 2;
+    }
+}
+
+verus! {
+    fn example() {
+        let mut p = Permissions::empty();
+        p.insert(Permissions::READ);
+        p.insert(Permissions::WRITE);
+        assert(p.contains(Permissions::WRITE));
+
+        let old = p.bits();
+        p.remove(Permissions::WRITE);
+        proof {
+            assert(p@ == old & !Permissions::WRITE@);
+        }
+    }
+}
+```
+
+## Zero-Cost Usage Pattern
+
+Use `bitflags_verus!` only during verification, falling back to plain `bitflags!` for production builds:
+
+```rust
+#[cfg(verus_only)]
+use bitflags_verus::bitflags_verus as bitflags;
+#[cfg(not(verus_only))]
+use bitflags::bitflags;
+
+bitflags! {
+    #[derive(Copy, Clone, Debug, Default)]
+    pub struct Permissions: u32 {
+        const READ    = 1 << 0;
+        const WRITE   = 1 << 1;
+        const EXECUTE = 1 << 2;
+    }
+}
+```
+
+This way, `bitflags_verus` is never compiled into release binaries—only used when Verus is verifying your code.
+
+## What Gets Specified
+
+| Category | Methods |
+|----------|---------|
+| Construction | `empty`, `all`, `from_bits`, `from_bits_truncate`, `from_bits_retain` |
+| Queries | `bits`, `is_empty`, `is_all`, `contains`, `intersects` |
+| Set operations | `union`, `intersection`, `difference`, `symmetric_difference`, `complement` |
+| Mutation | `insert`, `remove`, `toggle`, `set` |
+| Operators | `|`, `&`, `^`, `-`, `!`, `|=`, `&=`, `^=`, `-=` |
+| Constants | Each named flag (e.g., `Flags::READ`) |
+
+## Design
+
+Each bitflags struct is modeled as an opaque type with a single `spec fn view(self) -> Bits` mapping to the underlying integer. All specifications reduce to `view()`:
+
+- `flags.union(other).view() == flags.view() | other.view()`
+- `flags.contains(other) <==> (flags.view() & other.view()) == other.view()`
+- `flags.complement().view() == (!flags.view()) & Flags::all().view()`
+
+A single foundational axiom bridges the opaque struct to concrete bit values:
+
+```
+spec_from_bits_retain(bits).view() == bits
+```
+
+All other spec functions are `#[verifier::inline]` and unfold to expressions over `spec_from_bits_retain`, enabling automatic reasoning without additional axiom triggers.
+
+## Broadcast Lemmas
+
+The crate provides per-type broadcast groups with bit-vector identities the SMT solver cannot prove automatically:
+
+| Lemma | Identity |
+|-------|----------|
+| OR-AND absorption | `(a \| b) & b == b` |
+| OR preserves subset | `(a & b) == b ==> (a \| c) & b == b` |
+| Difference clears bits | `(a & !b) & b == 0` |
+
+Generated for: `u8`, `u16`, `u32`, `u64`, `usize`, `i32`, `isize`.
+
+The macro automatically imports the matching group for your struct's underlying type. For use in your own `verus!` blocks, import explicitly:
+
+```rust
+verus! {
+    broadcast use bitflags_verus::bitflags_bit_lemmas_u32;
+}
+```
+
+## Using `#[verus_spec]` with Existing Functions
+
+Annotate functions that take or return bitflags to add pre/postconditions:
+
+```rust
+#[verus_spec(
+    ensures *final(perms) == spec_union(*old(perms), Permissions::READ),
+)]
+fn grant_read(perms: &mut Permissions) {
+    perms.insert(Permissions::READ);
+}
+
+#[verus_spec(ret =>
+    ensures ret == ((perms@ & Permissions::EXECUTE@) == Permissions::EXECUTE@),
+)]
+fn has_execute(perms: &Permissions) -> bool {
+    perms.contains(Permissions::EXECUTE)
+}
+```
+
+## Supported Types
+
+Any integer type supported by `bitflags`: `u8`, `u16`, `u32`, `u64`, `u128`, `usize`, `i8`, `i16`, `i32`, `i64`, `i128`, `isize`.
+
+## Limitations
+
+- **Unverified assumptions.** All specifications use `assume_specification` (trusted axioms) rather than machine-checked proofs. Verus cannot currently inject proof code into macro-generated function bodies from external crates. Correctness relies on manual review against the `bitflags` implementation.
+
+- **Incomplete coverage.** Not every method or trait impl generated by `bitflags!` is specified. In particular, iterator-related methods, `Debug`/`Display` formatting, and `FromIterator` are not currently covered.
+
+## Running Tests
+
+The test crate lives at `bitflags_verus/tests/`. Verify using `cargo verus focus`:
+
+```bash
+# Verify the bitflags_verus crate itself
+cargo verus focus -p bitflags_verus --release
+
+# Verify all tests
+cd bitflags_verus/tests && cargo verus focus -p bitflags_verus_tests --release
+
+# Verify a single test module (e.g., u32 tests)
+cd bitflags_verus/tests && cargo verus focus -p bitflags_verus_tests --release -- --verify-only-module test_u32
+
+# Verify a single function
+cd bitflags_verus/tests && cargo verus focus -p bitflags_verus_tests --release -- --verify-function test_union
+```
+
+Run from the workspace root (`source/`).
+
+## License
+
+MIT