Magic Wands

The handling of magic wands is non-trivial, so this chapter takes a closer look at that. For further reading, see e.g. "Witnessing the elimination of magic wands". Blom, S.; and Huisman, M. STTT, 17(6): 757–781. 2015.

Also take a look at the Viper tutorial for wands: http://viper.ethz.ch/tutorial/?page=1&section=#magic-wands

What are Magic Wands?

The "Magic Wand" or separating implication is a connective in separation logic using the symbol -*. It represents a part of a resource (see "Predicates") or "resource with a hole": A -* B means "if you give me an A, I can give you a B in return". Thus, it is similar to a logical implication A ==> B; however, it consumes the A when it is exchanged for a B.

A common use case is if you have a predicate defining a recursive data structure like a linked list or a binary tree, and you take a part of that data structure to reason about explicitly, like a sub-tree. You can use the recursive predicate to reason about the sub-tree, but it is more difficult to reason about the remainder of the original tree: Since you took out the sub-tree and have explicit permission for it, the recursive predicate for the whole tree can no longer have the permission for that part, so it would have to stop recursing at a certain point. With a wand, you can resolve this: For a tree T with left sub-tree L and right sub-tree R, and a recursive predicate Tree(x), you can split Tree(T) into Tree(L) ** (Tree(L)-*Tree(T)). So you have the explicit resource for the left sub-tree, and a wand such that if you join the sub-tree back into it, you get the predicate for the whole tree back. This joining is called applying the wand.

Syntax in VerCors

We will use the following binary tree as example:

final class Tree {
  int value;
  int priority;
  Tree left;
  Tree right;

