Add invariant A10: Upon kick 't0ReserveSettleAmount' should be set to…

… 'BorrowerT0Debt * borrowFeeRate / 2' for the kicked borrower

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.

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");

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;
+        }
     }
 
     /********************************/

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);

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);
 }