Deployment of a contract using Truffle, Ganache and Etheno to test with Echidna

In this tutorial, we are going to show how to use Etheno and Echidna to test the contract from the TruffleCoin example (also called MetaCoin). We will start installing the TruffleCoin project from the corresponding Truffle University repository:

$ git clone https://github.com/truffleuniversity/TruffleCoin
$ cd TruffleCoin
$ npm i
$ npm truffle
$ touch .secret

Since we will use a few node packages from its local installation directory, it is a good idea to add the ./node_modules/.bin directory into the PATH before continue:

$ PATH=$PATH:./node_modules/.bin

First, we need a contract to test the TruffleCoin one. We will add the following one to test a single property in contracts/TEST.sol:

pragma solidity ^0.4.18;

import "./TruffleCoin.sol";

contract TEST is TruffleCoin {

        function mint(uint amount) public {
                balances[msg.sender] = amount;
        }

        function echidna_convert() public view returns (bool) {
                return getBalanceInEth(msg.sender) >= getBalance(msg.sender);
        }
}

At this point, you can test that all the contracts can be compiled:

$ truffle compile

Compiling your contracts...
===========================
✔ Fetching solc version list from solc-bin. Attempt #1
> Compiling ./contracts/ConvertLib.sol
> Compiling ./contracts/Migrations.sol
> Compiling ./contracts/TEST.sol
> Compiling ./contracts/TruffleCoin.sol
✔ Fetching solc version list from solc-bin. Attempt #1

However, if you try to test directly this contract with Echidna, it will fail:

$ echidna-test . --contract TEST
...
Analyzing contract: /home/g/Code/echidna-etheno/truffle-coin/contracts/TEST.sol:TEST
echidna-test: VM attempted an illegal operation: BadJumpDestination

There is a good reason for that: the deployment of TEST requires to the deploy/link of ConvertLib, which is specified in the migrations. To workaround this complexity, we will use Etheno to execute the complete migration process and then replay it in Echidna to test the resulting contracts.

As expected, we will need to install Etheno and Ganache first:

$ pip3 install etheno --user
$ npm i ganache ganache-cli

Before executing Etheno, we should make sure we will deploy the TEST contract modifying migrations/2_deploy_contracts.js to look like this:

var ConvertLib = artifacts.require("./ConvertLib.sol");
var TruffleCoin = artifacts.require("./TruffleCoin.sol");
var TEST = artifacts.require("./TEST.sol");

module.exports = function(deployer) {
  deployer.deploy(ConvertLib);
  deployer.link(ConvertLib, TruffleCoin);
  deployer.deploy(TruffleCoin);
  deployer.link(ConvertLib, TEST);
  deployer.deploy(TEST);
};

Then, we can execute the migration using Etheno.

$ etheno --truffle --ganache -p 7545 -i 5777 -x export.json
INFO     [01-06|15:16:09][Ganache@7546] Ganache CLI v6.7.0 (ganache-core: 2.8.0)
INFO:Ganache@7546:Ganache CLI v6.7.0 (ganache-core: 2.8.0)
INFO     [01-06|15:16:09][Ganache@7546] 
INFO:Ganache@7546:
...
INFO     [01-06|15:16:15][EventSummaryExportPlugin] Event summary JSON saved to export.json
INFO:EventSummaryExportPlugin:Event summary JSON saved to export.json
INFO     [01-06|15:16:19][EventSummaryExportPlugin] Event summary JSON saved to export.json
INFO:EventSummaryExportPlugin:Event summary JSON saved to export.json

At this point, Etheno will produce the export.js file and then wait indefinitely. We do not need it anymore, we can just kill it with Ctrl+C.

Before using Echidna, we need to create a small configuration file named to specify the use of the pre-initialized blockchain:

initialize: ./export.json

We named this file as config.yaml. Finally, we can use Echidna to run TEST and find a counter-example for the echidna_convert property:

$ echidna-test . --contract TEST --config config.yaml 
...
Analyzing contract: truffle-coin/contracts/TEST.sol:TEST
echidna_convert: failed!💥  
  Call sequence:
    mint(93749286633875523254547042675116875197716632035530460765794648324267796915376)