test: refactor streamed amount invariant

TECHNICAL-DOC.md

@@ -92,7 +92,8 @@ can only withdraw the available balance.
 
 16. if $isVoided = true \implies isPaused = true$ and $ud = 0$
 
-17. if $isVoided = false \implies \text{amount streamed with delay} = td + \text{amount withdrawn}$.
+17. if $isVoided = false \implies \text{expected amount streamed} \ge td + \text{amount withdrawn}$ and
+    $\text{expected amount streamed} - (td + \text{amount withdrawn}) \le 10$
 
 ## Limitation
 

tests/invariant/Flow.t.sol

@@ -332,45 +332,57 @@ contract Flow_Invariant_Test is Base_Test {
         }
     }
 
-    /// @dev For non-voided streams, the difference between the total amount streamed adjusted including the delay and
-    /// the sum of total debt and total withdrawn should be equal. Also, total streamed amount with delay must never
-    /// exceed total streamed amount without delay.
-    function invariant_TotalStreamedWithDelayEqTotalDebtPlusWithdrawn() external view {
+    /// @dev For non-voided streams, the expected streamed amount should be greater than or equal to the sum of total
+    /// debt and withdrawn amount. And, the difference between the two should not exceed 10 wei.
+    function invariant_TotalStreamedEqTotalDebtPlusWithdrawn() external view {
         uint256 lastStreamId = flowStore.lastStreamId();
         for (uint256 i = 0; i < lastStreamId; ++i) {
             uint256 streamId = flowStore.streamIds(i);
 
             // Skip the voided streams.
             if (!flow.isVoided(streamId)) {
+                uint256 expectedTotalStreamed =
+                    calculateExpectedStreamedAmount(flowStore.streamIds(i), flow.getTokenDecimals(streamId));
+                uint256 actualTotalStreamed = flow.totalDebtOf(streamId) + flowStore.withdrawnAmounts(streamId);
+
+                assertGe(
+                    expectedTotalStreamed,
+                    actualTotalStreamed,
+                    "Invariant violation: expected streamed amount >= total debt + withdrawn amount"
+                );
+
                 assertLe(
-                    calculateTotalStreamedAmount(flowStore.streamIds(i), flow.getTokenDecimals(streamId)),
-                    flow.totalDebtOf(streamId) + flowStore.withdrawnAmounts(streamId),
-                    "Invariant violation: total streamed amount with delay = total debt + withdrawn amount"
+                    expectedTotalStreamed - actualTotalStreamed,
+                    10,
+                    "Invariant violation: expected streamed amount - total debt + withdrawn amount <= 10"
                 );
             }
         }
     }
 
-    /// @dev Calculates the total streamed amounts by iterating over each period.
-    function calculateTotalStreamedAmount(
+    /// @dev Calculates the maximum possible amount streamed, denoted in token's decimal, by iterating over all the
+    /// periods during which rate per second remained constant followed by descaling at the last step.
+    function calculateExpectedStreamedAmount(
         uint256 streamId,
         uint8 decimals
     )
         internal
         view
-        returns (uint256 totalStreamedAmount)
+        returns (uint256 expectedStreamedAmount)
     {
-        uint256 totalDelayedAmount;
-        uint256 periodsCount = flowStore.getPeriods(streamId).length;
+        uint256 count = flowStore.getPeriods(streamId).length;
 
-        for (uint256 i = 0; i < periodsCount; ++i) {
+        for (uint256 i = 0; i < count; ++i) {
             FlowStore.Period memory period = flowStore.getPeriod(streamId, i);
 
-            // If end time is 0, it means the current period is still active.
+            // If end time is 0, consider current time as the end time.
             uint128 elapsed = period.end > 0 ? period.end - period.start : uint40(block.timestamp) - period.start;
 
-            // Calculate the total streamed amount for the current period.
-            totalStreamedAmount += getDescaledAmount(period.ratePerSecond * elapsed, decimals);
+            // Increment total streamed amount by the amount streamed during this period.
+            expectedStreamedAmount += period.ratePerSecond * elapsed;
         }
+
+        // Descale the total streamed amount to token's decimal to get the maximum possible amount streamed.
+        return getDescaledAmount(expectedStreamedAmount, decimals);
     }
 }

tests/invariant/handlers/FlowHandler.sol

@@ -287,11 +287,5 @@ contract FlowHandler is BaseHandler {
 
         // Update the withdrawn amount.
         flowStore.updateStreamWithdrawnAmountsSum(currentStreamId, flow.getToken(currentStreamId), amount);
-
-        // If the stream isn't paused, update the delay:
-        uint128 ratePerSecond = flow.getRatePerSecond(currentStreamId).unwrap();
-        if (ratePerSecond > 0) {
-            flowStore.pushPeriod(currentStreamId, ratePerSecond, "withdraw");
-        }
     }
 }

tests/invariant/stores/FlowStore.sol

@@ -29,12 +29,12 @@ contract FlowStore {
     mapping(uint256 streamId => uint256 amount) public previousUncoveredDebtOf;
 
     /// @dev This struct represents a time period during which rate per second remains constant.
-    /// @param typeOfPeriod The type of the period, which is the function name.
+    /// @param funcName The name of the function updating the struct.
     /// @param ratePerSecond The rate per second for this period.
     /// @param start The start time of the period.
     /// @param end The end time of the period.
     struct Period {
-        string typeOfPeriod;
+        string funcName;
         uint128 ratePerSecond;
         uint40 start;
         uint40 end;
@@ -73,20 +73,20 @@ contract FlowStore {
         // Store the stream id and the period during which provided ratePerSecond applies.
         streamIds.push(streamId);
         periods[streamId].push(
-            Period({ typeOfPeriod: "create", ratePerSecond: ratePerSecond, start: uint40(block.timestamp), end: 0 })
+            Period({ funcName: "create", ratePerSecond: ratePerSecond, start: uint40(block.timestamp), end: 0 })
         );
 
         // Update the last stream id.
         lastStreamId = streamId;
     }
 
-    function pushPeriod(uint256 streamId, uint128 ratePerSecond, string memory typeOfPeriod) external {
+    function pushPeriod(uint256 streamId, uint128 newRatePerSecond, string memory typeOfPeriod) external {
         // Update the end time of the previous period.
         periods[streamId][periods[streamId].length - 1].end = uint40(block.timestamp);
 
         // Push the new period with the provided rate per second.
         periods[streamId].push(
-            Period({ ratePerSecond: ratePerSecond, start: uint40(block.timestamp), end: 0, typeOfPeriod: typeOfPeriod })
+            Period({ funcName: typeOfPeriod, ratePerSecond: newRatePerSecond, start: uint40(block.timestamp), end: 0 })
         );
     }