Formal verification is a mathematical method for proving the

Formal verification can be performed by means of several techniques. Here, we shall focus on equivalence checking. Equivalence checking ensures that two designs or implementations of a system are equivalent, and they will behave identically under all possible inputs and conditions. In the context of formal verification of smart contracts, equivalence checking can be used to ensure that different versions of a smart contract, or a smart contract and its specification, are equivalent. This can be particularly useful in situations where a smart contract has been modified or updated, as it can help to ensure that the modified contract is still correct and behaves as intended.

The MulDiv function calculates floor

In this blog article we use equivalence checking to prove the correctness of MulDiv with respect to a reference model (see Figure below). In principle, one can use their own abstracted reference model as well, but for this article we will use the aforementioned model which is publicly available. Both the models are implemented in Solidity and they achieve the same goal. However, both the models are implemented in a slightly different way. Our goal is to prove that both models are indeed implementing the same functionality.

For equivalence checking, we are using Z3 theorem prover. First, we need to transform the Solidity implementation of MulDiv to a representation Z3 solver understands. Either we can write the MulDiv function code into SMT-Lib format directly or we can use Z3’s Python API. For this blog article, we will use Python 3 here. The first step is to install

pip install z3-solver

Afterwards, create a new Python file and import z3. At this point, we have to build a syntax tree of a mathematical formula which is solved by Z3. This can be done in multiple ways. In this blog, we utilize the following approach:

We start by declaring the function mulDiv which takes 3 parameters as input,

We then declare all locally used variables as symbolic variables of type Bit Vector. Here, it is worth mentioning that we will use Static Single Assignment (SSA). SSA is a form of intermediate representation (IR) in which each variable is assigned exactly once, and every variable is defined before it is used. This has several benefits for analysis of programs. Some of the declarations with 256-bits bitwidth are shown below:

from z3 import * def mulDiv (a, b, denominator): prod0= BitVec("prod0",256) prod00= BitVec("prod00",256) prod000= BitVec("prod000",256) prod1 = BitVec ("prod1",256) mm= BitVec("mm",256) result0 = BitVec ("result0",256) result1 = BitVec ("result1",256)

Here, prod0 represents the variable defined the first time, prod00 represents “prod0” defined the second time, and so on. As a next step, we analyze the mulDiv Solidity code shown below

let mm := mulmod(a, b, not(0)) prod0 := mul(a, b) prod1 := sub(sub(mm, prod0), lt(mm, prod0))

In the code excerpt, there is a solidity variable

s.add (mm == (a * b) % int(negate(0))) s.add (prod0 == a * b)

One important thing to note is that there are no assignments in Z3. Equality symbol (==) is always used. If the code is written in a different way using standard Python syntax, then Python transforms the code into equality symbol by itself.

For

If (condition, then, else)

The

s.add (If(ULT(mm, prod0), prod1 == mm - prod0 - BitVecVal(0x1, 256), prod1 == mm - prod0 - BitVecVal(0x0, 256)))

we start with the unsigned comparison of

…. …. if (prod1 == 0) { require(denominator > 0); assembly { result := div(prod0, denominator) } return result; } … … result = prod0 * inv; return result;

To represent the 2 aforementioned cases, we add the following statement:

s.add (If (prod1 == 0, result == result0, result == result1))

We create a variable

Similarly, the mulDiv code from Mikhail is also converted in to Z3 expressions. Once both the functions are implemented, we check if they are equivalent or not. For this, we define an invariant using Z3Py

s.add(Not(ForAll (X, ForAll (Y, ForAll (denom, mulDiv (X,Y,denom) ==mulDiv_medium(X,Y,denom)))))) ans = s.check() if ans == sat: print (ans) print (s.model()) elif ans == unsat: print ("unsat") else: print ("unknown")

It means, we want to check, for all the values of

At this point, we have Uniswap mulDiv function and Mikhail mulDiv function implemented using Z3 expressions. Additionally, we have the invariant which should always hold true if there are no bugs. The final step is to run the Python code with the following command:

Python Filename.py

The code output is UNSAT, which means for all X, Y, and denom, there does not exist any input value which results in different outputs. Hence, it is proof that the implemented functionality is indeed correct.

We also defined more invariants (properties which should always stay True) but we shall talk about those in our upcoming articles.

The complete code can be downloaded from our GitHub.

About Truscova:

Truscova comes with 30+ years of academic research and hundreds of academic publications which pioneered the area of Formal Verification. The team combines academic leadership, industrial strength and Blockchain expertise. Truscova currently analyzes Solidity code combining Formal Verification techniques: abstract interpretation, constraint solving, theorem proving, and equivalence checking.

The Next Step?