From 88eb69acff446163d5336eb750e45a3d123b5ee0 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Fri, 24 Jul 2026 16:26:28 +0000
Subject: [PATCH 01/10] certora: verify ERC4626 round-trip properties

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01CfzVWCYX7Nrnu4P6h4EuP9
---
 .github/workflows/certora.yml |   1 +
 certora/confs/ERC4626.conf    |  19 +++++
 certora/specs/ERC4626.spec    | 151 ++++++++++++++++++++++++++++++++++
 3 files changed, 171 insertions(+)
 create mode 100644 certora/confs/ERC4626.conf
 create mode 100644 certora/specs/ERC4626.spec

diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
index 1269fa07..85a3993d 100644
--- a/.github/workflows/certora.yml
+++ b/.github/workflows/certora.yml
@@ -18,6 +18,7 @@ jobs:
         conf:
           - ConsistentState
           - DistinctIdentifiers
+          - ERC4626
           - Enabled
           - Immutability
           - LastUpdated
diff --git a/certora/confs/ERC4626.conf b/certora/confs/ERC4626.conf
new file mode 100644
index 00000000..1bbc409e
--- /dev/null
+++ b/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"
+}
diff --git a/certora/specs/ERC4626.spec b/certora/specs/ERC4626.spec
new file mode 100644
index 00000000..930eca60
--- /dev/null
+++ b/certora/specs/ERC4626.spec
@@ -0,0 +1,151 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+// Verification of the ERC4626 round-trip properties (formal-verification wish
+// list, issue #333: a16z erc4626-tests/ERC4626.prop.sol L244-318). The
+// round-trip properties state that no round trip lets a user extract more value
+// than they put in: e.g. redeem(deposit(a)) <= a, mint(withdraw(a)) >= a, etc.
+//
+// Modeling choice (documented, see the accompanying report).
+// MetaMorpho.totalAssets() sums MORPHO.expectedSupplyAssets over the whole
+// withdrawQueue and, together with the performance-fee accrual, makes every
+// conversion depend on Morpho Blue state through a loop -- the source of the
+// timeouts seen in #419. That dependency has a single funnel in the conversion
+// path: the internal _accruedFeeShares(), which is the only place
+// convert*/preview* read totalAssets() and the fee. We summarize it to return
+// an arbitrary but fixed pair of totals (gFeeShares, gTotalAssets). This is a
+// SOUND over-approximation: we prove the inequalities for every possible pair
+// of totals, hence in particular for the real ones. It also makes the
+// conversions pure arithmetic over fixed virtual totals, with no Morpho Blue
+// state and no loop.
+//
+// We additionally fix the decimals offset to 0 (an 18-decimals underlying, the
+// DECIMALS_OFFSET == 0 case) so that `10 ** _decimalsOffset()` stays concrete
+// for the SMT solver. The round-trip inequalities are offset-independent, so
+// this is a tractability scoping, not a correctness assumption; generalizing to
+// a symbolic offset is a documented follow-up.
+//
+// At fixed totals the shares/assets returned by deposit/mint/withdraw/redeem
+// equal the corresponding preview* quotes: each entry point computes its result
+// with the same _convertTo{Shares,Assets}WithTotals and the rounding
+// deposit = Floor, mint = Ceil, withdraw = Ceil, redeem = Floor. We therefore
+// verify each a16z round trip on the preview* composition at fixed totals,
+// which isolates exactly the rounding-direction correctness that guarantees no
+// round-trip profit. The fully stateful composition (calling deposit then
+// redeem with the totals updating in between) additionally requires Morpho
+// Blue's supply accounting and is left to iterate against CI.
+
+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;
+
+    // Cut the Morpho Blue-dependent, fee-dependent totals to fixed ghosts (see header).
+    function _accruedFeeShares() internal returns (uint256, uint256) => summaryAccruedFeeShares();
+    // Keep `10 ** _decimalsOffset()` concrete for the SMT solver (see header).
+    function _decimalsOffset() internal returns (uint8) => summaryDecimalsOffset();
+    // Replace OZ's 512-bit assembly mulDiv (which the conversions use, and which
+    // the SMT solver cannot reason about for these lemmas) by its exact
+    // mathematical meaning. Sound: cvlMulDiv is floor/ceil of x*y/denominator.
+    function Math.mulDiv(uint256 x, uint256 y, uint256 denominator, Math.Rounding rounding) internal returns (uint256) => cvlMulDiv(x, y, denominator, rounding);
+}
+
+// Arbitrary but fixed virtual totals shared by every conversion in a rule.
+ghost uint256 gTotalAssets;
+ghost uint256 gFeeShares;
+
+function summaryAccruedFeeShares() returns (uint256, uint256) {
+    return (gFeeShares, gTotalAssets);
+}
+
+function summaryDecimalsOffset() returns uint8 {
+    return 0;
+}
+
+// Exact floor/ceil semantics of x * y / denominator. `require_uint256` models
+// OZ mulDiv reverting when the result does not fit in a uint256; all call sites
+// here have denominator >= 1 (newTotalAssets + 1, newTotalSupply + 1).
+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);
+    }
+}
+
+// convertToAssets is a left inverse of convertToShares up to rounding: converting
+// assets to shares and back never yields more assets than you started with.
+rule convertRoundTripAssets(uint256 assets) {
+    uint256 shares = convertToShares(assets);
+    uint256 assets2 = convertToAssets(shares);
+    assert assets2 <= assets;
+}
+
+// Symmetric conversion lemma for shares.
+rule convertRoundTripShares(uint256 shares) {
+    uint256 assets = convertToAssets(shares);
+    uint256 shares2 = convertToShares(assets);
+    assert shares2 <= shares;
+}
+
+// a16z prop_RT_deposit_redeem (L249-255): redeem(deposit(a)) <= a.
+rule roundTripDepositRedeem(uint256 assets) {
+    uint256 shares = previewDeposit(assets);
+    uint256 assets2 = previewRedeem(shares);
+    assert assets2 <= assets;
+}
+
+// a16z prop_RT_deposit_withdraw (L257-265): the shares burned by withdraw(a) are
+// at least the shares minted by deposit(a).
+rule roundTripDepositWithdraw(uint256 assets) {
+    uint256 shares1 = previewDeposit(assets);
+    uint256 shares2 = previewWithdraw(assets);
+    assert shares2 >= shares1;
+}
+
+// a16z prop_RT_redeem_deposit (L267-273): deposit(redeem(s)) <= s.
+rule roundTripRedeemDeposit(uint256 shares) {
+    uint256 assets = previewRedeem(shares);
+    uint256 shares2 = previewDeposit(assets);
+    assert shares2 <= shares;
+}
+
+// a16z prop_RT_redeem_mint (L275-283): the assets paid by mint(s) are at least
+// the assets returned by redeem(s).
+rule roundTripRedeemMint(uint256 shares) {
+    uint256 assets1 = previewRedeem(shares);
+    uint256 assets2 = previewMint(shares);
+    assert assets2 >= assets1;
+}
+
+// a16z prop_RT_mint_withdraw (L285-291): withdraw(mint(s)) >= s.
+rule roundTripMintWithdraw(uint256 shares) {
+    uint256 assets = previewMint(shares);
+    uint256 shares2 = previewWithdraw(assets);
+    assert shares2 >= shares;
+}
+
+// a16z prop_RT_mint_redeem (L293-301): the assets returned by redeem(s) are at
+// most the assets paid by mint(s).
+rule roundTripMintRedeem(uint256 shares) {
+    uint256 assets1 = previewMint(shares);
+    uint256 assets2 = previewRedeem(shares);
+    assert assets2 <= assets1;
+}
+
+// a16z prop_RT_withdraw_mint (L303-309): mint(withdraw(a)) >= a.
+rule roundTripWithdrawMint(uint256 assets) {
+    uint256 shares = previewWithdraw(assets);
+    uint256 assets2 = previewMint(shares);
+    assert assets2 >= assets;
+}
+
+// a16z prop_RT_withdraw_deposit (L311-318): the shares minted by deposit(a) are
+// at most the shares burned by withdraw(a).
+rule roundTripWithdrawDeposit(uint256 assets) {
+    uint256 shares1 = previewWithdraw(assets);
+    uint256 shares2 = previewDeposit(assets);
+    assert shares2 <= shares1;
+}

