Skip to content

[Certora] Liquidate buffer #704

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 12 commits into from
Closed
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .github/workflows/certora.yml
Original file line number Diff line number Diff line change
@@ -23,6 +23,7 @@ jobs:
- ExchangeRate
- Health
- LibSummary
- LiquidateBuffer
- Liveness
- Reentrancy
- Reverts
19 changes: 19 additions & 0 deletions certora/confs/LiquidateBuffer.conf
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
{
"files": [
"certora/harness/MorphoLiquidateHarness.sol",
"certora/harness/Util.sol"
],
"solc": "solc-0.8.19",
"verify": "MorphoLiquidateHarness:certora/specs/LiquidateBuffer.spec",
"prover_args": [
"-depth 5",
"-mediumTimeout 5",
"-timeout 3600",
"-adaptiveSolverConfig false",
"-smt_nonLinearArithmetic true",
"-solvers [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:lia2]"
],
"rule_sanity": "basic",
"server": "production",
"msg": "Morpho Blue Liquidate Buffer"
}
38 changes: 38 additions & 0 deletions certora/harness/MorphoLiquidateHarness.sol
Original file line number Diff line number Diff line change
@@ -0,0 +1,38 @@
// SPDX-License-Identifier: GPL-2.0-or-later
pragma solidity 0.8.19;

import "./MorphoHarness.sol";

contract MorphoLiquidateHarness is MorphoHarness {
using MarketParamsLib for MarketParams;
using MathLib for uint256;
using SharesMathLib for uint256;

constructor(address newOwner) MorphoHarness(newOwner) {}

function liquidateView(
MarketParams memory marketParams,
uint256 seizedAssets,
uint256 repaidShares,
uint256 collateralPrice
) external view returns (uint256, uint256, uint256, uint256) {
Id id = marketParams.id();
uint256 liquidationIncentiveFactor = UtilsLib.min(
MAX_LIQUIDATION_INCENTIVE_FACTOR, WAD.wDivDown(WAD - LIQUIDATION_CURSOR.wMulDown(WAD - marketParams.lltv))
);

if (seizedAssets > 0) {
uint256 seizedAssetsQuoted = seizedAssets.mulDivUp(collateralPrice, ORACLE_PRICE_SCALE);

repaidShares = seizedAssetsQuoted.wDivUp(liquidationIncentiveFactor).toSharesUp(
market[id].totalBorrowAssets, market[id].totalBorrowShares
);
} else {
seizedAssets = repaidShares.toAssetsDown(market[id].totalBorrowAssets, market[id].totalBorrowShares)
.wMulDown(liquidationIncentiveFactor).mulDivDown(ORACLE_PRICE_SCALE, collateralPrice);
}
uint256 repaidAssets = repaidShares.toAssetsUp(market[id].totalBorrowAssets, market[id].totalBorrowShares);

return (seizedAssets, repaidShares, repaidAssets, liquidationIncentiveFactor);
}
}
4 changes: 4 additions & 0 deletions certora/harness/Util.sol
Original file line number Diff line number Diff line change
@@ -17,6 +17,10 @@ contract Util {
return MAX_FEE;
}

function oraclePriceScale() external pure returns (uint256) {
return ORACLE_PRICE_SCALE;
}

function libId(MarketParams memory marketParams) external pure returns (Id) {
return marketParams.id();
}
71 changes: 71 additions & 0 deletions certora/specs/LiquidateBuffer.spec
Original file line number Diff line number Diff line change
@@ -0,0 +1,71 @@
// SPDX-License-Identifier: GPL-2.0-or-later

using Util as Util;

methods {
function extSloads(bytes32[]) external returns (bytes32[]) => NONDET DELETE;

function market_(MorphoLiquidateHarness.Id) external returns (MorphoLiquidateHarness.Market) envfree;
function virtualTotalBorrowAssets(MorphoLiquidateHarness.Id) external returns uint256 envfree;
function virtualTotalBorrowShares(MorphoLiquidateHarness.Id) external returns uint256 envfree;
function liquidateView(MorphoLiquidateHarness.MarketParams, uint256, uint256, uint256) external returns (uint256, uint256, uint256, uint256) envfree;

function Util.wad() external returns (uint256) envfree;
function Util.libId(MorphoLiquidateHarness.MarketParams) external returns (MorphoLiquidateHarness.Id) envfree;
function Util.oraclePriceScale() 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 summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 {
// Todo: why is this require ok ?
return require_uint256((x * y + (d - 1)) / d);
}

function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 {
// Todo: why is this require ok ?
return require_uint256((x * y) / d);
}

rule liquidateImprovePosition(MorphoLiquidateHarness.MarketParams marketParams, uint256 seizedAssetsInput, uint256 repaidSharesInput) {
MorphoLiquidateHarness.Id id = Util.libId(marketParams);

// TODO: use a fixed price oracle instead of passing it to liquidateView.
uint256 collateralPrice;
require collateralPrice > 0;

// TODO: take those directly from the borrower, and manage accrue interest.
uint256 borrowerShares;
uint256 borrowerCollateral;

require borrowerShares <= market_(id).totalBorrowShares;
uint256 borrowerAssets = summaryMulDivUp(borrowerShares, virtualTotalBorrowAssets(id), virtualTotalBorrowShares(id));

require (seizedAssetsInput > 0 && repaidSharesInput == 0) || (seizedAssetsInput == 0 && repaidSharesInput > 0);

uint256 seizedAssets;
uint256 repaidShares;
uint256 repaidAssets;
uint256 lif;
(seizedAssets, repaidShares, repaidAssets, lif) = liquidateView(marketParams, seizedAssetsInput, repaidSharesInput, collateralPrice);

uint256 borrowerCollateralQuoted = summaryMulDivDown(borrowerCollateral, collateralPrice, Util.oraclePriceScale());
require summaryMulDivUp(lif, borrowerAssets, Util.wad()) <= borrowerCollateralQuoted;
assert borrowerCollateral * collateralPrice * virtualTotalBorrowShares(id) * Util.wad() >= borrowerShares * Util.oraclePriceScale() * virtualTotalBorrowAssets(id) * lif;

assert repaidShares * Util.oraclePriceScale() * virtualTotalBorrowAssets(id) * lif >= seizedAssets * collateralPrice * virtualTotalBorrowShares(id) * Util.wad();

uint256 newBorrowerShares = require_uint256(borrowerShares - repaidShares);
uint256 newTotalShares = require_uint256(virtualTotalBorrowShares(id) - repaidShares);
uint256 newTotalAssets = require_uint256(virtualTotalBorrowAssets(id) - repaidAssets);

uint256 newBorrowerAssets = summaryMulDivUp(newBorrowerShares, newTotalAssets, newTotalShares);
uint256 newBorrowerCollateral = require_uint256(borrowerCollateral - seizedAssets);

assert repaidShares * borrowerCollateral >= seizedAssets * borrowerShares;
assert borrowerShares * newBorrowerCollateral >= newBorrowerShares * borrowerCollateral;
assert newTotalShares * virtualTotalBorrowAssets(id) >= newTotalAssets * virtualTotalBorrowShares(id);
assert borrowerShares * virtualTotalBorrowAssets(id) * newTotalShares * newBorrowerCollateral >= newBorrowerShares * virtualTotalBorrowShares(id) * newTotalAssets * borrowerCollateral;
// assert borrowerAssets * newBorrowerCollateral >= newBorrowerAssetsDown * borrowerCollateral;
}