I'm having this famous integer overflow function within my Test code so that I'm sure it is failed and captured within the corpus.

*r  |     function inc(uint256 val) public {
*r  |         uint256 tmp = counter;
    |         unchecked {
*r  |             counter += val;
    |         }
*r  |         assert(tmp <= counter);
    |     }

How I know for sure that at some point this function got to the breaking point is that, in the result set, I have

inc(uint256): failed!💥  
  Call sequence:

and also in the corpus, I have

    "_value": "0x0",
    "_dst": "0x00a329c0648769A73afAc7F9381E08FB43dBEA72",
    "_gas'": "0xbebc20",
    "_gasprice'": "0x0",
    "_delay": [
    "_call": {
        "tag": "SolCall",
        "contents": [
                    "tag": "AbiUInt",
                    "contents": [
    "_src": "0x0000000000000000000000000000000000020000"

So my actual expectation is that, with a test as this,

*r  |     function test_transfer(uint256 amount) public {
r   |         mint(user, amount);
    |         transfer(receiver, amount);
*   |         assert(balanceOf(receiver) == amount);
    |     }

where, in the actual mint method, I don't mint anything, (which I can also see that the function is reached by echidna)

r   |     function mint(address to, uint256 amount) public onlyRole(MINTER_ROLE) {
    |         // _mint(to, amount);
    |     }

I'm expecting that, this fuzzing must break from the starting point itself and got the invariants captured within the corpus right away.

However, all I get within the tests results log is,

test_transfer(uint256):  passed! 🎉

and the corpus have many recorded invariants with random values starting from small to big integers ranging within uint256.

What am I missing here? How can I make the assertion worthwhile so that it actually captures the breaking points, and then from that point onwards, try actually minting some ERC20 and fuzz that too and at least make sure the minting of ERC20 with openzeppelin code is absolutely error free?

  • I have further extended this test and used Property mode this time, and basically put the unchecked addition method to a different contract which then inherits it by the test contract which does the actual echidna testing. There also, the failure doesn't occur; even for that value almost around the above failure (~2^256). What am I missing here? Sep 6, 2023 at 14:13


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.