diff --git a/test/invariant/OpenEnded.t.sol b/test/invariant/OpenEnded.t.sol index e210ad56..af3b26c7 100644 --- a/test/invariant/OpenEnded.t.sol +++ b/test/invariant/OpenEnded.t.sol @@ -71,27 +71,35 @@ contract OpenEnded_Invariant_Test is Invariant_Test { } } - function invariant_ContractBalanceGeStreamBalancesAndRemainingAmountsSum() external useCurrentTimestamp { + function invariant_ContractBalanceGeStreamBalances() external useCurrentTimestamp { uint256 contractBalance = dai.balanceOf(address(openEnded)); uint256 lastStreamId = openEndedStore.lastStreamId(); uint256 streamBalancesSumNormalized; - uint256 remainingAmountsSumNormalized; for (uint256 i = 0; i < lastStreamId; ++i) { uint256 streamId = openEndedStore.streamIds(i); streamBalancesSumNormalized += uint256(normalizeBalance(streamId)); - remainingAmountsSumNormalized += - uint256(normalizeTransferAmount(streamId, openEndedStore.remainingAmountsSum(streamId))); } assertGe( contractBalance, - streamBalancesSumNormalized + remainingAmountsSumNormalized, + streamBalancesSumNormalized, unicode"Invariant violation: contract balanceOf < Σ stream balances + remaining amounts normalized" ); } - function invariant_DepositedAmountsSumGeExtractedAmountsSumPlusRemainingAmount() external useCurrentTimestamp { + function invariant_DepositedAmountsSumGeExtractedAmountsSum() external useCurrentTimestamp { + uint256 lastStreamId = openEndedStore.lastStreamId(); + for (uint256 i = 0; i < lastStreamId; ++i) { + uint256 streamId = openEndedStore.streamIds(i); + + assertGe( + openEndedStore.depositedAmounts(streamId), + openEndedStore.extractedAmounts(streamId), + "Invariant violation: deposited amount < extracted amount" + ); + } + uint256 streamDepositedAmountsSum = openEndedStore.streamDepositedAmountsSum(); uint256 streamExtractedAmountsSum = openEndedStore.streamExtractedAmountsSum(); @@ -102,6 +110,20 @@ contract OpenEnded_Invariant_Test is Invariant_Test { ); } + function invariant_Debt_WithdrawableAmountEqBalance() external useCurrentTimestamp { + uint256 lastStreamId = openEndedStore.lastStreamId(); + for (uint256 i = 0; i < lastStreamId; ++i) { + uint256 streamId = openEndedStore.streamIds(i); + if (openEnded.streamDebtOf(streamId) > 0) { + assertEq( + openEnded.withdrawableAmountOf(streamId), + openEnded.getBalance(streamId), + "Invariant violation: withdrawable amount != balance" + ); + } + } + } + function invariant_NextStreamId() external useCurrentTimestamp { uint256 lastStreamId = openEndedStore.lastStreamId(); for (uint256 i = 0; i < lastStreamId; ++i) { @@ -110,98 +132,95 @@ contract OpenEnded_Invariant_Test is Invariant_Test { } } - function invariant_StreamBalanceEqWithdrawableAmountPlusRefundableAmountMinusRemainingAmount() - external - useCurrentTimestamp - { + function invariant_DepositAmountsSumGeExtractedAmountsSum() external useCurrentTimestamp { + uint256 streamDepositedAmountsSum = openEndedStore.streamDepositedAmountsSum(); + uint256 streamExtractedAmountsSum = openEndedStore.streamExtractedAmountsSum(); + + assertGe( + streamDepositedAmountsSum, + streamExtractedAmountsSum, + "Invariant violation: stream deposited amounts sum < stream extracted amounts sum" + ); + } + + function invariant_NoDebt_StreamedPaused_WithdrawableAmountEqRemainingAmount() external useCurrentTimestamp { uint256 lastStreamId = openEndedStore.lastStreamId(); for (uint256 i = 0; i < lastStreamId; ++i) { uint256 streamId = openEndedStore.streamIds(i); - if (!openEnded.isPaused(streamId)) { + if (openEnded.isPaused(streamId) && openEnded.streamDebtOf(streamId) == 0) { assertEq( - openEnded.getBalance(streamId), - openEnded.withdrawableAmountOf(streamId) + openEnded.refundableAmountOf(streamId) - - openEnded.getRemainingAmount(streamId), - "Invariant violation: stream balance != withdrawable amount + refundable amount - remaining amount" + openEnded.withdrawableAmountOf(streamId), + openEnded.getRemainingAmount(streamId), + "Invariant violation: paused stream withdrawable amount != remaining amount" ); } } } - function invariant_StreamBalanceGeRefundableAmount() external useCurrentTimestamp { + function invariant_NoDebt_WithdrawableAmountEqStreamedAmountPlusRemainingAmount() external useCurrentTimestamp { uint256 lastStreamId = openEndedStore.lastStreamId(); for (uint256 i = 0; i < lastStreamId; ++i) { uint256 streamId = openEndedStore.streamIds(i); - if (!openEnded.isPaused(streamId)) { - assertGe( - openEnded.getBalance(streamId), - openEnded.refundableAmountOf(streamId), - "Invariant violation: stream balance < refundable amount" + if (!openEnded.isPaused(streamId) && openEnded.streamDebtOf(streamId) == 0) { + assertEq( + openEnded.withdrawableAmountOf(streamId), + openEnded.streamedAmountOf(streamId) + openEnded.getRemainingAmount(streamId), + "Invariant violation: withdrawable amount != streamed amount + remaining amount" ); } } } - function invariatn_StreamPaused_BalanceZero() external useCurrentTimestamp { + function invariant_StreamBalanceEqWithdrawableAmountPlusRefundableAmount() external useCurrentTimestamp { uint256 lastStreamId = openEndedStore.lastStreamId(); for (uint256 i = 0; i < lastStreamId; ++i) { uint256 streamId = openEndedStore.streamIds(i); - if (openEnded.isPaused(streamId)) { - assertEq( - openEnded.getBalance(streamId), 0, "Invariant violation: paused stream with a non-zero balance" - ); - } + assertEq( + openEnded.getBalance(streamId), + openEnded.withdrawableAmountOf(streamId) + openEnded.refundableAmountOf(streamId), + "Invariant violation: stream balance != withdrawable amount + refundable amount" + ); } } - function invariant_StreamPaused_RatePerSecondZero() external useCurrentTimestamp { + function invariant_StreamBalanceGeRefundableAmount() external useCurrentTimestamp { uint256 lastStreamId = openEndedStore.lastStreamId(); for (uint256 i = 0; i < lastStreamId; ++i) { uint256 streamId = openEndedStore.streamIds(i); - if (openEnded.isPaused(streamId)) { - assertEq( - openEnded.getRatePerSecond(streamId), - 0, - "Invariant violation: paused stream with a non-zero rate per second" + if (!openEnded.isPaused(streamId)) { + assertGe( + openEnded.getBalance(streamId), + openEnded.refundableAmountOf(streamId), + "Invariant violation: stream balance < refundable amount" ); } } } - function invariant_StreamedPaused_WithdrawableAmountEqRemainingAmount() external useCurrentTimestamp { + function invariant_StreamBalanceGeWithdrawableAmount() external useCurrentTimestamp { uint256 lastStreamId = openEndedStore.lastStreamId(); for (uint256 i = 0; i < lastStreamId; ++i) { uint256 streamId = openEndedStore.streamIds(i); - if (openEnded.isPaused(streamId)) { - assertEq( - openEnded.withdrawableAmountOf(streamId), - openEnded.getRemainingAmount(streamId), - "Invariant violation: paused stream withdrawable amount != remaining amount" - ); - } + + assertGe( + openEnded.getBalance(streamId), + openEnded.withdrawableAmountOf(streamId), + "Invariant violation: withdrawable amount <= balance" + ); } } - /// @dev The invariant is: withdrawable amount = min(balance, streamed amount) + remaining amount - /// This includes both paused and non-paused streams. - function invariant_WithdrawableAmount() external useCurrentTimestamp { + function invariant_StreamPaused_RatePerSecondZero() external useCurrentTimestamp { uint256 lastStreamId = openEndedStore.lastStreamId(); for (uint256 i = 0; i < lastStreamId; ++i) { uint256 streamId = openEndedStore.streamIds(i); - uint128 balance = openEnded.getBalance(streamId); - uint128 streamedAmount = 0; - - if (!openEnded.isPaused(streamId)) { - streamedAmount = openEnded.streamedAmountOf(streamId); + if (openEnded.isPaused(streamId)) { + assertEq( + openEnded.getRatePerSecond(streamId), + 0, + "Invariant violation: paused stream with a non-zero rate per second" + ); } - - uint128 balanceOrStreamedAmount = balance > streamedAmount ? streamedAmount : balance; - - assertEq( - openEnded.withdrawableAmountOf(streamId), - balanceOrStreamedAmount + openEnded.getRemainingAmount(streamId), - "Invariant violation: withdrawable amount != min(balance, streamed amount) + remaining amount" - ); } } } diff --git a/test/invariant/handlers/OpenEndedCreateHandler.sol b/test/invariant/handlers/OpenEndedCreateHandler.sol index bfa5f8f3..28500607 100644 --- a/test/invariant/handlers/OpenEndedCreateHandler.sol +++ b/test/invariant/handlers/OpenEndedCreateHandler.sol @@ -70,7 +70,7 @@ contract OpenEndedCreateHandler is BaseHandler { openEnded.create(params.sender, params.recipient, params.ratePerSecond, asset, params.isTransferable); // Store the stream id. - openEndedStore.pushStreamId(streamId, params.sender, params.recipient); + openEndedStore.pushStreamId(streamId, params.sender, params.recipient, openEnded.getLastTimeUpdate(streamId)); } function createAndDeposit( @@ -104,9 +104,9 @@ contract OpenEndedCreateHandler is BaseHandler { ); // Store the stream id. - openEndedStore.pushStreamId(streamId, params.sender, params.recipient); + openEndedStore.pushStreamId(streamId, params.sender, params.recipient, openEnded.getLastTimeUpdate(streamId)); // Store the deposited amount. - openEndedStore.updateStreamDepositedAmountsSum(depositAmount); + openEndedStore.updateStreamDepositedAmountsSum(streamId, depositAmount); } } diff --git a/test/invariant/handlers/OpenEndedHandler.sol b/test/invariant/handlers/OpenEndedHandler.sol index c49c7330..cb652a54 100644 --- a/test/invariant/handlers/OpenEndedHandler.sol +++ b/test/invariant/handlers/OpenEndedHandler.sol @@ -99,16 +99,8 @@ contract OpenEndedHandler is BaseHandler { newRatePerSecond += 1; } - uint128 balance = openEnded.getBalance(currentStreamId); - uint128 streamedAmount = openEnded.streamedAmountOf(currentStreamId); - - uint128 remainingAmount = balance > streamedAmount ? streamedAmount : balance; - // Adjust the rate per second. openEnded.adjustRatePerSecond(currentStreamId, newRatePerSecond); - - // Store the remaining amount. - openEndedStore.sumRemainingAmount(currentStreamId, remainingAmount); } function pause( @@ -126,20 +118,8 @@ contract OpenEndedHandler is BaseHandler { return; } - uint128 balance = openEnded.getBalance(currentStreamId); - uint128 senderAmount = openEnded.refundableAmountOf(currentStreamId); - uint128 streamedAmount = openEnded.streamedAmountOf(currentStreamId); - - uint128 remainingAmount = balance > streamedAmount ? streamedAmount : balance; - // Pause the stream. openEnded.pause(currentStreamId); - - // Store the extracted amount. - openEndedStore.updateStreamExtractedAmountsSum(senderAmount); - - // Store the remaining amount. - openEndedStore.sumRemainingAmount(currentStreamId, remainingAmount); } function deposit( @@ -151,11 +131,6 @@ contract OpenEndedHandler is BaseHandler { useFuzzedStream(streamIndexSeed) useFuzzedStreamSender { - // Only non paused streams can be deposited. - if (openEnded.isPaused(currentStreamId)) { - return; - } - // Bound the deposit amount. depositAmount = uint128(_bound(depositAmount, 100e18, 1_000_000_000e18)); @@ -170,7 +145,7 @@ contract OpenEndedHandler is BaseHandler { openEnded.deposit({ streamId: currentStreamId, amount: depositAmount }); // Store the deposited amount. - openEndedStore.updateStreamDepositedAmountsSum(depositAmount); + openEndedStore.updateStreamDepositedAmountsSum(currentStreamId, depositAmount); } function refundFromStream( @@ -184,11 +159,6 @@ contract OpenEndedHandler is BaseHandler { useFuzzedStream(streamIndexSeed) useFuzzedStreamSender { - // Only non paused streams can be refunded. - if (openEnded.isPaused(currentStreamId)) { - return; - } - // The protocol doesn't allow zero refund amounts. uint128 refundableAmount = openEnded.refundableAmountOf(currentStreamId); if (refundableAmount == 0) { @@ -202,7 +172,7 @@ contract OpenEndedHandler is BaseHandler { openEnded.refundFromStream(currentStreamId, refundableAmount); // Store the deposited amount. - openEndedStore.updateStreamExtractedAmountsSum(refundAmount); + openEndedStore.updateStreamExtractedAmountsSum(currentStreamId, refundAmount); } function restartStream( @@ -235,7 +205,7 @@ contract OpenEndedHandler is BaseHandler { uint128 depositAmount ) external - instrument("restartStream") + instrument("restartStreamAndDeposit") adjustTimestamp(timeJumpSeed) useFuzzedStream(streamIndexSeed) useFuzzedStreamSender @@ -260,7 +230,7 @@ contract OpenEndedHandler is BaseHandler { openEnded.restartStreamAndDeposit(currentStreamId, ratePerSecond, depositAmount); // Store the deposited amount. - openEndedStore.updateStreamDepositedAmountsSum(depositAmount); + openEndedStore.updateStreamDepositedAmountsSum(currentStreamId, depositAmount); } function withdrawAt( @@ -295,16 +265,12 @@ contract OpenEndedHandler is BaseHandler { to = currentRecipient; } - uint128 remainingAmount = openEnded.getRemainingAmount(currentStreamId); uint128 withdrawAmount = openEnded.withdrawableAmountOf(currentStreamId, time); // Withdraw from the stream. openEnded.withdrawAt({ streamId: currentStreamId, to: to, time: time }); // Store the extracted amount. - openEndedStore.updateStreamExtractedAmountsSum(withdrawAmount); - - // Remove the remaining amount. - openEndedStore.subtractRemainingAmount(currentStreamId, remainingAmount); + openEndedStore.updateStreamExtractedAmountsSum(currentStreamId, withdrawAmount); } } diff --git a/test/invariant/stores/OpenEndedStore.sol b/test/invariant/stores/OpenEndedStore.sol index c711b030..fde337b0 100644 --- a/test/invariant/stores/OpenEndedStore.sol +++ b/test/invariant/stores/OpenEndedStore.sol @@ -10,7 +10,9 @@ contract OpenEndedStore { uint256 public lastStreamId; mapping(uint256 streamId => address recipient) public recipients; mapping(uint256 streamId => address sender) public senders; - mapping(uint256 streamId => uint128 remainingAmount) public remainingAmountsSum; + mapping(uint256 streamId => uint40 firstTimeUpdate) public firstTimeUpdates; + mapping(uint256 streamId => uint128 depositedAmount) public depositedAmounts; + mapping(uint256 streamId => uint128 extractedAmount) public extractedAmounts; uint256[] public streamIds; uint256 public streamDepositedAmountsSum; uint256 public streamExtractedAmountsSum; @@ -19,29 +21,24 @@ contract OpenEndedStore { HELPERS //////////////////////////////////////////////////////////////////////////*/ - function pushStreamId(uint256 streamId, address sender, address recipient) external { + function pushStreamId(uint256 streamId, address sender, address recipient, uint40 firstTimeUpdate) external { // Store the stream ids, the senders, and the recipients. streamIds.push(streamId); senders[streamId] = sender; recipients[streamId] = recipient; + firstTimeUpdates[streamId] = firstTimeUpdate; // Update the last stream id. lastStreamId = streamId; } - function sumRemainingAmount(uint256 streamId, uint128 amount) external { - remainingAmountsSum[streamId] += amount; - } - - function subtractRemainingAmount(uint256 streamId, uint128 amount) external { - remainingAmountsSum[streamId] -= amount; - } - - function updateStreamDepositedAmountsSum(uint256 amount) external { + function updateStreamDepositedAmountsSum(uint256 streamId, uint128 amount) external { + depositedAmounts[streamId] += amount; streamDepositedAmountsSum += amount; } - function updateStreamExtractedAmountsSum(uint256 amount) external { + function updateStreamExtractedAmountsSum(uint256 streamId, uint128 amount) external { + extractedAmounts[streamId] += amount; streamExtractedAmountsSum += amount; } }