A Complete Example

The following is a use case that uses most of the features presented in previous sections:

A Contract Implementing a Linked List

contract LinkedList {
  struct Element {
    bytes32 nextKey;
    uint256 exists;
  }

  struct List {
    bytes32 head;
    mapping(bytes32 => Element) elements;
  }

  List list;

  /**
   * @notice Inserts an element into a doubly linked list.
   * @param  key The key of the element to insert.
   * @param  afterKey The key of the element that comes before the
   *         element to insert. Or 0 to insert at the head.
   */
  function insertAfter(bytes32 key, bytes32 afterKey) public {
    require(key != bytes32(0), "Key must be defined");
    require(!contains(key), "Can't insert an existing element");
    require(afterKey != key, "Key cannot be the same as afterKey");

    Element storage element = list.elements[key];
    element.exists = 1;
    if (afterKey == 0) {
      element.nextKey = list.head; // ghost(2-vocab): updateSucc(key, list.head)
      list.head = key;
    } else {
      require(contains(afterKey),
          "If afterKey is defined, it must exist in the list");
      bytes32 tmp = list.elements[afterKey].nextKey;
      element.nextKey = tmp;
      list.elements[afterKey].nextKey = key;
    }
  }

  function getSucc(bytes32 key) public returns (bytes32) {
    return list.elements[key].nextKey;
  }

  function head() public returns (bytes32) {
    return list.head;
  }
  /**
   * @notice Returns whether or not a particular key is present in
   *         the sorted list.
   * @param  key The element key.
   * @return Whether or not the key is in the sorted list.
   */
  function contains(bytes32 key) public view returns (bool) {
    return list.elements[key].exists != 0;
  }
}

A Spec Using a Ghost to Compute Reachability

methods {
  insertAfter(bytes32, bytes32) envfree
  getSucc(bytes32) returns (bytes32) envfree
  contains(bytes32) returns (bool) envfree
  head() returns (bytes32) envfree
}

sort Node;

ghost toNode(bytes32) returns Node;
ghost reach(Node, Node) returns bool {
  axiom forall Node X. reach(X, X);
  axiom forall Node X. forall Node Y.
      reach(X, Y) && reach(Y, X) => X == Y;
  axiom forall Node X. forall Node Y. forall Node Z.
      reach(X, Y) && reach(Y, Z) => reach(X, Z);
  axiom forall Node X. forall Node Y. forall Node Z.
      reach(X, Y) && reach(X, Z) => (reach(Y, Z) || reach(Z,Y));
}

definition isSucc(Node a, Node b) returns bool =
    reach(a, b) && a != b &&
        (forall Node X. reach(a, X) && reach(X, b) => (a == X || b == X));

definition updateSucc(Node a, Node b) returns bool =
    forall Node X. forall Node Y. reach@new(X, Y) ==
        (X == Y ||
        (reach@old(X, Y) && !(reach@old(X, a) && a != Y &&
            reach@old(a, Y))) ||
        (reach@old(X, a) && reach@old(b, Y)));

hook Sstore (slot 0).(offset 32)[KEY bytes32 key].(offset 0)
    bytes32 newNextKey {
  havoc reach assuming updateSucc(toNode(key), toNode(newNextKey));
}

hook Sload bytes32 nextKey (slot 0).(offset 32)[KEY bytes32 key].(offset 0) {
  require isSucc(toNode(key), toNode(nextKey));
}

rule checkGetSucc {
  bytes32 key;
  bytes32 afterKey = getSucc(key);
  assert reach(toNode(key), toNode(afterKey));
}

// Rules for full correctness of API calls.
rule checkInsertHead {
  bytes32 key;
  bytes32 afterKey;
  bytes32 headKey = sinvoke head();
  require !reach(toNode(key), toNode(afterKey));
  // inserts at head
  require afterKey == 0;
  insertAfter@norevert(key, afterKey);
  assert reach(toNode(key), toNode(headKey));
}

rule checkInsertSuccessor {
  bytes32 key;
  bytes32 afterKey;
  require !reach(toNode(afterKey), toNode(key));
  // do not insert at head
  require afterKey != 0;
  insertAfter@norevert(key, afterKey);
  assert reach(toNode(afterKey), toNode(key));
}

rule checkInsert {
  bytes32 key;
  bytes32 afterKey;
  bytes32 randoBoi;
  bytes32 oldHeadKey = head@norevert();
  require reach(toNode(oldHeadKey), toNode(randoBoi));
  // this could be replaced by a hook, but we need to be able to
  // put invokes in hooks for that to work
  require contains(key) <=> reach(toNode(oldHeadKey), toNode(key));
  require contains(afterKey) <=> reach(toNode(oldHeadKey), toNode(afterKey));
  insertAfter@norevert(key, afterKey);    bytes32 newHeadKey = head@norevert();
  assert reach(toNode(newHeadKey), toNode(randoBoi));
}