Module invariant 

Macros

open_atomic_invariant

Macro used to temporarily “open” an AtomicInvariant object, obtaining the stored value within.

open_atomic_invariant_in_proof

open_local_invariant

Macro used to temporarily “open” a LocalInvariant object, obtaining the stored value within.

open_local_invariant_in_proof

Structs

AtomicInvariant

An AtomicInvariant is a ghost object that provides “interior mutability” for ghost objects, specifically, for tracked ghost objects. A reference &AtomicInvariant may be shared between clients. A client holding such a reference may open the invariant to obtain ghost ownership of v1: V, and then close the invariant by returning ghost ownership of a (potentially) different object v2: V.

LocalInvariant

A LocalInvariant is a ghost object that provides “interior mutability” for ghost objects, specifically, for tracked ghost objects. A reference &LocalInvariant may be shared between clients. A client holding such a reference may open the invariant to obtain ghost ownership of v1: V, and then close the invariant by returning ghost ownership of a (potentially) different object v2: V.

OpenInvariantCredit

Traits

InvariantPredicate

Trait used to specify an invariant predicate for LocalInvariant and AtomicInvariant.

Functions

create_open_invariant_credit