FIP-0086 Include message-rebroadcast and skipping rounds

FIPS/fip-0086.md

@@ -348,97 +348,193 @@ GossiPBFT(instance, inputChain, baseChain, participants) → decision, PoF:
 2:    decideSent ← False
 3:    proposal ← inputChain  \* holds what the participant locally believes should be a decision
 4:    timeout ← 2*Δ
-5:    value ← proposal \* used to communicate the voted value to others (proposal or 丄)
-6:    evidence ← nil   \* used to communicate optional evidence for the voted value
-7:    C ← {baseChain}
-
-8:    while (NOT decideSent)  {
-9:      if (round = 0)
-10:       BEBroadcast <QUALITY, value, instance>; trigger (timeout)
-11:       collect a clean set M of valid QUALITY messages from this instance
+5:    timeout_rebroadcast  ← timeout + 1 \* at least >timeout, how much greater is up to the participant to decide locally
+6:    value ← proposal \* used to communicate the voted value to others (proposal or 丄)
+7:    evidence ← nil   \* used to communicate optional evidence for the voted value
+8:    receiver_queue ←newQueue(size: 7*n) \* bounded queue, where n is the number of participants.
+9:    C ← {baseChain}
+10:   step ← nil
+11:   latest_broadcast ← {} \* map with latest msgs sent by this participant per step
+
+
+12:    while (step != DECIDE)  {
+13:      if (round = 0)
+14:       BEBroadcast <QUALITY, value, instance>; trigger (timeout)
+15:	  updateStep(round, QUALITY)
+16:       collect a clean set M of valid QUALITY messages from this instance
           until HasStrongQuorum(proposal, M) OR timeout expires
-12:       C ← C ∪ {prefix : IsPrefix(prefix,proposal) and HasStrongQuorum(prefix,M)}
-13:       proposal ← heaviest prefix ∈ C \* this becomes baseChain or sth heavier
-14:       value ← proposal
-
-15:     if (round > 0)     \* CONVERGE
-16:       ticket ← VRF(Randomness(baseChain) || instance || round)
-17:       value ← proposal \* set local proposal as value in CONVERGE message
-18:       BEBroadcast <CONVERGE, value, instance, round, evidence, ticket>; trigger(timeout)
-19:       collect a clean set M of valid CONVERGE msgs from this round and instance
+17: 	  updateStep(round, QUALITY)
+18:       C ← C ∪ {prefix : IsPrefix(prefix,proposal) and HasStrongQuorum(prefix,M)}
+19:       proposal ← heaviest prefix ∈ C \* this becomes baseChain or sth heavier
+20:       value ← proposal
+
+21:     if (round > 0)     \* CONVERGE
+22:       ticket ← VRF(Randomness(baseChain) || instance || round)
+23:       value ← proposal \* set local proposal as value in CONVERGE message
+24:       BEBroadcast <CONVERGE, value, instance, round, evidence, ticket>; trigger(timeout)
+25: 	  updateStep(round, CONVERGE)
+26:     collect a clean set M of valid CONVERGE msgs from this round and instance
           until timeout expires
-20:       prepareReadyToSend ← False
-21:		  while (not prepareReadyToSend){ 
-22:			  value, evidence ← GreatestTicketProposal(M)	\* leader election
-23:			  if (evidence is a strong quorum of PREPAREs AND mightHaveBeenDecided(value, r-1)):
-24:				  C ← C ∪ {value}
-25:			  if (value ∈ C)
-26:				  proposal ←value \* we sway proposal if the value is incentive compatible (i.e., in C)
-27:				  prepareReadyToSend ← True    \* Exit loop 
-28:			  else 
-29:				  M = {m ∈ M | m.value != value AND m.evidence.value != evidence.value} \* Update M for next iteration } 
-
-30:     BEBroadcast <PREPARE, value, instance, round, evidence>; trigger(timeout) \* evidence is nil in round=0
-31:	collect a clean set M of valid PREPARE messages from this round and instance
-    	until  (HasStrongQuorumValue(M) AND StrongQuorumValue(M) = proposal)  
-	  OR (timeout expires AND Power(M)>2/3)
-32:	if (HasStrongQuorumValue AND StrongQuorumValue(M) = proposal) \* strong quorum of PREPAREs for local proposal
-33:       value ← proposal \* vote for deciding proposal (COMMIT)
-34:       evidence ← Aggregate(M) \* strong quorum of PREPAREs is evidence
-35:     else
-36:       value ← 丄 \* vote for not deciding in this round
-37:       evidence ← nil
-
-38:     BEBroadcast <COMMIT, value, instance, round, evidence>; trigger(timeout)
-39:     collect a clean set M of valid COMMIT messages from this round and instance
-        until (HasStrongQuorumValue(M) AND StrongQuorumValue(M) ≠ 丄)
+27:     prepareReadyToSend ← False
+28:		  while (not prepareReadyToSend){ 
+29:			  value, evidence ← LowestTicketProposal(M)	\* leader election
+30:			  if (evidence is a strong quorum of PREPAREs AND mayHaveStrongQuorum(value, r-1, COMMIT, 1/3)):
+31:				  C ← C ∪ {value}
+32:			  if (value ∈ C)
+33:				  proposal ←value \* we sway proposal if the value is incentive compatible (i.e., in C)
+34:				  prepareReadyToSend ← True    \* Exit loop 
+35:			  else 
+36:				  M = {m ∈ M | m.value != value AND m.evidence.value != evidence.value} \* Update M for next iteration } 
+
+37:     reBroadcast <PREPARE, value, instance, round, evidence>; trigger(timeout) \* evidence is nil in round=0
+38:	collect a clean set M of valid PREPARE messages from this round and instance
+    	until (HasStrongQuorumValue(M) AND StrongQuorumValue(M) = proposal)
+          OR (NOT mayHaveStrongQuorum(proposal, round, step, 0))
+	        OR (timeout expires AND Power(M)>2/3)
+39:	if (HasStrongQuorumValue AND StrongQuorumValue(M) = proposal) \* strong quorum of PREPAREs for local proposal
+40:       value ← proposal \* vote for deciding proposal (COMMIT)
+41:       evidence ← Aggregate(M) \* strong quorum of PREPAREs is evidence
+42:     else
+43:       value ← 丄 \* vote for not deciding in this round
+44:       evidence ← nil
+
+45:     reBroadcast <COMMIT, value, instance, round, evidence>; trigger(timeout)
+46:     collect a clean set M of valid COMMIT messages from this round and instance
+	        OR (NOT mayHaveStrongQuorum(value, round, step, 0) for all value ≠ 丄)
           OR (timeout expires AND Power(M)>2/3)
-40:     if (HasStrongQuorumValue(M) AND StrongQuorumValue(M) ≠ 丄)    \* decide
-41:       evidence ← Aggregate(M)
-42:       BEBroadcast <DECIDE, StrongQuorumValue(M), instance, evidence>
-43:       decideSent ← True \* break loop, wait for other DECIDE messages
-44:     if (∃ m ∈ M: m.value ≠ 丄 s.t. mightHaveBeenDecided(m.value, r)) \* m.value was possibly decided by others
-45:       C ← C ∪ {m.value} 		\* add to candidate values if not there
-46:       proposal ← m.value; \* sway local proposal to possibly decided value
-47:       evidence ← m.evidence \* strong PREPARE quorum is inherited evidence
-48:     else \* no participant decided in this round
-49:       evidence ← Aggregate(M) \* strong quorum of COMMITs for 丄 is evidence
-50:     round ← round + 1;
-51:     timeout ← updateTimeout(timeout, round)
-52:   }  \*end while
-
-53:   collect a clean set M of valid DECIDE messages
+47:     if (HasStrongQuorumValue(M) AND StrongQuorumValue(M) ≠ 丄)    \* decide
+48:       evidence ← Aggregate(M)
+49:       reBroadcast <DECIDE, StrongQuorumValue(M), instance, evidence>  \* break loop, wait for other DECIDE messages
+50:     if (∃ m ∈ M: m.value ≠ 丄 s.t. mayHaveStrongQuorum(m.value, r, COMMIT, 1/3)) \* m.value was possibly decided by others
+51:       C ← C ∪ {m.value} 		\* add to candidate values if not there
+52:       proposal ← m.value; \* sway local proposal to possibly decided value
+53:       evidence ← m.evidence \* strong PREPARE quorum is inherited evidence
+54:     else \* no participant decided in this round
+55:       evidence ← Aggregate(M) \* strong quorum of COMMITs for 丄 is evidence
+56:     round ← round + 1;
+57:     timeout ← updateTimeout(timeout, round)
+58:     timeout_rebroadcast ← max(timeout+1, timeout_rebroadcast)
+59:   }  \*end while
+
+60:   collect a clean set M of valid DECIDE messages
       until (HasStrongQuorumValue(M)) \* collect a strong quorum of decide outside the round loop
