paused and voided branch in refund and withdraw

[smol-ninja]

Original discussion: #290 (comment) created by @andreivladbrg.

Context

• Refund and Withdraw are only functions allowed on voided streams.
• We have an invariant that checks "if a stream is voided, it must also be paused"
• withdraw tree has neither of given paused or given voided branches
• refund only has given paused branch

What is the right approach?

• Should we include both paused and voided branches in refund and withdraw concrete tests?
• Should we add only paused branch, given that as per above invariant if its voided, it must also be paused?
• Should we not include these branches at all given these functions don't check the paused or voided status of a stream?

Based on our testing pattern, we do not include branches that are not a part of the implementation. So since neither of these functions check for paused or voided status, these branches should not be a part of it.

Thus starting this issue in the form of a discussion to understand what is the right approach here.

[smol-ninja]

cc @sablier-labs/solidity for RFC.

[PaulRBerg]

This is one of those ugly situations (which I refer to ass "statically bimodal paths") that are not fully captured by the existing BTT spec.

Before I share my feedback, I would like to clarify this:

Refund and Withdraw are only functions allowed on voided streams.

I am confused by this statement. It doesn't seem correct. Can you take a look and re-explain what you meant to say, @smol-ninja?

[PaulRBerg]

The following functions does not revert if the stream has VOIDED status: withdraw, withdrawMax, refund.

Exactly. This contradicts what you said in the OP: refund and withdraw are only functions allowed on voided streams. Can you double-check? It seems to me that you meant to say non-voided instead of voided.

Can you please explain what that means?

Completely equivalent branches that both need to be tested. The issue is which branch to highlight in the BTT tree — or should both be highlighted?

I need to open a discussion about this in the Bulloak repo.

[smol-ninja]

It seems to me that you meant to say non-voided instead of voided

Right, I should have included withdrawMax too. So, I wanted to say that on voided streams, only refund, withdraw and withdrawMax operations can succeed.

The issue is which branch to highlight in the BTT tree — or should both be highlighted

Yes or None? Because, as I mentioned in the OP, refund and withdraw do not even check whether the stream is paused or not. The tree branches test various if..else and revert conditions. If there are no paused conditions in these two functions, should they create branches in the tree? If yes, then which one between paused and voided? Or both?

I need to open a discussion about this in the Bulloak repo.

How is it relevant to Bulloak repo? It can be achived as the following (since there is an invariant that all voided streams are paused but all paused streams need not to be voided).

├── given paused
│   ├── given voided
│   │   └── do this
│   └── given not voided
│       └── do this
└── given not paused
    └── do something else

[PaulRBerg]

OK, I see what you mean now. Let me paraphrase to make sure we are on the same page:

When a stream is voided, the only functions throughout the whole contract that the user can call are refund, withdraw, and withdrawMax. All other functions would result into a revert.

Right? The original text made me think that you meant that refund & withdraw work only on voided streams, which is obviously not the case.

Yes or None?
should they create branches in the tree? If yes, then which one between paused and voided? Or both?

I don't know. This is why I said to open a discussion in Bulloak and agree upon a standardized solution for cases like this.

How is it relevant to Bulloak repo?

Coming up with a standardized solution for static bimodal paths.

[smol-ninja]

Right?

Yes you are right. We are on the same page now.

Coming up with a standardized solution for static bimodal paths

Fair enough. Lets start a discussion then. I have some ideas too. But before that, I'd appreciate your answer to the following question.

The issue is which branch to highlight in the BTT tree — or should both be highlighted?

You are focussing on the following two options:

1. Which of the two should be highlighted in the BTT tree?
2. Should both be highlighted?

But there is a third question as well which is "Should none of these branches be highlighted given that withdraw and refund don't even check for paused or voided status of a stream?". A simpler example below:

function isOdd(uint a) {
    if (a % 2 == 0) {
        return false;
    }
    return true;
}

├── when divisible by 2
│   └── it should return false
└── when not divisible by 2
    └── it should return true

vs

├── when divisible by 2
│   └── it should return false
└── when not divisible by 2
    ├── when prime
    │   └── it should return true
    └── when not prime
        └── it should return true

where the prime branch is analogous to paused / voided branch in case of refund and withdraw. This analogy comes because isOdd does not even check for primality of a number. Does it make sense?

[PaulRBerg]

Yes you are right. We are on the same page now.

Great, thanks for confirming.

But there is a third question as well which is "Should none of these branches be highlighted given that withdraw and refund don't even check for paused or voided status of a stream?".

Good point.

This analogy comes because isOdd does not even check for primality of a number. Does it make sense?

Yeah, good analogy.

Let me think about this, will follow up shortly.