Rule Sanity Checks

The --rule_sanity option enables some automatic checks that can warn users about certain classes of mistakes in specifications.

There are several kinds of sanity checks:

• Vacuity checks determine whether rules pass vacuously because they rule out all models.

• Assert tautology checks determine whether individual assert statements are tautologies.

• Trivial invariant checks detect invariants that hold in all states, rather than just reachable states.

• Assertion structure checks detect unnecessarily complex assert statements.

• Redundant require checks detect unnecessary require statements.

The --rule_sanity option may be followed by one of none, basic, or advanced options to control which sanity checks should be executed:

• With --rule_sanity none or without passing --rule_sanity, no sanity checks are performed.

• With --rule_sanity basic or just --rule_sanity without a mode, the vacuity check and the trivial invariant check are performed.

• With --rule_sanity advanced, all the sanity checks will be performed for all invariants and rules.

We recommend starting with the basic mode, since not all rules flagged by the advanced mode are incorrect.

When the Prover is run with any of these options, it first checks that the rule passes; if it does pass then the sanity checks are performed. If the sanity checks also pass, the rule is marked as verified with a green checkmark; if the sanity check fails, the rule is marked with a yellow symbol:

If a sanity check fails, you can expand the problems view to see the details of the failure:

The remainder of this document describes these checks in detail.

Vacuity checks

The vacuity sanity check ensures that even when ignoring all the user-provided assertions, the end of the rule is reachable. This check ensures that that the combination of require statements does not rule out all possible counterexamples. Rules that rule out all possible counterexamples are called vacuous rules. Since they don’t actually check any assertions, they are almost certainly incorrect.

For example, the following rule would be flagged by the vacuity check:

rule vacuous {
    uint x;
    require x > 2;
    require x < 1;
    assert f(x) == 2, "f must return 2";
}

Since there are no models satisfying both x > 2 and x < 1, this rule will always pass, regardless of the behavior of the contract. This is an example of a vacuous rule — one that passes only because the preconditions are contradictory.

The vacuity check also flags situations where counterexamples are ruled out for reasons other than require statements. A common example comes from reusing env variables. Consider the following poorly-written rule:

env e; uint amount; address recipient;

require balanceOf(recipient) == 0;
require amount > 0;

deposit(e, amount);
transfer(e, recipient, amount);

assert balanceOf(recipient) > 0,
    "depositing and then transferring makes recipient's balance positive";

Although it looks like this rule is reasonable, it may actually be vacuous. The problem is that the environment e is reused, and in particular e.msg.value is the same in the calls to deposit and transfer. Since transfer is not payable, it will always revert if e.msg.value != 0. On the other hand, deposit always reverts when e.msg.value == 0. Therefore every example will either cause deposit or transfer to revert, so there are no models that reach the assert statement.

Assert tautology checks

The assert tautology sanity check ensures that individual assert statements are not tautologies. A tautology is a statement that is true on all examples, even if all the require and if conditions are removed. Tautology checks also consider the bodies of the contract functions. For example, assert square(x) >= 0; is a tautology if square is a contract function that squares its input.

For example, the following rule would be flagged by the assert tautology check:

rule tautology {
  uint x; uint y;
  require x != y;
  ...
  assert x < 2 || x >= 2,
   "x must be smaller than 2 or greater than or equal to 2";
}

Since every uint satisfies the assertion, the assertion is tautological, which may indicate an error in the specification.

Trivial invariant checks

The Trivial invariant sanity check ensures that invariants are not trivial. A trivial invariant is one that holds in all possible states, not just in reachable states.

For example, the following invariant is trivial:

invariant squaresNonNeg(int x)
    x * x >= 0

While it does hold in every reachable state, it also holds in every non-reachable state. Therefore it could be more efficiently checked as a rule:

rule squaresNonNeg(int x) {
    assert x * x >= 0;
}

The rule version is more efficient because it can do a single check in an arbitrary state rather than separately checking states after arbitrary method invocations.

Assertion structure checks

The assertion structure sanity check ensures that complex assert statements can’t be replaced with simpler ones.

If an assertion expression is more complex than necessary, it can pass for misleading reasons. For example, consider the following assertion:

uint x;
assert (x < 5) => (x >= 0);

In this case, the assertion is true, but only because x is a uint and is therefore always non-negative. The fact that x >= 0 has nothing to do with the fact that x < 5. Therefore this complex assertion could be replaced with the more informative assertion assert x >= 0;.

Similarly, if the premise of the assertion is always false, then the implication is vacuously true. For example:

uint x;
assert (x < 0) => (x >= 5);

This assertion will pass, but only because the unsigned integer x is never negative. This may mislead the user into thinking that they have checked that x >= 5 in some interesting situation, when in fact they have not. The simpler assertion assert x >= 0; more clearly describes what is going on.

Overly complex assertions like this may indicate a mistake in the rule. In this case, for example, the fact that the user was checking that x >= 0 may indicate that they should have declared x as an int instead of a uint.

The assertion structure check tries to prove some complex logical statements by breaking them into simpler parts. The following situations are reported by the assertion structure check:

• assert p => q; is reported as a sanity violation if p is false whenever the assertion is reached (in which case the simpler assertion assert !p; more clearly describes the situation), or if q is always true (in which case assert q; is a clearer alternative).

• assert p <=> q; is reported as a sanity violation if either p and q are both true whenever the assertion is reached (in which case the simpler assertions assert p; assert q; more clearly describe the situation), or if neither p nor q are ever true (in which case assert !p; assert !q; is a clearer alternative).

• assert p || q; is reported as a sanity violation if either p is true whenever the assertion is reached (in which case assert p; more clearly describes the situation) or if q is always true (in which case assert q; is a clearer alternative).

Redundant require checks

The require redundancy sanity check highlights redundant require statements. A require is considered to be redundant if it does not rule out any models that haven’t been ruled out by previous requires.

For example, the require-redundancy check would flag the following rule:

rule require_redundant {
  uint x;
  require x > 3;
  require x > 2;
  assert f(x) == 2, "f must return 2";
}

In this example, the second requirement is redundant, since any x greater than 3 will also be greater than 2.