Proof Brittleness and Countermeasures

Certain proofs are too complex for the underlying tools and SMT solvers. This causes proof brittleness, i.e. proofs that (non-deterministically) fail even when the annotations are correct.

This page gives a practical overview of patterns we know that can cause proof brittleness, and some counter measures to these. The counter measures are explained in more detail on their own pages:

• Frames & Extract
• Opaque Functions
• Unique Types

Causes of Proof Brittleness

In these cases, we have often observed proof brittleness:

• Programs with many complex quantifiers
• Programs with many arrays, which have their permissions specified by quantifiers
• Big monolithic functions
• Non-linear arithmetic

The underlying cause is that we rely on automated SMT solvers, which cannot solve every possible proof query efficiently. In practice, the more complex the task given to an SMT solver, the more brittle the proof can become.

If a proof fails at different error lines, suddenly fails after a small unrelated change, or fails under tighter time/resource settings, you are probably dealing with proof brittleness.

Cause: Complex Quantifiers

VerCors requires quantifiers to have triggers, so that the underlying SMT solver can decide when to instantiate a quantifier. However, when a suboptimal trigger is supplied, it can happen that:

• The trigger is too restrictive, causing the quantifier not to be instantiated at all.
• The quantifier causes a matching loop, which can time out verification as too many quantifiers are instantiated.

We recommend reading the quantifier section of the Viper Tutorial for more details.

Furthermore, we recommend using the SmtScope tool to understand and debug quantifier instantiations produced by the SMT solver. VerCors can produce the correct output to be analysed by SmtScope by passing the following arguments:

vct ./file.pvl \
  --backend-option --numberOfParallelVerifiers=1 \
  --backend-option --proverArgs="trace=true proof=true"

Or VerCors can dump the .smt2 file it gives to Z3:

vct ./file.pvl \
  --backend-option --numberOfParallelVerifiers=1 \
  --backend-option --proverLogFile="query"

On which Z3 can be run with:

z3 trace=true proof=true trace-file-name=foo.log ./query-01.smt2

Cause: Many Arrays & Quantifier Permissions

Typically for arrays, the permissions are specified by permission quantifiers (or Iterated Separating Conjunctions). Having too many of these can cause verification time to blow up. This occurs even when only a few arrays are present, but the program to be verified is complex, such as with many GPU kernels.

In general, we suggest using read-only data types, such as sequences, whenever possible. In PVL files this is often possible to model. For GPU or C files, read the section about Unique Types for alternatives.

More details about this issue can be found in the paper Scalable Deductive Verification of Data-Level Parallel Programs.

Cause: Big Monolithic Functions

Code with many different execution paths and high complexity can cause the underlying verifiers to struggle. Often, reducing complexity by splitting code into smaller functions helps the verifier. With the extract functionality, code can also be extracted and verified in isolation. In essence, this has the same effect as refactoring code into smaller functions; however, this is only done for verification purposes, and the actually executed code is not aware of it. Refer to the section about Frames & Extract for more details.

Sometimes, the annotations themselves might impose overhead. It can be smart to encode the annotations in pure functions, and use the opaque keyword to hide the body of the function from the verification scope. See the section on Opaque Functions for more details.

Cause: Non-linear arithmetic

Suppose we want to prove the following fact[^1] about integers.

  requires x >=0 && y >= 0 && x < m && y < n;
void f(int x, int y, int m, int n) {
  assert n * x + y < m * n;
}

Solving non-linear arithmetic is undecidable in general, and asking this fact to the underlying Z3 SMT solver may cause a timeout. Luckily, Z3 has a dedicated non-linear solver, which can be enabled by adding the following flag to VerCors:

--prover-config:smt.arith.solver=6

When dealing with non-linearity, we suggest using frame and extract on code blocks with non-linear statements.

Additionally, facts that cannot be proven in VerCors can be proven externally and then brought in as an axiom or assumption. Structurally, one could for instance define the following abstract pure function, and call this whenever the specific information is needed.

  // Proven by Lean with the Nat.mul_add_lt_mul_of_lt_of_lt lemma
  requires x >=0 && y >= 0 && x < m && y < n;
  ensures n * x + y < m * n;
pure void mul_add_lt_mul_of_lt_of_lt(int x, int y, int m, int n);

[^1]: See the Lean lemma which proves this.