Syntax Update: Ghost Variables and Ghost Mappings

Variable-style declarations

CVL now allows for top-level declarations of ghosts that follow the common scheme for variable declarations. Ghost variables can be scalars (uint etc.) or mappings.

ghost uint myGhost;
ghost mapping(uint => uint) myGhostMapping;

Nested (multi-dimensional) ghost mappings are supported, too.

ghost mapping(uint => mapping(uint => uint)) myTwoDimensionalGhostMapping

Background: Semantically there is no difference between the new variable-style and the old function-style declarations. I.e., the declaration ghost uint myGhost creates the same semantic object as the declaration ghost myGhost() returns uint .

Variable-style access

Ghosts that have been declared as scalar variables are accessed like normal variables, e.g. :

y = myGhost;
myGhost = x;

Ghosts that have been declared as mapping variables are accessed like normal mappings:

y = myGhostMapping[i];
myGhostMapping[j] = x;

Mapping-style updates

The update syntax myGhostMapping[j] = x can replace many uses of the havoc .. assuming .. syntax.

In particular, the old syntax

havoc myGhostMapping assuming forall k. k = j ? 
      myGhostMapping@new[k] = x : 
      myGhostMapping@new[k] = myGhostMapping@old[k];

can be replaced by

myGhostMapping[j] = x;

Note that this syntax avoids the quantifiers also internally, so it is strongly recommended to use it if possible.