Formal verification wish list

[QGarchery]

List all the additional steps we could follow to improve the formal verification work:

• update to main, notably taking into account the storage refactor (done in [Certora] Updated dev with all checks enabled #373)
• fix timeouts (mostly done in [Certora] Set proverargs hashingScheme to plaininjectivity  #442, see below for more)
• refactor, file splitting and renaming (done in [Certora] Cleaning, renaming & document rules #461)
• document the rules (done in [Certora] Cleaning, renaming & document rules #461)
• document the whole verification (done in [Certora] Add README #465 and [Certora] Documentation #538)
• additional properties
  • there are no accounts with non zero borrow and with zero collateral (done in [Certora] Updated dev with all checks enabled #373, rule always collateralized)
  • assuming no reverts due to external contracts, it's always possible to completely exit a borrow position, but it requires liquidity for a supply position (done for the most part in [Certora] Liveness #451, except for the repayAll rule in [Certora] Verify that it's always possible to repay all #492)
  • liveness properties about all the main functions (done in [Certora] Complete liveness #467)
  • roundtrip property with borrow-repay (done in [Certora] Refactor ExactMath #619)
  • similar properties to the "owned/owed" properties of ExitLiquidity but for supply/borrow/supplyCollateral (see [Certora] Dev #136 (comment), done in [Certora] Assets accounting when entering a position #623)
  • a position gets healthier after a liquidation if its LTV was lower than 1 / LIF. This would ensure that the liquidation system has some breathing room to liquidate users before it leads to bad debt (done in [Certora] Liquidate buffer, with executable code #708)
  • check overflow reverting case on accrue interest (abandoned)
  • check overflow reverting case on token (abandoned)
  • check overflow reverting case on oracle (abandoned)
• improve rules
  • onlyLiquidateCanDecreaseSupplyRatio can be more specific and require that the bad debt has been realized for the ratio to have decreased (new rule liquidateWithoutBadDebtRealizationIncreasesSupplyRatio written in [Certora] Supply ratio for liquidate #622)
  • userWithoutBorrowCannotLoseCollateral can also state that only the liquidate function can make him lose collateral (new rule userCannotLoseCollateralExceptLiquidate written in [Certora] Cleaning, renaming & document rules #461)
  • supply-withdraw roundtrip with arbitrary withdraw (see [Certora] Check supply followed by withdraw is not profitable #345 (comment), done in [Certora] Refactor ExactMath #619)
  • fix timeout on liquidate for the increase borrow ratio rule (done in [Certora] Last timeouts #679)
  • fix timeout on repay for the stay healthy rule (done in [Certora] Last timeouts #679)
  • fix timeout on borrow for the stay healthy rule (done in [Certora] Last timeouts #679)
  • fix timeout on liquidate for the stay healthy rule (done in [Certora] Stay healthy liquidate #684)
• switch to compilation via IR (not planned, see [Certora] Via IR #466 (comment))
• remove munging when no longer necessary
  • remove munging on Morpho.extSloads (done in [Certora] remove extSloads munging #458)
  • check MarketParamsLib.id optimization (done in [Certora] Check id summary #491)
  • remove munging on MarketParamsLib.id (done in [Certora] Remove munging #494)
• switch back from certora-cli-beta when no longer necessary
• robustness of the verification
  • test with sanity (done in [Certora] Add basic sanity checks #599)
  • test with mutations (done in [Certora] Mutations #564)

Previous invariant lists in #96 and #256.

[QGarchery]

Completed ! 🎉