Formal verification wish list

[QGarchery]

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

• [x] there is a tree of roles: owner > curator > allocator, and owner > guardian (started in #334, finished in #389)
• [x] depositing puts all the tokens into Morpho Blue (done in #382)
• [x] withdrawing takes all the tokens from Morpho Blue (done in #382)
• [x] reallocating does not change where the tokens are (done in #382)
• [x] cannot have more assets than the cap right after a transaction, except for donations and interest accrual (tried in #419 but abandoned because of tough timeouts)
• [x] timelock is always between the bounds (done in #385)
• [x] fee is always smaller than max fee (done in #385)
• [x] supply queue and withdraw queue have length <= max length (done in #385)
• [x] no dirty pending values (done in #387)
• [x] pending value is different from current value (done in #387)
• [x] withdraw queue has no duplicates (done in #393)
• [x] the enabled field tracks if a market is in the withdraw queue (done in #393)
• [x] a market can't be marked for removal and (have supply cap > 0 or have a pending cap) (done in #399)
• [x] cannot change timelocked variables for a given amount of time (done in #409, see the corresponding computations)
• [x] withdraw queue contains the markets with supply cap > 0 (done in #390)
• [x] input validation and revert condition (done in #390)
• [x] cannot lose fees to unset fee recipient (done in #390)
• [x] cannot set the the same value (done in #390)
• [x] prove immutability (done in #398)
• [x] reentrancy safety (done in #396)
• [x] hard liveness properties can withdraw all under conditions, can reallocate all supply from a market under conditions
• [x] can pause supply, can recover from takeovers, can remove market even if it reverts (done in #400)
• [x] can change timelocked values in the specified computation time (done in #409)
• [x] 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)
• [x] cannot deposit nor withdraw on a non enabled market (done in #410)
• [x] 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:

• [x] Metamorpho can't deposit on a non enabled market