From ac936c6da3062a8e37f41fead115bd2330dca329 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Fri, 24 Jul 2026 17:15:42 +0000
Subject: [PATCH 02/10] certora: fix inherited internal method summary
 receivers in ERC4626 spec

---
 certora/specs/ERC4626.spec | 79 ++++++++++----------------------------
 1 file changed, 20 insertions(+), 59 deletions(-)

diff --git a/certora/specs/ERC4626.spec b/certora/specs/ERC4626.spec
index 930eca60..3edd0d3f 100644
--- a/certora/specs/ERC4626.spec
+++ b/certora/specs/ERC4626.spec
@@ -1,38 +1,13 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 
-// Verification of the ERC4626 round-trip properties (formal-verification wish
-// list, issue #333: a16z erc4626-tests/ERC4626.prop.sol L244-318). The
-// round-trip properties state that no round trip lets a user extract more value
-// than they put in: e.g. redeem(deposit(a)) <= a, mint(withdraw(a)) >= a, etc.
-//
-// Modeling choice (documented, see the accompanying report).
-// MetaMorpho.totalAssets() sums MORPHO.expectedSupplyAssets over the whole
-// withdrawQueue and, together with the performance-fee accrual, makes every
-// conversion depend on Morpho Blue state through a loop -- the source of the
-// timeouts seen in #419. That dependency has a single funnel in the conversion
-// path: the internal _accruedFeeShares(), which is the only place
-// convert*/preview* read totalAssets() and the fee. We summarize it to return
-// an arbitrary but fixed pair of totals (gFeeShares, gTotalAssets). This is a
-// SOUND over-approximation: we prove the inequalities for every possible pair
-// of totals, hence in particular for the real ones. It also makes the
-// conversions pure arithmetic over fixed virtual totals, with no Morpho Blue
-// state and no loop.
-//
-// We additionally fix the decimals offset to 0 (an 18-decimals underlying, the
-// DECIMALS_OFFSET == 0 case) so that `10 ** _decimalsOffset()` stays concrete
-// for the SMT solver. The round-trip inequalities are offset-independent, so
-// this is a tractability scoping, not a correctness assumption; generalizing to
-// a symbolic offset is a documented follow-up.
-//
-// At fixed totals the shares/assets returned by deposit/mint/withdraw/redeem
-// equal the corresponding preview* quotes: each entry point computes its result
-// with the same _convertTo{Shares,Assets}WithTotals and the rounding
-// deposit = Floor, mint = Ceil, withdraw = Ceil, redeem = Floor. We therefore
-// verify each a16z round trip on the preview* composition at fixed totals,
-// which isolates exactly the rounding-direction correctness that guarantees no
-// round-trip profit. The fully stateful composition (calling deposit then
-// redeem with the totals updating in between) additionally requires Morpho
-// Blue's supply accounting and is left to iterate against CI.
+// ERC4626 round-trip properties (issue #333, a16z erc4626-tests/ERC4626.prop.sol
+// L244-318): no round trip lets a user extract more value than they put in, e.g.
+// redeem(deposit(a)) <= a and mint(withdraw(a)) >= a. The Morpho Blue- and
+// fee-dependent totals are summarized to an arbitrary but fixed pair (a sound
+// over-approximation that removes the Morpho Blue state and loop behind
+// _accruedFeeShares), the decimals offset is fixed to 0 to keep
+// 10 ** _decimalsOffset() concrete, and OZ's 512-bit mulDiv is replaced by its
+// exact floor/ceil meaning.
 
 methods {
     function convertToShares(uint256) external returns(uint256) envfree;
@@ -42,17 +17,11 @@ methods {
     function previewWithdraw(uint256) external returns(uint256) envfree;
     function previewRedeem(uint256) external returns(uint256) envfree;
 
-    // Cut the Morpho Blue-dependent, fee-dependent totals to fixed ghosts (see header).
-    function _accruedFeeShares() internal returns (uint256, uint256) => summaryAccruedFeeShares();
-    // Keep `10 ** _decimalsOffset()` concrete for the SMT solver (see header).
-    function _decimalsOffset() internal returns (uint8) => summaryDecimalsOffset();
-    // Replace OZ's 512-bit assembly mulDiv (which the conversions use, and which
-    // the SMT solver cannot reason about for these lemmas) by its exact
-    // mathematical meaning. Sound: cvlMulDiv is floor/ceil of x*y/denominator.
+    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);
 }
 
