Skip to content

Commit

Permalink
test: update invariant tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@andreivladbrg @smol-ninja
andreivladbrg authored and smol-ninja committed May 22, 2024
1 parent 6aa9680 commit 119918d
Show file tree
Hide file tree
Showing 4 changed files with 93 additions and 111 deletions.
133 changes: 76 additions & 57 deletions test/invariant/OpenEnded.t.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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();

Expand All @@ -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) {
Expand All @@ -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"
);
}
}
}
6 changes: 3 additions & 3 deletions test/invariant/handlers/OpenEndedCreateHandler.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand Down Expand Up @@ -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);
}
}
44 changes: 5 additions & 39 deletions test/invariant/handlers/OpenEndedHandler.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand All @@ -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(
Expand All @@ -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));

Expand All @@ -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(
Expand All @@ -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) {
Expand All @@ -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(
Expand Down Expand Up @@ -235,7 +205,7 @@ contract OpenEndedHandler is BaseHandler {
uint128 depositAmount
)
external
instrument("restartStream")
instrument("restartStreamAndDeposit")
adjustTimestamp(timeJumpSeed)
useFuzzedStream(streamIndexSeed)
useFuzzedStreamSender
Expand All @@ -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(
Expand Down Expand Up @@ -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);
}
}
21 changes: 9 additions & 12 deletions test/invariant/stores/OpenEndedStore.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;
}
}

0 comments on commit 119918d

Please sign in to comment.