FREI-PI approach in _cancel and _withdraw

[PaulRBerg]

I just read this article that introduces a new development principle called FREI-PI (Function Requirements, Effects, Interactions - Protocol Invariants):

You're writing require statements wrong

Which got me thinking: what if we added a _verifyBalances check at the end of the function execution in _withdraw, which would check that the balance withdrawn matches the initial balance minus the withdraw amount?

We could then add a similar check in _cancel.

[Pet3ris]

FYI – example of how we use invariants in Aera with the Sablier commenting style:

https://github.com/aera-finance/aera-contracts-public/blob/main/v2/AeraV2Factory.sol#L127

[PaulRBerg]

@andreivladbrg could you please explore the possibility of using FREI-PI in the EOES implementation?

[smol-ninja]

What is EOES?

[andreivladbrg]

EVM open-ended streams

[smol-ninja]

I just read the article and I say that I like the approach.

what if we added a _verifyBalances check at the end of the function execution in _withdraw, which would check that the balance withdrawn matches the initial balance minus the withdraw amount?

I don't get what you mean by "the balance withdrawn matches the initial balance minus the withdraw amount", the balance to withdraw should be less than or equal to the initial balance minus the withdrawn amount.

I assume you mean the user-specific invariant, ${amountToWithdraw} <= {withdrawableAmount}$, which we already have as a first requirement. Please correct me if I misunderstood something.

  // Checks: the withdraw amount is not greater than the withdrawable amount.
  if (amount > withdrawableAmount) {
      revert Errors.SablierV2Lockup_Overdraw(streamId, amount, withdrawableAmount);
  }
  ........

Also, my understanding is that in FREI-PI design, the invariant check is over the post-CEI states. That means our invariant should not have action input parameters and should only take into account the protocol states.

What do you think of the following user level invariant?

For a given stream $i$:
$stream[i].amounts.withdrawn + stream[i].amounts.refunded <= stream[i].amounts.deposited$

Functions similar to deposit, withdraw and cancel can have this check. And I think this should hold true for any case.

Protocol level invariant?

I can not think of any protocol level invariant that involves simplicity and is not very expensive to compute. Would love to have your thoughts on this.

[andreivladbrg]

I don't get what you mean by "the balance withdrawn matches the initial balance minus the withdraw amount", the balance to withdraw should be less than or equal to the initial balance minus the withdrawn amount.

I think what he's referring to is about ERC20 balances, not internal amounts:

uint256 balanceBefore = IERC20(asset).balanceOf(address.this);

// rest of the function

require(balanceBefore - withdrawAmount == IERC20(asset).balanceOf(address.this));

[smol-ninja]

Ah, I see! Thanks for clarifying Andrei. That's an essential check for sure. Assuming invariant checks happen after interactions (FREI-PI) then this may not necessarily hold true when the recipient is a contract.

// This is also an interaction 
try ISablierV2LockupRecipient(recipient).onStreamWithdrawn(...)

This callback can invoke a direct deposit into the contract and break the invariant. Of course, there is no incentive for anyone to do that but just saying theoretically (now that I am thinking may be there is, for ex. when a user makes a single tx to withdraw and create another stream that leads to deposit assets & this is a legit user flow).

I think its still interesting. Do you think its a good idea to explore this new pattern for EOES? That article is quite tempting.

[andreivladbrg]

This callback can invoke a direct deposit into the contract and break the invariant

that's correct

the comparison operator should have been "<=" and not "=="

[andreivladbrg]

Do you think its a good idea to explore this new pattern for EOES? That article is quite tempting

yes, it might be a good idea

[PaulRBerg]

Thanks, Shub, for diving into this.

Andrei's observation about the ERC-20 balance state is correct - that's what I had in mind.

I agree with you that pursuing this methodology in V2OpenEnded is the way to go (because of the comparatively smaller refactor cost there). As a result, I've moved this discussion over to our global discussions repository.