From ed6c5ead50b2e3487dfa7124e21f3659c4913bd6 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 1 Dec 2023 17:12:02 +0100 Subject: [PATCH 1/8] fix: renaming myBalances to balance consistently --- certora/specs/Liveness.spec | 40 ++++++++++++++++++------------------- certora/specs/Transfer.spec | 17 ++++++++-------- 2 files changed, 28 insertions(+), 29 deletions(-) diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec index 0c621ac77..17afc6a2a 100644 --- a/certora/specs/Liveness.spec +++ b/certora/specs/Liveness.spec @@ -23,8 +23,8 @@ methods { function SafeTransferLib.safeTransferFrom(address token, address from, address to, uint256 value) internal => summarySafeTransferFrom(token, from, to, value); } -ghost mapping(address => mathint) myBalances { - init_state axiom (forall address token. myBalances[token] == 0); +ghost mapping(address => mathint) balance { + init_state axiom (forall address token. balance[token] == 0); } function summaryId(MorphoInternalAccess.MarketParams marketParams) returns MorphoInternalAccess.Id { @@ -34,11 +34,11 @@ function summaryId(MorphoInternalAccess.MarketParams marketParams) returns Morph function summarySafeTransferFrom(address token, address from, address to, uint256 amount) { if (from == currentContract) { // Safe require because the reference implementation would revert. - myBalances[token] = require_uint256(myBalances[token] - amount); + balance[token] = require_uint256(balance[token] - amount); } if (to == currentContract) { // Safe require because the reference implementation would revert. - myBalances[token] = require_uint256(myBalances[token] + amount); + balance[token] = require_uint256(balance[token] + amount); } } @@ -75,7 +75,7 @@ rule supplyChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marke require lastUpdate(id) == e.block.timestamp; mathint sharesBefore = supplyShares(id, onBehalf); - mathint balanceBefore = myBalances[marketParams.loanToken]; + mathint balanceBefore = balance[marketParams.loanToken]; mathint liquidityBefore = totalSupplyAssets(id) - totalBorrowAssets(id); uint256 suppliedAssets; @@ -83,7 +83,7 @@ rule supplyChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marke suppliedAssets, suppliedShares = supply(e, marketParams, assets, shares, onBehalf, data); mathint sharesAfter = supplyShares(id, onBehalf); - mathint balanceAfter = myBalances[marketParams.loanToken]; + mathint balanceAfter = balance[marketParams.loanToken]; mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id); assert assets != 0 => suppliedAssets == assets; @@ -111,7 +111,7 @@ rule withdrawChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams mar require lastUpdate(id) == e.block.timestamp; mathint sharesBefore = supplyShares(id, onBehalf); - mathint balanceBefore = myBalances[marketParams.loanToken]; + mathint balanceBefore = balance[marketParams.loanToken]; mathint liquidityBefore = totalSupplyAssets(id) - totalBorrowAssets(id); uint256 withdrawnAssets; @@ -119,7 +119,7 @@ rule withdrawChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams mar withdrawnAssets, withdrawnShares = withdraw(e, marketParams, assets, shares, onBehalf, receiver); mathint sharesAfter = supplyShares(id, onBehalf); - mathint balanceAfter = myBalances[marketParams.loanToken]; + mathint balanceAfter = balance[marketParams.loanToken]; mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id); assert assets != 0 => withdrawnAssets == assets; @@ -147,7 +147,7 @@ rule borrowChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marke require lastUpdate(id) == e.block.timestamp; mathint sharesBefore = borrowShares(id, onBehalf); - mathint balanceBefore = myBalances[marketParams.loanToken]; + mathint balanceBefore = balance[marketParams.loanToken]; mathint liquidityBefore = totalSupplyAssets(id) - totalBorrowAssets(id); uint256 borrowedAssets; @@ -155,7 +155,7 @@ rule borrowChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marke borrowedAssets, borrowedShares = borrow(e, marketParams, assets, shares, onBehalf, receiver); mathint sharesAfter = borrowShares(id, onBehalf); - mathint balanceAfter = myBalances[marketParams.loanToken]; + mathint balanceAfter = balance[marketParams.loanToken]; mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id); assert assets != 0 => borrowedAssets == assets; @@ -183,7 +183,7 @@ rule repayChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams market require lastUpdate(id) == e.block.timestamp; mathint sharesBefore = borrowShares(id, onBehalf); - mathint balanceBefore = myBalances[marketParams.loanToken]; + mathint balanceBefore = balance[marketParams.loanToken]; mathint liquidityBefore = totalSupplyAssets(id) - totalBorrowAssets(id); mathint borrowAssetsBefore = totalBorrowAssets(id); @@ -193,7 +193,7 @@ rule repayChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams market repaidAssets, repaidShares = repay(e, marketParams, assets, shares, onBehalf, data); mathint sharesAfter = borrowShares(id, onBehalf); - mathint balanceAfter = myBalances[marketParams.loanToken]; + mathint balanceAfter = balance[marketParams.loanToken]; mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id); assert assets != 0 => repaidAssets == assets; @@ -220,12 +220,12 @@ rule supplyCollateralChangesTokensAndBalance(env e, MorphoInternalAccess.MarketP require currentContract != e.msg.sender; mathint collateralBefore = collateral(id, onBehalf); - mathint balanceBefore = myBalances[marketParams.collateralToken]; + mathint balanceBefore = balance[marketParams.collateralToken]; supplyCollateral(e, marketParams, assets, onBehalf, data); mathint collateralAfter = collateral(id, onBehalf); - mathint balanceAfter = myBalances[marketParams.collateralToken]; + mathint balanceAfter = balance[marketParams.collateralToken]; assert collateralAfter == collateralBefore + assets; assert balanceAfter == balanceBefore + assets; @@ -241,12 +241,12 @@ rule withdrawCollateralChangesTokensAndBalance(env e, MorphoInternalAccess.Marke require lastUpdate(id) == e.block.timestamp; mathint collateralBefore = collateral(id, onBehalf); - mathint balanceBefore = myBalances[marketParams.collateralToken]; + mathint balanceBefore = balance[marketParams.collateralToken]; withdrawCollateral(e, marketParams, assets, onBehalf, receiver); mathint collateralAfter = collateral(id, onBehalf); - mathint balanceAfter = myBalances[marketParams.collateralToken]; + mathint balanceAfter = balance[marketParams.collateralToken]; assert collateralAfter == collateralBefore - assets; assert balanceAfter == balanceBefore - assets; @@ -264,8 +264,8 @@ rule liquidateChangesTokens(env e, MorphoInternalAccess.MarketParams marketParam require lastUpdate(id) == e.block.timestamp; mathint collateralBefore = collateral(id, borrower); - mathint balanceLoanBefore = myBalances[marketParams.loanToken]; - mathint balanceCollateralBefore = myBalances[marketParams.collateralToken]; + mathint balanceLoanBefore = balance[marketParams.loanToken]; + mathint balanceCollateralBefore = balance[marketParams.collateralToken]; mathint liquidityBefore = totalSupplyAssets(id) - totalBorrowAssets(id); mathint borrowLoanAssetsBefore = totalBorrowAssets(id); @@ -275,8 +275,8 @@ rule liquidateChangesTokens(env e, MorphoInternalAccess.MarketParams marketParam seizedAssets, repaidAssets = liquidate(e, marketParams, borrower, seized, repaidShares, data); mathint collateralAfter = collateral(id, borrower); - mathint balanceLoanAfter = myBalances[marketParams.loanToken]; - mathint balanceCollateralAfter = myBalances[marketParams.collateralToken]; + mathint balanceLoanAfter = balance[marketParams.loanToken]; + mathint balanceCollateralAfter = balance[marketParams.collateralToken]; mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id); assert seized != 0 => seizedAssets == seized; diff --git a/certora/specs/Transfer.spec b/certora/specs/Transfer.spec index a560f0658..f06903902 100644 --- a/certora/specs/Transfer.spec +++ b/certora/specs/Transfer.spec @@ -13,19 +13,18 @@ methods { function _.totalSupply() external => DISPATCHER(true); } -ghost mapping(address => mathint) myBalances -{ - init_state axiom (forall address token. myBalances[token] == 0); +ghost mapping(address => mathint) balance { + init_state axiom (forall address token. balance[token] == 0); } function summarySafeTransferFrom(address token, address from, address to, uint256 amount) { if (from == currentContract) { // Safe require because the reference implementation would revert. - myBalances[token] = require_uint256(myBalances[token] - amount); + balance[token] = require_uint256(balance[token] - amount); } if (to == currentContract) { // Safe require because the reference implementation would revert. - myBalances[token] = require_uint256(myBalances[token] + amount); + balance[token] = require_uint256(balance[token] + amount); } } @@ -38,9 +37,9 @@ rule checkTransferSummary(address token, address to, uint256 amount) { libSafeTransfer(token, to, amount); mathint finalBalance = balanceOf(token, currentContract); - require myBalances[token] == initialBalance; + require balance[token] == initialBalance; summarySafeTransferFrom(token, currentContract, to, amount); - assert myBalances[token] == finalBalance; + assert balance[token] == finalBalance; } // Check the functional correctness of the summary of safeTransferFrom. @@ -52,9 +51,9 @@ rule checkTransferFromSummary(address token, address from, uint256 amount) { libSafeTransferFrom(token, from, currentContract, amount); mathint finalBalance = balanceOf(token, currentContract); - require myBalances[token] == initialBalance; + require balance[token] == initialBalance; summarySafeTransferFrom(token, from, currentContract, amount); - assert myBalances[token] == finalBalance; + assert balance[token] == finalBalance; } // Check the revert condition of the summary of safeTransfer. From f07f08ccd9662cac1b36beb0cbf3bcac4193565a Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 1 Dec 2023 17:12:19 +0100 Subject: [PATCH 2/8] feat: add supplyLiquidity --- certora/specs/ExitLiquidity.spec | 35 ++++++++++++++++++++++++-------- 1 file changed, 26 insertions(+), 9 deletions(-) diff --git a/certora/specs/ExitLiquidity.spec b/certora/specs/ExitLiquidity.spec index 73c5af58c..dae8c8c65 100644 --- a/certora/specs/ExitLiquidity.spec +++ b/certora/specs/ExitLiquidity.spec @@ -16,9 +16,28 @@ methods { function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; } -// Check that it's not possible to withdraw more assets than what the user owns. -rule withdrawLiquidity(MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { - env e; +// Check that the assets supplied are greater than the assets owned in the end. +rule supplyLiquidity(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { + MorphoHarness.Id id = libId(marketParams); + + // Assume no interest as it would increase the total supply assets. + require lastUpdate(id) == e.block.timestamp; + // Assume no supply position to begin with. + require supplyShares(id, onBehalf) == 0; + + uint256 suppliedAssets; + suppliedAssets, _ = supply(e, marketParams, assets, shares, onBehalf, data); + + uint256 finalShares = supplyShares(id, onBehalf); + uint256 finalTotalSupply = virtualTotalSupplyAssets(id); + uint256 finalTotalSupplyShares = virtualTotalSupplyShares(id); + uint256 ownedAssets = libMulDivDown(finalShares, finalTotalSupply, finalTotalSupplyShares); + + assert suppliedAssets >= ownedAssets; +} + +// Check that the assets withdrawn are less than the assets owned initially. +rule withdrawLiquidity(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { MorphoHarness.Id id = libId(marketParams); // Assume no interest as it would increase the total supply assets. @@ -35,9 +54,8 @@ rule withdrawLiquidity(MorphoHarness.MarketParams marketParams, uint256 assets, assert withdrawnAssets <= ownedAssets; } -// Check that it's not possible to withdraw more collateral than what the user owns. -rule withdrawCollateralLiquidity(MorphoHarness.MarketParams marketParams, uint256 withdrawnAssets, address onBehalf, address receiver) { - env e; +// Check that the collateral assets withdrawn are less than the assets owned initially. +rule withdrawCollateralLiquidity(env e, MorphoHarness.MarketParams marketParams, uint256 withdrawnAssets, address onBehalf, address receiver) { MorphoHarness.Id id = libId(marketParams); uint256 ownedAssets = collateral(id, onBehalf); @@ -47,9 +65,8 @@ rule withdrawCollateralLiquidity(MorphoHarness.MarketParams marketParams, uint25 assert withdrawnAssets <= ownedAssets; } -// Check than when repaying the full outstanding debt requires more assets than what the user owes. -rule repayLiquidity(MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { - env e; +// Check that the assets repaid are greater than the assets owed initially. +rule repayLiquidity(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { MorphoHarness.Id id = libId(marketParams); // Assume no interest as it would increase the total borrowed assets. From 7c8b3262f8ca4f0a69aec3cb4989e0ad638f1010 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 1 Dec 2023 17:46:25 +0100 Subject: [PATCH 3/8] feat: add supplyCollateral and borrow assets accounting --- certora/specs/ExitLiquidity.spec | 70 ++++++++++++++++++++++++-------- 1 file changed, 54 insertions(+), 16 deletions(-) diff --git a/certora/specs/ExitLiquidity.spec b/certora/specs/ExitLiquidity.spec index dae8c8c65..3e5bd6782 100644 --- a/certora/specs/ExitLiquidity.spec +++ b/certora/specs/ExitLiquidity.spec @@ -16,8 +16,24 @@ methods { function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; } +function ownedSupplyAssets(MorphoHarness.Id id, address user) returns uint256 { + uint256 userShares = supplyShares(id, user); + uint256 totalSupplyAssets = virtualTotalSupplyAssets(id); + uint256 totalSupplyShares = virtualTotalSupplyShares(id); + + return libMulDivDown(userShares, totalSupplyAssets, totalSupplyShares); +} + +function owedBorrowAssets(MorphoHarness.Id id, address user) returns uint256 { + uint256 userShares = borrowShares(id, user); + uint256 totalBorrowAssets = virtualTotalBorrowAssets(id); + uint256 totalBorrowShares = virtualTotalBorrowShares(id); + + return libMulDivUp(userShares, totalBorrowAssets, totalBorrowShares); +} + // Check that the assets supplied are greater than the assets owned in the end. -rule supplyLiquidity(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { +rule supplyAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { MorphoHarness.Id id = libId(marketParams); // Assume no interest as it would increase the total supply assets. @@ -28,25 +44,19 @@ rule supplyLiquidity(env e, MorphoHarness.MarketParams marketParams, uint256 ass uint256 suppliedAssets; suppliedAssets, _ = supply(e, marketParams, assets, shares, onBehalf, data); - uint256 finalShares = supplyShares(id, onBehalf); - uint256 finalTotalSupply = virtualTotalSupplyAssets(id); - uint256 finalTotalSupplyShares = virtualTotalSupplyShares(id); - uint256 ownedAssets = libMulDivDown(finalShares, finalTotalSupply, finalTotalSupplyShares); + uint256 ownedAssets = ownedSupplyAssets(id, onBehalf); assert suppliedAssets >= ownedAssets; } // Check that the assets withdrawn are less than the assets owned initially. -rule withdrawLiquidity(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { +rule withdrawAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { MorphoHarness.Id id = libId(marketParams); // Assume no interest as it would increase the total supply assets. require lastUpdate(id) == e.block.timestamp; - uint256 initialShares = supplyShares(id, onBehalf); - uint256 initialTotalSupply = virtualTotalSupplyAssets(id); - uint256 initialTotalSupplyShares = virtualTotalSupplyShares(id); - uint256 ownedAssets = libMulDivDown(initialShares, initialTotalSupply, initialTotalSupplyShares); + uint256 ownedAssets = ownedSupplyAssets(id, onBehalf); uint256 withdrawnAssets; withdrawnAssets, _ = withdraw(e, marketParams, assets, shares, onBehalf, receiver); @@ -54,8 +64,22 @@ rule withdrawLiquidity(env e, MorphoHarness.MarketParams marketParams, uint256 a assert withdrawnAssets <= ownedAssets; } +// Check that the collateral assets supplied are greater than the assets owned in the end. +rule supplyCollateralAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 suppliedAssets, address onBehalf, bytes data) { + MorphoHarness.Id id = libId(marketParams); + + // Assume no collateral to begin with. + require collateral(id, onBehalf) == 0; + + supplyCollateral(e, marketParams, suppliedAssets, onBehalf, data); + + uint256 ownedAssets = collateral(id, onBehalf); + + assert suppliedAssets >= ownedAssets; +} + // Check that the collateral assets withdrawn are less than the assets owned initially. -rule withdrawCollateralLiquidity(env e, MorphoHarness.MarketParams marketParams, uint256 withdrawnAssets, address onBehalf, address receiver) { +rule withdrawCollateralAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 withdrawnAssets, address onBehalf, address receiver) { MorphoHarness.Id id = libId(marketParams); uint256 ownedAssets = collateral(id, onBehalf); @@ -65,17 +89,31 @@ rule withdrawCollateralLiquidity(env e, MorphoHarness.MarketParams marketParams, assert withdrawnAssets <= ownedAssets; } +// Check that the assets borrowed are less than the assets owed in the end. +rule borrowAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { + MorphoHarness.Id id = libId(marketParams); + + // Assume no interest as it would increase the total borrowed assets. + require lastUpdate(id) == e.block.timestamp; + // Assume no outstanding debt to begin with. + require borrowShares(id, onBehalf) == 0; + + uint256 borrowedAssets; + borrowedAssets, _ = borrow(e, marketParams, assets, shares, onBehalf, receiver); + + uint256 owedAssets = owedBorrowAssets(id, onBehalf); + + assert borrowedAssets <= owedAssets; +} + // Check that the assets repaid are greater than the assets owed initially. -rule repayLiquidity(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { +rule repayAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { MorphoHarness.Id id = libId(marketParams); // Assume no interest as it would increase the total borrowed assets. require lastUpdate(id) == e.block.timestamp; - uint256 initialShares = borrowShares(id, onBehalf); - uint256 initialTotalBorrow = virtualTotalBorrowAssets(id); - uint256 initialTotalBorrowShares = virtualTotalBorrowShares(id); - uint256 owedAssets = libMulDivUp(initialShares, initialTotalBorrow, initialTotalBorrowShares); + uint256 owedAssets = owedBorrowAssets(id, onBehalf); uint256 repaidAssets; repaidAssets, _ = repay(e, marketParams, assets, shares, onBehalf, data); From 1df99e329ac3b0b9bd46c2f4794e52dc093bef25 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 1 Dec 2023 18:03:10 +0100 Subject: [PATCH 4/8] refactor: rename ExitLiquidity into AssetsAccounting --- .github/workflows/certora.yml | 2 +- certora/README.md | 3 ++- certora/confs/AssetsAccounting.conf | 8 ++++++++ certora/confs/ExitLiquidity.conf | 8 -------- .../specs/{ExitLiquidity.spec => AssetsAccounting.spec} | 0 5 files changed, 11 insertions(+), 10 deletions(-) create mode 100644 certora/confs/AssetsAccounting.conf delete mode 100644 certora/confs/ExitLiquidity.conf rename certora/specs/{ExitLiquidity.spec => AssetsAccounting.spec} (100%) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 402149e56..e4bcbbacf 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -17,9 +17,9 @@ jobs: matrix: conf: - AccrueInterest + - AssetsAccounting - ConsistentState - ExactMath - - ExitLiquidity - Health - LibSummary - Liveness diff --git a/certora/README.md b/certora/README.md index 29f44afbb..d2dbdbcc7 100644 --- a/certora/README.md +++ b/certora/README.md @@ -243,11 +243,12 @@ The [`certora/specs`](specs) folder contains the following files: - [`AccrueInterest.spec`](specs/AccrueInterest.spec) checks that the main functions accrue interest at the start of the interaction. This is done by ensuring that accruing interest before calling the function does not change the outcome compared to just calling the function. View functions do not necessarily respect this property (for example, `totalSupplyShares`), and are filtered out. +- [`AssetsAccounting.spec`](specs/AssetsAccounting.spec) checks that when exiting a position the user cannot get more than what was owed. + Similarly, when entering a position, the assets owned as a result are no greater than what was given. - [`ConsistentState.spec`](specs/ConsistentState.spec) checks that the state (storage) of the Morpho contract is consistent. This includes checking that the accounting of the total amount and shares is correct, that markets are independent from each other, that only enabled IRMs and LLTVs can be used, and that users cannot have their position made worse by an unauthorized account. - [`ExactMath.spec`](specs/ExactMath.spec) checks precise properties when taking into account exact multiplication and division. Notably, this file specifies that using supply and withdraw in the same block cannot yield more funds than at the start. -- [`ExitLiquidity.spec`](specs/ExitLiquidity.spec) checks that when exiting a position with withdraw, withdrawCollateral, or repay, the user cannot get more than what was owed. - [`Health.spec`](specs/Health.spec) checks properties about the health of the positions. Notably, functions cannot render an account unhealthy, and debt positions always have some collateral (thanks to the bad debt realization mechanism). - [`LibSummary.spec`](specs/LibSummary.spec) checks the summarization of the library functions that are used in other specification files. diff --git a/certora/confs/AssetsAccounting.conf b/certora/confs/AssetsAccounting.conf new file mode 100644 index 000000000..8bdc141ec --- /dev/null +++ b/certora/confs/AssetsAccounting.conf @@ -0,0 +1,8 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol" + ], + "verify": "MorphoHarness:certora/specs/AssetsAccounting.spec", + "rule_sanity": "basic", + "msg": "Morpho Blue Assets Accounting" +} diff --git a/certora/confs/ExitLiquidity.conf b/certora/confs/ExitLiquidity.conf deleted file mode 100644 index 336359251..000000000 --- a/certora/confs/ExitLiquidity.conf +++ /dev/null @@ -1,8 +0,0 @@ -{ - "files": [ - "certora/harness/MorphoHarness.sol" - ], - "verify": "MorphoHarness:certora/specs/ExitLiquidity.spec", - "rule_sanity": "basic", - "msg": "Morpho Blue Exit Liquidity" -} diff --git a/certora/specs/ExitLiquidity.spec b/certora/specs/AssetsAccounting.spec similarity index 100% rename from certora/specs/ExitLiquidity.spec rename to certora/specs/AssetsAccounting.spec From e3aca4977294a924d0113841d0bfb07ba3644f0b Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 4 Dec 2023 11:15:00 +0100 Subject: [PATCH 5/8] refactor: reorder assets accounting rules --- certora/specs/AssetsAccounting.spec | 50 ++++++++++++++--------------- 1 file changed, 25 insertions(+), 25 deletions(-) diff --git a/certora/specs/AssetsAccounting.spec b/certora/specs/AssetsAccounting.spec index 3e5bd6782..5fec5ffab 100644 --- a/certora/specs/AssetsAccounting.spec +++ b/certora/specs/AssetsAccounting.spec @@ -64,31 +64,6 @@ rule withdrawAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, ui assert withdrawnAssets <= ownedAssets; } -// Check that the collateral assets supplied are greater than the assets owned in the end. -rule supplyCollateralAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 suppliedAssets, address onBehalf, bytes data) { - MorphoHarness.Id id = libId(marketParams); - - // Assume no collateral to begin with. - require collateral(id, onBehalf) == 0; - - supplyCollateral(e, marketParams, suppliedAssets, onBehalf, data); - - uint256 ownedAssets = collateral(id, onBehalf); - - assert suppliedAssets >= ownedAssets; -} - -// Check that the collateral assets withdrawn are less than the assets owned initially. -rule withdrawCollateralAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 withdrawnAssets, address onBehalf, address receiver) { - MorphoHarness.Id id = libId(marketParams); - - uint256 ownedAssets = collateral(id, onBehalf); - - withdrawCollateral(e, marketParams, withdrawnAssets, onBehalf, receiver); - - assert withdrawnAssets <= ownedAssets; -} - // Check that the assets borrowed are less than the assets owed in the end. rule borrowAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { MorphoHarness.Id id = libId(marketParams); @@ -123,3 +98,28 @@ rule repayAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint2 assert repaidAssets >= owedAssets; } + +// Check that the collateral assets supplied are greater than the assets owned in the end. +rule supplyCollateralAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 suppliedAssets, address onBehalf, bytes data) { + MorphoHarness.Id id = libId(marketParams); + + // Assume no collateral to begin with. + require collateral(id, onBehalf) == 0; + + supplyCollateral(e, marketParams, suppliedAssets, onBehalf, data); + + uint256 ownedAssets = collateral(id, onBehalf); + + assert suppliedAssets >= ownedAssets; +} + +// Check that the collateral assets withdrawn are less than the assets owned initially. +rule withdrawCollateralAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 withdrawnAssets, address onBehalf, address receiver) { + MorphoHarness.Id id = libId(marketParams); + + uint256 ownedAssets = collateral(id, onBehalf); + + withdrawCollateral(e, marketParams, withdrawnAssets, onBehalf, receiver); + + assert withdrawnAssets <= ownedAssets; +} From 343b36d6728409da92df0ba7cbbca77bb61ccc9e Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 4 Dec 2023 18:06:24 +0100 Subject: [PATCH 6/8] refactor: borrow assets accounting restricted to shares --- certora/specs/AssetsAccounting.spec | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/certora/specs/AssetsAccounting.spec b/certora/specs/AssetsAccounting.spec index 5fec5ffab..12adea876 100644 --- a/certora/specs/AssetsAccounting.spec +++ b/certora/specs/AssetsAccounting.spec @@ -65,7 +65,7 @@ rule withdrawAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, ui } // Check that the assets borrowed are less than the assets owed in the end. -rule borrowAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { +rule borrowAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 shares, address onBehalf, address receiver) { MorphoHarness.Id id = libId(marketParams); // Assume no interest as it would increase the total borrowed assets. @@ -73,8 +73,9 @@ rule borrowAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint // Assume no outstanding debt to begin with. require borrowShares(id, onBehalf) == 0; + // The borrow call is restricted to shares as input to make it easier on the prover. uint256 borrowedAssets; - borrowedAssets, _ = borrow(e, marketParams, assets, shares, onBehalf, receiver); + borrowedAssets, _ = borrow(e, marketParams, 0, shares, onBehalf, receiver); uint256 owedAssets = owedBorrowAssets(id, onBehalf); From 3516804676443904f6eb9cd6c86c6eeac8f257d2 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 5 Dec 2023 13:58:38 +0100 Subject: [PATCH 7/8] refactor: improve supply collateral assets accounting rule --- certora/specs/AssetsAccounting.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/specs/AssetsAccounting.spec b/certora/specs/AssetsAccounting.spec index 12adea876..0a807ba71 100644 --- a/certora/specs/AssetsAccounting.spec +++ b/certora/specs/AssetsAccounting.spec @@ -111,7 +111,7 @@ rule supplyCollateralAssetsAccounting(env e, MorphoHarness.MarketParams marketPa uint256 ownedAssets = collateral(id, onBehalf); - assert suppliedAssets >= ownedAssets; + assert suppliedAssets == ownedAssets; } // Check that the collateral assets withdrawn are less than the assets owned initially. From f42fdb341c9b66cfd5eb3c7997e7329ba3617f15 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 5 Dec 2023 13:58:52 +0100 Subject: [PATCH 8/8] refactor: rename owned/owed assets functions --- certora/specs/AssetsAccounting.spec | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/certora/specs/AssetsAccounting.spec b/certora/specs/AssetsAccounting.spec index 0a807ba71..007500b6d 100644 --- a/certora/specs/AssetsAccounting.spec +++ b/certora/specs/AssetsAccounting.spec @@ -16,7 +16,7 @@ methods { function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; } -function ownedSupplyAssets(MorphoHarness.Id id, address user) returns uint256 { +function expectedSupplyAssets(MorphoHarness.Id id, address user) returns uint256 { uint256 userShares = supplyShares(id, user); uint256 totalSupplyAssets = virtualTotalSupplyAssets(id); uint256 totalSupplyShares = virtualTotalSupplyShares(id); @@ -24,7 +24,7 @@ function ownedSupplyAssets(MorphoHarness.Id id, address user) returns uint256 { return libMulDivDown(userShares, totalSupplyAssets, totalSupplyShares); } -function owedBorrowAssets(MorphoHarness.Id id, address user) returns uint256 { +function expectedBorrowAssets(MorphoHarness.Id id, address user) returns uint256 { uint256 userShares = borrowShares(id, user); uint256 totalBorrowAssets = virtualTotalBorrowAssets(id); uint256 totalBorrowShares = virtualTotalBorrowShares(id); @@ -44,7 +44,7 @@ rule supplyAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint uint256 suppliedAssets; suppliedAssets, _ = supply(e, marketParams, assets, shares, onBehalf, data); - uint256 ownedAssets = ownedSupplyAssets(id, onBehalf); + uint256 ownedAssets = expectedSupplyAssets(id, onBehalf); assert suppliedAssets >= ownedAssets; } @@ -56,7 +56,7 @@ rule withdrawAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, ui // Assume no interest as it would increase the total supply assets. require lastUpdate(id) == e.block.timestamp; - uint256 ownedAssets = ownedSupplyAssets(id, onBehalf); + uint256 ownedAssets = expectedSupplyAssets(id, onBehalf); uint256 withdrawnAssets; withdrawnAssets, _ = withdraw(e, marketParams, assets, shares, onBehalf, receiver); @@ -77,7 +77,7 @@ rule borrowAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint uint256 borrowedAssets; borrowedAssets, _ = borrow(e, marketParams, 0, shares, onBehalf, receiver); - uint256 owedAssets = owedBorrowAssets(id, onBehalf); + uint256 owedAssets = expectedBorrowAssets(id, onBehalf); assert borrowedAssets <= owedAssets; } @@ -89,7 +89,7 @@ rule repayAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint2 // Assume no interest as it would increase the total borrowed assets. require lastUpdate(id) == e.block.timestamp; - uint256 owedAssets = owedBorrowAssets(id, onBehalf); + uint256 owedAssets = expectedBorrowAssets(id, onBehalf); uint256 repaidAssets; repaidAssets, _ = repay(e, marketParams, assets, shares, onBehalf, data);