diff --git a/source/Cargo.toml b/source/Cargo.toml index a0d82a3..d8288cd 100644 --- a/source/Cargo.toml +++ b/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 diff --git a/source/bitflags_verus/Cargo.toml b/source/bitflags_verus/Cargo.toml new file mode 100644 index 0000000..eaef339 --- /dev/null +++ b/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)'] } diff --git a/source/bitflags_verus/README.md b/source/bitflags_verus/README.md new file mode 100644 index 0000000..42e9c8f --- /dev/null +++ b/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 diff --git a/source/bitflags_verus/src/lib.rs b/source/bitflags_verus/src/lib.rs new file mode 100644 index 0000000..95a5211 --- /dev/null +++ b/source/bitflags_verus/src/lib.rs @@ -0,0 +1,616 @@ +// SPDX-License-Identifier: MIT +//! # bitflags_verus +//! +//! Formal [Verus](https://github.com/verus-lang/verus) specifications for +//! Rust's [`bitflags`](https://docs.rs/bitflags) crate. +//! +//! This crate provides the [`bitflags_verus!`] macro, a drop-in wrapper around +//! `bitflags::bitflags!` that additionally emits Verus `assume_specification` +//! annotations for every generated method and operator. This lets you write +//! verified code that reasons about bitflags values using their underlying +//! integer representation—without giving up the ergonomics of `bitflags`. +//! +//! ## Limitations +//! +//! - **Unverified assumptions.** All specifications are provided via +//! `assume_specification` (i.e., trusted axioms) rather than verified proofs. +//! Verus currently cannot inject proof code into macro-generated function +//! bodies from external crates, so the correctness of these specs relies on +//! manual review against the `bitflags` implementation, not machine-checked +//! proofs. +//! +//! - **Incomplete coverage.** This crate may not provide specifications for +//! every method or trait impl that `bitflags!` generates. In particular, +//! iterator-related methods, `Debug`/`Display` formatting, and +//! `FromIterator` are not currently specified. +//! +//! ## Design +//! +//! Each bitflags struct is modeled as an opaque type with a single +//! `spec fn view(self) -> Bits` that maps to the underlying integer value. +//! All specifications are expressed in terms of `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 ([`axiom_from_bits_retain`](traits::axiom_from_bits_retain)) +//! bridges the opaque struct to concrete bit values: +//! `spec_from_bits_retain(bits).view() == bits`. +//! +//! ## Quick Start +//! +//! Add to your `Cargo.toml`: +//! ```toml +//! [dependencies] +//! bitflags = "2" +//! bitflags_verus = "0.1" +//! ``` +//! +//! Then define flags with full Verus specifications: +//! ```ignore +//! 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@); +//! } +//! } +//! } +//! ``` +//! +//! ## What Gets Specified +//! +//! The macro emits specifications for: +//! +//! | 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`) | +//! +//! ## Broadcast Lemmas +//! +//! This crate provides per-type broadcast groups (`bitflags_bit_lemmas_`) +//! with commonly needed bit-vector identities that Verus's SMT solver cannot +//! prove automatically: +//! +//! - **OR-AND absorption:** `(a | b) & b == b` +//! - **OR preserves subset:** `(a & b) == b ==> (a | c) & b == b` +//! - **Difference clears bits:** `(a & !b) & b == 0` +//! +//! These are generated for `u8`, `u16`, `u32`, `u64`, `usize`, `i32`, and +//! `isize`. The macro automatically imports the group matching your struct's +//! underlying type. For use in your own `verus!` blocks, import explicitly: +//! +//! ```ignore +//! verus! { +//! broadcast use bitflags_verus::bitflags_bit_lemmas_u32; +//! } +//! ``` +//! +//! ## Using `#[verus_spec]` with Existing Functions +//! +//! You can annotate existing functions that take or return bitflags with +//! `#[verus_spec]` to add pre/postconditions using the `view()` model: +//! +//! ```ignore +//! #[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; +//! } +//! } +//! +//! #[verus_spec( +//! ensures *final(perms) == spec_union(*old(perms), Permissions::READ), +//! )] +//! fn grant_read(perms: &mut Permissions) { +//! perms.insert(Permissions::READ); +//! } +//! +//! #[verus_spec( +//! ensures *final(perms) == spec_difference(*old(perms), Permissions::WRITE), +//! )] +//! fn revoke_write(perms: &mut Permissions) { +//! perms.remove(Permissions::WRITE); +//! } +//! +//! #[verus_spec(ret => +//! ensures ret == ((perms@ & Permissions::EXECUTE@) == Permissions::EXECUTE@), +//! )] +//! fn has_execute(perms: &Permissions) -> bool { +//! perms.contains(Permissions::EXECUTE) +//! } +//! ``` +//! +//! ## Supported Underlying Types +//! +//! Any integer type supported by `bitflags`: `u8`, `u16`, `u32`, `u64`, +//! `u128`, `usize`, `i8`, `i16`, `i32`, `i64`, `i128`, `isize`. +#![no_std] + +pub mod traits; +pub use vstd::prelude::*; + +verus! { + +#[cfg(verus_only)] +pub use traits::spec_from_bits_retain; +#[cfg(verus_only)] +pub use traits::FlagsSpec; + +/// Core broadcast group auto-imported by all consumers of this crate. +/// +/// Contains [`axiom_from_bits_retain`](traits::axiom_from_bits_retain), the +/// foundational axiom that connects the opaque bitflags struct to its +/// underlying bit representation: `spec_from_bits_retain(bits).view() == bits`. +#[cfg_attr(verus_only, verifier::broadcast_use_by_default_when_this_crate_is_imported)] +pub broadcast group bigflags_axioms { + traits::axiom_from_bits_retain, +} + +} // verus! +/// Generate broadcast proofs for bit-vector identities for a single integer type. +/// +/// Each invocation produces three broadcast lemmas and one broadcast group: +/// - `lemma_bitor_band_absorb_`: `(a | b) & b == b` +/// - `lemma_bitor_preserves_subset_`: `(a & b) == b ==> (a | c) & b == b` +/// - `lemma_band_not_clears_`: `(a & !b) & b == 0` +/// - `bitflags_bit_lemmas_`: group containing all three +macro_rules! bitflags_bit_lemmas { + ($($suffix:ident : $uN:ty),* $(,)?) => { + paste! { verus! { $( + /// OR-AND absorption: `(a | b) & b == b` + pub broadcast proof fn [](a: $uN, b: $uN) + ensures #[trigger] ((a | b) & b) == b + { assert((a | b) & b == b) by(bit_vector); } + + /// OR preserves subset: if `(a & b) == b` then `((a | c) & b) == b` + pub broadcast proof fn [](a: $uN, b: $uN, c: $uN) + requires (a & b) == b, + ensures #[trigger] ((a | c) & b) == b + { assert((a & b) == b ==> (a | c) & b == b) by(bit_vector); } + + /// Difference clears target bits: `(a & !b) & b == 0` + pub broadcast proof fn [](a: $uN, b: $uN) + ensures #[trigger] ((a & !b) & b) == (0 as $uN) + { assert((a & !b) & b == (0 as $uN)) by(bit_vector); } + + /// Per-type broadcast group for bit-vector lemmas. + pub broadcast group [] { + [], + [], + [], + } + )* } +} + }; +} + +bitflags_bit_lemmas!(u8: u8, u16: u16, u32: u32, u64: u64, usize: usize, i32: i32, isize: isize); + +/// Define a bitflags struct with full Verus formal specifications. +/// +/// This macro wraps [`bitflags::bitflags!`] and emits Verus +/// `assume_specification` annotations for all generated methods, operators, +/// and named constants. The specifications model each flags value as an +/// opaque type with `spec fn view(self) -> Bits` returning the underlying +/// integer representation. +/// +/// # Syntax +/// +/// Identical to `bitflags::bitflags!`: +/// +/// ```ignore +/// bitflags_verus! { +/// #[derive(Copy, Clone, Debug, Default)] +/// pub struct MyFlags: u32 { +/// const A = 1 << 0; +/// const B = 1 << 1; +/// const C = 1 << 2; +/// } +/// } +/// ``` +/// +/// # Requirements +/// +/// Your crate must depend on `bitflags` (version 2.x) directly—this macro +/// invokes `::bitflags::bitflags!` from the consumer's namespace. +/// +/// # Generated Specifications +/// +/// For each struct, the macro generates: +/// - `spec fn view(self) -> Bits` — the underlying integer value +/// - `spec fn spec_all() -> Self` — all defined flags OR'd together +/// - `spec fn spec_empty() -> Self` — zero value +/// - Inline specs for all set operations (`spec_union`, `spec_intersection`, etc.) +/// - `assume_specification` for every exec method and operator +/// - `spec const SPEC_` for each named constant +/// - Operator trait impls (`BitOrSpecImpl`, `BitAndSpecImpl`, etc.) +/// +/// # Example (Verus verification) +/// +/// ```ignore +/// verus! { +/// // Import bit-vector lemmas for the underlying type +/// broadcast use bitflags_verus::bitflags_bit_lemmas_u32; +/// +/// proof fn union_is_bitor(a: MyFlags, b: MyFlags) { +/// assert(a.union(b)@ == a@ | b@); +/// } +/// +/// proof fn contains_is_subset(flags: MyFlags, check: MyFlags) { +/// assert(flags.contains(check) == ((flags@ & check@) == check@)); +/// } +/// } +/// ``` +#[macro_export] +macro_rules! bitflags_verus { + ( + $(#[$outer:meta])* + $vis:vis struct $name:ident : $bits:ty { + $( + $(#[$cmeta:meta])* + const $cname:ident = $cvalue:expr; + )* + } + ) => { + paste! { + mod [] { + use super::*; + ::bitflags::bitflags! { + $(#[$outer])* + $vis struct $name : $bits { + $( + $(#[$cmeta])* + const $cname = $cvalue; + )* + } + } + + $crate::__bitflags_verus_one! { + $name, $bits, [ $( $cname = ($cvalue) ),* ] + } + } + use []::*; + } + }; +} + +/// Internal helper macro for [`bitflags_verus!`]. Do not use directly. +/// +/// Emits all Verus specifications for a single bitflags struct: the +/// `external_type_specification`, `FlagsSpecImpl`, spec mirrors, +/// `assume_specification` annotations, and operator trait impls. +#[doc(hidden)] +#[macro_export] +macro_rules! __bitflags_verus_one { + ($name:ident, $bits:ty, [ $( $cname:ident = ($cvalue:expr) ),* $(,)? ]) => { + #[cfg(verus_only)] + $crate::paste! {$crate::verus! { + use super::*; + impl $name { + #[verifier::inline] + pub open spec fn view(self) -> $bits { + self.bits_spec() + } + } + /// Register the bitflags-emitted struct as a Verus-known + /// external type so an inherent `spec fn` can be added. + #[verifier::external_type_specification] + #[verifier::external_body] + pub struct ExBitflagsView($name); + // -- spec mirrors used by `when_used_as_spec` ---------------- + // + // For every exec method that takes only spec-friendly inputs + // and returns a spec-friendly value, define a `spec_` + // free function with the same signature. The matching + // `#[verifier::when_used_as_spec(spec_)]` attribute + // on the `assume_specification` then lets calls to the exec + // method appear in `requires`/`ensures` and `#[verus_spec]` + // positions. + + #[verifier::inline] + pub open spec fn spec_all() -> $name { + $crate::spec_from_bits_retain((0 as $bits) $( | ($cvalue as $bits) )*) + } + + #[verifier::inline] + pub open spec fn spec_empty() -> $name { + $crate::spec_from_bits_retain(0 as $bits) + } + + pub open spec fn spec_bits(s: &$name) -> $bits { + s.view() + } + + #[verifier::inline] + pub open spec fn spec_from_bits_truncate(bits: $bits) -> $name { + $crate::spec_from_bits_retain(bits & spec_all().view()) + } + + #[verifier::inline] + pub open spec fn spec_from_bits(bits: $bits) -> Option<$name> { + if bits == (bits & spec_all().view()) { + Some($crate::spec_from_bits_retain(bits)) + } else { + None + } + } + + pub open spec fn spec_is_empty(s: &$name) -> bool { + s.view() == 0 as $bits + } + + pub open spec fn spec_is_all(s: &$name) -> bool { + (s.view() | $name::all().view()) == s.view() + } + + pub open spec fn spec_intersects(s: &$name, other: $name) -> bool { + s.view() & other.view() != 0 as $bits + } + + pub open spec fn spec_contains(s: &$name, other: $name) -> bool { + (s.view() & other.view()) == other.view() + } + + #[verifier::inline] + pub open spec fn spec_intersection(s: $name, other: $name) -> $name { + $crate::spec_from_bits_retain(s.view() & other.view()) + } + + #[verifier::inline] + pub open spec fn spec_union(s: $name, other: $name) -> $name { + $crate::spec_from_bits_retain(s.view() | other.view()) + } + + #[verifier::inline] + pub open spec fn spec_difference(s: $name, other: $name) -> $name { + $crate::spec_from_bits_retain(s.view() & !other.view()) + } + + #[verifier::inline] + pub open spec fn spec_symmetric_difference(s: $name, other: $name) -> $name { + $crate::spec_from_bits_retain(s.view() ^ other.view()) + } + + #[verifier::inline] + pub open spec fn spec_complement(s: $name) -> $name { + $crate::spec_from_bits_retain((!s.view()) & spec_all().view()) + } + + #[verifier::inline] + pub open spec fn spec_from_bits_retain(bits: $bits) -> $name { + $crate::spec_from_bits_retain(bits) + } + + $( + pub spec const []: $name = spec_from_bits_retain($cvalue as $bits); + #[allow(non_snake_case)] + #[verifier::when_used_as_spec([])] + pub assume_specification[ $name::$cname ] -> (r: $name) + ensures r == []; + )* + + // -- assume_specifications, each tied to its spec mirror ----- + + #[verifier::when_used_as_spec(spec_all)] + pub assume_specification[ $name::all ]() -> (r: $name) + ensures r == spec_all(); + + #[verifier::when_used_as_spec(spec_empty)] + pub assume_specification[ $name::empty ]() -> (r: $name) + ensures r.view() == 0 as $bits; + + #[verifier::when_used_as_spec(spec_bits)] + pub assume_specification[ $name::bits ](s: &$name) -> (r: $bits) + ensures r == s.view(); + + #[verifier::when_used_as_spec(spec_from_bits_retain)] + pub assume_specification[ $name::from_bits_retain ](bits: $bits) + -> (r: $name) + ensures + r === spec_from_bits_retain(bits), + r.view() == bits; + + #[verifier::when_used_as_spec(spec_from_bits_truncate)] + pub assume_specification[ $name::from_bits_truncate ](bits: $bits) + -> (r: $name) + ensures + r == spec_from_bits_truncate(bits), + r.view() == (bits & $name::all().view()); + + #[verifier::when_used_as_spec(spec_from_bits)] + pub assume_specification[ $name::from_bits ](bits: $bits) + -> (r: Option<$name>) + ensures + r == spec_from_bits(bits), + r.is_some() == (bits == (bits & $name::all().view())), + match r { + Some(v) => v.view() == bits, + None => true, + }; + + #[verifier::when_used_as_spec(spec_is_empty)] + pub assume_specification[ $name::is_empty ](s: &$name) -> (r: bool) + ensures r == spec_is_empty(s); + + #[verifier::when_used_as_spec(spec_is_all)] + pub assume_specification[ $name::is_all ](s: &$name) -> (r: bool) + ensures r == spec_is_all(s); + + #[verifier::when_used_as_spec(spec_intersects)] + pub assume_specification[ $name::intersects ](s: &$name, other: $name) + -> (r: bool) + ensures r == spec_intersects(s, other); + + #[verifier::when_used_as_spec(spec_contains)] + pub assume_specification[ $name::contains ](s: &$name, other: $name) + -> (r: bool) + ensures r == spec_contains(s, other); + + #[verifier::when_used_as_spec(spec_intersection)] + pub assume_specification[ $name::intersection ](s: $name, other: $name) + -> (r: $name) + ensures + r == spec_intersection(s, other), + r.view() == s.view() & other.view(); + + #[verifier::when_used_as_spec(spec_union)] + pub assume_specification[ $name::union ](s: $name, other: $name) + -> (r: $name) + ensures + r == spec_union(s, other), + r.view() == s.view() | other.view(); + + #[verifier::when_used_as_spec(spec_difference)] + pub assume_specification[ $name::difference ](s: $name, other: $name) + -> (r: $name) + ensures + r == spec_difference(s, other), + r.view() == s.view() & !other.view(); + + #[verifier::when_used_as_spec(spec_symmetric_difference)] + pub assume_specification[ $name::symmetric_difference ](s: $name, other: $name) + -> (r: $name) + ensures + r == spec_symmetric_difference(s, other), + r.view() == s.view() ^ other.view(); + + #[verifier::when_used_as_spec(spec_complement)] + pub assume_specification[ $name::complement ](s: $name) -> (r: $name) + ensures + r == spec_complement(s), + r.view() == (!s.view()) & $name::all().view(); + + // Mutating methods (no `when_used_as_spec` — they return ()). + + pub assume_specification[ $name::insert ](s: &mut $name, other: $name) + ensures *final(s) == spec_union(*old(s), other); + + pub assume_specification[ $name::remove ](s: &mut $name, other: $name) + ensures *final(s) == spec_difference(*old(s), other); + + pub assume_specification[ $name::toggle ](s: &mut $name, other: $name) + ensures *final(s) == spec_symmetric_difference(*old(s), other); + + pub assume_specification[ $name::set ]( + s: &mut $name, other: $name, value: bool, + ) + ensures + *final(s) == if value { + spec_union(*old(s), other) + } else { + spec_difference(*old(s), other) + }; + + // -- include operators even when they are defined outside the verus! ------ + impl $crate::traits::FlagsSpecImpl for $name { + open spec fn obeys_bitflags_spec() -> bool { true } + uninterp spec fn bits_spec(&self) -> Self::Bits; + } + + impl vstd::std_specs::ops::BitOrSpecImpl for $name { + open spec fn obeys_bitor_spec() -> bool { true } + open spec fn bitor_req(self, other: $name) -> bool { true } + open spec fn bitor_spec(self, other: $name) -> $name { + spec_union(self, other) + } + } + impl vstd::std_specs::ops::BitAndSpecImpl for $name { + open spec fn obeys_bitand_spec() -> bool { true } + open spec fn bitand_req(self, other: $name) -> bool { true } + open spec fn bitand_spec(self, other: $name) -> $name { + spec_intersection(self, other) + } + } + impl vstd::std_specs::ops::BitXorSpecImpl for $name { + open spec fn obeys_bitxor_spec() -> bool { true } + open spec fn bitxor_req(self, other: $name) -> bool { true } + open spec fn bitxor_spec(self, other: $name) -> $name { + spec_symmetric_difference(self, other) + } + } + impl vstd::std_specs::ops::SubSpecImpl for $name { + open spec fn obeys_sub_spec() -> bool { true } + open spec fn sub_req(self, other: $name) -> bool { true } + open spec fn sub_spec(self, other: $name) -> $name { + spec_difference(self, other) + } + } + impl vstd::std_specs::ops::NotSpecImpl for $name { + open spec fn obeys_not_spec() -> bool { true } + open spec fn not_req(self) -> bool { true } + open spec fn not_spec(self) -> $name { + spec_complement(self) + } + } + pub assume_specification[ <$name as ::core::ops::BitOr>::bitor ]( + s: $name, other: $name, + ) -> (r: $name); + + pub assume_specification[ <$name as ::core::ops::BitAnd>::bitand ]( + s: $name, other: $name, + ) -> (r: $name); + + pub assume_specification[ <$name as ::core::ops::BitXor>::bitxor ]( + s: $name, other: $name, + ) -> (r: $name); + + pub assume_specification[ <$name as ::core::ops::Sub>::sub ]( + s: $name, other: $name, + ) -> (r: $name); + + pub assume_specification[ <$name as ::core::ops::Not>::not ](s: $name) + -> (r: $name); + + pub assume_specification[ <$name as ::core::ops::BitOrAssign>::bitor_assign ]( + s: &mut $name, other: $name, + ); + + pub assume_specification[ <$name as ::core::ops::BitAndAssign>::bitand_assign ]( + s: &mut $name, other: $name, + ); + + pub assume_specification[ <$name as ::core::ops::BitXorAssign>::bitxor_assign ]( + s: &mut $name, other: $name, + ); + + pub assume_specification[ <$name as ::core::ops::SubAssign>::sub_assign ]( + s: &mut $name, other: $name, + ); + } +} + }; +} + +#[doc(hidden)] +pub use paste::paste; diff --git a/source/bitflags_verus/src/traits.rs b/source/bitflags_verus/src/traits.rs new file mode 100644 index 0000000..1bba66f --- /dev/null +++ b/source/bitflags_verus/src/traits.rs @@ -0,0 +1,53 @@ +// SPDX-License-Identifier: MIT OR Apache-2.0 +// +// Author: Ziqiao Zhou +// +// External specifications for the `bitflags` crate traits. +#![cfg(verus_only)] +use bitflags::Bits; +use vstd::prelude::*; + +verus! { + +pub uninterp spec fn spec_from_bits_retain(bits: B) -> T; + +pub broadcast axiom fn axiom_from_bits_retain(bits: T::Bits) where T: bitflags::Flags + ensures + T::obeys_bitflags_spec() ==> (#[trigger] spec_from_bits_retain::( + bits, + )).bits_spec() == bits, +; + +#[verifier::external_trait_specification] +pub trait ExBits: Clone + Copy + core::cmp::PartialEq + core::ops::BitAnd< + Output = Self, +> + core::ops::BitOr + core::ops::BitXor + core::ops::Not< + Output = Self, +> + Sized + 'static { + type ExternalTraitSpecificationFor: bitflags::Bits; +} + +#[verifier::external_trait_specification] +#[verifier::external_trait_extension(FlagsSpec via FlagsSpecImpl)] +pub trait ExFlags: Sized + 'static { + type ExternalTraitSpecificationFor: bitflags::Flags; + + /// The underlying bits type. + type Bits: bitflags::Bits; + + spec fn obeys_bitflags_spec() -> bool; + + spec fn bits_spec(&self) -> Self::Bits; + + fn from_bits_retain(bits: Self::Bits) -> (ret: Self) + ensures + Self::obeys_bitflags_spec() ==> ret == spec_from_bits_retain::(bits), + ; + + fn bits(&self) -> (ret: Self::Bits) + ensures + Self::obeys_bitflags_spec() ==> ret == self.bits_spec(), + ; +} + +} // verus! diff --git a/source/bitflags_verus/tests/Cargo.toml b/source/bitflags_verus/tests/Cargo.toml new file mode 100644 index 0000000..9dbfd8f --- /dev/null +++ b/source/bitflags_verus/tests/Cargo.toml @@ -0,0 +1,15 @@ +[package] +name = "bitflags_verus_tests" +version = "0.1.0" +edition = "2024" +publish = false + +[dependencies] +bitflags_verus = { path = ".." } +bitflags = "2.11.0" +paste = "1.0" +vstd = { version = "=0.0.0-2026-05-24-0157", features = ["alloc", "allow_panic"], default-features = false } + +[package.metadata.verus] +verify = true + diff --git a/source/bitflags_verus/tests/src/lib.rs b/source/bitflags_verus/tests/src/lib.rs new file mode 100644 index 0000000..03029ed --- /dev/null +++ b/source/bitflags_verus/tests/src/lib.rs @@ -0,0 +1,13 @@ +// SPDX-License-Identifier: MIT +//! Demonstration tests for `bitflags_verus!` showing how the macro provides +//! Verus specifications for bitflags-generated types. +//! +//! Tests cover four underlying bit types: u32, usize, i32, isize. +//! All assertions are relational (no concrete value checks). +#![no_std] + +pub mod test_i32; +pub mod test_isize; +pub mod test_u32; +pub mod test_usize; +pub mod test_verus_spec; diff --git a/source/bitflags_verus/tests/src/test_i32.rs b/source/bitflags_verus/tests/src/test_i32.rs new file mode 100644 index 0000000..162b83d --- /dev/null +++ b/source/bitflags_verus/tests/src/test_i32.rs @@ -0,0 +1,120 @@ +use bitflags_verus::*; + +bitflags_verus! { + #[derive(Copy, Clone, Debug, Default)] + pub struct Status32: i32 { + const ACTIVE = 1 << 0; + const PENDING = 1 << 1; + const ERROR = 1 << 2; + } +} + +bitflags::bitflags! { + #[derive(Copy, Clone, Debug, Default)] + pub struct Status32_2: i32 { + const ACTIVE = 1 << 0; + const PENDING = 1 << 1; + const ERROR = 1 << 2; + } +} + +verus! { + +broadcast use bitflags_verus::bitflags_bit_lemmas_i32; + +proof fn test_union(a: Status32, b: Status32) { + let c = a.union(b); + assert(c@ == a@ | b@); +} + +proof fn test_intersection(a: Status32, b: Status32) { + let c = a.intersection(b); + assert(c@ == a@ & b@); +} + +proof fn test_difference(a: Status32, b: Status32) { + let c = a.difference(b); + assert(c@ == a@ & !b@); +} + +proof fn test_symmetric_difference(a: Status32, b: Status32) { + let c = a.symmetric_difference(b); + assert(c@ == a@ ^ b@); +} + +proof fn test_complement(a: Status32) { + let c = a.complement(); + assert(c@ == (!a@) & Status32::all()@); +} + +proof fn test_contains(flags: Status32, check: Status32) { + assert(flags.contains(check) == ((flags@ & check@) == check@)); +} + +proof fn test_empty() { + let e = Status32::empty(); + assert(e@ == 0i32); +} + +proof fn test_from_bits_retain(bits: i32) { + let f = Status32::from_bits_retain(bits); + assert(f@ == bits); +} + +proof fn test_from_bits_truncate(bits: i32) { + let f = Status32::from_bits_truncate(bits); + assert(f@ == (bits & Status32::all()@)); +} + +fn test_insert_remove() { + let mut p = Status32::empty(); + p.insert(Status32::ACTIVE); + p.insert(Status32::PENDING); + proof { + assert(p@ == (0i32 | Status32::ACTIVE@) | Status32::PENDING@); + } + assert(p.contains(Status32::PENDING)); + + let old_view = p.bits(); + p.remove(Status32::PENDING); + proof { + assert(p@ == old_view & !Status32::PENDING@); + assert(p@ & Status32::PENDING@ == 0i32); + } +} +fn test_operators() { + let a = Status32::ACTIVE; + let b = Status32::ERROR; + let c = a | b; + proof { assert(c@ == a@ | b@); } + + let d = c & a; + proof { assert(d@ == c@ & a@); } + let e = c - b; + proof { assert(e@ == c@ & !b@); } +} + +fn test_toggle() { + let mut p = Status32::ACTIVE; + let old_view = p.bits(); + let mask = Status32::ACTIVE | Status32::PENDING; + p.toggle(mask); + proof { + assert(p@ == old_view ^ mask@); + } +} + +fn test_set() { + let mut p = Status32::empty(); + p.set(Status32::ERROR, true); + proof { + assert(p@ == 0i32 | Status32::ERROR@); + } + let old_view = p.bits(); + p.set(Status32::ERROR, false); + proof { + assert(p@ == old_view & !Status32::ERROR@); + } +} + +} // verus! diff --git a/source/bitflags_verus/tests/src/test_isize.rs b/source/bitflags_verus/tests/src/test_isize.rs new file mode 100644 index 0000000..440c695 --- /dev/null +++ b/source/bitflags_verus/tests/src/test_isize.rs @@ -0,0 +1,111 @@ +use bitflags_verus::*; + +bitflags_verus! { + #[derive(Copy, Clone, Debug, Default)] + pub struct Caps: isize { + const NET = 1 << 0; + const DISK = 1 << 1; + const ADMIN = 1 << 2; + } +} + +verus! { + +broadcast use bitflags_verus::bitflags_bit_lemmas_isize; + +proof fn test_union(a: Caps, b: Caps) { + let c = a.union(b); + assert(c@ == a@ | b@); +} + +proof fn test_intersection(a: Caps, b: Caps) { + let c = a.intersection(b); + assert(c@ == a@ & b@); +} + +proof fn test_difference(a: Caps, b: Caps) { + let c = a.difference(b); + assert(c@ == a@ & !b@); +} + +proof fn test_symmetric_difference(a: Caps, b: Caps) { + let c = a.symmetric_difference(b); + assert(c@ == a@ ^ b@); +} + +proof fn test_complement(a: Caps) { + let c = a.complement(); + assert(c@ == (!a@) & Caps::all()@); +} + +proof fn test_contains(flags: Caps, check: Caps) { + assert(flags.contains(check) == ((flags@ & check@) == check@)); +} + +proof fn test_empty() { + let e = Caps::empty(); + assert(e@ == 0isize); +} + +proof fn test_from_bits_retain(bits: isize) { + let f = Caps::from_bits_retain(bits); + assert(f@ == bits); +} + +proof fn test_from_bits_truncate(bits: isize) { + let f = Caps::from_bits_truncate(bits); + assert(f@ == (bits & Caps::all()@)); +} + +fn test_insert_remove() { + let mut p = Caps::empty(); + p.insert(Caps::NET); + p.insert(Caps::DISK); + proof { + assert(p@ == (0isize | Caps::NET@) | Caps::DISK@); + } + assert(p.contains(Caps::DISK)); + + let old_view = p.bits(); + p.remove(Caps::DISK); + proof { + assert(p@ == old_view & !Caps::DISK@); + assert(p@ & Caps::DISK@ == 0isize); + } +} + +fn test_operators() { + let a = Caps::NET; + let b = Caps::ADMIN; + let c = a | b; + proof { assert(c@ == a@ | b@); } + let d = c & a; + proof { assert(d@ == c@ & a@); } + let e = c - b; + proof { assert(e@ == c@ & !b@); } +} + +fn test_toggle() { + let mut p = Caps::NET; + let old_view = p.bits(); + let mask = Caps::NET | Caps::DISK; + p.toggle(mask); + proof { + assert(p@ == old_view ^ mask@); + } +} + +fn test_set() { + let mut p = Caps::empty(); + p.set(Caps::ADMIN, true); + proof { + assert(p@ == 0isize | Caps::ADMIN@); + } + let old_view = p.bits(); + p.set(Caps::ADMIN, false); + proof { + assert(p@ == old_view & !Caps::ADMIN@); + } +} + +} // verus! diff --git a/source/bitflags_verus/tests/src/test_u32.rs b/source/bitflags_verus/tests/src/test_u32.rs new file mode 100644 index 0000000..d5fb2a2 --- /dev/null +++ b/source/bitflags_verus/tests/src/test_u32.rs @@ -0,0 +1,111 @@ +use bitflags_verus::*; + +bitflags_verus! { + #[derive(Copy, Clone, Debug, Default)] + pub struct Perms32: u32 { + const READ = 1 << 0; + const WRITE = 1 << 1; + const EXECUTE = 1 << 2; + } +} + +verus! { + +broadcast use bitflags_verus::bitflags_bit_lemmas_u32; + +proof fn test_union(a: Perms32, b: Perms32) { + let c = a.union(b); + assert(c@ == a@ | b@); +} + +proof fn test_intersection(a: Perms32, b: Perms32) { + let c = a.intersection(b); + assert(c@ == a@ & b@); +} + +proof fn test_difference(a: Perms32, b: Perms32) { + let c = a.difference(b); + assert(c@ == a@ & !b@); +} + +proof fn test_symmetric_difference(a: Perms32, b: Perms32) { + let c = a.symmetric_difference(b); + assert(c@ == a@ ^ b@); +} + +proof fn test_complement(a: Perms32) { + let c = a.complement(); + assert(c@ == (!a@) & Perms32::all()@); +} + +proof fn test_contains(flags: Perms32, check: Perms32) { + assert(flags.contains(check) == ((flags@ & check@) == check@)); +} + +proof fn test_empty() { + let e = Perms32::empty(); + assert(e@ == 0u32); +} + +proof fn test_from_bits_retain(bits: u32) { + let f = Perms32::from_bits_retain(bits); + assert(f@ == bits); +} + +proof fn test_from_bits_truncate(bits: u32) { + let f = Perms32::from_bits_truncate(bits); + assert(f@ == (bits & Perms32::all()@)); +} + +fn test_insert_remove() { + let mut p = Perms32::empty(); + p.insert(Perms32::READ); + p.insert(Perms32::WRITE); + proof { + assert(p@ == (0u32 | Perms32::READ@) | Perms32::WRITE@); + } + assert(p.contains(Perms32::WRITE)); + + let old_view = p.bits(); + p.remove(Perms32::WRITE); + proof { + assert(p@ == old_view & !Perms32::WRITE@); + assert(p@ & Perms32::WRITE@ == 0u32); + } +} + +fn test_operators() { + let a = Perms32::READ; + let b = Perms32::WRITE; + let c = a | b; + proof { assert(c@ == a@ | b@); } + let d = c & a; + proof { assert(d@ == c@ & a@); } + let e = c - b; + proof { assert(e@ == c@ & !b@); } +} + +fn test_toggle() { + let mut p = Perms32::READ; + let old_view = p.bits(); + let mask = Perms32::READ | Perms32::WRITE; + p.toggle(mask); + proof { + assert(p@ == old_view ^ mask@); + } +} + +fn test_set() { + let mut p = Perms32::empty(); + p.set(Perms32::EXECUTE, true); + proof { + assert(p@ == 0u32 | Perms32::EXECUTE@); + } + let old_view = p.bits(); + p.set(Perms32::EXECUTE, false); + proof { + assert(p@ == old_view & !Perms32::EXECUTE@); + } +} + +} // verus! diff --git a/source/bitflags_verus/tests/src/test_usize.rs b/source/bitflags_verus/tests/src/test_usize.rs new file mode 100644 index 0000000..9b30586 --- /dev/null +++ b/source/bitflags_verus/tests/src/test_usize.rs @@ -0,0 +1,113 @@ +use bitflags_verus::*; + +bitflags_verus! { + #[derive(Copy, Clone, Debug, Default)] + pub struct PageFlags: usize { + const PRESENT = 1 << 0; + const WRITABLE = 1 << 1; + const USER = 1 << 2; + const ACCESSED = 1 << 5; + const DIRTY = 1 << 6; + } +} + +verus! { + +broadcast use bitflags_verus::bitflags_bit_lemmas_usize; + +proof fn test_union(a: PageFlags, b: PageFlags) { + let c = a.union(b); + assert(c@ == a@ | b@); +} + +proof fn test_intersection(a: PageFlags, b: PageFlags) { + let c = a.intersection(b); + assert(c@ == a@ & b@); +} + +proof fn test_difference(a: PageFlags, b: PageFlags) { + let c = a.difference(b); + assert(c@ == a@ & !b@); +} + +proof fn test_symmetric_difference(a: PageFlags, b: PageFlags) { + let c = a.symmetric_difference(b); + assert(c@ == a@ ^ b@); +} + +proof fn test_complement(a: PageFlags) { + let c = a.complement(); + assert(c@ == (!a@) & PageFlags::all()@); +} + +proof fn test_contains(flags: PageFlags, check: PageFlags) { + assert(flags.contains(check) == ((flags@ & check@) == check@)); +} + +proof fn test_empty() { + let e = PageFlags::empty(); + assert(e@ == 0usize); +} + +proof fn test_from_bits_retain(bits: usize) { + let f = PageFlags::from_bits_retain(bits); + assert(f@ == bits); +} + +proof fn test_from_bits_truncate(bits: usize) { + let f = PageFlags::from_bits_truncate(bits); + assert(f@ == (bits & PageFlags::all()@)); +} + +fn test_insert_remove() { + let mut p = PageFlags::empty(); + p.insert(PageFlags::PRESENT); + p.insert(PageFlags::WRITABLE); + proof { + assert(p@ == (0usize | PageFlags::PRESENT@) | PageFlags::WRITABLE@); + } + assert(p.contains(PageFlags::WRITABLE)); + + let old_view = p.bits(); + p.remove(PageFlags::WRITABLE); + proof { + assert(p@ == old_view & !PageFlags::WRITABLE@); + assert(p@ & PageFlags::WRITABLE@ == 0usize); + } +} + +fn test_operators() { + let a = PageFlags::PRESENT; + let b = PageFlags::USER; + let c = a | b; + proof { assert(c@ == a@ | b@); } + let d = c & a; + proof { assert(d@ == c@ & a@); } + let e = c - b; + proof { assert(e@ == c@ & !b@); } +} + +fn test_toggle() { + let mut p = PageFlags::PRESENT; + let old_view = p.bits(); + let mask = PageFlags::PRESENT | PageFlags::WRITABLE; + p.toggle(mask); + proof { + assert(p@ == old_view ^ mask@); + } +} + +fn test_set() { + let mut p = PageFlags::empty(); + p.set(PageFlags::ACCESSED, true); + proof { + assert(p@ == 0usize | PageFlags::ACCESSED@); + } + let old_view = p.bits(); + p.set(PageFlags::ACCESSED, false); + proof { + assert(p@ == old_view & !PageFlags::ACCESSED@); + } +} + +} // verus! diff --git a/source/bitflags_verus/tests/src/test_verus_spec.rs b/source/bitflags_verus/tests/src/test_verus_spec.rs new file mode 100644 index 0000000..8209496 --- /dev/null +++ b/source/bitflags_verus/tests/src/test_verus_spec.rs @@ -0,0 +1,35 @@ +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! { + broadcast use bitflags_verus::bitflags_bit_lemmas_u32; +} + +#[verus_spec( + ensures *final(perms) == spec_union(*old(perms), Permissions::READ), +)] +fn grant_read(perms: &mut Permissions) { + perms.insert(Permissions::READ); +} + +#[verus_spec( + ensures *final(perms) == spec_difference(*old(perms), Permissions::WRITE), +)] +fn revoke_write(perms: &mut Permissions) { + perms.remove(Permissions::WRITE); +} + +#[verus_spec(ret => + ensures ret == ((perms@ & Permissions::EXECUTE@) == Permissions::EXECUTE@), +)] +fn has_execute(perms: &Permissions) -> bool { + perms.contains(Permissions::EXECUTE) +}