-// Arbitrary but fixed virtual totals shared by every conversion in a rule.
 ghost uint256 gTotalAssets;
 ghost uint256 gFeeShares;
 
@@ -64,9 +33,6 @@ function summaryDecimalsOffset() returns uint8 {
     return 0;
 }
 
-// Exact floor/ceil semantics of x * y / denominator. `require_uint256` models
-// OZ mulDiv reverting when the result does not fit in a uint256; all call sites
-// here have denominator >= 1 (newTotalAssets + 1, newTotalSupply + 1).
 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);
@@ -75,75 +41,70 @@ function cvlMulDiv(uint256 x, uint256 y, uint256 denominator, Math.Rounding roun
     }
 }
 
-// convertToAssets is a left inverse of convertToShares up to rounding: converting
-// assets to shares and back never yields more assets than you started with.
+// convertToAssets(convertToShares(a)) <= a.
 rule convertRoundTripAssets(uint256 assets) {
     uint256 shares = convertToShares(assets);
     uint256 assets2 = convertToAssets(shares);
     assert assets2 <= assets;
 }
 
-// Symmetric conversion lemma for shares.
+// convertToShares(convertToAssets(s)) <= s.
 rule convertRoundTripShares(uint256 shares) {
     uint256 assets = convertToAssets(shares);
     uint256 shares2 = convertToShares(assets);
     assert shares2 <= shares;
 }
 
-// a16z prop_RT_deposit_redeem (L249-255): redeem(deposit(a)) <= a.
+// redeem(deposit(a)) <= a.
 rule roundTripDepositRedeem(uint256 assets) {
     uint256 shares = previewDeposit(assets);
     uint256 assets2 = previewRedeem(shares);
     assert assets2 <= assets;
 }
 
-// a16z prop_RT_deposit_withdraw (L257-265): the shares burned by withdraw(a) are
-// at least the shares minted by deposit(a).
+// withdraw(a) burns at least as many shares as deposit(a) mints.
 rule roundTripDepositWithdraw(uint256 assets) {
     uint256 shares1 = previewDeposit(assets);
     uint256 shares2 = previewWithdraw(assets);
     assert shares2 >= shares1;
 }
 
-// a16z prop_RT_redeem_deposit (L267-273): deposit(redeem(s)) <= s.
+// deposit(redeem(s)) <= s.
 rule roundTripRedeemDeposit(uint256 shares) {
     uint256 assets = previewRedeem(shares);
     uint256 shares2 = previewDeposit(assets);
     assert shares2 <= shares;
 }
 
-// a16z prop_RT_redeem_mint (L275-283): the assets paid by mint(s) are at least
-// the assets returned by redeem(s).
+// mint(s) pays at least as many assets as redeem(s) returns.
 rule roundTripRedeemMint(uint256 shares) {
     uint256 assets1 = previewRedeem(shares);
     uint256 assets2 = previewMint(shares);
     assert assets2 >= assets1;
 }
 
-// a16z prop_RT_mint_withdraw (L285-291): withdraw(mint(s)) >= s.
+// withdraw(mint(s)) >= s.
 rule roundTripMintWithdraw(uint256 shares) {
     uint256 assets = previewMint(shares);
     uint256 shares2 = previewWithdraw(assets);
     assert shares2 >= shares;
 }
 
-// a16z prop_RT_mint_redeem (L293-301): the assets returned by redeem(s) are at
-// most the assets paid by mint(s).
+// redeem(s) returns at most as many assets as mint(s) pays.
 rule roundTripMintRedeem(uint256 shares) {
     uint256 assets1 = previewMint(shares);
     uint256 assets2 = previewRedeem(shares);
     assert assets2 <= assets1;
 }
 
-// a16z prop_RT_withdraw_mint (L303-309): mint(withdraw(a)) >= a.
+// mint(withdraw(a)) >= a.
 rule roundTripWithdrawMint(uint256 assets) {
     uint256 shares = previewWithdraw(assets);
     uint256 assets2 = previewMint(shares);
     assert assets2 >= assets;
 }
 
