Merge pull request #785 from ebtc-protocol/feat-surplus-invariant

Feat surplus invariant
ebtc-protocol · Mar 8, 2024 · ef4f90d · ef4f90d
2 parents ecdb55d + 2b46535
commit ef4f90d
Show file tree

Hide file tree

Showing 3 changed files with 40 additions and 2 deletions.
diff --git a/packages/contracts/contracts/TestContracts/invariants/BeforeAfter.sol b/packages/contracts/contracts/TestContracts/invariants/BeforeAfter.sol
@@ -10,6 +10,8 @@ abstract contract BeforeAfter is BaseStorageVariables {
     using Pretty for bool;
 
     struct Vars {
+        uint256 userSurplusBefore;
+        uint256 userSurplusAfter;
         uint256 valueInSystemBefore;
         uint256 valueInSystemAfter;
         uint256 nicrBefore;
@@ -82,6 +84,9 @@ abstract contract BeforeAfter is BaseStorageVariables {
     function _before(bytes32 _cdpId) internal {
         vars.priceBefore = priceFeedMock.fetchPrice();
 
+        address ownerToCheck = sortedCdps.getOwnerAddress(_cdpId);
+        vars.userSurplusBefore = collSurplusPool.getSurplusCollShares(ownerToCheck);
+
         (uint256 debtBefore, ) = cdpManager.getSyncedDebtAndCollShares(_cdpId);
 
         vars.nicrBefore = _cdpId != bytes32(0) ? crLens.quoteRealNICR(_cdpId) : 0;
@@ -140,6 +145,9 @@ abstract contract BeforeAfter is BaseStorageVariables {
     }
 
     function _after(bytes32 _cdpId) internal {
+        address ownerToCheck = sortedCdps.getOwnerAddress(_cdpId);
+        vars.userSurplusAfter = collSurplusPool.getSurplusCollShares(ownerToCheck);
+
         vars.priceAfter = priceFeedMock.fetchPrice();
 
         vars.nicrAfter = _cdpId != bytes32(0) ? crLens.quoteRealNICR(_cdpId) : 0;

diff --git a/packages/contracts/contracts/TestContracts/invariants/TargetFunctions.sol b/packages/contracts/contracts/TestContracts/invariants/TargetFunctions.sol
@@ -226,6 +226,7 @@ abstract contract TargetFunctions is Properties {
         _before(_cdpId);
 
         uint256 _icrToLiq = cdpManager.getSyncedICR(_cdpId, priceFeedMock.getPrice());
+
         (success, returnData) = actor.proxy(
             address(cdpManager),
             abi.encodeWithSelector(CdpManager.liquidate.selector, _cdpId)
@@ -234,6 +235,12 @@ abstract contract TargetFunctions is Properties {
         _after(_cdpId);
 
         if (success) {
+            // SURPLUS-CHECK-1 | The surplus is capped at 4 wei | NOTE: Proxy of growth, storage var would further refine
+            if (_icrToLiq <= cdpManager.MCR()) {
+                gte(vars.collSurplusPoolBefore + 4, vars.collSurplusPoolAfter, "SURPLUS-CHECK-1");
+                gte(vars.userSurplusBefore + 4, vars.userSurplusAfter, "SURPLUS-CHECK-2");
+            }
+
             // if ICR >= TCR then we ignore
             // We could check that Liquidated is not above TCR
             if (
@@ -421,6 +428,9 @@ abstract contract TargetFunctions is Properties {
         _after(bytes32(0));
 
         if (success) {
+            // SURPLUS-CHECK-1 | The surplus is capped at 4 wei | NOTE: We use Liquidate for the exact CDP check
+            gte(vars.collSurplusPoolBefore + 4, vars.collSurplusPoolAfter, "SURPLUS-CHECK-1");
+
             Cdp[] memory cdpsAfter = _getCdpIdsAndICRs();
 
             Cdp[] memory cdpsLiquidated = _cdpIdsAndICRsDiff(cdpsBefore, cdpsAfter);

diff --git a/packages/contracts/foundry_test/EchidnaToFoundry.t.sol b/packages/contracts/foundry_test/EchidnaToFoundry.t.sol
@@ -25,13 +25,16 @@ contract EToFoundry is
 {
     modifier setup() override {
         _;
+        address sender = uint160(msg.sender) % 3 == 0 ? address(USER1) : uint160(msg.sender) % 3 == 1
+            ? address(USER2)
+            : address(USER3);
+        actor = actors[sender];
     }
 
     function setUp() public {
         _setUp();
         _setUpActors();
-        actor = actors[USER1];
-        vm.startPrank(address(actor));
+        actor = actors[address(USER1)];
     }
 
     function _checkTotals() internal {
@@ -221,9 +224,17 @@ contract EToFoundry is
     function _logStakes() internal {
         bytes32 currentCdp = sortedCdps.getFirst();
 
+        console2.log("=== LogStakes ===");
+
+        uint256 currentPrice = priceFeedMock.fetchPrice();
+        uint256 currentPricePerShare = collateral.getPooledEthByShares(1 ether);
+        console2.log("currentPrice", currentPrice);
+        console2.log("currentPricePerShare", currentPricePerShare);
+
         while (currentCdp != bytes32(0)) {
             emit DebugBytes32(currentCdp);
             console2.log("CdpId", vm.toString(currentCdp));
+            console2.log("===============================");
             console2.log("cdpManager.getCdpStake(currentCdp)", cdpManager.getCdpStake(currentCdp));
             console2.log(
                 "cdpManager.getSyncedCdpCollShares(currentCdp)",
@@ -239,7 +250,16 @@ contract EToFoundry is
                 "cdpManager.getSyncedNominalICR(currentCdp)",
                 cdpManager.getSyncedNominalICR(currentCdp)
             );
+            console2.log(
+                "cdpManager.getCachedICR(currentCdp, currentPrice)",
+                cdpManager.getCachedICR(currentCdp, currentPrice)
+            );
+            console2.log(
+                "cdpManager.getSyncedICR(currentCdp, currentPrice)",
+                cdpManager.getSyncedICR(currentCdp, currentPrice)
+            );
             currentCdp = sortedCdps.getNext(currentCdp);
+            console2.log("");
         }
 
         console2.log(