Struct NonAtomicInvariant 

pub struct NonAtomicInvariant<T: Protocol>(/* private fields */);

A ghost structure, that holds a piece of data (T) together with an protocol.

Note

NonAtomicInvariant is not Sync, and is invariant in the underlying data.

• It is not Sync precisely because it is non-atomic, so access to the data is unsynchronized.
• It is invariant because it gives access to a mutable borrow of this data.

If you need to share an invariant across threads, consider AtomicInvariantSC or AtomicInvariant.

Implementations

impl<T: Protocol> NonAtomicInvariant<T>

pub fn new(value: Ghost<T>, namespace: Snapshot<Namespace>) -> Ghost<Self>

Construct a NonAtomicInvariant

Parameters

• value: the actual data contained in the invariant. Use Self::open to access it. Also called the ‘private’ part of the invariant.
• namespace: the namespace of the invariant. This is required to avoid opening the same invariant twice.

requires

value.protocol()

ensures

result.public() == value.public()

ensures

result.namespace() == *namespace

ghost

pub fn into_inner(self) -> T

Gives the actual invariant held by the NonAtomicInvariant.

ensures

result.public() == self.public() && result.protocol()

ghost

pub fn namespace(self) -> Namespace

Get the namespace associated with this invariant.

logic(opaque)

pub fn public(self) -> T::Public

Get the ‘public’ part of this invariant.

logic(opaque)

pub fn open<'a, A>( this: Ghost<&'a Self>, tokens: Ghost<Tokens<'a>>, f: impl FnOnce(Ghost<&'a mut T>) -> A, ) -> A

Open the invariant to get the data stored inside.

This will call the closure f with the inner data. You must restore the contained Protocol before returning from the closure.

requires

tokens.contains(this.namespace())

requires

forall<t: Ghost<&mut T>> t.public() == this.public() && t.protocol() && inv(t) ==>
    f.precondition((t,)) &&
    // f must restore the invariant
    (forall<res: A> f.postcondition_once((t,), res) ==> (^t).public() == this.public() && (^t).protocol())

ensures

exists<t: Ghost<&mut T>> t.public() == this.public() && t.protocol() && inv(t) &&
    f.postcondition_once((t,), result)

pub fn open_const<'a>(&'a self, tokens: &'a Tokens<'_>) -> &'a T

Open the invariant to get the data stored inside, immutably. This allows reentrant access to the invariant.

requires

tokens.contains(self.namespace())

ensures

result.public() == self.public() && result.protocol()

ghost

pub fn open_mut<'a, A>( this: Ghost<&'a mut Self>, f: impl FnOnce(Ghost<&'a mut T>) -> A, ) -> A

Open the invariant to get the data stored inside.

See Self::open.

This requires a mutable borrow on the invariant, but in exchange, you are allowed to change the public part of the invariant.

ghost

requires

forall<t: Ghost<&mut T>> t.protocol() && t.public() == this.public() && inv(t) ==>
    f.precondition((t,)) &&
    (forall<res: A> f.postcondition_once((t,), res) ==> (^t).protocol())

ensures

exists<t: Ghost<&mut T>> t.protocol() && t.public() == this.public() && inv(t) &&
    f.postcondition_once((t,), result) && (^this).public() == (^t).public()

ensures

this.namespace() == (^this).namespace()

Trait Implementations

impl<T: Protocol> Send for NonAtomicInvariant<T>