-54:   return (StrongQuorumValue(M), Aggregate(M)) \* terminate the algorithm with a decision
+61:   return (StrongQuorumValue(M), Aggregate(M)) \* terminate the algorithm with a decision
 ```
 ```
 \* decide anytime
-55: upon reception of a valid <DECIDE, instance, v, evidence> AND not decideSent
-56:	  decideSent ← True
-57:	  BEBroadcast <DECIDE, v, instance, evidence)
-58:	  go to line 53. 
+62: upon reception of a valid <DECIDE, instance, v, evidence> AND not decideSent
+63:	  reBroadcast <DECIDE, v, instance, evidence)
+64:	  go to line 60. 
 ```
 
-The helper function mightHaveBeenDecided returns False if, given the already delivered messages, the participant knows for a fact that no correct participant could have decided the given value in the given round, even in the presence of an adversary controlling <⅓ the QAP equivocating, and True otherwise: 
+The helper function mayHaveStrongQuorum returns False if, given the already delivered messages, the participant knows for a fact that no correct participant could have decided the given value in the given round, even in the presence of an adversary controlling advPower the relative amount of total QAP equivocating, and True otherwise. The parameter advPower can be set to 0 in order to consider the possibility of the participant locally deciding, whereas when set to 1/3 it considers the possibility of any participant deciding:
 
 ```
