Lost assets (no share price decrease)

[MathisGD]

Version of Metamorpho which does not realise bad debt.

The way it works is the following:

• at each interest accruing interaction (function which call the previous _accrueFees()), compute the new totalAssets on morpho (sum of the assets on each cap>0 market) (now called "realTotalAssets").
• if realTotalAssets increased, make totalAsset increase by the same amount (interest are always accrued, unlike in No share price decrease (1) #4).
• if realTotalAssets decreased, don't make totalAsset decrease and accumulate the missing assets in a new storage variable called lostAssets.

Important notes:

• we don't have the invariant "lostAssets = Σ bad debt realised on markets for the vault", because:
  • the lostAssets is only updated when there is an interaction with the vault. So if at t0 there is a bad debt of x, and 2x of interest is accrued between t0 and the next iteration t1, lostAssets would not be accrued at all.
  • on _deposit and _withdraw, lastTotalAssets is updated "optimistically" meaning that it can think the vault thinks it has one more assets than in reality, which can turn into lostAsset after. (see Add missing tests #23)
• we don't have the invariant "share price is increasing" as is. Indeed, if we query the share price in a view manner at t0, it's well possible that at t1 it's lower.
• "lostAssets <= totalAssets" is true but non trivial. Indeed, we need to know how Morpho handles bad debt realisation (reduces value of the balance of MM on the market) because it's not enforced in Metamorpho itself.

About the verification:

• LostAssetsNoLink assumes that Morpho is view (in order not to change the ghost variable sumBalances).
• LostAssetsLink links the concrete implementation of Morpho (necessary to prove "lostAssets <= totalAssets")

Other notes:

• now lastTotalAssets is updated twice in deposit/mint and withdraw/redeem (and events are logs twice too)
• we don't use zeroFloorsub anymore in withdraw/redeem, as it was useless (you can never withdraw more than the vault's total assets)

TODO:

• fix last two rules formal verif

[Jean-Grimal]

This means that bad debt is not taken into account in the vault share pricing (using convertToAssets as we do now to price ERC-4626 shares).

Which means that a vault with a lot of bad debt would have its shares overpriced, and a share holder could borrow almost "against nothing" if a morpho market uses those shares as collateral. (Other way to see this : someone who borrows against those shares wouldn't be liquidated if the vault occurred bad debt. And so bad debt would also occur on the market with shares as collateral)

So we should use new custom oracles to price MetaMorpho shares

[MathisGD]

So we should use new custom oracles to price MetaMorpho shares

• I think that the fair value of a vault with 1% of bad debt is not 99% of the underlying, but 100%. And on the opposite side, I think that the fair value of a vault with 50% bad debt is near zero and not 50% of the underlying.
• I don't think that it's safe at all to lend against a vault that has a lot of bad debt (at any time it can bankrupt, and then you lose everything).

So to me there is no need to change the oracle at all.

Although this should be noted somewhere in the docs: with the normal vault you just had to have a look at the potential future bad debt of a vault (=risk), and with this one you have to look at the current hole plus the potential future bad debt.

[Rubilmax]

The point is here:

Although this should be noted somewhere in the docs: with the normal vault you just had to have a look at the potential future bad debt of a vault (=risk), and with this one you have to look at the current hole plus the potential future bad debt.

the current hole

Bad debt, if significant (as defined by the oracle), should be atomically taken into account otherwise lenders can be atomically drained

[MathisGD]

Bad debt, if significant (as defined by the oracle), should be atomically taken into account otherwise lenders can be atomically drained

So it would be an oracle returning zero if the relative bad debt exceeds a certain threshold and the normal price otherwise right?

EDIT: for opening new positions, that makes sense, for liquidating no, because it means you can seize the collateral and repay nothing

[Rubilmax]

I guess it's a very relevant example of the benefit of separating the price used to open positions and the one used to close

[QGarchery]

I guess it's a very relevant example of the benefit of separating the price used to open positions and the one used to close

I would agree if we could say what would be the price used to close positions in that case. If not then there is still only one price. If we can have an oracle to close positions, then wouldn't it be a good candidate as an oracle to open positions ?

[adhusson]

revert reason changed when someone is trying to withdraw/redeem more than the vault's totalAssets (from "NotEnoughLiquidity" to "underflow")

This creates a difference in behavior between the two MM versions that has to be accounted for when using MM as a developer. I'm not sure what is gained to counterbalance that.

edit: tried it here: #18