[Certora] Verif expected reverts

morpho-org / pre-liquidation

Other

3 stars 1 forks source link

[Certora] Verif expected reverts #37

Closed colin-morpho closed 1 month ago

colin-morpho commented 2 months ago

This PR implements the specification of the related issue and resolves #26.

Please make sure of the following before accepting this PR:

[x] the verification succeeds;
[x] the README file has been updated to provide some documentation;
[x] the CI has been updated as required.

QGarchery commented 2 months ago

I think you can update your branch by doing some merging. Right now it show 54 commits

colin-morpho commented 2 months ago

@QGarchery and @MathisGD the specification nonLiquidatablePoisitionReverts introduced in commit https://github.com/morpho-org/pre-liquidation/pull/37/commits/c410c158295cbe5fbef595309cb5fa36d496afa0 succeeds the verification. However, the version of commit https://github.com/morpho-org/pre-liquidation/pull/37/commits/68bcaf661f30bbf204c6a300a86e436fd0f38f0e, updated to match the current implementation in solidity catch a possible division by zero. How should we handle this?

colin-morpho commented 1 month ago

After talking with @QGarchery, the revert check for markets(id).lastUpdate != 0 needs to be checked in a different file/config to avoid conflicts with between parametric contracts and invariants. Now the CI should pass checking many interesting properties.