spec: algorithm clarifications and changes around L29

[ancazamfir]

We had a discussion around the case where lockedRoundp = vr ∧ lockedValuep != v here as it should only happen if we accept equivocating votes.

28: upon (PROPOSAL, hp, roundp, v, vr) from proposer(hp, roundp) AND 2f + 1 (PREVOTE, hp, vr, id(v)) while
      step = propose ∧ (vr ≥ 0 ∧ vr < roundp) do
29:     if valid(v) ∧ (lockedRoundp ≤ vr ∨ lockedValuep = v) then 
30:        broadcast (PREVOTE, hp, roundp, id(v))
31: else
32:        broadcast (PREVOTE, hp, roundp, nil)
33: step ← prevote

@milosevic clarified:
The condition lockedValuep = v is probably not needed for the correctness as the important part is having 2f+1 prevotes for some value in the higher or equal round to the lockedRoundp. I cannot recall why we have added this condition as it would basically allow a process that have locked value v in higher round than the validRoundp to prevote for it. But this is actually not really needed for the correctness and can be seen as optimisation but it is probably insignificant and should be removed so it does not create confusion.

Concretly the proposal is to change to:

28: upon (PROPOSAL, hp, roundp, v, vr) from proposer(hp, roundp) AND 2f + 1 (PREVOTE, hp, vr, id(v)) while
      step = propose ∧ (vr ≥ 0 ∧ vr < roundp) do
29:     if valid(v) ∧ lockedRoundp ≤ vr then 
30:        broadcast (PREVOTE, hp, roundp, id(v))
31: else
32:        broadcast (PREVOTE, hp, roundp, nil)
33: step ← prevote

And the case where lockedRoundp = vr ∧ lockedValuep != v should have been caught by equivocation system, making it impossible to reach L28 in this case. Nevertheless in the code we will check for this case and not prevote, neither id(v) nor nil

[cason]

Some additional context on this: cometbft/cometbft#1309.

This covers specifically the case when lockedRoundp == vr but lockedValuep != v.

This issue was closed because I was unable to write a test unit that covers this scenario in Comet.

[cason]

I cannot recall why we have added this condition as it would basically allow a process that have locked value v in higher round than the validRoundp to prevote for it

With the time I realized that this pseudo-code is very influenced by the implementation.

In order to implement PBTS, we removed that possibility (voting the lockedValue) from the implementation, see: tendermint/tendermint#6850.

[cason]

So, is it safe to prevote the local lockedValue? Yes, it is. This is the only value that we can prevote, except if we receive a Polka for a different value in round vr > lockedRound. However, this is an optimization that creates some scenarios not covered in the pseudo-code and the models we have for Tendermint. Namely, we can have a situation where we have a Proposal for id(X) and the validator prevotes id(Y) where Y == lockedValue != X.

The probable reason for having this condition in the pseudo-code, up to Comet v1.x at least, is that it saves us the need for receiving the full value (block) re-proposed in round r as we already have this full value stored in the lockedValue field. This is, in summary, a problem related to the distinction between the pseudo-code, where PROPOSAL messages carry full values, and the implementations, where Proposal messages carry value IDs, and the node needs to retrieve the associated full value (block), as discussed in #365.

[cason]

A more conservative solution, which presumes that the threshold of failures f < n/3 is always respected, would be:

29:     if valid(v) ∧ (lockedRoundp < vr ∨ (lockedRoundp = vr ∧ lockedValuep = v))  then 

In this case, the third clause (lockedRoundp = vr ∧ lockedValuep = v) is always true by construction.

If this is not the case, we are clearly in a situation where we have f >= n/3. This means that when applying the certificate 2f + 1 (PREVOTE, hp, vr, id(v)) provided by the proposer we are catching at least f+1 equivocating votes, since we by construction have in our local log 2f + 1 (PREVOTE, hp, vr, id(lockedValuep)) that has lead us to lock on lockedValuep != v at round lockedRoundp = vr .

This is indeed an interesting point.