Macro __verus_proof_idempotent_fold__ 

macro_rules! __verus_proof_idempotent_fold__ {
    (
        acc = $accty:ty, 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 fold closure (shape |acc, item| with acc: &mut A) with a Verus-checked proof of idempotence.

Use verus_proof_idempotent_reduce! for reduce, whose accumulator is seeded with the first element, which needs an additional obligation.

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 on an item x once, and on x twice in a row, 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:

stream.fold(
    q!(|| 0u32),
    q!(
        |acc, x| { if x > *acc { *acc = x; } },
        idempotent = verus_proof_idempotent_fold!(acc = u32, item = u32)
    ),
);

Read-only captures are declared in a captures = |...| clause, exactly as for verus_proof_commutative_fold!; the macro checks at compile time that every capture is declared.

An optional proof = |state, x| { ... } clause supplies a proof script to help the SMT solver, with ghost bindings for the initial accumulator and the item (e.g. proof = |s, x| { assert(((s | x) | x) == (s | x)) by (bit_vector); }). 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 VerusIdempotentProof marker.