From 744d0ffe2cb587e0802195f77bfdd6417d355830 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 22 Nov 2023 19:35:49 +0100 Subject: [PATCH 1/3] test: mutant 3 --- src/Morpho.sol | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Morpho.sol b/src/Morpho.sol index f755904b6..4491e7c86 100644 --- a/src/Morpho.sol +++ b/src/Morpho.sol @@ -246,7 +246,10 @@ contract Morpho is IMorphoStaticTyping { _accrueInterest(marketParams, id); if (assets > 0) shares = assets.toSharesUp(market[id].totalBorrowAssets, market[id].totalBorrowShares); - else assets = shares.toAssetsDown(market[id].totalBorrowAssets, market[id].totalBorrowShares); + /// DeleteExpressionMutation(`assets = shares.toAssetsDown(market[id].totalBorrowAssets, + /// market[id].totalBorrowShares)` |==> `assert(true)`) of: `else assets = + /// shares.toAssetsDown(market[id].totalBorrowAssets, market[id].totalBorrowShares);` + else assert(true); position[id][onBehalf].borrowShares += shares.toUint128(); market[id].totalBorrowShares += shares.toUint128(); From 5753c9f777defab6ef725d90644503befc57924e Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 23 Nov 2023 16:05:08 +0100 Subject: [PATCH 2/3] feat: can use shares properties --- certora/specs/Liveness.spec | 36 ++++++++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec index e5b96af82..ed16cc96b 100644 --- a/certora/specs/Liveness.spec +++ b/certora/specs/Liveness.spec @@ -85,6 +85,15 @@ rule supplyChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marke assert balanceAfter == balanceBefore + suppliedAssets; } +// Check that you can supply non-zero tokens by passing shares. +rule canSupplyByPassingShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, address onBehalf, bytes data) { + uint256 suppliedAssets; + uint256 suppliedShares; + suppliedAssets, suppliedShares = supply(e, marketParams, 0, shares, onBehalf, data); + + satisfy suppliedAssets != 0; +} + // Check that tokens and shares are properly accounted following a withdraw. rule withdrawChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { MorphoInternalAccess.Id id = libId(marketParams); @@ -110,6 +119,15 @@ rule withdrawChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams mar assert balanceAfter == balanceBefore - withdrawnAssets; } +// Check that you can withdraw non-zero tokens by passing shares. +rule canWithdrawByPassingShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, address onBehalf, address receiver) { + uint256 withdrawnAssets; + uint256 withdrawnShares; + withdrawnAssets, withdrawnShares = withdraw(e, marketParams, 0, shares, onBehalf, receiver); + + satisfy withdrawnAssets != 0; +} + // Check that tokens and shares are properly accounted following a borrow. rule borrowChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { MorphoInternalAccess.Id id = libId(marketParams); @@ -135,6 +153,15 @@ rule borrowChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marke assert balanceAfter == balanceBefore - borrowedAssets; } +// Check that you can borrow non-zero tokens by passing shares. +rule canBorrowByPassingShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, address onBehalf, address receiver) { + uint256 borrowedAssets; + uint256 borrowedShares; + borrowedAssets, borrowedShares = borrow(e, marketParams, 0, shares, onBehalf, receiver); + + satisfy borrowedAssets != 0; +} + // Check that tokens and shares are properly accounted following a repay. rule repayChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { MorphoInternalAccess.Id id = libId(marketParams); @@ -160,6 +187,15 @@ rule repayChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams market assert balanceAfter == balanceBefore + repaidAssets; } +// Check that you can repay non-zero tokens by passing shares. +rule canRepayByPassingShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, address onBehalf, bytes data) { + uint256 repaidAssets; + uint256 repaidShares; + repaidAssets, repaidShares = repay(e, marketParams, 0, shares, onBehalf, data); + + satisfy repaidAssets != 0; +} + // Check that tokens and balances are properly accounted following a supplyCollateral. rule supplyCollateralChangesTokensAndBalance(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, address onBehalf, bytes data) { MorphoInternalAccess.Id id = libId(marketParams); From 87d55a603e85bfebae47adabf1157340de8ac631 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 24 Nov 2023 09:12:24 +0100 Subject: [PATCH 3/3] Revert "test: mutant 3" This reverts commit 744d0ffe2cb587e0802195f77bfdd6417d355830. --- src/Morpho.sol | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/Morpho.sol b/src/Morpho.sol index 4491e7c86..f755904b6 100644 --- a/src/Morpho.sol +++ b/src/Morpho.sol @@ -246,10 +246,7 @@ contract Morpho is IMorphoStaticTyping { _accrueInterest(marketParams, id); if (assets > 0) shares = assets.toSharesUp(market[id].totalBorrowAssets, market[id].totalBorrowShares); - /// DeleteExpressionMutation(`assets = shares.toAssetsDown(market[id].totalBorrowAssets, - /// market[id].totalBorrowShares)` |==> `assert(true)`) of: `else assets = - /// shares.toAssetsDown(market[id].totalBorrowAssets, market[id].totalBorrowShares);` - else assert(true); + else assets = shares.toAssetsDown(market[id].totalBorrowAssets, market[id].totalBorrowShares); position[id][onBehalf].borrowShares += shares.toUint128(); market[id].totalBorrowShares += shares.toUint128();