FIP-0086: Using max ticket (#987)

* FIP-0086 Propagate some implementation decisions back to the spec.

* Removed weak quorum

* Review responses.

* Update valid(m) function

* Update fip-0086.md

Remove redundant clause

* First round of changes from Guy's first Audit

* Update GossiPBFT Pseudocode (TODO still update line numbering and other pseudocodes)

* Update references to line numbers

* Fix typos (code statements, indenting)

* Fix valid(m) and validEvidence(m)

* Fix DECIDE format

* Update fip-0086.md

* Changes from 2nd audit by Guy

* Make C a globally scoped variable and update line numbering

* Small fix

* Fix couple comments

* Typos and indentation fixes

* Update to use greatest ticket and adjust by power

* Specify no need to store equivocating messages.

---------

Co-authored-by: Alex North <[email protected]>

Author: ranchalp

FIPS/fip-0086.md

@@ -294,7 +294,7 @@ The receiver of a message only considers messages with valid signatures and disc
 
 Two (or more) messages $m1$ and $m2$ are called _equivocating messages_ if $m1.Sender=m2.Sender \land m1.Instance=m2.Instance \land m1.Value ≠ m2.Value \land m1.MsgType=m2.MsgType \land \texttt(if applicable)\ m1.Round=m2.Round$. We call $m1.Sender$ an _equivocating sender_.
 
-A set of messages $M$ that does not contain equivocating messages is called _clean_. Participants discard all equivocating messages when forming clean sets.
+A set of messages $M$ that does not contain equivocating messages is called _clean_. Participants discard all equivocating messages when forming clean sets. In fact, in the proposed version of GossiPBFT in this document, only one of the equivocating messages needs to be stored (thanks to evidences explicitly validating a message).
 
 
 #### Predicates and functions used in the protocol
@@ -323,10 +323,10 @@ A set of messages $M$ that does not contain equivocating messages is called _cle
       ```
 * `StrongQuorumValue(M)`
     * Returns $v$ if $\texttt{HasStrongQuorumValue}(M)$ holds, $nil$ otherwise.
-* `LowestTicketProposal(M)`
+* `GreatestTicketProposal(M)`
     * Let $M$ be a clean set of CONVERGE messages for the same round.
     * If $M = ∅$, the predicate returns $baseChain$.
-    * If $M \ne ∅$, the predicate returns $m.value$ and $m.evidence$, such that $m$ is the message in $M$ with the lowest ticket ($m.ticket$). M will never be empty as the participant must at least deliver its own CONVERGE message.
+    * If $M \ne ∅$, the predicate returns $m.value$ and $m.evidence$, such that $m$ is the message in $M$ with the greatest ticket after adjusting for the power of the sender ($m.ticket*m.sender.power$). M will never be empty as the participant must at least deliver its own CONVERGE message.
 
 * `Aggregate(M)`
     * Where $M$ is a clean set of messages of the same type $T$, round $r$, and instance $i$, with $v=\texttt{StrongQuorumValue}(M)≠nil$.
@@ -369,7 +369,7 @@ GossiPBFT(instance, inputChain, baseChain, participants) → decision, PoF:
           until timeout expires
 20:       prepareReadyToSend ← False
 21:		  while (not prepareReadyToSend){ 
-22:			  value, evidence ← LowestTicketProposal(M)	\* leader election
+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)
@@ -713,7 +713,7 @@ Because of changes to the EC fork choice rule, this FIP requires a network upgra
          - EB: the common input is decided in the first round.
        - \>⅔ QAP send QUALITY messages for some chain $c$, while the rest for some chain $c'$ ($c$ and $c'$ only share $baseChain$ as common prefix). After sending QUALITY messages, participants that sent $c$ and that hold <⅓ QAP crash.
          - EB: $c$ is decided (participants that sent $c'$ swayed to $c$) in the first round.
-       - Same setup as the test with [three different partitions](#three-partitions), but participants holding less than ⅓ QAP in Q crash after sending QUALITY. One more participant (still in total <⅓ QAP), holding the lowest ticket, crashes in the second round right after sending its CONVERGE.
+       - Same setup as the test with [three different partitions](#three-partitions), but participants holding less than ⅓ QAP in Q crash after sending QUALITY. One more participant (still in total <⅓ QAP), holding the greatest ticket, crashes in the second round right after sending its CONVERGE.
          - EB: the chain voted by the crashed participant (i.e., $c'$) is decided.
      * Crash-recovery:
        - Repeat tests and their EB when, at a given moment, all participants crash and recover (can be done on smaller scales)
@@ -722,7 +722,7 @@ Because of changes to the EC fork choice rule, this FIP requires a network upgra
        - Three partitions, $F$ holding <⅓ QAP, $P$ and $Q$ holding the rest of QAP (with $P$ holding more QAP than $Q$). Participants in $P$ do not receive messages from $Q$ timely, and vice versa, in the first round. Participants in $F$ send QUALITY for $c$ to $P$ and QUALITY for $c'$ to _P'_. They do the same with PREPARE, PROPOSE, COMMIT. Synchrony is restored in round 2.
          - EB: in the first round, participants in $P$ decide $c$. Participants in $Q$ go to round 2, where they also decide $c$. Participants in $F$ are detected as equivocating by $p$ and $Q$ eventually.
        - Same setup as the test with [three different partitions](#three-partitions), but participants holding just less than ⅓ QAP in $Q$ equivocate after sending QUALITY by sending PREPARE and PROPOSE for $c$ to $P$ and for $c'$ to honest participants in $Q$ and $T$.
-         - EB: honest participants in $Q$ and $T$ decide $c'$ in the first round. Once synchrony is restored in the second round, participants in $P$ decide $c'$ too (perhaps subject to the lower ticket being held by non-Byzantine).
+         - EB: honest participants in $Q$ and $T$ decide $c'$ in the first round. Once synchrony is restored in the second round, participants in $P$ decide $c'$ too (perhaps subject to the greatest ticket being held by non-Byzantine).
        - Flooding messages for future instances/rounds
          - Participants holding <⅓ QAP keep sending QUALITY and PREPARE messages for future rounds/instances (as they do not require evidence), intending to flood memory.
            - EB: the system can handle buffering a large load of future messages.