From 436170849af68bb5c68dff403e87704d8cf57072 Mon Sep 17 00:00:00 2001
From: wtj2021 <wtj2022@proton.me>
Date: Wed, 6 Mar 2024 14:58:47 -0800
Subject: [PATCH 01/11] Adding CDP stake related invariants

---
 .../TestContracts/invariants/BeforeAfter.sol  | 18 ++++++
 .../TestContracts/invariants/Properties.sol   | 55 +++++++++++++++++++
 .../invariants/PropertiesDescriptions.sol     | 10 ++++
 .../invariants/TargetFunctions.sol            | 40 +++++++++++++-
 .../invariants/echidna/EchidnaProperties.sol  | 20 +++++++
 5 files changed, 142 insertions(+), 1 deletion(-)

diff --git a/packages/contracts/contracts/TestContracts/invariants/BeforeAfter.sol b/packages/contracts/contracts/TestContracts/invariants/BeforeAfter.sol
index 6af6937fd..799e2b2d8 100644
--- a/packages/contracts/contracts/TestContracts/invariants/BeforeAfter.sol
+++ b/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;
@@ -90,6 +98,7 @@ abstract contract BeforeAfter is BaseStorageVariables {
             : 0;
         vars.cdpCollBefore = _cdpId != bytes32(0) ? cdpManager.getCdpCollShares(_cdpId) : 0;
         vars.cdpDebtBefore = _cdpId != bytes32(0) ? debtBefore : 0;
+        vars.cdpStakeBefore = _cdpId != bytes32(0) ? cdpManager.getCdpStake(_cdpId) : 0;
         vars.liquidatorRewardSharesBefore = _cdpId != bytes32(0)
             ? cdpManager.getCdpLiquidatorRewardShares(_cdpId)
             : 0;
@@ -137,6 +146,10 @@ 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 {
@@ -146,6 +159,7 @@ abstract contract BeforeAfter is BaseStorageVariables {
         vars.icrAfter = _cdpId != bytes32(0) ? cdpManager.getCachedICR(_cdpId, vars.priceAfter) : 0;
         vars.cdpCollAfter = _cdpId != bytes32(0) ? cdpManager.getCdpCollShares(_cdpId) : 0;
         vars.cdpDebtAfter = _cdpId != bytes32(0) ? cdpManager.getCdpDebt(_cdpId) : 0;
+        vars.cdpStakeAfter = _cdpId != bytes32(0) ? cdpManager.getCdpStake(_cdpId) : 0;
         vars.liquidatorRewardSharesAfter = _cdpId != bytes32(0)
             ? cdpManager.getCdpLiquidatorRewardShares(_cdpId)
             : 0;
@@ -200,6 +214,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) {
diff --git a/packages/contracts/contracts/TestContracts/invariants/Properties.sol b/packages/contracts/contracts/TestContracts/invariants/Properties.sol
index ef70400dd..8051db9ac 100644
--- a/packages/contracts/contracts/TestContracts/invariants/Properties.sol
+++ b/packages/contracts/contracts/TestContracts/invariants/Properties.sol
@@ -117,6 +117,61 @@ abstract contract Properties is BeforeAfter, PropertiesDescriptions, Asserts, Pr
             isApproximateEq(vars.valueInSystemAfter, vars.valueInSystemBefore, 0.01e18);
     }
 
+    function invariant_CDPM_07(Vars memory vars) internal view returns (bool) {
+        if (vars.cdpCollAfter < vars.cdpCollBefore) {
+            return vars.cdpStakeAfter < vars.cdpStakeBefore;
+        }
+        return true;
+    }
+
+    function invariant_CDPM_08(Vars memory vars) internal view returns (bool) {
+        if (vars.cdpCollAfter > vars.cdpCollBefore) {
+            return vars.cdpStakeAfter > vars.cdpStakeBefore;
+        }
+        return true;
+    }
+
+    function invariant_CDPM_09(Vars memory vars) internal view returns (bool) {
+        return
+            vars.cdpStakeAfter ==
+            (vars.cdpCollAfter * vars.totalStakesSnapshotAfter) / vars.totalCollateralSnapshotAfter;
+    }
+
+    function invariant_CDPM_10(
+        CdpManager cdpManager,
+        Vars memory vars
+    ) internal view returns (bool) {
+        if (vars.afterStEthFeeIndex > vars.prevStEthFeeIndex) {
+            return cdpManager.totalStakesSnapshot() == vars.totalStakesAfter;
+        }
+        return true;
+    }
+
+    function invariant_CDPM_11(
+        CdpManager cdpManager,
+        Vars memory vars
+    ) internal view returns (bool) {
+        if (vars.afterStEthFeeIndex > vars.prevStEthFeeIndex) {
+            return cdpManager.totalCollateralSnapshot() == vars.totalCollateralSnapshotAfter;
+        }
+        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
diff --git a/packages/contracts/contracts/TestContracts/invariants/PropertiesDescriptions.sol b/packages/contracts/contracts/TestContracts/invariants/PropertiesDescriptions.sol
index d3bb4e1a0..f53564af6 100644
--- a/packages/contracts/contracts/TestContracts/invariants/PropertiesDescriptions.sol
+++ b/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
diff --git a/packages/contracts/contracts/TestContracts/invariants/TargetFunctions.sol b/packages/contracts/contracts/TestContracts/invariants/TargetFunctions.sol
index 8627b013e..a28ace9dd 100644
--- a/packages/contracts/contracts/TestContracts/invariants/TargetFunctions.sol
+++ b/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();
             }
+
+            _check_CDPM_09();
         } else if (vars.sortedCdpsSizeBefore > _i) {
             assertRevertReasonNotEqual(returnData, "Panic(17)");
         }
@@ -367,11 +369,21 @@ abstract contract TargetFunctions is Properties {
 
             gte(_partialAmount, borrowerOperations.MIN_CHANGE(), GENERAL_16);
             gte(vars.cdpDebtAfter, borrowerOperations.MIN_CHANGE(), GENERAL_15);
+
+            _check_CDPM_09();
         } else {
             assertRevertReasonNotEqual(returnData, "Panic(17)");
         }
     }
 
