Medusa should extract constants from the returned values of the EVM execution

[ggrieco-tob]

This is a feature request. Medusa fails to solve the (in)famous SimpleDSChielf example. There is a bit of history about this abstracted code from MakerDAO here. I copied the code here:

contract SimpleDSChief {
    mapping(bytes32=>address) public slates;
    mapping(address=>bytes32) public votes;
    mapping(address=>uint256) public approvals;
    mapping(address=>uint256) public deposits;

    function lock(uint wad) public {
        deposits[msg.sender] = add(deposits[msg.sender], wad);
        addWeight(wad, votes[msg.sender]);
    }

    function free(uint wad) public {
        deposits[msg.sender] = sub(deposits[msg.sender], wad);
        subWeight(wad, votes[msg.sender]);
    }

    function voteYays(address yay) public returns (bytes32){
        bytes32 slate = etch(yay);
        voteSlate(slate);

        return slate;
    }

    function etch(address yay) public returns (bytes32 slate) {
        bytes32 hash = keccak256(abi.encodePacked(yay));

        slates[hash] = yay;

        return hash;
    }
    
    function voteSlate(bytes32 slate) public {
        uint weight = deposits[msg.sender];
        subWeight(weight, votes[msg.sender]);
        votes[msg.sender] = slate;
        addWeight(weight, votes[msg.sender]);
    }

    function addWeight(uint weight, bytes32 slate) internal {
        address yay = slates[slate];
        approvals[yay] = add(approvals[yay], weight);
    }

    function subWeight(uint weight, bytes32 slate) internal {
        address yay = slates[slate];
        approvals[yay] = sub(approvals[yay], weight);
    }

    function add(uint x, uint y) internal pure returns (uint z) {
        require((z = x + y) >= x);
    }

    function sub(uint x, uint y) internal pure returns (uint z) {
        require((z = x - y) <= x);
    }

    function checkAnInvariant() public {
        bytes32 senderSlate = votes[msg.sender];
        address option = slates[senderSlate];
        uint256 senderDeposit = deposits[msg.sender];
        
        assert(approvals[option] >= senderDeposit);
    }
}

To reproduce, just run:

medusa fuzz --compilation-target test.sol --target-contracts SimpleDSChief

Medusa will have a lot of trouble to break the invariant since it needs some value is dynamically produced in the votesSlate function. It was the example that pushed our tools to catch these values during the testing.

Echidna output when running the example:

checkAnInvariant(): failed!💥  
  Call sequence, shrinking 1385/5000:
    SimpleDSChief.lock(1)
    SimpleDSChief.voteSlate("\182\151]\SOfud)ID\236\239\199\141\226\184\177$\DC1vm\129\144\&7\168&\153\192rL\202#")
    SimpleDSChief.etch(0x20000)
    SimpleDSChief.checkAnInvariant()