[Certora] Check not liquidatable position equivalence

[QGarchery]

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 #77 (comment)

[colin-morpho]

Done in #37, if I'm not mistaken. See,

pre-liquidation/certora/specs/Reverts.spec

Line 132 in 98c5060

rule preLiquidatableEquivlLtvLTPreLltv() {

[QGarchery]

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]

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

[QGarchery]

Nice !

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

[colin-morpho]

This done in #89. See

pre-liquidation/certora/specs/SafeMath.spec

Line 17 in 65ab7ba

rule borrowedLECollatQuotedTimesLLTVEqLtvLTEqLLTV {