test: invariant to compare total debt, streamed amount and withdrawn …

…amount

README.md

@@ -179,4 +179,4 @@ Currently, it's not possible to address this precision problem entirely.
 
 13. if $isVoided = true \implies isPaused = true$, $ra = 0$ and $ud = 0$
 
-14. For a given stream, if $δ(rps) = 0$ $\implies td = streamedAmount - totalWithdrawn$
+14. For a given non-voided stream, $\text{total debt} = \text{streamed amount} - \text{withdrawn amount}$

test/fork/Flow.t.sol

@@ -584,10 +584,6 @@ contract Flow_Fork_Test is Fork_Test {
         uint256 initialTokenBalance = token.balanceOf(address(flow));
         uint128 totalDebt = flow.totalDebtOf(streamId);
 
-        uint128 ongoingDebtNormalized = getNormalizedAmount(flow.ongoingDebtOf(streamId), tokenDecimals);
-        uint128 ratePerSecond = flow.getRatePerSecond(streamId).unwrap();
-        uint40 snapshotTime = flow.getSnapshotTime(streamId);
-
         vars.expectedSnapshotTime = getBlockTimestamp();
 
         (, address caller,) = vm.readCallers();

test/invariant/Flow.t.sol

@@ -261,23 +261,17 @@ contract Flow_Invariant_Test is Base_Test {
         }
     }
 
-    /// @dev If ratePerSecond is not changed, then the total debt should be equal to the streamed amount minus the
+    /// @dev For any non-voided stream, the total debt should be equal to the total streamed amount minus the total
     /// withdrawn amount.
     function invariant_TotalDebtEqStreamedMinusWithdrawn() external view {
         uint256 lastStreamId = flowStore.lastStreamId();
         for (uint256 i = 0; i < lastStreamId; ++i) {
-            uint256 streamId = flowStore.streamIds(i);
-            uint128 streamedAmount = getDenormalizedAmount(
-                flow.getRatePerSecond(streamId).unwrap() * (getBlockTimestamp() - flow.getSnapshotTime(streamId)),
-                flow.getTokenDecimals(streamId)
-            );
-            if (
-                flowHandler.calls("adjustRatePerSecond") == 0 && flowHandler.calls("pause") == 0
-                    && flowHandler.calls("void") == 0
-            ) {
+            // Skip voided streams, because `void` changes the total debt without making any withdraw.
+            if (flowHandler.calls("void") == 0) {
+                uint256 streamId = flowStore.streamIds(i);
                 assertEq(
                     flow.totalDebtOf(streamId),
-                    streamedAmount - flowStore.withdrawnAmounts(streamId),
+                    flowStore.streamedAmount(streamId) - flowStore.withdrawnAmounts(streamId),
                     "Invariant violation: total debt != streamed amount - withdrawn amount"
                 );
             }

test/invariant/handlers/BaseHandler.sol

@@ -43,11 +43,26 @@ abstract contract BaseHandler is StdCheats, Utils {
                                      MODIFIERS
     //////////////////////////////////////////////////////////////////////////*/
 
-    /// @dev Simulates the passage of time. The time jump is upper bounded so that streams don't settle too quickly.
+    /// @notice Simulates the passage of time. The time jump is upper bounded so that streams don't settle too quickly.
+    /// @dev Updates the streamed amounts of all streams after the time jump.
     /// @param timeJumpSeed A fuzzed value needed for generating random time warps.
     modifier adjustTimestamp(uint256 timeJumpSeed) {
+        // Record the initial total debts of all streams.
+        uint128[] memory initialTotalDebts = new uint128[](flowStore.lastStreamId());
+        for (uint256 i = 0; i < flowStore.lastStreamId(); ++i) {
+            uint256 streamId = flowStore.streamIds(i);
+            initialTotalDebts[i] = flow.totalDebtOf(streamId);
+        }
+
         uint256 timeJump = _bound(timeJumpSeed, 0 seconds, 40 days);
         vm.warp(getBlockTimestamp() + timeJump);
+
+        // Update the streamed amounts by adding up the difference between the total debt before and after.
+        for (uint256 i = 0; i < flowStore.lastStreamId(); ++i) {
+            uint256 streamId = flowStore.streamIds(i);
+            flowStore.updateStreamedAmount(streamId, flow.totalDebtOf(streamId) - initialTotalDebts[i]);
+        }
+
         _;
     }
 

test/invariant/handlers/FlowCreateHandler.sol

@@ -100,10 +100,8 @@ contract FlowCreateHandler is BaseHandler {
     {
         vm.assume(flowStore.lastStreamId() < MAX_STREAM_COUNT);
 
-        uint8 decimals = IERC20Metadata(address(currentToken)).decimals();
-
         // Calculate the upper bound, based on the token decimals, for the deposit amount.
-        uint128 upperBound = getDenormalizedAmount(1_000_000e18, decimals);
+        uint128 upperBound = getDenormalizedAmount(1_000_000e18, IERC20Metadata(address(currentToken)).decimals());
 
         // Bound the stream parameters.
         params.ratePerSecond = boundRatePerSecond(params.ratePerSecond);

test/invariant/stores/FlowStore.sol

@@ -12,6 +12,7 @@ contract FlowStore {
     mapping(uint256 streamId => address sender) public senders;
     mapping(uint256 streamId => uint128 depositedAmount) public depositedAmounts;
     mapping(uint256 streamId => uint128 refundedAmount) public refundedAmounts;
+    mapping(uint256 streamId => uint128 streamedAmount) public streamedAmount;
     mapping(uint256 streamId => uint128 withdrawnAmount) public withdrawnAmounts;
     uint256[] public streamIds;
     uint256 public streamDepositedAmountsSum;
@@ -37,6 +38,10 @@ contract FlowStore {
         streamDepositedAmountsSum += amount;
     }
 
+    function updateStreamedAmount(uint256 streamId, uint128 amount) external {
+        streamedAmount[streamId] += amount;
+    }
+
     function updateStreamRefundedAmountsSum(uint256 streamId, uint128 amount) external {
         refundedAmounts[streamId] += amount;
         streamRefundedAmountsSum += amount;