Module invariant 

Define atomic and non-atomic invariants.

Atomic invariants are used to specify concurrent operations.

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

These invariants are not the same as type 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.

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: PermCell<T>,
    permission: Ghost<NonAtomicInvariant<PermCellNAInv<T>>>,
}
impl<T: Invariant> Invariant for CellInv<T> {
    #[logic]
    fn invariant(self) -> bool {
        self.permission.namespace() == PERMCELL() && self.permission.public() == self.data.id()
    }
}

struct PermCellNAInv<T>(Box<Perm<PermCell<T>>>);
impl<T: Invariant> Protocol for PermCellNAInv<T> {
    type Public = Id;

    #[logic]
    fn protocol(self, id: Id) -> bool {
        self.0.id() == id
    }
}

impl<T: Invariant> CellInv<T> {
    #[requires(tokens.contains(PERMCELL()))]
    pub fn write(&self, x: T, tokens: Ghost<Tokens>) {
        NonAtomicInvariant::open(self.permission.borrow(), tokens, move |perm| unsafe {
            *self.data.borrow_mut(ghost!(&mut perm.into_inner().0)) = 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

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.

Tokens

Invariant tokens.

Traits

NonAtomicInvariantExt

Define method call syntax for NonAtomicInvariant::open.

Protocol

A variant of Invariant for use in AtomicInvariants and NonAtomicInvariants.