How to use Echidna with multiple contracts

In this short tutorial, we are going to show how to use Echidna to test multiple contracts at the same time, using a simple patter called "master contract". This special contract will be used to initialize the state of the other contracts and act as proxy for Echidna.

Let's suppose we have a contract like this one:

contract A {
  uint multiplier;
  uint threshold;

  constructor(uint x) public {
    multiplier = x;
  }

  function set(uint x) public {
    threshold = x;
  }

  function get(uint x) public returns (uint) {
    if (threshold == 0)
      return x;
    return multiplier*x+threshold;
  }
    
}

Contract A requires a parameter to be deployed (which sets multiplier). It has a state that can be changed using the set function (which sets threshold). In order to test a simple property of this contract, we are going to use a "master contract" to correctly initialize this contract and to proxy the Echidna to the trigger to code of A. Aaaand, to make things more interesting, we are going to instantiate two copies of the same contract with different parameters:

contract Master {
  
  A a1;
  A a2;
  uint i1;
  uint i2;

  constructor() public {
    a1 = new A(10**27);
    a2 = new A(10**10);
  }

  function set_input_a1(uint x) public {
    i1 = x;
  }

  function set_input_a2(uint x) public {
    i2 = x;
  }

  function set_threshold_a1(uint x) public {
    a1.set(x);
  }

  function set_threshold_a2(uint x) public {
    a2.set(x);
  }

  function echidna_property() public returns (bool) {
    return (i1 <= a1.get(i1)) && (i2 <= a2.get(i2));
  }
    
}

It is interesting to note that the get functions need some input. We need to temporarily store that input somewhere, before actually testing the property. We used set_input_a1 and set_input_a2 to allow echidna to store the inputs before calling get in each contract. Running Echidna in these contracts (in a single file) produce the expected results:

$ echidna-test multiple.sol Master
Analyzing contract: multiple.sol:Master
echidna_property: failed!💥  
  Call sequence, shrinking (2983/5000):
    set_threshold_a1(8)
    set_input_a1(14474011154664524427946373126085988481658748083205070504932198000989141204992)

Seed: -8613763206272600641