Macro verus_proof_commutative_map 

macro_rules! verus_proof_commutative_map {
    (
        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 map-like closure (shape |item| -> out, e.g. for map) that may mutate a captured singleton reference (from Singleton::by_mut), with a Verus-checked proof of commutativity.

What commutativity means for a map closure: 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) produce the same multiset of output values (the outputs may be swapped in order, but not changed). Both conditions are required for downstream determinism: outputs that depend on the processing order (e.g. emitting a running total) are not commutative even if the state update is.

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.

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, then asserts that the final states are equal and that the two runs’ outputs are equal as a multiset (pairwise or crossed). 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 count_mut = my_count.by_mut();
stream.map(q!(
    |x| {
        *count_mut = count_mut.wrapping_add(x);
        x // outputting `*count_mut` here would NOT be commutative!
    },
    commutative = verus_proof_commutative_map!(
        item = i32,
        captures_mut = |count_mut: i32|
    )
));