  /*@
  resource tree() = Perm(value, write) ** Perm(priority, write) ** Perm(left, write) ** Perm(right, write) 
    ** (left != null ==> left.tree()) ** (right != null ==> right.tree());

  requires t.tree();
  static pure boolean sorted(Tree t) 
  = t != null ==> \unfolding t.tree() \in 
    (t.left != null ==> sorted(t.left) && \unfolding t.left.tree() \in t.priority >= t.left.priority) 
    && (t.right!= null ==> sorted(t.right) && \unfolding t.right.tree() \in t.priority >= t.right.priority);
  @*/

So a Tree contains a data item value, a priority and two references to the sub-trees; the tree resource contains write permissions for all those fields, as well as recursive permissions for the sub-trees; and the sorted function ensures that the priority in the root node is the largest in the Tree (like in a priority queue).

Creating a Wand

To create a wand, use the keyword create {...}. Inside the curly braces, you have to provide the necessary information to create the wand:

You need to explicitly specify which resources from the current context should be folded into the wand. The keyword for this is use. Note that, like with folding a normal predicated, any permissions folded into the wand are no longer available in the environment. You can also use boolean facts from the current context, e.g. use a==b;.

When creating a wand A-*B, you need to describe how exactly to merge A with the content of the wand to obtain B. For example, A may contain permissions for the left sub-tree and the wand those for the right sub-tree, and to get the full tree, you need to perform a fold. All necessary permissions and boolean facts for such a merger must be provided via use.

The final statement within the curly braces of create has to be qed A-*B;, with A-*B being replaced by the wand you created.

Note that the wand operator -* has the precedence like an implication, thus it is less binding than the separating conjunct ** and boolean connectives like &&.

/*@
requires t != null;
requires t.tree();
requires \unfolding t.tree() \in t.left != null;
ensures \result != null ** \result.tree();
ensures \result.tree() -* t.tree();
@*/
static Tree get_left(Tree t) {
  //@ unfold t.tree();
  Tree res = t.left;
  /*@
  create {
    use Perm(t.value, write) ** Perm(t.priority, write) ** Perm(t.left, write) ** Perm(t.right, write);
    use t.right != null ==> t.right.tree();
    use res == t.left;
    fold t.tree();
    qed res.tree() -* t.tree();
  }
  @*/
  return res;
}

Notice how in the example, all the permissions necessary for folding tree(t) are provided with use, except the part that is in the premise of the wand, tree(t.left). If we had provided that as well, it would have become part of the wand, rather than being the "missing piece", and the first post-condition ensures tree(\result) would have failed for lack of permission (since this permission is bundled into the wand, and no longer directly available). Additionally, we had to provide the fact that res is the left sub-tree of t, so that fold tree(t) knows that the premise of the wand fits into the missing part of the predicate.

Applying a Wand

To combine the "missing piece" with the wand and obtain the full resource, use the keyword apply. Since we already specified how the merging works when we created the wand, no further logic is needed now:

/*@
context t != null;
context t.tree();
requires \unfolding t.tree() \in t.left != null;
@*/
static boolean check_left_priority(Tree t, int max_priority) {
  Tree left = get_left(t);
  // now we have tree(left) and a wand tree(left) -* tree(t)
  //@ unfold left.tree();
  boolean res = left.priority <= max_priority;
  //@ fold left.tree();
  //@ apply left.tree() -* t.tree();
  // now left.tree() is no longer directly available, but t.tree() is back
  return res;
}

More Complex Expressions

Sometimes, we may want to reason about the things contained in a wand; for example we decompose a sorted tree, and want to say it will be sorted again after the merger. However, as long as tree(t) is split into the sub-tree and the wand, we cannot call sorted(t) as it needs the full predicate tree(t). But simply ignoring the sortedness when splitting and later merging again would mean that we can no longer make any assertions about sortedness afterwards. As a solution, we encode the property into the wand, by adding conjuncts to the premise and antecedence of the wand: A**B -* C**D. We can only apply such a wand if we hold the permissions of A and the properties in B hold. This stricter requirement is rewarded with the fact that we will get both the permissions in C and the properties of D after applying the wand.

Note that VerCors currently only allows method calls as conjuncts in wands, so properties like an equality a==b must be wrapped in a function in order to be used.

/*@
requires t != null ** t.tree();
static boolean wand_helper(Tree t, int max_prio)
  = \unfolding t.tree() \in t.priority <= max_prio;
@*/

/*@
yields int root_prio;
requires t != null;
requires t.tree() ** sorted(t);
requires \unfolding t.tree() \in t.left != null;
ensures \result != null ** \result.tree();
ensures sorted(\result) && wand_helper(\result, root_prio);
ensures \result.tree() ** sorted(\result) ** wand_helper(\result, root_prio) 
        -* 
        t.tree() ** sorted(t);
@*/
static Tree get_left_sorted(Tree t) {
  //@ unfold t.tree();
  //@ ghost root_prio = t.priority;
  Tree res = t.left;
  /*@
  create {
    // necessary parts for t.tree()
    use Perm(t.value, write) ** Perm(t.priority, write) ** Perm(t.left, write) ** Perm(t.right, write);
    use t.right != null ==> t.right.tree();
    use res == t.left;
    // necessary parts for t.sorted()
    use res != null;
    use t.priority == root_prio;
    use t.right != null ==> sorted(t.right) && \unfolding t.right.tree() \in t.priority >= t.right.priority;
    // assemble parts
    fold t.tree();
    qed res.tree() ** sorted(res) ** wand_helper(res, root_prio) 
        -* 
        t.tree() ** sorted(t);
  }
  @*/
  return res;
}

/*@
context t != null;
context t.tree() ** sorted(t);
requires \unfolding t.tree() \in t.left != null;
@*/
static boolean check_left_priority_sorted(Tree t, int max_priority) {
  //@ ghost int root_prio;
  Tree left = get_left_sorted(t) /*@ then { root_prio = root_prio; } @*/;
  // now we have left.tree(), sorted(left) and wand_helper(left, root_prio), as well as the wand
  //@ unfold left.tree();
  boolean res = left.priority <= max_priority;
  //@ fold left.tree();
  //@ apply (left.tree() ** sorted(left) ** wand_helper(left, root_prio)) -* (t.tree() ** sorted(t));
  // now left.tree() is no longer directly available, but t.tree() is back and sorted
  return res;
}

Now, when creating the wand, we need to use additional information in order to be able to ensure sortedness after the merger: The condition for the right side can simply be provided. The condition for the left side is part of the premise of the wand (in particular sorted). The comparison between the priority of the root and the priority of the left node is wrapped into a helper function, wand_helper. Since the premise of the wand contains no permissions for t.priority, we use a ghost variable root_prio to communicate that value.

Applying the wand is nearly as simple as before. However, we again need to use the ghost variable root_prio as an intermediate storage for the priority of t.

You see that adding such additional constraints about the wand's resources is possible, but can carry significant overhead of helper functions, use statements, etc.