Certora: verify ERC4626 round-trip properties

.github/workflows/certora.yml

@@ -18,6 +18,7 @@ jobs:
         conf:
           - ConsistentState
           - DistinctIdentifiers
+          - ERC4626
           - Enabled
           - Immutability
           - LastUpdated

certora/confs/ERC4626.conf

@@ -0,0 +1,19 @@
+{
+  "files": [
+    "certora/helpers/MetaMorphoHarness.sol"
+  ],
+  "solc": "solc-0.8.21",
+  "verify": "MetaMorphoHarness:certora/specs/ERC4626.spec",
+  "loop_iter": "2",
+  "optimistic_loop": true,
+  "prover_args": [
+    "-depth 0",
+    "-timeout 300",
+    "-smt_nonLinearArithmetic true",
+    "-backendStrategy singlerace",
+    "-solvers [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]"
+  ],
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "MetaMorpho ERC4626"
+}

certora/specs/ERC4626.spec

@@ -0,0 +1,76 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+methods {
+    function convertToShares(uint256) external returns(uint256) envfree;
+    function convertToAssets(uint256) external returns(uint256) envfree;
+    function previewDeposit(uint256) external returns(uint256) envfree;
+    function previewMint(uint256) external returns(uint256) envfree;
+    function previewWithdraw(uint256) external returns(uint256) envfree;
+    function previewRedeem(uint256) external returns(uint256) envfree;
+
+    function MetaMorpho._accruedFeeShares() internal returns (uint256, uint256) => summaryAccruedFeeShares();
+    function ERC4626._decimalsOffset() internal returns (uint8) => summaryDecimalsOffset();
+    function Math.mulDiv(uint256 x, uint256 y, uint256 denominator, Math.Rounding rounding) internal returns (uint256) => cvlMulDiv(x, y, denominator, rounding);
+}
+
+ghost uint256 gTotalAssets;
+ghost uint256 gFeeShares;
+persistent ghost uint8 gDecimalsOffset;
+
+function summaryAccruedFeeShares() returns (uint256, uint256) {
+    return (gFeeShares, gTotalAssets);
+}
+
+function summaryDecimalsOffset() returns uint8 {
+    require to_mathint(gDecimalsOffset) <= 18;
+    return gDecimalsOffset;
+}
+
+// necessary because metamorpho uses unmodelable 512 bits math.
+function cvlMulDiv(uint256 x, uint256 y, uint256 denominator, Math.Rounding rounding) returns uint256 {
+    if (rounding == Math.Rounding.Ceil || rounding == Math.Rounding.Expand) {
+        return require_uint256((x * y + (denominator - 1)) / denominator);
+    } else {
+        return require_uint256((x * y) / denominator);
+    }
+}
+
+rule convertRoundTripAssets(uint256 assets) {
+    assert convertToAssets(convertToShares(assets)) <= assets;
+}
+
+rule convertRoundTripShares(uint256 shares) {
+    assert convertToShares(convertToAssets(shares)) <= shares;
+}
+
+rule roundTripDepositRedeem(uint256 assets) {
+    assert previewRedeem(previewDeposit(assets)) <= assets;
+}
+
+rule roundTripDepositWithdraw(uint256 assets) {
+    assert previewWithdraw(assets) >= previewDeposit(assets);
+}
+
+rule roundTripRedeemDeposit(uint256 shares) {
+    assert previewDeposit(previewRedeem(shares)) <= shares;
+}
+
+rule roundTripRedeemMint(uint256 shares) {
+    assert previewMint(shares) >= previewRedeem(shares);
+}
+
+rule roundTripMintWithdraw(uint256 shares) {
+    assert previewWithdraw(previewMint(shares)) >= shares;
+}
+
+rule roundTripMintRedeem(uint256 shares) {
+    assert previewRedeem(shares) <= previewMint(shares);
+}
+
+rule roundTripWithdrawMint(uint256 assets) {
+    assert previewMint(previewWithdraw(assets)) >= assets;
+}
+
+rule roundTripWithdrawDeposit(uint256 assets) {
+    assert previewDeposit(assets) <= previewWithdraw(assets);
+}