Intro: the Distributed Finance Trilemma

There is a growing consensus that one of the key hurdles the Decentralized Finance (DeFi) world has to overcome is the problem of smart contract security.

Indeed, when the news cycle is dominated by stories of fraud and loss, wider mainstream adoption remains a distant prospect, to say nothing of true competition with the current financial services and investment banking incumbents like Visa, J.P. Morgan, and Goldman-Sachs.

Contrary to what many people outside the Blockchain community say, this problem is not simply a product of over-hyped projects with insane deadlines or start-ups with a “cowboy coding” culture.

These well-publicized factors certainly exist in some cases, and they definitely don’t help, but laying the blame solely at their feet is utter nonsense, as anyone inside the Blockchain community can tell you.

It is actually much, much worse.

This is because developing a DeFi product is an engineering problem of deceptive depth — it is easy to write a smart contract in Solidity that (mostly) does what you want, but it is hard to do it well. Much like Vitalik Buterin’s famous Blockchain Trilemma, the process of Smart Contract development is also guided by three separate, and often conflicting, goals:

• Minimize gas consumption. As in high frequency trading, seemingly “trivial” optimizations can have far reaching implications for gas cost and therefore usability. After exhausting the usual “bag of tricks”, improving the gas cost of various operations often necessitates writing in assembly instead of Solidity (or Viper) or finding clever tricks to compute approximations for non-linear and computationally heavy functions.
• Maximize security. Like hardware, smart contracts are immutable by design, which means that any bug introduced in the development process is here to stay. True, upgradable contracts exist and can bypass immutability. However, their presence introduces another tradeoff: users are never sure that the contract they interact with won’t change, and with every upgrade comes the risk of introducing new bugs. Combined with the large amounts of money handled by DeFi protocols and the inherent decoupling of EOA addresses and real world identities (as well as “Code is Law” philosophy), these realities can make any vulnerability in the code an extremely dangerous and costly one. In particular, it means that one has to be extremely careful of rounding errors, edge cases, and mathematical design problems.

• Minimize time-to-market. This is a pressing matter in any software project, but more so in the extremely competitive and highly volatile world of decentralized finance. Unfortunately, even if one were to accomplish the goal of gas optimization and security simultaneously, it is clear that the additional checks imposed in every step would slow the development process considerably.

Formal Verification in the Development Cycle

Helping developers reach a better equilibrium without compromising on one of these three requirements, Certora has been developing a new product called the Equivalence Checker. Unlike the Certora Prover which is focused on testing and security, this lightweight formal verification allows DeFi programmers to compare different versions of the same mathematical formula written in:

1. low-level (Yul or assembly)
2. high-level (Solidity)
3. pure logic (encoded in Certora Verification Language or CVL for short)

and show that they are equivalent (more on that below). It is meant to be used as a rapid development tool during the entire life-cycle of the project and help with both security, development time, and gas consumption.

The remainder of this post demonstrates the workflow of this new tool in a concrete case. We explain about the different modes of the Equivalence Checker and demonstrate how it has been able to both immediately detect a famous old bug as well as a new, previously undiscovered bug, in live code (remark: readers should note this is a low-severity bug chosen for didactic purposes. In the sequel to this blog we will reveal and analyze a more elaborate case where a high-severity bug was detected using the Equivalence Checker —so please stay tuned for more!)

But first,

What exactly does ‘functional equivalence’ mean?

A Solidity/Yul function is said to be pure if it does not read or modify the state (they can however revert potential state changes if an error occurs). It can have multiple input and output values. For example, the following function is pure:

    function safeAdd(uint a, uint b) public pure returns (uint c) {
        c = a + b;
        require(c >= a);
    }

We will say that two pure functions f(…) and g(…) are equivalent if:

1. They have the same input/output variables.
2. [assuming 1 holds:] for a given tuple of input values -

(a) f reverts if and only if g reverts.

(b) [assuming f and g did not revert:] the return values of f and g are identical.

Of course, this definition can be extended to suitable fragments of EVM bytecode and made precise in the formalism of the Ethereum Yellow Paper. (the equivalence between a pure function and a logic formula is similar, but slightly more subtle and explained best by the second example below).

Now that we have properly defined equivalence, it is time to begin our discussion in earnest.

Background: implementing fixed-point division

It is well-known that the Ethereum Virtual Machine (EVM) natively supports only two data types: the 256-bit word and 8-bit byte. Furthermore, most EVM opcodes deal with word-size chunks of data at a time, including all the mathematical ones. Thus, there are basically only two numerical data types in Ethereum:

• signed 256-bit integers.
• unsigned 256-bit integers,

which are represented in Solidity by the uint256 and int256 data types, respectively.

This is unfortunate, since virtually any type of financial application needs to implement some support for fractional arithmetic. There are a few different ways to go about this, but the most popular in DeFi applications (by far) is fixed-point numbers. These are basically simple fractions whose denominator is a predefined constant, usually a power of 2 (“binary”) or 10 (“decimal”). The standard choices of denominator in the decimal case are 10¹⁸ (known as a “wad”) or 10²⁷ (a “ray”). Thus, existing Solidity fixed-point libraries often represent a wad as a 256-bit integer. This is pretty straightforward for addition and subtraction, but when performing multiplication or division one must rescale the result to get the right answer.