+    function _check_CDPM_09() private {
+        eq(
+            vars.cdpStakeAfter,
+            (vars.cdpCollAfter * vars.totalStakesSnapshotAfter) / vars.totalCollateralSnapshotAfter,
+            CDPM_09
+        );
+    }
+
     /** Active Pool TWAP Revert Checks */
     function observe() public {
         // We verify that any observation will never revert
@@ -463,6 +475,8 @@ abstract contract TargetFunctions is Properties {
                 lt(cdpManager.lastEBTCDebtErrorRedistribution(), cdpManager.totalStakes(), L_17);
                 totalCdpDustMaxCap += cdpManager.getActiveCdpsCount();
             }
+
+            _check_CDPM_09();
         } else if (vars.sortedCdpsSizeBefore > _n) {
             if (_atLeastOneCdpIsLiquidatable(cdpsBefore, vars.isRecoveryModeBefore)) {
                 assertRevertReasonNotEqual(returnData, "Panic(17)");
@@ -482,6 +496,7 @@ abstract contract TargetFunctions is Properties {
             _partialRedemptionHintNICR,
             false,
             false,
+            false,
             _maxFeePercentage,
             _maxIterations
         );
@@ -493,6 +508,7 @@ abstract contract TargetFunctions is Properties {
         uint256 _partialRedemptionHintNICRFromMedusa,
         bool useProperFirstHint,
         bool useProperPartialHint,
+        bool failPartialRedemption,
         uint _maxFeePercentage,
         uint _maxIterations
     ) public setup {
@@ -502,6 +518,7 @@ abstract contract TargetFunctions is Properties {
             _partialRedemptionHintNICRFromMedusa,
             useProperFirstHint,
             useProperPartialHint,
+            failPartialRedemption,
             _maxFeePercentage,
             _maxIterations
         );
@@ -513,6 +530,7 @@ abstract contract TargetFunctions is Properties {
         uint256 _partialRedemptionHintNICRFromMedusa,
         bool useProperFirstHint,
         bool useProperPartialHint,
+        bool failPartialRedemption,
         uint _maxFeePercentage,
         uint _maxIterations
     ) internal {
@@ -558,7 +576,7 @@ abstract contract TargetFunctions is Properties {
                     _firstRedemptionHintFromMedusa,
                     bytes32(0),
                     bytes32(0),
-                    _partialRedemptionHintNICRFromMedusa,
+                    failPartialRedemption ? 0 : _partialRedemptionHintNICRFromMedusa,
                     _maxIterations,
                     _maxFeePercentage
                 )
@@ -604,6 +622,8 @@ abstract contract TargetFunctions is Properties {
         if (vars.isRecoveryModeBefore && !vars.isRecoveryModeAfter) {
             t(!vars.lastGracePeriodStartTimestampIsSetAfter, L_16);
         }
+
+        _check_CDPM_09();
     }
 
     ///////////////////////////////////////////////////////
@@ -661,6 +681,8 @@ abstract contract TargetFunctions is Properties {
         if (vars.isRecoveryModeBefore && !vars.isRecoveryModeAfter) {
             t(!vars.lastGracePeriodStartTimestampIsSetAfter, L_16);
         }
+
+        _check_CDPM_09();
     }
 
     ///////////////////////////////////////////////////////
@@ -715,6 +737,8 @@ abstract contract TargetFunctions is Properties {
         if (vars.isRecoveryModeBefore && !vars.isRecoveryModeAfter) {
             t(!vars.lastGracePeriodStartTimestampIsSetAfter, L_16);
         }
+
+        _check_CDPM_09();
     }
 
     function openCdp(uint256 _col, uint256 _EBTCAmount) public setup returns (bytes32 _cdpId) {
@@ -798,6 +822,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);
+
+            _check_CDPM_09();
         } else {
             assertRevertReasonNotEqual(returnData, "Panic(17)"); /// Done
         }
@@ -898,6 +924,8 @@ abstract contract TargetFunctions is Properties {
             }
 
             gte(_coll, borrowerOperations.MIN_CHANGE(), GENERAL_16);
+
+            _check_CDPM_09();
         } else {
             assertRevertReasonNotEqual(returnData, "Panic(17)");
         }
@@ -968,6 +996,8 @@ abstract contract TargetFunctions is Properties {
             }
 
             gte(_amount, borrowerOperations.MIN_CHANGE(), GENERAL_16);
+
+            _check_CDPM_09();
         } else {
             assertRevertReasonNotEqual(returnData, "Panic(17)");
         }
@@ -1040,6 +1070,8 @@ abstract contract TargetFunctions is Properties {
 
             gte(_amount, borrowerOperations.MIN_CHANGE(), GENERAL_16);
             gte(vars.cdpDebtAfter, borrowerOperations.MIN_CHANGE(), GENERAL_15);
+
+            _check_CDPM_09();
         } else {
             assertRevertReasonNotEqual(returnData, "Panic(17)");
         }
@@ -1112,6 +1144,8 @@ abstract contract TargetFunctions is Properties {
 
             gte(_amount, borrowerOperations.MIN_CHANGE(), GENERAL_16);
             gte(vars.cdpDebtAfter, borrowerOperations.MIN_CHANGE(), GENERAL_15);
+
+            _check_CDPM_09();
         } else {
             assertRevertReasonNotEqual(returnData, "Panic(17)");
         }
@@ -1188,6 +1222,8 @@ abstract contract TargetFunctions is Properties {
             if (vars.isRecoveryModeBefore && !vars.isRecoveryModeAfter) {
                 t(!vars.lastGracePeriodStartTimestampIsSetAfter, L_16);
             }
+
+            _check_CDPM_09();
         } else {
             assertRevertReasonNotEqual(returnData, "Panic(17)");
         }
@@ -1275,6 +1311,8 @@ abstract contract TargetFunctions is Properties {
             }
         }
         gte(vars.cdpDebtAfter, borrowerOperations.MIN_CHANGE(), GENERAL_15);
