2.7. Vacuity

Introduction

A rule is called vacuous if there are no computation paths satisfying the necessary requirements (excluding the rule’s assertions). The Prover can find no counterexamples for such rules, since there no examples exist. By default, the Prover v8.0 and newer uses the built-in rule sanity feature to check if the rules being verified are vacuous and marks them accordingly in the results. But, if --rule_sanity none is added to the command line (or conf file), the Prover will mark such rules as verified, which can lead to confusion since they are actually meaningless.

Simple Example

Here is a simple example for a vacuous rule, containing contradictory requirements.

rule simpleVacuousRule(uint256 x, uint256 y) {
    // Contradictory requirement
    require (x > y) && (y > x);
    assert false;  // Should always fail
}

When using the default rule_sanity the Prover will indicate this rule fails the basic sanity checks. When running with --rule_sanity none, the Prover will mark this rule as verified since there is no counterexample (i.e. no case when the :solidity:assert fails) because the :solidity:assert is not reachable at all.

Reverting computation paths

By default, the Prover ignores computation paths that result in a revert of the simulated blockchain transaction. So, by default the Prover considers only those computation paths where all Solidity require statements are satisfied. Moreover, any overflow or underflow paths are ignored (when using Solidity version 0.8.0 or higher which reverts on overflow and underflow).

To include computation paths that result in a revert, use the operator @withrevert when calling a Solidity function, e.g. someFunction@withrevert(args). CVL has a builtin boolean variable lastReverted that is true if the last Solidity function called reverted (whether it used @withrevert or not).

Note that if the call someFunction@withrevert(args) does revert, its return value will be arbitrary and all Solidity variables will revert to their values before the call.

Note

In Ghosts and hooks we will learn about ghost variables, which are roughly CVL global variables. When a Solidity function reverts, ghost variables also revert unless they are declared persistent.

More examples

We’ll use the following simple contract, the code is found in Vacuous.sol.

pragma solidity ^0.8.0;

/// @title Examples of vacuous rules
contract Vacuous {

  mapping (address => uint256) public amounts;
  uint256 public immutable maximalAmount = 1000;

  function add(address user, uint256 amount) public returns (uint256) {
    require(amounts[user] + amount <= maximalAmount);
    amounts[user] += amount;
    return amounts[user];
  }

  function sub(address user, uint256 amount) public returns (uint256) {
    amounts[user] -= amount;
    return amounts[user];
  }
}

The following CVL examples are from Vacuous.spec. In the same folder there are also two config files for running this spec. One config file without rule_sanity: Vacuous.conf, while the other uses basic rule_sanity: Vacuous_sanity.conf.

Vacuous rule

The following rule is vacuous. It will be verified when running the conf with "rule_sanity": "none".

rule subtleVacuousRule(address user, uint256 amount) {
    uint256 userAmount = amounts(user);
    require amount > userAmount;
    sub(user, amount);
    assert false;  // Should always fail
}

Do you understand why this rule is vacuous?

Answer

In the specified Solidity version (“^0.8.0”), arithmetic underflow will cause a revert. The require statement in the rule forces underflow in the Solidity sub function. So, that function reverts in all possible executions, making the assert statement unreachable.

Using withrevert

This is similar to the previous example, but here we call sub using the @withrevert operator. We assert that the function will always revert. This rule is correctly verified.

rule revertingRule(address user, uint256 amount) {
    uint256 userAmount = amounts(user);
    require amount > userAmount;
    sub@withrevert(user, amount);
    assert lastReverted;
}