Adding CDP stake related invariants

packages/contracts/contracts/CRLens.sol

@@ -75,6 +75,16 @@ contract CRLens {
         return icr;
     }
 
+    function getRealStake(bytes32 cdpId) external returns (uint256) {
+        cdpManager.syncAccounting(cdpId);
+        uint256 collShares = cdpManager.getCdpCollShares(cdpId);
+        return
+            cdpManager.totalCollateralSnapshot() == 0
+                ? collShares
+                : (collShares * cdpManager.totalStakesSnapshot()) /
+                    cdpManager.totalCollateralSnapshot();
+    }
+
     /// @dev Returns 1 if we're in RM
     function getCheckRecoveryMode(bool revertValue) external returns (uint256) {
         // Synch State

packages/contracts/contracts/Interfaces/ICdpManagerData.sol

@@ -265,4 +265,8 @@ interface ICdpManagerData is IRecoveryModeGracePeriod {
     ) external view returns (uint256 debt, uint256 collShares);
 
     function canLiquidateRecoveryMode(uint256 icr, uint256 tcr) external view returns (bool);
+
+    function totalCollateralSnapshot() external view returns (uint256);
+
+    function totalStakesSnapshot() external view returns (uint256);
 }

packages/contracts/contracts/TestContracts/invariants/BeforeAfter.sol

