Make sure that liquidity is isolated from a market to another

[MerlinEgalite]

We want to avoid that because of a bad IRM or oracle, someone is able to steal money from different markets using the same asset

[MathisGD]

It's already the case now, thanks to the liquidity check. What do you want to add exactly ? Tests ? Proofs ?

[MerlinEgalite]

Proof would be great. I fear that integrators could fear that

[MathisGD]

I suggest that we open an issue with invariants idea for when we will formal prove the contract, to gather everything together (and avoid having too much issues). wdyt ? @MerlinEgalite @QGarchery

[MerlinEgalite]

Done here: #96

Closing this one

[QGarchery]

Lol I thought of the same thing, and opened #96

Thinking a little bit about it, this invariant does not seem to be verified because of the liquidate function which can reduce the total supply. This seems to be a big issue

[QGarchery]

Reopening because this particular issue is not solved I think (see comment above)

[MerlinEgalite]

I was closing not because it's solved but because you listed it on the things to verify. But I'm fine keeping it since we should fix it (it seems).

[MathisGD]

Thinking a little bit about it, this invariant does not seem to be verified because of the liquidate function which can reduce the total supply. This seems to be a big issue

The liquidation doesn't touch the totalSupply right ?

[QGarchery]

The liquidation doesn't touch the totalSupply right ?

It does when bad debt is realized

[MathisGD]

I don't think that there is an issue. Worst case scenario the withdraw reverts because there are not any assets (div by zero) but it seems ok.

[QGarchery]

I don't think that there is an issue. Worst case scenario the withdraw reverts because there are not any assets (div by zero) but it seems ok.

Yes but the issue is that we can have totalSupply[id] < totalBorrow[id], which essentially means that we have taken tokens from a market other than id

[MathisGD]

How ? the totalBorrow is also reduced when realizing bad debt

[QGarchery]

Oh yes you are right, this is beautiful !

Closing this because it will be verified in #96