feat: partial liquidations invariant with fix

ebtc-protocol · Oct 9, 2023 · 881cd5d · 881cd5d
1 parent 0f1500b
commit 881cd5d
Show file tree

Hide file tree

Showing 4 changed files with 22 additions and 1 deletion.
diff --git a/packages/contracts/contracts/LiquidationLibrary.sol b/packages/contracts/contracts/LiquidationLibrary.sol
@@ -44,6 +44,7 @@ contract LiquidationLibrary is CdpManagerStorage {
         bytes32 _upperPartialHint,
         bytes32 _lowerPartialHint
     ) external nonReentrantSelfAndBOps {
+        require(_partialAmount != 0, "LiquidationLibrary: use `liquidate` for 100%");
         _liquidateIndividualCdpSetup(_cdpId, _partialAmount, _upperPartialHint, _lowerPartialHint);
     }
 

diff --git a/packages/contracts/contracts/TestContracts/invariants/TargetFunctions.sol b/packages/contracts/contracts/TestContracts/invariants/TargetFunctions.sol
@@ -316,6 +316,8 @@ abstract contract TargetFunctions is Properties {
                 L_01
             );
 
+            eq(vars.sortedCdpsSizeAfter, vars.sortedCdpsSizeBefore, "L-17 : Partial Liquidations do not close Cdps");
+
             // https://github.com/Badger-Finance/ebtc-fuzz-review/issues/4
             if (vars.sortedCdpsSizeAfter == vars.sortedCdpsSizeBefore) {
                 // CDP was not fully liquidated
@@ -1245,8 +1247,14 @@ abstract contract TargetFunctions is Properties {
         } else if (parameter == 1) {
             value = between(value, 0, activePool.getFeeRecipientClaimableCollShares());
             hevm.prank(defaultGovernance);
+            _before(bytes32(0));
             activePool.claimFeeRecipientCollShares(value);
-            eq(vars.feeRecipientCollSharesAfter + value, vars.feeRecipientCollSharesBefore, F_01);
+            _after(bytes32(0));
+            // If there was something to claim
+            if(value > 0) {
+                // Claiming will increase the balance
+                gte(vars.feeRecipientCollSharesAfter, vars.feeRecipientCollSharesBefore, F_01);
+            }
         } else if (parameter == 2) {
             value = between(value, 0, cdpManager.MAX_REWARD_SPLIT());
             hevm.prank(defaultGovernance);

diff --git a/packages/contracts/foundry_test/EchidnaToFoundry.t.sol b/packages/contracts/foundry_test/EchidnaToFoundry.t.sol
@@ -216,6 +216,16 @@ contract EToFoundry is
         );
     }
 
+    function testPartialLiquidationCanCloseCDPS() public {
+        openCdp(67534042799335353648407647554112468697195277953615236438520200454730440793371, 8);
+        openCdp(115792089237316195423570985008687907853269984665640564039457584007913129639931, 1000000000000000900);
+        setEthPerShare(48542174391735010270995007834653745032392815149632706327135797120960854131722);
+        setEthPerShare(40);
+        console2.log("cdpManager.getActiveCdpsCount()", cdpManager.getActiveCdpsCount());
+        partialLiquidate(10055443073786697780288631944863873711310414440862685961782620523444705292193, 0);
+        console2.log("cdpManager.getActiveCdpsCount()", cdpManager.getActiveCdpsCount());
+    }
+
     function testBrokenImprovementofNICR() public {
         bytes32 cdpId = openCdp(36, 1);
         setEthPerShare(

diff --git a/packages/contracts/specs/PROPERTIES.md b/packages/contracts/specs/PROPERTIES.md
@@ -142,6 +142,8 @@ Recon Attack IMO - And scrap here
 | L-14 | If the RM grace period is set and we're in recovery mode, new actions that keep the system in recovery mode should not change the cooldown timestamp | High Level | ✅ |
 | L-15 | The RM grace period should set if a BO/liquidation/redistribution makes the TCR above CCR | High Level | ✅ |
 | L-16 | The RM grace period should reset if a BO/liquidation/redistribution makes the TCR below CCR | High Level | ✅ |
+| L-17 | Partial Liquidations do not close Cdps | High Level | TO TEST |
+
 
 ## Fees - Antonio pls implement this one first