Find one core invariant and 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?