Help My Verification Fails

Step one is always to make sure that your annotations are actually correct, and that the verifier has enough information to continue. Use some proof debugging to get insight into why your verification fails. Some steps require extra assertions or verification lemmas before a proof can be completed.

Sometimes, your annotations are actually correct, but the proof fails (non-deterministically). This is called proof brittleness; see Proof Brittleness and Countermeasures for more details.

Proof debugging

Often, you will not write a specification that immediately proves your code correct. In this section, we suggest some general proof debugging steps to help your progress. We suggest using the --watch flag (see VerCors usage tips).

Dafny, a similar verifier (but not based on separation logic), also has a useful section on proof debugging. Most tips are also applicable to VerCors.

Using assert, assume, inhale, and exhale

Using assert

Sometimes an obvious fact to you may not be obvious to VerCors. For example, the following fails verification.

 requires |a| == 1 && |b| == 1 && a <= b;
void same_elems(set<int> a, set<int> b) {
  int x = \choose(a); // Random element from a
  int y = \choose(b); // Random element from b
  assert x == y;
}

Often it is useful to keep adding assertions that you assume to be true, to see exactly which step is failing. Sometimes adding these will make verification go through, as in the following example.

 requires |a| == 1 && |b| == 1 && a <= b;
void same_elems(set<int> a, set<int> b) {
  int x = \choose(a);
  int y = \choose(b);
  assert x in a;
  assert x in b;
  assert |a - {x}| == 0;
  assert |b - {x}| == 0;
  assert x == y;
}

Apparently the line assert |b - {x}| == 0; was essential for VerCors to prove this. This has to do with how sets are encoded in this case. In general, adding assertions helps you better understand verification failures.

Different branches

Suppose you want to verify code with the following structure.

 requires A;
 ensures B;
void f(...) {
  if(...){
    ...
  } else if(...) {
    ...
  } else {
    ...
  }
}

And the ensures annotation fails, but you do not know for which branch. This can be discovered as follows.

 requires A;
 ensures B;
void f(...) {
  if(...){
    ...
    assert B; // First branch passes
  } else if(...) {
    ...
    assert B; // Second branch passes
  } else {
    ...
    assert B; // Throws a verification error, so apparently the error was here.
  }
}

Inserting assume false for faster answers

After an assume false is placed, all verification conditions afterward, within the same path, pass vacuously. Typically, this allows verification to be faster when building up a proof. For example:

 requires A;
 ensures B;
void f(...) {
  if(...){
    assume false; // This branch is skipped
    ...
  } else if(...) {
    assume false; // Just like this branch
    ...
  } else {
    ... // This branch is still verified.
  }
}

Checking whether code is reached

Sometimes, it might be unclear whether code is actually reached. It could be that the path conditions are formed in such a way that this is impossible. Placing assert false will only throw an assertion error if this point is reached.

 requires A;
 ensures B;
void f(...) {
  if(...){
    ...
  } else if(...) {
    assert false; // If this doesn't raise an assertion error, apparently this code is not reached.
    ...
  } else {
    ...
  }
}

Using inhale and exhale to model a complex problem

Sometimes a proof fails deep inside nested statements. It can then be easier to model the program using inhales and exhales to see what is going on, with less complex verification conditions. For example, in the following we build up an arbitrary array, which we can then modify.

void test(){
 int[] A;
 assume A != null && A.length == 32;
 inhale (\forall* int i; 0<=i && i<32; Perm({:A[i]:}, write));
 assume (\forall int i; 0<=i && i<32; {:A[i]:} > 0);
 loop_invariant... // For loop which modifies the array, you want to check
 for (int i=0; i<32;i++) {
   ....
 }
}

Verification lemmas

A verification lemma is a ghost/proof method whose main purpose is to establish a logical property used by other code.

A concrete example from this repository is the reachability proof in reachability.pvl:

// If pathExists(start, v) and u is a direct successor of v, then pathExists(start, u).
  requires ValidGraph(N, transitions);
  requires 0 <= start && start < N;
  requires 0 <= v && v < N;
  requires 0 <= u && u < N;
  requires pathExists(N, transitions, start, v);
  requires u in transitions[v];
  ensures pathExists(N, transitions, start, u);
  decreases;
void ExtendPath(int N, seq<set<int>> transitions, int start, int v, int u)
{
  if(start == u) {
  } else if(start == v) {
    seq<int> path = [v, u];
    assert isAPath(N, transitions, path);
  } else {
    seq<int> path :| isAPath(N, transitions, path) && path[0] == start && path[|path| - 1] == v;
    seq<int> newPath = path + [u];
    assert newPath[|path|] == u;
    assert newPath[|newPath| - 1] == u;
    assert isAPath(N, transitions, newPath);
  }
}

This lemma is then used by another lemma (ExtendPathPrefix) to lift the argument to all successors, and eventually by the algorithm proof.

Without these intermediate lemmas, it is often impossible to prove the intended properties.