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 counter-examples for such rules, since there are no examples whatsoever for such rules. By default, the Prover will mark such rules as verfied, but they are in fact meaningless.

The solution is to use the Prover’s built-in rule sanity. Adding --rule_sanity basic to the command line, or "rule_sanity": "basic" to the config file will cause the Prover to check if the rules being verified are vacuous.

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 running without rule_sanity, the Prover will mark this rule as verified since it has no counter-example, even though the assertion can never be satisfied. When using rule_sanity the Prover will indicate this rule fails sanity checks.

Reverting computation paths

By default, the Prover ignores computation paths that result in a revert. 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 versions that revert 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 also revert.

Note

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

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 without rule_sanity.

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, underflow will cause a revert. The require statement in the rule forces underflow in the Solidity sub function. In the specified Solidity compileer version, this underflow will cause a revert.

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;
}