+
+        _check_CDPM_09();
     }
 
     ///////////////////////////////////////////////////////
diff --git a/packages/contracts/contracts/TestContracts/invariants/echidna/EchidnaProperties.sol b/packages/contracts/contracts/TestContracts/invariants/echidna/EchidnaProperties.sol
index a8b0de4c1..7c65d6dba 100644
--- a/packages/contracts/contracts/TestContracts/invariants/echidna/EchidnaProperties.sol
+++ b/packages/contracts/contracts/TestContracts/invariants/echidna/EchidnaProperties.sol
@@ -40,6 +40,26 @@ abstract contract EchidnaProperties is TargetContractSetup, Properties {
         return invariant_CDPM_03(cdpManager);
     }
 
+    function echidna_cdp_manager_invariant_7() public returns (bool) {
+        return invariant_CDPM_07(vars);
+    }
+
+    function echidna_cdp_manager_invariant_8() public returns (bool) {
+        return invariant_CDPM_08(vars);
+    }
+
+    function echidna_cdp_manager_invariant_10() public returns (bool) {
+        return invariant_CDPM_10(cdpManager, vars);
+    }
+
+    function echidna_cdp_manager_invariant_11() public returns (bool) {
+        return invariant_CDPM_11(cdpManager, vars);
+    }
+
+    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) {

From c45acdea768b01cbdaf371670d5f28d2bb97858a Mon Sep 17 00:00:00 2001
From: wtj2021 <wtj2022@proton.me>
Date: Wed, 6 Mar 2024 15:07:25 -0800
Subject: [PATCH 02/11] cannot redeem last CDP

---
 .../contracts/TestContracts/invariants/Properties.sol       | 6 ------
 .../contracts/TestContracts/invariants/TargetFunctions.sol  | 2 ++
 2 files changed, 2 insertions(+), 6 deletions(-)

diff --git a/packages/contracts/contracts/TestContracts/invariants/Properties.sol b/packages/contracts/contracts/TestContracts/invariants/Properties.sol
index 8051db9ac..50af9db53 100644
--- a/packages/contracts/contracts/TestContracts/invariants/Properties.sol
+++ b/packages/contracts/contracts/TestContracts/invariants/Properties.sol
@@ -131,12 +131,6 @@ abstract contract Properties is BeforeAfter, PropertiesDescriptions, Asserts, Pr
         return true;
     }
 
