Annotation for specifying reverts

[suhabe]

How can I write solc-verify annotations for the following function to specify that the function reverts when a>=10?

contract test {
    function add(uint256 a) public pure returns (uint256) {
        require(a < 10);
    }
}

[dddejan]

This is an interesting question/featue.

First to clarify what's going on. The current approach we take is verification modulo successfully completed transactions. So, e.g, for a function postcondition, we try to prove that for any inputs where the function terminates "as expected", the postcondition holds. Simplifying a bit, we treat "as expected" to be "no assertion failures". Reverts are treated as expected failures used for things like specifying inputs requirements. This means we use assume to model require in our logic.

In your example the require statement in essence is the specification that the function reverts when a >= 10. But, since it is in code, it doesn't really look like a spec and it cannot be used to reason modularly at call sites of the function. Also require can be written anywhere in code.

For internal functions, one can specify a function precondition that guarantees "as expected" termination (see example), but this is not exactly what's needed.

To be able to specify and reason about revert/assert failures we would need to model them with more operational detail. So yes, needs work and is probably a useful feature. We will need this eventually to be able to handle try/catch that will show in 0.6.