Verify invariants about the protocol

[QGarchery]

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 / assets on 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 applying toAssetsDown on both sides. For these reasons, it has been replaced with the following property: a given user cannot withdraw more than supplyShares(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 than borrowShares(address).toAssetsUp()) (done in [Certora] Exit liquidity #316)

(some of the invariants were taken from comments below, and put there for easier tracking)

[MathisGD]

Some more ideas:

• sum_addresses(supplyShares(address)) = totalSupplyShare
• sum_addresses(borrowShares(address)) = totalBorrowShare
• sum_addresses(supplyShares(address).toAssets()) <= totalSupply
• sum_addresses(borrowShares(address).toAssets()) >= totalBorrow

[Jean-Grimal]

I conducted all of these tests (except for the enabled LLTVs and IRMs) and they all pass, Do you have other invariants in mind that could be tested ?

[Rubilmax]

Some more ideas:

• sum_markets(totalSupply(id) - totalBorrow(id)) <= ERC20(market.borrowableAsset).balanceOf(blue)

[pakim249CAL]

Some more ideas:

* [ ]  `sum_markets(totalSupply(id) - totalBorrow(id)) <= ERC20(market.borrowableAsset).balanceOf(blue)`

Related to this, I would also consider adding collateral to the left hand side of this assertion

[Rubilmax]

So it would be something like:

For every asset, the sum of totalSupply - totalBorrow of each market having this asset as borrowable + the sum of collateral supplied on each market having this asset as collateral should equal Blue's balance

[pakim249CAL]

Yes, except technically I believe it should be <= since it is possible that blue is sent tokens without an interaction in blue.

[Rubilmax]

So we can have equality of the invariant in tests, but only inequality in production

[Jean-Grimal]

So it would be something like:

For every asset, the sum of totalSupply - totalBorrow of each market having this asset as borrowable + the sum of collateral supplied on each market having this asset as collateral should equal Blue's balance

In #231 the equality stands

[QGarchery]

I'm closing this as I opened a general issue about formal verification to keep track of what's left to do. See #390