Closed
Description
The idea is to list the invariants about the protocols. This way we will remember to add them as forge invariants or certora invariants.
Current invariant list :
- borrow is less than supply on a given market. It has to be checked with the liquidate function too. (done in [Certora] Added borrow less supply invariant #294)
- for each market, on the singleton there is at least (totalSupply - totalBorrow) borrowable tokens and the whole collateral (done in [Certora] Liquidity #304)
- only the markets with enabled LLTVs have non-zero data (done in [Certora] Only enabled lltv/irm #290)
- only the markets with enabled IRMs have non-zero data (done in [Certora] Only enabled lltv/irm #290)
- the ratio
shares / assetson a market is increasing, except in liquidate (in progress in [Certora] Verify share ratio #341) - sum_addresses(supplyShares(address)) = totalSupplyShare (done in [Certora] Dev #136)
- sum_addresses(borrowShares(address)) = totalBorrowShare (done in [Certora] Dev #136)
- sum_addresses(supplyShares(address).toAssetsDown()) <= totalSupply
This invariant is difficult to check because every user's owed assets can change at each interaction. Moreover, it can be deduced (modulo virtual assets and shares) given the 2 previous invariants by applyingtoAssetsDownon both sides. For these reasons, it has been replaced with the following property: a given user cannot withdraw more thansupplyShares(address).toAssetsDown()assets. (done in [Certora] Exit liquidity #316) - sum_addresses(borrowShares(address).toAssetsUp()) >= totalBorrow
For similar reasons as the invariant above, this invariant has been replaced with the following property: when repaying the whole position, a user is transfering more tokens thanborrowShares(address).toAssetsUp())(done in [Certora] Exit liquidity #316)
(some of the invariants were taken from comments below, and put there for easier tracking)