-// a16z prop_RT_withdraw_deposit (L311-318): the shares minted by deposit(a) are
-// at most the shares burned by withdraw(a).
+// deposit(a) mints at most as many shares as withdraw(a) burns.
 rule roundTripWithdrawDeposit(uint256 assets) {
     uint256 shares1 = previewWithdraw(assets);
     uint256 shares2 = previewDeposit(assets);

From 1dab280e6c0aaf9c191f7fe2012d9741cc58fc2d Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Fri, 24 Jul 2026 17:46:29 +0000
Subject: [PATCH 03/10] certora: inline ERC4626 round-trip rules to one-liners

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01CfzVWCYX7Nrnu4P6h4EuP9
---
 certora/specs/ERC4626.spec | 60 +++++++-------------------------------
 1 file changed, 10 insertions(+), 50 deletions(-)

diff --git a/certora/specs/ERC4626.spec b/certora/specs/ERC4626.spec
index 3edd0d3f..dc71788c 100644
--- a/certora/specs/ERC4626.spec
+++ b/certora/specs/ERC4626.spec
@@ -42,71 +42,31 @@ function cvlMulDiv(uint256 x, uint256 y, uint256 denominator, Math.Rounding roun
 }
 
 // convertToAssets(convertToShares(a)) <= a.
-rule convertRoundTripAssets(uint256 assets) {
-    uint256 shares = convertToShares(assets);
-    uint256 assets2 = convertToAssets(shares);
-    assert assets2 <= assets;
-}
+rule convertRoundTripAssets(uint256 assets) { assert convertToAssets(convertToShares(assets)) <= assets; }
 
 // convertToShares(convertToAssets(s)) <= s.
-rule convertRoundTripShares(uint256 shares) {
-    uint256 assets = convertToAssets(shares);
-    uint256 shares2 = convertToShares(assets);
-    assert shares2 <= shares;
-}
+rule convertRoundTripShares(uint256 shares) { assert convertToShares(convertToAssets(shares)) <= shares; }
 
 // redeem(deposit(a)) <= a.
-rule roundTripDepositRedeem(uint256 assets) {
-    uint256 shares = previewDeposit(assets);
-    uint256 assets2 = previewRedeem(shares);
-    assert assets2 <= assets;
-}
+rule roundTripDepositRedeem(uint256 assets) { assert previewRedeem(previewDeposit(assets)) <= assets; }
 
 // withdraw(a) burns at least as many shares as deposit(a) mints.
-rule roundTripDepositWithdraw(uint256 assets) {
-    uint256 shares1 = previewDeposit(assets);
-    uint256 shares2 = previewWithdraw(assets);
-    assert shares2 >= shares1;
-}
+rule roundTripDepositWithdraw(uint256 assets) { assert previewWithdraw(assets) >= previewDeposit(assets); }
 
 // deposit(redeem(s)) <= s.
-rule roundTripRedeemDeposit(uint256 shares) {
-    uint256 assets = previewRedeem(shares);
-    uint256 shares2 = previewDeposit(assets);
-    assert shares2 <= shares;
-}
+rule roundTripRedeemDeposit(uint256 shares) { assert previewDeposit(previewRedeem(shares)) <= shares; }
 
 // mint(s) pays at least as many assets as redeem(s) returns.
-rule roundTripRedeemMint(uint256 shares) {
-    uint256 assets1 = previewRedeem(shares);
-    uint256 assets2 = previewMint(shares);
-    assert assets2 >= assets1;
-}
+rule roundTripRedeemMint(uint256 shares) { assert previewMint(shares) >= previewRedeem(shares); }
 
 // withdraw(mint(s)) >= s.
-rule roundTripMintWithdraw(uint256 shares) {
-    uint256 assets = previewMint(shares);
-    uint256 shares2 = previewWithdraw(assets);
-    assert shares2 >= shares;
-}
+rule roundTripMintWithdraw(uint256 shares) { assert previewWithdraw(previewMint(shares)) >= shares; }
 
 // redeem(s) returns at most as many assets as mint(s) pays.
-rule roundTripMintRedeem(uint256 shares) {
-    uint256 assets1 = previewMint(shares);
-    uint256 assets2 = previewRedeem(shares);
-    assert assets2 <= assets1;
-}
+rule roundTripMintRedeem(uint256 shares) { assert previewRedeem(shares) <= previewMint(shares); }
 
 // mint(withdraw(a)) >= a.
-rule roundTripWithdrawMint(uint256 assets) {
-    uint256 shares = previewWithdraw(assets);
-    uint256 assets2 = previewMint(shares);
-    assert assets2 >= assets;
-}
+rule roundTripWithdrawMint(uint256 assets) { assert previewMint(previewWithdraw(assets)) >= assets; }
 
 // deposit(a) mints at most as many shares as withdraw(a) burns.
-rule roundTripWithdrawDeposit(uint256 assets) {
-    uint256 shares1 = previewWithdraw(assets);
-    uint256 shares2 = previewDeposit(assets);
-    assert shares2 <= shares1;
-}
+rule roundTripWithdrawDeposit(uint256 assets) { assert previewDeposit(assets) <= previewWithdraw(assets); }

From cae88ee070402d9c63317004fe2c1a46e8515792 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Fri, 24 Jul 2026 18:01:24 +0000
Subject: [PATCH 04/10] certora: format ERC4626 rules as blocks, drop per-rule
 comments

---
 certora/specs/ERC4626.spec | 50 +++++++++++++++++++++++---------------
 1 file changed, 30 insertions(+), 20 deletions(-)

diff --git a/certora/specs/ERC4626.spec b/certora/specs/ERC4626.spec
index dc71788c..7bb70b74 100644
--- a/certora/specs/ERC4626.spec
+++ b/certora/specs/ERC4626.spec
@@ -41,32 +41,42 @@ function cvlMulDiv(uint256 x, uint256 y, uint256 denominator, Math.Rounding roun
     }
 }
 
-// convertToAssets(convertToShares(a)) <= a.
-rule convertRoundTripAssets(uint256 assets) { assert convertToAssets(convertToShares(assets)) <= assets; }
+rule convertRoundTripAssets(uint256 assets) {
+    assert convertToAssets(convertToShares(assets)) <= assets;
+}
 
-// convertToShares(convertToAssets(s)) <= s.
-rule convertRoundTripShares(uint256 shares) { assert convertToShares(convertToAssets(shares)) <= shares; }
+rule convertRoundTripShares(uint256 shares) {
+    assert convertToShares(convertToAssets(shares)) <= shares;
+}
 
-// redeem(deposit(a)) <= a.
-rule roundTripDepositRedeem(uint256 assets) { assert previewRedeem(previewDeposit(assets)) <= assets; }
+rule roundTripDepositRedeem(uint256 assets) {
+    assert previewRedeem(previewDeposit(assets)) <= assets;
+}
 
-// withdraw(a) burns at least as many shares as deposit(a) mints.
-rule roundTripDepositWithdraw(uint256 assets) { assert previewWithdraw(assets) >= previewDeposit(assets); }
+rule roundTripDepositWithdraw(uint256 assets) {
+    assert previewWithdraw(assets) >= previewDeposit(assets);
+}
 
-// deposit(redeem(s)) <= s.
-rule roundTripRedeemDeposit(uint256 shares) { assert previewDeposit(previewRedeem(shares)) <= shares; }
+rule roundTripRedeemDeposit(uint256 shares) {
+    assert previewDeposit(previewRedeem(shares)) <= shares;
+}
 
-// mint(s) pays at least as many assets as redeem(s) returns.
-rule roundTripRedeemMint(uint256 shares) { assert previewMint(shares) >= previewRedeem(shares); }
+rule roundTripRedeemMint(uint256 shares) {
+    assert previewMint(shares) >= previewRedeem(shares);
+}
 
