Skip to content

Commit

Permalink
Merge pull request #91 from morpho-org/verif/simplify-setup
Browse files Browse the repository at this point in the history 
[Certora] Simplify setup
  • Loading branch information
@MathisGD
MathisGD authored Dec 15, 2024
2 parents efcd39b + 9a89107 commit 16978c5
Show file tree
Hide file tree
Showing 7 changed files with 62 additions and 121 deletions.
10 changes: 5 additions & 5 deletions certora/confs/MarketExists.conf
View file
Original file line number Diff line number Diff line change
@@ -1,18 +1,18 @@
{
"files": [
"src/PreLiquidation.sol",
"lib/morpho-blue/src/Morpho.sol"
"lib/morpho-blue/certora/harness/MorphoHarness.sol",
"src/PreLiquidation.sol"
],
"link": [
"PreLiquidation:MORPHO=Morpho"
"PreLiquidation:MORPHO=MorphoHarness"
],
"parametric_contracts": [
"Morpho"
"MorphoHarness"
],
"solc_optimize": "99999",
"solc_via_ir": true,
"solc_map": {
"Morpho": "solc-0.8.19",
"MorphoHarness": "solc-0.8.19",
"PreLiquidation": "solc-0.8.27"
},
"verify": "PreLiquidation:certora/specs/MarketExists.spec",
Expand Down
8 changes: 3 additions & 5 deletions certora/specs/ConsistentInstantiation.spec
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,13 +3,11 @@
import "SummaryLib.spec";

methods {
// To fix an issue where immutable variables are not linked in the constructor.
function _.market(PreLiquidation.Id) external => DISPATCHER(true);

function Util.libId(PreLiquidation.MarketParams) external
returns PreLiquidation.Id envfree;
}

//Ensure constructor requirements.
// Ensure constructor requirements.

// Base case for mutually dependent invariants.
// Ensure that in a successfully deployed contract the preLLTV value is not zero.
Expand Down Expand Up @@ -49,7 +47,7 @@ invariant preLIFNotZero()
invariant preLIFConsistent()
WAD() < currentContract.PRE_LIF_1
&& currentContract.PRE_LIF_1 <= currentContract.PRE_LIF_2
&& currentContract.PRE_LIF_2 <= summaryWDivDown(WAD(),currentContract.LLTV)
&& currentContract.PRE_LIF_2 <= summaryWDivDown(WAD(), currentContract.LLTV)
{
preserved {
requireInvariant lltvNotZero();
Expand Down
1 change: 0 additions & 1 deletion certora/specs/Liveness.spec
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,6 @@ rule preLiquidateRepays(method f, env e, calldataarg data) {
// Safe require because Morpho cannot send transactions.
require e.msg.sender != currentContract.MORPHO;


// Capture the first method call which is not performed with a CALL opcode.
if (f.selector == sig:preLiquidate(address, uint256, uint256, bytes).selector) {
preLiquidateCalled = true;
Expand Down
15 changes: 4 additions & 11 deletions certora/specs/MarketExists.spec
View file
Original file line number Diff line number Diff line change
@@ -1,12 +1,11 @@
// SPDX-License-Identifier: GPL-2.0-or-later

using Morpho as MORPHO;
using MorphoHarness as MORPHO;

methods {
function MORPHO.lastUpdate(PreLiquidation.Id) external returns (uint256) envfree;
// To fix an issue where immutable variables are not linked in the constructor.
function _.market(PreLiquidation.Id) external => DISPATCHER(true);
function MORPHO.market(PreLiquidation.Id) external
returns (uint128, uint128, uint128,uint128, uint128, uint128) envfree;
function _.price() external => NONDET;
}

persistent ghost uint256 lastTimestamp;
Expand All @@ -19,13 +18,7 @@ hook TIMESTAMP uint newTimestamp {
lastTimestamp = newTimestamp;
}

function lastUpdateIsNotNil(PreLiquidation.Id id) returns bool {
mathint lastUpdate;
(_,_,_,_,lastUpdate,_) = MORPHO.market(id);
return lastUpdate != 0;
}

// Ensure that the pre-liquidation contract interacts with a created market.

invariant marketExists()
lastUpdateIsNotNil(currentContract.ID);
MORPHO.lastUpdate(currentContract.ID) != 0;
87 changes: 28 additions & 59 deletions certora/specs/Reverts.spec
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,21 +4,6 @@ import "ConsistentInstantiation.spec";

methods {
function _.price() external => mockPrice() expect uint256;

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);
function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal
returns uint256 => summaryMulDivUp(a,b,c);

function SharesMathLib.toSharesUp(uint256 a, uint256 b, uint256 c) internal
returns uint256 => summaryToSharesUp(a,b,c);
function SharesMathLib.toAssetsUp(uint256 a, uint256 b, uint256 c) internal
returns uint256 => summaryToAssetsUp(a,b,c);
}

// Checks that onMorphoRepay is only triggered by Morpho.
Expand Down Expand Up @@ -48,7 +33,7 @@ rule zeroCollateralQuotedReverts(env e, address borrower, uint256 seizedAssets,
uint256 higherBound = summaryWMulDown(collateralQuoted, currentContract.LLTV);
uint256 lowerBound = summaryWMulDown(collateralQuoted, currentContract.PRE_LLTV);

assert collateralQuoted == 0 => (lowerBound >= borrowed || borrowed > higherBound);
assert collateralQuoted == 0 => (lowerBound >= borrowed || borrowed > higherBound);
}

// Check that pre-liquidating a position such that LTV <= PRE_LLTV reverts.
Expand All @@ -58,13 +43,11 @@ rule nonLiquidatablePositionReverts(env e, address borrower, uint256 seizedAsset
requireInvariant preLCFConsistent();
requireInvariant preLIFConsistent();

PreLiquidation.Market m = MORPHO.market_(currentContract.ID);

// Ensure that no interest is accumulated.
// Safe require as the invariant ID == marketParams().id() holds, see ConsistentInstantion hashOfMarketParamsOf.
require m.lastUpdate == e.block.timestamp;
require MORPHO.lastUpdate(currentContract.ID) == e.block.timestamp;

mathint ltv = getLtv(borrower);
uint256 ltv = getLtv(borrower);

preLiquidate@withrevert(e, borrower, seizedAssets, 0, data);

Expand All @@ -80,13 +63,11 @@ rule liquidatablePositionReverts(env e, address borrower, uint256 seizedAssets,
requireInvariant preLCFConsistent();
requireInvariant preLIFConsistent();
PreLiquidation.Market m = MORPHO.market_(currentContract.ID);
// Ensure that no interest is accumulated.
// Safe require as the invariant ID == marketParams().id() holds, see ConsistentInstantion hashOfMarketParamsOf.
require m.lastUpdate == e.block.timestamp;
require MORPHO.lastUpdate(currentContract.ID) == e.block.timestamp;

mathint ltv = getLtv(borrower);
uint256 ltv = getLtv(borrower);

preLiquidate@withrevert(e, borrower, seizedAssets, 0, data);

Expand All @@ -102,38 +83,31 @@ rule excessivePreliquidationWithAssetsReverts(env e, address borrower, uint256 s
requireInvariant preLCFConsistent();
requireInvariant preLIFConsistent();

PreLiquidation.Market m = MORPHO.market_(currentContract.ID);

// Ensure that no interest is accumulated.
// Safe require as the invariant ID == marketParams().id() holds, see ConsistentInstantion hashOfMarketParamsOf.
require m.lastUpdate == e.block.timestamp;

PreLiquidation.Position p = MORPHO.position_(currentContract.ID, borrower);
require MORPHO.lastUpdate(currentContract.ID) == e.block.timestamp;

mathint ltv = getLtv(borrower);
uint256 ltv = getLtv(borrower);

mathint preLIF = computeLinearCombination(ltv,
uint256 preLIF = computeLinearCombination(ltv,
currentContract.LLTV,
currentContract.PRE_LLTV,
currentContract.PRE_LIF_1,
currentContract.PRE_LIF_2) ;
currentContract.PRE_LIF_2);

// Safe require as implementation would revert with InconsistentInput.
require seizedAssets > 0;
uint256 seizedAssetsQuoted = summaryMulDivUp(seizedAssets, mockPrice(), ORACLE_PRICE_SCALE());

mathint seizedAssetsQuoted = require_uint256(summaryMulDivUp(seizedAssets, mockPrice(), ORACLE_PRICE_SCALE()));
uint256 totalAssets = MORPHO.virtualTotalBorrowAssets(currentContract.ID);
uint256 totalShares = MORPHO.virtualTotalBorrowShares(currentContract.ID);
uint256 repaidShares = summaryMulDivUp(summaryWDivUp(seizedAssetsQuoted, preLIF), totalShares, totalAssets);

mathint repaidShares = summaryToSharesUp(summaryWDivUp(require_uint256(seizedAssetsQuoted), require_uint256(preLIF)),
m.totalBorrowAssets,
m.totalBorrowShares);

mathint closeFactor = computeLinearCombination(ltv,
currentContract.LLTV,
currentContract.PRE_LLTV,
currentContract.PRE_LCF_1,
currentContract.PRE_LCF_2) ;
uint256 preLCF = computeLinearCombination(ltv,
currentContract.LLTV,
currentContract.PRE_LLTV,
currentContract.PRE_LCF_1,
currentContract.PRE_LCF_2) ;

mathint repayableShares = summaryWMulDown(p.borrowShares, require_uint256(closeFactor));
uint256 repayableShares = summaryWMulDown(MORPHO.borrowShares(currentContract.ID, borrower), preLCF);

preLiquidate@withrevert(e, borrower, seizedAssets, 0, data);

Expand All @@ -150,26 +124,21 @@ rule excessivePreliquidationWithSharesReverts(env e, address borrower, uint256 r
requireInvariant preLCFConsistent();
requireInvariant preLIFConsistent();
PreLiquidation.Market m = MORPHO.market_(currentContract.ID);
// Ensure that no interest is accumulated.
// Safe require as the invariant ID == marketParams().id() holds, see ConsistentInstantion hashOfMarketParamsOf.
require m.lastUpdate == e.block.timestamp;
require MORPHO.lastUpdate(currentContract.ID) == e.block.timestamp;

PreLiquidation.Position p = MORPHO.position_(currentContract.ID, borrower);
uint256 borrowerShares = MORPHO.borrowShares(currentContract.ID, borrower);

mathint ltv = getLtv(borrower);
uint256 ltv = getLtv(borrower);

// Safe require as implementation would revert with InconsistentInput.
require repaidShares > 0;

mathint closeFactor = computeLinearCombination(ltv,
currentContract.LLTV,
currentContract.PRE_LLTV,
currentContract.PRE_LCF_1,
currentContract.PRE_LCF_2) ;
uint256 preLCF = computeLinearCombination(ltv,
currentContract.LLTV,
currentContract.PRE_LLTV,
currentContract.PRE_LCF_1,
currentContract.PRE_LCF_2);

mathint repayableShares = summaryWMulDown(p.borrowShares, require_uint256(closeFactor));
uint256 repayableShares = summaryWMulDown(borrowerShares, preLCF);

preLiquidate@withrevert(e, borrower, 0, repaidShares, data);

Expand Down
4 changes: 2 additions & 2 deletions certora/specs/SafeMath.spec
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,11 +2,11 @@

definition WAD() returns mathint = 10^18;

function summaryWMulDown(mathint x,mathint y) returns mathint {
function summaryWMulDown(mathint x, mathint y) returns mathint {
return (x * y) / WAD();
}

function summaryWDivUp(mathint x,mathint y) returns mathint {
function summaryWDivUp(mathint x, mathint y) returns mathint {
return (x * WAD() + (y-1)) / y;
}

Expand Down
58 changes: 20 additions & 38 deletions certora/specs/SummaryLib.spec
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,20 +4,19 @@ using MorphoHarness as MORPHO;
using Util as Util;

methods {
function MORPHO.market_(PreLiquidation.Id) external
returns (PreLiquidation.Market memory) envfree;
function MORPHO.position_(PreLiquidation.Id, address) external
returns (PreLiquidation.Position memory) envfree;
function MORPHO.virtualTotalBorrowAssets(PreLiquidation.Id) external returns (uint256) envfree;
function MORPHO.virtualTotalBorrowShares(PreLiquidation.Id) external returns (uint256) envfree;
function MORPHO.borrowShares(PreLiquidation.Id, address) external returns (uint256) envfree;
function MORPHO.collateral(PreLiquidation.Id, address) external returns (uint256) envfree;
function MORPHO.lastUpdate(PreLiquidation.Id) external returns (uint256) envfree;

function Util.libId(PreLiquidation.MarketParams) external returns (PreLiquidation.Id) envfree;
}

definition WAD() returns uint256 = 10^18;

definition ORACLE_PRICE_SCALE() returns uint256 = 10^36;

definition VIRTUAL_SHARES() returns uint256 = 10^6;

definition VIRTUAL_ASSETS() returns uint256 = 1;

function summaryWMulDown(uint256 x,uint256 y) returns uint256 {
return summaryMulDivDown(x, y, WAD());
}
Expand All @@ -28,7 +27,7 @@ function summaryWDivDown(uint256 x,uint256 y) returns uint256 {

function summaryMulDivDown(uint256 x,uint256 y, uint256 d) returns uint256 {
// Safe require because the reference implementation would revert.
return require_uint256((x * y)/d);
return require_uint256((x * y) / d);
}

function summaryWDivUp(uint256 x,uint256 y) returns uint256 {
Expand All @@ -37,26 +36,7 @@ function summaryWDivUp(uint256 x,uint256 y) returns uint256 {

function summaryMulDivUp(uint256 x,uint256 y, uint256 d) returns uint256 {
// Safe require because the reference implementation would revert.
return require_uint256((x * y + (d-1)) / d);

}

function summaryToAssetsDown(uint256 shares, uint256 totalAssets, uint256 totalShares) returns uint256 {
return summaryMulDivDown(shares,
require_uint256(totalAssets + VIRTUAL_ASSETS()),
require_uint256(totalShares + VIRTUAL_SHARES()));
}

function summaryToSharesUp(uint256 assets, uint256 totalAssets, uint256 totalShares) returns uint256 {
return summaryMulDivUp(assets,
require_uint256(totalShares + VIRTUAL_SHARES()),
require_uint256(totalAssets + VIRTUAL_ASSETS()));
}

function summaryToAssetsUp(uint256 shares, uint256 totalAssets, uint256 totalShares) returns uint256 {
return summaryMulDivUp(shares,
require_uint256(totalAssets + VIRTUAL_ASSETS()),
require_uint256(totalShares + VIRTUAL_SHARES()));
return require_uint256((x * y + (d - 1)) / d);
}

function summaryMarketParams() returns PreLiquidation.MarketParams {
Expand Down Expand Up @@ -86,18 +66,19 @@ function mockPrice() returns uint256 {
return updatedPrice;
}


// 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) {
PreLiquidation.Market m = MORPHO.market_(currentContract.ID);
PreLiquidation.Position p = MORPHO.position_(currentContract.ID, borrower);
uint256 borrowerShares = MORPHO.borrowShares(currentContract.ID, borrower);
uint256 borrowerCollateral = MORPHO.collateral(currentContract.ID, borrower);

uint256 collateralQuoted = require_uint256(summaryMulDivDown(p.collateral, mockPrice(), ORACLE_PRICE_SCALE()));
uint256 collateralQuoted = summaryMulDivDown(borrowerCollateral, mockPrice(), ORACLE_PRICE_SCALE());

// Safe require because the implementation would revert, see rule zeroCollateralQuotedReverts.
require collateralQuoted > 0;

uint256 borrowed = require_uint256(summaryToAssetsUp(p.borrowShares, m.totalBorrowAssets, m.totalBorrowShares));
uint256 totalAssets = MORPHO.virtualTotalBorrowAssets(currentContract.ID);
uint256 totalShares = MORPHO.virtualTotalBorrowShares(currentContract.ID);
uint256 borrowed = summaryMulDivUp(borrowerShares, totalAssets, totalShares);

return (borrowed, collateralQuoted);
}
Expand All @@ -111,7 +92,8 @@ function getLtv(address borrower) returns uint256 {
return summaryWDivUp(borrowed, collateralQuoted);
}

definition computeLinearCombination(mathint ltv, mathint lltv, mathint preLltv, mathint yAtPreLltv, mathint yAtLltv)
returns mathint = summaryWMulDown(summaryWDivDown(require_uint256(ltv - preLltv),
require_uint256(lltv - preLltv)),
require_uint256(yAtLltv - yAtPreLltv)) + yAtPreLltv;
// Safe requires because the implementation would revert.
definition computeLinearCombination(uint256 ltv, uint256 lltv, uint256 preLltv, uint256 yAtPreLltv, uint256 yAtLltv) returns uint256 =
require_uint256(summaryWMulDown(summaryWDivDown(require_uint256(ltv - preLltv),
require_uint256(lltv - preLltv)),
require_uint256(yAtLltv - yAtPreLltv)) + yAtPreLltv);

0 comments on commit 16978c5

Please sign in to comment.