test: inequality in streamed amount invariant (#315)

* test: use inequality in inv test

test: remove delay from store

* test: refactor streamed amount invariant

---------

Co-authored-by: smol-ninja <shubhamy2015@gmail.com>

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,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);
  }
 }

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");
- }
  }
 }

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,