Macro __verus_proof_idempotent_map__ 

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

What idempotence means for a map closure: processing an item twice in a row, starting from the same captured state, must (1) leave the captured state in the same final value as processing it once, and (2) produce the same output both times as processing it once. Because the output stream also has at-least-once semantics, a retried element may re-emit its output, but must not emit a different one: a closure that reports whether an element is new (e.g. true then false) is not idempotent even if its state update is.

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.

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 max_mut = max_seen.by_mut();
stream.map(q!(
    |x| {
        if x > *max_mut { *max_mut = x; }
        x // outputting `x > *max_mut` (is this new?) would NOT be idempotent!
    },
    idempotent = verus_proof_idempotent_map!(
        item = u32,
        captures_mut = |max_mut: u32|
    )
));