-    function invariant_CDPM_09(Vars memory vars) internal view returns (bool) {
-        return
-            vars.cdpStakeAfter ==
-            (vars.cdpCollAfter * vars.totalStakesSnapshotAfter) / vars.totalCollateralSnapshotAfter;
-    }
-
     function invariant_CDPM_10(
         CdpManager cdpManager,
         Vars memory vars
diff --git a/packages/contracts/contracts/TestContracts/invariants/TargetFunctions.sol b/packages/contracts/contracts/TestContracts/invariants/TargetFunctions.sol
index a28ace9dd..f571e4f2e 100644
--- a/packages/contracts/contracts/TestContracts/invariants/TargetFunctions.sol
+++ b/packages/contracts/contracts/TestContracts/invariants/TargetFunctions.sol
@@ -534,6 +534,8 @@ abstract contract TargetFunctions is Properties {
         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);

From 06ca3168b251f2f0dc3c6b9b6273bd16b9a62ad1 Mon Sep 17 00:00:00 2001
From: wtj2021 <wtj2022@proton.me>
Date: Wed, 6 Mar 2024 16:15:56 -0800
Subject: [PATCH 03/11] debugging CDPM-09

---
 .../invariants/TargetFunctions.sol            | 28 +++++++++++++++----
 .../foundry_test/EchidnaToFoundry.t.sol       |  4 +--
 2 files changed, 25 insertions(+), 7 deletions(-)

diff --git a/packages/contracts/contracts/TestContracts/invariants/TargetFunctions.sol b/packages/contracts/contracts/TestContracts/invariants/TargetFunctions.sol
index f571e4f2e..981efd835 100644
--- a/packages/contracts/contracts/TestContracts/invariants/TargetFunctions.sol
+++ b/packages/contracts/contracts/TestContracts/invariants/TargetFunctions.sol
@@ -26,6 +26,7 @@ import "./BeforeAfter.sol";
 import "./TargetContractSetup.sol";
 import "./Asserts.sol";
 import "../BaseStorageVariables.sol";
+import "forge-std/console2.sol";
 
 abstract contract TargetFunctions is Properties {
     modifier setup() virtual {
@@ -377,11 +378,28 @@ abstract contract TargetFunctions is Properties {
     }
 
     function _check_CDPM_09() private {
-        eq(
-            vars.cdpStakeAfter,
-            (vars.cdpCollAfter * vars.totalStakesSnapshotAfter) / vars.totalCollateralSnapshotAfter,
-            CDPM_09
-        );
+        console2.log("cdpStakeAfter", vars.cdpStakeAfter);
+        console2.log("cdpCollAfter", vars.cdpCollAfter);
+        console2.log("cdpManager.totalStakes()", cdpManager.totalStakes());
+        console2.log("cdpManager.getSystemCollShares()", cdpManager.getSystemCollShares());
+        console2.log("cdpManager.totalStakesSnapshot()", cdpManager.totalStakesSnapshot());
+        console2.log("cdpManager.totalCollateralSnapshot()", cdpManager.totalCollateralSnapshot());
+        console2.log("totalStakesSnapshotAfter", vars.totalStakesSnapshotAfter);
+        console2.log("totalCollateralSnapshotAfter", vars.totalCollateralSnapshotAfter);
+
+        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 */
diff --git a/packages/contracts/foundry_test/EchidnaToFoundry.t.sol b/packages/contracts/foundry_test/EchidnaToFoundry.t.sol
index 05a53a78a..f606a7c2f 100644
--- a/packages/contracts/foundry_test/EchidnaToFoundry.t.sol
+++ b/packages/contracts/foundry_test/EchidnaToFoundry.t.sol
@@ -505,7 +505,7 @@ contract EToFoundry is
             51745835282927565687010251523416875790034155913406312339604760725754223914917,
             1000
         );
-        vm.warp(block.timestamp + cdpManager.recoveryModeGracePeriodDuration() + 1);
+        /*vm.warp(block.timestamp + cdpManager.recoveryModeGracePeriodDuration() + 1);
         setEthPerShare(
             79832022615203712424393490440177025697015516400034287083326403000335384151815
         );
@@ -528,7 +528,7 @@ contract EToFoundry is
             vars.newIcrBefore < cdpManager.MCR() ||
                 (vars.newIcrBefore < cdpManager.CCR() && vars.isRecoveryModeBefore),
             "Mcr, ccr"
-        );
+        );*/
     }
 
     function testPartialLiquidationCanCloseCDPS() public {

From 28ef54aabef7050670ecb46883a3f979e9d51b92 Mon Sep 17 00:00:00 2001
From: wtj2021 <wtj2022@proton.me>
Date: Wed, 6 Mar 2024 16:43:44 -0800
Subject: [PATCH 04/11] removing CDPM-9 from partialLiquidate

---
 .../invariants/TargetFunctions.sol            | 20 +++----------------
 .../foundry_test/EchidnaToFoundry.t.sol       |  4 ++--
 2 files changed, 5 insertions(+), 19 deletions(-)

diff --git a/packages/contracts/contracts/TestContracts/invariants/TargetFunctions.sol b/packages/contracts/contracts/TestContracts/invariants/TargetFunctions.sol
index 981efd835..84af3b0e3 100644
--- a/packages/contracts/contracts/TestContracts/invariants/TargetFunctions.sol
+++ b/packages/contracts/contracts/TestContracts/invariants/TargetFunctions.sol
@@ -370,35 +370,21 @@ abstract contract TargetFunctions is Properties {
 
             gte(_partialAmount, borrowerOperations.MIN_CHANGE(), GENERAL_16);
             gte(vars.cdpDebtAfter, borrowerOperations.MIN_CHANGE(), GENERAL_15);
-
-            _check_CDPM_09();
         } else {
             assertRevertReasonNotEqual(returnData, "Panic(17)");
         }
     }
 
     function _check_CDPM_09() private {
-        console2.log("cdpStakeAfter", vars.cdpStakeAfter);
-        console2.log("cdpCollAfter", vars.cdpCollAfter);
-        console2.log("cdpManager.totalStakes()", cdpManager.totalStakes());
-        console2.log("cdpManager.getSystemCollShares()", cdpManager.getSystemCollShares());
-        console2.log("cdpManager.totalStakesSnapshot()", cdpManager.totalStakesSnapshot());
-        console2.log("cdpManager.totalCollateralSnapshot()", cdpManager.totalCollateralSnapshot());
-        console2.log("totalStakesSnapshotAfter", vars.totalStakesSnapshotAfter);
-        console2.log("totalCollateralSnapshotAfter", vars.totalCollateralSnapshotAfter);
-
         if (vars.totalCollateralSnapshotAfter > 0) {
             eq(
                 vars.cdpStakeAfter,
-                (vars.cdpCollAfter * vars.totalStakesSnapshotAfter) / vars.totalCollateralSnapshotAfter,
+                (vars.cdpCollAfter * vars.totalStakesSnapshotAfter) /
+                    vars.totalCollateralSnapshotAfter,
                 CDPM_09
             );
         } else {
-            eq(
-                vars.cdpStakeAfter,
-                vars.cdpCollAfter,
-                CDPM_09
-            );
+            eq(vars.cdpStakeAfter, vars.cdpCollAfter, CDPM_09);
         }
     }
 
diff --git a/packages/contracts/foundry_test/EchidnaToFoundry.t.sol b/packages/contracts/foundry_test/EchidnaToFoundry.t.sol
index f606a7c2f..05a53a78a 100644
--- a/packages/contracts/foundry_test/EchidnaToFoundry.t.sol
+++ b/packages/contracts/foundry_test/EchidnaToFoundry.t.sol
@@ -505,7 +505,7 @@ contract EToFoundry is
             51745835282927565687010251523416875790034155913406312339604760725754223914917,
             1000
         );
-        /*vm.warp(block.timestamp + cdpManager.recoveryModeGracePeriodDuration() + 1);
+        vm.warp(block.timestamp + cdpManager.recoveryModeGracePeriodDuration() + 1);
         setEthPerShare(
             79832022615203712424393490440177025697015516400034287083326403000335384151815
         );
@@ -528,7 +528,7 @@ contract EToFoundry is
             vars.newIcrBefore < cdpManager.MCR() ||
                 (vars.newIcrBefore < cdpManager.CCR() && vars.isRecoveryModeBefore),
             "Mcr, ccr"
-        );*/
+        );
     }
 
     function testPartialLiquidationCanCloseCDPS() public {

From 394e181d64efdc47bb89e6ecf15e4a34036e85c5 Mon Sep 17 00:00:00 2001
From: wtj2021 <wtj2022@proton.me>
Date: Thu, 7 Mar 2024 08:58:45 -0800
Subject: [PATCH 05/11] updating properties

---
 .../TestContracts/invariants/Properties.sol        | 14 ++++----------
 .../invariants/echidna/EchidnaProperties.sol       |  4 ++--
 2 files changed, 6 insertions(+), 12 deletions(-)

diff --git a/packages/contracts/contracts/TestContracts/invariants/Properties.sol b/packages/contracts/contracts/TestContracts/invariants/Properties.sol
index 50af9db53..d1b23fbf2 100644
--- a/packages/contracts/contracts/TestContracts/invariants/Properties.sol
+++ b/packages/contracts/contracts/TestContracts/invariants/Properties.sol
@@ -131,22 +131,16 @@ abstract contract Properties is BeforeAfter, PropertiesDescriptions, Asserts, Pr
         return true;
     }
 
