"Coverage Required" annotation

[bsamuels453]

While writing assertion-based properties, sometimes you have a property that requires a function to be called before the property can be fully validated:

    function deposit(uint256 assets) public {
        vault.deposit(assets, address(this));
    }

    function verify_withdrawRoundingDirection(uint256 tokens) public {
        require(tokens > 0);
        uint256 sharesRedeemed = vault.withdraw(tokens);
        assertGt(sharesRedeemed, 0, "withdraw() must not allow assets to be withdrawn at no cost");
    }

In the example above, the verify_withdrawRoundingDirection prop cannot be fully "explored" unless deposit() is called first. Testers must verify that all the code in the property is reached using code coverage.

It would be nice to have some kind of annotation to mark a property as "not fully tested" if full coverage is not achieved. This would raise an error at the end of the run if the annotation was not reached:

    function verify_withdrawRoundingDirection(uint256 tokens) public {
        require(tokens > 0);
        uint256 sharesRedeemed = vault.withdraw(tokens);
        assertGt(sharesRedeemed, 0, "withdraw() must not allow assets to be withdrawn at no cost");
        /// @coverageRequired
    }

[ggrieco-tob]

Uhm, it is unclear how to do it. I feel that adding assert(false) is the usual way to workaround this.

[bsamuels453]

I'm looking for the opposite though; I think it will make more sense if I describe a naive implementation of the feature;

Add new opcode "MUSTCOVER". This opcode is a no-op.

When coverage is calculated for a project, each  "MUSTCOVER" operation that has not been reached during execution at least once should raise an error. 

Example in code:
    function verify_withdrawReachableByPropertySuite(uint256 tokens) public {
        vault.withdraw(tokens);
        assembly {
            mustcover()
        }
    }

Without a feature like this, I need to manually check the coverage file to make sure Echidna was able to fully test the property.

I've been having to do this very often while testing the generic ERC4626 property suite - sometimes a vault's deposit() function cannot be executed successfully without some kind of precondition that the generic property suite is not fulfilling. In a case like this, none of the withdraw() properties are being verified (because we can't successfully deposit) & the only way for an end user to discover the problem is to inspect the coverage file.

Let me know if this makes sense, or if there might be a different way to verify a code path is reachable

[ggrieco-tob]

I think the main blocker here is that we don't know if the solc mapping will include a comment (most likely not), so crytic-compile should inject a value into the mappings, something that is not trivial to do :disappointed: