From f6f620ef8f3c93245299d31e790671fdb3caab28 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 22 Nov 2024 12:19:07 +0100 Subject: [PATCH 01/12] feat: start liquidate buffer --- certora/confs/LiquidateBuffer.conf | 11 +++++ certora/harness/MorphoLiquidateHarness.sol | 38 +++++++++++++++++ certora/harness/Util.sol | 4 ++ certora/specs/LiquidateBuffer.spec | 49 ++++++++++++++++++++++ 4 files changed, 102 insertions(+) create mode 100644 certora/confs/LiquidateBuffer.conf create mode 100644 certora/harness/MorphoLiquidateHarness.sol create mode 100644 certora/specs/LiquidateBuffer.spec diff --git a/certora/confs/LiquidateBuffer.conf b/certora/confs/LiquidateBuffer.conf new file mode 100644 index 00000000..15ef761d --- /dev/null +++ b/certora/confs/LiquidateBuffer.conf @@ -0,0 +1,11 @@ +{ + "files": [ + "certora/harness/MorphoLiquidateHarness.sol", + "certora/harness/Util.sol" + ], + "solc": "solc-0.8.19", + "verify": "MorphoLiquidateHarness:certora/specs/LiquidateBuffer.spec", + "rule_sanity": "basic", + "server": "production", + "msg": "Morpho Blue Liquidate Buffer" +} diff --git a/certora/harness/MorphoLiquidateHarness.sol b/certora/harness/MorphoLiquidateHarness.sol new file mode 100644 index 00000000..6b402119 --- /dev/null +++ b/certora/harness/MorphoLiquidateHarness.sol @@ -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); + } +} diff --git a/certora/harness/Util.sol b/certora/harness/Util.sol index cef51dea..823dc6f7 100644 --- a/certora/harness/Util.sol +++ b/certora/harness/Util.sol @@ -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(); } diff --git a/certora/specs/LiquidateBuffer.spec b/certora/specs/LiquidateBuffer.spec new file mode 100644 index 00000000..65fb1e45 --- /dev/null +++ b/certora/specs/LiquidateBuffer.spec @@ -0,0 +1,49 @@ +// SPDX-License-Identifier: GPL-2.0-or-later + +using Util as Util; + +methods { + function liquidateView(MorphoLiquidateHarness.MarketParams, uint256, uint256, uint256) external returns (uint256, uint256, uint256, uint256) envfree; + + function extSloads(bytes32[]) external returns (bytes32[]) => NONDET DELETE; + + 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 { + // Safe require because the reference implementation would revert. + return require_uint256((x * y + (d - 1)) / d); +} + +function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 { + // Safe require because the reference implementation would revert. + return require_uint256((x * y) / d); +} + +rule liquidateImprovePosition(MorphoLiquidateHarness.MarketParams marketParams, uint256 seizedAssetsInput, uint256 repaidSharesInput) { + uint256 collateralPrice; + + // uint256 borrowerShares; + // uint256 borrowerCollateral; + + // require borrowerShares < totalShares + // require borrowerAssets < totalAssets + + // require LTV < 1 / LIF; + + require seizedAssetsInput > 0 && repaidSharesInput == 0; + + uint256 seizedAssets; + uint256 repaidShares; + uint256 repaidAssets; + uint256 lif; + (seizedAssets, repaidShares, repaidAssets, lif) = liquidateView(marketParams, seizedAssetsInput, repaidSharesInput, collateralPrice); + + assert summaryMulDivDown(lif, repaidAssets, WAD) >= summaryMulDivUp(seizedAssets, collateralPrice, oraclePriceScale()); + + // assert repaidShares * borrowerCollateral > seizedAssets * borrowerShares; +} From 6168626731ad5e48a71f96ec779e3a02af6aa172 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 22 Nov 2024 13:40:24 +0100 Subject: [PATCH 02/12] fix: compilation with Util --- .github/workflows/certora.yml | 1 + certora/specs/LiquidateBuffer.spec | 3 ++- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 87a17a69..9eef0744 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -23,6 +23,7 @@ jobs: - ExchangeRate - Health - LibSummary + - LiquidateBuffer - Liveness - Reentrancy - Reverts diff --git a/certora/specs/LiquidateBuffer.spec b/certora/specs/LiquidateBuffer.spec index 65fb1e45..fe1f4fa1 100644 --- a/certora/specs/LiquidateBuffer.spec +++ b/certora/specs/LiquidateBuffer.spec @@ -7,6 +7,7 @@ methods { function extSloads(bytes32[]) external returns (bytes32[]) => NONDET DELETE; + function Util.wad() external returns (uint256) envfree; function Util.libId(MorphoLiquidateHarness.MarketParams) external returns (MorphoLiquidateHarness.Id) envfree; function Util.oraclePriceScale() external returns (uint256) envfree; @@ -43,7 +44,7 @@ rule liquidateImprovePosition(MorphoLiquidateHarness.MarketParams marketParams, uint256 lif; (seizedAssets, repaidShares, repaidAssets, lif) = liquidateView(marketParams, seizedAssetsInput, repaidSharesInput, collateralPrice); - assert summaryMulDivDown(lif, repaidAssets, WAD) >= summaryMulDivUp(seizedAssets, collateralPrice, oraclePriceScale()); + assert summaryMulDivDown(lif, repaidAssets, Util.wad()) >= summaryMulDivUp(seizedAssets, collateralPrice, Util.oraclePriceScale()); // assert repaidShares * borrowerCollateral > seizedAssets * borrowerShares; } From 701d11d14f93bbff1616d12ef3bbabc4e665aaf9 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 22 Nov 2024 14:35:17 +0100 Subject: [PATCH 03/12] feat: start borrower proof --- certora/specs/LiquidateBuffer.spec | 26 ++++++++++++++++++-------- 1 file changed, 18 insertions(+), 8 deletions(-) diff --git a/certora/specs/LiquidateBuffer.spec b/certora/specs/LiquidateBuffer.spec index fe1f4fa1..2dd46874 100644 --- a/certora/specs/LiquidateBuffer.spec +++ b/certora/specs/LiquidateBuffer.spec @@ -3,10 +3,12 @@ using Util as Util; methods { - function liquidateView(MorphoLiquidateHarness.MarketParams, uint256, uint256, uint256) external returns (uint256, uint256, uint256, uint256) envfree; - function extSloads(bytes32[]) external returns (bytes32[]) => NONDET DELETE; + 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; @@ -26,25 +28,33 @@ function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 { } rule liquidateImprovePosition(MorphoLiquidateHarness.MarketParams marketParams, uint256 seizedAssetsInput, uint256 repaidSharesInput) { - uint256 collateralPrice; + MorphoLiquidateHarness.Id id = Util.libId(marketParams); - // uint256 borrowerShares; - // uint256 borrowerCollateral; + // TODO: use a fixed price oracle instead of passing it to liquidateView. + uint256 collateralPrice; - // require borrowerShares < totalShares - // require borrowerAssets < totalAssets + // TODO: take those directly from the borrower, and manage accrue interest. + uint256 borrowerShares; + uint256 borrowerCollateral; - // require LTV < 1 / LIF; + require borrowerShares <= market_(id).totalBorrowShares; + uint256 borrowerAssets = summaryMulDivUp(borrowerShares, virtualTotalBorrowAssets(id), virtualTotalBorrowShares(id)); + require borrowerAssets > 0; require seizedAssetsInput > 0 && repaidSharesInput == 0; uint256 seizedAssets; uint256 repaidShares; uint256 repaidAssets; + require repaidAssets > 0; uint256 lif; (seizedAssets, repaidShares, repaidAssets, lif) = liquidateView(marketParams, seizedAssetsInput, repaidSharesInput, collateralPrice); + require summaryMulDivUp(borrowerCollateral, collateralPrice, Util.oraclePriceScale()) >= summaryMulDivUp(lif, borrowerAssets, Util.wad()); + assert summaryMulDivDown(summaryMulDivUp(borrowerCollateral, collateralPrice, Util.oraclePriceScale()), Util.wad(), borrowerAssets) >= lif; + assert summaryMulDivDown(lif, repaidAssets, Util.wad()) >= summaryMulDivUp(seizedAssets, collateralPrice, Util.oraclePriceScale()); + assert lif >= summaryMulDivDown(summaryMulDivUp(seizedAssets, collateralPrice, Util.oraclePriceScale()), Util.wad(), repaidAssets); // assert repaidShares * borrowerCollateral > seizedAssets * borrowerShares; } From f7ac78a682ac8a827fa056e58143196b049465ce Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 22 Nov 2024 15:11:46 +0100 Subject: [PATCH 04/12] refactor: simplify with wDivDown --- certora/specs/LiquidateBuffer.spec | 24 ++++++++++++++++-------- 1 file changed, 16 insertions(+), 8 deletions(-) diff --git a/certora/specs/LiquidateBuffer.spec b/certora/specs/LiquidateBuffer.spec index 2dd46874..84262e4c 100644 --- a/certora/specs/LiquidateBuffer.spec +++ b/certora/specs/LiquidateBuffer.spec @@ -5,6 +5,7 @@ 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; @@ -18,20 +19,25 @@ methods { } function summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 { - // Safe require because the reference implementation would revert. + // Todo: why is this require ok ? return require_uint256((x * y + (d - 1)) / d); } function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 { - // Safe require because the reference implementation would revert. + // Todo: why is this require ok ? return require_uint256((x * y) / d); } +function wDivDown(uint256 x, uint256 y) returns uint256 { + return summaryMulDivDown(x, Util.wad(), y); +} + 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; @@ -41,20 +47,22 @@ rule liquidateImprovePosition(MorphoLiquidateHarness.MarketParams marketParams, uint256 borrowerAssets = summaryMulDivUp(borrowerShares, virtualTotalBorrowAssets(id), virtualTotalBorrowShares(id)); require borrowerAssets > 0; - require seizedAssetsInput > 0 && repaidSharesInput == 0; + require (seizedAssetsInput > 0 && repaidSharesInput == 0) || (seizedAssetsInput == 0 && repaidSharesInput > 0); uint256 seizedAssets; uint256 repaidShares; uint256 repaidAssets; - require repaidAssets > 0; uint256 lif; (seizedAssets, repaidShares, repaidAssets, lif) = liquidateView(marketParams, seizedAssetsInput, repaidSharesInput, collateralPrice); + require repaidAssets > 0; - require summaryMulDivUp(borrowerCollateral, collateralPrice, Util.oraclePriceScale()) >= summaryMulDivUp(lif, borrowerAssets, Util.wad()); - assert summaryMulDivDown(summaryMulDivUp(borrowerCollateral, collateralPrice, Util.oraclePriceScale()), Util.wad(), borrowerAssets) >= lif; + uint256 borrowerCollateralQuoted = summaryMulDivUp(borrowerCollateral, collateralPrice, Util.oraclePriceScale()); + require borrowerCollateralQuoted >= summaryMulDivUp(lif, borrowerAssets, Util.wad()); + assert wDivDown(borrowerCollateralQuoted, borrowerAssets) >= lif; - assert summaryMulDivDown(lif, repaidAssets, Util.wad()) >= summaryMulDivUp(seizedAssets, collateralPrice, Util.oraclePriceScale()); - assert lif >= summaryMulDivDown(summaryMulDivUp(seizedAssets, collateralPrice, Util.oraclePriceScale()), Util.wad(), repaidAssets); + uint256 seizedCollateralQuoted = summaryMulDivUp(seizedAssets, collateralPrice, Util.oraclePriceScale()); + assert summaryMulDivDown(lif, repaidAssets, Util.wad()) >= seizedCollateralQuoted; + assert lif >= wDivDown(seizedCollateralQuoted, repaidAssets); // assert repaidShares * borrowerCollateral > seizedAssets * borrowerShares; } From 1809386b378f8a8ae9132b65d5e1bce27686bff9 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 22 Nov 2024 16:20:21 +0100 Subject: [PATCH 05/12] feat: share improvement --- certora/specs/LiquidateBuffer.spec | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/certora/specs/LiquidateBuffer.spec b/certora/specs/LiquidateBuffer.spec index 84262e4c..997ea63c 100644 --- a/certora/specs/LiquidateBuffer.spec +++ b/certora/specs/LiquidateBuffer.spec @@ -32,6 +32,10 @@ function wDivDown(uint256 x, uint256 y) returns uint256 { return summaryMulDivDown(x, Util.wad(), y); } +function wDivUp(uint256 x, uint256 y) returns uint256 { + return summaryMulDivUp(x, Util.wad(), y); +} + rule liquidateImprovePosition(MorphoLiquidateHarness.MarketParams marketParams, uint256 seizedAssetsInput, uint256 repaidSharesInput) { MorphoLiquidateHarness.Id id = Util.libId(marketParams); @@ -56,13 +60,21 @@ rule liquidateImprovePosition(MorphoLiquidateHarness.MarketParams marketParams, (seizedAssets, repaidShares, repaidAssets, lif) = liquidateView(marketParams, seizedAssetsInput, repaidSharesInput, collateralPrice); require repaidAssets > 0; - uint256 borrowerCollateralQuoted = summaryMulDivUp(borrowerCollateral, collateralPrice, Util.oraclePriceScale()); + uint256 borrowerCollateralQuoted = summaryMulDivDown(borrowerCollateral, collateralPrice, Util.oraclePriceScale()); require borrowerCollateralQuoted >= summaryMulDivUp(lif, borrowerAssets, Util.wad()); assert wDivDown(borrowerCollateralQuoted, borrowerAssets) >= lif; uint256 seizedCollateralQuoted = summaryMulDivUp(seizedAssets, collateralPrice, Util.oraclePriceScale()); assert summaryMulDivDown(lif, repaidAssets, Util.wad()) >= seizedCollateralQuoted; - assert lif >= wDivDown(seizedCollateralQuoted, repaidAssets); + assert lif >= wDivUp(seizedCollateralQuoted, repaidAssets); + + uint256 newBorrowerShares = require_uint256(borrowerShares - repaidShares); + uint256 newTotalShares = require_uint256(virtualTotalBorrowShares(id) - repaidShares); + uint256 newTotalAssets = require_uint256(virtualTotalBorrowAssets(id) - repaidAssets); + + require seizedAssets <= borrowerCollateral; + + uint256 newBorrowerAssets = summaryMulDivUp(newBorrowerShares, newTotalAssets, newTotalShares); - // assert repaidShares * borrowerCollateral > seizedAssets * borrowerShares; + assert repaidShares * borrowerCollateral >= seizedAssets * borrowerShares; } From 29762f55f43f102920d71ef328fbbaac72458a01 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 22 Nov 2024 17:50:42 +0100 Subject: [PATCH 06/12] refactor: simplify assumptions --- certora/specs/LiquidateBuffer.spec | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/certora/specs/LiquidateBuffer.spec b/certora/specs/LiquidateBuffer.spec index 997ea63c..ba0018c3 100644 --- a/certora/specs/LiquidateBuffer.spec +++ b/certora/specs/LiquidateBuffer.spec @@ -49,7 +49,6 @@ rule liquidateImprovePosition(MorphoLiquidateHarness.MarketParams marketParams, require borrowerShares <= market_(id).totalBorrowShares; uint256 borrowerAssets = summaryMulDivUp(borrowerShares, virtualTotalBorrowAssets(id), virtualTotalBorrowShares(id)); - require borrowerAssets > 0; require (seizedAssetsInput > 0 && repaidSharesInput == 0) || (seizedAssetsInput == 0 && repaidSharesInput > 0); @@ -61,12 +60,10 @@ rule liquidateImprovePosition(MorphoLiquidateHarness.MarketParams marketParams, require repaidAssets > 0; uint256 borrowerCollateralQuoted = summaryMulDivDown(borrowerCollateral, collateralPrice, Util.oraclePriceScale()); - require borrowerCollateralQuoted >= summaryMulDivUp(lif, borrowerAssets, Util.wad()); - assert wDivDown(borrowerCollateralQuoted, borrowerAssets) >= lif; + require summaryMulDivUp(lif, borrowerAssets, Util.wad()) <= borrowerCollateralQuoted; + assert borrowerCollateral * collateralPrice * Util.wad() * virtualTotalBorrowShares(id) >= lif * borrowerShares * virtualTotalBorrowAssets(id) * Util.oraclePriceScale(); - uint256 seizedCollateralQuoted = summaryMulDivUp(seizedAssets, collateralPrice, Util.oraclePriceScale()); - assert summaryMulDivDown(lif, repaidAssets, Util.wad()) >= seizedCollateralQuoted; - assert lif >= wDivUp(seizedCollateralQuoted, repaidAssets); + assert lif * virtualTotalBorrowAssets(id) * Util.oraclePriceScale() * repaidShares >= virtualTotalBorrowShares(id) * collateralPrice * seizedAssets * Util.wad(); uint256 newBorrowerShares = require_uint256(borrowerShares - repaidShares); uint256 newTotalShares = require_uint256(virtualTotalBorrowShares(id) - repaidShares); From 44d51a1af92e111e0f6564ba8a2300a9dbb94170 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 22 Nov 2024 18:07:04 +0100 Subject: [PATCH 07/12] refactor: order in the multiplication --- certora/specs/LiquidateBuffer.spec | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/certora/specs/LiquidateBuffer.spec b/certora/specs/LiquidateBuffer.spec index ba0018c3..f0276595 100644 --- a/certora/specs/LiquidateBuffer.spec +++ b/certora/specs/LiquidateBuffer.spec @@ -61,9 +61,9 @@ rule liquidateImprovePosition(MorphoLiquidateHarness.MarketParams marketParams, uint256 borrowerCollateralQuoted = summaryMulDivDown(borrowerCollateral, collateralPrice, Util.oraclePriceScale()); require summaryMulDivUp(lif, borrowerAssets, Util.wad()) <= borrowerCollateralQuoted; - assert borrowerCollateral * collateralPrice * Util.wad() * virtualTotalBorrowShares(id) >= lif * borrowerShares * virtualTotalBorrowAssets(id) * Util.oraclePriceScale(); + assert borrowerCollateral * collateralPrice * virtualTotalBorrowShares(id) * Util.wad() >= borrowerShares * Util.oraclePriceScale() * virtualTotalBorrowAssets(id) * lif; - assert lif * virtualTotalBorrowAssets(id) * Util.oraclePriceScale() * repaidShares >= virtualTotalBorrowShares(id) * collateralPrice * seizedAssets * Util.wad(); + 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); From 6b41f7b3a30f18d4a631517d5ad6008673c25205 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 22 Nov 2024 18:17:26 +0100 Subject: [PATCH 08/12] feat: add payload --- certora/specs/LiquidateBuffer.spec | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/certora/specs/LiquidateBuffer.spec b/certora/specs/LiquidateBuffer.spec index f0276595..4cd657d8 100644 --- a/certora/specs/LiquidateBuffer.spec +++ b/certora/specs/LiquidateBuffer.spec @@ -61,7 +61,7 @@ rule liquidateImprovePosition(MorphoLiquidateHarness.MarketParams marketParams, 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 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(); @@ -69,9 +69,9 @@ rule liquidateImprovePosition(MorphoLiquidateHarness.MarketParams marketParams, uint256 newTotalShares = require_uint256(virtualTotalBorrowShares(id) - repaidShares); uint256 newTotalAssets = require_uint256(virtualTotalBorrowAssets(id) - repaidAssets); - require seizedAssets <= borrowerCollateral; - uint256 newBorrowerAssets = summaryMulDivUp(newBorrowerShares, newTotalAssets, newTotalShares); + uint256 newBorrowerCollateral = require_uint256(borrowerCollateral - seizedAssets); assert repaidShares * borrowerCollateral >= seizedAssets * borrowerShares; + assert borrowerAssets * newBorrowerCollateral >= newBorrowerAssets * borrowerCollateral; } From f04942e0fdcbcd165bc2be1524cee5614e81c55f Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 22 Nov 2024 19:00:18 +0100 Subject: [PATCH 09/12] feat: add hints for the final assert --- certora/specs/LiquidateBuffer.spec | 12 +++--------- 1 file changed, 3 insertions(+), 9 deletions(-) diff --git a/certora/specs/LiquidateBuffer.spec b/certora/specs/LiquidateBuffer.spec index 4cd657d8..0259d79b 100644 --- a/certora/specs/LiquidateBuffer.spec +++ b/certora/specs/LiquidateBuffer.spec @@ -28,14 +28,6 @@ function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 { return require_uint256((x * y) / d); } -function wDivDown(uint256 x, uint256 y) returns uint256 { - return summaryMulDivDown(x, Util.wad(), y); -} - -function wDivUp(uint256 x, uint256 y) returns uint256 { - return summaryMulDivUp(x, Util.wad(), y); -} - rule liquidateImprovePosition(MorphoLiquidateHarness.MarketParams marketParams, uint256 seizedAssetsInput, uint256 repaidSharesInput) { MorphoLiquidateHarness.Id id = Util.libId(marketParams); @@ -57,7 +49,6 @@ rule liquidateImprovePosition(MorphoLiquidateHarness.MarketParams marketParams, uint256 repaidAssets; uint256 lif; (seizedAssets, repaidShares, repaidAssets, lif) = liquidateView(marketParams, seizedAssetsInput, repaidSharesInput, collateralPrice); - require repaidAssets > 0; uint256 borrowerCollateralQuoted = summaryMulDivDown(borrowerCollateral, collateralPrice, Util.oraclePriceScale()); require summaryMulDivUp(lif, borrowerAssets, Util.wad()) <= borrowerCollateralQuoted; @@ -73,5 +64,8 @@ rule liquidateImprovePosition(MorphoLiquidateHarness.MarketParams marketParams, 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 >= newBorrowerAssets * borrowerCollateral; } From 60991b4fe9b240d32bb49bc05fc6dc6df4886b01 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 25 Nov 2024 13:17:08 +0100 Subject: [PATCH 10/12] fix: wait for results in the CI --- .github/workflows/certora.yml | 2 +- certora/specs/LiquidateBuffer.spec | 5 +++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 9eef0744..4c503fb8 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -50,6 +50,6 @@ jobs: sudo mv solc-static-linux /usr/local/bin/solc-0.8.19 - name: Verify ${{ matrix.conf }} - run: certoraRun certora/confs/${{ matrix.conf }}.conf + run: certoraRun certora/confs/${{ matrix.conf }}.conf --wait_for_results env: CERTORAKEY: ${{ secrets.CERTORAKEY }} diff --git a/certora/specs/LiquidateBuffer.spec b/certora/specs/LiquidateBuffer.spec index 0259d79b..33ead7f4 100644 --- a/certora/specs/LiquidateBuffer.spec +++ b/certora/specs/LiquidateBuffer.spec @@ -61,11 +61,12 @@ rule liquidateImprovePosition(MorphoLiquidateHarness.MarketParams marketParams, uint256 newTotalAssets = require_uint256(virtualTotalBorrowAssets(id) - repaidAssets); uint256 newBorrowerAssets = summaryMulDivUp(newBorrowerShares, newTotalAssets, newTotalShares); + uint256 newBorrowerAssetsDown = summaryMulDivDown(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 >= newBorrowerAssets * borrowerCollateral; + require borrowerShares * virtualTotalBorrowAssets(id) * newTotalShares * newBorrowerCollateral >= newBorrowerShares * virtualTotalBorrowShares(id) * newTotalAssets * borrowerCollateral; + assert borrowerAssets * newBorrowerCollateral >= newBorrowerAssetsDown * borrowerCollateral; } From 5179b34c14b451d974b4766a7dbd68959f1b3fc3 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 26 Nov 2024 09:58:51 +0100 Subject: [PATCH 11/12] Revert "fix: wait for results in the CI" This reverts commit 60991b4fe9b240d32bb49bc05fc6dc6df4886b01. --- .github/workflows/certora.yml | 2 +- certora/specs/LiquidateBuffer.spec | 5 ++--- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 4c503fb8..9eef0744 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -50,6 +50,6 @@ jobs: sudo mv solc-static-linux /usr/local/bin/solc-0.8.19 - name: Verify ${{ matrix.conf }} - run: certoraRun certora/confs/${{ matrix.conf }}.conf --wait_for_results + run: certoraRun certora/confs/${{ matrix.conf }}.conf env: CERTORAKEY: ${{ secrets.CERTORAKEY }} diff --git a/certora/specs/LiquidateBuffer.spec b/certora/specs/LiquidateBuffer.spec index 33ead7f4..0259d79b 100644 --- a/certora/specs/LiquidateBuffer.spec +++ b/certora/specs/LiquidateBuffer.spec @@ -61,12 +61,11 @@ rule liquidateImprovePosition(MorphoLiquidateHarness.MarketParams marketParams, uint256 newTotalAssets = require_uint256(virtualTotalBorrowAssets(id) - repaidAssets); uint256 newBorrowerAssets = summaryMulDivUp(newBorrowerShares, newTotalAssets, newTotalShares); - uint256 newBorrowerAssetsDown = summaryMulDivDown(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); - require borrowerShares * virtualTotalBorrowAssets(id) * newTotalShares * newBorrowerCollateral >= newBorrowerShares * virtualTotalBorrowShares(id) * newTotalAssets * borrowerCollateral; - assert borrowerAssets * newBorrowerCollateral >= newBorrowerAssetsDown * borrowerCollateral; + assert borrowerShares * virtualTotalBorrowAssets(id) * newTotalShares * newBorrowerCollateral >= newBorrowerShares * virtualTotalBorrowShares(id) * newTotalAssets * borrowerCollateral; + assert borrowerAssets * newBorrowerCollateral >= newBorrowerAssets * borrowerCollateral; } From 18c624399265c491406a69aa448b161441c922da Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Sat, 30 Nov 2024 18:00:34 +0100 Subject: [PATCH 12/12] chore: try out multiple seeds for Z3 --- certora/confs/LiquidateBuffer.conf | 8 ++++++++ certora/specs/LiquidateBuffer.spec | 2 +- 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/certora/confs/LiquidateBuffer.conf b/certora/confs/LiquidateBuffer.conf index 15ef761d..b0c7a702 100644 --- a/certora/confs/LiquidateBuffer.conf +++ b/certora/confs/LiquidateBuffer.conf @@ -5,6 +5,14 @@ ], "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" diff --git a/certora/specs/LiquidateBuffer.spec b/certora/specs/LiquidateBuffer.spec index 0259d79b..b444c64a 100644 --- a/certora/specs/LiquidateBuffer.spec +++ b/certora/specs/LiquidateBuffer.spec @@ -67,5 +67,5 @@ rule liquidateImprovePosition(MorphoLiquidateHarness.MarketParams marketParams, 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 >= newBorrowerAssets * borrowerCollateral; + // assert borrowerAssets * newBorrowerCollateral >= newBorrowerAssetsDown * borrowerCollateral; }