Module properties 

Types for reasoning about algebraic properties for Rust closures.

Macros

manual_proof

Fulfills a proof parameter by declaring a human-written justification for why the algebraic property (e.g. commutativity, idempotence) holds.

verus_proof_commutative_effect

Fulfills a commutative = ... 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 commutativity of the captured-state update.

verus_proof_commutative_filter

Fulfills a commutative = ... proof parameter for a filter predicate (shape |item| -> bool where item is received by reference) that may mutate a captured singleton reference (from Singleton::by_mut), with a Verus-checked proof of commutativity.

verus_proof_commutative_fold

Fulfills a commutative = ... proof parameter for an aggregation closure (fold / reduce, shape |acc, item| with acc: &mut A) with a Verus-checked proof of commutativity.

verus_proof_commutative_map

Fulfills a commutative = ... proof parameter for a map-like closure (shape |item| -> out, e.g. for map) that may mutate a captured singleton reference (from Singleton::by_mut), with a Verus-checked proof of commutativity.

Structs

AggFuncAlgebra

Algebraic properties for an aggregation function of type (T, &mut A) -> ().

ManualProof

A hand-written human proof of the correctness property.

SingletonMapFuncAlgebra

Algebraic properties for a singleton map function of type T -> U.

StreamMapFuncAlgebra

Algebraic properties for a stream map function of type T -> U.

VerusCommutativeProof

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

Enums

NotProved

Marks that the property is not proved.

Proved

Marks that the property is proven.

Traits

ApplyMonotoneKeyedStream

Marker trait identifying the boundedness of a singleton given a monotonicity property of an aggregation on a keyed stream.

ApplyMonotoneStream

Marker trait identifying the boundedness of a singleton given a monotonicity property of an aggregation on a stream.

ApplyOrderPreservingSingleton

Marker trait identifying the boundedness of a singleton after a map operation, given an order-preserving property.

CommutativeProof

A trait for proof mechanisms that can validate commutativity.

ConsistencyProof

A trait for proof mechanisms that can validate consistency of a collection.

IdempotentProof

A trait for proof mechanisms that can validate idempotence.

MonotoneProof

A trait for proof mechanisms that can validate monotonicity.

OrderPreservingProof

A trait for proof mechanisms that can validate order-preservation (monotonicity of a map function).

ValidCommutativityFor

Marker trait identifying that the commutativity property is valid for the given stream ordering.

ValidIdempotenceFor

Marker trait identifying that the idempotence property is valid for the given stream ordering.

ValidMutBorrowCommutativityFor

Marker trait for commutativity of closures that borrow their input (FnMut(&In) -> Out).

ValidMutBorrowIdempotenceFor

Marker trait for idempotence of closures that borrow their input (FnMut(&In) -> Out).

ValidMutCommutativityFor

Marker trait identifying that the commutativity property is valid for the given stream ordering.

ValidMutIdempotenceFor

Marker trait identifying that the idempotence property is valid for the given stream ordering.