Struct VerusCommutativeProof 

pub struct VerusCommutativeProof { /* private fields */ }

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

Created by the verus_proof_commutative_fold!, verus_proof_commutative_map!, verus_proof_commutative_filter!, and verus_proof_commutative_effect! macros, one per closure shape, each generating the precise obligation that makes reordering unobservable for that shape (final accumulator, output multiset, retained multiset, or captured state, respectively). The obligation is generated by the macro directly from the actual closure body — it symbolically executes the body in both orders (x then y, and y then x) 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.

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. This type only implements CommutativeProof, so it cannot be used to fulfill a different property (e.g. idempotent = ...).

Trait Implementations

impl<T, B: Boundedness> CommutativeProof<T, B> for VerusCommutativeProof

fn register_proof(&self, _expr: &Expr)

Registers the expression with the proof mechanism.

fn take_hook(&mut self) -> Option<OrderingHook<T, B>>

Takes the simulator ordering hook attached to this proof, if any.

impl Default for VerusCommutativeProof

fn default() -> Self

Returns the “default value” for a type.