Module invariant 

Resource invariants.

Resource invariants allow the use of a shared piece of data to be used in the invariant (see Protocol), but in return they impose a much more restricted access to the underlying data, as well as the use of Tokens.

Atomic invariants are used to specify concurrent operations.

Non-atomic invariants are used to specify thread-local operations.

Not to be confused with loop invariants or type invariants.

Example

Building a simplified Cell, that only asserts its content’s type invariant.

declare_namespace! { PERMCELL }

/// A cell that simply asserts its content's type invariant.
pub struct CellInv<T: Invariant> {
    data: PCell<T>,
    permission: Ghost<NonAtomicInvariant<PCellNAInv<T>>>,
}
impl<T: Invariant> Invariant for CellInv<T> {
    #[logic]
    fn invariant(self) -> bool {
        self.permission.namespace() == PERMCELL() && self.permission.public() == self.data.id()
    }
}

struct PCellNAInv<T>(Perm<PCell<T>>);
impl<T: Invariant> Protocol for PCellNAInv<T> {
    type Public = Id;

    #[logic]
    fn public(self) -> Id { self.0.id() }

    #[logic]
    fn protocol(self) -> bool { true }
}

impl<T: Invariant> CellInv<T> {
    #[requires(tokens.contains(PERMCELL()))]
    pub fn write(&self, x: T, tokens: Ghost<Tokens>) {
        ghost_let!(perm = &mut self.permission.open(tokens.into_inner()).inner.0);
        unsafe { *self.data.borrow_mut(perm) = x }
    }
}

Explicit tokens

For now, Tokens must be explicitely passed to open. We plan to relax this limitation at some point.

Macros

declare_namespace

Declare a new namespace.

Structs

AtomicInvariant

A shareable invariant for atomic accesses between threads.

AtomicInvariantSC

A shareable invariant for sequentially consistent accesses between threads.

Namespace

The type of namespaces of associated with non-atomic invariants.

NonAtomicInvariant

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

OpenGuard

Guard for NonAtomicInvariant::open.

OpenMutGuard

Guard for NonAtomicInvariant::open_mut.

Tokens

Invariant tokens.

Traits

Protocol

A variant of Invariant for use in AtomicInvariantSCs, AtomicInvariants and NonAtomicInvariants.