opens_invariants

The opens_invariants clause may be applied to any proof or exec function.

This indicates the set of names of tracked invariants that may be opened by the function. At this time, it has three forms. See the documentation for open_local_invariant for more information about why Verus enforces these restrictions.

fn example()
    opens_invariants any
{
    // Any invariant may be opened here
}

or:

fn example()
    opens_invariants none
{
    // No invariant may be opened here
}

or:

fn example()
    opens_invariants [ $EXPR1, $EXPR2, ... ]
{
    // Only invariants with names in [ $EXPR1, $EXPR2, ... ] may be opened.
}

Defaults

For exec functions, the default is opens_invariants any.

For proof functions, the default is opens_invariants none.