Find one core invariant and apply FREI-PI

sablier-labs / flow

🍃 Smart contracts of the Sablier Flow protocol.

Other

8 stars 0 forks source link

Find one core invariant and apply FREI-PI #146

Open smol-ninja opened 4 months ago

smol-ninja commented 4 months ago

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

Reading

smol-ninja commented 1 month ago

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 commented 1 month ago

Nice one @smol-ninja.

Basically, what goes out must be precisely recorded.

smol-ninja commented 1 month ago

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 commented 1 week ago

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 commented 1 week ago

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?