Add error or warning if `returns(bool)` missing in `property_...`

[iirekm]

try this.withdrawAll() {
} catch Error(string memory reason) {
    assert(false);
}

I know that I can use property_... mode to test withdrawAll, however the behavior above is not how other tools (e.g. forge test) works, and can be reason of confusion and even serious bugs if somebody misses it.

[iirekm]

What's funnier behavior of require and assert inside property... (both fail) is different that behavior in a method called by property (only assert fails). What a terrible idea, and another source of unnecessary confusion and bugs!!! One of principles in software engineering is "Principle of Least Astonishment" - this behavior completely messes with it and IMHO should be deprecated.

[elopez]

Hi! could you please elaborate on what you expected, what you observe instead and what's broken? If you can provide a complete sample test case that'd be great too.

[iirekm]

How to write invariant "in any state, user can exit the protocol and withdraw all funds"? It's possible with Certora, possible with forge test, and seems impossible with Medusa because of this misbehavior.

Most invariants are like "for all method calls this and that holds" - those are easy with Medus. But "can withdraw all" is different, because it combines "for all methods calls .. exists 'withdraw' method call such that..." , and this design choice seems to make it impossible or at least not obvious to implement it.

[iirekm]

    function property_canWithdrawAll() public {
...
        withdrawAll(); // try this.withdrawAll() as I would use in forge fuzz doesnt' help either
...
    }

function withdrawAll() public {
   require(false); // simple emulation of honeypot - property_canWithdrawAll should fail, but doesn't!!!
}

[elopez]

I get an instantly failing property with something resembling your example, so I'm not sure I follow.

contract Counter {
    function property_canWithdrawAll() public returns (bool) {
       withdrawAll();
    }

    function withdrawAll() public {
        require(false);
    }
}

...
⇾ Fuzzer stopped, test results follow below ...
⇾ [PASSED] Assertion Test: Counter.withdrawAll()
⇾ [FAILED] Property Test: Counter.property_canWithdrawAll()
...

Please check and make sure you're defining your property functions correctly. They must start with the prefix set in the configuration and return a bool value. Your property_canWithdrawAll function in your code snippet does not return bool so it won't be considered a property and you won't see "Property Test" lines on the medusa output.

[iirekm]

Finally I found the cause: function property_canWithdrawAll() public returns(bool) - works as expected. function property_canWithdrawAll() public (no returns) - doesn't work. It would be nice if Medusa emitted some error or at least warning when property_ is present but returns(bool) is missing. It's an obvious user's error.

[anishnaik]

closed by #725