Skip to content

Commit

Permalink
test: add invariant_DebtGt0_RpsGt0_DebtIncrease (#129)
Browse files Browse the repository at this point in the history 
* test(invariant): add two new invariants
docs: update invariants in readme
test(invariant): replace extractedAmounts with refundedAmounts and withdrawnAmounts
test(invariant): add updateFlowStates modifier
test(invariant): remove restartAndDeposit
test(invariant): add natspecs over invariant tests

* docs: add 'only to recipient' note in access control

* docs: use latex only where needed

test: correct grammar in dev natspec
test: order invariants alphabetically

* docs: reorder invariants list in readme according to invariants order

* test(invariant): remove unnecessary invariants

* test: remove invariant_RpsGt0_RemainingPlusStreamedIncrease invariant

---------

Co-authored-by: andreivladbrg <andreivladbrg@gmail.com>
  • Loading branch information
@smol-ninja @andreivladbrg
smol-ninja and andreivladbrg authored May 28, 2024
1 parent 3e897f8 commit c45a6d4
Show file tree
Hide file tree
Showing 4 changed files with 102 additions and 110 deletions.
42 changes: 23 additions & 19 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -147,32 +147,36 @@ Sender address **must** be checked because there is no `ERC20` transfer in `_cre

### Invariants:

_wa ≤ bal_
1. For any stream, $\ ltu \le now $

_if(debt = 0) then wa = sa + ra_
2. For a given asset, $\sum$ stream balances normalized to asset decimal $\leq$ asset.balanceOf(SablierFlow)

_if(debt = 0 && isPaused = true) then wa = ra_
3. For any stream, if $debt > 0 \implies wa = bal$

_if(debt > 0) then wa = bal_
4. if $rps \gt 0$ and no deposits are made $\implies$ debt should never decrease

_bal = sum of deposits - sum of withdrawals_
5. For any stream, sum of deposited amounts $\ge$ sum of withdrawn amounts + sum of refunded

_sum of withdrawn amounts ≤ sum of deposits_
6. sum of all deposited amounts $\ge$ sum of all withdrawn amounts + sum of all refunded

_sum of stream balances normalized to asset decimals ≤ asset.balanceOf(SablierFlow)_
7. next stream id = current stream id + 1

_ltu ≤ now_
8. if $debt = 0$ and $isPaused = true \implies wa = ra$

_if(isPaused = true) then rps = 0_
9. if $debt = 0$ and $isPaused = false \implies wa = ra + sa$

### Actions Access Control:
10. $bal = rfa + wa$

| Action | Sender | Recipient | Operator(s) | Unknown User |
| ------------------- | :----: | :-------: | :---------: | :--------------------: |
| AdjustRatePerSecond | ✅ | ❌ | ❌ | ❌ |
| Deposit | ✅ | ✅ | ✅ | ✅ |
| Refund | ✅ | ❌ | ❌ | ❌ |
| Restart | ✅ | ❌ | ❌ | ❌ |
| Pause | ✅ | ❌ | ❌ | ❌ |
| Transfer NFT | ❌ | ✅ | ✅ | ❌ |
| Withdraw | ✅ | ✅ | ✅ | ✅ (only to Recipient) |
11. if $isPaused = true \implies rps = 0$

### Access Control:

| Action | Sender | Recipient | Operator(s) | Unknown User |
| ------------------- | :--------------------: | :-------: | :---------: | :--------------------: |
| AdjustRatePerSecond | ✅ | ❌ | ❌ | ❌ |
| Deposit | ✅ | ✅ | ✅ | ✅ |
| Refund | ✅ | ❌ | ❌ | ❌ |
| Restart | ✅ | ❌ | ❌ | ❌ |
| Pause | ✅ | ❌ | ❌ | ❌ |
| Transfer NFT | ❌ | ✅ | ✅ | ❌ |
| Withdraw | ✅ (only to Recipient) | ✅ | ✅ | ✅ (only to Recipient) |
85 changes: 39 additions & 46 deletions test/invariant/Flow.t.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,7 @@ contract Flow_Invariant_Test is Invariant_Test {
INVARIANTS
//////////////////////////////////////////////////////////////////////////*/

/// @dev For any stream, `lastTimeUpdate` should never exceed the current block timestamp.
function invariant_BlockTimestampGeLastTimeUpdate() external view {
uint256 lastStreamId = flowStore.lastStreamId();
for (uint256 i = 0; i < lastStreamId; ++i) {
Expand All @@ -61,8 +62,8 @@ contract Flow_Invariant_Test is Invariant_Test {
}
}

/// @dev The sum of all stream balances for a specific asset should be less than or equal to the contract
/// `ERC20.balanceOf`.
/// @dev For a given asset, the sum of all stream balances normalized to the asset's decimal should never exceed
/// the asset balance of the flow contract.
function invariant_ContractBalanceGeStreamBalances() external view {
uint256 contractBalance = dai.balanceOf(address(flow));

Expand All @@ -76,10 +77,11 @@ contract Flow_Invariant_Test is Invariant_Test {
assertGe(
contractBalance,
streamBalancesSumNormalized,
unicode"Invariant violation: contract balanceOf < Σ stream balances"
unicode"Invariant violation: contract balance < Σ stream balances"
);
}

/// @dev For any stream, if debt > 0, then the withdrawable amount should equal the stream balance.
function invariant_Debt_WithdrawableAmountEqBalance() external view {
uint256 lastStreamId = flowStore.lastStreamId();
for (uint256 i = 0; i < lastStreamId; ++i) {
Expand All @@ -94,47 +96,61 @@ contract Flow_Invariant_Test is Invariant_Test {
}
}

function invariant_DepositAmountsSumGeExtractedAmountsSum() external view {
uint256 streamDepositedAmountsSum = flowStore.streamDepositedAmountsSum();
uint256 streamExtractedAmountsSum = flowStore.streamExtractedAmountsSum();

assertGe(
streamDepositedAmountsSum,
streamExtractedAmountsSum,
"Invariant violation: stream deposited amounts sum < stream extracted amounts sum"
);
/// @dev If rps > 0, and no additional deposits are made, then the debt should never decrease.
function invariant_DebtGt0_RpsGt0_DebtIncrease() external view {
uint256 lastStreamId = flowStore.lastStreamId();
for (uint256 i = 0; i < lastStreamId; ++i) {
uint256 streamId = flowStore.streamIds(i);
if (flow.getRatePerSecond(streamId) > 0 && flowHandler.calls("deposit") == 0) {
assertGe(
flow.streamDebtOf(streamId),
flowHandler.previousDebtOf(streamId),
"Invariant violation: debt should never decrease"
);
}
}
}

function invariant_DepositedAmountsSumGeExtractedAmountsSum() external view {
/// @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 {
uint256 lastStreamId = flowStore.lastStreamId();
for (uint256 i = 0; i < lastStreamId; ++i) {
uint256 streamId = flowStore.streamIds(i);

assertGe(
flowStore.depositedAmounts(streamId),
flowStore.extractedAmounts(streamId),
"Invariant violation: deposited amount < extracted amount"
flowStore.refundedAmounts(streamId) + flowStore.withdrawnAmounts(streamId),
"Invariant violation: deposited amount < refunded amount + withdrawn amount"
);
}
}

/// @dev The sum of all deposited amounts should always be greater than or equal to the sum of withdrawn and
/// refunded amounts.
function invariant_InflowsSumGeOutflowsSum() external view {
uint256 streamDepositedAmountsSum = flowStore.streamDepositedAmountsSum();
uint256 streamExtractedAmountsSum = flowStore.streamExtractedAmountsSum();
uint256 streamRefundedAmountsSum = flowStore.streamRefundedAmountsSum();
uint256 streamWithdrawnAmountsSum = flowStore.streamWithdrawnAmountsSum();

assertGe(
streamDepositedAmountsSum,
streamExtractedAmountsSum,
"Invariant violation: stream deposited amounts sum < stream extracted amounts sum"
streamRefundedAmountsSum + streamWithdrawnAmountsSum,
"Invariant violation: stream deposited amounts sum < refunded amounts sum + withdrawn amounts sum"
);
}

/// @dev The next stream ID should always be incremented by 1.
function invariant_NextStreamId() external view {
uint256 lastStreamId = flowStore.lastStreamId();
for (uint256 i = 0; i < lastStreamId; ++i) {
uint256 nextStreamId = flow.nextStreamId();
assertEq(nextStreamId, lastStreamId + 1, "Invariant violation: next stream id not incremented");
assertEq(nextStreamId, lastStreamId + 1, "Invariant violation: next stream ID not incremented");
}
}

/// @dev If there is no debt and the stream is paused, the withdrawable amount should always be equal to the
/// remaining amount.
function invariant_NoDebt_StreamedPaused_WithdrawableAmountEqRemainingAmount() external view {
uint256 lastStreamId = flowStore.lastStreamId();
for (uint256 i = 0; i < lastStreamId; ++i) {
Expand All @@ -149,6 +165,8 @@ contract Flow_Invariant_Test is Invariant_Test {
}
}

/// @dev If there is no debt and the stream is not paused, the withdrawable amount should always be equal to the
/// remaining amount plus the streamed amount.
function invariant_NoDebt_WithdrawableAmountEqStreamedAmountPlusRemainingAmount() external view {
uint256 lastStreamId = flowStore.lastStreamId();
for (uint256 i = 0; i < lastStreamId; ++i) {
Expand All @@ -163,6 +181,7 @@ contract Flow_Invariant_Test is Invariant_Test {
}
}

/// @dev The stream balance should be equal to the sum of the withdrawable amount and the refundable amount.
function invariant_StreamBalanceEqWithdrawableAmountPlusRefundableAmount() external view {
uint256 lastStreamId = flowStore.lastStreamId();
for (uint256 i = 0; i < lastStreamId; ++i) {
Expand All @@ -175,33 +194,7 @@ contract Flow_Invariant_Test is Invariant_Test {
}
}

function invariant_StreamBalanceGeRefundableAmount() external view {
uint256 lastStreamId = flowStore.lastStreamId();
for (uint256 i = 0; i < lastStreamId; ++i) {
uint256 streamId = flowStore.streamIds(i);
if (!flow.isPaused(streamId)) {
assertGe(
flow.getBalance(streamId),
flow.refundableAmountOf(streamId),
"Invariant violation: stream balance < refundable amount"
);
}
}
}

function invariant_StreamBalanceGeWithdrawableAmount() external view {
uint256 lastStreamId = flowStore.lastStreamId();
for (uint256 i = 0; i < lastStreamId; ++i) {
uint256 streamId = flowStore.streamIds(i);

assertGe(
flow.getBalance(streamId),
flow.withdrawableAmountOf(streamId),
"Invariant violation: withdrawable amount <= balance"
);
}
}

/// @dev If the stream is paused, then the rate per second should always be zero.
function invariant_StreamPaused_RatePerSecondZero() external view {
uint256 lastStreamId = flowStore.lastStreamId();
for (uint256 i = 0; i < lastStreamId; ++i) {
Expand Down
68 changes: 28 additions & 40 deletions test/invariant/handlers/FlowHandler.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,11 @@ contract FlowHandler is BaseHandler {
address internal currentSender;
uint256 internal currentStreamId;

/// @dev Debt, remaining and streamed amount mapped to each stream id.
mapping(uint256 streamId => uint128 amount) public previousDebtOf;
mapping(uint256 streamId => uint128 amount) public lastRemainingAmountOf;
mapping(uint256 streamId => uint128 amount) public lastStreamedAmountOf;

/*//////////////////////////////////////////////////////////////////////////
CONSTRUCTOR
//////////////////////////////////////////////////////////////////////////*/
Expand All @@ -37,6 +42,18 @@ contract FlowHandler is BaseHandler {
MODIFIERS
//////////////////////////////////////////////////////////////////////////*/

/// @dev Updates the states of Flow stream.
modifier updateFlowStates() {
previousDebtOf[currentStreamId] = flow.streamDebtOf(currentStreamId);
lastRemainingAmountOf[currentStreamId] = flow.getRemainingAmount(currentStreamId);
if (!flow.isPaused(currentStreamId)) {
lastStreamedAmountOf[currentStreamId] = flow.streamedAmountOf(currentStreamId);
} else {
lastStreamedAmountOf[currentStreamId] = 0;
}
_;
}

/// @dev Picks a random stream from the store.
/// @param streamIndexSeed A fuzzed value needed for picking the random stream.
modifier useFuzzedStream(uint256 streamIndexSeed) {
Expand Down Expand Up @@ -77,6 +94,7 @@ contract FlowHandler is BaseHandler {
adjustTimestamp(timeJumpSeed)
useFuzzedStream(streamIndexSeed)
useFuzzedStreamSender
updateFlowStates
{
// Only non paused streams can have their rate per second adjusted.
if (flow.isPaused(currentStreamId)) {
Expand Down Expand Up @@ -104,6 +122,7 @@ contract FlowHandler is BaseHandler {
adjustTimestamp(timeJumpSeed)
useFuzzedStream(streamIndexSeed)
useFuzzedStreamSender
updateFlowStates
{
// Paused streams cannot be paused again.
if (flow.isPaused(currentStreamId)) {
Expand All @@ -124,6 +143,7 @@ contract FlowHandler is BaseHandler {
adjustTimestamp(timeJumpSeed)
useFuzzedStream(streamIndexSeed)
useFuzzedStreamSender
updateFlowStates
{
// Bound the deposit amount.
depositAmount = uint128(_bound(depositAmount, 100e18, 1_000_000_000e18));
Expand All @@ -138,7 +158,7 @@ contract FlowHandler is BaseHandler {
// Deposit into the stream.
flow.deposit({ streamId: currentStreamId, amount: depositAmount });

// Store the deposited amount.
// Update the deposited amount.
flowStore.updateStreamDepositedAmountsSum(currentStreamId, depositAmount);
}

Expand All @@ -152,6 +172,7 @@ contract FlowHandler is BaseHandler {
adjustTimestamp(timeJumpSeed)
useFuzzedStream(streamIndexSeed)
useFuzzedStreamSender
updateFlowStates
{
uint128 refundableAmount = flow.refundableAmountOf(currentStreamId);

Expand All @@ -166,8 +187,8 @@ contract FlowHandler is BaseHandler {
// Refund from stream.
flow.refund(currentStreamId, refundAmount);

// Store the refunded amount.
flowStore.updateStreamExtractedAmountsSum(currentStreamId, refundAmount);
// Update the refunded amount.
flowStore.updateStreamRefundedAmountsSum(currentStreamId, refundAmount);
}

function restart(
Expand All @@ -180,6 +201,7 @@ contract FlowHandler is BaseHandler {
adjustTimestamp(timeJumpSeed)
useFuzzedStream(streamIndexSeed)
useFuzzedStreamSender
updateFlowStates
{
// Only paused streams can be restarted.
if (!flow.isPaused(currentStreamId)) {
Expand All @@ -193,41 +215,6 @@ contract FlowHandler is BaseHandler {
flow.restart(currentStreamId, ratePerSecond);
}

function restartAndDeposit(
uint256 timeJumpSeed,
uint256 streamIndexSeed,
uint128 ratePerSecond,
uint128 depositAmount
)
external
instrument("restartAndDeposit")
adjustTimestamp(timeJumpSeed)
useFuzzedStream(streamIndexSeed)
useFuzzedStreamSender
{
// Only paused streams can be restarted.
if (!flow.isPaused(currentStreamId)) {
return;
}

// Bound the stream parameter.
ratePerSecond = uint128(_bound(ratePerSecond, 0.0001e18, 1e18));
depositAmount = uint128(_bound(depositAmount, 100e18, 1_000_000_000e18));

// Mint enough assets to the Sender.
address sender = flowStore.senders(currentStreamId);
deal({ token: address(asset), to: sender, give: asset.balanceOf(sender) + depositAmount });

// Approve {SablierFlow} to spend the assets.
asset.approve({ spender: address(flow), value: depositAmount });

// Restart the stream.
flow.restartAndDeposit(currentStreamId, ratePerSecond, depositAmount);

// Store the deposited amount.
flowStore.updateStreamDepositedAmountsSum(currentStreamId, depositAmount);
}

function withdrawAt(
uint256 timeJumpSeed,
uint256 streamIndexSeed,
Expand All @@ -239,6 +226,7 @@ contract FlowHandler is BaseHandler {
adjustTimestamp(timeJumpSeed)
useFuzzedStream(streamIndexSeed)
useFuzzedStreamRecipient
updateFlowStates
{
// The protocol doesn't allow the withdrawal address to be the zero address.
if (to == address(0)) {
Expand All @@ -265,7 +253,7 @@ contract FlowHandler is BaseHandler {
// Withdraw from the stream.
flow.withdrawAt({ streamId: currentStreamId, to: to, time: time });

// Store the extracted amount.
flowStore.updateStreamExtractedAmountsSum(currentStreamId, withdrawAmount);
// Update the withdrawn amount.
flowStore.updateStreamWithdrawnAmountsSum(currentStreamId, withdrawAmount);
}
}
Loading

0 comments on commit c45a6d4

Please sign in to comment.