Macro __verus_proof_idempotent_effect__ 

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

Fulfills an idempotent = ... 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 idempotence of the captured-state update.

What idempotence means for an effectful closure: processing an item twice in a row, starting from the same captured state, must leave the captured state in the same final value as processing it once. Because the closure returns () (enforced by this macro; use verus_proof_idempotent_map! or verus_proof_idempotent_filter! for closures whose return value is observable), the state is the only observable effect.

The mutated 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. 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).

An optional proof = |state, x| { ... } clause supplies a proof script to help the SMT solver, with ghost bindings for the initial captured state and the item.

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.

Example

let flags_mut = flags.by_mut();
stream.for_each(q!(
    |x| { *flags_mut |= x; },
    idempotent = verus_proof_idempotent_effect!(
        item = u32,
        captures_mut = |flags_mut: u32|,
        proof = |s, x| { assert(((s | x) | x) == (s | x)) by (bit_vector); }
    )
));