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.

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

test: polish invariants #237

Merged
merged 1 commit into from
Sep 17, 2024
Merged

test: polish invariants #237

merged 1 commit into from
Sep 17, 2024

Conversation

smol-ninja
Copy link
Member

@smol-ninja smol-ninja commented Sep 13, 2024

Changelog

  • Sort invariants based on readme
  • Adds Protocol Invariant in withdraw function. Related Apply FREI-PI #146.

Depends on

Note

The following implementation is incorrect. See #237 (comment) for more details.

Until now, there was no way to validate the accuracy of the streamed amount. The amount streamed is only changed whenever there is a passage of time. Therefore, the new variable streamedAmount in FlowStore tracks the streamed amount through adjustTimestamp modifier.

The precision-related problems that we had been facing are mostly introduced only in the _withdraw function. So, the new invariant aims to validate that the update in the total debt matches the difference between the streamed amount and the withdrawn amount all the time.

@smol-ninja smol-ninja force-pushed the test/add-invariant branch 2 times, most recently from 8135889 to 2588c21 Compare September 13, 2024 13:55
Base automatically changed from refactor/withdraw-amount to main September 13, 2024 15:00
@smol-ninja
Copy link
Member Author

@andreivladbrg I've been trying to figure out an invariant that compares the total debt with the streamed amount. It goes like the following:

For any non-voided stream, the total debt should be equal to the total streamed amount minus the total withdrawn amount.

I chose non-voided stream because void can change total debt without any withdraw. The problem, the invariant keeps failing and I am not sure why. I can't find any error in the implementation. When you have time, I'd appreciate if you can have a look at it.

Copy link
Member

@andreivladbrg andreivladbrg left a comment

Choose a reason for hiding this comment

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

left some comments for now:

test/invariant/Flow.t.sol Outdated Show resolved Hide resolved
test/invariant/Flow.t.sol Outdated Show resolved Hide resolved
test/invariant/handlers/BaseHandler.sol Outdated Show resolved Hide resolved
// Update the streamed amounts by adding up the difference between the ongoing debt before and after.
for (uint256 i = 0; i < flowStore.lastStreamId(); ++i) {
uint256 streamId = flowStore.streamIds(i);
flowStore.updateStreamedAmount(streamId, flow.ongoingDebtOf(streamId) - initialOngoingDebts[i]);
Copy link
Member Author

Choose a reason for hiding this comment

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

This updates an incorrect streamed amount. Because it calls ongoingDebt and add it to streamedAmount very frequently, given that on every update, there will be some precision loss, then after a long time, when we compare the actual ongoing debt with the streamed amount, the different would be huge.

The actual ongoing debt = streamed amount + all those small amounts we missed in every update.

An alternate way is to store corrected time here and then use rps * (corrected time - previous stored time) to calculate streamed amount in the invariant.

Copy link
Member Author

@smol-ninja smol-ninja Sep 17, 2024

Choose a reason for hiding this comment

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

I've removed it from this PR.

@smol-ninja smol-ninja force-pushed the test/add-invariant branch 2 times, most recently from 24408e3 to 54e505b Compare September 17, 2024 15:37
@smol-ninja smol-ninja changed the base branch from main to test/vm-assume-invariant September 17, 2024 15:37
Base automatically changed from test/vm-assume-invariant to main September 17, 2024 15:42
test: invariant to compare total debt, streamed amount and withdrawn amount

test: calculate streamed amount from ongoing debt before and after

Co-authored-by: Andrei Vlad Birgaoanu <[email protected]>

test(invariant): update function calls made by stream ID
test(invariant): move depositAmount to CreateParams struct to avoid stack too deep error

Co-authored-by: Andrei Vlad Birgaoanu <[email protected]>

test: remove incorrect invariant
@smol-ninja smol-ninja changed the title test: add a new invariant for streamed amount test: polish invariants Sep 17, 2024
@smol-ninja
Copy link
Member Author

Merging this as well since the changes in this PR are minor and will be useful during testing.

@smol-ninja smol-ninja merged commit 187d57a into main Sep 17, 2024
7 checks passed
@smol-ninja smol-ninja deleted the test/add-invariant branch September 17, 2024 15:51
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants