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.

MapFuncAlgebra

Algebraic properties for a 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.

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.