-    function invariant_CDPM_10(
-        CdpManager cdpManager,
-        Vars memory vars
-    ) internal view returns (bool) {
+    function invariant_CDPM_10(CdpManager cdpManager) internal view returns (bool) {
         if (vars.afterStEthFeeIndex > vars.prevStEthFeeIndex) {
-            return cdpManager.totalStakesSnapshot() == vars.totalStakesAfter;
+            return cdpManager.totalStakesSnapshot() == cdpManager.totalStakes();
         }
         return true;
     }
 
-    function invariant_CDPM_11(
-        CdpManager cdpManager,
-        Vars memory vars
-    ) internal view returns (bool) {
+    function invariant_CDPM_11(CdpManager cdpManager) internal view returns (bool) {
         if (vars.afterStEthFeeIndex > vars.prevStEthFeeIndex) {
-            return cdpManager.totalCollateralSnapshot() == vars.totalCollateralSnapshotAfter;
+            return cdpManager.totalCollateralSnapshot() == cdpManager.getSystemCollShares();
         }
         return true;
     }
diff --git a/packages/contracts/contracts/TestContracts/invariants/echidna/EchidnaProperties.sol b/packages/contracts/contracts/TestContracts/invariants/echidna/EchidnaProperties.sol
index 7c65d6dba..d71fb0c54 100644
--- a/packages/contracts/contracts/TestContracts/invariants/echidna/EchidnaProperties.sol
+++ b/packages/contracts/contracts/TestContracts/invariants/echidna/EchidnaProperties.sol
@@ -49,11 +49,11 @@ abstract contract EchidnaProperties is TargetContractSetup, Properties {
     }
 
     function echidna_cdp_manager_invariant_10() public returns (bool) {
-        return invariant_CDPM_10(cdpManager, vars);
+        return invariant_CDPM_10(cdpManager);
     }
 
     function echidna_cdp_manager_invariant_11() public returns (bool) {
-        return invariant_CDPM_11(cdpManager, vars);
+        return invariant_CDPM_11(cdpManager);
     }
 
     function echidna_cdp_manager_invariant_12() public returns (bool) {

From 1d9c93325fdbeec112855935a6f58ef65e713fce Mon Sep 17 00:00:00 2001
From: wtj2021 <wtj2022@proton.me>
Date: Thu, 7 Mar 2024 10:37:11 -0800
Subject: [PATCH 06/11] fixing invariants

---
 packages/contracts/contracts/CRLens.sol       | 10 ++++++
 .../contracts/Interfaces/ICdpManagerData.sol  |  4 +++
 .../TestContracts/invariants/BeforeAfter.sol  | 12 ++++---
 .../TestContracts/invariants/Properties.sol   | 14 --------
 .../invariants/TargetFunctions.sol            | 34 ++++++++++++-------
 .../invariants/echidna/EchidnaProperties.sol  |  8 -----
 6 files changed, 42 insertions(+), 40 deletions(-)

diff --git a/packages/contracts/contracts/CRLens.sol b/packages/contracts/contracts/CRLens.sol
index 978e43a2d..a21c4d5e8 100644
--- a/packages/contracts/contracts/CRLens.sol
+++ b/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
diff --git a/packages/contracts/contracts/Interfaces/ICdpManagerData.sol b/packages/contracts/contracts/Interfaces/ICdpManagerData.sol
index 978477c67..6060bebf8 100644
--- a/packages/contracts/contracts/Interfaces/ICdpManagerData.sol
+++ b/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);
 }
diff --git a/packages/contracts/contracts/TestContracts/invariants/BeforeAfter.sol b/packages/contracts/contracts/TestContracts/invariants/BeforeAfter.sol
index 799e2b2d8..bffb6d5c0 100644
--- a/packages/contracts/contracts/TestContracts/invariants/BeforeAfter.sol
+++ b/packages/contracts/contracts/TestContracts/invariants/BeforeAfter.sol
@@ -90,15 +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) ? cdpManager.getCdpStake(_cdpId) : 0;
+        vars.cdpStakeBefore = _cdpId != bytes32(0) ? crLens.getRealStake(_cdpId) : 0;
         vars.liquidatorRewardSharesBefore = _cdpId != bytes32(0)
             ? cdpManager.getCdpLiquidatorRewardShares(_cdpId)
             : 0;
