Macro __verus_proof_commutative_effect__ 

macro_rules! __verus_proof_commutative_effect__ {
    (
        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 unit-returning, effectful closure (shape |item| -> (), e.g. for for_each or inspect) that mutates a captured singleton reference (from Singleton::by_mut), with a Verus-checked proof of commutativity of the captured-state update.

What commutativity means for an effectful closure: processing any two items in either order, starting from the same captured state, must leave the captured state in the same final value. Because the closure returns () (enforced by this macro; use verus_proof_commutative_map! or verus_proof_commutative_filter! for closures whose return value is observable), the state is the only observable effect.

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 (e.g. &u32 for inspect).

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 closure body in both orders — x then y, and y then x — from equal captured states, and asserts that the final states are equal. 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 flags_mut = flags.by_mut();
stream.for_each(q!(
    |x| { *flags_mut |= x; },
    commutative = verus_proof_commutative_effect!(
        item = u32,
        captures_mut = |flags_mut: u32|,
        proof = |s, x, y| { assert(((s | x) | y) == ((s | y) | x)) by (bit_vector); }
    )
));