LocalInvariant

vstd::invariant

Struct 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 InvariantPredicate type bound, that determines what values V may 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> LocalInvariant<K, V, Pred>

Source

pub uninterp fn constant(&self) -> K

The constant specified upon the initialization of this LocalInvariant.

Source

pub uninterp fn namespace(&self) -> int

Namespace the invariant was declared in.

Source§

impl<K, V, Pred: InvariantPredicate<K, V>> LocalInvariant<K, V, Pred>

Source

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).

Source

pub proof fn new(k: K, tracked v: V, ns: int) -> tracked i : LocalInvariant<K, V, Pred>

requires
Pred::inv(k, v),
ensures
i.constant() == k,
i.namespace() == ns,

Initialize a new LocalInvariant with constant k. initial stored (tracked) value v, and in the namespace ns.

Source

pub proof fn into_inner(self) -> tracked v : V

ensures
self.inv(v),

Destroys the LocalInvariant, returning the tracked value contained within.

Trait Implementations§

Source§

impl<K, V, Pred> !Sync for LocalInvariant<K, V, Pred>

Auto Trait Implementations§

§

impl<K, V, Pred> Freeze for LocalInvariant<K, V, Pred>

§

impl<K, V, Pred> RefUnwindSafe for LocalInvariant<K, V, Pred>
where V: RefUnwindSafe, K: RefUnwindSafe, Pred: RefUnwindSafe,

§

impl<K, V, Pred> Send for LocalInvariant<K, V, Pred>
where V: Send,

§

impl<K, V, Pred> Unpin for LocalInvariant<K, V, Pred>
where V: Unpin, K: Unpin, Pred: Unpin,

§

impl<K, V, Pred> UnwindSafe for LocalInvariant<K, V, Pred>
where V: UnwindSafe + RefUnwindSafe, K: UnwindSafe, Pred: UnwindSafe,

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

Source§

impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: From<T>,

Source§

exec fn obeys_from_spec() -> bool

Source§

exec fn from_spec(v: T) -> VERUS_SPEC__A

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

Source§

impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: Into<T>,

Source§

exec fn obeys_into_spec() -> bool

Source§

exec fn into_spec(self) -> T

Source§

impl<T, U> IntoSpecImpl<U> for T
where U: From<T>,

Source§

open spec fn obeys_into_spec() -> bool

{ <U as FromSpec<Self>>::obeys_from_spec() }
Source§

open spec fn into_spec(self) -> U

{ U::from_spec(self) }
Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
Source§

impl<T, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryFrom<T>,

Source§

exec fn obeys_try_from_spec() -> bool

Source§

exec fn try_from_spec( v: T, ) -> Result<VERUS_SPEC__A, <VERUS_SPEC__A as TryFrom<T>>::Error>

Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.
Source§

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryInto<T>,

Source§

exec fn obeys_try_into_spec() -> bool

Source§

exec fn try_into_spec(self) -> Result<T, <VERUS_SPEC__A as TryInto<T>>::Error>

Source§

impl<T, U> TryIntoSpecImpl<U> for T
where U: TryFrom<T>,

Source§

open spec fn obeys_try_into_spec() -> bool

{ <U as TryFromSpec<Self>>::obeys_try_from_spec() }
Source§

open spec fn try_into_spec(self) -> Result<U, <U as TryFrom<T>>::Error>

{ <U as TryFromSpec<Self>>::try_from_spec(self) }