test: add invariant_DebtGt0_RpsGt0_DebtIncrease

[smol-ninja]

Changelog

One New Invariant

1. If rps > 0 and no additional deposits are made, then debt should never decrease. This invariant failing led me to feat: persist amount owed beyond depletion timestamp #126 PR.

Other changes

1. In README.md, I have used LaTeX to re-write invariant formulas. The order of invariants match the same order in which they are written in Flow.t.sol.
2. Adds NatSpec over all invariant functions. It match the formulas mentioned in README file.
3. Makes some changes to invariant_DepositAmountsSumGeExtractedAmountsSum and also renamed them.
4. Adds new variables in FlowHandler to track key data. These new variables are required by the above 2 new invariants.
5. updateFlowStates modifier it added to handler to update states prior to the function call.
6. I have removed restartAndDeposit from handler as its just a proxy for restart and deposit.
7. Replaced extractedAmounts with refundedAmounts and withdrawnAmounts
8. Added "only to recipient" note for withdraw made by sender

PR dependencies

• test: remove TimestampStore from invariant tests #128

Note

The CI test would fail. It demonstrates the bug in the current implementation.

[andreivladbrg]

If rps > 0 and no additional deposits are made, then debt should never decrease. This invariant failing led me to #126 PR.
If rps > 0 and no withdraws are made, remaining amount + streamed amount should never decrease

aren't these pretty much the same?

let's keep only one - invariant_RpsGt0_RemainingPlusStreamedIncrease

[smol-ninja]

aren't these pretty much the same?

I think no, they are not the same.

• The first invariant focusses on the debt while the second focusses on the amount owed to the recipient.
• When debt = 0 and rps > 0, the amount owed should keep increasing.
• When debt > 0 and rps > 0, the debt should keep increasing.

The test thats failing is invariant_DebtGt0_RpsGt0_DebtIncrease and not invariant_RpsGt0_RemainingPlusStreamedIncrease. So we should keep invariant_DebtGt0_RpsGt0_DebtIncrease but invariant_RpsGt0_RemainingPlusStreamedIncrease is important too for recipient.

[andreivladbrg]

• The first invariant focusses on the debt while the second focusses on the amount owed to the recipient

amount owed to the recipient and the stream debt are correlated

it is the same argument you said here

you can't have one(invariant) without the other

but invariant_RpsGt0_RemainingPlusStreamedIncrease is important too for recipient

same thing you can say for $bal \ge rfa$ it is useful for recipient but it is not needed since we have $bal = rfa + wa$

wdyt?

[smol-ninja]

May be, invariant_RpsGt0_RemainingPlusStreamedIncrease is not a key invariant and the same invariant may already be achieved by other invariants. (I am still thinking if its true). But its not same as the invariant_DebtGt0_RpsGt0_DebtIncrease otherwise both should fail at the same time.

I can remove it for now since I don't have any good argument in its support.

[smol-ninja]

@andreivladbrg I have removed invariant_RpsGt0_RemainingPlusStreamedIncrease invariant. lmk if all looks good now.

[andreivladbrg]

looks good now