Macro __verus_proof_idempotent_reduce__ 

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

Fulfills an idempotent = ... proof parameter for a reduce closure (shape |acc, item| with acc: &mut T and item: T) with a Verus-checked proof of idempotence.

reduce seeds its accumulator with the first element, so in addition to the verus_proof_idempotent_fold! obligation (applying x twice in a row equals applying it once, from any accumulator), this macro also proves the seed obligation: if the first element is duplicated, applying the closure to an accumulator seeded with x and the item x must leave the accumulator equal to x. The fold obligation alone does not imply this; for example, |acc, x| *acc = max(*acc, x + 1) satisfies it, but reducing [a, a] yields a + 1 instead of a.

stream.reduce(q!(
    |curr, new| { if new > *curr { *curr = new; } },
    idempotent = verus_proof_idempotent_reduce!(item = u32)
));

Read-only captures are declared in a captures = |...| clause. An optional proof = |state, x| { ... } script is inserted into both obligations (for the seed obligation, state is bound to the item itself).

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 VerusIdempotentProof marker.