@@ -155,11 +155,13 @@ abstract contract BeforeAfter is BaseStorageVariables {
     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) ? cdpManager.getCdpStake(_cdpId) : 0;
+        vars.cdpStakeAfter = _cdpId != bytes32(0) ? crLens.getRealStake(_cdpId) : 0;
         vars.liquidatorRewardSharesAfter = _cdpId != bytes32(0)
             ? cdpManager.getCdpLiquidatorRewardShares(_cdpId)
             : 0;
diff --git a/packages/contracts/contracts/TestContracts/invariants/Properties.sol b/packages/contracts/contracts/TestContracts/invariants/Properties.sol
index d1b23fbf2..b5e0d75d5 100644
--- a/packages/contracts/contracts/TestContracts/invariants/Properties.sol
+++ b/packages/contracts/contracts/TestContracts/invariants/Properties.sol
@@ -117,20 +117,6 @@ abstract contract Properties is BeforeAfter, PropertiesDescriptions, Asserts, Pr
             isApproximateEq(vars.valueInSystemAfter, vars.valueInSystemBefore, 0.01e18);
     }
 
-    function invariant_CDPM_07(Vars memory vars) internal view returns (bool) {
-        if (vars.cdpCollAfter < vars.cdpCollBefore) {
-            return vars.cdpStakeAfter < vars.cdpStakeBefore;
-        }
-        return true;
-    }
-
-    function invariant_CDPM_08(Vars memory vars) internal view returns (bool) {
-        if (vars.cdpCollAfter > vars.cdpCollBefore) {
-            return vars.cdpStakeAfter > vars.cdpStakeBefore;
-        }
-        return true;
-    }
-
     function invariant_CDPM_10(CdpManager cdpManager) internal view returns (bool) {
         if (vars.afterStEthFeeIndex > vars.prevStEthFeeIndex) {
             return cdpManager.totalStakesSnapshot() == cdpManager.totalStakes();
diff --git a/packages/contracts/contracts/TestContracts/invariants/TargetFunctions.sol b/packages/contracts/contracts/TestContracts/invariants/TargetFunctions.sol
index 84af3b0e3..e835340c8 100644
--- a/packages/contracts/contracts/TestContracts/invariants/TargetFunctions.sol
+++ b/packages/contracts/contracts/TestContracts/invariants/TargetFunctions.sol
@@ -282,7 +282,7 @@ abstract contract TargetFunctions is Properties {
                 totalCdpDustMaxCap += cdpManager.getActiveCdpsCount();
             }
 
-            _check_CDPM_09();
+            _checkStakeInvariants();
         } else if (vars.sortedCdpsSizeBefore > _i) {
             assertRevertReasonNotEqual(returnData, "Panic(17)");
         }
@@ -375,7 +375,15 @@ abstract contract TargetFunctions is Properties {
         }
     }
 
