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

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.

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