[Certora] Check Missing Reverts

morpho-org / morpho-token-upgradeable

Other

7 stars 7 forks source link

[Certora] Check Missing Reverts #98

Open colin-morpho opened 1 week ago

colin-morpho commented 1 week ago

This PR: check revert conditions. It provides rules to exhaustively check reverts conditions. The OZ specs do not check everything we'd like to verify.

Please ensure that

[x] README is updated;
[x] CI is updated;
[x] verification succeeds.

colin-morpho commented 1 week ago

As is, I dislike having that much spec files but, I'm afraid it's hard to do less without harnessing. A harness could be used to expose the internal function (_transfer, _approve, _mint, _burn) at the cost of maintaining the harness (probably minor though). They both have inconveniences, happily willing to implement suggestions 😄!