-    function _check_CDPM_09() private {
+    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,
@@ -480,7 +488,7 @@ abstract contract TargetFunctions is Properties {
                 totalCdpDustMaxCap += cdpManager.getActiveCdpsCount();
             }
 
-            _check_CDPM_09();
+            _checkStakeInvariants();
         } else if (vars.sortedCdpsSizeBefore > _n) {
             if (_atLeastOneCdpIsLiquidatable(cdpsBefore, vars.isRecoveryModeBefore)) {
                 assertRevertReasonNotEqual(returnData, "Panic(17)");
@@ -629,7 +637,7 @@ abstract contract TargetFunctions is Properties {
             t(!vars.lastGracePeriodStartTimestampIsSetAfter, L_16);
         }
 
-        _check_CDPM_09();
+        _checkStakeInvariants();
     }
 
     ///////////////////////////////////////////////////////
@@ -688,7 +696,7 @@ abstract contract TargetFunctions is Properties {
             t(!vars.lastGracePeriodStartTimestampIsSetAfter, L_16);
         }
 
-        _check_CDPM_09();
+        _checkStakeInvariants();
     }
 
     ///////////////////////////////////////////////////////
@@ -744,7 +752,7 @@ abstract contract TargetFunctions is Properties {
             t(!vars.lastGracePeriodStartTimestampIsSetAfter, L_16);
         }
 
-        _check_CDPM_09();
+        _checkStakeInvariants();
     }
 
     function openCdp(uint256 _col, uint256 _EBTCAmount) public setup returns (bytes32 _cdpId) {
@@ -829,7 +837,7 @@ abstract contract TargetFunctions is Properties {
             gte(vars.cdpDebtAfter, borrowerOperations.MIN_CHANGE(), GENERAL_15);
             require(invariant_BO_09(cdpManager, priceFeedMock.getPrice(), _cdpId), BO_09);
 
-            _check_CDPM_09();
+            _checkStakeInvariants();
         } else {
             assertRevertReasonNotEqual(returnData, "Panic(17)"); /// Done
         }
@@ -931,7 +939,7 @@ abstract contract TargetFunctions is Properties {
 
             gte(_coll, borrowerOperations.MIN_CHANGE(), GENERAL_16);
 
-            _check_CDPM_09();
+            _checkStakeInvariants();
         } else {
             assertRevertReasonNotEqual(returnData, "Panic(17)");
         }
@@ -1003,7 +1011,7 @@ abstract contract TargetFunctions is Properties {
 
             gte(_amount, borrowerOperations.MIN_CHANGE(), GENERAL_16);
 
-            _check_CDPM_09();
+            _checkStakeInvariants();
         } else {
             assertRevertReasonNotEqual(returnData, "Panic(17)");
         }
@@ -1077,7 +1085,7 @@ abstract contract TargetFunctions is Properties {
             gte(_amount, borrowerOperations.MIN_CHANGE(), GENERAL_16);
             gte(vars.cdpDebtAfter, borrowerOperations.MIN_CHANGE(), GENERAL_15);
 
-            _check_CDPM_09();
+            _checkStakeInvariants();
         } else {
             assertRevertReasonNotEqual(returnData, "Panic(17)");
         }
@@ -1151,7 +1159,7 @@ abstract contract TargetFunctions is Properties {
             gte(_amount, borrowerOperations.MIN_CHANGE(), GENERAL_16);
             gte(vars.cdpDebtAfter, borrowerOperations.MIN_CHANGE(), GENERAL_15);
 
-            _check_CDPM_09();
+            _checkStakeInvariants();
         } else {
             assertRevertReasonNotEqual(returnData, "Panic(17)");
         }
@@ -1229,7 +1237,7 @@ abstract contract TargetFunctions is Properties {
                 t(!vars.lastGracePeriodStartTimestampIsSetAfter, L_16);
             }
 
-            _check_CDPM_09();
+            _checkStakeInvariants();
         } else {
             assertRevertReasonNotEqual(returnData, "Panic(17)");
         }
@@ -1318,7 +1326,7 @@ abstract contract TargetFunctions is Properties {
         }
         gte(vars.cdpDebtAfter, borrowerOperations.MIN_CHANGE(), GENERAL_15);
 
-        _check_CDPM_09();
+        _checkStakeInvariants();
     }
 
     ///////////////////////////////////////////////////////
