Syntax Update: Ghost Variables and Ghost Mappings
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 .
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;
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.