# 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:

- The invariant holds over the post state
- The postconditions hold for every method level behaviour