-// withdraw(mint(s)) >= s.
-rule roundTripMintWithdraw(uint256 shares) { assert previewWithdraw(previewMint(shares)) >= shares; }
+rule roundTripMintWithdraw(uint256 shares) {
+    assert previewWithdraw(previewMint(shares)) >= shares;
+}
 
-// redeem(s) returns at most as many assets as mint(s) pays.
-rule roundTripMintRedeem(uint256 shares) { assert previewRedeem(shares) <= previewMint(shares); }
+rule roundTripMintRedeem(uint256 shares) {
+    assert previewRedeem(shares) <= previewMint(shares);
+}
 
-// mint(withdraw(a)) >= a.
-rule roundTripWithdrawMint(uint256 assets) { assert previewMint(previewWithdraw(assets)) >= assets; }
+rule roundTripWithdrawMint(uint256 assets) {
+    assert previewMint(previewWithdraw(assets)) >= assets;
+}
 
-// deposit(a) mints at most as many shares as withdraw(a) burns.
-rule roundTripWithdrawDeposit(uint256 assets) { assert previewDeposit(assets) <= previewWithdraw(assets); }
+rule roundTripWithdrawDeposit(uint256 assets) {
+    assert previewDeposit(assets) <= previewWithdraw(assets);
+}

From 263baeb4d9d095856b4b2fa704a3c994a43fd3c6 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Fri, 31 Jul 2026 16:47:28 +0000
Subject: [PATCH 05/10] certora: generalize ERC4626 round-trips to arbitrary
 decimals offset

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01CfzVWCYX7Nrnu4P6h4EuP9
---
 certora/specs/ERC4626.spec | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/certora/specs/ERC4626.spec b/certora/specs/ERC4626.spec
index 7bb70b74..138ffd00 100644
--- a/certora/specs/ERC4626.spec
+++ b/certora/specs/ERC4626.spec
@@ -5,9 +5,12 @@
 // redeem(deposit(a)) <= a and mint(withdraw(a)) >= a. The Morpho Blue- and
 // fee-dependent totals are summarized to an arbitrary but fixed pair (a sound
 // over-approximation that removes the Morpho Blue state and loop behind
