Macro vstd::invariant::open_local_invariant
source · macro_rules! open_local_invariant { [$($tail:tt)*] => { ... }; }
Expand description
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