Macro vstd::open_local_invariant

macro_rules! open_local_invariant {
    [$($tail:tt)*] => { ... };
}

Macro used to temporarily “open” a LocalInvariant object, obtaining the stored value within.

Usage

The form of the macro looks like,

open_local_invariant($inv => $id => {
    // Inner scope
});

The operation of opening an invariant is a ghost one; however, the inner code block may contain arbitrary exec-mode code. The invariant remains “open” for the duration of the inner code block, and it is closed again of the end of the block.

The $inv parameter should be an expression of type &LocalInvariant<K, V, Pred>, the invariant object to be opened. The $id is an identifier which is bound within the code block as a mut variable of type V. This gives the user ownership over the V value, which they may manipulate freely within the code block. At the end of the code block, the variable $id is consumed.

The obtained object v: V, will satisfy the LocalInvariant’s invariant predicate $inv.inv(v). Furthermore, the user must prove that this invariant still holds at the end. In other words, the macro usage is roughly equivalent to the following:

{
    let $id: V = /* an arbitrary value */;
    assume($inv.inv($id));
    /* user code block here */
    assert($inv.inv($id));
    consume($id);
}

Avoiding Reentrancy

Verus adds additional checks to ensure that an invariant is never opened more than once at the same time. For example, suppose that you attempt to nest the use of open_invariant, supplying the same argument inv to each:

open_local_invariant(inv => id1 => {
    open_local_invariant(inv => id2 => {
    });
});

In this situation, Verus would produce an error:

error: possible invariant collision
  |
  |   open_atomic_invariant!(&inv => id1 => {
  |                           ^ this invariant
  |       open_atomic_invariant!(&inv => id2 => {
  |                               ^ might be the same as this invariant
  ...
  |       }
  |   }

When generating these conditions, Verus compares invariants via their namespace() values. An invariant’s namespace (represented simply as an integer) is specified upon the call to LocalInvariant::new. If you have the need to open multiple invariants at once, make sure to given them different namespaces.

So that Verus can ensure that there are no nested invariant accesses across function boundaries, every proof and exec function has, as part of its specification, the set of invariant namespaces that it might open.

UNDER CONSTRUCTION: right now the forms of these specifications are somewhat limited and we expect to expand them.

The invariant set of a function can be specified by putting either opens_invariants none or opens_invariants any in the function signature. The default for an exec-mode function is to open any, while the default for a proof-mode function is to open none.

It’s not legal to use open_local_invariant! in proof mode. In proof mode, you need to use open_local_invariant_in_proof! instead. This takes one extra parameter, an open-invariant credit, which you can get by calling create_open_invariant_credit() before you enter proof mode.

Example

TODO fill this in

More Examples

TODO fill this in