Struct vstd::invariant::LocalInvariant
source · pub struct LocalInvariant<K, V, Pred> { /* private fields */ }Expand description
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.
A LocalInvariant cannot be shared between threads
(that is, it does not implement Sync).
However, this means that a LocalInvariant can be opened for an indefinite length
of time, since there is no risk of a race with another thread.
For an invariant object with the opposite properties, see AtomicInvariant.
A LocalInvariant 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 (LocalInvariant::new).
These values are fixed for the lifetime of the LocalInvariant object.
To open the invariant and access the stored object V,
use the macro open_local_invariant!.
The LocalInvariant API is an instance of the “invariant” method in Verus’s general philosophy on interior mutability.
Implementations§
source§impl<K, V, Pred: InvariantPredicate<K, V>> LocalInvariant<K, V, Pred>
impl<K, V, Pred: InvariantPredicate<K, V>> LocalInvariant<K, V, Pred>
sourcepub spec fn constant(&self) -> K
pub spec fn constant(&self) -> K
The constant specified upon the initialization of this LocalInvariant.
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 LocalInvariant.
This is equivalent to Pred::inv(self.constant(), v).
sourcepub proof fn new(k: K, tracked v: V, ns: int) -> tracked i : LocalInvariant<K, V, Pred>
pub proof fn new(k: K, tracked v: V, ns: int) -> tracked i : LocalInvariant<K, V, Pred>
Pred::inv(k, v),i.constant() == k,i.namespace() == ns,Initialize a new LocalInvariant 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 LocalInvariant, returning the tracked value contained within.