Output giving a fail yet not returning a counterexample on why it failed

[ghost]

I'm using forge build to compile and hevm test --match function to run the tests

I have the following structure for my prove_ tests:

Declaring my ERC20 Token (simply OpenZeppelin implementation where I mint some tokens initially)

//OpenZeppelinERC20.sol
// SPDX-License-Identifier: MIT 
pragma solidity ^0.8.0;

import "@openzeppelin/contracts/token/ERC20/ERC20.sol";

contract OpenZeppelinERC20 is ERC20 {
    constructor(string memory name, string memory symbol, uint256 initialSupply, address deployer) ERC20(name, symbol) {
        _mint(deployer, initialSupply);
    }
}

My ERC20 properties folder where all tests should inherit

//ERC20Props.sol
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

import {Test} from "forge-std/Test.sol";
import {IERC20} from"@openzeppelin/contracts/interfaces/IERC20.sol";

abstract contract ER20Props is Test {
    address internal token;

    address[] internal holders;

    function setUp() public virtual;

    //This function is problematic for some reason
    function prop_ERC20_transferChangeState(address sender, address receiver, address other, uint256 amount) public {
        // consider other that are neither sender or receiver
        require(other != sender);
        require(other != receiver);

        // record their current balance
        uint256 oldBalanceSender   = IERC20(token).balanceOf(sender);
        uint256 oldBalanceReceiver = IERC20(token).balanceOf(receiver);
        uint256 oldBalanceOther    = IERC20(token).balanceOf(other);

        vm.prank(sender);
        IERC20(token).transfer(receiver, amount);

        if (sender != receiver) {
            assert(IERC20(token).balanceOf(sender) <= oldBalanceSender); // ensure no subtraction overflow
            assert(IERC20(token).balanceOf(sender) == oldBalanceSender - amount);
            assert(IERC20(token).balanceOf(receiver) >= oldBalanceReceiver); // ensure no addition overflow
            assert(IERC20(token).balanceOf(receiver) == oldBalanceReceiver + amount);
        } else {
            // sender and receiver may be the same
            assert(IERC20(token).balanceOf(sender) == oldBalanceSender);
            assert(IERC20(token).balanceOf(receiver) == oldBalanceReceiver);
        }

        // make sure other balance is not affected
        // if I comment out the line below the test gives me a PASS
        assert(IERC20(token).balanceOf(other) == oldBalanceOther);
    }
}

OpenZeppelin's ERC20 test file.

// OpenZeppelinERC20Tests.t.sol
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

import {OpenZeppelinERC20} from "src/OpenZeppelinERC20.sol";
import "contracts/ERC20Props.sol"; 

contract OpenZeppelinERC20Tests is ER20Props {

    function setUp() public override {
        address deployer = address(this);

        OpenZeppelinERC20 token_ = new OpenZeppelinERC20("OpenZeppelinERC20", "OpenZeppelinERC20", 1_000_000_000e18, deployer);
        token = address(token_);

        holders = new address[](3);
        holders[0] = address(0x1000);
        holders[1] = address(0x2000);
        holders[2] = address(0x3000);

        for (uint256 i = 0; i < holders.length; i++) {
            address account = holders[i];
            uint256 balance = token_.totalSupply() / 10;
            vm.prank(deployer);
            token_.transfer(account, balance);

            for(uint256 j = 0; j < i; j++) {
                address other = holders[j];
                uint256 amount = token_.totalSupply() / 10;
                vm.prank(account);
                token_.approve(other, amount);
            }
        }
    }

    function prove_transferChangeState(address receiver, address other, uint256 amount) public {
        super.prop_ERC20_transferChangeState(address(this), receiver, other, amount);
    }
}

When I run hevm test --match prove_transferChangeState it returns me the following:

Running 1 tests for test/OpenZeppelinERC20Tests.t.sol:OpenZeppelinERC20Tests Exploring contract Simplifying expression Explored contract (18 branches) Checking for reachability of 9 potential property violation(s) [FAIL] prove_transferChangeState(address,address,uint256)

Failure: prove_transferChangeState(address,address,uint256)

However if I comment out the last line of the property implementation ->assert(IERC20(token).balanceOf(other) == oldBalanceOther); the test gives me a PASS. What is the actual reason for this test to be failing?

[msooseth]

Oh, that's interesting! Thanks for the very detailed bug report, it's super-helpful. Sorry about that issue, and sorry for being so late in responding. Let me look at this the beginning of next week!

Mate

[msooseth]

@0xRalts Can you give a full run? I have a feeling it may have also printed, after that text, something along the lines of:

No reachable assertion violations, but all branches reverted
Prefix this testname with `proveFail` if this is expected

Did it? Or did it not print anything afterwards?

BTW, based on this issue, I am updating the printing so it'll be less ambiguous :)

[msooseth]

Ahhh I think I can reproduce this now! Sorry... working on it now!

[msooseth]

I think something like this can happen:

Running 2 test(s) for src/contract-bail.sol:MyContract
Exploring contract
Explored contract (2 branches)
Checking for reachability of 1 potential property violation(s)
[FAIL] prove_add_value2(address,uint256)
Exploring contract
Explored contract (3 branches)
Checking for reachability of 2 potential property violation(s)
[FAIL] prove_add_value(address,uint256)
  List of counterexaple(s) follow.
  Counterexample:
    result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
    calldata: prove_add_value2(0x0000000000000000000000000000000000001312,23158417847463239084714197001737581570653996933128112807891516801582625927989)

  List of counterexaple(s) follow.
  Counterexample:
    result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
    calldata: prove_add_value(0x0000000000000000000000000000000000000000,23158417847463239084714197001737581570653996933128112807891516801582625927989)

Which is counterintutive. I'll fix this now.

[msooseth]

I have really been making a lot of progress here. Thank you SO MUCH for highlighting this issue. I myself have been confused. It's gonna be a lot clearer from now on :)

[joaovaladares]

Hi @msooseth , I'm using this account since I could recover it.

If it still helps:

@0xRalts Can you give a full run? I have a feeling it may have also printed, after that text, something along the lines of: No reachable assertion violations, but all branches reverted Prefix this testname with proveFail if this is expected Did it? Or did it not print anything afterwards?

It didn't print anything as far as I remember. But could actually happen what you stated that was counter intuitive.

Thank you for the updates. I'm looking forward to keep up with hevm development and helping if possible!

[msooseth]

@joaovaladares Thanks for the feedback! This PR should help: https://github.com/ethereum/hevm/pull/472 Please let me know if the printed output looks more sane than before -- there is an example in the PR both of the OLD and the NEW. Let me know if you'd prefer it to be different! I am not a visual designer, but it should be at least better than what was there before :)

[joaovaladares]

I'm also not a visual designer but from a user perspective this looks way nicer!

[msooseth]

Hey @joaovaladares the related PR has now been merged, yay! Also, thanks to @zoep we got an even-nicer looking output, yay! Thanks so much for opening this issue, it really highlighted that the output was very messy indeed. Thanks again! Closing.