Quantifier Grounding

Quantified expressions are a very powerful tool for writing specifications, but they can also lead to incredibly long running times. For this reason, the Prover uses an approximation called “grounding”.

It is not possible to ground every expression perfectly. While grounding is sound (i.e. it will not allow a rule to be verified if it is not true), there are cases where it may generate counterexamples even for rules that should pass. For example, a counterexample may not obey a require statement that contains a quantifier.

You can prevent spurious counterexamples by turning off grounding (by passing --prover_args '-smt_groundQuantifiers false'), but without grounding the Prover may run considerably slower, and is likely to time out.

The remainder of this document explains grounding in more detail, and lists the specific kinds of quantified expressions that may lead to spurious counterexamples. We also include some suggestions for rewriting your quantified statements to avoid spurious counterexamples.

How grounding works

Quantifier grounding transforms a quantified statement into a series of non-quantified statements. For example, suppose a specification contains the following ghost axiom:

ghost f(uint x) returns (mathint) {
    init_state axiom forall uint x . f(x) == 0
}

This statement logically says that f(0) == 0 and f(1) == 0 and f(2) == 0 and so on. In practice, however, the verification may only make use of a small finite number of these facts. Grounding is the process of automatically replacing the forall statement with the specific unquantified statements that are necessary.

For example, if the program and specification only ever access f(2), f(9), f(y+3), and f(z), then the axiom above would be automatically replaced with:

ghost f(uint x) returns (mathint) {
    init_state axiom f(2)   == 0;
    init_state axiom f(9)   == 0;
    init_state axiom f(y+3) == 0;
    init_state axiom f(z)   == 0;
}

The Prover will also ground more complex quantified expressions, and will ground them anywhere that you can write a quantified statement (e.g. assert and require statements, ghost axioms, and invariants). Grounding also works with exists quantifiers.

Limitations on grounding

In some cases, there is an easy way to rewrite your expression with fewer quantifiers. For example, the following quantified statement requires that f(x) is always odd, but it is written in a way that violates one of the restrictions on quantifiers:

require forall uint x . forall mathint y . f(x) != 2 * y;

However, there is a much simpler way to require that f(x) is odd by using %:

require forall uint x . f(x) % 2 == 1;

This rewritten statement obeys the rules listed below, and therefore will not produce any spurious counterexamples.

The remainder of this section describes specific cases where the Prover cannot ground quantified statements, and gives advice on how to work around those limitations.

Alternating Quantifiers

Alternating quantifiers (those containing forall followed by exist or vice-versa) complicate the process of grounding, so there are limitations to what statements you can write and which of them are grounded.

In most contexts, you may not have a forall expression contained inside of an exists statement. For example, this is allowed:

assert forall address x . forall uint y . exists uint z . exists uint w . e(x,y,z,w);

but this is disallowed:

assert forall address x . exists address y . exists address z . forall address w . e(x,y,z,w);

In the latter case, the forall address w is contained inside the exists address z.

Logical negations and require statements reverse the rules for forall and exists statements: in those contexts, you cannot nest an exists expression inside of a forall statement. Including another negation will again reverse the rules. For example, the following are allowed:

require    exists address x . forall uint y . e(x,y);
assert   !(exists address x . forall uint y . e(x,y));
require  !(forall address x . exists uint y . e(x,y));
assert !(!(forall address x . exists uint y . e(x,y)));

but these are disallowed:

require  forall address x . exists uint y . e(x,y);
assert !(forall address x . exists uint y . e(x,y));

One common way to work around these limitations is by replacing exists expressions with concrete expressions that produce the values that should exist.

For example, suppose your contract function always returned twice its input:

function f(uint x) external returns(uint) { return 2 * x; }

You might like to prove that if x is positive, then it’s possible for f to output something smaller than f(x):

assert forall uint x . (x > 0) => (exists uint y . f(y) < f(x));

This is clearly true; for example f(x - 1) is always smaller than f(x), as is f(0). However, to work around the nested quantifier restriction, we have to help the Prover find the correct value for y. We could replace this statement with either of the following two:

assert forall uint x . (x > 0) => f(0) < f(x);
assert forall uint x . (x > 0) => f(x-1) < f(x);

Recursion

Quantified statements that relate a function with itself on two different inputs may give incorrect counterexamples. For example, the following forall statement refers to f twice:

rule recursiveQuantifier {
    require forall uint x . f(x) > f(x-1);
    assert f(8) > f(6);
}

Although we can see that the assertion must be true, we would need to combine the statements f(8) > f(7) and f(7) > f(6) to prove it, and the grounding mechanism is unable to do this.

In these cases, you may see a counterexample that doesn’t satisfy the require statement; in this case the best option is to disable grounding with --prover_args '-smt_groundQuantifiers false'.

Variables must be arguments

In order for grounding to work, every variable appearing in a quantified statement must be used at least once as an argument to a ghost or contract function. For example, neither of the following examples are allowed:

require forall mathint x . x * 2 != y;
require forall uint x . forall mathint y . f(x) != 2 * y;

In the first example, x is not used as an argument to a function, while in the second case, y is not.

Although you are allowed to call functions on complicated expressions that use quantified variables, doing so may produce spurious counterexamples. For example, the following is allowed, but is likely to produce spurious counterexamples (because x itself is not an argument to a function):

require forall uint x . f(2 * x) == 0;

This particular example requires that all even inputs to f produce 0 as output; it could be rewritten as follows:

require forall uint y . (y % 2 == 0) => f(y) == 0;

If you use a quantified variable in an argument to two different functions, you may produce spurious counterexamples. For example:

require forall uint x . f(x) <= g(x+1) && g(x+1) != 0;

Here, x + 1 is used as an argument to g, but x is not; you may get counterexamples where g(x+1) == 0 for some x. In that case, you can add an additional equivalent require that does use the quantified variable as an argument to g:

require forall uint x . f(x) < g(x+1) && g(x+1) != 0;
require forall uint x . f(x-1) < g(x) && g(x) != 0;

This will make x a direct argument to g, so the expression will be grounded properly.

Double Polarity

The polarity of a sub-formula is the direction of the effect it has on the output of the formula. This is best demonstrated through an example:

a && (b || !c)

In this example, b possesses a positive polarity because changing b from false to true can’t make the formula false if it wasn’t before. Informally, making b “more true” can only make the whole formula “more true”.

In this example, a also possesses positive polarity: if the formula was true when a was false, it must also be true when a is true.

On the other hand, c has a negative polarity because changing c from true to false can only make the statement “more false”. If can’t become true if it wasn’t true before.

Sub-expressions can also have double polarity. For example, consider the formula

a <=> b

In this example, a has double polarity, because making a true could cause the formula to become false when it was true before, but it could also cause the formula to become true when it wasn’t before.

Grounding is disallowed when the quantified expression has double polarity in the rule. For example, the following is disallowed, because the forall statement has double polarity.

rule r {
    ...
    assert (forall uint x . f(x) > 0) <=> y;
}

In many cases you can split a rule with a quantifier in a double-polarity position into multiple rules with single-polarity quantifiers. For example, the above assertion could be split into two rules:

rule r1 {
    ...
    assert (forall uint x . f(x) > 0) => y;
}

rule r2 {
    ...
    assert y => (forall uint x . f(x) > 0);
}

Verifying r1 and r2 is logically equivalent to verifying r, but the quantified expression appears with single polarity in each of the two rules.