For example,

1.5 * 2.7 == 4.05
//Regular integer arithmetic adds orders of magnitude:
150 * 270 == 40500
// Wad arithmetic does not add orders of magnitude:
wadMul(1.5 ether, 2.7 ether) == 4.05 ether

Consider the following test case. We want to write a function wadDiv that divides two wads, rounding half wad and above up to the nearest wad. These types of arithmetic functions are very common in DeFi. They are necessary to take into account the difference between how integer arithmetic behaves normally, and how decimal arithmetic should actually work.

Step 1: Test the code

As a first step, we consider the following reference implementation for wadDiv written in Solidity:

uint256 internal constant WAD = 1e18;
function wadDivSol(uint256 a, uint256 b) public pure returns (uint256 c)
{
  c = (a * WAD + (b/2)) / b;
  return c;
}

In an attempt to optimize it, we played around with assembly a bit and created the following provisional Yul version:

function wadDivAsm(uint256 a, uint256 b) public pure returns (uint256 c)
{
  assembly
  {
    if iszero(iszero(gt(a, div(sub(not(0), div(b, 2)), WAD))))
    { revert(0, 0) }
    c := div(add(mul(a, WAD), div(b, 2)), b)
  }
}

and indeed we see a substantial reduction in gas costs: the Solidity version requires ~860 gas to perform the computation while the assembly one only spends ~140 gas.

Question. Does this work (i.e., are these two functions equivalent)?

Instead of racking our brains trying to find the answer, the Equivalence Checker generic rules template immediately produces the following two rules, written in CVL (Certora Verification Language), and submits them to the Prover for formal verification.

Almost immediately, the prover detects a discrepancy between the two revert conditions:

and yields the following counterexample:

(Why? Because division by zero in Yul returns zero instead of reverting! See the linked tweeter thread for a detailed discussion)

Step 2: Test the logic

Suppose we have now fixed the bug and written a new Yul version:

function wadDivAsmNew(uint256 a, uint256 b) public pure returns (uint256 c)
{
  assembly 
  {
    if or(iszero(b), iszero(iszero(gt(a, div(sub(not(0), div(b, 2)), WAD))))) 
    { revert(0, 0) }
    c := div(add(mul(a, WAD), div(b, 2)), b)
  }
}

Question. Are we done?

Good news: Running the Equivalence Checker now shows that it is the same as the Solidity version!

Bad news: Not so fast… because our original Solidity version is WRONG.

To see that, we need to run the Equivalence Checker in a different configuration. In the previous paragraph we explained how we can use the Equivalence Checker to compare code (wadDivAsmOld) vs. code (wadDivSol/wadDivAsmNew).

Now we need to compare a piece of code (wadDivSol) which carries out a certain mathematical computation on the EVM) with two mathematical functions which describe its behavior:

• wadDiv_ShouldRevert — which encodes the desired revert condition, namely it is a boolean-valued function that accepts the same input parameters as wadDivSol and returns true if and only if the execution of wadDivSol by the EVM with the specified input parameters should result in a revert. In our case, we want wadDivSol to revert if and only if the denominator is zero or the result is bigger than 2²⁵⁶-1 (the largest integer that can be stored in a uint256), causing an integer overflow.
• wadDiv_ComputeInMathint — which accepts the same input parameters as wadDivSoland encodes the formula which produces the output as computed over the integers.

Written in CVL, the specification for these two functions is -

In this case, equivalence testing consists of checking that the following two rules are true -

What do they mean?

• Well, the first rule is precisely what it looks like. It says that wadDiv_ShouldRevertreverts if and only if wadDivSolreverts.
• The second rule is a bit more subtle. It states that given the same inputs, wadDivSoland wadDiv_ComputeInMathintreturn the same uint256 value provided that wadDivSoldid not revert (note the lack of the @withrevert modifier) in the second rule.

Running the Prover results in a counterexample:

Indeed, after converting these values to decimal, we get:

X (as WAD) = 1766847064778384331350144565521302847.177628462396921805
Y (as WAD) = 0.000000000000000003
=> X/Y (as WAD) = 588949021592794777116714855173767615725876154132307268.333333333333333333

which is still within range and can be represented by a uint256 type. Thus, we find that the Solidity version we wrote reverts “too eagerly,” i.e., the way we choose to implement the computation causes reverts to occur even when they shouldn’t.

Conclusion

The Equivalence Checker is a flexible, easy to use CLI tool which allows a user to compare two pieces of code, or an implementation vs a specification, for functional equivalence. Its purpose is to accelerate code development and improve gas efficiency without compromising security. The current prototype version supports Yul, Solidity, and CVL. It is expected to be released in 2023 Q2.

Future planned versions may allow for comparison between Solidity/Yul and Vyper (or even Cairo).

I hope you enjoyed this tutorial and exploring the tool’s capabilities. We would love to get feedback and improvement proposals from developers and users — please comment below if you have any questions or suggestions.

Finally, as we mentioned before this blog is only the first part of a series — stay tuned for more!