Skip to content

Commit

Permalink
test: add a new invariant for streamed amount
Browse files Browse the repository at this point in the history
  • Loading branch information
@smol-ninja
smol-ninja committed Sep 13, 2024
1 parent 0c7a3b1 commit 8135889
Show file tree
Hide file tree
Showing 3 changed files with 55 additions and 46 deletions.
18 changes: 9 additions & 9 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -157,26 +157,26 @@ Currently, it's not possible to address this precision problem entirely.
`flow.collectProtocolRevenue` handlers. In real life, someone can transfer tokens to the contract or admin can
withdraw revenue from the contract.

3. for any stream, if $ud > 0 \implies cd = bal$
3. snapshot time should never decrease

4. if $rps \gt 0$ and no deposits are made $\implies \frac{d(ud)}{dt} \ge 0$
4. for any stream, if $ud > 0 \implies cd = bal$

5. if $rps \gt 0$, and no withdraw is made $\implies \frac{d(td)}{dt} \ge 0$
5. if $rps \gt 0$ and no deposits are made $\implies \frac{d(ud)}{dt} \ge 0$

6. for any stream, sum of deposited amounts $\ge$ sum of withdrawn amounts + sum of refunded
6. if $rps \gt 0$, and no withdraw is made $\implies \frac{d(td)}{dt} \ge 0$

7. sum of all deposited amounts $\ge$ sum of all withdrawn amounts + sum of all refunded
7. for any stream, sum of deposited amounts $\ge$ sum of withdrawn amounts + sum of refunded

8. next stream id = current stream id + 1
8. sum of all deposited amounts $\ge$ sum of all withdrawn amounts + sum of all refunded

9. if $ud = 0$ and $isPaused = true \implies cd = sa$
9. next stream id = current stream id + 1

10. if $ud = 0$ and $isPaused = false \implies cd = sa + oa$
10. if $ud = 0$ \implies cd = td$

11. $bal = ra + cd$

12. if $isPaused = true \implies rps = 0$

13. if $isVoided = true \implies isPaused = true$, $ra = 0$ and $ud = 0$

14. snapshot time should never decrease
14. For a given stream, if $δ(rps) = 0$ $\implies td = streamedAmount - totalWithdrawn$
3 changes: 3 additions & 0 deletions src/SablierFlow.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -824,6 +824,9 @@ contract SablierFlow is
// Interaction: perform the ERC-20 transfer.
token.safeTransfer({ to: to, value: amount });

// Protocol Invariant: the difference in total debt should be equal to the difference in the stream balance.
assert(totalDebt - _totalDebtOf(streamId) == balance - _streams[streamId].balance);

// Log the withdrawal.
emit ISablierFlow.WithdrawFromFlowStream({
streamId: streamId,
Expand Down
80 changes: 43 additions & 37 deletions test/invariant/Flow.t.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -131,7 +131,7 @@ contract Flow_Invariant_Test is Base_Test {
}

/// @dev If rps > 0, and no additional deposits are made, then the uncovered debt should never decrease.
function invariant_UncoveredDebtGt0_RpsGt0_UncoveredDebtIncrease() external view {
function invariant_RpsGt0_UncoveredDebtGt0_UncoveredDebtIncrease() external view {
uint256 lastStreamId = flowStore.lastStreamId();
for (uint256 i = 0; i < lastStreamId; ++i) {
uint256 streamId = flowStore.streamIds(i);
Expand All @@ -145,6 +145,21 @@ contract Flow_Invariant_Test is Base_Test {
}
}

/// @dev If rps > 0, no withdraw is made, the total debt should always increase.
function invariant_RpsGt0_TotalDebtAlwaysIncreases() external view {
uint256 lastStreamId = flowStore.lastStreamId();
for (uint256 i = 0; i < lastStreamId; ++i) {
uint256 streamId = flowStore.streamIds(i);
if (flow.getRatePerSecond(streamId).unwrap() != 0 && flowHandler.calls("withdraw") == 0) {
assertGe(
flow.totalDebtOf(streamId),
flowHandler.previousTotalDebtOf(streamId),
"Invariant violation: total debt should be monotonically increasing"
);
}
}
}

/// @dev For any stream, the sum of all deposited amounts should always be greater than or equal to the sum of all
/// withdrawn and refunded amounts.
function invariant_InflowGeOutflow() external view {
Expand Down Expand Up @@ -183,48 +198,17 @@ contract Flow_Invariant_Test is Base_Test {
}
}

/// @dev If there is no uncovered debt and the stream is paused, the covered debt should always be equal to
/// the snapshot debt.
function invariant_NoUncoveredDebt_StreamedPaused_CoveredDebtEqSnapshotAmount() external view {
uint256 lastStreamId = flowStore.lastStreamId();
for (uint256 i = 0; i < lastStreamId; ++i) {
uint256 streamId = flowStore.streamIds(i);
if (flow.isPaused(streamId) && flow.uncoveredDebtOf(streamId) == 0) {
assertEq(
flow.coveredDebtOf(streamId),
flow.getSnapshotDebt(streamId),
"Invariant violation: paused stream covered debt != snapshot debt"
);
}
}
}

/// @dev If there is no uncovered debt and the stream is not paused, the covered debt should always be equal
/// to the sum of snapshot debt and ongoing debt.
function invariant_NoDebt_CoveredDebtEqOngoingDebtPlusSnapshotAmount() external view {
/// @dev If there is no uncovered debt, the covered debt should always be equal to
/// the total debt.
function invariant_NoUncoveredDebt_StreamedPaused_CoveredDebtEqTotalDebt() external view {
uint256 lastStreamId = flowStore.lastStreamId();
for (uint256 i = 0; i < lastStreamId; ++i) {
uint256 streamId = flowStore.streamIds(i);
if (!flow.isPaused(streamId) && flow.uncoveredDebtOf(streamId) == 0) {
if (flow.uncoveredDebtOf(streamId) == 0) {
assertEq(
flow.coveredDebtOf(streamId),
flow.ongoingDebtOf(streamId) + flow.getSnapshotDebt(streamId),
"Invariant violation: covered debt != ongoing debt + snapshot debt"
);
}
}
}

/// @dev If rps > 0, no withdraw is made, the total debt should always increase.
function invariant_RpsGt0_TotalDebtAlwaysIncreases() external view {
uint256 lastStreamId = flowStore.lastStreamId();
for (uint256 i = 0; i < lastStreamId; ++i) {
uint256 streamId = flowStore.streamIds(i);
if (flow.getRatePerSecond(streamId).unwrap() != 0 && flowHandler.calls("withdraw") == 0) {
assertGe(
flow.totalDebtOf(streamId),
flowHandler.previousTotalDebtOf(streamId),
"Invariant violation: total debt should be monotonically increasing"
"Invariant violation: paused stream covered debt != snapshot debt"
);
}
}
Expand Down Expand Up @@ -276,4 +260,26 @@ 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
/// 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
) { }
assertEq(
flow.totalDebtOf(streamId),
streamedAmount - flowStore.withdrawnAmounts(streamId),
"Invariant violation: total debt != streamed amount - withdrawn amount"
);
}
}
}

0 comments on commit 8135889

Please sign in to comment.