From f04942e0fdcbcd165bc2be1524cee5614e81c55f Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 22 Nov 2024 19:00:18 +0100 Subject: [PATCH] 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; }