Module vstd::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.

Traits

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

Functions

• create_open_invariant_credit