@@ -34,6 +34,8 @@ abstract contract BeforeAfter is BaseStorageVariables {
         uint256 cdpCollAfter;
         uint256 cdpDebtBefore;
         uint256 cdpDebtAfter;
+        uint256 cdpStakeBefore;
+        uint256 cdpStakeAfter;
         uint256 liquidatorRewardSharesBefore;
         uint256 liquidatorRewardSharesAfter;
         uint256 sortedCdpsSizeBefore;
@@ -71,6 +73,12 @@ abstract contract BeforeAfter is BaseStorageVariables {
         uint256 cumulativeCdpsAtTimeOfRebase;
         uint256 prevStEthFeeIndex;
         uint256 afterStEthFeeIndex;
+        uint256 totalStakesBefore;
+        uint256 totalStakesAfter;
+        uint256 totalStakesSnapshotBefore;
+        uint256 totalStakesSnapshotAfter;
+        uint256 totalCollateralSnapshotBefore;
+        uint256 totalCollateralSnapshotAfter;
     }
 
     Vars vars;
@@ -82,14 +90,15 @@ abstract contract BeforeAfter is BaseStorageVariables {
     function _before(bytes32 _cdpId) internal {
         vars.priceBefore = priceFeedMock.fetchPrice();
 
-        (uint256 debtBefore, ) = cdpManager.getSyncedDebtAndCollShares(_cdpId);
+        (uint256 debtBefore, uint256 collBefore) = cdpManager.getSyncedDebtAndCollShares(_cdpId);
 
         vars.nicrBefore = _cdpId != bytes32(0) ? crLens.quoteRealNICR(_cdpId) : 0;
         vars.icrBefore = _cdpId != bytes32(0)
             ? cdpManager.getCachedICR(_cdpId, vars.priceBefore)
             : 0;
-        vars.cdpCollBefore = _cdpId != bytes32(0) ? cdpManager.getCdpCollShares(_cdpId) : 0;
+        vars.cdpCollBefore = _cdpId != bytes32(0) ? collBefore : 0;
         vars.cdpDebtBefore = _cdpId != bytes32(0) ? debtBefore : 0;
+        vars.cdpStakeBefore = _cdpId != bytes32(0) ? crLens.getRealStake(_cdpId) : 0;
         vars.liquidatorRewardSharesBefore = _cdpId != bytes32(0)
             ? cdpManager.getCdpLiquidatorRewardShares(_cdpId)
             : 0;
@@ -137,15 +146,22 @@ abstract contract BeforeAfter is BaseStorageVariables {
                 1e18 -
                 vars.activePoolDebtBefore;
         vars.prevStEthFeeIndex = cdpManager.systemStEthFeePerUnitIndex();
+
+        vars.totalStakesBefore = cdpManager.totalStakes();
+        vars.totalStakesSnapshotBefore = cdpManager.totalStakesSnapshot();
+        vars.totalCollateralSnapshotBefore = cdpManager.totalCollateralSnapshot();
     }
 
     function _after(bytes32 _cdpId) internal {
         vars.priceAfter = priceFeedMock.fetchPrice();
 
+        (, uint256 collAfter) = cdpManager.getSyncedDebtAndCollShares(_cdpId);
+
         vars.nicrAfter = _cdpId != bytes32(0) ? crLens.quoteRealNICR(_cdpId) : 0;
         vars.icrAfter = _cdpId != bytes32(0) ? cdpManager.getCachedICR(_cdpId, vars.priceAfter) : 0;
-        vars.cdpCollAfter = _cdpId != bytes32(0) ? cdpManager.getCdpCollShares(_cdpId) : 0;
+        vars.cdpCollAfter = _cdpId != bytes32(0) ? collAfter : 0;
         vars.cdpDebtAfter = _cdpId != bytes32(0) ? cdpManager.getCdpDebt(_cdpId) : 0;
+        vars.cdpStakeAfter = _cdpId != bytes32(0) ? crLens.getRealStake(_cdpId) : 0;
         vars.liquidatorRewardSharesAfter = _cdpId != bytes32(0)
             ? cdpManager.getCdpLiquidatorRewardShares(_cdpId)
             : 0;
@@ -200,6 +216,10 @@ abstract contract BeforeAfter is BaseStorageVariables {
         if (vars.afterStEthFeeIndex > vars.prevStEthFeeIndex) {
             vars.cumulativeCdpsAtTimeOfRebase += cdpManager.getActiveCdpsCount();
         }
+
+        vars.totalStakesAfter = cdpManager.totalStakes();
+        vars.totalStakesSnapshotAfter = cdpManager.totalStakesSnapshot();
+        vars.totalCollateralSnapshotAfter = cdpManager.totalCollateralSnapshot();
     }
 
     function _diff() internal view returns (string memory log) {

packages/contracts/contracts/TestContracts/invariants/Properties.sol

@@ -117,6 +117,35 @@ abstract contract Properties is BeforeAfter, PropertiesDescriptions, Asserts, Pr
             isApproximateEq(vars.valueInSystemAfter, vars.valueInSystemBefore, 0.01e18);
     }
 
+    function invariant_CDPM_10(CdpManager cdpManager) internal view returns (bool) {
+        if (vars.afterStEthFeeIndex > vars.prevStEthFeeIndex) {
+            return cdpManager.totalStakesSnapshot() == cdpManager.totalStakes();
+        }
+        return true;
+    }
+
+    function invariant_CDPM_11(CdpManager cdpManager) internal view returns (bool) {
+        if (vars.afterStEthFeeIndex > vars.prevStEthFeeIndex) {
+            return cdpManager.totalCollateralSnapshot() == cdpManager.getSystemCollShares();
+        }
+        return true;
+    }
+
+    function invariant_CDPM_12(
+        SortedCdps sortedCdps,
+        Vars memory vars
+    ) internal view returns (bool) {
+        bytes32 currentCdp = sortedCdps.getFirst();
+
+        uint256 sumStakes;
+        while (currentCdp != bytes32(0)) {
+            sumStakes += cdpManager.getCdpStake(currentCdp);
+            currentCdp = sortedCdps.getNext(currentCdp);
+        }
+
+        return sumStakes == vars.totalStakesAfter;
+    }
+
     function invariant_CSP_01(
         ICollateralToken collateral,
         CollSurplusPool collSurplusPool

packages/contracts/contracts/TestContracts/invariants/PropertiesDescriptions.sol

@@ -28,6 +28,16 @@ abstract contract PropertiesDescriptions {
     string constant CDPM_04 = "CDPM-04: The total system value does not decrease during redemptions";
     string constant CDPM_05 = "CDPM-05: Redemptions do not increase the total system debt";
     string constant CDPM_06 = "CDPM-06: Redemptions do not increase the total system debt";
+    string constant CDPM_07 = "CDPM-07: Stake decreases when collShares decreases for a CDP";
+    string constant CDPM_08 = "CDPM-08: Stake increases when collShares increases for a CDP";
+    string constant CDPM_09 =
+        "CDPM-09: expectedStake = coll * totalStakesSnapshot / totalCollateralSnapshot after every operation involving a CDP";
+    string constant CDPM_10 =
+        "CDPM-10: totalStakesSnapshot matches totalStakes after an operation, if rebase index changed during the OP";
+    string constant CDPM_11 =
+        "CDPM-11: totalCollateralSnapshot matches activePool.systemCollShares after an operation, if rebase index changed during the OP";
+    string constant CDPM_12 =
+        "CDPM-12: Sum of all individual CDP stakes should equal to totalStakes";
 
     ///////////////////////////////////////////////////////
     // Collateral Surplus Pool

packages/contracts/contracts/TestContracts/invariants/TargetFunctions.sol

@@ -280,6 +280,8 @@ abstract contract TargetFunctions is Properties {
                 lt(cdpManager.lastEBTCDebtErrorRedistribution(), cdpManager.totalStakes(), L_17);
                 totalCdpDustMaxCap += cdpManager.getActiveCdpsCount();
             }
+
+            _checkStakeInvariants();
         } else if (vars.sortedCdpsSizeBefore > _i) {
             assertRevertReasonNotEqual(returnData, "Panic(17)");
         }
@@ -372,6 +374,27 @@ abstract contract TargetFunctions is Properties {
         }
     }
 
+    function _checkStakeInvariants() private {
+        if (vars.cdpCollAfter < vars.cdpCollBefore) {
+            lt(vars.cdpStakeAfter, vars.cdpStakeBefore, CDPM_07);
+        }
+
+        if (vars.cdpCollAfter > vars.cdpCollBefore) {
+            gt(vars.cdpStakeAfter, vars.cdpStakeBefore, CDPM_08);
+        }
+
+        if (vars.totalCollateralSnapshotAfter > 0) {
+            eq(
+                vars.cdpStakeAfter,
+                (vars.cdpCollAfter * vars.totalStakesSnapshotAfter) /
+                    vars.totalCollateralSnapshotAfter,
+                CDPM_09
+            );
+        } else {
+            eq(vars.cdpStakeAfter, vars.cdpCollAfter, CDPM_09);
+        }
+    }
+
     /** Active Pool TWAP Revert Checks */
     function observe() public {
         // We verify that any observation will never revert
@@ -463,6 +486,8 @@ abstract contract TargetFunctions is Properties {
                 lt(cdpManager.lastEBTCDebtErrorRedistribution(), cdpManager.totalStakes(), L_17);
                 totalCdpDustMaxCap += cdpManager.getActiveCdpsCount();
             }
+
+            _checkStakeInvariants();
         } else if (vars.sortedCdpsSizeBefore > _n) {
             if (_atLeastOneCdpIsLiquidatable(cdpsBefore, vars.isRecoveryModeBefore)) {
                 assertRevertReasonNotEqual(returnData, "Panic(17)");
@@ -482,6 +507,7 @@ abstract contract TargetFunctions is Properties {
             _partialRedemptionHintNICR,
             false,
             false,
+            false,
             _maxFeePercentage,
             _maxIterations
         );
@@ -493,6 +519,7 @@ abstract contract TargetFunctions is Properties {
         uint256 _partialRedemptionHintNICRFromMedusa,
         bool useProperFirstHint,
         bool useProperPartialHint,
+        bool failPartialRedemption,
         uint _maxFeePercentage,
         uint _maxIterations
     ) public setup {
@@ -502,6 +529,7 @@ abstract contract TargetFunctions is Properties {
             _partialRedemptionHintNICRFromMedusa,
             useProperFirstHint,
             useProperPartialHint,
+            failPartialRedemption,
             _maxFeePercentage,
             _maxIterations
         );
@@ -513,9 +541,12 @@ abstract contract TargetFunctions is Properties {
         uint256 _partialRedemptionHintNICRFromMedusa,
         bool useProperFirstHint,
         bool useProperPartialHint,
+        bool failPartialRedemption,
         uint _maxFeePercentage,
         uint _maxIterations
     ) internal {
+        require(cdpManager.getActiveCdpsCount() > 1, "Cannot redeem last CDP");
+
         _EBTCAmount = between(_EBTCAmount, 0, eBTCToken.balanceOf(address(actor)));
 
         _maxIterations = between(_maxIterations, 0, 10);
@@ -558,7 +589,7 @@ abstract contract TargetFunctions is Properties {
                     _firstRedemptionHintFromMedusa,
                     bytes32(0),
                     bytes32(0),
-                    _partialRedemptionHintNICRFromMedusa,
+                    failPartialRedemption ? 0 : _partialRedemptionHintNICRFromMedusa,
                     _maxIterations,
                     _maxFeePercentage
                 )
@@ -604,6 +635,8 @@ abstract contract TargetFunctions is Properties {
         if (vars.isRecoveryModeBefore && !vars.isRecoveryModeAfter) {
             t(!vars.lastGracePeriodStartTimestampIsSetAfter, L_16);
         }
+
+        _checkStakeInvariants();
     }
 
     ///////////////////////////////////////////////////////
@@ -661,6 +694,8 @@ abstract contract TargetFunctions is Properties {
         if (vars.isRecoveryModeBefore && !vars.isRecoveryModeAfter) {
             t(!vars.lastGracePeriodStartTimestampIsSetAfter, L_16);
         }
+
+        _checkStakeInvariants();
     }
 
     ///////////////////////////////////////////////////////
@@ -715,6 +750,8 @@ abstract contract TargetFunctions is Properties {
         if (vars.isRecoveryModeBefore && !vars.isRecoveryModeAfter) {
             t(!vars.lastGracePeriodStartTimestampIsSetAfter, L_16);
         }
+
+        _checkStakeInvariants();
     }
 
     function openCdp(uint256 _col, uint256 _EBTCAmount) public setup returns (bytes32 _cdpId) {
@@ -798,6 +835,8 @@ abstract contract TargetFunctions is Properties {
             gte(_EBTCAmount, borrowerOperations.MIN_CHANGE(), GENERAL_16);
             gte(vars.cdpDebtAfter, borrowerOperations.MIN_CHANGE(), GENERAL_15);
             require(invariant_BO_09(cdpManager, priceFeedMock.getPrice(), _cdpId), BO_09);
+
+            _checkStakeInvariants();
         } else {
             assertRevertReasonNotEqual(returnData, "Panic(17)"); /// Done
         }
@@ -898,6 +937,8 @@ abstract contract TargetFunctions is Properties {
             }
 
             gte(_coll, borrowerOperations.MIN_CHANGE(), GENERAL_16);
+
+            _checkStakeInvariants();
         } else {
             assertRevertReasonNotEqual(returnData, "Panic(17)");
         }
@@ -968,6 +1009,8 @@ abstract contract TargetFunctions is Properties {
             }
 
             gte(_amount, borrowerOperations.MIN_CHANGE(), GENERAL_16);
+
+            _checkStakeInvariants();
         } else {
             assertRevertReasonNotEqual(returnData, "Panic(17)");
         }
@@ -1040,6 +1083,8 @@ abstract contract TargetFunctions is Properties {
 
             gte(_amount, borrowerOperations.MIN_CHANGE(), GENERAL_16);
             gte(vars.cdpDebtAfter, borrowerOperations.MIN_CHANGE(), GENERAL_15);
+
+            _checkStakeInvariants();
         } else {
             assertRevertReasonNotEqual(returnData, "Panic(17)");
         }
@@ -1112,6 +1157,8 @@ abstract contract TargetFunctions is Properties {
 
             gte(_amount, borrowerOperations.MIN_CHANGE(), GENERAL_16);
             gte(vars.cdpDebtAfter, borrowerOperations.MIN_CHANGE(), GENERAL_15);
+
+            _checkStakeInvariants();
         } else {
             assertRevertReasonNotEqual(returnData, "Panic(17)");
         }
@@ -1188,6 +1235,8 @@ abstract contract TargetFunctions is Properties {
             if (vars.isRecoveryModeBefore && !vars.isRecoveryModeAfter) {
                 t(!vars.lastGracePeriodStartTimestampIsSetAfter, L_16);
             }
+
+            _checkStakeInvariants();
         } else {
             assertRevertReasonNotEqual(returnData, "Panic(17)");
         }
@@ -1275,6 +1324,8 @@ abstract contract TargetFunctions is Properties {
             }
         }
         gte(vars.cdpDebtAfter, borrowerOperations.MIN_CHANGE(), GENERAL_15);
+
+        _checkStakeInvariants();
     }
 
     ///////////////////////////////////////////////////////

packages/contracts/contracts/TestContracts/invariants/echidna/EchidnaProperties.sol

@@ -40,6 +40,18 @@ abstract contract EchidnaProperties is TargetContractSetup, Properties {
         return invariant_CDPM_03(cdpManager);
     }
 
+    function echidna_cdp_manager_invariant_10() public returns (bool) {
+        return invariant_CDPM_10(cdpManager);
+    }
+
+    function echidna_cdp_manager_invariant_11() public returns (bool) {
+        return invariant_CDPM_11(cdpManager);
+    }
+
+    function echidna_cdp_manager_invariant_12() public returns (bool) {
+        return invariant_CDPM_12(sortedCdps, vars);
+    }
+
     // CDPM_04 is a vars invariant
 
     function echidna_coll_surplus_pool_invariant_1() public returns (bool) {

packages/contracts/foundry.toml

@@ -6,6 +6,7 @@ test = 'foundry_test'
 cache_path  = 'forge-cache'
 gas_reports = ["*"]
 no_match_contract = 'Echidna'
+solc_version= '0.8.17'
 
 evm_version = 'london'
 

packages/contracts/remappings.txt

@@ -1,4 +1,4 @@
 ds-test/=lib/forge-std/lib/ds-test/src/
 forge-std/=lib/forge-std/src/
 @crytic/properties/=node_modules/@crytic/properties/
-@openzeppelin/=node_modules/@openzeppelin/
+@openzeppelin/=node_modules/@openzeppelin/