Module local_invariant 

Define local invariants.

Local invariants are not the same as type invariants: they 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<LocalInvariant<PermCellLocalInv<T>>>,
}
impl<T: Invariant> Invariant for CellInv<T> {
    #[logic]
    fn invariant(self) -> bool {
        self.permission.namespace() == PERMCELL() && self.permission.public() == self.data.id()
    }
}

struct PermCellLocalInv<T>(PermCellOwn<T>);
impl<T: Invariant> Protocol for PermCellLocalInv<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>) {
        LocalInvariant::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

LocalInvariant

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

Namespace

The type of namespaces of associated with local invariants.

Tokens

Invariant tokens.

Traits

LocalInvariantExt

Define method call syntax for LocalInvariant::open.

Protocol

A variant of Invariant for use in LocalInvariants.