diff --git a/.gitignore b/.gitignore index 98487917b..84536674b 100644 --- a/.gitignore +++ b/.gitignore @@ -18,6 +18,7 @@ docs/ # Certora .certora** +emv-*-certora* # Hardhat /types diff --git a/certora/harness/MorphoHarness.sol b/certora/harness/MorphoHarness.sol index 6d31a22a6..3b40f10d0 100644 --- a/certora/harness/MorphoHarness.sol +++ b/certora/harness/MorphoHarness.sol @@ -20,4 +20,12 @@ contract MorphoHarness is Morpho { function getMarketId(Market memory market) external pure returns (Id) { return market.id(); } + + function mathLibMulDivUp(uint256 x, uint256 y, uint256 d) public pure returns (uint256) { + return MathLib.mulDivUp(x, y, d); + } + + function mathLibMulDivDown(uint256 x, uint256 y, uint256 d) public pure returns (uint256) { + return MathLib.mulDivDown(x, y, d); + } } diff --git a/certora/scripts/verifyBlueRatioMath.sh b/certora/scripts/verifyBlueRatioMath.sh new file mode 100755 index 000000000..c8cbf3987 --- /dev/null +++ b/certora/scripts/verifyBlueRatioMath.sh @@ -0,0 +1,9 @@ +#!/bin/sh + +certoraRun \ + certora/harness/MorphoHarness.sol \ + --verify MorphoHarness:certora/specs/BlueRatioMath.spec \ + --solc_allow_path src \ + --msg "Morpho Ratio Math" \ + --send_only \ + "$@" diff --git a/certora/scripts/verifyBlueRatioMathSummary.sh b/certora/scripts/verifyBlueRatioMathSummary.sh new file mode 100755 index 000000000..f0a9305b9 --- /dev/null +++ b/certora/scripts/verifyBlueRatioMathSummary.sh @@ -0,0 +1,7 @@ +#!/bin/sh + +certoraRun \ + certora/harness/MorphoHarness.sol \ + --verify MorphoHarness:certora/specs/BlueRatioMathSummary.spec \ + --msg "Morpho Ratio Math Summary" \ + "$@" diff --git a/certora/specs/Blue.spec b/certora/specs/Blue.spec index c31c76f65..e45806fb1 100644 --- a/certora/specs/Blue.spec +++ b/certora/specs/Blue.spec @@ -6,17 +6,22 @@ methods { function totalBorrow(MorphoHarness.Id) external returns uint256 envfree; function totalSupplyShares(MorphoHarness.Id) external returns uint256 envfree; function totalBorrowShares(MorphoHarness.Id) external returns uint256 envfree; + function fee(MorphoHarness.Id) external returns uint256 envfree; + function getMarketId(MorphoHarness.Market) external returns MorphoHarness.Id envfree; + function idToMarket(MorphoHarness.Id) external returns (address, address, address, address, uint256) envfree; + function isAuthorized(address, address) external returns bool envfree; function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; function isLltvEnabled(uint256) external returns bool envfree; function isIrmEnabled(address) external returns bool envfree; - function _.borrowRate(MorphoHarness.Market) external => DISPATCHER(true); + function _.borrowRate(MorphoHarness.Market) external => HAVOC_ECF; function getMarketId(MorphoHarness.Market) external returns MorphoHarness.Id envfree; - // function _.safeTransfer(address, uint256) internal => DISPATCHER(true); - // function _.safeTransferFrom(address, address, uint256) internal => DISPATCHER(true); + // Temporary workaround a bug that requires to have address instead of an interface in the signature + function SafeTransferLib.tmpSafeTransfer(address token, address to, uint256 value) internal => summarySafeTransferFrom(token, currentContract, to, value); + function SafeTransferLib.tmpSafeTransferFrom(address token, address from, address to, uint256 value) internal => summarySafeTransferFrom(token, from, to, value); } ghost mapping(MorphoHarness.Id => mathint) sumSupplyShares @@ -31,6 +36,24 @@ ghost mapping(MorphoHarness.Id => mathint) sumCollateral { init_state axiom (forall MorphoHarness.Id id. sumCollateral[id] == 0); } +ghost mapping(address => mathint) myBalances +{ + init_state axiom (forall address token. myBalances[token] == 0); +} +ghost mapping(address => mathint) expectedAmount +{ + init_state axiom (forall address token. expectedAmount[token] == 0); +} + +ghost mapping(MorphoHarness.Id => address) idToBorrowable; +ghost mapping(MorphoHarness.Id => address) idToCollateral; + +hook Sstore idToMarket[KEY MorphoHarness.Id id].borrowableToken address token STORAGE { + idToBorrowable[id] = token; +} +hook Sstore idToMarket[KEY MorphoHarness.Id id].collateralToken address token STORAGE { + idToCollateral[id] = token; +} hook Sstore supplyShares[KEY MorphoHarness.Id id][KEY address owner] uint256 newShares (uint256 oldShares) STORAGE { sumSupplyShares[id] = sumSupplyShares[id] - oldShares + newShares; @@ -42,10 +65,35 @@ hook Sstore borrowShares[KEY MorphoHarness.Id id][KEY address owner] uint256 new hook Sstore collateral[KEY MorphoHarness.Id id][KEY address owner] uint256 newAmount (uint256 oldAmount) STORAGE { sumCollateral[id] = sumCollateral[id] - oldAmount + newAmount; + expectedAmount[idToCollateral[id]] = expectedAmount[idToCollateral[id]] - oldAmount + newAmount; +} + +hook Sstore totalSupply[KEY MorphoHarness.Id id] uint256 newAmount (uint256 oldAmount) STORAGE { + expectedAmount[idToBorrowable[id]] = expectedAmount[idToBorrowable[id]] - oldAmount + newAmount; +} + +hook Sstore totalBorrow[KEY MorphoHarness.Id id] uint256 newAmount (uint256 oldAmount) STORAGE { + expectedAmount[idToBorrowable[id]] = expectedAmount[idToBorrowable[id]] + oldAmount - newAmount; +} + +function summarySafeTransferFrom(address token, address from, address to, uint256 amount) { + if (from == currentContract) { + myBalances[token] = require_uint256(myBalances[token] - amount); + } + if (to == currentContract) { + myBalances[token] = require_uint256(myBalances[token] + amount); + } } definition VIRTUAL_ASSETS() returns mathint = 1; -definition VIRTUAL_SHARES() returns mathint = 1000000000000000000; +definition VIRTUAL_SHARES() returns mathint = 10^18; +definition MAX_FEE() returns mathint = 10^18 * 25/100; +definition isInitialized(MorphoHarness.Id id) returns bool = + (lastUpdate(id) != 0); + + +invariant feeInRange(MorphoHarness.Id id) + to_mathint(fee(id)) <= MAX_FEE(); invariant sumSupplySharesCorrect(MorphoHarness.Id id) to_mathint(totalSupplyShares(id)) == sumSupplyShares[id]; @@ -55,6 +103,44 @@ invariant sumBorrowSharesCorrect(MorphoHarness.Id id) invariant borrowLessSupply(MorphoHarness.Id id) totalBorrow(id) <= totalSupply(id); +invariant marketInvariant(MorphoHarness.Market market) + isInitialized(getMarketId(market)) => + idToBorrowable[getMarketId(market)] == market.borrowableToken + && idToCollateral[getMarketId(market)] == market.collateralToken; + +invariant isLiquid(address token) + expectedAmount[token] <= myBalances[token] +{ + preserved supply(MorphoHarness.Market market, uint256 _a, uint256 _s, address _o, bytes _d) with (env e) { + requireInvariant marketInvariant(market); + require e.msg.sender != currentContract; + } + preserved withdraw(MorphoHarness.Market market, uint256 _a, uint256 _s, address _o, address _r) with (env e) { + requireInvariant marketInvariant(market); + require e.msg.sender != currentContract; + } + preserved borrow(MorphoHarness.Market market, uint256 _a, uint256 _s, address _o, address _r) with (env e) { + requireInvariant marketInvariant(market); + require e.msg.sender != currentContract; + } + preserved repay(MorphoHarness.Market market, uint256 _a, uint256 _s, address _o, bytes _d) with (env e) { + requireInvariant marketInvariant(market); + require e.msg.sender != currentContract; + } + preserved supplyCollateral(MorphoHarness.Market market, uint256 _a, address _o, bytes _d) with (env e) { + requireInvariant marketInvariant(market); + require e.msg.sender != currentContract; + } + preserved withdrawCollateral(MorphoHarness.Market market, uint256 _a, address _o, address _r) with (env e) { + requireInvariant marketInvariant(market); + require e.msg.sender != currentContract; + } + preserved liquidate(MorphoHarness.Market market, address _b, uint256 _s, bytes _d) with (env e) { + requireInvariant marketInvariant(market); + require e.msg.sender != currentContract; + } +} + rule supplyRevertZero(MorphoHarness.Market market) { env e; bytes b; @@ -65,7 +151,20 @@ rule supplyRevertZero(MorphoHarness.Market market) { } invariant invOnlyEnabledLltv(MorphoHarness.Market market) - lastUpdate(getMarketId(market)) != 0 => isLltvEnabled(market.lltv); + isInitialized(getMarketId(market)) => isLltvEnabled(market.lltv); invariant invOnlyEnabledIrm(MorphoHarness.Market market) - lastUpdate(getMarketId(market)) != 0 => isIrmEnabled(market.irm); + isInitialized(getMarketId(market)) => isIrmEnabled(market.irm); + +rule marketIdUnique() { + MorphoHarness.Market market1; + MorphoHarness.Market market2; + + require getMarketId(market1) == getMarketId(market2); + + assert market1.borrowableToken == market2.borrowableToken; + assert market1.collateralToken == market2.collateralToken; + assert market1.oracle == market2.oracle; + assert market1.irm == market2.irm; + assert market1.lltv == market2.lltv; +} diff --git a/certora/specs/BlueRatioMath.spec b/certora/specs/BlueRatioMath.spec new file mode 100644 index 000000000..ea5a48cb1 --- /dev/null +++ b/certora/specs/BlueRatioMath.spec @@ -0,0 +1,58 @@ +methods { + function totalSupply(MorphoHarness.Id) external returns uint256 envfree; + function totalSupplyShares(MorphoHarness.Id) external returns uint256 envfree; + function fee(MorphoHarness.Id) external returns uint256 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 MathLib.wTaylorCompounded(uint256, uint256) internal returns uint256 => NONDET; + + function _.borrowRate(MorphoHarness.Market) external => HAVOC_ECF; +} + +definition VIRTUAL_ASSETS() returns mathint = 1; +definition VIRTUAL_SHARES() returns mathint = 10^18; +definition MAX_FEE() returns mathint = 10^18 * 25/100; + +invariant feeInRange(MorphoHarness.Id id) + to_mathint(fee(id)) <= MAX_FEE(); + +/* This is a simple overapproximative summary, stating that it rounds in the right direction. + * The summary is checked by the specification in BlueRatioMathSummary.spec. + */ +function summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 { + uint256 result; + require result * d >= x * y; + return result; +} + +/* This is a simple overapproximative summary, stating that it rounds in the right direction. + * The summary is checked by the specification in BlueRatioMathSummary.spec. + */ +function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 { + uint256 result; + require result * d <= x * y; + return result; +} + +rule onlyLiquidateCanDecreasesRatio(method f) +filtered { + f -> f.selector != sig:liquidate(MorphoHarness.Market, address, uint256, bytes).selector +} +{ + MorphoHarness.Id id; + requireInvariant feeInRange(id); + + mathint assetsBefore = totalSupply(id) + VIRTUAL_ASSETS(); + mathint sharesBefore = totalSupplyShares(id) + VIRTUAL_SHARES(); + + env e; + calldataarg args; + f(e,args); + + mathint assetsAfter = totalSupply(id) + VIRTUAL_ASSETS(); + mathint sharesAfter = totalSupplyShares(id) + VIRTUAL_SHARES(); + + // check if ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter; + assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore; +} diff --git a/certora/specs/BlueRatioMathSummary.spec b/certora/specs/BlueRatioMathSummary.spec new file mode 100644 index 000000000..d83492f03 --- /dev/null +++ b/certora/specs/BlueRatioMathSummary.spec @@ -0,0 +1,15 @@ +methods { + function mathLibMulDivUp(uint256, uint256, uint256) external returns uint256 envfree; + function mathLibMulDivDown(uint256, uint256, uint256) external returns uint256 envfree; +} + +/* Check the summaries required by BlueRatioMath.spec */ +rule checkSummaryMulDivUp(uint256 x, uint256 y, uint256 d) { + uint256 result = mathLibMulDivUp(x, y, d); + assert result * d >= x * y; +} + +rule checkSummaryMulDivDown(uint256 x, uint256 y, uint256 d) { + uint256 result = mathLibMulDivDown(x, y, d); + assert result * d <= x * y; +} diff --git a/src/libraries/SafeTransferLib.sol b/src/libraries/SafeTransferLib.sol index cfb7c2ab9..8b968374d 100644 --- a/src/libraries/SafeTransferLib.sol +++ b/src/libraries/SafeTransferLib.sol @@ -11,20 +11,29 @@ import {IERC20} from "../interfaces/IERC20.sol"; /// @notice Library to manage tokens not fully ERC20 compliant: /// not returning a boolean for `transfer` and `transferFrom` functions. library SafeTransferLib { - function safeTransfer(IERC20 token, address to, uint256 value) internal { - (bool success, bytes memory returndata) = address(token).call(abi.encodeCall(token.transfer, (to, value))); + function tmpSafeTransfer(address token, address to, uint256 value) internal { + (bool success, bytes memory returndata) = + address(token).call(abi.encodeCall(IERC20(token).transfer, (to, value))); require( success && address(token).code.length > 0 && (returndata.length == 0 || abi.decode(returndata, (bool))), ErrorsLib.TRANSFER_FAILED ); } - function safeTransferFrom(IERC20 token, address from, address to, uint256 value) internal { + function tmpSafeTransferFrom(address token, address from, address to, uint256 value) internal { (bool success, bytes memory returndata) = - address(token).call(abi.encodeCall(token.transferFrom, (from, to, value))); + address(token).call(abi.encodeCall(IERC20(token).transferFrom, (from, to, value))); require( success && address(token).code.length > 0 && (returndata.length == 0 || abi.decode(returndata, (bool))), ErrorsLib.TRANSFER_FROM_FAILED ); } + + function safeTransfer(IERC20 token, address to, uint256 value) internal { + tmpSafeTransfer(address(token), to, value); + } + + function safeTransferFrom(IERC20 token, address from, address to, uint256 value) internal { + tmpSafeTransferFrom(address(token), from, to, value); + } }