-// _accruedFeeShares), the decimals offset is fixed to 0 to keep
-// 10 ** _decimalsOffset() concrete, and OZ's 512-bit mulDiv is replaced by its
-// exact floor/ceil meaning.
+// _accruedFeeShares), the decimals offset is an arbitrary but fixed value bounded
+// to its real 0..18 range (DECIMALS_OFFSET = 18.zeroFloorSub(assetDecimals) in the
+// constructor) so the round trips are proven for any decimals offset rather than
+// only 0; the bound also keeps the symbolic-exponent 10 ** _decimalsOffset() term
+// away from overflow-revert paths and within uint256. OZ's 512-bit mulDiv is
+// replaced by its exact floor/ceil meaning.
 
 methods {
     function convertToShares(uint256) external returns(uint256) envfree;
@@ -24,13 +27,15 @@ methods {
 
 ghost uint256 gTotalAssets;
 ghost uint256 gFeeShares;
+persistent ghost uint8 gDecimalsOffset;
 
 function summaryAccruedFeeShares() returns (uint256, uint256) {
     return (gFeeShares, gTotalAssets);
 }
 
 function summaryDecimalsOffset() returns uint8 {
-    return 0;
+    require to_mathint(gDecimalsOffset) <= 18;
+    return gDecimalsOffset;
 }
 
 function cvlMulDiv(uint256 x, uint256 y, uint256 denominator, Math.Rounding rounding) returns uint256 {

From cd47e8994de464edf3e822773ab7371278cf7ea3 Mon Sep 17 00:00:00 2001
From: MathisGD <74971347+MathisGD@users.noreply.github.com>
Date: Fri, 31 Jul 2026 19:15:16 +0200
Subject: [PATCH 06/10] Apply suggestion from @MathisGD

Signed-off-by: MathisGD <74971347+MathisGD@users.noreply.github.com>
---
 certora/specs/ERC4626.spec | 12 ------------
 1 file changed, 12 deletions(-)

diff --git a/certora/specs/ERC4626.spec b/certora/specs/ERC4626.spec
index 138ffd00..a61a8170 100644
--- a/certora/specs/ERC4626.spec
+++ b/certora/specs/ERC4626.spec
@@ -1,17 +1,5 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 
-// ERC4626 round-trip properties (issue #333, a16z erc4626-tests/ERC4626.prop.sol
-// L244-318): no round trip lets a user extract more value than they put in, e.g.
-// redeem(deposit(a)) <= a and mint(withdraw(a)) >= a. The Morpho Blue- and
-// fee-dependent totals are summarized to an arbitrary but fixed pair (a sound
-// over-approximation that removes the Morpho Blue state and loop behind
-// _accruedFeeShares), the decimals offset is an arbitrary but fixed value bounded
-// to its real 0..18 range (DECIMALS_OFFSET = 18.zeroFloorSub(assetDecimals) in the
-// constructor) so the round trips are proven for any decimals offset rather than
-// only 0; the bound also keeps the symbolic-exponent 10 ** _decimalsOffset() term
-// away from overflow-revert paths and within uint256. OZ's 512-bit mulDiv is
-// replaced by its exact floor/ceil meaning.
-
 methods {
     function convertToShares(uint256) external returns(uint256) envfree;
     function convertToAssets(uint256) external returns(uint256) envfree;

From e9bb08548b701e9650915632392604bcb0ec097f Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Fri, 31 Jul 2026 17:31:09 +0000
Subject: [PATCH 07/10] certora: prove Math.mulDiv matches basic floor/ceil
 (discharge summary)

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01CfzVWCYX7Nrnu4P6h4EuP9
---
 .github/workflows/certora.yml         |  1 +
 certora/confs/MulDivCorrectness.conf  | 19 ++++++++++++
 certora/helpers/MetaMorphoHarness.sol |  8 +++++
 certora/specs/MulDivCorrectness.spec  | 44 +++++++++++++++++++++++++++
 4 files changed, 72 insertions(+)
 create mode 100644 certora/confs/MulDivCorrectness.conf
 create mode 100644 certora/specs/MulDivCorrectness.spec

diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
index 85a3993d..140d7b19 100644
--- a/.github/workflows/certora.yml
+++ b/.github/workflows/certora.yml
@@ -24,6 +24,7 @@ jobs:
           - LastUpdated
           - Liveness
           - MarketInteractions
+          - MulDivCorrectness
           - PendingValues
           - Range
           - Reentrancy
diff --git a/certora/confs/MulDivCorrectness.conf b/certora/confs/MulDivCorrectness.conf
new file mode 100644
index 00000000..3b6a1d5b
--- /dev/null
+++ b/certora/confs/MulDivCorrectness.conf
@@ -0,0 +1,19 @@
+{
+  "files": [
+    "certora/helpers/MetaMorphoHarness.sol"
+  ],
+  "solc": "solc-0.8.21",
+  "verify": "MetaMorphoHarness:certora/specs/MulDivCorrectness.spec",
+  "loop_iter": "2",
+  "optimistic_loop": true,
+  "prover_args": [
+    "-depth 0",
+    "-timeout 600",
+    "-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 MulDivCorrectness"
+}
diff --git a/certora/helpers/MetaMorphoHarness.sol b/certora/helpers/MetaMorphoHarness.sol
index c812670a..3c18742e 100644
--- a/certora/helpers/MetaMorphoHarness.sol
+++ b/certora/helpers/MetaMorphoHarness.sol
@@ -37,6 +37,14 @@ contract MetaMorphoHarness is MetaMorpho {
         return pendingCap[id];
     }
 
+    function mulDivWrapper(uint256 x, uint256 y, uint256 denominator, Math.Rounding rounding)
+        external
+        pure
+        returns (uint256)
+    {
+        return Math.mulDiv(x, y, denominator, rounding);
+    }
+
     function minTimelock() external pure returns (uint256) {
         return ConstantsLib.MIN_TIMELOCK;
     }
diff --git a/certora/specs/MulDivCorrectness.spec b/certora/specs/MulDivCorrectness.spec
new file mode 100644
index 00000000..55d9d5be
--- /dev/null
+++ b/certora/specs/MulDivCorrectness.spec
@@ -0,0 +1,44 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+// Intermediate lemma: prove that OpenZeppelin's real 512-bit `Math.mulDiv`
+// returns the same VALUE as the basic floor/ceil `cvlMulDiv` used as a summary
+// in ERC4626.spec. This discharges the `Math.mulDiv => cvlMulDiv` summary,
+// turning it from an assumption into a proven-faithful abstraction.
+//
+// Safety only: we assert the returned value is correct ON THE NON-REVERTING
+// PATH. We do NOT prove liveness (i.e. that mulDiv returns whenever the exact
+// result fits in a uint256). `Math.mulDiv` is intentionally NOT summarized in
+// this spec, so the real implementation is what gets verified.
+
+methods {
+    function mulDivWrapper(uint256 x, uint256 y, uint256 denominator, Math.Rounding rounding)
+        external returns (uint256) envfree;
+}
+
+// Floor: rounds toward negative infinity == exact mathint floor of (x*y)/d.
+rule mulDivFloorValue(uint256 x, uint256 y, uint256 d) {
+    require d != 0;
+    uint256 result = mulDivWrapper@withrevert(x, y, d, Math.Rounding.Floor);
+    assert !lastReverted => result == require_uint256((x * y) / d);
+}
+
+// Trunc: for non-negative operands, truncation toward zero == floor.
+rule mulDivTruncValue(uint256 x, uint256 y, uint256 d) {
+    require d != 0;
+    uint256 result = mulDivWrapper@withrevert(x, y, d, Math.Rounding.Trunc);
+    assert !lastReverted => result == require_uint256((x * y) / d);
+}
+
+// Ceil: rounds toward positive infinity == exact mathint ceil of (x*y)/d.
+rule mulDivCeilValue(uint256 x, uint256 y, uint256 d) {
+    require d != 0;
+    uint256 result = mulDivWrapper@withrevert(x, y, d, Math.Rounding.Ceil);
+    assert !lastReverted => result == require_uint256((x * y + (d - 1)) / d);
+}
+
+// Expand: for non-negative operands, rounding away from zero == ceil.
+rule mulDivExpandValue(uint256 x, uint256 y, uint256 d) {
+    require d != 0;
+    uint256 result = mulDivWrapper@withrevert(x, y, d, Math.Rounding.Expand);
+    assert !lastReverted => result == require_uint256((x * y + (d - 1)) / d);
+}

From 2fe19d0e32be5be314ef503e8df279764195b80d Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Fri, 31 Jul 2026 17:35:26 +0000
Subject: [PATCH 08/10] certora: prove mulDiv via tight two-sided bounds (more
 SMT-tractable)

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01CfzVWCYX7Nrnu4P6h4EuP9
---
 certora/specs/MulDivCorrectness.spec | 44 +++++++++++++++++++---------
 1 file changed, 30 insertions(+), 14 deletions(-)

diff --git a/certora/specs/MulDivCorrectness.spec b/certora/specs/MulDivCorrectness.spec
index 55d9d5be..7f247870 100644
--- a/certora/specs/MulDivCorrectness.spec
+++ b/certora/specs/MulDivCorrectness.spec
@@ -1,14 +1,26 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 
 // Intermediate lemma: prove that OpenZeppelin's real 512-bit `Math.mulDiv`
-// returns the same VALUE as the basic floor/ceil `cvlMulDiv` used as a summary
-// in ERC4626.spec. This discharges the `Math.mulDiv => cvlMulDiv` summary,
+// rounds exactly like the basic floor/ceil `cvlMulDiv` used as a summary in
+// ERC4626.spec. This discharges the `Math.mulDiv => cvlMulDiv` summary,
 // turning it from an assumption into a proven-faithful abstraction.
 //
-// Safety only: we assert the returned value is correct ON THE NON-REVERTING
-// PATH. We do NOT prove liveness (i.e. that mulDiv returns whenever the exact
-// result fits in a uint256). `Math.mulDiv` is intentionally NOT summarized in
-// this spec, so the real implementation is what gets verified.
+// Strength: instead of a single mathint-division equality
+// (`res == (x*y)/d`), which forces the SMT solver to reason about division of
+// a 512-bit product and tends to time out, we prove the two TIGHT two-sided
+// multiplicative bounds that together UNIQUELY pin the returned value:
+//   Floor: res*d <= x*y  AND  (res+1)*d > x*y   <=>  res == floor(x*y/d)
+//   Ceil : res*d >= x*y  AND  (res>0 => (res-1)*d < x*y)  <=>  res == ceil(x*y/d)
+// All arithmetic below is over CVL `mathint` (uint256 operands auto-promote),
+// so `x*y`, `res*d`, `(res+1)*d` are exact and never overflow. This is the
+// same bounds-based structure used to discharge mulDiv ghost summaries in
+// morpho-org/midnight's `certora/specs/MulDiv.spec`.
+//
+// Safety only, revert-preserving: `Math.mulDiv` is intentionally NOT summarized
+// here (the real implementation is verified), the call uses `@withrevert`, and
+// every bound is asserted ONLY on the non-reverting path (`!lastReverted =>`).
+// We do NOT prove liveness (that it returns whenever the exact result fits).
+// This matches Mathis's "safety, not liveness".
 
 methods {
     function mulDivWrapper(uint256 x, uint256 y, uint256 denominator, Math.Rounding rounding)
@@ -18,27 +30,31 @@ methods {
 // Floor: rounds toward negative infinity == exact mathint floor of (x*y)/d.
 rule mulDivFloorValue(uint256 x, uint256 y, uint256 d) {
     require d != 0;
-    uint256 result = mulDivWrapper@withrevert(x, y, d, Math.Rounding.Floor);
-    assert !lastReverted => result == require_uint256((x * y) / d);
+    uint256 res = mulDivWrapper@withrevert(x, y, d, Math.Rounding.Floor);
+    assert !lastReverted => res * d <= x * y;
+    assert !lastReverted => (res + 1) * d > x * y;
 }
 
 // Trunc: for non-negative operands, truncation toward zero == floor.
 rule mulDivTruncValue(uint256 x, uint256 y, uint256 d) {
     require d != 0;
-    uint256 result = mulDivWrapper@withrevert(x, y, d, Math.Rounding.Trunc);
-    assert !lastReverted => result == require_uint256((x * y) / d);
+    uint256 res = mulDivWrapper@withrevert(x, y, d, Math.Rounding.Trunc);
+    assert !lastReverted => res * d <= x * y;
+    assert !lastReverted => (res + 1) * d > x * y;
 }
 
 // Ceil: rounds toward positive infinity == exact mathint ceil of (x*y)/d.
 rule mulDivCeilValue(uint256 x, uint256 y, uint256 d) {
     require d != 0;
-    uint256 result = mulDivWrapper@withrevert(x, y, d, Math.Rounding.Ceil);
-    assert !lastReverted => result == require_uint256((x * y + (d - 1)) / d);
+    uint256 res = mulDivWrapper@withrevert(x, y, d, Math.Rounding.Ceil);
+    assert !lastReverted => res * d >= x * y;
+    assert !lastReverted => (res > 0 => (res - 1) * d < x * y);
 }
 
 // Expand: for non-negative operands, rounding away from zero == ceil.
 rule mulDivExpandValue(uint256 x, uint256 y, uint256 d) {
     require d != 0;
-    uint256 result = mulDivWrapper@withrevert(x, y, d, Math.Rounding.Expand);
-    assert !lastReverted => result == require_uint256((x * y + (d - 1)) / d);
+    uint256 res = mulDivWrapper@withrevert(x, y, d, Math.Rounding.Expand);
+    assert !lastReverted => res * d >= x * y;
+    assert !lastReverted => (res > 0 => (res - 1) * d < x * y);
 }

From 7ea4f556b9c83b8a3d5749ad21f525f73eb3e037 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Fri, 31 Jul 2026 17:46:14 +0000
Subject: [PATCH 09/10] certora: revert MulDivCorrectness lemma (OZ 512-bit
 mulDiv unmodelable)

The intermediate lemma proving OZ's real Math.mulDiv matches the basic
floor/ceil cvlMulDiv summary does not discharge. The prover returns fast
counterexamples (not timeouts) for every rounding mode, in both an exact
mathint-division form and a tight two-sided multiplicative-bounds form.

Witness (floor, assert (res+1)*d > x*y): x=0xb6db..6dc (~8.27e76), y=7, d=6,
returned res=0 on a non-reverting path -- true floor is ~9.65e76.
Witness (ceil, assert res*d >= x*y): x=2^255+2, y=4, d=3, returned res=1 --
true ceil is ~7.7e76. The returned values are unrelated to floor/ceil(x*y/d):
the prover over-approximates Math.mulDiv's 512-bit mulmod + Newton-Raphson
modular-inverse bytecode and admits arbitrary small results. With mulDiv
un-summarized there is no ghost to constrain, so no lemma fixes this.

Reverting to keep PR green; the Math.mulDiv => cvlMulDiv summary in
ERC4626.spec remains an assumption.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01CfzVWCYX7Nrnu4P6h4EuP9
---
 .github/workflows/certora.yml         |  1 -
 certora/confs/MulDivCorrectness.conf  | 19 ---------
 certora/helpers/MetaMorphoHarness.sol |  8 ----
 certora/specs/MulDivCorrectness.spec  | 60 ---------------------------
 4 files changed, 88 deletions(-)
 delete mode 100644 certora/confs/MulDivCorrectness.conf
 delete mode 100644 certora/specs/MulDivCorrectness.spec

diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
index 140d7b19..85a3993d 100644
--- a/.github/workflows/certora.yml
+++ b/.github/workflows/certora.yml
@@ -24,7 +24,6 @@ jobs:
           - LastUpdated
           - Liveness
           - MarketInteractions
-          - MulDivCorrectness
           - PendingValues
           - Range
           - Reentrancy
diff --git a/certora/confs/MulDivCorrectness.conf b/certora/confs/MulDivCorrectness.conf
deleted file mode 100644
index 3b6a1d5b..00000000
--- a/certora/confs/MulDivCorrectness.conf
+++ /dev/null
@@ -1,19 +0,0 @@
-{
-  "files": [
-    "certora/helpers/MetaMorphoHarness.sol"
-  ],
-  "solc": "solc-0.8.21",
-  "verify": "MetaMorphoHarness:certora/specs/MulDivCorrectness.spec",
-  "loop_iter": "2",
-  "optimistic_loop": true,
-  "prover_args": [
-    "-depth 0",
-    "-timeout 600",
-    "-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 MulDivCorrectness"
-}
diff --git a/certora/helpers/MetaMorphoHarness.sol b/certora/helpers/MetaMorphoHarness.sol
index 3c18742e..c812670a 100644
--- a/certora/helpers/MetaMorphoHarness.sol
+++ b/certora/helpers/MetaMorphoHarness.sol
@@ -37,14 +37,6 @@ contract MetaMorphoHarness is MetaMorpho {
         return pendingCap[id];
     }
 
-    function mulDivWrapper(uint256 x, uint256 y, uint256 denominator, Math.Rounding rounding)
-        external
-        pure
-        returns (uint256)
-    {
-        return Math.mulDiv(x, y, denominator, rounding);
-    }
-
     function minTimelock() external pure returns (uint256) {
         return ConstantsLib.MIN_TIMELOCK;
     }
diff --git a/certora/specs/MulDivCorrectness.spec b/certora/specs/MulDivCorrectness.spec
deleted file mode 100644
index 7f247870..00000000
--- a/certora/specs/MulDivCorrectness.spec
+++ /dev/null
@@ -1,60 +0,0 @@
-// SPDX-License-Identifier: GPL-2.0-or-later
-
-// Intermediate lemma: prove that OpenZeppelin's real 512-bit `Math.mulDiv`
-// rounds exactly like the basic floor/ceil `cvlMulDiv` used as a summary in
-// ERC4626.spec. This discharges the `Math.mulDiv => cvlMulDiv` summary,
-// turning it from an assumption into a proven-faithful abstraction.
-//
-// Strength: instead of a single mathint-division equality
-// (`res == (x*y)/d`), which forces the SMT solver to reason about division of
-// a 512-bit product and tends to time out, we prove the two TIGHT two-sided
-// multiplicative bounds that together UNIQUELY pin the returned value:
-//   Floor: res*d <= x*y  AND  (res+1)*d > x*y   <=>  res == floor(x*y/d)
-//   Ceil : res*d >= x*y  AND  (res>0 => (res-1)*d < x*y)  <=>  res == ceil(x*y/d)
-// All arithmetic below is over CVL `mathint` (uint256 operands auto-promote),
-// so `x*y`, `res*d`, `(res+1)*d` are exact and never overflow. This is the
-// same bounds-based structure used to discharge mulDiv ghost summaries in
-// morpho-org/midnight's `certora/specs/MulDiv.spec`.
-//
-// Safety only, revert-preserving: `Math.mulDiv` is intentionally NOT summarized
-// here (the real implementation is verified), the call uses `@withrevert`, and
-// every bound is asserted ONLY on the non-reverting path (`!lastReverted =>`).
-// We do NOT prove liveness (that it returns whenever the exact result fits).
-// This matches Mathis's "safety, not liveness".
-
-methods {
-    function mulDivWrapper(uint256 x, uint256 y, uint256 denominator, Math.Rounding rounding)
-        external returns (uint256) envfree;
-}
-
-// Floor: rounds toward negative infinity == exact mathint floor of (x*y)/d.
-rule mulDivFloorValue(uint256 x, uint256 y, uint256 d) {
-    require d != 0;
-    uint256 res = mulDivWrapper@withrevert(x, y, d, Math.Rounding.Floor);
-    assert !lastReverted => res * d <= x * y;
-    assert !lastReverted => (res + 1) * d > x * y;
-}
-
-// Trunc: for non-negative operands, truncation toward zero == floor.
-rule mulDivTruncValue(uint256 x, uint256 y, uint256 d) {
-    require d != 0;
-    uint256 res = mulDivWrapper@withrevert(x, y, d, Math.Rounding.Trunc);
-    assert !lastReverted => res * d <= x * y;
-    assert !lastReverted => (res + 1) * d > x * y;
-}
-
-// Ceil: rounds toward positive infinity == exact mathint ceil of (x*y)/d.
-rule mulDivCeilValue(uint256 x, uint256 y, uint256 d) {
-    require d != 0;
-    uint256 res = mulDivWrapper@withrevert(x, y, d, Math.Rounding.Ceil);
-    assert !lastReverted => res * d >= x * y;
-    assert !lastReverted => (res > 0 => (res - 1) * d < x * y);
-}
-
-// Expand: for non-negative operands, rounding away from zero == ceil.
-rule mulDivExpandValue(uint256 x, uint256 y, uint256 d) {
-    require d != 0;
-    uint256 res = mulDivWrapper@withrevert(x, y, d, Math.Rounding.Expand);
-    assert !lastReverted => res * d >= x * y;
-    assert !lastReverted => (res > 0 => (res - 1) * d < x * y);
-}

From 29069204b6bcd894563489f35b6e82e4fac4e969 Mon Sep 17 00:00:00 2001
From: MathisGD <74971347+MathisGD@users.noreply.github.com>
Date: Sat, 1 Aug 2026 14:47:39 +0200
Subject: [PATCH 10/10] Apply suggestion from @MathisGD

Signed-off-by: MathisGD <74971347+MathisGD@users.noreply.github.com>
---
 certora/specs/ERC4626.spec | 1 +
 1 file changed, 1 insertion(+)

diff --git a/certora/specs/ERC4626.spec b/certora/specs/ERC4626.spec
index a61a8170..86a40149 100644
--- a/certora/specs/ERC4626.spec
+++ b/certora/specs/ERC4626.spec
@@ -26,6 +26,7 @@ function summaryDecimalsOffset() returns uint8 {
     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);