Formal verification wish list

[QGarchery]

Here is a list of properties that we can try to verify using Certora:

• there is a tree of roles: owner > curator > allocator, and owner > guardian (started in [Certora] Dev #334, finished in [Certora] Roles tree #389)
• depositing puts all the tokens into Morpho Blue (done in [Certora] Tokens #382)
• withdrawing takes all the tokens from Morpho Blue (done in [Certora] Tokens #382)
• reallocating does not change where the tokens are (done in [Certora] Tokens #382)
• cannot have more assets than the cap right after a transaction, except for donations and interest accrual (tried in [Certora] Supply cap #419 but abandoned because of tough timeouts)
• timelock is always between the bounds (done in [Certora] Consistent State #385)
• fee is always smaller than max fee (done in [Certora] Consistent State #385)
• supply queue and withdraw queue have length <= max length (done in [Certora] Consistent State #385)
• no dirty pending values (done in [Certora] Consistent pending values #387)
• pending value is different from current value (done in [Certora] Consistent pending values #387)
• withdraw queue has no duplicates (done in [Certora] Enabled flag #393)
• the enabled field tracks if a market is in the withdraw queue (done in [Certora] Enabled flag #393)
• a market can't be marked for removal and (have supply cap > 0 or have a pending cap) (done in [Certora] Forced market removal independence #399)
• cannot change timelocked variables for a given amount of time (done in [Certora] Timelock computations #409, see the corresponding computations)
• withdraw queue contains the markets with supply cap > 0 (done in [Certora] Reverts #390)
• input validation and revert condition (done in [Certora] Reverts #390)
• cannot lose fees to unset fee recipient (done in [Certora] Reverts #390)
• cannot set the the same value (done in [Certora] Reverts #390)
• prove immutability (done in [Certora] Immutability #398)
• reentrancy safety (done in [Certora] Reentrancy #396)
• hard liveness properties can withdraw all under conditions, can reallocate all supply from a market under conditions
• can pause supply, can recover from takeovers, can remove market even if it reverts (done in [Certora] First liveness properties #400)
• can change timelocked values in the specified computation time (done in [Certora] Timelock computations #409)
• additional reallocate revert conditions have been checked separately: it also reverts if a given market isn't enabled (checked in MarketInteractions.spec), and it reverts if supplied!=withdrawn (checked in Tokens.spec)
• cannot deposit nor withdraw on a non enabled market (done in [Certora] Market interactions #410)
• for any tx: the share price, totalAssets() / totalSupply(), does not decrease. This is true only assuming that underlying markets are not updated, otherwise there could be some bad debt realization or forced market removal which would break the property
• cannot bypass guardian if the guardian is responsive
• the ERC4626 properties, especially the round-trip properties, hold.

[MathisGD]

Other ideas:

• Metamorpho can't deposit on a non enabled market