Macro verus_proof_commutative_filter 

macro_rules! verus_proof_commutative_filter {
    (
        item = $itemty:ty
        $(, captures = |$($cap:ident : $capty:ty),* $(,)?|)?
        , captures_mut = |$mcap:ident : $mcapty:ty $(,)?|
        $(, proof = |$pstate:ident, $px:ident, $py:ident| { $($proof_body:tt)* })?
        , __target = { $(move)? |$titem:ident $(: $titemty:ty)?| $target_body:expr }
        , __captures = [$($fv:ident),* $(,)?] $(,)?
    ) => { ... };
    (
        $($rest:tt)*
    ) => { ... };
}

Fulfills a commutative = ... proof parameter for a filter predicate (shape |item| -> bool where item is received by reference) that may mutate a captured singleton reference (from Singleton::by_mut), with a Verus-checked proof of commutativity.

What commutativity means for a filter predicate: processing any two items in either order, starting from the same captured state, must (1) leave the captured state in the same final value, and (2) retain the same multiset of elements. The second condition is essential for soundness: a stateful predicate like a rate limiter converges to the same state either way, but which element passes depends on the order, which is not commutative (unless the elements are equal).

The commuting state is the mutable capture, declared (with the type behind the reference) in the required captures_mut = |state: S| clause; additional read-only captures can be declared in a captures = |...| clause. q! also passes the closure’s capture list (as a trailing __captures = [...] argument), and the macro checks at compile time that every capture is declared. The item = ... type must be written exactly as the closure receives it (for filter, a reference like &u32).

Users never write the proof obligation: this macro receives the quoted closure itself from q! (as a trailing __target = { ... } argument) and generates a Verus function that symbolically executes the actual predicate body in both orders — x then y, and y then x — from equal captured states, then asserts that the final states are equal and that the retained multisets are equal: either the per-item decisions match across the two orders, or the two items are equal and the number of retained copies matches. Verifying this also proves the body panic-free.

An optional proof = |state, x, y| { ... } clause supplies a proof script to help the SMT solver, with ghost bindings for the initial captured state and the two items. The script is checked by Verus and cannot weaken the obligation.

The proof is gated on cfg(verus_keep_ghost), so it only exists when the crate is compiled by the Verus driver (cargo verus verify). Under normal compilation the macro just produces a VerusCommutativeProof marker.

Example

let seen_mut = seen_count.by_mut();
stream.filter(q!(
    |x| {
        *seen_mut = seen_mut.wrapping_add(1);
        *x > 1 // the decision must not depend on the mutable state!
    },
    commutative = verus_proof_commutative_filter!(
        item = &u32,
        captures_mut = |seen_mut: u32|
    )
));