search

morpho-org / pre-liquidation

Other
3 stars 1 forks source link

[Certora] Check not liquidatable position equivalence #81

Closed QGarchery closed 2 weeks ago

QGarchery commented 1 month ago

The requires computation was changed in de168dd, so now this is exactly the same as in Morpho Blue. But we could still verify that this is equivalent to checking that ltv <= LLTV.

_Originally posted by @QGarchery in https://github.com/morpho-org/pre-liquidation/pull/77#discussion_r1788645020_

colin-morpho commented 1 month ago

Done in #37, if I'm not mistaken. See, https://github.com/morpho-org/pre-liquidation/blob/98c5060b28860853c543a555b21ea8bb788b99fc/certora/specs/Reverts.spec#L132

QGarchery commented 1 month ago

Actually I'm talking about the other require-statement, where we want to show the equivalence ltv <= LLTV <=> borrowed <= collateralQuoted.wMulDown(LLTV)

Saw-mon-and-Natalie commented 1 month ago

For the proof see: https://cantina.xyz/code/3299e8a6-8ba4-4c84-a40d-0e36341104e7/findings/3#comment-31648379-6aeb-459d-bb49-4ad99097c9e5

QGarchery commented 1 month ago

Nice !

A similar proof, for the require (and it's comment) just next to it actually

colin-morpho commented 3 weeks ago

This done in #89. See https://github.com/morpho-org/pre-liquidation/blob/65ab7ba56c980c572a9108f44a3151a9079e280b/certora/specs/SafeMath.spec#L17