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.

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.

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.