diff --git a/TECHNICAL-DOC.md b/TECHNICAL-DOC.md index ecbcafa1..55b65c7c 100644 --- a/TECHNICAL-DOC.md +++ b/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 diff --git a/tests/invariant/Flow.t.sol b/tests/invariant/Flow.t.sol index 9283a55f..060bd290 100644 --- a/tests/invariant/Flow.t.sol +++ b/tests/invariant/Flow.t.sol @@ -332,60 +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 totalStreamedAmount, uint256 totalStreamedAmountWithDelay) = - calculateTotalStreamedAmounts(flowStore.streamIds(i), flow.getTokenDecimals(streamId)); + uint256 expectedTotalStreamed = + calculateExpectedStreamedAmount(flowStore.streamIds(i), flow.getTokenDecimals(streamId)); + uint256 actualTotalStreamed = flow.totalDebtOf(streamId) + flowStore.withdrawnAmounts(streamId); assertGe( - totalStreamedAmount, - totalStreamedAmountWithDelay, - "Invariant violation: total streamed amount without delay >= total streamed amount with delay" + expectedTotalStreamed, + actualTotalStreamed, + "Invariant violation: expected streamed amount >= total debt + withdrawn amount" ); - assertEq( - totalStreamedAmountWithDelay, - flow.totalDebtOf(streamId) + flowStore.withdrawnAmounts(streamId), - "Invariant violation: total streamed amount with delay = total debt + withdrawn amount" + assertLe( + 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 calculateTotalStreamedAmounts( + /// @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, uint256 totalStreamedAmountWithDelay) + 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); - - // Calculate the total delayed amount for the current period. - totalDelayedAmount += getDescaledAmount(period.delay * period.ratePerSecond, decimals); + // Increment total streamed amount by the amount streamed during this period. + expectedStreamedAmount += period.ratePerSecond * elapsed; } - // Calculate the total streamed amount with delay. - totalStreamedAmountWithDelay = totalStreamedAmount - totalDelayedAmount; + // Descale the total streamed amount to token's decimal to get the maximum possible amount streamed. + return getDescaledAmount(expectedStreamedAmount, decimals); } } diff --git a/tests/invariant/handlers/FlowHandler.sol b/tests/invariant/handlers/FlowHandler.sol index 8fb55bc3..06d8fb10 100644 --- a/tests/invariant/handlers/FlowHandler.sol +++ b/tests/invariant/handlers/FlowHandler.sol @@ -103,7 +103,6 @@ contract FlowHandler is BaseHandler { // Adjust the rate per second. flow.adjustRatePerSecond(currentStreamId, newRatePerSecond); - flowStore.updateDelay(currentStreamId, previousRatePerSecond, decimals); flowStore.pushPeriod(currentStreamId, newRatePerSecond.unwrap(), "adjustRatePerSecond"); } @@ -166,10 +165,6 @@ contract FlowHandler is BaseHandler { // Paused streams cannot be paused again. vm.assume(!flow.isPaused(currentStreamId)); - flowStore.updateDelay( - currentStreamId, flow.getRatePerSecond(currentStreamId).unwrap(), flow.getTokenDecimals(currentStreamId) - ); - // Pause the stream. flow.pause(currentStreamId); @@ -292,12 +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.updateDelay(currentStreamId, ratePerSecond, flow.getTokenDecimals(currentStreamId)); - flowStore.pushPeriod(currentStreamId, ratePerSecond, "withdraw"); - } } } diff --git a/tests/invariant/stores/FlowStore.sol b/tests/invariant/stores/FlowStore.sol index 9d2c4615..0859620d 100644 --- a/tests/invariant/stores/FlowStore.sol +++ b/tests/invariant/stores/FlowStore.sol @@ -29,17 +29,15 @@ 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. - /// @param delay The delay for the period. struct Period { - string typeOfPeriod; + string funcName; uint128 ratePerSecond; uint40 start; uint40 end; - uint40 delay; } /// @dev Each stream is mapped to an array of periods. This is used to calculate the total streamed amount. @@ -75,59 +73,23 @@ 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, - delay: 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, - delay: 0, - typeOfPeriod: typeOfPeriod - }) + Period({ funcName: typeOfPeriod, ratePerSecond: newRatePerSecond, start: uint40(block.timestamp), end: 0 }) ); } - function updateDelay(uint256 streamId, uint128 ratePerSecond, uint8 decimals) external { - // Skip the delay update if the decimals are 18. - if (decimals == 18) { - return; - } - - uint256 periodCount = periods[streamId].length - 1; - uint256 factor = uint128(10 ** (18 - decimals)); - uint256 blockTimestamp = uint40(block.timestamp); - uint256 start = periods[streamId][periodCount].start; - - uint256 rescaledStreamedAmount = ratePerSecond * (blockTimestamp - start) / factor * factor; - - uint40 delay; - if (rescaledStreamedAmount > ratePerSecond) { - delay = uint40(blockTimestamp - start - (rescaledStreamedAmount / ratePerSecond)); - // Since we are reverse engineering the delay, we need to subtract 1 from the delay, which would normally be - // added in the constant interval calculation - delay = delay > 1 ? delay - 1 : 0; - } - - periods[streamId][periodCount].delay += delay; - } - function updatePreviousValues( uint256 streamId, uint40 snapshotTime,