fix: use getters for the morpho-blue project

morpho-org · Oct 28, 2024 · 8c4110a · 8c4110a
1 parent 66e34b8
commit 8c4110a
Show file tree

Hide file tree

Showing 7 changed files with 48 additions and 91 deletions.
diff --git a/certora/confs/ConsistentInstantiation.conf b/certora/confs/ConsistentInstantiation.conf
@@ -1,21 +1,21 @@
 {
   "files": [
-    "certora/helpers/PreLiquidationHarness.sol",
-    "certora/helpers/Util.sol",
-    "lib/morpho-blue/src/Morpho.sol",
+    "src/PreLiquidation.sol",
+    "lib/morpho-blue/certora/harness/MorphoHarness.sol",
+    "lib/morpho-blue/certora/harness/Util.sol",
   ],
   "link": [
-    "PreLiquidationHarness:MORPHO=Morpho",
+    "PreLiquidation:MORPHO=MorphoHarness",
   ],
-  "parametric_contracts" : ["PreLiquidationHarness"],
+  "parametric_contracts" : ["PreLiquidation"],
   "solc_optimize" : "99999",
   "solc_via_ir" : true,
   "solc_map": {
-    "Morpho": "solc-0.8.19",
-    "PreLiquidationHarness": "solc-0.8.27",
-    "Util": "solc-0.8.27",
+    "MorphoHarness": "solc-0.8.19",
+    "Util": "solc-0.8.19",
+    "PreLiquidation": "solc-0.8.27",
   },
-  "verify": "PreLiquidationHarness:certora/specs/ConsistentInstantiation.spec",
+  "verify": "PreLiquidation:certora/specs/ConsistentInstantiation.spec",
   "prover_args": [
     "-depth 5",
     "-mediumTimeout 5",
@@ -25,5 +25,5 @@
   ],
   "rule_sanity": "basic",
   "server": "production",
-  "msg": "PreLiquidationHarness ConsistentInstantiation",
+  "msg": "PreLiquidation ConsistentInstantiation",
 }
diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf
@@ -1,21 +1,21 @@
 {
   "files": [
-    "certora/helpers/PreLiquidationHarness.sol",
-    "certora/helpers/Util.sol",
-    "lib/morpho-blue/src/Morpho.sol",
+    "src/PreLiquidation.sol",
+    "lib/morpho-blue/certora/harness/MorphoHarness.sol",
+    "lib/morpho-blue/certora/harness/Util.sol",
   ],
   "link": [
-    "PreLiquidationHarness:MORPHO=Morpho",
+    "PreLiquidation:MORPHO=MorphoHarness",
   ],
-  "parametric_contracts" : ["PreLiquidationHarness"],
+  "parametric_contracts" : ["PreLiquidation"],
   "solc_optimize" : "99999",
   "solc_via_ir" : true,
   "solc_map": {
-    "Morpho": "solc-0.8.19",
-    "PreLiquidationHarness": "solc-0.8.27",
-    "Util": "solc-0.8.27",
+    "PreLiquidation": "solc-0.8.27",
+    "MorphoHarness": "solc-0.8.19",
+    "Util": "solc-0.8.19",
   },
-  "verify": "PreLiquidationHarness:certora/specs/Reverts.spec",
+  "verify": "PreLiquidation:certora/specs/Reverts.spec",
   "prover_args": [
     "-depth 5",
     "-mediumTimeout 40",

diff --git a/certora/helpers/PreLiquidationHarness.sol b/certora/helpers/PreLiquidationHarness.sol
diff --git a/certora/helpers/Util.sol b/certora/helpers/Util.sol
diff --git a/certora/specs/ConsistentInstantiation.spec b/certora/specs/ConsistentInstantiation.spec
@@ -2,13 +2,11 @@
 
 import "SummaryLib.spec";
 
-using Util as Util;
-
 methods {
-    function _.market(PreLiquidationHarness.Id) external => DISPATCHER(true);
+    function _.market(PreLiquidation.Id) external => DISPATCHER(true);
 
-    function Util.libId(PreLiquidationHarness.MarketParams) external
-        returns PreLiquidationHarness.Id envfree;
+    function Util.libId(PreLiquidation.MarketParams) external
+        returns PreLiquidation.Id envfree;
 }
 
 //Ensure constructor requirements.

diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
@@ -4,8 +4,11 @@ import "ConsistentInstantiation.spec";
 
 methods {
     function _.price() external => mockPrice() expect uint256;
-    function market_(PreLiquidationHarness.Id) external
-        returns (PreLiquidationHarness.Market memory) envfree;
+
+    function MORPHO.market_(PreLiquidation.Id) external
+        returns (PreLiquidation.Market memory) envfree;
+    function MORPHO.position_(PreLiquidation.Id, address) external
+        returns (PreLiquidation.Position memory) envfree;
 
     function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal
         returns uint256 => summaryMulDivDown(a,b,c);
@@ -54,9 +57,8 @@ rule nonLiquidatablePositionReverts(env e, address borrower, uint256 seizedAsset
     requireInvariant preLltvConsistent();
     requireInvariant preLCFConsistent();
     requireInvariant preLIFConsistent();
-    requireInvariant hashOfMarketParamsOf();
 
-    PreLiquidationHarness.Market m = market_(currentContract.ID);
+    PreLiquidation.Market m = MORPHO.market_(currentContract.ID);
 
     // Ensure that no interest is accumulated.
     require m.lastUpdate == e.block.timestamp;
@@ -77,7 +79,7 @@ rule liquidatablePositionReverts(env e, address borrower, uint256 seizedAssets,
     requireInvariant preLCFConsistent();
     requireInvariant preLIFConsistent();
 
-    PreLiquidationHarness.Market m = market_(currentContract.ID);
+    PreLiquidation.Market m = MORPHO.market_(currentContract.ID);
 
     // Ensure that no interest is accumulated.
     require m.lastUpdate == e.block.timestamp;
@@ -94,19 +96,16 @@ rule liquidatablePositionReverts(env e, address borrower, uint256 seizedAssets,
 
 // Check that a pre-liquidation that repays more shares than available or allowed by the preLCF reverts.
 rule excessivePreliquidationWithAssetsReverts(env e, address borrower, uint256 seizedAssets, bytes data) {
-    // Position values.
-    uint256 pBorrowShares;
-
     requireInvariant preLltvConsistent();
     requireInvariant preLCFConsistent();
     requireInvariant preLIFConsistent();
 
-    PreLiquidationHarness.Market m = market_(currentContract.ID);
+    PreLiquidation.Market m = MORPHO.market_(currentContract.ID);
 
     // Ensure that no interest is accumulated.
     require m.lastUpdate == e.block.timestamp;
 
-    (_, pBorrowShares, _) = MORPHO.position(currentContract.ID, borrower);
+    PreLiquidation.Position p = MORPHO.position_(currentContract.ID, borrower);
 
     mathint ltv = getLtv(borrower);
 
@@ -131,7 +130,7 @@ rule excessivePreliquidationWithAssetsReverts(env e, address borrower, uint256 s
                                                    currentContract.PRE_LCF_1,
                                                    currentContract.PRE_LCF_2) ;
 
-    mathint repayableShares = summaryWMulDown(pBorrowShares, require_uint256(closeFactor));
+    mathint repayableShares = summaryWMulDown(p.borrowShares, require_uint256(closeFactor));
 
     preLiquidate@withrevert(e, borrower, seizedAssets, 0, data);
 
@@ -144,19 +143,16 @@ rule excessivePreliquidationWithAssetsReverts(env e, address borrower, uint256 s
 
 // Check that repaying more shares than available or allowed by the preLCF would revert.
 rule excessivePreliquidationWithSharesReverts(env e, address borrower, uint256 repaidShares, bytes data) {
-    // Position values.
-    uint256 pBorrowShares;
-
     requireInvariant preLltvConsistent();
     requireInvariant preLCFConsistent();
     requireInvariant preLIFConsistent();
 
-    PreLiquidationHarness.Market m = market_(currentContract.ID);
+    PreLiquidation.Market m = MORPHO.market_(currentContract.ID);
 
     // Ensure that no interest is accumulated.
     require m.lastUpdate == e.block.timestamp;
 
-    (_, pBorrowShares, _) = MORPHO.position(currentContract.ID, borrower);
+    PreLiquidation.Position p = MORPHO.position_(currentContract.ID, borrower);
 
     mathint ltv = getLtv(borrower);
 
@@ -169,7 +165,7 @@ rule excessivePreliquidationWithSharesReverts(env e, address borrower, uint256 r
                                                    currentContract.PRE_LCF_1,
                                                    currentContract.PRE_LCF_2) ;
 
-    mathint repayableShares = summaryWMulDown(pBorrowShares, require_uint256(closeFactor));
+    mathint repayableShares = summaryWMulDown(p.borrowShares, require_uint256(closeFactor));
 
     preLiquidate@withrevert(e, borrower, 0, repaidShares, data);
 

diff --git a/certora/specs/SummaryLib.spec b/certora/specs/SummaryLib.spec
@@ -1,13 +1,13 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 
-using Morpho as MORPHO;
+using MorphoHarness as MORPHO;
+using Util as Util;
 
 methods {
-    function MORPHO.position(PreLiquidationHarness.Id, address) external
-        returns (uint256, uint128, uint128) envfree;
-
-    function market_(PreLiquidationHarness.Id) external
-        returns (PreLiquidationHarness.Market memory) envfree;
+    function MORPHO.market_(PreLiquidation.Id) external
+        returns (PreLiquidation.Market memory) envfree;
+    function MORPHO.position_(PreLiquidation.Id, address) external
+        returns (PreLiquidation.Position memory) envfree;
 }
 
 definition WAD() returns uint256 = 10^18;
@@ -59,8 +59,8 @@ function summaryToAssetsUp(uint256 shares, uint256 totalAssets, uint256 totalSha
                            require_uint256(totalShares + VIRTUAL_SHARES()));
 }
 
-function summaryMarketParams() returns PreLiquidationHarness.MarketParams {
-    PreLiquidationHarness.MarketParams x;
+function summaryMarketParams() returns PreLiquidation.MarketParams {
+    PreLiquidation.MarketParams x;
     require
         x.loanToken == currentContract.LOAN_TOKEN
         && x.collateralToken == currentContract.COLLATERAL_TOKEN
@@ -87,22 +87,17 @@ function mockPrice() returns uint256 {
 }
 
 
-// Ensure this function is only used when no interest is accrued,
-// or enforce that the last update matches the current timestamp.
+// Ensure this function is only used when no interest is accrued, or enforce that the last update matches the current timestamp.
 function positionAsAssets (address borrower) returns (uint256, uint256) {
-    uint256 pBorrowShares;
-    uint256 pCollateral;
-
-    PreLiquidationHarness.Market m = market_(currentContract.ID);
-
-    (_, pBorrowShares, pCollateral) = MORPHO.position(currentContract.ID, borrower);
+    PreLiquidation.Market m = MORPHO.market_(currentContract.ID);
+    PreLiquidation.Position p = MORPHO.position_(currentContract.ID, borrower);
 
-    uint256 collateralQuoted = require_uint256(summaryMulDivDown(pCollateral, mockPrice(), ORACLE_PRICE_SCALE()));
+    uint256 collateralQuoted = require_uint256(summaryMulDivDown(p.collateral, mockPrice(), ORACLE_PRICE_SCALE()));
 
     // Safe require because the implementation would revert, see rule zeroCollateralQuotedReverts.
     require collateralQuoted > 0;
 
-    uint256 borrowed = require_uint256(summaryToAssetsUp(pBorrowShares, m.totalBorrowAssets, m.totalBorrowShares));
+    uint256 borrowed = require_uint256(summaryToAssetsUp(p.borrowShares, m.totalBorrowAssets, m.totalBorrowShares));
 
     return (borrowed, collateralQuoted);
 }