test(invariant): amount owed should never decrease in absence of a `withdraw`

[smol-ninja]

Changelog

• Adds a new invariant: invariant_AmountOwedAlwaysIncrease. See comment for more info.
• Increase number of invariant runs in CI
• Remove unused variables from FlowHandler.sol
• Add passTime in FlowHandler.sol: a function that does nothing but warp the time into the future. This is important to simulate the time dependent behaviour of recent-amount.

[andreivladbrg]

Q: Why did you move adjustTimestamp after updateFlowHandlerStates (fka updateFlowStates)? A: That's because we are interested into snapshotting flow states before the function is called by the invariant. The function call includes time warp, that's why its a good idea to take the snapshot before time is adjusted.

I think this is incorrect.

If we update the state before we warp the time, it would cause discrepancies between the actual state in the flow contract and the handler state. For example, when adjustRatePerSecond is called:

• The updateState modifier is called at t0, where the recent amount is, let’s say 100, and with this amount, the handler updates its state.
• The adjustTimestamp is called and changes the timestamp to t1.
• The flow.adjustRatePerSecond is called, and the internal state of the flow contract is changed with the recent amount calculated at t1, which is greater than or equal to 100, for the example above.

---

After seeing the changes made in this PR, I understood better what you’ve proposed in your alternative and realized that I was wrong in saying it tests the same thing - it doesn’t.

The invariant should test that if any action is made on the stream that triggers the remaining amount, this amount should never be greater than the streamed amount (the streamed amount is the sum of recent amounts for each interval regardless if the ltu and rps are changed). In your invariant, you don’t test anything related to the remaining amount. This assertion will always check 0 == 0.

Also, this condition flowHandler.previousLastTimeUpdateOf(streamId) == flow.getLastTimeUpdate(streamId) passes only when no action is being made on the stream and only the time has passed.

I’ve created a new branch to address this invariant. Which I would open a PR for in favor of this.

---

Maybe we can keep both invariants, but I am not sure what this test is for anymore :))

[smol-ninja]

Thanks for taking time to review this. Please find my comments below:

If we update the state before we warp the time, it would cause discrepancies between the actual state in the flow contract and the handler state

I disagree. Previously, since we were updating states after the adjustTimestamp, we were logging states right BEFORE the functions are called. These states DO NOT represent flow states because the flow states are the state changes caused by the function call.

With the new changes, we are now logging states right AFTER the call is made by updating states before adjustTimestamp modifier. So doesn't the new approach create more consistencies between the flow states and the handler states?

An alternative solution could be to change the modifier so that it updates states right after the function is called.

modifier updateFlowHandlerStates() {
    _;
    previousDebtOf[currentStreamId] = flow.streamDebtOf(currentStreamId);
    previousLastTimeUpdateOf[currentStreamId] = flow.getLastTimeUpdate(currentStreamId);
    previousRecentAmountOf[currentStreamId] = flow.recentAmountOf(currentStreamId);
    previousRemainingAmountOf[currentStreamId] = flow.getRemainingAmount(currentStreamId);
}

[smol-ninja]

you don’t test anything related to the remaining amount. This assertion will always check 0 == 0

Why do you says it always test 0 == 0? Its not true because value of the remaining amount will never be zero without calling withdraw and it also never decreases. Thus, the invariant tests that rca and ra behave according to the rules.

but I am not sure what this test is for anymore :))

This tests what is written in the natspec i.e. recent amount should keep increasing with time and remaining amount should remain constant. It is equivalent to the invariant that amount owed (= rca + ra) should never decrease with time if no withdraw is called.

I’ve created a new branch to address this invariant

I had a look at it. The one problem I see with that invariant is that because you have streamedAmounts[currentStreamId] += flow.recentAmountOf(currentStreamId) and flow.recentAmountOf(currentStreamId) can never be negative because its uint type so streamedAmounts[currentStreamId] will always be greater than zero even in the presence of bug. This is same as

y += x where x > 0 then y > x is true always. So this may not be an invariant at all.

I suggest we discuss more before making a decision on which invariant should keep.

[andreivladbrg]

Why do you says it always test 0 == 0? Its not true because value of the remaining amount will never be zero without calling withdraw and it also never decreases. Thus, the invariant tests that rca and ra behave according to the rules.

because the function that updates the remaining amount from 0 to a value greater than 0 (which doesn't also set the rps to zero) is adjustRatePerSecond. and this function also updates the ltu, and in the if block, we have this check. which means that the invariant test will enter the if block assertions only when ra == 0

it is not about having it increased and then set to zero due to withdraw, it's about never actually increasing it above 0

This tests what is written in the natspec i.e. recent amount should keep increasing with time and

yes, indeed it tests the fact recent amount is monotonic, only when no action is made that effects the ltu. but that's not i wanted to achieve.

what i wanted to achieve: from the start time to the any point in future, the ra should never be greater than streamed amount (no matter what actions are made to the stream adjustRps, withdraw, restart pause, restartt again - i am not mentioning deposits/refunds as the don't modify ra/ltu). if the rps is adjusted, one time or multiple times, the calculation of the streamed amount is divided into multiple "segments"

remaining amount should remain constant

yes, indeed it's constant, but it would always be 0 in this assertion

I had a look at it. The one problem I see with that invariant is that because you have streamedAmounts[currentStreamId] += flow.recentAmountOf(currentStreamId) and flow.recentAmountOf(currentStreamId) can never be negative because its uint type so streamedAmounts[currentStreamId]

why does it need to be negative? the time goes only in one direction, it is always increasing.

will always be greater than zero even in the presence of bug. This is same as += x where x > 0 then y > x is true always. So this may not be an invariant at all.

fair point, but my counter argument is that the ra is not only updated with +rca, but it is also update to the balance, and if we've made an error in the code, it can be caught

[andreivladbrg]

as time passes, i feel like both of these invariants aren't that useful

[smol-ninja]

Good explanation @andreivladbrg. Let me think about it more. If you want feel free to push your commit (with the new invariant) into this PR. And I will review it later.

I would appreciate if you can also provide your comment on updateFlowHandlerStates argument.

[andreivladbrg]

I would appreciate if you can also provide your comment on updateFlowHandlerStates argument

as we discussed on the call, there is a problem with this approach because recentAmountOf streamDebtOf functions are time dependent

[smol-ninja]

I agree. I will revert it back.

[smol-ninja]

I have revised this PR to track the following invariant:

• If $rps \gt 0$, and no withdraw is made $\implies \frac{d(amountowed)}{dt} \ge 0$ i.e. amount owed shall never decrease.

Rationale

There are two important time-dependent macros: stream-debt and amount-owed.

Even though we had an invariant, invariant_DebtGt0_RpsGt0_DebtIncrease, which tracks debt monotonicity with time, no invariant tracking the monotonicity of amount owed. The discussions we had in this PR led me to realize that invariant_AmountOwedAlwaysIncrease is indeed an important invariant which we missed previously.

A quick summary on the importance

1. stream-debt: indirectly tracks that recent amount works as expected after solvency period.
2. amount-owed: indirectly tracks the recent amount works as expected throughout the stream lifecycle.