Struct VerusIdempotentProof 

pub struct VerusIdempotentProof { /* private fields */ }

A machine-checked proof of idempotence, verified by Verus.

Created by the verus_proof_idempotent_fold!, verus_proof_idempotent_reduce!, verus_proof_idempotent_map!, verus_proof_idempotent_filter!, and verus_proof_idempotent_effect! macros, one per closure shape, each generating the precise obligation that makes a retried (duplicated) element unobservable for that shape (final accumulator, re-emitted output, retention decision, or captured state, respectively). The obligation is generated by the macro directly from the actual closure body — it symbolically executes the body on an element once, and on the same element twice in a row, from equal initial states, and requires the observable results to be equal — so users never write (and cannot weaken) the assertion. Users only declare the types involved and, optionally, provide a proof script to help the SMT solver, which is itself checked by Verus.

Combined with a commutativity proof (required on unordered streams), the obligation also covers duplicates that are not adjacent to the original element, since commutativity allows moving the duplicate next to it.

When the crate is verified with cargo verus verify, Verus checks the obligation (which also proves the closure body panic-free, e.g. no arithmetic overflow). Under normal compilation, the proof is erased and this type simply marks the property as proven. Note that the simulator does not inject retries, so (unlike commutativity) idempotence claims are not explored by simulation tests at all; a Verus proof is the only mechanical check. This type only implements IdempotentProof, so it cannot be used to fulfill a different property (e.g. commutative = ...).

Trait Implementations

impl Default for VerusIdempotentProof

fn default() -> Self

Returns the “default value” for a type.

impl IdempotentProof for VerusIdempotentProof

fn register_proof(&self, _expr: &Expr)

Registers the expression with the proof mechanism.