feat: can use shares properties

morpho-org · Nov 23, 2023 · 5753c9f · 5753c9f
1 parent 744d0ff
commit 5753c9f
Showing 1 changed file with 36 additions and 0 deletions.
diff --git 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);