diff --git a/packages/contracts/contracts/TestContracts/invariants/echidna/EchidnaProperties.sol b/packages/contracts/contracts/TestContracts/invariants/echidna/EchidnaProperties.sol
index d71fb0c54..8b930bb39 100644
--- a/packages/contracts/contracts/TestContracts/invariants/echidna/EchidnaProperties.sol
+++ b/packages/contracts/contracts/TestContracts/invariants/echidna/EchidnaProperties.sol
@@ -40,14 +40,6 @@ abstract contract EchidnaProperties is TargetContractSetup, Properties {
         return invariant_CDPM_03(cdpManager);
     }
 
-    function echidna_cdp_manager_invariant_7() public returns (bool) {
-        return invariant_CDPM_07(vars);
-    }
-
-    function echidna_cdp_manager_invariant_8() public returns (bool) {
-        return invariant_CDPM_08(vars);
-    }
-
     function echidna_cdp_manager_invariant_10() public returns (bool) {
         return invariant_CDPM_10(cdpManager);
     }

From 96b13f1c7c0f2b89a4b9eb14a66950b0c00d457b Mon Sep 17 00:00:00 2001
From: wtj2021 <wtj2022@proton.me>
Date: Thu, 7 Mar 2024 10:56:29 -0800
Subject: [PATCH 07/11] removing bad import

---
 .../contracts/TestContracts/invariants/TargetFunctions.sol       | 1 -
 1 file changed, 1 deletion(-)

diff --git a/packages/contracts/contracts/TestContracts/invariants/TargetFunctions.sol b/packages/contracts/contracts/TestContracts/invariants/TargetFunctions.sol
index e835340c8..f4f66e1ee 100644
--- a/packages/contracts/contracts/TestContracts/invariants/TargetFunctions.sol
+++ b/packages/contracts/contracts/TestContracts/invariants/TargetFunctions.sol
@@ -26,7 +26,6 @@ import "./BeforeAfter.sol";
 import "./TargetContractSetup.sol";
 import "./Asserts.sol";
 import "../BaseStorageVariables.sol";
-import "forge-std/console2.sol";
 
 abstract contract TargetFunctions is Properties {
     modifier setup() virtual {

From 8490e1ee7bbb02f37cfb3cbce2077efba5e77f79 Mon Sep 17 00:00:00 2001
From: wtj2021 <wtj2022@proton.me>
Date: Thu, 7 Mar 2024 14:29:18 -0800
Subject: [PATCH 08/11] setting solc version

---
 packages/contracts/foundry.toml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/packages/contracts/foundry.toml b/packages/contracts/foundry.toml
index 8554675e2..ff558e3b1 100644
--- a/packages/contracts/foundry.toml
+++ b/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'
 

From 4022621fabd4edd5f5117aac08f27d3e87abb12b Mon Sep 17 00:00:00 2001
From: wtj2021 <wtj2022@proton.me>
Date: Thu, 7 Mar 2024 14:40:08 -0800
Subject: [PATCH 09/11] adding remapping

---
 packages/contracts/foundry.toml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/packages/contracts/foundry.toml b/packages/contracts/foundry.toml
index ff558e3b1..54e8d1c09 100644
--- a/packages/contracts/foundry.toml
+++ b/packages/contracts/foundry.toml
@@ -13,3 +13,7 @@ evm_version = 'london'
 [fuzz]
 max_test_rejects=2147483647
 runs=200
+
+remappings = [
+    "@crytic/=lib/"
+]
\ No newline at end of file

From e58c1f368ecd62fd3d3295e8fb46f4e46f547745 Mon Sep 17 00:00:00 2001
From: wtj2021 <wtj2022@proton.me>
Date: Thu, 7 Mar 2024 14:56:14 -0800
Subject: [PATCH 10/11] remapping

---
 packages/contracts/remappings.txt | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/packages/contracts/remappings.txt b/packages/contracts/remappings.txt
index 0c0cd3440..9493bd592 100644
--- a/packages/contracts/remappings.txt
+++ b/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/
\ No newline at end of file
+@crytic/properties/=lib/properties/
+@openzeppelin/=node_modules/@openzeppelin/

From d423cead559788050cda9173a63eb13da8e48662 Mon Sep 17 00:00:00 2001
From: wtj2021 <wtj2022@proton.me>
Date: Thu, 7 Mar 2024 16:58:19 -0800
Subject: [PATCH 11/11] removing remappings

---
 packages/contracts/foundry.toml   | 4 ----
 packages/contracts/remappings.txt | 2 +-
 2 files changed, 1 insertion(+), 5 deletions(-)

diff --git a/packages/contracts/foundry.toml b/packages/contracts/foundry.toml
index 54e8d1c09..ff558e3b1 100644
--- a/packages/contracts/foundry.toml
+++ b/packages/contracts/foundry.toml
@@ -13,7 +13,3 @@ evm_version = 'london'
 [fuzz]
 max_test_rejects=2147483647
 runs=200
-
-remappings = [
-    "@crytic/=lib/"
-]
\ No newline at end of file
diff --git a/packages/contracts/remappings.txt b/packages/contracts/remappings.txt
index 9493bd592..77c39f7a4 100644
--- a/packages/contracts/remappings.txt
+++ b/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/=lib/properties/
+@crytic/properties/=node_modules/@crytic/properties/
 @openzeppelin/=node_modules/@openzeppelin/