From ec03d254900e976da6a78964a82e7a5833d6af05 Mon Sep 17 00:00:00 2001 From: prateek105 Date: Wed, 10 Jan 2024 19:29:47 +0530 Subject: [PATCH] Add invariant A10: Upon kick 't0ReserveSettleAmount' should be set to 'BorrowerT0Debt * borrowFeeRate / 2' for the kicked borrower --- tests/INVARIANTS.md | 1 + .../base/LiquidationInvariants.t.sol | 14 ++++++++++ .../base/handlers/unbounded/BaseHandler.sol | 9 ++++++ .../UnboundedLiquidationPoolHandler.sol | 28 +++++++++++++++---- .../invariants/interfaces/IBaseHandler.sol | 2 ++ 5 files changed, 48 insertions(+), 6 deletions(-) diff --git a/tests/INVARIANTS.md b/tests/INVARIANTS.md index 22ed7618e..726e1a274 100644 --- a/tests/INVARIANTS.md +++ b/tests/INVARIANTS.md @@ -26,6 +26,7 @@ - **A7**: total bond escrowed accumulator (`AuctionsState.totalBondEscrowed`) should increase when auction is kicked with the difference needed to cover the bond and should decrease only when kicker bonds withdrawn (`Pool.withdrawBonds`). Claimable bonds should be available for withdrawal from pool at any time. - **A8**: Upon a take/arbtake/deposittake the kicker reward <= borrower penalty - **A9**: reference prices in liquidation queue shall not decrease +- **A10**: Upon kick `t0ReserveSettleAmount` should be set to `BorrowerT0Debt * borrowFeeRate / 2` for the kicked borrower. ## Loans - **L1**: for each `Loan` in loans array (`LoansState.loans`) starting from index 1, the corresponding address (`Loan.borrower`) is not `0x`, the borrower t0 debt to collateral (`Loan.t0DebtToCollateral`) is different than 0 and the id mapped in indices mapping (`LoansState.indices`) equals index of loan in loans array. diff --git a/tests/forge/invariants/base/LiquidationInvariants.t.sol b/tests/forge/invariants/base/LiquidationInvariants.t.sol index 9b0727a7f..552142947 100644 --- a/tests/forge/invariants/base/LiquidationInvariants.t.sol +++ b/tests/forge/invariants/base/LiquidationInvariants.t.sol @@ -22,6 +22,7 @@ abstract contract LiquidationInvariants is BasicInvariants { _invariant_A7(); _invariant_A8(); _invariant_A9(); + _invariant_A10(); } /// @dev checks sum of all borrower's t0debt is equals to total pool t0debtInAuction @@ -152,6 +153,19 @@ abstract contract LiquidationInvariants is BasicInvariants { lastReferencePrice = referencePrice; } } + + /// @dev borrower t0 reserve settle amount should be set borrowerT0debt * borrowFeeRate / 2. + function _invariant_A10() internal view { + uint256 actorCount = IBaseHandler(_handler).getActorsCount(); + + for (uint256 i = 0; i < actorCount; i++) { + address borrower = IBaseHandler(_handler).actors(i); + uint256 borrowerT0ReserveSettleAmount = IBaseHandler(_handler).borrowerT0ReserveSettleAmount(borrower); + (,,,,,,,uint256 requiredT0ReserveSettleAmount,,,) = _pool.auctionInfo(borrower); + + require(borrowerT0ReserveSettleAmount == requiredT0ReserveSettleAmount, "Auction Invariant A10"); + } + } function invariant_call_summary() public virtual override useCurrentTimestamp { console.log("\nCall Summary\n"); diff --git a/tests/forge/invariants/base/handlers/unbounded/BaseHandler.sol b/tests/forge/invariants/base/handlers/unbounded/BaseHandler.sol index 17cfcb6dc..daf4848a0 100644 --- a/tests/forge/invariants/base/handlers/unbounded/BaseHandler.sol +++ b/tests/forge/invariants/base/handlers/unbounded/BaseHandler.sol @@ -143,6 +143,9 @@ abstract contract BaseHandler is Test { uint256 public borrowerPenalty; // Borrower penalty on take uint256 public kickerReward; // Kicker reward on take + // Borrower reserve settlement state + mapping(address => uint256) public borrowerT0ReserveSettleAmount; + // All Buckets used in invariant testing that also includes Buckets where collateral is added when a borrower is in auction and has partial NFT EnumerableSet.UintSet internal buckets; @@ -527,6 +530,12 @@ abstract contract BaseHandler is Test { decreaseInBonds = 0; // record totalBondEscrowed before each action (previousTotalBonds, , , , ) = _pool.reservesInfo(); + + // Record borrower reserve settle amount + for(uint256 i = 0; i < actors.length; i++) { + address borrower = actors[i]; + borrowerT0ReserveSettleAmount[borrower] = _getAuctionInfo(borrower).t0ReserveSettleAmount; + } } /********************************/ diff --git a/tests/forge/invariants/base/handlers/unbounded/UnboundedLiquidationPoolHandler.sol b/tests/forge/invariants/base/handlers/unbounded/UnboundedLiquidationPoolHandler.sol index 3a647542a..5d8339e1c 100644 --- a/tests/forge/invariants/base/handlers/unbounded/UnboundedLiquidationPoolHandler.sol +++ b/tests/forge/invariants/base/handlers/unbounded/UnboundedLiquidationPoolHandler.sol @@ -4,12 +4,18 @@ pragma solidity 0.8.18; import '../../../../utils/DSTestPlus.sol'; import '@openzeppelin/contracts/utils/structs/EnumerableSet.sol'; -import { Math } from '@openzeppelin/contracts/utils/math/Math.sol'; - -import { Maths } from 'src/libraries/internal/Maths.sol'; -import { _priceAt, _indexOf, MIN_PRICE, MAX_PRICE } from 'src/libraries/helpers/PoolHelper.sol'; -import { MAX_FENWICK_INDEX } from 'src/libraries/helpers/PoolHelper.sol'; -import { Buckets } from 'src/libraries/internal/Buckets.sol'; +import { Math } from '@openzeppelin/contracts/utils/math/Math.sol'; + +import { Maths } from 'src/libraries/internal/Maths.sol'; +import { + _priceAt, + _indexOf, + _borrowFeeRate, + MIN_PRICE, + MAX_PRICE, + MAX_FENWICK_INDEX +} from 'src/libraries/helpers/PoolHelper.sol'; +import { Buckets } from 'src/libraries/internal/Buckets.sol'; import { BaseHandler } from './BaseHandler.sol'; import '@std/Vm.sol'; @@ -40,6 +46,8 @@ abstract contract UnboundedLiquidationPoolHandler is BaseHandler { BorrowerInfo memory borrowerInfo = _getBorrowerInfo(borrower_); KickerInfo memory kickerInfoBeforeKick = _getKickerInfo(_actor); + (uint256 interestRate, ) = _pool.interestRateInfo(); + // ensure actor always has the amount to pay for bond _ensureQuoteAmount(_actor, borrowerInfo.debt); @@ -53,6 +61,9 @@ abstract contract UnboundedLiquidationPoolHandler is BaseHandler { // **A7**: totalBondEscrowed should increase when auctioned kicked with the difference needed to cover the bond increaseInBonds += kickerInfoAfterKick.totalBond - kickerInfoBeforeKick.totalBond; + + // **A10**: toReserve should be set to borrowerT0debt * borrowerFeeRate / 2 + borrowerT0ReserveSettleAmount[borrower_] = Maths.wmul(borrowerInfo.t0Debt, _borrowFeeRate(interestRate)) / 2; } catch (bytes memory err) { _ensurePoolError(err); } @@ -71,6 +82,8 @@ abstract contract UnboundedLiquidationPoolHandler is BaseHandler { BucketInfo memory bucketInfoBeforeKick = _getBucketInfo(bucketIndex_); KickerInfo memory kickerInfoBeforeKick = _getKickerInfo(_actor); + (uint256 interestRate, ) = _pool.interestRateInfo(); + // record fenwick tree state before action fenwickDeposits[bucketIndex_] = bucketInfoBeforeKick.deposit; @@ -89,6 +102,9 @@ abstract contract UnboundedLiquidationPoolHandler is BaseHandler { // **A7**: totalBondEscrowed should increase when auctioned kicked with the difference needed to cover the bond increaseInBonds += kickerInfoAfterKick.totalBond - kickerInfoBeforeKick.totalBond; + // **A10**: toReserve should be set to borrowerT0debt * borrowerFeeRate / 2 + borrowerT0ReserveSettleAmount[maxBorrower] = Maths.wmul(borrowerInfo.t0Debt, _borrowFeeRate(interestRate)) / 2; + _fenwickRemove(bucketInfoBeforeKick.deposit - bucketInfoAfterKick.deposit, bucketIndex_); } catch (bytes memory err) { _ensurePoolError(err); diff --git a/tests/forge/invariants/interfaces/IBaseHandler.sol b/tests/forge/invariants/interfaces/IBaseHandler.sol index f14fb1023..7c2f7b296 100644 --- a/tests/forge/invariants/interfaces/IBaseHandler.sol +++ b/tests/forge/invariants/interfaces/IBaseHandler.sol @@ -38,5 +38,7 @@ interface IBaseHandler { function lenderDepositTime(address lender, uint256 bucketIndex) external view returns(uint256); + function borrowerT0ReserveSettleAmount(address borrower) external view returns(uint256); + function getBuckets() external view returns(uint256[] memory); } \ No newline at end of file