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 self, tokens: Tokens<'a>, ) -> Guarded<&'a mut T, OpenGuard<T>>

Open the invariant to get the data stored inside.

The returned borrow satisfies the protocol on T. This protocol must be re-established before this borrow ends, with the same public value.

Notes on ghost_let

The Guarded type can assert its type invariant at inconvenient times. To work around this, it is often desirable to use a ghost_let to extract the inner borrow, and be able to freely break the protocol during its lifetime:

use creusot_std::{
    ghost::invariant::{NonAtomicInvariant, Protocol, Tokens, declare_namespace},
    prelude::*,
};
struct Gt0(i32);
impl Protocol for Gt0 {
    type Public = ();
    #[logic] fn public(self) {}
    #[logic] fn protocol(self) -> bool { self.0 > 0i32 }
}

declare_namespace! { NS }

#[requires(tokens.contains(NS()))]
fn foo(tokens: Ghost<Tokens>) {
    let inv = NonAtomicInvariant::new(ghost!(Gt0(1i32)), snapshot!(NS()));
    // ...
    ghost_let!(mut gt = &mut *inv.open(tokens.into_inner()).inner);

    ghost! { gt.0 = -1 };
    // ... maybe do some non-ghost operations here ...
    ghost! { gt.0 = 2 };
}

If we were using the guard variable directly, the type invariant (and thus the protocol) would be asserted at the end of each ghost! { gt.0 = ... } block, and the first would fail.

requires

tokens.contains(self.namespace())

ensures

result.guard().0 == self.public()

ghost

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(&mut self) -> Guarded<&mut T, OpenMutGuard>

Open the invariant to get the data stored inside. The protocol must be restored by the end of the returned borrow’s lifetime.

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

See Self::open for a version that only need a shared borrow, but cannot change the public part.

ghost

ensures

result.inner.public() == self.public()

ensures

(^result.inner).public() == (^self).public()

ensures

(^self).namespace() == (*self).namespace()

Trait Implementations

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