SMT Backend

The SMT backend for Act is currently able to automatically prove that:

  • post conditions are implied by pre conditions
  • contract level invariants hold

To perform these proofs, you can simply run act prove --file <PATH_TO_SPEC> against your spec.

act prove also accepts the following configuration flags:

  • --solver: you can choose to use cvc4 or z3 as the solver backend. The default is z3. Sometimes cvc4 may be able to prove things that z3 cannot (and vice versa). You can also prove the same properties with multiple solvers to gain confidence that the proofs are not affected by a bug in the solver itself.
  • --smttimeout: the timeout given for each smt query. This is set to 20s by default.
  • --debug: this prints the raw query dispatched to the SMT solver to stdout. Note that these queries are machine generated by the sbv library and so are fairly challenging to inspect manually.

Examples

Automatic Market Maker

As an example consider the following specification of a simplified uniswap style automatic market maker. For the purposes of this example we focus only on the core logic, and ignore e.g. interactions with the underlying tokens.

The Amm has two state variables representing its underlying token balances, reserve0 and reserve1. These are initialized to 1000 units each upon creation.

We define a single invariant, that the product of the two reserves should never decrease. This is an important safety property, if it is violated, an attacker will be able to execute a sequence of trades that can drain all funds from the exchange.

behaviour init of Amm
interface constructor()

creates

    uint256 reserve0 := 1000
    uint256 reserve1 := 1000

invariants

    1000 * 1000 <= reserve0 * reserve1

Next, we define the two swap methods, that allow a user to exchange tokens. These methods take an amount (amt) of input reserves, and the Amm will adjust the size of the other reserve according to the x * y == k constant product formula.

behaviour swap0 of Amm
interface swap0(uint256 amt)

iff in range uint256

    reserve0 + amt

storage

    reserve0 => reserve0 + amt
    reserve1 => (reserve0 * reserve1) / (reserve0 + amt)

behaviour swap1 of Amm
interface swap1(uint256 amt)

iff in range uint256

    reserve1 + amt

storage

    reserve0 => (reserve0 * reserve1) / (reserve1 + amt)
    reserve1 => reserve1 + amt

If we run act prove against the above spec, we find that there is in fact an error. If the Amm starts with reserve0 == 1 and reserve1 == 1,000,000, and swap0 is called with amt == 2, the final state of the Amm will be reserve0 == 3 and reserve1 == 333,333. In this case 3 * 333,333 is 999,999, and in fact the product of the reserves has decreased slightly due to imprecision introduced by the EVM's flooring division.

A safe specification for the swap methods is as follows. Notice the extra +1 added to the output reserve in both cases. With this implementation, the rounding error is now in favor of the pool instead of the trader, and the contract is now safe against this particular attack.

If we again run act prove against the fixed specification, we see that the invariant holds for all possible executions of the contract.

behaviour swap0 of Amm
interface swap0(uint256 amt)

iff in range uint256

    reserve0 + amt

storage

    reserve0 => reserve0 + amt
    reserve1 => (reserve0 * reserve1) / (reserve0 + amt) + 1

behaviour swap1 of Amm
interface swap1(uint256 amt)

iff in range uint256

    reserve1 + amt

storage

    reserve0 => (reserve0 * reserve1) / (reserve1 + amt) + 1
    reserve1 => reserve1 + amt

Underpowered Invariant

Due to the inductive nature of the proof, there are some true invariants that the SMT backend is unable to prove. For example, consider the following state machine:

behaviour init of C
interface constructor()

creates
    uint x := 0

invariants
    x < 9

behaviour f of C
interface f()

case x == 0:

    storage
        x => 1

behaviour g of C
interface g()

case x == 1:

    storage
        x => 2

behaviour j of C
interface j()

case x == 7:

    storage
        x => 100

The contract C can never be in a state were x == 7 and so the write of 100 to x in j() can never occur, however if we run act prove against this specification, this exact case (x == 7) is found as a counterexample.

This is due to the inductive nature of the proof: act checks that the invariant holds after running the constructor, and then for each method assumes that the invariant holds over the pre state and checks that the invariant holds over the post state.

In the case above, the invariant states that x < 9, and if this is assumed as a precondition, then the x == 7 branch in j() is still reachable.

We can fix this by strengthening the invariant to make the x == 7 branch unreachable, in the case of the spec above, an invariant of x < 7 is sufficient, although x < 3 is the strongest invariant of this form that holds over the full transition system.

Limitations

Although SMT solvers are powerful tools there are some important limitations to be aware of:

  • The invariants proven can only be inductive in nature, and can only be expressed in terms of state variables and constructor arguments.
  • SMT solvers do not support the exponentiation operation.
  • The solver may be unable to prove properties about behaviours making extensive use of non linear arithmetic (i.e. multiplication or division by a symbolic value). This is an inherent limitation of all SMT solvers.

Implementation Strategy

For each invariant claim, Act builds an individual SMT query for each behaviour in the transtion system. If there are no invariant claims defined, then act will insert an implicit invariant of True, meaning that the postconditions are still checked.

If the behaviour is a constructor, the query asks the solver to find instances where:

  • the preconditions hold
  • the storage values in the poststate match those specified by the creates block of the constructor
  • the invariant does not hold over the post state or the postconditions do not hold over the poststate

If the behaviour is a method, the query asks the solver to find instances where:

  • the invariant holds over the pre state
  • the preconditions hold
  • all storage variables in the prestate are within the range specified by their type
  • a predicate relating the pre and post state according to the specification in the storage block holds
  • the invariant does not hold over the post state or the postconditions do not hold over the poststate

If all of the queries for an invariant claim return unsat, then two properties have been proved about the transition system:

  1. The invariant holds over the post state
  2. The postconditions hold for every method level behaviour