Macro verus_proof_commutative_fold 

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

Fulfills a commutative = ... proof parameter for an aggregation closure (fold / reduce, shape |acc, item| with acc: &mut A) with a Verus-checked proof of commutativity.

Users never write the proof obligation (so they cannot get it wrong): 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 — starting from equal accumulators, and asserts that the final accumulators are equal. Verifying this obligation also proves the closure body panic-free (e.g. no arithmetic overflow). Users only declare the accumulator and item types:

batch.reduce(q!(
    |curr, new| { if new > *curr { *curr = new; } },
    commutative = verus_proof_commutative_fold!(acc = u32, item = u32)
));

If the closure captures (read-only) variables from its environment, re-declare them (with their runtime types) in a captures = |...| clause; the obligation is then universally quantified over the capture values, which is sound since any particular execution uses some fixed value. 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.

An optional proof = |state, x, y| { ... } clause supplies a proof script to help the SMT solver, with ghost bindings for the initial accumulator and the two items (e.g. proof = |s, x, y| { assert((s | x) | y == (s | y) | x) by (bit_vector); }). The script is checked by Verus and cannot weaken the obligation (though, as anywhere in Verus, assume is an explicit soundness escape hatch).

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, so the types go through the ordinary commutative = ... mechanism with zero overhead.