pub struct AtomicInvariant<K, V, Pred> { /* private fields */ }Expand description
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.
An AtomicInvariant implements Sync
and may be shared between threads.
However, this means that an AtomicInvariant can be only opened for
the duration of a single sequentially consistent atomic operation.
Such operations are provided by our PAtomic library.
For an invariant object without this atomicity restriction,
see LocalInvariant, which gives up thread safety in exchange.
An AtomicInvariant consists of:
- A predicate specified via the
InvariantPredicatetype bound, that determines what valuesVmay be saved inside the invariant. - A constant
K, specified at construction type. The predicate function takes this constant as a parameter, so the constant allows users to dynamically configure the predicate function in a way that can’t be done at the type level. - A namespace. This is a bit of a technicality, and you can often just declare
it as an arbitrary integer with no issues. See the
open_local_invariant!documentation for more details.
The constant and namespace are specified at construction time (AtomicInvariant::new).
These values are fixed for the lifetime of the AtomicInvariant object.
To open the invariant and access the stored object V,
use the macro open_atomic_invariant!.
The AtomicInvariant API is an instance of the “invariant” method in Verus’s general philosophy on interior mutability.
Note: Rather than using AtomicInvariant directly, we generally recommend
using the atomic_ghost APIs.
Implementations§
Source§impl<K, V, Pred: InvariantPredicate<K, V>> AtomicInvariant<K, V, Pred>
impl<K, V, Pred: InvariantPredicate<K, V>> AtomicInvariant<K, V, Pred>
Sourcepub uninterp fn constant(&self) -> K
pub uninterp fn constant(&self) -> K
The constant specified upon the initialization of this AtomicInvariant.
Sourcepub open spec fn inv(&self, v: V) -> bool
pub open spec fn inv(&self, v: V) -> bool
{ Pred::inv(self.constant(), v) }Returns true if it is possible to store the value v into the AtomicInvariant.
This is equivalent to Pred::inv(self.constant(), v).
Sourcepub proof fn new(k: K, tracked v: V, ns: int) -> tracked i : AtomicInvariant<K, V, Pred>
pub proof fn new(k: K, tracked v: V, ns: int) -> tracked i : AtomicInvariant<K, V, Pred>
Pred::inv(k, v),i.constant() == k,i.namespace() == ns,Initialize a new AtomicInvariant with constant k. initial stored (tracked) value v,
and in the namespace ns.
Sourcepub proof fn into_inner(self) -> tracked v : V
pub proof fn into_inner(self) -> tracked v : V
self.inv(v),Destroys the AtomicInvariant, returning the tracked value contained within.