test: Add ghost variables and inline assertions (SC-485)

foundry.toml

@@ -13,17 +13,20 @@ runs = 1000
 runs = 20
 depth = 1000
 shrink_run_limit = 1000
+fail_on_revert = true
 
 [profile.pr.invariant]
 runs = 200
 depth = 1000
+shrink_run_limit = 50_000
 
 [profile.pr.fuzz]
 runs = 100_000
 
 [profile.master.invariant]
 runs = 200
 depth = 10_000
+shrink_run_limit = 100_000
 
 [profile.master.fuzz]
 runs = 1_000_000

test/invariant/Invariants.t.sol

@@ -42,13 +42,14 @@ abstract contract PSMInvariantTestBase is PSMTestBase {
     /**********************************************************************************************/
 
     function _checkInvariant_A() public view {
-        assertEq(
-            psm.shares(address(lpHandler.lps(0))) +
-            psm.shares(address(lpHandler.lps(1))) +
-            psm.shares(address(lpHandler.lps(2))) +
-            1e18,  // Seed amount
-            psm.totalShares()
-        );
+        uint256 lpShares = 1e18;  // Seed amount
+
+        // TODO: Update to be dynamic
+        for (uint256 i = 0; i < 3; i++) {
+            lpShares += psm.shares(lpHandler.lps(i));
+        }
+
+        assertEq(lpShares, psm.totalShares());
     }
 
     function _checkInvariant_B() public view {
@@ -60,14 +61,104 @@ abstract contract PSMInvariantTestBase is PSMTestBase {
     }
 
     function _checkInvariant_C() public view {
-        assertApproxEqAbs(
-            psm.convertToAssetValue(psm.shares(address(lpHandler.lps(0)))) +
-            psm.convertToAssetValue(psm.shares(address(lpHandler.lps(1)))) +
-            psm.convertToAssetValue(psm.shares(address(lpHandler.lps(2)))) +
-            psm.convertToAssetValue(1e18),  // Seed amount
-            psm.totalAssets(),
-            4
-        );
+        uint256 lpAssetValue = psm.convertToAssetValue(1e18);  // Seed amount
+
+        for (uint256 i = 0; i < 3; i++) {
+            lpAssetValue += psm.convertToAssetValue(psm.shares(lpHandler.lps(i)));
+        }
+
+        assertApproxEqAbs(lpAssetValue, psm.totalAssets(), 4);
+    }
+
+    // This might be failing because of swap rounding errors.
+    function _checkInvariant_D() public view {
+        // Seed amounts
+        uint256 lpDeposits   = 1e18;
+        uint256 lpAssetValue = psm.convertToAssetValue(1e18);
+
+        for (uint256 i = 0; i < 3; i++) {
+            address lp = lpHandler.lps(i);
+
+            lpDeposits   += _getLpDepositsValue(lp);
+            lpAssetValue += psm.convertToAssetValue(psm.shares(lp));
+        }
+
+        // LPs position value can increase from transfers into the PSM and from swapping rounding
+        // errors increasing the value of the PSM slightly.
+        // Allow a 2e12 tolerance for negative rounding on conversion calculations.
+        assertGe(lpAssetValue + 2e12, lpDeposits);
+
+        // Include seed deposit, allow for 2e12 negative tolerance.
+        assertGe(psm.totalAssets() + 2e12, lpDeposits);
+    }
+
+    function _checkInvariant_E() public view {
+        uint256 expectedUsdcBalance = 0;
+        uint256 expectedDaiBalance  = 1e18;  // Seed amount
+        uint256 expectedSDaiBalance = 0;
+
+        for(uint256 i; i < 3; i++) {
+            address lp      = lpHandler.lps(i);
+            address swapper = swapperHandler.swappers(i);
+
+            expectedUsdcBalance += lpHandler.lpDeposits(lp, address(usdc));
+            expectedDaiBalance  += lpHandler.lpDeposits(lp, address(dai));
+            expectedSDaiBalance += lpHandler.lpDeposits(lp, address(sDai));
+
+            expectedUsdcBalance += swapperHandler.swapsIn(swapper, address(usdc));
+            expectedDaiBalance  += swapperHandler.swapsIn(swapper, address(dai));
+            expectedSDaiBalance += swapperHandler.swapsIn(swapper, address(sDai));
+        }
+
+        if (address(transferHandler) != address(0)) {
+            expectedUsdcBalance += transferHandler.transfersIn(address(usdc));
+            expectedDaiBalance  += transferHandler.transfersIn(address(dai));
+            expectedSDaiBalance += transferHandler.transfersIn(address(sDai));
+        }
+
+        // Loop twice to avoid underflows between LPs
+        for(uint256 i; i < 3; i++) {
+            address lp      = lpHandler.lps(i);
+            address swapper = swapperHandler.swappers(i);
+
+            expectedUsdcBalance -= lpHandler.lpWithdrawals(lp, address(usdc));
+            expectedDaiBalance  -= lpHandler.lpWithdrawals(lp, address(dai));
+            expectedSDaiBalance -= lpHandler.lpWithdrawals(lp, address(sDai));
+
+            expectedUsdcBalance -= swapperHandler.swapsOut(swapper, address(usdc));
+            expectedDaiBalance  -= swapperHandler.swapsOut(swapper, address(dai));
+            expectedSDaiBalance -= swapperHandler.swapsOut(swapper, address(sDai));
+        }
+
+        assertEq(usdc.balanceOf(address(psm)), expectedUsdcBalance);
+        assertEq(dai.balanceOf(address(psm)),  expectedDaiBalance);
+        assertEq(sDai.balanceOf(address(psm)), expectedSDaiBalance);
+    }
+
+    function _checkInvariant_F() public view {
+        uint256 totalValueSwappedIn;
+        uint256 totalValueSwappedOut;
+
+        for(uint256 i; i < 3; i++) {
+            address swapper = swapperHandler.swappers(i);
+
+            totalValueSwappedIn +=
+                swapperHandler.swapsIn(swapper, address(usdc)) * 1e12 +
+                swapperHandler.swapsIn(swapper, address(dai)) +
+                swapperHandler.swapsIn(swapper, address(sDai)) * rateProvider.getConversionRate() / 1e27;
+        }
+
+        // Loop twice to avoid underflows between LPs
+        for(uint256 i; i < 3; i++) {
+            address swapper = swapperHandler.swappers(i);
+
+            totalValueSwappedOut +=
+                swapperHandler.swapsIn(swapper, address(usdc)) * 1e12 +
+                swapperHandler.swapsIn(swapper, address(dai)) +
+                swapperHandler.swapsIn(swapper, address(sDai)) * rateProvider.getConversionRate() / 1e27;
+        }
+
+        assertEq(totalValueSwappedIn, totalValueSwappedOut);
     }
 
     /**********************************************************************************************/
@@ -98,6 +189,20 @@ abstract contract PSMInvariantTestBase is PSMTestBase {
         return daiValue + usdcValue + sDaiValue;
     }
 
+    function _getLpDepositsValue(address lp) internal view returns (uint256) {
+        uint256 depositValue =
+            lpHandler.lpDeposits(lp, address(dai)) +
+            lpHandler.lpDeposits(lp, address(usdc)) * 1e12 +
+            lpHandler.lpDeposits(lp, address(sDai)) * rateProvider.getConversionRate() / 1e27;
+
+        uint256 withdrawValue =
+            lpHandler.lpWithdrawals(lp, address(dai)) +
+            lpHandler.lpWithdrawals(lp, address(usdc)) * 1e12 +
+            lpHandler.lpWithdrawals(lp, address(sDai)) * rateProvider.getConversionRate() / 1e27;
+
+        return withdrawValue > depositValue ? 0 : depositValue - withdrawValue;
+    }
+
     /**********************************************************************************************/
     /*** After invariant hook functions                                                         ***/
     /**********************************************************************************************/
@@ -210,6 +315,9 @@ contract PSMInvariants_ConstantRate_NoTransfer is PSMInvariantTestBase {
 
         targetContract(address(lpHandler));
         targetContract(address(swapperHandler));
+
+        // Check that LPs used for swap assertions are correct to not get zero values
+        assertEq(swapperHandler.lp0(), lpHandler.lps(0));
     }
 
     function invariant_A() public view {
@@ -224,6 +332,18 @@ contract PSMInvariants_ConstantRate_NoTransfer is PSMInvariantTestBase {
         _checkInvariant_C();
     }
 
+    function invariant_D() public view {
+        _checkInvariant_D();
+    }
+
+    function invariant_E() public view {
+        _checkInvariant_E();
+    }
+
+    function invariant_F() public view {
+        _checkInvariant_F();
+    }
+
     function afterInvariant() public {
         _withdrawAllPositions();
     }
@@ -256,6 +376,17 @@ contract PSMInvariants_ConstantRate_WithTransfers is PSMInvariantTestBase {
         _checkInvariant_C();
     }
 
+    // No invariant D because rate changes lead to large rounding errors when compared with
+    // ghost variables
+
+    function invariant_E() public view {
+        _checkInvariant_E();
+    }
+
+    function invariant_F() public view {
+        _checkInvariant_F();
+    }
+
     function afterInvariant() public {
         _withdrawAllPositions();
     }
@@ -268,12 +399,15 @@ contract PSMInvariants_RateSetting_NoTransfer is PSMInvariantTestBase {
         super.setUp();
 
         lpHandler         = new LpHandler(psm, dai, usdc, sDai, 3);
-        rateSetterHandler = new RateSetterHandler(address(rateProvider), 1.25e27);
+        rateSetterHandler = new RateSetterHandler(psm, address(rateProvider), 1.25e27);
         swapperHandler    = new SwapperHandler(psm, dai, usdc, sDai, 3);
 
         targetContract(address(lpHandler));
         targetContract(address(rateSetterHandler));
         targetContract(address(swapperHandler));
+
+        // Check that LPs used for swap assertions are correct to not get zero values
+        assertEq(swapperHandler.lp0(), lpHandler.lps(0));
     }
 
     function invariant_A() public view {
@@ -288,6 +422,17 @@ contract PSMInvariants_RateSetting_NoTransfer is PSMInvariantTestBase {
         _checkInvariant_C();
     }
 
+    // No invariant D because rate changes lead to large rounding errors when compared with
+    // ghost variables
+
+    function invariant_E() public view {
+        _checkInvariant_E();
+    }
+
+    function invariant_F() public view {
+        _checkInvariant_F();
+    }
+
     function afterInvariant() public {
         _withdrawAllPositions();
     }
@@ -300,14 +445,17 @@ contract PSMInvariants_RateSetting_WithTransfers is PSMInvariantTestBase {
         super.setUp();
 
         lpHandler         = new LpHandler(psm, dai, usdc, sDai, 3);
-        rateSetterHandler = new RateSetterHandler(address(rateProvider), 1.25e27);
+        rateSetterHandler = new RateSetterHandler(psm, address(rateProvider), 1.25e27);
         swapperHandler    = new SwapperHandler(psm, dai, usdc, sDai, 3);
         transferHandler   = new TransferHandler(psm, dai, usdc, sDai);
 
         targetContract(address(lpHandler));
         targetContract(address(rateSetterHandler));
         targetContract(address(swapperHandler));
         targetContract(address(transferHandler));
+
+        // Check that LPs used for swap assertions are correct to not get zero values
+        assertEq(swapperHandler.lp0(), lpHandler.lps(0));
     }
 
     function invariant_A() public view {
@@ -322,6 +470,17 @@ contract PSMInvariants_RateSetting_WithTransfers is PSMInvariantTestBase {
         _checkInvariant_C();
     }
 
+    // No invariant D because rate changes lead to large rounding errors when compared with
+    // ghost variables
+
+    function invariant_E() public view {
+        _checkInvariant_E();
+    }
+
+    function invariant_F() public view {
+        _checkInvariant_F();
+    }
+
     function afterInvariant() public {
         _withdrawAllPositions();
     }
@@ -343,7 +502,7 @@ contract PSMInvariants_TimeBasedRateSetting_NoTransfer is PSMInvariantTestBase {
 
         lpHandler            = new LpHandler(psm, dai, usdc, sDai, 3);
         swapperHandler       = new SwapperHandler(psm, dai, usdc, sDai, 3);
-        timeBasedRateHandler = new TimeBasedRateHandler(dsrOracle);
+        timeBasedRateHandler = new TimeBasedRateHandler(psm, dsrOracle);
 
         // Handler acts in the same way as a receiver on L2, so add as a data provider to the
         // oracle.
@@ -352,14 +511,17 @@ contract PSMInvariants_TimeBasedRateSetting_NoTransfer is PSMInvariantTestBase {
         rateProvider = IRateProviderLike(address(dsrOracle));
 
         // Manually set initial values for the oracle through the handler to start
-        timeBasedRateHandler.setPotData(1e27, block.timestamp);
+        timeBasedRateHandler.setPotData(1e27);
 
         targetContract(address(lpHandler));
         targetContract(address(swapperHandler));
         targetContract(address(timeBasedRateHandler));
+
+        // Check that LPs used for swap assertions are correct to not get zero values
+        assertEq(swapperHandler.lp0(), lpHandler.lps(0));
     }
 
-    function invariant_A() public view {
+    function invariant_A_test() public view {
         _checkInvariant_A();
     }
 
@@ -371,6 +533,17 @@ contract PSMInvariants_TimeBasedRateSetting_NoTransfer is PSMInvariantTestBase {
         _checkInvariant_C();
     }
 
+    // No invariant D because rate changes lead to large rounding errors when compared with
+    // ghost variables
+
+    function invariant_E() public view {
+        _checkInvariant_E();
+    }
+
+    function invariant_F() public view {
+        _checkInvariant_F();
+    }
+
     function afterInvariant() public {
         _withdrawAllPositions();
     }
@@ -392,7 +565,7 @@ contract PSMInvariants_TimeBasedRateSetting_WithTransfers is PSMInvariantTestBas
 
         lpHandler            = new LpHandler(psm, dai, usdc, sDai, 3);
         swapperHandler       = new SwapperHandler(psm, dai, usdc, sDai, 3);
-        timeBasedRateHandler = new TimeBasedRateHandler(dsrOracle);
+        timeBasedRateHandler = new TimeBasedRateHandler(psm, dsrOracle);
         transferHandler      = new TransferHandler(psm, dai, usdc, sDai);
 
         // Handler acts in the same way as a receiver on L2, so add as a data provider to the
@@ -402,12 +575,15 @@ contract PSMInvariants_TimeBasedRateSetting_WithTransfers is PSMInvariantTestBas
         rateProvider = IRateProviderLike(address(dsrOracle));
 
         // Manually set initial values for the oracle through the handler to start
-        timeBasedRateHandler.setPotData(1e27, block.timestamp);
+        timeBasedRateHandler.setPotData(1e27);
 
         targetContract(address(lpHandler));
         targetContract(address(swapperHandler));
         targetContract(address(timeBasedRateHandler));
         targetContract(address(transferHandler));
+
+        // Check that LPs used for swap assertions are correct to not get zero values
+        assertEq(swapperHandler.lp0(), lpHandler.lps(0));
     }
 
     function invariant_A() public view {
@@ -422,6 +598,17 @@ contract PSMInvariants_TimeBasedRateSetting_WithTransfers is PSMInvariantTestBas
         _checkInvariant_C();
     }
 
+    // No invariant D because rate changes lead to large rounding errors when compared with
+    // ghost variables
+
+    function invariant_E() public view {
+        _checkInvariant_E();
+    }
+
+    function invariant_F() public view {
+        _checkInvariant_F();
+    }
+
     function afterInvariant() public {
         _withdrawAllPositions();
     }