Testing Truffle projects with Echidna

In this short tutorial, we are going to show how to use Echidna to test the contract from the pet shop Truffle project. To start, let's install the pet-shop project from corresponding truffle university repository:

$ git clone https://github.com/truffleuniversity/truffle-shop
$ cd truffle-shop
$ npm i

This small project only includes the Adoption contract, which allow any user to adopt a pet, given a valid petId:

pragma solidity ^0.5.0;

contract Adoption {
  address[16] public adopters;

  // Adopting a pet
  function adopt(uint petId) public returns (uint) {
    require(petId >= 0 && petId <= 15);

    adopters[petId] = msg.sender;

    return petId;
  }

  // Retrieving the adopters
  function getAdopters() public view returns (address[16] memory) {
    return adopters;
  }
}

We are going to test two properties:

• If a user adopts using a valid petID, then the getAdopters will return an array where the corresponding petId corresponds to the user.

• If a user tries to adopt a pet with an invalid petId, then the adopt function should revert.

We will create the following contract in the contracts/TestEchidna.sol file:

pragma solidity ^0.5.0;

import "./Adoption.sol";

contract TestEchidna is Adoption {
  uint i;
  function set_input(uint _i) public {
    i = _i;
  }

  function echidna_valid_adoption() public returns (bool) {
    uint petId = i % 16;
    adopt(petId);
    return (getAdopters()[petId] == msg.sender);
  }

  function echidna_revert_invalid_adoption() public returns (bool) {
    if (i < 16)
      revert();
    else
      adopt(i);
  }

}

Finally we can run Echidna to test these properties, pointing it to the current directory (.):

$ echidna-test . TestEchidna
Analyzing contract: contracts/TestEchidna.sol:TestEchidna
echidna_valid_adoption: passed! 🎉
echidna_revert_invalid_adoption: passed! 🎉

Seed: 4073542311594334568