ethereum / hevm

symbolic EVM evaluator
https://hevm.dev
GNU Affero General Public License v3.0
225 stars 46 forks source link

Test fails but return no info about it #437

Closed ghost closed 7 months ago

ghost commented 8 months ago

Currently I'm using hevm to implement some tests for my graduate thesis and I'm still kinda exploring it and trying to understand the best way to handle stuff. However I got hit with the following issue: I have this prove test implementation:

 /** 
    *  @dev
    *  property ERC20-STDPROP-16 implementation
    *
    *  transferFrom calls doesn't change state unexpectedly.
    *
    *  All non-reverting calls of transferFrom(from, to, amount) that succeeds
    *  should only modify the following:
    *  - balance of address 'to'
    *  - balance of address 'from'
    *  - allowance from 'msg.sender' for the address 'from'
    */ 
    function prove_transferFromChangeState(address from, address to, uint256 amount, address unrelatedAddress) public {
        require(unrelatedAddress != from);
        require(unrelatedAddress != to);
        require(unrelatedAddress != address(0));
        require(from != to);
        require(from != address(0));
        require(to != address(0));
        require(amount > 0);
        require(amount != UINT256_MAX);

        // Setup: Mint tokens and set allowances
        token._mint(from, amount);
        token.approve(msg.sender, amount);

        // Capture initial state
        uint256 initialFromBalance = token.balanceOf(from);
        uint256 initialToBalance = token.balanceOf(to);
        uint256 initialUnrelatedBalance = token.balanceOf(unrelatedAddress);
        uint256 initialSupply = token.totalSupply();
        uint256 initialAllowance = token.allowance(from, msg.sender);

        require(initialFromBalance > 0);
        require(initialAllowance >= amount);

        // Perform the transferFrom
        bool success = token.transferFrom(from, to, amount);
        require(success, "TransferFrom failed");

        // Assert expected state changes
        assert(token.balanceOf(from) == initialFromBalance - amount);
        assert(token.balanceOf(to) == initialToBalance + amount);
        assert(token.allowance(from, msg.sender) == initialAllowance - amount);

        // Assert no unexpected state changes
        assert(token.balanceOf(unrelatedAddress) == initialUnrelatedBalance);
        assert(token.totalSupply() == initialSupply);
    }

The idea of the test is to prove that on a transferFrom call the states of some variables don't change (i.e. variables not involved in the function), so I setup the test in a way that it wouldn't revert to trim down the number of branches (hence the requires). However when I run it with hevm test - I'm using forge to build it - it simply runs for some time and the returns me a FAIL:

Running 1 tests for test/OpenZeppelinERC20.t.sol:OpenZeppelinERC20Test Exploring contract Simplifying expression Explored contract (163 branches) Checking for reachability of 76 potential property violation(s) [FAIL] prove_transferFromChangeState(address,address,uint256,address)

Failure: prove_transferFromChangeState(address,address,uint256,address)

But with no information why it failed. I'm not sure if this is on my end and I'm having the wrong approach here, but would be grateful if some help could be shared. Thanks!

ghost commented 7 months ago

I'll open another issue with a better walkthrough on how to reproduce this