diff --git a/FIPS/fip-0086.md b/FIPS/fip-0086.md index 471b702c..a1dd60c3 100644 --- a/FIPS/fip-0086.md +++ b/FIPS/fip-0086.md @@ -179,9 +179,9 @@ The algorithm starts by initializing $finalizedTipsets[0]$ with the genesis tips 1. Wait until the current epoch is at least two epochs from that of the latest finalized head. 2. Obtain the set of participants of instance $i$ from the power table determined by the finalized tipset 10 instances ago. -4. Call the $\texttt{HeaviestUnfinalizedChain}()$ function that returns the tipsets of the locally observed chain constructed by EC from finalizedTipset[i-1].Head (including the head of the finalized chain) and sets the $proposal$ variable to the returned value. We assume that such a function is available to the finalizer. Note that the proposal is pruned so that its head is at most a tipset from the previous epoch, not the current epoch. -5. Execute the instance $i$ of GossiPBFT consensus. -6. Add the returned tipset from the consensus execution to the $finalizedTipsets$ list. +3. Call the $\texttt{HeaviestUnfinalizedChain}()$ function that returns the tipsets of the locally observed chain constructed by EC from finalizedTipset[i-1].Head (including the head of the finalized chain) and sets the $proposal$ variable to the returned value. We assume that such a function is available to the finalizer. Note that the proposal is pruned so that its head is at most a tipset from the previous epoch, not the current epoch. +4. Execute the instance $i$ of GossiPBFT consensus. +5. Add the returned tipset from the consensus execution to the $finalizedTipsets$ list. To prevent useless instances of GossiPBFT deciding on the same $baseChain$ because of the lack of a new epoch that provides a new proposal, we make the $\texttt{ChainHead}()$ function blocking in that it does not return a proposal unless the current chain head is different from the chain head of the finalized chain. @@ -360,132 +360,200 @@ We illustrate the pseudocode for GossiPBFT below, consisting of 3 steps per roun GossiPBFT(instance, inputChain, baseChain, participants) → decision, PoF: \*participants is implicitly used to calculate quorums -1: round ← 0 -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 ; trigger (timeout) -11: 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 ; trigger(timeout) -19: 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 EC 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 ; 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 ; trigger(timeout) -39: collect a clean set M of valid COMMIT messages from this round and instance - until (HasStrongQuorumValue(M) AND StrongQuorumValue(M) ≠ 丄) - OR (timeout expires AND Power(M)>2/3) -40: if (HasStrongQuorumValue(M) AND StrongQuorumValue(M) ≠ 丄) \* decide -41: evidence ← Aggregate(M) -42: BEBroadcast -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 - 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 +01: round ← 0 +02: decideSent ← False +03: proposal ← inputChain \* holds what the participant locally believes should be a decision +04: timeout ← 2*Δ +05: timeout_rebroadcast ← timeout + 1 + \* timeout_rebroadcast is at least >timeout, how much greater is up to the participant +06: value ← proposal \* used to communicate the voted value to others (proposal or 丄) +07: evidence ← nil \* used to communicate optional evidence for the voted value +08: C ← {baseChain} +09: step ← nil +10: own_msgs ← {} \* specified as a set of msgs, exact data structure can be implementation specific + +11: while (step != DECIDE) { +12: if (round = 0) +13: BEBroadcast ; trigger (timeout) +14: step ← QUALITY +15: collect a clean set M of valid QUALITY messages from this instance + until HasStrongQuorum(proposal, M) OR timeout expires +17: C ← C ∪ {prefix : IsPrefix(prefix,proposal) and HasStrongQuorum(prefix,M)} +18: proposal ← heaviest prefix ∈ C \* this becomes baseChain or sth heavier +19: value ← proposal + +20: if (round > 0) \* CONVERGE +21: ticket ← VRF(Randomness(baseChain) || instance || round) +22: value ← proposal \* set local proposal as value in CONVERGE message +23: reBroadcast ; trigger(timeout) +25: collect a clean set M of valid CONVERGE msgs from this round and instance + until timeout expires +26: value, justification ← GreatestTicketProposal(M) \* leader election +27: if (evidence is a strong quorum of PREPAREs AND mayHaveStrongQuorum(value, r-1, COMMIT, 1/3)) +28: C ← C ∪ {value} +29: if (value ∈ C) +30: proposal ← value \* we sway proposal if the value is EC compatible (i.e., in C) +31: evidence ← justification \* otherwise keep existing proposal and evidence + +32: reBroadcast ; trigger(timeout) + \* note that evidence is nil in round=0 +33: 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, PREPARE, 0)) + OR (timeout expires AND isStrongQuorum(M)) +34: if (HasStrongQuorumValue AND StrongQuorumValue(M) = proposal) + \* strong quorum of PREPAREs for local proposal +35: value ← proposal \* vote for deciding proposal (COMMIT) +36: evidence ← Aggregate(M) \* strong quorum of PREPAREs is evidence +37: else +38: value ← 丄 \* vote for not deciding in this round +39: evidence ← nil + +40: reBroadcast ; trigger(timeout) +41: collect a clean set M of valid COMMIT messages from this round and instance + until HasStrongQuorumValue(M) OR (timeout expires AND IsStrongQuorum(M)) +42: if (HasStrongQuorumValue(M)) +43: if (StrongQuorumValue(M) ≠ 丄) \* decide +44: evidence ← Aggregate(M) +45: reBroadcast + \* effectively breaks the while loop, next line is 56 - wait for other DECIDE messages +46: else \* no participant decided in this round +47: evidence ← Aggregate(M) \* strong quorum of COMMITs for 丄 is evidence +48: if (∃ m ∈ M: m.value ≠ 丄) \* m.value was possibly decided by others +49: C ← C ∪ {m.value} \* add to candidate values if not there +50: proposal ← m.value; \* sway local proposal to possibly decided value +51: evidence ← m.evidence \* strong PREPARE quorum is inherited evidence +52: round ← round + 1; +53: timeout ← updateTimeout(timeout, round) +54: timeout_rebroadcast ← max(timeout+1, timeout_rebroadcast) +55: } \*end while + +56: collect a clean set M of valid DECIDE messages + until (HasStrongQuorumValue(M)) \* collect a strong quorum of decide outside the round loop +57: return (StrongQuorumValue(M), Aggregate(M)) \* terminate the algorithm with a decision ``` ``` \* decide anytime -55: upon reception of a valid AND not decideSent -56: decideSent ← True -57: BEBroadcast AND not decideSent +59: reBroadcast +60: go to line 56. ``` -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 +61: mayHaveStrongQuorum(value, round, step, advPower): +62: M ← { m | m.step = step AND m.round = round AND m is valid} /* clean set of messages +63: M' ← { m | m ∈ M AND m.value = value } +64: if Power(M') + (1-Power(M)) < ⅔ - advPower : \* value cannot have been decided +65: return False +66: 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 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`). +``` +67: reBroadcast(msg): +68: own_msgs = own_msgs ∪ {msg} +69: BEBroadcast(msg) +70: trigger(timeout_rebroadcast) +71: step ← msg.step +72: upon timeout_rebroadcast expires: +73: if step = msg.step AND msg.round = round AND msg.instance = instance + \* stuck, need to rebroadcast +74: switch (msg.step) { +75: case DECIDE: +76: BEBroadcast(m ∈ own_msgs: m.round=0 AND m.type=DECIDE) \* only rebroadcast DECIDE +77: break; // Exit, no cascading +78: case COMMIT: +79: BEBroadcast(m ∈ own_msgs: m.round=msg.round AND m.type=COMMIT) + \* no break, cascade to broadcast PREPARE, CONVERGE +80: case PREPARE: +81: BEBroadcast(m ∈ own_msgs: m.round=msg.round AND m.type=PREPARE) + \* no break, cascade to broadcast CONVERGE +82: default: \send CONVERGE here because of cascading effect of switch cases +83: if msg.round > 0: +84: BEBroadcast(m ∈ own_msgs: m.round=msg.round AND m.type=CONVERGE) +85: BEBroadcast(m ∈ own_msgs: m.round=msg.round-1 AND m.type=COMMIT) +86: BEBroadcast(m ∈ own_msgs: m.round=msg.round-1 AND m.type=PREPARE) +87: break; +88: } +89: update(timeout_rebroadcast); \* increase and trigger again timeout_rebroadcast +90: trigger(timeout_rebroadcast) +``` +The conditions for skipping rounds and buffering messages are shown below (below, max_lookahead_rounds is an implementation config parameter): + +``` +100: upon reception of a valid msg: + \* validity assumes same instance as currently running + \* different instances treated elsewhere (not scope of this doc) +101: if (msg.round > round + max_lookahead_rounds) AND msg.step = COMMIT AND msg.value = 丄 +102: return \* drop message +103: deliver(msg) +104: if (msg' ← shouldJump(round, step) s.t. msg' != nil) + \* one of the rest of conditions to be able to jump +105: round ← msg'.round; +106: timeout ← 2*Δ*backOffExponent**msg'.round +107: timeout_rebroadcast ← max(timeout+1, timeout_rebroadcast) +108: if msg'.evidence.step = PREPARE: \* either this or strong quorum of COMMITs for 丄 +109: C ← C ∪ {msg'.value} \* add to candidate values if not there +110: proposal ← msg'.value; \* sway local proposal to possibly decided value +111: evidence ← msg'.evidence + \* strong PREPARE quorum is inherited evidence for the value + \* it exists because the value might have been decided +112: go to line 21 \* start new round>0 by jumping forward + +113: shouldJump(round, step): +114: if step = QUALITY OR step = DECIDE: \* never jump on DECIDE or QUALITY +115: return nil +116: if (∃ msg' st. msg'.step = CONVERGE \* there must be a CONVERGE for the new round + AND msg'.round > round \* round must be greater + AND ∃ M s.t. M is clean and valid and contains a weak quorum of PREPAREs for msg'.round) +117: return msg' +118: return nil +``` + +Note that the selection of the heaviest prefix in line 18 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 11. + +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 15, 25, 33, 41, 56, 58, 62, 100 and 116) is defined below. ``` -Valid(m): | For a message m to be valid, - if m.signature does not verify | m must be properly signed. - return False | - if m.instance != instance | m must match the instance ID. - return False | - if m.sender has zero power or is unknown: | The sender must have power and be known. - return False | - if NOT (m.value = 丄 | m's value must extend baseChain - OR baseChain.isPrefix(m.value)) | or be 丄 - return False | - if m.step != CONVERGE AND m.ticket != nil | ticket must be nil if not CONVERGE - return False | - if m.step = QUALITY AND | A QUALITY message must - (m.round != 0 OR m.value = 丄) | have round 0 and non-丄 value. - return False | - if m.step = CONVERGE AND | A CONVERGE message must - (m.round = 0 OR m.value = 丄 OR | have non-zero round, non-丄 value, - m.ticket does not pass VRF validation) | and a valid ticket. - return False | - if m.step = DECIDE AND | A DECIDE message must - (m.round != 0 OR m.value = 丄) | have round 0 and non-丄 value. - return False | - if m.step IN {QUALITY} | If the step never requires evidence - if m.evidence != nil: | (QUALITY), evidence should not be present. - return False | - if len(m.value) > 100: | Proposal's head must be at most 99 tipsets - return False | ahead of baseChain's head - else | - return ValidEvidence(m) | - return True | +Valid(m): | For a message m to be valid, + if m.signature does not verify | m must be properly signed. + return False | + if m.instance != instance | m must match the instance ID. + return False | + if m.sender has zero power or is unknown: | The sender must have power and be known. + return False | + if NOT (m.value = 丄 OR | m's value must extend baseChain + baseChain.isPrefix(m.value)) | or be 丄 + return False | + if m.step != CONVERGE AND m.ticket != nil | ticket must be nil if not CONVERGE + return False | + if m.step = QUALITY AND | A QUALITY message must + (m.round != 0 OR m.value = 丄) | have round 0 and non-丄 value. + return False | + if m.step = CONVERGE AND | A CONVERGE message must + (m.round = 0 OR m.value = 丄 OR | have non-zero round, non-丄 value, + m.ticket does not pass VRF validation) | and a valid ticket. + return False | + if m.step = DECIDE AND | A DECIDE message must + (m.round != 0 OR m.value = 丄) | have round 0 and non-丄 value. + return False | + if m.step IN {QUALITY} | If the step never requires evidence + if m.evidence != nil: | (QUALITY), evidence should not be present. + return False | + if len(m.value) > 100: | Proposal's head must be at most 99 tipsets + return False | ahead of baseChain's head. + else | + return ValidEvidence(m) | + return True | ``` The $\texttt{ValidEvidence}()$ predicate is defined below. Note that QUALITY messages do not need evidence. @@ -493,37 +561,37 @@ The $\texttt{ValidEvidence}()$ predicate is defined below. Note that QUALITY mes ``` ValidEvidence(m= ): -if ( step = PREPARE and round = 0) | in the first round, - AND (evidence = nil) | evidence for PREPARE - return True | is nil - -if (step = COMMIT and value = 丄) | a COMMIT for 丄 carries no evidence - AND (evidence = nil) - return True - -If (evidence.instance != instance) | the instance of the evidence must be the - return False | same as that of the message - - | valid evidences for -return (step = CONVERGE OR (step = PREPARE AND round>0) | CONVERGE and PREPARE in - AND (∃ M: Power(M)>⅔ AND evidence=Aggregate(M) | round>0 is strong quorum - AND ((∀ m’ ∈ M: m’.step = COMMIT AND m’.value = 丄) | of COMMIT msgs for 丄 - OR (∀ m’ ∈ M: m’.step = PREPARE AND | or PREPARE msgs for - m’.value = value)) | CONVERGE value - AND (∀ m’ ∈ M: m’.round = round-1))) | from previous round - - -OR (step=COMMIT | valid COMMIT evidence - AND (∃ M: Power(M)>⅔ AND evidence=Aggregate(M) | is a strong quorum - AND ∀ m’ ∈ M: m’.step = PREPARE | of PREPARE messages - AND ∀ m’ ∈ M: m’.round = round | from the same round - AND ∀ m’ ∈ M: m’.value = value)) | for the same value, or - -OR (step = DECIDE | valid DECIDE evidence - AND (∃ M: Power(M)>⅔ AND evidence=Aggregate(M) | is a strong quorum - AND ∀ m’ ∈ M: m’.step = COMMIT | of COMMIT messages - AND ∀ m’ ∈ M: m’.round = round | from the same round - AND ∀ m’ ∈ M: m’.value = value)) | for the same value +if (step = PREPARE AND round = 0) AND | in the first round, for PREPARE + (evidence = nil) | evidence is nil + return True + +if (step = COMMIT and value = 丄) AND | a COMMIT for 丄 + (evidence = nil) | carries no evidence + return True + +if (evidence.instance != instance) | the instance of the evidence must be the + return False | same as that of the message + + | valid evidences for +return (step = CONVERGE OR (step = PREPARE AND round>0) | CONVERGE and PREPARE in + AND (∃ M: IsStrongQuorum(M) AND evidence=Aggregate(M) | round>0 is strong quorum + AND ((∀ m’ ∈ M: m’.step = COMMIT AND m’.value = 丄) | of COMMIT msgs for 丄 + OR (∀ m’ ∈ M: m’.step = PREPARE AND | or PREPARE msgs for + m’.value = value)) | CONVERGE value + AND (∀ m’ ∈ M: m’.round = round-1))) | from previous round + + +OR (step=COMMIT | valid COMMIT evidence + AND (∃ M: IsStrongQuorum(M) AND evidence=Aggregate(M) | is a strong quorum + AND ∀ m’ ∈ M: m’.step = PREPARE | of PREPARE messages + AND ∀ m’ ∈ M: m’.round = round | from the same round + AND ∀ m’ ∈ M: m’.value = value)) | for the same value, or + +OR (step = DECIDE | valid DECIDE evidence + AND (∃ M: IsStrongQuorum(M) AND evidence=Aggregate(M)| is a strong quorum + AND ∀ m’ ∈ M: m’.step = COMMIT | of COMMIT messages + AND ∀ m’,m'' ∈ M: m’.round = m''.round | from the same round + AND ∀ m’ ∈ M: m’.value = value)) | for the same value ``` ### Evidence verification complexity @@ -542,10 +610,10 @@ 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 53), and works as follows: -* Participants start an instance with $Δ=2s$. -* Participants set their timeout for the current round to $Δ*2^{r}$ where $r$ is the round number ($r=0$ for the first round). +* Participants start an instance with `Δ=2s`. +* Participants set their timeout for the current round to `Δ*backOffExpoinent^{r}` where $r$ is the round number ($r=0$ for the first round) and `backOffExponent=2`. Additionally, as an optimization, participants may continue to the subsequent step once the execution of the current step has been determined, without waiting for the timeout. For example, if a participant receives QUALITY messages from all participants, it can proceed to the next step without waiting for the timeout. More generally, if the remaining valid messages to be received cannot change the execution of the step, regardless of the values contained in the messages, then a participant may continue to the next step.