Apply FREI-PI

[smol-ninja]

Find "one" core invariant that can be verified at the end of every execution.

Reading

1. https://www.nascent.xyz/idea/youre-writing-require-statements-wrong for ideas
2. https://github.com/orgs/sablier-labs/discussions/7

[smol-ninja]

I think I found the core invariant for Flow.

At the end of every execution, the following must hold true.

assert(previousTotalDebt - _totalDebtOf(streamId) == previousBalance - _streams[streamId].balance);

It also ensures that if no change in balance is observed, there should be no change in total debt as well. This also ensures that snapshotTime is correctly updated which is also crucial for the health of Flow streams.

i.e. the change in total debt must be equal to the change in the stream balance. cc @sablier-labs/solidity thoughts?

Re. gas: the storage is already loaded, so it won't impact gas so much.

[PaulRBerg]

Nice one @smol-ninja.

Basically, what goes out must be precisely recorded.

[smol-ninja]

what goes out must be precisely recorded.

Yes true for non-incoming payments. But it would fail for deposits so I am thinking how we can extend it to apply for deposits as well.

[smol-ninja]

Closing this with the following comments:

• There does not exist a single invariant that can be checked at the end of every function call without increasing the gas cost significantly.
• As a start, we've added a protocol invariant in withdraw function.

[PaulRBerg]

A gas cost increase is not a good reason to eschew FREI-PI.

A good reason is invariants being superfluous.

Could you share an example of a costly invariant to see if it's superfluous or not?

[smol-ninja]

A gas cost increase is not a good reason to eschew FREI-PI

Good point @PaulRBerg. That was an excuse on my part.

Could you share an example of a costly invariant to see if it's superfluous or not?

The below amount check must always hold true at the end of every function.

For a given streamId:

$\text{stream balance} = \text{total deposited} - \text{total withdrawn} - \text{total refunded}$

If there is an attack that can leak funds through one of the functions, the execution would update either one of the above values and the invariant would fail.

While stream balance is at our disposal, we would have to store the remaining three in storage and so an increase in gas cost (5k per variable => 15k in total).

Thoughts on this?

[PaulRBerg]

Let me have a think!

Wouldn't that be 15k gas extra only for those functions that touch all three variables? It should be less than that for functions that touch fewer variables.

There might be other (informational) benefits to having those values in storage.

[smol-ninja]

Yes you are right. Each of deposit, refund and withdraw will see an increase of 9300 (= 1 SSTORE + 3 cold SLOAD + 1 hot SLOAD) whereas other functions will see an increase of 8400 ( = 4 cold SLOAD). No function will write to more than one variable at a time.

Defining these variables would also mean removing aggregateBalance introduced by #234. aggregateBalance was chosen to replace having 3 variables as discussed in https://github.com/sablier-labs/company-discussions/discussions/11#discussioncomment-8243522.

[PaulRBerg]

Great, thanks for sharing the quantitative data.

That ~9k gas is an acceptable cost for building an 'invariant wall' around the protocol.

Are your gas estimates inclusive of the removal of aggregateBalance? Presumably, removing that variable would lead to a decrease in gas costs.

[smol-ninja]

Are your gas estimates inclusive of the removal of aggregateBalance? Presumably, removing that variable would lead to a decrease in gas costs

No it does not. Plus there will be some arithmetic gas cost as well. But in the end, it seems to be well below 10k.

[PaulRBerg]

Great, well in this case, I'm in favor of using FREI-PI.