Converting Failed Property Tests Into Foundry

Use Recon's built-in tool to turn a failed Echidna/Medusa test into a Foundry unit test

May 02, 2024

Why?

When you have a failing Echidna/Medusa test the output shown in the call trace is sometimes not sufficient to understand what the issue is so creating a foundry unit test with it can allow you to inspect the call trace with higher verbosity (-vvv) to figure out where exactly your test is failing.

Foundry unit tests have the addition of being much faster to run than an Echidna/Medusa job so if you have a unit test that breaks one of your properties you can use it to easily test if you’ve resolved the issue after fixing your code instead of potentially having to wait hours for an Echidna/Medusa run to test the same call trace.

Defining the Invariant

We’ll be using the default Foundry template that gets setup when you start a new Foundry project which creates the following Counter contract:

contract Counter {
    uint256 public number;

    function setNumber(uint256 newNumber) public {
        number = newNumber;
    }

    function increment() public {
        number++;
    }
}

After scaffolding our testing suite with Recon we can define the following simple invariant in our Properties contract:

function invariant_neverZero() public returns (bool) {
        return counter.number() != 0;
}

This invariant just states that the value of the number state variable in Counter is never 0. It’s not hard to see that since there is no conditional statement in setNumber, all the fuzzer will need to do is call setNumber(0) to break the invariant.

Running the Fuzzer

Medusa

Running our property test with Medusa it finds the violation in 3 seconds and gives us the following output:

From here we just need to copy the logs from the point where it states “Fuzzer stopped, test results follow below ...” which we’ll paste into the Recon Medusa tool in the Paste Medusa Logs Here text box.

Echidna

Running our property test with Echidna it also quickly breaks the invariant and gives the following output:

We copy these logs from the line “invariant_neverZero: failed!” to paste into the Recon Echidna tool in the Paste Echidna Logs Here text box.

Creating the Test

Using the logs, Recon will generate a Foundry unit test for the fuzzer used:

Test generated with the above Medusa logs

Test generated for the above Echidna logs

We can see that the Foundry tests replicate the call sequences generated in the Echidna/Medusa logs.

We can also add a prefix in the Add a Prefix for your convenience text box. Which appends the input value to the end of the test name:

Prefix gets added to the end of the test name

These can then easily be added to the CryticToFoundry contract that Recon has created for us. Adding the same assertion from our invariant tests to these unit tests allows us to replicate the functionality of the unit test in a more easily runnable format:

// medusa test: renamed to remove invariant_ keyword to not confuse foundry to run it as an invariant test
function test_neverZero() public {
        counter_setNumber(0);
        t(counter.number() != 0, "number can be 0");
}

// echidna test
function test_prefix_0() public {
        counter_setNumber(0);
        t(counter.number() != 0, "number can be 0");
}

running these tests we get violations of the assertion, leading to a failing test:

Using the verbosity flag with -vvv to run our test we can get a more detailed description of the call trace that led to our assertion failure than what was given in the Echidna/Medusa logs:

Fixing the Bug

We can now use this unit test to fix the line in the Counter contract that breaks our invariant:

function setNumber(uint256 newNumber) public {
        // added conditional statement to not allow changing number to 0
        if(newNumber != 0) {
            number = newNumber;
        }
}

and we can use our unit tests to quickly verify that we have in fact resolved the issue:

On a production codebase this would save us time as the Echidna/Medusa runs usually take longer than Foundry unit tests to run. Additionally, now that this unit test is a part of our test suite, we can add it to the test file for the Counter contract to execute every time tests are run, ensuring that any future changes do not cause this invariant to break again.

Recon