invariant_reserves failure when take / bucketTake (#1050)

* Add test_regression_failure_reserves_bucketTake_18precision

* Add regular take test failure

* adjust reserves tolerance to allow for large inflators

* fix issue with extreme TPs and reserves accrusing

* Add test_regression_reservesTakeAction_failure

* added tolerance for large inflator value in reserves change for takeAuction

* added comments to regression test sequences

* Commented change to reserves error margin

* fixed up invariants.md to reflect code

---------

Co-authored-by: mwc <[email protected]>
Co-authored-by: Ian Harvey <[email protected]>

Author: 3 people

tests/INVARIANTS.md

@@ -64,7 +64,7 @@
 - **R7**: Exchange rates are unchanged under depositTakes
 - **R8**: Exchange rates are unchanged under arbTakes
 
-## Reserves (margin of 1e15 on comparisons)
+## Reserves (margin of 1e13 on comparisons)
 - **RE1**:  Reserves are unchanged by pledging collateral
 - **RE2**:  Reserves are unchanged by removing collateral
 - **RE3**:  Reserves increase upon every deposit and when moving quote tokens into a lower-priced bucket.

tests/forge/invariants/base/handlers/unbounded/UnboundedLiquidationPoolHandler.sol

@@ -196,11 +196,15 @@ abstract contract UnboundedLiquidationPoolHandler is BaseHandler {
                 kickerReward += afterTakeVars.kickerBond - beforeTakeVars.kickerBond;
             }
 
+            // Reserves can increase by up to 2e-18 (1/5e17) due to rounding error in inflator value multiplied with t0Debt
+            (uint256 inflator, ) = _pool.inflatorInfo();
+            reservesErrorMargin = Math.max(reservesErrorMargin, inflator/5e17);
+
             // **RE7**: Reserves increase with the quote token paid by taker.
             increaseInReserves += totalBalanceAfterTake - totalBalanceBeforeTake;
 
             // **RE9**: Reserves unchanged by takes and bucket takes below TP(at the time of kick)
-            if (auctionInfo.auctionPrice < auctionInfo.debtToCollateral) {
+            if (auctionInfo.auctionPrice < Maths.min(auctionInfo.debtToCollateral, auctionInfo.neutralPrice)) {
                 increaseInReserves = 0;
                 decreaseInReserves = 0;
             }
@@ -294,6 +298,10 @@ abstract contract UnboundedLiquidationPoolHandler is BaseHandler {
                 reservesErrorMargin = (beforeTakeVars.deposit - afterTakeVars.deposit) / auctionInfo.auctionPrice;
             }
 
+            // Reserves can increase by up to 2e-18 (1/5e17) due to rounding error in inflator value multiplied with t0Debt
+            (uint256 inflator, ) = _pool.inflatorInfo();
+            reservesErrorMargin = Math.max(reservesErrorMargin, inflator/5e17);
+
             // In case of bucket take, collateral is taken at bucket price.
             uint256 takePrice = _priceAt(bucketIndex_);