-59: mightHaveBeenDecided(value, round): 
-60:	M  ← { m | m.step = COMMIT AND m.round = round AND m is valid}
-61:     M' ← { m | m ∈ M AND m.value = value } 
-62:     f Power(M') + (1-Power(M)) < ⅓  : \* value cannot have been decided 
-63:		return False
-64:     return True
+65: mayHaveStrongQuorum(value, round, step, advPower): 
+66:	M  ← { m | m.step = step AND m.round = round AND m is valid} /* clean set of messages
+67:     M' ← { m | m ∈ M AND m.value = value } 
+68:     f Power(M') + (1-Power(M)) < ⅔ - advPower  : \* value cannot have been decided 
+69:		return False
+70:     return True
 ```
-Note that the selection of the heaviest prefix in line 13 does not need access to the tipsets' EC weights, as only prefixes that extend each other can gather a strong quorum in QUALITY. In other words: if there are two tipsets $t_1, t_2$ that gather a strong quorum of QUALITY, then either the corresponding chain that has $t_1$ as head tipset is a prefix of the analogous chain that has $t_2$ as head, or viceversa (since the adversary controls < ⅓ of the QAP). As a result, selecting the heaviest prefix is as simple as selecting the highest blockheight (greatest number of blocks), while ensuring all proposed prefixes that gather a strong quorum in QUALITY extend each other as a sanity check.
 
-Implementations may optimise this algorithm to treat the reception of an aggregated signature over some (MsgType, Instance, Round, Value) as evidence of a message as if it had received the same tuple of values directly from each participant in the aggregate. This may be used to effectively skip a partially-complete step. In the particular case of a DECIDE message, which carries evidence of a strong quorum of COMMITs for the same round and value, a participant immediately sends its own DECIDE for the same value (copying the evidence) and exits the loop at line 8.
+The reBroadcast function rebroadcasts all the messages in the current round if the participant cannot terminate the step that it is in by the time the timeout has expired. 
 
-Also, concurrently, we expect that the participant feeds to GossiPBFT chains that are incentive-compatible with EC. To this end, we restrict the set C of candidate values that the participant contributes to deciding to only values that either (i) pass the QUALITY step or (ii) may have been decided by other participants (hence the functin `mightHaveBeenDecided`).
+```
+71: func reBroadcast(msg): 
+72:     latest_broadcast[msg.step] = msg
+73:	BEBroadcast(msg)
+74:  	trigger(timeout_rebroadcast) 
+75:     updateStep(msg.round, msg.step)
+76:	upon timeout_rebroadcast expires:
+77:		If step = msg.step AND msg.round = round AND msg.instance = instance \* stuck, need to rebroadcast
+78: 			switch (msg.step) {
+79:     				case DECIDE:
+80:         					BEBroadcast(latest_broadcast[DECIDE]) \* only rebroadcast DECIDE
+81:         					break;  // Exit, no cascading
+82:     				case COMMIT:
+83:        					BEBroadcast(latest_broadcast[COMMIT]) \* no break, cascade to broadcast PREPARE, CONVERGE
+84:     				case PREPARE:
+85:						BEBroadcast(latest_broadcast[PREPARE]) \* no break, cascade to broadcast CONVERGE
+86:     				default: \* QUALITY or CONVERGE, which will never reach this point, but send CONVERGE here because of cascading effect of switch cases
+87: 					if msg.round > 0:
+88:						BEBroadcast(latest_broadcast[CONVERGE])
+89:         				break;
+90: 			}
+91:			update(timeout_rebroadcast); \* increase and trigger again timeout_rebroadcast 
+92:			trigger(timeout_rebroadcast) 
+```
+
+The updateStep function simply updates the step and delivers locally all buffered messages for the new step and round:
+
+```
+93: func updateStep(round, new_step): 
+94:	step ← new_step
+95: 	receiveAll(receiver_queue.PopAll(round, step)) \* deliver all queued messages in the queue for this instance, round and step, and remove from queue
+```
+
+The conditions for skipping rounds and buffering messages are shown below:
+
+```
+96: upon reception of a valid msg: \* assume validity implies same instance as currently running, different instances treated elsewhere (not scope of this doc)
+97: 	if msg.round < round \* drop message
+98:		return
+99:	else if msg.step = DECIDE 
+100:		deliver(DECIDE) \*DECIDE immediately delivered within an instance
+101:	else if msg.step = step and msg.round = round
+102:		deliver(msg) \* can be delivered as it is for this round and step
+103:	else if msg.round > round
+104:		receiver_queue.Add(msg) 
+105: 		receiver_queue.Trim() \* selectively drop messages if bound met. See text below.
+106:       	if  (msg' ← shouldJump(round, step, timeout) s.t. msg' != nil) 	\* one of the rest of conditions to be able to jump
+107:			round ← msg.round;
+108:   			timeout ← 2*Δ*2**msg.round
+109:			timeout_rebroadcast ← max(timeout+1, timeout_rebroadcast)
+110:			if msg'.evidence.step = PREPARE: \* either this or strong quorum of COMMITs for 丄
+111:	 			C ← C ∪ {msg'.value} 		\* add to candidate values if not there
+112:				proposal ← msg'.value; 		\* sway local proposal to possibly decided value
+113:			evidence ← msg'.evidence	\* strong PREPARE quorum is inherited evidence for the value (it exists because the value might have been decided)
+114:			go to line 22  \* start new round by jumping forward
+
+115: func shouldJump(round, step, timeout): 
+116: 	if step = QUALITY OR step = DECIDE: \* never jump on DECIDE or QUALITY
+117: 		return nil
+118:     if (∃ msg' ∈ receiver_queue st. msg'.step = CONVERGE		\* there must be a CONVERGE for the new round
+	     AND msg'.round > round)					\* round must be greater	
+119: 		if ∃ M ⊆ receiver_queue s.t. M is clean and valid and contains a weak quorum of PREPAREs for msg'.round
+120:			return msg'
+121:		if timeout expired AND NOT canTerminateStep(round, step)
+122:			return msg'
+123:	return nil
+```
+
+The function canTerminateStep(round, step) returns True if the step contains the conditions to terminate in the round (lines 26, 38, 46, for CONVERGE, PREPARE, COMMIT, respectively), and False otherwise. 
+
+The function receiver_queue.Trim() contains a bounded queue that suffices to store at least the following messages from this instance:
+
+(a) One valid CONVERGE message for the greatest round available of all received messages for this instance. Let us call this round greatest_round.
+  (a.1) :
+	- A strong quorum of PREPARE messages for greatest_round AND
+	- A strong quorum of COMMIT messages for greatest_round. 
+  (a.2) :
+	- Enough messages to advance in the current round
+(b)  A strong quorum of DECIDE messages
+(c)  A strong quorum of QUALITY messages (if not yet executed for this instance)
+
+QUALITY messages in the queue can be removed once the QUALITY phase is executed. Also, once a valid DECIDE message is received, all other messages in the queue for this instance can be removed. All messages are dropped from the queue when delivered, and messages from the greatest_round are dropped once greatest_round is updated, except for the cases that greatest_round was the current round (because of (b)).
+
+The queue size must store at least all messages satisfying the above constraints, meaning at most 7*n messages (but in most cases it will be significantly less).
+
+Note that the selection of the heaviest prefix in line 19 does not need access to the tipsets' EC weights, as only prefixes that extend each other can gather a strong quorum in QUALITY. In other words: if there are two tipsets $t_1, t_2$ that gather a strong quorum of QUALITY, then either the corresponding chain that has $t_1$ as head tipset is a prefix of the analogous chain that has $t_2$ as head, or viceversa (since the adversary controls < ⅓ of the QAP). As a result, selecting the heaviest prefix is as simple as selecting the highest blockheight (greatest number of blocks), while ensuring all proposed prefixes that gather a strong quorum in QUALITY extend each other as a sanity check.
+
+Implementations may optimise this algorithm to treat the reception of an aggregated signature over some (MsgType, Instance, Round, Value) as evidence of a message as if it had received the same tuple of values directly from each participant in the aggregate. This may be used to effectively skip a partially-complete step. In the particular case of a DECIDE message, which carries evidence of a strong quorum of COMMITs for the same round and value, a participant immediately sends its own DECIDE for the same value (copying the evidence) and exits the loop at line 12.
+
+Also, we restrict the set C of candidate values that the participant contributes to deciding to only values that either (i) pass the QUALITY step or (ii) may have been decided by other participants (hence the function `mayHaveStrongQuorum`).
 
 
 #### Valid messages and evidence
 
-The $\texttt{Valid}()$ predicate (referred to in lines 11, 19, 31, and 39, 53, 55) is defined below.
+The $\texttt{Valid}()$ predicate (referred to in lines 16, 26, 38, 46, 60, 62, 66, 96 and 119) is defined below.
 ```
 Valid(m):                                      | For a message m to be valid,
   if m.signature does not verify               |   m must be properly signed.
@@ -524,7 +620,7 @@ GossiPBFT ensures termination provided that (i) all participants start the insta
 
 [Given prior tests performed on GossipSub](https://research.protocol.ai/publications/gossipsub-v1.1-evaluation-report/vyzovitis2020.pdf) (see also [here](https://gist.github.com/jsoares/9ce4c0ba6ebcfd2afa8f8993890e2d98)), we expect that sent messages will reach almost all participants within $Δ=3s$, with a majority receiving them even after $Δ=2s$. However, if several participants start the instance $Δ + ε$ after some other participants, termination is not guaranteed for the selected timeouts of $2*Δ$. Thus, we do not rely on an explicit synchrony bound for correctness. Instead, we increase the estimate of Δ locally within an instance as rounds progress without decision.
 
-The synchronization of participants is performed in the call to $\texttt{updateTimeout(timeout, round)}$ (line 51), and works as follows:
+The synchronization of participants is performed in the call to $\texttt{updateTimeout(timeout, round)}$ (line 57), and works as follows:
 
 * Participants start an instance with $Δ=2s$.
 * Participants set their timeout for the current round to $Δ*1.3^{r}$ where $r$ is the round number ($r=0$ for the first round).