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 ifp
is false whenever the assertion is reached (in which case the simpler assertionassert !p;
more clearly describes the situation), or ifq
is always true (in which caseassert q;
is a clearer alternative).assert p <=> q;
is reported as a sanity violation if eitherp
andq
are both true whenever the assertion is reached (in which case the simpler assertionsassert p; assert q;
more clearly describe the situation), or if neitherp
norq
are ever true (in which caseassert !p; assert !q;
is a clearer alternative).assert p || q;
is reported as a sanity violation if eitherp
is true whenever the assertion is reached (in which caseassert p;
more clearly describes the situation) or ifq
is always true (in which caseassert 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.