Echidna

[t4sk]

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.3;

contract ArrayRemoveByShifting {
    uint[] internal arr;

    function remove(uint _index) internal {
        require(_index < arr.length, "index out of bound");

        for (uint i = _index; i < arr.length - 1; i++) {
            arr[i] = arr[i + 1];
        }
        arr.pop();
    }

    // function test() external {
    //     arr = [1, 2, 3, 4, 5];
    //     remove(2);
    //     // [1, 2, 4, 5]
    //     assert(arr[0] == 1);
    //     assert(arr[1] == 2);
    //     assert(arr[2] == 4);
    //     assert(arr[3] == 5);
    //     assert(arr.length == 4);

    //     arr = [1];
    //     remove(0);
    //     // []
    //     assert(arr.length == 0);
    // }
}

contract EchidnaTestArrayShift is ArrayRemoveByShifting {
    uint[] private copy;

    event AssertionFailed();

    function test_remove(uint[] memory _arr, uint _i) public {
        require(_i < _arr.length);

        // emit AssertionFailed();

        arr = _arr;

        // reset copy
        delete copy;
        // copy elements except _i th element
        for (uint i = 0; i < arr.length; i++) {
            if (i != _i) {
                copy.push(arr[i]);
            }
        }

        remove(_i);

        if (arr.length != copy.length) {
            emit AssertionFailed();
        }

        for (uint i = 0; i < arr.length; i++) {
            if (arr[i] != copy[i]) {
                emit AssertionFailed();
            }
        }
    }
}

/*
docker pull trailofbits/eth-security-toolbox
docker run -it --rm -v $PWD:/code trailofbits/eth-security-toolbox

echidna-test ./EchidnaTestArrayShift.sol --contract EchidnaTestArrayShift --check-asserts --test-limit 5000
*/

[t4sk]

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.3;

contract ArrayRemoveByShifting {
    uint[] internal arr;

    function remove(uint _index) internal {
        require(_index < arr.length, "index out of bound");

        for (uint i = _index; i < arr.length - 1; i++) {
            arr[i] = arr[i + 1];
        }
        arr.pop();
    }

    // function test() external {
    //     arr = [1, 2, 3, 4, 5];
    //     remove(2);
    //     // [1, 2, 4, 5]
    //     assert(arr[0] == 1);
    //     assert(arr[1] == 2);
    //     assert(arr[2] == 4);
    //     assert(arr[3] == 5);
    //     assert(arr.length == 4);

    //     arr = [1];
    //     remove(0);
    //     // []
    //     assert(arr.length == 0);
    // }
}

contract EchidnaTestArrayShift is ArrayRemoveByShifting {
    uint[] private copy;

    event AssertionFailed();

    function test_remove(uint[] memory _arr, uint _i) public {
        require(_i < _arr.length);

        // emit AssertionFailed();

        arr = _arr;

        // reset copy
        delete copy;
        // copy elements except _i th element
        for (uint i = 0; i < arr.length; i++) {
            if (i != _i) {
                copy.push(arr[i]);
            }
        }

        remove(_i);

        if (arr.length != copy.length) {
            emit AssertionFailed();
        }

        for (uint i = 0; i < arr.length; i++) {
            if (arr[i] != copy[i]) {
                emit AssertionFailed();
            }
        }
    }
}

/*
docker pull trailofbits/eth-security-toolbox
docker run -it --rm -v $PWD:/code trailofbits/eth-security-toolbox

echidna-test ./EchidnaTestArrayShift.sol --contract EchidnaTestArrayShift --check-asserts --test-limit 5000
*/

[t4sk]

Echidna doesnt catch failing asserts