From 8c4110a8134c977d27abc287859c44e362cde28e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Colin=20Gonz=C3=A1lez?= Date: Mon, 28 Oct 2024 13:57:09 +0100 Subject: [PATCH] fix: use getters for the morpho-blue project --- certora/confs/ConsistentInstantiation.conf | 20 +++++++------- certora/confs/Reverts.conf | 18 ++++++------- certora/helpers/PreLiquidationHarness.sol | 18 ------------- certora/helpers/Util.sol | 14 ---------- certora/specs/ConsistentInstantiation.spec | 8 +++--- certora/specs/Reverts.spec | 30 +++++++++------------ certora/specs/SummaryLib.spec | 31 +++++++++------------- 7 files changed, 48 insertions(+), 91 deletions(-) delete mode 100644 certora/helpers/PreLiquidationHarness.sol delete mode 100644 certora/helpers/Util.sol diff --git a/certora/confs/ConsistentInstantiation.conf b/certora/confs/ConsistentInstantiation.conf index 2fef3e8..42e80c9 100644 --- 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 index 095d16f..c5efb9c 100644 --- 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 deleted file mode 100644 index 59891df..0000000 --- a/certora/helpers/PreLiquidationHarness.sol +++ /dev/null @@ -1,18 +0,0 @@ -// SPDX-License-Identifier: GPL-2.0-or-later -pragma solidity 0.8.27; - -import {PreLiquidation, Market, Position, Id, PreLiquidationParams} from "src/PreLiquidation.sol"; - -contract PreLiquidationHarness is PreLiquidation { - constructor(address morpho, Id id, PreLiquidationParams memory _preLiquidationParams) - PreLiquidation(morpho, id, _preLiquidationParams) - {} - - function market_(Id id) external view returns (Market memory) { - return MORPHO.market(id); - } - - function position_(Id id, address borrower) external view returns (Position memory) { - return MORPHO.position(id, borrower); - } -} diff --git a/certora/helpers/Util.sol b/certora/helpers/Util.sol deleted file mode 100644 index 7dc5bef..0000000 --- a/certora/helpers/Util.sol +++ /dev/null @@ -1,14 +0,0 @@ -// SPDX-License-Identifier: GPL-2.0-or-later -pragma solidity 0.8.27; - -import {Id, MarketParams} from "src/PreLiquidation.sol"; - -import {MarketParamsLib} from "lib/morpho-blue/src/libraries/MarketParamsLib.sol"; - -contract Util { - using MarketParamsLib for MarketParams; - - function libId(MarketParams memory marketParams) external pure returns (Id) { - return marketParams.id(); - } -} diff --git a/certora/specs/ConsistentInstantiation.spec b/certora/specs/ConsistentInstantiation.spec index 62d223f..ec8ec1a 100644 --- 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 index 56d4b88..3760287 100644 --- 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 index 6b7804c..f2e898a 100644 --- 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); }