Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

test: inequality in streamed amount invariant #315

Merged
merged 2 commits into from
Oct 17, 2024
Merged

test: inequality in streamed amount invariant #315

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
24bb66f
test: use inequality in inv test
andreivladbrg Oct 16, 2024
45436e9
test: refactor streamed amount invariant
smol-ninja Oct 17, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion TECHNICAL-DOC.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
51 changes: 24 additions & 27 deletions tests/invariant/Flow.t.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I wonder why is there an "Le" here? Previously, we had the following relations:

  1. $totalStreamedAmount \ge totalStreamedAmountWithDelay$
  2. $totalStreamedAmountWithDelay = totalDebt + totalWithdrawn$

Therefore from the above two, the new relation should be

  • $totalStreamedAmount \ge totalDebt + totalWithdrawn$

and not the opposite.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

45436e9

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);
}
}
12 changes: 0 additions & 12 deletions tests/invariant/handlers/FlowHandler.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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");
}

Expand Down Expand Up @@ -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);

Expand Down Expand Up @@ -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");
}
}
}
48 changes: 5 additions & 43 deletions tests/invariant/stores/FlowStore.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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,
Expand Down
Loading