|
| 1 | +--- |
| 2 | +title: 🪨 Coq of Solidity – part 2 |
| 3 | +tags: [formal verification, Coq, Solidity, Yul] |
| 4 | +authors: [] |
| 5 | +--- |
| 6 | + |
| 7 | +We present how we develop a formal verification framework for [Solidity](https://soliditylang.org/) smart contracts with the [Coq](https://coq.inria.fr/) proof assistant. We use the [coq-of-solidity](https://github.com/formal-land/solidity) tool to translate Solidity code to Coq that we presented in our previous blog post [🪨 Coq of Solidity – part 1](/blog/2024/06/28/coq-of-solidity-1). |
| 8 | + |
| 9 | +We will take the example of an [ERC-20 smart contract](https://en.wikipedia.org/wiki/Ethereum#ERC20) implementation and show that it is equivalent to a purely functional definition in Coq acting as a specification. |
| 10 | + |
| 11 | +<!-- truncate --> |
| 12 | + |
| 13 | +:::info AlephZero |
| 14 | + |
| 15 | +_We are happy to be working with [AlephZero](https://alephzero.org/) to develop tools to bring more security for the audit of Solidity smart contracts, thanks to the use of formal verification and the interactive theorem prover [Coq](https://coq.inria.fr/). We thank the Aleph Zero Foundation for their support._ |
| 16 | + |
| 17 | +::: |
| 18 | + |
| 19 | +<figure> |
| 20 | +  |
| 21 | +</figure> |
| 22 | + |
| 23 | +## Simplifying the code |
| 24 | + |
| 25 | +We take the ERC-20 smart contract given in the tests of the Solidity compiler: [test/libsolidity/semanticTests/various/erc20.sol](https://github.com/ethereum/solidity/blob/develop/test/libsolidity/semanticTests/various/erc20.sol). It contains around **100 lines of Solidity**. We translate it with `coq-of-solidity` to the file [CoqOfSolidity/test/libsolidity/semanticTests/various/erc20/ERC20.v](https://github.com/formal-land/solidity/blob/guillaume-claret%40experiments-with-yul/CoqOfSolidity/test/libsolidity/semanticTests/various/erc20/ERC20.v) of **6,662 lines of Coq**. These lines are generated but this is still a large increase in terms of code size, more than sixty times. Looking at the Yul code of the contrat, the intermediate representation of the Solidity code that we use to make a translation to Coq, we get around **1,000 lines of Yul** when pretty-printed with the `--ir-optimized` option of the Solidity compiler. This is the actual size of the code that we need to analyze, once we remove the verbosity due to our Coq notations. |
| 26 | + |
| 27 | +The beginning of the contract in Solidity looks like this: |
| 28 | + |
| 29 | +```solidity |
| 30 | +pragma solidity >=0.4.0 <0.9.0; |
| 31 | +
|
| 32 | +contract ERC20 { |
| 33 | + event Transfer(address indexed from, address indexed to, uint256 value); |
| 34 | + event Approval(address indexed owner, address indexed spender, uint256 value); |
| 35 | +
|
| 36 | + mapping (address => uint256) private _balances; |
| 37 | + mapping (address => mapping (address => uint256)) private _allowances; |
| 38 | + uint256 private _totalSupply; |
| 39 | +
|
| 40 | + constructor() { |
| 41 | + _mint(msg.sender, 20); |
| 42 | + } |
| 43 | +
|
| 44 | + // ... |
| 45 | +``` |
| 46 | + |
| 47 | +Here is the constructor of the contract, calling the function `_mint` defined below. In Yul we get for the code of the constructor: |
| 48 | + |
| 49 | +```go |
| 50 | +object "ERC20_403" { |
| 51 | + code { |
| 52 | + { |
| 53 | + /// @src 0:33:3484 "contract ERC20 {..." |
| 54 | + mstore(64, memoryguard(0x80)) |
| 55 | + if callvalue() |
| 56 | + { |
| 57 | + revert_error_ca66f745a3ce8ff40e2ccaf1ad45db7774001b90d25810abd9040049be7bf4bb() |
| 58 | + } |
| 59 | + constructor_ERC20() |
| 60 | + let _1 := allocate_unbounded() |
| 61 | + codecopy(_1, dataoffset("ERC20_403_deployed"), datasize("ERC20_403_deployed")) |
| 62 | + return(_1, datasize("ERC20_403_deployed")) |
| 63 | + } |
| 64 | + function allocate_unbounded() -> memPtr |
| 65 | + { memPtr := mload(64) } |
| 66 | + function revert_error_ca66f745a3ce8ff40e2ccaf1ad45db7774001b90d25810abd9040049be7bf4bb() |
| 67 | + { revert(0, 0) } |
| 68 | + function cleanup_rational_by(value) -> cleaned |
| 69 | + { cleaned := value } |
| 70 | + function cleanup_uint256(value) -> cleaned |
| 71 | + { cleaned := value } |
| 72 | + // ... |
| 73 | +``` |
| 74 | +
|
| 75 | +As we can see there is a lot of small intermediate functions that are introduced and for many of them they are very simple, or even doing nothing. The translation in Coq is the following: |
| 76 | +
|
| 77 | +```coq |
| 78 | +(* Generated by coq-of-solidity *) |
| 79 | +Require Import CoqOfSolidity.CoqOfSolidity. |
| 80 | + |
| 81 | +Module ERC20. |
| 82 | + Definition code : Code.t := {| |
| 83 | + Code.name := "ERC20_403"; |
| 84 | + Code.hex_name := 0x45524332305f3430330000000000000000000000000000000000000000000000; |
| 85 | + Code.functions := |
| 86 | + [ |
| 87 | + Code.Function.make ( |
| 88 | + "allocate_unbounded", |
| 89 | + [], |
| 90 | + ["memPtr"], |
| 91 | + M.scope ( |
| 92 | + do* ltac:(M.monadic ( |
| 93 | + M.assign (| |
| 94 | + ["memPtr"], |
| 95 | + Some (M.call (| |
| 96 | + "mload", |
| 97 | + [ |
| 98 | + [Literal.number 64] |
| 99 | + ] |
| 100 | + |)) |
| 101 | + |) |
| 102 | + )) in |
| 103 | + M.pure BlockUnit.Tt |
| 104 | + ) |
| 105 | + ); |
| 106 | + Code.Function.make ( |
| 107 | + "revert_error_ca66f745a3ce8ff40e2ccaf1ad45db7774001b90d25810abd9040049be7bf4bb", |
| 108 | + [], |
| 109 | + [], |
| 110 | + M.scope ( |
| 111 | + do* ltac:(M.monadic ( |
| 112 | + M.expr_stmt (| |
| 113 | + M.call (| |
| 114 | + "revert", |
| 115 | + [ |
| 116 | + [Literal.number 0]; |
| 117 | + [Literal.number 0] |
| 118 | + ] |
| 119 | + |) |
| 120 | + |) |
| 121 | + )) in |
| 122 | + M.pure BlockUnit.Tt |
| 123 | + ) |
| 124 | + ); |
| 125 | + Code.Function.make ( |
| 126 | + "cleanup_rational_by", |
| 127 | + ["value"], |
| 128 | + ["cleaned"], |
| 129 | + M.scope ( |
| 130 | + do* ltac:(M.monadic ( |
| 131 | + M.assign (| |
| 132 | + ["cleaned"], |
| 133 | + Some (M.get_var (| "value" |)) |
| 134 | + |) |
| 135 | + )) in |
| 136 | + M.pure BlockUnit.Tt |
| 137 | + ) |
| 138 | + ); |
| 139 | + Code.Function.make ( |
| 140 | + "cleanup_uint256", |
| 141 | + ["value"], |
| 142 | + ["cleaned"], |
| 143 | + M.scope ( |
| 144 | + do* ltac:(M.monadic ( |
| 145 | + M.assign (| |
| 146 | + ["cleaned"], |
| 147 | + Some (M.get_var (| "value" |)) |
| 148 | + |) |
| 149 | + )) in |
| 150 | + M.pure BlockUnit.Tt |
| 151 | + ) |
| 152 | + ); |
| 153 | +``` |
| 154 | +
|
| 155 | +This version is far longer, but the main difference is that here the variables are represented as names that are strings instead of proper Coq variable names. |
| 156 | +
|
| 157 | +A first thing we want to do is to rewrite all of these functions in Coq: |
| 158 | +
|
| 159 | +- simplifying the obvious cases, like removing the calls to identity functions, |
| 160 | +- using proper Coq variables and functions instead of strings. |
| 161 | +
|
| 162 | +:::warning For more |
| 163 | +
|
| 164 | +If you have smart contract projects that you want to formally verify, going further than a manual audit to find bugs, contact us at [contact@formal.land](mailto:contact@formal.land)! Formal verification has the unique advantage of covering all possible execution cases. |
| 165 | +
|
| 166 | +::: |
| 167 | +
|
| 168 | +## Conclusion |
| 169 | +
|
| 170 | +We have presented our ongoing development of a formal verification tool for Solidity using the Coq proof assistant. We have briefly shown how we translate Solidity code to Coq using the Yul intermediate language and how we define the semantics of Yul in Coq. We have tested our tool on the examples of the Solidity compiler's test suite to check that our formalization is correct. |
| 171 | +
|
| 172 | +Our next steps will be to: |
| 173 | +
|
| 174 | +1. Complete our definitions of the Ethereum's primitives, to have a 100% success on the Solidity test suite. |
| 175 | +2. Formally specify and verify an example of contract, looking at the [erc20.sol](https://github.com/formal-land/solidity/blob/guillaume-claret%40experiments-with-yul/test/libsolidity/semanticTests/various/erc20.sol) example. |
0 commit comments